MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) and(false(),Y) -> false() and(true(),X) -> X first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) from(X) -> cons(X,from(s(X))) if(false(),X,Y) -> Y if(true(),X,Y) -> X - Signature: {add/2,and/2,first/2,from/1,if/3} / {0/0,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {add,and,first,from,if} and constructors {0,cons,false,nil ,s,true} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = MiniSMT} + Details: The input can not be schown compatible. MAYBE