MAYBE 866.85/297.01 MAYBE 866.85/297.01 866.85/297.01 We are left with following problem, upon which TcT provides the 866.85/297.01 certificate MAYBE. 866.85/297.01 866.85/297.01 Strict Trs: 866.85/297.01 { plus(0(), x) -> x 866.85/297.01 , plus(s(x), y) -> s(plus(p(s(x)), y)) 866.85/297.01 , p(s(0())) -> 0() 866.85/297.01 , p(s(s(x))) -> s(p(s(x))) 866.85/297.01 , times(0(), y) -> 0() 866.85/297.01 , times(s(x), y) -> plus(y, times(p(s(x)), y)) 866.85/297.01 , exp(x, 0()) -> s(0()) 866.85/297.01 , exp(x, s(y)) -> times(x, exp(x, y)) 866.85/297.01 , tower(x, y) -> towerIter(x, y, s(0())) 866.85/297.01 , towerIter(0(), y, z) -> z 866.85/297.01 , towerIter(s(x), y, z) -> towerIter(p(s(x)), y, exp(y, z)) } 866.85/297.01 Obligation: 866.85/297.01 innermost runtime complexity 866.85/297.01 Answer: 866.85/297.01 MAYBE 866.85/297.01 866.85/297.01 None of the processors succeeded. 866.85/297.01 866.85/297.01 Details of failed attempt(s): 866.85/297.01 ----------------------------- 866.85/297.01 1) 'empty' failed due to the following reason: 866.85/297.01 866.85/297.01 Empty strict component of the problem is NOT empty. 866.85/297.01 866.85/297.01 2) 'Best' failed due to the following reason: 866.85/297.01 866.85/297.01 None of the processors succeeded. 866.85/297.01 866.85/297.01 Details of failed attempt(s): 866.85/297.01 ----------------------------- 866.85/297.01 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 866.85/297.01 following reason: 866.85/297.01 866.85/297.01 Computation stopped due to timeout after 297.0 seconds. 866.85/297.01 866.85/297.01 2) 'Best' failed due to the following reason: 866.85/297.01 866.85/297.01 None of the processors succeeded. 866.85/297.01 866.85/297.01 Details of failed attempt(s): 866.85/297.01 ----------------------------- 866.85/297.01 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 866.85/297.01 seconds)' failed due to the following reason: 866.85/297.01 866.85/297.01 Computation stopped due to timeout after 148.0 seconds. 866.85/297.01 866.85/297.01 2) 'Best' failed due to the following reason: 866.85/297.01 866.85/297.01 None of the processors succeeded. 866.85/297.01 866.85/297.01 Details of failed attempt(s): 866.85/297.01 ----------------------------- 866.85/297.01 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 866.85/297.01 following reason: 866.85/297.01 866.85/297.01 The input cannot be shown compatible 866.85/297.01 866.85/297.01 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 866.85/297.01 to the following reason: 866.85/297.01 866.85/297.01 The input cannot be shown compatible 866.85/297.01 866.85/297.01 866.85/297.01 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 866.85/297.01 failed due to the following reason: 866.85/297.01 866.85/297.01 None of the processors succeeded. 866.85/297.01 866.85/297.01 Details of failed attempt(s): 866.85/297.01 ----------------------------- 866.85/297.01 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 866.85/297.01 failed due to the following reason: 866.85/297.01 866.85/297.01 match-boundness of the problem could not be verified. 866.85/297.01 866.85/297.01 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 866.85/297.01 failed due to the following reason: 866.85/297.01 866.85/297.01 match-boundness of the problem could not be verified. 866.85/297.01 866.85/297.01 866.85/297.01 866.85/297.01 866.85/297.01 866.85/297.01 Arrrr.. 866.97/297.17 EOF