MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { 0(1(2(3(4(5(1(x1))))))) -> 0(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(x1))))))))))))))))))) , 0(1(2(3(4(5(1(x1))))))) -> 1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1))))))))))))))))))))))))) , 0(1(2(3(4(5(1(x1))))))) -> 1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1))))))))))))))))))))))))))))))) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { 0^#(1(2(3(4(5(1(x1))))))) -> c_1(0^#(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(x1))))))))))))))))))), 0^#(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))), 0^#(1(2(3(4(5(x1))))))) , 0^#(1(2(3(4(5(1(x1))))))) -> c_2(0^#(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))), 0^#(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))), 0^#(1(2(3(4(5(x1))))))) , 0^#(1(2(3(4(5(1(x1))))))) -> c_3(0^#(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))))))), 0^#(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))), 0^#(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))), 0^#(1(2(3(4(5(x1))))))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { 0^#(1(2(3(4(5(1(x1))))))) -> c_1(0^#(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(x1))))))))))))))))))), 0^#(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))), 0^#(1(2(3(4(5(x1))))))) , 0^#(1(2(3(4(5(1(x1))))))) -> c_2(0^#(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))), 0^#(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))), 0^#(1(2(3(4(5(x1))))))) , 0^#(1(2(3(4(5(1(x1))))))) -> c_3(0^#(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))))))), 0^#(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))), 0^#(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))), 0^#(1(2(3(4(5(x1))))))) } Weak Trs: { 0(1(2(3(4(5(1(x1))))))) -> 0(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(x1))))))))))))))))))) , 0(1(2(3(4(5(1(x1))))))) -> 1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1))))))))))))))))))))))))) , 0(1(2(3(4(5(1(x1))))))) -> 1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1))))))))))))))))))))))))))))))) } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { 0^#(1(2(3(4(5(1(x1))))))) -> c_1(0^#(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(x1))))))))))))))))))), 0^#(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))), 0^#(1(2(3(4(5(x1))))))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { 0^#(1(2(3(4(5(1(x1))))))) -> c_1(0^#(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))), 0^#(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))), 0^#(1(2(3(4(5(x1))))))) , 0^#(1(2(3(4(5(1(x1))))))) -> c_2(0^#(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))))))), 0^#(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))), 0^#(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))), 0^#(1(2(3(4(5(x1))))))) , 0^#(1(2(3(4(5(1(x1))))))) -> c_3(0^#(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))), 0^#(1(2(3(4(5(x1))))))) } Weak Trs: { 0(1(2(3(4(5(1(x1))))))) -> 0(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(x1))))))))))))))))))) , 0(1(2(3(4(5(1(x1))))))) -> 1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1))))))))))))))))))))))))) , 0(1(2(3(4(5(1(x1))))))) -> 1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1))))))))))))))))))))))))))))))) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..