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