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