MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { rev(nil()) -> nil() , rev(++(x, y)) -> ++(rev1(x, y), rev2(x, y)) , rev1(x, nil()) -> x , rev1(x, ++(y, z)) -> rev1(y, z) , rev2(x, nil()) -> nil() , rev2(x, ++(y, z)) -> rev(++(x, rev(rev2(y, z)))) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { rev^#(nil()) -> c_1() , rev^#(++(x, y)) -> c_2(rev1^#(x, y), rev2^#(x, y)) , rev1^#(x, nil()) -> c_3() , rev1^#(x, ++(y, z)) -> c_4(rev1^#(y, z)) , rev2^#(x, nil()) -> c_5() , rev2^#(x, ++(y, z)) -> c_6(rev^#(++(x, rev(rev2(y, z)))), rev^#(rev2(y, z)), rev2^#(y, z)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { rev^#(nil()) -> c_1() , rev^#(++(x, y)) -> c_2(rev1^#(x, y), rev2^#(x, y)) , rev1^#(x, nil()) -> c_3() , rev1^#(x, ++(y, z)) -> c_4(rev1^#(y, z)) , rev2^#(x, nil()) -> c_5() , rev2^#(x, ++(y, z)) -> c_6(rev^#(++(x, rev(rev2(y, z)))), rev^#(rev2(y, z)), rev2^#(y, z)) } Weak Trs: { rev(nil()) -> nil() , rev(++(x, y)) -> ++(rev1(x, y), rev2(x, y)) , rev1(x, nil()) -> x , rev1(x, ++(y, z)) -> rev1(y, z) , rev2(x, nil()) -> nil() , rev2(x, ++(y, z)) -> rev(++(x, rev(rev2(y, z)))) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,3,5} by applications of Pre({1,3,5}) = {2,4,6}. Here rules are labeled as follows: DPs: { 1: rev^#(nil()) -> c_1() , 2: rev^#(++(x, y)) -> c_2(rev1^#(x, y), rev2^#(x, y)) , 3: rev1^#(x, nil()) -> c_3() , 4: rev1^#(x, ++(y, z)) -> c_4(rev1^#(y, z)) , 5: rev2^#(x, nil()) -> c_5() , 6: rev2^#(x, ++(y, z)) -> c_6(rev^#(++(x, rev(rev2(y, z)))), rev^#(rev2(y, z)), rev2^#(y, z)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { rev^#(++(x, y)) -> c_2(rev1^#(x, y), rev2^#(x, y)) , rev1^#(x, ++(y, z)) -> c_4(rev1^#(y, z)) , rev2^#(x, ++(y, z)) -> c_6(rev^#(++(x, rev(rev2(y, z)))), rev^#(rev2(y, z)), rev2^#(y, z)) } Weak DPs: { rev^#(nil()) -> c_1() , rev1^#(x, nil()) -> c_3() , rev2^#(x, nil()) -> c_5() } Weak Trs: { rev(nil()) -> nil() , rev(++(x, y)) -> ++(rev1(x, y), rev2(x, y)) , rev1(x, nil()) -> x , rev1(x, ++(y, z)) -> rev1(y, z) , rev2(x, nil()) -> nil() , rev2(x, ++(y, z)) -> rev(++(x, rev(rev2(y, z)))) } 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. { rev^#(nil()) -> c_1() , rev1^#(x, nil()) -> c_3() , rev2^#(x, nil()) -> c_5() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { rev^#(++(x, y)) -> c_2(rev1^#(x, y), rev2^#(x, y)) , rev1^#(x, ++(y, z)) -> c_4(rev1^#(y, z)) , rev2^#(x, ++(y, z)) -> c_6(rev^#(++(x, rev(rev2(y, z)))), rev^#(rev2(y, z)), rev2^#(y, z)) } Weak Trs: { rev(nil()) -> nil() , rev(++(x, y)) -> ++(rev1(x, y), rev2(x, y)) , rev1(x, nil()) -> x , rev1(x, ++(y, z)) -> rev1(y, z) , rev2(x, nil()) -> nil() , rev2(x, ++(y, z)) -> rev(++(x, rev(rev2(y, z)))) } 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: Following exception was raised: stack overflow 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..