MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { a__zeros() -> cons(0(), zeros()) , a__zeros() -> zeros() , a__tail(X) -> tail(X) , a__tail(cons(X, XS)) -> mark(XS) , mark(cons(X1, X2)) -> cons(mark(X1), X2) , mark(0()) -> 0() , mark(zeros()) -> a__zeros() , mark(tail(X)) -> a__tail(mark(X)) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { a__zeros^#() -> c_1() , a__zeros^#() -> c_2() , a__tail^#(X) -> c_3() , a__tail^#(cons(X, XS)) -> c_4(mark^#(XS)) , mark^#(cons(X1, X2)) -> c_5(mark^#(X1)) , mark^#(0()) -> c_6() , mark^#(zeros()) -> c_7(a__zeros^#()) , mark^#(tail(X)) -> c_8(a__tail^#(mark(X)), mark^#(X)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__zeros^#() -> c_1() , a__zeros^#() -> c_2() , a__tail^#(X) -> c_3() , a__tail^#(cons(X, XS)) -> c_4(mark^#(XS)) , mark^#(cons(X1, X2)) -> c_5(mark^#(X1)) , mark^#(0()) -> c_6() , mark^#(zeros()) -> c_7(a__zeros^#()) , mark^#(tail(X)) -> c_8(a__tail^#(mark(X)), mark^#(X)) } Weak Trs: { a__zeros() -> cons(0(), zeros()) , a__zeros() -> zeros() , a__tail(X) -> tail(X) , a__tail(cons(X, XS)) -> mark(XS) , mark(cons(X1, X2)) -> cons(mark(X1), X2) , mark(0()) -> 0() , mark(zeros()) -> a__zeros() , mark(tail(X)) -> a__tail(mark(X)) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,6} by applications of Pre({1,2,3,6}) = {4,5,7,8}. Here rules are labeled as follows: DPs: { 1: a__zeros^#() -> c_1() , 2: a__zeros^#() -> c_2() , 3: a__tail^#(X) -> c_3() , 4: a__tail^#(cons(X, XS)) -> c_4(mark^#(XS)) , 5: mark^#(cons(X1, X2)) -> c_5(mark^#(X1)) , 6: mark^#(0()) -> c_6() , 7: mark^#(zeros()) -> c_7(a__zeros^#()) , 8: mark^#(tail(X)) -> c_8(a__tail^#(mark(X)), mark^#(X)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__tail^#(cons(X, XS)) -> c_4(mark^#(XS)) , mark^#(cons(X1, X2)) -> c_5(mark^#(X1)) , mark^#(zeros()) -> c_7(a__zeros^#()) , mark^#(tail(X)) -> c_8(a__tail^#(mark(X)), mark^#(X)) } Weak DPs: { a__zeros^#() -> c_1() , a__zeros^#() -> c_2() , a__tail^#(X) -> c_3() , mark^#(0()) -> c_6() } Weak Trs: { a__zeros() -> cons(0(), zeros()) , a__zeros() -> zeros() , a__tail(X) -> tail(X) , a__tail(cons(X, XS)) -> mark(XS) , mark(cons(X1, X2)) -> cons(mark(X1), X2) , mark(0()) -> 0() , mark(zeros()) -> a__zeros() , mark(tail(X)) -> a__tail(mark(X)) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {3} by applications of Pre({3}) = {1,2,4}. Here rules are labeled as follows: DPs: { 1: a__tail^#(cons(X, XS)) -> c_4(mark^#(XS)) , 2: mark^#(cons(X1, X2)) -> c_5(mark^#(X1)) , 3: mark^#(zeros()) -> c_7(a__zeros^#()) , 4: mark^#(tail(X)) -> c_8(a__tail^#(mark(X)), mark^#(X)) , 5: a__zeros^#() -> c_1() , 6: a__zeros^#() -> c_2() , 7: a__tail^#(X) -> c_3() , 8: mark^#(0()) -> c_6() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__tail^#(cons(X, XS)) -> c_4(mark^#(XS)) , mark^#(cons(X1, X2)) -> c_5(mark^#(X1)) , mark^#(tail(X)) -> c_8(a__tail^#(mark(X)), mark^#(X)) } Weak DPs: { a__zeros^#() -> c_1() , a__zeros^#() -> c_2() , a__tail^#(X) -> c_3() , mark^#(0()) -> c_6() , mark^#(zeros()) -> c_7(a__zeros^#()) } Weak Trs: { a__zeros() -> cons(0(), zeros()) , a__zeros() -> zeros() , a__tail(X) -> tail(X) , a__tail(cons(X, XS)) -> mark(XS) , mark(cons(X1, X2)) -> cons(mark(X1), X2) , mark(0()) -> 0() , mark(zeros()) -> a__zeros() , mark(tail(X)) -> a__tail(mark(X)) } 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. { a__zeros^#() -> c_1() , a__zeros^#() -> c_2() , a__tail^#(X) -> c_3() , mark^#(0()) -> c_6() , mark^#(zeros()) -> c_7(a__zeros^#()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__tail^#(cons(X, XS)) -> c_4(mark^#(XS)) , mark^#(cons(X1, X2)) -> c_5(mark^#(X1)) , mark^#(tail(X)) -> c_8(a__tail^#(mark(X)), mark^#(X)) } Weak Trs: { a__zeros() -> cons(0(), zeros()) , a__zeros() -> zeros() , a__tail(X) -> tail(X) , a__tail(cons(X, XS)) -> mark(XS) , mark(cons(X1, X2)) -> cons(mark(X1), X2) , mark(0()) -> 0() , mark(zeros()) -> a__zeros() , mark(tail(X)) -> a__tail(mark(X)) } 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..