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