%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : LCL751_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 11:56:27 AM UTC 2026 % Result : Timeout 287.22s 41.46s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : LCL751_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.04/0.30 % Computer : n012.cluster.edu % 0.04/0.30 % Model : x86_64 x86_64 % 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.04/0.30 % Memory : 8046.5625MB % 0.04/0.30 % OS : Linux 6.8.0-71-generic % 0.04/0.30 % CPULimit : 300 % 0.04/0.30 % WCLimit : 300 % 0.04/0.30 % DateTime : Sun Sep 27 16:43:34 UTC 2026 % 0.04/0.30 % CPUTime : % 0.04/0.30 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.04/0.32 Running first-order theorem proving % 0.04/0.32 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 % 4.63/1.20 % (2582546)Detected formulas, will run a generic FOF schedule. % 4.63/1.20 % (2582557)dis-21_1_sil=8000:lcm=predicate:random_seed=2312901809:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 4.63/1.20 % (2582552)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=2689326519:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 4.63/1.20 % (2582555)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2851467397:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 4.63/1.20 % (2582551)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=1052542143:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 4.63/1.20 % (2582554)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1488481852:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 4.63/1.20 % (2582553)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=230855095:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 4.63/1.20 % (2582556)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=510657135:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 4.63/1.20 % (2582554)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 4.63/1.20 % (2582553)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 4.63/1.20 % (2582554)Refutation not found, incomplete strategy % 4.63/1.20 % (2582554)------------------------------ % 4.63/1.20 % (2582554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.63/1.20 % (2582554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.63/1.20 % (2582554)CaDiCaL version: 2.1.3 % 4.63/1.20 % (2582554)Termination reason: Refutation not found, incomplete strategy % 4.63/1.20 % (2582554)Time elapsed: 0.005 s % 4.63/1.20 % (2582554)Peak memory usage: 89 MB % 4.63/1.20 % (2582554)Instructions burned: 16 (million) % 4.63/1.20 % (2582557)Instruction limit reached! % 4.63/1.20 % (2582557)------------------------------ % 4.63/1.20 % (2582557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.63/1.20 % (2582557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.63/1.20 % (2582557)CaDiCaL version: 2.1.3 % 4.63/1.20 % (2582557)Termination reason: Instruction limit % 4.63/1.20 % (2582557)Termination phase: Saturation % 4.63/1.20 % (2582557)Time elapsed: 0.034 s % 4.63/1.20 % (2582557)Peak memory usage: 90 MB % 4.63/1.20 % (2582557)Instructions burned: 131 (million) % 4.63/1.20 % (2582555)Instruction limit reached! % 4.63/1.20 % (2582555)------------------------------ % 4.63/1.20 % (2582555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.63/1.20 % (2582555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.63/1.20 % (2582555)CaDiCaL version: 2.1.3 % 4.63/1.20 % (2582555)Termination reason: Instruction limit % 4.63/1.20 % (2582555)Termination phase: Saturation % 4.63/1.20 % (2582555)Time elapsed: 0.039 s % 4.63/1.20 % (2582555)Peak memory usage: 88 MB % 4.63/1.20 % (2582555)Instructions burned: 122 (million) % 4.63/1.20 % (2582556)Instruction limit reached! % 4.63/1.20 % (2582556)------------------------------ % 4.63/1.20 % (2582556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.63/1.20 % (2582556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.63/1.20 % (2582556)CaDiCaL version: 2.1.3 % 4.63/1.20 % (2582556)Termination reason: Instruction limit % 4.63/1.20 % (2582556)Termination phase: Saturation % 4.63/1.20 % (2582556)Time elapsed: 0.059 s % 4.63/1.20 % (2582556)Peak memory usage: 89 MB % 4.63/1.20 % (2582556)Instructions burned: 140 (million) % 4.63/1.20 % (2582565)lrs+10_1_sil=8000:sp=occurrence:random_seed=1925458296:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi) % 4.63/1.20 % (2582566)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3265036526:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi) % 4.63/1.20 % (2582567)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1724329507:i=325:sd=1:ss=axioms:sgt=32_2998 on theBenchmark for (2998ds/325Mi) % 4.63/1.20 % (2582554)------------------------------ % 5.60/1.40 % (2582554)------------------------------ % 5.60/1.40 % (2582566)Instruction limit reached! % 5.60/1.40 % (2582566)------------------------------ % 5.60/1.40 % (2582566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.60/1.40 % (2582566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.40 % (2582566)CaDiCaL version: 2.1.3 % 5.60/1.40 % (2582566)Termination reason: Instruction limit % 5.60/1.40 % (2582566)Termination phase: Saturation % 5.60/1.40 % (2582566)Time elapsed: 0.050 s % 5.60/1.40 % (2582566)Peak memory usage: 90 MB % 5.60/1.40 % (2582566)Instructions burned: 159 (million) % 5.60/1.40 % Exception at run slice level % 5.60/1.40 User error: GNN currently only supports monomorphic FOL.% Exception at run slice level % 5.60/1.40 % 5.60/1.40 User error: GNN currently only supports monomorphic FOL. % 5.60/1.40 % Exception at run slice level % 5.60/1.40 User error: GNN currently only supports monomorphic FOL. % 5.60/1.40 % (2582565)Instruction limit reached! % 5.60/1.40 % (2582565)------------------------------ % 5.60/1.40 % (2582565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.60/1.40 % (2582565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.40 % (2582565)CaDiCaL version: 2.1.3 % 5.60/1.40 % (2582565)Termination reason: Instruction limit % 5.60/1.40 % (2582565)Termination phase: Saturation % 5.60/1.40 % (2582565)Time elapsed: 0.091 s % 5.60/1.40 % (2582565)Peak memory usage: 91 MB % 5.60/1.40 % (2582565)Instructions burned: 287 (million) % 5.60/1.40 % (2582571)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=583035115:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 5.60/1.40 % (2582567)Instruction limit reached! % 5.60/1.40 % (2582567)------------------------------ % 5.60/1.40 % (2582567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.60/1.40 % (2582567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.40 % (2582567)CaDiCaL version: 2.1.3 % 5.60/1.40 % (2582567)Termination reason: Instruction limit % 5.60/1.40 % (2582567)Termination phase: Saturation % 5.60/1.40 % (2582567)Time elapsed: 0.111 s % 5.60/1.40 % (2582567)Peak memory usage: 91 MB % 5.60/1.40 % (2582567)Instructions burned: 326 (million) % 5.60/1.40 % (2582572)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1475211761:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi) % 5.60/1.40 % (2582572)Refutation not found, incomplete strategy % 5.60/1.40 % (2582572)------------------------------ % 5.60/1.40 % (2582572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.60/1.40 % (2582572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.40 % (2582572)CaDiCaL version: 2.1.3 % 5.60/1.40 % (2582572)Termination reason: Refutation not found, incomplete strategy % 5.60/1.40 % (2582572)Time elapsed: 0.007 s % 5.60/1.40 % (2582572)Peak memory usage: 89 MB % 5.60/1.40 % (2582572)Instructions burned: 25 (million) % 5.60/1.40 % (2582573)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2691454903:i=2350_2996 on theBenchmark for (2996ds/2350Mi) % 5.60/1.40 % (2582574)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=670779859:cts=off:i=113:fsr=off:ss=included:sgt=4_2996 on theBenchmark for (2996ds/113Mi) % 5.60/1.40 % (2582575)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1440505981:i=127:av=off:fsr=off:sup=off_2996 on theBenchmark for (2996ds/127Mi) % 5.60/1.40 % (2582576)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1231693494:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2996 on theBenchmark for (2996ds/114Mi) % 5.60/1.40 % (2582575)Instruction limit reached! % 5.60/1.40 % (2582575)------------------------------ % 5.60/1.40 % (2582575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.60/1.40 % (2582575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.40 % (2582575)CaDiCaL version: 2.1.3 % 5.60/1.40 % (2582575)Termination reason: Instruction limit % 5.60/1.40 % (2582575)Termination phase: Saturation % 5.60/1.40 % (2582575)Time elapsed: 0.032 s % 5.60/1.40 % (2582575)Peak memory usage: 88 MB % 5.60/1.40 % (2582575)Instructions burned: 128 (million) % 5.60/1.40 % (2582574)Instruction limit reached! % 5.60/1.40 % (2582574)------------------------------ % 5.60/1.40 % (2582574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.12/1.61 % (2582574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.12/1.61 % (2582574)CaDiCaL version: 2.1.3 % 7.12/1.61 % (2582574)Termination reason: Instruction limit % 7.12/1.61 % (2582574)Termination phase: Saturation % 7.12/1.61 % (2582574)Time elapsed: 0.033 s % 7.12/1.61 % (2582574)Peak memory usage: 89 MB % 7.12/1.61 % (2582574)Instructions burned: 116 (million) % 7.12/1.61 % (2582571)Instruction limit reached! % 7.12/1.61 % (2582571)------------------------------ % 7.12/1.61 % (2582571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.12/1.61 % (2582571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.12/1.61 % (2582571)CaDiCaL version: 2.1.3 % 7.12/1.61 % (2582571)Termination reason: Instruction limit % 7.12/1.61 % (2582571)Termination phase: Saturation % 7.12/1.61 % (2582571)Time elapsed: 0.078 s % 7.12/1.61 % (2582571)Peak memory usage: 90 MB % 7.12/1.61 % (2582571)Instructions burned: 250 (million) % 7.12/1.61 % (2582576)Instruction limit reached! % 7.12/1.61 % (2582576)------------------------------ % 7.12/1.61 % (2582576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.12/1.61 % (2582576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.12/1.61 % (2582576)CaDiCaL version: 2.1.3 % 7.12/1.61 % (2582576)Termination reason: Instruction limit % 7.12/1.61 % (2582576)Termination phase: Saturation % 7.12/1.61 % (2582576)Time elapsed: 0.035 s % 7.12/1.61 % (2582576)Peak memory usage: 88 MB % 7.12/1.61 % (2582576)Instructions burned: 114 (million) % 7.12/1.61 % (2582579)lrs+10_1_sil=8000:sp=occurrence:random_seed=519397546:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2996 on theBenchmark for (2996ds/907Mi) % 7.12/1.61 % (2582586)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3163900343:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2995 on theBenchmark for (2995ds/134Mi) % 7.12/1.61 % (2582585)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2971248139:i=5202:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/5202Mi) % 7.12/1.61 % (2582584)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3251196046:i=437:sd=1:aac=none:ss=included_2995 on theBenchmark for (2995ds/437Mi) % 7.12/1.61 % (2582572)------------------------------ % 7.12/1.61 % (2582572)------------------------------ % 7.12/1.61 % (2582584)Refutation not found, incomplete strategy % 7.12/1.61 % (2582584)------------------------------ % 7.12/1.61 % (2582584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.12/1.61 % (2582584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.12/1.61 % (2582584)CaDiCaL version: 2.1.3 % 7.12/1.61 % (2582584)Termination reason: Refutation not found, incomplete strategy % 7.12/1.61 % (2582584)Time elapsed: 0.009 s % 7.12/1.61 % (2582584)Peak memory usage: 89 MB % 7.12/1.61 % (2582584)Instructions burned: 31 (million) % 7.12/1.61 % (2582587)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3279037621:st=8:i=592:sd=3:ep=RST:ss=axioms_2995 on theBenchmark for (2995ds/592Mi) % 7.12/1.61 % (2582587)Refutation not found, incomplete strategy % 7.12/1.61 % (2582587)------------------------------ % 7.12/1.61 % (2582587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.12/1.61 % (2582587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.12/1.61 % (2582587)CaDiCaL version: 2.1.3 % 7.12/1.61 % (2582587)Termination reason: Refutation not found, incomplete strategy % 7.12/1.61 % (2582587)Time elapsed: 0.007 s % 7.12/1.61 % (2582587)Peak memory usage: 89 MB % 7.12/1.61 % (2582587)Instructions burned: 26 (million) % 7.12/1.61 % (2582586)Instruction limit reached! % 7.12/1.61 % (2582586)------------------------------ % 7.12/1.61 % (2582586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.12/1.61 % (2582586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.12/1.61 % (2582586)CaDiCaL version: 2.1.3 % 7.12/1.61 % (2582586)Termination reason: Instruction limit % 7.12/1.61 % (2582586)Termination phase: Saturation % 7.12/1.61 % (2582586)Time elapsed: 0.044 s % 7.12/1.61 % (2582586)Peak memory usage: 90 MB % 7.12/1.61 % (2582586)Instructions burned: 137 (million) % 7.12/1.61 % Exception at run slice level % 7.12/1.61 User error: GNN currently only supports monomorphic FOL. % 7.12/1.61 % (2582592)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3407538553:st=3:i=13193:sd=3:ss=axioms_2994 on theBenchmark for (2994ds/13193Mi) % 7.12/1.61 % (2582594)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=2013915281:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/125Mi) % 8.41/1.97 % (2582594)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 8.41/1.97 % (2582584)------------------------------ % 8.41/1.97 % (2582584)------------------------------ % 8.41/1.97 % (2582587)------------------------------ % 8.41/1.97 % (2582587)------------------------------ % 8.41/1.97 % (2582594)Instruction limit reached! % 8.41/1.97 % (2582594)------------------------------ % 8.41/1.97 % (2582594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.41/1.97 % (2582594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.41/1.97 % (2582594)CaDiCaL version: 2.1.3 % 8.41/1.97 % (2582594)Termination reason: Instruction limit % 8.41/1.97 % (2582594)Termination phase: Saturation % 8.41/1.97 % (2582594)Time elapsed: 0.039 s % 8.41/1.97 % (2582594)Peak memory usage: 91 MB % 8.41/1.97 % (2582594)Instructions burned: 127 (million) % 8.41/1.97 % (2582595)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=514063677:i=134:gtgl=5:slsql=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/134Mi) % 8.41/1.97 % Exception at run slice level % 8.41/1.97 User error: Immediate (shared) subterms of term/literal list_case(X1,X0,X3,X2,nil(X0)) = sF48(X1,X0,X3,X2) have different types/not well-typed! % 8.41/1.97 % Exception at run slice level % 8.41/1.97 User error: GNN currently only supports monomorphic FOL. % 8.41/1.97 % (2582579)Instruction limit reached! % 8.41/1.97 % (2582579)------------------------------ % 8.41/1.97 % (2582579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.41/1.97 % (2582579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.41/1.97 % (2582579)CaDiCaL version: 2.1.3 % 8.41/1.97 % (2582579)Termination reason: Instruction limit % 8.41/1.97 % (2582579)Termination phase: Saturation % 8.41/1.97 % (2582579)Time elapsed: 0.303 s % 8.41/1.97 % (2582579)Peak memory usage: 96 MB % 8.41/1.97 % (2582579)Instructions burned: 907 (million) % 8.41/1.97 % (2582598)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3746048429:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2992 on theBenchmark for (2992ds/141Mi) % 8.41/1.97 % (2582598)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 8.41/1.97 % (2582600)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1433239611:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/431Mi) % 8.41/1.97 % (2582601)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=2013807204:i=6060:aac=none:ins=25_2992 on theBenchmark for (2992ds/6060Mi) % 8.41/1.97 % (2582602)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=177906061:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2992 on theBenchmark for (2992ds/150Mi) % 8.41/1.97 % (2582602)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 8.41/1.97 % (2582598)Instruction limit reached! % 8.41/1.97 % (2582598)------------------------------ % 8.41/1.97 % (2582598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.41/1.97 % (2582598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.41/1.97 % (2582598)CaDiCaL version: 2.1.3 % 8.41/1.97 % (2582598)Termination reason: Instruction limit % 8.41/1.97 % (2582598)Termination phase: Saturation % 8.41/1.97 % (2582598)Time elapsed: 0.035 s % 8.41/1.97 % (2582598)Peak memory usage: 90 MB % 8.41/1.97 % (2582598)Instructions burned: 143 (million) % 8.41/1.97 % Exception at run slice level % 8.41/1.97 User error: GNN currently only supports monomorphic FOL. % 8.41/1.97 % (2582603)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1799141928:i=14155:bd=all_2992 on theBenchmark for (2992ds/14155Mi) % 8.41/1.97 % (2582604)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3936348615:i=667:av=off:fsr=off_2992 on theBenchmark for (2992ds/667Mi) % 8.41/1.97 % (2582602)Instruction limit reached! % 8.41/1.97 % (2582602)------------------------------ % 8.41/1.97 % (2582602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.35/2.71 % (2582602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.35/2.71 % (2582602)CaDiCaL version: 2.1.3 % 14.35/2.71 % (2582602)Termination reason: Instruction limit % 14.35/2.71 % (2582602)Termination phase: Saturation % 14.35/2.71 % (2582602)Time elapsed: 0.055 s % 14.35/2.71 % (2582602)Peak memory usage: 91 MB % 14.35/2.71 % (2582602)Instructions burned: 151 (million) % 14.35/2.71 % (2582600)Instruction limit reached! % 14.35/2.71 % (2582600)------------------------------ % 14.35/2.71 % (2582600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.35/2.71 % (2582600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.35/2.71 % (2582600)CaDiCaL version: 2.1.3 % 14.35/2.71 % (2582600)Termination reason: Instruction limit % 14.35/2.71 % (2582600)Termination phase: Saturation % 14.35/2.71 % (2582600)Time elapsed: 0.107 s % 14.35/2.71 % (2582600)Peak memory usage: 91 MB % 14.35/2.71 % (2582600)Instructions burned: 432 (million) % 14.35/2.71 % (2582609)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=293205133:s2a=on:i=185:s2at=1.8:fdi=4_2991 on theBenchmark for (2991ds/185Mi) % 14.35/2.71 % (2582611)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3348895274:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2991 on theBenchmark for (2991ds/193Mi) % 14.35/2.71 % (2582613)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=514198920:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2991 on theBenchmark for (2991ds/4850Mi) % 14.35/2.71 % (2582609)Instruction limit reached! % 14.35/2.71 % (2582609)------------------------------ % 14.35/2.71 % (2582609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.35/2.71 % (2582609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.35/2.71 % (2582609)CaDiCaL version: 2.1.3 % 14.35/2.71 % (2582609)Termination reason: Instruction limit % 14.35/2.71 % (2582609)Termination phase: Saturation % 14.35/2.71 % (2582609)Time elapsed: 0.057 s % 14.35/2.71 % (2582609)Peak memory usage: 90 MB % 14.35/2.71 % (2582609)Instructions burned: 190 (million) % 14.35/2.71 % (2582611)Instruction limit reached! % 14.35/2.71 % (2582611)------------------------------ % 14.35/2.71 % (2582611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.35/2.71 % (2582611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.35/2.71 % (2582611)CaDiCaL version: 2.1.3 % 14.35/2.71 % (2582611)Termination reason: Instruction limit % 14.35/2.71 % (2582611)Termination phase: Saturation % 14.35/2.71 % (2582611)Time elapsed: 0.065 s % 14.35/2.71 % (2582611)Peak memory usage: 90 MB % 14.35/2.71 % (2582611)Instructions burned: 196 (million) % 14.35/2.71 % (2582614)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1622718908:i=12111:sd=1:ss=included_2990 on theBenchmark for (2990ds/12111Mi) % 14.35/2.71 % Exception at run slice level % 14.35/2.71 User error: GNN currently only supports monomorphic FOL. % 14.35/2.71 % (2582604)Instruction limit reached! % 14.35/2.71 % (2582604)------------------------------ % 14.35/2.71 % (2582604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.35/2.71 % (2582604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.35/2.71 % (2582604)CaDiCaL version: 2.1.3 % 14.35/2.71 % (2582604)Termination reason: Instruction limit % 14.35/2.71 % (2582604)Termination phase: Saturation % 14.35/2.71 % (2582604)Time elapsed: 0.188 s % 14.35/2.71 % (2582604)Peak memory usage: 90 MB % 14.35/2.71 % (2582604)Instructions burned: 669 (million) % 14.35/2.71 % Exception at run slice level % 14.35/2.71 User error: GNN currently only supports monomorphic FOL. % 14.35/2.71 % (2582618)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3614146749:i=319:kws=precedence:fsr=off_2990 on theBenchmark for (2990ds/319Mi) % 14.35/2.71 % (2582620)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1504564208:i=2064:ep=RST_2989 on theBenchmark for (2989ds/2064Mi) % 14.35/2.71 % (2582620)Refutation not found, incomplete strategy % 14.35/2.71 % (2582620)------------------------------ % 14.35/2.71 % (2582620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.35/2.71 % (2582620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.35/2.71 % (2582620)CaDiCaL version: 2.1.3 % 18.96/3.38 % (2582620)Termination reason: Refutation not found, incomplete strategy % 18.96/3.38 % (2582620)Time elapsed: 0.007 s % 18.96/3.38 % (2582620)Peak memory usage: 89 MB % 18.96/3.38 % (2582620)Instructions burned: 25 (million) % 18.96/3.38 % (2582621)dis-1011_128_sil=32000:random_seed=2540004897:i=3706:ep=RST:av=off_2989 on theBenchmark for (2989ds/3706Mi) % 18.96/3.38 % (2582622)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1364583351:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2989 on theBenchmark for (2989ds/757Mi) % 18.96/3.38 % (2582623)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3833112464:i=13913:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/13913Mi) % 18.96/3.38 % (2582622)Refutation not found, incomplete strategy % 18.96/3.38 % (2582622)------------------------------ % 18.96/3.38 % (2582622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.96/3.38 % (2582622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.96/3.38 % (2582622)CaDiCaL version: 2.1.3 % 18.96/3.38 % (2582622)Termination reason: Refutation not found, incomplete strategy % 18.96/3.38 % (2582622)Time elapsed: 0.008 s % 18.96/3.38 % (2582622)Peak memory usage: 89 MB % 18.96/3.38 % (2582622)Instructions burned: 29 (million) % 18.96/3.38 % (2582618)Instruction limit reached! % 18.96/3.38 % (2582618)------------------------------ % 18.96/3.38 % (2582618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.96/3.38 % (2582618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.96/3.38 % (2582618)CaDiCaL version: 2.1.3 % 18.96/3.38 % (2582618)Termination reason: Instruction limit % 18.96/3.38 % (2582618)Termination phase: Saturation % 18.96/3.38 % (2582618)Time elapsed: 0.111 s % 18.96/3.38 % (2582618)Peak memory usage: 92 MB % 18.96/3.38 % (2582618)Instructions burned: 321 (million) % 18.96/3.38 % Exception at run slice level % 18.96/3.38 User error: GNN currently only supports monomorphic FOL. % 18.96/3.38 % (2582620)------------------------------ % 18.96/3.38 % (2582620)------------------------------ % 18.96/3.38 % (2582629)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=843251639:i=9925:aac=none_2988 on theBenchmark for (2988ds/9925Mi) % 18.96/3.38 % (2582630)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3513260075:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2987 on theBenchmark for (2987ds/2479Mi) % 18.96/3.38 % (2582622)------------------------------ % 18.96/3.38 % (2582622)------------------------------ % 18.96/3.38 % (2582630)Refutation not found, incomplete strategy % 18.96/3.38 % (2582630)------------------------------ % 18.96/3.38 % (2582630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.96/3.38 % (2582630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.96/3.38 % (2582630)CaDiCaL version: 2.1.3 % 18.96/3.38 % (2582630)Termination reason: Refutation not found, incomplete strategy % 18.96/3.38 % (2582630)Time elapsed: 0.006 s % 18.96/3.38 % (2582630)Peak memory usage: 89 MB % 18.96/3.38 % (2582630)Instructions burned: 19 (million) % 18.96/3.38 % (2582631)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1339293832:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/440Mi) % 18.96/3.38 % (2582631)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 18.96/3.38 % Exception at run slice level % 18.96/3.38 User error: GNN currently only supports monomorphic FOL. % 18.96/3.38 % (2582634)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3559559045:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2986 on theBenchmark for (2986ds/11145Mi) % 18.96/3.38 % (2582636)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=3876513889:cts=off:i=3034:av=off:er=known:fsd=on_2986 on theBenchmark for (2986ds/3034Mi) % 18.96/3.38 % (2582630)------------------------------ % 18.96/3.38 % (2582630)------------------------------ % 18.96/3.38 % (2582631)Instruction limit reached! % 18.96/3.38 % (2582631)------------------------------ % 18.96/3.38 % (2582631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.96/3.38 % (2582631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.96/3.38 % (2582631)CaDiCaL version: 2.1.3 % 18.96/3.38 % (2582631)Termination reason: Instruction limit % 22.76/3.99 % (2582631)Termination phase: Saturation % 22.76/3.99 % (2582631)Time elapsed: 0.123 s % 22.76/3.99 % (2582631)Peak memory usage: 92 MB % 22.76/3.99 % (2582631)Instructions burned: 442 (million) % 22.76/3.99 % Exception at run slice level % 22.76/3.99 User error: GNN currently only supports monomorphic FOL. % 22.76/3.99 % (2582640)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=926674424:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2985 on theBenchmark for (2985ds/1016Mi) % 22.76/3.99 % (2582639)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3713213370:st=2:s2a=on:i=524:s2at=2:ss=axioms_2985 on theBenchmark for (2985ds/524Mi) % 22.76/3.99 % (2582641)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3942947260:i=14123:bd=preordered:ins=4_2985 on theBenchmark for (2985ds/14123Mi) % 22.76/3.99 % Exception at run slice level % 22.76/3.99 User error: GNN currently only supports monomorphic FOL. % 22.76/3.99 % Exception at run slice level % 22.76/3.99 User error: GNN currently only supports monomorphic FOL. % 22.76/3.99 % (2582645)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=168641275:i=5781:kws=precedence:bd=all:rawr=on_2984 on theBenchmark for (2984ds/5781Mi) % 22.76/3.99 % (2582639)Instruction limit reached! % 22.76/3.99 % (2582639)------------------------------ % 22.76/3.99 % (2582639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.76/3.99 % (2582639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.76/3.99 % (2582639)CaDiCaL version: 2.1.3 % 22.76/3.99 % (2582639)Termination reason: Instruction limit % 22.76/3.99 % (2582639)Termination phase: Saturation % 22.76/3.99 % (2582639)Time elapsed: 0.145 s % 22.76/3.99 % (2582639)Peak memory usage: 91 MB % 22.76/3.99 % (2582639)Instructions burned: 524 (million) % 22.76/3.99 % (2582646)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=2605644658:i=2448:gtgl=5:bd=preordered:gtg=all_2983 on theBenchmark for (2983ds/2448Mi) % 22.76/3.99 % Exception at run slice level % 22.76/3.99 User error: GNN currently only supports monomorphic FOL. % 22.76/3.99 % (2582648)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3792641544:i=3223:kws=precedence:fgj=on:av=off_2982 on theBenchmark for (2982ds/3223Mi) % 22.76/3.99 % (2582640)Instruction limit reached! % 22.76/3.99 % (2582640)------------------------------ % 22.76/3.99 % (2582640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.76/3.99 % (2582640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.76/3.99 % (2582640)CaDiCaL version: 2.1.3 % 22.76/3.99 % (2582640)Termination reason: Instruction limit % 22.76/3.99 % (2582640)Termination phase: Saturation % 22.76/3.99 % (2582640)Time elapsed: 0.313 s % 22.76/3.99 % (2582640)Peak memory usage: 98 MB % 22.76/3.99 % (2582640)Instructions burned: 1017 (million) % 22.76/3.99 % (2582650)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3550545586:st=5.6:i=2033:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/2033Mi) % 22.76/3.99 % Exception at run slice level % 22.76/3.99 User error: GNN currently only supports monomorphic FOL. % 22.76/3.99 % (2582653)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3817893910:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2981 on theBenchmark for (2981ds/2055Mi) % 22.76/3.99 % Exception at run slice level % 22.76/3.99 User error: GNN currently only supports monomorphic FOL. % 22.76/3.99 % (2582654)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=3738101568:i=21611:sd=3:ss=axioms_2980 on theBenchmark for (2980ds/21611Mi) % 22.76/3.99 % Exception at run slice level % 22.76/3.99 User error: GNN currently only supports monomorphic FOL. % 22.76/3.99 % (2582656)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1421009180:i=4835:sd=13:ss=axioms:sgt=23_2979 on theBenchmark for (2979ds/4835Mi) % 22.76/3.99 % Exception at run slice level % 22.76/3.99 User error: GNN currently only supports monomorphic FOL. % 22.76/3.99 % (2582658)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=3921832115:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2979 on theBenchmark for (2979ds/797Mi) % 22.76/3.99 % (2582621)Instruction limit reached! % 28.99/4.75 % (2582621)------------------------------ % 28.99/4.75 % (2582621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.99/4.75 % (2582621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.99/4.75 % (2582621)CaDiCaL version: 2.1.3 % 28.99/4.75 % (2582621)Termination reason: Instruction limit % 28.99/4.75 % (2582621)Termination phase: Saturation % 28.99/4.75 % (2582621)Time elapsed: 1.099 s % 28.99/4.75 % (2582621)Peak memory usage: 117 MB % 28.99/4.75 % (2582621)Instructions burned: 3709 (million) % 28.99/4.75 % (2582660)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1040643974:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2978 on theBenchmark for (2978ds/2326Mi) % 28.99/4.75 % Exception at run slice level % 28.99/4.75 User error: GNN currently only supports monomorphic FOL. % 28.99/4.75 % (2582662)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=239632027:i=6038:nm=6_2977 on theBenchmark for (2977ds/6038Mi) % 28.99/4.75 % (2582664)lrs+10_1_sil=32000:sp=occurrence:random_seed=4291359660:st=2:i=33334:sd=3:ss=included:sgt=32_2977 on theBenchmark for (2977ds/33334Mi) % 28.99/4.75 % (2582658)Instruction limit reached! % 28.99/4.75 % (2582658)------------------------------ % 28.99/4.75 % (2582658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.99/4.75 % (2582658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.99/4.75 % (2582658)CaDiCaL version: 2.1.3 % 28.99/4.75 % (2582658)Termination reason: Instruction limit % 28.99/4.75 % (2582658)Termination phase: Saturation % 28.99/4.75 % (2582658)Time elapsed: 0.240 s % 28.99/4.75 % (2582658)Peak memory usage: 96 MB % 28.99/4.75 % (2582658)Instructions burned: 798 (million) % 28.99/4.75 % (2582613)Instruction limit reached! % 28.99/4.75 % (2582613)------------------------------ % 28.99/4.75 % (2582613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.99/4.75 % (2582613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.99/4.75 % (2582613)CaDiCaL version: 2.1.3 % 28.99/4.75 % (2582613)Termination reason: Instruction limit % 28.99/4.75 % (2582613)Termination phase: Saturation % 28.99/4.75 % (2582613)Time elapsed: 1.432 s % 28.99/4.75 % (2582613)Peak memory usage: 103 MB % 28.99/4.75 % (2582613)Instructions burned: 4853 (million) % 28.99/4.75 % Exception at run slice level % 28.99/4.75 User error: GNN currently only supports monomorphic FOL. % 28.99/4.75 % (2582667)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1263087773:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2975 on theBenchmark for (2975ds/1008Mi) % 28.99/4.75 % (2582668)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=1853402329:i=8327:s2at=5:bd=preordered_2975 on theBenchmark for (2975ds/8327Mi) % 28.99/4.75 % (2582669)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=2669180899:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2975 on theBenchmark for (2975ds/1083Mi) % 28.99/4.75 % Exception at run slice level % 28.99/4.75 User error: GNN currently only supports monomorphic FOL. % 28.99/4.75 % (2582667)Instruction limit reached! % 28.99/4.75 % (2582667)------------------------------ % 28.99/4.75 % (2582667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.99/4.75 % (2582667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.99/4.75 % (2582667)CaDiCaL version: 2.1.3 % 28.99/4.75 % (2582667)Termination reason: Instruction limit % 28.99/4.75 % (2582667)Termination phase: Saturation % 28.99/4.75 % (2582667)Time elapsed: 0.283 s % 28.99/4.75 % (2582667)Peak memory usage: 97 MB % 28.99/4.75 % (2582667)Instructions burned: 1012 (million) % 28.99/4.75 % (2582673)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=742466592:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2972 on theBenchmark for (2972ds/1084Mi) % 28.99/4.75 % (2582669)Instruction limit reached! % 28.99/4.75 % (2582669)------------------------------ % 28.99/4.75 % (2582669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.99/4.75 % (2582669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.99/4.75 % (2582669)CaDiCaL version: 2.1.3 % 28.99/4.75 % (2582669)Termination reason: Instruction limit % 35.63/5.72 % (2582669)Termination phase: Saturation % 35.63/5.72 % (2582669)Time elapsed: 0.287 s % 35.63/5.72 % (2582669)Peak memory usage: 97 MB % 35.63/5.72 % (2582669)Instructions burned: 1084 (million) % 35.63/5.72 % (2582674)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=918842314:i=6995:s2at=5:gtg=all_2972 on theBenchmark for (2972ds/6995Mi) % 35.63/5.72 % Exception at run slice level % 35.63/5.72 User error: Immediate (shared) subterms of term/literal aa(fun(X1,X0),fun(X1,fun(list(X0),list(X0))),sF50(X0,X1),X3) = sF51(X1,X0,X3) have different types/not well-typed! % 35.63/5.72 % (2582660)Instruction limit reached! % 35.63/5.72 % (2582660)------------------------------ % 35.63/5.72 % (2582660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.63/5.72 % (2582660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.63/5.72 % (2582660)CaDiCaL version: 2.1.3 % 35.63/5.72 % (2582660)Termination reason: Instruction limit % 35.63/5.72 % (2582660)Termination phase: Saturation % 35.63/5.72 % (2582660)Time elapsed: 0.696 s % 35.63/5.72 % (2582660)Peak memory usage: 96 MB % 35.63/5.72 % (2582660)Instructions burned: 2327 (million) % 35.63/5.72 % (2582676)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1971448435:st=2:i=6225:sd=15:ss=axioms_2971 on theBenchmark for (2971ds/6225Mi) % 35.63/5.72 % (2582678)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=4023090905:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2971 on theBenchmark for (2971ds/3372Mi) % 35.63/5.72 % (2582679)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1514880780:st=2.3:i=26457:sd=10:ss=included:sgt=8_2970 on theBenchmark for (2970ds/26457Mi) % 35.63/5.72 % (2582673)Instruction limit reached! % 35.63/5.72 % (2582673)------------------------------ % 35.63/5.72 % (2582673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.63/5.72 % (2582673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.63/5.72 % (2582673)CaDiCaL version: 2.1.3 % 35.63/5.72 % (2582673)Termination reason: Instruction limit % 35.63/5.72 % (2582673)Termination phase: Saturation % 35.63/5.72 % (2582673)Time elapsed: 0.315 s % 35.63/5.72 % (2582673)Peak memory usage: 97 MB % 35.63/5.72 % (2582673)Instructions burned: 1088 (million) % 35.63/5.72 % Exception at run slice level % 35.63/5.72 User error: GNN currently only supports monomorphic FOL. % 35.63/5.72 % (2582683)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=2582190108:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2968 on theBenchmark for (2968ds/13494Mi) % 35.63/5.72 % Exception at run slice level % 35.63/5.72 User error: GNN currently only supports monomorphic FOL. % 35.63/5.72 % (2582684)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=3024046673:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2968 on theBenchmark for (2968ds/2503Mi) % 35.63/5.72 % (2582684)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 35.63/5.72 % (2582686)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=1579699146:i=2559:sd=1:ep=RSTC:ss=axioms_2967 on theBenchmark for (2967ds/2559Mi) % 35.63/5.72 % (2582645)Instruction limit reached! % 35.63/5.72 % (2582645)------------------------------ % 35.63/5.72 % (2582645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.63/5.72 % (2582645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.63/5.72 % (2582645)CaDiCaL version: 2.1.3 % 35.63/5.72 % (2582645)Termination reason: Instruction limit % 35.63/5.72 % (2582645)Termination phase: Saturation % 35.63/5.72 % (2582645)Time elapsed: 1.660 s % 35.63/5.72 % (2582645)Peak memory usage: 103 MB % 35.63/5.72 % (2582645)Instructions burned: 5783 (million) % 35.63/5.72 % Exception at run slice level % 35.63/5.72 User error: GNN currently only supports monomorphic FOL. % 35.63/5.72 % (2582689)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2538011710:i=30753:av=off:ss=included_2966 on theBenchmark for (2966ds/30753Mi) % 35.63/5.72 % Exception at run slice level % 35.63/5.72 User error: GNN currently only supports monomorphic FOL. % 35.63/5.72 % (2582656)Instruction limit reached! % 35.63/5.72 % (2582656)------------------------------ % 43.31/6.76 % (2582656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.31/6.76 % (2582656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.31/6.76 % (2582656)CaDiCaL version: 2.1.3 % 43.31/6.76 % (2582656)Termination reason: Instruction limit % 43.31/6.76 % (2582656)Termination phase: Saturation % 43.31/6.76 % (2582656)Time elapsed: 1.385 s % 43.31/6.76 % (2582656)Peak memory usage: 108 MB % 43.31/6.76 % (2582656)Instructions burned: 4839 (million) % 43.31/6.76 % (2582690)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3250643941:i=26473:ep=RSTC_2965 on theBenchmark for (2965ds/26473Mi) % 43.31/6.76 % Exception at run slice level % 43.31/6.76 User error: GNN currently only supports monomorphic FOL. % 43.31/6.76 % (2582692)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=3280145818:cts=off:i=2759:kws=inv_arity:fgj=on_2965 on theBenchmark for (2965ds/2759Mi) % 43.31/6.76 % (2582693)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=4207785299:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2965 on theBenchmark for (2965ds/5665Mi) % 43.31/6.76 % (2582693)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 43.31/6.76 % Exception at run slice level % 43.31/6.76 User error: GNN currently only supports monomorphic FOL. % 43.31/6.76 % (2582695)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=3667139005:i=1532:ep=RS:ss=axioms_2964 on theBenchmark for (2964ds/1532Mi) % 43.31/6.76 % (2582699)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=712099595:i=1565:sd=2:ss=axioms:sgt=32_2963 on theBenchmark for (2963ds/1565Mi) % 43.31/6.76 % Exception at run slice level % 43.31/6.76 User error: GNN currently only supports monomorphic FOL. % 43.31/6.76 % Exception at run slice level % 43.31/6.76 User error: GNN currently only supports monomorphic FOL. % 43.31/6.76 % (2582701)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=2234446304:i=1572:fgj=on:gsp=on_2962 on theBenchmark for (2962ds/1572Mi) % 43.31/6.76 % (2582701)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 43.31/6.76 % Exception at run slice level % 43.31/6.76 User error: GNN currently only supports monomorphic FOL. % 43.31/6.76 % (2582702)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=2636040897:i=6052:sd=4:ss=axioms:sgt=24_2962 on theBenchmark for (2962ds/6052Mi) % 43.31/6.76 % Exception at run slice level % 43.31/6.76 User error: GNN currently only supports monomorphic FOL. % 43.31/6.76 % (2582704)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=1599855956:i=3500:sd=1:bd=preordered:sup=off:ss=included_2961 on theBenchmark for (2961ds/3500Mi) % 43.31/6.76 % (2582706)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=2571404600:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2960 on theBenchmark for (2960ds/1842Mi) % 43.31/6.76 % (2582706)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 43.31/6.76 % Exception at run slice level % 43.31/6.76 User error: GNN currently only supports monomorphic FOL. % 43.31/6.76 % Exception at run slice level % 43.31/6.76 User error: GNN currently only supports monomorphic FOL. % 43.31/6.76 % (2582709)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=845895499:i=66096:add=on_2959 on theBenchmark for (2959ds/66096Mi) % 43.31/6.76 % Exception at run slice level % 43.31/6.76 User error: GNN currently only supports monomorphic FOL. % 43.31/6.76 % (2582710)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=3795046043:i=1884:sd=1:nm=60:ss=axioms_2959 on theBenchmark for (2959ds/1884Mi) % 43.31/6.76 % Exception at run slice level % 43.31/6.76 User error: GNN currently only supports monomorphic FOL. % 43.31/6.76 % (2582712)lrs-1011_4:1_sil=16000:bsr=on:random_seed=126225447:cts=off:i=5469:bs=on:fsr=off_2958 on theBenchmark for (2958ds/5469Mi) % 51.03/7.84 % (2582714)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=517469624:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2957 on theBenchmark for (2957ds/2037Mi) % 51.03/7.84 % Exception at run slice level % 51.03/7.84 User error: GNN currently only supports monomorphic FOL. % 51.03/7.84 % Exception at run slice level % 51.03/7.84 User error: GNN currently only supports monomorphic FOL. % 51.03/7.84 % (2582717)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=441825909:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2956 on theBenchmark for (2956ds/2110Mi) % 51.03/7.84 % (2582676)Instruction limit reached! % 51.03/7.84 % (2582676)------------------------------ % 51.03/7.84 % (2582676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.03/7.84 % (2582676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.03/7.84 % (2582676)CaDiCaL version: 2.1.3 % 51.03/7.84 % (2582676)Termination reason: Instruction limit % 51.03/7.84 % (2582676)Termination phase: Saturation % 51.03/7.84 % (2582676)Time elapsed: 1.511 s % 51.03/7.84 % (2582676)Peak memory usage: 133 MB % 51.03/7.84 % (2582676)Instructions burned: 6228 (million) % 51.03/7.84 % (2582718)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=2328103244:i=2430:add=off:aac=none:nm=16_2956 on theBenchmark for (2956ds/2430Mi) % 51.03/7.84 % Exception at run slice level % 51.03/7.84 User error: GNN currently only supports monomorphic FOL. % 51.03/7.84 % (2582721)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=580591411:cond=fast:i=4891_2955 on theBenchmark for (2955ds/4891Mi) % 51.03/7.84 % Exception at run slice level % 51.03/7.84 User error: GNN currently only supports monomorphic FOL. % 51.03/7.84 % (2582722)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=2108042376:st=2:i=14845:sd=2:ss=included:fsd=on_2954 on theBenchmark for (2954ds/14845Mi) % 51.03/7.84 % Exception at run slice level % 51.03/7.84 User error: GNN currently only supports monomorphic FOL. % 51.03/7.84 % (2582725)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=183187962:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2953 on theBenchmark for (2953ds/7534Mi) % 51.03/7.84 % Exception at run slice level % 51.03/7.84 User error: GNN currently only supports monomorphic FOL. % 51.03/7.84 % (2582726)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=1122467323:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2953 on theBenchmark for (2953ds/10353Mi) % 51.03/7.84 % Exception at run slice level % 51.03/7.84 User error: GNN currently only supports monomorphic FOL. % 51.03/7.84 % (2582728)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2897084869:i=7860_2952 on theBenchmark for (2952ds/7860Mi) % 51.03/7.84 % Exception at run slice level % 51.03/7.84 User error: GNN currently only supports monomorphic FOL. % 51.03/7.84 % (2582730)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=3389760001:i=7896:sd=2:bs=on:ss=included:sgt=20_2951 on theBenchmark for (2951ds/7896Mi) % 51.03/7.84 % Exception at run slice level % 51.03/7.84 User error: GNN currently only supports monomorphic FOL. % 51.03/7.84 % (2582732)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1480264630:i=5812:gtgl=2:gtg=all_2950 on theBenchmark for (2950ds/5812Mi) % 51.03/7.84 % (2582734)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=3245454872:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2950 on theBenchmark for (2950ds/2965Mi) % 51.03/7.84 % Exception at run slice level % 51.03/7.84 User error: GNN currently only supports monomorphic FOL. % 51.03/7.84 % Exception at run slice level % 51.03/7.84 User error: GNN currently only supports monomorphic FOL. % 51.03/7.84 % (2582737)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=4169513104:i=2967:kws=precedence:bd=preordered:av=off_2948 on theBenchmark for (2948ds/2967Mi) % 72.96/10.93 % Exception at run slice level % 72.96/10.93 User error: GNN currently only supports monomorphic FOL. % 72.96/10.93 % (2582738)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=3019933954:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2948 on theBenchmark for (2948ds/3022Mi) % 72.96/10.93 % (2582740)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=3343896965:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2947 on theBenchmark for (2947ds/3207Mi) % 72.96/10.93 % Exception at run slice level % 72.96/10.93 User error: GNN currently only supports monomorphic FOL. % 72.96/10.93 % Exception at run slice level % 72.96/10.93 User error: GNN currently only supports monomorphic FOL. % 72.96/10.93 % (2582743)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=73239194:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2945 on theBenchmark for (2945ds/3289Mi) % 72.96/10.93 % Exception at run slice level % 72.96/10.93 User error: GNN currently only supports monomorphic FOL. % 72.96/10.93 % (2582744)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=1317464011:i=38569:sd=3:ss=axioms:sgt=32_2945 on theBenchmark for (2945ds/38569Mi) % 72.96/10.93 % (2582746)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=1762502792:cts=off:i=3394_2944 on theBenchmark for (2944ds/3394Mi) % 72.96/10.93 % Exception at run slice level % 72.96/10.93 User error: GNN currently only supports monomorphic FOL. % 72.96/10.93 % Exception at run slice level % 72.96/10.93 User error: GNN currently only supports monomorphic FOL. % 72.96/10.93 % (2582749)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=2011434683:i=33824:bd=preordered_2942 on theBenchmark for (2942ds/33824Mi) % 72.96/10.93 % Exception at run slice level % 72.96/10.93 User error: GNN currently only supports monomorphic FOL. % 72.96/10.93 % (2582750)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=2657937577:i=20684:bd=all:gtg=exists_sym_2942 on theBenchmark for (2942ds/20684Mi) % 72.96/10.93 % (2582752)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=903881873: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_2941 on theBenchmark for (2941ds/7222Mi) % 72.96/10.93 % (2582752)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 72.96/10.93 % Exception at run slice level % 72.96/10.93 User error: GNN currently only supports monomorphic FOL. % 72.96/10.93 % Exception at run slice level % 72.96/10.93 User error: GNN currently only supports monomorphic FOL. % 72.96/10.93 % (2582755)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=3267801818:st=4:i=7295:sd=4:ep=R:ss=axioms_2939 on theBenchmark for (2939ds/7295Mi) % 72.96/10.93 % Exception at run slice level % 72.96/10.93 User error: GNN currently only supports monomorphic FOL. % 72.96/10.93 % (2582756)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=2004114998:i=4036:ins=10_2939 on theBenchmark for (2939ds/4036Mi) % 72.96/10.93 % (2582712)Instruction limit reached! % 72.96/10.93 % (2582712)------------------------------ % 72.96/10.93 % (2582712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.96/10.93 % (2582712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.96/10.93 % (2582712)CaDiCaL version: 2.1.3 % 72.96/10.93 % (2582712)Termination reason: Instruction limit % 72.96/10.93 % (2582712)Termination phase: Saturation % 72.96/10.93 % (2582712)Time elapsed: 1.972 s % 72.96/10.93 % (2582712)Peak memory usage: 125 MB % 72.96/10.93 % (2582712)Instructions burned: 5469 (million) % 72.96/10.93 % (2582758)lrs+10_1_sil=128000:lcm=predicate:random_seed=3862458994:st=3:i=43697:sd=5:ss=axioms_2938 on theBenchmark for (2938ds/43697Mi) % 83.76/12.44 % (2582760)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=4000234801:i=17599:gtg=all:ss=axioms:fsd=on_2937 on theBenchmark for (2937ds/17599Mi) % 83.76/12.44 % Exception at run slice level % 83.76/12.44 User error: GNN currently only supports monomorphic FOL. % 83.76/12.44 % Exception at run slice level % 83.76/12.44 User error: GNN currently only supports monomorphic FOL. % 83.76/12.44 % (2582763)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=2444016117:i=4547:bd=preordered_2936 on theBenchmark for (2936ds/4547Mi) % 83.76/12.44 % (2582764)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=3996047807:i=9294:av=off_2936 on theBenchmark for (2936ds/9294Mi) % 83.76/12.44 % Exception at run slice level % 83.76/12.44 User error: GNN currently only supports monomorphic FOL. % 83.76/12.44 % (2582767)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3364841752:i=32849:add=on_2934 on theBenchmark for (2934ds/32849Mi) % 83.76/12.44 % Exception at run slice level % 83.76/12.44 User error: GNN currently only supports monomorphic FOL. % 83.76/12.44 % Exception at run slice level % 83.76/12.44 User error: GNN currently only supports monomorphic FOL. % 83.76/12.44 % (2582769)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1153159899:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2933 on theBenchmark for (2933ds/4793Mi) % 83.76/12.44 % (2582770)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=1412249850:i=4840:nm=4:av=off_2933 on theBenchmark for (2933ds/4840Mi) % 83.76/12.44 % Exception at run slice level % 83.76/12.44 User error: GNN currently only supports monomorphic FOL. % 83.76/12.44 % (2582773)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=4111077157:cts=off:i=5002_2931 on theBenchmark for (2931ds/5002Mi) % 83.76/12.44 % Exception at run slice level % 83.76/12.44 User error: GNN currently only supports monomorphic FOL. % 83.76/12.44 % Exception at run slice level % 83.76/12.44 User error: GNN currently only supports monomorphic FOL. % 83.76/12.44 % (2582775)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=1924921056:i=30479:sd=3:ss=axioms_2930 on theBenchmark for (2930ds/30479Mi) % 83.76/12.44 % (2582776)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=2384834416:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2930 on theBenchmark for (2930ds/11035Mi) % 83.76/12.44 % (2582776)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 83.76/12.44 % Exception at run slice level % 83.76/12.44 User error: GNN currently only supports monomorphic FOL. % 83.76/12.44 % (2582728)Instruction limit reached! % 83.76/12.44 % (2582728)------------------------------ % 83.76/12.44 % (2582728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.76/12.44 % (2582728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.76/12.44 % (2582728)CaDiCaL version: 2.1.3 % 83.76/12.44 % (2582728)Termination reason: Instruction limit % 83.76/12.44 % (2582728)Termination phase: Saturation % 83.76/12.44 % (2582728)Time elapsed: 2.280 s % 83.76/12.44 % (2582728)Peak memory usage: 105 MB % 83.76/12.44 % (2582728)Instructions burned: 7863 (million) % 83.76/12.44 % (2582779)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=3791602762:i=5835_2928 on theBenchmark for (2928ds/5835Mi) % 83.76/12.44 % Exception at run slice level % 83.76/12.44 User error: GNN currently only supports monomorphic FOL. % 83.76/12.44 % (2582780)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=1138112365:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2928 on theBenchmark for (2928ds/5890Mi) % 83.76/12.44 % Exception at run slice level % 83.76/12.44 User error: GNN currently only supports monomorphic FOL. % 83.76/12.44 % (2582783)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=4125528457:cts=off:i=19910:ep=RS_2927 on theBenchmark for (2927ds/19910Mi) % 96.46/14.26 % (2582784)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=2303578860:i=20312:bd=preordered:fsr=off:er=filter_2927 on theBenchmark for (2927ds/20312Mi) % 96.46/14.26 % Exception at run slice level % 96.46/14.26 User error: GNN currently only supports monomorphic FOL. % 96.46/14.26 % Exception at run slice level % 96.46/14.26 User error: GNN currently only supports monomorphic FOL. % 96.46/14.26 % (2582787)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=1278189276:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2925 on theBenchmark for (2925ds/13822Mi) % 96.46/14.26 % (2582788)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=3638045242:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2925 on theBenchmark for (2925ds/7144Mi) % 96.46/14.26 % Exception at run slice level % 96.46/14.26 User error: GNN currently only supports monomorphic FOL. % 96.46/14.26 % (2582791)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=3511661927:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2924 on theBenchmark for (2924ds/15184Mi) % 96.46/14.26 % Exception at run slice level % 96.46/14.26 User error: GNN currently only supports monomorphic FOL. % 96.46/14.26 % (2582793)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=2480195291:i=107375_2922 on theBenchmark for (2922ds/107375Mi) % 96.46/14.26 % Exception at run slice level % 96.46/14.26 User error: GNN currently only supports monomorphic FOL. % 96.46/14.26 % (2582795)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=2153175134:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2921 on theBenchmark for (2921ds/7958Mi) % 96.46/14.26 % Exception at run slice level % 96.46/14.26 User error: GNN currently only supports monomorphic FOL. % 96.46/14.26 % (2582797)dis+10_128_sil=16000:nwc=0.7:random_seed=1195236858:i=15999:nm=2:gsp=on_2920 on theBenchmark for (2920ds/15999Mi) % 96.46/14.26 % (2582797)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 96.46/14.26 % Exception at run slice level % 96.46/14.26 User error: GNN currently only supports monomorphic FOL. % 96.46/14.26 % (2582799)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=1719789376:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2918 on theBenchmark for (2918ds/8139Mi) % 96.46/14.26 % (2582788)Instruction limit reached! % 96.46/14.26 % (2582788)------------------------------ % 96.46/14.26 % (2582788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.46/14.26 % (2582788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.46/14.26 % (2582788)CaDiCaL version: 2.1.3 % 96.46/14.26 % (2582788)Termination reason: Instruction limit % 96.46/14.26 % (2582788)Termination phase: Saturation % 96.46/14.26 % (2582788)Time elapsed: 1.954 s % 96.46/14.26 % (2582788)Peak memory usage: 149 MB % 96.46/14.26 % (2582788)Instructions burned: 7145 (million) % 96.46/14.26 % (2582801)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=4249674791:st=4:i=8950:sd=5:ss=axioms_2905 on theBenchmark for (2905ds/8950Mi) % 96.46/14.26 % Exception at run slice level % 96.46/14.26 User error: GNN currently only supports monomorphic FOL. % 96.46/14.26 % (2582803)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=1183658067:i=9809:ins=10:av=off_2901 on theBenchmark for (2901ds/9809Mi) % 96.46/14.26 % Exception at run slice level % 96.46/14.26 User error: GNN currently only supports monomorphic FOL. % 96.46/14.26 % (2582805)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=4005523954:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2898 on theBenchmark for (2898ds/9885Mi) % 96.46/14.26 % Exception at run slice level % 96.46/14.26 User error: GNN currently only supports monomorphic FOL. % 96.46/14.26 % (2582799)Instruction limit reached! % 96.46/14.26 % (2582799)------------------------------ % 96.46/14.26 % (2582799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.08/17.20 % (2582799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.08/17.20 % (2582799)CaDiCaL version: 2.1.3 % 117.08/17.20 % (2582799)Termination reason: Instruction limit % 117.08/17.20 % (2582799)Termination phase: Saturation % 117.08/17.20 % (2582799)Time elapsed: 2.164 s % 117.08/17.20 % (2582799)Peak memory usage: 124 MB % 117.08/17.20 % (2582799)Instructions burned: 8139 (million) % 117.08/17.20 % (2582807)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=522162095:cond=fast:i=32078:fgj=on:av=off_2895 on theBenchmark for (2895ds/32078Mi) % 117.08/17.20 % (2582808)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=3903373134:i=11101:bd=all:ss=axioms:sgt=8_2895 on theBenchmark for (2895ds/11101Mi) % 117.08/17.20 % Exception at run slice level % 117.08/17.20 User error: GNN currently only supports monomorphic FOL. % 117.08/17.20 % (2582811)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=3129167935:cond=on:i=13220:s2at=3:aac=none:fsd=on_2893 on theBenchmark for (2893ds/13220Mi) % 117.08/17.20 % (2582690)Instruction limit reached! % 117.08/17.20 % (2582690)------------------------------ % 117.08/17.20 % (2582690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.08/17.20 % (2582690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.08/17.20 % (2582690)CaDiCaL version: 2.1.3 % 117.08/17.20 % (2582690)Termination reason: Instruction limit % 117.08/17.20 % (2582690)Termination phase: Saturation % 117.08/17.20 % (2582690)Time elapsed: 7.307 s % 117.08/17.20 % (2582690)Peak memory usage: 447 MB % 117.08/17.20 % (2582690)Instructions burned: 26474 (million) % 117.08/17.20 % (2582813)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=1779824664:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2891 on theBenchmark for (2891ds/13528Mi) % 117.08/17.20 % Exception at run slice level % 117.08/17.20 User error: GNN currently only supports monomorphic FOL. % 117.08/17.20 % (2582815)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=2751612499:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2890 on theBenchmark for (2890ds/14854Mi) % 117.08/17.20 % Exception at run slice level % 117.08/17.20 User error: GNN currently only supports monomorphic FOL. % 117.08/17.20 % (2582817)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=3437993160:i=14974:ss=axioms:sgt=16_2888 on theBenchmark for (2888ds/14974Mi) % 117.08/17.20 % Exception at run slice level % 117.08/17.20 User error: GNN currently only supports monomorphic FOL. % 117.08/17.20 % (2582819)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=2646098703:i=33081:aac=none:fgj=on:bd=all:fsr=off_2887 on theBenchmark for (2887ds/33081Mi) % 117.08/17.20 % Exception at run slice level % 117.08/17.20 User error: GNN currently only supports monomorphic FOL. % 117.08/17.20 % (2582821)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=2671648141:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2885 on theBenchmark for (2885ds/50856Mi) % 117.08/17.20 % Exception at run slice level % 117.08/17.20 User error: GNN currently only supports monomorphic FOL. % 117.08/17.20 % (2582823)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=484829013:i=69865_2884 on theBenchmark for (2884ds/69865Mi) % 117.08/17.20 % Exception at run slice level % 117.08/17.20 User error: GNN currently only supports monomorphic FOL. % 117.08/17.20 % (2582825)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=1357805084:cond=fast:i=17802:gtgl=3:gtg=all_2882 on theBenchmark for (2882ds/17802Mi) % 117.08/17.20 % Exception at run slice level % 117.08/17.20 User error: Immediate (shared) subterms of term/literal list_case(X1,X0,X3,X2,nil(X0)) = sF44(X1,X0,X3,X2) have different types/not well-typed! % 117.08/17.20 % Exception at run slice level % 117.08/17.20 User error: GNN currently only supports monomorphic FOL. % 117.08/17.20 % (2582827)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=459670961:i=96644_2881 on theBenchmark for (2881ds/96644Mi) % 128.71/18.82 % (2582828)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 128.71/18.82 % (2582828)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=2305477291:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2881 on theBenchmark for (2881ds/21161Mi) % 128.71/18.82 % (2582797)Instruction limit reached! % 128.71/18.82 % (2582797)------------------------------ % 128.71/18.82 % (2582797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 128.71/18.82 % (2582797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.71/18.82 % (2582797)CaDiCaL version: 2.1.3 % 128.71/18.82 % (2582797)Termination reason: Instruction limit % 128.71/18.82 % (2582797)Termination phase: Saturation % 128.71/18.82 % (2582797)Time elapsed: 4.239 s % 128.71/18.82 % (2582797)Peak memory usage: 132 MB % 128.71/18.82 % (2582797)Instructions burned: 16003 (million) % 128.71/18.82 % (2582831)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=1563524370:i=22761:gtg=all:ss=axioms:fsd=on_2876 on theBenchmark for (2876ds/22761Mi) % 128.71/18.82 % Exception at run slice level % 128.71/18.82 User error: GNN currently only supports monomorphic FOL. % 128.71/18.82 % (2582833)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=2303006193:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2873 on theBenchmark for (2873ds/23713Mi) % 128.71/18.82 % (2582783)Instruction limit reached! % 128.71/18.82 % (2582783)------------------------------ % 128.71/18.82 % (2582783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 128.71/18.82 % (2582783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.71/18.82 % (2582783)CaDiCaL version: 2.1.3 % 128.71/18.82 % (2582783)Termination reason: Instruction limit % 128.71/18.82 % (2582783)Termination phase: Saturation % 128.71/18.82 % (2582783)Time elapsed: 5.680 s % 128.71/18.82 % (2582783)Peak memory usage: 149 MB % 128.71/18.82 % (2582783)Instructions burned: 19913 (million) % 128.71/18.82 % (2582835)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=2293428106:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2869 on theBenchmark for (2869ds/26509Mi) % 128.71/18.82 % Exception at run slice level % 128.71/18.82 User error: GNN currently only supports monomorphic FOL. % 128.71/18.82 % (2582664)Instruction limit reached! % 128.71/18.82 % (2582664)------------------------------ % 128.71/18.82 % (2582664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 128.71/18.82 % (2582664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.71/18.82 % (2582664)CaDiCaL version: 2.1.3 % 128.71/18.82 % (2582664)Termination reason: Instruction limit % 128.71/18.82 % (2582664)Termination phase: Saturation % 128.71/18.82 % (2582664)Time elapsed: 11.006 s % 128.71/18.82 % (2582664)Peak memory usage: 227 MB % 128.71/18.82 % (2582664)Instructions burned: 33336 (million) % 128.71/18.82 % (2582837)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=1215950275:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2866 on theBenchmark for (2866ds/28957Mi) % 128.71/18.82 % (2582838)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=946719489:i=29246:s2at=-1:kws=inv_arity:ins=10_2866 on theBenchmark for (2866ds/29246Mi) % 128.71/18.82 % Exception at run slice level % 128.71/18.82 User error: GNN currently only supports monomorphic FOL. % 128.71/18.82 % (2582841)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=1485005116:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2863 on theBenchmark for (2863ds/30082Mi) % 128.71/18.82 % (2582841)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 128.71/18.82 % (2582808)Instruction limit reached! % 128.71/18.82 % (2582808)------------------------------ % 128.71/18.82 % (2582808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 128.71/18.82 % (2582808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.71/18.82 % (2582808)CaDiCaL version: 2.1.3 % 134.35/19.68 % (2582808)Termination reason: Instruction limit % 134.35/19.68 % (2582808)Termination phase: Saturation % 134.35/19.68 % (2582808)Time elapsed: 3.238 s % 134.35/19.68 % (2582808)Peak memory usage: 130 MB % 134.35/19.68 % (2582808)Instructions burned: 11104 (million) % 134.35/19.68 % (2582843)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=2239746698:i=32262:bd=preordered_2862 on theBenchmark for (2862ds/32262Mi) % 134.35/19.68 % Exception at run slice level % 134.35/19.68 User error: GNN currently only supports monomorphic FOL. % 134.35/19.68 % (2582845)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=1265980919:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2860 on theBenchmark for (2860ds/32870Mi) % 134.35/19.68 % Exception at run slice level % 134.35/19.68 User error: GNN currently only supports monomorphic FOL. % 134.35/19.68 % (2582847)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=1876241866:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2859 on theBenchmark for (2859ds/33295Mi) % 134.35/19.68 % Exception at run slice level % 134.35/19.68 User error: GNN currently only supports monomorphic FOL. % 134.35/19.68 % (2582849)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=3054900542:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2857 on theBenchmark for (2857ds/36826Mi) % 134.35/19.68 % Exception at run slice level % 134.35/19.68 User error: GNN currently only supports monomorphic FOL. % 134.35/19.68 % (2582851)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=466491368:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2856 on theBenchmark for (2856ds/92981Mi) % 134.35/19.68 % Exception at run slice level % 134.35/19.68 User error: GNN currently only supports monomorphic FOL. % 134.35/19.68 % (2582853)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=2920314395:s2pl=on:i=49423_2853 on theBenchmark for (2853ds/49423Mi) % 134.35/19.68 % Exception at run slice level % 134.35/19.68 User error: GNN currently only supports monomorphic FOL. % 134.35/19.68 % (2582855)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=2921371643:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2850 on theBenchmark for (2850ds/57299Mi) % 134.35/19.68 % Exception at run slice level % 134.35/19.68 User error: GNN currently only supports monomorphic FOL. % 134.35/19.68 % (2582857)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=2352391617:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2847 on theBenchmark for (2847ds/127679Mi) % 134.35/19.68 % Exception at run slice level % 134.35/19.68 User error: GNN currently only supports monomorphic FOL. % 134.35/19.68 % (2582859)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=3051115992:i=69402:add=on:aac=none:fsr=off_2844 on theBenchmark for (2844ds/69402Mi) % 134.35/19.68 % Exception at run slice level % 134.35/19.68 User error: GNN currently only supports monomorphic FOL. % 134.35/19.68 % (2582861)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=3765414324:i=100512:doe=on:fgj=on:bd=all:fsd=on_2841 on theBenchmark for (2841ds/100512Mi) % 134.35/19.68 % Exception at run slice level % 134.35/19.68 User error: GNN currently only supports monomorphic FOL. % 134.35/19.68 % (2582863)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=3871029092:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2838 on theBenchmark for (2838ds/138761Mi) % 134.35/19.68 % Exception at run slice level % 134.35/19.68 User error: GNN currently only supports monomorphic FOL. % 134.35/19.68 % (2582865)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=2732827439:i=282386:rtra=on_2836 on theBenchmark for (2836ds/282386Mi) % 134.35/19.68 % Exception at run slice level % 140.87/20.55 User error: GNN currently only supports monomorphic FOL. % 140.87/20.55 % (2582867)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=2271894950:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2833 on theBenchmark for (2833ds/269354Mi) % 140.87/20.55 % Exception at run slice level % 140.87/20.55 User error: GNN currently only supports monomorphic FOL. % 140.87/20.55 % (2582869)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=819418435:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2830 on theBenchmark for (2830ds/283390Mi) % 140.87/20.55 % (2582869)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 140.87/20.55 % Exception at run slice level % 140.87/20.55 User error: GNN currently only supports monomorphic FOL. % 140.87/20.55 % (2582871)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=2280484830:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2827 on theBenchmark for (2827ds/218Mi) % 140.87/20.55 % (2582871)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 140.87/20.55 % (2582871)Refutation not found, incomplete strategy % 140.87/20.55 % (2582871)------------------------------ % 140.87/20.55 % (2582871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.87/20.55 % (2582871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.87/20.55 % (2582871)CaDiCaL version: 2.1.3 % 140.87/20.55 % (2582871)Termination reason: Refutation not found, incomplete strategy % 140.87/20.55 % (2582871)Time elapsed: 0.006 s % 140.87/20.55 % (2582871)Peak memory usage: 89 MB % 140.87/20.55 % (2582871)Instructions burned: 16 (million) % 140.87/20.55 % (2582871)------------------------------ % 140.87/20.55 % (2582871)------------------------------ % 140.87/20.55 % (2582873)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=3978780527:i=238:av=off:rtra=on:ss=axioms_2824 on theBenchmark for (2824ds/238Mi) % 140.87/20.55 % (2582873)Instruction limit reached! % 140.87/20.55 % (2582873)------------------------------ % 140.87/20.55 % (2582873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.87/20.55 % (2582873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.87/20.55 % (2582873)CaDiCaL version: 2.1.3 % 140.87/20.55 % (2582873)Termination reason: Instruction limit % 140.87/20.55 % (2582873)Termination phase: Saturation % 140.87/20.55 % (2582873)Time elapsed: 0.077 s % 140.87/20.55 % (2582873)Peak memory usage: 89 MB % 140.87/20.55 % (2582873)Instructions burned: 241 (million) % 140.87/20.55 % (2582875)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=3743991757:s2a=on:i=278:rtra=on:gtg=position_2823 on theBenchmark for (2823ds/278Mi) % 140.87/20.55 % (2582875)Instruction limit reached! % 140.87/20.55 % (2582875)------------------------------ % 140.87/20.55 % (2582875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.87/20.55 % (2582875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.87/20.55 % (2582875)CaDiCaL version: 2.1.3 % 140.87/20.55 % (2582875)Termination reason: Instruction limit % 140.87/20.55 % (2582875)Termination phase: Saturation % 140.87/20.55 % (2582875)Time elapsed: 0.093 s % 140.87/20.55 % (2582875)Peak memory usage: 91 MB % 140.87/20.55 % (2582875)Instructions burned: 280 (million) % 140.87/20.55 % (2582877)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=433603235:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2821 on theBenchmark for (2821ds/258Mi) % 140.87/20.55 % (2582877)Instruction limit reached! % 140.87/20.55 % (2582877)------------------------------ % 140.87/20.55 % (2582877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.87/20.55 % (2582877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.87/20.55 % (2582877)CaDiCaL version: 2.1.3 % 140.87/20.55 % (2582877)Termination reason: Instruction limit % 140.87/20.55 % (2582877)Termination phase: Saturation % 140.87/20.55 % (2582877)Time elapsed: 0.068 s % 140.87/20.55 % (2582877)Peak memory usage: 92 MB % 140.87/20.55 % (2582877)Instructions burned: 260 (million) % 140.87/20.55 % (2582879)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=2720438216:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2819 on theBenchmark for (2819ds/570Mi) % 140.87/20.55 % (2582879)Instruction limit reached! % 140.87/20.55 % (2582879)------------------------------ % 140.87/20.55 % (2582879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.55/20.95 % (2582879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.55/20.95 % (2582879)CaDiCaL version: 2.1.3 % 143.55/20.95 % (2582879)Termination reason: Instruction limit % 143.55/20.95 % (2582879)Termination phase: Saturation % 143.55/20.95 % (2582879)Time elapsed: 0.188 s % 143.55/20.95 % (2582879)Peak memory usage: 94 MB % 143.55/20.95 % (2582879)Instructions burned: 571 (million) % 143.55/20.95 % (2582881)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=3272090807:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2816 on theBenchmark for (2816ds/314Mi) % 143.55/20.95 % (2582881)Instruction limit reached! % 143.55/20.95 % (2582881)------------------------------ % 143.55/20.95 % (2582881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.55/20.95 % (2582881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.55/20.95 % (2582881)CaDiCaL version: 2.1.3 % 143.55/20.95 % (2582881)Termination reason: Instruction limit % 143.55/20.95 % (2582881)Termination phase: Saturation % 143.55/20.95 % (2582881)Time elapsed: 0.097 s % 143.55/20.95 % (2582881)Peak memory usage: 91 MB % 143.55/20.95 % (2582881)Instructions burned: 316 (million) % 143.55/20.95 % (2582828)Instruction limit reached! % 143.55/20.95 % (2582828)------------------------------ % 143.55/20.95 % (2582828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.55/20.95 % (2582828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.55/20.95 % (2582828)CaDiCaL version: 2.1.3 % 143.55/20.95 % (2582828)Termination reason: Instruction limit % 143.55/20.95 % (2582828)Termination phase: Saturation % 143.55/20.95 % (2582828)Time elapsed: 6.606 s % 143.55/20.95 % (2582828)Peak memory usage: 197 MB % 143.55/20.95 % (2582828)Instructions burned: 21163 (million) % 143.55/20.95 % (2582883)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=4065198917:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2815 on theBenchmark for (2815ds/650Mi) % 143.55/20.95 % (2582884)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=1089400142:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2814 on theBenchmark for (2814ds/496Mi) % 143.55/20.95 % (2582883)Instruction limit reached! % 143.55/20.95 % (2582883)------------------------------ % 143.55/20.95 % (2582883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.55/20.95 % (2582883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.55/20.95 % (2582883)CaDiCaL version: 2.1.3 % 143.55/20.95 % (2582883)Termination reason: Instruction limit % 143.55/20.95 % (2582883)Termination phase: Saturation % 143.55/20.95 % (2582883)Time elapsed: 0.218 s % 143.55/20.95 % (2582883)Peak memory usage: 95 MB % 143.55/20.95 % (2582883)Instructions burned: 650 (million) % 143.55/20.95 % (2582884)Instruction limit reached! % 143.55/20.95 % (2582884)------------------------------ % 143.55/20.95 % (2582884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.55/20.95 % (2582884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.55/20.95 % (2582884)CaDiCaL version: 2.1.3 % 143.55/20.95 % (2582884)Termination reason: Instruction limit % 143.55/20.95 % (2582884)Termination phase: Saturation % 143.55/20.95 % (2582884)Time elapsed: 0.150 s % 143.55/20.95 % (2582884)Peak memory usage: 91 MB % 143.55/20.95 % (2582884)Instructions burned: 499 (million) % 143.55/20.95 % (2582887)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=1625695381:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2812 on theBenchmark for (2812ds/588Mi) % 143.55/20.95 % (2582887)Refutation not found, incomplete strategy % 143.55/20.95 % (2582887)------------------------------ % 143.55/20.95 % (2582887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.55/20.95 % (2582887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.55/20.95 % (2582887)CaDiCaL version: 2.1.3 % 143.55/20.95 % (2582887)Termination reason: Refutation not found, incomplete strategy % 143.55/20.95 % (2582887)Time elapsed: 0.008 s % 143.55/20.95 % (2582887)Peak memory usage: 89 MB % 143.55/20.95 % (2582887)Instructions burned: 26 (million) % 143.55/20.95 % (2582888)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=2184501830:i=4700:rtra=on_2811 on theBenchmark for (2811ds/4700Mi) % 143.55/20.95 % (2582887)------------------------------ % 143.55/20.95 % (2582887)------------------------------ % 143.55/20.95 % Exception at run slice level % 143.55/20.95 User error: GNN currently only supports monomorphic FOL. % 143.55/20.95 % (2582891)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=767801079:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2809 on theBenchmark for (2809ds/226Mi) % 146.76/21.49 % (2582892)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=935746637:i=254:av=off:fsr=off:rtra=on:sup=off_2808 on theBenchmark for (2808ds/254Mi) % 146.76/21.49 % (2582891)Instruction limit reached! % 146.76/21.49 % (2582891)------------------------------ % 146.76/21.49 % (2582891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.76/21.49 % (2582891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.76/21.49 % (2582891)CaDiCaL version: 2.1.3 % 146.76/21.49 % (2582891)Termination reason: Instruction limit % 146.76/21.49 % (2582891)Termination phase: Saturation % 146.76/21.49 % (2582891)Time elapsed: 0.072 s % 146.76/21.49 % (2582891)Peak memory usage: 90 MB % 146.76/21.49 % (2582891)Instructions burned: 229 (million) % 146.76/21.49 % (2582892)Instruction limit reached! % 146.76/21.49 % (2582892)------------------------------ % 146.76/21.49 % (2582892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.76/21.49 % (2582892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.76/21.49 % (2582892)CaDiCaL version: 2.1.3 % 146.76/21.49 % (2582892)Termination reason: Instruction limit % 146.76/21.49 % (2582892)Termination phase: Saturation % 146.76/21.49 % (2582892)Time elapsed: 0.064 s % 146.76/21.49 % (2582892)Peak memory usage: 89 MB % 146.76/21.49 % (2582892)Instructions burned: 256 (million) % 146.76/21.49 % (2582895)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=3495644480:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2807 on theBenchmark for (2807ds/228Mi) % 146.76/21.49 % (2582896)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=113812344:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2807 on theBenchmark for (2807ds/1814Mi) % 146.76/21.49 % (2582895)Instruction limit reached! % 146.76/21.49 % (2582895)------------------------------ % 146.76/21.49 % (2582895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.76/21.49 % (2582895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.76/21.49 % (2582895)CaDiCaL version: 2.1.3 % 146.76/21.49 % (2582895)Termination reason: Instruction limit % 146.76/21.49 % (2582895)Termination phase: Saturation % 146.76/21.49 % (2582895)Time elapsed: 0.072 s % 146.76/21.49 % (2582895)Peak memory usage: 89 MB % 146.76/21.49 % (2582895)Instructions burned: 230 (million) % 146.76/21.49 % (2582899)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=3823129141:i=874:sd=1:aac=none:rtra=on:ss=included_2805 on theBenchmark for (2805ds/874Mi) % 146.76/21.49 % (2582899)Refutation not found, incomplete strategy % 146.76/21.49 % (2582899)------------------------------ % 146.76/21.49 % (2582899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.76/21.49 % (2582899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.76/21.49 % (2582899)CaDiCaL version: 2.1.3 % 146.76/21.49 % (2582899)Termination reason: Refutation not found, incomplete strategy % 146.76/21.49 % (2582899)Time elapsed: 0.010 s % 146.76/21.49 % (2582899)Peak memory usage: 89 MB % 146.76/21.49 % (2582899)Instructions burned: 32 (million) % 146.76/21.49 % (2582899)------------------------------ % 146.76/21.49 % (2582899)------------------------------ % 146.76/21.49 % (2582901)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=582805572:i=10404:rtra=on:ss=axioms:sgt=16_2803 on theBenchmark for (2803ds/10404Mi) % 146.76/21.49 % Exception at run slice level % 146.76/21.49 User error: GNN currently only supports monomorphic FOL. % 146.76/21.49 % (2582896)Instruction limit reached! % 146.76/21.49 % (2582896)------------------------------ % 146.76/21.49 % (2582896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.76/21.49 % (2582896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.76/21.49 % (2582896)CaDiCaL version: 2.1.3 % 146.76/21.49 % (2582896)Termination reason: Instruction limit % 146.76/21.49 % (2582896)Termination phase: Saturation % 146.76/21.49 % (2582896)Time elapsed: 0.629 s % 146.76/21.49 % (2582896)Peak memory usage: 105 MB % 146.76/21.49 % (2582896)Instructions burned: 1816 (million) % 146.76/21.49 % (2582833)Instruction limit reached! % 146.76/21.49 % (2582833)------------------------------ % 146.76/21.49 % (2582833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.76/21.49 % (2582833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.76/21.49 % (2582833)CaDiCaL version: 2.1.3 % 146.76/21.49 % (2582833)Termination reason: Instruction limit % 152.38/22.20 % (2582833)Termination phase: Saturation % 152.38/22.20 % (2582833)Time elapsed: 7.323 s % 152.38/22.20 % (2582833)Peak memory usage: 323 MB % 152.38/22.20 % (2582833)Instructions burned: 23716 (million) % 152.38/22.20 % (2582904)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3252571467:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2800 on theBenchmark for (2800ds/268Mi) % 152.38/22.20 % (2582905)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=1938871457:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2799 on theBenchmark for (2799ds/1184Mi) % 152.38/22.20 % (2582905)Refutation not found, incomplete strategy % 152.38/22.20 % (2582905)------------------------------ % 152.38/22.20 % (2582905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.38/22.20 % (2582905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.38/22.20 % (2582905)CaDiCaL version: 2.1.3 % 152.38/22.20 % (2582905)Termination reason: Refutation not found, incomplete strategy % 152.38/22.20 % (2582905)Time elapsed: 0.008 s % 152.38/22.20 % (2582905)Peak memory usage: 89 MB % 152.38/22.20 % (2582905)Instructions burned: 27 (million) % 152.38/22.20 % (2582904)Instruction limit reached! % 152.38/22.20 % (2582904)------------------------------ % 152.38/22.20 % (2582904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.38/22.20 % (2582904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.38/22.20 % (2582904)CaDiCaL version: 2.1.3 % 152.38/22.20 % (2582904)Termination reason: Instruction limit % 152.38/22.20 % (2582904)Termination phase: Saturation % 152.38/22.20 % (2582904)Time elapsed: 0.084 s % 152.38/22.20 % (2582904)Peak memory usage: 92 MB % 152.38/22.20 % (2582904)Instructions burned: 270 (million) % 152.38/22.20 % (2582907)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=799230307:st=3:i=26386:sd=3:rtra=on:ss=axioms_2799 on theBenchmark for (2799ds/26386Mi) % 152.38/22.20 % (2582910)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=896731626:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2798 on theBenchmark for (2798ds/250Mi) % 152.38/22.20 % (2582910)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 152.38/22.20 % (2582905)------------------------------ % 152.38/22.20 % (2582905)------------------------------ % 152.38/22.20 % (2582910)Instruction limit reached! % 152.38/22.20 % (2582910)------------------------------ % 152.38/22.20 % (2582910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.38/22.20 % (2582910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.38/22.20 % (2582910)CaDiCaL version: 2.1.3 % 152.38/22.20 % (2582910)Termination reason: Instruction limit % 152.38/22.20 % (2582910)Termination phase: Saturation % 152.38/22.20 % (2582910)Time elapsed: 0.076 s % 152.38/22.20 % (2582910)Peak memory usage: 93 MB % 152.38/22.20 % (2582910)Instructions burned: 252 (million) % 152.38/22.20 % Exception at run slice level % 152.38/22.20 User error: GNN currently only supports monomorphic FOL. % 152.38/22.20 % (2582912)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=4117591047:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2797 on theBenchmark for (2797ds/268Mi) % 152.38/22.20 % Exception at run slice level % 152.38/22.20 User error: Immediate (shared) subterms of term/literal aa(X1,fun(X2,X0),X3,X4) = sF59(X1,X2,X0,X3,X4) have different types/not well-typed! % 152.38/22.20 % (2582913)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=120620415:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2796 on theBenchmark for (2796ds/282Mi) % 152.38/22.20 % (2582913)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 152.38/22.20 % (2582914)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=2491198333:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2796 on theBenchmark for (2796ds/862Mi) % 152.38/22.20 % (2582914)Refutation not found, incomplete strategy % 152.38/22.20 % (2582914)------------------------------ % 152.38/22.20 % (2582914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.38/22.20 % (2582914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.38/22.20 % (2582914)CaDiCaL version: 2.1.3 % 152.38/22.20 % (2582914)Termination reason: Refutation not found, incomplete strategy % 152.38/22.20 % (2582914)Time elapsed: 0.008 s % 152.38/22.20 % (2582914)Peak memory usage: 89 MB % 159.82/23.29 % (2582914)Instructions burned: 24 (million) % 159.82/23.29 % (2582913)Instruction limit reached! % 159.82/23.29 % (2582913)------------------------------ % 159.82/23.29 % (2582913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.82/23.29 % (2582913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.82/23.29 % (2582913)CaDiCaL version: 2.1.3 % 159.82/23.29 % (2582913)Termination reason: Instruction limit % 159.82/23.29 % (2582913)Termination phase: Saturation % 159.82/23.29 % (2582913)Time elapsed: 0.069 s % 159.82/23.29 % (2582913)Peak memory usage: 91 MB % 159.82/23.29 % (2582913)Instructions burned: 284 (million) % 159.82/23.29 % (2582916)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=2300578111:i=12120:aac=none:ins=25:rtra=on_2796 on theBenchmark for (2796ds/12120Mi) % 159.82/23.29 % (2582919)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=1182456420:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2795 on theBenchmark for (2795ds/300Mi) % 159.82/23.29 % (2582919)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 159.82/23.29 % (2582914)------------------------------ % 159.82/23.29 % (2582914)------------------------------ % 159.82/23.29 % (2582919)Instruction limit reached! % 159.82/23.29 % (2582919)------------------------------ % 159.82/23.29 % (2582919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.82/23.29 % (2582919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.82/23.29 % (2582919)CaDiCaL version: 2.1.3 % 159.82/23.29 % (2582919)Termination reason: Instruction limit % 159.82/23.29 % (2582919)Termination phase: Saturation % 159.82/23.29 % (2582919)Time elapsed: 0.105 s % 159.82/23.29 % (2582919)Peak memory usage: 93 MB % 159.82/23.29 % (2582919)Instructions burned: 300 (million) % 159.82/23.29 % Exception at run slice level % 159.82/23.29 User error: GNN currently only supports monomorphic FOL. % 159.82/23.29 % (2582922)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=4116271815:i=28310:bd=all:rtra=on_2794 on theBenchmark for (2794ds/28310Mi) % 159.82/23.29 % (2582923)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2472541787:i=1334:av=off:fsr=off:rtra=on_2793 on theBenchmark for (2793ds/1334Mi) % 159.82/23.29 % (2582924)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=2116834096:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2793 on theBenchmark for (2793ds/370Mi) % 159.82/23.29 % (2582758)Instruction limit reached! % 159.82/23.29 % (2582758)------------------------------ % 159.82/23.29 % (2582758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.82/23.29 % (2582758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.82/23.29 % (2582758)CaDiCaL version: 2.1.3 % 159.82/23.29 % (2582758)Termination reason: Instruction limit % 159.82/23.29 % (2582758)Termination phase: Saturation % 159.82/23.29 % (2582758)Time elapsed: 14.602 s % 159.82/23.29 % (2582758)Peak memory usage: 312 MB % 159.82/23.29 % (2582758)Instructions burned: 43698 (million) % 159.82/23.29 % (2582924)Instruction limit reached! % 159.82/23.29 % (2582924)------------------------------ % 159.82/23.29 % (2582924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.82/23.29 % (2582924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.82/23.29 % (2582924)CaDiCaL version: 2.1.3 % 159.82/23.29 % (2582924)Termination reason: Instruction limit % 159.82/23.29 % (2582924)Termination phase: Saturation % 159.82/23.29 % (2582924)Time elapsed: 0.106 s % 159.82/23.29 % (2582924)Peak memory usage: 92 MB % 159.82/23.29 % (2582924)Instructions burned: 370 (million) % 159.82/23.29 % Exception at run slice level % 159.82/23.29 User error: GNN currently only supports monomorphic FOL. % 159.82/23.29 % (2582928)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=906734437:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2791 on theBenchmark for (2791ds/386Mi) % 159.82/23.29 % (2582929)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=938910596:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2791 on theBenchmark for (2791ds/9700Mi) % 159.82/23.29 % (2582930)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=2478660250:i=24222:sd=1:rtra=on:ss=included_2791 on theBenchmark for (2791ds/24222Mi) % 167.22/24.38 % (2582928)Instruction limit reached! % 167.22/24.38 % (2582928)------------------------------ % 167.22/24.38 % (2582928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.22/24.38 % (2582928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.22/24.38 % (2582928)CaDiCaL version: 2.1.3 % 167.22/24.38 % (2582928)Termination reason: Instruction limit % 167.22/24.38 % (2582928)Termination phase: Saturation % 167.22/24.38 % (2582928)Time elapsed: 0.129 s % 167.22/24.38 % (2582928)Peak memory usage: 92 MB % 167.22/24.38 % (2582928)Instructions burned: 388 (million) % 167.22/24.38 % (2582923)Instruction limit reached! % 167.22/24.38 % (2582923)------------------------------ % 167.22/24.38 % (2582923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.22/24.38 % (2582923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.22/24.38 % (2582923)CaDiCaL version: 2.1.3 % 167.22/24.38 % (2582923)Termination reason: Instruction limit % 167.22/24.38 % (2582923)Termination phase: Saturation % 167.22/24.38 % (2582923)Time elapsed: 0.363 s % 167.22/24.38 % (2582923)Peak memory usage: 90 MB % 167.22/24.38 % (2582923)Instructions burned: 1337 (million) % 167.22/24.38 % (2582934)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=3855957987:i=638:kws=precedence:fsr=off:rtra=on_2789 on theBenchmark for (2789ds/638Mi) % 167.22/24.38 % Exception at run slice level % 167.22/24.38 User error: GNN currently only supports monomorphic FOL. % 167.22/24.38 % (2582935)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1379722977:i=4128:ep=RST:rtra=on_2788 on theBenchmark for (2788ds/4128Mi) % 167.22/24.38 % (2582935)Refutation not found, incomplete strategy % 167.22/24.38 % (2582935)------------------------------ % 167.22/24.38 % (2582935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.22/24.38 % (2582935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.22/24.38 % (2582935)CaDiCaL version: 2.1.3 % 167.22/24.38 % (2582935)Termination reason: Refutation not found, incomplete strategy % 167.22/24.38 % (2582935)Time elapsed: 0.008 s % 167.22/24.38 % (2582935)Peak memory usage: 89 MB % 167.22/24.38 % (2582935)Instructions burned: 27 (million) % 167.22/24.38 % (2582937)dis-1011_128_sil=32000:si=on:random_seed=1971958228:i=7412:ep=RST:av=off:rtra=on_2788 on theBenchmark for (2788ds/7412Mi) % 167.22/24.38 % (2582935)------------------------------ % 167.22/24.38 % (2582935)------------------------------ % 167.22/24.38 % (2582934)Instruction limit reached! % 167.22/24.38 % (2582934)------------------------------ % 167.22/24.38 % (2582934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.22/24.38 % (2582934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.22/24.38 % (2582934)CaDiCaL version: 2.1.3 % 167.22/24.38 % (2582934)Termination reason: Instruction limit % 167.22/24.38 % (2582934)Termination phase: Saturation % 167.22/24.38 % (2582934)Time elapsed: 0.197 s % 167.22/24.38 % (2582934)Peak memory usage: 94 MB % 167.22/24.38 % (2582934)Instructions burned: 641 (million) % 167.22/24.38 % (2582940)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3365158610:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2786 on theBenchmark for (2786ds/1514Mi) % 167.22/24.38 % (2582940)Refutation not found, incomplete strategy % 167.22/24.38 % (2582940)------------------------------ % 167.22/24.38 % (2582940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.22/24.38 % (2582940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.22/24.38 % (2582940)CaDiCaL version: 2.1.3 % 167.22/24.38 % (2582940)Termination reason: Refutation not found, incomplete strategy % 167.22/24.38 % (2582940)Time elapsed: 0.009 s % 167.22/24.38 % (2582940)Peak memory usage: 89 MB % 167.22/24.38 % (2582940)Instructions burned: 30 (million) % 167.22/24.38 % (2582941)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=3943205925:i=27826:rtra=on:ss=axioms:sgt=8_2786 on theBenchmark for (2786ds/27826Mi) % 167.22/24.38 % (2582940)------------------------------ % 167.22/24.38 % (2582940)------------------------------ % 167.22/24.38 % Exception at run slice level % 167.22/24.38 User error: GNN currently only supports monomorphic FOL. % 167.22/24.38 % (2582944)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=3662719785:i=19850:aac=none:rtra=on_2784 on theBenchmark for (2784ds/19850Mi) % 174.90/25.48 % (2582945)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3738764822:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2783 on theBenchmark for (2783ds/4958Mi) % 174.90/25.48 % (2582945)Refutation not found, incomplete strategy % 174.90/25.48 % (2582945)------------------------------ % 174.90/25.48 % (2582945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.90/25.48 % (2582945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.90/25.48 % (2582945)CaDiCaL version: 2.1.3 % 174.90/25.48 % (2582945)Termination reason: Refutation not found, incomplete strategy % 174.90/25.48 % (2582945)Time elapsed: 0.007 s % 174.90/25.48 % (2582945)Peak memory usage: 89 MB % 174.90/25.48 % (2582945)Instructions burned: 20 (million) % 174.90/25.48 % Exception at run slice level % 174.90/25.48 User error: GNN currently only supports monomorphic FOL. % 174.90/25.48 % (2582945)------------------------------ % 174.90/25.48 % (2582945)------------------------------ % 174.90/25.48 % (2582949)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=2837494870:st=1.5:i=22290:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2781 on theBenchmark for (2781ds/22290Mi) % 174.90/25.48 % (2582948)ott+1002_64_sil=16000:si=on:sp=const_min:nwc=0.5:random_seed=1403420586:i=880:nm=2:av=off:rtra=on:gtg=exists_all:fdi=8:gsp=on_2781 on theBenchmark for (2781ds/880Mi) % 174.90/25.48 % (2582948)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 174.90/25.48 % Exception at run slice level % 174.90/25.48 User error: GNN currently only supports monomorphic FOL. % 174.90/25.48 % (2582952)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=159804494:cts=off:i=6068:av=off:rtra=on:er=known:fsd=on_2778 on theBenchmark for (2778ds/6068Mi) % 174.90/25.48 % (2582948)Instruction limit reached! % 174.90/25.48 % (2582948)------------------------------ % 174.90/25.48 % (2582948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.90/25.48 % (2582948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.90/25.48 % (2582948)CaDiCaL version: 2.1.3 % 174.90/25.48 % (2582948)Termination reason: Instruction limit % 174.90/25.48 % (2582948)Termination phase: Saturation % 174.90/25.48 % (2582948)Time elapsed: 0.307 s % 174.90/25.48 % (2582948)Peak memory usage: 98 MB % 174.90/25.48 % (2582948)Instructions burned: 881 (million) % 174.90/25.48 % (2582954)lrs-1011_64:1_sil=8000:si=on:erd=off:urr=on:nwc=0.7:br=off:random_seed=3629921890:st=2:s2a=on:i=1048:s2at=2:rtra=on:ss=axioms_2777 on theBenchmark for (2777ds/1048Mi) % 174.90/25.48 % Exception at run slice level % 174.90/25.48 User error: GNN currently only supports monomorphic FOL. % 174.90/25.48 % (2582837)Instruction limit reached! % 174.90/25.48 % (2582837)------------------------------ % 174.90/25.48 % (2582837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.90/25.48 % (2582837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.90/25.48 % (2582837)CaDiCaL version: 2.1.3 % 174.90/25.48 % (2582837)Termination reason: Instruction limit % 174.90/25.48 % (2582837)Termination phase: Saturation % 174.90/25.48 % (2582837)Time elapsed: 9.122 s % 174.90/25.48 % (2582837)Peak memory usage: 252 MB % 174.90/25.48 % (2582837)Instructions burned: 28959 (million) % 174.90/25.48 % (2582956)lrs+1011_16:1_sil=8000:si=on:acc=on:urr=on:fd=preordered:flr=on:random_seed=4183107029:avsq=on:i=2032:avsqr=676809,524288:sd=1:rtra=on:ss=axioms_2775 on theBenchmark for (2775ds/2032Mi) % 174.90/25.48 % (2582957)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:si=on:s2agt=16:random_seed=2886594082:i=28246:bd=preordered:ins=4:rtra=on_2774 on theBenchmark for (2774ds/28246Mi) % 174.90/25.48 % (2582954)Instruction limit reached! % 174.90/25.48 % (2582954)------------------------------ % 174.90/25.48 % (2582954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.90/25.48 % (2582954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.90/25.48 % (2582954)CaDiCaL version: 2.1.3 % 174.90/25.48 % (2582954)Termination reason: Instruction limit % 174.90/25.48 % (2582954)Termination phase: Saturation % 174.90/25.48 % (2582954)Time elapsed: 0.304 s % 174.90/25.48 % (2582954)Peak memory usage: 93 MB % 174.90/25.48 % (2582954)Instructions burned: 1052 (million) % 174.90/25.48 % (2582960)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:si=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1729762009:i=11562:kws=precedence:bd=all:rtra=on:rawr=on_2773 on theBenchmark for (2773ds/11562Mi) % 185.08/26.87 % Exception at run slice level % 185.08/26.87 User error: GNN currently only supports monomorphic FOL. % 185.08/26.87 % (2582962)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=1158582561:i=4896:gtgl=5:bd=preordered:rtra=on:gtg=all_2771 on theBenchmark for (2771ds/4896Mi) % 185.08/26.87 % Exception at run slice level % 185.08/26.87 User error: GNN currently only supports monomorphic FOL. % 185.08/26.87 % (2582964)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:si=on:lcm=reverse:random_seed=1575361139:i=6446:kws=precedence:fgj=on:av=off:rtra=on_2768 on theBenchmark for (2768ds/6446Mi) % 185.08/26.87 % (2582956)Instruction limit reached! % 185.08/26.87 % (2582956)------------------------------ % 185.08/26.87 % (2582956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.08/26.87 % (2582956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.08/26.87 % (2582956)CaDiCaL version: 2.1.3 % 185.08/26.87 % (2582956)Termination reason: Instruction limit % 185.08/26.87 % (2582956)Termination phase: Saturation % 185.08/26.87 % (2582956)Time elapsed: 0.637 s % 185.08/26.87 % (2582956)Peak memory usage: 107 MB % 185.08/26.87 % (2582956)Instructions burned: 2033 (million) % 185.08/26.87 % (2582966)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:si=on:sp=occurrence:sos=on:random_seed=2856674830:st=5.6:i=4066:sd=3:rtra=on:ss=axioms_2767 on theBenchmark for (2767ds/4066Mi) % 185.08/26.87 % Exception at run slice level % 185.08/26.87 User error: GNN currently only supports monomorphic FOL. % 185.08/26.87 % (2582968)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:si=on:random_seed=641143945:i=4110:nm=16:rtra=on:gtg=position:ss=axioms:fsd=on_2765 on theBenchmark for (2765ds/4110Mi) % 185.08/26.87 % Exception at run slice level % 185.08/26.87 User error: GNN currently only supports monomorphic FOL. % 185.08/26.87 % (2582970)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=3258275589:i=43222:sd=3:rtra=on:ss=axioms_2764 on theBenchmark for (2764ds/43222Mi) % 185.08/26.87 % (2582937)Instruction limit reached! % 185.08/26.87 % (2582937)------------------------------ % 185.08/26.87 % (2582937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.08/26.87 % (2582937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.08/26.87 % (2582937)CaDiCaL version: 2.1.3 % 185.08/26.87 % (2582937)Termination reason: Instruction limit % 185.08/26.87 % (2582937)Termination phase: Saturation % 185.08/26.87 % (2582937)Time elapsed: 2.351 s % 185.08/26.87 % (2582937)Peak memory usage: 153 MB % 185.08/26.87 % (2582937)Instructions burned: 7412 (million) % 185.08/26.87 % Exception at run slice level % 185.08/26.87 User error: GNN currently only supports monomorphic FOL. % 185.08/26.87 % (2582972)lrs+10_1_sil=8000:si=on:sp=occurrence:sos=all:lma=off:random_seed=640843431:i=9670:sd=13:rtra=on:ss=axioms:sgt=23_2763 on theBenchmark for (2763ds/9670Mi) % 185.08/26.87 % (2582929)Instruction limit reached! % 185.08/26.87 % (2582929)------------------------------ % 185.08/26.87 % (2582929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.08/26.87 % (2582929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.08/26.87 % (2582929)CaDiCaL version: 2.1.3 % 185.08/26.87 % (2582929)Termination reason: Instruction limit % 185.08/26.87 % (2582929)Termination phase: Saturation % 185.08/26.87 % (2582929)Time elapsed: 2.786 s % 185.08/26.87 % (2582929)Peak memory usage: 111 MB % 185.08/26.87 % (2582929)Instructions burned: 9702 (million) % 185.08/26.87 % (2582973)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=2291128429:st=5:i=1594:s2at=3:sd=4:bs=unit_only:av=off:rtra=on:sup=off:ss=included_2763 on theBenchmark for (2763ds/1594Mi) % 185.08/26.87 % Exception at run slice level % 185.08/26.87 User error: GNN currently only supports monomorphic FOL. % 185.08/26.87 % (2582975)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=3169313057:i=4652:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:rtra=on:fsd=on_2762 on theBenchmark for (2762ds/4652Mi) % 185.08/26.87 % (2582975)Refutation not found, incomplete strategy % 185.08/26.87 % (2582975)------------------------------ % 185.08/26.87 % (2582975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.83/27.96 % (2582975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.83/27.96 % (2582975)CaDiCaL version: 2.1.3 % 192.83/27.96 % (2582975)Termination reason: Refutation not found, incomplete strategy % 192.83/27.96 % (2582975)Time elapsed: 0.038 s % 192.83/27.96 % (2582975)Peak memory usage: 90 MB % 192.83/27.96 % (2582975)Instructions burned: 108 (million) % 192.83/27.96 % (2582977)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:si=on:sos=all:urr=on:br=off:random_seed=306150018:i=12076:nm=6:rtra=on_2761 on theBenchmark for (2761ds/12076Mi) % 192.83/27.96 % (2582975)------------------------------ % 192.83/27.96 % (2582975)------------------------------ % 192.83/27.96 % Exception at run slice level % 192.83/27.96 User error: GNN currently only supports monomorphic FOL. % 192.83/27.96 % (2582980)lrs+10_1_sil=32000:si=on:sp=occurrence:random_seed=1804463239:st=2:i=66668:sd=3:rtra=on:ss=included:sgt=32_2759 on theBenchmark for (2759ds/66668Mi) % 192.83/27.96 % (2582981)lrs+10_4_sil=8000:plsq=on:si=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2771336443:st=3.7:s2a=on:i=2016:s2at=1.2:sd=3:bd=all:av=off:rtra=on:fdi=8:sup=off:ss=axioms_2758 on theBenchmark for (2758ds/2016Mi) % 192.83/27.96 % (2582973)Instruction limit reached! % 192.83/27.96 % (2582973)------------------------------ % 192.83/27.96 % (2582973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.83/27.96 % (2582973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.83/27.96 % (2582973)CaDiCaL version: 2.1.3 % 192.83/27.96 % (2582973)Termination reason: Instruction limit % 192.83/27.96 % (2582973)Termination phase: Saturation % 192.83/27.96 % (2582973)Time elapsed: 0.468 s % 192.83/27.96 % (2582973)Peak memory usage: 100 MB % 192.83/27.96 % (2582973)Instructions burned: 1595 (million) % 192.83/27.96 % (2582984)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:si=on:sp=const_frequency:spb=intro:gs=on:random_seed=1421739147:i=16654:s2at=5:bd=preordered:rtra=on_2757 on theBenchmark for (2757ds/16654Mi) % 192.83/27.96 % Exception at run slice level % 192.83/27.96 User error: GNN currently only supports monomorphic FOL. % 192.83/27.96 % (2582849)Instruction limit reached! % 192.83/27.96 % (2582849)------------------------------ % 192.83/27.96 % (2582849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.83/27.96 % (2582849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.83/27.96 % (2582849)CaDiCaL version: 2.1.3 % 192.83/27.96 % (2582849)Termination reason: Instruction limit % 192.83/27.96 % (2582849)Termination phase: Saturation % 192.83/27.96 % (2582849)Time elapsed: 10.269 s % 192.83/27.96 % (2582849)Peak memory usage: 228 MB % 192.83/27.96 % (2582849)Instructions burned: 36828 (million) % 192.83/27.96 % (2582986)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:si=on:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=891299610:s2a=on:i=2166:s2at=1.87328:slsql=off:ep=RSTC:rtra=on:fdi=16_2754 on theBenchmark for (2754ds/2166Mi) % 192.83/27.96 % (2582987)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:si=on:spb=goal:fd=preordered:random_seed=1021039157:i=2168:sd=1:bd=preordered:av=off:fsr=off:rtra=on:ss=axioms:sgt=14_2753 on theBenchmark for (2753ds/2168Mi) % 192.83/27.96 % (2582981)Instruction limit reached! % 192.83/27.96 % (2582981)------------------------------ % 192.83/27.96 % (2582981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.83/27.96 % (2582981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.83/27.96 % (2582981)CaDiCaL version: 2.1.3 % 192.83/27.96 % (2582981)Termination reason: Instruction limit % 192.83/27.96 % (2582981)Termination phase: Saturation % 192.83/27.96 % (2582981)Time elapsed: 0.544 s % 192.83/27.96 % (2582981)Peak memory usage: 105 MB % 192.83/27.96 % (2582981)Instructions burned: 2017 (million) % 192.83/27.96 % (2582990)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:si=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=831738635:i=13990:s2at=5:rtra=on:gtg=all_2752 on theBenchmark for (2752ds/13990Mi) % 192.83/27.96 % Exception at run slice level % 192.83/27.96 User error: Immediate (shared) subterms of term/literal sF55(X1,X0,X3) = aa(fun(X1,X0),fun(X1,fun(list(X0),list(X0))),sF54(X0,X1),X3) have different types/not well-typed! % 192.83/27.96 % (2582992)lrs+10_1_sil=32000:si=on:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1225074943:st=2:i=12450:sd=15:rtra=on:ss=axioms_2751 on theBenchmark for (2751ds/12450Mi) % 203.24/29.44 % (2582986)Instruction limit reached! % 203.24/29.44 % (2582986)------------------------------ % 203.24/29.44 % (2582986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.24/29.44 % (2582986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.24/29.44 % (2582986)CaDiCaL version: 2.1.3 % 203.24/29.44 % (2582986)Termination reason: Instruction limit % 203.24/29.44 % (2582986)Termination phase: Saturation % 203.24/29.44 % (2582986)Time elapsed: 0.615 s % 203.24/29.44 % (2582986)Peak memory usage: 107 MB % 203.24/29.44 % (2582986)Instructions burned: 2170 (million) % 203.24/29.44 % (2582987)Instruction limit reached! % 203.24/29.44 % (2582987)------------------------------ % 203.24/29.44 % (2582987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.24/29.44 % (2582987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.24/29.44 % (2582987)CaDiCaL version: 2.1.3 % 203.24/29.44 % (2582987)Termination reason: Instruction limit % 203.24/29.44 % (2582987)Termination phase: Saturation % 203.24/29.44 % (2582987)Time elapsed: 0.681 s % 203.24/29.44 % (2582987)Peak memory usage: 107 MB % 203.24/29.44 % (2582987)Instructions burned: 2168 (million) % 203.24/29.44 % (2582994)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:si=on:lcm=reverse:random_seed=2301550857:cond=fast:i=6744:sd=1:nm=16:rtra=on:gtg=position:ss=axioms_2747 on theBenchmark for (2747ds/6744Mi) % 203.24/29.44 % (2582995)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sos=all:random_seed=1991944754:st=2.3:i=52914:sd=10:rtra=on:ss=included:sgt=8_2746 on theBenchmark for (2746ds/52914Mi) % 203.24/29.44 % Exception at run slice level % 203.24/29.44 User error: GNN currently only supports monomorphic FOL. % 203.24/29.44 % (2582998)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:si=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=498270131:i=26988:s2at=1.31:bd=all:ins=10:rtra=on:gtg=exists_top_2744 on theBenchmark for (2744ds/26988Mi) % 203.24/29.44 % Exception at run slice level % 203.24/29.44 User error: GNN currently only supports monomorphic FOL. % 203.24/29.44 % (2583000)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:si=on:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=1961074850:i=5006:nm=4:rtra=on:gsp=on:ss=axioms:sgt=15_2743 on theBenchmark for (2743ds/5006Mi) % 203.24/29.44 % (2583000)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 203.24/29.44 % Exception at run slice level % 203.24/29.44 User error: GNN currently only supports monomorphic FOL. % 203.24/29.44 % Exception at run slice level % 203.24/29.44 User error: GNN currently only supports monomorphic FOL. % 203.24/29.44 % (2583002)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:si=on:sos=on:lsd=10:random_seed=1606020289:i=5118:sd=1:ep=RSTC:rtra=on:ss=axioms_2741 on theBenchmark for (2741ds/5118Mi) % 203.24/29.44 % (2583004)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:si=on:fdtod=off:random_seed=1998864960:i=61506:av=off:rtra=on:ss=included_2740 on theBenchmark for (2740ds/61506Mi) % 203.24/29.44 % (2582960)Instruction limit reached! % 203.24/29.44 % (2582960)------------------------------ % 203.24/29.44 % (2582960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.24/29.44 % (2582960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.24/29.44 % (2582960)CaDiCaL version: 2.1.3 % 203.24/29.44 % (2582960)Termination reason: Instruction limit % 203.24/29.44 % (2582960)Termination phase: Saturation % 203.24/29.44 % (2582960)Time elapsed: 3.325 s % 203.24/29.44 % (2582960)Peak memory usage: 111 MB % 203.24/29.44 % (2582960)Instructions burned: 11565 (million) % 203.24/29.44 % Exception at run slice level % 203.24/29.44 User error: GNN currently only supports monomorphic FOL. % 203.24/29.44 % (2583006)lrs+10_1024_sil=64000:plsq=on:plsqc=4:si=on:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=735754035:i=52946:ep=RSTC:rtra=on_2738 on theBenchmark for (2738ds/52946Mi) % 203.24/29.44 % (2583007)dis-1011_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:tgt=ground:npcc=on:si=on:sp=arity:sos=on:erd=off:rp=on:gs=on:kmz=on:random_seed=2054245022:cts=off:i=5518:kws=inv_arity:fgj=on:rtra=on_2738 on theBenchmark for (2738ds/5518Mi) % 203.24/29.44 % Exception at run slice level % 203.24/29.44 User error: GNN currently only supports monomorphic FOL. % 203.24/29.44 % (2583010)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:si=on:sp=weighted_frequency:sos=all:spb=goal_then_units:urr=ec_only:sac=on:random_seed=1330497406:st=1.2:i=11330:sd=2:ep=RSTC:rtra=on:gsp=on:ss=axioms_2737 on theBenchmark for (2737ds/11330Mi) % 217.07/31.37 % (2583010)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 217.07/31.37 % Exception at run slice level % 217.07/31.37 User error: GNN currently only supports monomorphic FOL. % 217.07/31.37 % Exception at run slice level % 217.07/31.37 User error: GNN currently only supports monomorphic FOL. % 217.07/31.37 % (2583012)dis+1011_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:npcc=on:si=on:sos=on:lsd=20:urr=full:alpa=true:sac=on:random_seed=932652303:i=3064:ep=RS:rtra=on:ss=axioms_2735 on theBenchmark for (2735ds/3064Mi) % 217.07/31.37 % (2583013)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3923225257:i=3130:sd=2:rtra=on:ss=axioms:sgt=32_2734 on theBenchmark for (2734ds/3130Mi) % 217.07/31.37 % (2582972)Instruction limit reached! % 217.07/31.37 % (2582972)------------------------------ % 217.07/31.37 % (2582972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.07/31.37 % (2582972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.07/31.37 % (2582972)CaDiCaL version: 2.1.3 % 217.07/31.37 % (2582972)Termination reason: Instruction limit % 217.07/31.37 % (2582972)Termination phase: Saturation % 217.07/31.37 % (2582972)Time elapsed: 3.011 s % 217.07/31.37 % (2582972)Peak memory usage: 139 MB % 217.07/31.37 % (2582972)Instructions burned: 9672 (million) % 217.07/31.37 % Exception at run slice level % 217.07/31.37 User error: GNN currently only supports monomorphic FOL. % 217.07/31.37 % (2583016)lrs-1011_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:sims=off:bsd=on:si=on:sp=unary_first:erd=off:spb=goal:lcm=reverse:gs=on:s2agt=8:random_seed=4095075834:i=3144:fgj=on:rtra=on:gsp=on_2732 on theBenchmark for (2732ds/3144Mi) % 217.07/31.37 % (2583016)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 217.07/31.37 % Exception at run slice level % 217.07/31.37 User error: GNN currently only supports monomorphic FOL. % 217.07/31.37 % (2583017)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:si=on:sp=occurrence:sos=on:newcnf=on:random_seed=1994492253:i=12104:sd=4:rtra=on:ss=axioms:sgt=24_2732 on theBenchmark for (2732ds/12104Mi) % 217.07/31.37 % (2583019)lrs+21_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:si=on:sp=arity:sos=on:erd=off:lcm=predicate:alpa=false:sac=on:random_seed=102288442:i=7000:sd=1:bd=preordered:rtra=on:sup=off:ss=included_2731 on theBenchmark for (2731ds/7000Mi) % 217.07/31.37 % Exception at run slice level % 217.07/31.37 User error: GNN currently only supports monomorphic FOL. % 217.07/31.37 % Exception at run slice level % 217.07/31.37 User error: GNN currently only supports monomorphic FOL. % 217.07/31.37 % Exception at run slice level % 217.07/31.37 User error: GNN currently only supports monomorphic FOL. % 217.07/31.37 % (2583022)lrs+35_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:npcc=on:fde=none:si=on:sp=weighted_frequency:erd=off:spb=non_intro:updr=off:newcnf=on:random_seed=1972997156:i=3684:sd=3:fgj=on:rtra=on:gtg=position:gsp=on:ss=axioms:sgt=20_2729 on theBenchmark for (2729ds/3684Mi) % 217.07/31.37 % (2583022)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 217.07/31.37 % (2583023)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:si=on:bsr=unit_only:random_seed=2832747713:i=132192:add=on:rtra=on_2729 on theBenchmark for (2729ds/132192Mi) % 217.07/31.37 % (2583025)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:si=on:random_seed=359379862:i=3768:sd=1:nm=60:rtra=on:ss=axioms_2728 on theBenchmark for (2728ds/3768Mi) % 217.07/31.37 % Exception at run slice level % 217.07/31.37 User error: GNN currently only supports monomorphic FOL. % 217.07/31.37 % Exception at run slice level % 217.07/31.37 User error: GNN currently only supports monomorphic FOL. % 217.07/31.37 % Exception at run slice level % 217.07/31.37 User error: GNN currently only supports monomorphic FOL. % 217.07/31.37 % (2583028)lrs-1011_4:1_sil=16000:si=on:bsr=on:random_seed=1873326325:cts=off:i=10938:bs=on:fsr=off:rtra=on_2726 on theBenchmark for (2726ds/10938Mi) % 217.07/31.37 % (2583029)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=unary_frequency:urr=on:bce=on:alpa=false:sac=on:random_seed=3896721740:i=4074:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:rtra=on:gtg=exists_all_2726 on theBenchmark for (2726ds/4074Mi) % 231.66/33.41 % (2583031)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:si=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=4165571581:st=-1:i=4220:kws=precedence:av=off:rtra=on:ss=axioms:er=known_2725 on theBenchmark for (2725ds/4220Mi) % 231.66/33.41 % Exception at run slice level % 231.66/33.41 User error: GNN currently only supports monomorphic FOL. % 231.66/33.41 % Exception at run slice level % 231.66/33.41 User error: GNN currently only supports monomorphic FOL. % 231.66/33.41 % (2583034)dis-1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:si=on:sp=unary_first:spb=goal:lcm=reverse:fd=off:flr=on:random_seed=1178011438:i=4860:add=off:aac=none:nm=16:rtra=on_2723 on theBenchmark for (2723ds/4860Mi) % 231.66/33.41 % (2583035)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=unary_first:spb=units:acc=on:bsr=unit_only:gs=on:sac=on:random_seed=2976460573:cond=fast:i=9782:rtra=on_2722 on theBenchmark for (2722ds/9782Mi) % 231.66/33.41 % Exception at run slice level % 231.66/33.41 User error: GNN currently only supports monomorphic FOL. % 231.66/33.41 % Exception at run slice level % 231.66/33.41 User error: GNN currently only supports monomorphic FOL. % 231.66/33.41 % (2583038)lrs+4_1_anc=all:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:si=on:sos=on:spb=goal_then_units:lcm=reverse:gs=on:s2agt=16:sac=on:newcnf=on:random_seed=3984940159:st=2:i=29690:sd=2:rtra=on:ss=included:fsd=on_2720 on theBenchmark for (2720ds/29690Mi) % 231.66/33.41 % (2582992)Instruction limit reached! % 231.66/33.41 % (2582992)------------------------------ % 231.66/33.41 % (2582992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.66/33.41 % (2582992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.66/33.41 % (2582992)CaDiCaL version: 2.1.3 % 231.66/33.41 % (2582992)Termination reason: Instruction limit % 231.66/33.41 % (2582992)Termination phase: Saturation % 231.66/33.41 % (2582992)Time elapsed: 3.106 s % 231.66/33.41 % (2582992)Peak memory usage: 178 MB % 231.66/33.41 % (2582992)Instructions burned: 12451 (million) % 231.66/33.41 % (2583039)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:si=on:urr=ec_only:br=off:random_seed=808463157:i=15068:sd=3:ins=1:rtra=on:gtg=exists_top:ss=included:sgt=8_2719 on theBenchmark for (2719ds/15068Mi) % 231.66/33.41 % (2583041)lrs-1002_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=ground:npcc=on:prc=on:fde=none:sims=off:si=on:spb=goal:bsr=unit_only:s2agt=32:random_seed=2936592285:cond=fast:i=20706:bs=on:av=off:rtra=on:ss=axioms:fsd=on:sgt=64:fsdmm=10_2719 on theBenchmark for (2719ds/20706Mi) % 231.66/33.41 % Exception at run slice level % 231.66/33.41 User error: GNN currently only supports monomorphic FOL. % 231.66/33.41 % Exception at run slice level % 231.66/33.41 User error: GNN currently only supports monomorphic FOL. % 231.66/33.41 % (2583044)lrs+2_4096_sil=8000:plsq=on:si=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=684083674:i=15720:rtra=on_2717 on theBenchmark for (2717ds/15720Mi) % 231.66/33.41 % Exception at run slice level % 231.66/33.41 User error: GNN currently only supports monomorphic FOL. % 231.66/33.41 % (2583046)ott+1011_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:fde=unused:si=on:spb=goal:lsd=30:lcm=predicate:fd=off:gs=on:sac=on:random_seed=255319820:i=15792:sd=2:bs=on:rtra=on:ss=included:sgt=20_2716 on theBenchmark for (2716ds/15792Mi) % 231.66/33.41 % (2583047)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:si=on:random_seed=1810133289:i=11624:gtgl=2:rtra=on:gtg=all_2716 on theBenchmark for (2716ds/11624Mi) % 231.66/33.41 % Exception at run slice level % 231.66/33.41 User error: GNN currently only supports monomorphic FOL. % 231.66/33.41 % Exception at run slice level % 231.66/33.41 User error: GNN currently only supports monomorphic FOL. % 231.66/33.41 % (2583050)ott-1011_1_anc=none:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:si=on:sp=const_frequency:sos=on:lsd=100:random_seed=3332536652:i=5930:s2at=3.7:aac=none:fgj=on:rtra=on:fdi=2:er=known_2713 on theBenchmark for (2713ds/5930Mi) % 231.66/33.41 % (2583051)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:si=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1268226306:i=5934:kws=precedence:bd=preordered:av=off:rtra=on_2713 on theBenchmark for (2713ds/5934Mi) % 231.66/33.41 % Exception at run slice level % 231.66/33.41 User error: GNN currently only supports monomorphic FOL. % 287.22/41.46 % Exception at run slice level % 287.22/41.46 User error: GNN currently only supports monomorphic FOL. % 287.22/41.46 % (2583054)ott+1002_1_anc=all:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:si=on:sos=on:spb=goal_then_units:alpa=false:sac=on:random_seed=305879845:i=6044:sd=1:kws=frequency:aac=none:ep=RST:nm=16:rtra=on:ss=axioms:er=known_2710 on theBenchmark for (2710ds/6044Mi) % 287.22/41.46 % (2583055)lrs-1010_1_ncem=casc2026/models/loop4.pt:sil=32000:tgt=ground:npcc=on:prc=on:si=on:sp=const_frequency:sos=all:lcm=predicate:acc=on:bsr=unit_only:gs=on:sac=on:newcnf=on:random_seed=2917991934:prac=on:i=6414:kws=frequency:fgj=on:rtra=on:ss=axioms:er=filter:sgt=8_2710 on theBenchmark for (2710ds/6414Mi) % 287.22/41.46 % Exception at run slice level % 287.22/41.46 User error: GNN currently only supports monomorphic FOL. % 287.22/41.46 % Exception at run slice level % 287.22/41.46 User error: GNN currently only supports monomorphic FOL. % 287.22/41.46 % (2583058)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:si=on:sos=on:lcm=predicate:random_seed=4022923433:st=4.2:i=6578:sd=5:aac=none:rtra=on:ss=included:sgt=10_2707 on theBenchmark for (2707ds/6578Mi) % 287.22/41.46 % (2583059)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:si=on:random_seed=2097914311:i=77138:sd=3:rtra=on:ss=axioms:sgt=32_2707 on theBenchmark for (2707ds/77138Mi) % 287.22/41.46 % Exception at run slice level % 287.22/41.46 User error: GNN currently only supports monomorphic FOL. % 287.22/41.46 % Exception at run slice level % 287.22/41.46 User error: GNN currently only supports monomorphic FOL. % 287.22/41.46 % (2583062)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:si=on:bsr=on:random_seed=2879109462:cts=off:i=6788:rtra=on_2704 on theBenchmark for (2704ds/6788Mi) % 287.22/41.46 % (2583063)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:si=on:sp=arity:spb=intro:lcm=reverse:urr=ec_only:fd=preordered:gs=on:sac=on:random_seed=2647240075:i=67648:bd=preordered:rtra=on_2704 on theBenchmark for (2704ds/67648Mi) % 287.22/41.46 % Exception at run slice level % 287.22/41.46 User error: GNN currently only supports monomorphic FOL. % 287.22/41.46 % Exception at run slice level % 287.22/41.46 User error: GNN currently only supports monomorphic FOL. % 287.22/41.46 % (2583066)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:si=on:random_seed=954983240:i=41368:bd=all:rtra=on:gtg=exists_sym_2701 on theBenchmark for (2701ds/41368Mi) % 287.22/41.46 % (2583067)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:irw=on:npcc=on:prc=on:bsd=on:si=on:sp=reverse_frequency:sos=on:erd=off:spb=goal:lcm=reverse:urr=full:bsr=on:s2agt=32:alpa=random:kmz=on:random_seed=2851320355:st=3:prac=on:i=14444:kws=arity_squared:add=on:fgj=on:bd=preordered:rtra=on:gtg=exists_top:gsp=on:ss=axioms:er=known:sgt=8:proc=on_2701 on theBenchmark for (2701ds/14444Mi) % 287.22/41.46 % (2583067)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 287.22/41.46 % Exception at run slice level % 287.22/41.46 User error: GNN currently only supports monomorphic FOL. % 287.22/41.46 % Exception at run slice level % 287.22/41.46 User error: GNN currently only supports monomorphic FOL. % 287.22/41.46 % (2583070)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:spb=goal_then_units:random_seed=2511994226:st=4:i=14590:sd=4:ep=R:rtra=on:ss=axioms_2698 on theBenchmark for (2698ds/14590Mi) % 287.22/41.46 % (2583071)lrs+32_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:fde=none:si=on:sp=occurrence:urr=ec_only:fd=preordered:random_seed=1374976663:i=8072:ins=10:rtra=on_2698 on theBenchmark for (2698ds/8072Mi) % 287.22/41.46 % Exception at run slice level % 287.22/41.46 User error: GNN currently only supports monomorphic FOL. % 287.22/41.46 % Exception at run slice level % 287.22/41.46 User error: GNN currently only supports monomorphic FOL. % 287.22/41.46 % (2583074)lrs+10_1_sil=128000:si=on:lcm=predicate:random_seed=1683546633:st=3:i=87394:sd=5:rtra=on:ss=axioms_2695 on theBenchmark for (2695ds/87394Mi) % 287.22/41.46 % (2583075)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:si=on:sp=const_frequency:sos=all:lcm=predicate:urr=on:s2agt=20:sac=on:random_seed=4234604307:i=35198:rtra=on:gtg=all:ss=axioms:fsd=on_2695 on theBenchmark for (2695ds/35198Mi) % 287.22/41.46 % Exception at run slice level % 287.22/41.46 User error: GNN currently only supports monomorphic FOL. % 287.22/41.46 % (2583078)lrs+1011_1_to=lpo:ncem=casc2026/modeTerminated % 300.52/43.33 % Vampire exiting % 300.52/43.34 Terminated %------------------------------------------------------------------------------