MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { function(iszero(), 0(), dummy, dummy2) -> true() , function(iszero(), s(x), dummy, dummy2) -> false() , function(p(), 0(), dummy, dummy2) -> 0() , function(p(), s(0()), dummy, dummy2) -> 0() , function(p(), s(s(x)), dummy, dummy2) -> s(function(p(), s(x), x, x)) , function(plus(), dummy, x, y) -> function(if(), function(iszero(), x, x, x), x, y) , function(if(), true(), x, y) -> y , function(if(), false(), x, y) -> function(plus(), function(third(), x, y, y), function(p(), x, x, y), s(y)) , function(third(), x, y, z) -> z } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 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: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { function^#(iszero(), 0(), dummy, dummy2) -> c_1() , function^#(iszero(), s(x), dummy, dummy2) -> c_2() , function^#(p(), 0(), dummy, dummy2) -> c_3() , function^#(p(), s(0()), dummy, dummy2) -> c_4() , function^#(p(), s(s(x)), dummy, dummy2) -> c_5(function^#(p(), s(x), x, x)) , function^#(plus(), dummy, x, y) -> c_6(function^#(if(), function(iszero(), x, x, x), x, y)) , function^#(if(), true(), x, y) -> c_7(y) , function^#(if(), false(), x, y) -> c_8(function^#(plus(), function(third(), x, y, y), function(p(), x, x, y), s(y))) , function^#(third(), x, y, z) -> c_9(z) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { function^#(iszero(), 0(), dummy, dummy2) -> c_1() , function^#(iszero(), s(x), dummy, dummy2) -> c_2() , function^#(p(), 0(), dummy, dummy2) -> c_3() , function^#(p(), s(0()), dummy, dummy2) -> c_4() , function^#(p(), s(s(x)), dummy, dummy2) -> c_5(function^#(p(), s(x), x, x)) , function^#(plus(), dummy, x, y) -> c_6(function^#(if(), function(iszero(), x, x, x), x, y)) , function^#(if(), true(), x, y) -> c_7(y) , function^#(if(), false(), x, y) -> c_8(function^#(plus(), function(third(), x, y, y), function(p(), x, x, y), s(y))) , function^#(third(), x, y, z) -> c_9(z) } Strict Trs: { function(iszero(), 0(), dummy, dummy2) -> true() , function(iszero(), s(x), dummy, dummy2) -> false() , function(p(), 0(), dummy, dummy2) -> 0() , function(p(), s(0()), dummy, dummy2) -> 0() , function(p(), s(s(x)), dummy, dummy2) -> s(function(p(), s(x), x, x)) , function(plus(), dummy, x, y) -> function(if(), function(iszero(), x, x, x), x, y) , function(if(), true(), x, y) -> y , function(if(), false(), x, y) -> function(plus(), function(third(), x, y, y), function(p(), x, x, y), s(y)) , function(third(), x, y, z) -> z } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,4} by applications of Pre({1,2,3,4}) = {5,7,9}. Here rules are labeled as follows: DPs: { 1: function^#(iszero(), 0(), dummy, dummy2) -> c_1() , 2: function^#(iszero(), s(x), dummy, dummy2) -> c_2() , 3: function^#(p(), 0(), dummy, dummy2) -> c_3() , 4: function^#(p(), s(0()), dummy, dummy2) -> c_4() , 5: function^#(p(), s(s(x)), dummy, dummy2) -> c_5(function^#(p(), s(x), x, x)) , 6: function^#(plus(), dummy, x, y) -> c_6(function^#(if(), function(iszero(), x, x, x), x, y)) , 7: function^#(if(), true(), x, y) -> c_7(y) , 8: function^#(if(), false(), x, y) -> c_8(function^#(plus(), function(third(), x, y, y), function(p(), x, x, y), s(y))) , 9: function^#(third(), x, y, z) -> c_9(z) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { function^#(p(), s(s(x)), dummy, dummy2) -> c_5(function^#(p(), s(x), x, x)) , function^#(plus(), dummy, x, y) -> c_6(function^#(if(), function(iszero(), x, x, x), x, y)) , function^#(if(), true(), x, y) -> c_7(y) , function^#(if(), false(), x, y) -> c_8(function^#(plus(), function(third(), x, y, y), function(p(), x, x, y), s(y))) , function^#(third(), x, y, z) -> c_9(z) } Strict Trs: { function(iszero(), 0(), dummy, dummy2) -> true() , function(iszero(), s(x), dummy, dummy2) -> false() , function(p(), 0(), dummy, dummy2) -> 0() , function(p(), s(0()), dummy, dummy2) -> 0() , function(p(), s(s(x)), dummy, dummy2) -> s(function(p(), s(x), x, x)) , function(plus(), dummy, x, y) -> function(if(), function(iszero(), x, x, x), x, y) , function(if(), true(), x, y) -> y , function(if(), false(), x, y) -> function(plus(), function(third(), x, y, y), function(p(), x, x, y), s(y)) , function(third(), x, y, z) -> z } Weak DPs: { function^#(iszero(), 0(), dummy, dummy2) -> c_1() , function^#(iszero(), s(x), dummy, dummy2) -> c_2() , function^#(p(), 0(), dummy, dummy2) -> c_3() , function^#(p(), s(0()), dummy, dummy2) -> c_4() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..