%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV669_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:19:14 PM UTC 2026 % Result : Timeout 291.26s 42.04s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV669_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.06/0.18 % Computer : n003.cluster.edu % 0.06/0.18 % Model : x86_64 x86_64 % 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.18 % Memory : 8046.5625MB % 0.06/0.18 % OS : Linux 6.8.0-71-generic % 0.06/0.18 % CPULimit : 300 % 0.06/0.18 % WCLimit : 300 % 0.06/0.18 % DateTime : Mon Sep 28 12:14:12 UTC 2026 % 0.06/0.18 % CPUTime : % 0.06/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.06/0.22 Running first-order theorem proving % 0.06/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 10.50/2.14 % (1546558)Detected formulas, will run a generic FOF schedule. % 10.50/2.14 % (1546580)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=1067323024:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 10.50/2.14 % (1546585)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2416168866:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 10.50/2.14 % (1546584)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=965958791:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 10.50/2.14 % (1546581)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=682348836:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 10.50/2.14 % (1546583)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3197728055:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 10.50/2.14 % (1546583)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.50/2.14 % (1546582)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=3431278154:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 10.50/2.14 % (1546582)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.50/2.14 % (1546586)dis-21_1_sil=8000:lcm=predicate:random_seed=738164596:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 10.50/2.14 % (1546585)Instruction limit reached! % 10.50/2.14 % (1546585)------------------------------ % 10.50/2.14 % (1546585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.50/2.14 % (1546585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.50/2.14 % (1546585)CaDiCaL version: 2.1.3 % 10.50/2.14 % (1546585)Termination reason: Instruction limit % 10.50/2.14 % (1546585)Termination phase: Saturation % 10.50/2.14 % (1546585)Time elapsed: 0.122 s % 10.50/2.14 % (1546585)Peak memory usage: 90 MB % 10.50/2.14 % (1546585)Instructions burned: 140 (million) % 10.50/2.14 % (1546584)Instruction limit reached! % 10.50/2.14 % (1546584)------------------------------ % 10.50/2.14 % (1546584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.50/2.14 % (1546584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.50/2.14 % (1546584)CaDiCaL version: 2.1.3 % 10.50/2.14 % (1546584)Termination reason: Instruction limit % 10.50/2.14 % (1546584)Termination phase: Saturation % 10.50/2.14 % (1546584)Time elapsed: 0.089 s % 10.50/2.14 % (1546584)Peak memory usage: 88 MB % 10.50/2.14 % (1546584)Instructions burned: 119 (million) % 10.50/2.14 % (1546583)Instruction limit reached! % 10.50/2.14 % (1546583)------------------------------ % 10.50/2.14 % (1546583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.50/2.14 % (1546583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.50/2.14 % (1546583)CaDiCaL version: 2.1.3 % 10.50/2.14 % (1546583)Termination reason: Instruction limit % 10.50/2.14 % (1546583)Termination phase: Saturation % 10.50/2.14 % (1546583)Time elapsed: 0.099 s % 10.50/2.14 % (1546583)Peak memory usage: 89 MB % 10.50/2.14 % (1546583)Instructions burned: 113 (million) % 10.50/2.14 % (1546586)Instruction limit reached! % 10.50/2.14 % (1546586)------------------------------ % 10.50/2.14 % (1546586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.50/2.14 % (1546586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.50/2.14 % (1546586)CaDiCaL version: 2.1.3 % 10.50/2.14 % (1546586)Termination reason: Instruction limit % 10.50/2.14 % (1546586)Termination phase: Saturation % 10.50/2.14 % (1546586)Time elapsed: 0.114 s % 10.50/2.14 % (1546586)Peak memory usage: 89 MB % 10.50/2.14 % (1546586)Instructions burned: 130 (million) % 10.50/2.14 % Exception at run slice level % 10.50/2.14 User error: GNN currently only supports monomorphic FOL. % 10.50/2.14 % (1546599)lrs+10_1_sil=32000:urr=on:br=off:random_seed=845791543:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi) % 10.50/2.14 % (1546598)lrs+10_1_sil=8000:sp=occurrence:random_seed=1254477512:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi) % 10.50/2.14 % (1546605)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=73125367:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi) % 11.08/2.32 % (1546603)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2246556375:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi) % 11.08/2.32 % (1546606)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3104448755:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 11.08/2.32 % (1546606)Refutation not found, incomplete strategy % 11.08/2.32 % (1546606)------------------------------ % 11.08/2.32 % (1546606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.08/2.32 % (1546606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.08/2.32 % (1546606)CaDiCaL version: 2.1.3 % 11.08/2.32 % (1546606)Termination reason: Refutation not found, incomplete strategy % 11.08/2.32 % (1546606)Time elapsed: 0.008 s % 11.08/2.32 % (1546606)Peak memory usage: 89 MB % 11.08/2.32 % (1546606)Instructions burned: 15 (million) % 11.08/2.32 % (1546599)Instruction limit reached! % 11.08/2.32 % (1546599)------------------------------ % 11.08/2.32 % (1546599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.08/2.32 % (1546599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.08/2.32 % (1546599)CaDiCaL version: 2.1.3 % 11.08/2.32 % (1546599)Termination reason: Instruction limit % 11.08/2.32 % (1546599)Termination phase: Saturation % 11.08/2.32 % (1546599)Time elapsed: 0.136 s % 11.08/2.32 % (1546599)Peak memory usage: 90 MB % 11.08/2.32 % (1546599)Instructions burned: 158 (million) % 11.08/2.32 % (1546605)Instruction limit reached! % 11.08/2.32 % (1546605)------------------------------ % 11.08/2.32 % (1546605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.08/2.32 % (1546605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.08/2.32 % (1546605)CaDiCaL version: 2.1.3 % 11.08/2.32 % (1546605)Termination reason: Instruction limit % 11.08/2.32 % (1546605)Termination phase: Saturation % 11.08/2.32 % (1546605)Time elapsed: 0.207 s % 11.08/2.32 % (1546605)Peak memory usage: 90 MB % 11.08/2.32 % (1546605)Instructions burned: 248 (million) % 11.08/2.32 % (1546598)Instruction limit reached! % 11.08/2.32 % (1546598)------------------------------ % 11.08/2.32 % (1546598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.08/2.32 % (1546598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.08/2.32 % (1546598)CaDiCaL version: 2.1.3 % 11.08/2.32 % (1546598)Termination reason: Instruction limit % 11.08/2.32 % (1546598)Termination phase: Saturation % 11.08/2.32 % (1546598)Time elapsed: 0.228 s % 11.08/2.32 % (1546598)Peak memory usage: 90 MB % 11.08/2.32 % (1546598)Instructions burned: 285 (million) % 11.08/2.32 % Exception at run slice level % 11.08/2.32 User error: GNN currently only supports monomorphic FOL. % 11.08/2.32 % (1546606)------------------------------ % 11.08/2.32 % (1546606)------------------------------ % 11.08/2.32 % Exception at run slice level % 11.08/2.32 User error: GNN currently only supports monomorphic FOL. % 11.08/2.32 % (1546603)Instruction limit reached! % 11.08/2.32 % (1546603)------------------------------ % 11.08/2.32 % (1546603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.08/2.32 % (1546603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.08/2.32 % (1546603)CaDiCaL version: 2.1.3 % 11.08/2.32 % (1546603)Termination reason: Instruction limit % 11.08/2.32 % (1546603)Termination phase: Saturation % 11.08/2.32 % (1546603)Time elapsed: 0.307 s % 11.08/2.32 % (1546603)Peak memory usage: 91 MB % 11.08/2.32 % (1546603)Instructions burned: 326 (million) % 11.08/2.32 % (1546616)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4235929980:i=2350_2993 on theBenchmark for (2993ds/2350Mi) % 11.08/2.32 % (1546618)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3207356656:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi) % 11.08/2.32 % (1546619)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=21516136:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi) % 11.08/2.32 % (1546619)Refutation not found, incomplete strategy % 11.08/2.32 % (1546619)------------------------------ % 11.08/2.32 % (1546619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.08/2.32 % (1546619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.08/2.32 % (1546619)CaDiCaL version: 2.1.3 % 12.31/2.66 % (1546619)Termination reason: Refutation not found, incomplete strategy % 12.31/2.66 % (1546619)Time elapsed: 0.011 s % 12.31/2.66 % (1546619)Peak memory usage: 88 MB % 12.31/2.66 % (1546619)Instructions burned: 15 (million) % 12.31/2.66 % (1546621)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3156138987:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi) % 12.31/2.66 % (1546623)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=506655294:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi) % 12.31/2.66 % (1546623)Refutation not found, incomplete strategy % 12.31/2.66 % (1546623)------------------------------ % 12.31/2.66 % (1546623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.31/2.66 % (1546623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.31/2.66 % (1546623)CaDiCaL version: 2.1.3 % 12.31/2.66 % (1546623)Termination reason: Refutation not found, incomplete strategy % 12.31/2.66 % (1546623)Time elapsed: 0.008 s % 12.31/2.66 % (1546623)Peak memory usage: 88 MB % 12.31/2.66 % (1546623)Instructions burned: 17 (million) % 12.31/2.66 % (1546626)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4285271328:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi) % 12.31/2.66 % (1546622)lrs+10_1_sil=8000:sp=occurrence:random_seed=1773983853:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi) % 12.31/2.66 % (1546618)Instruction limit reached! % 12.31/2.66 % (1546618)------------------------------ % 12.31/2.66 % (1546618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.31/2.66 % (1546618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.31/2.66 % (1546618)CaDiCaL version: 2.1.3 % 12.31/2.66 % (1546618)Termination reason: Instruction limit % 12.31/2.66 % (1546618)Termination phase: Saturation % 12.31/2.66 % (1546618)Time elapsed: 0.103 s % 12.31/2.66 % (1546618)Peak memory usage: 89 MB % 12.31/2.66 % (1546618)Instructions burned: 114 (million) % 12.31/2.66 % (1546621)Instruction limit reached! % 12.31/2.66 % (1546621)------------------------------ % 12.31/2.66 % (1546621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.31/2.66 % (1546621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.31/2.66 % (1546621)CaDiCaL version: 2.1.3 % 12.31/2.66 % (1546621)Termination reason: Instruction limit % 12.31/2.66 % (1546621)Termination phase: Saturation % 12.31/2.66 % (1546621)Time elapsed: 0.104 s % 12.31/2.66 % (1546621)Peak memory usage: 89 MB % 12.31/2.66 % (1546621)Instructions burned: 115 (million) % 12.31/2.66 % (1546623)------------------------------ % 12.31/2.66 % (1546623)------------------------------ % 12.31/2.66 % (1546637)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=242035442:st=8:i=592:sd=3:ep=RST:ss=axioms_2989 on theBenchmark for (2989ds/592Mi) % 12.31/2.66 % (1546636)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3348316025:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi) % 12.31/2.66 % (1546619)------------------------------ % 12.31/2.66 % (1546619)------------------------------ % 12.31/2.66 % (1546636)Instruction limit reached! % 12.31/2.66 % (1546636)------------------------------ % 12.31/2.66 % (1546636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.31/2.66 % (1546636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.31/2.66 % (1546636)CaDiCaL version: 2.1.3 % 12.31/2.66 % (1546636)Termination reason: Instruction limit % 12.31/2.66 % (1546636)Termination phase: Saturation % 12.31/2.66 % (1546636)Time elapsed: 0.077 s % 12.31/2.66 % (1546636)Peak memory usage: 90 MB % 12.31/2.66 % (1546636)Instructions burned: 135 (million) % 12.31/2.66 % (1546640)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4265573766:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi) % 12.31/2.66 % Exception at run slice level % 12.31/2.66 User error: GNN currently only supports monomorphic FOL. % 12.31/2.66 % (1546643)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=3126096121:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/125Mi) % 12.31/2.66 % Exception at run slice level % 12.31/2.66 User error: GNN currently only supports monomorphic FOL. % 12.31/2.66 % (1546643)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 12.31/2.66 % (1546644)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3784449624:i=134:gtgl=5:slsql=off:gtg=exists_sym_2986 on theBenchmark for (2986ds/134Mi) % 17.60/3.18 % Exception at run slice level % 17.60/3.18 User error: Immediate (shared) subterms of term/literal aa(X2,X0,combb(X1,X0,X2,X5,X4),X3) = sF24(X2,X0,X1,X5,X4,X3) have different types/not well-typed! % 17.60/3.18 % (1546646)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1915646558:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/141Mi) % 17.60/3.18 % (1546646)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 17.60/3.18 % (1546646)Refutation not found, incomplete strategy % 17.60/3.18 % (1546646)------------------------------ % 17.60/3.18 % (1546646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.60/3.18 % (1546646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.60/3.18 % (1546646)CaDiCaL version: 2.1.3 % 17.60/3.18 % (1546646)Termination reason: Refutation not found, incomplete strategy % 17.60/3.18 % (1546646)Time elapsed: 0.002 s % 17.60/3.18 % (1546646)Peak memory usage: 88 MB % 17.60/3.18 % (1546646)Instructions burned: 4 (million) % 17.60/3.18 % (1546643)Instruction limit reached! % 17.60/3.18 % (1546643)------------------------------ % 17.60/3.18 % (1546643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.60/3.18 % (1546643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.60/3.18 % (1546643)CaDiCaL version: 2.1.3 % 17.60/3.18 % (1546643)Termination reason: Instruction limit % 17.60/3.18 % (1546643)Termination phase: Saturation % 17.60/3.18 % (1546643)Time elapsed: 0.071 s % 17.60/3.18 % (1546643)Peak memory usage: 90 MB % 17.60/3.18 % (1546643)Instructions burned: 125 (million) % 17.60/3.18 % (1546637)Instruction limit reached! % 17.60/3.18 % (1546637)------------------------------ % 17.60/3.18 % (1546637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.60/3.18 % (1546637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.60/3.18 % (1546637)CaDiCaL version: 2.1.3 % 17.60/3.18 % (1546637)Termination reason: Instruction limit % 17.60/3.18 % (1546637)Termination phase: Saturation % 17.60/3.18 % (1546637)Time elapsed: 0.272 s % 17.60/3.18 % (1546637)Peak memory usage: 89 MB % 17.60/3.18 % (1546637)Instructions burned: 594 (million) % 17.60/3.18 % (1546648)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2085314973:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2985 on theBenchmark for (2985ds/431Mi) % 17.60/3.18 % (1546648)Refutation not found, incomplete strategy % 17.60/3.18 % (1546648)------------------------------ % 17.60/3.18 % (1546648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.60/3.18 % (1546648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.60/3.18 % (1546648)CaDiCaL version: 2.1.3 % 17.60/3.18 % (1546648)Termination reason: Refutation not found, incomplete strategy % 17.60/3.18 % (1546648)Time elapsed: 0.008 s % 17.60/3.18 % (1546648)Peak memory usage: 89 MB % 17.60/3.18 % (1546648)Instructions burned: 13 (million) % 17.60/3.18 % (1546651)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=3540550088:i=6060:aac=none:ins=25_2985 on theBenchmark for (2985ds/6060Mi) % 17.60/3.18 % (1546622)Instruction limit reached! % 17.60/3.18 % (1546622)------------------------------ % 17.60/3.18 % (1546622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.60/3.18 % (1546622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.60/3.18 % (1546622)CaDiCaL version: 2.1.3 % 17.60/3.18 % (1546622)Termination reason: Instruction limit % 17.60/3.18 % (1546622)Termination phase: Saturation % 17.60/3.18 % (1546622)Time elapsed: 0.608 s % 17.60/3.18 % (1546622)Peak memory usage: 98 MB % 17.60/3.18 % (1546622)Instructions burned: 908 (million) % 17.60/3.18 % (1546653)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=3735516055:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2984 on theBenchmark for (2984ds/150Mi) % 17.60/3.18 % (1546646)------------------------------ % 17.60/3.18 % (1546646)------------------------------ % 17.60/3.18 % (1546653)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 24.12/4.09 % (1546654)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3695976913:i=14155:bd=all_2984 on theBenchmark for (2984ds/14155Mi) % 24.12/4.09 % (1546680)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=3576183985:s2a=on:i=185:s2at=1.8:fdi=4_2983 on theBenchmark for (2983ds/185Mi) % 24.12/4.09 % (1546653)Instruction limit reached! % 24.12/4.09 % (1546653)------------------------------ % 24.12/4.09 % (1546653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.12/4.09 % (1546653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.12/4.09 % (1546653)CaDiCaL version: 2.1.3 % 24.12/4.09 % (1546653)Termination reason: Instruction limit % 24.12/4.09 % (1546653)Termination phase: Saturation % 24.12/4.09 % (1546653)Time elapsed: 0.095 s % 24.12/4.09 % (1546653)Peak memory usage: 90 MB % 24.12/4.09 % (1546653)Instructions burned: 150 (million) % 24.12/4.09 % Exception at run slice level % 24.12/4.09 User error: GNN currently only supports monomorphic FOL. % 24.12/4.09 % (1546669)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=101615064:i=667:av=off:fsr=off_2983 on theBenchmark for (2983ds/667Mi) % 24.12/4.09 % (1546669)Refutation not found, incomplete strategy % 24.12/4.09 % (1546669)------------------------------ % 24.12/4.09 % (1546669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.12/4.09 % (1546669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.12/4.09 % (1546669)CaDiCaL version: 2.1.3 % 24.12/4.09 % (1546669)Termination reason: Refutation not found, incomplete strategy % 24.12/4.09 % (1546669)Time elapsed: 0.009 s % 24.12/4.09 % (1546669)Peak memory usage: 88 MB % 24.12/4.09 % (1546669)Instructions burned: 17 (million) % 24.12/4.09 % (1546680)Instruction limit reached! % 24.12/4.09 % (1546680)------------------------------ % 24.12/4.09 % (1546680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.12/4.09 % (1546680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.12/4.09 % (1546680)CaDiCaL version: 2.1.3 % 24.12/4.09 % (1546680)Termination reason: Instruction limit % 24.12/4.09 % (1546680)Termination phase: Saturation % 24.12/4.09 % (1546680)Time elapsed: 0.064 s % 24.12/4.09 % (1546680)Peak memory usage: 91 MB % 24.12/4.09 % (1546680)Instructions burned: 186 (million) % 24.12/4.09 % (1546648)------------------------------ % 24.12/4.09 % (1546648)------------------------------ % 24.12/4.09 % (1546714)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1766619919:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2982 on theBenchmark for (2982ds/4850Mi) % 24.12/4.09 % (1546711)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1140915136:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2982 on theBenchmark for (2982ds/193Mi) % 24.12/4.09 % (1546714)Refutation not found, incomplete strategy % 24.12/4.09 % (1546714)------------------------------ % 24.12/4.09 % (1546714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.12/4.09 % (1546714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.12/4.09 % (1546714)CaDiCaL version: 2.1.3 % 24.12/4.09 % (1546714)Termination reason: Refutation not found, incomplete strategy % 24.12/4.09 % (1546714)Time elapsed: 0.007 s % 24.12/4.09 % (1546714)Peak memory usage: 88 MB % 24.12/4.09 % (1546714)Instructions burned: 12 (million) % 24.12/4.09 % (1546736)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2095596359:i=12111:sd=1:ss=included_2981 on theBenchmark for (2981ds/12111Mi) % 24.12/4.09 % (1546739)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1966207085:i=319:kws=precedence:fsr=off_2981 on theBenchmark for (2981ds/319Mi) % 24.12/4.09 % Exception at run slice level % 24.12/4.09 User error: GNN currently only supports monomorphic FOL. % 24.12/4.09 % (1546711)Instruction limit reached! % 24.12/4.09 % (1546711)------------------------------ % 24.12/4.09 % (1546711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.12/4.09 % (1546711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.12/4.09 % (1546711)CaDiCaL version: 2.1.3 % 24.12/4.09 % (1546711)Termination reason: Instruction limit % 24.12/4.09 % (1546711)Termination phase: Saturation % 24.12/4.09 % (1546711)Time elapsed: 0.116 s % 24.12/4.09 % (1546711)Peak memory usage: 90 MB % 27.58/5.03 % (1546711)Instructions burned: 194 (million) % 27.58/5.03 % (1546669)------------------------------ % 27.58/5.03 % (1546669)------------------------------ % 27.58/5.03 % Exception at run slice level % 27.58/5.03 User error: GNN currently only supports monomorphic FOL. % 27.58/5.03 % Exception at run slice level % 27.58/5.03 User error: GNN currently only supports monomorphic FOL. % 27.58/5.03 % (1546776)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2392086275:i=2064:ep=RST_2980 on theBenchmark for (2980ds/2064Mi) % 27.58/5.03 % (1546777)dis-1011_128_sil=32000:random_seed=2312814594:i=3706:ep=RST:av=off_2980 on theBenchmark for (2980ds/3706Mi) % 27.58/5.03 % (1546714)------------------------------ % 27.58/5.03 % (1546714)------------------------------ % 27.58/5.03 % (1546739)Instruction limit reached! % 27.58/5.03 % (1546739)------------------------------ % 27.58/5.03 % (1546739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.58/5.03 % (1546739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.58/5.03 % (1546739)CaDiCaL version: 2.1.3 % 27.58/5.03 % (1546739)Termination reason: Instruction limit % 27.58/5.03 % (1546739)Termination phase: Saturation % 27.58/5.03 % (1546739)Time elapsed: 0.190 s % 27.58/5.03 % (1546739)Peak memory usage: 92 MB % 27.58/5.03 % (1546739)Instructions burned: 319 (million) % 27.58/5.03 % (1546778)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1883802525:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2979 on theBenchmark for (2979ds/757Mi) % 27.58/5.03 % (1546779)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3242475931:i=13913:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/13913Mi) % 27.58/5.03 % (1546778)Refutation not found, incomplete strategy % 27.58/5.03 % (1546778)------------------------------ % 27.58/5.03 % (1546778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.58/5.03 % (1546778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.58/5.03 % (1546778)CaDiCaL version: 2.1.3 % 27.58/5.03 % (1546778)Termination reason: Refutation not found, incomplete strategy % 27.58/5.03 % (1546778)Time elapsed: 0.009 s % 27.58/5.03 % (1546778)Peak memory usage: 89 MB % 27.58/5.03 % (1546778)Instructions burned: 16 (million) % 27.58/5.03 % (1546785)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=210258227:i=9925:aac=none_2979 on theBenchmark for (2979ds/9925Mi) % 27.58/5.03 % (1546797)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1144890703:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2978 on theBenchmark for (2978ds/2479Mi) % 27.58/5.03 % (1546810)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3841942551:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2978 on theBenchmark for (2978ds/440Mi) % 27.58/5.03 % (1546797)Refutation not found, incomplete strategy % 27.58/5.03 % (1546797)------------------------------ % 27.58/5.03 % (1546797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.58/5.03 % (1546797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.58/5.03 % (1546797)CaDiCaL version: 2.1.3 % 27.58/5.03 % (1546797)Termination reason: Refutation not found, incomplete strategy % 27.58/5.03 % (1546797)Time elapsed: 0.008 s % 27.58/5.03 % (1546797)Peak memory usage: 89 MB % 27.58/5.03 % (1546797)Instructions burned: 13 (million) % 27.58/5.03 % (1546810)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 27.58/5.03 % Exception at run slice level % 27.58/5.03 User error: GNN currently only supports monomorphic FOL. % 27.58/5.03 % (1546778)------------------------------ % 27.58/5.03 % (1546778)------------------------------ % 27.58/5.03 % (1546837)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3172908951:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2976 on theBenchmark for (2976ds/11145Mi) % 27.58/5.03 % Exception at run slice level % 27.58/5.03 User error: GNN currently only supports monomorphic FOL. % 27.58/5.03 % (1546810)Instruction limit reached! % 27.58/5.03 % (1546810)------------------------------ % 27.58/5.03 % (1546810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.58/5.03 % (1546810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.58/5.03 % (1546810)CaDiCaL version: 2.1.3 % 27.58/5.03 % (1546810)Termination reason: Instruction limit % 27.58/5.03 % (1546810)Termination phase: Saturation % 33.69/5.57 % (1546810)Time elapsed: 0.240 s % 33.69/5.57 % (1546810)Peak memory usage: 91 MB % 33.69/5.57 % (1546810)Instructions burned: 441 (million) % 33.69/5.57 % (1546797)------------------------------ % 33.69/5.57 % (1546797)------------------------------ % 33.69/5.57 % (1546838)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=1049095397:cts=off:i=3034:av=off:er=known:fsd=on_2975 on theBenchmark for (2975ds/3034Mi) % 33.69/5.57 % (1546841)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3337154745:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2974 on theBenchmark for (2974ds/1016Mi) % 33.69/5.57 % (1546840)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=4025820518:st=2:s2a=on:i=524:s2at=2:ss=axioms_2974 on theBenchmark for (2974ds/524Mi) % 33.69/5.57 % (1546842)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=398759027:i=14123:bd=preordered:ins=4_2974 on theBenchmark for (2974ds/14123Mi) % 33.69/5.57 % Exception at run slice level % 33.69/5.57 User error: GNN currently only supports monomorphic FOL. % 33.69/5.57 % (1546847)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2066746352:i=5781:kws=precedence:bd=all:rawr=on_2973 on theBenchmark for (2973ds/5781Mi) % 33.69/5.57 % Exception at run slice level % 33.69/5.57 User error: GNN currently only supports monomorphic FOL. % 33.69/5.57 % (1546840)Instruction limit reached! % 33.69/5.57 % (1546840)------------------------------ % 33.69/5.57 % (1546840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.69/5.57 % (1546840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.69/5.57 % (1546840)CaDiCaL version: 2.1.3 % 33.69/5.57 % (1546840)Termination reason: Instruction limit % 33.69/5.57 % (1546840)Termination phase: Saturation % 33.69/5.57 % (1546840)Time elapsed: 0.306 s % 33.69/5.57 % (1546840)Peak memory usage: 95 MB % 33.69/5.57 % (1546840)Instructions burned: 525 (million) % 33.69/5.57 % Exception at run slice level % 33.69/5.57 User error: GNN currently only supports monomorphic FOL. % 33.69/5.57 % (1546849)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=4128020027:i=2448:gtgl=5:bd=preordered:gtg=all_2970 on theBenchmark for (2970ds/2448Mi) % 33.69/5.57 % (1546776)Instruction limit reached! % 33.69/5.57 % (1546776)------------------------------ % 33.69/5.57 % (1546776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.69/5.57 % (1546776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.69/5.57 % (1546776)CaDiCaL version: 2.1.3 % 33.69/5.57 % (1546776)Termination reason: Instruction limit % 33.69/5.57 % (1546776)Termination phase: Saturation % 33.69/5.57 % (1546776)Time elapsed: 0.929 s % 33.69/5.57 % (1546776)Peak memory usage: 92 MB % 33.69/5.57 % (1546776)Instructions burned: 2064 (million) % 33.69/5.57 % (1546850)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1464189237:i=3223:kws=precedence:fgj=on:av=off_2970 on theBenchmark for (2970ds/3223Mi) % 33.69/5.57 % (1546851)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3029828313:st=5.6:i=2033:sd=3:ss=axioms_2969 on theBenchmark for (2969ds/2033Mi) % 33.69/5.57 % (1546853)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1538862209:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2969 on theBenchmark for (2969ds/2055Mi) % 33.69/5.57 % (1546841)Instruction limit reached! % 33.69/5.57 % (1546841)------------------------------ % 33.69/5.57 % (1546841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.69/5.57 % (1546841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.69/5.57 % (1546841)CaDiCaL version: 2.1.3 % 33.69/5.57 % (1546841)Termination reason: Instruction limit % 33.69/5.57 % (1546841)Termination phase: Saturation % 33.69/5.57 % (1546841)Time elapsed: 0.584 s % 33.69/5.57 % (1546841)Peak memory usage: 99 MB % 33.69/5.57 % (1546841)Instructions burned: 1017 (million) % 33.69/5.57 % (1546857)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=4087082686:i=21611:sd=3:ss=axioms_2967 on theBenchmark for (2967ds/21611Mi) % 33.69/5.57 % Exception at run slice level % 33.69/5.57 User error: GNN currently only supports monomorphic FOL. % 33.69/5.57 % Exception at run slice level % 43.01/6.92 User error: GNN currently only supports monomorphic FOL. % 43.01/6.92 % Exception at run slice level % 43.01/6.92 User error: GNN currently only supports monomorphic FOL. % 43.01/6.92 % Exception at run slice level % 43.01/6.92 User error: GNN currently only supports monomorphic FOL. % 43.01/6.92 % (1546859)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3797160058:i=4835:sd=13:ss=axioms:sgt=23_2966 on theBenchmark for (2966ds/4835Mi) % 43.01/6.92 % (1546860)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=625131782:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2965 on theBenchmark for (2965ds/797Mi) % 43.01/6.92 % (1546861)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1850940954:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2964 on theBenchmark for (2964ds/2326Mi) % 43.01/6.92 % (1546863)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1118011014:i=6038:nm=6_2964 on theBenchmark for (2964ds/6038Mi) % 43.01/6.92 % (1546777)Instruction limit reached! % 43.01/6.92 % (1546777)------------------------------ % 43.01/6.92 % (1546777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.01/6.92 % (1546777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.01/6.92 % (1546777)CaDiCaL version: 2.1.3 % 43.01/6.92 % (1546777)Termination reason: Instruction limit % 43.01/6.92 % (1546777)Termination phase: Saturation % 43.01/6.92 % (1546777)Time elapsed: 1.542 s % 43.01/6.92 % (1546777)Peak memory usage: 92 MB % 43.01/6.92 % (1546777)Instructions burned: 3707 (million) % 43.01/6.92 % (1546861)Refutation not found, incomplete strategy % 43.01/6.92 % (1546861)------------------------------ % 43.01/6.92 % (1546861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.01/6.92 % (1546861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.01/6.92 % (1546861)CaDiCaL version: 2.1.3 % 43.01/6.92 % (1546861)Termination reason: Refutation not found, incomplete strategy % 43.01/6.92 % (1546861)Time elapsed: 0.012 s % 43.01/6.92 % (1546861)Peak memory usage: 89 MB % 43.01/6.92 % (1546861)Instructions burned: 20 (million) % 43.01/6.92 % Exception at run slice level % 43.01/6.92 User error: GNN currently only supports monomorphic FOL. % 43.01/6.92 % (1546867)lrs+10_1_sil=32000:sp=occurrence:random_seed=3599766760:st=2:i=33334:sd=3:ss=included:sgt=32_2963 on theBenchmark for (2963ds/33334Mi) % 43.01/6.92 % (1546868)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1223546809:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2962 on theBenchmark for (2962ds/1008Mi) % 43.01/6.92 % (1546861)------------------------------ % 43.01/6.92 % (1546861)------------------------------ % 43.01/6.92 % (1546860)Instruction limit reached! % 43.01/6.92 % (1546860)------------------------------ % 43.01/6.92 % (1546860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.01/6.92 % (1546860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.01/6.92 % (1546860)CaDiCaL version: 2.1.3 % 43.01/6.92 % (1546860)Termination reason: Instruction limit % 43.01/6.92 % (1546860)Termination phase: Saturation % 43.01/6.92 % (1546860)Time elapsed: 0.388 s % 43.01/6.92 % (1546860)Peak memory usage: 128 MB % 43.01/6.92 % (1546860)Instructions burned: 799 (million) % 43.01/6.92 % Exception at run slice level % 43.01/6.92 User error: GNN currently only supports monomorphic FOL. % 43.01/6.92 % (1546871)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=2514068795:i=8327:s2at=5:bd=preordered_2960 on theBenchmark for (2960ds/8327Mi) % 43.01/6.92 % (1546872)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=2964927122:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2960 on theBenchmark for (2960ds/1083Mi) % 43.01/6.92 % (1546873)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=786829617:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2959 on theBenchmark for (2959ds/1084Mi) % 43.01/6.92 % (1546868)Instruction limit reached! % 43.01/6.92 % (1546868)------------------------------ % 43.01/6.92 % (1546868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.41/8.08 % (1546868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.41/8.08 % (1546868)CaDiCaL version: 2.1.3 % 52.41/8.08 % (1546868)Termination reason: Instruction limit % 52.41/8.08 % (1546868)Termination phase: Saturation % 52.41/8.08 % (1546868)Time elapsed: 0.525 s % 52.41/8.08 % (1546868)Peak memory usage: 99 MB % 52.41/8.08 % (1546868)Instructions burned: 1008 (million) % 52.41/8.08 % Exception at run slice level % 52.41/8.08 User error: GNN currently only supports monomorphic FOL. % 52.41/8.08 % (1546847)Instruction limit reached! % 52.41/8.08 % (1546847)------------------------------ % 52.41/8.08 % (1546847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.41/8.08 % (1546847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.41/8.08 % (1546847)CaDiCaL version: 2.1.3 % 52.41/8.08 % (1546847)Termination reason: Instruction limit % 52.41/8.08 % (1546847)Termination phase: Saturation % 52.41/8.08 % (1546847)Time elapsed: 1.676 s % 52.41/8.08 % (1546847)Peak memory usage: 124 MB % 52.41/8.08 % (1546847)Instructions burned: 5781 (million) % 52.41/8.08 % (1546877)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2023826036:i=6995:s2at=5:gtg=all_2956 on theBenchmark for (2956ds/6995Mi) % 52.41/8.08 % (1546878)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1261338653:st=2:i=6225:sd=15:ss=axioms_2956 on theBenchmark for (2956ds/6225Mi) % 52.41/8.08 % (1546878)Refutation not found, incomplete strategy % 52.41/8.08 % (1546878)------------------------------ % 52.41/8.08 % (1546878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.41/8.08 % (1546878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.41/8.08 % (1546878)CaDiCaL version: 2.1.3 % 52.41/8.08 % (1546878)Termination reason: Refutation not found, incomplete strategy % 52.41/8.08 % (1546878)Time elapsed: 0.008 s % 52.41/8.08 % (1546878)Peak memory usage: 89 MB % 52.41/8.08 % (1546878)Instructions burned: 13 (million) % 52.41/8.08 % (1546879)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2636765472:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2955 on theBenchmark for (2955ds/3372Mi) % 52.41/8.08 % (1546872)Instruction limit reached! % 52.41/8.08 % (1546872)------------------------------ % 52.41/8.08 % (1546872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.41/8.08 % (1546872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.41/8.08 % (1546872)CaDiCaL version: 2.1.3 % 52.41/8.08 % (1546872)Termination reason: Instruction limit % 52.41/8.08 % (1546872)Termination phase: Saturation % 52.41/8.08 % (1546872)Time elapsed: 0.529 s % 52.41/8.08 % (1546872)Peak memory usage: 97 MB % 52.41/8.08 % (1546872)Instructions burned: 1085 (million) % 52.41/8.08 % Exception at run slice level % 52.41/8.08 User error: GNN currently only supports monomorphic FOL. % 52.41/8.08 % (1546883)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1928000624:st=2.3:i=26457:sd=10:ss=included:sgt=8_2953 on theBenchmark for (2953ds/26457Mi) % 52.41/8.08 % (1546878)------------------------------ % 52.41/8.08 % (1546878)------------------------------ % 52.41/8.08 % (1546873)Instruction limit reached! % 52.41/8.08 % (1546873)------------------------------ % 52.41/8.08 % (1546873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.41/8.09 % (1546873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.41/8.09 % (1546873)CaDiCaL version: 2.1.3 % 52.41/8.09 % (1546873)Termination reason: Instruction limit % 52.41/8.09 % (1546873)Termination phase: Saturation % 52.41/8.09 % (1546873)Time elapsed: 0.624 s % 52.41/8.09 % (1546873)Peak memory usage: 98 MB % 52.41/8.09 % (1546873)Instructions burned: 1084 (million) % 52.41/8.09 % (1546884)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=2553940496:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2952 on theBenchmark for (2952ds/13494Mi) % 52.41/8.09 % Exception at run slice level % 52.41/8.09 User error: GNN currently only supports monomorphic FOL. % 52.41/8.09 % (1546886)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=685816647:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2952 on theBenchmark for (2952ds/2503Mi) % 52.41/8.09 % (1546886)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 62.61/9.64 % (1546887)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=3771694382:i=2559:sd=1:ep=RSTC:ss=axioms_2952 on theBenchmark for (2952ds/2559Mi) % 62.61/9.64 % (1546889)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3776323632:i=30753:av=off:ss=included_2951 on theBenchmark for (2951ds/30753Mi) % 62.61/9.64 % Exception at run slice level % 62.61/9.64 User error: GNN currently only supports monomorphic FOL. % 62.61/9.64 % (1546893)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2946808874:i=26473:ep=RSTC_2949 on theBenchmark for (2949ds/26473Mi) % 62.61/9.64 % Exception at run slice level % 62.61/9.64 User error: GNN currently only supports monomorphic FOL. % 62.61/9.64 % (1546895)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=387902948:cts=off:i=2759:kws=inv_arity:fgj=on_2948 on theBenchmark for (2948ds/2759Mi) % 62.61/9.64 % Exception at run slice level % 62.61/9.64 User error: GNN currently only supports monomorphic FOL. % 62.61/9.64 % Exception at run slice level % 62.61/9.64 User error: GNN currently only supports monomorphic FOL. % 62.61/9.64 % Exception at run slice level % 62.61/9.64 User error: GNN currently only supports monomorphic FOL. % 62.61/9.64 % (1546897)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=4279634065:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2947 on theBenchmark for (2947ds/5665Mi) % 62.61/9.64 % (1546897)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 62.61/9.64 % (1546898)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=1082513471:i=1532:ep=RS:ss=axioms_2947 on theBenchmark for (2947ds/1532Mi) % 62.61/9.64 % (1546899)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=1216849466:i=1565:sd=2:ss=axioms:sgt=32_2946 on theBenchmark for (2946ds/1565Mi) % 62.61/9.64 % Exception at run slice level % 62.61/9.64 User error: GNN currently only supports monomorphic FOL. % 62.61/9.64 % (1546903)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=1061105533:i=1572:fgj=on:gsp=on_2943 on theBenchmark for (2943ds/1572Mi) % 62.61/9.64 % (1546903)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 62.61/9.64 % Exception at run slice level % 62.61/9.64 User error: GNN currently only supports monomorphic FOL. % 62.61/9.64 % Exception at run slice level % 62.61/9.64 User error: GNN currently only supports monomorphic FOL. % 62.61/9.64 % Exception at run slice level % 62.61/9.64 User error: GNN currently only supports monomorphic FOL. % 62.61/9.64 % (1546905)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=947979181:i=6052:sd=4:ss=axioms:sgt=24_2942 on theBenchmark for (2942ds/6052Mi) % 62.61/9.64 % (1546906)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=303945575:i=3500:sd=1:bd=preordered:sup=off:ss=included_2942 on theBenchmark for (2942ds/3500Mi) % 62.61/9.64 % (1546907)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=2345712086:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2941 on theBenchmark for (2941ds/1842Mi) % 62.61/9.64 % (1546907)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 62.61/9.64 % Exception at run slice level % 62.61/9.64 User error: GNN currently only supports monomorphic FOL. % 62.61/9.64 % Exception at run slice level % 62.61/9.64 User error: GNN currently only supports monomorphic FOL. % 62.61/9.64 % (1546911)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1025961775:i=66096:add=on_2939 on theBenchmark for (2939ds/66096Mi) % 62.61/9.64 % (1546859)Instruction limit reached! % 62.61/9.64 % (1546859)------------------------------ % 62.61/9.64 % (1546859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.70/11.13 % (1546859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.70/11.13 % (1546859)CaDiCaL version: 2.1.3 % 73.70/11.13 % (1546859)Termination reason: Instruction limit % 73.70/11.13 % (1546859)Termination phase: Saturation % 73.70/11.13 % (1546859)Time elapsed: 2.716 s % 73.70/11.13 % (1546859)Peak memory usage: 114 MB % 73.70/11.13 % (1546859)Instructions burned: 4835 (million) % 73.70/11.13 % Exception at run slice level % 73.70/11.13 User error: GNN currently only supports monomorphic FOL. % 73.70/11.13 % Exception at run slice level % 73.70/11.13 User error: GNN currently only supports monomorphic FOL. % 73.70/11.13 % (1546912)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=1467796375:i=1884:sd=1:nm=60:ss=axioms_2937 on theBenchmark for (2937ds/1884Mi) % 73.70/11.13 % (1546914)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3253502059:cts=off:i=5469:bs=on:fsr=off_2937 on theBenchmark for (2937ds/5469Mi) % 73.70/11.13 % (1546915)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=4194939611:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2937 on theBenchmark for (2937ds/2037Mi) % 73.70/11.13 % (1546917)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2965622727:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2936 on theBenchmark for (2936ds/2110Mi) % 73.70/11.13 % Exception at run slice level % 73.70/11.13 User error: GNN currently only supports monomorphic FOL. % 73.70/11.13 % Exception at run slice level % 73.70/11.13 User error: GNN currently only supports monomorphic FOL. % 73.70/11.13 % (1546921)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=3406501402:i=2430:add=off:aac=none:nm=16_2934 on theBenchmark for (2934ds/2430Mi) % 73.70/11.13 % Exception at run slice level % 73.70/11.13 User error: GNN currently only supports monomorphic FOL. % 73.70/11.13 % (1546922)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=2670666836:cond=fast:i=4891_2932 on theBenchmark for (2932ds/4891Mi) % 73.70/11.13 % Exception at run slice level % 73.70/11.13 User error: GNN currently only supports monomorphic FOL. % 73.70/11.13 % (1546924)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=3773123991:st=2:i=14845:sd=2:ss=included:fsd=on_2932 on theBenchmark for (2932ds/14845Mi) % 73.70/11.13 % (1546926)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=1691989730:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2931 on theBenchmark for (2931ds/7534Mi) % 73.70/11.13 % Exception at run slice level % 73.70/11.13 User error: GNN currently only supports monomorphic FOL. % 73.70/11.13 % Exception at run slice level % 73.70/11.13 User error: GNN currently only supports monomorphic FOL. % 73.70/11.13 % (1546929)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=2537703957:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2929 on theBenchmark for (2929ds/10353Mi) % 73.70/11.13 % Exception at run slice level % 73.70/11.13 User error: GNN currently only supports monomorphic FOL. % 73.70/11.13 % Exception at run slice level % 73.70/11.13 User error: GNN currently only supports monomorphic FOL. % 73.70/11.13 % (1546930)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1879315048:i=7860_2928 on theBenchmark for (2928ds/7860Mi) % 73.70/11.13 % (1546930)Refutation not found, incomplete strategy % 73.70/11.13 % (1546930)------------------------------ % 73.70/11.13 % (1546930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.70/11.13 % (1546930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.70/11.13 % (1546930)CaDiCaL version: 2.1.3 % 73.70/11.13 % (1546930)Termination reason: Refutation not found, incomplete strategy % 73.70/11.13 % (1546930)Time elapsed: 0.008 s % 73.70/11.13 % (1546930)Peak memory usage: 88 MB % 73.70/11.13 % (1546930)Instructions burned: 15 (million) % 73.70/11.13 % (1546932)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=231155671:i=7896:sd=2:bs=on:ss=included:sgt=20_2927 on theBenchmark for (2927ds/7896Mi) % 90.49/13.49 % (1546934)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=2769665927:i=5812:gtgl=2:gtg=all_2926 on theBenchmark for (2926ds/5812Mi) % 90.49/13.49 % Exception at run slice level % 90.49/13.49 User error: GNN currently only supports monomorphic FOL. % 90.49/13.49 % (1546930)------------------------------ % 90.49/13.49 % (1546930)------------------------------ % 90.49/13.49 % (1546938)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=1733449313:i=2967:kws=precedence:bd=preordered:av=off_2924 on theBenchmark for (2924ds/2967Mi) % 90.49/13.49 % (1546937)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=4246366552:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2924 on theBenchmark for (2924ds/2965Mi) % 90.49/13.49 % Exception at run slice level % 90.49/13.49 User error: GNN currently only supports monomorphic FOL. % 90.49/13.49 % Exception at run slice level % 90.49/13.49 User error: GNN currently only supports monomorphic FOL. % 90.49/13.49 % (1546941)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=3139867527:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2922 on theBenchmark for (2922ds/3022Mi) % 90.49/13.49 % (1546942)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=1268555913:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2921 on theBenchmark for (2921ds/3207Mi) % 90.49/13.49 % Exception at run slice level % 90.49/13.49 User error: GNN currently only supports monomorphic FOL. % 90.49/13.49 % Exception at run slice level % 90.49/13.49 User error: GNN currently only supports monomorphic FOL. % 90.49/13.49 % (1546945)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=2176549972:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2919 on theBenchmark for (2919ds/3289Mi) % 90.49/13.49 % (1546946)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=2133317969:i=38569:sd=3:ss=axioms:sgt=32_2919 on theBenchmark for (2919ds/38569Mi) % 90.49/13.49 % Exception at run slice level % 90.49/13.49 User error: GNN currently only supports monomorphic FOL. % 90.49/13.49 % Exception at run slice level % 90.49/13.49 User error: GNN currently only supports monomorphic FOL. % 90.49/13.49 % (1546949)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=403340930:cts=off:i=3394_2917 on theBenchmark for (2917ds/3394Mi) % 90.49/13.49 % (1546950)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=3997058121:i=33824:bd=preordered_2916 on theBenchmark for (2916ds/33824Mi) % 90.49/13.49 % Exception at run slice level % 90.49/13.49 User error: GNN currently only supports monomorphic FOL. % 90.49/13.49 % Exception at run slice level % 90.49/13.49 User error: GNN currently only supports monomorphic FOL. % 90.49/13.49 % (1546953)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=4065476660:i=20684:bd=all:gtg=exists_sym_2914 on theBenchmark for (2914ds/20684Mi) % 90.49/13.49 % (1546954)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=3185988800: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_2914 on theBenchmark for (2914ds/7222Mi) % 90.49/13.49 % (1546954)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 90.49/13.49 % Exception at run slice level % 90.49/13.49 User error: GNN currently only supports monomorphic FOL. % 90.49/13.49 % Exception at run slice level % 90.49/13.49 User error: GNN currently only supports monomorphic FOL. % 90.49/13.49 % (1546957)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=1868134604:st=4:i=7295:sd=4:ep=R:ss=axioms_2912 on theBenchmark for (2912ds/7295Mi) % 90.49/13.49 % (1546958)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=767201209:i=4036:ins=10_2911 on theBenchmark for (2911ds/4036Mi) % 113.58/16.73 % Exception at run slice level % 113.58/16.73 User error: GNN currently only supports monomorphic FOL. % 113.58/16.73 % Exception at run slice level % 113.58/16.73 User error: GNN currently only supports monomorphic FOL. % 113.58/16.73 % (1546961)lrs+10_1_sil=128000:lcm=predicate:random_seed=2876554812:st=3:i=43697:sd=5:ss=axioms_2909 on theBenchmark for (2909ds/43697Mi) % 113.58/16.73 % (1546962)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=2609668628:i=17599:gtg=all:ss=axioms:fsd=on_2909 on theBenchmark for (2909ds/17599Mi) % 113.58/16.73 % Exception at run slice level % 113.58/16.73 User error: GNN currently only supports monomorphic FOL. % 113.58/16.73 % Exception at run slice level % 113.58/16.73 User error: GNN currently only supports monomorphic FOL. % 113.58/16.73 % (1546965)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=1485174486:i=4547:bd=preordered_2907 on theBenchmark for (2907ds/4547Mi) % 113.58/16.73 % (1546966)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=1790724631:i=9294:av=off_2906 on theBenchmark for (2906ds/9294Mi) % 113.58/16.73 % Exception at run slice level % 113.58/16.73 User error: GNN currently only supports monomorphic FOL. % 113.58/16.73 % (1546914)Instruction limit reached! % 113.58/16.73 % (1546914)------------------------------ % 113.58/16.73 % (1546914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.58/16.73 % (1546914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.58/16.73 % (1546914)CaDiCaL version: 2.1.3 % 113.58/16.73 % (1546914)Termination reason: Instruction limit % 113.58/16.73 % (1546914)Termination phase: Saturation % 113.58/16.73 % (1546914)Time elapsed: 3.243 s % 113.58/16.73 % (1546914)Peak memory usage: 118 MB % 113.58/16.73 % (1546914)Instructions burned: 5471 (million) % 113.58/16.73 % (1546969)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2359548282:i=32849:add=on_2904 on theBenchmark for (2904ds/32849Mi) % 113.58/16.73 % Exception at run slice level % 113.58/16.73 User error: GNN currently only supports monomorphic FOL. % 113.58/16.73 % (1546970)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4239394890:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2903 on theBenchmark for (2903ds/4793Mi) % 113.58/16.73 % Exception at run slice level % 113.58/16.73 User error: GNN currently only supports monomorphic FOL. % 113.58/16.73 % (1546972)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=653894842:i=4840:nm=4:av=off_2902 on theBenchmark for (2902ds/4840Mi) % 113.58/16.73 % (1546974)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=2293230726:cts=off:i=5002_2901 on theBenchmark for (2901ds/5002Mi) % 113.58/16.73 % Exception at run slice level % 113.58/16.73 User error: GNN currently only supports monomorphic FOL. % 113.58/16.73 % Exception at run slice level % 113.58/16.73 User error: GNN currently only supports monomorphic FOL. % 113.58/16.73 % (1546977)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=3875752465:i=30479:sd=3:ss=axioms_2899 on theBenchmark for (2899ds/30479Mi) % 113.58/16.73 % Exception at run slice level % 113.58/16.73 User error: GNN currently only supports monomorphic FOL. % 113.58/16.73 % (1546978)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=157601653:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2898 on theBenchmark for (2898ds/11035Mi) % 113.58/16.73 % (1546978)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 113.58/16.73 % Exception at run slice level % 113.58/16.73 User error: GNN currently only supports monomorphic FOL. % 113.58/16.73 % (1546980)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=1280660350:i=5835_2897 on theBenchmark for (2897ds/5835Mi) % 113.58/16.73 % (1546982)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=1866712562:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2896 on theBenchmark for (2896ds/5890Mi) % 123.37/18.06 % Exception at run slice level % 123.37/18.06 User error: GNN currently only supports monomorphic FOL. % 123.37/18.06 % Exception at run slice level % 123.37/18.06 User error: GNN currently only supports monomorphic FOL. % 123.37/18.06 % (1546985)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=3448892974:cts=off:i=19910:ep=RS_2894 on theBenchmark for (2894ds/19910Mi) % 123.37/18.06 % (1546985)Refutation not found, incomplete strategy % 123.37/18.06 % (1546985)------------------------------ % 123.37/18.06 % (1546985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.37/18.06 % (1546985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.37/18.06 % (1546985)CaDiCaL version: 2.1.3 % 123.37/18.06 % (1546985)Termination reason: Refutation not found, incomplete strategy % 123.37/18.06 % (1546985)Time elapsed: 0.009 s % 123.37/18.06 % (1546985)Peak memory usage: 89 MB % 123.37/18.06 % (1546985)Instructions burned: 16 (million) % 123.37/18.06 % Exception at run slice level % 123.37/18.06 User error: GNN currently only supports monomorphic FOL. % 123.37/18.06 % (1546986)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=2776531185:i=20312:bd=preordered:fsr=off:er=filter_2893 on theBenchmark for (2893ds/20312Mi) % 123.37/18.06 % Exception at run slice level % 123.37/18.06 User error: GNN currently only supports monomorphic FOL. % 123.37/18.06 % (1546988)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=1348500811:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2892 on theBenchmark for (2892ds/13822Mi) % 123.37/18.06 % (1546985)------------------------------ % 123.37/18.06 % (1546985)------------------------------ % 123.37/18.06 % (1546990)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=4217508987:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2891 on theBenchmark for (2891ds/7144Mi) % 123.37/18.06 % (1546992)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=1034779548:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2890 on theBenchmark for (2890ds/15184Mi) % 123.37/18.06 % Exception at run slice level % 123.37/18.06 User error: GNN currently only supports monomorphic FOL. % 123.37/18.06 % Exception at run slice level % 123.37/18.06 User error: GNN currently only supports monomorphic FOL. % 123.37/18.06 % (1546995)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=3238923443:i=107375_2888 on theBenchmark for (2888ds/107375Mi) % 123.37/18.06 % (1546996)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=3225085459:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2887 on theBenchmark for (2887ds/7958Mi) % 123.37/18.06 % Exception at run slice level % 123.37/18.06 User error: GNN currently only supports monomorphic FOL. % 123.37/18.06 % (1546999)dis+10_128_sil=16000:nwc=0.7:random_seed=1854942527:i=15999:nm=2:gsp=on_2886 on theBenchmark for (2886ds/15999Mi) % 123.37/18.06 % (1546999)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 123.37/18.06 % Exception at run slice level % 123.37/18.06 User error: GNN currently only supports monomorphic FOL. % 123.37/18.06 % Exception at run slice level % 123.37/18.06 User error: GNN currently only supports monomorphic FOL. % 123.37/18.06 % (1547001)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=3782344522:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2883 on theBenchmark for (2883ds/8139Mi) % 123.37/18.06 % (1547002)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=3358474279:st=4:i=8950:sd=5:ss=axioms_2882 on theBenchmark for (2882ds/8950Mi) % 123.37/18.06 % Exception at run slice level % 123.37/18.06 User error: GNN currently only supports monomorphic FOL. % 123.37/18.06 % (1547005)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=1358151751:i=9809:ins=10:av=off_2878 on theBenchmark for (2878ds/9809Mi) % 123.37/18.06 % Exception at run slice level % 123.37/18.06 User error: GNN currently only supports monomorphic FOL. % 123.37/18.06 % (1547008)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=2746076046:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2873 on theBenchmark for (2873ds/9885Mi) % 159.55/23.14 % (1546893)Instruction limit reached! % 159.55/23.14 % (1546893)------------------------------ % 159.55/23.14 % (1546893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.55/23.14 % (1546893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.55/23.14 % (1546893)CaDiCaL version: 2.1.3 % 159.55/23.14 % (1546893)Termination reason: Instruction limit % 159.55/23.14 % (1546893)Termination phase: Saturation % 159.55/23.14 % (1546893)Time elapsed: 7.737 s % 159.55/23.14 % (1546893)Peak memory usage: 284 MB % 159.55/23.14 % (1546893)Instructions burned: 26476 (million) % 159.55/23.14 % (1547056)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=3753755285:cond=fast:i=32078:fgj=on:av=off_2871 on theBenchmark for (2871ds/32078Mi) % 159.55/23.14 % Exception at run slice level % 159.55/23.14 User error: GNN currently only supports monomorphic FOL. % 159.55/23.14 % Exception at run slice level % 159.55/23.14 User error: GNN currently only supports monomorphic FOL. % 159.55/23.14 % (1547168)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=3393169303:i=11101:bd=all:ss=axioms:sgt=8_2868 on theBenchmark for (2868ds/11101Mi) % 159.55/23.14 % (1547189)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=238874303:cond=on:i=13220:s2at=3:aac=none:fsd=on_2868 on theBenchmark for (2868ds/13220Mi) % 159.55/23.14 % Exception at run slice level % 159.55/23.14 User error: GNN currently only supports monomorphic FOL. % 159.55/23.14 % (1547290)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=2893285178:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2861 on theBenchmark for (2861ds/13528Mi) % 159.55/23.14 % Exception at run slice level % 159.55/23.14 User error: GNN currently only supports monomorphic FOL. % 159.55/23.14 % (1547292)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=3814758498:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2855 on theBenchmark for (2855ds/14854Mi) % 159.55/23.14 % Exception at run slice level % 159.55/23.14 User error: GNN currently only supports monomorphic FOL. % 159.55/23.14 % (1547294)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=3755618875:i=14974:ss=axioms:sgt=16_2850 on theBenchmark for (2850ds/14974Mi) % 159.55/23.14 % (1546990)Instruction limit reached! % 159.55/23.14 % (1546990)------------------------------ % 159.55/23.14 % (1546990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.55/23.14 % (1546990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.55/23.14 % (1546990)CaDiCaL version: 2.1.3 % 159.55/23.14 % (1546990)Termination reason: Instruction limit % 159.55/23.14 % (1546990)Termination phase: Saturation % 159.55/23.14 % (1546990)Time elapsed: 4.339 s % 159.55/23.14 % (1546990)Peak memory usage: 136 MB % 159.55/23.14 % (1546990)Instructions burned: 7144 (million) % 159.55/23.14 % (1547296)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=3320567513:i=33081:aac=none:fgj=on:bd=all:fsr=off_2847 on theBenchmark for (2847ds/33081Mi) % 159.55/23.14 % Exception at run slice level % 159.55/23.14 User error: GNN currently only supports monomorphic FOL. % 159.55/23.14 % (1547298)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=3666106296:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2845 on theBenchmark for (2845ds/50856Mi) % 159.55/23.14 % Exception at run slice level % 159.55/23.14 User error: GNN currently only supports monomorphic FOL. % 159.55/23.14 % (1547300)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=2866695357:i=69865_2842 on theBenchmark for (2842ds/69865Mi) % 159.55/23.14 % Exception at run slice level % 159.55/23.14 User error: GNN currently only supports monomorphic FOL. % 159.55/23.14 % (1547302)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=2587942536:cond=fast:i=17802:gtgl=3:gtg=all_2840 on theBenchmark for (2840ds/17802Mi) % 159.55/23.14 % Exception at run slice level % 171.72/24.93 User error: Immediate (shared) subterms of term/literal aa(X2,X0,combb(X1,X0,X2,X5,X4),X3) = sF7(X2,X0,X1,X5,X4,X3) have different types/not well-typed! % 171.72/24.93 % (1547304)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=3762067279:i=96644_2839 on theBenchmark for (2839ds/96644Mi) % 171.72/24.93 % Exception at run slice level % 171.72/24.93 User error: GNN currently only supports monomorphic FOL. % 171.72/24.93 % (1547306)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 171.72/24.93 % (1547306)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=2130443202:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2837 on theBenchmark for (2837ds/21161Mi) % 171.72/24.93 % (1547001)Instruction limit reached! % 171.72/24.93 % (1547001)------------------------------ % 171.72/24.93 % (1547001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.72/24.93 % (1547001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.72/24.93 % (1547001)CaDiCaL version: 2.1.3 % 171.72/24.93 % (1547001)Termination reason: Instruction limit % 171.72/24.93 % (1547001)Termination phase: Saturation % 171.72/24.93 % (1547001)Time elapsed: 4.669 s % 171.72/24.93 % (1547001)Peak memory usage: 128 MB % 171.72/24.93 % (1547001)Instructions burned: 8140 (million) % 171.72/24.93 % (1547168)Instruction limit reached! % 171.72/24.93 % (1547168)------------------------------ % 171.72/24.93 % (1547168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.72/24.93 % (1547168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.72/24.93 % (1547168)CaDiCaL version: 2.1.3 % 171.72/24.93 % (1547168)Termination reason: Instruction limit % 171.72/24.93 % (1547168)Termination phase: Saturation % 171.72/24.93 % (1547168)Time elapsed: 3.247 s % 171.72/24.93 % (1547168)Peak memory usage: 135 MB % 171.72/24.93 % (1547168)Instructions burned: 11103 (million) % 171.72/24.93 % (1547308)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=1277917085:i=22761:gtg=all:ss=axioms:fsd=on_2835 on theBenchmark for (2835ds/22761Mi) % 171.72/24.93 % (1547309)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=1185613408:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2835 on theBenchmark for (2835ds/23713Mi) % 171.72/24.93 % (1547309)Refutation not found, incomplete strategy % 171.72/24.93 % (1547309)------------------------------ % 171.72/24.93 % (1547309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.72/24.93 % (1547309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.72/24.93 % (1547309)CaDiCaL version: 2.1.3 % 171.72/24.93 % (1547309)Termination reason: Refutation not found, incomplete strategy % 171.72/24.93 % (1547309)Time elapsed: 0.004 s % 171.72/24.93 % (1547309)Peak memory usage: 88 MB % 171.72/24.93 % (1547309)Instructions burned: 10 (million) % 171.72/24.93 % (1547309)------------------------------ % 171.72/24.93 % (1547309)------------------------------ % 171.72/24.93 % (1547312)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=1184733678:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2832 on theBenchmark for (2832ds/26509Mi) % 171.72/24.93 % Exception at run slice level % 171.72/24.93 User error: GNN currently only supports monomorphic FOL. % 171.72/24.93 % Exception at run slice level % 171.72/24.93 User error: GNN currently only supports monomorphic FOL. % 171.72/24.93 % (1547314)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=251167785:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2830 on theBenchmark for (2830ds/28957Mi) % 171.72/24.93 % (1547315)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=3818600888:i=29246:s2at=-1:kws=inv_arity:ins=10_2829 on theBenchmark for (2829ds/29246Mi) % 171.72/24.93 % Exception at run slice level % 171.72/24.93 User error: GNN currently only supports monomorphic FOL. % 171.72/24.93 % (1547318)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=3261021704:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2826 on theBenchmark for (2826ds/30082Mi) % 179.07/25.95 % (1547318)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 179.07/25.95 % Exception at run slice level % 179.07/25.95 User error: GNN currently only supports monomorphic FOL. % 179.07/25.95 % (1547320)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=1529393137:i=32262:bd=preordered_2824 on theBenchmark for (2824ds/32262Mi) % 179.07/25.95 % Exception at run slice level % 179.07/25.95 User error: GNN currently only supports monomorphic FOL. % 179.07/25.95 % (1547322)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=646471645:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2821 on theBenchmark for (2821ds/32870Mi) % 179.07/25.95 % Exception at run slice level % 179.07/25.95 User error: GNN currently only supports monomorphic FOL. % 179.07/25.95 % (1547324)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=468850449:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2818 on theBenchmark for (2818ds/33295Mi) % 179.07/25.95 % Exception at run slice level % 179.07/25.95 User error: GNN currently only supports monomorphic FOL. % 179.07/25.95 % (1547326)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=4139677575:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2815 on theBenchmark for (2815ds/36826Mi) % 179.07/25.95 % (1546999)Instruction limit reached! % 179.07/25.95 % (1546999)------------------------------ % 179.07/25.95 % (1546999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 179.07/25.95 % (1546999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.07/25.95 % (1546999)CaDiCaL version: 2.1.3 % 179.07/25.95 % (1546999)Termination reason: Instruction limit % 179.07/25.95 % (1546999)Termination phase: Saturation % 179.07/25.95 % (1546999)Time elapsed: 7.874 s % 179.07/25.95 % (1546999)Peak memory usage: 146 MB % 179.07/25.95 % (1546999)Instructions burned: 15999 (million) % 179.07/25.95 % (1547328)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=4017808074:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2805 on theBenchmark for (2805ds/92981Mi) % 179.07/25.95 % Exception at run slice level % 179.07/25.95 User error: GNN currently only supports monomorphic FOL. % 179.07/25.95 % (1547330)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=1508507139:s2pl=on:i=49423_2800 on theBenchmark for (2800ds/49423Mi) % 179.07/25.95 % Exception at run slice level % 179.07/25.95 User error: GNN currently only supports monomorphic FOL. % 179.07/25.95 % (1547332)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=205211275:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2796 on theBenchmark for (2796ds/57299Mi) % 179.07/25.95 % Exception at run slice level % 179.07/25.95 User error: GNN currently only supports monomorphic FOL. % 179.07/25.95 % (1547334)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=1816721900:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2791 on theBenchmark for (2791ds/127679Mi) % 179.07/25.95 % Exception at run slice level % 179.07/25.95 User error: GNN currently only supports monomorphic FOL. % 179.07/25.95 % (1547336)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=2759156911:i=69402:add=on:aac=none:fsr=off_2786 on theBenchmark for (2786ds/69402Mi) % 179.07/25.95 % Exception at run slice level % 179.07/25.95 User error: GNN currently only supports monomorphic FOL. % 179.07/25.95 % (1547338)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=128603786:i=100512:doe=on:fgj=on:bd=all:fsd=on_2781 on theBenchmark for (2781ds/100512Mi) % 179.07/25.95 % Exception at run slice level % 179.07/25.95 User error: GNN currently only supports monomorphic FOL. % 179.07/25.95 % (1547340)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=4264540220:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2776 on theBenchmark for (2776ds/138761Mi) % 192.51/27.86 % Exception at run slice level % 192.51/27.86 User error: GNN currently only supports monomorphic FOL. % 192.51/27.86 % (1547342)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=1649722570:i=282386:rtra=on_2771 on theBenchmark for (2771ds/282386Mi) % 192.51/27.86 % (1546867)Instruction limit reached! % 192.51/27.86 % (1546867)------------------------------ % 192.51/27.86 % (1546867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.51/27.86 % (1546867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.51/27.86 % (1546867)CaDiCaL version: 2.1.3 % 192.51/27.86 % (1546867)Termination reason: Instruction limit % 192.51/27.86 % (1546867)Termination phase: Saturation % 192.51/27.86 % (1546867)Time elapsed: 19.417 s % 192.51/27.86 % (1546867)Peak memory usage: 244 MB % 192.51/27.86 % (1546867)Instructions burned: 33336 (million) % 192.51/27.86 % Exception at run slice level % 192.51/27.86 User error: GNN currently only supports monomorphic FOL. % 192.51/27.86 % (1547344)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=1082625842:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2767 on theBenchmark for (2767ds/269354Mi) % 192.51/27.86 % (1547345)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=1746911517:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2766 on theBenchmark for (2766ds/283390Mi) % 192.51/27.86 % (1547345)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 192.51/27.86 % Exception at run slice level % 192.51/27.86 User error: GNN currently only supports monomorphic FOL. % 192.51/27.86 % Exception at run slice level % 192.51/27.86 User error: GNN currently only supports monomorphic FOL. % 192.51/27.86 % (1547348)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=271189951:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2762 on theBenchmark for (2762ds/218Mi) % 192.51/27.86 % (1547348)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 192.51/27.86 % (1547349)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=2910551241:i=238:av=off:rtra=on:ss=axioms_2761 on theBenchmark for (2761ds/238Mi) % 192.51/27.86 % (1547348)Instruction limit reached! % 192.51/27.86 % (1547348)------------------------------ % 192.51/27.86 % (1547348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.51/27.86 % (1547348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.51/27.86 % (1547348)CaDiCaL version: 2.1.3 % 192.51/27.86 % (1547348)Termination reason: Instruction limit % 192.51/27.86 % (1547348)Termination phase: Saturation % 192.51/27.86 % (1547348)Time elapsed: 0.107 s % 192.51/27.86 % (1547348)Peak memory usage: 90 MB % 192.51/27.86 % (1547348)Instructions burned: 218 (million) % 192.51/27.86 % (1547349)Instruction limit reached! % 192.51/27.86 % (1547349)------------------------------ % 192.51/27.86 % (1547349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.51/27.86 % (1547349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.51/27.86 % (1547349)CaDiCaL version: 2.1.3 % 192.51/27.86 % (1547349)Termination reason: Instruction limit % 192.51/27.86 % (1547349)Termination phase: Saturation % 192.51/27.86 % (1547349)Time elapsed: 0.125 s % 192.51/27.86 % (1547349)Peak memory usage: 89 MB % 192.51/27.86 % (1547349)Instructions burned: 239 (million) % 192.51/27.86 % (1547352)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=4143267059:s2a=on:i=278:rtra=on:gtg=position_2760 on theBenchmark for (2760ds/278Mi) % 192.51/27.86 % (1547353)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=878822032:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2759 on theBenchmark for (2759ds/258Mi) % 192.51/27.86 % (1547352)Instruction limit reached! % 192.51/27.86 % (1547352)------------------------------ % 192.51/27.86 % (1547352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.51/27.86 % (1547352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.51/27.86 % (1547352)CaDiCaL version: 2.1.3 % 192.51/27.86 % (1547352)Termination reason: Instruction limit % 192.51/27.86 % (1547352)Termination phase: Saturation % 192.51/27.86 % (1547352)Time elapsed: 0.164 s % 197.45/28.53 % (1547352)Peak memory usage: 91 MB % 197.45/28.53 % (1547352)Instructions burned: 279 (million) % 197.45/28.53 % (1547353)Instruction limit reached! % 197.45/28.53 % (1547353)------------------------------ % 197.45/28.53 % (1547353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.45/28.53 % (1547353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.45/28.53 % (1547353)CaDiCaL version: 2.1.3 % 197.45/28.53 % (1547353)Termination reason: Instruction limit % 197.45/28.53 % (1547353)Termination phase: Saturation % 197.45/28.53 % (1547353)Time elapsed: 0.129 s % 197.45/28.53 % (1547353)Peak memory usage: 90 MB % 197.45/28.53 % (1547353)Instructions burned: 260 (million) % 197.45/28.53 % (1547356)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=3007081627:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2757 on theBenchmark for (2757ds/570Mi) % 197.45/28.53 % (1547357)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=3779361503:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2756 on theBenchmark for (2756ds/314Mi) % 197.45/28.53 % (1547357)Instruction limit reached! % 197.45/28.53 % (1547357)------------------------------ % 197.45/28.53 % (1547357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.45/28.53 % (1547357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.45/28.53 % (1547357)CaDiCaL version: 2.1.3 % 197.45/28.53 % (1547357)Termination reason: Instruction limit % 197.45/28.53 % (1547357)Termination phase: Saturation % 197.45/28.53 % (1547357)Time elapsed: 0.189 s % 197.45/28.53 % (1547357)Peak memory usage: 92 MB % 197.45/28.53 % (1547357)Instructions burned: 314 (million) % 197.45/28.53 % (1547356)Instruction limit reached! % 197.45/28.53 % (1547356)------------------------------ % 197.45/28.53 % (1547356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.45/28.53 % (1547356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.45/28.53 % (1547356)CaDiCaL version: 2.1.3 % 197.45/28.53 % (1547356)Termination reason: Instruction limit % 197.45/28.53 % (1547356)Termination phase: Saturation % 197.45/28.53 % (1547356)Time elapsed: 0.324 s % 197.45/28.53 % (1547356)Peak memory usage: 93 MB % 197.45/28.53 % (1547356)Instructions burned: 571 (million) % 197.45/28.53 % (1547360)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=1868600549:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2753 on theBenchmark for (2753ds/650Mi) % 197.45/28.53 % (1547361)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=2376148407:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2752 on theBenchmark for (2752ds/496Mi) % 197.45/28.53 % (1547361)Instruction limit reached! % 197.45/28.53 % (1547361)------------------------------ % 197.45/28.53 % (1547361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.45/28.53 % (1547361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.45/28.53 % (1547361)CaDiCaL version: 2.1.3 % 197.45/28.53 % (1547361)Termination reason: Instruction limit % 197.45/28.53 % (1547361)Termination phase: Saturation % 197.45/28.53 % (1547361)Time elapsed: 0.287 s % 197.45/28.53 % (1547361)Peak memory usage: 94 MB % 197.45/28.53 % (1547361)Instructions burned: 497 (million) % 197.45/28.53 % (1547360)Instruction limit reached! % 197.45/28.53 % (1547360)------------------------------ % 197.45/28.53 % (1547360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.45/28.53 % (1547360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.45/28.53 % (1547360)CaDiCaL version: 2.1.3 % 197.45/28.53 % (1547360)Termination reason: Instruction limit % 197.45/28.53 % (1547360)Termination phase: Saturation % 197.45/28.53 % (1547360)Time elapsed: 0.374 s % 197.45/28.53 % (1547360)Peak memory usage: 95 MB % 197.45/28.53 % (1547360)Instructions burned: 650 (million) % 197.45/28.53 % (1547365)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=1055501292:i=4700:rtra=on_2748 on theBenchmark for (2748ds/4700Mi) % 197.45/28.53 % (1547364)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=1635190176:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2748 on theBenchmark for (2748ds/588Mi) % 197.45/28.53 % (1547364)Refutation not found, incomplete strategy % 197.45/28.53 % (1547364)------------------------------ % 197.45/28.53 % (1547364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.45/28.53 % (1547364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.45/28.53 % (1547364)CaDiCaL version: 2.1.3 % 197.45/28.53 % (1547364)Termination reason: Refutation not found, incomplete strategy % 197.45/28.53 % (1547364)Time elapsed: 0.010 s % 203.40/29.46 % (1547364)Peak memory usage: 89 MB % 203.40/29.46 % (1547364)Instructions burned: 16 (million) % 203.40/29.46 % (1547364)------------------------------ % 203.40/29.46 % (1547364)------------------------------ % 203.40/29.46 % Exception at run slice level % 203.40/29.46 User error: GNN currently only supports monomorphic FOL. % 203.40/29.46 % (1547368)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2699314379:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2744 on theBenchmark for (2744ds/226Mi) % 203.40/29.46 % (1547369)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1440114227:i=254:av=off:fsr=off:rtra=on:sup=off_2743 on theBenchmark for (2743ds/254Mi) % 203.40/29.46 % (1547369)Refutation not found, incomplete strategy % 203.40/29.46 % (1547369)------------------------------ % 203.40/29.46 % (1547369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.40/29.46 % (1547369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.40/29.46 % (1547369)CaDiCaL version: 2.1.3 % 203.40/29.46 % (1547369)Termination reason: Refutation not found, incomplete strategy % 203.40/29.46 % (1547369)Time elapsed: 0.009 s % 203.40/29.46 % (1547369)Peak memory usage: 88 MB % 203.40/29.46 % (1547369)Instructions burned: 16 (million) % 203.40/29.46 % (1547368)Instruction limit reached! % 203.40/29.46 % (1547368)------------------------------ % 203.40/29.46 % (1547368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.40/29.46 % (1547368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.40/29.46 % (1547368)CaDiCaL version: 2.1.3 % 203.40/29.46 % (1547368)Termination reason: Instruction limit % 203.40/29.46 % (1547368)Termination phase: Saturation % 203.40/29.46 % (1547368)Time elapsed: 0.133 s % 203.40/29.46 % (1547368)Peak memory usage: 90 MB % 203.40/29.46 % (1547368)Instructions burned: 226 (million) % 203.40/29.46 % (1547372)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=4106247162:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2742 on theBenchmark for (2742ds/228Mi) % 203.40/29.46 % (1547369)------------------------------ % 203.40/29.46 % (1547369)------------------------------ % 203.40/29.46 % (1547372)Instruction limit reached! % 203.40/29.46 % (1547372)------------------------------ % 203.40/29.46 % (1547372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.40/29.46 % (1547372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.40/29.46 % (1547372)CaDiCaL version: 2.1.3 % 203.40/29.46 % (1547372)Termination reason: Instruction limit % 203.40/29.46 % (1547372)Termination phase: Saturation % 203.40/29.46 % (1547372)Time elapsed: 0.122 s % 203.40/29.46 % (1547372)Peak memory usage: 90 MB % 203.40/29.46 % (1547372)Instructions burned: 229 (million) % 203.40/29.46 % (1547374)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=3338249584:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2739 on theBenchmark for (2739ds/1814Mi) % 203.40/29.46 % (1547375)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=2688506526:i=874:sd=1:aac=none:rtra=on:ss=included_2739 on theBenchmark for (2739ds/874Mi) % 203.40/29.46 % (1547375)Refutation not found, incomplete strategy % 203.40/29.46 % (1547375)------------------------------ % 203.40/29.46 % (1547375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.40/29.46 % (1547375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.40/29.46 % (1547375)CaDiCaL version: 2.1.3 % 203.40/29.46 % (1547375)Termination reason: Refutation not found, incomplete strategy % 203.40/29.46 % (1547375)Time elapsed: 0.010 s % 203.40/29.46 % (1547375)Peak memory usage: 89 MB % 203.40/29.46 % (1547375)Instructions burned: 18 (million) % 203.40/29.46 % (1547375)------------------------------ % 203.40/29.46 % (1547375)------------------------------ % 203.40/29.46 % (1547378)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=4184504307:i=10404:rtra=on:ss=axioms:sgt=16_2735 on theBenchmark for (2735ds/10404Mi) % 203.40/29.46 % Exception at run slice level % 203.40/29.46 User error: GNN currently only supports monomorphic FOL. % 203.40/29.46 % (1547380)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1631846698:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2730 on theBenchmark for (2730ds/268Mi) % 203.40/29.46 % (1547380)Instruction limit reached! % 203.40/29.46 % (1547380)------------------------------ % 203.40/29.46 % (1547380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.40/29.46 % (1547380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.90/29.94 % (1547380)CaDiCaL version: 2.1.3 % 206.90/29.94 % (1547380)Termination reason: Instruction limit % 206.90/29.94 % (1547380)Termination phase: Saturation % 206.90/29.94 % (1547380)Time elapsed: 0.146 s % 206.90/29.94 % (1547380)Peak memory usage: 91 MB % 206.90/29.94 % (1547380)Instructions burned: 268 (million) % 206.90/29.94 % (1547374)Instruction limit reached! % 206.90/29.94 % (1547374)------------------------------ % 206.90/29.94 % (1547374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.90/29.94 % (1547374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.90/29.94 % (1547374)CaDiCaL version: 2.1.3 % 206.90/29.94 % (1547374)Termination reason: Instruction limit % 206.90/29.94 % (1547374)Termination phase: Saturation % 206.90/29.94 % (1547374)Time elapsed: 1.068 s % 206.90/29.94 % (1547374)Peak memory usage: 108 MB % 206.90/29.94 % (1547374)Instructions burned: 1814 (million) % 206.90/29.94 % (1547382)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=279668945:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2728 on theBenchmark for (2728ds/1184Mi) % 206.90/29.94 % (1547383)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=3465309647:st=3:i=26386:sd=3:rtra=on:ss=axioms_2727 on theBenchmark for (2727ds/26386Mi) % 206.90/29.94 % (1547306)Instruction limit reached! % 206.90/29.94 % (1547306)------------------------------ % 206.90/29.94 % (1547306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.90/29.94 % (1547306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.90/29.94 % (1547306)CaDiCaL version: 2.1.3 % 206.90/29.94 % (1547306)Termination reason: Instruction limit % 206.90/29.94 % (1547306)Termination phase: Saturation % 206.90/29.94 % (1547306)Time elapsed: 11.003 s % 206.90/29.94 % (1547306)Peak memory usage: 215 MB % 206.90/29.94 % (1547306)Instructions burned: 21162 (million) % 206.90/29.94 % (1547386)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=2801579287:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2725 on theBenchmark for (2725ds/250Mi) % 206.90/29.94 % (1547386)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 206.90/29.94 % (1547386)Instruction limit reached! % 206.90/29.94 % (1547386)------------------------------ % 206.90/29.94 % (1547386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.90/29.94 % (1547386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.90/29.94 % (1547386)CaDiCaL version: 2.1.3 % 206.90/29.94 % (1547386)Termination reason: Instruction limit % 206.90/29.94 % (1547386)Termination phase: Saturation % 206.90/29.94 % (1547386)Time elapsed: 0.143 s % 206.90/29.94 % (1547386)Peak memory usage: 91 MB % 206.90/29.94 % (1547386)Instructions burned: 251 (million) % 206.90/29.94 % Exception at run slice level % 206.90/29.94 User error: GNN currently only supports monomorphic FOL. % 206.90/29.94 % (1547388)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=2780804167:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2723 on theBenchmark for (2723ds/268Mi) % 206.90/29.94 % Exception at run slice level % 206.90/29.94 User error: Immediate (shared) subterms of term/literal aa(X1,X2,combs(X1,X0,X2,X3,X5),X4) = sF0(X1,X2,X0,X3,X5,X4) have different types/not well-typed! % 206.90/29.94 % (1547389)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2584801065:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2722 on theBenchmark for (2722ds/282Mi) % 206.90/29.94 % (1547389)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 206.90/29.94 % (1547389)Refutation not found, incomplete strategy % 206.90/29.94 % (1547389)------------------------------ % 206.90/29.94 % (1547389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.90/29.94 % (1547389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.90/29.94 % (1547389)CaDiCaL version: 2.1.3 % 206.90/29.94 % (1547389)Termination reason: Refutation not found, incomplete strategy % 206.90/29.94 % (1547389)Time elapsed: 0.003 s % 206.90/29.94 % (1547389)Peak memory usage: 88 MB % 206.90/29.94 % (1547389)Instructions burned: 4 (million) % 206.90/29.94 % (1547382)Instruction limit reached! % 206.90/29.94 % (1547382)------------------------------ % 206.90/29.94 % (1547382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.90/29.94 % (1547382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.59/31.83 % (1547382)CaDiCaL version: 2.1.3 % 219.59/31.83 % (1547382)Termination reason: Instruction limit % 219.59/31.83 % (1547382)Termination phase: Saturation % 219.59/31.83 % (1547382)Time elapsed: 0.550 s % 219.59/31.83 % (1547382)Peak memory usage: 91 MB % 219.59/31.83 % (1547382)Instructions burned: 1184 (million) % 219.59/31.83 % (1547391)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=489398637:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2721 on theBenchmark for (2721ds/862Mi) % 219.59/31.83 % (1547391)Refutation not found, incomplete strategy % 219.59/31.83 % (1547391)------------------------------ % 219.59/31.83 % (1547391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.59/31.83 % (1547391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.59/31.83 % (1547391)CaDiCaL version: 2.1.3 % 219.59/31.83 % (1547391)Termination reason: Refutation not found, incomplete strategy % 219.59/31.83 % (1547391)Time elapsed: 0.009 s % 219.59/31.83 % (1547391)Peak memory usage: 89 MB % 219.59/31.83 % (1547391)Instructions burned: 15 (million) % 219.59/31.83 % (1547393)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=2761242984:i=12120:aac=none:ins=25:rtra=on_2721 on theBenchmark for (2721ds/12120Mi) % 219.59/31.83 % (1547389)------------------------------ % 219.59/31.83 % (1547389)------------------------------ % 219.59/31.83 % (1547391)------------------------------ % 219.59/31.83 % (1547391)------------------------------ % 219.59/31.83 % (1547396)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=3619201084:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2719 on theBenchmark for (2719ds/300Mi) % 219.59/31.83 % (1547396)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 219.59/31.83 % (1547397)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=1601543948:i=28310:bd=all:rtra=on_2717 on theBenchmark for (2717ds/28310Mi) % 219.59/31.83 % Exception at run slice level % 219.59/31.83 User error: GNN currently only supports monomorphic FOL. % 219.59/31.83 % (1547396)Instruction limit reached! % 219.59/31.83 % (1547396)------------------------------ % 219.59/31.83 % (1547396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.59/31.83 % (1547396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.59/31.83 % (1547396)CaDiCaL version: 2.1.3 % 219.59/31.83 % (1547396)Termination reason: Instruction limit % 219.59/31.83 % (1547396)Termination phase: Saturation % 219.59/31.83 % (1547396)Time elapsed: 0.188 s % 219.59/31.83 % (1547396)Peak memory usage: 92 MB % 219.59/31.83 % (1547396)Instructions burned: 300 (million) % 219.59/31.83 % (1547400)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=709546268:i=1334:av=off:fsr=off:rtra=on_2716 on theBenchmark for (2716ds/1334Mi) % 219.59/31.83 % (1547400)Refutation not found, incomplete strategy % 219.59/31.83 % (1547400)------------------------------ % 219.59/31.83 % (1547400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.59/31.83 % (1547400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.59/31.83 % (1547400)CaDiCaL version: 2.1.3 % 219.59/31.83 % (1547400)Termination reason: Refutation not found, incomplete strategy % 219.59/31.83 % (1547400)Time elapsed: 0.011 s % 219.59/31.83 % (1547400)Peak memory usage: 89 MB % 219.59/31.83 % (1547400)Instructions burned: 18 (million) % 219.59/31.83 % (1547401)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=232831202:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2715 on theBenchmark for (2715ds/370Mi) % 219.59/31.83 % Exception at run slice level % 219.59/31.83 User error: GNN currently only supports monomorphic FOL. % 219.59/31.83 % (1547400)------------------------------ % 219.59/31.83 % (1547400)------------------------------ % 219.59/31.83 % (1547401)Instruction limit reached! % 219.59/31.83 % (1547401)------------------------------ % 219.59/31.83 % (1547401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.59/31.83 % (1547401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.59/31.83 % (1547401)CaDiCaL version: 2.1.3 % 219.59/31.83 % (1547401)Termination reason: Instruction limit % 219.59/31.83 % (1547401)Termination phase: Saturation % 231.02/33.33 % (1547401)Time elapsed: 0.237 s % 231.02/33.33 % (1547401)Peak memory usage: 92 MB % 231.02/33.33 % (1547401)Instructions burned: 370 (million) % 231.02/33.33 % (1547404)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=1003645489:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2712 on theBenchmark for (2712ds/386Mi) % 231.02/33.33 % (1547326)Instruction limit reached! % 231.02/33.33 % (1547326)------------------------------ % 231.02/33.33 % (1547326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.02/33.33 % (1547326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.02/33.33 % (1547326)CaDiCaL version: 2.1.3 % 231.02/33.33 % (1547326)Termination reason: Instruction limit % 231.02/33.33 % (1547326)Termination phase: Saturation % 231.02/33.33 % (1547326)Time elapsed: 10.340 s % 231.02/33.33 % (1547326)Peak memory usage: 279 MB % 231.02/33.33 % (1547326)Instructions burned: 36830 (million) % 231.02/33.33 % (1547405)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=1594611459:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2712 on theBenchmark for (2712ds/9700Mi) % 231.02/33.33 % (1547405)Refutation not found, incomplete strategy % 231.02/33.33 % (1547405)------------------------------ % 231.02/33.33 % (1547405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.02/33.33 % (1547405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.02/33.33 % (1547405)CaDiCaL version: 2.1.3 % 231.02/33.33 % (1547405)Termination reason: Refutation not found, incomplete strategy % 231.02/33.33 % (1547405)Time elapsed: 0.008 s % 231.02/33.33 % (1547405)Peak memory usage: 88 MB % 231.02/33.33 % (1547405)Instructions burned: 14 (million) % 231.02/33.33 % (1547406)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=1805746216:i=24222:sd=1:rtra=on:ss=included_2712 on theBenchmark for (2712ds/24222Mi) % 231.02/33.33 % (1547409)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=2821315975:i=638:kws=precedence:fsr=off:rtra=on_2711 on theBenchmark for (2711ds/638Mi) % 231.02/33.33 % (1547404)Instruction limit reached! % 231.02/33.33 % (1547404)------------------------------ % 231.02/33.33 % (1547404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.02/33.33 % (1547404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.02/33.33 % (1547404)CaDiCaL version: 2.1.3 % 231.02/33.33 % (1547404)Termination reason: Instruction limit % 231.02/33.33 % (1547404)Termination phase: Saturation % 231.02/33.33 % (1547404)Time elapsed: 0.229 s % 231.02/33.33 % (1547404)Peak memory usage: 91 MB % 231.02/33.33 % (1547404)Instructions burned: 387 (million) % 231.02/33.33 % (1547405)------------------------------ % 231.02/33.33 % (1547405)------------------------------ % 231.02/33.33 % (1547409)Instruction limit reached! % 231.02/33.33 % (1547409)------------------------------ % 231.02/33.33 % (1547409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.02/33.33 % (1547409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.02/33.33 % (1547409)CaDiCaL version: 2.1.3 % 231.02/33.33 % (1547409)Termination reason: Instruction limit % 231.02/33.33 % (1547409)Termination phase: Saturation % 231.02/33.33 % (1547409)Time elapsed: 0.199 s % 231.02/33.33 % (1547409)Peak memory usage: 94 MB % 231.02/33.33 % (1547409)Instructions burned: 640 (million) % 231.02/33.33 % (1547412)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3196337130:i=4128:ep=RST:rtra=on_2709 on theBenchmark for (2709ds/4128Mi) % 231.02/33.33 % (1547413)dis-1011_128_sil=32000:si=on:random_seed=1576503332:i=7412:ep=RST:av=off:rtra=on_2708 on theBenchmark for (2708ds/7412Mi) % 231.02/33.33 % (1547414)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1744595085:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2708 on theBenchmark for (2708ds/1514Mi) % 231.02/33.33 % Exception at run slice level % 231.02/33.33 User error: GNN currently only supports monomorphic FOL. % 231.02/33.33 % (1547414)Refutation not found, incomplete strategy % 231.02/33.33 % (1547414)------------------------------ % 231.02/33.33 % (1547414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.02/33.33 % (1547414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.02/33.33 % (1547414)CaDiCaL version: 2.1.3 % 231.02/33.33 % (1547414)Termination reason: Refutation not found, incomplete strategy % 231.02/33.33 % (1547414)Time elapsed: 0.005 s % 231.02/33.33 % (1547414)Peak memory usage: 89 MB % 241.53/34.97 % (1547414)Instructions burned: 17 (million) % 241.53/34.97 % (1547418)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=1319799649:i=27826:rtra=on:ss=axioms:sgt=8_2707 on theBenchmark for (2707ds/27826Mi) % 241.53/34.97 % (1547414)------------------------------ % 241.53/34.97 % (1547414)------------------------------ % 241.53/34.97 % (1547420)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=3444807230:i=19850:aac=none:rtra=on_2705 on theBenchmark for (2705ds/19850Mi) % 241.53/34.97 % Exception at run slice level % 241.53/34.97 User error: GNN currently only supports monomorphic FOL. % 241.53/34.97 % Exception at run slice level % 241.53/34.97 User error: GNN currently only supports monomorphic FOL. % 241.53/34.97 % (1547422)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2422456777:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2702 on theBenchmark for (2702ds/4958Mi) % 241.53/34.97 % (1547422)Refutation not found, incomplete strategy % 241.53/34.97 % (1547422)------------------------------ % 241.53/34.97 % (1547422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.53/34.97 % (1547422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.53/34.97 % (1547422)CaDiCaL version: 2.1.3 % 241.53/34.97 % (1547422)Termination reason: Refutation not found, incomplete strategy % 241.53/34.97 % (1547422)Time elapsed: 0.005 s % 241.53/34.97 % (1547422)Peak memory usage: 89 MB % 241.53/34.97 % (1547422)Instructions burned: 13 (million) % 241.53/34.97 % (1547423)ott+1002_64_sil=16000:si=on:sp=const_min:nwc=0.5:random_seed=2223834171:i=880:nm=2:av=off:rtra=on:gtg=exists_all:fdi=8:gsp=on_2702 on theBenchmark for (2702ds/880Mi) % 241.53/34.97 % (1547423)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 241.53/34.97 % (1547422)------------------------------ % 241.53/34.97 % (1547422)------------------------------ % 241.53/34.97 % (1547426)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=1142071178:st=1.5:i=22290:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2699 on theBenchmark for (2699ds/22290Mi) % 241.53/34.97 % Exception at run slice level % 241.53/34.97 User error: GNN currently only supports monomorphic FOL. % 241.53/34.97 % (1547423)Instruction limit reached! % 241.53/34.97 % (1547423)------------------------------ % 241.53/34.97 % (1547423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.53/34.97 % (1547423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.53/34.97 % (1547423)CaDiCaL version: 2.1.3 % 241.53/34.97 % (1547423)Termination reason: Instruction limit % 241.53/34.97 % (1547423)Termination phase: Saturation % 241.53/34.97 % (1547423)Time elapsed: 0.469 s % 241.53/34.97 % (1547423)Peak memory usage: 98 MB % 241.53/34.97 % (1547423)Instructions burned: 880 (million) % 241.53/34.97 % (1547428)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=4097474598:cts=off:i=6068:av=off:rtra=on:er=known:fsd=on_2696 on theBenchmark for (2696ds/6068Mi) % 241.53/34.97 % (1547429)lrs-1011_64:1_sil=8000:si=on:erd=off:urr=on:nwc=0.7:br=off:random_seed=4132700083:st=2:s2a=on:i=1048:s2at=2:rtra=on:ss=axioms_2696 on theBenchmark for (2696ds/1048Mi) % 241.53/34.97 % Exception at run slice level % 241.53/34.97 User error: GNN currently only supports monomorphic FOL. % 241.53/34.97 % (1547432)lrs+1011_16:1_sil=8000:si=on:acc=on:urr=on:fd=preordered:flr=on:random_seed=2026103867:avsq=on:i=2032:avsqr=676809,524288:sd=1:rtra=on:ss=axioms_2693 on theBenchmark for (2693ds/2032Mi) % 241.53/34.97 % (1547412)Instruction limit reached! % 241.53/34.97 % (1547412)------------------------------ % 241.53/34.97 % (1547412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.53/34.97 % (1547412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.53/34.97 % (1547412)CaDiCaL version: 2.1.3 % 241.53/34.97 % (1547412)Termination reason: Instruction limit % 241.53/34.97 % (1547412)Termination phase: Saturation % 241.53/34.97 % (1547412)Time elapsed: 1.735 s % 241.53/34.97 % (1547412)Peak memory usage: 94 MB % 241.53/34.97 % (1547412)Instructions burned: 4129 (million) % 241.53/34.97 % (1547434)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:si=on:s2agt=16:random_seed=1152706363:i=28246:bd=preordered:ins=4:rtra=on_2690 on theBenchmark for (2690ds/28246Mi) % 241.53/34.97 % (1547429)Instruction limit reached! % 252.21/36.32 % (1547429)------------------------------ % 252.21/36.32 % (1547429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.21/36.32 % (1547429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.21/36.32 % (1547429)CaDiCaL version: 2.1.3 % 252.21/36.32 % (1547429)Termination reason: Instruction limit % 252.21/36.32 % (1547429)Termination phase: Saturation % 252.21/36.32 % (1547429)Time elapsed: 0.638 s % 252.21/36.32 % (1547429)Peak memory usage: 101 MB % 252.21/36.32 % (1547429)Instructions burned: 1048 (million) % 252.21/36.32 % (1547436)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:si=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3636348605:i=11562:kws=precedence:bd=all:rtra=on:rawr=on_2688 on theBenchmark for (2688ds/11562Mi) % 252.21/36.32 % (1547432)Instruction limit reached! % 252.21/36.32 % (1547432)------------------------------ % 252.21/36.32 % (1547432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.21/36.32 % (1547432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.21/36.32 % (1547432)CaDiCaL version: 2.1.3 % 252.21/36.32 % (1547432)Termination reason: Instruction limit % 252.21/36.32 % (1547432)Termination phase: Saturation % 252.21/36.32 % (1547432)Time elapsed: 0.654 s % 252.21/36.32 % (1547432)Peak memory usage: 109 MB % 252.21/36.32 % (1547432)Instructions burned: 2034 (million) % 252.21/36.32 % Exception at run slice level % 252.21/36.32 User error: GNN currently only supports monomorphic FOL. % 252.21/36.32 % (1547438)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=4227011241:i=4896:gtgl=5:bd=preordered:rtra=on:gtg=all_2686 on theBenchmark for (2686ds/4896Mi) % 252.21/36.32 % (1547439)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:si=on:lcm=reverse:random_seed=2954956464:i=6446:kws=precedence:fgj=on:av=off:rtra=on_2685 on theBenchmark for (2685ds/6446Mi) % 252.21/36.32 % Exception at run slice level % 252.21/36.32 User error: GNN currently only supports monomorphic FOL. % 252.21/36.32 % (1547442)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:si=on:sp=occurrence:sos=on:random_seed=306300701:st=5.6:i=4066:sd=3:rtra=on:ss=axioms_2683 on theBenchmark for (2683ds/4066Mi) % 252.21/36.32 % Exception at run slice level % 252.21/36.32 User error: GNN currently only supports monomorphic FOL. % 252.21/36.32 % Exception at run slice level % 252.21/36.32 User error: GNN currently only supports monomorphic FOL. % 252.21/36.32 % (1547444)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:si=on:random_seed=3251132398:i=4110:nm=16:rtra=on:gtg=position:ss=axioms:fsd=on_2679 on theBenchmark for (2679ds/4110Mi) % 252.21/36.32 % (1547445)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=2869880665:i=43222:sd=3:rtra=on:ss=axioms_2678 on theBenchmark for (2678ds/43222Mi) % 252.21/36.32 % (1547413)Instruction limit reached! % 252.21/36.32 % (1547413)------------------------------ % 252.21/36.32 % (1547413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.21/36.32 % (1547413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.21/36.32 % (1547413)CaDiCaL version: 2.1.3 % 252.21/36.32 % (1547413)Termination reason: Instruction limit % 252.21/36.32 % (1547413)Termination phase: Saturation % 252.21/36.32 % (1547413)Time elapsed: 2.975 s % 252.21/36.32 % (1547413)Peak memory usage: 93 MB % 252.21/36.32 % (1547413)Instructions burned: 7414 (million) % 252.21/36.32 % (1547448)lrs+10_1_sil=8000:si=on:sp=occurrence:sos=all:lma=off:random_seed=1492178987:i=9670:sd=13:rtra=on:ss=axioms:sgt=23_2677 on theBenchmark for (2677ds/9670Mi) % 252.21/36.32 % Exception at run slice level % 252.21/36.32 User error: GNN currently only supports monomorphic FOL. % 252.21/36.32 % Exception at run slice level % 252.21/36.32 User error: GNN currently only supports monomorphic FOL. % 252.21/36.32 % (1547450)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=3943033555:st=5:i=1594:s2at=3:sd=4:bs=unit_only:av=off:rtra=on:sup=off:ss=included_2675 on theBenchmark for (2675ds/1594Mi) % 252.21/36.32 % (1547452)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=775717546:i=4652:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:rtra=on:fsd=on_2674 on theBenchmark for (2674ds/4652Mi) % 252.21/36.32 % (1547452)Refutation not found, incomplete strategy % 252.21/36.32 % (1547452)------------------------------ % 268.03/38.52 % (1547452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.03/38.52 % (1547452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.03/38.52 % (1547452)CaDiCaL version: 2.1.3 % 268.03/38.52 % (1547452)Termination reason: Refutation not found, incomplete strategy % 268.03/38.52 % (1547452)Time elapsed: 0.014 s % 268.03/38.52 % (1547452)Peak memory usage: 89 MB % 268.03/38.52 % (1547452)Instructions burned: 22 (million) % 268.03/38.52 % (1547314)Instruction limit reached! % 268.03/38.52 % (1547314)------------------------------ % 268.03/38.52 % (1547314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.03/38.52 % (1547314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.03/38.52 % (1547314)CaDiCaL version: 2.1.3 % 268.03/38.52 % (1547314)Termination reason: Instruction limit % 268.03/38.52 % (1547314)Termination phase: Saturation % 268.03/38.52 % (1547314)Time elapsed: 15.675 s % 268.03/38.52 % (1547314)Peak memory usage: 259 MB % 268.03/38.52 % (1547314)Instructions burned: 28957 (million) % 268.03/38.52 % (1547454)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:si=on:sos=all:urr=on:br=off:random_seed=983328447:i=12076:nm=6:rtra=on_2672 on theBenchmark for (2672ds/12076Mi) % 268.03/38.52 % (1547452)------------------------------ % 268.03/38.52 % (1547452)------------------------------ % 268.03/38.52 % (1547450)Instruction limit reached! % 268.03/38.52 % (1547450)------------------------------ % 268.03/38.52 % (1547450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.03/38.52 % (1547450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.03/38.52 % (1547450)CaDiCaL version: 2.1.3 % 268.03/38.52 % (1547450)Termination reason: Instruction limit % 268.03/38.52 % (1547450)Termination phase: Saturation % 268.03/38.52 % (1547450)Time elapsed: 0.416 s % 268.03/38.52 % (1547450)Peak memory usage: 157 MB % 268.03/38.52 % (1547450)Instructions burned: 1597 (million) % 268.03/38.52 % (1547457)lrs+10_4_sil=8000:plsq=on:si=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=649409654:st=3.7:s2a=on:i=2016:s2at=1.2:sd=3:bd=all:av=off:rtra=on:fdi=8:sup=off:ss=axioms_2670 on theBenchmark for (2670ds/2016Mi) % 268.03/38.52 % (1547456)lrs+10_1_sil=32000:si=on:sp=occurrence:random_seed=4244430992:st=2:i=66668:sd=3:rtra=on:ss=included:sgt=32_2670 on theBenchmark for (2670ds/66668Mi) % 268.03/38.52 % Exception at run slice level % 268.03/38.52 User error: GNN currently only supports monomorphic FOL. % 268.03/38.52 % (1547460)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=2349071554:i=16654:s2at=5:bd=preordered:rtra=on_2667 on theBenchmark for (2667ds/16654Mi) % 268.03/38.52 % (1547457)Instruction limit reached! % 268.03/38.52 % (1547457)------------------------------ % 268.03/38.52 % (1547457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.03/38.52 % (1547457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.03/38.52 % (1547457)CaDiCaL version: 2.1.3 % 268.03/38.52 % (1547457)Termination reason: Instruction limit % 268.03/38.52 % (1547457)Termination phase: Saturation % 268.03/38.52 % (1547457)Time elapsed: 0.547 s % 268.03/38.52 % (1547457)Peak memory usage: 105 MB % 268.03/38.52 % (1547457)Instructions burned: 2021 (million) % 268.03/38.52 % (1547462)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=2785672289:s2a=on:i=2166:s2at=1.87328:slsql=off:ep=RSTC:rtra=on:fdi=16_2664 on theBenchmark for (2664ds/2166Mi) % 268.03/38.52 % Exception at run slice level % 268.03/38.52 User error: GNN currently only supports monomorphic FOL. % 268.03/38.52 % (1547464)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:si=on:spb=goal:fd=preordered:random_seed=2692070940:i=2168:sd=1:bd=preordered:av=off:fsr=off:rtra=on:ss=axioms:sgt=14_2662 on theBenchmark for (2662ds/2168Mi) % 268.03/38.52 % (1547462)Instruction limit reached! % 268.03/38.52 % (1547462)------------------------------ % 268.03/38.52 % (1547462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.03/38.52 % (1547462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.03/38.52 % (1547462)CaDiCaL version: 2.1.3 % 268.03/38.52 % (1547462)Termination reason: Instruction limit % 268.03/38.52 % (1547462)Termination phase: Saturation % 268.03/38.52 % (1547462)Time elapsed: 0.628 s % 268.03/38.52 % (1547462)Peak memory usage: 103 MB % 268.03/38.52 % (1547462)Instructions burned: 2169 (million) % 279.11/40.06 % (1547466)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=484180570:i=13990:s2at=5:rtra=on:gtg=all_2656 on theBenchmark for (2656ds/13990Mi) % 279.11/40.06 % (1546961)Instruction limit reached! % 279.11/40.06 % (1546961)------------------------------ % 279.11/40.06 % (1546961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.11/40.06 % (1546961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.11/40.06 % (1546961)CaDiCaL version: 2.1.3 % 279.11/40.06 % (1546961)Termination reason: Instruction limit % 279.11/40.06 % (1546961)Termination phase: Saturation % 279.11/40.06 % (1546961)Time elapsed: 25.262 s % 279.11/40.06 % (1546961)Peak memory usage: 254 MB % 279.11/40.06 % (1546961)Instructions burned: 43697 (million) % 279.11/40.06 % (1547468)lrs+10_1_sil=32000:si=on:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=4159999974:st=2:i=12450:sd=15:rtra=on:ss=axioms_2655 on theBenchmark for (2655ds/12450Mi) % 279.11/40.06 % Exception at run slice level % 279.11/40.06 User error: GNN currently only supports monomorphic FOL. % 279.11/40.06 % (1547468)Refutation not found, incomplete strategy % 279.11/40.06 % (1547468)------------------------------ % 279.11/40.06 % (1547468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.11/40.06 % (1547468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.11/40.06 % (1547468)CaDiCaL version: 2.1.3 % 279.11/40.06 % (1547468)Termination reason: Refutation not found, incomplete strategy % 279.11/40.06 % (1547468)Time elapsed: 0.008 s % 279.11/40.06 % (1547468)Peak memory usage: 89 MB % 279.11/40.06 % (1547468)Instructions burned: 13 (million) % 279.11/40.06 % (1547470)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:si=on:lcm=reverse:random_seed=2368485264:cond=fast:i=6744:sd=1:nm=16:rtra=on:gtg=position:ss=axioms_2654 on theBenchmark for (2654ds/6744Mi) % 279.11/40.06 % (1547468)------------------------------ % 279.11/40.06 % (1547468)------------------------------ % 279.11/40.06 % Exception at run slice level % 279.11/40.06 User error: GNN currently only supports monomorphic FOL. % 279.11/40.06 % (1547473)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=3209173381:i=26988:s2at=1.31:bd=all:ins=10:rtra=on:gtg=exists_top_2651 on theBenchmark for (2651ds/26988Mi) % 279.11/40.06 % (1547472)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sos=all:random_seed=2969000389:st=2.3:i=52914:sd=10:rtra=on:ss=included:sgt=8_2651 on theBenchmark for (2651ds/52914Mi) % 279.11/40.06 % (1547464)Instruction limit reached! % 279.11/40.06 % (1547464)------------------------------ % 279.11/40.06 % (1547464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.11/40.06 % (1547464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.11/40.06 % (1547464)CaDiCaL version: 2.1.3 % 279.11/40.06 % (1547464)Termination reason: Instruction limit % 279.11/40.06 % (1547464)Termination phase: Saturation % 279.11/40.06 % (1547464)Time elapsed: 1.290 s % 279.11/40.06 % (1547464)Peak memory usage: 109 MB % 279.11/40.06 % (1547464)Instructions burned: 2169 (million) % 279.11/40.06 % Exception at run slice level % 279.11/40.06 User error: GNN currently only supports monomorphic FOL. % 279.11/40.06 % (1547477)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:si=on:sos=on:lsd=10:random_seed=3015278024:i=5118:sd=1:ep=RSTC:rtra=on:ss=axioms_2648 on theBenchmark for (2648ds/5118Mi) % 279.11/40.06 % (1547476)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=95619453:i=5006:nm=4:rtra=on:gsp=on:ss=axioms:sgt=15_2648 on theBenchmark for (2648ds/5006Mi) % 279.11/40.06 % (1547476)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 279.11/40.06 % Exception at run slice level % 279.11/40.06 User error: GNN currently only supports monomorphic FOL. % 279.11/40.06 % Exception at run slice level % 279.11/40.06 User error: GNN currently only supports monomorphic FOL. % 279.11/40.06 % (1547480)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:si=on:fdtod=off:random_seed=2398326655:i=61506:av=off:rtra=on:ss=included_2646 on theBenchmark for (2646ds/61506Mi) % 279.11/40.06 % (1547481)lrs+10_1024_sil=64000:plsq=on:plsqc=4:si=on:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=1558173171:i=52946:ep=RSTC:rtra=on_2645 on theBenchmark for (2645ds/52946Mi) % 291.26/42.04 % Exception at run slice level % 291.26/42.04 User error: GNN currently only supports monomorphic FOL. % 291.26/42.04 % (1547484)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=3265677217:cts=off:i=5518:kws=inv_arity:fgj=on:rtra=on_2643 on theBenchmark for (2643ds/5518Mi) % 291.26/42.04 % Exception at run slice level % 291.26/42.04 User error: GNN currently only supports monomorphic FOL. % 291.26/42.04 % (1547486)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=238614713:st=1.2:i=11330:sd=2:ep=RSTC:rtra=on:gsp=on:ss=axioms_2641 on theBenchmark for (2641ds/11330Mi) % 291.26/42.04 % (1547486)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 291.26/42.04 % Exception at run slice level % 291.26/42.04 User error: GNN currently only supports monomorphic FOL. % 291.26/42.04 % (1547488)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=474642366:i=3064:ep=RS:rtra=on:ss=axioms_2638 on theBenchmark for (2638ds/3064Mi) % 291.26/42.04 % Exception at run slice level % 291.26/42.04 User error: GNN currently only supports monomorphic FOL. % 291.26/42.04 % (1547490)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=204367628:i=3130:sd=2:rtra=on:ss=axioms:sgt=32_2636 on theBenchmark for (2636ds/3130Mi) % 291.26/42.04 % Exception at run slice level % 291.26/42.04 User error: GNN currently only supports monomorphic FOL. % 291.26/42.04 % (1547492)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=1739714731:i=3144:fgj=on:rtra=on:gsp=on_2633 on theBenchmark for (2633ds/3144Mi) % 291.26/42.04 % (1547492)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 291.26/42.04 % Exception at run slice level % 291.26/42.04 User error: GNN currently only supports monomorphic FOL. % 291.26/42.04 % (1547494)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:si=on:sp=occurrence:sos=on:newcnf=on:random_seed=1885421262:i=12104:sd=4:rtra=on:ss=axioms:sgt=24_2631 on theBenchmark for (2631ds/12104Mi) % 291.26/42.04 % Exception at run slice level % 291.26/42.04 User error: GNN currently only supports monomorphic FOL. % 291.26/42.04 % (1547496)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=1384293382:i=7000:sd=1:bd=preordered:rtra=on:sup=off:ss=included_2628 on theBenchmark for (2628ds/7000Mi) % 291.26/42.04 % Exception at run slice level % 291.26/42.04 User error: GNN currently only supports monomorphic FOL. % 291.26/42.04 % (1547498)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=109076090:i=3684:sd=3:fgj=on:rtra=on:gtg=position:gsp=on:ss=axioms:sgt=20_2626 on theBenchmark for (2626ds/3684Mi) % 291.26/42.04 % (1547498)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 291.26/42.04 % Exception at run slice level % 291.26/42.04 User error: GNN currently only supports monomorphic FOL. % 291.26/42.04 % (1547500)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:si=on:bsr=unit_only:random_seed=2537587025:i=132192:add=on:rtra=on_2623 on theBenchmark for (2623ds/132192Mi) % 291.26/42.04 % (1547436)Instruction limit reached! % 291.26/42.04 % (1547436)------------------------------ % 291.26/42.04 % (1547436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.26/42.04 % (1547436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.26/42.04 % (1547436)CaDiCaL version: 2.1.3 % 291.26/42.04 % (1547436)Termination reason: Instruction limit % 291.26/42.04 % (1547436)Termination phase: Saturation % 291.26/42.04 % (1547436)Time elapsed: 6.486 s % 291.26/42.04 % (1547436)Peak memory usage: 157 MB % 291.26/42.04 % (1547436)Instructions burned: 11563 (million) % 291.26/42.04 % Exception at run slice level % 291.26/42.04 User error: GNN currently only supports monomorphic FOL. % 291.26/42.04 % (1547448)Instruction limit reached! % 291.26/42.04 % (1547448)------------------------------ % 291.26/42.04 % (1547448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16Terminated %------------------------------------------------------------------------------