%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : LCL752_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 : n019.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 11:56:27 AM UTC 2026 % Result : Timeout 300.36s 43.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL752_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.11/0.38 % Computer : n019.cluster.edu % 0.11/0.38 % Model : x86_64 x86_64 % 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.38 % Memory : 8046.5625MB % 0.11/0.38 % OS : Linux 6.8.0-71-generic % 0.11/0.38 % CPULimit : 300 % 0.11/0.38 % WCLimit : 300 % 0.11/0.38 % DateTime : Sun Sep 27 16:44:34 UTC 2026 % 0.11/0.38 % CPUTime : % 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.11/0.42 Running first-order theorem proving % 0.11/0.42 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 % 4.77/1.79 % (3253443)Detected formulas, will run a generic FOF schedule. % 4.77/1.79 % (3253454)dis-21_1_sil=8000:lcm=predicate:random_seed=3758997691: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) % 4.77/1.79 % (3253450)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=1001123984:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 4.77/1.79 % (3253453)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2322813558:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 4.77/1.79 % (3253448)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=2063691894:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 4.77/1.79 % (3253449)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=1472997041:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 4.77/1.79 % (3253450)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 4.77/1.79 % (3253452)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2141989428:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 4.77/1.79 % (3253451)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=436765326:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 4.77/1.79 % (3253451)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 4.77/1.79 % (3253454)Instruction limit reached! % 4.77/1.79 % (3253454)------------------------------ % 4.77/1.79 % (3253454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.77/1.79 % (3253454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.77/1.79 % (3253454)CaDiCaL version: 2.1.3 % 4.77/1.79 % (3253454)Termination reason: Instruction limit % 4.77/1.79 % (3253454)Termination phase: Saturation % 4.77/1.79 % (3253454)Time elapsed: 0.035 s % 4.77/1.79 % (3253454)Peak memory usage: 90 MB % 4.77/1.79 % (3253454)Instructions burned: 130 (million) % 4.77/1.79 % (3253451)Refutation not found, incomplete strategy % 4.77/1.79 % (3253451)------------------------------ % 4.77/1.79 % (3253451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.77/1.79 % (3253451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.77/1.79 % (3253451)CaDiCaL version: 2.1.3 % 4.77/1.79 % (3253451)Termination reason: Refutation not found, incomplete strategy % 4.77/1.79 % (3253451)Time elapsed: 0.015 s % 4.77/1.79 % (3253451)Peak memory usage: 89 MB % 4.77/1.79 % (3253451)Instructions burned: 26 (million) % 4.77/1.79 % (3253452)Instruction limit reached! % 4.77/1.79 % (3253452)------------------------------ % 4.77/1.79 % (3253452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.77/1.79 % (3253452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.77/1.79 % (3253452)CaDiCaL version: 2.1.3 % 4.77/1.79 % (3253452)Termination reason: Instruction limit % 4.77/1.79 % (3253452)Termination phase: Saturation % 4.77/1.79 % (3253452)Time elapsed: 0.071 s % 4.77/1.79 % (3253452)Peak memory usage: 88 MB % 4.77/1.79 % (3253452)Instructions burned: 120 (million) % 4.77/1.79 % (3253453)Instruction limit reached! % 4.77/1.79 % (3253453)------------------------------ % 4.77/1.79 % (3253453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.77/1.79 % (3253453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.77/1.79 % (3253453)CaDiCaL version: 2.1.3 % 4.77/1.79 % (3253453)Termination reason: Instruction limit % 4.77/1.79 % (3253453)Termination phase: Saturation % 4.77/1.79 % (3253453)Time elapsed: 0.091 s % 4.77/1.79 % (3253453)Peak memory usage: 89 MB % 4.77/1.79 % (3253453)Instructions burned: 140 (million) % 4.77/1.79 % (3253462)lrs+10_1_sil=8000:sp=occurrence:random_seed=1895164598:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi) % 4.77/1.79 % (3253462)Instruction limit reached! % 4.77/1.79 % (3253462)------------------------------ % 4.77/1.79 % (3253462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.77/1.79 % (3253462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.77/1.79 % (3253462)CaDiCaL version: 2.1.3 % 9.21/2.15 % (3253462)Termination reason: Instruction limit % 9.21/2.15 % (3253462)Termination phase: Saturation % 9.21/2.15 % (3253462)Time elapsed: 0.094 s % 9.21/2.15 % (3253462)Peak memory usage: 91 MB % 9.21/2.15 % (3253462)Instructions burned: 288 (million) % 9.21/2.15 % (3253463)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2244065851:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 9.21/2.15 % (3253464)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4211768521:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 9.21/2.15 % (3253451)------------------------------ % 9.21/2.15 % (3253451)------------------------------ % 9.21/2.15 % (3253466)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=998580530:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi) % 9.21/2.15 % (3253463)Instruction limit reached! % 9.21/2.15 % (3253463)------------------------------ % 9.21/2.15 % (3253463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.21/2.15 % (3253463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.21/2.15 % (3253463)CaDiCaL version: 2.1.3 % 9.21/2.15 % (3253463)Termination reason: Instruction limit % 9.21/2.15 % (3253463)Termination phase: Saturation % 9.21/2.15 % (3253463)Time elapsed: 0.093 s % 9.21/2.15 % (3253463)Peak memory usage: 90 MB % 9.21/2.15 % (3253463)Instructions burned: 159 (million) % 9.21/2.15 % Exception at run slice level % 9.21/2.15 % Exception at run slice levelUser error: % 9.21/2.15 GNN currently only supports monomorphic FOL. % 9.21/2.15 User error: GNN currently only supports monomorphic FOL. % 9.21/2.15 % Exception at run slice level % 9.21/2.15 User error: GNN currently only supports monomorphic FOL. % 9.21/2.15 % (3253466)Instruction limit reached! % 9.21/2.15 % (3253466)------------------------------ % 9.21/2.15 % (3253466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.21/2.15 % (3253466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.21/2.15 % (3253466)CaDiCaL version: 2.1.3 % 9.21/2.15 % (3253466)Termination reason: Instruction limit % 9.21/2.15 % (3253466)Termination phase: Saturation % 9.21/2.15 % (3253466)Time elapsed: 0.076 s % 9.21/2.15 % (3253466)Peak memory usage: 90 MB % 9.21/2.15 % (3253466)Instructions burned: 248 (million) % 9.21/2.15 % (3253469)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1476726039:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 9.21/2.15 % (3253469)Refutation not found, incomplete strategy % 9.21/2.15 % (3253469)------------------------------ % 9.21/2.15 % (3253469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.21/2.15 % (3253469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.21/2.15 % (3253469)CaDiCaL version: 2.1.3 % 9.21/2.15 % (3253469)Termination reason: Refutation not found, incomplete strategy % 9.21/2.15 % (3253469)Time elapsed: 0.010 s % 9.21/2.15 % (3253469)Peak memory usage: 89 MB % 9.21/2.15 % (3253469)Instructions burned: 16 (million) % 9.21/2.15 % (3253464)Instruction limit reached! % 9.21/2.15 % (3253464)------------------------------ % 9.21/2.15 % (3253464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.21/2.15 % (3253464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.21/2.15 % (3253464)CaDiCaL version: 2.1.3 % 9.21/2.15 % (3253464)Termination reason: Instruction limit % 9.21/2.15 % (3253464)Termination phase: Saturation % 9.21/2.15 % (3253464)Time elapsed: 0.203 s % 9.21/2.15 % (3253464)Peak memory usage: 91 MB % 9.21/2.15 % (3253464)Instructions burned: 327 (million) % 9.21/2.15 % (3253471)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=996058697:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 9.21/2.15 % (3253475)lrs+10_1_sil=8000:sp=occurrence:random_seed=812097006:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 9.21/2.15 % (3253473)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3897653442:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 9.21/2.15 % (3253474)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=627235048:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 9.21/2.15 % (3253472)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1965338287:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 9.21/2.15 % (3253474)Refutation not found, incomplete strategy % 10.15/2.44 % (3253474)------------------------------ % 10.15/2.44 % (3253474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.15/2.44 % (3253474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.15/2.44 % (3253474)CaDiCaL version: 2.1.3 % 10.15/2.44 % (3253474)Termination reason: Refutation not found, incomplete strategy % 10.15/2.44 % (3253474)Time elapsed: 0.042 s % 10.15/2.44 % (3253474)Peak memory usage: 89 MB % 10.15/2.44 % (3253474)Instructions burned: 81 (million) % 10.15/2.44 % (3253477)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1642074407:i=437:sd=1:aac=none:ss=included_2994 on theBenchmark for (2994ds/437Mi) % 10.15/2.44 % (3253477)Refutation not found, incomplete strategy % 10.15/2.44 % (3253477)------------------------------ % 10.15/2.44 % (3253477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.15/2.44 % (3253477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.15/2.44 % (3253477)CaDiCaL version: 2.1.3 % 10.15/2.44 % (3253477)Termination reason: Refutation not found, incomplete strategy % 10.15/2.44 % (3253477)Time elapsed: 0.010 s % 10.15/2.44 % (3253477)Peak memory usage: 88 MB % 10.15/2.44 % (3253477)Instructions burned: 16 (million) % 10.15/2.44 % (3253473)Instruction limit reached! % 10.15/2.44 % (3253473)------------------------------ % 10.15/2.44 % (3253473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.15/2.44 % (3253473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.15/2.44 % (3253473)CaDiCaL version: 2.1.3 % 10.15/2.44 % (3253473)Termination reason: Instruction limit % 10.15/2.44 % (3253473)Termination phase: Saturation % 10.15/2.44 % (3253473)Time elapsed: 0.062 s % 10.15/2.44 % (3253473)Peak memory usage: 88 MB % 10.15/2.44 % (3253473)Instructions burned: 129 (million) % 10.15/2.44 % (3253472)Instruction limit reached! % 10.15/2.44 % (3253472)------------------------------ % 10.15/2.44 % (3253472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.15/2.44 % (3253472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.15/2.44 % (3253472)CaDiCaL version: 2.1.3 % 10.15/2.44 % (3253472)Termination reason: Instruction limit % 10.15/2.44 % (3253472)Termination phase: Saturation % 10.15/2.44 % (3253472)Time elapsed: 0.067 s % 10.15/2.44 % (3253472)Peak memory usage: 89 MB % 10.15/2.44 % (3253472)Instructions burned: 114 (million) % 10.15/2.44 % (3253469)------------------------------ % 10.15/2.44 % (3253469)------------------------------ % 10.15/2.44 % (3253485)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2640157513:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2992 on theBenchmark for (2992ds/134Mi) % 10.15/2.44 % (3253484)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3905652124:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi) % 10.15/2.44 % (3253475)Instruction limit reached! % 10.15/2.44 % (3253475)------------------------------ % 10.15/2.44 % (3253475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.15/2.44 % (3253475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.15/2.44 % (3253475)CaDiCaL version: 2.1.3 % 10.15/2.44 % (3253475)Termination reason: Instruction limit % 10.15/2.44 % (3253475)Termination phase: Saturation % 10.15/2.44 % (3253475)Time elapsed: 0.289 s % 10.15/2.44 % (3253475)Peak memory usage: 94 MB % 10.15/2.44 % (3253475)Instructions burned: 909 (million) % 10.15/2.44 % (3253485)Instruction limit reached! % 10.15/2.44 % (3253485)------------------------------ % 10.15/2.44 % (3253485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.15/2.44 % (3253485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.15/2.44 % (3253485)CaDiCaL version: 2.1.3 % 10.15/2.44 % (3253485)Termination reason: Instruction limit % 10.15/2.44 % (3253485)Termination phase: Saturation % 10.15/2.44 % (3253485)Time elapsed: 0.080 s % 10.15/2.44 % (3253485)Peak memory usage: 90 MB % 10.15/2.44 % (3253485)Instructions burned: 134 (million) % 10.15/2.44 % (3253474)------------------------------ % 10.15/2.44 % (3253474)------------------------------ % 10.15/2.44 % (3253486)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2776996164:st=8:i=592:sd=3:ep=RST:ss=axioms_2991 on theBenchmark for (2991ds/592Mi) % 10.15/2.44 % (3253486)Refutation not found, incomplete strategy % 10.15/2.44 % (3253486)------------------------------ % 10.15/2.44 % (3253486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.80/3.05 % (3253486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.80/3.05 % (3253486)CaDiCaL version: 2.1.3 % 15.80/3.05 % (3253486)Termination reason: Refutation not found, incomplete strategy % 15.80/3.05 % (3253486)Time elapsed: 0.008 s % 15.80/3.05 % (3253486)Peak memory usage: 88 MB % 15.80/3.05 % (3253486)Instructions burned: 13 (million) % 15.80/3.05 % (3253477)------------------------------ % 15.80/3.05 % (3253477)------------------------------ % 15.80/3.05 % Exception at run slice level % 15.80/3.05 User error: GNN currently only supports monomorphic FOL. % 15.80/3.05 % (3253489)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2044037065:st=3:i=13193:sd=3:ss=axioms_2991 on theBenchmark for (2991ds/13193Mi) % 15.80/3.05 % (3253490)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=2859659233:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/125Mi) % 15.80/3.05 % (3253490)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 15.80/3.05 % (3253492)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2065665621:i=134:gtgl=5:slsql=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/134Mi) % 15.80/3.05 % Exception at run slice level % 15.80/3.05 User error: Immediate (shared) subterms of term/literal combb(fun(X1,X0),fun(fun(X2,X1),fun(X2,X0)),X0) = sF20(X1,X0,X2) have different types/not well-typed! % 15.80/3.05 % (3253493)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=228693829:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/141Mi) % 15.80/3.05 % (3253493)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 15.80/3.05 % (3253493)Refutation not found, incomplete strategy % 15.80/3.05 % (3253493)------------------------------ % 15.80/3.05 % (3253493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.80/3.05 % (3253493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.80/3.05 % (3253493)CaDiCaL version: 2.1.3 % 15.80/3.05 % (3253493)Termination reason: Refutation not found, incomplete strategy % 15.80/3.05 % (3253493)Time elapsed: 0.006 s % 15.80/3.05 % (3253493)Peak memory usage: 88 MB % 15.80/3.05 % (3253493)Instructions burned: 8 (million) % 15.80/3.05 % (3253494)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1404109340:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2990 on theBenchmark for (2990ds/431Mi) % 15.80/3.05 % (3253490)Instruction limit reached! % 15.80/3.05 % (3253490)------------------------------ % 15.80/3.05 % (3253490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.80/3.05 % (3253490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.80/3.05 % (3253490)CaDiCaL version: 2.1.3 % 15.80/3.05 % (3253490)Termination reason: Instruction limit % 15.80/3.05 % (3253490)Termination phase: Saturation % 15.80/3.05 % (3253490)Time elapsed: 0.075 s % 15.80/3.05 % (3253490)Peak memory usage: 90 MB % 15.80/3.05 % (3253490)Instructions burned: 125 (million) % 15.80/3.05 % (3253486)------------------------------ % 15.80/3.05 % (3253486)------------------------------ % 15.80/3.05 % Exception at run slice level % 15.80/3.05 User error: GNN currently only supports monomorphic FOL. % 15.80/3.05 % (3253499)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=472026471:i=6060:aac=none:ins=25_2989 on theBenchmark for (2989ds/6060Mi) % 15.80/3.05 % Exception at run slice level % 15.80/3.05 User error: GNN currently only supports monomorphic FOL. % 15.80/3.05 % (3253501)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=196342258:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2988 on theBenchmark for (2988ds/150Mi) % 15.80/3.05 % (3253501)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 15.80/3.05 % (3253504)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1972164515:i=667:av=off:fsr=off_2988 on theBenchmark for (2988ds/667Mi) % 15.80/3.05 % (3253502)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3643805022:i=14155:bd=all_2988 on theBenchmark for (2988ds/14155Mi) % 19.92/3.99 % (3253494)Instruction limit reached! % 19.92/3.99 % (3253494)------------------------------ % 19.92/3.99 % (3253494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.92/3.99 % (3253494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.92/3.99 % (3253494)CaDiCaL version: 2.1.3 % 19.92/3.99 % (3253494)Termination reason: Instruction limit % 19.92/3.99 % (3253494)Termination phase: Saturation % 19.92/3.99 % (3253494)Time elapsed: 0.217 s % 19.92/3.99 % (3253494)Peak memory usage: 92 MB % 19.92/3.99 % (3253494)Instructions burned: 431 (million) % 19.92/3.99 % (3253493)------------------------------ % 19.92/3.99 % (3253493)------------------------------ % 19.92/3.99 % (3253505)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=1365379726:s2a=on:i=185:s2at=1.8:fdi=4_2987 on theBenchmark for (2987ds/185Mi) % 19.92/3.99 % (3253501)Instruction limit reached! % 19.92/3.99 % (3253501)------------------------------ % 19.92/3.99 % (3253501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.92/3.99 % (3253501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.92/3.99 % (3253501)CaDiCaL version: 2.1.3 % 19.92/3.99 % (3253501)Termination reason: Instruction limit % 19.92/3.99 % (3253501)Termination phase: Saturation % 19.92/3.99 % (3253501)Time elapsed: 0.099 s % 19.92/3.99 % (3253501)Peak memory usage: 90 MB % 19.92/3.99 % (3253501)Instructions burned: 150 (million) % 19.92/3.99 % (3253504)Instruction limit reached! % 19.92/3.99 % (3253504)------------------------------ % 19.92/3.99 % (3253504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.92/3.99 % (3253504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.92/3.99 % (3253504)CaDiCaL version: 2.1.3 % 19.92/3.99 % (3253504)Termination reason: Instruction limit % 19.92/3.99 % (3253504)Termination phase: Saturation % 19.92/3.99 % (3253504)Time elapsed: 0.154 s % 19.92/3.99 % (3253504)Peak memory usage: 97 MB % 19.92/3.99 % (3253504)Instructions burned: 671 (million) % 19.92/3.99 % (3253509)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=669959266:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2986 on theBenchmark for (2986ds/193Mi) % 19.92/3.99 % (3253510)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3486346382:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2986 on theBenchmark for (2986ds/4850Mi) % 19.92/3.99 % (3253505)Instruction limit reached! % 19.92/3.99 % (3253505)------------------------------ % 19.92/3.99 % (3253505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.92/3.99 % (3253505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.92/3.99 % (3253505)CaDiCaL version: 2.1.3 % 19.92/3.99 % (3253505)Termination reason: Instruction limit % 19.92/3.99 % (3253505)Termination phase: Saturation % 19.92/3.99 % (3253505)Time elapsed: 0.124 s % 19.92/3.99 % (3253505)Peak memory usage: 91 MB % 19.92/3.99 % (3253505)Instructions burned: 186 (million) % 19.92/3.99 % (3253512)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=96573265:i=12111:sd=1:ss=included_2986 on theBenchmark for (2986ds/12111Mi) % 19.92/3.99 % (3253514)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=183409375:i=319:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/319Mi) % 19.92/3.99 % (3253509)Instruction limit reached! % 19.92/3.99 % (3253509)------------------------------ % 19.92/3.99 % (3253509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.92/3.99 % (3253509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.92/3.99 % (3253509)CaDiCaL version: 2.1.3 % 19.92/3.99 % (3253509)Termination reason: Instruction limit % 19.92/3.99 % (3253509)Termination phase: Saturation % 19.92/3.99 % (3253509)Time elapsed: 0.117 s % 19.92/3.99 % (3253509)Peak memory usage: 91 MB % 19.92/3.99 % (3253509)Instructions burned: 195 (million) % 19.92/3.99 % Exception at run slice level % 19.92/3.99 User error: GNN currently only supports monomorphic FOL. % 19.92/3.99 % (3253516)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=4000805494:i=2064:ep=RST_2985 on theBenchmark for (2985ds/2064Mi) % 19.92/3.99 % (3253516)Refutation not found, incomplete strategy % 19.92/3.99 % (3253516)------------------------------ % 19.92/3.99 % (3253516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.92/3.99 % (3253516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.15/4.92 % (3253516)CaDiCaL version: 2.1.3 % 27.15/4.92 % (3253516)Termination reason: Refutation not found, incomplete strategy % 27.15/4.92 % (3253516)Time elapsed: 0.007 s % 27.15/4.92 % (3253516)Peak memory usage: 88 MB % 27.15/4.92 % (3253516)Instructions burned: 12 (million) % 27.15/4.92 % (3253514)Instruction limit reached! % 27.15/4.92 % (3253514)------------------------------ % 27.15/4.92 % (3253514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.15/4.92 % (3253514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.15/4.92 % (3253514)CaDiCaL version: 2.1.3 % 27.15/4.92 % (3253514)Termination reason: Instruction limit % 27.15/4.92 % (3253514)Termination phase: Saturation % 27.15/4.92 % (3253514)Time elapsed: 0.099 s % 27.15/4.92 % (3253514)Peak memory usage: 92 MB % 27.15/4.92 % (3253514)Instructions burned: 319 (million) % 27.15/4.92 % Exception at run slice level % 27.15/4.92 User error: GNN currently only supports monomorphic FOL. % 27.15/4.92 % (3253519)dis-1011_128_sil=32000:random_seed=2902809713:i=3706:ep=RST:av=off_2984 on theBenchmark for (2984ds/3706Mi) % 27.15/4.92 % (3253520)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1620932537:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2984 on theBenchmark for (2984ds/757Mi) % 27.15/4.92 % (3253520)Refutation not found, incomplete strategy % 27.15/4.92 % (3253520)------------------------------ % 27.15/4.92 % (3253520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.15/4.92 % (3253520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.15/4.92 % (3253520)CaDiCaL version: 2.1.3 % 27.15/4.92 % (3253520)Termination reason: Refutation not found, incomplete strategy % 27.15/4.92 % (3253520)Time elapsed: 0.010 s % 27.15/4.92 % (3253520)Peak memory usage: 89 MB % 27.15/4.92 % (3253520)Instructions burned: 16 (million) % 27.15/4.92 % (3253522)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2306835534:i=13913:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/13913Mi) % 27.15/4.92 % (3253524)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=105784030:i=9925:aac=none_2983 on theBenchmark for (2983ds/9925Mi) % 27.15/4.92 % Exception at run slice level % 27.15/4.92 User error: GNN currently only supports monomorphic FOL. % 27.15/4.92 % (3253516)------------------------------ % 27.15/4.92 % (3253516)------------------------------ % 27.15/4.92 % Exception at run slice level % 27.15/4.92 User error: GNN currently only supports monomorphic FOL. % 27.15/4.92 % (3253520)------------------------------ % 27.15/4.92 % (3253520)------------------------------ % 27.15/4.92 % (3253528)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2200565813:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2981 on theBenchmark for (2981ds/2479Mi) % 27.15/4.92 % (3253529)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2756684482:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/440Mi) % 27.15/4.92 % (3253528)Refutation not found, incomplete strategy % 27.15/4.92 % (3253528)------------------------------ % 27.15/4.92 % (3253528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.15/4.92 % (3253528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.15/4.92 % (3253528)CaDiCaL version: 2.1.3 % 27.15/4.92 % (3253528)Termination reason: Refutation not found, incomplete strategy % 27.15/4.92 % (3253528)Time elapsed: 0.013 s % 27.15/4.92 % (3253528)Peak memory usage: 89 MB % 27.15/4.92 % (3253528)Instructions burned: 20 (million) % 27.15/4.92 % (3253529)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 27.15/4.92 % (3253530)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2930113069:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2981 on theBenchmark for (2981ds/11145Mi) % 27.15/4.92 % (3253531)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=3838400275:cts=off:i=3034:av=off:er=known:fsd=on_2980 on theBenchmark for (2980ds/3034Mi) % 27.15/4.92 % Exception at run slice level % 27.15/4.92 User error: GNN currently only supports monomorphic FOL. % 27.15/4.92 % Exception at run slice level % 27.15/4.92 User error: GNN currently only supports monomorphic FOL. % 27.15/4.92 % (3253528)------------------------------ % 27.15/4.92 % (3253528)------------------------------ % 37.89/6.58 % (3253529)Instruction limit reached! % 37.89/6.58 % (3253529)------------------------------ % 37.89/6.58 % (3253529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.89/6.58 % (3253529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.89/6.58 % (3253529)CaDiCaL version: 2.1.3 % 37.89/6.58 % (3253529)Termination reason: Instruction limit % 37.89/6.58 % (3253529)Termination phase: Saturation % 37.89/6.58 % (3253529)Time elapsed: 0.238 s % 37.89/6.58 % (3253529)Peak memory usage: 93 MB % 37.89/6.58 % (3253529)Instructions burned: 442 (million) % 37.89/6.58 % (3253537)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=697814856:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2978 on theBenchmark for (2978ds/1016Mi) % 37.89/6.58 % (3253536)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=905372660:st=2:s2a=on:i=524:s2at=2:ss=axioms_2978 on theBenchmark for (2978ds/524Mi) % 37.89/6.58 % (3253539)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1512525688:i=5781:kws=precedence:bd=all:rawr=on_2977 on theBenchmark for (2977ds/5781Mi) % 37.89/6.58 % (3253538)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1720902376:i=14123:bd=preordered:ins=4_2977 on theBenchmark for (2977ds/14123Mi) % 37.89/6.58 % Exception at run slice level % 37.89/6.58 User error: GNN currently only supports monomorphic FOL. % 37.89/6.58 % (3253537)Instruction limit reached! % 37.89/6.58 % (3253537)------------------------------ % 37.89/6.58 % (3253537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.89/6.58 % (3253537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.89/6.58 % (3253537)CaDiCaL version: 2.1.3 % 37.89/6.58 % (3253537)Termination reason: Instruction limit % 37.89/6.58 % (3253537)Termination phase: Saturation % 37.89/6.58 % (3253537)Time elapsed: 0.243 s % 37.89/6.58 % (3253537)Peak memory usage: 98 MB % 37.89/6.58 % (3253537)Instructions burned: 1018 (million) % 37.89/6.58 % (3253544)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=790807493:i=2448:gtgl=5:bd=preordered:gtg=all_2975 on theBenchmark for (2975ds/2448Mi) % 37.89/6.58 % (3253536)Instruction limit reached! % 37.89/6.58 % (3253536)------------------------------ % 37.89/6.58 % (3253536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.89/6.58 % (3253536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.89/6.58 % (3253536)CaDiCaL version: 2.1.3 % 37.89/6.58 % (3253536)Termination reason: Instruction limit % 37.89/6.58 % (3253536)Termination phase: Saturation % 37.89/6.58 % (3253536)Time elapsed: 0.281 s % 37.89/6.58 % (3253536)Peak memory usage: 92 MB % 37.89/6.58 % (3253536)Instructions burned: 524 (million) % 37.89/6.58 % (3253545)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2905130823:i=3223:kws=precedence:fgj=on:av=off_2974 on theBenchmark for (2974ds/3223Mi) % 37.89/6.58 % Exception at run slice level % 37.89/6.58 User error: GNN currently only supports monomorphic FOL. % 37.89/6.58 % (3253547)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3079362221:st=5.6:i=2033:sd=3:ss=axioms_2974 on theBenchmark for (2974ds/2033Mi) % 37.89/6.58 % Exception at run slice level % 37.89/6.58 User error: GNN currently only supports monomorphic FOL. % 37.89/6.58 % (3253549)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1924615699:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2973 on theBenchmark for (2973ds/2055Mi) % 37.89/6.58 % (3253551)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=434824858:i=21611:sd=3:ss=axioms_2972 on theBenchmark for (2972ds/21611Mi) % 37.89/6.58 % Exception at run slice level % 37.89/6.58 User error: GNN currently only supports monomorphic FOL. % 37.89/6.58 % (3253554)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3655850301:i=4835:sd=13:ss=axioms:sgt=23_2970 on theBenchmark for (2970ds/4835Mi) % 37.89/6.58 % Exception at run slice level % 37.89/6.58 User error: GNN currently only supports monomorphic FOL. % 37.89/6.58 % Exception at run slice level % 37.89/6.58 User error: GNN currently only supports monomorphic FOL. % 37.89/6.58 % (3253556)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=2913856326:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2969 on theBenchmark for (2969ds/797Mi) % 47.30/8.10 % Exception at run slice level % 47.30/8.10 User error: GNN currently only supports monomorphic FOL. % 47.30/8.10 % (3253557)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1499677329:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2969 on theBenchmark for (2969ds/2326Mi) % 47.30/8.10 % (3253557)Refutation not found, incomplete strategy % 47.30/8.10 % (3253557)------------------------------ % 47.30/8.10 % (3253557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.30/8.10 % (3253557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.30/8.10 % (3253557)CaDiCaL version: 2.1.3 % 47.30/8.10 % (3253557)Termination reason: Refutation not found, incomplete strategy % 47.30/8.10 % (3253557)Time elapsed: 0.012 s % 47.30/8.10 % (3253557)Peak memory usage: 89 MB % 47.30/8.10 % (3253557)Instructions burned: 19 (million) % 47.30/8.10 % (3253559)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=677044462:i=6038:nm=6_2968 on theBenchmark for (2968ds/6038Mi) % 47.30/8.10 % (3253556)Instruction limit reached! % 47.30/8.10 % (3253556)------------------------------ % 47.30/8.10 % (3253556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.30/8.10 % (3253556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.30/8.10 % (3253556)CaDiCaL version: 2.1.3 % 47.30/8.10 % (3253556)Termination reason: Instruction limit % 47.30/8.10 % (3253556)Termination phase: Saturation % 47.30/8.10 % (3253556)Time elapsed: 0.216 s % 47.30/8.10 % (3253556)Peak memory usage: 91 MB % 47.30/8.10 % (3253556)Instructions burned: 798 (million) % 47.30/8.10 % (3253557)------------------------------ % 47.30/8.10 % (3253557)------------------------------ % 47.30/8.10 % (3253562)lrs+10_1_sil=32000:sp=occurrence:random_seed=3729612222:st=2:i=33334:sd=3:ss=included:sgt=32_2966 on theBenchmark for (2966ds/33334Mi) % 47.30/8.10 % (3253564)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3656052040:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2965 on theBenchmark for (2965ds/1008Mi) % 47.30/8.10 % Exception at run slice level % 47.30/8.10 User error: GNN currently only supports monomorphic FOL. % 47.30/8.10 % (3253566)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=1910325272:i=8327:s2at=5:bd=preordered_2963 on theBenchmark for (2963ds/8327Mi) % 47.30/8.10 % (3253519)Instruction limit reached! % 47.30/8.10 % (3253519)------------------------------ % 47.30/8.10 % (3253519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.30/8.10 % (3253519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.30/8.10 % (3253519)CaDiCaL version: 2.1.3 % 47.30/8.10 % (3253519)Termination reason: Instruction limit % 47.30/8.10 % (3253519)Termination phase: Saturation % 47.30/8.10 % (3253519)Time elapsed: 2.143 s % 47.30/8.10 % (3253519)Peak memory usage: 115 MB % 47.30/8.10 % (3253519)Instructions burned: 3707 (million) % 47.30/8.10 % (3253568)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=3633506619:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2961 on theBenchmark for (2961ds/1083Mi) % 47.30/8.10 % (3253564)Instruction limit reached! % 47.30/8.10 % (3253564)------------------------------ % 47.30/8.10 % (3253564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.30/8.10 % (3253564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.30/8.10 % (3253564)CaDiCaL version: 2.1.3 % 47.30/8.10 % (3253564)Termination reason: Instruction limit % 47.30/8.10 % (3253564)Termination phase: Saturation % 47.30/8.10 % (3253564)Time elapsed: 0.496 s % 47.30/8.10 % (3253564)Peak memory usage: 93 MB % 47.30/8.10 % (3253564)Instructions burned: 1008 (million) % 47.30/8.10 % (3253510)Instruction limit reached! % 47.30/8.10 % (3253510)------------------------------ % 47.30/8.10 % (3253510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.30/8.10 % (3253510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.30/8.10 % (3253510)CaDiCaL version: 2.1.3 % 47.30/8.10 % (3253510)Termination reason: Instruction limit % 57.19/9.51 % (3253510)Termination phase: Saturation % 57.19/9.51 % (3253510)Time elapsed: 2.607 s % 57.19/9.51 % (3253510)Peak memory usage: 115 MB % 57.19/9.51 % (3253510)Instructions burned: 4851 (million) % 57.19/9.51 % Exception at run slice level % 57.19/9.51 User error: GNN currently only supports monomorphic FOL. % 57.19/9.51 % (3253570)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1620835825:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2959 on theBenchmark for (2959ds/1084Mi) % 57.19/9.51 % (3253571)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=388017197:i=6995:s2at=5:gtg=all_2959 on theBenchmark for (2959ds/6995Mi) % 57.19/9.51 % (3253572)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2064905397:st=2:i=6225:sd=15:ss=axioms_2958 on theBenchmark for (2958ds/6225Mi) % 57.19/9.51 % (3253568)Instruction limit reached! % 57.19/9.51 % (3253568)------------------------------ % 57.19/9.51 % (3253568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.19/9.51 % (3253568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.19/9.51 % (3253568)CaDiCaL version: 2.1.3 % 57.19/9.51 % (3253568)Termination reason: Instruction limit % 57.19/9.51 % (3253568)Termination phase: Saturation % 57.19/9.51 % (3253568)Time elapsed: 0.525 s % 57.19/9.51 % (3253568)Peak memory usage: 97 MB % 57.19/9.51 % (3253568)Instructions burned: 1083 (million) % 57.19/9.51 % (3253576)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3218125342:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2955 on theBenchmark for (2955ds/3372Mi) % 57.19/9.51 % (3253570)Instruction limit reached! % 57.19/9.51 % (3253570)------------------------------ % 57.19/9.51 % (3253570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.19/9.51 % (3253570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.19/9.51 % (3253570)CaDiCaL version: 2.1.3 % 57.19/9.51 % (3253570)Termination reason: Instruction limit % 57.19/9.51 % (3253570)Termination phase: Saturation % 57.19/9.51 % (3253570)Time elapsed: 0.587 s % 57.19/9.51 % (3253570)Peak memory usage: 94 MB % 57.19/9.51 % (3253570)Instructions burned: 1084 (million) % 57.19/9.51 % (3253578)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=439693862:st=2.3:i=26457:sd=10:ss=included:sgt=8_2952 on theBenchmark for (2952ds/26457Mi) % 57.19/9.51 % Exception at run slice level % 57.19/9.51 User error: GNN currently only supports monomorphic FOL. % 57.19/9.51 % (3253539)Instruction limit reached! % 57.19/9.51 % (3253539)------------------------------ % 57.19/9.51 % (3253539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.19/9.51 % (3253539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.19/9.51 % (3253539)CaDiCaL version: 2.1.3 % 57.19/9.51 % (3253539)Termination reason: Instruction limit % 57.19/9.51 % (3253539)Termination phase: Saturation % 57.19/9.51 % (3253539)Time elapsed: 2.919 s % 57.19/9.51 % (3253539)Peak memory usage: 102 MB % 57.19/9.51 % (3253539)Instructions burned: 5781 (million) % 57.19/9.51 % (3253580)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=2824308093:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2948 on theBenchmark for (2948ds/13494Mi) % 57.19/9.51 % (3253581)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=2458181491:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2947 on theBenchmark for (2947ds/2503Mi) % 57.19/9.51 % (3253581)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 57.19/9.51 % Exception at run slice level% Exception at run slice level % 57.19/9.51 % 57.19/9.51 User error: User error: GNN currently only supports monomorphic FOL.GNN currently only supports monomorphic FOL. % 57.19/9.51 % 57.19/9.51 % (3253585)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3154843412:i=30753:av=off:ss=included_2944 on theBenchmark for (2944ds/30753Mi) % 57.19/9.51 % (3253584)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=930927385:i=2559:sd=1:ep=RSTC:ss=axioms_2944 on theBenchmark for (2944ds/2559Mi) % 57.19/9.51 % Exception at run slice level % 57.19/9.51 User error: GNN currently only supports monomorphic FOL. % 57.19/9.51 % Exception at run slice level % 66.31/11.03 User error: GNN currently only supports monomorphic FOL. % 66.31/11.03 % (3253588)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2725862039:i=26473:ep=RSTC_2943 on theBenchmark for (2943ds/26473Mi) % 66.31/11.03 % (3253589)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=2783170125:cts=off:i=2759:kws=inv_arity:fgj=on_2942 on theBenchmark for (2942ds/2759Mi) % 66.31/11.03 % (3253554)Instruction limit reached! % 66.31/11.03 % (3253554)------------------------------ % 66.31/11.03 % (3253554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.31/11.03 % (3253554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.31/11.03 % (3253554)CaDiCaL version: 2.1.3 % 66.31/11.03 % (3253554)Termination reason: Instruction limit % 66.31/11.03 % (3253554)Termination phase: Saturation % 66.31/11.03 % (3253554)Time elapsed: 2.868 s % 66.31/11.03 % (3253554)Peak memory usage: 111 MB % 66.31/11.03 % (3253554)Instructions burned: 4835 (million) % 66.31/11.03 % Exception at run slice level % 66.31/11.03 User error: GNN currently only supports monomorphic FOL. % 66.31/11.03 % Exception at run slice level % 66.31/11.03 User error: GNN currently only supports monomorphic FOL. % 66.31/11.03 % (3253592)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=1471055486:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2940 on theBenchmark for (2940ds/5665Mi) % 66.31/11.03 % (3253592)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 66.31/11.03 % (3253593)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=2259802646:i=1532:ep=RS:ss=axioms_2940 on theBenchmark for (2940ds/1532Mi) % 66.31/11.03 % (3253594)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3168239735:i=1565:sd=2:ss=axioms:sgt=32_2940 on theBenchmark for (2940ds/1565Mi) % 66.31/11.03 % Exception at run slice level % 66.31/11.03 User error: GNN currently only supports monomorphic FOL. % 66.31/11.03 % (3253572)Instruction limit reached! % 66.31/11.03 % (3253572)------------------------------ % 66.31/11.03 % (3253572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.31/11.03 % (3253572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.31/11.03 % (3253572)CaDiCaL version: 2.1.3 % 66.31/11.03 % (3253572)Termination reason: Instruction limit % 66.31/11.03 % (3253572)Termination phase: Saturation % 66.31/11.03 % (3253572)Time elapsed: 2.684 s % 66.31/11.03 % (3253572)Peak memory usage: 146 MB % 66.31/11.03 % (3253572)Instructions burned: 6839 (million) % 66.31/11.03 % (3253598)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=4217328443:i=1572:fgj=on:gsp=on_2937 on theBenchmark for (2937ds/1572Mi) % 66.31/11.03 % (3253598)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 66.31/11.03 % Exception at run slice level % 66.31/11.03 User error: GNN currently only supports monomorphic FOL. % 66.31/11.03 % (3253600)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=785109053:i=6052:sd=4:ss=axioms:sgt=24_2930 on theBenchmark for (2930ds/6052Mi) % 66.31/11.03 % Exception at run slice level% Exception at run slice level % 66.31/11.03 User error: % 66.31/11.03 GNN currently only supports monomorphic FOL. % 66.31/11.03 User error: GNN currently only supports monomorphic FOL. % 66.31/11.03 % (3253602)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=1326731443:i=3500:sd=1:bd=preordered:sup=off:ss=included_2929 on theBenchmark for (2929ds/3500Mi) % 66.31/11.03 % (3253604)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=176619063:i=66096:add=on_2928 on theBenchmark for (2928ds/66096Mi) % 66.31/11.03 % (3253603)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=737774810:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2928 on theBenchmark for (2928ds/1842Mi) % 66.31/11.03 % (3253603)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 77.94/12.52 % Exception at run slice level % 77.94/12.52 User error: GNN currently only supports monomorphic FOL. % 77.94/12.52 % Exception at run slice level % 77.94/12.52 User error: GNN currently only supports monomorphic FOL. % 77.94/12.52 % (3253608)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=4168557860:i=1884:sd=1:nm=60:ss=axioms_2926 on theBenchmark for (2926ds/1884Mi) % 77.94/12.52 % Exception at run slice level % 77.94/12.52 User error: GNN currently only supports monomorphic FOL. % 77.94/12.52 % (3253609)lrs-1011_4:1_sil=16000:bsr=on:random_seed=655613756:cts=off:i=5469:bs=on:fsr=off_2925 on theBenchmark for (2925ds/5469Mi) % 77.94/12.52 % Exception at run slice level% Exception at run slice level % 77.94/12.52 User error: % 77.94/12.52 GNN currently only supports monomorphic FOL.User error: % 77.94/12.52 GNN currently only supports monomorphic FOL. % 77.94/12.52 % (3253611)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=4109717634:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2924 on theBenchmark for (2924ds/2037Mi) % 77.94/12.52 % (3253614)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=495661128:i=2430:add=off:aac=none:nm=16_2923 on theBenchmark for (2923ds/2430Mi) % 77.94/12.52 % (3253613)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3764722149:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2923 on theBenchmark for (2923ds/2110Mi) % 77.94/12.52 % Exception at run slice level % 77.94/12.52 User error: GNN currently only supports monomorphic FOL. % 77.94/12.52 % (3253618)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=2624092130:cond=fast:i=4891_2921 on theBenchmark for (2921ds/4891Mi) % 77.94/12.52 % Exception at run slice level % 77.94/12.52 User error: GNN currently only supports monomorphic FOL. % 77.94/12.52 % Exception at run slice level % 77.94/12.52 User error: GNN currently only supports monomorphic FOL. % 77.94/12.52 % Exception at run slice level % 77.94/12.52 User error: GNN currently only supports monomorphic FOL. % 77.94/12.52 % (3253620)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=3748667087:st=2:i=14845:sd=2:ss=included:fsd=on_2919 on theBenchmark for (2919ds/14845Mi) % 77.94/12.52 % (3253622)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=2922988930:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2919 on theBenchmark for (2919ds/10353Mi) % 77.94/12.52 % (3253621)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=377914548:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2919 on theBenchmark for (2919ds/7534Mi) % 77.94/12.52 % Exception at run slice level % 77.94/12.52 User error: GNN currently only supports monomorphic FOL. % 77.94/12.52 % (3253626)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2147532141:i=7860_2916 on theBenchmark for (2916ds/7860Mi) % 77.94/12.52 % (3253626)Refutation not found, incomplete strategy % 77.94/12.52 % (3253626)------------------------------ % 77.94/12.52 % (3253626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.94/12.52 % (3253626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.94/12.52 % (3253626)CaDiCaL version: 2.1.3 % 77.94/12.52 % (3253626)Termination reason: Refutation not found, incomplete strategy % 77.94/12.52 % (3253626)Time elapsed: 0.009 s % 77.94/12.52 % (3253626)Peak memory usage: 88 MB % 77.94/12.52 % (3253626)Instructions burned: 15 (million) % 77.94/12.52 % Exception at run slice level % 77.94/12.52 User error: GNN currently only supports monomorphic FOL. % 77.94/12.52 % Exception at run slice level % 77.94/12.52 User error: GNN currently only supports monomorphic FOL. % 77.94/12.52 % Exception at run slice level % 77.94/12.52 User error: GNN currently only supports monomorphic FOL. % 77.94/12.52 % (3253628)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=2664009125:i=7896:sd=2:bs=on:ss=included:sgt=20_2914 on theBenchmark for (2914ds/7896Mi) % 109.26/16.86 % (3253626)------------------------------ % 109.26/16.86 % (3253626)------------------------------ % 109.26/16.86 % (3253630)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=699628224:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2914 on theBenchmark for (2914ds/2965Mi) % 109.26/16.86 % (3253629)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=2542449710:i=5812:gtgl=2:gtg=all_2914 on theBenchmark for (2914ds/5812Mi) % 109.26/16.86 % (3253632)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=335471965:i=2967:kws=precedence:bd=preordered:av=off_2912 on theBenchmark for (2912ds/2967Mi) % 109.26/16.86 % Exception at run slice level % 109.26/16.86 User error: GNN currently only supports monomorphic FOL. % 109.26/16.86 % Exception at run slice level% Exception at run slice level % 109.26/16.86 % 109.26/16.86 User error: User error: GNN currently only supports monomorphic FOL.GNN currently only supports monomorphic FOL. % 109.26/16.86 % 109.26/16.86 % (3253636)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=1170921492:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2909 on theBenchmark for (2909ds/3022Mi) % 109.26/16.86 % Exception at run slice level % 109.26/16.86 User error: GNN currently only supports monomorphic FOL. % 109.26/16.86 % (3253638)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=412730094:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2909 on theBenchmark for (2909ds/3289Mi) % 109.26/16.86 % (3253637)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=2323668852:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2909 on theBenchmark for (2909ds/3207Mi) % 109.26/16.86 % (3253642)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=3253922845:i=38569:sd=3:ss=axioms:sgt=32_2907 on theBenchmark for (2907ds/38569Mi) % 109.26/16.86 % Exception at run slice level % 109.26/16.86 User error: GNN currently only supports monomorphic FOL. % 109.26/16.86 % Exception at run slice level % 109.26/16.86 User error: GNN currently only supports monomorphic FOL. % 109.26/16.86 % Exception at run slice level % 109.26/16.86 User error: GNN currently only supports monomorphic FOL. % 109.26/16.86 % (3253644)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=2216955125:cts=off:i=3394_2904 on theBenchmark for (2904ds/3394Mi) % 109.26/16.86 % Exception at run slice level % 109.26/16.86 User error: GNN currently only supports monomorphic FOL. % 109.26/16.86 % (3253646)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=656053459:i=20684:bd=all:gtg=exists_sym_2904 on theBenchmark for (2904ds/20684Mi) % 109.26/16.86 % (3253645)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=1604827084:i=33824:bd=preordered_2904 on theBenchmark for (2904ds/33824Mi) % 109.26/16.86 % (3253649)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=1765692115: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_2903 on theBenchmark for (2903ds/7222Mi) % 109.26/16.86 % (3253649)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 109.26/16.86 % Exception at run slice level % 109.26/16.86 User error: GNN currently only supports monomorphic FOL. % 109.26/16.86 % Exception at run slice level % 109.26/16.86 User error: GNN currently only supports monomorphic FOL. % 109.26/16.86 % Exception at run slice level % 109.26/16.86 User error: GNN currently only supports monomorphic FOL. % 109.26/16.86 % (3253652)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=2621142461:st=4:i=7295:sd=4:ep=R:ss=axioms_2899 on theBenchmark for (2899ds/7295Mi) % 109.26/16.86 % (3253654)lrs+10_1_sil=128000:lcm=predicate:random_seed=1549414877:st=3:i=43697:sd=5:ss=axioms_2899 on theBenchmark for (2899ds/43697Mi) % 109.26/16.86 % (3253653)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=2074977510:i=4036:ins=10_2899 on theBenchmark for (2899ds/4036Mi) % 124.00/18.97 % Exception at run slice level % 124.00/18.97 User error: GNN currently only supports monomorphic FOL. % 124.00/18.97 % (3253658)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=1444401985:i=17599:gtg=all:ss=axioms:fsd=on_2898 on theBenchmark for (2898ds/17599Mi) % 124.00/18.97 % Exception at run slice level % 124.00/18.97 User error: GNN currently only supports monomorphic FOL. % 124.00/18.97 % Exception at run slice level % 124.00/18.97 User error: GNN currently only supports monomorphic FOL. % 124.00/18.97 % (3253660)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=2675708426:i=4547:bd=preordered_2895 on theBenchmark for (2895ds/4547Mi) % 124.00/18.97 % (3253661)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=338671018:i=9294:av=off_2894 on theBenchmark for (2894ds/9294Mi) % 124.00/18.97 % Exception at run slice level % 124.00/18.97 User error: GNN currently only supports monomorphic FOL. % 124.00/18.97 % (3253664)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1384225997:i=32849:add=on_2893 on theBenchmark for (2893ds/32849Mi) % 124.00/18.97 % (3253609)Instruction limit reached! % 124.00/18.97 % (3253609)------------------------------ % 124.00/18.97 % (3253609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.00/18.97 % (3253609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.00/18.97 % (3253609)CaDiCaL version: 2.1.3 % 124.00/18.97 % (3253609)Termination reason: Instruction limit % 124.00/18.97 % (3253609)Termination phase: Saturation % 124.00/18.97 % (3253609)Time elapsed: 3.341 s % 124.00/18.97 % (3253609)Peak memory usage: 110 MB % 124.00/18.97 % (3253609)Instructions burned: 5470 (million) % 124.00/18.97 % Exception at run slice level % 124.00/18.97 User error: GNN currently only supports monomorphic FOL. % 124.00/18.97 % Exception at run slice level % 124.00/18.97 User error: GNN currently only supports monomorphic FOL. % 124.00/18.97 % (3253666)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1734575024:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2890 on theBenchmark for (2890ds/4793Mi) % 124.00/18.97 % (3253667)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=436757659:i=4840:nm=4:av=off_2890 on theBenchmark for (2890ds/4840Mi) % 124.00/18.97 % (3253668)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=721358221:cts=off:i=5002_2889 on theBenchmark for (2889ds/5002Mi) % 124.00/18.97 % Exception at run slice level % 124.00/18.97 User error: GNN currently only supports monomorphic FOL. % 124.00/18.97 % (3253672)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=331931100:i=30479:sd=3:ss=axioms_2888 on theBenchmark for (2888ds/30479Mi) % 124.00/18.97 % Exception at run slice level % 124.00/18.97 User error: GNN currently only supports monomorphic FOL. % 124.00/18.97 % Exception at run slice level % 124.00/18.97 User error: GNN currently only supports monomorphic FOL. % 124.00/18.97 % Exception at run slice level % 124.00/18.97 User error: GNN currently only supports monomorphic FOL. % 124.00/18.97 % (3253674)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=128244958:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2885 on theBenchmark for (2885ds/11035Mi) % 124.00/18.97 % (3253674)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 124.00/18.97 % (3253675)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=388541814:i=5835_2885 on theBenchmark for (2885ds/5835Mi) % 124.00/18.97 % (3253676)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=1273886936:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2884 on theBenchmark for (2884ds/5890Mi) % 124.00/18.97 % Exception at run slice level % 124.00/18.97 User error: GNN currently only supports monomorphic FOL. % 150.70/22.84 % (3253680)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=2068377819:cts=off:i=19910:ep=RS_2883 on theBenchmark for (2883ds/19910Mi) % 150.70/22.84 % Exception at run slice level % 150.70/22.84 User error: GNN currently only supports monomorphic FOL. % 150.70/22.84 % Exception at run slice level % 150.70/22.84 User error: GNN currently only supports monomorphic FOL. % 150.70/22.84 % Exception at run slice level % 150.70/22.84 User error: GNN currently only supports monomorphic FOL. % 150.70/22.84 % (3253682)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=1506978701:i=20312:bd=preordered:fsr=off:er=filter_2881 on theBenchmark for (2881ds/20312Mi) % 150.70/22.84 % (3253683)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=1167611325:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2880 on theBenchmark for (2880ds/13822Mi) % 150.70/22.84 % (3253684)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=12764555:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2880 on theBenchmark for (2880ds/7144Mi) % 150.70/22.84 % Exception at run slice level % 150.70/22.84 User error: GNN currently only supports monomorphic FOL. % 150.70/22.84 % Exception at run slice level % 150.70/22.84 User error: GNN currently only supports monomorphic FOL. % 150.70/22.84 % (3253688)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=2869924202:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2876 on theBenchmark for (2876ds/15184Mi) % 150.70/22.84 % (3253689)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=1574740148:i=107375_2875 on theBenchmark for (2875ds/107375Mi) % 150.70/22.84 % Exception at run slice level % 150.70/22.84 User error: GNN currently only supports monomorphic FOL. % 150.70/22.84 % Exception at run slice level % 150.70/22.84 User error: GNN currently only supports monomorphic FOL. % 150.70/22.84 % (3253692)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=2814076958:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2871 on theBenchmark for (2871ds/7958Mi) % 150.70/22.84 % (3253693)dis+10_128_sil=16000:nwc=0.7:random_seed=3445405014:i=15999:nm=2:gsp=on_2870 on theBenchmark for (2870ds/15999Mi) % 150.70/22.84 % (3253693)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 150.70/22.84 % Exception at run slice level % 150.70/22.84 User error: GNN currently only supports monomorphic FOL. % 150.70/22.84 % (3253696)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=3958418761:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2866 on theBenchmark for (2866ds/8139Mi) % 150.70/22.84 % (3253562)Instruction limit reached! % 150.70/22.84 % (3253562)------------------------------ % 150.70/22.84 % (3253562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.70/22.84 % (3253562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.70/22.84 % (3253562)CaDiCaL version: 2.1.3 % 150.70/22.84 % (3253562)Termination reason: Instruction limit % 150.70/22.84 % (3253562)Termination phase: Saturation % 150.70/22.84 % (3253562)Time elapsed: 11.712 s % 150.70/22.84 % (3253562)Peak memory usage: 192 MB % 150.70/22.84 % (3253562)Instructions burned: 33336 (million) % 150.70/22.84 % (3253698)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=1634216794:st=4:i=8950:sd=5:ss=axioms_2848 on theBenchmark for (2848ds/8950Mi) % 150.70/22.84 % Exception at run slice level % 150.70/22.84 User error: GNN currently only supports monomorphic FOL. % 150.70/22.84 % (3253700)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=1167338867:i=9809:ins=10:av=off_2845 on theBenchmark for (2845ds/9809Mi) % 150.70/22.84 % Exception at run slice level % 150.70/22.84 User error: GNN currently only supports monomorphic FOL. % 150.70/22.84 % (3253702)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=3327013530:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2842 on theBenchmark for (2842ds/9885Mi) % 150.70/22.84 % Exception at run slice level % 150.70/22.84 User error: GNN currently only supports monomorphic FOL. % 186.07/27.64 % (3253704)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=127352909:cond=fast:i=32078:fgj=on:av=off_2839 on theBenchmark for (2839ds/32078Mi) % 186.07/27.64 % (3253684)Instruction limit reached! % 186.07/27.64 % (3253684)------------------------------ % 186.07/27.64 % (3253684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.07/27.64 % (3253684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.07/27.64 % (3253684)CaDiCaL version: 2.1.3 % 186.07/27.64 % (3253684)Termination reason: Instruction limit % 186.07/27.64 % (3253684)Termination phase: Saturation % 186.07/27.64 % (3253684)Time elapsed: 4.006 s % 186.07/27.64 % (3253684)Peak memory usage: 123 MB % 186.07/27.64 % (3253684)Instructions burned: 7144 (million) % 186.07/27.64 % (3253706)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=1466138147:i=11101:bd=all:ss=axioms:sgt=8_2838 on theBenchmark for (2838ds/11101Mi) % 186.07/27.64 % Exception at run slice level % 186.07/27.64 User error: GNN currently only supports monomorphic FOL. % 186.07/27.64 % (3253708)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=1290651489:cond=on:i=13220:s2at=3:aac=none:fsd=on_2836 on theBenchmark for (2836ds/13220Mi) % 186.07/27.64 % Exception at run slice level % 186.07/27.64 User error: GNN currently only supports monomorphic FOL. % 186.07/27.64 % (3253710)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=1882006970:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2834 on theBenchmark for (2834ds/13528Mi) % 186.07/27.64 % Exception at run slice level % 186.07/27.64 User error: GNN currently only supports monomorphic FOL. % 186.07/27.64 % (3253712)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=2619627147:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2831 on theBenchmark for (2831ds/14854Mi) % 186.07/27.64 % Exception at run slice level % 186.07/27.64 User error: GNN currently only supports monomorphic FOL. % 186.07/27.64 % (3253714)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=2131748375:i=14974:ss=axioms:sgt=16_2828 on theBenchmark for (2828ds/14974Mi) % 186.07/27.64 % Exception at run slice level % 186.07/27.64 User error: GNN currently only supports monomorphic FOL. % 186.07/27.64 % (3253716)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=2283255696:i=33081:aac=none:fgj=on:bd=all:fsr=off_2825 on theBenchmark for (2825ds/33081Mi) % 186.07/27.64 % (3253696)Instruction limit reached! % 186.07/27.64 % (3253696)------------------------------ % 186.07/27.64 % (3253696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.07/27.64 % (3253696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.07/27.64 % (3253696)CaDiCaL version: 2.1.3 % 186.07/27.64 % (3253696)Termination reason: Instruction limit % 186.07/27.64 % (3253696)Termination phase: Saturation % 186.07/27.64 % (3253696)Time elapsed: 4.200 s % 186.07/27.64 % (3253696)Peak memory usage: 123 MB % 186.07/27.64 % (3253696)Instructions burned: 8139 (million) % 186.07/27.64 % Exception at run slice level % 186.07/27.64 User error: GNN currently only supports monomorphic FOL. % 186.07/27.64 % (3253718)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=2683528723:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2823 on theBenchmark for (2823ds/50856Mi) % 186.07/27.64 % (3253719)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=1690424127:i=69865_2822 on theBenchmark for (2822ds/69865Mi) % 186.07/27.64 % Exception at run slice level % 186.07/27.64 User error: GNN currently only supports monomorphic FOL. % 186.07/27.64 % (3253722)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=376186129:cond=fast:i=17802:gtgl=3:gtg=all_2819 on theBenchmark for (2819ds/17802Mi) % 186.07/27.64 % Exception at run slice level % 186.07/27.64 User error: Immediate (shared) subterms of term/literal aa(X2,X0,combs(X2,X1,X0,X5,X4),X3) = sF25(X2,X0,X1,X5,X4,X3) have different types/not well-typed! % 204.56/30.29 % Exception at run slice level % 204.56/30.29 User error: GNN currently only supports monomorphic FOL. % 204.56/30.29 % (3253724)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=3271932026:i=96644_2818 on theBenchmark for (2818ds/96644Mi) % 204.56/30.29 % (3253725)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 204.56/30.29 % (3253725)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=2948537611:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2818 on theBenchmark for (2818ds/21161Mi) % 204.56/30.29 % (3253588)Instruction limit reached! % 204.56/30.29 % (3253588)------------------------------ % 204.56/30.29 % (3253588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.56/30.29 % (3253588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.56/30.29 % (3253588)CaDiCaL version: 2.1.3 % 204.56/30.29 % (3253588)Termination reason: Instruction limit % 204.56/30.29 % (3253588)Termination phase: Saturation % 204.56/30.29 % (3253588)Time elapsed: 14.996 s % 204.56/30.29 % (3253588)Peak memory usage: 466 MB % 204.56/30.29 % (3253588)Instructions burned: 26474 (million) % 204.56/30.29 % (3253728)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=1326941248:i=22761:gtg=all:ss=axioms:fsd=on_2791 on theBenchmark for (2791ds/22761Mi) % 204.56/30.29 % (3253693)Instruction limit reached! % 204.56/30.29 % (3253693)------------------------------ % 204.56/30.29 % (3253693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.56/30.29 % (3253693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.56/30.29 % (3253693)CaDiCaL version: 2.1.3 % 204.56/30.29 % (3253693)Termination reason: Instruction limit % 204.56/30.29 % (3253693)Termination phase: Saturation % 204.56/30.29 % (3253693)Time elapsed: 8.148 s % 204.56/30.29 % (3253693)Peak memory usage: 123 MB % 204.56/30.29 % (3253693)Instructions burned: 16000 (million) % 204.56/30.29 % (3253730)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=2830822452:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2787 on theBenchmark for (2787ds/23713Mi) % 204.56/30.29 % Exception at run slice level % 204.56/30.29 User error: GNN currently only supports monomorphic FOL. % 204.56/30.29 % (3253680)Instruction limit reached! % 204.56/30.29 % (3253680)------------------------------ % 204.56/30.29 % (3253680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.56/30.29 % (3253680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.56/30.29 % (3253680)CaDiCaL version: 2.1.3 % 204.56/30.29 % (3253680)Termination reason: Instruction limit % 204.56/30.29 % (3253680)Termination phase: Saturation % 204.56/30.29 % (3253680)Time elapsed: 9.634 s % 204.56/30.29 % (3253680)Peak memory usage: 154 MB % 204.56/30.29 % (3253680)Instructions burned: 19911 (million) % 204.56/30.29 % (3253732)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=4250901230:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2786 on theBenchmark for (2786ds/26509Mi) % 204.56/30.29 % (3253733)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=4176445841:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2785 on theBenchmark for (2785ds/28957Mi) % 204.56/30.29 % Exception at run slice level % 204.56/30.29 User error: GNN currently only supports monomorphic FOL. % 204.56/30.29 % (3253706)Instruction limit reached! % 204.56/30.29 % (3253706)------------------------------ % 204.56/30.29 % (3253706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.56/30.29 % (3253706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.56/30.29 % (3253706)CaDiCaL version: 2.1.3 % 204.56/30.29 % (3253706)Termination reason: Instruction limit % 204.56/30.29 % (3253706)Termination phase: Saturation % 204.56/30.29 % (3253706)Time elapsed: 5.613 s % 204.56/30.29 % (3253706)Peak memory usage: 144 MB % 204.56/30.29 % (3253706)Instructions burned: 11101 (million) % 204.56/30.29 % (3253737)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=344344642:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2781 on theBenchmark for (2781ds/30082Mi) % 204.56/30.29 % (3253736)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=4169606860:i=29246:s2at=-1:kws=inv_arity:ins=10_2781 on theBenchmark for (2781ds/29246Mi) % 218.78/32.26 % (3253737)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 218.78/32.26 % Exception at run slice level % 218.78/32.26 User error: GNN currently only supports monomorphic FOL. % 218.78/32.26 % Exception at run slice level % 218.78/32.26 User error: GNN currently only supports monomorphic FOL. % 218.78/32.26 % (3253740)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=870855801:i=32262:bd=preordered_2776 on theBenchmark for (2776ds/32262Mi) % 218.78/32.26 % (3253741)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=1066998394:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2776 on theBenchmark for (2776ds/32870Mi) % 218.78/32.26 % Exception at run slice level % 218.78/32.26 User error: GNN currently only supports monomorphic FOL. % 218.78/32.26 % Exception at run slice level % 218.78/32.26 User error: GNN currently only supports monomorphic FOL. % 218.78/32.26 % (3253744)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=2348150874:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2771 on theBenchmark for (2771ds/33295Mi) % 218.78/32.26 % (3253745)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=2908963540:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2771 on theBenchmark for (2771ds/36826Mi) % 218.78/32.26 % Exception at run slice level % 218.78/32.26 User error: GNN currently only supports monomorphic FOL. % 218.78/32.26 % (3253748)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=2614651313:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2766 on theBenchmark for (2766ds/92981Mi) % 218.78/32.26 % Exception at run slice level % 218.78/32.26 User error: GNN currently only supports monomorphic FOL. % 218.78/32.26 % (3253750)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=4261495255:s2pl=on:i=49423_2762 on theBenchmark for (2762ds/49423Mi) % 218.78/32.26 % Exception at run slice level % 218.78/32.26 User error: GNN currently only supports monomorphic FOL. % 218.78/32.26 % (3253752)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=1668112699:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2757 on theBenchmark for (2757ds/57299Mi) % 218.78/32.26 % Exception at run slice level % 218.78/32.26 User error: GNN currently only supports monomorphic FOL. % 218.78/32.26 % (3253754)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=3006643155:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2752 on theBenchmark for (2752ds/127679Mi) % 218.78/32.26 % Exception at run slice level % 218.78/32.26 User error: GNN currently only supports monomorphic FOL. % 218.78/32.26 % (3253756)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=1415258674:i=69402:add=on:aac=none:fsr=off_2747 on theBenchmark for (2747ds/69402Mi) % 218.78/32.26 % Exception at run slice level % 218.78/32.26 User error: GNN currently only supports monomorphic FOL. % 218.78/32.26 % (3253758)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=2121519511:i=100512:doe=on:fgj=on:bd=all:fsd=on_2742 on theBenchmark for (2742ds/100512Mi) % 218.78/32.26 % Exception at run slice level % 218.78/32.26 User error: GNN currently only supports monomorphic FOL. % 218.78/32.26 % (3253760)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=3210836087:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2738 on theBenchmark for (2738ds/138761Mi) % 218.78/32.26 % Exception at run slice level % 218.78/32.26 User error: GNN currently only supports monomorphic FOL. % 218.78/32.26 % (3253762)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=2379886385:i=282386:rtra=on_2733 on theBenchmark for (2733ds/282386Mi) % 230.78/33.93 % Exception at run slice level % 230.78/33.93 User error: GNN currently only supports monomorphic FOL. % 230.78/33.93 % (3253764)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=1236641065:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2728 on theBenchmark for (2728ds/269354Mi) % 230.78/33.93 % Exception at run slice level % 230.78/33.93 User error: GNN currently only supports monomorphic FOL. % 230.78/33.93 % (3253766)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=1836652666:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2723 on theBenchmark for (2723ds/283390Mi) % 230.78/33.93 % (3253766)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 230.78/33.93 % Exception at run slice level % 230.78/33.93 User error: GNN currently only supports monomorphic FOL. % 230.78/33.93 % (3253768)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=4149282881:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2718 on theBenchmark for (2718ds/218Mi) % 230.78/33.93 % (3253768)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 230.78/33.93 % (3253768)Refutation not found, incomplete strategy % 230.78/33.93 % (3253768)------------------------------ % 230.78/33.93 % (3253768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.78/33.93 % (3253768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.78/33.93 % (3253768)CaDiCaL version: 2.1.3 % 230.78/33.93 % (3253768)Termination reason: Refutation not found, incomplete strategy % 230.78/33.93 % (3253768)Time elapsed: 0.016 s % 230.78/33.93 % (3253768)Peak memory usage: 89 MB % 230.78/33.93 % (3253768)Instructions burned: 27 (million) % 230.78/33.93 % (3253768)------------------------------ % 230.78/33.93 % (3253768)------------------------------ % 230.78/33.93 % (3253770)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=1042963854:i=238:av=off:rtra=on:ss=axioms_2714 on theBenchmark for (2714ds/238Mi) % 230.78/33.93 % (3253770)Instruction limit reached! % 230.78/33.93 % (3253770)------------------------------ % 230.78/33.93 % (3253770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.78/33.93 % (3253770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.78/33.93 % (3253770)CaDiCaL version: 2.1.3 % 230.78/33.93 % (3253770)Termination reason: Instruction limit % 230.78/33.93 % (3253770)Termination phase: Saturation % 230.78/33.93 % (3253770)Time elapsed: 0.140 s % 230.78/33.93 % (3253770)Peak memory usage: 90 MB % 230.78/33.93 % (3253770)Instructions burned: 238 (million) % 230.78/33.93 % (3253772)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=1712767767:s2a=on:i=278:rtra=on:gtg=position_2712 on theBenchmark for (2712ds/278Mi) % 230.78/33.93 % (3253772)Instruction limit reached! % 230.78/33.93 % (3253772)------------------------------ % 230.78/33.93 % (3253772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.78/33.93 % (3253772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.78/33.93 % (3253772)CaDiCaL version: 2.1.3 % 230.78/33.93 % (3253772)Termination reason: Instruction limit % 230.78/33.93 % (3253772)Termination phase: Saturation % 230.78/33.93 % (3253772)Time elapsed: 0.174 s % 230.78/33.93 % (3253772)Peak memory usage: 91 MB % 230.78/33.93 % (3253772)Instructions burned: 278 (million) % 230.78/33.93 % (3253774)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=2255496156:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2709 on theBenchmark for (2709ds/258Mi) % 230.78/33.93 % (3253774)Instruction limit reached! % 230.78/33.93 % (3253774)------------------------------ % 230.78/33.93 % (3253774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.78/33.93 % (3253774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.78/33.93 % (3253774)CaDiCaL version: 2.1.3 % 230.78/33.93 % (3253774)Termination reason: Instruction limit % 230.78/33.93 % (3253774)Termination phase: Saturation % 230.78/33.93 % (3253774)Time elapsed: 0.125 s % 230.78/33.93 % (3253774)Peak memory usage: 92 MB % 230.78/33.93 % (3253774)Instructions burned: 260 (million) % 230.78/33.93 % (3253776)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=933211381:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2706 on theBenchmark for (2706ds/570Mi) % 238.85/35.07 % (3253776)Instruction limit reached! % 238.85/35.07 % (3253776)------------------------------ % 238.85/35.07 % (3253776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.85/35.07 % (3253776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.85/35.07 % (3253776)CaDiCaL version: 2.1.3 % 238.85/35.07 % (3253776)Termination reason: Instruction limit % 238.85/35.07 % (3253776)Termination phase: Saturation % 238.85/35.07 % (3253776)Time elapsed: 0.351 s % 238.85/35.07 % (3253776)Peak memory usage: 92 MB % 238.85/35.07 % (3253776)Instructions burned: 571 (million) % 238.85/35.07 % (3253778)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=1156704440:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2702 on theBenchmark for (2702ds/314Mi) % 238.85/35.07 % (3253778)Instruction limit reached! % 238.85/35.07 % (3253778)------------------------------ % 238.85/35.07 % (3253778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.85/35.07 % (3253778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.85/35.07 % (3253778)CaDiCaL version: 2.1.3 % 238.85/35.07 % (3253778)Termination reason: Instruction limit % 238.85/35.07 % (3253778)Termination phase: Saturation % 238.85/35.07 % (3253778)Time elapsed: 0.178 s % 238.85/35.07 % (3253778)Peak memory usage: 91 MB % 238.85/35.07 % (3253778)Instructions burned: 316 (million) % 238.85/35.07 % (3253780)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=1337194830:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2698 on theBenchmark for (2698ds/650Mi) % 238.85/35.07 % (3253780)Instruction limit reached! % 238.85/35.07 % (3253780)------------------------------ % 238.85/35.07 % (3253780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.85/35.07 % (3253780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.85/35.07 % (3253780)CaDiCaL version: 2.1.3 % 238.85/35.07 % (3253780)Termination reason: Instruction limit % 238.85/35.07 % (3253780)Termination phase: Saturation % 238.85/35.07 % (3253780)Time elapsed: 0.406 s % 238.85/35.07 % (3253780)Peak memory usage: 93 MB % 238.85/35.07 % (3253780)Instructions burned: 651 (million) % 238.85/35.07 % (3253782)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=2671275617:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2693 on theBenchmark for (2693ds/496Mi) % 238.85/35.07 % (3253725)Instruction limit reached! % 238.85/35.07 % (3253725)------------------------------ % 238.85/35.07 % (3253725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.85/35.07 % (3253725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.85/35.07 % (3253725)CaDiCaL version: 2.1.3 % 238.85/35.07 % (3253725)Termination reason: Instruction limit % 238.85/35.07 % (3253725)Termination phase: Saturation % 238.85/35.07 % (3253725)Time elapsed: 12.737 s % 238.85/35.07 % (3253725)Peak memory usage: 194 MB % 238.85/35.07 % (3253725)Instructions burned: 21163 (million) % 238.85/35.07 % (3253782)Instruction limit reached! % 238.85/35.07 % (3253782)------------------------------ % 238.85/35.07 % (3253782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.85/35.07 % (3253782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.85/35.07 % (3253782)CaDiCaL version: 2.1.3 % 238.85/35.07 % (3253782)Termination reason: Instruction limit % 238.85/35.07 % (3253782)Termination phase: Saturation % 238.85/35.07 % (3253782)Time elapsed: 0.284 s % 238.85/35.07 % (3253782)Peak memory usage: 92 MB % 238.85/35.07 % (3253782)Instructions burned: 496 (million) % 238.85/35.07 % (3253784)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=3156054124:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2689 on theBenchmark for (2689ds/588Mi) % 238.85/35.07 % (3253785)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=827142265:i=4700:rtra=on_2689 on theBenchmark for (2689ds/4700Mi) % 238.85/35.07 % (3253784)Refutation not found, incomplete strategy % 238.85/35.07 % (3253784)------------------------------ % 238.85/35.07 % (3253784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.85/35.07 % (3253784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.85/35.07 % (3253784)CaDiCaL version: 2.1.3 % 238.85/35.07 % (3253784)Termination reason: Refutation not found, incomplete strategy % 238.85/35.07 % (3253784)Time elapsed: 0.011 s % 238.85/35.07 % (3253784)Peak memory usage: 89 MB % 238.85/35.07 % (3253784)Instructions burned: 16 (million) % 238.85/35.07 % (3253784)------------------------------ % 238.85/35.07 % (3253784)------------------------------ % 246.69/36.18 % Exception at run slice level % 246.69/36.18 User error: GNN currently only supports monomorphic FOL. % 246.69/36.18 % (3253788)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2885953506:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2685 on theBenchmark for (2685ds/226Mi) % 246.69/36.18 % (3253789)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4071594789:i=254:av=off:fsr=off:rtra=on:sup=off_2684 on theBenchmark for (2684ds/254Mi) % 246.69/36.18 % (3253788)Instruction limit reached! % 246.69/36.18 % (3253788)------------------------------ % 246.69/36.18 % (3253788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.69/36.18 % (3253788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.69/36.18 % (3253788)CaDiCaL version: 2.1.3 % 246.69/36.18 % (3253788)Termination reason: Instruction limit % 246.69/36.18 % (3253788)Termination phase: Saturation % 246.69/36.18 % (3253788)Time elapsed: 0.127 s % 246.69/36.18 % (3253788)Peak memory usage: 90 MB % 246.69/36.18 % (3253788)Instructions burned: 227 (million) % 246.69/36.18 % (3253789)Instruction limit reached! % 246.69/36.18 % (3253789)------------------------------ % 246.69/36.18 % (3253789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.69/36.18 % (3253789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.69/36.18 % (3253789)CaDiCaL version: 2.1.3 % 246.69/36.18 % (3253789)Termination reason: Instruction limit % 246.69/36.18 % (3253789)Termination phase: Saturation % 246.69/36.18 % (3253789)Time elapsed: 0.126 s % 246.69/36.18 % (3253789)Peak memory usage: 90 MB % 246.69/36.18 % (3253789)Instructions burned: 255 (million) % 246.69/36.18 % (3253792)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=664269654:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2683 on theBenchmark for (2683ds/228Mi) % 246.69/36.18 % (3253792)Refutation not found, incomplete strategy % 246.69/36.18 % (3253792)------------------------------ % 246.69/36.18 % (3253792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.69/36.18 % (3253792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.69/36.18 % (3253792)CaDiCaL version: 2.1.3 % 246.69/36.18 % (3253792)Termination reason: Refutation not found, incomplete strategy % 246.69/36.18 % (3253792)Time elapsed: 0.042 s % 246.69/36.18 % (3253792)Peak memory usage: 89 MB % 246.69/36.18 % (3253792)Instructions burned: 80 (million) % 246.69/36.18 % (3253793)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=1925350144:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2682 on theBenchmark for (2682ds/1814Mi) % 246.69/36.18 % (3253792)------------------------------ % 246.69/36.18 % (3253792)------------------------------ % 246.69/36.18 % (3253796)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=148986347:i=874:sd=1:aac=none:rtra=on:ss=included_2679 on theBenchmark for (2679ds/874Mi) % 246.69/36.18 % (3253796)Refutation not found, incomplete strategy % 246.69/36.18 % (3253796)------------------------------ % 246.69/36.18 % (3253796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.69/36.18 % (3253796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.69/36.18 % (3253796)CaDiCaL version: 2.1.3 % 246.69/36.18 % (3253796)Termination reason: Refutation not found, incomplete strategy % 246.69/36.18 % (3253796)Time elapsed: 0.011 s % 246.69/36.18 % (3253796)Peak memory usage: 89 MB % 246.69/36.18 % (3253796)Instructions burned: 17 (million) % 246.69/36.18 % (3253796)------------------------------ % 246.69/36.18 % (3253796)------------------------------ % 246.69/36.18 % (3253798)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=3418068373:i=10404:rtra=on:ss=axioms:sgt=16_2675 on theBenchmark for (2675ds/10404Mi) % 246.69/36.18 % Exception at run slice level % 246.69/36.18 User error: GNN currently only supports monomorphic FOL. % 246.69/36.18 % (3253793)Instruction limit reached! % 246.69/36.18 % (3253793)------------------------------ % 246.69/36.18 % (3253793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.69/36.18 % (3253793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.69/36.18 % (3253793)CaDiCaL version: 2.1.3 % 246.69/36.18 % (3253793)Termination reason: Instruction limit % 246.69/36.18 % (3253793)Termination phase: Saturation % 246.69/36.18 % (3253793)Time elapsed: 1.133 s % 246.69/36.18 % (3253793)Peak memory usage: 98 MB % 246.69/36.18 % (3253793)Instructions burned: 1815 (million) % 246.69/36.18 % (3253800)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=80667508:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2670 on theBenchmark for (2670ds/268Mi) % 256.23/37.53 % (3253801)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=2241782173:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2669 on theBenchmark for (2669ds/1184Mi) % 256.23/37.53 % (3253801)Refutation not found, incomplete strategy % 256.23/37.53 % (3253801)------------------------------ % 256.23/37.53 % (3253801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.23/37.53 % (3253801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.23/37.53 % (3253801)CaDiCaL version: 2.1.3 % 256.23/37.53 % (3253801)Termination reason: Refutation not found, incomplete strategy % 256.23/37.53 % (3253801)Time elapsed: 0.009 s % 256.23/37.53 % (3253801)Peak memory usage: 89 MB % 256.23/37.53 % (3253801)Instructions burned: 13 (million) % 256.23/37.53 % (3253800)Instruction limit reached! % 256.23/37.53 % (3253800)------------------------------ % 256.23/37.53 % (3253800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.23/37.53 % (3253800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.23/37.53 % (3253800)CaDiCaL version: 2.1.3 % 256.23/37.53 % (3253800)Termination reason: Instruction limit % 256.23/37.53 % (3253800)Termination phase: Saturation % 256.23/37.53 % (3253800)Time elapsed: 0.154 s % 256.23/37.53 % (3253800)Peak memory usage: 91 MB % 256.23/37.53 % (3253800)Instructions burned: 270 (million) % 256.23/37.53 % (3253804)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=1163255966:st=3:i=26386:sd=3:rtra=on:ss=axioms_2667 on theBenchmark for (2667ds/26386Mi) % 256.23/37.53 % (3253801)------------------------------ % 256.23/37.53 % (3253801)------------------------------ % 256.23/37.53 % (3253806)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=3359081870:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2665 on theBenchmark for (2665ds/250Mi) % 256.23/37.53 % (3253806)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 256.23/37.53 % (3253806)Instruction limit reached! % 256.23/37.53 % (3253806)------------------------------ % 256.23/37.53 % (3253806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.23/37.53 % (3253806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.23/37.53 % (3253806)CaDiCaL version: 2.1.3 % 256.23/37.53 % (3253806)Termination reason: Instruction limit % 256.23/37.53 % (3253806)Termination phase: Saturation % 256.23/37.53 % (3253806)Time elapsed: 0.153 s % 256.23/37.53 % (3253806)Peak memory usage: 92 MB % 256.23/37.53 % (3253806)Instructions burned: 251 (million) % 256.23/37.53 % Exception at run slice level % 256.23/37.53 User error: GNN currently only supports monomorphic FOL. % 256.23/37.53 % (3253808)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=3949508679:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2663 on theBenchmark for (2663ds/268Mi) % 256.23/37.53 % Exception at run slice level % 256.23/37.53 User error: Immediate (shared) subterms of term/literal aa(fun(X2,X0),fun(X2,X1),sF55(X0,X1,X2,X3),X5) = sF56(X2,X0,X1,X3,X5) have different types/not well-typed! % 256.23/37.53 % (3253809)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2647800068:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2662 on theBenchmark for (2662ds/282Mi) % 256.23/37.53 % (3253809)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 256.23/37.53 % (3253809)Refutation not found, incomplete strategy % 256.23/37.53 % (3253809)------------------------------ % 256.23/37.53 % (3253809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.23/37.53 % (3253809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.23/37.53 % (3253809)CaDiCaL version: 2.1.3 % 256.23/37.53 % (3253809)Termination reason: Refutation not found, incomplete strategy % 256.23/37.53 % (3253809)Time elapsed: 0.006 s % 256.23/37.53 % (3253809)Peak memory usage: 89 MB % 256.23/37.53 % (3253809)Instructions burned: 9 (million) % 256.23/37.53 % (3253811)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=1394610040:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2661 on theBenchmark for (2661ds/862Mi) % 256.23/37.53 % (3253809)------------------------------ % 256.23/37.53 % (3253809)------------------------------ % 256.23/37.53 % (3253814)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=2575907060:i=12120:aac=none:ins=25:rtra=on_2659 on theBenchmark for (2659ds/12120Mi) % 268.44/39.25 % (3253811)Instruction limit reached! % 268.44/39.25 % (3253811)------------------------------ % 268.44/39.25 % (3253811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.44/39.25 % (3253811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.44/39.25 % (3253811)CaDiCaL version: 2.1.3 % 268.44/39.25 % (3253811)Termination reason: Instruction limit % 268.44/39.25 % (3253811)Termination phase: Saturation % 268.44/39.25 % (3253811)Time elapsed: 0.431 s % 268.44/39.25 % (3253811)Peak memory usage: 96 MB % 268.44/39.25 % (3253811)Instructions burned: 864 (million) % 268.44/39.25 % (3253816)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=1608214515:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2656 on theBenchmark for (2656ds/300Mi) % 268.44/39.25 % (3253816)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 268.44/39.25 % Exception at run slice level % 268.44/39.25 User error: GNN currently only supports monomorphic FOL. % 268.44/39.25 % (3253816)Instruction limit reached! % 268.44/39.25 % (3253816)------------------------------ % 268.44/39.25 % (3253816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.44/39.25 % (3253816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.44/39.25 % (3253816)CaDiCaL version: 2.1.3 % 268.44/39.25 % (3253816)Termination reason: Instruction limit % 268.44/39.25 % (3253816)Termination phase: Saturation % 268.44/39.25 % (3253816)Time elapsed: 0.154 s % 268.44/39.25 % (3253816)Peak memory usage: 91 MB % 268.44/39.25 % (3253816)Instructions burned: 300 (million) % 268.44/39.25 % (3253730)Instruction limit reached! % 268.44/39.25 % (3253730)------------------------------ % 268.44/39.25 % (3253730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.44/39.25 % (3253730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.44/39.25 % (3253730)CaDiCaL version: 2.1.3 % 268.44/39.25 % (3253730)Termination reason: Instruction limit % 268.44/39.25 % (3253730)Termination phase: Saturation % 268.44/39.25 % (3253730)Time elapsed: 13.382 s % 268.44/39.25 % (3253730)Peak memory usage: 121 MB % 268.44/39.25 % (3253730)Instructions burned: 23713 (million) % 268.44/39.25 % (3253818)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=2288278762:i=28310:bd=all:rtra=on_2654 on theBenchmark for (2654ds/28310Mi) % 268.44/39.25 % (3253819)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2930867215:i=1334:av=off:fsr=off:rtra=on_2653 on theBenchmark for (2653ds/1334Mi) % 268.44/39.25 % (3253821)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=1897846604:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2652 on theBenchmark for (2652ds/370Mi) % 268.44/39.25 % (3253821)Instruction limit reached! % 268.44/39.25 % (3253821)------------------------------ % 268.44/39.25 % (3253821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.44/39.25 % (3253821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.44/39.25 % (3253821)CaDiCaL version: 2.1.3 % 268.44/39.25 % (3253821)Termination reason: Instruction limit % 268.44/39.25 % (3253821)Termination phase: Saturation % 268.44/39.25 % (3253821)Time elapsed: 0.234 s % 268.44/39.25 % (3253821)Peak memory usage: 93 MB % 268.44/39.25 % (3253821)Instructions burned: 371 (million) % 268.44/39.25 % Exception at run slice level % 268.44/39.25 User error: GNN currently only supports monomorphic FOL. % 268.44/39.25 % (3253824)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=361280491:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2649 on theBenchmark for (2649ds/386Mi) % 268.44/39.25 % (3253825)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=2305573385:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2649 on theBenchmark for (2649ds/9700Mi) % 268.44/39.25 % (3253819)Instruction limit reached! % 268.44/39.25 % (3253819)------------------------------ % 268.44/39.25 % (3253819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.44/39.25 % (3253819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.95/41.31 % (3253819)CaDiCaL version: 2.1.3 % 282.95/41.31 % (3253819)Termination reason: Instruction limit % 282.95/41.31 % (3253819)Termination phase: Saturation % 282.95/41.31 % (3253819)Time elapsed: 0.541 s % 282.95/41.31 % (3253819)Peak memory usage: 101 MB % 282.95/41.31 % (3253819)Instructions burned: 1336 (million) % 282.95/41.31 % (3253824)Instruction limit reached! % 282.95/41.31 % (3253824)------------------------------ % 282.95/41.31 % (3253824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.95/41.31 % (3253824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.95/41.31 % (3253824)CaDiCaL version: 2.1.3 % 282.95/41.31 % (3253824)Termination reason: Instruction limit % 282.95/41.31 % (3253824)Termination phase: Saturation % 282.95/41.31 % (3253824)Time elapsed: 0.231 s % 282.95/41.31 % (3253824)Peak memory usage: 93 MB % 282.95/41.31 % (3253824)Instructions burned: 386 (million) % 282.95/41.31 % (3253828)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=1356481517:i=24222:sd=1:rtra=on:ss=included_2646 on theBenchmark for (2646ds/24222Mi) % 282.95/41.31 % (3253829)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=563869886:i=638:kws=precedence:fsr=off:rtra=on_2645 on theBenchmark for (2645ds/638Mi) % 282.95/41.31 % Exception at run slice level % 282.95/41.31 User error: GNN currently only supports monomorphic FOL. % 282.95/41.31 % (3253829)Instruction limit reached! % 282.95/41.31 % (3253829)------------------------------ % 282.95/41.31 % (3253829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.95/41.31 % (3253829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.95/41.31 % (3253829)CaDiCaL version: 2.1.3 % 282.95/41.31 % (3253829)Termination reason: Instruction limit % 282.95/41.31 % (3253829)Termination phase: Saturation % 282.95/41.31 % (3253829)Time elapsed: 0.371 s % 282.95/41.31 % (3253829)Peak memory usage: 94 MB % 282.95/41.31 % (3253829)Instructions burned: 639 (million) % 282.95/41.31 % (3253832)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3585419428:i=4128:ep=RST:rtra=on_2641 on theBenchmark for (2641ds/4128Mi) % 282.95/41.31 % (3253832)Refutation not found, incomplete strategy % 282.95/41.31 % (3253832)------------------------------ % 282.95/41.31 % (3253832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.95/41.31 % (3253832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.95/41.31 % (3253832)CaDiCaL version: 2.1.3 % 282.95/41.31 % (3253832)Termination reason: Refutation not found, incomplete strategy % 282.95/41.31 % (3253832)Time elapsed: 0.008 s % 282.95/41.31 % (3253832)Peak memory usage: 88 MB % 282.95/41.31 % (3253832)Instructions burned: 13 (million) % 282.95/41.31 % (3253833)dis-1011_128_sil=32000:si=on:random_seed=879104398:i=7412:ep=RST:av=off:rtra=on_2640 on theBenchmark for (2640ds/7412Mi) % 282.95/41.31 % (3253832)------------------------------ % 282.95/41.31 % (3253832)------------------------------ % 282.95/41.31 % (3253836)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=371761537:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2638 on theBenchmark for (2638ds/1514Mi) % 282.95/41.31 % (3253836)Refutation not found, incomplete strategy % 282.95/41.31 % (3253836)------------------------------ % 282.95/41.31 % (3253836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.95/41.31 % (3253836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.95/41.31 % (3253836)CaDiCaL version: 2.1.3 % 282.95/41.31 % (3253836)Termination reason: Refutation not found, incomplete strategy % 282.95/41.31 % (3253836)Time elapsed: 0.010 s % 282.95/41.31 % (3253836)Peak memory usage: 89 MB % 282.95/41.31 % (3253836)Instructions burned: 15 (million) % 282.95/41.31 % (3253654)Instruction limit reached! % 282.95/41.31 % (3253654)------------------------------ % 282.95/41.31 % (3253654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.95/41.31 % (3253654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.95/41.31 % (3253654)CaDiCaL version: 2.1.3 % 282.95/41.31 % (3253654)Termination reason: Instruction limit % 282.95/41.31 % (3253654)Termination phase: Saturation % 282.95/41.31 % (3253654)Time elapsed: 26.356 s % 282.95/41.31 % (3253654)Peak memory usage: 214 MB % 282.95/41.31 % (3253654)Instructions burned: 43698 (million) % 282.95/41.31 % (3253836)------------------------------ % 282.95/41.31 % (3253836)------------------------------ % 282.95/41.31 % (3253838)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=2614759218:i=27826:rtra=on:ss=axioms:sgt=8_2634 on theBenchmark for (2634ds/27826Mi) % 300.36/43.83 % (3253839)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=1946631709:i=19850:aac=none:rtra=on_2634 on theBenchmark for (2634ds/19850Mi) % 300.36/43.83 % Exception at run slice level % 300.36/43.83 User error: GNN currently only supports monomorphic FOL. % 300.36/43.83 % Exception at run slice level % 300.36/43.83 User error: GNN currently only supports monomorphic FOL. % 300.36/43.83 % (3253842)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1922653952:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2629 on theBenchmark for (2629ds/4958Mi) % 300.36/43.83 % (3253843)ott+1002_64_sil=16000:si=on:sp=const_min:nwc=0.5:random_seed=3108774220:i=880:nm=2:av=off:rtra=on:gtg=exists_all:fdi=8:gsp=on_2629 on theBenchmark for (2629ds/880Mi) % 300.36/43.83 % (3253843)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.36/43.83 % (3253842)Refutation not found, incomplete strategy % 300.36/43.83 % (3253842)------------------------------ % 300.36/43.83 % (3253842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.36/43.83 % (3253842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.36/43.83 % (3253842)CaDiCaL version: 2.1.3 % 300.36/43.83 % (3253842)Termination reason: Refutation not found, incomplete strategy % 300.36/43.83 % (3253842)Time elapsed: 0.014 s % 300.36/43.83 % (3253842)Peak memory usage: 89 MB % 300.36/43.83 % (3253842)Instructions burned: 22 (million) % 300.36/43.83 % (3253842)------------------------------ % 300.36/43.83 % (3253842)------------------------------ % 300.36/43.83 % (3253846)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=3435570802:st=1.5:i=22290:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2625 on theBenchmark for (2625ds/22290Mi) % 300.36/43.83 % (3253843)Instruction limit reached! % 300.36/43.83 % (3253843)------------------------------ % 300.36/43.83 % (3253843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.36/43.83 % (3253843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.36/43.83 % (3253843)CaDiCaL version: 2.1.3 % 300.36/43.83 % (3253843)Termination reason: Instruction limit % 300.36/43.83 % (3253843)Termination phase: Saturation % 300.36/43.83 % (3253843)Time elapsed: 0.444 s % 300.36/43.83 % (3253843)Peak memory usage: 96 MB % 300.36/43.83 % (3253843)Instructions burned: 880 (million) % 300.36/43.83 % (3253733)Instruction limit reached! % 300.36/43.83 % (3253733)------------------------------ % 300.36/43.83 % (3253733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.36/43.83 % (3253733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.36/43.83 % (3253733)CaDiCaL version: 2.1.3 % 300.36/43.83 % (3253733)Termination reason: Instruction limit % 300.36/43.83 % (3253733)Termination phase: Saturation % 300.36/43.83 % (3253733)Time elapsed: 16.118 s % 300.36/43.83 % (3253733)Peak memory usage: 194 MB % 300.36/43.83 % (3253733)Instructions burned: 28957 (million) % 300.36/43.83 % (3253848)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=1142775414:cts=off:i=6068:av=off:rtra=on:er=known:fsd=on_2623 on theBenchmark for (2623ds/6068Mi) % 300.36/43.83 % (3253849)lrs-1011_64:1_sil=8000:si=on:erd=off:urr=on:nwc=0.7:br=off:random_seed=3928620331:st=2:s2a=on:i=1048:s2at=2:rtra=on:ss=axioms_2622 on theBenchmark for (2622ds/1048Mi) % 300.36/43.83 % Exception at run slice level % 300.36/43.83 User error: GNN currently only supports monomorphic FOL. % 300.36/43.83 % (3253852)lrs+1011_16:1_sil=8000:si=on:acc=on:urr=on:fd=preordered:flr=on:random_seed=266436294:avsq=on:i=2032:avsqr=676809,524288:sd=1:rtra=on:ss=axioms_2620 on theBenchmark for (2620ds/2032Mi) % 300.36/43.83 % Exception at run slice level % 300.36/43.83 User error: GNN currently only supports monomorphic FOL. % 300.36/43.83 % (3253854)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:si=on:s2agt=16:random_seed=2854080664:i=28246:bd=preordered:ins=4:rtra=on_2618 on theBenchmark for (2618ds/28246Mi) % 300.36/43.83 % (3253849)Instruction limit reached! % 300.36/43.83 % (3253849)------------------------------ % 300.36/43.83 % (3253849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.36/43.83 % (3253849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178- % 300.36/43.83 Terminated %------------------------------------------------------------------------------