(VAR x x' xs xs' y )
(STRATEGY INNERMOST)
(RULES 
        lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs)
        lte(Cons(x,xs),Nil) -> False
        even(Cons(x,Nil)) -> False
        even(Cons(x',Cons(x,xs))) -> even(xs)
        notEmpty(Cons(x,xs)) -> True
        notEmpty(Nil) -> False
        lte(Nil,y) -> True
        even(Nil) -> True
        goal(x,y) -> and(lte(x,y),even(x))
        and(False,False) ->= False
        and(True,False) ->= False
        and(False,True) ->= False
        and(True,True) ->= True
)