(VAR b x x' xs y )
(STRATEGY INNERMOST)
(RULES 
        head(Cons(x,xs)) -> x
        e(Cons(F,Nil),b) -> False
        e(Cons(T,Nil),b) -> False
        e(Cons(B,Nil),b) -> False
        e(Cons(A,Nil),b) -> e[Match][Cons][Ite][True][Match](A,Nil,b)
        e(Cons(F,Cons(x,xs)),b) -> False
        e(Cons(T,Cons(x,xs)),b) -> False
        e(Cons(B,Cons(x,xs)),b) -> False
        e(Cons(A,Cons(x,xs)),b) -> False
        equal(F,F) -> True
        equal(F,T) -> False
        equal(F,B) -> False
        equal(F,A) -> False
        equal(T,F) -> False
        equal(T,T) -> True
        equal(T,B) -> False
        equal(T,A) -> False
        equal(B,F) -> False
        equal(B,T) -> False
        equal(B,B) -> True
        equal(B,A) -> False
        equal(A,F) -> False
        equal(A,T) -> False
        equal(A,B) -> False
        equal(A,A) -> True
        notEmpty(Cons(x,xs)) -> True
        notEmpty(Nil) -> False
        e(Nil,b) -> False
        t(x,y) -> t[Ite](e(x,y),x,y)
        r(x,y) -> r[Ite](e(x,y),x,y)
        q(x,y) -> q[Ite](e(x,y),x,y)
        p(x,y) -> p[Ite](e(x,y),x,y)
        goal(x,y) -> q(x,y)
        and(False,False) ->= False
        and(True,False) ->= False
        and(False,True) ->= False
        and(True,True) ->= True
        q[Ite](False,x',Cons(F,Cons(F,xs))) ->= q[Ite][False][Ite][True][Ite](and(p(x',Cons(F,Cons(F,xs))),q(x',Cons(F,xs))),x',Cons(F,Cons(F,xs)))
        q[Ite](False,x,Cons(F,Cons(T,xs))) ->= False
        q[Ite](False,x,Cons(F,Cons(B,xs))) ->= False
        q[Ite](False,x,Cons(F,Cons(A,xs))) ->= False
        q[Ite](False,x,Cons(T,Cons(F,xs))) ->= False
        q[Ite](False,x,Cons(T,Cons(T,xs))) ->= False
        q[Ite](False,x,Cons(T,Cons(B,xs))) ->= False
        q[Ite](False,x,Cons(T,Cons(A,xs))) ->= False
        q[Ite](False,x,Cons(B,Cons(F,xs))) ->= False
        q[Ite](False,x,Cons(B,Cons(T,xs))) ->= False
        q[Ite](False,x,Cons(B,Cons(B,xs))) ->= False
        q[Ite](False,x,Cons(B,Cons(A,xs))) ->= False
        q[Ite](False,x,Cons(A,Cons(F,xs))) ->= False
        q[Ite](False,x,Cons(A,Cons(T,xs))) ->= False
        q[Ite](False,x,Cons(A,Cons(B,xs))) ->= False
        q[Ite](False,x,Cons(A,Cons(A,xs))) ->= False
        q[Ite](False,x',Cons(F,Nil)) ->= q[Ite][False][Ite](and(True,and(True,and(False,equal(head(Nil),F)))),x',Cons(F,Nil))
        q[Ite](False,x',Cons(T,Nil)) ->= q[Ite][False][Ite](and(True,and(False,and(False,equal(head(Nil),F)))),x',Cons(T,Nil))
        q[Ite](False,x',Cons(B,Nil)) ->= q[Ite][False][Ite](and(True,and(False,and(False,equal(head(Nil),F)))),x',Cons(B,Nil))
        q[Ite](False,x',Cons(A,Nil)) ->= q[Ite][False][Ite](and(True,and(False,and(False,equal(head(Nil),F)))),x',Cons(A,Nil))
        r[Ite](False,x',Cons(F,xs)) ->= r[Ite][False][Ite][True][Ite](and(q(x',xs),r(x',xs)),x',Cons(F,xs))
        r[Ite](False,x,Cons(T,xs)) ->= False
        r[Ite](False,x,Cons(B,xs)) ->= False
        r[Ite](False,x,Cons(A,xs)) ->= False
        p[Ite](False,x',Cons(F,xs)) ->= and(r(x',Cons(F,xs)),p(x',xs))
        p[Ite](False,x,Cons(T,xs)) ->= False
        p[Ite](False,x,Cons(B,xs)) ->= False
        p[Ite](False,x,Cons(A,xs)) ->= False
        q[Ite][False][Ite](True,x',Cons(x,xs)) ->= q[Ite][False][Ite][True][Ite](and(p(x',Cons(x,xs)),q(x',xs)),x',Cons(x,xs))
        t[Ite](False,x,y) ->= True
        t[Ite](True,x,y) ->= True
        r[Ite](True,x,y) ->= True
        q[Ite](True,x,y) ->= True
        q[Ite][False][Ite](False,x,y) ->= False
        p[Ite](True,x,y) ->= True
)