MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { f1(x, a()) -> g2(x, x) , f1(a(), x) -> g1(x, x) , g1(x, a()) -> h2(x) , g1(a(), x) -> h1(x) , g2(x, a()) -> h2(x) , g2(a(), x) -> h1(x) , f2(x, a()) -> g2(x, x) , f2(a(), x) -> g1(x, x) , h1(a()) -> i() , h2(a()) -> i() , e1(x1, x1, x, y, z, a()) -> e5(x1, x, y, z) , e1(h1(w), h2(w), x, y, z, w) -> e2(x, x, y, z, z, w) , e2(x, x, y, z, z, a()) -> e6(x, y, z) , e2(f1(w, w), x, y, z, f2(w, w), w) -> e3(x, y, x, y, y, z, y, z, x, y, z, w) , e2(i(), x, y, z, i(), a()) -> e6(x, y, z) , e5(i(), x, y, z) -> e6(x, y, z) , e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) , e3(x, y, x, y, y, z, y, z, x, y, z, a()) -> e6(x, y, z) , e4(x, x, x, x, x, x, x, x, x, x, x, a()) -> e6(x, x, x) , e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) -> e1(x1, x1, x, y, z, w) , e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> e5(x1, x, y, z) } 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) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) '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 2) '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 3) '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) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { f1^#(x, a()) -> c_1(g2^#(x, x)) , f1^#(a(), x) -> c_2(g1^#(x, x)) , g2^#(x, a()) -> c_5(h2^#(x)) , g2^#(a(), x) -> c_6(h1^#(x)) , g1^#(x, a()) -> c_3(h2^#(x)) , g1^#(a(), x) -> c_4(h1^#(x)) , h2^#(a()) -> c_10() , h1^#(a()) -> c_9() , f2^#(x, a()) -> c_7(g2^#(x, x)) , f2^#(a(), x) -> c_8(g1^#(x, x)) , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) , e1^#(h1(w), h2(w), x, y, z, w) -> c_12(e2^#(x, x, y, z, z, w)) , e5^#(i(), x, y, z) -> c_16(x, y, z) , e2^#(x, x, y, z, z, a()) -> c_13(x, y, z) , e2^#(f1(w, w), x, y, z, f2(w, w), w) -> c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w)) , e2^#(i(), x, y, z, i(), a()) -> c_15(x, y, z) , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18(x, y, z) , e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19(x, x, x) , e4^#(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) -> c_20(e1^#(x1, x1, x, y, z, w)) , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> c_21(e5^#(x1, x, y, z)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { f1^#(x, a()) -> c_1(g2^#(x, x)) , f1^#(a(), x) -> c_2(g1^#(x, x)) , g2^#(x, a()) -> c_5(h2^#(x)) , g2^#(a(), x) -> c_6(h1^#(x)) , g1^#(x, a()) -> c_3(h2^#(x)) , g1^#(a(), x) -> c_4(h1^#(x)) , h2^#(a()) -> c_10() , h1^#(a()) -> c_9() , f2^#(x, a()) -> c_7(g2^#(x, x)) , f2^#(a(), x) -> c_8(g1^#(x, x)) , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) , e1^#(h1(w), h2(w), x, y, z, w) -> c_12(e2^#(x, x, y, z, z, w)) , e5^#(i(), x, y, z) -> c_16(x, y, z) , e2^#(x, x, y, z, z, a()) -> c_13(x, y, z) , e2^#(f1(w, w), x, y, z, f2(w, w), w) -> c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w)) , e2^#(i(), x, y, z, i(), a()) -> c_15(x, y, z) , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18(x, y, z) , e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19(x, x, x) , e4^#(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) -> c_20(e1^#(x1, x1, x, y, z, w)) , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> c_21(e5^#(x1, x, y, z)) } Strict Trs: { f1(x, a()) -> g2(x, x) , f1(a(), x) -> g1(x, x) , g1(x, a()) -> h2(x) , g1(a(), x) -> h1(x) , g2(x, a()) -> h2(x) , g2(a(), x) -> h1(x) , f2(x, a()) -> g2(x, x) , f2(a(), x) -> g1(x, x) , h1(a()) -> i() , h2(a()) -> i() , e1(x1, x1, x, y, z, a()) -> e5(x1, x, y, z) , e1(h1(w), h2(w), x, y, z, w) -> e2(x, x, y, z, z, w) , e2(x, x, y, z, z, a()) -> e6(x, y, z) , e2(f1(w, w), x, y, z, f2(w, w), w) -> e3(x, y, x, y, y, z, y, z, x, y, z, w) , e2(i(), x, y, z, i(), a()) -> e6(x, y, z) , e5(i(), x, y, z) -> e6(x, y, z) , e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) , e3(x, y, x, y, y, z, y, z, x, y, z, a()) -> e6(x, y, z) , e4(x, x, x, x, x, x, x, x, x, x, x, a()) -> e6(x, x, x) , e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) -> e1(x1, x1, x, y, z, w) , e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> e5(x1, x, y, z) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {7,8} by applications of Pre({7,8}) = {3,4,5,6,13,14,16,18,19}. Here rules are labeled as follows: DPs: { 1: f1^#(x, a()) -> c_1(g2^#(x, x)) , 2: f1^#(a(), x) -> c_2(g1^#(x, x)) , 3: g2^#(x, a()) -> c_5(h2^#(x)) , 4: g2^#(a(), x) -> c_6(h1^#(x)) , 5: g1^#(x, a()) -> c_3(h2^#(x)) , 6: g1^#(a(), x) -> c_4(h1^#(x)) , 7: h2^#(a()) -> c_10() , 8: h1^#(a()) -> c_9() , 9: f2^#(x, a()) -> c_7(g2^#(x, x)) , 10: f2^#(a(), x) -> c_8(g1^#(x, x)) , 11: e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) , 12: e1^#(h1(w), h2(w), x, y, z, w) -> c_12(e2^#(x, x, y, z, z, w)) , 13: e5^#(i(), x, y, z) -> c_16(x, y, z) , 14: e2^#(x, x, y, z, z, a()) -> c_13(x, y, z) , 15: e2^#(f1(w, w), x, y, z, f2(w, w), w) -> c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w)) , 16: e2^#(i(), x, y, z, i(), a()) -> c_15(x, y, z) , 17: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) , 18: e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18(x, y, z) , 19: e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19(x, x, x) , 20: e4^#(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) -> c_20(e1^#(x1, x1, x, y, z, w)) , 21: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> c_21(e5^#(x1, x, y, z)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { f1^#(x, a()) -> c_1(g2^#(x, x)) , f1^#(a(), x) -> c_2(g1^#(x, x)) , g2^#(x, a()) -> c_5(h2^#(x)) , g2^#(a(), x) -> c_6(h1^#(x)) , g1^#(x, a()) -> c_3(h2^#(x)) , g1^#(a(), x) -> c_4(h1^#(x)) , f2^#(x, a()) -> c_7(g2^#(x, x)) , f2^#(a(), x) -> c_8(g1^#(x, x)) , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) , e1^#(h1(w), h2(w), x, y, z, w) -> c_12(e2^#(x, x, y, z, z, w)) , e5^#(i(), x, y, z) -> c_16(x, y, z) , e2^#(x, x, y, z, z, a()) -> c_13(x, y, z) , e2^#(f1(w, w), x, y, z, f2(w, w), w) -> c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w)) , e2^#(i(), x, y, z, i(), a()) -> c_15(x, y, z) , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18(x, y, z) , e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19(x, x, x) , e4^#(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) -> c_20(e1^#(x1, x1, x, y, z, w)) , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> c_21(e5^#(x1, x, y, z)) } Strict Trs: { f1(x, a()) -> g2(x, x) , f1(a(), x) -> g1(x, x) , g1(x, a()) -> h2(x) , g1(a(), x) -> h1(x) , g2(x, a()) -> h2(x) , g2(a(), x) -> h1(x) , f2(x, a()) -> g2(x, x) , f2(a(), x) -> g1(x, x) , h1(a()) -> i() , h2(a()) -> i() , e1(x1, x1, x, y, z, a()) -> e5(x1, x, y, z) , e1(h1(w), h2(w), x, y, z, w) -> e2(x, x, y, z, z, w) , e2(x, x, y, z, z, a()) -> e6(x, y, z) , e2(f1(w, w), x, y, z, f2(w, w), w) -> e3(x, y, x, y, y, z, y, z, x, y, z, w) , e2(i(), x, y, z, i(), a()) -> e6(x, y, z) , e5(i(), x, y, z) -> e6(x, y, z) , e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) , e3(x, y, x, y, y, z, y, z, x, y, z, a()) -> e6(x, y, z) , e4(x, x, x, x, x, x, x, x, x, x, x, a()) -> e6(x, x, x) , e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) -> e1(x1, x1, x, y, z, w) , e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> e5(x1, x, y, z) } Weak DPs: { h2^#(a()) -> c_10() , h1^#(a()) -> c_9() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {3,4,5,6} by applications of Pre({3,4,5,6}) = {1,2,7,8,11,12,14,16,17}. Here rules are labeled as follows: DPs: { 1: f1^#(x, a()) -> c_1(g2^#(x, x)) , 2: f1^#(a(), x) -> c_2(g1^#(x, x)) , 3: g2^#(x, a()) -> c_5(h2^#(x)) , 4: g2^#(a(), x) -> c_6(h1^#(x)) , 5: g1^#(x, a()) -> c_3(h2^#(x)) , 6: g1^#(a(), x) -> c_4(h1^#(x)) , 7: f2^#(x, a()) -> c_7(g2^#(x, x)) , 8: f2^#(a(), x) -> c_8(g1^#(x, x)) , 9: e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) , 10: e1^#(h1(w), h2(w), x, y, z, w) -> c_12(e2^#(x, x, y, z, z, w)) , 11: e5^#(i(), x, y, z) -> c_16(x, y, z) , 12: e2^#(x, x, y, z, z, a()) -> c_13(x, y, z) , 13: e2^#(f1(w, w), x, y, z, f2(w, w), w) -> c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w)) , 14: e2^#(i(), x, y, z, i(), a()) -> c_15(x, y, z) , 15: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) , 16: e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18(x, y, z) , 17: e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19(x, x, x) , 18: e4^#(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) -> c_20(e1^#(x1, x1, x, y, z, w)) , 19: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> c_21(e5^#(x1, x, y, z)) , 20: h2^#(a()) -> c_10() , 21: h1^#(a()) -> c_9() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { f1^#(x, a()) -> c_1(g2^#(x, x)) , f1^#(a(), x) -> c_2(g1^#(x, x)) , f2^#(x, a()) -> c_7(g2^#(x, x)) , f2^#(a(), x) -> c_8(g1^#(x, x)) , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) , e1^#(h1(w), h2(w), x, y, z, w) -> c_12(e2^#(x, x, y, z, z, w)) , e5^#(i(), x, y, z) -> c_16(x, y, z) , e2^#(x, x, y, z, z, a()) -> c_13(x, y, z) , e2^#(f1(w, w), x, y, z, f2(w, w), w) -> c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w)) , e2^#(i(), x, y, z, i(), a()) -> c_15(x, y, z) , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18(x, y, z) , e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19(x, x, x) , e4^#(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) -> c_20(e1^#(x1, x1, x, y, z, w)) , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> c_21(e5^#(x1, x, y, z)) } Strict Trs: { f1(x, a()) -> g2(x, x) , f1(a(), x) -> g1(x, x) , g1(x, a()) -> h2(x) , g1(a(), x) -> h1(x) , g2(x, a()) -> h2(x) , g2(a(), x) -> h1(x) , f2(x, a()) -> g2(x, x) , f2(a(), x) -> g1(x, x) , h1(a()) -> i() , h2(a()) -> i() , e1(x1, x1, x, y, z, a()) -> e5(x1, x, y, z) , e1(h1(w), h2(w), x, y, z, w) -> e2(x, x, y, z, z, w) , e2(x, x, y, z, z, a()) -> e6(x, y, z) , e2(f1(w, w), x, y, z, f2(w, w), w) -> e3(x, y, x, y, y, z, y, z, x, y, z, w) , e2(i(), x, y, z, i(), a()) -> e6(x, y, z) , e5(i(), x, y, z) -> e6(x, y, z) , e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) , e3(x, y, x, y, y, z, y, z, x, y, z, a()) -> e6(x, y, z) , e4(x, x, x, x, x, x, x, x, x, x, x, a()) -> e6(x, x, x) , e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) -> e1(x1, x1, x, y, z, w) , e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> e5(x1, x, y, z) } Weak DPs: { g2^#(x, a()) -> c_5(h2^#(x)) , g2^#(a(), x) -> c_6(h1^#(x)) , g1^#(x, a()) -> c_3(h2^#(x)) , g1^#(a(), x) -> c_4(h1^#(x)) , h2^#(a()) -> c_10() , h1^#(a()) -> c_9() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,4} by applications of Pre({1,2,3,4}) = {7,8,10,12,13}. Here rules are labeled as follows: DPs: { 1: f1^#(x, a()) -> c_1(g2^#(x, x)) , 2: f1^#(a(), x) -> c_2(g1^#(x, x)) , 3: f2^#(x, a()) -> c_7(g2^#(x, x)) , 4: f2^#(a(), x) -> c_8(g1^#(x, x)) , 5: e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) , 6: e1^#(h1(w), h2(w), x, y, z, w) -> c_12(e2^#(x, x, y, z, z, w)) , 7: e5^#(i(), x, y, z) -> c_16(x, y, z) , 8: e2^#(x, x, y, z, z, a()) -> c_13(x, y, z) , 9: e2^#(f1(w, w), x, y, z, f2(w, w), w) -> c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w)) , 10: e2^#(i(), x, y, z, i(), a()) -> c_15(x, y, z) , 11: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) , 12: e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18(x, y, z) , 13: e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19(x, x, x) , 14: e4^#(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) -> c_20(e1^#(x1, x1, x, y, z, w)) , 15: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> c_21(e5^#(x1, x, y, z)) , 16: g2^#(x, a()) -> c_5(h2^#(x)) , 17: g2^#(a(), x) -> c_6(h1^#(x)) , 18: g1^#(x, a()) -> c_3(h2^#(x)) , 19: g1^#(a(), x) -> c_4(h1^#(x)) , 20: h2^#(a()) -> c_10() , 21: h1^#(a()) -> c_9() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) , e1^#(h1(w), h2(w), x, y, z, w) -> c_12(e2^#(x, x, y, z, z, w)) , e5^#(i(), x, y, z) -> c_16(x, y, z) , e2^#(x, x, y, z, z, a()) -> c_13(x, y, z) , e2^#(f1(w, w), x, y, z, f2(w, w), w) -> c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w)) , e2^#(i(), x, y, z, i(), a()) -> c_15(x, y, z) , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18(x, y, z) , e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19(x, x, x) , e4^#(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) -> c_20(e1^#(x1, x1, x, y, z, w)) , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> c_21(e5^#(x1, x, y, z)) } Strict Trs: { f1(x, a()) -> g2(x, x) , f1(a(), x) -> g1(x, x) , g1(x, a()) -> h2(x) , g1(a(), x) -> h1(x) , g2(x, a()) -> h2(x) , g2(a(), x) -> h1(x) , f2(x, a()) -> g2(x, x) , f2(a(), x) -> g1(x, x) , h1(a()) -> i() , h2(a()) -> i() , e1(x1, x1, x, y, z, a()) -> e5(x1, x, y, z) , e1(h1(w), h2(w), x, y, z, w) -> e2(x, x, y, z, z, w) , e2(x, x, y, z, z, a()) -> e6(x, y, z) , e2(f1(w, w), x, y, z, f2(w, w), w) -> e3(x, y, x, y, y, z, y, z, x, y, z, w) , e2(i(), x, y, z, i(), a()) -> e6(x, y, z) , e5(i(), x, y, z) -> e6(x, y, z) , e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) , e3(x, y, x, y, y, z, y, z, x, y, z, a()) -> e6(x, y, z) , e4(x, x, x, x, x, x, x, x, x, x, x, a()) -> e6(x, x, x) , e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) -> e1(x1, x1, x, y, z, w) , e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> e5(x1, x, y, z) } Weak DPs: { f1^#(x, a()) -> c_1(g2^#(x, x)) , f1^#(a(), x) -> c_2(g1^#(x, x)) , g2^#(x, a()) -> c_5(h2^#(x)) , g2^#(a(), x) -> c_6(h1^#(x)) , g1^#(x, a()) -> c_3(h2^#(x)) , g1^#(a(), x) -> c_4(h1^#(x)) , h2^#(a()) -> c_10() , h1^#(a()) -> c_9() , f2^#(x, a()) -> c_7(g2^#(x, x)) , f2^#(a(), x) -> c_8(g1^#(x, x)) } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..