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