%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV775_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:19:29 PM UTC 2026 % Result : Timeout 301.25s 43.11s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV775_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.19 % Computer : n018.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 12:33:40 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.22 Running first-order theorem proving % 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.81/1.68 % (3345559)Detected formulas, will run a generic FOF schedule. % 5.81/1.68 % (3345564)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=714731818:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 5.81/1.68 % (3345568)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2313931436:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 5.81/1.68 % (3345566)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=52481431:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 5.81/1.68 % (3345567)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2628738899:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 5.81/1.68 % (3345565)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=153107091:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 5.81/1.68 % (3345567)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.81/1.68 % (3345566)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.81/1.68 % (3345570)dis-21_1_sil=8000:lcm=predicate:random_seed=1633500024:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 5.81/1.68 % (3345569)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3283263091:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 5.81/1.68 % (3345568)Instruction limit reached! % 5.81/1.68 % (3345568)------------------------------ % 5.81/1.68 % (3345568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.81/1.68 % (3345568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.81/1.68 % (3345568)CaDiCaL version: 2.1.3 % 5.81/1.68 % (3345568)Termination reason: Instruction limit % 5.81/1.68 % (3345568)Termination phase: Saturation % 5.81/1.68 % (3345568)Time elapsed: 0.070 s % 5.81/1.68 % (3345568)Peak memory usage: 89 MB % 5.81/1.68 % (3345568)Instructions burned: 120 (million) % 5.81/1.68 % (3345567)Instruction limit reached! % 5.81/1.68 % (3345567)------------------------------ % 5.81/1.68 % (3345567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.81/1.68 % (3345567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.81/1.68 % (3345567)CaDiCaL version: 2.1.3 % 5.81/1.68 % (3345567)Termination reason: Instruction limit % 5.81/1.68 % (3345567)Termination phase: Saturation % 5.81/1.68 % (3345567)Time elapsed: 0.064 s % 5.81/1.68 % (3345567)Peak memory usage: 89 MB % 5.81/1.68 % (3345567)Instructions burned: 110 (million) % 5.81/1.68 % (3345570)Instruction limit reached! % 5.81/1.68 % (3345570)------------------------------ % 5.81/1.68 % (3345570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.81/1.68 % (3345570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.81/1.68 % (3345570)CaDiCaL version: 2.1.3 % 5.81/1.68 % (3345570)Termination reason: Instruction limit % 5.81/1.68 % (3345570)Termination phase: Saturation % 5.81/1.68 % (3345570)Time elapsed: 0.072 s % 5.81/1.68 % (3345570)Peak memory usage: 89 MB % 5.81/1.68 % (3345570)Instructions burned: 129 (million) % 5.81/1.68 % (3345569)Instruction limit reached! % 5.81/1.68 % (3345569)------------------------------ % 5.81/1.68 % (3345569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.81/1.68 % (3345569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.81/1.68 % (3345569)CaDiCaL version: 2.1.3 % 5.81/1.68 % (3345569)Termination reason: Instruction limit % 5.81/1.68 % (3345569)Termination phase: Saturation % 5.81/1.68 % (3345569)Time elapsed: 0.087 s % 5.81/1.68 % (3345569)Peak memory usage: 89 MB % 5.81/1.68 % (3345569)Instructions burned: 139 (million) % 5.81/1.68 % Exception at run slice level % 5.81/1.68 User error: GNN currently only supports monomorphic FOL. % 5.81/1.68 % (3345579)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1936175092:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 5.81/1.68 % (3345578)lrs+10_1_sil=8000:sp=occurrence:random_seed=1270277671:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 5.81/1.68 % (3345580)lrs+1011_1_sil=32000:sp=occurrence:random_seed=236782766:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 6.92/1.89 % (3345581)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2487672682:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 6.92/1.89 % (3345582)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3683013146:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi) % 6.92/1.89 % (3345579)Instruction limit reached! % 6.92/1.89 % (3345579)------------------------------ % 6.92/1.89 % (3345579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.92/1.89 % (3345579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.92/1.89 % (3345579)CaDiCaL version: 2.1.3 % 6.92/1.89 % (3345579)Termination reason: Instruction limit % 6.92/1.89 % (3345579)Termination phase: Saturation % 6.92/1.89 % (3345579)Time elapsed: 0.087 s % 6.92/1.89 % (3345579)Peak memory usage: 90 MB % 6.92/1.89 % (3345579)Instructions burned: 158 (million) % 6.92/1.89 % (3345582)Instruction limit reached! % 6.92/1.89 % (3345582)------------------------------ % 6.92/1.89 % (3345582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.92/1.89 % (3345582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.92/1.89 % (3345582)CaDiCaL version: 2.1.3 % 6.92/1.89 % (3345582)Termination reason: Instruction limit % 6.92/1.89 % (3345582)Termination phase: Saturation % 6.92/1.89 % (3345582)Time elapsed: 0.082 s % 6.92/1.89 % (3345582)Peak memory usage: 89 MB % 6.92/1.89 % (3345582)Instructions burned: 296 (million) % 6.92/1.89 % (3345578)Instruction limit reached! % 6.92/1.89 % (3345578)------------------------------ % 6.92/1.89 % (3345578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.92/1.89 % (3345578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.92/1.89 % (3345578)CaDiCaL version: 2.1.3 % 6.92/1.89 % (3345578)Termination reason: Instruction limit % 6.92/1.89 % (3345578)Termination phase: Saturation % 6.92/1.89 % (3345578)Time elapsed: 0.169 s % 6.92/1.89 % (3345578)Peak memory usage: 90 MB % 6.92/1.89 % (3345578)Instructions burned: 286 (million) % 6.92/1.89 % Exception at run slice level % 6.92/1.89 User error: GNN currently only supports monomorphic FOL. % 6.92/1.89 % Exception at run slice level % 6.92/1.89 User error: GNN currently only supports monomorphic FOL. % 6.92/1.89 % (3345581)Instruction limit reached! % 6.92/1.89 % (3345581)------------------------------ % 6.92/1.89 % (3345581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.92/1.89 % (3345581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.92/1.89 % (3345581)CaDiCaL version: 2.1.3 % 6.92/1.89 % (3345581)Termination reason: Instruction limit % 6.92/1.89 % (3345581)Termination phase: Saturation % 6.92/1.89 % (3345581)Time elapsed: 0.138 s % 6.92/1.89 % (3345581)Peak memory usage: 90 MB % 6.92/1.89 % (3345581)Instructions burned: 249 (million) % 6.92/1.89 % (3345580)Instruction limit reached! % 6.92/1.89 % (3345580)------------------------------ % 6.92/1.89 % (3345580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.92/1.89 % (3345580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.92/1.89 % (3345580)CaDiCaL version: 2.1.3 % 6.92/1.89 % (3345580)Termination reason: Instruction limit % 6.92/1.89 % (3345580)Termination phase: Saturation % 6.92/1.89 % (3345580)Time elapsed: 0.194 s % 6.92/1.89 % (3345580)Peak memory usage: 91 MB % 6.92/1.89 % (3345580)Instructions burned: 325 (million) % 6.92/1.89 % (3345589)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1042033389:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi) % 6.92/1.89 % (3345588)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3067984376:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 6.92/1.89 % (3345589)Instruction limit reached! % 6.92/1.89 % (3345589)------------------------------ % 6.92/1.89 % (3345589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.92/1.89 % (3345589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.92/1.89 % (3345589)CaDiCaL version: 2.1.3 % 6.92/1.89 % (3345589)Termination reason: Instruction limit % 6.92/1.89 % (3345589)Termination phase: Saturation % 6.92/1.89 % (3345589)Time elapsed: 0.033 s % 6.92/1.89 % (3345589)Peak memory usage: 89 MB % 6.92/1.89 % (3345589)Instructions burned: 114 (million) % 6.92/1.89 % (3345590)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1850801056:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 11.03/2.23 % (3345591)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1691857396:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 11.03/2.23 % (3345592)lrs+10_1_sil=8000:sp=occurrence:random_seed=3801147766:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 11.03/2.23 % (3345593)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1839631704:i=437:sd=1:aac=none:ss=included_2994 on theBenchmark for (2994ds/437Mi) % 11.03/2.23 % (3345590)Refutation not found, incomplete strategy % 11.03/2.23 % (3345590)------------------------------ % 11.03/2.23 % (3345590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.03/2.23 % (3345590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.03/2.23 % (3345590)CaDiCaL version: 2.1.3 % 11.03/2.23 % (3345590)Termination reason: Refutation not found, incomplete strategy % 11.03/2.23 % (3345590)Time elapsed: 0.012 s % 11.03/2.23 % (3345590)Peak memory usage: 88 MB % 11.03/2.23 % (3345590)Instructions burned: 24 (million) % 11.03/2.23 % (3345597)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2904297993:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2994 on theBenchmark for (2994ds/134Mi) % 11.03/2.23 % (3345593)Refutation not found, incomplete strategy % 11.03/2.23 % (3345593)------------------------------ % 11.03/2.23 % (3345593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.03/2.23 % (3345593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.03/2.23 % (3345593)CaDiCaL version: 2.1.3 % 11.03/2.23 % (3345593)Termination reason: Refutation not found, incomplete strategy % 11.03/2.23 % (3345593)Time elapsed: 0.013 s % 11.03/2.23 % (3345593)Peak memory usage: 89 MB % 11.03/2.23 % (3345593)Instructions burned: 23 (million) % 11.03/2.23 % (3345596)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1586546630:i=5202:ss=axioms:sgt=16_2994 on theBenchmark for (2994ds/5202Mi) % 11.03/2.23 % (3345597)Instruction limit reached! % 11.03/2.23 % (3345597)------------------------------ % 11.03/2.23 % (3345597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.03/2.23 % (3345597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.03/2.23 % (3345597)CaDiCaL version: 2.1.3 % 11.03/2.23 % (3345597)Termination reason: Instruction limit % 11.03/2.23 % (3345597)Termination phase: Saturation % 11.03/2.23 % (3345597)Time elapsed: 0.041 s % 11.03/2.23 % (3345597)Peak memory usage: 90 MB % 11.03/2.23 % (3345597)Instructions burned: 136 (million) % 11.03/2.23 % (3345591)Instruction limit reached! % 11.03/2.23 % (3345591)------------------------------ % 11.03/2.23 % (3345591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.03/2.23 % (3345591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.03/2.23 % (3345591)CaDiCaL version: 2.1.3 % 11.03/2.23 % (3345591)Termination reason: Instruction limit % 11.03/2.23 % (3345591)Termination phase: Saturation % 11.03/2.23 % (3345591)Time elapsed: 0.059 s % 11.03/2.23 % (3345591)Peak memory usage: 89 MB % 11.03/2.23 % (3345591)Instructions burned: 115 (million) % 11.03/2.23 % (3345604)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=666673964:st=8:i=592:sd=3:ep=RST:ss=axioms_2992 on theBenchmark for (2992ds/592Mi) % 11.03/2.23 % (3345605)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=396472840:st=3:i=13193:sd=3:ss=axioms_2992 on theBenchmark for (2992ds/13193Mi) % 11.03/2.23 % (3345590)------------------------------ % 11.03/2.23 % (3345590)------------------------------ % 11.03/2.23 % (3345593)------------------------------ % 11.03/2.23 % (3345593)------------------------------ % 11.03/2.23 % Exception at run slice level % 11.03/2.23 User error: GNN currently only supports monomorphic FOL. % 11.03/2.23 % (3345604)Instruction limit reached! % 11.03/2.23 % (3345604)------------------------------ % 11.03/2.23 % (3345604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.03/2.23 % (3345604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.03/2.23 % (3345604)CaDiCaL version: 2.1.3 % 11.03/2.23 % (3345604)Termination reason: Instruction limit % 11.03/2.23 % (3345604)Termination phase: Saturation % 11.03/2.23 % (3345604)Time elapsed: 0.180 s % 11.03/2.23 % (3345604)Peak memory usage: 94 MB % 11.03/2.23 % (3345604)Instructions burned: 593 (million) % 11.03/2.23 % (3345608)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3351734501:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/125Mi) % 13.37/2.87 % (3345608)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.37/2.87 % (3345609)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=634766219:i=134:gtgl=5:slsql=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/134Mi) % 13.37/2.87 % (3345610)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1027451899:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/141Mi) % 13.37/2.87 % (3345610)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.37/2.87 % Exception at run slice level % 13.37/2.87 User error: Immediate (shared) subterms of term/literal combs(X0,bool,bool,sF70(X0,X1),sF92(X0,X2,X3,X4,X1)) have different types/not well-typed! % 13.37/2.87 % Exception at run slice level % 13.37/2.87 User error: GNN currently only supports monomorphic FOL. % 13.37/2.87 % (3345610)Refutation not found, incomplete strategy % 13.37/2.87 % (3345610)------------------------------ % 13.37/2.87 % (3345610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.37/2.87 % (3345610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.37/2.87 % (3345610)CaDiCaL version: 2.1.3 % 13.37/2.87 % (3345610)Termination reason: Refutation not found, incomplete strategy % 13.37/2.87 % (3345610)Time elapsed: 0.005 s % 13.37/2.87 % (3345610)Peak memory usage: 89 MB % 13.37/2.87 % (3345610)Instructions burned: 8 (million) % 13.37/2.87 % (3345611)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2676843958:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2990 on theBenchmark for (2990ds/431Mi) % 13.37/2.87 % (3345608)Instruction limit reached! % 13.37/2.87 % (3345608)------------------------------ % 13.37/2.87 % (3345608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.37/2.87 % (3345608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.37/2.87 % (3345608)CaDiCaL version: 2.1.3 % 13.37/2.87 % (3345608)Termination reason: Instruction limit % 13.37/2.87 % (3345608)Termination phase: Saturation % 13.37/2.87 % (3345608)Time elapsed: 0.072 s % 13.37/2.87 % (3345608)Peak memory usage: 90 MB % 13.37/2.87 % (3345608)Instructions burned: 126 (million) % 13.37/2.87 % (3345611)Instruction limit reached! % 13.37/2.87 % (3345611)------------------------------ % 13.37/2.87 % (3345611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.37/2.87 % (3345611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.37/2.87 % (3345611)CaDiCaL version: 2.1.3 % 13.37/2.87 % (3345611)Termination reason: Instruction limit % 13.37/2.87 % (3345611)Termination phase: Saturation % 13.37/2.87 % (3345611)Time elapsed: 0.118 s % 13.37/2.87 % (3345611)Peak memory usage: 90 MB % 13.37/2.87 % (3345611)Instructions burned: 434 (million) % 13.37/2.87 % (3345617)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1477441491:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2989 on theBenchmark for (2989ds/150Mi) % 13.37/2.87 % (3345615)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2686542309:i=6060:aac=none:ins=25_2989 on theBenchmark for (2989ds/6060Mi) % 13.37/2.87 % (3345617)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.37/2.87 % (3345592)Instruction limit reached! % 13.37/2.87 % (3345592)------------------------------ % 13.37/2.87 % (3345592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.37/2.87 % (3345592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.37/2.87 % (3345592)CaDiCaL version: 2.1.3 % 13.37/2.87 % (3345592)Termination reason: Instruction limit % 13.37/2.87 % (3345592)Termination phase: Saturation % 13.37/2.87 % (3345592)Time elapsed: 0.538 s % 13.37/2.87 % (3345592)Peak memory usage: 96 MB % 13.37/2.87 % (3345592)Instructions burned: 907 (million) % 13.37/2.87 % Exception at run slice level % 13.37/2.87 User error: GNN currently only supports monomorphic FOL. % 13.37/2.87 % (3345618)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3141958633:i=14155:bd=all_2988 on theBenchmark for (2988ds/14155Mi) % 19.59/3.58 % (3345620)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1109354050:i=667:av=off:fsr=off_2988 on theBenchmark for (2988ds/667Mi) % 19.59/3.58 % (3345617)Instruction limit reached! % 19.59/3.58 % (3345617)------------------------------ % 19.59/3.58 % (3345617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.59/3.58 % (3345617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.59/3.58 % (3345617)CaDiCaL version: 2.1.3 % 19.59/3.58 % (3345617)Termination reason: Instruction limit % 19.59/3.58 % (3345617)Termination phase: Saturation % 19.59/3.58 % (3345617)Time elapsed: 0.090 s % 19.59/3.58 % (3345617)Peak memory usage: 90 MB % 19.59/3.58 % (3345617)Instructions burned: 150 (million) % 19.59/3.58 % (3345620)Refutation not found, incomplete strategy % 19.59/3.58 % (3345620)------------------------------ % 19.59/3.58 % (3345620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.59/3.58 % (3345620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.59/3.58 % (3345620)CaDiCaL version: 2.1.3 % 19.59/3.58 % (3345620)Termination reason: Refutation not found, incomplete strategy % 19.59/3.58 % (3345620)Time elapsed: 0.009 s % 19.59/3.58 % (3345620)Peak memory usage: 89 MB % 19.59/3.58 % (3345620)Instructions burned: 32 (million) % 19.59/3.58 % (3345610)------------------------------ % 19.59/3.58 % (3345610)------------------------------ % 19.59/3.58 % (3345622)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3288084940:s2a=on:i=185:s2at=1.8:fdi=4_2988 on theBenchmark for (2988ds/185Mi) % 19.59/3.58 % (3345623)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3605097983:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2987 on theBenchmark for (2987ds/193Mi) % 19.59/3.58 % (3345626)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2722300454:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2987 on theBenchmark for (2987ds/4850Mi) % 19.59/3.58 % (3345626)Refutation not found, incomplete strategy % 19.59/3.58 % (3345626)------------------------------ % 19.59/3.58 % (3345626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.59/3.58 % (3345626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.59/3.58 % (3345626)CaDiCaL version: 2.1.3 % 19.59/3.58 % (3345626)Termination reason: Refutation not found, incomplete strategy % 19.59/3.58 % (3345626)Time elapsed: 0.011 s % 19.59/3.58 % (3345626)Peak memory usage: 88 MB % 19.59/3.58 % (3345626)Instructions burned: 20 (million) % 19.59/3.58 % (3345620)------------------------------ % 19.59/3.58 % (3345620)------------------------------ % 19.59/3.58 % (3345627)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=608180776:i=12111:sd=1:ss=included_2986 on theBenchmark for (2986ds/12111Mi) % 19.59/3.58 % (3345622)Instruction limit reached! % 19.59/3.58 % (3345622)------------------------------ % 19.59/3.58 % (3345622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.59/3.58 % (3345622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.59/3.58 % (3345622)CaDiCaL version: 2.1.3 % 19.59/3.58 % (3345622)Termination reason: Instruction limit % 19.59/3.58 % (3345622)Termination phase: Saturation % 19.59/3.58 % (3345622)Time elapsed: 0.113 s % 19.59/3.58 % (3345622)Peak memory usage: 91 MB % 19.59/3.58 % (3345622)Instructions burned: 185 (million) % 19.59/3.58 % (3345623)Instruction limit reached! % 19.59/3.58 % (3345623)------------------------------ % 19.59/3.58 % (3345623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.59/3.58 % (3345623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.59/3.58 % (3345623)CaDiCaL version: 2.1.3 % 19.59/3.58 % (3345623)Termination reason: Instruction limit % 19.59/3.58 % (3345623)Termination phase: Saturation % 19.59/3.58 % (3345623)Time elapsed: 0.118 s % 19.59/3.58 % (3345623)Peak memory usage: 90 MB % 19.59/3.58 % (3345623)Instructions burned: 194 (million) % 19.59/3.58 % (3345631)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3462118890:i=319:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/319Mi) % 19.59/3.58 % Exception at run slice level % 19.59/3.58 User error: GNN currently only supports monomorphic FOL. % 19.59/3.58 % (3345634)dis-1011_128_sil=32000:random_seed=690070078:i=3706:ep=RST:av=off_2985 on theBenchmark for (2985ds/3706Mi) % 25.81/4.34 % (3345633)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=846360371:i=2064:ep=RST_2985 on theBenchmark for (2985ds/2064Mi) % 25.81/4.34 % Exception at run slice level % 25.81/4.34 User error: GNN currently only supports monomorphic FOL. % 25.81/4.34 % (3345631)Instruction limit reached! % 25.81/4.34 % (3345631)------------------------------ % 25.81/4.34 % (3345631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.81/4.34 % (3345631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.81/4.34 % (3345631)CaDiCaL version: 2.1.3 % 25.81/4.34 % (3345631)Termination reason: Instruction limit % 25.81/4.34 % (3345631)Termination phase: Saturation % 25.81/4.34 % (3345631)Time elapsed: 0.102 s % 25.81/4.34 % (3345631)Peak memory usage: 91 MB % 25.81/4.34 % (3345631)Instructions burned: 320 (million) % 25.81/4.34 % (3345626)------------------------------ % 25.81/4.34 % (3345626)------------------------------ % 25.81/4.34 % (3345636)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=544239270:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2984 on theBenchmark for (2984ds/757Mi) % 25.81/4.34 % (3345639)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2586236920:i=13913:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/13913Mi) % 25.81/4.34 % (3345636)Refutation not found, incomplete strategy % 25.81/4.34 % (3345636)------------------------------ % 25.81/4.34 % (3345636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.81/4.34 % (3345636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.81/4.34 % (3345636)CaDiCaL version: 2.1.3 % 25.81/4.34 % (3345636)Termination reason: Refutation not found, incomplete strategy % 25.81/4.34 % (3345636)Time elapsed: 0.013 s % 25.81/4.34 % (3345636)Peak memory usage: 89 MB % 25.81/4.34 % (3345636)Instructions burned: 25 (million) % 25.81/4.34 % (3345640)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3040663387:i=9925:aac=none_2983 on theBenchmark for (2983ds/9925Mi) % 25.81/4.34 % (3345641)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4113710600:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2983 on theBenchmark for (2983ds/2479Mi) % 25.81/4.34 % Exception at run slice level % 25.81/4.34 User error: GNN currently only supports monomorphic FOL. % 25.81/4.34 % (3345641)Refutation not found, incomplete strategy % 25.81/4.34 % (3345641)------------------------------ % 25.81/4.34 % (3345641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.81/4.34 % (3345641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.81/4.34 % (3345641)CaDiCaL version: 2.1.3 % 25.81/4.34 % (3345641)Termination reason: Refutation not found, incomplete strategy % 25.81/4.34 % (3345641)Time elapsed: 0.013 s % 25.81/4.34 % (3345641)Peak memory usage: 89 MB % 25.81/4.34 % (3345641)Instructions burned: 24 (million) % 25.81/4.34 % Exception at run slice level % 25.81/4.34 User error: GNN currently only supports monomorphic FOL. % 25.81/4.34 % (3345636)------------------------------ % 25.81/4.34 % (3345636)------------------------------ % 25.81/4.34 % (3345646)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=167156518:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/440Mi) % 25.81/4.34 % (3345646)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 25.81/4.34 % (3345647)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2244717982:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2981 on theBenchmark for (2981ds/11145Mi) % 25.81/4.34 % (3345641)------------------------------ % 25.81/4.34 % (3345641)------------------------------ % 25.81/4.34 % (3345649)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=722953126:cts=off:i=3034:av=off:er=known:fsd=on_2980 on theBenchmark for (2980ds/3034Mi) % 25.81/4.34 % Exception at run slice level % 25.81/4.34 User error: GNN currently only supports monomorphic FOL. % 25.81/4.34 % (3345671)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3966040460:st=2:s2a=on:i=524:s2at=2:ss=axioms_2979 on theBenchmark for (2979ds/524Mi) % 25.81/4.34 % Exception at run slice level % 25.81/4.34 User error: GNN currently only supports monomorphic FOL. % 25.81/4.34 % (3345646)Instruction limit reached! % 35.15/5.78 % (3345646)------------------------------ % 35.15/5.78 % (3345646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.15/5.78 % (3345646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.15/5.78 % (3345646)CaDiCaL version: 2.1.3 % 35.15/5.78 % (3345646)Termination reason: Instruction limit % 35.15/5.78 % (3345646)Termination phase: Saturation % 35.15/5.78 % (3345646)Time elapsed: 0.265 s % 35.15/5.78 % (3345646)Peak memory usage: 94 MB % 35.15/5.78 % (3345646)Instructions burned: 440 (million) % 35.15/5.78 % (3345693)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2740926132:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2978 on theBenchmark for (2978ds/1016Mi) % 35.15/5.78 % (3345717)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=626974281:i=14123:bd=preordered:ins=4_2978 on theBenchmark for (2978ds/14123Mi) % 35.15/5.78 % (3345723)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1660743049:i=5781:kws=precedence:bd=all:rawr=on_2977 on theBenchmark for (2977ds/5781Mi) % 35.15/5.78 % Exception at run slice level % 35.15/5.78 User error: GNN currently only supports monomorphic FOL. % 35.15/5.78 % (3345742)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=2122220232:i=2448:gtgl=5:bd=preordered:gtg=all_2976 on theBenchmark for (2976ds/2448Mi) % 35.15/5.78 % (3345671)Instruction limit reached! % 35.15/5.78 % (3345671)------------------------------ % 35.15/5.78 % (3345671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.15/5.78 % (3345671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.15/5.78 % (3345671)CaDiCaL version: 2.1.3 % 35.15/5.78 % (3345671)Termination reason: Instruction limit % 35.15/5.78 % (3345671)Termination phase: Saturation % 35.15/5.78 % (3345671)Time elapsed: 0.273 s % 35.15/5.78 % (3345671)Peak memory usage: 91 MB % 35.15/5.78 % (3345671)Instructions burned: 525 (million) % 35.15/5.78 % (3345783)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3235556389:i=3223:kws=precedence:fgj=on:av=off_2975 on theBenchmark for (2975ds/3223Mi) % 35.15/5.78 % Exception at run slice level % 35.15/5.78 User error: GNN currently only supports monomorphic FOL. % 35.15/5.78 % (3345633)Instruction limit reached! % 35.15/5.78 % (3345633)------------------------------ % 35.15/5.78 % (3345633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.15/5.78 % (3345633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.15/5.78 % (3345633)CaDiCaL version: 2.1.3 % 35.15/5.78 % (3345633)Termination reason: Instruction limit % 35.15/5.78 % (3345633)Termination phase: Saturation % 35.15/5.78 % (3345633)Time elapsed: 1.073 s % 35.15/5.78 % (3345633)Peak memory usage: 96 MB % 35.15/5.78 % (3345633)Instructions burned: 2065 (million) % 35.15/5.78 % Exception at run slice level % 35.15/5.78 User error: GNN currently only supports monomorphic FOL. % 35.15/5.78 % (3345785)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3046884596:st=5.6:i=2033:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/2033Mi) % 35.15/5.78 % (3345693)Instruction limit reached! % 35.15/5.78 % (3345693)------------------------------ % 35.15/5.78 % (3345693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.15/5.78 % (3345693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.15/5.78 % (3345693)CaDiCaL version: 2.1.3 % 35.15/5.78 % (3345693)Termination reason: Instruction limit % 35.15/5.78 % (3345693)Termination phase: Saturation % 35.15/5.78 % (3345693)Time elapsed: 0.541 s % 35.15/5.78 % (3345693)Peak memory usage: 93 MB % 35.15/5.78 % (3345693)Instructions burned: 1016 (million) % 35.15/5.78 % (3345786)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=4247540433:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2973 on theBenchmark for (2973ds/2055Mi) % 35.15/5.78 % (3345787)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=2552110606:i=21611:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/21611Mi) % 35.15/5.78 % (3345789)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2508738322:i=4835:sd=13:ss=axioms:sgt=23_2972 on theBenchmark for (2972ds/4835Mi) % 35.15/5.78 % Exception at run slice level % 35.15/5.78 User error: GNN currently only supports monomorphic FOL. % 43.02/6.88 % Exception at run slice level % 43.02/6.88 User error: GNN currently only supports monomorphic FOL. % 43.02/6.88 % (3345793)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=1264307876:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2970 on theBenchmark for (2970ds/797Mi) % 43.02/6.88 % (3345794)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1537673655:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2970 on theBenchmark for (2970ds/2326Mi) % 43.02/6.88 % (3345794)Refutation not found, incomplete strategy % 43.02/6.88 % (3345794)------------------------------ % 43.02/6.88 % (3345794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.02/6.88 % (3345794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.02/6.88 % (3345794)CaDiCaL version: 2.1.3 % 43.02/6.88 % (3345794)Termination reason: Refutation not found, incomplete strategy % 43.02/6.88 % (3345794)Time elapsed: 0.025 s % 43.02/6.88 % (3345794)Peak memory usage: 89 MB % 43.02/6.88 % (3345794)Instructions burned: 43 (million) % 43.02/6.88 % Exception at run slice level% Exception at run slice level % 43.02/6.88 % 43.02/6.88 User error: User error: GNN currently only supports monomorphic FOL.GNN currently only supports monomorphic FOL. % 43.02/6.88 % 43.02/6.88 % (3345793)Instruction limit reached! % 43.02/6.88 % (3345793)------------------------------ % 43.02/6.88 % (3345793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.02/6.88 % (3345793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.02/6.88 % (3345793)CaDiCaL version: 2.1.3 % 43.02/6.88 % (3345793)Termination reason: Instruction limit % 43.02/6.88 % (3345793)Termination phase: Saturation % 43.02/6.88 % (3345793)Time elapsed: 0.176 s % 43.02/6.88 % (3345793)Peak memory usage: 89 MB % 43.02/6.88 % (3345793)Instructions burned: 798 (million) % 43.02/6.88 % (3345799)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=4186955943:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2968 on theBenchmark for (2968ds/1008Mi) % 43.02/6.88 % (3345797)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3002335397:i=6038:nm=6_2968 on theBenchmark for (2968ds/6038Mi) % 43.02/6.88 % (3345798)lrs+10_1_sil=32000:sp=occurrence:random_seed=683584636:st=2:i=33334:sd=3:ss=included:sgt=32_2968 on theBenchmark for (2968ds/33334Mi) % 43.02/6.88 % (3345794)------------------------------ % 43.02/6.88 % (3345794)------------------------------ % 43.02/6.88 % (3345803)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=3309899101:i=8327:s2at=5:bd=preordered_2966 on theBenchmark for (2966ds/8327Mi) % 43.02/6.88 % (3345634)Instruction limit reached! % 43.02/6.88 % (3345634)------------------------------ % 43.02/6.88 % (3345634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.02/6.88 % (3345634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.02/6.88 % (3345634)CaDiCaL version: 2.1.3 % 43.02/6.88 % (3345634)Termination reason: Instruction limit % 43.02/6.88 % (3345634)Termination phase: Saturation % 43.02/6.88 % (3345634)Time elapsed: 1.978 s % 43.02/6.88 % (3345634)Peak memory usage: 99 MB % 43.02/6.88 % (3345634)Instructions burned: 3707 (million) % 43.02/6.88 % (3345799)Instruction limit reached! % 43.02/6.88 % (3345799)------------------------------ % 43.02/6.88 % (3345799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.02/6.88 % (3345799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.02/6.88 % (3345799)CaDiCaL version: 2.1.3 % 43.02/6.88 % (3345799)Termination reason: Instruction limit % 43.02/6.88 % (3345799)Termination phase: Saturation % 43.02/6.88 % (3345799)Time elapsed: 0.284 s % 43.02/6.88 % (3345799)Peak memory usage: 93 MB % 43.02/6.88 % (3345799)Instructions burned: 1012 (million) % 43.02/6.88 % Exception at run slice level % 43.02/6.88 User error: GNN currently only supports monomorphic FOL. % 43.02/6.88 % (3345805)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=122469590:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2964 on theBenchmark for (2964ds/1083Mi) % 43.02/6.88 % (3345806)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1658479861:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2964 on theBenchmark for (2964ds/1084Mi) % 51.00/8.01 % (3345808)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=4124541106:i=6995:s2at=5:gtg=all_2963 on theBenchmark for (2963ds/6995Mi) % 51.00/8.01 % Exception at run slice level % 51.00/8.01 User error: GNN currently only supports monomorphic FOL. % 51.00/8.01 % (3345805)Instruction limit reached! % 51.00/8.01 % (3345805)------------------------------ % 51.00/8.01 % (3345805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.00/8.01 % (3345805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.00/8.01 % (3345805)CaDiCaL version: 2.1.3 % 51.00/8.01 % (3345805)Termination reason: Instruction limit % 51.00/8.01 % (3345805)Termination phase: Saturation % 51.00/8.01 % (3345805)Time elapsed: 0.289 s % 51.00/8.01 % (3345805)Peak memory usage: 96 MB % 51.00/8.01 % (3345805)Instructions burned: 1088 (million) % 51.00/8.01 % (3345811)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=3304596639:st=2:i=6225:sd=15:ss=axioms_2961 on theBenchmark for (2961ds/6225Mi) % 51.00/8.01 % (3345812)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=1650847833:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2960 on theBenchmark for (2960ds/3372Mi) % 51.00/8.01 % Exception at run slice level % 51.00/8.01 User error: GNN currently only supports monomorphic FOL. % 51.00/8.01 % Exception at run slice level % 51.00/8.01 User error: GNN currently only supports monomorphic FOL. % 51.00/8.01 % (3345815)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=485583748:st=2.3:i=26457:sd=10:ss=included:sgt=8_2958 on theBenchmark for (2958ds/26457Mi) % 51.00/8.01 % (3345806)Instruction limit reached! % 51.00/8.01 % (3345806)------------------------------ % 51.00/8.01 % (3345806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.00/8.01 % (3345806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.00/8.01 % (3345806)CaDiCaL version: 2.1.3 % 51.00/8.01 % (3345806)Termination reason: Instruction limit % 51.00/8.01 % (3345806)Termination phase: Saturation % 51.00/8.01 % (3345806)Time elapsed: 0.583 s % 51.00/8.01 % (3345806)Peak memory usage: 94 MB % 51.00/8.01 % (3345806)Instructions burned: 1084 (million) % 51.00/8.01 % (3345816)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=172875185:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2957 on theBenchmark for (2957ds/13494Mi) % 51.00/8.01 % (3345818)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=1375147422:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2957 on theBenchmark for (2957ds/2503Mi) % 51.00/8.01 % (3345818)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 51.00/8.01 % Exception at run slice level % 51.00/8.01 User error: GNN currently only supports monomorphic FOL. % 51.00/8.01 % (3345821)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=2448632378:i=2559:sd=1:ep=RSTC:ss=axioms_2954 on theBenchmark for (2954ds/2559Mi) % 51.00/8.01 % Exception at run slice level % 51.00/8.01 User error: GNN currently only supports monomorphic FOL. % 51.00/8.01 % Exception at run slice level % 51.00/8.01 User error: GNN currently only supports monomorphic FOL. % 51.00/8.01 % (3345823)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1948235796:i=30753:av=off:ss=included_2953 on theBenchmark for (2953ds/30753Mi) % 51.00/8.01 % Exception at run slice level % 51.00/8.01 User error: GNN currently only supports monomorphic FOL. % 51.00/8.01 % (3345826)dis-1011_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:tgt=ground:npcc=on:sp=arity:sos=on:erd=off:rp=on:gs=on:kmz=on:random_seed=1545991537:cts=off:i=2759:kws=inv_arity:fgj=on_2952 on theBenchmark for (2952ds/2759Mi) % 51.00/8.01 % (3345825)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=799662531:i=26473:ep=RSTC_2952 on theBenchmark for (2952ds/26473Mi) % 51.00/8.01 % Exception at run slice level % 51.00/8.01 User error: GNN currently only supports monomorphic FOL. % 51.00/8.01 % Exception at run slice level % 51.00/8.01 User error: GNN currently only supports monomorphic FOL. % 61.10/9.37 % (3345829)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:sos=all:spb=goal_then_units:urr=ec_only:sac=on:random_seed=2097428473:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2949 on theBenchmark for (2949ds/5665Mi) % 61.10/9.37 % (3345829)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 61.10/9.37 % (3345830)dis+1011_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:npcc=on:sos=on:lsd=20:urr=full:alpa=true:sac=on:random_seed=1037304799:i=1532:ep=RS:ss=axioms_2948 on theBenchmark for (2948ds/1532Mi) % 61.10/9.37 % Exception at run slice level % 61.10/9.37 User error: GNN currently only supports monomorphic FOL. % 61.10/9.37 % (3345789)Instruction limit reached! % 61.10/9.37 % (3345789)------------------------------ % 61.10/9.37 % (3345789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.10/9.37 % (3345789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.10/9.37 % (3345789)CaDiCaL version: 2.1.3 % 61.10/9.37 % (3345789)Termination reason: Instruction limit % 61.10/9.37 % (3345789)Termination phase: Saturation % 61.10/9.37 % (3345789)Time elapsed: 2.472 s % 61.10/9.37 % (3345789)Peak memory usage: 105 MB % 61.10/9.37 % (3345789)Instructions burned: 4836 (million) % 61.10/9.37 % (3345833)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=1388013608:i=1565:sd=2:ss=axioms:sgt=32_2946 on theBenchmark for (2946ds/1565Mi) % 61.10/9.37 % (3345834)lrs-1011_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:sims=off:bsd=on:sp=unary_first:erd=off:spb=goal:lcm=reverse:gs=on:s2agt=8:random_seed=2711075296:i=1572:fgj=on:gsp=on_2946 on theBenchmark for (2946ds/1572Mi) % 61.10/9.37 % (3345834)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 61.10/9.37 % Exception at run slice level % 61.10/9.37 User error: GNN currently only supports monomorphic FOL. % 61.10/9.37 % Exception at run slice level % 61.10/9.37 User error: GNN currently only supports monomorphic FOL. % 61.10/9.37 % (3345838)lrs+21_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:sos=on:erd=off:lcm=predicate:alpa=false:sac=on:random_seed=4156739896:i=3500:sd=1:bd=preordered:sup=off:ss=included_2943 on theBenchmark for (2943ds/3500Mi) % 61.10/9.37 % (3345723)Instruction limit reached! % 61.10/9.37 % (3345723)------------------------------ % 61.10/9.37 % (3345723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.10/9.37 % (3345723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.10/9.37 % (3345723)CaDiCaL version: 2.1.3 % 61.10/9.37 % (3345723)Termination reason: Instruction limit % 61.10/9.37 % (3345723)Termination phase: Saturation % 61.10/9.37 % (3345723)Time elapsed: 3.389 s % 61.10/9.37 % (3345723)Peak memory usage: 126 MB % 61.10/9.37 % (3345723)Instructions burned: 5783 (million) % 61.10/9.37 % (3345837)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=2559580542:i=6052:sd=4:ss=axioms:sgt=24_2943 on theBenchmark for (2943ds/6052Mi) % 61.10/9.37 % (3345840)lrs+35_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:npcc=on:fde=none:sp=weighted_frequency:erd=off:spb=non_intro:updr=off:newcnf=on:random_seed=1819911054:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2942 on theBenchmark for (2942ds/1842Mi) % 61.10/9.37 % (3345840)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 61.10/9.37 % Exception at run slice level % 61.10/9.37 User error: GNN currently only supports monomorphic FOL. % 61.10/9.37 % Exception at run slice level % 61.10/9.37 User error: GNN currently only supports monomorphic FOL. % 61.10/9.37 % (3345844)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=1361508378:i=1884:sd=1:nm=60:ss=axioms_2940 on theBenchmark for (2940ds/1884Mi) % 61.10/9.37 % (3345843)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1309318620:i=66096:add=on_2941 on theBenchmark for (2941ds/66096Mi) % 61.10/9.37 % Exception at run slice level % 61.10/9.37 User error: GNN currently only supports monomorphic FOL. % 61.10/9.37 % Exception at run slice level % 61.10/9.37 User error: GNN currently only supports monomorphic FOL. % 61.10/9.37 % Exception at run slice level % 61.10/9.37 User error: GNN currently only supports monomorphic FOL. % 72.35/10.95 % (3345847)lrs-1011_4:1_sil=16000:bsr=on:random_seed=1909095740:cts=off:i=5469:bs=on:fsr=off_2938 on theBenchmark for (2938ds/5469Mi) % 72.35/10.95 % (3345848)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=unary_frequency:urr=on:bce=on:alpa=false:sac=on:random_seed=2400964373:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2938 on theBenchmark for (2938ds/2037Mi) % 72.35/10.95 % (3345849)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2883017803:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2937 on theBenchmark for (2937ds/2110Mi) % 72.35/10.95 % Exception at run slice level % 72.35/10.95 User error: GNN currently only supports monomorphic FOL. % 72.35/10.95 % Exception at run slice level % 72.35/10.95 User error: GNN currently only supports monomorphic FOL. % 72.35/10.95 % (3345853)dis-1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:lcm=reverse:fd=off:flr=on:random_seed=386049364:i=2430:add=off:aac=none:nm=16_2936 on theBenchmark for (2936ds/2430Mi) % 72.35/10.95 % (3345854)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:spb=units:acc=on:bsr=unit_only:gs=on:sac=on:random_seed=1069287472:cond=fast:i=4891_2935 on theBenchmark for (2935ds/4891Mi) % 72.35/10.95 % Exception at run slice level % 72.35/10.95 User error: GNN currently only supports monomorphic FOL. % 72.35/10.95 % Exception at run slice level % 72.35/10.95 User error: GNN currently only supports monomorphic FOL. % 72.35/10.95 % (3345858)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=954731332:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2932 on theBenchmark for (2932ds/7534Mi) % 72.35/10.95 % (3345857)lrs+4_1_anc=all:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sos=on:spb=goal_then_units:lcm=reverse:gs=on:s2agt=16:sac=on:newcnf=on:random_seed=2407533590:st=2:i=14845:sd=2:ss=included:fsd=on_2932 on theBenchmark for (2932ds/14845Mi) % 72.35/10.95 % Exception at run slice level % 72.35/10.95 User error: GNN currently only supports monomorphic FOL. % 72.35/10.95 % (3345861)lrs-1002_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=ground:npcc=on:prc=on:fde=none:sims=off:spb=goal:bsr=unit_only:s2agt=32:random_seed=2335688147:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2931 on theBenchmark for (2931ds/10353Mi) % 72.35/10.95 % Exception at run slice level % 72.35/10.95 User error: GNN currently only supports monomorphic FOL. % 72.35/10.95 % (3345811)Instruction limit reached! % 72.35/10.95 % (3345811)------------------------------ % 72.35/10.95 % (3345811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.35/10.95 % (3345811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.35/10.95 % (3345811)CaDiCaL version: 2.1.3 % 72.35/10.95 % (3345811)Termination reason: Instruction limit % 72.35/10.95 % (3345811)Termination phase: Saturation % 72.35/10.95 % (3345811)Time elapsed: 3.060 s % 72.35/10.95 % (3345811)Peak memory usage: 116 MB % 72.35/10.95 % (3345811)Instructions burned: 6227 (million) % 72.35/10.95 % (3345863)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2003687180:i=7860_2929 on theBenchmark for (2929ds/7860Mi) % 72.35/10.95 % (3345863)Refutation not found, incomplete strategy % 72.35/10.95 % (3345863)------------------------------ % 72.35/10.95 % (3345863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.35/10.95 % (3345863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.35/10.95 % (3345863)CaDiCaL version: 2.1.3 % 72.35/10.95 % (3345863)Termination reason: Refutation not found, incomplete strategy % 72.35/10.95 % (3345863)Time elapsed: 0.008 s % 72.35/10.95 % (3345863)Peak memory usage: 89 MB % 72.35/10.95 % (3345863)Instructions burned: 28 (million) % 72.35/10.95 % (3345864)ott+1011_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:fde=unused:spb=goal:lsd=30:lcm=predicate:fd=off:gs=on:sac=on:random_seed=1549616347:i=7896:sd=2:bs=on:ss=included:sgt=20_2929 on theBenchmark for (2929ds/7896Mi) % 72.35/10.95 % Exception at run slice level % 72.35/10.95 User error: GNN currently only supports monomorphic FOL. % 72.35/10.95 % (3345863)------------------------------ % 72.35/10.95 % (3345863)------------------------------ % 72.35/10.95 % (3345867)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1628309977:i=5812:gtgl=2:gtg=all_2927 on theBenchmark for (2927ds/5812Mi) % 113.38/16.67 % Exception at run slice level % 113.38/16.67 User error: GNN currently only supports monomorphic FOL. % 113.38/16.67 % (3345868)ott-1011_1_anc=none:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=const_frequency:sos=on:lsd=100:random_seed=1559528994:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2927 on theBenchmark for (2927ds/2965Mi) % 113.38/16.67 % (3345870)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=922915156:i=2967:kws=precedence:bd=preordered:av=off_2926 on theBenchmark for (2926ds/2967Mi) % 113.38/16.67 % Exception at run slice level % 113.38/16.67 User error: GNN currently only supports monomorphic FOL. % 113.38/16.67 % Exception at run slice level % 113.38/16.67 User error: GNN currently only supports monomorphic FOL. % 113.38/16.67 % (3345874)lrs-1010_1_ncem=casc2026/models/loop4.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=const_frequency:sos=all:lcm=predicate:acc=on:bsr=unit_only:gs=on:sac=on:newcnf=on:random_seed=2166389860:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2924 on theBenchmark for (2924ds/3207Mi) % 113.38/16.67 % (3345873)ott+1002_1_anc=all:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:sos=on:spb=goal_then_units:alpa=false:sac=on:random_seed=1417448515:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2924 on theBenchmark for (2924ds/3022Mi) % 113.38/16.67 % Exception at run slice level % 113.38/16.67 User error: GNN currently only supports monomorphic FOL. % 113.38/16.67 % Exception at run slice level % 113.38/16.67 User error: GNN currently only supports monomorphic FOL. % 113.38/16.67 % (3345877)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=528481176:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2922 on theBenchmark for (2922ds/3289Mi) % 113.38/16.67 % Exception at run slice level % 113.38/16.67 User error: GNN currently only supports monomorphic FOL. % 113.38/16.67 % (3345878)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=1770658660:i=38569:sd=3:ss=axioms:sgt=32_2921 on theBenchmark for (2921ds/38569Mi) % 113.38/16.67 % (3345880)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=65402731:cts=off:i=3394_2920 on theBenchmark for (2920ds/3394Mi) % 113.38/16.67 % Exception at run slice level % 113.38/16.67 User error: GNN currently only supports monomorphic FOL. % 113.38/16.67 % Exception at run slice level % 113.38/16.67 User error: GNN currently only supports monomorphic FOL. % 113.38/16.67 % (3345883)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=arity:spb=intro:lcm=reverse:urr=ec_only:fd=preordered:gs=on:sac=on:random_seed=1666768999:i=33824:bd=preordered_2919 on theBenchmark for (2919ds/33824Mi) % 113.38/16.67 % Exception at run slice level % 113.38/16.67 User error: GNN currently only supports monomorphic FOL. % 113.38/16.67 % Exception at run slice level % 113.38/16.67 User error: GNN currently only supports monomorphic FOL. % 113.38/16.67 % (3345884)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=250840801:i=20684:bd=all:gtg=exists_sym_2917 on theBenchmark for (2917ds/20684Mi) % 113.38/16.67 % (3345886)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:irw=on:npcc=on:prc=on:bsd=on:sp=reverse_frequency:sos=on:erd=off:spb=goal:lcm=reverse:urr=full:bsr=on:s2agt=32:alpa=random:kmz=on:random_seed=3854580549:st=3:prac=on:i=7222:kws=arity_squared:add=on:fgj=on:bd=preordered:gtg=exists_top:gsp=on:ss=axioms:er=known:sgt=8:proc=on_2917 on theBenchmark for (2917ds/7222Mi) % 113.38/16.67 % (3345886)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 113.38/16.67 % Exception at run slice level % 113.38/16.67 User error: GNN currently only supports monomorphic FOL. % 113.38/16.67 % (3345888)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=2813115795:st=4:i=7295:sd=4:ep=R:ss=axioms_2916 on theBenchmark for (2916ds/7295Mi) % 113.38/16.67 % (3345890)lrs+32_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:fde=none:sp=occurrence:urr=ec_only:fd=preordered:random_seed=2264193868:i=4036:ins=10_2915 on theBenchmark for (2915ds/4036Mi) % 113.38/16.67 % Exception at run slice level % 113.38/16.67 User error: GNN currently only supports monomorphic FOL. % 113.38/16.67 % Exception at run slice level % 113.38/16.67 User error: GNN currently only supports monomorphic FOL. % 113.38/16.67 % Exception at run slice level % 135.60/19.87 User error: GNN currently only supports monomorphic FOL. % 135.60/19.87 % (3345893)lrs+10_1_sil=128000:lcm=predicate:random_seed=465792169:st=3:i=43697:sd=5:ss=axioms_2912 on theBenchmark for (2912ds/43697Mi) % 135.60/19.87 % Exception at run slice level % 135.60/19.87 User error: GNN currently only supports monomorphic FOL. % 135.60/19.87 % (3345894)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:sp=const_frequency:sos=all:lcm=predicate:urr=on:s2agt=20:sac=on:random_seed=4114371563:i=17599:gtg=all:ss=axioms:fsd=on_2912 on theBenchmark for (2912ds/17599Mi) % 135.60/19.87 % (3345895)lrs+1011_1_to=lpo:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=occurrence:lcm=reverse:urr=ec_only:gs=on:random_seed=1526285715:i=4547:bd=preordered_2912 on theBenchmark for (2912ds/4547Mi) % 135.60/19.87 % (3345897)lrs+1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:urr=ec_only:newcnf=on:random_seed=2497259759:i=9294:av=off_2911 on theBenchmark for (2911ds/9294Mi) % 135.60/19.87 % Exception at run slice level % 135.60/19.87 User error: GNN currently only supports monomorphic FOL. % 135.60/19.87 % Exception at run slice level % 135.60/19.87 User error: GNN currently only supports monomorphic FOL. % 135.60/19.87 % (3345901)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1731086061:i=32849:add=on_2907 on theBenchmark for (2907ds/32849Mi) % 135.60/19.87 % Exception at run slice level % 135.60/19.87 User error: GNN currently only supports monomorphic FOL. % 135.60/19.87 % (3345902)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2152375233:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2907 on theBenchmark for (2907ds/4793Mi) % 135.60/19.87 % (3345904)dis+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:prc=on:drc=off:sims=off:sp=const_frequency:sos=on:spb=non_intro:gs=on:updr=off:newcnf=on:random_seed=3371896390:i=4840:nm=4:av=off_2906 on theBenchmark for (2906ds/4840Mi) % 135.60/19.87 % (3345847)Instruction limit reached! % 135.60/19.87 % (3345847)------------------------------ % 135.60/19.87 % (3345847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.60/19.87 % (3345847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.60/19.87 % (3345847)CaDiCaL version: 2.1.3 % 135.60/19.87 % (3345847)Termination reason: Instruction limit % 135.60/19.87 % (3345847)Termination phase: Saturation % 135.60/19.87 % (3345847)Time elapsed: 3.368 s % 135.60/19.87 % (3345847)Peak memory usage: 117 MB % 135.60/19.87 % (3345847)Instructions burned: 5469 (million) % 135.60/19.87 % Exception at run slice level % 135.60/19.87 User error: GNN currently only supports monomorphic FOL. % 135.60/19.87 % Exception at run slice level % 135.60/19.87 User error: GNN currently only supports monomorphic FOL. % 135.60/19.87 % (3345907)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=1505038547:cts=off:i=5002_2903 on theBenchmark for (2903ds/5002Mi) % 135.60/19.87 % (3345908)dis+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=3274466084:i=30479:sd=3:ss=axioms_2903 on theBenchmark for (2903ds/30479Mi) % 135.60/19.87 % (3345909)lrs+1011_1_anc=none:ncem=casc2026/models/loop2.pt:sil=32000:tgt=full:npcc=on:fde=unused:sas=cadical:sp=const_frequency:spb=non_intro:lsd=10:lcm=predicate:rp=on:sac=on:newcnf=on:random_seed=1106600368:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2902 on theBenchmark for (2902ds/11035Mi) % 135.60/19.87 % (3345909)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 135.60/19.87 % Exception at run slice level % 135.60/19.87 User error: GNN currently only supports monomorphic FOL. % 135.60/19.87 % (3345913)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=1945356948:i=5835_2901 on theBenchmark for (2901ds/5835Mi) % 135.60/19.87 % Exception at run slice level % 135.60/19.87 User error: GNN currently only supports monomorphic FOL. % 135.60/19.87 % Exception at run slice level % 135.60/19.87 User error: GNN currently only supports monomorphic FOL. % 135.60/19.87 % Exception at run slice level % 135.60/19.87 User error: GNN currently only supports monomorphic FOL. % 135.60/19.87 % (3345915)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=2538824418:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2898 on theBenchmark for (2898ds/5890Mi) % 135.60/19.87 % (3345916)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=1493419490:cts=off:i=19910:ep=RS_2898 on theBenchmark for (2898ds/19910Mi) % 160.80/23.30 % (3345917)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:drc=off:sp=arity:fd=preordered:s2agt=16:sac=on:random_seed=1078300671:i=20312:bd=preordered:fsr=off:er=filter_2898 on theBenchmark for (2898ds/20312Mi) % 160.80/23.30 % Exception at run slice level % 160.80/23.30 User error: GNN currently only supports monomorphic FOL. % 160.80/23.30 % (3345921)lrs+1011_1_ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal_then_units:urr=on:gs=on:sac=on:random_seed=1328046714:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2896 on theBenchmark for (2896ds/13822Mi) % 160.80/23.30 % Exception at run slice level % 160.80/23.30 User error: GNN currently only supports monomorphic FOL. % 160.80/23.30 % Exception at run slice level % 160.80/23.30 User error: GNN currently only supports monomorphic FOL. % 160.80/23.30 % (3345923)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=3680637338:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2893 on theBenchmark for (2893ds/7144Mi) % 160.80/23.30 % (3345924)lrs+21_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=2001754229:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2893 on theBenchmark for (2893ds/15184Mi) % 160.80/23.30 % Exception at run slice level % 160.80/23.30 User error: GNN currently only supports monomorphic FOL. % 160.80/23.30 % (3345927)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1042730880:i=107375_2891 on theBenchmark for (2891ds/107375Mi) % 160.80/23.30 % Exception at run slice level % 160.80/23.30 User error: GNN currently only supports monomorphic FOL. % 160.80/23.30 % (3345929)dis+11_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=full:npcc=on:sp=const_frequency:spb=units:lcm=predicate:fd=off:sac=on:newcnf=on:random_seed=2464718497:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2888 on theBenchmark for (2888ds/7958Mi) % 160.80/23.30 % Exception at run slice level % 160.80/23.30 User error: GNN currently only supports monomorphic FOL. % 160.80/23.30 % (3345931)dis+10_128_sil=16000:nwc=0.7:random_seed=574366027:i=15999:nm=2:gsp=on_2886 on theBenchmark for (2886ds/15999Mi) % 160.80/23.30 % (3345931)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 160.80/23.30 % Exception at run slice level % 160.80/23.30 User error: GNN currently only supports monomorphic FOL. % 160.80/23.30 % (3345933)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=3382035332:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2883 on theBenchmark for (2883ds/8139Mi) % 160.80/23.30 % (3345923)Instruction limit reached! % 160.80/23.30 % (3345923)------------------------------ % 160.80/23.30 % (3345923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.80/23.30 % (3345923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.80/23.30 % (3345923)CaDiCaL version: 2.1.3 % 160.80/23.30 % (3345923)Termination reason: Instruction limit % 160.80/23.30 % (3345923)Termination phase: Saturation % 160.80/23.30 % (3345923)Time elapsed: 3.416 s % 160.80/23.30 % (3345923)Peak memory usage: 176 MB % 160.80/23.30 % (3345923)Instructions burned: 7147 (million) % 160.80/23.30 % (3346181)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=1132357956:st=4:i=8950:sd=5:ss=axioms_2858 on theBenchmark for (2858ds/8950Mi) % 160.80/23.30 % Exception at run slice level % 160.80/23.30 User error: GNN currently only supports monomorphic FOL. % 160.80/23.30 % (3346191)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=2571453473:i=9809:ins=10:av=off_2852 on theBenchmark for (2852ds/9809Mi) % 160.80/23.30 % Exception at run slice level % 160.80/23.30 User error: GNN currently only supports monomorphic FOL. % 160.80/23.30 % (3346202)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=3242373964:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2845 on theBenchmark for (2845ds/9885Mi) % 160.80/23.30 % Exception at run slice level % 160.80/23.30 User error: GNN currently only supports monomorphic FOL. % 160.80/23.30 % (3346281)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=1059675487:cond=fast:i=32078:fgj=on:av=off_2841 on theBenchmark for (2841ds/32078Mi) % 171.83/25.00 % (3345933)Instruction limit reached! % 171.83/25.00 % (3345933)------------------------------ % 171.83/25.00 % (3345933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.83/25.00 % (3345933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.83/25.00 % (3345933)CaDiCaL version: 2.1.3 % 171.83/25.00 % (3345933)Termination reason: Instruction limit % 171.83/25.00 % (3345933)Termination phase: Saturation % 171.83/25.00 % (3345933)Time elapsed: 4.226 s % 171.83/25.00 % (3345933)Peak memory usage: 146 MB % 171.83/25.00 % (3345933)Instructions burned: 8140 (million) % 171.83/25.00 % (3346312)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=2796350706:i=11101:bd=all:ss=axioms:sgt=8_2839 on theBenchmark for (2839ds/11101Mi) % 171.83/25.00 % Exception at run slice level % 171.83/25.00 User error: GNN currently only supports monomorphic FOL. % 171.83/25.00 % (3346361)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=3415211166:cond=on:i=13220:s2at=3:aac=none:fsd=on_2836 on theBenchmark for (2836ds/13220Mi) % 171.83/25.00 % Exception at run slice level % 171.83/25.00 User error: GNN currently only supports monomorphic FOL. % 171.83/25.00 % (3346363)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=168007541:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2831 on theBenchmark for (2831ds/13528Mi) % 171.83/25.00 % Exception at run slice level % 171.83/25.00 User error: GNN currently only supports monomorphic FOL. % 171.83/25.00 % (3346365)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:sp=reverse_frequency:bce=on:bsr=unit_only:s2agt=32:newcnf=on:random_seed=2895118165:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2826 on theBenchmark for (2826ds/14854Mi) % 171.83/25.00 % Exception at run slice level % 171.83/25.00 User error: GNN currently only supports monomorphic FOL. % 171.83/25.00 % (3346367)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=176847148:i=14974:ss=axioms:sgt=16_2821 on theBenchmark for (2821ds/14974Mi) % 171.83/25.00 % (3345825)Instruction limit reached! % 171.83/25.00 % (3345825)------------------------------ % 171.83/25.00 % (3345825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.83/25.00 % (3345825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.83/25.00 % (3345825)CaDiCaL version: 2.1.3 % 171.83/25.00 % (3345825)Termination reason: Instruction limit % 171.83/25.00 % (3345825)Termination phase: Saturation % 171.83/25.00 % (3345825)Time elapsed: 13.344 s % 171.83/25.00 % (3345825)Peak memory usage: 190 MB % 171.83/25.00 % (3345825)Instructions burned: 26475 (million) % 171.83/25.00 % Exception at run slice level % 171.83/25.00 User error: GNN currently only supports monomorphic FOL. % 171.83/25.00 % (3346369)lrs-1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:sas=cadical:sp=arity:spb=units:lsd=1:acc=on:urr=ec_only:fd=preordered:gs=on:s2agt=16:random_seed=628864042:i=33081:aac=none:fgj=on:bd=all:fsr=off_2817 on theBenchmark for (2817ds/33081Mi) % 171.83/25.00 % (3346370)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sims=off:sas=cadical:etr=on:spb=goal:acc=on:s2agt=60:alpa=true:random_seed=874404116:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2816 on theBenchmark for (2816ds/50856Mi) % 171.83/25.00 % Exception at run slice level % 171.83/25.00 User error: GNN currently only supports monomorphic FOL. % 171.83/25.00 % Exception at run slice level % 171.83/25.00 User error: GNN currently only supports monomorphic FOL. % 171.83/25.00 % (3346373)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=77881148:i=69865_2812 on theBenchmark for (2812ds/69865Mi) % 171.83/25.00 % (3346374)lrs+1002_1_anc=none:to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:sp=arity:sos=on:spb=intro:lcm=reverse:random_seed=817198345:cond=fast:i=17802:gtgl=3:gtg=all_2811 on theBenchmark for (2811ds/17802Mi) % 171.83/25.00 % Exception at run slice level % 171.83/25.00 User error: Immediate (shared) subterms of term/literal combs(X0,bool,bool,sF68(X0,X1),sF90(X0,X2,X3,X4,X1)) have different types/not well-typed! % 171.83/25.00 % (3346377)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=110893254:i=96644_2810 on theBenchmark for (2810ds/96644Mi) % 171.83/25.00 % Exception at run slice level % 171.83/25.00 User error: GNN currently only supports monomorphic FOL. % 181.05/26.19 % (3346379)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 181.05/26.19 % (3346379)dis+1011_1_to=kbo:ncem=casc2026/models/loop8.pt:tgt=ground:irw=on:drc=off:sp=unary_first:bce=on:bsr=unit_only:kmz=on:sac=on:random_seed=424030355:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2807 on theBenchmark for (2807ds/21161Mi) % 181.05/26.19 % (3345931)Instruction limit reached! % 181.05/26.19 % (3345931)------------------------------ % 181.05/26.19 % (3345931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.05/26.19 % (3345931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.05/26.19 % (3345931)CaDiCaL version: 2.1.3 % 181.05/26.19 % (3345931)Termination reason: Instruction limit % 181.05/26.19 % (3345931)Termination phase: Saturation % 181.05/26.19 % (3345931)Time elapsed: 8.527 s % 181.05/26.19 % (3345931)Peak memory usage: 156 MB % 181.05/26.19 % (3345931)Instructions burned: 16000 (million) % 181.05/26.19 % (3346381)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:sp=const_frequency:sos=all:lcm=predicate:urr=on:s2agt=20:sac=on:random_seed=2718786652:i=22761:gtg=all:ss=axioms:fsd=on_2800 on theBenchmark for (2800ds/22761Mi) % 181.05/26.19 % Exception at run slice level % 181.05/26.19 User error: GNN currently only supports monomorphic FOL. % 181.05/26.19 % (3346383)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=2696499521:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2795 on theBenchmark for (2795ds/23713Mi) % 181.05/26.19 % (3345916)Instruction limit reached! % 181.05/26.19 % (3345916)------------------------------ % 181.05/26.19 % (3345916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.05/26.19 % (3345916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.05/26.19 % (3345916)CaDiCaL version: 2.1.3 % 181.05/26.19 % (3345916)Termination reason: Instruction limit % 181.05/26.19 % (3345916)Termination phase: Saturation % 181.05/26.19 % (3345916)Time elapsed: 10.718 s % 181.05/26.19 % (3345916)Peak memory usage: 124 MB % 181.05/26.19 % (3345916)Instructions burned: 19911 (million) % 181.05/26.19 % (3346385)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=453091909:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2789 on theBenchmark for (2789ds/26509Mi) % 181.05/26.19 % Exception at run slice level % 181.05/26.19 User error: GNN currently only supports monomorphic FOL. % 181.05/26.19 % (3346387)dis+1011_1_to=kbo:ncem=casc2026/models/loop6.pt:tgt=ground:drc=off:fde=unused:sp=const_frequency:spb=units:bsr=on:sac=on:random_seed=2079667883:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2784 on theBenchmark for (2784ds/28957Mi) % 181.05/26.19 % (3345893)Instruction limit reached! % 181.05/26.19 % (3345893)------------------------------ % 181.05/26.19 % (3345893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.05/26.19 % (3345893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.05/26.19 % (3345893)CaDiCaL version: 2.1.3 % 181.05/26.19 % (3345893)Termination reason: Instruction limit % 181.05/26.19 % (3345893)Termination phase: Saturation % 181.05/26.19 % (3345893)Time elapsed: 13.456 s % 181.05/26.19 % (3345893)Peak memory usage: 353 MB % 181.05/26.19 % (3345893)Instructions burned: 43701 (million) % 181.05/26.19 % (3346389)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:drc=off:sp=const_max:spb=goal_then_units:lcm=predicate:urr=ec_only:fd=preordered:gs=on:sac=on:random_seed=1219865088:i=29246:s2at=-1:kws=inv_arity:ins=10_2777 on theBenchmark for (2777ds/29246Mi) % 181.05/26.19 % (3346312)Instruction limit reached! % 181.05/26.19 % (3346312)------------------------------ % 181.05/26.19 % (3346312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.05/26.19 % (3346312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.05/26.19 % (3346312)CaDiCaL version: 2.1.3 % 181.05/26.19 % (3346312)Termination reason: Instruction limit % 181.05/26.19 % (3346312)Termination phase: Saturation % 181.05/26.19 % (3346312)Time elapsed: 6.369 s % 181.05/26.19 % (3346312)Peak memory usage: 146 MB % 181.05/26.19 % (3346312)Instructions burned: 11102 (million) % 181.05/26.19 % Exception at run slice level % 181.05/26.19 User error: GNN currently only supports monomorphic FOL. % 181.05/26.19 % (3346392)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=3348513539:i=32262:bd=preordered_2774 on theBenchmark for (2774ds/32262Mi) % 187.45/27.07 % (3346391)ott+1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:sp=weighted_frequency:urr=on:gs=on:s2agt=32:sac=on:random_seed=4252527426:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2774 on theBenchmark for (2774ds/30082Mi) % 187.45/27.07 % (3346391)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 187.45/27.07 % Exception at run slice level % 187.45/27.07 User error: GNN currently only supports monomorphic FOL. % 187.45/27.07 % (3346395)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=1579498599:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2771 on theBenchmark for (2771ds/32870Mi) % 187.45/27.07 % Exception at run slice level % 187.45/27.07 User error: GNN currently only supports monomorphic FOL. % 187.45/27.07 % (3345798)Instruction limit reached! % 187.45/27.07 % (3345798)------------------------------ % 187.45/27.07 % (3345798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.45/27.07 % (3345798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.45/27.07 % (3345798)CaDiCaL version: 2.1.3 % 187.45/27.07 % (3345798)Termination reason: Instruction limit % 187.45/27.07 % (3345798)Termination phase: Saturation % 187.45/27.07 % (3345798)Time elapsed: 19.769 s % 187.45/27.07 % (3345798)Peak memory usage: 275 MB % 187.45/27.07 % (3345798)Instructions burned: 33335 (million) % 187.45/27.07 % Exception at run slice level % 187.45/27.07 User error: GNN currently only supports monomorphic FOL. % 187.45/27.07 % (3346397)lrs-1010_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:prc=on:sp=reverse_frequency:spb=goal:acc=on:kmz=on:random_seed=3560702591:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2769 on theBenchmark for (2769ds/33295Mi) % 187.45/27.07 % (3346398)dis+11_1_anc=none:sfv=off:to=kbo:ncem=casc2026/models/loop6.pt:lma=off:bsr=unit_only:s2agt=8:kmz=on:sac=on:random_seed=1631475878:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2769 on theBenchmark for (2769ds/36826Mi) % 187.45/27.07 % (3346399)lrs-1003_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:spb=goal:bsr=unit_only:gs=on:br=off:flr=on:sac=on:random_seed=3974735832:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2768 on theBenchmark for (2768ds/92981Mi) % 187.45/27.07 % Exception at run slice level % 187.45/27.07 User error: GNN currently only supports monomorphic FOL. % 187.45/27.07 % (3346403)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=3629743412:s2pl=on:i=49423_2765 on theBenchmark for (2765ds/49423Mi) % 187.45/27.07 % Exception at run slice level % 187.45/27.07 User error: GNN currently only supports monomorphic FOL. % 187.45/27.07 % (3346405)lrs+1002_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:tgt=ground:npcc=on:prc=on:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:rp=on:updr=off:sac=on:random_seed=4125859189:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2764 on theBenchmark for (2764ds/57299Mi) % 187.45/27.07 % Exception at run slice level % 187.45/27.07 User error: GNN currently only supports monomorphic FOL. % 187.45/27.07 % (3346407)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=3536732661:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2763 on theBenchmark for (2763ds/127679Mi) % 187.45/27.07 % Exception at run slice level % 187.45/27.07 User error: GNN currently only supports monomorphic FOL. % 187.45/27.07 % Exception at run slice level % 187.45/27.07 User error: GNN currently only supports monomorphic FOL. % 187.45/27.07 % (3346409)lrs+31_1_anc=all:to=lpo:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_arity:fs=off:lcm=predicate:alpa=false:flr=on:random_seed=3430439897:i=69402:add=on:aac=none:fsr=off_2760 on theBenchmark for (2760ds/69402Mi) % 187.45/27.07 % (3346410)lrs-2_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:drc=off:sas=cadical:sp=reverse_frequency:lcm=predicate:acc=on:bsr=unit_only:fd=preordered:sac=on:random_seed=741268017:i=100512:doe=on:fgj=on:bd=all:fsd=on_2760 on theBenchmark for (2760ds/100512Mi) % 187.45/27.07 % Exception at run slice level % 187.45/27.07 User error: GNN currently only supports monomorphic FOL. % 187.45/27.07 % (3346413)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=3493639600:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2757 on theBenchmark for (2757ds/138761Mi) % 197.51/28.59 % Exception at run slice level % 197.51/28.59 User error: GNN currently only supports monomorphic FOL. % 197.51/28.59 % Exception at run slice level % 197.51/28.59 User error: GNN currently only supports monomorphic FOL. % 197.51/28.59 % (3346415)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:si=on:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2992067206:i=282386:rtra=on_2755 on theBenchmark for (2755ds/282386Mi) % 197.51/28.59 % (3346416)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:si=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2503205819:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2754 on theBenchmark for (2754ds/269354Mi) % 197.51/28.59 % Exception at run slice level % 197.51/28.59 User error: GNN currently only supports monomorphic FOL. % 197.51/28.59 % (3346419)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:si=on:sos=all:bsr=unit_only:sac=on:random_seed=1188766419:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2751 on theBenchmark for (2751ds/283390Mi) % 197.51/28.59 % (3346419)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 197.51/28.59 % Exception at run slice level % 197.51/28.59 User error: GNN currently only supports monomorphic FOL. % 197.51/28.59 % (3346421)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=1320895641:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2750 on theBenchmark for (2750ds/218Mi) % 197.51/28.59 % Exception at run slice level % 197.51/28.59 User error: GNN currently only supports monomorphic FOL. % 197.51/28.59 % (3346421)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 197.51/28.59 % (3346423)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=3500930157:i=238:av=off:rtra=on:ss=axioms_2748 on theBenchmark for (2748ds/238Mi) % 197.51/28.59 % (3346421)Instruction limit reached! % 197.51/28.59 % (3346421)------------------------------ % 197.51/28.59 % (3346421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.51/28.59 % (3346421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.51/28.59 % (3346421)CaDiCaL version: 2.1.3 % 197.51/28.59 % (3346421)Termination reason: Instruction limit % 197.51/28.59 % (3346421)Termination phase: Saturation % 197.51/28.59 % (3346421)Time elapsed: 0.133 s % 197.51/28.59 % (3346421)Peak memory usage: 90 MB % 197.51/28.59 % (3346421)Instructions burned: 218 (million) % 197.51/28.59 % (3346423)Instruction limit reached! % 197.51/28.59 % (3346423)------------------------------ % 197.51/28.59 % (3346423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.51/28.59 % (3346423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.51/28.59 % (3346423)CaDiCaL version: 2.1.3 % 197.51/28.59 % (3346423)Termination reason: Instruction limit % 197.51/28.59 % (3346423)Termination phase: Saturation % 197.51/28.59 % (3346423)Time elapsed: 0.073 s % 197.51/28.59 % (3346423)Peak memory usage: 90 MB % 197.51/28.59 % (3346423)Instructions burned: 238 (million) % 197.51/28.59 % (3346426)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=2186793738:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2747 on theBenchmark for (2747ds/258Mi) % 197.51/28.59 % (3346425)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=674029926:s2a=on:i=278:rtra=on:gtg=position_2747 on theBenchmark for (2747ds/278Mi) % 197.51/28.59 % (3346426)Instruction limit reached! % 197.51/28.59 % (3346426)------------------------------ % 197.51/28.59 % (3346426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.51/28.59 % (3346426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.51/28.59 % (3346426)CaDiCaL version: 2.1.3 % 197.51/28.59 % (3346426)Termination reason: Instruction limit % 197.51/28.59 % (3346426)Termination phase: Saturation % 197.51/28.59 % (3346426)Time elapsed: 0.076 s % 197.51/28.59 % (3346426)Peak memory usage: 90 MB % 197.51/28.59 % (3346426)Instructions burned: 259 (million) % 197.51/28.59 % (3346429)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=650896959:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2745 on theBenchmark for (2745ds/570Mi) % 197.51/28.59 % (3346425)Instruction limit reached! % 197.51/28.59 % (3346425)------------------------------ % 197.51/28.59 % (3346425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.51/28.59 % (3346425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.49/29.53 % (3346425)CaDiCaL version: 2.1.3 % 204.49/29.53 % (3346425)Termination reason: Instruction limit % 204.49/29.53 % (3346425)Termination phase: Saturation % 204.49/29.53 % (3346425)Time elapsed: 0.176 s % 204.49/29.53 % (3346425)Peak memory usage: 91 MB % 204.49/29.53 % (3346425)Instructions burned: 278 (million) % 204.49/29.53 % (3346431)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=2406094563:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2744 on theBenchmark for (2744ds/314Mi) % 204.49/29.53 % (3346429)Instruction limit reached! % 204.49/29.53 % (3346429)------------------------------ % 204.49/29.53 % (3346429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.49/29.53 % (3346429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.49/29.53 % (3346429)CaDiCaL version: 2.1.3 % 204.49/29.53 % (3346429)Termination reason: Instruction limit % 204.49/29.53 % (3346429)Termination phase: Saturation % 204.49/29.53 % (3346429)Time elapsed: 0.187 s % 204.49/29.53 % (3346429)Peak memory usage: 93 MB % 204.49/29.53 % (3346429)Instructions burned: 571 (million) % 204.49/29.53 % (3346433)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=1206819810:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2742 on theBenchmark for (2742ds/650Mi) % 204.49/29.53 % (3346431)Instruction limit reached! % 204.49/29.53 % (3346431)------------------------------ % 204.49/29.53 % (3346431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.49/29.53 % (3346431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.49/29.53 % (3346431)CaDiCaL version: 2.1.3 % 204.49/29.53 % (3346431)Termination reason: Instruction limit % 204.49/29.53 % (3346431)Termination phase: Saturation % 204.49/29.53 % (3346431)Time elapsed: 0.169 s % 204.49/29.53 % (3346431)Peak memory usage: 90 MB % 204.49/29.53 % (3346431)Instructions burned: 315 (million) % 204.49/29.53 % (3346435)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:si=on:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2993128305:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2741 on theBenchmark for (2741ds/496Mi) % 204.49/29.53 % (3346433)Instruction limit reached! % 204.49/29.53 % (3346433)------------------------------ % 204.49/29.53 % (3346433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.49/29.53 % (3346433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.49/29.53 % (3346433)CaDiCaL version: 2.1.3 % 204.49/29.53 % (3346433)Termination reason: Instruction limit % 204.49/29.53 % (3346433)Termination phase: Saturation % 204.49/29.53 % (3346433)Time elapsed: 0.207 s % 204.49/29.53 % (3346433)Peak memory usage: 92 MB % 204.49/29.53 % (3346433)Instructions burned: 650 (million) % 204.49/29.53 % (3346437)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=468320711:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2740 on theBenchmark for (2740ds/588Mi) % 204.49/29.53 % (3346435)Instruction limit reached! % 204.49/29.53 % (3346435)------------------------------ % 204.49/29.53 % (3346435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.49/29.53 % (3346435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.49/29.53 % (3346435)CaDiCaL version: 2.1.3 % 204.49/29.53 % (3346435)Termination reason: Instruction limit % 204.49/29.53 % (3346435)Termination phase: Saturation % 204.49/29.53 % (3346435)Time elapsed: 0.273 s % 204.49/29.53 % (3346435)Peak memory usage: 91 MB % 204.49/29.53 % (3346435)Instructions burned: 496 (million) % 204.49/29.53 % (3346437)Instruction limit reached! % 204.49/29.53 % (3346437)------------------------------ % 204.49/29.53 % (3346437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.49/29.53 % (3346437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.49/29.53 % (3346437)CaDiCaL version: 2.1.3 % 204.49/29.53 % (3346437)Termination reason: Instruction limit % 204.49/29.53 % (3346437)Termination phase: Saturation % 204.49/29.53 % (3346437)Time elapsed: 0.179 s % 204.49/29.53 % (3346437)Peak memory usage: 90 MB % 204.49/29.53 % (3346437)Instructions burned: 591 (million) % 204.49/29.53 % (3346440)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3096350989:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2737 on theBenchmark for (2737ds/226Mi) % 204.49/29.53 % (3346439)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=3373637284:i=4700:rtra=on_2737 on theBenchmark for (2737ds/4700Mi) % 204.49/29.53 % (3346440)Instruction limit reached! % 204.49/29.53 % (3346440)------------------------------ % 204.49/29.53 % (3346440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.71/30.89 % (3346440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.71/30.89 % (3346440)CaDiCaL version: 2.1.3 % 213.71/30.89 % (3346440)Termination reason: Instruction limit % 213.71/30.89 % (3346440)Termination phase: Saturation % 213.71/30.89 % (3346440)Time elapsed: 0.067 s % 213.71/30.89 % (3346440)Peak memory usage: 90 MB % 213.71/30.89 % (3346440)Instructions burned: 229 (million) % 213.71/30.89 % (3346443)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=266398443:i=254:av=off:fsr=off:rtra=on:sup=off_2735 on theBenchmark for (2735ds/254Mi) % 213.71/30.89 % (3346443)Refutation not found, incomplete strategy % 213.71/30.89 % (3346443)------------------------------ % 213.71/30.89 % (3346443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.71/30.89 % (3346443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.71/30.89 % (3346443)CaDiCaL version: 2.1.3 % 213.71/30.89 % (3346443)Termination reason: Refutation not found, incomplete strategy % 213.71/30.89 % (3346443)Time elapsed: 0.007 s % 213.71/30.89 % (3346443)Peak memory usage: 88 MB % 213.71/30.89 % (3346443)Instructions burned: 25 (million) % 213.71/30.89 % (3346443)------------------------------ % 213.71/30.89 % (3346443)------------------------------ % 213.71/30.89 % Exception at run slice level % 213.71/30.89 User error: GNN currently only supports monomorphic FOL. % 213.71/30.89 % (3346445)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=1012362023:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2733 on theBenchmark for (2733ds/228Mi) % 213.71/30.89 % (3346445)Instruction limit reached! % 213.71/30.89 % (3346445)------------------------------ % 213.71/30.89 % (3346445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.71/30.89 % (3346445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.71/30.89 % (3346445)CaDiCaL version: 2.1.3 % 213.71/30.89 % (3346445)Termination reason: Instruction limit % 213.71/30.89 % (3346445)Termination phase: Saturation % 213.71/30.89 % (3346445)Time elapsed: 0.063 s % 213.71/30.89 % (3346445)Peak memory usage: 89 MB % 213.71/30.89 % (3346445)Instructions burned: 232 (million) % 213.71/30.89 % (3346446)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=1119547808:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2732 on theBenchmark for (2732ds/1814Mi) % 213.71/30.89 % (3346448)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=3182883576:i=874:sd=1:aac=none:rtra=on:ss=included_2731 on theBenchmark for (2731ds/874Mi) % 213.71/30.89 % (3346448)Refutation not found, incomplete strategy % 213.71/30.89 % (3346448)------------------------------ % 213.71/30.89 % (3346448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.71/30.89 % (3346448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.71/30.89 % (3346448)CaDiCaL version: 2.1.3 % 213.71/30.89 % (3346448)Termination reason: Refutation not found, incomplete strategy % 213.71/30.89 % (3346448)Time elapsed: 0.008 s % 213.71/30.89 % (3346448)Peak memory usage: 89 MB % 213.71/30.89 % (3346448)Instructions burned: 24 (million) % 213.71/30.89 % (3346448)------------------------------ % 213.71/30.89 % (3346448)------------------------------ % 213.71/30.89 % (3346451)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=2233126437:i=10404:rtra=on:ss=axioms:sgt=16_2729 on theBenchmark for (2729ds/10404Mi) % 213.71/30.89 % Exception at run slice level % 213.71/30.89 User error: GNN currently only supports monomorphic FOL. % 213.71/30.89 % (3346453)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1367432038:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2726 on theBenchmark for (2726ds/268Mi) % 213.71/30.89 % (3346453)Instruction limit reached! % 213.71/30.89 % (3346453)------------------------------ % 213.71/30.89 % (3346453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.71/30.89 % (3346453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.71/30.89 % (3346453)CaDiCaL version: 2.1.3 % 213.71/30.89 % (3346453)Termination reason: Instruction limit % 213.71/30.89 % (3346453)Termination phase: Saturation % 213.71/30.89 % (3346453)Time elapsed: 0.079 s % 213.71/30.89 % (3346453)Peak memory usage: 91 MB % 213.71/30.89 % (3346453)Instructions burned: 270 (million) % 213.71/30.89 % (3346455)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=3165623721:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2725 on theBenchmark for (2725ds/1184Mi) % 213.71/30.89 % (3346446)Instruction limit reached! % 237.43/34.09 % (3346446)------------------------------ % 237.43/34.09 % (3346446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.43/34.09 % (3346446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.43/34.09 % (3346446)CaDiCaL version: 2.1.3 % 237.43/34.09 % (3346446)Termination reason: Instruction limit % 237.43/34.09 % (3346446)Termination phase: Saturation % 237.43/34.09 % (3346446)Time elapsed: 1.091 s % 237.43/34.09 % (3346446)Peak memory usage: 102 MB % 237.43/34.09 % (3346446)Instructions burned: 1815 (million) % 237.43/34.09 % (3346455)Instruction limit reached! % 237.43/34.09 % (3346455)------------------------------ % 237.43/34.09 % (3346455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.43/34.09 % (3346455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.43/34.09 % (3346455)CaDiCaL version: 2.1.3 % 237.43/34.09 % (3346455)Termination reason: Instruction limit % 237.43/34.09 % (3346455)Termination phase: Saturation % 237.43/34.09 % (3346455)Time elapsed: 0.377 s % 237.43/34.09 % (3346455)Peak memory usage: 99 MB % 237.43/34.09 % (3346455)Instructions burned: 1184 (million) % 237.43/34.09 % (3346498)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:si=on:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=239376895:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2720 on theBenchmark for (2720ds/250Mi) % 237.43/34.09 % (3346498)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 237.43/34.09 % (3346487)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=1314415873:st=3:i=26386:sd=3:rtra=on:ss=axioms_2720 on theBenchmark for (2720ds/26386Mi) % 237.43/34.09 % (3346498)Instruction limit reached! % 237.43/34.09 % (3346498)------------------------------ % 237.43/34.09 % (3346498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.43/34.09 % (3346498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.43/34.09 % (3346498)CaDiCaL version: 2.1.3 % 237.43/34.09 % (3346498)Termination reason: Instruction limit % 237.43/34.09 % (3346498)Termination phase: Saturation % 237.43/34.09 % (3346498)Time elapsed: 0.079 s % 237.43/34.09 % (3346498)Peak memory usage: 92 MB % 237.43/34.09 % (3346498)Instructions burned: 252 (million) % 237.43/34.09 % (3346568)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=3404330581:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2718 on theBenchmark for (2718ds/268Mi) % 237.43/34.09 % Exception at run slice level % 237.43/34.09 User error: Immediate (shared) subterms of term/literal aa(X0,X2,combs(X0,X1,X2,X3,X4),X5) = sF98(X0,X2,X1,X3,X4,X5) have different types/not well-typed! % 237.43/34.09 % (3346579)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4144418863:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2717 on theBenchmark for (2717ds/282Mi) % 237.43/34.09 % (3346579)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 237.43/34.09 % (3346579)Refutation not found, incomplete strategy % 237.43/34.09 % (3346579)------------------------------ % 237.43/34.09 % (3346579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.43/34.09 % (3346579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.43/34.09 % (3346579)CaDiCaL version: 2.1.3 % 237.43/34.09 % (3346579)Termination reason: Refutation not found, incomplete strategy % 237.43/34.09 % (3346579)Time elapsed: 0.003 s % 237.43/34.09 % (3346579)Peak memory usage: 88 MB % 237.43/34.09 % (3346579)Instructions burned: 8 (million) % 237.43/34.09 % Exception at run slice level % 237.43/34.09 User error: GNN currently only supports monomorphic FOL. % 237.43/34.09 % (3346579)------------------------------ % 237.43/34.09 % (3346579)------------------------------ % 237.43/34.09 % (3346581)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=1952349617:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2715 on theBenchmark for (2715ds/862Mi) % 237.43/34.09 % (3346582)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:si=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2272346087:i=12120:aac=none:ins=25:rtra=on_2715 on theBenchmark for (2715ds/12120Mi) % 237.43/34.09 % Exception at run slice level % 237.43/34.09 User error: GNN currently only supports monomorphic FOL. % 237.43/34.09 % (3346651)lrs+10_16_anc=all:slsqr=32,1:sil=8000:si=on:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1772301039:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2712 on theBenchmark for (2712ds/300Mi) % 255.75/36.75 % (3346651)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 255.75/36.75 % (3346651)Instruction limit reached! % 255.75/36.75 % (3346651)------------------------------ % 255.75/36.75 % (3346651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.75/36.75 % (3346651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.75/36.75 % (3346651)CaDiCaL version: 2.1.3 % 255.75/36.75 % (3346651)Termination reason: Instruction limit % 255.75/36.75 % (3346651)Termination phase: Saturation % 255.75/36.75 % (3346651)Time elapsed: 0.094 s % 255.75/36.75 % (3346651)Peak memory usage: 91 MB % 255.75/36.75 % (3346651)Instructions burned: 305 (million) % 255.75/36.75 % (3346581)Instruction limit reached! % 255.75/36.75 % (3346581)------------------------------ % 255.75/36.75 % (3346581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.75/36.75 % (3346581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.75/36.75 % (3346581)CaDiCaL version: 2.1.3 % 255.75/36.75 % (3346581)Termination reason: Instruction limit % 255.75/36.75 % (3346581)Termination phase: Saturation % 255.75/36.75 % (3346581)Time elapsed: 0.455 s % 255.75/36.75 % (3346581)Peak memory usage: 93 MB % 255.75/36.75 % (3346581)Instructions burned: 862 (million) % 255.75/36.75 % (3346712)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=178878259:i=28310:bd=all:rtra=on_2710 on theBenchmark for (2710ds/28310Mi) % 255.75/36.75 % (3346725)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=551181122:i=1334:av=off:fsr=off:rtra=on_2709 on theBenchmark for (2709ds/1334Mi) % 255.75/36.75 % (3346725)Refutation not found, incomplete strategy % 255.75/36.75 % (3346725)------------------------------ % 255.75/36.75 % (3346725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.75/36.75 % (3346725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.75/36.75 % (3346725)CaDiCaL version: 2.1.3 % 255.75/36.75 % (3346725)Termination reason: Refutation not found, incomplete strategy % 255.75/36.75 % (3346725)Time elapsed: 0.031 s % 255.75/36.75 % (3346725)Peak memory usage: 89 MB % 255.75/36.75 % (3346725)Instructions burned: 33 (million) % 255.75/36.75 % Exception at run slice level % 255.75/36.75 User error: GNN currently only supports monomorphic FOL. % 255.75/36.75 % (3346749)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:si=on:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3967785251:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2705 on theBenchmark for (2705ds/370Mi) % 255.75/36.75 % (3346725)------------------------------ % 255.75/36.75 % (3346725)------------------------------ % 255.75/36.75 % (3346749)Instruction limit reached! % 255.75/36.75 % (3346749)------------------------------ % 255.75/36.75 % (3346749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.75/36.75 % (3346749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.75/36.75 % (3346749)CaDiCaL version: 2.1.3 % 255.75/36.75 % (3346749)Termination reason: Instruction limit % 255.75/36.75 % (3346749)Termination phase: Saturation % 255.75/36.75 % (3346749)Time elapsed: 0.195 s % 255.75/36.75 % (3346749)Peak memory usage: 92 MB % 255.75/36.75 % (3346749)Instructions burned: 371 (million) % 255.75/36.75 % (3346751)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=663991988:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2703 on theBenchmark for (2703ds/386Mi) % 255.75/36.75 % (3346752)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=2196311438:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2701 on theBenchmark for (2701ds/9700Mi) % 255.75/36.75 % (3346752)Refutation not found, incomplete strategy % 255.75/36.75 % (3346752)------------------------------ % 255.75/36.75 % (3346752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.75/36.75 % (3346752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.75/36.75 % (3346752)CaDiCaL version: 2.1.3 % 255.75/36.75 % (3346752)Termination reason: Refutation not found, incomplete strategy % 255.75/36.75 % (3346752)Time elapsed: 0.011 s % 255.75/36.75 % (3346752)Peak memory usage: 88 MB % 255.75/36.75 % (3346752)Instructions burned: 22 (million) % 255.75/36.75 % (3346752)------------------------------ % 255.75/36.75 % (3346752)------------------------------ % 255.75/36.75 % (3346751)Instruction limit reached! % 277.21/39.80 % (3346751)------------------------------ % 277.21/39.80 % (3346751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.21/39.80 % (3346751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.21/39.80 % (3346751)CaDiCaL version: 2.1.3 % 277.21/39.80 % (3346751)Termination reason: Instruction limit % 277.21/39.80 % (3346751)Termination phase: Saturation % 277.21/39.80 % (3346751)Time elapsed: 0.370 s % 277.21/39.80 % (3346751)Peak memory usage: 92 MB % 277.21/39.80 % (3346751)Instructions burned: 386 (million) % 277.21/39.80 % (3346761)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:si=on:sp=const_frequency:acc=on:urr=on:random_seed=879250340:i=24222:sd=1:rtra=on:ss=included_2698 on theBenchmark for (2698ds/24222Mi) % 277.21/39.80 % (3346764)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=310606441:i=638:kws=precedence:fsr=off:rtra=on_2697 on theBenchmark for (2697ds/638Mi) % 277.21/39.80 % Exception at run slice level % 277.21/39.80 User error: GNN currently only supports monomorphic FOL. % 277.21/39.80 % (3346767)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=4137010622:i=4128:ep=RST:rtra=on_2694 on theBenchmark for (2694ds/4128Mi) % 277.21/39.80 % (3346764)Instruction limit reached! % 277.21/39.80 % (3346764)------------------------------ % 277.21/39.80 % (3346764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.21/39.80 % (3346764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.21/39.80 % (3346764)CaDiCaL version: 2.1.3 % 277.21/39.80 % (3346764)Termination reason: Instruction limit % 277.21/39.80 % (3346764)Termination phase: Saturation % 277.21/39.80 % (3346764)Time elapsed: 0.598 s % 277.21/39.80 % (3346764)Peak memory usage: 94 MB % 277.21/39.80 % (3346764)Instructions burned: 639 (million) % 277.21/39.80 % (3346775)dis-1011_128_sil=32000:si=on:random_seed=866703272:i=7412:ep=RST:av=off:rtra=on_2689 on theBenchmark for (2689ds/7412Mi) % 277.21/39.80 % (3346767)Instruction limit reached! % 277.21/39.80 % (3346767)------------------------------ % 277.21/39.80 % (3346767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.21/39.80 % (3346767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.21/39.80 % (3346767)CaDiCaL version: 2.1.3 % 277.21/39.80 % (3346767)Termination reason: Instruction limit % 277.21/39.80 % (3346767)Termination phase: Saturation % 277.21/39.80 % (3346767)Time elapsed: 1.788 s % 277.21/39.80 % (3346767)Peak memory usage: 102 MB % 277.21/39.80 % (3346767)Instructions burned: 4130 (million) % 277.21/39.80 % (3346779)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=804651439:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2674 on theBenchmark for (2674ds/1514Mi) % 277.21/39.80 % (3346779)Refutation not found, incomplete strategy % 277.21/39.80 % (3346779)------------------------------ % 277.21/39.80 % (3346779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.21/39.80 % (3346779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.21/39.80 % (3346779)CaDiCaL version: 2.1.3 % 277.21/39.80 % (3346779)Termination reason: Refutation not found, incomplete strategy % 277.21/39.80 % (3346779)Time elapsed: 0.016 s % 277.21/39.80 % (3346779)Peak memory usage: 89 MB % 277.21/39.80 % (3346779)Instructions burned: 27 (million) % 277.21/39.80 % (3346379)Instruction limit reached! % 277.21/39.80 % (3346379)------------------------------ % 277.21/39.80 % (3346379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.21/39.80 % (3346379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.21/39.80 % (3346379)CaDiCaL version: 2.1.3 % 277.21/39.80 % (3346379)Termination reason: Instruction limit % 277.21/39.80 % (3346379)Termination phase: Saturation % 277.21/39.80 % (3346379)Time elapsed: 13.415 s % 277.21/39.80 % (3346379)Peak memory usage: 204 MB % 277.21/39.80 % (3346379)Instructions burned: 21162 (million) % 277.21/39.80 % (3346779)------------------------------ % 277.21/39.80 % (3346779)------------------------------ % 277.21/39.80 % (3346781)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=768680178:i=27826:rtra=on:ss=axioms:sgt=8_2672 on theBenchmark for (2672ds/27826Mi) % 277.21/39.80 % (3346784)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=629146395:i=19850:aac=none:rtra=on_2670 on theBenchmark for (2670ds/19850Mi) % 277.21/39.80 % Exception at run slice level % 277.21/39.80 User error: GNN currently onTerminated %------------------------------------------------------------------------------