MAYBE
752.73/297.04	MAYBE
752.73/297.04	
752.73/297.04	We are left with following problem, upon which TcT provides the
752.73/297.04	certificate MAYBE.
752.73/297.04	
752.73/297.04	Strict Trs:
752.73/297.04	  { isLeaf(leaf()) -> true()
752.73/297.04	  , isLeaf(cons(u, v)) -> false()
752.73/297.04	  , left(cons(u, v)) -> u
752.73/297.04	  , right(cons(u, v)) -> v
752.73/297.04	  , concat(leaf(), y) -> y
752.73/297.04	  , concat(cons(u, v), y) -> cons(u, concat(v, y))
752.73/297.04	  , less_leaves(u, v) -> if1(isLeaf(u), isLeaf(v), u, v)
752.73/297.04	  , if1(b, true(), u, v) -> false()
752.73/297.04	  , if1(b, false(), u, v) -> if2(b, u, v)
752.73/297.04	  , if2(true(), u, v) -> true()
752.73/297.04	  , if2(false(), u, v) ->
752.73/297.04	    less_leaves(concat(left(u), right(u)), concat(left(v), right(v))) }
752.73/297.04	Obligation:
752.73/297.04	  runtime complexity
752.73/297.04	Answer:
752.73/297.04	  MAYBE
752.73/297.04	
752.73/297.04	None of the processors succeeded.
752.73/297.04	
752.73/297.04	Details of failed attempt(s):
752.73/297.04	-----------------------------
752.73/297.04	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
752.73/297.04	   following reason:
752.73/297.04	   
752.73/297.04	   Computation stopped due to timeout after 297.0 seconds.
752.73/297.04	
752.73/297.04	2) 'Best' failed due to the following reason:
752.73/297.04	   
752.73/297.04	   None of the processors succeeded.
752.73/297.04	   
752.73/297.04	   Details of failed attempt(s):
752.73/297.04	   -----------------------------
752.73/297.04	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
752.73/297.04	      seconds)' failed due to the following reason:
752.73/297.04	      
752.73/297.04	      Computation stopped due to timeout after 148.0 seconds.
752.73/297.04	   
752.73/297.04	   2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
752.73/297.04	      failed due to the following reason:
752.73/297.04	      
752.73/297.04	      None of the processors succeeded.
752.73/297.04	      
752.73/297.04	      Details of failed attempt(s):
752.73/297.04	      -----------------------------
752.73/297.04	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
752.73/297.04	         failed due to the following reason:
752.73/297.04	         
752.73/297.04	         match-boundness of the problem could not be verified.
752.73/297.04	      
752.73/297.04	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
752.73/297.04	         failed due to the following reason:
752.73/297.04	         
752.73/297.04	         match-boundness of the problem could not be verified.
752.73/297.04	      
752.73/297.04	   
752.73/297.04	   3) 'Best' failed due to the following reason:
752.73/297.04	      
752.73/297.04	      None of the processors succeeded.
752.73/297.04	      
752.73/297.04	      Details of failed attempt(s):
752.73/297.04	      -----------------------------
752.73/297.04	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
752.73/297.04	         following reason:
752.73/297.04	         
752.73/297.04	         The processor is inapplicable, reason:
752.73/297.04	           Processor only applicable for innermost runtime complexity analysis
752.73/297.04	      
752.73/297.04	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
752.73/297.04	         to the following reason:
752.73/297.04	         
752.73/297.04	         The processor is inapplicable, reason:
752.73/297.04	           Processor only applicable for innermost runtime complexity analysis
752.73/297.04	      
752.73/297.04	   
752.73/297.04	
752.73/297.04	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
752.73/297.04	   the following reason:
752.73/297.04	   
752.73/297.04	   We add the following weak dependency pairs:
752.73/297.04	   
752.73/297.04	   Strict DPs:
752.73/297.04	     { isLeaf^#(leaf()) -> c_1()
752.73/297.04	     , isLeaf^#(cons(u, v)) -> c_2()
752.73/297.04	     , left^#(cons(u, v)) -> c_3(u)
752.73/297.04	     , right^#(cons(u, v)) -> c_4(v)
752.73/297.04	     , concat^#(leaf(), y) -> c_5(y)
752.73/297.04	     , concat^#(cons(u, v), y) -> c_6(u, concat^#(v, y))
752.73/297.04	     , less_leaves^#(u, v) -> c_7(if1^#(isLeaf(u), isLeaf(v), u, v))
752.73/297.04	     , if1^#(b, true(), u, v) -> c_8()
752.73/297.04	     , if1^#(b, false(), u, v) -> c_9(if2^#(b, u, v))
752.73/297.04	     , if2^#(true(), u, v) -> c_10()
752.73/297.04	     , if2^#(false(), u, v) ->
752.73/297.04	       c_11(less_leaves^#(concat(left(u), right(u)),
752.73/297.04	                          concat(left(v), right(v)))) }
752.73/297.04	   
752.73/297.04	   and mark the set of starting terms.
752.73/297.04	   
752.73/297.04	   We are left with following problem, upon which TcT provides the
752.73/297.04	   certificate MAYBE.
752.73/297.04	   
752.73/297.04	   Strict DPs:
752.73/297.04	     { isLeaf^#(leaf()) -> c_1()
752.73/297.04	     , isLeaf^#(cons(u, v)) -> c_2()
752.73/297.04	     , left^#(cons(u, v)) -> c_3(u)
752.73/297.04	     , right^#(cons(u, v)) -> c_4(v)
752.73/297.04	     , concat^#(leaf(), y) -> c_5(y)
752.73/297.04	     , concat^#(cons(u, v), y) -> c_6(u, concat^#(v, y))
752.73/297.04	     , less_leaves^#(u, v) -> c_7(if1^#(isLeaf(u), isLeaf(v), u, v))
752.73/297.04	     , if1^#(b, true(), u, v) -> c_8()
752.73/297.04	     , if1^#(b, false(), u, v) -> c_9(if2^#(b, u, v))
752.73/297.04	     , if2^#(true(), u, v) -> c_10()
752.73/297.04	     , if2^#(false(), u, v) ->
752.73/297.04	       c_11(less_leaves^#(concat(left(u), right(u)),
752.73/297.04	                          concat(left(v), right(v)))) }
752.73/297.04	   Strict Trs:
752.73/297.04	     { isLeaf(leaf()) -> true()
752.73/297.04	     , isLeaf(cons(u, v)) -> false()
752.73/297.04	     , left(cons(u, v)) -> u
752.73/297.04	     , right(cons(u, v)) -> v
752.73/297.04	     , concat(leaf(), y) -> y
752.73/297.04	     , concat(cons(u, v), y) -> cons(u, concat(v, y))
752.73/297.04	     , less_leaves(u, v) -> if1(isLeaf(u), isLeaf(v), u, v)
752.73/297.04	     , if1(b, true(), u, v) -> false()
752.73/297.04	     , if1(b, false(), u, v) -> if2(b, u, v)
752.73/297.04	     , if2(true(), u, v) -> true()
752.73/297.04	     , if2(false(), u, v) ->
752.73/297.04	       less_leaves(concat(left(u), right(u)), concat(left(v), right(v))) }
752.73/297.04	   Obligation:
752.73/297.04	     runtime complexity
752.73/297.04	   Answer:
752.73/297.04	     MAYBE
752.73/297.04	   
752.73/297.04	   We estimate the number of application of {1,2,8,10} by applications
752.73/297.04	   of Pre({1,2,8,10}) = {3,4,5,6,7,9}. Here rules are labeled as
752.73/297.04	   follows:
752.73/297.04	   
752.73/297.04	     DPs:
752.73/297.04	       { 1: isLeaf^#(leaf()) -> c_1()
752.73/297.04	       , 2: isLeaf^#(cons(u, v)) -> c_2()
752.73/297.04	       , 3: left^#(cons(u, v)) -> c_3(u)
752.73/297.04	       , 4: right^#(cons(u, v)) -> c_4(v)
752.73/297.04	       , 5: concat^#(leaf(), y) -> c_5(y)
752.73/297.04	       , 6: concat^#(cons(u, v), y) -> c_6(u, concat^#(v, y))
752.73/297.04	       , 7: less_leaves^#(u, v) -> c_7(if1^#(isLeaf(u), isLeaf(v), u, v))
752.73/297.04	       , 8: if1^#(b, true(), u, v) -> c_8()
752.73/297.04	       , 9: if1^#(b, false(), u, v) -> c_9(if2^#(b, u, v))
752.73/297.04	       , 10: if2^#(true(), u, v) -> c_10()
752.73/297.04	       , 11: if2^#(false(), u, v) ->
752.73/297.04	             c_11(less_leaves^#(concat(left(u), right(u)),
752.73/297.04	                                concat(left(v), right(v)))) }
752.73/297.04	   
752.73/297.04	   We are left with following problem, upon which TcT provides the
752.73/297.04	   certificate MAYBE.
752.73/297.04	   
752.73/297.04	   Strict DPs:
752.73/297.04	     { left^#(cons(u, v)) -> c_3(u)
752.73/297.04	     , right^#(cons(u, v)) -> c_4(v)
752.73/297.04	     , concat^#(leaf(), y) -> c_5(y)
752.73/297.04	     , concat^#(cons(u, v), y) -> c_6(u, concat^#(v, y))
752.73/297.04	     , less_leaves^#(u, v) -> c_7(if1^#(isLeaf(u), isLeaf(v), u, v))
752.73/297.04	     , if1^#(b, false(), u, v) -> c_9(if2^#(b, u, v))
752.73/297.04	     , if2^#(false(), u, v) ->
752.73/297.04	       c_11(less_leaves^#(concat(left(u), right(u)),
752.73/297.04	                          concat(left(v), right(v)))) }
752.73/297.04	   Strict Trs:
752.73/297.04	     { isLeaf(leaf()) -> true()
752.73/297.04	     , isLeaf(cons(u, v)) -> false()
752.73/297.04	     , left(cons(u, v)) -> u
752.73/297.04	     , right(cons(u, v)) -> v
752.73/297.04	     , concat(leaf(), y) -> y
752.73/297.04	     , concat(cons(u, v), y) -> cons(u, concat(v, y))
752.73/297.04	     , less_leaves(u, v) -> if1(isLeaf(u), isLeaf(v), u, v)
752.73/297.04	     , if1(b, true(), u, v) -> false()
752.73/297.04	     , if1(b, false(), u, v) -> if2(b, u, v)
752.73/297.04	     , if2(true(), u, v) -> true()
752.73/297.04	     , if2(false(), u, v) ->
752.73/297.04	       less_leaves(concat(left(u), right(u)), concat(left(v), right(v))) }
752.73/297.04	   Weak DPs:
752.73/297.04	     { isLeaf^#(leaf()) -> c_1()
752.73/297.04	     , isLeaf^#(cons(u, v)) -> c_2()
752.73/297.04	     , if1^#(b, true(), u, v) -> c_8()
752.73/297.04	     , if2^#(true(), u, v) -> c_10() }
752.73/297.04	   Obligation:
752.73/297.04	     runtime complexity
752.73/297.04	   Answer:
752.73/297.04	     MAYBE
752.73/297.04	   
752.73/297.04	   Empty strict component of the problem is NOT empty.
752.73/297.04	
752.73/297.04	
752.73/297.04	Arrrr..
753.04/297.34	EOF