YES
(ignored inputs)COMMENT the following rules are removed from the original TRS F ( G ( x , A ( ) , B ( ) ) ) -> x G ( F ( H ( C ( ) , D ( ) ) ) , x , y ) -> H ( K1 ( x ) , K2 ( y ) ) K1 ( A ( ) ) -> C ( ) K2 ( B ( ) ) -> D ( )
: CR

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