%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : COM073_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n012.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 09:39:31 AM UTC 2026 % Result : Timeout 300.39s 43.06s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : COM073_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.05/0.12 % Computer : n012.cluster.edu % 0.05/0.12 % Model : x86_64 x86_64 % 0.05/0.12 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.05/0.12 % Memory : 8046.5625MB % 0.05/0.12 % OS : Linux 6.8.0-71-generic % 0.05/0.12 % CPULimit : 300 % 0.05/0.12 % WCLimit : 300 % 0.05/0.12 % DateTime : Mon Sep 28 21:52:04 UTC 2026 % 0.05/0.12 % CPUTime : % 0.05/0.12 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.05/0.13 Running first-order theorem proving % 0.05/0.13 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 5.17/1.16 % (3818182)Detected formulas, will run a generic FOF schedule. % 5.17/1.16 % (3818188)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=4182287111:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 5.17/1.16 % (3818191)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1925715170:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 5.17/1.16 % (3818192)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1593367190:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 5.17/1.16 % (3818187)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=1568933689:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 5.17/1.16 % (3818189)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=295079465:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 5.17/1.16 % (3818190)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2755773844:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 5.17/1.16 % (3818193)dis-21_1_sil=8000:lcm=predicate:random_seed=3106315427:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 5.17/1.16 % (3818190)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.17/1.16 % (3818190)Refutation not found, incomplete strategy % 5.17/1.16 % (3818190)------------------------------ % 5.17/1.16 % (3818190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.17/1.16 % (3818190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.17/1.16 % (3818190)CaDiCaL version: 2.1.3 % 5.17/1.16 % (3818190)Termination reason: Refutation not found, incomplete strategy % 5.17/1.16 % (3818190)Time elapsed: 0.001 s % 5.17/1.16 % (3818190)Peak memory usage: 88 MB % 5.17/1.16 % (3818190)Instructions burned: 1 (million) % 5.17/1.16 % (3818189)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.17/1.16 % (3818191)Instruction limit reached! % 5.17/1.16 % (3818191)------------------------------ % 5.17/1.16 % (3818191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.17/1.16 % (3818191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.17/1.16 % (3818191)CaDiCaL version: 2.1.3 % 5.17/1.16 % (3818191)Termination reason: Instruction limit % 5.17/1.16 % (3818191)Termination phase: Saturation % 5.17/1.16 % (3818191)Time elapsed: 0.031 s % 5.17/1.16 % (3818191)Peak memory usage: 87 MB % 5.17/1.16 % (3818191)Instructions burned: 121 (million) % 5.17/1.16 % (3818193)Instruction limit reached! % 5.17/1.16 % (3818193)------------------------------ % 5.17/1.16 % (3818193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.17/1.16 % (3818193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.17/1.16 % (3818193)CaDiCaL version: 2.1.3 % 5.17/1.16 % (3818193)Termination reason: Instruction limit % 5.17/1.16 % (3818193)Termination phase: Saturation % 5.17/1.16 % (3818193)Time elapsed: 0.041 s % 5.17/1.16 % (3818193)Peak memory usage: 90 MB % 5.17/1.16 % (3818193)Instructions burned: 132 (million) % 5.17/1.16 % (3818192)Instruction limit reached! % 5.17/1.16 % (3818192)------------------------------ % 5.17/1.16 % (3818192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.17/1.16 % (3818192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.17/1.16 % (3818192)CaDiCaL version: 2.1.3 % 5.17/1.16 % (3818192)Termination reason: Instruction limit % 5.17/1.16 % (3818192)Termination phase: Saturation % 5.17/1.16 % (3818192)Time elapsed: 0.050 s % 5.17/1.16 % (3818192)Peak memory usage: 89 MB % 5.17/1.16 % (3818192)Instructions burned: 139 (million) % 5.17/1.16 % (3818201)lrs+10_1_sil=8000:sp=occurrence:random_seed=1521754293:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi) % 5.17/1.16 % (3818190)------------------------------ % 5.17/1.16 % (3818190)------------------------------ % 5.17/1.16 % (3818202)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2461083733:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi) % 5.17/1.16 % (3818202)Refutation not found, incomplete strategy % 5.17/1.16 % (3818202)------------------------------ % 6.19/1.35 % (3818202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.19/1.35 % (3818202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.19/1.35 % (3818202)CaDiCaL version: 2.1.3 % 6.19/1.35 % (3818202)Termination reason: Refutation not found, incomplete strategy % 6.19/1.35 % (3818202)Time elapsed: 0.001 s % 6.19/1.35 % (3818202)Peak memory usage: 89 MB % 6.19/1.35 % (3818202)Instructions burned: 2 (million) % 6.19/1.35 % (3818203)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3203303954:i=325:sd=1:ss=axioms:sgt=32_2998 on theBenchmark for (2998ds/325Mi) % 6.19/1.35 % Exception at run slice level% Exception at run slice level % 6.19/1.35 % 6.19/1.35 User error: User error: % Exception at run slice levelGNN currently only supports monomorphic FOL.GNN currently only supports monomorphic FOL. % 6.19/1.35 % 6.19/1.35 % 6.19/1.35 User error: GNN currently only supports monomorphic FOL. % 6.19/1.35 % (3818201)Instruction limit reached! % 6.19/1.35 % (3818201)------------------------------ % 6.19/1.35 % (3818201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.19/1.35 % (3818201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.19/1.35 % (3818201)CaDiCaL version: 2.1.3 % 6.19/1.35 % (3818201)Termination reason: Instruction limit % 6.19/1.35 % (3818201)Termination phase: Saturation % 6.19/1.35 % (3818201)Time elapsed: 0.077 s % 6.19/1.35 % (3818201)Peak memory usage: 89 MB % 6.19/1.35 % (3818201)Instructions burned: 288 (million) % 6.19/1.35 % (3818205)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=1854732106:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 6.19/1.35 % (3818203)Instruction limit reached! % 6.19/1.35 % (3818203)------------------------------ % 6.19/1.35 % (3818203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.19/1.35 % (3818203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.19/1.35 % (3818203)CaDiCaL version: 2.1.3 % 6.19/1.35 % (3818203)Termination reason: Instruction limit % 6.19/1.35 % (3818203)Termination phase: Saturation % 6.19/1.35 % (3818203)Time elapsed: 0.103 s % 6.19/1.35 % (3818203)Peak memory usage: 90 MB % 6.19/1.35 % (3818203)Instructions burned: 326 (million) % 6.19/1.35 % (3818210)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3873407563:cts=off:i=113:fsr=off:ss=included:sgt=4_2996 on theBenchmark for (2996ds/113Mi) % 6.19/1.35 % (3818209)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=623167960:i=2350_2996 on theBenchmark for (2996ds/2350Mi) % 6.19/1.35 % (3818208)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2722275228:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi) % 6.19/1.35 % (3818202)------------------------------ % 6.19/1.35 % (3818202)------------------------------ % 6.19/1.35 % (3818208)Refutation not found, incomplete strategy % 6.19/1.35 % (3818208)------------------------------ % 6.19/1.35 % (3818208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.19/1.35 % (3818208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.19/1.35 % (3818208)CaDiCaL version: 2.1.3 % 6.19/1.35 % (3818208)Termination reason: Refutation not found, incomplete strategy % 6.19/1.35 % (3818208)Time elapsed: 0.005 s % 6.19/1.35 % (3818208)Peak memory usage: 88 MB % 6.19/1.35 % (3818208)Instructions burned: 18 (million) % 6.19/1.35 % (3818211)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4174488677:i=127:av=off:fsr=off:sup=off_2996 on theBenchmark for (2996ds/127Mi) % 6.19/1.35 % (3818210)Refutation not found, incomplete strategy % 6.19/1.35 % (3818210)------------------------------ % 6.19/1.35 % (3818210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.19/1.35 % (3818210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.19/1.35 % (3818210)CaDiCaL version: 2.1.3 % 6.19/1.35 % (3818210)Termination reason: Refutation not found, incomplete strategy % 6.19/1.35 % (3818210)Time elapsed: 0.007 s % 6.19/1.35 % (3818210)Peak memory usage: 89 MB % 6.19/1.35 % (3818210)Instructions burned: 23 (million) % 6.19/1.35 % (3818211)Refutation not found, incomplete strategy % 6.19/1.35 % (3818211)------------------------------ % 6.19/1.35 % (3818211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.19/1.35 % (3818211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.58 % (3818211)CaDiCaL version: 2.1.3 % 7.25/1.58 % (3818211)Termination reason: Refutation not found, incomplete strategy % 7.25/1.58 % (3818211)Time elapsed: 0.005 s % 7.25/1.58 % (3818211)Peak memory usage: 88 MB % 7.25/1.58 % (3818211)Instructions burned: 17 (million) % 7.25/1.58 % (3818205)Instruction limit reached! % 7.25/1.58 % (3818205)------------------------------ % 7.25/1.58 % (3818205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.25/1.58 % (3818205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.58 % (3818205)CaDiCaL version: 2.1.3 % 7.25/1.58 % (3818205)Termination reason: Instruction limit % 7.25/1.58 % (3818205)Termination phase: Saturation % 7.25/1.58 % (3818205)Time elapsed: 0.073 s % 7.25/1.58 % (3818205)Peak memory usage: 90 MB % 7.25/1.58 % (3818205)Instructions burned: 248 (million) % 7.25/1.58 % (3818213)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=140593924:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2995 on theBenchmark for (2995ds/114Mi) % 7.25/1.58 % (3818213)Refutation not found, incomplete strategy % 7.25/1.58 % (3818213)------------------------------ % 7.25/1.58 % (3818213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.25/1.58 % (3818213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.58 % (3818213)CaDiCaL version: 2.1.3 % 7.25/1.58 % (3818213)Termination reason: Refutation not found, incomplete strategy % 7.25/1.58 % (3818213)Time elapsed: 0.007 s % 7.25/1.58 % (3818213)Peak memory usage: 89 MB % 7.25/1.58 % (3818213)Instructions burned: 22 (million) % 7.25/1.58 % (3818218)lrs+10_1_sil=8000:sp=occurrence:random_seed=705034712:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2995 on theBenchmark for (2995ds/907Mi) % 7.25/1.58 % (3818219)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1437890243:i=437:sd=1:aac=none:ss=included_2995 on theBenchmark for (2995ds/437Mi) % 7.25/1.58 % (3818219)Refutation not found, incomplete strategy % 7.25/1.58 % (3818219)------------------------------ % 7.25/1.58 % (3818219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.25/1.58 % (3818219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.58 % (3818219)CaDiCaL version: 2.1.3 % 7.25/1.58 % (3818219)Termination reason: Refutation not found, incomplete strategy % 7.25/1.58 % (3818219)Time elapsed: 0.005 s % 7.25/1.58 % (3818219)Peak memory usage: 89 MB % 7.25/1.58 % (3818219)Instructions burned: 13 (million) % 7.25/1.58 % (3818208)------------------------------ % 7.25/1.58 % (3818208)------------------------------ % 7.25/1.58 % (3818210)------------------------------ % 7.25/1.58 % (3818210)------------------------------ % 7.25/1.58 % (3818211)------------------------------ % 7.25/1.58 % (3818211)------------------------------ % 7.25/1.58 % Exception at run slice level % 7.25/1.58 User error: GNN currently only supports monomorphic FOL. % 7.25/1.58 % (3818213)------------------------------ % 7.25/1.58 % (3818213)------------------------------ % 7.25/1.58 % (3818224)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1695371276:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2993 on theBenchmark for (2993ds/134Mi) % 7.25/1.58 % (3818223)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1196039530:i=5202:ss=axioms:sgt=16_2993 on theBenchmark for (2993ds/5202Mi) % 7.25/1.58 % (3818225)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1521183662:st=8:i=592:sd=3:ep=RST:ss=axioms_2993 on theBenchmark for (2993ds/592Mi) % 7.25/1.58 % (3818219)------------------------------ % 7.25/1.58 % (3818219)------------------------------ % 7.25/1.58 % (3818224)Instruction limit reached! % 7.25/1.58 % (3818224)------------------------------ % 7.25/1.58 % (3818224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.25/1.58 % (3818224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.25/1.58 % (3818224)CaDiCaL version: 2.1.3 % 7.25/1.58 % (3818224)Termination reason: Instruction limit % 7.25/1.58 % (3818224)Termination phase: Saturation % 7.25/1.58 % (3818224)Time elapsed: 0.039 s % 7.25/1.58 % (3818224)Peak memory usage: 89 MB % 7.25/1.58 % (3818224)Instructions burned: 134 (million) % 7.25/1.58 % (3818226)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2764622923:st=3:i=13193:sd=3:ss=axioms_2993 on theBenchmark for (2993ds/13193Mi) % 7.25/1.58 % (3818227)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=3769401971:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2992 on theBenchmark for (2992ds/125Mi) % 9.63/2.00 % (3818227)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 9.63/2.00 % (3818218)Instruction limit reached! % 9.63/2.00 % (3818218)------------------------------ % 9.63/2.00 % (3818218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.63/2.00 % (3818218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.63/2.00 % (3818218)CaDiCaL version: 2.1.3 % 9.63/2.00 % (3818218)Termination reason: Instruction limit % 9.63/2.00 % (3818218)Termination phase: Saturation % 9.63/2.00 % (3818218)Time elapsed: 0.253 s % 9.63/2.00 % (3818218)Peak memory usage: 91 MB % 9.63/2.00 % (3818218)Instructions burned: 907 (million) % 9.63/2.00 % (3818227)Instruction limit reached! % 9.63/2.00 % (3818227)------------------------------ % 9.63/2.00 % (3818227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.63/2.00 % (3818227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.63/2.00 % (3818227)CaDiCaL version: 2.1.3 % 9.63/2.00 % (3818227)Termination reason: Instruction limit % 9.63/2.00 % (3818227)Termination phase: Saturation % 9.63/2.00 % (3818227)Time elapsed: 0.034 s % 9.63/2.00 % (3818227)Peak memory usage: 90 MB % 9.63/2.00 % (3818227)Instructions burned: 125 (million) % 9.63/2.00 % (3818231)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2516105735:i=134:gtgl=5:slsql=off:gtg=exists_sym_2992 on theBenchmark for (2992ds/134Mi) % 9.63/2.00 % Exception at run slice level % 9.63/2.00 User error: Immediate (shared) subterms of term/literal aa(X1,fun(list(X1),X0),X4,X3) = sF17(X1,X0,X4,X3) have different types/not well-typed! % 9.63/2.00 % (3818232)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2308707786:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2992 on theBenchmark for (2992ds/141Mi) % 9.63/2.00 % (3818232)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 9.63/2.00 % (3818232)Refutation not found, incomplete strategy % 9.63/2.00 % (3818232)------------------------------ % 9.63/2.00 % (3818232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.63/2.00 % (3818232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.63/2.00 % (3818232)CaDiCaL version: 2.1.3 % 9.63/2.00 % (3818232)Termination reason: Refutation not found, incomplete strategy % 9.63/2.00 % (3818232)Time elapsed: 0.001 s % 9.63/2.00 % (3818232)Peak memory usage: 88 MB % 9.63/2.00 % (3818232)Instructions burned: 1 (million) % 9.63/2.00 % (3818225)Instruction limit reached! % 9.63/2.00 % (3818225)------------------------------ % 9.63/2.00 % (3818225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.63/2.00 % (3818225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.63/2.00 % (3818225)CaDiCaL version: 2.1.3 % 9.63/2.00 % (3818225)Termination reason: Instruction limit % 9.63/2.00 % (3818225)Termination phase: Saturation % 9.63/2.00 % (3818225)Time elapsed: 0.172 s % 9.63/2.00 % (3818225)Peak memory usage: 91 MB % 9.63/2.00 % (3818225)Instructions burned: 594 (million) % 9.63/2.00 % (3818235)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3677689777:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/431Mi) % 9.63/2.00 % (3818235)Refutation not found, incomplete strategy % 9.63/2.00 % (3818235)------------------------------ % 9.63/2.00 % (3818235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.63/2.00 % (3818235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.63/2.00 % (3818235)CaDiCaL version: 2.1.3 % 9.63/2.00 % (3818235)Termination reason: Refutation not found, incomplete strategy % 9.63/2.00 % (3818235)Time elapsed: 0.002 s % 9.63/2.00 % (3818235)Peak memory usage: 89 MB % 9.63/2.00 % (3818235)Instructions burned: 4 (million) % 9.63/2.00 % Exception at run slice level % 9.63/2.00 User error: GNN currently only supports monomorphic FOL. % 9.63/2.00 % (3818236)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=3008254672:i=6060:aac=none:ins=25_2991 on theBenchmark for (2991ds/6060Mi) % 9.63/2.00 % Exception at run slice level % 9.63/2.00 User error: GNN currently only supports monomorphic FOL. % 9.63/2.00 % (3818238)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=1571918980:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2991 on theBenchmark for (2991ds/150Mi) % 13.60/2.48 % (3818238)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.60/2.48 % (3818240)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2558194207:i=14155:bd=all_2990 on theBenchmark for (2990ds/14155Mi) % 13.60/2.48 % (3818232)------------------------------ % 13.60/2.48 % (3818232)------------------------------ % 13.60/2.48 % (3818238)Instruction limit reached! % 13.60/2.48 % (3818238)------------------------------ % 13.60/2.48 % (3818238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.60/2.48 % (3818238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.60/2.48 % (3818238)CaDiCaL version: 2.1.3 % 13.60/2.48 % (3818238)Termination reason: Instruction limit % 13.60/2.48 % (3818238)Termination phase: Saturation % 13.60/2.48 % (3818238)Time elapsed: 0.050 s % 13.60/2.48 % (3818238)Peak memory usage: 90 MB % 13.60/2.48 % (3818238)Instructions burned: 153 (million) % 13.60/2.48 % (3818242)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=79348688:i=667:av=off:fsr=off_2990 on theBenchmark for (2990ds/667Mi) % 13.60/2.48 % (3818242)Refutation not found, incomplete strategy % 13.60/2.48 % (3818242)------------------------------ % 13.60/2.48 % (3818242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.60/2.48 % (3818242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.60/2.48 % (3818242)CaDiCaL version: 2.1.3 % 13.60/2.48 % (3818242)Termination reason: Refutation not found, incomplete strategy % 13.60/2.48 % (3818242)Time elapsed: 0.006 s % 13.60/2.48 % (3818242)Peak memory usage: 89 MB % 13.60/2.48 % (3818242)Instructions burned: 19 (million) % 13.60/2.48 % (3818235)------------------------------ % 13.60/2.48 % (3818235)------------------------------ % 13.60/2.48 % (3818244)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=4191029101:s2a=on:i=185:s2at=1.8:fdi=4_2989 on theBenchmark for (2989ds/185Mi) % 13.60/2.48 % Exception at run slice level % 13.60/2.48 User error: GNN currently only supports monomorphic FOL. % 13.60/2.48 % (3818244)Instruction limit reached! % 13.60/2.48 % (3818244)------------------------------ % 13.60/2.48 % (3818244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.60/2.48 % (3818244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.60/2.48 % (3818244)CaDiCaL version: 2.1.3 % 13.60/2.48 % (3818244)Termination reason: Instruction limit % 13.60/2.48 % (3818244)Termination phase: Saturation % 13.60/2.48 % (3818244)Time elapsed: 0.064 s % 13.60/2.48 % (3818244)Peak memory usage: 91 MB % 13.60/2.48 % (3818244)Instructions burned: 185 (million) % 13.60/2.48 % (3818248)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1779052947:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2989 on theBenchmark for (2989ds/193Mi) % 13.60/2.48 % (3818249)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1882199405:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2989 on theBenchmark for (2989ds/4850Mi) % 13.60/2.48 % (3818249)Refutation not found, incomplete strategy % 13.60/2.48 % (3818249)------------------------------ % 13.60/2.48 % (3818249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.60/2.48 % (3818249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.60/2.48 % (3818249)CaDiCaL version: 2.1.3 % 13.60/2.48 % (3818249)Termination reason: Refutation not found, incomplete strategy % 13.60/2.48 % (3818249)Time elapsed: 0.004 s % 13.60/2.48 % (3818249)Peak memory usage: 88 MB % 13.60/2.48 % (3818249)Instructions burned: 14 (million) % 13.60/2.48 % (3818250)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3465823034:i=12111:sd=1:ss=included_2988 on theBenchmark for (2988ds/12111Mi) % 13.60/2.48 % (3818242)------------------------------ % 13.60/2.48 % (3818242)------------------------------ % 13.60/2.48 % (3818248)Instruction limit reached! % 13.60/2.48 % (3818248)------------------------------ % 13.60/2.48 % (3818248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.60/2.48 % (3818248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.99/2.87 % (3818248)CaDiCaL version: 2.1.3 % 15.99/2.87 % (3818248)Termination reason: Instruction limit % 15.99/2.87 % (3818248)Termination phase: Saturation % 15.99/2.87 % (3818248)Time elapsed: 0.060 s % 15.99/2.87 % (3818248)Peak memory usage: 89 MB % 15.99/2.87 % (3818248)Instructions burned: 193 (million) % 15.99/2.87 % Exception at run slice level % 15.99/2.87 User error: GNN currently only supports monomorphic FOL. % 15.99/2.87 % (3818252)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=75110481:i=319:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/319Mi) % 15.99/2.87 % (3818255)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=164669928:i=2064:ep=RST_2988 on theBenchmark for (2988ds/2064Mi) % 15.99/2.87 % (3818257)dis-1011_128_sil=32000:random_seed=3727845504:i=3706:ep=RST:av=off_2987 on theBenchmark for (2987ds/3706Mi) % 15.99/2.87 % (3818249)------------------------------ % 15.99/2.87 % (3818249)------------------------------ % 15.99/2.87 % (3818258)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2178136459:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2987 on theBenchmark for (2987ds/757Mi) % 15.99/2.88 % (3818258)Refutation not found, incomplete strategy % 15.99/2.88 % (3818258)------------------------------ % 15.99/2.88 % (3818258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.99/2.88 % (3818258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.99/2.88 % (3818258)CaDiCaL version: 2.1.3 % 15.99/2.88 % (3818258)Termination reason: Refutation not found, incomplete strategy % 15.99/2.88 % (3818258)Time elapsed: 0.006 s % 15.99/2.88 % (3818258)Peak memory usage: 89 MB % 15.99/2.88 % (3818258)Instructions burned: 19 (million) % 15.99/2.88 % (3818259)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2017350219:i=13913:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/13913Mi) % 15.99/2.88 % (3818252)Instruction limit reached! % 15.99/2.88 % (3818252)------------------------------ % 15.99/2.88 % (3818252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.99/2.88 % (3818252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.99/2.88 % (3818252)CaDiCaL version: 2.1.3 % 15.99/2.88 % (3818252)Termination reason: Instruction limit % 15.99/2.88 % (3818252)Termination phase: Saturation % 15.99/2.88 % (3818252)Time elapsed: 0.082 s % 15.99/2.88 % (3818252)Peak memory usage: 90 MB % 15.99/2.88 % (3818252)Instructions burned: 321 (million) % 15.99/2.88 % Exception at run slice level % 15.99/2.88 User error: GNN currently only supports monomorphic FOL. % 15.99/2.88 % (3818263)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3014276404:i=9925:aac=none_2986 on theBenchmark for (2986ds/9925Mi) % 15.99/2.88 % (3818266)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1634098806:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2986 on theBenchmark for (2986ds/2479Mi) % 15.99/2.88 % (3818266)Refutation not found, incomplete strategy % 15.99/2.88 % (3818266)------------------------------ % 15.99/2.88 % (3818266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.99/2.88 % (3818266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.99/2.88 % (3818266)CaDiCaL version: 2.1.3 % 15.99/2.88 % (3818266)Termination reason: Refutation not found, incomplete strategy % 15.99/2.88 % (3818266)Time elapsed: 0.001 s % 15.99/2.88 % (3818266)Peak memory usage: 89 MB % 15.99/2.88 % (3818266)Instructions burned: 2 (million) % 15.99/2.88 % (3818258)------------------------------ % 15.99/2.88 % (3818258)------------------------------ % 15.99/2.88 % (3818267)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3251709104:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/440Mi) % 15.99/2.88 % (3818267)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 15.99/2.88 % Exception at run slice level % 15.99/2.88 User error: GNN currently only supports monomorphic FOL. % 15.99/2.88 % (3818266)------------------------------ % 15.99/2.88 % (3818266)------------------------------ % 15.99/2.88 % (3818270)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2041610217:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2984 on theBenchmark for (2984ds/11145Mi) % 15.99/2.88 % Exception at run slice level % 15.99/2.88 User error: GNN currently only supports monomorphic FOL. % 21.44/3.54 % (3818267)Instruction limit reached! % 21.44/3.54 % (3818267)------------------------------ % 21.44/3.54 % (3818267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.44/3.54 % (3818267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.44/3.54 % (3818267)CaDiCaL version: 2.1.3 % 21.44/3.54 % (3818267)Termination reason: Instruction limit % 21.44/3.54 % (3818267)Termination phase: Saturation % 21.44/3.54 % (3818267)Time elapsed: 0.125 s % 21.44/3.54 % (3818267)Peak memory usage: 89 MB % 21.44/3.54 % (3818267)Instructions burned: 441 (million) % 21.44/3.54 % (3818272)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=2028184009:cts=off:i=3034:av=off:er=known:fsd=on_2984 on theBenchmark for (2984ds/3034Mi) % 21.44/3.54 % (3818274)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1805886831:st=2:s2a=on:i=524:s2at=2:ss=axioms_2983 on theBenchmark for (2983ds/524Mi) % 21.44/3.54 % (3818275)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1173563386:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2983 on theBenchmark for (2983ds/1016Mi) % 21.44/3.54 % (3818276)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2552630672:i=14123:bd=preordered:ins=4_2982 on theBenchmark for (2982ds/14123Mi) % 21.44/3.54 % Exception at run slice level % 21.44/3.54 User error: GNN currently only supports monomorphic FOL. % 21.44/3.54 % (3818255)Instruction limit reached! % 21.44/3.54 % (3818255)------------------------------ % 21.44/3.54 % (3818255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.44/3.54 % (3818255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.44/3.54 % (3818255)CaDiCaL version: 2.1.3 % 21.44/3.54 % (3818255)Termination reason: Instruction limit % 21.44/3.54 % (3818255)Termination phase: Saturation % 21.44/3.54 % (3818255)Time elapsed: 0.584 s % 21.44/3.54 % (3818255)Peak memory usage: 94 MB % 21.44/3.54 % (3818255)Instructions burned: 2064 (million) % 21.44/3.54 % Exception at run slice level % 21.44/3.54 User error: GNN currently only supports monomorphic FOL. % 21.44/3.54 % (3818274)Instruction limit reached! % 21.44/3.54 % (3818274)------------------------------ % 21.44/3.54 % (3818274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.44/3.54 % (3818274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.44/3.54 % (3818274)CaDiCaL version: 2.1.3 % 21.44/3.54 % (3818274)Termination reason: Instruction limit % 21.44/3.54 % (3818274)Termination phase: Saturation % 21.44/3.54 % (3818274)Time elapsed: 0.147 s % 21.44/3.54 % (3818274)Peak memory usage: 91 MB % 21.44/3.54 % (3818274)Instructions burned: 527 (million) % 21.44/3.54 % (3818281)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3791946728:i=5781:kws=precedence:bd=all:rawr=on_2981 on theBenchmark for (2981ds/5781Mi) % 21.44/3.54 % (3818282)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=555100027:i=2448:gtgl=5:bd=preordered:gtg=all_2981 on theBenchmark for (2981ds/2448Mi) % 21.44/3.54 % Exception at run slice level % 21.44/3.54 User error: GNN currently only supports monomorphic FOL. % 21.44/3.54 % (3818284)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3916136255:st=5.6:i=2033:sd=3:ss=axioms_2980 on theBenchmark for (2980ds/2033Mi) % 21.44/3.54 % (3818283)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2993126634:i=3223:kws=precedence:fgj=on:av=off_2980 on theBenchmark for (2980ds/3223Mi) % 21.44/3.54 % (3818275)Instruction limit reached! % 21.44/3.54 % (3818275)------------------------------ % 21.44/3.54 % (3818275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.44/3.54 % (3818275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.44/3.54 % (3818275)CaDiCaL version: 2.1.3 % 21.44/3.54 % (3818275)Termination reason: Instruction limit % 21.44/3.54 % (3818275)Termination phase: Saturation % 21.44/3.54 % (3818275)Time elapsed: 0.301 s % 21.44/3.54 % (3818275)Peak memory usage: 97 MB % 21.44/3.54 % (3818275)Instructions burned: 1019 (million) % 21.44/3.54 % (3818287)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3169030266:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2979 on theBenchmark for (2979ds/2055Mi) % 21.44/3.54 % (3818257)Instruction limit reached! % 27.38/4.36 % (3818257)------------------------------ % 27.38/4.36 % (3818257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.38/4.36 % (3818257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.38/4.36 % (3818257)CaDiCaL version: 2.1.3 % 27.38/4.36 % (3818257)Termination reason: Instruction limit % 27.38/4.36 % (3818257)Termination phase: Saturation % 27.38/4.36 % (3818257)Time elapsed: 0.813 s % 27.38/4.36 % (3818257)Peak memory usage: 91 MB % 27.38/4.36 % (3818257)Instructions burned: 3711 (million) % 27.38/4.36 % Exception at run slice level % 27.38/4.36 User error: GNN currently only supports monomorphic FOL. % 27.38/4.36 % (3818290)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=108357024:i=21611:sd=3:ss=axioms_2979 on theBenchmark for (2979ds/21611Mi) % 27.38/4.36 % Exception at run slice level % 27.38/4.36 User error: GNN currently only supports monomorphic FOL. % 27.38/4.36 % Exception at run slice level % 27.38/4.36 User error: GNN currently only supports monomorphic FOL. % 27.38/4.36 % (3818292)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3007479012:i=4835:sd=13:ss=axioms:sgt=23_2978 on theBenchmark for (2978ds/4835Mi) % 27.38/4.36 % (3818292)Refutation not found, incomplete strategy % 27.38/4.36 % (3818292)------------------------------ % 27.38/4.36 % (3818292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.38/4.36 % (3818292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.38/4.36 % (3818292)CaDiCaL version: 2.1.3 % 27.38/4.36 % (3818292)Termination reason: Refutation not found, incomplete strategy % 27.38/4.36 % (3818292)Time elapsed: 0.007 s % 27.38/4.36 % (3818292)Peak memory usage: 89 MB % 27.38/4.36 % (3818292)Instructions burned: 24 (million) % 27.38/4.36 % (3818293)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=1686584011:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2977 on theBenchmark for (2977ds/797Mi) % 27.38/4.36 % Exception at run slice level % 27.38/4.36 User error: GNN currently only supports monomorphic FOL. % 27.38/4.36 % (3818296)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2835951196:i=6038:nm=6_2977 on theBenchmark for (2977ds/6038Mi) % 27.38/4.36 % (3818295)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1827498701:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2977 on theBenchmark for (2977ds/2326Mi) % 27.38/4.36 % (3818295)Refutation not found, incomplete strategy % 27.38/4.36 % (3818295)------------------------------ % 27.38/4.36 % (3818295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.38/4.36 % (3818295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.38/4.36 % (3818295)CaDiCaL version: 2.1.3 % 27.38/4.36 % (3818295)Termination reason: Refutation not found, incomplete strategy % 27.38/4.36 % (3818295)Time elapsed: 0.009 s % 27.38/4.36 % (3818295)Peak memory usage: 89 MB % 27.38/4.36 % (3818295)Instructions burned: 28 (million) % 27.38/4.36 % Exception at run slice level % 27.38/4.36 User error: GNN currently only supports monomorphic FOL. % 27.38/4.36 % (3818292)------------------------------ % 27.38/4.36 % (3818292)------------------------------ % 27.38/4.36 % (3818299)lrs+10_1_sil=32000:sp=occurrence:random_seed=862951891:st=2:i=33334:sd=3:ss=included:sgt=32_2976 on theBenchmark for (2976ds/33334Mi) % 27.38/4.36 % (3818295)------------------------------ % 27.38/4.36 % (3818295)------------------------------ % 27.38/4.36 % (3818293)Instruction limit reached! % 27.38/4.36 % (3818293)------------------------------ % 27.38/4.36 % (3818293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.38/4.36 % (3818293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.38/4.36 % (3818293)CaDiCaL version: 2.1.3 % 27.38/4.36 % (3818293)Termination reason: Instruction limit % 27.38/4.36 % (3818293)Termination phase: Saturation % 27.38/4.36 % (3818293)Time elapsed: 0.189 s % 27.38/4.36 % (3818293)Peak memory usage: 90 MB % 27.38/4.36 % (3818293)Instructions burned: 802 (million) % 27.38/4.36 % (3818303)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=3480374259:i=8327:s2at=5:bd=preordered_2975 on theBenchmark for (2975ds/8327Mi) % 27.38/4.36 % (3818302)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1378518389:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2975 on theBenchmark for (2975ds/1008Mi) % 34.00/5.20 % Exception at run slice level % 34.00/5.20 User error: GNN currently only supports monomorphic FOL. % 34.00/5.20 % (3818305)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=2534206677:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2974 on theBenchmark for (2974ds/1083Mi) % 34.00/5.20 % (3818306)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=510325867:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2974 on theBenchmark for (2974ds/1084Mi) % 34.00/5.20 % (3818306)Refutation not found, incomplete strategy % 34.00/5.20 % (3818306)------------------------------ % 34.00/5.20 % (3818306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.00/5.20 % (3818306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.00/5.20 % (3818306)CaDiCaL version: 2.1.3 % 34.00/5.20 % (3818306)Termination reason: Refutation not found, incomplete strategy % 34.00/5.20 % (3818306)Time elapsed: 0.016 s % 34.00/5.20 % (3818306)Peak memory usage: 88 MB % 34.00/5.20 % (3818306)Instructions burned: 54 (million) % 34.00/5.20 % (3818309)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3618595317:i=6995:s2at=5:gtg=all_2974 on theBenchmark for (2974ds/6995Mi) % 34.00/5.20 % Exception at run slice level % 34.00/5.20 User error: GNN currently only supports monomorphic FOL. % 34.00/5.20 % (3818306)------------------------------ % 34.00/5.20 % (3818306)------------------------------ % 34.00/5.20 % (3818302)Instruction limit reached! % 34.00/5.20 % (3818302)------------------------------ % 34.00/5.20 % (3818302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.00/5.20 % (3818302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.00/5.20 % (3818302)CaDiCaL version: 2.1.3 % 34.00/5.20 % (3818302)Termination reason: Instruction limit % 34.00/5.20 % (3818302)Termination phase: Saturation % 34.00/5.20 % (3818302)Time elapsed: 0.275 s % 34.00/5.20 % (3818302)Peak memory usage: 97 MB % 34.00/5.20 % (3818302)Instructions burned: 1008 (million) % 34.00/5.20 % (3818313)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1500744368:st=2:i=6225:sd=15:ss=axioms_2972 on theBenchmark for (2972ds/6225Mi) % 34.00/5.20 % Exception at run slice level % 34.00/5.20 User error: GNN currently only supports monomorphic FOL. % 34.00/5.20 % (3818305)Instruction limit reached! % 34.00/5.20 % (3818305)------------------------------ % 34.00/5.20 % (3818305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.00/5.20 % (3818305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.00/5.20 % (3818305)CaDiCaL version: 2.1.3 % 34.00/5.20 % (3818305)Termination reason: Instruction limit % 34.00/5.20 % (3818305)Termination phase: Saturation % 34.00/5.20 % (3818305)Time elapsed: 0.271 s % 34.00/5.20 % (3818305)Peak memory usage: 95 MB % 34.00/5.20 % (3818305)Instructions burned: 1087 (million) % 34.00/5.20 % (3818314)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=1358688168:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2971 on theBenchmark for (2971ds/3372Mi) % 34.00/5.20 % (3818315)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2612419450:st=2.3:i=26457:sd=10:ss=included:sgt=8_2971 on theBenchmark for (2971ds/26457Mi) % 34.00/5.20 % (3818317)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=3306330116:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2971 on theBenchmark for (2971ds/13494Mi) % 34.00/5.20 % (3818318)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=3531035790:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2970 on theBenchmark for (2970ds/2503Mi) % 34.00/5.20 % (3818318)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 34.00/5.20 % Exception at run slice level % 34.00/5.20 User error: GNN currently only supports monomorphic FOL. % 34.00/5.20 % Exception at run slice level % 34.00/5.20 User error: GNN currently only supports monomorphic FOL. % 34.00/5.20 % Exception at run slice level % 41.33/6.33 User error: GNN currently only supports monomorphic FOL. % 41.33/6.33 % Exception at run slice level % 41.33/6.33 User error: GNN currently only supports monomorphic FOL. % 41.33/6.33 % (3818323)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=2293074225:i=2559:sd=1:ep=RSTC:ss=axioms_2968 on theBenchmark for (2968ds/2559Mi) % 41.33/6.33 % (3818324)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3577318571:i=30753:av=off:ss=included_2968 on theBenchmark for (2968ds/30753Mi) % 41.33/6.33 % (3818325)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=1196563557:i=26473:ep=RSTC_2967 on theBenchmark for (2967ds/26473Mi) % 41.33/6.33 % (3818326)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=1893491066:cts=off:i=2759:kws=inv_arity:fgj=on_2967 on theBenchmark for (2967ds/2759Mi) % 41.33/6.33 % (3818281)Instruction limit reached! % 41.33/6.33 % (3818281)------------------------------ % 41.33/6.33 % (3818281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.33/6.33 % (3818281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.33/6.33 % (3818281)CaDiCaL version: 2.1.3 % 41.33/6.33 % (3818281)Termination reason: Instruction limit % 41.33/6.33 % (3818281)Termination phase: Saturation % 41.33/6.33 % (3818281)Time elapsed: 1.436 s % 41.33/6.33 % (3818281)Peak memory usage: 97 MB % 41.33/6.33 % (3818281)Instructions burned: 5786 (million) % 41.33/6.33 % Exception at run slice level % 41.33/6.33 User error: GNN currently only supports monomorphic FOL. % 41.33/6.33 % Exception at run slice level % 41.33/6.33 User error: GNN currently only supports monomorphic FOL. % 41.33/6.33 % (3818331)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=1503736892:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2965 on theBenchmark for (2965ds/5665Mi) % 41.33/6.33 % (3818331)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 41.33/6.33 % (3818332)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=1645799564:i=1532:ep=RS:ss=axioms_2965 on theBenchmark for (2965ds/1532Mi) % 41.33/6.33 % (3818333)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3529379503:i=1565:sd=2:ss=axioms:sgt=32_2965 on theBenchmark for (2965ds/1565Mi) % 41.33/6.33 % Exception at run slice level % 41.33/6.33 User error: GNN currently only supports monomorphic FOL. % 41.33/6.33 % (3818337)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=2959436052:i=1572:fgj=on:gsp=on_2964 on theBenchmark for (2964ds/1572Mi) % 41.33/6.33 % Exception at run slice level % 41.33/6.33 User error: GNN currently only supports monomorphic FOL. % 41.33/6.33 % (3818337)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 41.33/6.33 % Exception at run slice level % 41.33/6.33 % Exception at run slice levelUser error: GNN currently only supports monomorphic FOL. % 41.33/6.33 % 41.33/6.33 User error: GNN currently only supports monomorphic FOL. % 41.33/6.33 % (3818339)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=659200642:i=6052:sd=4:ss=axioms:sgt=24_2962 on theBenchmark for (2962ds/6052Mi) % 41.33/6.33 % (3818341)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=2195448984:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2962 on theBenchmark for (2962ds/1842Mi) % 41.33/6.33 % (3818340)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=1934804428:i=3500:sd=1:bd=preordered:sup=off:ss=included_2962 on theBenchmark for (2962ds/3500Mi) % 41.33/6.33 % (3818341)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 41.33/6.33 % Exception at run slice level % 41.33/6.33 User error: GNN currently only supports monomorphic FOL. % 41.33/6.33 % Exception at run slice level % 41.33/6.33 User error: GNN currently only supports monomorphic FOL. % 47.60/7.23 % (3818345)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1966262964:i=66096:add=on_2960 on theBenchmark for (2960ds/66096Mi) % 47.60/7.23 % Exception at run slice level % 47.60/7.23 User error: GNN currently only supports monomorphic FOL. % 47.60/7.23 % Exception at run slice level % 47.60/7.23 User error: GNN currently only supports monomorphic FOL. % 47.60/7.23 % (3818346)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=3213103234:i=1884:sd=1:nm=60:ss=axioms_2959 on theBenchmark for (2959ds/1884Mi) % 47.60/7.23 % (3818349)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=2671283920:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2959 on theBenchmark for (2959ds/2037Mi) % 47.60/7.23 % (3818348)lrs-1011_4:1_sil=16000:bsr=on:random_seed=4257917372:cts=off:i=5469:bs=on:fsr=off_2959 on theBenchmark for (2959ds/5469Mi) % 47.60/7.23 % Exception at run slice level % 47.60/7.23 User error: GNN currently only supports monomorphic FOL. % 47.60/7.23 % Exception at run slice level % 47.60/7.23 User error: GNN currently only supports monomorphic FOL. % 47.60/7.23 % (3818353)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=1259976433:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2957 on theBenchmark for (2957ds/2110Mi) % 47.60/7.23 % Exception at run slice level % 47.60/7.23 User error: GNN currently only supports monomorphic FOL. % 47.60/7.23 % (3818354)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=1825931611:i=2430:add=off:aac=none:nm=16_2956 on theBenchmark for (2956ds/2430Mi) % 47.60/7.23 % (3818313)Instruction limit reached! % 47.60/7.23 % (3818313)------------------------------ % 47.60/7.23 % (3818313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.60/7.23 % (3818313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.60/7.23 % (3818313)CaDiCaL version: 2.1.3 % 47.60/7.23 % (3818313)Termination reason: Instruction limit % 47.60/7.23 % (3818313)Termination phase: Saturation % 47.60/7.23 % (3818313)Time elapsed: 1.600 s % 47.60/7.23 % (3818313)Peak memory usage: 106 MB % 47.60/7.23 % (3818313)Instructions burned: 6228 (million) % 47.60/7.23 % (3818356)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=2984007725:cond=fast:i=4891_2955 on theBenchmark for (2955ds/4891Mi) % 47.60/7.23 % (3818358)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=3731110459:st=2:i=14845:sd=2:ss=included:fsd=on_2955 on theBenchmark for (2955ds/14845Mi) % 47.60/7.23 % Exception at run slice level % 47.60/7.23 User error: GNN currently only supports monomorphic FOL. % 47.60/7.23 % Exception at run slice level % 47.60/7.23 User error: GNN currently only supports monomorphic FOL. % 47.60/7.23 % (3818361)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=3447091450:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2953 on theBenchmark for (2953ds/7534Mi) % 47.60/7.23 % Exception at run slice level % 47.60/7.23 User error: GNN currently only supports monomorphic FOL. % 47.60/7.23 % (3818362)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=1274019533:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2953 on theBenchmark for (2953ds/10353Mi) % 47.60/7.23 % Exception at run slice level % 47.60/7.23 User error: GNN currently only supports monomorphic FOL. % 47.60/7.23 % (3818364)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1218198051:i=7860_2952 on theBenchmark for (2952ds/7860Mi) % 47.60/7.23 % (3818364)Refutation not found, incomplete strategy % 47.60/7.23 % (3818364)------------------------------ % 47.60/7.23 % (3818364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.60/7.23 % (3818364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.60/7.23 % (3818364)CaDiCaL version: 2.1.3 % 47.60/7.23 % (3818364)Termination reason: Refutation not found, incomplete strategy % 47.60/7.23 % (3818364)Time elapsed: 0.006 s % 66.85/10.01 % (3818364)Peak memory usage: 89 MB % 66.85/10.01 % (3818364)Instructions burned: 19 (million) % 66.85/10.01 % (3818366)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=2179896238:i=7896:sd=2:bs=on:ss=included:sgt=20_2952 on theBenchmark for (2952ds/7896Mi) % 66.85/10.01 % Exception at run slice level % 66.85/10.01 User error: GNN currently only supports monomorphic FOL. % 66.85/10.01 % Exception at run slice level % 66.85/10.01 User error: GNN currently only supports monomorphic FOL. % 66.85/10.01 % (3818364)------------------------------ % 66.85/10.01 % (3818364)------------------------------ % 66.85/10.01 % (3818369)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=2078463354:i=5812:gtgl=2:gtg=all_2950 on theBenchmark for (2950ds/5812Mi) % 66.85/10.01 % (3818370)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=234457267:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2950 on theBenchmark for (2950ds/2965Mi) % 66.85/10.01 % Exception at run slice level % 66.85/10.01 User error: GNN currently only supports monomorphic FOL. % 66.85/10.01 % (3818371)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=915600616:i=2967:kws=precedence:bd=preordered:av=off_2949 on theBenchmark for (2949ds/2967Mi) % 66.85/10.01 % (3818374)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=3220227347:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2948 on theBenchmark for (2948ds/3022Mi) % 66.85/10.01 % Exception at run slice level % 66.85/10.01 User error: GNN currently only supports monomorphic FOL. % 66.85/10.01 % Exception at run slice level % 66.85/10.01 User error: GNN currently only supports monomorphic FOL. % 66.85/10.01 % Exception at run slice level % 66.85/10.01 User error: GNN currently only supports monomorphic FOL. % 66.85/10.01 % (3818377)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=3369729378:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2946 on theBenchmark for (2946ds/3207Mi) % 66.85/10.01 % (3818378)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=3288631586:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2946 on theBenchmark for (2946ds/3289Mi) % 66.85/10.01 % Exception at run slice level % 66.85/10.01 User error: GNN currently only supports monomorphic FOL. % 66.85/10.01 % (3818379)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=14730272:i=38569:sd=3:ss=axioms:sgt=32_2946 on theBenchmark for (2946ds/38569Mi) % 66.85/10.01 % (3818382)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=1923498518:cts=off:i=3394_2945 on theBenchmark for (2945ds/3394Mi) % 66.85/10.01 % Exception at run slice level% Exception at run slice level % 66.85/10.01 % 66.85/10.01 User error: User error: GNN currently only supports monomorphic FOL.GNN currently only supports monomorphic FOL. % 66.85/10.01 % 66.85/10.01 % Exception at run slice level % 66.85/10.01 User error: GNN currently only supports monomorphic FOL. % 66.85/10.01 % (3818385)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=3052057498:i=33824:bd=preordered_2943 on theBenchmark for (2943ds/33824Mi) % 66.85/10.01 % (3818386)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=1001486516:i=20684:bd=all:gtg=exists_sym_2943 on theBenchmark for (2943ds/20684Mi) % 66.85/10.01 % Exception at run slice level % 66.85/10.01 User error: GNN currently only supports monomorphic FOL. % 66.85/10.01 % (3818387)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=748355203: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_2943 on theBenchmark for (2943ds/7222Mi) % 66.85/10.01 % (3818387)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 66.85/10.01 % (3818390)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=3920698700:st=4:i=7295:sd=4:ep=R:ss=axioms_2942 on theBenchmark for (2942ds/7295Mi) % 82.49/12.13 % Exception at run slice level % 82.49/12.13 User error: GNN currently only supports monomorphic FOL. % 82.49/12.13 % Exception at run slice level % 82.49/12.13 User error: GNN currently only supports monomorphic FOL. % 82.49/12.13 % Exception at run slice level % 82.49/12.13 User error: GNN currently only supports monomorphic FOL. % 82.49/12.13 % Exception at run slice level % 82.49/12.13 User error: GNN currently only supports monomorphic FOL. % 82.49/12.13 % (3818348)Instruction limit reached! % 82.49/12.13 % (3818348)------------------------------ % 82.49/12.13 % (3818348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.49/12.13 % (3818348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.49/12.13 % (3818348)CaDiCaL version: 2.1.3 % 82.49/12.13 % (3818348)Termination reason: Instruction limit % 82.49/12.13 % (3818348)Termination phase: Saturation % 82.49/12.13 % (3818348)Time elapsed: 1.998 s % 82.49/12.13 % (3818348)Peak memory usage: 119 MB % 82.49/12.13 % (3818348)Instructions burned: 5469 (million) % 82.49/12.13 % (3818393)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=3348046154:i=4036:ins=10_2939 on theBenchmark for (2939ds/4036Mi) % 82.49/12.13 % (3818394)lrs+10_1_sil=128000:lcm=predicate:random_seed=4231932281:st=3:i=43697:sd=5:ss=axioms_2938 on theBenchmark for (2938ds/43697Mi) % 82.49/12.13 % (3818395)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=3749203081:i=17599:gtg=all:ss=axioms:fsd=on_2938 on theBenchmark for (2938ds/17599Mi) % 82.49/12.13 % (3818396)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=2777734276:i=4547:bd=preordered_2937 on theBenchmark for (2937ds/4547Mi) % 82.49/12.13 % (3818397)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=3248769381:i=9294:av=off_2937 on theBenchmark for (2937ds/9294Mi) % 82.49/12.13 % Exception at run slice level % 82.49/12.13 User error: GNN currently only supports monomorphic FOL. % 82.49/12.13 % Exception at run slice level % 82.49/12.13 User error: GNN currently only supports monomorphic FOL. % 82.49/12.13 % Exception at run slice level % 82.49/12.13 User error: GNN currently only supports monomorphic FOL. % 82.49/12.13 % Exception at run slice level % 82.49/12.13 User error: GNN currently only supports monomorphic FOL. % 82.49/12.13 % (3818403)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2849807202:i=32849:add=on_2935 on theBenchmark for (2935ds/32849Mi) % 82.49/12.13 % (3818404)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2443722090:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2935 on theBenchmark for (2935ds/4793Mi) % 82.49/12.13 % (3818405)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=1397398615:i=4840:nm=4:av=off_2934 on theBenchmark for (2934ds/4840Mi) % 82.49/12.13 % (3818406)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=4180120921:cts=off:i=5002_2934 on theBenchmark for (2934ds/5002Mi) % 82.49/12.13 % Exception at run slice level % 82.49/12.13 User error: GNN currently only supports monomorphic FOL. % 82.49/12.13 % Exception at run slice level % 82.49/12.13 User error: GNN currently only supports monomorphic FOL. % 82.49/12.13 % Exception at run slice level % 82.49/12.13 User error: GNN currently only supports monomorphic FOL. % 82.49/12.13 % Exception at run slice level % 82.49/12.13 User error: GNN currently only supports monomorphic FOL. % 82.49/12.13 % (3818411)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=3762754112:i=30479:sd=3:ss=axioms_2932 on theBenchmark for (2932ds/30479Mi) % 82.49/12.13 % (3818412)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=2552148235:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2932 on theBenchmark for (2932ds/11035Mi) % 82.49/12.13 % (3818412)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 92.01/13.51 % (3818413)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=1636806444:i=5835_2931 on theBenchmark for (2931ds/5835Mi) % 92.01/13.51 % (3818414)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=776443016:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2931 on theBenchmark for (2931ds/5890Mi) % 92.01/13.51 % Exception at run slice level % 92.01/13.51 User error: GNN currently only supports monomorphic FOL. % 92.01/13.51 % Exception at run slice level % 92.01/13.51 User error: GNN currently only supports monomorphic FOL. % 92.01/13.51 % Exception at run slice level % 92.01/13.51 User error: GNN currently only supports monomorphic FOL. % 92.01/13.51 % (3818419)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=2253557499:cts=off:i=19910:ep=RS_2929 on theBenchmark for (2929ds/19910Mi) % 92.01/13.51 % Exception at run slice level % 92.01/13.51 User error: GNN currently only supports monomorphic FOL. % 92.01/13.51 % (3818420)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=2022567448:i=20312:bd=preordered:fsr=off:er=filter_2928 on theBenchmark for (2928ds/20312Mi) % 92.01/13.51 % (3818421)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=2582765583:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2928 on theBenchmark for (2928ds/13822Mi) % 92.01/13.51 % (3818423)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=3296534209:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2927 on theBenchmark for (2927ds/7144Mi) % 92.01/13.51 % Exception at run slice level % 92.01/13.51 User error: GNN currently only supports monomorphic FOL. % 92.01/13.51 % Exception at run slice level % 92.01/13.51 User error: GNN currently only supports monomorphic FOL. % 92.01/13.51 % (3818427)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=4028603814:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2925 on theBenchmark for (2925ds/15184Mi) % 92.01/13.51 % (3818428)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=1169790870:i=107375_2925 on theBenchmark for (2925ds/107375Mi) % 92.01/13.51 % Exception at run slice level % 92.01/13.51 User error: GNN currently only supports monomorphic FOL. % 92.01/13.51 % Exception at run slice level % 92.01/13.51 User error: GNN currently only supports monomorphic FOL. % 92.01/13.51 % (3818431)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=1067989462:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2922 on theBenchmark for (2922ds/7958Mi) % 92.01/13.51 % (3818432)dis+10_128_sil=16000:nwc=0.7:random_seed=975587958:i=15999:nm=2:gsp=on_2922 on theBenchmark for (2922ds/15999Mi) % 92.01/13.51 % (3818432)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 92.01/13.51 % Exception at run slice level % 92.01/13.51 User error: GNN currently only supports monomorphic FOL. % 92.01/13.51 % (3818435)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=3664884260:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2919 on theBenchmark for (2919ds/8139Mi) % 92.01/13.51 % (3818423)Instruction limit reached! % 92.01/13.51 % (3818423)------------------------------ % 92.01/13.51 % (3818423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.01/13.51 % (3818423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.01/13.51 % (3818423)CaDiCaL version: 2.1.3 % 92.01/13.51 % (3818423)Termination reason: Instruction limit % 92.01/13.51 % (3818423)Termination phase: Saturation % 92.01/13.51 % (3818423)Time elapsed: 1.886 s % 92.01/13.51 % (3818423)Peak memory usage: 99 MB % 92.01/13.51 % (3818423)Instructions burned: 7144 (million) % 92.01/13.51 % (3818437)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=4213050977:st=4:i=8950:sd=5:ss=axioms_2907 on theBenchmark for (2907ds/8950Mi) % 92.01/13.51 % Exception at run slice level % 92.01/13.51 User error: GNN currently only supports monomorphic FOL. % 92.01/13.51 % (3818439)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=3894204129:i=9809:ins=10:av=off_2904 on theBenchmark for (2904ds/9809Mi) % 112.41/16.44 % Exception at run slice level % 112.41/16.44 User error: GNN currently only supports monomorphic FOL. % 112.41/16.44 % (3818435)Instruction limit reached! % 112.41/16.44 % (3818435)------------------------------ % 112.41/16.44 % (3818435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.41/16.44 % (3818435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.41/16.44 % (3818435)CaDiCaL version: 2.1.3 % 112.41/16.44 % (3818435)Termination reason: Instruction limit % 112.41/16.44 % (3818435)Termination phase: Saturation % 112.41/16.44 % (3818435)Time elapsed: 1.713 s % 112.41/16.44 % (3818435)Peak memory usage: 91 MB % 112.41/16.44 % (3818435)Instructions burned: 8143 (million) % 112.41/16.44 % (3818442)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=105142420:cond=fast:i=32078:fgj=on:av=off_2901 on theBenchmark for (2901ds/32078Mi) % 112.41/16.44 % (3818441)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=118906505:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2901 on theBenchmark for (2901ds/9885Mi) % 112.41/16.44 % Exception at run slice level % 112.41/16.44 User error: GNN currently only supports monomorphic FOL. % 112.41/16.44 % Exception at run slice level % 112.41/16.44 User error: GNN currently only supports monomorphic FOL. % 112.41/16.44 % (3818446)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=2697403327:cond=on:i=13220:s2at=3:aac=none:fsd=on_2897 on theBenchmark for (2897ds/13220Mi) % 112.41/16.44 % (3818445)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=1746228844:i=11101:bd=all:ss=axioms:sgt=8_2897 on theBenchmark for (2897ds/11101Mi) % 112.41/16.44 % Exception at run slice level % 112.41/16.44 User error: GNN currently only supports monomorphic FOL. % 112.41/16.44 % (3818449)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=2197867192:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2894 on theBenchmark for (2894ds/13528Mi) % 112.41/16.44 % Exception at run slice level % 112.41/16.44 User error: GNN currently only supports monomorphic FOL. % 112.41/16.44 % (3818451)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=2760047759:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2891 on theBenchmark for (2891ds/14854Mi) % 112.41/16.44 % (3818325)Instruction limit reached! % 112.41/16.44 % (3818325)------------------------------ % 112.41/16.44 % (3818325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.41/16.44 % (3818325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.41/16.44 % (3818325)CaDiCaL version: 2.1.3 % 112.41/16.44 % (3818325)Termination reason: Instruction limit % 112.41/16.44 % (3818325)Termination phase: Saturation % 112.41/16.44 % (3818325)Time elapsed: 7.834 s % 112.41/16.44 % (3818325)Peak memory usage: 289 MB % 112.41/16.44 % (3818325)Instructions burned: 26474 (million) % 112.41/16.44 % Exception at run slice level % 112.41/16.44 User error: GNN currently only supports monomorphic FOL. % 112.41/16.44 % (3818454)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=2034147003:i=33081:aac=none:fgj=on:bd=all:fsr=off_2888 on theBenchmark for (2888ds/33081Mi) % 112.41/16.44 % (3818453)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=3629388469:i=14974:ss=axioms:sgt=16_2888 on theBenchmark for (2888ds/14974Mi) % 112.41/16.44 % Exception at run slice level % 112.41/16.44 User error: GNN currently only supports monomorphic FOL. % 112.41/16.44 % Exception at run slice level % 112.41/16.44 User error: GNN currently only supports monomorphic FOL. % 112.41/16.44 % (3818458)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=3612961708:i=69865_2884 on theBenchmark for (2884ds/69865Mi) % 112.41/16.44 % (3818457)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=1062568630:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2884 on theBenchmark for (2884ds/50856Mi) % 112.41/16.44 % (3818432)Instruction limit reached! % 125.12/18.24 % (3818432)------------------------------ % 125.12/18.24 % (3818432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 125.12/18.24 % (3818432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.12/18.24 % (3818432)CaDiCaL version: 2.1.3 % 125.12/18.24 % (3818432)Termination reason: Instruction limit % 125.12/18.24 % (3818432)Termination phase: Saturation % 125.12/18.24 % (3818432)Time elapsed: 3.916 s % 125.12/18.24 % (3818432)Peak memory usage: 107 MB % 125.12/18.24 % (3818432)Instructions burned: 15999 (million) % 125.12/18.24 % Exception at run slice level% Exception at run slice level % 125.12/18.24 % 125.12/18.24 User error: User error: GNN currently only supports monomorphic FOL.GNN currently only supports monomorphic FOL. % 125.12/18.24 % 125.12/18.24 % (3818461)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=347944244:cond=fast:i=17802:gtgl=3:gtg=all_2881 on theBenchmark for (2881ds/17802Mi) % 125.12/18.24 % Exception at run slice level % 125.12/18.24 User error: Immediate (shared) subterms of term/literal aa(X1,fun(list(X1),X0),X4,X3) = sF14(X1,X0,X4,X3) have different types/not well-typed! % 125.12/18.24 % (3818463)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 125.12/18.24 % (3818463)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=1889932668:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2881 on theBenchmark for (2881ds/21161Mi) % 125.12/18.24 % (3818462)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=872021993:i=96644_2881 on theBenchmark for (2881ds/96644Mi) % 125.12/18.24 % (3818465)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=3773590277:i=22761:gtg=all:ss=axioms:fsd=on_2880 on theBenchmark for (2880ds/22761Mi) % 125.12/18.24 % Exception at run slice level % 125.12/18.24 User error: GNN currently only supports monomorphic FOL. % 125.12/18.24 % (3818469)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=2061163959:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2877 on theBenchmark for (2877ds/23713Mi) % 125.12/18.24 % (3818299)Instruction limit reached! % 125.12/18.24 % (3818299)------------------------------ % 125.12/18.24 % (3818299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 125.12/18.24 % (3818299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.12/18.24 % (3818299)CaDiCaL version: 2.1.3 % 125.12/18.24 % (3818299)Termination reason: Instruction limit % 125.12/18.24 % (3818299)Termination phase: Saturation % 125.12/18.24 % (3818299)Time elapsed: 10.132 s % 125.12/18.24 % (3818299)Peak memory usage: 162 MB % 125.12/18.24 % (3818299)Instructions burned: 33335 (million) % 125.12/18.24 % (3818471)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=715469717:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2873 on theBenchmark for (2873ds/26509Mi) % 125.12/18.24 % Exception at run slice level % 125.12/18.24 User error: GNN currently only supports monomorphic FOL. % 125.12/18.24 % (3818473)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=3493587372:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2870 on theBenchmark for (2870ds/28957Mi) % 125.12/18.24 % (3818445)Instruction limit reached! % 125.12/18.24 % (3818445)------------------------------ % 125.12/18.24 % (3818445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 125.12/18.24 % (3818445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.12/18.24 % (3818445)CaDiCaL version: 2.1.3 % 125.12/18.24 % (3818445)Termination reason: Instruction limit % 125.12/18.24 % (3818445)Termination phase: Saturation % 125.12/18.24 % (3818445)Time elapsed: 2.834 s % 125.12/18.24 % (3818445)Peak memory usage: 108 MB % 125.12/18.24 % (3818445)Instructions burned: 11106 (million) % 125.12/18.24 % (3818419)Instruction limit reached! % 125.12/18.24 % (3818419)------------------------------ % 125.12/18.24 % (3818419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 125.12/18.24 % (3818419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.12/18.24 % (3818419)CaDiCaL version: 2.1.3 % 125.12/18.24 % (3818419)Termination reason: Instruction limit % 125.12/18.24 % (3818419)Termination phase: Saturation % 128.94/18.82 % (3818419)Time elapsed: 5.996 s % 128.94/18.82 % (3818419)Peak memory usage: 152 MB % 128.94/18.82 % (3818419)Instructions burned: 19913 (million) % 128.94/18.82 % (3818475)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=3013753978:i=29246:s2at=-1:kws=inv_arity:ins=10_2868 on theBenchmark for (2868ds/29246Mi) % 128.94/18.82 % (3818476)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=260771776:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2868 on theBenchmark for (2868ds/30082Mi) % 128.94/18.82 % (3818476)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 128.94/18.82 % Exception at run slice level % 128.94/18.82 User error: GNN currently only supports monomorphic FOL. % 128.94/18.82 % Exception at run slice level % 128.94/18.82 User error: GNN currently only supports monomorphic FOL. % 128.94/18.82 % (3818479)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=3193030775:i=32262:bd=preordered_2865 on theBenchmark for (2865ds/32262Mi) % 128.94/18.82 % (3818480)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=1819014867:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2864 on theBenchmark for (2864ds/32870Mi) % 128.94/18.82 % Exception at run slice level % 128.94/18.82 User error: GNN currently only supports monomorphic FOL. % 128.94/18.82 % Exception at run slice level % 128.94/18.82 User error: GNN currently only supports monomorphic FOL. % 128.94/18.82 % (3818483)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=3321840292:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2861 on theBenchmark for (2861ds/33295Mi) % 128.94/18.82 % (3818484)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=2503900793:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2861 on theBenchmark for (2861ds/36826Mi) % 128.94/18.82 % Exception at run slice level % 128.94/18.82 User error: GNN currently only supports monomorphic FOL. % 128.94/18.82 % (3818487)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=3995188711:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2858 on theBenchmark for (2858ds/92981Mi) % 128.94/18.82 % Exception at run slice level % 128.94/18.82 User error: GNN currently only supports monomorphic FOL. % 128.94/18.82 % (3818489)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=4193320809:s2pl=on:i=49423_2855 on theBenchmark for (2855ds/49423Mi) % 128.94/18.82 % Exception at run slice level % 128.94/18.82 User error: GNN currently only supports monomorphic FOL. % 128.94/18.82 % (3818492)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=2603048366:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2852 on theBenchmark for (2852ds/57299Mi) % 128.94/18.82 % Exception at run slice level % 128.94/18.82 User error: GNN currently only supports monomorphic FOL. % 128.94/18.82 % (3818494)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=688707569:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2848 on theBenchmark for (2848ds/127679Mi) % 128.94/18.82 % Exception at run slice level % 128.94/18.82 User error: GNN currently only supports monomorphic FOL. % 128.94/18.82 % (3818496)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=1387877472:i=69402:add=on:aac=none:fsr=off_2845 on theBenchmark for (2845ds/69402Mi) % 128.94/18.82 % Exception at run slice level % 128.94/18.82 User error: GNN currently only supports monomorphic FOL. % 128.94/18.82 % (3818498)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=3414501062:i=100512:doe=on:fgj=on:bd=all:fsd=on_2842 on theBenchmark for (2842ds/100512Mi) % 128.94/18.82 % Exception at run slice level % 132.28/19.27 User error: GNN currently only supports monomorphic FOL. % 132.28/19.27 % (3818500)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=3127590003:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2838 on theBenchmark for (2838ds/138761Mi) % 132.28/19.27 % Exception at run slice level % 132.28/19.27 User error: GNN currently only supports monomorphic FOL. % 132.28/19.27 % (3818502)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=2151734338:i=282386:rtra=on_2835 on theBenchmark for (2835ds/282386Mi) % 132.28/19.27 % Exception at run slice level % 132.28/19.27 User error: GNN currently only supports monomorphic FOL. % 132.28/19.27 % (3818504)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=3410249805:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2832 on theBenchmark for (2832ds/269354Mi) % 132.28/19.27 % Exception at run slice level % 132.28/19.27 User error: GNN currently only supports monomorphic FOL. % 132.28/19.27 % (3818506)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=2419813444:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2828 on theBenchmark for (2828ds/283390Mi) % 132.28/19.27 % (3818506)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 132.28/19.27 % Exception at run slice level % 132.28/19.27 User error: GNN currently only supports monomorphic FOL. % 132.28/19.27 % (3818469)Instruction limit reached! % 132.28/19.27 % (3818469)------------------------------ % 132.28/19.27 % (3818469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.28/19.27 % (3818469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.28/19.27 % (3818469)CaDiCaL version: 2.1.3 % 132.28/19.27 % (3818469)Termination reason: Instruction limit % 132.28/19.27 % (3818469)Termination phase: Saturation % 132.28/19.27 % (3818469)Time elapsed: 5.128 s % 132.28/19.27 % (3818469)Peak memory usage: 249 MB % 132.28/19.27 % (3818469)Instructions burned: 23715 (million) % 132.28/19.27 % (3818508)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=3074226927:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2825 on theBenchmark for (2825ds/218Mi) % 132.28/19.27 % (3818508)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 132.28/19.27 % (3818508)Refutation not found, incomplete strategy % 132.28/19.27 % (3818508)------------------------------ % 132.28/19.27 % (3818508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.28/19.27 % (3818508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.28/19.27 % (3818508)CaDiCaL version: 2.1.3 % 132.28/19.27 % (3818508)Termination reason: Refutation not found, incomplete strategy % 132.28/19.27 % (3818508)Time elapsed: 0.001 s % 132.28/19.27 % (3818508)Peak memory usage: 88 MB % 132.28/19.27 % (3818508)Instructions burned: 1 (million) % 132.28/19.27 % (3818509)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=3073291452:i=238:av=off:rtra=on:ss=axioms_2824 on theBenchmark for (2824ds/238Mi) % 132.28/19.27 % (3818509)Instruction limit reached! % 132.28/19.27 % (3818509)------------------------------ % 132.28/19.27 % (3818509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.28/19.27 % (3818509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.28/19.27 % (3818509)CaDiCaL version: 2.1.3 % 132.28/19.27 % (3818509)Termination reason: Instruction limit % 132.28/19.27 % (3818509)Termination phase: Saturation % 132.28/19.27 % (3818509)Time elapsed: 0.065 s % 132.28/19.27 % (3818509)Peak memory usage: 88 MB % 132.28/19.27 % (3818509)Instructions burned: 239 (million) % 132.28/19.27 % (3818508)------------------------------ % 132.28/19.27 % (3818508)------------------------------ % 132.28/19.27 % (3818512)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=3839942352:s2a=on:i=278:rtra=on:gtg=position_2823 on theBenchmark for (2823ds/278Mi) % 132.28/19.27 % (3818513)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=914838877:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2822 on theBenchmark for (2822ds/258Mi) % 132.28/19.27 % (3818512)Instruction limit reached! % 132.28/19.27 % (3818512)------------------------------ % 132.28/19.27 % (3818512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.54/20.05 % (3818512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.54/20.05 % (3818512)CaDiCaL version: 2.1.3 % 124.54/20.05 % (3818512)Termination reason: Instruction limit % 124.54/20.05 % (3818512)Termination phase: Saturation % 124.54/20.05 % (3818512)Time elapsed: 0.099 s % 124.54/20.05 % (3818512)Peak memory usage: 91 MB % 124.54/20.05 % (3818512)Instructions burned: 279 (million) % 124.54/20.05 % (3818513)Instruction limit reached! % 124.54/20.05 % (3818513)------------------------------ % 124.54/20.05 % (3818513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.54/20.05 % (3818513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.54/20.05 % (3818513)CaDiCaL version: 2.1.3 % 124.54/20.05 % (3818513)Termination reason: Instruction limit % 124.54/20.05 % (3818513)Termination phase: Saturation % 124.54/20.05 % (3818513)Time elapsed: 0.081 s % 124.54/20.05 % (3818513)Peak memory usage: 92 MB % 124.54/20.05 % (3818513)Instructions burned: 261 (million) % 124.54/20.05 % (3818516)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=291825020:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2820 on theBenchmark for (2820ds/570Mi) % 124.54/20.05 % (3818517)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=3799833232:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2820 on theBenchmark for (2820ds/314Mi) % 124.54/20.05 % (3818517)Refutation not found, incomplete strategy % 124.54/20.05 % (3818517)------------------------------ % 124.54/20.05 % (3818517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.54/20.05 % (3818517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.54/20.05 % (3818517)CaDiCaL version: 2.1.3 % 124.54/20.05 % (3818517)Termination reason: Refutation not found, incomplete strategy % 124.54/20.05 % (3818517)Time elapsed: 0.001 s % 124.54/20.05 % (3818517)Peak memory usage: 88 MB % 124.54/20.05 % (3818517)Instructions burned: 2 (million) % 124.54/20.05 % (3818516)Instruction limit reached! % 124.54/20.05 % (3818516)------------------------------ % 124.54/20.05 % (3818516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.54/20.05 % (3818516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.54/20.05 % (3818516)CaDiCaL version: 2.1.3 % 124.54/20.05 % (3818516)Termination reason: Instruction limit % 124.54/20.05 % (3818516)Termination phase: Saturation % 124.54/20.05 % (3818516)Time elapsed: 0.158 s % 124.54/20.05 % (3818516)Peak memory usage: 90 MB % 124.54/20.05 % (3818516)Instructions burned: 572 (million) % 124.54/20.05 % (3818517)------------------------------ % 124.54/20.05 % (3818517)------------------------------ % 124.54/20.05 % (3818463)Instruction limit reached! % 124.54/20.05 % (3818463)------------------------------ % 124.54/20.05 % (3818463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.54/20.05 % (3818463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.54/20.05 % (3818463)CaDiCaL version: 2.1.3 % 124.54/20.05 % (3818463)Termination reason: Instruction limit % 124.54/20.05 % (3818463)Termination phase: Saturation % 124.54/20.05 % (3818463)Time elapsed: 6.286 s % 124.54/20.05 % (3818463)Peak memory usage: 164 MB % 124.54/20.05 % (3818463)Instructions burned: 21161 (million) % 124.54/20.05 % (3818520)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=743090813:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2817 on theBenchmark for (2817ds/650Mi) % 124.54/20.05 % (3818521)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=4090357494:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2817 on theBenchmark for (2817ds/496Mi) % 124.54/20.05 % (3818522)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=3866438694:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2817 on theBenchmark for (2817ds/588Mi) % 124.54/20.05 % (3818522)Refutation not found, incomplete strategy % 124.54/20.05 % (3818522)------------------------------ % 124.54/20.05 % (3818522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.54/20.05 % (3818522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.54/20.05 % (3818522)CaDiCaL version: 2.1.3 % 124.54/20.05 % (3818522)Termination reason: Refutation not found, incomplete strategy % 124.54/20.05 % (3818522)Time elapsed: 0.006 s % 124.54/20.05 % (3818522)Peak memory usage: 89 MB % 124.54/20.05 % (3818522)Instructions burned: 19 (million) % 124.54/20.05 % (3818521)Instruction limit reached! % 124.54/20.05 % (3818521)------------------------------ % 124.54/20.05 % (3818521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.54/20.05 % (3818521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.61/20.41 % (3818521)CaDiCaL version: 2.1.3 % 140.61/20.41 % (3818521)Termination reason: Instruction limit % 140.61/20.41 % (3818521)Termination phase: Saturation % 140.61/20.41 % (3818521)Time elapsed: 0.140 s % 140.61/20.41 % (3818521)Peak memory usage: 92 MB % 140.61/20.41 % (3818521)Instructions burned: 496 (million) % 140.61/20.41 % (3818520)Instruction limit reached! % 140.61/20.41 % (3818520)------------------------------ % 140.61/20.41 % (3818520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.61/20.41 % (3818520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.61/20.41 % (3818520)CaDiCaL version: 2.1.3 % 140.61/20.41 % (3818520)Termination reason: Instruction limit % 140.61/20.41 % (3818520)Termination phase: Saturation % 140.61/20.41 % (3818520)Time elapsed: 0.200 s % 140.61/20.41 % (3818520)Peak memory usage: 92 MB % 140.61/20.41 % (3818520)Instructions burned: 652 (million) % 140.61/20.41 % (3818522)------------------------------ % 140.61/20.41 % (3818522)------------------------------ % 140.61/20.41 % (3818526)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=1271260142:i=4700:rtra=on_2815 on theBenchmark for (2815ds/4700Mi) % 140.61/20.41 % (3818527)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3827686838:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2814 on theBenchmark for (2814ds/226Mi) % 140.61/20.41 % (3818527)Refutation not found, incomplete strategy % 140.61/20.41 % (3818527)------------------------------ % 140.61/20.41 % (3818527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.61/20.41 % (3818527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.61/20.41 % (3818527)CaDiCaL version: 2.1.3 % 140.61/20.41 % (3818527)Termination reason: Refutation not found, incomplete strategy % 140.61/20.41 % (3818527)Time elapsed: 0.008 s % 140.61/20.41 % (3818527)Peak memory usage: 89 MB % 140.61/20.41 % (3818527)Instructions burned: 25 (million) % 140.61/20.41 % (3818528)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=482992771:i=254:av=off:fsr=off:rtra=on:sup=off_2814 on theBenchmark for (2814ds/254Mi) % 140.61/20.41 % (3818528)Refutation not found, incomplete strategy % 140.61/20.41 % (3818528)------------------------------ % 140.61/20.41 % (3818528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.61/20.41 % (3818528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.61/20.41 % (3818528)CaDiCaL version: 2.1.3 % 140.61/20.41 % (3818528)Termination reason: Refutation not found, incomplete strategy % 140.61/20.41 % (3818528)Time elapsed: 0.005 s % 140.61/20.41 % (3818528)Peak memory usage: 88 MB % 140.61/20.41 % (3818528)Instructions burned: 19 (million) % 140.61/20.41 % (3818527)------------------------------ % 140.61/20.41 % (3818527)------------------------------ % 140.61/20.41 % Exception at run slice level % 140.61/20.41 User error: GNN currently only supports monomorphic FOL. % 140.61/20.41 % (3818528)------------------------------ % 140.61/20.41 % (3818528)------------------------------ % 140.61/20.41 % (3818533)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=2448203549:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2811 on theBenchmark for (2811ds/1814Mi) % 140.61/20.41 % (3818532)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=3734338446:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2812 on theBenchmark for (2812ds/228Mi) % 140.61/20.41 % (3818532)Refutation not found, incomplete strategy % 140.61/20.41 % (3818532)------------------------------ % 140.61/20.41 % (3818532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.61/20.41 % (3818532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.61/20.41 % (3818532)CaDiCaL version: 2.1.3 % 140.61/20.41 % (3818532)Termination reason: Refutation not found, incomplete strategy % 140.61/20.41 % (3818532)Time elapsed: 0.007 s % 140.61/20.41 % (3818532)Peak memory usage: 88 MB % 140.61/20.41 % (3818532)Instructions burned: 22 (million) % 140.61/20.41 % (3818534)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=482543982:i=874:sd=1:aac=none:rtra=on:ss=included_2811 on theBenchmark for (2811ds/874Mi) % 140.61/20.41 % (3818534)Refutation not found, incomplete strategy % 140.61/20.41 % (3818534)------------------------------ % 140.61/20.41 % (3818534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.61/20.41 % (3818534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.61/20.41 % (3818534)CaDiCaL version: 2.1.3 % 140.61/20.41 % (3818534)Termination reason: Refutation not found, incomplete strategy % 144.06/20.99 % (3818534)Time elapsed: 0.005 s % 144.06/20.99 % (3818534)Peak memory usage: 89 MB % 144.06/20.99 % (3818534)Instructions burned: 14 (million) % 144.06/20.99 % (3818532)------------------------------ % 144.06/20.99 % (3818532)------------------------------ % 144.06/20.99 % (3818534)------------------------------ % 144.06/20.99 % (3818534)------------------------------ % 144.06/20.99 % (3818538)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=3926351481:i=10404:rtra=on:ss=axioms:sgt=16_2809 on theBenchmark for (2809ds/10404Mi) % 144.06/20.99 % (3818539)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=256310741:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2809 on theBenchmark for (2809ds/268Mi) % 144.06/20.99 % (3818539)Instruction limit reached! % 144.06/20.99 % (3818539)------------------------------ % 144.06/20.99 % (3818539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 144.06/20.99 % (3818539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.06/20.99 % (3818539)CaDiCaL version: 2.1.3 % 144.06/20.99 % (3818539)Termination reason: Instruction limit % 144.06/20.99 % (3818539)Termination phase: Saturation % 144.06/20.99 % (3818539)Time elapsed: 0.076 s % 144.06/20.99 % (3818539)Peak memory usage: 91 MB % 144.06/20.99 % (3818539)Instructions burned: 270 (million) % 144.06/20.99 % Exception at run slice level % 144.06/20.99 User error: GNN currently only supports monomorphic FOL. % 144.06/20.99 % (3818542)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=1523744023:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2807 on theBenchmark for (2807ds/1184Mi) % 144.06/20.99 % (3818533)Instruction limit reached! % 144.06/20.99 % (3818533)------------------------------ % 144.06/20.99 % (3818533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 144.06/20.99 % (3818533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.06/20.99 % (3818533)CaDiCaL version: 2.1.3 % 144.06/20.99 % (3818533)Termination reason: Instruction limit % 144.06/20.99 % (3818533)Termination phase: Saturation % 144.06/20.99 % (3818533)Time elapsed: 0.525 s % 144.06/20.99 % (3818533)Peak memory usage: 93 MB % 144.06/20.99 % (3818533)Instructions burned: 1814 (million) % 144.06/20.99 % (3818543)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=3677527762:st=3:i=26386:sd=3:rtra=on:ss=axioms_2806 on theBenchmark for (2806ds/26386Mi) % 144.06/20.99 % (3818545)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=184776997:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2805 on theBenchmark for (2805ds/250Mi) % 144.06/20.99 % (3818545)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 144.06/20.99 % (3818545)Instruction limit reached! % 144.06/20.99 % (3818545)------------------------------ % 144.06/20.99 % (3818545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 144.06/20.99 % (3818545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.06/20.99 % (3818545)CaDiCaL version: 2.1.3 % 144.06/20.99 % (3818545)Termination reason: Instruction limit % 144.06/20.99 % (3818545)Termination phase: Saturation % 144.06/20.99 % (3818545)Time elapsed: 0.063 s % 144.06/20.99 % (3818545)Peak memory usage: 90 MB % 144.06/20.99 % (3818545)Instructions burned: 252 (million) % 144.06/20.99 % (3818394)Instruction limit reached! % 144.06/20.99 % (3818394)------------------------------ % 144.06/20.99 % (3818394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 144.06/20.99 % (3818394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.06/20.99 % (3818394)CaDiCaL version: 2.1.3 % 144.06/20.99 % (3818394)Termination reason: Instruction limit % 144.06/20.99 % (3818394)Termination phase: Saturation % 144.06/20.99 % (3818394)Time elapsed: 13.454 s % 144.06/20.99 % (3818394)Peak memory usage: 169 MB % 144.06/20.99 % (3818394)Instructions burned: 43700 (million) % 144.06/20.99 % Exception at run slice level % 144.06/20.99 User error: GNN currently only supports monomorphic FOL. % 144.06/20.99 % (3818542)Instruction limit reached! % 144.06/20.99 % (3818542)------------------------------ % 144.06/20.99 % (3818542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 144.06/20.99 % (3818542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.06/20.99 % (3818542)CaDiCaL version: 2.1.3 % 144.06/20.99 % (3818542)Termination reason: Instruction limit % 144.06/20.99 % (3818542)Termination phase: Saturation % 151.20/21.97 % (3818542)Time elapsed: 0.306 s % 151.20/21.97 % (3818542)Peak memory usage: 92 MB % 151.20/21.97 % (3818542)Instructions burned: 1188 (million) % 151.20/21.97 % (3818548)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=3751495873:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2803 on theBenchmark for (2803ds/268Mi) % 151.20/21.97 % Exception at run slice level % 151.20/21.97 User error: Immediate (shared) subterms of term/literal aa(X1,fun(list(X1),X0),X5,X2) = sF17(X1,X0,X5,X2) have different types/not well-typed! % 151.20/21.97 % (3818549)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3140404605:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2803 on theBenchmark for (2803ds/282Mi) % 151.20/21.97 % (3818549)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 151.20/21.97 % (3818549)Refutation not found, incomplete strategy % 151.20/21.97 % (3818549)------------------------------ % 151.20/21.97 % (3818549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.20/21.97 % (3818549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.20/21.97 % (3818549)CaDiCaL version: 2.1.3 % 151.20/21.97 % (3818549)Termination reason: Refutation not found, incomplete strategy % 151.20/21.97 % (3818549)Time elapsed: 0.001 s % 151.20/21.97 % (3818549)Peak memory usage: 88 MB % 151.20/21.97 % (3818549)Instructions burned: 1 (million) % 151.20/21.97 % (3818550)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=2514467969:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2802 on theBenchmark for (2802ds/862Mi) % 151.20/21.97 % (3818550)Refutation not found, incomplete strategy % 151.20/21.97 % (3818550)------------------------------ % 151.20/21.97 % (3818550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.20/21.97 % (3818550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.20/21.97 % (3818550)CaDiCaL version: 2.1.3 % 151.20/21.97 % (3818550)Termination reason: Refutation not found, incomplete strategy % 151.20/21.97 % (3818550)Time elapsed: 0.002 s % 151.20/21.97 % (3818550)Peak memory usage: 89 MB % 151.20/21.97 % (3818550)Instructions burned: 4 (million) % 151.20/21.97 % (3818551)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=1003432072:i=12120:aac=none:ins=25:rtra=on_2802 on theBenchmark for (2802ds/12120Mi) % 151.20/21.97 % (3818553)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=1142073883:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2802 on theBenchmark for (2802ds/300Mi) % 151.20/21.97 % (3818553)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 151.20/21.97 % (3818549)------------------------------ % 151.20/21.97 % (3818549)------------------------------ % 151.20/21.97 % (3818550)------------------------------ % 151.20/21.97 % (3818550)------------------------------ % 151.20/21.97 % (3818553)Instruction limit reached! % 151.20/21.97 % (3818553)------------------------------ % 151.20/21.97 % (3818553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.20/21.97 % (3818553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.20/21.97 % (3818553)CaDiCaL version: 2.1.3 % 151.20/21.97 % (3818553)Termination reason: Instruction limit % 151.20/21.97 % (3818553)Termination phase: Saturation % 151.20/21.97 % (3818553)Time elapsed: 0.096 s % 151.20/21.97 % (3818553)Peak memory usage: 92 MB % 151.20/21.97 % (3818553)Instructions burned: 300 (million) % 151.20/21.97 % Exception at run slice level % 151.20/21.97 User error: GNN currently only supports monomorphic FOL. % 151.20/21.97 % (3818558)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=2194814797:i=28310:bd=all:rtra=on_2800 on theBenchmark for (2800ds/28310Mi) % 151.20/21.97 % (3818559)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=840433717:i=1334:av=off:fsr=off:rtra=on_2800 on theBenchmark for (2800ds/1334Mi) % 151.20/21.97 % (3818559)Refutation not found, incomplete strategy % 151.20/21.97 % (3818559)------------------------------ % 151.20/21.97 % (3818559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.20/21.97 % (3818559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.20/21.97 % (3818559)CaDiCaL version: 2.1.3 % 156.05/22.79 % (3818559)Termination reason: Refutation not found, incomplete strategy % 156.05/22.79 % (3818559)Time elapsed: 0.006 s % 156.05/22.79 % (3818559)Peak memory usage: 89 MB % 156.05/22.79 % (3818559)Instructions burned: 21 (million) % 156.05/22.79 % (3818560)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=2381520117:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2800 on theBenchmark for (2800ds/370Mi) % 156.05/22.79 % (3818561)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=1799505027:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2799 on theBenchmark for (2799ds/386Mi) % 156.05/22.79 % (3818560)Instruction limit reached! % 156.05/22.79 % (3818560)------------------------------ % 156.05/22.79 % (3818560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.05/22.79 % (3818560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.05/22.79 % (3818560)CaDiCaL version: 2.1.3 % 156.05/22.79 % (3818560)Termination reason: Instruction limit % 156.05/22.79 % (3818560)Termination phase: Saturation % 156.05/22.79 % (3818560)Time elapsed: 0.116 s % 156.05/22.79 % (3818560)Peak memory usage: 92 MB % 156.05/22.79 % (3818560)Instructions burned: 370 (million) % 156.05/22.79 % (3818559)------------------------------ % 156.05/22.79 % (3818559)------------------------------ % 156.05/22.79 % Exception at run slice level % 156.05/22.79 User error: GNN currently only supports monomorphic FOL. % 156.05/22.79 % (3818561)Instruction limit reached! % 156.05/22.79 % (3818561)------------------------------ % 156.05/22.79 % (3818561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.05/22.79 % (3818561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.05/22.79 % (3818561)CaDiCaL version: 2.1.3 % 156.05/22.79 % (3818561)Termination reason: Instruction limit % 156.05/22.79 % (3818561)Termination phase: Saturation % 156.05/22.79 % (3818561)Time elapsed: 0.115 s % 156.05/22.79 % (3818561)Peak memory usage: 91 MB % 156.05/22.79 % (3818561)Instructions burned: 388 (million) % 156.05/22.79 % (3818566)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=2422791724:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2797 on theBenchmark for (2797ds/9700Mi) % 156.05/22.79 % (3818566)Refutation not found, incomplete strategy % 156.05/22.79 % (3818566)------------------------------ % 156.05/22.79 % (3818566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.05/22.79 % (3818566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.05/22.79 % (3818566)CaDiCaL version: 2.1.3 % 156.05/22.79 % (3818566)Termination reason: Refutation not found, incomplete strategy % 156.05/22.79 % (3818566)Time elapsed: 0.005 s % 156.05/22.79 % (3818566)Peak memory usage: 88 MB % 156.05/22.79 % (3818566)Instructions burned: 14 (million) % 156.05/22.79 % (3818567)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=3802335962:i=24222:sd=1:rtra=on:ss=included_2797 on theBenchmark for (2797ds/24222Mi) % 156.05/22.79 % (3818568)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=763762649:i=638:kws=precedence:fsr=off:rtra=on_2797 on theBenchmark for (2797ds/638Mi) % 156.05/22.79 % (3818569)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2312751881:i=4128:ep=RST:rtra=on_2797 on theBenchmark for (2797ds/4128Mi) % 156.05/22.79 % (3818566)------------------------------ % 156.05/22.79 % (3818566)------------------------------ % 156.05/22.79 % (3818568)Instruction limit reached! % 156.05/22.79 % (3818568)------------------------------ % 156.05/22.79 % (3818568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.05/22.79 % (3818568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.05/22.79 % (3818568)CaDiCaL version: 2.1.3 % 156.05/22.79 % (3818568)Termination reason: Instruction limit % 156.05/22.79 % (3818568)Termination phase: Saturation % 156.05/22.79 % (3818568)Time elapsed: 0.153 s % 156.05/22.79 % (3818568)Peak memory usage: 90 MB % 156.05/22.79 % (3818568)Instructions burned: 640 (million) % 156.05/22.79 % Exception at run slice level % 156.05/22.79 User error: GNN currently only supports monomorphic FOL. % 156.05/22.79 % (3818574)dis-1011_128_sil=32000:si=on:random_seed=3027832458:i=7412:ep=RST:av=off:rtra=on_2795 on theBenchmark for (2795ds/7412Mi) % 156.05/22.79 % (3818575)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3455352503:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2794 on theBenchmark for (2794ds/1514Mi) % 162.61/23.76 % (3818576)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=4126102702:i=27826:rtra=on:ss=axioms:sgt=8_2794 on theBenchmark for (2794ds/27826Mi) % 162.61/23.76 % (3818575)Refutation not found, incomplete strategy % 162.61/23.76 % (3818575)------------------------------ % 162.61/23.76 % (3818575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.61/23.76 % (3818575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.61/23.76 % (3818575)CaDiCaL version: 2.1.3 % 162.61/23.76 % (3818575)Termination reason: Refutation not found, incomplete strategy % 162.61/23.76 % (3818575)Time elapsed: 0.006 s % 162.61/23.76 % (3818575)Peak memory usage: 88 MB % 162.61/23.76 % (3818575)Instructions burned: 18 (million) % 162.61/23.76 % (3818575)------------------------------ % 162.61/23.76 % (3818575)------------------------------ % 162.61/23.76 % Exception at run slice level % 162.61/23.76 User error: GNN currently only supports monomorphic FOL. % 162.61/23.76 % (3818580)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=4200403313:i=19850:aac=none:rtra=on_2791 on theBenchmark for (2791ds/19850Mi) % 162.61/23.76 % (3818581)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1256197159:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2791 on theBenchmark for (2791ds/4958Mi) % 162.61/23.76 % (3818581)Refutation not found, incomplete strategy % 162.61/23.76 % (3818581)------------------------------ % 162.61/23.76 % (3818581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.61/23.76 % (3818581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.61/23.76 % (3818581)CaDiCaL version: 2.1.3 % 162.61/23.76 % (3818581)Termination reason: Refutation not found, incomplete strategy % 162.61/23.76 % (3818581)Time elapsed: 0.002 s % 162.61/23.76 % (3818581)Peak memory usage: 89 MB % 162.61/23.76 % (3818581)Instructions burned: 2 (million) % 162.61/23.76 % Exception at run slice level % 162.61/23.76 User error: GNN currently only supports monomorphic FOL. % 162.61/23.76 % (3818581)------------------------------ % 162.61/23.76 % (3818581)------------------------------ % 162.61/23.76 % (3818585)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=3658919654:st=1.5:i=22290:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2788 on theBenchmark for (2788ds/22290Mi) % 162.61/23.76 % (3818584)ott+1002_64_sil=16000:si=on:sp=const_min:nwc=0.5:random_seed=3919634378:i=880:nm=2:av=off:rtra=on:gtg=exists_all:fdi=8:gsp=on_2788 on theBenchmark for (2788ds/880Mi) % 162.61/23.76 % (3818584)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 162.61/23.76 % (3818569)Instruction limit reached! % 162.61/23.76 % (3818569)------------------------------ % 162.61/23.76 % (3818569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.61/23.76 % (3818569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.61/23.76 % (3818569)CaDiCaL version: 2.1.3 % 162.61/23.76 % (3818569)Termination reason: Instruction limit % 162.61/23.76 % (3818569)Termination phase: Saturation % 162.61/23.76 % (3818569)Time elapsed: 1.023 s % 162.61/23.76 % (3818569)Peak memory usage: 96 MB % 162.61/23.76 % (3818569)Instructions burned: 4132 (million) % 162.61/23.76 % Exception at run slice level % 162.61/23.76 User error: GNN currently only supports monomorphic FOL. % 162.61/23.76 % (3818584)Instruction limit reached! % 162.61/23.76 % (3818584)------------------------------ % 162.61/23.76 % (3818584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.61/23.76 % (3818584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.61/23.76 % (3818584)CaDiCaL version: 2.1.3 % 162.61/23.76 % (3818584)Termination reason: Instruction limit % 162.61/23.76 % (3818584)Termination phase: Saturation % 162.61/23.76 % (3818584)Time elapsed: 0.253 s % 162.61/23.76 % (3818584)Peak memory usage: 89 MB % 162.61/23.76 % (3818584)Instructions burned: 882 (million) % 162.61/23.76 % (3818588)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=1767707956:cts=off:i=6068:av=off:rtra=on:er=known:fsd=on_2785 on theBenchmark for (2785ds/6068Mi) % 162.61/23.76 % (3818589)lrs-1011_64:1_sil=8000:si=on:erd=off:urr=on:nwc=0.7:br=off:random_seed=3796730630:st=2:s2a=on:i=1048:s2at=2:rtra=on:ss=axioms_2785 on theBenchmark for (2785ds/1048Mi) % 162.61/23.76 % (3818590)lrs+1011_16:1_sil=8000:si=on:acc=on:urr=on:fd=preordered:flr=on:random_seed=1556014961:avsq=on:i=2032:avsqr=676809,524288:sd=1:rtra=on:ss=axioms_2784 on theBenchmark for (2784ds/2032Mi) % 173.45/25.11 % Exception at run slice level % 173.45/25.11 User error: GNN currently only supports monomorphic FOL. % 173.45/25.11 % (3818589)Instruction limit reached! % 173.45/25.11 % (3818589)------------------------------ % 173.45/25.11 % (3818589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.45/25.11 % (3818589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.45/25.11 % (3818589)CaDiCaL version: 2.1.3 % 173.45/25.11 % (3818589)Termination reason: Instruction limit % 173.45/25.11 % (3818589)Termination phase: Saturation % 173.45/25.11 % (3818589)Time elapsed: 0.296 s % 173.45/25.11 % (3818589)Peak memory usage: 95 MB % 173.45/25.11 % (3818589)Instructions burned: 1048 (million) % 173.45/25.11 % (3818594)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:si=on:s2agt=16:random_seed=436777307:i=28246:bd=preordered:ins=4:rtra=on_2782 on theBenchmark for (2782ds/28246Mi) % 173.45/25.11 % (3818473)Instruction limit reached! % 173.45/25.11 % (3818473)------------------------------ % 173.45/25.11 % (3818473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.45/25.11 % (3818473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.45/25.11 % (3818473)CaDiCaL version: 2.1.3 % 173.45/25.11 % (3818473)Termination reason: Instruction limit % 173.45/25.11 % (3818473)Termination phase: Saturation % 173.45/25.11 % (3818473)Time elapsed: 8.929 s % 173.45/25.11 % (3818473)Peak memory usage: 192 MB % 173.45/25.11 % (3818473)Instructions burned: 28958 (million) % 173.45/25.11 % (3818595)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:si=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2742112360:i=11562:kws=precedence:bd=all:rtra=on:rawr=on_2781 on theBenchmark for (2781ds/11562Mi) % 173.45/25.11 % Exception at run slice level % 173.45/25.11 User error: GNN currently only supports monomorphic FOL. % 173.45/25.11 % (3818598)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=4270809799:i=4896:gtgl=5:bd=preordered:rtra=on:gtg=all_2779 on theBenchmark for (2779ds/4896Mi) % 173.45/25.11 % (3818574)Instruction limit reached! % 173.45/25.11 % (3818574)------------------------------ % 173.45/25.11 % (3818574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.45/25.11 % (3818574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.45/25.11 % (3818574)CaDiCaL version: 2.1.3 % 173.45/25.11 % (3818574)Termination reason: Instruction limit % 173.45/25.11 % (3818574)Termination phase: Saturation % 173.45/25.11 % (3818574)Time elapsed: 1.569 s % 173.45/25.11 % (3818574)Peak memory usage: 92 MB % 173.45/25.11 % (3818574)Instructions burned: 7416 (million) % 173.45/25.11 % (3818599)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:si=on:lcm=reverse:random_seed=3034014884:i=6446:kws=precedence:fgj=on:av=off:rtra=on_2779 on theBenchmark for (2779ds/6446Mi) % 173.45/25.11 % (3818590)Instruction limit reached! % 173.45/25.11 % (3818590)------------------------------ % 173.45/25.11 % (3818590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.45/25.11 % (3818590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.45/25.11 % (3818590)CaDiCaL version: 2.1.3 % 173.45/25.11 % (3818590)Termination reason: Instruction limit % 173.45/25.11 % (3818590)Termination phase: Saturation % 173.45/25.11 % (3818590)Time elapsed: 0.599 s % 173.45/25.11 % (3818590)Peak memory usage: 104 MB % 173.45/25.11 % (3818590)Instructions burned: 2034 (million) % 173.45/25.11 % (3818601)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:si=on:sp=occurrence:sos=on:random_seed=1849042468:st=5.6:i=4066:sd=3:rtra=on:ss=axioms_2778 on theBenchmark for (2778ds/4066Mi) % 173.45/25.11 % Exception at run slice level % 173.45/25.11 User error: GNN currently only supports monomorphic FOL. % 173.45/25.11 % (3818603)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:si=on:random_seed=3864962124:i=4110:nm=16:rtra=on:gtg=position:ss=axioms:fsd=on_2777 on theBenchmark for (2777ds/4110Mi) % 173.45/25.11 % Exception at run slice level % 173.45/25.11 User error: GNN currently only supports monomorphic FOL. % 173.45/25.11 % (3818605)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=1400408168:i=43222:sd=3:rtra=on:ss=axioms_2776 on theBenchmark for (2776ds/43222Mi) % 180.48/26.02 % Exception at run slice level % 180.48/26.02 User error: GNN currently only supports monomorphic FOL. % 180.48/26.02 % (3818607)lrs+10_1_sil=8000:si=on:sp=occurrence:sos=all:lma=off:random_seed=381041744:i=9670:sd=13:rtra=on:ss=axioms:sgt=23_2775 on theBenchmark for (2775ds/9670Mi) % 180.48/26.02 % (3818607)Refutation not found, incomplete strategy % 180.48/26.02 % (3818607)------------------------------ % 180.48/26.02 % (3818607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.48/26.02 % (3818607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.48/26.02 % (3818607)CaDiCaL version: 2.1.3 % 180.48/26.02 % (3818607)Termination reason: Refutation not found, incomplete strategy % 180.48/26.02 % (3818607)Time elapsed: 0.007 s % 180.48/26.02 % (3818607)Peak memory usage: 89 MB % 180.48/26.02 % (3818607)Instructions burned: 23 (million) % 180.48/26.02 % Exception at run slice level % 180.48/26.02 User error: GNN currently only supports monomorphic FOL. % 180.48/26.02 % (3818609)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=2716140805:st=5:i=1594:s2at=3:sd=4:bs=unit_only:av=off:rtra=on:sup=off:ss=included_2774 on theBenchmark for (2774ds/1594Mi) % 180.48/26.02 % Exception at run slice level % 180.48/26.02 User error: GNN currently only supports monomorphic FOL. % 180.48/26.02 % (3818611)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=316513382:i=4652:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:rtra=on:fsd=on_2774 on theBenchmark for (2774ds/4652Mi) % 180.48/26.02 % (3818607)------------------------------ % 180.48/26.02 % (3818607)------------------------------ % 180.48/26.02 % (3818611)Refutation not found, incomplete strategy % 180.48/26.02 % (3818611)------------------------------ % 180.48/26.02 % (3818611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.48/26.02 % (3818611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.48/26.02 % (3818611)CaDiCaL version: 2.1.3 % 180.48/26.02 % (3818611)Termination reason: Refutation not found, incomplete strategy % 180.48/26.02 % (3818611)Time elapsed: 0.010 s % 180.48/26.02 % (3818611)Peak memory usage: 89 MB % 180.48/26.02 % (3818611)Instructions burned: 29 (million) % 180.48/26.02 % (3818613)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:si=on:sos=all:urr=on:br=off:random_seed=2703680966:i=12076:nm=6:rtra=on_2773 on theBenchmark for (2773ds/12076Mi) % 180.48/26.02 % (3818615)lrs+10_1_sil=32000:si=on:sp=occurrence:random_seed=2156000283:st=2:i=66668:sd=3:rtra=on:ss=included:sgt=32_2772 on theBenchmark for (2772ds/66668Mi) % 180.48/26.02 % (3818611)------------------------------ % 180.48/26.02 % (3818611)------------------------------ % 180.48/26.02 % Exception at run slice level % 180.48/26.02 User error: GNN currently only supports monomorphic FOL. % 180.48/26.02 % (3818618)lrs+10_4_sil=8000:plsq=on:si=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2552970828:st=3.7:s2a=on:i=2016:s2at=1.2:sd=3:bd=all:av=off:rtra=on:fdi=8:sup=off:ss=axioms_2771 on theBenchmark for (2771ds/2016Mi) % 180.48/26.02 % (3818609)Instruction limit reached! % 180.48/26.02 % (3818609)------------------------------ % 180.48/26.02 % (3818609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.48/26.02 % (3818609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.48/26.02 % (3818609)CaDiCaL version: 2.1.3 % 180.48/26.02 % (3818609)Termination reason: Instruction limit % 180.48/26.02 % (3818609)Termination phase: Saturation % 180.48/26.02 % (3818609)Time elapsed: 0.361 s % 180.48/26.02 % (3818609)Peak memory usage: 90 MB % 180.48/26.02 % (3818609)Instructions burned: 1596 (million) % 180.48/26.02 % (3818619)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=1092567563:i=16654:s2at=5:bd=preordered:rtra=on_2770 on theBenchmark for (2770ds/16654Mi) % 180.48/26.02 % (3818621)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=1817141365:s2a=on:i=2166:s2at=1.87328:slsql=off:ep=RSTC:rtra=on:fdi=16_2769 on theBenchmark for (2769ds/2166Mi) % 180.48/26.02 % Exception at run slice level % 180.48/26.02 User error: GNN currently only supports monomorphic FOL. % 180.48/26.02 % (3818624)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:si=on:spb=goal:fd=preordered:random_seed=3040647537:i=2168:sd=1:bd=preordered:av=off:fsr=off:rtra=on:ss=axioms:sgt=14_2766 on theBenchmark for (2766ds/2168Mi) % 190.71/27.57 % (3818624)Refutation not found, incomplete strategy % 190.71/27.57 % (3818624)------------------------------ % 190.71/27.57 % (3818624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.71/27.57 % (3818624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.71/27.57 % (3818624)CaDiCaL version: 2.1.3 % 190.71/27.57 % (3818624)Termination reason: Refutation not found, incomplete strategy % 190.71/27.57 % (3818624)Time elapsed: 0.031 s % 190.71/27.57 % (3818624)Peak memory usage: 88 MB % 190.71/27.57 % (3818624)Instructions burned: 109 (million) % 190.71/27.57 % (3818618)Instruction limit reached! % 190.71/27.57 % (3818618)------------------------------ % 190.71/27.57 % (3818618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.71/27.57 % (3818618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.71/27.57 % (3818618)CaDiCaL version: 2.1.3 % 190.71/27.57 % (3818618)Termination reason: Instruction limit % 190.71/27.57 % (3818618)Termination phase: Saturation % 190.71/27.57 % (3818618)Time elapsed: 0.555 s % 190.71/27.57 % (3818618)Peak memory usage: 107 MB % 190.71/27.57 % (3818618)Instructions burned: 2020 (million) % 190.71/27.57 % (3818624)------------------------------ % 190.71/27.57 % (3818624)------------------------------ % 190.71/27.57 % (3818626)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:si=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2811325617:i=13990:s2at=5:rtra=on:gtg=all_2764 on theBenchmark for (2764ds/13990Mi) % 190.71/27.57 % (3818627)lrs+10_1_sil=32000:si=on:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=444170869:st=2:i=12450:sd=15:rtra=on:ss=axioms_2763 on theBenchmark for (2763ds/12450Mi) % 190.71/27.57 % (3818621)Instruction limit reached! % 190.71/27.57 % (3818621)------------------------------ % 190.71/27.57 % (3818621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.71/27.57 % (3818621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.71/27.57 % (3818621)CaDiCaL version: 2.1.3 % 190.71/27.57 % (3818621)Termination reason: Instruction limit % 190.71/27.57 % (3818621)Termination phase: Saturation % 190.71/27.57 % (3818621)Time elapsed: 0.614 s % 190.71/27.57 % (3818621)Peak memory usage: 104 MB % 190.71/27.57 % (3818621)Instructions burned: 2167 (million) % 190.71/27.57 % (3818630)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:si=on:lcm=reverse:random_seed=3851878237:cond=fast:i=6744:sd=1:nm=16:rtra=on:gtg=position:ss=axioms_2762 on theBenchmark for (2762ds/6744Mi) % 190.71/27.57 % Exception at run slice level % 190.71/27.57 User error: GNN currently only supports monomorphic FOL. % 190.71/27.57 % (3818632)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sos=all:random_seed=3971788494:st=2.3:i=52914:sd=10:rtra=on:ss=included:sgt=8_2761 on theBenchmark for (2761ds/52914Mi) % 190.71/27.57 % Exception at run slice level % 190.71/27.57 User error: GNN currently only supports monomorphic FOL. % 190.71/27.57 % (3818634)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:si=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=1490859428:i=26988:s2at=1.31:bd=all:ins=10:rtra=on:gtg=exists_top_2759 on theBenchmark for (2759ds/26988Mi) % 190.71/27.57 % Exception at run slice level % 190.71/27.57 User error: GNN currently only supports monomorphic FOL. % 190.71/27.57 % (3818636)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:si=on:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=3257998397:i=5006:nm=4:rtra=on:gsp=on:ss=axioms:sgt=15_2757 on theBenchmark for (2757ds/5006Mi) % 190.71/27.57 % (3818636)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 190.71/27.57 % Exception at run slice level % 190.71/27.57 User error: GNN currently only supports monomorphic FOL. % 190.71/27.57 % (3818638)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:si=on:sos=on:lsd=10:random_seed=3098141508:i=5118:sd=1:ep=RSTC:rtra=on:ss=axioms_2756 on theBenchmark for (2756ds/5118Mi) % 190.71/27.57 % Exception at run slice level % 190.71/27.57 User error: GNN currently only supports monomorphic FOL. % 190.71/27.57 % (3818640)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:si=on:fdtod=off:random_seed=2629351849:i=61506:av=off:rtra=on:ss=included_2754 on theBenchmark for (2754ds/61506Mi) % 190.71/27.57 % Exception at run slice level % 190.71/27.57 User error: GNN currently only supports monomorphic FOL. % 190.71/27.57 % (3818484)Instruction limit reached! % 199.87/28.82 % (3818484)------------------------------ % 199.87/28.82 % (3818484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 199.87/28.82 % (3818484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.87/28.82 % (3818484)CaDiCaL version: 2.1.3 % 199.87/28.82 % (3818484)Termination reason: Instruction limit % 199.87/28.82 % (3818484)Termination phase: Saturation % 199.87/28.82 % (3818484)Time elapsed: 10.794 s % 199.87/28.82 % (3818484)Peak memory usage: 227 MB % 199.87/28.82 % (3818484)Instructions burned: 36832 (million) % 199.87/28.82 % (3818642)lrs+10_1024_sil=64000:plsq=on:plsqc=4:si=on:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2813769941:i=52946:ep=RSTC:rtra=on_2752 on theBenchmark for (2752ds/52946Mi) % 199.87/28.82 % Exception at run slice level % 199.87/28.82 User error: GNN currently only supports monomorphic FOL. % 199.87/28.82 % (3818643)dis-1011_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:tgt=ground:npcc=on:si=on:sp=arity:sos=on:erd=off:rp=on:gs=on:kmz=on:random_seed=1612628089:cts=off:i=5518:kws=inv_arity:fgj=on:rtra=on_2752 on theBenchmark for (2752ds/5518Mi) % 199.87/28.82 % (3818645)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:si=on:sp=weighted_frequency:sos=all:spb=goal_then_units:urr=ec_only:sac=on:random_seed=3986111189:st=1.2:i=11330:sd=2:ep=RSTC:rtra=on:gsp=on:ss=axioms_2751 on theBenchmark for (2751ds/11330Mi) % 199.87/28.82 % (3818645)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 199.87/28.82 % (3818595)Instruction limit reached! % 199.87/28.82 % (3818595)------------------------------ % 199.87/28.82 % (3818595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 199.87/28.82 % (3818595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.87/28.82 % (3818595)CaDiCaL version: 2.1.3 % 199.87/28.82 % (3818595)Termination reason: Instruction limit % 199.87/28.82 % (3818595)Termination phase: Saturation % 199.87/28.82 % (3818595)Time elapsed: 3.002 s % 199.87/28.82 % (3818595)Peak memory usage: 104 MB % 199.87/28.82 % (3818595)Instructions burned: 11563 (million) % 199.87/28.82 % Exception at run slice level % 199.87/28.82 User error: GNN currently only supports monomorphic FOL. % 199.87/28.82 % (3818648)dis+1011_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:npcc=on:si=on:sos=on:lsd=20:urr=full:alpa=true:sac=on:random_seed=4283063332:i=3064:ep=RS:rtra=on:ss=axioms_2749 on theBenchmark for (2749ds/3064Mi) % 199.87/28.82 % Exception at run slice level % 199.87/28.82 User error: GNN currently only supports monomorphic FOL. % 199.87/28.82 % (3818649)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=4063536631:i=3130:sd=2:rtra=on:ss=axioms:sgt=32_2748 on theBenchmark for (2748ds/3130Mi) % 199.87/28.82 % (3818651)lrs-1011_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:sims=off:bsd=on:si=on:sp=unary_first:erd=off:spb=goal:lcm=reverse:gs=on:s2agt=8:random_seed=1829424354:i=3144:fgj=on:rtra=on:gsp=on_2748 on theBenchmark for (2748ds/3144Mi) % 199.87/28.82 % (3818651)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 199.87/28.82 % Exception at run slice level % 199.87/28.82 User error: GNN currently only supports monomorphic FOL. % 199.87/28.82 % Exception at run slice level % 199.87/28.82 User error: GNN currently only supports monomorphic FOL. % 199.87/28.82 % (3818654)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:si=on:sp=occurrence:sos=on:newcnf=on:random_seed=853257556:i=12104:sd=4:rtra=on:ss=axioms:sgt=24_2746 on theBenchmark for (2746ds/12104Mi) % 199.87/28.82 % Exception at run slice level % 199.87/28.82 User error: GNN currently only supports monomorphic FOL. % 199.87/28.82 % (3818655)lrs+21_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:si=on:sp=arity:sos=on:erd=off:lcm=predicate:alpa=false:sac=on:random_seed=2027133755:i=7000:sd=1:bd=preordered:rtra=on:sup=off:ss=included_2745 on theBenchmark for (2745ds/7000Mi) % 199.87/28.82 % (3818657)lrs+35_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:npcc=on:fde=none:si=on:sp=weighted_frequency:erd=off:spb=non_intro:updr=off:newcnf=on:random_seed=452096405:i=3684:sd=3:fgj=on:rtra=on:gtg=position:gsp=on:ss=axioms:sgt=20_2744 on theBenchmark for (2744ds/3684Mi) % 199.87/28.82 % (3818657)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 199.87/28.82 % Exception at run slice level % 211.78/30.50 User error: GNN currently only supports monomorphic FOL. % 211.78/30.50 % Exception at run slice level % 211.78/30.50 User error: GNN currently only supports monomorphic FOL. % 211.78/30.50 % (3818660)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:si=on:bsr=unit_only:random_seed=1812388464:i=132192:add=on:rtra=on_2743 on theBenchmark for (2743ds/132192Mi) % 211.78/30.50 % Exception at run slice level % 211.78/30.50 User error: GNN currently only supports monomorphic FOL. % 211.78/30.50 % (3818661)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:si=on:random_seed=2564005999:i=3768:sd=1:nm=60:rtra=on:ss=axioms_2742 on theBenchmark for (2742ds/3768Mi) % 211.78/30.50 % (3818663)lrs-1011_4:1_sil=16000:si=on:bsr=on:random_seed=1594923124:cts=off:i=10938:bs=on:fsr=off:rtra=on_2741 on theBenchmark for (2741ds/10938Mi) % 211.78/30.50 % Exception at run slice level % 211.78/30.50 User error: GNN currently only supports monomorphic FOL. % 211.78/30.50 % Exception at run slice level % 211.78/30.50 User error: GNN currently only supports monomorphic FOL. % 211.78/30.50 % (3818666)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=unary_frequency:urr=on:bce=on:alpa=false:sac=on:random_seed=2339991490:i=4074:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:rtra=on:gtg=exists_all_2739 on theBenchmark for (2739ds/4074Mi) % 211.78/30.50 % (3818667)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:si=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=1026667241:st=-1:i=4220:kws=precedence:av=off:rtra=on:ss=axioms:er=known_2738 on theBenchmark for (2738ds/4220Mi) % 211.78/30.50 % Exception at run slice level % 211.78/30.50 User error: GNN currently only supports monomorphic FOL. % 211.78/30.50 % Exception at run slice level % 211.78/30.50 User error: GNN currently only supports monomorphic FOL. % 211.78/30.50 % (3818670)dis-1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:si=on:sp=unary_first:spb=goal:lcm=reverse:fd=off:flr=on:random_seed=2582598037:i=4860:add=off:aac=none:nm=16:rtra=on_2736 on theBenchmark for (2736ds/4860Mi) % 211.78/30.50 % (3818671)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=unary_first:spb=units:acc=on:bsr=unit_only:gs=on:sac=on:random_seed=1485056525:cond=fast:i=9782:rtra=on_2735 on theBenchmark for (2735ds/9782Mi) % 211.78/30.50 % Exception at run slice level % 211.78/30.50 User error: GNN currently only supports monomorphic FOL. % 211.78/30.50 % Exception at run slice level % 211.78/30.50 User error: GNN currently only supports monomorphic FOL. % 211.78/30.50 % (3818674)lrs+4_1_anc=all:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:si=on:sos=on:spb=goal_then_units:lcm=reverse:gs=on:s2agt=16:sac=on:newcnf=on:random_seed=1730295480:st=2:i=29690:sd=2:rtra=on:ss=included:fsd=on_2733 on theBenchmark for (2733ds/29690Mi) % 211.78/30.50 % (3818675)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:si=on:urr=ec_only:br=off:random_seed=1088682564:i=15068:sd=3:ins=1:rtra=on:gtg=exists_top:ss=included:sgt=8_2732 on theBenchmark for (2732ds/15068Mi) % 211.78/30.50 % Exception at run slice level % 211.78/30.50 User error: GNN currently only supports monomorphic FOL. % 211.78/30.50 % (3818627)Instruction limit reached! % 211.78/30.50 % (3818627)------------------------------ % 211.78/30.50 % (3818627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.78/30.50 % (3818627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.78/30.50 % (3818627)CaDiCaL version: 2.1.3 % 211.78/30.50 % (3818627)Termination reason: Instruction limit % 211.78/30.50 % (3818627)Termination phase: Saturation % 211.78/30.50 % (3818627)Time elapsed: 3.364 s % 211.78/30.50 % (3818627)Peak memory usage: 129 MB % 211.78/30.50 % (3818627)Instructions burned: 12453 (million) % 211.78/30.50 % Exception at run slice level % 211.78/30.50 User error: GNN currently only supports monomorphic FOL. % 211.78/30.50 % (3818678)lrs-1002_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=ground:npcc=on:prc=on:fde=none:sims=off:si=on:spb=goal:bsr=unit_only:s2agt=32:random_seed=4276670150:cond=fast:i=20706:bs=on:av=off:rtra=on:ss=axioms:fsd=on:sgt=64:fsdmm=10_2729 on theBenchmark for (2729ds/20706Mi) % 211.78/30.50 % (3818679)lrs+2_4096_sil=8000:plsq=on:si=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2214607648:i=15720:rtra=on_2728 on theBenchmark for (2728ds/15720Mi) % 211.78/30.50 % (3818679)Refutation not found, incomplete strategy % 211.78/30.50 % (3818679)------------------------------ % 211.78/30.50 % (3818679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.78/35.12 % (3818679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.78/35.12 % (3818679)CaDiCaL version: 2.1.3 % 240.78/35.12 % (3818679)Termination reason: Refutation not found, incomplete strategy % 240.78/35.12 % (3818679)Time elapsed: 0.007 s % 240.78/35.12 % (3818679)Peak memory usage: 89 MB % 240.78/35.12 % (3818679)Instructions burned: 20 (million) % 240.78/35.12 % (3818680)ott+1011_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:fde=unused:si=on:spb=goal:lsd=30:lcm=predicate:fd=off:gs=on:sac=on:random_seed=805652763:i=15792:sd=2:bs=on:rtra=on:ss=included:sgt=20_2728 on theBenchmark for (2728ds/15792Mi) % 240.78/35.12 % Exception at run slice level % 240.78/35.12 User error: GNN currently only supports monomorphic FOL. % 240.78/35.12 % (3818679)------------------------------ % 240.78/35.12 % (3818679)------------------------------ % 240.78/35.12 % Exception at run slice level % 240.78/35.12 User error: GNN currently only supports monomorphic FOL. % 240.78/35.12 % (3818684)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:si=on:random_seed=1798605191:i=11624:gtgl=2:rtra=on:gtg=all_2726 on theBenchmark for (2726ds/11624Mi) % 240.78/35.12 % (3818685)ott-1011_1_anc=none:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:si=on:sp=const_frequency:sos=on:lsd=100:random_seed=3758340581:i=5930:s2at=3.7:aac=none:fgj=on:rtra=on:fdi=2:er=known_2725 on theBenchmark for (2725ds/5930Mi) % 240.78/35.12 % (3818686)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:si=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1187807053:i=5934:kws=precedence:bd=preordered:av=off:rtra=on_2725 on theBenchmark for (2725ds/5934Mi) % 240.78/35.12 % Exception at run slice level % 240.78/35.12 User error: GNN currently only supports monomorphic FOL. % 240.78/35.12 % Exception at run slice level % 240.78/35.12 User error: GNN currently only supports monomorphic FOL. % 240.78/35.12 % Exception at run slice level % 240.78/35.12 User error: GNN currently only supports monomorphic FOL. % 240.78/35.12 % (3818690)ott+1002_1_anc=all:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:si=on:sos=on:spb=goal_then_units:alpa=false:sac=on:random_seed=3537634829:i=6044:sd=1:kws=frequency:aac=none:ep=RST:nm=16:rtra=on:ss=axioms:er=known_2723 on theBenchmark for (2723ds/6044Mi) % 240.78/35.12 % (3818691)lrs-1010_1_ncem=casc2026/models/loop4.pt:sil=32000:tgt=ground:npcc=on:prc=on:si=on:sp=const_frequency:sos=all:lcm=predicate:acc=on:bsr=unit_only:gs=on:sac=on:newcnf=on:random_seed=3676265119:prac=on:i=6414:kws=frequency:fgj=on:rtra=on:ss=axioms:er=filter:sgt=8_2722 on theBenchmark for (2722ds/6414Mi) % 240.78/35.12 % (3818692)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:si=on:sos=on:lcm=predicate:random_seed=2668795129:st=4.2:i=6578:sd=5:aac=none:rtra=on:ss=included:sgt=10_2722 on theBenchmark for (2722ds/6578Mi) % 240.78/35.12 % Exception at run slice level % 240.78/35.12 User error: GNN currently only supports monomorphic FOL. % 240.78/35.12 % Exception at run slice level % 240.78/35.12 User error: GNN currently only supports monomorphic FOL. % 240.78/35.12 % Exception at run slice level % 240.78/35.12 User error: GNN currently only supports monomorphic FOL. % 240.78/35.12 % (3818696)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:si=on:random_seed=4124287755:i=77138:sd=3:rtra=on:ss=axioms:sgt=32_2719 on theBenchmark for (2719ds/77138Mi) % 240.78/35.12 % (3818697)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:si=on:bsr=on:random_seed=433135322:cts=off:i=6788:rtra=on_2719 on theBenchmark for (2719ds/6788Mi) % 240.78/35.12 % (3818698)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:si=on:sp=arity:spb=intro:lcm=reverse:urr=ec_only:fd=preordered:gs=on:sac=on:random_seed=1328996773:i=67648:bd=preordered:rtra=on_2719 on theBenchmark for (2719ds/67648Mi) % 240.78/35.12 % Exception at run slice level % 240.78/35.12 User error: GNN currently only supports monomorphic FOL. % 240.78/35.12 % Exception at run slice level % 240.78/35.12 User error: GNN currently only supports monomorphic FOL. % 240.78/35.12 % Exception at run slice level % 240.78/35.12 User error: GNN currently only supports monomorphic FOL. % 240.78/35.12 % (3818702)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:si=on:random_seed=1234621358:i=41368:bd=all:rtra=on:gtg=exists_sym_2716 on theBenchmark for (2716ds/41368Mi) % 240.78/35.12 % (3818703)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:irw=on:npcc=on:prc=on:bsd=on:si=on:sp=reverse_frequency:sos=on:erd=off:spb=goal:lcm=reverse:urr=full:bsr=on:s2agt=32:alpa=random:kmz=on:random_seed=3499694076:st=3:prac=on:i=14444:kws=arity_squared:add=on:fgj=on:bd=preordered:rtra=on:gtg=exists_top:gsp=on:ss=axioms:er=known:sgt=8:proc=on_2716 on theBenchmark for (2716ds/14444Mi) % 283.81/40.82 % (3818703)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 283.81/40.82 % (3818704)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:spb=goal_then_units:random_seed=2329207325:st=4:i=14590:sd=4:ep=R:rtra=on:ss=axioms_2715 on theBenchmark for (2715ds/14590Mi) % 283.81/40.82 % Exception at run slice level % 283.81/40.82 User error: GNN currently only supports monomorphic FOL. % 283.81/40.82 % Exception at run slice level % 283.81/40.82 User error: GNN currently only supports monomorphic FOL. % 283.81/40.82 % Exception at run slice level % 283.81/40.82 User error: GNN currently only supports monomorphic FOL. % 283.81/40.82 % (3818708)lrs+32_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:fde=none:si=on:sp=occurrence:urr=ec_only:fd=preordered:random_seed=676396810:i=8072:ins=10:rtra=on_2713 on theBenchmark for (2713ds/8072Mi) % 283.81/40.82 % (3818709)lrs+10_1_sil=128000:si=on:lcm=predicate:random_seed=3552176994:st=3:i=87394:sd=5:rtra=on:ss=axioms_2713 on theBenchmark for (2713ds/87394Mi) % 283.81/40.82 % (3818710)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:si=on:sp=const_frequency:sos=all:lcm=predicate:urr=on:s2agt=20:sac=on:random_seed=522162485:i=35198:rtra=on:gtg=all:ss=axioms:fsd=on_2712 on theBenchmark for (2712ds/35198Mi) % 283.81/40.82 % Exception at run slice level % 283.81/40.82 User error: GNN currently only supports monomorphic FOL. % 283.81/40.82 % Exception at run slice level % 283.81/40.82 User error: GNN currently only supports monomorphic FOL. % 283.81/40.82 % (3818714)lrs+1011_1_to=lpo:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:si=on:sp=occurrence:lcm=reverse:urr=ec_only:gs=on:random_seed=3204730338:i=9094:bd=preordered:rtra=on_2710 on theBenchmark for (2710ds/9094Mi) % 283.81/40.82 % (3818715)lrs+1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:si=on:sp=unary_first:spb=goal:urr=ec_only:newcnf=on:random_seed=3714632293:i=18588:av=off:rtra=on_2709 on theBenchmark for (2709ds/18588Mi) % 283.81/40.82 % Exception at run slice level % 283.81/40.82 User error: GNN currently only supports monomorphic FOL. % 283.81/40.82 % Exception at run slice level % 283.81/40.82 User error: GNN currently only supports monomorphic FOL. % 283.81/40.82 % (3818718)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:si=on:bsr=unit_only:random_seed=3156346518:i=65698:add=on:rtra=on_2706 on theBenchmark for (2706ds/65698Mi) % 283.81/40.82 % (3818719)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:si=on:erd=off:lsd=100:bsr=unit_only:random_seed=3511075763:st=1.5:i=9586:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2706 on theBenchmark for (2706ds/9586Mi) % 283.81/40.82 % Exception at run slice level % 283.81/40.82 User error: GNN currently only supports monomorphic FOL. % 283.81/40.82 % Exception at run slice level % 283.81/40.82 User error: GNN currently only supports monomorphic FOL. % 283.81/40.82 % (3818722)dis+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:prc=on:drc=off:sims=off:si=on:sp=const_frequency:sos=on:spb=non_intro:gs=on:updr=off:newcnf=on:random_seed=432946087:i=9680:nm=4:av=off:rtra=on_2703 on theBenchmark for (2703ds/9680Mi) % 283.81/40.82 % (3818723)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:gs=on:newcnf=on:random_seed=4130388331:cts=off:i=10004:rtra=on_2702 on theBenchmark for (2702ds/10004Mi) % 283.81/40.82 % Exception at run slice level % 283.81/40.82 User error: GNN currently only supports monomorphic FOL. % 283.81/40.82 % Exception at run slice level % 283.81/40.82 User error: GNN currently only supports monomorphic FOL. % 283.81/40.82 % (3818726)dis+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fde=unused:si=on:sp=const_frequency:spb=goal:acc=on:random_seed=4198024083:i=60958:sd=3:rtra=on:ss=axioms_2700 on theBenchmark for (2700ds/60958Mi) % 283.81/40.82 % (3818727)lrs+1011_1_anc=none:ncem=casc2026/models/loop2.pt:sil=32000:tgt=full:npcc=on:fde=unused:sas=cadical:si=on:sp=const_frequency:spb=non_intro:lsd=10:lcm=predicate:rp=on:sac=on:newcnf=on:random_seed=205972157:i=22070:s2at=5:kws=inv_arity:bs=on:rtra=on:gsp=on_2699 on theBenchmark for (2699ds/22070Mi) % 283.81/40.82 % (3818727)WARNING: Not using GeneralSplittingTerminated % 300.39/43.06 % Vampire exiting %------------------------------------------------------------------------------