YES
(ignored inputs)COMMENT reduction failed
Rewrite Rules:
   [ a(?x) -> ?x,
     a(b(?x)) -> c(b(b(a(a(?x))))),
     b(?x) -> c(?x),
     c(c(?x)) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ a(c(?x_2)) = c(b(b(a(a(?x_2))))),
     c(?x) = c(?x) ]
Outer CPs:
   [ b(?x_1) = c(b(b(a(a(?x_1))))) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ c(b(b(a(a(?x_1))))) = b(?x_1),
     c(?x) = c(b(b(a(a(?x))))),
     b(?x) = c(b(b(a(a(?x))))),
     a(c(?x)) = c(b(b(a(a(?x))))),
     c(b(b(a(a(?x))))) = a(c(?x)),
     c(?x_1) = c(?x_1),
     ?x_1 = c(c(?x_1)) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <a(c(?x_2)), c(b(b(a(a(?x_2)))))> by Rules <2, 1> preceded by [(a,1)]
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1),(b,1),(b,1)],0),([(c,1),(b,1)],2),([(c,1)],2),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1),(b,1),(b,1)],0),([(c,1),(b,1)],2),([(c,1)],2),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1),(b,1),(b,1)],0),([(c,1)],2),([(c,1),(c,1)],2),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1),(b,1),(b,1)],0),([(c,1)],2),([(c,1),(c,1)],2),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1),(b,1),(b,1)],0),([(c,1)],2),([],3),([],2)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1),(b,1)],2),([(c,1),(b,1),(c,1)],0),([(c,1)],2),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1),(b,1)],2),([(c,1),(b,1),(c,1)],0),([(c,1)],2),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1),(b,1)],2),([(c,1)],2),([(c,1),(c,1),(c,1)],0),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1),(b,1)],2),([(c,1)],2),([(c,1),(c,1),(c,1)],0),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1),(b,1)],2),([(c,1)],2),([(c,1)],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1),(b,1)],2),([(c,1)],2),([],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1)],2),([(c,1),(c,1),(b,1)],0),([(c,1),(c,1)],2),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1)],2),([(c,1),(c,1),(b,1)],0),([(c,1),(c,1)],2),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1)],2),([(c,1),(c,1),(b,1)],0),([],3),([],2)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1)],2),([(c,1),(c,1)],2),([(c,1),(c,1),(c,1)],0),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1)],2),([(c,1),(c,1)],2),([(c,1),(c,1),(c,1)],0),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1)],2),([(c,1),(c,1)],2),([(c,1)],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1)],2),([(c,1),(c,1)],2),([],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1)],2),([],3),([(b,1)],0),([],2)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1),(a,1)],0),([(c,1)],2),([],3),([],2),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1),(b,1),(b,1)],0),([(c,1),(b,1)],2),([(c,1)],2),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1),(b,1),(b,1)],0),([(c,1),(b,1)],2),([(c,1)],2),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1),(b,1),(b,1)],0),([(c,1)],2),([(c,1),(c,1)],2),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1),(b,1),(b,1)],0),([(c,1)],2),([(c,1),(c,1)],2),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1),(b,1),(b,1)],0),([(c,1)],2),([],3),([],2)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1),(b,1)],2),([(c,1),(b,1),(c,1)],0),([(c,1)],2),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1),(b,1)],2),([(c,1),(b,1),(c,1)],0),([(c,1)],2),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1),(b,1)],2),([(c,1)],2),([(c,1),(c,1),(c,1)],0),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1),(b,1)],2),([(c,1)],2),([(c,1),(c,1),(c,1)],0),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1),(b,1)],2),([(c,1)],2),([(c,1)],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1),(b,1)],2),([(c,1)],2),([],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1)],2),([(c,1),(c,1),(b,1)],0),([(c,1),(c,1)],2),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1)],2),([(c,1),(c,1),(b,1)],0),([(c,1),(c,1)],2),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1)],2),([(c,1),(c,1),(b,1)],0),([],3),([],2)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1)],2),([(c,1),(c,1)],2),([(c,1),(c,1),(c,1)],0),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1)],2),([(c,1),(c,1)],2),([(c,1),(c,1),(c,1)],0),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1)],2),([(c,1),(c,1)],2),([(c,1)],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1)],2),([(c,1),(c,1)],2),([],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1)],2),([],3),([(b,1)],0),([],2)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1),(b,1)],0),([(c,1)],2),([],3),([],2),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1),(b,1),(c,1),(a,1)],0),([(c,1),(b,1),(c,1)],0),([(c,1)],2),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1),(b,1),(c,1),(a,1)],0),([(c,1),(b,1),(c,1)],0),([(c,1)],2),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1),(b,1),(c,1),(a,1)],0),([(c,1)],2),([(c,1),(c,1),(c,1)],0),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1),(b,1),(c,1),(a,1)],0),([(c,1)],2),([(c,1),(c,1),(c,1)],0),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1),(b,1),(c,1),(a,1)],0),([(c,1)],2),([(c,1)],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1),(b,1),(c,1),(a,1)],0),([(c,1)],2),([],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1),(b,1),(c,1)],0),([(c,1),(b,1),(c,1)],0),([(c,1)],2),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1),(b,1),(c,1)],0),([(c,1),(b,1),(c,1)],0),([(c,1)],2),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1),(b,1),(c,1)],0),([(c,1)],2),([(c,1),(c,1),(c,1)],0),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1),(b,1),(c,1)],0),([(c,1)],2),([(c,1),(c,1),(c,1)],0),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1),(b,1),(c,1)],0),([(c,1)],2),([(c,1)],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1),(b,1),(c,1)],0),([(c,1)],2),([],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1)],2),([(c,1),(c,1),(c,1),(a,1)],0),([(c,1),(c,1),(c,1)],0),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1)],2),([(c,1),(c,1),(c,1),(a,1)],0),([(c,1),(c,1),(c,1)],0),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1)],2),([(c,1),(c,1),(c,1),(a,1)],0),([(c,1)],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1)],2),([(c,1),(c,1),(c,1),(a,1)],0),([],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1)],2),([(c,1),(c,1),(c,1)],0),([(c,1),(c,1),(c,1)],0),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1)],2),([(c,1),(c,1),(c,1)],0),([(c,1),(c,1),(c,1)],0),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1)],2),([(c,1),(c,1),(c,1)],0),([(c,1)],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1)],2),([(c,1),(c,1),(c,1)],0),([],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1)],2),([(c,1)],3),([(c,1),(a,1)],0),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1)],2),([(c,1)],3),([(c,1)],0),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1)],2),([],3),([(c,1),(a,1)],0),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1),(b,1)],2),([(c,1)],2),([],3),([(c,1)],0),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1),(a,1)],0),([(c,1),(c,1),(b,1)],0),([(c,1),(c,1)],2),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1),(a,1)],0),([(c,1),(c,1),(b,1)],0),([(c,1),(c,1)],2),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1),(a,1)],0),([(c,1),(c,1),(b,1)],0),([],3),([],2)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1),(a,1)],0),([(c,1),(c,1)],2),([(c,1),(c,1),(c,1)],0),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1),(a,1)],0),([(c,1),(c,1)],2),([(c,1),(c,1),(c,1)],0),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1),(a,1)],0),([(c,1),(c,1)],2),([(c,1)],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1),(a,1)],0),([(c,1),(c,1)],2),([],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1),(a,1)],0),([],3),([(b,1)],0),([],2)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1),(a,1)],0),([],3),([],2),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1)],0),([(c,1),(c,1),(b,1)],0),([(c,1),(c,1)],2),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1)],0),([(c,1),(c,1),(b,1)],0),([(c,1),(c,1)],2),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1)],0),([(c,1),(c,1),(b,1)],0),([],3),([],2)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1)],0),([(c,1),(c,1)],2),([(c,1),(c,1),(c,1)],0),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1)],0),([(c,1),(c,1)],2),([(c,1),(c,1),(c,1)],0),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1)],0),([(c,1),(c,1)],2),([(c,1)],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1)],0),([(c,1),(c,1)],2),([],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1)],0),([],3),([(b,1)],0),([],2)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1),(b,1)],0),([],3),([],2),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1)],2),([(c,1),(c,1),(c,1),(a,1)],0),([(c,1),(c,1),(c,1)],0),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1)],2),([(c,1),(c,1),(c,1),(a,1)],0),([(c,1),(c,1),(c,1)],0),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1)],2),([(c,1),(c,1),(c,1),(a,1)],0),([(c,1)],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1)],2),([(c,1),(c,1),(c,1),(a,1)],0),([],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1)],2),([(c,1),(c,1),(c,1)],0),([(c,1),(c,1),(c,1)],0),([(c,1)],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1)],2),([(c,1),(c,1),(c,1)],0),([(c,1),(c,1),(c,1)],0),([],3)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1)],2),([(c,1),(c,1),(c,1)],0),([(c,1)],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1)],2),([(c,1),(c,1),(c,1)],0),([],3),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1)],2),([(c,1)],3),([(c,1),(a,1)],0),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1)],2),([(c,1)],3),([(c,1)],0),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1)],2),([],3),([(c,1),(a,1)],0),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([(c,1),(c,1)],2),([],3),([(c,1)],0),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([],3),([(b,1),(a,1)],0),([(b,1)],0),([],2)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([],3),([(b,1),(a,1)],0),([],2),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([],3),([(b,1)],0),([(b,1)],0),([],2)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([],3),([(b,1)],0),([],2),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([],3),([],2),([(c,1),(a,1)],0),([(c,1)],0)]>
 joinable by a reduction of rules <[([],0)], [([(c,1)],2),([],3),([],2),([(c,1)],0),([(c,1)],0)]>
