0.00/0.03	NO
0.00/0.03	(ignored inputs)COMMENT [75] Example 10 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.03	Conditional Rewrite Rules:
0.00/0.03	   [ f(g(?x)) -> ?x | ?x == s(0),
0.00/0.03	     g(s(?x)) -> g(?x) ]
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	   [ f(g(?x)) -> U0(?x,?x),
0.00/0.03	     U0(s(0),?x) -> ?x,
0.00/0.03	     g(s(?x)) -> g(?x) ]
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	   [ f(g(?x_1)) = s(?x_1) | s(?x_1) == s(0) ]
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	   [ f(g(?x_1)) = s(?x_1) | s(?x_1) == s(0) ]
0.00/0.03	A non-joinable pair: f(g(0)) <-*- o -*-> s(0)
0.00/0.03	instanciated and reduced from f(g(?x_1)) = s(?x_1) | s(?x_1) == s(0)
0.00/0.03	/export/starexec/sandbox/benchmark/theBenchmark.trs: Success(not CR)
0.00/0.03	(4 msec.)
0.00/0.03	EOF