%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW550_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 : n011.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:30:47 PM UTC 2026 % Result : Timeout 294.76s 42.23s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW550_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.10/0.19 % Computer : n011.cluster.edu % 0.10/0.19 % Model : x86_64 x86_64 % 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.19 % Memory : 8046.5625MB % 0.10/0.19 % OS : Linux 6.8.0-71-generic % 0.10/0.19 % CPULimit : 300 % 0.10/0.19 % WCLimit : 300 % 0.10/0.19 % DateTime : Mon Sep 28 14:18:31 UTC 2026 % 0.10/0.19 % CPUTime : % 0.10/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.10/0.23 Running first-order theorem proving % 0.10/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 % 4.69/1.52 % (3410225)Detected formulas, will run a generic FOF schedule. % 4.69/1.52 % (3410232)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=652387895:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 4.69/1.52 % (3410232)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 4.69/1.52 % (3410233)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3925157491:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 4.69/1.52 % (3410234)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2086435160:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 4.69/1.52 % (3410236)dis-21_1_sil=8000:lcm=predicate:random_seed=3014351083:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 4.69/1.52 % (3410230)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=185496347:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 4.69/1.52 % (3410235)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2990064277:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 4.69/1.52 % (3410231)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=3140246488:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 4.69/1.52 % (3410233)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 4.69/1.52 % (3410234)Instruction limit reached! % 4.69/1.52 % (3410234)------------------------------ % 4.69/1.52 % (3410234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.69/1.52 % (3410234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.69/1.52 % (3410234)CaDiCaL version: 2.1.3 % 4.69/1.52 % (3410234)Termination reason: Instruction limit % 4.69/1.52 % (3410234)Termination phase: Saturation % 4.69/1.52 % (3410234)Time elapsed: 0.061 s % 4.69/1.52 % (3410234)Peak memory usage: 88 MB % 4.69/1.52 % (3410234)Instructions burned: 121 (million) % 4.69/1.52 % (3410233)Instruction limit reached! % 4.69/1.52 % (3410233)------------------------------ % 4.69/1.52 % (3410233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.69/1.52 % (3410233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.69/1.52 % (3410233)CaDiCaL version: 2.1.3 % 4.69/1.52 % (3410233)Termination reason: Instruction limit % 4.69/1.52 % (3410233)Termination phase: Saturation % 4.69/1.52 % (3410233)Time elapsed: 0.061 s % 4.69/1.52 % (3410233)Peak memory usage: 89 MB % 4.69/1.52 % (3410233)Instructions burned: 110 (million) % 4.69/1.52 % (3410236)Instruction limit reached! % 4.69/1.52 % (3410236)------------------------------ % 4.69/1.52 % (3410236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.69/1.52 % (3410236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.69/1.52 % (3410236)CaDiCaL version: 2.1.3 % 4.69/1.52 % (3410236)Termination reason: Instruction limit % 4.69/1.52 % (3410236)Termination phase: Saturation % 4.69/1.52 % (3410236)Time elapsed: 0.071 s % 4.69/1.52 % (3410236)Peak memory usage: 89 MB % 4.69/1.52 % (3410236)Instructions burned: 130 (million) % 4.69/1.52 % (3410235)Instruction limit reached! % 4.69/1.52 % (3410235)------------------------------ % 4.69/1.52 % (3410235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.69/1.52 % (3410235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.69/1.52 % (3410235)CaDiCaL version: 2.1.3 % 4.69/1.52 % (3410235)Termination reason: Instruction limit % 4.69/1.52 % (3410235)Termination phase: Saturation % 4.69/1.52 % (3410235)Time elapsed: 0.089 s % 4.69/1.52 % (3410235)Peak memory usage: 90 MB % 4.69/1.52 % (3410235)Instructions burned: 140 (million) % 4.69/1.52 % Exception at run slice level % 4.69/1.52 User error: GNN currently only supports monomorphic FOL. % 4.69/1.52 % (3410244)lrs+10_1_sil=8000:sp=occurrence:random_seed=176991630:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 4.69/1.52 % (3410245)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1028083021:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 4.69/1.52 % (3410246)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3540600699:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 7.94/1.95 % (3410247)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=2329799242:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 7.94/1.95 % (3410248)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4197875757:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi) % 7.94/1.95 % (3410245)Instruction limit reached! % 7.94/1.95 % (3410245)------------------------------ % 7.94/1.95 % (3410245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.94/1.95 % (3410245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.94/1.95 % (3410245)CaDiCaL version: 2.1.3 % 7.94/1.95 % (3410245)Termination reason: Instruction limit % 7.94/1.95 % (3410245)Termination phase: Saturation % 7.94/1.95 % (3410245)Time elapsed: 0.085 s % 7.94/1.95 % (3410245)Peak memory usage: 90 MB % 7.94/1.95 % (3410245)Instructions burned: 159 (million) % 7.94/1.95 % (3410248)Instruction limit reached! % 7.94/1.95 % (3410248)------------------------------ % 7.94/1.95 % (3410248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.94/1.95 % (3410248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.94/1.95 % (3410248)CaDiCaL version: 2.1.3 % 7.94/1.95 % (3410248)Termination reason: Instruction limit % 7.94/1.95 % (3410248)Termination phase: Saturation % 7.94/1.95 % (3410248)Time elapsed: 0.088 s % 7.94/1.95 % (3410248)Peak memory usage: 90 MB % 7.94/1.95 % (3410248)Instructions burned: 296 (million) % 7.94/1.95 % (3410244)Instruction limit reached! % 7.94/1.95 % (3410244)------------------------------ % 7.94/1.95 % (3410244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.94/1.95 % (3410244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.94/1.95 % (3410244)CaDiCaL version: 2.1.3 % 7.94/1.95 % (3410244)Termination reason: Instruction limit % 7.94/1.95 % (3410244)Termination phase: Saturation % 7.94/1.95 % (3410244)Time elapsed: 0.156 s % 7.94/1.95 % (3410244)Peak memory usage: 90 MB % 7.94/1.95 % (3410244)Instructions burned: 285 (million) % 7.94/1.95 % (3410247)Instruction limit reached! % 7.94/1.95 % (3410247)------------------------------ % 7.94/1.95 % (3410247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.94/1.95 % (3410247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.94/1.95 % (3410247)CaDiCaL version: 2.1.3 % 7.94/1.95 % (3410247)Termination reason: Instruction limit % 7.94/1.95 % (3410247)Termination phase: Saturation % 7.94/1.95 % (3410247)Time elapsed: 0.130 s % 7.94/1.95 % (3410247)Peak memory usage: 90 MB % 7.94/1.95 % (3410247)Instructions burned: 250 (million) % 7.94/1.95 % Exception at run slice level % 7.94/1.95 User error: GNN currently only supports monomorphic FOL. % 7.94/1.95 % Exception at run slice level % 7.94/1.95 User error: GNN currently only supports monomorphic FOL. % 7.94/1.95 % (3410246)Instruction limit reached! % 7.94/1.95 % (3410246)------------------------------ % 7.94/1.95 % (3410246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.94/1.95 % (3410246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.94/1.95 % (3410246)CaDiCaL version: 2.1.3 % 7.94/1.95 % (3410246)Termination reason: Instruction limit % 7.94/1.95 % (3410246)Termination phase: Saturation % 7.94/1.95 % (3410246)Time elapsed: 0.180 s % 7.94/1.95 % (3410246)Peak memory usage: 91 MB % 7.94/1.95 % (3410246)Instructions burned: 328 (million) % 7.94/1.95 % (3410254)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1454210669:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 7.94/1.95 % (3410255)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1168360488:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi) % 7.94/1.95 % (3410255)Instruction limit reached! % 7.94/1.95 % (3410255)------------------------------ % 7.94/1.95 % (3410255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.94/1.95 % (3410255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.94/1.95 % (3410255)CaDiCaL version: 2.1.3 % 7.94/1.95 % (3410255)Termination reason: Instruction limit % 7.94/1.95 % (3410255)Termination phase: Saturation % 7.94/1.95 % (3410255)Time elapsed: 0.035 s % 7.94/1.95 % (3410255)Peak memory usage: 89 MB % 7.94/1.95 % (3410255)Instructions burned: 117 (million) % 7.94/1.95 % (3410256)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3103801912:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 10.04/2.12 % (3410258)lrs+10_1_sil=8000:sp=occurrence:random_seed=3457071712:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 10.04/2.12 % (3410257)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=719067142:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 10.04/2.12 % (3410259)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2102878575:i=437:sd=1:aac=none:ss=included_2994 on theBenchmark for (2994ds/437Mi) % 10.04/2.12 % (3410260)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1756915912:i=5202:ss=axioms:sgt=16_2994 on theBenchmark for (2994ds/5202Mi) % 10.04/2.12 % (3410259)Refutation not found, incomplete strategy % 10.04/2.12 % (3410259)------------------------------ % 10.04/2.12 % (3410259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.04/2.12 % (3410259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.04/2.12 % (3410259)CaDiCaL version: 2.1.3 % 10.04/2.12 % (3410259)Termination reason: Refutation not found, incomplete strategy % 10.04/2.12 % (3410259)Time elapsed: 0.012 s % 10.04/2.12 % (3410259)Peak memory usage: 89 MB % 10.04/2.12 % (3410259)Instructions burned: 20 (million) % 10.04/2.12 % (3410256)Instruction limit reached! % 10.04/2.12 % (3410256)------------------------------ % 10.04/2.12 % (3410256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.04/2.12 % (3410256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.04/2.12 % (3410256)CaDiCaL version: 2.1.3 % 10.04/2.12 % (3410256)Termination reason: Instruction limit % 10.04/2.12 % (3410256)Termination phase: Saturation % 10.04/2.12 % (3410256)Time elapsed: 0.058 s % 10.04/2.12 % (3410256)Peak memory usage: 88 MB % 10.04/2.12 % (3410256)Instructions burned: 128 (million) % 10.04/2.12 % (3410263)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2079652296:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2993 on theBenchmark for (2993ds/134Mi) % 10.04/2.12 % (3410257)Instruction limit reached! % 10.04/2.12 % (3410257)------------------------------ % 10.04/2.12 % (3410257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.04/2.12 % (3410257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.04/2.12 % (3410257)CaDiCaL version: 2.1.3 % 10.04/2.12 % (3410257)Termination reason: Instruction limit % 10.04/2.12 % (3410257)Termination phase: Saturation % 10.04/2.12 % (3410257)Time elapsed: 0.054 s % 10.04/2.12 % (3410257)Peak memory usage: 89 MB % 10.04/2.12 % (3410257)Instructions burned: 117 (million) % 10.04/2.12 % (3410263)Instruction limit reached! % 10.04/2.12 % (3410263)------------------------------ % 10.04/2.12 % (3410263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.04/2.12 % (3410263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.04/2.12 % (3410263)CaDiCaL version: 2.1.3 % 10.04/2.12 % (3410263)Termination reason: Instruction limit % 10.04/2.12 % (3410263)Termination phase: Saturation % 10.04/2.12 % (3410263)Time elapsed: 0.041 s % 10.04/2.12 % (3410263)Peak memory usage: 90 MB % 10.04/2.12 % (3410263)Instructions burned: 135 (million) % 10.04/2.12 % (3410269)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4021690792:st=8:i=592:sd=3:ep=RST:ss=axioms_2993 on theBenchmark for (2993ds/592Mi) % 10.04/2.12 % (3410272)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=2227114485:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2992 on theBenchmark for (2992ds/125Mi) % 10.04/2.12 % (3410272)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.04/2.12 % (3410271)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1825328344:st=3:i=13193:sd=3:ss=axioms_2992 on theBenchmark for (2992ds/13193Mi) % 10.04/2.12 % (3410272)Instruction limit reached! % 10.04/2.12 % (3410272)------------------------------ % 10.04/2.12 % (3410272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.04/2.12 % (3410272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.04/2.12 % (3410272)CaDiCaL version: 2.1.3 % 10.04/2.12 % (3410272)Termination reason: Instruction limit % 10.04/2.12 % (3410272)Termination phase: Saturation % 10.04/2.12 % (3410272)Time elapsed: 0.039 s % 13.79/2.82 % (3410272)Peak memory usage: 90 MB % 13.79/2.82 % (3410272)Instructions burned: 125 (million) % 13.79/2.82 % (3410259)------------------------------ % 13.79/2.82 % (3410259)------------------------------ % 13.79/2.82 % Exception at run slice level % 13.79/2.82 User error: GNN currently only supports monomorphic FOL. % 13.79/2.82 % (3410276)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2468943972:i=134:gtgl=5:slsql=off:gtg=exists_sym_2991 on theBenchmark for (2991ds/134Mi) % 13.79/2.82 % Exception at run slice level % 13.79/2.82 User error: Immediate (shared) subterms of term/literal huffma107959123e_case(X1,X0,X6,X5,huffma1146269203erNode(X1,X4,X3,X2)) = sF52(X1,X0,X6,X5,X4,X3,X2) have different types/not well-typed! % 13.79/2.82 % (3410280)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=189669568:i=6060:aac=none:ins=25_2990 on theBenchmark for (2990ds/6060Mi) % 13.79/2.82 % Exception at run slice level % 13.79/2.82 User error: GNN currently only supports monomorphic FOL. % 13.79/2.82 % (3410277)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1648811040:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/141Mi) % 13.79/2.82 % (3410277)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.79/2.82 % (3410277)Refutation not found, incomplete strategy % 13.79/2.82 % (3410277)------------------------------ % 13.79/2.82 % (3410277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.79/2.82 % (3410277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.79/2.82 % (3410277)CaDiCaL version: 2.1.3 % 13.79/2.82 % (3410277)Termination reason: Refutation not found, incomplete strategy % 13.79/2.82 % (3410277)Time elapsed: 0.006 s % 13.79/2.82 % (3410277)Peak memory usage: 89 MB % 13.79/2.82 % (3410277)Instructions burned: 9 (million) % 13.79/2.82 % (3410278)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3364132685:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2990 on theBenchmark for (2990ds/431Mi) % 13.79/2.82 % (3410258)Instruction limit reached! % 13.79/2.82 % (3410258)------------------------------ % 13.79/2.82 % (3410258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.79/2.82 % (3410258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.79/2.82 % (3410258)CaDiCaL version: 2.1.3 % 13.79/2.82 % (3410258)Termination reason: Instruction limit % 13.79/2.82 % (3410258)Termination phase: Saturation % 13.79/2.82 % (3410258)Time elapsed: 0.500 s % 13.79/2.82 % (3410258)Peak memory usage: 95 MB % 13.79/2.82 % (3410258)Instructions burned: 907 (million) % 13.79/2.82 % (3410269)Instruction limit reached! % 13.79/2.82 % (3410269)------------------------------ % 13.79/2.82 % (3410269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.79/2.82 % (3410269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.79/2.82 % (3410269)CaDiCaL version: 2.1.3 % 13.79/2.82 % (3410269)Termination reason: Instruction limit % 13.79/2.82 % (3410269)Termination phase: Saturation % 13.79/2.82 % (3410269)Time elapsed: 0.346 s % 13.79/2.82 % (3410269)Peak memory usage: 94 MB % 13.79/2.82 % (3410269)Instructions burned: 593 (million) % 13.79/2.82 % (3410282)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=918572154:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2989 on theBenchmark for (2989ds/150Mi) % 13.79/2.82 % (3410282)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.79/2.82 % Exception at run slice level % 13.79/2.82 User error: GNN currently only supports monomorphic FOL. % 13.79/2.82 % Exception at run slice level % 13.79/2.82 User error: GNN currently only supports monomorphic FOL. % 13.79/2.82 % (3410282)Instruction limit reached! % 13.79/2.82 % (3410282)------------------------------ % 13.79/2.82 % (3410282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.79/2.82 % (3410282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.79/2.82 % (3410282)CaDiCaL version: 2.1.3 % 13.79/2.82 % (3410282)Termination reason: Instruction limit % 13.79/2.82 % (3410282)Termination phase: Saturation % 13.79/2.82 % (3410282)Time elapsed: 0.089 s % 13.79/2.82 % (3410282)Peak memory usage: 89 MB % 13.79/2.82 % (3410282)Instructions burned: 151 (million) % 13.79/2.82 % (3410278)Instruction limit reached! % 19.48/3.69 % (3410278)------------------------------ % 19.48/3.69 % (3410278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.48/3.69 % (3410278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.48/3.69 % (3410278)CaDiCaL version: 2.1.3 % 19.48/3.69 % (3410278)Termination reason: Instruction limit % 19.48/3.69 % (3410278)Termination phase: Saturation % 19.48/3.69 % (3410278)Time elapsed: 0.217 s % 19.48/3.69 % (3410278)Peak memory usage: 90 MB % 19.48/3.69 % (3410278)Instructions burned: 432 (million) % 19.48/3.69 % (3410287)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=78021837:i=667:av=off:fsr=off_2988 on theBenchmark for (2988ds/667Mi) % 19.48/3.69 % (3410286)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=934886567:i=14155:bd=all_2988 on theBenchmark for (2988ds/14155Mi) % 19.48/3.69 % (3410287)Refutation not found, incomplete strategy % 19.48/3.69 % (3410287)------------------------------ % 19.48/3.69 % (3410287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.48/3.69 % (3410287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.48/3.69 % (3410287)CaDiCaL version: 2.1.3 % 19.48/3.69 % (3410287)Termination reason: Refutation not found, incomplete strategy % 19.48/3.69 % (3410287)Time elapsed: 0.018 s % 19.48/3.69 % (3410287)Peak memory usage: 89 MB % 19.48/3.69 % (3410287)Instructions burned: 37 (million) % 19.48/3.69 % (3410277)------------------------------ % 19.48/3.69 % (3410277)------------------------------ % 19.48/3.69 % (3410290)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4183707953:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2987 on theBenchmark for (2987ds/193Mi) % 19.48/3.69 % (3410289)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=2508921833:s2a=on:i=185:s2at=1.8:fdi=4_2988 on theBenchmark for (2988ds/185Mi) % 19.48/3.69 % (3410290)Instruction limit reached! % 19.48/3.69 % (3410290)------------------------------ % 19.48/3.69 % (3410290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.48/3.69 % (3410290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.48/3.69 % (3410290)CaDiCaL version: 2.1.3 % 19.48/3.69 % (3410290)Termination reason: Instruction limit % 19.48/3.69 % (3410290)Termination phase: Saturation % 19.48/3.69 % (3410290)Time elapsed: 0.051 s % 19.48/3.69 % (3410290)Peak memory usage: 90 MB % 19.48/3.69 % (3410290)Instructions burned: 195 (million) % 19.48/3.69 % (3410291)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3521064105:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2987 on theBenchmark for (2987ds/4850Mi) % 19.48/3.69 % (3410291)Refutation not found, incomplete strategy % 19.48/3.69 % (3410291)------------------------------ % 19.48/3.69 % (3410291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.48/3.69 % (3410291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.48/3.69 % (3410291)CaDiCaL version: 2.1.3 % 19.48/3.69 % (3410291)Termination reason: Refutation not found, incomplete strategy % 19.48/3.69 % (3410291)Time elapsed: 0.008 s % 19.48/3.69 % (3410291)Peak memory usage: 88 MB % 19.48/3.69 % (3410291)Instructions burned: 14 (million) % 19.48/3.69 % (3410294)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2604299467:i=12111:sd=1:ss=included_2987 on theBenchmark for (2987ds/12111Mi) % 19.48/3.69 % (3410289)Instruction limit reached! % 19.48/3.69 % (3410289)------------------------------ % 19.48/3.69 % (3410289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.48/3.69 % (3410289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.48/3.69 % (3410289)CaDiCaL version: 2.1.3 % 19.48/3.69 % (3410289)Termination reason: Instruction limit % 19.48/3.69 % (3410289)Termination phase: Saturation % 19.48/3.69 % (3410289)Time elapsed: 0.104 s % 19.48/3.69 % (3410289)Peak memory usage: 90 MB % 19.48/3.69 % (3410289)Instructions burned: 185 (million) % 19.48/3.69 % (3410296)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3687772710:i=319:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/319Mi) % 19.48/3.69 % (3410298)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=676670608:i=2064:ep=RST_2986 on theBenchmark for (2986ds/2064Mi) % 27.49/4.77 % (3410287)------------------------------ % 27.49/4.77 % (3410287)------------------------------ % 27.49/4.77 % (3410302)dis-1011_128_sil=32000:random_seed=3220404676:i=3706:ep=RST:av=off_2985 on theBenchmark for (2985ds/3706Mi) % 27.49/4.77 % (3410296)Instruction limit reached! % 27.49/4.77 % (3410296)------------------------------ % 27.49/4.77 % (3410296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.49/4.77 % (3410296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.49/4.77 % (3410296)CaDiCaL version: 2.1.3 % 27.49/4.77 % (3410296)Termination reason: Instruction limit % 27.49/4.77 % (3410296)Termination phase: Saturation % 27.49/4.77 % (3410296)Time elapsed: 0.158 s % 27.49/4.77 % (3410296)Peak memory usage: 90 MB % 27.49/4.77 % (3410296)Instructions burned: 320 (million) % 27.49/4.77 % (3410291)------------------------------ % 27.49/4.77 % (3410291)------------------------------ % 27.49/4.77 % Exception at run slice level % 27.49/4.77 User error: GNN currently only supports monomorphic FOL. % 27.49/4.77 % (3410304)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2308981262:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2984 on theBenchmark for (2984ds/757Mi) % 27.49/4.77 % (3410306)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=652401591:i=13913:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/13913Mi) % 27.49/4.77 % (3410307)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3413579061:i=9925:aac=none_2983 on theBenchmark for (2983ds/9925Mi) % 27.49/4.77 % (3410308)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1347619823:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2983 on theBenchmark for (2983ds/2479Mi) % 27.49/4.77 % Exception at run slice level % 27.49/4.77 User error: GNN currently only supports monomorphic FOL. % 27.49/4.77 % (3410308)Refutation not found, incomplete strategy % 27.49/4.77 % (3410308)------------------------------ % 27.49/4.77 % (3410308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.49/4.77 % (3410308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.49/4.77 % (3410308)CaDiCaL version: 2.1.3 % 27.49/4.77 % (3410308)Termination reason: Refutation not found, incomplete strategy % 27.49/4.77 % (3410308)Time elapsed: 0.010 s % 27.49/4.77 % (3410308)Peak memory usage: 89 MB % 27.49/4.77 % (3410308)Instructions burned: 17 (million) % 27.49/4.77 % (3410313)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=148779353:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2982 on theBenchmark for (2982ds/440Mi) % 27.49/4.77 % (3410313)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 27.49/4.77 % (3410308)------------------------------ % 27.49/4.77 % (3410308)------------------------------ % 27.49/4.77 % (3410304)Instruction limit reached! % 27.49/4.77 % (3410304)------------------------------ % 27.49/4.77 % (3410304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.49/4.77 % (3410304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.49/4.77 % (3410304)CaDiCaL version: 2.1.3 % 27.49/4.77 % (3410304)Termination reason: Instruction limit % 27.49/4.77 % (3410304)Termination phase: Saturation % 27.49/4.77 % (3410304)Time elapsed: 0.370 s % 27.49/4.77 % (3410304)Peak memory usage: 94 MB % 27.49/4.77 % (3410304)Instructions burned: 757 (million) % 27.49/4.77 % Exception at run slice level % 27.49/4.77 User error: GNN currently only supports monomorphic FOL. % 27.49/4.77 % (3410298)Instruction limit reached! % 27.49/4.77 % (3410298)------------------------------ % 27.49/4.77 % (3410298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.49/4.77 % (3410298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.49/4.77 % (3410298)CaDiCaL version: 2.1.3 % 27.49/4.77 % (3410298)Termination reason: Instruction limit % 27.49/4.77 % (3410298)Termination phase: Saturation % 27.49/4.77 % (3410298)Time elapsed: 0.640 s % 27.49/4.77 % (3410298)Peak memory usage: 101 MB % 27.49/4.77 % (3410298)Instructions burned: 2064 (million) % 27.49/4.77 % Exception at run slice level % 27.49/4.77 User error: GNN currently only supports monomorphic FOL. % 27.49/4.77 % (3410313)Instruction limit reached! % 27.49/4.77 % (3410313)------------------------------ % 27.49/4.77 % (3410313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.49/4.77 % (3410313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.49/4.77 % (3410313)CaDiCaL version: 2.1.3 % 33.07/5.43 % (3410313)Termination reason: Instruction limit % 33.07/5.43 % (3410313)Termination phase: Saturation % 33.07/5.43 % (3410313)Time elapsed: 0.233 s % 33.07/5.43 % (3410313)Peak memory usage: 89 MB % 33.07/5.43 % (3410313)Instructions burned: 441 (million) % 33.07/5.43 % (3410315)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1575258224:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2979 on theBenchmark for (2979ds/11145Mi) % 33.07/5.43 % (3410316)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=1045021753:cts=off:i=3034:av=off:er=known:fsd=on_2979 on theBenchmark for (2979ds/3034Mi) % 33.07/5.43 % (3410318)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2399720317:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2978 on theBenchmark for (2978ds/1016Mi) % 33.07/5.43 % (3410317)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3658459281:st=2:s2a=on:i=524:s2at=2:ss=axioms_2979 on theBenchmark for (2979ds/524Mi) % 33.07/5.43 % (3410319)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=4207050082:i=14123:bd=preordered:ins=4_2978 on theBenchmark for (2978ds/14123Mi) % 33.07/5.43 % (3410320)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=4077001842:i=5781:kws=precedence:bd=all:rawr=on_2978 on theBenchmark for (2978ds/5781Mi) % 33.07/5.43 % (3410317)Instruction limit reached! % 33.07/5.43 % (3410317)------------------------------ % 33.07/5.43 % (3410317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.07/5.43 % (3410317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.07/5.43 % (3410317)CaDiCaL version: 2.1.3 % 33.07/5.43 % (3410317)Termination reason: Instruction limit % 33.07/5.43 % (3410317)Termination phase: Saturation % 33.07/5.43 % (3410317)Time elapsed: 0.245 s % 33.07/5.43 % (3410317)Peak memory usage: 92 MB % 33.07/5.43 % (3410317)Instructions burned: 524 (million) % 33.07/5.43 % (3410318)Instruction limit reached! % 33.07/5.43 % (3410318)------------------------------ % 33.07/5.43 % (3410318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.07/5.43 % (3410318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.07/5.43 % (3410318)CaDiCaL version: 2.1.3 % 33.07/5.43 % (3410318)Termination reason: Instruction limit % 33.07/5.43 % (3410318)Termination phase: Saturation % 33.07/5.43 % (3410318)Time elapsed: 0.297 s % 33.07/5.43 % (3410318)Peak memory usage: 94 MB % 33.07/5.43 % (3410318)Instructions burned: 1017 (million) % 33.07/5.43 % Exception at run slice level % 33.07/5.43 User error: GNN currently only supports monomorphic FOL. % 33.07/5.43 % Exception at run slice level % 33.07/5.43 User error: GNN currently only supports monomorphic FOL. % 33.07/5.43 % (3410328)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=945278570:i=3223:kws=precedence:fgj=on:av=off_2975 on theBenchmark for (2975ds/3223Mi) % 33.07/5.43 % (3410327)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=4220614666:i=2448:gtgl=5:bd=preordered:gtg=all_2975 on theBenchmark for (2975ds/2448Mi) % 33.07/5.43 % Exception at run slice level % 33.07/5.43 User error: GNN currently only supports monomorphic FOL. % 33.07/5.43 % (3410329)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=400581318:st=5.6:i=2033:sd=3:ss=axioms_2974 on theBenchmark for (2974ds/2033Mi) % 33.07/5.43 % (3410330)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3840835300:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2974 on theBenchmark for (2974ds/2055Mi) % 33.07/5.43 % Exception at run slice level % 33.07/5.43 User error: GNN currently only supports monomorphic FOL. % 33.07/5.43 % (3410333)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=2605506624:i=21611:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/21611Mi) % 33.07/5.43 % (3410336)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1316783294:i=4835:sd=13:ss=axioms:sgt=23_2972 on theBenchmark for (2972ds/4835Mi) % 33.07/5.43 % Exception at run slice level % 33.07/5.43 User error: GNN currently only supports monomorphic FOL. % 33.07/5.43 % Exception at run slice level % 33.07/5.43 User error: GNN currently only supports monomorphic FOL. % 41.13/6.56 % Exception at run slice level % 41.13/6.56 User error: GNN currently only supports monomorphic FOL. % 41.13/6.56 % (3410339)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=2605016341:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2970 on theBenchmark for (2970ds/797Mi) % 41.13/6.56 % Exception at run slice level % 41.13/6.56 User error: GNN currently only supports monomorphic FOL. % 41.13/6.56 % (3410340)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=4228836524:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2969 on theBenchmark for (2969ds/2326Mi) % 41.13/6.56 % (3410341)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3659965733:i=6038:nm=6_2969 on theBenchmark for (2969ds/6038Mi) % 41.13/6.56 % (3410340)Refutation not found, incomplete strategy % 41.13/6.56 % (3410340)------------------------------ % 41.13/6.56 % (3410340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.13/6.56 % (3410340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.13/6.56 % (3410340)CaDiCaL version: 2.1.3 % 41.13/6.56 % (3410340)Termination reason: Refutation not found, incomplete strategy % 41.13/6.56 % (3410340)Time elapsed: 0.054 s % 41.13/6.56 % (3410340)Peak memory usage: 90 MB % 41.13/6.56 % (3410340)Instructions burned: 82 (million) % 41.13/6.56 % (3410343)lrs+10_1_sil=32000:sp=occurrence:random_seed=730416399:st=2:i=33334:sd=3:ss=included:sgt=32_2968 on theBenchmark for (2968ds/33334Mi) % 41.13/6.56 % (3410340)------------------------------ % 41.13/6.56 % (3410340)------------------------------ % 41.13/6.56 % Exception at run slice level % 41.13/6.56 User error: GNN currently only supports monomorphic FOL. % 41.13/6.56 % (3410339)Instruction limit reached! % 41.13/6.56 % (3410339)------------------------------ % 41.13/6.56 % (3410339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.13/6.56 % (3410339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.13/6.56 % (3410339)CaDiCaL version: 2.1.3 % 41.13/6.56 % (3410339)Termination reason: Instruction limit % 41.13/6.56 % (3410339)Termination phase: Saturation % 41.13/6.56 % (3410339)Time elapsed: 0.468 s % 41.13/6.56 % (3410339)Peak memory usage: 95 MB % 41.13/6.56 % (3410339)Instructions burned: 799 (million) % 41.13/6.56 % (3410347)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3290532845:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2965 on theBenchmark for (2965ds/1008Mi) % 41.13/6.56 % (3410302)Instruction limit reached! % 41.13/6.56 % (3410302)------------------------------ % 41.13/6.56 % (3410302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.13/6.56 % (3410302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.13/6.56 % (3410302)CaDiCaL version: 2.1.3 % 41.13/6.56 % (3410302)Termination reason: Instruction limit % 41.13/6.56 % (3410302)Termination phase: Saturation % 41.13/6.56 % (3410302)Time elapsed: 2.052 s % 41.13/6.56 % (3410302)Peak memory usage: 102 MB % 41.13/6.56 % (3410302)Instructions burned: 3706 (million) % 41.13/6.56 % (3410348)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=2399289362:i=8327:s2at=5:bd=preordered_2964 on theBenchmark for (2964ds/8327Mi) % 41.13/6.56 % (3410349)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=2299930286:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2964 on theBenchmark for (2964ds/1083Mi) % 41.13/6.56 % (3410351)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2580092928:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2963 on theBenchmark for (2963ds/1084Mi) % 41.13/6.56 % Exception at run slice level % 41.13/6.56 User error: GNN currently only supports monomorphic FOL. % 41.13/6.56 % (3410347)Instruction limit reached! % 41.13/6.56 % (3410347)------------------------------ % 41.13/6.56 % (3410347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.13/6.56 % (3410347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.13/6.56 % (3410347)CaDiCaL version: 2.1.3 % 41.13/6.56 % (3410347)Termination reason: Instruction limit % 52.58/8.04 % (3410347)Termination phase: Saturation % 52.58/8.04 % (3410347)Time elapsed: 0.540 s % 52.58/8.04 % (3410347)Peak memory usage: 97 MB % 52.58/8.04 % (3410347)Instructions burned: 1010 (million) % 52.58/8.04 % (3410355)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1168020592:i=6995:s2at=5:gtg=all_2959 on theBenchmark for (2959ds/6995Mi) % 52.58/8.04 % Exception at run slice level % 52.58/8.04 User error: Immediate (shared) subterms of term/literal huffma107959123e_case(X1,X0,X6,X5,huffma1146269203erNode(X1,X4,X3,X2)) = sF16(X1,X0,X6,X5,X4,X3,X2) have different types/not well-typed! % 52.58/8.04 % (3410336)Instruction limit reached! % 52.58/8.04 % (3410336)------------------------------ % 52.58/8.04 % (3410336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.58/8.04 % (3410336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.58/8.04 % (3410336)CaDiCaL version: 2.1.3 % 52.58/8.04 % (3410336)Termination reason: Instruction limit % 52.58/8.04 % (3410336)Termination phase: Saturation % 52.58/8.04 % (3410336)Time elapsed: 1.319 s % 52.58/8.04 % (3410336)Peak memory usage: 103 MB % 52.58/8.04 % (3410336)Instructions burned: 4837 (million) % 52.58/8.04 % (3410349)Instruction limit reached! % 52.58/8.04 % (3410349)------------------------------ % 52.58/8.04 % (3410349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.58/8.04 % (3410349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.58/8.04 % (3410349)CaDiCaL version: 2.1.3 % 52.58/8.04 % (3410349)Termination reason: Instruction limit % 52.58/8.04 % (3410349)Termination phase: Saturation % 52.58/8.04 % (3410349)Time elapsed: 0.553 s % 52.58/8.04 % (3410349)Peak memory usage: 98 MB % 52.58/8.04 % (3410349)Instructions burned: 1085 (million) % 52.58/8.04 % (3410356)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=3466327228:st=2:i=6225:sd=15:ss=axioms_2958 on theBenchmark for (2958ds/6225Mi) % 52.58/8.04 % (3410359)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=645123597:st=2.3:i=26457:sd=10:ss=included:sgt=8_2958 on theBenchmark for (2958ds/26457Mi) % 52.58/8.04 % (3410358)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3417476853:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2958 on theBenchmark for (2958ds/3372Mi) % 52.58/8.04 % (3410351)Instruction limit reached! % 52.58/8.04 % (3410351)------------------------------ % 52.58/8.04 % (3410351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.58/8.04 % (3410351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.58/8.04 % (3410351)CaDiCaL version: 2.1.3 % 52.58/8.04 % (3410351)Termination reason: Instruction limit % 52.58/8.04 % (3410351)Termination phase: Saturation % 52.58/8.04 % (3410351)Time elapsed: 0.532 s % 52.58/8.04 % (3410351)Peak memory usage: 94 MB % 52.58/8.04 % (3410351)Instructions burned: 1084 (million) % 52.58/8.04 % (3410360)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=2728473824:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2957 on theBenchmark for (2957ds/13494Mi) % 52.58/8.04 % (3410364)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=549227781:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2957 on theBenchmark for (2957ds/2503Mi) % 52.58/8.04 % (3410364)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 52.58/8.04 % Exception at run slice level % 52.58/8.04 User error: GNN currently only supports monomorphic FOL. % 52.58/8.04 % (3410367)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=2663507768:i=2559:sd=1:ep=RSTC:ss=axioms_2955 on theBenchmark for (2955ds/2559Mi) % 52.58/8.04 % Exception at run slice level % 52.58/8.04 User error: GNN currently only supports monomorphic FOL. % 52.58/8.04 % Exception at run slice level % 52.58/8.04 User error: GNN currently only supports monomorphic FOL. % 52.58/8.04 % Exception at run slice level % 52.58/8.04 User error: GNN currently only supports monomorphic FOL. % 52.58/8.04 % (3410369)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2198816648:i=30753:av=off:ss=included_2953 on theBenchmark for (2953ds/30753Mi) % 52.58/8.04 % Exception at run slice level % 52.58/8.04 User error: GNN currently only supports monomorphic FOL. % 60.76/9.25 % (3410371)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=2640422854:cts=off:i=2759:kws=inv_arity:fgj=on_2952 on theBenchmark for (2952ds/2759Mi) % 60.76/9.25 % (3410370)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=1794267284:i=26473:ep=RSTC_2952 on theBenchmark for (2952ds/26473Mi) % 60.76/9.25 % (3410373)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=3156654046:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2952 on theBenchmark for (2952ds/5665Mi) % 60.76/9.25 % (3410373)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 60.76/9.25 % Exception at run slice level % 60.76/9.25 User error: GNN currently only supports monomorphic FOL. % 60.76/9.25 % (3410377)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=1473977701:i=1532:ep=RS:ss=axioms_2949 on theBenchmark for (2949ds/1532Mi) % 60.76/9.25 % Exception at run slice level % 60.76/9.25 User error: GNN currently only supports monomorphic FOL. % 60.76/9.25 % (3410379)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=878415276:i=1565:sd=2:ss=axioms:sgt=32_2948 on theBenchmark for (2948ds/1565Mi) % 60.76/9.25 % Exception at run slice level % 60.76/9.25 User error: GNN currently only supports monomorphic FOL. % 60.76/9.25 % (3410320)Instruction limit reached! % 60.76/9.25 % (3410320)------------------------------ % 60.76/9.25 % (3410320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.76/9.25 % (3410320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.76/9.25 % (3410320)CaDiCaL version: 2.1.3 % 60.76/9.25 % (3410320)Termination reason: Instruction limit % 60.76/9.25 % (3410320)Termination phase: Saturation % 60.76/9.25 % (3410320)Time elapsed: 2.986 s % 60.76/9.25 % (3410320)Peak memory usage: 120 MB % 60.76/9.25 % (3410320)Instructions burned: 5781 (million) % 60.76/9.25 % Exception at run slice level % 60.76/9.25 User error: GNN currently only supports monomorphic FOL. % 60.76/9.25 % (3410381)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=3012149464:i=1572:fgj=on:gsp=on_2947 on theBenchmark for (2947ds/1572Mi) % 60.76/9.25 % (3410381)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 60.76/9.25 % (3410383)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=2102661728:i=3500:sd=1:bd=preordered:sup=off:ss=included_2946 on theBenchmark for (2946ds/3500Mi) % 60.76/9.25 % (3410382)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=783646564:i=6052:sd=4:ss=axioms:sgt=24_2947 on theBenchmark for (2947ds/6052Mi) % 60.76/9.25 % Exception at run slice level % 60.76/9.25 User error: GNN currently only supports monomorphic FOL. % 60.76/9.25 % Exception at run slice level % 60.76/9.25 User error: GNN currently only supports monomorphic FOL. % 60.76/9.25 % (3410387)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=401959982:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2944 on theBenchmark for (2944ds/1842Mi) % 60.76/9.25 % (3410387)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 60.76/9.25 % (3410388)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=4239880568:i=66096:add=on_2943 on theBenchmark for (2943ds/66096Mi) % 60.76/9.25 % Exception at run slice level % 60.76/9.25 User error: GNN currently only supports monomorphic FOL. % 60.76/9.25 % Exception at run slice level % 60.76/9.25 User error: GNN currently only supports monomorphic FOL. % 60.76/9.25 % Exception at run slice level % 60.76/9.25 User error: GNN currently only supports monomorphic FOL. % 60.76/9.25 % (3410391)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=209262011:i=1884:sd=1:nm=60:ss=axioms_2942 on theBenchmark for (2942ds/1884Mi) % 60.76/9.25 % (3410392)lrs-1011_4:1_sil=16000:bsr=on:random_seed=409833474:cts=off:i=5469:bs=on:fsr=off_2942 on theBenchmark for (2942ds/5469Mi) % 71.51/10.83 % (3410393)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=2628057262:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2941 on theBenchmark for (2941ds/2037Mi) % 71.51/10.83 % Exception at run slice level % 71.51/10.83 User error: GNN currently only supports monomorphic FOL. % 71.51/10.83 % Exception at run slice level % 71.51/10.83 User error: GNN currently only supports monomorphic FOL. % 71.51/10.83 % (3410397)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=737661998:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2939 on theBenchmark for (2939ds/2110Mi) % 71.51/10.83 % (3410398)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=1250366764:i=2430:add=off:aac=none:nm=16_2938 on theBenchmark for (2938ds/2430Mi) % 71.51/10.83 % Exception at run slice level % 71.51/10.83 User error: GNN currently only supports monomorphic FOL. % 71.51/10.83 % (3410401)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=2227352353:cond=fast:i=4891_2937 on theBenchmark for (2937ds/4891Mi) % 71.51/10.83 % Exception at run slice level % 71.51/10.83 User error: GNN currently only supports monomorphic FOL. % 71.51/10.83 % (3410403)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=1201418634:st=2:i=14845:sd=2:ss=included:fsd=on_2935 on theBenchmark for (2935ds/14845Mi) % 71.51/10.83 % Exception at run slice level % 71.51/10.83 User error: GNN currently only supports monomorphic FOL. % 71.51/10.83 % (3410405)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=2402605545:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2934 on theBenchmark for (2934ds/7534Mi) % 71.51/10.83 % Exception at run slice level % 71.51/10.83 User error: GNN currently only supports monomorphic FOL. % 71.51/10.83 % Exception at run slice level % 71.51/10.83 User error: GNN currently only supports monomorphic FOL. % 71.51/10.83 % (3410407)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=1802992505:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2932 on theBenchmark for (2932ds/10353Mi) % 71.51/10.83 % (3410408)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3953620866:i=7860_2932 on theBenchmark for (2932ds/7860Mi) % 71.51/10.83 % (3410408)Refutation not found, incomplete strategy % 71.51/10.83 % (3410408)------------------------------ % 71.51/10.83 % (3410408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.51/10.83 % (3410408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.51/10.83 % (3410408)CaDiCaL version: 2.1.3 % 71.51/10.83 % (3410408)Termination reason: Refutation not found, incomplete strategy % 71.51/10.83 % (3410408)Time elapsed: 0.011 s % 71.51/10.83 % (3410408)Peak memory usage: 89 MB % 71.51/10.83 % (3410408)Instructions burned: 19 (million) % 71.51/10.83 % Exception at run slice level % 71.51/10.83 User error: GNN currently only supports monomorphic FOL. % 71.51/10.83 % Exception at run slice level % 71.51/10.83 User error: GNN currently only supports monomorphic FOL. % 71.51/10.83 % (3410411)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=136175925:i=7896:sd=2:bs=on:ss=included:sgt=20_2930 on theBenchmark for (2930ds/7896Mi) % 71.51/10.83 % (3410408)------------------------------ % 71.51/10.83 % (3410408)------------------------------ % 71.51/10.83 % (3410412)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1917623357:i=5812:gtgl=2:gtg=all_2929 on theBenchmark for (2929ds/5812Mi) % 71.51/10.83 % (3410414)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=2707362136:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2928 on theBenchmark for (2928ds/2965Mi) % 71.51/10.83 % Exception at run slice level % 71.51/10.83 User error: GNN currently only supports monomorphic FOL. % 71.51/10.83 % (3410417)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=2904544036:i=2967:kws=precedence:bd=preordered:av=off_2927 on theBenchmark for (2927ds/2967Mi) % 106.10/15.66 % (3410356)Instruction limit reached! % 106.10/15.66 % (3410356)------------------------------ % 106.10/15.66 % (3410356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.10/15.66 % (3410356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.10/15.66 % (3410356)CaDiCaL version: 2.1.3 % 106.10/15.66 % (3410356)Termination reason: Instruction limit % 106.10/15.66 % (3410356)Termination phase: Saturation % 106.10/15.66 % (3410356)Time elapsed: 3.256 s % 106.10/15.66 % (3410356)Peak memory usage: 118 MB % 106.10/15.66 % (3410356)Instructions burned: 6226 (million) % 106.10/15.66 % Exception at run slice level % 106.10/15.66 User error: GNN currently only supports monomorphic FOL. % 106.10/15.66 % Exception at run slice level % 106.10/15.66 User error: GNN currently only supports monomorphic FOL. % 106.10/15.66 % Exception at run slice level % 106.10/15.66 User error: GNN currently only supports monomorphic FOL. % 106.10/15.66 % (3410419)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=260690829:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2925 on theBenchmark for (2925ds/3022Mi) % 106.10/15.66 % (3410420)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=2903144532:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2924 on theBenchmark for (2924ds/3207Mi) % 106.10/15.66 % (3410421)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=3040845056:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2924 on theBenchmark for (2924ds/3289Mi) % 106.10/15.66 % (3410422)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=2041873775:i=38569:sd=3:ss=axioms:sgt=32_2923 on theBenchmark for (2923ds/38569Mi) % 106.10/15.66 % Exception at run slice level % 106.10/15.66 User error: GNN currently only supports monomorphic FOL. % 106.10/15.66 % (3410427)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=436381866:cts=off:i=3394_2921 on theBenchmark for (2921ds/3394Mi) % 106.10/15.66 % Exception at run slice level % 106.10/15.66 User error: GNN currently only supports monomorphic FOL. % 106.10/15.66 % Exception at run slice level % 106.10/15.66 User error: GNN currently only supports monomorphic FOL. % 106.10/15.66 % Exception at run slice level % 106.10/15.66 User error: GNN currently only supports monomorphic FOL. % 106.10/15.66 % (3410429)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=3641352980:i=33824:bd=preordered_2920 on theBenchmark for (2920ds/33824Mi) % 106.10/15.66 % Exception at run slice level % 106.10/15.66 User error: GNN currently only supports monomorphic FOL. % 106.10/15.66 % (3410430)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=1159469030:i=20684:bd=all:gtg=exists_sym_2919 on theBenchmark for (2919ds/20684Mi) % 106.10/15.66 % (3410432)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=3819827313: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_2918 on theBenchmark for (2918ds/7222Mi) % 106.10/15.66 % (3410432)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 106.10/15.66 % (3410433)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=307494357:st=4:i=7295:sd=4:ep=R:ss=axioms_2918 on theBenchmark for (2918ds/7295Mi) % 106.10/15.66 % Exception at run slice level % 106.10/15.66 User error: GNN currently only supports monomorphic FOL. % 106.10/15.66 % Exception at run slice level % 106.10/15.66 User error: GNN currently only supports monomorphic FOL. % 106.10/15.66 % Exception at run slice level % 106.10/15.66 User error: GNN currently only supports monomorphic FOL. % 106.10/15.66 % (3410438)lrs+10_1_sil=128000:lcm=predicate:random_seed=848919606:st=3:i=43697:sd=5:ss=axioms_2915 on theBenchmark for (2915ds/43697Mi) % 106.10/15.66 % (3410437)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=1386803289:i=4036:ins=10_2915 on theBenchmark for (2915ds/4036Mi) % 135.07/19.70 % Exception at run slice level % 135.07/19.70 User error: GNN currently only supports monomorphic FOL. % 135.07/19.70 % (3410439)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=3573801246:i=17599:gtg=all:ss=axioms:fsd=on_2914 on theBenchmark for (2914ds/17599Mi) % 135.07/19.70 % (3410442)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=3200646971:i=4547:bd=preordered_2914 on theBenchmark for (2914ds/4547Mi) % 135.07/19.70 % Exception at run slice level % 135.07/19.70 User error: GNN currently only supports monomorphic FOL. % 135.07/19.70 % Exception at run slice level % 135.07/19.70 User error: GNN currently only supports monomorphic FOL. % 135.07/19.70 % Exception at run slice level % 135.07/19.70 User error: GNN currently only supports monomorphic FOL. % 135.07/19.70 % (3410445)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=3413917759:i=9294:av=off_2910 on theBenchmark for (2910ds/9294Mi) % 135.07/19.70 % (3410446)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3512770111:i=32849:add=on_2909 on theBenchmark for (2909ds/32849Mi) % 135.07/19.70 % (3410448)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1477778397:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2909 on theBenchmark for (2909ds/4793Mi) % 135.07/19.70 % (3410392)Instruction limit reached! % 135.07/19.70 % (3410392)------------------------------ % 135.07/19.70 % (3410392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.07/19.70 % (3410392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.07/19.70 % (3410392)CaDiCaL version: 2.1.3 % 135.07/19.70 % (3410392)Termination reason: Instruction limit % 135.07/19.70 % (3410392)Termination phase: Saturation % 135.07/19.70 % (3410392)Time elapsed: 3.403 s % 135.07/19.70 % (3410392)Peak memory usage: 117 MB % 135.07/19.70 % (3410392)Instructions burned: 5469 (million) % 135.07/19.70 % (3410451)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=167056451:i=4840:nm=4:av=off_2906 on theBenchmark for (2906ds/4840Mi) % 135.07/19.70 % Exception at run slice level % 135.07/19.70 User error: GNN currently only supports monomorphic FOL. % 135.07/19.70 % Exception at run slice level % 135.07/19.70 User error: GNN currently only supports monomorphic FOL. % 135.07/19.70 % Exception at run slice level % 135.07/19.70 User error: GNN currently only supports monomorphic FOL. % 135.07/19.70 % (3410453)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=251707250:cts=off:i=5002_2905 on theBenchmark for (2905ds/5002Mi) % 135.07/19.70 % (3410454)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=1956548134:i=30479:sd=3:ss=axioms_2904 on theBenchmark for (2904ds/30479Mi) % 135.07/19.70 % (3410456)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=560605693:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2904 on theBenchmark for (2904ds/11035Mi) % 135.07/19.70 % (3410456)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 135.07/19.70 % Exception at run slice level % 135.07/19.70 User error: GNN currently only supports monomorphic FOL. % 135.07/19.70 % (3410459)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=3275188776:i=5835_2902 on theBenchmark for (2902ds/5835Mi) % 135.07/19.70 % Exception at run slice level % 135.07/19.70 User error: GNN currently only supports monomorphic FOL. % 135.07/19.70 % Exception at run slice level % 135.07/19.70 User error: GNN currently only supports monomorphic FOL. % 135.07/19.70 % Exception at run slice level % 135.07/19.70 User error: GNN currently only supports monomorphic FOL. % 135.07/19.70 % (3410461)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=1054006282:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2900 on theBenchmark for (2900ds/5890Mi) % 135.07/19.70 % (3410462)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=3650465733:cts=off:i=19910:ep=RS_2899 on theBenchmark for (2899ds/19910Mi) % 153.77/22.36 % (3410464)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=3186823364:i=20312:bd=preordered:fsr=off:er=filter_2899 on theBenchmark for (2899ds/20312Mi) % 153.77/22.36 % Exception at run slice level % 153.77/22.36 User error: GNN currently only supports monomorphic FOL. % 153.77/22.36 % (3410467)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=3653369976:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2897 on theBenchmark for (2897ds/13822Mi) % 153.77/22.36 % Exception at run slice level % 153.77/22.36 User error: GNN currently only supports monomorphic FOL. % 153.77/22.36 % (3410469)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=884513034:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2895 on theBenchmark for (2895ds/7144Mi) % 153.77/22.36 % Exception at run slice level % 153.77/22.36 User error: GNN currently only supports monomorphic FOL. % 153.77/22.36 % (3410471)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=976703361:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2894 on theBenchmark for (2894ds/15184Mi) % 153.77/22.36 % Exception at run slice level % 153.77/22.36 User error: GNN currently only supports monomorphic FOL. % 153.77/22.36 % (3410473)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=1861756711:i=107375_2892 on theBenchmark for (2892ds/107375Mi) % 153.77/22.36 % Exception at run slice level % 153.77/22.36 User error: GNN currently only supports monomorphic FOL. % 153.77/22.36 % (3410475)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=670563011:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2889 on theBenchmark for (2889ds/7958Mi) % 153.77/22.36 % Exception at run slice level % 153.77/22.36 User error: GNN currently only supports monomorphic FOL. % 153.77/22.36 % (3410477)dis+10_128_sil=16000:nwc=0.7:random_seed=2527011356:i=15999:nm=2:gsp=on_2887 on theBenchmark for (2887ds/15999Mi) % 153.77/22.36 % (3410477)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 153.77/22.36 % Exception at run slice level % 153.77/22.36 User error: GNN currently only supports monomorphic FOL. % 153.77/22.36 % (3410479)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=1543464653:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2884 on theBenchmark for (2884ds/8139Mi) % 153.77/22.36 % (3410469)Instruction limit reached! % 153.77/22.36 % (3410469)------------------------------ % 153.77/22.36 % (3410469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.77/22.36 % (3410469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.77/22.36 % (3410469)CaDiCaL version: 2.1.3 % 153.77/22.36 % (3410469)Termination reason: Instruction limit % 153.77/22.36 % (3410469)Termination phase: Saturation % 153.77/22.36 % (3410469)Time elapsed: 3.759 s % 153.77/22.36 % (3410469)Peak memory usage: 99 MB % 153.77/22.36 % (3410469)Instructions burned: 7144 (million) % 153.77/22.36 % (3410727)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=3410836862:st=4:i=8950:sd=5:ss=axioms_2856 on theBenchmark for (2856ds/8950Mi) % 153.77/22.36 % Exception at run slice level % 153.77/22.36 User error: GNN currently only supports monomorphic FOL. % 153.77/22.36 % (3410479)Instruction limit reached! % 153.77/22.36 % (3410479)------------------------------ % 153.77/22.36 % (3410479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.77/22.36 % (3410479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.77/22.36 % (3410479)CaDiCaL version: 2.1.3 % 153.77/22.36 % (3410479)Termination reason: Instruction limit % 153.77/22.36 % (3410479)Termination phase: Saturation % 153.77/22.36 % (3410479)Time elapsed: 3.190 s % 153.77/22.36 % (3410479)Peak memory usage: 90 MB % 153.77/22.36 % (3410479)Instructions burned: 8139 (million) % 153.77/22.36 % (3410737)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=750983662:i=9809:ins=10:av=off_2852 on theBenchmark for (2852ds/9809Mi) % 166.84/24.19 % (3410738)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=1008405912:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2851 on theBenchmark for (2851ds/9885Mi) % 166.84/24.19 % Exception at run slice level % 166.84/24.19 User error: % Exception at run slice levelGNN currently only supports monomorphic FOL. % 166.84/24.19 % 166.84/24.19 User error: GNN currently only supports monomorphic FOL. % 166.84/24.19 % (3410749)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=1714177178:cond=fast:i=32078:fgj=on:av=off_2845 on theBenchmark for (2845ds/32078Mi) % 166.84/24.19 % (3410750)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=3007966801:i=11101:bd=all:ss=axioms:sgt=8_2845 on theBenchmark for (2845ds/11101Mi) % 166.84/24.19 % Exception at run slice level % 166.84/24.19 User error: GNN currently only supports monomorphic FOL. % 166.84/24.19 % (3410854)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=3459126910:cond=on:i=13220:s2at=3:aac=none:fsd=on_2840 on theBenchmark for (2840ds/13220Mi) % 166.84/24.19 % Exception at run slice level % 166.84/24.19 User error: GNN currently only supports monomorphic FOL. % 166.84/24.19 % (3410908)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=3495439304:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2835 on theBenchmark for (2835ds/13528Mi) % 166.84/24.19 % Exception at run slice level % 166.84/24.19 User error: GNN currently only supports monomorphic FOL. % 166.84/24.19 % (3410910)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=564947068:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2830 on theBenchmark for (2830ds/14854Mi) % 166.84/24.19 % Exception at run slice level % 166.84/24.19 User error: GNN currently only supports monomorphic FOL. % 166.84/24.19 % (3410912)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=2762623014:i=14974:ss=axioms:sgt=16_2825 on theBenchmark for (2825ds/14974Mi) % 166.84/24.19 % Exception at run slice level % 166.84/24.19 User error: GNN currently only supports monomorphic FOL. % 166.84/24.19 % (3410914)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=1422285350:i=33081:aac=none:fgj=on:bd=all:fsr=off_2820 on theBenchmark for (2820ds/33081Mi) % 166.84/24.19 % Exception at run slice level % 166.84/24.19 User error: GNN currently only supports monomorphic FOL. % 166.84/24.19 % (3410916)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=2502932607:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2815 on theBenchmark for (2815ds/50856Mi) % 166.84/24.19 % (3410370)Instruction limit reached! % 166.84/24.19 % (3410370)------------------------------ % 166.84/24.19 % (3410370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 166.84/24.19 % (3410370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.84/24.19 % (3410370)CaDiCaL version: 2.1.3 % 166.84/24.19 % (3410370)Termination reason: Instruction limit % 166.84/24.19 % (3410370)Termination phase: Saturation % 166.84/24.19 % (3410370)Time elapsed: 13.959 s % 166.84/24.19 % (3410370)Peak memory usage: 220 MB % 166.84/24.19 % (3410370)Instructions burned: 26474 (million) % 166.84/24.19 % Exception at run slice level % 166.84/24.19 User error: GNN currently only supports monomorphic FOL. % 166.84/24.19 % (3410918)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=976822217:i=69865_2811 on theBenchmark for (2811ds/69865Mi) % 166.84/24.19 % (3410477)Instruction limit reached! % 166.84/24.19 % (3410477)------------------------------ % 166.84/24.19 % (3410477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 166.84/24.19 % (3410477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.84/24.19 % (3410477)CaDiCaL version: 2.1.3 % 166.84/24.19 % (3410477)Termination reason: Instruction limit % 166.84/24.19 % (3410477)Termination phase: Saturation % 166.84/24.19 % (3410477)Time elapsed: 7.623 s % 166.84/24.19 % (3410477)Peak memory usage: 113 MB % 166.84/24.19 % (3410477)Instructions burned: 15999 (million) % 166.84/24.19 % (3410919)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=234625209:cond=fast:i=17802:gtgl=3:gtg=all_2810 on theBenchmark for (2810ds/17802Mi) % 176.07/25.50 % Exception at run slice level % 176.07/25.50 User error: Immediate (shared) subterms of term/literal huffma107959123e_case(X1,X0,X6,X5,huffma1146269203erNode(X1,X4,X3,X2)) = sF48(X1,X0,X6,X5,X4,X3,X2) have different types/not well-typed! % 176.07/25.50 % (3410921)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=226262751:i=96644_2809 on theBenchmark for (2809ds/96644Mi) % 176.07/25.50 % (3410923)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 176.07/25.50 % (3410923)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=3162965629:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2809 on theBenchmark for (2809ds/21161Mi) % 176.07/25.50 % Exception at run slice level % 176.07/25.50 User error: GNN currently only supports monomorphic FOL. % 176.07/25.50 % (3410926)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=2104617374:i=22761:gtg=all:ss=axioms:fsd=on_2806 on theBenchmark for (2806ds/22761Mi) % 176.07/25.50 % Exception at run slice level % 176.07/25.50 User error: GNN currently only supports monomorphic FOL. % 176.07/25.50 % (3410928)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=4163600894:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2801 on theBenchmark for (2801ds/23713Mi) % 176.07/25.50 % (3410343)Instruction limit reached! % 176.07/25.50 % (3410343)------------------------------ % 176.07/25.50 % (3410343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.07/25.50 % (3410343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.07/25.50 % (3410343)CaDiCaL version: 2.1.3 % 176.07/25.50 % (3410343)Termination reason: Instruction limit % 176.07/25.50 % (3410343)Termination phase: Saturation % 176.07/25.50 % (3410343)Time elapsed: 17.038 s % 176.07/25.50 % (3410343)Peak memory usage: 156 MB % 176.07/25.50 % (3410343)Instructions burned: 33335 (million) % 176.07/25.50 % (3410930)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=2877120510:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2796 on theBenchmark for (2796ds/26509Mi) % 176.07/25.50 % Exception at run slice level % 176.07/25.50 User error: GNN currently only supports monomorphic FOL. % 176.07/25.50 % (3410932)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=3127907127:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2791 on theBenchmark for (2791ds/28957Mi) % 176.07/25.50 % (3410750)Instruction limit reached! % 176.07/25.50 % (3410750)------------------------------ % 176.07/25.50 % (3410750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.07/25.50 % (3410750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.07/25.50 % (3410750)CaDiCaL version: 2.1.3 % 176.07/25.50 % (3410750)Termination reason: Instruction limit % 176.07/25.50 % (3410750)Termination phase: Saturation % 176.07/25.50 % (3410750)Time elapsed: 5.630 s % 176.07/25.50 % (3410750)Peak memory usage: 129 MB % 176.07/25.50 % (3410750)Instructions burned: 11103 (million) % 176.07/25.50 % (3410934)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=1740678529:i=29246:s2at=-1:kws=inv_arity:ins=10_2787 on theBenchmark for (2787ds/29246Mi) % 176.07/25.50 % (3410462)Instruction limit reached! % 176.07/25.50 % (3410462)------------------------------ % 176.07/25.50 % (3410462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.07/25.50 % (3410462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.07/25.50 % (3410462)CaDiCaL version: 2.1.3 % 176.07/25.50 % (3410462)Termination reason: Instruction limit % 176.07/25.50 % (3410462)Termination phase: Saturation % 176.07/25.50 % (3410462)Time elapsed: 11.369 s % 176.07/25.50 % (3410462)Peak memory usage: 195 MB % 176.07/25.50 % (3410462)Instructions burned: 19912 (million) % 176.07/25.50 % (3410936)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=2580086442:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2784 on theBenchmark for (2784ds/30082Mi) % 181.98/26.32 % Exception at run slice level % 181.98/26.32 User error: GNN currently only supports monomorphic FOL. % 181.98/26.32 % (3410936)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 181.98/26.32 % (3410938)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=244728121:i=32262:bd=preordered_2783 on theBenchmark for (2783ds/32262Mi) % 181.98/26.32 % (3410438)Instruction limit reached! % 181.98/26.32 % (3410438)------------------------------ % 181.98/26.32 % (3410438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.98/26.32 % (3410438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.98/26.32 % (3410438)CaDiCaL version: 2.1.3 % 181.98/26.32 % (3410438)Termination reason: Instruction limit % 181.98/26.32 % (3410438)Termination phase: Saturation % 181.98/26.32 % (3410438)Time elapsed: 13.442 s % 181.98/26.32 % (3410438)Peak memory usage: 246 MB % 181.98/26.32 % (3410438)Instructions burned: 43698 (million) % 181.98/26.32 % Exception at run slice level % 181.98/26.32 User error: GNN currently only supports monomorphic FOL. % 181.98/26.32 % (3410940)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=163577007:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2779 on theBenchmark for (2779ds/32870Mi) % 181.98/26.32 % (3410941)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=3957251658:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2779 on theBenchmark for (2779ds/33295Mi) % 181.98/26.32 % Exception at run slice level % 181.98/26.32 User error: GNN currently only supports monomorphic FOL. % 181.98/26.32 % Exception at run slice level % 181.98/26.32 User error: GNN currently only supports monomorphic FOL. % 181.98/26.32 % (3410944)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=1592142385:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2777 on theBenchmark for (2777ds/36826Mi) % 181.98/26.32 % (3410945)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=1572233385:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2776 on theBenchmark for (2776ds/92981Mi) % 181.98/26.32 % Exception at run slice level % 181.98/26.32 User error: GNN currently only supports monomorphic FOL. % 181.98/26.32 % Exception at run slice level % 181.98/26.32 User error: GNN currently only supports monomorphic FOL. % 181.98/26.32 % (3410948)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=1291635699:s2pl=on:i=49423_2774 on theBenchmark for (2774ds/49423Mi) % 181.98/26.32 % (3410949)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=2267932835:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2773 on theBenchmark for (2773ds/57299Mi) % 181.98/26.32 % Exception at run slice level % 181.98/26.32 User error: GNN currently only supports monomorphic FOL. % 181.98/26.32 % (3410952)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=696039204:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2770 on theBenchmark for (2770ds/127679Mi) % 181.98/26.32 % Exception at run slice level % 181.98/26.32 User error: GNN currently only supports monomorphic FOL. % 181.98/26.32 % (3410954)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=1262125583:i=69402:add=on:aac=none:fsr=off_2769 on theBenchmark for (2769ds/69402Mi) % 181.98/26.32 % Exception at run slice level % 181.98/26.32 User error: GNN currently only supports monomorphic FOL. % 181.98/26.32 % (3410956)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=1389599109:i=100512:doe=on:fgj=on:bd=all:fsd=on_2768 on theBenchmark for (2768ds/100512Mi) % 181.98/26.32 % Exception at run slice level % 181.98/26.32 User error: GNN currently only supports monomorphic FOL. % 181.98/26.32 % Exception at run slice level % 181.98/26.32 User error: GNN currently only supports monomorphic FOL. % 189.63/27.42 % (3410958)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=455458279:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2765 on theBenchmark for (2765ds/138761Mi) % 189.63/27.42 % (3410959)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=3396193974:i=282386:rtra=on_2764 on theBenchmark for (2764ds/282386Mi) % 189.63/27.42 % Exception at run slice level % 189.63/27.42 User error: GNN currently only supports monomorphic FOL. % 189.63/27.42 % (3410962)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=1253317679:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2762 on theBenchmark for (2762ds/269354Mi) % 189.63/27.42 % Exception at run slice level % 189.63/27.42 User error: GNN currently only supports monomorphic FOL. % 189.63/27.42 % Exception at run slice level % 189.63/27.42 User error: GNN currently only supports monomorphic FOL. % 189.63/27.42 % (3410965)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=3881544648:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2759 on theBenchmark for (2759ds/218Mi) % 189.63/27.42 % (3410965)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 189.63/27.42 % (3410965)Refutation not found, incomplete strategy % 189.63/27.42 % (3410965)------------------------------ % 189.63/27.42 % (3410965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.63/27.42 % (3410965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.63/27.42 % (3410965)CaDiCaL version: 2.1.3 % 189.63/27.42 % (3410965)Termination reason: Refutation not found, incomplete strategy % 189.63/27.42 % (3410965)Time elapsed: 0.004 s % 189.63/27.42 % (3410965)Peak memory usage: 89 MB % 189.63/27.42 % (3410965)Instructions burned: 14 (million) % 189.63/27.42 % (3410964)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=3168190959:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2759 on theBenchmark for (2759ds/283390Mi) % 189.63/27.42 % (3410964)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 189.63/27.42 % (3410965)------------------------------ % 189.63/27.42 % (3410965)------------------------------ % 189.63/27.42 % (3410968)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=414623717:i=238:av=off:rtra=on:ss=axioms_2757 on theBenchmark for (2757ds/238Mi) % 189.63/27.42 % (3410968)Instruction limit reached! % 189.63/27.42 % (3410968)------------------------------ % 189.63/27.42 % (3410968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.63/27.42 % (3410968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.63/27.42 % (3410968)CaDiCaL version: 2.1.3 % 189.63/27.42 % (3410968)Termination reason: Instruction limit % 189.63/27.42 % (3410968)Termination phase: Saturation % 189.63/27.42 % (3410968)Time elapsed: 0.067 s % 189.63/27.42 % (3410968)Peak memory usage: 89 MB % 189.63/27.42 % (3410968)Instructions burned: 243 (million) % 189.63/27.42 % (3410970)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=1997641173:s2a=on:i=278:rtra=on:gtg=position_2755 on theBenchmark for (2755ds/278Mi) % 189.63/27.42 % Exception at run slice level % 189.63/27.42 User error: GNN currently only supports monomorphic FOL. % 189.63/27.42 % (3410970)Instruction limit reached! % 189.63/27.42 % (3410970)------------------------------ % 189.63/27.42 % (3410970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.63/27.42 % (3410970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.63/27.42 % (3410970)CaDiCaL version: 2.1.3 % 189.63/27.42 % (3410970)Termination reason: Instruction limit % 189.63/27.42 % (3410970)Termination phase: Saturation % 189.63/27.42 % (3410970)Time elapsed: 0.095 s % 189.63/27.42 % (3410970)Peak memory usage: 91 MB % 189.63/27.42 % (3410970)Instructions burned: 278 (million) % 189.63/27.42 % (3410972)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=2504782297:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2754 on theBenchmark for (2754ds/258Mi) % 189.63/27.42 % (3410973)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=668772582:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2753 on theBenchmark for (2753ds/570Mi) % 189.63/27.42 % (3410972)Instruction limit reached! % 197.47/28.56 % (3410972)------------------------------ % 197.47/28.56 % (3410972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.47/28.56 % (3410972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.47/28.56 % (3410972)CaDiCaL version: 2.1.3 % 197.47/28.56 % (3410972)Termination reason: Instruction limit % 197.47/28.56 % (3410972)Termination phase: Saturation % 197.47/28.56 % (3410972)Time elapsed: 0.155 s % 197.47/28.56 % (3410972)Peak memory usage: 91 MB % 197.47/28.56 % (3410972)Instructions burned: 259 (million) % 197.47/28.56 % (3410973)Instruction limit reached! % 197.47/28.56 % (3410973)------------------------------ % 197.47/28.56 % (3410973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.47/28.56 % (3410973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.47/28.56 % (3410973)CaDiCaL version: 2.1.3 % 197.47/28.56 % (3410973)Termination reason: Instruction limit % 197.47/28.56 % (3410973)Termination phase: Saturation % 197.47/28.56 % (3410973)Time elapsed: 0.175 s % 197.47/28.56 % (3410973)Peak memory usage: 92 MB % 197.47/28.56 % (3410973)Instructions burned: 571 (million) % 197.47/28.56 % (3410976)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=4024222524:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2751 on theBenchmark for (2751ds/314Mi) % 197.47/28.56 % (3410977)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=3001413786:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2750 on theBenchmark for (2750ds/650Mi) % 197.47/28.56 % (3410976)Instruction limit reached! % 197.47/28.56 % (3410976)------------------------------ % 197.47/28.56 % (3410976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.47/28.56 % (3410976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.47/28.56 % (3410976)CaDiCaL version: 2.1.3 % 197.47/28.56 % (3410976)Termination reason: Instruction limit % 197.47/28.56 % (3410976)Termination phase: Saturation % 197.47/28.56 % (3410976)Time elapsed: 0.167 s % 197.47/28.56 % (3410976)Peak memory usage: 90 MB % 197.47/28.56 % (3410976)Instructions burned: 315 (million) % 197.47/28.56 % (3410977)Instruction limit reached! % 197.47/28.56 % (3410977)------------------------------ % 197.47/28.56 % (3410977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.47/28.56 % (3410977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.47/28.56 % (3410977)CaDiCaL version: 2.1.3 % 197.47/28.56 % (3410977)Termination reason: Instruction limit % 197.47/28.56 % (3410977)Termination phase: Saturation % 197.47/28.56 % (3410977)Time elapsed: 0.200 s % 197.47/28.56 % (3410977)Peak memory usage: 93 MB % 197.47/28.56 % (3410977)Instructions burned: 653 (million) % 197.47/28.56 % (3410980)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=2486168220:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2748 on theBenchmark for (2748ds/496Mi) % 197.47/28.56 % (3410981)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=1756357270:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2748 on theBenchmark for (2748ds/588Mi) % 197.47/28.56 % (3410981)Instruction limit reached! % 197.47/28.56 % (3410981)------------------------------ % 197.47/28.56 % (3410981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.47/28.56 % (3410981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.47/28.56 % (3410981)CaDiCaL version: 2.1.3 % 197.47/28.56 % (3410981)Termination reason: Instruction limit % 197.47/28.56 % (3410981)Termination phase: Saturation % 197.47/28.56 % (3410981)Time elapsed: 0.173 s % 197.47/28.56 % (3410981)Peak memory usage: 91 MB % 197.47/28.56 % (3410981)Instructions burned: 589 (million) % 197.47/28.56 % (3410980)Instruction limit reached! % 197.47/28.56 % (3410980)------------------------------ % 197.47/28.56 % (3410980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.47/28.56 % (3410980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.47/28.56 % (3410980)CaDiCaL version: 2.1.3 % 197.47/28.56 % (3410980)Termination reason: Instruction limit % 197.47/28.56 % (3410980)Termination phase: Saturation % 197.47/28.56 % (3410980)Time elapsed: 0.249 s % 197.47/28.56 % (3410980)Peak memory usage: 92 MB % 197.47/28.56 % (3410980)Instructions burned: 498 (million) % 197.47/28.56 % (3410984)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=3908812669:i=4700:rtra=on_2745 on theBenchmark for (2745ds/4700Mi) % 197.47/28.56 % (3410985)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=639220705:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2744 on theBenchmark for (2744ds/226Mi) % 202.68/29.25 % Exception at run slice level % 202.68/29.25 User error: GNN currently only supports monomorphic FOL. % 202.68/29.25 % (3410985)Instruction limit reached! % 202.68/29.25 % (3410985)------------------------------ % 202.68/29.25 % (3410985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.68/29.25 % (3410985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.68/29.25 % (3410985)CaDiCaL version: 2.1.3 % 202.68/29.25 % (3410985)Termination reason: Instruction limit % 202.68/29.25 % (3410985)Termination phase: Saturation % 202.68/29.25 % (3410985)Time elapsed: 0.138 s % 202.68/29.25 % (3410985)Peak memory usage: 91 MB % 202.68/29.25 % (3410985)Instructions burned: 227 (million) % 202.68/29.25 % (3410988)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2684379667:i=254:av=off:fsr=off:rtra=on:sup=off_2742 on theBenchmark for (2742ds/254Mi) % 202.68/29.25 % (3410988)Instruction limit reached! % 202.68/29.25 % (3410988)------------------------------ % 202.68/29.25 % (3410988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.68/29.25 % (3410988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.68/29.25 % (3410988)CaDiCaL version: 2.1.3 % 202.68/29.25 % (3410988)Termination reason: Instruction limit % 202.68/29.25 % (3410988)Termination phase: Saturation % 202.68/29.25 % (3410988)Time elapsed: 0.060 s % 202.68/29.25 % (3410988)Peak memory usage: 89 MB % 202.68/29.25 % (3410988)Instructions burned: 255 (million) % 202.68/29.25 % (3410989)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=2811302634:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2742 on theBenchmark for (2742ds/228Mi) % 202.68/29.25 % (3410992)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=2977082804:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2740 on theBenchmark for (2740ds/1814Mi) % 202.68/29.25 % (3410989)Instruction limit reached! % 202.68/29.25 % (3410989)------------------------------ % 202.68/29.25 % (3410989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.68/29.25 % (3410989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.68/29.25 % (3410989)CaDiCaL version: 2.1.3 % 202.68/29.25 % (3410989)Termination reason: Instruction limit % 202.68/29.25 % (3410989)Termination phase: Saturation % 202.68/29.25 % (3410989)Time elapsed: 0.106 s % 202.68/29.25 % (3410989)Peak memory usage: 89 MB % 202.68/29.25 % (3410989)Instructions burned: 229 (million) % 202.68/29.25 % (3410994)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=3889564143:i=874:sd=1:aac=none:rtra=on:ss=included_2739 on theBenchmark for (2739ds/874Mi) % 202.68/29.25 % (3410994)Refutation not found, incomplete strategy % 202.68/29.25 % (3410994)------------------------------ % 202.68/29.25 % (3410994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.68/29.25 % (3410994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.68/29.25 % (3410994)CaDiCaL version: 2.1.3 % 202.68/29.25 % (3410994)Termination reason: Refutation not found, incomplete strategy % 202.68/29.25 % (3410994)Time elapsed: 0.056 s % 202.68/29.25 % (3410994)Peak memory usage: 90 MB % 202.68/29.25 % (3410994)Instructions burned: 99 (million) % 202.68/29.25 % (3410994)------------------------------ % 202.68/29.25 % (3410994)------------------------------ % 202.68/29.25 % (3410992)Instruction limit reached! % 202.68/29.25 % (3410992)------------------------------ % 202.68/29.25 % (3410992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.68/29.25 % (3410992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.68/29.25 % (3410992)CaDiCaL version: 2.1.3 % 202.68/29.25 % (3410992)Termination reason: Instruction limit % 202.68/29.25 % (3410992)Termination phase: Saturation % 202.68/29.25 % (3410992)Time elapsed: 0.566 s % 202.68/29.25 % (3410992)Peak memory usage: 98 MB % 202.68/29.25 % (3410992)Instructions burned: 1814 (million) % 202.68/29.25 % (3410996)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=2813045427:i=10404:rtra=on:ss=axioms:sgt=16_2735 on theBenchmark for (2735ds/10404Mi) % 202.68/29.25 % (3410997)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=339102882:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2734 on theBenchmark for (2734ds/268Mi) % 202.68/29.25 % (3410997)Instruction limit reached! % 202.68/29.25 % (3410997)------------------------------ % 202.68/29.25 % (3410997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.68/29.25 % (3410997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.98/32.07 % (3410997)CaDiCaL version: 2.1.3 % 222.98/32.07 % (3410997)Termination reason: Instruction limit % 222.98/32.07 % (3410997)Termination phase: Saturation % 222.98/32.07 % (3410997)Time elapsed: 0.083 s % 222.98/32.07 % (3410997)Peak memory usage: 91 MB % 222.98/32.07 % (3410997)Instructions burned: 268 (million) % 222.98/32.07 % (3411000)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=4229079678:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2732 on theBenchmark for (2732ds/1184Mi) % 222.98/32.07 % (3411000)Refutation not found, incomplete strategy % 222.98/32.07 % (3411000)------------------------------ % 222.98/32.07 % (3411000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 222.98/32.07 % (3411000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.98/32.07 % (3411000)CaDiCaL version: 2.1.3 % 222.98/32.07 % (3411000)Termination reason: Refutation not found, incomplete strategy % 222.98/32.07 % (3411000)Time elapsed: 0.006 s % 222.98/32.07 % (3411000)Peak memory usage: 89 MB % 222.98/32.07 % (3411000)Instructions burned: 19 (million) % 222.98/32.07 % Exception at run slice level % 222.98/32.07 User error: GNN currently only supports monomorphic FOL. % 222.98/32.07 % (3411000)------------------------------ % 222.98/32.07 % (3411000)------------------------------ % 222.98/32.07 % (3411003)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=1166732264:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2729 on theBenchmark for (2729ds/250Mi) % 222.98/32.07 % (3411003)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 222.98/32.07 % (3411002)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=1247397990:st=3:i=26386:sd=3:rtra=on:ss=axioms_2730 on theBenchmark for (2730ds/26386Mi) % 222.98/32.07 % (3411003)Instruction limit reached! % 222.98/32.07 % (3411003)------------------------------ % 222.98/32.07 % (3411003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 222.98/32.07 % (3411003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.98/32.07 % (3411003)CaDiCaL version: 2.1.3 % 222.98/32.07 % (3411003)Termination reason: Instruction limit % 222.98/32.07 % (3411003)Termination phase: Saturation % 222.98/32.07 % (3411003)Time elapsed: 0.074 s % 222.98/32.07 % (3411003)Peak memory usage: 91 MB % 222.98/32.07 % (3411003)Instructions burned: 251 (million) % 222.98/32.07 % (3411006)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=210786483:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2728 on theBenchmark for (2728ds/268Mi) % 222.98/32.07 % Exception at run slice level % 222.98/32.07 User error: Immediate (shared) subterms of term/literal aa1(X1,X0,combb(X2,X0,X1,X3,X4),X5) = sF28(X1,X0,X2,X3,X4,X5) have different types/not well-typed! % 222.98/32.07 % (3411008)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1779560068:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2727 on theBenchmark for (2727ds/282Mi) % 222.98/32.07 % (3411008)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 222.98/32.07 % (3411008)Refutation not found, incomplete strategy % 222.98/32.07 % (3411008)------------------------------ % 222.98/32.07 % (3411008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 222.98/32.07 % (3411008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.98/32.07 % (3411008)CaDiCaL version: 2.1.3 % 222.98/32.07 % (3411008)Termination reason: Refutation not found, incomplete strategy % 222.98/32.07 % (3411008)Time elapsed: 0.003 s % 222.98/32.07 % (3411008)Peak memory usage: 89 MB % 222.98/32.07 % (3411008)Instructions burned: 10 (million) % 222.98/32.07 % Exception at run slice level % 222.98/32.07 User error: GNN currently only supports monomorphic FOL. % 222.98/32.07 % (3411008)------------------------------ % 222.98/32.07 % (3411008)------------------------------ % 222.98/32.07 % (3411011)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=565364599:i=12120:aac=none:ins=25:rtra=on_2724 on theBenchmark for (2724ds/12120Mi) % 222.98/32.07 % (3411010)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=200079206:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2725 on theBenchmark for (2725ds/862Mi) % 222.98/32.07 % Exception at run slice level % 222.98/32.07 User error: GNN currently only supports monomorphic FOL. % 222.98/32.07 % (3411014)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=2935529694:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2722 on theBenchmark for (2722ds/300Mi) % 237.79/34.19 % (3411014)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 237.79/34.19 % (3411014)Instruction limit reached! % 237.79/34.19 % (3411014)------------------------------ % 237.79/34.19 % (3411014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.79/34.19 % (3411014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.79/34.19 % (3411014)CaDiCaL version: 2.1.3 % 237.79/34.19 % (3411014)Termination reason: Instruction limit % 237.79/34.19 % (3411014)Termination phase: Saturation % 237.79/34.19 % (3411014)Time elapsed: 0.099 s % 237.79/34.19 % (3411014)Peak memory usage: 90 MB % 237.79/34.19 % (3411014)Instructions burned: 302 (million) % 237.79/34.19 % (3411010)Instruction limit reached! % 237.79/34.19 % (3411010)------------------------------ % 237.79/34.19 % (3411010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.79/34.19 % (3411010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.79/34.19 % (3411010)CaDiCaL version: 2.1.3 % 237.79/34.19 % (3411010)Termination reason: Instruction limit % 237.79/34.19 % (3411010)Termination phase: Saturation % 237.79/34.19 % (3411010)Time elapsed: 0.440 s % 237.79/34.19 % (3411010)Peak memory usage: 95 MB % 237.79/34.19 % (3411010)Instructions burned: 862 (million) % 237.79/34.19 % (3411027)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=793617480:i=28310:bd=all:rtra=on_2720 on theBenchmark for (2720ds/28310Mi) % 237.79/34.19 % (3411047)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2576089498:i=1334:av=off:fsr=off:rtra=on_2719 on theBenchmark for (2719ds/1334Mi) % 237.79/34.19 % (3411047)Refutation not found, incomplete strategy % 237.79/34.19 % (3411047)------------------------------ % 237.79/34.19 % (3411047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.79/34.19 % (3411047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.79/34.19 % (3411047)CaDiCaL version: 2.1.3 % 237.79/34.19 % (3411047)Termination reason: Refutation not found, incomplete strategy % 237.79/34.19 % (3411047)Time elapsed: 0.018 s % 237.79/34.19 % (3411047)Peak memory usage: 89 MB % 237.79/34.19 % (3411047)Instructions burned: 37 (million) % 237.79/34.19 % Exception at run slice level % 237.79/34.19 User error: GNN currently only supports monomorphic FOL. % 237.79/34.19 % (3411136)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=1585605478:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2717 on theBenchmark for (2717ds/370Mi) % 237.79/34.19 % (3411047)------------------------------ % 237.79/34.19 % (3411047)------------------------------ % 237.79/34.19 % (3411136)Instruction limit reached! % 237.79/34.19 % (3411136)------------------------------ % 237.79/34.19 % (3411136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.79/34.19 % (3411136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.79/34.19 % (3411136)CaDiCaL version: 2.1.3 % 237.79/34.19 % (3411136)Termination reason: Instruction limit % 237.79/34.19 % (3411136)Termination phase: Saturation % 237.79/34.19 % (3411136)Time elapsed: 0.104 s % 237.79/34.19 % (3411136)Peak memory usage: 91 MB % 237.79/34.19 % (3411136)Instructions burned: 371 (million) % 237.79/34.19 % (3411139)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=2636189253:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2715 on theBenchmark for (2715ds/9700Mi) % 237.79/34.19 % (3411139)Refutation not found, incomplete strategy % 237.79/34.19 % (3411139)------------------------------ % 237.79/34.19 % (3411139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.79/34.19 % (3411139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.79/34.19 % (3411139)CaDiCaL version: 2.1.3 % 237.79/34.19 % (3411139)Termination reason: Refutation not found, incomplete strategy % 237.79/34.19 % (3411139)Time elapsed: 0.005 s % 237.79/34.19 % (3411139)Peak memory usage: 88 MB % 237.79/34.19 % (3411139)Instructions burned: 16 (million) % 237.79/34.19 % (3411138)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=3877630362:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2715 on theBenchmark for (2715ds/386Mi) % 265.39/38.13 % (3410928)Instruction limit reached! % 265.39/38.13 % (3410928)------------------------------ % 265.39/38.13 % (3410928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.39/38.13 % (3410928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.39/38.13 % (3410928)CaDiCaL version: 2.1.3 % 265.39/38.13 % (3410928)Termination reason: Instruction limit % 265.39/38.13 % (3410928)Termination phase: Saturation % 265.39/38.13 % (3410928)Time elapsed: 8.756 s % 265.39/38.13 % (3410928)Peak memory usage: 166 MB % 265.39/38.13 % (3410928)Instructions burned: 23716 (million) % 265.39/38.13 % (3411139)------------------------------ % 265.39/38.13 % (3411139)------------------------------ % 265.39/38.13 % (3411138)Instruction limit reached! % 265.39/38.13 % (3411138)------------------------------ % 265.39/38.13 % (3411138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.39/38.13 % (3411138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.39/38.13 % (3411138)CaDiCaL version: 2.1.3 % 265.39/38.13 % (3411138)Termination reason: Instruction limit % 265.39/38.13 % (3411138)Termination phase: Saturation % 265.39/38.13 % (3411138)Time elapsed: 0.192 s % 265.39/38.13 % (3411138)Peak memory usage: 91 MB % 265.39/38.13 % (3411138)Instructions burned: 386 (million) % 265.39/38.13 % (3411160)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=1643557258:i=24222:sd=1:rtra=on:ss=included_2712 on theBenchmark for (2712ds/24222Mi) % 265.39/38.13 % (3411164)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=3441213542:i=638:kws=precedence:fsr=off:rtra=on_2712 on theBenchmark for (2712ds/638Mi) % 265.39/38.13 % (3411186)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=4159309676:i=4128:ep=RST:rtra=on_2712 on theBenchmark for (2712ds/4128Mi) % 265.39/38.13 % (3411164)Instruction limit reached! % 265.39/38.13 % (3411164)------------------------------ % 265.39/38.13 % (3411164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.39/38.13 % (3411164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.39/38.13 % (3411164)CaDiCaL version: 2.1.3 % 265.39/38.13 % (3411164)Termination reason: Instruction limit % 265.39/38.13 % (3411164)Termination phase: Saturation % 265.39/38.13 % (3411164)Time elapsed: 0.218 s % 265.39/38.13 % (3411164)Peak memory usage: 91 MB % 265.39/38.13 % (3411164)Instructions burned: 642 (million) % 265.39/38.13 % (3411277)dis-1011_128_sil=32000:si=on:random_seed=1110206010:i=7412:ep=RST:av=off:rtra=on_2709 on theBenchmark for (2709ds/7412Mi) % 265.39/38.13 % Exception at run slice level % 265.39/38.13 User error: GNN currently only supports monomorphic FOL. % 265.39/38.13 % (3411305)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=144025760:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2707 on theBenchmark for (2707ds/1514Mi) % 265.39/38.13 % (3411305)Instruction limit reached! % 265.39/38.13 % (3411305)------------------------------ % 265.39/38.13 % (3411305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.39/38.13 % (3411305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.39/38.13 % (3411305)CaDiCaL version: 2.1.3 % 265.39/38.13 % (3411305)Termination reason: Instruction limit % 265.39/38.13 % (3411305)Termination phase: Saturation % 265.39/38.13 % (3411305)Time elapsed: 1.363 s % 265.39/38.13 % (3411305)Peak memory usage: 104 MB % 265.39/38.13 % (3411305)Instructions burned: 1515 (million) % 265.39/38.13 % (3411338)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=1732475070:i=27826:rtra=on:ss=axioms:sgt=8_2691 on theBenchmark for (2691ds/27826Mi) % 265.39/38.13 % (3410923)Instruction limit reached! % 265.39/38.13 % (3410923)------------------------------ % 265.39/38.13 % (3410923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.39/38.13 % (3410923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.39/38.13 % (3410923)CaDiCaL version: 2.1.3 % 265.39/38.13 % (3410923)Termination reason: Instruction limit % 265.39/38.13 % (3410923)Termination phase: Saturation % 265.39/38.13 % (3410923)Time elapsed: 11.976 s % 265.39/38.13 % (3410923)Peak memory usage: 182 MB % 265.39/38.13 % (3410923)Instructions burned: 21162 (million) % 265.39/38.13 % (3411342)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=3276022287:i=19850:aac=none:rtra=on_2688 on theBenchmark for (2688ds/19850Mi) % 294.76/42.23 % Exception at run slice level % 294.76/42.23 User error: GNN currently only supports monomorphic FOL. % 294.76/42.23 % (3411346)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2030536234:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2683 on theBenchmark for (2683ds/4958Mi) % 294.76/42.23 % (3411346)Refutation not found, incomplete strategy % 294.76/42.23 % (3411346)------------------------------ % 294.76/42.23 % (3411346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 294.76/42.23 % (3411346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.76/42.23 % (3411346)CaDiCaL version: 2.1.3 % 294.76/42.23 % (3411346)Termination reason: Refutation not found, incomplete strategy % 294.76/42.23 % (3411346)Time elapsed: 0.017 s % 294.76/42.23 % (3411346)Peak memory usage: 89 MB % 294.76/42.23 % (3411346)Instructions burned: 21 (million) % 294.76/42.23 % Exception at run slice level % 294.76/42.23 User error: GNN currently only supports monomorphic FOL. % 294.76/42.23 % (3411346)------------------------------ % 294.76/42.23 % (3411346)------------------------------ % 294.76/42.23 % (3411348)ott+1002_64_sil=16000:si=on:sp=const_min:nwc=0.5:random_seed=3083303105:i=880:nm=2:av=off:rtra=on:gtg=exists_all:fdi=8:gsp=on_2679 on theBenchmark for (2679ds/880Mi) % 294.76/42.23 % (3411348)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 294.76/42.23 % (3411349)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=4217537151:st=1.5:i=22290:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2677 on theBenchmark for (2677ds/22290Mi) % 294.76/42.23 % (3411186)Instruction limit reached! % 294.76/42.23 % (3411186)------------------------------ % 294.76/42.23 % (3411186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 294.76/42.23 % (3411186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.76/42.23 % (3411186)CaDiCaL version: 2.1.3 % 294.76/42.23 % (3411186)Termination reason: Instruction limit % 294.76/42.23 % (3411186)Termination phase: Saturation % 294.76/42.23 % (3411186)Time elapsed: 3.604 s % 294.76/42.23 % (3411186)Peak memory usage: 112 MB % 294.76/42.23 % (3411186)Instructions burned: 4128 (million) % 294.76/42.23 % (3411352)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=4151153075:cts=off:i=6068:av=off:rtra=on:er=known:fsd=on_2674 on theBenchmark for (2674ds/6068Mi) % 294.76/42.23 % (3411277)Instruction limit reached! % 294.76/42.23 % (3411277)------------------------------ % 294.76/42.23 % (3411277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 294.76/42.23 % (3411277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.76/42.23 % (3411277)CaDiCaL version: 2.1.3 % 294.76/42.23 % (3411277)Termination reason: Instruction limit % 294.76/42.23 % (3411277)Termination phase: Saturation % 294.76/42.23 % (3411277)Time elapsed: 3.771 s % 294.76/42.23 % (3411277)Peak memory usage: 116 MB % 294.76/42.23 % (3411277)Instructions burned: 7413 (million) % 294.76/42.23 % Exception at run slice level % 294.76/42.23 User error: GNN currently only supports monomorphic FOL. % 294.76/42.23 % (3411348)Instruction limit reached! % 294.76/42.23 % (3411348)------------------------------ % 294.76/42.23 % (3411348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 294.76/42.23 % (3411348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.76/42.23 % (3411348)CaDiCaL version: 2.1.3 % 294.76/42.23 % (3411348)Termination reason: Instruction limit % 294.76/42.23 % (3411348)Termination phase: Saturation % 294.76/42.23 % (3411348)Time elapsed: 0.794 s % 294.76/42.23 % (3411348)Peak memory usage: 90 MB % 294.76/42.23 % (3411348)Instructions burned: 880 (million) % 294.76/42.23 % (3411354)lrs-1011_64:1_sil=8000:si=on:erd=off:urr=on:nwc=0.7:br=off:random_seed=2345156819:st=2:s2a=on:i=1048:s2at=2:rtra=on:ss=axioms_2669 on theBenchmark for (2669ds/1048Mi) % 294.76/42.23 % (3411355)lrs+1011_16:1_sil=8000:si=on:acc=on:urr=on:fd=preordered:flr=on:random_seed=1601953752:avsq=on:i=2032:avsqr=676809,524288:sd=1:rtra=on:ss=axioms_2669 on theBenchmark for (2669ds/2032Mi) % 294.76/42.23 % (3411356)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:si=on:s2agt=16:random_seed=3228315723:i=28246:bd=preordered:ins=4:rtra=on_2669 on theBenchmark for (2669ds/28246Mi) % 294.76/42.23 % Exception at run slice level % 294.76/42.23 User error: GNN currently only supports monomorphic FOL. % 294.76/42.23 % (3411364)dis+10_4096_slsqTerminated %------------------------------------------------------------------------------