MAYBE 1186.05/297.62 MAYBE 1186.05/297.62 1186.05/297.62 We are left with following problem, upon which TcT provides the 1186.05/297.62 certificate MAYBE. 1186.05/297.62 1186.05/297.62 Strict Trs: 1186.05/297.62 { g(A()) -> A() 1186.05/297.62 , g(B()) -> A() 1186.05/297.62 , g(B()) -> B() 1186.05/297.62 , g(C()) -> A() 1186.05/297.62 , g(C()) -> B() 1186.05/297.62 , g(C()) -> C() 1186.05/297.62 , foldB(t, 0()) -> t 1186.05/297.62 , foldB(t, s(n)) -> f(foldB(t, n), B()) 1186.05/297.62 , f(t, x) -> f'(t, g(x)) 1186.05/297.62 , foldC(t, 0()) -> t 1186.05/297.62 , foldC(t, s(n)) -> f(foldC(t, n), C()) 1186.05/297.62 , f'(triple(a, b, c), A()) -> f''(foldB(triple(s(a), 0(), c), b)) 1186.05/297.62 , f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()) 1186.05/297.62 , f'(triple(a, b, c), C()) -> triple(a, b, s(c)) 1186.05/297.62 , f''(triple(a, b, c)) -> foldC(triple(a, b, 0()), c) 1186.05/297.62 , fold(t, x, 0()) -> t 1186.05/297.62 , fold(t, x, s(n)) -> f(fold(t, x, n), x) } 1186.05/297.62 Obligation: 1186.05/297.62 runtime complexity 1186.05/297.62 Answer: 1186.05/297.62 MAYBE 1186.05/297.62 1186.05/297.62 None of the processors succeeded. 1186.05/297.62 1186.05/297.62 Details of failed attempt(s): 1186.05/297.62 ----------------------------- 1186.05/297.62 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1186.05/297.62 following reason: 1186.05/297.62 1186.05/297.62 Computation stopped due to timeout after 297.0 seconds. 1186.05/297.62 1186.05/297.62 2) 'Best' failed due to the following reason: 1186.05/297.62 1186.05/297.62 None of the processors succeeded. 1186.05/297.62 1186.05/297.62 Details of failed attempt(s): 1186.05/297.62 ----------------------------- 1186.05/297.62 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1186.05/297.62 seconds)' failed due to the following reason: 1186.05/297.62 1186.05/297.62 Computation stopped due to timeout after 148.0 seconds. 1186.05/297.62 1186.05/297.62 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1186.05/297.62 failed due to the following reason: 1186.05/297.62 1186.05/297.62 None of the processors succeeded. 1186.05/297.62 1186.05/297.62 Details of failed attempt(s): 1186.05/297.62 ----------------------------- 1186.05/297.62 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1186.05/297.62 failed due to the following reason: 1186.05/297.62 1186.05/297.62 match-boundness of the problem could not be verified. 1186.05/297.62 1186.05/297.62 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1186.05/297.62 failed due to the following reason: 1186.05/297.62 1186.05/297.62 match-boundness of the problem could not be verified. 1186.05/297.62 1186.05/297.62 1186.05/297.62 3) 'Best' failed due to the following reason: 1186.05/297.62 1186.05/297.62 None of the processors succeeded. 1186.05/297.62 1186.05/297.62 Details of failed attempt(s): 1186.05/297.62 ----------------------------- 1186.05/297.62 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1186.05/297.62 following reason: 1186.05/297.62 1186.05/297.62 The processor is inapplicable, reason: 1186.05/297.62 Processor only applicable for innermost runtime complexity analysis 1186.05/297.62 1186.05/297.62 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1186.05/297.62 to the following reason: 1186.05/297.62 1186.05/297.62 The processor is inapplicable, reason: 1186.05/297.62 Processor only applicable for innermost runtime complexity analysis 1186.05/297.62 1186.05/297.62 1186.05/297.62 1186.05/297.62 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1186.05/297.62 the following reason: 1186.05/297.62 1186.05/297.62 We add the following weak dependency pairs: 1186.05/297.62 1186.05/297.62 Strict DPs: 1186.05/297.62 { g^#(A()) -> c_1() 1186.05/297.62 , g^#(B()) -> c_2() 1186.05/297.62 , g^#(B()) -> c_3() 1186.05/297.62 , g^#(C()) -> c_4() 1186.05/297.62 , g^#(C()) -> c_5() 1186.05/297.62 , g^#(C()) -> c_6() 1186.05/297.62 , foldB^#(t, 0()) -> c_7(t) 1186.05/297.62 , foldB^#(t, s(n)) -> c_8(f^#(foldB(t, n), B())) 1186.05/297.62 , f^#(t, x) -> c_9(f'^#(t, g(x))) 1186.05/297.62 , f'^#(triple(a, b, c), A()) -> 1186.05/297.62 c_12(f''^#(foldB(triple(s(a), 0(), c), b))) 1186.05/297.62 , f'^#(triple(a, b, c), B()) -> c_13(f^#(triple(a, b, c), A())) 1186.05/297.62 , f'^#(triple(a, b, c), C()) -> c_14(a, b, c) 1186.05/297.62 , foldC^#(t, 0()) -> c_10(t) 1186.05/297.62 , foldC^#(t, s(n)) -> c_11(f^#(foldC(t, n), C())) 1186.05/297.62 , f''^#(triple(a, b, c)) -> c_15(foldC^#(triple(a, b, 0()), c)) 1186.05/297.62 , fold^#(t, x, 0()) -> c_16(t) 1186.05/297.62 , fold^#(t, x, s(n)) -> c_17(f^#(fold(t, x, n), x)) } 1186.05/297.62 1186.05/297.62 and mark the set of starting terms. 1186.05/297.62 1186.05/297.62 We are left with following problem, upon which TcT provides the 1186.05/297.62 certificate MAYBE. 1186.05/297.62 1186.05/297.62 Strict DPs: 1186.05/297.62 { g^#(A()) -> c_1() 1186.05/297.62 , g^#(B()) -> c_2() 1186.05/297.62 , g^#(B()) -> c_3() 1186.05/297.62 , g^#(C()) -> c_4() 1186.05/297.62 , g^#(C()) -> c_5() 1186.05/297.62 , g^#(C()) -> c_6() 1186.05/297.62 , foldB^#(t, 0()) -> c_7(t) 1186.05/297.62 , foldB^#(t, s(n)) -> c_8(f^#(foldB(t, n), B())) 1186.05/297.62 , f^#(t, x) -> c_9(f'^#(t, g(x))) 1186.05/297.62 , f'^#(triple(a, b, c), A()) -> 1186.05/297.62 c_12(f''^#(foldB(triple(s(a), 0(), c), b))) 1186.05/297.62 , f'^#(triple(a, b, c), B()) -> c_13(f^#(triple(a, b, c), A())) 1186.05/297.62 , f'^#(triple(a, b, c), C()) -> c_14(a, b, c) 1186.05/297.62 , foldC^#(t, 0()) -> c_10(t) 1186.05/297.62 , foldC^#(t, s(n)) -> c_11(f^#(foldC(t, n), C())) 1186.05/297.62 , f''^#(triple(a, b, c)) -> c_15(foldC^#(triple(a, b, 0()), c)) 1186.05/297.62 , fold^#(t, x, 0()) -> c_16(t) 1186.05/297.62 , fold^#(t, x, s(n)) -> c_17(f^#(fold(t, x, n), x)) } 1186.05/297.62 Strict Trs: 1186.05/297.62 { g(A()) -> A() 1186.05/297.62 , g(B()) -> A() 1186.05/297.62 , g(B()) -> B() 1186.05/297.62 , g(C()) -> A() 1186.05/297.62 , g(C()) -> B() 1186.05/297.62 , g(C()) -> C() 1186.05/297.62 , foldB(t, 0()) -> t 1186.05/297.62 , foldB(t, s(n)) -> f(foldB(t, n), B()) 1186.05/297.62 , f(t, x) -> f'(t, g(x)) 1186.05/297.62 , foldC(t, 0()) -> t 1186.05/297.62 , foldC(t, s(n)) -> f(foldC(t, n), C()) 1186.05/297.62 , f'(triple(a, b, c), A()) -> f''(foldB(triple(s(a), 0(), c), b)) 1186.05/297.62 , f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()) 1186.05/297.62 , f'(triple(a, b, c), C()) -> triple(a, b, s(c)) 1186.05/297.62 , f''(triple(a, b, c)) -> foldC(triple(a, b, 0()), c) 1186.05/297.62 , fold(t, x, 0()) -> t 1186.05/297.62 , fold(t, x, s(n)) -> f(fold(t, x, n), x) } 1186.05/297.62 Obligation: 1186.05/297.62 runtime complexity 1186.05/297.62 Answer: 1186.05/297.62 MAYBE 1186.05/297.62 1186.05/297.62 We estimate the number of application of {1,2,3,4,5,6} by 1186.05/297.62 applications of Pre({1,2,3,4,5,6}) = {7,12,13,16}. Here rules are 1186.05/297.62 labeled as follows: 1186.05/297.62 1186.05/297.62 DPs: 1186.05/297.62 { 1: g^#(A()) -> c_1() 1186.05/297.62 , 2: g^#(B()) -> c_2() 1186.05/297.62 , 3: g^#(B()) -> c_3() 1186.05/297.62 , 4: g^#(C()) -> c_4() 1186.05/297.62 , 5: g^#(C()) -> c_5() 1186.05/297.62 , 6: g^#(C()) -> c_6() 1186.05/297.62 , 7: foldB^#(t, 0()) -> c_7(t) 1186.05/297.62 , 8: foldB^#(t, s(n)) -> c_8(f^#(foldB(t, n), B())) 1186.05/297.62 , 9: f^#(t, x) -> c_9(f'^#(t, g(x))) 1186.05/297.62 , 10: f'^#(triple(a, b, c), A()) -> 1186.05/297.62 c_12(f''^#(foldB(triple(s(a), 0(), c), b))) 1186.05/297.62 , 11: f'^#(triple(a, b, c), B()) -> c_13(f^#(triple(a, b, c), A())) 1186.05/297.62 , 12: f'^#(triple(a, b, c), C()) -> c_14(a, b, c) 1186.05/297.62 , 13: foldC^#(t, 0()) -> c_10(t) 1186.05/297.62 , 14: foldC^#(t, s(n)) -> c_11(f^#(foldC(t, n), C())) 1186.05/297.62 , 15: f''^#(triple(a, b, c)) -> c_15(foldC^#(triple(a, b, 0()), c)) 1186.05/297.62 , 16: fold^#(t, x, 0()) -> c_16(t) 1186.05/297.62 , 17: fold^#(t, x, s(n)) -> c_17(f^#(fold(t, x, n), x)) } 1186.05/297.62 1186.05/297.62 We are left with following problem, upon which TcT provides the 1186.05/297.62 certificate MAYBE. 1186.05/297.62 1186.05/297.62 Strict DPs: 1186.05/297.62 { foldB^#(t, 0()) -> c_7(t) 1186.05/297.62 , foldB^#(t, s(n)) -> c_8(f^#(foldB(t, n), B())) 1186.05/297.62 , f^#(t, x) -> c_9(f'^#(t, g(x))) 1186.05/297.62 , f'^#(triple(a, b, c), A()) -> 1186.05/297.62 c_12(f''^#(foldB(triple(s(a), 0(), c), b))) 1186.05/297.62 , f'^#(triple(a, b, c), B()) -> c_13(f^#(triple(a, b, c), A())) 1186.05/297.62 , f'^#(triple(a, b, c), C()) -> c_14(a, b, c) 1186.05/297.62 , foldC^#(t, 0()) -> c_10(t) 1186.05/297.62 , foldC^#(t, s(n)) -> c_11(f^#(foldC(t, n), C())) 1186.05/297.62 , f''^#(triple(a, b, c)) -> c_15(foldC^#(triple(a, b, 0()), c)) 1186.05/297.62 , fold^#(t, x, 0()) -> c_16(t) 1186.05/297.62 , fold^#(t, x, s(n)) -> c_17(f^#(fold(t, x, n), x)) } 1186.05/297.62 Strict Trs: 1186.05/297.62 { g(A()) -> A() 1186.05/297.62 , g(B()) -> A() 1186.05/297.62 , g(B()) -> B() 1186.05/297.62 , g(C()) -> A() 1186.05/297.62 , g(C()) -> B() 1186.05/297.62 , g(C()) -> C() 1186.05/297.62 , foldB(t, 0()) -> t 1186.05/297.62 , foldB(t, s(n)) -> f(foldB(t, n), B()) 1186.05/297.62 , f(t, x) -> f'(t, g(x)) 1186.05/297.62 , foldC(t, 0()) -> t 1186.05/297.62 , foldC(t, s(n)) -> f(foldC(t, n), C()) 1186.05/297.62 , f'(triple(a, b, c), A()) -> f''(foldB(triple(s(a), 0(), c), b)) 1186.05/297.62 , f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()) 1186.05/297.62 , f'(triple(a, b, c), C()) -> triple(a, b, s(c)) 1186.05/297.62 , f''(triple(a, b, c)) -> foldC(triple(a, b, 0()), c) 1186.05/297.62 , fold(t, x, 0()) -> t 1186.05/297.62 , fold(t, x, s(n)) -> f(fold(t, x, n), x) } 1186.05/297.62 Weak DPs: 1186.05/297.62 { g^#(A()) -> c_1() 1186.05/297.62 , g^#(B()) -> c_2() 1186.05/297.62 , g^#(B()) -> c_3() 1186.05/297.62 , g^#(C()) -> c_4() 1186.05/297.62 , g^#(C()) -> c_5() 1186.05/297.62 , g^#(C()) -> c_6() } 1186.05/297.62 Obligation: 1186.05/297.62 runtime complexity 1186.05/297.62 Answer: 1186.05/297.62 MAYBE 1186.05/297.62 1186.05/297.62 Empty strict component of the problem is NOT empty. 1186.05/297.62 1186.05/297.62 1186.05/297.62 Arrrr.. 1187.02/298.53 EOF