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