MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { active(and(X1, X2)) -> and(active(X1), X2) , active(and(true(), X)) -> mark(X) , active(and(false(), Y)) -> mark(false()) , active(if(X1, X2, X3)) -> if(active(X1), X2, X3) , active(if(true(), X, Y)) -> mark(X) , active(if(false(), X, Y)) -> mark(Y) , active(add(X1, X2)) -> add(active(X1), X2) , active(add(0(), X)) -> mark(X) , active(add(s(X), Y)) -> mark(s(add(X, Y))) , active(first(X1, X2)) -> first(X1, active(X2)) , active(first(X1, X2)) -> first(active(X1), X2) , active(first(0(), X)) -> mark(nil()) , active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))) , active(from(X)) -> mark(cons(X, from(s(X)))) , and(mark(X1), X2) -> mark(and(X1, X2)) , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) , if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)) , if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)) , add(mark(X1), X2) -> mark(add(X1, X2)) , add(ok(X1), ok(X2)) -> ok(add(X1, X2)) , s(ok(X)) -> ok(s(X)) , first(X1, mark(X2)) -> mark(first(X1, X2)) , first(mark(X1), X2) -> mark(first(X1, X2)) , first(ok(X1), ok(X2)) -> ok(first(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , from(ok(X)) -> ok(from(X)) , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) , proper(true()) -> ok(true()) , proper(false()) -> ok(false()) , proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)) , proper(add(X1, X2)) -> add(proper(X1), proper(X2)) , proper(0()) -> ok(0()) , proper(s(X)) -> s(proper(X)) , proper(first(X1, X2)) -> first(proper(X1), proper(X2)) , proper(nil()) -> ok(nil()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(from(X)) -> from(proper(X)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { active^#(and(X1, X2)) -> c_1(and^#(active(X1), X2)) , active^#(and(true(), X)) -> c_2(X) , active^#(and(false(), Y)) -> c_3() , active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3)) , active^#(if(true(), X, Y)) -> c_5(X) , active^#(if(false(), X, Y)) -> c_6(Y) , active^#(add(X1, X2)) -> c_7(add^#(active(X1), X2)) , active^#(add(0(), X)) -> c_8(X) , active^#(add(s(X), Y)) -> c_9(s^#(add(X, Y))) , active^#(first(X1, X2)) -> c_10(first^#(X1, active(X2))) , active^#(first(X1, X2)) -> c_11(first^#(active(X1), X2)) , active^#(first(0(), X)) -> c_12() , active^#(first(s(X), cons(Y, Z))) -> c_13(cons^#(Y, first(X, Z))) , active^#(from(X)) -> c_14(cons^#(X, from(s(X)))) , and^#(mark(X1), X2) -> c_15(and^#(X1, X2)) , and^#(ok(X1), ok(X2)) -> c_16(and^#(X1, X2)) , if^#(mark(X1), X2, X3) -> c_17(if^#(X1, X2, X3)) , if^#(ok(X1), ok(X2), ok(X3)) -> c_18(if^#(X1, X2, X3)) , add^#(mark(X1), X2) -> c_19(add^#(X1, X2)) , add^#(ok(X1), ok(X2)) -> c_20(add^#(X1, X2)) , s^#(ok(X)) -> c_21(s^#(X)) , first^#(X1, mark(X2)) -> c_22(first^#(X1, X2)) , first^#(mark(X1), X2) -> c_23(first^#(X1, X2)) , first^#(ok(X1), ok(X2)) -> c_24(first^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_25(cons^#(X1, X2)) , from^#(ok(X)) -> c_26(from^#(X)) , proper^#(and(X1, X2)) -> c_27(and^#(proper(X1), proper(X2))) , proper^#(true()) -> c_28() , proper^#(false()) -> c_29() , proper^#(if(X1, X2, X3)) -> c_30(if^#(proper(X1), proper(X2), proper(X3))) , proper^#(add(X1, X2)) -> c_31(add^#(proper(X1), proper(X2))) , proper^#(0()) -> c_32() , proper^#(s(X)) -> c_33(s^#(proper(X))) , proper^#(first(X1, X2)) -> c_34(first^#(proper(X1), proper(X2))) , proper^#(nil()) -> c_35() , proper^#(cons(X1, X2)) -> c_36(cons^#(proper(X1), proper(X2))) , proper^#(from(X)) -> c_37(from^#(proper(X))) , top^#(mark(X)) -> c_38(top^#(proper(X))) , top^#(ok(X)) -> c_39(top^#(active(X))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { active^#(and(X1, X2)) -> c_1(and^#(active(X1), X2)) , active^#(and(true(), X)) -> c_2(X) , active^#(and(false(), Y)) -> c_3() , active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3)) , active^#(if(true(), X, Y)) -> c_5(X) , active^#(if(false(), X, Y)) -> c_6(Y) , active^#(add(X1, X2)) -> c_7(add^#(active(X1), X2)) , active^#(add(0(), X)) -> c_8(X) , active^#(add(s(X), Y)) -> c_9(s^#(add(X, Y))) , active^#(first(X1, X2)) -> c_10(first^#(X1, active(X2))) , active^#(first(X1, X2)) -> c_11(first^#(active(X1), X2)) , active^#(first(0(), X)) -> c_12() , active^#(first(s(X), cons(Y, Z))) -> c_13(cons^#(Y, first(X, Z))) , active^#(from(X)) -> c_14(cons^#(X, from(s(X)))) , and^#(mark(X1), X2) -> c_15(and^#(X1, X2)) , and^#(ok(X1), ok(X2)) -> c_16(and^#(X1, X2)) , if^#(mark(X1), X2, X3) -> c_17(if^#(X1, X2, X3)) , if^#(ok(X1), ok(X2), ok(X3)) -> c_18(if^#(X1, X2, X3)) , add^#(mark(X1), X2) -> c_19(add^#(X1, X2)) , add^#(ok(X1), ok(X2)) -> c_20(add^#(X1, X2)) , s^#(ok(X)) -> c_21(s^#(X)) , first^#(X1, mark(X2)) -> c_22(first^#(X1, X2)) , first^#(mark(X1), X2) -> c_23(first^#(X1, X2)) , first^#(ok(X1), ok(X2)) -> c_24(first^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_25(cons^#(X1, X2)) , from^#(ok(X)) -> c_26(from^#(X)) , proper^#(and(X1, X2)) -> c_27(and^#(proper(X1), proper(X2))) , proper^#(true()) -> c_28() , proper^#(false()) -> c_29() , proper^#(if(X1, X2, X3)) -> c_30(if^#(proper(X1), proper(X2), proper(X3))) , proper^#(add(X1, X2)) -> c_31(add^#(proper(X1), proper(X2))) , proper^#(0()) -> c_32() , proper^#(s(X)) -> c_33(s^#(proper(X))) , proper^#(first(X1, X2)) -> c_34(first^#(proper(X1), proper(X2))) , proper^#(nil()) -> c_35() , proper^#(cons(X1, X2)) -> c_36(cons^#(proper(X1), proper(X2))) , proper^#(from(X)) -> c_37(from^#(proper(X))) , top^#(mark(X)) -> c_38(top^#(proper(X))) , top^#(ok(X)) -> c_39(top^#(active(X))) } Strict Trs: { active(and(X1, X2)) -> and(active(X1), X2) , active(and(true(), X)) -> mark(X) , active(and(false(), Y)) -> mark(false()) , active(if(X1, X2, X3)) -> if(active(X1), X2, X3) , active(if(true(), X, Y)) -> mark(X) , active(if(false(), X, Y)) -> mark(Y) , active(add(X1, X2)) -> add(active(X1), X2) , active(add(0(), X)) -> mark(X) , active(add(s(X), Y)) -> mark(s(add(X, Y))) , active(first(X1, X2)) -> first(X1, active(X2)) , active(first(X1, X2)) -> first(active(X1), X2) , active(first(0(), X)) -> mark(nil()) , active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))) , active(from(X)) -> mark(cons(X, from(s(X)))) , and(mark(X1), X2) -> mark(and(X1, X2)) , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) , if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)) , if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)) , add(mark(X1), X2) -> mark(add(X1, X2)) , add(ok(X1), ok(X2)) -> ok(add(X1, X2)) , s(ok(X)) -> ok(s(X)) , first(X1, mark(X2)) -> mark(first(X1, X2)) , first(mark(X1), X2) -> mark(first(X1, X2)) , first(ok(X1), ok(X2)) -> ok(first(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , from(ok(X)) -> ok(from(X)) , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) , proper(true()) -> ok(true()) , proper(false()) -> ok(false()) , proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)) , proper(add(X1, X2)) -> add(proper(X1), proper(X2)) , proper(0()) -> ok(0()) , proper(s(X)) -> s(proper(X)) , proper(first(X1, X2)) -> first(proper(X1), proper(X2)) , proper(nil()) -> ok(nil()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(from(X)) -> from(proper(X)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE Consider the dependency graph: 1: active^#(and(X1, X2)) -> c_1(and^#(active(X1), X2)) -->_1 and^#(ok(X1), ok(X2)) -> c_16(and^#(X1, X2)) :16 -->_1 and^#(mark(X1), X2) -> c_15(and^#(X1, X2)) :15 2: active^#(and(true(), X)) -> c_2(X) -->_1 top^#(ok(X)) -> c_39(top^#(active(X))) :39 -->_1 top^#(mark(X)) -> c_38(top^#(proper(X))) :38 -->_1 proper^#(from(X)) -> c_37(from^#(proper(X))) :37 -->_1 proper^#(cons(X1, X2)) -> c_36(cons^#(proper(X1), proper(X2))) :36 -->_1 proper^#(first(X1, X2)) -> c_34(first^#(proper(X1), proper(X2))) :34 -->_1 proper^#(s(X)) -> c_33(s^#(proper(X))) :33 -->_1 proper^#(add(X1, X2)) -> c_31(add^#(proper(X1), proper(X2))) :31 -->_1 proper^#(if(X1, X2, X3)) -> c_30(if^#(proper(X1), proper(X2), proper(X3))) :30 -->_1 proper^#(and(X1, X2)) -> c_27(and^#(proper(X1), proper(X2))) :27 -->_1 from^#(ok(X)) -> c_26(from^#(X)) :26 -->_1 cons^#(ok(X1), ok(X2)) -> c_25(cons^#(X1, X2)) :25 -->_1 first^#(ok(X1), ok(X2)) -> c_24(first^#(X1, X2)) :24 -->_1 first^#(mark(X1), X2) -> c_23(first^#(X1, X2)) :23 -->_1 first^#(X1, mark(X2)) -> c_22(first^#(X1, X2)) :22 -->_1 s^#(ok(X)) -> c_21(s^#(X)) :21 -->_1 add^#(ok(X1), ok(X2)) -> c_20(add^#(X1, X2)) :20 -->_1 add^#(mark(X1), X2) -> c_19(add^#(X1, X2)) :19 -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_18(if^#(X1, X2, X3)) :18 -->_1 if^#(mark(X1), X2, X3) -> c_17(if^#(X1, X2, X3)) :17 -->_1 and^#(ok(X1), ok(X2)) -> c_16(and^#(X1, X2)) :16 -->_1 and^#(mark(X1), X2) -> c_15(and^#(X1, X2)) :15 -->_1 active^#(from(X)) -> c_14(cons^#(X, from(s(X)))) :14 -->_1 active^#(first(s(X), cons(Y, Z))) -> c_13(cons^#(Y, first(X, Z))) :13 -->_1 active^#(first(X1, X2)) -> c_11(first^#(active(X1), X2)) :11 -->_1 active^#(first(X1, X2)) -> c_10(first^#(X1, active(X2))) :10 -->_1 active^#(add(s(X), Y)) -> c_9(s^#(add(X, Y))) :9 -->_1 active^#(add(0(), X)) -> c_8(X) :8 -->_1 active^#(add(X1, X2)) -> c_7(add^#(active(X1), X2)) :7 -->_1 active^#(if(false(), X, Y)) -> c_6(Y) :6 -->_1 active^#(if(true(), X, Y)) -> c_5(X) :5 -->_1 active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3)) :4 -->_1 proper^#(nil()) -> c_35() :35 -->_1 proper^#(0()) -> c_32() :32 -->_1 proper^#(false()) -> c_29() :29 -->_1 proper^#(true()) -> c_28() :28 -->_1 active^#(first(0(), X)) -> c_12() :12 -->_1 active^#(and(false(), Y)) -> c_3() :3 -->_1 active^#(and(true(), X)) -> c_2(X) :2 -->_1 active^#(and(X1, X2)) -> c_1(and^#(active(X1), X2)) :1 3: active^#(and(false(), Y)) -> c_3() 4: active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3)) -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_18(if^#(X1, X2, X3)) :18 -->_1 if^#(mark(X1), X2, X3) -> c_17(if^#(X1, X2, X3)) :17 5: active^#(if(true(), X, Y)) -> c_5(X) -->_1 top^#(ok(X)) -> c_39(top^#(active(X))) :39 -->_1 top^#(mark(X)) -> c_38(top^#(proper(X))) :38 -->_1 proper^#(from(X)) -> c_37(from^#(proper(X))) :37 -->_1 proper^#(cons(X1, X2)) -> c_36(cons^#(proper(X1), proper(X2))) :36 -->_1 proper^#(first(X1, X2)) -> c_34(first^#(proper(X1), proper(X2))) :34 -->_1 proper^#(s(X)) -> c_33(s^#(proper(X))) :33 -->_1 proper^#(add(X1, X2)) -> c_31(add^#(proper(X1), proper(X2))) :31 -->_1 proper^#(if(X1, X2, X3)) -> c_30(if^#(proper(X1), proper(X2), proper(X3))) :30 -->_1 proper^#(and(X1, X2)) -> c_27(and^#(proper(X1), proper(X2))) :27 -->_1 from^#(ok(X)) -> c_26(from^#(X)) :26 -->_1 cons^#(ok(X1), ok(X2)) -> c_25(cons^#(X1, X2)) :25 -->_1 first^#(ok(X1), ok(X2)) -> c_24(first^#(X1, X2)) :24 -->_1 first^#(mark(X1), X2) -> c_23(first^#(X1, X2)) :23 -->_1 first^#(X1, mark(X2)) -> c_22(first^#(X1, X2)) :22 -->_1 s^#(ok(X)) -> c_21(s^#(X)) :21 -->_1 add^#(ok(X1), ok(X2)) -> c_20(add^#(X1, X2)) :20 -->_1 add^#(mark(X1), X2) -> c_19(add^#(X1, X2)) :19 -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_18(if^#(X1, X2, X3)) :18 -->_1 if^#(mark(X1), X2, X3) -> c_17(if^#(X1, X2, X3)) :17 -->_1 and^#(ok(X1), ok(X2)) -> c_16(and^#(X1, X2)) :16 -->_1 and^#(mark(X1), X2) -> c_15(and^#(X1, X2)) :15 -->_1 active^#(from(X)) -> c_14(cons^#(X, from(s(X)))) :14 -->_1 active^#(first(s(X), cons(Y, Z))) -> c_13(cons^#(Y, first(X, Z))) :13 -->_1 active^#(first(X1, X2)) -> c_11(first^#(active(X1), X2)) :11 -->_1 active^#(first(X1, X2)) -> c_10(first^#(X1, active(X2))) :10 -->_1 active^#(add(s(X), Y)) -> c_9(s^#(add(X, Y))) :9 -->_1 active^#(add(0(), X)) -> c_8(X) :8 -->_1 active^#(add(X1, X2)) -> c_7(add^#(active(X1), X2)) :7 -->_1 active^#(if(false(), X, Y)) -> c_6(Y) :6 -->_1 proper^#(nil()) -> c_35() :35 -->_1 proper^#(0()) -> c_32() :32 -->_1 proper^#(false()) -> c_29() :29 -->_1 proper^#(true()) -> c_28() :28 -->_1 active^#(first(0(), X)) -> c_12() :12 -->_1 active^#(if(true(), X, Y)) -> c_5(X) :5 -->_1 active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3)) :4 -->_1 active^#(and(false(), Y)) -> c_3() :3 -->_1 active^#(and(true(), X)) -> c_2(X) :2 -->_1 active^#(and(X1, X2)) -> c_1(and^#(active(X1), X2)) :1 6: active^#(if(false(), X, Y)) -> c_6(Y) -->_1 top^#(ok(X)) -> c_39(top^#(active(X))) :39 -->_1 top^#(mark(X)) -> c_38(top^#(proper(X))) :38 -->_1 proper^#(from(X)) -> c_37(from^#(proper(X))) :37 -->_1 proper^#(cons(X1, X2)) -> c_36(cons^#(proper(X1), proper(X2))) :36 -->_1 proper^#(first(X1, X2)) -> c_34(first^#(proper(X1), proper(X2))) :34 -->_1 proper^#(s(X)) -> c_33(s^#(proper(X))) :33 -->_1 proper^#(add(X1, X2)) -> c_31(add^#(proper(X1), proper(X2))) :31 -->_1 proper^#(if(X1, X2, X3)) -> c_30(if^#(proper(X1), proper(X2), proper(X3))) :30 -->_1 proper^#(and(X1, X2)) -> c_27(and^#(proper(X1), proper(X2))) :27 -->_1 from^#(ok(X)) -> c_26(from^#(X)) :26 -->_1 cons^#(ok(X1), ok(X2)) -> c_25(cons^#(X1, X2)) :25 -->_1 first^#(ok(X1), ok(X2)) -> c_24(first^#(X1, X2)) :24 -->_1 first^#(mark(X1), X2) -> c_23(first^#(X1, X2)) :23 -->_1 first^#(X1, mark(X2)) -> c_22(first^#(X1, X2)) :22 -->_1 s^#(ok(X)) -> c_21(s^#(X)) :21 -->_1 add^#(ok(X1), ok(X2)) -> c_20(add^#(X1, X2)) :20 -->_1 add^#(mark(X1), X2) -> c_19(add^#(X1, X2)) :19 -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_18(if^#(X1, X2, X3)) :18 -->_1 if^#(mark(X1), X2, X3) -> c_17(if^#(X1, X2, X3)) :17 -->_1 and^#(ok(X1), ok(X2)) -> c_16(and^#(X1, X2)) :16 -->_1 and^#(mark(X1), X2) -> c_15(and^#(X1, X2)) :15 -->_1 active^#(from(X)) -> c_14(cons^#(X, from(s(X)))) :14 -->_1 active^#(first(s(X), cons(Y, Z))) -> c_13(cons^#(Y, first(X, Z))) :13 -->_1 active^#(first(X1, X2)) -> c_11(first^#(active(X1), X2)) :11 -->_1 active^#(first(X1, X2)) -> c_10(first^#(X1, active(X2))) :10 -->_1 active^#(add(s(X), Y)) -> c_9(s^#(add(X, Y))) :9 -->_1 active^#(add(0(), X)) -> c_8(X) :8 -->_1 active^#(add(X1, X2)) -> c_7(add^#(active(X1), X2)) :7 -->_1 proper^#(nil()) -> c_35() :35 -->_1 proper^#(0()) -> c_32() :32 -->_1 proper^#(false()) -> c_29() :29 -->_1 proper^#(true()) -> c_28() :28 -->_1 active^#(first(0(), X)) -> c_12() :12 -->_1 active^#(if(false(), X, Y)) -> c_6(Y) :6 -->_1 active^#(if(true(), X, Y)) -> c_5(X) :5 -->_1 active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3)) :4 -->_1 active^#(and(false(), Y)) -> c_3() :3 -->_1 active^#(and(true(), X)) -> c_2(X) :2 -->_1 active^#(and(X1, X2)) -> c_1(and^#(active(X1), X2)) :1 7: active^#(add(X1, X2)) -> c_7(add^#(active(X1), X2)) -->_1 add^#(ok(X1), ok(X2)) -> c_20(add^#(X1, X2)) :20 -->_1 add^#(mark(X1), X2) -> c_19(add^#(X1, X2)) :19 8: active^#(add(0(), X)) -> c_8(X) -->_1 top^#(ok(X)) -> c_39(top^#(active(X))) :39 -->_1 top^#(mark(X)) -> c_38(top^#(proper(X))) :38 -->_1 proper^#(from(X)) -> c_37(from^#(proper(X))) :37 -->_1 proper^#(cons(X1, X2)) -> c_36(cons^#(proper(X1), proper(X2))) :36 -->_1 proper^#(first(X1, X2)) -> c_34(first^#(proper(X1), proper(X2))) :34 -->_1 proper^#(s(X)) -> c_33(s^#(proper(X))) :33 -->_1 proper^#(add(X1, X2)) -> c_31(add^#(proper(X1), proper(X2))) :31 -->_1 proper^#(if(X1, X2, X3)) -> c_30(if^#(proper(X1), proper(X2), proper(X3))) :30 -->_1 proper^#(and(X1, X2)) -> c_27(and^#(proper(X1), proper(X2))) :27 -->_1 from^#(ok(X)) -> c_26(from^#(X)) :26 -->_1 cons^#(ok(X1), ok(X2)) -> c_25(cons^#(X1, X2)) :25 -->_1 first^#(ok(X1), ok(X2)) -> c_24(first^#(X1, X2)) :24 -->_1 first^#(mark(X1), X2) -> c_23(first^#(X1, X2)) :23 -->_1 first^#(X1, mark(X2)) -> c_22(first^#(X1, X2)) :22 -->_1 s^#(ok(X)) -> c_21(s^#(X)) :21 -->_1 add^#(ok(X1), ok(X2)) -> c_20(add^#(X1, X2)) :20 -->_1 add^#(mark(X1), X2) -> c_19(add^#(X1, X2)) :19 -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_18(if^#(X1, X2, X3)) :18 -->_1 if^#(mark(X1), X2, X3) -> c_17(if^#(X1, X2, X3)) :17 -->_1 and^#(ok(X1), ok(X2)) -> c_16(and^#(X1, X2)) :16 -->_1 and^#(mark(X1), X2) -> c_15(and^#(X1, X2)) :15 -->_1 active^#(from(X)) -> c_14(cons^#(X, from(s(X)))) :14 -->_1 active^#(first(s(X), cons(Y, Z))) -> c_13(cons^#(Y, first(X, Z))) :13 -->_1 active^#(first(X1, X2)) -> c_11(first^#(active(X1), X2)) :11 -->_1 active^#(first(X1, X2)) -> c_10(first^#(X1, active(X2))) :10 -->_1 active^#(add(s(X), Y)) -> c_9(s^#(add(X, Y))) :9 -->_1 proper^#(nil()) -> c_35() :35 -->_1 proper^#(0()) -> c_32() :32 -->_1 proper^#(false()) -> c_29() :29 -->_1 proper^#(true()) -> c_28() :28 -->_1 active^#(first(0(), X)) -> c_12() :12 -->_1 active^#(add(0(), X)) -> c_8(X) :8 -->_1 active^#(add(X1, X2)) -> c_7(add^#(active(X1), X2)) :7 -->_1 active^#(if(false(), X, Y)) -> c_6(Y) :6 -->_1 active^#(if(true(), X, Y)) -> c_5(X) :5 -->_1 active^#(if(X1, X2, X3)) -> c_4(if^#(active(X1), X2, X3)) :4 -->_1 active^#(and(false(), Y)) -> c_3() :3 -->_1 active^#(and(true(), X)) -> c_2(X) :2 -->_1 active^#(and(X1, X2)) -> c_1(and^#(active(X1), X2)) :1 9: active^#(add(s(X), Y)) -> c_9(s^#(add(X, Y))) -->_1 s^#(ok(X)) -> c_21(s^#(X)) :21 10: active^#(first(X1, X2)) -> c_10(first^#(X1, active(X2))) -->_1 first^#(ok(X1), ok(X2)) -> c_24(first^#(X1, X2)) :24 -->_1 first^#(mark(X1), X2) -> c_23(first^#(X1, X2)) :23 -->_1 first^#(X1, mark(X2)) -> c_22(first^#(X1, X2)) :22 11: active^#(first(X1, X2)) -> c_11(first^#(active(X1), X2)) -->_1 first^#(ok(X1), ok(X2)) -> c_24(first^#(X1, X2)) :24 -->_1 first^#(mark(X1), X2) -> c_23(first^#(X1, X2)) :23 -->_1 first^#(X1, mark(X2)) -> c_22(first^#(X1, X2)) :22 12: active^#(first(0(), X)) -> c_12() 13: active^#(first(s(X), cons(Y, Z))) -> c_13(cons^#(Y, first(X, Z))) -->_1 cons^#(ok(X1), ok(X2)) -> c_25(cons^#(X1, X2)) :25 14: active^#(from(X)) -> c_14(cons^#(X, from(s(X)))) -->_1 cons^#(ok(X1), ok(X2)) -> c_25(cons^#(X1, X2)) :25 15: and^#(mark(X1), X2) -> c_15(and^#(X1, X2)) -->_1 and^#(ok(X1), ok(X2)) -> c_16(and^#(X1, X2)) :16 -->_1 and^#(mark(X1), X2) -> c_15(and^#(X1, X2)) :15 16: and^#(ok(X1), ok(X2)) -> c_16(and^#(X1, X2)) -->_1 and^#(ok(X1), ok(X2)) -> c_16(and^#(X1, X2)) :16 -->_1 and^#(mark(X1), X2) -> c_15(and^#(X1, X2)) :15 17: if^#(mark(X1), X2, X3) -> c_17(if^#(X1, X2, X3)) -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_18(if^#(X1, X2, X3)) :18 -->_1 if^#(mark(X1), X2, X3) -> c_17(if^#(X1, X2, X3)) :17 18: if^#(ok(X1), ok(X2), ok(X3)) -> c_18(if^#(X1, X2, X3)) -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_18(if^#(X1, X2, X3)) :18 -->_1 if^#(mark(X1), X2, X3) -> c_17(if^#(X1, X2, X3)) :17 19: add^#(mark(X1), X2) -> c_19(add^#(X1, X2)) -->_1 add^#(ok(X1), ok(X2)) -> c_20(add^#(X1, X2)) :20 -->_1 add^#(mark(X1), X2) -> c_19(add^#(X1, X2)) :19 20: add^#(ok(X1), ok(X2)) -> c_20(add^#(X1, X2)) -->_1 add^#(ok(X1), ok(X2)) -> c_20(add^#(X1, X2)) :20 -->_1 add^#(mark(X1), X2) -> c_19(add^#(X1, X2)) :19 21: s^#(ok(X)) -> c_21(s^#(X)) -->_1 s^#(ok(X)) -> c_21(s^#(X)) :21 22: first^#(X1, mark(X2)) -> c_22(first^#(X1, X2)) -->_1 first^#(ok(X1), ok(X2)) -> c_24(first^#(X1, X2)) :24 -->_1 first^#(mark(X1), X2) -> c_23(first^#(X1, X2)) :23 -->_1 first^#(X1, mark(X2)) -> c_22(first^#(X1, X2)) :22 23: first^#(mark(X1), X2) -> c_23(first^#(X1, X2)) -->_1 first^#(ok(X1), ok(X2)) -> c_24(first^#(X1, X2)) :24 -->_1 first^#(mark(X1), X2) -> c_23(first^#(X1, X2)) :23 -->_1 first^#(X1, mark(X2)) -> c_22(first^#(X1, X2)) :22 24: first^#(ok(X1), ok(X2)) -> c_24(first^#(X1, X2)) -->_1 first^#(ok(X1), ok(X2)) -> c_24(first^#(X1, X2)) :24 -->_1 first^#(mark(X1), X2) -> c_23(first^#(X1, X2)) :23 -->_1 first^#(X1, mark(X2)) -> c_22(first^#(X1, X2)) :22 25: cons^#(ok(X1), ok(X2)) -> c_25(cons^#(X1, X2)) -->_1 cons^#(ok(X1), ok(X2)) -> c_25(cons^#(X1, X2)) :25 26: from^#(ok(X)) -> c_26(from^#(X)) -->_1 from^#(ok(X)) -> c_26(from^#(X)) :26 27: proper^#(and(X1, X2)) -> c_27(and^#(proper(X1), proper(X2))) -->_1 and^#(ok(X1), ok(X2)) -> c_16(and^#(X1, X2)) :16 -->_1 and^#(mark(X1), X2) -> c_15(and^#(X1, X2)) :15 28: proper^#(true()) -> c_28() 29: proper^#(false()) -> c_29() 30: proper^#(if(X1, X2, X3)) -> c_30(if^#(proper(X1), proper(X2), proper(X3))) -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_18(if^#(X1, X2, X3)) :18 -->_1 if^#(mark(X1), X2, X3) -> c_17(if^#(X1, X2, X3)) :17 31: proper^#(add(X1, X2)) -> c_31(add^#(proper(X1), proper(X2))) -->_1 add^#(ok(X1), ok(X2)) -> c_20(add^#(X1, X2)) :20 -->_1 add^#(mark(X1), X2) -> c_19(add^#(X1, X2)) :19 32: proper^#(0()) -> c_32() 33: proper^#(s(X)) -> c_33(s^#(proper(X))) -->_1 s^#(ok(X)) -> c_21(s^#(X)) :21 34: proper^#(first(X1, X2)) -> c_34(first^#(proper(X1), proper(X2))) -->_1 first^#(ok(X1), ok(X2)) -> c_24(first^#(X1, X2)) :24 -->_1 first^#(mark(X1), X2) -> c_23(first^#(X1, X2)) :23 -->_1 first^#(X1, mark(X2)) -> c_22(first^#(X1, X2)) :22 35: proper^#(nil()) -> c_35() 36: proper^#(cons(X1, X2)) -> c_36(cons^#(proper(X1), proper(X2))) -->_1 cons^#(ok(X1), ok(X2)) -> c_25(cons^#(X1, X2)) :25 37: proper^#(from(X)) -> c_37(from^#(proper(X))) -->_1 from^#(ok(X)) -> c_26(from^#(X)) :26 38: top^#(mark(X)) -> c_38(top^#(proper(X))) -->_1 top^#(ok(X)) -> c_39(top^#(active(X))) :39 -->_1 top^#(mark(X)) -> c_38(top^#(proper(X))) :38 39: top^#(ok(X)) -> c_39(top^#(active(X))) -->_1 top^#(ok(X)) -> c_39(top^#(active(X))) :39 -->_1 top^#(mark(X)) -> c_38(top^#(proper(X))) :38 Only the nodes {15,16,17,18,19,20,21,22,24,23,25,26,28,29,32,35,38,39} are reachable from nodes {15,16,17,18,19,20,21,22,23,24,25,26,28,29,32,35,38,39} that start derivation from marked basic terms. The nodes not reachable are removed from the problem. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { and^#(mark(X1), X2) -> c_15(and^#(X1, X2)) , and^#(ok(X1), ok(X2)) -> c_16(and^#(X1, X2)) , if^#(mark(X1), X2, X3) -> c_17(if^#(X1, X2, X3)) , if^#(ok(X1), ok(X2), ok(X3)) -> c_18(if^#(X1, X2, X3)) , add^#(mark(X1), X2) -> c_19(add^#(X1, X2)) , add^#(ok(X1), ok(X2)) -> c_20(add^#(X1, X2)) , s^#(ok(X)) -> c_21(s^#(X)) , first^#(X1, mark(X2)) -> c_22(first^#(X1, X2)) , first^#(mark(X1), X2) -> c_23(first^#(X1, X2)) , first^#(ok(X1), ok(X2)) -> c_24(first^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_25(cons^#(X1, X2)) , from^#(ok(X)) -> c_26(from^#(X)) , proper^#(true()) -> c_28() , proper^#(false()) -> c_29() , proper^#(0()) -> c_32() , proper^#(nil()) -> c_35() , top^#(mark(X)) -> c_38(top^#(proper(X))) , top^#(ok(X)) -> c_39(top^#(active(X))) } Strict Trs: { active(and(X1, X2)) -> and(active(X1), X2) , active(and(true(), X)) -> mark(X) , active(and(false(), Y)) -> mark(false()) , active(if(X1, X2, X3)) -> if(active(X1), X2, X3) , active(if(true(), X, Y)) -> mark(X) , active(if(false(), X, Y)) -> mark(Y) , active(add(X1, X2)) -> add(active(X1), X2) , active(add(0(), X)) -> mark(X) , active(add(s(X), Y)) -> mark(s(add(X, Y))) , active(first(X1, X2)) -> first(X1, active(X2)) , active(first(X1, X2)) -> first(active(X1), X2) , active(first(0(), X)) -> mark(nil()) , active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))) , active(from(X)) -> mark(cons(X, from(s(X)))) , and(mark(X1), X2) -> mark(and(X1, X2)) , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) , if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)) , if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)) , add(mark(X1), X2) -> mark(add(X1, X2)) , add(ok(X1), ok(X2)) -> ok(add(X1, X2)) , s(ok(X)) -> ok(s(X)) , first(X1, mark(X2)) -> mark(first(X1, X2)) , first(mark(X1), X2) -> mark(first(X1, X2)) , first(ok(X1), ok(X2)) -> ok(first(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , from(ok(X)) -> ok(from(X)) , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) , proper(true()) -> ok(true()) , proper(false()) -> ok(false()) , proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)) , proper(add(X1, X2)) -> add(proper(X1), proper(X2)) , proper(0()) -> ok(0()) , proper(s(X)) -> s(proper(X)) , proper(first(X1, X2)) -> first(proper(X1), proper(X2)) , proper(nil()) -> ok(nil()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(from(X)) -> from(proper(X)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {13,14,15,16} by applications of Pre({13,14,15,16}) = {}. Here rules are labeled as follows: DPs: { 1: and^#(mark(X1), X2) -> c_15(and^#(X1, X2)) , 2: and^#(ok(X1), ok(X2)) -> c_16(and^#(X1, X2)) , 3: if^#(mark(X1), X2, X3) -> c_17(if^#(X1, X2, X3)) , 4: if^#(ok(X1), ok(X2), ok(X3)) -> c_18(if^#(X1, X2, X3)) , 5: add^#(mark(X1), X2) -> c_19(add^#(X1, X2)) , 6: add^#(ok(X1), ok(X2)) -> c_20(add^#(X1, X2)) , 7: s^#(ok(X)) -> c_21(s^#(X)) , 8: first^#(X1, mark(X2)) -> c_22(first^#(X1, X2)) , 9: first^#(mark(X1), X2) -> c_23(first^#(X1, X2)) , 10: first^#(ok(X1), ok(X2)) -> c_24(first^#(X1, X2)) , 11: cons^#(ok(X1), ok(X2)) -> c_25(cons^#(X1, X2)) , 12: from^#(ok(X)) -> c_26(from^#(X)) , 13: proper^#(true()) -> c_28() , 14: proper^#(false()) -> c_29() , 15: proper^#(0()) -> c_32() , 16: proper^#(nil()) -> c_35() , 17: top^#(mark(X)) -> c_38(top^#(proper(X))) , 18: top^#(ok(X)) -> c_39(top^#(active(X))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { and^#(mark(X1), X2) -> c_15(and^#(X1, X2)) , and^#(ok(X1), ok(X2)) -> c_16(and^#(X1, X2)) , if^#(mark(X1), X2, X3) -> c_17(if^#(X1, X2, X3)) , if^#(ok(X1), ok(X2), ok(X3)) -> c_18(if^#(X1, X2, X3)) , add^#(mark(X1), X2) -> c_19(add^#(X1, X2)) , add^#(ok(X1), ok(X2)) -> c_20(add^#(X1, X2)) , s^#(ok(X)) -> c_21(s^#(X)) , first^#(X1, mark(X2)) -> c_22(first^#(X1, X2)) , first^#(mark(X1), X2) -> c_23(first^#(X1, X2)) , first^#(ok(X1), ok(X2)) -> c_24(first^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_25(cons^#(X1, X2)) , from^#(ok(X)) -> c_26(from^#(X)) , top^#(mark(X)) -> c_38(top^#(proper(X))) , top^#(ok(X)) -> c_39(top^#(active(X))) } Strict Trs: { active(and(X1, X2)) -> and(active(X1), X2) , active(and(true(), X)) -> mark(X) , active(and(false(), Y)) -> mark(false()) , active(if(X1, X2, X3)) -> if(active(X1), X2, X3) , active(if(true(), X, Y)) -> mark(X) , active(if(false(), X, Y)) -> mark(Y) , active(add(X1, X2)) -> add(active(X1), X2) , active(add(0(), X)) -> mark(X) , active(add(s(X), Y)) -> mark(s(add(X, Y))) , active(first(X1, X2)) -> first(X1, active(X2)) , active(first(X1, X2)) -> first(active(X1), X2) , active(first(0(), X)) -> mark(nil()) , active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))) , active(from(X)) -> mark(cons(X, from(s(X)))) , and(mark(X1), X2) -> mark(and(X1, X2)) , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) , if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)) , if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)) , add(mark(X1), X2) -> mark(add(X1, X2)) , add(ok(X1), ok(X2)) -> ok(add(X1, X2)) , s(ok(X)) -> ok(s(X)) , first(X1, mark(X2)) -> mark(first(X1, X2)) , first(mark(X1), X2) -> mark(first(X1, X2)) , first(ok(X1), ok(X2)) -> ok(first(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , from(ok(X)) -> ok(from(X)) , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) , proper(true()) -> ok(true()) , proper(false()) -> ok(false()) , proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)) , proper(add(X1, X2)) -> add(proper(X1), proper(X2)) , proper(0()) -> ok(0()) , proper(s(X)) -> s(proper(X)) , proper(first(X1, X2)) -> first(proper(X1), proper(X2)) , proper(nil()) -> ok(nil()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(from(X)) -> from(proper(X)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Weak DPs: { proper^#(true()) -> c_28() , proper^#(false()) -> c_29() , proper^#(0()) -> c_32() , proper^#(nil()) -> c_35() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..