MAYBE 1066.91/297.05 MAYBE 1066.91/297.05 1066.91/297.05 We are left with following problem, upon which TcT provides the 1066.91/297.05 certificate MAYBE. 1066.91/297.05 1066.91/297.05 Strict Trs: 1066.91/297.05 { -(x, 0()) -> x 1066.91/297.05 , -(s(x), s(y)) -> -(x, y) 1066.91/297.05 , p(s(x)) -> x 1066.91/297.05 , f(x, s(y)) -> f(p(-(x, s(y))), p(-(s(y), x))) 1066.91/297.05 , f(s(x), y) -> f(p(-(s(x), y)), p(-(y, s(x)))) } 1066.91/297.05 Obligation: 1066.91/297.05 runtime complexity 1066.91/297.05 Answer: 1066.91/297.05 MAYBE 1066.91/297.05 1066.91/297.05 None of the processors succeeded. 1066.91/297.05 1066.91/297.05 Details of failed attempt(s): 1066.91/297.05 ----------------------------- 1066.91/297.05 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1066.91/297.05 following reason: 1066.91/297.05 1066.91/297.05 Computation stopped due to timeout after 297.0 seconds. 1066.91/297.05 1066.91/297.05 2) 'Best' failed due to the following reason: 1066.91/297.05 1066.91/297.05 None of the processors succeeded. 1066.91/297.05 1066.91/297.05 Details of failed attempt(s): 1066.91/297.05 ----------------------------- 1066.91/297.05 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1066.91/297.05 seconds)' failed due to the following reason: 1066.91/297.05 1066.91/297.05 Computation stopped due to timeout after 148.0 seconds. 1066.91/297.05 1066.91/297.05 2) 'Best' failed due to the following reason: 1066.91/297.05 1066.91/297.05 None of the processors succeeded. 1066.91/297.05 1066.91/297.05 Details of failed attempt(s): 1066.91/297.05 ----------------------------- 1066.91/297.05 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1066.91/297.05 to the following reason: 1066.91/297.05 1066.91/297.05 The processor is inapplicable, reason: 1066.91/297.05 Processor only applicable for innermost runtime complexity analysis 1066.91/297.05 1066.91/297.05 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1066.91/297.05 following reason: 1066.91/297.05 1066.91/297.05 The processor is inapplicable, reason: 1066.91/297.05 Processor only applicable for innermost runtime complexity analysis 1066.91/297.05 1066.91/297.05 1066.91/297.05 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1066.91/297.05 failed due to the following reason: 1066.91/297.05 1066.91/297.05 None of the processors succeeded. 1066.91/297.05 1066.91/297.05 Details of failed attempt(s): 1066.91/297.05 ----------------------------- 1066.91/297.05 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1066.91/297.05 failed due to the following reason: 1066.91/297.05 1066.91/297.05 match-boundness of the problem could not be verified. 1066.91/297.05 1066.91/297.05 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1066.91/297.05 failed due to the following reason: 1066.91/297.05 1066.91/297.05 match-boundness of the problem could not be verified. 1066.91/297.05 1066.91/297.05 1066.91/297.05 1066.91/297.05 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1066.91/297.05 the following reason: 1066.91/297.05 1066.91/297.05 We add the following weak dependency pairs: 1066.91/297.05 1066.91/297.05 Strict DPs: 1066.91/297.05 { -^#(x, 0()) -> c_1(x) 1066.91/297.05 , -^#(s(x), s(y)) -> c_2(-^#(x, y)) 1066.91/297.05 , p^#(s(x)) -> c_3(x) 1066.91/297.05 , f^#(x, s(y)) -> c_4(f^#(p(-(x, s(y))), p(-(s(y), x)))) 1066.91/297.05 , f^#(s(x), y) -> c_5(f^#(p(-(s(x), y)), p(-(y, s(x))))) } 1066.91/297.05 1066.91/297.05 and mark the set of starting terms. 1066.91/297.05 1066.91/297.05 We are left with following problem, upon which TcT provides the 1066.91/297.05 certificate MAYBE. 1066.91/297.05 1066.91/297.05 Strict DPs: 1066.91/297.05 { -^#(x, 0()) -> c_1(x) 1066.91/297.05 , -^#(s(x), s(y)) -> c_2(-^#(x, y)) 1066.91/297.05 , p^#(s(x)) -> c_3(x) 1066.91/297.05 , f^#(x, s(y)) -> c_4(f^#(p(-(x, s(y))), p(-(s(y), x)))) 1066.91/297.05 , f^#(s(x), y) -> c_5(f^#(p(-(s(x), y)), p(-(y, s(x))))) } 1066.91/297.05 Strict Trs: 1066.91/297.05 { -(x, 0()) -> x 1066.91/297.05 , -(s(x), s(y)) -> -(x, y) 1066.91/297.05 , p(s(x)) -> x 1066.91/297.05 , f(x, s(y)) -> f(p(-(x, s(y))), p(-(s(y), x))) 1066.91/297.05 , f(s(x), y) -> f(p(-(s(x), y)), p(-(y, s(x)))) } 1066.91/297.05 Obligation: 1066.91/297.05 runtime complexity 1066.91/297.05 Answer: 1066.91/297.05 MAYBE 1066.91/297.05 1066.91/297.05 Empty strict component of the problem is NOT empty. 1066.91/297.05 1066.91/297.05 1066.91/297.05 Arrrr.. 1067.92/297.91 EOF