(include-book "models/jvm/m1/m1-story" :dir :system)
(certify-book "fact-out" ?)