%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV613_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 : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:19:06 PM UTC 2026 % Result : Timeout 300.68s 43.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV613_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.20 % Computer : n006.cluster.edu % 0.08/0.20 % Model : x86_64 x86_64 % 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.20 % Memory : 8046.5625MB % 0.08/0.20 % OS : Linux 6.8.0-71-generic % 0.08/0.20 % CPULimit : 300 % 0.08/0.20 % WCLimit : 300 % 0.08/0.20 % DateTime : Mon Sep 28 12:02:22 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.23 Running first-order theorem proving % 0.08/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.73/1.76 % (3917204)Detected formulas, will run a generic FOF schedule. % 6.73/1.76 % (3917210)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=3373565491:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 6.73/1.76 % (3917209)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=2254477088:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 6.73/1.76 % (3917214)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2412210832:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 6.73/1.76 % (3917213)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1267425100:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 6.73/1.76 % (3917215)dis-21_1_sil=8000:lcm=predicate:random_seed=371988349: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.73/1.76 % (3917211)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=2317542590:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 6.73/1.76 % (3917212)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2036410129:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 6.73/1.76 % (3917212)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 6.73/1.76 % (3917212)Refutation not found, incomplete strategy % 6.73/1.76 % (3917212)------------------------------ % 6.73/1.76 % (3917212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.73/1.76 % (3917212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.76 % (3917212)CaDiCaL version: 2.1.3 % 6.73/1.76 % (3917212)Termination reason: Refutation not found, incomplete strategy % 6.73/1.76 % (3917212)Time elapsed: 0.002 s % 6.73/1.76 % (3917212)Peak memory usage: 88 MB % 6.73/1.76 % (3917212)Instructions burned: 1 (million) % 6.73/1.76 % (3917211)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 6.73/1.76 % (3917213)Instruction limit reached! % 6.73/1.76 % (3917213)------------------------------ % 6.73/1.76 % (3917213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.73/1.76 % (3917213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.76 % (3917213)CaDiCaL version: 2.1.3 % 6.73/1.76 % (3917213)Termination reason: Instruction limit % 6.73/1.76 % (3917213)Termination phase: Saturation % 6.73/1.76 % (3917213)Time elapsed: 0.050 s % 6.73/1.76 % (3917213)Peak memory usage: 87 MB % 6.73/1.76 % (3917213)Instructions burned: 121 (million) % 6.73/1.76 % (3917215)Instruction limit reached! % 6.73/1.76 % (3917215)------------------------------ % 6.73/1.76 % (3917215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.73/1.76 % (3917215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.76 % (3917215)CaDiCaL version: 2.1.3 % 6.73/1.76 % (3917215)Termination reason: Instruction limit % 6.73/1.76 % (3917215)Termination phase: Saturation % 6.73/1.76 % (3917215)Time elapsed: 0.060 s % 6.73/1.76 % (3917215)Peak memory usage: 88 MB % 6.73/1.76 % (3917215)Instructions burned: 130 (million) % 6.73/1.76 % (3917214)Instruction limit reached! % 6.73/1.76 % (3917214)------------------------------ % 6.73/1.76 % (3917214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.73/1.76 % (3917214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.76 % (3917214)CaDiCaL version: 2.1.3 % 6.73/1.76 % (3917214)Termination reason: Instruction limit % 6.73/1.76 % (3917214)Termination phase: Saturation % 6.73/1.76 % (3917214)Time elapsed: 0.081 s % 6.73/1.76 % (3917214)Peak memory usage: 89 MB % 6.73/1.76 % (3917214)Instructions burned: 139 (million) % 6.73/1.76 % Exception at run slice level % 6.73/1.76 User error: GNN currently only supports monomorphic FOL. % 6.73/1.76 % (3917223)lrs+10_1_sil=8000:sp=occurrence:random_seed=2880591964:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 6.73/1.76 % (3917224)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2497639963:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 6.73/1.76 % (3917225)lrs+1011_1_sil=32000:sp=occurrence:random_seed=19903888:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 7.77/1.98 % (3917212)------------------------------ % 7.77/1.98 % (3917212)------------------------------ % 7.77/1.98 % (3917226)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=1340478323:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi) % 7.77/1.98 % (3917224)Instruction limit reached! % 7.77/1.98 % (3917224)------------------------------ % 7.77/1.98 % (3917224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.77/1.98 % (3917224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.77/1.98 % (3917224)CaDiCaL version: 2.1.3 % 7.77/1.98 % (3917224)Termination reason: Instruction limit % 7.77/1.98 % (3917224)Termination phase: Saturation % 7.77/1.98 % (3917224)Time elapsed: 0.081 s % 7.77/1.98 % (3917224)Peak memory usage: 89 MB % 7.77/1.98 % (3917224)Instructions burned: 158 (million) % 7.77/1.98 % (3917226)Instruction limit reached! % 7.77/1.98 % (3917226)------------------------------ % 7.77/1.98 % (3917226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.77/1.98 % (3917226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.77/1.98 % (3917226)CaDiCaL version: 2.1.3 % 7.77/1.98 % (3917226)Termination reason: Instruction limit % 7.77/1.98 % (3917226)Termination phase: Saturation % 7.77/1.98 % (3917226)Time elapsed: 0.074 s % 7.77/1.98 % (3917226)Peak memory usage: 90 MB % 7.77/1.98 % (3917226)Instructions burned: 249 (million) % 7.77/1.98 % Exception at run slice level % 7.77/1.98 User error: GNN currently only supports monomorphic FOL. % 7.77/1.98 % (3917223)Instruction limit reached! % 7.77/1.98 % (3917223)------------------------------ % 7.77/1.98 % (3917223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.77/1.98 % (3917223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.77/1.98 % (3917223)CaDiCaL version: 2.1.3 % 7.77/1.98 % (3917223)Termination reason: Instruction limit % 7.77/1.98 % (3917223)Termination phase: Saturation % 7.77/1.98 % (3917223)Time elapsed: 0.151 s % 7.77/1.98 % (3917223)Peak memory usage: 89 MB % 7.77/1.98 % (3917223)Instructions burned: 285 (million) % 7.77/1.98 % Exception at run slice level % 7.77/1.98 User error: GNN currently only supports monomorphic FOL. % 7.77/1.98 % (3917230)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2686213697:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 7.77/1.98 % (3917230)Refutation not found, incomplete strategy % 7.77/1.98 % (3917230)------------------------------ % 7.77/1.98 % (3917230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.77/1.98 % (3917230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.77/1.98 % (3917230)CaDiCaL version: 2.1.3 % 7.77/1.98 % (3917230)Termination reason: Refutation not found, incomplete strategy % 7.77/1.98 % (3917230)Time elapsed: 0.006 s % 7.77/1.98 % (3917230)Peak memory usage: 88 MB % 7.77/1.98 % (3917230)Instructions burned: 8 (million) % 7.77/1.98 % (3917225)Instruction limit reached! % 7.77/1.98 % (3917225)------------------------------ % 7.77/1.98 % (3917225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.77/1.98 % (3917225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.77/1.98 % (3917225)CaDiCaL version: 2.1.3 % 7.77/1.98 % (3917225)Termination reason: Instruction limit % 7.77/1.98 % (3917225)Termination phase: Saturation % 7.77/1.98 % (3917225)Time elapsed: 0.177 s % 7.77/1.98 % (3917225)Peak memory usage: 90 MB % 7.77/1.98 % (3917225)Instructions burned: 325 (million) % 7.77/1.98 % (3917232)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3268571743:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 7.77/1.98 % (3917233)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1644672317:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 7.77/1.98 % (3917233)Instruction limit reached! % 7.77/1.98 % (3917233)------------------------------ % 7.77/1.98 % (3917233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.77/1.98 % (3917233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.77/1.98 % (3917233)CaDiCaL version: 2.1.3 % 7.77/1.98 % (3917233)Termination reason: Instruction limit % 7.77/1.98 % (3917233)Termination phase: Saturation % 7.77/1.98 % (3917233)Time elapsed: 0.038 s % 7.77/1.98 % (3917233)Peak memory usage: 90 MB % 7.77/1.98 % (3917233)Instructions burned: 114 (million) % 11.16/2.35 % (3917234)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1715338784:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 11.16/2.35 % (3917234)Refutation not found, incomplete strategy % 11.16/2.35 % (3917234)------------------------------ % 11.16/2.35 % (3917234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.16/2.35 % (3917234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.16/2.35 % (3917234)CaDiCaL version: 2.1.3 % 11.16/2.35 % (3917234)Termination reason: Refutation not found, incomplete strategy % 11.16/2.35 % (3917234)Time elapsed: 0.004 s % 11.16/2.35 % (3917234)Peak memory usage: 87 MB % 11.16/2.35 % (3917234)Instructions burned: 6 (million) % 11.16/2.35 % (3917235)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=941086056:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 11.16/2.35 % (3917235)Refutation not found, incomplete strategy % 11.16/2.35 % (3917235)------------------------------ % 11.16/2.35 % (3917235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.16/2.35 % (3917235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.16/2.35 % (3917235)CaDiCaL version: 2.1.3 % 11.16/2.35 % (3917235)Termination reason: Refutation not found, incomplete strategy % 11.16/2.35 % (3917235)Time elapsed: 0.003 s % 11.16/2.35 % (3917235)Peak memory usage: 88 MB % 11.16/2.35 % (3917235)Instructions burned: 4 (million) % 11.16/2.35 % (3917236)lrs+10_1_sil=8000:sp=occurrence:random_seed=558885356:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 11.16/2.35 % (3917238)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2812634728:i=437:sd=1:aac=none:ss=included_2994 on theBenchmark for (2994ds/437Mi) % 11.16/2.35 % (3917242)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2955951811:i=5202:ss=axioms:sgt=16_2993 on theBenchmark for (2993ds/5202Mi) % 11.16/2.35 % (3917230)------------------------------ % 11.16/2.35 % (3917230)------------------------------ % 11.16/2.35 % (3917234)------------------------------ % 11.16/2.35 % (3917234)------------------------------ % 11.16/2.35 % (3917235)------------------------------ % 11.16/2.35 % (3917235)------------------------------ % 11.16/2.35 % (3917238)Instruction limit reached! % 11.16/2.35 % (3917238)------------------------------ % 11.16/2.35 % (3917238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.16/2.35 % (3917238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.16/2.35 % (3917238)CaDiCaL version: 2.1.3 % 11.16/2.35 % (3917238)Termination reason: Instruction limit % 11.16/2.35 % (3917238)Termination phase: Saturation % 11.16/2.35 % (3917238)Time elapsed: 0.216 s % 11.16/2.35 % (3917238)Peak memory usage: 91 MB % 11.16/2.35 % (3917238)Instructions burned: 439 (million) % 11.16/2.35 % Exception at run slice level % 11.16/2.35 User error: GNN currently only supports monomorphic FOL. % 11.16/2.35 % Exception at run slice level % 11.16/2.35 User error: GNN currently only supports monomorphic FOL. % 11.16/2.35 % (3917247)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1864143508:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2991 on theBenchmark for (2991ds/134Mi) % 11.16/2.35 % (3917248)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3945875294:st=8:i=592:sd=3:ep=RST:ss=axioms_2990 on theBenchmark for (2990ds/592Mi) % 11.16/2.35 % (3917248)Refutation not found, incomplete strategy % 11.16/2.35 % (3917248)------------------------------ % 11.16/2.35 % (3917248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.16/2.35 % (3917248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.16/2.35 % (3917248)CaDiCaL version: 2.1.3 % 11.16/2.35 % (3917248)Termination reason: Refutation not found, incomplete strategy % 11.16/2.35 % (3917248)Time elapsed: 0.004 s % 11.16/2.35 % (3917248)Peak memory usage: 88 MB % 11.16/2.35 % (3917248)Instructions burned: 6 (million) % 11.16/2.35 % (3917249)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=153840610:st=3:i=13193:sd=3:ss=axioms_2990 on theBenchmark for (2990ds/13193Mi) % 11.16/2.35 % (3917251)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4221509863:i=134:gtgl=5:slsql=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/134Mi) % 11.16/2.35 % (3917247)Instruction limit reached! % 11.16/2.35 % (3917247)------------------------------ % 11.16/2.35 % (3917247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.68/2.88 % (3917247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.68/2.88 % (3917247)CaDiCaL version: 2.1.3 % 13.68/2.88 % (3917247)Termination reason: Instruction limit % 13.68/2.88 % (3917247)Termination phase: Saturation % 13.68/2.88 % (3917247)Time elapsed: 0.081 s % 13.68/2.88 % (3917247)Peak memory usage: 89 MB % 13.68/2.88 % (3917247)Instructions burned: 136 (million) % 13.68/2.88 % (3917250)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=1005297362:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/125Mi) % 13.68/2.88 % (3917251)Instruction limit reached! % 13.68/2.88 % (3917251)------------------------------ % 13.68/2.88 % (3917251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.68/2.88 % (3917251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.68/2.88 % (3917251)CaDiCaL version: 2.1.3 % 13.68/2.88 % (3917251)Termination reason: Instruction limit % 13.68/2.88 % (3917251)Termination phase: Saturation % 13.68/2.88 % (3917251)Time elapsed: 0.040 s % 13.68/2.88 % (3917251)Peak memory usage: 89 MB % 13.68/2.88 % (3917251)Instructions burned: 135 (million) % 13.68/2.88 % (3917250)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.68/2.88 % (3917250)Refutation not found, incomplete strategy % 13.68/2.88 % (3917250)------------------------------ % 13.68/2.88 % (3917250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.68/2.88 % (3917250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.68/2.88 % (3917250)CaDiCaL version: 2.1.3 % 13.68/2.88 % (3917250)Termination reason: Refutation not found, incomplete strategy % 13.68/2.88 % (3917250)Time elapsed: 0.003 s % 13.68/2.88 % (3917250)Peak memory usage: 88 MB % 13.68/2.88 % (3917250)Instructions burned: 3 (million) % 13.68/2.88 % (3917252)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3734387123:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/141Mi) % 13.68/2.88 % (3917252)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.68/2.88 % (3917252)Refutation not found, incomplete strategy % 13.68/2.88 % (3917252)------------------------------ % 13.68/2.88 % (3917252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.68/2.88 % (3917252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.68/2.88 % (3917252)CaDiCaL version: 2.1.3 % 13.68/2.88 % (3917252)Termination reason: Refutation not found, incomplete strategy % 13.68/2.88 % (3917252)Time elapsed: 0.002 s % 13.68/2.88 % (3917252)Peak memory usage: 88 MB % 13.68/2.88 % (3917252)Instructions burned: 1 (million) % 13.68/2.88 % (3917236)Instruction limit reached! % 13.68/2.88 % (3917236)------------------------------ % 13.68/2.88 % (3917236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.68/2.88 % (3917236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.68/2.88 % (3917236)CaDiCaL version: 2.1.3 % 13.68/2.88 % (3917236)Termination reason: Instruction limit % 13.68/2.88 % (3917236)Termination phase: Saturation % 13.68/2.88 % (3917236)Time elapsed: 0.477 s % 13.68/2.88 % (3917236)Peak memory usage: 91 MB % 13.68/2.88 % (3917236)Instructions burned: 907 (million) % 13.68/2.88 % (3917257)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=604842027:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/431Mi) % 13.68/2.88 % (3917257)Refutation not found, incomplete strategy % 13.68/2.88 % (3917257)------------------------------ % 13.68/2.88 % (3917257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.68/2.88 % (3917257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.68/2.88 % (3917257)CaDiCaL version: 2.1.3 % 13.68/2.88 % (3917257)Termination reason: Refutation not found, incomplete strategy % 13.68/2.88 % (3917257)Time elapsed: 0.003 s % 13.68/2.88 % (3917257)Peak memory usage: 88 MB % 13.68/2.88 % (3917257)Instructions burned: 4 (million) % 13.68/2.88 % (3917248)------------------------------ % 13.68/2.88 % (3917248)------------------------------ % 13.68/2.88 % Exception at run slice level % 13.68/2.88 User error: GNN currently only supports monomorphic FOL. % 13.68/2.88 % (3917259)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=1572376848:i=6060:aac=none:ins=25_2988 on theBenchmark for (2988ds/6060Mi) % 19.95/3.60 % (3917261)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=81677513:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2988 on theBenchmark for (2988ds/150Mi) % 19.95/3.60 % (3917261)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 19.95/3.60 % (3917250)------------------------------ % 19.95/3.60 % (3917250)------------------------------ % 19.95/3.60 % (3917252)------------------------------ % 19.95/3.60 % (3917252)------------------------------ % 19.95/3.60 % (3917263)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=665298975:i=14155:bd=all_2986 on theBenchmark for (2986ds/14155Mi) % 19.95/3.60 % (3917261)Instruction limit reached! % 19.95/3.60 % (3917261)------------------------------ % 19.95/3.60 % (3917261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.95/3.60 % (3917261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.95/3.60 % (3917261)CaDiCaL version: 2.1.3 % 19.95/3.60 % (3917261)Termination reason: Instruction limit % 19.95/3.60 % (3917261)Termination phase: Saturation % 19.95/3.60 % (3917261)Time elapsed: 0.085 s % 19.95/3.60 % (3917261)Peak memory usage: 90 MB % 19.95/3.60 % (3917261)Instructions burned: 152 (million) % 19.95/3.60 % (3917264)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2195584345:i=667:av=off:fsr=off_2986 on theBenchmark for (2986ds/667Mi) % 19.95/3.60 % (3917257)------------------------------ % 19.95/3.60 % (3917257)------------------------------ % 19.95/3.60 % (3917267)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=882723069:s2a=on:i=185:s2at=1.8:fdi=4_2986 on theBenchmark for (2986ds/185Mi) % 19.95/3.60 % (3917268)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3165020742:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2985 on theBenchmark for (2985ds/193Mi) % 19.95/3.60 % (3917270)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3006101834:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2985 on theBenchmark for (2985ds/4850Mi) % 19.95/3.60 % (3917270)Refutation not found, incomplete strategy % 19.95/3.60 % (3917270)------------------------------ % 19.95/3.60 % (3917270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.95/3.60 % (3917270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.95/3.60 % (3917270)CaDiCaL version: 2.1.3 % 19.95/3.60 % (3917270)Termination reason: Refutation not found, incomplete strategy % 19.95/3.60 % (3917270)Time elapsed: 0.004 s % 19.95/3.60 % (3917270)Peak memory usage: 87 MB % 19.95/3.60 % (3917270)Instructions burned: 5 (million) % 19.95/3.60 % Exception at run slice level % 19.95/3.60 User error: GNN currently only supports monomorphic FOL. % 19.95/3.60 % (3917268)Instruction limit reached! % 19.95/3.60 % (3917268)------------------------------ % 19.95/3.60 % (3917268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.95/3.60 % (3917268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.95/3.60 % (3917268)CaDiCaL version: 2.1.3 % 19.95/3.60 % (3917268)Termination reason: Instruction limit % 19.95/3.60 % (3917268)Termination phase: Saturation % 19.95/3.60 % (3917268)Time elapsed: 0.086 s % 19.95/3.60 % (3917268)Peak memory usage: 89 MB % 19.95/3.60 % (3917268)Instructions burned: 194 (million) % 19.95/3.60 % (3917272)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2325933446:i=12111:sd=1:ss=included_2985 on theBenchmark for (2985ds/12111Mi) % 19.95/3.60 % (3917267)Instruction limit reached! % 19.95/3.60 % (3917267)------------------------------ % 19.95/3.60 % (3917267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.95/3.60 % (3917267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.95/3.60 % (3917267)CaDiCaL version: 2.1.3 % 19.95/3.60 % (3917267)Termination reason: Instruction limit % 19.95/3.60 % (3917267)Termination phase: Saturation % 19.95/3.60 % (3917267)Time elapsed: 0.117 s % 19.95/3.60 % (3917267)Peak memory usage: 91 MB % 19.95/3.60 % (3917267)Instructions burned: 185 (million) % 19.95/3.60 % Exception at run slice level % 19.95/3.60 User error: GNN currently only supports monomorphic FOL. % 26.96/4.68 % (3917264)Instruction limit reached! % 26.96/4.68 % (3917264)------------------------------ % 26.96/4.68 % (3917264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.96/4.68 % (3917264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.96/4.68 % (3917264)CaDiCaL version: 2.1.3 % 26.96/4.68 % (3917264)Termination reason: Instruction limit % 26.96/4.68 % (3917264)Termination phase: Saturation % 26.96/4.68 % (3917264)Time elapsed: 0.264 s % 26.96/4.68 % (3917264)Peak memory usage: 88 MB % 26.96/4.68 % (3917264)Instructions burned: 668 (million) % 26.96/4.68 % (3917276)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1388785804:i=319:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/319Mi) % 26.96/4.68 % (3917277)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=4169418344:i=2064:ep=RST_2983 on theBenchmark for (2983ds/2064Mi) % 26.96/4.68 % (3917277)Refutation not found, incomplete strategy % 26.96/4.68 % (3917277)------------------------------ % 26.96/4.68 % (3917277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.96/4.68 % (3917277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.96/4.68 % (3917277)CaDiCaL version: 2.1.3 % 26.96/4.68 % (3917277)Termination reason: Refutation not found, incomplete strategy % 26.96/4.68 % (3917277)Time elapsed: 0.004 s % 26.96/4.68 % (3917277)Peak memory usage: 88 MB % 26.96/4.68 % (3917277)Instructions burned: 6 (million) % 26.96/4.68 % (3917279)dis-1011_128_sil=32000:random_seed=1943119023:i=3706:ep=RST:av=off_2983 on theBenchmark for (2983ds/3706Mi) % 26.96/4.68 % (3917270)------------------------------ % 26.96/4.68 % (3917270)------------------------------ % 26.96/4.68 % (3917276)Instruction limit reached! % 26.96/4.68 % (3917276)------------------------------ % 26.96/4.68 % (3917276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.96/4.68 % (3917276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.96/4.68 % (3917276)CaDiCaL version: 2.1.3 % 26.96/4.68 % (3917276)Termination reason: Instruction limit % 26.96/4.68 % (3917276)Termination phase: Saturation % 26.96/4.68 % (3917276)Time elapsed: 0.096 s % 26.96/4.68 % (3917276)Peak memory usage: 91 MB % 26.96/4.68 % (3917276)Instructions burned: 319 (million) % 26.96/4.68 % (3917280)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2563322444:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2983 on theBenchmark for (2983ds/757Mi) % 26.96/4.68 % (3917281)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1268536993:i=13913:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/13913Mi) % 26.96/4.68 % (3917286)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=931049851:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2981 on theBenchmark for (2981ds/2479Mi) % 26.96/4.68 % (3917286)Refutation not found, incomplete strategy % 26.96/4.68 % (3917286)------------------------------ % 26.96/4.68 % (3917286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.96/4.68 % (3917286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.96/4.68 % (3917286)CaDiCaL version: 2.1.3 % 26.96/4.68 % (3917286)Termination reason: Refutation not found, incomplete strategy % 26.96/4.68 % (3917286)Time elapsed: 0.001 s % 26.96/4.68 % (3917286)Peak memory usage: 88 MB % 26.96/4.68 % (3917286)Instructions burned: 1 (million) % 26.96/4.68 % (3917285)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1653865223:i=9925:aac=none_2981 on theBenchmark for (2981ds/9925Mi) % 26.96/4.68 % Exception at run slice level % 26.96/4.68 User error: GNN currently only supports monomorphic FOL. % 26.96/4.68 % (3917277)------------------------------ % 26.96/4.68 % (3917277)------------------------------ % 26.96/4.68 % (3917286)------------------------------ % 26.96/4.68 % (3917286)------------------------------ % 26.96/4.68 % (3917291)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1778092585:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2979 on theBenchmark for (2979ds/440Mi) % 26.96/4.68 % (3917291)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 26.96/4.68 % (3917292)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4180764955:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2979 on theBenchmark for (2979ds/11145Mi) % 32.74/5.33 % (3917293)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=2159514076:cts=off:i=3034:av=off:er=known:fsd=on_2979 on theBenchmark for (2979ds/3034Mi) % 32.74/5.33 % Exception at run slice level % 32.74/5.33 User error: GNN currently only supports monomorphic FOL. % 32.74/5.33 % (3917280)Instruction limit reached! % 32.74/5.33 % (3917280)------------------------------ % 32.74/5.33 % (3917280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.74/5.33 % (3917280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.74/5.33 % (3917280)CaDiCaL version: 2.1.3 % 32.74/5.33 % (3917280)Termination reason: Instruction limit % 32.74/5.33 % (3917280)Termination phase: Saturation % 32.74/5.33 % (3917280)Time elapsed: 0.413 s % 32.74/5.33 % (3917280)Peak memory usage: 99 MB % 32.74/5.33 % (3917280)Instructions burned: 758 (million) % 32.74/5.33 % Exception at run slice level % 32.74/5.33 User error: GNN currently only supports monomorphic FOL. % 32.74/5.33 % (3917297)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2943573052:st=2:s2a=on:i=524:s2at=2:ss=axioms_2977 on theBenchmark for (2977ds/524Mi) % 32.74/5.33 % Exception at run slice level % 32.74/5.33 User error: GNN currently only supports monomorphic FOL. % 32.74/5.33 % (3917291)Instruction limit reached! % 32.74/5.33 % (3917291)------------------------------ % 32.74/5.33 % (3917291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.74/5.33 % (3917291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.74/5.33 % (3917291)CaDiCaL version: 2.1.3 % 32.74/5.33 % (3917291)Termination reason: Instruction limit % 32.74/5.33 % (3917291)Termination phase: Saturation % 32.74/5.33 % (3917291)Time elapsed: 0.227 s % 32.74/5.33 % (3917291)Peak memory usage: 89 MB % 32.74/5.33 % (3917291)Instructions burned: 440 (million) % 32.74/5.33 % (3917298)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2037936627:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2977 on theBenchmark for (2977ds/1016Mi) % 32.74/5.33 % (3917299)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3496180621:i=14123:bd=preordered:ins=4_2976 on theBenchmark for (2976ds/14123Mi) % 32.74/5.33 % (3917301)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2897641814:i=5781:kws=precedence:bd=all:rawr=on_2975 on theBenchmark for (2975ds/5781Mi) % 32.74/5.33 % (3917303)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=485849742:i=2448:gtgl=5:bd=preordered:gtg=all_2975 on theBenchmark for (2975ds/2448Mi) % 32.74/5.33 % Exception at run slice level % 32.74/5.33 User error: GNN currently only supports monomorphic FOL. % 32.74/5.33 % (3917297)Instruction limit reached! % 32.74/5.33 % (3917297)------------------------------ % 32.74/5.33 % (3917297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.74/5.33 % (3917297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.74/5.33 % (3917297)CaDiCaL version: 2.1.3 % 32.74/5.33 % (3917297)Termination reason: Instruction limit % 32.74/5.33 % (3917297)Termination phase: Saturation % 32.74/5.33 % (3917297)Time elapsed: 0.271 s % 32.74/5.33 % (3917297)Peak memory usage: 91 MB % 32.74/5.33 % (3917297)Instructions burned: 526 (million) % 32.74/5.33 % (3917307)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3009024937:i=3223:kws=precedence:fgj=on:av=off_2974 on theBenchmark for (2974ds/3223Mi) % 32.74/5.33 % (3917308)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2663154662:st=5.6:i=2033:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/2033Mi) % 32.74/5.33 % Exception at run slice level % 32.74/5.33 User error: GNN currently only supports monomorphic FOL. % 32.74/5.33 % Exception at run slice level % 32.74/5.33 User error: GNN currently only supports monomorphic FOL. % 32.74/5.33 % (3917298)Instruction limit reached! % 32.74/5.33 % (3917298)------------------------------ % 32.74/5.33 % (3917298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.74/5.33 % (3917298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.74/5.33 % (3917298)CaDiCaL version: 2.1.3 % 32.74/5.33 % (3917298)Termination reason: Instruction limit % 32.74/5.33 % (3917298)Termination phase: Saturation % 32.74/5.33 % (3917298)Time elapsed: 0.523 s % 32.74/5.33 % (3917298)Peak memory usage: 94 MB % 39.83/6.36 % (3917298)Instructions burned: 1016 (million) % 39.83/6.36 % (3917311)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=4264935724:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2971 on theBenchmark for (2971ds/2055Mi) % 39.83/6.36 % Exception at run slice level % 39.83/6.36 User error: GNN currently only supports monomorphic FOL. % 39.83/6.36 % (3917312)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=24684024:i=21611:sd=3:ss=axioms_2970 on theBenchmark for (2970ds/21611Mi) % 39.83/6.36 % (3917313)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1621184347:i=4835:sd=13:ss=axioms:sgt=23_2970 on theBenchmark for (2970ds/4835Mi) % 39.83/6.36 % (3917313)Refutation not found, incomplete strategy % 39.83/6.36 % (3917313)------------------------------ % 39.83/6.36 % (3917313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.83/6.36 % (3917313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.83/6.36 % (3917313)CaDiCaL version: 2.1.3 % 39.83/6.36 % (3917313)Termination reason: Refutation not found, incomplete strategy % 39.83/6.36 % (3917313)Time elapsed: 0.002 s % 39.83/6.36 % (3917313)Peak memory usage: 88 MB % 39.83/6.36 % (3917313)Instructions burned: 1 (million) % 39.83/6.36 % Exception at run slice level % 39.83/6.36 User error: GNN currently only supports monomorphic FOL. % 39.83/6.36 % (3917316)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=584442427:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2969 on theBenchmark for (2969ds/797Mi) % 39.83/6.36 % (3917318)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3633446976:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2968 on theBenchmark for (2968ds/2326Mi) % 39.83/6.36 % (3917313)------------------------------ % 39.83/6.36 % (3917313)------------------------------ % 39.83/6.36 % Exception at run slice level % 39.83/6.36 User error: GNN currently only supports monomorphic FOL. % 39.83/6.36 % Exception at run slice level % 39.83/6.36 User error: GNN currently only supports monomorphic FOL. % 39.83/6.36 % (3917321)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=153516215:i=6038:nm=6_2966 on theBenchmark for (2966ds/6038Mi) % 39.83/6.36 % (3917322)lrs+10_1_sil=32000:sp=occurrence:random_seed=3824783597:st=2:i=33334:sd=3:ss=included:sgt=32_2966 on theBenchmark for (2966ds/33334Mi) % 39.83/6.36 % (3917323)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3547307787:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2965 on theBenchmark for (2965ds/1008Mi) % 39.83/6.36 % (3917316)Instruction limit reached! % 39.83/6.36 % (3917316)------------------------------ % 39.83/6.36 % (3917316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.83/6.36 % (3917316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.83/6.36 % (3917316)CaDiCaL version: 2.1.3 % 39.83/6.36 % (3917316)Termination reason: Instruction limit % 39.83/6.36 % (3917316)Termination phase: Saturation % 39.83/6.36 % (3917316)Time elapsed: 0.500 s % 39.83/6.36 % (3917316)Peak memory usage: 94 MB % 39.83/6.36 % (3917316)Instructions burned: 797 (million) % 39.83/6.36 % Exception at run slice level % 39.83/6.36 User error: GNN currently only supports monomorphic FOL. % 39.83/6.36 % (3917327)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=3565225608:i=8327:s2at=5:bd=preordered_2962 on theBenchmark for (2962ds/8327Mi) % 39.83/6.36 % (3917279)Instruction limit reached! % 39.83/6.36 % (3917279)------------------------------ % 39.83/6.36 % (3917279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.83/6.36 % (3917279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.83/6.36 % (3917279)CaDiCaL version: 2.1.3 % 39.83/6.36 % (3917279)Termination reason: Instruction limit % 39.83/6.36 % (3917279)Termination phase: Saturation % 39.83/6.36 % (3917279)Time elapsed: 2.131 s % 39.83/6.36 % (3917279)Peak memory usage: 113 MB % 39.83/6.36 % (3917279)Instructions burned: 3707 (million) % 39.83/6.36 % (3917328)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=525954225:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2961 on theBenchmark for (2961ds/1083Mi) % 48.11/7.56 % (3917330)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1407918813:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2960 on theBenchmark for (2960ds/1084Mi) % 48.11/7.56 % (3917323)Instruction limit reached! % 48.11/7.56 % (3917323)------------------------------ % 48.11/7.56 % (3917323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.11/7.56 % (3917323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.11/7.56 % (3917323)CaDiCaL version: 2.1.3 % 48.11/7.56 % (3917323)Termination reason: Instruction limit % 48.11/7.56 % (3917323)Termination phase: Saturation % 48.11/7.56 % (3917323)Time elapsed: 0.524 s % 48.11/7.56 % (3917323)Peak memory usage: 95 MB % 48.11/7.56 % (3917323)Instructions burned: 1010 (million) % 48.11/7.56 % (3917301)Instruction limit reached! % 48.11/7.56 % (3917301)------------------------------ % 48.11/7.56 % (3917301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.11/7.56 % (3917301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.11/7.56 % (3917301)CaDiCaL version: 2.1.3 % 48.11/7.56 % (3917301)Termination reason: Instruction limit % 48.11/7.56 % (3917301)Termination phase: Saturation % 48.11/7.56 % (3917301)Time elapsed: 1.615 s % 48.11/7.56 % (3917301)Peak memory usage: 105 MB % 48.11/7.56 % (3917301)Instructions burned: 5782 (million) % 48.11/7.56 % (3917334)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1503167840:st=2:i=6225:sd=15:ss=axioms_2958 on theBenchmark for (2958ds/6225Mi) % 48.11/7.56 % (3917334)Refutation not found, incomplete strategy % 48.11/7.56 % (3917334)------------------------------ % 48.11/7.56 % (3917334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.11/7.56 % (3917334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.11/7.56 % (3917334)CaDiCaL version: 2.1.3 % 48.11/7.56 % (3917334)Termination reason: Refutation not found, incomplete strategy % 48.11/7.56 % (3917334)Time elapsed: 0.003 s % 48.11/7.56 % (3917334)Peak memory usage: 89 MB % 48.11/7.56 % (3917334)Instructions burned: 7 (million) % 48.11/7.56 % Exception at run slice level % 48.11/7.56 User error: GNN currently only supports monomorphic FOL. % 48.11/7.56 % (3917333)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=857958856:i=6995:s2at=5:gtg=all_2958 on theBenchmark for (2958ds/6995Mi) % 48.11/7.56 % (3917334)------------------------------ % 48.11/7.56 % (3917334)------------------------------ % 48.11/7.56 % (3917336)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2498860975:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2957 on theBenchmark for (2957ds/3372Mi) % 48.11/7.56 % (3917328)Instruction limit reached! % 48.11/7.56 % (3917328)------------------------------ % 48.11/7.56 % (3917328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.11/7.56 % (3917328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.11/7.56 % (3917328)CaDiCaL version: 2.1.3 % 48.11/7.56 % (3917328)Termination reason: Instruction limit % 48.11/7.56 % (3917328)Termination phase: Saturation % 48.11/7.56 % (3917328)Time elapsed: 0.474 s % 48.11/7.56 % (3917328)Peak memory usage: 92 MB % 48.11/7.56 % (3917328)Instructions burned: 1086 (million) % 48.11/7.56 % (3917338)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=65619387:st=2.3:i=26457:sd=10:ss=included:sgt=8_2956 on theBenchmark for (2956ds/26457Mi) % 48.11/7.56 % (3917318)Instruction limit reached! % 48.11/7.56 % (3917318)------------------------------ % 48.11/7.56 % (3917318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.11/7.56 % (3917318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.11/7.56 % (3917318)CaDiCaL version: 2.1.3 % 48.11/7.56 % (3917318)Termination reason: Instruction limit % 48.11/7.56 % (3917318)Termination phase: Saturation % 48.11/7.56 % (3917318)Time elapsed: 1.203 s % 48.11/7.56 % (3917318)Peak memory usage: 102 MB % 48.11/7.56 % (3917318)Instructions burned: 2328 (million) % 48.11/7.56 % (3917340)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=2867329460:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2955 on theBenchmark for (2955ds/13494Mi) % 48.11/7.56 % Exception at run slice level % 61.50/9.30 User error: GNN currently only supports monomorphic FOL. % 61.50/9.30 % (3917330)Instruction limit reached! % 61.50/9.30 % (3917330)------------------------------ % 61.50/9.30 % (3917330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.50/9.30 % (3917330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.50/9.30 % (3917330)CaDiCaL version: 2.1.3 % 61.50/9.30 % (3917330)Termination reason: Instruction limit % 61.50/9.30 % (3917330)Termination phase: Saturation % 61.50/9.30 % (3917330)Time elapsed: 0.583 s % 61.50/9.30 % (3917330)Peak memory usage: 93 MB % 61.50/9.30 % (3917330)Instructions burned: 1084 (million) % 61.50/9.30 % (3917342)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=2884500129:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2954 on theBenchmark for (2954ds/2503Mi) % 61.50/9.30 % (3917342)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 61.50/9.30 % Exception at run slice level % 61.50/9.30 User error: GNN currently only supports monomorphic FOL. % 61.50/9.30 % (3917344)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=1751684530:i=2559:sd=1:ep=RSTC:ss=axioms_2953 on theBenchmark for (2953ds/2559Mi) % 61.50/9.30 % Exception at run slice level % 61.50/9.30 User error: GNN currently only supports monomorphic FOL. % 61.50/9.30 % (3917345)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2110742836:i=30753:av=off:ss=included_2953 on theBenchmark for (2953ds/30753Mi) % 61.50/9.30 % (3917347)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=820621860:i=26473:ep=RSTC_2952 on theBenchmark for (2952ds/26473Mi) % 61.50/9.30 % (3917349)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=542831132:cts=off:i=2759:kws=inv_arity:fgj=on_2951 on theBenchmark for (2951ds/2759Mi) % 61.50/9.30 % Exception at run slice level % 61.50/9.30 User error: GNN currently only supports monomorphic FOL. % 61.50/9.30 % Exception at run slice level % 61.50/9.30 User error: GNN currently only supports monomorphic FOL. % 61.50/9.30 % Exception at run slice level % 61.50/9.30 User error: GNN currently only supports monomorphic FOL. % 61.50/9.30 % (3917353)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=4211886865:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2949 on theBenchmark for (2949ds/5665Mi) % 61.50/9.30 % (3917353)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 61.50/9.30 % Exception at run slice level % 61.50/9.30 User error: GNN currently only supports monomorphic FOL. % 61.50/9.30 % (3917354)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=3159877876:i=1532:ep=RS:ss=axioms_2949 on theBenchmark for (2949ds/1532Mi) % 61.50/9.30 % (3917355)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=1322383147:i=1565:sd=2:ss=axioms:sgt=32_2948 on theBenchmark for (2948ds/1565Mi) % 61.50/9.30 % Exception at run slice level % 61.50/9.30 User error: GNN currently only supports monomorphic FOL. % 61.50/9.31 % (3917357)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=1110612982:i=1572:fgj=on:gsp=on_2948 on theBenchmark for (2948ds/1572Mi) % 61.50/9.31 % (3917357)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 61.50/9.31 % (3917360)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=557217085:i=6052:sd=4:ss=axioms:sgt=24_2946 on theBenchmark for (2946ds/6052Mi) % 61.50/9.31 % Exception at run slice level % 61.50/9.31 User error: GNN currently only supports monomorphic FOL. % 61.50/9.31 % Exception at run slice level % 61.50/9.31 User error: GNN currently only supports monomorphic FOL. % 61.50/9.31 % Exception at run slice level % 61.50/9.31 User error: GNN currently only supports monomorphic FOL. % 61.50/9.31 % (3917363)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=3364307747:i=3500:sd=1:bd=preordered:sup=off:ss=included_2944 on theBenchmark for (2944ds/3500Mi) % 70.48/10.86 % Exception at run slice level % 70.48/10.86 User error: GNN currently only supports monomorphic FOL. % 70.48/10.86 % (3917364)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=3847273882:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2944 on theBenchmark for (2944ds/1842Mi) % 70.48/10.86 % (3917364)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 70.48/10.86 % (3917365)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=296973626:i=66096:add=on_2943 on theBenchmark for (2943ds/66096Mi) % 70.48/10.86 % Exception at run slice level % 70.48/10.86 User error: GNN currently only supports monomorphic FOL. % 70.48/10.86 % (3917367)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=3311729781:i=1884:sd=1:nm=60:ss=axioms_2943 on theBenchmark for (2943ds/1884Mi) % 70.48/10.86 % (3917370)lrs-1011_4:1_sil=16000:bsr=on:random_seed=1268915246:cts=off:i=5469:bs=on:fsr=off_2941 on theBenchmark for (2941ds/5469Mi) % 70.48/10.86 % Exception at run slice level % 70.48/10.86 User error: GNN currently only supports monomorphic FOL. % 70.48/10.86 % Exception at run slice level % 70.48/10.86 User error: GNN currently only supports monomorphic FOL. % 70.48/10.86 % Exception at run slice level % 70.48/10.86 User error: GNN currently only supports monomorphic FOL. % 70.48/10.86 % (3917373)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=3952734900:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2939 on theBenchmark for (2939ds/2037Mi) % 70.48/10.86 % Exception at run slice level % 70.48/10.86 User error: GNN currently only supports monomorphic FOL. % 70.48/10.86 % (3917374)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=491936001:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2938 on theBenchmark for (2938ds/2110Mi) % 70.48/10.86 % (3917375)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=1448634086:i=2430:add=off:aac=none:nm=16_2938 on theBenchmark for (2938ds/2430Mi) % 70.48/10.86 % (3917377)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=1503868642:cond=fast:i=4891_2937 on theBenchmark for (2937ds/4891Mi) % 70.48/10.86 % Exception at run slice level % 70.48/10.86 User error: GNN currently only supports monomorphic FOL. % 70.48/10.86 % Exception at run slice level % 70.48/10.86 User error: GNN currently only supports monomorphic FOL. % 70.48/10.86 % Exception at run slice level % 70.48/10.86 User error: GNN currently only supports monomorphic FOL. % 70.48/10.86 % (3917381)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=1835653084:st=2:i=14845:sd=2:ss=included:fsd=on_2934 on theBenchmark for (2934ds/14845Mi) % 70.48/10.86 % Exception at run slice level % 70.48/10.86 User error: GNN currently only supports monomorphic FOL. % 70.48/10.86 % (3917382)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=3355670804:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2933 on theBenchmark for (2933ds/7534Mi) % 70.48/10.86 % (3917383)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=1770312155:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2933 on theBenchmark for (2933ds/10353Mi) % 70.48/10.86 % (3917385)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2083422767:i=7860_2932 on theBenchmark for (2932ds/7860Mi) % 70.48/10.86 % (3917385)Refutation not found, incomplete strategy % 70.48/10.86 % (3917385)------------------------------ % 70.48/10.86 % (3917385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.48/10.86 % (3917385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.48/10.86 % (3917385)CaDiCaL version: 2.1.3 % 70.48/10.86 % (3917385)Termination reason: Refutation not found, incomplete strategy % 70.48/10.86 % (3917385)Time elapsed: 0.005 s % 83.52/12.59 % (3917385)Peak memory usage: 88 MB % 83.52/12.59 % (3917385)Instructions burned: 7 (million) % 83.52/12.59 % Exception at run slice level % 83.52/12.59 User error: GNN currently only supports monomorphic FOL. % 83.52/12.59 % (3917385)------------------------------ % 83.52/12.59 % (3917385)------------------------------ % 83.52/12.59 % Exception at run slice level % 83.52/12.59 User error: GNN currently only supports monomorphic FOL. % 83.52/12.59 % Exception at run slice level % 83.52/12.59 User error: GNN currently only supports monomorphic FOL. % 83.52/12.59 % (3917389)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=3412929837:i=7896:sd=2:bs=on:ss=included:sgt=20_2929 on theBenchmark for (2929ds/7896Mi) % 83.52/12.59 % (3917390)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=3813161508:i=5812:gtgl=2:gtg=all_2928 on theBenchmark for (2928ds/5812Mi) % 83.52/12.59 % (3917391)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=1225009030:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2928 on theBenchmark for (2928ds/2965Mi) % 83.52/12.59 % (3917392)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=2351183185:i=2967:kws=precedence:bd=preordered:av=off_2927 on theBenchmark for (2927ds/2967Mi) % 83.52/12.59 % Exception at run slice level % 83.52/12.59 User error: GNN currently only supports monomorphic FOL. % 83.52/12.59 % Exception at run slice level % 83.52/12.59 User error: GNN currently only supports monomorphic FOL. % 83.52/12.59 % Exception at run slice level % 83.52/12.59 User error: GNN currently only supports monomorphic FOL. % 83.52/12.59 % Exception at run slice level % 83.52/12.59 User error: GNN currently only supports monomorphic FOL. % 83.52/12.59 % (3917397)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=1847748328:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2923 on theBenchmark for (2923ds/3022Mi) % 83.52/12.59 % (3917398)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=3113439099:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2923 on theBenchmark for (2923ds/3207Mi) % 83.52/12.59 % (3917399)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=3166218220:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2923 on theBenchmark for (2923ds/3289Mi) % 83.52/12.59 % (3917400)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=3094870287:i=38569:sd=3:ss=axioms:sgt=32_2922 on theBenchmark for (2922ds/38569Mi) % 83.52/12.59 % Exception at run slice level % 83.52/12.59 User error: GNN currently only supports monomorphic FOL. % 83.52/12.59 % Exception at run slice level % 83.52/12.59 User error: GNN currently only supports monomorphic FOL. % 83.52/12.59 % Exception at run slice level % 83.52/12.59 User error: GNN currently only supports monomorphic FOL. % 83.52/12.59 % Exception at run slice level % 83.52/12.59 User error: GNN currently only supports monomorphic FOL. % 83.52/12.59 % (3917405)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=2163675396:cts=off:i=3394_2918 on theBenchmark for (2918ds/3394Mi) % 83.52/12.59 % (3917406)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=1419222468:i=33824:bd=preordered_2918 on theBenchmark for (2918ds/33824Mi) % 83.52/12.59 % (3917407)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=3521608766:i=20684:bd=all:gtg=exists_sym_2917 on theBenchmark for (2917ds/20684Mi) % 83.52/12.59 % (3917408)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=3761363268:st=3:prac=on:i=7222:kws=arity_squared:add=on:fgj=on:bd=preordered:gtg=exists_top:gsp=on:ss=axioms:er=known:sgt=8:proc=on_2917 on theBenchmark for (2917ds/7222Mi) % 83.52/12.59 % (3917408)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 83.52/12.59 % Exception at run slice level % 83.52/12.59 User error: GNN currently only supports monomorphic FOL. % 104.27/15.40 % Exception at run slice level % 104.27/15.40 User error: GNN currently only supports monomorphic FOL. % 104.27/15.40 % Exception at run slice level % 104.27/15.40 User error: GNN currently only supports monomorphic FOL. % 104.27/15.40 % Exception at run slice level % 104.27/15.40 User error: GNN currently only supports monomorphic FOL. % 104.27/15.40 % (3917413)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=3586834646:st=4:i=7295:sd=4:ep=R:ss=axioms_2913 on theBenchmark for (2913ds/7295Mi) % 104.27/15.40 % (3917414)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=2513374367:i=4036:ins=10_2913 on theBenchmark for (2913ds/4036Mi) % 104.27/15.40 % (3917415)lrs+10_1_sil=128000:lcm=predicate:random_seed=88586061:st=3:i=43697:sd=5:ss=axioms_2912 on theBenchmark for (2912ds/43697Mi) % 104.27/15.40 % (3917416)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=1727882769:i=17599:gtg=all:ss=axioms:fsd=on_2912 on theBenchmark for (2912ds/17599Mi) % 104.27/15.40 % (3917370)Instruction limit reached! % 104.27/15.40 % (3917370)------------------------------ % 104.27/15.40 % (3917370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.27/15.40 % (3917370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.27/15.40 % (3917370)CaDiCaL version: 2.1.3 % 104.27/15.40 % (3917370)Termination reason: Instruction limit % 104.27/15.40 % (3917370)Termination phase: Saturation % 104.27/15.40 % (3917370)Time elapsed: 3.122 s % 104.27/15.40 % (3917370)Peak memory usage: 106 MB % 104.27/15.40 % (3917370)Instructions burned: 5469 (million) % 104.27/15.40 % Exception at run slice level % 104.27/15.40 User error: GNN currently only supports monomorphic FOL. % 104.27/15.40 % Exception at run slice level % 104.27/15.40 User error: GNN currently only supports monomorphic FOL. % 104.27/15.40 % Exception at run slice level % 104.27/15.40 User error: GNN currently only supports monomorphic FOL. % 104.27/15.40 % (3917421)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=1892302254:i=4547:bd=preordered_2908 on theBenchmark for (2908ds/4547Mi) % 104.27/15.40 % (3917422)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=1440350394:i=9294:av=off_2908 on theBenchmark for (2908ds/9294Mi) % 104.27/15.40 % (3917423)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3549744261:i=32849:add=on_2908 on theBenchmark for (2908ds/32849Mi) % 104.27/15.40 % (3917426)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2852030912:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2907 on theBenchmark for (2907ds/4793Mi) % 104.27/15.40 % Exception at run slice level % 104.27/15.40 User error: GNN currently only supports monomorphic FOL. % 104.27/15.40 % Exception at run slice level % 104.27/15.40 User error: GNN currently only supports monomorphic FOL. % 104.27/15.40 % Exception at run slice level % 104.27/15.40 User error: GNN currently only supports monomorphic FOL. % 104.27/15.40 % (3917429)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=1057977164:i=4840:nm=4:av=off_2903 on theBenchmark for (2903ds/4840Mi) % 104.27/15.40 % Exception at run slice level % 104.27/15.40 User error: GNN currently only supports monomorphic FOL. % 104.27/15.40 % (3917430)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=2956581575:cts=off:i=5002_2903 on theBenchmark for (2903ds/5002Mi) % 104.27/15.40 % (3917431)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=1375998665:i=30479:sd=3:ss=axioms_2902 on theBenchmark for (2902ds/30479Mi) % 104.27/15.40 % (3917433)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=625194298:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2901 on theBenchmark for (2901ds/11035Mi) % 104.27/15.40 % (3917433)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 104.27/15.40 % Exception at run slice level % 104.27/15.40 User error: GNN currently only supports monomorphic FOL. % 123.88/18.17 % Exception at run slice level % 123.88/18.17 User error: GNN currently only supports monomorphic FOL. % 123.88/18.17 % Exception at run slice level % 123.88/18.17 User error: GNN currently only supports monomorphic FOL. % 123.88/18.17 % (3917437)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=278310956:i=5835_2898 on theBenchmark for (2898ds/5835Mi) % 123.88/18.17 % Exception at run slice level % 123.88/18.17 User error: GNN currently only supports monomorphic FOL. % 123.88/18.17 % (3917439)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=3617702125:cts=off:i=19910:ep=RS_2897 on theBenchmark for (2897ds/19910Mi) % 123.88/18.17 % (3917439)Refutation not found, incomplete strategy % 123.88/18.17 % (3917439)------------------------------ % 123.88/18.17 % (3917439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.88/18.17 % (3917439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.88/18.17 % (3917439)CaDiCaL version: 2.1.3 % 123.88/18.17 % (3917439)Termination reason: Refutation not found, incomplete strategy % 123.88/18.17 % (3917439)Time elapsed: 0.004 s % 123.88/18.17 % (3917439)Peak memory usage: 88 MB % 123.88/18.17 % (3917439)Instructions burned: 6 (million) % 123.88/18.17 % (3917438)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=3800588979:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2897 on theBenchmark for (2897ds/5890Mi) % 123.88/18.17 % (3917441)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=3574900370:i=20312:bd=preordered:fsr=off:er=filter_2896 on theBenchmark for (2896ds/20312Mi) % 123.88/18.17 % (3917439)------------------------------ % 123.88/18.17 % (3917439)------------------------------ % 123.88/18.17 % Exception at run slice level % 123.88/18.17 User error: GNN currently only supports monomorphic FOL. % 123.88/18.17 % Exception at run slice level % 123.88/18.17 User error: GNN currently only supports monomorphic FOL. % 123.88/18.17 % (3917445)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=4159003945:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2893 on theBenchmark for (2893ds/13822Mi) % 123.88/18.17 % Exception at run slice level % 123.88/18.17 User error: GNN currently only supports monomorphic FOL. % 123.88/18.17 % (3917446)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=3797311770:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2892 on theBenchmark for (2892ds/7144Mi) % 123.88/18.17 % (3917447)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=839207544:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2892 on theBenchmark for (2892ds/15184Mi) % 123.88/18.17 % (3917450)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=907400762:i=107375_2891 on theBenchmark for (2891ds/107375Mi) % 123.88/18.17 % Exception at run slice level % 123.88/18.17 User error: GNN currently only supports monomorphic FOL. % 123.88/18.17 % Exception at run slice level % 123.88/18.17 User error: GNN currently only supports monomorphic FOL. % 123.88/18.17 % Exception at run slice level % 123.88/18.17 User error: GNN currently only supports monomorphic FOL. % 123.88/18.17 % (3917453)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=736061421:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2887 on theBenchmark for (2887ds/7958Mi) % 123.88/18.17 % (3917454)dis+10_128_sil=16000:nwc=0.7:random_seed=4136410120:i=15999:nm=2:gsp=on_2886 on theBenchmark for (2886ds/15999Mi) % 123.88/18.17 % (3917454)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 123.88/18.17 % (3917456)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=3389961689:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2886 on theBenchmark for (2886ds/8139Mi) % 123.88/18.17 % Exception at run slice level % 123.88/18.17 User error: GNN currently only supports monomorphic FOL. % 123.88/18.17 % (3917459)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=275739345:st=4:i=8950:sd=5:ss=axioms_2882 on theBenchmark for (2882ds/8950Mi) % 152.82/22.25 % Exception at run slice level % 152.82/22.25 User error: GNN currently only supports monomorphic FOL. % 152.82/22.25 % (3917461)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=4145793746:i=9809:ins=10:av=off_2877 on theBenchmark for (2877ds/9809Mi) % 152.82/22.25 % Exception at run slice level % 152.82/22.25 User error: GNN currently only supports monomorphic FOL. % 152.82/22.25 % (3917463)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=1880749239:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2872 on theBenchmark for (2872ds/9885Mi) % 152.82/22.25 % (3917347)Instruction limit reached! % 152.82/22.25 % (3917347)------------------------------ % 152.82/22.25 % (3917347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.82/22.25 % (3917347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.82/22.25 % (3917347)CaDiCaL version: 2.1.3 % 152.82/22.25 % (3917347)Termination reason: Instruction limit % 152.82/22.25 % (3917347)Termination phase: Saturation % 152.82/22.25 % (3917347)Time elapsed: 8.197 s % 152.82/22.25 % (3917347)Peak memory usage: 237 MB % 152.82/22.25 % (3917347)Instructions burned: 26473 (million) % 152.82/22.25 % (3917465)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=23184268:cond=fast:i=32078:fgj=on:av=off_2869 on theBenchmark for (2869ds/32078Mi) % 152.82/22.25 % Exception at run slice level % 152.82/22.25 User error: GNN currently only supports monomorphic FOL. % 152.82/22.25 % Exception at run slice level % 152.82/22.25 User error: GNN currently only supports monomorphic FOL. % 152.82/22.25 % (3917467)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=1886886077:i=11101:bd=all:ss=axioms:sgt=8_2866 on theBenchmark for (2866ds/11101Mi) % 152.82/22.25 % (3917468)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=2613005357:cond=on:i=13220:s2at=3:aac=none:fsd=on_2866 on theBenchmark for (2866ds/13220Mi) % 152.82/22.25 % Exception at run slice level % 152.82/22.25 User error: GNN currently only supports monomorphic FOL. % 152.82/22.25 % (3917471)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=3325815102:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2863 on theBenchmark for (2863ds/13528Mi) % 152.82/22.25 % Exception at run slice level % 152.82/22.25 User error: GNN currently only supports monomorphic FOL. % 152.82/22.25 % (3917446)Instruction limit reached! % 152.82/22.25 % (3917446)------------------------------ % 152.82/22.25 % (3917446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.82/22.25 % (3917446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.82/22.25 % (3917446)CaDiCaL version: 2.1.3 % 152.82/22.25 % (3917446)Termination reason: Instruction limit % 152.82/22.25 % (3917446)Termination phase: Saturation % 152.82/22.25 % (3917446)Time elapsed: 3.137 s % 152.82/22.25 % (3917446)Peak memory usage: 134 MB % 152.82/22.25 % (3917446)Instructions burned: 7145 (million) % 152.82/22.25 % (3917473)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=1374254310:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2860 on theBenchmark for (2860ds/14854Mi) % 152.82/22.25 % (3917474)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=1122261312:i=14974:ss=axioms:sgt=16_2859 on theBenchmark for (2859ds/14974Mi) % 152.82/22.25 % Exception at run slice level % 152.82/22.25 User error: GNN currently only supports monomorphic FOL. % 152.82/22.25 % (3917477)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=680490434:i=33081:aac=none:fgj=on:bd=all:fsr=off_2857 on theBenchmark for (2857ds/33081Mi) % 152.82/22.25 % Exception at run slice level % 152.82/22.25 User error: GNN currently only supports monomorphic FOL. % 152.82/22.25 % Exception at run slice level % 152.82/22.25 User error: GNN currently only supports monomorphic FOL. % 152.82/22.25 % (3917479)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=1283825379:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2854 on theBenchmark for (2854ds/50856Mi) % 152.82/22.25 % (3917480)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=3258543147:i=69865_2853 on theBenchmark for (2853ds/69865Mi) % 159.85/23.26 % Exception at run slice level % 159.85/23.26 User error: GNN currently only supports monomorphic FOL. % 159.85/23.26 % Exception at run slice level % 159.85/23.26 User error: GNN currently only supports monomorphic FOL. % 159.85/23.26 % (3917483)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=2320948139:cond=fast:i=17802:gtgl=3:gtg=all_2850 on theBenchmark for (2850ds/17802Mi) % 159.85/23.26 % (3917484)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=1878736411:i=96644_2849 on theBenchmark for (2849ds/96644Mi) % 159.85/23.26 % Exception at run slice level % 159.85/23.26 User error: GNN currently only supports monomorphic FOL. % 159.85/23.26 % (3917487)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 159.85/23.26 % (3917487)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=339493168:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2847 on theBenchmark for (2847ds/21161Mi) % 159.85/23.26 % (3917456)Instruction limit reached! % 159.85/23.26 % (3917456)------------------------------ % 159.85/23.26 % (3917456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.85/23.26 % (3917456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.85/23.26 % (3917456)CaDiCaL version: 2.1.3 % 159.85/23.26 % (3917456)Termination reason: Instruction limit % 159.85/23.26 % (3917456)Termination phase: Saturation % 159.85/23.26 % (3917456)Time elapsed: 3.994 s % 159.85/23.26 % (3917456)Peak memory usage: 94 MB % 159.85/23.26 % (3917456)Instructions burned: 8142 (million) % 159.85/23.26 % (3917489)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=378109755:i=22761:gtg=all:ss=axioms:fsd=on_2844 on theBenchmark for (2844ds/22761Mi) % 159.85/23.26 % Exception at run slice level % 159.85/23.26 User error: GNN currently only supports monomorphic FOL. % 159.85/23.26 % (3917491)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=2293403061:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2839 on theBenchmark for (2839ds/23713Mi) % 159.85/23.26 % (3917491)Refutation not found, incomplete strategy % 159.85/23.26 % (3917491)------------------------------ % 159.85/23.26 % (3917491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.85/23.26 % (3917491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.85/23.26 % (3917491)CaDiCaL version: 2.1.3 % 159.85/23.26 % (3917491)Termination reason: Refutation not found, incomplete strategy % 159.85/23.26 % (3917491)Time elapsed: 0.004 s % 159.85/23.26 % (3917491)Peak memory usage: 88 MB % 159.85/23.26 % (3917491)Instructions burned: 5 (million) % 159.85/23.26 % (3917491)------------------------------ % 159.85/23.26 % (3917491)------------------------------ % 159.85/23.26 % (3917493)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=1376961280:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2835 on theBenchmark for (2835ds/26509Mi) % 159.85/23.26 % Exception at run slice level % 159.85/23.26 User error: GNN currently only supports monomorphic FOL. % 159.85/23.26 % (3917495)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=2249215822:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2830 on theBenchmark for (2830ds/28957Mi) % 159.85/23.26 % (3917467)Instruction limit reached! % 159.85/23.26 % (3917467)------------------------------ % 159.85/23.26 % (3917467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.85/23.26 % (3917467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.85/23.26 % (3917467)CaDiCaL version: 2.1.3 % 159.85/23.26 % (3917467)Termination reason: Instruction limit % 159.85/23.26 % (3917467)Termination phase: Saturation % 159.85/23.26 % (3917467)Time elapsed: 3.866 s % 159.85/23.26 % (3917467)Peak memory usage: 93 MB % 159.85/23.26 % (3917467)Instructions burned: 11102 (million) % 159.85/23.26 % (3917497)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=447847571:i=29246:s2at=-1:kws=inv_arity:ins=10_2826 on theBenchmark for (2826ds/29246Mi) % 164.19/23.93 % Exception at run slice level % 164.19/23.93 User error: GNN currently only supports monomorphic FOL. % 164.19/23.93 % (3917499)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=3645875151:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2821 on theBenchmark for (2821ds/30082Mi) % 164.19/23.93 % (3917499)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 164.19/23.93 % Exception at run slice level % 164.19/23.93 User error: GNN currently only supports monomorphic FOL. % 164.19/23.93 % (3917501)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=3041140682:i=32262:bd=preordered_2816 on theBenchmark for (2816ds/32262Mi) % 164.19/23.93 % Exception at run slice level % 164.19/23.93 User error: GNN currently only supports monomorphic FOL. % 164.19/23.93 % (3917503)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=3605631052:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2811 on theBenchmark for (2811ds/32870Mi) % 164.19/23.93 % Exception at run slice level % 164.19/23.93 User error: GNN currently only supports monomorphic FOL. % 164.19/23.93 % (3917505)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=1667632577:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2805 on theBenchmark for (2805ds/33295Mi) % 164.19/23.93 % Exception at run slice level % 164.19/23.93 User error: GNN currently only supports monomorphic FOL. % 164.19/23.93 % (3917454)Instruction limit reached! % 164.19/23.93 % (3917454)------------------------------ % 164.19/23.93 % (3917454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.19/23.93 % (3917454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.19/23.93 % (3917454)CaDiCaL version: 2.1.3 % 164.19/23.93 % (3917454)Termination reason: Instruction limit % 164.19/23.93 % (3917454)Termination phase: Saturation % 164.19/23.93 % (3917454)Time elapsed: 8.540 s % 164.19/23.93 % (3917454)Peak memory usage: 158 MB % 164.19/23.93 % (3917454)Instructions burned: 15999 (million) % 164.19/23.93 % (3917507)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=1873429965:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2800 on theBenchmark for (2800ds/36826Mi) % 164.19/23.93 % (3917508)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=3634703943:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2799 on theBenchmark for (2799ds/92981Mi) % 164.19/23.93 % Exception at run slice level % 164.19/23.93 User error: GNN currently only supports monomorphic FOL. % 164.19/23.93 % (3917511)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=4118337024:s2pl=on:i=49423_2794 on theBenchmark for (2794ds/49423Mi) % 164.19/23.93 % Exception at run slice level % 164.19/23.93 User error: GNN currently only supports monomorphic FOL. % 164.19/23.93 % (3917487)Instruction limit reached! % 164.19/23.93 % (3917487)------------------------------ % 164.19/23.93 % (3917487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.19/23.93 % (3917487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.19/23.93 % (3917487)CaDiCaL version: 2.1.3 % 164.19/23.93 % (3917487)Termination reason: Instruction limit % 164.19/23.93 % (3917487)Termination phase: Saturation % 164.19/23.93 % (3917487)Time elapsed: 5.752 s % 164.19/23.93 % (3917487)Peak memory usage: 177 MB % 164.19/23.93 % (3917487)Instructions burned: 21165 (million) % 164.19/23.93 % (3917513)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=2679401003:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2789 on theBenchmark for (2789ds/57299Mi) % 164.19/23.93 % (3917514)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=525178504:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2788 on theBenchmark for (2788ds/127679Mi) % 164.19/23.93 % Exception at run slice level % 164.19/23.93 User error: GNN currently only supports monomorphic FOL. % 164.19/23.93 % Exception at run slice level % 164.19/23.93 User error: GNN currently only supports monomorphic FOL. % 170.34/24.87 % (3917517)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=3573001101:i=69402:add=on:aac=none:fsr=off_2785 on theBenchmark for (2785ds/69402Mi) % 170.34/24.87 % (3917322)Instruction limit reached! % 170.34/24.87 % (3917322)------------------------------ % 170.34/24.87 % (3917322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.34/24.87 % (3917322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.34/24.87 % (3917322)CaDiCaL version: 2.1.3 % 170.34/24.87 % (3917322)Termination reason: Instruction limit % 170.34/24.87 % (3917322)Termination phase: Saturation % 170.34/24.87 % (3917322)Time elapsed: 18.098 s % 170.34/24.87 % (3917322)Peak memory usage: 184 MB % 170.34/24.87 % (3917322)Instructions burned: 33336 (million) % 170.34/24.87 % (3917519)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=805611092:i=100512:doe=on:fgj=on:bd=all:fsd=on_2784 on theBenchmark for (2784ds/100512Mi) % 170.34/24.87 % Exception at run slice level % 170.34/24.87 User error: GNN currently only supports monomorphic FOL. % 170.34/24.87 % (3917520)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=2118644801:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2783 on theBenchmark for (2783ds/138761Mi) % 170.34/24.87 % (3917522)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=4196946273:i=282386:rtra=on_2782 on theBenchmark for (2782ds/282386Mi) % 170.34/24.87 % Exception at run slice level % 170.34/24.87 User error: GNN currently only supports monomorphic FOL. % 170.34/24.87 % Exception at run slice level % 170.34/24.87 User error: GNN currently only supports monomorphic FOL. % 170.34/24.87 % Exception at run slice level % 170.34/24.87 User error: GNN currently only supports monomorphic FOL. % 170.34/24.87 % (3917525)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=3588349284:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2779 on theBenchmark for (2779ds/269354Mi) % 170.34/24.87 % (3917526)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=115756592:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2778 on theBenchmark for (2778ds/283390Mi) % 170.34/24.87 % (3917526)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 170.34/24.87 % (3917527)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=2299499026:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2778 on theBenchmark for (2778ds/218Mi) % 170.34/24.87 % (3917527)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 170.34/24.87 % (3917527)Refutation not found, incomplete strategy % 170.34/24.87 % (3917527)------------------------------ % 170.34/24.87 % (3917527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.34/24.87 % (3917527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.34/24.87 % (3917527)CaDiCaL version: 2.1.3 % 170.34/24.87 % (3917527)Termination reason: Refutation not found, incomplete strategy % 170.34/24.87 % (3917527)Time elapsed: 0.002 s % 170.34/24.87 % (3917527)Peak memory usage: 88 MB % 170.34/24.87 % (3917527)Instructions burned: 2 (million) % 170.34/24.87 % Exception at run slice level % 170.34/24.87 User error: GNN currently only supports monomorphic FOL. % 170.34/24.87 % (3917531)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=1501934179:i=238:av=off:rtra=on:ss=axioms_2775 on theBenchmark for (2775ds/238Mi) % 170.34/24.87 % (3917527)------------------------------ % 170.34/24.87 % (3917527)------------------------------ % 170.34/24.87 % (3917531)Instruction limit reached! % 170.34/24.87 % (3917531)------------------------------ % 170.34/24.87 % (3917531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.34/24.87 % (3917531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.34/24.87 % (3917531)CaDiCaL version: 2.1.3 % 170.34/24.87 % (3917531)Termination reason: Instruction limit % 170.34/24.87 % (3917531)Termination phase: Saturation % 170.34/24.87 % (3917531)Time elapsed: 0.054 s % 177.39/25.74 % (3917531)Peak memory usage: 88 MB % 177.39/25.74 % (3917531)Instructions burned: 239 (million) % 177.39/25.74 % Exception at run slice level % 177.39/25.74 User error: GNN currently only supports monomorphic FOL. % 177.39/25.74 % (3917534)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=2921187001:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2774 on theBenchmark for (2774ds/258Mi) % 177.39/25.74 % (3917533)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=3812474929:s2a=on:i=278:rtra=on:gtg=position_2774 on theBenchmark for (2774ds/278Mi) % 177.39/25.74 % (3917534)Instruction limit reached! % 177.39/25.74 % (3917534)------------------------------ % 177.39/25.74 % (3917534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.39/25.74 % (3917534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.39/25.74 % (3917534)CaDiCaL version: 2.1.3 % 177.39/25.74 % (3917534)Termination reason: Instruction limit % 177.39/25.74 % (3917534)Termination phase: Saturation % 177.39/25.74 % (3917534)Time elapsed: 0.066 s % 177.39/25.74 % (3917534)Peak memory usage: 89 MB % 177.39/25.74 % (3917534)Instructions burned: 260 (million) % 177.39/25.74 % (3917535)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=2872096213:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2773 on theBenchmark for (2773ds/570Mi) % 177.39/25.74 % (3917533)Instruction limit reached! % 177.39/25.74 % (3917533)------------------------------ % 177.39/25.74 % (3917533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.39/25.74 % (3917533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.39/25.74 % (3917533)CaDiCaL version: 2.1.3 % 177.39/25.74 % (3917533)Termination reason: Instruction limit % 177.39/25.74 % (3917533)Termination phase: Saturation % 177.39/25.74 % (3917533)Time elapsed: 0.158 s % 177.39/25.74 % (3917533)Peak memory usage: 90 MB % 177.39/25.74 % (3917533)Instructions burned: 279 (million) % 177.39/25.74 % (3917538)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=1285442476:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2772 on theBenchmark for (2772ds/314Mi) % 177.39/25.74 % (3917538)Instruction limit reached! % 177.39/25.74 % (3917538)------------------------------ % 177.39/25.74 % (3917538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.39/25.74 % (3917538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.39/25.74 % (3917538)CaDiCaL version: 2.1.3 % 177.39/25.74 % (3917538)Termination reason: Instruction limit % 177.39/25.74 % (3917538)Termination phase: Saturation % 177.39/25.74 % (3917538)Time elapsed: 0.085 s % 177.39/25.74 % (3917538)Peak memory usage: 91 MB % 177.39/25.74 % (3917538)Instructions burned: 316 (million) % 177.39/25.74 % (3917540)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=1684108626:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2771 on theBenchmark for (2771ds/650Mi) % 177.39/25.74 % (3917542)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=241149358:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2770 on theBenchmark for (2770ds/496Mi) % 177.39/25.74 % (3917535)Instruction limit reached! % 177.39/25.74 % (3917535)------------------------------ % 177.39/25.74 % (3917535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.39/25.74 % (3917535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.39/25.74 % (3917535)CaDiCaL version: 2.1.3 % 177.39/25.74 % (3917535)Termination reason: Instruction limit % 177.39/25.74 % (3917535)Termination phase: Saturation % 177.39/25.74 % (3917535)Time elapsed: 0.316 s % 177.39/25.74 % (3917535)Peak memory usage: 90 MB % 177.39/25.74 % (3917535)Instructions burned: 570 (million) % 177.39/25.74 % (3917542)Instruction limit reached! % 177.39/25.74 % (3917542)------------------------------ % 177.39/25.74 % (3917542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.39/25.74 % (3917542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.39/25.74 % (3917542)CaDiCaL version: 2.1.3 % 177.39/25.74 % (3917542)Termination reason: Instruction limit % 177.39/25.74 % (3917542)Termination phase: Saturation % 177.39/25.74 % (3917542)Time elapsed: 0.150 s % 177.39/25.74 % (3917542)Peak memory usage: 92 MB % 177.39/25.74 % (3917542)Instructions burned: 498 (million) % 177.39/25.74 % (3917545)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=651892301:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2769 on theBenchmark for (2769ds/588Mi) % 177.39/25.74 % (3917545)Refutation not found, incomplete strategy % 177.39/25.74 % (3917545)------------------------------ % 177.39/25.74 % (3917545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.96/26.49 % (3917545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.96/26.49 % (3917545)CaDiCaL version: 2.1.3 % 181.96/26.49 % (3917545)Termination reason: Refutation not found, incomplete strategy % 181.96/26.49 % (3917545)Time elapsed: 0.006 s % 181.96/26.49 % (3917545)Peak memory usage: 89 MB % 181.96/26.49 % (3917545)Instructions burned: 8 (million) % 181.96/26.49 % (3917540)Instruction limit reached! % 181.96/26.49 % (3917540)------------------------------ % 181.96/26.49 % (3917540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.96/26.49 % (3917540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.96/26.49 % (3917540)CaDiCaL version: 2.1.3 % 181.96/26.49 % (3917540)Termination reason: Instruction limit % 181.96/26.49 % (3917540)Termination phase: Saturation % 181.96/26.49 % (3917540)Time elapsed: 0.337 s % 181.96/26.49 % (3917540)Peak memory usage: 94 MB % 181.96/26.49 % (3917540)Instructions burned: 652 (million) % 181.96/26.49 % (3917546)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=941852359:i=4700:rtra=on_2767 on theBenchmark for (2767ds/4700Mi) % 181.96/26.49 % (3917545)------------------------------ % 181.96/26.49 % (3917545)------------------------------ % 181.96/26.49 % (3917548)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1570457202:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2766 on theBenchmark for (2766ds/226Mi) % 181.96/26.49 % Exception at run slice level % 181.96/26.49 User error: GNN currently only supports monomorphic FOL. % 181.96/26.49 % (3917550)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3203980711:i=254:av=off:fsr=off:rtra=on:sup=off_2764 on theBenchmark for (2764ds/254Mi) % 181.96/26.49 % (3917550)Refutation not found, incomplete strategy % 181.96/26.49 % (3917550)------------------------------ % 181.96/26.49 % (3917550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.96/26.49 % (3917550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.96/26.49 % (3917550)CaDiCaL version: 2.1.3 % 181.96/26.49 % (3917550)Termination reason: Refutation not found, incomplete strategy % 181.96/26.49 % (3917550)Time elapsed: 0.005 s % 181.96/26.49 % (3917550)Peak memory usage: 88 MB % 181.96/26.49 % (3917550)Instructions burned: 7 (million) % 181.96/26.49 % (3917548)Instruction limit reached! % 181.96/26.49 % (3917548)------------------------------ % 181.96/26.49 % (3917548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.96/26.49 % (3917548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.96/26.49 % (3917548)CaDiCaL version: 2.1.3 % 181.96/26.49 % (3917548)Termination reason: Instruction limit % 181.96/26.49 % (3917548)Termination phase: Saturation % 181.96/26.49 % (3917548)Time elapsed: 0.142 s % 181.96/26.49 % (3917548)Peak memory usage: 92 MB % 181.96/26.49 % (3917548)Instructions burned: 226 (million) % 181.96/26.49 % (3917552)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=1767274370:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2764 on theBenchmark for (2764ds/228Mi) % 181.96/26.49 % (3917552)Refutation not found, incomplete strategy % 181.96/26.49 % (3917552)------------------------------ % 181.96/26.49 % (3917552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.96/26.49 % (3917552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.96/26.49 % (3917552)CaDiCaL version: 2.1.3 % 181.96/26.49 % (3917552)Termination reason: Refutation not found, incomplete strategy % 181.96/26.49 % (3917552)Time elapsed: 0.002 s % 181.96/26.49 % (3917552)Peak memory usage: 88 MB % 181.96/26.49 % (3917552)Instructions burned: 4 (million) % 181.96/26.49 % (3917554)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=1227812536:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2763 on theBenchmark for (2763ds/1814Mi) % 181.96/26.49 % (3917552)------------------------------ % 181.96/26.49 % (3917552)------------------------------ % 181.96/26.49 % (3917550)------------------------------ % 181.96/26.49 % (3917550)------------------------------ % 181.96/26.49 % (3917557)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=3652325894:i=874:sd=1:aac=none:rtra=on:ss=included_2761 on theBenchmark for (2761ds/874Mi) % 181.96/26.49 % (3917558)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=2610765867:i=10404:rtra=on:ss=axioms:sgt=16_2760 on theBenchmark for (2760ds/10404Mi) % 181.96/26.49 % (3917557)Instruction limit reached! % 181.96/26.49 % (3917557)------------------------------ % 188.14/27.27 % (3917557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.14/27.27 % (3917557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.14/27.27 % (3917557)CaDiCaL version: 2.1.3 % 188.14/27.27 % (3917557)Termination reason: Instruction limit % 188.14/27.27 % (3917557)Termination phase: Saturation % 188.14/27.27 % (3917557)Time elapsed: 0.237 s % 188.14/27.27 % (3917557)Peak memory usage: 94 MB % 188.14/27.27 % (3917557)Instructions burned: 876 (million) % 188.14/27.27 % (3917561)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2939120016:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2757 on theBenchmark for (2757ds/268Mi) % 188.14/27.27 % (3917561)Instruction limit reached! % 188.14/27.27 % (3917561)------------------------------ % 188.14/27.27 % (3917561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.14/27.27 % (3917561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.14/27.27 % (3917561)CaDiCaL version: 2.1.3 % 188.14/27.27 % (3917561)Termination reason: Instruction limit % 188.14/27.27 % (3917561)Termination phase: Saturation % 188.14/27.27 % (3917561)Time elapsed: 0.079 s % 188.14/27.27 % (3917561)Peak memory usage: 91 MB % 188.14/27.27 % (3917561)Instructions burned: 269 (million) % 188.14/27.27 % Exception at run slice level % 188.14/27.27 User error: GNN currently only supports monomorphic FOL. % 188.14/27.27 % (3917563)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=2659638341:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2755 on theBenchmark for (2755ds/1184Mi) % 188.14/27.27 % (3917563)Refutation not found, incomplete strategy % 188.14/27.27 % (3917563)------------------------------ % 188.14/27.27 % (3917563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.14/27.27 % (3917563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.14/27.27 % (3917563)CaDiCaL version: 2.1.3 % 188.14/27.27 % (3917563)Termination reason: Refutation not found, incomplete strategy % 188.14/27.27 % (3917563)Time elapsed: 0.002 s % 188.14/27.27 % (3917563)Peak memory usage: 88 MB % 188.14/27.27 % (3917563)Instructions burned: 6 (million) % 188.14/27.27 % (3917564)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=2227071693:st=3:i=26386:sd=3:rtra=on:ss=axioms_2755 on theBenchmark for (2755ds/26386Mi) % 188.14/27.27 % (3917563)------------------------------ % 188.14/27.27 % (3917563)------------------------------ % 188.14/27.27 % (3917567)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=2846284921:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2753 on theBenchmark for (2753ds/250Mi) % 188.14/27.27 % (3917567)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 188.14/27.27 % (3917567)Refutation not found, incomplete strategy % 188.14/27.27 % (3917567)------------------------------ % 188.14/27.27 % (3917567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.14/27.27 % (3917567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.14/27.27 % (3917567)CaDiCaL version: 2.1.3 % 188.14/27.27 % (3917567)Termination reason: Refutation not found, incomplete strategy % 188.14/27.27 % (3917567)Time elapsed: 0.001 s % 188.14/27.27 % (3917567)Peak memory usage: 88 MB % 188.14/27.27 % (3917567)Instructions burned: 3 (million) % 188.14/27.27 % (3917554)Instruction limit reached! % 188.14/27.27 % (3917554)------------------------------ % 188.14/27.27 % (3917554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.14/27.27 % (3917554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.14/27.27 % (3917554)CaDiCaL version: 2.1.3 % 188.14/27.27 % (3917554)Termination reason: Instruction limit % 188.14/27.27 % (3917554)Termination phase: Saturation % 188.14/27.27 % (3917554)Time elapsed: 1.001 s % 188.14/27.27 % (3917554)Peak memory usage: 93 MB % 188.14/27.27 % (3917554)Instructions burned: 1815 (million) % 188.14/27.27 % (3917567)------------------------------ % 188.14/27.27 % (3917567)------------------------------ % 188.14/27.27 % Exception at run slice level % 188.14/27.27 User error: GNN currently only supports monomorphic FOL. % 188.14/27.27 % (3917569)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=938423242:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2751 on theBenchmark for (2751ds/268Mi) % 188.14/27.27 % (3917570)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4052062374:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2750 on theBenchmark for (2750ds/282Mi) % 205.46/29.74 % (3917570)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 205.46/29.74 % (3917570)Refutation not found, incomplete strategy % 205.46/29.74 % (3917570)------------------------------ % 205.46/29.74 % (3917570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 205.46/29.74 % (3917570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.46/29.74 % (3917570)CaDiCaL version: 2.1.3 % 205.46/29.74 % (3917570)Termination reason: Refutation not found, incomplete strategy % 205.46/29.74 % (3917570)Time elapsed: 0.001 s % 205.46/29.74 % (3917570)Peak memory usage: 88 MB % 205.46/29.74 % (3917570)Instructions burned: 1 (million) % 205.46/29.74 % (3917571)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=748408874:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2750 on theBenchmark for (2750ds/862Mi) % 205.46/29.74 % (3917571)Refutation not found, incomplete strategy % 205.46/29.74 % (3917571)------------------------------ % 205.46/29.74 % (3917571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 205.46/29.74 % (3917571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.46/29.74 % (3917571)CaDiCaL version: 2.1.3 % 205.46/29.74 % (3917571)Termination reason: Refutation not found, incomplete strategy % 205.46/29.74 % (3917571)Time elapsed: 0.004 s % 205.46/29.74 % (3917571)Peak memory usage: 88 MB % 205.46/29.74 % (3917571)Instructions burned: 4 (million) % 205.46/29.74 % (3917569)Instruction limit reached! % 205.46/29.74 % (3917569)------------------------------ % 205.46/29.74 % (3917569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 205.46/29.74 % (3917569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.46/29.74 % (3917569)CaDiCaL version: 2.1.3 % 205.46/29.74 % (3917569)Termination reason: Instruction limit % 205.46/29.74 % (3917569)Termination phase: Saturation % 205.46/29.74 % (3917569)Time elapsed: 0.164 s % 205.46/29.74 % (3917569)Peak memory usage: 90 MB % 205.46/29.74 % (3917569)Instructions burned: 269 (million) % 205.46/29.74 % (3917570)------------------------------ % 205.46/29.74 % (3917570)------------------------------ % 205.46/29.74 % (3917575)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=649464492:i=12120:aac=none:ins=25:rtra=on_2748 on theBenchmark for (2748ds/12120Mi) % 205.46/29.74 % (3917576)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=4267932759:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2747 on theBenchmark for (2747ds/300Mi) % 205.46/29.74 % (3917576)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 205.46/29.74 % (3917571)------------------------------ % 205.46/29.74 % (3917571)------------------------------ % 205.46/29.74 % (3917576)Instruction limit reached! % 205.46/29.74 % (3917576)------------------------------ % 205.46/29.74 % (3917576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 205.46/29.74 % (3917576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.46/29.74 % (3917576)CaDiCaL version: 2.1.3 % 205.46/29.74 % (3917576)Termination reason: Instruction limit % 205.46/29.74 % (3917576)Termination phase: Saturation % 205.46/29.74 % (3917576)Time elapsed: 0.085 s % 205.46/29.74 % (3917576)Peak memory usage: 92 MB % 205.46/29.74 % (3917576)Instructions burned: 301 (million) % 205.46/29.74 % (3917579)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=264777918:i=28310:bd=all:rtra=on_2746 on theBenchmark for (2746ds/28310Mi) % 205.46/29.74 % (3917580)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2758650112:i=1334:av=off:fsr=off:rtra=on_2745 on theBenchmark for (2745ds/1334Mi) % 205.46/29.74 % Exception at run slice level % 205.46/29.74 User error: GNN currently only supports monomorphic FOL. % 205.46/29.74 % (3917580)Instruction limit reached! % 205.46/29.74 % (3917580)------------------------------ % 205.46/29.74 % (3917580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 205.46/29.74 % (3917580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.46/29.74 % (3917580)CaDiCaL version: 2.1.3 % 205.46/29.74 % (3917580)Termination reason: Instruction limit % 205.46/29.74 % (3917580)Termination phase: Saturation % 205.46/29.74 % (3917580)Time elapsed: 0.277 s % 217.90/31.43 % (3917580)Peak memory usage: 89 MB % 217.90/31.43 % (3917580)Instructions burned: 1339 (million) % 217.90/31.43 % (3917583)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=2798936321:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2743 on theBenchmark for (2743ds/370Mi) % 217.90/31.43 % Exception at run slice level % 217.90/31.43 User error: GNN currently only supports monomorphic FOL. % 217.90/31.43 % (3917584)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=3504158683:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2741 on theBenchmark for (2741ds/386Mi) % 217.90/31.43 % (3917584)Instruction limit reached! % 217.90/31.43 % (3917584)------------------------------ % 217.90/31.43 % (3917584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.90/31.43 % (3917584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.90/31.43 % (3917584)CaDiCaL version: 2.1.3 % 217.90/31.43 % (3917584)Termination reason: Instruction limit % 217.90/31.43 % (3917584)Termination phase: Saturation % 217.90/31.43 % (3917584)Time elapsed: 0.091 s % 217.90/31.43 % (3917584)Peak memory usage: 89 MB % 217.90/31.43 % (3917584)Instructions burned: 391 (million) % 217.90/31.43 % (3917586)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=3412869712:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2741 on theBenchmark for (2741ds/9700Mi) % 217.90/31.43 % (3917586)Refutation not found, incomplete strategy % 217.90/31.43 % (3917586)------------------------------ % 217.90/31.43 % (3917586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.90/31.43 % (3917586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.90/31.43 % (3917586)CaDiCaL version: 2.1.3 % 217.90/31.43 % (3917586)Termination reason: Refutation not found, incomplete strategy % 217.90/31.43 % (3917586)Time elapsed: 0.004 s % 217.90/31.43 % (3917586)Peak memory usage: 88 MB % 217.90/31.43 % (3917586)Instructions burned: 6 (million) % 217.90/31.43 % (3917583)Instruction limit reached! % 217.90/31.43 % (3917583)------------------------------ % 217.90/31.43 % (3917583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.90/31.43 % (3917583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.90/31.43 % (3917583)CaDiCaL version: 2.1.3 % 217.90/31.43 % (3917583)Termination reason: Instruction limit % 217.90/31.43 % (3917583)Termination phase: Saturation % 217.90/31.43 % (3917583)Time elapsed: 0.219 s % 217.90/31.43 % (3917583)Peak memory usage: 92 MB % 217.90/31.43 % (3917583)Instructions burned: 372 (million) % 217.90/31.43 % (3917588)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=4290218308:i=24222:sd=1:rtra=on:ss=included_2739 on theBenchmark for (2739ds/24222Mi) % 217.90/31.43 % (3917590)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=2054724174:i=638:kws=precedence:fsr=off:rtra=on_2739 on theBenchmark for (2739ds/638Mi) % 217.90/31.43 % (3917586)------------------------------ % 217.90/31.43 % (3917586)------------------------------ % 217.90/31.43 % Exception at run slice level % 217.90/31.43 User error: GNN currently only supports monomorphic FOL. % 217.90/31.43 % (3917593)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1785814576:i=4128:ep=RST:rtra=on_2737 on theBenchmark for (2737ds/4128Mi) % 217.90/31.43 % (3917593)Refutation not found, incomplete strategy % 217.90/31.43 % (3917593)------------------------------ % 217.90/31.43 % (3917593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.90/31.43 % (3917593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.90/31.43 % (3917593)CaDiCaL version: 2.1.3 % 217.90/31.43 % (3917593)Termination reason: Refutation not found, incomplete strategy % 217.90/31.43 % (3917593)Time elapsed: 0.005 s % 217.90/31.43 % (3917593)Peak memory usage: 88 MB % 217.90/31.43 % (3917593)Instructions burned: 7 (million) % 217.90/31.43 % (3917594)dis-1011_128_sil=32000:si=on:random_seed=1468911315:i=7412:ep=RST:av=off:rtra=on_2736 on theBenchmark for (2736ds/7412Mi) % 217.90/31.43 % (3917590)Instruction limit reached! % 217.90/31.43 % (3917590)------------------------------ % 217.90/31.43 % (3917590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.90/31.43 % (3917590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.90/31.43 % (3917590)CaDiCaL version: 2.1.3 % 217.90/31.43 % (3917590)Termination reason: Instruction limit % 235.49/33.96 % (3917590)Termination phase: Saturation % 235.49/33.96 % (3917590)Time elapsed: 0.357 s % 235.49/33.96 % (3917590)Peak memory usage: 92 MB % 235.49/33.96 % (3917590)Instructions burned: 640 (million) % 235.49/33.96 % (3917593)------------------------------ % 235.49/33.96 % (3917593)------------------------------ % 235.49/33.96 % (3917597)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=678117681:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2733 on theBenchmark for (2733ds/1514Mi) % 235.49/33.96 % (3917598)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=2547561715:i=27826:rtra=on:ss=axioms:sgt=8_2733 on theBenchmark for (2733ds/27826Mi) % 235.49/33.96 % Exception at run slice level % 235.49/33.96 User error: GNN currently only supports monomorphic FOL. % 235.49/33.96 % (3917601)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=542245987:i=19850:aac=none:rtra=on_2727 on theBenchmark for (2727ds/19850Mi) % 235.49/33.96 % (3917597)Instruction limit reached! % 235.49/33.96 % (3917597)------------------------------ % 235.49/33.96 % (3917597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.49/33.96 % (3917597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.49/33.96 % (3917597)CaDiCaL version: 2.1.3 % 235.49/33.96 % (3917597)Termination reason: Instruction limit % 235.49/33.96 % (3917597)Termination phase: Saturation % 235.49/33.96 % (3917597)Time elapsed: 0.822 s % 235.49/33.96 % (3917597)Peak memory usage: 106 MB % 235.49/33.96 % (3917597)Instructions burned: 1514 (million) % 235.49/33.96 % Exception at run slice level % 235.49/33.96 User error: GNN currently only supports monomorphic FOL. % 235.49/33.96 % (3917603)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1630490992:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2724 on theBenchmark for (2724ds/4958Mi) % 235.49/33.96 % (3917603)Refutation not found, incomplete strategy % 235.49/33.96 % (3917603)------------------------------ % 235.49/33.96 % (3917603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.49/33.96 % (3917603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.49/33.96 % (3917603)CaDiCaL version: 2.1.3 % 235.49/33.96 % (3917603)Termination reason: Refutation not found, incomplete strategy % 235.49/33.96 % (3917603)Time elapsed: 0.002 s % 235.49/33.96 % (3917603)Peak memory usage: 88 MB % 235.49/33.96 % (3917603)Instructions burned: 2 (million) % 235.49/33.96 % (3917604)ott+1002_64_sil=16000:si=on:sp=const_min:nwc=0.5:random_seed=3500725667:i=880:nm=2:av=off:rtra=on:gtg=exists_all:fdi=8:gsp=on_2722 on theBenchmark for (2722ds/880Mi) % 235.49/33.96 % (3917604)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 235.49/33.96 % (3917603)------------------------------ % 235.49/33.96 % (3917603)------------------------------ % 235.49/33.96 % (3917607)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=2748565560:st=1.5:i=22290:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2719 on theBenchmark for (2719ds/22290Mi) % 235.49/33.96 % (3917604)Instruction limit reached! % 235.49/33.96 % (3917604)------------------------------ % 235.49/33.96 % (3917604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.49/33.96 % (3917604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.49/33.96 % (3917604)CaDiCaL version: 2.1.3 % 235.49/33.96 % (3917604)Termination reason: Instruction limit % 235.49/33.96 % (3917604)Termination phase: Saturation % 235.49/33.96 % (3917604)Time elapsed: 0.482 s % 235.49/33.96 % (3917604)Peak memory usage: 91 MB % 235.49/33.96 % (3917604)Instructions burned: 881 (million) % 235.49/33.96 % Exception at run slice level % 235.49/33.96 User error: GNN currently only supports monomorphic FOL. % 235.49/33.96 % (3917609)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=3304970653:cts=off:i=6068:av=off:rtra=on:er=known:fsd=on_2716 on theBenchmark for (2716ds/6068Mi) % 235.49/33.96 % (3917610)lrs-1011_64:1_sil=8000:si=on:erd=off:urr=on:nwc=0.7:br=off:random_seed=3579276054:st=2:s2a=on:i=1048:s2at=2:rtra=on:ss=axioms_2714 on theBenchmark for (2714ds/1048Mi) % 235.49/33.96 % Exception at run slice level % 235.49/33.96 User error: GNN currently only supports monomorphic FOL. % 235.49/33.96 % (3917613)lrs+1011_16:1_sil=8000:si=on:acc=on:urr=on:fd=preordered:flr=on:random_seed=1024829266:avsq=on:i=2032:avsqr=676809,524288:sd=1:rtra=on:ss=axioms_2710 on theBenchmark for (2710ds/2032Mi) % 244.67/35.22 % (3917610)Instruction limit reached! % 244.67/35.22 % (3917610)------------------------------ % 244.67/35.22 % (3917610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.67/35.22 % (3917610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.67/35.22 % (3917610)CaDiCaL version: 2.1.3 % 244.67/35.22 % (3917610)Termination reason: Instruction limit % 244.67/35.22 % (3917610)Termination phase: Saturation % 244.67/35.22 % (3917610)Time elapsed: 0.547 s % 244.67/35.22 % (3917610)Peak memory usage: 94 MB % 244.67/35.22 % (3917610)Instructions burned: 1048 (million) % 244.67/35.22 % (3917495)Instruction limit reached! % 244.67/35.22 % (3917495)------------------------------ % 244.67/35.22 % (3917495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.67/35.22 % (3917495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.67/35.22 % (3917495)CaDiCaL version: 2.1.3 % 244.67/35.22 % (3917495)Termination reason: Instruction limit % 244.67/35.22 % (3917495)Termination phase: Saturation % 244.67/35.22 % (3917495)Time elapsed: 12.262 s % 244.67/35.22 % (3917495)Peak memory usage: 188 MB % 244.67/35.22 % (3917495)Instructions burned: 28962 (million) % 244.67/35.22 % (3917615)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:si=on:s2agt=16:random_seed=1051066883:i=28246:bd=preordered:ins=4:rtra=on_2707 on theBenchmark for (2707ds/28246Mi) % 244.67/35.22 % (3917616)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:si=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=164632395:i=11562:kws=precedence:bd=all:rtra=on:rawr=on_2706 on theBenchmark for (2706ds/11562Mi) % 244.67/35.22 % (3917594)Instruction limit reached! % 244.67/35.22 % (3917594)------------------------------ % 244.67/35.22 % (3917594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.67/35.22 % (3917594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.67/35.22 % (3917594)CaDiCaL version: 2.1.3 % 244.67/35.22 % (3917594)Termination reason: Instruction limit % 244.67/35.22 % (3917594)Termination phase: Saturation % 244.67/35.22 % (3917594)Time elapsed: 3.077 s % 244.67/35.22 % (3917594)Peak memory usage: 100 MB % 244.67/35.22 % (3917594)Instructions burned: 7413 (million) % 244.67/35.22 % (3917619)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=3000333840:i=4896:gtgl=5:bd=preordered:rtra=on:gtg=all_2704 on theBenchmark for (2704ds/4896Mi) % 244.67/35.22 % Exception at run slice level % 244.67/35.22 User error: GNN currently only supports monomorphic FOL. % 244.67/35.22 % (3917621)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:si=on:lcm=reverse:random_seed=2471607483:i=6446:kws=precedence:fgj=on:av=off:rtra=on_2702 on theBenchmark for (2702ds/6446Mi) % 244.67/35.22 % Exception at run slice level % 244.67/35.22 User error: GNN currently only supports monomorphic FOL. % 244.67/35.22 % (3917613)Instruction limit reached! % 244.67/35.22 % (3917613)------------------------------ % 244.67/35.22 % (3917613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.67/35.22 % (3917613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.67/35.22 % (3917613)CaDiCaL version: 2.1.3 % 244.67/35.22 % (3917613)Termination reason: Instruction limit % 244.67/35.22 % (3917613)Termination phase: Saturation % 244.67/35.22 % (3917613)Time elapsed: 1.035 s % 244.67/35.22 % (3917613)Peak memory usage: 99 MB % 244.67/35.22 % (3917613)Instructions burned: 2032 (million) % 244.67/35.22 % (3917623)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:si=on:sp=occurrence:sos=on:random_seed=3887848124:st=5.6:i=4066:sd=3:rtra=on:ss=axioms_2699 on theBenchmark for (2699ds/4066Mi) % 244.67/35.22 % (3917624)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:si=on:random_seed=166096017:i=4110:nm=16:rtra=on:gtg=position:ss=axioms:fsd=on_2698 on theBenchmark for (2698ds/4110Mi) % 244.67/35.22 % Exception at run slice level % 244.67/35.22 User error: GNN currently only supports monomorphic FOL. % 244.67/35.22 % (3917627)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:si=on:sp=const_frequency:spb=goal:acc=on:random_seed=1525611526:i=43222:sd=3:rtra=on:ss=axioms_2697 on theBenchmark for (2697ds/43222Mi) % 244.67/35.22 % Exception at run slice level % 244.67/35.22 User error: GNN currently only supports monomorphic FOL. % 244.67/35.22 % Exception at run slice level % 244.67/35.22 User error: GNN currently only supports monomorphic FOL. % 244.67/35.22 % (3917629)lrs+10_1_sil=8000:si=on:sp=occurrence:sos=all:lma=off:random_seed=1047895136:i=9670:sd=13:rtra=on:ss=axioms:sgt=23_2693 on theBenchmark for (2693ds/9670Mi) % 259.72/37.37 % (3917629)Refutation not found, incomplete strategy % 259.72/37.37 % (3917629)------------------------------ % 259.72/37.37 % (3917629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 259.72/37.37 % (3917629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.72/37.37 % (3917629)CaDiCaL version: 2.1.3 % 259.72/37.37 % (3917629)Termination reason: Refutation not found, incomplete strategy % 259.72/37.37 % (3917629)Time elapsed: 0.002 s % 259.72/37.37 % (3917629)Peak memory usage: 88 MB % 259.72/37.37 % (3917629)Instructions burned: 1 (million) % 259.72/37.37 % (3917630)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:si=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=976479652:st=5:i=1594:s2at=3:sd=4:bs=unit_only:av=off:rtra=on:sup=off:ss=included_2693 on theBenchmark for (2693ds/1594Mi) % 259.72/37.37 % Exception at run slice level % 259.72/37.37 User error: GNN currently only supports monomorphic FOL. % 259.72/37.37 % (3917633)lrs-1011_5_sil=8000:si=on:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2317159581:i=4652:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:rtra=on:fsd=on_2691 on theBenchmark for (2691ds/4652Mi) % 259.72/37.37 % (3917629)------------------------------ % 259.72/37.37 % (3917629)------------------------------ % 259.72/37.37 % (3917635)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:si=on:sos=all:urr=on:br=off:random_seed=2762395881:i=12076:nm=6:rtra=on_2689 on theBenchmark for (2689ds/12076Mi) % 259.72/37.37 % Exception at run slice level % 259.72/37.37 User error: GNN currently only supports monomorphic FOL. % 259.72/37.37 % (3917637)lrs+10_1_sil=32000:si=on:sp=occurrence:random_seed=2272098561:st=2:i=66668:sd=3:rtra=on:ss=included:sgt=32_2684 on theBenchmark for (2684ds/66668Mi) % 259.72/37.37 % (3917630)Instruction limit reached! % 259.72/37.37 % (3917630)------------------------------ % 259.72/37.37 % (3917630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 259.72/37.37 % (3917630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.72/37.37 % (3917630)CaDiCaL version: 2.1.3 % 259.72/37.37 % (3917630)Termination reason: Instruction limit % 259.72/37.37 % (3917630)Termination phase: Saturation % 259.72/37.37 % (3917630)Time elapsed: 1.059 s % 259.72/37.37 % (3917630)Peak memory usage: 98 MB % 259.72/37.37 % (3917630)Instructions burned: 1594 (million) % 259.72/37.37 % (3917639)lrs+10_4_sil=8000:plsq=on:si=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2030628042:st=3.7:s2a=on:i=2016:s2at=1.2:sd=3:bd=all:av=off:rtra=on:fdi=8:sup=off:ss=axioms_2681 on theBenchmark for (2681ds/2016Mi) % 259.72/37.37 % (3917616)Instruction limit reached! % 259.72/37.37 % (3917616)------------------------------ % 259.72/37.37 % (3917616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 259.72/37.37 % (3917616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.72/37.37 % (3917616)CaDiCaL version: 2.1.3 % 259.72/37.37 % (3917616)Termination reason: Instruction limit % 259.72/37.37 % (3917616)Termination phase: Saturation % 259.72/37.37 % (3917616)Time elapsed: 3.429 s % 259.72/37.37 % (3917616)Peak memory usage: 118 MB % 259.72/37.37 % (3917616)Instructions burned: 11564 (million) % 259.72/37.37 % (3917641)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:si=on:sp=const_frequency:spb=intro:gs=on:random_seed=3541416515:i=16654:s2at=5:bd=preordered:rtra=on_2670 on theBenchmark for (2670ds/16654Mi) % 259.72/37.37 % (3917639)Instruction limit reached! % 259.72/37.37 % (3917639)------------------------------ % 259.72/37.37 % (3917639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 259.72/37.37 % (3917639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.72/37.37 % (3917639)CaDiCaL version: 2.1.3 % 259.72/37.37 % (3917639)Termination reason: Instruction limit % 259.72/37.37 % (3917639)Termination phase: Saturation % 259.72/37.37 % (3917639)Time elapsed: 1.118 s % 259.72/37.37 % (3917639)Peak memory usage: 114 MB % 259.72/37.37 % (3917639)Instructions burned: 2016 (million) % 259.72/37.37 % Exception at run slice level % 259.72/37.37 User error: GNN currently only supports monomorphic FOL. % 259.72/37.37 % (3917643)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:si=on:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=1638053342:s2a=on:i=2166:s2at=1.87328:slsql=off:ep=RSTC:rtra=on:fdi=16_2668 on theBenchmark for (2668ds/2166Mi) % 271.10/39.02 % (3917644)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:si=on:spb=goal:fd=preordered:random_seed=2165852292:i=2168:sd=1:bd=preordered:av=off:fsr=off:rtra=on:ss=axioms:sgt=14_2667 on theBenchmark for (2667ds/2168Mi) % 271.10/39.02 % (3917633)Instruction limit reached! % 271.10/39.02 % (3917633)------------------------------ % 271.10/39.02 % (3917633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.10/39.02 % (3917633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.10/39.02 % (3917633)CaDiCaL version: 2.1.3 % 271.10/39.02 % (3917633)Termination reason: Instruction limit % 271.10/39.02 % (3917633)Termination phase: Saturation % 271.10/39.02 % (3917633)Time elapsed: 2.482 s % 271.10/39.02 % (3917633)Peak memory usage: 96 MB % 271.10/39.02 % (3917633)Instructions burned: 4654 (million) % 271.10/39.02 % (3917647)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:si=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1993899718:i=13990:s2at=5:rtra=on:gtg=all_2665 on theBenchmark for (2665ds/13990Mi) % 271.10/39.02 % Exception at run slice level % 271.10/39.02 User error: GNN currently only supports monomorphic FOL. % 271.10/39.02 % (3917644)Instruction limit reached! % 271.10/39.02 % (3917644)------------------------------ % 271.10/39.02 % (3917644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.10/39.02 % (3917644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.10/39.02 % (3917644)CaDiCaL version: 2.1.3 % 271.10/39.02 % (3917644)Termination reason: Instruction limit % 271.10/39.02 % (3917644)Termination phase: Saturation % 271.10/39.02 % (3917644)Time elapsed: 0.653 s % 271.10/39.02 % (3917644)Peak memory usage: 98 MB % 271.10/39.02 % (3917644)Instructions burned: 2169 (million) % 271.10/39.02 % (3917649)lrs+10_1_sil=32000:si=on:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2942718566:st=2:i=12450:sd=15:rtra=on:ss=axioms_2660 on theBenchmark for (2660ds/12450Mi) % 271.10/39.02 % (3917649)Refutation not found, incomplete strategy % 271.10/39.02 % (3917649)------------------------------ % 271.10/39.02 % (3917649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.10/39.02 % (3917649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.10/39.02 % (3917649)CaDiCaL version: 2.1.3 % 271.10/39.02 % (3917649)Termination reason: Refutation not found, incomplete strategy % 271.10/39.02 % (3917649)Time elapsed: 0.005 s % 271.10/39.02 % (3917649)Peak memory usage: 89 MB % 271.10/39.02 % (3917649)Instructions burned: 7 (million) % 271.10/39.02 % (3917650)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:si=on:lcm=reverse:random_seed=792739208:cond=fast:i=6744:sd=1:nm=16:rtra=on:gtg=position:ss=axioms_2659 on theBenchmark for (2659ds/6744Mi) % 271.10/39.02 % Exception at run slice level % 271.10/39.02 User error: GNN currently only supports monomorphic FOL. % 271.10/39.02 % (3917643)Instruction limit reached! % 271.10/39.02 % (3917643)------------------------------ % 271.10/39.02 % (3917643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.10/39.02 % (3917643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.10/39.02 % (3917643)CaDiCaL version: 2.1.3 % 271.10/39.02 % (3917643)Termination reason: Instruction limit % 271.10/39.02 % (3917643)Termination phase: Saturation % 271.10/39.02 % (3917643)Time elapsed: 1.084 s % 271.10/39.02 % (3917643)Peak memory usage: 99 MB % 271.10/39.02 % (3917643)Instructions burned: 2167 (million) % 271.10/39.02 % (3917649)------------------------------ % 271.10/39.02 % (3917649)------------------------------ % 271.10/39.02 % (3917653)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sos=all:random_seed=612619666:st=2.3:i=52914:sd=10:rtra=on:ss=included:sgt=8_2656 on theBenchmark for (2656ds/52914Mi) % 271.10/39.02 % (3917654)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:si=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=3988023233:i=26988:s2at=1.31:bd=all:ins=10:rtra=on:gtg=exists_top_2656 on theBenchmark for (2656ds/26988Mi) % 271.10/39.02 % (3917655)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:si=on:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=3723108870:i=5006:nm=4:rtra=on:gsp=on:ss=axioms:sgt=15_2656 on theBenchmark for (2656ds/5006Mi) % 271.10/39.02 % (3917655)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 283.01/40.73 % Exception at run slice level % 283.01/40.73 User error: GNN currently only supports monomorphic FOL. % 283.01/40.73 % (3917659)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:si=on:sos=on:lsd=10:random_seed=86180456:i=5118:sd=1:ep=RSTC:rtra=on:ss=axioms_2653 on theBenchmark for (2653ds/5118Mi) % 283.01/40.73 % Exception at run slice level % 283.01/40.73 User error: GNN currently only supports monomorphic FOL. % 283.01/40.73 % Exception at run slice level % 283.01/40.73 User error: GNN currently only supports monomorphic FOL. % 283.01/40.73 % Exception at run slice level % 283.01/40.73 User error: GNN currently only supports monomorphic FOL. % 283.01/40.73 % (3917661)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:si=on:fdtod=off:random_seed=2466865983:i=61506:av=off:rtra=on:ss=included_2651 on theBenchmark for (2651ds/61506Mi) % 283.01/40.73 % (3917662)lrs+10_1024_sil=64000:plsq=on:plsqc=4:si=on:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3510882837:i=52946:ep=RSTC:rtra=on_2650 on theBenchmark for (2650ds/52946Mi) % 283.01/40.73 % (3917663)dis-1011_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:tgt=ground:npcc=on:si=on:sp=arity:sos=on:erd=off:rp=on:gs=on:kmz=on:random_seed=285910336:cts=off:i=5518:kws=inv_arity:fgj=on:rtra=on_2650 on theBenchmark for (2650ds/5518Mi) % 283.01/40.73 % Exception at run slice level % 283.01/40.73 User error: GNN currently only supports monomorphic FOL. % 283.01/40.73 % Exception at run slice level % 283.01/40.73 User error: GNN currently only supports monomorphic FOL. % 283.01/40.73 % (3917667)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:si=on:sp=weighted_frequency:sos=all:spb=goal_then_units:urr=ec_only:sac=on:random_seed=2509794220:st=1.2:i=11330:sd=2:ep=RSTC:rtra=on:gsp=on:ss=axioms_2646 on theBenchmark for (2646ds/11330Mi) % 283.01/40.73 % (3917667)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 283.01/40.73 % (3917668)dis+1011_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:npcc=on:si=on:sos=on:lsd=20:urr=full:alpa=true:sac=on:random_seed=3516917687:i=3064:ep=RS:rtra=on:ss=axioms_2646 on theBenchmark for (2646ds/3064Mi) % 283.01/40.73 % Exception at run slice level % 283.01/40.73 User error: GNN currently only supports monomorphic FOL. % 283.01/40.73 % (3917671)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=2239389394:i=3130:sd=2:rtra=on:ss=axioms:sgt=32_2643 on theBenchmark for (2643ds/3130Mi) % 283.01/40.73 % Exception at run slice level % 283.01/40.73 User error: GNN currently only supports monomorphic FOL. % 283.01/40.73 % Exception at run slice level % 283.01/40.73 User error: GNN currently only supports monomorphic FOL. % 283.01/40.73 % (3917673)lrs-1011_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:sims=off:bsd=on:si=on:sp=unary_first:erd=off:spb=goal:lcm=reverse:gs=on:s2agt=8:random_seed=3551533785:i=3144:fgj=on:rtra=on:gsp=on_2640 on theBenchmark for (2640ds/3144Mi) % 283.01/40.73 % (3917673)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 283.01/40.73 % (3917674)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:si=on:sp=occurrence:sos=on:newcnf=on:random_seed=2203082966:i=12104:sd=4:rtra=on:ss=axioms:sgt=24_2640 on theBenchmark for (2640ds/12104Mi) % 283.01/40.73 % Exception at run slice level % 283.01/40.73 User error: GNN currently only supports monomorphic FOL. % 283.01/40.73 % (3917677)lrs+21_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:si=on:sp=arity:sos=on:erd=off:lcm=predicate:alpa=false:sac=on:random_seed=2019023999:i=7000:sd=1:bd=preordered:rtra=on:sup=off:ss=included_2637 on theBenchmark for (2637ds/7000Mi) % 283.01/40.73 % Exception at run slice level % 283.01/40.73 User error: GNN currently only supports monomorphic FOL. % 283.01/40.73 % Exception at run slice level % 283.01/40.73 User error: GNN currently only supports monomorphic FOL. % 283.01/40.73 % (3917679)lrs+35_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:npcc=on:fde=none:si=on:sp=weighted_frequency:erd=off:spb=non_intro:updr=off:newcnf=on:random_seed=1749868465:i=3684:sd=3:fgj=on:rtra=on:gtg=position:gsp=on:ss=axioms:sgt=20_2635 on theBenchmark for (2635ds/3684Mi) % 283.01/40.73 % (3917679)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 283.01/40.73 % (3917680)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:si=on:bsr=unit_only:random_seed=379673199Terminated %------------------------------------------------------------------------------