%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW511_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:30:43 PM UTC 2026 % Result : Timeout 289.09s 41.62s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW511_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.18 % Computer : n006.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 14:16:53 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.22 Running first-order theorem proving % 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.10/1.72 % (3991918)Detected formulas, will run a generic FOF schedule. % 6.10/1.72 % (3991929)dis-21_1_sil=8000:lcm=predicate:random_seed=4142091410:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 6.10/1.72 % (3991929)Instruction limit reached! % 6.10/1.72 % (3991929)------------------------------ % 6.10/1.72 % (3991929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.10/1.72 % (3991929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.72 % (3991929)CaDiCaL version: 2.1.3 % 6.10/1.72 % (3991929)Termination reason: Instruction limit % 6.10/1.72 % (3991929)Termination phase: Saturation % 6.10/1.72 % (3991929)Time elapsed: 0.035 s % 6.10/1.72 % (3991929)Peak memory usage: 89 MB % 6.10/1.72 % (3991929)Instructions burned: 132 (million) % 6.10/1.72 % (3991923)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=698693644:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 6.10/1.72 % (3991924)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=4232627865:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 6.10/1.72 % (3991927)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=51626490:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 6.10/1.72 % (3991928)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3733737903:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 6.10/1.72 % (3991926)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=211984549:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 6.10/1.72 % (3991925)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=3533567313:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 6.10/1.72 % (3991926)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 6.10/1.72 % (3991925)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 6.10/1.72 % (3991926)Refutation not found, incomplete strategy % 6.10/1.72 % (3991926)------------------------------ % 6.10/1.72 % (3991926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.10/1.72 % (3991926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.72 % (3991926)CaDiCaL version: 2.1.3 % 6.10/1.72 % (3991926)Termination reason: Refutation not found, incomplete strategy % 6.10/1.72 % (3991926)Time elapsed: 0.010 s % 6.10/1.72 % (3991926)Peak memory usage: 89 MB % 6.10/1.72 % (3991926)Instructions burned: 17 (million) % 6.10/1.72 % (3991927)Instruction limit reached! % 6.10/1.72 % (3991927)------------------------------ % 6.10/1.72 % (3991927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.10/1.72 % (3991927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.72 % (3991927)CaDiCaL version: 2.1.3 % 6.10/1.72 % (3991927)Termination reason: Instruction limit % 6.10/1.72 % (3991927)Termination phase: Saturation % 6.10/1.72 % (3991927)Time elapsed: 0.075 s % 6.10/1.72 % (3991927)Peak memory usage: 89 MB % 6.10/1.72 % (3991927)Instructions burned: 120 (million) % 6.10/1.72 % (3991928)Instruction limit reached! % 6.10/1.72 % (3991928)------------------------------ % 6.10/1.72 % (3991928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.10/1.72 % (3991928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.72 % (3991928)CaDiCaL version: 2.1.3 % 6.10/1.72 % (3991928)Termination reason: Instruction limit % 6.10/1.72 % (3991928)Termination phase: Saturation % 6.10/1.72 % (3991928)Time elapsed: 0.090 s % 6.10/1.72 % (3991928)Peak memory usage: 89 MB % 6.10/1.72 % (3991928)Instructions burned: 139 (million) % 6.10/1.72 % (3991931)lrs+10_1_sil=8000:sp=occurrence:random_seed=932967722:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi) % 6.10/1.72 % (3991931)Instruction limit reached! % 6.10/1.72 % (3991931)------------------------------ % 6.10/1.72 % (3991931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.10/1.72 % (3991931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.72 % (3991931)CaDiCaL version: 2.1.3 % 9.65/2.04 % (3991931)Termination reason: Instruction limit % 9.65/2.04 % (3991931)Termination phase: Saturation % 9.65/2.04 % (3991931)Time elapsed: 0.091 s % 9.65/2.04 % (3991931)Peak memory usage: 91 MB % 9.65/2.04 % (3991931)Instructions burned: 288 (million) % 9.65/2.04 % (3991938)lrs+10_1_sil=32000:urr=on:br=off:random_seed=108722041:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 9.65/2.04 % (3991926)------------------------------ % 9.65/2.04 % (3991926)------------------------------ % 9.65/2.04 % (3991939)lrs+1011_1_sil=32000:sp=occurrence:random_seed=716552844:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 9.65/2.04 % (3991941)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=766381211:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi) % 9.65/2.04 % (3991938)Instruction limit reached! % 9.65/2.04 % (3991938)------------------------------ % 9.65/2.04 % (3991938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.65/2.04 % (3991938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.65/2.04 % (3991938)CaDiCaL version: 2.1.3 % 9.65/2.04 % (3991938)Termination reason: Instruction limit % 9.65/2.04 % (3991938)Termination phase: Saturation % 9.65/2.04 % (3991938)Time elapsed: 0.093 s % 9.65/2.04 % (3991938)Peak memory usage: 90 MB % 9.65/2.04 % (3991938)Instructions burned: 159 (million) % 9.65/2.04 % Exception at run slice level % 9.65/2.04 User error: % Exception at run slice levelGNN currently only supports monomorphic FOL. % 9.65/2.04 % 9.65/2.04 User error: GNN currently only supports monomorphic FOL. % 9.65/2.04 % Exception at run slice level % 9.65/2.04 User error: GNN currently only supports monomorphic FOL. % 9.65/2.04 % (3991941)Instruction limit reached! % 9.65/2.04 % (3991941)------------------------------ % 9.65/2.04 % (3991941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.65/2.04 % (3991941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.65/2.04 % (3991941)CaDiCaL version: 2.1.3 % 9.65/2.04 % (3991941)Termination reason: Instruction limit % 9.65/2.04 % (3991941)Termination phase: Saturation % 9.65/2.04 % (3991941)Time elapsed: 0.066 s % 9.65/2.04 % (3991941)Peak memory usage: 90 MB % 9.65/2.04 % (3991941)Instructions burned: 250 (million) % 9.65/2.04 % (3991939)Instruction limit reached! % 9.65/2.04 % (3991939)------------------------------ % 9.65/2.04 % (3991939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.65/2.04 % (3991939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.65/2.04 % (3991939)CaDiCaL version: 2.1.3 % 9.65/2.04 % (3991939)Termination reason: Instruction limit % 9.65/2.04 % (3991939)Termination phase: Saturation % 9.65/2.04 % (3991939)Time elapsed: 0.157 s % 9.65/2.04 % (3991939)Peak memory usage: 89 MB % 9.65/2.04 % (3991939)Instructions burned: 327 (million) % 9.65/2.04 % (3991944)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2879284329:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 9.65/2.04 % (3991946)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2558775731:i=2350_2994 on theBenchmark for (2994ds/2350Mi) % 9.65/2.04 % (3991950)lrs+10_1_sil=8000:sp=occurrence:random_seed=2074886026:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 9.65/2.04 % (3991949)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3757768759:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 9.65/2.04 % (3991948)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=258118652:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 9.65/2.04 % (3991947)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1791628320:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 9.65/2.04 % (3991948)Instruction limit reached! % 9.65/2.04 % (3991948)------------------------------ % 9.65/2.04 % (3991948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.65/2.04 % (3991948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.65/2.04 % (3991948)CaDiCaL version: 2.1.3 % 9.65/2.04 % (3991948)Termination reason: Instruction limit % 9.65/2.04 % (3991948)Termination phase: Saturation % 9.65/2.04 % (3991948)Time elapsed: 0.056 s % 9.65/2.04 % (3991948)Peak memory usage: 88 MB % 9.65/2.04 % (3991948)Instructions burned: 127 (million) % 9.65/2.04 % (3991947)Instruction limit reached! % 11.66/2.40 % (3991947)------------------------------ % 11.66/2.40 % (3991947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.66/2.40 % (3991947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.66/2.40 % (3991947)CaDiCaL version: 2.1.3 % 11.66/2.40 % (3991947)Termination reason: Instruction limit % 11.66/2.40 % (3991947)Termination phase: Saturation % 11.66/2.40 % (3991947)Time elapsed: 0.060 s % 11.66/2.40 % (3991947)Peak memory usage: 89 MB % 11.66/2.40 % (3991947)Instructions burned: 113 (million) % 11.66/2.40 % (3991949)Instruction limit reached! % 11.66/2.40 % (3991949)------------------------------ % 11.66/2.40 % (3991949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.66/2.40 % (3991949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.66/2.40 % (3991949)CaDiCaL version: 2.1.3 % 11.66/2.40 % (3991949)Termination reason: Instruction limit % 11.66/2.40 % (3991949)Termination phase: Saturation % 11.66/2.40 % (3991949)Time elapsed: 0.062 s % 11.66/2.40 % (3991949)Peak memory usage: 89 MB % 11.66/2.40 % (3991949)Instructions burned: 115 (million) % 11.66/2.40 % (3991952)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=635232387:i=437:sd=1:aac=none:ss=included_2994 on theBenchmark for (2994ds/437Mi) % 11.66/2.40 % (3991944)Instruction limit reached! % 11.66/2.40 % (3991944)------------------------------ % 11.66/2.40 % (3991944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.66/2.40 % (3991944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.66/2.40 % (3991944)CaDiCaL version: 2.1.3 % 11.66/2.40 % (3991944)Termination reason: Instruction limit % 11.66/2.40 % (3991944)Termination phase: Saturation % 11.66/2.40 % (3991944)Time elapsed: 0.146 s % 11.66/2.40 % (3991944)Peak memory usage: 89 MB % 11.66/2.40 % (3991944)Instructions burned: 296 (million) % 11.66/2.40 % (3991958)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=363979612:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi) % 11.66/2.40 % (3991961)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3754765468:st=8:i=592:sd=3:ep=RST:ss=axioms_2992 on theBenchmark for (2992ds/592Mi) % 11.66/2.40 % (3991960)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=431798468:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2992 on theBenchmark for (2992ds/134Mi) % 11.66/2.40 % (3991962)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=285463653:st=3:i=13193:sd=3:ss=axioms_2992 on theBenchmark for (2992ds/13193Mi) % 11.66/2.40 % (3991952)Instruction limit reached! % 11.66/2.40 % (3991952)------------------------------ % 11.66/2.40 % (3991952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.66/2.40 % (3991952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.66/2.40 % (3991952)CaDiCaL version: 2.1.3 % 11.66/2.40 % (3991952)Termination reason: Instruction limit % 11.66/2.40 % (3991952)Termination phase: Saturation % 11.66/2.40 % (3991952)Time elapsed: 0.166 s % 11.66/2.40 % (3991952)Peak memory usage: 88 MB % 11.66/2.40 % (3991952)Instructions burned: 438 (million) % 11.66/2.40 % (3991950)Instruction limit reached! % 11.66/2.40 % (3991950)------------------------------ % 11.66/2.40 % (3991950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.66/2.40 % (3991950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.66/2.40 % (3991950)CaDiCaL version: 2.1.3 % 11.66/2.40 % (3991950)Termination reason: Instruction limit % 11.66/2.40 % (3991950)Termination phase: Saturation % 11.66/2.40 % (3991950)Time elapsed: 0.279 s % 11.66/2.40 % (3991950)Peak memory usage: 94 MB % 11.66/2.40 % (3991950)Instructions burned: 909 (million) % 11.66/2.40 % (3991960)Instruction limit reached! % 11.66/2.40 % (3991960)------------------------------ % 11.66/2.40 % (3991960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.66/2.40 % (3991960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.66/2.40 % (3991960)CaDiCaL version: 2.1.3 % 11.66/2.40 % (3991960)Termination reason: Instruction limit % 11.66/2.40 % (3991960)Termination phase: Saturation % 11.66/2.40 % (3991960)Time elapsed: 0.080 s % 11.66/2.40 % (3991960)Peak memory usage: 90 MB % 11.66/2.40 % (3991960)Instructions burned: 135 (million) % 11.66/2.40 % Exception at run slice level % 11.66/2.40 User error: GNN currently only supports monomorphic FOL. % 11.66/2.40 % (3991967)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=1565742394:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/125Mi) % 17.74/3.18 % (3991967)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 17.74/3.18 % (3991968)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1370093036:i=134:gtgl=5:slsql=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/134Mi) % 17.74/3.18 % Exception at run slice level % 17.74/3.18 User error: Immediate (shared) subterms of term/literal hoare_376461865e_case(X1,X0,X5,hoare_1841697145triple(X1,X4,X3,X2)) = sF95(X1,X0,X5,X4,X3,X2) have different types/not well-typed! % 17.74/3.18 % (3991969)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=576360539:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/141Mi) % 17.74/3.18 % (3991969)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 17.74/3.18 % (3991967)Instruction limit reached! % 17.74/3.18 % (3991967)------------------------------ % 17.74/3.18 % (3991967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.74/3.18 % (3991967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.74/3.18 % (3991967)CaDiCaL version: 2.1.3 % 17.74/3.18 % (3991967)Termination reason: Instruction limit % 17.74/3.18 % (3991967)Termination phase: Saturation % 17.74/3.18 % (3991967)Time elapsed: 0.065 s % 17.74/3.18 % (3991967)Peak memory usage: 90 MB % 17.74/3.18 % (3991967)Instructions burned: 125 (million) % 17.74/3.18 % (3991969)Refutation not found, incomplete strategy % 17.74/3.18 % (3991969)------------------------------ % 17.74/3.18 % (3991969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.74/3.18 % (3991969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.74/3.18 % (3991969)CaDiCaL version: 2.1.3 % 17.74/3.18 % (3991969)Termination reason: Refutation not found, incomplete strategy % 17.74/3.18 % (3991969)Time elapsed: 0.007 s % 17.74/3.18 % (3991969)Peak memory usage: 88 MB % 17.74/3.18 % (3991969)Instructions burned: 12 (million) % 17.74/3.18 % (3991961)Instruction limit reached! % 17.74/3.18 % (3991961)------------------------------ % 17.74/3.18 % (3991961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.74/3.18 % (3991961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.74/3.18 % (3991961)CaDiCaL version: 2.1.3 % 17.74/3.18 % (3991961)Termination reason: Instruction limit % 17.74/3.18 % (3991961)Termination phase: Saturation % 17.74/3.18 % (3991961)Time elapsed: 0.261 s % 17.74/3.18 % (3991961)Peak memory usage: 92 MB % 17.74/3.18 % (3991961)Instructions burned: 594 (million) % 17.74/3.18 % (3991973)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=733076089:i=6060:aac=none:ins=25_2989 on theBenchmark for (2989ds/6060Mi) % 17.74/3.18 % (3991970)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3593991432:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/431Mi) % 17.74/3.18 % Exception at run slice level % 17.74/3.18 User error: GNN currently only supports monomorphic FOL. % 17.74/3.18 % Exception at run slice level % 17.74/3.18 User error: GNN currently only supports monomorphic FOL. % 17.74/3.18 % (3991975)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=1156259741:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2988 on theBenchmark for (2988ds/150Mi) % 17.74/3.18 % (3991975)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 17.74/3.18 % (3991976)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1150412889:i=14155:bd=all_2988 on theBenchmark for (2988ds/14155Mi) % 17.74/3.18 % (3991969)------------------------------ % 17.74/3.18 % (3991969)------------------------------ % 17.74/3.18 % (3991975)Instruction limit reached! % 17.74/3.18 % (3991975)------------------------------ % 17.74/3.18 % (3991975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.74/3.18 % (3991975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.74/3.18 % (3991975)CaDiCaL version: 2.1.3 % 17.74/3.18 % (3991975)Termination reason: Instruction limit % 17.74/3.18 % (3991975)Termination phase: Saturation % 24.17/4.07 % (3991975)Time elapsed: 0.089 s % 24.17/4.07 % (3991975)Peak memory usage: 90 MB % 24.17/4.07 % (3991975)Instructions burned: 150 (million) % 24.17/4.07 % Exception at run slice level % 24.17/4.07 User error: GNN currently only supports monomorphic FOL. % 24.17/4.07 % (3991979)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=968497532:i=667:av=off:fsr=off_2987 on theBenchmark for (2987ds/667Mi) % 24.17/4.07 % (3991980)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=3147489033:s2a=on:i=185:s2at=1.8:fdi=4_2987 on theBenchmark for (2987ds/185Mi) % 24.17/4.07 % (3991970)Instruction limit reached! % 24.17/4.07 % (3991970)------------------------------ % 24.17/4.07 % (3991970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.17/4.07 % (3991970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.17/4.07 % (3991970)CaDiCaL version: 2.1.3 % 24.17/4.07 % (3991970)Termination reason: Instruction limit % 24.17/4.07 % (3991970)Termination phase: Saturation % 24.17/4.07 % (3991970)Time elapsed: 0.247 s % 24.17/4.07 % (3991970)Peak memory usage: 91 MB % 24.17/4.07 % (3991970)Instructions burned: 432 (million) % 24.17/4.07 % (3991985)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1765062766:i=12111:sd=1:ss=included_2986 on theBenchmark for (2986ds/12111Mi) % 24.17/4.07 % (3991983)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4089850691:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2986 on theBenchmark for (2986ds/193Mi) % 24.17/4.07 % (3991984)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2104700836:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2986 on theBenchmark for (2986ds/4850Mi) % 24.17/4.07 % (3991980)Instruction limit reached! % 24.17/4.07 % (3991980)------------------------------ % 24.17/4.07 % (3991980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.17/4.07 % (3991980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.17/4.07 % (3991980)CaDiCaL version: 2.1.3 % 24.17/4.07 % (3991980)Termination reason: Instruction limit % 24.17/4.07 % (3991980)Termination phase: Saturation % 24.17/4.07 % (3991980)Time elapsed: 0.120 s % 24.17/4.07 % (3991980)Peak memory usage: 91 MB % 24.17/4.07 % (3991980)Instructions burned: 186 (million) % 24.17/4.07 % (3991988)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2617972153:i=319:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/319Mi) % 24.17/4.07 % (3991983)Instruction limit reached! % 24.17/4.07 % (3991983)------------------------------ % 24.17/4.07 % (3991983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.17/4.07 % (3991983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.17/4.07 % (3991983)CaDiCaL version: 2.1.3 % 24.17/4.07 % (3991983)Termination reason: Instruction limit % 24.17/4.07 % (3991983)Termination phase: Saturation % 24.17/4.07 % (3991983)Time elapsed: 0.117 s % 24.17/4.07 % (3991983)Peak memory usage: 91 MB % 24.17/4.07 % (3991983)Instructions burned: 193 (million) % 24.17/4.07 % Exception at run slice level % 24.17/4.07 User error: GNN currently only supports monomorphic FOL. % 24.17/4.07 % (3991992)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3010487958:i=2064:ep=RST_2984 on theBenchmark for (2984ds/2064Mi) % 24.17/4.07 % (3991979)Instruction limit reached! % 24.17/4.07 % (3991979)------------------------------ % 24.17/4.07 % (3991979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.17/4.07 % (3991979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.17/4.07 % (3991979)CaDiCaL version: 2.1.3 % 24.17/4.07 % (3991979)Termination reason: Instruction limit % 24.17/4.07 % (3991979)Termination phase: Saturation % 24.17/4.07 % (3991979)Time elapsed: 0.289 s % 24.17/4.07 % (3991979)Peak memory usage: 90 MB % 24.17/4.07 % (3991979)Instructions burned: 668 (million) % 24.17/4.07 % Exception at run slice level % 24.17/4.07 User error: GNN currently only supports monomorphic FOL. % 24.17/4.07 % (3991988)Instruction limit reached! % 24.17/4.07 % (3991988)------------------------------ % 24.17/4.07 % (3991988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.17/4.07 % (3991988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.17/4.07 % (3991988)CaDiCaL version: 2.1.3 % 24.17/4.07 % (3991988)Termination reason: Instruction limit % 31.28/5.05 % (3991988)Termination phase: Saturation % 31.28/5.05 % (3991988)Time elapsed: 0.147 s % 31.28/5.05 % (3991988)Peak memory usage: 90 MB % 31.28/5.05 % (3991988)Instructions burned: 320 (million) % 31.28/5.05 % (3991994)dis-1011_128_sil=32000:random_seed=4014506957:i=3706:ep=RST:av=off_2983 on theBenchmark for (2983ds/3706Mi) % 31.28/5.05 % (3991998)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=814643117:i=9925:aac=none_2982 on theBenchmark for (2982ds/9925Mi) % 31.28/5.05 % (3991996)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=587782929:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2983 on theBenchmark for (2983ds/757Mi) % 31.28/5.05 % (3991997)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=719385480:i=13913:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/13913Mi) % 31.28/5.05 % (3991999)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2253411119:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2982 on theBenchmark for (2982ds/2479Mi) % 31.28/5.05 % Exception at run slice level % 31.28/5.05 User error: GNN currently only supports monomorphic FOL. % 31.28/5.05 % (3992005)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3490508239:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2979 on theBenchmark for (2979ds/440Mi) % 31.28/5.05 % (3992005)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 31.28/5.05 % (3991996)Instruction limit reached! % 31.28/5.05 % (3991996)------------------------------ % 31.28/5.05 % (3991996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.28/5.05 % (3991996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.28/5.05 % (3991996)CaDiCaL version: 2.1.3 % 31.28/5.05 % (3991996)Termination reason: Instruction limit % 31.28/5.05 % (3991996)Termination phase: Saturation % 31.28/5.05 % (3991996)Time elapsed: 0.386 s % 31.28/5.05 % (3991996)Peak memory usage: 97 MB % 31.28/5.05 % (3991996)Instructions burned: 758 (million) % 31.28/5.05 % Exception at run slice level % 31.28/5.05 User error: GNN currently only supports monomorphic FOL. % 31.28/5.05 % (3992005)Instruction limit reached! % 31.28/5.05 % (3992005)------------------------------ % 31.28/5.05 % (3992005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.28/5.05 % (3992005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.28/5.05 % (3992005)CaDiCaL version: 2.1.3 % 31.28/5.05 % (3992005)Termination reason: Instruction limit % 31.28/5.05 % (3992005)Termination phase: Saturation % 31.28/5.05 % (3992005)Time elapsed: 0.121 s % 31.28/5.05 % (3992005)Peak memory usage: 89 MB % 31.28/5.05 % (3992005)Instructions burned: 443 (million) % 31.28/5.05 % (3992007)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3401104310:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2977 on theBenchmark for (2977ds/11145Mi) % 31.28/5.05 % (3992008)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=119422086:cts=off:i=3034:av=off:er=known:fsd=on_2977 on theBenchmark for (2977ds/3034Mi) % 31.28/5.05 % (3991992)Instruction limit reached! % 31.28/5.05 % (3991992)------------------------------ % 31.28/5.05 % (3991992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.28/5.05 % (3991992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.28/5.05 % (3991992)CaDiCaL version: 2.1.3 % 31.28/5.05 % (3991992)Termination reason: Instruction limit % 31.28/5.05 % (3991992)Termination phase: Saturation % 31.28/5.05 % (3991992)Time elapsed: 0.687 s % 31.28/5.05 % (3991992)Peak memory usage: 88 MB % 31.28/5.05 % (3991992)Instructions burned: 2066 (million) % 31.28/5.05 % (3992009)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=91434457:st=2:s2a=on:i=524:s2at=2:ss=axioms_2977 on theBenchmark for (2977ds/524Mi) % 31.28/5.05 % (3992009)Instruction limit reached! % 31.28/5.05 % (3992009)------------------------------ % 31.28/5.05 % (3992009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.28/5.05 % (3992009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.28/5.05 % (3992009)CaDiCaL version: 2.1.3 % 31.28/5.05 % (3992009)Termination reason: Instruction limit % 31.28/5.05 % (3992009)Termination phase: Saturation % 31.28/5.05 % (3992009)Time elapsed: 0.136 s % 31.28/5.05 % (3992009)Peak memory usage: 90 MB % 34.46/5.60 % (3992009)Instructions burned: 526 (million) % 34.46/5.60 % (3992013)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=915623351:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2976 on theBenchmark for (2976ds/1016Mi) % 34.46/5.60 % (3992014)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2000185354:i=14123:bd=preordered:ins=4_2974 on theBenchmark for (2974ds/14123Mi) % 34.46/5.60 % Exception at run slice level % 34.46/5.60 User error: GNN currently only supports monomorphic FOL. % 34.46/5.60 % Exception at run slice level % 34.46/5.60 User error: GNN currently only supports monomorphic FOL. % 34.46/5.60 % (3991999)Instruction limit reached! % 34.46/5.60 % (3991999)------------------------------ % 34.46/5.60 % (3991999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.46/5.60 % (3991999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.46/5.60 % (3991999)CaDiCaL version: 2.1.3 % 34.46/5.60 % (3991999)Termination reason: Instruction limit % 34.46/5.60 % (3991999)Termination phase: Saturation % 34.46/5.60 % (3991999)Time elapsed: 0.845 s % 34.46/5.60 % (3991999)Peak memory usage: 89 MB % 34.46/5.60 % (3991999)Instructions burned: 2480 (million) % 34.46/5.60 % Exception at run slice level % 34.46/5.60 User error: GNN currently only supports monomorphic FOL. % 34.46/5.60 % (3992017)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3407466102:i=5781:kws=precedence:bd=all:rawr=on_2972 on theBenchmark for (2972ds/5781Mi) % 34.46/5.60 % (3992018)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=3064236661:i=2448:gtgl=5:bd=preordered:gtg=all_2972 on theBenchmark for (2972ds/2448Mi) % 34.46/5.60 % (3992019)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3108568936:i=3223:kws=precedence:fgj=on:av=off_2972 on theBenchmark for (2972ds/3223Mi) % 34.46/5.60 % (3992020)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=4181842030:st=5.6:i=2033:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/2033Mi) % 34.46/5.60 % (3992013)Instruction limit reached! % 34.46/5.60 % (3992013)------------------------------ % 34.46/5.60 % (3992013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.46/5.60 % (3992013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.46/5.60 % (3992013)CaDiCaL version: 2.1.3 % 34.46/5.60 % (3992013)Termination reason: Instruction limit % 34.46/5.60 % (3992013)Termination phase: Saturation % 34.46/5.60 % (3992013)Time elapsed: 0.439 s % 34.46/5.60 % (3992013)Peak memory usage: 103 MB % 34.46/5.60 % (3992013)Instructions burned: 1017 (million) % 34.46/5.60 % (3991984)Instruction limit reached! % 34.46/5.60 % (3991984)------------------------------ % 34.46/5.60 % (3991984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.46/5.60 % (3991984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.46/5.60 % (3991984)CaDiCaL version: 2.1.3 % 34.46/5.60 % (3991984)Termination reason: Instruction limit % 34.46/5.60 % (3991984)Termination phase: Saturation % 34.46/5.60 % (3991984)Time elapsed: 1.611 s % 34.46/5.60 % (3991984)Peak memory usage: 89 MB % 34.46/5.60 % (3991984)Instructions burned: 4852 (million) % 34.46/5.60 % (3992025)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2821186638:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2970 on theBenchmark for (2970ds/2055Mi) % 34.46/5.60 % Exception at run slice level % 34.46/5.60 User error: GNN currently only supports monomorphic FOL. % 34.46/5.60 % Exception at run slice level % 34.46/5.60 User error: GNN currently only supports monomorphic FOL. % 34.46/5.60 % Exception at run slice level % 34.46/5.60 User error: GNN currently only supports monomorphic FOL. % 34.46/5.60 % (3992026)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=2535552425:i=21611:sd=3:ss=axioms_2968 on theBenchmark for (2968ds/21611Mi) % 34.46/5.60 % (3992028)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=927389583:i=4835:sd=13:ss=axioms:sgt=23_2968 on theBenchmark for (2968ds/4835Mi) % 34.46/5.60 % (3992029)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=2015454283:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2967 on theBenchmark for (2967ds/797Mi) % 42.99/6.86 % (3992030)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2757484031:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2967 on theBenchmark for (2967ds/2326Mi) % 42.99/6.86 % Exception at run slice level % 42.99/6.86 User error: GNN currently only supports monomorphic FOL. % 42.99/6.86 % Exception at run slice level % 42.99/6.86 User error: GNN currently only supports monomorphic FOL. % 42.99/6.86 % (3992035)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1661174137:i=6038:nm=6_2964 on theBenchmark for (2964ds/6038Mi) % 42.99/6.86 % (3992029)Instruction limit reached! % 42.99/6.86 % (3992029)------------------------------ % 42.99/6.86 % (3992029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.99/6.86 % (3992029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.99/6.86 % (3992029)CaDiCaL version: 2.1.3 % 42.99/6.86 % (3992029)Termination reason: Instruction limit % 42.99/6.86 % (3992029)Termination phase: Saturation % 42.99/6.86 % (3992029)Time elapsed: 0.354 s % 42.99/6.86 % (3992029)Peak memory usage: 89 MB % 42.99/6.86 % (3992029)Instructions burned: 798 (million) % 42.99/6.86 % (3992036)lrs+10_1_sil=32000:sp=occurrence:random_seed=790342872:st=2:i=33334:sd=3:ss=included:sgt=32_2963 on theBenchmark for (2963ds/33334Mi) % 42.99/6.86 % (3992038)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=964767757:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2962 on theBenchmark for (2962ds/1008Mi) % 42.99/6.86 % (3991994)Instruction limit reached! % 42.99/6.86 % (3991994)------------------------------ % 42.99/6.86 % (3991994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.99/6.86 % (3991994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.99/6.86 % (3991994)CaDiCaL version: 2.1.3 % 42.99/6.86 % (3991994)Termination reason: Instruction limit % 42.99/6.86 % (3991994)Termination phase: Saturation % 42.99/6.86 % (3991994)Time elapsed: 2.167 s % 42.99/6.86 % (3991994)Peak memory usage: 108 MB % 42.99/6.86 % (3991994)Instructions burned: 3707 (million) % 42.99/6.86 % Exception at run slice level % 42.99/6.86 User error: GNN currently only supports monomorphic FOL. % 42.99/6.86 % (3992041)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=2675233786:i=8327:s2at=5:bd=preordered_2960 on theBenchmark for (2960ds/8327Mi) % 42.99/6.86 % (3992028)Instruction limit reached! % 42.99/6.86 % (3992028)------------------------------ % 42.99/6.86 % (3992028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.99/6.86 % (3992028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.99/6.86 % (3992028)CaDiCaL version: 2.1.3 % 42.99/6.86 % (3992028)Termination reason: Instruction limit % 42.99/6.86 % (3992028)Termination phase: Saturation % 42.99/6.86 % (3992028)Time elapsed: 0.844 s % 42.99/6.86 % (3992028)Peak memory usage: 89 MB % 42.99/6.86 % (3992028)Instructions burned: 4836 (million) % 42.99/6.86 % (3992042)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=639148671:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2959 on theBenchmark for (2959ds/1083Mi) % 42.99/6.86 % (3992030)Instruction limit reached! % 42.99/6.86 % (3992030)------------------------------ % 42.99/6.86 % (3992030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.99/6.86 % (3992030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.99/6.86 % (3992030)CaDiCaL version: 2.1.3 % 42.99/6.86 % (3992030)Termination reason: Instruction limit % 42.99/6.86 % (3992030)Termination phase: Saturation % 42.99/6.86 % (3992030)Time elapsed: 0.800 s % 42.99/6.86 % (3992030)Peak memory usage: 89 MB % 42.99/6.86 % (3992030)Instructions burned: 2328 (million) % 42.99/6.86 % (3992044)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=4054017320:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2958 on theBenchmark for (2958ds/1084Mi) % 42.99/6.86 % (3992046)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2639922254:i=6995:s2at=5:gtg=all_2957 on theBenchmark for (2957ds/6995Mi) % 42.99/6.86 % Exception at run slice level % 42.99/6.86 User error: Immediate (shared) subterms of term/literal hoare_376461865e_case(X1,X0,X5,hoare_1841697145triple(X1,X4,X3,X2)) = sF46(X1,X0,X5,X4,X3,X2) have different types/not well-typed! % 52.21/8.11 % (3992038)Instruction limit reached! % 52.21/8.11 % (3992038)------------------------------ % 52.21/8.11 % (3992038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.21/8.11 % (3992038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.21/8.11 % (3992038)CaDiCaL version: 2.1.3 % 52.21/8.11 % (3992038)Termination reason: Instruction limit % 52.21/8.11 % (3992038)Termination phase: Saturation % 52.21/8.11 % (3992038)Time elapsed: 0.483 s % 52.21/8.11 % (3992038)Peak memory usage: 95 MB % 52.21/8.11 % (3992038)Instructions burned: 1010 (million) % 52.21/8.11 % Exception at run slice level % 52.21/8.11 User error: GNN currently only supports monomorphic FOL. % 52.21/8.11 % (3992044)Instruction limit reached! % 52.21/8.11 % (3992044)------------------------------ % 52.21/8.11 % (3992044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.21/8.11 % (3992044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.21/8.11 % (3992044)CaDiCaL version: 2.1.3 % 52.21/8.11 % (3992044)Termination reason: Instruction limit % 52.21/8.11 % (3992044)Termination phase: Saturation % 52.21/8.11 % (3992044)Time elapsed: 0.269 s % 52.21/8.11 % (3992044)Peak memory usage: 94 MB % 52.21/8.11 % (3992044)Instructions burned: 1087 (million) % 52.21/8.11 % (3992049)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2270531139:st=2:i=6225:sd=15:ss=axioms_2956 on theBenchmark for (2956ds/6225Mi) % 52.21/8.11 % (3992050)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3074423806:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2956 on theBenchmark for (2956ds/3372Mi) % 52.21/8.11 % (3992049)Refutation not found, incomplete strategy % 52.21/8.11 % (3992049)------------------------------ % 52.21/8.11 % (3992049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.21/8.11 % (3992049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.21/8.11 % (3992049)CaDiCaL version: 2.1.3 % 52.21/8.11 % (3992049)Termination reason: Refutation not found, incomplete strategy % 52.21/8.11 % (3992049)Time elapsed: 0.018 s % 52.21/8.11 % (3992049)Peak memory usage: 89 MB % 52.21/8.11 % (3992049)Instructions burned: 33 (million) % 52.21/8.11 % (3992052)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=485964123:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2954 on theBenchmark for (2954ds/13494Mi) % 52.21/8.11 % (3992051)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1317780471:st=2.3:i=26457:sd=10:ss=included:sgt=8_2955 on theBenchmark for (2955ds/26457Mi) % 52.21/8.11 % (3992042)Instruction limit reached! % 52.21/8.11 % (3992042)------------------------------ % 52.21/8.11 % (3992042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.21/8.11 % (3992042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.21/8.11 % (3992042)CaDiCaL version: 2.1.3 % 52.21/8.11 % (3992042)Termination reason: Instruction limit % 52.21/8.11 % (3992042)Termination phase: Saturation % 52.21/8.11 % (3992042)Time elapsed: 0.590 s % 52.21/8.11 % (3992042)Peak memory usage: 100 MB % 52.21/8.11 % (3992042)Instructions burned: 1084 (million) % 52.21/8.11 % (3992049)------------------------------ % 52.21/8.11 % (3992049)------------------------------ % 52.21/8.11 % Exception at run slice level % 52.21/8.11 User error: GNN currently only supports monomorphic FOL. % 52.21/8.11 % Exception at run slice level % 52.21/8.11 User error: GNN currently only supports monomorphic FOL. % 52.21/8.11 % (3992057)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=435696770:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2952 on theBenchmark for (2952ds/2503Mi) % 52.21/8.11 % (3992057)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 52.21/8.11 % (3992059)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4269191775:i=30753:av=off:ss=included_2951 on theBenchmark for (2951ds/30753Mi) % 52.21/8.11 % (3992058)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=2547807672:i=2559:sd=1:ep=RSTC:ss=axioms_2952 on theBenchmark for (2952ds/2559Mi) % 61.42/9.48 % Exception at run slice level % 61.42/9.48 User error: GNN currently only supports monomorphic FOL. % 61.42/9.48 % (3992061)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=442921701:i=26473:ep=RSTC_2950 on theBenchmark for (2950ds/26473Mi) % 61.42/9.48 % Exception at run slice level % 61.42/9.48 User error: GNN currently only supports monomorphic FOL. % 61.42/9.48 % (3992064)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=3485854905:cts=off:i=2759:kws=inv_arity:fgj=on_2950 on theBenchmark for (2950ds/2759Mi) % 61.42/9.48 % (3992066)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=4180109239:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2948 on theBenchmark for (2948ds/5665Mi) % 61.42/9.48 % (3992066)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 61.42/9.48 % Exception at run slice level % 61.42/9.48 User error: GNN currently only supports monomorphic FOL. % 61.42/9.48 % Exception at run slice level % 61.42/9.48 User error: GNN currently only supports monomorphic FOL. % 61.42/9.48 % (3992070)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3381808905:i=1565:sd=2:ss=axioms:sgt=32_2947 on theBenchmark for (2947ds/1565Mi) % 61.42/9.48 % (3992069)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=1478656829:i=1532:ep=RS:ss=axioms_2947 on theBenchmark for (2947ds/1532Mi) % 61.42/9.48 % Exception at run slice level % 61.42/9.48 User error: GNN currently only supports monomorphic FOL. % 61.42/9.48 % Exception at run slice level % 61.42/9.48 User error: GNN currently only supports monomorphic FOL. % 61.42/9.48 % (3992073)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=3214316730:i=1572:fgj=on:gsp=on_2945 on theBenchmark for (2945ds/1572Mi) % 61.42/9.48 % (3992073)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 61.42/9.48 % (3992074)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=3625368663:i=6052:sd=4:ss=axioms:sgt=24_2944 on theBenchmark for (2944ds/6052Mi) % 61.42/9.48 % Exception at run slice level % 61.42/9.48 User error: GNN currently only supports monomorphic FOL. % 61.42/9.48 % Exception at run slice level % 61.42/9.48 User error: GNN currently only supports monomorphic FOL. % 61.42/9.48 % Exception at run slice level % 61.42/9.48 User error: GNN currently only supports monomorphic FOL. % 61.42/9.48 % (3992077)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=2708738601:i=3500:sd=1:bd=preordered:sup=off:ss=included_2942 on theBenchmark for (2942ds/3500Mi) % 61.42/9.48 % (3992078)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=837817033:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2941 on theBenchmark for (2941ds/1842Mi) % 61.42/9.48 % (3992079)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1164308306:i=66096:add=on_2941 on theBenchmark for (2941ds/66096Mi) % 61.42/9.48 % (3992078)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 61.42/9.48 % (3992017)Instruction limit reached! % 61.42/9.48 % (3992017)------------------------------ % 61.42/9.48 % (3992017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.42/9.48 % (3992017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.42/9.48 % (3992017)CaDiCaL version: 2.1.3 % 61.42/9.48 % (3992017)Termination reason: Instruction limit % 61.42/9.48 % (3992017)Termination phase: Saturation % 61.42/9.48 % (3992017)Time elapsed: 3.186 s % 61.42/9.48 % (3992017)Peak memory usage: 109 MB % 61.42/9.48 % (3992017)Instructions burned: 5781 (million) % 61.42/9.48 % Exception at run slice level % 61.42/9.48 User error: GNN currently only supports monomorphic FOL. % 61.42/9.48 % Exception at run slice level % 61.42/9.48 User error: GNN currently only supports monomorphic FOL. % 61.42/9.48 % (3992083)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=1043348043:i=1884:sd=1:nm=60:ss=axioms_2939 on theBenchmark for (2939ds/1884Mi) % 75.29/11.31 % (3992085)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=3508551129:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2939 on theBenchmark for (2939ds/2037Mi) % 75.29/11.31 % (3992084)lrs-1011_4:1_sil=16000:bsr=on:random_seed=1758526032:cts=off:i=5469:bs=on:fsr=off_2939 on theBenchmark for (2939ds/5469Mi) % 75.29/11.31 % Exception at run slice level% Exception at run slice level % 75.29/11.31 % 75.29/11.31 User error: GNN currently only supports monomorphic FOL.User error: % 75.29/11.31 GNN currently only supports monomorphic FOL. % 75.29/11.31 % Exception at run slice level % 75.29/11.31 User error: GNN currently only supports monomorphic FOL. % 75.29/11.31 % (3992089)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2743781453:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2936 on theBenchmark for (2936ds/2110Mi) % 75.29/11.31 % (3992090)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=1056960777:i=2430:add=off:aac=none:nm=16_2936 on theBenchmark for (2936ds/2430Mi) % 75.29/11.31 % (3992091)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=4219119737:cond=fast:i=4891_2935 on theBenchmark for (2935ds/4891Mi) % 75.29/11.31 % Exception at run slice level % 75.29/11.31 User error: GNN currently only supports monomorphic FOL. % 75.29/11.31 % Exception at run slice level % 75.29/11.31 User error: GNN currently only supports monomorphic FOL. % 75.29/11.31 % (3992095)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=3599600087:st=2:i=14845:sd=2:ss=included:fsd=on_2934 on theBenchmark for (2934ds/14845Mi) % 75.29/11.31 % (3992097)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=2760827061:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2932 on theBenchmark for (2932ds/7534Mi) % 75.29/11.31 % Exception at run slice level % 75.29/11.31 User error: GNN currently only supports monomorphic FOL. % 75.29/11.31 % Exception at run slice level % 75.29/11.31 User error: GNN currently only supports monomorphic FOL. % 75.29/11.31 % (3992099)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=2916798347:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2931 on theBenchmark for (2931ds/10353Mi) % 75.29/11.31 % (3992100)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=795689172:i=7860_2931 on theBenchmark for (2931ds/7860Mi) % 75.29/11.31 % (3992100)Refutation not found, incomplete strategy % 75.29/11.31 % (3992100)------------------------------ % 75.29/11.31 % (3992100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.29/11.31 % (3992100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.29/11.31 % (3992100)CaDiCaL version: 2.1.3 % 75.29/11.31 % (3992100)Termination reason: Refutation not found, incomplete strategy % 75.29/11.31 % (3992100)Time elapsed: 0.016 s % 75.29/11.31 % (3992100)Peak memory usage: 89 MB % 75.29/11.31 % (3992100)Instructions burned: 31 (million) % 75.29/11.31 % Exception at run slice level % 75.29/11.31 User error: GNN currently only supports monomorphic FOL. % 75.29/11.31 % Exception at run slice level % 75.29/11.31 User error: GNN currently only supports monomorphic FOL. % 75.29/11.31 % (3992103)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=978880596:i=7896:sd=2:bs=on:ss=included:sgt=20_2929 on theBenchmark for (2929ds/7896Mi) % 75.29/11.31 % (3992104)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=3170131814:i=5812:gtgl=2:gtg=all_2929 on theBenchmark for (2929ds/5812Mi) % 75.29/11.31 % (3992100)------------------------------ % 75.29/11.31 % (3992100)------------------------------ % 75.29/11.31 % Exception at run slice level % 75.29/11.31 User error: GNN currently only supports monomorphic FOL. % 75.29/11.31 % Exception at run slice level % 75.29/11.31 User error: GNN currently only supports monomorphic FOL. % 75.29/11.31 % (3992107)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=474583744:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2927 on theBenchmark for (2927ds/2965Mi) % 111.09/16.37 % (3992108)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=379136957:i=2967:kws=precedence:bd=preordered:av=off_2926 on theBenchmark for (2926ds/2967Mi) % 111.09/16.37 % (3992109)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=3803657617:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2926 on theBenchmark for (2926ds/3022Mi) % 111.09/16.37 % Exception at run slice level % 111.09/16.37 User error: GNN currently only supports monomorphic FOL. % 111.09/16.37 % Exception at run slice level % 111.09/16.37 User error: GNN currently only supports monomorphic FOL. % 111.09/16.37 % (3992113)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=769184647:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2923 on theBenchmark for (2923ds/3207Mi) % 111.09/16.37 % (3992114)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=3854214318:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2923 on theBenchmark for (2923ds/3289Mi) % 111.09/16.37 % Exception at run slice level % 111.09/16.37 User error: GNN currently only supports monomorphic FOL. % 111.09/16.37 % Exception at run slice level % 111.09/16.37 User error: GNN currently only supports monomorphic FOL. % 111.09/16.37 % (3992117)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=4234400991:i=38569:sd=3:ss=axioms:sgt=32_2921 on theBenchmark for (2921ds/38569Mi) % 111.09/16.37 % Exception at run slice level % 111.09/16.37 User error: GNN currently only supports monomorphic FOL. % 111.09/16.37 % (3992118)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=3369815485:cts=off:i=3394_2920 on theBenchmark for (2920ds/3394Mi) % 111.09/16.37 % (3992120)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=3297753890:i=33824:bd=preordered_2919 on theBenchmark for (2919ds/33824Mi) % 111.09/16.37 % Exception at run slice level % 111.09/16.37 User error: GNN currently only supports monomorphic FOL. % 111.09/16.37 % (3992123)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=1104032546:i=20684:bd=all:gtg=exists_sym_2918 on theBenchmark for (2918ds/20684Mi) % 111.09/16.37 % Exception at run slice level % 111.09/16.37 User error: GNN currently only supports monomorphic FOL. % 111.09/16.37 % Exception at run slice level % 111.09/16.37 User error: GNN currently only supports monomorphic FOL. % 111.09/16.37 % Exception at run slice level % 111.09/16.37 User error: GNN currently only supports monomorphic FOL. % 111.09/16.37 % (3992125)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=1634682587: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_2916 on theBenchmark for (2916ds/7222Mi) % 111.09/16.37 % (3992125)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 111.09/16.37 % (3992126)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=2281245176:st=4:i=7295:sd=4:ep=R:ss=axioms_2916 on theBenchmark for (2916ds/7295Mi) % 111.09/16.37 % (3992128)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=577205921:i=4036:ins=10_2915 on theBenchmark for (2915ds/4036Mi) % 111.09/16.37 % Exception at run slice level % 111.09/16.37 User error: GNN currently only supports monomorphic FOL. % 111.09/16.37 % Exception at run slice level % 111.09/16.37 User error: GNN currently only supports monomorphic FOL. % 111.09/16.37 % (3992131)lrs+10_1_sil=128000:lcm=predicate:random_seed=2119766780:st=3:i=43697:sd=5:ss=axioms_2913 on theBenchmark for (2913ds/43697Mi) % 111.09/16.37 % (3992132)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=562589873:i=17599:gtg=all:ss=axioms:fsd=on_2913 on theBenchmark for (2913ds/17599Mi) % 139.71/20.41 % Exception at run slice level % 139.71/20.41 User error: GNN currently only supports monomorphic FOL. % 139.71/20.41 % Exception at run slice level % 139.71/20.41 User error: GNN currently only supports monomorphic FOL. % 139.71/20.41 % (3992135)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=3240214223:i=4547:bd=preordered_2911 on theBenchmark for (2911ds/4547Mi) % 139.71/20.41 % (3992136)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=1577192720:i=9294:av=off_2910 on theBenchmark for (2910ds/9294Mi) % 139.71/20.41 % Exception at run slice level % 139.71/20.41 User error: GNN currently only supports monomorphic FOL. % 139.71/20.41 % (3992139)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1106391573:i=32849:add=on_2908 on theBenchmark for (2908ds/32849Mi) % 139.71/20.41 % Exception at run slice level % 139.71/20.41 User error: GNN currently only supports monomorphic FOL. % 139.71/20.41 % Exception at run slice level % 139.71/20.41 User error: GNN currently only supports monomorphic FOL. % 139.71/20.41 % (3992141)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1546735667:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2905 on theBenchmark for (2905ds/4793Mi) % 139.71/20.41 % (3992142)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=720960956:i=4840:nm=4:av=off_2904 on theBenchmark for (2904ds/4840Mi) % 139.71/20.41 % Exception at run slice level % 139.71/20.41 User error: GNN currently only supports monomorphic FOL. % 139.71/20.41 % (3992084)Instruction limit reached! % 139.71/20.41 % (3992084)------------------------------ % 139.71/20.41 % (3992084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.71/20.41 % (3992084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.71/20.41 % (3992084)CaDiCaL version: 2.1.3 % 139.71/20.41 % (3992084)Termination reason: Instruction limit % 139.71/20.41 % (3992084)Termination phase: Saturation % 139.71/20.41 % (3992084)Time elapsed: 3.663 s % 139.71/20.41 % (3992084)Peak memory usage: 116 MB % 139.71/20.41 % (3992084)Instructions burned: 5470 (million) % 139.71/20.41 % (3992145)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=2389161022:cts=off:i=5002_2902 on theBenchmark for (2902ds/5002Mi) % 139.71/20.41 % Exception at run slice level % 139.71/20.41 User error: GNN currently only supports monomorphic FOL. % 139.71/20.41 % (3992146)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=1958878493:i=30479:sd=3:ss=axioms_2901 on theBenchmark for (2901ds/30479Mi) % 139.71/20.41 % Exception at run slice level % 139.71/20.41 User error: GNN currently only supports monomorphic FOL. % 139.71/20.41 % (3992148)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=1772791543:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2900 on theBenchmark for (2900ds/11035Mi) % 139.71/20.41 % (3992148)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 139.71/20.41 % (3992150)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=100089813:i=5835_2899 on theBenchmark for (2899ds/5835Mi) % 139.71/20.41 % Exception at run slice level % 139.71/20.41 User error: GNN currently only supports monomorphic FOL. % 139.71/20.41 % Exception at run slice level % 139.71/20.41 User error: GNN currently only supports monomorphic FOL. % 139.71/20.41 % (3992153)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=4222006935:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2897 on theBenchmark for (2897ds/5890Mi) % 139.71/20.41 % Exception at run slice level % 139.71/20.41 User error: GNN currently only supports monomorphic FOL. % 139.71/20.41 % Exception at run slice level % 139.71/20.41 User error: GNN currently only supports monomorphic FOL. % 139.71/20.41 % (3992154)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=55823381:cts=off:i=19910:ep=RS_2895 on theBenchmark for (2895ds/19910Mi) % 139.71/20.41 % (3992156)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=1639356139:i=20312:bd=preordered:fsr=off:er=filter_2895 on theBenchmark for (2895ds/20312Mi) % 162.88/23.68 % (3992157)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=369931464:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2894 on theBenchmark for (2894ds/13822Mi) % 162.88/23.68 % Exception at run slice level % 162.88/23.68 User error: GNN currently only supports monomorphic FOL. % 162.88/23.68 % (3992161)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=2497289554:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2892 on theBenchmark for (2892ds/7144Mi) % 162.88/23.68 % Exception at run slice level % 162.88/23.68 User error: GNN currently only supports monomorphic FOL. % 162.88/23.68 % Exception at run slice level % 162.88/23.68 User error: GNN currently only supports monomorphic FOL. % 162.88/23.68 % (3992163)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=3571060721:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2889 on theBenchmark for (2889ds/15184Mi) % 162.88/23.68 % (3992164)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=4272039651:i=107375_2888 on theBenchmark for (2888ds/107375Mi) % 162.88/23.68 % Exception at run slice level % 162.88/23.68 User error: GNN currently only supports monomorphic FOL. % 162.88/23.68 % Exception at run slice level % 162.88/23.68 User error: GNN currently only supports monomorphic FOL. % 162.88/23.68 % (3992167)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=3884698445:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2884 on theBenchmark for (2884ds/7958Mi) % 162.88/23.68 % (3992168)dis+10_128_sil=16000:nwc=0.7:random_seed=2687876025:i=15999:nm=2:gsp=on_2883 on theBenchmark for (2883ds/15999Mi) % 162.88/23.68 % (3992168)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 162.88/23.68 % Exception at run slice level % 162.88/23.68 User error: GNN currently only supports monomorphic FOL. % 162.88/23.68 % (3992171)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=2134032570:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2879 on theBenchmark for (2879ds/8139Mi) % 162.88/23.68 % (3992161)Instruction limit reached! % 162.88/23.68 % (3992161)------------------------------ % 162.88/23.68 % (3992161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.88/23.68 % (3992161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.88/23.68 % (3992161)CaDiCaL version: 2.1.3 % 162.88/23.68 % (3992161)Termination reason: Instruction limit % 162.88/23.68 % (3992161)Termination phase: Saturation % 162.88/23.68 % (3992161)Time elapsed: 3.646 s % 162.88/23.68 % (3992161)Peak memory usage: 245 MB % 162.88/23.68 % (3992161)Instructions burned: 7145 (million) % 162.88/23.68 % (3992173)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=1730596355:st=4:i=8950:sd=5:ss=axioms_2853 on theBenchmark for (2853ds/8950Mi) % 162.88/23.68 % Exception at run slice level % 162.88/23.68 User error: GNN currently only supports monomorphic FOL. % 162.88/23.68 % (3992175)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=2895718832:i=9809:ins=10:av=off_2848 on theBenchmark for (2848ds/9809Mi) % 162.88/23.68 % (3992171)Instruction limit reached! % 162.88/23.68 % (3992171)------------------------------ % 162.88/23.68 % (3992171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.88/23.68 % (3992171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.88/23.68 % (3992171)CaDiCaL version: 2.1.3 % 162.88/23.68 % (3992171)Termination reason: Instruction limit % 162.88/23.68 % (3992171)Termination phase: Saturation % 162.88/23.68 % (3992171)Time elapsed: 3.316 s % 162.88/23.68 % (3992171)Peak memory usage: 91 MB % 162.88/23.68 % (3992171)Instructions burned: 8142 (million) % 162.88/23.68 % Exception at run slice level % 162.88/23.68 User error: GNN currently only supports monomorphic FOL. % 162.88/23.68 % (3992177)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=3661513607:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2844 on theBenchmark for (2844ds/9885Mi) % 181.21/26.21 % (3992178)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=2162584337:cond=fast:i=32078:fgj=on:av=off_2843 on theBenchmark for (2843ds/32078Mi) % 181.21/26.21 % Exception at run slice level % 181.21/26.21 User error: GNN currently only supports monomorphic FOL. % 181.21/26.21 % Exception at run slice level % 181.21/26.21 User error: GNN currently only supports monomorphic FOL. % 181.21/26.21 % (3992181)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=3508734048:i=11101:bd=all:ss=axioms:sgt=8_2839 on theBenchmark for (2839ds/11101Mi) % 181.21/26.21 % (3992182)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=3550188518:cond=on:i=13220:s2at=3:aac=none:fsd=on_2837 on theBenchmark for (2837ds/13220Mi) % 181.21/26.21 % Exception at run slice level % 181.21/26.21 User error: GNN currently only supports monomorphic FOL. % 181.21/26.21 % (3992185)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=3914128671:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2832 on theBenchmark for (2832ds/13528Mi) % 181.21/26.21 % Exception at run slice level % 181.21/26.21 User error: GNN currently only supports monomorphic FOL. % 181.21/26.21 % (3992188)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=1514075306:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2827 on theBenchmark for (2827ds/14854Mi) % 181.21/26.21 % Exception at run slice level % 181.21/26.21 User error: GNN currently only supports monomorphic FOL. % 181.21/26.21 % (3992190)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=4194078104:i=14974:ss=axioms:sgt=16_2821 on theBenchmark for (2821ds/14974Mi) % 181.21/26.21 % Exception at run slice level % 181.21/26.21 User error: GNN currently only supports monomorphic FOL. % 181.21/26.21 % (3992192)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=2369749185:i=33081:aac=none:fgj=on:bd=all:fsr=off_2816 on theBenchmark for (2816ds/33081Mi) % 181.21/26.21 % Exception at run slice level % 181.21/26.21 User error: GNN currently only supports monomorphic FOL. % 181.21/26.21 % (3992194)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=2419263246:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2811 on theBenchmark for (2811ds/50856Mi) % 181.21/26.21 % Exception at run slice level % 181.21/26.21 User error: GNN currently only supports monomorphic FOL. % 181.21/26.21 % (3992061)Instruction limit reached! % 181.21/26.21 % (3992061)------------------------------ % 181.21/26.21 % (3992061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.21/26.21 % (3992061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.21/26.21 % (3992061)CaDiCaL version: 2.1.3 % 181.21/26.21 % (3992061)Termination reason: Instruction limit % 181.21/26.21 % (3992061)Termination phase: Saturation % 181.21/26.21 % (3992061)Time elapsed: 14.483 s % 181.21/26.21 % (3992061)Peak memory usage: 528 MB % 181.21/26.21 % (3992061)Instructions burned: 26474 (million) % 181.21/26.21 % (3992196)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=1179766269:i=69865_2805 on theBenchmark for (2805ds/69865Mi) % 181.21/26.21 % (3992168)Instruction limit reached! % 181.21/26.21 % (3992168)------------------------------ % 181.21/26.21 % (3992168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.21/26.21 % (3992168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.21/26.21 % (3992168)CaDiCaL version: 2.1.3 % 181.21/26.21 % (3992168)Termination reason: Instruction limit % 181.21/26.21 % (3992168)Termination phase: Saturation % 181.21/26.21 % (3992168)Time elapsed: 7.775 s % 181.21/26.21 % (3992168)Peak memory usage: 110 MB % 181.21/26.21 % (3992168)Instructions burned: 16000 (million) % 181.21/26.21 % (3992198)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=709039930:cond=fast:i=17802:gtgl=3:gtg=all_2804 on theBenchmark for (2804ds/17802Mi) % 181.21/26.21 % Exception at run slice level % 181.21/26.21 User error: Immediate (shared) subterms of term/literal hoare_376461865e_case(X1,X0,X5,hoare_1841697145triple(X1,X4,X3,X2)) = sF83(X1,X0,X5,X4,X3,X2) have different types/not well-typed! % 191.42/27.73 % (3992199)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=4183687804:i=96644_2803 on theBenchmark for (2803ds/96644Mi) % 191.42/27.73 % (3992201)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 191.42/27.73 % (3992201)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=3557706301:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2802 on theBenchmark for (2802ds/21161Mi) % 191.42/27.73 % Exception at run slice level % 191.42/27.73 User error: GNN currently only supports monomorphic FOL. % 191.42/27.73 % (3992154)Instruction limit reached! % 191.42/27.73 % (3992154)------------------------------ % 191.42/27.73 % (3992154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.42/27.73 % (3992154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.42/27.73 % (3992154)CaDiCaL version: 2.1.3 % 191.42/27.73 % (3992154)Termination reason: Instruction limit % 191.42/27.73 % (3992154)Termination phase: Saturation % 191.42/27.73 % (3992154)Time elapsed: 9.385 s % 191.42/27.73 % (3992154)Peak memory usage: 136 MB % 191.42/27.73 % (3992154)Instructions burned: 19911 (million) % 191.42/27.73 % (3992204)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=1651458599:i=22761:gtg=all:ss=axioms:fsd=on_2800 on theBenchmark for (2800ds/22761Mi) % 191.42/27.73 % (3992205)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=2719633473:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2800 on theBenchmark for (2800ds/23713Mi) % 191.42/27.73 % Exception at run slice level % 191.42/27.73 User error: GNN currently only supports monomorphic FOL. % 191.42/27.73 % (3992208)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=1529278870:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2795 on theBenchmark for (2795ds/26509Mi) % 191.42/27.73 % Exception at run slice level % 191.42/27.73 User error: GNN currently only supports monomorphic FOL. % 191.42/27.73 % (3992210)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=4074689271:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2790 on theBenchmark for (2790ds/28957Mi) % 191.42/27.73 % (3992036)Instruction limit reached! % 191.42/27.73 % (3992036)------------------------------ % 191.42/27.73 % (3992036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.42/27.73 % (3992036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.42/27.73 % (3992036)CaDiCaL version: 2.1.3 % 191.42/27.73 % (3992036)Termination reason: Instruction limit % 191.42/27.73 % (3992036)Termination phase: Saturation % 191.42/27.73 % (3992036)Time elapsed: 18.554 s % 191.42/27.73 % (3992036)Peak memory usage: 150 MB % 191.42/27.73 % (3992036)Instructions burned: 33334 (million) % 191.42/27.73 % (3992212)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=4072556087:i=29246:s2at=-1:kws=inv_arity:ins=10_2776 on theBenchmark for (2776ds/29246Mi) % 191.42/27.73 % Exception at run slice level % 191.42/27.73 User error: GNN currently only supports monomorphic FOL. % 191.42/27.73 % (3992181)Instruction limit reached! % 191.42/27.73 % (3992181)------------------------------ % 191.42/27.73 % (3992181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.42/27.73 % (3992181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.42/27.73 % (3992181)CaDiCaL version: 2.1.3 % 191.42/27.73 % (3992181)Termination reason: Instruction limit % 191.42/27.73 % (3992181)Termination phase: Saturation % 191.42/27.73 % (3992181)Time elapsed: 6.643 s % 191.42/27.73 % (3992181)Peak memory usage: 150 MB % 191.42/27.73 % (3992181)Instructions burned: 11103 (million) % 191.42/27.73 % (3992214)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=2319487351:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2771 on theBenchmark for (2771ds/30082Mi) % 191.42/27.73 % (3992214)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 196.18/28.48 % (3992215)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=1110141525:i=32262:bd=preordered_2771 on theBenchmark for (2771ds/32262Mi) % 196.18/28.48 % Exception at run slice level % 196.18/28.48 User error: GNN currently only supports monomorphic FOL. % 196.18/28.48 % Exception at run slice level % 196.18/28.48 User error: GNN currently only supports monomorphic FOL. % 196.18/28.48 % (3992218)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=1484069801:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2766 on theBenchmark for (2766ds/32870Mi) % 196.18/28.48 % (3992219)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=109097111:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2766 on theBenchmark for (2766ds/33295Mi) % 196.18/28.48 % (3992131)Instruction limit reached! % 196.18/28.48 % (3992131)------------------------------ % 196.18/28.48 % (3992131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.18/28.48 % (3992131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.18/28.48 % (3992131)CaDiCaL version: 2.1.3 % 196.18/28.48 % (3992131)Termination reason: Instruction limit % 196.18/28.48 % (3992131)Termination phase: Saturation % 196.18/28.48 % (3992131)Time elapsed: 14.839 s % 196.18/28.48 % (3992131)Peak memory usage: 335 MB % 196.18/28.48 % (3992131)Instructions burned: 43699 (million) % 196.18/28.48 % (3992222)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=2794833095:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2763 on theBenchmark for (2763ds/36826Mi) % 196.18/28.48 % Exception at run slice level % 196.18/28.48 User error: GNN currently only supports monomorphic FOL. % 196.18/28.48 % Exception at run slice level % 196.18/28.48 User error: GNN currently only supports monomorphic FOL. % 196.18/28.48 % (3992224)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=1226365566:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2761 on theBenchmark for (2761ds/92981Mi) % 196.18/28.48 % (3992225)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=1320461856:s2pl=on:i=49423_2761 on theBenchmark for (2761ds/49423Mi) % 196.18/28.48 % Exception at run slice level % 196.18/28.48 User error: GNN currently only supports monomorphic FOL. % 196.18/28.48 % Exception at run slice level % 196.18/28.48 User error: GNN currently only supports monomorphic FOL. % 196.18/28.48 % (3992228)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=520919984:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2756 on theBenchmark for (2756ds/57299Mi) % 196.18/28.48 % (3992229)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=3871798673:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2755 on theBenchmark for (2755ds/127679Mi) % 196.18/28.48 % Exception at run slice level % 196.18/28.48 User error: GNN currently only supports monomorphic FOL. % 196.18/28.48 % Exception at run slice level % 196.18/28.48 User error: GNN currently only supports monomorphic FOL. % 196.18/28.48 % (3992232)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=2598857395:i=69402:add=on:aac=none:fsr=off_2751 on theBenchmark for (2751ds/69402Mi) % 196.18/28.48 % (3992233)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=1617808736:i=100512:doe=on:fgj=on:bd=all:fsd=on_2750 on theBenchmark for (2750ds/100512Mi) % 196.18/28.48 % Exception at run slice level % 196.18/28.48 User error: GNN currently only supports monomorphic FOL. % 196.18/28.48 % Exception at run slice level % 196.18/28.48 User error: GNN currently only supports monomorphic FOL. % 196.18/28.48 % (3992236)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=3347245248:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2746 on theBenchmark for (2746ds/138761Mi) % 204.55/29.52 % (3992237)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=948502167:i=282386:rtra=on_2745 on theBenchmark for (2745ds/282386Mi) % 204.55/29.52 % Exception at run slice level % 204.55/29.52 User error: GNN currently only supports monomorphic FOL. % 204.55/29.52 % Exception at run slice level % 204.55/29.52 User error: GNN currently only supports monomorphic FOL. % 204.55/29.52 % (3992240)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=1603459463:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2740 on theBenchmark for (2740ds/269354Mi) % 204.55/29.52 % (3992241)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=2887590431:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2740 on theBenchmark for (2740ds/283390Mi) % 204.55/29.52 % (3992241)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 204.55/29.52 % Exception at run slice level % 204.55/29.52 User error: GNN currently only supports monomorphic FOL. % 204.55/29.52 % Exception at run slice level % 204.55/29.52 User error: GNN currently only supports monomorphic FOL. % 204.55/29.52 % (3992244)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=2709879922:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2735 on theBenchmark for (2735ds/218Mi) % 204.55/29.52 % (3992244)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 204.55/29.52 % (3992244)Refutation not found, incomplete strategy % 204.55/29.52 % (3992244)------------------------------ % 204.55/29.52 % (3992244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.55/29.52 % (3992244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.55/29.52 % (3992244)CaDiCaL version: 2.1.3 % 204.55/29.52 % (3992244)Termination reason: Refutation not found, incomplete strategy % 204.55/29.52 % (3992244)Time elapsed: 0.011 s % 204.55/29.52 % (3992244)Peak memory usage: 89 MB % 204.55/29.52 % (3992244)Instructions burned: 18 (million) % 204.55/29.52 % (3992245)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=4054823450:i=238:av=off:rtra=on:ss=axioms_2735 on theBenchmark for (2735ds/238Mi) % 204.55/29.52 % (3992245)Instruction limit reached! % 204.55/29.52 % (3992245)------------------------------ % 204.55/29.52 % (3992245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.55/29.52 % (3992245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.55/29.52 % (3992245)CaDiCaL version: 2.1.3 % 204.55/29.52 % (3992245)Termination reason: Instruction limit % 204.55/29.52 % (3992245)Termination phase: Saturation % 204.55/29.52 % (3992245)Time elapsed: 0.147 s % 204.55/29.52 % (3992245)Peak memory usage: 89 MB % 204.55/29.52 % (3992245)Instructions burned: 238 (million) % 204.55/29.52 % (3992244)------------------------------ % 204.55/29.52 % (3992244)------------------------------ % 204.55/29.52 % (3992201)Instruction limit reached! % 204.55/29.52 % (3992201)------------------------------ % 204.55/29.52 % (3992201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.55/29.52 % (3992201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.55/29.52 % (3992201)CaDiCaL version: 2.1.3 % 204.55/29.52 % (3992201)Termination reason: Instruction limit % 204.55/29.52 % (3992201)Termination phase: Saturation % 204.55/29.52 % (3992201)Time elapsed: 6.954 s % 204.55/29.52 % (3992201)Peak memory usage: 105 MB % 204.55/29.52 % (3992201)Instructions burned: 21162 (million) % 204.55/29.52 % (3992248)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=3740424488:s2a=on:i=278:rtra=on:gtg=position_2732 on theBenchmark for (2732ds/278Mi) % 204.55/29.52 % (3992249)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=55059878:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2731 on theBenchmark for (2731ds/258Mi) % 204.55/29.52 % (3992250)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=2379430236:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2731 on theBenchmark for (2731ds/570Mi) % 204.55/29.52 % (3992248)Instruction limit reached! % 204.55/29.52 % (3992248)------------------------------ % 204.55/29.52 % (3992248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.55/29.52 % (3992248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.55/29.52 % (3992248)CaDiCaL version: 2.1.3 % 212.28/30.73 % (3992248)Termination reason: Instruction limit % 212.28/30.73 % (3992248)Termination phase: Saturation % 212.28/30.73 % (3992248)Time elapsed: 0.168 s % 212.28/30.73 % (3992248)Peak memory usage: 90 MB % 212.28/30.73 % (3992248)Instructions burned: 279 (million) % 212.28/30.73 % (3992249)Instruction limit reached! % 212.28/30.73 % (3992249)------------------------------ % 212.28/30.73 % (3992249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.28/30.73 % (3992249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.28/30.73 % (3992249)CaDiCaL version: 2.1.3 % 212.28/30.73 % (3992249)Termination reason: Instruction limit % 212.28/30.73 % (3992249)Termination phase: Saturation % 212.28/30.73 % (3992249)Time elapsed: 0.139 s % 212.28/30.73 % (3992249)Peak memory usage: 90 MB % 212.28/30.73 % (3992249)Instructions burned: 259 (million) % 212.28/30.73 % (3992254)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=1937552443:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2729 on theBenchmark for (2729ds/314Mi) % 212.28/30.73 % (3992255)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=405412868:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2728 on theBenchmark for (2728ds/650Mi) % 215.70/31.11 % (3992250)Instruction limit reached! % 215.70/31.11 % (3992250)------------------------------ % 215.70/31.11 % (3992250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.70/31.11 % (3992250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.70/31.11 % (3992250)CaDiCaL version: 2.1.3 % 215.70/31.11 % (3992250)Termination reason: Instruction limit % 215.70/31.11 % (3992250)Termination phase: Saturation % 215.70/31.11 % (3992250)Time elapsed: 0.341 s % 215.70/31.11 % (3992250)Peak memory usage: 93 MB % 215.70/31.11 % (3992250)Instructions burned: 571 (million) % 215.70/31.11 % (3992254)Instruction limit reached! % 215.70/31.11 % (3992254)------------------------------ % 215.70/31.11 % (3992254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.70/31.11 % (3992254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.70/31.11 % (3992254)CaDiCaL version: 2.1.3 % 215.70/31.11 % (3992254)Termination reason: Instruction limit % 215.70/31.11 % (3992254)Termination phase: Saturation % 215.70/31.11 % (3992254)Time elapsed: 0.171 s % 215.70/31.11 % (3992254)Peak memory usage: 92 MB % 215.70/31.11 % (3992254)Instructions burned: 314 (million) % 215.70/31.11 % (3992258)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=1734787158:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2726 on theBenchmark for (2726ds/496Mi) % 215.70/31.11 % (3992259)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=2556312014:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2726 on theBenchmark for (2726ds/588Mi) % 215.70/31.11 % (3992255)Instruction limit reached! % 215.70/31.11 % (3992255)------------------------------ % 215.70/31.11 % (3992255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.70/31.11 % (3992255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.70/31.11 % (3992255)CaDiCaL version: 2.1.3 % 215.70/31.11 % (3992255)Termination reason: Instruction limit % 215.70/31.11 % (3992255)Termination phase: Saturation % 215.70/31.11 % (3992255)Time elapsed: 0.278 s % 215.70/31.11 % (3992255)Peak memory usage: 90 MB % 215.70/31.11 % (3992255)Instructions burned: 651 (million) % 215.70/31.11 % (3992262)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=198907634:i=4700:rtra=on_2724 on theBenchmark for (2724ds/4700Mi) % 215.70/31.11 % (3992258)Instruction limit reached! % 215.70/31.11 % (3992258)------------------------------ % 215.70/31.11 % (3992258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.70/31.11 % (3992258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.70/31.11 % (3992258)CaDiCaL version: 2.1.3 % 215.70/31.11 % (3992258)Termination reason: Instruction limit % 215.70/31.11 % (3992258)Termination phase: Saturation % 215.70/31.11 % (3992258)Time elapsed: 0.243 s % 215.70/31.11 % (3992258)Peak memory usage: 91 MB % 215.70/31.11 % (3992258)Instructions burned: 498 (million) % 215.70/31.11 % (3992259)Instruction limit reached! % 215.70/31.11 % (3992259)------------------------------ % 215.70/31.11 % (3992259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.70/31.11 % (3992259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.70/31.11 % (3992259)CaDiCaL version: 2.1.3 % 215.70/31.11 % (3992259)Termination reason: Instruction limit % 215.70/31.11 % (3992259)Termination phase: Saturation % 215.70/31.11 % (3992259)Time elapsed: 0.270 s % 218.46/31.56 % (3992259)Peak memory usage: 90 MB % 218.46/31.56 % (3992259)Instructions burned: 588 (million) % 218.46/31.56 % (3992264)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1083878885:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2722 on theBenchmark for (2722ds/226Mi) % 218.46/31.56 % (3992265)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2816173860:i=254:av=off:fsr=off:rtra=on:sup=off_2721 on theBenchmark for (2721ds/254Mi) % 218.46/31.56 % (3992264)Instruction limit reached! % 218.46/31.56 % (3992264)------------------------------ % 218.46/31.56 % (3992264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.46/31.56 % (3992264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.46/31.56 % (3992264)CaDiCaL version: 2.1.3 % 218.46/31.56 % (3992264)Termination reason: Instruction limit % 218.46/31.56 % (3992264)Termination phase: Saturation % 218.46/31.56 % (3992264)Time elapsed: 0.124 s % 218.46/31.56 % (3992264)Peak memory usage: 90 MB % 218.46/31.56 % (3992264)Instructions burned: 227 (million) % 218.46/31.56 % (3992265)Instruction limit reached! % 218.46/31.56 % (3992265)------------------------------ % 218.46/31.56 % (3992265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.46/31.56 % (3992265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.46/31.56 % (3992265)CaDiCaL version: 2.1.3 % 218.46/31.56 % (3992265)Termination reason: Instruction limit % 218.46/31.56 % (3992265)Termination phase: Saturation % 218.46/31.56 % (3992265)Time elapsed: 0.113 s % 218.46/31.56 % (3992265)Peak memory usage: 88 MB % 218.46/31.56 % (3992265)Instructions burned: 255 (million) % 218.46/31.56 % Exception at run slice level % 218.46/31.56 User error: GNN currently only supports monomorphic FOL. % 218.46/31.56 % (3992268)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=3263312472:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2719 on theBenchmark for (2719ds/228Mi) % 218.46/31.56 % (3992269)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=198503390:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2719 on theBenchmark for (2719ds/1814Mi) % 218.46/31.56 % (3992270)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=4002595582:i=874:sd=1:aac=none:rtra=on:ss=included_2719 on theBenchmark for (2719ds/874Mi) % 218.46/31.56 % (3992268)Instruction limit reached! % 218.46/31.56 % (3992268)------------------------------ % 218.46/31.56 % (3992268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.46/31.56 % (3992268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.46/31.56 % (3992268)CaDiCaL version: 2.1.3 % 218.46/31.56 % (3992268)Termination reason: Instruction limit % 218.46/31.56 % (3992268)Termination phase: Saturation % 218.46/31.56 % (3992268)Time elapsed: 0.125 s % 218.46/31.56 % (3992268)Peak memory usage: 90 MB % 218.46/31.56 % (3992268)Instructions burned: 228 (million) % 218.46/31.56 % (3992274)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=3857420733:i=10404:rtra=on:ss=axioms:sgt=16_2716 on theBenchmark for (2716ds/10404Mi) % 218.46/31.56 % (3992270)Instruction limit reached! % 218.46/31.56 % (3992270)------------------------------ % 218.46/31.56 % (3992270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.46/31.56 % (3992270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.46/31.56 % (3992270)CaDiCaL version: 2.1.3 % 218.46/31.56 % (3992270)Termination reason: Instruction limit % 218.46/31.56 % (3992270)Termination phase: Saturation % 218.46/31.56 % (3992270)Time elapsed: 0.319 s % 218.46/31.56 % (3992270)Peak memory usage: 89 MB % 218.46/31.56 % (3992270)Instructions burned: 875 (million) % 218.46/31.56 % (3992276)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2704262033:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2714 on theBenchmark for (2714ds/268Mi) % 218.46/31.56 % Exception at run slice level % 218.46/31.56 User error: GNN currently only supports monomorphic FOL. % 218.46/31.56 % (3992276)Instruction limit reached! % 218.46/31.56 % (3992276)------------------------------ % 218.46/31.56 % (3992276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.46/31.56 % (3992276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.46/31.56 % (3992276)CaDiCaL version: 2.1.3 % 218.46/31.56 % (3992276)Termination reason: Instruction limit % 218.46/31.56 % (3992276)Termination phase: Saturation % 218.46/31.56 % (3992276)Time elapsed: 0.150 s % 218.46/31.56 % (3992276)Peak memory usage: 91 MB % 218.46/31.56 % (3992276)Instructions burned: 269 (million) % 231.30/33.38 % (3992279)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=351713845:st=3:i=26386:sd=3:rtra=on:ss=axioms_2711 on theBenchmark for (2711ds/26386Mi) % 231.30/33.38 % (3992278)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=3423642625:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2711 on theBenchmark for (2711ds/1184Mi) % 231.30/33.38 % (3992269)Instruction limit reached! % 231.30/33.38 % (3992269)------------------------------ % 231.30/33.38 % (3992269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.30/33.38 % (3992269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.30/33.38 % (3992269)CaDiCaL version: 2.1.3 % 231.30/33.38 % (3992269)Termination reason: Instruction limit % 231.30/33.38 % (3992269)Termination phase: Saturation % 231.30/33.38 % (3992269)Time elapsed: 1.001 s % 231.30/33.38 % (3992269)Peak memory usage: 94 MB % 231.30/33.38 % (3992269)Instructions burned: 1815 (million) % 231.30/33.38 % Exception at run slice level % 231.30/33.38 User error: GNN currently only supports monomorphic FOL. % 231.30/33.38 % (3992282)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=962910170:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2707 on theBenchmark for (2707ds/250Mi) % 231.30/33.38 % (3992282)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 231.30/33.38 % (3992278)Instruction limit reached! % 231.30/33.38 % (3992278)------------------------------ % 231.30/33.38 % (3992278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.30/33.38 % (3992282)Instruction limit reached! % 231.30/33.38 % (3992282)------------------------------ % 231.30/33.38 % (3992282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.30/33.38 % (3992278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.30/33.38 % (3992278)CaDiCaL version: 2.1.3 % 231.30/33.38 % (3992278)Termination reason: Instruction limit % 231.30/33.38 % (3992278)Termination phase: Saturation % 231.30/33.38 % (3992278)Time elapsed: 0.534 s % 231.30/33.38 % (3992278)Peak memory usage: 97 MB % 231.30/33.38 % (3992278)Instructions burned: 1228 (million) % 231.30/33.38 % (3992282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.30/33.38 % (3992282)CaDiCaL version: 2.1.3 % 231.30/33.38 % (3992282)Termination reason: Instruction limit % 231.30/33.38 % (3992282)Termination phase: Saturation % 231.30/33.38 % (3992282)Time elapsed: 0.147 s % 231.30/33.38 % (3992282)Peak memory usage: 91 MB % 231.30/33.38 % (3992282)Instructions burned: 271 (million) % 231.30/33.38 % (3992283)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=3293048823:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2706 on theBenchmark for (2706ds/268Mi) % 231.30/33.38 % Exception at run slice level % 231.30/33.38 User error: Immediate (shared) subterms of term/literal sF117(X1,X0,X3,X2) = aa(X1,X0,combk(X0,X1,X3),X2) have different types/not well-typed! % 231.30/33.38 % (3992287)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=20395574:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2704 on theBenchmark for (2704ds/862Mi) % 231.30/33.38 % (3992286)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=245550130:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2704 on theBenchmark for (2704ds/282Mi) % 231.30/33.38 % (3992286)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 231.30/33.38 % (3992286)Refutation not found, incomplete strategy % 231.30/33.38 % (3992286)------------------------------ % 231.30/33.38 % (3992286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.30/33.38 % (3992286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.30/33.38 % (3992286)CaDiCaL version: 2.1.3 % 231.30/33.38 % (3992286)Termination reason: Refutation not found, incomplete strategy % 231.30/33.38 % (3992286)Time elapsed: 0.008 s % 231.30/33.38 % (3992286)Peak memory usage: 89 MB % 231.30/33.38 % (3992286)Instructions burned: 12 (million) % 231.30/33.38 % (3992288)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=347633308:i=12120:aac=none:ins=25:rtra=on_2704 on theBenchmark for (2704ds/12120Mi) % 231.30/33.38 % (3992286)------------------------------ % 231.30/33.38 % (3992286)------------------------------ % 231.30/33.38 % Exception at run slice level % 243.95/35.07 User error: GNN currently only supports monomorphic FOL. % 243.95/35.07 % (3992293)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=293917729:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2700 on theBenchmark for (2700ds/300Mi) % 243.95/35.07 % (3992293)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 243.95/35.07 % (3992287)Instruction limit reached! % 243.95/35.07 % (3992287)------------------------------ % 243.95/35.07 % (3992287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.95/35.07 % (3992287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.95/35.07 % (3992287)CaDiCaL version: 2.1.3 % 243.95/35.07 % (3992287)Termination reason: Instruction limit % 243.95/35.07 % (3992287)Termination phase: Saturation % 243.95/35.07 % (3992287)Time elapsed: 0.475 s % 243.95/35.07 % (3992287)Peak memory usage: 94 MB % 243.95/35.07 % (3992287)Instructions burned: 863 (million) % 243.95/35.07 % (3992294)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=457459585:i=28310:bd=all:rtra=on_2699 on theBenchmark for (2699ds/28310Mi) % 243.95/35.07 % (3992293)Instruction limit reached! % 243.95/35.07 % (3992293)------------------------------ % 243.95/35.07 % (3992293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.95/35.07 % (3992293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.95/35.07 % (3992293)CaDiCaL version: 2.1.3 % 243.95/35.07 % (3992293)Termination reason: Instruction limit % 243.95/35.07 % (3992293)Termination phase: Saturation % 243.95/35.07 % (3992293)Time elapsed: 0.178 s % 243.95/35.07 % (3992293)Peak memory usage: 92 MB % 243.95/35.07 % (3992293)Instructions burned: 301 (million) % 243.95/35.07 % (3992296)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2489734681:i=1334:av=off:fsr=off:rtra=on_2698 on theBenchmark for (2698ds/1334Mi) % 243.95/35.07 % (3992298)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=3720231146:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2697 on theBenchmark for (2697ds/370Mi) % 243.95/35.07 % (3992210)Instruction limit reached! % 243.95/35.07 % (3992210)------------------------------ % 243.95/35.07 % (3992210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.95/35.07 % (3992210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.95/35.07 % (3992210)CaDiCaL version: 2.1.3 % 243.95/35.07 % (3992210)Termination reason: Instruction limit % 243.95/35.07 % (3992210)Termination phase: Saturation % 243.95/35.07 % (3992210)Time elapsed: 9.483 s % 243.95/35.07 % (3992210)Peak memory usage: 105 MB % 243.95/35.07 % (3992210)Instructions burned: 28959 (million) % 243.95/35.07 % (3992298)Instruction limit reached! % 243.95/35.07 % (3992298)------------------------------ % 243.95/35.07 % (3992298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.95/35.07 % (3992298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.95/35.07 % (3992298)CaDiCaL version: 2.1.3 % 243.95/35.07 % (3992298)Termination reason: Instruction limit % 243.95/35.07 % (3992298)Termination phase: Saturation % 243.95/35.07 % (3992298)Time elapsed: 0.252 s % 243.95/35.07 % (3992298)Peak memory usage: 93 MB % 243.95/35.07 % (3992298)Instructions burned: 371 (million) % 243.95/35.07 % Exception at run slice level % 243.95/35.07 User error: GNN currently only supports monomorphic FOL. % 243.95/35.07 % (3992301)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=2078736821:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2693 on theBenchmark for (2693ds/386Mi) % 243.95/35.07 % (3992302)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=425621923:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2693 on theBenchmark for (2693ds/9700Mi) % 243.95/35.07 % (3992303)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=3964905930:i=24222:sd=1:rtra=on:ss=included_2692 on theBenchmark for (2692ds/24222Mi) % 243.95/35.07 % (3992296)Instruction limit reached! % 243.95/35.07 % (3992296)------------------------------ % 243.95/35.07 % (3992296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.95/35.07 % (3992296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.02/36.41 % (3992296)CaDiCaL version: 2.1.3 % 253.02/36.41 % (3992296)Termination reason: Instruction limit % 253.02/36.41 % (3992296)Termination phase: Saturation % 253.02/36.41 % (3992296)Time elapsed: 0.592 s % 253.02/36.41 % (3992296)Peak memory usage: 96 MB % 253.02/36.41 % (3992296)Instructions burned: 1336 (million) % 253.02/36.41 % (3992301)Instruction limit reached! % 253.02/36.41 % (3992301)------------------------------ % 253.02/36.41 % (3992301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.02/36.41 % (3992301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.02/36.41 % (3992301)CaDiCaL version: 2.1.3 % 253.02/36.41 % (3992301)Termination reason: Instruction limit % 253.02/36.41 % (3992301)Termination phase: Saturation % 253.02/36.41 % (3992301)Time elapsed: 0.227 s % 253.02/36.41 % (3992301)Peak memory usage: 92 MB % 253.02/36.41 % (3992301)Instructions burned: 388 (million) % 253.02/36.41 % (3992307)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=681725451:i=638:kws=precedence:fsr=off:rtra=on_2690 on theBenchmark for (2690ds/638Mi) % 253.02/36.41 % (3992308)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3193775354:i=4128:ep=RST:rtra=on_2689 on theBenchmark for (2689ds/4128Mi) % 253.02/36.41 % Exception at run slice level % 253.02/36.41 User error: GNN currently only supports monomorphic FOL. % 253.02/36.41 % (3992307)Instruction limit reached! % 253.02/36.41 % (3992307)------------------------------ % 253.02/36.41 % (3992307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.02/36.41 % (3992307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.02/36.41 % (3992307)CaDiCaL version: 2.1.3 % 253.02/36.41 % (3992307)Termination reason: Instruction limit % 253.02/36.41 % (3992307)Termination phase: Saturation % 253.02/36.41 % (3992307)Time elapsed: 0.285 s % 253.02/36.41 % (3992307)Peak memory usage: 90 MB % 253.02/36.41 % (3992307)Instructions burned: 638 (million) % 253.02/36.41 % (3992311)dis-1011_128_sil=32000:si=on:random_seed=1530844991:i=7412:ep=RST:av=off:rtra=on_2687 on theBenchmark for (2687ds/7412Mi) % 253.02/36.41 % (3992312)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2969532828:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2686 on theBenchmark for (2686ds/1514Mi) % 253.02/36.41 % (3992205)Instruction limit reached! % 253.02/36.41 % (3992205)------------------------------ % 253.02/36.41 % (3992205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.02/36.41 % (3992205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.02/36.41 % (3992205)CaDiCaL version: 2.1.3 % 253.02/36.41 % (3992205)Termination reason: Instruction limit % 253.02/36.41 % (3992205)Termination phase: Saturation % 253.02/36.41 % (3992205)Time elapsed: 12.159 s % 253.02/36.41 % (3992205)Peak memory usage: 223 MB % 253.02/36.41 % (3992205)Instructions burned: 23714 (million) % 253.02/36.41 % (3992312)Instruction limit reached! % 253.02/36.41 % (3992312)------------------------------ % 253.02/36.41 % (3992312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.02/36.41 % (3992312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.02/36.41 % (3992312)CaDiCaL version: 2.1.3 % 253.02/36.41 % (3992312)Termination reason: Instruction limit % 253.02/36.41 % (3992312)Termination phase: Saturation % 253.02/36.41 % (3992312)Time elapsed: 0.817 s % 253.02/36.41 % (3992312)Peak memory usage: 105 MB % 253.02/36.41 % (3992312)Instructions burned: 1515 (million) % 253.02/36.41 % (3992315)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=3437743363:i=27826:rtra=on:ss=axioms:sgt=8_2676 on theBenchmark for (2676ds/27826Mi) % 253.02/36.41 % (3992316)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=2116972249:i=19850:aac=none:rtra=on_2676 on theBenchmark for (2676ds/19850Mi) % 253.02/36.41 % (3992308)Instruction limit reached! % 253.02/36.41 % (3992308)------------------------------ % 253.02/36.41 % (3992308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.02/36.41 % (3992308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.02/36.41 % (3992308)CaDiCaL version: 2.1.3 % 253.02/36.41 % (3992308)Termination reason: Instruction limit % 253.02/36.41 % (3992308)Termination phase: Saturation % 253.02/36.41 % (3992308)Time elapsed: 1.363 s % 253.02/36.41 % (3992308)Peak memory usage: 89 MB % 253.02/36.41 % (3992308)Instructions burned: 4130 (million) % 253.02/36.41 % (3992319)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2027671073:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2674 on theBenchmark for (2674ds/4958Mi) % 268.53/38.53 % Exception at run slice level % 268.53/38.53 User error: GNN currently only supports monomorphic FOL. % 268.53/38.53 % Exception at run slice level % 268.53/38.53 User error: GNN currently only supports monomorphic FOL. % 268.53/38.53 % (3992321)ott+1002_64_sil=16000:si=on:sp=const_min:nwc=0.5:random_seed=1464599373:i=880:nm=2:av=off:rtra=on:gtg=exists_all:fdi=8:gsp=on_2671 on theBenchmark for (2671ds/880Mi) % 268.53/38.53 % (3992321)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 268.53/38.53 % (3992322)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:si=on:erd=off:lsd=100:bsr=unit_only:random_seed=126753121:st=1.5:i=22290:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2671 on theBenchmark for (2671ds/22290Mi) % 268.53/38.53 % Exception at run slice level % 268.53/38.53 User error: GNN currently only supports monomorphic FOL. % 268.53/38.53 % (3992321)Instruction limit reached! % 268.53/38.53 % (3992321)------------------------------ % 268.53/38.53 % (3992321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.53/38.53 % (3992321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.53/38.53 % (3992321)CaDiCaL version: 2.1.3 % 268.53/38.53 % (3992321)Termination reason: Instruction limit % 268.53/38.53 % (3992321)Termination phase: Saturation % 268.53/38.53 % (3992321)Time elapsed: 0.510 s % 268.53/38.53 % (3992321)Peak memory usage: 90 MB % 268.53/38.53 % (3992321)Instructions burned: 881 (million) % 268.53/38.53 % (3992325)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=3869280548:cts=off:i=6068:av=off:rtra=on:er=known:fsd=on_2666 on theBenchmark for (2666ds/6068Mi) % 268.53/38.53 % (3992326)lrs-1011_64:1_sil=8000:si=on:erd=off:urr=on:nwc=0.7:br=off:random_seed=2381467458:st=2:s2a=on:i=1048:s2at=2:rtra=on:ss=axioms_2665 on theBenchmark for (2665ds/1048Mi) % 268.53/38.53 % Exception at run slice level % 268.53/38.53 User error: GNN currently only supports monomorphic FOL. % 268.53/38.53 % (3992302)Instruction limit reached! % 268.53/38.53 % (3992302)------------------------------ % 268.53/38.53 % (3992302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.53/38.53 % (3992302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.53/38.53 % (3992302)CaDiCaL version: 2.1.3 % 268.53/38.53 % (3992302)Termination reason: Instruction limit % 268.53/38.53 % (3992302)Termination phase: Saturation % 268.53/38.53 % (3992302)Time elapsed: 3.193 s % 268.53/38.53 % (3992302)Peak memory usage: 89 MB % 268.53/38.53 % (3992302)Instructions burned: 9700 (million) % 268.53/38.53 % (3992329)lrs+1011_16:1_sil=8000:si=on:acc=on:urr=on:fd=preordered:flr=on:random_seed=2170974637:avsq=on:i=2032:avsqr=676809,524288:sd=1:rtra=on:ss=axioms_2660 on theBenchmark for (2660ds/2032Mi) % 268.53/38.53 % (3992326)Instruction limit reached! % 268.53/38.53 % (3992326)------------------------------ % 268.53/38.53 % (3992326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.53/38.53 % (3992326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.53/38.53 % (3992326)CaDiCaL version: 2.1.3 % 268.53/38.53 % (3992326)Termination reason: Instruction limit % 268.53/38.53 % (3992326)Termination phase: Saturation % 268.53/38.53 % (3992326)Time elapsed: 0.510 s % 268.53/38.53 % (3992326)Peak memory usage: 92 MB % 268.53/38.53 % (3992326)Instructions burned: 1049 (million) % 268.53/38.53 % (3992330)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:si=on:s2agt=16:random_seed=1303087122:i=28246:bd=preordered:ins=4:rtra=on_2659 on theBenchmark for (2659ds/28246Mi) % 268.53/38.53 % (3992332)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:si=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1390278165:i=11562:kws=precedence:bd=all:rtra=on:rawr=on_2658 on theBenchmark for (2658ds/11562Mi) % 268.53/38.53 % (3992319)Instruction limit reached! % 268.53/38.53 % (3992319)------------------------------ % 268.53/38.53 % (3992319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.53/38.53 % (3992319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.53/38.53 % (3992319)CaDiCaL version: 2.1.3 % 268.53/38.53 % (3992319)Termination reason: Instruction limit % 268.53/38.53 % (3992319)Termination phase: Saturation % 268.53/38.53 % (3992319)Time elapsed: 1.686 s % 268.53/38.53 % (3992319)Peak memory usage: 89 MB % 268.53/38.53 % (3992319)Instructions burned: 4959 (million) % 276.38/39.73 % (3992335)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:si=on:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=3201852377:i=4896:gtgl=5:bd=preordered:rtra=on:gtg=all_2655 on theBenchmark for (2655ds/4896Mi) % 276.38/39.73 % Exception at run slice level % 276.38/39.73 User error: GNN currently only supports monomorphic FOL. % 276.38/39.73 % (3992337)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:si=on:lcm=reverse:random_seed=3559433039:i=6446:kws=precedence:fgj=on:av=off:rtra=on_2654 on theBenchmark for (2654ds/6446Mi) % 276.38/39.73 % (3992222)Instruction limit reached! % 276.38/39.73 % (3992222)------------------------------ % 276.38/39.73 % (3992222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.38/39.73 % (3992222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.38/39.73 % (3992222)CaDiCaL version: 2.1.3 % 276.38/39.73 % (3992222)Termination reason: Instruction limit % 276.38/39.73 % (3992222)Termination phase: Saturation % 276.38/39.73 % (3992222)Time elapsed: 11.052 s % 276.38/39.73 % (3992222)Peak memory usage: 238 MB % 276.38/39.73 % (3992222)Instructions burned: 36829 (million) % 276.38/39.73 % (3992339)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:si=on:sp=occurrence:sos=on:random_seed=3953286594:st=5.6:i=4066:sd=3:rtra=on:ss=axioms_2651 on theBenchmark for (2651ds/4066Mi) % 276.38/39.73 % Exception at run slice level % 276.38/39.73 User error: GNN currently only supports monomorphic FOL. % 276.38/39.73 % (3992329)Instruction limit reached! % 276.38/39.73 % (3992329)------------------------------ % 276.38/39.73 % (3992329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.38/39.73 % (3992329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.38/39.73 % (3992329)CaDiCaL version: 2.1.3 % 276.38/39.73 % (3992329)Termination reason: Instruction limit % 276.38/39.73 % (3992329)Termination phase: Saturation % 276.38/39.73 % (3992329)Time elapsed: 0.865 s % 276.38/39.73 % (3992329)Peak memory usage: 118 MB % 276.38/39.73 % (3992329)Instructions burned: 2032 (million) % 276.38/39.73 % (3992341)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:si=on:random_seed=590042878:i=4110:nm=16:rtra=on:gtg=position:ss=axioms:fsd=on_2650 on theBenchmark for (2650ds/4110Mi) % 276.38/39.73 % Exception at run slice level % 276.38/39.73 User error: GNN currently only supports monomorphic FOL. % 276.38/39.73 % (3992342)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:si=on:sp=const_frequency:spb=goal:acc=on:random_seed=3083502951:i=43222:sd=3:rtra=on:ss=axioms_2650 on theBenchmark for (2650ds/43222Mi) % 276.38/39.73 % Exception at run slice level % 276.38/39.73 User error: GNN currently only supports monomorphic FOL. % 276.38/39.73 % (3992346)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:si=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=1996062008:st=5:i=1594:s2at=3:sd=4:bs=unit_only:av=off:rtra=on:sup=off:ss=included_2648 on theBenchmark for (2648ds/1594Mi) % 276.38/39.73 % (3992344)lrs+10_1_sil=8000:si=on:sp=occurrence:sos=all:lma=off:random_seed=3730186829:i=9670:sd=13:rtra=on:ss=axioms:sgt=23_2648 on theBenchmark for (2648ds/9670Mi) % 276.38/39.73 % Exception at run slice level % 276.38/39.73 User error: GNN currently only supports monomorphic FOL. % 276.38/39.73 % Exception at run slice level % 276.38/39.73 User error: GNN currently only supports monomorphic FOL. % 276.38/39.73 % (3992349)lrs-1011_5_sil=8000:si=on:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2183901012:i=4652:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:rtra=on:fsd=on_2645 on theBenchmark for (2645ds/4652Mi) % 276.38/39.73 % (3992346)Instruction limit reached! % 276.38/39.73 % (3992346)------------------------------ % 276.38/39.73 % (3992346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.38/39.73 % (3992346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.38/39.73 % (3992346)CaDiCaL version: 2.1.3 % 276.38/39.73 % (3992346)Termination reason: Instruction limit % 276.38/39.73 % (3992346)Termination phase: Saturation % 276.38/39.73 % (3992346)Time elapsed: 0.376 s % 276.38/39.73 % (3992346)Peak memory usage: 90 MB % 276.38/39.73 % (3992346)Instructions burned: 1596 (million) % 276.38/39.73 % (3992350)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:si=on:sos=all:urr=on:br=off:random_seed=1893479592:i=12076:nm=6:rtra=on_2645 on theBenchmark for (2645ds/12076Mi) % 276.38/39.73 % (3992352)lrs+10_1_sil=32000:si=on:sp=occurrence:random_seed=1951278575:st=2:i=66668:sd=3:rtra=on:ss=included:sgt=32_2643 on theBenchmark for (2643ds/66668Mi) % 289.09/41.62 % (3992311)Instruction limit reached! % 289.09/41.62 % (3992311)------------------------------ % 289.09/41.62 % (3992311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.09/41.62 % (3992311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.09/41.62 % (3992311)CaDiCaL version: 2.1.3 % 289.09/41.62 % (3992311)Termination reason: Instruction limit % 289.09/41.62 % (3992311)Termination phase: Saturation % 289.09/41.62 % (3992311)Time elapsed: 4.513 s % 289.09/41.62 % (3992311)Peak memory usage: 119 MB % 289.09/41.62 % (3992311)Instructions burned: 7413 (million) % 289.09/41.62 % Exception at run slice level % 289.09/41.62 User error: GNN currently only supports monomorphic FOL. % 289.09/41.62 % (3992355)lrs+10_4_sil=8000:plsq=on:si=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1455282654:st=3.7:s2a=on:i=2016:s2at=1.2:sd=3:bd=all:av=off:rtra=on:fdi=8:sup=off:ss=axioms_2640 on theBenchmark for (2640ds/2016Mi) % 289.09/41.62 % (3992356)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:si=on:sp=const_frequency:spb=intro:gs=on:random_seed=791165793:i=16654:s2at=5:bd=preordered:rtra=on_2640 on theBenchmark for (2640ds/16654Mi) % 289.09/41.62 % Exception at run slice level % 289.09/41.62 User error: GNN currently only supports monomorphic FOL. % 289.09/41.62 % (3992359)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:si=on:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=3587776205:s2a=on:i=2166:s2at=1.87328:slsql=off:ep=RSTC:rtra=on:fdi=16_2634 on theBenchmark for (2634ds/2166Mi) % 289.09/41.62 % (3992355)Instruction limit reached! % 289.09/41.62 % (3992355)------------------------------ % 289.09/41.62 % (3992355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.09/41.62 % (3992355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.09/41.62 % (3992355)CaDiCaL version: 2.1.3 % 289.09/41.62 % (3992355)Termination reason: Instruction limit % 289.09/41.62 % (3992355)Termination phase: Saturation % 289.09/41.62 % (3992355)Time elapsed: 0.915 s % 289.09/41.62 % (3992355)Peak memory usage: 99 MB % 289.09/41.62 % (3992355)Instructions burned: 2016 (million) % 289.09/41.62 % (3992361)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:si=on:spb=goal:fd=preordered:random_seed=2592602631:i=2168:sd=1:bd=preordered:av=off:fsr=off:rtra=on:ss=axioms:sgt=14_2629 on theBenchmark for (2629ds/2168Mi) % 289.09/41.62 % (3992349)Instruction limit reached! % 289.09/41.62 % (3992349)------------------------------ % 289.09/41.62 % (3992349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.09/41.62 % (3992349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.09/41.62 % (3992349)CaDiCaL version: 2.1.3 % 289.09/41.62 % (3992349)Termination reason: Instruction limit % 289.09/41.62 % (3992349)Termination phase: Saturation % 289.09/41.62 % (3992349)Time elapsed: 1.603 s % 289.09/41.62 % (3992349)Peak memory usage: 89 MB % 289.09/41.62 % (3992349)Instructions burned: 4653 (million) % 289.09/41.62 % (3992363)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:si=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1092558839:i=13990:s2at=5:rtra=on:gtg=all_2627 on theBenchmark for (2627ds/13990Mi) % 289.09/41.62 % Exception at run slice level % 289.09/41.62 User error: Immediate (shared) subterms of term/literal aa(fun(X1,fun(state,bool)),fun(com,fun(fun(X1,fun(state,bool)),X0)),X4,X5) = sF46(X1,X0,X4,X5) have different types/not well-typed! % 289.09/41.62 % (3992365)lrs+10_1_sil=32000:si=on:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=186623370:st=2:i=12450:sd=15:rtra=on:ss=axioms_2626 on theBenchmark for (2626ds/12450Mi) % 289.09/41.62 % (3992365)Refutation not found, incomplete strategy % 289.09/41.62 % (3992365)------------------------------ % 289.09/41.62 % (3992365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.09/41.62 % (3992365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.09/41.62 % (3992365)CaDiCaL version: 2.1.3 % 289.09/41.62 % (3992365)Termination reason: Refutation not found, incomplete strategy % 289.09/41.62 % (3992365)Time elapsed: 0.020 s % 289.09/41.62 % (3992365)Peak memory usage: 89 MB % 289.09/41.62 % (3992365)Instructions burned: 34 (million) % 289.09/41.62 % (3992365)------------------------------ % 289.09/41.62 % (3992365)------------------------------ % 289.09/41.62 % (3992359)Instruction limit reached! % 289.09/41.62 % (3992359)Terminated %------------------------------------------------------------------------------