%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW555_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 : n006.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:48 PM UTC 2026 % Result : Timeout 295.79s 42.73s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW555_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.26 % Computer : n006.cluster.edu % 0.10/0.26 % Model : x86_64 x86_64 % 0.10/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.26 % Memory : 8046.5625MB % 0.10/0.26 % OS : Linux 6.8.0-71-generic % 0.10/0.26 % CPULimit : 300 % 0.10/0.26 % WCLimit : 300 % 0.10/0.26 % DateTime : Mon Sep 28 14:18:55 UTC 2026 % 0.10/0.26 % CPUTime : % 0.10/0.26 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.25/0.31 Running first-order theorem proving % 0.25/0.31 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 % 10.17/2.39 % (3994751)Detected formulas, will run a generic FOF schedule. % 10.17/2.39 % (3994758)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=2310712445:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 10.17/2.39 % (3994763)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1194001761:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 10.17/2.39 % (3994759)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=3932028329:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 10.17/2.39 % (3994764)dis-21_1_sil=8000:lcm=predicate:random_seed=1149946373: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) % 10.17/2.39 % (3994761)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4013532322:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 10.17/2.39 % (3994762)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=885989597:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 10.17/2.39 % (3994761)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.17/2.39 % (3994761)Refutation not found, incomplete strategy % 10.17/2.39 % (3994761)------------------------------ % 10.17/2.39 % (3994761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.17/2.39 % (3994761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.17/2.39 % (3994761)CaDiCaL version: 2.1.3 % 10.17/2.39 % (3994761)Termination reason: Refutation not found, incomplete strategy % 10.17/2.39 % (3994761)Time elapsed: 0.004 s % 10.17/2.39 % (3994761)Peak memory usage: 88 MB % 10.17/2.39 % (3994761)Instructions burned: 3 (million) % 10.17/2.39 % (3994760)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=2375756953:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 10.17/2.39 % (3994760)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.17/2.39 % (3994762)Instruction limit reached! % 10.17/2.39 % (3994762)------------------------------ % 10.17/2.39 % (3994762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.17/2.39 % (3994762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.17/2.39 % (3994762)CaDiCaL version: 2.1.3 % 10.17/2.39 % (3994762)Termination reason: Instruction limit % 10.17/2.39 % (3994762)Termination phase: Saturation % 10.17/2.39 % (3994762)Time elapsed: 0.104 s % 10.17/2.39 % (3994762)Peak memory usage: 88 MB % 10.17/2.39 % (3994762)Instructions burned: 119 (million) % 10.17/2.39 % (3994764)Instruction limit reached! % 10.17/2.39 % (3994764)------------------------------ % 10.17/2.39 % (3994764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.17/2.39 % (3994764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.17/2.39 % (3994764)CaDiCaL version: 2.1.3 % 10.17/2.39 % (3994764)Termination reason: Instruction limit % 10.17/2.39 % (3994764)Termination phase: Saturation % 10.17/2.39 % (3994764)Time elapsed: 0.116 s % 10.17/2.39 % (3994764)Peak memory usage: 89 MB % 10.17/2.39 % (3994764)Instructions burned: 133 (million) % 10.17/2.39 % (3994763)Instruction limit reached! % 10.17/2.39 % (3994763)------------------------------ % 10.17/2.39 % (3994763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.17/2.39 % (3994763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.17/2.39 % (3994763)CaDiCaL version: 2.1.3 % 10.17/2.39 % (3994763)Termination reason: Instruction limit % 10.17/2.39 % (3994763)Termination phase: Saturation % 10.17/2.39 % (3994763)Time elapsed: 0.130 s % 10.17/2.39 % (3994763)Peak memory usage: 89 MB % 10.17/2.39 % (3994763)Instructions burned: 140 (million) % 10.17/2.39 % Exception at run slice level % 10.17/2.39 User error: GNN currently only supports monomorphic FOL. % 10.17/2.39 % (3994776)lrs+10_1_sil=8000:sp=occurrence:random_seed=3951123942:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi) % 10.17/2.39 % (3994777)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3893840848:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi) % 10.17/2.39 % (3994761)------------------------------ % 10.17/2.39 % (3994761)------------------------------ % 15.89/3.06 % (3994778)lrs+1011_1_sil=32000:sp=occurrence:random_seed=239035411:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi) % 15.89/3.06 % Exception at run slice level % 15.89/3.06 User error: GNN currently only supports monomorphic FOL. % 15.89/3.06 % (3994777)Instruction limit reached! % 15.89/3.06 % (3994777)------------------------------ % 15.89/3.06 % (3994777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.89/3.06 % (3994777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.89/3.06 % (3994777)CaDiCaL version: 2.1.3 % 15.89/3.06 % (3994777)Termination reason: Instruction limit % 15.89/3.06 % (3994777)Termination phase: Saturation % 15.89/3.06 % (3994777)Time elapsed: 0.138 s % 15.89/3.06 % (3994777)Peak memory usage: 89 MB % 15.89/3.06 % (3994777)Instructions burned: 158 (million) % 15.89/3.06 % (3994779)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=1569388164:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi) % 15.89/3.06 % Exception at run slice level % 15.89/3.06 User error: GNN currently only supports monomorphic FOL. % 15.89/3.06 % (3994784)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2113987041:i=2350_2993 on theBenchmark for (2993ds/2350Mi) % 15.89/3.06 % (3994782)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=210282142:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi) % 15.89/3.06 % (3994776)Instruction limit reached! % 15.89/3.06 % (3994776)------------------------------ % 15.89/3.06 % (3994776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.89/3.06 % (3994776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.89/3.06 % (3994776)CaDiCaL version: 2.1.3 % 15.89/3.06 % (3994776)Termination reason: Instruction limit % 15.89/3.06 % (3994776)Termination phase: Saturation % 15.89/3.06 % (3994776)Time elapsed: 0.270 s % 15.89/3.06 % (3994776)Peak memory usage: 90 MB % 15.89/3.06 % (3994776)Instructions burned: 286 (million) % 15.89/3.06 % (3994779)Instruction limit reached! % 15.89/3.06 % (3994779)------------------------------ % 15.89/3.06 % (3994779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.89/3.06 % (3994779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.89/3.06 % (3994779)CaDiCaL version: 2.1.3 % 15.89/3.06 % (3994779)Termination reason: Instruction limit % 15.89/3.06 % (3994779)Termination phase: Saturation % 15.89/3.06 % (3994779)Time elapsed: 0.114 s % 15.89/3.06 % (3994779)Peak memory usage: 90 MB % 15.89/3.06 % (3994779)Instructions burned: 249 (million) % 15.89/3.06 % (3994782)Refutation not found, incomplete strategy % 15.89/3.06 % (3994782)------------------------------ % 15.89/3.06 % (3994782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.89/3.06 % (3994782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.89/3.06 % (3994782)CaDiCaL version: 2.1.3 % 15.89/3.06 % (3994782)Termination reason: Refutation not found, incomplete strategy % 15.89/3.06 % (3994782)Time elapsed: 0.017 s % 15.89/3.06 % (3994782)Peak memory usage: 88 MB % 15.89/3.06 % (3994782)Instructions burned: 18 (million) % 15.89/3.06 % (3994778)Instruction limit reached! % 15.89/3.06 % (3994778)------------------------------ % 15.89/3.06 % (3994778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.89/3.06 % (3994778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.89/3.06 % (3994778)CaDiCaL version: 2.1.3 % 15.89/3.06 % (3994778)Termination reason: Instruction limit % 15.89/3.06 % (3994778)Termination phase: Saturation % 15.89/3.06 % (3994778)Time elapsed: 0.291 s % 15.89/3.06 % (3994778)Peak memory usage: 91 MB % 15.89/3.06 % (3994778)Instructions burned: 326 (million) % 15.89/3.06 % (3994785)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2186614910:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi) % 15.89/3.06 % (3994785)Instruction limit reached! % 15.89/3.06 % (3994785)------------------------------ % 15.89/3.06 % (3994785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.89/3.06 % (3994785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.89/3.06 % (3994785)CaDiCaL version: 2.1.3 % 15.89/3.06 % (3994785)Termination reason: Instruction limit % 15.89/3.06 % (3994785)Termination phase: Saturation % 15.89/3.06 % (3994785)Time elapsed: 0.107 s % 15.89/3.06 % (3994785)Peak memory usage: 89 MB % 15.89/3.06 % (3994785)Instructions burned: 114 (million) % 18.45/3.67 % (3994787)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=218993115:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi) % 18.45/3.67 % (3994787)Refutation not found, incomplete strategy % 18.45/3.67 % (3994787)------------------------------ % 18.45/3.67 % (3994787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.45/3.67 % (3994787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.45/3.67 % (3994787)CaDiCaL version: 2.1.3 % 18.45/3.67 % (3994787)Termination reason: Refutation not found, incomplete strategy % 18.45/3.67 % (3994787)Time elapsed: 0.016 s % 18.45/3.67 % (3994787)Peak memory usage: 88 MB % 18.45/3.67 % (3994787)Instructions burned: 18 (million) % 18.45/3.67 % (3994791)lrs+10_1_sil=8000:sp=occurrence:random_seed=2671073554:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi) % 18.45/3.67 % (3994790)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2185573076:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi) % 18.45/3.67 % Exception at run slice level % 18.45/3.67 User error: GNN currently only supports monomorphic FOL. % 18.45/3.67 % (3994792)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3734332974:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi) % 18.45/3.67 % (3994792)Refutation not found, incomplete strategy % 18.45/3.67 % (3994792)------------------------------ % 18.45/3.67 % (3994792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.45/3.67 % (3994792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.45/3.67 % (3994792)CaDiCaL version: 2.1.3 % 18.45/3.67 % (3994792)Termination reason: Refutation not found, incomplete strategy % 18.45/3.67 % (3994792)Time elapsed: 0.020 s % 18.45/3.67 % (3994792)Peak memory usage: 89 MB % 18.45/3.67 % (3994792)Instructions burned: 23 (million) % 18.45/3.67 % (3994790)Instruction limit reached! % 18.45/3.67 % (3994790)------------------------------ % 18.45/3.67 % (3994790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.45/3.67 % (3994790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.45/3.67 % (3994790)CaDiCaL version: 2.1.3 % 18.45/3.67 % (3994790)Termination reason: Instruction limit % 18.45/3.67 % (3994790)Termination phase: Saturation % 18.45/3.67 % (3994790)Time elapsed: 0.106 s % 18.45/3.67 % (3994790)Peak memory usage: 89 MB % 18.45/3.67 % (3994790)Instructions burned: 114 (million) % 18.45/3.67 % (3994782)------------------------------ % 18.45/3.67 % (3994782)------------------------------ % 18.45/3.67 % (3994795)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1216173407:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi) % 18.45/3.67 % (3994798)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4278058410:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi) % 18.45/3.67 % (3994798)Instruction limit reached! % 18.45/3.67 % (3994798)------------------------------ % 18.45/3.67 % (3994798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.45/3.67 % (3994798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.45/3.67 % (3994798)CaDiCaL version: 2.1.3 % 18.45/3.67 % (3994798)Termination reason: Instruction limit % 18.45/3.67 % (3994798)Termination phase: Saturation % 18.45/3.67 % (3994798)Time elapsed: 0.065 s % 18.45/3.67 % (3994798)Peak memory usage: 89 MB % 18.45/3.67 % (3994798)Instructions burned: 134 (million) % 18.45/3.67 % (3994787)------------------------------ % 18.45/3.67 % (3994787)------------------------------ % 18.45/3.67 % (3994801)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4248630537:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi) % 18.45/3.67 % (3994801)Refutation not found, incomplete strategy % 18.45/3.67 % (3994801)------------------------------ % 18.45/3.67 % (3994801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.45/3.67 % (3994801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.45/3.67 % (3994801)CaDiCaL version: 2.1.3 % 18.45/3.67 % (3994801)Termination reason: Refutation not found, incomplete strategy % 18.45/3.67 % (3994801)Time elapsed: 0.022 s % 18.45/3.67 % (3994801)Peak memory usage: 88 MB % 18.45/3.67 % (3994801)Instructions burned: 25 (million) % 18.45/3.67 % (3994804)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=402405667:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi) % 23.88/4.24 % (3994792)------------------------------ % 23.88/4.24 % (3994792)------------------------------ % 23.88/4.24 % (3994817)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=4014429795:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi) % 23.88/4.24 % (3994817)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 23.88/4.24 % (3994821)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1371860280:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi) % 23.88/4.24 % Exception at run slice level % 23.88/4.24 User error: Immediate (shared) subterms of term/literal combk(option(X1),X0,none(X1)) = sF80(X1,X0) have different types/not well-typed! % 23.88/4.24 % (3994817)Instruction limit reached! % 23.88/4.24 % (3994817)------------------------------ % 23.88/4.24 % (3994817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.88/4.24 % (3994817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.88/4.24 % (3994817)CaDiCaL version: 2.1.3 % 23.88/4.24 % (3994817)Termination reason: Instruction limit % 23.88/4.24 % (3994817)Termination phase: Saturation % 23.88/4.24 % (3994817)Time elapsed: 0.082 s % 23.88/4.24 % (3994817)Peak memory usage: 90 MB % 23.88/4.24 % (3994817)Instructions burned: 126 (million) % 23.88/4.24 % (3994824)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3152263829:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/141Mi) % 23.88/4.24 % (3994824)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 23.88/4.24 % (3994824)Refutation not found, incomplete strategy % 23.88/4.24 % (3994824)------------------------------ % 23.88/4.24 % (3994824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.88/4.24 % (3994824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.88/4.24 % (3994824)CaDiCaL version: 2.1.3 % 23.88/4.24 % (3994824)Termination reason: Refutation not found, incomplete strategy % 23.88/4.24 % (3994824)Time elapsed: 0.004 s % 23.88/4.24 % (3994824)Peak memory usage: 88 MB % 23.88/4.24 % (3994824)Instructions burned: 3 (million) % 23.88/4.24 % (3994801)------------------------------ % 23.88/4.24 % (3994801)------------------------------ % 23.88/4.24 % (3994827)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1559330543:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2982 on theBenchmark for (2982ds/431Mi) % 23.88/4.24 % (3994791)Instruction limit reached! % 23.88/4.24 % (3994791)------------------------------ % 23.88/4.24 % (3994791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.88/4.24 % (3994791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.88/4.24 % (3994791)CaDiCaL version: 2.1.3 % 23.88/4.24 % (3994791)Termination reason: Instruction limit % 23.88/4.24 % (3994791)Termination phase: Saturation % 23.88/4.24 % (3994791)Time elapsed: 0.800 s % 23.88/4.24 % (3994791)Peak memory usage: 95 MB % 23.88/4.24 % (3994791)Instructions burned: 907 (million) % 23.88/4.24 % (3994827)Refutation not found, incomplete strategy % 23.88/4.24 % (3994827)------------------------------ % 23.88/4.24 % (3994827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.88/4.24 % (3994827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.88/4.24 % (3994827)CaDiCaL version: 2.1.3 % 23.88/4.24 % (3994827)Termination reason: Refutation not found, incomplete strategy % 23.88/4.24 % (3994827)Time elapsed: 0.009 s % 23.88/4.24 % (3994827)Peak memory usage: 88 MB % 23.88/4.24 % (3994827)Instructions burned: 18 (million) % 23.88/4.24 % Exception at run slice level % 23.88/4.24 User error: GNN currently only supports monomorphic FOL. % 23.88/4.24 % (3994829)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=4053113833:i=6060:aac=none:ins=25_2982 on theBenchmark for (2982ds/6060Mi) % 23.88/4.24 % Exception at run slice level % 23.88/4.24 User error: GNN currently only supports monomorphic FOL. % 23.88/4.24 % (3994827)------------------------------ % 23.88/4.24 % (3994827)------------------------------ % 23.88/4.24 % (3994832)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=3645389238:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2980 on theBenchmark for (2980ds/150Mi) % 33.65/5.63 % (3994833)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3036528153:i=14155:bd=all_2980 on theBenchmark for (2980ds/14155Mi) % 33.65/5.63 % (3994832)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 33.65/5.63 % (3994834)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3238522743:i=667:av=off:fsr=off_2980 on theBenchmark for (2980ds/667Mi) % 33.65/5.63 % (3994824)------------------------------ % 33.65/5.63 % (3994824)------------------------------ % 33.65/5.63 % (3994832)Instruction limit reached! % 33.65/5.63 % (3994832)------------------------------ % 33.65/5.63 % (3994832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.65/5.63 % (3994832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.65/5.63 % (3994832)CaDiCaL version: 2.1.3 % 33.65/5.63 % (3994832)Termination reason: Instruction limit % 33.65/5.63 % (3994832)Termination phase: Saturation % 33.65/5.63 % (3994832)Time elapsed: 0.130 s % 33.65/5.63 % (3994832)Peak memory usage: 90 MB % 33.65/5.63 % (3994832)Instructions burned: 151 (million) % 33.65/5.63 % (3994837)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=464733961:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2978 on theBenchmark for (2978ds/193Mi) % 33.65/5.63 % (3994836)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=3819124408:s2a=on:i=185:s2at=1.8:fdi=4_2978 on theBenchmark for (2978ds/185Mi) % 33.65/5.63 % (3994837)Instruction limit reached! % 33.65/5.63 % (3994837)------------------------------ % 33.65/5.63 % (3994837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.65/5.63 % (3994837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.65/5.63 % (3994837)CaDiCaL version: 2.1.3 % 33.65/5.63 % (3994837)Termination reason: Instruction limit % 33.65/5.63 % (3994837)Termination phase: Saturation % 33.65/5.63 % (3994837)Time elapsed: 0.089 s % 33.65/5.63 % (3994837)Peak memory usage: 89 MB % 33.65/5.63 % (3994837)Instructions burned: 193 (million) % 33.65/5.63 % (3994841)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3513811746:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2977 on theBenchmark for (2977ds/4850Mi) % 33.65/5.63 % (3994841)Refutation not found, incomplete strategy % 33.65/5.63 % (3994841)------------------------------ % 33.65/5.63 % (3994841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.65/5.63 % (3994841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.65/5.63 % (3994841)CaDiCaL version: 2.1.3 % 33.65/5.63 % (3994841)Termination reason: Refutation not found, incomplete strategy % 33.65/5.63 % (3994841)Time elapsed: 0.018 s % 33.65/5.63 % (3994841)Peak memory usage: 88 MB % 33.65/5.63 % (3994841)Instructions burned: 19 (million) % 33.65/5.63 % (3994842)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=407505262:i=12111:sd=1:ss=included_2976 on theBenchmark for (2976ds/12111Mi) % 33.65/5.63 % (3994836)Instruction limit reached! % 33.65/5.63 % (3994836)------------------------------ % 33.65/5.63 % (3994836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.65/5.63 % (3994836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.65/5.63 % (3994836)CaDiCaL version: 2.1.3 % 33.65/5.63 % (3994836)Termination reason: Instruction limit % 33.65/5.63 % (3994836)Termination phase: Saturation % 33.65/5.63 % (3994836)Time elapsed: 0.175 s % 33.65/5.63 % (3994836)Peak memory usage: 90 MB % 33.65/5.63 % (3994836)Instructions burned: 185 (million) % 33.65/5.63 % Exception at run slice level % 33.65/5.63 User error: GNN currently only supports monomorphic FOL. % 33.65/5.63 % (3994845)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3822788299:i=319:kws=precedence:fsr=off_2975 on theBenchmark for (2975ds/319Mi) % 33.65/5.63 % Exception at run slice level % 33.65/5.63 User error: GNN currently only supports monomorphic FOL. % 33.65/5.63 % (3994848)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2599105604:i=2064:ep=RST_2974 on theBenchmark for (2974ds/2064Mi) % 33.65/5.63 % (3994834)Instruction limit reached! % 33.65/5.63 % (3994834)------------------------------ % 44.85/7.18 % (3994834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.85/7.18 % (3994834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.85/7.18 % (3994834)CaDiCaL version: 2.1.3 % 44.85/7.18 % (3994834)Termination reason: Instruction limit % 44.85/7.18 % (3994834)Termination phase: Saturation % 44.85/7.18 % (3994834)Time elapsed: 0.577 s % 44.85/7.18 % (3994834)Peak memory usage: 89 MB % 44.85/7.18 % (3994834)Instructions burned: 667 (million) % 44.85/7.18 % (3994848)Refutation not found, incomplete strategy % 44.85/7.18 % (3994848)------------------------------ % 44.85/7.18 % (3994848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.85/7.18 % (3994848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.85/7.18 % (3994848)CaDiCaL version: 2.1.3 % 44.85/7.18 % (3994848)Termination reason: Refutation not found, incomplete strategy % 44.85/7.18 % (3994848)Time elapsed: 0.019 s % 44.85/7.18 % (3994848)Peak memory usage: 88 MB % 44.85/7.18 % (3994848)Instructions burned: 21 (million) % 44.85/7.18 % (3994849)dis-1011_128_sil=32000:random_seed=2616244787:i=3706:ep=RST:av=off_2973 on theBenchmark for (2973ds/3706Mi) % 44.85/7.18 % (3994841)------------------------------ % 44.85/7.18 % (3994841)------------------------------ % 44.85/7.18 % (3994845)Instruction limit reached! % 44.85/7.18 % (3994845)------------------------------ % 44.85/7.18 % (3994845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.85/7.18 % (3994845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.85/7.18 % (3994845)CaDiCaL version: 2.1.3 % 44.85/7.18 % (3994845)Termination reason: Instruction limit % 44.85/7.18 % (3994845)Termination phase: Saturation % 44.85/7.18 % (3994845)Time elapsed: 0.271 s % 44.85/7.18 % (3994845)Peak memory usage: 91 MB % 44.85/7.18 % (3994845)Instructions burned: 319 (million) % 44.85/7.18 % (3994851)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2634770241:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2971 on theBenchmark for (2971ds/757Mi) % 44.85/7.18 % (3994857)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1697444079:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2970 on theBenchmark for (2970ds/2479Mi) % 44.85/7.18 % (3994851)Refutation not found, incomplete strategy % 44.85/7.18 % (3994851)------------------------------ % 44.85/7.18 % (3994851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.85/7.18 % (3994851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.85/7.18 % (3994851)CaDiCaL version: 2.1.3 % 44.85/7.18 % (3994851)Termination reason: Refutation not found, incomplete strategy % 44.85/7.18 % (3994851)Time elapsed: 0.019 s % 44.85/7.18 % (3994851)Peak memory usage: 88 MB % 44.85/7.18 % (3994851)Instructions burned: 20 (million) % 44.85/7.18 % (3994857)Refutation not found, incomplete strategy % 44.85/7.18 % (3994857)------------------------------ % 44.85/7.18 % (3994857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.85/7.18 % (3994857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.85/7.18 % (3994857)CaDiCaL version: 2.1.3 % 44.85/7.18 % (3994857)Termination reason: Refutation not found, incomplete strategy % 44.85/7.18 % (3994857)Time elapsed: 0.002 s % 44.85/7.18 % (3994857)Peak memory usage: 88 MB % 44.85/7.18 % (3994857)Instructions burned: 5 (million) % 44.85/7.18 % (3994853)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2109986760:i=13913:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/13913Mi) % 44.85/7.18 % Exception at run slice level % 44.85/7.18 User error: GNN currently only supports monomorphic FOL. % 44.85/7.18 % (3994855)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2929198893:i=9925:aac=none_2970 on theBenchmark for (2970ds/9925Mi) % 44.85/7.18 % (3994848)------------------------------ % 44.85/7.18 % (3994848)------------------------------ % 44.85/7.18 % (3994857)------------------------------ % 44.85/7.18 % (3994857)------------------------------ % 44.85/7.18 % (3994867)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=472966673:cts=off:i=3034:av=off:er=known:fsd=on_2967 on theBenchmark for (2967ds/3034Mi) % 44.85/7.18 % (3994862)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2540631433:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2968 on theBenchmark for (2968ds/440Mi) % 44.85/7.18 % (3994862)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 62.16/9.65 % (3994851)------------------------------ % 62.16/9.65 % (3994851)------------------------------ % 62.16/9.65 % (3994866)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=918869935:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2967 on theBenchmark for (2967ds/11145Mi) % 62.16/9.65 % Exception at run slice level % 62.16/9.65 User error: GNN currently only supports monomorphic FOL. % 62.16/9.65 % Exception at run slice level % 62.16/9.65 User error: GNN currently only supports monomorphic FOL. % 62.16/9.65 % (3994872)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=744617257:st=2:s2a=on:i=524:s2at=2:ss=axioms_2965 on theBenchmark for (2965ds/524Mi) % 62.16/9.65 % (3994876)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=225658100:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2963 on theBenchmark for (2963ds/1016Mi) % 62.16/9.65 % Exception at run slice level % 62.16/9.65 User error: GNN currently only supports monomorphic FOL. % 62.16/9.65 % (3994862)Instruction limit reached! % 62.16/9.65 % (3994862)------------------------------ % 62.16/9.65 % (3994862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.16/9.65 % (3994862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.16/9.65 % (3994862)CaDiCaL version: 2.1.3 % 62.16/9.65 % (3994862)Termination reason: Instruction limit % 62.16/9.65 % (3994862)Termination phase: Saturation % 62.16/9.65 % (3994862)Time elapsed: 0.423 s % 62.16/9.65 % (3994862)Peak memory usage: 92 MB % 62.16/9.65 % (3994862)Instructions burned: 441 (million) % 62.16/9.65 % (3994877)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=534633633:i=14123:bd=preordered:ins=4_2963 on theBenchmark for (2963ds/14123Mi) % 62.16/9.65 % (3994881)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=3051529802:i=2448:gtgl=5:bd=preordered:gtg=all_2961 on theBenchmark for (2961ds/2448Mi) % 62.16/9.65 % (3994880)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3254309731:i=5781:kws=precedence:bd=all:rawr=on_2961 on theBenchmark for (2961ds/5781Mi) % 62.16/9.65 % Exception at run slice level % 62.16/9.65 User error: GNN currently only supports monomorphic FOL. % 62.16/9.65 % (3994876)Instruction limit reached! % 62.16/9.65 % (3994876)------------------------------ % 62.16/9.65 % (3994876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.16/9.65 % (3994876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.16/9.65 % (3994876)CaDiCaL version: 2.1.3 % 62.16/9.65 % (3994876)Termination reason: Instruction limit % 62.16/9.65 % (3994876)Termination phase: Saturation % 62.16/9.65 % (3994876)Time elapsed: 0.341 s % 62.16/9.65 % (3994876)Peak memory usage: 94 MB % 62.16/9.65 % (3994876)Instructions burned: 1017 (million) % 62.16/9.65 % (3994872)Instruction limit reached! % 62.16/9.65 % (3994872)------------------------------ % 62.16/9.65 % (3994872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.16/9.65 % (3994872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.16/9.65 % (3994872)CaDiCaL version: 2.1.3 % 62.16/9.65 % (3994872)Termination reason: Instruction limit % 62.16/9.65 % (3994872)Termination phase: Saturation % 62.16/9.65 % (3994872)Time elapsed: 0.458 s % 62.16/9.65 % (3994872)Peak memory usage: 92 MB % 62.16/9.65 % (3994872)Instructions burned: 525 (million) % 62.16/9.65 % (3994891)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3391515128:i=3223:kws=precedence:fgj=on:av=off_2959 on theBenchmark for (2959ds/3223Mi) % 62.16/9.65 % (3994892)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2399039778:st=5.6:i=2033:sd=3:ss=axioms_2959 on theBenchmark for (2959ds/2033Mi) % 62.16/9.65 % (3994893)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1668973924:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2957 on theBenchmark for (2957ds/2055Mi) % 62.16/9.65 % Exception at run slice level % 62.16/9.65 User error: GNN currently only supports monomorphic FOL. % 62.16/9.65 % Exception at run slice level % 62.16/9.65 User error: GNN currently only supports monomorphic FOL. % 62.16/9.65 % Exception at run slice level % 62.16/9.65 User error: GNN currently only supports monomorphic FOL. % 62.16/9.65 % (3994897)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=2414195907:i=21611:sd=3:ss=axioms_2954 on theBenchmark for (2954ds/21611Mi) % 75.91/11.62 % Exception at run slice level % 75.91/11.62 User error: GNN currently only supports monomorphic FOL. % 75.91/11.62 % (3994898)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2200691905:i=4835:sd=13:ss=axioms:sgt=23_2953 on theBenchmark for (2953ds/4835Mi) % 75.91/11.62 % (3994899)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=2701326276:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2952 on theBenchmark for (2952ds/797Mi) % 75.91/11.62 % Exception at run slice level % 75.91/11.62 User error: GNN currently only supports monomorphic FOL. % 75.91/11.62 % (3994903)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2511749773:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2951 on theBenchmark for (2951ds/2326Mi) % 75.91/11.62 % (3994903)Refutation not found, incomplete strategy % 75.91/11.62 % (3994903)------------------------------ % 75.91/11.62 % (3994903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.91/11.62 % (3994903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.91/11.62 % (3994903)CaDiCaL version: 2.1.3 % 75.91/11.62 % (3994903)Termination reason: Refutation not found, incomplete strategy % 75.91/11.62 % (3994903)Time elapsed: 0.028 s % 75.91/11.62 % (3994903)Peak memory usage: 89 MB % 75.91/11.62 % (3994903)Instructions burned: 28 (million) % 75.91/11.62 % (3994899)Instruction limit reached! % 75.91/11.62 % (3994899)------------------------------ % 75.91/11.62 % (3994899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.91/11.62 % (3994899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.91/11.62 % (3994899)CaDiCaL version: 2.1.3 % 75.91/11.62 % (3994899)Termination reason: Instruction limit % 75.91/11.62 % (3994899)Termination phase: Saturation % 75.91/11.62 % (3994899)Time elapsed: 0.224 s % 75.91/11.62 % (3994899)Peak memory usage: 94 MB % 75.91/11.62 % (3994899)Instructions burned: 798 (million) % 75.91/11.62 % (3994908)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3716442498:i=6038:nm=6_2950 on theBenchmark for (2950ds/6038Mi) % 75.91/11.62 % (3994910)lrs+10_1_sil=32000:sp=occurrence:random_seed=3671733900:st=2:i=33334:sd=3:ss=included:sgt=32_2948 on theBenchmark for (2948ds/33334Mi) % 75.91/11.62 % Exception at run slice level % 75.91/11.62 User error: GNN currently only supports monomorphic FOL. % 75.91/11.62 % (3994903)------------------------------ % 75.91/11.62 % (3994903)------------------------------ % 75.91/11.62 % (3994913)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3770545777:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2946 on theBenchmark for (2946ds/1008Mi) % 75.91/11.62 % (3994849)Instruction limit reached! % 75.91/11.62 % (3994849)------------------------------ % 75.91/11.62 % (3994849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.91/11.62 % (3994849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.91/11.62 % (3994849)CaDiCaL version: 2.1.3 % 75.91/11.62 % (3994849)Termination reason: Instruction limit % 75.91/11.62 % (3994849)Termination phase: Saturation % 75.91/11.62 % (3994849)Time elapsed: 2.864 s % 75.91/11.62 % (3994849)Peak memory usage: 102 MB % 75.91/11.62 % (3994849)Instructions burned: 3707 (million) % 75.91/11.62 % (3994917)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=2136062109:i=8327:s2at=5:bd=preordered_2944 on theBenchmark for (2944ds/8327Mi) % 75.91/11.62 % Exception at run slice level % 75.91/11.62 User error: GNN currently only supports monomorphic FOL. % 75.91/11.62 % (3994920)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=2040521190:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2942 on theBenchmark for (2942ds/1083Mi) % 75.91/11.62 % (3994922)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=4111175102:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2942 on theBenchmark for (2942ds/1084Mi) % 75.91/11.62 % Exception at run slice level % 95.37/14.32 User error: GNN currently only supports monomorphic FOL. % 95.37/14.32 % (3994913)Instruction limit reached! % 95.37/14.32 % (3994913)------------------------------ % 95.37/14.32 % (3994913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.37/14.32 % (3994913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.37/14.32 % (3994913)CaDiCaL version: 2.1.3 % 95.37/14.32 % (3994913)Termination reason: Instruction limit % 95.37/14.32 % (3994913)Termination phase: Saturation % 95.37/14.32 % (3994913)Time elapsed: 0.884 s % 95.37/14.32 % (3994913)Peak memory usage: 98 MB % 95.37/14.32 % (3994913)Instructions burned: 1008 (million) % 95.37/14.32 % (3994925)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2606334890:i=6995:s2at=5:gtg=all_2936 on theBenchmark for (2936ds/6995Mi) % 95.37/14.32 % (3994926)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=4207013528:st=2:i=6225:sd=15:ss=axioms_2934 on theBenchmark for (2934ds/6225Mi) % 95.37/14.32 % (3994920)Instruction limit reached! % 95.37/14.32 % (3994920)------------------------------ % 95.37/14.32 % (3994920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.37/14.32 % (3994920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.37/14.32 % (3994920)CaDiCaL version: 2.1.3 % 95.37/14.32 % (3994920)Termination reason: Instruction limit % 95.37/14.32 % (3994920)Termination phase: Saturation % 95.37/14.32 % (3994920)Time elapsed: 1.002 s % 95.37/14.32 % (3994920)Peak memory usage: 98 MB % 95.37/14.32 % (3994920)Instructions burned: 1083 (million) % 95.37/14.32 % (3994922)Instruction limit reached! % 95.37/14.32 % (3994922)------------------------------ % 95.37/14.32 % (3994922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.37/14.32 % (3994922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.37/14.32 % (3994922)CaDiCaL version: 2.1.3 % 95.37/14.32 % (3994922)Termination reason: Instruction limit % 95.37/14.32 % (3994922)Termination phase: Saturation % 95.37/14.32 % (3994922)Time elapsed: 0.969 s % 95.37/14.32 % (3994922)Peak memory usage: 95 MB % 95.37/14.32 % (3994922)Instructions burned: 1084 (million) % 95.37/14.32 % Exception at run slice level % 95.37/14.32 User error: GNN currently only supports monomorphic FOL. % 95.37/14.32 % (3994933)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=778224055:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2930 on theBenchmark for (2930ds/3372Mi) % 95.37/14.32 % (3994934)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1001764766:st=2.3:i=26457:sd=10:ss=included:sgt=8_2930 on theBenchmark for (2930ds/26457Mi) % 95.37/14.32 % (3994935)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=18334609:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2927 on theBenchmark for (2927ds/13494Mi) % 95.37/14.32 % Exception at run slice level % 95.37/14.32 User error: GNN currently only supports monomorphic FOL. % 95.37/14.32 % Exception at run slice level % 95.37/14.32 User error: GNN currently only supports monomorphic FOL. % 95.37/14.32 % (3994941)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=1859041365:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2921 on theBenchmark for (2921ds/2503Mi) % 95.37/14.32 % (3994942)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=2453951639:i=2559:sd=1:ep=RSTC:ss=axioms_2921 on theBenchmark for (2921ds/2559Mi) % 95.37/14.32 % (3994941)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 95.37/14.32 % Exception at run slice level % 95.37/14.32 User error: GNN currently only supports monomorphic FOL. % 95.37/14.32 % (3994945)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1130817533:i=30753:av=off:ss=included_2918 on theBenchmark for (2918ds/30753Mi) % 95.37/14.32 % Exception at run slice level % 95.37/14.32 User error: GNN currently only supports monomorphic FOL. % 95.37/14.32 % Exception at run slice level % 95.37/14.32 User error: GNN currently only supports monomorphic FOL. % 95.37/14.32 % (3994880)Instruction limit reached! % 95.37/14.32 % (3994880)------------------------------ % 95.37/14.32 % (3994880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.37/14.32 % (3994880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.63/17.31 % (3994880)CaDiCaL version: 2.1.3 % 116.63/17.31 % (3994880)Termination reason: Instruction limit % 116.63/17.31 % (3994880)Termination phase: Saturation % 116.63/17.31 % (3994880)Time elapsed: 4.736 s % 116.63/17.31 % (3994880)Peak memory usage: 102 MB % 116.63/17.31 % (3994880)Instructions burned: 5782 (million) % 116.63/17.31 % (3994955)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3267223741:i=26473:ep=RSTC_2913 on theBenchmark for (2913ds/26473Mi) % 116.63/17.31 % (3994956)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=1543592230:cts=off:i=2759:kws=inv_arity:fgj=on_2913 on theBenchmark for (2913ds/2759Mi) % 116.63/17.31 % Exception at run slice level % 116.63/17.31 User error: GNN currently only supports monomorphic FOL. % 116.63/17.31 % (3994957)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=547915865:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2911 on theBenchmark for (2911ds/5665Mi) % 116.63/17.31 % (3994957)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 116.63/17.31 % (3994898)Instruction limit reached! % 116.63/17.31 % (3994898)------------------------------ % 116.63/17.31 % (3994898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.63/17.31 % (3994898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.63/17.31 % (3994898)CaDiCaL version: 2.1.3 % 116.63/17.31 % (3994898)Termination reason: Instruction limit % 116.63/17.31 % (3994898)Termination phase: Saturation % 116.63/17.31 % (3994898)Time elapsed: 4.218 s % 116.63/17.31 % (3994898)Peak memory usage: 101 MB % 116.63/17.31 % (3994898)Instructions burned: 4836 (million) % 116.63/17.31 % (3994960)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=2707375987:i=1532:ep=RS:ss=axioms_2909 on theBenchmark for (2909ds/1532Mi) % 116.63/17.31 % (3994962)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=4281789528:i=1565:sd=2:ss=axioms:sgt=32_2908 on theBenchmark for (2908ds/1565Mi) % 116.63/17.31 % Exception at run slice level % 116.63/17.31 User error: GNN currently only supports monomorphic FOL. % 116.63/17.31 % Exception at run slice level % 116.63/17.31 User error: GNN currently only supports monomorphic FOL. % 116.63/17.31 % (3994965)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=3911446102:i=1572:fgj=on:gsp=on_2905 on theBenchmark for (2905ds/1572Mi) % 116.63/17.31 % (3994965)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 116.63/17.31 % Exception at run slice level % 116.63/17.31 User error: GNN currently only supports monomorphic FOL. % 116.63/17.31 % (3994966)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=1863379780:i=6052:sd=4:ss=axioms:sgt=24_2903 on theBenchmark for (2903ds/6052Mi) % 116.63/17.31 % Exception at run slice level % 116.63/17.31 User error: GNN currently only supports monomorphic FOL. % 116.63/17.31 % (3994968)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=3772192950:i=3500:sd=1:bd=preordered:sup=off:ss=included_2901 on theBenchmark for (2901ds/3500Mi) % 116.63/17.31 % (3994970)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=2571941942:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2900 on theBenchmark for (2900ds/1842Mi) % 116.63/17.31 % (3994970)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 116.63/17.31 % Exception at run slice level % 116.63/17.31 User error: GNN currently only supports monomorphic FOL. % 116.63/17.31 % Exception at run slice level % 116.63/17.31 User error: GNN currently only supports monomorphic FOL. % 116.63/17.31 % (3994973)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=216732959:i=66096:add=on_2896 on theBenchmark for (2896ds/66096Mi) % 116.63/17.31 % Exception at run slice level % 116.63/17.31 User error: GNN currently only supports monomorphic FOL. % 116.63/17.31 % (3994974)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=3004239047:i=1884:sd=1:nm=60:ss=axioms_2894 on theBenchmark for (2894ds/1884Mi) % 133.73/20.04 % Exception at run slice level % 133.73/20.04 User error: GNN currently only supports monomorphic FOL. % 133.73/20.04 % (3994976)lrs-1011_4:1_sil=16000:bsr=on:random_seed=1058548585:cts=off:i=5469:bs=on:fsr=off_2892 on theBenchmark for (2892ds/5469Mi) % 133.73/20.04 % (3994978)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=1156724813:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2891 on theBenchmark for (2891ds/2037Mi) % 133.73/20.04 % Exception at run slice level % 133.73/20.04 User error: GNN currently only supports monomorphic FOL. % 133.73/20.04 % Exception at run slice level % 133.73/20.04 User error: GNN currently only supports monomorphic FOL. % 133.73/20.04 % (3994981)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=1828980224:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2887 on theBenchmark for (2887ds/2110Mi) % 133.73/20.04 % (3994982)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=3442397987:i=2430:add=off:aac=none:nm=16_2886 on theBenchmark for (2886ds/2430Mi) % 133.73/20.04 % Exception at run slice level % 133.73/20.04 User error: GNN currently only supports monomorphic FOL. % 133.73/20.04 % (3994985)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=3479965625:cond=fast:i=4891_2882 on theBenchmark for (2882ds/4891Mi) % 133.73/20.04 % Exception at run slice level % 133.73/20.04 User error: GNN currently only supports monomorphic FOL. % 133.73/20.04 % Exception at run slice level % 133.73/20.04 User error: GNN currently only supports monomorphic FOL. % 133.73/20.04 % (3994926)Instruction limit reached! % 133.73/20.04 % (3994926)------------------------------ % 133.73/20.04 % (3994926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.73/20.04 % (3994926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.73/20.04 % (3994926)CaDiCaL version: 2.1.3 % 133.73/20.04 % (3994926)Termination reason: Instruction limit % 133.73/20.04 % (3994926)Termination phase: Saturation % 133.73/20.04 % (3994926)Time elapsed: 5.510 s % 133.73/20.04 % (3994926)Peak memory usage: 124 MB % 133.73/20.04 % (3994926)Instructions burned: 6226 (million) % 133.73/20.04 % (3994987)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=1575661143:st=2:i=14845:sd=2:ss=included:fsd=on_2878 on theBenchmark for (2878ds/14845Mi) % 133.73/20.04 % (3994988)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=1967242556:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2878 on theBenchmark for (2878ds/7534Mi) % 133.73/20.04 % (3994989)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=1931902200:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2876 on theBenchmark for (2876ds/10353Mi) % 133.73/20.04 % Exception at run slice level % 133.73/20.04 User error: GNN currently only supports monomorphic FOL. % 133.73/20.04 % (3994993)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=120742289:i=7860_2873 on theBenchmark for (2873ds/7860Mi) % 133.73/20.04 % Exception at run slice level % 133.73/20.04 User error: GNN currently only supports monomorphic FOL. % 133.73/20.04 % Exception at run slice level % 133.73/20.04 User error: GNN currently only supports monomorphic FOL. % 133.73/20.04 % Exception at run slice level % 133.73/20.04 User error: GNN currently only supports monomorphic FOL. % 133.73/20.04 % (3994995)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=1096262391:i=7896:sd=2:bs=on:ss=included:sgt=20_2869 on theBenchmark for (2869ds/7896Mi) % 133.73/20.04 % (3994996)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1007298202:i=5812:gtgl=2:gtg=all_2869 on theBenchmark for (2869ds/5812Mi) % 133.73/20.04 % (3994997)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=3639888467:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2868 on theBenchmark for (2868ds/2965Mi) % 171.64/25.11 % Exception at run slice level % 171.64/25.11 User error: GNN currently only supports monomorphic FOL. % 171.64/25.11 % Exception at run slice level % 171.64/25.11 User error: GNN currently only supports monomorphic FOL. % 171.64/25.11 % (3995003)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=2806913927:i=2967:kws=precedence:bd=preordered:av=off_2862 on theBenchmark for (2862ds/2967Mi) % 171.64/25.11 % Exception at run slice level % 171.64/25.11 User error: GNN currently only supports monomorphic FOL. % 171.64/25.11 % (3995004)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=3087084490:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2860 on theBenchmark for (2860ds/3022Mi) % 171.64/25.11 % (3995006)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=1056104851:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2859 on theBenchmark for (2859ds/3207Mi) % 171.64/25.11 % Exception at run slice level % 171.64/25.11 User error: GNN currently only supports monomorphic FOL. % 171.64/25.11 % Exception at run slice level % 171.64/25.11 User error: GNN currently only supports monomorphic FOL. % 171.64/25.11 % (3995009)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=1562336390:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2853 on theBenchmark for (2853ds/3289Mi) % 171.64/25.11 % Exception at run slice level % 171.64/25.11 User error: GNN currently only supports monomorphic FOL. % 171.64/25.11 % (3995010)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=2445636854:i=38569:sd=3:ss=axioms:sgt=32_2852 on theBenchmark for (2852ds/38569Mi) % 171.64/25.11 % (3995012)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=2745247851:cts=off:i=3394_2851 on theBenchmark for (2851ds/3394Mi) % 171.64/25.11 % Exception at run slice level % 171.64/25.11 User error: GNN currently only supports monomorphic FOL. % 171.64/25.11 % Exception at run slice level % 171.64/25.11 User error: GNN currently only supports monomorphic FOL. % 171.64/25.11 % (3995023)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=960432487:i=33824:bd=preordered_2845 on theBenchmark for (2845ds/33824Mi) % 171.64/25.11 % Exception at run slice level % 171.64/25.11 User error: GNN currently only supports monomorphic FOL. % 171.64/25.11 % (3995024)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=1348960668:i=20684:bd=all:gtg=exists_sym_2844 on theBenchmark for (2844ds/20684Mi) % 171.64/25.11 % (3994976)Instruction limit reached! % 171.64/25.11 % (3994976)------------------------------ % 171.64/25.11 % (3994976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.64/25.11 % (3994976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.64/25.11 % (3994976)CaDiCaL version: 2.1.3 % 171.64/25.11 % (3994976)Termination reason: Instruction limit % 171.64/25.11 % (3994976)Termination phase: Saturation % 171.64/25.11 % (3994976)Time elapsed: 4.984 s % 171.64/25.11 % (3994976)Peak memory usage: 102 MB % 171.64/25.11 % (3994976)Instructions burned: 5470 (million) % 171.64/25.11 % (3995026)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=2051031625: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_2842 on theBenchmark for (2842ds/7222Mi) % 171.64/25.11 % (3995026)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 171.64/25.11 % Exception at run slice level % 171.64/25.11 User error: GNN currently only supports monomorphic FOL. % 171.64/25.11 % (3995031)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=39698002:st=4:i=7295:sd=4:ep=R:ss=axioms_2839 on theBenchmark for (2839ds/7295Mi) % 171.64/25.11 % Exception at run slice level % 171.64/25.11 User error: GNN currently only supports monomorphic FOL. % 171.64/25.11 % (3995035)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=1426779283:i=4036:ins=10_2837 on theBenchmark for (2837ds/4036Mi) % 203.18/29.60 % Exception at run slice level % 203.18/29.60 User error: GNN currently only supports monomorphic FOL. % 203.18/29.60 % Exception at run slice level % 203.18/29.60 User error: GNN currently only supports monomorphic FOL. % 203.18/29.60 % (3995036)lrs+10_1_sil=128000:lcm=predicate:random_seed=1886407907:st=3:i=43697:sd=5:ss=axioms_2835 on theBenchmark for (2835ds/43697Mi) % 203.18/29.60 % (3995038)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=3728582912:i=17599:gtg=all:ss=axioms:fsd=on_2834 on theBenchmark for (2834ds/17599Mi) % 203.18/29.60 % (3995039)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=1962661374:i=4547:bd=preordered_2833 on theBenchmark for (2833ds/4547Mi) % 203.18/29.60 % Exception at run slice level % 203.18/29.60 User error: GNN currently only supports monomorphic FOL. % 203.18/29.60 % Exception at run slice level % 203.18/29.60 User error: GNN currently only supports monomorphic FOL. % 203.18/29.60 % (3995043)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=1623140794:i=9294:av=off_2829 on theBenchmark for (2829ds/9294Mi) % 203.18/29.60 % (3995044)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2158784634:i=32849:add=on_2829 on theBenchmark for (2829ds/32849Mi) % 203.18/29.60 % Exception at run slice level % 203.18/29.60 User error: GNN currently only supports monomorphic FOL. % 203.18/29.60 % Exception at run slice level % 203.18/29.60 User error: GNN currently only supports monomorphic FOL. % 203.18/29.60 % (3995047)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1318339932:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2825 on theBenchmark for (2825ds/4793Mi) % 203.18/29.60 % (3995048)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=3990195915:i=4840:nm=4:av=off_2823 on theBenchmark for (2823ds/4840Mi) % 203.18/29.60 % Exception at run slice level % 203.18/29.60 User error: GNN currently only supports monomorphic FOL. % 203.18/29.60 % (3995051)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=1733780679:cts=off:i=5002_2821 on theBenchmark for (2821ds/5002Mi) % 203.18/29.60 % Exception at run slice level % 203.18/29.60 User error: GNN currently only supports monomorphic FOL. % 203.18/29.60 % Exception at run slice level % 203.18/29.60 User error: GNN currently only supports monomorphic FOL. % 203.18/29.60 % (3995053)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=2044285941:i=30479:sd=3:ss=axioms_2818 on theBenchmark for (2818ds/30479Mi) % 203.18/29.60 % (3995054)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=2718826463:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2817 on theBenchmark for (2817ds/11035Mi) % 203.18/29.60 % (3995054)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 203.18/29.60 % Exception at run slice level % 203.18/29.60 User error: GNN currently only supports monomorphic FOL. % 203.18/29.60 % Exception at run slice level % 203.18/29.60 User error: GNN currently only supports monomorphic FOL. % 203.18/29.60 % (3995057)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=492066507:i=5835_2813 on theBenchmark for (2813ds/5835Mi) % 203.18/29.60 % (3995058)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=3977325699:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2812 on theBenchmark for (2812ds/5890Mi) % 203.18/29.60 % Exception at run slice level % 203.18/29.60 User error: GNN currently only supports monomorphic FOL. % 203.18/29.60 % (3994993)Instruction limit reached! % 203.18/29.60 % (3994993)------------------------------ % 203.18/29.60 % (3994993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.18/29.60 % (3994993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.18/29.60 % (3994993)CaDiCaL version: 2.1.3 % 203.18/29.60 % (3994993)Termination reason: Instruction limit % 217.42/31.56 % (3994993)Termination phase: Saturation % 217.42/31.56 % (3994993)Time elapsed: 6.268 s % 217.42/31.56 % (3994993)Peak memory usage: 104 MB % 217.42/31.56 % (3994993)Instructions burned: 7862 (million) % 217.42/31.56 % Exception at run slice level % 217.42/31.56 User error: GNN currently only supports monomorphic FOL. % 217.42/31.56 % (3995063)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=2375685218:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2807 on theBenchmark for (2807ds/13822Mi) % 217.42/31.56 % (3995062)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=4049101277:i=20312:bd=preordered:fsr=off:er=filter_2807 on theBenchmark for (2807ds/20312Mi) % 217.42/31.56 % (3995061)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=3655369966:cts=off:i=19910:ep=RS_2808 on theBenchmark for (2808ds/19910Mi) % 217.42/31.56 % Exception at run slice level % 217.42/31.56 User error: GNN currently only supports monomorphic FOL. % 217.42/31.56 % (3995069)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=3373809604:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2805 on theBenchmark for (2805ds/7144Mi) % 217.42/31.56 % Exception at run slice level % 217.42/31.56 User error: GNN currently only supports monomorphic FOL. % 217.42/31.56 % Exception at run slice level % 217.42/31.56 User error: GNN currently only supports monomorphic FOL. % 217.42/31.56 % (3995071)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=825660486:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2800 on theBenchmark for (2800ds/15184Mi) % 217.42/31.56 % (3995072)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=2889540202:i=107375_2799 on theBenchmark for (2799ds/107375Mi) % 217.42/31.56 % Exception at run slice level % 217.42/31.56 User error: GNN currently only supports monomorphic FOL. % 217.42/31.56 % Exception at run slice level % 217.42/31.56 User error: GNN currently only supports monomorphic FOL. % 217.42/31.56 % (3995075)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=1171264177:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2792 on theBenchmark for (2792ds/7958Mi) % 217.42/31.56 % (3995076)dis+10_128_sil=16000:nwc=0.7:random_seed=1985479161:i=15999:nm=2:gsp=on_2790 on theBenchmark for (2790ds/15999Mi) % 217.42/31.56 % (3995076)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 217.42/31.56 % Exception at run slice level % 217.42/31.56 User error: GNN currently only supports monomorphic FOL. % 217.42/31.56 % (3995079)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=2111701697:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2783 on theBenchmark for (2783ds/8139Mi) % 217.42/31.56 % (3995069)Instruction limit reached! % 217.42/31.56 % (3995069)------------------------------ % 217.42/31.56 % (3995069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.42/31.56 % (3995069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.42/31.56 % (3995069)CaDiCaL version: 2.1.3 % 217.42/31.56 % (3995069)Termination reason: Instruction limit % 217.42/31.56 % (3995069)Termination phase: Saturation % 217.42/31.56 % (3995069)Time elapsed: 3.496 s % 217.42/31.56 % (3995069)Peak memory usage: 143 MB % 217.42/31.56 % (3995069)Instructions burned: 7145 (million) % 217.42/31.56 % (3995081)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=514064063:st=4:i=8950:sd=5:ss=axioms_2768 on theBenchmark for (2768ds/8950Mi) % 217.42/31.56 % Exception at run slice level % 217.42/31.56 User error: GNN currently only supports monomorphic FOL. % 217.42/31.56 % (3995085)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=478659104:i=9809:ins=10:av=off_2763 on theBenchmark for (2763ds/9809Mi) % 217.42/31.56 % Exception at run slice level % 217.42/31.56 User error: GNN currently only supports monomorphic FOL. % 217.42/31.56 % (3994910)Instruction limit reached! % 217.42/31.56 % (3994910)------------------------------ % 217.42/31.56 % (3994910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.42/31.56 % (3994910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.80/35.45 % (3994910)CaDiCaL version: 2.1.3 % 244.80/35.45 % (3994910)Termination reason: Instruction limit % 244.80/35.45 % (3994910)Termination phase: Saturation % 244.80/35.45 % (3994910)Time elapsed: 18.901 s % 244.80/35.45 % (3994910)Peak memory usage: 233 MB % 244.80/35.45 % (3994910)Instructions burned: 33334 (million) % 244.80/35.45 % (3995091)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=2363125770:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2758 on theBenchmark for (2758ds/9885Mi) % 244.80/35.45 % (3995092)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=3728994518:cond=fast:i=32078:fgj=on:av=off_2756 on theBenchmark for (2756ds/32078Mi) % 244.80/35.45 % Exception at run slice level % 244.80/35.45 User error: GNN currently only supports monomorphic FOL. % 244.80/35.45 % (3995095)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=217831068:i=11101:bd=all:ss=axioms:sgt=8_2752 on theBenchmark for (2752ds/11101Mi) % 244.80/35.45 % Exception at run slice level % 244.80/35.45 User error: GNN currently only supports monomorphic FOL. % 244.80/35.45 % (3995097)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=290595127:cond=on:i=13220:s2at=3:aac=none:fsd=on_2748 on theBenchmark for (2748ds/13220Mi) % 244.80/35.45 % Exception at run slice level % 244.80/35.45 User error: GNN currently only supports monomorphic FOL. % 244.80/35.45 % (3995101)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=3553049626:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2739 on theBenchmark for (2739ds/13528Mi) % 244.80/35.45 % Exception at run slice level % 244.80/35.45 User error: GNN currently only supports monomorphic FOL. % 244.80/35.45 % (3995103)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=3055255905:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2730 on theBenchmark for (2730ds/14854Mi) % 244.80/35.45 % Exception at run slice level % 244.80/35.45 User error: GNN currently only supports monomorphic FOL. % 244.80/35.45 % (3995175)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=1784689723:i=14974:ss=axioms:sgt=16_2724 on theBenchmark for (2724ds/14974Mi) % 244.80/35.45 % Exception at run slice level % 244.80/35.45 User error: GNN currently only supports monomorphic FOL. % 244.80/35.45 % (3995079)Instruction limit reached! % 244.80/35.45 % (3995079)------------------------------ % 244.80/35.45 % (3995079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.80/35.45 % (3995079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.80/35.45 % (3995079)CaDiCaL version: 2.1.3 % 244.80/35.45 % (3995079)Termination reason: Instruction limit % 244.80/35.45 % (3995079)Termination phase: Saturation % 244.80/35.45 % (3995079)Time elapsed: 6.098 s % 244.80/35.45 % (3995079)Peak memory usage: 112 MB % 244.80/35.45 % (3995079)Instructions burned: 8141 (million) % 244.80/35.45 % (3995264)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=3978513746:i=33081:aac=none:fgj=on:bd=all:fsr=off_2719 on theBenchmark for (2719ds/33081Mi) % 244.80/35.45 % (3995265)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=2432198456:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2719 on theBenchmark for (2719ds/50856Mi) % 244.80/35.45 % Exception at run slice level % 244.80/35.45 User error: GNN currently only supports monomorphic FOL. % 244.80/35.45 % Exception at run slice level % 244.80/35.45 User error: GNN currently only supports monomorphic FOL. % 244.80/35.45 % (3995268)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=1588792148:i=69865_2714 on theBenchmark for (2714ds/69865Mi) % 244.80/35.45 % (3995269)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=357234097:cond=fast:i=17802:gtgl=3:gtg=all_2714 on theBenchmark for (2714ds/17802Mi) % 244.80/35.45 % Exception at run slice level % 244.80/35.45 User error: Immediate (shared) subterms of term/literal combk(option(X1),X0,none(X1)) = sF80(X1,X0) have different types/not well-typed! % 252.72/36.51 % (3995095)Instruction limit reached! % 252.72/36.51 % (3995095)------------------------------ % 252.72/36.51 % (3995095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.72/36.51 % (3995095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.72/36.51 % (3995095)CaDiCaL version: 2.1.3 % 252.72/36.51 % (3995095)Termination reason: Instruction limit % 252.72/36.51 % (3995095)Termination phase: Saturation % 252.72/36.51 % (3995095)Time elapsed: 3.828 s % 252.72/36.51 % (3995095)Peak memory usage: 134 MB % 252.72/36.51 % (3995095)Instructions burned: 11108 (million) % 252.72/36.51 % (3995273)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 252.72/36.51 % (3995273)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=766437440:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2712 on theBenchmark for (2712ds/21161Mi) % 252.72/36.51 % (3995272)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=977004333:i=96644_2712 on theBenchmark for (2712ds/96644Mi) % 252.72/36.51 % (3994955)Instruction limit reached! % 252.72/36.51 % (3994955)------------------------------ % 252.72/36.51 % (3994955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.72/36.51 % (3994955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.72/36.51 % (3994955)CaDiCaL version: 2.1.3 % 252.72/36.51 % (3994955)Termination reason: Instruction limit % 252.72/36.51 % (3994955)Termination phase: Saturation % 252.72/36.51 % (3994955)Time elapsed: 20.083 s % 252.72/36.51 % (3994955)Peak memory usage: 453 MB % 252.72/36.51 % (3994955)Instructions burned: 26475 (million) % 252.72/36.51 % Exception at run slice level % 252.72/36.51 User error: GNN currently only supports monomorphic FOL. % 252.72/36.51 % (3995276)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=2203627766:i=22761:gtg=all:ss=axioms:fsd=on_2709 on theBenchmark for (2709ds/22761Mi) % 252.72/36.51 % (3995277)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=382099726:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2709 on theBenchmark for (2709ds/23713Mi) % 252.72/36.51 % (3995277)Refutation not found, incomplete strategy % 252.72/36.51 % (3995277)------------------------------ % 252.72/36.51 % (3995277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.72/36.51 % (3995277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.72/36.51 % (3995277)CaDiCaL version: 2.1.3 % 252.72/36.51 % (3995277)Termination reason: Refutation not found, incomplete strategy % 252.72/36.51 % (3995277)Time elapsed: 0.011 s % 252.72/36.51 % (3995277)Peak memory usage: 88 MB % 252.72/36.51 % (3995277)Instructions burned: 20 (million) % 252.72/36.51 % (3995277)------------------------------ % 252.72/36.51 % (3995277)------------------------------ % 252.72/36.51 % Exception at run slice level % 252.72/36.51 User error: GNN currently only supports monomorphic FOL. % 252.72/36.51 % (3995280)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=1968659283:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2705 on theBenchmark for (2705ds/26509Mi) % 252.72/36.51 % (3995281)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=2331476053:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2704 on theBenchmark for (2704ds/28957Mi) % 252.72/36.51 % Exception at run slice level % 252.72/36.51 User error: GNN currently only supports monomorphic FOL. % 252.72/36.51 % (3995284)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=2780959137:i=29246:s2at=-1:kws=inv_arity:ins=10_2699 on theBenchmark for (2699ds/29246Mi) % 252.72/36.51 % Exception at run slice level % 252.72/36.51 User error: GNN currently only supports monomorphic FOL. % 252.72/36.51 % (3995286)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=3332752551:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2694 on theBenchmark for (2694ds/30082Mi) % 252.72/36.51 % (3995286)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 257.43/37.20 % Exception at run slice level % 257.43/37.20 User error: GNN currently only supports monomorphic FOL. % 257.43/37.20 % (3995288)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=539380161:i=32262:bd=preordered_2689 on theBenchmark for (2689ds/32262Mi) % 257.43/37.20 % Exception at run slice level % 257.43/37.20 User error: GNN currently only supports monomorphic FOL. % 257.43/37.20 % (3995076)Instruction limit reached! % 257.43/37.20 % (3995076)------------------------------ % 257.43/37.20 % (3995076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.43/37.20 % (3995076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.43/37.20 % (3995076)CaDiCaL version: 2.1.3 % 257.43/37.20 % (3995076)Termination reason: Instruction limit % 257.43/37.20 % (3995076)Termination phase: Saturation % 257.43/37.20 % (3995076)Time elapsed: 10.446 s % 257.43/37.20 % (3995076)Peak memory usage: 128 MB % 257.43/37.20 % (3995076)Instructions burned: 15999 (million) % 257.43/37.20 % (3995290)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=2509833508:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2684 on theBenchmark for (2684ds/32870Mi) % 257.43/37.20 % (3995291)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=1331287200:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2683 on theBenchmark for (2683ds/33295Mi) % 257.43/37.20 % Exception at run slice level % 257.43/37.20 User error: GNN currently only supports monomorphic FOL. % 257.43/37.20 % Exception at run slice level % 257.43/37.20 User error: GNN currently only supports monomorphic FOL. % 257.43/37.20 % (3995294)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=4193896875:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2678 on theBenchmark for (2678ds/36826Mi) % 257.43/37.20 % (3995295)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=4182457252:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2678 on theBenchmark for (2678ds/92981Mi) % 257.43/37.20 % Exception at run slice level % 257.43/37.20 User error: GNN currently only supports monomorphic FOL. % 257.43/37.20 % (3995298)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=4163740074:s2pl=on:i=49423_2673 on theBenchmark for (2673ds/49423Mi) % 257.43/37.20 % Exception at run slice level % 257.43/37.20 User error: GNN currently only supports monomorphic FOL. % 257.43/37.20 % (3995300)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=2903762743:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2667 on theBenchmark for (2667ds/57299Mi) % 257.43/37.20 % Exception at run slice level % 257.43/37.20 User error: GNN currently only supports monomorphic FOL. % 257.43/37.20 % (3995302)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=2222247549:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2662 on theBenchmark for (2662ds/127679Mi) % 257.43/37.20 % Exception at run slice level % 257.43/37.20 User error: GNN currently only supports monomorphic FOL. % 257.43/37.20 % (3995061)Instruction limit reached! % 257.43/37.20 % (3995061)------------------------------ % 257.43/37.20 % (3995061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.43/37.20 % (3995061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.43/37.20 % (3995061)CaDiCaL version: 2.1.3 % 257.43/37.20 % (3995061)Termination reason: Instruction limit % 257.43/37.20 % (3995061)Termination phase: Saturation % 257.43/37.20 % (3995061)Time elapsed: 14.998 s % 257.43/37.20 % (3995061)Peak memory usage: 228 MB % 257.43/37.20 % (3995061)Instructions burned: 19911 (million) % 257.43/37.20 % (3995304)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=2131680450:i=69402:add=on:aac=none:fsr=off_2657 on theBenchmark for (2657ds/69402Mi) % 257.43/37.20 % (3995306)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=2584820333:i=100512:doe=on:fgj=on:bd=all:fsd=on_2655 on theBenchmark for (2655ds/100512Mi) % 262.42/37.99 % (3995273)Instruction limit reached! % 262.42/37.99 % (3995273)------------------------------ % 262.42/37.99 % (3995273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.42/37.99 % (3995273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.42/37.99 % (3995273)CaDiCaL version: 2.1.3 % 262.42/37.99 % (3995273)Termination reason: Instruction limit % 262.42/37.99 % (3995273)Termination phase: Saturation % 262.42/37.99 % (3995273)Time elapsed: 5.772 s % 262.42/37.99 % (3995273)Peak memory usage: 183 MB % 262.42/37.99 % (3995273)Instructions burned: 21161 (million) % 262.42/37.99 % (3995308)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=1606510434:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2653 on theBenchmark for (2653ds/138761Mi) % 262.42/37.99 % Exception at run slice level % 262.42/37.99 User error: GNN currently only supports monomorphic FOL. % 262.42/37.99 % (3995310)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=2763372055:i=282386:rtra=on_2652 on theBenchmark for (2652ds/282386Mi) % 262.42/37.99 % Exception at run slice level % 262.42/37.99 User error: GNN currently only supports monomorphic FOL. % 262.42/37.99 % Exception at run slice level % 262.42/37.99 User error: GNN currently only supports monomorphic FOL. % 262.42/37.99 % (3995312)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=1359514187:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2650 on theBenchmark for (2650ds/269354Mi) % 262.42/37.99 % (3995313)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=3333205684:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2650 on theBenchmark for (2650ds/283390Mi) % 262.42/37.99 % (3995313)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 262.42/37.99 % Exception at run slice level % 262.42/37.99 User error: GNN currently only supports monomorphic FOL. % 262.42/37.99 % Exception at run slice level % 262.42/37.99 User error: GNN currently only supports monomorphic FOL. % 262.42/37.99 % (3995316)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=1557962359:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2647 on theBenchmark for (2647ds/218Mi) % 262.42/37.99 % (3995316)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 262.42/37.99 % (3995316)Refutation not found, incomplete strategy % 262.42/37.99 % (3995316)------------------------------ % 262.42/37.99 % (3995316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.42/37.99 % (3995316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.42/37.99 % (3995316)CaDiCaL version: 2.1.3 % 262.42/37.99 % (3995316)Termination reason: Refutation not found, incomplete strategy % 262.42/37.99 % (3995316)Time elapsed: 0.001 s % 262.42/37.99 % (3995316)Peak memory usage: 88 MB % 262.42/37.99 % (3995316)Instructions burned: 3 (million) % 262.42/37.99 % (3995317)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=121799391:i=238:av=off:rtra=on:ss=axioms_2646 on theBenchmark for (2646ds/238Mi) % 262.42/37.99 % Exception at run slice level % 262.42/37.99 User error: GNN currently only supports monomorphic FOL. % 262.42/37.99 % (3995316)------------------------------ % 262.42/37.99 % (3995316)------------------------------ % 262.42/37.99 % (3995317)Instruction limit reached! % 262.42/37.99 % (3995317)------------------------------ % 262.42/37.99 % (3995317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.42/37.99 % (3995317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.42/37.99 % (3995317)CaDiCaL version: 2.1.3 % 262.42/37.99 % (3995317)Termination reason: Instruction limit % 262.42/37.99 % (3995317)Termination phase: Saturation % 262.42/37.99 % (3995317)Time elapsed: 0.127 s % 262.42/37.99 % (3995317)Peak memory usage: 89 MB % 262.42/37.99 % (3995317)Instructions burned: 239 (million) % 262.42/37.99 % (3995320)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=4094934070:s2a=on:i=278:rtra=on:gtg=position_2644 on theBenchmark for (2644ds/278Mi) % 262.42/37.99 % (3995321)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=3430031321:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2644 on theBenchmark for (2644ds/258Mi) % 268.71/38.82 % (3995321)Instruction limit reached! % 268.71/38.82 % (3995321)------------------------------ % 268.71/38.82 % (3995321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.71/38.82 % (3995321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.71/38.82 % (3995321)CaDiCaL version: 2.1.3 % 268.71/38.82 % (3995321)Termination reason: Instruction limit % 268.71/38.82 % (3995321)Termination phase: Saturation % 268.71/38.82 % (3995321)Time elapsed: 0.067 s % 268.71/38.82 % (3995321)Peak memory usage: 90 MB % 268.71/38.82 % (3995321)Instructions burned: 261 (million) % 268.71/38.82 % (3995322)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=1848922974:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2643 on theBenchmark for (2643ds/570Mi) % 268.71/38.82 % (3995320)Instruction limit reached! % 268.71/38.82 % (3995320)------------------------------ % 268.71/38.82 % (3995320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.71/38.82 % (3995320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.71/38.82 % (3995320)CaDiCaL version: 2.1.3 % 268.71/38.82 % (3995320)Termination reason: Instruction limit % 268.71/38.82 % (3995320)Termination phase: Saturation % 268.71/38.82 % (3995320)Time elapsed: 0.171 s % 268.71/38.82 % (3995320)Peak memory usage: 90 MB % 268.71/38.82 % (3995320)Instructions burned: 279 (million) % 268.71/38.82 % (3995325)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=4255897908:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2642 on theBenchmark for (2642ds/314Mi) % 268.71/38.82 % (3995325)Instruction limit reached! % 268.71/38.82 % (3995325)------------------------------ % 268.71/38.82 % (3995325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.71/38.82 % (3995325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.71/38.82 % (3995325)CaDiCaL version: 2.1.3 % 268.71/38.82 % (3995325)Termination reason: Instruction limit % 268.71/38.82 % (3995325)Termination phase: Saturation % 268.71/38.82 % (3995325)Time elapsed: 0.093 s % 268.71/38.82 % (3995325)Peak memory usage: 90 MB % 268.71/38.82 % (3995325)Instructions burned: 316 (million) % 268.71/38.82 % (3995327)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=4137245307:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2641 on theBenchmark for (2641ds/650Mi) % 268.71/38.82 % (3995329)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=1375771610:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2640 on theBenchmark for (2640ds/496Mi) % 268.71/38.82 % (3995322)Instruction limit reached! % 268.71/38.82 % (3995322)------------------------------ % 268.71/38.82 % (3995322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.71/38.82 % (3995322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.71/38.82 % (3995322)CaDiCaL version: 2.1.3 % 268.71/38.82 % (3995322)Termination reason: Instruction limit % 268.71/38.82 % (3995322)Termination phase: Saturation % 268.71/38.82 % (3995322)Time elapsed: 0.339 s % 268.71/38.82 % (3995322)Peak memory usage: 93 MB % 268.71/38.82 % (3995322)Instructions burned: 570 (million) % 268.71/38.82 % (3995329)Instruction limit reached! % 268.71/38.82 % (3995329)------------------------------ % 268.71/38.82 % (3995329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.71/38.82 % (3995329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.71/38.82 % (3995329)CaDiCaL version: 2.1.3 % 268.71/38.82 % (3995329)Termination reason: Instruction limit % 268.71/38.82 % (3995329)Termination phase: Saturation % 268.71/38.82 % (3995329)Time elapsed: 0.138 s % 268.71/38.82 % (3995329)Peak memory usage: 92 MB % 268.71/38.82 % (3995329)Instructions burned: 500 (million) % 268.71/38.82 % (3995332)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=1826137204:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2638 on theBenchmark for (2638ds/588Mi) % 268.71/38.82 % (3995332)Refutation not found, incomplete strategy % 268.71/38.82 % (3995332)------------------------------ % 268.71/38.82 % (3995332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.71/38.82 % (3995332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.71/38.82 % (3995332)CaDiCaL version: 2.1.3 % 268.71/38.82 % (3995332)Termination reason: Refutation not found, incomplete strategy % 268.71/38.82 % (3995332)Time elapsed: 0.012 s % 268.71/38.82 % (3995332)Peak memory usage: 89 MB % 268.71/38.82 % (3995332)Instructions burned: 20 (million) % 268.71/38.82 % (3995333)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=3318143149:i=4700:rtra=on_2637 on theBenchmark for (2637ds/4700Mi) % 274.64/39.77 % (3995327)Instruction limit reached! % 274.64/39.77 % (3995327)------------------------------ % 274.64/39.77 % (3995327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.64/39.77 % (3995327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.64/39.77 % (3995327)CaDiCaL version: 2.1.3 % 274.64/39.77 % (3995327)Termination reason: Instruction limit % 274.64/39.77 % (3995327)Termination phase: Saturation % 274.64/39.77 % (3995327)Time elapsed: 0.367 s % 274.64/39.77 % (3995327)Peak memory usage: 93 MB % 274.64/39.77 % (3995327)Instructions burned: 650 (million) % 274.64/39.77 % (3995332)------------------------------ % 274.64/39.77 % (3995332)------------------------------ % 274.64/39.77 % (3995336)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=316854715:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2636 on theBenchmark for (2636ds/226Mi) % 274.64/39.77 % Exception at run slice level % 274.64/39.77 User error: GNN currently only supports monomorphic FOL. % 274.64/39.77 % (3995336)Instruction limit reached! % 274.64/39.77 % (3995336)------------------------------ % 274.64/39.77 % (3995336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.64/39.77 % (3995336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.64/39.77 % (3995336)CaDiCaL version: 2.1.3 % 274.64/39.77 % (3995336)Termination reason: Instruction limit % 274.64/39.77 % (3995336)Termination phase: Saturation % 274.64/39.77 % (3995336)Time elapsed: 0.132 s % 274.64/39.77 % (3995336)Peak memory usage: 90 MB % 274.64/39.77 % (3995336)Instructions burned: 227 (million) % 274.64/39.77 % (3995339)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=3407428081:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2634 on theBenchmark for (2634ds/228Mi) % 274.64/39.77 % (3995337)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1730899879:i=254:av=off:fsr=off:rtra=on:sup=off_2634 on theBenchmark for (2634ds/254Mi) % 274.64/39.77 % (3995337)Refutation not found, incomplete strategy % 274.64/39.77 % (3995337)------------------------------ % 274.64/39.77 % (3995337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.64/39.77 % (3995337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.64/39.77 % (3995337)CaDiCaL version: 2.1.3 % 274.64/39.77 % (3995337)Termination reason: Refutation not found, incomplete strategy % 274.64/39.77 % (3995337)Time elapsed: 0.011 s % 274.64/39.77 % (3995337)Peak memory usage: 88 MB % 274.64/39.77 % (3995337)Instructions burned: 20 (million) % 274.64/39.77 % (3995339)Instruction limit reached! % 274.64/39.77 % (3995339)------------------------------ % 274.64/39.77 % (3995339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.64/39.77 % (3995339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.64/39.77 % (3995339)CaDiCaL version: 2.1.3 % 274.64/39.77 % (3995339)Termination reason: Instruction limit % 274.64/39.77 % (3995339)Termination phase: Saturation % 274.64/39.77 % (3995339)Time elapsed: 0.068 s % 274.64/39.77 % (3995339)Peak memory usage: 89 MB % 274.64/39.77 % (3995339)Instructions burned: 231 (million) % 274.64/39.77 % (3995342)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=2451579150:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2633 on theBenchmark for (2633ds/1814Mi) % 274.64/39.77 % (3995343)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=2862481099:i=874:sd=1:aac=none:rtra=on:ss=included_2632 on theBenchmark for (2632ds/874Mi) % 274.64/39.77 % (3995343)Refutation not found, incomplete strategy % 274.64/39.77 % (3995343)------------------------------ % 274.64/39.77 % (3995343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.64/39.77 % (3995343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.64/39.77 % (3995343)CaDiCaL version: 2.1.3 % 274.64/39.77 % (3995343)Termination reason: Refutation not found, incomplete strategy % 274.64/39.77 % (3995343)Time elapsed: 0.008 s % 274.64/39.77 % (3995343)Peak memory usage: 89 MB % 274.64/39.77 % (3995343)Instructions burned: 26 (million) % 274.64/39.77 % (3995337)------------------------------ % 274.64/39.77 % (3995337)------------------------------ % 274.64/39.77 % (3995343)------------------------------ % 274.64/39.77 % (3995343)------------------------------ % 274.64/39.77 % (3995346)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=1687321070:i=10404:rtra=on:ss=axioms:sgt=16_2630 on theBenchmark for (2630ds/10404Mi) % 274.64/39.77 % (3995347)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2698709258:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2629 on theBenchmark for (2629ds/268Mi) % 280.96/40.52 % (3995347)Instruction limit reached! % 280.96/40.52 % (3995347)------------------------------ % 280.96/40.52 % (3995347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.96/40.52 % (3995347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.96/40.52 % (3995347)CaDiCaL version: 2.1.3 % 280.96/40.52 % (3995347)Termination reason: Instruction limit % 280.96/40.52 % (3995347)Termination phase: Saturation % 280.96/40.52 % (3995347)Time elapsed: 0.079 s % 280.96/40.52 % (3995347)Peak memory usage: 90 MB % 280.96/40.52 % (3995347)Instructions burned: 268 (million) % 280.96/40.52 % (3995350)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=2533259992:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2627 on theBenchmark for (2627ds/1184Mi) % 280.96/40.52 % (3995350)Refutation not found, incomplete strategy % 280.96/40.52 % (3995350)------------------------------ % 280.96/40.52 % (3995350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.96/40.52 % (3995350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.96/40.52 % (3995350)CaDiCaL version: 2.1.3 % 280.96/40.52 % (3995350)Termination reason: Refutation not found, incomplete strategy % 280.96/40.52 % (3995350)Time elapsed: 0.008 s % 280.96/40.52 % (3995350)Peak memory usage: 88 MB % 280.96/40.52 % (3995350)Instructions burned: 28 (million) % 280.96/40.52 % Exception at run slice level % 280.96/40.52 User error: GNN currently only supports monomorphic FOL. % 280.96/40.52 % (3995350)------------------------------ % 280.96/40.52 % (3995350)------------------------------ % 280.96/40.52 % (3995352)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=4019949639:st=3:i=26386:sd=3:rtra=on:ss=axioms_2625 on theBenchmark for (2625ds/26386Mi) % 280.96/40.52 % (3995353)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=2411335609:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2624 on theBenchmark for (2624ds/250Mi) % 280.96/40.52 % (3995353)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 280.96/40.52 % (3995353)Instruction limit reached! % 280.96/40.52 % (3995353)------------------------------ % 280.96/40.52 % (3995353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.96/40.52 % (3995353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.96/40.52 % (3995353)CaDiCaL version: 2.1.3 % 280.96/40.52 % (3995353)Termination reason: Instruction limit % 280.96/40.52 % (3995353)Termination phase: Saturation % 280.96/40.52 % (3995353)Time elapsed: 0.072 s % 280.96/40.52 % (3995353)Peak memory usage: 91 MB % 280.96/40.52 % (3995353)Instructions burned: 250 (million) % 280.96/40.52 % (3995356)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=285658087:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2622 on theBenchmark for (2622ds/268Mi) % 280.96/40.52 % Exception at run slice level % 280.96/40.52 User error: Immediate (shared) subterms of term/literal aa(X1,X0,combk(X0,X1,X3),X2) = sF76(X1,X0,X3,X2) have different types/not well-typed! % 280.96/40.52 % (3995342)Instruction limit reached! % 280.96/40.52 % (3995342)------------------------------ % 280.96/40.52 % (3995342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.96/40.52 % (3995342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.96/40.52 % (3995342)CaDiCaL version: 2.1.3 % 280.96/40.52 % (3995342)Termination reason: Instruction limit % 280.96/40.52 % (3995342)Termination phase: Saturation % 280.96/40.52 % (3995342)Time elapsed: 1.058 s % 280.96/40.52 % (3995342)Peak memory usage: 100 MB % 280.96/40.52 % (3995342)Instructions burned: 1815 (million) % 280.96/40.52 % (3995358)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2200382338:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2621 on theBenchmark for (2621ds/282Mi) % 280.96/40.52 % (3995358)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 280.96/40.52 % (3995358)Refutation not found, incomplete strategy % 280.96/40.52 % (3995358)------------------------------ % 280.96/40.52 % (3995358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.96/40.52 % (3995358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.79/42.73 % (3995358)CaDiCaL version: 2.1.3 % 295.79/42.73 % (3995358)Termination reason: Refutation not found, incomplete strategy % 295.79/42.73 % (3995358)Time elapsed: 0.002 s % 295.79/42.73 % (3995358)Peak memory usage: 88 MB % 295.79/42.73 % (3995358)Instructions burned: 3 (million) % 295.79/42.73 % Exception at run slice level % 295.79/42.73 User error: GNN currently only supports monomorphic FOL. % 295.79/42.73 % (3995359)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=384178279:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2620 on theBenchmark for (2620ds/862Mi) % 295.79/42.73 % (3995359)Refutation not found, incomplete strategy % 295.79/42.73 % (3995359)------------------------------ % 295.79/42.73 % (3995359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.79/42.73 % (3995359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.79/42.73 % (3995359)CaDiCaL version: 2.1.3 % 295.79/42.73 % (3995359)Termination reason: Refutation not found, incomplete strategy % 295.79/42.73 % (3995359)Time elapsed: 0.012 s % 295.79/42.73 % (3995359)Peak memory usage: 89 MB % 295.79/42.73 % (3995359)Instructions burned: 21 (million) % 295.79/42.73 % (3995358)------------------------------ % 295.79/42.73 % (3995358)------------------------------ % 295.79/42.73 % (3995361)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=731139369:i=12120:aac=none:ins=25:rtra=on_2619 on theBenchmark for (2619ds/12120Mi) % 295.79/42.73 % (3995363)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=2898122777:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2618 on theBenchmark for (2618ds/300Mi) % 295.79/42.73 % (3995363)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 295.79/42.73 % (3995359)------------------------------ % 295.79/42.73 % (3995359)------------------------------ % 295.79/42.73 % (3995363)Instruction limit reached! % 295.79/42.73 % (3995363)------------------------------ % 295.79/42.73 % (3995363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.79/42.73 % (3995363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.79/42.73 % (3995363)CaDiCaL version: 2.1.3 % 295.79/42.73 % (3995363)Termination reason: Instruction limit % 295.79/42.73 % (3995363)Termination phase: Saturation % 295.79/42.73 % (3995363)Time elapsed: 0.083 s % 295.79/42.73 % (3995363)Peak memory usage: 91 MB % 295.79/42.73 % (3995363)Instructions burned: 304 (million) % 295.79/42.73 % (3995366)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=484423793:i=28310:bd=all:rtra=on_2616 on theBenchmark for (2616ds/28310Mi) % 295.79/42.73 % (3995367)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=387587376:i=1334:av=off:fsr=off:rtra=on_2616 on theBenchmark for (2616ds/1334Mi) % 295.79/42.73 % Exception at run slice level % 295.79/42.73 User error: GNN currently only supports monomorphic FOL. % 295.79/42.73 % Exception at run slice level % 295.79/42.73 User error: GNN currently only supports monomorphic FOL. % 295.79/42.73 % (3995370)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=1608717714:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2614 on theBenchmark for (2614ds/370Mi) % 295.79/42.73 % (3995371)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=4119547860:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2613 on theBenchmark for (2613ds/386Mi) % 295.79/42.73 % (3995371)Instruction limit reached! % 295.79/42.73 % (3995371)------------------------------ % 295.79/42.73 % (3995371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.79/42.73 % (3995371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.79/42.73 % (3995371)CaDiCaL version: 2.1.3 % 295.79/42.73 % (3995371)Termination reason: Instruction limit % 295.79/42.73 % (3995371)Termination phase: Saturation % 295.79/42.73 % (3995371)Time elapsed: 0.102 s % 295.79/42.73 % (3995371)Peak memory usage: 89 MB % 295.79/42.73 % (3995371)Instructions burned: 388 (million) % 295.79/42.73 % (3995370)Instruction limit reached! % 295.79/42.73 % (3995370)------------------------------ % 295.79/42.73 % (3995370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.79/42.73 % (3995370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3Terminated %------------------------------------------------------------------------------