MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: *(#(),x) -> #() *(*(x,y),z) -> *(x,*(y,z)) *(0(x),y) -> 0(*(x,y)) *(1(x),y) -> +(0(*(x,y)),y) +(x,#()) -> x +(#(),x) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(x),0(y)) -> 0(+(x,y)) +(0(x),1(y)) -> 1(+(x,y)) +(1(x),0(y)) -> 1(+(x,y)) +(1(x),1(y)) -> 0(+(+(x,y),1(#()))) 0(#()) -> #() prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> 1(#()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0(#()) - Signature: {*/2,+/2,0/1,prod/1,sum/1} / {#/0,1/1,cons/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {*,+,0,prod,sum} and constructors {#,1,cons,nil} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = Z3} + Details: The input can not be schown compatible. MAYBE