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