MAYBE
892.61/297.13	MAYBE
892.61/297.13	
892.61/297.13	We are left with following problem, upon which TcT provides the
892.61/297.13	certificate MAYBE.
892.61/297.13	
892.61/297.13	Strict Trs:
892.61/297.13	  { active(__(X1, X2)) -> __(X1, active(X2))
892.61/297.13	  , active(__(X1, X2)) -> __(active(X1), X2)
892.61/297.13	  , active(__(X, nil())) -> mark(X)
892.61/297.13	  , active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z)))
892.61/297.13	  , active(__(nil(), X)) -> mark(X)
892.61/297.13	  , active(and(X1, X2)) -> and(active(X1), X2)
892.61/297.13	  , active(and(tt(), X)) -> mark(X)
892.61/297.13	  , active(isList(V)) -> mark(isNeList(V))
892.61/297.13	  , active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2)))
892.61/297.13	  , active(isList(nil())) -> mark(tt())
892.61/297.13	  , active(isNeList(V)) -> mark(isQid(V))
892.61/297.13	  , active(isNeList(__(V1, V2))) ->
892.61/297.13	    mark(and(isList(V1), isNeList(V2)))
892.61/297.13	  , active(isNeList(__(V1, V2))) ->
892.61/297.13	    mark(and(isNeList(V1), isList(V2)))
892.61/297.13	  , active(isQid(a())) -> mark(tt())
892.61/297.13	  , active(isQid(e())) -> mark(tt())
892.61/297.13	  , active(isQid(i())) -> mark(tt())
892.61/297.13	  , active(isQid(o())) -> mark(tt())
892.61/297.13	  , active(isQid(u())) -> mark(tt())
892.61/297.13	  , active(isNePal(V)) -> mark(isQid(V))
892.61/297.13	  , active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P)))
892.61/297.13	  , active(isPal(V)) -> mark(isNePal(V))
892.61/297.13	  , active(isPal(nil())) -> mark(tt())
892.61/297.13	  , __(X1, mark(X2)) -> mark(__(X1, X2))
892.61/297.13	  , __(mark(X1), X2) -> mark(__(X1, X2))
892.61/297.13	  , __(ok(X1), ok(X2)) -> ok(__(X1, X2))
892.61/297.13	  , and(mark(X1), X2) -> mark(and(X1, X2))
892.61/297.13	  , and(ok(X1), ok(X2)) -> ok(and(X1, X2))
892.61/297.13	  , isList(ok(X)) -> ok(isList(X))
892.61/297.13	  , isNeList(ok(X)) -> ok(isNeList(X))
892.61/297.13	  , isQid(ok(X)) -> ok(isQid(X))
892.61/297.13	  , isNePal(ok(X)) -> ok(isNePal(X))
892.61/297.13	  , isPal(ok(X)) -> ok(isPal(X))
892.61/297.13	  , proper(__(X1, X2)) -> __(proper(X1), proper(X2))
892.61/297.13	  , proper(nil()) -> ok(nil())
892.61/297.13	  , proper(and(X1, X2)) -> and(proper(X1), proper(X2))
892.61/297.13	  , proper(tt()) -> ok(tt())
892.61/297.13	  , proper(isList(X)) -> isList(proper(X))
892.61/297.13	  , proper(isNeList(X)) -> isNeList(proper(X))
892.61/297.13	  , proper(isQid(X)) -> isQid(proper(X))
892.61/297.13	  , proper(isNePal(X)) -> isNePal(proper(X))
892.61/297.13	  , proper(isPal(X)) -> isPal(proper(X))
892.61/297.13	  , proper(a()) -> ok(a())
892.61/297.13	  , proper(e()) -> ok(e())
892.61/297.13	  , proper(i()) -> ok(i())
892.61/297.13	  , proper(o()) -> ok(o())
892.61/297.13	  , proper(u()) -> ok(u())
892.61/297.13	  , top(mark(X)) -> top(proper(X))
892.61/297.13	  , top(ok(X)) -> top(active(X)) }
892.61/297.13	Obligation:
892.61/297.13	  derivational complexity
892.61/297.13	Answer:
892.61/297.13	  MAYBE
892.61/297.13	
892.61/297.13	None of the processors succeeded.
892.61/297.13	
892.61/297.13	Details of failed attempt(s):
892.61/297.13	-----------------------------
892.61/297.13	1) 'Inspecting Problem... (timeout of 297 seconds)' failed due to
892.61/297.13	   the following reason:
892.61/297.13	   
892.61/297.13	   Computation stopped due to timeout after 297.0 seconds.
892.61/297.13	
892.61/297.13	2) 'Fastest (timeout of 60 seconds)' failed due to the following
892.61/297.13	   reason:
892.61/297.13	   
892.61/297.13	   Computation stopped due to timeout after 60.0 seconds.
892.61/297.13	
892.61/297.13	3) 'iteProgress (timeout of 297 seconds)' failed due to the
892.61/297.13	   following reason:
892.61/297.13	   
892.61/297.13	   Fail
892.61/297.13	
892.61/297.13	4) 'bsearch-matrix (timeout of 297 seconds)' failed due to the
892.61/297.13	   following reason:
892.61/297.13	   
892.61/297.13	   The input cannot be shown compatible
892.61/297.13	
892.61/297.13	
892.61/297.13	Arrrr..
892.86/297.32	EOF