0.00/0.11	YES
0.00/0.11	(ignored inputs)COMMENT doi:10.1007/978-1-4757-3661-8 [18] Example 7.2.45 submitted by: Raul Gutierrez and Salvador Lucas
0.00/0.11	Conditional Rewrite Rules:
0.00/0.11	   [ a -> a | b == ?x,c == ?x,
0.00/0.11	     b -> d | d == ?x,e == ?x,
0.00/0.11	     c -> d | d == ?x,e == ?x ]
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	   [ a -> U0(b),
0.00/0.11	     U0(?x) -> U1(c,?x),
0.00/0.11	     U1(?x,?x) -> a,
0.00/0.11	     b -> U2(d),
0.00/0.11	     U2(?x) -> U3(e,?x),
0.00/0.11	     U3(?x,?x) -> d,
0.00/0.11	     c -> U4(d),
0.00/0.11	     U4(?x) -> U5(e,?x),
0.00/0.11	     U5(?x,?x) -> d ]
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	OK
0.00/0.11	Check whether the input is properly oriented
0.00/0.11	OK
0.00/0.11	Check whether the input is right-stable
0.00/0.11	not right-stable
0.00/0.11	OK
0.00/0.11	Check U(R) is confluent
0.00/0.11	Rewrite Rules:
0.00/0.11	   [ a -> U0(b),
0.00/0.11	     U0(?x) -> U1(c,?x),
0.00/0.11	     U1(?x,?x) -> a,
0.00/0.11	     b -> U2(d),
0.00/0.11	     U2(?x) -> U3(e,?x),
0.00/0.11	     U3(?x,?x) -> d,
0.00/0.11	     c -> U4(d),
0.00/0.11	     U4(?x) -> U5(e,?x),
0.00/0.11	     U5(?x,?x) -> d ]
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	(67 msec.)
0.00/0.12	EOF