(VAR x x1 x2 y1 y2 )
(STRATEGY INNERMOST)
(RULES 
        f(C(x1,x2)) -> C(f(x1),f(x2))
        f(Z) -> Z
        eqZList(C(x1,x2),C(y1,y2)) -> and(eqZList(x1,y1),eqZList(x2,y2))
        eqZList(C(x1,x2),Z) -> False
        eqZList(Z,C(y1,y2)) -> False
        eqZList(Z,Z) -> True
        second(C(x1,x2)) -> x2
        first(C(x1,x2)) -> x1
        g(x) -> x
        and(False,False) ->= False
        and(True,False) ->= False
        and(False,True) ->= False
        and(True,True) ->= True
)