YES (ignored inputs)COMMENT the following rules are removed from the original TRS f ( a ( ) , f ( a ( ) , f ( a ( ) , f ( a ( ) , y ) ) ) ) -> f ( a ( ) , f ( a ( ) , f ( a ( ) , g ( y , f ( a ( ) , y ) ) ) ) ) f ( x , y ) -> g ( y , f ( x , y ) ) : CR Combined result: CR /tmp/file5c2Taf.trs: Success(CR) (0 msec.)