MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          #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)
      - 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),nil()) -> #false()
          #eq(nil(),::(@y_1,@y_2)) -> #false()
          #eq(nil(),nil()) -> #true()
      - Signature:
          {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0
          ,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove
          ,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
  + Applied Processor:
      Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = MiniSMT}
  + Details:
      The input can not be schown compatible.
MAYBE