%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : COM025_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 : n003.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 09:39:26 AM UTC 2026 % Result : Timeout 296.65s 42.58s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : COM025_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.07/0.19 % Computer : n003.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.20 % CPULimit : 300 % 0.07/0.20 % WCLimit : 300 % 0.07/0.20 % DateTime : Mon Sep 28 21:50:43 UTC 2026 % 0.07/0.20 % CPUTime : % 0.07/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.07/0.23 Running first-order theorem proving % 0.07/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 % 6.78/1.81 % (2067128)Detected formulas, will run a generic FOF schedule. % 6.78/1.81 % (2067136)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1342173543:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 6.78/1.81 % (2067136)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 6.78/1.81 % (2067136)Refutation not found, incomplete strategy % 6.78/1.81 % (2067136)------------------------------ % 6.78/1.81 % (2067136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.78/1.81 % (2067136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.78/1.81 % (2067136)CaDiCaL version: 2.1.3 % 6.78/1.81 % (2067136)Termination reason: Refutation not found, incomplete strategy % 6.78/1.81 % (2067136)Time elapsed: 0.002 s % 6.78/1.81 % (2067136)Peak memory usage: 88 MB % 6.78/1.81 % (2067136)Instructions burned: 3 (million) % 6.78/1.81 % (2067137)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2854423229:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 6.78/1.81 % (2067134)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=1125285285:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 6.78/1.81 % (2067135)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=2198757588:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 6.78/1.81 % (2067138)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=745641236:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 6.78/1.81 % (2067133)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=4204291508:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 6.78/1.81 % (2067135)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 6.78/1.81 % (2067139)dis-21_1_sil=8000:lcm=predicate:random_seed=2527067620: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) % 6.78/1.81 % (2067137)Instruction limit reached! % 6.78/1.81 % (2067137)------------------------------ % 6.78/1.81 % (2067137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.78/1.81 % (2067137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.78/1.81 % (2067137)CaDiCaL version: 2.1.3 % 6.78/1.81 % (2067137)Termination reason: Instruction limit % 6.78/1.81 % (2067137)Termination phase: Saturation % 6.78/1.81 % (2067137)Time elapsed: 0.066 s % 6.78/1.81 % (2067137)Peak memory usage: 88 MB % 6.78/1.81 % (2067137)Instructions burned: 119 (million) % 6.78/1.81 % (2067139)Instruction limit reached! % 6.78/1.81 % (2067139)------------------------------ % 6.78/1.81 % (2067139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.78/1.81 % (2067139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.78/1.81 % (2067139)CaDiCaL version: 2.1.3 % 6.78/1.81 % (2067139)Termination reason: Instruction limit % 6.78/1.81 % (2067139)Termination phase: Saturation % 6.78/1.81 % (2067139)Time elapsed: 0.071 s % 6.78/1.81 % (2067139)Peak memory usage: 89 MB % 6.78/1.81 % (2067139)Instructions burned: 129 (million) % 6.78/1.81 % (2067138)Instruction limit reached! % 6.78/1.81 % (2067138)------------------------------ % 6.78/1.81 % (2067138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.78/1.81 % (2067138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.78/1.81 % (2067138)CaDiCaL version: 2.1.3 % 6.78/1.81 % (2067138)Termination reason: Instruction limit % 6.78/1.81 % (2067138)Termination phase: Saturation % 6.78/1.81 % (2067138)Time elapsed: 0.094 s % 6.78/1.81 % (2067138)Peak memory usage: 89 MB % 6.78/1.81 % (2067138)Instructions burned: 139 (million) % 6.78/1.81 % (2067136)------------------------------ % 6.78/1.81 % (2067136)------------------------------ % 6.78/1.81 % (2067150)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=28139025:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 6.78/1.81 % (2067147)lrs+10_1_sil=8000:sp=occurrence:random_seed=1827375260:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 6.78/1.81 % (2067148)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1183070082:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 9.95/2.09 % (2067149)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2737823625:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 9.95/2.09 % (2067150)Instruction limit reached! % 9.95/2.09 % (2067150)------------------------------ % 9.95/2.09 % (2067150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.95/2.09 % (2067150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.95/2.09 % (2067150)CaDiCaL version: 2.1.3 % 9.95/2.09 % (2067150)Termination reason: Instruction limit % 9.95/2.09 % (2067150)Termination phase: Saturation % 9.95/2.09 % (2067150)Time elapsed: 0.076 s % 9.95/2.09 % (2067150)Peak memory usage: 90 MB % 9.95/2.09 % (2067150)Instructions burned: 249 (million) % 9.95/2.09 % (2067148)Instruction limit reached! % 9.95/2.09 % (2067148)------------------------------ % 9.95/2.09 % (2067148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.95/2.09 % (2067148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.95/2.10 % (2067148)CaDiCaL version: 2.1.3 % 9.95/2.10 % (2067148)Termination reason: Instruction limit % 9.95/2.10 % (2067148)Termination phase: Saturation % 9.95/2.10 % (2067148)Time elapsed: 0.093 s % 9.95/2.10 % (2067148)Peak memory usage: 89 MB % 9.95/2.10 % (2067148)Instructions burned: 157 (million) % 9.95/2.10 % Exception at run slice level % 9.95/2.10 User error: GNN currently only supports monomorphic FOL.% Exception at run slice level % 9.95/2.10 % 9.95/2.10 User error: GNN currently only supports monomorphic FOL. % 9.95/2.10 % Exception at run slice level % 9.95/2.10 User error: GNN currently only supports monomorphic FOL. % 9.95/2.10 % (2067147)Instruction limit reached! % 9.95/2.10 % (2067147)------------------------------ % 9.95/2.10 % (2067147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.95/2.10 % (2067147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.95/2.10 % (2067147)CaDiCaL version: 2.1.3 % 9.95/2.10 % (2067147)Termination reason: Instruction limit % 9.95/2.10 % (2067147)Termination phase: Saturation % 9.95/2.10 % (2067147)Time elapsed: 0.165 s % 9.95/2.10 % (2067147)Peak memory usage: 91 MB % 9.95/2.10 % (2067147)Instructions burned: 287 (million) % 9.95/2.10 % (2067155)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1230598090:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 9.95/2.10 % (2067149)Instruction limit reached! % 9.95/2.10 % (2067149)------------------------------ % 9.95/2.10 % (2067149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.95/2.10 % (2067149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.95/2.10 % (2067149)CaDiCaL version: 2.1.3 % 9.95/2.10 % (2067149)Termination reason: Instruction limit % 9.95/2.10 % (2067149)Termination phase: Saturation % 9.95/2.10 % (2067149)Time elapsed: 0.209 s % 9.95/2.10 % (2067149)Peak memory usage: 91 MB % 9.95/2.10 % (2067149)Instructions burned: 326 (million) % 9.95/2.10 % (2067156)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1976426240:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 9.95/2.10 % (2067155)Instruction limit reached! % 9.95/2.10 % (2067155)------------------------------ % 9.95/2.10 % (2067155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.95/2.10 % (2067155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.95/2.10 % (2067155)CaDiCaL version: 2.1.3 % 9.95/2.10 % (2067155)Termination reason: Instruction limit % 9.95/2.10 % (2067155)Termination phase: Saturation % 9.95/2.10 % (2067155)Time elapsed: 0.093 s % 9.95/2.10 % (2067155)Peak memory usage: 90 MB % 9.95/2.10 % (2067155)Instructions burned: 296 (million) % 9.95/2.10 % (2067157)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1970092077:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 9.95/2.10 % (2067158)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4019012898:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 9.95/2.10 % (2067159)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1373637340:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 9.95/2.10 % (2067160)lrs+10_1_sil=8000:sp=occurrence:random_seed=448407788:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 9.95/2.10 % (2067158)Instruction limit reached! % 11.01/2.47 % (2067158)------------------------------ % 11.01/2.47 % (2067158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.01/2.47 % (2067158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.01/2.47 % (2067158)CaDiCaL version: 2.1.3 % 11.01/2.47 % (2067158)Termination reason: Instruction limit % 11.01/2.47 % (2067158)Termination phase: Saturation % 11.01/2.47 % (2067158)Time elapsed: 0.061 s % 11.01/2.47 % (2067158)Peak memory usage: 88 MB % 11.01/2.47 % (2067158)Instructions burned: 128 (million) % 11.01/2.47 % (2067159)Instruction limit reached! % 11.01/2.47 % (2067159)------------------------------ % 11.01/2.47 % (2067159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.01/2.47 % (2067159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.01/2.47 % (2067159)CaDiCaL version: 2.1.3 % 11.01/2.47 % (2067159)Termination reason: Instruction limit % 11.01/2.47 % (2067159)Termination phase: Saturation % 11.01/2.47 % (2067159)Time elapsed: 0.061 s % 11.01/2.47 % (2067159)Peak memory usage: 89 MB % 11.01/2.47 % (2067159)Instructions burned: 116 (million) % 11.01/2.47 % (2067157)Instruction limit reached! % 11.01/2.47 % (2067157)------------------------------ % 11.01/2.47 % (2067157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.01/2.47 % (2067157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.01/2.47 % (2067157)CaDiCaL version: 2.1.3 % 11.01/2.47 % (2067157)Termination reason: Instruction limit % 11.01/2.47 % (2067157)Termination phase: Saturation % 11.01/2.47 % (2067157)Time elapsed: 0.075 s % 11.01/2.47 % (2067157)Peak memory usage: 89 MB % 11.01/2.47 % (2067157)Instructions burned: 114 (million) % 11.01/2.47 % (2067162)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1198153103:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi) % 11.01/2.47 % (2067164)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2465316266:i=5202:ss=axioms:sgt=16_2993 on theBenchmark for (2993ds/5202Mi) % 11.01/2.47 % (2067169)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=487395870:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2992 on theBenchmark for (2992ds/134Mi) % 11.01/2.47 % (2067170)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1495097422:st=8:i=592:sd=3:ep=RST:ss=axioms_2992 on theBenchmark for (2992ds/592Mi) % 11.01/2.47 % (2067171)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2277321123:st=3:i=13193:sd=3:ss=axioms_2992 on theBenchmark for (2992ds/13193Mi) % 11.01/2.47 % Exception at run slice level % 11.01/2.47 User error: GNN currently only supports monomorphic FOL. % 11.01/2.47 % (2067169)Instruction limit reached! % 11.01/2.47 % (2067169)------------------------------ % 11.01/2.47 % (2067169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.01/2.47 % (2067169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.01/2.47 % (2067169)CaDiCaL version: 2.1.3 % 11.01/2.47 % (2067169)Termination reason: Instruction limit % 11.01/2.47 % (2067169)Termination phase: Saturation % 11.01/2.47 % (2067169)Time elapsed: 0.079 s % 11.01/2.47 % (2067169)Peak memory usage: 90 MB % 11.01/2.47 % (2067169)Instructions burned: 134 (million) % 11.01/2.47 % Exception at run slice level % 11.01/2.47 User error: GNN currently only supports monomorphic FOL. % 11.01/2.47 % (2067162)Instruction limit reached! % 11.01/2.47 % (2067162)------------------------------ % 11.01/2.47 % (2067162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.01/2.47 % (2067162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.01/2.47 % (2067162)CaDiCaL version: 2.1.3 % 11.01/2.47 % (2067162)Termination reason: Instruction limit % 11.01/2.47 % (2067162)Termination phase: Saturation % 11.01/2.47 % (2067162)Time elapsed: 0.242 s % 11.01/2.47 % (2067162)Peak memory usage: 91 MB % 11.01/2.47 % (2067162)Instructions burned: 439 (million) % 11.01/2.47 % (2067178)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3872395927:i=134:gtgl=5:slsql=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/134Mi) % 11.01/2.47 % Exception at run slice level % 11.01/2.47 User error: Immediate (shared) subterms of term/literal aa(X1,fun(list(X1),X0),X4,X3) = sF27(X1,X0,X4,X3) have different types/not well-typed! % 11.01/2.47 % (2067177)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=1294755975:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/125Mi) % 18.87/3.46 % (2067177)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 18.87/3.46 % (2067179)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1977767060:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/141Mi) % 18.87/3.46 % (2067180)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2288627596:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/431Mi) % 18.87/3.46 % (2067179)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 18.87/3.46 % (2067179)Refutation not found, incomplete strategy % 18.87/3.46 % (2067179)------------------------------ % 18.87/3.46 % (2067179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.87/3.46 % (2067179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.87/3.46 % (2067179)CaDiCaL version: 2.1.3 % 18.87/3.46 % (2067179)Termination reason: Refutation not found, incomplete strategy % 18.87/3.46 % (2067179)Time elapsed: 0.003 s % 18.87/3.46 % (2067179)Peak memory usage: 88 MB % 18.87/3.46 % (2067179)Instructions burned: 2 (million) % 18.87/3.46 % (2067180)Refutation not found, incomplete strategy % 18.87/3.46 % (2067180)------------------------------ % 18.87/3.46 % (2067180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.87/3.46 % (2067180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.87/3.46 % (2067180)CaDiCaL version: 2.1.3 % 18.87/3.46 % (2067180)Termination reason: Refutation not found, incomplete strategy % 18.87/3.46 % (2067180)Time elapsed: 0.012 s % 18.87/3.46 % (2067180)Peak memory usage: 89 MB % 18.87/3.46 % (2067180)Instructions burned: 20 (million) % 18.87/3.46 % (2067177)Instruction limit reached! % 18.87/3.46 % (2067177)------------------------------ % 18.87/3.46 % (2067177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.87/3.46 % (2067177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.87/3.46 % (2067177)CaDiCaL version: 2.1.3 % 18.87/3.46 % (2067177)Termination reason: Instruction limit % 18.87/3.46 % (2067177)Termination phase: Saturation % 18.87/3.46 % (2067177)Time elapsed: 0.086 s % 18.87/3.46 % (2067177)Peak memory usage: 90 MB % 18.87/3.46 % (2067177)Instructions burned: 125 (million) % 18.87/3.46 % (2067182)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=548429320:i=6060:aac=none:ins=25_2989 on theBenchmark for (2989ds/6060Mi) % 18.87/3.46 % (2067170)Instruction limit reached! % 18.87/3.46 % (2067170)------------------------------ % 18.87/3.46 % (2067170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.87/3.46 % (2067170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.87/3.46 % (2067170)CaDiCaL version: 2.1.3 % 18.87/3.46 % (2067170)Termination reason: Instruction limit % 18.87/3.46 % (2067170)Termination phase: Saturation % 18.87/3.46 % (2067170)Time elapsed: 0.344 s % 18.87/3.46 % (2067170)Peak memory usage: 94 MB % 18.87/3.46 % (2067170)Instructions burned: 594 (million) % 18.87/3.46 % (2067160)Instruction limit reached! % 18.87/3.46 % (2067160)------------------------------ % 18.87/3.46 % (2067160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.87/3.46 % (2067160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.87/3.46 % (2067160)CaDiCaL version: 2.1.3 % 18.87/3.46 % (2067160)Termination reason: Instruction limit % 18.87/3.46 % (2067160)Termination phase: Saturation % 18.87/3.46 % (2067160)Time elapsed: 0.558 s % 18.87/3.46 % (2067160)Peak memory usage: 96 MB % 18.87/3.46 % (2067160)Instructions burned: 907 (million) % 18.87/3.46 % Exception at run slice level % 18.87/3.46 User error: GNN currently only supports monomorphic FOL. % 18.87/3.46 % (2067187)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=849244046:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2987 on theBenchmark for (2987ds/150Mi) % 18.87/3.46 % (2067187)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 18.87/3.46 % (2067179)------------------------------ % 18.87/3.46 % (2067179)------------------------------ % 18.87/3.46 % (2067180)------------------------------ % 18.87/3.46 % (2067180)------------------------------ % 24.52/4.15 % Exception at run slice level % 24.52/4.15 User error: GNN currently only supports monomorphic FOL. % 24.52/4.15 % (2067188)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3994054165:i=14155:bd=all_2987 on theBenchmark for (2987ds/14155Mi) % 24.52/4.15 % (2067189)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3923111734:i=667:av=off:fsr=off_2987 on theBenchmark for (2987ds/667Mi) % 24.52/4.15 % (2067190)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=3023300642:s2a=on:i=185:s2at=1.8:fdi=4_2987 on theBenchmark for (2987ds/185Mi) % 24.52/4.15 % (2067187)Instruction limit reached! % 24.52/4.15 % (2067187)------------------------------ % 24.52/4.15 % (2067187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.52/4.15 % (2067187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.52/4.15 % (2067187)CaDiCaL version: 2.1.3 % 24.52/4.15 % (2067187)Termination reason: Instruction limit % 24.52/4.15 % (2067187)Termination phase: Saturation % 24.52/4.15 % (2067187)Time elapsed: 0.095 s % 24.52/4.15 % (2067187)Peak memory usage: 90 MB % 24.52/4.15 % (2067187)Instructions burned: 150 (million) % 24.52/4.15 % (2067194)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1575942454:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2985 on theBenchmark for (2985ds/193Mi) % 24.52/4.15 % (2067190)Instruction limit reached! % 24.52/4.15 % (2067190)------------------------------ % 24.52/4.15 % (2067190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.52/4.15 % (2067190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.52/4.15 % (2067190)CaDiCaL version: 2.1.3 % 24.52/4.15 % (2067190)Termination reason: Instruction limit % 24.52/4.15 % (2067190)Termination phase: Saturation % 24.52/4.15 % (2067190)Time elapsed: 0.117 s % 24.52/4.15 % (2067190)Peak memory usage: 91 MB % 24.52/4.15 % (2067190)Instructions burned: 185 (million) % 24.52/4.15 % (2067194)Instruction limit reached! % 24.52/4.15 % (2067194)------------------------------ % 24.52/4.15 % (2067194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.52/4.15 % (2067194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.52/4.15 % (2067194)CaDiCaL version: 2.1.3 % 24.52/4.15 % (2067194)Termination reason: Instruction limit % 24.52/4.15 % (2067194)Termination phase: Saturation % 24.52/4.15 % (2067194)Time elapsed: 0.050 s % 24.52/4.15 % (2067194)Peak memory usage: 89 MB % 24.52/4.15 % (2067194)Instructions burned: 194 (million) % 24.52/4.15 % (2067196)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3054108545:i=12111:sd=1:ss=included_2985 on theBenchmark for (2985ds/12111Mi) % 24.52/4.15 % (2067195)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2450993442:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2985 on theBenchmark for (2985ds/4850Mi) % 24.52/4.15 % (2067198)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=895510994:i=319:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/319Mi) % 24.52/4.15 % (2067203)dis-1011_128_sil=32000:random_seed=3066113180:i=3706:ep=RST:av=off_2984 on theBenchmark for (2984ds/3706Mi) % 24.52/4.15 % (2067200)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=197080290:i=2064:ep=RST_2984 on theBenchmark for (2984ds/2064Mi) % 24.52/4.15 % (2067189)Instruction limit reached! % 24.52/4.15 % (2067189)------------------------------ % 24.52/4.15 % (2067189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.52/4.15 % (2067189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.52/4.15 % (2067189)CaDiCaL version: 2.1.3 % 24.52/4.15 % (2067189)Termination reason: Instruction limit % 24.52/4.15 % (2067189)Termination phase: Saturation % 24.52/4.15 % (2067189)Time elapsed: 0.294 s % 24.52/4.15 % (2067189)Peak memory usage: 90 MB % 24.52/4.15 % (2067189)Instructions burned: 668 (million) % 24.52/4.15 % Exception at run slice level % 24.52/4.15 User error: GNN currently only supports monomorphic FOL. % 24.52/4.15 % (2067198)Instruction limit reached! % 24.52/4.15 % (2067198)------------------------------ % 24.52/4.15 % (2067198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.52/4.15 % (2067198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.62/5.31 % (2067198)CaDiCaL version: 2.1.3 % 32.62/5.31 % (2067198)Termination reason: Instruction limit % 32.62/5.31 % (2067198)Termination phase: Saturation % 32.62/5.31 % (2067198)Time elapsed: 0.183 s % 32.62/5.31 % (2067198)Peak memory usage: 92 MB % 32.62/5.31 % (2067198)Instructions burned: 320 (million) % 32.62/5.31 % (2067207)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=870058771:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2982 on theBenchmark for (2982ds/757Mi) % 32.62/5.31 % (2067209)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3383349843:i=9925:aac=none_2982 on theBenchmark for (2982ds/9925Mi) % 32.62/5.31 % (2067208)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3824153279:i=13913:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/13913Mi) % 32.62/5.31 % Exception at run slice level % 32.62/5.31 User error: GNN currently only supports monomorphic FOL. % 32.62/5.31 % (2067213)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2448133852:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2980 on theBenchmark for (2980ds/2479Mi) % 32.62/5.31 % (2067213)Refutation not found, incomplete strategy % 32.62/5.31 % (2067213)------------------------------ % 32.62/5.31 % (2067213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.62/5.31 % (2067213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.62/5.31 % (2067213)CaDiCaL version: 2.1.3 % 32.62/5.31 % (2067213)Termination reason: Refutation not found, incomplete strategy % 32.62/5.31 % (2067213)Time elapsed: 0.004 s % 32.62/5.31 % (2067213)Peak memory usage: 88 MB % 32.62/5.31 % (2067213)Instructions burned: 4 (million) % 32.62/5.31 % Exception at run slice level% Exception at run slice level % 32.62/5.31 % 32.62/5.31 User error: User error: GNN currently only supports monomorphic FOL.GNN currently only supports monomorphic FOL. % 32.62/5.31 % 32.62/5.31 % (2067207)Instruction limit reached! % 32.62/5.31 % (2067207)------------------------------ % 32.62/5.31 % (2067207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.62/5.31 % (2067207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.62/5.31 % (2067207)CaDiCaL version: 2.1.3 % 32.62/5.31 % (2067207)Termination reason: Instruction limit % 32.62/5.31 % (2067207)Termination phase: Saturation % 32.62/5.31 % (2067207)Time elapsed: 0.450 s % 32.62/5.31 % (2067207)Peak memory usage: 96 MB % 32.62/5.31 % (2067207)Instructions burned: 757 (million) % 32.62/5.31 % (2067213)------------------------------ % 32.62/5.31 % (2067213)------------------------------ % 32.62/5.31 % (2067216)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3691860942:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2977 on theBenchmark for (2977ds/11145Mi) % 32.62/5.31 % (2067215)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=477215135:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2977 on theBenchmark for (2977ds/440Mi) % 32.62/5.31 % (2067215)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 32.62/5.31 % (2067217)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=1203906457:cts=off:i=3034:av=off:er=known:fsd=on_2976 on theBenchmark for (2976ds/3034Mi) % 32.62/5.31 % (2067218)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3035925495:st=2:s2a=on:i=524:s2at=2:ss=axioms_2976 on theBenchmark for (2976ds/524Mi) % 32.62/5.31 % (2067215)Instruction limit reached! % 32.62/5.31 % (2067215)------------------------------ % 32.62/5.31 % (2067215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.62/5.31 % (2067215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.62/5.31 % (2067215)CaDiCaL version: 2.1.3 % 32.62/5.31 % (2067215)Termination reason: Instruction limit % 32.62/5.31 % (2067215)Termination phase: Saturation % 32.62/5.31 % (2067215)Time elapsed: 0.256 s % 32.62/5.31 % (2067215)Peak memory usage: 92 MB % 32.62/5.31 % (2067215)Instructions burned: 441 (million) % 32.62/5.31 % (2067218)Instruction limit reached! % 32.62/5.31 % (2067218)------------------------------ % 32.62/5.31 % (2067218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.62/5.31 % (2067218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.62/5.31 % (2067218)CaDiCaL version: 2.1.3 % 32.62/5.31 % (2067218)Termination reason: Instruction limit % 40.28/6.42 % (2067218)Termination phase: Saturation % 40.28/6.42 % (2067218)Time elapsed: 0.273 s % 40.28/6.42 % (2067218)Peak memory usage: 91 MB % 40.28/6.42 % (2067218)Instructions burned: 524 (million) % 40.28/6.42 % (2067200)Instruction limit reached! % 40.28/6.42 % (2067200)------------------------------ % 40.28/6.42 % (2067200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.28/6.42 % (2067200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.28/6.42 % (2067200)CaDiCaL version: 2.1.3 % 40.28/6.42 % (2067200)Termination reason: Instruction limit % 40.28/6.42 % (2067200)Termination phase: Saturation % 40.28/6.42 % (2067200)Time elapsed: 1.093 s % 40.28/6.42 % (2067200)Peak memory usage: 99 MB % 40.28/6.42 % (2067200)Instructions burned: 2066 (million) % 40.28/6.42 % Exception at run slice level % 40.28/6.42 User error: GNN currently only supports monomorphic FOL. % 40.28/6.42 % Exception at run slice level % 40.28/6.42 User error: GNN currently only supports monomorphic FOL. % 40.28/6.42 % (2067223)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=521233387:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2972 on theBenchmark for (2972ds/1016Mi) % 40.28/6.42 % (2067203)Instruction limit reached! % 40.28/6.42 % (2067203)------------------------------ % 40.28/6.42 % (2067203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.28/6.42 % (2067203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.28/6.42 % (2067203)CaDiCaL version: 2.1.3 % 40.28/6.42 % (2067203)Termination reason: Instruction limit % 40.28/6.42 % (2067203)Termination phase: Saturation % 40.28/6.42 % (2067203)Time elapsed: 1.174 s % 40.28/6.42 % (2067203)Peak memory usage: 108 MB % 40.28/6.42 % (2067203)Instructions burned: 3706 (million) % 40.28/6.42 % (2067224)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2477981804:i=14123:bd=preordered:ins=4_2972 on theBenchmark for (2972ds/14123Mi) % 40.28/6.42 % (2067225)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1970642642:i=5781:kws=precedence:bd=all:rawr=on_2972 on theBenchmark for (2972ds/5781Mi) % 40.28/6.42 % (2067226)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=1365451997:i=2448:gtgl=5:bd=preordered:gtg=all_2971 on theBenchmark for (2971ds/2448Mi) % 40.28/6.42 % (2067227)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=24944355:i=3223:kws=precedence:fgj=on:av=off_2971 on theBenchmark for (2971ds/3223Mi) % 40.28/6.42 % (2067229)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3139061985:st=5.6:i=2033:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/2033Mi) % 40.28/6.42 % Exception at run slice level % 40.28/6.42 User error: GNN currently only supports monomorphic FOL. % 40.28/6.42 % Exception at run slice level % 40.28/6.42 User error: GNN currently only supports monomorphic FOL. % 40.28/6.42 % (2067235)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2493805207:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2968 on theBenchmark for (2968ds/2055Mi) % 40.28/6.42 % Exception at run slice level % 40.28/6.42 User error: GNN currently only supports monomorphic FOL. % 40.28/6.42 % Exception at run slice level % 40.28/6.42 User error: GNN currently only supports monomorphic FOL. % 40.28/6.42 % (2067223)Instruction limit reached! % 40.28/6.42 % (2067223)------------------------------ % 40.28/6.42 % (2067223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.28/6.42 % (2067223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.28/6.42 % (2067223)CaDiCaL version: 2.1.3 % 40.28/6.42 % (2067223)Termination reason: Instruction limit % 40.28/6.42 % (2067223)Termination phase: Saturation % 40.28/6.42 % (2067223)Time elapsed: 0.505 s % 40.28/6.42 % (2067223)Peak memory usage: 93 MB % 40.28/6.42 % (2067223)Instructions burned: 1018 (million) % 40.28/6.42 % (2067236)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=1481614771:i=21611:sd=3:ss=axioms_2967 on theBenchmark for (2967ds/21611Mi) % 40.28/6.42 % (2067239)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=2640102666:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2966 on theBenchmark for (2966ds/797Mi) % 51.14/7.96 % (2067238)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3585396768:i=4835:sd=13:ss=axioms:sgt=23_2966 on theBenchmark for (2966ds/4835Mi) % 51.14/7.96 % Exception at run slice level % 51.14/7.96 User error: GNN currently only supports monomorphic FOL. % 51.14/7.96 % (2067240)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=685284363:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2966 on theBenchmark for (2966ds/2326Mi) % 51.14/7.96 % (2067244)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2491979598:i=6038:nm=6_2965 on theBenchmark for (2965ds/6038Mi) % 51.14/7.96 % Exception at run slice level % 51.14/7.96 User error: GNN currently only supports monomorphic FOL. % 51.14/7.96 % Exception at run slice level % 51.14/7.96 User error: GNN currently only supports monomorphic FOL. % 51.14/7.96 % (2067239)Instruction limit reached! % 51.14/7.96 % (2067239)------------------------------ % 51.14/7.96 % (2067239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.14/7.96 % (2067239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.14/7.96 % (2067239)CaDiCaL version: 2.1.3 % 51.14/7.96 % (2067239)Termination reason: Instruction limit % 51.14/7.96 % (2067239)Termination phase: Saturation % 51.14/7.96 % (2067239)Time elapsed: 0.373 s % 51.14/7.96 % (2067239)Peak memory usage: 89 MB % 51.14/7.96 % (2067239)Instructions burned: 799 (million) % 51.14/7.96 % (2067248)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=4152241733:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2961 on theBenchmark for (2961ds/1008Mi) % 51.14/7.96 % (2067247)lrs+10_1_sil=32000:sp=occurrence:random_seed=1589620476:st=2:i=33334:sd=3:ss=included:sgt=32_2962 on theBenchmark for (2962ds/33334Mi) % 51.14/7.96 % (2067249)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=2047079824:i=8327:s2at=5:bd=preordered_2961 on theBenchmark for (2961ds/8327Mi) % 51.14/7.96 % (2067248)Instruction limit reached! % 51.14/7.96 % (2067248)------------------------------ % 51.14/7.96 % (2067248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.14/7.96 % (2067248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.14/7.96 % (2067248)CaDiCaL version: 2.1.3 % 51.14/7.96 % (2067248)Termination reason: Instruction limit % 51.14/7.96 % (2067248)Termination phase: Saturation % 51.14/7.96 % (2067248)Time elapsed: 0.282 s % 51.14/7.96 % (2067248)Peak memory usage: 98 MB % 51.14/7.96 % (2067248)Instructions burned: 1011 (million) % 51.14/7.96 % (2067253)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=2171049693:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2957 on theBenchmark for (2957ds/1083Mi) % 51.14/7.96 % Exception at run slice level % 51.14/7.96 User error: GNN currently only supports monomorphic FOL. % 51.14/7.96 % (2067195)Instruction limit reached! % 51.14/7.96 % (2067195)------------------------------ % 51.14/7.96 % (2067195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.14/7.96 % (2067195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.14/7.96 % (2067195)CaDiCaL version: 2.1.3 % 51.14/7.96 % (2067195)Termination reason: Instruction limit % 51.14/7.96 % (2067195)Termination phase: Saturation % 51.14/7.96 % (2067195)Time elapsed: 2.791 s % 51.14/7.96 % (2067195)Peak memory usage: 109 MB % 51.14/7.96 % (2067195)Instructions burned: 4852 (million) % 51.14/7.96 % (2067256)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=321440955:i=6995:s2at=5:gtg=all_2956 on theBenchmark for (2956ds/6995Mi) % 51.14/7.96 % (2067255)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2914780288:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2956 on theBenchmark for (2956ds/1084Mi) % 51.14/7.96 % (2067240)Instruction limit reached! % 51.14/7.96 % (2067240)------------------------------ % 51.14/7.96 % (2067240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.14/7.96 % (2067240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.14/7.96 % (2067240)CaDiCaL version: 2.1.3 % 51.14/7.96 % (2067240)Termination reason: Instruction limit % 51.14/7.96 % (2067240)Termination phase: Saturation % 62.54/9.54 % (2067240)Time elapsed: 1.111 s % 62.54/9.54 % (2067240)Peak memory usage: 91 MB % 62.54/9.54 % (2067240)Instructions burned: 2327 (million) % 62.54/9.54 % (2067253)Instruction limit reached! % 62.54/9.54 % (2067253)------------------------------ % 62.54/9.54 % (2067253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.54/9.54 % (2067253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.54/9.54 % (2067253)CaDiCaL version: 2.1.3 % 62.54/9.54 % (2067253)Termination reason: Instruction limit % 62.54/9.54 % (2067253)Termination phase: Saturation % 62.54/9.54 % (2067253)Time elapsed: 0.308 s % 62.54/9.54 % (2067253)Peak memory usage: 98 MB % 62.54/9.54 % (2067253)Instructions burned: 1086 (million) % 62.54/9.54 % (2067260)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2898067683:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2953 on theBenchmark for (2953ds/3372Mi) % 62.54/9.54 % (2067259)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2602499017:st=2:i=6225:sd=15:ss=axioms_2953 on theBenchmark for (2953ds/6225Mi) % 62.54/9.54 % Exception at run slice level % 62.54/9.54 User error: GNN currently only supports monomorphic FOL. % 62.54/9.54 % Exception at run slice level % 62.54/9.54 User error: GNN currently only supports monomorphic FOL. % 62.54/9.54 % (2067263)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2658359409:st=2.3:i=26457:sd=10:ss=included:sgt=8_2950 on theBenchmark for (2950ds/26457Mi) % 62.54/9.54 % (2067264)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=2875568230:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2950 on theBenchmark for (2950ds/13494Mi) % 62.54/9.54 % (2067255)Instruction limit reached! % 62.54/9.54 % (2067255)------------------------------ % 62.54/9.54 % (2067255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.54/9.54 % (2067255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.54/9.54 % (2067255)CaDiCaL version: 2.1.3 % 62.54/9.54 % (2067255)Termination reason: Instruction limit % 62.54/9.54 % (2067255)Termination phase: Saturation % 62.54/9.54 % (2067255)Time elapsed: 0.531 s % 62.54/9.54 % (2067255)Peak memory usage: 97 MB % 62.54/9.54 % (2067255)Instructions burned: 1086 (million) % 62.54/9.54 % (2067267)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=2560921745:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2949 on theBenchmark for (2949ds/2503Mi) % 62.54/9.54 % (2067267)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 62.54/9.54 % Exception at run slice level % 62.54/9.54 User error: GNN currently only supports monomorphic FOL. % 62.54/9.54 % (2067270)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=1371821648:i=2559:sd=1:ep=RSTC:ss=axioms_2947 on theBenchmark for (2947ds/2559Mi) % 62.54/9.54 % Exception at run slice level % 62.54/9.54 User error: GNN currently only supports monomorphic FOL. % 62.54/9.54 % (2067272)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1647120632:i=30753:av=off:ss=included_2945 on theBenchmark for (2945ds/30753Mi) % 62.54/9.54 % Exception at run slice level % 62.54/9.54 User error: GNN currently only supports monomorphic FOL. % 62.54/9.54 % Exception at run slice level % 62.54/9.54 User error: GNN currently only supports monomorphic FOL. % 62.54/9.54 % (2067225)Instruction limit reached! % 62.54/9.54 % (2067225)------------------------------ % 62.54/9.54 % (2067225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.54/9.54 % (2067225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.54/9.54 % (2067225)CaDiCaL version: 2.1.3 % 62.54/9.54 % (2067225)Termination reason: Instruction limit % 62.54/9.54 % (2067225)Termination phase: Saturation % 62.54/9.54 % (2067225)Time elapsed: 2.699 s % 62.54/9.54 % (2067225)Peak memory usage: 119 MB % 62.54/9.54 % (2067225)Instructions burned: 5783 (million) % 62.54/9.54 % (2067274)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=1334428633:i=26473:ep=RSTC_2944 on theBenchmark for (2944ds/26473Mi) % 62.54/9.54 % (2067275)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=2425790131:cts=off:i=2759:kws=inv_arity:fgj=on_2944 on theBenchmark for (2944ds/2759Mi) % 76.23/11.47 % (2067276)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=3233315346:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2943 on theBenchmark for (2943ds/5665Mi) % 76.23/11.47 % (2067276)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 76.23/11.47 % Exception at run slice level % 76.23/11.47 User error: GNN currently only supports monomorphic FOL. % 76.23/11.47 % (2067280)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=3010924550:i=1532:ep=RS:ss=axioms_2940 on theBenchmark for (2940ds/1532Mi) % 76.23/11.47 % Exception at run slice level % 76.23/11.47 User error: GNN currently only supports monomorphic FOL. % 76.23/11.47 % (2067238)Instruction limit reached! % 76.23/11.47 % (2067238)------------------------------ % 76.23/11.47 % (2067238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.23/11.47 % (2067238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.23/11.47 % (2067238)CaDiCaL version: 2.1.3 % 76.23/11.47 % (2067238)Termination reason: Instruction limit % 76.23/11.47 % (2067238)Termination phase: Saturation % 76.23/11.47 % (2067238)Time elapsed: 2.638 s % 76.23/11.47 % (2067238)Peak memory usage: 120 MB % 76.23/11.47 % (2067238)Instructions burned: 4835 (million) % 76.23/11.47 % Exception at run slice level % 76.23/11.47 User error: GNN currently only supports monomorphic FOL. % 76.23/11.47 % (2067282)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=1258304735:i=1565:sd=2:ss=axioms:sgt=32_2938 on theBenchmark for (2938ds/1565Mi) % 76.23/11.47 % (2067283)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=3664832410:i=1572:fgj=on:gsp=on_2938 on theBenchmark for (2938ds/1572Mi) % 76.23/11.47 % (2067283)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 76.23/11.47 % (2067284)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=2493599382:i=6052:sd=4:ss=axioms:sgt=24_2938 on theBenchmark for (2938ds/6052Mi) % 76.23/11.47 % Exception at run slice level % 76.23/11.47 User error: GNN currently only supports monomorphic FOL. % 76.23/11.47 % Exception at run slice level % 76.23/11.47 User error: GNN currently only supports monomorphic FOL. % 76.23/11.47 % Exception at run slice level % 76.23/11.47 User error: GNN currently only supports monomorphic FOL. % 76.23/11.47 % (2067288)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=2671131342:i=3500:sd=1:bd=preordered:sup=off:ss=included_2935 on theBenchmark for (2935ds/3500Mi) % 76.23/11.47 % Exception at run slice level % 76.23/11.47 User error: GNN currently only supports monomorphic FOL. % 76.23/11.47 % (2067291)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1502845937:i=66096:add=on_2933 on theBenchmark for (2933ds/66096Mi) % 76.23/11.47 % (2067290)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=2488114162:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2933 on theBenchmark for (2933ds/1842Mi) % 76.23/11.47 % (2067290)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 76.23/11.47 % (2067292)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=4099454273:i=1884:sd=1:nm=60:ss=axioms_2933 on theBenchmark for (2933ds/1884Mi) % 76.23/11.47 % Exception at run slice level % 76.23/11.47 User error: GNN currently only supports monomorphic FOL. % 76.23/11.47 % Exception at run slice level % 76.23/11.47 User error: GNN currently only supports monomorphic FOL. % 76.23/11.47 % Exception at run slice level % 76.23/11.47 User error: GNN currently only supports monomorphic FOL. % 76.23/11.47 % (2067296)lrs-1011_4:1_sil=16000:bsr=on:random_seed=1062248700:cts=off:i=5469:bs=on:fsr=off_2930 on theBenchmark for (2930ds/5469Mi) % 76.23/11.47 % Exception at run slice level % 76.23/11.47 User error: GNN currently only supports monomorphic FOL. % 76.23/11.47 % (2067297)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=1255711994:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2928 on theBenchmark for (2928ds/2037Mi) % 90.48/13.51 % (2067298)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3549995431:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2928 on theBenchmark for (2928ds/2110Mi) % 90.48/13.51 % (2067300)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=543562738:i=2430:add=off:aac=none:nm=16_2928 on theBenchmark for (2928ds/2430Mi) % 90.48/13.51 % Exception at run slice level % 90.48/13.51 User error: GNN currently only supports monomorphic FOL. % 90.48/13.51 % Exception at run slice level % 90.48/13.51 User error: GNN currently only supports monomorphic FOL. % 90.48/13.51 % (2067259)Instruction limit reached! % 90.48/13.51 % (2067259)------------------------------ % 90.48/13.51 % (2067259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.48/13.51 % (2067259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.48/13.51 % (2067259)CaDiCaL version: 2.1.3 % 90.48/13.51 % (2067259)Termination reason: Instruction limit % 90.48/13.51 % (2067259)Termination phase: Saturation % 90.48/13.51 % (2067259)Time elapsed: 2.891 s % 90.48/13.51 % (2067259)Peak memory usage: 135 MB % 90.48/13.51 % (2067259)Instructions burned: 6227 (million) % 90.48/13.51 % Exception at run slice level % 90.48/13.51 User error: GNN currently only supports monomorphic FOL. % 90.48/13.51 % (2067304)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=2454897826:cond=fast:i=4891_2923 on theBenchmark for (2923ds/4891Mi) % 90.48/13.51 % (2067305)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=3975386637:st=2:i=14845:sd=2:ss=included:fsd=on_2923 on theBenchmark for (2923ds/14845Mi) % 90.48/13.51 % (2067306)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=2137705679:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2923 on theBenchmark for (2923ds/7534Mi) % 90.48/13.51 % (2067307)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=3482685957:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2923 on theBenchmark for (2923ds/10353Mi) % 90.48/13.51 % Exception at run slice level % 90.48/13.51 User error: GNN currently only supports monomorphic FOL. % 90.48/13.51 % Exception at run slice level % 90.48/13.51 User error: GNN currently only supports monomorphic FOL. % 90.48/13.51 % Exception at run slice level% Exception at run slice level % 90.48/13.51 % 90.48/13.51 User error: User error: GNN currently only supports monomorphic FOL.GNN currently only supports monomorphic FOL. % 90.48/13.51 % 90.48/13.51 % (2067312)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=820454446:i=7860_2918 on theBenchmark for (2918ds/7860Mi) % 90.48/13.51 % (2067313)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=2736774268:i=7896:sd=2:bs=on:ss=included:sgt=20_2918 on theBenchmark for (2918ds/7896Mi) % 90.48/13.51 % (2067315)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=425121749:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2918 on theBenchmark for (2918ds/2965Mi) % 90.48/13.51 % (2067314)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=3492936443:i=5812:gtgl=2:gtg=all_2918 on theBenchmark for (2918ds/5812Mi) % 90.48/13.51 % Exception at run slice level % 90.48/13.51 User error: GNN currently only supports monomorphic FOL. % 90.48/13.51 % Exception at run slice level % 90.48/13.51 User error: GNN currently only supports monomorphic FOL. % 90.48/13.51 % Exception at run slice level % 90.48/13.51 User error: GNN currently only supports monomorphic FOL. % 90.48/13.51 % (2067320)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=1645832199:i=2967:kws=precedence:bd=preordered:av=off_2913 on theBenchmark for (2913ds/2967Mi) % 90.48/13.51 % (2067322)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=3598429022:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2912 on theBenchmark for (2912ds/3207Mi) % 117.00/17.19 % (2067321)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=1278732809:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2912 on theBenchmark for (2912ds/3022Mi) % 117.00/17.19 % Exception at run slice level % 117.00/17.19 User error: GNN currently only supports monomorphic FOL. % 117.00/17.19 % Exception at run slice level % 117.00/17.19 User error: GNN currently only supports monomorphic FOL. % 117.00/17.19 % Exception at run slice level % 117.00/17.19 User error: GNN currently only supports monomorphic FOL. % 117.00/17.19 % (2067326)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=4271420646:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2908 on theBenchmark for (2908ds/3289Mi) % 117.00/17.19 % (2067328)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=2452339599:cts=off:i=3394_2907 on theBenchmark for (2907ds/3394Mi) % 117.00/17.19 % (2067327)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=3951711832:i=38569:sd=3:ss=axioms:sgt=32_2907 on theBenchmark for (2907ds/38569Mi) % 117.00/17.19 % Exception at run slice level % 117.00/17.19 User error: GNN currently only supports monomorphic FOL. % 117.00/17.19 % Exception at run slice level % 117.00/17.19 User error: GNN currently only supports monomorphic FOL. % 117.00/17.19 % Exception at run slice level % 117.00/17.19 User error: GNN currently only supports monomorphic FOL. % 117.00/17.19 % (2067332)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=2327942700:i=33824:bd=preordered_2902 on theBenchmark for (2902ds/33824Mi) % 117.00/17.19 % (2067333)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=1133071139:i=20684:bd=all:gtg=exists_sym_2902 on theBenchmark for (2902ds/20684Mi) % 117.00/17.19 % (2067334)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=1250319655: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_2902 on theBenchmark for (2902ds/7222Mi) % 117.00/17.19 % (2067334)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 117.00/17.19 % Exception at run slice level % 117.00/17.19 User error: GNN currently only supports monomorphic FOL. % 117.00/17.19 % Exception at run slice level % 117.00/17.19 User error: GNN currently only supports monomorphic FOL. % 117.00/17.19 % Exception at run slice level % 117.00/17.19 User error: GNN currently only supports monomorphic FOL. % 117.00/17.19 % (2067340)lrs+10_1_sil=128000:lcm=predicate:random_seed=4127890521:st=3:i=43697:sd=5:ss=axioms_2897 on theBenchmark for (2897ds/43697Mi) % 117.00/17.19 % (2067339)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=1567688759:i=4036:ins=10_2897 on theBenchmark for (2897ds/4036Mi) % 117.00/17.19 % (2067338)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=1052562293:st=4:i=7295:sd=4:ep=R:ss=axioms_2897 on theBenchmark for (2897ds/7295Mi) % 117.00/17.19 % (2067296)Instruction limit reached! % 117.00/17.19 % (2067296)------------------------------ % 117.00/17.19 % (2067296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.00/17.19 % (2067296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.00/17.19 % (2067296)CaDiCaL version: 2.1.3 % 117.00/17.19 % (2067296)Termination reason: Instruction limit % 117.00/17.19 % (2067296)Termination phase: Saturation % 117.00/17.19 % (2067296)Time elapsed: 3.472 s % 117.00/17.19 % (2067296)Peak memory usage: 124 MB % 117.00/17.19 % (2067296)Instructions burned: 5470 (million) % 117.00/17.19 % Exception at run slice level% Exception at run slice level % 117.00/17.19 User error: % 117.00/17.19 GNN currently only supports monomorphic FOL. % 117.00/17.19 User error: GNN currently only supports monomorphic FOL. % 117.00/17.19 % (2067344)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=265900620:i=17599:gtg=all:ss=axioms:fsd=on_2893 on theBenchmark for (2893ds/17599Mi) % 131.15/19.14 % (2067346)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=4103178815:i=9294:av=off_2892 on theBenchmark for (2892ds/9294Mi) % 131.15/19.14 % (2067345)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=112204834:i=4547:bd=preordered_2892 on theBenchmark for (2892ds/4547Mi) % 131.15/19.14 % Exception at run slice level % 131.15/19.14 User error: GNN currently only supports monomorphic FOL. % 131.15/19.14 % Exception at run slice level % 131.15/19.14 User error: GNN currently only supports monomorphic FOL. % 131.15/19.14 % Exception at run slice level % 131.15/19.14 User error: GNN currently only supports monomorphic FOL. % 131.15/19.14 % (2067350)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1212905843:i=32849:add=on_2888 on theBenchmark for (2888ds/32849Mi) % 131.15/19.14 % (2067352)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=1278716440:i=4840:nm=4:av=off_2887 on theBenchmark for (2887ds/4840Mi) % 131.15/19.14 % (2067351)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1619206793:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2887 on theBenchmark for (2887ds/4793Mi) % 131.15/19.14 % Exception at run slice level % 131.15/19.14 User error: GNN currently only supports monomorphic FOL. % 131.15/19.14 % Exception at run slice level % 131.15/19.14 User error: GNN currently only supports monomorphic FOL. % 131.15/19.14 % Exception at run slice level % 131.15/19.14 User error: GNN currently only supports monomorphic FOL. % 131.15/19.14 % (2067356)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=2500072418:cts=off:i=5002_2883 on theBenchmark for (2883ds/5002Mi) % 131.15/19.14 % (2067357)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=2701765900:i=30479:sd=3:ss=axioms_2882 on theBenchmark for (2882ds/30479Mi) % 131.15/19.14 % (2067358)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=3508176160:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2882 on theBenchmark for (2882ds/11035Mi) % 131.15/19.14 % (2067358)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 131.15/19.14 % Exception at run slice level % 131.15/19.14 User error: GNN currently only supports monomorphic FOL. % 131.15/19.14 % Exception at run slice level % 131.15/19.14 User error: GNN currently only supports monomorphic FOL. % 131.15/19.14 % Exception at run slice level % 131.15/19.14 User error: GNN currently only supports monomorphic FOL. % 131.15/19.14 % (2067362)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=313323710:i=5835_2878 on theBenchmark for (2878ds/5835Mi) % 131.15/19.14 % (2067363)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=2616152304:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2877 on theBenchmark for (2877ds/5890Mi) % 131.15/19.14 % (2067364)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=750463766:cts=off:i=19910:ep=RS_2876 on theBenchmark for (2876ds/19910Mi) % 131.15/19.14 % (2067312)Instruction limit reached! % 131.15/19.14 % (2067312)------------------------------ % 131.15/19.14 % (2067312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.15/19.14 % (2067312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.15/19.14 % (2067312)CaDiCaL version: 2.1.3 % 131.15/19.14 % (2067312)Termination reason: Instruction limit % 131.15/19.14 % (2067312)Termination phase: Saturation % 131.15/19.14 % (2067312)Time elapsed: 4.345 s % 131.15/19.14 % (2067312)Peak memory usage: 140 MB % 131.15/19.14 % (2067312)Instructions burned: 7861 (million) % 131.15/19.14 % Exception at run slice level % 131.15/19.14 User error: GNN currently only supports monomorphic FOL. % 131.15/19.14 % Exception at run slice level % 131.15/19.14 User error: GNN currently only supports monomorphic FOL. % 131.15/19.14 % (2067368)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=587421611:i=20312:bd=preordered:fsr=off:er=filter_2873 on theBenchmark for (2873ds/20312Mi) % 173.08/25.06 % (2067369)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=4119206571:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2872 on theBenchmark for (2872ds/13822Mi) % 173.08/25.06 % (2067370)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=1014938180:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2871 on theBenchmark for (2871ds/7144Mi) % 173.08/25.06 % (2067274)Instruction limit reached! % 173.08/25.06 % (2067274)------------------------------ % 173.08/25.06 % (2067274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.08/25.06 % (2067274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.08/25.06 % (2067274)CaDiCaL version: 2.1.3 % 173.08/25.06 % (2067274)Termination reason: Instruction limit % 173.08/25.06 % (2067274)Termination phase: Saturation % 173.08/25.06 % (2067274)Time elapsed: 7.329 s % 173.08/25.06 % (2067274)Peak memory usage: 417 MB % 173.08/25.06 % (2067274)Instructions burned: 26473 (million) % 173.08/25.06 % (2067374)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=2731952154:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2869 on theBenchmark for (2869ds/15184Mi) % 173.08/25.06 % Exception at run slice level % 173.08/25.06 User error: GNN currently only supports monomorphic FOL. % 173.08/25.06 % Exception at run slice level % 173.08/25.06 User error: GNN currently only supports monomorphic FOL. % 173.08/25.06 % (2067376)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=1277523864:i=107375_2868 on theBenchmark for (2868ds/107375Mi) % 173.08/25.06 % Exception at run slice level % 173.08/25.06 User error: GNN currently only supports monomorphic FOL. % 173.08/25.06 % (2067377)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=1502618074:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2867 on theBenchmark for (2867ds/7958Mi) % 173.08/25.06 % (2067379)dis+10_128_sil=16000:nwc=0.7:random_seed=3860021056:i=15999:nm=2:gsp=on_2866 on theBenchmark for (2866ds/15999Mi) % 173.08/25.06 % (2067379)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 173.08/25.06 % Exception at run slice level % 173.08/25.06 User error: GNN currently only supports monomorphic FOL. % 173.08/25.06 % Exception at run slice level % 173.08/25.06 User error: GNN currently only supports monomorphic FOL. % 173.08/25.06 % (2067382)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=1215455129:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2862 on theBenchmark for (2862ds/8139Mi) % 173.08/25.06 % (2067383)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=4046236829:st=4:i=8950:sd=5:ss=axioms_2862 on theBenchmark for (2862ds/8950Mi) % 173.08/25.06 % Exception at run slice level % 173.08/25.06 User error: GNN currently only supports monomorphic FOL. % 173.08/25.06 % (2067386)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=253076908:i=9809:ins=10:av=off_2857 on theBenchmark for (2857ds/9809Mi) % 173.08/25.06 % Exception at run slice level % 173.08/25.06 User error: GNN currently only supports monomorphic FOL. % 173.08/25.06 % (2067388)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=2285624874:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2852 on theBenchmark for (2852ds/9885Mi) % 173.08/25.06 % Exception at run slice level % 173.08/25.06 User error: GNN currently only supports monomorphic FOL. % 173.08/25.06 % (2067390)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=4150392105:cond=fast:i=32078:fgj=on:av=off_2847 on theBenchmark for (2847ds/32078Mi) % 173.08/25.06 % Exception at run slice level % 173.08/25.06 User error: GNN currently only supports monomorphic FOL. % 173.08/25.06 % (2067392)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=3144769933:i=11101:bd=all:ss=axioms:sgt=8_2841 on theBenchmark for (2841ds/11101Mi) % 173.08/25.06 % (2067370)Instruction limit reached! % 191.07/27.67 % (2067370)------------------------------ % 191.07/27.67 % (2067370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.07/27.67 % (2067370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.07/27.67 % (2067370)CaDiCaL version: 2.1.3 % 191.07/27.67 % (2067370)Termination reason: Instruction limit % 191.07/27.67 % (2067370)Termination phase: Saturation % 191.07/27.67 % (2067370)Time elapsed: 3.536 s % 191.07/27.67 % (2067370)Peak memory usage: 176 MB % 191.07/27.67 % (2067370)Instructions burned: 7145 (million) % 191.07/27.67 % (2067394)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=1847329011:cond=on:i=13220:s2at=3:aac=none:fsd=on_2834 on theBenchmark for (2834ds/13220Mi) % 191.07/27.67 % Exception at run slice level % 191.07/27.67 User error: GNN currently only supports monomorphic FOL. % 191.07/27.67 % (2067396)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=2403138478:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2829 on theBenchmark for (2829ds/13528Mi) % 191.07/27.67 % Exception at run slice level % 191.07/27.67 User error: GNN currently only supports monomorphic FOL. % 191.07/27.67 % (2067379)Instruction limit reached! % 191.07/27.67 % (2067379)------------------------------ % 191.07/27.67 % (2067379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.07/27.67 % (2067379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.07/27.67 % (2067379)CaDiCaL version: 2.1.3 % 191.07/27.67 % (2067379)Termination reason: Instruction limit % 191.07/27.67 % (2067379)Termination phase: Saturation % 191.07/27.67 % (2067379)Time elapsed: 4.137 s % 191.07/27.67 % (2067379)Peak memory usage: 158 MB % 191.07/27.67 % (2067379)Instructions burned: 16002 (million) % 191.07/27.67 % (2067398)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=3132261422:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2824 on theBenchmark for (2824ds/14854Mi) % 191.07/27.67 % (2067399)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=1538466710:i=14974:ss=axioms:sgt=16_2823 on theBenchmark for (2823ds/14974Mi) % 191.07/27.67 % (2067382)Instruction limit reached! % 191.07/27.67 % (2067382)------------------------------ % 191.07/27.67 % (2067382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.07/27.67 % (2067382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.07/27.67 % (2067382)CaDiCaL version: 2.1.3 % 191.07/27.67 % (2067382)Termination reason: Instruction limit % 191.07/27.67 % (2067382)Termination phase: Saturation % 191.07/27.67 % (2067382)Time elapsed: 3.902 s % 191.07/27.67 % (2067382)Peak memory usage: 129 MB % 191.07/27.67 % (2067382)Instructions burned: 8140 (million) % 191.07/27.67 % (2067402)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=3109796644:i=33081:aac=none:fgj=on:bd=all:fsr=off_2822 on theBenchmark for (2822ds/33081Mi) % 191.07/27.67 % Exception at run slice level % 191.07/27.67 User error: GNN currently only supports monomorphic FOL. % 191.07/27.67 % (2067404)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=1165025737:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2820 on theBenchmark for (2820ds/50856Mi) % 191.07/27.67 % Exception at run slice level % 191.07/27.67 User error: GNN currently only supports monomorphic FOL. % 191.07/27.67 % Exception at run slice level % 191.07/27.67 User error: GNN currently only supports monomorphic FOL. % 191.07/27.67 % (2067406)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=2682015358:i=69865_2818 on theBenchmark for (2818ds/69865Mi) % 191.07/27.67 % Exception at run slice level % 191.07/27.67 User error: GNN currently only supports monomorphic FOL. % 191.07/27.67 % (2067407)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=184902670:cond=fast:i=17802:gtgl=3:gtg=all_2817 on theBenchmark for (2817ds/17802Mi) % 191.07/27.67 % Exception at run slice level % 191.07/27.67 User error: Immediate (shared) subterms of term/literal aa(X1,fun(list(X1),X0),X4,X3) = sF27(X1,X0,X4,X3) have different types/not well-typed! % 191.07/27.67 % (2067409)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=3431974950:i=96644_2816 on theBenchmark for (2816ds/96644Mi) % 203.23/29.35 % (2067411)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 203.23/29.35 % (2067411)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=2251486849:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2816 on theBenchmark for (2816ds/21161Mi) % 203.23/29.35 % Exception at run slice level % 203.23/29.35 User error: GNN currently only supports monomorphic FOL. % 203.23/29.35 % (2067414)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=2442597018:i=22761:gtg=all:ss=axioms:fsd=on_2813 on theBenchmark for (2813ds/22761Mi) % 203.23/29.35 % Exception at run slice level % 203.23/29.35 User error: GNN currently only supports monomorphic FOL. % 203.23/29.35 % (2067416)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=4167963686:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2808 on theBenchmark for (2808ds/23713Mi) % 203.23/29.35 % (2067392)Instruction limit reached! % 203.23/29.35 % (2067392)------------------------------ % 203.23/29.35 % (2067392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.23/29.35 % (2067392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.23/29.35 % (2067392)CaDiCaL version: 2.1.3 % 203.23/29.35 % (2067392)Termination reason: Instruction limit % 203.23/29.35 % (2067392)Termination phase: Saturation % 203.23/29.35 % (2067392)Time elapsed: 5.920 s % 203.23/29.35 % (2067392)Peak memory usage: 139 MB % 203.23/29.35 % (2067392)Instructions burned: 11102 (million) % 203.23/29.35 % (2067418)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=3568286054:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2780 on theBenchmark for (2780ds/26509Mi) % 203.23/29.35 % Exception at run slice level % 203.23/29.35 User error: GNN currently only supports monomorphic FOL. % 203.23/29.35 % (2067420)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=1516623630:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2775 on theBenchmark for (2775ds/28957Mi) % 203.23/29.35 % (2067364)Instruction limit reached! % 203.23/29.35 % (2067364)------------------------------ % 203.23/29.35 % (2067364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.23/29.35 % (2067364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.23/29.35 % (2067364)CaDiCaL version: 2.1.3 % 203.23/29.35 % (2067364)Termination reason: Instruction limit % 203.23/29.35 % (2067364)Termination phase: Saturation % 203.23/29.35 % (2067364)Time elapsed: 11.154 s % 203.23/29.35 % (2067364)Peak memory usage: 140 MB % 203.23/29.35 % (2067364)Instructions burned: 19912 (million) % 203.23/29.35 % (2067422)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=2762678788:i=29246:s2at=-1:kws=inv_arity:ins=10_2763 on theBenchmark for (2763ds/29246Mi) % 203.23/29.35 % Exception at run slice level % 203.23/29.35 User error: GNN currently only supports monomorphic FOL. % 203.23/29.35 % (2067247)Instruction limit reached! % 203.23/29.35 % (2067247)------------------------------ % 203.23/29.35 % (2067247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.23/29.35 % (2067247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.23/29.35 % (2067247)CaDiCaL version: 2.1.3 % 203.23/29.35 % (2067247)Termination reason: Instruction limit % 203.23/29.35 % (2067247)Termination phase: Saturation % 203.23/29.35 % (2067247)Time elapsed: 20.273 s % 203.23/29.35 % (2067247)Peak memory usage: 262 MB % 203.23/29.35 % (2067247)Instructions burned: 33335 (million) % 203.23/29.35 % (2067424)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=430886670:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2758 on theBenchmark for (2758ds/30082Mi) % 203.23/29.35 % (2067424)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 203.23/29.35 % (2067425)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=2514213963:i=32262:bd=preordered_2757 on theBenchmark for (2757ds/32262Mi) % 214.21/30.91 % Exception at run slice level % 214.21/30.91 User error: GNN currently only supports monomorphic FOL. % 214.21/30.91 % Exception at run slice level % 214.21/30.91 User error: GNN currently only supports monomorphic FOL. % 214.21/30.91 % (2067428)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=3985867702:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2753 on theBenchmark for (2753ds/32870Mi) % 214.21/30.91 % (2067429)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=1525421293:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2752 on theBenchmark for (2752ds/33295Mi) % 214.21/30.91 % (2067411)Instruction limit reached! % 214.21/30.91 % (2067411)------------------------------ % 214.21/30.91 % (2067411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.21/30.91 % (2067411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.21/30.91 % (2067411)CaDiCaL version: 2.1.3 % 214.21/30.91 % (2067411)Termination reason: Instruction limit % 214.21/30.91 % (2067411)Termination phase: Saturation % 214.21/30.91 % (2067411)Time elapsed: 6.495 s % 214.21/30.91 % (2067411)Peak memory usage: 219 MB % 214.21/30.91 % (2067411)Instructions burned: 21162 (million) % 214.21/30.91 % (2067432)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=1086585234:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2749 on theBenchmark for (2749ds/36826Mi) % 214.21/30.91 % Exception at run slice level % 214.21/30.91 User error: GNN currently only supports monomorphic FOL. % 214.21/30.91 % Exception at run slice level % 214.21/30.91 User error: GNN currently only supports monomorphic FOL. % 214.21/30.91 % (2067434)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=2863345861:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2748 on theBenchmark for (2748ds/92981Mi) % 214.21/30.91 % (2067435)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=2864650959:s2pl=on:i=49423_2747 on theBenchmark for (2747ds/49423Mi) % 214.21/30.91 % Exception at run slice level % 214.21/30.91 User error: GNN currently only supports monomorphic FOL. % 214.21/30.91 % Exception at run slice level % 214.21/30.91 User error: GNN currently only supports monomorphic FOL. % 214.21/30.91 % (2067438)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=772194204:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2742 on theBenchmark for (2742ds/57299Mi) % 214.21/30.91 % (2067439)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=1226051231:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2742 on theBenchmark for (2742ds/127679Mi) % 214.21/30.91 % Exception at run slice level % 214.21/30.91 User error: GNN currently only supports monomorphic FOL. % 214.21/30.91 % Exception at run slice level % 214.21/30.91 User error: GNN currently only supports monomorphic FOL. % 214.21/30.91 % (2067442)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=41227861:i=69402:add=on:aac=none:fsr=off_2737 on theBenchmark for (2737ds/69402Mi) % 214.21/30.91 % (2067443)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=2344167399:i=100512:doe=on:fgj=on:bd=all:fsd=on_2736 on theBenchmark for (2736ds/100512Mi) % 214.21/30.91 % Exception at run slice level % 214.21/30.91 User error: GNN currently only supports monomorphic FOL. % 214.21/30.91 % Exception at run slice level % 214.21/30.91 User error: GNN currently only supports monomorphic FOL. % 214.21/30.91 % (2067446)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=3049585586:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2732 on theBenchmark for (2732ds/138761Mi) % 214.21/30.91 % (2067447)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=2669393612:i=282386:rtra=on_2731 on theBenchmark for (2731ds/282386Mi) % 225.74/32.58 % Exception at run slice level % 225.74/32.58 User error: GNN currently only supports monomorphic FOL. % 225.74/32.58 % Exception at run slice level % 225.74/32.58 User error: GNN currently only supports monomorphic FOL. % 225.74/32.58 % (2067450)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=2862960189:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2727 on theBenchmark for (2727ds/269354Mi) % 225.74/32.58 % (2067451)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=3305834782:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2726 on theBenchmark for (2726ds/283390Mi) % 225.74/32.58 % (2067451)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 225.74/32.58 % Exception at run slice level % 225.74/32.58 User error: GNN currently only supports monomorphic FOL. % 225.74/32.58 % Exception at run slice level % 225.74/32.58 User error: GNN currently only supports monomorphic FOL. % 225.74/32.58 % (2067454)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=610343667:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2721 on theBenchmark for (2721ds/218Mi) % 225.74/32.58 % (2067454)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 225.74/32.58 % (2067454)Refutation not found, incomplete strategy % 225.74/32.58 % (2067454)------------------------------ % 225.74/32.58 % (2067454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.74/32.58 % (2067454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.74/32.58 % (2067454)CaDiCaL version: 2.1.3 % 225.74/32.58 % (2067454)Termination reason: Refutation not found, incomplete strategy % 225.74/32.58 % (2067454)Time elapsed: 0.004 s % 225.74/32.58 % (2067454)Peak memory usage: 88 MB % 225.74/32.58 % (2067454)Instructions burned: 3 (million) % 225.74/32.58 % (2067455)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=3690627997:i=238:av=off:rtra=on:ss=axioms_2721 on theBenchmark for (2721ds/238Mi) % 225.74/32.58 % (2067455)Instruction limit reached! % 225.74/32.58 % (2067455)------------------------------ % 225.74/32.58 % (2067455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.74/32.58 % (2067455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.74/32.58 % (2067455)CaDiCaL version: 2.1.3 % 225.74/32.58 % (2067455)Termination reason: Instruction limit % 225.74/32.58 % (2067455)Termination phase: Saturation % 225.74/32.58 % (2067455)Time elapsed: 0.124 s % 225.74/32.58 % (2067455)Peak memory usage: 89 MB % 225.74/32.58 % (2067455)Instructions burned: 239 (million) % 225.74/32.58 % (2067454)------------------------------ % 225.74/32.58 % (2067454)------------------------------ % 225.74/32.58 % (2067458)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=3454235346:s2a=on:i=278:rtra=on:gtg=position_2718 on theBenchmark for (2718ds/278Mi) % 225.74/32.58 % (2067459)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=4137432482:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2717 on theBenchmark for (2717ds/258Mi) % 225.74/32.58 % (2067458)Instruction limit reached! % 225.74/32.58 % (2067458)------------------------------ % 225.74/32.58 % (2067458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.74/32.58 % (2067458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.74/32.58 % (2067458)CaDiCaL version: 2.1.3 % 225.74/32.58 % (2067458)Termination reason: Instruction limit % 225.74/32.58 % (2067458)Termination phase: Saturation % 225.74/32.58 % (2067458)Time elapsed: 0.186 s % 225.74/32.58 % (2067458)Peak memory usage: 91 MB % 225.74/32.58 % (2067458)Instructions burned: 279 (million) % 225.74/32.58 % (2067459)Instruction limit reached! % 225.74/32.58 % (2067459)------------------------------ % 225.74/32.58 % (2067459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.74/32.58 % (2067459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.74/32.58 % (2067459)CaDiCaL version: 2.1.3 % 225.74/32.58 % (2067459)Termination reason: Instruction limit % 225.74/32.58 % (2067459)Termination phase: Saturation % 225.74/32.58 % (2067459)Time elapsed: 0.143 s % 225.74/32.58 % (2067459)Peak memory usage: 90 MB % 225.74/32.58 % (2067459)Instructions burned: 260 (million) % 225.74/32.58 % (2067462)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=1841991492:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2714 on theBenchmark for (2714ds/570Mi) % 237.57/34.20 % (2067463)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=3398921084:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2714 on theBenchmark for (2714ds/314Mi) % 237.57/34.20 % (2067463)Instruction limit reached! % 237.57/34.20 % (2067463)------------------------------ % 237.57/34.20 % (2067463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.57/34.20 % (2067463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.57/34.20 % (2067463)CaDiCaL version: 2.1.3 % 237.57/34.20 % (2067463)Termination reason: Instruction limit % 237.57/34.20 % (2067463)Termination phase: Saturation % 237.57/34.20 % (2067463)Time elapsed: 0.185 s % 237.57/34.20 % (2067463)Peak memory usage: 90 MB % 237.57/34.20 % (2067463)Instructions burned: 315 (million) % 237.57/34.20 % (2067462)Instruction limit reached! % 237.57/34.20 % (2067462)------------------------------ % 237.57/34.20 % (2067462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.57/34.20 % (2067462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.57/34.20 % (2067462)CaDiCaL version: 2.1.3 % 237.57/34.20 % (2067462)Termination reason: Instruction limit % 237.57/34.20 % (2067462)Termination phase: Saturation % 237.57/34.20 % (2067462)Time elapsed: 0.322 s % 237.57/34.20 % (2067462)Peak memory usage: 92 MB % 237.57/34.20 % (2067462)Instructions burned: 571 (million) % 237.57/34.20 % (2067466)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=4019856828:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2711 on theBenchmark for (2711ds/650Mi) % 237.57/34.20 % (2067467)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=88589748:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2710 on theBenchmark for (2710ds/496Mi) % 237.57/34.20 % (2067467)Instruction limit reached! % 237.57/34.20 % (2067467)------------------------------ % 237.57/34.20 % (2067467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.57/34.20 % (2067467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.57/34.20 % (2067467)CaDiCaL version: 2.1.3 % 237.57/34.20 % (2067467)Termination reason: Instruction limit % 237.57/34.20 % (2067467)Termination phase: Saturation % 237.57/34.20 % (2067467)Time elapsed: 0.275 s % 237.57/34.20 % (2067467)Peak memory usage: 91 MB % 237.57/34.20 % (2067467)Instructions burned: 497 (million) % 237.57/34.20 % (2067466)Instruction limit reached! % 237.57/34.20 % (2067466)------------------------------ % 237.57/34.20 % (2067466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.57/34.20 % (2067466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.57/34.20 % (2067466)CaDiCaL version: 2.1.3 % 237.57/34.20 % (2067466)Termination reason: Instruction limit % 237.57/34.20 % (2067466)Termination phase: Saturation % 237.57/34.20 % (2067466)Time elapsed: 0.411 s % 237.57/34.20 % (2067466)Peak memory usage: 94 MB % 237.57/34.20 % (2067466)Instructions burned: 651 (million) % 237.57/34.20 % (2067470)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=105865238:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2705 on theBenchmark for (2705ds/588Mi) % 237.57/34.20 % (2067471)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=2233872911:i=4700:rtra=on_2705 on theBenchmark for (2705ds/4700Mi) % 237.57/34.20 % (2067470)Instruction limit reached! % 237.57/34.20 % (2067470)------------------------------ % 237.57/34.20 % (2067470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.57/34.20 % (2067470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.57/34.20 % (2067470)CaDiCaL version: 2.1.3 % 237.57/34.20 % (2067470)Termination reason: Instruction limit % 237.57/34.20 % (2067470)Termination phase: Saturation % 237.57/34.20 % (2067470)Time elapsed: 0.353 s % 237.57/34.20 % (2067470)Peak memory usage: 91 MB % 237.57/34.20 % (2067470)Instructions burned: 588 (million) % 237.57/34.20 % Exception at run slice level % 237.57/34.20 User error: GNN currently only supports monomorphic FOL. % 237.57/34.20 % (2067474)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=161335637:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2700 on theBenchmark for (2700ds/226Mi) % 237.57/34.20 % (2067475)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=330269024:i=254:av=off:fsr=off:rtra=on:sup=off_2700 on theBenchmark for (2700ds/254Mi) % 237.57/34.20 % (2067474)Instruction limit reached! % 237.57/34.20 % (2067474)------------------------------ % 237.57/34.20 % (2067474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.68/35.19 % (2067474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.68/35.19 % (2067474)CaDiCaL version: 2.1.3 % 244.68/35.19 % (2067474)Termination reason: Instruction limit % 244.68/35.19 % (2067474)Termination phase: Saturation % 244.68/35.19 % (2067474)Time elapsed: 0.146 s % 244.68/35.19 % (2067474)Peak memory usage: 90 MB % 244.68/35.19 % (2067474)Instructions burned: 227 (million) % 244.68/35.19 % (2067475)Instruction limit reached! % 244.68/35.19 % (2067475)------------------------------ % 244.68/35.19 % (2067475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.68/35.19 % (2067475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.68/35.19 % (2067475)CaDiCaL version: 2.1.3 % 244.68/35.19 % (2067475)Termination reason: Instruction limit % 244.68/35.19 % (2067475)Termination phase: Saturation % 244.68/35.19 % (2067475)Time elapsed: 0.120 s % 244.68/35.19 % (2067475)Peak memory usage: 89 MB % 244.68/35.19 % (2067475)Instructions burned: 256 (million) % 244.68/35.19 % (2067478)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=3731373057:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2697 on theBenchmark for (2697ds/228Mi) % 244.68/35.19 % (2067479)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=1893766223:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2697 on theBenchmark for (2697ds/1814Mi) % 244.68/35.19 % (2067478)Instruction limit reached! % 244.68/35.19 % (2067478)------------------------------ % 244.68/35.19 % (2067478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.68/35.19 % (2067478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.68/35.19 % (2067478)CaDiCaL version: 2.1.3 % 244.68/35.19 % (2067478)Termination reason: Instruction limit % 244.68/35.19 % (2067478)Termination phase: Saturation % 244.68/35.19 % (2067478)Time elapsed: 0.115 s % 244.68/35.19 % (2067478)Peak memory usage: 89 MB % 244.68/35.19 % (2067478)Instructions burned: 228 (million) % 244.68/35.19 % (2067482)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=2655686802:i=874:sd=1:aac=none:rtra=on:ss=included_2694 on theBenchmark for (2694ds/874Mi) % 244.68/35.19 % (2067482)Instruction limit reached! % 244.68/35.19 % (2067482)------------------------------ % 244.68/35.19 % (2067482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.68/35.19 % (2067482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.68/35.19 % (2067482)CaDiCaL version: 2.1.3 % 244.68/35.19 % (2067482)Termination reason: Instruction limit % 244.68/35.19 % (2067482)Termination phase: Saturation % 244.68/35.19 % (2067482)Time elapsed: 0.497 s % 244.68/35.19 % (2067482)Peak memory usage: 94 MB % 244.68/35.19 % (2067482)Instructions burned: 874 (million) % 244.68/35.19 % (2067484)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=657027589:i=10404:rtra=on:ss=axioms:sgt=16_2688 on theBenchmark for (2688ds/10404Mi) % 244.68/35.19 % (2067479)Instruction limit reached! % 244.68/35.19 % (2067479)------------------------------ % 244.68/35.19 % (2067479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.68/35.19 % (2067479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.68/35.19 % (2067479)CaDiCaL version: 2.1.3 % 244.68/35.19 % (2067479)Termination reason: Instruction limit % 244.68/35.19 % (2067479)Termination phase: Saturation % 244.68/35.19 % (2067479)Time elapsed: 1.151 s % 244.68/35.19 % (2067479)Peak memory usage: 105 MB % 244.68/35.19 % (2067479)Instructions burned: 1814 (million) % 244.68/35.19 % Exception at run slice level % 244.68/35.19 User error: GNN currently only supports monomorphic FOL. % 244.68/35.19 % (2067486)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1966023890:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2684 on theBenchmark for (2684ds/268Mi) % 244.68/35.19 % (2067487)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=1672021571:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2682 on theBenchmark for (2682ds/1184Mi) % 244.68/35.19 % (2067486)Instruction limit reached! % 244.68/35.19 % (2067486)------------------------------ % 244.68/35.19 % (2067486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.68/35.19 % (2067486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.68/35.19 % (2067486)CaDiCaL version: 2.1.3 % 244.68/35.19 % (2067486)Termination reason: Instruction limit % 244.68/35.19 % (2067486)Termination phase: Saturation % 244.68/35.19 % (2067486)Time elapsed: 0.156 s % 244.68/35.19 % (2067486)Peak memory usage: 91 MB % 244.68/35.19 % (2067486)Instructions burned: 269 (million) % 260.51/37.49 % (2067490)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=2285852412:st=3:i=26386:sd=3:rtra=on:ss=axioms_2680 on theBenchmark for (2680ds/26386Mi) % 260.51/37.49 % Exception at run slice level % 260.51/37.49 User error: GNN currently only supports monomorphic FOL. % 260.51/37.49 % (2067492)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=1861332493:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2675 on theBenchmark for (2675ds/250Mi) % 260.51/37.49 % (2067487)Instruction limit reached! % 260.51/37.49 % (2067487)------------------------------ % 260.51/37.49 % (2067487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.51/37.49 % (2067487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.51/37.49 % (2067487)CaDiCaL version: 2.1.3 % 260.51/37.49 % (2067487)Termination reason: Instruction limit % 260.51/37.49 % (2067487)Termination phase: Saturation % 260.51/37.49 % (2067487)Time elapsed: 0.682 s % 260.51/37.49 % (2067487)Peak memory usage: 99 MB % 260.51/37.49 % (2067487)Instructions burned: 1184 (million) % 260.51/37.49 % (2067492)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 260.51/37.49 % (2067494)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=3784374688:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2674 on theBenchmark for (2674ds/268Mi) % 260.51/37.49 % Exception at run slice level % 260.51/37.49 User error: Immediate (shared) subterms of term/literal aa(X1,fun(list(X1),X0),X3,X4) = sF22(X1,X0,X3,X4) have different types/not well-typed! % 260.51/37.49 % (2067492)Instruction limit reached! % 260.51/37.49 % (2067492)------------------------------ % 260.51/37.49 % (2067492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.51/37.49 % (2067492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.51/37.49 % (2067492)CaDiCaL version: 2.1.3 % 260.51/37.49 % (2067492)Termination reason: Instruction limit % 260.51/37.49 % (2067492)Termination phase: Saturation % 260.51/37.49 % (2067492)Time elapsed: 0.172 s % 260.51/37.49 % (2067492)Peak memory usage: 92 MB % 260.51/37.49 % (2067492)Instructions burned: 251 (million) % 260.51/37.49 % (2067497)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=2414467757:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2672 on theBenchmark for (2672ds/862Mi) % 260.51/37.49 % (2067496)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4020942654:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2672 on theBenchmark for (2672ds/282Mi) % 260.51/37.49 % (2067496)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 260.51/37.49 % (2067496)Refutation not found, incomplete strategy % 260.51/37.49 % (2067496)------------------------------ % 260.51/37.49 % (2067496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.51/37.49 % (2067496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.51/37.49 % (2067496)CaDiCaL version: 2.1.3 % 260.51/37.49 % (2067496)Termination reason: Refutation not found, incomplete strategy % 260.51/37.49 % (2067496)Time elapsed: 0.003 s % 260.51/37.49 % (2067496)Peak memory usage: 88 MB % 260.51/37.49 % (2067496)Instructions burned: 3 (million) % 260.51/37.49 % (2067496)------------------------------ % 260.51/37.49 % (2067496)------------------------------ % 260.51/37.49 % (2067500)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=3919299979:i=12120:aac=none:ins=25:rtra=on_2668 on theBenchmark for (2668ds/12120Mi) % 260.51/37.49 % (2067497)Instruction limit reached! % 260.51/37.49 % (2067497)------------------------------ % 260.51/37.49 % (2067497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.51/37.49 % (2067497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.51/37.49 % (2067497)CaDiCaL version: 2.1.3 % 260.51/37.49 % (2067497)Termination reason: Instruction limit % 260.51/37.49 % (2067497)Termination phase: Saturation % 260.51/37.49 % (2067497)Time elapsed: 0.440 s % 260.51/37.49 % (2067497)Peak memory usage: 91 MB % 260.51/37.49 % (2067497)Instructions burned: 863 (million) % 260.51/37.49 % (2067502)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=2056782727:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2666 on theBenchmark for (2666ds/300Mi) % 269.97/38.99 % (2067502)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 269.97/38.99 % Exception at run slice level % 269.97/38.99 User error: GNN currently only supports monomorphic FOL. % 269.97/38.99 % (2067502)Instruction limit reached! % 269.97/38.99 % (2067502)------------------------------ % 269.97/38.99 % (2067502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.97/38.99 % (2067502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.97/38.99 % (2067502)CaDiCaL version: 2.1.3 % 269.97/38.99 % (2067502)Termination reason: Instruction limit % 269.97/38.99 % (2067502)Termination phase: Saturation % 269.97/38.99 % (2067502)Time elapsed: 0.187 s % 269.97/38.99 % (2067502)Peak memory usage: 92 MB % 269.97/38.99 % (2067502)Instructions burned: 301 (million) % 269.97/38.99 % (2067432)Instruction limit reached! % 269.97/38.99 % (2067432)------------------------------ % 269.97/38.99 % (2067432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.97/38.99 % (2067432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.97/38.99 % (2067432)CaDiCaL version: 2.1.3 % 269.97/38.99 % (2067432)Termination reason: Instruction limit % 269.97/38.99 % (2067432)Termination phase: Saturation % 269.97/38.99 % (2067432)Time elapsed: 8.637 s % 269.97/38.99 % (2067432)Peak memory usage: 183 MB % 269.97/38.99 % (2067432)Instructions burned: 36827 (million) % 269.97/38.99 % (2067504)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=2306538433:i=28310:bd=all:rtra=on_2663 on theBenchmark for (2663ds/28310Mi) % 269.97/38.99 % (2067505)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=430769191:i=1334:av=off:fsr=off:rtra=on_2662 on theBenchmark for (2662ds/1334Mi) % 269.97/38.99 % (2067506)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=2090238253:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2662 on theBenchmark for (2662ds/370Mi) % 269.97/38.99 % (2067506)Instruction limit reached! % 269.97/38.99 % (2067506)------------------------------ % 269.97/38.99 % (2067506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.97/38.99 % (2067506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.97/38.99 % (2067506)CaDiCaL version: 2.1.3 % 269.97/38.99 % (2067506)Termination reason: Instruction limit % 269.97/38.99 % (2067506)Termination phase: Saturation % 269.97/38.99 % (2067506)Time elapsed: 0.126 s % 269.97/38.99 % (2067506)Peak memory usage: 93 MB % 269.97/38.99 % (2067506)Instructions burned: 371 (million) % 269.97/38.99 % (2067510)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=1566937297:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2659 on theBenchmark for (2659ds/386Mi) % 269.97/38.99 % Exception at run slice level % 269.97/38.99 User error: GNN currently only supports monomorphic FOL. % 269.97/38.99 % (2067510)Refutation not found, incomplete strategy % 269.97/38.99 % (2067510)------------------------------ % 269.97/38.99 % (2067510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.97/38.99 % (2067510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.97/38.99 % (2067510)CaDiCaL version: 2.1.3 % 269.97/38.99 % (2067510)Termination reason: Refutation not found, incomplete strategy % 269.97/38.99 % (2067510)Time elapsed: 0.087 s % 269.97/38.99 % (2067510)Peak memory usage: 90 MB % 269.97/38.99 % (2067510)Instructions burned: 345 (million) % 269.97/38.99 % (2067512)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=2705820785:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2658 on theBenchmark for (2658ds/9700Mi) % 269.97/38.99 % (2067510)------------------------------ % 269.97/38.99 % (2067510)------------------------------ % 269.97/38.99 % (2067505)Instruction limit reached! % 269.97/38.99 % (2067505)------------------------------ % 269.97/38.99 % (2067505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.97/38.99 % (2067505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.97/38.99 % (2067505)CaDiCaL version: 2.1.3 % 269.97/38.99 % (2067505)Termination reason: Instruction limit % 269.97/38.99 % (2067505)Termination phase: Saturation % 269.97/38.99 % (2067505)Time elapsed: 0.528 s % 269.97/38.99 % (2067505)Peak memory usage: 90 MB % 269.97/38.99 % (2067505)Instructions burned: 1334 (million) % 269.97/38.99 % (2067514)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=4213475432:i=24222:sd=1:rtra=on:ss=included_2656 on theBenchmark for (2656ds/24222Mi) % 281.76/40.49 % (2067515)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=3403974804:i=638:kws=precedence:fsr=off:rtra=on_2656 on theBenchmark for (2656ds/638Mi) % 281.76/40.49 % Exception at run slice level % 281.76/40.49 User error: GNN currently only supports monomorphic FOL. % 281.76/40.49 % (2067518)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1214973401:i=4128:ep=RST:rtra=on_2652 on theBenchmark for (2652ds/4128Mi) % 281.76/40.49 % (2067515)Instruction limit reached! % 281.76/40.49 % (2067515)------------------------------ % 281.76/40.49 % (2067515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.76/40.49 % (2067515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.76/40.49 % (2067515)CaDiCaL version: 2.1.3 % 281.76/40.49 % (2067515)Termination reason: Instruction limit % 281.76/40.49 % (2067515)Termination phase: Saturation % 281.76/40.49 % (2067515)Time elapsed: 0.362 s % 281.76/40.49 % (2067515)Peak memory usage: 93 MB % 281.76/40.49 % (2067515)Instructions burned: 638 (million) % 281.76/40.49 % (2067520)dis-1011_128_sil=32000:si=on:random_seed=1802995983:i=7412:ep=RST:av=off:rtra=on_2650 on theBenchmark for (2650ds/7412Mi) % 281.76/40.49 % (2067416)Instruction limit reached! % 281.76/40.49 % (2067416)------------------------------ % 281.76/40.49 % (2067416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.76/40.49 % (2067416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.76/40.49 % (2067416)CaDiCaL version: 2.1.3 % 281.76/40.49 % (2067416)Termination reason: Instruction limit % 281.76/40.49 % (2067416)Termination phase: Saturation % 281.76/40.49 % (2067416)Time elapsed: 16.395 s % 281.76/40.49 % (2067416)Peak memory usage: 232 MB % 281.76/40.49 % (2067416)Instructions burned: 23713 (million) % 281.76/40.49 % (2067522)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3159669383:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2642 on theBenchmark for (2642ds/1514Mi) % 281.76/40.49 % (2067518)Instruction limit reached! % 281.76/40.49 % (2067518)------------------------------ % 281.76/40.49 % (2067518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.76/40.49 % (2067518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.76/40.49 % (2067518)CaDiCaL version: 2.1.3 % 281.76/40.49 % (2067518)Termination reason: Instruction limit % 281.76/40.49 % (2067518)Termination phase: Saturation % 281.76/40.49 % (2067518)Time elapsed: 1.277 s % 281.76/40.49 % (2067518)Peak memory usage: 111 MB % 281.76/40.49 % (2067518)Instructions burned: 4128 (million) % 281.76/40.49 % (2067524)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=187299314:i=27826:rtra=on:ss=axioms:sgt=8_2638 on theBenchmark for (2638ds/27826Mi) % 281.76/40.49 % Exception at run slice level % 281.76/40.49 User error: GNN currently only supports monomorphic FOL. % 281.76/40.49 % (2067526)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=1684514571:i=19850:aac=none:rtra=on_2635 on theBenchmark for (2635ds/19850Mi) % 281.76/40.49 % (2067340)Instruction limit reached! % 281.76/40.49 % (2067340)------------------------------ % 281.76/40.49 % (2067340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.76/40.49 % (2067340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.76/40.49 % (2067340)CaDiCaL version: 2.1.3 % 281.76/40.49 % (2067340)Termination reason: Instruction limit % 281.76/40.49 % (2067340)Termination phase: Saturation % 281.76/40.49 % (2067340)Time elapsed: 26.216 s % 281.76/40.49 % (2067340)Peak memory usage: 268 MB % 281.76/40.49 % (2067340)Instructions burned: 43699 (million) % 281.76/40.49 % Exception at run slice level % 281.76/40.49 User error: GNN currently only supports monomorphic FOL. % 281.76/40.49 % (2067528)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3352579625:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2633 on theBenchmark for (2633ds/4958Mi) % 281.76/40.49 % (2067528)Refutation not found, incomplete strategy % 281.76/40.49 % (2067528)------------------------------ % 281.76/40.49 % (2067528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.76/40.49 % (2067528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.76/40.49 % (2067528)CaDiCaL version: 2.1.3 % 296.65/42.58 % (2067528)Termination reason: Refutation not found, incomplete strategy % 296.65/42.58 % (2067528)Time elapsed: 0.004 s % 296.65/42.58 % (2067528)Peak memory usage: 88 MB % 296.65/42.58 % (2067528)Instructions burned: 4 (million) % 296.65/42.58 % (2067522)Instruction limit reached! % 296.65/42.58 % (2067522)------------------------------ % 296.65/42.58 % (2067522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.65/42.58 % (2067522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.65/42.58 % (2067522)CaDiCaL version: 2.1.3 % 296.65/42.58 % (2067522)Termination reason: Instruction limit % 296.65/42.58 % (2067522)Termination phase: Saturation % 296.65/42.58 % (2067522)Time elapsed: 0.897 s % 296.65/42.58 % (2067522)Peak memory usage: 94 MB % 296.65/42.58 % (2067522)Instructions burned: 1515 (million) % 296.65/42.58 % (2067529)ott+1002_64_sil=16000:si=on:sp=const_min:nwc=0.5:random_seed=2831254898:i=880:nm=2:av=off:rtra=on:gtg=exists_all:fdi=8:gsp=on_2632 on theBenchmark for (2632ds/880Mi) % 296.65/42.58 % (2067529)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 296.65/42.58 % (2067531)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:si=on:erd=off:lsd=100:bsr=unit_only:random_seed=1156602179:st=1.5:i=22290:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2631 on theBenchmark for (2631ds/22290Mi) % 296.65/42.58 % (2067528)------------------------------ % 296.65/42.58 % (2067528)------------------------------ % 296.65/42.58 % (2067529)Instruction limit reached! % 296.65/42.58 % (2067529)------------------------------ % 296.65/42.58 % (2067529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.65/42.58 % (2067529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.65/42.58 % (2067529)CaDiCaL version: 2.1.3 % 296.65/42.58 % (2067529)Termination reason: Instruction limit % 296.65/42.58 % (2067529)Termination phase: Saturation % 296.65/42.58 % (2067529)Time elapsed: 0.264 s % 296.65/42.58 % (2067529)Peak memory usage: 92 MB % 296.65/42.58 % (2067529)Instructions burned: 883 (million) % 296.65/42.58 % (2067534)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=1271712234:cts=off:i=6068:av=off:rtra=on:er=known:fsd=on_2629 on theBenchmark for (2629ds/6068Mi) % 296.65/42.58 % (2067535)lrs-1011_64:1_sil=8000:si=on:erd=off:urr=on:nwc=0.7:br=off:random_seed=3145456014:st=2:s2a=on:i=1048:s2at=2:rtra=on:ss=axioms_2628 on theBenchmark for (2628ds/1048Mi) % 296.65/42.58 % Exception at run slice level % 296.65/42.58 User error: GNN currently only supports monomorphic FOL. % 296.65/42.58 % (2067538)lrs+1011_16:1_sil=8000:si=on:acc=on:urr=on:fd=preordered:flr=on:random_seed=282775434:avsq=on:i=2032:avsqr=676809,524288:sd=1:rtra=on:ss=axioms_2626 on theBenchmark for (2626ds/2032Mi) % 296.65/42.58 % (2067535)Instruction limit reached! % 296.65/42.58 % (2067535)------------------------------ % 296.65/42.58 % (2067535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.65/42.58 % (2067535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.65/42.58 % (2067535)CaDiCaL version: 2.1.3 % 296.65/42.58 % (2067535)Termination reason: Instruction limit % 296.65/42.58 % (2067535)Termination phase: Saturation % 296.65/42.58 % (2067535)Time elapsed: 0.293 s % 296.65/42.58 % (2067535)Peak memory usage: 94 MB % 296.65/42.58 % (2067535)Instructions burned: 1051 (million) % 296.65/42.58 % Exception at run slice level % 296.65/42.58 User error: GNN currently only supports monomorphic FOL. % 296.65/42.58 % (2067540)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:si=on:s2agt=16:random_seed=3794818552:i=28246:bd=preordered:ins=4:rtra=on_2624 on theBenchmark for (2624ds/28246Mi) % 296.65/42.58 % (2067541)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:si=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=4195085639:i=11562:kws=precedence:bd=all:rtra=on:rawr=on_2624 on theBenchmark for (2624ds/11562Mi) % 296.65/42.58 % Exception at run slice level % 296.65/42.58 User error: GNN currently only supports monomorphic FOL. % 296.65/42.58 % (2067544)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:si=on:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=433933251:i=4896:gtgl=5:bd=preordered:rtra=on:gtg=all_2621 on theBenchmark for (2621ds/4896Mi) % 296.65/42.58 % Exception at run slice level % 296.65/42.58 User error: GNN currently only supports monomorphic FOL. % 296.65/42.58 % (2067546)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:si=on:lcm=reverse:random_seed=3774Terminated %------------------------------------------------------------------------------