%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV609_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:19:05 PM UTC 2026 % Result : Timeout 295.02s 42.23s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV609_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.20 % Computer : n014.cluster.edu % 0.08/0.20 % Model : x86_64 x86_64 % 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.20 % Memory : 8046.5625MB % 0.08/0.20 % OS : Linux 6.8.0-71-generic % 0.08/0.20 % CPULimit : 300 % 0.08/0.20 % WCLimit : 300 % 0.08/0.20 % DateTime : Mon Sep 28 12:01:01 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.23 Running first-order theorem proving % 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.59/1.69 % (1735699)Detected formulas, will run a generic FOF schedule. % 5.59/1.69 % (1735708)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4230284452:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 5.59/1.69 % (1735705)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=1756321828:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 5.59/1.69 % (1735708)Instruction limit reached! % 5.59/1.69 % (1735708)------------------------------ % 5.59/1.69 % (1735708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.59/1.69 % (1735708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.59/1.69 % (1735708)CaDiCaL version: 2.1.3 % 5.59/1.69 % (1735708)Termination reason: Instruction limit % 5.59/1.69 % (1735708)Termination phase: Saturation % 5.59/1.69 % (1735708)Time elapsed: 0.039 s % 5.59/1.69 % (1735708)Peak memory usage: 88 MB % 5.59/1.69 % (1735708)Instructions burned: 120 (million) % 5.59/1.69 % (1735706)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=619686318:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 5.59/1.69 % (1735704)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=2569734778:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 5.59/1.69 % (1735706)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.59/1.69 % (1735707)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1278668404:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 5.59/1.69 % (1735707)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.59/1.69 % (1735707)Refutation not found, incomplete strategy % 5.59/1.69 % (1735707)------------------------------ % 5.59/1.69 % (1735707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.59/1.69 % (1735707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.59/1.69 % (1735707)CaDiCaL version: 2.1.3 % 5.59/1.69 % (1735707)Termination reason: Refutation not found, incomplete strategy % 5.59/1.69 % (1735707)Time elapsed: 0.002 s % 5.59/1.69 % (1735707)Peak memory usage: 88 MB % 5.59/1.69 % (1735707)Instructions burned: 2 (million) % 5.59/1.69 % (1735710)dis-21_1_sil=8000:lcm=predicate:random_seed=4212086293:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 5.59/1.69 % (1735709)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=678455041:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 5.59/1.69 % (1735710)Instruction limit reached! % 5.59/1.69 % (1735710)------------------------------ % 5.59/1.69 % (1735710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.59/1.69 % (1735710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.59/1.69 % (1735710)CaDiCaL version: 2.1.3 % 5.59/1.69 % (1735710)Termination reason: Instruction limit % 5.59/1.69 % (1735710)Termination phase: Saturation % 5.59/1.69 % (1735710)Time elapsed: 0.066 s % 5.59/1.69 % (1735710)Peak memory usage: 88 MB % 5.59/1.70 % (1735710)Instructions burned: 131 (million) % 5.59/1.70 % (1735715)lrs+10_1_sil=8000:sp=occurrence:random_seed=3261171081:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi) % 5.59/1.70 % (1735709)Instruction limit reached! % 5.59/1.70 % (1735709)------------------------------ % 5.59/1.70 % (1735709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.59/1.70 % (1735709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.59/1.70 % (1735709)CaDiCaL version: 2.1.3 % 5.59/1.70 % (1735709)Termination reason: Instruction limit % 5.59/1.70 % (1735709)Termination phase: Saturation % 5.59/1.70 % (1735709)Time elapsed: 0.093 s % 5.59/1.70 % (1735709)Peak memory usage: 89 MB % 5.59/1.70 % (1735709)Instructions burned: 140 (million) % 5.59/1.70 % (1735715)Instruction limit reached! % 5.59/1.70 % (1735715)------------------------------ % 5.59/1.70 % (1735715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.59/1.70 % (1735715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.59/1.70 % (1735715)CaDiCaL version: 2.1.3 % 7.66/1.98 % (1735715)Termination reason: Instruction limit % 7.66/1.98 % (1735715)Termination phase: Saturation % 7.66/1.98 % (1735715)Time elapsed: 0.096 s % 7.66/1.98 % (1735715)Peak memory usage: 90 MB % 7.66/1.98 % (1735715)Instructions burned: 290 (million) % 7.66/1.98 % (1735719)lrs+10_1_sil=32000:urr=on:br=off:random_seed=365508762:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 7.66/1.98 % (1735721)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1859838201:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 7.66/1.98 % (1735707)------------------------------ % 7.66/1.98 % (1735707)------------------------------ % 7.66/1.98 % (1735722)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=3387844808:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi) % 7.66/1.98 % (1735719)Instruction limit reached! % 7.66/1.98 % (1735719)------------------------------ % 7.66/1.98 % (1735719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.66/1.98 % (1735719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.66/1.98 % (1735719)CaDiCaL version: 2.1.3 % 7.66/1.98 % (1735719)Termination reason: Instruction limit % 7.66/1.98 % (1735719)Termination phase: Saturation % 7.66/1.98 % (1735719)Time elapsed: 0.077 s % 7.66/1.98 % (1735719)Peak memory usage: 90 MB % 7.66/1.98 % (1735719)Instructions burned: 158 (million) % 7.66/1.98 % (1735722)Instruction limit reached! % 7.66/1.98 % (1735722)------------------------------ % 7.66/1.98 % (1735722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.66/1.98 % (1735722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.66/1.98 % (1735722)CaDiCaL version: 2.1.3 % 7.66/1.98 % (1735722)Termination reason: Instruction limit % 7.66/1.98 % (1735722)Termination phase: Saturation % 7.66/1.98 % (1735722)Time elapsed: 0.077 s % 7.66/1.98 % (1735722)Peak memory usage: 90 MB % 7.66/1.98 % (1735722)Instructions burned: 251 (million) % 7.66/1.98 % Exception at run slice level % 7.66/1.98 User error: GNN currently only supports monomorphic FOL. % 7.66/1.98 % Exception at run slice level % 7.66/1.98 User error: GNN currently only supports monomorphic FOL. % 7.66/1.98 % Exception at run slice level % 7.66/1.98 User error: GNN currently only supports monomorphic FOL. % 7.66/1.98 % (1735725)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1917314824:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 7.66/1.98 % (1735725)Refutation not found, incomplete strategy % 7.66/1.98 % (1735725)------------------------------ % 7.66/1.98 % (1735725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.66/1.98 % (1735725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.66/1.98 % (1735725)CaDiCaL version: 2.1.3 % 7.66/1.98 % (1735725)Termination reason: Refutation not found, incomplete strategy % 7.66/1.98 % (1735725)Time elapsed: 0.007 s % 7.66/1.98 % (1735725)Peak memory usage: 88 MB % 7.66/1.98 % (1735725)Instructions burned: 11 (million) % 7.66/1.98 % (1735727)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=155214821:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 7.66/1.98 % (1735728)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1112357923:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi) % 7.66/1.98 % (1735721)Instruction limit reached! % 7.66/1.98 % (1735721)------------------------------ % 7.66/1.98 % (1735721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.66/1.98 % (1735721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.66/1.98 % (1735721)CaDiCaL version: 2.1.3 % 7.66/1.98 % (1735721)Termination reason: Instruction limit % 7.66/1.98 % (1735721)Termination phase: Saturation % 7.66/1.98 % (1735721)Time elapsed: 0.208 s % 7.66/1.98 % (1735721)Peak memory usage: 91 MB % 7.66/1.98 % (1735721)Instructions burned: 325 (million) % 7.66/1.98 % (1735728)Instruction limit reached! % 7.66/1.98 % (1735728)------------------------------ % 7.66/1.98 % (1735728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.66/1.98 % (1735728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.66/1.98 % (1735728)CaDiCaL version: 2.1.3 % 7.66/1.98 % (1735728)Termination reason: Instruction limit % 7.66/1.98 % (1735728)Termination phase: Saturation % 7.66/1.98 % (1735728)Time elapsed: 0.038 s % 7.66/1.98 % (1735728)Peak memory usage: 89 MB % 7.66/1.98 % (1735728)Instructions burned: 113 (million) % 10.76/2.25 % (1735731)lrs+10_1_sil=8000:sp=occurrence:random_seed=1611463529:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 10.76/2.25 % (1735730)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1702202:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 10.76/2.25 % (1735729)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1979541265:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 10.76/2.25 % (1735730)Refutation not found, incomplete strategy % 10.76/2.25 % (1735730)------------------------------ % 10.76/2.25 % (1735730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.76/2.25 % (1735730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.76/2.25 % (1735730)CaDiCaL version: 2.1.3 % 10.76/2.25 % (1735730)Termination reason: Refutation not found, incomplete strategy % 10.76/2.25 % (1735730)Time elapsed: 0.004 s % 10.76/2.25 % (1735730)Peak memory usage: 88 MB % 10.76/2.25 % (1735730)Instructions burned: 6 (million) % 10.76/2.25 % (1735729)Refutation not found, incomplete strategy % 10.76/2.25 % (1735729)------------------------------ % 10.76/2.25 % (1735729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.76/2.25 % (1735729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.76/2.25 % (1735729)CaDiCaL version: 2.1.3 % 10.76/2.25 % (1735729)Termination reason: Refutation not found, incomplete strategy % 10.76/2.25 % (1735729)Time elapsed: 0.008 s % 10.76/2.25 % (1735729)Peak memory usage: 88 MB % 10.76/2.25 % (1735729)Instructions burned: 13 (million) % 10.76/2.25 % (1735736)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3398388635:i=5202:ss=axioms:sgt=16_2993 on theBenchmark for (2993ds/5202Mi) % 10.76/2.25 % (1735735)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3774857837:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi) % 10.76/2.25 % (1735725)------------------------------ % 10.76/2.25 % (1735725)------------------------------ % 10.76/2.25 % (1735730)------------------------------ % 10.76/2.25 % (1735730)------------------------------ % 10.76/2.25 % (1735729)------------------------------ % 10.76/2.25 % (1735729)------------------------------ % 10.76/2.25 % Exception at run slice level % 10.76/2.25 User error: GNN currently only supports monomorphic FOL. % 10.76/2.25 % (1735742)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3873470733:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2992 on theBenchmark for (2992ds/134Mi) % 10.76/2.25 % Exception at run slice level % 10.76/2.25 User error: GNN currently only supports monomorphic FOL. % 10.76/2.25 % (1735735)Instruction limit reached! % 10.76/2.25 % (1735735)------------------------------ % 10.76/2.25 % (1735735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.76/2.25 % (1735735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.76/2.25 % (1735735)CaDiCaL version: 2.1.3 % 10.76/2.25 % (1735735)Termination reason: Instruction limit % 10.76/2.25 % (1735735)Termination phase: Saturation % 10.76/2.25 % (1735735)Time elapsed: 0.244 s % 10.76/2.25 % (1735735)Peak memory usage: 91 MB % 10.76/2.25 % (1735735)Instructions burned: 438 (million) % 10.76/2.25 % (1735745)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=2257996144:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/125Mi) % 10.76/2.25 % (1735745)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.76/2.25 % (1735742)Instruction limit reached! % 10.76/2.25 % (1735742)------------------------------ % 10.76/2.25 % (1735742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.76/2.25 % (1735742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.76/2.25 % (1735742)CaDiCaL version: 2.1.3 % 10.76/2.25 % (1735742)Termination reason: Instruction limit % 10.76/2.25 % (1735742)Termination phase: Saturation % 10.76/2.25 % (1735742)Time elapsed: 0.075 s % 10.76/2.25 % (1735742)Peak memory usage: 90 MB % 10.76/2.25 % (1735742)Instructions burned: 136 (million) % 10.76/2.25 % (1735744)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3996022820:st=3:i=13193:sd=3:ss=axioms_2991 on theBenchmark for (2991ds/13193Mi) % 10.76/2.25 % (1735743)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3387984544:st=8:i=592:sd=3:ep=RST:ss=axioms_2991 on theBenchmark for (2991ds/592Mi) % 14.44/2.93 % (1735745)Instruction limit reached! % 14.44/2.93 % (1735745)------------------------------ % 14.44/2.93 % (1735745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.44/2.93 % (1735745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.44/2.93 % (1735745)CaDiCaL version: 2.1.3 % 14.44/2.93 % (1735745)Termination reason: Instruction limit % 14.44/2.93 % (1735745)Termination phase: Saturation % 14.44/2.93 % (1735745)Time elapsed: 0.036 s % 14.44/2.93 % (1735745)Peak memory usage: 89 MB % 14.44/2.93 % (1735745)Instructions burned: 127 (million) % 14.44/2.93 % (1735747)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4240839115:i=134:gtgl=5:slsql=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/134Mi) % 14.44/2.93 % Exception at run slice level % 14.44/2.93 User error: Immediate (shared) subterms of term/literal combk(X1,X0,zero_zero(X1)) = sF17(X1,X0) have different types/not well-typed! % 14.44/2.93 % (1735753)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=2810508211:i=6060:aac=none:ins=25_2989 on theBenchmark for (2989ds/6060Mi) % 14.44/2.93 % (1735748)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2549502519:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/141Mi) % 14.44/2.93 % (1735748)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 14.44/2.93 % (1735748)Refutation not found, incomplete strategy % 14.44/2.93 % (1735748)------------------------------ % 14.44/2.93 % (1735748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.44/2.93 % (1735748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.44/2.93 % (1735748)CaDiCaL version: 2.1.3 % 14.44/2.93 % (1735748)Termination reason: Refutation not found, incomplete strategy % 14.44/2.93 % (1735748)Time elapsed: 0.002 s % 14.44/2.93 % (1735748)Peak memory usage: 88 MB % 14.44/2.93 % (1735748)Instructions burned: 2 (million) % 14.44/2.93 % (1735750)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=564372609:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/431Mi) % 14.44/2.93 % (1735731)Instruction limit reached! % 14.44/2.93 % (1735731)------------------------------ % 14.44/2.93 % (1735731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.44/2.93 % (1735731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.44/2.93 % (1735731)CaDiCaL version: 2.1.3 % 14.44/2.93 % (1735731)Termination reason: Instruction limit % 14.44/2.93 % (1735731)Termination phase: Saturation % 14.44/2.93 % (1735731)Time elapsed: 0.553 s % 14.44/2.93 % (1735731)Peak memory usage: 93 MB % 14.44/2.93 % (1735731)Instructions burned: 907 (million) % 14.44/2.93 % (1735755)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=1001316342:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2989 on theBenchmark for (2989ds/150Mi) % 14.44/2.93 % (1735755)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 14.44/2.93 % (1735755)Instruction limit reached! % 14.44/2.93 % (1735755)------------------------------ % 14.44/2.93 % (1735755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.44/2.93 % (1735755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.44/2.93 % (1735755)CaDiCaL version: 2.1.3 % 14.44/2.93 % (1735755)Termination reason: Instruction limit % 14.44/2.93 % (1735755)Termination phase: Saturation % 14.44/2.93 % (1735755)Time elapsed: 0.097 s % 14.44/2.93 % (1735755)Peak memory usage: 90 MB % 14.44/2.93 % (1735755)Instructions burned: 150 (million) % 14.44/2.93 % (1735750)Instruction limit reached! % 14.44/2.93 % (1735750)------------------------------ % 14.44/2.93 % (1735750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.44/2.93 % (1735750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.44/2.93 % (1735750)CaDiCaL version: 2.1.3 % 14.44/2.93 % (1735750)Termination reason: Instruction limit % 14.44/2.93 % (1735750)Termination phase: Saturation % 14.44/2.93 % (1735750)Time elapsed: 0.178 s % 14.44/2.93 % (1735750)Peak memory usage: 89 MB % 14.44/2.93 % (1735750)Instructions burned: 432 (million) % 14.44/2.93 % Exception at run slice level % 20.01/3.62 User error: GNN currently only supports monomorphic FOL. % 20.01/3.62 % (1735759)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=4138113157:i=14155:bd=all_2988 on theBenchmark for (2988ds/14155Mi) % 20.01/3.62 % (1735748)------------------------------ % 20.01/3.62 % (1735748)------------------------------ % 20.01/3.62 % (1735743)Instruction limit reached! % 20.01/3.62 % (1735743)------------------------------ % 20.01/3.62 % (1735743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.01/3.62 % (1735743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.01/3.62 % (1735743)CaDiCaL version: 2.1.3 % 20.01/3.62 % (1735743)Termination reason: Instruction limit % 20.01/3.62 % (1735743)Termination phase: Saturation % 20.01/3.62 % (1735743)Time elapsed: 0.348 s % 20.01/3.62 % (1735743)Peak memory usage: 92 MB % 20.01/3.62 % (1735743)Instructions burned: 594 (million) % 20.01/3.62 % Exception at run slice level % 20.01/3.62 User error: GNN currently only supports monomorphic FOL. % 20.01/3.62 % (1735762)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=312660300:s2a=on:i=185:s2at=1.8:fdi=4_2986 on theBenchmark for (2986ds/185Mi) % 20.01/3.62 % (1735761)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1865153898:i=667:av=off:fsr=off_2986 on theBenchmark for (2986ds/667Mi) % 20.01/3.62 % (1735761)Refutation not found, incomplete strategy % 20.01/3.62 % (1735761)------------------------------ % 20.01/3.62 % (1735761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.01/3.62 % (1735761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.01/3.62 % (1735761)CaDiCaL version: 2.1.3 % 20.01/3.62 % (1735761)Termination reason: Refutation not found, incomplete strategy % 20.01/3.62 % (1735761)Time elapsed: 0.007 s % 20.01/3.62 % (1735761)Peak memory usage: 88 MB % 20.01/3.62 % (1735761)Instructions burned: 11 (million) % 20.01/3.62 % (1735764)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=71564575:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2986 on theBenchmark for (2986ds/193Mi) % 20.01/3.62 % (1735762)Instruction limit reached! % 20.01/3.62 % (1735762)------------------------------ % 20.01/3.62 % (1735762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.01/3.62 % (1735762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.01/3.62 % (1735762)CaDiCaL version: 2.1.3 % 20.01/3.62 % (1735762)Termination reason: Instruction limit % 20.01/3.62 % (1735762)Termination phase: Saturation % 20.01/3.62 % (1735762)Time elapsed: 0.062 s % 20.01/3.62 % (1735762)Peak memory usage: 91 MB % 20.01/3.62 % (1735762)Instructions burned: 185 (million) % 20.01/3.62 % (1735765)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2902888891:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2986 on theBenchmark for (2986ds/4850Mi) % 20.01/3.62 % (1735765)Refutation not found, incomplete strategy % 20.01/3.62 % (1735765)------------------------------ % 20.01/3.62 % (1735765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.01/3.62 % (1735765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.01/3.62 % (1735765)CaDiCaL version: 2.1.3 % 20.01/3.62 % (1735765)Termination reason: Refutation not found, incomplete strategy % 20.01/3.62 % (1735765)Time elapsed: 0.006 s % 20.01/3.62 % (1735765)Peak memory usage: 88 MB % 20.01/3.62 % (1735765)Instructions burned: 10 (million) % 20.01/3.62 % (1735766)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2572305586:i=12111:sd=1:ss=included_2986 on theBenchmark for (2986ds/12111Mi) % 20.01/3.62 % (1735768)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1859146970:i=319:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/319Mi) % 20.01/3.62 % (1735771)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2709316832:i=2064:ep=RST_2985 on theBenchmark for (2985ds/2064Mi) % 20.01/3.62 % (1735764)Instruction limit reached! % 20.01/3.62 % (1735764)------------------------------ % 20.01/3.62 % (1735764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.01/3.62 % (1735764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.01/3.62 % (1735764)CaDiCaL version: 2.1.3 % 20.01/3.62 % (1735764)Termination reason: Instruction limit % 27.43/4.69 % (1735764)Termination phase: Saturation % 27.43/4.69 % (1735764)Time elapsed: 0.129 s % 27.43/4.69 % (1735764)Peak memory usage: 91 MB % 27.43/4.69 % (1735764)Instructions burned: 193 (million) % 27.43/4.69 % (1735761)------------------------------ % 27.43/4.69 % (1735761)------------------------------ % 27.43/4.69 % Exception at run slice level % 27.43/4.69 User error: GNN currently only supports monomorphic FOL. % 27.43/4.69 % (1735768)Instruction limit reached! % 27.43/4.69 % (1735768)------------------------------ % 27.43/4.69 % (1735768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.43/4.69 % (1735768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.43/4.69 % (1735768)CaDiCaL version: 2.1.3 % 27.43/4.69 % (1735768)Termination reason: Instruction limit % 27.43/4.69 % (1735768)Termination phase: Saturation % 27.43/4.69 % (1735768)Time elapsed: 0.169 s % 27.43/4.69 % (1735768)Peak memory usage: 90 MB % 27.43/4.69 % (1735768)Instructions burned: 320 (million) % 27.43/4.69 % (1735776)dis-1011_128_sil=32000:random_seed=2143984388:i=3706:ep=RST:av=off_2984 on theBenchmark for (2984ds/3706Mi) % 27.43/4.69 % (1735765)------------------------------ % 27.43/4.69 % (1735765)------------------------------ % 27.43/4.69 % (1735777)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=513154643:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2983 on theBenchmark for (2983ds/757Mi) % 27.43/4.69 % (1735779)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3161005122:i=9925:aac=none_2983 on theBenchmark for (2983ds/9925Mi) % 27.43/4.69 % (1735778)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1050945463:i=13913:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/13913Mi) % 27.43/4.69 % Exception at run slice level % 27.43/4.69 User error: GNN currently only supports monomorphic FOL. % 27.43/4.69 % (1735781)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3557844337:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2982 on theBenchmark for (2982ds/2479Mi) % 27.43/4.69 % (1735781)Refutation not found, incomplete strategy % 27.43/4.69 % (1735781)------------------------------ % 27.43/4.69 % (1735781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.43/4.69 % (1735781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.43/4.69 % (1735781)CaDiCaL version: 2.1.3 % 27.43/4.69 % (1735781)Termination reason: Refutation not found, incomplete strategy % 27.43/4.69 % (1735781)Time elapsed: 0.005 s % 27.43/4.69 % (1735781)Peak memory usage: 88 MB % 27.43/4.69 % (1735781)Instructions burned: 6 (million) % 27.43/4.69 % (1735785)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1336230228:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/440Mi) % 27.43/4.69 % (1735785)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 27.43/4.69 % (1735781)------------------------------ % 27.43/4.69 % (1735781)------------------------------ % 27.43/4.69 % (1735771)Instruction limit reached! % 27.43/4.69 % (1735771)------------------------------ % 27.43/4.69 % (1735771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.43/4.69 % (1735771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.43/4.69 % (1735771)CaDiCaL version: 2.1.3 % 27.43/4.69 % (1735771)Termination reason: Instruction limit % 27.43/4.69 % (1735771)Termination phase: Saturation % 27.43/4.69 % (1735771)Time elapsed: 0.593 s % 27.43/4.69 % (1735771)Peak memory usage: 97 MB % 27.43/4.69 % (1735771)Instructions burned: 2066 (million) % 27.43/4.69 % Exception at run slice level % 27.43/4.69 User error: GNN currently only supports monomorphic FOL. % 27.43/4.69 % Exception at run slice level % 27.43/4.69 User error: GNN currently only supports monomorphic FOL. % 27.43/4.69 % (1735789)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=2541005742:cts=off:i=3034:av=off:er=known:fsd=on_2978 on theBenchmark for (2978ds/3034Mi) % 27.43/4.69 % (1735788)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3337871206:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2978 on theBenchmark for (2978ds/11145Mi) % 27.43/4.69 % (1735785)Instruction limit reached! % 27.43/4.69 % (1735785)------------------------------ % 27.43/4.69 % (1735785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.43/4.69 % (1735785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.20/5.75 % (1735785)CaDiCaL version: 2.1.3 % 35.20/5.75 % (1735785)Termination reason: Instruction limit % 35.20/5.75 % (1735785)Termination phase: Saturation % 35.20/5.75 % (1735785)Time elapsed: 0.243 s % 35.20/5.75 % (1735785)Peak memory usage: 89 MB % 35.20/5.75 % (1735785)Instructions burned: 441 (million) % 35.20/5.75 % (1735777)Instruction limit reached! % 35.20/5.75 % (1735777)------------------------------ % 35.20/5.75 % (1735777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.20/5.75 % (1735777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.20/5.75 % (1735777)CaDiCaL version: 2.1.3 % 35.20/5.75 % (1735777)Termination reason: Instruction limit % 35.20/5.75 % (1735777)Termination phase: Saturation % 35.20/5.75 % (1735777)Time elapsed: 0.483 s % 35.20/5.75 % (1735777)Peak memory usage: 94 MB % 35.20/5.75 % (1735777)Instructions burned: 758 (million) % 35.20/5.75 % (1735791)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3581689226:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2978 on theBenchmark for (2978ds/1016Mi) % 35.20/5.75 % (1735790)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3975386076:st=2:s2a=on:i=524:s2at=2:ss=axioms_2978 on theBenchmark for (2978ds/524Mi) % 35.20/5.75 % (1735794)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2972228178:i=14123:bd=preordered:ins=4_2977 on theBenchmark for (2977ds/14123Mi) % 35.20/5.75 % Exception at run slice level % 35.20/5.75 User error: GNN currently only supports monomorphic FOL. % 35.20/5.75 % (1735795)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=287048867:i=5781:kws=precedence:bd=all:rawr=on_2976 on theBenchmark for (2976ds/5781Mi) % 35.20/5.75 % (1735799)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=4244787361:i=2448:gtgl=5:bd=preordered:gtg=all_2975 on theBenchmark for (2975ds/2448Mi) % 35.20/5.75 % (1735790)Instruction limit reached! % 35.20/5.75 % (1735790)------------------------------ % 35.20/5.75 % (1735790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.20/5.75 % (1735790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.20/5.75 % (1735790)CaDiCaL version: 2.1.3 % 35.20/5.75 % (1735790)Termination reason: Instruction limit % 35.20/5.75 % (1735790)Termination phase: Saturation % 35.20/5.75 % (1735790)Time elapsed: 0.265 s % 35.20/5.75 % (1735790)Peak memory usage: 91 MB % 35.20/5.75 % (1735790)Instructions burned: 525 (million) % 35.20/5.75 % Exception at run slice level % 35.20/5.75 User error: GNN currently only supports monomorphic FOL. % 35.20/5.75 % (1735802)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=656777842:i=3223:kws=precedence:fgj=on:av=off_2974 on theBenchmark for (2974ds/3223Mi) % 35.20/5.75 % Exception at run slice level % 35.20/5.75 User error: GNN currently only supports monomorphic FOL. % 35.20/5.75 % (1735803)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2767098423:st=5.6:i=2033:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/2033Mi) % 35.20/5.75 % Exception at run slice level % 35.20/5.75 User error: GNN currently only supports monomorphic FOL. % 35.20/5.75 % (1735805)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=811564266:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2972 on theBenchmark for (2972ds/2055Mi) % 35.20/5.75 % (1735791)Instruction limit reached! % 35.20/5.75 % (1735791)------------------------------ % 35.20/5.75 % (1735791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.20/5.75 % (1735791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.20/5.75 % (1735791)CaDiCaL version: 2.1.3 % 35.20/5.75 % (1735791)Termination reason: Instruction limit % 35.20/5.75 % (1735791)Termination phase: Saturation % 35.20/5.75 % (1735791)Time elapsed: 0.516 s % 35.20/5.75 % (1735791)Peak memory usage: 94 MB % 35.20/5.75 % (1735791)Instructions burned: 1017 (million) % 35.20/5.75 % (1735807)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=715816639:i=21611:sd=3:ss=axioms_2972 on theBenchmark for (2972ds/21611Mi) % 35.20/5.75 % (1735809)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1513486491:i=4835:sd=13:ss=axioms:sgt=23_2971 on theBenchmark for (2971ds/4835Mi) % 43.35/7.01 % Exception at run slice level % 43.35/7.01 User error: GNN currently only supports monomorphic FOL. % 43.35/7.01 % Exception at run slice level % 43.35/7.01 User error: GNN currently only supports monomorphic FOL. % 43.35/7.01 % (1735812)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=1055350811:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2970 on theBenchmark for (2970ds/797Mi) % 43.35/7.01 % Exception at run slice level % 43.35/7.01 User error: GNN currently only supports monomorphic FOL. % 43.35/7.01 % (1735813)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2547402765:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2969 on theBenchmark for (2969ds/2326Mi) % 43.35/7.01 % Exception at run slice level % 43.35/7.01 User error: GNN currently only supports monomorphic FOL. % 43.35/7.01 % (1735815)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2948430933:i=6038:nm=6_2968 on theBenchmark for (2968ds/6038Mi) % 43.35/7.01 % (1735812)Instruction limit reached! % 43.35/7.01 % (1735812)------------------------------ % 43.35/7.01 % (1735812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.35/7.01 % (1735812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.35/7.01 % (1735812)CaDiCaL version: 2.1.3 % 43.35/7.01 % (1735812)Termination reason: Instruction limit % 43.35/7.01 % (1735812)Termination phase: Saturation % 43.35/7.01 % (1735812)Time elapsed: 0.221 s % 43.35/7.01 % (1735812)Peak memory usage: 91 MB % 43.35/7.01 % (1735812)Instructions burned: 801 (million) % 43.35/7.01 % (1735817)lrs+10_1_sil=32000:sp=occurrence:random_seed=4071183233:st=2:i=33334:sd=3:ss=included:sgt=32_2967 on theBenchmark for (2967ds/33334Mi) % 43.35/7.01 % (1735819)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=279103677:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2966 on theBenchmark for (2966ds/1008Mi) % 43.35/7.01 % Exception at run slice level % 43.35/7.01 User error: GNN currently only supports monomorphic FOL. % 43.35/7.01 % (1735819)Instruction limit reached! % 43.35/7.01 % (1735819)------------------------------ % 43.35/7.01 % (1735819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.35/7.01 % (1735819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.35/7.01 % (1735819)CaDiCaL version: 2.1.3 % 43.35/7.01 % (1735819)Termination reason: Instruction limit % 43.35/7.01 % (1735819)Termination phase: Saturation % 43.35/7.01 % (1735819)Time elapsed: 0.252 s % 43.35/7.01 % (1735819)Peak memory usage: 97 MB % 43.35/7.01 % (1735819)Instructions burned: 1011 (million) % 43.35/7.01 % (1735776)Instruction limit reached! % 43.35/7.01 % (1735776)------------------------------ % 43.35/7.01 % (1735776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.35/7.01 % (1735776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.35/7.01 % (1735776)CaDiCaL version: 2.1.3 % 43.35/7.01 % (1735776)Termination reason: Instruction limit % 43.35/7.01 % (1735776)Termination phase: Saturation % 43.35/7.01 % (1735776)Time elapsed: 1.984 s % 43.35/7.01 % (1735776)Peak memory usage: 107 MB % 43.35/7.01 % (1735776)Instructions burned: 3706 (million) % 43.35/7.01 % (1735822)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=2069620535:i=8327:s2at=5:bd=preordered_2963 on theBenchmark for (2963ds/8327Mi) % 43.35/7.01 % (1735823)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=1329590998:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2963 on theBenchmark for (2963ds/1083Mi) % 43.35/7.01 % (1735824)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2131793676:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2962 on theBenchmark for (2962ds/1084Mi) % 43.35/7.01 % (1735823)Instruction limit reached! % 43.35/7.01 % (1735823)------------------------------ % 43.35/7.01 % (1735823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.35/7.01 % (1735823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.35/7.01 % (1735823)CaDiCaL version: 2.1.3 % 43.35/7.01 % (1735823)Termination reason: Instruction limit % 54.00/8.31 % (1735823)Termination phase: Saturation % 54.00/8.31 % (1735823)Time elapsed: 0.290 s % 54.00/8.31 % (1735823)Peak memory usage: 96 MB % 54.00/8.31 % (1735823)Instructions burned: 1084 (million) % 54.00/8.31 % Exception at run slice level % 54.00/8.31 User error: GNN currently only supports monomorphic FOL. % 54.00/8.31 % (1735828)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=555260981:i=6995:s2at=5:gtg=all_2959 on theBenchmark for (2959ds/6995Mi) % 54.00/8.31 % (1735829)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=353015410:st=2:i=6225:sd=15:ss=axioms_2959 on theBenchmark for (2959ds/6225Mi) % 54.00/8.31 % Exception at run slice level % 54.00/8.31 User error: GNN currently only supports monomorphic FOL. % 54.00/8.31 % (1735832)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3144556567:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2956 on theBenchmark for (2956ds/3372Mi) % 54.00/8.31 % (1735824)Instruction limit reached! % 54.00/8.31 % (1735824)------------------------------ % 54.00/8.31 % (1735824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.00/8.31 % (1735824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.00/8.31 % (1735824)CaDiCaL version: 2.1.3 % 54.00/8.31 % (1735824)Termination reason: Instruction limit % 54.00/8.31 % (1735824)Termination phase: Saturation % 54.00/8.31 % (1735824)Time elapsed: 0.609 s % 54.00/8.31 % (1735824)Peak memory usage: 96 MB % 54.00/8.31 % (1735824)Instructions burned: 1085 (million) % 54.00/8.31 % (1735834)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1993556771:st=2.3:i=26457:sd=10:ss=included:sgt=8_2955 on theBenchmark for (2955ds/26457Mi) % 54.00/8.31 % Exception at run slice level % 54.00/8.31 User error: GNN currently only supports monomorphic FOL. % 54.00/8.31 % (1735813)Instruction limit reached! % 54.00/8.31 % (1735813)------------------------------ % 54.00/8.31 % (1735813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.00/8.31 % (1735813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.00/8.31 % (1735813)CaDiCaL version: 2.1.3 % 54.00/8.31 % (1735813)Termination reason: Instruction limit % 54.00/8.31 % (1735813)Termination phase: Saturation % 54.00/8.31 % (1735813)Time elapsed: 1.405 s % 54.00/8.31 % (1735813)Peak memory usage: 95 MB % 54.00/8.31 % (1735813)Instructions burned: 2327 (million) % 54.00/8.31 % (1735836)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=4076728277:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2954 on theBenchmark for (2954ds/13494Mi) % 54.00/8.31 % (1735837)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=1371061338:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2954 on theBenchmark for (2954ds/2503Mi) % 54.00/8.31 % (1735837)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 54.00/8.31 % (1735795)Instruction limit reached! % 54.00/8.31 % (1735795)------------------------------ % 54.00/8.31 % (1735795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.00/8.31 % (1735795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.00/8.31 % (1735795)CaDiCaL version: 2.1.3 % 54.00/8.31 % (1735795)Termination reason: Instruction limit % 54.00/8.31 % (1735795)Termination phase: Saturation % 54.00/8.31 % (1735795)Time elapsed: 2.413 s % 54.00/8.31 % (1735795)Peak memory usage: 103 MB % 54.00/8.31 % (1735795)Instructions burned: 5784 (million) % 54.00/8.31 % Exception at run slice level % 54.00/8.31 User error: GNN currently only supports monomorphic FOL. % 54.00/8.31 % Exception at run slice level % 54.00/8.31 User error: GNN currently only supports monomorphic FOL. % 54.00/8.31 % (1735841)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=92941004:i=30753:av=off:ss=included_2951 on theBenchmark for (2951ds/30753Mi) % 54.00/8.31 % (1735840)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=3602747998:i=2559:sd=1:ep=RSTC:ss=axioms_2951 on theBenchmark for (2951ds/2559Mi) % 54.00/8.31 % Exception at run slice level % 54.00/8.31 User error: GNN currently only supports monomorphic FOL. % 54.00/8.31 % (1735843)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3242270668:i=26473:ep=RSTC_2950 on theBenchmark for (2950ds/26473Mi) % 61.82/9.40 % Exception at run slice level % 61.82/9.40 User error: GNN currently only supports monomorphic FOL. % 61.82/9.40 % (1735846)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=1819057958:cts=off:i=2759:kws=inv_arity:fgj=on_2949 on theBenchmark for (2949ds/2759Mi) % 61.82/9.40 % (1735847)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=3466007995:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2948 on theBenchmark for (2948ds/5665Mi) % 61.82/9.40 % (1735847)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 61.82/9.40 % Exception at run slice level % 61.82/9.40 User error: GNN currently only supports monomorphic FOL. % 61.82/9.40 % Exception at run slice level % 61.82/9.40 User error: GNN currently only supports monomorphic FOL. % 61.82/9.40 % (1735850)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=530716742:i=1532:ep=RS:ss=axioms_2946 on theBenchmark for (2946ds/1532Mi) % 61.82/9.40 % (1735851)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3142848828:i=1565:sd=2:ss=axioms:sgt=32_2945 on theBenchmark for (2945ds/1565Mi) % 61.82/9.40 % Exception at run slice level % 61.82/9.40 User error: GNN currently only supports monomorphic FOL. % 61.82/9.40 % (1735854)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=178591132:i=1572:fgj=on:gsp=on_2944 on theBenchmark for (2944ds/1572Mi) % 61.82/9.40 % (1735854)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 61.82/9.40 % Exception at run slice level % 61.82/9.40 User error: GNN currently only supports monomorphic FOL. % 61.82/9.40 % (1735809)Instruction limit reached! % 61.82/9.40 % (1735809)------------------------------ % 61.82/9.40 % (1735809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.82/9.40 % (1735809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.82/9.40 % (1735809)CaDiCaL version: 2.1.3 % 61.82/9.40 % (1735809)Termination reason: Instruction limit % 61.82/9.40 % (1735809)Termination phase: Saturation % 61.82/9.40 % (1735809)Time elapsed: 2.840 s % 61.82/9.40 % (1735809)Peak memory usage: 110 MB % 61.82/9.40 % (1735809)Instructions burned: 4835 (million) % 61.82/9.40 % (1735856)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=2047202433:i=6052:sd=4:ss=axioms:sgt=24_2942 on theBenchmark for (2942ds/6052Mi) % 61.82/9.40 % Exception at run slice level % 61.82/9.40 User error: GNN currently only supports monomorphic FOL. % 61.82/9.40 % (1735858)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=1548958210:i=3500:sd=1:bd=preordered:sup=off:ss=included_2942 on theBenchmark for (2942ds/3500Mi) % 61.82/9.40 % (1735859)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=1672939323:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2941 on theBenchmark for (2941ds/1842Mi) % 61.82/9.40 % (1735859)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 61.82/9.40 % Exception at run slice level % 61.82/9.40 User error: GNN currently only supports monomorphic FOL. % 61.82/9.40 % Exception at run slice level % 61.82/9.40 User error: GNN currently only supports monomorphic FOL. % 61.82/9.40 % (1735862)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1104590121:i=66096:add=on_2940 on theBenchmark for (2940ds/66096Mi) % 61.82/9.40 % (1735863)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=4105367927:i=1884:sd=1:nm=60:ss=axioms_2939 on theBenchmark for (2939ds/1884Mi) % 61.82/9.40 % Exception at run slice level % 61.82/9.40 User error: GNN currently only supports monomorphic FOL. % 61.82/9.40 % Exception at run slice level % 61.82/9.40 User error: GNN currently only supports monomorphic FOL. % 61.82/9.40 % Exception at run slice level % 61.82/9.40 User error: GNN currently only supports monomorphic FOL. % 70.48/10.74 % (1735866)lrs-1011_4:1_sil=16000:bsr=on:random_seed=2636838368:cts=off:i=5469:bs=on:fsr=off_2937 on theBenchmark for (2937ds/5469Mi) % 70.48/10.74 % (1735867)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=613344902:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2937 on theBenchmark for (2937ds/2037Mi) % 70.48/10.74 % (1735868)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2991014347:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2936 on theBenchmark for (2936ds/2110Mi) % 70.48/10.74 % Exception at run slice level % 70.48/10.74 User error: GNN currently only supports monomorphic FOL. % 70.48/10.74 % (1735872)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=3097467532:i=2430:add=off:aac=none:nm=16_2934 on theBenchmark for (2934ds/2430Mi) % 70.48/10.74 % Exception at run slice level % 70.48/10.74 User error: GNN currently only supports monomorphic FOL. % 70.48/10.74 % Exception at run slice level % 70.48/10.74 User error: GNN currently only supports monomorphic FOL. % 70.48/10.74 % (1735874)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=3430977223:cond=fast:i=4891_2932 on theBenchmark for (2932ds/4891Mi) % 70.48/10.74 % (1735875)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=3109983424:st=2:i=14845:sd=2:ss=included:fsd=on_2931 on theBenchmark for (2931ds/14845Mi) % 70.48/10.74 % Exception at run slice level % 70.48/10.74 User error: GNN currently only supports monomorphic FOL. % 70.48/10.74 % (1735878)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=2333867304:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2929 on theBenchmark for (2929ds/7534Mi) % 70.48/10.74 % (1735829)Instruction limit reached! % 70.48/10.74 % (1735829)------------------------------ % 70.48/10.74 % (1735829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.48/10.74 % (1735829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.48/10.74 % (1735829)CaDiCaL version: 2.1.3 % 70.48/10.74 % (1735829)Termination reason: Instruction limit % 70.48/10.74 % (1735829)Termination phase: Saturation % 70.48/10.74 % (1735829)Time elapsed: 2.988 s % 70.48/10.74 % (1735829)Peak memory usage: 131 MB % 70.48/10.74 % (1735829)Instructions burned: 6227 (million) % 70.48/10.74 % Exception at run slice level % 70.48/10.74 User error: GNN currently only supports monomorphic FOL. % 70.48/10.74 % Exception at run slice level % 70.48/10.74 User error: GNN currently only supports monomorphic FOL. % 70.48/10.74 % (1735880)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=2295870698:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2927 on theBenchmark for (2927ds/10353Mi) % 70.48/10.74 % (1735881)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4021769280:i=7860_2927 on theBenchmark for (2927ds/7860Mi) % 70.48/10.74 % (1735881)Refutation not found, incomplete strategy % 70.48/10.74 % (1735881)------------------------------ % 70.48/10.74 % (1735881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.48/10.74 % (1735881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.48/10.74 % (1735881)CaDiCaL version: 2.1.3 % 70.48/10.74 % (1735881)Termination reason: Refutation not found, incomplete strategy % 70.48/10.74 % (1735881)Time elapsed: 0.007 s % 70.48/10.74 % (1735881)Peak memory usage: 88 MB % 70.48/10.74 % (1735881)Instructions burned: 11 (million) % 70.48/10.74 % (1735882)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=4275946080:i=7896:sd=2:bs=on:ss=included:sgt=20_2926 on theBenchmark for (2926ds/7896Mi) % 70.48/10.74 % Exception at run slice level % 70.48/10.74 User error: GNN currently only supports monomorphic FOL. % 70.48/10.74 % (1735881)------------------------------ % 70.48/10.74 % (1735881)------------------------------ % 70.48/10.74 % (1735886)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1476046761:i=5812:gtgl=2:gtg=all_2924 on theBenchmark for (2924ds/5812Mi) % 106.68/15.77 % Exception at run slice level % 106.68/15.77 User error: GNN currently only supports monomorphic FOL. % 106.68/15.77 % (1735887)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=3945797215:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2923 on theBenchmark for (2923ds/2965Mi) % 106.68/15.77 % Exception at run slice level % 106.68/15.77 User error: GNN currently only supports monomorphic FOL. % 106.68/15.77 % (1735889)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=1484450761:i=2967:kws=precedence:bd=preordered:av=off_2923 on theBenchmark for (2923ds/2967Mi) % 106.68/15.77 % (1735891)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=4097603062:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2921 on theBenchmark for (2921ds/3022Mi) % 106.68/15.77 % Exception at run slice level % 106.68/15.77 User error: GNN currently only supports monomorphic FOL. % 106.68/15.77 % (1735866)Instruction limit reached! % 106.68/15.77 % (1735866)------------------------------ % 106.68/15.77 % (1735866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.68/15.77 % (1735866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.68/15.77 % (1735866)CaDiCaL version: 2.1.3 % 106.68/15.77 % (1735866)Termination reason: Instruction limit % 106.68/15.77 % (1735866)Termination phase: Saturation % 106.68/15.77 % (1735866)Time elapsed: 1.717 s % 106.68/15.77 % (1735866)Peak memory usage: 96 MB % 106.68/15.77 % (1735866)Instructions burned: 5474 (million) % 106.68/15.77 % Exception at run slice level % 106.68/15.77 User error: GNN currently only supports monomorphic FOL. % 106.68/15.77 % (1735894)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=3486376526:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2919 on theBenchmark for (2919ds/3207Mi) % 106.68/15.77 % (1735895)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=1576282920:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2919 on theBenchmark for (2919ds/3289Mi) % 106.68/15.77 % Exception at run slice level % 106.68/15.77 User error: GNN currently only supports monomorphic FOL. % 106.68/15.77 % (1735896)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=2992256928:i=38569:sd=3:ss=axioms:sgt=32_2918 on theBenchmark for (2918ds/38569Mi) % 106.68/15.77 % Exception at run slice level % 106.68/15.77 User error: GNN currently only supports monomorphic FOL. % 106.68/15.77 % (1735899)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=1958649905:cts=off:i=3394_2918 on theBenchmark for (2918ds/3394Mi) % 106.68/15.77 % Exception at run slice level % 106.68/15.77 User error: GNN currently only supports monomorphic FOL. % 106.68/15.77 % (1735901)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=2780066437:i=33824:bd=preordered_2917 on theBenchmark for (2917ds/33824Mi) % 106.68/15.77 % (1735903)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=1585029732:i=20684:bd=all:gtg=exists_sym_2916 on theBenchmark for (2916ds/20684Mi) % 106.68/15.77 % Exception at run slice level % 106.68/15.77 User error: GNN currently only supports monomorphic FOL. % 106.68/15.77 % Exception at run slice level % 106.68/15.77 User error: GNN currently only supports monomorphic FOL. % 106.68/15.77 % (1735906)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=1777588363: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_2915 on theBenchmark for (2915ds/7222Mi) % 106.68/15.77 % (1735906)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 106.68/15.77 % Exception at run slice level % 106.68/15.77 User error: GNN currently only supports monomorphic FOL. % 106.68/15.77 % Exception at run slice level % 106.68/15.77 User error: GNN currently only supports monomorphic FOL. % 106.68/15.77 % (1735909)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=132637054:i=4036:ins=10_2913 on theBenchmark for (2913ds/4036Mi) % 121.39/17.88 % (1735907)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=2038330829:st=4:i=7295:sd=4:ep=R:ss=axioms_2913 on theBenchmark for (2913ds/7295Mi) % 121.39/17.88 % Exception at run slice level % 121.39/17.88 User error: GNN currently only supports monomorphic FOL. % 121.39/17.88 % (1735910)lrs+10_1_sil=128000:lcm=predicate:random_seed=3350570597:st=3:i=43697:sd=5:ss=axioms_2913 on theBenchmark for (2913ds/43697Mi) % 121.39/17.88 % (1735913)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=1278895560:i=17599:gtg=all:ss=axioms:fsd=on_2912 on theBenchmark for (2912ds/17599Mi) % 121.39/17.88 % Exception at run slice level % 121.39/17.88 User error: GNN currently only supports monomorphic FOL. % 121.39/17.88 % Exception at run slice level % 121.39/17.88 User error: GNN currently only supports monomorphic FOL. % 121.39/17.88 % (1735916)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=1221109062:i=4547:bd=preordered_2910 on theBenchmark for (2910ds/4547Mi) % 121.39/17.88 % Exception at run slice level % 121.39/17.88 User error: GNN currently only supports monomorphic FOL. % 121.39/17.88 % (1735917)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=47038663:i=9294:av=off_2910 on theBenchmark for (2910ds/9294Mi) % 121.39/17.88 % Exception at run slice level % 121.39/17.88 User error: GNN currently only supports monomorphic FOL. % 121.39/17.88 % (1735919)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3154568915:i=32849:add=on_2909 on theBenchmark for (2909ds/32849Mi) % 121.39/17.88 % Exception at run slice level % 121.39/17.88 User error: GNN currently only supports monomorphic FOL. % 121.39/17.88 % (1735921)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3442869513:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2907 on theBenchmark for (2907ds/4793Mi) % 121.39/17.88 % (1735923)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=3791626900:i=4840:nm=4:av=off_2907 on theBenchmark for (2907ds/4840Mi) % 121.39/17.88 % Exception at run slice level % 121.39/17.88 User error: GNN currently only supports monomorphic FOL. % 121.39/17.88 % Exception at run slice level % 121.39/17.88 User error: GNN currently only supports monomorphic FOL. % 121.39/17.88 % (1735927)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=510639101:i=30479:sd=3:ss=axioms_2905 on theBenchmark for (2905ds/30479Mi) % 121.39/17.88 % Exception at run slice level % 121.39/17.88 User error: GNN currently only supports monomorphic FOL. % 121.39/17.88 % (1735926)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=4079901969:cts=off:i=5002_2905 on theBenchmark for (2905ds/5002Mi) % 121.39/17.88 % (1735929)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=1464603440:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2904 on theBenchmark for (2904ds/11035Mi) % 121.39/17.88 % (1735929)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 121.39/17.88 % Exception at run slice level % 121.39/17.88 User error: GNN currently only supports monomorphic FOL. % 121.39/17.88 % Exception at run slice level % 121.39/17.88 User error: GNN currently only supports monomorphic FOL. % 121.39/17.88 % (1735933)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=4197473012:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2902 on theBenchmark for (2902ds/5890Mi) % 121.39/17.88 % (1735932)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=2916916607:i=5835_2902 on theBenchmark for (2902ds/5835Mi) % 121.39/17.88 % Exception at run slice level % 121.39/17.88 User error: GNN currently only supports monomorphic FOL. % 121.39/17.88 % Exception at run slice level % 121.39/17.88 User error: GNN currently only supports monomorphic FOL. % 121.39/17.88 % Exception at run slice level % 121.39/17.88 User error: GNN currently only supports monomorphic FOL. % 163.06/23.69 % (1735936)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=3809593973:cts=off:i=19910:ep=RS_2900 on theBenchmark for (2900ds/19910Mi) % 163.06/23.69 % (1735938)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=2200749715:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2899 on theBenchmark for (2899ds/13822Mi) % 163.06/23.69 % (1735937)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=3123518145:i=20312:bd=preordered:fsr=off:er=filter_2899 on theBenchmark for (2899ds/20312Mi) % 163.06/23.69 % Exception at run slice level % 163.06/23.69 User error: GNN currently only supports monomorphic FOL. % 163.06/23.69 % Exception at run slice level % 163.06/23.69 User error: GNN currently only supports monomorphic FOL. % 163.06/23.69 % (1735942)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=3577439991:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2897 on theBenchmark for (2897ds/7144Mi) % 163.06/23.69 % (1735943)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=2147661165:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2896 on theBenchmark for (2896ds/15184Mi) % 163.06/23.69 % Exception at run slice level % 163.06/23.69 User error: GNN currently only supports monomorphic FOL. % 163.06/23.69 % Exception at run slice level % 163.06/23.69 User error: GNN currently only supports monomorphic FOL. % 163.06/23.69 % (1735946)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=3182065898:i=107375_2894 on theBenchmark for (2894ds/107375Mi) % 163.06/23.69 % (1735947)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=989024965:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2893 on theBenchmark for (2893ds/7958Mi) % 163.06/23.69 % Exception at run slice level % 163.06/23.69 User error: GNN currently only supports monomorphic FOL. % 163.06/23.69 % (1735950)dis+10_128_sil=16000:nwc=0.7:random_seed=3117628177:i=15999:nm=2:gsp=on_2890 on theBenchmark for (2890ds/15999Mi) % 163.06/23.69 % (1735950)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 163.06/23.69 % Exception at run slice level % 163.06/23.69 User error: GNN currently only supports monomorphic FOL. % 163.06/23.69 % (1735952)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=2261943438:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2889 on theBenchmark for (2889ds/8139Mi) % 163.06/23.69 % (1735952)Instruction limit reached! % 163.06/23.69 % (1735952)------------------------------ % 163.06/23.69 % (1735952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.06/23.69 % (1735952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.06/23.69 % (1735952)CaDiCaL version: 2.1.3 % 163.06/23.69 % (1735952)Termination reason: Instruction limit % 163.06/23.69 % (1735952)Termination phase: Saturation % 163.06/23.69 % (1735952)Time elapsed: 3.327 s % 163.06/23.69 % (1735952)Peak memory usage: 91 MB % 163.06/23.69 % (1735952)Instructions burned: 8140 (million) % 163.06/23.69 % (1735954)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=3617072753:st=4:i=8950:sd=5:ss=axioms_2855 on theBenchmark for (2855ds/8950Mi) % 163.06/23.69 % (1735942)Instruction limit reached! % 163.06/23.69 % (1735942)------------------------------ % 163.06/23.69 % (1735942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.06/23.69 % (1735942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.06/23.69 % (1735942)CaDiCaL version: 2.1.3 % 163.06/23.69 % (1735942)Termination reason: Instruction limit % 163.06/23.69 % (1735942)Termination phase: Saturation % 163.06/23.69 % (1735942)Time elapsed: 4.344 s % 163.06/23.69 % (1735942)Peak memory usage: 134 MB % 163.06/23.69 % (1735942)Instructions burned: 7144 (million) % 163.06/23.69 % (1735956)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=139286621:i=9809:ins=10:av=off_2852 on theBenchmark for (2852ds/9809Mi) % 163.06/23.69 % Exception at run slice level % 163.06/23.69 User error: GNN currently only supports monomorphic FOL. % 163.06/23.69 % (1735958)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=684122003:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2850 on theBenchmark for (2850ds/9885Mi) % 198.09/28.66 % Exception at run slice level % 198.09/28.66 User error: GNN currently only supports monomorphic FOL. % 198.09/28.66 % (1735960)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=2723683648:cond=fast:i=32078:fgj=on:av=off_2847 on theBenchmark for (2847ds/32078Mi) % 198.09/28.66 % Exception at run slice level % 198.09/28.66 User error: GNN currently only supports monomorphic FOL. % 198.09/28.66 % (1735962)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=3846340004:i=11101:bd=all:ss=axioms:sgt=8_2845 on theBenchmark for (2845ds/11101Mi) % 198.09/28.66 % Exception at run slice level % 198.09/28.66 User error: GNN currently only supports monomorphic FOL. % 198.09/28.66 % (1735950)Instruction limit reached! % 198.09/28.66 % (1735950)------------------------------ % 198.09/28.66 % (1735950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 198.09/28.66 % (1735950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.09/28.66 % (1735950)CaDiCaL version: 2.1.3 % 198.09/28.66 % (1735950)Termination reason: Instruction limit % 198.09/28.66 % (1735950)Termination phase: Saturation % 198.09/28.66 % (1735950)Time elapsed: 4.817 s % 198.09/28.66 % (1735950)Peak memory usage: 166 MB % 198.09/28.66 % (1735950)Instructions burned: 16001 (million) % 198.09/28.66 % (1735964)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=1255273163:cond=on:i=13220:s2at=3:aac=none:fsd=on_2842 on theBenchmark for (2842ds/13220Mi) % 198.09/28.66 % (1735965)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=3697982925:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2841 on theBenchmark for (2841ds/13528Mi) % 198.09/28.66 % Exception at run slice level % 198.09/28.66 User error: GNN currently only supports monomorphic FOL. % 198.09/28.66 % (1735968)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=2977167626:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2838 on theBenchmark for (2838ds/14854Mi) % 198.09/28.66 % Exception at run slice level % 198.09/28.66 User error: GNN currently only supports monomorphic FOL. % 198.09/28.66 % (1735970)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=3454663142:i=14974:ss=axioms:sgt=16_2837 on theBenchmark for (2837ds/14974Mi) % 198.09/28.66 % Exception at run slice level % 198.09/28.66 User error: GNN currently only supports monomorphic FOL. % 198.09/28.66 % (1735972)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=317314486:i=33081:aac=none:fgj=on:bd=all:fsr=off_2836 on theBenchmark for (2836ds/33081Mi) % 198.09/28.66 % Exception at run slice level % 198.09/28.66 User error: GNN currently only supports monomorphic FOL. % 198.09/28.66 % Exception at run slice level % 198.09/28.66 User error: GNN currently only supports monomorphic FOL. % 198.09/28.66 % (1735974)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=248022734:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2833 on theBenchmark for (2833ds/50856Mi) % 198.09/28.66 % (1735975)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=4141393661:i=69865_2832 on theBenchmark for (2832ds/69865Mi) % 198.09/28.66 % Exception at run slice level % 198.09/28.66 User error: GNN currently only supports monomorphic FOL. % 198.09/28.66 % (1735978)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=606026148:cond=fast:i=17802:gtgl=3:gtg=all_2830 on theBenchmark for (2830ds/17802Mi) % 198.09/28.66 % Exception at run slice level % 198.09/28.66 User error: Immediate (shared) subterms of term/literal combk(X1,X0,zero_zero(X1)) = sF17(X1,X0) have different types/not well-typed! % 198.09/28.66 % (1735980)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=3322087760:i=96644_2829 on theBenchmark for (2829ds/96644Mi) % 198.09/28.66 % Exception at run slice level % 198.09/28.66 User error: GNN currently only supports monomorphic FOL. % 215.80/31.11 % (1735982)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 215.80/31.11 % (1735982)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=4264235694:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2827 on theBenchmark for (2827ds/21161Mi) % 215.80/31.11 % (1735843)Instruction limit reached! % 215.80/31.11 % (1735843)------------------------------ % 215.80/31.11 % (1735843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.80/31.11 % (1735843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.80/31.11 % (1735843)CaDiCaL version: 2.1.3 % 215.80/31.11 % (1735843)Termination reason: Instruction limit % 215.80/31.11 % (1735843)Termination phase: Saturation % 215.80/31.11 % (1735843)Time elapsed: 14.097 s % 215.80/31.11 % (1735843)Peak memory usage: 202 MB % 215.80/31.11 % (1735843)Instructions burned: 26473 (million) % 215.80/31.11 % (1735984)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=1623310290:i=22761:gtg=all:ss=axioms:fsd=on_2808 on theBenchmark for (2808ds/22761Mi) % 215.80/31.11 % Exception at run slice level % 215.80/31.11 User error: GNN currently only supports monomorphic FOL. % 215.80/31.11 % (1735986)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=3006580581:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2803 on theBenchmark for (2803ds/23713Mi) % 215.80/31.11 % (1735936)Instruction limit reached! % 215.80/31.11 % (1735936)------------------------------ % 215.80/31.11 % (1735936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.80/31.11 % (1735936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.80/31.11 % (1735936)CaDiCaL version: 2.1.3 % 215.80/31.11 % (1735936)Termination reason: Instruction limit % 215.80/31.11 % (1735936)Termination phase: Saturation % 215.80/31.11 % (1735936)Time elapsed: 10.336 s % 215.80/31.11 % (1735936)Peak memory usage: 149 MB % 215.80/31.11 % (1735936)Instructions burned: 19911 (million) % 215.80/31.11 % (1735988)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=3990217611:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2795 on theBenchmark for (2795ds/26509Mi) % 215.80/31.11 % Exception at run slice level % 215.80/31.11 User error: GNN currently only supports monomorphic FOL. % 215.80/31.11 % (1735990)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=30639430:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2790 on theBenchmark for (2790ds/28957Mi) % 215.80/31.11 % (1735962)Instruction limit reached! % 215.80/31.11 % (1735962)------------------------------ % 215.80/31.11 % (1735962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.80/31.11 % (1735962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.80/31.11 % (1735962)CaDiCaL version: 2.1.3 % 215.80/31.11 % (1735962)Termination reason: Instruction limit % 215.80/31.11 % (1735962)Termination phase: Saturation % 215.80/31.11 % (1735962)Time elapsed: 6.332 s % 215.80/31.11 % (1735962)Peak memory usage: 138 MB % 215.80/31.11 % (1735962)Instructions burned: 11101 (million) % 215.80/31.11 % (1735992)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=684597435:i=29246:s2at=-1:kws=inv_arity:ins=10_2780 on theBenchmark for (2780ds/29246Mi) % 215.80/31.11 % Exception at run slice level % 215.80/31.11 User error: GNN currently only supports monomorphic FOL. % 215.80/31.11 % (1735994)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=2501486607:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2775 on theBenchmark for (2775ds/30082Mi) % 215.80/31.11 % (1735994)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 215.80/31.11 % Exception at run slice level % 215.80/31.11 User error: GNN currently only supports monomorphic FOL. % 215.80/31.11 % (1735996)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=1777463848:i=32262:bd=preordered_2771 on theBenchmark for (2771ds/32262Mi) % 224.69/32.33 % Exception at run slice level % 224.69/32.33 User error: GNN currently only supports monomorphic FOL. % 224.69/32.33 % (1735998)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=2050301823:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2766 on theBenchmark for (2766ds/32870Mi) % 224.69/32.33 % (1735817)Instruction limit reached! % 224.69/32.33 % (1735817)------------------------------ % 224.69/32.33 % (1735817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.69/32.33 % (1735817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.69/32.33 % (1735817)CaDiCaL version: 2.1.3 % 224.69/32.33 % (1735817)Termination reason: Instruction limit % 224.69/32.33 % (1735817)Termination phase: Saturation % 224.69/32.33 % (1735817)Time elapsed: 20.189 s % 224.69/32.33 % (1735817)Peak memory usage: 188 MB % 224.69/32.33 % (1735817)Instructions burned: 33334 (million) % 224.69/32.33 % (1736000)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=536674625:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2764 on theBenchmark for (2764ds/33295Mi) % 224.69/32.33 % Exception at run slice level % 224.69/32.33 User error: GNN currently only supports monomorphic FOL. % 224.69/32.33 % (1736002)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=1231450108:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2761 on theBenchmark for (2761ds/36826Mi) % 224.69/32.33 % Exception at run slice level % 224.69/32.33 User error: GNN currently only supports monomorphic FOL. % 224.69/32.33 % (1736004)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=3213306759:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2759 on theBenchmark for (2759ds/92981Mi) % 224.69/32.33 % Exception at run slice level % 224.69/32.33 User error: GNN currently only supports monomorphic FOL. % 224.69/32.33 % (1736006)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=688804850:s2pl=on:i=49423_2754 on theBenchmark for (2754ds/49423Mi) % 224.69/32.33 % Exception at run slice level % 224.69/32.33 User error: GNN currently only supports monomorphic FOL. % 224.69/32.33 % (1736008)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=2495198588:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2749 on theBenchmark for (2749ds/57299Mi) % 224.69/32.33 % Exception at run slice level % 224.69/32.33 User error: GNN currently only supports monomorphic FOL. % 224.69/32.33 % (1736010)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=2569496887:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2744 on theBenchmark for (2744ds/127679Mi) % 224.69/32.33 % Exception at run slice level % 224.69/32.33 User error: GNN currently only supports monomorphic FOL. % 224.69/32.33 % (1736012)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=580244361:i=69402:add=on:aac=none:fsr=off_2739 on theBenchmark for (2739ds/69402Mi) % 224.69/32.33 % Exception at run slice level % 224.69/32.33 User error: GNN currently only supports monomorphic FOL. % 224.69/32.33 % (1736014)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=2010271522:i=100512:doe=on:fgj=on:bd=all:fsd=on_2734 on theBenchmark for (2734ds/100512Mi) % 224.69/32.33 % Exception at run slice level % 224.69/32.33 User error: GNN currently only supports monomorphic FOL. % 224.69/32.33 % (1736016)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=1241101737:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2729 on theBenchmark for (2729ds/138761Mi) % 224.69/32.33 % Exception at run slice level % 224.69/32.33 User error: GNN currently only supports monomorphic FOL. % 224.69/32.33 % (1736018)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=2786220693:i=282386:rtra=on_2724 on theBenchmark for (2724ds/282386Mi) % 224.69/32.33 % Exception at run slice level % 235.36/33.88 User error: GNN currently only supports monomorphic FOL. % 235.36/33.88 % (1736020)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=1819616898:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2720 on theBenchmark for (2720ds/269354Mi) % 235.36/33.88 % Exception at run slice level % 235.36/33.88 User error: GNN currently only supports monomorphic FOL. % 235.36/33.88 % (1736022)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=1344014958:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2715 on theBenchmark for (2715ds/283390Mi) % 235.36/33.88 % (1736022)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 235.36/33.88 % Exception at run slice level % 235.36/33.88 User error: GNN currently only supports monomorphic FOL. % 235.36/33.88 % (1736024)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=3587295420:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2710 on theBenchmark for (2710ds/218Mi) % 235.36/33.88 % (1736024)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 235.36/33.88 % (1736024)Refutation not found, incomplete strategy % 235.36/33.88 % (1736024)------------------------------ % 235.36/33.88 % (1736024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.36/33.88 % (1736024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.36/33.88 % (1736024)CaDiCaL version: 2.1.3 % 235.36/33.88 % (1736024)Termination reason: Refutation not found, incomplete strategy % 235.36/33.88 % (1736024)Time elapsed: 0.002 s % 235.36/33.88 % (1736024)Peak memory usage: 88 MB % 235.36/33.88 % (1736024)Instructions burned: 2 (million) % 235.36/33.88 % (1736024)------------------------------ % 235.36/33.88 % (1736024)------------------------------ % 235.36/33.88 % (1736026)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=373840788:i=238:av=off:rtra=on:ss=axioms_2706 on theBenchmark for (2706ds/238Mi) % 235.36/33.88 % (1736026)Instruction limit reached! % 235.36/33.88 % (1736026)------------------------------ % 235.36/33.88 % (1736026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.36/33.88 % (1736026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.36/33.88 % (1736026)CaDiCaL version: 2.1.3 % 235.36/33.88 % (1736026)Termination reason: Instruction limit % 235.36/33.88 % (1736026)Termination phase: Saturation % 235.36/33.88 % (1736026)Time elapsed: 0.139 s % 235.36/33.88 % (1736026)Peak memory usage: 89 MB % 235.36/33.88 % (1736026)Instructions burned: 239 (million) % 235.36/33.88 % (1736028)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=1181463108:s2a=on:i=278:rtra=on:gtg=position_2703 on theBenchmark for (2703ds/278Mi) % 235.36/33.88 % (1736028)Instruction limit reached! % 235.36/33.88 % (1736028)------------------------------ % 235.36/33.88 % (1736028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.36/33.88 % (1736028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.36/33.88 % (1736028)CaDiCaL version: 2.1.3 % 235.36/33.88 % (1736028)Termination reason: Instruction limit % 235.36/33.88 % (1736028)Termination phase: Saturation % 235.36/33.88 % (1736028)Time elapsed: 0.183 s % 235.36/33.88 % (1736028)Peak memory usage: 91 MB % 235.36/33.88 % (1736028)Instructions burned: 279 (million) % 235.36/33.88 % (1736030)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=1907679424:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2700 on theBenchmark for (2700ds/258Mi) % 235.36/33.88 % (1736030)Instruction limit reached! % 235.36/33.88 % (1736030)------------------------------ % 235.36/33.88 % (1736030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.36/33.88 % (1736030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.36/33.88 % (1736030)CaDiCaL version: 2.1.3 % 235.36/33.88 % (1736030)Termination reason: Instruction limit % 235.36/33.88 % (1736030)Termination phase: Saturation % 235.36/33.88 % (1736030)Time elapsed: 0.134 s % 235.36/33.88 % (1736030)Peak memory usage: 89 MB % 235.36/33.88 % (1736030)Instructions burned: 260 (million) % 235.36/33.88 % (1736032)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=3785789639:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2698 on theBenchmark for (2698ds/570Mi) % 235.36/33.88 % (1735982)Instruction limit reached! % 235.36/33.88 % (1735982)------------------------------ % 235.36/33.88 % (1735982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.84/34.54 % (1735982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.84/34.54 % (1735982)CaDiCaL version: 2.1.3 % 239.84/34.54 % (1735982)Termination reason: Instruction limit % 239.84/34.54 % (1735982)Termination phase: Saturation % 239.84/34.54 % (1735982)Time elapsed: 13.081 s % 239.84/34.54 % (1735982)Peak memory usage: 154 MB % 239.84/34.54 % (1735982)Instructions burned: 21161 (million) % 239.84/34.54 % (1736034)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=1734006634:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2695 on theBenchmark for (2695ds/314Mi) % 239.84/34.54 % (1736032)Instruction limit reached! % 239.84/34.54 % (1736032)------------------------------ % 239.84/34.54 % (1736032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.84/34.54 % (1736032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.84/34.54 % (1736032)CaDiCaL version: 2.1.3 % 239.84/34.54 % (1736032)Termination reason: Instruction limit % 239.84/34.54 % (1736032)Termination phase: Saturation % 239.84/34.54 % (1736032)Time elapsed: 0.351 s % 239.84/34.54 % (1736032)Peak memory usage: 92 MB % 239.84/34.54 % (1736032)Instructions burned: 571 (million) % 239.84/34.54 % (1736034)Instruction limit reached! % 239.84/34.54 % (1736034)------------------------------ % 239.84/34.54 % (1736034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.84/34.54 % (1736034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.84/34.54 % (1736034)CaDiCaL version: 2.1.3 % 239.84/34.54 % (1736034)Termination reason: Instruction limit % 239.84/34.54 % (1736034)Termination phase: Saturation % 239.84/34.54 % (1736034)Time elapsed: 0.150 s % 239.84/34.54 % (1736034)Peak memory usage: 91 MB % 239.84/34.54 % (1736034)Instructions burned: 316 (million) % 239.84/34.54 % (1736036)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=3443152384:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2693 on theBenchmark for (2693ds/650Mi) % 239.84/34.54 % (1736037)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=1556942360:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2692 on theBenchmark for (2692ds/496Mi) % 239.84/34.54 % (1736037)Instruction limit reached! % 239.84/34.54 % (1736037)------------------------------ % 239.84/34.54 % (1736037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.84/34.54 % (1736037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.84/34.54 % (1736037)CaDiCaL version: 2.1.3 % 239.84/34.54 % (1736037)Termination reason: Instruction limit % 239.84/34.54 % (1736037)Termination phase: Saturation % 239.84/34.54 % (1736037)Time elapsed: 0.271 s % 239.84/34.54 % (1736037)Peak memory usage: 92 MB % 239.84/34.54 % (1736037)Instructions burned: 497 (million) % 239.84/34.54 % (1736036)Instruction limit reached! % 239.84/34.54 % (1736036)------------------------------ % 239.84/34.54 % (1736036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.84/34.54 % (1736036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.84/34.54 % (1736036)CaDiCaL version: 2.1.3 % 239.84/34.54 % (1736036)Termination reason: Instruction limit % 239.84/34.54 % (1736036)Termination phase: Saturation % 239.84/34.54 % (1736036)Time elapsed: 0.387 s % 239.84/34.54 % (1736036)Peak memory usage: 92 MB % 239.84/34.54 % (1736036)Instructions burned: 651 (million) % 239.84/34.54 % (1736040)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=4071386470:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2688 on theBenchmark for (2688ds/588Mi) % 239.84/34.54 % (1736040)Refutation not found, incomplete strategy % 239.84/34.54 % (1736040)------------------------------ % 239.84/34.54 % (1736040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.84/34.54 % (1736040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.84/34.54 % (1736040)CaDiCaL version: 2.1.3 % 239.84/34.54 % (1736040)Termination reason: Refutation not found, incomplete strategy % 239.84/34.54 % (1736040)Time elapsed: 0.008 s % 239.84/34.54 % (1736040)Peak memory usage: 88 MB % 239.84/34.54 % (1736040)Instructions burned: 12 (million) % 239.84/34.54 % (1736041)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=2217077190:i=4700:rtra=on_2688 on theBenchmark for (2688ds/4700Mi) % 239.84/34.54 % (1736040)------------------------------ % 239.84/34.54 % (1736040)------------------------------ % 239.84/34.54 % (1736044)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4240699406:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2684 on theBenchmark for (2684ds/226Mi) % 247.80/35.61 % Exception at run slice level % 247.80/35.61 User error: GNN currently only supports monomorphic FOL. % 247.80/35.61 % (1736044)Instruction limit reached! % 247.80/35.61 % (1736044)------------------------------ % 247.80/35.61 % (1736044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.80/35.61 % (1736044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.80/35.61 % (1736044)CaDiCaL version: 2.1.3 % 247.80/35.61 % (1736044)Termination reason: Instruction limit % 247.80/35.61 % (1736044)Termination phase: Saturation % 247.80/35.61 % (1736044)Time elapsed: 0.146 s % 247.80/35.61 % (1736044)Peak memory usage: 91 MB % 247.80/35.61 % (1736044)Instructions burned: 227 (million) % 247.80/35.61 % (1736046)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1391655796:i=254:av=off:fsr=off:rtra=on:sup=off_2683 on theBenchmark for (2683ds/254Mi) % 247.80/35.61 % (1736046)Refutation not found, incomplete strategy % 247.80/35.61 % (1736046)------------------------------ % 247.80/35.61 % (1736046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.80/35.61 % (1736046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.80/35.61 % (1736046)CaDiCaL version: 2.1.3 % 247.80/35.61 % (1736046)Termination reason: Refutation not found, incomplete strategy % 247.80/35.61 % (1736046)Time elapsed: 0.009 s % 247.80/35.61 % (1736046)Peak memory usage: 88 MB % 247.80/35.61 % (1736046)Instructions burned: 15 (million) % 247.80/35.61 % (1736047)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=2639471162:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2681 on theBenchmark for (2681ds/228Mi) % 247.80/35.61 % (1736047)Refutation not found, incomplete strategy % 247.80/35.61 % (1736047)------------------------------ % 247.80/35.61 % (1736047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.80/35.61 % (1736047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.80/35.61 % (1736047)CaDiCaL version: 2.1.3 % 247.80/35.61 % (1736047)Termination reason: Refutation not found, incomplete strategy % 247.80/35.61 % (1736047)Time elapsed: 0.004 s % 247.80/35.61 % (1736047)Peak memory usage: 88 MB % 247.80/35.61 % (1736047)Instructions burned: 6 (million) % 247.80/35.61 % (1736046)------------------------------ % 247.80/35.61 % (1736046)------------------------------ % 247.80/35.61 % (1736047)------------------------------ % 247.80/35.61 % (1736047)------------------------------ % 247.80/35.61 % (1736050)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=1240824078:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2679 on theBenchmark for (2679ds/1814Mi) % 247.80/35.61 % (1736052)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=811801333:i=874:sd=1:aac=none:rtra=on:ss=included_2678 on theBenchmark for (2678ds/874Mi) % 247.80/35.61 % (1736052)Refutation not found, incomplete strategy % 247.80/35.61 % (1736052)------------------------------ % 247.80/35.61 % (1736052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.80/35.61 % (1736052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.80/35.61 % (1736052)CaDiCaL version: 2.1.3 % 247.80/35.61 % (1736052)Termination reason: Refutation not found, incomplete strategy % 247.80/35.61 % (1736052)Time elapsed: 0.009 s % 247.80/35.61 % (1736052)Peak memory usage: 88 MB % 247.80/35.61 % (1736052)Instructions burned: 13 (million) % 247.80/35.61 % (1736052)------------------------------ % 247.80/35.61 % (1736052)------------------------------ % 247.80/35.61 % (1736054)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=2944520190:i=10404:rtra=on:ss=axioms:sgt=16_2674 on theBenchmark for (2674ds/10404Mi) % 247.80/35.61 % Exception at run slice level % 247.80/35.61 User error: GNN currently only supports monomorphic FOL. % 247.80/35.61 % (1735986)Instruction limit reached! % 247.80/35.61 % (1735986)------------------------------ % 247.80/35.61 % (1735986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.80/35.61 % (1735986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.80/35.61 % (1735986)CaDiCaL version: 2.1.3 % 247.80/35.61 % (1735986)Termination reason: Instruction limit % 247.80/35.61 % (1735986)Termination phase: Saturation % 247.80/35.61 % (1735986)Time elapsed: 13.279 s % 247.80/35.61 % (1735986)Peak memory usage: 152 MB % 247.80/35.61 % (1735986)Instructions burned: 23714 (million) % 247.80/35.61 % (1736056)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3518769754:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2669 on theBenchmark for (2669ds/268Mi) % 260.97/37.40 % (1736057)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=3504409151:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2669 on theBenchmark for (2669ds/1184Mi) % 260.97/37.40 % (1736050)Instruction limit reached! % 260.97/37.40 % (1736050)------------------------------ % 260.97/37.40 % (1736050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.97/37.40 % (1736050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.97/37.40 % (1736050)CaDiCaL version: 2.1.3 % 260.97/37.40 % (1736050)Termination reason: Instruction limit % 260.97/37.40 % (1736050)Termination phase: Saturation % 260.97/37.40 % (1736050)Time elapsed: 1.134 s % 260.97/37.40 % (1736050)Peak memory usage: 99 MB % 260.97/37.40 % (1736050)Instructions burned: 1815 (million) % 260.97/37.40 % (1736056)Instruction limit reached! % 260.97/37.40 % (1736056)------------------------------ % 260.97/37.40 % (1736056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.97/37.40 % (1736056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.97/37.40 % (1736056)CaDiCaL version: 2.1.3 % 260.97/37.40 % (1736056)Termination reason: Instruction limit % 260.97/37.40 % (1736056)Termination phase: Saturation % 260.97/37.40 % (1736056)Time elapsed: 0.137 s % 260.97/37.40 % (1736056)Peak memory usage: 90 MB % 260.97/37.40 % (1736056)Instructions burned: 268 (million) % 260.97/37.40 % (1736060)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=2009866911:st=3:i=26386:sd=3:rtra=on:ss=axioms_2666 on theBenchmark for (2666ds/26386Mi) % 260.97/37.40 % (1736061)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=1819478640:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2666 on theBenchmark for (2666ds/250Mi) % 260.97/37.40 % (1736061)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 260.97/37.40 % (1736061)Instruction limit reached! % 260.97/37.40 % (1736061)------------------------------ % 260.97/37.40 % (1736061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.97/37.40 % (1736061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.97/37.40 % (1736061)CaDiCaL version: 2.1.3 % 260.97/37.40 % (1736061)Termination reason: Instruction limit % 260.97/37.40 % (1736061)Termination phase: Saturation % 260.97/37.40 % (1736061)Time elapsed: 0.128 s % 260.97/37.40 % (1736061)Peak memory usage: 91 MB % 260.97/37.40 % (1736061)Instructions burned: 252 (million) % 260.97/37.40 % (1736064)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=26388989:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2664 on theBenchmark for (2664ds/268Mi) % 260.97/37.40 % Exception at run slice level % 260.97/37.40 User error: Immediate (shared) subterms of term/literal combb(fun(X2,X1),fun(fun(X2,bool),X1),X0,big_co1399186613setsum(X2,X1),combc(X2,X0,X1,X4)) = sF16(X2,X1,X0,X4) have different types/not well-typed! % 260.97/37.40 % Exception at run slice level % 260.97/37.40 User error: GNN currently only supports monomorphic FOL. % 260.97/37.40 % (1736066)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3398205209:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2662 on theBenchmark for (2662ds/282Mi) % 260.97/37.40 % (1736066)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 260.97/37.40 % (1736066)Refutation not found, incomplete strategy % 260.97/37.40 % (1736066)------------------------------ % 260.97/37.40 % (1736066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.97/37.40 % (1736066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.97/37.40 % (1736066)CaDiCaL version: 2.1.3 % 260.97/37.40 % (1736066)Termination reason: Refutation not found, incomplete strategy % 260.97/37.40 % (1736066)Time elapsed: 0.003 s % 260.97/37.40 % (1736066)Peak memory usage: 88 MB % 260.97/37.40 % (1736066)Instructions burned: 2 (million) % 260.97/37.40 % (1736057)Instruction limit reached! % 260.97/37.40 % (1736057)------------------------------ % 260.97/37.40 % (1736057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.97/37.40 % (1736057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.97/37.40 % (1736057)CaDiCaL version: 2.1.3 % 260.97/37.40 % (1736057)Termination reason: Instruction limit % 260.97/37.40 % (1736057)Termination phase: Saturation % 260.97/37.40 % (1736057)Time elapsed: 0.656 s % 260.97/37.40 % (1736057)Peak memory usage: 94 MB % 260.97/37.40 % (1736057)Instructions burned: 1184 (million) % 270.31/38.99 % (1736067)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=205491684:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2661 on theBenchmark for (2661ds/862Mi) % 270.31/38.99 % (1736069)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=3193867928:i=12120:aac=none:ins=25:rtra=on_2661 on theBenchmark for (2661ds/12120Mi) % 270.31/38.99 % (1736066)------------------------------ % 270.31/38.99 % (1736066)------------------------------ % 270.31/38.99 % (1736072)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=3192174799:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2658 on theBenchmark for (2658ds/300Mi) % 270.31/38.99 % (1736072)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 270.31/38.99 % (1736067)Instruction limit reached! % 270.31/38.99 % (1736067)------------------------------ % 270.31/38.99 % (1736067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.31/38.99 % (1736067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.31/38.99 % (1736067)CaDiCaL version: 2.1.3 % 270.31/38.99 % (1736067)Termination reason: Instruction limit % 270.31/38.99 % (1736067)Termination phase: Saturation % 270.31/38.99 % (1736067)Time elapsed: 0.368 s % 270.31/38.99 % (1736067)Peak memory usage: 96 MB % 270.31/38.99 % (1736067)Instructions burned: 862 (million) % 270.31/38.99 % Exception at run slice level % 270.31/38.99 User error: GNN currently only supports monomorphic FOL. % 270.31/38.99 % (1736072)Instruction limit reached! % 270.31/38.99 % (1736072)------------------------------ % 270.31/38.99 % (1736072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.31/38.99 % (1736072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.31/38.99 % (1736072)CaDiCaL version: 2.1.3 % 270.31/38.99 % (1736072)Termination reason: Instruction limit % 270.31/38.99 % (1736072)Termination phase: Saturation % 270.31/38.99 % (1736072)Time elapsed: 0.192 s % 270.31/38.99 % (1736072)Peak memory usage: 93 MB % 270.31/38.99 % (1736072)Instructions burned: 300 (million) % 270.31/38.99 % (1736074)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=2513136998:i=28310:bd=all:rtra=on_2656 on theBenchmark for (2656ds/28310Mi) % 270.31/38.99 % (1736075)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2881523316:i=1334:av=off:fsr=off:rtra=on_2656 on theBenchmark for (2656ds/1334Mi) % 270.31/38.99 % (1736075)Refutation not found, incomplete strategy % 270.31/38.99 % (1736075)------------------------------ % 270.31/38.99 % (1736075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.31/38.99 % (1736075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.31/38.99 % (1736075)CaDiCaL version: 2.1.3 % 270.31/38.99 % (1736075)Termination reason: Refutation not found, incomplete strategy % 270.31/38.99 % (1736075)Time elapsed: 0.008 s % 270.31/38.99 % (1736075)Peak memory usage: 88 MB % 270.31/38.99 % (1736075)Instructions burned: 11 (million) % 270.31/38.99 % (1736076)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=3823615670:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2655 on theBenchmark for (2655ds/370Mi) % 270.31/38.99 % (1736075)------------------------------ % 270.31/38.99 % (1736075)------------------------------ % 270.31/38.99 % (1736076)Instruction limit reached! % 270.31/38.99 % (1736076)------------------------------ % 270.31/38.99 % (1736076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.31/38.99 % (1736076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.31/38.99 % (1736076)CaDiCaL version: 2.1.3 % 270.31/38.99 % (1736076)Termination reason: Instruction limit % 270.31/38.99 % (1736076)Termination phase: Saturation % 270.31/38.99 % (1736076)Time elapsed: 0.216 s % 270.31/38.99 % (1736076)Peak memory usage: 92 MB % 270.31/38.99 % (1736076)Instructions burned: 371 (million) % 270.31/38.99 % Exception at run slice level % 270.31/38.99 User error: GNN currently only supports monomorphic FOL. % 270.31/38.99 % (1736080)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=380712278:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2652 on theBenchmark for (2652ds/386Mi) % 270.31/38.99 % (1736081)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=1054890497:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2651 on theBenchmark for (2651ds/9700Mi) % 280.58/40.30 % (1736081)Refutation not found, incomplete strategy % 280.58/40.30 % (1736081)------------------------------ % 280.58/40.30 % (1736081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.58/40.30 % (1736081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.58/40.30 % (1736081)CaDiCaL version: 2.1.3 % 280.58/40.30 % (1736081)Termination reason: Refutation not found, incomplete strategy % 280.58/40.30 % (1736081)Time elapsed: 0.007 s % 280.58/40.30 % (1736081)Peak memory usage: 88 MB % 280.58/40.30 % (1736081)Instructions burned: 10 (million) % 280.58/40.30 % (1736082)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=743738350:i=24222:sd=1:rtra=on:ss=included_2651 on theBenchmark for (2651ds/24222Mi) % 280.58/40.30 % (1736080)Instruction limit reached! % 280.58/40.30 % (1736080)------------------------------ % 280.58/40.30 % (1736080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.58/40.30 % (1736080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.58/40.30 % (1736080)CaDiCaL version: 2.1.3 % 280.58/40.30 % (1736080)Termination reason: Instruction limit % 280.58/40.30 % (1736080)Termination phase: Saturation % 280.58/40.30 % (1736080)Time elapsed: 0.253 s % 280.58/40.30 % (1736080)Peak memory usage: 94 MB % 280.58/40.30 % (1736080)Instructions burned: 387 (million) % 280.58/40.30 % (1736081)------------------------------ % 280.58/40.30 % (1736081)------------------------------ % 280.58/40.30 % (1736086)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=3472762324:i=638:kws=precedence:fsr=off:rtra=on_2648 on theBenchmark for (2648ds/638Mi) % 280.58/40.30 % Exception at run slice level % 280.58/40.30 User error: GNN currently only supports monomorphic FOL. % 280.58/40.30 % (1736087)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=21672441:i=4128:ep=RST:rtra=on_2648 on theBenchmark for (2648ds/4128Mi) % 280.58/40.30 % (1736090)dis-1011_128_sil=32000:si=on:random_seed=3908802966:i=7412:ep=RST:av=off:rtra=on_2646 on theBenchmark for (2646ds/7412Mi) % 280.58/40.30 % (1736086)Instruction limit reached! % 280.58/40.30 % (1736086)------------------------------ % 280.58/40.30 % (1736086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.58/40.30 % (1736086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.58/40.30 % (1736086)CaDiCaL version: 2.1.3 % 280.58/40.30 % (1736086)Termination reason: Instruction limit % 280.58/40.30 % (1736086)Termination phase: Saturation % 280.58/40.30 % (1736086)Time elapsed: 0.346 s % 280.58/40.30 % (1736086)Peak memory usage: 93 MB % 280.58/40.30 % (1736086)Instructions burned: 638 (million) % 280.58/40.30 % (1736092)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=362206231:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2644 on theBenchmark for (2644ds/1514Mi) % 280.58/40.30 % (1735910)Instruction limit reached! % 280.58/40.30 % (1735910)------------------------------ % 280.58/40.30 % (1735910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.58/40.30 % (1735910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.58/40.30 % (1735910)CaDiCaL version: 2.1.3 % 280.58/40.30 % (1735910)Termination reason: Instruction limit % 280.58/40.30 % (1735910)Termination phase: Saturation % 280.58/40.30 % (1735910)Time elapsed: 27.417 s % 280.58/40.30 % (1735910)Peak memory usage: 236 MB % 280.58/40.30 % (1735910)Instructions burned: 43699 (million) % 280.58/40.30 % (1736094)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=2058551343:i=27826:rtra=on:ss=axioms:sgt=8_2637 on theBenchmark for (2637ds/27826Mi) % 280.58/40.30 % (1736092)Instruction limit reached! % 280.58/40.30 % (1736092)------------------------------ % 280.58/40.30 % (1736092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.58/40.30 % (1736092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.58/40.30 % (1736092)CaDiCaL version: 2.1.3 % 280.58/40.30 % (1736092)Termination reason: Instruction limit % 280.58/40.30 % (1736092)Termination phase: Saturation % 280.58/40.30 % (1736092)Time elapsed: 0.990 s % 280.58/40.30 % (1736092)Peak memory usage: 96 MB % 280.58/40.30 % (1736092)Instructions burned: 1514 (million) % 280.58/40.30 % Exception at run slice level % 280.58/40.30 User error: GNN currently only supports monomorphic FOL. % 295.02/42.23 % (1736096)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=3502052229:i=19850:aac=none:rtra=on_2632 on theBenchmark for (2632ds/19850Mi) % 295.02/42.23 % (1736097)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2839831620:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2632 on theBenchmark for (2632ds/4958Mi) % 295.02/42.23 % (1736097)Refutation not found, incomplete strategy % 295.02/42.23 % (1736097)------------------------------ % 295.02/42.23 % (1736097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.02/42.23 % (1736097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.02/42.23 % (1736097)CaDiCaL version: 2.1.3 % 295.02/42.23 % (1736097)Termination reason: Refutation not found, incomplete strategy % 295.02/42.23 % (1736097)Time elapsed: 0.005 s % 295.02/42.23 % (1736097)Peak memory usage: 88 MB % 295.02/42.23 % (1736097)Instructions burned: 6 (million) % 295.02/42.23 % (1736097)------------------------------ % 295.02/42.23 % (1736097)------------------------------ % 295.02/42.23 % Exception at run slice level % 295.02/42.23 User error: GNN currently only supports monomorphic FOL. % 295.02/42.23 % (1736100)ott+1002_64_sil=16000:si=on:sp=const_min:nwc=0.5:random_seed=1261547694:i=880:nm=2:av=off:rtra=on:gtg=exists_all:fdi=8:gsp=on_2628 on theBenchmark for (2628ds/880Mi) % 295.02/42.23 % (1736100)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 295.02/42.23 % (1736101)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=3250201031:st=1.5:i=22290:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2628 on theBenchmark for (2628ds/22290Mi) % 295.02/42.23 % (1736087)Instruction limit reached! % 295.02/42.23 % (1736087)------------------------------ % 295.02/42.23 % (1736087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.02/42.23 % (1736087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.02/42.23 % (1736087)CaDiCaL version: 2.1.3 % 295.02/42.23 % (1736087)Termination reason: Instruction limit % 295.02/42.23 % (1736087)Termination phase: Saturation % 295.02/42.23 % (1736087)Time elapsed: 2.133 s % 295.02/42.23 % (1736087)Peak memory usage: 102 MB % 295.02/42.23 % (1736087)Instructions burned: 4129 (million) % 295.02/42.23 % (1736104)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=3279101826:cts=off:i=6068:av=off:rtra=on:er=known:fsd=on_2625 on theBenchmark for (2625ds/6068Mi) % 295.02/42.23 % Exception at run slice level % 295.02/42.23 User error: GNN currently only supports monomorphic FOL. % 295.02/42.23 % (1736100)Instruction limit reached! % 295.02/42.23 % (1736100)------------------------------ % 295.02/42.23 % (1736100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.02/42.23 % (1736100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.02/42.23 % (1736100)CaDiCaL version: 2.1.3 % 295.02/42.23 % (1736100)Termination reason: Instruction limit % 295.02/42.23 % (1736100)Termination phase: Saturation % 295.02/42.23 % (1736100)Time elapsed: 0.507 s % 295.02/42.23 % (1736100)Peak memory usage: 89 MB % 295.02/42.23 % (1736100)Instructions burned: 881 (million) % 295.02/42.23 % (1736106)lrs-1011_64:1_sil=8000:si=on:erd=off:urr=on:nwc=0.7:br=off:random_seed=1085755335:st=2:s2a=on:i=1048:s2at=2:rtra=on:ss=axioms_2623 on theBenchmark for (2623ds/1048Mi) % 295.02/42.23 % (1736107)lrs+1011_16:1_sil=8000:si=on:acc=on:urr=on:fd=preordered:flr=on:random_seed=3367846407:avsq=on:i=2032:avsqr=676809,524288:sd=1:rtra=on:ss=axioms_2622 on theBenchmark for (2622ds/2032Mi) % 295.02/42.23 % Exception at run slice level % 295.02/42.23 User error: GNN currently only supports monomorphic FOL. % 295.02/42.23 % (1736110)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:si=on:s2agt=16:random_seed=3282711372:i=28246:bd=preordered:ins=4:rtra=on_2620 on theBenchmark for (2620ds/28246Mi) % 295.02/42.23 % (1736106)Instruction limit reached! % 295.02/42.23 % (1736106)------------------------------ % 295.02/42.23 % (1736106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.02/42.23 % (1736106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.02/42.23 % (1736106)CaDiCaL version: 2.1.3 % 295.02/42.23 % (1736106)Termination reason: Instruction limit % 295.02/42.23 % (1736106)Termination phase: Saturation % 295.02/42.23 % (1736106)Time elapsed: 0.525 s % 300.96/43.07 % (1736106)Peak memory usage: 93 MB % 300.96/43.07 % (1736106)Instructions burned: 1049 (million) % 300.96/43.07 % Exception at run slice level % 300.96/43.07 User error: GNN currently only supports monomorphic FOL. % 300.96/43.07 % (1736112)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:si=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3049440607:i=11562:kws=precedence:bd=all:rtra=on:rawr=on_2616 on theBenchmark for (2616ds/11562Mi) % 300.96/43.07 % (1736113)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:si=on:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=2441437986:i=4896:gtgl=5:bd=preordered:rtra=on:gtg=all_2615 on theBenchmark for (2615ds/4896Mi) % 300.96/43.07 % (1735990)Instruction limit reached! % 300.96/43.07 % (1735990)------------------------------ % 300.96/43.07 % (1735990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.96/43.07 % (1735990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.96/43.07 % (1735990)CaDiCaL version: 2.1.3 % 300.96/43.07 % (1735990)Termination reason: Instruction limit % 300.96/43.07 % (1735990)Termination phase: Saturation % 300.96/43.07 % (1735990)Time elapsed: 17.722 s % 300.96/43.07 % (1735990)Peak memory usage: 175 MB % 300.96/43.07 % (1735990)Instructions burned: 28958 (million) % 300.96/43.07 % (1736107)Instruction limit reached! % 300.96/43.07 % (1736107)------------------------------ % 300.96/43.07 % (1736107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.96/43.07 % (1736107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.96/43.07 % (1736107)CaDiCaL version: 2.1.3 % 300.96/43.07 % (1736107)Termination reason: Instruction limit % 300.96/43.07 % (1736107)Termination phase: Saturation % 300.96/43.07 % (1736107)Time elapsed: 0.979 s % 300.96/43.07 % (1736107)Peak memory usage: 99 MB % 300.96/43.07 % (1736107)Instructions burned: 2032 (million) % 300.96/43.07 % (1736116)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:si=on:lcm=reverse:random_seed=2018069074:i=6446:kws=precedence:fgj=on:av=off:rtra=on_2612 on theBenchmark for (2612ds/6446Mi) % 300.96/43.07 % Exception at run slice level % 300.96/43.07 User error: GNN currently only supports monomorphic FOL. % 300.96/43.07 % (1736117)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:si=on:sp=occurrence:sos=on:random_seed=1412455529:st=5.6:i=4066:sd=3:rtra=on:ss=axioms_2611 on theBenchmark for (2611ds/4066Mi) % 300.96/43.07 % (1736119)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:si=on:random_seed=2529798816:i=4110:nm=16:rtra=on:gtg=position:ss=axioms:fsd=on_2610 on theBenchmark for (2610ds/4110Mi) % 300.96/43.07 % Exception at run slice level % 300.96/43.07 User error: GNN currently only supports monomorphic FOL. % 300.96/43.07 % Exception at run slice level % 300.96/43.07 User error: GNN currently only supports monomorphic FOL. % 300.96/43.07 % (1736122)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:si=on:sp=const_frequency:spb=goal:acc=on:random_seed=148453067:i=43222:sd=3:rtra=on:ss=axioms_2607 on theBenchmark for (2607ds/43222Mi) % 300.96/43.07 % Exception at run slice level % 300.96/43.07 User error: GNN currently only supports monomorphic FOL. % 300.96/43.07 % (1736123)lrs+10_1_sil=8000:si=on:sp=occurrence:sos=all:lma=off:random_seed=2797777038:i=9670:sd=13:rtra=on:ss=axioms:sgt=23_2606 on theBenchmark for (2606ds/9670Mi) % 300.96/43.07 % (1736123)Refutation not found, incomplete strategy % 300.96/43.07 % (1736123)------------------------------ % 300.96/43.07 % (1736123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.96/43.07 % (1736123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.96/43.07 % (1736123)CaDiCaL version: 2.1.3 % 300.96/43.07 % (1736123)Termination reason: Refutation not found, incomplete strategy % 300.96/43.07 % (1736123)Time elapsed: 0.012 s % 300.96/43.07 % (1736123)Peak memory usage: 88 MB % 300.96/43.07 % (1736123)Instructions burned: 18 (million) % 300.96/43.07 % (1736125)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:si=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=3403241114:st=5:i=1594:s2at=3:sd=4:bs=unit_only:av=off:rtra=on:sup=off:ss=included_2605 on theBenchmark for (2605ds/1594Mi) % 300.96/43.07 % (1736090)Instruction limit reached! % 300.96/43.07 % (1736090)------------------------------ % 300.96/43.07 % (1736090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.96/43.07 % (1736090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.96/43.07 % (173 % 300.96/43.08 Terminated %------------------------------------------------------------------------------