0.00/0.15 YES 0.00/0.15 (ignored inputs)COMMENT TPDB SRS_Standard/Waldmann_06_SRS/jw4 0.00/0.15 Rewrite Rules: 0.00/0.15 [ b(a(b(b(?x)))) -> b(b(b(a(b(?x))))), 0.00/0.15 b(a(a(b(b(?x))))) -> b(a(b(b(a(a(b(?x))))))), 0.00/0.15 b(a(a(a(b(b(?x)))))) -> b(a(a(b(b(a(a(a(b(?x))))))))) ] 0.00/0.15 Apply Direct Methods... 0.00/0.15 Inner CPs: 0.00/0.15 [ b(a(b(b(a(b(b(a(a(b(?x_1)))))))))) = b(b(b(a(b(a(a(b(b(?x_1))))))))), 0.00/0.15 b(a(b(b(a(a(b(b(a(a(a(b(?x_2)))))))))))) = b(b(b(a(b(a(a(a(b(b(?x_2)))))))))), 0.00/0.15 b(a(a(b(b(b(b(a(b(?x))))))))) = b(a(b(b(a(a(b(a(b(b(?x)))))))))), 0.00/0.15 b(a(a(b(b(a(a(b(b(a(a(a(b(?x_2))))))))))))) = b(a(b(b(a(a(b(a(a(a(b(b(?x_2)))))))))))), 0.00/0.15 b(a(a(a(b(b(b(b(a(b(?x)))))))))) = b(a(a(b(b(a(a(a(b(a(b(b(?x)))))))))))), 0.00/0.15 b(a(a(a(b(b(a(b(b(a(a(b(?x_1)))))))))))) = b(a(a(b(b(a(a(a(b(a(a(b(b(?x_1))))))))))))), 0.00/0.15 b(a(b(b(b(b(a(b(?x)))))))) = b(b(b(a(b(a(b(b(?x)))))))), 0.00/0.15 b(a(a(b(b(a(b(b(a(a(b(?x))))))))))) = b(a(b(b(a(a(b(a(a(b(b(?x))))))))))), 0.00/0.15 b(a(a(a(b(b(a(a(b(b(a(a(a(b(?x)))))))))))))) = b(a(a(b(b(a(a(a(b(a(a(a(b(b(?x)))))))))))))) ] 0.00/0.15 Outer CPs: 0.00/0.15 [ ] 0.00/0.15 not Overlay, check Termination... 0.00/0.15 unknown/not Terminating 0.00/0.15 unknown Knuth & Bendix 0.00/0.15 Linear 0.00/0.15 unknown Development Closed 0.00/0.15 Strongly Closed 0.00/0.15 Direct Methods: CR 0.00/0.15 0.00/0.15 Combined result: CR 0.00/0.15 /export/starexec/sandbox/benchmark/theBenchmark.trs: Success(CR) 0.00/0.15 (91 msec.) 0.00/0.15 EOF