(VAR t e x xs y ys cnf clause assign l ls)

(RULES
  if(true, t, e) -> t
  if(false, t, e) -> e

  member(x, []) -> false
  member(x, ::(y,ys)) -> if(eq(x,y), true, member(x,ys))

  eq([],[])    -> true
  eq(O(x), O(y)) -> eq(x,y)
  eq(O(x), 1(y)) -> false
  eq(1(x), O(y)) -> false
  eq(1(x), 1(y)) -> eq(x,y)

  negate(0(x)) -> 1(x)
  negate(1(x)) -> 0(x)

  choice(::(x,xs))  -> x
  choice(::(x,xs))  -> choice(xs)
  
  guess([]) -> []
  guess(::(clause,cnf)) -> ::(choice(clause), guess(cnf))  

  verify([]) -> true
  verify(::(l,ls)) -> if(member(negate(l),ls), false, verify(ls))

  sat(cnf) -> satck(cnf,guess(cnf))
  satck(cnf,assign) -> if(verify(assign),assign,unsat)

)