%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : COM082_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 : n006.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:32 AM UTC 2026 % Result : Timeout 295.17s 43.19s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : COM082_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.20 % Computer : n006.cluster.edu % 0.10/0.20 % Model : x86_64 x86_64 % 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.20 % Memory : 8046.5625MB % 0.10/0.20 % OS : Linux 6.8.0-71-generic % 0.10/0.20 % CPULimit : 300 % 0.10/0.20 % WCLimit : 300 % 0.10/0.20 % DateTime : Mon Sep 28 21:52:55 UTC 2026 % 0.10/0.20 % CPUTime : % 0.10/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.23 Running first-order theorem proving % 0.10/0.23 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.41/1.69 % (245352)Detected formulas, will run a generic FOF schedule. % 5.41/1.69 % (245443)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2574516498:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 5.41/1.69 % (245443)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.41/1.69 % (245443)Refutation not found, incomplete strategy % 5.41/1.69 % (245443)------------------------------ % 5.41/1.69 % (245443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.41/1.69 % (245443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.41/1.69 % (245443)CaDiCaL version: 2.1.3 % 5.41/1.69 % (245443)Termination reason: Refutation not found, incomplete strategy % 5.41/1.69 % (245443)Time elapsed: 0.001 s % 5.41/1.69 % (245443)Peak memory usage: 87 MB % 5.41/1.69 % (245443)Instructions burned: 1 (million) % 5.41/1.69 % (245440)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=3764884655:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 5.41/1.69 % (245439)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=4191407646:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 5.41/1.69 % (245444)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=161071237:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 5.41/1.69 % (245445)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=291194853:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 5.41/1.69 % (245446)dis-21_1_sil=8000:lcm=predicate:random_seed=2968244687: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.41/1.69 % (245441)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=1612577695:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 5.41/1.69 % (245441)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.41/1.69 % (245444)Instruction limit reached! % 5.41/1.69 % (245444)------------------------------ % 5.41/1.69 % (245444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.41/1.69 % (245444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.41/1.69 % (245444)CaDiCaL version: 2.1.3 % 5.41/1.69 % (245444)Termination reason: Instruction limit % 5.41/1.69 % (245444)Termination phase: Saturation % 5.41/1.69 % (245444)Time elapsed: 0.073 s % 5.41/1.69 % (245444)Peak memory usage: 88 MB % 5.41/1.69 % (245444)Instructions burned: 119 (million) % 5.41/1.69 % (245445)Instruction limit reached! % 5.41/1.69 % (245445)------------------------------ % 5.41/1.69 % (245445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.41/1.69 % (245445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.41/1.69 % (245445)CaDiCaL version: 2.1.3 % 5.41/1.69 % (245445)Termination reason: Instruction limit % 5.41/1.69 % (245445)Termination phase: Saturation % 5.41/1.69 % (245445)Time elapsed: 0.076 s % 5.41/1.69 % (245445)Peak memory usage: 88 MB % 5.41/1.69 % (245445)Instructions burned: 139 (million) % 5.41/1.69 % (245446)Instruction limit reached! % 5.41/1.69 % (245446)------------------------------ % 5.41/1.69 % (245446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.41/1.69 % (245446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.41/1.69 % (245446)CaDiCaL version: 2.1.3 % 5.41/1.69 % (245446)Termination reason: Instruction limit % 5.41/1.69 % (245446)Termination phase: Saturation % 5.41/1.69 % (245446)Time elapsed: 0.080 s % 5.41/1.69 % (245446)Peak memory usage: 89 MB % 5.41/1.69 % (245446)Instructions burned: 129 (million) % 5.41/1.69 % (245443)------------------------------ % 5.41/1.69 % (245443)------------------------------ % 5.41/1.69 % (245502)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2629916714:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 5.41/1.69 % (245500)lrs+10_1_sil=8000:sp=occurrence:random_seed=2619242325:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 5.41/1.69 % (245519)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=36955912:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi) % 9.79/2.05 % (245510)lrs+1011_1_sil=32000:sp=occurrence:random_seed=47300023:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 9.79/2.05 % (245519)Instruction limit reached! % 9.79/2.05 % (245519)------------------------------ % 9.79/2.05 % (245519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.79/2.05 % (245519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.79/2.05 % (245519)CaDiCaL version: 2.1.3 % 9.79/2.05 % (245519)Termination reason: Instruction limit % 9.79/2.05 % (245519)Termination phase: Saturation % 9.79/2.05 % (245519)Time elapsed: 0.065 s % 9.79/2.05 % (245519)Peak memory usage: 90 MB % 9.79/2.05 % (245519)Instructions burned: 249 (million) % 9.79/2.05 % (245502)Instruction limit reached! % 9.79/2.05 % (245502)------------------------------ % 9.79/2.05 % (245502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.79/2.05 % (245502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.79/2.05 % (245502)CaDiCaL version: 2.1.3 % 9.79/2.05 % (245502)Termination reason: Instruction limit % 9.79/2.05 % (245502)Termination phase: Saturation % 9.79/2.05 % (245502)Time elapsed: 0.076 s % 9.79/2.05 % (245502)Peak memory usage: 89 MB % 9.79/2.05 % (245502)Instructions burned: 157 (million) % 9.79/2.05 % Exception at run slice level % 9.79/2.05 User error: GNN currently only supports monomorphic FOL. % 9.79/2.05 % Exception at run slice level % 9.79/2.05 User error: GNN currently only supports monomorphic FOL. % 9.79/2.05 % (245500)Instruction limit reached! % 9.79/2.05 % (245500)------------------------------ % 9.79/2.05 % (245500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.79/2.05 % (245500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.79/2.05 % (245500)CaDiCaL version: 2.1.3 % 9.79/2.05 % (245500)Termination reason: Instruction limit % 9.79/2.05 % (245500)Termination phase: Saturation % 9.79/2.05 % (245500)Time elapsed: 0.157 s % 9.79/2.05 % (245500)Peak memory usage: 91 MB % 9.79/2.05 % (245500)Instructions burned: 286 (million) % 9.79/2.05 % (245554)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1584568548:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 9.79/2.05 % Exception at run slice level % 9.79/2.05 User error: GNN currently only supports monomorphic FOL. % 9.79/2.05 % (245554)Refutation not found, incomplete strategy % 9.79/2.05 % (245554)------------------------------ % 9.79/2.05 % (245554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.79/2.05 % (245554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.79/2.05 % (245554)CaDiCaL version: 2.1.3 % 9.79/2.05 % (245554)Termination reason: Refutation not found, incomplete strategy % 9.79/2.05 % (245554)Time elapsed: 0.003 s % 9.79/2.05 % (245554)Peak memory usage: 88 MB % 9.79/2.05 % (245554)Instructions burned: 9 (million) % 9.79/2.05 % (245510)Instruction limit reached! % 9.79/2.05 % (245510)------------------------------ % 9.79/2.05 % (245510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.79/2.05 % (245510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.79/2.05 % (245510)CaDiCaL version: 2.1.3 % 9.79/2.05 % (245510)Termination reason: Instruction limit % 9.79/2.05 % (245510)Termination phase: Saturation % 9.79/2.05 % (245510)Time elapsed: 0.170 s % 9.79/2.05 % (245510)Peak memory usage: 91 MB % 9.79/2.05 % (245510)Instructions burned: 326 (million) % 9.79/2.05 % (245561)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=571322840:i=2350_2994 on theBenchmark for (2994ds/2350Mi) % 9.79/2.05 % (245574)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3612960506:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 9.79/2.05 % (245586)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3171346469:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 9.79/2.05 % (245596)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3232925171:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 9.79/2.05 % (245604)lrs+10_1_sil=8000:sp=occurrence:random_seed=237745585:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi) % 9.79/2.05 % (245574)Instruction limit reached! % 9.79/2.05 % (245574)------------------------------ % 9.79/2.05 % (245574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.37/2.41 % (245574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.37/2.41 % (245574)CaDiCaL version: 2.1.3 % 11.37/2.41 % (245574)Termination reason: Instruction limit % 11.37/2.41 % (245574)Termination phase: Saturation % 11.37/2.41 % (245574)Time elapsed: 0.070 s % 11.37/2.41 % (245574)Peak memory usage: 89 MB % 11.37/2.41 % (245574)Instructions burned: 113 (million) % 11.37/2.41 % (245554)------------------------------ % 11.37/2.41 % (245554)------------------------------ % 11.37/2.41 % (245610)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3753032830:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi) % 11.37/2.41 % (245586)Instruction limit reached! % 11.37/2.41 % (245586)------------------------------ % 11.37/2.41 % (245586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.37/2.41 % (245586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.37/2.41 % (245586)CaDiCaL version: 2.1.3 % 11.37/2.41 % (245586)Termination reason: Instruction limit % 11.37/2.41 % (245586)Termination phase: Saturation % 11.37/2.41 % (245586)Time elapsed: 0.063 s % 11.37/2.41 % (245586)Peak memory usage: 88 MB % 11.37/2.41 % (245586)Instructions burned: 129 (million) % 11.37/2.41 % (245610)Refutation not found, incomplete strategy % 11.37/2.41 % (245610)------------------------------ % 11.37/2.41 % (245610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.37/2.41 % (245610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.37/2.41 % (245610)CaDiCaL version: 2.1.3 % 11.37/2.41 % (245610)Termination reason: Refutation not found, incomplete strategy % 11.37/2.41 % (245610)Time elapsed: 0.006 s % 11.37/2.41 % (245610)Peak memory usage: 88 MB % 11.37/2.41 % (245610)Instructions burned: 9 (million) % 11.37/2.41 % (245596)Instruction limit reached! % 11.37/2.41 % (245596)------------------------------ % 11.37/2.41 % (245596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.37/2.41 % (245596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.37/2.41 % (245596)CaDiCaL version: 2.1.3 % 11.37/2.41 % (245596)Termination reason: Instruction limit % 11.37/2.41 % (245596)Termination phase: Saturation % 11.37/2.41 % (245596)Time elapsed: 0.060 s % 11.37/2.41 % (245596)Peak memory usage: 88 MB % 11.37/2.41 % (245596)Instructions burned: 114 (million) % 11.37/2.41 % (245646)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=128047327:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2992 on theBenchmark for (2992ds/134Mi) % 11.37/2.41 % (245646)Instruction limit reached! % 11.37/2.41 % (245646)------------------------------ % 11.37/2.41 % (245646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.37/2.41 % (245646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.37/2.41 % (245646)CaDiCaL version: 2.1.3 % 11.37/2.41 % (245646)Termination reason: Instruction limit % 11.37/2.41 % (245646)Termination phase: Saturation % 11.37/2.41 % (245646)Time elapsed: 0.037 s % 11.37/2.41 % (245646)Peak memory usage: 89 MB % 11.37/2.41 % (245646)Instructions burned: 135 (million) % 11.37/2.41 % (245645)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1415663432:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi) % 11.37/2.41 % (245648)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4058387539:st=8:i=592:sd=3:ep=RST:ss=axioms_2992 on theBenchmark for (2992ds/592Mi) % 11.37/2.41 % (245649)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=238522934:st=3:i=13193:sd=3:ss=axioms_2992 on theBenchmark for (2992ds/13193Mi) % 11.37/2.41 % (245648)Refutation not found, incomplete strategy % 11.37/2.41 % (245648)------------------------------ % 11.37/2.41 % (245648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.37/2.41 % (245648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.37/2.41 % (245648)CaDiCaL version: 2.1.3 % 11.37/2.41 % (245648)Termination reason: Refutation not found, incomplete strategy % 11.37/2.41 % (245648)Time elapsed: 0.006 s % 11.37/2.41 % (245648)Peak memory usage: 88 MB % 11.37/2.41 % (245648)Instructions burned: 10 (million) % 11.37/2.41 % (245657)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=2134909640:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/125Mi) % 11.37/2.41 % (245657)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 16.87/3.06 % Exception at run slice level % 16.87/3.06 User error: GNN currently only supports monomorphic FOL. % 16.87/3.06 % (245610)------------------------------ % 16.87/3.06 % (245610)------------------------------ % 16.87/3.06 % (245657)Instruction limit reached! % 16.87/3.06 % (245657)------------------------------ % 16.87/3.06 % (245657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.87/3.06 % (245657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.87/3.06 % (245657)CaDiCaL version: 2.1.3 % 16.87/3.06 % (245657)Termination reason: Instruction limit % 16.87/3.06 % (245657)Termination phase: Saturation % 16.87/3.06 % (245657)Time elapsed: 0.037 s % 16.87/3.06 % (245657)Peak memory usage: 90 MB % 16.87/3.06 % (245657)Instructions burned: 128 (million) % 16.87/3.06 % (245703)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3171129782:i=134:gtgl=5:slsql=off:gtg=exists_sym_2989 on theBenchmark for (2989ds/134Mi) % 16.87/3.06 % (245705)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4104206354:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/431Mi) % 16.87/3.06 % Exception at run slice level % 16.87/3.06 User error: Immediate (shared) subterms of term/literal amap_fm(X1,X0,X3,neg(X1,X2)) = sF35(X1,X0,X3,X2) have different types/not well-typed! % 16.87/3.06 % (245704)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=625192647:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/141Mi) % 16.87/3.06 % (245704)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 16.87/3.06 % (245704)Refutation not found, incomplete strategy % 16.87/3.06 % (245704)------------------------------ % 16.87/3.06 % (245704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.87/3.06 % (245704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.87/3.06 % (245704)CaDiCaL version: 2.1.3 % 16.87/3.06 % (245704)Termination reason: Refutation not found, incomplete strategy % 16.87/3.06 % (245704)Time elapsed: 0.002 s % 16.87/3.06 % (245704)Peak memory usage: 88 MB % 16.87/3.06 % (245704)Instructions burned: 1 (million) % 16.87/3.06 % (245648)------------------------------ % 16.87/3.06 % (245648)------------------------------ % 16.87/3.06 % (245604)Instruction limit reached! % 16.87/3.06 % (245604)------------------------------ % 16.87/3.06 % (245604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.87/3.06 % (245604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.87/3.06 % (245604)CaDiCaL version: 2.1.3 % 16.87/3.06 % (245604)Termination reason: Instruction limit % 16.87/3.06 % (245604)Termination phase: Saturation % 16.87/3.06 % (245604)Time elapsed: 0.505 s % 16.87/3.06 % (245604)Peak memory usage: 98 MB % 16.87/3.06 % (245604)Instructions burned: 908 (million) % 16.87/3.06 % (245705)Instruction limit reached! % 16.87/3.06 % (245705)------------------------------ % 16.87/3.06 % (245705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.87/3.06 % (245705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.87/3.06 % (245705)CaDiCaL version: 2.1.3 % 16.87/3.06 % (245705)Termination reason: Instruction limit % 16.87/3.06 % (245705)Termination phase: Saturation % 16.87/3.06 % (245705)Time elapsed: 0.116 s % 16.87/3.06 % (245705)Peak memory usage: 89 MB % 16.87/3.06 % (245705)Instructions burned: 434 (million) % 16.87/3.06 % Exception at run slice level % 16.87/3.06 User error: GNN currently only supports monomorphic FOL. % 16.87/3.06 % Exception at run slice level % 16.87/3.06 User error: GNN currently only supports monomorphic FOL. % 16.87/3.06 % (245708)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=3029020455:i=6060:aac=none:ins=25_2988 on theBenchmark for (2988ds/6060Mi) % 16.87/3.06 % (245710)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=2625173747:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2988 on theBenchmark for (2988ds/150Mi) % 16.87/3.06 % (245710)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 16.87/3.06 % (245712)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=37045012:i=667:av=off:fsr=off_2987 on theBenchmark for (2987ds/667Mi) % 25.62/4.32 % (245712)Refutation not found, incomplete strategy % 25.62/4.32 % (245712)------------------------------ % 25.62/4.32 % (245712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.62/4.32 % (245712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.62/4.32 % (245712)CaDiCaL version: 2.1.3 % 25.62/4.32 % (245712)Termination reason: Refutation not found, incomplete strategy % 25.62/4.32 % (245712)Time elapsed: 0.003 s % 25.62/4.32 % (245712)Peak memory usage: 88 MB % 25.62/4.32 % (245712)Instructions burned: 8 (million) % 25.62/4.32 % (245711)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=52164013:i=14155:bd=all_2987 on theBenchmark for (2987ds/14155Mi) % 25.62/4.32 % (245713)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=3119167078:s2a=on:i=185:s2at=1.8:fdi=4_2987 on theBenchmark for (2987ds/185Mi) % 25.62/4.32 % (245710)Instruction limit reached! % 25.62/4.32 % (245710)------------------------------ % 25.62/4.32 % (245710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.62/4.32 % (245710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.62/4.32 % (245710)CaDiCaL version: 2.1.3 % 25.62/4.32 % (245710)Termination reason: Instruction limit % 25.62/4.32 % (245710)Termination phase: Saturation % 25.62/4.32 % (245710)Time elapsed: 0.080 s % 25.62/4.32 % (245710)Peak memory usage: 90 MB % 25.62/4.32 % (245710)Instructions burned: 152 (million) % 25.62/4.32 % (245704)------------------------------ % 25.62/4.32 % (245704)------------------------------ % 25.62/4.32 % (245715)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2475911829:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2986 on theBenchmark for (2986ds/193Mi) % 25.62/4.32 % (245713)Instruction limit reached! % 25.62/4.32 % (245713)------------------------------ % 25.62/4.32 % (245713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.62/4.32 % (245713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.62/4.32 % (245713)CaDiCaL version: 2.1.3 % 25.62/4.32 % (245713)Termination reason: Instruction limit % 25.62/4.32 % (245713)Termination phase: Saturation % 25.62/4.32 % (245713)Time elapsed: 0.099 s % 25.62/4.32 % (245713)Peak memory usage: 90 MB % 25.62/4.32 % (245713)Instructions burned: 187 (million) % 25.62/4.32 % (245712)------------------------------ % 25.62/4.32 % (245712)------------------------------ % 25.62/4.32 % (245720)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1698380412:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2985 on theBenchmark for (2985ds/4850Mi) % 25.62/4.32 % (245715)Instruction limit reached! % 25.62/4.32 % (245715)------------------------------ % 25.62/4.32 % (245715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.62/4.32 % (245715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.62/4.32 % (245715)CaDiCaL version: 2.1.3 % 25.62/4.32 % (245715)Termination reason: Instruction limit % 25.62/4.32 % (245715)Termination phase: Saturation % 25.62/4.32 % (245715)Time elapsed: 0.107 s % 25.62/4.32 % (245715)Peak memory usage: 91 MB % 25.62/4.32 % (245715)Instructions burned: 195 (million) % 25.62/4.32 % (245721)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=546715795:i=12111:sd=1:ss=included_2985 on theBenchmark for (2985ds/12111Mi) % 25.62/4.32 % (245724)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3858434156:i=2064:ep=RST_2984 on theBenchmark for (2984ds/2064Mi) % 25.62/4.32 % (245724)Refutation not found, incomplete strategy % 25.62/4.32 % (245724)------------------------------ % 25.62/4.32 % (245724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.62/4.32 % (245724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.62/4.32 % (245724)CaDiCaL version: 2.1.3 % 25.62/4.32 % (245724)Termination reason: Refutation not found, incomplete strategy % 25.62/4.32 % (245724)Time elapsed: 0.003 s % 25.62/4.32 % (245724)Peak memory usage: 88 MB % 25.62/4.32 % (245724)Instructions burned: 9 (million) % 25.62/4.32 % Exception at run slice level % 25.62/4.32 User error: GNN currently only supports monomorphic FOL. % 25.62/4.32 % (245723)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3111200862:i=319:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/319Mi) % 25.62/4.32 % (245726)dis-1011_128_sil=32000:random_seed=4103775853:i=3706:ep=RST:av=off_2984 on theBenchmark for (2984ds/3706Mi) % 31.07/5.04 % Exception at run slice level % 31.07/5.04 User error: GNN currently only supports monomorphic FOL. % 31.07/5.04 % (245724)------------------------------ % 31.07/5.04 % (245724)------------------------------ % 31.07/5.04 % (245729)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=915694561:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2983 on theBenchmark for (2983ds/757Mi) % 31.07/5.04 % (245729)Refutation not found, incomplete strategy % 31.07/5.04 % (245729)------------------------------ % 31.07/5.04 % (245729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.07/5.04 % (245729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.07/5.04 % (245729)CaDiCaL version: 2.1.3 % 31.07/5.04 % (245729)Termination reason: Refutation not found, incomplete strategy % 31.07/5.04 % (245729)Time elapsed: 0.005 s % 31.07/5.04 % (245729)Peak memory usage: 88 MB % 31.07/5.04 % (245729)Instructions burned: 8 (million) % 31.07/5.04 % (245723)Instruction limit reached! % 31.07/5.04 % (245723)------------------------------ % 31.07/5.04 % (245723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.07/5.04 % (245723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.07/5.04 % (245723)CaDiCaL version: 2.1.3 % 31.07/5.04 % (245723)Termination reason: Instruction limit % 31.07/5.04 % (245723)Termination phase: Saturation % 31.07/5.04 % (245723)Time elapsed: 0.160 s % 31.07/5.04 % (245723)Peak memory usage: 91 MB % 31.07/5.04 % (245723)Instructions burned: 320 (million) % 31.07/5.04 % (245733)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=775200164:i=9925:aac=none_2982 on theBenchmark for (2982ds/9925Mi) % 31.07/5.04 % (245732)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1244895161:i=13913:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/13913Mi) % 31.07/5.04 % Exception at run slice level % 31.07/5.04 User error: GNN currently only supports monomorphic FOL. % 31.07/5.04 % (245735)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1010441259:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2981 on theBenchmark for (2981ds/2479Mi) % 31.07/5.04 % (245735)Refutation not found, incomplete strategy % 31.07/5.04 % (245735)------------------------------ % 31.07/5.04 % (245735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.07/5.04 % (245735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.07/5.04 % (245735)CaDiCaL version: 2.1.3 % 31.07/5.04 % (245735)Termination reason: Refutation not found, incomplete strategy % 31.07/5.04 % (245735)Time elapsed: 0.004 s % 31.07/5.04 % (245735)Peak memory usage: 88 MB % 31.07/5.04 % (245735)Instructions burned: 6 (million) % 31.07/5.04 % (245729)------------------------------ % 31.07/5.04 % (245729)------------------------------ % 31.07/5.04 % Exception at run slice level % 31.07/5.04 User error: GNN currently only supports monomorphic FOL. % 31.07/5.04 % (245738)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1562170493:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/440Mi) % 31.07/5.04 % (245738)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 31.07/5.04 % (245741)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=2056031715:cts=off:i=3034:av=off:er=known:fsd=on_2978 on theBenchmark for (2978ds/3034Mi) % 31.07/5.04 % (245740)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=961223550:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2979 on theBenchmark for (2979ds/11145Mi) % 31.07/5.04 % (245735)------------------------------ % 31.07/5.04 % (245735)------------------------------ % 31.07/5.04 % Exception at run slice level % 31.07/5.04 User error: GNN currently only supports monomorphic FOL. % 31.07/5.04 % (245738)Instruction limit reached! % 31.07/5.04 % (245738)------------------------------ % 31.07/5.04 % (245738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.07/5.04 % (245738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.07/5.04 % (245738)CaDiCaL version: 2.1.3 % 31.07/5.04 % (245738)Termination reason: Instruction limit % 31.07/5.04 % (245738)Termination phase: Saturation % 31.07/5.04 % (245738)Time elapsed: 0.230 s % 31.07/5.04 % (245738)Peak memory usage: 92 MB % 38.12/6.05 % (245738)Instructions burned: 440 (million) % 38.12/6.05 % (245745)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=4193845297:st=2:s2a=on:i=524:s2at=2:ss=axioms_2977 on theBenchmark for (2977ds/524Mi) % 38.12/6.05 % Exception at run slice level % 38.12/6.05 User error: GNN currently only supports monomorphic FOL. % 38.12/6.05 % (245746)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2252677027:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2976 on theBenchmark for (2976ds/1016Mi) % 38.12/6.05 % (245747)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3623811875:i=14123:bd=preordered:ins=4_2976 on theBenchmark for (2976ds/14123Mi) % 38.12/6.05 % (245749)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2703181866:i=5781:kws=precedence:bd=all:rawr=on_2975 on theBenchmark for (2975ds/5781Mi) % 38.12/6.05 % Exception at run slice level % 38.12/6.05 User error: GNN currently only supports monomorphic FOL. % 38.12/6.05 % (245745)Instruction limit reached! % 38.12/6.05 % (245745)------------------------------ % 38.12/6.06 % (245745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.12/6.06 % (245745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.12/6.06 % (245745)CaDiCaL version: 2.1.3 % 38.12/6.06 % (245745)Termination reason: Instruction limit % 38.12/6.06 % (245745)Termination phase: Saturation % 38.12/6.06 % (245745)Time elapsed: 0.243 s % 38.12/6.06 % (245745)Peak memory usage: 90 MB % 38.12/6.06 % (245745)Instructions burned: 525 (million) % 38.12/6.06 % (245753)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=181777205:i=2448:gtgl=5:bd=preordered:gtg=all_2974 on theBenchmark for (2974ds/2448Mi) % 38.12/6.06 % (245754)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1449097702:i=3223:kws=precedence:fgj=on:av=off_2973 on theBenchmark for (2973ds/3223Mi) % 38.12/6.06 % Exception at run slice level % 38.12/6.06 User error: GNN currently only supports monomorphic FOL. % 38.12/6.06 % (245746)Instruction limit reached! % 38.12/6.06 % (245746)------------------------------ % 38.12/6.06 % (245746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.12/6.06 % (245746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.12/6.06 % (245746)CaDiCaL version: 2.1.3 % 38.12/6.06 % (245746)Termination reason: Instruction limit % 38.12/6.06 % (245746)Termination phase: Saturation % 38.12/6.06 % (245746)Time elapsed: 0.523 s % 38.12/6.06 % (245746)Peak memory usage: 104 MB % 38.12/6.06 % (245746)Instructions burned: 1018 (million) % 38.12/6.06 % (245757)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2550759665:st=5.6:i=2033:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/2033Mi) % 38.12/6.06 % Exception at run slice level % 38.12/6.06 User error: GNN currently only supports monomorphic FOL. % 38.12/6.06 % (245758)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=946662955:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2970 on theBenchmark for (2970ds/2055Mi) % 38.12/6.06 % Exception at run slice level % 38.12/6.06 User error: GNN currently only supports monomorphic FOL. % 38.12/6.06 % (245760)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=1895336427:i=21611:sd=3:ss=axioms_2968 on theBenchmark for (2968ds/21611Mi) % 38.12/6.06 % (245762)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1532149594:i=4835:sd=13:ss=axioms:sgt=23_2968 on theBenchmark for (2968ds/4835Mi) % 38.12/6.06 % Exception at run slice level % 38.12/6.06 User error: GNN currently only supports monomorphic FOL. % 38.12/6.06 % Exception at run slice level % 38.12/6.06 User error: GNN currently only supports monomorphic FOL. % 38.12/6.06 % (245765)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=1735940788:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2965 on theBenchmark for (2965ds/797Mi) % 38.12/6.06 % Exception at run slice level % 38.12/6.06 User error: GNN currently only supports monomorphic FOL. % 38.12/6.06 % (245766)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=194683825:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2965 on theBenchmark for (2965ds/2326Mi) % 49.98/8.80 % (245766)Refutation not found, incomplete strategy % 49.98/8.80 % (245766)------------------------------ % 49.98/8.80 % (245766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.98/8.80 % (245766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.98/8.80 % (245766)CaDiCaL version: 2.1.3 % 49.98/8.80 % (245766)Termination reason: Refutation not found, incomplete strategy % 49.98/8.80 % (245766)Time elapsed: 0.006 s % 49.98/8.80 % (245766)Peak memory usage: 88 MB % 49.98/8.80 % (245766)Instructions burned: 10 (million) % 49.98/8.80 % (245768)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=545873417:i=6038:nm=6_2963 on theBenchmark for (2963ds/6038Mi) % 49.98/8.80 % (245766)------------------------------ % 49.98/8.80 % (245766)------------------------------ % 49.98/8.80 % (245726)Instruction limit reached! % 49.98/8.80 % (245726)------------------------------ % 49.98/8.80 % (245726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.98/8.80 % (245726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.98/8.80 % (245726)CaDiCaL version: 2.1.3 % 49.98/8.80 % (245726)Termination reason: Instruction limit % 49.98/8.80 % (245726)Termination phase: Saturation % 49.98/8.80 % (245726)Time elapsed: 2.177 s % 49.98/8.80 % (245726)Peak memory usage: 96 MB % 49.98/8.80 % (245726)Instructions burned: 3707 (million) % 49.98/8.80 % (245765)Instruction limit reached! % 49.98/8.80 % (245765)------------------------------ % 49.98/8.80 % (245765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.98/8.80 % (245765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.98/8.80 % (245765)CaDiCaL version: 2.1.3 % 49.98/8.80 % (245765)Termination reason: Instruction limit % 49.98/8.80 % (245765)Termination phase: Saturation % 49.98/8.80 % (245765)Time elapsed: 0.447 s % 49.98/8.80 % (245765)Peak memory usage: 97 MB % 49.98/8.80 % (245765)Instructions burned: 798 (million) % 49.98/8.80 % (245771)lrs+10_1_sil=32000:sp=occurrence:random_seed=2898906822:st=2:i=33334:sd=3:ss=included:sgt=32_2961 on theBenchmark for (2961ds/33334Mi) % 49.98/8.80 % (245772)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3850396394:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2960 on theBenchmark for (2960ds/1008Mi) % 49.98/8.80 % Exception at run slice level % 49.98/8.80 User error: GNN currently only supports monomorphic FOL. % 49.98/8.80 % (245720)Instruction limit reached! % 49.98/8.80 % (245720)------------------------------ % 49.98/8.80 % (245720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.98/8.80 % (245720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.98/8.80 % (245720)CaDiCaL version: 2.1.3 % 49.98/8.80 % (245720)Termination reason: Instruction limit % 49.98/8.80 % (245720)Termination phase: Saturation % 49.98/8.80 % (245720)Time elapsed: 2.606 s % 49.98/8.80 % (245720)Peak memory usage: 113 MB % 49.98/8.80 % (245720)Instructions burned: 4851 (million) % 49.98/8.80 % (245773)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=3251094029:i=8327:s2at=5:bd=preordered_2959 on theBenchmark for (2959ds/8327Mi) % 49.98/8.80 % (245749)Instruction limit reached! % 49.98/8.80 % (245749)------------------------------ % 49.98/8.80 % (245749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.98/8.80 % (245749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.98/8.80 % (245749)CaDiCaL version: 2.1.3 % 49.98/8.80 % (245749)Termination reason: Instruction limit % 49.98/8.80 % (245749)Termination phase: Saturation % 49.98/8.80 % (245749)Time elapsed: 1.683 s % 49.98/8.80 % (245749)Peak memory usage: 131 MB % 49.98/8.80 % (245749)Instructions burned: 5781 (million) % 49.98/8.80 % (245776)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=1856012505:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2958 on theBenchmark for (2958ds/1083Mi) % 49.98/8.80 % (245777)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=3550632058:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2958 on theBenchmark for (2958ds/1084Mi) % 49.98/8.80 % (245779)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2467905009:i=6995:s2at=5:gtg=all_2957 on theBenchmark for (2957ds/6995Mi) % 60.78/10.17 % Exception at run slice level % 60.78/10.17 User error: GNN currently only supports monomorphic FOL. % 60.78/10.17 % Exception at run slice level % 60.78/10.17 User error: GNN currently only supports monomorphic FOL. % 60.78/10.17 % (245772)Instruction limit reached! % 60.78/10.17 % (245772)------------------------------ % 60.78/10.17 % (245772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.78/10.17 % (245772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.78/10.17 % (245772)CaDiCaL version: 2.1.3 % 60.78/10.17 % (245772)Termination reason: Instruction limit % 60.78/10.17 % (245772)Termination phase: Saturation % 60.78/10.17 % (245772)Time elapsed: 0.504 s % 60.78/10.17 % (245772)Peak memory usage: 96 MB % 60.78/10.17 % (245772)Instructions burned: 1010 (million) % 60.78/10.17 % (245784)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2561688708:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2954 on theBenchmark for (2954ds/3372Mi) % 60.78/10.17 % (245783)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2489735401:st=2:i=6225:sd=15:ss=axioms_2954 on theBenchmark for (2954ds/6225Mi) % 60.78/10.17 % (245777)Instruction limit reached! % 60.78/10.17 % (245777)------------------------------ % 60.78/10.17 % (245777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.78/10.17 % (245777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.78/10.17 % (245777)CaDiCaL version: 2.1.3 % 60.78/10.17 % (245777)Termination reason: Instruction limit % 60.78/10.17 % (245777)Termination phase: Saturation % 60.78/10.17 % (245777)Time elapsed: 0.372 s % 60.78/10.17 % (245777)Peak memory usage: 88 MB % 60.78/10.17 % (245777)Instructions burned: 1085 (million) % 60.78/10.17 % (245785)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=3824654623:st=2.3:i=26457:sd=10:ss=included:sgt=8_2954 on theBenchmark for (2954ds/26457Mi) % 60.78/10.17 % (245776)Instruction limit reached! % 60.78/10.17 % (245776)------------------------------ % 60.78/10.17 % (245776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.78/10.17 % (245776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.78/10.17 % (245776)CaDiCaL version: 2.1.3 % 60.78/10.17 % (245776)Termination reason: Instruction limit % 60.78/10.17 % (245776)Termination phase: Saturation % 60.78/10.17 % (245776)Time elapsed: 0.529 s % 60.78/10.17 % (245776)Peak memory usage: 101 MB % 60.78/10.17 % (245776)Instructions burned: 1085 (million) % 60.78/10.17 % Exception at run slice level % 60.78/10.17 User error: GNN currently only supports monomorphic FOL. % 60.78/10.17 % (245788)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=3222355591:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2952 on theBenchmark for (2952ds/13494Mi) % 60.78/10.17 % (245790)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=345846385:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2951 on theBenchmark for (2951ds/2503Mi) % 60.78/10.17 % (245790)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 60.78/10.17 % (245792)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=2806851964:i=2559:sd=1:ep=RSTC:ss=axioms_2951 on theBenchmark for (2951ds/2559Mi) % 60.78/10.17 % Exception at run slice level % 60.78/10.17 User error: GNN currently only supports monomorphic FOL. % 60.78/10.17 % Exception at run slice level % 60.78/10.17 User error: GNN currently only supports monomorphic FOL. % 60.78/10.17 % Exception at run slice level % 60.78/10.17 User error: GNN currently only supports monomorphic FOL. % 60.78/10.17 % (245795)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=42989459:i=30753:av=off:ss=included_2949 on theBenchmark for (2949ds/30753Mi) % 60.78/10.17 % (245796)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=1116547153:i=26473:ep=RSTC_2948 on theBenchmark for (2948ds/26473Mi) % 60.78/10.17 % Exception at run slice level % 60.78/10.17 User error: GNN currently only supports monomorphic FOL. % 60.78/10.17 % (245797)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=2175030050:cts=off:i=2759:kws=inv_arity:fgj=on_2947 on theBenchmark for (2947ds/2759Mi) % 71.57/11.74 % (245800)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=366240629:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2946 on theBenchmark for (2946ds/5665Mi) % 71.57/11.74 % (245800)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 71.57/11.74 % Exception at run slice level % 71.57/11.74 User error: GNN currently only supports monomorphic FOL. % 71.57/11.74 % Exception at run slice level % 71.57/11.74 User error: GNN currently only supports monomorphic FOL. % 71.57/11.74 % (245803)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=1646779982:i=1532:ep=RS:ss=axioms_2943 on theBenchmark for (2943ds/1532Mi) % 71.57/11.74 % (245804)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=609793935:i=1565:sd=2:ss=axioms:sgt=32_2942 on theBenchmark for (2942ds/1565Mi) % 71.57/11.74 % (245762)Instruction limit reached! % 71.57/11.74 % (245762)------------------------------ % 71.57/11.74 % (245762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.57/11.74 % (245762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.57/11.74 % (245762)CaDiCaL version: 2.1.3 % 71.57/11.74 % (245762)Termination reason: Instruction limit % 71.57/11.74 % (245762)Termination phase: Saturation % 71.57/11.74 % (245762)Time elapsed: 2.660 s % 71.57/11.74 % (245762)Peak memory usage: 109 MB % 71.57/11.74 % (245762)Instructions burned: 4836 (million) % 71.57/11.74 % (245807)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=1177771209:i=1572:fgj=on:gsp=on_2940 on theBenchmark for (2940ds/1572Mi) % 71.57/11.74 % (245807)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 71.57/11.74 % Exception at run slice level % 71.57/11.74 User error: GNN currently only supports monomorphic FOL. % 71.57/11.74 % (245809)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=1652192829:i=6052:sd=4:ss=axioms:sgt=24_2935 on theBenchmark for (2935ds/6052Mi) % 71.57/11.74 % Exception at run slice level% Exception at run slice level % 71.57/11.74 % 71.57/11.74 User error: User error: GNN currently only supports monomorphic FOL.GNN currently only supports monomorphic FOL. % 71.57/11.74 % 71.57/11.74 % Exception at run slice level % 71.57/11.74 User error: GNN currently only supports monomorphic FOL. % 71.57/11.74 % Exception at run slice level % 71.57/11.74 User error: GNN currently only supports monomorphic FOL. % 71.57/11.74 % (245783)Instruction limit reached! % 71.57/11.74 % (245783)------------------------------ % 71.57/11.74 % (245783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.57/11.74 % (245783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.57/11.74 % (245783)CaDiCaL version: 2.1.3 % 71.57/11.74 % (245783)Termination reason: Instruction limit % 71.57/11.74 % (245783)Termination phase: Saturation % 71.57/11.74 % (245783)Time elapsed: 2.853 s % 71.57/11.74 % (245783)Peak memory usage: 149 MB % 71.57/11.74 % (245783)Instructions burned: 6226 (million) % 71.57/11.74 % (245811)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=2124291932:i=3500:sd=1:bd=preordered:sup=off:ss=included_2925 on theBenchmark for (2925ds/3500Mi) % 71.57/11.74 % (245813)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=458127473:i=66096:add=on_2925 on theBenchmark for (2925ds/66096Mi) % 71.57/11.74 % (245814)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=820576946:i=1884:sd=1:nm=60:ss=axioms_2925 on theBenchmark for (2925ds/1884Mi) % 71.57/11.74 % (245812)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=1580838152:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2925 on theBenchmark for (2925ds/1842Mi) % 71.57/11.74 % (245812)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 71.57/11.74 % (245815)lrs-1011_4:1_sil=16000:bsr=on:random_seed=210485650:cts=off:i=5469:bs=on:fsr=off_2924 on theBenchmark for (2924ds/5469Mi) % 83.21/13.49 % Exception at run slice level% Exception at run slice level % 83.21/13.49 % 83.21/13.49 % Exception at run slice levelUser error: User error: GNN currently only supports monomorphic FOL.GNN currently only supports monomorphic FOL. % 83.21/13.49 % Exception at run slice level % 83.21/13.49 % 83.21/13.49 User error: GNN currently only supports monomorphic FOL. % 83.21/13.49 % 83.21/13.49 User error: GNN currently only supports monomorphic FOL. % 83.21/13.49 % (245822)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3565784448:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2917 on theBenchmark for (2917ds/2110Mi) % 83.21/13.49 % (245821)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=1403656687:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2917 on theBenchmark for (2917ds/2037Mi) % 83.21/13.49 % (245823)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=2827494578:i=2430:add=off:aac=none:nm=16_2917 on theBenchmark for (2917ds/2430Mi) % 83.21/13.49 % (245824)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=4292993083:cond=fast:i=4891_2917 on theBenchmark for (2917ds/4891Mi) % 83.21/13.49 % Exception at run slice level % 83.21/13.49 User error: GNN currently only supports monomorphic FOL. % 83.21/13.49 % Exception at run slice level % 83.21/13.49 User error: GNN currently only supports monomorphic FOL. % 83.21/13.49 % Exception at run slice level % 83.21/13.49 User error: GNN currently only supports monomorphic FOL. % 83.21/13.49 % Exception at run slice level % 83.21/13.49 User error: GNN currently only supports monomorphic FOL. % 83.21/13.49 % (245831)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=562076162:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2911 on theBenchmark for (2911ds/10353Mi) % 83.21/13.49 % (245832)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3171281210:i=7860_2911 on theBenchmark for (2911ds/7860Mi) % 83.21/13.49 % (245829)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=2581773475:st=2:i=14845:sd=2:ss=included:fsd=on_2911 on theBenchmark for (2911ds/14845Mi) % 83.21/13.49 % (245830)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=1830319057:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2911 on theBenchmark for (2911ds/7534Mi) % 83.21/13.49 % (245832)Refutation not found, incomplete strategy % 83.21/13.49 % (245832)------------------------------ % 83.21/13.49 % (245832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.21/13.49 % (245832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.21/13.49 % (245832)CaDiCaL version: 2.1.3 % 83.21/13.49 % (245832)Termination reason: Refutation not found, incomplete strategy % 83.21/13.49 % (245832)Time elapsed: 0.006 s % 83.21/13.49 % (245832)Peak memory usage: 88 MB % 83.21/13.49 % (245832)Instructions burned: 9 (million) % 83.21/13.49 % (245832)------------------------------ % 83.21/13.49 % (245832)------------------------------ % 83.21/13.49 % Exception at run slice level% Exception at run slice level % 83.21/13.49 User error: GNN currently only supports monomorphic FOL. % 83.21/13.49 % 83.21/13.49 User error: GNN currently only supports monomorphic FOL. % 83.21/13.49 % Exception at run slice level % 83.21/13.49 User error: GNN currently only supports monomorphic FOL. % 83.21/13.49 % (245837)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=424449540:i=7896:sd=2:bs=on:ss=included:sgt=20_2907 on theBenchmark for (2907ds/7896Mi) % 83.21/13.49 % (245838)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=3099780412:i=5812:gtgl=2:gtg=all_2906 on theBenchmark for (2906ds/5812Mi) % 83.21/13.49 % (245839)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=1227808274:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2906 on theBenchmark for (2906ds/2965Mi) % 83.21/13.49 % (245840)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=3040665675:i=2967:kws=precedence:bd=preordered:av=off_2906 on theBenchmark for (2906ds/2967Mi) % 100.86/15.87 % Exception at run slice level % 100.86/15.87 User error: GNN currently only supports monomorphic FOL. % 100.86/15.87 % Exception at run slice level % 100.86/15.87 User error: GNN currently only supports monomorphic FOL. % 100.86/15.87 % Exception at run slice level % 100.86/15.87 User error: GNN currently only supports monomorphic FOL. % 100.86/15.87 % Exception at run slice level % 100.86/15.87 User error: GNN currently only supports monomorphic FOL. % 100.86/15.87 % (245845)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=4260744818:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2902 on theBenchmark for (2902ds/3022Mi) % 100.86/15.87 % (245846)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=740809712:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2901 on theBenchmark for (2901ds/3207Mi) % 100.86/15.87 % (245847)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=2724419649:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2901 on theBenchmark for (2901ds/3289Mi) % 100.86/15.87 % (245848)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=1449205934:i=38569:sd=3:ss=axioms:sgt=32_2901 on theBenchmark for (2901ds/38569Mi) % 100.86/15.87 % Exception at run slice level % 100.86/15.87 User error: GNN currently only supports monomorphic FOL. % 100.86/15.87 % Exception at run slice level % 100.86/15.87 User error: GNN currently only supports monomorphic FOL. % 100.86/15.87 % Exception at run slice level % 100.86/15.87 User error: GNN currently only supports monomorphic FOL. % 100.86/15.87 % Exception at run slice level % 100.86/15.87 User error: GNN currently only supports monomorphic FOL. % 100.86/15.87 % (245853)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=374684370:cts=off:i=3394_2897 on theBenchmark for (2897ds/3394Mi) % 100.86/15.87 % (245854)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=3269532393:i=33824:bd=preordered_2896 on theBenchmark for (2896ds/33824Mi) % 100.86/15.87 % (245855)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=121193246:i=20684:bd=all:gtg=exists_sym_2896 on theBenchmark for (2896ds/20684Mi) % 100.86/15.87 % (245856)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=4225365391: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_2896 on theBenchmark for (2896ds/7222Mi) % 100.86/15.87 % (245856)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 100.86/15.87 % Exception at run slice level % 100.86/15.87 User error: GNN currently only supports monomorphic FOL. % 100.86/15.87 % Exception at run slice level % 100.86/15.87 User error: GNN currently only supports monomorphic FOL. % 100.86/15.87 % Exception at run slice level % 100.86/15.87 User error: GNN currently only supports monomorphic FOL. % 100.86/15.87 % Exception at run slice level % 100.86/15.87 User error: GNN currently only supports monomorphic FOL. % 100.86/15.87 % (245861)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=3296689446:st=4:i=7295:sd=4:ep=R:ss=axioms_2892 on theBenchmark for (2892ds/7295Mi) % 100.86/15.87 % (245862)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=1685545498:i=4036:ins=10_2891 on theBenchmark for (2891ds/4036Mi) % 100.86/15.87 % (245864)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=559448751:i=17599:gtg=all:ss=axioms:fsd=on_2891 on theBenchmark for (2891ds/17599Mi) % 100.86/15.87 % (245863)lrs+10_1_sil=128000:lcm=predicate:random_seed=1808344970:st=3:i=43697:sd=5:ss=axioms_2891 on theBenchmark for (2891ds/43697Mi) % 100.86/15.87 % (245815)Instruction limit reached! % 100.86/15.87 % (245815)------------------------------ % 131.26/20.03 % (245815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.26/20.03 % (245815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.26/20.03 % (245815)CaDiCaL version: 2.1.3 % 131.26/20.03 % (245815)Termination reason: Instruction limit % 131.26/20.03 % (245815)Termination phase: Saturation % 131.26/20.03 % (245815)Time elapsed: 2.946 s % 131.26/20.03 % (245815)Peak memory usage: 129 MB % 131.26/20.03 % (245815)Instructions burned: 5470 (million) % 131.26/20.03 % (245869)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=3161385273:i=4547:bd=preordered_2889 on theBenchmark for (2889ds/4547Mi) % 131.26/20.03 % Exception at run slice level % 131.26/20.03 User error: GNN currently only supports monomorphic FOL. % 131.26/20.03 % Exception at run slice level % 131.26/20.03 User error: % Exception at run slice levelGNN currently only supports monomorphic FOL. % 131.26/20.03 % 131.26/20.03 User error: GNN currently only supports monomorphic FOL. % 131.26/20.03 % (245871)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=1319037526:i=9294:av=off_2886 on theBenchmark for (2886ds/9294Mi) % 131.26/20.03 % (245873)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1247757506:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2886 on theBenchmark for (2886ds/4793Mi) % 131.26/20.03 % (245872)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3636376102:i=32849:add=on_2886 on theBenchmark for (2886ds/32849Mi) % 131.26/20.03 % Exception at run slice level % 131.26/20.03 User error: GNN currently only supports monomorphic FOL. % 131.26/20.03 % (245877)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=3725429043:i=4840:nm=4:av=off_2884 on theBenchmark for (2884ds/4840Mi) % 131.26/20.03 % Exception at run slice level % 131.26/20.03 User error: GNN currently only supports monomorphic FOL. % 131.26/20.03 % Exception at run slice level % 131.26/20.03 User error: GNN currently only supports monomorphic FOL. % 131.26/20.03 % Exception at run slice level % 131.26/20.03 User error: GNN currently only supports monomorphic FOL. % 131.26/20.03 % (245879)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=4133842087:cts=off:i=5002_2881 on theBenchmark for (2881ds/5002Mi) % 131.26/20.03 % (245880)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=506214159:i=30479:sd=3:ss=axioms_2881 on theBenchmark for (2881ds/30479Mi) % 131.26/20.03 % (245881)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=2132790728:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2881 on theBenchmark for (2881ds/11035Mi) % 131.26/20.03 % (245881)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 131.26/20.03 % Exception at run slice level % 131.26/20.03 User error: GNN currently only supports monomorphic FOL. % 131.26/20.03 % (245885)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=1480237456:i=5835_2878 on theBenchmark for (2878ds/5835Mi) % 131.26/20.03 % Exception at run slice level % 131.26/20.03 User error: GNN currently only supports monomorphic FOL. % 131.26/20.03 % Exception at run slice level % 131.26/20.03 User error: GNN currently only supports monomorphic FOL. % 131.26/20.03 % Exception at run slice level % 131.26/20.03 User error: GNN currently only supports monomorphic FOL. % 131.26/20.03 % (245887)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=218236657:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2876 on theBenchmark for (2876ds/5890Mi) % 131.26/20.03 % (245888)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=1947395542:cts=off:i=19910:ep=RS_2875 on theBenchmark for (2875ds/19910Mi) % 131.26/20.03 % (245889)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=2316173922:i=20312:bd=preordered:fsr=off:er=filter_2875 on theBenchmark for (2875ds/20312Mi) % 131.26/20.03 % Exception at run slice level % 131.26/20.03 User error: GNN currently only supports monomorphic FOL. % 131.26/20.03 % (245893)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=2184597657:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2873 on theBenchmark for (2873ds/13822Mi) % 159.62/24.06 % Exception at run slice level % 159.62/24.06 User error: GNN currently only supports monomorphic FOL. % 159.62/24.06 % Exception at run slice level % 159.62/24.06 User error: GNN currently only supports monomorphic FOL. % 159.62/24.06 % (245796)Instruction limit reached! % 159.62/24.06 % (245796)------------------------------ % 159.62/24.06 % (245796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.62/24.06 % (245796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.62/24.06 % (245796)CaDiCaL version: 2.1.3 % 159.62/24.06 % (245796)Termination reason: Instruction limit % 159.62/24.06 % (245796)Termination phase: Saturation % 159.62/24.06 % (245796)Time elapsed: 7.686 s % 159.62/24.06 % (245796)Peak memory usage: 394 MB % 159.62/24.06 % (245796)Instructions burned: 26474 (million) % 159.62/24.06 % (245895)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=1865181276:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2871 on theBenchmark for (2871ds/7144Mi) % 159.62/24.06 % (245896)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=4058968455:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2870 on theBenchmark for (2870ds/15184Mi) % 159.62/24.06 % Exception at run slice level % 159.62/24.06 User error: GNN currently only supports monomorphic FOL. % 159.62/24.06 % (245897)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=3873140381:i=107375_2869 on theBenchmark for (2869ds/107375Mi) % 159.62/24.06 % (245900)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=1498457480:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2868 on theBenchmark for (2868ds/7958Mi) % 159.62/24.06 % Exception at run slice level % 159.62/24.06 User error: GNN currently only supports monomorphic FOL. % 159.62/24.06 % Exception at run slice level % 159.62/24.06 User error: GNN currently only supports monomorphic FOL. % 159.62/24.06 % (245903)dis+10_128_sil=16000:nwc=0.7:random_seed=2620083365:i=15999:nm=2:gsp=on_2865 on theBenchmark for (2865ds/15999Mi) % 159.62/24.06 % (245903)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 159.62/24.06 % Exception at run slice level % 159.62/24.06 User error: GNN currently only supports monomorphic FOL. % 159.62/24.06 % (245905)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=2969139218:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2864 on theBenchmark for (2864ds/8139Mi) % 159.62/24.06 % (245932)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=59468402:st=4:i=8950:sd=5:ss=axioms_2863 on theBenchmark for (2863ds/8950Mi) % 159.62/24.06 % Exception at run slice level % 159.62/24.06 User error: GNN currently only supports monomorphic FOL. % 159.62/24.06 % (246041)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=3455177667:i=9809:ins=10:av=off_2858 on theBenchmark for (2858ds/9809Mi) % 159.62/24.06 % Exception at run slice level % 159.62/24.06 User error: GNN currently only supports monomorphic FOL. % 159.62/24.06 % (246153)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=3139862169:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2852 on theBenchmark for (2852ds/9885Mi) % 159.62/24.06 % (245895)Instruction limit reached! % 159.62/24.06 % (245895)------------------------------ % 159.62/24.06 % (245895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.62/24.06 % (245895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.62/24.06 % (245895)CaDiCaL version: 2.1.3 % 159.62/24.06 % (245895)Termination reason: Instruction limit % 159.62/24.06 % (245895)Termination phase: Saturation % 159.62/24.06 % (245895)Time elapsed: 2.012 s % 159.62/24.06 % (245895)Peak memory usage: 181 MB % 159.62/24.06 % (245895)Instructions burned: 7146 (million) % 159.62/24.06 % (246175)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=1695831658:cond=fast:i=32078:fgj=on:av=off_2849 on theBenchmark for (2849ds/32078Mi) % 184.65/27.63 % Exception at run slice level % 184.65/27.63 User error: GNN currently only supports monomorphic FOL. % 184.65/27.63 % Exception at run slice level % 184.65/27.63 User error: GNN currently only supports monomorphic FOL. % 184.65/27.63 % (246177)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=4127794566:i=11101:bd=all:ss=axioms:sgt=8_2846 on theBenchmark for (2846ds/11101Mi) % 184.65/27.63 % (246182)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=3829383105:cond=on:i=13220:s2at=3:aac=none:fsd=on_2845 on theBenchmark for (2845ds/13220Mi) % 184.65/27.63 % Exception at run slice level % 184.65/27.63 User error: GNN currently only supports monomorphic FOL. % 184.65/27.63 % (246197)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=2441576444:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2838 on theBenchmark for (2838ds/13528Mi) % 184.65/27.63 % Exception at run slice level % 184.65/27.63 User error: GNN currently only supports monomorphic FOL. % 184.65/27.63 % (246304)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=197124904:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2833 on theBenchmark for (2833ds/14854Mi) % 184.65/27.63 % Exception at run slice level % 184.65/27.63 User error: GNN currently only supports monomorphic FOL. % 184.65/27.63 % (246353)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=17114478:i=14974:ss=axioms:sgt=16_2828 on theBenchmark for (2828ds/14974Mi) % 184.65/27.63 % Exception at run slice level % 184.65/27.63 User error: GNN currently only supports monomorphic FOL. % 184.65/27.63 % (246355)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=373374569:i=33081:aac=none:fgj=on:bd=all:fsr=off_2822 on theBenchmark for (2822ds/33081Mi) % 184.65/27.63 % Exception at run slice level % 184.65/27.63 User error: GNN currently only supports monomorphic FOL. % 184.65/27.63 % (245905)Instruction limit reached! % 184.65/27.63 % (245905)------------------------------ % 184.65/27.63 % (245905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.65/27.63 % (245905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.65/27.63 % (245905)CaDiCaL version: 2.1.3 % 184.65/27.63 % (245905)Termination reason: Instruction limit % 184.65/27.63 % (245905)Termination phase: Saturation % 184.65/27.63 % (245905)Time elapsed: 4.539 s % 184.65/27.63 % (245905)Peak memory usage: 143 MB % 184.65/27.63 % (245905)Instructions burned: 8141 (million) % 184.65/27.63 % (246357)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=2963154832:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2817 on theBenchmark for (2817ds/50856Mi) % 184.65/27.63 % (246358)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=3287773535:i=69865_2817 on theBenchmark for (2817ds/69865Mi) % 184.65/27.63 % Exception at run slice level % 184.65/27.63 User error: GNN currently only supports monomorphic FOL. % 184.65/27.63 % Exception at run slice level % 184.65/27.63 User error: GNN currently only supports monomorphic FOL. % 184.65/27.63 % (246361)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=4018004753:cond=fast:i=17802:gtgl=3:gtg=all_2812 on theBenchmark for (2812ds/17802Mi) % 184.65/27.63 % Exception at run slice level % 184.65/27.63 User error: Immediate (shared) subterms of term/literal amap_fm(X1,X0,X3,neg(X1,X2)) = sF25(X1,X0,X3,X2) have different types/not well-typed! % 184.65/27.63 % (246362)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=575671510:i=96644_2812 on theBenchmark for (2812ds/96644Mi) % 184.65/27.63 % (246364)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 184.65/27.63 % (246364)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=1537018981:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2810 on theBenchmark for (2810ds/21161Mi) % 184.65/27.63 % (246177)Instruction limit reached! % 193.17/28.89 % (246177)------------------------------ % 193.17/28.89 % (246177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 193.17/28.89 % (246177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.17/28.89 % (246177)CaDiCaL version: 2.1.3 % 193.17/28.89 % (246177)Termination reason: Instruction limit % 193.17/28.89 % (246177)Termination phase: Saturation % 193.17/28.89 % (246177)Time elapsed: 3.779 s % 193.17/28.89 % (246177)Peak memory usage: 179 MB % 193.17/28.89 % (246177)Instructions burned: 11106 (million) % 193.17/28.89 % (246367)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=4252211135:i=22761:gtg=all:ss=axioms:fsd=on_2806 on theBenchmark for (2806ds/22761Mi) % 193.17/28.89 % Exception at run slice level % 193.17/28.89 User error: GNN currently only supports monomorphic FOL. % 193.17/28.89 % (246369)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=1339564769:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2803 on theBenchmark for (2803ds/23713Mi) % 193.17/28.89 % (245903)Instruction limit reached! % 193.17/28.89 % (245903)------------------------------ % 193.17/28.89 % (245903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 193.17/28.89 % (245903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.17/28.89 % (245903)CaDiCaL version: 2.1.3 % 193.17/28.89 % (245903)Termination reason: Instruction limit % 193.17/28.89 % (245903)Termination phase: Saturation % 193.17/28.89 % (245903)Time elapsed: 8.533 s % 193.17/28.89 % (245903)Peak memory usage: 214 MB % 193.17/28.89 % (245903)Instructions burned: 16000 (million) % 193.17/28.89 % (246371)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=2748197678:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2778 on theBenchmark for (2778ds/26509Mi) % 193.17/28.89 % (245771)Instruction limit reached! % 193.17/28.89 % (245771)------------------------------ % 193.17/28.89 % (245771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 193.17/28.89 % (245771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.17/28.89 % (245771)CaDiCaL version: 2.1.3 % 193.17/28.89 % (245771)Termination reason: Instruction limit % 193.17/28.89 % (245771)Termination phase: Saturation % 193.17/28.89 % (245771)Time elapsed: 18.352 s % 193.17/28.89 % (245771)Peak memory usage: 357 MB % 193.17/28.89 % (245771)Instructions burned: 33335 (million) % 193.17/28.89 % (246373)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=2717973126:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2775 on theBenchmark for (2775ds/28957Mi) % 193.17/28.89 % Exception at run slice level % 193.17/28.89 User error: GNN currently only supports monomorphic FOL. % 193.17/28.89 % (245888)Instruction limit reached! % 193.17/28.89 % (245888)------------------------------ % 193.17/28.89 % (245888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 193.17/28.89 % (245888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.17/28.89 % (245888)CaDiCaL version: 2.1.3 % 193.17/28.89 % (245888)Termination reason: Instruction limit % 193.17/28.89 % (245888)Termination phase: Saturation % 193.17/28.89 % (245888)Time elapsed: 10.264 s % 193.17/28.89 % (245888)Peak memory usage: 128 MB % 193.17/28.89 % (245888)Instructions burned: 19911 (million) % 193.17/28.89 % (246375)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=3593417782:i=29246:s2at=-1:kws=inv_arity:ins=10_2773 on theBenchmark for (2773ds/29246Mi) % 193.17/28.89 % (246376)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=2743855214:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2771 on theBenchmark for (2771ds/30082Mi) % 193.17/28.89 % (246376)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 193.17/28.89 % Exception at run slice level % 193.17/28.89 User error: GNN currently only supports monomorphic FOL. % 193.17/28.89 % Exception at run slice level % 193.17/28.89 User error: GNN currently only supports monomorphic FOL. % 193.17/28.89 % (246379)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=916604705:i=32262:bd=preordered_2767 on theBenchmark for (2767ds/32262Mi) % 200.14/29.86 % (246380)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=2458775607:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2766 on theBenchmark for (2766ds/32870Mi) % 200.14/29.86 % Exception at run slice level % 200.14/29.86 User error: GNN currently only supports monomorphic FOL. % 200.14/29.86 % Exception at run slice level % 200.14/29.86 User error: GNN currently only supports monomorphic FOL. % 200.14/29.86 % (246383)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=3681290357:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2762 on theBenchmark for (2762ds/33295Mi) % 200.14/29.86 % (246384)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=3776912575:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2761 on theBenchmark for (2761ds/36826Mi) % 200.14/29.86 % Exception at run slice level % 200.14/29.86 User error: GNN currently only supports monomorphic FOL. % 200.14/29.86 % (246387)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=3344536355:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2757 on theBenchmark for (2757ds/92981Mi) % 200.14/29.86 % Exception at run slice level % 200.14/29.86 User error: GNN currently only supports monomorphic FOL. % 200.14/29.86 % (246389)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=3631689725:s2pl=on:i=49423_2752 on theBenchmark for (2752ds/49423Mi) % 200.14/29.86 % Exception at run slice level % 200.14/29.86 User error: GNN currently only supports monomorphic FOL. % 200.14/29.86 % (246391)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=2836395959:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2746 on theBenchmark for (2746ds/57299Mi) % 200.14/29.86 % Exception at run slice level % 200.14/29.86 User error: GNN currently only supports monomorphic FOL. % 200.14/29.86 % (246369)Instruction limit reached! % 200.14/29.86 % (246369)------------------------------ % 200.14/29.86 % (246369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.14/29.86 % (246369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.14/29.86 % (246369)CaDiCaL version: 2.1.3 % 200.14/29.86 % (246369)Termination reason: Instruction limit % 200.14/29.86 % (246369)Termination phase: Saturation % 200.14/29.86 % (246369)Time elapsed: 6.185 s % 200.14/29.86 % (246369)Peak memory usage: 159 MB % 200.14/29.86 % (246369)Instructions burned: 23714 (million) % 200.14/29.86 % (246393)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=2792876149:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2741 on theBenchmark for (2741ds/127679Mi) % 200.14/29.86 % (246395)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=1566368502:i=69402:add=on:aac=none:fsr=off_2740 on theBenchmark for (2740ds/69402Mi) % 200.14/29.86 % Exception at run slice level % 200.14/29.86 User error: GNN currently only supports monomorphic FOL. % 200.14/29.86 % Exception at run slice level % 200.14/29.86 User error: GNN currently only supports monomorphic FOL. % 200.14/29.86 % (246397)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=3257266910:i=100512:doe=on:fgj=on:bd=all:fsd=on_2736 on theBenchmark for (2736ds/100512Mi) % 200.14/29.86 % (246398)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=1416885050:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2736 on theBenchmark for (2736ds/138761Mi) % 200.14/29.86 % Exception at run slice level % 200.14/29.86 User error: GNN currently only supports monomorphic FOL. % 200.14/29.86 % (246401)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=2951108474:i=282386:rtra=on_2733 on theBenchmark for (2733ds/282386Mi) % 200.14/29.86 % Exception at run slice level % 200.14/29.86 User error: GNN currently only supports monomorphic FOL. % 200.14/29.86 % Exception at run slice level % 206.82/30.72 User error: GNN currently only supports monomorphic FOL. % 206.82/30.72 % (246403)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=3941938372:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2731 on theBenchmark for (2731ds/269354Mi) % 206.82/30.72 % (246404)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=2852231967:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2730 on theBenchmark for (2730ds/283390Mi) % 206.82/30.72 % (246404)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 206.82/30.72 % Exception at run slice level % 206.82/30.72 User error: GNN currently only supports monomorphic FOL. % 206.82/30.72 % Exception at run slice level % 206.82/30.72 User error: GNN currently only supports monomorphic FOL. % 206.82/30.72 % (246407)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=1486945503:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2727 on theBenchmark for (2727ds/218Mi) % 206.82/30.72 % (246407)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 206.82/30.72 % (246407)Refutation not found, incomplete strategy % 206.82/30.72 % (246407)------------------------------ % 206.82/30.72 % (246407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.82/30.72 % (246407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.82/30.72 % (246407)CaDiCaL version: 2.1.3 % 206.82/30.72 % (246407)Termination reason: Refutation not found, incomplete strategy % 206.82/30.72 % (246407)Time elapsed: 0.001 s % 206.82/30.72 % (246407)Peak memory usage: 87 MB % 206.82/30.72 % (246407)Instructions burned: 2 (million) % 206.82/30.72 % (246407)------------------------------ % 206.82/30.72 % (246407)------------------------------ % 206.82/30.72 % (246408)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=2222833828:i=238:av=off:rtra=on:ss=axioms_2725 on theBenchmark for (2725ds/238Mi) % 206.82/30.72 % (246408)Instruction limit reached! % 206.82/30.72 % (246408)------------------------------ % 206.82/30.72 % (246408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.82/30.72 % (246408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.82/30.72 % (246408)CaDiCaL version: 2.1.3 % 206.82/30.72 % (246408)Termination reason: Instruction limit % 206.82/30.72 % (246408)Termination phase: Saturation % 206.82/30.72 % (246408)Time elapsed: 0.119 s % 206.82/30.72 % (246408)Peak memory usage: 89 MB % 206.82/30.72 % (246408)Instructions burned: 239 (million) % 206.82/30.72 % (246411)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=641347785:s2a=on:i=278:rtra=on:gtg=position_2724 on theBenchmark for (2724ds/278Mi) % 206.82/30.72 % (246412)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=3250823816:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2722 on theBenchmark for (2722ds/258Mi) % 206.82/30.72 % (246411)Instruction limit reached! % 206.82/30.72 % (246411)------------------------------ % 206.82/30.72 % (246411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.82/30.72 % (246411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.82/30.72 % (246411)CaDiCaL version: 2.1.3 % 206.82/30.72 % (246411)Termination reason: Instruction limit % 206.82/30.72 % (246411)Termination phase: Saturation % 206.82/30.72 % (246411)Time elapsed: 0.143 s % 206.82/30.72 % (246411)Peak memory usage: 90 MB % 206.82/30.72 % (246411)Instructions burned: 278 (million) % 206.82/30.72 % (246412)Instruction limit reached! % 206.82/30.72 % (246412)------------------------------ % 206.82/30.72 % (246412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.82/30.72 % (246412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.82/30.72 % (246412)CaDiCaL version: 2.1.3 % 206.82/30.72 % (246412)Termination reason: Instruction limit % 206.82/30.72 % (246412)Termination phase: Saturation % 206.82/30.72 % (246412)Time elapsed: 0.145 s % 206.82/30.72 % (246412)Peak memory usage: 91 MB % 206.82/30.72 % (246412)Instructions burned: 259 (million) % 206.82/30.72 % (246415)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=1202664589:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2721 on theBenchmark for (2721ds/570Mi) % 206.82/30.72 % (246416)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=4220933232:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2719 on theBenchmark for (2719ds/314Mi) % 206.82/30.72 % (246415)Instruction limit reached! % 212.79/31.66 % (246415)------------------------------ % 212.79/31.66 % (246415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.79/31.66 % (246415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.79/31.66 % (246415)CaDiCaL version: 2.1.3 % 212.79/31.66 % (246415)Termination reason: Instruction limit % 212.79/31.66 % (246415)Termination phase: Saturation % 212.79/31.66 % (246415)Time elapsed: 0.173 s % 212.79/31.66 % (246415)Peak memory usage: 94 MB % 212.79/31.66 % (246415)Instructions burned: 572 (million) % 212.79/31.66 % (246416)Instruction limit reached! % 212.79/31.66 % (246416)------------------------------ % 212.79/31.66 % (246416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.79/31.66 % (246416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.79/31.66 % (246416)CaDiCaL version: 2.1.3 % 212.79/31.66 % (246416)Termination reason: Instruction limit % 212.79/31.66 % (246416)Termination phase: Saturation % 212.79/31.66 % (246416)Time elapsed: 0.152 s % 212.79/31.66 % (246416)Peak memory usage: 92 MB % 212.79/31.66 % (246416)Instructions burned: 314 (million) % 212.79/31.66 % (246419)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=257663035:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2717 on theBenchmark for (2717ds/650Mi) % 212.79/31.66 % (246420)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=409706654:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2716 on theBenchmark for (2716ds/496Mi) % 212.79/31.66 % (246419)Instruction limit reached! % 212.79/31.66 % (246419)------------------------------ % 212.79/31.66 % (246419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.79/31.66 % (246419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.79/31.66 % (246419)CaDiCaL version: 2.1.3 % 212.79/31.66 % (246419)Termination reason: Instruction limit % 212.79/31.66 % (246419)Termination phase: Saturation % 212.79/31.66 % (246419)Time elapsed: 0.188 s % 212.79/31.66 % (246419)Peak memory usage: 94 MB % 212.79/31.66 % (246419)Instructions burned: 654 (million) % 212.79/31.66 % (246424)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=1212228205:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2714 on theBenchmark for (2714ds/588Mi) % 212.79/31.66 % (246424)Refutation not found, incomplete strategy % 212.79/31.66 % (246424)------------------------------ % 212.79/31.66 % (246424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.79/31.66 % (246424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.79/31.66 % (246424)CaDiCaL version: 2.1.3 % 212.79/31.66 % (246424)Termination reason: Refutation not found, incomplete strategy % 212.79/31.66 % (246424)Time elapsed: 0.006 s % 212.79/31.66 % (246424)Peak memory usage: 88 MB % 212.79/31.66 % (246424)Instructions burned: 9 (million) % 212.79/31.66 % (246420)Instruction limit reached! % 212.79/31.66 % (246420)------------------------------ % 212.79/31.66 % (246420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.79/31.66 % (246420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.79/31.66 % (246420)CaDiCaL version: 2.1.3 % 212.79/31.66 % (246420)Termination reason: Instruction limit % 212.79/31.66 % (246420)Termination phase: Saturation % 212.79/31.66 % (246420)Time elapsed: 0.245 s % 212.79/31.66 % (246420)Peak memory usage: 94 MB % 212.79/31.66 % (246420)Instructions burned: 496 (million) % 212.79/31.66 % (246424)------------------------------ % 212.79/31.66 % (246424)------------------------------ % 212.79/31.66 % (246476)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=742231396:i=4700:rtra=on_2712 on theBenchmark for (2712ds/4700Mi) % 212.79/31.66 % (246516)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2460244737:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2711 on theBenchmark for (2711ds/226Mi) % 212.79/31.66 % (246516)Instruction limit reached! % 212.79/31.66 % (246516)------------------------------ % 212.79/31.66 % (246516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.79/31.66 % (246516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.79/31.66 % (246516)CaDiCaL version: 2.1.3 % 212.79/31.66 % (246516)Termination reason: Instruction limit % 212.79/31.66 % (246516)Termination phase: Saturation % 212.79/31.66 % (246516)Time elapsed: 0.072 s % 212.79/31.66 % (246516)Peak memory usage: 90 MB % 212.79/31.66 % (246516)Instructions burned: 226 (million) % 212.79/31.66 % (246591)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1097845578:i=254:av=off:fsr=off:rtra=on:sup=off_2709 on theBenchmark for (2709ds/254Mi) % 218.81/32.54 % (246591)Instruction limit reached! % 218.81/32.54 % (246591)------------------------------ % 218.81/32.54 % (246591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.81/32.54 % (246591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.81/32.54 % (246591)CaDiCaL version: 2.1.3 % 218.81/32.54 % (246591)Termination reason: Instruction limit % 218.81/32.54 % (246591)Termination phase: Saturation % 218.81/32.54 % (246591)Time elapsed: 0.065 s % 218.81/32.54 % (246591)Peak memory usage: 89 MB % 218.81/32.54 % (246591)Instructions burned: 257 (million) % 218.81/32.54 % Exception at run slice level % 218.81/32.54 User error: GNN currently only supports monomorphic FOL. % 218.81/32.54 % (246638)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=2315375696:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2707 on theBenchmark for (2707ds/228Mi) % 218.81/32.54 % (246639)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=1420254852:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2707 on theBenchmark for (2707ds/1814Mi) % 218.81/32.54 % (246638)Instruction limit reached! % 218.81/32.54 % (246638)------------------------------ % 218.81/32.54 % (246638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.81/32.54 % (246638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.81/32.54 % (246638)CaDiCaL version: 2.1.3 % 218.81/32.54 % (246638)Termination reason: Instruction limit % 218.81/32.54 % (246638)Termination phase: Saturation % 218.81/32.54 % (246638)Time elapsed: 0.063 s % 218.81/32.54 % (246638)Peak memory usage: 89 MB % 218.81/32.54 % (246638)Instructions burned: 228 (million) % 218.81/32.54 % (246364)Instruction limit reached! % 218.81/32.54 % (246364)------------------------------ % 218.81/32.54 % (246364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.81/32.54 % (246364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.81/32.54 % (246364)CaDiCaL version: 2.1.3 % 218.81/32.54 % (246364)Termination reason: Instruction limit % 218.81/32.54 % (246364)Termination phase: Saturation % 218.81/32.54 % (246364)Time elapsed: 10.364 s % 218.81/32.54 % (246364)Peak memory usage: 228 MB % 218.81/32.54 % (246364)Instructions burned: 21161 (million) % 218.81/32.54 % (246688)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=284998656:i=874:sd=1:aac=none:rtra=on:ss=included_2705 on theBenchmark for (2705ds/874Mi) % 218.81/32.54 % (246688)Refutation not found, incomplete strategy % 218.81/32.54 % (246688)------------------------------ % 218.81/32.54 % (246688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.81/32.54 % (246688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.81/32.54 % (246688)CaDiCaL version: 2.1.3 % 218.81/32.54 % (246688)Termination reason: Refutation not found, incomplete strategy % 218.81/32.54 % (246688)Time elapsed: 0.003 s % 218.81/32.54 % (246688)Peak memory usage: 88 MB % 218.81/32.54 % (246688)Instructions burned: 10 (million) % 218.81/32.54 % (246710)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=3598705968:i=10404:rtra=on:ss=axioms:sgt=16_2705 on theBenchmark for (2705ds/10404Mi) % 218.81/32.54 % (246688)------------------------------ % 218.81/32.54 % (246688)------------------------------ % 218.81/32.54 % (246795)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1158174882:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2703 on theBenchmark for (2703ds/268Mi) % 218.81/32.54 % (246795)Instruction limit reached! % 218.81/32.54 % (246795)------------------------------ % 218.81/32.54 % (246795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.81/32.54 % (246795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.81/32.54 % (246795)CaDiCaL version: 2.1.3 % 218.81/32.54 % (246795)Termination reason: Instruction limit % 218.81/32.54 % (246795)Termination phase: Saturation % 218.81/32.54 % (246795)Time elapsed: 0.071 s % 218.81/32.54 % (246795)Peak memory usage: 91 MB % 218.81/32.54 % (246795)Instructions burned: 269 (million) % 218.81/32.54 % Exception at run slice level % 218.81/32.54 User error: GNN currently only supports monomorphic FOL. % 218.81/32.54 % (246800)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=3380429803:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2700 on theBenchmark for (2700ds/1184Mi) % 218.81/32.54 % (246800)Refutation not found, incomplete strategy % 218.81/32.54 % (246800)------------------------------ % 218.81/32.54 % (246800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.77/34.87 % (246800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.77/34.87 % (246800)CaDiCaL version: 2.1.3 % 235.77/34.87 % (246800)Termination reason: Refutation not found, incomplete strategy % 235.77/34.87 % (246800)Time elapsed: 0.003 s % 235.77/34.87 % (246800)Peak memory usage: 88 MB % 235.77/34.87 % (246800)Instructions burned: 10 (million) % 235.77/34.87 % (246801)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=3153126032:st=3:i=26386:sd=3:rtra=on:ss=axioms_2700 on theBenchmark for (2700ds/26386Mi) % 235.77/34.87 % (246800)------------------------------ % 235.77/34.87 % (246800)------------------------------ % 235.77/34.87 % (246804)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=2157583050:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2698 on theBenchmark for (2698ds/250Mi) % 235.77/34.87 % (246804)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 235.77/34.87 % (246804)Instruction limit reached! % 235.77/34.87 % (246804)------------------------------ % 235.77/34.87 % (246804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.77/34.87 % (246804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.77/34.87 % (246804)CaDiCaL version: 2.1.3 % 235.77/34.87 % (246804)Termination reason: Instruction limit % 235.77/34.87 % (246804)Termination phase: Saturation % 235.77/34.87 % (246804)Time elapsed: 0.071 s % 235.77/34.87 % (246804)Peak memory usage: 92 MB % 235.77/34.87 % (246804)Instructions burned: 254 (million) % 235.77/34.87 % (246639)Instruction limit reached! % 235.77/34.87 % (246639)------------------------------ % 235.77/34.87 % (246639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.77/34.87 % (246639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.77/34.87 % (246639)CaDiCaL version: 2.1.3 % 235.77/34.87 % (246639)Termination reason: Instruction limit % 235.77/34.87 % (246639)Termination phase: Saturation % 235.77/34.87 % (246639)Time elapsed: 1.036 s % 235.77/34.87 % (246639)Peak memory usage: 107 MB % 235.77/34.87 % (246639)Instructions burned: 1816 (million) % 235.77/34.87 % Exception at run slice level % 235.77/34.87 User error: GNN currently only supports monomorphic FOL. % 235.77/34.87 % (246806)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=3190647814:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2696 on theBenchmark for (2696ds/268Mi) % 235.77/34.87 % Exception at run slice level % 235.77/34.87 User error: Immediate (shared) subterms of term/literal amap_fm(X1,X0,X2,neg(X1,X3)) = sF13(X1,X0,X2,X3) have different types/not well-typed! % 235.77/34.87 % (246807)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2743515001:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2695 on theBenchmark for (2695ds/282Mi) % 235.77/34.87 % (246807)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 235.77/34.87 % (246807)Refutation not found, incomplete strategy % 235.77/34.87 % (246807)------------------------------ % 235.77/34.87 % (246807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.77/34.87 % (246807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.77/34.87 % (246807)CaDiCaL version: 2.1.3 % 235.77/34.87 % (246807)Termination reason: Refutation not found, incomplete strategy % 235.77/34.87 % (246807)Time elapsed: 0.002 s % 235.77/34.87 % (246807)Peak memory usage: 88 MB % 235.77/34.87 % (246807)Instructions burned: 1 (million) % 235.77/34.87 % (246810)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=717067342:i=12120:aac=none:ins=25:rtra=on_2694 on theBenchmark for (2694ds/12120Mi) % 235.77/34.87 % (246808)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=3402663286:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2694 on theBenchmark for (2694ds/862Mi) % 235.77/34.87 % Exception at run slice level % 235.77/34.87 User error: GNN currently only supports monomorphic FOL. % 235.77/34.87 % (246807)------------------------------ % 235.77/34.87 % (246807)------------------------------ % 235.77/34.87 % (246815)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=1492672859:i=28310:bd=all:rtra=on_2691 on theBenchmark for (2691ds/28310Mi) % 235.77/34.87 % (246814)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=601369016:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2691 on theBenchmark for (2691ds/300Mi) % 249.48/36.71 % (246814)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 249.48/36.71 % (246814)Instruction limit reached! % 249.48/36.71 % (246814)------------------------------ % 249.48/36.71 % (246814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 249.48/36.71 % (246814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.48/36.71 % (246814)CaDiCaL version: 2.1.3 % 249.48/36.71 % (246814)Termination reason: Instruction limit % 249.48/36.71 % (246814)Termination phase: Saturation % 249.48/36.71 % (246814)Time elapsed: 0.099 s % 249.48/36.71 % (246814)Peak memory usage: 92 MB % 249.48/36.71 % (246814)Instructions burned: 303 (million) % 249.48/36.71 % (246808)Instruction limit reached! % 249.48/36.71 % (246808)------------------------------ % 249.48/36.71 % (246808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 249.48/36.71 % (246808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.48/36.71 % (246808)CaDiCaL version: 2.1.3 % 249.48/36.71 % (246808)Termination reason: Instruction limit % 249.48/36.71 % (246808)Termination phase: Saturation % 249.48/36.71 % (246808)Time elapsed: 0.431 s % 249.48/36.71 % (246808)Peak memory usage: 91 MB % 249.48/36.71 % (246808)Instructions burned: 862 (million) % 249.48/36.71 % (246818)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2086252928:i=1334:av=off:fsr=off:rtra=on_2689 on theBenchmark for (2689ds/1334Mi) % 249.48/36.71 % (246818)Refutation not found, incomplete strategy % 249.48/36.71 % (246818)------------------------------ % 249.48/36.71 % (246818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 249.48/36.71 % (246818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.48/36.71 % (246818)CaDiCaL version: 2.1.3 % 249.48/36.71 % (246818)Termination reason: Refutation not found, incomplete strategy % 249.48/36.71 % (246818)Time elapsed: 0.003 s % 249.48/36.71 % (246818)Peak memory usage: 88 MB % 249.48/36.71 % (246818)Instructions burned: 8 (million) % 249.48/36.71 % (246819)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=2561835437:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2689 on theBenchmark for (2689ds/370Mi) % 249.48/36.71 % Exception at run slice level % 249.48/36.71 User error: GNN currently only supports monomorphic FOL. % 249.48/36.71 % (246818)------------------------------ % 249.48/36.71 % (246818)------------------------------ % 249.48/36.71 % (246819)Instruction limit reached! % 249.48/36.71 % (246819)------------------------------ % 249.48/36.71 % (246819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 249.48/36.71 % (246819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.48/36.71 % (246819)CaDiCaL version: 2.1.3 % 249.48/36.71 % (246819)Termination reason: Instruction limit % 249.48/36.71 % (246819)Termination phase: Saturation % 249.48/36.71 % (246819)Time elapsed: 0.186 s % 249.48/36.71 % (246819)Peak memory usage: 92 MB % 249.48/36.71 % (246819)Instructions burned: 372 (million) % 249.48/36.71 % (246822)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=1522773325:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2686 on theBenchmark for (2686ds/386Mi) % 249.48/36.71 % (246823)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=1492508533:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2686 on theBenchmark for (2686ds/9700Mi) % 249.48/36.71 % (246824)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=3167712463:i=24222:sd=1:rtra=on:ss=included_2685 on theBenchmark for (2685ds/24222Mi) % 249.48/36.71 % (246822)Instruction limit reached! % 249.48/36.71 % (246822)------------------------------ % 249.48/36.71 % (246822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 249.48/36.71 % (246822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.48/36.71 % (246822)CaDiCaL version: 2.1.3 % 249.48/36.71 % (246822)Termination reason: Instruction limit % 249.48/36.71 % (246822)Termination phase: Saturation % 249.48/36.71 % (246822)Time elapsed: 0.209 s % 249.48/36.71 % (246822)Peak memory usage: 93 MB % 249.48/36.71 % (246822)Instructions burned: 387 (million) % 249.48/36.71 % (246828)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=728327243:i=638:kws=precedence:fsr=off:rtra=on_2683 on theBenchmark for (2683ds/638Mi) % 260.05/38.29 % Exception at run slice level % 260.05/38.29 User error: GNN currently only supports monomorphic FOL. % 260.05/38.29 % (246830)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=589889331:i=4128:ep=RST:rtra=on_2680 on theBenchmark for (2680ds/4128Mi) % 260.05/38.29 % (246830)Refutation not found, incomplete strategy % 260.05/38.29 % (246830)------------------------------ % 260.05/38.29 % (246830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.05/38.29 % (246830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.05/38.29 % (246830)CaDiCaL version: 2.1.3 % 260.05/38.29 % (246830)Termination reason: Refutation not found, incomplete strategy % 260.05/38.29 % (246830)Time elapsed: 0.006 s % 260.05/38.29 % (246830)Peak memory usage: 88 MB % 260.05/38.29 % (246830)Instructions burned: 10 (million) % 260.05/38.29 % (246828)Instruction limit reached! % 260.05/38.29 % (246828)------------------------------ % 260.05/38.29 % (246828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.05/38.29 % (246828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.05/38.29 % (246828)CaDiCaL version: 2.1.3 % 260.05/38.29 % (246828)Termination reason: Instruction limit % 260.05/38.29 % (246828)Termination phase: Saturation % 260.05/38.29 % (246828)Time elapsed: 0.309 s % 260.05/38.29 % (246828)Peak memory usage: 93 MB % 260.05/38.29 % (246828)Instructions burned: 639 (million) % 260.05/38.29 % (246832)dis-1011_128_sil=32000:si=on:random_seed=135407589:i=7412:ep=RST:av=off:rtra=on_2678 on theBenchmark for (2678ds/7412Mi) % 260.05/38.29 % (246830)------------------------------ % 260.05/38.29 % (246830)------------------------------ % 260.05/38.29 % (246834)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2875531130:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2676 on theBenchmark for (2676ds/1514Mi) % 260.05/38.29 % (246834)Refutation not found, incomplete strategy % 260.05/38.29 % (246834)------------------------------ % 260.05/38.29 % (246834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.05/38.29 % (246834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.05/38.29 % (246834)CaDiCaL version: 2.1.3 % 260.05/38.29 % (246834)Termination reason: Refutation not found, incomplete strategy % 260.05/38.29 % (246834)Time elapsed: 0.006 s % 260.05/38.29 % (246834)Peak memory usage: 89 MB % 260.05/38.29 % (246834)Instructions burned: 8 (million) % 260.05/38.29 % (246834)------------------------------ % 260.05/38.29 % (246834)------------------------------ % 260.05/38.29 % (246836)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=1797892870:i=27826:rtra=on:ss=axioms:sgt=8_2671 on theBenchmark for (2671ds/27826Mi) % 260.05/38.29 % Exception at run slice level % 260.05/38.29 User error: GNN currently only supports monomorphic FOL. % 260.05/38.29 % (246838)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=232825403:i=19850:aac=none:rtra=on_2666 on theBenchmark for (2666ds/19850Mi) % 260.05/38.29 % Exception at run slice level % 260.05/38.29 User error: GNN currently only supports monomorphic FOL. % 260.05/38.29 % (246840)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=476161944:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2661 on theBenchmark for (2661ds/4958Mi) % 260.05/38.29 % (246840)Refutation not found, incomplete strategy % 260.05/38.29 % (246840)------------------------------ % 260.05/38.29 % (246840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.05/38.29 % (246840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.05/38.29 % (246840)CaDiCaL version: 2.1.3 % 260.05/38.29 % (246840)Termination reason: Refutation not found, incomplete strategy % 260.05/38.29 % (246840)Time elapsed: 0.005 s % 260.05/38.29 % (246840)Peak memory usage: 89 MB % 260.05/38.29 % (246840)Instructions burned: 6 (million) % 260.05/38.29 % (246823)Instruction limit reached! % 260.05/38.29 % (246823)------------------------------ % 260.05/38.29 % (246823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.05/38.29 % (246823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.05/38.29 % (246823)CaDiCaL version: 2.1.3 % 260.05/38.29 % (246823)Termination reason: Instruction limit % 260.05/38.29 % (246823)Termination phase: Saturation % 260.05/38.29 % (246823)Time elapsed: 2.672 s % 274.97/40.30 % (246823)Peak memory usage: 126 MB % 274.97/40.30 % (246823)Instructions burned: 9704 (million) % 274.97/40.30 % (246840)------------------------------ % 274.97/40.30 % (246840)------------------------------ % 274.97/40.30 % (246842)ott+1002_64_sil=16000:si=on:sp=const_min:nwc=0.5:random_seed=2493668167:i=880:nm=2:av=off:rtra=on:gtg=exists_all:fdi=8:gsp=on_2658 on theBenchmark for (2658ds/880Mi) % 274.97/40.30 % (246842)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 274.97/40.30 % (246843)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=1850173996:st=1.5:i=22290:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2656 on theBenchmark for (2656ds/22290Mi) % 274.97/40.30 % (246842)Instruction limit reached! % 274.97/40.30 % (246842)------------------------------ % 274.97/40.30 % (246842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.97/40.30 % (246842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.97/40.30 % (246842)CaDiCaL version: 2.1.3 % 274.97/40.30 % (246842)Termination reason: Instruction limit % 274.97/40.30 % (246842)Termination phase: Saturation % 274.97/40.30 % (246842)Time elapsed: 0.216 s % 274.97/40.30 % (246842)Peak memory usage: 96 MB % 274.97/40.30 % (246842)Instructions burned: 881 (million) % 274.97/40.30 % (246846)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=2761435971:cts=off:i=6068:av=off:rtra=on:er=known:fsd=on_2654 on theBenchmark for (2654ds/6068Mi) % 274.97/40.30 % (245863)Instruction limit reached! % 274.97/40.30 % (245863)------------------------------ % 274.97/40.30 % (245863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.97/40.30 % (245863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.97/40.30 % (245863)CaDiCaL version: 2.1.3 % 274.97/40.30 % (245863)Termination reason: Instruction limit % 274.97/40.30 % (245863)Termination phase: Saturation % 274.97/40.30 % (245863)Time elapsed: 23.740 s % 274.97/40.30 % (245863)Peak memory usage: 477 MB % 274.97/40.30 % (245863)Instructions burned: 43698 (million) % 274.97/40.30 % Exception at run slice level % 274.97/40.30 User error: GNN currently only supports monomorphic FOL. % 274.97/40.30 % Exception at run slice level % 274.97/40.30 User error: GNN currently only supports monomorphic FOL. % 274.97/40.30 % (246848)lrs-1011_64:1_sil=8000:si=on:erd=off:urr=on:nwc=0.7:br=off:random_seed=3146328867:st=2:s2a=on:i=1048:s2at=2:rtra=on:ss=axioms_2651 on theBenchmark for (2651ds/1048Mi) % 274.97/40.30 % (246850)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:si=on:s2agt=16:random_seed=770961821:i=28246:bd=preordered:ins=4:rtra=on_2651 on theBenchmark for (2651ds/28246Mi) % 274.97/40.30 % (246849)lrs+1011_16:1_sil=8000:si=on:acc=on:urr=on:fd=preordered:flr=on:random_seed=3540194267:avsq=on:i=2032:avsqr=676809,524288:sd=1:rtra=on:ss=axioms_2651 on theBenchmark for (2651ds/2032Mi) % 274.97/40.30 % Exception at run slice level % 274.97/40.30 User error: GNN currently only supports monomorphic FOL. % 274.97/40.30 % (246854)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:si=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=556080355:i=11562:kws=precedence:bd=all:rtra=on:rawr=on_2648 on theBenchmark for (2648ds/11562Mi) % 274.97/40.30 % (246848)Instruction limit reached! % 274.97/40.30 % (246848)------------------------------ % 274.97/40.30 % (246848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.97/40.30 % (246848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.97/40.30 % (246848)CaDiCaL version: 2.1.3 % 274.97/40.30 % (246848)Termination reason: Instruction limit % 274.97/40.30 % (246848)Termination phase: Saturation % 274.97/40.30 % (246848)Time elapsed: 0.510 s % 274.97/40.30 % (246848)Peak memory usage: 94 MB % 274.97/40.30 % (246848)Instructions burned: 1049 (million) % 274.97/40.30 % (246856)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=1638876164:i=4896:gtgl=5:bd=preordered:rtra=on:gtg=all_2645 on theBenchmark for (2645ds/4896Mi) % 274.97/40.30 % Exception at run slice level % 274.97/40.30 User error: GNN currently only supports monomorphic FOL. % 274.97/40.30 % (246849)Instruction limit reached! % 274.97/40.30 % (246849)------------------------------ % 274.97/40.30 % (246849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.97/40.30 % (246849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.17/43.19 % (246849)CaDiCaL version: 2.1.3 % 295.17/43.19 % (246849)Termination reason: Instruction limit % 295.17/43.19 % (246849)Termination phase: Saturation % 295.17/43.19 % (246849)Time elapsed: 1.059 s % 295.17/43.19 % (246849)Peak memory usage: 118 MB % 295.17/43.19 % (246849)Instructions burned: 2032 (million) % 295.17/43.19 % (246858)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:si=on:lcm=reverse:random_seed=2850033083:i=6446:kws=precedence:fgj=on:av=off:rtra=on_2640 on theBenchmark for (2640ds/6446Mi) % 295.17/43.19 % (246859)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:si=on:sp=occurrence:sos=on:random_seed=2865476862:st=5.6:i=4066:sd=3:rtra=on:ss=axioms_2639 on theBenchmark for (2639ds/4066Mi) % 295.17/43.19 % Exception at run slice level % 295.17/43.19 User error: GNN currently only supports monomorphic FOL. % 295.17/43.19 % Exception at run slice level % 295.17/43.19 User error: GNN currently only supports monomorphic FOL. % 295.17/43.19 % (246862)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:si=on:random_seed=1912399883:i=4110:nm=16:rtra=on:gtg=position:ss=axioms:fsd=on_2635 on theBenchmark for (2635ds/4110Mi) % 295.17/43.19 % (246373)Instruction limit reached! % 295.17/43.19 % (246373)------------------------------ % 295.17/43.19 % (246373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.17/43.19 % (246373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.17/43.19 % (246373)CaDiCaL version: 2.1.3 % 295.17/43.19 % (246373)Termination reason: Instruction limit % 295.17/43.19 % (246373)Termination phase: Saturation % 295.17/43.19 % (246373)Time elapsed: 14.063 s % 295.17/43.19 % (246373)Peak memory usage: 262 MB % 295.17/43.19 % (246373)Instructions burned: 28959 (million) % 295.17/43.19 % (246832)Instruction limit reached! % 295.17/43.19 % (246832)------------------------------ % 295.17/43.19 % (246832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.17/43.19 % (246832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.17/43.19 % (246832)CaDiCaL version: 2.1.3 % 295.17/43.19 % (246832)Termination reason: Instruction limit % 295.17/43.19 % (246832)Termination phase: Saturation % 295.17/43.19 % (246832)Time elapsed: 4.346 s % 295.17/43.19 % (246832)Peak memory usage: 104 MB % 295.17/43.19 % (246832)Instructions burned: 7412 (million) % 295.17/43.19 % (246863)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=3325480562:i=43222:sd=3:rtra=on:ss=axioms_2634 on theBenchmark for (2634ds/43222Mi) % 295.17/43.19 % (246865)lrs+10_1_sil=8000:si=on:sp=occurrence:sos=all:lma=off:random_seed=2974808046:i=9670:sd=13:rtra=on:ss=axioms:sgt=23_2633 on theBenchmark for (2633ds/9670Mi) % 295.17/43.19 % (246866)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=2216763807:st=5:i=1594:s2at=3:sd=4:bs=unit_only:av=off:rtra=on:sup=off:ss=included_2633 on theBenchmark for (2633ds/1594Mi) % 295.17/43.19 % Exception at run slice level % 295.17/43.19 User error: GNN currently only supports monomorphic FOL. % 295.17/43.19 % Exception at run slice level % 295.17/43.19 User error: GNN currently only supports monomorphic FOL. % 295.17/43.19 % (246870)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=2185883676:i=4652:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:rtra=on:fsd=on_2629 on theBenchmark for (2629ds/4652Mi) % 295.17/43.19 % (246870)Refutation not found, incomplete strategy % 295.17/43.19 % (246870)------------------------------ % 295.17/43.19 % (246870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.17/43.19 % (246870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.17/43.19 % (246870)CaDiCaL version: 2.1.3 % 295.17/43.19 % (246870)Termination reason: Refutation not found, incomplete strategy % 295.17/43.19 % (246870)Time elapsed: 0.007 s % 295.17/43.19 % (246870)Peak memory usage: 89 MB % 295.17/43.19 % (246870)Instructions burned: 11 (million) % 295.17/43.19 % (246871)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:si=on:sos=all:urr=on:br=off:random_seed=3565865935:i=12076:nm=6:rtra=on_2629 on theBenchmark for (2629ds/12076Mi) % 295.17/43.19 % (246870)------------------------------ % 295.17/43.19 % (246870)------------------------------ % 295.17/43.19 % (246874)lrs+10_1_sil=32000:si=on:sp=occurrence:random_seed=3431537675:st=2:i=66668:sd=3:rtra=on:ss=included:sgt=32_2625 on theBenchmark for (2625ds/66668Mi) % 295.17/43.19 % Exception at run slice levTerminated %------------------------------------------------------------------------------