%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW531_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 : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:30:45 PM UTC 2026 % Result : Timeout 295.17s 42.38s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW531_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.17 % Computer : n003.cluster.edu % 0.08/0.17 % Model : x86_64 x86_64 % 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.17 % Memory : 8046.5625MB % 0.08/0.17 % OS : Linux 6.8.0-71-generic % 0.08/0.17 % CPULimit : 300 % 0.08/0.17 % WCLimit : 300 % 0.08/0.17 % DateTime : Mon Sep 28 14:19:12 UTC 2026 % 0.08/0.17 % CPUTime : % 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.21 Running first-order theorem proving % 0.08/0.21 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.02/1.60 % (1614141)Detected formulas, will run a generic FOF schedule. % 6.02/1.60 % (1614157)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=1131668557:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 6.02/1.60 % (1614157)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 6.02/1.60 % (1614155)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=2953730709:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 6.02/1.60 % (1614156)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=3154712675:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 6.02/1.60 % (1614161)dis-21_1_sil=8000:lcm=predicate:random_seed=2549620692: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.02/1.60 % (1614159)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2708271381:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 6.02/1.60 % (1614158)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1817125486:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 6.02/1.60 % (1614158)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 6.02/1.60 % (1614158)Refutation not found, incomplete strategy % 6.02/1.60 % (1614158)------------------------------ % 6.02/1.60 % (1614158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.02/1.60 % (1614158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.02/1.60 % (1614158)CaDiCaL version: 2.1.3 % 6.02/1.60 % (1614158)Termination reason: Refutation not found, incomplete strategy % 6.02/1.60 % (1614158)Time elapsed: 0.002 s % 6.02/1.60 % (1614158)Peak memory usage: 88 MB % 6.02/1.60 % (1614158)Instructions burned: 1 (million) % 6.02/1.60 % (1614160)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1987931271:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 6.02/1.60 % (1614161)Instruction limit reached! % 6.02/1.60 % (1614161)------------------------------ % 6.02/1.60 % (1614161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.02/1.60 % (1614161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.02/1.60 % (1614161)CaDiCaL version: 2.1.3 % 6.02/1.60 % (1614161)Termination reason: Instruction limit % 6.02/1.60 % (1614161)Termination phase: Saturation % 6.02/1.60 % (1614161)Time elapsed: 0.068 s % 6.02/1.60 % (1614161)Peak memory usage: 89 MB % 6.02/1.60 % (1614161)Instructions burned: 129 (million) % 6.02/1.60 % (1614159)Instruction limit reached! % 6.02/1.60 % (1614159)------------------------------ % 6.02/1.60 % (1614159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.02/1.60 % (1614159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.02/1.60 % (1614159)CaDiCaL version: 2.1.3 % 6.02/1.60 % (1614159)Termination reason: Instruction limit % 6.02/1.60 % (1614159)Termination phase: Saturation % 6.02/1.60 % (1614159)Time elapsed: 0.070 s % 6.02/1.60 % (1614159)Peak memory usage: 88 MB % 6.02/1.60 % (1614159)Instructions burned: 120 (million) % 6.02/1.60 % (1614160)Instruction limit reached! % 6.02/1.60 % (1614160)------------------------------ % 6.02/1.60 % (1614160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.02/1.60 % (1614160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.02/1.60 % (1614160)CaDiCaL version: 2.1.3 % 6.02/1.60 % (1614160)Termination reason: Instruction limit % 6.02/1.60 % (1614160)Termination phase: Saturation % 6.02/1.60 % (1614160)Time elapsed: 0.102 s % 6.02/1.60 % (1614160)Peak memory usage: 89 MB % 6.02/1.60 % (1614160)Instructions burned: 139 (million) % 6.02/1.60 % Exception at run slice level % 6.02/1.60 User error: GNN currently only supports monomorphic FOL. % 6.02/1.60 % (1614180)lrs+10_1_sil=32000:urr=on:br=off:random_seed=804338468:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 6.02/1.60 % (1614178)lrs+10_1_sil=8000:sp=occurrence:random_seed=3492617914:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 6.02/1.60 % (1614180)Refutation not found, incomplete strategy % 6.02/1.60 % (1614180)------------------------------ % 7.65/2.01 % (1614180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.65/2.01 % (1614180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.65/2.01 % (1614180)CaDiCaL version: 2.1.3 % 7.65/2.01 % (1614180)Termination reason: Refutation not found, incomplete strategy % 7.65/2.01 % (1614180)Time elapsed: 0.003 s % 7.65/2.01 % (1614180)Peak memory usage: 88 MB % 7.65/2.01 % (1614180)Instructions burned: 2 (million) % 7.65/2.01 % (1614158)------------------------------ % 7.65/2.01 % (1614158)------------------------------ % 7.65/2.01 % (1614216)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=8062694:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 7.65/2.01 % (1614210)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2439779539:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 7.65/2.01 % (1614210)Refutation not found, incomplete strategy % 7.65/2.01 % (1614210)------------------------------ % 7.65/2.01 % (1614210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.65/2.01 % (1614210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.65/2.01 % (1614210)CaDiCaL version: 2.1.3 % 7.65/2.01 % (1614210)Termination reason: Refutation not found, incomplete strategy % 7.65/2.01 % (1614210)Time elapsed: 0.002 s % 7.65/2.01 % (1614210)Peak memory usage: 88 MB % 7.65/2.01 % (1614210)Instructions burned: 1 (million) % 7.65/2.01 % (1614216)Instruction limit reached! % 7.65/2.01 % (1614216)------------------------------ % 7.65/2.01 % (1614216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.65/2.01 % (1614216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.65/2.01 % (1614216)CaDiCaL version: 2.1.3 % 7.65/2.01 % (1614216)Termination reason: Instruction limit % 7.65/2.01 % (1614216)Termination phase: Saturation % 7.65/2.01 % (1614216)Time elapsed: 0.072 s % 7.65/2.01 % (1614216)Peak memory usage: 90 MB % 7.65/2.01 % (1614216)Instructions burned: 252 (million) % 7.65/2.01 % Exception at run slice level % 7.65/2.01 User error: GNN currently only supports monomorphic FOL. % 7.65/2.01 % Exception at run slice level % 7.65/2.01 User error: GNN currently only supports monomorphic FOL. % 7.65/2.01 % (1614178)Instruction limit reached! % 7.65/2.01 % (1614178)------------------------------ % 7.65/2.01 % (1614178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.65/2.01 % (1614178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.65/2.01 % (1614178)CaDiCaL version: 2.1.3 % 7.65/2.01 % (1614178)Termination reason: Instruction limit % 7.65/2.01 % (1614178)Termination phase: Saturation % 7.65/2.01 % (1614178)Time elapsed: 0.161 s % 7.65/2.01 % (1614178)Peak memory usage: 89 MB % 7.65/2.01 % (1614178)Instructions burned: 286 (million) % 7.65/2.01 % (1614256)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=872752796:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi) % 7.65/2.01 % (1614256)Refutation not found, incomplete strategy % 7.65/2.01 % (1614256)------------------------------ % 7.65/2.01 % (1614256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.65/2.01 % (1614256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.65/2.01 % (1614256)CaDiCaL version: 2.1.3 % 7.65/2.01 % (1614256)Termination reason: Refutation not found, incomplete strategy % 7.65/2.01 % (1614256)Time elapsed: 0.005 s % 7.65/2.01 % (1614256)Peak memory usage: 88 MB % 7.65/2.01 % (1614256)Instructions burned: 6 (million) % 7.65/2.01 % (1614280)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1419790209:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 7.65/2.01 % (1614180)------------------------------ % 7.65/2.01 % (1614180)------------------------------ % 7.65/2.01 % (1614284)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4153017930:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi) % 7.65/2.01 % (1614284)Refutation not found, incomplete strategy % 7.65/2.01 % (1614284)------------------------------ % 7.65/2.01 % (1614284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.65/2.01 % (1614284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.65/2.01 % (1614284)CaDiCaL version: 2.1.3 % 7.65/2.01 % (1614284)Termination reason: Refutation not found, incomplete strategy % 7.65/2.01 % (1614284)Time elapsed: 0.007 s % 10.52/2.30 % (1614284)Peak memory usage: 88 MB % 10.52/2.30 % (1614284)Instructions burned: 9 (million) % 10.52/2.30 % (1614285)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2280272487:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi) % 10.52/2.30 % (1614287)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2931547583:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 10.52/2.30 % (1614287)Refutation not found, incomplete strategy % 10.52/2.30 % (1614287)------------------------------ % 10.52/2.30 % (1614287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.52/2.30 % (1614287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.52/2.30 % (1614287)CaDiCaL version: 2.1.3 % 10.52/2.30 % (1614287)Termination reason: Refutation not found, incomplete strategy % 10.52/2.30 % (1614287)Time elapsed: 0.006 s % 10.52/2.30 % (1614287)Peak memory usage: 88 MB % 10.52/2.30 % (1614287)Instructions burned: 8 (million) % 10.52/2.30 % (1614210)------------------------------ % 10.52/2.30 % (1614210)------------------------------ % 10.52/2.30 % (1614285)Instruction limit reached! % 10.52/2.30 % (1614285)------------------------------ % 10.52/2.30 % (1614285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.52/2.30 % (1614285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.52/2.30 % (1614285)CaDiCaL version: 2.1.3 % 10.52/2.30 % (1614285)Termination reason: Instruction limit % 10.52/2.30 % (1614285)Termination phase: Saturation % 10.52/2.30 % (1614285)Time elapsed: 0.063 s % 10.52/2.30 % (1614285)Peak memory usage: 88 MB % 10.52/2.30 % (1614285)Instructions burned: 128 (million) % 10.52/2.30 % (1614297)lrs+10_1_sil=8000:sp=occurrence:random_seed=1551670834:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi) % 10.52/2.30 % Exception at run slice level % 10.52/2.30 User error: GNN currently only supports monomorphic FOL. % 10.52/2.30 % (1614256)------------------------------ % 10.52/2.30 % (1614256)------------------------------ % 10.52/2.30 % (1614332)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4018301496:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi) % 10.52/2.30 % (1614332)Refutation not found, incomplete strategy % 10.52/2.30 % (1614332)------------------------------ % 10.52/2.30 % (1614332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.52/2.30 % (1614332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.52/2.30 % (1614332)CaDiCaL version: 2.1.3 % 10.52/2.30 % (1614332)Termination reason: Refutation not found, incomplete strategy % 10.52/2.30 % (1614332)Time elapsed: 0.008 s % 10.52/2.30 % (1614332)Peak memory usage: 88 MB % 10.52/2.30 % (1614332)Instructions burned: 10 (million) % 10.52/2.30 % (1614341)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4114182005:i=5202:ss=axioms:sgt=16_2993 on theBenchmark for (2993ds/5202Mi) % 10.52/2.30 % (1614343)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3734488077:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2992 on theBenchmark for (2992ds/134Mi) % 10.52/2.30 % (1614284)------------------------------ % 10.52/2.30 % (1614284)------------------------------ % 10.52/2.30 % (1614343)Instruction limit reached! % 10.52/2.30 % (1614343)------------------------------ % 10.52/2.30 % (1614343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.52/2.30 % (1614343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.52/2.30 % (1614343)CaDiCaL version: 2.1.3 % 10.52/2.30 % (1614343)Termination reason: Instruction limit % 10.52/2.30 % (1614343)Termination phase: Saturation % 10.52/2.30 % (1614343)Time elapsed: 0.046 s % 10.52/2.30 % (1614343)Peak memory usage: 90 MB % 10.52/2.30 % (1614343)Instructions burned: 136 (million) % 10.52/2.30 % (1614287)------------------------------ % 10.52/2.30 % (1614287)------------------------------ % 10.52/2.30 % (1614344)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1906736227:st=8:i=592:sd=3:ep=RST:ss=axioms_2992 on theBenchmark for (2992ds/592Mi) % 10.52/2.30 % (1614344)Refutation not found, incomplete strategy % 10.52/2.30 % (1614344)------------------------------ % 10.52/2.30 % (1614344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.52/2.30 % (1614344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.52/2.30 % (1614344)CaDiCaL version: 2.1.3 % 10.52/2.30 % (1614344)Termination reason: Refutation not found, incomplete strategy % 13.85/2.94 % (1614344)Time elapsed: 0.007 s % 13.85/2.94 % (1614344)Peak memory usage: 88 MB % 13.85/2.94 % (1614344)Instructions burned: 10 (million) % 13.85/2.94 % (1614348)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=228749893:st=3:i=13193:sd=3:ss=axioms_2991 on theBenchmark for (2991ds/13193Mi) % 13.85/2.94 % (1614350)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4103420092:i=134:gtgl=5:slsql=off:gtg=exists_sym_2991 on theBenchmark for (2991ds/134Mi) % 13.85/2.94 % (1614349)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=2551765293:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/125Mi) % 13.85/2.94 % (1614349)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.85/2.94 % Exception at run slice level % 13.85/2.94 User error: Immediate (shared) subterms of term/literal huffma107959123e_case(X1,X0,X5,X4,huffma2021818691e_Leaf(X1,X3,X2)) = sF29(X1,X0,X5,X4,X3,X2) have different types/not well-typed! % 13.85/2.94 % (1614332)------------------------------ % 13.85/2.94 % (1614332)------------------------------ % 13.85/2.94 % (1614349)Instruction limit reached! % 13.85/2.94 % (1614349)------------------------------ % 13.85/2.94 % (1614349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.85/2.94 % (1614349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.85/2.94 % (1614349)CaDiCaL version: 2.1.3 % 13.85/2.94 % (1614349)Termination reason: Instruction limit % 13.85/2.94 % (1614349)Termination phase: Saturation % 13.85/2.94 % (1614349)Time elapsed: 0.083 s % 13.85/2.94 % (1614349)Peak memory usage: 89 MB % 13.85/2.94 % (1614349)Instructions burned: 125 (million) % 13.85/2.94 % (1614355)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3234047503:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/141Mi) % 13.85/2.94 % (1614355)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.85/2.94 % (1614355)Refutation not found, incomplete strategy % 13.85/2.94 % (1614355)------------------------------ % 13.85/2.94 % (1614355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.85/2.94 % (1614355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.85/2.94 % (1614355)CaDiCaL version: 2.1.3 % 13.85/2.94 % (1614355)Termination reason: Refutation not found, incomplete strategy % 13.85/2.94 % (1614355)Time elapsed: 0.001 s % 13.85/2.94 % (1614355)Peak memory usage: 88 MB % 13.85/2.94 % (1614355)Instructions burned: 1 (million) % 13.85/2.94 % (1614344)------------------------------ % 13.85/2.94 % (1614344)------------------------------ % 13.85/2.94 % (1614356)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=780454431:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/431Mi) % 13.85/2.94 % Exception at run slice level % 13.85/2.94 User error: GNN currently only supports monomorphic FOL. % 13.85/2.94 % (1614357)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=390148565:i=6060:aac=none:ins=25_2989 on theBenchmark for (2989ds/6060Mi) % 13.85/2.94 % (1614297)Instruction limit reached! % 13.85/2.94 % (1614297)------------------------------ % 13.85/2.94 % (1614297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.85/2.94 % (1614297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.85/2.94 % (1614297)CaDiCaL version: 2.1.3 % 13.85/2.94 % (1614297)Termination reason: Instruction limit % 13.85/2.94 % (1614297)Termination phase: Saturation % 13.85/2.94 % (1614297)Time elapsed: 0.512 s % 13.85/2.94 % (1614297)Peak memory usage: 93 MB % 13.85/2.94 % (1614297)Instructions burned: 909 (million) % 13.85/2.94 % (1614355)------------------------------ % 13.85/2.94 % (1614355)------------------------------ % 13.85/2.94 % (1614359)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=179595936:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2988 on theBenchmark for (2988ds/150Mi) % 13.85/2.94 % (1614359)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.85/2.94 % (1614361)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3956045967:i=14155:bd=all_2988 on theBenchmark for (2988ds/14155Mi) % 18.97/3.54 % (1614364)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=2244705289:s2a=on:i=185:s2at=1.8:fdi=4_2987 on theBenchmark for (2987ds/185Mi) % 18.97/3.54 % (1614359)Instruction limit reached! % 18.97/3.54 % (1614359)------------------------------ % 18.97/3.54 % (1614359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.97/3.54 % (1614359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.97/3.54 % (1614359)CaDiCaL version: 2.1.3 % 18.97/3.54 % (1614359)Termination reason: Instruction limit % 18.97/3.54 % (1614359)Termination phase: Saturation % 18.97/3.54 % (1614359)Time elapsed: 0.068 s % 18.97/3.54 % (1614359)Peak memory usage: 90 MB % 18.97/3.54 % (1614359)Instructions burned: 153 (million) % 18.97/3.54 % (1614363)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1613143394:i=667:av=off:fsr=off_2987 on theBenchmark for (2987ds/667Mi) % 18.97/3.54 % (1614363)Refutation not found, incomplete strategy % 18.97/3.54 % (1614363)------------------------------ % 18.97/3.54 % (1614363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.97/3.54 % (1614363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.97/3.54 % (1614363)CaDiCaL version: 2.1.3 % 18.97/3.54 % (1614363)Termination reason: Refutation not found, incomplete strategy % 18.97/3.54 % (1614363)Time elapsed: 0.006 s % 18.97/3.54 % (1614363)Peak memory usage: 88 MB % 18.97/3.54 % (1614363)Instructions burned: 9 (million) % 18.97/3.54 % Exception at run slice level % 18.97/3.54 User error: GNN currently only supports monomorphic FOL. % 18.97/3.54 % (1614356)Instruction limit reached! % 18.97/3.54 % (1614356)------------------------------ % 18.97/3.54 % (1614356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.97/3.54 % (1614356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.97/3.54 % (1614356)CaDiCaL version: 2.1.3 % 18.97/3.54 % (1614356)Termination reason: Instruction limit % 18.97/3.54 % (1614356)Termination phase: Saturation % 18.97/3.54 % (1614356)Time elapsed: 0.216 s % 18.97/3.54 % (1614356)Peak memory usage: 92 MB % 18.97/3.54 % (1614356)Instructions burned: 432 (million) % 18.97/3.54 % (1614364)Instruction limit reached! % 18.97/3.54 % (1614364)------------------------------ % 18.97/3.54 % (1614364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.97/3.54 % (1614364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.97/3.54 % (1614364)CaDiCaL version: 2.1.3 % 18.97/3.54 % (1614364)Termination reason: Instruction limit % 18.97/3.54 % (1614364)Termination phase: Saturation % 18.97/3.54 % (1614364)Time elapsed: 0.066 s % 18.97/3.54 % (1614364)Peak memory usage: 90 MB % 18.97/3.54 % (1614364)Instructions burned: 187 (million) % 18.97/3.54 % (1614368)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3077465514:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2986 on theBenchmark for (2986ds/193Mi) % 18.97/3.54 % (1614370)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=519526288:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2986 on theBenchmark for (2986ds/4850Mi) % 18.97/3.54 % (1614372)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=164747078:i=319:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/319Mi) % 18.97/3.54 % (1614371)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4293014486:i=12111:sd=1:ss=included_2986 on theBenchmark for (2986ds/12111Mi) % 18.97/3.54 % Exception at run slice level % 18.97/3.54 User error: GNN currently only supports monomorphic FOL. % 18.97/3.54 % (1614372)Instruction limit reached! % 18.97/3.54 % (1614372)------------------------------ % 18.97/3.54 % (1614372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.97/3.54 % (1614372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.97/3.54 % (1614372)CaDiCaL version: 2.1.3 % 18.97/3.54 % (1614372)Termination reason: Instruction limit % 18.97/3.54 % (1614372)Termination phase: Saturation % 18.97/3.54 % (1614372)Time elapsed: 0.102 s % 18.97/3.54 % (1614372)Peak memory usage: 91 MB % 18.97/3.54 % (1614372)Instructions burned: 319 (million) % 18.97/3.54 % (1614368)Instruction limit reached! % 18.97/3.54 % (1614368)------------------------------ % 18.97/3.54 % (1614368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.99/4.83 % (1614368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.99/4.83 % (1614368)CaDiCaL version: 2.1.3 % 27.99/4.83 % (1614368)Termination reason: Instruction limit % 27.99/4.83 % (1614368)Termination phase: Saturation % 27.99/4.83 % (1614368)Time elapsed: 0.129 s % 27.99/4.83 % (1614368)Peak memory usage: 91 MB % 27.99/4.83 % (1614368)Instructions burned: 194 (million) % 27.99/4.83 % (1614363)------------------------------ % 27.99/4.83 % (1614363)------------------------------ % 27.99/4.83 % Exception at run slice level % 27.99/4.83 User error: GNN currently only supports monomorphic FOL. % 27.99/4.83 % (1614378)dis-1011_128_sil=32000:random_seed=337158702:i=3706:ep=RST:av=off_2983 on theBenchmark for (2983ds/3706Mi) % 27.99/4.83 % (1614377)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2087208176:i=2064:ep=RST_2984 on theBenchmark for (2984ds/2064Mi) % 27.99/4.83 % (1614377)Refutation not found, incomplete strategy % 27.99/4.83 % (1614377)------------------------------ % 27.99/4.83 % (1614377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.99/4.83 % (1614377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.99/4.83 % (1614377)CaDiCaL version: 2.1.3 % 27.99/4.83 % (1614377)Termination reason: Refutation not found, incomplete strategy % 27.99/4.83 % (1614377)Time elapsed: 0.006 s % 27.99/4.83 % (1614377)Peak memory usage: 88 MB % 27.99/4.83 % (1614377)Instructions burned: 10 (million) % 27.99/4.83 % (1614379)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2942824525:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2983 on theBenchmark for (2983ds/757Mi) % 27.99/4.83 % (1614379)Refutation not found, incomplete strategy % 27.99/4.83 % (1614379)------------------------------ % 27.99/4.83 % (1614379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.99/4.83 % (1614379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.99/4.83 % (1614379)CaDiCaL version: 2.1.3 % 27.99/4.83 % (1614379)Termination reason: Refutation not found, incomplete strategy % 27.99/4.83 % (1614379)Time elapsed: 0.006 s % 27.99/4.83 % (1614379)Peak memory usage: 89 MB % 27.99/4.83 % (1614379)Instructions burned: 8 (million) % 27.99/4.83 % (1614380)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1143032481:i=13913:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/13913Mi) % 27.99/4.83 % (1614381)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=115523638:i=9925:aac=none_2983 on theBenchmark for (2983ds/9925Mi) % 27.99/4.83 % Exception at run slice level % 27.99/4.83 User error: GNN currently only supports monomorphic FOL. % 27.99/4.83 % (1614377)------------------------------ % 27.99/4.83 % (1614377)------------------------------ % 27.99/4.83 % (1614379)------------------------------ % 27.99/4.83 % (1614379)------------------------------ % 27.99/4.83 % (1614387)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3528165024:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2981 on theBenchmark for (2981ds/2479Mi) % 27.99/4.83 % (1614387)Refutation not found, incomplete strategy % 27.99/4.83 % (1614387)------------------------------ % 27.99/4.83 % (1614387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.99/4.83 % (1614387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.99/4.83 % (1614387)CaDiCaL version: 2.1.3 % 27.99/4.83 % (1614387)Termination reason: Refutation not found, incomplete strategy % 27.99/4.83 % (1614387)Time elapsed: 0.003 s % 27.99/4.83 % (1614387)Peak memory usage: 88 MB % 27.99/4.83 % (1614387)Instructions burned: 2 (million) % 27.99/4.83 % (1614388)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=4079480521:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/440Mi) % 27.99/4.83 % Exception at run slice level % 27.99/4.83 User error: GNN currently only supports monomorphic FOL. % 27.99/4.83 % (1614388)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 27.99/4.83 % (1614389)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2023417486:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2980 on theBenchmark for (2980ds/11145Mi) % 27.99/4.83 % Exception at run slice level % 27.99/4.83 User error: GNN currently only supports monomorphic FOL. % 27.99/4.83 % (1614393)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=3869057289:cts=off:i=3034:av=off:er=known:fsd=on_2978 on theBenchmark for (2978ds/3034Mi) % 33.57/5.48 % (1614387)------------------------------ % 33.57/5.48 % (1614387)------------------------------ % 33.57/5.48 % (1614394)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=212490863:st=2:s2a=on:i=524:s2at=2:ss=axioms_2978 on theBenchmark for (2978ds/524Mi) % 33.57/5.48 % (1614388)Instruction limit reached! % 33.57/5.48 % (1614388)------------------------------ % 33.57/5.48 % (1614388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.57/5.48 % (1614388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.57/5.48 % (1614388)CaDiCaL version: 2.1.3 % 33.57/5.48 % (1614388)Termination reason: Instruction limit % 33.57/5.48 % (1614388)Termination phase: Saturation % 33.57/5.48 % (1614388)Time elapsed: 0.249 s % 33.57/5.48 % (1614388)Peak memory usage: 90 MB % 33.57/5.48 % (1614388)Instructions burned: 440 (million) % 33.57/5.48 % (1614396)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1809414600:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2977 on theBenchmark for (2977ds/1016Mi) % 33.57/5.48 % (1614396)Refutation not found, incomplete strategy % 33.57/5.48 % (1614396)------------------------------ % 33.57/5.48 % (1614396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.57/5.48 % (1614396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.57/5.48 % (1614396)CaDiCaL version: 2.1.3 % 33.57/5.48 % (1614396)Termination reason: Refutation not found, incomplete strategy % 33.57/5.48 % (1614396)Time elapsed: 0.002 s % 33.57/5.48 % (1614396)Peak memory usage: 89 MB % 33.57/5.48 % (1614396)Instructions burned: 2 (million) % 33.57/5.48 % Exception at run slice level % 33.57/5.48 User error: GNN currently only supports monomorphic FOL. % 33.57/5.48 % (1614398)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1401051355:i=14123:bd=preordered:ins=4_2976 on theBenchmark for (2976ds/14123Mi) % 33.57/5.48 % (1614394)Instruction limit reached! % 33.57/5.48 % (1614394)------------------------------ % 33.57/5.48 % (1614394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.57/5.48 % (1614394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.57/5.48 % (1614394)CaDiCaL version: 2.1.3 % 33.57/5.48 % (1614394)Termination reason: Instruction limit % 33.57/5.48 % (1614394)Termination phase: Saturation % 33.57/5.48 % (1614394)Time elapsed: 0.239 s % 33.57/5.48 % (1614394)Peak memory usage: 90 MB % 33.57/5.48 % (1614394)Instructions burned: 525 (million) % 33.57/5.48 % Exception at run slice level % 33.57/5.48 User error: GNN currently only supports monomorphic FOL. % 33.57/5.48 % (1614400)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1478238102:i=5781:kws=precedence:bd=all:rawr=on_2975 on theBenchmark for (2975ds/5781Mi) % 33.57/5.48 % (1614396)------------------------------ % 33.57/5.48 % (1614396)------------------------------ % 33.57/5.48 % (1614402)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=4094153564:i=2448:gtgl=5:bd=preordered:gtg=all_2974 on theBenchmark for (2974ds/2448Mi) % 33.57/5.48 % (1614404)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=104325977:i=3223:kws=precedence:fgj=on:av=off_2973 on theBenchmark for (2973ds/3223Mi) % 33.57/5.48 % (1614378)Instruction limit reached! % 33.57/5.48 % (1614378)------------------------------ % 33.57/5.48 % (1614378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.57/5.48 % (1614378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.57/5.48 % (1614378)CaDiCaL version: 2.1.3 % 33.57/5.48 % (1614378)Termination reason: Instruction limit % 33.57/5.48 % (1614378)Termination phase: Saturation % 33.57/5.48 % (1614378)Time elapsed: 1.071 s % 33.57/5.48 % (1614378)Peak memory usage: 104 MB % 33.57/5.48 % (1614378)Instructions burned: 3707 (million) % 33.57/5.48 % (1614405)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1520706271:st=5.6:i=2033:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/2033Mi) % 33.57/5.48 % (1614408)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1276770622:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2972 on theBenchmark for (2972ds/2055Mi) % 41.88/6.77 % Exception at run slice level % 41.88/6.77 User error: GNN currently only supports monomorphic FOL. % 41.88/6.77 % (1614411)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=804783747:i=21611:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/21611Mi) % 41.88/6.77 % Exception at run slice level % 41.88/6.77 User error: GNN currently only supports monomorphic FOL. % 41.88/6.77 % Exception at run slice level % 41.88/6.77 User error: GNN currently only supports monomorphic FOL. % 41.88/6.77 % Exception at run slice level % 41.88/6.77 User error: GNN currently only supports monomorphic FOL. % 41.88/6.77 % (1614414)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=618126382:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2969 on theBenchmark for (2969ds/797Mi) % 41.88/6.77 % Exception at run slice level % 41.88/6.77 User error: GNN currently only supports monomorphic FOL. % 41.88/6.77 % (1614413)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=421665785:i=4835:sd=13:ss=axioms:sgt=23_2969 on theBenchmark for (2969ds/4835Mi) % 41.88/6.77 % (1614415)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1266651349:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2969 on theBenchmark for (2969ds/2326Mi) % 41.88/6.77 % (1614417)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2423315082:i=6038:nm=6_2968 on theBenchmark for (2968ds/6038Mi) % 41.88/6.77 % Exception at run slice level % 41.88/6.77 User error: GNN currently only supports monomorphic FOL. % 41.88/6.77 % (1614414)Instruction limit reached! % 41.88/6.77 % (1614414)------------------------------ % 41.88/6.77 % (1614414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.88/6.77 % (1614414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.88/6.77 % (1614414)CaDiCaL version: 2.1.3 % 41.88/6.77 % (1614414)Termination reason: Instruction limit % 41.88/6.77 % (1614414)Termination phase: Saturation % 41.88/6.77 % (1614414)Time elapsed: 0.247 s % 41.88/6.77 % (1614414)Peak memory usage: 96 MB % 41.88/6.77 % (1614414)Instructions burned: 801 (million) % 41.88/6.77 % (1614422)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=998366849:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2966 on theBenchmark for (2966ds/1008Mi) % 41.88/6.77 % (1614421)lrs+10_1_sil=32000:sp=occurrence:random_seed=3327754166:st=2:i=33334:sd=3:ss=included:sgt=32_2966 on theBenchmark for (2966ds/33334Mi) % 41.88/6.77 % Exception at run slice level % 41.88/6.77 User error: GNN currently only supports monomorphic FOL. % 41.88/6.77 % (1614422)Instruction limit reached! % 41.88/6.77 % (1614422)------------------------------ % 41.88/6.77 % (1614422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.88/6.77 % (1614422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.88/6.77 % (1614422)CaDiCaL version: 2.1.3 % 41.88/6.77 % (1614422)Termination reason: Instruction limit % 41.88/6.77 % (1614422)Termination phase: Saturation % 41.88/6.77 % (1614422)Time elapsed: 0.280 s % 41.88/6.77 % (1614422)Peak memory usage: 97 MB % 41.88/6.77 % (1614422)Instructions burned: 1010 (million) % 41.88/6.77 % (1614425)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=3124957040:i=8327:s2at=5:bd=preordered_2963 on theBenchmark for (2963ds/8327Mi) % 41.88/6.77 % (1614426)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=776140314:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2962 on theBenchmark for (2962ds/1083Mi) % 41.88/6.77 % (1614426)Instruction limit reached! % 41.88/6.77 % (1614426)------------------------------ % 41.88/6.77 % (1614426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.88/6.77 % (1614426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.88/6.77 % (1614426)CaDiCaL version: 2.1.3 % 41.88/6.77 % (1614426)Termination reason: Instruction limit % 41.88/6.77 % (1614426)Termination phase: Saturation % 41.88/6.77 % (1614426)Time elapsed: 0.283 s % 41.88/6.77 % (1614426)Peak memory usage: 94 MB % 41.88/6.77 % (1614426)Instructions burned: 1087 (million) % 41.88/6.77 % Exception at run slice level % 48.95/7.71 User error: GNN currently only supports monomorphic FOL. % 48.95/7.71 % (1614429)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=3872613049:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2958 on theBenchmark for (2958ds/1084Mi) % 48.95/7.71 % (1614429)Refutation not found, incomplete strategy % 48.95/7.71 % (1614429)------------------------------ % 48.95/7.71 % (1614429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.95/7.71 % (1614429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.95/7.71 % (1614429)CaDiCaL version: 2.1.3 % 48.95/7.71 % (1614429)Termination reason: Refutation not found, incomplete strategy % 48.95/7.71 % (1614429)Time elapsed: 0.001 s % 48.95/7.71 % (1614429)Peak memory usage: 88 MB % 48.95/7.71 % (1614429)Instructions burned: 2 (million) % 48.95/7.71 % (1614370)Instruction limit reached! % 48.95/7.71 % (1614370)------------------------------ % 48.95/7.71 % (1614370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.95/7.71 % (1614370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.95/7.71 % (1614370)CaDiCaL version: 2.1.3 % 48.95/7.71 % (1614370)Termination reason: Instruction limit % 48.95/7.71 % (1614370)Termination phase: Saturation % 48.95/7.71 % (1614370)Time elapsed: 2.741 s % 48.95/7.71 % (1614370)Peak memory usage: 129 MB % 48.95/7.71 % (1614370)Instructions burned: 4851 (million) % 48.95/7.71 % (1614430)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3045347440:i=6995:s2at=5:gtg=all_2958 on theBenchmark for (2958ds/6995Mi) % 48.95/7.71 % (1614429)------------------------------ % 48.95/7.71 % (1614429)------------------------------ % 48.95/7.71 % (1614432)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=47694843:st=2:i=6225:sd=15:ss=axioms_2957 on theBenchmark for (2957ds/6225Mi) % 48.95/7.71 % (1614432)Refutation not found, incomplete strategy % 48.95/7.71 % (1614432)------------------------------ % 48.95/7.71 % (1614432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.95/7.71 % (1614432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.95/7.71 % (1614432)CaDiCaL version: 2.1.3 % 48.95/7.71 % (1614432)Termination reason: Refutation not found, incomplete strategy % 48.95/7.71 % (1614432)Time elapsed: 0.006 s % 48.95/7.71 % (1614432)Peak memory usage: 88 MB % 48.95/7.71 % (1614432)Instructions burned: 8 (million) % 48.95/7.71 % (1614434)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3572780252:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2956 on theBenchmark for (2956ds/3372Mi) % 48.95/7.71 % (1614432)------------------------------ % 48.95/7.71 % (1614432)------------------------------ % 48.95/7.71 % Exception at run slice level % 48.95/7.71 User error: GNN currently only supports monomorphic FOL. % 48.95/7.71 % Exception at run slice level % 48.95/7.71 User error: GNN currently only supports monomorphic FOL. % 48.95/7.71 % (1614415)Instruction limit reached! % 48.95/7.71 % (1614415)------------------------------ % 48.95/7.71 % (1614415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.95/7.71 % (1614415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.95/7.71 % (1614415)CaDiCaL version: 2.1.3 % 48.95/7.71 % (1614415)Termination reason: Instruction limit % 48.95/7.71 % (1614415)Termination phase: Saturation % 48.95/7.71 % (1614415)Time elapsed: 1.436 s % 48.95/7.71 % (1614415)Peak memory usage: 95 MB % 48.95/7.71 % (1614415)Instructions burned: 2326 (million) % 48.95/7.71 % (1614438)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=2201862291:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2953 on theBenchmark for (2953ds/13494Mi) % 48.95/7.71 % (1614437)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2749384201:st=2.3:i=26457:sd=10:ss=included:sgt=8_2953 on theBenchmark for (2953ds/26457Mi) % 48.95/7.71 % (1614439)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=4262260595:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2953 on theBenchmark for (2953ds/2503Mi) % 48.95/7.71 % (1614439)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 48.95/7.71 % (1614440)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=437030888:i=2559:sd=1:ep=RSTC:ss=axioms_2953 on theBenchmark for (2953ds/2559Mi) % 57.73/9.02 % Exception at run slice level % 57.73/9.02 User error: GNN currently only supports monomorphic FOL. % 57.73/9.02 % (1614445)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3712861574:i=30753:av=off:ss=included_2950 on theBenchmark for (2950ds/30753Mi) % 57.73/9.02 % Exception at run slice level % 57.73/9.02 User error: GNN currently only supports monomorphic FOL. % 57.73/9.02 % Exception at run slice level % 57.73/9.02 User error: GNN currently only supports monomorphic FOL. % 57.73/9.02 % Exception at run slice level % 57.73/9.02 User error: GNN currently only supports monomorphic FOL. % 57.73/9.02 % (1614447)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3111288130:i=26473:ep=RSTC_2948 on theBenchmark for (2948ds/26473Mi) % 57.73/9.02 % Exception at run slice level % 57.73/9.02 User error: GNN currently only supports monomorphic FOL. % 57.73/9.02 % (1614448)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=938893198:cts=off:i=2759:kws=inv_arity:fgj=on_2948 on theBenchmark for (2948ds/2759Mi) % 57.73/9.02 % (1614449)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=1907616566:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2948 on theBenchmark for (2948ds/5665Mi) % 57.73/9.02 % (1614449)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 57.73/9.02 % (1614451)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=388064963:i=1532:ep=RS:ss=axioms_2947 on theBenchmark for (2947ds/1532Mi) % 57.73/9.02 % Exception at run slice level % 57.73/9.02 User error: GNN currently only supports monomorphic FOL. % 57.73/9.02 % (1614455)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=2027840828:i=1565:sd=2:ss=axioms:sgt=32_2944 on theBenchmark for (2944ds/1565Mi) % 57.73/9.02 % Exception at run slice level % 57.73/9.02 User error: GNN currently only supports monomorphic FOL. % 57.73/9.02 % Exception at run slice level % 57.73/9.02 User error: GNN currently only supports monomorphic FOL. % 57.73/9.02 % (1614457)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=4269725882:i=1572:fgj=on:gsp=on_2943 on theBenchmark for (2943ds/1572Mi) % 57.73/9.02 % (1614458)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=4109846319:i=6052:sd=4:ss=axioms:sgt=24_2943 on theBenchmark for (2943ds/6052Mi) % 57.73/9.02 % (1614457)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 57.73/9.02 % (1614400)Instruction limit reached! % 57.73/9.02 % (1614400)------------------------------ % 57.73/9.02 % (1614400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.73/9.02 % (1614400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.73/9.02 % (1614400)CaDiCaL version: 2.1.3 % 57.73/9.02 % (1614400)Termination reason: Instruction limit % 57.73/9.02 % (1614400)Termination phase: Saturation % 57.73/9.02 % (1614400)Time elapsed: 3.160 s % 57.73/9.02 % (1614400)Peak memory usage: 103 MB % 57.73/9.02 % (1614400)Instructions burned: 5781 (million) % 57.73/9.02 % Exception at run slice level % 57.73/9.02 User error: GNN currently only supports monomorphic FOL. % 57.73/9.02 % (1614461)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=476444627:i=3500:sd=1:bd=preordered:sup=off:ss=included_2942 on theBenchmark for (2942ds/3500Mi) % 57.73/9.02 % (1614462)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=1468607982:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2941 on theBenchmark for (2941ds/1842Mi) % 57.73/9.02 % (1614462)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 57.73/9.02 % (1614413)Instruction limit reached! % 57.73/9.02 % (1614413)------------------------------ % 57.73/9.02 % (1614413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.33/10.40 % (1614413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.33/10.40 % (1614413)CaDiCaL version: 2.1.3 % 68.33/10.40 % (1614413)Termination reason: Instruction limit % 68.33/10.40 % (1614413)Termination phase: Saturation % 68.33/10.40 % (1614413)Time elapsed: 2.903 s % 68.33/10.40 % (1614413)Peak memory usage: 105 MB % 68.33/10.40 % (1614413)Instructions burned: 4836 (million) % 68.33/10.40 % Exception at run slice level % 68.33/10.40 User error: GNN currently only supports monomorphic FOL. % 68.33/10.40 % Exception at run slice level % 68.33/10.40 User error: GNN currently only supports monomorphic FOL. % 68.33/10.40 % Exception at run slice level % 68.33/10.40 User error: GNN currently only supports monomorphic FOL. % 68.33/10.40 % (1614466)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=1717711323:i=1884:sd=1:nm=60:ss=axioms_2939 on theBenchmark for (2939ds/1884Mi) % 68.33/10.40 % (1614465)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1285334829:i=66096:add=on_2939 on theBenchmark for (2939ds/66096Mi) % 68.33/10.40 % (1614467)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3544715909:cts=off:i=5469:bs=on:fsr=off_2938 on theBenchmark for (2938ds/5469Mi) % 68.33/10.40 % Exception at run slice level % 68.33/10.40 User error: GNN currently only supports monomorphic FOL.% (1614468)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=3347159597:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2938 on theBenchmark for (2938ds/2037Mi) % 68.33/10.40 % 68.33/10.40 % Exception at run slice level % 68.33/10.40 User error: GNN currently only supports monomorphic FOL. % 68.33/10.40 % (1614473)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3879790949:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2937 on theBenchmark for (2937ds/2110Mi) % 68.33/10.40 % (1614474)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=1788336812:i=2430:add=off:aac=none:nm=16_2936 on theBenchmark for (2936ds/2430Mi) % 68.33/10.40 % Exception at run slice level % 68.33/10.40 User error: GNN currently only supports monomorphic FOL. % 68.33/10.40 % Exception at run slice level % 68.33/10.40 User error: GNN currently only supports monomorphic FOL. % 68.33/10.40 % Exception at run slice level % 68.33/10.40 User error: GNN currently only supports monomorphic FOL. % 68.33/10.40 % (1614477)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=574410093:cond=fast:i=4891_2934 on theBenchmark for (2934ds/4891Mi) % 68.33/10.40 % (1614479)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=541319360:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2933 on theBenchmark for (2933ds/7534Mi) % 68.33/10.40 % Exception at run slice level % 68.33/10.40 User error: GNN currently only supports monomorphic FOL. % 68.33/10.40 % (1614478)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=9651004:st=2:i=14845:sd=2:ss=included:fsd=on_2933 on theBenchmark for (2933ds/14845Mi) % 68.33/10.40 % (1614482)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=1807329093:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2932 on theBenchmark for (2932ds/10353Mi) % 68.33/10.40 % Exception at run slice level % 68.33/10.40 User error: GNN currently only supports monomorphic FOL. % 68.33/10.40 % (1614485)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3174206408:i=7860_2930 on theBenchmark for (2930ds/7860Mi) % 68.33/10.40 % (1614485)Refutation not found, incomplete strategy % 68.33/10.40 % (1614485)------------------------------ % 68.33/10.40 % (1614485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.33/10.40 % (1614485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.33/10.40 % (1614485)CaDiCaL version: 2.1.3 % 68.33/10.40 % (1614485)Termination reason: Refutation not found, incomplete strategy % 68.33/10.40 % (1614485)Time elapsed: 0.004 s % 68.33/10.40 % (1614485)Peak memory usage: 88 MB % 68.33/10.40 % (1614485)Instructions burned: 10 (million) % 105.05/15.50 % Exception at run slice level % 105.05/15.50 User error: GNN currently only supports monomorphic FOL. % 105.05/15.50 % Exception at run slice level % 105.05/15.50 User error: GNN currently only supports monomorphic FOL. % 105.05/15.50 % (1614485)------------------------------ % 105.05/15.50 % (1614485)------------------------------ % 105.05/15.50 % (1614487)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=282932980:i=7896:sd=2:bs=on:ss=included:sgt=20_2929 on theBenchmark for (2929ds/7896Mi) % 105.05/15.50 % Exception at run slice level % 105.05/15.50 User error: GNN currently only supports monomorphic FOL. % 105.05/15.50 % (1614488)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=430056787:i=5812:gtgl=2:gtg=all_2928 on theBenchmark for (2928ds/5812Mi) % 105.05/15.50 % (1614489)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=3964419513:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2928 on theBenchmark for (2928ds/2965Mi) % 105.05/15.50 % (1614491)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=3954622711:i=2967:kws=precedence:bd=preordered:av=off_2927 on theBenchmark for (2927ds/2967Mi) % 105.05/15.50 % Exception at run slice level % 105.05/15.50 User error: GNN currently only supports monomorphic FOL. % 105.05/15.50 % Exception at run slice level % 105.05/15.50 User error: GNN currently only supports monomorphic FOL. % 105.05/15.50 % (1614495)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=637200474:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2925 on theBenchmark for (2925ds/3022Mi) % 105.05/15.50 % Exception at run slice level % 105.05/15.50 User error: GNN currently only supports monomorphic FOL. % 105.05/15.50 % (1614496)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=3220870966:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2924 on theBenchmark for (2924ds/3207Mi) % 105.05/15.50 % Exception at run slice level % 105.05/15.50 User error: GNN currently only supports monomorphic FOL. % 105.05/15.50 % (1614498)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=1774451646:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2923 on theBenchmark for (2923ds/3289Mi) % 105.05/15.50 % Exception at run slice level % 105.05/15.50 User error: GNN currently only supports monomorphic FOL. % 105.05/15.50 % (1614502)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=1479316659:cts=off:i=3394_2922 on theBenchmark for (2922ds/3394Mi) % 105.05/15.50 % (1614500)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=3135429896:i=38569:sd=3:ss=axioms:sgt=32_2922 on theBenchmark for (2922ds/38569Mi) % 105.05/15.50 % Exception at run slice level % 105.05/15.50 User error: GNN currently only supports monomorphic FOL. % 105.05/15.50 % Exception at run slice level % 105.05/15.50 User error: GNN currently only supports monomorphic FOL. % 105.05/15.50 % Exception at run slice level % 105.05/15.50 User error: GNN currently only supports monomorphic FOL. % 105.05/15.50 % (1614505)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=624246863:i=33824:bd=preordered_2919 on theBenchmark for (2919ds/33824Mi) % 105.05/15.50 % (1614506)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=2962988248:i=20684:bd=all:gtg=exists_sym_2919 on theBenchmark for (2919ds/20684Mi) % 105.05/15.50 % Exception at run slice level % 105.05/15.50 User error: GNN currently only supports monomorphic FOL. % 105.05/15.50 % (1614507)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=3170809306: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_2919 on theBenchmark for (2919ds/7222Mi) % 105.05/15.50 % (1614507)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 105.05/15.50 % Exception at run slice level % 105.05/15.50 User error: GNN currently only supports monomorphic FOL. % 119.65/17.70 % (1614510)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=3398759137:st=4:i=7295:sd=4:ep=R:ss=axioms_2917 on theBenchmark for (2917ds/7295Mi) % 119.65/17.70 % (1614512)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=1919881319:i=4036:ins=10_2916 on theBenchmark for (2916ds/4036Mi) % 119.65/17.70 % Exception at run slice level % 119.65/17.70 User error: GNN currently only supports monomorphic FOL. % 119.65/17.70 % Exception at run slice level % 119.65/17.70 User error: GNN currently only supports monomorphic FOL. % 119.65/17.70 % Exception at run slice level % 119.65/17.70 User error: GNN currently only supports monomorphic FOL. % 119.65/17.70 % (1614515)lrs+10_1_sil=128000:lcm=predicate:random_seed=3793655461:st=3:i=43697:sd=5:ss=axioms_2914 on theBenchmark for (2914ds/43697Mi) % 119.65/17.70 % (1614517)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=747904046:i=4547:bd=preordered_2914 on theBenchmark for (2914ds/4547Mi) % 119.65/17.70 % Exception at run slice level % 119.65/17.70 User error: GNN currently only supports monomorphic FOL. % 119.65/17.70 % (1614516)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=2916100085:i=17599:gtg=all:ss=axioms:fsd=on_2914 on theBenchmark for (2914ds/17599Mi) % 119.65/17.70 % (1614521)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=3427248393:i=9294:av=off_2912 on theBenchmark for (2912ds/9294Mi) % 119.65/17.70 % Exception at run slice level % 119.65/17.70 User error: GNN currently only supports monomorphic FOL. % 119.65/17.70 % (1614523)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2929227670:i=32849:add=on_2911 on theBenchmark for (2911ds/32849Mi) % 119.65/17.70 % Exception at run slice level % 119.65/17.70 User error: GNN currently only supports monomorphic FOL. % 119.65/17.70 % Exception at run slice level % 119.65/17.70 User error: GNN currently only supports monomorphic FOL. % 119.65/17.70 % Exception at run slice level % 119.65/17.70 User error: GNN currently only supports monomorphic FOL. % 119.65/17.70 % (1614525)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=552621227:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2909 on theBenchmark for (2909ds/4793Mi) % 119.65/17.70 % (1614526)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=2893170141:i=4840:nm=4:av=off_2908 on theBenchmark for (2908ds/4840Mi) % 119.65/17.70 % (1614527)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=1908183961:cts=off:i=5002_2908 on theBenchmark for (2908ds/5002Mi) % 119.65/17.70 % Exception at run slice level % 119.65/17.70 User error: GNN currently only supports monomorphic FOL. % 119.65/17.70 % (1614531)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=1811633619:i=30479:sd=3:ss=axioms_2905 on theBenchmark for (2905ds/30479Mi) % 119.65/17.70 % (1614467)Instruction limit reached! % 119.65/17.70 % (1614467)------------------------------ % 119.65/17.70 % (1614467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.65/17.70 % (1614467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.65/17.70 % (1614467)CaDiCaL version: 2.1.3 % 119.65/17.70 % (1614467)Termination reason: Instruction limit % 119.65/17.70 % (1614467)Termination phase: Saturation % 119.65/17.70 % (1614467)Time elapsed: 3.317 s % 119.65/17.70 % (1614467)Peak memory usage: 97 MB % 119.65/17.70 % (1614467)Instructions burned: 5469 (million) % 119.65/17.70 % Exception at run slice level % 119.65/17.70 User error: GNN currently only supports monomorphic FOL. % 119.65/17.70 % (1614533)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=4080003649:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2904 on theBenchmark for (2904ds/11035Mi) % 119.65/17.70 % (1614533)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 119.65/17.70 % Exception at run slice level % 155.54/22.64 User error: GNN currently only supports monomorphic FOL. % 155.54/22.64 % (1614534)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=3315303123:i=5835_2904 on theBenchmark for (2904ds/5835Mi) % 155.54/22.64 % Exception at run slice level % 155.54/22.64 User error: GNN currently only supports monomorphic FOL. % 155.54/22.64 % (1614536)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=1513563164:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2902 on theBenchmark for (2902ds/5890Mi) % 155.54/22.64 % (1614538)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=2415439551:cts=off:i=19910:ep=RS_2902 on theBenchmark for (2902ds/19910Mi) % 155.54/22.64 % Exception at run slice level % 155.54/22.64 User error: GNN currently only supports monomorphic FOL. % 155.54/22.64 % Exception at run slice level % 155.54/22.64 User error: GNN currently only supports monomorphic FOL. % 155.54/22.64 % (1614542)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=3901656314:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2899 on theBenchmark for (2899ds/13822Mi) % 155.54/22.64 % (1614541)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=951574109:i=20312:bd=preordered:fsr=off:er=filter_2899 on theBenchmark for (2899ds/20312Mi) % 155.54/22.64 % Exception at run slice level % 155.54/22.64 User error: GNN currently only supports monomorphic FOL. % 155.54/22.64 % (1614545)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=2620913019:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2897 on theBenchmark for (2897ds/7144Mi) % 155.54/22.64 % Exception at run slice level % 155.54/22.64 User error: GNN currently only supports monomorphic FOL. % 155.54/22.64 % Exception at run slice level % 155.54/22.64 User error: GNN currently only supports monomorphic FOL. % 155.54/22.64 % (1614547)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=1632962418:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2893 on theBenchmark for (2893ds/15184Mi) % 155.54/22.64 % (1614548)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=3141777988:i=107375_2893 on theBenchmark for (2893ds/107375Mi) % 155.54/22.64 % Exception at run slice level % 155.54/22.64 User error: GNN currently only supports monomorphic FOL. % 155.54/22.64 % Exception at run slice level % 155.54/22.64 User error: GNN currently only supports monomorphic FOL. % 155.54/22.64 % (1614552)dis+10_128_sil=16000:nwc=0.7:random_seed=2631530601:i=15999:nm=2:gsp=on_2888 on theBenchmark for (2888ds/15999Mi) % 155.54/22.64 % (1614551)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=3455373516:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2888 on theBenchmark for (2888ds/7958Mi) % 155.54/22.64 % (1614552)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 155.54/22.64 % Exception at run slice level % 155.54/22.64 User error: GNN currently only supports monomorphic FOL. % 155.54/22.64 % (1614555)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=2318295769:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2884 on theBenchmark for (2884ds/8139Mi) % 155.54/22.64 % (1614545)Instruction limit reached! % 155.54/22.64 % (1614545)------------------------------ % 155.54/22.64 % (1614545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.54/22.64 % (1614545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.54/22.64 % (1614545)CaDiCaL version: 2.1.3 % 155.54/22.64 % (1614545)Termination reason: Instruction limit % 155.54/22.64 % (1614545)Termination phase: Saturation % 155.54/22.64 % (1614545)Time elapsed: 3.780 s % 155.54/22.64 % (1614545)Peak memory usage: 105 MB % 155.54/22.64 % (1614545)Instructions burned: 7146 (million) % 155.54/22.64 % (1614900)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=839856986:st=4:i=8950:sd=5:ss=axioms_2858 on theBenchmark for (2858ds/8950Mi) % 155.54/22.64 % Exception at run slice level % 155.54/22.64 User error: GNN currently only supports monomorphic FOL. % 155.54/22.64 % (1614902)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=3905662601:i=9809:ins=10:av=off_2853 on theBenchmark for (2853ds/9809Mi) % 183.19/26.57 % (1614555)Instruction limit reached! % 183.19/26.57 % (1614555)------------------------------ % 183.19/26.57 % (1614555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.19/26.57 % (1614555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.19/26.57 % (1614555)CaDiCaL version: 2.1.3 % 183.19/26.57 % (1614555)Termination reason: Instruction limit % 183.19/26.57 % (1614555)Termination phase: Saturation % 183.19/26.57 % (1614555)Time elapsed: 3.415 s % 183.19/26.57 % (1614555)Peak memory usage: 91 MB % 183.19/26.57 % (1614555)Instructions burned: 8140 (million) % 183.19/26.57 % Exception at run slice level % 183.19/26.57 User error: GNN currently only supports monomorphic FOL. % 183.19/26.57 % (1614904)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=852679683:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2848 on theBenchmark for (2848ds/9885Mi) % 183.19/26.57 % (1614905)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=1926786280:cond=fast:i=32078:fgj=on:av=off_2848 on theBenchmark for (2848ds/32078Mi) % 183.19/26.57 % Exception at run slice level % 183.19/26.57 User error: GNN currently only supports monomorphic FOL. % 183.19/26.57 % Exception at run slice level % 183.19/26.57 User error: GNN currently only supports monomorphic FOL. % 183.19/26.57 % (1614908)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=1696818582:i=11101:bd=all:ss=axioms:sgt=8_2843 on theBenchmark for (2843ds/11101Mi) % 183.19/26.57 % (1614909)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=775263214:cond=on:i=13220:s2at=3:aac=none:fsd=on_2843 on theBenchmark for (2843ds/13220Mi) % 183.19/26.57 % (1614538)Instruction limit reached! % 183.19/26.57 % (1614538)------------------------------ % 183.19/26.57 % (1614538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.19/26.57 % (1614538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.19/26.57 % (1614538)CaDiCaL version: 2.1.3 % 183.19/26.57 % (1614538)Termination reason: Instruction limit % 183.19/26.57 % (1614538)Termination phase: Saturation % 183.19/26.57 % (1614538)Time elapsed: 6.026 s % 183.19/26.57 % (1614538)Peak memory usage: 184 MB % 183.19/26.57 % (1614538)Instructions burned: 19913 (million) % 183.19/26.57 % (1614912)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=2630624025:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2841 on theBenchmark for (2841ds/13528Mi) % 183.19/26.57 % Exception at run slice level % 183.19/26.57 User error: GNN currently only supports monomorphic FOL. % 183.19/26.57 % Exception at run slice level % 183.19/26.57 User error: GNN currently only supports monomorphic FOL. % 183.19/26.57 % (1614915)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=958965067:i=14974:ss=axioms:sgt=16_2838 on theBenchmark for (2838ds/14974Mi) % 183.19/26.57 % (1614914)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=3050686854:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2838 on theBenchmark for (2838ds/14854Mi) % 183.19/26.57 % Exception at run slice level % 183.19/26.57 User error: GNN currently only supports monomorphic FOL. % 183.19/26.57 % (1614918)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=3118590765:i=33081:aac=none:fgj=on:bd=all:fsr=off_2835 on theBenchmark for (2835ds/33081Mi) % 183.19/26.57 % Exception at run slice level % 183.19/26.57 User error: GNN currently only supports monomorphic FOL. % 183.19/26.57 % Exception at run slice level % 183.19/26.57 User error: GNN currently only supports monomorphic FOL. % 183.19/26.57 % (1614920)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=341526289:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2833 on theBenchmark for (2833ds/50856Mi) % 183.19/26.57 % (1614921)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=1605412520:i=69865_2832 on theBenchmark for (2832ds/69865Mi) % 183.19/26.57 % Exception at run slice level % 203.49/29.48 User error: GNN currently only supports monomorphic FOL. % 203.49/29.48 % (1614924)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=3865800357:cond=fast:i=17802:gtgl=3:gtg=all_2829 on theBenchmark for (2829ds/17802Mi) % 203.49/29.48 % Exception at run slice level % 203.49/29.48 User error: Immediate (shared) subterms of term/literal huffma107959123e_case(X1,X0,X5,X4,huffma2021818691e_Leaf(X1,X3,X2)) = sF27(X1,X0,X5,X4,X3,X2) have different types/not well-typed! % 203.49/29.48 % Exception at run slice level % 203.49/29.48 User error: GNN currently only supports monomorphic FOL. % 203.49/29.48 % (1614926)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=1305498939:i=96644_2829 on theBenchmark for (2829ds/96644Mi) % 203.49/29.48 % (1614927)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 203.49/29.48 % (1614927)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=1323583267:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2828 on theBenchmark for (2828ds/21161Mi) % 203.49/29.48 % (1614552)Instruction limit reached! % 203.49/29.48 % (1614552)------------------------------ % 203.49/29.48 % (1614552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.49/29.48 % (1614552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.49/29.48 % (1614552)CaDiCaL version: 2.1.3 % 203.49/29.48 % (1614552)Termination reason: Instruction limit % 203.49/29.48 % (1614552)Termination phase: Saturation % 203.49/29.48 % (1614552)Time elapsed: 7.966 s % 203.49/29.48 % (1614552)Peak memory usage: 129 MB % 203.49/29.48 % (1614552)Instructions burned: 15999 (million) % 203.49/29.48 % (1614930)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=1990884426:i=22761:gtg=all:ss=axioms:fsd=on_2807 on theBenchmark for (2807ds/22761Mi) % 203.49/29.48 % Exception at run slice level % 203.49/29.48 User error: GNN currently only supports monomorphic FOL. % 203.49/29.48 % (1614932)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=3753694300:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2803 on theBenchmark for (2803ds/23713Mi) % 203.49/29.48 % (1614447)Instruction limit reached! % 203.49/29.48 % (1614447)------------------------------ % 203.49/29.48 % (1614447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.49/29.48 % (1614447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.49/29.48 % (1614447)CaDiCaL version: 2.1.3 % 203.49/29.48 % (1614447)Termination reason: Instruction limit % 203.49/29.48 % (1614447)Termination phase: Saturation % 203.49/29.48 % (1614447)Time elapsed: 14.980 s % 203.49/29.48 % (1614447)Peak memory usage: 307 MB % 203.49/29.48 % (1614447)Instructions burned: 26474 (million) % 203.49/29.48 % (1614934)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=1303833844:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2797 on theBenchmark for (2797ds/26509Mi) % 203.49/29.48 % Exception at run slice level % 203.49/29.48 User error: GNN currently only supports monomorphic FOL. % 203.49/29.48 % (1614936)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=2961543903:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2792 on theBenchmark for (2792ds/28957Mi) % 203.49/29.48 % (1614908)Instruction limit reached! % 203.49/29.48 % (1614908)------------------------------ % 203.49/29.48 % (1614908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.49/29.48 % (1614908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.49/29.48 % (1614908)CaDiCaL version: 2.1.3 % 203.49/29.48 % (1614908)Termination reason: Instruction limit % 203.49/29.48 % (1614908)Termination phase: Saturation % 203.49/29.48 % (1614908)Time elapsed: 6.122 s % 203.49/29.48 % (1614908)Peak memory usage: 130 MB % 203.49/29.48 % (1614908)Instructions burned: 11103 (million) % 203.49/29.48 % (1614421)Instruction limit reached! % 203.49/29.48 % (1614421)------------------------------ % 203.49/29.48 % (1614421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.49/29.48 % (1614421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.49/29.48 % (1614421)CaDiCaL version: 2.1.3 % 203.49/29.48 % (1614421)Termination reason: Instruction limit % 210.85/30.47 % (1614421)Termination phase: Saturation % 210.85/30.47 % (1614421)Time elapsed: 18.449 s % 210.85/30.47 % (1614421)Peak memory usage: 160 MB % 210.85/30.47 % (1614421)Instructions burned: 33336 (million) % 210.85/30.47 % (1614938)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=2550519823:i=29246:s2at=-1:kws=inv_arity:ins=10_2781 on theBenchmark for (2781ds/29246Mi) % 210.85/30.47 % (1614939)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=2150834407:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2780 on theBenchmark for (2780ds/30082Mi) % 210.85/30.47 % (1614939)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 210.85/30.47 % Exception at run slice level % 210.85/30.47 User error: GNN currently only supports monomorphic FOL. % 210.85/30.47 % Exception at run slice level % 210.85/30.47 User error: GNN currently only supports monomorphic FOL. % 210.85/30.47 % (1614942)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=1388383463:i=32262:bd=preordered_2776 on theBenchmark for (2776ds/32262Mi) % 210.85/30.47 % (1614943)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=4210098798:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2775 on theBenchmark for (2775ds/32870Mi) % 210.85/30.47 % Exception at run slice level % 210.85/30.47 User error: GNN currently only supports monomorphic FOL. % 210.85/30.47 % Exception at run slice level % 210.85/30.47 User error: GNN currently only supports monomorphic FOL. % 210.85/30.47 % (1614946)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=1661222320:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2771 on theBenchmark for (2771ds/33295Mi) % 210.85/30.47 % (1614947)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=2295758568:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2770 on theBenchmark for (2770ds/36826Mi) % 210.85/30.47 % Exception at run slice level % 210.85/30.47 User error: GNN currently only supports monomorphic FOL. % 210.85/30.47 % (1614950)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=2161069348:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2766 on theBenchmark for (2766ds/92981Mi) % 210.85/30.47 % Exception at run slice level % 210.85/30.47 User error: GNN currently only supports monomorphic FOL. % 210.85/30.47 % (1614952)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=448266908:s2pl=on:i=49423_2761 on theBenchmark for (2761ds/49423Mi) % 210.85/30.47 % Exception at run slice level % 210.85/30.47 User error: GNN currently only supports monomorphic FOL. % 210.85/30.47 % (1614954)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=3846359309:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2757 on theBenchmark for (2757ds/57299Mi) % 210.85/30.47 % Exception at run slice level % 210.85/30.47 User error: GNN currently only supports monomorphic FOL. % 210.85/30.47 % (1614956)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=1266393692:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2752 on theBenchmark for (2752ds/127679Mi) % 210.85/30.47 % Exception at run slice level % 210.85/30.47 User error: GNN currently only supports monomorphic FOL. % 210.85/30.47 % (1614958)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=3761033752:i=69402:add=on:aac=none:fsr=off_2747 on theBenchmark for (2747ds/69402Mi) % 210.85/30.47 % Exception at run slice level % 210.85/30.47 User error: GNN currently only supports monomorphic FOL. % 210.85/30.47 % (1614960)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=621805582:i=100512:doe=on:fgj=on:bd=all:fsd=on_2742 on theBenchmark for (2742ds/100512Mi) % 220.73/31.99 % Exception at run slice level % 220.73/31.99 User error: GNN currently only supports monomorphic FOL. % 220.73/31.99 % (1614962)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=3389329418:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2737 on theBenchmark for (2737ds/138761Mi) % 220.73/31.99 % Exception at run slice level % 220.73/31.99 User error: GNN currently only supports monomorphic FOL. % 220.73/31.99 % (1614964)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=3861907949:i=282386:rtra=on_2732 on theBenchmark for (2732ds/282386Mi) % 220.73/31.99 % Exception at run slice level % 220.73/31.99 User error: GNN currently only supports monomorphic FOL. % 220.73/31.99 % (1614966)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=2755716634:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2727 on theBenchmark for (2727ds/269354Mi) % 220.73/31.99 % Exception at run slice level % 220.73/31.99 User error: GNN currently only supports monomorphic FOL. % 220.73/31.99 % (1614968)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=323884756:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2722 on theBenchmark for (2722ds/283390Mi) % 220.73/31.99 % (1614968)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 220.73/31.99 % (1614927)Instruction limit reached! % 220.73/31.99 % (1614927)------------------------------ % 220.73/31.99 % (1614927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.73/31.99 % (1614927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.73/31.99 % (1614927)CaDiCaL version: 2.1.3 % 220.73/31.99 % (1614927)Termination reason: Instruction limit % 220.73/31.99 % (1614927)Termination phase: Saturation % 220.73/31.99 % (1614927)Time elapsed: 10.874 s % 220.73/31.99 % (1614927)Peak memory usage: 159 MB % 220.73/31.99 % (1614927)Instructions burned: 21162 (million) % 220.73/31.99 % Exception at run slice level % 220.73/31.99 User error: GNN currently only supports monomorphic FOL. % 220.73/31.99 % (1614979)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=31277325:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2718 on theBenchmark for (2718ds/218Mi) % 220.73/31.99 % (1614979)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 220.73/31.99 % (1614979)Refutation not found, incomplete strategy % 220.73/31.99 % (1614979)------------------------------ % 220.73/31.99 % (1614979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.73/31.99 % (1614979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.73/31.99 % (1614979)CaDiCaL version: 2.1.3 % 220.73/31.99 % (1614979)Termination reason: Refutation not found, incomplete strategy % 220.73/31.99 % (1614979)Time elapsed: 0.002 s % 220.73/31.99 % (1614979)Peak memory usage: 88 MB % 220.73/31.99 % (1614979)Instructions burned: 1 (million) % 220.73/31.99 % (1614988)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=2727243165:i=238:av=off:rtra=on:ss=axioms_2717 on theBenchmark for (2717ds/238Mi) % 220.73/31.99 % (1614988)Instruction limit reached! % 220.73/31.99 % (1614988)------------------------------ % 220.73/31.99 % (1614988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.73/31.99 % (1614988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.73/31.99 % (1614988)CaDiCaL version: 2.1.3 % 220.73/31.99 % (1614988)Termination reason: Instruction limit % 220.73/31.99 % (1614988)Termination phase: Saturation % 220.73/31.99 % (1614988)Time elapsed: 0.140 s % 220.73/31.99 % (1614988)Peak memory usage: 88 MB % 220.73/31.99 % (1614988)Instructions burned: 238 (million) % 220.73/31.99 % (1614979)------------------------------ % 220.73/31.99 % (1614979)------------------------------ % 220.73/31.99 % (1615090)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=3706318948:s2a=on:i=278:rtra=on:gtg=position_2715 on theBenchmark for (2715ds/278Mi) % 220.73/31.99 % (1615091)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=1733376596:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2714 on theBenchmark for (2714ds/258Mi) % 220.73/31.99 % (1615090)Instruction limit reached! % 220.73/31.99 % (1615090)------------------------------ % 229.08/33.06 % (1615090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.08/33.06 % (1615090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.08/33.06 % (1615090)CaDiCaL version: 2.1.3 % 229.08/33.06 % (1615090)Termination reason: Instruction limit % 229.08/33.06 % (1615090)Termination phase: Saturation % 229.08/33.06 % (1615090)Time elapsed: 0.178 s % 229.08/33.06 % (1615090)Peak memory usage: 90 MB % 229.08/33.06 % (1615090)Instructions burned: 279 (million) % 229.08/33.06 % (1615091)Instruction limit reached! % 229.08/33.06 % (1615091)------------------------------ % 229.08/33.06 % (1615091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.08/33.06 % (1615091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.08/33.06 % (1615091)CaDiCaL version: 2.1.3 % 229.08/33.06 % (1615091)Termination reason: Instruction limit % 229.08/33.06 % (1615091)Termination phase: Saturation % 229.08/33.06 % (1615091)Time elapsed: 0.137 s % 229.08/33.06 % (1615091)Peak memory usage: 91 MB % 229.08/33.06 % (1615091)Instructions burned: 259 (million) % 229.08/33.06 % (1615094)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=3129029384:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2712 on theBenchmark for (2712ds/570Mi) % 229.08/33.06 % (1615095)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=1005239467:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2711 on theBenchmark for (2711ds/314Mi) % 229.08/33.06 % (1615095)Refutation not found, incomplete strategy % 229.08/33.06 % (1615095)------------------------------ % 229.08/33.06 % (1615095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.08/33.06 % (1615095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.08/33.06 % (1615095)CaDiCaL version: 2.1.3 % 229.08/33.06 % (1615095)Termination reason: Refutation not found, incomplete strategy % 229.08/33.06 % (1615095)Time elapsed: 0.003 s % 229.08/33.06 % (1615095)Peak memory usage: 88 MB % 229.08/33.06 % (1615095)Instructions burned: 2 (million) % 229.08/33.06 % (1615095)------------------------------ % 229.08/33.06 % (1615095)------------------------------ % 229.08/33.06 % (1615094)Instruction limit reached! % 229.08/33.06 % (1615094)------------------------------ % 229.08/33.06 % (1615094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.08/33.06 % (1615094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.08/33.06 % (1615094)CaDiCaL version: 2.1.3 % 229.08/33.06 % (1615094)Termination reason: Instruction limit % 229.08/33.06 % (1615094)Termination phase: Saturation % 229.08/33.06 % (1615094)Time elapsed: 0.328 s % 229.08/33.06 % (1615094)Peak memory usage: 91 MB % 229.08/33.06 % (1615094)Instructions burned: 570 (million) % 229.08/33.06 % (1615201)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=1011440204:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2707 on theBenchmark for (2707ds/650Mi) % 229.08/33.06 % (1615201)Refutation not found, incomplete strategy % 229.08/33.06 % (1615201)------------------------------ % 229.08/33.06 % (1615201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.08/33.06 % (1615201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.08/33.06 % (1615201)CaDiCaL version: 2.1.3 % 229.08/33.06 % (1615201)Termination reason: Refutation not found, incomplete strategy % 229.08/33.06 % (1615201)Time elapsed: 0.004 s % 229.08/33.06 % (1615201)Peak memory usage: 88 MB % 229.08/33.06 % (1615201)Instructions burned: 2 (million) % 229.08/33.06 % (1615209)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=809407875:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2707 on theBenchmark for (2707ds/496Mi) % 229.08/33.06 % (1615201)------------------------------ % 229.08/33.06 % (1615201)------------------------------ % 229.08/33.06 % (1615209)Instruction limit reached! % 229.08/33.06 % (1615209)------------------------------ % 229.08/33.06 % (1615209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.08/33.06 % (1615209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.08/33.06 % (1615209)CaDiCaL version: 2.1.3 % 229.08/33.06 % (1615209)Termination reason: Instruction limit % 229.08/33.06 % (1615209)Termination phase: Saturation % 229.08/33.06 % (1615209)Time elapsed: 0.247 s % 229.08/33.06 % (1615209)Peak memory usage: 93 MB % 229.08/33.06 % (1615209)Instructions burned: 496 (million) % 229.08/33.06 % (1615276)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=2684364931:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2703 on theBenchmark for (2703ds/588Mi) % 229.08/33.06 % (1615276)Refutation not found, incomplete strategy % 229.08/33.06 % (1615276)------------------------------ % 233.30/33.63 % (1615276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.30/33.63 % (1615276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.30/33.63 % (1615276)CaDiCaL version: 2.1.3 % 233.30/33.63 % (1615276)Termination reason: Refutation not found, incomplete strategy % 233.30/33.63 % (1615276)Time elapsed: 0.005 s % 233.30/33.63 % (1615276)Peak memory usage: 88 MB % 233.30/33.63 % (1615276)Instructions burned: 6 (million) % 233.30/33.63 % (1615288)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=2471990030:i=4700:rtra=on_2703 on theBenchmark for (2703ds/4700Mi) % 233.30/33.63 % (1615276)------------------------------ % 233.30/33.63 % (1615276)------------------------------ % 233.30/33.63 % Exception at run slice level % 233.30/33.63 User error: GNN currently only supports monomorphic FOL. % 233.30/33.63 % (1615291)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4213281418:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2699 on theBenchmark for (2699ds/226Mi) % 233.30/33.63 % (1615291)Refutation not found, incomplete strategy % 233.30/33.63 % (1615291)------------------------------ % 233.30/33.63 % (1615291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.30/33.63 % (1615291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.30/33.63 % (1615291)CaDiCaL version: 2.1.3 % 233.30/33.63 % (1615291)Termination reason: Refutation not found, incomplete strategy % 233.30/33.63 % (1615291)Time elapsed: 0.007 s % 233.30/33.63 % (1615291)Peak memory usage: 89 MB % 233.30/33.63 % (1615291)Instructions burned: 10 (million) % 233.30/33.63 % (1615292)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=813707285:i=254:av=off:fsr=off:rtra=on:sup=off_2698 on theBenchmark for (2698ds/254Mi) % 233.30/33.63 % (1615292)Instruction limit reached! % 233.30/33.63 % (1615292)------------------------------ % 233.30/33.63 % (1615292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.30/33.63 % (1615292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.30/33.63 % (1615292)CaDiCaL version: 2.1.3 % 233.30/33.63 % (1615292)Termination reason: Instruction limit % 233.30/33.63 % (1615292)Termination phase: Saturation % 233.30/33.63 % (1615292)Time elapsed: 0.110 s % 233.30/33.63 % (1615292)Peak memory usage: 89 MB % 233.30/33.63 % (1615292)Instructions burned: 256 (million) % 233.30/33.63 % (1615291)------------------------------ % 233.30/33.63 % (1615291)------------------------------ % 233.30/33.63 % (1615295)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=4072499975:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2696 on theBenchmark for (2696ds/228Mi) % 233.30/33.63 % (1615296)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=1237215141:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2695 on theBenchmark for (2695ds/1814Mi) % 233.30/33.63 % (1615295)Refutation not found, incomplete strategy % 233.30/33.63 % (1615295)------------------------------ % 233.30/33.63 % (1615295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.30/33.63 % (1615295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.30/33.63 % (1615295)CaDiCaL version: 2.1.3 % 233.30/33.63 % (1615295)Termination reason: Refutation not found, incomplete strategy % 233.30/33.63 % (1615295)Time elapsed: 0.006 s % 233.30/33.63 % (1615295)Peak memory usage: 89 MB % 233.30/33.63 % (1615295)Instructions burned: 8 (million) % 233.30/33.63 % (1615295)------------------------------ % 233.30/33.63 % (1615295)------------------------------ % 233.30/33.63 % (1615299)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=884710290:i=874:sd=1:aac=none:rtra=on:ss=included_2692 on theBenchmark for (2692ds/874Mi) % 233.30/33.63 % (1615299)Refutation not found, incomplete strategy % 233.30/33.63 % (1615299)------------------------------ % 233.30/33.63 % (1615299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.30/33.63 % (1615299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.30/33.63 % (1615299)CaDiCaL version: 2.1.3 % 233.30/33.63 % (1615299)Termination reason: Refutation not found, incomplete strategy % 233.30/33.63 % (1615299)Time elapsed: 0.007 s % 233.30/33.63 % (1615299)Peak memory usage: 88 MB % 233.30/33.63 % (1615299)Instructions burned: 11 (million) % 233.30/33.63 % (1615299)------------------------------ % 233.30/33.63 % (1615299)------------------------------ % 233.30/33.63 % (1615316)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=1466867506:i=10404:rtra=on:ss=axioms:sgt=16_2688 on theBenchmark for (2688ds/10404Mi) % 239.22/34.49 % (1615296)Instruction limit reached! % 239.22/34.49 % (1615296)------------------------------ % 239.22/34.49 % (1615296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.22/34.49 % (1615296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.22/34.49 % (1615296)CaDiCaL version: 2.1.3 % 239.22/34.49 % (1615296)Termination reason: Instruction limit % 239.22/34.49 % (1615296)Termination phase: Saturation % 239.22/34.49 % (1615296)Time elapsed: 1.007 s % 239.22/34.49 % (1615296)Peak memory usage: 95 MB % 239.22/34.49 % (1615296)Instructions burned: 1814 (million) % 239.22/34.49 % Exception at run slice level % 239.22/34.49 User error: GNN currently only supports monomorphic FOL. % 239.22/34.49 % (1615416)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2675111008:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2684 on theBenchmark for (2684ds/268Mi) % 239.22/34.49 % (1615417)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=3915624789:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2683 on theBenchmark for (2683ds/1184Mi) % 239.22/34.49 % (1615417)Refutation not found, incomplete strategy % 239.22/34.49 % (1615417)------------------------------ % 239.22/34.49 % (1615417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.22/34.49 % (1615417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.22/34.49 % (1615417)CaDiCaL version: 2.1.3 % 239.22/34.49 % (1615417)Termination reason: Refutation not found, incomplete strategy % 239.22/34.49 % (1615417)Time elapsed: 0.007 s % 239.22/34.49 % (1615417)Peak memory usage: 88 MB % 239.22/34.49 % (1615417)Instructions burned: 11 (million) % 239.22/34.49 % (1615416)Instruction limit reached! % 239.22/34.49 % (1615416)------------------------------ % 239.22/34.49 % (1615416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.22/34.49 % (1615416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.22/34.49 % (1615416)CaDiCaL version: 2.1.3 % 239.22/34.49 % (1615416)Termination reason: Instruction limit % 239.22/34.49 % (1615416)Termination phase: Saturation % 239.22/34.49 % (1615416)Time elapsed: 0.158 s % 239.22/34.49 % (1615416)Peak memory usage: 91 MB % 239.22/34.49 % (1615416)Instructions burned: 269 (million) % 239.22/34.49 % (1615420)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=3717897898:st=3:i=26386:sd=3:rtra=on:ss=axioms_2681 on theBenchmark for (2681ds/26386Mi) % 239.22/34.49 % (1615417)------------------------------ % 239.22/34.49 % (1615417)------------------------------ % 239.22/34.49 % (1615422)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=1259805378:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2679 on theBenchmark for (2679ds/250Mi) % 239.22/34.49 % (1615422)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 239.22/34.49 % (1614932)Instruction limit reached! % 239.22/34.49 % (1614932)------------------------------ % 239.22/34.49 % (1614932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.22/34.49 % (1614932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.22/34.49 % (1614932)CaDiCaL version: 2.1.3 % 239.22/34.49 % (1614932)Termination reason: Instruction limit % 239.22/34.49 % (1614932)Termination phase: Saturation % 239.22/34.49 % (1614932)Time elapsed: 12.396 s % 239.22/34.49 % (1614932)Peak memory usage: 133 MB % 239.22/34.49 % (1614932)Instructions burned: 23714 (million) % 239.22/34.49 % (1615422)Instruction limit reached! % 239.22/34.49 % (1615422)------------------------------ % 239.22/34.49 % (1615422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.22/34.49 % (1615422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.22/34.49 % (1615422)CaDiCaL version: 2.1.3 % 239.22/34.49 % (1615422)Termination reason: Instruction limit % 239.22/34.49 % (1615422)Termination phase: Saturation % 239.22/34.49 % (1615422)Time elapsed: 0.163 s % 239.22/34.49 % (1615422)Peak memory usage: 91 MB % 239.22/34.49 % (1615422)Instructions burned: 250 (million) % 239.22/34.49 % Exception at run slice level % 239.22/34.49 User error: GNN currently only supports monomorphic FOL. % 239.22/34.49 % (1615424)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=3337155412:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2677 on theBenchmark for (2677ds/268Mi) % 239.22/34.49 % Exception at run slice level % 239.22/34.49 User error: Immediate (shared) subterms of term/literal aa(X1,fun(X1,X1),sF36(X0,X1,X4,X6,X5,X2),huffma1280178957ee_rec(X0,X1,X3,X4,X5)) = sF37(X1,X0,X4,X6,X5,X2,X3) have different types/not well-typed! % 250.87/36.13 % (1615425)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=307588909:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2676 on theBenchmark for (2676ds/282Mi) % 250.87/36.13 % (1615425)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 250.87/36.13 % (1615425)Refutation not found, incomplete strategy % 250.87/36.13 % (1615425)------------------------------ % 250.87/36.13 % (1615425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.87/36.13 % (1615425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.87/36.13 % (1615425)CaDiCaL version: 2.1.3 % 250.87/36.13 % (1615425)Termination reason: Refutation not found, incomplete strategy % 250.87/36.13 % (1615425)Time elapsed: 0.002 s % 250.87/36.13 % (1615425)Peak memory usage: 88 MB % 250.87/36.13 % (1615425)Instructions burned: 1 (million) % 250.87/36.13 % (1615426)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=1287967494:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2676 on theBenchmark for (2676ds/862Mi) % 250.87/36.13 % (1615428)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=617520115:i=12120:aac=none:ins=25:rtra=on_2676 on theBenchmark for (2676ds/12120Mi) % 250.87/36.13 % (1614515)Instruction limit reached! % 250.87/36.13 % (1614515)------------------------------ % 250.87/36.13 % (1614515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.87/36.13 % (1614515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.87/36.13 % (1614515)CaDiCaL version: 2.1.3 % 250.87/36.13 % (1614515)Termination reason: Instruction limit % 250.87/36.13 % (1614515)Termination phase: Saturation % 250.87/36.13 % (1614515)Time elapsed: 23.884 s % 250.87/36.13 % (1614515)Peak memory usage: 179 MB % 250.87/36.13 % (1614515)Instructions burned: 43699 (million) % 250.87/36.13 % (1615425)------------------------------ % 250.87/36.13 % (1615425)------------------------------ % 250.87/36.13 % (1615432)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=1241612416:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2674 on theBenchmark for (2674ds/300Mi) % 250.87/36.13 % (1615432)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 250.87/36.13 % (1615432)Instruction limit reached! % 250.87/36.13 % (1615432)------------------------------ % 250.87/36.13 % (1615432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.87/36.13 % (1615432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.87/36.13 % (1615432)CaDiCaL version: 2.1.3 % 250.87/36.13 % (1615432)Termination reason: Instruction limit % 250.87/36.13 % (1615432)Termination phase: Saturation % 250.87/36.13 % (1615432)Time elapsed: 0.120 s % 250.87/36.13 % (1615432)Peak memory usage: 91 MB % 250.87/36.13 % (1615432)Instructions burned: 303 (million) % 250.87/36.13 % (1615434)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=3059212092:i=28310:bd=all:rtra=on_2673 on theBenchmark for (2673ds/28310Mi) % 250.87/36.13 % Exception at run slice level % 250.87/36.13 User error: GNN currently only supports monomorphic FOL. % 250.87/36.13 % (1615426)Instruction limit reached! % 250.87/36.13 % (1615426)------------------------------ % 250.87/36.13 % (1615426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.87/36.13 % (1615426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.87/36.13 % (1615426)CaDiCaL version: 2.1.3 % 250.87/36.13 % (1615426)Termination reason: Instruction limit % 250.87/36.13 % (1615426)Termination phase: Saturation % 250.87/36.13 % (1615426)Time elapsed: 0.396 s % 250.87/36.13 % (1615426)Peak memory usage: 96 MB % 250.87/36.13 % (1615426)Instructions burned: 864 (million) % 250.87/36.13 % (1615435)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1466196738:i=1334:av=off:fsr=off:rtra=on_2672 on theBenchmark for (2672ds/1334Mi) % 250.87/36.13 % (1615435)Refutation not found, incomplete strategy % 250.87/36.13 % (1615435)------------------------------ % 250.87/36.13 % (1615435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.70/38.49 % (1615435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.70/38.49 % (1615435)CaDiCaL version: 2.1.3 % 267.70/38.49 % (1615435)Termination reason: Refutation not found, incomplete strategy % 267.70/38.49 % (1615435)Time elapsed: 0.007 s % 267.70/38.49 % (1615435)Peak memory usage: 89 MB % 267.70/38.49 % (1615435)Instructions burned: 9 (million) % 267.70/38.49 % (1615437)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=4243711870:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2671 on theBenchmark for (2671ds/370Mi) % 267.70/38.49 % (1615438)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=3941232790:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2671 on theBenchmark for (2671ds/386Mi) % 267.70/38.49 % (1615435)------------------------------ % 267.70/38.49 % (1615435)------------------------------ % 267.70/38.49 % Exception at run slice level % 267.70/38.49 User error: GNN currently only supports monomorphic FOL. % 267.70/38.49 % (1615437)Instruction limit reached! % 267.70/38.49 % (1615437)------------------------------ % 267.70/38.49 % (1615437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.70/38.49 % (1615437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.70/38.49 % (1615437)CaDiCaL version: 2.1.3 % 267.70/38.49 % (1615437)Termination reason: Instruction limit % 267.70/38.49 % (1615437)Termination phase: Saturation % 267.70/38.49 % (1615437)Time elapsed: 0.239 s % 267.70/38.49 % (1615437)Peak memory usage: 91 MB % 267.70/38.49 % (1615437)Instructions burned: 370 (million) % 267.70/38.49 % (1615438)Instruction limit reached! % 267.70/38.49 % (1615438)------------------------------ % 267.70/38.49 % (1615438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.70/38.49 % (1615438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.70/38.49 % (1615438)CaDiCaL version: 2.1.3 % 267.70/38.49 % (1615438)Termination reason: Instruction limit % 267.70/38.49 % (1615438)Termination phase: Saturation % 267.70/38.49 % (1615438)Time elapsed: 0.248 s % 267.70/38.49 % (1615438)Peak memory usage: 93 MB % 267.70/38.49 % (1615438)Instructions burned: 386 (million) % 267.70/38.49 % (1615442)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=1256953179:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2668 on theBenchmark for (2668ds/9700Mi) % 267.70/38.49 % (1615443)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=1337986218:i=24222:sd=1:rtra=on:ss=included_2668 on theBenchmark for (2668ds/24222Mi) % 267.70/38.49 % (1615444)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=2028898822:i=638:kws=precedence:fsr=off:rtra=on_2667 on theBenchmark for (2667ds/638Mi) % 267.70/38.49 % (1615445)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=589956541:i=4128:ep=RST:rtra=on_2667 on theBenchmark for (2667ds/4128Mi) % 267.70/38.49 % (1615445)Refutation not found, incomplete strategy % 267.70/38.49 % (1615445)------------------------------ % 267.70/38.49 % (1615445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.70/38.49 % (1615445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.70/38.49 % (1615445)CaDiCaL version: 2.1.3 % 267.70/38.49 % (1615445)Termination reason: Refutation not found, incomplete strategy % 267.70/38.49 % (1615445)Time elapsed: 0.007 s % 267.70/38.49 % (1615445)Peak memory usage: 88 MB % 267.70/38.49 % (1615445)Instructions burned: 11 (million) % 267.70/38.49 % (1615445)------------------------------ % 267.70/38.49 % (1615445)------------------------------ % 267.70/38.49 % Exception at run slice level % 267.70/38.49 User error: GNN currently only supports monomorphic FOL. % 267.70/38.49 % (1615450)dis-1011_128_sil=32000:si=on:random_seed=343546213:i=7412:ep=RST:av=off:rtra=on_2663 on theBenchmark for (2663ds/7412Mi) % 267.70/38.49 % (1615444)Instruction limit reached! % 267.70/38.49 % (1615444)------------------------------ % 267.70/38.49 % (1615444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.70/38.49 % (1615444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.70/38.49 % (1615444)CaDiCaL version: 2.1.3 % 267.70/38.49 % (1615444)Termination reason: Instruction limit % 267.70/38.49 % (1615444)Termination phase: Saturation % 267.70/38.49 % (1615444)Time elapsed: 0.381 s % 267.70/38.49 % (1615444)Peak memory usage: 94 MB % 267.70/38.49 % (1615444)Instructions burned: 638 (million) % 267.70/38.49 % (1615451)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3843069794:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2663 on theBenchmark for (2663ds/1514Mi) % 282.72/40.67 % (1615451)Refutation not found, incomplete strategy % 282.72/40.67 % (1615451)------------------------------ % 282.72/40.67 % (1615451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.72/40.67 % (1615451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.72/40.67 % (1615451)CaDiCaL version: 2.1.3 % 282.72/40.67 % (1615451)Termination reason: Refutation not found, incomplete strategy % 282.72/40.67 % (1615451)Time elapsed: 0.006 s % 282.72/40.67 % (1615451)Peak memory usage: 89 MB % 282.72/40.67 % (1615451)Instructions burned: 8 (million) % 282.72/40.67 % (1615453)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=3895665354:i=27826:rtra=on:ss=axioms:sgt=8_2662 on theBenchmark for (2662ds/27826Mi) % 282.72/40.67 % (1615451)------------------------------ % 282.72/40.67 % (1615451)------------------------------ % 282.72/40.67 % (1615456)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=2801437702:i=19850:aac=none:rtra=on_2659 on theBenchmark for (2659ds/19850Mi) % 282.72/40.67 % Exception at run slice level % 282.72/40.67 User error: GNN currently only supports monomorphic FOL. % 282.72/40.67 % (1615458)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3811587713:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2657 on theBenchmark for (2657ds/4958Mi) % 282.72/40.67 % (1615458)Refutation not found, incomplete strategy % 282.72/40.67 % (1615458)------------------------------ % 282.72/40.67 % (1615458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.72/40.67 % (1615458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.72/40.67 % (1615458)CaDiCaL version: 2.1.3 % 282.72/40.67 % (1615458)Termination reason: Refutation not found, incomplete strategy % 282.72/40.67 % (1615458)Time elapsed: 0.003 s % 282.72/40.67 % (1615458)Peak memory usage: 88 MB % 282.72/40.67 % (1615458)Instructions burned: 2 (million) % 282.72/40.67 % Exception at run slice level % 282.72/40.67 User error: GNN currently only supports monomorphic FOL. % 282.72/40.67 % (1615458)------------------------------ % 282.72/40.67 % (1615458)------------------------------ % 282.72/40.67 % (1615460)ott+1002_64_sil=16000:si=on:sp=const_min:nwc=0.5:random_seed=101963286:i=880:nm=2:av=off:rtra=on:gtg=exists_all:fdi=8:gsp=on_2654 on theBenchmark for (2654ds/880Mi) % 282.72/40.67 % (1615460)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 282.72/40.67 % (1615461)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=1608065940:st=1.5:i=22290:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2654 on theBenchmark for (2654ds/22290Mi) % 282.72/40.67 % Exception at run slice level % 282.72/40.67 User error: GNN currently only supports monomorphic FOL. % 282.72/40.67 % (1615460)Instruction limit reached! % 282.72/40.67 % (1615460)------------------------------ % 282.72/40.67 % (1615460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.72/40.67 % (1615460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.72/40.67 % (1615460)CaDiCaL version: 2.1.3 % 282.72/40.67 % (1615460)Termination reason: Instruction limit % 282.72/40.67 % (1615460)Termination phase: Saturation % 282.72/40.67 % (1615460)Time elapsed: 0.510 s % 282.72/40.67 % (1615460)Peak memory usage: 91 MB % 282.72/40.67 % (1615460)Instructions burned: 881 (million) % 282.72/40.67 % (1615464)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=1117964590:cts=off:i=6068:av=off:rtra=on:er=known:fsd=on_2649 on theBenchmark for (2649ds/6068Mi) % 282.72/40.67 % (1615465)lrs-1011_64:1_sil=8000:si=on:erd=off:urr=on:nwc=0.7:br=off:random_seed=3694314422:st=2:s2a=on:i=1048:s2at=2:rtra=on:ss=axioms_2648 on theBenchmark for (2648ds/1048Mi) % 282.72/40.67 % (1614936)Instruction limit reached! % 282.72/40.67 % (1614936)------------------------------ % 282.72/40.67 % (1614936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.72/40.67 % (1614936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.72/40.67 % (1614936)CaDiCaL version: 2.1.3 % 282.72/40.67 % (1614936)Termination reason: Instruction limit % 282.72/40.67 % (1614936)Termination phase: Saturation % 282.72/40.67 % (1614936)Time elapsed: 14.551 s % 295.17/42.38 % (1614936)Peak memory usage: 161 MB % 295.17/42.38 % (1614936)Instructions burned: 28958 (million) % 295.17/42.38 % (1615468)lrs+1011_16:1_sil=8000:si=on:acc=on:urr=on:fd=preordered:flr=on:random_seed=21214818:avsq=on:i=2032:avsqr=676809,524288:sd=1:rtra=on:ss=axioms_2645 on theBenchmark for (2645ds/2032Mi) % 295.17/42.38 % Exception at run slice level % 295.17/42.38 User error: GNN currently only supports monomorphic FOL. % 295.17/42.38 % (1615468)Refutation not found, incomplete strategy % 295.17/42.38 % (1615468)------------------------------ % 295.17/42.38 % (1615468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.17/42.38 % (1615468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.17/42.38 % (1615468)CaDiCaL version: 2.1.3 % 295.17/42.38 % (1615468)Termination reason: Refutation not found, incomplete strategy % 295.17/42.38 % (1615468)Time elapsed: 0.002 s % 295.17/42.38 % (1615468)Peak memory usage: 89 MB % 295.17/42.38 % (1615468)Instructions burned: 2 (million) % 295.17/42.38 % (1615470)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:si=on:s2agt=16:random_seed=234680391:i=28246:bd=preordered:ins=4:rtra=on_2644 on theBenchmark for (2644ds/28246Mi) % 295.17/42.38 % (1615465)Instruction limit reached! % 295.17/42.38 % (1615465)------------------------------ % 295.17/42.38 % (1615465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.17/42.38 % (1615465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.17/42.38 % (1615465)CaDiCaL version: 2.1.3 % 295.17/42.38 % (1615465)Termination reason: Instruction limit % 295.17/42.38 % (1615465)Termination phase: Saturation % 295.17/42.38 % (1615465)Time elapsed: 0.466 s % 295.17/42.38 % (1615465)Peak memory usage: 90 MB % 295.17/42.38 % (1615465)Instructions burned: 1049 (million) % 295.17/42.38 % (1615468)------------------------------ % 295.17/42.38 % (1615468)------------------------------ % 295.17/42.38 % (1615472)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:si=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=4136081764:i=11562:kws=precedence:bd=all:rtra=on:rawr=on_2642 on theBenchmark for (2642ds/11562Mi) % 295.17/42.38 % (1615473)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=645327088:i=4896:gtgl=5:bd=preordered:rtra=on:gtg=all_2641 on theBenchmark for (2641ds/4896Mi) % 295.17/42.38 % Exception at run slice level % 295.17/42.38 User error: GNN currently only supports monomorphic FOL. % 295.17/42.38 % (1615476)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:si=on:lcm=reverse:random_seed=4222277501:i=6446:kws=precedence:fgj=on:av=off:rtra=on_2639 on theBenchmark for (2639ds/6446Mi) % 295.17/42.38 % Exception at run slice level % 295.17/42.38 User error: GNN currently only supports monomorphic FOL. % 295.17/42.38 % (1615478)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:si=on:sp=occurrence:sos=on:random_seed=2972673762:st=5.6:i=4066:sd=3:rtra=on:ss=axioms_2636 on theBenchmark for (2636ds/4066Mi) % 295.17/42.38 % Exception at run slice level % 295.17/42.38 User error: GNN currently only supports monomorphic FOL. % 295.17/42.38 % (1615480)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:si=on:random_seed=2353823156:i=4110:nm=16:rtra=on:gtg=position:ss=axioms:fsd=on_2634 on theBenchmark for (2634ds/4110Mi) % 295.17/42.38 % Exception at run slice level % 295.17/42.38 User error: GNN currently only supports monomorphic FOL. % 295.17/42.38 % (1615482)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=1473164746:i=43222:sd=3:rtra=on:ss=axioms_2632 on theBenchmark for (2632ds/43222Mi) % 295.17/42.38 % Exception at run slice level % 295.17/42.38 User error: GNN currently only supports monomorphic FOL. % 295.17/42.38 % (1615484)lrs+10_1_sil=8000:si=on:sp=occurrence:sos=all:lma=off:random_seed=3425943362:i=9670:sd=13:rtra=on:ss=axioms:sgt=23_2629 on theBenchmark for (2629ds/9670Mi) % 295.17/42.38 % Exception at run slice level % 295.17/42.38 User error: GNN currently only supports monomorphic FOL. % 295.17/42.38 % (1615486)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=1797160133:st=5:i=1594:s2at=3:sd=4:bs=unit_only:av=off:rtra=on:sup=off:ss=included_2627 on theBenchmark for (2627ds/1594Mi) % 295.17/42.38 % (1615450)Instruction limit reached! % 295.17/42.38 % (1615450)------------------------------ % 295.17/42.38 % (1615450)Version: Vampire 5.0.1 (RTerminated %------------------------------------------------------------------------------