MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: add(0(),x) -> x add(s(x),y) -> s(add(x,y)) cond1(true(),x,y) -> cond2(gr(x,y),x,y) cond2(false(),x,y) -> cond3(eq(x,y),x,y) cond2(true(),x,y) -> cond1(gr(add(x,y),0()),p(x),y) cond3(false(),x,y) -> cond1(gr(add(x,y),0()),x,p(y)) cond3(true(),x,y) -> cond1(gr(add(x,y),0()),p(x),y) eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x - Signature: {add/2,cond1/3,cond2/3,cond3/3,eq/2,gr/2,p/1} / {0/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {add,cond1,cond2,cond3,eq,gr,p} and constructors {0,false ,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs add#(0(),x) -> c_1() add#(s(x),y) -> c_2(add#(x,y)) cond1#(true(),x,y) -> c_3(cond2#(gr(x,y),x,y),gr#(x,y)) cond2#(false(),x,y) -> c_4(cond3#(eq(x,y),x,y),eq#(x,y)) cond2#(true(),x,y) -> c_5(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) cond3#(false(),x,y) -> c_6(cond1#(gr(add(x,y),0()),x,p(y)),gr#(add(x,y),0()),add#(x,y),p#(y)) cond3#(true(),x,y) -> c_7(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) eq#(0(),0()) -> c_8() eq#(0(),s(x)) -> c_9() eq#(s(x),0()) -> c_10() eq#(s(x),s(y)) -> c_11(eq#(x,y)) gr#(0(),x) -> c_12() gr#(s(x),0()) -> c_13() gr#(s(x),s(y)) -> c_14(gr#(x,y)) p#(0()) -> c_15() p#(s(x)) -> c_16() Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: add#(0(),x) -> c_1() add#(s(x),y) -> c_2(add#(x,y)) cond1#(true(),x,y) -> c_3(cond2#(gr(x,y),x,y),gr#(x,y)) cond2#(false(),x,y) -> c_4(cond3#(eq(x,y),x,y),eq#(x,y)) cond2#(true(),x,y) -> c_5(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) cond3#(false(),x,y) -> c_6(cond1#(gr(add(x,y),0()),x,p(y)),gr#(add(x,y),0()),add#(x,y),p#(y)) cond3#(true(),x,y) -> c_7(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) eq#(0(),0()) -> c_8() eq#(0(),s(x)) -> c_9() eq#(s(x),0()) -> c_10() eq#(s(x),s(y)) -> c_11(eq#(x,y)) gr#(0(),x) -> c_12() gr#(s(x),0()) -> c_13() gr#(s(x),s(y)) -> c_14(gr#(x,y)) p#(0()) -> c_15() p#(s(x)) -> c_16() - Weak TRS: add(0(),x) -> x add(s(x),y) -> s(add(x,y)) cond1(true(),x,y) -> cond2(gr(x,y),x,y) cond2(false(),x,y) -> cond3(eq(x,y),x,y) cond2(true(),x,y) -> cond1(gr(add(x,y),0()),p(x),y) cond3(false(),x,y) -> cond1(gr(add(x,y),0()),x,p(y)) cond3(true(),x,y) -> cond1(gr(add(x,y),0()),p(x),y) eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x - Signature: {add/2,cond1/3,cond2/3,cond3/3,eq/2,gr/2,p/1,add#/2,cond1#/3,cond2#/3,cond3#/3,eq#/2,gr#/2,p#/1} / {0/0 ,false/0,s/1,true/0,c_1/0,c_2/1,c_3/2,c_4/2,c_5/4,c_6/4,c_7/4,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {add#,cond1#,cond2#,cond3#,eq#,gr#,p#} and constructors {0 ,false,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: add(0(),x) -> x add(s(x),y) -> s(add(x,y)) eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x add#(0(),x) -> c_1() add#(s(x),y) -> c_2(add#(x,y)) cond1#(true(),x,y) -> c_3(cond2#(gr(x,y),x,y),gr#(x,y)) cond2#(false(),x,y) -> c_4(cond3#(eq(x,y),x,y),eq#(x,y)) cond2#(true(),x,y) -> c_5(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) cond3#(false(),x,y) -> c_6(cond1#(gr(add(x,y),0()),x,p(y)),gr#(add(x,y),0()),add#(x,y),p#(y)) cond3#(true(),x,y) -> c_7(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) eq#(0(),0()) -> c_8() eq#(0(),s(x)) -> c_9() eq#(s(x),0()) -> c_10() eq#(s(x),s(y)) -> c_11(eq#(x,y)) gr#(0(),x) -> c_12() gr#(s(x),0()) -> c_13() gr#(s(x),s(y)) -> c_14(gr#(x,y)) p#(0()) -> c_15() p#(s(x)) -> c_16() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: add#(0(),x) -> c_1() add#(s(x),y) -> c_2(add#(x,y)) cond1#(true(),x,y) -> c_3(cond2#(gr(x,y),x,y),gr#(x,y)) cond2#(false(),x,y) -> c_4(cond3#(eq(x,y),x,y),eq#(x,y)) cond2#(true(),x,y) -> c_5(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) cond3#(false(),x,y) -> c_6(cond1#(gr(add(x,y),0()),x,p(y)),gr#(add(x,y),0()),add#(x,y),p#(y)) cond3#(true(),x,y) -> c_7(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) eq#(0(),0()) -> c_8() eq#(0(),s(x)) -> c_9() eq#(s(x),0()) -> c_10() eq#(s(x),s(y)) -> c_11(eq#(x,y)) gr#(0(),x) -> c_12() gr#(s(x),0()) -> c_13() gr#(s(x),s(y)) -> c_14(gr#(x,y)) p#(0()) -> c_15() p#(s(x)) -> c_16() - Weak TRS: add(0(),x) -> x add(s(x),y) -> s(add(x,y)) eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x - Signature: {add/2,cond1/3,cond2/3,cond3/3,eq/2,gr/2,p/1,add#/2,cond1#/3,cond2#/3,cond3#/3,eq#/2,gr#/2,p#/1} / {0/0 ,false/0,s/1,true/0,c_1/0,c_2/1,c_3/2,c_4/2,c_5/4,c_6/4,c_7/4,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {add#,cond1#,cond2#,cond3#,eq#,gr#,p#} and constructors {0 ,false,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,8,9,10,12,13,15,16} by application of Pre({1,8,9,10,12,13,15,16}) = {2,3,4,5,6,7,11,14}. Here rules are labelled as follows: 1: add#(0(),x) -> c_1() 2: add#(s(x),y) -> c_2(add#(x,y)) 3: cond1#(true(),x,y) -> c_3(cond2#(gr(x,y),x,y),gr#(x,y)) 4: cond2#(false(),x,y) -> c_4(cond3#(eq(x,y),x,y),eq#(x,y)) 5: cond2#(true(),x,y) -> c_5(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) 6: cond3#(false(),x,y) -> c_6(cond1#(gr(add(x,y),0()),x,p(y)),gr#(add(x,y),0()),add#(x,y),p#(y)) 7: cond3#(true(),x,y) -> c_7(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) 8: eq#(0(),0()) -> c_8() 9: eq#(0(),s(x)) -> c_9() 10: eq#(s(x),0()) -> c_10() 11: eq#(s(x),s(y)) -> c_11(eq#(x,y)) 12: gr#(0(),x) -> c_12() 13: gr#(s(x),0()) -> c_13() 14: gr#(s(x),s(y)) -> c_14(gr#(x,y)) 15: p#(0()) -> c_15() 16: p#(s(x)) -> c_16() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: add#(s(x),y) -> c_2(add#(x,y)) cond1#(true(),x,y) -> c_3(cond2#(gr(x,y),x,y),gr#(x,y)) cond2#(false(),x,y) -> c_4(cond3#(eq(x,y),x,y),eq#(x,y)) cond2#(true(),x,y) -> c_5(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) cond3#(false(),x,y) -> c_6(cond1#(gr(add(x,y),0()),x,p(y)),gr#(add(x,y),0()),add#(x,y),p#(y)) cond3#(true(),x,y) -> c_7(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) eq#(s(x),s(y)) -> c_11(eq#(x,y)) gr#(s(x),s(y)) -> c_14(gr#(x,y)) - Weak DPs: add#(0(),x) -> c_1() eq#(0(),0()) -> c_8() eq#(0(),s(x)) -> c_9() eq#(s(x),0()) -> c_10() gr#(0(),x) -> c_12() gr#(s(x),0()) -> c_13() p#(0()) -> c_15() p#(s(x)) -> c_16() - Weak TRS: add(0(),x) -> x add(s(x),y) -> s(add(x,y)) eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x - Signature: {add/2,cond1/3,cond2/3,cond3/3,eq/2,gr/2,p/1,add#/2,cond1#/3,cond2#/3,cond3#/3,eq#/2,gr#/2,p#/1} / {0/0 ,false/0,s/1,true/0,c_1/0,c_2/1,c_3/2,c_4/2,c_5/4,c_6/4,c_7/4,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {add#,cond1#,cond2#,cond3#,eq#,gr#,p#} and constructors {0 ,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:add#(s(x),y) -> c_2(add#(x,y)) -->_1 add#(0(),x) -> c_1():9 -->_1 add#(s(x),y) -> c_2(add#(x,y)):1 2:S:cond1#(true(),x,y) -> c_3(cond2#(gr(x,y),x,y),gr#(x,y)) -->_2 gr#(s(x),s(y)) -> c_14(gr#(x,y)):8 -->_1 cond2#(true(),x,y) -> c_5(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)):4 -->_1 cond2#(false(),x,y) -> c_4(cond3#(eq(x,y),x,y),eq#(x,y)):3 -->_2 gr#(s(x),0()) -> c_13():14 -->_2 gr#(0(),x) -> c_12():13 3:S:cond2#(false(),x,y) -> c_4(cond3#(eq(x,y),x,y),eq#(x,y)) -->_2 eq#(s(x),s(y)) -> c_11(eq#(x,y)):7 -->_1 cond3#(true(),x,y) -> c_7(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)):6 -->_1 cond3#(false(),x,y) -> c_6(cond1#(gr(add(x,y),0()),x,p(y)),gr#(add(x,y),0()),add#(x,y),p#(y)):5 -->_2 eq#(s(x),0()) -> c_10():12 -->_2 eq#(0(),s(x)) -> c_9():11 -->_2 eq#(0(),0()) -> c_8():10 4:S:cond2#(true(),x,y) -> c_5(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) -->_4 p#(s(x)) -> c_16():16 -->_4 p#(0()) -> c_15():15 -->_2 gr#(s(x),0()) -> c_13():14 -->_2 gr#(0(),x) -> c_12():13 -->_3 add#(0(),x) -> c_1():9 -->_1 cond1#(true(),x,y) -> c_3(cond2#(gr(x,y),x,y),gr#(x,y)):2 -->_3 add#(s(x),y) -> c_2(add#(x,y)):1 5:S:cond3#(false(),x,y) -> c_6(cond1#(gr(add(x,y),0()),x,p(y)),gr#(add(x,y),0()),add#(x,y),p#(y)) -->_4 p#(s(x)) -> c_16():16 -->_4 p#(0()) -> c_15():15 -->_2 gr#(s(x),0()) -> c_13():14 -->_2 gr#(0(),x) -> c_12():13 -->_3 add#(0(),x) -> c_1():9 -->_1 cond1#(true(),x,y) -> c_3(cond2#(gr(x,y),x,y),gr#(x,y)):2 -->_3 add#(s(x),y) -> c_2(add#(x,y)):1 6:S:cond3#(true(),x,y) -> c_7(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) -->_4 p#(s(x)) -> c_16():16 -->_4 p#(0()) -> c_15():15 -->_2 gr#(s(x),0()) -> c_13():14 -->_2 gr#(0(),x) -> c_12():13 -->_3 add#(0(),x) -> c_1():9 -->_1 cond1#(true(),x,y) -> c_3(cond2#(gr(x,y),x,y),gr#(x,y)):2 -->_3 add#(s(x),y) -> c_2(add#(x,y)):1 7:S:eq#(s(x),s(y)) -> c_11(eq#(x,y)) -->_1 eq#(s(x),0()) -> c_10():12 -->_1 eq#(0(),s(x)) -> c_9():11 -->_1 eq#(0(),0()) -> c_8():10 -->_1 eq#(s(x),s(y)) -> c_11(eq#(x,y)):7 8:S:gr#(s(x),s(y)) -> c_14(gr#(x,y)) -->_1 gr#(s(x),0()) -> c_13():14 -->_1 gr#(0(),x) -> c_12():13 -->_1 gr#(s(x),s(y)) -> c_14(gr#(x,y)):8 9:W:add#(0(),x) -> c_1() 10:W:eq#(0(),0()) -> c_8() 11:W:eq#(0(),s(x)) -> c_9() 12:W:eq#(s(x),0()) -> c_10() 13:W:gr#(0(),x) -> c_12() 14:W:gr#(s(x),0()) -> c_13() 15:W:p#(0()) -> c_15() 16:W:p#(s(x)) -> c_16() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 10: eq#(0(),0()) -> c_8() 11: eq#(0(),s(x)) -> c_9() 12: eq#(s(x),0()) -> c_10() 15: p#(0()) -> c_15() 16: p#(s(x)) -> c_16() 13: gr#(0(),x) -> c_12() 14: gr#(s(x),0()) -> c_13() 9: add#(0(),x) -> c_1() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: add#(s(x),y) -> c_2(add#(x,y)) cond1#(true(),x,y) -> c_3(cond2#(gr(x,y),x,y),gr#(x,y)) cond2#(false(),x,y) -> c_4(cond3#(eq(x,y),x,y),eq#(x,y)) cond2#(true(),x,y) -> c_5(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) cond3#(false(),x,y) -> c_6(cond1#(gr(add(x,y),0()),x,p(y)),gr#(add(x,y),0()),add#(x,y),p#(y)) cond3#(true(),x,y) -> c_7(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) eq#(s(x),s(y)) -> c_11(eq#(x,y)) gr#(s(x),s(y)) -> c_14(gr#(x,y)) - Weak TRS: add(0(),x) -> x add(s(x),y) -> s(add(x,y)) eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x - Signature: {add/2,cond1/3,cond2/3,cond3/3,eq/2,gr/2,p/1,add#/2,cond1#/3,cond2#/3,cond3#/3,eq#/2,gr#/2,p#/1} / {0/0 ,false/0,s/1,true/0,c_1/0,c_2/1,c_3/2,c_4/2,c_5/4,c_6/4,c_7/4,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {add#,cond1#,cond2#,cond3#,eq#,gr#,p#} and constructors {0 ,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:add#(s(x),y) -> c_2(add#(x,y)) -->_1 add#(s(x),y) -> c_2(add#(x,y)):1 2:S:cond1#(true(),x,y) -> c_3(cond2#(gr(x,y),x,y),gr#(x,y)) -->_2 gr#(s(x),s(y)) -> c_14(gr#(x,y)):8 -->_1 cond2#(true(),x,y) -> c_5(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)):4 -->_1 cond2#(false(),x,y) -> c_4(cond3#(eq(x,y),x,y),eq#(x,y)):3 3:S:cond2#(false(),x,y) -> c_4(cond3#(eq(x,y),x,y),eq#(x,y)) -->_2 eq#(s(x),s(y)) -> c_11(eq#(x,y)):7 -->_1 cond3#(true(),x,y) -> c_7(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)):6 -->_1 cond3#(false(),x,y) -> c_6(cond1#(gr(add(x,y),0()),x,p(y)),gr#(add(x,y),0()),add#(x,y),p#(y)):5 4:S:cond2#(true(),x,y) -> c_5(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) -->_1 cond1#(true(),x,y) -> c_3(cond2#(gr(x,y),x,y),gr#(x,y)):2 -->_3 add#(s(x),y) -> c_2(add#(x,y)):1 5:S:cond3#(false(),x,y) -> c_6(cond1#(gr(add(x,y),0()),x,p(y)),gr#(add(x,y),0()),add#(x,y),p#(y)) -->_1 cond1#(true(),x,y) -> c_3(cond2#(gr(x,y),x,y),gr#(x,y)):2 -->_3 add#(s(x),y) -> c_2(add#(x,y)):1 6:S:cond3#(true(),x,y) -> c_7(cond1#(gr(add(x,y),0()),p(x),y),gr#(add(x,y),0()),add#(x,y),p#(x)) -->_1 cond1#(true(),x,y) -> c_3(cond2#(gr(x,y),x,y),gr#(x,y)):2 -->_3 add#(s(x),y) -> c_2(add#(x,y)):1 7:S:eq#(s(x),s(y)) -> c_11(eq#(x,y)) -->_1 eq#(s(x),s(y)) -> c_11(eq#(x,y)):7 8:S:gr#(s(x),s(y)) -> c_14(gr#(x,y)) -->_1 gr#(s(x),s(y)) -> c_14(gr#(x,y)):8 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: cond2#(true(),x,y) -> c_5(cond1#(gr(add(x,y),0()),p(x),y),add#(x,y)) cond3#(false(),x,y) -> c_6(cond1#(gr(add(x,y),0()),x,p(y)),add#(x,y)) cond3#(true(),x,y) -> c_7(cond1#(gr(add(x,y),0()),p(x),y),add#(x,y)) * Step 6: Failure MAYBE + Considered Problem: - Strict DPs: add#(s(x),y) -> c_2(add#(x,y)) cond1#(true(),x,y) -> c_3(cond2#(gr(x,y),x,y),gr#(x,y)) cond2#(false(),x,y) -> c_4(cond3#(eq(x,y),x,y),eq#(x,y)) cond2#(true(),x,y) -> c_5(cond1#(gr(add(x,y),0()),p(x),y),add#(x,y)) cond3#(false(),x,y) -> c_6(cond1#(gr(add(x,y),0()),x,p(y)),add#(x,y)) cond3#(true(),x,y) -> c_7(cond1#(gr(add(x,y),0()),p(x),y),add#(x,y)) eq#(s(x),s(y)) -> c_11(eq#(x,y)) gr#(s(x),s(y)) -> c_14(gr#(x,y)) - Weak TRS: add(0(),x) -> x add(s(x),y) -> s(add(x,y)) eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x - Signature: {add/2,cond1/3,cond2/3,cond3/3,eq/2,gr/2,p/1,add#/2,cond1#/3,cond2#/3,cond3#/3,eq#/2,gr#/2,p#/1} / {0/0 ,false/0,s/1,true/0,c_1/0,c_2/1,c_3/2,c_4/2,c_5/2,c_6/2,c_7/2,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {add#,cond1#,cond2#,cond3#,eq#,gr#,p#} and constructors {0 ,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE