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