MAYBE
1110.76/297.06	MAYBE
1110.76/297.06	
1110.76/297.06	We are left with following problem, upon which TcT provides the
1110.76/297.06	certificate MAYBE.
1110.76/297.06	
1110.76/297.06	Strict Trs:
1110.76/297.06	  { start(i) ->
1110.76/297.06	    busy(F(), closed(), stop(), false(), false(), false(), i)
1110.76/297.06	  , busy(fl, open(), up(), b1, b2, b3, i) -> incorrect()
1110.76/297.06	  , busy(fl, open(), down(), b1, b2, b3, i) -> incorrect()
1110.76/297.06	  , busy(F(), d, stop(), b1, true(), b3, i) ->
1110.76/297.06	    idle(F(), open(), stop(), b1, false(), b3, i)
1110.76/297.06	  , busy(F(), closed(), stop(), false(), false(), false(), empty())
1110.76/297.06	    -> correct()
1110.76/297.06	  , busy(F(),
1110.76/297.06	         closed(),
1110.76/297.06	         stop(),
1110.76/297.06	         false(),
1110.76/297.06	         false(),
1110.76/297.06	         false(),
1110.76/297.06	         newbuttons(i1, i2, i3, i))
1110.76/297.06	    ->
1110.76/297.06	    idle(F(),
1110.76/297.06	         closed(),
1110.76/297.06	         stop(),
1110.76/297.06	         false(),
1110.76/297.06	         false(),
1110.76/297.06	         false(),
1110.76/297.06	         newbuttons(i1, i2, i3, i))
1110.76/297.06	  , busy(F(), closed(), stop(), false(), false(), true(), i) ->
1110.76/297.06	    idle(F(), closed(), up(), false(), false(), true(), i)
1110.76/297.06	  , busy(F(), closed(), stop(), true(), false(), b3, i) ->
1110.76/297.06	    idle(F(), closed(), down(), true(), false(), b3, i)
1110.76/297.06	  , busy(F(), closed(), up(), b1, false(), b3, i) ->
1110.76/297.06	    idle(FS(), closed(), up(), b1, false(), b3, i)
1110.76/297.06	  , busy(F(), closed(), up(), b1, true(), b3, i) ->
1110.76/297.06	    idle(F(), closed(), stop(), b1, true(), b3, i)
1110.76/297.06	  , busy(F(), closed(), down(), b1, false(), b3, i) ->
1110.76/297.06	    idle(BF(), closed(), down(), b1, false(), b3, i)
1110.76/297.06	  , busy(F(), closed(), down(), b1, true(), b3, i) ->
1110.76/297.06	    idle(F(), closed(), stop(), b1, true(), b3, i)
1110.76/297.06	  , busy(F(), open(), stop(), b1, false(), b3, i) ->
1110.76/297.06	    idle(F(), closed(), stop(), b1, false(), b3, i)
1110.76/297.06	  , busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect()
1110.76/297.06	  , busy(BF(), closed(), up(), b1, b2, b3, i) ->
1110.76/297.06	    idle(F(), closed(), up(), b1, b2, b3, i)
1110.76/297.06	  , busy(BF(), closed(), down(), b1, b2, b3, i) ->
1110.76/297.06	    idle(B(), closed(), down(), b1, b2, b3, i)
1110.76/297.06	  , busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect()
1110.76/297.06	  , busy(FS(), closed(), up(), b1, b2, b3, i) ->
1110.76/297.06	    idle(S(), closed(), up(), b1, b2, b3, i)
1110.76/297.06	  , busy(FS(), closed(), down(), b1, b2, b3, i) ->
1110.76/297.06	    idle(F(), closed(), down(), b1, b2, b3, i)
1110.76/297.06	  , busy(B(), d, stop(), true(), b2, b3, i) ->
1110.76/297.06	    idle(B(), open(), stop(), false(), b2, b3, i)
1110.76/297.06	  , busy(B(), closed(), stop(), false(), false(), false(), empty())
1110.76/297.06	    -> correct()
1110.76/297.06	  , busy(B(),
1110.76/297.06	         closed(),
1110.76/297.06	         stop(),
1110.76/297.06	         false(),
1110.76/297.06	         false(),
1110.76/297.06	         false(),
1110.76/297.06	         newbuttons(i1, i2, i3, i))
1110.76/297.06	    ->
1110.76/297.06	    idle(B(),
1110.76/297.06	         closed(),
1110.76/297.06	         stop(),
1110.76/297.06	         false(),
1110.76/297.06	         false(),
1110.76/297.06	         false(),
1110.76/297.06	         newbuttons(i1, i2, i3, i))
1110.76/297.06	  , busy(B(), closed(), stop(), false(), false(), true(), i) ->
1110.76/297.06	    idle(B(), closed(), up(), false(), false(), true(), i)
1110.76/297.06	  , busy(B(), closed(), stop(), false(), true(), b3, i) ->
1110.76/297.06	    idle(B(), closed(), up(), false(), true(), b3, i)
1110.76/297.06	  , busy(B(), closed(), up(), false(), b2, b3, i) ->
1110.76/297.06	    idle(BF(), closed(), up(), false(), b2, b3, i)
1110.76/297.06	  , busy(B(), closed(), up(), true(), b2, b3, i) ->
1110.76/297.06	    idle(B(), closed(), stop(), true(), b2, b3, i)
1110.76/297.06	  , busy(B(), closed(), down(), b1, b2, b3, i) ->
1110.76/297.06	    idle(B(), closed(), stop(), b1, b2, b3, i)
1110.76/297.06	  , busy(B(), open(), stop(), false(), b2, b3, i) ->
1110.76/297.06	    idle(B(), closed(), stop(), false(), b2, b3, i)
1110.76/297.06	  , busy(S(), d, stop(), b1, b2, true(), i) ->
1110.76/297.06	    idle(S(), open(), stop(), b1, b2, false(), i)
1110.76/297.06	  , busy(S(), closed(), stop(), b1, true(), false(), i) ->
1110.76/297.06	    idle(S(), closed(), down(), b1, true(), false(), i)
1110.76/297.06	  , busy(S(), closed(), stop(), false(), false(), false(), empty())
1110.76/297.06	    -> correct()
1110.76/297.06	  , busy(S(),
1110.76/297.06	         closed(),
1110.76/297.06	         stop(),
1110.76/297.06	         false(),
1110.76/297.06	         false(),
1110.76/297.06	         false(),
1110.76/297.06	         newbuttons(i1, i2, i3, i))
1110.76/297.06	    ->
1110.76/297.06	    idle(S(),
1110.76/297.06	         closed(),
1110.76/297.06	         stop(),
1110.76/297.06	         false(),
1110.76/297.06	         false(),
1110.76/297.06	         false(),
1110.76/297.06	         newbuttons(i1, i2, i3, i))
1110.76/297.06	  , busy(S(), closed(), stop(), true(), false(), false(), i) ->
1110.76/297.06	    idle(S(), closed(), down(), true(), false(), false(), i)
1110.76/297.06	  , busy(S(), closed(), up(), b1, b2, b3, i) ->
1110.76/297.06	    idle(S(), closed(), stop(), b1, b2, b3, i)
1110.76/297.06	  , busy(S(), closed(), down(), b1, b2, false(), i) ->
1110.76/297.06	    idle(FS(), closed(), down(), b1, b2, false(), i)
1110.76/297.06	  , busy(S(), closed(), down(), b1, b2, true(), i) ->
1110.76/297.06	    idle(S(), closed(), stop(), b1, b2, true(), i)
1110.76/297.06	  , busy(S(), open(), stop(), b1, b2, false(), i) ->
1110.76/297.06	    idle(S(), closed(), stop(), b1, b2, false(), i)
1110.76/297.06	  , idle(fl, d, m, b1, b2, b3, empty()) ->
1110.76/297.06	    busy(fl, d, m, b1, b2, b3, empty())
1110.76/297.06	  , idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
1110.76/297.06	    busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
1110.76/297.06	  , or(false(), b) -> b
1110.76/297.06	  , or(true(), b) -> true() }
1110.76/297.06	Obligation:
1110.76/297.06	  innermost runtime complexity
1110.76/297.06	Answer:
1110.76/297.06	  MAYBE
1110.76/297.06	
1110.76/297.06	None of the processors succeeded.
1110.76/297.06	
1110.76/297.06	Details of failed attempt(s):
1110.76/297.06	-----------------------------
1110.76/297.06	1) 'empty' failed due to the following reason:
1110.76/297.06	   
1110.76/297.06	   Empty strict component of the problem is NOT empty.
1110.76/297.06	
1110.76/297.06	2) 'Best' failed due to the following reason:
1110.76/297.06	   
1110.76/297.06	   None of the processors succeeded.
1110.76/297.06	   
1110.76/297.06	   Details of failed attempt(s):
1110.76/297.06	   -----------------------------
1110.76/297.06	   1) 'With Problem ... (timeout of 297 seconds)' failed due to the
1110.76/297.06	      following reason:
1110.76/297.06	      
1110.76/297.06	      Computation stopped due to timeout after 297.0 seconds.
1110.76/297.06	   
1110.76/297.06	   2) 'Best' failed due to the following reason:
1110.76/297.06	      
1110.76/297.06	      None of the processors succeeded.
1110.76/297.06	      
1110.76/297.06	      Details of failed attempt(s):
1110.76/297.06	      -----------------------------
1110.76/297.06	      1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
1110.76/297.06	         seconds)' failed due to the following reason:
1110.76/297.06	         
1110.76/297.06	         Computation stopped due to timeout after 148.0 seconds.
1110.76/297.06	      
1110.76/297.06	      2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
1110.76/297.06	         failed due to the following reason:
1110.76/297.06	         
1110.76/297.06	         Computation stopped due to timeout after 24.0 seconds.
1110.76/297.06	      
1110.76/297.06	      3) 'Best' failed due to the following reason:
1110.76/297.06	         
1110.76/297.06	         None of the processors succeeded.
1110.76/297.06	         
1110.76/297.06	         Details of failed attempt(s):
1110.76/297.06	         -----------------------------
1110.76/297.06	         1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
1110.76/297.06	            following reason:
1110.76/297.06	            
1110.76/297.06	            The input cannot be shown compatible
1110.76/297.06	         
1110.76/297.06	         2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
1110.76/297.06	            to the following reason:
1110.76/297.06	            
1110.76/297.06	            The input cannot be shown compatible
1110.76/297.06	         
1110.76/297.06	      
1110.76/297.06	   
1110.76/297.06	
1110.76/297.06	
1110.76/297.06	Arrrr..
1110.95/297.19	EOF