Preparation for CASC HOL 2026 #1

[mezpusz]

FIrst batch of fixes and improvements in preparation for CASC HOL 2026.

1. Function definition introduction was adapted for HOL.
2. Backward simplifying indices (i.e. essentially SubstitutionTree::FastInstancesIterator) were adapted for HOL in somewhat inefficient way to avoid variable capture/loose DB indices.
3. A bug related to proxification (e.g. with --cnf_on_the_fly lazy_gen) was fixed, because proxification cannot handle type quantifiers. We simply don't proxify, but clausify such clauses instead of crashing.
4. A safeguard was added in term sharing to ensure that everything is appified when doing HOL
5. HOL sampler was adapted (for example, removing FMB options for now).

Multiple rounds of debug sampling TPTP did not show any related new errors (1 related to z3, 2 related to function definition inlining showed up, but these are in FOL).

Regression tests (run 0 is master, run 1 is this branch):

Testing 1 (-fdi 5):

Discount FOL
run 0 unsat: 5099 (0) sat: 878 (1) cputime: 67963.24 s instructions: 300768768 Mi memory: 2402548.99 MB
run 1 unsat: 5099 (0) sat: 877 (0) cputime: 67951.24 s instructions: 300764373 Mi memory: 2403903.48 MB

Otter FOL
run 0 unsat: 5448 (0) sat: 873 (0) cputime: 60802.40 s instructions: 293972229 Mi memory: 1592099.27 MB
run 1 unsat: 5448 (0) sat: 873 (0) cputime: 60791.79 s instructions: 293967069 Mi memory: 1592198.68 MB

Discount HOL
run 0 unsat: 1252 (15) sat: 1 (0) cputime: 14236.33 s instructions: 68655709 Mi memory: 301840.90 MB
run 1 unsat: 1690 (453) sat: 1 (0) cputime: 14082.85 s instructions: 59927145 Mi memory: 212328.85 MB

Otter HOL
run 0 unsat: 1373 (25) sat: 1 (0) cputime: 14229.10 s instructions: 66266612 Mi memory: 319064.22 MB
run 1 unsat: 1832 (484) sat: 1 (0) cputime: 13653.15 s instructions: 57393162 Mi memory: 246531.99 MB

Testing 2 (-bd all -bs on -bsr on -bsd on):

Discount FOL
run 0 unsat: 9216 (0) sat: 1037 (0) cputime: 58293.40 s instructions: 223371056 Mi memory: 1366568.48 MB
run 1 unsat: 9216 (0) sat: 1037 (0) cputime: 58086.35 s instructions: 223345152 Mi memory: 1367555.50 MB

Otter FOL
run 0 unsat: 8647 (0) sat: 1042 (0) cputime: 58066.52 s instructions: 232982427 Mi memory: 870111.44 MB
run 1 unsat: 8649 (2) sat: 1043 (1) cputime: 57886.80 s instructions: 232934534 Mi memory: 871439.43 MB

Discount HOL
run 0 unsat: 2215 (8) sat: 1 (0) cputime: 8674.66 s instructions: 42609874 Mi memory: 108997.51 MB
run 1 unsat: 2210 (3) sat: 1 (0) cputime: 8777.30 s instructions: 44130364 Mi memory: 110371.84 MB

Otter HOL
run 0 unsat: 2048 (19) sat: 1 (0) cputime: 8348.47 s instructions: 43514643 Mi memory: 88434.15 MB
run 1 unsat: 2036 (7) sat: 1 (0) cputime: 8642.95 s instructions: 46776999 Mi memory: 85916.72 MB

(for the last 2 a bunch of crashes were eliminated, this does not show up on the stats)

Testing 3 (-cnfonf lazy_gen):

Discount HOL
run 0 unsat: 1093 (0) sat: 1 (0) cputime: 13956.15 s instructions: 72164295 Mi memory: 119783.33 MB
run 1 unsat: 1121 (28) sat: 1 (0) cputime: 14491.28 s instructions: 75106955 Mi memory: 123262.69 MB

Otter HOL
run 0 unsat: 1080 (0) sat: 1 (0) cputime: 14095.52 s instructions: 71881760 Mi memory: 92542.40 MB
run 1 unsat: 1111 (31) sat: 1 (0) cputime: 14626.63 s instructions: 74767708 Mi memory: 94973.46 MB