MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { acka(y(), n) -> s(n) , acka(a(m), y()) -> acka(m, s(0())) , acka(a(m), a(n)) -> acka(m, ackb(s(m), n)) , s(n) -> a(n) , s(n) -> b(n) , 0() -> y() , 0() -> z() , ackb(z(), n) -> s(n) , ackb(b(m), z()) -> ackb(m, s(0())) , ackb(b(m), b(n)) -> acka(m, ackb(s(m), n)) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { acka^#(y(), n) -> c_1(s^#(n)) , acka^#(a(m), y()) -> c_2(acka^#(m, s(0())), s^#(0()), 0^#()) , acka^#(a(m), a(n)) -> c_3(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n), s^#(m)) , s^#(n) -> c_4() , s^#(n) -> c_5() , 0^#() -> c_6() , 0^#() -> c_7() , ackb^#(z(), n) -> c_8(s^#(n)) , ackb^#(b(m), z()) -> c_9(ackb^#(m, s(0())), s^#(0()), 0^#()) , ackb^#(b(m), b(n)) -> c_10(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n), s^#(m)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { acka^#(y(), n) -> c_1(s^#(n)) , acka^#(a(m), y()) -> c_2(acka^#(m, s(0())), s^#(0()), 0^#()) , acka^#(a(m), a(n)) -> c_3(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n), s^#(m)) , s^#(n) -> c_4() , s^#(n) -> c_5() , 0^#() -> c_6() , 0^#() -> c_7() , ackb^#(z(), n) -> c_8(s^#(n)) , ackb^#(b(m), z()) -> c_9(ackb^#(m, s(0())), s^#(0()), 0^#()) , ackb^#(b(m), b(n)) -> c_10(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n), s^#(m)) } Weak Trs: { acka(y(), n) -> s(n) , acka(a(m), y()) -> acka(m, s(0())) , acka(a(m), a(n)) -> acka(m, ackb(s(m), n)) , s(n) -> a(n) , s(n) -> b(n) , 0() -> y() , 0() -> z() , ackb(z(), n) -> s(n) , ackb(b(m), z()) -> ackb(m, s(0())) , ackb(b(m), b(n)) -> acka(m, ackb(s(m), n)) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {4,5,6,7} by applications of Pre({4,5,6,7}) = {1,2,3,8,9,10}. Here rules are labeled as follows: DPs: { 1: acka^#(y(), n) -> c_1(s^#(n)) , 2: acka^#(a(m), y()) -> c_2(acka^#(m, s(0())), s^#(0()), 0^#()) , 3: acka^#(a(m), a(n)) -> c_3(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n), s^#(m)) , 4: s^#(n) -> c_4() , 5: s^#(n) -> c_5() , 6: 0^#() -> c_6() , 7: 0^#() -> c_7() , 8: ackb^#(z(), n) -> c_8(s^#(n)) , 9: ackb^#(b(m), z()) -> c_9(ackb^#(m, s(0())), s^#(0()), 0^#()) , 10: ackb^#(b(m), b(n)) -> c_10(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n), s^#(m)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { acka^#(y(), n) -> c_1(s^#(n)) , acka^#(a(m), y()) -> c_2(acka^#(m, s(0())), s^#(0()), 0^#()) , acka^#(a(m), a(n)) -> c_3(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n), s^#(m)) , ackb^#(z(), n) -> c_8(s^#(n)) , ackb^#(b(m), z()) -> c_9(ackb^#(m, s(0())), s^#(0()), 0^#()) , ackb^#(b(m), b(n)) -> c_10(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n), s^#(m)) } Weak DPs: { s^#(n) -> c_4() , s^#(n) -> c_5() , 0^#() -> c_6() , 0^#() -> c_7() } Weak Trs: { acka(y(), n) -> s(n) , acka(a(m), y()) -> acka(m, s(0())) , acka(a(m), a(n)) -> acka(m, ackb(s(m), n)) , s(n) -> a(n) , s(n) -> b(n) , 0() -> y() , 0() -> z() , ackb(z(), n) -> s(n) , ackb(b(m), z()) -> ackb(m, s(0())) , ackb(b(m), b(n)) -> acka(m, ackb(s(m), n)) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,4} by applications of Pre({1,4}) = {2,3,5,6}. Here rules are labeled as follows: DPs: { 1: acka^#(y(), n) -> c_1(s^#(n)) , 2: acka^#(a(m), y()) -> c_2(acka^#(m, s(0())), s^#(0()), 0^#()) , 3: acka^#(a(m), a(n)) -> c_3(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n), s^#(m)) , 4: ackb^#(z(), n) -> c_8(s^#(n)) , 5: ackb^#(b(m), z()) -> c_9(ackb^#(m, s(0())), s^#(0()), 0^#()) , 6: ackb^#(b(m), b(n)) -> c_10(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n), s^#(m)) , 7: s^#(n) -> c_4() , 8: s^#(n) -> c_5() , 9: 0^#() -> c_6() , 10: 0^#() -> c_7() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { acka^#(a(m), y()) -> c_2(acka^#(m, s(0())), s^#(0()), 0^#()) , acka^#(a(m), a(n)) -> c_3(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n), s^#(m)) , ackb^#(b(m), z()) -> c_9(ackb^#(m, s(0())), s^#(0()), 0^#()) , ackb^#(b(m), b(n)) -> c_10(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n), s^#(m)) } Weak DPs: { acka^#(y(), n) -> c_1(s^#(n)) , s^#(n) -> c_4() , s^#(n) -> c_5() , 0^#() -> c_6() , 0^#() -> c_7() , ackb^#(z(), n) -> c_8(s^#(n)) } Weak Trs: { acka(y(), n) -> s(n) , acka(a(m), y()) -> acka(m, s(0())) , acka(a(m), a(n)) -> acka(m, ackb(s(m), n)) , s(n) -> a(n) , s(n) -> b(n) , 0() -> y() , 0() -> z() , ackb(z(), n) -> s(n) , ackb(b(m), z()) -> ackb(m, s(0())) , ackb(b(m), b(n)) -> acka(m, ackb(s(m), n)) } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { acka^#(y(), n) -> c_1(s^#(n)) , s^#(n) -> c_4() , s^#(n) -> c_5() , 0^#() -> c_6() , 0^#() -> c_7() , ackb^#(z(), n) -> c_8(s^#(n)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { acka^#(a(m), y()) -> c_2(acka^#(m, s(0())), s^#(0()), 0^#()) , acka^#(a(m), a(n)) -> c_3(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n), s^#(m)) , ackb^#(b(m), z()) -> c_9(ackb^#(m, s(0())), s^#(0()), 0^#()) , ackb^#(b(m), b(n)) -> c_10(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n), s^#(m)) } Weak Trs: { acka(y(), n) -> s(n) , acka(a(m), y()) -> acka(m, s(0())) , acka(a(m), a(n)) -> acka(m, ackb(s(m), n)) , s(n) -> a(n) , s(n) -> b(n) , 0() -> y() , 0() -> z() , ackb(z(), n) -> s(n) , ackb(b(m), z()) -> ackb(m, s(0())) , ackb(b(m), b(n)) -> acka(m, ackb(s(m), n)) } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { acka^#(a(m), y()) -> c_2(acka^#(m, s(0())), s^#(0()), 0^#()) , acka^#(a(m), a(n)) -> c_3(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n), s^#(m)) , ackb^#(b(m), z()) -> c_9(ackb^#(m, s(0())), s^#(0()), 0^#()) , ackb^#(b(m), b(n)) -> c_10(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n), s^#(m)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { acka^#(a(m), y()) -> c_1(acka^#(m, s(0()))) , acka^#(a(m), a(n)) -> c_2(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n)) , ackb^#(b(m), z()) -> c_3(ackb^#(m, s(0()))) , ackb^#(b(m), b(n)) -> c_4(acka^#(m, ackb(s(m), n)), ackb^#(s(m), n)) } Weak Trs: { acka(y(), n) -> s(n) , acka(a(m), y()) -> acka(m, s(0())) , acka(a(m), a(n)) -> acka(m, ackb(s(m), n)) , s(n) -> a(n) , s(n) -> b(n) , 0() -> y() , 0() -> z() , ackb(z(), n) -> s(n) , ackb(b(m), z()) -> ackb(m, s(0())) , ackb(b(m), b(n)) -> acka(m, ackb(s(m), n)) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrices' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrix interpretation of dimension 4' failed due to the following reason: The input cannot be shown compatible 2) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 3) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 4) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 5) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 6) 'matrix interpretation of dimension 1' failed due to the following reason: The input cannot be shown compatible 2) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. Arrrr..