%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW936+1 : TPTP v9.3.1. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:38:03 PM UTC 2026 % Result : Timeout 293.38s 42.22s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWW936+1 : TPTP v9.3.1. Released v7.3.0. % 0.00/0.02 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.06/0.11 % Computer : n012.cluster.edu % 0.06/0.11 % Model : x86_64 x86_64 % 0.06/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.11 % Memory : 8046.5625MB % 0.06/0.11 % OS : Linux 6.8.0-71-generic % 0.06/0.11 % CPULimit : 300 % 0.06/0.11 % WCLimit : 300 % 0.06/0.11 % DateTime : Mon Sep 28 14:45:08 UTC 2026 % 0.06/0.12 % CPUTime : % 0.06/0.12 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.06/0.13 Running first-order theorem proving % 0.06/0.13 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 6.94/1.43 % (3428311)Detected formulas, will run a generic FOF schedule. % 6.94/1.43 % (3428322)dis-21_1_sil=8000:lcm=predicate:random_seed=2585640104: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.94/1.43 % (3428321)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3533798043:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 6.94/1.43 % (3428317)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=2584967983:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 6.94/1.43 % (3428319)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1175977303:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 6.94/1.43 % (3428316)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=3885020830:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 6.94/1.43 % (3428320)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2588790630:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 6.94/1.43 % (3428318)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=3979148093:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 6.94/1.43 % (3428319)Refutation not found, incomplete strategy % 6.94/1.43 % (3428319)------------------------------ % 6.94/1.43 % (3428319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.94/1.43 % (3428319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.94/1.43 % (3428319)CaDiCaL version: 2.1.3 % 6.94/1.43 % (3428319)Termination reason: Refutation not found, incomplete strategy % 6.94/1.43 % (3428319)Time elapsed: 0.001 s % 6.94/1.43 % (3428319)Peak memory usage: 88 MB % 6.94/1.43 % (3428322)Refutation not found, incomplete strategy % 6.94/1.43 % (3428322)------------------------------ % 6.94/1.43 % (3428322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.94/1.43 % (3428322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.94/1.43 % (3428322)CaDiCaL version: 2.1.3 % 6.94/1.43 % (3428322)Termination reason: Refutation not found, incomplete strategy % 6.94/1.43 % (3428322)Time elapsed: 0.001 s % 6.94/1.43 % (3428322)Peak memory usage: 88 MB % 6.94/1.43 % (3428322)Instructions burned: 3 (million) % 6.94/1.43 % (3428320)Instruction limit reached! % 6.94/1.43 % (3428320)------------------------------ % 6.94/1.43 % (3428320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.94/1.43 % (3428320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.94/1.43 % (3428320)CaDiCaL version: 2.1.3 % 6.94/1.43 % (3428320)Termination reason: Instruction limit % 6.94/1.43 % (3428320)Termination phase: Saturation % 6.94/1.43 % (3428320)Time elapsed: 0.031 s % 6.94/1.43 % (3428320)Peak memory usage: 87 MB % 6.94/1.43 % (3428320)Instructions burned: 120 (million) % 6.94/1.43 % (3428321)Instruction limit reached! % 6.94/1.43 % (3428321)------------------------------ % 6.94/1.43 % (3428321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.94/1.43 % (3428321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.94/1.43 % (3428321)CaDiCaL version: 2.1.3 % 6.94/1.43 % (3428321)Termination reason: Instruction limit % 6.94/1.43 % (3428321)Termination phase: Saturation % 6.94/1.43 % (3428321)Time elapsed: 0.042 s % 6.94/1.43 % (3428321)Peak memory usage: 89 MB % 6.94/1.43 % (3428321)Instructions burned: 141 (million) % 6.94/1.43 % (3428330)lrs+10_1_sil=8000:sp=occurrence:random_seed=3128732462:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi) % 6.94/1.43 % (3428331)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3115256028:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi) % 6.94/1.43 % (3428319)------------------------------ % 6.94/1.43 % (3428319)------------------------------ % 6.94/1.43 % (3428322)------------------------------ % 6.94/1.43 % (3428322)------------------------------ % 6.94/1.43 % (3428331)Instruction limit reached! % 6.94/1.43 % (3428331)------------------------------ % 6.94/1.43 % (3428331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.94/1.43 % (3428331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.75/1.91 % (3428331)CaDiCaL version: 2.1.3 % 9.75/1.91 % (3428331)Termination reason: Instruction limit % 9.75/1.91 % (3428331)Termination phase: Saturation % 9.75/1.91 % (3428331)Time elapsed: 0.046 s % 9.75/1.91 % (3428331)Peak memory usage: 90 MB % 9.75/1.91 % (3428331)Instructions burned: 160 (million) % 9.75/1.91 % (3428330)Instruction limit reached! % 9.75/1.91 % (3428330)------------------------------ % 9.75/1.91 % (3428330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.75/1.91 % (3428330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.75/1.91 % (3428330)CaDiCaL version: 2.1.3 % 9.75/1.91 % (3428330)Termination reason: Instruction limit % 9.75/1.91 % (3428330)Termination phase: Saturation % 9.75/1.91 % (3428330)Time elapsed: 0.077 s % 9.75/1.91 % (3428330)Peak memory usage: 90 MB % 9.75/1.91 % (3428330)Instructions burned: 288 (million) % 9.75/1.91 % (3428335)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=2631339899:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 9.75/1.91 % (3428334)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3384443942:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 9.75/1.91 % (3428336)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3241734084:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2997 on theBenchmark for (2997ds/294Mi) % 9.75/1.91 % (3428336)Refutation not found, incomplete strategy % 9.75/1.91 % (3428336)------------------------------ % 9.75/1.91 % (3428336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.75/1.91 % (3428336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.75/1.91 % (3428336)CaDiCaL version: 2.1.3 % 9.75/1.91 % (3428336)Termination reason: Refutation not found, incomplete strategy % 9.75/1.91 % (3428336)Time elapsed: 0.002 s % 9.75/1.91 % (3428336)Peak memory usage: 88 MB % 9.75/1.91 % (3428336)Instructions burned: 4 (million) % 9.75/1.91 % (3428337)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1913295640:i=2350_2996 on theBenchmark for (2996ds/2350Mi) % 9.75/1.91 % (3428335)Instruction limit reached! % 9.75/1.91 % (3428335)------------------------------ % 9.75/1.91 % (3428335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.75/1.91 % (3428335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.75/1.91 % (3428335)CaDiCaL version: 2.1.3 % 9.75/1.91 % (3428335)Termination reason: Instruction limit % 9.75/1.91 % (3428335)Termination phase: Saturation % 9.75/1.91 % (3428335)Time elapsed: 0.074 s % 9.75/1.91 % (3428335)Peak memory usage: 91 MB % 9.75/1.91 % (3428335)Instructions burned: 251 (million) % 9.75/1.91 % (3428334)Instruction limit reached! % 9.75/1.91 % (3428334)------------------------------ % 9.75/1.91 % (3428334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.75/1.91 % (3428334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.75/1.91 % (3428334)CaDiCaL version: 2.1.3 % 9.75/1.91 % (3428334)Termination reason: Instruction limit % 9.75/1.91 % (3428334)Termination phase: Saturation % 9.75/1.91 % (3428334)Time elapsed: 0.092 s % 9.75/1.91 % (3428334)Peak memory usage: 90 MB % 9.75/1.91 % (3428334)Instructions burned: 328 (million) % 9.75/1.91 % (3428342)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1436694749:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi) % 9.75/1.91 % (3428336)------------------------------ % 9.75/1.91 % (3428336)------------------------------ % 9.75/1.91 % (3428343)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=455620476:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi) % 9.75/1.91 % (3428342)Instruction limit reached! % 9.75/1.91 % (3428342)------------------------------ % 9.75/1.91 % (3428342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.75/1.91 % (3428342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.75/1.91 % (3428342)CaDiCaL version: 2.1.3 % 9.75/1.91 % (3428342)Termination reason: Instruction limit % 9.75/1.91 % (3428342)Termination phase: Saturation % 9.75/1.91 % (3428342)Time elapsed: 0.031 s % 9.75/1.91 % (3428342)Peak memory usage: 88 MB % 9.75/1.91 % (3428342)Instructions burned: 115 (million) % 9.75/1.91 % (3428343)Refutation not found, incomplete strategy % 9.75/1.91 % (3428343)------------------------------ % 9.75/1.91 % (3428343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.97/3.33 % (3428343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.97/3.33 % (3428343)CaDiCaL version: 2.1.3 % 20.97/3.33 % (3428343)Termination reason: Refutation not found, incomplete strategy % 20.97/3.33 % (3428343)Time elapsed: 0.001 s % 20.97/3.33 % (3428343)Peak memory usage: 88 MB % 20.97/3.33 % (3428343)Instructions burned: 2 (million) % 20.97/3.33 % (3428345)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=404979166:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 20.97/3.33 % (3428347)lrs+10_1_sil=8000:sp=occurrence:random_seed=3678941123:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 20.97/3.33 % (3428345)Instruction limit reached! % 20.97/3.33 % (3428345)------------------------------ % 20.97/3.33 % (3428345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.97/3.33 % (3428345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.97/3.33 % (3428345)CaDiCaL version: 2.1.3 % 20.97/3.33 % (3428345)Termination reason: Instruction limit % 20.97/3.33 % (3428345)Termination phase: Saturation % 20.97/3.33 % (3428345)Time elapsed: 0.035 s % 20.97/3.33 % (3428345)Peak memory usage: 89 MB % 20.97/3.33 % (3428345)Instructions burned: 117 (million) % 20.97/3.33 % (3428343)------------------------------ % 20.97/3.33 % (3428343)------------------------------ % 20.97/3.33 % (3428350)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4041687756:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi) % 20.97/3.33 % (3428350)Refutation not found, incomplete strategy % 20.97/3.33 % (3428350)------------------------------ % 20.97/3.33 % (3428350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.97/3.33 % (3428350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.97/3.33 % (3428350)CaDiCaL version: 2.1.3 % 20.97/3.33 % (3428350)Termination reason: Refutation not found, incomplete strategy % 20.97/3.33 % (3428350)Time elapsed: 0.002 s % 20.97/3.33 % (3428350)Peak memory usage: 88 MB % 20.97/3.33 % (3428350)Instructions burned: 3 (million) % 20.97/3.33 % (3428351)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1516669830:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi) % 20.97/3.33 % (3428347)Instruction limit reached! % 20.97/3.33 % (3428347)------------------------------ % 20.97/3.33 % (3428347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.97/3.33 % (3428347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.97/3.33 % (3428347)CaDiCaL version: 2.1.3 % 20.97/3.33 % (3428347)Termination reason: Instruction limit % 20.97/3.33 % (3428347)Termination phase: Saturation % 20.97/3.33 % (3428347)Time elapsed: 0.220 s % 20.97/3.33 % (3428347)Peak memory usage: 90 MB % 20.97/3.33 % (3428347)Instructions burned: 909 (million) % 20.97/3.33 % (3428350)------------------------------ % 20.97/3.33 % (3428350)------------------------------ % 20.97/3.33 % (3428354)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2969236178:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2991 on theBenchmark for (2991ds/134Mi) % 20.97/3.33 % (3428354)Refutation not found, incomplete strategy % 20.97/3.33 % (3428354)------------------------------ % 20.97/3.33 % (3428354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.97/3.33 % (3428354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.97/3.33 % (3428354)CaDiCaL version: 2.1.3 % 20.97/3.33 % (3428354)Termination reason: Refutation not found, incomplete strategy % 20.97/3.33 % (3428354)Time elapsed: 0.002 s % 20.97/3.33 % (3428354)Peak memory usage: 89 MB % 20.97/3.33 % (3428354)Instructions burned: 3 (million) % 20.97/3.33 % (3428355)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=527615862:st=8:i=592:sd=3:ep=RST:ss=axioms_2990 on theBenchmark for (2990ds/592Mi) % 20.97/3.33 % (3428354)------------------------------ % 20.97/3.33 % (3428354)------------------------------ % 20.97/3.33 % (3428337)Instruction limit reached! % 20.97/3.33 % (3428337)------------------------------ % 20.97/3.33 % (3428337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.97/3.33 % (3428337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.97/3.33 % (3428337)CaDiCaL version: 2.1.3 % 20.97/3.33 % (3428337)Termination reason: Instruction limit % 20.97/3.33 % (3428337)Termination phase: Saturation % 20.97/3.33 % (3428337)Time elapsed: 0.707 s % 20.97/3.33 % (3428337)Peak memory usage: 134 MB % 33.83/5.19 % (3428337)Instructions burned: 2354 (million) % 33.83/5.19 % (3428355)Instruction limit reached! % 33.83/5.19 % (3428355)------------------------------ % 33.83/5.19 % (3428355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.83/5.19 % (3428355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.83/5.19 % (3428355)CaDiCaL version: 2.1.3 % 33.83/5.19 % (3428355)Termination reason: Instruction limit % 33.83/5.19 % (3428355)Termination phase: Saturation % 33.83/5.19 % (3428355)Time elapsed: 0.137 s % 33.83/5.19 % (3428355)Peak memory usage: 89 MB % 33.83/5.19 % (3428355)Instructions burned: 593 (million) % 33.83/5.19 % (3428358)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1751331436:st=3:i=13193:sd=3:ss=axioms_2988 on theBenchmark for (2988ds/13193Mi) % 33.83/5.19 % (3428359)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=2071968485:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/125Mi) % 33.83/5.19 % (3428360)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4107072059:i=134:gtgl=5:slsql=off:gtg=exists_sym_2988 on theBenchmark for (2988ds/134Mi) % 33.83/5.19 % (3428359)Instruction limit reached! % 33.83/5.19 % (3428359)------------------------------ % 33.83/5.19 % (3428359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.83/5.19 % (3428359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.83/5.19 % (3428359)CaDiCaL version: 2.1.3 % 33.83/5.19 % (3428359)Termination reason: Instruction limit % 33.83/5.19 % (3428359)Termination phase: Saturation % 33.83/5.19 % (3428359)Time elapsed: 0.043 s % 33.83/5.19 % (3428359)Peak memory usage: 91 MB % 33.83/5.19 % (3428359)Instructions burned: 127 (million) % 33.83/5.19 % (3428360)Instruction limit reached! % 33.83/5.19 % (3428360)------------------------------ % 33.83/5.19 % (3428360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.83/5.19 % (3428360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.83/5.19 % (3428360)CaDiCaL version: 2.1.3 % 33.83/5.19 % (3428360)Termination reason: Instruction limit % 33.83/5.19 % (3428360)Termination phase: Saturation % 33.83/5.19 % (3428360)Time elapsed: 0.039 s % 33.83/5.19 % (3428360)Peak memory usage: 90 MB % 33.83/5.19 % (3428360)Instructions burned: 136 (million) % 33.83/5.19 % (3428364)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2535122010:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/141Mi) % 33.83/5.19 % (3428365)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4093781235:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2987 on theBenchmark for (2987ds/431Mi) % 33.83/5.19 % (3428364)Refutation not found, incomplete strategy % 33.83/5.19 % (3428364)------------------------------ % 33.83/5.19 % (3428364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.83/5.19 % (3428364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.83/5.19 % (3428364)CaDiCaL version: 2.1.3 % 33.83/5.19 % (3428364)Termination reason: Refutation not found, incomplete strategy % 33.83/5.19 % (3428364)Time elapsed: 0.001 s % 33.83/5.19 % (3428364)Peak memory usage: 88 MB % 33.83/5.19 % (3428364)Instructions burned: 2 (million) % 33.83/5.19 % (3428365)Refutation not found, incomplete strategy % 33.83/5.19 % (3428365)------------------------------ % 33.83/5.19 % (3428365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.83/5.19 % (3428365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.83/5.19 % (3428365)CaDiCaL version: 2.1.3 % 33.83/5.19 % (3428365)Termination reason: Refutation not found, incomplete strategy % 33.83/5.19 % (3428365)Time elapsed: 0.001 s % 33.83/5.19 % (3428365)Peak memory usage: 88 MB % 33.83/5.19 % (3428365)Instructions burned: 2 (million) % 33.83/5.19 % (3428365)------------------------------ % 33.83/5.19 % (3428365)------------------------------ % 33.83/5.19 % (3428364)------------------------------ % 33.83/5.19 % (3428364)------------------------------ % 33.83/5.19 % (3428369)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=2368101831:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2984 on theBenchmark for (2984ds/150Mi) % 33.83/5.19 % (3428368)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=987216788:i=6060:aac=none:ins=25_2985 on theBenchmark for (2985ds/6060Mi) % 47.93/7.15 % (3428369)Instruction limit reached! % 47.93/7.15 % (3428369)------------------------------ % 47.93/7.15 % (3428369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.93/7.15 % (3428369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.93/7.15 % (3428369)CaDiCaL version: 2.1.3 % 47.93/7.15 % (3428369)Termination reason: Instruction limit % 47.93/7.15 % (3428369)Termination phase: Saturation % 47.93/7.15 % (3428369)Time elapsed: 0.034 s % 47.93/7.15 % (3428369)Peak memory usage: 88 MB % 47.93/7.15 % (3428369)Instructions burned: 154 (million) % 47.93/7.15 % (3428372)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1692813666:i=14155:bd=all_2983 on theBenchmark for (2983ds/14155Mi) % 47.93/7.15 % (3428351)Instruction limit reached! % 47.93/7.15 % (3428351)------------------------------ % 47.93/7.15 % (3428351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.93/7.15 % (3428351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.93/7.15 % (3428351)CaDiCaL version: 2.1.3 % 47.93/7.15 % (3428351)Termination reason: Instruction limit % 47.93/7.15 % (3428351)Termination phase: Saturation % 47.93/7.15 % (3428351)Time elapsed: 1.514 s % 47.93/7.15 % (3428351)Peak memory usage: 168 MB % 47.93/7.15 % (3428351)Instructions burned: 5204 (million) % 47.93/7.15 % (3428374)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=662793744:i=667:av=off:fsr=off_2976 on theBenchmark for (2976ds/667Mi) % 47.93/7.15 % (3428374)Instruction limit reached! % 47.93/7.15 % (3428374)------------------------------ % 47.93/7.15 % (3428374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.93/7.15 % (3428374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.93/7.15 % (3428374)CaDiCaL version: 2.1.3 % 47.93/7.15 % (3428374)Termination reason: Instruction limit % 47.93/7.15 % (3428374)Termination phase: Saturation % 47.93/7.15 % (3428374)Time elapsed: 0.158 s % 47.93/7.15 % (3428374)Peak memory usage: 99 MB % 47.93/7.15 % (3428374)Instructions burned: 671 (million) % 47.93/7.15 % (3428376)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=224532206:s2a=on:i=185:s2at=1.8:fdi=4_2974 on theBenchmark for (2974ds/185Mi) % 47.93/7.15 % (3428376)Instruction limit reached! % 47.93/7.15 % (3428376)------------------------------ % 47.93/7.15 % (3428376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.93/7.15 % (3428376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.93/7.15 % (3428376)CaDiCaL version: 2.1.3 % 47.93/7.15 % (3428376)Termination reason: Instruction limit % 47.93/7.15 % (3428376)Termination phase: Saturation % 47.93/7.15 % (3428376)Time elapsed: 0.052 s % 47.93/7.15 % (3428376)Peak memory usage: 90 MB % 47.93/7.15 % (3428376)Instructions burned: 189 (million) % 47.93/7.15 % (3428378)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2070432032:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2972 on theBenchmark for (2972ds/193Mi) % 47.93/7.15 % (3428378)Instruction limit reached! % 47.93/7.15 % (3428378)------------------------------ % 47.93/7.15 % (3428378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.93/7.15 % (3428378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.93/7.15 % (3428378)CaDiCaL version: 2.1.3 % 47.93/7.15 % (3428378)Termination reason: Instruction limit % 47.93/7.15 % (3428378)Termination phase: Saturation % 47.93/7.15 % (3428378)Time elapsed: 0.056 s % 47.93/7.15 % (3428378)Peak memory usage: 89 MB % 47.93/7.15 % (3428378)Instructions burned: 196 (million) % 47.93/7.15 % (3428380)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2153835066:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2970 on theBenchmark for (2970ds/4850Mi) % 47.93/7.15 % (3428380)Refutation not found, incomplete strategy % 47.93/7.15 % (3428380)------------------------------ % 47.93/7.15 % (3428380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.93/7.15 % (3428380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.93/7.15 % (3428380)CaDiCaL version: 2.1.3 % 47.93/7.15 % (3428380)Termination reason: Refutation not found, incomplete strategy % 47.93/7.15 % (3428380)Time elapsed: 0.001 s % 62.58/9.21 % (3428380)Peak memory usage: 88 MB % 62.58/9.21 % (3428380)Instructions burned: 1 (million) % 62.58/9.21 % (3428380)------------------------------ % 62.58/9.21 % (3428380)------------------------------ % 62.58/9.21 % (3428382)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2847611831:i=12111:sd=1:ss=included_2968 on theBenchmark for (2968ds/12111Mi) % 62.58/9.21 % (3428368)Instruction limit reached! % 62.58/9.21 % (3428368)------------------------------ % 62.58/9.21 % (3428368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.58/9.21 % (3428368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.58/9.21 % (3428368)CaDiCaL version: 2.1.3 % 62.58/9.21 % (3428368)Termination reason: Instruction limit % 62.58/9.21 % (3428368)Termination phase: Saturation % 62.58/9.21 % (3428368)Time elapsed: 1.756 s % 62.58/9.21 % (3428368)Peak memory usage: 146 MB % 62.58/9.21 % (3428368)Instructions burned: 6062 (million) % 62.58/9.21 % (3428384)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3289352846:i=319:kws=precedence:fsr=off_2966 on theBenchmark for (2966ds/319Mi) % 62.58/9.21 % (3428384)Instruction limit reached! % 62.58/9.21 % (3428384)------------------------------ % 62.58/9.21 % (3428384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.58/9.21 % (3428384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.58/9.21 % (3428384)CaDiCaL version: 2.1.3 % 62.58/9.21 % (3428384)Termination reason: Instruction limit % 62.58/9.21 % (3428384)Termination phase: Saturation % 62.58/9.21 % (3428384)Time elapsed: 0.076 s % 62.58/9.21 % (3428384)Peak memory usage: 89 MB % 62.58/9.21 % (3428384)Instructions burned: 322 (million) % 62.58/9.21 % (3428386)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1749449878:i=2064:ep=RST_2964 on theBenchmark for (2964ds/2064Mi) % 62.58/9.21 % (3428386)Instruction limit reached! % 62.58/9.21 % (3428386)------------------------------ % 62.58/9.21 % (3428386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.58/9.21 % (3428386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.58/9.21 % (3428386)CaDiCaL version: 2.1.3 % 62.58/9.21 % (3428386)Termination reason: Instruction limit % 62.58/9.21 % (3428386)Termination phase: Saturation % 62.58/9.21 % (3428386)Time elapsed: 0.440 s % 62.58/9.21 % (3428386)Peak memory usage: 90 MB % 62.58/9.21 % (3428386)Instructions burned: 2068 (million) % 62.58/9.21 % (3428388)dis-1011_128_sil=32000:random_seed=1475534482:i=3706:ep=RST:av=off_2959 on theBenchmark for (2959ds/3706Mi) % 62.58/9.21 % (3428358)Instruction limit reached! % 62.58/9.21 % (3428358)------------------------------ % 62.58/9.21 % (3428358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.58/9.21 % (3428358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.58/9.21 % (3428358)CaDiCaL version: 2.1.3 % 62.58/9.21 % (3428358)Termination reason: Instruction limit % 62.58/9.21 % (3428358)Termination phase: Saturation % 62.58/9.21 % (3428358)Time elapsed: 3.334 s % 62.58/9.21 % (3428358)Peak memory usage: 143 MB % 62.58/9.21 % (3428358)Instructions burned: 13195 (million) % 62.58/9.21 % (3428390)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2474319259:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2954 on theBenchmark for (2954ds/757Mi) % 62.58/9.21 % (3428390)Instruction limit reached! % 62.58/9.21 % (3428390)------------------------------ % 62.58/9.21 % (3428390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.58/9.21 % (3428390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.58/9.21 % (3428390)CaDiCaL version: 2.1.3 % 62.58/9.21 % (3428390)Termination reason: Instruction limit % 62.58/9.21 % (3428390)Termination phase: Saturation % 62.58/9.21 % (3428390)Time elapsed: 0.194 s % 62.58/9.21 % (3428390)Peak memory usage: 106 MB % 62.58/9.21 % (3428390)Instructions burned: 757 (million) % 62.58/9.21 % (3428388)Instruction limit reached! % 62.58/9.21 % (3428388)------------------------------ % 62.58/9.21 % (3428388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.58/9.21 % (3428388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.58/9.21 % (3428388)CaDiCaL version: 2.1.3 % 62.58/9.21 % (3428388)Termination reason: Instruction limit % 62.58/9.21 % (3428388)Termination phase: Saturation % 62.58/9.21 % (3428388)Time elapsed: 0.716 s % 62.58/9.21 % (3428388)Peak memory usage: 89 MB % 62.58/9.21 % (3428388)Instructions burned: 3708 (million) % 69.07/10.19 % (3428392)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3652029385:i=13913:ss=axioms:sgt=8_2951 on theBenchmark for (2951ds/13913Mi) % 69.07/10.19 % (3428393)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=814740520:i=9925:aac=none_2951 on theBenchmark for (2951ds/9925Mi) % 69.07/10.19 % (3428372)Instruction limit reached! % 69.07/10.19 % (3428372)------------------------------ % 69.07/10.19 % (3428372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.07/10.19 % (3428372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.07/10.19 % (3428372)CaDiCaL version: 2.1.3 % 69.07/10.19 % (3428372)Termination reason: Instruction limit % 69.07/10.19 % (3428372)Termination phase: Saturation % 69.07/10.19 % (3428372)Time elapsed: 3.703 s % 69.07/10.19 % (3428372)Peak memory usage: 152 MB % 69.07/10.19 % (3428372)Instructions burned: 14156 (million) % 69.07/10.19 % (3428396)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=864483099:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2945 on theBenchmark for (2945ds/2479Mi) % 69.07/10.19 % (3428396)Refutation not found, incomplete strategy % 69.07/10.19 % (3428396)------------------------------ % 69.07/10.19 % (3428396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.07/10.19 % (3428396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.07/10.19 % (3428396)CaDiCaL version: 2.1.3 % 69.07/10.19 % (3428396)Termination reason: Refutation not found, incomplete strategy % 69.07/10.19 % (3428396)Time elapsed: 0.001 s % 69.07/10.19 % (3428396)Peak memory usage: 88 MB % 69.07/10.19 % (3428396)------------------------------ % 69.07/10.19 % (3428396)------------------------------ % 69.07/10.19 % (3428398)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=534515687:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2943 on theBenchmark for (2943ds/440Mi) % 69.07/10.19 % (3428398)Instruction limit reached! % 69.07/10.19 % (3428398)------------------------------ % 69.07/10.19 % (3428398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.07/10.19 % (3428398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.07/10.19 % (3428398)CaDiCaL version: 2.1.3 % 69.07/10.19 % (3428398)Termination reason: Instruction limit % 69.07/10.19 % (3428398)Termination phase: Saturation % 69.07/10.19 % (3428398)Time elapsed: 0.109 s % 69.07/10.19 % (3428398)Peak memory usage: 93 MB % 69.07/10.19 % (3428398)Instructions burned: 442 (million) % 69.07/10.19 % (3428400)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1882952033:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2941 on theBenchmark for (2941ds/11145Mi) % 69.07/10.19 % (3428400)Refutation not found, incomplete strategy % 69.07/10.19 % (3428400)------------------------------ % 69.07/10.19 % (3428400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.07/10.19 % (3428400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.07/10.19 % (3428400)CaDiCaL version: 2.1.3 % 69.07/10.19 % (3428400)Termination reason: Refutation not found, incomplete strategy % 69.07/10.19 % (3428400)Time elapsed: 0.460 s % 69.07/10.19 % (3428400)Peak memory usage: 131 MB % 69.07/10.19 % (3428400)Instructions burned: 1304 (million) % 69.07/10.19 % (3428382)Instruction limit reached! % 69.07/10.19 % (3428382)------------------------------ % 69.07/10.19 % (3428382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.07/10.19 % (3428382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.07/10.19 % (3428382)CaDiCaL version: 2.1.3 % 69.07/10.19 % (3428382)Termination reason: Instruction limit % 69.07/10.19 % (3428382)Termination phase: Saturation % 69.07/10.19 % (3428382)Time elapsed: 3.256 s % 69.07/10.19 % (3428382)Peak memory usage: 161 MB % 69.07/10.19 % (3428382)Instructions burned: 12115 (million) % 69.07/10.19 % (3428400)------------------------------ % 69.07/10.19 % (3428400)------------------------------ % 69.07/10.19 % (3428402)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=3444925308:cts=off:i=3034:av=off:er=known:fsd=on_2934 on theBenchmark for (2934ds/3034Mi) % 69.07/10.19 % (3428403)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2493185528:st=2:s2a=on:i=524:s2at=2:ss=axioms_2934 on theBenchmark for (2934ds/524Mi) % 69.07/10.19 % (3428403)Instruction limit reached! % 69.07/10.19 % (3428403)------------------------------ % 76.47/11.23 % (3428403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.47/11.23 % (3428403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.47/11.23 % (3428403)CaDiCaL version: 2.1.3 % 76.47/11.23 % (3428403)Termination reason: Instruction limit % 76.47/11.23 % (3428403)Termination phase: Saturation % 76.47/11.23 % (3428403)Time elapsed: 0.143 s % 76.47/11.23 % (3428403)Peak memory usage: 93 MB % 76.47/11.23 % (3428403)Instructions burned: 527 (million) % 76.47/11.23 % (3428406)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=900085173:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2931 on theBenchmark for (2931ds/1016Mi) % 76.47/11.23 % (3428406)Refutation not found, incomplete strategy % 76.47/11.23 % (3428406)------------------------------ % 76.47/11.23 % (3428406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.47/11.23 % (3428406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.47/11.23 % (3428406)CaDiCaL version: 2.1.3 % 76.47/11.23 % (3428406)Termination reason: Refutation not found, incomplete strategy % 76.47/11.23 % (3428406)Time elapsed: 0.001 s % 76.47/11.23 % (3428406)Peak memory usage: 89 MB % 76.47/11.23 % (3428406)------------------------------ % 76.47/11.23 % (3428406)------------------------------ % 76.47/11.23 % (3428408)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3254215139:i=14123:bd=preordered:ins=4_2929 on theBenchmark for (2929ds/14123Mi) % 76.47/11.23 % (3428402)Instruction limit reached! % 76.47/11.23 % (3428402)------------------------------ % 76.47/11.23 % (3428402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.47/11.23 % (3428402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.47/11.23 % (3428402)CaDiCaL version: 2.1.3 % 76.47/11.23 % (3428402)Termination reason: Instruction limit % 76.47/11.23 % (3428402)Termination phase: Saturation % 76.47/11.23 % (3428402)Time elapsed: 0.898 s % 76.47/11.23 % (3428402)Peak memory usage: 131 MB % 76.47/11.23 % (3428402)Instructions burned: 3037 (million) % 76.47/11.23 % (3428410)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3256319087:i=5781:kws=precedence:bd=all:rawr=on_2924 on theBenchmark for (2924ds/5781Mi) % 76.47/11.23 % (3428393)Instruction limit reached! % 76.47/11.23 % (3428393)------------------------------ % 76.47/11.23 % (3428393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.47/11.23 % (3428393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.47/11.23 % (3428393)CaDiCaL version: 2.1.3 % 76.47/11.23 % (3428393)Termination reason: Instruction limit % 76.47/11.23 % (3428393)Termination phase: Saturation % 76.47/11.23 % (3428393)Time elapsed: 3.026 s % 76.47/11.23 % (3428393)Peak memory usage: 156 MB % 76.47/11.23 % (3428393)Instructions burned: 9928 (million) % 76.47/11.23 % (3428412)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=3113956223:i=2448:gtgl=5:bd=preordered:gtg=all_2920 on theBenchmark for (2920ds/2448Mi) % 76.47/11.23 % (3428392)Instruction limit reached! % 76.47/11.23 % (3428392)------------------------------ % 76.47/11.23 % (3428392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.47/11.23 % (3428392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.47/11.23 % (3428392)CaDiCaL version: 2.1.3 % 76.47/11.23 % (3428392)Termination reason: Instruction limit % 76.47/11.23 % (3428392)Termination phase: Saturation % 76.47/11.23 % (3428392)Time elapsed: 3.474 s % 76.47/11.23 % (3428392)Peak memory usage: 140 MB % 76.47/11.23 % (3428392)Instructions burned: 13915 (million) % 76.47/11.23 % (3428414)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=156184532:i=3223:kws=precedence:fgj=on:av=off_2916 on theBenchmark for (2916ds/3223Mi) % 76.47/11.23 % (3428412)Instruction limit reached! % 76.47/11.23 % (3428412)------------------------------ % 76.47/11.23 % (3428412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.47/11.23 % (3428412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.47/11.23 % (3428412)CaDiCaL version: 2.1.3 % 76.47/11.23 % (3428412)Termination reason: Instruction limit % 76.47/11.23 % (3428412)Termination phase: Saturation % 76.47/11.23 % (3428412)Time elapsed: 0.779 s % 76.47/11.23 % (3428412)Peak memory usage: 143 MB % 76.47/11.23 % (3428412)Instructions burned: 2451 (million) % 76.47/11.23 % (3428410)Instruction limit reached! % 91.43/13.34 % (3428410)------------------------------ % 91.43/13.34 % (3428410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.43/13.34 % (3428410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.43/13.34 % (3428410)CaDiCaL version: 2.1.3 % 91.43/13.34 % (3428410)Termination reason: Instruction limit % 91.43/13.34 % (3428410)Termination phase: Saturation % 91.43/13.34 % (3428410)Time elapsed: 1.274 s % 91.43/13.34 % (3428410)Peak memory usage: 98 MB % 91.43/13.34 % (3428410)Instructions burned: 5783 (million) % 91.43/13.34 % (3428416)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1001961851:st=5.6:i=2033:sd=3:ss=axioms_2911 on theBenchmark for (2911ds/2033Mi) % 91.43/13.34 % (3428417)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1459232271:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2911 on theBenchmark for (2911ds/2055Mi) % 91.43/13.34 % (3428416)Refutation not found, incomplete strategy % 91.43/13.34 % (3428416)------------------------------ % 91.43/13.34 % (3428416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.43/13.34 % (3428416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.43/13.34 % (3428416)CaDiCaL version: 2.1.3 % 91.43/13.34 % (3428416)Termination reason: Refutation not found, incomplete strategy % 91.43/13.34 % (3428416)Time elapsed: 0.330 s % 91.43/13.34 % (3428416)Peak memory usage: 128 MB % 91.43/13.34 % (3428416)Instructions burned: 904 (million) % 91.43/13.34 % (3428416)------------------------------ % 91.43/13.34 % (3428416)------------------------------ % 91.43/13.34 % (3428414)Instruction limit reached! % 91.43/13.34 % (3428414)------------------------------ % 91.43/13.34 % (3428414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.43/13.34 % (3428414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.43/13.34 % (3428414)CaDiCaL version: 2.1.3 % 91.43/13.34 % (3428414)Termination reason: Instruction limit % 91.43/13.34 % (3428414)Termination phase: Saturation % 91.43/13.34 % (3428414)Time elapsed: 0.973 s % 91.43/13.34 % (3428414)Peak memory usage: 136 MB % 91.43/13.34 % (3428414)Instructions burned: 3224 (million) % 91.43/13.34 % (3428420)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=1174301764:i=21611:sd=3:ss=axioms_2905 on theBenchmark for (2905ds/21611Mi) % 91.43/13.34 % (3428421)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3242140651:i=4835:sd=13:ss=axioms:sgt=23_2905 on theBenchmark for (2905ds/4835Mi) % 91.43/13.34 % (3428417)Instruction limit reached! % 91.43/13.34 % (3428417)------------------------------ % 91.43/13.34 % (3428417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.43/13.34 % (3428417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.43/13.34 % (3428417)CaDiCaL version: 2.1.3 % 91.43/13.34 % (3428417)Termination reason: Instruction limit % 91.43/13.34 % (3428417)Termination phase: Saturation % 91.43/13.34 % (3428417)Time elapsed: 0.627 s % 91.43/13.34 % (3428417)Peak memory usage: 131 MB % 91.43/13.34 % (3428417)Instructions burned: 2055 (million) % 91.43/13.34 % (3428424)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=3358780992:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2903 on theBenchmark for (2903ds/797Mi) % 91.43/13.34 % (3428424)Refutation not found, incomplete strategy % 91.43/13.34 % (3428424)------------------------------ % 91.43/13.34 % (3428424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.43/13.34 % (3428424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.43/13.34 % (3428424)CaDiCaL version: 2.1.3 % 91.43/13.34 % (3428424)Termination reason: Refutation not found, incomplete strategy % 91.43/13.34 % (3428424)Time elapsed: 0.001 s % 91.43/13.34 % (3428424)Peak memory usage: 88 MB % 91.43/13.34 % (3428424)Instructions burned: 3 (million) % 91.43/13.34 % (3428424)------------------------------ % 91.43/13.34 % (3428424)------------------------------ % 91.43/13.34 % (3428420)Refutation not found, incomplete strategy % 91.43/13.34 % (3428420)------------------------------ % 91.43/13.34 % (3428420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.43/13.34 % (3428420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.43/13.34 % (3428420)CaDiCaL version: 2.1.3 % 91.43/13.34 % (3428420)Termination reason: Refutation not found, incomplete strategy % 136.20/19.72 % (3428420)Time elapsed: 0.349 s % 136.20/19.72 % (3428420)Peak memory usage: 129 MB % 136.20/19.72 % (3428420)Instructions burned: 948 (million) % 136.20/19.72 % (3428426)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3758781109:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2901 on theBenchmark for (2901ds/2326Mi) % 136.20/19.72 % (3428426)Refutation not found, incomplete strategy % 136.20/19.72 % (3428426)------------------------------ % 136.20/19.72 % (3428426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.20/19.72 % (3428426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.20/19.72 % (3428426)CaDiCaL version: 2.1.3 % 136.20/19.72 % (3428426)Termination reason: Refutation not found, incomplete strategy % 136.20/19.72 % (3428426)Time elapsed: 0.001 s % 136.20/19.72 % (3428426)Peak memory usage: 88 MB % 136.20/19.72 % (3428426)Instructions burned: 3 (million) % 136.20/19.72 % (3428420)------------------------------ % 136.20/19.72 % (3428420)------------------------------ % 136.20/19.72 % (3428426)------------------------------ % 136.20/19.72 % (3428426)------------------------------ % 136.20/19.72 % (3428428)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=4132868628:i=6038:nm=6_2899 on theBenchmark for (2899ds/6038Mi) % 136.20/19.72 % (3428429)lrs+10_1_sil=32000:sp=occurrence:random_seed=1327142463:st=2:i=33334:sd=3:ss=included:sgt=32_2898 on theBenchmark for (2898ds/33334Mi) % 136.20/19.72 % (3428428)Refutation not found, incomplete strategy % 136.20/19.72 % (3428428)------------------------------ % 136.20/19.72 % (3428428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.20/19.72 % (3428428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.20/19.72 % (3428428)CaDiCaL version: 2.1.3 % 136.20/19.72 % (3428428)Termination reason: Refutation not found, incomplete strategy % 136.20/19.72 % (3428428)Time elapsed: 0.331 s % 136.20/19.72 % (3428428)Peak memory usage: 129 MB % 136.20/19.72 % (3428428)Instructions burned: 903 (million) % 136.20/19.72 % (3428428)------------------------------ % 136.20/19.72 % (3428428)------------------------------ % 136.20/19.72 % (3428432)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1980508476:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2893 on theBenchmark for (2893ds/1008Mi) % 136.20/19.72 % (3428408)Instruction limit reached! % 136.20/19.72 % (3428408)------------------------------ % 136.20/19.72 % (3428408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.20/19.72 % (3428408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.20/19.72 % (3428408)CaDiCaL version: 2.1.3 % 136.20/19.72 % (3428408)Termination reason: Instruction limit % 136.20/19.72 % (3428408)Termination phase: Saturation % 136.20/19.72 % (3428408)Time elapsed: 3.561 s % 136.20/19.72 % (3428408)Peak memory usage: 145 MB % 136.20/19.72 % (3428408)Instructions burned: 14124 (million) % 136.20/19.72 % (3428432)Refutation not found, incomplete strategy % 136.20/19.72 % (3428432)------------------------------ % 136.20/19.72 % (3428432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.20/19.72 % (3428432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.20/19.72 % (3428432)CaDiCaL version: 2.1.3 % 136.20/19.72 % (3428432)Termination reason: Refutation not found, incomplete strategy % 136.20/19.72 % (3428432)Time elapsed: 0.012 s % 136.20/19.72 % (3428432)Peak memory usage: 89 MB % 136.20/19.72 % (3428432)Instructions burned: 35 (million) % 136.20/19.72 % (3428421)Instruction limit reached! % 136.20/19.72 % (3428421)------------------------------ % 136.20/19.72 % (3428421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.20/19.72 % (3428421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.20/19.72 % (3428421)CaDiCaL version: 2.1.3 % 136.20/19.72 % (3428421)Termination reason: Instruction limit % 136.20/19.72 % (3428421)Termination phase: Saturation % 136.20/19.72 % (3428421)Time elapsed: 1.236 s % 136.20/19.72 % (3428421)Peak memory usage: 100 MB % 136.20/19.72 % (3428421)Instructions burned: 4838 (million) % 136.20/19.72 % (3428434)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=3478754042:i=8327:s2at=5:bd=preordered_2892 on theBenchmark for (2892ds/8327Mi) % 136.20/19.72 % (3428432)------------------------------ % 136.20/19.72 % (3428432)------------------------------ % 136.20/19.72 % (3428435)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=3346061156:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2891 on theBenchmark for (2891ds/1083Mi) % 153.58/22.17 % (3428437)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=4063941361:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2891 on theBenchmark for (2891ds/1084Mi) % 153.58/22.17 % (3428435)Instruction limit reached! % 153.58/22.17 % (3428435)------------------------------ % 153.58/22.17 % (3428435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.58/22.17 % (3428435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.58/22.17 % (3428435)CaDiCaL version: 2.1.3 % 153.58/22.17 % (3428435)Termination reason: Instruction limit % 153.58/22.17 % (3428435)Termination phase: Saturation % 153.58/22.17 % (3428435)Time elapsed: 0.240 s % 153.58/22.17 % (3428435)Peak memory usage: 96 MB % 153.58/22.17 % (3428435)Instructions burned: 1087 (million) % 153.58/22.17 % (3428440)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1538653316:i=6995:s2at=5:gtg=all_2888 on theBenchmark for (2888ds/6995Mi) % 153.58/22.17 % (3428437)Instruction limit reached! % 153.58/22.17 % (3428437)------------------------------ % 153.58/22.17 % (3428437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.58/22.17 % (3428437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.58/22.17 % (3428437)CaDiCaL version: 2.1.3 % 153.58/22.17 % (3428437)Termination reason: Instruction limit % 153.58/22.17 % (3428437)Termination phase: Saturation % 153.58/22.17 % (3428437)Time elapsed: 0.296 s % 153.58/22.17 % (3428437)Peak memory usage: 93 MB % 153.58/22.17 % (3428437)Instructions burned: 1088 (million) % 153.58/22.17 % (3428442)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1679751449:st=2:i=6225:sd=15:ss=axioms_2887 on theBenchmark for (2887ds/6225Mi) % 153.58/22.17 % (3428442)Refutation not found, incomplete strategy % 153.58/22.17 % (3428442)------------------------------ % 153.58/22.17 % (3428442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.58/22.17 % (3428442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.58/22.17 % (3428442)CaDiCaL version: 2.1.3 % 153.58/22.17 % (3428442)Termination reason: Refutation not found, incomplete strategy % 153.58/22.17 % (3428442)Time elapsed: 0.002 s % 153.58/22.17 % (3428442)Peak memory usage: 89 MB % 153.58/22.17 % (3428442)Instructions burned: 4 (million) % 153.58/22.17 % (3428442)------------------------------ % 153.58/22.17 % (3428442)------------------------------ % 153.58/22.17 % (3428444)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3509667304:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2884 on theBenchmark for (2884ds/3372Mi) % 153.58/22.17 % (3428444)Refutation not found, incomplete strategy % 153.58/22.17 % (3428444)------------------------------ % 153.58/22.17 % (3428444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.58/22.17 % (3428444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.58/22.17 % (3428444)CaDiCaL version: 2.1.3 % 153.58/22.17 % (3428444)Termination reason: Refutation not found, incomplete strategy % 153.58/22.17 % (3428444)Time elapsed: 0.310 s % 153.58/22.17 % (3428444)Peak memory usage: 127 MB % 153.58/22.17 % (3428444)Instructions burned: 855 (million) % 153.58/22.17 % (3428444)------------------------------ % 153.58/22.17 % (3428444)------------------------------ % 153.58/22.17 % (3428446)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=748543870:st=2.3:i=26457:sd=10:ss=included:sgt=8_2878 on theBenchmark for (2878ds/26457Mi) % 153.58/22.17 % (3428434)Instruction limit reached! % 153.58/22.17 % (3428434)------------------------------ % 153.58/22.17 % (3428434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.58/22.17 % (3428434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.58/22.17 % (3428434)CaDiCaL version: 2.1.3 % 153.58/22.17 % (3428434)Termination reason: Instruction limit % 153.58/22.17 % (3428434)Termination phase: Saturation % 153.58/22.17 % (3428434)Time elapsed: 2.107 s % 153.58/22.17 % (3428434)Peak memory usage: 138 MB % 153.58/22.17 % (3428434)Instructions burned: 8330 (million) % 153.58/22.17 % (3428448)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=3184374112:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2870 on theBenchmark for (2870ds/13494Mi) % 164.91/23.81 % (3428440)Instruction limit reached! % 164.91/23.81 % (3428440)------------------------------ % 164.91/23.81 % (3428440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.91/23.81 % (3428440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.91/23.81 % (3428440)CaDiCaL version: 2.1.3 % 164.91/23.81 % (3428440)Termination reason: Instruction limit % 164.91/23.81 % (3428440)Termination phase: Saturation % 164.91/23.81 % (3428440)Time elapsed: 2.442 s % 164.91/23.81 % (3428440)Peak memory usage: 191 MB % 164.91/23.81 % (3428440)Instructions burned: 6996 (million) % 164.91/23.81 % (3428450)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=3826293525:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2862 on theBenchmark for (2862ds/2503Mi) % 164.91/23.81 % (3428450)Instruction limit reached! % 164.91/23.81 % (3428450)------------------------------ % 164.91/23.81 % (3428450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.91/23.81 % (3428450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.91/23.81 % (3428450)CaDiCaL version: 2.1.3 % 164.91/23.81 % (3428450)Termination reason: Instruction limit % 164.91/23.81 % (3428450)Termination phase: Saturation % 164.91/23.81 % (3428450)Time elapsed: 0.751 s % 164.91/23.81 % (3428450)Peak memory usage: 135 MB % 164.91/23.81 % (3428450)Instructions burned: 2506 (million) % 164.91/23.81 % (3428452)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=1621308391:i=2559:sd=1:ep=RSTC:ss=axioms_2854 on theBenchmark for (2854ds/2559Mi) % 164.91/23.81 % (3428452)Refutation not found, incomplete strategy % 164.91/23.81 % (3428452)------------------------------ % 164.91/23.81 % (3428452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.91/23.81 % (3428452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.91/23.81 % (3428452)CaDiCaL version: 2.1.3 % 164.91/23.81 % (3428452)Termination reason: Refutation not found, incomplete strategy % 164.91/23.81 % (3428452)Time elapsed: 0.322 s % 164.91/23.81 % (3428452)Peak memory usage: 128 MB % 164.91/23.81 % (3428452)Instructions burned: 895 (million) % 164.91/23.81 % (3428452)------------------------------ % 164.91/23.81 % (3428452)------------------------------ % 164.91/23.81 % (3428454)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2074169946:i=30753:av=off:ss=included_2848 on theBenchmark for (2848ds/30753Mi) % 164.91/23.81 % (3428448)Instruction limit reached! % 164.91/23.81 % (3428448)------------------------------ % 164.91/23.81 % (3428448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.91/23.81 % (3428448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.91/23.81 % (3428448)CaDiCaL version: 2.1.3 % 164.91/23.81 % (3428448)Termination reason: Instruction limit % 164.91/23.81 % (3428448)Termination phase: Saturation % 164.91/23.81 % (3428448)Time elapsed: 3.839 s % 164.91/23.81 % (3428448)Peak memory usage: 190 MB % 164.91/23.81 % (3428448)Instructions burned: 13500 (million) % 164.91/23.81 % (3428456)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2966624502:i=26473:ep=RSTC_2831 on theBenchmark for (2831ds/26473Mi) % 164.91/23.81 % (3428429)Instruction limit reached! % 164.91/23.81 % (3428429)------------------------------ % 164.91/23.81 % (3428429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.91/23.81 % (3428429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.91/23.81 % (3428429)CaDiCaL version: 2.1.3 % 164.91/23.81 % (3428429)Termination reason: Instruction limit % 164.91/23.81 % (3428429)Termination phase: Saturation % 164.91/23.81 % (3428429)Time elapsed: 8.759 s % 164.91/23.81 % (3428429)Peak memory usage: 119 MB % 164.91/23.81 % (3428429)Instructions burned: 33334 (million) % 164.91/23.81 % (3428458)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=438498977:cts=off:i=2759:kws=inv_arity:fgj=on_2810 on theBenchmark for (2810ds/2759Mi) % 164.91/23.81 % (3428458)Refutation not found, incomplete strategy % 164.91/23.81 % (3428458)------------------------------ % 164.91/23.81 % (3428458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.91/23.81 % (3428458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.78/25.68 % (3428458)CaDiCaL version: 2.1.3 % 177.78/25.68 % (3428458)Termination reason: Refutation not found, incomplete strategy % 177.78/25.68 % (3428458)Time elapsed: 0.312 s % 177.78/25.68 % (3428458)Peak memory usage: 129 MB % 177.78/25.68 % (3428458)Instructions burned: 861 (million) % 177.78/25.68 % (3428458)------------------------------ % 177.78/25.68 % (3428458)------------------------------ % 177.78/25.68 % (3428460)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=2089870576:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2804 on theBenchmark for (2804ds/5665Mi) % 177.78/25.68 % (3428446)Instruction limit reached! % 177.78/25.68 % (3428446)------------------------------ % 177.78/25.68 % (3428446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.78/25.68 % (3428446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.78/25.68 % (3428446)CaDiCaL version: 2.1.3 % 177.78/25.68 % (3428446)Termination reason: Instruction limit % 177.78/25.68 % (3428446)Termination phase: Saturation % 177.78/25.68 % (3428446)Time elapsed: 7.803 s % 177.78/25.68 % (3428446)Peak memory usage: 194 MB % 177.78/25.68 % (3428446)Instructions burned: 26459 (million) % 177.78/25.68 % (3428462)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=1135192280:i=1532:ep=RS:ss=axioms_2799 on theBenchmark for (2799ds/1532Mi) % 177.78/25.68 % (3428462)Refutation not found, incomplete strategy % 177.78/25.68 % (3428462)------------------------------ % 177.78/25.68 % (3428462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.78/25.68 % (3428462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.78/25.68 % (3428462)CaDiCaL version: 2.1.3 % 177.78/25.68 % (3428462)Termination reason: Refutation not found, incomplete strategy % 177.78/25.68 % (3428462)Time elapsed: 0.324 s % 177.78/25.68 % (3428462)Peak memory usage: 128 MB % 177.78/25.68 % (3428462)Instructions burned: 886 (million) % 177.78/25.68 % (3428462)------------------------------ % 177.78/25.68 % (3428462)------------------------------ % 177.78/25.68 % (3428464)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=1567399461:i=1565:sd=2:ss=axioms:sgt=32_2793 on theBenchmark for (2793ds/1565Mi) % 177.78/25.68 % (3428464)Instruction limit reached! % 177.78/25.68 % (3428464)------------------------------ % 177.78/25.68 % (3428464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.78/25.68 % (3428464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.78/25.68 % (3428464)CaDiCaL version: 2.1.3 % 177.78/25.68 % (3428464)Termination reason: Instruction limit % 177.78/25.68 % (3428464)Termination phase: Saturation % 177.78/25.68 % (3428464)Time elapsed: 0.519 s % 177.78/25.68 % (3428464)Peak memory usage: 131 MB % 177.78/25.68 % (3428464)Instructions burned: 1567 (million) % 177.78/25.68 % (3428466)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=3534521044:i=1572:fgj=on:gsp=on_2787 on theBenchmark for (2787ds/1572Mi) % 177.78/25.68 % (3428460)Instruction limit reached! % 177.78/25.68 % (3428460)------------------------------ % 177.78/25.68 % (3428460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.78/25.68 % (3428460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.78/25.68 % (3428460)CaDiCaL version: 2.1.3 % 177.78/25.68 % (3428460)Termination reason: Instruction limit % 177.78/25.68 % (3428460)Termination phase: Saturation % 177.78/25.68 % (3428460)Time elapsed: 2.067 s % 177.78/25.68 % (3428460)Peak memory usage: 150 MB % 177.78/25.68 % (3428460)Instructions burned: 5666 (million) % 177.78/25.68 % (3428468)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=3455079560:i=6052:sd=4:ss=axioms:sgt=24_2782 on theBenchmark for (2782ds/6052Mi) % 177.78/25.68 % (3428466)Instruction limit reached! % 177.78/25.68 % (3428466)------------------------------ % 177.78/25.68 % (3428466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.78/25.68 % (3428466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.78/25.68 % (3428466)CaDiCaL version: 2.1.3 % 177.78/25.68 % (3428466)Termination reason: Instruction limit % 177.78/25.68 % (3428466)Termination phase: Saturation % 177.78/25.68 % (3428466)Time elapsed: 0.527 s % 177.78/25.68 % (3428466)Peak memory usage: 132 MB % 177.78/25.68 % (3428466)Instructions burned: 1574 (million) % 202.91/29.16 % (3428470)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=2478792192:i=3500:sd=1:bd=preordered:sup=off:ss=included_2781 on theBenchmark for (2781ds/3500Mi) % 202.91/29.16 % (3428468)Refutation not found, incomplete strategy % 202.91/29.16 % (3428468)------------------------------ % 202.91/29.16 % (3428468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.91/29.16 % (3428468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.91/29.16 % (3428468)CaDiCaL version: 2.1.3 % 202.91/29.16 % (3428468)Termination reason: Refutation not found, incomplete strategy % 202.91/29.16 % (3428468)Time elapsed: 0.333 s % 202.91/29.16 % (3428468)Peak memory usage: 128 MB % 202.91/29.16 % (3428468)Instructions burned: 905 (million) % 202.91/29.16 % (3428470)Refutation not found, incomplete strategy % 202.91/29.16 % (3428470)------------------------------ % 202.91/29.16 % (3428470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.91/29.16 % (3428470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.91/29.16 % (3428470)CaDiCaL version: 2.1.3 % 202.91/29.16 % (3428470)Termination reason: Refutation not found, incomplete strategy % 202.91/29.16 % (3428470)Time elapsed: 0.315 s % 202.91/29.16 % (3428470)Peak memory usage: 128 MB % 202.91/29.16 % (3428470)Instructions burned: 861 (million) % 202.91/29.16 % (3428468)------------------------------ % 202.91/29.16 % (3428468)------------------------------ % 202.91/29.16 % (3428470)------------------------------ % 202.91/29.16 % (3428470)------------------------------ % 202.91/29.16 % (3428472)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=2831788939:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2776 on theBenchmark for (2776ds/1842Mi) % 202.91/29.16 % (3428474)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2750970909:i=66096:add=on_2775 on theBenchmark for (2775ds/66096Mi) % 202.91/29.16 % (3428454)Instruction limit reached! % 202.91/29.16 % (3428454)------------------------------ % 202.91/29.16 % (3428454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.91/29.16 % (3428454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.91/29.16 % (3428454)CaDiCaL version: 2.1.3 % 202.91/29.16 % (3428454)Termination reason: Instruction limit % 202.91/29.16 % (3428454)Termination phase: Saturation % 202.91/29.16 % (3428454)Time elapsed: 7.614 s % 202.91/29.16 % (3428454)Peak memory usage: 148 MB % 202.91/29.16 % (3428454)Instructions burned: 30755 (million) % 202.91/29.16 % (3428476)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=777029246:i=1884:sd=1:nm=60:ss=axioms_2771 on theBenchmark for (2771ds/1884Mi) % 202.91/29.16 % (3428472)Instruction limit reached! % 202.91/29.16 % (3428472)------------------------------ % 202.91/29.16 % (3428472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.91/29.16 % (3428472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.91/29.16 % (3428472)CaDiCaL version: 2.1.3 % 202.91/29.16 % (3428472)Termination reason: Instruction limit % 202.91/29.16 % (3428472)Termination phase: Saturation % 202.91/29.16 % (3428472)Time elapsed: 0.564 s % 202.91/29.16 % (3428472)Peak memory usage: 132 MB % 202.91/29.16 % (3428472)Instructions burned: 1843 (million) % 202.91/29.16 % (3428478)lrs-1011_4:1_sil=16000:bsr=on:random_seed=2538787234:cts=off:i=5469:bs=on:fsr=off_2770 on theBenchmark for (2770ds/5469Mi) % 202.91/29.16 % (3428476)Refutation not found, incomplete strategy % 202.91/29.16 % (3428476)------------------------------ % 202.91/29.16 % (3428476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.91/29.16 % (3428476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.91/29.16 % (3428476)CaDiCaL version: 2.1.3 % 202.91/29.16 % (3428476)Termination reason: Refutation not found, incomplete strategy % 202.91/29.16 % (3428476)Time elapsed: 0.315 s % 202.91/29.16 % (3428476)Peak memory usage: 127 MB % 202.91/29.16 % (3428476)Instructions burned: 855 (million) % 202.91/29.16 % (3428476)------------------------------ % 202.91/29.16 % (3428476)------------------------------ % 202.91/29.16 % (3428480)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=1345936982:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2766 on theBenchmark for (2766ds/2037Mi) % 217.02/31.18 % (3428480)Instruction limit reached! % 217.02/31.18 % (3428480)------------------------------ % 217.02/31.18 % (3428480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.02/31.18 % (3428480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.02/31.18 % (3428480)CaDiCaL version: 2.1.3 % 217.02/31.18 % (3428480)Termination reason: Instruction limit % 217.02/31.18 % (3428480)Termination phase: Saturation % 217.02/31.18 % (3428480)Time elapsed: 0.683 s % 217.02/31.18 % (3428480)Peak memory usage: 138 MB % 217.02/31.18 % (3428480)Instructions burned: 2038 (million) % 217.02/31.18 % (3428482)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=1719258152:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2758 on theBenchmark for (2758ds/2110Mi) % 217.02/31.18 % (3428478)Instruction limit reached! % 217.02/31.18 % (3428478)------------------------------ % 217.02/31.18 % (3428478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.02/31.18 % (3428478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.02/31.18 % (3428478)CaDiCaL version: 2.1.3 % 217.02/31.18 % (3428478)Termination reason: Instruction limit % 217.02/31.18 % (3428478)Termination phase: Saturation % 217.02/31.18 % (3428478)Time elapsed: 1.370 s % 217.02/31.18 % (3428478)Peak memory usage: 96 MB % 217.02/31.18 % (3428478)Instructions burned: 5473 (million) % 217.02/31.18 % (3428456)Instruction limit reached! % 217.02/31.18 % (3428456)------------------------------ % 217.02/31.18 % (3428456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.02/31.18 % (3428456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.02/31.18 % (3428456)CaDiCaL version: 2.1.3 % 217.02/31.18 % (3428456)Termination reason: Instruction limit % 217.02/31.18 % (3428456)Termination phase: Saturation % 217.02/31.18 % (3428456)Time elapsed: 7.538 s % 217.02/31.18 % (3428456)Peak memory usage: 814 MB % 217.02/31.18 % (3428456)Instructions burned: 26474 (million) % 217.02/31.18 % (3428484)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=2623173943:i=2430:add=off:aac=none:nm=16_2755 on theBenchmark for (2755ds/2430Mi) % 217.02/31.18 % (3428486)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=1460361954:cond=fast:i=4891_2754 on theBenchmark for (2754ds/4891Mi) % 217.02/31.18 % (3428482)Instruction limit reached! % 217.02/31.18 % (3428482)------------------------------ % 217.02/31.18 % (3428482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.02/31.18 % (3428482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.02/31.18 % (3428482)CaDiCaL version: 2.1.3 % 217.02/31.18 % (3428482)Termination reason: Instruction limit % 217.02/31.18 % (3428482)Termination phase: Saturation % 217.02/31.18 % (3428482)Time elapsed: 0.650 s % 217.02/31.18 % (3428482)Peak memory usage: 132 MB % 217.02/31.18 % (3428482)Instructions burned: 2110 (million) % 217.02/31.18 % (3428488)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=1571984547:st=2:i=14845:sd=2:ss=included:fsd=on_2750 on theBenchmark for (2750ds/14845Mi) % 217.02/31.18 % (3428484)Instruction limit reached! % 217.02/31.18 % (3428484)------------------------------ % 217.02/31.18 % (3428484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.02/31.18 % (3428484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.02/31.18 % (3428484)CaDiCaL version: 2.1.3 % 217.02/31.18 % (3428484)Termination reason: Instruction limit % 217.02/31.18 % (3428484)Termination phase: Saturation % 217.02/31.18 % (3428484)Time elapsed: 0.783 s % 217.02/31.18 % (3428484)Peak memory usage: 140 MB % 217.02/31.18 % (3428484)Instructions burned: 2432 (million) % 217.02/31.18 % (3428488)Refutation not found, incomplete strategy % 217.02/31.18 % (3428488)------------------------------ % 217.02/31.18 % (3428488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.02/31.18 % (3428488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.02/31.18 % (3428488)CaDiCaL version: 2.1.3 % 217.02/31.18 % (3428488)Termination reason: Refutation not found, incomplete strategy % 217.02/31.18 % (3428488)Time elapsed: 0.324 s % 217.02/31.18 % (3428488)Peak memory usage: 128 MB % 217.02/31.18 % (3428488)Instructions burned: 892 (million) % 254.19/36.42 % (3428490)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=3651774386:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2746 on theBenchmark for (2746ds/7534Mi) % 254.19/36.42 % (3428488)------------------------------ % 254.19/36.42 % (3428488)------------------------------ % 254.19/36.42 % (3428492)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=875602984:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2744 on theBenchmark for (2744ds/10353Mi) % 254.19/36.42 % (3428486)Instruction limit reached! % 254.19/36.42 % (3428486)------------------------------ % 254.19/36.42 % (3428486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.19/36.42 % (3428486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.19/36.42 % (3428486)CaDiCaL version: 2.1.3 % 254.19/36.42 % (3428486)Termination reason: Instruction limit % 254.19/36.42 % (3428486)Termination phase: Saturation % 254.19/36.42 % (3428486)Time elapsed: 1.411 s % 254.19/36.42 % (3428486)Peak memory usage: 141 MB % 254.19/36.42 % (3428486)Instructions burned: 4893 (million) % 254.19/36.42 % (3428494)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1508884450:i=7860_2739 on theBenchmark for (2739ds/7860Mi) % 254.19/36.42 % (3428494)Refutation not found, incomplete strategy % 254.19/36.42 % (3428494)------------------------------ % 254.19/36.42 % (3428494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.19/36.42 % (3428494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.19/36.42 % (3428494)CaDiCaL version: 2.1.3 % 254.19/36.42 % (3428494)Termination reason: Refutation not found, incomplete strategy % 254.19/36.42 % (3428494)Time elapsed: 0.001 s % 254.19/36.42 % (3428494)Peak memory usage: 88 MB % 254.19/36.42 % (3428494)Instructions burned: 3 (million) % 254.19/36.42 % (3428494)------------------------------ % 254.19/36.42 % (3428494)------------------------------ % 254.19/36.42 % (3428496)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=349410798:i=7896:sd=2:bs=on:ss=included:sgt=20_2736 on theBenchmark for (2736ds/7896Mi) % 254.19/36.42 % (3428490)Instruction limit reached! % 254.19/36.42 % (3428490)------------------------------ % 254.19/36.42 % (3428490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.19/36.42 % (3428490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.19/36.42 % (3428490)CaDiCaL version: 2.1.3 % 254.19/36.42 % (3428490)Termination reason: Instruction limit % 254.19/36.42 % (3428490)Termination phase: Saturation % 254.19/36.42 % (3428490)Time elapsed: 2.018 s % 254.19/36.42 % (3428490)Peak memory usage: 139 MB % 254.19/36.42 % (3428490)Instructions burned: 7538 (million) % 254.19/36.42 % (3428498)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=2312930888:i=5812:gtgl=2:gtg=all_2725 on theBenchmark for (2725ds/5812Mi) % 254.19/36.42 % (3428492)Instruction limit reached! % 254.19/36.42 % (3428492)------------------------------ % 254.19/36.42 % (3428492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.19/36.42 % (3428492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.19/36.42 % (3428492)CaDiCaL version: 2.1.3 % 254.19/36.42 % (3428492)Termination reason: Instruction limit % 254.19/36.42 % (3428492)Termination phase: Saturation % 254.19/36.42 % (3428492)Time elapsed: 2.824 s % 254.19/36.42 % (3428492)Peak memory usage: 141 MB % 254.19/36.42 % (3428492)Instructions burned: 10356 (million) % 254.19/36.42 % (3428500)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=4291383288:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2715 on theBenchmark for (2715ds/2965Mi) % 254.19/36.42 % (3428496)Instruction limit reached! % 254.19/36.42 % (3428496)------------------------------ % 254.19/36.42 % (3428496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.19/36.42 % (3428496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.19/36.42 % (3428496)CaDiCaL version: 2.1.3 % 254.19/36.42 % (3428496)Termination reason: Instruction limit % 254.19/36.42 % (3428496)Termination phase: Saturation % 254.19/36.42 % (3428496)Time elapsed: 2.370 s % 254.19/36.42 % (3428496)Peak memory usage: 158 MB % 254.19/36.42 % (3428496)Instructions burned: 7898 (million) % 254.19/36.42 % (3428500)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 278.18/39.88 % (3428500)------------------------------ % 278.18/39.88 % (3428500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.18/39.88 % (3428500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.18/39.88 % (3428500)CaDiCaL version: 2.1.3 % 278.18/39.88 % (3428500)Termination reason: Unknown % 278.18/39.88 % (3428500)Termination phase: Saturation % 278.18/39.88 % (3428500)Time elapsed: 0.308 s % 278.18/39.88 % (3428500)Peak memory usage: 128 MB % 278.18/39.88 % (3428500)Instructions burned: 850 (million) % 278.18/39.88 % (3428502)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=453532095:i=2967:kws=precedence:bd=preordered:av=off_2711 on theBenchmark for (2711ds/2967Mi) % 278.18/39.88 % (3428503)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=506998182:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2711 on theBenchmark for (2711ds/3022Mi) % 278.18/39.88 % (3428498)Instruction limit reached! % 278.18/39.88 % (3428498)------------------------------ % 278.18/39.88 % (3428498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.18/39.88 % (3428498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.18/39.88 % (3428498)CaDiCaL version: 2.1.3 % 278.18/39.88 % (3428498)Termination reason: Instruction limit % 278.18/39.88 % (3428498)Termination phase: Saturation % 278.18/39.88 % (3428498)Time elapsed: 1.879 s % 278.18/39.88 % (3428498)Peak memory usage: 203 MB % 278.18/39.88 % (3428498)Instructions burned: 5815 (million) % 278.18/39.88 % (3428506)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=749032273:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2705 on theBenchmark for (2705ds/3207Mi) % 278.18/39.88 % (3428502)Instruction limit reached! % 278.18/39.88 % (3428502)------------------------------ % 278.18/39.88 % (3428502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.18/39.88 % (3428502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.18/39.88 % (3428502)CaDiCaL version: 2.1.3 % 278.18/39.88 % (3428502)Termination reason: Instruction limit % 278.18/39.88 % (3428502)Termination phase: Saturation % 278.18/39.88 % (3428502)Time elapsed: 0.898 s % 278.18/39.88 % (3428502)Peak memory usage: 133 MB % 278.18/39.88 % (3428502)Instructions burned: 2969 (million) % 278.18/39.88 % (3428503)Instruction limit reached! % 278.18/39.88 % (3428503)------------------------------ % 278.18/39.88 % (3428503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.18/39.88 % (3428503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.18/39.88 % (3428503)CaDiCaL version: 2.1.3 % 278.18/39.88 % (3428503)Termination reason: Instruction limit % 278.18/39.88 % (3428503)Termination phase: Saturation % 278.18/39.88 % (3428503)Time elapsed: 0.926 s % 278.18/39.88 % (3428503)Peak memory usage: 133 MB % 278.18/39.88 % (3428503)Instructions burned: 3023 (million) % 278.18/39.88 % (3428506)Refutation not found, incomplete strategy % 278.18/39.88 % (3428506)------------------------------ % 278.18/39.88 % (3428506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.18/39.88 % (3428506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.18/39.88 % (3428506)CaDiCaL version: 2.1.3 % 278.18/39.88 % (3428506)Termination reason: Refutation not found, incomplete strategy % 278.18/39.88 % (3428506)Time elapsed: 0.322 s % 278.18/39.88 % (3428506)Peak memory usage: 128 MB % 278.18/39.88 % (3428506)Instructions burned: 892 (million) % 278.18/39.88 % (3428508)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=1946279009:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2701 on theBenchmark for (2701ds/3289Mi) % 278.18/39.88 % (3428509)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=3795616369:i=38569:sd=3:ss=axioms:sgt=32_2701 on theBenchmark for (2701ds/38569Mi) % 278.18/39.88 % (3428506)------------------------------ % 278.18/39.88 % (3428506)------------------------------ % 278.18/39.88 % (3428512)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=3408338058:cts=off:i=3394_2699 on theBenchmark for (2699ds/3394Mi) % 278.18/39.88 % (3428508)Instruction limit reached! % 278.18/39.88 % (3428508)------------------------------ % 278.18/39.88 % (3428508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.38/42.22 % (3428508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.38/42.22 % (3428508)CaDiCaL version: 2.1.3 % 293.38/42.22 % (3428508)Termination reason: Instruction limit % 293.38/42.22 % (3428508)Termination phase: Saturation % 293.38/42.22 % (3428508)Time elapsed: 0.939 s % 293.38/42.22 % (3428508)Peak memory usage: 135 MB % 293.38/42.22 % (3428508)Instructions burned: 3290 (million) % 293.38/42.22 % (3428514)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=1410449590:i=33824:bd=preordered_2691 on theBenchmark for (2691ds/33824Mi) % 293.38/42.22 % (3428512)Instruction limit reached! % 293.38/42.22 % (3428512)------------------------------ % 293.38/42.22 % (3428512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.38/42.22 % (3428512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.38/42.22 % (3428512)CaDiCaL version: 2.1.3 % 293.38/42.22 % (3428512)Termination reason: Instruction limit % 293.38/42.22 % (3428512)Termination phase: Saturation % 293.38/42.22 % (3428512)Time elapsed: 0.989 s % 293.38/42.22 % (3428512)Peak memory usage: 134 MB % 293.38/42.22 % (3428512)Instructions burned: 3396 (million) % 293.38/42.22 % (3428516)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=3616674332:i=20684:bd=all:gtg=exists_sym_2688 on theBenchmark for (2688ds/20684Mi) % 293.38/42.22 % (3428317)Instruction limit reached! % 293.38/42.22 % (3428317)------------------------------ % 293.38/42.22 % (3428317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.38/42.22 % (3428317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.38/42.22 % (3428317)CaDiCaL version: 2.1.3 % 293.38/42.22 % (3428317)Termination reason: Instruction limit % 293.38/42.22 % (3428317)Termination phase: Saturation % 293.38/42.22 % (3428317)Time elapsed: 34.321 s % 293.38/42.22 % (3428317)Peak memory usage: 189 MB % 293.38/42.22 % (3428317)Instructions burned: 134679 (million) % 293.38/42.22 % (3428518)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=1208519760: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_2655 on theBenchmark for (2655ds/7222Mi) % 293.38/42.22 % (3428518)Refutation not found, incomplete strategy % 293.38/42.22 % (3428518)------------------------------ % 293.38/42.22 % (3428518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.38/42.22 % (3428518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.38/42.22 % (3428518)CaDiCaL version: 2.1.3 % 293.38/42.22 % (3428518)Termination reason: Refutation not found, incomplete strategy % 293.38/42.22 % (3428518)Time elapsed: 0.319 s % 293.38/42.22 % (3428518)Peak memory usage: 129 MB % 293.38/42.22 % (3428518)Instructions burned: 868 (million) % 293.38/42.22 % (3428518)------------------------------ % 293.38/42.22 % (3428518)------------------------------ % 293.38/42.22 % (3428520)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=3063896086:st=4:i=7295:sd=4:ep=R:ss=axioms_2649 on theBenchmark for (2649ds/7295Mi) % 293.38/42.22 % (3428520)Refutation not found, incomplete strategy % 293.38/42.22 % (3428520)------------------------------ % 293.38/42.22 % (3428520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.38/42.22 % (3428520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.38/42.22 % (3428520)CaDiCaL version: 2.1.3 % 293.38/42.22 % (3428520)Termination reason: Refutation not found, incomplete strategy % 293.38/42.22 % (3428520)Time elapsed: 0.319 s % 293.38/42.22 % (3428520)Peak memory usage: 128 MB % 293.38/42.22 % (3428520)Instructions burned: 883 (million) % 293.38/42.22 % (3428520)------------------------------ % 293.38/42.22 % (3428520)------------------------------ % 293.38/42.22 % (3428522)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=3705930725:i=4036:ins=10_2644 on theBenchmark for (2644ds/4036Mi) % 293.38/42.22 % (3428316)Instruction limit reached! % 293.38/42.22 % (3428316)------------------------------ % 293.38/42.22 % (3428316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.38/42.22 % (3428316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.81/43.05 % (3428316)CaDiCaL version: 2.1.3 % 300.81/43.05 % (3428316)Termination reason: Instruction limit % 300.81/43.05 % (3428316)Termination phase: Saturation % 300.81/43.05 % (3428316)Time elapsed: 35.993 s % 300.81/43.05 % (3428316)Peak memory usage: 408 MB % 300.81/43.05 % (3428316)Instructions burned: 141197 (million) % 300.81/43.05 % (3428524)lrs+10_1_sil=128000:lcm=predicate:random_seed=3137226749:st=3:i=43697:sd=5:ss=axioms_2638 on theBenchmark for (2638ds/43697Mi) % 300.81/43.05 % (3428516)Instruction limit reached! % 300.81/43.05 % (3428516)------------------------------ % 300.81/43.05 % (3428516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.81/43.05 % (3428516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.81/43.05 % (3428516)CaDiCaL version: 2.1.3 % 300.81/43.05 % (3428516)Termination reason: Instruction limit % 300.81/43.05 % (3428516)Termination phase: Saturation % 300.81/43.05 % (3428516)Time elapsed: 5.446 s % 300.81/43.05 % (3428516)Peak memory usage: 197 MB % 300.81/43.05 % (3428516)Instructions burned: 20688 (million) % 300.81/43.05 % (3428522)Instruction limit reached! % 300.81/43.05 % (3428522)------------------------------ % 300.81/43.05 % (3428522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.81/43.05 % (3428522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.81/43.05 % (3428522)CaDiCaL version: 2.1.3 % 300.81/43.05 % (3428522)Termination reason: Instruction limit % 300.81/43.05 % (3428522)Termination phase: Saturation % 300.81/43.05 % (3428522)Time elapsed: 1.091 s % 300.81/43.05 % (3428522)Peak memory usage: 133 MB % 300.81/43.05 % (3428522)Instructions burned: 4037 (million) % 300.81/43.05 % (3428526)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=1475766545:i=17599:gtg=all:ss=axioms:fsd=on_2632 on theBenchmark for (2632ds/17599Mi) % 300.81/43.05 % (3428527)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=2022552740:i=4547:bd=preordered_2632 on theBenchmark for (2632ds/4547Mi) % 300.81/43.05 % (3428474)Instruction limit reached! % 300.81/43.05 % (3428474)------------------------------ % 300.81/43.05 % (3428474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.81/43.05 % (3428474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.81/43.05 % (3428474)CaDiCaL version: 2.1.3 % 300.81/43.05 % (3428474)Termination reason: Instruction limit % 300.81/43.05 % (3428474)Termination phase: Saturation % 300.81/43.05 % (3428474)Time elapsed: 15.733 s % 300.81/43.05 % (3428474)Peak memory usage: 176 MB % 300.81/43.05 % (3428474)Instructions burned: 66098 (million) % 300.81/43.05 % (3428527)Instruction limit reached! % 300.81/43.05 % (3428527)------------------------------ % 300.81/43.05 % (3428527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.81/43.05 % (3428527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.81/43.05 % (3428527)CaDiCaL version: 2.1.3 % 300.81/43.05 % (3428527)Termination reason: Instruction limit % 300.81/43.05 % (3428527)Termination phase: Saturation % 300.81/43.05 % (3428527)Time elapsed: 1.384 s % 300.81/43.05 % (3428527)Peak memory usage: 151 MB % 300.81/43.05 % (3428527)Instructions burned: 4550 (million) % 300.81/43.05 % (3428531)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3700156776:i=32849:add=on_2617 on theBenchmark for (2617ds/32849Mi) % 300.81/43.05 % (3428530)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=663600765:i=9294:av=off_2617 on theBenchmark for (2617ds/9294Mi) % 300.81/43.05 % (3428509)Instruction limit reached! % 300.81/43.05 % (3428509)------------------------------ % 300.81/43.05 % (3428509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.81/43.05 % (3428509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.81/43.05 % (3428509)CaDiCaL version: 2.1.3 % 300.81/43.05 % (3428509)Termination reason: Instruction limit % 300.81/43.05 % (3428509)Termination phase: Saturation % 300.81/43.05 % (3428509)Time elapsed: 9.488 s % 300.81/43.05 % (3428509)Peak memory usage: 152 MB % 300.81/43.05 % (3428509)Instructions burned: 38572 (million) % 300.81/43.05 % (3428534)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=880072570:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2605 on theBenchmark for (2605ds/4 % 300.81/43.05 Terminated %------------------------------------------------------------------------------