MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: eql(Cons(x,xs)) -> eql(Cons(x,xs)) eql(Nil()) -> Nil() goal(x) -> nesteql(x) nesteql(Cons(x,xs)) -> nesteql(eql(Cons(x,xs))) nesteql(Nil()) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil()))))))))))))))))) number17(n) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil()))))))))))))))))) - Signature: {eql/1,goal/1,nesteql/1,number17/1} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {eql,goal,nesteql,number17} and constructors {Cons,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