Seems I shared the wrong message. But HOL-ex also runs fine. Larry > On 31 Aug 2024, at 13:22, Manuel Eberl <manuel at pruvisto.org> wrote: > > In the example you linked, HOL-ex is the one that fails. No idea why; I don't know anything about "refute".