YES (ignored inputs)COMMENT TPDB SRS_Standard/Trafo_06/un02 Rewrite Rules: [ b(a(a(b(b(?x))))) -> b(a(a(a(a(b(b(?x))))))), b(a(b(b(?x)))) -> b(b(?x)), b(a(b(a(a(a(a(b(?x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(?x)))))))))))))))))))))), b(a(a(b(a(a(a(a(b(?x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(?x))))))))))))))), b(a(a(a(b(a(a(a(a(b(?x)))))))))) -> b(?x) ] Apply Direct Methods... Inner CPs: [ b(a(a(b(b(b(?x_1)))))) = b(a(a(a(a(b(b(a(b(b(?x_1)))))))))), b(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(?x_2)))))))))))))))))))))))))) = b(a(a(a(a(b(b(a(b(a(a(a(a(b(?x_2)))))))))))))), b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(?x_3))))))))))))))))))) = b(a(a(a(a(b(b(a(a(b(a(a(a(a(b(?x_3))))))))))))))), b(a(a(b(b(?x_4))))) = b(a(a(a(a(b(b(a(a(a(b(a(a(a(a(b(?x_4)))))))))))))))), b(a(b(b(a(a(a(a(b(b(?x)))))))))) = b(b(a(a(b(b(?x)))))), b(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(?x_2))))))))))))))))))))))))) = b(b(a(b(a(a(a(a(b(?x_2))))))))), b(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(?x_3)))))))))))))))))) = b(b(a(a(b(a(a(a(a(b(?x_3)))))))))), b(a(b(b(?x_4)))) = b(b(a(a(a(b(a(a(a(a(b(?x_4))))))))))), b(a(b(a(a(a(a(b(a(a(a(a(b(b(?x)))))))))))))) = b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(?x)))))))))))))))))))))))))), b(a(b(a(a(a(a(b(b(?x_1))))))))) = b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(b(?x_1))))))))))))))))))))))))), b(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(?x_3)))))))))))))))))))))) = b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(?x_3)))))))))))))))))))))))))))))), b(a(b(a(a(a(a(b(?x_4)))))))) = b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(?x_4))))))))))))))))))))))))))))))), b(a(a(b(a(a(a(a(b(a(a(a(a(b(b(?x))))))))))))))) = b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(?x))))))))))))))))))), b(a(a(b(a(a(a(a(b(b(?x_1)))))))))) = b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(b(?x_1)))))))))))))))))), b(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(?x_2)))))))))))))))))))))))))))))) = b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(?x_2)))))))))))))))))))))), b(a(a(b(a(a(a(a(b(?x_4))))))))) = b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(?x_4)))))))))))))))))))))))), b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(?x)))))))))))))))) = b(a(a(b(b(?x))))), b(a(a(a(b(a(a(a(a(b(b(?x_1))))))))))) = b(a(b(b(?x_1)))), b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(?x_2))))))))))))))))))))))))))))))) = b(a(b(a(a(a(a(b(?x_2)))))))), b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(?x_3)))))))))))))))))))))))) = b(a(a(b(a(a(a(a(b(?x_3))))))))), b(a(a(b(b(a(a(a(a(b(b(?x))))))))))) = b(a(a(a(a(b(b(a(a(b(b(?x))))))))))), b(a(b(b(b(?x))))) = b(b(a(b(b(?x))))), b(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(?x))))))))))))))))))))))))))))) = b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(?x))))))))))))))))))))))))))))), b(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(?x))))))))))))))))))))))) = b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(?x))))))))))))))))))))))), b(a(a(a(b(a(a(a(a(b(?x)))))))))) = b(a(a(a(b(a(a(a(a(b(?x)))))))))) ] Outer CPs: [ ] not Overlay, check Termination... unknown/not Terminating unknown Knuth & Bendix Linear unknown Development Closed Strongly Closed Direct Methods: CR Combined result: CR 978.trs: Success(CR) (21737 msec.)