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