MAYBE
af/ONE-SORTED/116.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 -> b7,
     b7 -> b1,
     b7 -> c1 ]
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 -> b7,
     b7 -> b1,
     b7 -> c1 ]
Constructor pattern: []
Defined pattern: [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 b7:
   [ b7 -> b1 ]
   [ b7 -> c1 ]
candidate for a6:
   [ a6 -> b6 ]
   [ a6 -> c6 ]
candidate for c6:
   [ c6 -> b7 ]
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 ...
failed to find an ordering.
Try to supplement auxiliary rules.
{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}Supplemented Rules:
   [ ]
failed to supplement auxiliary rules
check Non-Ground-Confluence...
ground constructor terms for instantiation: {}
ground terms for instantiation: {a1:o}
obtain 31 rules by 3 steps unfolding
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (failure)
: Failure(unknown)
(1769 msec.)
2.92