0.00/0.09	MAYBE
0.00/0.09	(ignored inputs)COMMENT Example 2 in extended version of [92]
0.00/0.09	Conditional Rewrite Rules:
0.00/0.09	   [ f(c(?x),c(c(?y))) -> a(a(?x)) | c(f(?x,?y)) == c(a(b)),
0.00/0.09	     f(c(c(c(?x))),?y) -> a(?y) | c(f(c(?x),c(c(?y)))) == c(a(a(b))),
0.00/0.09	     a(?x) -> b,
0.00/0.09	     a(?x) -> f(?x,?x) ]
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	   [ f(c(?x),c(c(?y))) -> U0(c(f(?x,?y)),?x,?y),
0.00/0.09	     U0(c(a(b)),?x,?y) -> a(a(?x)),
0.00/0.09	     f(c(c(c(?x))),?y) -> U1(c(f(c(?x),c(c(?y)))),?x,?y),
0.00/0.09	     U1(c(a(a(b))),?x,?y) -> a(?y),
0.00/0.09	     a(?x) -> b,
0.00/0.09	     a(?x) -> f(?x,?x) ]
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	   [ a(c(c(?y))) = a(a(c(c(?x_1)))) | c(f(c(?x_1),c(c(c(c(?y)))))) == c(a(a(b))),c(f(c(c(?x_1)),?y)) == c(a(b)),
0.00/0.09	     a(a(c(c(?x_1)))) = a(c(c(?y))) | c(f(c(c(?x_1)),?y)) == c(a(b)),c(f(c(?x_1),c(c(c(c(?y)))))) == c(a(a(b))),
0.00/0.09	     f(?x_3,?x_3) = b,
0.00/0.09	     b = f(?x_2,?x_2) ]
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	not absolutely irreducible
0.00/0.09	/export/starexec/sandbox/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.09	(45 msec.)
0.00/0.09	EOF