MAYBE
867.41/297.23	MAYBE
867.41/297.23	
867.41/297.23	We are left with following problem, upon which TcT provides the
867.41/297.23	certificate MAYBE.
867.41/297.23	
867.41/297.23	Strict Trs:
867.41/297.23	  { minus(X1, X2) -> n__minus(X1, X2)
867.41/297.23	  , minus(n__0(), Y) -> 0()
867.41/297.23	  , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y))
867.41/297.23	  , 0() -> n__0()
867.41/297.23	  , activate(X) -> X
867.41/297.23	  , activate(n__0()) -> 0()
867.41/297.23	  , activate(n__s(X)) -> s(activate(X))
867.41/297.23	  , activate(n__div(X1, X2)) -> div(activate(X1), X2)
867.41/297.23	  , activate(n__minus(X1, X2)) -> minus(X1, X2)
867.41/297.23	  , geq(X, n__0()) -> true()
867.41/297.23	  , geq(n__0(), n__s(Y)) -> false()
867.41/297.23	  , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y))
867.41/297.23	  , div(X1, X2) -> n__div(X1, X2)
867.41/297.23	  , div(0(), n__s(Y)) -> 0()
867.41/297.23	  , div(s(X), n__s(Y)) ->
867.41/297.23	    if(geq(X, activate(Y)),
867.41/297.23	       n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))),
867.41/297.23	       n__0())
867.41/297.23	  , s(X) -> n__s(X)
867.41/297.23	  , if(true(), X, Y) -> activate(X)
867.41/297.23	  , if(false(), X, Y) -> activate(Y) }
867.41/297.23	Obligation:
867.41/297.23	  runtime complexity
867.41/297.23	Answer:
867.41/297.23	  MAYBE
867.41/297.23	
867.41/297.23	None of the processors succeeded.
867.41/297.23	
867.41/297.23	Details of failed attempt(s):
867.41/297.23	-----------------------------
867.41/297.23	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
867.41/297.23	   following reason:
867.41/297.23	   
867.41/297.23	   Computation stopped due to timeout after 297.0 seconds.
867.41/297.23	
867.41/297.23	2) 'Best' failed due to the following reason:
867.41/297.23	   
867.41/297.23	   None of the processors succeeded.
867.41/297.23	   
867.41/297.23	   Details of failed attempt(s):
867.41/297.23	   -----------------------------
867.41/297.23	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
867.41/297.23	      seconds)' failed due to the following reason:
867.41/297.23	      
867.41/297.23	      Computation stopped due to timeout after 148.0 seconds.
867.41/297.23	   
867.41/297.23	   2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
867.41/297.23	      failed due to the following reason:
867.41/297.23	      
867.41/297.23	      None of the processors succeeded.
867.41/297.23	      
867.41/297.23	      Details of failed attempt(s):
867.41/297.23	      -----------------------------
867.41/297.23	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
867.41/297.23	         failed due to the following reason:
867.41/297.23	         
867.41/297.23	         match-boundness of the problem could not be verified.
867.41/297.23	      
867.41/297.23	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
867.41/297.23	         failed due to the following reason:
867.41/297.23	         
867.41/297.23	         match-boundness of the problem could not be verified.
867.41/297.23	      
867.41/297.23	   
867.41/297.23	   3) 'Best' failed due to the following reason:
867.41/297.23	      
867.41/297.23	      None of the processors succeeded.
867.41/297.23	      
867.41/297.23	      Details of failed attempt(s):
867.41/297.23	      -----------------------------
867.41/297.23	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
867.41/297.23	         following reason:
867.41/297.23	         
867.41/297.23	         The processor is inapplicable, reason:
867.41/297.23	           Processor only applicable for innermost runtime complexity analysis
867.41/297.23	      
867.41/297.23	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
867.41/297.23	         to the following reason:
867.41/297.23	         
867.41/297.23	         The processor is inapplicable, reason:
867.41/297.23	           Processor only applicable for innermost runtime complexity analysis
867.41/297.23	      
867.41/297.23	   
867.41/297.23	
867.41/297.23	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
867.41/297.23	   the following reason:
867.41/297.23	   
867.41/297.23	   We add the following weak dependency pairs:
867.41/297.23	   
867.41/297.23	   Strict DPs:
867.41/297.23	     { minus^#(X1, X2) -> c_1(X1, X2)
867.41/297.23	     , minus^#(n__0(), Y) -> c_2(0^#())
867.41/297.23	     , minus^#(n__s(X), n__s(Y)) ->
867.41/297.24	       c_3(minus^#(activate(X), activate(Y)))
867.41/297.24	     , 0^#() -> c_4()
867.41/297.24	     , activate^#(X) -> c_5(X)
867.41/297.24	     , activate^#(n__0()) -> c_6(0^#())
867.41/297.24	     , activate^#(n__s(X)) -> c_7(s^#(activate(X)))
867.41/297.24	     , activate^#(n__div(X1, X2)) -> c_8(div^#(activate(X1), X2))
867.41/297.24	     , activate^#(n__minus(X1, X2)) -> c_9(minus^#(X1, X2))
867.41/297.24	     , s^#(X) -> c_16(X)
867.41/297.24	     , div^#(X1, X2) -> c_13(X1, X2)
867.41/297.24	     , div^#(0(), n__s(Y)) -> c_14(0^#())
867.41/297.24	     , div^#(s(X), n__s(Y)) ->
867.41/297.24	       c_15(if^#(geq(X, activate(Y)),
867.41/297.24	                 n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))),
867.41/297.24	                 n__0()))
867.41/297.24	     , geq^#(X, n__0()) -> c_10()
867.41/297.24	     , geq^#(n__0(), n__s(Y)) -> c_11()
867.41/297.24	     , geq^#(n__s(X), n__s(Y)) -> c_12(geq^#(activate(X), activate(Y)))
867.41/297.24	     , if^#(true(), X, Y) -> c_17(activate^#(X))
867.41/297.24	     , if^#(false(), X, Y) -> c_18(activate^#(Y)) }
867.41/297.24	   
867.41/297.24	   and mark the set of starting terms.
867.41/297.24	   
867.41/297.24	   We are left with following problem, upon which TcT provides the
867.41/297.24	   certificate MAYBE.
867.41/297.24	   
867.41/297.24	   Strict DPs:
867.41/297.24	     { minus^#(X1, X2) -> c_1(X1, X2)
867.41/297.24	     , minus^#(n__0(), Y) -> c_2(0^#())
867.41/297.24	     , minus^#(n__s(X), n__s(Y)) ->
867.41/297.24	       c_3(minus^#(activate(X), activate(Y)))
867.41/297.24	     , 0^#() -> c_4()
867.41/297.24	     , activate^#(X) -> c_5(X)
867.41/297.24	     , activate^#(n__0()) -> c_6(0^#())
867.41/297.24	     , activate^#(n__s(X)) -> c_7(s^#(activate(X)))
867.41/297.24	     , activate^#(n__div(X1, X2)) -> c_8(div^#(activate(X1), X2))
867.41/297.24	     , activate^#(n__minus(X1, X2)) -> c_9(minus^#(X1, X2))
867.41/297.24	     , s^#(X) -> c_16(X)
867.41/297.24	     , div^#(X1, X2) -> c_13(X1, X2)
867.41/297.24	     , div^#(0(), n__s(Y)) -> c_14(0^#())
867.41/297.24	     , div^#(s(X), n__s(Y)) ->
867.41/297.24	       c_15(if^#(geq(X, activate(Y)),
867.41/297.24	                 n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))),
867.41/297.24	                 n__0()))
867.41/297.24	     , geq^#(X, n__0()) -> c_10()
867.41/297.24	     , geq^#(n__0(), n__s(Y)) -> c_11()
867.41/297.24	     , geq^#(n__s(X), n__s(Y)) -> c_12(geq^#(activate(X), activate(Y)))
867.41/297.24	     , if^#(true(), X, Y) -> c_17(activate^#(X))
867.41/297.24	     , if^#(false(), X, Y) -> c_18(activate^#(Y)) }
867.41/297.24	   Strict Trs:
867.41/297.24	     { minus(X1, X2) -> n__minus(X1, X2)
867.41/297.24	     , minus(n__0(), Y) -> 0()
867.41/297.24	     , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y))
867.41/297.24	     , 0() -> n__0()
867.41/297.24	     , activate(X) -> X
867.41/297.24	     , activate(n__0()) -> 0()
867.41/297.24	     , activate(n__s(X)) -> s(activate(X))
867.41/297.24	     , activate(n__div(X1, X2)) -> div(activate(X1), X2)
867.41/297.24	     , activate(n__minus(X1, X2)) -> minus(X1, X2)
867.41/297.24	     , geq(X, n__0()) -> true()
867.41/297.24	     , geq(n__0(), n__s(Y)) -> false()
867.41/297.24	     , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y))
867.41/297.24	     , div(X1, X2) -> n__div(X1, X2)
867.41/297.24	     , div(0(), n__s(Y)) -> 0()
867.41/297.24	     , div(s(X), n__s(Y)) ->
867.41/297.24	       if(geq(X, activate(Y)),
867.41/297.24	          n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))),
867.41/297.24	          n__0())
867.41/297.24	     , s(X) -> n__s(X)
867.41/297.24	     , if(true(), X, Y) -> activate(X)
867.41/297.24	     , if(false(), X, Y) -> activate(Y) }
867.41/297.24	   Obligation:
867.41/297.24	     runtime complexity
867.41/297.24	   Answer:
867.41/297.24	     MAYBE
867.41/297.24	   
867.41/297.24	   We estimate the number of application of {4,14,15} by applications
867.41/297.24	   of Pre({4,14,15}) = {1,2,5,6,10,11,12,16}. Here rules are labeled
867.41/297.24	   as follows:
867.41/297.24	   
867.41/297.24	     DPs:
867.41/297.24	       { 1: minus^#(X1, X2) -> c_1(X1, X2)
867.41/297.24	       , 2: minus^#(n__0(), Y) -> c_2(0^#())
867.41/297.24	       , 3: minus^#(n__s(X), n__s(Y)) ->
867.41/297.24	            c_3(minus^#(activate(X), activate(Y)))
867.41/297.24	       , 4: 0^#() -> c_4()
867.41/297.24	       , 5: activate^#(X) -> c_5(X)
867.41/297.24	       , 6: activate^#(n__0()) -> c_6(0^#())
867.41/297.24	       , 7: activate^#(n__s(X)) -> c_7(s^#(activate(X)))
867.41/297.24	       , 8: activate^#(n__div(X1, X2)) -> c_8(div^#(activate(X1), X2))
867.41/297.24	       , 9: activate^#(n__minus(X1, X2)) -> c_9(minus^#(X1, X2))
867.41/297.24	       , 10: s^#(X) -> c_16(X)
867.41/297.24	       , 11: div^#(X1, X2) -> c_13(X1, X2)
867.41/297.24	       , 12: div^#(0(), n__s(Y)) -> c_14(0^#())
867.41/297.24	       , 13: div^#(s(X), n__s(Y)) ->
867.41/297.24	             c_15(if^#(geq(X, activate(Y)),
867.41/297.24	                       n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))),
867.41/297.24	                       n__0()))
867.41/297.24	       , 14: geq^#(X, n__0()) -> c_10()
867.41/297.24	       , 15: geq^#(n__0(), n__s(Y)) -> c_11()
867.41/297.24	       , 16: geq^#(n__s(X), n__s(Y)) ->
867.41/297.24	             c_12(geq^#(activate(X), activate(Y)))
867.41/297.24	       , 17: if^#(true(), X, Y) -> c_17(activate^#(X))
867.41/297.24	       , 18: if^#(false(), X, Y) -> c_18(activate^#(Y)) }
867.41/297.24	   
867.41/297.24	   We are left with following problem, upon which TcT provides the
867.41/297.24	   certificate MAYBE.
867.41/297.24	   
867.41/297.24	   Strict DPs:
867.41/297.24	     { minus^#(X1, X2) -> c_1(X1, X2)
867.41/297.24	     , minus^#(n__0(), Y) -> c_2(0^#())
867.41/297.24	     , minus^#(n__s(X), n__s(Y)) ->
867.41/297.24	       c_3(minus^#(activate(X), activate(Y)))
867.41/297.24	     , activate^#(X) -> c_5(X)
867.41/297.24	     , activate^#(n__0()) -> c_6(0^#())
867.41/297.24	     , activate^#(n__s(X)) -> c_7(s^#(activate(X)))
867.41/297.24	     , activate^#(n__div(X1, X2)) -> c_8(div^#(activate(X1), X2))
867.41/297.24	     , activate^#(n__minus(X1, X2)) -> c_9(minus^#(X1, X2))
867.41/297.24	     , s^#(X) -> c_16(X)
867.41/297.24	     , div^#(X1, X2) -> c_13(X1, X2)
867.41/297.24	     , div^#(0(), n__s(Y)) -> c_14(0^#())
867.41/297.24	     , div^#(s(X), n__s(Y)) ->
867.41/297.24	       c_15(if^#(geq(X, activate(Y)),
867.41/297.24	                 n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))),
867.41/297.24	                 n__0()))
867.41/297.24	     , geq^#(n__s(X), n__s(Y)) -> c_12(geq^#(activate(X), activate(Y)))
867.41/297.24	     , if^#(true(), X, Y) -> c_17(activate^#(X))
867.41/297.24	     , if^#(false(), X, Y) -> c_18(activate^#(Y)) }
867.41/297.24	   Strict Trs:
867.41/297.24	     { minus(X1, X2) -> n__minus(X1, X2)
867.41/297.24	     , minus(n__0(), Y) -> 0()
867.41/297.24	     , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y))
867.41/297.24	     , 0() -> n__0()
867.41/297.24	     , activate(X) -> X
867.41/297.24	     , activate(n__0()) -> 0()
867.41/297.24	     , activate(n__s(X)) -> s(activate(X))
867.41/297.24	     , activate(n__div(X1, X2)) -> div(activate(X1), X2)
867.41/297.24	     , activate(n__minus(X1, X2)) -> minus(X1, X2)
867.41/297.24	     , geq(X, n__0()) -> true()
867.41/297.24	     , geq(n__0(), n__s(Y)) -> false()
867.41/297.24	     , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y))
867.41/297.24	     , div(X1, X2) -> n__div(X1, X2)
867.41/297.24	     , div(0(), n__s(Y)) -> 0()
867.41/297.24	     , div(s(X), n__s(Y)) ->
867.41/297.24	       if(geq(X, activate(Y)),
867.41/297.24	          n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))),
867.41/297.24	          n__0())
867.41/297.24	     , s(X) -> n__s(X)
867.41/297.24	     , if(true(), X, Y) -> activate(X)
867.41/297.24	     , if(false(), X, Y) -> activate(Y) }
867.41/297.24	   Weak DPs:
867.41/297.24	     { 0^#() -> c_4()
867.41/297.24	     , geq^#(X, n__0()) -> c_10()
867.41/297.24	     , geq^#(n__0(), n__s(Y)) -> c_11() }
867.41/297.24	   Obligation:
867.41/297.24	     runtime complexity
867.41/297.24	   Answer:
867.41/297.24	     MAYBE
867.41/297.24	   
867.41/297.24	   We estimate the number of application of {2,5,11} by applications
867.41/297.24	   of Pre({2,5,11}) = {1,3,4,7,8,9,10,14,15}. Here rules are labeled
867.41/297.24	   as follows:
867.41/297.24	   
867.41/297.24	     DPs:
867.41/297.24	       { 1: minus^#(X1, X2) -> c_1(X1, X2)
867.41/297.24	       , 2: minus^#(n__0(), Y) -> c_2(0^#())
867.41/297.24	       , 3: minus^#(n__s(X), n__s(Y)) ->
867.41/297.24	            c_3(minus^#(activate(X), activate(Y)))
867.41/297.24	       , 4: activate^#(X) -> c_5(X)
867.41/297.24	       , 5: activate^#(n__0()) -> c_6(0^#())
867.41/297.24	       , 6: activate^#(n__s(X)) -> c_7(s^#(activate(X)))
867.41/297.24	       , 7: activate^#(n__div(X1, X2)) -> c_8(div^#(activate(X1), X2))
867.41/297.24	       , 8: activate^#(n__minus(X1, X2)) -> c_9(minus^#(X1, X2))
867.41/297.24	       , 9: s^#(X) -> c_16(X)
867.41/297.24	       , 10: div^#(X1, X2) -> c_13(X1, X2)
867.41/297.24	       , 11: div^#(0(), n__s(Y)) -> c_14(0^#())
867.41/297.24	       , 12: div^#(s(X), n__s(Y)) ->
867.41/297.24	             c_15(if^#(geq(X, activate(Y)),
867.41/297.24	                       n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))),
867.41/297.24	                       n__0()))
867.41/297.24	       , 13: geq^#(n__s(X), n__s(Y)) ->
867.41/297.24	             c_12(geq^#(activate(X), activate(Y)))
867.41/297.24	       , 14: if^#(true(), X, Y) -> c_17(activate^#(X))
867.41/297.24	       , 15: if^#(false(), X, Y) -> c_18(activate^#(Y))
867.41/297.24	       , 16: 0^#() -> c_4()
867.41/297.24	       , 17: geq^#(X, n__0()) -> c_10()
867.41/297.24	       , 18: geq^#(n__0(), n__s(Y)) -> c_11() }
867.41/297.24	   
867.41/297.24	   We are left with following problem, upon which TcT provides the
867.41/297.24	   certificate MAYBE.
867.41/297.24	   
867.41/297.24	   Strict DPs:
867.41/297.24	     { minus^#(X1, X2) -> c_1(X1, X2)
867.41/297.24	     , minus^#(n__s(X), n__s(Y)) ->
867.41/297.24	       c_3(minus^#(activate(X), activate(Y)))
867.41/297.24	     , activate^#(X) -> c_5(X)
867.41/297.24	     , activate^#(n__s(X)) -> c_7(s^#(activate(X)))
867.41/297.24	     , activate^#(n__div(X1, X2)) -> c_8(div^#(activate(X1), X2))
867.41/297.24	     , activate^#(n__minus(X1, X2)) -> c_9(minus^#(X1, X2))
867.41/297.24	     , s^#(X) -> c_16(X)
867.41/297.24	     , div^#(X1, X2) -> c_13(X1, X2)
867.41/297.24	     , div^#(s(X), n__s(Y)) ->
867.41/297.24	       c_15(if^#(geq(X, activate(Y)),
867.41/297.24	                 n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))),
867.41/297.24	                 n__0()))
867.41/297.24	     , geq^#(n__s(X), n__s(Y)) -> c_12(geq^#(activate(X), activate(Y)))
867.41/297.24	     , if^#(true(), X, Y) -> c_17(activate^#(X))
867.41/297.24	     , if^#(false(), X, Y) -> c_18(activate^#(Y)) }
867.41/297.24	   Strict Trs:
867.41/297.24	     { minus(X1, X2) -> n__minus(X1, X2)
867.41/297.24	     , minus(n__0(), Y) -> 0()
867.41/297.24	     , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y))
867.41/297.24	     , 0() -> n__0()
867.41/297.24	     , activate(X) -> X
867.41/297.24	     , activate(n__0()) -> 0()
867.41/297.24	     , activate(n__s(X)) -> s(activate(X))
867.41/297.24	     , activate(n__div(X1, X2)) -> div(activate(X1), X2)
867.41/297.24	     , activate(n__minus(X1, X2)) -> minus(X1, X2)
867.41/297.24	     , geq(X, n__0()) -> true()
867.41/297.24	     , geq(n__0(), n__s(Y)) -> false()
867.41/297.24	     , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y))
867.41/297.24	     , div(X1, X2) -> n__div(X1, X2)
867.41/297.24	     , div(0(), n__s(Y)) -> 0()
867.41/297.24	     , div(s(X), n__s(Y)) ->
867.41/297.24	       if(geq(X, activate(Y)),
867.41/297.24	          n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))),
867.41/297.24	          n__0())
867.41/297.24	     , s(X) -> n__s(X)
867.41/297.24	     , if(true(), X, Y) -> activate(X)
867.41/297.24	     , if(false(), X, Y) -> activate(Y) }
867.41/297.24	   Weak DPs:
867.41/297.24	     { minus^#(n__0(), Y) -> c_2(0^#())
867.41/297.24	     , 0^#() -> c_4()
867.41/297.24	     , activate^#(n__0()) -> c_6(0^#())
867.41/297.24	     , div^#(0(), n__s(Y)) -> c_14(0^#())
867.41/297.24	     , geq^#(X, n__0()) -> c_10()
867.41/297.24	     , geq^#(n__0(), n__s(Y)) -> c_11() }
867.41/297.24	   Obligation:
867.41/297.24	     runtime complexity
867.41/297.24	   Answer:
867.41/297.24	     MAYBE
867.41/297.24	   
867.41/297.24	   Empty strict component of the problem is NOT empty.
867.41/297.24	
867.41/297.24	
867.41/297.24	Arrrr..
867.71/297.43	EOF