(VAR @a @as @futurequeue @queue @sofar @t @t' @t1 @t2 @toreverse @ts @x @x_1 @x_2 @x_3 @xs @y @y_1 @y_2 @y_3 )
(STRATEGY INNERMOST)
(RULES 
        #equal(@x,@y) -> #eq(@x,@y)
        appendreverse(@toreverse,@sofar) -> appendreverse#1(@toreverse,@sofar)
        appendreverse#1(::(@a,@as),@sofar) -> appendreverse(@as,::(@a,@sofar))
        appendreverse#1(nil,@sofar) -> @sofar
        bfs(@queue,@futurequeue,@x) -> bfs#1(@queue,@futurequeue,@x)
        bfs#1(::(@t,@ts),@futurequeue,@x) -> bfs#3(@t,@futurequeue,@ts,@x)
        bfs#1(nil,@futurequeue,@x) -> bfs#2(@futurequeue,@x)
        bfs#2(::(@t,@ts),@x) -> bfs(reverse(::(@t,@ts)),nil,@x)
        bfs#2(nil,@x) -> leaf
        bfs#3(leaf,@futurequeue,@ts,@x) -> bfs(@ts,@futurequeue,@x)
        bfs#3(node(@y,@t1,@t2),@futurequeue,@ts,@x) -> bfs#4(#equal(@x,@y),@futurequeue,@t1,@t2,@ts,@x,@y)
        bfs#4(#false,@futurequeue,@t1,@t2,@ts,@x,@y) -> bfs(@ts,::(@t2,::(@t1,@futurequeue)),@x)
        bfs#4(#true,@futurequeue,@t1,@t2,@ts,@x,@y) -> node(@y,@t1,@t2)
        bfs2(@t,@x) -> bfs2#1(dobfs(@t,@x),@x)
        bfs2#1(@t',@x) -> dobfs(@t',@x)
        dfs(@queue,@x) -> dfs#1(@queue,@x)
        dfs#1(::(@t,@ts),@x) -> dfs#2(@t,@t,@ts,@x)
        dfs#1(nil,@x) -> leaf
        dfs#2(leaf,@t,@ts,@x) -> dfs(@ts,@x)
        dfs#2(node(@a,@t1,@t2),@t,@ts,@x) -> dfs#3(#equal(@a,@x),@t,@t1,@t2,@ts,@x)
        dfs#3(#false,@t,@t1,@t2,@ts,@x) -> dfs(::(@t1,::(@t2,@ts)),@x)
        dfs#3(#true,@t,@t1,@t2,@ts,@x) -> @t
        dobfs(@t,@x) -> bfs(::(@t,nil),nil,@x)
        dodfs(@t,@x) -> dfs(::(@t,nil),@x)
        reverse(@xs) -> appendreverse(@xs,nil)
        #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),leaf) ->= #false
        #eq(::(@x_1,@x_2),nil) ->= #false
        #eq(::(@x_1,@x_2),node(@y_1,@y_2,@y_3)) ->= #false
        #eq(leaf,::(@y_1,@y_2)) ->= #false
        #eq(leaf,leaf) ->= #true
        #eq(leaf,nil) ->= #false
        #eq(leaf,node(@y_1,@y_2,@y_3)) ->= #false
        #eq(nil,::(@y_1,@y_2)) ->= #false
        #eq(nil,leaf) ->= #false
        #eq(nil,nil) ->= #true
        #eq(nil,node(@y_1,@y_2,@y_3)) ->= #false
        #eq(node(@x_1,@x_2,@x_3),::(@y_1,@y_2)) ->= #false
        #eq(node(@x_1,@x_2,@x_3),leaf) ->= #false
        #eq(node(@x_1,@x_2,@x_3),nil) ->= #false
        #eq(node(@x_1,@x_2,@x_3),node(@y_1,@y_2,@y_3)) ->= #and(#eq(@x_1,@y_1),#and(#eq(@x_2,@y_2),#eq(@x_3,@y_3)))
)