MAYBE
779.27/297.10	MAYBE
779.27/297.10	
779.27/297.10	We are left with following problem, upon which TcT provides the
779.27/297.10	certificate MAYBE.
779.27/297.10	
779.27/297.10	Strict Trs:
779.27/297.10	  { fstsplit(0(), x) -> nil()
779.27/297.10	  , fstsplit(s(n), nil()) -> nil()
779.27/297.10	  , fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
779.27/297.10	  , sndsplit(0(), x) -> x
779.27/297.10	  , sndsplit(s(n), nil()) -> nil()
779.27/297.10	  , sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
779.27/297.10	  , empty(nil()) -> true()
779.27/297.10	  , empty(cons(h, t)) -> false()
779.27/297.10	  , leq(0(), m) -> true()
779.27/297.10	  , leq(s(n), 0()) -> false()
779.27/297.10	  , leq(s(n), s(m)) -> leq(n, m)
779.27/297.10	  , length(nil()) -> 0()
779.27/297.10	  , length(cons(h, t)) -> s(length(t))
779.27/297.10	  , app(nil(), x) -> x
779.27/297.10	  , app(cons(h, t), x) -> cons(h, app(t, x))
779.27/297.10	  , map_f(pid, nil()) -> nil()
779.27/297.10	  , map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
779.27/297.10	  , process(store, m) -> if1(store, m, leq(m, length(store)))
779.27/297.10	  , if1(store, m, true()) -> if2(store, m, empty(fstsplit(m, store)))
779.27/297.10	  , if1(store, m, false()) ->
779.27/297.10	    if3(store, m, empty(fstsplit(m, app(map_f(self(), nil()), store))))
779.27/297.10	  , if2(store, m, false()) ->
779.27/297.10	    process(app(map_f(self(), nil()), sndsplit(m, store)), m)
779.27/297.10	  , if3(store, m, false()) ->
779.27/297.10	    process(sndsplit(m, app(map_f(self(), nil()), store)), m) }
779.27/297.10	Obligation:
779.27/297.10	  innermost runtime complexity
779.27/297.10	Answer:
779.27/297.10	  MAYBE
779.27/297.10	
779.27/297.10	None of the processors succeeded.
779.27/297.10	
779.27/297.10	Details of failed attempt(s):
779.27/297.10	-----------------------------
779.27/297.10	1) 'empty' failed due to the following reason:
779.27/297.10	   
779.27/297.10	   Empty strict component of the problem is NOT empty.
779.27/297.10	
779.27/297.10	2) 'Best' failed due to the following reason:
779.27/297.10	   
779.27/297.10	   None of the processors succeeded.
779.27/297.10	   
779.27/297.10	   Details of failed attempt(s):
779.27/297.10	   -----------------------------
779.27/297.10	   1) 'With Problem ... (timeout of 297 seconds)' failed due to the
779.27/297.10	      following reason:
779.27/297.10	      
779.27/297.10	      Computation stopped due to timeout after 297.0 seconds.
779.27/297.10	   
779.27/297.10	   2) 'Best' failed due to the following reason:
779.27/297.10	      
779.27/297.10	      None of the processors succeeded.
779.27/297.10	      
779.27/297.10	      Details of failed attempt(s):
779.27/297.10	      -----------------------------
779.27/297.10	      1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
779.27/297.10	         seconds)' failed due to the following reason:
779.27/297.10	         
779.27/297.10	         Computation stopped due to timeout after 148.0 seconds.
779.27/297.10	      
779.27/297.10	      2) 'Best' failed due to the following reason:
779.27/297.10	         
779.27/297.10	         None of the processors succeeded.
779.27/297.10	         
779.27/297.10	         Details of failed attempt(s):
779.27/297.10	         -----------------------------
779.27/297.10	         1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
779.27/297.10	            to the following reason:
779.27/297.10	            
779.27/297.10	            The input cannot be shown compatible
779.27/297.10	         
779.27/297.10	         2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
779.27/297.10	            following reason:
779.27/297.10	            
779.27/297.10	            The input cannot be shown compatible
779.27/297.10	         
779.27/297.10	      
779.27/297.10	      3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
779.27/297.10	         failed due to the following reason:
779.27/297.10	         
779.27/297.10	         None of the processors succeeded.
779.27/297.10	         
779.27/297.10	         Details of failed attempt(s):
779.27/297.10	         -----------------------------
779.27/297.10	         1) 'Bounds with minimal-enrichment and initial automaton 'match''
779.27/297.10	            failed due to the following reason:
779.27/297.10	            
779.27/297.10	            match-boundness of the problem could not be verified.
779.27/297.10	         
779.27/297.10	         2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
779.27/297.10	            failed due to the following reason:
779.27/297.10	            
779.27/297.10	            match-boundness of the problem could not be verified.
779.27/297.10	         
779.27/297.10	      
779.27/297.10	   
779.27/297.10	
779.27/297.10	
779.27/297.10	Arrrr..
779.38/297.23	EOF