%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW540_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 : n001.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:30:46 PM UTC 2026 % Result : Timeout 298.73s 43.11s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW540_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.09/0.19 % Computer : n001.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 14:24:03 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.23 Running first-order theorem proving % 0.09/0.23 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 % 7.20/1.67 % (374382)Detected formulas, will run a generic FOF schedule. % 7.20/1.67 % (374406)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4066903958:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 7.20/1.67 % (374407)dis-21_1_sil=8000:lcm=predicate:random_seed=1452843320: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) % 7.20/1.67 % (374404)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3891654848:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 7.20/1.67 % (374400)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=2696370967:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 7.20/1.67 % (374399)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=489180504:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 7.20/1.67 % (374403)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2335124700:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 7.20/1.67 % (374402)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=867895641:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 7.20/1.67 % (374403)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 7.20/1.67 % (374403)Refutation not found, incomplete strategy % 7.20/1.67 % (374403)------------------------------ % 7.20/1.67 % (374403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.20/1.67 % (374403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.20/1.67 % (374403)CaDiCaL version: 2.1.3 % 7.20/1.67 % (374403)Termination reason: Refutation not found, incomplete strategy % 7.20/1.67 % (374403)Time elapsed: 0.001 s % 7.20/1.67 % (374403)Peak memory usage: 88 MB % 7.20/1.67 % (374403)Instructions burned: 1 (million) % 7.20/1.67 % (374402)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 7.20/1.67 % (374406)Instruction limit reached! % 7.20/1.67 % (374406)------------------------------ % 7.20/1.67 % (374406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.20/1.67 % (374406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.20/1.67 % (374406)CaDiCaL version: 2.1.3 % 7.20/1.67 % (374406)Termination reason: Instruction limit % 7.20/1.67 % (374406)Termination phase: Saturation % 7.20/1.67 % (374406)Time elapsed: 0.051 s % 7.20/1.67 % (374406)Peak memory usage: 89 MB % 7.20/1.67 % (374406)Instructions burned: 142 (million) % 7.20/1.67 % (374404)Instruction limit reached! % 7.20/1.67 % (374404)------------------------------ % 7.20/1.67 % (374404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.20/1.67 % (374404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.20/1.67 % (374404)CaDiCaL version: 2.1.3 % 7.20/1.67 % (374404)Termination reason: Instruction limit % 7.20/1.67 % (374404)Termination phase: Saturation % 7.20/1.67 % (374404)Time elapsed: 0.067 s % 7.20/1.67 % (374404)Peak memory usage: 88 MB % 7.20/1.67 % (374404)Instructions burned: 119 (million) % 7.20/1.67 % (374407)Instruction limit reached! % 7.20/1.67 % (374407)------------------------------ % 7.20/1.67 % (374407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.20/1.67 % (374407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.20/1.67 % (374407)CaDiCaL version: 2.1.3 % 7.20/1.67 % (374407)Termination reason: Instruction limit % 7.20/1.67 % (374407)Termination phase: Saturation % 7.20/1.67 % (374407)Time elapsed: 0.076 s % 7.20/1.67 % (374407)Peak memory usage: 89 MB % 7.20/1.67 % (374407)Instructions burned: 134 (million) % 7.20/1.67 % (374480)lrs+10_1_sil=8000:sp=occurrence:random_seed=983211826:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 7.20/1.67 % (374485)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1593837128:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 7.20/1.67 % (374485)Refutation not found, incomplete strategy % 7.20/1.67 % (374485)------------------------------ % 7.20/1.67 % (374485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.20/1.67 % (374485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.19/2.15 % (374485)CaDiCaL version: 2.1.3 % 11.19/2.15 % (374485)Termination reason: Refutation not found, incomplete strategy % 11.19/2.15 % (374485)Time elapsed: 0.003 s % 11.19/2.15 % (374485)Peak memory usage: 88 MB % 11.19/2.15 % (374485)Instructions burned: 4 (million) % 11.19/2.15 % (374403)------------------------------ % 11.19/2.15 % (374403)------------------------------ % 11.19/2.15 % (374486)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2438285386:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 11.19/2.15 % (374480)Instruction limit reached! % 11.19/2.15 % (374480)------------------------------ % 11.19/2.15 % (374480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.19/2.15 % (374480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.19/2.15 % (374480)CaDiCaL version: 2.1.3 % 11.19/2.15 % (374480)Termination reason: Instruction limit % 11.19/2.15 % (374480)Termination phase: Saturation % 11.19/2.15 % (374480)Time elapsed: 0.094 s % 11.19/2.15 % (374480)Peak memory usage: 91 MB % 11.19/2.15 % (374480)Instructions burned: 287 (million) % 11.19/2.15 % Exception at run slice level % 11.19/2.15 User error: GNN currently only supports monomorphic FOL. % 11.19/2.15 % Exception at run slice level % 11.19/2.15 User error: GNN currently only supports monomorphic FOL. % 11.19/2.15 % (374528)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=787048450:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 11.19/2.15 % Exception at run slice level % 11.19/2.15 User error: GNN currently only supports monomorphic FOL. % 11.19/2.15 % (374529)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3216664113:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 11.19/2.15 % (374529)Refutation not found, incomplete strategy % 11.19/2.15 % (374529)------------------------------ % 11.19/2.15 % (374529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.19/2.15 % (374529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.19/2.15 % (374529)CaDiCaL version: 2.1.3 % 11.19/2.15 % (374529)Termination reason: Refutation not found, incomplete strategy % 11.19/2.15 % (374529)Time elapsed: 0.006 s % 11.19/2.15 % (374529)Peak memory usage: 88 MB % 11.19/2.15 % (374529)Instructions burned: 10 (million) % 11.19/2.15 % (374486)Instruction limit reached! % 11.19/2.15 % (374486)------------------------------ % 11.19/2.15 % (374486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.19/2.15 % (374486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.19/2.15 % (374486)CaDiCaL version: 2.1.3 % 11.19/2.15 % (374486)Termination reason: Instruction limit % 11.19/2.15 % (374486)Termination phase: Saturation % 11.19/2.15 % (374486)Time elapsed: 0.188 s % 11.19/2.15 % (374486)Peak memory usage: 90 MB % 11.19/2.15 % (374486)Instructions burned: 325 (million) % 11.19/2.15 % (374528)Instruction limit reached! % 11.19/2.15 % (374528)------------------------------ % 11.19/2.15 % (374528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.19/2.15 % (374528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.19/2.15 % (374528)CaDiCaL version: 2.1.3 % 11.19/2.15 % (374528)Termination reason: Instruction limit % 11.19/2.15 % (374528)Termination phase: Saturation % 11.19/2.15 % (374528)Time elapsed: 0.072 s % 11.19/2.15 % (374528)Peak memory usage: 90 MB % 11.19/2.15 % (374528)Instructions burned: 251 (million) % 11.19/2.15 % (374485)------------------------------ % 11.19/2.15 % (374485)------------------------------ % 11.19/2.15 % (374542)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=228935661:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 11.19/2.15 % (374542)Refutation not found, incomplete strategy % 11.19/2.15 % (374542)------------------------------ % 11.19/2.15 % (374542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.19/2.15 % (374542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.19/2.15 % (374542)CaDiCaL version: 2.1.3 % 11.19/2.15 % (374542)Termination reason: Refutation not found, incomplete strategy % 11.19/2.15 % (374542)Time elapsed: 0.007 s % 11.19/2.15 % (374542)Peak memory usage: 88 MB % 11.19/2.15 % (374542)Instructions burned: 10 (million) % 11.19/2.15 % (374540)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=114268850:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 13.03/2.51 % (374545)lrs+10_1_sil=8000:sp=occurrence:random_seed=1531593723:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi) % 13.03/2.51 % (374544)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2807289599:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 13.03/2.51 % (374539)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=423561776:i=2350_2994 on theBenchmark for (2994ds/2350Mi) % 13.03/2.51 % (374546)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1385160555:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi) % 13.03/2.51 % (374540)Instruction limit reached! % 13.03/2.51 % (374540)------------------------------ % 13.03/2.51 % (374540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.03/2.51 % (374540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.03/2.51 % (374540)CaDiCaL version: 2.1.3 % 13.03/2.51 % (374540)Termination reason: Instruction limit % 13.03/2.51 % (374540)Termination phase: Saturation % 13.03/2.51 % (374540)Time elapsed: 0.066 s % 13.03/2.51 % (374540)Peak memory usage: 89 MB % 13.03/2.51 % (374540)Instructions burned: 115 (million) % 13.03/2.51 % (374546)Refutation not found, incomplete strategy % 13.03/2.51 % (374546)------------------------------ % 13.03/2.51 % (374546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.03/2.51 % (374546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.03/2.51 % (374546)CaDiCaL version: 2.1.3 % 13.03/2.51 % (374546)Termination reason: Refutation not found, incomplete strategy % 13.03/2.51 % (374546)Time elapsed: 0.008 s % 13.03/2.51 % (374546)Peak memory usage: 88 MB % 13.03/2.51 % (374546)Instructions burned: 14 (million) % 13.03/2.51 % (374544)Instruction limit reached! % 13.03/2.51 % (374544)------------------------------ % 13.03/2.51 % (374544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.03/2.51 % (374544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.03/2.51 % (374544)CaDiCaL version: 2.1.3 % 13.03/2.51 % (374544)Termination reason: Instruction limit % 13.03/2.51 % (374544)Termination phase: Saturation % 13.03/2.51 % (374544)Time elapsed: 0.062 s % 13.03/2.51 % (374544)Peak memory usage: 88 MB % 13.03/2.51 % (374544)Instructions burned: 114 (million) % 13.03/2.51 % (374529)------------------------------ % 13.03/2.51 % (374529)------------------------------ % 13.03/2.51 % (374542)------------------------------ % 13.03/2.51 % (374542)------------------------------ % 13.03/2.51 % (374553)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1917614286:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi) % 13.03/2.51 % (374554)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=596705842:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2992 on theBenchmark for (2992ds/134Mi) % 13.03/2.51 % (374555)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4158828292:st=8:i=592:sd=3:ep=RST:ss=axioms_2991 on theBenchmark for (2991ds/592Mi) % 13.03/2.51 % (374545)Instruction limit reached! % 13.03/2.51 % (374545)------------------------------ % 13.03/2.51 % (374545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.03/2.51 % (374545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.03/2.51 % (374545)CaDiCaL version: 2.1.3 % 13.03/2.51 % (374545)Termination reason: Instruction limit % 13.03/2.51 % (374545)Termination phase: Saturation % 13.03/2.51 % (374545)Time elapsed: 0.315 s % 13.03/2.51 % (374545)Peak memory usage: 95 MB % 13.03/2.51 % (374545)Instructions burned: 907 (million) % 13.03/2.51 % (374554)Instruction limit reached! % 13.03/2.51 % (374554)------------------------------ % 13.03/2.51 % (374554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.03/2.51 % (374554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.03/2.51 % (374554)CaDiCaL version: 2.1.3 % 13.03/2.51 % (374554)Termination reason: Instruction limit % 13.03/2.51 % (374554)Termination phase: Saturation % 13.03/2.51 % (374554)Time elapsed: 0.122 s % 13.03/2.51 % (374554)Peak memory usage: 90 MB % 13.03/2.51 % (374554)Instructions burned: 134 (million) % 13.03/2.51 % (374546)------------------------------ % 13.03/2.51 % (374546)------------------------------ % 13.03/2.51 % Exception at run slice level % 13.03/2.51 User error: GNN currently only supports monomorphic FOL. % 13.03/2.51 % (374565)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3920980650:st=3:i=13193:sd=3:ss=axioms_2990 on theBenchmark for (2990ds/13193Mi) % 18.88/3.13 % (374568)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=622192117:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/125Mi) % 18.88/3.13 % (374568)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 18.88/3.13 % (374570)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1160583440:i=134:gtgl=5:slsql=off:gtg=exists_sym_2989 on theBenchmark for (2989ds/134Mi) % 18.88/3.13 % Exception at run slice level % 18.88/3.13 User error: Immediate (shared) subterms of term/literal list_case(X1,X0,X3,X2,nil(X0)) = sF17(X1,X0,X3,X2) have different types/not well-typed! % 18.88/3.13 % (374580)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3444384106:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2987 on theBenchmark for (2987ds/431Mi) % 18.88/3.13 % (374571)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1509480698:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/141Mi) % 18.88/3.13 % (374571)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 18.88/3.13 % (374571)Refutation not found, incomplete strategy % 18.88/3.13 % (374571)------------------------------ % 18.88/3.13 % (374571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.88/3.13 % (374571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.88/3.13 % (374571)CaDiCaL version: 2.1.3 % 18.88/3.13 % (374571)Termination reason: Refutation not found, incomplete strategy % 18.88/3.13 % (374571)Time elapsed: 0.002 s % 18.88/3.13 % (374571)Peak memory usage: 88 MB % 18.88/3.13 % (374571)Instructions burned: 1 (million) % 18.88/3.13 % (374580)Refutation not found, incomplete strategy % 18.88/3.13 % (374580)------------------------------ % 18.88/3.13 % (374580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.88/3.13 % (374580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.88/3.13 % (374580)CaDiCaL version: 2.1.3 % 18.88/3.13 % (374580)Termination reason: Refutation not found, incomplete strategy % 18.88/3.13 % (374580)Time elapsed: 0.003 s % 18.88/3.13 % (374580)Peak memory usage: 88 MB % 18.88/3.13 % (374580)Instructions burned: 3 (million) % 18.88/3.13 % (374568)Instruction limit reached! % 18.88/3.13 % (374568)------------------------------ % 18.88/3.13 % (374568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.88/3.13 % (374568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.88/3.13 % (374568)CaDiCaL version: 2.1.3 % 18.88/3.13 % (374568)Termination reason: Instruction limit % 18.88/3.13 % (374568)Termination phase: Saturation % 18.88/3.13 % (374568)Time elapsed: 0.138 s % 18.88/3.13 % (374568)Peak memory usage: 90 MB % 18.88/3.13 % (374568)Instructions burned: 125 (million) % 18.88/3.13 % Exception at run slice level % 18.88/3.13 User error: GNN currently only supports monomorphic FOL. % 18.88/3.13 % (374555)Instruction limit reached! % 18.88/3.13 % (374555)------------------------------ % 18.88/3.13 % (374555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.88/3.13 % (374555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.88/3.13 % (374555)CaDiCaL version: 2.1.3 % 18.88/3.13 % (374555)Termination reason: Instruction limit % 18.88/3.13 % (374555)Termination phase: Saturation % 18.88/3.13 % (374555)Time elapsed: 0.540 s % 18.88/3.13 % (374555)Peak memory usage: 92 MB % 18.88/3.13 % (374555)Instructions burned: 592 (million) % 18.88/3.13 % (374585)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=3755156073:i=6060:aac=none:ins=25_2986 on theBenchmark for (2986ds/6060Mi) % 18.88/3.13 % (374588)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=210206276:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2985 on theBenchmark for (2985ds/150Mi) % 18.88/3.13 % (374588)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 18.88/3.13 % (374580)------------------------------ % 18.88/3.13 % (374580)------------------------------ % 18.88/3.13 % (374571)------------------------------ % 18.88/3.13 % (374571)------------------------------ % 21.75/3.88 % Exception at run slice level % 21.75/3.88 User error: GNN currently only supports monomorphic FOL. % 21.75/3.88 % (374592)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1873982312:i=14155:bd=all_2984 on theBenchmark for (2984ds/14155Mi) % 21.75/3.88 % (374594)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3919153921:i=667:av=off:fsr=off_2984 on theBenchmark for (2984ds/667Mi) % 21.75/3.88 % (374594)Refutation not found, incomplete strategy % 21.75/3.88 % (374594)------------------------------ % 21.75/3.88 % (374594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.75/3.88 % (374594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.75/3.88 % (374594)CaDiCaL version: 2.1.3 % 21.75/3.88 % (374594)Termination reason: Refutation not found, incomplete strategy % 21.75/3.88 % (374594)Time elapsed: 0.008 s % 21.75/3.88 % (374594)Peak memory usage: 88 MB % 21.75/3.88 % (374594)Instructions burned: 13 (million) % 21.75/3.88 % (374588)Instruction limit reached! % 21.75/3.88 % (374588)------------------------------ % 21.75/3.88 % (374588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.75/3.88 % (374588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.75/3.88 % (374588)CaDiCaL version: 2.1.3 % 21.75/3.88 % (374588)Termination reason: Instruction limit % 21.75/3.88 % (374588)Termination phase: Saturation % 21.75/3.88 % (374588)Time elapsed: 0.100 s % 21.75/3.88 % (374588)Peak memory usage: 90 MB % 21.75/3.88 % (374588)Instructions burned: 151 (million) % 21.75/3.88 % Exception at run slice level % 21.75/3.88 User error: GNN currently only supports monomorphic FOL. % 21.75/3.88 % (374596)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=1603236727:s2a=on:i=185:s2at=1.8:fdi=4_2983 on theBenchmark for (2983ds/185Mi) % 21.75/3.88 % (374597)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2441678439:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2982 on theBenchmark for (2982ds/193Mi) % 21.75/3.88 % (374598)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3240699887:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2982 on theBenchmark for (2982ds/4850Mi) % 21.75/3.88 % (374598)Refutation not found, incomplete strategy % 21.75/3.88 % (374598)------------------------------ % 21.75/3.88 % (374598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.75/3.88 % (374598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.75/3.88 % (374598)CaDiCaL version: 2.1.3 % 21.75/3.88 % (374598)Termination reason: Refutation not found, incomplete strategy % 21.75/3.88 % (374598)Time elapsed: 0.006 s % 21.75/3.88 % (374598)Peak memory usage: 88 MB % 21.75/3.88 % (374598)Instructions burned: 11 (million) % 21.75/3.88 % (374601)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2532733149:i=12111:sd=1:ss=included_2982 on theBenchmark for (2982ds/12111Mi) % 21.75/3.88 % (374596)Instruction limit reached! % 21.75/3.88 % (374596)------------------------------ % 21.75/3.88 % (374596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.75/3.88 % (374596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.75/3.88 % (374596)CaDiCaL version: 2.1.3 % 21.75/3.88 % (374596)Termination reason: Instruction limit % 21.75/3.88 % (374596)Termination phase: Saturation % 21.75/3.88 % (374596)Time elapsed: 0.118 s % 21.75/3.88 % (374596)Peak memory usage: 91 MB % 21.75/3.88 % (374596)Instructions burned: 185 (million) % 21.75/3.88 % (374603)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4253959463:i=319:kws=precedence:fsr=off_2981 on theBenchmark for (2981ds/319Mi) % 21.75/3.88 % (374597)Instruction limit reached! % 21.75/3.88 % (374597)------------------------------ % 21.75/3.88 % (374597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.75/3.88 % (374597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.75/3.88 % (374597)CaDiCaL version: 2.1.3 % 21.75/3.88 % (374597)Termination reason: Instruction limit % 21.75/3.88 % (374597)Termination phase: Saturation % 21.75/3.88 % (374597)Time elapsed: 0.107 s % 21.75/3.88 % (374597)Peak memory usage: 90 MB % 21.75/3.88 % (374597)Instructions burned: 196 (million) % 21.75/3.88 % (374594)------------------------------ % 21.75/3.88 % (374594)------------------------------ % 21.75/3.88 % (374603)Instruction limit reached! % 29.27/4.99 % (374603)------------------------------ % 29.27/4.99 % (374603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.27/4.99 % (374603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.27/4.99 % (374603)CaDiCaL version: 2.1.3 % 29.27/4.99 % (374603)Termination reason: Instruction limit % 29.27/4.99 % (374603)Termination phase: Saturation % 29.27/4.99 % (374603)Time elapsed: 0.090 s % 29.27/4.99 % (374603)Peak memory usage: 91 MB % 29.27/4.99 % (374603)Instructions burned: 321 (million) % 29.27/4.99 % Exception at run slice level % 29.27/4.99 User error: GNN currently only supports monomorphic FOL. % 29.27/4.99 % (374622)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2658801605:i=2064:ep=RST_2980 on theBenchmark for (2980ds/2064Mi) % 29.27/4.99 % (374626)dis-1011_128_sil=32000:random_seed=1789950613:i=3706:ep=RST:av=off_2980 on theBenchmark for (2980ds/3706Mi) % 29.27/4.99 % (374598)------------------------------ % 29.27/4.99 % (374598)------------------------------ % 29.27/4.99 % (374632)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1618975091:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2980 on theBenchmark for (2980ds/757Mi) % 29.27/4.99 % (374632)Refutation not found, incomplete strategy % 29.27/4.99 % (374632)------------------------------ % 29.27/4.99 % (374632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.27/4.99 % (374632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.27/4.99 % (374632)CaDiCaL version: 2.1.3 % 29.27/4.99 % (374632)Termination reason: Refutation not found, incomplete strategy % 29.27/4.99 % (374632)Time elapsed: 0.007 s % 29.27/4.99 % (374632)Peak memory usage: 88 MB % 29.27/4.99 % (374632)Instructions burned: 11 (million) % 29.27/4.99 % (374665)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2665288538:i=13913:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/13913Mi) % 29.27/4.99 % (374682)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=249740623:i=9925:aac=none_2979 on theBenchmark for (2979ds/9925Mi) % 29.27/4.99 % (374696)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2593549053:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2978 on theBenchmark for (2978ds/2479Mi) % 29.27/4.99 % (374696)Refutation not found, incomplete strategy % 29.27/4.99 % (374696)------------------------------ % 29.27/4.99 % (374696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.27/4.99 % (374696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.27/4.99 % (374696)CaDiCaL version: 2.1.3 % 29.27/4.99 % (374696)Termination reason: Refutation not found, incomplete strategy % 29.27/4.99 % (374696)Time elapsed: 0.003 s % 29.27/4.99 % (374696)Peak memory usage: 88 MB % 29.27/4.99 % (374696)Instructions burned: 3 (million) % 29.27/4.99 % Exception at run slice level % 29.27/4.99 User error: GNN currently only supports monomorphic FOL. % 29.27/4.99 % Exception at run slice level % 29.27/4.99 User error: GNN currently only supports monomorphic FOL. % 29.27/4.99 % (374632)------------------------------ % 29.27/4.99 % (374632)------------------------------ % 29.27/4.99 % (374726)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2238649204:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2976 on theBenchmark for (2976ds/440Mi) % 29.27/4.99 % (374726)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 29.27/4.99 % (374735)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3159563567:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2976 on theBenchmark for (2976ds/11145Mi) % 29.27/4.99 % (374696)------------------------------ % 29.27/4.99 % (374696)------------------------------ % 29.27/4.99 % (374748)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=1736811131:cts=off:i=3034:av=off:er=known:fsd=on_2976 on theBenchmark for (2976ds/3034Mi) % 29.27/4.99 % Exception at run slice level % 29.27/4.99 User error: GNN currently only supports monomorphic FOL. % 29.27/4.99 % Exception at run slice level % 29.27/4.99 User error: GNN currently only supports monomorphic FOL. % 29.27/4.99 % (374779)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3237617735:st=2:s2a=on:i=524:s2at=2:ss=axioms_2974 on theBenchmark for (2974ds/524Mi) % 29.27/4.99 % (374726)Instruction limit reached! % 37.10/5.90 % (374726)------------------------------ % 37.10/5.90 % (374726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.10/5.90 % (374726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.10/5.90 % (374726)CaDiCaL version: 2.1.3 % 37.10/5.90 % (374726)Termination reason: Instruction limit % 37.10/5.90 % (374726)Termination phase: Saturation % 37.10/5.90 % (374726)Time elapsed: 0.216 s % 37.10/5.90 % (374726)Peak memory usage: 91 MB % 37.10/5.90 % (374726)Instructions burned: 442 (million) % 37.10/5.90 % (374780)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2660966414:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2973 on theBenchmark for (2973ds/1016Mi) % 37.10/5.90 % (374780)Refutation not found, incomplete strategy % 37.10/5.90 % (374780)------------------------------ % 37.10/5.90 % (374780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.10/5.90 % (374780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.10/5.90 % (374780)CaDiCaL version: 2.1.3 % 37.10/5.90 % (374780)Termination reason: Refutation not found, incomplete strategy % 37.10/5.90 % (374780)Time elapsed: 0.003 s % 37.10/5.90 % (374780)Peak memory usage: 89 MB % 37.10/5.90 % (374780)Instructions burned: 2 (million) % 37.10/5.90 % (374781)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3117366959:i=14123:bd=preordered:ins=4_2973 on theBenchmark for (2973ds/14123Mi) % 37.10/5.90 % (374783)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2505019608:i=5781:kws=precedence:bd=all:rawr=on_2973 on theBenchmark for (2973ds/5781Mi) % 37.10/5.90 % Exception at run slice level % 37.10/5.90 User error: GNN currently only supports monomorphic FOL. % 37.10/5.90 % (374779)Instruction limit reached! % 37.10/5.90 % (374779)------------------------------ % 37.10/5.90 % (374779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.10/5.90 % (374779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.10/5.90 % (374779)CaDiCaL version: 2.1.3 % 37.10/5.90 % (374779)Termination reason: Instruction limit % 37.10/5.90 % (374779)Termination phase: Saturation % 37.10/5.90 % (374779)Time elapsed: 0.266 s % 37.10/5.90 % (374779)Peak memory usage: 90 MB % 37.10/5.90 % (374779)Instructions burned: 526 (million) % 37.10/5.90 % Exception at run slice level % 37.10/5.90 User error: GNN currently only supports monomorphic FOL. % 37.10/5.90 % (374780)------------------------------ % 37.10/5.90 % (374780)------------------------------ % 37.10/5.90 % (374788)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=2389395670:i=2448:gtgl=5:bd=preordered:gtg=all_2971 on theBenchmark for (2971ds/2448Mi) % 37.10/5.90 % (374789)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=265681568:i=3223:kws=precedence:fgj=on:av=off_2970 on theBenchmark for (2970ds/3223Mi) % 37.10/5.90 % (374790)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=4079780642:st=5.6:i=2033:sd=3:ss=axioms_2970 on theBenchmark for (2970ds/2033Mi) % 37.10/5.90 % (374791)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=308953130:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2970 on theBenchmark for (2970ds/2055Mi) % 37.10/5.90 % (374622)Instruction limit reached! % 37.10/5.90 % (374622)------------------------------ % 37.10/5.90 % (374622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.10/5.90 % (374622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.10/5.90 % (374622)CaDiCaL version: 2.1.3 % 37.10/5.90 % (374622)Termination reason: Instruction limit % 37.10/5.90 % (374622)Termination phase: Saturation % 37.10/5.90 % (374622)Time elapsed: 1.173 s % 37.10/5.90 % (374622)Peak memory usage: 99 MB % 37.10/5.90 % (374622)Instructions burned: 2065 (million) % 37.10/5.90 % Exception at run slice level % 37.10/5.90 User error: GNN currently only supports monomorphic FOL. % 37.10/5.90 % (374797)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2093599026:i=4835:sd=13:ss=axioms:sgt=23_2967 on theBenchmark for (2967ds/4835Mi) % 37.10/5.90 % (374796)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=3471874970:i=21611:sd=3:ss=axioms_2967 on theBenchmark for (2967ds/21611Mi) % 37.10/5.90 % Exception at run slice level % 37.10/5.90 User error: GNN currently only supports monomorphic FOL. % 47.17/7.19 % Exception at run slice level % 47.17/7.19 User error: GNN currently only supports monomorphic FOL. % 47.17/7.19 % Exception at run slice level % 47.17/7.19 User error: GNN currently only supports monomorphic FOL. % 47.17/7.19 % (374800)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=1342132121:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2965 on theBenchmark for (2965ds/797Mi) % 47.17/7.19 % (374801)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2373682396:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2965 on theBenchmark for (2965ds/2326Mi) % 47.17/7.19 % (374801)Refutation not found, incomplete strategy % 47.17/7.19 % (374801)------------------------------ % 47.17/7.19 % (374801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.17/7.19 % (374801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.17/7.19 % (374801)CaDiCaL version: 2.1.3 % 47.17/7.19 % (374801)Termination reason: Refutation not found, incomplete strategy % 47.17/7.19 % (374801)Time elapsed: 0.012 s % 47.17/7.19 % (374801)Peak memory usage: 89 MB % 47.17/7.19 % (374801)Instructions burned: 18 (million) % 47.17/7.19 % (374802)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1943020111:i=6038:nm=6_2964 on theBenchmark for (2964ds/6038Mi) % 47.17/7.19 % Exception at run slice level % 47.17/7.19 User error: GNN currently only supports monomorphic FOL. % 47.17/7.19 % (374801)------------------------------ % 47.17/7.19 % (374801)------------------------------ % 47.17/7.19 % (374806)lrs+10_1_sil=32000:sp=occurrence:random_seed=1523610256:st=2:i=33334:sd=3:ss=included:sgt=32_2962 on theBenchmark for (2962ds/33334Mi) % 47.17/7.19 % (374800)Instruction limit reached! % 47.17/7.19 % (374800)------------------------------ % 47.17/7.19 % (374800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.17/7.19 % (374800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.17/7.19 % (374800)CaDiCaL version: 2.1.3 % 47.17/7.19 % (374800)Termination reason: Instruction limit % 47.17/7.19 % (374800)Termination phase: Saturation % 47.17/7.19 % (374800)Time elapsed: 0.448 s % 47.17/7.19 % (374800)Peak memory usage: 94 MB % 47.17/7.19 % (374800)Instructions burned: 797 (million) % 47.17/7.19 % (374807)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1997583505:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2961 on theBenchmark for (2961ds/1008Mi) % 47.17/7.19 % Exception at run slice level % 47.17/7.19 User error: GNN currently only supports monomorphic FOL. % 47.17/7.19 % (374810)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=196164941:i=8327:s2at=5:bd=preordered_2959 on theBenchmark for (2959ds/8327Mi) % 47.17/7.19 % (374811)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=1159919011:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2959 on theBenchmark for (2959ds/1083Mi) % 47.17/7.19 % (374626)Instruction limit reached! % 47.17/7.19 % (374626)------------------------------ % 47.17/7.19 % (374626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.17/7.19 % (374626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.17/7.19 % (374626)CaDiCaL version: 2.1.3 % 47.17/7.19 % (374626)Termination reason: Instruction limit % 47.17/7.19 % (374626)Termination phase: Saturation % 47.17/7.19 % (374626)Time elapsed: 2.138 s % 47.17/7.19 % (374626)Peak memory usage: 120 MB % 47.17/7.19 % (374626)Instructions burned: 3707 (million) % 47.17/7.19 % (374814)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=4105356041:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2957 on theBenchmark for (2957ds/1084Mi) % 47.17/7.19 % (374807)Instruction limit reached! % 47.17/7.19 % (374807)------------------------------ % 47.17/7.19 % (374807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.17/7.19 % (374807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.17/7.19 % (374807)CaDiCaL version: 2.1.3 % 47.17/7.19 % (374807)Termination reason: Instruction limit % 47.17/7.19 % (374807)Termination phase: Saturation % 55.77/8.45 % (374807)Time elapsed: 0.501 s % 55.77/8.45 % (374807)Peak memory usage: 93 MB % 55.77/8.45 % (374807)Instructions burned: 1010 (million) % 55.77/8.45 % Exception at run slice level % 55.77/8.45 User error: GNN currently only supports monomorphic FOL. % 55.77/8.45 % (374817)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=3218433100:st=2:i=6225:sd=15:ss=axioms_2954 on theBenchmark for (2954ds/6225Mi) % 55.77/8.45 % (374816)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1732577373:i=6995:s2at=5:gtg=all_2954 on theBenchmark for (2954ds/6995Mi) % 55.77/8.45 % Exception at run slice level % 55.77/8.45 User error: Immediate (shared) subterms of term/literal product(X1,X0,nil(X1),X2) = sF13(X1,X0,X2) have different types/not well-typed! % 55.77/8.45 % (374811)Instruction limit reached! % 55.77/8.45 % (374811)------------------------------ % 55.77/8.45 % (374811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.77/8.45 % (374811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.77/8.45 % (374811)CaDiCaL version: 2.1.3 % 55.77/8.45 % (374811)Termination reason: Instruction limit % 55.77/8.45 % (374811)Termination phase: Saturation % 55.77/8.45 % (374811)Time elapsed: 0.564 s % 55.77/8.45 % (374811)Peak memory usage: 97 MB % 55.77/8.45 % (374811)Instructions burned: 1084 (million) % 55.77/8.45 % (374797)Instruction limit reached! % 55.77/8.45 % (374797)------------------------------ % 55.77/8.45 % (374797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.77/8.45 % (374797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.77/8.45 % (374797)CaDiCaL version: 2.1.3 % 55.77/8.45 % (374797)Termination reason: Instruction limit % 55.77/8.45 % (374797)Termination phase: Saturation % 55.77/8.45 % (374797)Time elapsed: 1.390 s % 55.77/8.45 % (374797)Peak memory usage: 115 MB % 55.77/8.45 % (374797)Instructions burned: 4837 (million) % 55.77/8.45 % (374820)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2248220494:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2953 on theBenchmark for (2953ds/3372Mi) % 55.77/8.45 % (374821)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2551021914:st=2.3:i=26457:sd=10:ss=included:sgt=8_2952 on theBenchmark for (2952ds/26457Mi) % 55.77/8.45 % (374822)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=14086373:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2951 on theBenchmark for (2951ds/13494Mi) % 55.77/8.45 % (374814)Instruction limit reached! % 55.77/8.45 % (374814)------------------------------ % 55.77/8.45 % (374814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.77/8.45 % (374814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.77/8.45 % (374814)CaDiCaL version: 2.1.3 % 55.77/8.45 % (374814)Termination reason: Instruction limit % 55.77/8.45 % (374814)Termination phase: Saturation % 55.77/8.45 % (374814)Time elapsed: 0.562 s % 55.77/8.45 % (374814)Peak memory usage: 95 MB % 55.77/8.45 % (374814)Instructions burned: 1085 (million) % 55.77/8.45 % Exception at run slice level % 55.77/8.45 User error: GNN currently only supports monomorphic FOL. % 55.77/8.45 % (374826)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=4116174772:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2950 on theBenchmark for (2950ds/2503Mi) % 55.77/8.45 % (374826)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 55.77/8.45 % Exception at run slice level % 55.77/8.45 User error: GNN currently only supports monomorphic FOL. % 55.77/8.45 % (374827)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=1220008386:i=2559:sd=1:ep=RSTC:ss=axioms_2948 on theBenchmark for (2948ds/2559Mi) % 55.77/8.45 % Exception at run slice level % 55.77/8.45 User error: GNN currently only supports monomorphic FOL. % 55.77/8.45 % (374829)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2754488522:i=30753:av=off:ss=included_2947 on theBenchmark for (2947ds/30753Mi) % 55.77/8.45 % (374831)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3008963982:i=26473:ep=RSTC_2947 on theBenchmark for (2947ds/26473Mi) % 55.77/8.45 % Exception at run slice level % 67.52/10.54 User error: GNN currently only supports monomorphic FOL. % 67.52/10.54 % Exception at run slice level % 67.52/10.54 User error: GNN currently only supports monomorphic FOL. % 67.52/10.54 % (374834)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=314754981:cts=off:i=2759:kws=inv_arity:fgj=on_2945 on theBenchmark for (2945ds/2759Mi) % 67.52/10.54 % (374835)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=1978711499:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2944 on theBenchmark for (2944ds/5665Mi) % 67.52/10.54 % (374835)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 67.52/10.54 % Exception at run slice level % 67.52/10.54 User error: GNN currently only supports monomorphic FOL. % 67.52/10.54 % (374783)Instruction limit reached! % 67.52/10.54 % (374783)------------------------------ % 67.52/10.54 % (374783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.52/10.54 % (374783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.52/10.54 % (374783)CaDiCaL version: 2.1.3 % 67.52/10.54 % (374783)Termination reason: Instruction limit % 67.52/10.54 % (374783)Termination phase: Saturation % 67.52/10.54 % (374783)Time elapsed: 2.925 s % 67.52/10.54 % (374783)Peak memory usage: 107 MB % 67.52/10.54 % (374783)Instructions burned: 5782 (million) % 67.52/10.54 % Exception at run slice level % 67.52/10.54 User error: GNN currently only supports monomorphic FOL. % 67.52/10.54 % (374838)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=2903815978:i=1532:ep=RS:ss=axioms_2942 on theBenchmark for (2942ds/1532Mi) % 67.52/10.54 % (374840)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=2431773674:i=1572:fgj=on:gsp=on_2942 on theBenchmark for (2942ds/1572Mi) % 67.52/10.54 % (374840)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 67.52/10.54 % (374839)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=2189973406:i=1565:sd=2:ss=axioms:sgt=32_2942 on theBenchmark for (2942ds/1565Mi) % 67.52/10.54 % Exception at run slice level % 67.52/10.54 User error: GNN currently only supports monomorphic FOL. % 67.52/10.54 % Exception at run slice level % 67.52/10.54 User error: GNN currently only supports monomorphic FOL. % 67.52/10.54 % (374845)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=397824694:i=3500:sd=1:bd=preordered:sup=off:ss=included_2939 on theBenchmark for (2939ds/3500Mi) % 67.52/10.54 % (374844)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=583792123:i=6052:sd=4:ss=axioms:sgt=24_2939 on theBenchmark for (2939ds/6052Mi) % 67.52/10.54 % Exception at run slice level % 67.52/10.54 User error: GNN currently only supports monomorphic FOL. % 67.52/10.54 % Exception at run slice level % 67.52/10.54 User error: GNN currently only supports monomorphic FOL. % 67.52/10.54 % Exception at run slice level % 67.52/10.54 User error: GNN currently only supports monomorphic FOL. % 67.52/10.54 % (374848)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=2814552443:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2937 on theBenchmark for (2937ds/1842Mi) % 67.52/10.54 % (374848)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 67.52/10.54 % (374849)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3246237487:i=66096:add=on_2937 on theBenchmark for (2937ds/66096Mi) % 67.52/10.54 % (374851)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=3019190705:i=1884:sd=1:nm=60:ss=axioms_2936 on theBenchmark for (2936ds/1884Mi) % 67.52/10.54 % Exception at run slice level % 67.52/10.54 User error: GNN currently only supports monomorphic FOL. % 67.52/10.54 % Exception at run slice level % 67.52/10.54 User error: GNN currently only supports monomorphic FOL. % 67.52/10.54 % (374854)lrs-1011_4:1_sil=16000:bsr=on:random_seed=2220705442:cts=off:i=5469:bs=on:fsr=off_2934 on theBenchmark for (2934ds/5469Mi) % 77.24/11.92 % Exception at run slice level % 77.24/11.92 User error: GNN currently only supports monomorphic FOL. % 77.24/11.92 % Exception at run slice level % 77.24/11.92 User error: GNN currently only supports monomorphic FOL. % 77.24/11.92 % (374855)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=2411337526:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2932 on theBenchmark for (2932ds/2037Mi) % 77.24/11.92 % (374857)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3271906645:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2932 on theBenchmark for (2932ds/2110Mi) % 77.24/11.92 % (374858)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=1323489657:i=2430:add=off:aac=none:nm=16_2932 on theBenchmark for (2932ds/2430Mi) % 77.24/11.92 % Exception at run slice level % 77.24/11.92 User error: GNN currently only supports monomorphic FOL. % 77.24/11.92 % (374862)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=4048522656:cond=fast:i=4891_2929 on theBenchmark for (2929ds/4891Mi) % 77.24/11.92 % Exception at run slice level % 77.24/11.92 User error: GNN currently only supports monomorphic FOL. % 77.24/11.92 % Exception at run slice level % 77.24/11.92 User error: GNN currently only supports monomorphic FOL. % 77.24/11.92 % Exception at run slice level % 77.24/11.92 User error: GNN currently only supports monomorphic FOL. % 77.24/11.92 % (374864)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=3462178902:st=2:i=14845:sd=2:ss=included:fsd=on_2927 on theBenchmark for (2927ds/14845Mi) % 77.24/11.92 % (374865)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=960828453:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2926 on theBenchmark for (2926ds/7534Mi) % 77.24/11.92 % (374866)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=3785373967:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2926 on theBenchmark for (2926ds/10353Mi) % 77.24/11.92 % Exception at run slice level % 77.24/11.92 User error: GNN currently only supports monomorphic FOL. % 77.24/11.92 % Exception at run slice level % 77.24/11.92 User error: GNN currently only supports monomorphic FOL. % 77.24/11.92 % Exception at run slice level % 77.24/11.92 User error: GNN currently only supports monomorphic FOL. % 77.24/11.92 % (374870)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=983232901:i=7860_2922 on theBenchmark for (2922ds/7860Mi) % 77.24/11.92 % (374870)Refutation not found, incomplete strategy % 77.24/11.92 % (374870)------------------------------ % 77.24/11.92 % (374870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.24/11.92 % (374870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.24/11.92 % (374870)CaDiCaL version: 2.1.3 % 77.24/11.92 % (374870)Termination reason: Refutation not found, incomplete strategy % 77.24/11.92 % (374870)Time elapsed: 0.004 s % 77.24/11.92 % (374870)Peak memory usage: 88 MB % 77.24/11.92 % (374870)Instructions burned: 13 (million) % 77.24/11.92 % (374817)Instruction limit reached! % 77.24/11.92 % (374817)------------------------------ % 77.24/11.92 % (374817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.24/11.92 % (374817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.24/11.92 % (374817)CaDiCaL version: 2.1.3 % 77.24/11.92 % (374817)Termination reason: Instruction limit % 77.24/11.92 % (374817)Termination phase: Saturation % 77.24/11.92 % (374817)Time elapsed: 3.274 s % 77.24/11.92 % (374817)Peak memory usage: 117 MB % 77.24/11.92 % (374817)Instructions burned: 6225 (million) % 77.24/11.92 % (374871)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=3959870749:i=7896:sd=2:bs=on:ss=included:sgt=20_2921 on theBenchmark for (2921ds/7896Mi) % 77.24/11.92 % (374873)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=22285732:i=5812:gtgl=2:gtg=all_2921 on theBenchmark for (2921ds/5812Mi) % 111.60/16.79 % (374870)------------------------------ % 111.60/16.79 % (374870)------------------------------ % 111.60/16.79 % (374875)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=3622687692:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2920 on theBenchmark for (2920ds/2965Mi) % 111.60/16.79 % (374877)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=3154133514:i=2967:kws=precedence:bd=preordered:av=off_2920 on theBenchmark for (2920ds/2967Mi) % 111.60/16.79 % Exception at run slice level % 111.60/16.79 User error: GNN currently only supports monomorphic FOL. % 111.60/16.79 % Exception at run slice level % 111.60/16.79 User error: GNN currently only supports monomorphic FOL. % 111.60/16.79 % Exception at run slice level % 111.60/16.79 User error: GNN currently only supports monomorphic FOL. % 111.60/16.79 % (374880)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=485389130:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2916 on theBenchmark for (2916ds/3022Mi) % 111.60/16.79 % Exception at run slice level % 111.60/16.79 User error: GNN currently only supports monomorphic FOL. % 111.60/16.79 % (374881)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=346699978:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2916 on theBenchmark for (2916ds/3207Mi) % 111.60/16.79 % (374882)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=670821654:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2915 on theBenchmark for (2915ds/3289Mi) % 111.60/16.79 % Exception at run slice level % 111.60/16.79 User error: GNN currently only supports monomorphic FOL. % 111.60/16.79 % (374884)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=357428814:i=38569:sd=3:ss=axioms:sgt=32_2915 on theBenchmark for (2915ds/38569Mi) % 111.60/16.79 % (374888)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=2262641751:cts=off:i=3394_2913 on theBenchmark for (2913ds/3394Mi) % 111.60/16.79 % Exception at run slice level % 111.60/16.79 User error: GNN currently only supports monomorphic FOL. % 111.60/16.79 % Exception at run slice level % 111.60/16.79 User error: GNN currently only supports monomorphic FOL. % 111.60/16.79 % Exception at run slice level % 111.60/16.79 User error: GNN currently only supports monomorphic FOL. % 111.60/16.79 % Exception at run slice level % 111.60/16.79 User error: GNN currently only supports monomorphic FOL. % 111.60/16.79 % (374892)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=3910828498: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_2909 on theBenchmark for (2909ds/7222Mi) % 111.60/16.79 % (374892)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 111.60/16.79 % (374891)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=3433583508:i=20684:bd=all:gtg=exists_sym_2910 on theBenchmark for (2910ds/20684Mi) % 111.60/16.79 % (374893)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=1921108270:st=4:i=7295:sd=4:ep=R:ss=axioms_2909 on theBenchmark for (2909ds/7295Mi) % 111.60/16.79 % (374890)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=3396320156:i=33824:bd=preordered_2910 on theBenchmark for (2910ds/33824Mi) % 111.60/16.79 % Exception at run slice level % 111.60/16.79 User error: GNN currently only supports monomorphic FOL. % 111.60/16.79 % (374854)Instruction limit reached! % 111.60/16.79 % (374854)------------------------------ % 111.60/16.79 % (374854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.60/16.79 % (374854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.60/16.79 % (374854)CaDiCaL version: 2.1.3 % 111.60/16.79 % (374854)Termination reason: Instruction limit % 111.60/16.79 % (374854)Termination phase: Saturation % 111.60/16.79 % (374854)Time elapsed: 3.355 s % 111.60/16.79 % (374854)Peak memory usage: 118 MB % 111.60/16.79 % (374854)Instructions burned: 5470 (million) % 128.91/19.20 % (374898)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=2503941551:i=4036:ins=10_2899 on theBenchmark for (2899ds/4036Mi) % 128.91/19.20 % Exception at run slice level % 128.91/19.20 User error: GNN currently only supports monomorphic FOL. % 128.91/19.20 % Exception at run slice level % 128.91/19.20 User error: GNN currently only supports monomorphic FOL. % 128.91/19.20 % Exception at run slice level % 128.91/19.20 User error: GNN currently only supports monomorphic FOL. % 128.91/19.20 % (374899)lrs+10_1_sil=128000:lcm=predicate:random_seed=699943237:st=3:i=43697:sd=5:ss=axioms_2899 on theBenchmark for (2899ds/43697Mi) % 128.91/19.20 % Exception at run slice level % 128.91/19.20 User error: GNN currently only supports monomorphic FOL. % 128.91/19.20 % (374903)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=90727751:i=4547:bd=preordered_2897 on theBenchmark for (2897ds/4547Mi) % 128.91/19.20 % (374904)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=182833742:i=9294:av=off_2897 on theBenchmark for (2897ds/9294Mi) % 128.91/19.20 % (374902)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=1040394552:i=17599:gtg=all:ss=axioms:fsd=on_2897 on theBenchmark for (2897ds/17599Mi) % 128.91/19.20 % (374905)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3897043033:i=32849:add=on_2896 on theBenchmark for (2896ds/32849Mi) % 128.91/19.20 % Exception at run slice level % 128.91/19.20 User error: GNN currently only supports monomorphic FOL. % 128.91/19.20 % Exception at run slice level % 128.91/19.20 User error: GNN currently only supports monomorphic FOL. % 128.91/19.20 % Exception at run slice level % 128.91/19.20 User error: GNN currently only supports monomorphic FOL. % 128.91/19.20 % Exception at run slice level % 128.91/19.20 User error: GNN currently only supports monomorphic FOL. % 128.91/19.20 % (374910)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=954395989:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2892 on theBenchmark for (2892ds/4793Mi) % 128.91/19.20 % (374911)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=3158850419:i=4840:nm=4:av=off_2892 on theBenchmark for (2892ds/4840Mi) % 128.91/19.20 % (374913)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=2453039687:i=30479:sd=3:ss=axioms_2892 on theBenchmark for (2892ds/30479Mi) % 128.91/19.20 % (374912)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=4212325118:cts=off:i=5002_2892 on theBenchmark for (2892ds/5002Mi) % 128.91/19.20 % Exception at run slice level % 128.91/19.20 User error: GNN currently only supports monomorphic FOL. % 128.91/19.20 % (374918)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=2345053921:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2889 on theBenchmark for (2889ds/11035Mi) % 128.91/19.20 % (374918)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 128.91/19.20 % Exception at run slice level% Exception at run slice level % 128.91/19.20 % 128.91/19.20 User error: User error: GNN currently only supports monomorphic FOL.GNN currently only supports monomorphic FOL. % 128.91/19.20 % 128.91/19.20 % Exception at run slice level % 128.91/19.20 User error: GNN currently only supports monomorphic FOL. % 128.91/19.20 % Exception at run slice level % 128.91/19.20 User error: GNN currently only supports monomorphic FOL. % 128.91/19.20 % (374920)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=588439045:i=5835_2887 on theBenchmark for (2887ds/5835Mi) % 128.91/19.20 % (374921)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=1159726436:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2887 on theBenchmark for (2887ds/5890Mi) % 128.91/19.20 % (374922)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=1845408238:cts=off:i=19910:ep=RS_2887 on theBenchmark for (2887ds/19910Mi) % 128.91/19.20 % (374923)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=3278062433:i=20312:bd=preordered:fsr=off:er=filter_2886 on theBenchmark for (2886ds/20312Mi) % 163.84/24.07 % Exception at run slice level % 163.84/24.07 User error: GNN currently only supports monomorphic FOL. % 163.84/24.07 % Exception at run slice level % 163.84/24.07 User error: GNN currently only supports monomorphic FOL. % 163.84/24.07 % Exception at run slice level % 163.84/24.07 User error: GNN currently only supports monomorphic FOL. % 163.84/24.07 % (374928)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=78075777:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2883 on theBenchmark for (2883ds/13822Mi) % 163.84/24.07 % (374930)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=511875670:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2881 on theBenchmark for (2881ds/15184Mi) % 163.84/24.07 % (374929)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=3778636958:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2881 on theBenchmark for (2881ds/7144Mi) % 163.84/24.07 % Exception at run slice level % 163.84/24.07 User error: GNN currently only supports monomorphic FOL. % 163.84/24.07 % Exception at run slice level % 163.84/24.07 User error: GNN currently only supports monomorphic FOL. % 163.84/24.07 % (374934)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=3429273567:i=107375_2878 on theBenchmark for (2878ds/107375Mi) % 163.84/24.07 % (374935)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=1898193264:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2876 on theBenchmark for (2876ds/7958Mi) % 163.84/24.07 % Exception at run slice level % 163.84/24.07 User error: GNN currently only supports monomorphic FOL. % 163.84/24.07 % Exception at run slice level % 163.84/24.07 User error: GNN currently only supports monomorphic FOL. % 163.84/24.07 % (374938)dis+10_128_sil=16000:nwc=0.7:random_seed=4068859116:i=15999:nm=2:gsp=on_2872 on theBenchmark for (2872ds/15999Mi) % 163.84/24.07 % (374938)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 163.84/24.07 % (374939)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=284162998:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2871 on theBenchmark for (2871ds/8139Mi) % 163.84/24.07 % (374929)Instruction limit reached! % 163.84/24.07 % (374929)------------------------------ % 163.84/24.07 % (374929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.84/24.07 % (374929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.84/24.07 % (374929)CaDiCaL version: 2.1.3 % 163.84/24.07 % (374929)Termination reason: Instruction limit % 163.84/24.07 % (374929)Termination phase: Saturation % 163.84/24.07 % (374929)Time elapsed: 3.565 s % 163.84/24.07 % (374929)Peak memory usage: 124 MB % 163.84/24.07 % (374929)Instructions burned: 7144 (million) % 163.84/24.07 % (375301)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=3303148158:st=4:i=8950:sd=5:ss=axioms_2844 on theBenchmark for (2844ds/8950Mi) % 163.84/24.07 % Exception at run slice level % 163.84/24.07 User error: GNN currently only supports monomorphic FOL. % 163.84/24.07 % (374922)Instruction limit reached! % 163.84/24.07 % (374922)------------------------------ % 163.84/24.07 % (374922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.84/24.07 % (374922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.84/24.07 % (374922)CaDiCaL version: 2.1.3 % 163.84/24.07 % (374922)Termination reason: Instruction limit % 163.84/24.07 % (374922)Termination phase: Saturation % 163.84/24.07 % (374922)Time elapsed: 4.753 s % 163.84/24.07 % (374922)Peak memory usage: 111 MB % 163.84/24.07 % (374922)Instructions burned: 19912 (million) % 163.84/24.07 % (375303)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=3884894839:i=9809:ins=10:av=off_2839 on theBenchmark for (2839ds/9809Mi) % 163.84/24.07 % (375304)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=3801390278:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2837 on theBenchmark for (2837ds/9885Mi) % 181.46/26.61 % Exception at run slice level % 181.46/26.61 User error: GNN currently only supports monomorphic FOL. % 181.46/26.61 % Exception at run slice level % 181.46/26.61 User error: GNN currently only supports monomorphic FOL. % 181.46/26.61 % (375307)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=792724673:cond=fast:i=32078:fgj=on:av=off_2834 on theBenchmark for (2834ds/32078Mi) % 181.46/26.61 % (375308)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=3794228724:i=11101:bd=all:ss=axioms:sgt=8_2834 on theBenchmark for (2834ds/11101Mi) % 181.46/26.61 % Exception at run slice level % 181.46/26.61 User error: GNN currently only supports monomorphic FOL. % 181.46/26.61 % (375311)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=380655096:cond=on:i=13220:s2at=3:aac=none:fsd=on_2831 on theBenchmark for (2831ds/13220Mi) % 181.46/26.61 % Exception at run slice level % 181.46/26.61 User error: GNN currently only supports monomorphic FOL. % 181.46/26.61 % (375313)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=33337236:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2828 on theBenchmark for (2828ds/13528Mi) % 181.46/26.61 % (374939)Instruction limit reached! % 181.46/26.61 % (374939)------------------------------ % 181.46/26.61 % (374939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.46/26.61 % (374939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.46/26.61 % (374939)CaDiCaL version: 2.1.3 % 181.46/26.61 % (374939)Termination reason: Instruction limit % 181.46/26.61 % (374939)Termination phase: Saturation % 181.46/26.61 % (374939)Time elapsed: 4.448 s % 181.46/26.61 % (374939)Peak memory usage: 134 MB % 181.46/26.61 % (374939)Instructions burned: 8140 (million) % 181.46/26.61 % Exception at run slice level % 181.46/26.61 User error: GNN currently only supports monomorphic FOL. % 181.46/26.61 % (375315)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=1834986667:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2825 on theBenchmark for (2825ds/14854Mi) % 181.46/26.61 % (375316)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=2136818664:i=14974:ss=axioms:sgt=16_2824 on theBenchmark for (2824ds/14974Mi) % 181.46/26.61 % Exception at run slice level % 181.46/26.61 User error: GNN currently only supports monomorphic FOL. % 181.46/26.61 % (375319)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=676450316:i=33081:aac=none:fgj=on:bd=all:fsr=off_2821 on theBenchmark for (2821ds/33081Mi) % 181.46/26.61 % Exception at run slice level % 181.46/26.61 User error: GNN currently only supports monomorphic FOL. % 181.46/26.61 % Exception at run slice level % 181.46/26.61 User error: GNN currently only supports monomorphic FOL. % 181.46/26.61 % (375321)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=3061682976:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2819 on theBenchmark for (2819ds/50856Mi) % 181.46/26.61 % (375322)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=3088385601:i=69865_2818 on theBenchmark for (2818ds/69865Mi) % 181.46/26.61 % Exception at run slice level % 181.46/26.61 User error: GNN currently only supports monomorphic FOL. % 181.46/26.61 % Exception at run slice level % 181.46/26.61 User error: GNN currently only supports monomorphic FOL. % 181.46/26.61 % (375325)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=3046647631:cond=fast:i=17802:gtgl=3:gtg=all_2815 on theBenchmark for (2815ds/17802Mi) % 181.46/26.61 % Exception at run slice level % 181.46/26.61 User error: Immediate (shared) subterms of term/literal list_case(X1,X0,X3,X2,nil(X0)) = sF13(X1,X0,X3,X2) have different types/not well-typed! % 181.46/26.61 % (375326)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=3131847815:i=96644_2814 on theBenchmark for (2814ds/96644Mi) % 181.46/26.61 % (375328)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 191.22/27.95 % (375328)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=3694674751:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2813 on theBenchmark for (2813ds/21161Mi) % 191.22/27.95 % (374831)Instruction limit reached! % 191.22/27.95 % (374831)------------------------------ % 191.22/27.95 % (374831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.22/27.95 % (374831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.22/27.95 % (374831)CaDiCaL version: 2.1.3 % 191.22/27.95 % (374831)Termination reason: Instruction limit % 191.22/27.95 % (374831)Termination phase: Saturation % 191.22/27.95 % (374831)Time elapsed: 13.787 s % 191.22/27.95 % (374831)Peak memory usage: 298 MB % 191.22/27.95 % (374831)Instructions burned: 26474 (million) % 191.22/27.95 % (375331)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=3425012732:i=22761:gtg=all:ss=axioms:fsd=on_2807 on theBenchmark for (2807ds/22761Mi) % 191.22/27.95 % Exception at run slice level % 191.22/27.95 User error: GNN currently only supports monomorphic FOL. % 191.22/27.95 % (375333)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=3850475878:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2802 on theBenchmark for (2802ds/23713Mi) % 191.22/27.95 % (374938)Instruction limit reached! % 191.22/27.95 % (374938)------------------------------ % 191.22/27.95 % (374938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.22/27.95 % (374938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.22/27.95 % (374938)CaDiCaL version: 2.1.3 % 191.22/27.95 % (374938)Termination reason: Instruction limit % 191.22/27.95 % (374938)Termination phase: Saturation % 191.22/27.95 % (374938)Time elapsed: 8.297 s % 191.22/27.95 % (374938)Peak memory usage: 157 MB % 191.22/27.95 % (374938)Instructions burned: 16001 (million) % 191.22/27.95 % (375335)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=1590700670:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2788 on theBenchmark for (2788ds/26509Mi) % 191.22/27.95 % Exception at run slice level % 191.22/27.95 User error: GNN currently only supports monomorphic FOL. % 191.22/27.95 % (375337)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=3652059934:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2782 on theBenchmark for (2782ds/28957Mi) % 191.22/27.95 % (375308)Instruction limit reached! % 191.22/27.95 % (375308)------------------------------ % 191.22/27.95 % (375308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.22/27.95 % (375308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.22/27.95 % (375308)CaDiCaL version: 2.1.3 % 191.22/27.95 % (375308)Termination reason: Instruction limit % 191.22/27.95 % (375308)Termination phase: Saturation % 191.22/27.95 % (375308)Time elapsed: 6.252 s % 191.22/27.95 % (375308)Peak memory usage: 136 MB % 191.22/27.95 % (375308)Instructions burned: 11102 (million) % 191.22/27.95 % (375339)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=1550234876:i=29246:s2at=-1:kws=inv_arity:ins=10_2769 on theBenchmark for (2769ds/29246Mi) % 191.22/27.95 % (374806)Instruction limit reached! % 191.22/27.95 % (374806)------------------------------ % 191.22/27.95 % (374806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.22/27.95 % (374806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.22/27.95 % (374806)CaDiCaL version: 2.1.3 % 191.22/27.95 % (374806)Termination reason: Instruction limit % 191.22/27.95 % (374806)Termination phase: Saturation % 191.22/27.95 % (374806)Time elapsed: 19.471 s % 191.22/27.95 % (374806)Peak memory usage: 241 MB % 191.22/27.95 % (374806)Instructions burned: 33335 (million) % 191.22/27.95 % Exception at run slice level % 191.22/27.95 User error: GNN currently only supports monomorphic FOL. % 191.22/27.95 % (375341)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=4263904514:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2765 on theBenchmark for (2765ds/30082Mi) % 191.22/27.95 % (375341)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 198.05/28.92 % (375342)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=481503605:i=32262:bd=preordered_2764 on theBenchmark for (2764ds/32262Mi) % 198.05/28.92 % Exception at run slice level % 198.05/28.92 User error: GNN currently only supports monomorphic FOL. % 198.05/28.92 % Exception at run slice level % 198.05/28.92 User error: GNN currently only supports monomorphic FOL. % 198.05/28.92 % (375345)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=1033466795:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2760 on theBenchmark for (2760ds/32870Mi) % 198.05/28.92 % (375346)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=3724991878:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2759 on theBenchmark for (2759ds/33295Mi) % 198.05/28.92 % Exception at run slice level % 198.05/28.92 User error: GNN currently only supports monomorphic FOL. % 198.05/28.92 % Exception at run slice level % 198.05/28.92 User error: GNN currently only supports monomorphic FOL. % 198.05/28.92 % (375349)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=2600023145:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2754 on theBenchmark for (2754ds/36826Mi) % 198.05/28.92 % (375350)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=180453322:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2754 on theBenchmark for (2754ds/92981Mi) % 198.05/28.92 % (375328)Instruction limit reached! % 198.05/28.92 % (375328)------------------------------ % 198.05/28.92 % (375328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 198.05/28.92 % (375328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.05/28.92 % (375328)CaDiCaL version: 2.1.3 % 198.05/28.92 % (375328)Termination reason: Instruction limit % 198.05/28.92 % (375328)Termination phase: Saturation % 198.05/28.92 % (375328)Time elapsed: 6.271 s % 198.05/28.92 % (375328)Peak memory usage: 219 MB % 198.05/28.92 % (375328)Instructions burned: 21164 (million) % 198.05/28.92 % Exception at run slice level % 198.05/28.92 User error: GNN currently only supports monomorphic FOL. % 198.05/28.92 % (375353)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=1743381166:s2pl=on:i=49423_2749 on theBenchmark for (2749ds/49423Mi) % 198.05/28.92 % (375354)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=2310708952:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2748 on theBenchmark for (2748ds/57299Mi) % 198.05/28.92 % Exception at run slice level % 198.05/28.92 User error: GNN currently only supports monomorphic FOL. % 198.05/28.92 % (375357)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=3400486885:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2746 on theBenchmark for (2746ds/127679Mi) % 198.05/28.92 % Exception at run slice level % 198.05/28.92 User error: GNN currently only supports monomorphic FOL. % 198.05/28.92 % Exception at run slice level % 198.05/28.92 User error: GNN currently only supports monomorphic FOL. % 198.05/28.92 % (375359)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=1819932248:i=69402:add=on:aac=none:fsr=off_2743 on theBenchmark for (2743ds/69402Mi) % 198.05/28.92 % (375360)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=1229984703:i=100512:doe=on:fgj=on:bd=all:fsd=on_2743 on theBenchmark for (2743ds/100512Mi) % 198.05/28.92 % Exception at run slice level % 198.05/28.92 User error: GNN currently only supports monomorphic FOL. % 198.05/28.92 % (375363)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=3054194208:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2739 on theBenchmark for (2739ds/138761Mi) % 198.05/28.92 % Exception at run slice level % 198.05/28.92 User error: GNN currently only supports monomorphic FOL. % 209.46/30.56 % (375365)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=2507144800:i=282386:rtra=on_2738 on theBenchmark for (2738ds/282386Mi) % 209.46/30.56 % Exception at run slice level % 209.46/30.56 User error: GNN currently only supports monomorphic FOL. % 209.46/30.56 % (375367)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=2945952992:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2736 on theBenchmark for (2736ds/269354Mi) % 209.46/30.56 % Exception at run slice level % 209.46/30.56 User error: GNN currently only supports monomorphic FOL. % 209.46/30.56 % Exception at run slice level % 209.46/30.56 User error: GNN currently only supports monomorphic FOL. % 209.46/30.56 % (375369)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=1263523232:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2733 on theBenchmark for (2733ds/283390Mi) % 209.46/30.56 % (375369)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 209.46/30.56 % (375370)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=2341723040:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2733 on theBenchmark for (2733ds/218Mi) % 209.46/30.56 % (375370)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 209.46/30.56 % (375370)Refutation not found, incomplete strategy % 209.46/30.56 % (375370)------------------------------ % 209.46/30.56 % (375370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.46/30.56 % (375370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.46/30.56 % (375370)CaDiCaL version: 2.1.3 % 209.46/30.56 % (375370)Termination reason: Refutation not found, incomplete strategy % 209.46/30.56 % (375370)Time elapsed: 0.002 s % 209.46/30.56 % (375370)Peak memory usage: 88 MB % 209.46/30.56 % (375370)Instructions burned: 1 (million) % 209.46/30.56 % Exception at run slice level % 209.46/30.56 User error: GNN currently only supports monomorphic FOL. % 209.46/30.56 % (375370)------------------------------ % 209.46/30.56 % (375370)------------------------------ % 209.46/30.56 % (375373)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=1455314768:i=238:av=off:rtra=on:ss=axioms_2730 on theBenchmark for (2730ds/238Mi) % 209.46/30.56 % (375373)Instruction limit reached! % 209.46/30.56 % (375373)------------------------------ % 209.46/30.56 % (375373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.46/30.56 % (375373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.46/30.56 % (375373)CaDiCaL version: 2.1.3 % 209.46/30.56 % (375373)Termination reason: Instruction limit % 209.46/30.56 % (375373)Termination phase: Saturation % 209.46/30.56 % (375373)Time elapsed: 0.071 s % 209.46/30.56 % (375373)Peak memory usage: 89 MB % 209.46/30.56 % (375373)Instructions burned: 240 (million) % 209.46/30.56 % (375374)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=373699931:s2a=on:i=278:rtra=on:gtg=position_2729 on theBenchmark for (2729ds/278Mi) % 209.46/30.56 % (375376)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=2448325641:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2728 on theBenchmark for (2728ds/258Mi) % 209.46/30.56 % (375376)Instruction limit reached! % 209.46/30.56 % (375376)------------------------------ % 209.46/30.56 % (375376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.46/30.56 % (375376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.46/30.56 % (375376)CaDiCaL version: 2.1.3 % 209.46/30.56 % (375376)Termination reason: Instruction limit % 209.46/30.56 % (375376)Termination phase: Saturation % 209.46/30.56 % (375376)Time elapsed: 0.075 s % 209.46/30.56 % (375376)Peak memory usage: 90 MB % 209.46/30.56 % (375376)Instructions burned: 260 (million) % 209.46/30.56 % (375374)Instruction limit reached! % 209.46/30.56 % (375374)------------------------------ % 209.46/30.56 % (375374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.46/30.56 % (375374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.46/30.56 % (375374)CaDiCaL version: 2.1.3 % 209.46/30.56 % (375374)Termination reason: Instruction limit % 209.46/30.56 % (375374)Termination phase: Saturation % 209.46/30.56 % (375374)Time elapsed: 0.165 s % 209.46/30.56 % (375374)Peak memory usage: 91 MB % 209.46/30.56 % (375374)Instructions burned: 278 (million) % 209.46/30.56 % (375379)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=1908810213:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2726 on theBenchmark for (2726ds/570Mi) % 220.67/32.12 % (375380)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=1202409734:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2725 on theBenchmark for (2725ds/314Mi) % 220.67/32.12 % (375380)Refutation not found, incomplete strategy % 220.67/32.12 % (375380)------------------------------ % 220.67/32.12 % (375380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.67/32.12 % (375380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.67/32.12 % (375380)CaDiCaL version: 2.1.3 % 220.67/32.12 % (375380)Termination reason: Refutation not found, incomplete strategy % 220.67/32.12 % (375380)Time elapsed: 0.003 s % 220.67/32.12 % (375380)Peak memory usage: 88 MB % 220.67/32.12 % (375380)Instructions burned: 4 (million) % 220.67/32.12 % (375379)Instruction limit reached! % 220.67/32.12 % (375379)------------------------------ % 220.67/32.12 % (375379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.67/32.12 % (375379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.67/32.12 % (375379)CaDiCaL version: 2.1.3 % 220.67/32.12 % (375379)Termination reason: Instruction limit % 220.67/32.12 % (375379)Termination phase: Saturation % 220.67/32.12 % (375379)Time elapsed: 0.184 s % 220.67/32.12 % (375379)Peak memory usage: 92 MB % 220.67/32.12 % (375379)Instructions burned: 571 (million) % 220.67/32.12 % (375383)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=1861966032:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2723 on theBenchmark for (2723ds/650Mi) % 220.67/32.12 % (375380)------------------------------ % 220.67/32.12 % (375380)------------------------------ % 220.67/32.12 % (375385)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=171363301:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2721 on theBenchmark for (2721ds/496Mi) % 220.67/32.12 % (375383)Instruction limit reached! % 220.67/32.12 % (375383)------------------------------ % 220.67/32.12 % (375383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.67/32.12 % (375383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.67/32.12 % (375383)CaDiCaL version: 2.1.3 % 220.67/32.12 % (375383)Termination reason: Instruction limit % 220.67/32.12 % (375383)Termination phase: Saturation % 220.67/32.12 % (375383)Time elapsed: 0.187 s % 220.67/32.12 % (375383)Peak memory usage: 91 MB % 220.67/32.12 % (375383)Instructions burned: 652 (million) % 220.67/32.12 % (375387)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=1443919466:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2719 on theBenchmark for (2719ds/588Mi) % 220.67/32.12 % (375387)Refutation not found, incomplete strategy % 220.67/32.12 % (375387)------------------------------ % 220.67/32.12 % (375387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.67/32.12 % (375387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.67/32.12 % (375387)CaDiCaL version: 2.1.3 % 220.67/32.12 % (375387)Termination reason: Refutation not found, incomplete strategy % 220.67/32.12 % (375387)Time elapsed: 0.004 s % 220.67/32.12 % (375387)Peak memory usage: 88 MB % 220.67/32.12 % (375387)Instructions burned: 10 (million) % 220.67/32.12 % (375385)Instruction limit reached! % 220.67/32.12 % (375385)------------------------------ % 220.67/32.12 % (375385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.67/32.12 % (375385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.67/32.12 % (375385)CaDiCaL version: 2.1.3 % 220.67/32.12 % (375385)Termination reason: Instruction limit % 220.67/32.12 % (375385)Termination phase: Saturation % 220.67/32.12 % (375385)Time elapsed: 0.267 s % 220.67/32.12 % (375385)Peak memory usage: 91 MB % 220.67/32.12 % (375385)Instructions burned: 496 (million) % 220.67/32.12 % (375387)------------------------------ % 220.67/32.12 % (375387)------------------------------ % 220.67/32.12 % (375390)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=687051666:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2717 on theBenchmark for (2717ds/226Mi) % 220.67/32.12 % (375389)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=1111431886:i=4700:rtra=on_2717 on theBenchmark for (2717ds/4700Mi) % 220.67/32.12 % (375390)Instruction limit reached! % 220.67/32.12 % (375390)------------------------------ % 220.67/32.12 % (375390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.67/32.12 % (375390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.94/34.00 % (375390)CaDiCaL version: 2.1.3 % 232.94/34.00 % (375390)Termination reason: Instruction limit % 232.94/34.00 % (375390)Termination phase: Saturation % 232.94/34.00 % (375390)Time elapsed: 0.071 s % 232.94/34.00 % (375390)Peak memory usage: 90 MB % 232.94/34.00 % (375390)Instructions burned: 230 (million) % 232.94/34.00 % (375393)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1881213620:i=254:av=off:fsr=off:rtra=on:sup=off_2715 on theBenchmark for (2715ds/254Mi) % 232.94/34.00 % (375393)Refutation not found, incomplete strategy % 232.94/34.00 % (375393)------------------------------ % 232.94/34.00 % (375393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.94/34.00 % (375393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.94/34.00 % (375393)CaDiCaL version: 2.1.3 % 232.94/34.00 % (375393)Termination reason: Refutation not found, incomplete strategy % 232.94/34.00 % (375393)Time elapsed: 0.004 s % 232.94/34.00 % (375393)Peak memory usage: 88 MB % 232.94/34.00 % (375393)Instructions burned: 11 (million) % 232.94/34.00 % (375393)------------------------------ % 232.94/34.00 % (375393)------------------------------ % 232.94/34.00 % Exception at run slice level % 232.94/34.00 User error: GNN currently only supports monomorphic FOL. % 232.94/34.00 % (375414)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=847990660:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2712 on theBenchmark for (2712ds/228Mi) % 232.94/34.00 % (375416)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=612772664:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2712 on theBenchmark for (2712ds/1814Mi) % 232.94/34.00 % (375414)Instruction limit reached! % 232.94/34.00 % (375414)------------------------------ % 232.94/34.00 % (375414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.94/34.00 % (375414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.94/34.00 % (375414)CaDiCaL version: 2.1.3 % 232.94/34.00 % (375414)Termination reason: Instruction limit % 232.94/34.00 % (375414)Termination phase: Saturation % 232.94/34.00 % (375414)Time elapsed: 0.066 s % 232.94/34.00 % (375414)Peak memory usage: 89 MB % 232.94/34.00 % (375414)Instructions burned: 229 (million) % 232.94/34.00 % (375474)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=216016532:i=874:sd=1:aac=none:rtra=on:ss=included_2710 on theBenchmark for (2710ds/874Mi) % 232.94/34.00 % (375474)Refutation not found, incomplete strategy % 232.94/34.00 % (375474)------------------------------ % 232.94/34.00 % (375474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.94/34.00 % (375474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.94/34.00 % (375474)CaDiCaL version: 2.1.3 % 232.94/34.00 % (375474)Termination reason: Refutation not found, incomplete strategy % 232.94/34.00 % (375474)Time elapsed: 0.005 s % 232.94/34.00 % (375474)Peak memory usage: 89 MB % 232.94/34.00 % (375474)Instructions burned: 14 (million) % 232.94/34.00 % (375474)------------------------------ % 232.94/34.00 % (375474)------------------------------ % 232.94/34.00 % (375533)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=4286731119:i=10404:rtra=on:ss=axioms:sgt=16_2707 on theBenchmark for (2707ds/10404Mi) % 232.94/34.00 % Exception at run slice level % 232.94/34.00 User error: GNN currently only supports monomorphic FOL. % 232.94/34.00 % (375563)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1056462051:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2704 on theBenchmark for (2704ds/268Mi) % 232.94/34.00 % (375563)Instruction limit reached! % 232.94/34.00 % (375563)------------------------------ % 232.94/34.00 % (375563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.94/34.00 % (375563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.94/34.00 % (375563)CaDiCaL version: 2.1.3 % 232.94/34.00 % (375563)Termination reason: Instruction limit % 232.94/34.00 % (375563)Termination phase: Saturation % 232.94/34.00 % (375563)Time elapsed: 0.093 s % 232.94/34.00 % (375563)Peak memory usage: 91 MB % 232.94/34.00 % (375563)Instructions burned: 270 (million) % 232.94/34.00 % (375636)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=1749582823:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2702 on theBenchmark for (2702ds/1184Mi) % 232.94/34.00 % (375416)Instruction limit reached! % 232.94/34.00 % (375416)------------------------------ % 232.94/34.00 % (375416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.94/34.00 % (375416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.70/37.31 % (375416)CaDiCaL version: 2.1.3 % 240.70/37.31 % (375416)Termination reason: Instruction limit % 240.70/37.31 % (375416)Termination phase: Saturation % 240.70/37.31 % (375416)Time elapsed: 1.185 s % 240.70/37.31 % (375416)Peak memory usage: 102 MB % 240.70/37.31 % (375416)Instructions burned: 1814 (million) % 240.70/37.31 % (375693)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=3363448965:st=3:i=26386:sd=3:rtra=on:ss=axioms_2698 on theBenchmark for (2698ds/26386Mi) % 240.70/37.31 % (375636)Instruction limit reached! % 240.70/37.31 % (375636)------------------------------ % 240.70/37.31 % (375636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.70/37.31 % (375636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.70/37.31 % (375636)CaDiCaL version: 2.1.3 % 240.70/37.31 % (375636)Termination reason: Instruction limit % 240.70/37.31 % (375636)Termination phase: Saturation % 240.70/37.31 % (375636)Time elapsed: 0.543 s % 240.70/37.31 % (375636)Peak memory usage: 95 MB % 240.70/37.31 % (375636)Instructions burned: 1184 (million) % 240.70/37.31 % (375710)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=1535814641:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2695 on theBenchmark for (2695ds/250Mi) % 240.70/37.31 % (375710)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 240.70/37.31 % (375710)Instruction limit reached! % 240.70/37.31 % (375710)------------------------------ % 240.70/37.31 % (375710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.70/37.31 % (375710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.70/37.31 % (375710)CaDiCaL version: 2.1.3 % 240.70/37.31 % (375710)Termination reason: Instruction limit % 240.70/37.31 % (375710)Termination phase: Saturation % 240.70/37.31 % (375710)Time elapsed: 0.148 s % 240.70/37.31 % (375710)Peak memory usage: 91 MB % 240.70/37.31 % (375710)Instructions burned: 251 (million) % 240.70/37.31 % (375715)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=2462086593:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2692 on theBenchmark for (2692ds/268Mi) % 240.70/37.31 % Exception at run slice level % 240.70/37.31 User error: Immediate (shared) subterms of term/literal list_rec(X1,X0,X3,X4,cons(X0,X2,X5)) = sF16(X1,X0,X3,X4,X2,X5) have different types/not well-typed! % 240.70/37.31 % Exception at run slice level % 240.70/37.31 User error: GNN currently only supports monomorphic FOL. % 240.70/37.31 % (375724)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=238762047:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2690 on theBenchmark for (2690ds/282Mi) % 240.70/37.31 % (375724)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 240.70/37.31 % (375724)Refutation not found, incomplete strategy % 240.70/37.31 % (375724)------------------------------ % 240.70/37.31 % (375724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.70/37.31 % (375724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.70/37.31 % (375724)CaDiCaL version: 2.1.3 % 240.70/37.31 % (375724)Termination reason: Refutation not found, incomplete strategy % 240.70/37.31 % (375724)Time elapsed: 0.001 s % 240.70/37.31 % (375724)Peak memory usage: 88 MB % 240.70/37.31 % (375724)Instructions burned: 1 (million) % 240.70/37.31 % (375726)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=127963152:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2690 on theBenchmark for (2690ds/862Mi) % 240.70/37.31 % (375726)Refutation not found, incomplete strategy % 240.70/37.31 % (375726)------------------------------ % 240.70/37.31 % (375726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.70/37.31 % (375726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.70/37.31 % (375726)CaDiCaL version: 2.1.3 % 240.70/37.31 % (375726)Termination reason: Refutation not found, incomplete strategy % 240.70/37.31 % (375726)Time elapsed: 0.005 s % 240.70/37.31 % (375726)Peak memory usage: 88 MB % 240.70/37.31 % (375726)Instructions burned: 3 (million) % 240.70/37.31 % (375724)------------------------------ % 240.70/37.31 % (375724)------------------------------ % 240.70/37.31 % (375735)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=1872285487:i=12120:aac=none:ins=25:rtra=on_2685 on theBenchmark for (2685ds/12120Mi) % 272.84/39.41 % (375726)------------------------------ % 272.84/39.41 % (375726)------------------------------ % 272.84/39.41 % Exception at run slice level % 272.84/39.41 User error: GNN currently only supports monomorphic FOL. % 272.84/39.41 % (375737)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=1673349141:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2683 on theBenchmark for (2683ds/300Mi) % 272.84/39.41 % (375737)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 272.84/39.41 % (375740)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=43137856:i=28310:bd=all:rtra=on_2680 on theBenchmark for (2680ds/28310Mi) % 272.84/39.41 % (375737)Instruction limit reached! % 272.84/39.41 % (375737)------------------------------ % 272.84/39.41 % (375737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.84/39.41 % (375737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.84/39.41 % (375737)CaDiCaL version: 2.1.3 % 272.84/39.41 % (375737)Termination reason: Instruction limit % 272.84/39.41 % (375737)Termination phase: Saturation % 272.84/39.41 % (375737)Time elapsed: 0.284 s % 272.84/39.41 % (375737)Peak memory usage: 91 MB % 272.84/39.41 % (375737)Instructions burned: 301 (million) % 272.84/39.41 % Exception at run slice level % 272.84/39.41 User error: GNN currently only supports monomorphic FOL. % 272.84/39.41 % (375744)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2786477959:i=1334:av=off:fsr=off:rtra=on_2677 on theBenchmark for (2677ds/1334Mi) % 272.84/39.41 % (375744)Refutation not found, incomplete strategy % 272.84/39.41 % (375744)------------------------------ % 272.84/39.41 % (375744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.84/39.41 % (375744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.84/39.41 % (375744)CaDiCaL version: 2.1.3 % 272.84/39.41 % (375744)Termination reason: Refutation not found, incomplete strategy % 272.84/39.41 % (375744)Time elapsed: 0.015 s % 272.84/39.41 % (375744)Peak memory usage: 88 MB % 272.84/39.41 % (375744)Instructions burned: 13 (million) % 272.84/39.41 % (375746)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=1752138537:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2674 on theBenchmark for (2674ds/370Mi) % 272.84/39.41 % (375746)Instruction limit reached! % 272.84/39.41 % (375746)------------------------------ % 272.84/39.41 % (375746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.84/39.41 % (375746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.84/39.41 % (375746)CaDiCaL version: 2.1.3 % 272.84/39.41 % (375746)Termination reason: Instruction limit % 272.84/39.41 % (375746)Termination phase: Saturation % 272.84/39.41 % (375746)Time elapsed: 0.183 s % 272.84/39.41 % (375746)Peak memory usage: 92 MB % 272.84/39.41 % (375746)Instructions burned: 370 (million) % 272.84/39.41 % (375744)------------------------------ % 272.84/39.41 % (375744)------------------------------ % 272.84/39.41 % (375753)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=1624160645:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2670 on theBenchmark for (2670ds/386Mi) % 272.84/39.41 % (375754)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=1992462311:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2669 on theBenchmark for (2669ds/9700Mi) % 272.84/39.41 % (375754)Refutation not found, incomplete strategy % 272.84/39.41 % (375754)------------------------------ % 272.84/39.41 % (375754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.84/39.41 % (375754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.84/39.41 % (375754)CaDiCaL version: 2.1.3 % 272.84/39.41 % (375754)Termination reason: Refutation not found, incomplete strategy % 272.84/39.41 % (375754)Time elapsed: 0.007 s % 272.84/39.41 % (375754)Peak memory usage: 88 MB % 272.84/39.41 % (375754)Instructions burned: 12 (million) % 272.84/39.41 % (375754)------------------------------ % 272.84/39.41 % (375754)------------------------------ % 272.84/39.41 % (375753)Instruction limit reached! % 272.84/39.41 % (375753)------------------------------ % 272.84/39.41 % (375753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.84/39.41 % (375753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.73/43.11 % (375753)CaDiCaL version: 2.1.3 % 298.73/43.11 % (375753)Termination reason: Instruction limit % 298.73/43.11 % (375753)Termination phase: Saturation % 298.73/43.11 % (375753)Time elapsed: 0.360 s % 298.73/43.11 % (375753)Peak memory usage: 91 MB % 298.73/43.11 % (375753)Instructions burned: 386 (million) % 298.73/43.11 % (375757)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=1487509817:i=24222:sd=1:rtra=on:ss=included_2665 on theBenchmark for (2665ds/24222Mi) % 298.73/43.11 % (375758)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=1005101298:i=638:kws=precedence:fsr=off:rtra=on_2664 on theBenchmark for (2664ds/638Mi) % 298.73/43.11 % Exception at run slice level % 298.73/43.11 User error: GNN currently only supports monomorphic FOL. % 298.73/43.11 % (375761)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2957480640:i=4128:ep=RST:rtra=on_2659 on theBenchmark for (2659ds/4128Mi) % 298.73/43.11 % (375758)Instruction limit reached! % 298.73/43.11 % (375758)------------------------------ % 298.73/43.11 % (375758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 298.73/43.11 % (375758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.73/43.11 % (375758)CaDiCaL version: 2.1.3 % 298.73/43.11 % (375758)Termination reason: Instruction limit % 298.73/43.11 % (375758)Termination phase: Saturation % 298.73/43.11 % (375758)Time elapsed: 0.572 s % 298.73/43.11 % (375758)Peak memory usage: 93 MB % 298.73/43.11 % (375758)Instructions burned: 638 (million) % 298.73/43.11 % (375765)dis-1011_128_sil=32000:si=on:random_seed=3271943194:i=7412:ep=RST:av=off:rtra=on_2655 on theBenchmark for (2655ds/7412Mi) % 298.73/43.11 % (374899)Instruction limit reached! % 298.73/43.11 % (374899)------------------------------ % 298.73/43.11 % (374899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 298.73/43.11 % (374899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.73/43.11 % (374899)CaDiCaL version: 2.1.3 % 298.73/43.11 % (374899)Termination reason: Instruction limit % 298.73/43.11 % (374899)Termination phase: Saturation % 298.73/43.11 % (374899)Time elapsed: 25.881 s % 298.73/43.11 % (374899)Peak memory usage: 207 MB % 298.73/43.11 % (374899)Instructions burned: 43697 (million) % 298.73/43.11 % (375761)Instruction limit reached! % 298.73/43.11 % (375761)------------------------------ % 298.73/43.11 % (375761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 298.73/43.11 % (375761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.73/43.11 % (375761)CaDiCaL version: 2.1.3 % 298.73/43.11 % (375761)Termination reason: Instruction limit % 298.73/43.11 % (375761)Termination phase: Saturation % 298.73/43.11 % (375761)Time elapsed: 2.086 s % 298.73/43.11 % (375761)Peak memory usage: 106 MB % 298.73/43.11 % (375761)Instructions burned: 4129 (million) % 298.73/43.11 % (375781)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1817218813:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2638 on theBenchmark for (2638ds/1514Mi) % 298.73/43.11 % (375781)Refutation not found, incomplete strategy % 298.73/43.11 % (375781)------------------------------ % 298.73/43.11 % (375781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 298.73/43.11 % (375781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.73/43.11 % (375781)CaDiCaL version: 2.1.3 % 298.73/43.11 % (375781)Termination reason: Refutation not found, incomplete strategy % 298.73/43.11 % (375781)Time elapsed: 0.014 s % 298.73/43.11 % (375781)Peak memory usage: 88 MB % 298.73/43.11 % (375781)Instructions burned: 12 (million) % 298.73/43.11 % (375782)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=112228193:i=27826:rtra=on:ss=axioms:sgt=8_2636 on theBenchmark for (2636ds/27826Mi) % 298.73/43.11 % (375333)Instruction limit reached! % 298.73/43.11 % (375333)------------------------------ % 298.73/43.11 % (375333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 298.73/43.11 % (375333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.73/43.11 % (375333)CaDiCaL version: 2.1.3 % 298.73/43.11 % (375333)Termination reason: Instruction limit % 298.73/43.11 % (375333)Termination phase: Saturation % 298.73/43.11 % (375333)Time elapsed: 16.867 s % 298.73/43.11 % (375333)Peak memory usage: 250 MB % 298.73/43.11 % (375333)Instructions burned: 23713 (million) % 298.73/43.11 % (375781)------------------------------ % 298.73/43.11 % (375781)--------------Terminated %------------------------------------------------------------------------------