MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { nats() -> cons(0(), n__incr(nats())) , pairs() -> cons(0(), n__incr(odds())) , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(X) , head(cons(X, XS)) -> X , tail(cons(X, XS)) -> activate(XS) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: We add the following dependency tuples: Strict DPs: { nats^#() -> c_1(nats^#()) , pairs^#() -> c_2(odds^#()) , odds^#() -> c_3(incr^#(pairs()), pairs^#()) , incr^#(X) -> c_4() , incr^#(cons(X, XS)) -> c_5(activate^#(XS)) , activate^#(X) -> c_6() , activate^#(n__incr(X)) -> c_7(incr^#(X)) , head^#(cons(X, XS)) -> c_8() , tail^#(cons(X, XS)) -> c_9(activate^#(XS)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_1(nats^#()) , pairs^#() -> c_2(odds^#()) , odds^#() -> c_3(incr^#(pairs()), pairs^#()) , incr^#(X) -> c_4() , incr^#(cons(X, XS)) -> c_5(activate^#(XS)) , activate^#(X) -> c_6() , activate^#(n__incr(X)) -> c_7(incr^#(X)) , head^#(cons(X, XS)) -> c_8() , tail^#(cons(X, XS)) -> c_9(activate^#(XS)) } Weak Trs: { nats() -> cons(0(), n__incr(nats())) , pairs() -> cons(0(), n__incr(odds())) , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(X) , head(cons(X, XS)) -> X , tail(cons(X, XS)) -> activate(XS) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {4,6,8} by applications of Pre({4,6,8}) = {3,5,7,9}. Here rules are labeled as follows: DPs: { 1: nats^#() -> c_1(nats^#()) , 2: pairs^#() -> c_2(odds^#()) , 3: odds^#() -> c_3(incr^#(pairs()), pairs^#()) , 4: incr^#(X) -> c_4() , 5: incr^#(cons(X, XS)) -> c_5(activate^#(XS)) , 6: activate^#(X) -> c_6() , 7: activate^#(n__incr(X)) -> c_7(incr^#(X)) , 8: head^#(cons(X, XS)) -> c_8() , 9: tail^#(cons(X, XS)) -> c_9(activate^#(XS)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_1(nats^#()) , pairs^#() -> c_2(odds^#()) , odds^#() -> c_3(incr^#(pairs()), pairs^#()) , incr^#(cons(X, XS)) -> c_5(activate^#(XS)) , activate^#(n__incr(X)) -> c_7(incr^#(X)) , tail^#(cons(X, XS)) -> c_9(activate^#(XS)) } Weak DPs: { incr^#(X) -> c_4() , activate^#(X) -> c_6() , head^#(cons(X, XS)) -> c_8() } Weak Trs: { nats() -> cons(0(), n__incr(nats())) , pairs() -> cons(0(), n__incr(odds())) , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(X) , head(cons(X, XS)) -> X , tail(cons(X, XS)) -> activate(XS) } 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. { incr^#(X) -> c_4() , activate^#(X) -> c_6() , head^#(cons(X, XS)) -> c_8() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_1(nats^#()) , pairs^#() -> c_2(odds^#()) , odds^#() -> c_3(incr^#(pairs()), pairs^#()) , incr^#(cons(X, XS)) -> c_5(activate^#(XS)) , activate^#(n__incr(X)) -> c_7(incr^#(X)) , tail^#(cons(X, XS)) -> c_9(activate^#(XS)) } Weak Trs: { nats() -> cons(0(), n__incr(nats())) , pairs() -> cons(0(), n__incr(odds())) , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(X) , head(cons(X, XS)) -> X , tail(cons(X, XS)) -> activate(XS) } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: nats^#() -> c_1(nats^#()) -->_1 nats^#() -> c_1(nats^#()) :1 2: pairs^#() -> c_2(odds^#()) -->_1 odds^#() -> c_3(incr^#(pairs()), pairs^#()) :3 3: odds^#() -> c_3(incr^#(pairs()), pairs^#()) -->_1 incr^#(cons(X, XS)) -> c_5(activate^#(XS)) :4 -->_2 pairs^#() -> c_2(odds^#()) :2 4: incr^#(cons(X, XS)) -> c_5(activate^#(XS)) -->_1 activate^#(n__incr(X)) -> c_7(incr^#(X)) :5 5: activate^#(n__incr(X)) -> c_7(incr^#(X)) -->_1 incr^#(cons(X, XS)) -> c_5(activate^#(XS)) :4 6: tail^#(cons(X, XS)) -> c_9(activate^#(XS)) -->_1 activate^#(n__incr(X)) -> c_7(incr^#(X)) :5 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). { tail^#(cons(X, XS)) -> c_9(activate^#(XS)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_1(nats^#()) , pairs^#() -> c_2(odds^#()) , odds^#() -> c_3(incr^#(pairs()), pairs^#()) , incr^#(cons(X, XS)) -> c_5(activate^#(XS)) , activate^#(n__incr(X)) -> c_7(incr^#(X)) } Weak Trs: { nats() -> cons(0(), n__incr(nats())) , pairs() -> cons(0(), n__incr(odds())) , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(X) , head(cons(X, XS)) -> X , tail(cons(X, XS)) -> activate(XS) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { pairs() -> cons(0(), n__incr(odds())) , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(X) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_1(nats^#()) , pairs^#() -> c_2(odds^#()) , odds^#() -> c_3(incr^#(pairs()), pairs^#()) , incr^#(cons(X, XS)) -> c_5(activate^#(XS)) , activate^#(n__incr(X)) -> c_7(incr^#(X)) } Weak Trs: { pairs() -> cons(0(), n__incr(odds())) , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(X) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible 2) 'Fastest (timeout of 5 seconds)' failed due to the following reason: Computation stopped due to timeout after 5.0 seconds. 3) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(cons) = {2}, Uargs(n__incr) = {1}, Uargs(incr) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [nats] = [0] [cons](x1, x2) = [1] x1 + [1] x2 + [1] [0] = [7] [n__incr](x1) = [1] x1 + [7] [pairs] = [7] [odds] = [0] [incr](x1) = [1] x1 + [5] [s](x1) = [1] x1 + [7] [activate](x1) = [1] x1 + [0] [head](x1) = [1] x1 + [7] [tail](x1) = [1] x1 + [7] The following symbols are considered usable {nats, pairs, odds, incr, activate, head, tail} The order satisfies the following ordering constraints: [nats()] = [0] ? [15] = [cons(0(), n__incr(nats()))] [pairs()] = [7] ? [15] = [cons(0(), n__incr(odds()))] [odds()] = [0] ? [12] = [incr(pairs())] [incr(X)] = [1] X + [5] ? [1] X + [7] = [n__incr(X)] [incr(cons(X, XS))] = [1] X + [1] XS + [6] ? [1] X + [1] XS + [15] = [cons(s(X), n__incr(activate(XS)))] [activate(X)] = [1] X + [0] >= [1] X + [0] = [X] [activate(n__incr(X))] = [1] X + [7] > [1] X + [5] = [incr(X)] [head(cons(X, XS))] = [1] X + [1] XS + [8] > [1] X + [0] = [X] [tail(cons(X, XS))] = [1] X + [1] XS + [8] > [1] XS + [0] = [activate(XS)] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { nats() -> cons(0(), n__incr(nats())) , pairs() -> cons(0(), n__incr(odds())) , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X } Weak Trs: { activate(n__incr(X)) -> incr(X) , head(cons(X, XS)) -> X , tail(cons(X, XS)) -> activate(XS) } Obligation: innermost runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(cons) = {2}, Uargs(n__incr) = {1}, Uargs(incr) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [nats] = [0] [cons](x1, x2) = [1] x1 + [1] x2 + [0] [0] = [0] [n__incr](x1) = [1] x1 + [0] [pairs] = [0] [odds] = [0] [incr](x1) = [1] x1 + [0] [s](x1) = [1] x1 + [4] [activate](x1) = [1] x1 + [4] [head](x1) = [1] x1 + [7] [tail](x1) = [1] x1 + [7] The following symbols are considered usable {nats, pairs, odds, incr, activate, head, tail} The order satisfies the following ordering constraints: [nats()] = [0] >= [0] = [cons(0(), n__incr(nats()))] [pairs()] = [0] >= [0] = [cons(0(), n__incr(odds()))] [odds()] = [0] >= [0] = [incr(pairs())] [incr(X)] = [1] X + [0] >= [1] X + [0] = [n__incr(X)] [incr(cons(X, XS))] = [1] X + [1] XS + [0] ? [1] X + [1] XS + [8] = [cons(s(X), n__incr(activate(XS)))] [activate(X)] = [1] X + [4] > [1] X + [0] = [X] [activate(n__incr(X))] = [1] X + [4] > [1] X + [0] = [incr(X)] [head(cons(X, XS))] = [1] X + [1] XS + [7] > [1] X + [0] = [X] [tail(cons(X, XS))] = [1] X + [1] XS + [7] > [1] XS + [4] = [activate(XS)] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { nats() -> cons(0(), n__incr(nats())) , pairs() -> cons(0(), n__incr(odds())) , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) } Weak Trs: { activate(X) -> X , activate(n__incr(X)) -> incr(X) , head(cons(X, XS)) -> X , tail(cons(X, XS)) -> activate(XS) } Obligation: innermost runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(cons) = {2}, Uargs(n__incr) = {1}, Uargs(incr) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [nats] = [0] [cons](x1, x2) = [1] x1 + [1] x2 + [0] [0] = [0] [n__incr](x1) = [1] x1 + [0] [pairs] = [4] [odds] = [0] [incr](x1) = [1] x1 + [0] [s](x1) = [1] x1 + [4] [activate](x1) = [1] x1 + [4] [head](x1) = [1] x1 + [7] [tail](x1) = [1] x1 + [7] The following symbols are considered usable {nats, pairs, odds, incr, activate, head, tail} The order satisfies the following ordering constraints: [nats()] = [0] >= [0] = [cons(0(), n__incr(nats()))] [pairs()] = [4] > [0] = [cons(0(), n__incr(odds()))] [odds()] = [0] ? [4] = [incr(pairs())] [incr(X)] = [1] X + [0] >= [1] X + [0] = [n__incr(X)] [incr(cons(X, XS))] = [1] X + [1] XS + [0] ? [1] X + [1] XS + [8] = [cons(s(X), n__incr(activate(XS)))] [activate(X)] = [1] X + [4] > [1] X + [0] = [X] [activate(n__incr(X))] = [1] X + [4] > [1] X + [0] = [incr(X)] [head(cons(X, XS))] = [1] X + [1] XS + [7] > [1] X + [0] = [X] [tail(cons(X, XS))] = [1] X + [1] XS + [7] > [1] XS + [4] = [activate(XS)] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { nats() -> cons(0(), n__incr(nats())) , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) } Weak Trs: { pairs() -> cons(0(), n__incr(odds())) , activate(X) -> X , activate(n__incr(X)) -> incr(X) , head(cons(X, XS)) -> X , tail(cons(X, XS)) -> activate(XS) } Obligation: innermost runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(cons) = {2}, Uargs(n__incr) = {1}, Uargs(incr) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [nats] = [0] [cons](x1, x2) = [1] x1 + [1] x2 + [0] [0] = [0] [n__incr](x1) = [1] x1 + [0] [pairs] = [7] [odds] = [0] [incr](x1) = [1] x1 + [1] [s](x1) = [1] x1 + [0] [activate](x1) = [1] x1 + [4] [head](x1) = [1] x1 + [7] [tail](x1) = [1] x1 + [7] The following symbols are considered usable {nats, pairs, odds, incr, activate, head, tail} The order satisfies the following ordering constraints: [nats()] = [0] >= [0] = [cons(0(), n__incr(nats()))] [pairs()] = [7] > [0] = [cons(0(), n__incr(odds()))] [odds()] = [0] ? [8] = [incr(pairs())] [incr(X)] = [1] X + [1] > [1] X + [0] = [n__incr(X)] [incr(cons(X, XS))] = [1] X + [1] XS + [1] ? [1] X + [1] XS + [4] = [cons(s(X), n__incr(activate(XS)))] [activate(X)] = [1] X + [4] > [1] X + [0] = [X] [activate(n__incr(X))] = [1] X + [4] > [1] X + [1] = [incr(X)] [head(cons(X, XS))] = [1] X + [1] XS + [7] > [1] X + [0] = [X] [tail(cons(X, XS))] = [1] X + [1] XS + [7] > [1] XS + [4] = [activate(XS)] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { nats() -> cons(0(), n__incr(nats())) , odds() -> incr(pairs()) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) } Weak Trs: { pairs() -> cons(0(), n__incr(odds())) , incr(X) -> n__incr(X) , activate(X) -> X , activate(n__incr(X)) -> incr(X) , head(cons(X, XS)) -> X , tail(cons(X, XS)) -> activate(XS) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 5.0 seconds. 3) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible Arrrr..