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