MAYBE 1064.16/297.03 MAYBE 1064.16/297.03 1064.16/297.03 We are left with following problem, upon which TcT provides the 1064.16/297.03 certificate MAYBE. 1064.16/297.03 1064.16/297.03 Strict Trs: 1064.16/297.03 { g(A()) -> A() 1064.16/297.03 , g(B()) -> A() 1064.16/297.03 , g(B()) -> B() 1064.16/297.03 , g(C()) -> A() 1064.16/297.03 , g(C()) -> B() 1064.16/297.03 , g(C()) -> C() 1064.16/297.03 , foldB(t, 0()) -> t 1064.16/297.03 , foldB(t, s(n)) -> f(foldB(t, n), B()) 1064.16/297.03 , f(t, x) -> f'(t, g(x)) 1064.16/297.03 , foldC(t, 0()) -> t 1064.16/297.03 , foldC(t, s(n)) -> f(foldC(t, n), C()) 1064.16/297.03 , f'(triple(a, b, c), A()) -> f''(foldB(triple(s(a), 0(), c), b)) 1064.16/297.03 , f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()) 1064.16/297.03 , f'(triple(a, b, c), C()) -> triple(a, b, s(c)) 1064.16/297.03 , f''(triple(a, b, c)) -> foldC(triple(a, b, 0()), c) 1064.16/297.03 , fold(t, x, 0()) -> t 1064.16/297.03 , fold(t, x, s(n)) -> f(fold(t, x, n), x) } 1064.16/297.03 Obligation: 1064.16/297.03 innermost runtime complexity 1064.16/297.03 Answer: 1064.16/297.03 MAYBE 1064.16/297.03 1064.16/297.03 None of the processors succeeded. 1064.16/297.03 1064.16/297.03 Details of failed attempt(s): 1064.16/297.03 ----------------------------- 1064.16/297.03 1) 'empty' failed due to the following reason: 1064.16/297.03 1064.16/297.03 Empty strict component of the problem is NOT empty. 1064.16/297.03 1064.16/297.03 2) 'Best' failed due to the following reason: 1064.16/297.03 1064.16/297.03 None of the processors succeeded. 1064.16/297.03 1064.16/297.03 Details of failed attempt(s): 1064.16/297.03 ----------------------------- 1064.16/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1064.16/297.03 following reason: 1064.16/297.03 1064.16/297.03 Computation stopped due to timeout after 297.0 seconds. 1064.16/297.03 1064.16/297.03 2) 'Best' failed due to the following reason: 1064.16/297.03 1064.16/297.03 None of the processors succeeded. 1064.16/297.03 1064.16/297.03 Details of failed attempt(s): 1064.16/297.03 ----------------------------- 1064.16/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1064.16/297.03 seconds)' failed due to the following reason: 1064.16/297.03 1064.16/297.03 Computation stopped due to timeout after 148.0 seconds. 1064.16/297.03 1064.16/297.03 2) 'Best' failed due to the following reason: 1064.16/297.03 1064.16/297.03 None of the processors succeeded. 1064.16/297.03 1064.16/297.03 Details of failed attempt(s): 1064.16/297.03 ----------------------------- 1064.16/297.03 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1064.16/297.03 following reason: 1064.16/297.03 1064.16/297.03 The input cannot be shown compatible 1064.16/297.03 1064.16/297.03 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1064.16/297.03 to the following reason: 1064.16/297.03 1064.16/297.03 The input cannot be shown compatible 1064.16/297.03 1064.16/297.03 1064.16/297.03 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1064.16/297.03 failed due to the following reason: 1064.16/297.03 1064.16/297.03 None of the processors succeeded. 1064.16/297.03 1064.16/297.03 Details of failed attempt(s): 1064.16/297.03 ----------------------------- 1064.16/297.03 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1064.16/297.03 failed due to the following reason: 1064.16/297.03 1064.16/297.03 match-boundness of the problem could not be verified. 1064.16/297.03 1064.16/297.03 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1064.16/297.03 failed due to the following reason: 1064.16/297.03 1064.16/297.03 match-boundness of the problem could not be verified. 1064.16/297.03 1064.16/297.03 1064.16/297.03 1064.16/297.03 1064.16/297.03 1064.16/297.03 Arrrr.. 1064.50/297.35 EOF