(ignored inputs)COMMENT TPDB SRS_Standard/Secret_06_SRS/secr6
Rewrite Rules:
   [ a(b(c(?x))) -> c(c(c(b(b(b(a(a(a(?x))))))))),
     c(b(?x)) -> a(a(a(?x))),
     a(?x) -> ?x,
     b(?x) -> ?x,
     c(?x) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ a(b(a(a(a(?x_1))))) = c(c(c(b(b(b(a(a(a(b(?x_1)))))))))),
     a(c(?x)) = c(c(c(b(b(b(a(a(a(?x))))))))),
     a(b(?x_4)) = c(c(c(b(b(b(a(a(a(?x_4))))))))),
     c(?x_3) = a(a(a(?x_3))) ]
Outer CPs:
   [ c(c(c(b(b(b(a(a(a(?x))))))))) = b(c(?x)),
     a(a(a(?x_1))) = b(?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:
   [ a(a(a(?x_2))) = c(c(c(b(b(b(a(a(a(b(?x_2)))))))))),
     ?x = c(c(c(b(b(b(a(a(a(?x))))))))),
     c(?x) = c(c(c(b(b(b(a(a(a(?x))))))))),
     b(a(a(a(?x_2)))) = c(c(c(b(b(b(a(a(a(b(?x_2)))))))))),
     b(?x) = c(c(c(b(b(b(a(a(a(?x))))))))),
     a(a(a(a(?x_2)))) = c(c(c(b(b(b(a(a(a(b(?x_2)))))))))),
     a(?x) = c(c(c(b(b(b(a(a(a(?x))))))))),
     b(c(?x)) = c(c(c(b(b(b(a(a(a(?x))))))))),
     a(c(?x)) = c(c(c(b(b(b(a(a(a(?x))))))))),
     a(b(a(a(a(?x_2))))) = c(c(c(b(b(b(a(a(a(b(?x_2)))))))))),
     a(b(?x)) = c(c(c(b(b(b(a(a(a(?x))))))))),
     ?x = a(a(a(?x))),
     b(?x) = a(a(a(?x))),
     c(?x) = a(a(a(?x))),
     c(c(c(b(b(b(a(a(a(?x))))))))) = a(b(a(a(a(?x))))),
     c(c(c(b(b(b(a(a(a(b(?x)))))))))) = a(b(a(a(a(?x))))),
     c(c(c(b(b(b(a(a(a(?x_1))))))))) = b(c(?x_1)),
     c(c(c(b(b(b(a(a(a(?x_2))))))))) = a(c(?x_2)),
     a(a(a(?x))) = c(?x),
     a(a(a(?x_2))) = b(?x_2),
     c(c(c(b(b(b(a(a(a(?x))))))))) = a(b(?x)) ]
Okui (Simultaneous CPs)
Direct Methods: CR

Combined result: CR
938.trs: Success(CR)
YES
(212 msec.)