MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          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())
      - Weak TRS:
          #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)))
          #equal(@x,@y) -> #eq(@x,@y)
      - Signature:
          {#and/2,#eq/2,#equal/2,appendreverse/2,appendreverse#1/2,bfs/3,bfs#1/3,bfs#2/2,bfs#3/4,bfs#4/7,bfs2/2
          ,bfs2#1/2,dfs/2,dfs#1/2,dfs#2/4,dfs#3/6,dobfs/2,dodfs/2,reverse/1} / {#0/0,#false/0,#neg/1,#pos/1,#s/1
          ,#true/0,::/2,leaf/0,nil/0,node/3}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,appendreverse,appendreverse#1,bfs,bfs#1
          ,bfs#2,bfs#3,bfs#4,bfs2,bfs2#1,dfs,dfs#1,dfs#2,dfs#3,dobfs,dodfs,reverse} and constructors {#0,#false,#neg
          ,#pos,#s,#true,::,leaf,nil,node}
  + Applied Processor:
      MI {miKind = Automaton Nothing, miDimension = 3, miUArgs = NoUArgs, miURules = NoURules, miSelector = Nothing}
  + Details:
      Incompatible
MAYBE