MAYBE
871.58/297.10	MAYBE
871.58/297.10	
871.58/297.10	We are left with following problem, upon which TcT provides the
871.58/297.10	certificate MAYBE.
871.58/297.10	
871.58/297.10	Strict Trs:
871.58/297.10	  { active(f(X)) -> f(active(X))
871.58/297.10	  , active(f(X)) -> mark(if(X, c(), f(true())))
871.58/297.10	  , active(if(X1, X2, X3)) -> if(X1, active(X2), X3)
871.58/297.10	  , active(if(X1, X2, X3)) -> if(active(X1), X2, X3)
871.58/297.10	  , active(if(true(), X, Y)) -> mark(X)
871.58/297.10	  , active(if(false(), X, Y)) -> mark(Y)
871.58/297.10	  , f(mark(X)) -> mark(f(X))
871.58/297.10	  , f(ok(X)) -> ok(f(X))
871.58/297.10	  , if(X1, mark(X2), X3) -> mark(if(X1, X2, X3))
871.58/297.10	  , if(mark(X1), X2, X3) -> mark(if(X1, X2, X3))
871.58/297.10	  , if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3))
871.58/297.10	  , proper(f(X)) -> f(proper(X))
871.58/297.10	  , proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3))
871.58/297.10	  , proper(c()) -> ok(c())
871.58/297.10	  , proper(true()) -> ok(true())
871.58/297.10	  , proper(false()) -> ok(false())
871.58/297.10	  , top(mark(X)) -> top(proper(X))
871.58/297.10	  , top(ok(X)) -> top(active(X)) }
871.58/297.10	Obligation:
871.58/297.10	  derivational complexity
871.58/297.10	Answer:
871.58/297.10	  MAYBE
871.58/297.10	
871.58/297.10	None of the processors succeeded.
871.58/297.10	
871.58/297.10	Details of failed attempt(s):
871.58/297.10	-----------------------------
871.58/297.10	1) 'Inspecting Problem... (timeout of 297 seconds)' failed due to
871.58/297.10	   the following reason:
871.58/297.10	   
871.58/297.10	   Computation stopped due to timeout after 297.0 seconds.
871.58/297.10	
871.58/297.10	2) 'Fastest (timeout of 60 seconds)' failed due to the following
871.58/297.10	   reason:
871.58/297.10	   
871.58/297.10	   Computation stopped due to timeout after 60.0 seconds.
871.58/297.10	
871.58/297.10	3) 'iteProgress (timeout of 297 seconds)' failed due to the
871.58/297.10	   following reason:
871.58/297.10	   
871.58/297.10	   Fail
871.58/297.10	
871.58/297.10	4) 'bsearch-matrix (timeout of 297 seconds)' failed due to the
871.58/297.10	   following reason:
871.58/297.10	   
871.58/297.10	   The input cannot be shown compatible
871.58/297.10	
871.58/297.10	
871.58/297.10	Arrrr..
871.58/297.13	EOF