(in-package "ACL2")
(assert-event (identical-files-p "irrelevant-formals-log.txt" "irrelevant-formals-log.out"))