YES
(ignored inputs)COMMENT TPDB SRS_Standard/ICFP_2010/264370
Rewrite Rules:
   [ 0(1(2(3(4(?x))))) -> 0(2(1(3(4(?x))))),
     0(5(1(2(4(3(?x)))))) -> 0(5(2(1(4(3(?x)))))),
     0(5(2(4(1(3(?x)))))) -> 0(1(5(2(4(3(?x)))))),
     0(5(3(1(2(4(?x)))))) -> 0(1(5(3(2(4(?x)))))),
     0(5(4(1(3(2(?x)))))) -> 0(5(4(3(1(2(?x)))))) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR

Combined result: CR
951.trs: Success(CR)
(0 msec.)