YES
af/ONE-SORTED/115.trs
Input rules:
   [ a1 -> b1,
     a1 -> c1,
     b1 -> b2,
     c1 -> c2,
     a2 -> b2,
     a2 -> c2,
     b2 -> b3,
     c2 -> c3,
     a3 -> b3,
     a3 -> c3,
     b3 -> b4,
     c3 -> c4,
     a4 -> b4,
     a4 -> c4,
     b4 -> b5,
     c4 -> c5,
     a5 -> b5,
     a5 -> c5,
     b5 -> b6,
     c5 -> c6,
     a6 -> b6,
     a6 -> c6,
     b6 -> b7,
     c6 -> c7,
     a7 -> b7,
     a7 -> c7,
     b7 -> b8,
     c7 -> c8,
     a8 -> b8,
     a8 -> c8,
     b8 -> b9,
     c8 -> c9,
     a9 -> b9,
     a9 -> c9,
     b9 -> b10,
     c9 -> c10,
     a10 -> b11,
     b10 -> b11,
     c10 -> b11 ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ a1 -> b1,
     a1 -> c1,
     b1 -> b2,
     c1 -> c2,
     a2 -> b2,
     a2 -> c2,
     b2 -> b3,
     c2 -> c3,
     a3 -> b3,
     a3 -> c3,
     b3 -> b4,
     c3 -> c4,
     a4 -> b4,
     a4 -> c4,
     b4 -> b5,
     c4 -> c5,
     a5 -> b5,
     a5 -> c5,
     b5 -> b6,
     c5 -> c6,
     a6 -> b6,
     a6 -> c6,
     b6 -> b7,
     c6 -> c7,
     a7 -> b7,
     a7 -> c7,
     b7 -> b8,
     c7 -> c8,
     a8 -> b8,
     a8 -> c8,
     b8 -> b9,
     c8 -> c9,
     a9 -> b9,
     a9 -> c9,
     b9 -> b10,
     c9 -> c10,
     a10 -> b11,
     b10 -> b11,
     c10 -> b11 ]
Constructor pattern: [b11]
Defined pattern: [a10,c10,b10,a9,c9,b9,a8,c8,b8,a7,c7,b7,a6,c6,b6,a5,c5,b5,a4,c4,b4,a3,c3,b3,a2,c2,b2,c1,b1,a1]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for a10:
   [ a10 -> b11 ]
candidate for c10:
   [ c10 -> b11 ]
candidate for b10:
   [ b10 -> b11 ]
candidate for a9:
   [ a9 -> b9 ]
   [ a9 -> c9 ]
candidate for c9:
   [ c9 -> c10 ]
candidate for b9:
   [ b9 -> b10 ]
candidate for a8:
   [ a8 -> b8 ]
   [ a8 -> c8 ]
candidate for c8:
   [ c8 -> c9 ]
candidate for b8:
   [ b8 -> b9 ]
candidate for a7:
   [ a7 -> b7 ]
   [ a7 -> c7 ]
candidate for c7:
   [ c7 -> c8 ]
candidate for b7:
   [ b7 -> b8 ]
candidate for a6:
   [ a6 -> b6 ]
   [ a6 -> c6 ]
candidate for c6:
   [ c6 -> c7 ]
candidate for b6:
   [ b6 -> b7 ]
candidate for a5:
   [ a5 -> b5 ]
   [ a5 -> c5 ]
candidate for c5:
   [ c5 -> c6 ]
candidate for b5:
   [ b5 -> b6 ]
candidate for a4:
   [ a4 -> b4 ]
   [ a4 -> c4 ]
candidate for c4:
   [ c4 -> c5 ]
candidate for b4:
   [ b4 -> b5 ]
candidate for a3:
   [ a3 -> b3 ]
   [ a3 -> c3 ]
candidate for c3:
   [ c3 -> c4 ]
candidate for b3:
   [ b3 -> b4 ]
candidate for a2:
   [ a2 -> b2 ]
   [ a2 -> c2 ]
candidate for c2:
   [ c2 -> c3 ]
candidate for b2:
   [ b2 -> b3 ]
candidate for c1:
   [ c1 -> c2 ]
candidate for b1:
   [ b1 -> b2 ]
candidate for a1:
   [ a1 -> b1 ]
   [ a1 -> c1 ]
Find a quasi-ordering ...
order successfully found
Precedence:
 a10 : Mul,  b1 : Mul,  a1 : Mul;
 c1 : Mul;
 c2 : Mul;
 a7 : Mul,  a4 : Mul;
 a2 : Mul;
 b2 : Mul,  a6 : Mul,  a3 : Mul;
 a9 : Mul,  a5 : Mul;
 c3 : Mul;
 c4 : Mul,  b3 : Mul;
 b4 : Mul;
 b5 : Mul;
 b6 : Mul,  a8 : Mul;
 c5 : Mul;
 c6 : Mul,  b7 : Mul;
 c7 : Mul,  b8 : Mul;
 c8 : Mul,  b9 : Mul;
 b10 : Mul;
 c9 : Mul;
 c10 : Mul;
 b11 : Mul;
Rules:
   [ a10 -> b11,
     c10 -> b11,
     b10 -> b11,
     a9 -> b9,
     c9 -> c10,
     b9 -> b10,
     a8 -> b8,
     c8 -> c9,
     b8 -> b9,
     a7 -> b7,
     c7 -> c8,
     b7 -> b8,
     a6 -> b6,
     c6 -> c7,
     b6 -> b7,
     a5 -> b5,
     c5 -> c6,
     b5 -> b6,
     a4 -> b4,
     c4 -> c5,
     b4 -> b5,
     a3 -> b3,
     c3 -> c4,
     b3 -> b4,
     a2 -> b2,
     c2 -> c3,
     b2 -> b3,
     c1 -> c2,
     b1 -> b2,
     a1 -> c1 ]
Conjectures:
   [ a1 = b1,
     a2 = c2,
     a3 = c3,
     a4 = c4,
     a5 = c5,
     a6 = c6,
     a7 = c7,
     a8 = c8,
     a9 = c9 ]
STEP 0
ES:
   [ a1 = b1,
     a2 = c2,
     a3 = c3,
     a4 = c4,
     a5 = c5,
     a6 = c6,
     a7 = c7,
     a8 = c8,
     a9 = c9 ]
HS:
   [ ]
ES0:
   [ b11 = b11,
     b11 = b11,
     b11 = b11,
     b11 = b11,
     b11 = b11,
     b11 = b11,
     b11 = b11,
     b11 = b11,
     b11 = b11 ]
HS0:
   [ ]
ES1:
   [ ]
HS1:
   [ ]
: Success(GCR)
(55 msec.)
0.06