(VAR @l @l1 @l2 @x @x_1 @x_2 @xs @y @y_1 @y_2 @ys )
(STRATEGY INNERMOST)
(RULES 
        #equal(@x,@y) -> #eq(@x,@y)
        and(@x,@y) -> #and(@x,@y)
        eq(@l1,@l2) -> eq#1(@l1,@l2)
        eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
        eq#1(nil,@l2) -> eq#2(@l2)
        eq#2(::(@y,@ys)) -> #false
        eq#2(nil) -> #true
        eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
        eq#3(nil,@x,@xs) -> #false
        nub(@l) -> nub#1(@l)
        nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
        nub#1(nil) -> nil
        remove(@x,@l) -> remove#1(@l,@x)
        remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
        remove#1(nil,@x) -> nil
        remove#2(#false,@x,@y,@ys) -> ::(@y,remove(@x,@ys))
        remove#2(#true,@x,@y,@ys) -> remove(@x,@ys)
        #and(#false,#false) ->= #false
        #and(#false,#true) ->= #false
        #and(#true,#false) ->= #false
        #and(#true,#true) ->= #true
        #eq(#0,#0) ->= #true
        #eq(#0,#neg(@y)) ->= #false
        #eq(#0,#pos(@y)) ->= #false
        #eq(#0,#s(@y)) ->= #false
        #eq(#neg(@x),#0) ->= #false
        #eq(#neg(@x),#neg(@y)) ->= #eq(@x,@y)
        #eq(#neg(@x),#pos(@y)) ->= #false
        #eq(#pos(@x),#0) ->= #false
        #eq(#pos(@x),#neg(@y)) ->= #false
        #eq(#pos(@x),#pos(@y)) ->= #eq(@x,@y)
        #eq(#s(@x),#0) ->= #false
        #eq(#s(@x),#s(@y)) ->= #eq(@x,@y)
        #eq(::(@x_1,@x_2),::(@y_1,@y_2)) ->= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
        #eq(::(@x_1,@x_2),nil) ->= #false
        #eq(nil,::(@y_1,@y_2)) ->= #false
        #eq(nil,nil) ->= #true
)