[mezpusz]

This is a remnant of the HOL branch that we should merge, for completeness.

As usual, we get potentially many unifiers so I had to add one more level of iterations to equality factoring and
cleaned up the code a bit in the process.

We lose a few problems -- as already observed, HOL unification seems less useful than FOL unification and we also slow things down a tiny bit for all (including pure FOL) benchmarks.

Discount FOL TPTP

run 0 unsat: 9292 (0) sat: 1044 (0) cputime: 60480.62 s instructions: 221609469 Mi memory: 1787869.09 MB
run 1 unsat: 9292 (0) sat: 1044 (0) cputime: 60365.15 s instructions: 221616245 Mi memory: 1787358.21 MB

Otter FOL TPTP

run 0 unsat: 9399 (1) sat: 1027 (0) cputime: 65575.77 s instructions: 221404233 Mi memory: 2023168.04 MB
run 1 unsat: 9398 (0) sat: 1027 (0) cputime: 65495.45 s instructions: 221412464 Mi memory: 2022615.64 MB

Discount HOL TPTP

run 0 unsat: 2118 (9) sat: 1 (0) cputime: 10197.71 s instructions: 49688135 Mi memory: 209686.42 MB
run 1 unsat: 2113 (4) sat: 1 (0) cputime: 10188.57 s instructions: 49658091 Mi memory: 210849.95 MB

Otter HOL TPTP

run 0 unsat: 2091 (9) sat: 1 (0) cputime: 10356.22 s instructions: 50189754 Mi memory: 276131.06 MB
run 1 unsat: 2091 (9) sat: 1 (0) cputime: 10358.64 s instructions: 50179828 Mi memory: 280188.26 MB

[mezpusz]

I double checked the lost problem in Otter FOL TPTP and it had the same proof for both master and this branch.

[easychair]

What I learned from Spider experiments: if you run Vampire over TPTP twice with the same options, the set of solved problems is never the same (even for Otter and Discount) - runtimes may differ. The difference is especially large when using FMB: here may easily beover 10% difference. If you believe a simple problem becomes unsolvable, I would make a few runs to check. A

…

On Mon, 19 Oct 2026 at 08:59, Márton Hajdu ***@***.***> wrote: *mezpusz* left a comment (vprover/vampire#1024) <#1024 (comment)> I double checked the lost problem in Otter FOL TPTP and it had the same proof for both master and this branch. — Reply to this email directly, view it on GitHub <#1024?email_source=notifications&email_token=ABVY4BPKUVCEHOVALW7VASL5UXCWNA5CNFSNUABFM5UWIORPF5TWS5BNNB2WEL2JONZXKZKDN5WW2ZLOOQXTMMRWGI2TAMZVGE4KM4TFMFZW63VKON2WE43DOJUWEZLEUVSXMZLOOSWGM33PORSXEX3DNRUWG2Y#issuecomment-6262503518>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABVY4BIIEPBTIRJFFFYZ7DL5UXCWNAVCNFSNUABEKJSXA33TNF2G64TZHMYTQMBWG44TCMB3JFZXG5LFHM2TQOBVGE3DOMZXG2QXMAQ> . Triage notifications, keep track of coding agent tasks and review pull requests on the go with GitHub Mobile for iOS <https://github.com/notifications/mobile/ios/ABVY4BMI7DPFBNEWFUZGQLT5UXCWNA5CNFSNUABFM5UWIORPF5TWS5BNNB2WEL2JONZXKZKDN5WW2ZLOOQXTMMRWGI2TAMZVGE4KM4TFMFZW63VKON2WE43DOJUWEZLEUVSXMZLOOSVGM33PORSXEX3JN5ZQ> and Android <https://github.com/notifications/mobile/android/ABVY4BO5GKKLMOXOYO3NTAD5UXCWNA5CNFSNUABFM5UWIORPF5TWS5BNNB2WEL2JONZXKZKDN5WW2ZLOOQXTMMRWGI2TAMZVGE4KM4TFMFZW63VKON2WE43DOJUWEZLEUVSXMZLOOSXGM33PORSXEX3BNZSHE33JMQ>. Download it today! You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[mezpusz]

I agree with you but the instruction limit -i I found relatively stable. In this case, we probably slow the execution down a tiny bit and this is why it flipped, not because of noise.