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