(STRATEGY
    INNERMOST)

(VAR
    assign clause cnf e l ls t x xs
    y ys)
(DATATYPES
    A = µX.< true, false, nil, cons(X, X), O(X), 0(X), 1(X), unsat >)
(SIGNATURES
    if :: [A x A x A] -> A
    member :: [A x A] -> A
    eq :: [A x A] -> A
    negate :: [A] -> A
    choice :: [A] -> A
    guess :: [A] -> A
    verify :: [A] -> A
    sat :: [A] -> A
    satck :: [A x A] -> A)
(RULES
    if(true(),t,e) -> t
    if(false(),t,e) -> e
    member(x,nil()) -> false()
    member(x,cons(y,ys)) -> if(eq(x
                                 ,y)
                              ,true()
                              ,member(x,ys))
    eq(nil(),nil()) -> true()
    eq(O(x),0(y)) -> eq(x,y)
    eq(0(x),1(y)) -> false()
    eq(1(x),0(y)) -> false()
    eq(1(x),1(y)) -> eq(x,y)
    negate(0(x)) -> 1(x)
    negate(1(x)) -> 0(x)
    choice(cons(x,xs)) -> x
    choice(cons(x,xs)) -> choice(xs)
    guess(nil()) -> nil()
    guess(cons(clause,cnf)) ->
      cons(choice(clause),guess(cnf))
    verify(nil()) -> true()
    verify(cons(l,ls)) ->
      if(member(negate(l),ls)
        ,false()
        ,verify(ls))
    sat(cnf) -> satck(cnf
                     ,guess(cnf))
    satck(cnf,assign) ->
      if(verify(assign)
        ,assign
        ,unsat()))