0.10/0.10	YES
0.10/0.10	Conditional Rewrite Rules:
0.10/0.10	   [ b -> f(a),
0.10/0.10	     f(?x) -> f(a) | b == ?x ]
0.10/0.10	Check whether all rules are type 3
0.10/0.10	OK
0.10/0.10	Check whether the input is deterministic
0.10/0.10	OK
0.10/0.10	Result of unraveling:
0.10/0.10	   [ b -> f(a),
0.10/0.10	     f(?x) -> U0(b,?x),
0.10/0.10	     U0(?x,?x) -> f(a) ]
0.10/0.10	Check whether U(R) is terminating
0.10/0.10	failed to show termination
0.10/0.10	Check whether the input is weakly left-linear
0.10/0.10	OK
0.10/0.10	Conditional critical pairs (CCPs):
0.10/0.10	   [  ]
0.10/0.10	Check whether the input is almost orthogonale
0.10/0.10	OK
0.10/0.10	Check whether the input is properly oriented
0.10/0.10	OK
0.10/0.10	Check whether the input is right-stable
0.10/0.10	not right-stable
0.10/0.10	OK
0.10/0.10	Check U(R) is confluent
0.10/0.10	Rewrite Rules:
0.10/0.10	   [ b -> f(a),
0.10/0.10	     f(?x) -> U0(b,?x),
0.10/0.10	     U0(?x,?x) -> f(a) ]
0.10/0.10	Apply Direct Methods...
0.10/0.10	Inner CPs:
0.10/0.10	   [  ]
0.10/0.10	Outer CPs:
0.10/0.10	   [  ]
0.10/0.10	Overlay, check Innermost Termination...
0.10/0.10	unknown Innermost Terminating
0.10/0.10	unknown Knuth & Bendix
0.10/0.10	not Left-Linear, Right-Linear
0.10/0.10	Simple-Right-Linear
0.10/0.10	Direct Methods: CR
0.10/0.10	
0.10/0.10	Combined result: CR
0.10/0.10	U(R) is confluent
0.10/0.10	R is deterministic, weakly left-linear and U(R) is confluent
0.10/0.10	/home/www/colo6-c703/cocoweb/session/c9l2hu6ptm1v0ic6b4oohpr3d1/JLAMP21CTRS_2.trs: Success(CR)
0.10/0.10	(29 msec.)