0.00/0.03	MAYBE
0.00/0.03	(ignored inputs)COMMENT [75] Example 2 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.03	Conditional Rewrite Rules:
0.00/0.03	   [ s(p(?x)) -> ?x,
0.00/0.03	     p(s(?x)) -> ?x,
0.00/0.03	     pos(0) -> false,
0.00/0.03	     pos(s(0)) -> true,
0.00/0.03	     pos(s(?x)) -> true | pos(?x) == true,
0.00/0.03	     pos(p(?x)) -> false | pos(?x) == false ]
0.00/0.03	Check whether all rules are type 3
0.00/0.03	OK
0.00/0.03	Check whether the input is deterministic
0.00/0.03	OK
0.00/0.03	Result of unraveling:
0.00/0.03	   [ s(p(?x)) -> ?x,
0.00/0.03	     p(s(?x)) -> ?x,
0.00/0.03	     pos(0) -> false,
0.00/0.03	     pos(s(0)) -> true,
0.00/0.03	     pos(s(?x)) -> U0(pos(?x),?x),
0.00/0.03	     U0(true,?x) -> true,
0.00/0.03	     pos(p(?x)) -> U1(pos(?x),?x),
0.00/0.03	     U1(false,?x) -> false ]
0.00/0.03	Check whether U(R) is terminating
0.00/0.03	OK
0.00/0.03	Check whether the input is weakly left-linear
0.00/0.03	OK
0.00/0.03	Check whether U(R) is confluent
0.00/0.03	U(R) is not confluent
0.00/0.03	Conditional critical pairs (CCPs):
0.00/0.03	   [ s(?x_1) = s(?x_1),
0.00/0.03	     p(?x) = p(?x),
0.00/0.03	     true = true | pos(0) == true,
0.00/0.03	     pos(?x) = true | pos(p(?x)) == true,
0.00/0.03	     true = true | pos(0) == true,
0.00/0.03	     pos(?x_1) = false | pos(s(?x_1)) == false ]
0.00/0.03	Check whether the input is almost orthogonale
0.00/0.03	not almost orthogonal
0.00/0.03	OK
0.00/0.03	Check whether the input is absolutely irreducible
0.00/0.03	OK
0.00/0.03	Check whether all CCPs are joinable
0.00/0.03	Some ccp may be feasible but not joinable
0.00/0.03	   [ pos(?x) = true | pos(p(?x)) == true,
0.00/0.03	     pos(?x_1) = false | pos(s(?x_1)) == false ]
0.00/0.03	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.03	(4 msec.)
0.00/0.03	EOF