%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV653_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 : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:19:12 PM UTC 2026 % Result : Timeout 293.80s 42.06s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV653_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.09/0.18 % Computer : n015.cluster.edu % 0.09/0.18 % Model : x86_64 x86_64 % 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.18 % Memory : 8046.5625MB % 0.09/0.18 % OS : Linux 6.8.0-71-generic % 0.09/0.18 % CPULimit : 300 % 0.09/0.18 % WCLimit : 300 % 0.09/0.18 % DateTime : Mon Sep 28 12:13:02 UTC 2026 % 0.09/0.18 % CPUTime : % 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.22 Running first-order theorem proving % 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.90/1.75 % (2584054)Detected formulas, will run a generic FOF schedule. % 6.90/1.75 % (2584061)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=1462798838:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 6.90/1.75 % (2584061)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 6.90/1.75 % (2584060)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=1760067960:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 6.90/1.75 % (2584065)dis-21_1_sil=8000:lcm=predicate:random_seed=3777753723:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 6.90/1.75 % (2584059)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=1291456019:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 6.90/1.75 % (2584064)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1330783450:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 6.90/1.75 % (2584063)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2897473259:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 6.90/1.75 % (2584062)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1085689653:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 6.90/1.75 % (2584062)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 6.90/1.75 % (2584062)Refutation not found, incomplete strategy % 6.90/1.75 % (2584062)------------------------------ % 6.90/1.75 % (2584062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.90/1.75 % (2584062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.90/1.75 % (2584062)CaDiCaL version: 2.1.3 % 6.90/1.75 % (2584062)Termination reason: Refutation not found, incomplete strategy % 6.90/1.75 % (2584062)Time elapsed: 0.009 s % 6.90/1.75 % (2584062)Peak memory usage: 88 MB % 6.90/1.75 % (2584062)Instructions burned: 16 (million) % 6.90/1.75 % (2584065)Instruction limit reached! % 6.90/1.75 % (2584065)------------------------------ % 6.90/1.75 % (2584065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.90/1.75 % (2584065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.90/1.75 % (2584065)CaDiCaL version: 2.1.3 % 6.90/1.75 % (2584065)Termination reason: Instruction limit % 6.90/1.75 % (2584065)Termination phase: Saturation % 6.90/1.75 % (2584065)Time elapsed: 0.069 s % 6.90/1.75 % (2584065)Peak memory usage: 89 MB % 6.90/1.75 % (2584065)Instructions burned: 130 (million) % 6.90/1.75 % (2584063)Instruction limit reached! % 6.90/1.75 % (2584063)------------------------------ % 6.90/1.75 % (2584063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.90/1.75 % (2584063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.90/1.75 % (2584063)CaDiCaL version: 2.1.3 % 6.90/1.75 % (2584063)Termination reason: Instruction limit % 6.90/1.75 % (2584063)Termination phase: Saturation % 6.90/1.75 % (2584063)Time elapsed: 0.070 s % 6.90/1.75 % (2584063)Peak memory usage: 88 MB % 6.90/1.75 % (2584063)Instructions burned: 120 (million) % 6.90/1.75 % (2584064)Instruction limit reached! % 6.90/1.75 % (2584064)------------------------------ % 6.90/1.75 % (2584064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.90/1.75 % (2584064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.90/1.75 % (2584064)CaDiCaL version: 2.1.3 % 6.90/1.75 % (2584064)Termination reason: Instruction limit % 6.90/1.75 % (2584064)Termination phase: Saturation % 6.90/1.75 % (2584064)Time elapsed: 0.084 s % 6.90/1.75 % (2584064)Peak memory usage: 89 MB % 6.90/1.75 % (2584064)Instructions burned: 140 (million) % 6.90/1.75 % Exception at run slice level % 6.90/1.75 User error: GNN currently only supports monomorphic FOL. % 6.90/1.75 % (2584073)lrs+10_1_sil=8000:sp=occurrence:random_seed=2259363681:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 6.90/1.75 % (2584074)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2047067788:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 6.90/1.75 % (2584075)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2799621467:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 10.09/2.04 % (2584062)------------------------------ % 10.09/2.04 % (2584062)------------------------------ % 10.09/2.04 % (2584076)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=1185984233:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi) % 10.09/2.04 % (2584074)Instruction limit reached! % 10.09/2.04 % (2584074)------------------------------ % 10.09/2.04 % (2584074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.09/2.04 % (2584074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.09/2.04 % (2584074)CaDiCaL version: 2.1.3 % 10.09/2.04 % (2584074)Termination reason: Instruction limit % 10.09/2.04 % (2584074)Termination phase: Saturation % 10.09/2.04 % (2584074)Time elapsed: 0.085 s % 10.09/2.04 % (2584074)Peak memory usage: 89 MB % 10.09/2.04 % (2584074)Instructions burned: 158 (million) % 10.09/2.04 % (2584076)Instruction limit reached! % 10.09/2.04 % (2584076)------------------------------ % 10.09/2.04 % (2584076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.09/2.04 % (2584076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.09/2.04 % (2584076)CaDiCaL version: 2.1.3 % 10.09/2.04 % (2584076)Termination reason: Instruction limit % 10.09/2.04 % (2584076)Termination phase: Saturation % 10.09/2.04 % (2584076)Time elapsed: 0.076 s % 10.09/2.04 % (2584076)Peak memory usage: 90 MB % 10.09/2.04 % (2584076)Instructions burned: 250 (million) % 10.09/2.04 % Exception at run slice level % 10.09/2.04 User error: GNN currently only supports monomorphic FOL. % 10.09/2.04 % Exception at run slice level % 10.09/2.04 User error: GNN currently only supports monomorphic FOL. % 10.09/2.04 % (2584073)Instruction limit reached! % 10.09/2.04 % (2584073)------------------------------ % 10.09/2.04 % (2584073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.09/2.04 % (2584073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.09/2.04 % (2584073)CaDiCaL version: 2.1.3 % 10.09/2.04 % (2584073)Termination reason: Instruction limit % 10.09/2.04 % (2584073)Termination phase: Saturation % 10.09/2.04 % (2584073)Time elapsed: 0.169 s % 10.09/2.04 % (2584073)Peak memory usage: 90 MB % 10.09/2.04 % (2584073)Instructions burned: 285 (million) % 10.09/2.04 % (2584080)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=417486629:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 10.09/2.04 % (2584080)Refutation not found, incomplete strategy % 10.09/2.04 % (2584080)------------------------------ % 10.09/2.04 % (2584080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.09/2.04 % (2584080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.09/2.04 % (2584080)CaDiCaL version: 2.1.3 % 10.09/2.04 % (2584080)Termination reason: Refutation not found, incomplete strategy % 10.09/2.04 % (2584080)Time elapsed: 0.010 s % 10.09/2.04 % (2584080)Peak memory usage: 88 MB % 10.09/2.04 % (2584080)Instructions burned: 18 (million) % 10.09/2.04 % (2584082)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1505469249:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 10.09/2.04 % (2584083)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4110401298:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 10.09/2.04 % (2584075)Instruction limit reached! % 10.09/2.04 % (2584075)------------------------------ % 10.09/2.04 % (2584075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.09/2.04 % (2584075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.09/2.04 % (2584075)CaDiCaL version: 2.1.3 % 10.09/2.04 % (2584075)Termination reason: Instruction limit % 10.09/2.04 % (2584075)Termination phase: Saturation % 10.09/2.04 % (2584075)Time elapsed: 0.203 s % 10.09/2.04 % (2584075)Peak memory usage: 91 MB % 10.09/2.04 % (2584075)Instructions burned: 326 (million) % 10.09/2.04 % (2584083)Instruction limit reached! % 10.09/2.04 % (2584083)------------------------------ % 10.09/2.04 % (2584083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.09/2.04 % (2584083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.09/2.04 % (2584083)CaDiCaL version: 2.1.3 % 10.09/2.04 % (2584083)Termination reason: Instruction limit % 10.09/2.04 % (2584083)Termination phase: Saturation % 10.09/2.04 % (2584083)Time elapsed: 0.034 s % 10.09/2.04 % (2584083)Peak memory usage: 89 MB % 10.09/2.04 % (2584083)Instructions burned: 116 (million) % 10.92/2.33 % (2584084)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4149775981:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 10.92/2.33 % (2584085)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2877146154:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 10.92/2.33 % (2584084)Refutation not found, incomplete strategy % 10.92/2.33 % (2584084)------------------------------ % 10.92/2.33 % (2584084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.92/2.33 % (2584084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.92/2.33 % (2584084)CaDiCaL version: 2.1.3 % 10.92/2.33 % (2584084)Termination reason: Refutation not found, incomplete strategy % 10.92/2.33 % (2584084)Time elapsed: 0.006 s % 10.92/2.33 % (2584084)Peak memory usage: 88 MB % 10.92/2.33 % (2584084)Instructions burned: 9 (million) % 10.92/2.33 % (2584086)lrs+10_1_sil=8000:sp=occurrence:random_seed=3484174424:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 10.92/2.33 % (2584085)Instruction limit reached! % 10.92/2.33 % (2584085)------------------------------ % 10.92/2.33 % (2584085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.92/2.33 % (2584085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.92/2.33 % (2584085)CaDiCaL version: 2.1.3 % 10.92/2.33 % (2584085)Termination reason: Instruction limit % 10.92/2.33 % (2584085)Termination phase: Saturation % 10.92/2.33 % (2584085)Time elapsed: 0.053 s % 10.92/2.33 % (2584085)Peak memory usage: 88 MB % 10.92/2.33 % (2584085)Instructions burned: 116 (million) % 10.92/2.33 % (2584090)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1288029511:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi) % 10.92/2.33 % (2584090)Refutation not found, incomplete strategy % 10.92/2.33 % (2584090)------------------------------ % 10.92/2.33 % (2584090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.92/2.33 % (2584090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.92/2.33 % (2584090)CaDiCaL version: 2.1.3 % 10.92/2.33 % (2584090)Termination reason: Refutation not found, incomplete strategy % 10.92/2.33 % (2584090)Time elapsed: 0.010 s % 10.92/2.33 % (2584090)Peak memory usage: 88 MB % 10.92/2.33 % (2584090)Instructions burned: 18 (million) % 10.92/2.33 % (2584091)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1956732709:i=5202:ss=axioms:sgt=16_2993 on theBenchmark for (2993ds/5202Mi) % 10.92/2.33 % (2584080)------------------------------ % 10.92/2.33 % (2584080)------------------------------ % 10.92/2.33 % (2584095)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=890229487:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2992 on theBenchmark for (2992ds/134Mi) % 10.92/2.33 % (2584084)------------------------------ % 10.92/2.33 % (2584084)------------------------------ % 10.92/2.33 % Exception at run slice level % 10.92/2.33 User error: GNN currently only supports monomorphic FOL. % 10.92/2.33 % Exception at run slice level % 10.92/2.33 User error: GNN currently only supports monomorphic FOL. % 10.92/2.33 % (2584095)Instruction limit reached! % 10.92/2.33 % (2584095)------------------------------ % 10.92/2.33 % (2584095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.92/2.33 % (2584095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.92/2.33 % (2584095)CaDiCaL version: 2.1.3 % 10.92/2.33 % (2584095)Termination reason: Instruction limit % 10.92/2.33 % (2584095)Termination phase: Saturation % 10.92/2.33 % (2584095)Time elapsed: 0.075 s % 10.92/2.33 % (2584095)Peak memory usage: 90 MB % 10.92/2.33 % (2584095)Instructions burned: 136 (million) % 10.92/2.33 % (2584098)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=819777844:st=8:i=592:sd=3:ep=RST:ss=axioms_2991 on theBenchmark for (2991ds/592Mi) % 10.92/2.33 % (2584090)------------------------------ % 10.92/2.33 % (2584090)------------------------------ % 10.92/2.33 % (2584101)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=3992427672:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/125Mi) % 10.92/2.33 % (2584101)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.92/2.33 % (2584100)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3438378200:st=3:i=13193:sd=3:ss=axioms_2990 on theBenchmark for (2990ds/13193Mi) % 13.98/2.93 % (2584101)Instruction limit reached! % 13.98/2.93 % (2584101)------------------------------ % 13.98/2.93 % (2584101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.98/2.93 % (2584101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.98/2.93 % (2584101)CaDiCaL version: 2.1.3 % 13.98/2.93 % (2584101)Termination reason: Instruction limit % 13.98/2.93 % (2584101)Termination phase: Saturation % 13.98/2.93 % (2584101)Time elapsed: 0.040 s % 13.98/2.93 % (2584101)Peak memory usage: 90 MB % 13.98/2.93 % (2584101)Instructions burned: 129 (million) % 13.98/2.93 % (2584103)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3146948634:i=134:gtgl=5:slsql=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/134Mi) % 13.98/2.93 % (2584104)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=502557170:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/141Mi) % 13.98/2.93 % (2584104)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.98/2.93 % (2584104)Refutation not found, incomplete strategy % 13.98/2.93 % (2584104)------------------------------ % 13.98/2.93 % (2584104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.98/2.93 % (2584104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.98/2.93 % (2584104)CaDiCaL version: 2.1.3 % 13.98/2.93 % (2584104)Termination reason: Refutation not found, incomplete strategy % 13.98/2.93 % (2584104)Time elapsed: 0.005 s % 13.98/2.93 % (2584104)Peak memory usage: 88 MB % 13.98/2.93 % (2584104)Instructions burned: 8 (million) % 13.98/2.93 % Exception at run slice level % 13.98/2.93 User error: Immediate (shared) subterms of term/literal aa(X2,X0,combb(X1,X0,X2,X5,X4),X3) = sF20(X2,X0,X1,X5,X4,X3) have different types/not well-typed! % 13.98/2.93 % (2584105)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2875151012:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/431Mi) % 13.98/2.93 % (2584108)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=3750058650:i=6060:aac=none:ins=25_2988 on theBenchmark for (2988ds/6060Mi) % 13.98/2.93 % (2584098)Instruction limit reached! % 13.98/2.93 % (2584098)------------------------------ % 13.98/2.93 % (2584098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.98/2.93 % (2584098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.98/2.93 % (2584098)CaDiCaL version: 2.1.3 % 13.98/2.93 % (2584098)Termination reason: Instruction limit % 13.98/2.93 % (2584098)Termination phase: Saturation % 13.98/2.93 % (2584098)Time elapsed: 0.254 s % 13.98/2.93 % (2584098)Peak memory usage: 89 MB % 13.98/2.93 % (2584098)Instructions burned: 595 (million) % 13.98/2.93 % (2584086)Instruction limit reached! % 13.98/2.93 % (2584086)------------------------------ % 13.98/2.93 % (2584086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.98/2.93 % (2584086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.98/2.93 % (2584086)CaDiCaL version: 2.1.3 % 13.98/2.93 % (2584086)Termination reason: Instruction limit % 13.98/2.93 % (2584086)Termination phase: Saturation % 13.98/2.93 % (2584086)Time elapsed: 0.551 s % 13.98/2.93 % (2584086)Peak memory usage: 94 MB % 13.98/2.93 % (2584086)Instructions burned: 907 (million) % 13.98/2.93 % (2584111)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=1753403672:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2988 on theBenchmark for (2988ds/150Mi) % 13.98/2.93 % (2584111)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.98/2.93 % (2584104)------------------------------ % 13.98/2.93 % (2584104)------------------------------ % 13.98/2.93 % (2584105)Instruction limit reached! % 13.98/2.93 % (2584105)------------------------------ % 13.98/2.93 % (2584105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.98/2.93 % (2584105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.98/2.93 % (2584105)CaDiCaL version: 2.1.3 % 13.98/2.93 % (2584105)Termination reason: Instruction limit % 13.98/2.93 % (2584105)Termination phase: Saturation % 13.98/2.93 % (2584105)Time elapsed: 0.199 s % 20.42/3.82 % (2584105)Peak memory usage: 90 MB % 20.42/3.82 % (2584105)Instructions burned: 433 (million) % 20.42/3.82 % (2584111)Instruction limit reached! % 20.42/3.82 % (2584111)------------------------------ % 20.42/3.82 % (2584111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.42/3.82 % (2584111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.42/3.82 % (2584111)CaDiCaL version: 2.1.3 % 20.42/3.82 % (2584111)Termination reason: Instruction limit % 20.42/3.82 % (2584111)Termination phase: Saturation % 20.42/3.82 % (2584111)Time elapsed: 0.093 s % 20.42/3.82 % (2584111)Peak memory usage: 90 MB % 20.42/3.82 % (2584111)Instructions burned: 150 (million) % 20.42/3.82 % (2584115)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=847628830:i=667:av=off:fsr=off_2987 on theBenchmark for (2987ds/667Mi) % 20.42/3.82 % (2584114)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=4153847655:i=14155:bd=all_2987 on theBenchmark for (2987ds/14155Mi) % 20.42/3.82 % (2584115)Refutation not found, incomplete strategy % 20.42/3.82 % (2584115)------------------------------ % 20.42/3.82 % (2584115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.42/3.82 % (2584115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.42/3.82 % (2584115)CaDiCaL version: 2.1.3 % 20.42/3.82 % (2584115)Termination reason: Refutation not found, incomplete strategy % 20.42/3.82 % (2584115)Time elapsed: 0.010 s % 20.42/3.82 % (2584115)Peak memory usage: 88 MB % 20.42/3.82 % (2584115)Instructions burned: 18 (million) % 20.42/3.82 % Exception at run slice level % 20.42/3.82 User error: GNN currently only supports monomorphic FOL. % 20.42/3.82 % Exception at run slice level % 20.42/3.82 User error: GNN currently only supports monomorphic FOL. % 20.42/3.82 % (2584118)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1562065848:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2986 on theBenchmark for (2986ds/193Mi) % 20.42/3.82 % (2584119)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=164852674:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2986 on theBenchmark for (2986ds/4850Mi) % 20.42/3.82 % (2584117)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=2227534158:s2a=on:i=185:s2at=1.8:fdi=4_2986 on theBenchmark for (2986ds/185Mi) % 20.42/3.82 % (2584119)Refutation not found, incomplete strategy % 20.42/3.82 % (2584119)------------------------------ % 20.42/3.82 % (2584119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.42/3.82 % (2584119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.42/3.82 % (2584119)CaDiCaL version: 2.1.3 % 20.42/3.82 % (2584119)Termination reason: Refutation not found, incomplete strategy % 20.42/3.82 % (2584119)Time elapsed: 0.007 s % 20.42/3.82 % (2584119)Peak memory usage: 87 MB % 20.42/3.82 % (2584119)Instructions burned: 14 (million) % 20.42/3.82 % (2584122)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3603430649:i=12111:sd=1:ss=included_2985 on theBenchmark for (2985ds/12111Mi) % 20.42/3.82 % (2584123)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2955689970:i=319:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/319Mi) % 20.42/3.82 % (2584115)------------------------------ % 20.42/3.82 % (2584115)------------------------------ % 20.42/3.82 % (2584117)Instruction limit reached! % 20.42/3.82 % (2584117)------------------------------ % 20.42/3.82 % (2584117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.42/3.82 % (2584117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.42/3.82 % (2584117)CaDiCaL version: 2.1.3 % 20.42/3.82 % (2584117)Termination reason: Instruction limit % 20.42/3.82 % (2584117)Termination phase: Saturation % 20.42/3.82 % (2584117)Time elapsed: 0.119 s % 20.42/3.82 % (2584117)Peak memory usage: 91 MB % 20.42/3.82 % (2584117)Instructions burned: 185 (million) % 20.42/3.82 % (2584118)Instruction limit reached! % 20.42/3.82 % (2584118)------------------------------ % 20.42/3.82 % (2584118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.42/3.82 % (2584118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.42/3.82 % (2584118)CaDiCaL version: 2.1.3 % 20.42/3.82 % (2584118)Termination reason: Instruction limit % 20.42/3.82 % (2584118)Termination phase: Saturation % 28.42/4.87 % (2584118)Time elapsed: 0.124 s % 28.42/4.87 % (2584118)Peak memory usage: 90 MB % 28.42/4.87 % (2584118)Instructions burned: 193 (million) % 28.42/4.87 % Exception at run slice level % 28.42/4.87 User error: GNN currently only supports monomorphic FOL. % 28.42/4.87 % Exception at run slice level % 28.42/4.87 User error: GNN currently only supports monomorphic FOL. % 28.42/4.87 % (2584119)------------------------------ % 28.42/4.87 % (2584119)------------------------------ % 28.42/4.87 % (2584131)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1900550560:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2983 on theBenchmark for (2983ds/757Mi) % 28.42/4.87 % (2584130)dis-1011_128_sil=32000:random_seed=1103626037:i=3706:ep=RST:av=off_2983 on theBenchmark for (2983ds/3706Mi) % 28.42/4.87 % (2584129)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2910785375:i=2064:ep=RST_2983 on theBenchmark for (2983ds/2064Mi) % 28.42/4.87 % (2584123)Instruction limit reached! % 28.42/4.87 % (2584123)------------------------------ % 28.42/4.87 % (2584123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.42/4.87 % (2584123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.42/4.87 % (2584123)CaDiCaL version: 2.1.3 % 28.42/4.87 % (2584123)Termination reason: Instruction limit % 28.42/4.87 % (2584123)Termination phase: Saturation % 28.42/4.87 % (2584123)Time elapsed: 0.192 s % 28.42/4.87 % (2584123)Peak memory usage: 91 MB % 28.42/4.87 % (2584123)Instructions burned: 320 (million) % 28.42/4.87 % (2584131)Refutation not found, incomplete strategy % 28.42/4.87 % (2584131)------------------------------ % 28.42/4.87 % (2584131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.42/4.87 % (2584131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.42/4.87 % (2584131)CaDiCaL version: 2.1.3 % 28.42/4.87 % (2584131)Termination reason: Refutation not found, incomplete strategy % 28.42/4.87 % (2584131)Time elapsed: 0.009 s % 28.42/4.87 % (2584131)Peak memory usage: 88 MB % 28.42/4.87 % (2584131)Instructions burned: 16 (million) % 28.42/4.87 % (2584132)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2803331189:i=13913:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/13913Mi) % 28.42/4.87 % (2584133)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=614012551:i=9925:aac=none_2982 on theBenchmark for (2982ds/9925Mi) % 28.42/4.87 % (2584134)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=30631023:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2981 on theBenchmark for (2981ds/2479Mi) % 28.42/4.87 % (2584134)Refutation not found, incomplete strategy % 28.42/4.87 % (2584134)------------------------------ % 28.42/4.87 % (2584134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.42/4.87 % (2584134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.42/4.87 % (2584134)CaDiCaL version: 2.1.3 % 28.42/4.87 % (2584134)Termination reason: Refutation not found, incomplete strategy % 28.42/4.87 % (2584134)Time elapsed: 0.010 s % 28.42/4.87 % (2584134)Peak memory usage: 88 MB % 28.42/4.87 % (2584134)Instructions burned: 18 (million) % 28.42/4.87 % (2584138)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=173637024:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/440Mi) % 28.42/4.87 % (2584138)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 28.42/4.87 % Exception at run slice level % 28.42/4.87 User error: GNN currently only supports monomorphic FOL. % 28.42/4.87 % (2584131)------------------------------ % 28.42/4.87 % (2584131)------------------------------ % 28.42/4.87 % (2584143)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3679499565:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2979 on theBenchmark for (2979ds/11145Mi) % 28.42/4.87 % (2584134)------------------------------ % 28.42/4.87 % (2584134)------------------------------ % 28.42/4.87 % (2584144)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=3451722024:cts=off:i=3034:av=off:er=known:fsd=on_2979 on theBenchmark for (2979ds/3034Mi) % 28.42/4.87 % (2584138)Instruction limit reached! % 28.42/4.87 % (2584138)------------------------------ % 28.42/4.87 % (2584138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.96/5.38 % (2584138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.96/5.38 % (2584138)CaDiCaL version: 2.1.3 % 32.96/5.38 % (2584138)Termination reason: Instruction limit % 32.96/5.38 % (2584138)Termination phase: Saturation % 32.96/5.38 % (2584138)Time elapsed: 0.276 s % 32.96/5.38 % (2584138)Peak memory usage: 92 MB % 32.96/5.38 % (2584138)Instructions burned: 441 (million) % 32.96/5.38 % Exception at run slice level % 32.96/5.38 User error: GNN currently only supports monomorphic FOL. % 32.96/5.38 % (2584146)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1702663283:st=2:s2a=on:i=524:s2at=2:ss=axioms_2977 on theBenchmark for (2977ds/524Mi) % 32.96/5.38 % Exception at run slice level % 32.96/5.38 User error: GNN currently only supports monomorphic FOL. % 32.96/5.38 % (2584148)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=504306174:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2977 on theBenchmark for (2977ds/1016Mi) % 32.96/5.38 % (2584149)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=444864717:i=14123:bd=preordered:ins=4_2977 on theBenchmark for (2977ds/14123Mi) % 32.96/5.38 % (2584151)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2386641110:i=5781:kws=precedence:bd=all:rawr=on_2976 on theBenchmark for (2976ds/5781Mi) % 32.96/5.38 % Exception at run slice level % 32.96/5.38 User error: GNN currently only supports monomorphic FOL. % 32.96/5.38 % (2584129)Instruction limit reached! % 32.96/5.38 % (2584129)------------------------------ % 32.96/5.38 % (2584129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.96/5.38 % (2584129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.96/5.38 % (2584129)CaDiCaL version: 2.1.3 % 32.96/5.38 % (2584129)Termination reason: Instruction limit % 32.96/5.38 % (2584129)Termination phase: Saturation % 32.96/5.38 % (2584129)Time elapsed: 0.823 s % 32.96/5.38 % (2584129)Peak memory usage: 90 MB % 32.96/5.38 % (2584129)Instructions burned: 2064 (million) % 32.96/5.38 % (2584146)Instruction limit reached! % 32.96/5.38 % (2584146)------------------------------ % 32.96/5.38 % (2584146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.96/5.38 % (2584146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.96/5.38 % (2584146)CaDiCaL version: 2.1.3 % 32.96/5.38 % (2584146)Termination reason: Instruction limit % 32.96/5.38 % (2584146)Termination phase: Saturation % 32.96/5.38 % (2584146)Time elapsed: 0.283 s % 32.96/5.38 % (2584146)Peak memory usage: 92 MB % 32.96/5.38 % (2584146)Instructions burned: 524 (million) % 32.96/5.38 % (2584155)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=2426928701:i=2448:gtgl=5:bd=preordered:gtg=all_2973 on theBenchmark for (2973ds/2448Mi) % 32.96/5.38 % Exception at run slice level % 32.96/5.38 User error: GNN currently only supports monomorphic FOL. % 32.96/5.38 % (2584156)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2953831242:i=3223:kws=precedence:fgj=on:av=off_2973 on theBenchmark for (2973ds/3223Mi) % 32.96/5.38 % (2584157)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2256066955:st=5.6:i=2033:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/2033Mi) % 32.96/5.38 % (2584148)Instruction limit reached! % 32.96/5.38 % (2584148)------------------------------ % 32.96/5.38 % (2584148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.96/5.38 % (2584148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.96/5.38 % (2584148)CaDiCaL version: 2.1.3 % 32.96/5.38 % (2584148)Termination reason: Instruction limit % 32.96/5.38 % (2584148)Termination phase: Saturation % 32.96/5.38 % (2584148)Time elapsed: 0.549 s % 32.96/5.38 % (2584148)Peak memory usage: 98 MB % 32.96/5.38 % (2584148)Instructions burned: 1018 (million) % 32.96/5.38 % (2584160)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1576683957:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2971 on theBenchmark for (2971ds/2055Mi) % 32.96/5.38 % Exception at run slice level % 32.96/5.38 User error: GNN currently only supports monomorphic FOL. % 32.96/5.38 % (2584163)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=3390725018:i=21611:sd=3:ss=axioms_2970 on theBenchmark for (2970ds/21611Mi) % 32.96/5.38 % Exception at run slice level % 41.95/6.72 User error: GNN currently only supports monomorphic FOL. % 41.95/6.72 % Exception at run slice level % 41.95/6.72 User error: GNN currently only supports monomorphic FOL. % 41.95/6.72 % (2584130)Instruction limit reached! % 41.95/6.72 % (2584130)------------------------------ % 41.95/6.72 % (2584130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.95/6.72 % (2584130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.95/6.72 % (2584130)CaDiCaL version: 2.1.3 % 41.95/6.72 % (2584130)Termination reason: Instruction limit % 41.95/6.72 % (2584130)Termination phase: Saturation % 41.95/6.72 % (2584130)Time elapsed: 1.428 s % 41.95/6.72 % (2584130)Peak memory usage: 89 MB % 41.95/6.72 % (2584130)Instructions burned: 3706 (million) % 41.95/6.72 % (2584164)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=764217613:i=4835:sd=13:ss=axioms:sgt=23_2968 on theBenchmark for (2968ds/4835Mi) % 41.95/6.72 % (2584166)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=1601247226:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2968 on theBenchmark for (2968ds/797Mi) % 41.95/6.72 % Exception at run slice level % 41.95/6.72 User error: GNN currently only supports monomorphic FOL. % 41.95/6.72 % (2584167)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=311774265:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2968 on theBenchmark for (2968ds/2326Mi) % 41.95/6.72 % (2584167)Refutation not found, incomplete strategy % 41.95/6.72 % (2584167)------------------------------ % 41.95/6.72 % (2584167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.95/6.72 % (2584167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.95/6.72 % (2584167)CaDiCaL version: 2.1.3 % 41.95/6.72 % (2584167)Termination reason: Refutation not found, incomplete strategy % 41.95/6.72 % (2584167)Time elapsed: 0.019 s % 41.95/6.72 % (2584167)Peak memory usage: 89 MB % 41.95/6.72 % (2584167)Instructions burned: 29 (million) % 41.95/6.72 % (2584168)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2891001702:i=6038:nm=6_2967 on theBenchmark for (2967ds/6038Mi) % 41.95/6.72 % (2584171)lrs+10_1_sil=32000:sp=occurrence:random_seed=1350529679:st=2:i=33334:sd=3:ss=included:sgt=32_2966 on theBenchmark for (2966ds/33334Mi) % 41.95/6.72 % Exception at run slice level % 41.95/6.72 User error: GNN currently only supports monomorphic FOL. % 41.95/6.72 % (2584167)------------------------------ % 41.95/6.72 % (2584167)------------------------------ % 41.95/6.72 % (2584175)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2849867434:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2964 on theBenchmark for (2964ds/1008Mi) % 41.95/6.72 % (2584176)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=998971620:i=8327:s2at=5:bd=preordered_2963 on theBenchmark for (2963ds/8327Mi) % 41.95/6.72 % Exception at run slice level % 41.95/6.72 User error: GNN currently only supports monomorphic FOL. % 41.95/6.72 % (2584166)Instruction limit reached! % 41.95/6.72 % (2584166)------------------------------ % 41.95/6.72 % (2584166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.95/6.72 % (2584166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.95/6.72 % (2584166)CaDiCaL version: 2.1.3 % 41.95/6.72 % (2584166)Termination reason: Instruction limit % 41.95/6.72 % (2584166)Termination phase: Saturation % 41.95/6.72 % (2584166)Time elapsed: 0.487 s % 41.95/6.72 % (2584166)Peak memory usage: 93 MB % 41.95/6.72 % (2584166)Instructions burned: 798 (million) % 41.95/6.72 % (2584179)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=14150045:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2962 on theBenchmark for (2962ds/1083Mi) % 41.95/6.72 % (2584180)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=166220335:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2961 on theBenchmark for (2961ds/1084Mi) % 41.95/6.72 % Exception at run slice level % 41.95/6.72 User error: GNN currently only supports monomorphic FOL. % 41.95/6.72 % (2584175)Instruction limit reached! % 41.95/6.72 % (2584175)------------------------------ % 50.80/7.99 % (2584175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.80/7.99 % (2584175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.80/7.99 % (2584175)CaDiCaL version: 2.1.3 % 50.80/7.99 % (2584175)Termination reason: Instruction limit % 50.80/7.99 % (2584175)Termination phase: Saturation % 50.80/7.99 % (2584175)Time elapsed: 0.542 s % 50.80/7.99 % (2584175)Peak memory usage: 98 MB % 50.80/7.99 % (2584175)Instructions burned: 1010 (million) % 50.80/7.99 % (2584151)Instruction limit reached! % 50.80/7.99 % (2584151)------------------------------ % 50.80/7.99 % (2584151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.80/7.99 % (2584151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.80/7.99 % (2584151)CaDiCaL version: 2.1.3 % 50.80/7.99 % (2584151)Termination reason: Instruction limit % 50.80/7.99 % (2584151)Termination phase: Saturation % 50.80/7.99 % (2584151)Time elapsed: 1.784 s % 50.80/7.99 % (2584151)Peak memory usage: 107 MB % 50.80/7.99 % (2584151)Instructions burned: 5781 (million) % 50.80/7.99 % (2584183)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3454081080:i=6995:s2at=5:gtg=all_2958 on theBenchmark for (2958ds/6995Mi) % 50.80/7.99 % (2584184)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=3434764633:st=2:i=6225:sd=15:ss=axioms_2957 on theBenchmark for (2957ds/6225Mi) % 50.80/7.99 % (2584184)Refutation not found, incomplete strategy % 50.80/7.99 % (2584184)------------------------------ % 50.80/7.99 % (2584184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.80/7.99 % (2584184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.80/7.99 % (2584184)CaDiCaL version: 2.1.3 % 50.80/7.99 % (2584184)Termination reason: Refutation not found, incomplete strategy % 50.80/7.99 % (2584184)Time elapsed: 0.011 s % 50.80/7.99 % (2584184)Peak memory usage: 88 MB % 50.80/7.99 % (2584184)Instructions burned: 19 (million) % 50.80/7.99 % (2584185)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2911408969:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2957 on theBenchmark for (2957ds/3372Mi) % 50.80/7.99 % (2584179)Instruction limit reached! % 50.80/7.99 % (2584179)------------------------------ % 50.80/7.99 % (2584179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.80/7.99 % (2584179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.80/7.99 % (2584179)CaDiCaL version: 2.1.3 % 50.80/7.99 % (2584179)Termination reason: Instruction limit % 50.80/7.99 % (2584179)Termination phase: Saturation % 50.80/7.99 % (2584179)Time elapsed: 0.518 s % 50.80/7.99 % (2584179)Peak memory usage: 96 MB % 50.80/7.99 % (2584179)Instructions burned: 1083 (million) % 50.80/7.99 % (2584180)Instruction limit reached! % 50.80/7.99 % (2584180)------------------------------ % 50.80/7.99 % (2584180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.80/7.99 % (2584180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.80/7.99 % (2584180)CaDiCaL version: 2.1.3 % 50.80/7.99 % (2584180)Termination reason: Instruction limit % 50.80/7.99 % (2584180)Termination phase: Saturation % 50.80/7.99 % (2584180)Time elapsed: 0.578 s % 50.80/7.99 % (2584180)Peak memory usage: 95 MB % 50.80/7.99 % (2584180)Instructions burned: 1084 (million) % 50.80/7.99 % Exception at run slice level % 50.80/7.99 User error: GNN currently only supports monomorphic FOL. % 50.80/7.99 % (2584184)------------------------------ % 50.80/7.99 % (2584184)------------------------------ % 50.80/7.99 % (2584189)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=701619564:st=2.3:i=26457:sd=10:ss=included:sgt=8_2955 on theBenchmark for (2955ds/26457Mi) % 50.80/7.99 % Exception at run slice level % 50.80/7.99 User error: GNN currently only supports monomorphic FOL. % 50.80/7.99 % (2584190)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=568739681:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2954 on theBenchmark for (2954ds/13494Mi) % 50.80/7.99 % (2584191)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=729947545:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2953 on theBenchmark for (2953ds/2503Mi) % 50.80/7.99 % (2584191)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 62.73/9.64 % (2584193)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=859420369:i=2559:sd=1:ep=RSTC:ss=axioms_2953 on theBenchmark for (2953ds/2559Mi) % 62.73/9.64 % (2584194)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3502829815:i=30753:av=off:ss=included_2953 on theBenchmark for (2953ds/30753Mi) % 62.73/9.64 % Exception at run slice level % 62.73/9.64 User error: GNN currently only supports monomorphic FOL. % 62.73/9.64 % Exception at run slice level % 62.73/9.64 User error: GNN currently only supports monomorphic FOL. % 62.73/9.64 % (2584199)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=1895125556:i=26473:ep=RSTC_2950 on theBenchmark for (2950ds/26473Mi) % 62.73/9.64 % Exception at run slice level % 62.73/9.64 User error: GNN currently only supports monomorphic FOL. % 62.73/9.64 % Exception at run slice level % 62.73/9.64 User error: GNN currently only supports monomorphic FOL. % 62.73/9.64 % (2584200)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=1917072225:cts=off:i=2759:kws=inv_arity:fgj=on_2950 on theBenchmark for (2950ds/2759Mi) % 62.73/9.64 % Exception at run slice level % 62.73/9.64 User error: GNN currently only supports monomorphic FOL. % 62.73/9.64 % (2584202)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=1006978408:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2949 on theBenchmark for (2949ds/5665Mi) % 62.73/9.64 % (2584202)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 62.73/9.64 % (2584203)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=2569906930:i=1532:ep=RS:ss=axioms_2948 on theBenchmark for (2948ds/1532Mi) % 62.73/9.64 % (2584205)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3785076996:i=1565:sd=2:ss=axioms:sgt=32_2948 on theBenchmark for (2948ds/1565Mi) % 62.73/9.64 % Exception at run slice level % 62.73/9.64 User error: GNN currently only supports monomorphic FOL. % 62.73/9.64 % Exception at run slice level % 62.73/9.64 User error: GNN currently only supports monomorphic FOL. % 62.73/9.64 % Exception at run slice level % 62.73/9.64 User error: GNN currently only supports monomorphic FOL. % 62.73/9.64 % (2584209)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=2681567684:i=1572:fgj=on:gsp=on_2945 on theBenchmark for (2945ds/1572Mi) % 62.73/9.64 % (2584209)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 62.73/9.64 % Exception at run slice level % 62.73/9.64 User error: GNN currently only supports monomorphic FOL. % 62.73/9.64 % (2584210)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=3638329907:i=6052:sd=4:ss=axioms:sgt=24_2944 on theBenchmark for (2944ds/6052Mi) % 62.73/9.64 % (2584211)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=1878429288:i=3500:sd=1:bd=preordered:sup=off:ss=included_2943 on theBenchmark for (2943ds/3500Mi) % 62.73/9.64 % (2584213)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=455586144:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2943 on theBenchmark for (2943ds/1842Mi) % 62.73/9.64 % (2584213)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 62.73/9.64 % Exception at run slice level % 62.73/9.64 User error: GNN currently only supports monomorphic FOL. % 62.73/9.64 % (2584164)Instruction limit reached! % 62.73/9.64 % (2584164)------------------------------ % 62.73/9.64 % (2584164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.73/9.64 % (2584164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.73/9.64 % (2584164)CaDiCaL version: 2.1.3 % 62.73/9.64 % (2584164)Termination reason: Instruction limit % 62.73/9.64 % (2584164)Termination phase: Saturation % 62.73/9.64 % (2584164)Time elapsed: 2.796 s % 62.73/9.64 % (2584164)Peak memory usage: 105 MB % 74.93/11.20 % (2584164)Instructions burned: 4835 (million) % 74.93/11.20 % Exception at run slice level % 74.93/11.20 User error: GNN currently only supports monomorphic FOL. % 74.93/11.20 % Exception at run slice level % 74.93/11.20 User error: GNN currently only supports monomorphic FOL. % 74.93/11.20 % (2584217)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3590226300:i=66096:add=on_2939 on theBenchmark for (2939ds/66096Mi) % 74.93/11.20 % Exception at run slice level % 74.93/11.20 User error: GNN currently only supports monomorphic FOL. % 74.93/11.20 % (2584218)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=1244762084:i=1884:sd=1:nm=60:ss=axioms_2939 on theBenchmark for (2939ds/1884Mi) % 74.93/11.20 % (2584219)lrs-1011_4:1_sil=16000:bsr=on:random_seed=2363063658:cts=off:i=5469:bs=on:fsr=off_2939 on theBenchmark for (2939ds/5469Mi) % 74.93/11.20 % (2584220)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=1569346445:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2938 on theBenchmark for (2938ds/2037Mi) % 74.93/11.20 % (2584222)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3587574598:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2937 on theBenchmark for (2937ds/2110Mi) % 74.93/11.20 % Exception at run slice level % 74.93/11.20 User error: GNN currently only supports monomorphic FOL. % 74.93/11.20 % Exception at run slice level % 74.93/11.20 User error: GNN currently only supports monomorphic FOL. % 74.93/11.20 % Exception at run slice level % 74.93/11.20 User error: GNN currently only supports monomorphic FOL. % 74.93/11.20 % (2584227)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=479513985:i=2430:add=off:aac=none:nm=16_2934 on theBenchmark for (2934ds/2430Mi) % 74.93/11.20 % Exception at run slice level % 74.93/11.20 User error: GNN currently only supports monomorphic FOL. % 74.93/11.20 % (2584228)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=3324076484:cond=fast:i=4891_2934 on theBenchmark for (2934ds/4891Mi) % 74.93/11.20 % (2584229)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=452501685:st=2:i=14845:sd=2:ss=included:fsd=on_2933 on theBenchmark for (2933ds/14845Mi) % 74.93/11.20 % (2584231)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=3993404174:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2932 on theBenchmark for (2932ds/7534Mi) % 74.93/11.20 % Exception at run slice level % 74.93/11.20 User error: GNN currently only supports monomorphic FOL. % 74.93/11.20 % Exception at run slice level % 74.93/11.20 User error: GNN currently only supports monomorphic FOL. % 74.93/11.20 % Exception at run slice level % 74.93/11.20 User error: GNN currently only supports monomorphic FOL. % 74.93/11.20 % (2584235)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=3749077033:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2929 on theBenchmark for (2929ds/10353Mi) % 74.93/11.20 % Exception at run slice level % 74.93/11.20 User error: GNN currently only supports monomorphic FOL. % 74.93/11.20 % (2584236)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=955001575:i=7860_2929 on theBenchmark for (2929ds/7860Mi) % 74.93/11.20 % (2584236)Refutation not found, incomplete strategy % 74.93/11.20 % (2584236)------------------------------ % 74.93/11.20 % (2584236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.93/11.20 % (2584236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.93/11.20 % (2584236)CaDiCaL version: 2.1.3 % 74.93/11.20 % (2584236)Termination reason: Refutation not found, incomplete strategy % 74.93/11.20 % (2584236)Time elapsed: 0.010 s % 74.93/11.20 % (2584236)Peak memory usage: 88 MB % 74.93/11.20 % (2584236)Instructions burned: 17 (million) % 74.93/11.20 % (2584237)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=1891321048:i=7896:sd=2:bs=on:ss=included:sgt=20_2928 on theBenchmark for (2928ds/7896Mi) % 92.13/13.66 % (2584239)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=814793493:i=5812:gtgl=2:gtg=all_2927 on theBenchmark for (2927ds/5812Mi) % 92.13/13.66 % (2584236)------------------------------ % 92.13/13.66 % (2584236)------------------------------ % 92.13/13.66 % Exception at run slice level % 92.13/13.66 User error: GNN currently only supports monomorphic FOL. % 92.13/13.66 % (2584243)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=2256584088:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2924 on theBenchmark for (2924ds/2965Mi) % 92.13/13.66 % Exception at run slice level % 92.13/13.66 User error: GNN currently only supports monomorphic FOL. % 92.13/13.66 % (2584244)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=1047347397:i=2967:kws=precedence:bd=preordered:av=off_2924 on theBenchmark for (2924ds/2967Mi) % 92.13/13.66 % Exception at run slice level % 92.13/13.66 User error: GNN currently only supports monomorphic FOL. % 92.13/13.66 % (2584246)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=1322123986:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2923 on theBenchmark for (2923ds/3022Mi) % 92.13/13.66 % (2584248)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=991901512:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2922 on theBenchmark for (2922ds/3207Mi) % 92.13/13.66 % Exception at run slice level % 92.13/13.66 User error: GNN currently only supports monomorphic FOL. % 92.13/13.66 % Exception at run slice level % 92.13/13.66 User error: GNN currently only supports monomorphic FOL. % 92.13/13.66 % (2584251)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=3954924894:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2919 on theBenchmark for (2919ds/3289Mi) % 92.13/13.66 % Exception at run slice level % 92.13/13.66 User error: GNN currently only supports monomorphic FOL. % 92.13/13.66 % (2584252)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=3131976880:i=38569:sd=3:ss=axioms:sgt=32_2919 on theBenchmark for (2919ds/38569Mi) % 92.13/13.66 % Exception at run slice level % 92.13/13.66 User error: GNN currently only supports monomorphic FOL. % 92.13/13.66 % (2584254)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=3174154659:cts=off:i=3394_2917 on theBenchmark for (2917ds/3394Mi) % 92.13/13.66 % (2584256)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=540890924:i=33824:bd=preordered_2917 on theBenchmark for (2917ds/33824Mi) % 92.13/13.66 % Exception at run slice level % 92.13/13.66 User error: GNN currently only supports monomorphic FOL. % 92.13/13.66 % Exception at run slice level % 92.13/13.66 User error: GNN currently only supports monomorphic FOL. % 92.13/13.66 % (2584259)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=2611083421:i=20684:bd=all:gtg=exists_sym_2914 on theBenchmark for (2914ds/20684Mi) % 92.13/13.66 % Exception at run slice level % 92.13/13.66 User error: GNN currently only supports monomorphic FOL. % 92.13/13.66 % (2584260)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=4284141964:st=3:prac=on:i=7222:kws=arity_squared:add=on:fgj=on:bd=preordered:gtg=exists_top:gsp=on:ss=axioms:er=known:sgt=8:proc=on_2914 on theBenchmark for (2914ds/7222Mi) % 92.13/13.66 % (2584260)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 92.13/13.66 % Exception at run slice level % 92.13/13.66 User error: GNN currently only supports monomorphic FOL. % 92.13/13.66 % (2584263)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=2080978949:st=4:i=7295:sd=4:ep=R:ss=axioms_2912 on theBenchmark for (2912ds/7295Mi) % 92.13/13.66 % (2584264)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=313246532:i=4036:ins=10_2911 on theBenchmark for (2911ds/4036Mi) % 112.97/16.68 % Exception at run slice level % 112.97/16.68 User error: GNN currently only supports monomorphic FOL. % 112.97/16.68 % Exception at run slice level % 112.97/16.68 User error: GNN currently only supports monomorphic FOL. % 112.97/16.68 % (2584267)lrs+10_1_sil=128000:lcm=predicate:random_seed=4054471794:st=3:i=43697:sd=5:ss=axioms_2909 on theBenchmark for (2909ds/43697Mi) % 112.97/16.68 % (2584268)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=4054217237:i=17599:gtg=all:ss=axioms:fsd=on_2908 on theBenchmark for (2908ds/17599Mi) % 112.97/16.68 % Exception at run slice level % 112.97/16.68 User error: GNN currently only supports monomorphic FOL. % 112.97/16.68 % Exception at run slice level % 112.97/16.68 User error: GNN currently only supports monomorphic FOL. % 112.97/16.68 % (2584271)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=2388807045:i=4547:bd=preordered_2907 on theBenchmark for (2907ds/4547Mi) % 112.97/16.68 % (2584272)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=3726324469:i=9294:av=off_2906 on theBenchmark for (2906ds/9294Mi) % 112.97/16.68 % Exception at run slice level % 112.97/16.68 User error: GNN currently only supports monomorphic FOL. % 112.97/16.68 % (2584219)Instruction limit reached! % 112.97/16.68 % (2584219)------------------------------ % 112.97/16.68 % (2584219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.97/16.68 % (2584219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.97/16.68 % (2584219)CaDiCaL version: 2.1.3 % 112.97/16.68 % (2584219)Termination reason: Instruction limit % 112.97/16.68 % (2584219)Termination phase: Saturation % 112.97/16.68 % (2584219)Time elapsed: 3.364 s % 112.97/16.68 % (2584219)Peak memory usage: 112 MB % 112.97/16.68 % (2584219)Instructions burned: 5469 (million) % 112.97/16.68 % (2584275)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=267347387:i=32849:add=on_2903 on theBenchmark for (2903ds/32849Mi) % 112.97/16.68 % Exception at run slice level % 112.97/16.68 User error: GNN currently only supports monomorphic FOL. % 112.97/16.68 % (2584276)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3848791732:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2903 on theBenchmark for (2903ds/4793Mi) % 112.97/16.68 % Exception at run slice level % 112.97/16.68 User error: GNN currently only supports monomorphic FOL. % 112.97/16.68 % (2584279)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=2319544195:i=4840:nm=4:av=off_2902 on theBenchmark for (2902ds/4840Mi) % 112.97/16.68 % (2584280)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=2028258972:cts=off:i=5002_2901 on theBenchmark for (2901ds/5002Mi) % 112.97/16.68 % Exception at run slice level % 112.97/16.68 User error: GNN currently only supports monomorphic FOL. % 112.97/16.68 % Exception at run slice level % 112.97/16.68 User error: GNN currently only supports monomorphic FOL. % 112.97/16.68 % (2584283)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=4058789162:i=30479:sd=3:ss=axioms_2898 on theBenchmark for (2898ds/30479Mi) % 112.97/16.68 % Exception at run slice level % 112.97/16.68 User error: GNN currently only supports monomorphic FOL. % 112.97/16.68 % (2584284)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=2065174679:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2898 on theBenchmark for (2898ds/11035Mi) % 112.97/16.68 % (2584284)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 112.97/16.68 % Exception at run slice level % 112.97/16.68 User error: GNN currently only supports monomorphic FOL. % 112.97/16.68 % (2584287)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=3029246636:i=5835_2896 on theBenchmark for (2896ds/5835Mi) % 112.97/16.68 % (2584288)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=3515299914:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2896 on theBenchmark for (2896ds/5890Mi) % 149.53/21.76 % Exception at run slice level % 149.53/21.76 User error: GNN currently only supports monomorphic FOL. % 149.53/21.76 % Exception at run slice level % 149.53/21.76 User error: GNN currently only supports monomorphic FOL. % 149.53/21.76 % (2584291)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=421186299:cts=off:i=19910:ep=RS_2893 on theBenchmark for (2893ds/19910Mi) % 149.53/21.76 % (2584291)Refutation not found, incomplete strategy % 149.53/21.76 % (2584291)------------------------------ % 149.53/21.76 % (2584291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.53/21.76 % (2584291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.53/21.76 % (2584291)CaDiCaL version: 2.1.3 % 149.53/21.76 % (2584291)Termination reason: Refutation not found, incomplete strategy % 149.53/21.76 % (2584291)Time elapsed: 0.009 s % 149.53/21.76 % (2584291)Peak memory usage: 88 MB % 149.53/21.76 % (2584291)Instructions burned: 16 (million) % 149.53/21.76 % Exception at run slice level % 149.53/21.76 User error: GNN currently only supports monomorphic FOL. % 149.53/21.76 % (2584292)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=3281466230:i=20312:bd=preordered:fsr=off:er=filter_2893 on theBenchmark for (2893ds/20312Mi) % 149.53/21.76 % Exception at run slice level % 149.53/21.76 User error: GNN currently only supports monomorphic FOL. % 149.53/21.76 % (2584295)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=1888308238:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2891 on theBenchmark for (2891ds/13822Mi) % 149.53/21.76 % (2584291)------------------------------ % 149.53/21.76 % (2584291)------------------------------ % 149.53/21.76 % (2584296)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=330725692:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2890 on theBenchmark for (2890ds/7144Mi) % 149.53/21.76 % Exception at run slice level % 149.53/21.76 User error: GNN currently only supports monomorphic FOL. % 149.53/21.76 % (2584299)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=609745288:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2889 on theBenchmark for (2889ds/15184Mi) % 149.53/21.76 % Exception at run slice level % 149.53/21.76 User error: GNN currently only supports monomorphic FOL. % 149.53/21.76 % (2584300)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=2404838327:i=107375_2887 on theBenchmark for (2887ds/107375Mi) % 149.53/21.76 % (2584303)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=3044480270:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2886 on theBenchmark for (2886ds/7958Mi) % 149.53/21.76 % Exception at run slice level % 149.53/21.76 User error: GNN currently only supports monomorphic FOL. % 149.53/21.76 % Exception at run slice level % 149.53/21.76 User error: GNN currently only supports monomorphic FOL. % 149.53/21.76 % (2584305)dis+10_128_sil=16000:nwc=0.7:random_seed=838126741:i=15999:nm=2:gsp=on_2883 on theBenchmark for (2883ds/15999Mi) % 149.53/21.76 % (2584305)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 149.53/21.76 % Exception at run slice level % 149.53/21.76 User error: GNN currently only supports monomorphic FOL. % 149.53/21.76 % (2584306)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=1434700574:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2882 on theBenchmark for (2882ds/8139Mi) % 149.53/21.76 % (2584308)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=3212326739:st=4:i=8950:sd=5:ss=axioms_2881 on theBenchmark for (2881ds/8950Mi) % 149.53/21.76 % Exception at run slice level % 149.53/21.76 User error: GNN currently only supports monomorphic FOL. % 149.53/21.76 % (2584311)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=3224917079:i=9809:ins=10:av=off_2875 on theBenchmark for (2875ds/9809Mi) % 149.53/21.76 % Exception at run slice level % 149.53/21.76 User error: GNN currently only supports monomorphic FOL. % 149.53/21.76 % (2584199)Instruction limit reached! % 149.53/21.76 % (2584199)------------------------------ % 149.53/21.76 % (2584199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.49/27.11 % (2584199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.49/27.11 % (2584199)CaDiCaL version: 2.1.3 % 187.49/27.11 % (2584199)Termination reason: Instruction limit % 187.49/27.11 % (2584199)Termination phase: Saturation % 187.49/27.11 % (2584199)Time elapsed: 7.969 s % 187.49/27.11 % (2584199)Peak memory usage: 483 MB % 187.49/27.11 % (2584199)Instructions burned: 26477 (million) % 187.49/27.11 % (2584313)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=2957427981:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2870 on theBenchmark for (2870ds/9885Mi) % 187.49/27.11 % (2584314)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=1959766324:cond=fast:i=32078:fgj=on:av=off_2869 on theBenchmark for (2869ds/32078Mi) % 187.49/27.11 % Exception at run slice level % 187.49/27.11 User error: GNN currently only supports monomorphic FOL. % 187.49/27.11 % Exception at run slice level % 187.49/27.11 User error: GNN currently only supports monomorphic FOL. % 187.49/27.11 % (2584317)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=256245985:i=11101:bd=all:ss=axioms:sgt=8_2866 on theBenchmark for (2866ds/11101Mi) % 187.49/27.11 % (2584318)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=1683947045:cond=on:i=13220:s2at=3:aac=none:fsd=on_2865 on theBenchmark for (2865ds/13220Mi) % 187.49/27.11 % Exception at run slice level % 187.49/27.11 User error: GNN currently only supports monomorphic FOL. % 187.49/27.11 % (2584321)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=3120629571:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2860 on theBenchmark for (2860ds/13528Mi) % 187.49/27.11 % Exception at run slice level % 187.49/27.11 User error: GNN currently only supports monomorphic FOL. % 187.49/27.11 % (2584323)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=3360905525:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2854 on theBenchmark for (2854ds/14854Mi) % 187.49/27.11 % Exception at run slice level % 187.49/27.11 User error: GNN currently only supports monomorphic FOL. % 187.49/27.11 % (2584325)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=1278954399:i=14974:ss=axioms:sgt=16_2849 on theBenchmark for (2849ds/14974Mi) % 187.49/27.11 % (2584296)Instruction limit reached! % 187.49/27.11 % (2584296)------------------------------ % 187.49/27.11 % (2584296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.49/27.11 % (2584296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.49/27.11 % (2584296)CaDiCaL version: 2.1.3 % 187.49/27.11 % (2584296)Termination reason: Instruction limit % 187.49/27.11 % (2584296)Termination phase: Saturation % 187.49/27.11 % (2584296)Time elapsed: 4.285 s % 187.49/27.11 % (2584296)Peak memory usage: 130 MB % 187.49/27.11 % (2584296)Instructions burned: 7145 (million) % 187.49/27.11 % (2584327)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=521206854:i=33081:aac=none:fgj=on:bd=all:fsr=off_2846 on theBenchmark for (2846ds/33081Mi) % 187.49/27.11 % Exception at run slice level % 187.49/27.11 User error: GNN currently only supports monomorphic FOL. % 187.49/27.11 % (2584329)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=936263306:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2844 on theBenchmark for (2844ds/50856Mi) % 187.49/27.11 % Exception at run slice level % 187.49/27.11 User error: GNN currently only supports monomorphic FOL. % 187.49/27.11 % (2584306)Instruction limit reached! % 187.49/27.11 % (2584306)------------------------------ % 187.49/27.11 % (2584306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.49/27.11 % (2584306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.49/27.11 % (2584306)CaDiCaL version: 2.1.3 % 187.49/27.11 % (2584306)Termination reason: Instruction limit % 187.49/27.11 % (2584306)Termination phase: Saturation % 187.49/27.11 % (2584306)Time elapsed: 4.002 s % 187.49/27.11 % (2584306)Peak memory usage: 111 MB % 187.49/27.11 % (2584306)Instructions burned: 8139 (million) % 187.49/27.11 % (2584331)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=2584970:i=69865_2841 on theBenchmark for (2841ds/69865Mi) % 197.75/28.59 % (2584332)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=2401253827:cond=fast:i=17802:gtgl=3:gtg=all_2840 on theBenchmark for (2840ds/17802Mi) % 197.75/28.59 % Exception at run slice level % 197.75/28.59 User error: Immediate (shared) subterms of term/literal aa(X2,X0,combb(X1,X0,X2,X5,X4),X3) = sF20(X2,X0,X1,X5,X4,X3) have different types/not well-typed! % 197.75/28.59 % Exception at run slice level % 197.75/28.59 User error: GNN currently only supports monomorphic FOL. % 197.75/28.59 % (2584335)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=23790160:i=96644_2839 on theBenchmark for (2839ds/96644Mi) % 197.75/28.59 % (2584336)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 197.75/28.59 % (2584336)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=475390439:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2839 on theBenchmark for (2839ds/21161Mi) % 197.75/28.59 % Exception at run slice level % 197.75/28.59 User error: GNN currently only supports monomorphic FOL. % 197.75/28.59 % (2584339)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=2506328047:i=22761:gtg=all:ss=axioms:fsd=on_2836 on theBenchmark for (2836ds/22761Mi) % 197.75/28.59 % Exception at run slice level % 197.75/28.59 User error: GNN currently only supports monomorphic FOL. % 197.75/28.59 % (2584341)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=4132519668:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2830 on theBenchmark for (2830ds/23713Mi) % 197.75/28.59 % (2584317)Instruction limit reached! % 197.75/28.59 % (2584317)------------------------------ % 197.75/28.59 % (2584317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.75/28.59 % (2584317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.75/28.59 % (2584317)CaDiCaL version: 2.1.3 % 197.75/28.59 % (2584317)Termination reason: Instruction limit % 197.75/28.59 % (2584317)Termination phase: Saturation % 197.75/28.59 % (2584317)Time elapsed: 3.729 s % 197.75/28.59 % (2584317)Peak memory usage: 133 MB % 197.75/28.59 % (2584317)Instructions burned: 11101 (million) % 197.75/28.59 % (2584343)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=2416821178:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2827 on theBenchmark for (2827ds/26509Mi) % 197.75/28.59 % Exception at run slice level % 197.75/28.59 User error: GNN currently only supports monomorphic FOL. % 197.75/28.59 % (2584345)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=3022166221:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2824 on theBenchmark for (2824ds/28957Mi) % 197.75/28.59 % (2584305)Instruction limit reached! % 197.75/28.59 % (2584305)------------------------------ % 197.75/28.59 % (2584305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.75/28.59 % (2584305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.75/28.59 % (2584305)CaDiCaL version: 2.1.3 % 197.75/28.59 % (2584305)Termination reason: Instruction limit % 197.75/28.59 % (2584305)Termination phase: Saturation % 197.75/28.59 % (2584305)Time elapsed: 8.611 s % 197.75/28.59 % (2584305)Peak memory usage: 135 MB % 197.75/28.59 % (2584305)Instructions burned: 15999 (million) % 197.75/28.59 % (2584347)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=340493916:i=29246:s2at=-1:kws=inv_arity:ins=10_2796 on theBenchmark for (2796ds/29246Mi) % 197.75/28.59 % Exception at run slice level % 197.75/28.59 User error: GNN currently only supports monomorphic FOL. % 197.75/28.59 % (2584349)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=2540027075:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2790 on theBenchmark for (2790ds/30082Mi) % 197.75/28.59 % (2584349)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 203.23/29.30 % Exception at run slice level % 203.23/29.30 User error: GNN currently only supports monomorphic FOL. % 203.23/29.30 % (2584351)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=1208300595:i=32262:bd=preordered_2785 on theBenchmark for (2785ds/32262Mi) % 203.23/29.30 % Exception at run slice level % 203.23/29.30 User error: GNN currently only supports monomorphic FOL. % 203.23/29.30 % (2584353)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=2029035713:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2780 on theBenchmark for (2780ds/32870Mi) % 203.23/29.30 % Exception at run slice level % 203.23/29.30 User error: GNN currently only supports monomorphic FOL. % 203.23/29.30 % (2584355)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=863490008:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2774 on theBenchmark for (2774ds/33295Mi) % 203.23/29.30 % Exception at run slice level % 203.23/29.30 User error: GNN currently only supports monomorphic FOL. % 203.23/29.30 % (2584357)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=4220062196:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2769 on theBenchmark for (2769ds/36826Mi) % 203.23/29.30 % (2584171)Instruction limit reached! % 203.23/29.30 % (2584171)------------------------------ % 203.23/29.30 % (2584171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.23/29.30 % (2584171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.23/29.30 % (2584171)CaDiCaL version: 2.1.3 % 203.23/29.30 % (2584171)Termination reason: Instruction limit % 203.23/29.30 % (2584171)Termination phase: Saturation % 203.23/29.30 % (2584171)Time elapsed: 20.643 s % 203.23/29.30 % (2584171)Peak memory usage: 185 MB % 203.23/29.30 % (2584171)Instructions burned: 33334 (million) % 203.23/29.30 % (2584359)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=558409636:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2758 on theBenchmark for (2758ds/92981Mi) % 203.23/29.30 % Exception at run slice level % 203.23/29.30 User error: GNN currently only supports monomorphic FOL. % 203.23/29.30 % (2584361)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=1997853622:s2pl=on:i=49423_2753 on theBenchmark for (2753ds/49423Mi) % 203.23/29.30 % Exception at run slice level % 203.23/29.30 User error: GNN currently only supports monomorphic FOL. % 203.23/29.30 % (2584363)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=1738255052:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2747 on theBenchmark for (2747ds/57299Mi) % 203.23/29.30 % Exception at run slice level % 203.23/29.30 User error: GNN currently only supports monomorphic FOL. % 203.23/29.30 % (2584365)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=4191606490:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2742 on theBenchmark for (2742ds/127679Mi) % 203.23/29.30 % (2584345)Instruction limit reached! % 203.23/29.30 % (2584345)------------------------------ % 203.23/29.30 % (2584345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.23/29.30 % (2584345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.23/29.30 % (2584345)CaDiCaL version: 2.1.3 % 203.23/29.30 % (2584345)Termination reason: Instruction limit % 203.23/29.30 % (2584345)Termination phase: Saturation % 203.23/29.30 % (2584345)Time elapsed: 8.527 s % 203.23/29.30 % (2584345)Peak memory usage: 237 MB % 203.23/29.30 % (2584345)Instructions burned: 28959 (million) % 203.23/29.30 % Exception at run slice level % 203.23/29.30 User error: GNN currently only supports monomorphic FOL. % 203.23/29.30 % (2584367)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=1080013205:i=69402:add=on:aac=none:fsr=off_2737 on theBenchmark for (2737ds/69402Mi) % 203.23/29.30 % (2584368)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=1225299720:i=100512:doe=on:fgj=on:bd=all:fsd=on_2737 on theBenchmark for (2737ds/100512Mi) % 208.78/30.09 % Exception at run slice level % 208.78/30.09 User error: GNN currently only supports monomorphic FOL. % 208.78/30.09 % (2584371)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=2548989952:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2734 on theBenchmark for (2734ds/138761Mi) % 208.78/30.09 % Exception at run slice level % 208.78/30.09 User error: GNN currently only supports monomorphic FOL. % 208.78/30.09 % Exception at run slice level % 208.78/30.09 User error: GNN currently only supports monomorphic FOL. % 208.78/30.09 % (2584373)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=1949543684:i=282386:rtra=on_2731 on theBenchmark for (2731ds/282386Mi) % 208.78/30.09 % (2584374)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=904435900:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2731 on theBenchmark for (2731ds/269354Mi) % 208.78/30.09 % Exception at run slice level % 208.78/30.09 User error: GNN currently only supports monomorphic FOL. % 208.78/30.09 % (2584377)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=1795836784:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2728 on theBenchmark for (2728ds/283390Mi) % 208.78/30.09 % (2584377)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 208.78/30.09 % Exception at run slice level % 208.78/30.09 User error: GNN currently only supports monomorphic FOL. % 208.78/30.09 % (2584379)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=209537118:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2726 on theBenchmark for (2726ds/218Mi) % 208.78/30.09 % Exception at run slice level % 208.78/30.09 User error: GNN currently only supports monomorphic FOL. % 208.78/30.09 % (2584379)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 208.78/30.09 % (2584379)Refutation not found, incomplete strategy % 208.78/30.09 % (2584379)------------------------------ % 208.78/30.09 % (2584379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 208.78/30.09 % (2584379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.78/30.09 % (2584379)CaDiCaL version: 2.1.3 % 208.78/30.09 % (2584379)Termination reason: Refutation not found, incomplete strategy % 208.78/30.09 % (2584379)Time elapsed: 0.013 s % 208.78/30.09 % (2584379)Peak memory usage: 89 MB % 208.78/30.09 % (2584379)Instructions burned: 22 (million) % 208.78/30.09 % (2584381)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=1746047069:i=238:av=off:rtra=on:ss=axioms_2724 on theBenchmark for (2724ds/238Mi) % 208.78/30.09 % (2584381)Instruction limit reached! % 208.78/30.09 % (2584381)------------------------------ % 208.78/30.09 % (2584381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 208.78/30.09 % (2584381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.78/30.09 % (2584381)CaDiCaL version: 2.1.3 % 208.78/30.09 % (2584381)Termination reason: Instruction limit % 208.78/30.09 % (2584381)Termination phase: Saturation % 208.78/30.09 % (2584381)Time elapsed: 0.072 s % 208.78/30.09 % (2584381)Peak memory usage: 89 MB % 208.78/30.09 % (2584381)Instructions burned: 240 (million) % 208.78/30.09 % (2584379)------------------------------ % 208.78/30.09 % (2584379)------------------------------ % 208.78/30.09 % (2584383)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=4224442270:s2a=on:i=278:rtra=on:gtg=position_2722 on theBenchmark for (2722ds/278Mi) % 208.78/30.09 % (2584383)Instruction limit reached! % 208.78/30.09 % (2584383)------------------------------ % 208.78/30.09 % (2584383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 208.78/30.09 % (2584383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.78/30.09 % (2584383)CaDiCaL version: 2.1.3 % 208.78/30.09 % (2584383)Termination reason: Instruction limit % 208.78/30.09 % (2584383)Termination phase: Saturation % 208.78/30.09 % (2584383)Time elapsed: 0.087 s % 208.78/30.09 % (2584383)Peak memory usage: 90 MB % 208.78/30.09 % (2584383)Instructions burned: 279 (million) % 208.78/30.09 % (2584384)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=3033889432:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2722 on theBenchmark for (2722ds/258Mi) % 214.42/30.99 % (2584336)Instruction limit reached! % 214.42/30.99 % (2584336)------------------------------ % 214.42/30.99 % (2584336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.42/30.99 % (2584336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.42/30.99 % (2584336)CaDiCaL version: 2.1.3 % 214.42/30.99 % (2584336)Termination reason: Instruction limit % 214.42/30.99 % (2584336)Termination phase: Saturation % 214.42/30.99 % (2584336)Time elapsed: 11.784 s % 214.42/30.99 % (2584336)Peak memory usage: 196 MB % 214.42/30.99 % (2584336)Instructions burned: 21162 (million) % 214.42/30.99 % (2584386)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=467047132:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2720 on theBenchmark for (2720ds/570Mi) % 214.42/30.99 % (2584384)Instruction limit reached! % 214.42/30.99 % (2584384)------------------------------ % 214.42/30.99 % (2584384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.42/30.99 % (2584384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.42/30.99 % (2584384)CaDiCaL version: 2.1.3 % 214.42/30.99 % (2584384)Termination reason: Instruction limit % 214.42/30.99 % (2584384)Termination phase: Saturation % 214.42/30.99 % (2584384)Time elapsed: 0.140 s % 214.42/30.99 % (2584384)Peak memory usage: 90 MB % 214.42/30.99 % (2584384)Instructions burned: 260 (million) % 214.42/30.99 % (2584389)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=418491824:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2719 on theBenchmark for (2719ds/314Mi) % 214.42/30.99 % (2584390)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=930255924:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2719 on theBenchmark for (2719ds/650Mi) % 214.42/30.99 % (2584386)Instruction limit reached! % 214.42/30.99 % (2584386)------------------------------ % 214.42/30.99 % (2584386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.42/30.99 % (2584386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.42/30.99 % (2584386)CaDiCaL version: 2.1.3 % 214.42/30.99 % (2584386)Termination reason: Instruction limit % 214.42/30.99 % (2584386)Termination phase: Saturation % 214.42/30.99 % (2584386)Time elapsed: 0.190 s % 214.42/30.99 % (2584386)Peak memory usage: 92 MB % 214.42/30.99 % (2584386)Instructions burned: 575 (million) % 214.42/30.99 % (2584389)Instruction limit reached! % 214.42/30.99 % (2584389)------------------------------ % 214.42/30.99 % (2584389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.42/30.99 % (2584389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.42/30.99 % (2584389)CaDiCaL version: 2.1.3 % 214.42/30.99 % (2584389)Termination reason: Instruction limit % 214.42/30.99 % (2584389)Termination phase: Saturation % 214.42/30.99 % (2584389)Time elapsed: 0.158 s % 214.42/30.99 % (2584389)Peak memory usage: 91 MB % 214.42/30.99 % (2584389)Instructions burned: 315 (million) % 214.42/30.99 % (2584393)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=2295776755:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2717 on theBenchmark for (2717ds/496Mi) % 214.42/30.99 % (2584394)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=2733509883:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2716 on theBenchmark for (2716ds/588Mi) % 214.42/30.99 % (2584394)Refutation not found, incomplete strategy % 214.42/30.99 % (2584394)------------------------------ % 214.42/30.99 % (2584394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.42/30.99 % (2584394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.42/30.99 % (2584394)CaDiCaL version: 2.1.3 % 214.42/30.99 % (2584394)Termination reason: Refutation not found, incomplete strategy % 214.42/30.99 % (2584394)Time elapsed: 0.011 s % 214.42/30.99 % (2584394)Peak memory usage: 89 MB % 214.42/30.99 % (2584394)Instructions burned: 19 (million) % 214.42/30.99 % (2584393)Instruction limit reached! % 214.42/30.99 % (2584393)------------------------------ % 214.42/30.99 % (2584393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.42/30.99 % (2584393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.42/30.99 % (2584393)CaDiCaL version: 2.1.3 % 214.42/30.99 % (2584393)Termination reason: Instruction limit % 214.42/30.99 % (2584393)Termination phase: Saturation % 214.42/30.99 % (2584393)Time elapsed: 0.151 s % 214.42/30.99 % (2584393)Peak memory usage: 93 MB % 214.42/30.99 % (2584393)Instructions burned: 500 (million) % 214.42/30.99 % (2584390)Instruction limit reached! % 214.42/30.99 % (2584390)------------------------------ % 219.28/31.61 % (2584390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.28/31.61 % (2584390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.28/31.61 % (2584390)CaDiCaL version: 2.1.3 % 219.28/31.61 % (2584390)Termination reason: Instruction limit % 219.28/31.61 % (2584390)Termination phase: Saturation % 219.28/31.61 % (2584390)Time elapsed: 0.405 s % 219.28/31.61 % (2584390)Peak memory usage: 94 MB % 219.28/31.61 % (2584390)Instructions burned: 651 (million) % 219.28/31.61 % (2584397)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=3900492891:i=4700:rtra=on_2714 on theBenchmark for (2714ds/4700Mi) % 219.28/31.61 % (2584394)------------------------------ % 219.28/31.61 % (2584394)------------------------------ % 219.28/31.61 % (2584398)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1684591626:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2713 on theBenchmark for (2713ds/226Mi) % 219.28/31.61 % Exception at run slice level % 219.28/31.61 User error: GNN currently only supports monomorphic FOL. % 219.28/31.61 % (2584398)Instruction limit reached! % 219.28/31.61 % (2584398)------------------------------ % 219.28/31.61 % (2584398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.28/31.61 % (2584398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.28/31.61 % (2584398)CaDiCaL version: 2.1.3 % 219.28/31.61 % (2584398)Termination reason: Instruction limit % 219.28/31.61 % (2584398)Termination phase: Saturation % 219.28/31.61 % (2584398)Time elapsed: 0.131 s % 219.28/31.61 % (2584398)Peak memory usage: 90 MB % 219.28/31.61 % (2584398)Instructions burned: 227 (million) % 219.28/31.61 % (2584400)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3164409399:i=254:av=off:fsr=off:rtra=on:sup=off_2712 on theBenchmark for (2712ds/254Mi) % 219.28/31.61 % (2584400)Refutation not found, incomplete strategy % 219.28/31.61 % (2584400)------------------------------ % 219.28/31.61 % (2584400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.28/31.61 % (2584400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.28/31.61 % (2584400)CaDiCaL version: 2.1.3 % 219.28/31.61 % (2584400)Termination reason: Refutation not found, incomplete strategy % 219.28/31.61 % (2584400)Time elapsed: 0.006 s % 219.28/31.61 % (2584400)Peak memory usage: 88 MB % 219.28/31.61 % (2584400)Instructions burned: 10 (million) % 219.28/31.61 % (2584402)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=2004239458:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2711 on theBenchmark for (2711ds/228Mi) % 219.28/31.61 % (2584402)Instruction limit reached! % 219.28/31.61 % (2584402)------------------------------ % 219.28/31.61 % (2584402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.28/31.61 % (2584402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.28/31.61 % (2584402)CaDiCaL version: 2.1.3 % 219.28/31.61 % (2584402)Termination reason: Instruction limit % 219.28/31.61 % (2584402)Termination phase: Saturation % 219.28/31.61 % (2584402)Time elapsed: 0.056 s % 219.28/31.61 % (2584402)Peak memory usage: 89 MB % 219.28/31.61 % (2584402)Instructions burned: 231 (million) % 219.28/31.61 % (2584403)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=1196809532:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2710 on theBenchmark for (2710ds/1814Mi) % 219.28/31.61 % (2584406)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=1285112484:i=874:sd=1:aac=none:rtra=on:ss=included_2709 on theBenchmark for (2709ds/874Mi) % 219.28/31.61 % (2584406)Refutation not found, incomplete strategy % 219.28/31.61 % (2584406)------------------------------ % 219.28/31.61 % (2584406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.28/31.61 % (2584406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.28/31.61 % (2584406)CaDiCaL version: 2.1.3 % 219.28/31.61 % (2584406)Termination reason: Refutation not found, incomplete strategy % 219.28/31.61 % (2584406)Time elapsed: 0.006 s % 219.28/31.61 % (2584406)Peak memory usage: 89 MB % 219.28/31.61 % (2584406)Instructions burned: 19 (million) % 219.28/31.61 % (2584400)------------------------------ % 219.28/31.61 % (2584400)------------------------------ % 219.28/31.61 % (2584406)------------------------------ % 219.28/31.61 % (2584406)------------------------------ % 219.28/31.61 % (2584409)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=3810008048:i=10404:rtra=on:ss=axioms:sgt=16_2707 on theBenchmark for (2707ds/10404Mi) % 219.28/31.61 % (2584410)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3884768435:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2706 on theBenchmark for (2706ds/268Mi) % 224.57/32.37 % (2584410)Instruction limit reached! % 224.57/32.37 % (2584410)------------------------------ % 224.57/32.37 % (2584410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.57/32.37 % (2584410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.57/32.37 % (2584410)CaDiCaL version: 2.1.3 % 224.57/32.37 % (2584410)Termination reason: Instruction limit % 224.57/32.37 % (2584410)Termination phase: Saturation % 224.57/32.37 % (2584410)Time elapsed: 0.076 s % 224.57/32.37 % (2584410)Peak memory usage: 92 MB % 224.57/32.37 % (2584410)Instructions burned: 269 (million) % 224.57/32.37 % (2584413)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=3290906953:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2704 on theBenchmark for (2704ds/1184Mi) % 224.57/32.37 % Exception at run slice level % 224.57/32.37 User error: GNN currently only supports monomorphic FOL. % 224.57/32.37 % (2584413)Instruction limit reached! % 224.57/32.37 % (2584413)------------------------------ % 224.57/32.37 % (2584413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.57/32.37 % (2584413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.57/32.37 % (2584413)CaDiCaL version: 2.1.3 % 224.57/32.37 % (2584413)Termination reason: Instruction limit % 224.57/32.37 % (2584413)Termination phase: Saturation % 224.57/32.37 % (2584413)Time elapsed: 0.257 s % 224.57/32.37 % (2584413)Peak memory usage: 91 MB % 224.57/32.37 % (2584413)Instructions burned: 1184 (million) % 224.57/32.37 % (2584415)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=494534469:st=3:i=26386:sd=3:rtra=on:ss=axioms_2702 on theBenchmark for (2702ds/26386Mi) % 224.57/32.37 % (2584416)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=3772398932:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2701 on theBenchmark for (2701ds/250Mi) % 224.57/32.37 % (2584416)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 224.57/32.37 % (2584416)Instruction limit reached! % 224.57/32.37 % (2584416)------------------------------ % 224.57/32.37 % (2584416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.57/32.37 % (2584416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.57/32.37 % (2584416)CaDiCaL version: 2.1.3 % 224.57/32.37 % (2584416)Termination reason: Instruction limit % 224.57/32.37 % (2584416)Termination phase: Saturation % 224.57/32.37 % (2584416)Time elapsed: 0.072 s % 224.57/32.37 % (2584416)Peak memory usage: 91 MB % 224.57/32.37 % (2584416)Instructions burned: 251 (million) % 224.57/32.37 % (2584419)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=3264969214:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2699 on theBenchmark for (2699ds/268Mi) % 224.57/32.37 % Exception at run slice level % 224.57/32.37 User error: Immediate (shared) subterms of term/literal aa(X2,X0,combs(X2,X1,X0,X5,X4),X3) = sF45(X2,X0,X1,X5,X4,X3) have different types/not well-typed! % 224.57/32.37 % (2584403)Instruction limit reached! % 224.57/32.37 % (2584403)------------------------------ % 224.57/32.37 % (2584403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.57/32.37 % (2584403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.57/32.37 % (2584403)CaDiCaL version: 2.1.3 % 224.57/32.37 % (2584403)Termination reason: Instruction limit % 224.57/32.37 % (2584403)Termination phase: Saturation % 224.57/32.37 % (2584403)Time elapsed: 1.142 s % 224.57/32.37 % (2584403)Peak memory usage: 100 MB % 224.57/32.37 % (2584403)Instructions burned: 1815 (million) % 224.57/32.37 % Exception at run slice level % 224.57/32.37 User error: GNN currently only supports monomorphic FOL. % 224.57/32.37 % (2584421)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=174785604:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2697 on theBenchmark for (2697ds/282Mi) % 224.57/32.37 % (2584421)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 224.57/32.37 % (2584421)Refutation not found, incomplete strategy % 224.57/32.37 % (2584421)------------------------------ % 224.57/32.37 % (2584421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.57/32.37 % (2584421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.05/34.06 % (2584421)CaDiCaL version: 2.1.3 % 237.05/34.06 % (2584421)Termination reason: Refutation not found, incomplete strategy % 237.05/34.06 % (2584421)Time elapsed: 0.003 s % 237.05/34.06 % (2584421)Peak memory usage: 88 MB % 237.05/34.06 % (2584421)Instructions burned: 8 (million) % 237.05/34.06 % (2584422)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=1969702444:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2697 on theBenchmark for (2697ds/862Mi) % 237.05/34.06 % (2584341)Instruction limit reached! % 237.05/34.06 % (2584341)------------------------------ % 237.05/34.06 % (2584341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.05/34.06 % (2584341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.05/34.06 % (2584341)CaDiCaL version: 2.1.3 % 237.05/34.06 % (2584341)Termination reason: Instruction limit % 237.05/34.06 % (2584341)Termination phase: Saturation % 237.05/34.06 % (2584341)Time elapsed: 13.332 s % 237.05/34.06 % (2584341)Peak memory usage: 138 MB % 237.05/34.06 % (2584341)Instructions burned: 23715 (million) % 237.05/34.06 % (2584423)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=3084145910:i=12120:aac=none:ins=25:rtra=on_2697 on theBenchmark for (2697ds/12120Mi) % 237.05/34.06 % (2584421)------------------------------ % 237.05/34.06 % (2584421)------------------------------ % 237.05/34.06 % (2584426)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=3763827046:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2695 on theBenchmark for (2695ds/300Mi) % 237.05/34.06 % (2584426)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 237.05/34.06 % (2584428)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=1961823237:i=28310:bd=all:rtra=on_2695 on theBenchmark for (2695ds/28310Mi) % 237.05/34.06 % (2584426)Instruction limit reached! % 237.05/34.06 % (2584426)------------------------------ % 237.05/34.06 % (2584426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.05/34.06 % (2584426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.05/34.06 % (2584426)CaDiCaL version: 2.1.3 % 237.05/34.06 % (2584426)Termination reason: Instruction limit % 237.05/34.06 % (2584426)Termination phase: Saturation % 237.05/34.06 % (2584426)Time elapsed: 0.180 s % 237.05/34.06 % (2584426)Peak memory usage: 92 MB % 237.05/34.06 % (2584426)Instructions burned: 300 (million) % 237.05/34.06 % (2584422)Instruction limit reached! % 237.05/34.06 % (2584422)------------------------------ % 237.05/34.06 % (2584422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.05/34.06 % (2584422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.05/34.06 % (2584422)CaDiCaL version: 2.1.3 % 237.05/34.06 % (2584422)Termination reason: Instruction limit % 237.05/34.06 % (2584422)Termination phase: Saturation % 237.05/34.06 % (2584422)Time elapsed: 0.392 s % 237.05/34.06 % (2584422)Peak memory usage: 93 MB % 237.05/34.06 % (2584422)Instructions burned: 863 (million) % 237.05/34.06 % Exception at run slice level % 237.05/34.06 User error: GNN currently only supports monomorphic FOL. % 237.05/34.06 % Exception at run slice level % 237.05/34.06 User error: GNN currently only supports monomorphic FOL. % 237.05/34.06 % (2584431)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3343951770:i=1334:av=off:fsr=off:rtra=on_2692 on theBenchmark for (2692ds/1334Mi) % 237.05/34.06 % (2584433)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=161500775:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2692 on theBenchmark for (2692ds/386Mi) % 237.05/34.06 % (2584431)Refutation not found, incomplete strategy % 237.05/34.06 % (2584431)------------------------------ % 237.05/34.06 % (2584431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.05/34.06 % (2584431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.05/34.06 % (2584431)CaDiCaL version: 2.1.3 % 237.05/34.06 % (2584431)Termination reason: Refutation not found, incomplete strategy % 237.05/34.06 % (2584431)Time elapsed: 0.011 s % 237.05/34.06 % (2584431)Peak memory usage: 89 MB % 237.05/34.06 % (2584431)Instructions burned: 19 (million) % 237.05/34.06 % (2584432)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=1595547044:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2692 on theBenchmark for (2692ds/370Mi) % 251.22/36.06 % (2584434)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=364943584:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2692 on theBenchmark for (2692ds/9700Mi) % 251.22/36.06 % (2584434)Refutation not found, incomplete strategy % 251.22/36.06 % (2584434)------------------------------ % 251.22/36.06 % (2584434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.22/36.06 % (2584434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.22/36.06 % (2584434)CaDiCaL version: 2.1.3 % 251.22/36.06 % (2584434)Termination reason: Refutation not found, incomplete strategy % 251.22/36.06 % (2584434)Time elapsed: 0.008 s % 251.22/36.06 % (2584434)Peak memory usage: 88 MB % 251.22/36.06 % (2584434)Instructions burned: 14 (million) % 251.22/36.06 % (2584433)Instruction limit reached! % 251.22/36.06 % (2584433)------------------------------ % 251.22/36.06 % (2584433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.22/36.06 % (2584433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.22/36.06 % (2584433)CaDiCaL version: 2.1.3 % 251.22/36.06 % (2584433)Termination reason: Instruction limit % 251.22/36.06 % (2584433)Termination phase: Saturation % 251.22/36.06 % (2584433)Time elapsed: 0.129 s % 251.22/36.06 % (2584433)Peak memory usage: 93 MB % 251.22/36.06 % (2584433)Instructions burned: 389 (million) % 251.22/36.06 % (2584431)------------------------------ % 251.22/36.06 % (2584431)------------------------------ % 251.22/36.06 % (2584439)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=2576403568:i=24222:sd=1:rtra=on:ss=included_2689 on theBenchmark for (2689ds/24222Mi) % 251.22/36.06 % (2584432)Instruction limit reached! % 251.22/36.06 % (2584432)------------------------------ % 251.22/36.06 % (2584432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.22/36.06 % (2584432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.22/36.06 % (2584432)CaDiCaL version: 2.1.3 % 251.22/36.06 % (2584432)Termination reason: Instruction limit % 251.22/36.06 % (2584432)Termination phase: Saturation % 251.22/36.06 % (2584432)Time elapsed: 0.231 s % 251.22/36.06 % (2584432)Peak memory usage: 92 MB % 251.22/36.06 % (2584432)Instructions burned: 371 (million) % 251.22/36.06 % (2584434)------------------------------ % 251.22/36.06 % (2584434)------------------------------ % 251.22/36.06 % (2584440)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=1810319695:i=638:kws=precedence:fsr=off:rtra=on_2688 on theBenchmark for (2688ds/638Mi) % 251.22/36.06 % (2584442)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=20216144:i=4128:ep=RST:rtra=on_2688 on theBenchmark for (2688ds/4128Mi) % 251.22/36.06 % Exception at run slice level % 251.22/36.06 User error: GNN currently only supports monomorphic FOL. % 251.22/36.06 % (2584443)dis-1011_128_sil=32000:si=on:random_seed=1099107168:i=7412:ep=RST:av=off:rtra=on_2687 on theBenchmark for (2687ds/7412Mi) % 251.22/36.06 % (2584446)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3120493606:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2686 on theBenchmark for (2686ds/1514Mi) % 251.22/36.06 % (2584446)Refutation not found, incomplete strategy % 251.22/36.06 % (2584446)------------------------------ % 251.22/36.06 % (2584446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.22/36.06 % (2584446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.22/36.06 % (2584446)CaDiCaL version: 2.1.3 % 251.22/36.06 % (2584446)Termination reason: Refutation not found, incomplete strategy % 251.22/36.06 % (2584446)Time elapsed: 0.005 s % 251.22/36.06 % (2584446)Peak memory usage: 89 MB % 251.22/36.06 % (2584446)Instructions burned: 16 (million) % 251.22/36.06 % (2584440)Instruction limit reached! % 251.22/36.06 % (2584440)------------------------------ % 251.22/36.06 % (2584440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.22/36.06 % (2584440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.22/36.06 % (2584440)CaDiCaL version: 2.1.3 % 251.22/36.06 % (2584440)Termination reason: Instruction limit % 251.22/36.06 % (2584440)Termination phase: Saturation % 251.22/36.06 % (2584440)Time elapsed: 0.374 s % 251.22/36.06 % (2584440)Peak memory usage: 93 MB % 251.22/36.06 % (2584440)Instructions burned: 639 (million) % 251.22/36.06 % (2584446)------------------------------ % 251.22/36.06 % (2584446)------------------------------ % 266.51/38.24 % (2584449)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=3136937830:i=27826:rtra=on:ss=axioms:sgt=8_2683 on theBenchmark for (2683ds/27826Mi) % 266.51/38.24 % (2584450)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=4037971657:i=19850:aac=none:rtra=on_2682 on theBenchmark for (2682ds/19850Mi) % 266.51/38.24 % Exception at run slice level % 266.51/38.24 User error: GNN currently only supports monomorphic FOL. % 266.51/38.24 % (2584453)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4059345796:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2679 on theBenchmark for (2679ds/4958Mi) % 266.51/38.24 % (2584453)Refutation not found, incomplete strategy % 266.51/38.24 % (2584453)------------------------------ % 266.51/38.24 % (2584453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.51/38.24 % (2584453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.51/38.24 % (2584453)CaDiCaL version: 2.1.3 % 266.51/38.24 % (2584453)Termination reason: Refutation not found, incomplete strategy % 266.51/38.24 % (2584453)Time elapsed: 0.006 s % 266.51/38.24 % (2584453)Peak memory usage: 89 MB % 266.51/38.24 % (2584453)Instructions burned: 18 (million) % 266.51/38.24 % Exception at run slice level % 266.51/38.24 User error: GNN currently only supports monomorphic FOL. % 266.51/38.24 % (2584453)------------------------------ % 266.51/38.24 % (2584453)------------------------------ % 266.51/38.24 % (2584455)ott+1002_64_sil=16000:si=on:sp=const_min:nwc=0.5:random_seed=1697563427:i=880:nm=2:av=off:rtra=on:gtg=exists_all:fdi=8:gsp=on_2678 on theBenchmark for (2678ds/880Mi) % 266.51/38.24 % (2584455)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 266.51/38.24 % (2584456)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=1941692387:st=1.5:i=22290:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2676 on theBenchmark for (2676ds/22290Mi) % 266.51/38.24 % Exception at run slice level % 266.51/38.24 User error: GNN currently only supports monomorphic FOL. % 266.51/38.24 % (2584459)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=3656313839:cts=off:i=6068:av=off:rtra=on:er=known:fsd=on_2673 on theBenchmark for (2673ds/6068Mi) % 266.51/38.24 % (2584455)Instruction limit reached! % 266.51/38.24 % (2584455)------------------------------ % 266.51/38.24 % (2584455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.51/38.24 % (2584455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.51/38.24 % (2584455)CaDiCaL version: 2.1.3 % 266.51/38.24 % (2584455)Termination reason: Instruction limit % 266.51/38.24 % (2584455)Termination phase: Saturation % 266.51/38.24 % (2584455)Time elapsed: 0.496 s % 266.51/38.24 % (2584455)Peak memory usage: 94 MB % 266.51/38.24 % (2584455)Instructions burned: 881 (million) % 266.51/38.24 % (2584442)Instruction limit reached! % 266.51/38.24 % (2584442)------------------------------ % 266.51/38.24 % (2584442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.51/38.24 % (2584442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.51/38.24 % (2584442)CaDiCaL version: 2.1.3 % 266.51/38.24 % (2584442)Termination reason: Instruction limit % 266.51/38.24 % (2584442)Termination phase: Saturation % 266.51/38.24 % (2584442)Time elapsed: 1.611 s % 266.51/38.24 % (2584442)Peak memory usage: 92 MB % 266.51/38.24 % (2584442)Instructions burned: 4129 (million) % 266.51/38.24 % Exception at run slice level % 266.51/38.24 User error: GNN currently only supports monomorphic FOL. % 266.51/38.24 % (2584461)lrs-1011_64:1_sil=8000:si=on:erd=off:urr=on:nwc=0.7:br=off:random_seed=2196485326:st=2:s2a=on:i=1048:s2at=2:rtra=on:ss=axioms_2671 on theBenchmark for (2671ds/1048Mi) % 266.51/38.24 % (2584463)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:si=on:s2agt=16:random_seed=2671385184:i=28246:bd=preordered:ins=4:rtra=on_2670 on theBenchmark for (2670ds/28246Mi) % 266.51/38.24 % (2584462)lrs+1011_16:1_sil=8000:si=on:acc=on:urr=on:fd=preordered:flr=on:random_seed=3935929212:avsq=on:i=2032:avsqr=676809,524288:sd=1:rtra=on:ss=axioms_2670 on theBenchmark for (2670ds/2032Mi) % 266.51/38.24 % Exception at run slice level % 266.51/38.24 User error: GNN currently only supports monomorphic FOL. % 266.51/38.24 % (2584467)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:si=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2479402933:i=11562:kws=precedence:bd=all:rtra=on:rawr=on_2667 on theBenchmark for (2667ds/11562Mi) % 276.57/39.79 % (2584461)Instruction limit reached! % 276.57/39.79 % (2584461)------------------------------ % 276.57/39.79 % (2584461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.57/39.79 % (2584462)Instruction limit reached! % 276.57/39.79 % (2584462)------------------------------ % 276.57/39.79 % (2584462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.57/39.79 % (2584462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.57/39.79 % (2584462)CaDiCaL version: 2.1.3 % 276.57/39.79 % (2584462)Termination reason: Instruction limit % 276.57/39.79 % (2584462)Termination phase: Saturation % 276.57/39.79 % (2584462)Time elapsed: 1.104 s % 276.57/39.79 % (2584462)Peak memory usage: 106 MB % 276.57/39.79 % (2584462)Instructions burned: 2160 (million) % 276.57/39.79 % (2584461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.57/39.79 % (2584461)CaDiCaL version: 2.1.3 % 276.57/39.79 % (2584461)Termination reason: Instruction limit % 276.57/39.79 % (2584461)Termination phase: Saturation % 276.57/39.79 % (2584461)Time elapsed: 1.177 s % 276.57/39.79 % (2584461)Peak memory usage: 103 MB % 276.57/39.79 % (2584461)Instructions burned: 2133 (million) % 276.57/39.79 % (2584443)Instruction limit reached! % 276.57/39.79 % (2584443)------------------------------ % 276.57/39.79 % (2584443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.57/39.79 % (2584443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.57/39.79 % (2584443)CaDiCaL version: 2.1.3 % 276.57/39.79 % (2584443)Termination reason: Instruction limit % 276.57/39.79 % (2584443)Termination phase: Saturation % 276.57/39.79 % (2584443)Time elapsed: 2.841 s % 276.57/39.79 % (2584443)Peak memory usage: 91 MB % 276.57/39.79 % (2584443)Instructions burned: 7414 (million) % 276.57/39.79 % (2584469)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:si=on:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=3386510821:i=4896:gtgl=5:bd=preordered:rtra=on:gtg=all_2658 on theBenchmark for (2658ds/4896Mi) % 276.57/39.79 % (2584470)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:si=on:lcm=reverse:random_seed=724209533:i=6446:kws=precedence:fgj=on:av=off:rtra=on_2658 on theBenchmark for (2658ds/6446Mi) % 276.57/39.79 % (2584471)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:si=on:sp=occurrence:sos=on:random_seed=2635161584:st=5.6:i=4066:sd=3:rtra=on:ss=axioms_2658 on theBenchmark for (2658ds/4066Mi) % 276.57/39.79 % Exception at run slice level % 276.57/39.79 User error: GNN currently only supports monomorphic FOL. % 276.57/39.79 % Exception at run slice level % 276.57/39.79 User error: GNN currently only supports monomorphic FOL. % 276.57/39.79 % Exception at run slice level % 276.57/39.79 User error: GNN currently only supports monomorphic FOL. % 276.57/39.79 % (2584475)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:si=on:random_seed=1213276716:i=4110:nm=16:rtra=on:gtg=position:ss=axioms:fsd=on_2652 on theBenchmark for (2652ds/4110Mi) % 276.57/39.79 % (2584476)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:si=on:sp=const_frequency:spb=goal:acc=on:random_seed=1325255822:i=43222:sd=3:rtra=on:ss=axioms_2652 on theBenchmark for (2652ds/43222Mi) % 276.57/39.79 % (2584477)lrs+10_1_sil=8000:si=on:sp=occurrence:sos=all:lma=off:random_seed=2284128343:i=9670:sd=13:rtra=on:ss=axioms:sgt=23_2652 on theBenchmark for (2652ds/9670Mi) % 276.57/39.79 % Exception at run slice level % 276.57/39.79 User error: GNN currently only supports monomorphic FOL. % 276.57/39.79 % Exception at run slice level % 276.57/39.79 User error: GNN currently only supports monomorphic FOL. % 276.57/39.79 % (2584481)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:si=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=363343645:st=5:i=1594:s2at=3:sd=4:bs=unit_only:av=off:rtra=on:sup=off:ss=included_2647 on theBenchmark for (2647ds/1594Mi) % 276.57/39.79 % (2584482)lrs-1011_5_sil=8000:si=on:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2930254076:i=4652:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:rtra=on:fsd=on_2647 on theBenchmark for (2647ds/4652Mi) % 276.57/39.79 % (2584482)Refutation not found, incomplete strategy % 276.57/39.79 % (2584482)------------------------------ % 276.57/39.79 % (2584482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.80/42.06 % (2584482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.80/42.06 % (2584482)CaDiCaL version: 2.1.3 % 293.80/42.06 % (2584482)Termination reason: Refutation not found, incomplete strategy % 293.80/42.06 % (2584482)Time elapsed: 0.019 s % 293.80/42.06 % (2584482)Peak memory usage: 89 MB % 293.80/42.06 % (2584482)Instructions burned: 31 (million) % 293.80/42.06 % (2584482)------------------------------ % 293.80/42.06 % (2584482)------------------------------ % 293.80/42.06 % (2584267)Instruction limit reached! % 293.80/42.06 % (2584267)------------------------------ % 293.80/42.06 % (2584267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.80/42.06 % (2584267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.80/42.06 % (2584267)CaDiCaL version: 2.1.3 % 293.80/42.06 % (2584267)Termination reason: Instruction limit % 293.80/42.06 % (2584267)Termination phase: Saturation % 293.80/42.06 % (2584267)Time elapsed: 26.558 s % 293.80/42.06 % (2584267)Peak memory usage: 244 MB % 293.80/42.06 % (2584267)Instructions burned: 43697 (million) % 293.80/42.06 % (2584485)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:si=on:sos=all:urr=on:br=off:random_seed=3198253305:i=12076:nm=6:rtra=on_2643 on theBenchmark for (2643ds/12076Mi) % 293.80/42.06 % (2584487)lrs+10_1_sil=32000:si=on:sp=occurrence:random_seed=1711579034:st=2:i=66668:sd=3:rtra=on:ss=included:sgt=32_2641 on theBenchmark for (2641ds/66668Mi) % 293.80/42.06 % Exception at run slice level % 293.80/42.06 User error: GNN currently only supports monomorphic FOL. % 293.80/42.06 % (2584489)lrs+10_4_sil=8000:plsq=on:si=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3946064188:st=3.7:s2a=on:i=2016:s2at=1.2:sd=3:bd=all:av=off:rtra=on:fdi=8:sup=off:ss=axioms_2638 on theBenchmark for (2638ds/2016Mi) % 293.80/42.06 % (2584481)Instruction limit reached! % 293.80/42.06 % (2584481)------------------------------ % 293.80/42.06 % (2584481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.80/42.06 % (2584481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.80/42.06 % (2584481)CaDiCaL version: 2.1.3 % 293.80/42.06 % (2584481)Termination reason: Instruction limit % 293.80/42.06 % (2584481)Termination phase: Saturation % 293.80/42.06 % (2584481)Time elapsed: 0.996 s % 293.80/42.06 % (2584481)Peak memory usage: 99 MB % 293.80/42.06 % (2584481)Instructions burned: 1595 (million) % 293.80/42.06 % (2584491)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:si=on:sp=const_frequency:spb=intro:gs=on:random_seed=1554483526:i=16654:s2at=5:bd=preordered:rtra=on_2636 on theBenchmark for (2636ds/16654Mi) % 293.80/42.06 % Exception at run slice level % 293.80/42.06 User error: GNN currently only supports monomorphic FOL. % 293.80/42.06 % (2584493)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:si=on:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=811920611:s2a=on:i=2166:s2at=1.87328:slsql=off:ep=RSTC:rtra=on:fdi=16_2631 on theBenchmark for (2631ds/2166Mi) % 293.80/42.06 % (2584467)Instruction limit reached! % 293.80/42.06 % (2584467)------------------------------ % 293.80/42.06 % (2584467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.80/42.06 % (2584467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.80/42.06 % (2584467)CaDiCaL version: 2.1.3 % 293.80/42.06 % (2584467)Termination reason: Instruction limit % 293.80/42.06 % (2584467)Termination phase: Saturation % 293.80/42.06 % (2584467)Time elapsed: 3.717 s % 293.80/42.06 % (2584467)Peak memory usage: 120 MB % 293.80/42.06 % (2584467)Instructions burned: 11563 (million) % 293.80/42.06 % (2584495)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:si=on:spb=goal:fd=preordered:random_seed=469640005:i=2168:sd=1:bd=preordered:av=off:fsr=off:rtra=on:ss=axioms:sgt=14_2628 on theBenchmark for (2628ds/2168Mi) % 293.80/42.06 % (2584489)Instruction limit reached! % 293.80/42.06 % (2584489)------------------------------ % 293.80/42.06 % (2584489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.80/42.06 % (2584489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.80/42.06 % (2584489)CaDiCaL version: 2.1.3 % 293.80/42.06 % (2584489)Termination reason: Instruction limit % 293.80/42.06 % (2584489)Termination phase: Saturation % 293.80/42.06 % (2584489)Time elapsed: 1.097 s % 293.80/42.06 % (2584489)Peak memory usage: 107 MB % 293.80/42.06 % (2584489)Instructions burned: 2016 (million) % 293.80/42.06 % (2584497)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:si=on:erd=offTerminated %------------------------------------------------------------------------------