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