YES
(ignored inputs)COMMENT the following rules are removed from the original TRS g ( f ( f ( h ( x ) ) ) , y ) -> g ( g ( f ( h ( x ) ) , f ( f ( h ( x ) ) ) ) , y ) f ( x ) -> g ( x , f ( x ) ) h ( x ) -> g ( f ( x ) , x ) g ( x , y ) -> h ( g ( f ( x ) , f ( y ) ) )
: CR

Combined result: CR
/tmp/file57EVfn.trs: Success(CR)
(0 msec.)