0.00/0.04	MAYBE
0.00/0.04	(ignored inputs)COMMENT Example 1 in extended version of [92]
0.00/0.04	Conditional Rewrite Rules:
0.00/0.04	   [ f(c(?x),c(c(?y))) -> a(a(?x)) | c(f(?x,?y)) == c(a(b)),
0.00/0.04	     f(c(c(c(?x))),?y) -> a(?y) | c(f(c(?x),c(c(?y)))) == c(a(a(b))),
0.00/0.04	     h(b) -> b,
0.00/0.04	     h(a(a(?x))) -> a(b) | h(?x) == b ]
0.00/0.04	Check whether all rules are type 3
0.00/0.04	OK
0.00/0.04	Check whether the input is deterministic
0.00/0.04	OK
0.00/0.04	Result of unraveling:
0.00/0.04	   [ f(c(?x),c(c(?y))) -> U0(c(f(?x,?y)),?x,?y),
0.00/0.04	     U0(c(a(b)),?x,?y) -> a(a(?x)),
0.00/0.04	     f(c(c(c(?x))),?y) -> U1(c(f(c(?x),c(c(?y)))),?x,?y),
0.00/0.04	     U1(c(a(a(b))),?x,?y) -> a(?y),
0.00/0.04	     h(b) -> b,
0.00/0.04	     h(a(a(?x))) -> U2(h(?x),?x),
0.00/0.04	     U2(b,?x) -> a(b) ]
0.00/0.04	Check whether U(R) is terminating
0.00/0.04	OK
0.00/0.04	Check whether the input is weakly left-linear
0.00/0.04	OK
0.00/0.04	Check whether U(R) is confluent
0.00/0.04	U(R) is not confluent
0.00/0.04	Conditional critical pairs (CCPs):
0.00/0.04	   [ 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.04	     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.04	Check whether the input is almost orthogonale
0.00/0.04	not almost orthogonal
0.00/0.04	OK
0.00/0.04	Check whether the input is absolutely irreducible
0.00/0.04	OK
0.00/0.04	Check whether all CCPs are joinable
0.00/0.04	Some ccp may be feasible but not joinable
0.00/0.04	   [ 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.04	     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.04	/export/starexec/sandbox/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.04	(9 msec.)
0.00/0.04	EOF