MAYBE 1185.52/297.40 MAYBE 1185.52/297.40 1185.52/297.40 We are left with following problem, upon which TcT provides the 1185.52/297.40 certificate MAYBE. 1185.52/297.40 1185.52/297.40 Strict Trs: 1185.52/297.40 { a__minus(X1, X2) -> minus(X1, X2) 1185.52/297.40 , a__minus(0(), Y) -> 0() 1185.52/297.40 , a__minus(s(X), s(Y)) -> a__minus(X, Y) 1185.52/297.40 , a__geq(X1, X2) -> geq(X1, X2) 1185.52/297.40 , a__geq(X, 0()) -> true() 1185.52/297.40 , a__geq(0(), s(Y)) -> false() 1185.52/297.40 , a__geq(s(X), s(Y)) -> a__geq(X, Y) 1185.52/297.40 , a__div(X1, X2) -> div(X1, X2) 1185.52/297.40 , a__div(0(), s(Y)) -> 0() 1185.52/297.40 , a__div(s(X), s(Y)) -> 1185.52/297.40 a__if(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()) 1185.52/297.40 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1185.52/297.40 , a__if(true(), X, Y) -> mark(X) 1185.52/297.40 , a__if(false(), X, Y) -> mark(Y) 1185.52/297.40 , mark(0()) -> 0() 1185.52/297.40 , mark(s(X)) -> s(mark(X)) 1185.52/297.40 , mark(true()) -> true() 1185.52/297.40 , mark(false()) -> false() 1185.52/297.40 , mark(div(X1, X2)) -> a__div(mark(X1), X2) 1185.52/297.40 , mark(minus(X1, X2)) -> a__minus(X1, X2) 1185.52/297.40 , mark(geq(X1, X2)) -> a__geq(X1, X2) 1185.52/297.40 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) } 1185.52/297.40 Obligation: 1185.52/297.40 runtime complexity 1185.52/297.40 Answer: 1185.52/297.40 MAYBE 1185.52/297.40 1185.52/297.40 None of the processors succeeded. 1185.52/297.40 1185.52/297.40 Details of failed attempt(s): 1185.52/297.40 ----------------------------- 1185.52/297.40 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1185.52/297.40 following reason: 1185.52/297.40 1185.52/297.40 Computation stopped due to timeout after 297.0 seconds. 1185.52/297.40 1185.52/297.40 2) 'Best' failed due to the following reason: 1185.52/297.40 1185.52/297.40 None of the processors succeeded. 1185.52/297.40 1185.52/297.40 Details of failed attempt(s): 1185.52/297.40 ----------------------------- 1185.52/297.40 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1185.52/297.40 seconds)' failed due to the following reason: 1185.52/297.40 1185.52/297.40 Computation stopped due to timeout after 148.0 seconds. 1185.52/297.40 1185.52/297.40 2) 'Best' failed due to the following reason: 1185.52/297.40 1185.52/297.40 None of the processors succeeded. 1185.52/297.40 1185.52/297.40 Details of failed attempt(s): 1185.52/297.40 ----------------------------- 1185.52/297.40 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1185.52/297.40 following reason: 1185.52/297.40 1185.52/297.40 The processor is inapplicable, reason: 1185.52/297.40 Processor only applicable for innermost runtime complexity analysis 1185.52/297.40 1185.52/297.40 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1185.52/297.40 to the following reason: 1185.52/297.40 1185.52/297.40 The processor is inapplicable, reason: 1185.52/297.40 Processor only applicable for innermost runtime complexity analysis 1185.52/297.40 1185.52/297.40 1185.52/297.40 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1185.52/297.40 failed due to the following reason: 1185.52/297.40 1185.52/297.40 None of the processors succeeded. 1185.52/297.40 1185.52/297.40 Details of failed attempt(s): 1185.52/297.40 ----------------------------- 1185.52/297.40 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1185.52/297.40 failed due to the following reason: 1185.52/297.40 1185.52/297.40 match-boundness of the problem could not be verified. 1185.52/297.40 1185.52/297.40 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1185.52/297.40 failed due to the following reason: 1185.52/297.40 1185.52/297.40 match-boundness of the problem could not be verified. 1185.52/297.40 1185.52/297.40 1185.52/297.40 1185.52/297.40 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1185.52/297.40 the following reason: 1185.52/297.40 1185.52/297.40 We add the following weak dependency pairs: 1185.52/297.40 1185.52/297.40 Strict DPs: 1185.52/297.40 { a__minus^#(X1, X2) -> c_1(X1, X2) 1185.52/297.40 , a__minus^#(0(), Y) -> c_2() 1185.52/297.40 , a__minus^#(s(X), s(Y)) -> c_3(a__minus^#(X, Y)) 1185.52/297.40 , a__geq^#(X1, X2) -> c_4(X1, X2) 1185.52/297.40 , a__geq^#(X, 0()) -> c_5() 1185.52/297.40 , a__geq^#(0(), s(Y)) -> c_6() 1185.52/297.40 , a__geq^#(s(X), s(Y)) -> c_7(a__geq^#(X, Y)) 1185.52/297.40 , a__div^#(X1, X2) -> c_8(X1, X2) 1185.52/297.40 , a__div^#(0(), s(Y)) -> c_9() 1185.52/297.40 , a__div^#(s(X), s(Y)) -> 1185.52/297.40 c_10(a__if^#(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) 1185.52/297.40 , a__if^#(X1, X2, X3) -> c_11(X1, X2, X3) 1185.52/297.40 , a__if^#(true(), X, Y) -> c_12(mark^#(X)) 1185.52/297.40 , a__if^#(false(), X, Y) -> c_13(mark^#(Y)) 1185.52/297.40 , mark^#(0()) -> c_14() 1185.52/297.40 , mark^#(s(X)) -> c_15(mark^#(X)) 1185.52/297.40 , mark^#(true()) -> c_16() 1185.52/297.40 , mark^#(false()) -> c_17() 1185.52/297.40 , mark^#(div(X1, X2)) -> c_18(a__div^#(mark(X1), X2)) 1185.52/297.40 , mark^#(minus(X1, X2)) -> c_19(a__minus^#(X1, X2)) 1185.52/297.40 , mark^#(geq(X1, X2)) -> c_20(a__geq^#(X1, X2)) 1185.52/297.40 , mark^#(if(X1, X2, X3)) -> c_21(a__if^#(mark(X1), X2, X3)) } 1185.52/297.40 1185.52/297.40 and mark the set of starting terms. 1185.52/297.40 1185.52/297.40 We are left with following problem, upon which TcT provides the 1185.52/297.40 certificate MAYBE. 1185.52/297.40 1185.52/297.40 Strict DPs: 1185.52/297.40 { a__minus^#(X1, X2) -> c_1(X1, X2) 1185.52/297.40 , a__minus^#(0(), Y) -> c_2() 1185.52/297.40 , a__minus^#(s(X), s(Y)) -> c_3(a__minus^#(X, Y)) 1185.52/297.40 , a__geq^#(X1, X2) -> c_4(X1, X2) 1185.52/297.40 , a__geq^#(X, 0()) -> c_5() 1185.52/297.40 , a__geq^#(0(), s(Y)) -> c_6() 1185.52/297.40 , a__geq^#(s(X), s(Y)) -> c_7(a__geq^#(X, Y)) 1185.52/297.40 , a__div^#(X1, X2) -> c_8(X1, X2) 1185.52/297.40 , a__div^#(0(), s(Y)) -> c_9() 1185.52/297.40 , a__div^#(s(X), s(Y)) -> 1185.52/297.40 c_10(a__if^#(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) 1185.52/297.40 , a__if^#(X1, X2, X3) -> c_11(X1, X2, X3) 1185.52/297.40 , a__if^#(true(), X, Y) -> c_12(mark^#(X)) 1185.52/297.40 , a__if^#(false(), X, Y) -> c_13(mark^#(Y)) 1185.52/297.40 , mark^#(0()) -> c_14() 1185.52/297.40 , mark^#(s(X)) -> c_15(mark^#(X)) 1185.52/297.40 , mark^#(true()) -> c_16() 1185.52/297.40 , mark^#(false()) -> c_17() 1185.52/297.40 , mark^#(div(X1, X2)) -> c_18(a__div^#(mark(X1), X2)) 1185.52/297.40 , mark^#(minus(X1, X2)) -> c_19(a__minus^#(X1, X2)) 1185.52/297.40 , mark^#(geq(X1, X2)) -> c_20(a__geq^#(X1, X2)) 1185.52/297.40 , mark^#(if(X1, X2, X3)) -> c_21(a__if^#(mark(X1), X2, X3)) } 1185.52/297.40 Strict Trs: 1185.52/297.40 { a__minus(X1, X2) -> minus(X1, X2) 1185.52/297.40 , a__minus(0(), Y) -> 0() 1185.52/297.40 , a__minus(s(X), s(Y)) -> a__minus(X, Y) 1185.52/297.40 , a__geq(X1, X2) -> geq(X1, X2) 1185.52/297.40 , a__geq(X, 0()) -> true() 1185.52/297.40 , a__geq(0(), s(Y)) -> false() 1185.52/297.40 , a__geq(s(X), s(Y)) -> a__geq(X, Y) 1185.52/297.40 , a__div(X1, X2) -> div(X1, X2) 1185.52/297.40 , a__div(0(), s(Y)) -> 0() 1185.52/297.40 , a__div(s(X), s(Y)) -> 1185.52/297.40 a__if(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()) 1185.52/297.40 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1185.52/297.40 , a__if(true(), X, Y) -> mark(X) 1185.52/297.40 , a__if(false(), X, Y) -> mark(Y) 1185.52/297.40 , mark(0()) -> 0() 1185.52/297.40 , mark(s(X)) -> s(mark(X)) 1185.52/297.40 , mark(true()) -> true() 1185.52/297.40 , mark(false()) -> false() 1185.52/297.40 , mark(div(X1, X2)) -> a__div(mark(X1), X2) 1185.52/297.40 , mark(minus(X1, X2)) -> a__minus(X1, X2) 1185.52/297.40 , mark(geq(X1, X2)) -> a__geq(X1, X2) 1185.52/297.40 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) } 1185.52/297.40 Obligation: 1185.52/297.40 runtime complexity 1185.52/297.40 Answer: 1185.52/297.40 MAYBE 1185.52/297.40 1185.52/297.40 We estimate the number of application of {2,5,6,9,14,16,17} by 1185.52/297.40 applications of Pre({2,5,6,9,14,16,17}) = 1185.52/297.40 {1,3,4,7,8,11,12,13,15,18,19,20}. Here rules are labeled as 1185.52/297.40 follows: 1185.52/297.40 1185.52/297.40 DPs: 1185.52/297.40 { 1: a__minus^#(X1, X2) -> c_1(X1, X2) 1185.52/297.40 , 2: a__minus^#(0(), Y) -> c_2() 1185.52/297.40 , 3: a__minus^#(s(X), s(Y)) -> c_3(a__minus^#(X, Y)) 1185.52/297.40 , 4: a__geq^#(X1, X2) -> c_4(X1, X2) 1185.52/297.40 , 5: a__geq^#(X, 0()) -> c_5() 1185.52/297.40 , 6: a__geq^#(0(), s(Y)) -> c_6() 1185.52/297.40 , 7: a__geq^#(s(X), s(Y)) -> c_7(a__geq^#(X, Y)) 1185.52/297.40 , 8: a__div^#(X1, X2) -> c_8(X1, X2) 1185.52/297.40 , 9: a__div^#(0(), s(Y)) -> c_9() 1185.52/297.40 , 10: a__div^#(s(X), s(Y)) -> 1185.52/297.40 c_10(a__if^#(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) 1185.52/297.40 , 11: a__if^#(X1, X2, X3) -> c_11(X1, X2, X3) 1185.52/297.40 , 12: a__if^#(true(), X, Y) -> c_12(mark^#(X)) 1185.52/297.40 , 13: a__if^#(false(), X, Y) -> c_13(mark^#(Y)) 1185.52/297.40 , 14: mark^#(0()) -> c_14() 1185.52/297.40 , 15: mark^#(s(X)) -> c_15(mark^#(X)) 1185.52/297.40 , 16: mark^#(true()) -> c_16() 1185.52/297.40 , 17: mark^#(false()) -> c_17() 1185.52/297.40 , 18: mark^#(div(X1, X2)) -> c_18(a__div^#(mark(X1), X2)) 1185.52/297.40 , 19: mark^#(minus(X1, X2)) -> c_19(a__minus^#(X1, X2)) 1185.52/297.40 , 20: mark^#(geq(X1, X2)) -> c_20(a__geq^#(X1, X2)) 1185.52/297.40 , 21: mark^#(if(X1, X2, X3)) -> c_21(a__if^#(mark(X1), X2, X3)) } 1185.52/297.40 1185.52/297.40 We are left with following problem, upon which TcT provides the 1185.52/297.40 certificate MAYBE. 1185.52/297.40 1185.52/297.40 Strict DPs: 1185.52/297.40 { a__minus^#(X1, X2) -> c_1(X1, X2) 1185.52/297.40 , a__minus^#(s(X), s(Y)) -> c_3(a__minus^#(X, Y)) 1185.52/297.40 , a__geq^#(X1, X2) -> c_4(X1, X2) 1185.52/297.40 , a__geq^#(s(X), s(Y)) -> c_7(a__geq^#(X, Y)) 1185.52/297.40 , a__div^#(X1, X2) -> c_8(X1, X2) 1185.52/297.40 , a__div^#(s(X), s(Y)) -> 1185.52/297.40 c_10(a__if^#(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) 1185.52/297.40 , a__if^#(X1, X2, X3) -> c_11(X1, X2, X3) 1185.52/297.40 , a__if^#(true(), X, Y) -> c_12(mark^#(X)) 1185.52/297.40 , a__if^#(false(), X, Y) -> c_13(mark^#(Y)) 1185.52/297.40 , mark^#(s(X)) -> c_15(mark^#(X)) 1185.52/297.40 , mark^#(div(X1, X2)) -> c_18(a__div^#(mark(X1), X2)) 1185.52/297.40 , mark^#(minus(X1, X2)) -> c_19(a__minus^#(X1, X2)) 1185.52/297.40 , mark^#(geq(X1, X2)) -> c_20(a__geq^#(X1, X2)) 1185.52/297.41 , mark^#(if(X1, X2, X3)) -> c_21(a__if^#(mark(X1), X2, X3)) } 1185.52/297.41 Strict Trs: 1185.52/297.41 { a__minus(X1, X2) -> minus(X1, X2) 1185.52/297.41 , a__minus(0(), Y) -> 0() 1185.52/297.41 , a__minus(s(X), s(Y)) -> a__minus(X, Y) 1185.52/297.41 , a__geq(X1, X2) -> geq(X1, X2) 1185.52/297.41 , a__geq(X, 0()) -> true() 1185.52/297.41 , a__geq(0(), s(Y)) -> false() 1185.52/297.41 , a__geq(s(X), s(Y)) -> a__geq(X, Y) 1185.52/297.41 , a__div(X1, X2) -> div(X1, X2) 1185.52/297.41 , a__div(0(), s(Y)) -> 0() 1185.52/297.41 , a__div(s(X), s(Y)) -> 1185.52/297.41 a__if(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()) 1185.52/297.41 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1185.52/297.41 , a__if(true(), X, Y) -> mark(X) 1185.52/297.41 , a__if(false(), X, Y) -> mark(Y) 1185.52/297.41 , mark(0()) -> 0() 1185.52/297.41 , mark(s(X)) -> s(mark(X)) 1185.52/297.41 , mark(true()) -> true() 1185.52/297.41 , mark(false()) -> false() 1185.52/297.41 , mark(div(X1, X2)) -> a__div(mark(X1), X2) 1185.52/297.41 , mark(minus(X1, X2)) -> a__minus(X1, X2) 1185.52/297.41 , mark(geq(X1, X2)) -> a__geq(X1, X2) 1185.52/297.41 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) } 1185.52/297.41 Weak DPs: 1185.52/297.41 { a__minus^#(0(), Y) -> c_2() 1185.52/297.41 , a__geq^#(X, 0()) -> c_5() 1185.52/297.41 , a__geq^#(0(), s(Y)) -> c_6() 1185.52/297.41 , a__div^#(0(), s(Y)) -> c_9() 1185.52/297.41 , mark^#(0()) -> c_14() 1185.52/297.41 , mark^#(true()) -> c_16() 1185.52/297.41 , mark^#(false()) -> c_17() } 1185.52/297.41 Obligation: 1185.52/297.41 runtime complexity 1185.52/297.41 Answer: 1185.52/297.41 MAYBE 1185.52/297.41 1185.52/297.41 Empty strict component of the problem is NOT empty. 1185.52/297.41 1185.52/297.41 1185.52/297.41 Arrrr.. 1186.36/298.23 EOF