%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW563_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n013.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:49 PM UTC 2026 % Result : Timeout 288.66s 41.70s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW563_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.19 % Computer : n013.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 14:18:06 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.23 Running first-order theorem proving % 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.83/1.69 % (1210044)Detected formulas, will run a generic FOF schedule. % 5.83/1.69 % (1210160)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=3767551590:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 5.83/1.69 % (1210160)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.83/1.69 % (1210158)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=3980897828:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 5.83/1.69 % (1210163)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=855824594:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 5.83/1.69 % (1210164)dis-21_1_sil=8000:lcm=predicate:random_seed=285118696:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 5.83/1.69 % (1210159)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=311396952:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 5.83/1.69 % (1210162)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2362562617:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 5.83/1.69 % (1210161)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=51362485:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 5.83/1.69 % (1210161)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.83/1.69 % (1210161)Refutation not found, incomplete strategy % 5.83/1.69 % (1210161)------------------------------ % 5.83/1.69 % (1210161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.83/1.69 % (1210161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.83/1.69 % (1210161)CaDiCaL version: 2.1.3 % 5.83/1.69 % (1210161)Termination reason: Refutation not found, incomplete strategy % 5.83/1.69 % (1210161)Time elapsed: 0.002 s % 5.83/1.69 % (1210161)Peak memory usage: 88 MB % 5.83/1.69 % (1210161)Instructions burned: 2 (million) % 5.83/1.69 % (1210164)Instruction limit reached! % 5.83/1.69 % (1210164)------------------------------ % 5.83/1.69 % (1210164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.83/1.69 % (1210164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.83/1.69 % (1210164)CaDiCaL version: 2.1.3 % 5.83/1.69 % (1210164)Termination reason: Instruction limit % 5.83/1.69 % (1210164)Termination phase: Saturation % 5.83/1.69 % (1210164)Time elapsed: 0.055 s % 5.83/1.69 % (1210164)Peak memory usage: 88 MB % 5.83/1.69 % (1210164)Instructions burned: 130 (million) % 5.83/1.69 % (1210163)Instruction limit reached! % 5.83/1.69 % (1210163)------------------------------ % 5.83/1.69 % (1210163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.83/1.69 % (1210163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.83/1.69 % (1210163)CaDiCaL version: 2.1.3 % 5.83/1.69 % (1210163)Termination reason: Instruction limit % 5.83/1.69 % (1210163)Termination phase: Saturation % 5.83/1.69 % (1210163)Time elapsed: 0.056 s % 5.83/1.69 % (1210163)Peak memory usage: 88 MB % 5.83/1.69 % (1210163)Instructions burned: 141 (million) % 5.83/1.69 % (1210162)Instruction limit reached! % 5.83/1.69 % (1210162)------------------------------ % 5.83/1.69 % (1210162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.83/1.69 % (1210162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.83/1.69 % (1210162)CaDiCaL version: 2.1.3 % 5.83/1.69 % (1210162)Termination reason: Instruction limit % 5.83/1.69 % (1210162)Termination phase: Saturation % 5.83/1.69 % (1210162)Time elapsed: 0.070 s % 5.83/1.69 % (1210162)Peak memory usage: 88 MB % 5.83/1.69 % (1210162)Instructions burned: 120 (million) % 5.83/1.69 % Exception at run slice level % 5.83/1.69 User error: GNN currently only supports monomorphic FOL. % 5.83/1.69 % (1210172)lrs+10_1_sil=8000:sp=occurrence:random_seed=1611914800:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 5.83/1.69 % (1210173)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1259253334:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 5.83/1.69 % (1210174)lrs+1011_1_sil=32000:sp=occurrence:random_seed=343684225:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 6.83/1.86 % (1210173)Instruction limit reached! % 6.83/1.86 % (1210173)------------------------------ % 6.83/1.86 % (1210173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.83/1.86 % (1210173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.86 % (1210173)CaDiCaL version: 2.1.3 % 6.83/1.86 % (1210173)Termination reason: Instruction limit % 6.83/1.86 % (1210173)Termination phase: Saturation % 6.83/1.86 % (1210173)Time elapsed: 0.063 s % 6.83/1.86 % (1210173)Peak memory usage: 88 MB % 6.83/1.86 % (1210173)Instructions burned: 160 (million) % 6.83/1.86 % (1210175)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=1962050807:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi) % 6.83/1.86 % (1210161)------------------------------ % 6.83/1.86 % (1210161)------------------------------ % 6.83/1.86 % (1210175)Instruction limit reached! % 6.83/1.86 % (1210175)------------------------------ % 6.83/1.86 % (1210175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.83/1.86 % (1210175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.86 % (1210175)CaDiCaL version: 2.1.3 % 6.83/1.86 % (1210175)Termination reason: Instruction limit % 6.83/1.86 % (1210175)Termination phase: Saturation % 6.83/1.86 % (1210175)Time elapsed: 0.072 s % 6.83/1.86 % (1210175)Peak memory usage: 90 MB % 6.83/1.86 % (1210175)Instructions burned: 250 (million) % 6.83/1.86 % (1210172)Instruction limit reached! % 6.83/1.86 % (1210172)------------------------------ % 6.83/1.86 % (1210172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.83/1.86 % (1210172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.86 % (1210172)CaDiCaL version: 2.1.3 % 6.83/1.86 % (1210172)Termination reason: Instruction limit % 6.83/1.86 % (1210172)Termination phase: Saturation % 6.83/1.86 % (1210172)Time elapsed: 0.166 s % 6.83/1.86 % (1210172)Peak memory usage: 90 MB % 6.83/1.86 % (1210172)Instructions burned: 286 (million) % 6.83/1.86 % Exception at run slice level % 6.83/1.86 User error: GNN currently only supports monomorphic FOL. % 6.83/1.86 % Exception at run slice level % 6.83/1.86 User error: GNN currently only supports monomorphic FOL. % 6.83/1.86 % (1210181)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3005442760:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 6.83/1.86 % (1210180)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2048364522:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi) % 6.83/1.86 % (1210174)Instruction limit reached! % 6.83/1.86 % (1210174)------------------------------ % 6.83/1.86 % (1210174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.83/1.86 % (1210174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.86 % (1210174)CaDiCaL version: 2.1.3 % 6.83/1.86 % (1210174)Termination reason: Instruction limit % 6.83/1.86 % (1210174)Termination phase: Saturation % 6.83/1.86 % (1210174)Time elapsed: 0.189 s % 6.83/1.86 % (1210174)Peak memory usage: 90 MB % 6.83/1.86 % (1210174)Instructions burned: 325 (million) % 6.83/1.86 % (1210182)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2157577946:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi) % 6.83/1.86 % (1210182)Refutation not found, incomplete strategy % 6.83/1.86 % (1210182)------------------------------ % 6.83/1.86 % (1210182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.83/1.86 % (1210182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.86 % (1210182)CaDiCaL version: 2.1.3 % 6.83/1.86 % (1210182)Termination reason: Refutation not found, incomplete strategy % 6.83/1.86 % (1210182)Time elapsed: 0.035 s % 6.83/1.86 % (1210182)Peak memory usage: 89 MB % 6.83/1.86 % (1210182)Instructions burned: 38 (million) % 6.83/1.86 % (1210183)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1684017484:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi) % 6.83/1.86 % (1210185)lrs+10_1_sil=8000:sp=occurrence:random_seed=1831940274:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 6.83/1.86 % (1210184)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3216048203:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 6.83/1.86 % (1210188)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=137406931:i=437:sd=1:aac=none:ss=included_2994 on theBenchmark for (2994ds/437Mi) % 10.74/2.30 % (1210180)Instruction limit reached! % 10.74/2.30 % (1210180)------------------------------ % 10.74/2.30 % (1210180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.74/2.30 % (1210180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.74/2.30 % (1210180)CaDiCaL version: 2.1.3 % 10.74/2.30 % (1210180)Termination reason: Instruction limit % 10.74/2.30 % (1210180)Termination phase: Saturation % 10.74/2.30 % (1210180)Time elapsed: 0.149 s % 10.74/2.30 % (1210180)Peak memory usage: 89 MB % 10.74/2.30 % (1210180)Instructions burned: 295 (million) % 10.74/2.30 % (1210183)Instruction limit reached! % 10.74/2.30 % (1210183)------------------------------ % 10.74/2.30 % (1210183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.74/2.30 % (1210183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.74/2.30 % (1210183)CaDiCaL version: 2.1.3 % 10.74/2.30 % (1210183)Termination reason: Instruction limit % 10.74/2.30 % (1210183)Termination phase: Saturation % 10.74/2.30 % (1210183)Time elapsed: 0.063 s % 10.74/2.30 % (1210183)Peak memory usage: 88 MB % 10.74/2.30 % (1210183)Instructions burned: 128 (million) % 10.74/2.30 % (1210184)Instruction limit reached! % 10.74/2.30 % (1210184)------------------------------ % 10.74/2.30 % (1210184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.74/2.30 % (1210184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.74/2.30 % (1210184)CaDiCaL version: 2.1.3 % 10.74/2.30 % (1210184)Termination reason: Instruction limit % 10.74/2.30 % (1210184)Termination phase: Saturation % 10.74/2.30 % (1210184)Time elapsed: 0.065 s % 10.74/2.30 % (1210184)Peak memory usage: 89 MB % 10.74/2.30 % (1210184)Instructions burned: 114 (million) % 10.74/2.30 % (1210182)------------------------------ % 10.74/2.30 % (1210182)------------------------------ % 10.74/2.30 % (1210195)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3231675678:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2993 on theBenchmark for (2993ds/134Mi) % 10.74/2.30 % (1210194)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3826860564:i=5202:ss=axioms:sgt=16_2993 on theBenchmark for (2993ds/5202Mi) % 10.74/2.30 % (1210196)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2913585700:st=8:i=592:sd=3:ep=RST:ss=axioms_2992 on theBenchmark for (2992ds/592Mi) % 10.74/2.30 % (1210188)Instruction limit reached! % 10.74/2.30 % (1210188)------------------------------ % 10.74/2.30 % (1210188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.74/2.30 % (1210188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.74/2.30 % (1210188)CaDiCaL version: 2.1.3 % 10.74/2.30 % (1210188)Termination reason: Instruction limit % 10.74/2.30 % (1210188)Termination phase: Saturation % 10.74/2.30 % (1210188)Time elapsed: 0.185 s % 10.74/2.30 % (1210188)Peak memory usage: 89 MB % 10.74/2.30 % (1210188)Instructions burned: 437 (million) % 10.74/2.30 % (1210197)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4099964356:st=3:i=13193:sd=3:ss=axioms_2992 on theBenchmark for (2992ds/13193Mi) % 10.74/2.30 % (1210195)Instruction limit reached! % 10.74/2.30 % (1210195)------------------------------ % 10.74/2.30 % (1210195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.74/2.30 % (1210195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.74/2.30 % (1210195)CaDiCaL version: 2.1.3 % 10.74/2.30 % (1210195)Termination reason: Instruction limit % 10.74/2.30 % (1210195)Termination phase: Saturation % 10.74/2.30 % (1210195)Time elapsed: 0.075 s % 10.74/2.30 % (1210195)Peak memory usage: 89 MB % 10.74/2.30 % (1210195)Instructions burned: 134 (million) % 10.74/2.30 % Exception at run slice level % 10.74/2.30 User error: GNN currently only supports monomorphic FOL. % 10.74/2.30 % (1210202)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=4146529331:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/125Mi) % 10.74/2.30 % (1210202)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.74/2.30 % (1210203)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2028538643:i=134:gtgl=5:slsql=off:gtg=exists_sym_2991 on theBenchmark for (2991ds/134Mi) % 10.74/2.30 % Exception at run slice level % 14.18/2.94 User error: Immediate (shared) subterms of term/literal product_prod_rec(X0,X2,X1,X5,product_Pair(X0,X2,X4,X3)) = sF82(X0,X2,X1,X5,X4,X3) have different types/not well-typed! % 14.18/2.94 % (1210204)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2177461995:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/141Mi) % 14.18/2.94 % (1210204)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 14.18/2.94 % (1210204)Refutation not found, incomplete strategy % 14.18/2.94 % (1210204)------------------------------ % 14.18/2.94 % (1210204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.18/2.94 % (1210204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.18/2.94 % (1210204)CaDiCaL version: 2.1.3 % 14.18/2.94 % (1210204)Termination reason: Refutation not found, incomplete strategy % 14.18/2.94 % (1210204)Time elapsed: 0.003 s % 14.18/2.94 % (1210204)Peak memory usage: 88 MB % 14.18/2.94 % (1210204)Instructions burned: 3 (million) % 14.18/2.94 % (1210202)Instruction limit reached! % 14.18/2.94 % (1210202)------------------------------ % 14.18/2.94 % (1210202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.18/2.94 % (1210202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.18/2.94 % (1210202)CaDiCaL version: 2.1.3 % 14.18/2.94 % (1210202)Termination reason: Instruction limit % 14.18/2.94 % (1210202)Termination phase: Saturation % 14.18/2.94 % (1210202)Time elapsed: 0.073 s % 14.18/2.94 % (1210202)Peak memory usage: 90 MB % 14.18/2.94 % (1210202)Instructions burned: 126 (million) % 14.18/2.94 % Exception at run slice level % 14.18/2.94 User error: GNN currently only supports monomorphic FOL. % 14.18/2.94 % (1210196)Instruction limit reached! % 14.18/2.94 % (1210196)------------------------------ % 14.18/2.94 % (1210196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.18/2.94 % (1210196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.18/2.94 % (1210196)CaDiCaL version: 2.1.3 % 14.18/2.94 % (1210196)Termination reason: Instruction limit % 14.18/2.94 % (1210196)Termination phase: Saturation % 14.18/2.94 % (1210196)Time elapsed: 0.228 s % 14.18/2.94 % (1210196)Peak memory usage: 89 MB % 14.18/2.94 % (1210196)Instructions burned: 595 (million) % 14.18/2.94 % (1210210)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=2336609197:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2989 on theBenchmark for (2989ds/150Mi) % 14.18/2.94 % (1210210)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 14.18/2.94 % (1210207)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=113804894:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/431Mi) % 14.18/2.94 % (1210185)Instruction limit reached! % 14.18/2.94 % (1210185)------------------------------ % 14.18/2.94 % (1210185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.18/2.94 % (1210185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.18/2.94 % (1210185)CaDiCaL version: 2.1.3 % 14.18/2.94 % (1210185)Termination reason: Instruction limit % 14.18/2.94 % (1210185)Termination phase: Saturation % 14.18/2.94 % (1210185)Time elapsed: 0.527 s % 14.18/2.94 % (1210185)Peak memory usage: 95 MB % 14.18/2.94 % (1210185)Instructions burned: 908 (million) % 14.18/2.94 % (1210209)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=739496436:i=6060:aac=none:ins=25_2989 on theBenchmark for (2989ds/6060Mi) % 14.18/2.94 % Exception at run slice level % 14.18/2.94 User error: GNN currently only supports monomorphic FOL. % 14.18/2.94 % (1210210)Instruction limit reached! % 14.18/2.94 % (1210210)------------------------------ % 14.18/2.94 % (1210210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.18/2.94 % (1210210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.18/2.94 % (1210210)CaDiCaL version: 2.1.3 % 14.18/2.94 % (1210210)Termination reason: Instruction limit % 14.18/2.94 % (1210210)Termination phase: Saturation % 14.18/2.94 % (1210210)Time elapsed: 0.050 s % 14.18/2.94 % (1210210)Peak memory usage: 90 MB % 14.18/2.94 % (1210210)Instructions burned: 150 (million) % 14.18/2.94 % (1210211)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1082711632:i=14155:bd=all_2989 on theBenchmark for (2989ds/14155Mi) % 21.22/3.91 % (1210218)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3636350320:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2988 on theBenchmark for (2988ds/193Mi) % 21.22/3.91 % (1210204)------------------------------ % 21.22/3.91 % (1210204)------------------------------ % 21.22/3.91 % (1210215)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3717552840:i=667:av=off:fsr=off_2988 on theBenchmark for (2988ds/667Mi) % 21.22/3.91 % (1210217)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=3892624362:s2a=on:i=185:s2at=1.8:fdi=4_2988 on theBenchmark for (2988ds/185Mi) % 21.22/3.91 % (1210218)Instruction limit reached! % 21.22/3.91 % (1210218)------------------------------ % 21.22/3.91 % (1210218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.22/3.91 % (1210218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.22/3.91 % (1210218)CaDiCaL version: 2.1.3 % 21.22/3.91 % (1210218)Termination reason: Instruction limit % 21.22/3.91 % (1210218)Termination phase: Saturation % 21.22/3.91 % (1210218)Time elapsed: 0.063 s % 21.22/3.91 % (1210218)Peak memory usage: 90 MB % 21.22/3.91 % (1210218)Instructions burned: 194 (million) % 21.22/3.91 % (1210207)Instruction limit reached! % 21.22/3.91 % (1210207)------------------------------ % 21.22/3.91 % (1210207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.22/3.91 % (1210207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.22/3.91 % (1210207)CaDiCaL version: 2.1.3 % 21.22/3.91 % (1210207)Termination reason: Instruction limit % 21.22/3.91 % (1210207)Termination phase: Saturation % 21.22/3.91 % (1210207)Time elapsed: 0.209 s % 21.22/3.91 % (1210207)Peak memory usage: 90 MB % 21.22/3.91 % (1210207)Instructions burned: 432 (million) % 21.22/3.91 % (1210223)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3036372014:i=12111:sd=1:ss=included_2986 on theBenchmark for (2986ds/12111Mi) % 21.22/3.91 % (1210220)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=729945578:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2987 on theBenchmark for (2987ds/4850Mi) % 21.22/3.91 % (1210217)Instruction limit reached! % 21.22/3.91 % (1210217)------------------------------ % 21.22/3.91 % (1210217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.22/3.91 % (1210217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.22/3.91 % (1210217)CaDiCaL version: 2.1.3 % 21.22/3.91 % (1210217)Termination reason: Instruction limit % 21.22/3.91 % (1210217)Termination phase: Saturation % 21.22/3.91 % (1210217)Time elapsed: 0.111 s % 21.22/3.91 % (1210217)Peak memory usage: 90 MB % 21.22/3.91 % (1210217)Instructions burned: 185 (million) % 21.22/3.91 % (1210224)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=23136705:i=319:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/319Mi) % 21.22/3.91 % Exception at run slice level % 21.22/3.91 User error: GNN currently only supports monomorphic FOL. % 21.22/3.91 % Exception at run slice level % 21.22/3.91 User error: GNN currently only supports monomorphic FOL. % 21.22/3.91 % (1210227)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3703541076:i=2064:ep=RST_2985 on theBenchmark for (2985ds/2064Mi) % 21.22/3.91 % (1210215)Instruction limit reached! % 21.22/3.91 % (1210215)------------------------------ % 21.22/3.91 % (1210215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.22/3.91 % (1210215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.22/3.91 % (1210215)CaDiCaL version: 2.1.3 % 21.22/3.91 % (1210215)Termination reason: Instruction limit % 21.22/3.91 % (1210215)Termination phase: Saturation % 21.22/3.91 % (1210215)Time elapsed: 0.306 s % 21.22/3.91 % (1210215)Peak memory usage: 92 MB % 21.22/3.91 % (1210215)Instructions burned: 668 (million) % 21.22/3.91 % Exception at run slice level % 21.22/3.91 User error: GNN currently only supports monomorphic FOL. % 21.22/3.91 % (1210224)Instruction limit reached! % 21.22/3.91 % (1210224)------------------------------ % 21.22/3.91 % (1210224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.22/3.91 % (1210224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.20/4.70 % (1210224)CaDiCaL version: 2.1.3 % 27.20/4.70 % (1210224)Termination reason: Instruction limit % 27.20/4.70 % (1210224)Termination phase: Saturation % 27.20/4.70 % (1210224)Time elapsed: 0.123 s % 27.20/4.70 % (1210224)Peak memory usage: 89 MB % 27.20/4.70 % (1210224)Instructions burned: 321 (million) % 27.20/4.70 % (1210229)dis-1011_128_sil=32000:random_seed=2223745283:i=3706:ep=RST:av=off_2984 on theBenchmark for (2984ds/3706Mi) % 27.20/4.70 % (1210231)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2076040290:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2984 on theBenchmark for (2984ds/757Mi) % 27.20/4.70 % (1210233)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3684327678:i=9925:aac=none_2983 on theBenchmark for (2983ds/9925Mi) % 27.20/4.70 % (1210232)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4203396519:i=13913:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/13913Mi) % 27.20/4.70 % (1210234)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1403572685:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2983 on theBenchmark for (2983ds/2479Mi) % 27.20/4.70 % (1210234)Refutation not found, incomplete strategy % 27.20/4.70 % (1210234)------------------------------ % 27.20/4.70 % (1210234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.20/4.70 % (1210234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.20/4.70 % (1210234)CaDiCaL version: 2.1.3 % 27.20/4.70 % (1210234)Termination reason: Refutation not found, incomplete strategy % 27.20/4.70 % (1210234)Time elapsed: 0.006 s % 27.20/4.70 % (1210234)Peak memory usage: 88 MB % 27.20/4.70 % (1210234)Instructions burned: 9 (million) % 27.20/4.70 % Exception at run slice level % 27.20/4.70 User error: GNN currently only supports monomorphic FOL. % 27.20/4.70 % (1210240)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=128016243:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/440Mi) % 27.20/4.70 % (1210240)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 27.20/4.70 % (1210234)------------------------------ % 27.20/4.70 % (1210234)------------------------------ % 27.20/4.70 % Exception at run slice level % 27.20/4.70 User error: GNN currently only supports monomorphic FOL. % 27.20/4.70 % (1210240)Instruction limit reached! % 27.20/4.70 % (1210240)------------------------------ % 27.20/4.70 % (1210240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.20/4.70 % (1210240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.20/4.70 % (1210240)CaDiCaL version: 2.1.3 % 27.20/4.70 % (1210240)Termination reason: Instruction limit % 27.20/4.70 % (1210240)Termination phase: Saturation % 27.20/4.70 % (1210240)Time elapsed: 0.130 s % 27.20/4.70 % (1210240)Peak memory usage: 93 MB % 27.20/4.70 % (1210240)Instructions burned: 441 (million) % 27.20/4.70 % (1210242)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3858237045:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2979 on theBenchmark for (2979ds/11145Mi) % 27.20/4.70 % (1210231)Instruction limit reached! % 27.20/4.70 % (1210231)------------------------------ % 27.20/4.70 % (1210231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.20/4.70 % (1210231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.20/4.70 % (1210231)CaDiCaL version: 2.1.3 % 27.20/4.70 % (1210231)Termination reason: Instruction limit % 27.20/4.70 % (1210231)Termination phase: Saturation % 27.20/4.70 % (1210231)Time elapsed: 0.478 s % 27.20/4.70 % (1210231)Peak memory usage: 93 MB % 27.20/4.70 % (1210231)Instructions burned: 757 (million) % 27.20/4.70 % (1210244)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2857485430:st=2:s2a=on:i=524:s2at=2:ss=axioms_2978 on theBenchmark for (2978ds/524Mi) % 27.20/4.70 % (1210243)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=1520065860:cts=off:i=3034:av=off:er=known:fsd=on_2978 on theBenchmark for (2978ds/3034Mi) % 27.20/4.70 % (1210227)Instruction limit reached! % 27.20/4.70 % (1210227)------------------------------ % 27.20/4.70 % (1210227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.20/4.70 % (1210227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.20/4.70 % (1210227)CaDiCaL version: 2.1.3 % 32.12/5.24 % (1210227)Termination reason: Instruction limit % 32.12/5.24 % (1210227)Termination phase: Saturation % 32.12/5.24 % (1210227)Time elapsed: 0.705 s % 32.12/5.24 % (1210227)Peak memory usage: 89 MB % 32.12/5.24 % (1210227)Instructions burned: 2066 (million) % 32.12/5.24 % (1210246)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1675435920:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2978 on theBenchmark for (2978ds/1016Mi) % 32.12/5.24 % (1210244)Instruction limit reached! % 32.12/5.24 % (1210244)------------------------------ % 32.12/5.24 % (1210244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.12/5.24 % (1210244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.12/5.24 % (1210244)CaDiCaL version: 2.1.3 % 32.12/5.24 % (1210244)Termination reason: Instruction limit % 32.12/5.24 % (1210244)Termination phase: Saturation % 32.12/5.24 % (1210244)Time elapsed: 0.138 s % 32.12/5.24 % (1210244)Peak memory usage: 91 MB % 32.12/5.24 % (1210244)Instructions burned: 526 (million) % 32.12/5.24 % (1210249)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=44535322:i=14123:bd=preordered:ins=4_2977 on theBenchmark for (2977ds/14123Mi) % 32.12/5.24 % (1210251)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3666950255:i=5781:kws=precedence:bd=all:rawr=on_2976 on theBenchmark for (2976ds/5781Mi) % 32.12/5.24 % Exception at run slice level % 32.12/5.24 User error: GNN currently only supports monomorphic FOL. % 32.12/5.24 % Exception at run slice level % 32.12/5.24 User error: GNN currently only supports monomorphic FOL. % 32.12/5.24 % (1210254)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=3405733804:i=2448:gtgl=5:bd=preordered:gtg=all_2974 on theBenchmark for (2974ds/2448Mi) % 32.12/5.24 % (1210246)Instruction limit reached! % 32.12/5.24 % (1210246)------------------------------ % 32.12/5.24 % (1210246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.12/5.24 % (1210246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.12/5.24 % (1210246)CaDiCaL version: 2.1.3 % 32.12/5.24 % (1210246)Termination reason: Instruction limit % 32.12/5.24 % (1210246)Termination phase: Saturation % 32.12/5.24 % (1210246)Time elapsed: 0.400 s % 32.12/5.24 % (1210246)Peak memory usage: 90 MB % 32.12/5.24 % (1210246)Instructions burned: 1017 (million) % 32.12/5.24 % (1210255)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=951800918:i=3223:kws=precedence:fgj=on:av=off_2973 on theBenchmark for (2973ds/3223Mi) % 32.12/5.24 % Exception at run slice level % 32.12/5.24 User error: GNN currently only supports monomorphic FOL. % 32.12/5.24 % (1210257)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2726082404:st=5.6:i=2033:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/2033Mi) % 32.12/5.24 % (1210229)Instruction limit reached! % 32.12/5.24 % (1210229)------------------------------ % 32.12/5.24 % (1210229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.12/5.24 % (1210229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.12/5.24 % (1210229)CaDiCaL version: 2.1.3 % 32.12/5.24 % (1210229)Termination reason: Instruction limit % 32.12/5.24 % (1210229)Termination phase: Saturation % 32.12/5.24 % (1210229)Time elapsed: 1.237 s % 32.12/5.24 % (1210229)Peak memory usage: 88 MB % 32.12/5.24 % (1210229)Instructions burned: 3708 (million) % 32.12/5.24 % (1210259)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1723808113:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2972 on theBenchmark for (2972ds/2055Mi) % 32.12/5.24 % Exception at run slice level % 32.12/5.24 User error: GNN currently only supports monomorphic FOL. % 32.12/5.24 % (1210261)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=4290603267:i=21611:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/21611Mi) % 32.12/5.24 % Exception at run slice level % 32.12/5.24 User error: GNN currently only supports monomorphic FOL. % 32.12/5.24 % (1210263)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2442360266:i=4835:sd=13:ss=axioms:sgt=23_2970 on theBenchmark for (2970ds/4835Mi) % 32.12/5.24 % Exception at run slice level % 32.12/5.24 User error: GNN currently only supports monomorphic FOL. % 32.12/5.24 % (1210265)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=1697811189:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2968 on theBenchmark for (2968ds/797Mi) % 38.69/6.15 % Exception at run slice level % 38.69/6.15 User error: GNN currently only supports monomorphic FOL. % 38.69/6.15 % (1210267)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=43170334:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2968 on theBenchmark for (2968ds/2326Mi) % 38.69/6.15 % (1210267)Refutation not found, incomplete strategy % 38.69/6.15 % (1210267)------------------------------ % 38.69/6.15 % (1210267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.69/6.15 % (1210267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.69/6.15 % (1210267)CaDiCaL version: 2.1.3 % 38.69/6.15 % (1210267)Termination reason: Refutation not found, incomplete strategy % 38.69/6.15 % (1210267)Time elapsed: 0.019 s % 38.69/6.15 % (1210267)Peak memory usage: 89 MB % 38.69/6.15 % (1210267)Instructions burned: 32 (million) % 38.69/6.15 % Exception at run slice level % 38.69/6.15 User error: GNN currently only supports monomorphic FOL. % 38.69/6.15 % (1210220)Instruction limit reached! % 38.69/6.15 % (1210220)------------------------------ % 38.69/6.15 % (1210220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.69/6.15 % (1210220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.69/6.15 % (1210220)CaDiCaL version: 2.1.3 % 38.69/6.15 % (1210220)Termination reason: Instruction limit % 38.69/6.15 % (1210220)Termination phase: Saturation % 38.69/6.15 % (1210220)Time elapsed: 1.965 s % 38.69/6.15 % (1210220)Peak memory usage: 95 MB % 38.69/6.15 % (1210220)Instructions burned: 4852 (million) % 38.69/6.15 % (1210269)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1364586267:i=6038:nm=6_2967 on theBenchmark for (2967ds/6038Mi) % 38.69/6.15 % (1210272)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3432836980:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2966 on theBenchmark for (2966ds/1008Mi) % 38.69/6.15 % (1210271)lrs+10_1_sil=32000:sp=occurrence:random_seed=736402513:st=2:i=33334:sd=3:ss=included:sgt=32_2966 on theBenchmark for (2966ds/33334Mi) % 38.69/6.15 % (1210267)------------------------------ % 38.69/6.15 % (1210267)------------------------------ % 38.69/6.15 % (1210265)Instruction limit reached! % 38.69/6.15 % (1210265)------------------------------ % 38.69/6.15 % (1210265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.69/6.15 % (1210265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.69/6.15 % (1210265)CaDiCaL version: 2.1.3 % 38.69/6.15 % (1210265)Termination reason: Instruction limit % 38.69/6.15 % (1210265)Termination phase: Saturation % 38.69/6.15 % (1210265)Time elapsed: 0.441 s % 38.69/6.15 % (1210265)Peak memory usage: 95 MB % 38.69/6.15 % (1210265)Instructions burned: 798 (million) % 38.69/6.15 % (1210276)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=2526693656:i=8327:s2at=5:bd=preordered_2964 on theBenchmark for (2964ds/8327Mi) % 38.69/6.15 % Exception at run slice level % 38.69/6.15 User error: GNN currently only supports monomorphic FOL. % 38.69/6.15 % (1210277)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=2825524698:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2963 on theBenchmark for (2963ds/1083Mi) % 38.69/6.15 % (1210279)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=3944502322:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2962 on theBenchmark for (2962ds/1084Mi) % 38.69/6.15 % (1210272)Instruction limit reached! % 38.69/6.15 % (1210272)------------------------------ % 38.69/6.15 % (1210272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.69/6.15 % (1210272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.69/6.15 % (1210272)CaDiCaL version: 2.1.3 % 38.69/6.15 % (1210272)Termination reason: Instruction limit % 38.69/6.15 % (1210272)Termination phase: Saturation % 38.69/6.15 % (1210272)Time elapsed: 0.453 s % 38.69/6.15 % (1210272)Peak memory usage: 93 MB % 38.69/6.15 % (1210272)Instructions burned: 1009 (million) % 38.69/6.15 % (1210251)Instruction limit reached! % 46.70/7.45 % (1210251)------------------------------ % 46.70/7.45 % (1210251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.70/7.45 % (1210251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.70/7.45 % (1210251)CaDiCaL version: 2.1.3 % 46.70/7.45 % (1210251)Termination reason: Instruction limit % 46.70/7.45 % (1210251)Termination phase: Saturation % 46.70/7.45 % (1210251)Time elapsed: 1.598 s % 46.70/7.45 % (1210251)Peak memory usage: 108 MB % 46.70/7.45 % (1210251)Instructions burned: 5785 (million) % 46.70/7.45 % Exception at run slice level % 46.70/7.45 User error: GNN currently only supports monomorphic FOL. % 46.70/7.45 % (1210283)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=3012874167:st=2:i=6225:sd=15:ss=axioms_2959 on theBenchmark for (2959ds/6225Mi) % 46.70/7.45 % (1210282)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=4272532500:i=6995:s2at=5:gtg=all_2960 on theBenchmark for (2960ds/6995Mi) % 46.70/7.45 % (1210283)Refutation not found, incomplete strategy % 46.70/7.45 % (1210283)------------------------------ % 46.70/7.45 % (1210283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.70/7.45 % (1210283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.70/7.45 % (1210283)CaDiCaL version: 2.1.3 % 46.70/7.45 % (1210283)Termination reason: Refutation not found, incomplete strategy % 46.70/7.45 % (1210283)Time elapsed: 0.007 s % 46.70/7.45 % (1210283)Peak memory usage: 89 MB % 46.70/7.45 % (1210283)Instructions burned: 23 (million) % 46.70/7.45 % Exception at run slice level % 46.70/7.45 User error: Immediate (shared) subterms of term/literal product_prod_rec(X0,X2,X1,X5,product_Pair(X0,X2,X4,X3)) = sF71(X0,X2,X1,X5,X4,X3) have different types/not well-typed! % 46.70/7.45 % (1210284)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=1581060122:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2959 on theBenchmark for (2959ds/3372Mi) % 46.70/7.45 % (1210287)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2475293359:st=2.3:i=26457:sd=10:ss=included:sgt=8_2958 on theBenchmark for (2958ds/26457Mi) % 46.70/7.45 % (1210283)------------------------------ % 46.70/7.45 % (1210283)------------------------------ % 46.70/7.45 % (1210277)Instruction limit reached! % 46.70/7.45 % (1210277)------------------------------ % 46.70/7.45 % (1210277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.70/7.45 % (1210277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.70/7.45 % (1210277)CaDiCaL version: 2.1.3 % 46.70/7.45 % (1210277)Termination reason: Instruction limit % 46.70/7.45 % (1210277)Termination phase: Saturation % 46.70/7.45 % (1210277)Time elapsed: 0.548 s % 46.70/7.45 % (1210277)Peak memory usage: 96 MB % 46.70/7.45 % (1210277)Instructions burned: 1085 (million) % 46.70/7.45 % (1210290)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=389923786:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2957 on theBenchmark for (2957ds/13494Mi) % 46.70/7.45 % (1210279)Instruction limit reached! % 46.70/7.45 % (1210279)------------------------------ % 46.70/7.45 % (1210279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.70/7.45 % (1210279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.70/7.45 % (1210279)CaDiCaL version: 2.1.3 % 46.70/7.45 % (1210279)Termination reason: Instruction limit % 46.70/7.45 % (1210279)Termination phase: Saturation % 46.70/7.45 % (1210279)Time elapsed: 0.471 s % 46.70/7.45 % (1210279)Peak memory usage: 90 MB % 46.70/7.45 % (1210279)Instructions burned: 1084 (million) % 46.70/7.45 % (1210291)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=3056900348:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2956 on theBenchmark for (2956ds/2503Mi) % 46.70/7.45 % (1210291)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 46.70/7.45 % (1210293)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=2155941492:i=2559:sd=1:ep=RSTC:ss=axioms_2956 on theBenchmark for (2956ds/2559Mi) % 46.70/7.45 % Exception at run slice level % 46.70/7.45 User error: GNN currently only supports monomorphic FOL. % 46.70/7.45 % Exception at run slice level % 46.70/7.45 User error: GNN currently only supports monomorphic FOL. % 57.99/9.22 % Exception at run slice level % 57.99/9.22 User error: GNN currently only supports monomorphic FOL. % 57.99/9.22 % (1210296)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=261312917:i=30753:av=off:ss=included_2954 on theBenchmark for (2954ds/30753Mi) % 57.99/9.22 % (1210297)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=1293517248:i=26473:ep=RSTC_2954 on theBenchmark for (2954ds/26473Mi) % 57.99/9.22 % (1210298)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=3122653634:cts=off:i=2759:kws=inv_arity:fgj=on_2953 on theBenchmark for (2953ds/2759Mi) % 57.99/9.22 % Exception at run slice level % 57.99/9.22 User error: GNN currently only supports monomorphic FOL. % 57.99/9.22 % Exception at run slice level % 57.99/9.22 User error: GNN currently only supports monomorphic FOL. % 57.99/9.22 % Exception at run slice level % 57.99/9.22 User error: GNN currently only supports monomorphic FOL. % 57.99/9.22 % (1210303)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=652446753:i=1532:ep=RS:ss=axioms_2951 on theBenchmark for (2951ds/1532Mi) % 57.99/9.22 % (1210302)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=226125488:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2951 on theBenchmark for (2951ds/5665Mi) % 57.99/9.22 % (1210302)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 57.99/9.22 % (1210304)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=4183265118:i=1565:sd=2:ss=axioms:sgt=32_2951 on theBenchmark for (2951ds/1565Mi) % 57.99/9.22 % Exception at run slice level % 57.99/9.22 User error: GNN currently only supports monomorphic FOL. % 57.99/9.22 % Exception at run slice level % 57.99/9.22 User error: GNN currently only supports monomorphic FOL. % 57.99/9.22 % (1210309)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=1419259879:i=6052:sd=4:ss=axioms:sgt=24_2948 on theBenchmark for (2948ds/6052Mi) % 57.99/9.22 % (1210308)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=4287689711:i=1572:fgj=on:gsp=on_2948 on theBenchmark for (2948ds/1572Mi) % 57.99/9.22 % (1210308)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 57.99/9.22 % Exception at run slice level % 57.99/9.22 User error: GNN currently only supports monomorphic FOL. % 57.99/9.22 % (1210263)Instruction limit reached! % 57.99/9.22 % (1210263)------------------------------ % 57.99/9.22 % (1210263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.99/9.22 % (1210263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.99/9.22 % (1210263)CaDiCaL version: 2.1.3 % 57.99/9.22 % (1210263)Termination reason: Instruction limit % 57.99/9.22 % (1210263)Termination phase: Saturation % 57.99/9.22 % (1210263)Time elapsed: 2.202 s % 57.99/9.22 % (1210263)Peak memory usage: 107 MB % 57.99/9.22 % (1210263)Instructions burned: 4835 (million) % 57.99/9.22 % Exception at run slice level % 57.99/9.22 User error: GNN currently only supports monomorphic FOL. % 57.99/9.22 % Exception at run slice level % 57.99/9.22 User error: GNN currently only supports monomorphic FOL. % 57.99/9.22 % (1210312)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=388840638:i=3500:sd=1:bd=preordered:sup=off:ss=included_2946 on theBenchmark for (2946ds/3500Mi) % 57.99/9.22 % (1210313)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=3315189778:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2946 on theBenchmark for (2946ds/1842Mi) % 57.99/9.22 % (1210313)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 57.99/9.22 % (1210314)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3212232287:i=66096:add=on_2946 on theBenchmark for (2946ds/66096Mi) % 67.99/10.69 % (1210315)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=2870949022:i=1884:sd=1:nm=60:ss=axioms_2945 on theBenchmark for (2945ds/1884Mi) % 67.99/10.69 % Exception at run slice level % 67.99/10.69 User error: GNN currently only supports monomorphic FOL. % 67.99/10.69 % Exception at run slice level % 67.99/10.69 User error: GNN currently only supports monomorphic FOL. % 67.99/10.69 % (1210320)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3725285088:cts=off:i=5469:bs=on:fsr=off_2943 on theBenchmark for (2943ds/5469Mi) % 67.99/10.69 % Exception at run slice level % 67.99/10.69 User error: GNN currently only supports monomorphic FOL. % 67.99/10.69 % Exception at run slice level % 67.99/10.69 User error: GNN currently only supports monomorphic FOL. % 67.99/10.69 % Exception at run slice level % 67.99/10.69 User error: GNN currently only supports monomorphic FOL. % 67.99/10.69 % (1210321)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=3201145750:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2942 on theBenchmark for (2942ds/2037Mi) % 67.99/10.69 % (1210324)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=2009270378:i=2430:add=off:aac=none:nm=16_2941 on theBenchmark for (2941ds/2430Mi) % 67.99/10.69 % (1210323)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2146408929:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2941 on theBenchmark for (2941ds/2110Mi) % 67.99/10.69 % (1210325)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=952598096:cond=fast:i=4891_2941 on theBenchmark for (2941ds/4891Mi) % 67.99/10.69 % Exception at run slice level % 67.99/10.69 User error: GNN currently only supports monomorphic FOL. % 67.99/10.69 % (1210330)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=234222427:st=2:i=14845:sd=2:ss=included:fsd=on_2939 on theBenchmark for (2939ds/14845Mi) % 67.99/10.69 % Exception at run slice level % 67.99/10.69 User error: GNN currently only supports monomorphic FOL. % 67.99/10.69 % Exception at run slice level % 67.99/10.69 User error: GNN currently only supports monomorphic FOL. % 67.99/10.69 % Exception at run slice level % 67.99/10.69 User error: GNN currently only supports monomorphic FOL. % 67.99/10.69 % (1210332)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=248118096:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2937 on theBenchmark for (2937ds/7534Mi) % 67.99/10.69 % Exception at run slice level % 67.99/10.69 User error: GNN currently only supports monomorphic FOL. % 67.99/10.69 % (1210333)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=3402255485:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2936 on theBenchmark for (2936ds/10353Mi) % 67.99/10.69 % (1210336)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=1457429978:i=7896:sd=2:bs=on:ss=included:sgt=20_2936 on theBenchmark for (2936ds/7896Mi) % 67.99/10.69 % (1210334)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2979843971:i=7860_2936 on theBenchmark for (2936ds/7860Mi) % 67.99/10.69 % (1210334)Refutation not found, incomplete strategy % 67.99/10.69 % (1210334)------------------------------ % 67.99/10.69 % (1210334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.99/10.69 % (1210334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.99/10.69 % (1210334)CaDiCaL version: 2.1.3 % 67.99/10.69 % (1210334)Termination reason: Refutation not found, incomplete strategy % 67.99/10.69 % (1210334)Time elapsed: 0.011 s % 67.99/10.69 % (1210334)Peak memory usage: 89 MB % 67.99/10.69 % (1210334)Instructions burned: 20 (million) % 67.99/10.69 % Exception at run slice level % 67.99/10.69 User error: GNN currently only supports monomorphic FOL. % 67.99/10.69 % Exception at run slice level % 67.99/10.69 User error: GNN currently only supports monomorphic FOL. % 67.99/10.69 % (1210334)------------------------------ % 67.99/10.69 % (1210334)------------------------------ % 67.99/10.69 % (1210340)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=947176553:i=5812:gtgl=2:gtg=all_2933 on theBenchmark for (2933ds/5812Mi) % 119.24/17.80 % Exception at run slice level % 119.24/17.80 User error: GNN currently only supports monomorphic FOL. % 119.24/17.80 % (1210341)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=1673183267:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2932 on theBenchmark for (2932ds/2965Mi) % 119.24/17.80 % (1210342)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=2853893803:i=2967:kws=precedence:bd=preordered:av=off_2932 on theBenchmark for (2932ds/2967Mi) % 119.24/17.80 % (1210344)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=1376502615:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2931 on theBenchmark for (2931ds/3022Mi) % 119.24/17.80 % Exception at run slice level % 119.24/17.80 User error: GNN currently only supports monomorphic FOL. % 119.24/17.80 % (1210348)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=3394961747:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2930 on theBenchmark for (2930ds/3207Mi) % 119.24/17.80 % Exception at run slice level % 119.24/17.80 User error: GNN currently only supports monomorphic FOL. % 119.24/17.80 % Exception at run slice level % 119.24/17.80 User error: GNN currently only supports monomorphic FOL. % 119.24/17.80 % Exception at run slice level % 119.24/17.80 User error: GNN currently only supports monomorphic FOL. % 119.24/17.80 % Exception at run slice level % 119.24/17.80 User error: GNN currently only supports monomorphic FOL. % 119.24/17.80 % (1210352)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=1965057178:cts=off:i=3394_2927 on theBenchmark for (2927ds/3394Mi) % 119.24/17.80 % (1210350)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=1447157372:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2927 on theBenchmark for (2927ds/3289Mi) % 119.24/17.80 % (1210351)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=393319748:i=38569:sd=3:ss=axioms:sgt=32_2927 on theBenchmark for (2927ds/38569Mi) % 119.24/17.80 % (1210353)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=2497383867:i=33824:bd=preordered_2926 on theBenchmark for (2926ds/33824Mi) % 119.24/17.80 % Exception at run slice level % 119.24/17.80 User error: GNN currently only supports monomorphic FOL. % 119.24/17.80 % (1210358)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=509399849:i=20684:bd=all:gtg=exists_sym_2924 on theBenchmark for (2924ds/20684Mi) % 119.24/17.80 % Exception at run slice level % 119.24/17.80 User error: GNN currently only supports monomorphic FOL. % 119.24/17.80 % Exception at run slice level % 119.24/17.80 User error: GNN currently only supports monomorphic FOL. % 119.24/17.80 % Exception at run slice level % 119.24/17.80 User error: GNN currently only supports monomorphic FOL. % 119.24/17.80 % Exception at run slice level % 119.24/17.80 User error: GNN currently only supports monomorphic FOL. % 119.24/17.80 % (1210320)Instruction limit reached! % 119.24/17.80 % (1210320)------------------------------ % 119.24/17.80 % (1210320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.24/17.80 % (1210320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.24/17.80 % (1210320)CaDiCaL version: 2.1.3 % 119.24/17.80 % (1210320)Termination reason: Instruction limit % 119.24/17.80 % (1210320)Termination phase: Saturation % 119.24/17.80 % (1210320)Time elapsed: 2.658 s % 119.24/17.80 % (1210320)Peak memory usage: 103 MB % 119.24/17.80 % (1210320)Instructions burned: 5470 (million) % 119.24/17.80 % (1210363)lrs+10_1_sil=128000:lcm=predicate:random_seed=808687132:st=3:i=43697:sd=5:ss=axioms_2916 on theBenchmark for (2916ds/43697Mi) % 119.24/17.80 % (1210360)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=1741176196: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_2916 on theBenchmark for (2916ds/7222Mi) % 153.79/22.78 % (1210362)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=1192708266:i=4036:ins=10_2916 on theBenchmark for (2916ds/4036Mi) % 153.79/22.78 % (1210361)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=1956424153:st=4:i=7295:sd=4:ep=R:ss=axioms_2916 on theBenchmark for (2916ds/7295Mi) % 153.79/22.78 % (1210364)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=2413692258:i=17599:gtg=all:ss=axioms:fsd=on_2915 on theBenchmark for (2915ds/17599Mi) % 153.79/22.78 % (1210360)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 153.79/22.78 % Exception at run slice level % 153.79/22.78 User error: GNN currently only supports monomorphic FOL. % 153.79/22.78 % Exception at run slice level % 153.79/22.78 User error: GNN currently only supports monomorphic FOL. % 153.79/22.78 % Exception at run slice level % 153.79/22.78 User error: GNN currently only supports monomorphic FOL. % 153.79/22.78 % Exception at run slice level % 153.79/22.78 User error: GNN currently only supports monomorphic FOL. % 153.79/22.78 % (1210370)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=3737835939:i=4547:bd=preordered_2910 on theBenchmark for (2910ds/4547Mi) % 153.79/22.78 % (1210373)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3106510322:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2910 on theBenchmark for (2910ds/4793Mi) % 153.79/22.78 % (1210372)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3061522903:i=32849:add=on_2910 on theBenchmark for (2910ds/32849Mi) % 153.79/22.78 % (1210371)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=4150330965:i=9294:av=off_2910 on theBenchmark for (2910ds/9294Mi) % 153.79/22.78 % Exception at run slice level % 153.79/22.78 User error: GNN currently only supports monomorphic FOL. % 153.79/22.78 % Exception at run slice level % 153.79/22.78 User error: GNN currently only supports monomorphic FOL. % 153.79/22.78 % Exception at run slice level % 153.79/22.78 User error: GNN currently only supports monomorphic FOL. % 153.79/22.78 % Exception at run slice level % 153.79/22.78 User error: GNN currently only supports monomorphic FOL. % 153.79/22.78 % (1210378)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=1465019459:i=4840:nm=4:av=off_2906 on theBenchmark for (2906ds/4840Mi) % 153.79/22.78 % (1210379)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=4078467819:cts=off:i=5002_2906 on theBenchmark for (2906ds/5002Mi) % 153.79/22.78 % (1210381)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=392336705:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2906 on theBenchmark for (2906ds/11035Mi) % 153.79/22.78 % (1210380)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=594882904:i=30479:sd=3:ss=axioms_2906 on theBenchmark for (2906ds/30479Mi) % 153.79/22.78 % (1210381)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 153.79/22.78 % Exception at run slice level % 153.79/22.78 User error: GNN currently only supports monomorphic FOL. % 153.79/22.78 % Exception at run slice level % 153.79/22.78 User error: GNN currently only supports monomorphic FOL. % 153.79/22.78 % Exception at run slice level % 153.79/22.78 User error: GNN currently only supports monomorphic FOL. % 153.79/22.78 % Exception at run slice level % 153.79/22.78 User error: GNN currently only supports monomorphic FOL. % 153.79/22.78 % (1210386)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=2397326311:i=5835_2901 on theBenchmark for (2901ds/5835Mi) % 153.79/22.78 % (1210387)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=3934895568:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2901 on theBenchmark for (2901ds/5890Mi) % 153.79/22.78 % (1210389)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=2178775237:i=20312:bd=preordered:fsr=off:er=filter_2901 on theBenchmark for (2901ds/20312Mi) % 189.43/27.71 % (1210388)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=608346754:cts=off:i=19910:ep=RS_2901 on theBenchmark for (2901ds/19910Mi) % 189.43/27.71 % Exception at run slice level % 189.43/27.71 User error: GNN currently only supports monomorphic FOL. % 189.43/27.71 % Exception at run slice level % 189.43/27.71 User error: GNN currently only supports monomorphic FOL. % 189.43/27.71 % Exception at run slice level % 189.43/27.71 User error: GNN currently only supports monomorphic FOL. % 189.43/27.71 % (1210394)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=2674832519:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2896 on theBenchmark for (2896ds/13822Mi) % 189.43/27.71 % (1210396)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=3338925823:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2896 on theBenchmark for (2896ds/15184Mi) % 189.43/27.71 % (1210395)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=3836603809:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2896 on theBenchmark for (2896ds/7144Mi) % 189.43/27.71 % Exception at run slice level % 189.43/27.71 User error: GNN currently only supports monomorphic FOL. % 189.43/27.71 % Exception at run slice level % 189.43/27.71 User error: GNN currently only supports monomorphic FOL. % 189.43/27.71 % (1210400)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=1016865883:i=107375_2891 on theBenchmark for (2891ds/107375Mi) % 189.43/27.71 % (1210401)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=797146588:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2891 on theBenchmark for (2891ds/7958Mi) % 189.43/27.71 % Exception at run slice level % 189.43/27.71 User error: GNN currently only supports monomorphic FOL. % 189.43/27.71 % Exception at run slice level % 189.43/27.71 User error: GNN currently only supports monomorphic FOL. % 189.43/27.71 % (1210404)dis+10_128_sil=16000:nwc=0.7:random_seed=317675676:i=15999:nm=2:gsp=on_2886 on theBenchmark for (2886ds/15999Mi) % 189.43/27.71 % (1210404)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 189.43/27.71 % (1210405)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=277755529:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2886 on theBenchmark for (2886ds/8139Mi) % 189.43/27.71 % (1210395)Instruction limit reached! % 189.43/27.71 % (1210395)------------------------------ % 189.43/27.71 % (1210395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.43/27.71 % (1210395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.43/27.71 % (1210395)CaDiCaL version: 2.1.3 % 189.43/27.71 % (1210395)Termination reason: Instruction limit % 189.43/27.71 % (1210395)Termination phase: Saturation % 189.43/27.71 % (1210395)Time elapsed: 4.098 s % 189.43/27.71 % (1210395)Peak memory usage: 140 MB % 189.43/27.71 % (1210395)Instructions burned: 7144 (million) % 189.43/27.71 % (1210688)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=2870043587:st=4:i=8950:sd=5:ss=axioms_2853 on theBenchmark for (2853ds/8950Mi) % 189.43/27.71 % Exception at run slice level % 189.43/27.71 User error: GNN currently only supports monomorphic FOL. % 189.43/27.71 % (1210712)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=3666190531:i=9809:ins=10:av=off_2846 on theBenchmark for (2846ds/9809Mi) % 189.43/27.71 % Exception at run slice level % 189.43/27.71 User error: GNN currently only supports monomorphic FOL. % 189.43/27.71 % (1210718)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=3811744517:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2837 on theBenchmark for (2837ds/9885Mi) % 189.43/27.71 % Exception at run slice level % 189.43/27.71 User error: GNN currently only supports monomorphic FOL. % 189.43/27.71 % (1210405)Instruction limit reached! % 189.43/27.71 % (1210405)------------------------------ % 189.43/27.71 % (1210405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.08/30.63 % (1210405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.08/30.63 % (1210405)CaDiCaL version: 2.1.3 % 210.08/30.63 % (1210405)Termination reason: Instruction limit % 210.08/30.63 % (1210405)Termination phase: Saturation % 210.08/30.63 % (1210405)Time elapsed: 5.662 s % 210.08/30.63 % (1210405)Peak memory usage: 134 MB % 210.08/30.63 % (1210405)Instructions burned: 8139 (million) % 210.08/30.63 % (1210720)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=2954205556:cond=fast:i=32078:fgj=on:av=off_2829 on theBenchmark for (2829ds/32078Mi) % 210.08/30.63 % (1210721)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=305255219:i=11101:bd=all:ss=axioms:sgt=8_2828 on theBenchmark for (2828ds/11101Mi) % 210.08/30.63 % Exception at run slice level % 210.08/30.63 User error: GNN currently only supports monomorphic FOL. % 210.08/30.63 % (1210730)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=907988430:cond=on:i=13220:s2at=3:aac=none:fsd=on_2821 on theBenchmark for (2821ds/13220Mi) % 210.08/30.63 % Exception at run slice level % 210.08/30.63 User error: GNN currently only supports monomorphic FOL. % 210.08/30.63 % (1210734)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=920624639:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2813 on theBenchmark for (2813ds/13528Mi) % 210.08/30.63 % Exception at run slice level % 210.08/30.63 User error: GNN currently only supports monomorphic FOL. % 210.08/30.63 % (1210741)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=1157054863:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2805 on theBenchmark for (2805ds/14854Mi) % 210.08/30.63 % Exception at run slice level % 210.08/30.63 User error: GNN currently only supports monomorphic FOL. % 210.08/30.63 % (1210750)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=1367916259:i=14974:ss=axioms:sgt=16_2796 on theBenchmark for (2796ds/14974Mi) % 210.08/30.63 % (1210388)Instruction limit reached! % 210.08/30.63 % (1210388)------------------------------ % 210.08/30.63 % (1210388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.08/30.63 % (1210388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.08/30.63 % (1210388)CaDiCaL version: 2.1.3 % 210.08/30.63 % (1210388)Termination reason: Instruction limit % 210.08/30.63 % (1210388)Termination phase: Saturation % 210.08/30.63 % (1210388)Time elapsed: 10.947 s % 210.08/30.63 % (1210388)Peak memory usage: 92 MB % 210.08/30.63 % (1210388)Instructions burned: 19910 (million) % 210.08/30.63 % Exception at run slice level % 210.08/30.63 User error: GNN currently only supports monomorphic FOL. % 210.08/30.63 % (1210752)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=453006519:i=33081:aac=none:fgj=on:bd=all:fsr=off_2790 on theBenchmark for (2790ds/33081Mi) % 210.08/30.63 % (1210753)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=3181161342:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2788 on theBenchmark for (2788ds/50856Mi) % 210.08/30.63 % Exception at run slice level % 210.08/30.63 User error: GNN currently only supports monomorphic FOL. % 210.08/30.63 % (1210297)Instruction limit reached! % 210.08/30.63 % (1210297)------------------------------ % 210.08/30.63 % (1210297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.08/30.63 % (1210297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.08/30.63 % (1210297)CaDiCaL version: 2.1.3 % 210.08/30.63 % (1210297)Termination reason: Instruction limit % 210.08/30.63 % (1210297)Termination phase: Saturation % 210.08/30.63 % (1210297)Time elapsed: 17.137 s % 210.08/30.63 % (1210297)Peak memory usage: 350 MB % 210.08/30.63 % (1210297)Instructions burned: 26473 (million) % 210.08/30.63 % Exception at run slice level % 210.08/30.63 User error: GNN currently only supports monomorphic FOL. % 210.08/30.63 % (1210756)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=3003664845:i=69865_2782 on theBenchmark for (2782ds/69865Mi) % 210.08/30.63 % (1210757)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=2259425219:cond=fast:i=17802:gtgl=3:gtg=all_2781 on theBenchmark for (2781ds/17802Mi) % 223.27/32.55 % Exception at run slice level % 223.27/32.55 User error: Immediate (shared) subterms of term/literal product_prod_rec(X0,X2,X1,X5,product_Pair(X0,X2,X4,X3)) = sF71(X0,X2,X1,X5,X4,X3) have different types/not well-typed! % 223.27/32.55 % (1210758)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=3624078410:i=96644_2780 on theBenchmark for (2780ds/96644Mi) % 223.27/32.55 % (1210761)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 223.27/32.55 % (1210761)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=4077482690:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2778 on theBenchmark for (2778ds/21161Mi) % 223.27/32.55 % Exception at run slice level % 223.27/32.55 User error: GNN currently only supports monomorphic FOL. % 223.27/32.55 % (1210764)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=4163088869:i=22761:gtg=all:ss=axioms:fsd=on_2773 on theBenchmark for (2773ds/22761Mi) % 223.27/32.55 % (1210404)Instruction limit reached! % 223.27/32.55 % (1210404)------------------------------ % 223.27/32.55 % (1210404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.27/32.55 % (1210404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.27/32.55 % (1210404)CaDiCaL version: 2.1.3 % 223.27/32.55 % (1210404)Termination reason: Instruction limit % 223.27/32.55 % (1210404)Termination phase: Saturation % 223.27/32.55 % (1210404)Time elapsed: 11.742 s % 223.27/32.55 % (1210404)Peak memory usage: 123 MB % 223.27/32.55 % (1210404)Instructions burned: 16000 (million) % 223.27/32.55 % Exception at run slice level % 223.27/32.55 User error: GNN currently only supports monomorphic FOL. % 223.27/32.55 % (1210768)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=123238835:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2768 on theBenchmark for (2768ds/23713Mi) % 223.27/32.55 % (1210769)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=899534140:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2766 on theBenchmark for (2766ds/26509Mi) % 223.27/32.55 % Exception at run slice level % 223.27/32.55 User error: GNN currently only supports monomorphic FOL. % 223.27/32.55 % (1210776)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=2824916925:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2758 on theBenchmark for (2758ds/28957Mi) % 223.27/32.55 % (1210363)Instruction limit reached! % 223.27/32.55 % (1210363)------------------------------ % 223.27/32.55 % (1210363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.27/32.55 % (1210363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.27/32.55 % (1210363)CaDiCaL version: 2.1.3 % 223.27/32.55 % (1210363)Termination reason: Instruction limit % 223.27/32.55 % (1210363)Termination phase: Saturation % 223.27/32.55 % (1210363)Time elapsed: 18.001 s % 223.27/32.55 % (1210363)Peak memory usage: 215 MB % 223.27/32.55 % (1210363)Instructions burned: 43697 (million) % 223.27/32.55 % (1210778)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=944563904:i=29246:s2at=-1:kws=inv_arity:ins=10_2734 on theBenchmark for (2734ds/29246Mi) % 223.27/32.55 % (1210721)Instruction limit reached! % 223.27/32.55 % (1210721)------------------------------ % 223.27/32.55 % (1210721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.27/32.55 % (1210721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.27/32.55 % (1210721)CaDiCaL version: 2.1.3 % 223.27/32.55 % (1210721)Termination reason: Instruction limit % 223.27/32.55 % (1210721)Termination phase: Saturation % 223.27/32.55 % (1210721)Time elapsed: 9.478 s % 223.27/32.55 % (1210721)Peak memory usage: 119 MB % 223.27/32.55 % (1210721)Instructions burned: 11102 (million) % 223.27/32.55 % Exception at run slice level % 223.27/32.55 User error: GNN currently only supports monomorphic FOL. % 223.27/32.55 % (1210780)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=1919617581:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2731 on theBenchmark for (2731ds/30082Mi) % 233.30/33.94 % (1210780)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 233.30/33.94 % (1210781)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=1944624655:i=32262:bd=preordered_2730 on theBenchmark for (2730ds/32262Mi) % 233.30/33.94 % Exception at run slice level % 233.30/33.94 User error: GNN currently only supports monomorphic FOL. % 233.30/33.94 % (1210786)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=956266400:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2725 on theBenchmark for (2725ds/32870Mi) % 233.30/33.94 % (1210271)Instruction limit reached! % 233.30/33.94 % (1210271)------------------------------ % 233.30/33.94 % (1210271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.30/33.94 % (1210271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.30/33.94 % (1210271)CaDiCaL version: 2.1.3 % 233.30/33.94 % (1210271)Termination reason: Instruction limit % 233.30/33.94 % (1210271)Termination phase: Saturation % 233.30/33.94 % (1210271)Time elapsed: 24.060 s % 233.30/33.94 % (1210271)Peak memory usage: 194 MB % 233.30/33.94 % (1210271)Instructions burned: 33335 (million) % 233.30/33.94 % Exception at run slice level % 233.30/33.94 User error: GNN currently only supports monomorphic FOL. % 233.30/33.94 % (1210788)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=3214500792:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2723 on theBenchmark for (2723ds/33295Mi) % 233.30/33.94 % (1210789)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=1237808897:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2723 on theBenchmark for (2723ds/36826Mi) % 233.30/33.94 % Exception at run slice level % 233.30/33.94 User error: GNN currently only supports monomorphic FOL. % 233.30/33.94 % (1210792)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=2693338548:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2720 on theBenchmark for (2720ds/92981Mi) % 233.30/33.94 % Exception at run slice level % 233.30/33.94 User error: GNN currently only supports monomorphic FOL. % 233.30/33.94 % Exception at run slice level % 233.30/33.94 User error: GNN currently only supports monomorphic FOL. % 233.30/33.94 % (1210794)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=1613035155:s2pl=on:i=49423_2716 on theBenchmark for (2716ds/49423Mi) % 233.30/33.94 % (1210795)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=2175067772:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2715 on theBenchmark for (2715ds/57299Mi) % 233.30/33.94 % Exception at run slice level % 233.30/33.94 User error: GNN currently only supports monomorphic FOL. % 233.30/33.94 % Exception at run slice level % 233.30/33.94 User error: GNN currently only supports monomorphic FOL. % 233.30/33.94 % (1210798)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=1120012471:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2710 on theBenchmark for (2710ds/127679Mi) % 233.30/33.94 % (1210799)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=3323605699:i=69402:add=on:aac=none:fsr=off_2709 on theBenchmark for (2709ds/69402Mi) % 233.30/33.94 % Exception at run slice level % 233.30/33.94 User error: GNN currently only supports monomorphic FOL. % 233.30/33.94 % (1210802)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=1638860583:i=100512:doe=on:fgj=on:bd=all:fsd=on_2706 on theBenchmark for (2706ds/100512Mi) % 233.30/33.94 % Exception at run slice level % 233.30/33.94 User error: GNN currently only supports monomorphic FOL. % 233.30/33.94 % Exception at run slice level % 233.30/33.94 User error: GNN currently only supports monomorphic FOL. % 233.30/33.94 % (1210806)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=4106709685:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2701 on theBenchmark for (2701ds/138761Mi) % 245.73/35.67 % (1210807)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=4130597052:i=282386:rtra=on_2701 on theBenchmark for (2701ds/282386Mi) % 245.73/35.67 % Exception at run slice level % 245.73/35.67 User error: GNN currently only supports monomorphic FOL. % 245.73/35.67 % (1210810)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=820762951:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2697 on theBenchmark for (2697ds/269354Mi) % 245.73/35.67 % Exception at run slice level % 245.73/35.67 User error: GNN currently only supports monomorphic FOL. % 245.73/35.67 % Exception at run slice level % 245.73/35.67 User error: GNN currently only supports monomorphic FOL. % 245.73/35.67 % (1210812)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=3445535663:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2693 on theBenchmark for (2693ds/283390Mi) % 245.73/35.67 % (1210812)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 245.73/35.67 % (1210813)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=2415246766:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2692 on theBenchmark for (2692ds/218Mi) % 245.73/35.67 % (1210813)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 245.73/35.67 % (1210813)Refutation not found, incomplete strategy % 245.73/35.67 % (1210813)------------------------------ % 245.73/35.67 % (1210813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.73/35.67 % (1210813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.73/35.67 % (1210813)CaDiCaL version: 2.1.3 % 245.73/35.67 % (1210813)Termination reason: Refutation not found, incomplete strategy % 245.73/35.67 % (1210813)Time elapsed: 0.002 s % 245.73/35.67 % (1210813)Peak memory usage: 88 MB % 245.73/35.67 % (1210813)Instructions burned: 2 (million) % 245.73/35.67 % (1210813)------------------------------ % 245.73/35.67 % (1210813)------------------------------ % 245.73/35.67 % (1210816)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=1265459637:i=238:av=off:rtra=on:ss=axioms_2688 on theBenchmark for (2688ds/238Mi) % 245.73/35.67 % (1210816)Instruction limit reached! % 245.73/35.67 % (1210816)------------------------------ % 245.73/35.67 % (1210816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.73/35.67 % (1210816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.73/35.67 % (1210816)CaDiCaL version: 2.1.3 % 245.73/35.67 % (1210816)Termination reason: Instruction limit % 245.73/35.67 % (1210816)Termination phase: Saturation % 245.73/35.67 % (1210816)Time elapsed: 0.115 s % 245.73/35.67 % (1210816)Peak memory usage: 89 MB % 245.73/35.67 % (1210816)Instructions burned: 238 (million) % 245.73/35.67 % Exception at run slice level % 245.73/35.67 User error: GNN currently only supports monomorphic FOL. % 245.73/35.67 % (1210818)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=3801944953:s2a=on:i=278:rtra=on:gtg=position_2685 on theBenchmark for (2685ds/278Mi) % 245.73/35.67 % (1210818)Instruction limit reached! % 245.73/35.67 % (1210818)------------------------------ % 245.73/35.67 % (1210818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.73/35.67 % (1210818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.73/35.67 % (1210818)CaDiCaL version: 2.1.3 % 245.73/35.67 % (1210818)Termination reason: Instruction limit % 245.73/35.67 % (1210818)Termination phase: Saturation % 245.73/35.67 % (1210818)Time elapsed: 0.096 s % 245.73/35.67 % (1210818)Peak memory usage: 89 MB % 245.73/35.67 % (1210818)Instructions burned: 278 (million) % 245.73/35.67 % (1210819)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=3599411427:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2685 on theBenchmark for (2685ds/258Mi) % 245.73/35.67 % (1210821)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=2839266577:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2683 on theBenchmark for (2683ds/570Mi) % 245.73/35.67 % (1210819)Instruction limit reached! % 245.73/35.67 % (1210819)------------------------------ % 245.73/35.67 % (1210819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.82/36.89 % (1210819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.82/36.89 % (1210819)CaDiCaL version: 2.1.3 % 253.82/36.89 % (1210819)Termination reason: Instruction limit % 253.82/36.89 % (1210819)Termination phase: Saturation % 253.82/36.89 % (1210819)Time elapsed: 0.184 s % 253.82/36.89 % (1210819)Peak memory usage: 88 MB % 253.82/36.89 % (1210819)Instructions burned: 258 (million) % 253.82/36.89 % (1210821)Instruction limit reached! % 253.82/36.89 % (1210821)------------------------------ % 253.82/36.89 % (1210821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.82/36.89 % (1210821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.82/36.89 % (1210821)CaDiCaL version: 2.1.3 % 253.82/36.89 % (1210821)Termination reason: Instruction limit % 253.82/36.89 % (1210821)Termination phase: Saturation % 253.82/36.89 % (1210821)Time elapsed: 0.288 s % 253.82/36.89 % (1210821)Peak memory usage: 93 MB % 253.82/36.89 % (1210821)Instructions burned: 572 (million) % 253.82/36.89 % (1210824)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=1785946139:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2681 on theBenchmark for (2681ds/314Mi) % 253.82/36.89 % (1210826)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=2133111598:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2678 on theBenchmark for (2678ds/650Mi) % 253.82/36.89 % (1210824)Instruction limit reached! % 253.82/36.89 % (1210824)------------------------------ % 253.82/36.89 % (1210824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.82/36.89 % (1210824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.82/36.89 % (1210824)CaDiCaL version: 2.1.3 % 253.82/36.89 % (1210824)Termination reason: Instruction limit % 253.82/36.89 % (1210824)Termination phase: Saturation % 253.82/36.89 % (1210824)Time elapsed: 0.229 s % 253.82/36.89 % (1210824)Peak memory usage: 89 MB % 253.82/36.89 % (1210824)Instructions burned: 316 (million) % 253.82/36.89 % (1210828)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=4050804230:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2676 on theBenchmark for (2676ds/496Mi) % 253.82/36.89 % (1210826)Instruction limit reached! % 253.82/36.89 % (1210826)------------------------------ % 253.82/36.89 % (1210826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.82/36.89 % (1210826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.82/36.89 % (1210826)CaDiCaL version: 2.1.3 % 253.82/36.89 % (1210826)Termination reason: Instruction limit % 253.82/36.89 % (1210826)Termination phase: Saturation % 253.82/36.89 % (1210826)Time elapsed: 0.325 s % 253.82/36.89 % (1210826)Peak memory usage: 92 MB % 253.82/36.89 % (1210826)Instructions burned: 651 (million) % 253.82/36.89 % (1210830)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=3162443759:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2674 on theBenchmark for (2674ds/588Mi) % 253.82/36.89 % (1210830)Instruction limit reached! % 253.82/36.89 % (1210830)------------------------------ % 253.82/36.89 % (1210830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.82/36.89 % (1210830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.82/36.89 % (1210830)CaDiCaL version: 2.1.3 % 253.82/36.89 % (1210830)Termination reason: Instruction limit % 253.82/36.89 % (1210830)Termination phase: Saturation % 253.82/36.89 % (1210830)Time elapsed: 0.239 s % 253.82/36.89 % (1210830)Peak memory usage: 89 MB % 253.82/36.89 % (1210830)Instructions burned: 591 (million) % 253.82/36.89 % (1210828)Instruction limit reached! % 253.82/36.89 % (1210828)------------------------------ % 253.82/36.89 % (1210828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.82/36.89 % (1210828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.82/36.89 % (1210828)CaDiCaL version: 2.1.3 % 253.82/36.89 % (1210828)Termination reason: Instruction limit % 253.82/36.89 % (1210828)Termination phase: Saturation % 253.82/36.89 % (1210828)Time elapsed: 0.435 s % 253.82/36.89 % (1210828)Peak memory usage: 91 MB % 253.82/36.89 % (1210828)Instructions burned: 497 (million) % 253.82/36.89 % (1210832)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=2753660526:i=4700:rtra=on_2670 on theBenchmark for (2670ds/4700Mi) % 253.82/36.89 % (1210833)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1481614851:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2669 on theBenchmark for (2669ds/226Mi) % 253.82/36.89 % (1210833)Refutation not found, incomplete strategy % 263.70/38.15 % (1210833)------------------------------ % 263.70/38.15 % (1210833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.70/38.15 % (1210833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.70/38.15 % (1210833)CaDiCaL version: 2.1.3 % 263.70/38.15 % (1210833)Termination reason: Refutation not found, incomplete strategy % 263.70/38.15 % (1210833)Time elapsed: 0.046 s % 263.70/38.15 % (1210833)Peak memory usage: 89 MB % 263.70/38.15 % (1210833)Instructions burned: 43 (million) % 263.70/38.15 % Exception at run slice level % 263.70/38.15 User error: GNN currently only supports monomorphic FOL. % 263.70/38.15 % (1210836)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2215957002:i=254:av=off:fsr=off:rtra=on:sup=off_2665 on theBenchmark for (2665ds/254Mi) % 263.70/38.15 % (1210833)------------------------------ % 263.70/38.15 % (1210833)------------------------------ % 263.70/38.15 % (1210836)Instruction limit reached! % 263.70/38.15 % (1210836)------------------------------ % 263.70/38.15 % (1210836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.70/38.15 % (1210836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.70/38.15 % (1210836)CaDiCaL version: 2.1.3 % 263.70/38.15 % (1210836)Termination reason: Instruction limit % 263.70/38.15 % (1210836)Termination phase: Saturation % 263.70/38.15 % (1210836)Time elapsed: 0.119 s % 263.70/38.15 % (1210836)Peak memory usage: 89 MB % 263.70/38.15 % (1210836)Instructions burned: 254 (million) % 263.70/38.15 % (1210839)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=973822623:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2662 on theBenchmark for (2662ds/1814Mi) % 263.70/38.15 % (1210838)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=11478059:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2663 on theBenchmark for (2663ds/228Mi) % 263.70/38.15 % (1210838)Instruction limit reached! % 263.70/38.15 % (1210838)------------------------------ % 263.70/38.15 % (1210838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.70/38.15 % (1210838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.70/38.15 % (1210838)CaDiCaL version: 2.1.3 % 263.70/38.15 % (1210838)Termination reason: Instruction limit % 263.70/38.15 % (1210838)Termination phase: Saturation % 263.70/38.15 % (1210838)Time elapsed: 0.212 s % 263.70/38.15 % (1210838)Peak memory usage: 89 MB % 263.70/38.15 % (1210838)Instructions burned: 229 (million) % 263.70/38.15 % (1210842)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=992180019:i=874:sd=1:aac=none:rtra=on:ss=included_2658 on theBenchmark for (2658ds/874Mi) % 263.70/38.15 % (1210839)Instruction limit reached! % 263.70/38.15 % (1210839)------------------------------ % 263.70/38.15 % (1210839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.70/38.15 % (1210839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.70/38.15 % (1210839)CaDiCaL version: 2.1.3 % 263.70/38.15 % (1210839)Termination reason: Instruction limit % 263.70/38.15 % (1210839)Termination phase: Saturation % 263.70/38.15 % (1210839)Time elapsed: 0.892 s % 263.70/38.15 % (1210839)Peak memory usage: 100 MB % 263.70/38.15 % (1210839)Instructions burned: 1814 (million) % 263.70/38.15 % (1210842)Instruction limit reached! % 263.70/38.15 % (1210842)------------------------------ % 263.70/38.15 % (1210842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.70/38.15 % (1210842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.70/38.15 % (1210842)CaDiCaL version: 2.1.3 % 263.70/38.15 % (1210842)Termination reason: Instruction limit % 263.70/38.15 % (1210842)Termination phase: Saturation % 263.70/38.15 % (1210842)Time elapsed: 0.607 s % 263.70/38.15 % (1210842)Peak memory usage: 90 MB % 263.70/38.15 % (1210842)Instructions burned: 875 (million) % 263.70/38.15 % (1210844)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=283771843:i=10404:rtra=on:ss=axioms:sgt=16_2652 on theBenchmark for (2652ds/10404Mi) % 263.70/38.15 % (1210761)Instruction limit reached! % 263.70/38.15 % (1210761)------------------------------ % 263.70/38.15 % (1210761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.70/38.15 % (1210761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.70/38.15 % (1210761)CaDiCaL version: 2.1.3 % 263.70/38.15 % (1210761)Termination reason: Instruction limit % 263.70/38.15 % (1210761)Termination phase: Saturation % 263.70/38.15 % (1210761)Time elapsed: 12.645 s % 263.70/38.15 % (1210761)Peak memory usage: 105 MB % 263.70/38.15 % (1210761)Instructions burned: 21163 (million) % 288.66/41.70 % (1210845)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3477867915:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2650 on theBenchmark for (2650ds/268Mi) % 288.66/41.70 % (1210847)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=2967887204:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2649 on theBenchmark for (2649ds/1184Mi) % 288.66/41.70 % (1210845)Instruction limit reached! % 288.66/41.70 % (1210845)------------------------------ % 288.66/41.70 % (1210845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.66/41.70 % (1210845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.66/41.70 % (1210845)CaDiCaL version: 2.1.3 % 288.66/41.70 % (1210845)Termination reason: Instruction limit % 288.66/41.70 % (1210845)Termination phase: Saturation % 288.66/41.70 % (1210845)Time elapsed: 0.131 s % 288.66/41.70 % (1210845)Peak memory usage: 90 MB % 288.66/41.70 % (1210845)Instructions burned: 270 (million) % 288.66/41.70 % (1210850)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=3224126094:st=3:i=26386:sd=3:rtra=on:ss=axioms_2647 on theBenchmark for (2647ds/26386Mi) % 288.66/41.70 % Exception at run slice level % 288.66/41.70 User error: GNN currently only supports monomorphic FOL. % 288.66/41.70 % Exception at run slice level % 288.66/41.70 User error: GNN currently only supports monomorphic FOL. % 288.66/41.70 % (1210852)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=2791632372:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2644 on theBenchmark for (2644ds/250Mi) % 288.66/41.70 % (1210852)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 288.66/41.70 % (1210855)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=3783067039:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2643 on theBenchmark for (2643ds/268Mi) % 288.66/41.70 % Exception at run slice level % 288.66/41.70 User error: Immediate (shared) subterms of term/literal aa(X1,X2,sF82(X0,X1,X2,X4,X5),X3) = sF83(X1,X2,X0,X4,X5,X3) have different types/not well-typed! % 288.66/41.70 % (1210858)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1804212191:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2641 on theBenchmark for (2641ds/282Mi) % 288.66/41.70 % (1210858)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 288.66/41.70 % (1210858)Refutation not found, incomplete strategy % 288.66/41.70 % (1210858)------------------------------ % 288.66/41.70 % (1210858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.66/41.70 % (1210858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.66/41.70 % (1210858)CaDiCaL version: 2.1.3 % 288.66/41.70 % (1210858)Termination reason: Refutation not found, incomplete strategy % 288.66/41.70 % (1210858)Time elapsed: 0.003 s % 288.66/41.70 % (1210858)Peak memory usage: 88 MB % 288.66/41.70 % (1210858)Instructions burned: 3 (million) % 288.66/41.70 % (1210847)Instruction limit reached! % 288.66/41.70 % (1210847)------------------------------ % 288.66/41.70 % (1210847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.66/41.70 % (1210847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.66/41.70 % (1210847)CaDiCaL version: 2.1.3 % 288.66/41.70 % (1210847)Termination reason: Instruction limit % 288.66/41.70 % (1210847)Termination phase: Saturation % 288.66/41.70 % (1210847)Time elapsed: 0.758 s % 288.66/41.70 % (1210847)Peak memory usage: 90 MB % 288.66/41.70 % (1210847)Instructions burned: 1185 (million) % 288.66/41.70 % (1210852)Instruction limit reached! % 288.66/41.70 % (1210852)------------------------------ % 288.66/41.70 % (1210852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.66/41.70 % (1210852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.66/41.70 % (1210852)CaDiCaL version: 2.1.3 % 288.66/41.70 % (1210852)Termination reason: Instruction limit % 288.66/41.70 % (1210852)Termination phase: Saturation % 288.66/41.70 % (1210852)Time elapsed: 0.238 s % 288.66/41.70 % (1210852)Peak memory usage: 91 MB % 288.66/41.70 % (1210852)Instructions burned: 250 (million) % 288.66/41.70 % (1210860)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=3688982968:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2640 on theBenchmark for (2640ds/862Mi) % 288.66/41.70 % (1210858)------------------------------ % 299.71/43.25 % (1210858)------------------------------ % 299.71/43.25 % (1210861)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=1047156257:i=12120:aac=none:ins=25:rtra=on_2639 on theBenchmark for (2639ds/12120Mi) % 299.71/43.25 % (1210863)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=325411928:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2637 on theBenchmark for (2637ds/300Mi) % 299.71/43.25 % (1210863)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 299.71/43.25 % (1210863)Instruction limit reached! % 299.71/43.25 % (1210863)------------------------------ % 299.71/43.25 % (1210863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.71/43.25 % (1210863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.71/43.25 % (1210863)CaDiCaL version: 2.1.3 % 299.71/43.25 % (1210863)Termination reason: Instruction limit % 299.71/43.25 % (1210863)Termination phase: Saturation % 299.71/43.25 % (1210863)Time elapsed: 0.160 s % 299.71/43.25 % (1210863)Peak memory usage: 92 MB % 299.71/43.25 % (1210863)Instructions burned: 301 (million) % 299.71/43.25 % (1210866)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=3358509681:i=28310:bd=all:rtra=on_2634 on theBenchmark for (2634ds/28310Mi) % 299.71/43.25 % Exception at run slice level % 299.71/43.25 User error: GNN currently only supports monomorphic FOL. % 299.71/43.25 % (1210860)Instruction limit reached! % 299.71/43.25 % (1210860)------------------------------ % 299.71/43.25 % (1210860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.71/43.25 % (1210860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.71/43.25 % (1210860)CaDiCaL version: 2.1.3 % 299.71/43.25 % (1210860)Termination reason: Instruction limit % 299.71/43.25 % (1210860)Termination phase: Saturation % 299.71/43.25 % (1210860)Time elapsed: 0.678 s % 299.71/43.25 % (1210860)Peak memory usage: 94 MB % 299.71/43.25 % (1210860)Instructions burned: 863 (million) % 299.71/43.25 % (1210868)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3632709631:i=1334:av=off:fsr=off:rtra=on_2631 on theBenchmark for (2631ds/1334Mi) % 299.71/43.25 % Exception at run slice level % 299.71/43.25 User error: GNN currently only supports monomorphic FOL. % 299.71/43.25 % (1210869)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=684752695:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2631 on theBenchmark for (2631ds/370Mi) % 299.71/43.25 % (1210871)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=1142560029:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2629 on theBenchmark for (2629ds/386Mi) % 299.71/43.25 % (1210768)Instruction limit reached! % 299.71/43.25 % (1210768)------------------------------ % 299.71/43.25 % (1210768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.71/43.25 % (1210768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.71/43.25 % (1210768)CaDiCaL version: 2.1.3 % 299.71/43.25 % (1210768)Termination reason: Instruction limit % 299.71/43.25 % (1210768)Termination phase: Saturation % 299.71/43.25 % (1210768)Time elapsed: 13.968 s % 299.71/43.25 % (1210768)Peak memory usage: 88 MB % 299.71/43.25 % (1210768)Instructions burned: 23714 (million) % 299.71/43.25 % (1210871)Instruction limit reached! % 299.71/43.25 % (1210871)------------------------------ % 299.71/43.25 % (1210871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.71/43.25 % (1210871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.71/43.25 % (1210871)CaDiCaL version: 2.1.3 % 299.71/43.25 % (1210871)Termination reason: Instruction limit % 299.71/43.25 % (1210871)Termination phase: Saturation % 299.71/43.25 % (1210871)Time elapsed: 0.201 s % 299.71/43.25 % (1210871)Peak memory usage: 92 MB % 299.71/43.25 % (1210871)Instructions burned: 387 (million) % 299.71/43.25 % (1210869)Instruction limit reached! % 299.71/43.25 % (1210869)------------------------------ % 299.71/43.25 % (1210869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.71/43.25 % (1210869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.71/43.25 % (1210869)CaDiCaL version: 2.1.3 % 299.71/43.25 % (1210869)Termination reason: Instruction limit % 300.28/43.32 % (1210869)Termination phase: Saturation % 300.28/43.32 % (1210869)Time elapsed: 0.361 s % 300.28/43.32 % (1210869)Peak memory usage: 92 MB % 300.28/43.32 % (1210869)Instructions burned: 370 (million) % 300.28/43.32 % (1210874)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=1004347739:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2626 on theBenchmark for (2626ds/9700Mi) % 300.28/43.32 % (1210876)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=2859460123:i=638:kws=precedence:fsr=off:rtra=on_2625 on theBenchmark for (2625ds/638Mi) % 300.28/43.32 % (1210875)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:si=on:sp=const_frequency:acc=on:urr=on:random_seed=1252804870:i=24222:sd=1:rtra=on:ss=included_2625 on theBenchmark for (2625ds/24222Mi) % 300.28/43.32 % (1210876)Instruction limit reached! % 300.28/43.32 % (1210876)------------------------------ % 300.28/43.32 % (1210876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.28/43.32 % (1210876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.28/43.32 % (1210876)CaDiCaL version: 2.1.3 % 300.28/43.32 % (1210876)Termination reason: Instruction limit % 300.28/43.32 % (1210876)Termination phase: Saturation % 300.28/43.32 % (1210876)Time elapsed: 0.419 s % 300.28/43.32 % (1210876)Peak memory usage: 89 MB % 300.28/43.32 % (1210876)Instructions burned: 638 (million) % 300.28/43.32 % (1210868)Instruction limit reached! % 300.28/43.32 % (1210868)------------------------------ % 300.28/43.32 % (1210868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.28/43.32 % (1210868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.28/43.32 % (1210868)CaDiCaL version: 2.1.3 % 300.28/43.32 % (1210868)Termination reason: Instruction limit % 300.28/43.32 % (1210868)Termination phase: Saturation % 300.28/43.32 % (1210868)Time elapsed: 1.123 s % 300.28/43.32 % (1210868)Peak memory usage: 99 MB % 300.28/43.32 % (1210868)Instructions burned: 1334 (million) % 300.28/43.32 % Exception at run slice level % 300.28/43.32 User error: GNN currently only supports monomorphic FOL. % 300.28/43.32 % (1210880)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3119709640:i=4128:ep=RST:rtra=on_2619 on theBenchmark for (2619ds/4128Mi) % 300.28/43.32 % (1210881)dis-1011_128_sil=32000:si=on:random_seed=965958552:i=7412:ep=RST:av=off:rtra=on_2618 on theBenchmark for (2618ds/7412Mi) % 300.28/43.32 % (1210882)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=4268517135:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2617 on theBenchmark for (2617ds/1514Mi) % 300.28/43.32 % (1210882)Instruction limit reached! % 300.28/43.32 % (1210882)------------------------------ % 300.28/43.32 % (1210882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.28/43.32 % (1210882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.28/43.32 % (1210882)CaDiCaL version: 2.1.3 % 300.28/43.32 % (1210882)Termination reason: Instruction limit % 300.28/43.32 % (1210882)Termination phase: Saturation % 300.28/43.32 % (1210882)Time elapsed: 1.581 s % 300.28/43.32 % (1210882)Peak memory usage: 99 MB % 300.28/43.32 % (1210882)Instructions burned: 1514 (million) % 300.28/43.32 % (1210892)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=2129180769:i=27826:rtra=on:ss=axioms:sgt=8_2599 on theBenchmark for (2599ds/27826Mi) % 300.28/43.32 % (1210880)Instruction limit reached! % 300.28/43.32 % (1210880)------------------------------ % 300.28/43.32 % (1210880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.28/43.32 % (1210880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.28/43.32 % (1210880)CaDiCaL version: 2.1.3 % 300.28/43.32 % (1210880)Termination reason: Instruction limit % 300.28/43.32 % (1210880)Termination phase: Saturation % 300.28/43.32 % (1210880)Time elapsed: 2.477 s % 300.28/43.32 % (1210880)Peak memory usage: 89 MB % 300.28/43.32 % (1210880)Instructions burned: 4129 (million) % 300.28/43.32 % Exception at run slice level % 300.28/43.32 User error: GNN currently only supports monomorphic FOL. % 300.28/43.32 % (1210894)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=1227496521:i=19850:aac=none:rtra=on_2592 on theBenchmark for (2592ds/19850Mi) % 300.28/43.32 % (1210895)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2561624918:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2591 on theBenchmark for (259 % 300.28/43.33 Terminated %------------------------------------------------------------------------------