(VAR x1 x2 y y1 y2 )
(STRATEGY INNERMOST)
(RULES 
        a(C(x1,x2),y) -> C(a(x1,y),a(x2,C(x1,x2)))
        a(Z,y) -> 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
        and(False,False) ->= False
        and(True,False) ->= False
        and(False,True) ->= False
        and(True,True) ->= True
)