%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM953_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n009.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 12:17:41 PM UTC 2026 % Result : Timeout 292.48s 42.27s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM953_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.37 % Computer : n009.cluster.edu % 0.10/0.37 % Model : x86_64 x86_64 % 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.37 % Memory : 8046.5625MB % 0.10/0.37 % OS : Linux 6.8.0-71-generic % 0.10/0.37 % CPULimit : 300 % 0.10/0.37 % WCLimit : 300 % 0.10/0.37 % DateTime : Sun Sep 27 21:47:46 UTC 2026 % 0.10/0.37 % CPUTime : % 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.41 Running first-order theorem proving % 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 5.74/1.63 % (2429247)Detected formulas, will run a generic FOF schedule. % 5.74/1.63 % (2429257)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4004786882:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 5.74/1.63 % (2429256)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=552126653:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 5.74/1.63 % (2429252)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=4134834391:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 5.74/1.63 % (2429255)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1589037240:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 5.74/1.63 % (2429253)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=3550913595:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 5.74/1.63 % (2429254)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=1795288970:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 5.74/1.63 % (2429258)dis-21_1_sil=8000:lcm=predicate:random_seed=2356245242: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.74/1.63 % (2429255)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.74/1.63 % (2429254)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.74/1.63 % (2429255)Refutation not found, incomplete strategy % 5.74/1.63 % (2429255)------------------------------ % 5.74/1.63 % (2429255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.74/1.63 % (2429255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.74/1.63 % (2429255)CaDiCaL version: 2.1.3 % 5.74/1.63 % (2429255)Termination reason: Refutation not found, incomplete strategy % 5.74/1.63 % (2429255)Time elapsed: 0.004 s % 5.74/1.63 % (2429255)Peak memory usage: 88 MB % 5.74/1.63 % (2429255)Instructions burned: 4 (million) % 5.74/1.63 % (2429258)Instruction limit reached! % 5.74/1.63 % (2429258)------------------------------ % 5.74/1.63 % (2429258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.74/1.63 % (2429258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.74/1.63 % (2429258)CaDiCaL version: 2.1.3 % 5.74/1.63 % (2429258)Termination reason: Instruction limit % 5.74/1.63 % (2429258)Termination phase: Saturation % 5.74/1.63 % (2429258)Time elapsed: 0.057 s % 5.74/1.63 % (2429258)Peak memory usage: 89 MB % 5.74/1.63 % (2429258)Instructions burned: 130 (million) % 5.74/1.63 % (2429257)Instruction limit reached! % 5.74/1.63 % (2429257)------------------------------ % 5.74/1.63 % (2429257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.74/1.63 % (2429257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.74/1.63 % (2429257)CaDiCaL version: 2.1.3 % 5.74/1.63 % (2429257)Termination reason: Instruction limit % 5.74/1.63 % (2429257)Termination phase: Saturation % 5.74/1.63 % (2429257)Time elapsed: 0.062 s % 5.74/1.63 % (2429257)Peak memory usage: 89 MB % 5.74/1.63 % (2429257)Instructions burned: 139 (million) % 5.74/1.63 % (2429256)Instruction limit reached! % 5.74/1.63 % (2429256)------------------------------ % 5.74/1.63 % (2429256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.74/1.63 % (2429256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.74/1.63 % (2429256)CaDiCaL version: 2.1.3 % 5.74/1.63 % (2429256)Termination reason: Instruction limit % 5.74/1.63 % (2429256)Termination phase: Saturation % 5.74/1.63 % (2429256)Time elapsed: 0.067 s % 5.74/1.63 % (2429256)Peak memory usage: 88 MB % 5.74/1.63 % (2429256)Instructions burned: 120 (million) % 5.74/1.63 % (2429267)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3023751593:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 5.74/1.63 % (2429267)Instruction limit reached! % 5.74/1.63 % (2429267)------------------------------ % 5.74/1.63 % (2429267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.74/1.63 % (2429267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.74/1.63 % (2429267)CaDiCaL version: 2.1.3 % 7.39/1.89 % (2429267)Termination reason: Instruction limit % 7.39/1.89 % (2429267)Termination phase: Saturation % 7.39/1.89 % (2429267)Time elapsed: 0.045 s % 7.39/1.89 % (2429267)Peak memory usage: 89 MB % 7.39/1.89 % (2429267)Instructions burned: 157 (million) % 7.39/1.89 % (2429266)lrs+10_1_sil=8000:sp=occurrence:random_seed=1624724480:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 7.39/1.89 % (2429268)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3296525949:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 7.39/1.89 % (2429255)------------------------------ % 7.39/1.89 % (2429255)------------------------------ % 7.39/1.89 % (2429270)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=358151070:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi) % 7.39/1.89 % (2429266)Instruction limit reached! % 7.39/1.89 % (2429266)------------------------------ % 7.39/1.89 % (2429266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.39/1.89 % (2429266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.39/1.89 % (2429266)CaDiCaL version: 2.1.3 % 7.39/1.89 % (2429266)Termination reason: Instruction limit % 7.39/1.89 % (2429266)Termination phase: Saturation % 7.39/1.89 % (2429266)Time elapsed: 0.155 s % 7.39/1.89 % (2429266)Peak memory usage: 90 MB % 7.39/1.89 % (2429266)Instructions burned: 286 (million) % 7.39/1.89 % (2429270)Instruction limit reached! % 7.39/1.89 % (2429270)------------------------------ % 7.39/1.89 % (2429270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.39/1.89 % (2429270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.39/1.89 % (2429270)CaDiCaL version: 2.1.3 % 7.39/1.89 % (2429270)Termination reason: Instruction limit % 7.39/1.89 % (2429270)Termination phase: Saturation % 7.39/1.89 % (2429270)Time elapsed: 0.077 s % 7.39/1.89 % (2429270)Peak memory usage: 91 MB % 7.39/1.89 % (2429270)Instructions burned: 250 (million) % 7.39/1.89 % Exception at run slice level % 7.39/1.89 User error: GNN currently only supports monomorphic FOL. % 7.39/1.89 % Exception at run slice level % 7.39/1.89 User error: GNN currently only supports monomorphic FOL. % 7.39/1.89 % Exception at run slice level % 7.39/1.89 User error: GNN currently only supports monomorphic FOL. % 7.39/1.89 % (2429273)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=969634758:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi) % 7.39/1.89 % (2429268)Instruction limit reached! % 7.39/1.89 % (2429268)------------------------------ % 7.39/1.89 % (2429268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.39/1.89 % (2429268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.39/1.89 % (2429268)CaDiCaL version: 2.1.3 % 7.39/1.89 % (2429268)Termination reason: Instruction limit % 7.39/1.89 % (2429268)Termination phase: Saturation % 7.39/1.89 % (2429268)Time elapsed: 0.182 s % 7.39/1.89 % (2429268)Peak memory usage: 90 MB % 7.39/1.89 % (2429268)Instructions burned: 326 (million) % 7.39/1.89 % (2429273)Refutation not found, incomplete strategy % 7.39/1.89 % (2429273)------------------------------ % 7.39/1.89 % (2429273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.39/1.89 % (2429273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.39/1.89 % (2429273)CaDiCaL version: 2.1.3 % 7.39/1.89 % (2429273)Termination reason: Refutation not found, incomplete strategy % 7.39/1.89 % (2429273)Time elapsed: 0.033 s % 7.39/1.89 % (2429273)Peak memory usage: 89 MB % 7.39/1.89 % (2429273)Instructions burned: 64 (million) % 7.39/1.89 % (2429276)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1667363881:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi) % 7.39/1.89 % (2429276)Instruction limit reached! % 7.39/1.89 % (2429276)------------------------------ % 7.39/1.89 % (2429276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.39/1.89 % (2429276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.39/1.89 % (2429276)CaDiCaL version: 2.1.3 % 7.39/1.89 % (2429276)Termination reason: Instruction limit % 7.39/1.89 % (2429276)Termination phase: Saturation % 7.39/1.89 % (2429276)Time elapsed: 0.036 s % 7.39/1.89 % (2429276)Peak memory usage: 90 MB % 7.39/1.89 % (2429276)Instructions burned: 113 (million) % 7.39/1.89 % (2429279)lrs+10_1_sil=8000:sp=occurrence:random_seed=894019137:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 10.88/2.16 % (2429278)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3918862957:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 10.88/2.16 % (2429275)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3685923676:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 10.88/2.16 % (2429277)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3848444985:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 10.88/2.16 % (2429278)Refutation not found, incomplete strategy % 10.88/2.16 % (2429278)------------------------------ % 10.88/2.16 % (2429278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.88/2.16 % (2429278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.88/2.16 % (2429278)CaDiCaL version: 2.1.3 % 10.88/2.16 % (2429278)Termination reason: Refutation not found, incomplete strategy % 10.88/2.16 % (2429278)Time elapsed: 0.005 s % 10.88/2.16 % (2429278)Peak memory usage: 88 MB % 10.88/2.16 % (2429278)Instructions burned: 7 (million) % 10.88/2.16 % (2429277)Refutation not found, incomplete strategy % 10.88/2.16 % (2429277)------------------------------ % 10.88/2.16 % (2429277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.88/2.16 % (2429277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.88/2.16 % (2429277)CaDiCaL version: 2.1.3 % 10.88/2.16 % (2429277)Termination reason: Refutation not found, incomplete strategy % 10.88/2.16 % (2429277)Time elapsed: 0.005 s % 10.88/2.16 % (2429277)Peak memory usage: 88 MB % 10.88/2.16 % (2429277)Instructions burned: 10 (million) % 10.88/2.16 % (2429281)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=316634050:i=437:sd=1:aac=none:ss=included_2994 on theBenchmark for (2994ds/437Mi) % 10.88/2.16 % (2429281)Refutation not found, incomplete strategy % 10.88/2.16 % (2429281)------------------------------ % 10.88/2.16 % (2429281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.88/2.16 % (2429281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.88/2.16 % (2429281)CaDiCaL version: 2.1.3 % 10.88/2.16 % (2429281)Termination reason: Refutation not found, incomplete strategy % 10.88/2.16 % (2429281)Time elapsed: 0.006 s % 10.88/2.16 % (2429281)Peak memory usage: 88 MB % 10.88/2.16 % (2429281)Instructions burned: 10 (million) % 10.88/2.16 % (2429283)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1500992784:i=5202:ss=axioms:sgt=16_2993 on theBenchmark for (2993ds/5202Mi) % 10.88/2.16 % (2429273)------------------------------ % 10.88/2.16 % (2429273)------------------------------ % 10.88/2.16 % (2429278)------------------------------ % 10.88/2.16 % (2429278)------------------------------ % 10.88/2.16 % (2429277)------------------------------ % 10.88/2.16 % (2429277)------------------------------ % 10.88/2.16 % Exception at run slice level % 10.88/2.16 User error: GNN currently only supports monomorphic FOL. % 10.88/2.16 % (2429281)------------------------------ % 10.88/2.16 % (2429281)------------------------------ % 10.88/2.16 % (2429290)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1996189477:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2991 on theBenchmark for (2991ds/134Mi) % 10.88/2.16 % (2429293)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=169487898:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/125Mi) % 10.88/2.16 % (2429293)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.88/2.16 % Exception at run slice level % 10.88/2.16 User error: GNN currently only supports monomorphic FOL. % 10.88/2.16 % (2429292)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3420050755:st=3:i=13193:sd=3:ss=axioms_2991 on theBenchmark for (2991ds/13193Mi) % 10.88/2.16 % (2429291)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1104884129:st=8:i=592:sd=3:ep=RST:ss=axioms_2991 on theBenchmark for (2991ds/592Mi) % 10.88/2.16 % (2429293)Instruction limit reached! % 10.88/2.16 % (2429293)------------------------------ % 10.88/2.16 % (2429293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.88/2.16 % (2429293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.88/2.16 % (2429293)CaDiCaL version: 2.1.3 % 10.88/2.16 % (2429293)Termination reason: Instruction limit % 12.61/2.73 % (2429293)Termination phase: Saturation % 12.61/2.73 % (2429293)Time elapsed: 0.039 s % 12.61/2.73 % (2429293)Peak memory usage: 90 MB % 12.61/2.73 % (2429293)Instructions burned: 126 (million) % 12.61/2.73 % (2429290)Instruction limit reached! % 12.61/2.73 % (2429290)------------------------------ % 12.61/2.73 % (2429290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.61/2.73 % (2429290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.61/2.73 % (2429290)CaDiCaL version: 2.1.3 % 12.61/2.73 % (2429290)Termination reason: Instruction limit % 12.61/2.73 % (2429290)Termination phase: Saturation % 12.61/2.73 % (2429290)Time elapsed: 0.071 s % 12.61/2.73 % (2429290)Peak memory usage: 89 MB % 12.61/2.73 % (2429290)Instructions burned: 135 (million) % 12.61/2.73 % (2429294)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3514807079:i=134:gtgl=5:slsql=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/134Mi) % 12.61/2.73 % (2429279)Instruction limit reached! % 12.61/2.73 % (2429279)------------------------------ % 12.61/2.73 % (2429279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.61/2.73 % (2429279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.61/2.73 % (2429279)CaDiCaL version: 2.1.3 % 12.61/2.73 % (2429279)Termination reason: Instruction limit % 12.61/2.73 % (2429279)Termination phase: Saturation % 12.61/2.73 % (2429279)Time elapsed: 0.462 s % 12.61/2.73 % (2429279)Peak memory usage: 93 MB % 12.61/2.73 % (2429279)Instructions burned: 907 (million) % 12.61/2.73 % (2429300)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=28680404:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/431Mi) % 12.61/2.73 % (2429297)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2527907926:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/141Mi) % 12.61/2.73 % (2429297)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 12.61/2.73 % (2429297)Refutation not found, incomplete strategy % 12.61/2.73 % (2429297)------------------------------ % 12.61/2.73 % (2429297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.61/2.73 % (2429297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.61/2.73 % (2429297)CaDiCaL version: 2.1.3 % 12.61/2.73 % (2429297)Termination reason: Refutation not found, incomplete strategy % 12.61/2.73 % (2429297)Time elapsed: 0.002 s % 12.61/2.73 % (2429297)Peak memory usage: 88 MB % 12.61/2.73 % (2429297)Instructions burned: 2 (million) % 12.61/2.73 % (2429294)Instruction limit reached! % 12.61/2.73 % (2429294)------------------------------ % 12.61/2.73 % (2429294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.61/2.73 % (2429294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.61/2.73 % (2429294)CaDiCaL version: 2.1.3 % 12.61/2.73 % (2429294)Termination reason: Instruction limit % 12.61/2.73 % (2429294)Termination phase: Saturation % 12.61/2.73 % (2429294)Time elapsed: 0.080 s % 12.61/2.73 % (2429294)Peak memory usage: 90 MB % 12.61/2.73 % (2429294)Instructions burned: 134 (million) % 12.61/2.73 % (2429301)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=3051707249:i=6060:aac=none:ins=25_2989 on theBenchmark for (2989ds/6060Mi) % 12.61/2.73 % (2429300)Instruction limit reached! % 12.61/2.73 % (2429300)------------------------------ % 12.61/2.73 % (2429300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.61/2.73 % (2429300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.61/2.73 % (2429300)CaDiCaL version: 2.1.3 % 12.61/2.73 % (2429300)Termination reason: Instruction limit % 12.61/2.73 % (2429300)Termination phase: Saturation % 12.61/2.73 % (2429300)Time elapsed: 0.110 s % 12.61/2.73 % (2429300)Peak memory usage: 90 MB % 12.61/2.73 % (2429300)Instructions burned: 433 (million) % 12.61/2.73 % (2429303)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=3014653189:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2989 on theBenchmark for (2989ds/150Mi) % 12.61/2.73 % (2429303)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 12.61/2.73 % (2429307)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3973023653:i=14155:bd=all_2988 on theBenchmark for (2988ds/14155Mi) % 19.37/3.45 % (2429308)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2688717700:i=667:av=off:fsr=off_2987 on theBenchmark for (2987ds/667Mi) % 19.37/3.45 % (2429308)Refutation not found, incomplete strategy % 19.37/3.45 % (2429308)------------------------------ % 19.37/3.45 % (2429308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.37/3.45 % (2429308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.37/3.45 % (2429308)CaDiCaL version: 2.1.3 % 19.37/3.45 % (2429308)Termination reason: Refutation not found, incomplete strategy % 19.37/3.45 % (2429308)Time elapsed: 0.003 s % 19.37/3.45 % (2429308)Peak memory usage: 88 MB % 19.37/3.45 % (2429308)Instructions burned: 10 (million) % 19.37/3.45 % (2429303)Instruction limit reached! % 19.37/3.45 % (2429303)------------------------------ % 19.37/3.45 % (2429303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.37/3.45 % (2429303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.37/3.45 % (2429303)CaDiCaL version: 2.1.3 % 19.37/3.45 % (2429303)Termination reason: Instruction limit % 19.37/3.45 % (2429303)Termination phase: Saturation % 19.37/3.45 % (2429303)Time elapsed: 0.094 s % 19.37/3.45 % (2429303)Peak memory usage: 90 MB % 19.37/3.45 % (2429303)Instructions burned: 151 (million) % 19.37/3.45 % (2429291)Instruction limit reached! % 19.37/3.45 % (2429291)------------------------------ % 19.37/3.45 % (2429291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.37/3.45 % (2429291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.37/3.45 % (2429291)CaDiCaL version: 2.1.3 % 19.37/3.45 % (2429291)Termination reason: Instruction limit % 19.37/3.45 % (2429291)Termination phase: Saturation % 19.37/3.45 % (2429291)Time elapsed: 0.342 s % 19.37/3.45 % (2429291)Peak memory usage: 93 MB % 19.37/3.45 % (2429291)Instructions burned: 592 (million) % 19.37/3.45 % (2429297)------------------------------ % 19.37/3.45 % (2429297)------------------------------ % 19.37/3.45 % Exception at run slice level % 19.37/3.45 User error: GNN currently only supports monomorphic FOL. % 19.37/3.45 % (2429312)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=11232703:s2a=on:i=185:s2at=1.8:fdi=4_2986 on theBenchmark for (2986ds/185Mi) % 19.37/3.45 % (2429308)------------------------------ % 19.37/3.45 % (2429308)------------------------------ % 19.37/3.45 % (2429314)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1012179642:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2986 on theBenchmark for (2986ds/4850Mi) % 19.37/3.45 % (2429313)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2002752113:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2986 on theBenchmark for (2986ds/193Mi) % 19.37/3.45 % (2429314)Refutation not found, incomplete strategy % 19.37/3.45 % (2429314)------------------------------ % 19.37/3.45 % (2429314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.37/3.45 % (2429314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.37/3.45 % (2429314)CaDiCaL version: 2.1.3 % 19.37/3.45 % (2429314)Termination reason: Refutation not found, incomplete strategy % 19.37/3.45 % (2429314)Time elapsed: 0.005 s % 19.37/3.45 % (2429314)Peak memory usage: 88 MB % 19.37/3.45 % (2429314)Instructions burned: 8 (million) % 19.37/3.45 % (2429315)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2049098895:i=12111:sd=1:ss=included_2986 on theBenchmark for (2986ds/12111Mi) % 19.37/3.45 % Exception at run slice level % 19.37/3.45 User error: GNN currently only supports monomorphic FOL. % 19.37/3.45 % (2429317)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1369771551:i=319:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/319Mi) % 19.37/3.45 % (2429312)Instruction limit reached! % 19.37/3.45 % (2429312)------------------------------ % 19.37/3.45 % (2429312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.37/3.45 % (2429312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.37/3.45 % (2429312)CaDiCaL version: 2.1.3 % 19.37/3.45 % (2429312)Termination reason: Instruction limit % 19.37/3.45 % (2429312)Termination phase: Saturation % 19.37/3.45 % (2429312)Time elapsed: 0.103 s % 19.37/3.45 % (2429312)Peak memory usage: 90 MB % 19.37/3.45 % (2429312)Instructions burned: 186 (million) % 26.22/4.49 % (2429313)Instruction limit reached! % 26.22/4.49 % (2429313)------------------------------ % 26.22/4.49 % (2429313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.22/4.49 % (2429313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.22/4.49 % (2429313)CaDiCaL version: 2.1.3 % 26.22/4.49 % (2429313)Termination reason: Instruction limit % 26.22/4.49 % (2429313)Termination phase: Saturation % 26.22/4.49 % (2429313)Time elapsed: 0.116 s % 26.22/4.49 % (2429313)Peak memory usage: 91 MB % 26.22/4.49 % (2429313)Instructions burned: 194 (million) % 26.22/4.49 % (2429317)Instruction limit reached! % 26.22/4.49 % (2429317)------------------------------ % 26.22/4.49 % (2429317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.22/4.49 % (2429317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.22/4.49 % (2429317)CaDiCaL version: 2.1.3 % 26.22/4.49 % (2429317)Termination reason: Instruction limit % 26.22/4.49 % (2429317)Termination phase: Saturation % 26.22/4.49 % (2429317)Time elapsed: 0.089 s % 26.22/4.49 % (2429317)Peak memory usage: 91 MB % 26.22/4.49 % (2429317)Instructions burned: 320 (million) % 26.22/4.49 % (2429321)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=403668583:i=2064:ep=RST_2984 on theBenchmark for (2984ds/2064Mi) % 26.22/4.49 % Exception at run slice level % 26.22/4.49 User error: GNN currently only supports monomorphic FOL. % 26.22/4.49 % (2429323)dis-1011_128_sil=32000:random_seed=1927402958:i=3706:ep=RST:av=off_2984 on theBenchmark for (2984ds/3706Mi) % 26.22/4.49 % (2429325)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2843514292:i=13913:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/13913Mi) % 26.22/4.49 % (2429324)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1521783123:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2983 on theBenchmark for (2983ds/757Mi) % 26.22/4.49 % (2429314)------------------------------ % 26.22/4.49 % (2429314)------------------------------ % 26.22/4.49 % (2429324)Refutation not found, incomplete strategy % 26.22/4.49 % (2429324)------------------------------ % 26.22/4.49 % (2429324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.22/4.49 % (2429324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.22/4.49 % (2429324)CaDiCaL version: 2.1.3 % 26.22/4.49 % (2429324)Termination reason: Refutation not found, incomplete strategy % 26.22/4.49 % (2429324)Time elapsed: 0.007 s % 26.22/4.49 % (2429324)Peak memory usage: 89 MB % 26.22/4.49 % (2429324)Instructions burned: 11 (million) % 26.22/4.49 % (2429327)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=180373290:i=9925:aac=none_2983 on theBenchmark for (2983ds/9925Mi) % 26.22/4.49 % Exception at run slice level % 26.22/4.49 User error: GNN currently only supports monomorphic FOL. % 26.22/4.49 % (2429331)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3863921680:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2982 on theBenchmark for (2982ds/2479Mi) % 26.22/4.49 % (2429331)Refutation not found, incomplete strategy % 26.22/4.49 % (2429331)------------------------------ % 26.22/4.49 % (2429331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.22/4.49 % (2429331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.22/4.49 % (2429331)CaDiCaL version: 2.1.3 % 26.22/4.49 % (2429331)Termination reason: Refutation not found, incomplete strategy % 26.22/4.49 % (2429331)Time elapsed: 0.006 s % 26.22/4.49 % (2429331)Peak memory usage: 88 MB % 26.22/4.49 % (2429331)Instructions burned: 8 (million) % 26.22/4.49 % Exception at run slice level % 26.22/4.49 User error: GNN currently only supports monomorphic FOL. % 26.22/4.49 % (2429324)------------------------------ % 26.22/4.49 % (2429324)------------------------------ % 26.22/4.49 % (2429333)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1120577867:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/440Mi) % 26.22/4.49 % (2429335)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2796569144:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2980 on theBenchmark for (2980ds/11145Mi) % 26.22/4.49 % (2429333)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 26.22/4.49 % (2429336)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=1933295389:cts=off:i=3034:av=off:er=known:fsd=on_2980 on theBenchmark for (2980ds/3034Mi) % 34.91/5.68 % (2429331)------------------------------ % 34.91/5.68 % (2429331)------------------------------ % 34.91/5.68 % Exception at run slice level % 34.91/5.68 User error: GNN currently only supports monomorphic FOL. % 34.91/5.68 % Exception at run slice level % 34.91/5.68 User error: GNN currently only supports monomorphic FOL. % 34.91/5.68 % (2429333)Instruction limit reached! % 34.91/5.68 % (2429333)------------------------------ % 34.91/5.68 % (2429333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.91/5.68 % (2429333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.91/5.68 % (2429333)CaDiCaL version: 2.1.3 % 34.91/5.68 % (2429333)Termination reason: Instruction limit % 34.91/5.68 % (2429333)Termination phase: Saturation % 34.91/5.68 % (2429333)Time elapsed: 0.237 s % 34.91/5.68 % (2429333)Peak memory usage: 91 MB % 34.91/5.68 % (2429333)Instructions burned: 441 (million) % 34.91/5.68 % (2429340)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3260817418:st=2:s2a=on:i=524:s2at=2:ss=axioms_2978 on theBenchmark for (2978ds/524Mi) % 34.91/5.68 % (2429341)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=487736667:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2978 on theBenchmark for (2978ds/1016Mi) % 34.91/5.68 % (2429342)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2353387532:i=14123:bd=preordered:ins=4_2978 on theBenchmark for (2978ds/14123Mi) % 34.91/5.68 % (2429343)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1807273835:i=5781:kws=precedence:bd=all:rawr=on_2977 on theBenchmark for (2977ds/5781Mi) % 34.91/5.68 % Exception at run slice level % 34.91/5.68 User error: GNN currently only supports monomorphic FOL. % 34.91/5.68 % Exception at run slice level % 34.91/5.68 User error: GNN currently only supports monomorphic FOL. % 34.91/5.68 % (2429340)Instruction limit reached! % 34.91/5.68 % (2429340)------------------------------ % 34.91/5.68 % (2429340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.91/5.68 % (2429340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.91/5.68 % (2429340)CaDiCaL version: 2.1.3 % 34.91/5.68 % (2429340)Termination reason: Instruction limit % 34.91/5.68 % (2429340)Termination phase: Saturation % 34.91/5.68 % (2429340)Time elapsed: 0.277 s % 34.91/5.68 % (2429340)Peak memory usage: 92 MB % 34.91/5.68 % (2429340)Instructions burned: 525 (million) % 34.91/5.68 % (2429348)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=876949646:i=2448:gtgl=5:bd=preordered:gtg=all_2975 on theBenchmark for (2975ds/2448Mi) % 34.91/5.68 % (2429349)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3782396201:i=3223:kws=precedence:fgj=on:av=off_2975 on theBenchmark for (2975ds/3223Mi) % 34.91/5.68 % (2429350)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3980190446:st=5.6:i=2033:sd=3:ss=axioms_2974 on theBenchmark for (2974ds/2033Mi) % 34.91/5.68 % Exception at run slice level % 34.91/5.68 User error: GNN currently only supports monomorphic FOL. % 34.91/5.68 % (2429341)Instruction limit reached! % 34.91/5.68 % (2429341)------------------------------ % 34.91/5.68 % (2429341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.91/5.68 % (2429341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.91/5.68 % (2429341)CaDiCaL version: 2.1.3 % 34.91/5.68 % (2429341)Termination reason: Instruction limit % 34.91/5.68 % (2429341)Termination phase: Saturation % 34.91/5.68 % (2429341)Time elapsed: 0.517 s % 34.91/5.68 % (2429341)Peak memory usage: 95 MB % 34.91/5.68 % (2429341)Instructions burned: 1016 (million) % 34.91/5.68 % (2429321)Instruction limit reached! % 34.91/5.68 % (2429321)------------------------------ % 34.91/5.68 % (2429321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.91/5.68 % (2429321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.91/5.68 % (2429321)CaDiCaL version: 2.1.3 % 34.91/5.68 % (2429321)Termination reason: Instruction limit % 34.91/5.68 % (2429321)Termination phase: Saturation % 34.91/5.68 % (2429321)Time elapsed: 1.157 s % 34.91/5.68 % (2429321)Peak memory usage: 102 MB % 34.91/5.68 % (2429321)Instructions burned: 2065 (million) % 34.91/5.68 % (2429354)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3203467868:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2972 on theBenchmark for (2972ds/2055Mi) % 41.98/6.62 % (2429355)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=1202256420:i=21611:sd=3:ss=axioms_2972 on theBenchmark for (2972ds/21611Mi) % 41.98/6.62 % (2429356)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=4255291028:i=4835:sd=13:ss=axioms:sgt=23_2972 on theBenchmark for (2972ds/4835Mi) % 41.98/6.62 % Exception at run slice level % 41.98/6.62 User error: GNN currently only supports monomorphic FOL. % 41.98/6.62 % Exception at run slice level % 41.98/6.62 User error: GNN currently only supports monomorphic FOL. % 41.98/6.62 % Exception at run slice level % 41.98/6.62 User error: GNN currently only supports monomorphic FOL. % 41.98/6.62 % (2429361)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3890418007:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2969 on theBenchmark for (2969ds/2326Mi) % 41.98/6.62 % (2429360)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=1011155049:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2970 on theBenchmark for (2970ds/797Mi) % 41.98/6.62 % (2429362)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3937941678:i=6038:nm=6_2969 on theBenchmark for (2969ds/6038Mi) % 41.98/6.62 % Exception at run slice level % 41.98/6.62 User error: GNN currently only supports monomorphic FOL. % 41.98/6.62 % (2429366)lrs+10_1_sil=32000:sp=occurrence:random_seed=1149857440:st=2:i=33334:sd=3:ss=included:sgt=32_2967 on theBenchmark for (2967ds/33334Mi) % 41.98/6.62 % (2429360)Instruction limit reached! % 41.98/6.62 % (2429360)------------------------------ % 41.98/6.62 % (2429360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.98/6.62 % (2429360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.98/6.62 % (2429360)CaDiCaL version: 2.1.3 % 41.98/6.62 % (2429360)Termination reason: Instruction limit % 41.98/6.62 % (2429360)Termination phase: Saturation % 41.98/6.62 % (2429360)Time elapsed: 0.334 s % 41.98/6.62 % (2429360)Peak memory usage: 94 MB % 41.98/6.62 % (2429360)Instructions burned: 800 (million) % 41.98/6.62 % Exception at run slice level % 41.98/6.62 User error: GNN currently only supports monomorphic FOL. % 41.98/6.62 % (2429368)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1878788978:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2965 on theBenchmark for (2965ds/1008Mi) % 41.98/6.62 % (2429361)Instruction limit reached! % 41.98/6.62 % (2429361)------------------------------ % 41.98/6.62 % (2429361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.98/6.62 % (2429361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.98/6.62 % (2429361)CaDiCaL version: 2.1.3 % 41.98/6.62 % (2429361)Termination reason: Instruction limit % 41.98/6.62 % (2429361)Termination phase: Saturation % 41.98/6.62 % (2429361)Time elapsed: 0.487 s % 41.98/6.62 % (2429361)Peak memory usage: 97 MB % 41.98/6.62 % (2429361)Instructions burned: 2331 (million) % 41.98/6.62 % (2429369)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=798730677:i=8327:s2at=5:bd=preordered_2964 on theBenchmark for (2964ds/8327Mi) % 41.98/6.62 % (2429371)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=2351790333:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2963 on theBenchmark for (2963ds/1083Mi) % 41.98/6.62 % (2429323)Instruction limit reached! % 41.98/6.62 % (2429323)------------------------------ % 41.98/6.62 % (2429323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.98/6.62 % (2429323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.98/6.62 % (2429323)CaDiCaL version: 2.1.3 % 41.98/6.62 % (2429323)Termination reason: Instruction limit % 41.98/6.62 % (2429323)Termination phase: Saturation % 41.98/6.62 % (2429323)Time elapsed: 2.065 s % 41.98/6.62 % (2429323)Peak memory usage: 108 MB % 41.98/6.62 % (2429323)Instructions burned: 3706 (million) % 41.98/6.62 % (2429374)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=3135552759:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2962 on theBenchmark for (2962ds/1084Mi) % 49.37/7.68 % (2429371)Instruction limit reached! % 49.37/7.68 % (2429371)------------------------------ % 49.37/7.68 % (2429371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.37/7.68 % (2429371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.37/7.68 % (2429371)CaDiCaL version: 2.1.3 % 49.37/7.68 % (2429371)Termination reason: Instruction limit % 49.37/7.68 % (2429371)Termination phase: Saturation % 49.37/7.68 % (2429371)Time elapsed: 0.225 s % 49.37/7.68 % (2429371)Peak memory usage: 92 MB % 49.37/7.68 % (2429371)Instructions burned: 1083 (million) % 49.37/7.68 % (2429376)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1941713347:i=6995:s2at=5:gtg=all_2960 on theBenchmark for (2960ds/6995Mi) % 49.37/7.68 % Exception at run slice level % 49.37/7.68 User error: GNN currently only supports monomorphic FOL. % 49.37/7.68 % (2429368)Instruction limit reached! % 49.37/7.68 % (2429368)------------------------------ % 49.37/7.68 % (2429368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.37/7.68 % (2429368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.37/7.68 % (2429368)CaDiCaL version: 2.1.3 % 49.37/7.68 % (2429368)Termination reason: Instruction limit % 49.37/7.68 % (2429368)Termination phase: Saturation % 49.37/7.68 % (2429368)Time elapsed: 0.552 s % 49.37/7.68 % (2429368)Peak memory usage: 99 MB % 49.37/7.68 % (2429368)Instructions burned: 1009 (million) % 49.37/7.68 % (2429378)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1639187799:st=2:i=6225:sd=15:ss=axioms_2959 on theBenchmark for (2959ds/6225Mi) % 49.37/7.68 % Exception at run slice level % 49.37/7.68 User error: GNN currently only supports monomorphic FOL. % 49.37/7.68 % (2429379)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=1374281530:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2958 on theBenchmark for (2958ds/3372Mi) % 49.37/7.68 % (2429381)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=4291115912:st=2.3:i=26457:sd=10:ss=included:sgt=8_2958 on theBenchmark for (2958ds/26457Mi) % 49.37/7.68 % (2429374)Instruction limit reached! % 49.37/7.68 % (2429374)------------------------------ % 49.37/7.68 % (2429374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.37/7.68 % (2429374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.37/7.68 % (2429374)CaDiCaL version: 2.1.3 % 49.37/7.68 % (2429374)Termination reason: Instruction limit % 49.37/7.68 % (2429374)Termination phase: Saturation % 49.37/7.68 % (2429374)Time elapsed: 0.572 s % 49.37/7.68 % (2429374)Peak memory usage: 96 MB % 49.37/7.68 % (2429374)Instructions burned: 1084 (million) % 49.37/7.68 % Exception at run slice level % 49.37/7.68 User error: GNN currently only supports monomorphic FOL. % 49.37/7.68 % (2429385)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=1432523831:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2955 on theBenchmark for (2955ds/2503Mi) % 49.37/7.68 % (2429385)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 49.37/7.68 % (2429384)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=1467248525:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2955 on theBenchmark for (2955ds/13494Mi) % 49.37/7.68 % Exception at run slice level % 49.37/7.68 User error: GNN currently only supports monomorphic FOL. % 49.37/7.68 % (2429388)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=3082054358:i=2559:sd=1:ep=RSTC:ss=axioms_2953 on theBenchmark for (2953ds/2559Mi) % 49.37/7.68 % Exception at run slice level % 49.37/7.68 User error: GNN currently only supports monomorphic FOL. % 49.37/7.68 % (2429390)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2683062987:i=30753:av=off:ss=included_2952 on theBenchmark for (2952ds/30753Mi) % 49.37/7.68 % Exception at run slice level % 49.37/7.68 User error: GNN currently only supports monomorphic FOL. % 49.37/7.68 % Exception at run slice level % 49.37/7.68 User error: GNN currently only supports monomorphic FOL. % 49.37/7.68 % (2429392)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2873922010:i=26473:ep=RSTC_2950 on theBenchmark for (2950ds/26473Mi) % 58.28/9.01 % Exception at run slice level % 58.28/9.01 User error: GNN currently only supports monomorphic FOL. % 58.28/9.01 % (2429393)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=3919690675:cts=off:i=2759:kws=inv_arity:fgj=on_2949 on theBenchmark for (2949ds/2759Mi) % 58.28/9.01 % (2429395)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=2557035218:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2949 on theBenchmark for (2949ds/5665Mi) % 58.28/9.01 % (2429395)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 58.28/9.01 % Exception at run slice level % 58.28/9.01 User error: GNN currently only supports monomorphic FOL. % 58.28/9.01 % (2429356)Instruction limit reached! % 58.28/9.01 % (2429356)------------------------------ % 58.28/9.01 % (2429356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.28/9.01 % (2429356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.28/9.01 % (2429356)CaDiCaL version: 2.1.3 % 58.28/9.01 % (2429356)Termination reason: Instruction limit % 58.28/9.01 % (2429356)Termination phase: Saturation % 58.28/9.01 % (2429356)Time elapsed: 2.460 s % 58.28/9.01 % (2429356)Peak memory usage: 108 MB % 58.28/9.01 % (2429356)Instructions burned: 4837 (million) % 58.28/9.01 % (2429398)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=671796635:i=1532:ep=RS:ss=axioms_2946 on theBenchmark for (2946ds/1532Mi) % 58.28/9.01 % (2429343)Instruction limit reached! % 58.28/9.01 % (2429343)------------------------------ % 58.28/9.01 % (2429343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.28/9.01 % (2429343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.28/9.01 % (2429343)CaDiCaL version: 2.1.3 % 58.28/9.01 % (2429343)Termination reason: Instruction limit % 58.28/9.01 % (2429343)Termination phase: Saturation % 58.28/9.01 % (2429343)Time elapsed: 3.107 s % 58.28/9.01 % (2429343)Peak memory usage: 118 MB % 58.28/9.01 % (2429343)Instructions burned: 5781 (million) % 58.28/9.01 % (2429399)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=632906544:i=1565:sd=2:ss=axioms:sgt=32_2946 on theBenchmark for (2946ds/1565Mi) % 58.28/9.01 % Exception at run slice level % 58.28/9.01 User error: GNN currently only supports monomorphic FOL. % 58.28/9.01 % Exception at run slice level % 58.28/9.01 User error: GNN currently only supports monomorphic FOL. % 58.28/9.01 % (2429401)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=741236261:i=1572:fgj=on:gsp=on_2945 on theBenchmark for (2945ds/1572Mi) % 58.28/9.01 % (2429401)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 58.28/9.01 % (2429404)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=1548575835:i=3500:sd=1:bd=preordered:sup=off:ss=included_2944 on theBenchmark for (2944ds/3500Mi) % 58.28/9.01 % (2429403)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=2660403672:i=6052:sd=4:ss=axioms:sgt=24_2944 on theBenchmark for (2944ds/6052Mi) % 58.28/9.01 % Exception at run slice level % 58.28/9.01 User error: GNN currently only supports monomorphic FOL. % 58.28/9.01 % Exception at run slice level % 58.28/9.01 User error: GNN currently only supports monomorphic FOL. % 58.28/9.01 % (2429408)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=1030156625:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2941 on theBenchmark for (2941ds/1842Mi) % 58.28/9.01 % (2429408)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 58.28/9.01 % Exception at run slice level % 58.28/9.01 User error: GNN currently only supports monomorphic FOL. % 58.28/9.01 % (2429409)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1901199901:i=66096:add=on_2941 on theBenchmark for (2941ds/66096Mi) % 69.75/10.54 % Exception at run slice level % 69.75/10.54 User error: GNN currently only supports monomorphic FOL. % 69.75/10.54 % (2429411)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=2619125769:i=1884:sd=1:nm=60:ss=axioms_2940 on theBenchmark for (2940ds/1884Mi) % 69.75/10.54 % Exception at run slice level % 69.75/10.54 User error: GNN currently only supports monomorphic FOL. % 69.75/10.54 % (2429413)lrs-1011_4:1_sil=16000:bsr=on:random_seed=1310267256:cts=off:i=5469:bs=on:fsr=off_2939 on theBenchmark for (2939ds/5469Mi) % 69.75/10.54 % (2429415)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=1686358499:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2938 on theBenchmark for (2938ds/2037Mi) % 69.75/10.54 % Exception at run slice level % 69.75/10.54 User error: GNN currently only supports monomorphic FOL. % 69.75/10.54 % Exception at run slice level % 69.75/10.54 User error: GNN currently only supports monomorphic FOL. % 69.75/10.54 % Exception at run slice level % 69.75/10.54 User error: GNN currently only supports monomorphic FOL. % 69.75/10.54 % (2429418)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=4106510174:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2936 on theBenchmark for (2936ds/2110Mi) % 69.75/10.54 % (2429419)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=4106089754:i=2430:add=off:aac=none:nm=16_2935 on theBenchmark for (2935ds/2430Mi) % 69.75/10.54 % (2429420)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=3537359291:cond=fast:i=4891_2935 on theBenchmark for (2935ds/4891Mi) % 69.75/10.54 % Exception at run slice level % 69.75/10.54 User error: GNN currently only supports monomorphic FOL. % 69.75/10.54 % (2429424)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=3040495472:st=2:i=14845:sd=2:ss=included:fsd=on_2932 on theBenchmark for (2932ds/14845Mi) % 69.75/10.54 % (2429378)Instruction limit reached! % 69.75/10.54 % (2429378)------------------------------ % 69.75/10.54 % (2429378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.75/10.54 % (2429378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.75/10.54 % (2429378)CaDiCaL version: 2.1.3 % 69.75/10.54 % (2429378)Termination reason: Instruction limit % 69.75/10.54 % (2429378)Termination phase: Saturation % 69.75/10.54 % (2429378)Time elapsed: 2.623 s % 69.75/10.54 % (2429378)Peak memory usage: 107 MB % 69.75/10.54 % (2429378)Instructions burned: 6226 (million) % 69.75/10.54 % Exception at run slice level % 69.75/10.54 User error: GNN currently only supports monomorphic FOL. % 69.75/10.54 % (2429426)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=2078985148:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2932 on theBenchmark for (2932ds/7534Mi) % 69.75/10.54 % Exception at run slice level % 69.75/10.54 User error: GNN currently only supports monomorphic FOL. % 69.75/10.54 % (2429427)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=1583553054:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2931 on theBenchmark for (2931ds/10353Mi) % 69.75/10.54 % Exception at run slice level % 69.75/10.54 User error: GNN currently only supports monomorphic FOL. % 69.75/10.54 % (2429429)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2877132396:i=7860_2930 on theBenchmark for (2930ds/7860Mi) % 69.75/10.54 % (2429429)Refutation not found, incomplete strategy % 69.75/10.54 % (2429429)------------------------------ % 69.75/10.54 % (2429429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.75/10.54 % (2429429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.75/10.54 % (2429429)CaDiCaL version: 2.1.3 % 69.75/10.54 % (2429429)Termination reason: Refutation not found, incomplete strategy % 69.75/10.54 % (2429429)Time elapsed: 0.006 s % 69.75/10.54 % (2429429)Peak memory usage: 88 MB % 69.75/10.54 % (2429429)Instructions burned: 10 (million) % 69.75/10.54 % (2429431)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=2805681164:i=7896:sd=2:bs=on:ss=included:sgt=20_2930 on theBenchmark for (2930ds/7896Mi) % 108.19/15.98 % Exception at run slice level % 108.19/15.98 User error: GNN currently only supports monomorphic FOL. % 108.19/15.98 % Exception at run slice level % 108.19/15.98 User error: GNN currently only supports monomorphic FOL. % 108.19/15.98 % (2429429)------------------------------ % 108.19/15.98 % (2429429)------------------------------ % 108.19/15.98 % Exception at run slice level % 108.19/15.98 User error: GNN currently only supports monomorphic FOL. % 108.19/15.98 % (2429434)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1421214983:i=5812:gtgl=2:gtg=all_2927 on theBenchmark for (2927ds/5812Mi) % 108.19/15.98 % (2429435)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=3457944669:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2927 on theBenchmark for (2927ds/2965Mi) % 108.19/15.98 % (2429436)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=140791457:i=2967:kws=precedence:bd=preordered:av=off_2926 on theBenchmark for (2926ds/2967Mi) % 108.19/15.98 % (2429437)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=2067273000:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2926 on theBenchmark for (2926ds/3022Mi) % 108.19/15.98 % Exception at run slice level % 108.19/15.98 User error: GNN currently only supports monomorphic FOL. % 108.19/15.98 % (2429442)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=4227472562:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2924 on theBenchmark for (2924ds/3207Mi) % 108.19/15.98 % Exception at run slice level % 108.19/15.98 User error: GNN currently only supports monomorphic FOL. % 108.19/15.98 % Exception at run slice level % 108.19/15.98 User error: GNN currently only supports monomorphic FOL. % 108.19/15.98 % Exception at run slice level % 108.19/15.98 User error: GNN currently only supports monomorphic FOL. % 108.19/15.98 % Exception at run slice level % 108.19/15.98 User error: GNN currently only supports monomorphic FOL. % 108.19/15.98 % (2429445)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=3881669233:i=38569:sd=3:ss=axioms:sgt=32_2922 on theBenchmark for (2922ds/38569Mi) % 108.19/15.98 % (2429444)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=3876324762:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2922 on theBenchmark for (2922ds/3289Mi) % 108.19/15.98 % (2429447)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=2778348113:i=33824:bd=preordered_2921 on theBenchmark for (2921ds/33824Mi) % 108.19/15.98 % (2429446)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=695653647:cts=off:i=3394_2921 on theBenchmark for (2921ds/3394Mi) % 108.19/15.98 % Exception at run slice level % 108.19/15.98 User error: GNN currently only supports monomorphic FOL. % 108.19/15.98 % (2429452)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=3916634796:i=20684:bd=all:gtg=exists_sym_2918 on theBenchmark for (2918ds/20684Mi) % 108.19/15.98 % Exception at run slice level % 108.19/15.98 User error: GNN currently only supports monomorphic FOL. % 108.19/15.98 % Exception at run slice level % 108.19/15.98 User error: GNN currently only supports monomorphic FOL. % 108.19/15.98 % Exception at run slice level % 108.19/15.98 User error: GNN currently only supports monomorphic FOL. % 108.19/15.98 % (2429454)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=3374549713: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) % 108.19/15.98 % (2429454)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 108.19/15.98 % (2429455)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=1471450585:st=4:i=7295:sd=4:ep=R:ss=axioms_2917 on theBenchmark for (2917ds/7295Mi) % 136.19/20.00 % Exception at run slice level % 136.19/20.00 User error: GNN currently only supports monomorphic FOL. % 136.19/20.00 % (2429456)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=3518053025:i=4036:ins=10_2916 on theBenchmark for (2916ds/4036Mi) % 136.19/20.00 % (2429459)lrs+10_1_sil=128000:lcm=predicate:random_seed=4183817334:st=3:i=43697:sd=5:ss=axioms_2915 on theBenchmark for (2915ds/43697Mi) % 136.19/20.00 % Exception at run slice level % 136.19/20.00 User error: GNN currently only supports monomorphic FOL. % 136.19/20.00 % Exception at run slice level % 136.19/20.00 User error: GNN currently only supports monomorphic FOL. % 136.19/20.00 % Exception at run slice level % 136.19/20.00 User error: GNN currently only supports monomorphic FOL. % 136.19/20.00 % (2429462)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=4158808809:i=17599:gtg=all:ss=axioms:fsd=on_2912 on theBenchmark for (2912ds/17599Mi) % 136.19/20.00 % (2429463)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=896929806:i=4547:bd=preordered_2912 on theBenchmark for (2912ds/4547Mi) % 136.19/20.00 % (2429464)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=2997713551:i=9294:av=off_2911 on theBenchmark for (2911ds/9294Mi) % 136.19/20.00 % Exception at run slice level % 136.19/20.00 User error: GNN currently only supports monomorphic FOL. % 136.19/20.00 % Exception at run slice level % 136.19/20.00 User error: GNN currently only supports monomorphic FOL. % 136.19/20.00 % (2429413)Instruction limit reached! % 136.19/20.00 % (2429413)------------------------------ % 136.19/20.00 % (2429413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.19/20.00 % (2429413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.19/20.00 % (2429413)CaDiCaL version: 2.1.3 % 136.19/20.00 % (2429413)Termination reason: Instruction limit % 136.19/20.00 % (2429413)Termination phase: Saturation % 136.19/20.00 % (2429413)Time elapsed: 3.115 s % 136.19/20.00 % (2429413)Peak memory usage: 113 MB % 136.19/20.00 % (2429413)Instructions burned: 5469 (million) % 136.19/20.00 % Exception at run slice level % 136.19/20.00 User error: GNN currently only supports monomorphic FOL. % 136.19/20.00 % (2429468)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=285266872:i=32849:add=on_2907 on theBenchmark for (2907ds/32849Mi) % 136.19/20.00 % (2429469)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3953571599:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2907 on theBenchmark for (2907ds/4793Mi) % 136.19/20.00 % (2429470)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=691181201:i=4840:nm=4:av=off_2906 on theBenchmark for (2906ds/4840Mi) % 136.19/20.00 % (2429471)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=566301387:cts=off:i=5002_2906 on theBenchmark for (2906ds/5002Mi) % 136.19/20.00 % Exception at run slice level % 136.19/20.00 User error: GNN currently only supports monomorphic FOL. % 136.19/20.00 % Exception at run slice level % 136.19/20.00 User error: GNN currently only supports monomorphic FOL. % 136.19/20.00 % Exception at run slice level % 136.19/20.00 User error: GNN currently only supports monomorphic FOL. % 136.19/20.00 % Exception at run slice level % 136.19/20.00 User error: GNN currently only supports monomorphic FOL. % 136.19/20.00 % (2429477)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=1543829822:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2902 on theBenchmark for (2902ds/11035Mi) % 136.19/20.00 % (2429476)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=80273364:i=30479:sd=3:ss=axioms_2902 on theBenchmark for (2902ds/30479Mi) % 136.19/20.00 % (2429477)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 136.19/20.00 % (2429478)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=2833712581:i=5835_2902 on theBenchmark for (2902ds/5835Mi) % 160.36/23.25 % (2429479)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=2273448734:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2901 on theBenchmark for (2901ds/5890Mi) % 160.36/23.25 % Exception at run slice level % 160.36/23.25 User error: GNN currently only supports monomorphic FOL. % 160.36/23.25 % Exception at run slice level % 160.36/23.25 User error: GNN currently only supports monomorphic FOL. % 160.36/23.25 % Exception at run slice level % 160.36/23.25 User error: GNN currently only supports monomorphic FOL. % 160.36/23.25 % Exception at run slice level % 160.36/23.25 User error: GNN currently only supports monomorphic FOL. % 160.36/23.25 % (2429485)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=1996823422:i=20312:bd=preordered:fsr=off:er=filter_2898 on theBenchmark for (2898ds/20312Mi) % 160.36/23.25 % (2429484)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=2154360378:cts=off:i=19910:ep=RS_2898 on theBenchmark for (2898ds/19910Mi) % 160.36/23.25 % (2429487)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=850809495:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2897 on theBenchmark for (2897ds/7144Mi) % 160.36/23.25 % (2429486)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=2232488466:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2897 on theBenchmark for (2897ds/13822Mi) % 160.36/23.25 % Exception at run slice level % 160.36/23.25 User error: GNN currently only supports monomorphic FOL. % 160.36/23.25 % Exception at run slice level % 160.36/23.25 User error: GNN currently only supports monomorphic FOL. % 160.36/23.25 % (2429492)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=575057696:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2893 on theBenchmark for (2893ds/15184Mi) % 160.36/23.25 % (2429493)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=910472258:i=107375_2892 on theBenchmark for (2892ds/107375Mi) % 160.36/23.25 % Exception at run slice level % 160.36/23.25 User error: GNN currently only supports monomorphic FOL. % 160.36/23.25 % Exception at run slice level % 160.36/23.25 User error: GNN currently only supports monomorphic FOL. % 160.36/23.25 % (2429496)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=2603118632:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2888 on theBenchmark for (2888ds/7958Mi) % 160.36/23.25 % (2429497)dis+10_128_sil=16000:nwc=0.7:random_seed=3675556696:i=15999:nm=2:gsp=on_2887 on theBenchmark for (2887ds/15999Mi) % 160.36/23.25 % (2429497)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 160.36/23.25 % Exception at run slice level % 160.36/23.25 User error: GNN currently only supports monomorphic FOL. % 160.36/23.25 % (2429500)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=3249924291:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2883 on theBenchmark for (2883ds/8139Mi) % 160.36/23.25 % (2429487)Instruction limit reached! % 160.36/23.25 % (2429487)------------------------------ % 160.36/23.25 % (2429487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.36/23.25 % (2429487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.36/23.25 % (2429487)CaDiCaL version: 2.1.3 % 160.36/23.25 % (2429487)Termination reason: Instruction limit % 160.36/23.25 % (2429487)Termination phase: Saturation % 160.36/23.25 % (2429487)Time elapsed: 3.971 s % 160.36/23.25 % (2429487)Peak memory usage: 129 MB % 160.36/23.25 % (2429487)Instructions burned: 7144 (million) % 160.36/23.25 % (2429502)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=1372993865:st=4:i=8950:sd=5:ss=axioms_2855 on theBenchmark for (2855ds/8950Mi) % 160.36/23.25 % Exception at run slice level % 160.36/23.25 User error: GNN currently only supports monomorphic FOL. % 160.36/23.25 % (2429504)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=3231948735:i=9809:ins=10:av=off_2851 on theBenchmark for (2851ds/9809Mi) % 160.36/23.25 % Exception at run slice level % 172.30/24.96 User error: GNN currently only supports monomorphic FOL. % 172.30/24.96 % (2429506)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=2685682423:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2846 on theBenchmark for (2846ds/9885Mi) % 172.30/24.96 % Exception at run slice level % 172.30/24.96 User error: GNN currently only supports monomorphic FOL. % 172.30/24.96 % (2429508)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=3108678426:cond=fast:i=32078:fgj=on:av=off_2841 on theBenchmark for (2841ds/32078Mi) % 172.30/24.96 % (2429500)Instruction limit reached! % 172.30/24.96 % (2429500)------------------------------ % 172.30/24.96 % (2429500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 172.30/24.96 % (2429500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.30/24.96 % (2429500)CaDiCaL version: 2.1.3 % 172.30/24.96 % (2429500)Termination reason: Instruction limit % 172.30/24.96 % (2429500)Termination phase: Saturation % 172.30/24.96 % (2429500)Time elapsed: 4.466 s % 172.30/24.96 % (2429500)Peak memory usage: 123 MB % 172.30/24.96 % (2429500)Instructions burned: 8139 (million) % 172.30/24.96 % Exception at run slice level % 172.30/24.96 User error: GNN currently only supports monomorphic FOL. % 172.30/24.96 % (2429510)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=2415696161:i=11101:bd=all:ss=axioms:sgt=8_2837 on theBenchmark for (2837ds/11101Mi) % 172.30/24.96 % (2429511)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=2961061523:cond=on:i=13220:s2at=3:aac=none:fsd=on_2836 on theBenchmark for (2836ds/13220Mi) % 172.30/24.96 % Exception at run slice level % 172.30/24.96 User error: GNN currently only supports monomorphic FOL. % 172.30/24.96 % (2429514)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=3291762848:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2831 on theBenchmark for (2831ds/13528Mi) % 172.30/24.96 % Exception at run slice level % 172.30/24.96 User error: GNN currently only supports monomorphic FOL. % 172.30/24.96 % (2429517)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=1092354703:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2826 on theBenchmark for (2826ds/14854Mi) % 172.30/24.96 % Exception at run slice level % 172.30/24.96 User error: GNN currently only supports monomorphic FOL. % 172.30/24.96 % (2429519)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=1046262270:i=14974:ss=axioms:sgt=16_2821 on theBenchmark for (2821ds/14974Mi) % 172.30/24.96 % Exception at run slice level % 172.30/24.96 User error: GNN currently only supports monomorphic FOL. % 172.30/24.96 % (2429521)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=730938684:i=33081:aac=none:fgj=on:bd=all:fsr=off_2816 on theBenchmark for (2816ds/33081Mi) % 172.30/24.96 % Exception at run slice level % 172.30/24.96 User error: GNN currently only supports monomorphic FOL. % 172.30/24.96 % (2429523)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=1741230507:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2812 on theBenchmark for (2812ds/50856Mi) % 172.30/24.96 % (2429392)Instruction limit reached! % 172.30/24.96 % (2429392)------------------------------ % 172.30/24.96 % (2429392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 172.30/24.96 % (2429392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.30/24.96 % (2429392)CaDiCaL version: 2.1.3 % 172.30/24.96 % (2429392)Termination reason: Instruction limit % 172.30/24.96 % (2429392)Termination phase: Saturation % 172.30/24.96 % (2429392)Time elapsed: 13.892 s % 172.30/24.96 % (2429392)Peak memory usage: 286 MB % 172.30/24.96 % (2429392)Instructions burned: 26473 (million) % 172.30/24.96 % (2429525)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=978898778:i=69865_2810 on theBenchmark for (2810ds/69865Mi) % 172.30/24.96 % Exception at run slice level % 172.30/24.96 User error: GNN currently only supports monomorphic FOL. % 172.30/24.96 % (2429497)Instruction limit reached! % 172.30/24.96 % (2429497)------------------------------ % 185.56/26.85 % (2429497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.56/26.85 % (2429497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.56/26.85 % (2429497)CaDiCaL version: 2.1.3 % 185.56/26.85 % (2429497)Termination reason: Instruction limit % 185.56/26.85 % (2429497)Termination phase: Saturation % 185.56/26.85 % (2429497)Time elapsed: 8.0000 s % 185.56/26.85 % (2429497)Peak memory usage: 149 MB % 185.56/26.85 % (2429497)Instructions burned: 15999 (million) % 185.56/26.85 % (2429527)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=47971796:cond=fast:i=17802:gtgl=3:gtg=all_2807 on theBenchmark for (2807ds/17802Mi) % 185.56/26.85 % Exception at run slice level % 185.56/26.85 User error: GNN currently only supports monomorphic FOL. % 185.56/26.85 % (2429528)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=212768168:i=96644_2805 on theBenchmark for (2805ds/96644Mi) % 185.56/26.85 % (2429530)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 185.56/26.85 % (2429530)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=2146635138:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2805 on theBenchmark for (2805ds/21161Mi) % 185.56/26.85 % Exception at run slice level % 185.56/26.85 User error: GNN currently only supports monomorphic FOL. % 185.56/26.85 % (2429533)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=2431079284:i=22761:gtg=all:ss=axioms:fsd=on_2802 on theBenchmark for (2802ds/22761Mi) % 185.56/26.85 % Exception at run slice level % 185.56/26.85 User error: GNN currently only supports monomorphic FOL. % 185.56/26.85 % (2429535)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=425064405:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2797 on theBenchmark for (2797ds/23713Mi) % 185.56/26.85 % (2429484)Instruction limit reached! % 185.56/26.85 % (2429484)------------------------------ % 185.56/26.85 % (2429484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.56/26.85 % (2429484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.56/26.85 % (2429484)CaDiCaL version: 2.1.3 % 185.56/26.85 % (2429484)Termination reason: Instruction limit % 185.56/26.85 % (2429484)Termination phase: Saturation % 185.56/26.85 % (2429484)Time elapsed: 10.354 s % 185.56/26.85 % (2429484)Peak memory usage: 250 MB % 185.56/26.85 % (2429484)Instructions burned: 19911 (million) % 185.56/26.85 % (2429537)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=3592927702:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2792 on theBenchmark for (2792ds/26509Mi) % 185.56/26.85 % Exception at run slice level % 185.56/26.85 User error: GNN currently only supports monomorphic FOL. % 185.56/26.85 % (2429539)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=3063522079:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2788 on theBenchmark for (2788ds/28957Mi) % 185.56/26.85 % (2429459)Instruction limit reached! % 185.56/26.85 % (2429459)------------------------------ % 185.56/26.85 % (2429459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.56/26.85 % (2429459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.56/26.85 % (2429459)CaDiCaL version: 2.1.3 % 185.56/26.85 % (2429459)Termination reason: Instruction limit % 185.56/26.85 % (2429459)Termination phase: Saturation % 185.56/26.85 % (2429459)Time elapsed: 13.759 s % 185.56/26.85 % (2429459)Peak memory usage: 204 MB % 185.56/26.85 % (2429459)Instructions burned: 43700 (million) % 185.56/26.85 % (2429541)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=844404903:i=29246:s2at=-1:kws=inv_arity:ins=10_2777 on theBenchmark for (2777ds/29246Mi) % 185.56/26.85 % Exception at run slice level % 185.56/26.85 User error: GNN currently only supports monomorphic FOL. % 185.56/26.85 % (2429543)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=3444022189:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2774 on theBenchmark for (2774ds/30082Mi) % 192.86/27.81 % (2429543)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 192.86/27.81 % (2429510)Instruction limit reached! % 192.86/27.81 % (2429510)------------------------------ % 192.86/27.81 % (2429510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.86/27.81 % (2429510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.86/27.81 % (2429510)CaDiCaL version: 2.1.3 % 192.86/27.81 % (2429510)Termination reason: Instruction limit % 192.86/27.81 % (2429510)Termination phase: Saturation % 192.86/27.81 % (2429510)Time elapsed: 6.297 s % 192.86/27.81 % (2429510)Peak memory usage: 240 MB % 192.86/27.81 % (2429510)Instructions burned: 11103 (million) % 192.86/27.81 % (2429366)Instruction limit reached! % 192.86/27.81 % (2429366)------------------------------ % 192.86/27.81 % (2429366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.86/27.81 % (2429366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.86/27.81 % (2429366)CaDiCaL version: 2.1.3 % 192.86/27.81 % (2429366)Termination reason: Instruction limit % 192.86/27.81 % (2429366)Termination phase: Saturation % 192.86/27.81 % (2429366)Time elapsed: 19.369 s % 192.86/27.81 % (2429366)Peak memory usage: 170 MB % 192.86/27.81 % (2429366)Instructions burned: 33336 (million) % 192.86/27.81 % Exception at run slice level % 192.86/27.81 User error: GNN currently only supports monomorphic FOL. % 192.86/27.81 % (2429545)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=380619043:i=32262:bd=preordered_2772 on theBenchmark for (2772ds/32262Mi) % 192.86/27.81 % (2429546)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=1066176472:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2772 on theBenchmark for (2772ds/32870Mi) % 192.86/27.81 % (2429547)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=3457633333:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2771 on theBenchmark for (2771ds/33295Mi) % 192.86/27.81 % Exception at run slice level % 192.86/27.81 User error: GNN currently only supports monomorphic FOL. % 192.86/27.81 % (2429551)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=349863684:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2768 on theBenchmark for (2768ds/36826Mi) % 192.86/27.81 % Exception at run slice level % 192.86/27.81 User error: GNN currently only supports monomorphic FOL. % 192.86/27.81 % Exception at run slice level % 192.86/27.81 User error: GNN currently only supports monomorphic FOL. % 192.86/27.81 % (2429553)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=263010195:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2767 on theBenchmark for (2767ds/92981Mi) % 192.86/27.81 % (2429554)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=170306337:s2pl=on:i=49423_2767 on theBenchmark for (2767ds/49423Mi) % 192.86/27.81 % Exception at run slice level % 192.86/27.81 User error: GNN currently only supports monomorphic FOL. % 192.86/27.81 % Exception at run slice level % 192.86/27.81 User error: GNN currently only supports monomorphic FOL. % 192.86/27.81 % (2429557)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=1386383819:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2763 on theBenchmark for (2763ds/57299Mi) % 192.86/27.81 % (2429558)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=3607022382:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2762 on theBenchmark for (2762ds/127679Mi) % 192.86/27.81 % Exception at run slice level % 192.86/27.81 User error: GNN currently only supports monomorphic FOL. % 192.86/27.81 % Exception at run slice level % 192.86/27.81 User error: GNN currently only supports monomorphic FOL. % 192.86/27.81 % (2429561)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=3308392963:i=69402:add=on:aac=none:fsr=off_2758 on theBenchmark for (2758ds/69402Mi) % 192.86/27.81 % (2429562)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=3013899030:i=100512:doe=on:fgj=on:bd=all:fsd=on_2757 on theBenchmark for (2757ds/100512Mi) % 206.37/29.79 % Exception at run slice level % 206.37/29.79 User error: GNN currently only supports monomorphic FOL. % 206.37/29.79 % Exception at run slice level % 206.37/29.79 User error: GNN currently only supports monomorphic FOL. % 206.37/29.79 % (2429565)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=2977549866:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2753 on theBenchmark for (2753ds/138761Mi) % 206.37/29.79 % (2429566)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=566723066:i=282386:rtra=on_2752 on theBenchmark for (2752ds/282386Mi) % 206.37/29.79 % Exception at run slice level % 206.37/29.79 User error: GNN currently only supports monomorphic FOL. % 206.37/29.79 % Exception at run slice level % 206.37/29.79 User error: GNN currently only supports monomorphic FOL. % 206.37/29.79 % (2429569)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=3690008449:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2748 on theBenchmark for (2748ds/269354Mi) % 206.37/29.79 % (2429570)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=2902143939:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2748 on theBenchmark for (2748ds/283390Mi) % 206.37/29.79 % (2429570)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 206.37/29.79 % Exception at run slice level % 206.37/29.79 User error: GNN currently only supports monomorphic FOL. % 206.37/29.79 % Exception at run slice level % 206.37/29.79 User error: GNN currently only supports monomorphic FOL. % 206.37/29.79 % (2429573)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=2257564571:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2743 on theBenchmark for (2743ds/218Mi) % 206.37/29.79 % (2429573)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 206.37/29.79 % (2429573)Refutation not found, incomplete strategy % 206.37/29.79 % (2429573)------------------------------ % 206.37/29.79 % (2429573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.37/29.79 % (2429573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.37/29.79 % (2429573)CaDiCaL version: 2.1.3 % 206.37/29.79 % (2429573)Termination reason: Refutation not found, incomplete strategy % 206.37/29.79 % (2429573)Time elapsed: 0.004 s % 206.37/29.79 % (2429573)Peak memory usage: 89 MB % 206.37/29.79 % (2429573)Instructions burned: 5 (million) % 206.37/29.79 % (2429574)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=2635688151:i=238:av=off:rtra=on:ss=axioms_2743 on theBenchmark for (2743ds/238Mi) % 206.37/29.79 % (2429574)Instruction limit reached! % 206.37/29.79 % (2429574)------------------------------ % 206.37/29.79 % (2429574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.37/29.79 % (2429574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.37/29.79 % (2429574)CaDiCaL version: 2.1.3 % 206.37/29.79 % (2429574)Termination reason: Instruction limit % 206.37/29.79 % (2429574)Termination phase: Saturation % 206.37/29.79 % (2429574)Time elapsed: 0.135 s % 206.37/29.79 % (2429574)Peak memory usage: 89 MB % 206.37/29.79 % (2429574)Instructions burned: 240 (million) % 206.37/29.79 % (2429573)------------------------------ % 206.37/29.79 % (2429573)------------------------------ % 206.37/29.79 % (2429577)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=178645289:s2a=on:i=278:rtra=on:gtg=position_2740 on theBenchmark for (2740ds/278Mi) % 206.37/29.79 % (2429578)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=3436577847:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2739 on theBenchmark for (2739ds/258Mi) % 206.37/29.79 % (2429577)Instruction limit reached! % 206.37/29.79 % (2429577)------------------------------ % 206.37/29.79 % (2429577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.37/29.79 % (2429577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.37/29.79 % (2429577)CaDiCaL version: 2.1.3 % 206.37/29.79 % (2429577)Termination reason: Instruction limit % 213.36/30.73 % (2429577)Termination phase: Saturation % 213.36/30.73 % (2429577)Time elapsed: 0.149 s % 213.36/30.73 % (2429577)Peak memory usage: 90 MB % 213.36/30.73 % (2429577)Instructions burned: 278 (million) % 213.36/30.73 % (2429578)Instruction limit reached! % 213.36/30.73 % (2429578)------------------------------ % 213.36/30.73 % (2429578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.36/30.73 % (2429578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.36/30.73 % (2429578)CaDiCaL version: 2.1.3 % 213.36/30.73 % (2429578)Termination reason: Instruction limit % 213.36/30.73 % (2429578)Termination phase: Saturation % 213.36/30.73 % (2429578)Time elapsed: 0.112 s % 213.36/30.73 % (2429578)Peak memory usage: 90 MB % 213.36/30.73 % (2429578)Instructions burned: 260 (million) % 213.36/30.73 % (2429586)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=3422238463:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2737 on theBenchmark for (2737ds/570Mi) % 213.36/30.73 % (2429604)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=3765845251:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2737 on theBenchmark for (2737ds/314Mi) % 213.36/30.73 % (2429604)Instruction limit reached! % 213.36/30.73 % (2429604)------------------------------ % 213.36/30.73 % (2429604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.36/30.73 % (2429604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.36/30.73 % (2429604)CaDiCaL version: 2.1.3 % 213.36/30.73 % (2429604)Termination reason: Instruction limit % 213.36/30.73 % (2429604)Termination phase: Saturation % 213.36/30.73 % (2429604)Time elapsed: 0.168 s % 213.36/30.73 % (2429604)Peak memory usage: 91 MB % 213.36/30.73 % (2429604)Instructions burned: 316 (million) % 213.36/30.73 % (2429646)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=569728051:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2734 on theBenchmark for (2734ds/650Mi) % 213.36/30.73 % (2429586)Instruction limit reached! % 213.36/30.73 % (2429586)------------------------------ % 213.36/30.73 % (2429586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.36/30.73 % (2429586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.36/30.73 % (2429586)CaDiCaL version: 2.1.3 % 213.36/30.73 % (2429586)Termination reason: Instruction limit % 213.36/30.73 % (2429586)Termination phase: Saturation % 213.36/30.73 % (2429586)Time elapsed: 0.335 s % 213.36/30.73 % (2429586)Peak memory usage: 93 MB % 213.36/30.73 % (2429586)Instructions burned: 571 (million) % 213.36/30.73 % (2429659)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=807831925:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2732 on theBenchmark for (2732ds/496Mi) % 213.36/30.73 % (2429646)Instruction limit reached! % 213.36/30.73 % (2429646)------------------------------ % 213.36/30.73 % (2429646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.36/30.73 % (2429646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.36/30.73 % (2429646)CaDiCaL version: 2.1.3 % 213.36/30.73 % (2429646)Termination reason: Instruction limit % 213.36/30.73 % (2429646)Termination phase: Saturation % 213.36/30.73 % (2429646)Time elapsed: 0.364 s % 213.36/30.73 % (2429646)Peak memory usage: 92 MB % 213.36/30.73 % (2429646)Instructions burned: 650 (million) % 213.36/30.73 % (2429659)Instruction limit reached! % 213.36/30.73 % (2429659)------------------------------ % 213.36/30.73 % (2429659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.36/30.73 % (2429659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.36/30.73 % (2429659)CaDiCaL version: 2.1.3 % 213.36/30.73 % (2429659)Termination reason: Instruction limit % 213.36/30.73 % (2429659)Termination phase: Saturation % 213.36/30.73 % (2429659)Time elapsed: 0.286 s % 213.36/30.73 % (2429659)Peak memory usage: 93 MB % 213.36/30.73 % (2429659)Instructions burned: 496 (million) % 213.36/30.73 % (2429708)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=4105761126:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2729 on theBenchmark for (2729ds/588Mi) % 213.36/30.73 % (2429708)Refutation not found, incomplete strategy % 213.36/30.73 % (2429708)------------------------------ % 213.36/30.73 % (2429708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.36/30.73 % (2429708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.36/30.73 % (2429708)CaDiCaL version: 2.1.3 % 213.36/30.73 % (2429708)Termination reason: Refutation not found, incomplete strategy % 213.36/30.73 % (2429708)Time elapsed: 0.007 s % 213.36/30.73 % (2429708)Peak memory usage: 89 MB % 213.36/30.73 % (2429708)Instructions burned: 11 (million) % 218.97/31.64 % (2429709)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=2022533399:i=4700:rtra=on_2728 on theBenchmark for (2728ds/4700Mi) % 218.97/31.64 % (2429708)------------------------------ % 218.97/31.64 % (2429708)------------------------------ % 218.97/31.64 % (2429712)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2551941187:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2725 on theBenchmark for (2725ds/226Mi) % 218.97/31.64 % Exception at run slice level % 218.97/31.64 User error: GNN currently only supports monomorphic FOL. % 218.97/31.64 % (2429712)Instruction limit reached! % 218.97/31.64 % (2429712)------------------------------ % 218.97/31.64 % (2429712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.97/31.64 % (2429712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.97/31.64 % (2429712)CaDiCaL version: 2.1.3 % 218.97/31.64 % (2429712)Termination reason: Instruction limit % 218.97/31.64 % (2429712)Termination phase: Saturation % 218.97/31.64 % (2429712)Time elapsed: 0.133 s % 218.97/31.64 % (2429712)Peak memory usage: 93 MB % 218.97/31.64 % (2429712)Instructions burned: 227 (million) % 218.97/31.64 % (2429714)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=898727623:i=254:av=off:fsr=off:rtra=on:sup=off_2723 on theBenchmark for (2723ds/254Mi) % 218.97/31.64 % (2429714)Refutation not found, incomplete strategy % 218.97/31.64 % (2429714)------------------------------ % 218.97/31.64 % (2429714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.97/31.64 % (2429714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.97/31.64 % (2429714)CaDiCaL version: 2.1.3 % 218.97/31.64 % (2429714)Termination reason: Refutation not found, incomplete strategy % 218.97/31.64 % (2429714)Time elapsed: 0.006 s % 218.97/31.64 % (2429714)Peak memory usage: 88 MB % 218.97/31.64 % (2429714)Instructions burned: 10 (million) % 218.97/31.64 % (2429715)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=1543027997:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2722 on theBenchmark for (2722ds/228Mi) % 218.97/31.64 % (2429715)Refutation not found, incomplete strategy % 218.97/31.64 % (2429715)------------------------------ % 218.97/31.64 % (2429715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.97/31.64 % (2429715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.97/31.64 % (2429715)CaDiCaL version: 2.1.3 % 218.97/31.64 % (2429715)Termination reason: Refutation not found, incomplete strategy % 218.97/31.64 % (2429715)Time elapsed: 0.005 s % 218.97/31.64 % (2429715)Peak memory usage: 89 MB % 218.97/31.64 % (2429715)Instructions burned: 7 (million) % 218.97/31.64 % (2429714)------------------------------ % 218.97/31.64 % (2429714)------------------------------ % 218.97/31.64 % (2429715)------------------------------ % 218.97/31.64 % (2429715)------------------------------ % 218.97/31.64 % (2429718)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=3940571557:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2720 on theBenchmark for (2720ds/1814Mi) % 218.97/31.64 % (2429719)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=2944977907:i=874:sd=1:aac=none:rtra=on:ss=included_2719 on theBenchmark for (2719ds/874Mi) % 218.97/31.64 % (2429719)Refutation not found, incomplete strategy % 218.97/31.64 % (2429719)------------------------------ % 218.97/31.64 % (2429719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.97/31.64 % (2429719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.97/31.64 % (2429719)CaDiCaL version: 2.1.3 % 218.97/31.64 % (2429719)Termination reason: Refutation not found, incomplete strategy % 218.97/31.64 % (2429719)Time elapsed: 0.007 s % 218.97/31.64 % (2429719)Peak memory usage: 88 MB % 218.97/31.64 % (2429719)Instructions burned: 10 (million) % 218.97/31.64 % (2429719)------------------------------ % 218.97/31.64 % (2429719)------------------------------ % 218.97/31.64 % (2429722)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=3270602889:i=10404:rtra=on:ss=axioms:sgt=16_2715 on theBenchmark for (2715ds/10404Mi) % 218.97/31.64 % Exception at run slice level % 218.97/31.64 User error: GNN currently only supports monomorphic FOL. % 218.97/31.64 % (2429724)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2661250785:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2710 on theBenchmark for (2710ds/268Mi) % 218.97/31.64 % (2429718)Instruction limit reached! % 218.97/31.64 % (2429718)------------------------------ % 226.80/32.82 % (2429718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.80/32.82 % (2429718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.80/32.82 % (2429718)CaDiCaL version: 2.1.3 % 226.80/32.82 % (2429718)Termination reason: Instruction limit % 226.80/32.82 % (2429718)Termination phase: Saturation % 226.80/32.82 % (2429718)Time elapsed: 1.044 s % 226.80/32.82 % (2429718)Peak memory usage: 98 MB % 226.80/32.82 % (2429718)Instructions burned: 1814 (million) % 226.80/32.82 % (2429724)Instruction limit reached! % 226.80/32.82 % (2429724)------------------------------ % 226.80/32.82 % (2429724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.80/32.82 % (2429724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.80/32.82 % (2429724)CaDiCaL version: 2.1.3 % 226.80/32.82 % (2429724)Termination reason: Instruction limit % 226.80/32.82 % (2429724)Termination phase: Saturation % 226.80/32.82 % (2429724)Time elapsed: 0.132 s % 226.80/32.82 % (2429724)Peak memory usage: 90 MB % 226.80/32.82 % (2429724)Instructions burned: 270 (million) % 226.80/32.82 % (2429726)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=2695931682:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2708 on theBenchmark for (2708ds/1184Mi) % 226.80/32.82 % (2429727)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=3322246220:st=3:i=26386:sd=3:rtra=on:ss=axioms_2708 on theBenchmark for (2708ds/26386Mi) % 226.80/32.82 % Exception at run slice level % 226.80/32.82 User error: GNN currently only supports monomorphic FOL. % 226.80/32.82 % (2429730)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=2333112534:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2703 on theBenchmark for (2703ds/250Mi) % 226.80/32.82 % (2429730)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 226.80/32.82 % (2429730)Instruction limit reached! % 226.80/32.82 % (2429730)------------------------------ % 226.80/32.82 % (2429730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.80/32.82 % (2429730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.80/32.82 % (2429730)CaDiCaL version: 2.1.3 % 226.80/32.82 % (2429730)Termination reason: Instruction limit % 226.80/32.82 % (2429730)Termination phase: Saturation % 226.80/32.82 % (2429730)Time elapsed: 0.136 s % 226.80/32.82 % (2429730)Peak memory usage: 91 MB % 226.80/32.82 % (2429730)Instructions burned: 251 (million) % 226.80/32.82 % (2429726)Instruction limit reached! % 226.80/32.82 % (2429726)------------------------------ % 226.80/32.82 % (2429726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.80/32.82 % (2429726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.80/32.82 % (2429726)CaDiCaL version: 2.1.3 % 226.80/32.82 % (2429726)Termination reason: Instruction limit % 226.80/32.82 % (2429726)Termination phase: Saturation % 226.80/32.82 % (2429726)Time elapsed: 0.676 s % 226.80/32.82 % (2429726)Peak memory usage: 99 MB % 226.80/32.82 % (2429726)Instructions burned: 1185 (million) % 226.80/32.82 % (2429530)Instruction limit reached! % 226.80/32.82 % (2429530)------------------------------ % 226.80/32.82 % (2429530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.80/32.82 % (2429530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.80/32.82 % (2429530)CaDiCaL version: 2.1.3 % 226.80/32.82 % (2429530)Termination reason: Instruction limit % 226.80/32.82 % (2429530)Termination phase: Saturation % 226.80/32.82 % (2429530)Time elapsed: 10.380 s % 226.80/32.82 % (2429530)Peak memory usage: 235 MB % 226.80/32.82 % (2429530)Instructions burned: 21163 (million) % 226.80/32.82 % (2429732)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=3432380445:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2700 on theBenchmark for (2700ds/268Mi) % 226.80/32.82 % (2429733)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3554131523:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2700 on theBenchmark for (2700ds/282Mi) % 226.80/32.82 % (2429733)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 226.80/32.82 % (2429733)Refutation not found, incomplete strategy % 226.80/32.82 % (2429733)------------------------------ % 226.80/32.82 % (2429733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.80/32.82 % (2429733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.52/34.58 % (2429733)CaDiCaL version: 2.1.3 % 239.52/34.58 % (2429733)Termination reason: Refutation not found, incomplete strategy % 239.52/34.58 % (2429733)Time elapsed: 0.002 s % 239.52/34.58 % (2429733)Peak memory usage: 88 MB % 239.52/34.58 % (2429733)Instructions burned: 2 (million) % 239.52/34.58 % (2429734)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=2711064376:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2699 on theBenchmark for (2699ds/862Mi) % 239.52/34.58 % (2429732)Instruction limit reached! % 239.52/34.58 % (2429732)------------------------------ % 239.52/34.58 % (2429732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.52/34.58 % (2429732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.52/34.58 % (2429732)CaDiCaL version: 2.1.3 % 239.52/34.58 % (2429732)Termination reason: Instruction limit % 239.52/34.58 % (2429732)Termination phase: Saturation % 239.52/34.58 % (2429732)Time elapsed: 0.158 s % 239.52/34.58 % (2429732)Peak memory usage: 91 MB % 239.52/34.58 % (2429732)Instructions burned: 269 (million) % 239.52/34.58 % (2429733)------------------------------ % 239.52/34.58 % (2429733)------------------------------ % 239.52/34.58 % (2429738)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=454850866:i=12120:aac=none:ins=25:rtra=on_2697 on theBenchmark for (2697ds/12120Mi) % 239.52/34.58 % (2429739)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=705593389:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2696 on theBenchmark for (2696ds/300Mi) % 239.52/34.58 % (2429739)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 239.52/34.58 % (2429734)Instruction limit reached! % 239.52/34.58 % (2429734)------------------------------ % 239.52/34.58 % (2429734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.52/34.58 % (2429734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.52/34.58 % (2429734)CaDiCaL version: 2.1.3 % 239.52/34.58 % (2429734)Termination reason: Instruction limit % 239.52/34.58 % (2429734)Termination phase: Saturation % 239.52/34.58 % (2429734)Time elapsed: 0.347 s % 239.52/34.58 % (2429734)Peak memory usage: 91 MB % 239.52/34.58 % (2429734)Instructions burned: 863 (million) % 239.52/34.58 % (2429742)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=803510417:i=28310:bd=all:rtra=on_2694 on theBenchmark for (2694ds/28310Mi) % 239.52/34.58 % (2429739)Instruction limit reached! % 239.52/34.58 % (2429739)------------------------------ % 239.52/34.58 % (2429739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.52/34.58 % (2429739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.52/34.58 % (2429739)CaDiCaL version: 2.1.3 % 239.52/34.58 % (2429739)Termination reason: Instruction limit % 239.52/34.58 % (2429739)Termination phase: Saturation % 239.52/34.58 % (2429739)Time elapsed: 0.180 s % 239.52/34.58 % (2429739)Peak memory usage: 92 MB % 239.52/34.58 % (2429739)Instructions burned: 301 (million) % 239.52/34.58 % Exception at run slice level % 239.52/34.58 User error: GNN currently only supports monomorphic FOL. % 239.52/34.58 % (2429744)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=484712436:i=1334:av=off:fsr=off:rtra=on_2693 on theBenchmark for (2693ds/1334Mi) % 239.52/34.58 % (2429744)Refutation not found, incomplete strategy % 239.52/34.58 % (2429744)------------------------------ % 239.52/34.58 % (2429744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.52/34.58 % (2429744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.52/34.58 % (2429744)CaDiCaL version: 2.1.3 % 239.52/34.58 % (2429744)Termination reason: Refutation not found, incomplete strategy % 239.52/34.58 % (2429744)Time elapsed: 0.007 s % 239.52/34.58 % (2429744)Peak memory usage: 89 MB % 239.52/34.58 % (2429744)Instructions burned: 11 (million) % 239.52/34.58 % (2429745)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=1138704652:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2692 on theBenchmark for (2692ds/370Mi) % 239.52/34.58 % Exception at run slice level % 239.52/34.58 User error: GNN currently only supports monomorphic FOL. % 239.52/34.58 % (2429744)------------------------------ % 239.52/34.58 % (2429744)------------------------------ % 252.06/36.58 % (2429745)Instruction limit reached! % 252.06/36.58 % (2429745)------------------------------ % 252.06/36.58 % (2429745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.06/36.58 % (2429745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.06/36.58 % (2429745)CaDiCaL version: 2.1.3 % 252.06/36.58 % (2429745)Termination reason: Instruction limit % 252.06/36.58 % (2429745)Termination phase: Saturation % 252.06/36.58 % (2429745)Time elapsed: 0.190 s % 252.06/36.58 % (2429745)Peak memory usage: 91 MB % 252.06/36.58 % (2429745)Instructions burned: 371 (million) % 252.06/36.58 % (2429748)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=3108399838:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2689 on theBenchmark for (2689ds/386Mi) % 252.06/36.58 % (2429749)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=3914879819:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2689 on theBenchmark for (2689ds/9700Mi) % 252.06/36.58 % (2429749)Refutation not found, incomplete strategy % 252.06/36.58 % (2429749)------------------------------ % 252.06/36.58 % (2429749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.06/36.58 % (2429749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.06/36.58 % (2429749)CaDiCaL version: 2.1.3 % 252.06/36.58 % (2429749)Termination reason: Refutation not found, incomplete strategy % 252.06/36.58 % (2429749)Time elapsed: 0.005 s % 252.06/36.58 % (2429749)Peak memory usage: 88 MB % 252.06/36.58 % (2429749)Instructions burned: 9 (million) % 252.06/36.58 % (2429750)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=3865396576:i=24222:sd=1:rtra=on:ss=included_2689 on theBenchmark for (2689ds/24222Mi) % 252.06/36.58 % (2429748)Instruction limit reached! % 252.06/36.58 % (2429748)------------------------------ % 252.06/36.58 % (2429748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.06/36.58 % (2429748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.06/36.58 % (2429748)CaDiCaL version: 2.1.3 % 252.06/36.58 % (2429748)Termination reason: Instruction limit % 252.06/36.58 % (2429748)Termination phase: Saturation % 252.06/36.58 % (2429748)Time elapsed: 0.226 s % 252.06/36.58 % (2429748)Peak memory usage: 94 MB % 252.06/36.58 % (2429748)Instructions burned: 388 (million) % 252.06/36.58 % (2429749)------------------------------ % 252.06/36.58 % (2429749)------------------------------ % 252.06/36.58 % (2429754)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=1479405119:i=638:kws=precedence:fsr=off:rtra=on_2686 on theBenchmark for (2686ds/638Mi) % 252.06/36.58 % (2429755)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2731084687:i=4128:ep=RST:rtra=on_2685 on theBenchmark for (2685ds/4128Mi) % 252.06/36.58 % Exception at run slice level % 252.06/36.58 User error: GNN currently only supports monomorphic FOL. % 252.06/36.58 % (2429758)dis-1011_128_sil=32000:si=on:random_seed=1477794639:i=7412:ep=RST:av=off:rtra=on_2684 on theBenchmark for (2684ds/7412Mi) % 252.06/36.58 % (2429754)Instruction limit reached! % 252.06/36.58 % (2429754)------------------------------ % 252.06/36.58 % (2429754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.06/36.58 % (2429754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.06/36.58 % (2429754)CaDiCaL version: 2.1.3 % 252.06/36.58 % (2429754)Termination reason: Instruction limit % 252.06/36.58 % (2429754)Termination phase: Saturation % 252.06/36.58 % (2429754)Time elapsed: 0.343 s % 252.06/36.58 % (2429754)Peak memory usage: 94 MB % 252.06/36.58 % (2429754)Instructions burned: 639 (million) % 252.06/36.58 % (2429760)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3574734899:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2681 on theBenchmark for (2681ds/1514Mi) % 252.06/36.58 % (2429760)Refutation not found, incomplete strategy % 252.06/36.58 % (2429760)------------------------------ % 252.06/36.58 % (2429760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.06/36.58 % (2429760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.06/36.58 % (2429760)CaDiCaL version: 2.1.3 % 252.06/36.58 % (2429760)Termination reason: Refutation not found, incomplete strategy % 252.06/36.58 % (2429760)Time elapsed: 0.007 s % 252.06/36.58 % (2429760)Peak memory usage: 89 MB % 252.06/36.58 % (2429760)Instructions burned: 11 (million) % 252.06/36.58 % (2429760)------------------------------ % 252.06/36.58 % (2429760)------------------------------ % 270.75/39.17 % (2429762)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=1680544849:i=27826:rtra=on:ss=axioms:sgt=8_2677 on theBenchmark for (2677ds/27826Mi) % 270.75/39.17 % Exception at run slice level % 270.75/39.17 User error: GNN currently only supports monomorphic FOL. % 270.75/39.17 % (2429764)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=2751412417:i=19850:aac=none:rtra=on_2672 on theBenchmark for (2672ds/19850Mi) % 270.75/39.17 % (2429535)Instruction limit reached! % 270.75/39.17 % (2429535)------------------------------ % 270.75/39.17 % (2429535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.75/39.17 % (2429535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.75/39.17 % (2429535)CaDiCaL version: 2.1.3 % 270.75/39.17 % (2429535)Termination reason: Instruction limit % 270.75/39.17 % (2429535)Termination phase: Saturation % 270.75/39.17 % (2429535)Time elapsed: 12.896 s % 270.75/39.17 % (2429535)Peak memory usage: 254 MB % 270.75/39.17 % (2429535)Instructions burned: 23713 (million) % 270.75/39.17 % (2429551)Instruction limit reached! % 270.75/39.17 % (2429551)------------------------------ % 270.75/39.17 % (2429551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.75/39.17 % (2429551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.75/39.17 % (2429551)CaDiCaL version: 2.1.3 % 270.75/39.17 % (2429551)Termination reason: Instruction limit % 270.75/39.17 % (2429551)Termination phase: Saturation % 270.75/39.17 % (2429551)Time elapsed: 10.246 s % 270.75/39.17 % (2429551)Peak memory usage: 241 MB % 270.75/39.17 % (2429551)Instructions burned: 36828 (million) % 270.75/39.17 % (2429766)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1614159948:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2666 on theBenchmark for (2666ds/4958Mi) % 270.75/39.17 % (2429766)Refutation not found, incomplete strategy % 270.75/39.17 % (2429766)------------------------------ % 270.75/39.17 % (2429766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.75/39.17 % (2429766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.75/39.17 % (2429766)CaDiCaL version: 2.1.3 % 270.75/39.17 % (2429766)Termination reason: Refutation not found, incomplete strategy % 270.75/39.17 % (2429766)Time elapsed: 0.006 s % 270.75/39.17 % (2429766)Peak memory usage: 89 MB % 270.75/39.17 % (2429766)Instructions burned: 8 (million) % 270.75/39.17 % (2429767)ott+1002_64_sil=16000:si=on:sp=const_min:nwc=0.5:random_seed=3497954000:i=880:nm=2:av=off:rtra=on:gtg=exists_all:fdi=8:gsp=on_2665 on theBenchmark for (2665ds/880Mi) % 270.75/39.17 % (2429767)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 270.75/39.17 % (2429767)Instruction limit reached! % 270.75/39.17 % (2429767)------------------------------ % 270.75/39.17 % (2429767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.75/39.17 % (2429767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.75/39.17 % (2429767)CaDiCaL version: 2.1.3 % 270.75/39.17 % (2429767)Termination reason: Instruction limit % 270.75/39.17 % (2429767)Termination phase: Saturation % 270.75/39.17 % (2429767)Time elapsed: 0.222 s % 270.75/39.17 % (2429767)Peak memory usage: 96 MB % 270.75/39.17 % (2429767)Instructions burned: 883 (million) % 270.75/39.17 % (2429755)Instruction limit reached! % 270.75/39.17 % (2429755)------------------------------ % 270.75/39.17 % (2429755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.75/39.17 % (2429755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.75/39.17 % (2429755)CaDiCaL version: 2.1.3 % 270.75/39.17 % (2429755)Termination reason: Instruction limit % 270.75/39.17 % (2429755)Termination phase: Saturation % 270.75/39.17 % (2429755)Time elapsed: 2.305 s % 270.75/39.17 % (2429755)Peak memory usage: 115 MB % 270.75/39.17 % (2429755)Instructions burned: 4129 (million) % 270.75/39.17 % Exception at run slice level % 270.75/39.17 User error: GNN currently only supports monomorphic FOL. % 270.75/39.17 % (2429770)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:si=on:erd=off:lsd=100:bsr=unit_only:random_seed=2282080744:st=1.5:i=22290:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2662 on theBenchmark for (2662ds/22290Mi) % 270.75/39.17 % (2429771)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=2225271319:cts=off:i=6068:av=off:rtra=on:er=known:fsd=on_2661 on theBenchmark for (2661ds/6068Mi) % 278.13/40.30 % (2429772)lrs-1011_64:1_sil=8000:si=on:erd=off:urr=on:nwc=0.7:br=off:random_seed=823951983:st=2:s2a=on:i=1048:s2at=2:rtra=on:ss=axioms_2661 on theBenchmark for (2661ds/1048Mi) % 278.13/40.30 % (2429766)------------------------------ % 278.13/40.30 % (2429766)------------------------------ % 278.13/40.30 % Exception at run slice level % 278.13/40.30 User error: GNN currently only supports monomorphic FOL. % 278.13/40.30 % (2429776)lrs+1011_16:1_sil=8000:si=on:acc=on:urr=on:fd=preordered:flr=on:random_seed=1238165389:avsq=on:i=2032:avsqr=676809,524288:sd=1:rtra=on:ss=axioms_2660 on theBenchmark for (2660ds/2032Mi) % 278.13/40.30 % (2429777)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:si=on:s2agt=16:random_seed=2955790194:i=28246:bd=preordered:ins=4:rtra=on_2659 on theBenchmark for (2659ds/28246Mi) % 278.13/40.30 % Exception at run slice level % 278.13/40.30 User error: GNN currently only supports monomorphic FOL. % 278.13/40.30 % Exception at run slice level % 278.13/40.30 User error: GNN currently only supports monomorphic FOL. % 278.13/40.30 % (2429781)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:si=on:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=1871137994:i=4896:gtgl=5:bd=preordered:rtra=on:gtg=all_2656 on theBenchmark for (2656ds/4896Mi) % 278.13/40.30 % (2429780)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:si=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3270196912:i=11562:kws=precedence:bd=all:rtra=on:rawr=on_2656 on theBenchmark for (2656ds/11562Mi) % 278.13/40.30 % (2429772)Instruction limit reached! % 278.13/40.30 % (2429772)------------------------------ % 278.13/40.30 % (2429772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.13/40.30 % (2429772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.13/40.30 % (2429772)CaDiCaL version: 2.1.3 % 278.13/40.30 % (2429772)Termination reason: Instruction limit % 278.13/40.30 % (2429772)Termination phase: Saturation % 278.13/40.30 % (2429772)Time elapsed: 0.570 s % 278.13/40.30 % (2429772)Peak memory usage: 95 MB % 278.13/40.30 % (2429772)Instructions burned: 1049 (million) % 278.13/40.30 % Exception at run slice level % 278.13/40.30 User error: GNN currently only supports monomorphic FOL. % 278.13/40.30 % (2429784)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:si=on:lcm=reverse:random_seed=1925982055:i=6446:kws=precedence:fgj=on:av=off:rtra=on_2654 on theBenchmark for (2654ds/6446Mi) % 278.13/40.30 % (2429785)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:si=on:sp=occurrence:sos=on:random_seed=1654833339:st=5.6:i=4066:sd=3:rtra=on:ss=axioms_2653 on theBenchmark for (2653ds/4066Mi) % 278.13/40.30 % Exception at run slice level % 278.13/40.30 User error: GNN currently only supports monomorphic FOL. % 278.13/40.30 % (2429788)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:si=on:random_seed=743573389:i=4110:nm=16:rtra=on:gtg=position:ss=axioms:fsd=on_2650 on theBenchmark for (2650ds/4110Mi) % 278.13/40.30 % Exception at run slice level % 278.13/40.30 User error: GNN currently only supports monomorphic FOL. % 278.13/40.30 % (2429790)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:si=on:sp=const_frequency:spb=goal:acc=on:random_seed=3658923038:i=43222:sd=3:rtra=on:ss=axioms_2649 on theBenchmark for (2649ds/43222Mi) % 278.13/40.30 % Exception at run slice level % 278.13/40.30 User error: GNN currently only supports monomorphic FOL. % 278.13/40.30 % (2429776)Instruction limit reached! % 278.13/40.30 % (2429776)------------------------------ % 278.13/40.30 % (2429776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.13/40.30 % (2429776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.13/40.30 % (2429776)CaDiCaL version: 2.1.3 % 278.13/40.30 % (2429776)Termination reason: Instruction limit % 278.13/40.30 % (2429776)Termination phase: Saturation % 278.13/40.30 % (2429776)Time elapsed: 1.094 s % 278.13/40.30 % (2429776)Peak memory usage: 102 MB % 278.13/40.30 % (2429776)Instructions burned: 2033 (million) % 278.13/40.30 % (2429792)lrs+10_1_sil=8000:si=on:sp=occurrence:sos=all:lma=off:random_seed=2409148360:i=9670:sd=13:rtra=on:ss=axioms:sgt=23_2647 on theBenchmark for (2647ds/9670Mi) % 278.13/40.30 % (2429793)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:si=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=2880757442:st=5:i=1594:s2at=3:sd=4:bs=unit_only:av=off:rtra=on:sup=off:ss=included_2647 on theBenchmark for (2647ds/1594Mi) % 292.48/42.27 % (2429758)Instruction limit reached! % 292.48/42.27 % (2429758)------------------------------ % 292.48/42.27 % (2429758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.48/42.27 % (2429758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.48/42.27 % (2429758)CaDiCaL version: 2.1.3 % 292.48/42.27 % (2429758)Termination reason: Instruction limit % 292.48/42.27 % (2429758)Termination phase: Saturation % 292.48/42.27 % (2429758)Time elapsed: 4.273 s % 292.48/42.27 % (2429758)Peak memory usage: 126 MB % 292.48/42.27 % (2429758)Instructions burned: 7412 (million) % 292.48/42.27 % (2429796)lrs-1011_5_sil=8000:si=on:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=249878820:i=4652:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:rtra=on:fsd=on_2640 on theBenchmark for (2640ds/4652Mi) % 292.48/42.27 % Exception at run slice level % 292.48/42.27 User error: GNN currently only supports monomorphic FOL. % 292.48/42.27 % (2429798)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:si=on:sos=all:urr=on:br=off:random_seed=501027541:i=12076:nm=6:rtra=on_2638 on theBenchmark for (2638ds/12076Mi) % 292.48/42.27 % Exception at run slice level % 292.48/42.27 User error: GNN currently only supports monomorphic FOL. % 292.48/42.27 % (2429793)Instruction limit reached! % 292.48/42.27 % (2429793)------------------------------ % 292.48/42.27 % (2429793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.48/42.27 % (2429793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.48/42.27 % (2429793)CaDiCaL version: 2.1.3 % 292.48/42.27 % (2429793)Termination reason: Instruction limit % 292.48/42.27 % (2429793)Termination phase: Saturation % 292.48/42.27 % (2429793)Time elapsed: 0.716 s % 292.48/42.27 % (2429793)Peak memory usage: 105 MB % 292.48/42.27 % (2429793)Instructions burned: 1596 (million) % 292.48/42.27 % (2429800)lrs+10_1_sil=32000:si=on:sp=occurrence:random_seed=1777250481:st=2:i=66668:sd=3:rtra=on:ss=included:sgt=32_2633 on theBenchmark for (2633ds/66668Mi) % 292.48/42.27 % (2429801)lrs+10_4_sil=8000:plsq=on:si=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3025644536:st=3.7:s2a=on:i=2016:s2at=1.2:sd=3:bd=all:av=off:rtra=on:fdi=8:sup=off:ss=axioms_2633 on theBenchmark for (2633ds/2016Mi) % 292.48/42.27 % (2429539)Instruction limit reached! % 292.48/42.27 % (2429539)------------------------------ % 292.48/42.27 % (2429539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.48/42.27 % (2429539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.48/42.27 % (2429539)CaDiCaL version: 2.1.3 % 292.48/42.27 % (2429539)Termination reason: Instruction limit % 292.48/42.27 % (2429539)Termination phase: Saturation % 292.48/42.27 % (2429539)Time elapsed: 16.045 s % 292.48/42.27 % (2429539)Peak memory usage: 293 MB % 292.48/42.27 % (2429539)Instructions burned: 28957 (million) % 292.48/42.27 % (2429804)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:si=on:sp=const_frequency:spb=intro:gs=on:random_seed=4176673773:i=16654:s2at=5:bd=preordered:rtra=on_2626 on theBenchmark for (2626ds/16654Mi) % 292.48/42.27 % Exception at run slice level % 292.48/42.27 User error: GNN currently only supports monomorphic FOL. % 292.48/42.27 % (2429801)Instruction limit reached! % 292.48/42.27 % (2429801)------------------------------ % 292.48/42.27 % (2429801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.48/42.27 % (2429801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.48/42.27 % (2429801)CaDiCaL version: 2.1.3 % 292.48/42.27 % (2429801)Termination reason: Instruction limit % 292.48/42.27 % (2429801)Termination phase: Saturation % 292.48/42.27 % (2429801)Time elapsed: 1.117 s % 292.48/42.27 % (2429801)Peak memory usage: 109 MB % 292.48/42.27 % (2429801)Instructions burned: 2017 (million) % 292.48/42.27 % (2429806)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:si=on:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=524430431:s2a=on:i=2166:s2at=1.87328:slsql=off:ep=RSTC:rtra=on:fdi=16_2621 on theBenchmark for (2621ds/2166Mi) % 292.48/42.27 % (2429807)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:si=on:spb=goal:fd=preordered:random_seed=1120473683:i=2168:sd=1:bd=preordered:av=off:fsr=off:rtra=on:ss=axioms:sgt=14_2620 on theBenchmark for (2620ds/2168Mi) % 292.48/42.27 % (2429792)Instruction limit reached! % 292.48/42.27 % (2429792)------------------------------ % 292.48/42.27 % (2429792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.48/42.27 % (24297Terminated % 300.23/43.34 % Vampire exiting % 300.23/43.34 Terminated %------------------------------------------------------------------------------