0.00/0.03	NO
0.00/0.03	(ignored inputs)COMMENT submitted by: Florian Messner used by COPS #1145
0.00/0.03	Conditional Rewrite Rules:
0.00/0.03	   [ f(k(?z),a) -> g(?x,?x) | h(?z) == ?x,?x == b,
0.00/0.03	     f(k(a),h(a)) -> k(?x) | a == ?x,
0.00/0.03	     k(?x) -> h(?x),
0.00/0.03	     k(?x) -> b,
0.00/0.03	     k(?x) -> a,
0.00/0.03	     a -> b,
0.00/0.03	     g(?x,?x) -> a ]
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(k(?z),a) -> U0(h(?z),?z),
0.00/0.03	     U0(?x,?z) -> U1(?x,?z,?x),
0.00/0.03	     U1(b,?z,?x) -> g(?x,?x),
0.00/0.03	     f(k(a),h(a)) -> U2(a),
0.00/0.03	     U2(?x) -> k(?x),
0.00/0.03	     k(?x) -> h(?x),
0.00/0.03	     k(?x) -> b,
0.00/0.03	     k(?x) -> a,
0.00/0.03	     a -> b,
0.00/0.03	     g(?x,?x) -> a ]
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(h(?x_2),a) = g(?x,?x) | h(?x_2) == ?x,?x == b,
0.00/0.03	     f(b,a) = g(?x,?x) | h(?x_3) == ?x,?x == b,
0.00/0.03	     f(a,a) = g(?x,?x) | h(?x_4) == ?x,?x == b,
0.00/0.03	     f(k(?z),b) = g(?x,?x) | h(?z) == ?x,?x == b,
0.00/0.03	     f(h(a),h(a)) = k(?x_1) | a == ?x_1,
0.00/0.03	     f(b,h(a)) = k(?x_1) | a == ?x_1,
0.00/0.03	     f(a,h(a)) = k(?x_1) | a == ?x_1,
0.00/0.03	     f(k(b),h(a)) = k(?x_1) | a == ?x_1,
0.00/0.03	     f(k(a),h(b)) = k(?x_1) | a == ?x_1,
0.00/0.03	     b = h(?x_3),
0.00/0.03	     a = h(?x_4),
0.00/0.03	     h(?x_2) = b,
0.00/0.03	     a = b,
0.00/0.03	     h(?x_2) = a,
0.00/0.03	     b = a ]
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(h(?x_2),a) = g(?x,?x) | h(?x_2) == ?x,?x == b,
0.00/0.03	     f(b,a) = g(?x,?x) | h(?x_3) == ?x,?x == b,
0.00/0.03	     f(a,a) = g(?x,?x) | h(?x_4) == ?x,?x == b,
0.00/0.03	     f(k(?z),b) = g(?x,?x) | h(?z) == ?x,?x == b,
0.00/0.03	     f(h(a),h(a)) = k(?x_1) | a == ?x_1,
0.00/0.03	     f(b,h(a)) = k(?x_1) | a == ?x_1,
0.00/0.03	     f(a,h(a)) = k(?x_1) | a == ?x_1,
0.00/0.03	     f(k(b),h(a)) = k(?x_1) | a == ?x_1,
0.00/0.03	     f(k(a),h(b)) = k(?x_1) | a == ?x_1,
0.00/0.03	     b = h(?x_3),
0.00/0.03	     a = h(?x_4),
0.00/0.03	     h(?x_2) = b,
0.00/0.03	     h(?x_2) = a ]
0.00/0.03	A feasible but not joinable CCP: b = h(?x_3)
0.00/0.03	/export/starexec/sandbox/benchmark/theBenchmark.trs: Success(not CR)
0.00/0.03	(1 msec.)
0.00/0.03	EOF