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