MAYBE 704.47/297.03 MAYBE 704.47/297.03 704.47/297.03 We are left with following problem, upon which TcT provides the 704.47/297.03 certificate MAYBE. 704.47/297.03 704.47/297.03 Strict Trs: 704.47/297.03 { a__a() -> a__c() 704.47/297.03 , a__a() -> a__d() 704.47/297.03 , a__a() -> a() 704.47/297.03 , a__c() -> e() 704.47/297.03 , a__c() -> l() 704.47/297.03 , a__c() -> c() 704.47/297.03 , a__b() -> a__c() 704.47/297.03 , a__b() -> a__d() 704.47/297.03 , a__b() -> b() 704.47/297.03 , a__k() -> l() 704.47/297.03 , a__k() -> m() 704.47/297.03 , a__k() -> k() 704.47/297.03 , a__d() -> m() 704.47/297.03 , a__d() -> d() 704.47/297.03 , a__A() -> a__h(a__f(a__a()), a__f(a__b())) 704.47/297.03 , a__A() -> A() 704.47/297.03 , a__h(X, X) -> a__g(mark(X), mark(X), a__f(a__k())) 704.47/297.03 , a__h(X1, X2) -> h(X1, X2) 704.47/297.03 , a__f(X) -> a__z(mark(X), X) 704.47/297.03 , a__f(X) -> f(X) 704.47/297.03 , a__g(X1, X2, X3) -> g(X1, X2, X3) 704.47/297.03 , a__g(d(), X, X) -> a__A() 704.47/297.03 , mark(e()) -> e() 704.47/297.03 , mark(l()) -> l() 704.47/297.03 , mark(m()) -> m() 704.47/297.03 , mark(d()) -> a__d() 704.47/297.03 , mark(A()) -> a__A() 704.47/297.03 , mark(a()) -> a__a() 704.47/297.03 , mark(b()) -> a__b() 704.47/297.03 , mark(c()) -> a__c() 704.47/297.03 , mark(k()) -> a__k() 704.47/297.03 , mark(z(X1, X2)) -> a__z(mark(X1), X2) 704.47/297.03 , mark(f(X)) -> a__f(mark(X)) 704.47/297.03 , mark(h(X1, X2)) -> a__h(mark(X1), mark(X2)) 704.47/297.03 , mark(g(X1, X2, X3)) -> a__g(mark(X1), mark(X2), mark(X3)) 704.47/297.03 , a__z(X1, X2) -> z(X1, X2) 704.47/297.03 , a__z(e(), X) -> mark(X) } 704.47/297.03 Obligation: 704.47/297.03 runtime complexity 704.47/297.03 Answer: 704.47/297.03 MAYBE 704.47/297.03 704.47/297.03 None of the processors succeeded. 704.47/297.03 704.47/297.03 Details of failed attempt(s): 704.47/297.03 ----------------------------- 704.47/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 704.47/297.03 following reason: 704.47/297.03 704.47/297.03 Computation stopped due to timeout after 297.0 seconds. 704.47/297.03 704.47/297.03 2) 'Best' failed due to the following reason: 704.47/297.03 704.47/297.03 None of the processors succeeded. 704.47/297.03 704.47/297.03 Details of failed attempt(s): 704.47/297.03 ----------------------------- 704.47/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 704.47/297.03 seconds)' failed due to the following reason: 704.47/297.03 704.47/297.03 None of the processors succeeded. 704.47/297.03 704.47/297.03 Details of failed attempt(s): 704.47/297.03 ----------------------------- 704.47/297.03 1) 'empty' failed due to the following reason: 704.47/297.03 704.47/297.03 Empty strict component of the problem is NOT empty. 704.47/297.03 704.47/297.03 2) 'With Problem ...' failed due to the following reason: 704.47/297.03 704.47/297.03 None of the processors succeeded. 704.47/297.03 704.47/297.03 Details of failed attempt(s): 704.47/297.03 ----------------------------- 704.47/297.03 1) 'empty' failed due to the following reason: 704.47/297.03 704.47/297.03 Empty strict component of the problem is NOT empty. 704.47/297.03 704.47/297.03 2) 'Fastest' failed due to the following reason: 704.47/297.03 704.47/297.03 None of the processors succeeded. 704.47/297.03 704.47/297.03 Details of failed attempt(s): 704.47/297.03 ----------------------------- 704.47/297.03 1) 'With Problem ...' failed due to the following reason: 704.47/297.03 704.47/297.03 None of the processors succeeded. 704.47/297.03 704.47/297.03 Details of failed attempt(s): 704.47/297.03 ----------------------------- 704.47/297.03 1) 'empty' failed due to the following reason: 704.47/297.03 704.47/297.03 Empty strict component of the problem is NOT empty. 704.47/297.03 704.47/297.03 2) 'With Problem ...' failed due to the following reason: 704.47/297.03 704.47/297.03 None of the processors succeeded. 704.47/297.03 704.47/297.03 Details of failed attempt(s): 704.47/297.03 ----------------------------- 704.47/297.03 1) 'empty' failed due to the following reason: 704.47/297.03 704.47/297.03 Empty strict component of the problem is NOT empty. 704.47/297.03 704.47/297.03 2) 'With Problem ...' failed due to the following reason: 704.47/297.03 704.47/297.03 None of the processors succeeded. 704.47/297.03 704.47/297.03 Details of failed attempt(s): 704.47/297.03 ----------------------------- 704.47/297.03 1) 'empty' failed due to the following reason: 704.47/297.03 704.47/297.03 Empty strict component of the problem is NOT empty. 704.47/297.03 704.47/297.03 2) 'With Problem ...' failed due to the following reason: 704.47/297.03 704.47/297.03 Empty strict component of the problem is NOT empty. 704.47/297.03 704.47/297.03 704.47/297.03 704.47/297.03 704.47/297.03 2) 'With Problem ...' failed due to the following reason: 704.47/297.03 704.47/297.03 None of the processors succeeded. 704.47/297.03 704.47/297.03 Details of failed attempt(s): 704.47/297.03 ----------------------------- 704.47/297.03 1) 'empty' failed due to the following reason: 704.47/297.03 704.47/297.03 Empty strict component of the problem is NOT empty. 704.47/297.03 704.47/297.03 2) 'With Problem ...' failed due to the following reason: 704.47/297.03 704.47/297.03 Empty strict component of the problem is NOT empty. 704.47/297.03 704.47/297.03 704.47/297.03 704.47/297.03 704.47/297.03 704.47/297.03 2) 'Best' failed due to the following reason: 704.47/297.03 704.47/297.03 None of the processors succeeded. 704.47/297.03 704.47/297.03 Details of failed attempt(s): 704.47/297.03 ----------------------------- 704.47/297.03 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 704.47/297.03 following reason: 704.47/297.03 704.47/297.03 The processor is inapplicable, reason: 704.47/297.03 Processor only applicable for innermost runtime complexity analysis 704.47/297.03 704.47/297.03 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 704.47/297.03 to the following reason: 704.47/297.03 704.47/297.03 The processor is inapplicable, reason: 704.47/297.03 Processor only applicable for innermost runtime complexity analysis 704.47/297.03 704.47/297.03 704.47/297.03 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 704.47/297.03 failed due to the following reason: 704.47/297.03 704.47/297.03 None of the processors succeeded. 704.47/297.03 704.47/297.03 Details of failed attempt(s): 704.47/297.03 ----------------------------- 704.47/297.03 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 704.47/297.03 failed due to the following reason: 704.47/297.03 704.47/297.03 match-boundness of the problem could not be verified. 704.47/297.03 704.47/297.03 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 704.47/297.03 failed due to the following reason: 704.47/297.03 704.47/297.03 match-boundness of the problem could not be verified. 704.47/297.03 704.47/297.03 704.47/297.03 704.47/297.03 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 704.47/297.03 the following reason: 704.47/297.03 704.47/297.03 We add the following weak dependency pairs: 704.47/297.03 704.47/297.03 Strict DPs: 704.47/297.03 { a__a^#() -> c_1(a__c^#()) 704.47/297.03 , a__a^#() -> c_2(a__d^#()) 704.47/297.03 , a__a^#() -> c_3() 704.47/297.03 , a__c^#() -> c_4() 704.47/297.03 , a__c^#() -> c_5() 704.47/297.03 , a__c^#() -> c_6() 704.47/297.03 , a__d^#() -> c_13() 704.47/297.03 , a__d^#() -> c_14() 704.47/297.03 , a__b^#() -> c_7(a__c^#()) 704.47/297.03 , a__b^#() -> c_8(a__d^#()) 704.47/297.03 , a__b^#() -> c_9() 704.47/297.03 , a__k^#() -> c_10() 704.47/297.03 , a__k^#() -> c_11() 704.47/297.03 , a__k^#() -> c_12() 704.47/297.03 , a__A^#() -> c_15(a__h^#(a__f(a__a()), a__f(a__b()))) 704.47/297.03 , a__A^#() -> c_16() 704.47/297.03 , a__h^#(X, X) -> c_17(a__g^#(mark(X), mark(X), a__f(a__k()))) 704.47/297.03 , a__h^#(X1, X2) -> c_18(X1, X2) 704.47/297.03 , a__g^#(X1, X2, X3) -> c_21(X1, X2, X3) 704.47/297.03 , a__g^#(d(), X, X) -> c_22(a__A^#()) 704.47/297.03 , a__f^#(X) -> c_19(a__z^#(mark(X), X)) 704.47/297.03 , a__f^#(X) -> c_20(X) 704.47/297.03 , a__z^#(X1, X2) -> c_36(X1, X2) 704.47/297.03 , a__z^#(e(), X) -> c_37(mark^#(X)) 704.47/297.03 , mark^#(e()) -> c_23() 704.47/297.03 , mark^#(l()) -> c_24() 704.47/297.03 , mark^#(m()) -> c_25() 704.47/297.03 , mark^#(d()) -> c_26(a__d^#()) 704.47/297.03 , mark^#(A()) -> c_27(a__A^#()) 704.47/297.03 , mark^#(a()) -> c_28(a__a^#()) 704.47/297.03 , mark^#(b()) -> c_29(a__b^#()) 704.47/297.03 , mark^#(c()) -> c_30(a__c^#()) 704.47/297.03 , mark^#(k()) -> c_31(a__k^#()) 704.47/297.03 , mark^#(z(X1, X2)) -> c_32(a__z^#(mark(X1), X2)) 704.47/297.03 , mark^#(f(X)) -> c_33(a__f^#(mark(X))) 704.47/297.03 , mark^#(h(X1, X2)) -> c_34(a__h^#(mark(X1), mark(X2))) 704.47/297.03 , mark^#(g(X1, X2, X3)) -> 704.47/297.03 c_35(a__g^#(mark(X1), mark(X2), mark(X3))) } 704.47/297.03 704.47/297.03 and mark the set of starting terms. 704.47/297.03 704.47/297.03 We are left with following problem, upon which TcT provides the 704.47/297.03 certificate MAYBE. 704.47/297.03 704.47/297.03 Strict DPs: 704.47/297.03 { a__a^#() -> c_1(a__c^#()) 704.47/297.03 , a__a^#() -> c_2(a__d^#()) 704.47/297.03 , a__a^#() -> c_3() 704.47/297.03 , a__c^#() -> c_4() 704.47/297.03 , a__c^#() -> c_5() 704.47/297.03 , a__c^#() -> c_6() 704.47/297.03 , a__d^#() -> c_13() 704.47/297.03 , a__d^#() -> c_14() 704.47/297.03 , a__b^#() -> c_7(a__c^#()) 704.47/297.03 , a__b^#() -> c_8(a__d^#()) 704.47/297.03 , a__b^#() -> c_9() 704.47/297.03 , a__k^#() -> c_10() 704.47/297.03 , a__k^#() -> c_11() 704.47/297.03 , a__k^#() -> c_12() 704.47/297.03 , a__A^#() -> c_15(a__h^#(a__f(a__a()), a__f(a__b()))) 704.47/297.03 , a__A^#() -> c_16() 704.47/297.03 , a__h^#(X, X) -> c_17(a__g^#(mark(X), mark(X), a__f(a__k()))) 704.47/297.03 , a__h^#(X1, X2) -> c_18(X1, X2) 704.47/297.03 , a__g^#(X1, X2, X3) -> c_21(X1, X2, X3) 704.47/297.03 , a__g^#(d(), X, X) -> c_22(a__A^#()) 704.47/297.03 , a__f^#(X) -> c_19(a__z^#(mark(X), X)) 704.47/297.03 , a__f^#(X) -> c_20(X) 704.47/297.03 , a__z^#(X1, X2) -> c_36(X1, X2) 704.47/297.03 , a__z^#(e(), X) -> c_37(mark^#(X)) 704.47/297.03 , mark^#(e()) -> c_23() 704.47/297.03 , mark^#(l()) -> c_24() 704.47/297.03 , mark^#(m()) -> c_25() 704.47/297.03 , mark^#(d()) -> c_26(a__d^#()) 704.47/297.03 , mark^#(A()) -> c_27(a__A^#()) 704.47/297.03 , mark^#(a()) -> c_28(a__a^#()) 704.47/297.03 , mark^#(b()) -> c_29(a__b^#()) 704.47/297.03 , mark^#(c()) -> c_30(a__c^#()) 704.47/297.03 , mark^#(k()) -> c_31(a__k^#()) 704.47/297.03 , mark^#(z(X1, X2)) -> c_32(a__z^#(mark(X1), X2)) 704.47/297.03 , mark^#(f(X)) -> c_33(a__f^#(mark(X))) 704.47/297.03 , mark^#(h(X1, X2)) -> c_34(a__h^#(mark(X1), mark(X2))) 704.47/297.03 , mark^#(g(X1, X2, X3)) -> 704.47/297.03 c_35(a__g^#(mark(X1), mark(X2), mark(X3))) } 704.47/297.03 Strict Trs: 704.47/297.03 { a__a() -> a__c() 704.47/297.03 , a__a() -> a__d() 704.47/297.03 , a__a() -> a() 704.47/297.03 , a__c() -> e() 704.47/297.03 , a__c() -> l() 704.47/297.03 , a__c() -> c() 704.47/297.03 , a__b() -> a__c() 704.47/297.03 , a__b() -> a__d() 704.47/297.03 , a__b() -> b() 704.47/297.03 , a__k() -> l() 704.47/297.03 , a__k() -> m() 704.47/297.03 , a__k() -> k() 704.47/297.03 , a__d() -> m() 704.47/297.03 , a__d() -> d() 704.47/297.03 , a__A() -> a__h(a__f(a__a()), a__f(a__b())) 704.47/297.03 , a__A() -> A() 704.47/297.03 , a__h(X, X) -> a__g(mark(X), mark(X), a__f(a__k())) 704.47/297.03 , a__h(X1, X2) -> h(X1, X2) 704.47/297.03 , a__f(X) -> a__z(mark(X), X) 704.47/297.03 , a__f(X) -> f(X) 704.47/297.03 , a__g(X1, X2, X3) -> g(X1, X2, X3) 704.47/297.03 , a__g(d(), X, X) -> a__A() 704.47/297.03 , mark(e()) -> e() 704.47/297.03 , mark(l()) -> l() 704.47/297.03 , mark(m()) -> m() 704.47/297.03 , mark(d()) -> a__d() 704.47/297.03 , mark(A()) -> a__A() 704.47/297.03 , mark(a()) -> a__a() 704.47/297.03 , mark(b()) -> a__b() 704.47/297.03 , mark(c()) -> a__c() 704.47/297.03 , mark(k()) -> a__k() 704.47/297.03 , mark(z(X1, X2)) -> a__z(mark(X1), X2) 704.47/297.03 , mark(f(X)) -> a__f(mark(X)) 704.47/297.03 , mark(h(X1, X2)) -> a__h(mark(X1), mark(X2)) 704.47/297.03 , mark(g(X1, X2, X3)) -> a__g(mark(X1), mark(X2), mark(X3)) 704.47/297.03 , a__z(X1, X2) -> z(X1, X2) 704.47/297.03 , a__z(e(), X) -> mark(X) } 704.47/297.03 Obligation: 704.47/297.03 runtime complexity 704.47/297.03 Answer: 704.47/297.03 MAYBE 704.47/297.03 704.47/297.03 We estimate the number of application of 704.47/297.03 {3,4,5,6,7,8,11,12,13,14,16,25,26,27} by applications of 704.47/297.03 Pre({3,4,5,6,7,8,11,12,13,14,16,25,26,27}) = 704.47/297.03 {1,2,9,10,18,19,20,22,23,24,28,29,30,31,32,33}. Here rules are 704.47/297.03 labeled as follows: 704.47/297.03 704.47/297.03 DPs: 704.47/297.03 { 1: a__a^#() -> c_1(a__c^#()) 704.47/297.03 , 2: a__a^#() -> c_2(a__d^#()) 704.47/297.03 , 3: a__a^#() -> c_3() 704.47/297.03 , 4: a__c^#() -> c_4() 704.47/297.03 , 5: a__c^#() -> c_5() 704.47/297.03 , 6: a__c^#() -> c_6() 704.47/297.03 , 7: a__d^#() -> c_13() 704.47/297.03 , 8: a__d^#() -> c_14() 704.47/297.03 , 9: a__b^#() -> c_7(a__c^#()) 704.47/297.03 , 10: a__b^#() -> c_8(a__d^#()) 704.47/297.03 , 11: a__b^#() -> c_9() 704.47/297.03 , 12: a__k^#() -> c_10() 704.47/297.03 , 13: a__k^#() -> c_11() 704.47/297.03 , 14: a__k^#() -> c_12() 704.47/297.03 , 15: a__A^#() -> c_15(a__h^#(a__f(a__a()), a__f(a__b()))) 704.47/297.03 , 16: a__A^#() -> c_16() 704.47/297.03 , 17: a__h^#(X, X) -> c_17(a__g^#(mark(X), mark(X), a__f(a__k()))) 704.47/297.03 , 18: a__h^#(X1, X2) -> c_18(X1, X2) 704.47/297.03 , 19: a__g^#(X1, X2, X3) -> c_21(X1, X2, X3) 704.47/297.03 , 20: a__g^#(d(), X, X) -> c_22(a__A^#()) 704.47/297.03 , 21: a__f^#(X) -> c_19(a__z^#(mark(X), X)) 704.47/297.03 , 22: a__f^#(X) -> c_20(X) 704.47/297.03 , 23: a__z^#(X1, X2) -> c_36(X1, X2) 704.47/297.03 , 24: a__z^#(e(), X) -> c_37(mark^#(X)) 704.47/297.03 , 25: mark^#(e()) -> c_23() 704.47/297.03 , 26: mark^#(l()) -> c_24() 704.47/297.03 , 27: mark^#(m()) -> c_25() 704.47/297.03 , 28: mark^#(d()) -> c_26(a__d^#()) 704.47/297.03 , 29: mark^#(A()) -> c_27(a__A^#()) 704.47/297.03 , 30: mark^#(a()) -> c_28(a__a^#()) 704.47/297.03 , 31: mark^#(b()) -> c_29(a__b^#()) 704.47/297.03 , 32: mark^#(c()) -> c_30(a__c^#()) 704.47/297.03 , 33: mark^#(k()) -> c_31(a__k^#()) 704.47/297.03 , 34: mark^#(z(X1, X2)) -> c_32(a__z^#(mark(X1), X2)) 704.47/297.03 , 35: mark^#(f(X)) -> c_33(a__f^#(mark(X))) 704.47/297.03 , 36: mark^#(h(X1, X2)) -> c_34(a__h^#(mark(X1), mark(X2))) 704.47/297.03 , 37: mark^#(g(X1, X2, X3)) -> 704.47/297.03 c_35(a__g^#(mark(X1), mark(X2), mark(X3))) } 704.47/297.03 704.47/297.03 We are left with following problem, upon which TcT provides the 704.47/297.03 certificate MAYBE. 704.47/297.03 704.47/297.03 Strict DPs: 704.47/297.03 { a__a^#() -> c_1(a__c^#()) 704.47/297.03 , a__a^#() -> c_2(a__d^#()) 704.47/297.03 , a__b^#() -> c_7(a__c^#()) 704.47/297.03 , a__b^#() -> c_8(a__d^#()) 704.47/297.03 , a__A^#() -> c_15(a__h^#(a__f(a__a()), a__f(a__b()))) 704.47/297.03 , a__h^#(X, X) -> c_17(a__g^#(mark(X), mark(X), a__f(a__k()))) 704.47/297.03 , a__h^#(X1, X2) -> c_18(X1, X2) 704.47/297.03 , a__g^#(X1, X2, X3) -> c_21(X1, X2, X3) 704.47/297.03 , a__g^#(d(), X, X) -> c_22(a__A^#()) 704.47/297.03 , a__f^#(X) -> c_19(a__z^#(mark(X), X)) 704.47/297.03 , a__f^#(X) -> c_20(X) 704.47/297.03 , a__z^#(X1, X2) -> c_36(X1, X2) 704.47/297.03 , a__z^#(e(), X) -> c_37(mark^#(X)) 704.47/297.03 , mark^#(d()) -> c_26(a__d^#()) 704.47/297.03 , mark^#(A()) -> c_27(a__A^#()) 704.47/297.03 , mark^#(a()) -> c_28(a__a^#()) 704.47/297.03 , mark^#(b()) -> c_29(a__b^#()) 704.47/297.03 , mark^#(c()) -> c_30(a__c^#()) 704.47/297.03 , mark^#(k()) -> c_31(a__k^#()) 704.47/297.03 , mark^#(z(X1, X2)) -> c_32(a__z^#(mark(X1), X2)) 704.47/297.03 , mark^#(f(X)) -> c_33(a__f^#(mark(X))) 704.47/297.03 , mark^#(h(X1, X2)) -> c_34(a__h^#(mark(X1), mark(X2))) 704.47/297.03 , mark^#(g(X1, X2, X3)) -> 704.47/297.03 c_35(a__g^#(mark(X1), mark(X2), mark(X3))) } 704.47/297.03 Strict Trs: 704.47/297.03 { a__a() -> a__c() 704.47/297.03 , a__a() -> a__d() 704.47/297.03 , a__a() -> a() 704.47/297.03 , a__c() -> e() 704.47/297.03 , a__c() -> l() 704.47/297.03 , a__c() -> c() 704.47/297.03 , a__b() -> a__c() 704.47/297.03 , a__b() -> a__d() 704.47/297.03 , a__b() -> b() 704.47/297.03 , a__k() -> l() 704.47/297.03 , a__k() -> m() 704.47/297.03 , a__k() -> k() 704.47/297.03 , a__d() -> m() 704.47/297.03 , a__d() -> d() 704.47/297.03 , a__A() -> a__h(a__f(a__a()), a__f(a__b())) 704.47/297.03 , a__A() -> A() 704.47/297.03 , a__h(X, X) -> a__g(mark(X), mark(X), a__f(a__k())) 704.47/297.03 , a__h(X1, X2) -> h(X1, X2) 704.47/297.03 , a__f(X) -> a__z(mark(X), X) 704.47/297.03 , a__f(X) -> f(X) 704.47/297.03 , a__g(X1, X2, X3) -> g(X1, X2, X3) 704.47/297.03 , a__g(d(), X, X) -> a__A() 704.47/297.03 , mark(e()) -> e() 704.47/297.03 , mark(l()) -> l() 704.47/297.03 , mark(m()) -> m() 704.47/297.03 , mark(d()) -> a__d() 704.47/297.03 , mark(A()) -> a__A() 704.47/297.03 , mark(a()) -> a__a() 704.47/297.03 , mark(b()) -> a__b() 704.47/297.03 , mark(c()) -> a__c() 704.47/297.03 , mark(k()) -> a__k() 704.47/297.03 , mark(z(X1, X2)) -> a__z(mark(X1), X2) 704.47/297.03 , mark(f(X)) -> a__f(mark(X)) 704.47/297.03 , mark(h(X1, X2)) -> a__h(mark(X1), mark(X2)) 704.47/297.03 , mark(g(X1, X2, X3)) -> a__g(mark(X1), mark(X2), mark(X3)) 704.47/297.03 , a__z(X1, X2) -> z(X1, X2) 704.47/297.03 , a__z(e(), X) -> mark(X) } 704.47/297.03 Weak DPs: 704.47/297.03 { a__a^#() -> c_3() 704.47/297.03 , a__c^#() -> c_4() 704.47/297.03 , a__c^#() -> c_5() 704.47/297.03 , a__c^#() -> c_6() 704.47/297.03 , a__d^#() -> c_13() 704.47/297.03 , a__d^#() -> c_14() 704.47/297.03 , a__b^#() -> c_9() 704.47/297.03 , a__k^#() -> c_10() 704.47/297.03 , a__k^#() -> c_11() 704.47/297.03 , a__k^#() -> c_12() 704.47/297.03 , a__A^#() -> c_16() 704.47/297.03 , mark^#(e()) -> c_23() 704.47/297.03 , mark^#(l()) -> c_24() 704.47/297.03 , mark^#(m()) -> c_25() } 704.47/297.03 Obligation: 704.47/297.03 runtime complexity 704.47/297.03 Answer: 704.47/297.03 MAYBE 704.47/297.03 704.47/297.03 We estimate the number of application of {1,2,3,4,14,18,19} by 704.47/297.03 applications of Pre({1,2,3,4,14,18,19}) = {7,8,11,12,13,16,17}. 704.47/297.03 Here rules are labeled as follows: 704.47/297.03 704.47/297.03 DPs: 704.47/297.03 { 1: a__a^#() -> c_1(a__c^#()) 704.47/297.03 , 2: a__a^#() -> c_2(a__d^#()) 704.47/297.03 , 3: a__b^#() -> c_7(a__c^#()) 704.47/297.03 , 4: a__b^#() -> c_8(a__d^#()) 704.47/297.03 , 5: a__A^#() -> c_15(a__h^#(a__f(a__a()), a__f(a__b()))) 704.47/297.03 , 6: a__h^#(X, X) -> c_17(a__g^#(mark(X), mark(X), a__f(a__k()))) 704.47/297.03 , 7: a__h^#(X1, X2) -> c_18(X1, X2) 704.47/297.03 , 8: a__g^#(X1, X2, X3) -> c_21(X1, X2, X3) 704.47/297.03 , 9: a__g^#(d(), X, X) -> c_22(a__A^#()) 704.47/297.03 , 10: a__f^#(X) -> c_19(a__z^#(mark(X), X)) 704.47/297.03 , 11: a__f^#(X) -> c_20(X) 704.47/297.03 , 12: a__z^#(X1, X2) -> c_36(X1, X2) 704.47/297.03 , 13: a__z^#(e(), X) -> c_37(mark^#(X)) 704.47/297.03 , 14: mark^#(d()) -> c_26(a__d^#()) 704.47/297.03 , 15: mark^#(A()) -> c_27(a__A^#()) 704.47/297.03 , 16: mark^#(a()) -> c_28(a__a^#()) 704.47/297.03 , 17: mark^#(b()) -> c_29(a__b^#()) 704.47/297.03 , 18: mark^#(c()) -> c_30(a__c^#()) 704.47/297.03 , 19: mark^#(k()) -> c_31(a__k^#()) 704.47/297.03 , 20: mark^#(z(X1, X2)) -> c_32(a__z^#(mark(X1), X2)) 704.47/297.03 , 21: mark^#(f(X)) -> c_33(a__f^#(mark(X))) 704.47/297.03 , 22: mark^#(h(X1, X2)) -> c_34(a__h^#(mark(X1), mark(X2))) 704.47/297.03 , 23: mark^#(g(X1, X2, X3)) -> 704.47/297.03 c_35(a__g^#(mark(X1), mark(X2), mark(X3))) 704.47/297.03 , 24: a__a^#() -> c_3() 704.47/297.03 , 25: a__c^#() -> c_4() 704.47/297.03 , 26: a__c^#() -> c_5() 704.47/297.03 , 27: a__c^#() -> c_6() 704.47/297.03 , 28: a__d^#() -> c_13() 704.47/297.04 , 29: a__d^#() -> c_14() 704.47/297.04 , 30: a__b^#() -> c_9() 704.47/297.04 , 31: a__k^#() -> c_10() 704.47/297.04 , 32: a__k^#() -> c_11() 704.47/297.04 , 33: a__k^#() -> c_12() 704.47/297.04 , 34: a__A^#() -> c_16() 704.47/297.04 , 35: mark^#(e()) -> c_23() 704.47/297.04 , 36: mark^#(l()) -> c_24() 704.47/297.04 , 37: mark^#(m()) -> c_25() } 704.47/297.04 704.47/297.04 We are left with following problem, upon which TcT provides the 704.47/297.04 certificate MAYBE. 704.47/297.04 704.47/297.04 Strict DPs: 704.47/297.04 { a__A^#() -> c_15(a__h^#(a__f(a__a()), a__f(a__b()))) 704.47/297.04 , a__h^#(X, X) -> c_17(a__g^#(mark(X), mark(X), a__f(a__k()))) 704.47/297.04 , a__h^#(X1, X2) -> c_18(X1, X2) 704.47/297.04 , a__g^#(X1, X2, X3) -> c_21(X1, X2, X3) 704.47/297.04 , a__g^#(d(), X, X) -> c_22(a__A^#()) 704.47/297.04 , a__f^#(X) -> c_19(a__z^#(mark(X), X)) 704.47/297.04 , a__f^#(X) -> c_20(X) 704.47/297.04 , a__z^#(X1, X2) -> c_36(X1, X2) 704.47/297.04 , a__z^#(e(), X) -> c_37(mark^#(X)) 704.47/297.04 , mark^#(A()) -> c_27(a__A^#()) 704.47/297.04 , mark^#(a()) -> c_28(a__a^#()) 704.47/297.04 , mark^#(b()) -> c_29(a__b^#()) 704.47/297.04 , mark^#(z(X1, X2)) -> c_32(a__z^#(mark(X1), X2)) 704.47/297.04 , mark^#(f(X)) -> c_33(a__f^#(mark(X))) 704.47/297.04 , mark^#(h(X1, X2)) -> c_34(a__h^#(mark(X1), mark(X2))) 704.47/297.04 , mark^#(g(X1, X2, X3)) -> 704.47/297.04 c_35(a__g^#(mark(X1), mark(X2), mark(X3))) } 704.47/297.04 Strict Trs: 704.47/297.04 { a__a() -> a__c() 704.47/297.04 , a__a() -> a__d() 704.47/297.04 , a__a() -> a() 704.47/297.04 , a__c() -> e() 704.47/297.04 , a__c() -> l() 704.47/297.04 , a__c() -> c() 704.47/297.04 , a__b() -> a__c() 704.47/297.04 , a__b() -> a__d() 704.47/297.04 , a__b() -> b() 704.47/297.04 , a__k() -> l() 704.47/297.04 , a__k() -> m() 704.47/297.04 , a__k() -> k() 704.47/297.04 , a__d() -> m() 704.47/297.04 , a__d() -> d() 704.47/297.04 , a__A() -> a__h(a__f(a__a()), a__f(a__b())) 704.47/297.04 , a__A() -> A() 704.47/297.04 , a__h(X, X) -> a__g(mark(X), mark(X), a__f(a__k())) 704.47/297.04 , a__h(X1, X2) -> h(X1, X2) 704.47/297.04 , a__f(X) -> a__z(mark(X), X) 704.47/297.04 , a__f(X) -> f(X) 704.47/297.04 , a__g(X1, X2, X3) -> g(X1, X2, X3) 704.47/297.04 , a__g(d(), X, X) -> a__A() 704.47/297.04 , mark(e()) -> e() 704.47/297.04 , mark(l()) -> l() 704.47/297.04 , mark(m()) -> m() 704.47/297.04 , mark(d()) -> a__d() 704.47/297.04 , mark(A()) -> a__A() 704.47/297.04 , mark(a()) -> a__a() 704.47/297.04 , mark(b()) -> a__b() 704.47/297.04 , mark(c()) -> a__c() 704.47/297.04 , mark(k()) -> a__k() 704.47/297.04 , mark(z(X1, X2)) -> a__z(mark(X1), X2) 704.47/297.04 , mark(f(X)) -> a__f(mark(X)) 704.47/297.04 , mark(h(X1, X2)) -> a__h(mark(X1), mark(X2)) 704.47/297.04 , mark(g(X1, X2, X3)) -> a__g(mark(X1), mark(X2), mark(X3)) 704.47/297.04 , a__z(X1, X2) -> z(X1, X2) 704.47/297.04 , a__z(e(), X) -> mark(X) } 704.47/297.04 Weak DPs: 704.47/297.04 { a__a^#() -> c_1(a__c^#()) 704.47/297.04 , a__a^#() -> c_2(a__d^#()) 704.47/297.04 , a__a^#() -> c_3() 704.47/297.04 , a__c^#() -> c_4() 704.47/297.04 , a__c^#() -> c_5() 704.47/297.04 , a__c^#() -> c_6() 704.47/297.04 , a__d^#() -> c_13() 704.47/297.04 , a__d^#() -> c_14() 704.47/297.04 , a__b^#() -> c_7(a__c^#()) 704.47/297.04 , a__b^#() -> c_8(a__d^#()) 704.47/297.04 , a__b^#() -> c_9() 704.47/297.04 , a__k^#() -> c_10() 704.47/297.04 , a__k^#() -> c_11() 704.47/297.04 , a__k^#() -> c_12() 704.47/297.04 , a__A^#() -> c_16() 704.47/297.04 , mark^#(e()) -> c_23() 704.47/297.04 , mark^#(l()) -> c_24() 704.47/297.04 , mark^#(m()) -> c_25() 704.47/297.04 , mark^#(d()) -> c_26(a__d^#()) 704.47/297.04 , mark^#(c()) -> c_30(a__c^#()) 704.47/297.04 , mark^#(k()) -> c_31(a__k^#()) } 704.47/297.04 Obligation: 704.47/297.04 runtime complexity 704.47/297.04 Answer: 704.47/297.04 MAYBE 704.47/297.04 704.47/297.04 We estimate the number of application of {11,12} by applications of 704.47/297.04 Pre({11,12}) = {3,4,7,8,9}. Here rules are labeled as follows: 704.47/297.04 704.47/297.04 DPs: 704.47/297.04 { 1: a__A^#() -> c_15(a__h^#(a__f(a__a()), a__f(a__b()))) 704.47/297.04 , 2: a__h^#(X, X) -> c_17(a__g^#(mark(X), mark(X), a__f(a__k()))) 704.47/297.04 , 3: a__h^#(X1, X2) -> c_18(X1, X2) 704.47/297.04 , 4: a__g^#(X1, X2, X3) -> c_21(X1, X2, X3) 704.47/297.04 , 5: a__g^#(d(), X, X) -> c_22(a__A^#()) 704.47/297.04 , 6: a__f^#(X) -> c_19(a__z^#(mark(X), X)) 704.47/297.04 , 7: a__f^#(X) -> c_20(X) 704.47/297.04 , 8: a__z^#(X1, X2) -> c_36(X1, X2) 704.47/297.04 , 9: a__z^#(e(), X) -> c_37(mark^#(X)) 704.47/297.04 , 10: mark^#(A()) -> c_27(a__A^#()) 704.47/297.04 , 11: mark^#(a()) -> c_28(a__a^#()) 704.47/297.04 , 12: mark^#(b()) -> c_29(a__b^#()) 704.47/297.04 , 13: mark^#(z(X1, X2)) -> c_32(a__z^#(mark(X1), X2)) 704.47/297.04 , 14: mark^#(f(X)) -> c_33(a__f^#(mark(X))) 704.47/297.04 , 15: mark^#(h(X1, X2)) -> c_34(a__h^#(mark(X1), mark(X2))) 704.47/297.04 , 16: mark^#(g(X1, X2, X3)) -> 704.47/297.04 c_35(a__g^#(mark(X1), mark(X2), mark(X3))) 704.47/297.04 , 17: a__a^#() -> c_1(a__c^#()) 704.47/297.04 , 18: a__a^#() -> c_2(a__d^#()) 704.47/297.04 , 19: a__a^#() -> c_3() 704.47/297.04 , 20: a__c^#() -> c_4() 704.47/297.04 , 21: a__c^#() -> c_5() 704.47/297.04 , 22: a__c^#() -> c_6() 704.47/297.04 , 23: a__d^#() -> c_13() 704.47/297.04 , 24: a__d^#() -> c_14() 704.47/297.04 , 25: a__b^#() -> c_7(a__c^#()) 704.47/297.04 , 26: a__b^#() -> c_8(a__d^#()) 704.47/297.04 , 27: a__b^#() -> c_9() 704.47/297.04 , 28: a__k^#() -> c_10() 704.47/297.04 , 29: a__k^#() -> c_11() 704.47/297.04 , 30: a__k^#() -> c_12() 704.47/297.04 , 31: a__A^#() -> c_16() 704.47/297.04 , 32: mark^#(e()) -> c_23() 704.47/297.04 , 33: mark^#(l()) -> c_24() 704.47/297.04 , 34: mark^#(m()) -> c_25() 704.47/297.04 , 35: mark^#(d()) -> c_26(a__d^#()) 704.47/297.04 , 36: mark^#(c()) -> c_30(a__c^#()) 704.47/297.04 , 37: mark^#(k()) -> c_31(a__k^#()) } 704.47/297.04 704.47/297.04 We are left with following problem, upon which TcT provides the 704.47/297.04 certificate MAYBE. 704.47/297.04 704.47/297.04 Strict DPs: 704.47/297.04 { a__A^#() -> c_15(a__h^#(a__f(a__a()), a__f(a__b()))) 704.47/297.04 , a__h^#(X, X) -> c_17(a__g^#(mark(X), mark(X), a__f(a__k()))) 704.47/297.04 , a__h^#(X1, X2) -> c_18(X1, X2) 704.47/297.04 , a__g^#(X1, X2, X3) -> c_21(X1, X2, X3) 704.47/297.04 , a__g^#(d(), X, X) -> c_22(a__A^#()) 704.47/297.04 , a__f^#(X) -> c_19(a__z^#(mark(X), X)) 704.47/297.04 , a__f^#(X) -> c_20(X) 704.47/297.04 , a__z^#(X1, X2) -> c_36(X1, X2) 704.47/297.04 , a__z^#(e(), X) -> c_37(mark^#(X)) 704.47/297.04 , mark^#(A()) -> c_27(a__A^#()) 704.47/297.04 , mark^#(z(X1, X2)) -> c_32(a__z^#(mark(X1), X2)) 704.47/297.04 , mark^#(f(X)) -> c_33(a__f^#(mark(X))) 704.47/297.04 , mark^#(h(X1, X2)) -> c_34(a__h^#(mark(X1), mark(X2))) 704.47/297.04 , mark^#(g(X1, X2, X3)) -> 704.47/297.04 c_35(a__g^#(mark(X1), mark(X2), mark(X3))) } 704.47/297.04 Strict Trs: 704.47/297.04 { a__a() -> a__c() 704.47/297.04 , a__a() -> a__d() 704.47/297.04 , a__a() -> a() 704.47/297.04 , a__c() -> e() 704.47/297.04 , a__c() -> l() 704.47/297.04 , a__c() -> c() 704.47/297.04 , a__b() -> a__c() 704.47/297.04 , a__b() -> a__d() 704.47/297.04 , a__b() -> b() 704.47/297.04 , a__k() -> l() 704.47/297.04 , a__k() -> m() 704.47/297.04 , a__k() -> k() 704.47/297.04 , a__d() -> m() 704.47/297.04 , a__d() -> d() 704.47/297.04 , a__A() -> a__h(a__f(a__a()), a__f(a__b())) 704.47/297.04 , a__A() -> A() 704.47/297.04 , a__h(X, X) -> a__g(mark(X), mark(X), a__f(a__k())) 704.47/297.04 , a__h(X1, X2) -> h(X1, X2) 704.47/297.04 , a__f(X) -> a__z(mark(X), X) 704.47/297.04 , a__f(X) -> f(X) 704.47/297.04 , a__g(X1, X2, X3) -> g(X1, X2, X3) 704.47/297.04 , a__g(d(), X, X) -> a__A() 704.47/297.04 , mark(e()) -> e() 704.47/297.04 , mark(l()) -> l() 704.47/297.04 , mark(m()) -> m() 704.47/297.04 , mark(d()) -> a__d() 704.47/297.04 , mark(A()) -> a__A() 704.47/297.04 , mark(a()) -> a__a() 704.47/297.04 , mark(b()) -> a__b() 704.47/297.04 , mark(c()) -> a__c() 704.47/297.04 , mark(k()) -> a__k() 704.47/297.04 , mark(z(X1, X2)) -> a__z(mark(X1), X2) 704.47/297.04 , mark(f(X)) -> a__f(mark(X)) 704.47/297.04 , mark(h(X1, X2)) -> a__h(mark(X1), mark(X2)) 704.47/297.04 , mark(g(X1, X2, X3)) -> a__g(mark(X1), mark(X2), mark(X3)) 704.47/297.04 , a__z(X1, X2) -> z(X1, X2) 704.47/297.04 , a__z(e(), X) -> mark(X) } 704.47/297.04 Weak DPs: 704.47/297.04 { a__a^#() -> c_1(a__c^#()) 704.47/297.04 , a__a^#() -> c_2(a__d^#()) 704.47/297.04 , a__a^#() -> c_3() 704.47/297.04 , a__c^#() -> c_4() 704.47/297.04 , a__c^#() -> c_5() 704.47/297.04 , a__c^#() -> c_6() 704.47/297.04 , a__d^#() -> c_13() 704.47/297.04 , a__d^#() -> c_14() 704.47/297.04 , a__b^#() -> c_7(a__c^#()) 704.47/297.04 , a__b^#() -> c_8(a__d^#()) 704.47/297.04 , a__b^#() -> c_9() 704.47/297.04 , a__k^#() -> c_10() 704.47/297.04 , a__k^#() -> c_11() 704.47/297.04 , a__k^#() -> c_12() 704.47/297.04 , a__A^#() -> c_16() 704.47/297.04 , mark^#(e()) -> c_23() 704.47/297.04 , mark^#(l()) -> c_24() 704.47/297.04 , mark^#(m()) -> c_25() 704.47/297.04 , mark^#(d()) -> c_26(a__d^#()) 704.47/297.04 , mark^#(a()) -> c_28(a__a^#()) 704.47/297.04 , mark^#(b()) -> c_29(a__b^#()) 704.47/297.04 , mark^#(c()) -> c_30(a__c^#()) 704.47/297.04 , mark^#(k()) -> c_31(a__k^#()) } 704.47/297.04 Obligation: 704.47/297.04 runtime complexity 704.47/297.04 Answer: 704.47/297.04 MAYBE 704.47/297.04 704.47/297.04 Empty strict component of the problem is NOT empty. 704.47/297.04 704.47/297.04 704.47/297.04 Arrrr.. 704.60/297.16 EOF