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