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