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