// #A: assignment
// #F: formula
// #L: literal
// #R: relation in constraint

// UnitPropagate
#A M || ( & #F F #R D( 1  #L k ) )
(. #A M #L k) || ( & #F F #R D( 1  #L k ) )

// PureLiteral
#A M || #F G 
(. #A M #L k) || #F G

// Decide
#A N || #F G
(. #A N #L k*) || #F G

// Fail
#A P || (& #F G #R R())
FailState

// Backtrack
(. #A M #L l* #A N) || ( & #F F #R C())
(. #A M #L !l) ||(& #F F #R C())

// SemiSuperresolution
(. #A M #L k*) || #F F 
(. #A M #L k*) || (& #F F #R NDL())
// NDL = {The negation of all decision literals in (#A M #L k*)}

// Backjump
(. #A M #L l* #A N) || (& #F G #R C())
(. #A M #L k) || (& #F G #R C())

// Restart
#A M || #F F
{} || #F F