Critical Pair <c(?x), c(?x)> by Rules <3, 3> preceded by [(c,1)]
 joinable by a reduction of rules <[], []>
Critical Pair <c(b(b(a(a(?x_1))))), b(?x_1)> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[([(c,1),(b,1),(b,1),(a,1)],0),([(c,1),(b,1),(b,1)],0),([(c,1)],2),([],3)], []>
 joinable by a reduction of rules <[([(c,1),(b,1),(b,1),(a,1)],0),([(c,1)],2),([(c,1),(c,1),(b,1)],0),([],3)], []>
 joinable by a reduction of rules <[([(c,1),(b,1),(b,1),(a,1)],0),([(c,1)],2),([],3),([(b,1)],0)], []>
 joinable by a reduction of rules <[([(c,1),(b,1),(b,1)],0),([(c,1),(b,1),(b,1)],0),([(c,1)],2),([],3)], []>
 joinable by a reduction of rules <[([(c,1),(b,1),(b,1)],0),([(c,1)],2),([(c,1),(c,1),(b,1)],0),([],3)], []>
 joinable by a reduction of rules <[([(c,1),(b,1),(b,1)],0),([(c,1)],2),([],3),([(b,1)],0)], []>
 joinable by a reduction of rules <[([(c,1)],2),([(c,1),(c,1),(b,1),(a,1)],0),([(c,1),(c,1),(b,1)],0),([],3)], []>
 joinable by a reduction of rules <[([(c,1)],2),([(c,1),(c,1),(b,1),(a,1)],0),([],3),([(b,1)],0)], []>
 joinable by a reduction of rules <[([(c,1)],2),([(c,1),(c,1),(b,1)],0),([(c,1),(c,1),(b,1)],0),([],3)], []>
 joinable by a reduction of rules <[([(c,1)],2),([(c,1),(c,1),(b,1)],0),([],3),([(b,1)],0)], []>
 joinable by a reduction of rules <[([(c,1)],2),([],3),([(b,1),(a,1)],0),([(b,1)],0)], []>
 joinable by a reduction of rules <[([(c,1)],2),([],3),([(b,1)],0),([(b,1)],0)], []>
Satisfiable by 2>1>4,3; a(0)b(0)c(0); 1>2>3,4
Diagram Decreasing
Direct Methods: CR

Combined result: CR
/tmp/filejhDMCx.trs: Success(CR)
(106 msec.)