0.05/0.05	YES
0.05/0.05	Conditional Rewrite Rules:
0.05/0.05	   [ a -> c,
0.05/0.05	     c -> b,
0.05/0.05	     a -> ?x | a == ?x,?x == b ]
0.05/0.05	Check whether all rules are type 3
0.05/0.05	OK
0.05/0.05	Check whether the input is deterministic
0.05/0.05	OK
0.05/0.05	Result of unraveling:
0.05/0.05	   [ a -> c,
0.05/0.05	     c -> b,
0.05/0.05	     a -> U0(a),
0.05/0.05	     U0(?x) -> U1(?x,?x),
0.05/0.05	     U1(b,?x) -> ?x ]
0.05/0.05	Check whether U(R) is terminating
0.05/0.05	failed to show termination
0.05/0.05	Check whether the input is weakly left-linear
0.05/0.05	OK
0.05/0.05	Conditional critical pairs (CCPs):
0.05/0.05	   [ ?x = c | a == ?x,?x == b,
0.05/0.05	     c = ?x | a == ?x,?x == b ]
0.05/0.05	Check whether the input is almost orthogonale
0.05/0.05	not almost orthogonal
0.05/0.05	OK
0.05/0.05	Check U(R) is confluent
0.05/0.05	Rewrite Rules:
0.05/0.05	   [ a -> c,
0.05/0.05	     c -> b,
0.05/0.05	     a -> U0(a),
0.05/0.05	     U0(?x) -> U1(?x,?x),
0.05/0.05	     U1(b,?x) -> ?x ]
0.05/0.05	Apply Direct Methods...
0.05/0.05	Inner CPs:
0.05/0.05	   [  ]
0.05/0.05	Outer CPs:
0.05/0.05	   [ c = U0(a) ]
0.05/0.05	Overlay, check Innermost Termination...
0.05/0.05	unknown Innermost Terminating
0.05/0.05	unknown Knuth & Bendix
0.05/0.05	Left-Linear, not Right-Linear
0.05/0.05	unknown Development Closed
0.05/0.05	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
0.05/0.05	unknown Upside-Parallel-Closed/Outside-Closed
0.05/0.05	(inner) Parallel CPs: (not computed)
0.05/0.05	unknown Toyama (Parallel CPs)
0.05/0.05	Simultaneous CPs:
0.05/0.05	   [ U0(a) = c,
0.05/0.05	     c = U0(a) ]
0.05/0.05	unknown Okui (Simultaneous CPs)
0.05/0.05	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
0.05/0.05	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
0.05/0.05	check Locally Decreasing Diagrams by Rule Labelling...
0.05/0.05	Critical Pair <U0(a), c> by Rules <2, 0> preceded by []
0.05/0.05	 joinable by a reduction of rules <[([(U0,1)],0),([(U0,1)],1),([],3),([],4)], [([],1)]>
0.05/0.05	 joinable by a reduction of rules <[([(U0,1)],0),([],3),([(U1,1)],1),([],4)], []>
0.05/0.05	Satisfiable by 3>1,4,5>2; U0(2)U1(1,0); 3>1,4,5>2
0.05/0.05	Diagram Decreasing
0.05/0.05	Direct Methods: CR
0.05/0.05	
0.05/0.05	Combined result: CR
0.05/0.05	U(R) is confluent
0.05/0.05	R is deterministic, weakly left-linear and U(R) is confluent
0.05/0.05	/home/www/colo6-c703/cocoweb/session/c9l2hu6ptm1v0ic6b4oohpr3d1/JLAMP21CTRS_1.trs: Success(CR)
0.05/0.05	(5 msec.)