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