0.00/0.11	YES
0.00/0.11	(ignored inputs)COMMENT doi:10.1016/j.jlap.2009.08.001 [73] Example 16 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.11	Conditional Rewrite Rules:
0.00/0.11	   [ f(?x) -> c | a == b,
0.00/0.11	     g(?x,?x) -> g(f(a),f(b)) ]
0.00/0.11	Check whether all rules are type 3
0.00/0.11	OK
0.00/0.11	Check whether the input is deterministic
0.00/0.11	OK
0.00/0.11	Result of unraveling:
0.00/0.11	   [ f(?x) -> U0(a,?x),
0.00/0.11	     U0(b,?x) -> c,
0.00/0.11	     g(?x,?x) -> g(f(a),f(b)) ]
0.00/0.11	Check whether U(R) is terminating
0.00/0.11	failed to show termination
0.00/0.11	Check whether the input is weakly left-linear
0.00/0.11	OK
0.00/0.11	Conditional critical pairs (CCPs):
0.00/0.11	   [  ]
0.00/0.11	Check whether the input is almost orthogonale
0.00/0.11	not almost orthogonal
0.00/0.11	OK
0.00/0.11	Check U(R) is confluent
0.00/0.11	Rewrite Rules:
0.00/0.11	   [ f(?x) -> U0(a,?x),
0.00/0.11	     U0(b,?x) -> c,
0.00/0.11	     g(?x,?x) -> g(f(a),f(b)) ]
0.00/0.11	Apply Direct Methods...
0.00/0.11	Inner CPs:
0.00/0.11	   [  ]
0.00/0.11	Outer CPs:
0.00/0.11	   [  ]
0.00/0.11	Overlay, check Innermost Termination...
0.00/0.11	unknown Innermost Terminating
0.00/0.11	unknown Knuth & Bendix
0.00/0.11	not Left-Linear, Right-Linear
0.00/0.11	Simple-Right-Linear
0.00/0.11	Direct Methods: CR
0.00/0.11	
0.00/0.11	Combined result: CR
0.00/0.11	U(R) is confluent
0.00/0.11	R is deterministic, weakly left-linear and U(R) is confluent
0.00/0.11	/export/starexec/sandbox/benchmark/theBenchmark.trs: Success(CR)
0.00/0.11	(29 msec.)
0.00/0.11	EOF