0.00/0.09	NO
0.00/0.09	(ignored inputs)COMMENT doi:10.1016/0022-0000 ( 86 ) 90033-4 [47] p. 352 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.09	Conditional Rewrite Rules:
0.00/0.09	   [ p(q(?x)) -> p(r(?x)),
0.00/0.09	     q(h(?x)) -> r(?x),
0.00/0.09	     r(?x) -> r(h(?x)) | s(?x) == 0,
0.00/0.09	     s(?x) -> 1 ]
0.00/0.09	Check whether all rules are type 3
0.00/0.09	OK
0.00/0.09	Check whether the input is deterministic
0.00/0.09	OK
0.00/0.09	Result of unraveling:
0.00/0.09	   [ p(q(?x)) -> p(r(?x)),
0.00/0.09	     q(h(?x)) -> r(?x),
0.00/0.09	     r(?x) -> U0(s(?x),?x),
0.00/0.09	     U0(0,?x) -> r(h(?x)),
0.00/0.09	     s(?x) -> 1 ]
0.00/0.09	Check whether U(R) is terminating
0.00/0.09	OK
0.00/0.09	Check whether the input is weakly left-linear
0.00/0.09	OK
0.00/0.09	Check whether U(R) is confluent
0.00/0.09	U(R) is not confluent
0.00/0.09	Conditional critical pairs (CCPs):
0.00/0.09	   [ p(r(?x_1)) = p(r(h(?x_1))) ]
0.00/0.09	Check whether the input is almost orthogonale
0.00/0.09	not almost orthogonal
0.00/0.09	OK
0.00/0.09	Check whether the input is absolutely irreducible
0.00/0.09	OK
0.00/0.09	Check whether all CCPs are joinable
0.00/0.09	Some ccp may be feasible but not joinable
0.00/0.09	   [ p(r(?x_1)) = p(r(h(?x_1))) ]
0.00/0.09	A feasible but not joinable CCP: p(r(?x_1)) = p(r(h(?x_1)))
0.00/0.09	/export/starexec/sandbox/benchmark/theBenchmark.trs: Success(not CR)
0.00/0.09	(27 msec.)
0.00/0.09	EOF