%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV755_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 : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:19:25 PM UTC 2026 % Result : Timeout 287.63s 41.24s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV755_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.20 % Computer : n003.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 12:28:27 UTC 2026 % 0.09/0.21 % CPUTime : % 0.09/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.24 Running first-order theorem proving % 0.09/0.24 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 5.37/1.69 % (1553478)Detected formulas, will run a generic FOF schedule. % 5.37/1.69 % (1553484)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=3476648989:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 5.37/1.69 % (1553488)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3396727134:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 5.37/1.69 % (1553485)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=4266913064:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 5.37/1.69 % (1553489)dis-21_1_sil=8000:lcm=predicate:random_seed=1434965955:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 5.37/1.69 % (1553483)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=1602980556:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 5.37/1.69 % (1553486)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2560687158:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 5.37/1.69 % (1553487)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2973317389:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 5.37/1.69 % (1553486)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.37/1.69 % (1553485)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.37/1.69 % (1553486)Refutation not found, incomplete strategy % 5.37/1.69 % (1553486)------------------------------ % 5.37/1.69 % (1553486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.37/1.69 % (1553486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.37/1.69 % (1553486)CaDiCaL version: 2.1.3 % 5.37/1.69 % (1553486)Termination reason: Refutation not found, incomplete strategy % 5.37/1.69 % (1553486)Time elapsed: 0.008 s % 5.37/1.69 % (1553486)Peak memory usage: 88 MB % 5.37/1.69 % (1553486)Instructions burned: 13 (million) % 5.37/1.69 % (1553487)Instruction limit reached! % 5.37/1.69 % (1553487)------------------------------ % 5.37/1.69 % (1553487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.37/1.69 % (1553487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.37/1.69 % (1553487)CaDiCaL version: 2.1.3 % 5.37/1.69 % (1553487)Termination reason: Instruction limit % 5.37/1.69 % (1553487)Termination phase: Saturation % 5.37/1.69 % (1553487)Time elapsed: 0.064 s % 5.37/1.69 % (1553487)Peak memory usage: 87 MB % 5.37/1.69 % (1553487)Instructions burned: 121 (million) % 5.37/1.69 % (1553489)Instruction limit reached! % 5.37/1.69 % (1553489)------------------------------ % 5.37/1.69 % (1553489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.37/1.69 % (1553489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.37/1.69 % (1553489)CaDiCaL version: 2.1.3 % 5.37/1.69 % (1553489)Termination reason: Instruction limit % 5.37/1.69 % (1553489)Termination phase: Saturation % 5.37/1.69 % (1553489)Time elapsed: 0.073 s % 5.37/1.69 % (1553489)Peak memory usage: 88 MB % 5.37/1.69 % (1553489)Instructions burned: 130 (million) % 5.37/1.69 % (1553488)Instruction limit reached! % 5.37/1.69 % (1553488)------------------------------ % 5.37/1.69 % (1553488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.37/1.69 % (1553488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.37/1.69 % (1553488)CaDiCaL version: 2.1.3 % 5.37/1.69 % (1553488)Termination reason: Instruction limit % 5.37/1.69 % (1553488)Termination phase: Saturation % 5.37/1.69 % (1553488)Time elapsed: 0.086 s % 5.37/1.69 % (1553488)Peak memory usage: 89 MB % 5.37/1.69 % (1553488)Instructions burned: 139 (million) % 5.37/1.69 % Exception at run slice level % 5.37/1.69 User error: GNN currently only supports monomorphic FOL. % 5.37/1.69 % (1553497)lrs+10_1_sil=8000:sp=occurrence:random_seed=4021108501:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 5.37/1.69 % (1553498)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2115395980:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 5.37/1.69 % (1553499)lrs+1011_1_sil=32000:sp=occurrence:random_seed=375634080:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 9.91/2.08 % (1553486)------------------------------ % 9.91/2.08 % (1553486)------------------------------ % 9.91/2.08 % (1553500)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=925766378:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi) % 9.91/2.08 % (1553498)Instruction limit reached! % 9.91/2.08 % (1553498)------------------------------ % 9.91/2.08 % (1553498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.91/2.08 % (1553498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.91/2.08 % (1553498)CaDiCaL version: 2.1.3 % 9.91/2.08 % (1553498)Termination reason: Instruction limit % 9.91/2.08 % (1553498)Termination phase: Saturation % 9.91/2.08 % (1553498)Time elapsed: 0.093 s % 9.91/2.08 % (1553498)Peak memory usage: 90 MB % 9.91/2.08 % (1553498)Instructions burned: 158 (million) % 9.91/2.08 % Exception at run slice level% Exception at run slice level % 9.91/2.08 % 9.91/2.08 User error: User error: GNN currently only supports monomorphic FOL.GNN currently only supports monomorphic FOL. % 9.91/2.08 % 9.91/2.08 % (1553497)Instruction limit reached! % 9.91/2.08 % (1553497)------------------------------ % 9.91/2.08 % (1553497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.91/2.08 % (1553497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.91/2.08 % (1553497)CaDiCaL version: 2.1.3 % 9.91/2.08 % (1553497)Termination reason: Instruction limit % 9.91/2.08 % (1553497)Termination phase: Saturation % 9.91/2.08 % (1553497)Time elapsed: 0.156 s % 9.91/2.08 % (1553497)Peak memory usage: 90 MB % 9.91/2.08 % (1553497)Instructions burned: 286 (million) % 9.91/2.08 % (1553500)Instruction limit reached! % 9.91/2.08 % (1553500)------------------------------ % 9.91/2.08 % (1553500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.91/2.08 % (1553500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.91/2.08 % (1553500)CaDiCaL version: 2.1.3 % 9.91/2.08 % (1553500)Termination reason: Instruction limit % 9.91/2.08 % (1553500)Termination phase: Saturation % 9.91/2.08 % (1553500)Time elapsed: 0.080 s % 9.91/2.08 % (1553500)Peak memory usage: 90 MB % 9.91/2.08 % (1553500)Instructions burned: 250 (million) % 9.91/2.08 % (1553504)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3053458463:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 9.91/2.08 % (1553504)Refutation not found, incomplete strategy % 9.91/2.08 % (1553504)------------------------------ % 9.91/2.08 % (1553504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.91/2.08 % (1553504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.91/2.08 % (1553504)CaDiCaL version: 2.1.3 % 9.91/2.08 % (1553504)Termination reason: Refutation not found, incomplete strategy % 9.91/2.08 % (1553504)Time elapsed: 0.017 s % 9.91/2.08 % (1553504)Peak memory usage: 88 MB % 9.91/2.08 % (1553504)Instructions burned: 28 (million) % 9.91/2.08 % (1553499)Instruction limit reached! % 9.91/2.08 % (1553499)------------------------------ % 9.91/2.08 % (1553499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.91/2.08 % (1553499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.91/2.08 % (1553499)CaDiCaL version: 2.1.3 % 9.91/2.08 % (1553499)Termination reason: Instruction limit % 9.91/2.08 % (1553499)Termination phase: Saturation % 9.91/2.08 % (1553499)Time elapsed: 0.192 s % 9.91/2.08 % (1553499)Peak memory usage: 91 MB % 9.91/2.08 % (1553499)Instructions burned: 327 (million) % 9.91/2.08 % (1553506)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=671658481:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 9.91/2.08 % (1553510)lrs+10_1_sil=8000:sp=occurrence:random_seed=1370604547:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 9.91/2.08 % (1553508)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=675494424:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 9.91/2.08 % (1553509)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2412478636:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 9.91/2.08 % (1553507)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1938047332:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 9.91/2.08 % (1553509)Instruction limit reached! % 11.57/2.41 % (1553509)------------------------------ % 11.57/2.41 % (1553509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.41 % (1553509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.41 % (1553509)CaDiCaL version: 2.1.3 % 11.57/2.41 % (1553509)Termination reason: Instruction limit % 11.57/2.41 % (1553509)Termination phase: Saturation % 11.57/2.41 % (1553509)Time elapsed: 0.057 s % 11.57/2.41 % (1553509)Peak memory usage: 88 MB % 11.57/2.41 % (1553509)Instructions burned: 114 (million) % 11.57/2.41 % (1553508)Instruction limit reached! % 11.57/2.41 % (1553508)------------------------------ % 11.57/2.41 % (1553508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.41 % (1553508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.41 % (1553508)CaDiCaL version: 2.1.3 % 11.57/2.41 % (1553508)Termination reason: Instruction limit % 11.57/2.41 % (1553508)Termination phase: Saturation % 11.57/2.41 % (1553508)Time elapsed: 0.061 s % 11.57/2.41 % (1553508)Peak memory usage: 88 MB % 11.57/2.41 % (1553508)Instructions burned: 128 (million) % 11.57/2.41 % (1553512)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1934441059:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi) % 11.57/2.41 % (1553507)Instruction limit reached! % 11.57/2.41 % (1553507)------------------------------ % 11.57/2.41 % (1553507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.41 % (1553507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.41 % (1553507)CaDiCaL version: 2.1.3 % 11.57/2.41 % (1553507)Termination reason: Instruction limit % 11.57/2.41 % (1553507)Termination phase: Saturation % 11.57/2.41 % (1553507)Time elapsed: 0.074 s % 11.57/2.41 % (1553507)Peak memory usage: 89 MB % 11.57/2.41 % (1553507)Instructions burned: 114 (million) % 11.57/2.41 % (1553512)Refutation not found, incomplete strategy % 11.57/2.41 % (1553512)------------------------------ % 11.57/2.41 % (1553512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.41 % (1553512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.41 % (1553512)CaDiCaL version: 2.1.3 % 11.57/2.41 % (1553512)Termination reason: Refutation not found, incomplete strategy % 11.57/2.41 % (1553512)Time elapsed: 0.019 s % 11.57/2.41 % (1553512)Peak memory usage: 89 MB % 11.57/2.41 % (1553512)Instructions burned: 32 (million) % 11.57/2.41 % (1553504)------------------------------ % 11.57/2.41 % (1553504)------------------------------ % 11.57/2.41 % (1553510)Instruction limit reached! % 11.57/2.41 % (1553510)------------------------------ % 11.57/2.41 % (1553510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.41 % (1553510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.41 % (1553510)CaDiCaL version: 2.1.3 % 11.57/2.41 % (1553510)Termination reason: Instruction limit % 11.57/2.41 % (1553510)Termination phase: Saturation % 11.57/2.41 % (1553510)Time elapsed: 0.267 s % 11.57/2.41 % (1553510)Peak memory usage: 93 MB % 11.57/2.41 % (1553510)Instructions burned: 912 (million) % 11.57/2.41 % (1553518)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3157690652:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi) % 11.57/2.41 % (1553519)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3352719852:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2992 on theBenchmark for (2992ds/134Mi) % 11.57/2.41 % (1553521)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3955351369:st=8:i=592:sd=3:ep=RST:ss=axioms_2992 on theBenchmark for (2992ds/592Mi) % 11.57/2.41 % (1553521)Refutation not found, incomplete strategy % 11.57/2.41 % (1553521)------------------------------ % 11.57/2.41 % (1553521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.41 % (1553521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.41 % (1553521)CaDiCaL version: 2.1.3 % 11.57/2.41 % (1553521)Termination reason: Refutation not found, incomplete strategy % 11.57/2.41 % (1553521)Time elapsed: 0.011 s % 11.57/2.41 % (1553521)Peak memory usage: 88 MB % 11.57/2.41 % (1553521)Instructions burned: 18 (million) % 11.57/2.41 % Exception at run slice level % 11.57/2.41 User error: GNN currently only supports monomorphic FOL. % 11.57/2.41 % (1553519)Instruction limit reached! % 11.57/2.41 % (1553519)------------------------------ % 11.57/2.41 % (1553519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.05/2.94 % (1553519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.05/2.94 % (1553519)CaDiCaL version: 2.1.3 % 13.05/2.94 % (1553519)Termination reason: Instruction limit % 13.05/2.94 % (1553519)Termination phase: Saturation % 13.05/2.94 % (1553519)Time elapsed: 0.082 s % 13.05/2.94 % (1553519)Peak memory usage: 90 MB % 13.05/2.94 % (1553519)Instructions burned: 135 (million) % 13.05/2.94 % (1553522)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3140976920:st=3:i=13193:sd=3:ss=axioms_2991 on theBenchmark for (2991ds/13193Mi) % 13.05/2.94 % (1553512)------------------------------ % 13.05/2.94 % (1553512)------------------------------ % 13.05/2.94 % (1553525)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=1450325687:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/125Mi) % 13.05/2.94 % (1553525)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.05/2.94 % (1553525)Instruction limit reached! % 13.05/2.94 % (1553525)------------------------------ % 13.05/2.94 % (1553525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.05/2.94 % (1553525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.05/2.94 % (1553525)CaDiCaL version: 2.1.3 % 13.05/2.94 % (1553525)Termination reason: Instruction limit % 13.05/2.94 % (1553525)Termination phase: Saturation % 13.05/2.94 % (1553525)Time elapsed: 0.043 s % 13.05/2.94 % (1553525)Peak memory usage: 90 MB % 13.05/2.94 % (1553525)Instructions burned: 128 (million) % 13.05/2.94 % (1553527)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1337374236:i=134:gtgl=5:slsql=off:gtg=exists_sym_2989 on theBenchmark for (2989ds/134Mi) % 13.05/2.94 % Exception at run slice level % 13.05/2.94 User error: Immediate (shared) subterms of term/literal aa(X1,X0,X3,sK0(X0,X1,X2,X3)) = sF2(X1,X0,X3,X2) have different types/not well-typed! % 13.05/2.94 % (1553528)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=95425414:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/141Mi) % 13.05/2.94 % (1553528)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.05/2.94 % (1553528)Refutation not found, incomplete strategy % 13.05/2.94 % (1553528)------------------------------ % 13.05/2.94 % (1553528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.05/2.94 % (1553528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.05/2.94 % (1553528)CaDiCaL version: 2.1.3 % 13.05/2.94 % (1553528)Termination reason: Refutation not found, incomplete strategy % 13.05/2.94 % (1553528)Time elapsed: 0.006 s % 13.05/2.94 % (1553528)Peak memory usage: 88 MB % 13.05/2.94 % (1553528)Instructions burned: 7 (million) % 13.05/2.94 % (1553530)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=48977827:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/431Mi) % 13.05/2.94 % (1553521)------------------------------ % 13.05/2.94 % (1553521)------------------------------ % 13.05/2.94 % (1553532)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=140538099:i=6060:aac=none:ins=25_2988 on theBenchmark for (2988ds/6060Mi) % 13.05/2.94 % Exception at run slice level % 13.05/2.94 User error: GNN currently only supports monomorphic FOL. % 13.05/2.94 % (1553534)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=3470163370:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2988 on theBenchmark for (2988ds/150Mi) % 13.05/2.94 % (1553534)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.05/2.94 % (1553537)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=830142751:i=14155:bd=all_2987 on theBenchmark for (2987ds/14155Mi) % 13.05/2.94 % Exception at run slice level % 13.05/2.94 User error: GNN currently only supports monomorphic FOL. % 13.05/2.94 % (1553530)Instruction limit reached! % 13.05/2.94 % (1553530)------------------------------ % 13.05/2.94 % (1553530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.05/2.94 % (1553530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.71/4.19 % (1553530)CaDiCaL version: 2.1.3 % 24.71/4.19 % (1553530)Termination reason: Instruction limit % 24.71/4.19 % (1553530)Termination phase: Saturation % 24.71/4.19 % (1553530)Time elapsed: 0.208 s % 24.71/4.19 % (1553530)Peak memory usage: 90 MB % 24.71/4.19 % (1553530)Instructions burned: 432 (million) % 24.71/4.19 % (1553534)Instruction limit reached! % 24.71/4.19 % (1553534)------------------------------ % 24.71/4.19 % (1553534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.71/4.19 % (1553534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.71/4.19 % (1553534)CaDiCaL version: 2.1.3 % 24.71/4.19 % (1553534)Termination reason: Instruction limit % 24.71/4.19 % (1553534)Termination phase: Saturation % 24.71/4.19 % (1553534)Time elapsed: 0.093 s % 24.71/4.19 % (1553534)Peak memory usage: 90 MB % 24.71/4.19 % (1553534)Instructions burned: 150 (million) % 24.71/4.19 % Exception at run slice level % 24.71/4.19 User error: GNN currently only supports monomorphic FOL. % 24.71/4.19 % (1553528)------------------------------ % 24.71/4.19 % (1553528)------------------------------ % 24.71/4.19 % (1553539)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=4180171416:i=667:av=off:fsr=off_2987 on theBenchmark for (2987ds/667Mi) % 24.71/4.19 % (1553545)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1071051537:i=12111:sd=1:ss=included_2985 on theBenchmark for (2985ds/12111Mi) % 24.71/4.19 % (1553543)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2893018569:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2986 on theBenchmark for (2986ds/193Mi) % 24.71/4.19 % (1553542)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=3960249591:s2a=on:i=185:s2at=1.8:fdi=4_2986 on theBenchmark for (2986ds/185Mi) % 24.71/4.19 % (1553544)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1819113089:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2985 on theBenchmark for (2985ds/4850Mi) % 24.71/4.19 % (1553546)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2178787900:i=319:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/319Mi) % 24.71/4.19 % (1553539)Refutation not found, incomplete strategy % 24.71/4.19 % (1553539)------------------------------ % 24.71/4.19 % (1553539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.71/4.19 % (1553539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.71/4.19 % (1553539)CaDiCaL version: 2.1.3 % 24.71/4.19 % (1553539)Termination reason: Refutation not found, incomplete strategy % 24.71/4.19 % (1553539)Time elapsed: 0.139 s % 24.71/4.19 % (1553539)Peak memory usage: 89 MB % 24.71/4.19 % (1553539)Instructions burned: 277 (million) % 24.71/4.19 % (1553543)Instruction limit reached! % 24.71/4.19 % (1553543)------------------------------ % 24.71/4.19 % (1553543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.71/4.19 % (1553543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.71/4.19 % (1553543)CaDiCaL version: 2.1.3 % 24.71/4.19 % (1553543)Termination reason: Instruction limit % 24.71/4.19 % (1553543)Termination phase: Saturation % 24.71/4.19 % (1553543)Time elapsed: 0.103 s % 24.71/4.19 % (1553543)Peak memory usage: 91 MB % 24.71/4.19 % (1553543)Instructions burned: 194 (million) % 24.71/4.19 % (1553542)Instruction limit reached! % 24.71/4.19 % (1553542)------------------------------ % 24.71/4.19 % (1553542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.71/4.19 % (1553542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.71/4.19 % (1553542)CaDiCaL version: 2.1.3 % 24.71/4.19 % (1553542)Termination reason: Instruction limit % 24.71/4.19 % (1553542)Termination phase: Saturation % 24.71/4.19 % (1553542)Time elapsed: 0.117 s % 24.71/4.19 % (1553542)Peak memory usage: 90 MB % 24.71/4.19 % (1553542)Instructions burned: 185 (million) % 24.71/4.19 % Exception at run slice level % 24.71/4.19 User error: GNN currently only supports monomorphic FOL. % 24.71/4.19 % (1553546)Instruction limit reached! % 24.71/4.19 % (1553546)------------------------------ % 24.71/4.19 % (1553546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.71/4.19 % (1553546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.71/4.19 % (1553546)CaDiCaL version: 2.1.3 % 24.71/4.19 % (1553546)Termination reason: Instruction limit % 24.71/4.19 % (1553546)Termination phase: Saturation % 31.69/5.18 % (1553546)Time elapsed: 0.141 s % 31.69/5.18 % (1553546)Peak memory usage: 90 MB % 31.69/5.18 % (1553546)Instructions burned: 321 (million) % 31.69/5.18 % Exception at run slice level % 31.69/5.18 User error: GNN currently only supports monomorphic FOL. % 31.69/5.18 % (1553553)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2752803994:i=2064:ep=RST_2983 on theBenchmark for (2983ds/2064Mi) % 31.69/5.18 % (1553553)Refutation not found, incomplete strategy % 31.69/5.18 % (1553553)------------------------------ % 31.69/5.18 % (1553553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.69/5.18 % (1553553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.69/5.18 % (1553553)CaDiCaL version: 2.1.3 % 31.69/5.18 % (1553553)Termination reason: Refutation not found, incomplete strategy % 31.69/5.18 % (1553553)Time elapsed: 0.012 s % 31.69/5.18 % (1553553)Peak memory usage: 88 MB % 31.69/5.18 % (1553553)Instructions burned: 19 (million) % 31.69/5.18 % (1553554)dis-1011_128_sil=32000:random_seed=3970438419:i=3706:ep=RST:av=off_2983 on theBenchmark for (2983ds/3706Mi) % 31.69/5.18 % (1553555)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=463282070:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2982 on theBenchmark for (2982ds/757Mi) % 31.69/5.18 % (1553539)------------------------------ % 31.69/5.18 % (1553539)------------------------------ % 31.69/5.18 % (1553555)Refutation not found, incomplete strategy % 31.69/5.18 % (1553555)------------------------------ % 31.69/5.18 % (1553555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.69/5.18 % (1553555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.69/5.18 % (1553555)CaDiCaL version: 2.1.3 % 31.69/5.18 % (1553555)Termination reason: Refutation not found, incomplete strategy % 31.69/5.18 % (1553555)Time elapsed: 0.015 s % 31.69/5.18 % (1553555)Peak memory usage: 89 MB % 31.69/5.18 % (1553555)Instructions burned: 49 (million) % 31.69/5.18 % (1553556)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3333383664:i=13913:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/13913Mi) % 31.69/5.18 % (1553557)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3500682792:i=9925:aac=none_2982 on theBenchmark for (2982ds/9925Mi) % 31.69/5.18 % (1553555)------------------------------ % 31.69/5.18 % (1553555)------------------------------ % 31.69/5.18 % (1553561)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4285093030:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2981 on theBenchmark for (2981ds/2479Mi) % 31.69/5.18 % (1553561)Refutation not found, incomplete strategy % 31.69/5.18 % (1553561)------------------------------ % 31.69/5.18 % (1553561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.69/5.18 % (1553561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.69/5.18 % (1553561)CaDiCaL version: 2.1.3 % 31.69/5.18 % (1553561)Termination reason: Refutation not found, incomplete strategy % 31.69/5.18 % (1553561)Time elapsed: 0.012 s % 31.69/5.18 % (1553561)Peak memory usage: 89 MB % 31.69/5.18 % (1553561)Instructions burned: 19 (million) % 31.69/5.18 % (1553553)------------------------------ % 31.69/5.18 % (1553553)------------------------------ % 31.69/5.18 % (1553564)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3554475086:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/440Mi) % 31.69/5.18 % (1553564)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 31.69/5.18 % (1553566)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4290136461:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2979 on theBenchmark for (2979ds/11145Mi) % 31.69/5.18 % Exception at run slice level % 31.69/5.18 User error: GNN currently only supports monomorphic FOL. % 31.69/5.18 % (1553564)Instruction limit reached! % 31.69/5.18 % (1553564)------------------------------ % 31.69/5.18 % (1553564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.69/5.18 % (1553564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.69/5.18 % (1553564)CaDiCaL version: 2.1.3 % 31.69/5.18 % (1553564)Termination reason: Instruction limit % 31.69/5.18 % (1553564)Termination phase: Saturation % 31.69/5.18 % (1553564)Time elapsed: 0.123 s % 31.69/5.18 % (1553564)Peak memory usage: 92 MB % 31.69/5.18 % (1553564)Instructions burned: 444 (million) % 39.19/6.26 % Exception at run slice level % 39.19/6.26 User error: GNN currently only supports monomorphic FOL. % 39.19/6.26 % (1553561)------------------------------ % 39.19/6.26 % (1553561)------------------------------ % 39.19/6.26 % (1553570)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3527194022:st=2:s2a=on:i=524:s2at=2:ss=axioms_2977 on theBenchmark for (2977ds/524Mi) % 39.19/6.26 % (1553569)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=176348813:cts=off:i=3034:av=off:er=known:fsd=on_2977 on theBenchmark for (2977ds/3034Mi) % 39.19/6.26 % (1553571)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1278304980:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2977 on theBenchmark for (2977ds/1016Mi) % 39.19/6.26 % (1553572)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1844736798:i=14123:bd=preordered:ins=4_2977 on theBenchmark for (2977ds/14123Mi) % 39.19/6.26 % (1553570)Instruction limit reached! % 39.19/6.26 % (1553570)------------------------------ % 39.19/6.26 % (1553570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.19/6.26 % (1553570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.19/6.26 % (1553570)CaDiCaL version: 2.1.3 % 39.19/6.26 % (1553570)Termination reason: Instruction limit % 39.19/6.26 % (1553570)Termination phase: Saturation % 39.19/6.26 % (1553570)Time elapsed: 0.150 s % 39.19/6.26 % (1553570)Peak memory usage: 94 MB % 39.19/6.26 % (1553570)Instructions burned: 528 (million) % 39.19/6.26 % Exception at run slice level % 39.19/6.26 User error: GNN currently only supports monomorphic FOL. % 39.19/6.26 % (1553577)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=814532707:i=5781:kws=precedence:bd=all:rawr=on_2974 on theBenchmark for (2974ds/5781Mi) % 39.19/6.26 % (1553578)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=952419005:i=2448:gtgl=5:bd=preordered:gtg=all_2974 on theBenchmark for (2974ds/2448Mi) % 39.19/6.26 % Exception at run slice level % 39.19/6.26 User error: GNN currently only supports monomorphic FOL. % 39.19/6.26 % Exception at run slice level % 39.19/6.26 User error: GNN currently only supports monomorphic FOL. % 39.19/6.26 % (1553581)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=4167331201:i=3223:kws=precedence:fgj=on:av=off_2972 on theBenchmark for (2972ds/3223Mi) % 39.19/6.26 % (1553571)Instruction limit reached! % 39.19/6.26 % (1553571)------------------------------ % 39.19/6.26 % (1553571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.19/6.26 % (1553571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.19/6.26 % (1553571)CaDiCaL version: 2.1.3 % 39.19/6.26 % (1553571)Termination reason: Instruction limit % 39.19/6.26 % (1553571)Termination phase: Saturation % 39.19/6.26 % (1553571)Time elapsed: 0.539 s % 39.19/6.26 % (1553571)Peak memory usage: 101 MB % 39.19/6.26 % (1553571)Instructions burned: 1017 (million) % 39.19/6.26 % (1553582)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2276119306:st=5.6:i=2033:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/2033Mi) % 39.19/6.26 % Exception at run slice level % 39.19/6.26 User error: GNN currently only supports monomorphic FOL. % 39.19/6.26 % (1553584)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2228841910:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2970 on theBenchmark for (2970ds/2055Mi) % 39.19/6.26 % (1553586)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=2374967927:i=21611:sd=3:ss=axioms_2968 on theBenchmark for (2968ds/21611Mi) % 39.19/6.26 % Exception at run slice level % 39.19/6.26 User error: GNN currently only supports monomorphic FOL. % 39.19/6.26 % Exception at run slice level % 39.19/6.26 User error: GNN currently only supports monomorphic FOL. % 39.19/6.26 % (1553589)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3041601570:i=4835:sd=13:ss=axioms:sgt=23_2967 on theBenchmark for (2967ds/4835Mi) % 39.19/6.26 % Exception at run slice level % 39.19/6.26 User error: GNN currently only supports monomorphic FOL. % 39.19/6.26 % (1553590)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=236453072:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2966 on theBenchmark for (2966ds/797Mi) % 48.16/7.50 % Exception at run slice level % 48.16/7.50 User error: GNN currently only supports monomorphic FOL. % 48.16/7.50 % (1553592)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1436350386:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2965 on theBenchmark for (2965ds/2326Mi) % 48.16/7.50 % (1553554)Instruction limit reached! % 48.16/7.50 % (1553554)------------------------------ % 48.16/7.50 % (1553554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.16/7.50 % (1553554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.16/7.50 % (1553554)CaDiCaL version: 2.1.3 % 48.16/7.50 % (1553554)Termination reason: Instruction limit % 48.16/7.50 % (1553554)Termination phase: Saturation % 48.16/7.50 % (1553554)Time elapsed: 1.898 s % 48.16/7.50 % (1553554)Peak memory usage: 120 MB % 48.16/7.50 % (1553554)Instructions burned: 3706 (million) % 48.16/7.50 % (1553594)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3184277392:i=6038:nm=6_2963 on theBenchmark for (2963ds/6038Mi) % 48.16/7.50 % (1553596)lrs+10_1_sil=32000:sp=occurrence:random_seed=3305398239:st=2:i=33334:sd=3:ss=included:sgt=32_2962 on theBenchmark for (2962ds/33334Mi) % 48.16/7.50 % (1553590)Instruction limit reached! % 48.16/7.50 % (1553590)------------------------------ % 48.16/7.50 % (1553590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.16/7.50 % (1553590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.16/7.50 % (1553590)CaDiCaL version: 2.1.3 % 48.16/7.50 % (1553590)Termination reason: Instruction limit % 48.16/7.50 % (1553590)Termination phase: Saturation % 48.16/7.50 % (1553590)Time elapsed: 0.491 s % 48.16/7.50 % (1553590)Peak memory usage: 101 MB % 48.16/7.50 % (1553590)Instructions burned: 798 (million) % 48.16/7.50 % (1553577)Instruction limit reached! % 48.16/7.50 % (1553577)------------------------------ % 48.16/7.50 % (1553577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.16/7.50 % (1553577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.16/7.50 % (1553577)CaDiCaL version: 2.1.3 % 48.16/7.50 % (1553577)Termination reason: Instruction limit % 48.16/7.50 % (1553577)Termination phase: Saturation % 48.16/7.50 % (1553577)Time elapsed: 1.412 s % 48.16/7.50 % (1553577)Peak memory usage: 104 MB % 48.16/7.50 % (1553577)Instructions burned: 5786 (million) % 48.16/7.50 % Exception at run slice level % 48.16/7.50 User error: GNN currently only supports monomorphic FOL. % 48.16/7.50 % (1553599)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1519811426:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2960 on theBenchmark for (2960ds/1008Mi) % 48.16/7.50 % (1553600)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=302964517:i=8327:s2at=5:bd=preordered_2959 on theBenchmark for (2959ds/8327Mi) % 48.16/7.50 % (1553544)Instruction limit reached! % 48.16/7.50 % (1553544)------------------------------ % 48.16/7.50 % (1553544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.16/7.50 % (1553544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.16/7.50 % (1553544)CaDiCaL version: 2.1.3 % 48.16/7.50 % (1553544)Termination reason: Instruction limit % 48.16/7.50 % (1553544)Termination phase: Saturation % 48.16/7.50 % (1553544)Time elapsed: 2.754 s % 48.16/7.50 % (1553544)Peak memory usage: 125 MB % 48.16/7.50 % (1553544)Instructions burned: 4851 (million) % 48.16/7.50 % (1553601)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=2526942935:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2958 on theBenchmark for (2958ds/1083Mi) % 48.16/7.50 % Exception at run slice level % 48.16/7.50 User error: GNN currently only supports monomorphic FOL. % 48.16/7.50 % (1553605)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2025063498:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2956 on theBenchmark for (2956ds/1084Mi) % 48.16/7.50 % (1553606)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1626321013:i=6995:s2at=5:gtg=all_2956 on theBenchmark for (2956ds/6995Mi) % 56.40/8.70 % (1553599)Instruction limit reached! % 56.40/8.70 % (1553599)------------------------------ % 56.40/8.70 % (1553599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.40/8.70 % (1553599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.40/8.70 % (1553599)CaDiCaL version: 2.1.3 % 56.40/8.70 % (1553599)Termination reason: Instruction limit % 56.40/8.70 % (1553599)Termination phase: Saturation % 56.40/8.70 % (1553599)Time elapsed: 0.438 s % 56.40/8.70 % (1553599)Peak memory usage: 93 MB % 56.40/8.70 % (1553599)Instructions burned: 1010 (million) % 56.40/8.70 % Exception at run slice level % 56.40/8.70 User error: GNN currently only supports monomorphic FOL. % 56.40/8.70 % (1553609)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=318332818:st=2:i=6225:sd=15:ss=axioms_2954 on theBenchmark for (2954ds/6225Mi) % 56.40/8.70 % (1553610)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3222912337:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2953 on theBenchmark for (2953ds/3372Mi) % 56.40/8.70 % (1553601)Instruction limit reached! % 56.40/8.70 % (1553601)------------------------------ % 56.40/8.70 % (1553601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.40/8.70 % (1553601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.40/8.70 % (1553601)CaDiCaL version: 2.1.3 % 56.40/8.70 % (1553601)Termination reason: Instruction limit % 56.40/8.70 % (1553601)Termination phase: Saturation % 56.40/8.70 % (1553601)Time elapsed: 0.550 s % 56.40/8.70 % (1553601)Peak memory usage: 97 MB % 56.40/8.70 % (1553601)Instructions burned: 1085 (million) % 56.40/8.70 % Exception at run slice level % 56.40/8.70 User error: GNN currently only supports monomorphic FOL. % 56.40/8.70 % (1553613)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=482975964:st=2.3:i=26457:sd=10:ss=included:sgt=8_2951 on theBenchmark for (2951ds/26457Mi) % 56.40/8.70 % (1553605)Instruction limit reached! % 56.40/8.70 % (1553605)------------------------------ % 56.40/8.70 % (1553605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.40/8.70 % (1553605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.40/8.70 % (1553605)CaDiCaL version: 2.1.3 % 56.40/8.70 % (1553605)Termination reason: Instruction limit % 56.40/8.70 % (1553605)Termination phase: Saturation % 56.40/8.70 % (1553605)Time elapsed: 0.586 s % 56.40/8.70 % (1553605)Peak memory usage: 97 MB % 56.40/8.70 % (1553605)Instructions burned: 1085 (million) % 56.40/8.70 % (1553614)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=2987358585:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2949 on theBenchmark for (2949ds/13494Mi) % 56.40/8.70 % (1553592)Instruction limit reached! % 56.40/8.70 % (1553592)------------------------------ % 56.40/8.70 % (1553592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.40/8.70 % (1553592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.40/8.70 % (1553592)CaDiCaL version: 2.1.3 % 56.40/8.70 % (1553592)Termination reason: Instruction limit % 56.40/8.70 % (1553592)Termination phase: Saturation % 56.40/8.70 % (1553592)Time elapsed: 1.483 s % 56.40/8.70 % (1553592)Peak memory usage: 108 MB % 56.40/8.70 % (1553592)Instructions burned: 2327 (million) % 56.40/8.70 % (1553616)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=1742067239:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2949 on theBenchmark for (2949ds/2503Mi) % 56.40/8.70 % (1553616)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 56.40/8.70 % (1553618)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=120916733:i=2559:sd=1:ep=RSTC:ss=axioms_2948 on theBenchmark for (2948ds/2559Mi) % 56.40/8.70 % Exception at run slice level % 56.40/8.70 User error: GNN currently only supports monomorphic FOL. % 56.40/8.70 % Exception at run slice level % 56.40/8.70 User error: GNN currently only supports monomorphic FOL. % 56.40/8.70 % (1553621)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3946025717:i=30753:av=off:ss=included_2946 on theBenchmark for (2946ds/30753Mi) % 56.40/8.70 % Exception at run slice level % 56.40/8.70 User error: GNN currently only supports monomorphic FOL. % 56.40/8.70 % (1553622)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=1892143529:i=26473:ep=RSTC_2945 on theBenchmark for (2945ds/26473Mi) % 66.65/10.19 % Exception at run slice level % 66.65/10.19 User error: GNN currently only supports monomorphic FOL. % 66.65/10.19 % Exception at run slice level % 66.65/10.19 User error: GNN currently only supports monomorphic FOL. % 66.65/10.19 % (1553624)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=2052225237:cts=off:i=2759:kws=inv_arity:fgj=on_2944 on theBenchmark for (2944ds/2759Mi) % 66.65/10.19 % (1553626)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=2563347197:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2943 on theBenchmark for (2943ds/5665Mi) % 66.65/10.19 % (1553626)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 66.65/10.19 % (1553627)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=1840742344:i=1532:ep=RS:ss=axioms_2943 on theBenchmark for (2943ds/1532Mi) % 66.65/10.19 % Exception at run slice level % 66.65/10.19 User error: GNN currently only supports monomorphic FOL. % 66.65/10.19 % (1553631)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=1404972475:i=1565:sd=2:ss=axioms:sgt=32_2940 on theBenchmark for (2940ds/1565Mi) % 66.65/10.19 % Exception at run slice level % 66.65/10.19 User error: GNN currently only supports monomorphic FOL. % 66.65/10.19 % Exception at run slice level % 66.65/10.19 User error: GNN currently only supports monomorphic FOL. % 66.65/10.19 % (1553633)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=3371295147:i=1572:fgj=on:gsp=on_2939 on theBenchmark for (2939ds/1572Mi) % 66.65/10.19 % (1553633)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 66.65/10.19 % Exception at run slice level % 66.65/10.19 User error: GNN currently only supports monomorphic FOL. % 66.65/10.19 % (1553589)Instruction limit reached! % 66.65/10.19 % (1553589)------------------------------ % 66.65/10.19 % (1553589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.65/10.19 % (1553589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.65/10.19 % (1553589)CaDiCaL version: 2.1.3 % 66.65/10.19 % (1553589)Termination reason: Instruction limit % 66.65/10.19 % (1553589)Termination phase: Saturation % 66.65/10.19 % (1553589)Time elapsed: 2.854 s % 66.65/10.19 % (1553589)Peak memory usage: 113 MB % 66.65/10.19 % (1553589)Instructions burned: 4836 (million) % 66.65/10.19 % (1553634)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=1955050247:i=6052:sd=4:ss=axioms:sgt=24_2938 on theBenchmark for (2938ds/6052Mi) % 66.65/10.19 % (1553636)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=1284269099:i=3500:sd=1:bd=preordered:sup=off:ss=included_2937 on theBenchmark for (2937ds/3500Mi) % 66.65/10.19 % (1553637)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=4013567799:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2937 on theBenchmark for (2937ds/1842Mi) % 66.65/10.19 % (1553637)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 66.65/10.19 % Exception at run slice level % 66.65/10.19 User error: GNN currently only supports monomorphic FOL. % 66.65/10.19 % Exception at run slice level % 66.65/10.19 User error: GNN currently only supports monomorphic FOL. % 66.65/10.19 % (1553641)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=476548594:i=66096:add=on_2934 on theBenchmark for (2934ds/66096Mi) % 66.65/10.19 % Exception at run slice level % 66.65/10.19 User error: GNN currently only supports monomorphic FOL. % 66.65/10.19 % (1553642)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=3685415136:i=1884:sd=1:nm=60:ss=axioms_2933 on theBenchmark for (2933ds/1884Mi) % 66.65/10.19 % Exception at run slice level % 66.65/10.19 User error: GNN currently only supports monomorphic FOL. % 77.36/11.60 % (1553644)lrs-1011_4:1_sil=16000:bsr=on:random_seed=2894778701:cts=off:i=5469:bs=on:fsr=off_2932 on theBenchmark for (2932ds/5469Mi) % 77.36/11.60 % Exception at run slice level % 77.36/11.60 User error: GNN currently only supports monomorphic FOL. % 77.36/11.60 % (1553646)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=2889028263:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2931 on theBenchmark for (2931ds/2037Mi) % 77.36/11.60 % (1553648)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2837467386:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2930 on theBenchmark for (2930ds/2110Mi) % 77.36/11.60 % Exception at run slice level % 77.36/11.60 User error: GNN currently only supports monomorphic FOL. % 77.36/11.60 % Exception at run slice level % 77.36/11.60 User error: GNN currently only supports monomorphic FOL. % 77.36/11.60 % (1553651)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=3077397198:i=2430:add=off:aac=none:nm=16_2928 on theBenchmark for (2928ds/2430Mi) % 77.36/11.60 % Exception at run slice level % 77.36/11.60 User error: GNN currently only supports monomorphic FOL. % 77.36/11.60 % (1553652)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=3801209034:cond=fast:i=4891_2927 on theBenchmark for (2927ds/4891Mi) % 77.36/11.60 % (1553654)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=1237265865:st=2:i=14845:sd=2:ss=included:fsd=on_2926 on theBenchmark for (2926ds/14845Mi) % 77.36/11.60 % Exception at run slice level % 77.36/11.60 User error: GNN currently only supports monomorphic FOL. % 77.36/11.60 % Exception at run slice level % 77.36/11.60 User error: GNN currently only supports monomorphic FOL. % 77.36/11.60 % (1553657)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=841601581:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2924 on theBenchmark for (2924ds/7534Mi) % 77.36/11.60 % (1553658)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=2970568529:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2923 on theBenchmark for (2923ds/10353Mi) % 77.36/11.60 % (1553609)Instruction limit reached! % 77.36/11.60 % (1553609)------------------------------ % 77.36/11.60 % (1553609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.36/11.60 % (1553609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.36/11.60 % (1553609)CaDiCaL version: 2.1.3 % 77.36/11.60 % (1553609)Termination reason: Instruction limit % 77.36/11.60 % (1553609)Termination phase: Saturation % 77.36/11.60 % (1553609)Time elapsed: 3.081 s % 77.36/11.60 % (1553609)Peak memory usage: 145 MB % 77.36/11.60 % (1553609)Instructions burned: 6227 (million) % 77.36/11.60 % Exception at run slice level % 77.36/11.60 User error: GNN currently only supports monomorphic FOL. % 77.36/11.60 % Exception at run slice level % 77.36/11.60 User error: GNN currently only supports monomorphic FOL. % 77.36/11.60 % (1553661)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=787629781:i=7860_2921 on theBenchmark for (2921ds/7860Mi) % 77.36/11.60 % (1553661)Refutation not found, incomplete strategy % 77.36/11.60 % (1553661)------------------------------ % 77.36/11.60 % (1553661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.36/11.60 % (1553661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.36/11.60 % (1553661)CaDiCaL version: 2.1.3 % 77.36/11.60 % (1553661)Termination reason: Refutation not found, incomplete strategy % 77.36/11.60 % (1553661)Time elapsed: 0.018 s % 77.36/11.60 % (1553661)Peak memory usage: 89 MB % 77.36/11.60 % (1553661)Instructions burned: 30 (million) % 77.36/11.60 % (1553663)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1438947388:i=5812:gtgl=2:gtg=all_2921 on theBenchmark for (2921ds/5812Mi) % 77.36/11.60 % (1553662)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=784832133:i=7896:sd=2:bs=on:ss=included:sgt=20_2921 on theBenchmark for (2921ds/7896Mi) % 100.79/15.03 % Exception at run slice level % 100.79/15.03 User error: GNN currently only supports monomorphic FOL. % 100.79/15.03 % Exception at run slice level % 100.79/15.03 User error: GNN currently only supports monomorphic FOL. % 100.79/15.03 % (1553661)------------------------------ % 100.79/15.03 % (1553661)------------------------------ % 100.79/15.03 % (1553668)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=2884453439:i=2967:kws=precedence:bd=preordered:av=off_2917 on theBenchmark for (2917ds/2967Mi) % 100.79/15.03 % (1553667)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=1361900480:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2918 on theBenchmark for (2918ds/2965Mi) % 100.79/15.03 % Exception at run slice level % 100.79/15.03 User error: GNN currently only supports monomorphic FOL. % 100.79/15.03 % (1553669)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=4265300024:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2917 on theBenchmark for (2917ds/3022Mi) % 100.79/15.03 % Exception at run slice level % 100.79/15.03 User error: GNN currently only supports monomorphic FOL. % 100.79/15.03 % (1553672)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=3193445411:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2916 on theBenchmark for (2916ds/3207Mi) % 100.79/15.03 % (1553674)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=2574912279:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2914 on theBenchmark for (2914ds/3289Mi) % 100.79/15.03 % Exception at run slice level % 100.79/15.03 User error: GNN currently only supports monomorphic FOL. % 100.79/15.03 % Exception at run slice level % 100.79/15.03 User error: GNN currently only supports monomorphic FOL. % 100.79/15.03 % Exception at run slice level % 100.79/15.03 User error: GNN currently only supports monomorphic FOL. % 100.79/15.03 % (1553677)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=2231723566:i=38569:sd=3:ss=axioms:sgt=32_2913 on theBenchmark for (2913ds/38569Mi) % 100.79/15.03 % Exception at run slice level % 100.79/15.03 User error: GNN currently only supports monomorphic FOL. % 100.79/15.03 % (1553678)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=2422038730:cts=off:i=3394_2912 on theBenchmark for (2912ds/3394Mi) % 100.79/15.03 % (1553680)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=2958094860:i=33824:bd=preordered_2911 on theBenchmark for (2911ds/33824Mi) % 100.79/15.03 % (1553681)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=832746211:i=20684:bd=all:gtg=exists_sym_2910 on theBenchmark for (2910ds/20684Mi) % 100.79/15.03 % Exception at run slice level % 100.79/15.03 User error: GNN currently only supports monomorphic FOL. % 100.79/15.03 % Exception at run slice level % 100.79/15.03 User error: GNN currently only supports monomorphic FOL. % 100.79/15.03 % Exception at run slice level % 100.79/15.03 User error: GNN currently only supports monomorphic FOL. % 100.79/15.03 % (1553685)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=2155704986: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_2908 on theBenchmark for (2908ds/7222Mi) % 100.79/15.03 % (1553685)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 100.79/15.03 % (1553686)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=453603610:st=4:i=7295:sd=4:ep=R:ss=axioms_2907 on theBenchmark for (2907ds/7295Mi) % 100.79/15.03 % Exception at run slice level % 100.79/15.03 User error: GNN currently only supports monomorphic FOL. % 100.79/15.03 % (1553688)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=2595746145:i=4036:ins=10_2906 on theBenchmark for (2906ds/4036Mi) % 100.79/15.03 % Exception at run slice level % 100.79/15.03 User error: GNN currently only supports monomorphic FOL. % 131.41/19.21 % (1553690)lrs+10_1_sil=128000:lcm=predicate:random_seed=3278625336:st=3:i=43697:sd=5:ss=axioms_2905 on theBenchmark for (2905ds/43697Mi) % 131.41/19.21 % (1553692)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=445300734:i=17599:gtg=all:ss=axioms:fsd=on_2904 on theBenchmark for (2904ds/17599Mi) % 131.41/19.21 % Exception at run slice level % 131.41/19.21 User error: GNN currently only supports monomorphic FOL. % 131.41/19.21 % (1553644)Instruction limit reached! % 131.41/19.21 % (1553644)------------------------------ % 131.41/19.21 % (1553644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.41/19.21 % (1553644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.41/19.21 % (1553644)CaDiCaL version: 2.1.3 % 131.41/19.21 % (1553644)Termination reason: Instruction limit % 131.41/19.21 % (1553644)Termination phase: Saturation % 131.41/19.21 % (1553644)Time elapsed: 2.895 s % 131.41/19.21 % (1553644)Peak memory usage: 102 MB % 131.41/19.21 % (1553644)Instructions burned: 5471 (million) % 131.41/19.21 % Exception at run slice level % 131.41/19.21 User error: GNN currently only supports monomorphic FOL. % 131.41/19.21 % Exception at run slice level % 131.41/19.21 User error: GNN currently only supports monomorphic FOL. % 131.41/19.21 % (1553695)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=354896203:i=4547:bd=preordered_2902 on theBenchmark for (2902ds/4547Mi) % 131.41/19.21 % (1553696)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=552058788:i=9294:av=off_2902 on theBenchmark for (2902ds/9294Mi) % 131.41/19.21 % (1553698)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2526446239:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2901 on theBenchmark for (2901ds/4793Mi) % 131.41/19.21 % (1553697)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3701244931:i=32849:add=on_2901 on theBenchmark for (2901ds/32849Mi) % 131.41/19.21 % Exception at run slice level % 131.41/19.21 User error: GNN currently only supports monomorphic FOL. % 131.41/19.21 % Exception at run slice level % 131.41/19.21 User error: GNN currently only supports monomorphic FOL. % 131.41/19.21 % Exception at run slice level % 131.41/19.21 User error: GNN currently only supports monomorphic FOL. % 131.41/19.21 % (1553703)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=78600244:i=4840:nm=4:av=off_2898 on theBenchmark for (2898ds/4840Mi) % 131.41/19.21 % Exception at run slice level % 131.41/19.21 User error: GNN currently only supports monomorphic FOL. % 131.41/19.21 % (1553704)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=97629261:cts=off:i=5002_2897 on theBenchmark for (2897ds/5002Mi) % 131.41/19.21 % (1553705)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=1044792942:i=30479:sd=3:ss=axioms_2897 on theBenchmark for (2897ds/30479Mi) % 131.41/19.21 % Exception at run slice level % 131.41/19.21 User error: GNN currently only supports monomorphic FOL. % 131.41/19.21 % (1553707)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=2710408739:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2896 on theBenchmark for (2896ds/11035Mi) % 131.41/19.21 % (1553707)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 131.41/19.21 % (1553710)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=1058196443:i=5835_2895 on theBenchmark for (2895ds/5835Mi) % 131.41/19.21 % Exception at run slice level % 131.41/19.21 User error: GNN currently only supports monomorphic FOL. % 131.41/19.21 % Exception at run slice level % 131.41/19.21 User error: GNN currently only supports monomorphic FOL. % 131.41/19.21 % Exception at run slice level % 131.41/19.21 User error: GNN currently only supports monomorphic FOL. % 131.41/19.21 % Exception at run slice level % 131.41/19.21 User error: GNN currently only supports monomorphic FOL. % 131.41/19.21 % (1553713)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=4191673263:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2892 on theBenchmark for (2892ds/5890Mi) % 150.62/21.98 % (1553714)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=774819513:cts=off:i=19910:ep=RS_2892 on theBenchmark for (2892ds/19910Mi) % 150.62/21.98 % (1553715)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=3940055494:i=20312:bd=preordered:fsr=off:er=filter_2891 on theBenchmark for (2891ds/20312Mi) % 150.62/21.98 % (1553716)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=2460399338:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2891 on theBenchmark for (2891ds/13822Mi) % 150.62/21.98 % Exception at run slice level % 150.62/21.98 User error: GNN currently only supports monomorphic FOL. % 150.62/21.98 % (1553721)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=249515090:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2888 on theBenchmark for (2888ds/7144Mi) % 150.62/21.98 % Exception at run slice level % 150.62/21.98 User error: GNN currently only supports monomorphic FOL. % 150.62/21.98 % Exception at run slice level % 150.62/21.98 User error: GNN currently only supports monomorphic FOL. % 150.62/21.98 % (1553723)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=3662970906:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2887 on theBenchmark for (2887ds/15184Mi) % 150.62/21.98 % (1553724)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=7796908:i=107375_2885 on theBenchmark for (2885ds/107375Mi) % 150.62/21.98 % Exception at run slice level % 150.62/21.98 User error: GNN currently only supports monomorphic FOL. % 150.62/21.98 % Exception at run slice level % 150.62/21.98 User error: GNN currently only supports monomorphic FOL. % 150.62/21.98 % (1553727)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=2397495853:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2881 on theBenchmark for (2881ds/7958Mi) % 150.62/21.98 % (1553728)dis+10_128_sil=16000:nwc=0.7:random_seed=3194239077:i=15999:nm=2:gsp=on_2880 on theBenchmark for (2880ds/15999Mi) % 150.62/21.98 % (1553728)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 150.62/21.98 % Exception at run slice level % 150.62/21.98 User error: GNN currently only supports monomorphic FOL. % 150.62/21.98 % (1553731)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=3111018197:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2876 on theBenchmark for (2876ds/8139Mi) % 150.62/21.98 % (1553721)Instruction limit reached! % 150.62/21.98 % (1553721)------------------------------ % 150.62/21.98 % (1553721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.62/21.98 % (1553721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.62/21.98 % (1553721)CaDiCaL version: 2.1.3 % 150.62/21.98 % (1553721)Termination reason: Instruction limit % 150.62/21.98 % (1553721)Termination phase: Saturation % 150.62/21.98 % (1553721)Time elapsed: 1.968 s % 150.62/21.98 % (1553721)Peak memory usage: 159 MB % 150.62/21.98 % (1553721)Instructions burned: 7148 (million) % 150.62/21.98 % (1553733)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=3256928324:st=4:i=8950:sd=5:ss=axioms_2867 on theBenchmark for (2867ds/8950Mi) % 150.62/21.98 % Exception at run slice level % 150.62/21.98 User error: GNN currently only supports monomorphic FOL. % 150.62/21.98 % (1553735)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=259725159:i=9809:ins=10:av=off_2864 on theBenchmark for (2864ds/9809Mi) % 150.62/21.98 % Exception at run slice level % 150.62/21.98 User error: GNN currently only supports monomorphic FOL. % 150.62/21.98 % (1553737)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=1322892534:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2861 on theBenchmark for (2861ds/9885Mi) % 150.62/21.98 % Exception at run slice level % 150.62/21.98 User error: GNN currently only supports monomorphic FOL. % 150.62/21.98 % (1553739)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=2779347781:cond=fast:i=32078:fgj=on:av=off_2857 on theBenchmark for (2857ds/32078Mi) % 186.15/26.92 % Exception at run slice level % 186.15/26.92 User error: GNN currently only supports monomorphic FOL. % 186.15/26.92 % (1553741)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=2202739527:i=11101:bd=all:ss=axioms:sgt=8_2854 on theBenchmark for (2854ds/11101Mi) % 186.15/26.92 % (1553731)Instruction limit reached! % 186.15/26.92 % (1553731)------------------------------ % 186.15/26.92 % (1553731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.15/26.92 % (1553731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.15/26.92 % (1553731)CaDiCaL version: 2.1.3 % 186.15/26.92 % (1553731)Termination reason: Instruction limit % 186.15/26.92 % (1553731)Termination phase: Saturation % 186.15/26.92 % (1553731)Time elapsed: 3.750 s % 186.15/26.92 % (1553731)Peak memory usage: 117 MB % 186.15/26.92 % (1553731)Instructions burned: 8140 (million) % 186.15/26.92 % (1553743)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=321310940:cond=on:i=13220:s2at=3:aac=none:fsd=on_2837 on theBenchmark for (2837ds/13220Mi) % 186.15/26.92 % Exception at run slice level % 186.15/26.92 User error: GNN currently only supports monomorphic FOL. % 186.15/26.92 % (1553745)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=2439659308:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2832 on theBenchmark for (2832ds/13528Mi) % 186.15/26.92 % Exception at run slice level % 186.15/26.92 User error: GNN currently only supports monomorphic FOL. % 186.15/26.92 % (1553741)Instruction limit reached! % 186.15/26.92 % (1553741)------------------------------ % 186.15/26.92 % (1553741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.15/26.92 % (1553741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.15/26.92 % (1553741)CaDiCaL version: 2.1.3 % 186.15/26.92 % (1553741)Termination reason: Instruction limit % 186.15/26.92 % (1553741)Termination phase: Saturation % 186.15/26.92 % (1553741)Time elapsed: 2.783 s % 186.15/26.92 % (1553741)Peak memory usage: 126 MB % 186.15/26.92 % (1553741)Instructions burned: 11103 (million) % 186.15/26.92 % (1553747)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=2868162709:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2827 on theBenchmark for (2827ds/14854Mi) % 186.15/26.92 % (1553748)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=422858954:i=14974:ss=axioms:sgt=16_2825 on theBenchmark for (2825ds/14974Mi) % 186.15/26.92 % Exception at run slice level % 186.15/26.92 User error: GNN currently only supports monomorphic FOL. % 186.15/26.92 % Exception at run slice level % 186.15/26.92 User error: GNN currently only supports monomorphic FOL. % 186.15/26.92 % (1553751)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=375949426:i=33081:aac=none:fgj=on:bd=all:fsr=off_2822 on theBenchmark for (2822ds/33081Mi) % 186.15/26.92 % (1553752)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=1688522162:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2821 on theBenchmark for (2821ds/50856Mi) % 186.15/26.92 % Exception at run slice level % 186.15/26.92 User error: GNN currently only supports monomorphic FOL. % 186.15/26.92 % (1553755)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=112844342:i=69865_2819 on theBenchmark for (2819ds/69865Mi) % 186.15/26.92 % Exception at run slice level % 186.15/26.92 User error: GNN currently only supports monomorphic FOL. % 186.15/26.92 % Exception at run slice level % 186.15/26.92 User error: GNN currently only supports monomorphic FOL. % 186.15/26.92 % (1553757)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=2938212266:cond=fast:i=17802:gtgl=3:gtg=all_2816 on theBenchmark for (2816ds/17802Mi) % 186.15/26.92 % Exception at run slice level % 186.15/26.92 User error: Immediate (shared) subterms of term/literal aa(X1,X0,X3,sK0(X0,X1,X2,X3)) = sF2(X1,X0,X3,X2) have different types/not well-typed! % 186.15/26.92 % (1553758)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=3471498269:i=96644_2815 on theBenchmark for (2815ds/96644Mi) % 209.26/30.19 % (1553760)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 209.26/30.19 % (1553760)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=1311256461:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2814 on theBenchmark for (2814ds/21161Mi) % 209.26/30.19 % (1553622)Instruction limit reached! % 209.26/30.19 % (1553622)------------------------------ % 209.26/30.19 % (1553622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.26/30.19 % (1553622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.26/30.19 % (1553622)CaDiCaL version: 2.1.3 % 209.26/30.19 % (1553622)Termination reason: Instruction limit % 209.26/30.19 % (1553622)Termination phase: Saturation % 209.26/30.19 % (1553622)Time elapsed: 13.342 s % 209.26/30.19 % (1553622)Peak memory usage: 504 MB % 209.26/30.19 % (1553622)Instructions burned: 26474 (million) % 209.26/30.19 % (1553763)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=1054891191:i=22761:gtg=all:ss=axioms:fsd=on_2810 on theBenchmark for (2810ds/22761Mi) % 209.26/30.19 % (1553728)Instruction limit reached! % 209.26/30.19 % (1553728)------------------------------ % 209.26/30.19 % (1553728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.26/30.19 % (1553728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.26/30.19 % (1553728)CaDiCaL version: 2.1.3 % 209.26/30.19 % (1553728)Termination reason: Instruction limit % 209.26/30.19 % (1553728)Termination phase: Saturation % 209.26/30.19 % (1553728)Time elapsed: 7.249 s % 209.26/30.19 % (1553728)Peak memory usage: 137 MB % 209.26/30.19 % (1553728)Instructions burned: 16000 (million) % 209.26/30.19 % Exception at run slice level % 209.26/30.19 User error: GNN currently only supports monomorphic FOL. % 209.26/30.19 % (1553765)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=2684159983:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2806 on theBenchmark for (2806ds/23713Mi) % 209.26/30.19 % (1553766)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=1823165029:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2805 on theBenchmark for (2805ds/26509Mi) % 209.26/30.19 % Exception at run slice level % 209.26/30.19 User error: GNN currently only supports monomorphic FOL. % 209.26/30.19 % (1553769)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=2312099055:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2799 on theBenchmark for (2799ds/28957Mi) % 209.26/30.19 % (1553714)Instruction limit reached! % 209.26/30.19 % (1553714)------------------------------ % 209.26/30.19 % (1553714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.26/30.19 % (1553714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.26/30.19 % (1553714)CaDiCaL version: 2.1.3 % 209.26/30.19 % (1553714)Termination reason: Instruction limit % 209.26/30.19 % (1553714)Termination phase: Saturation % 209.26/30.19 % (1553714)Time elapsed: 9.577 s % 209.26/30.19 % (1553714)Peak memory usage: 131 MB % 209.26/30.19 % (1553714)Instructions burned: 19911 (million) % 209.26/30.19 % (1553771)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=2088655054:i=29246:s2at=-1:kws=inv_arity:ins=10_2794 on theBenchmark for (2794ds/29246Mi) % 209.26/30.19 % Exception at run slice level % 209.26/30.19 User error: GNN currently only supports monomorphic FOL. % 209.26/30.19 % (1553773)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=809982409:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2789 on theBenchmark for (2789ds/30082Mi) % 209.26/30.19 % (1553773)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 209.26/30.19 % (1553596)Instruction limit reached! % 209.26/30.19 % (1553596)------------------------------ % 209.26/30.19 % (1553596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.26/30.19 % (1553596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.44/32.51 % (1553596)CaDiCaL version: 2.1.3 % 225.44/32.51 % (1553596)Termination reason: Instruction limit % 225.44/32.51 % (1553596)Termination phase: Saturation % 225.44/32.51 % (1553596)Time elapsed: 17.426 s % 225.44/32.51 % (1553596)Peak memory usage: 243 MB % 225.44/32.51 % (1553596)Instructions burned: 33336 (million) % 225.44/32.51 % (1553775)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=1199446433:i=32262:bd=preordered_2786 on theBenchmark for (2786ds/32262Mi) % 225.44/32.51 % Exception at run slice level % 225.44/32.51 User error: GNN currently only supports monomorphic FOL. % 225.44/32.51 % (1553777)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=321673005:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2784 on theBenchmark for (2784ds/32870Mi) % 225.44/32.51 % Exception at run slice level % 225.44/32.51 User error: GNN currently only supports monomorphic FOL. % 225.44/32.51 % (1553779)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=58218517:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2781 on theBenchmark for (2781ds/33295Mi) % 225.44/32.51 % Exception at run slice level % 225.44/32.51 User error: GNN currently only supports monomorphic FOL. % 225.44/32.51 % (1553781)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=1166909203:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2779 on theBenchmark for (2779ds/36826Mi) % 225.44/32.51 % Exception at run slice level % 225.44/32.51 User error: GNN currently only supports monomorphic FOL. % 225.44/32.51 % (1553783)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=3908538631:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2776 on theBenchmark for (2776ds/92981Mi) % 225.44/32.51 % Exception at run slice level % 225.44/32.51 User error: GNN currently only supports monomorphic FOL. % 225.44/32.51 % (1553785)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=1092538513:s2pl=on:i=49423_2771 on theBenchmark for (2771ds/49423Mi) % 225.44/32.51 % Exception at run slice level % 225.44/32.51 User error: GNN currently only supports monomorphic FOL. % 225.44/32.51 % (1553787)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=2679515077:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2765 on theBenchmark for (2765ds/57299Mi) % 225.44/32.51 % Exception at run slice level % 225.44/32.51 User error: GNN currently only supports monomorphic FOL. % 225.44/32.51 % (1553789)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=2929257887:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2760 on theBenchmark for (2760ds/127679Mi) % 225.44/32.51 % Exception at run slice level % 225.44/32.51 User error: GNN currently only supports monomorphic FOL. % 225.44/32.51 % (1553791)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=1970632165:i=69402:add=on:aac=none:fsr=off_2755 on theBenchmark for (2755ds/69402Mi) % 225.44/32.51 % Exception at run slice level % 225.44/32.51 User error: GNN currently only supports monomorphic FOL. % 225.44/32.51 % (1553793)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=1538936334:i=100512:doe=on:fgj=on:bd=all:fsd=on_2750 on theBenchmark for (2750ds/100512Mi) % 225.44/32.51 % Exception at run slice level % 225.44/32.51 User error: GNN currently only supports monomorphic FOL. % 225.44/32.51 % (1553795)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=200428096:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2744 on theBenchmark for (2744ds/138761Mi) % 225.44/32.51 % Exception at run slice level % 225.44/32.51 User error: GNN currently only supports monomorphic FOL. % 225.44/32.51 % (1553797)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=132168670:i=282386:rtra=on_2739 on theBenchmark for (2739ds/282386Mi) % 236.94/34.04 % Exception at run slice level % 236.94/34.04 User error: GNN currently only supports monomorphic FOL. % 236.94/34.04 % (1553799)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=4003131353:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2734 on theBenchmark for (2734ds/269354Mi) % 236.94/34.04 % Exception at run slice level % 236.94/34.04 User error: GNN currently only supports monomorphic FOL. % 236.94/34.04 % (1553801)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=1612162888:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2728 on theBenchmark for (2728ds/283390Mi) % 236.94/34.04 % (1553801)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 236.94/34.04 % Exception at run slice level % 236.94/34.04 User error: GNN currently only supports monomorphic FOL. % 236.94/34.04 % (1553803)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=599844322:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2723 on theBenchmark for (2723ds/218Mi) % 236.94/34.04 % (1553803)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 236.94/34.04 % (1553803)Refutation not found, incomplete strategy % 236.94/34.04 % (1553803)------------------------------ % 236.94/34.04 % (1553803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.94/34.04 % (1553803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.94/34.04 % (1553803)CaDiCaL version: 2.1.3 % 236.94/34.04 % (1553803)Termination reason: Refutation not found, incomplete strategy % 236.94/34.04 % (1553803)Time elapsed: 0.009 s % 236.94/34.04 % (1553803)Peak memory usage: 89 MB % 236.94/34.04 % (1553803)Instructions burned: 14 (million) % 236.94/34.04 % (1553803)------------------------------ % 236.94/34.04 % (1553803)------------------------------ % 236.94/34.04 % (1553805)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=3130360818:i=238:av=off:rtra=on:ss=axioms_2719 on theBenchmark for (2719ds/238Mi) % 236.94/34.04 % (1553805)Instruction limit reached! % 236.94/34.04 % (1553805)------------------------------ % 236.94/34.04 % (1553805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.94/34.04 % (1553805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.94/34.04 % (1553805)CaDiCaL version: 2.1.3 % 236.94/34.04 % (1553805)Termination reason: Instruction limit % 236.94/34.04 % (1553805)Termination phase: Saturation % 236.94/34.04 % (1553805)Time elapsed: 0.122 s % 236.94/34.04 % (1553805)Peak memory usage: 89 MB % 236.94/34.04 % (1553805)Instructions burned: 239 (million) % 236.94/34.04 % (1553807)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=3253276488:s2a=on:i=278:rtra=on:gtg=position_2716 on theBenchmark for (2716ds/278Mi) % 236.94/34.04 % (1553807)Instruction limit reached! % 236.94/34.04 % (1553807)------------------------------ % 236.94/34.04 % (1553807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.94/34.04 % (1553807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.94/34.04 % (1553807)CaDiCaL version: 2.1.3 % 236.94/34.04 % (1553807)Termination reason: Instruction limit % 236.94/34.04 % (1553807)Termination phase: Saturation % 236.94/34.04 % (1553807)Time elapsed: 0.162 s % 236.94/34.04 % (1553807)Peak memory usage: 90 MB % 236.94/34.04 % (1553807)Instructions burned: 278 (million) % 236.94/34.04 % (1553809)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=3153177504:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2713 on theBenchmark for (2713ds/258Mi) % 236.94/34.04 % (1553809)Instruction limit reached! % 236.94/34.04 % (1553809)------------------------------ % 236.94/34.04 % (1553809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.94/34.04 % (1553809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.94/34.04 % (1553809)CaDiCaL version: 2.1.3 % 236.94/34.04 % (1553809)Termination reason: Instruction limit % 236.94/34.04 % (1553809)Termination phase: Saturation % 236.94/34.04 % (1553809)Time elapsed: 0.153 s % 236.94/34.04 % (1553809)Peak memory usage: 90 MB % 236.94/34.04 % (1553809)Instructions burned: 259 (million) % 236.94/34.04 % (1553811)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=3587945180:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2709 on theBenchmark for (2709ds/570Mi) % 236.94/34.04 % (1553811)Instruction limit reached! % 241.35/34.73 % (1553811)------------------------------ % 241.35/34.73 % (1553811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.35/34.73 % (1553811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.35/34.73 % (1553811)CaDiCaL version: 2.1.3 % 241.35/34.73 % (1553811)Termination reason: Instruction limit % 241.35/34.73 % (1553811)Termination phase: Saturation % 241.35/34.73 % (1553811)Time elapsed: 0.311 s % 241.35/34.73 % (1553811)Peak memory usage: 93 MB % 241.35/34.73 % (1553811)Instructions burned: 570 (million) % 241.35/34.73 % (1553813)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=98349627:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2704 on theBenchmark for (2704ds/314Mi) % 241.35/34.73 % (1553813)Instruction limit reached! % 241.35/34.73 % (1553813)------------------------------ % 241.35/34.73 % (1553813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.35/34.73 % (1553813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.35/34.73 % (1553813)CaDiCaL version: 2.1.3 % 241.35/34.73 % (1553813)Termination reason: Instruction limit % 241.35/34.73 % (1553813)Termination phase: Saturation % 241.35/34.73 % (1553813)Time elapsed: 0.185 s % 241.35/34.73 % (1553813)Peak memory usage: 92 MB % 241.35/34.73 % (1553813)Instructions burned: 315 (million) % 241.35/34.73 % (1553815)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=1260346065:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2701 on theBenchmark for (2701ds/650Mi) % 241.35/34.73 % (1553815)Instruction limit reached! % 241.35/34.73 % (1553815)------------------------------ % 241.35/34.73 % (1553815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.35/34.73 % (1553815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.35/34.73 % (1553815)CaDiCaL version: 2.1.3 % 241.35/34.73 % (1553815)Termination reason: Instruction limit % 241.35/34.73 % (1553815)Termination phase: Saturation % 241.35/34.73 % (1553815)Time elapsed: 0.413 s % 241.35/34.73 % (1553815)Peak memory usage: 94 MB % 241.35/34.73 % (1553815)Instructions burned: 650 (million) % 241.35/34.73 % (1553817)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=356990317:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2695 on theBenchmark for (2695ds/496Mi) % 241.35/34.73 % (1553817)Instruction limit reached! % 241.35/34.73 % (1553817)------------------------------ % 241.35/34.73 % (1553817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.35/34.73 % (1553817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.35/34.73 % (1553817)CaDiCaL version: 2.1.3 % 241.35/34.73 % (1553817)Termination reason: Instruction limit % 241.35/34.73 % (1553817)Termination phase: Saturation % 241.35/34.73 % (1553817)Time elapsed: 0.282 s % 241.35/34.73 % (1553817)Peak memory usage: 94 MB % 241.35/34.73 % (1553817)Instructions burned: 496 (million) % 241.35/34.73 % (1553819)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=3575482696:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2691 on theBenchmark for (2691ds/588Mi) % 241.35/34.73 % (1553819)Refutation not found, incomplete strategy % 241.35/34.73 % (1553819)------------------------------ % 241.35/34.73 % (1553819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.35/34.73 % (1553819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.35/34.73 % (1553819)CaDiCaL version: 2.1.3 % 241.35/34.73 % (1553819)Termination reason: Refutation not found, incomplete strategy % 241.35/34.73 % (1553819)Time elapsed: 0.018 s % 241.35/34.73 % (1553819)Peak memory usage: 89 MB % 241.35/34.73 % (1553819)Instructions burned: 29 (million) % 241.35/34.73 % (1553819)------------------------------ % 241.35/34.73 % (1553819)------------------------------ % 241.35/34.73 % (1553821)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=1006448616:i=4700:rtra=on_2686 on theBenchmark for (2686ds/4700Mi) % 241.35/34.73 % (1553765)Instruction limit reached! % 241.35/34.73 % (1553765)------------------------------ % 241.35/34.73 % (1553765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.35/34.73 % (1553765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.35/34.73 % (1553765)CaDiCaL version: 2.1.3 % 241.35/34.73 % (1553765)Termination reason: Instruction limit % 241.35/34.73 % (1553765)Termination phase: Saturation % 241.35/34.73 % (1553765)Time elapsed: 12.131 s % 241.35/34.73 % (1553765)Peak memory usage: 228 MB % 241.35/34.73 % (1553765)Instructions burned: 23714 (million) % 241.35/34.73 % (1553823)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=584334347:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2683 on theBenchmark for (2683ds/226Mi) % 247.73/35.71 % Exception at run slice level % 247.73/35.71 User error: GNN currently only supports monomorphic FOL. % 247.73/35.71 % (1553823)Instruction limit reached! % 247.73/35.71 % (1553823)------------------------------ % 247.73/35.71 % (1553823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.73/35.71 % (1553823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.73/35.71 % (1553823)CaDiCaL version: 2.1.3 % 247.73/35.71 % (1553823)Termination reason: Instruction limit % 247.73/35.71 % (1553823)Termination phase: Saturation % 247.73/35.71 % (1553823)Time elapsed: 0.149 s % 247.73/35.71 % (1553823)Peak memory usage: 91 MB % 247.73/35.71 % (1553823)Instructions burned: 227 (million) % 247.73/35.71 % (1553825)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2839349347:i=254:av=off:fsr=off:rtra=on:sup=off_2681 on theBenchmark for (2681ds/254Mi) % 247.73/35.71 % (1553826)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=3733376872:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2680 on theBenchmark for (2680ds/228Mi) % 247.73/35.71 % (1553825)Instruction limit reached! % 247.73/35.71 % (1553825)------------------------------ % 247.73/35.71 % (1553825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.73/35.71 % (1553825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.73/35.71 % (1553825)CaDiCaL version: 2.1.3 % 247.73/35.71 % (1553825)Termination reason: Instruction limit % 247.73/35.71 % (1553825)Termination phase: Saturation % 247.73/35.71 % (1553825)Time elapsed: 0.122 s % 247.73/35.71 % (1553825)Peak memory usage: 89 MB % 247.73/35.71 % (1553825)Instructions burned: 256 (million) % 247.73/35.71 % (1553826)Instruction limit reached! % 247.73/35.71 % (1553826)------------------------------ % 247.73/35.71 % (1553826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.73/35.71 % (1553826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.73/35.71 % (1553826)CaDiCaL version: 2.1.3 % 247.73/35.71 % (1553826)Termination reason: Instruction limit % 247.73/35.71 % (1553826)Termination phase: Saturation % 247.73/35.71 % (1553826)Time elapsed: 0.116 s % 247.73/35.71 % (1553826)Peak memory usage: 89 MB % 247.73/35.71 % (1553826)Instructions burned: 229 (million) % 247.73/35.71 % (1553829)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=697487897:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2678 on theBenchmark for (2678ds/1814Mi) % 247.73/35.71 % (1553830)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=2204198889:i=874:sd=1:aac=none:rtra=on:ss=included_2677 on theBenchmark for (2677ds/874Mi) % 247.73/35.71 % (1553830)Refutation not found, incomplete strategy % 247.73/35.71 % (1553830)------------------------------ % 247.73/35.71 % (1553830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.73/35.71 % (1553830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.73/35.71 % (1553830)CaDiCaL version: 2.1.3 % 247.73/35.71 % (1553830)Termination reason: Refutation not found, incomplete strategy % 247.73/35.71 % (1553830)Time elapsed: 0.020 s % 247.73/35.71 % (1553830)Peak memory usage: 89 MB % 247.73/35.71 % (1553830)Instructions burned: 33 (million) % 247.73/35.71 % (1553830)------------------------------ % 247.73/35.71 % (1553830)------------------------------ % 247.73/35.71 % (1553833)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=3003213848:i=10404:rtra=on:ss=axioms:sgt=16_2673 on theBenchmark for (2673ds/10404Mi) % 247.73/35.71 % Exception at run slice level % 247.73/35.71 User error: GNN currently only supports monomorphic FOL. % 247.73/35.71 % (1553829)Instruction limit reached! % 247.73/35.71 % (1553829)------------------------------ % 247.73/35.71 % (1553829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.73/35.71 % (1553829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.73/35.71 % (1553829)CaDiCaL version: 2.1.3 % 247.73/35.71 % (1553829)Termination reason: Instruction limit % 247.73/35.71 % (1553829)Termination phase: Saturation % 247.73/35.71 % (1553829)Time elapsed: 1.053 s % 247.73/35.71 % (1553829)Peak memory usage: 99 MB % 247.73/35.71 % (1553829)Instructions burned: 1814 (million) % 247.73/35.71 % (1553760)Instruction limit reached! % 247.73/35.71 % (1553760)------------------------------ % 247.73/35.71 % (1553760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.73/35.71 % (1553760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.44/36.86 % (1553760)CaDiCaL version: 2.1.3 % 255.44/36.86 % (1553760)Termination reason: Instruction limit % 255.44/36.86 % (1553760)Termination phase: Saturation % 255.44/36.86 % (1553760)Time elapsed: 14.677 s % 255.44/36.86 % (1553760)Peak memory usage: 220 MB % 255.44/36.86 % (1553760)Instructions burned: 21162 (million) % 255.44/36.86 % (1553835)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3753619557:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2668 on theBenchmark for (2668ds/268Mi) % 255.44/36.86 % (1553836)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=762380779:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2666 on theBenchmark for (2666ds/1184Mi) % 255.44/36.86 % (1553836)Refutation not found, incomplete strategy % 255.44/36.86 % (1553836)------------------------------ % 255.44/36.86 % (1553836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.44/36.86 % (1553836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.44/36.86 % (1553836)CaDiCaL version: 2.1.3 % 255.44/36.86 % (1553836)Termination reason: Refutation not found, incomplete strategy % 255.44/36.86 % (1553836)Time elapsed: 0.012 s % 255.44/36.86 % (1553836)Peak memory usage: 89 MB % 255.44/36.86 % (1553836)Instructions burned: 19 (million) % 255.44/36.86 % (1553835)Instruction limit reached! % 255.44/36.86 % (1553835)------------------------------ % 255.44/36.86 % (1553835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.44/36.86 % (1553835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.44/36.86 % (1553835)CaDiCaL version: 2.1.3 % 255.44/36.86 % (1553835)Termination reason: Instruction limit % 255.44/36.86 % (1553835)Termination phase: Saturation % 255.44/36.86 % (1553835)Time elapsed: 0.156 s % 255.44/36.86 % (1553835)Peak memory usage: 91 MB % 255.44/36.86 % (1553835)Instructions burned: 268 (million) % 255.44/36.86 % (1553838)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=2178901023:st=3:i=26386:sd=3:rtra=on:ss=axioms_2666 on theBenchmark for (2666ds/26386Mi) % 255.44/36.86 % (1553841)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=3681358407:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2664 on theBenchmark for (2664ds/250Mi) % 255.44/36.86 % (1553841)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 255.44/36.86 % (1553836)------------------------------ % 255.44/36.86 % (1553836)------------------------------ % 255.44/36.86 % (1553841)Instruction limit reached! % 255.44/36.86 % (1553841)------------------------------ % 255.44/36.86 % (1553841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.44/36.86 % (1553841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.44/36.86 % (1553841)CaDiCaL version: 2.1.3 % 255.44/36.86 % (1553841)Termination reason: Instruction limit % 255.44/36.86 % (1553841)Termination phase: Saturation % 255.44/36.86 % (1553841)Time elapsed: 0.160 s % 255.44/36.86 % (1553841)Peak memory usage: 92 MB % 255.44/36.86 % (1553841)Instructions burned: 252 (million) % 255.44/36.86 % Exception at run slice level % 255.44/36.86 User error: GNN currently only supports monomorphic FOL. % 255.44/36.86 % (1553843)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=3576623140:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2662 on theBenchmark for (2662ds/268Mi) % 255.44/36.86 % Exception at run slice level % 255.44/36.86 User error: Immediate (shared) subterms of term/literal aa(X1,X0,X3,sK1(X0,X1,X2,X3)) = sF25(X1,X0,X3,X2) have different types/not well-typed! % 255.44/36.86 % (1553844)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3667153037:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2661 on theBenchmark for (2661ds/282Mi) % 255.44/36.86 % (1553844)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 255.44/36.86 % (1553844)Refutation not found, incomplete strategy % 255.44/36.86 % (1553844)------------------------------ % 255.44/36.86 % (1553844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.44/36.86 % (1553844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.44/36.86 % (1553844)CaDiCaL version: 2.1.3 % 255.44/36.86 % (1553844)Termination reason: Refutation not found, incomplete strategy % 255.44/36.86 % (1553844)Time elapsed: 0.006 s % 255.44/36.86 % (1553844)Peak memory usage: 89 MB % 255.44/36.86 % (1553844)Instructions burned: 8 (million) % 255.44/36.86 % (1553845)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=3623599366:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2661 on theBenchmark for (2661ds/862Mi) % 275.31/39.57 % (1553847)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=3344687391:i=12120:aac=none:ins=25:rtra=on_2660 on theBenchmark for (2660ds/12120Mi) % 275.31/39.57 % (1553844)------------------------------ % 275.31/39.57 % (1553844)------------------------------ % 275.31/39.57 % (1553851)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=3424056486:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2657 on theBenchmark for (2657ds/300Mi) % 275.31/39.57 % (1553851)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 275.31/39.57 % Exception at run slice level % 275.31/39.57 User error: GNN currently only supports monomorphic FOL. % 275.31/39.57 % (1553845)Instruction limit reached! % 275.31/39.57 % (1553845)------------------------------ % 275.31/39.57 % (1553845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.31/39.57 % (1553845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.31/39.57 % (1553845)CaDiCaL version: 2.1.3 % 275.31/39.57 % (1553845)Termination reason: Instruction limit % 275.31/39.57 % (1553845)Termination phase: Saturation % 275.31/39.57 % (1553845)Time elapsed: 0.467 s % 275.31/39.57 % (1553845)Peak memory usage: 94 MB % 275.31/39.57 % (1553845)Instructions burned: 863 (million) % 275.31/39.57 % (1553851)Instruction limit reached! % 275.31/39.57 % (1553851)------------------------------ % 275.31/39.57 % (1553851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.31/39.57 % (1553851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.31/39.57 % (1553851)CaDiCaL version: 2.1.3 % 275.31/39.57 % (1553851)Termination reason: Instruction limit % 275.31/39.57 % (1553851)Termination phase: Saturation % 275.31/39.57 % (1553851)Time elapsed: 0.180 s % 275.31/39.57 % (1553851)Peak memory usage: 92 MB % 275.31/39.57 % (1553851)Instructions burned: 301 (million) % 275.31/39.57 % (1553853)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=2680436470:i=28310:bd=all:rtra=on_2655 on theBenchmark for (2655ds/28310Mi) % 275.31/39.57 % (1553854)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=880503826:i=1334:av=off:fsr=off:rtra=on_2654 on theBenchmark for (2654ds/1334Mi) % 275.31/39.57 % (1553855)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=2276453045:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2653 on theBenchmark for (2653ds/370Mi) % 275.31/39.57 % (1553854)Refutation not found, incomplete strategy % 275.31/39.57 % (1553854)------------------------------ % 275.31/39.57 % (1553854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.31/39.57 % (1553854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.31/39.57 % (1553854)CaDiCaL version: 2.1.3 % 275.31/39.57 % (1553854)Termination reason: Refutation not found, incomplete strategy % 275.31/39.57 % (1553854)Time elapsed: 0.141 s % 275.31/39.57 % (1553854)Peak memory usage: 90 MB % 275.31/39.57 % (1553854)Instructions burned: 278 (million) % 275.31/39.57 % (1553690)Instruction limit reached! % 275.31/39.57 % (1553690)------------------------------ % 275.31/39.57 % (1553690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.31/39.57 % (1553690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.31/39.57 % (1553690)CaDiCaL version: 2.1.3 % 275.31/39.57 % (1553690)Termination reason: Instruction limit % 275.31/39.57 % (1553690)Termination phase: Saturation % 275.31/39.57 % (1553690)Time elapsed: 25.246 s % 275.31/39.57 % (1553690)Peak memory usage: 246 MB % 275.31/39.57 % (1553690)Instructions burned: 43698 (million) % 275.31/39.57 % Exception at run slice level % 275.31/39.57 User error: GNN currently only supports monomorphic FOL. % 275.31/39.57 % (1553855)Instruction limit reached! % 275.31/39.57 % (1553855)------------------------------ % 275.31/39.57 % (1553855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.31/39.57 % (1553855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.31/39.57 % (1553855)CaDiCaL version: 2.1.3 % 287.63/41.24 % (1553855)Termination reason: Instruction limit % 287.63/41.24 % (1553855)Termination phase: Saturation % 287.63/41.24 % (1553855)Time elapsed: 0.234 s % 287.63/41.24 % (1553855)Peak memory usage: 93 MB % 287.63/41.24 % (1553855)Instructions burned: 371 (million) % 287.63/41.24 % (1553859)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=3176685210:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2651 on theBenchmark for (2651ds/386Mi) % 287.63/41.24 % (1553854)------------------------------ % 287.63/41.24 % (1553854)------------------------------ % 287.63/41.24 % (1553860)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=1152034316:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2650 on theBenchmark for (2650ds/9700Mi) % 287.63/41.24 % (1553861)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=1976131491:i=24222:sd=1:rtra=on:ss=included_2649 on theBenchmark for (2649ds/24222Mi) % 287.63/41.24 % (1553863)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=3787144919:i=638:kws=precedence:fsr=off:rtra=on_2649 on theBenchmark for (2649ds/638Mi) % 287.63/41.24 % (1553859)Instruction limit reached! % 287.63/41.24 % (1553859)------------------------------ % 287.63/41.24 % (1553859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.63/41.24 % (1553859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.63/41.24 % (1553859)CaDiCaL version: 2.1.3 % 287.63/41.24 % (1553859)Termination reason: Instruction limit % 287.63/41.24 % (1553859)Termination phase: Saturation % 287.63/41.24 % (1553859)Time elapsed: 0.212 s % 287.63/41.24 % (1553859)Peak memory usage: 94 MB % 287.63/41.24 % (1553859)Instructions burned: 386 (million) % 287.63/41.24 % (1553867)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3149851674:i=4128:ep=RST:rtra=on_2647 on theBenchmark for (2647ds/4128Mi) % 287.63/41.24 % (1553867)Refutation not found, incomplete strategy % 287.63/41.24 % (1553867)------------------------------ % 287.63/41.24 % (1553867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.63/41.24 % (1553867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.63/41.24 % (1553867)CaDiCaL version: 2.1.3 % 287.63/41.24 % (1553867)Termination reason: Refutation not found, incomplete strategy % 287.63/41.24 % (1553867)Time elapsed: 0.013 s % 287.63/41.24 % (1553867)Peak memory usage: 89 MB % 287.63/41.24 % (1553867)Instructions burned: 21 (million) % 287.63/41.24 % (1553863)Instruction limit reached! % 287.63/41.24 % (1553863)------------------------------ % 287.63/41.24 % (1553863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.63/41.24 % (1553863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.63/41.24 % (1553863)CaDiCaL version: 2.1.3 % 287.63/41.24 % (1553863)Termination reason: Instruction limit % 287.63/41.24 % (1553863)Termination phase: Saturation % 287.63/41.24 % (1553863)Time elapsed: 0.279 s % 287.63/41.24 % (1553863)Peak memory usage: 92 MB % 287.63/41.24 % (1553863)Instructions burned: 639 (million) % 287.63/41.24 % Exception at run slice level % 287.63/41.24 User error: GNN currently only supports monomorphic FOL. % 287.63/41.24 % (1553869)dis-1011_128_sil=32000:si=on:random_seed=2489140548:i=7412:ep=RST:av=off:rtra=on_2644 on theBenchmark for (2644ds/7412Mi) % 287.63/41.24 % (1553867)------------------------------ % 287.63/41.24 % (1553867)------------------------------ % 287.63/41.24 % (1553870)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1778581430:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2644 on theBenchmark for (2644ds/1514Mi) % 287.63/41.24 % (1553870)Refutation not found, incomplete strategy % 287.63/41.24 % (1553870)------------------------------ % 287.63/41.24 % (1553870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.63/41.24 % (1553870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.63/41.24 % (1553870)CaDiCaL version: 2.1.3 % 287.63/41.24 % (1553870)Termination reason: Refutation not found, incomplete strategy % 287.63/41.24 % (1553870)Time elapsed: 0.028 s % 287.63/41.24 % (1553870)Peak memory usage: 89 MB % 287.63/41.24 % (1553870)Instructions burned: 50 (million) % 287.63/41.24 % (1553872)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=3996666395:i=27826:rtra=on:ss=axioms:sgt=8_2643 on theBenchmark for (2643ds/27826Mi) % 287.63/41.24 % (1553870)------------------------------ % 287.63/41.24 % (1553870)------------------------------ % 287.63/41.24 % (1553875)lrs+10_1_ncem=casc2026/Terminated %------------------------------------------------------------------------------