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