%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW904+1 : TPTP v9.3.1. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n011.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:01 PM UTC 2026 % Result : Timeout 300.57s 43.07s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW904+1 : TPTP v9.3.1. Released v7.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.17 % Computer : n011.cluster.edu % 0.09/0.17 % Model : x86_64 x86_64 % 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.17 % Memory : 8046.5625MB % 0.09/0.17 % OS : Linux 6.8.0-71-generic % 0.09/0.17 % CPULimit : 300 % 0.09/0.17 % WCLimit : 300 % 0.09/0.17 % DateTime : Mon Sep 28 14:41:00 UTC 2026 % 0.09/0.17 % CPUTime : % 0.09/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.21 Running first-order theorem proving % 0.09/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 13.23/2.62 % (3435007)Detected formulas, will run a generic FOF schedule. % 13.23/2.62 % (3435012)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=2482984750:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 13.23/2.62 % (3435017)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3867930530:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 13.23/2.62 % (3435013)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=1837010635:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 13.23/2.62 % (3435015)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2049053953:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 13.23/2.62 % (3435016)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2731181210:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 13.23/2.62 % (3435014)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=3388268914:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 13.23/2.62 % (3435018)dis-21_1_sil=8000:lcm=predicate:random_seed=495110276: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) % 13.23/2.62 % (3435018)Instruction limit reached! % 13.23/2.62 % (3435018)------------------------------ % 13.23/2.62 % (3435018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.23/2.62 % (3435018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.23/2.62 % (3435018)CaDiCaL version: 2.1.3 % 13.23/2.62 % (3435018)Termination reason: Instruction limit % 13.23/2.62 % (3435018)Termination phase: Saturation % 13.23/2.62 % (3435018)Time elapsed: 0.049 s % 13.23/2.62 % (3435018)Peak memory usage: 89 MB % 13.23/2.62 % (3435018)Instructions burned: 129 (million) % 13.23/2.62 % (3435015)Instruction limit reached! % 13.23/2.62 % (3435015)------------------------------ % 13.23/2.62 % (3435015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.23/2.62 % (3435015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.23/2.62 % (3435015)CaDiCaL version: 2.1.3 % 13.23/2.62 % (3435015)Termination reason: Instruction limit % 13.23/2.62 % (3435015)Termination phase: Saturation % 13.23/2.62 % (3435015)Time elapsed: 0.051 s % 13.23/2.62 % (3435015)Peak memory usage: 89 MB % 13.23/2.62 % (3435015)Instructions burned: 110 (million) % 13.23/2.62 % (3435016)Instruction limit reached! % 13.23/2.62 % (3435016)------------------------------ % 13.23/2.62 % (3435016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.23/2.62 % (3435016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.23/2.62 % (3435016)CaDiCaL version: 2.1.3 % 13.23/2.62 % (3435016)Termination reason: Instruction limit % 13.23/2.62 % (3435016)Termination phase: Saturation % 13.23/2.62 % (3435016)Time elapsed: 0.061 s % 13.23/2.62 % (3435016)Peak memory usage: 88 MB % 13.23/2.62 % (3435016)Instructions burned: 119 (million) % 13.23/2.62 % (3435017)Instruction limit reached! % 13.23/2.62 % (3435017)------------------------------ % 13.23/2.62 % (3435017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.23/2.62 % (3435017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.23/2.62 % (3435017)CaDiCaL version: 2.1.3 % 13.23/2.62 % (3435017)Termination reason: Instruction limit % 13.23/2.62 % (3435017)Termination phase: Saturation % 13.23/2.62 % (3435017)Time elapsed: 0.063 s % 13.23/2.62 % (3435017)Peak memory usage: 89 MB % 13.23/2.62 % (3435017)Instructions burned: 140 (million) % 13.23/2.62 % (3435026)lrs+10_1_sil=8000:sp=occurrence:random_seed=2357570974:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 13.23/2.62 % (3435027)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2030722294:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 13.23/2.62 % (3435029)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=1045752776:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 13.23/2.62 % (3435028)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3693736075:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 13.23/2.62 % (3435027)Instruction limit reached! % 19.37/3.44 % (3435027)------------------------------ % 19.37/3.44 % (3435027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.37/3.44 % (3435027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.37/3.44 % (3435027)CaDiCaL version: 2.1.3 % 19.37/3.44 % (3435027)Termination reason: Instruction limit % 19.37/3.44 % (3435027)Termination phase: Saturation % 19.37/3.44 % (3435027)Time elapsed: 0.068 s % 19.37/3.44 % (3435027)Peak memory usage: 90 MB % 19.37/3.44 % (3435027)Instructions burned: 158 (million) % 19.37/3.44 % (3435026)Instruction limit reached! % 19.37/3.44 % (3435026)------------------------------ % 19.37/3.44 % (3435026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.37/3.44 % (3435026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.37/3.44 % (3435026)CaDiCaL version: 2.1.3 % 19.37/3.44 % (3435026)Termination reason: Instruction limit % 19.37/3.44 % (3435026)Termination phase: Saturation % 19.37/3.44 % (3435026)Time elapsed: 0.135 s % 19.37/3.44 % (3435026)Peak memory usage: 91 MB % 19.37/3.44 % (3435026)Instructions burned: 286 (million) % 19.37/3.44 % (3435029)Instruction limit reached! % 19.37/3.44 % (3435029)------------------------------ % 19.37/3.44 % (3435029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.37/3.44 % (3435029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.37/3.44 % (3435029)CaDiCaL version: 2.1.3 % 19.37/3.44 % (3435029)Termination reason: Instruction limit % 19.37/3.44 % (3435029)Termination phase: Saturation % 19.37/3.44 % (3435029)Time elapsed: 0.123 s % 19.37/3.44 % (3435029)Peak memory usage: 90 MB % 19.37/3.44 % (3435029)Instructions burned: 248 (million) % 19.37/3.44 % (3435028)Instruction limit reached! % 19.37/3.44 % (3435028)------------------------------ % 19.37/3.44 % (3435028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.37/3.44 % (3435028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.37/3.44 % (3435028)CaDiCaL version: 2.1.3 % 19.37/3.44 % (3435028)Termination reason: Instruction limit % 19.37/3.44 % (3435028)Termination phase: Saturation % 19.37/3.44 % (3435028)Time elapsed: 0.158 s % 19.37/3.44 % (3435028)Peak memory usage: 91 MB % 19.37/3.44 % (3435028)Instructions burned: 325 (million) % 19.37/3.44 % (3435034)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1386494060:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 19.37/3.44 % (3435035)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3103969264:i=2350_2994 on theBenchmark for (2994ds/2350Mi) % 19.37/3.44 % (3435036)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3462879959:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 19.37/3.44 % (3435037)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2680835142:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi) % 19.37/3.44 % (3435036)Instruction limit reached! % 19.37/3.44 % (3435036)------------------------------ % 19.37/3.44 % (3435036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.37/3.44 % (3435036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.37/3.44 % (3435036)CaDiCaL version: 2.1.3 % 19.37/3.44 % (3435036)Termination reason: Instruction limit % 19.37/3.44 % (3435036)Termination phase: Saturation % 19.37/3.44 % (3435036)Time elapsed: 0.047 s % 19.37/3.44 % (3435036)Peak memory usage: 89 MB % 19.37/3.44 % (3435036)Instructions burned: 114 (million) % 19.37/3.44 % (3435034)Instruction limit reached! % 19.37/3.44 % (3435034)------------------------------ % 19.37/3.44 % (3435034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.37/3.44 % (3435034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.37/3.44 % (3435034)CaDiCaL version: 2.1.3 % 19.37/3.44 % (3435034)Termination reason: Instruction limit % 19.37/3.44 % (3435034)Termination phase: Saturation % 19.37/3.44 % (3435034)Time elapsed: 0.130 s % 19.37/3.44 % (3435034)Peak memory usage: 90 MB % 19.37/3.44 % (3435034)Instructions burned: 295 (million) % 19.37/3.44 % (3435037)Instruction limit reached! % 19.37/3.44 % (3435037)------------------------------ % 19.37/3.44 % (3435037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.37/3.44 % (3435037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.37/3.44 % (3435037)CaDiCaL version: 2.1.3 % 19.37/3.44 % (3435037)Termination reason: Instruction limit % 42.30/6.78 % (3435037)Termination phase: Property scanning % 42.30/6.78 % (3435037)Time elapsed: 0.047 s % 42.30/6.78 % (3435037)Peak memory usage: 87 MB % 42.30/6.78 % (3435037)Instructions burned: 128 (million) % 42.30/6.78 % (3435042)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4179382629:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi) % 42.30/6.78 % (3435043)lrs+10_1_sil=8000:sp=occurrence:random_seed=1931627011:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi) % 42.30/6.78 % (3435042)Instruction limit reached! % 42.30/6.78 % (3435042)------------------------------ % 42.30/6.78 % (3435042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.30/6.78 % (3435042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.30/6.78 % (3435042)CaDiCaL version: 2.1.3 % 42.30/6.78 % (3435042)Termination reason: Instruction limit % 42.30/6.78 % (3435042)Termination phase: Property scanning % 42.30/6.78 % (3435042)Time elapsed: 0.040 s % 42.30/6.78 % (3435042)Peak memory usage: 86 MB % 42.30/6.78 % (3435042)Instructions burned: 114 (million) % 42.30/6.78 % (3435044)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2196727397:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi) % 42.30/6.78 % (3435047)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2427551484:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi) % 42.30/6.78 % (3435044)Instruction limit reached! % 42.30/6.78 % (3435044)------------------------------ % 42.30/6.78 % (3435044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.30/6.78 % (3435044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.30/6.78 % (3435044)CaDiCaL version: 2.1.3 % 42.30/6.78 % (3435044)Termination reason: Instruction limit % 42.30/6.78 % (3435044)Termination phase: Saturation % 42.30/6.78 % (3435044)Time elapsed: 0.215 s % 42.30/6.78 % (3435044)Peak memory usage: 93 MB % 42.30/6.78 % (3435044)Instructions burned: 437 (million) % 42.30/6.78 % (3435050)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=463762217:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi) % 42.30/6.78 % (3435043)Instruction limit reached! % 42.30/6.78 % (3435043)------------------------------ % 42.30/6.78 % (3435043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.30/6.78 % (3435043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.30/6.78 % (3435043)CaDiCaL version: 2.1.3 % 42.30/6.78 % (3435043)Termination reason: Instruction limit % 42.30/6.78 % (3435043)Termination phase: Saturation % 42.30/6.78 % (3435043)Time elapsed: 0.432 s % 42.30/6.78 % (3435043)Peak memory usage: 94 MB % 42.30/6.78 % (3435043)Instructions burned: 907 (million) % 42.30/6.78 % (3435050)Instruction limit reached! % 42.30/6.78 % (3435050)------------------------------ % 42.30/6.78 % (3435050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.30/6.78 % (3435050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.30/6.78 % (3435050)CaDiCaL version: 2.1.3 % 42.30/6.78 % (3435050)Termination reason: Instruction limit % 42.30/6.78 % (3435050)Termination phase: Property scanning % 42.30/6.78 % (3435050)Time elapsed: 0.047 s % 42.30/6.78 % (3435050)Peak memory usage: 86 MB % 42.30/6.78 % (3435050)Instructions burned: 136 (million) % 42.30/6.78 % (3435052)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=257226884:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi) % 42.30/6.78 % (3435053)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2202874724:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi) % 42.30/6.78 % (3435052)Instruction limit reached! % 42.30/6.78 % (3435052)------------------------------ % 42.30/6.78 % (3435052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.30/6.78 % (3435052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.30/6.78 % (3435052)CaDiCaL version: 2.1.3 % 42.30/6.78 % (3435052)Termination reason: Instruction limit % 42.30/6.78 % (3435052)Termination phase: Saturation % 42.30/6.78 % (3435052)Time elapsed: 0.257 s % 42.30/6.78 % (3435052)Peak memory usage: 91 MB % 42.30/6.78 % (3435052)Instructions burned: 593 (million) % 42.30/6.78 % (3435056)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=1660424491:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi) % 74.41/11.19 % (3435056)Instruction limit reached! % 74.41/11.19 % (3435056)------------------------------ % 74.41/11.19 % (3435056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.41/11.19 % (3435056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.41/11.19 % (3435056)CaDiCaL version: 2.1.3 % 74.41/11.19 % (3435056)Termination reason: Instruction limit % 74.41/11.19 % (3435056)Termination phase: General splitting % 74.41/11.19 % (3435056)Time elapsed: 0.046 s % 74.41/11.19 % (3435056)Peak memory usage: 87 MB % 74.41/11.19 % (3435056)Instructions burned: 127 (million) % 74.41/11.19 % (3435035)Instruction limit reached! % 74.41/11.19 % (3435035)------------------------------ % 74.41/11.19 % (3435035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.41/11.19 % (3435035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.41/11.19 % (3435035)CaDiCaL version: 2.1.3 % 74.41/11.19 % (3435035)Termination reason: Instruction limit % 74.41/11.19 % (3435035)Termination phase: Saturation % 74.41/11.19 % (3435035)Time elapsed: 1.329 s % 74.41/11.19 % (3435035)Peak memory usage: 143 MB % 74.41/11.19 % (3435035)Instructions burned: 2350 (million) % 74.41/11.19 % (3435058)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=879447841:i=134:gtgl=5:slsql=off:gtg=exists_sym_2979 on theBenchmark for (2979ds/134Mi) % 74.41/11.19 % (3435059)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=734181462:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi) % 74.41/11.19 % (3435058)Instruction limit reached! % 74.41/11.19 % (3435058)------------------------------ % 74.41/11.19 % (3435058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.41/11.19 % (3435058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.41/11.19 % (3435058)CaDiCaL version: 2.1.3 % 74.41/11.19 % (3435058)Termination reason: Instruction limit % 74.41/11.19 % (3435058)Termination phase: Twee Goal Transformation % 74.41/11.19 % (3435058)Time elapsed: 0.053 s % 74.41/11.19 % (3435058)Peak memory usage: 88 MB % 74.41/11.19 % (3435058)Instructions burned: 137 (million) % 74.41/11.19 % (3435059)Instruction limit reached! % 74.41/11.19 % (3435059)------------------------------ % 74.41/11.19 % (3435059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.41/11.19 % (3435059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.41/11.19 % (3435059)CaDiCaL version: 2.1.3 % 74.41/11.19 % (3435059)Termination reason: Instruction limit % 74.41/11.19 % (3435059)Termination phase: General splitting % 74.41/11.19 % (3435059)Time elapsed: 0.049 s % 74.41/11.19 % (3435059)Peak memory usage: 86 MB % 74.41/11.19 % (3435059)Instructions burned: 142 (million) % 74.41/11.19 % (3435062)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=415132047:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi) % 74.41/11.19 % (3435063)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=3508059647:i=6060:aac=none:ins=25_2977 on theBenchmark for (2977ds/6060Mi) % 74.41/11.19 % (3435062)Instruction limit reached! % 74.41/11.19 % (3435062)------------------------------ % 74.41/11.19 % (3435062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.41/11.19 % (3435062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.41/11.19 % (3435062)CaDiCaL version: 2.1.3 % 74.41/11.19 % (3435062)Termination reason: Instruction limit % 74.41/11.19 % (3435062)Termination phase: Saturation % 74.41/11.19 % (3435062)Time elapsed: 0.183 s % 74.41/11.19 % (3435062)Peak memory usage: 90 MB % 74.41/11.19 % (3435062)Instructions burned: 432 (million) % 74.41/11.19 % (3435066)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=898052408:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2974 on theBenchmark for (2974ds/150Mi) % 74.41/11.19 % (3435066)Instruction limit reached! % 74.41/11.19 % (3435066)------------------------------ % 74.41/11.19 % (3435066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.41/11.19 % (3435066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.41/11.19 % (3435066)CaDiCaL version: 2.1.3 % 74.41/11.19 % (3435066)Termination reason: Instruction limit % 74.41/11.19 % (3435066)Termination phase: General splitting % 101.11/15.01 % (3435066)Time elapsed: 0.053 s % 101.11/15.01 % (3435066)Peak memory usage: 87 MB % 101.11/15.01 % (3435066)Instructions burned: 152 (million) % 101.11/15.01 % (3435068)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2915778106:i=14155:bd=all_2972 on theBenchmark for (2972ds/14155Mi) % 101.11/15.01 % (3435047)Instruction limit reached! % 101.11/15.01 % (3435047)------------------------------ % 101.11/15.01 % (3435047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.11/15.01 % (3435047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.11/15.01 % (3435047)CaDiCaL version: 2.1.3 % 101.11/15.01 % (3435047)Termination reason: Instruction limit % 101.11/15.01 % (3435047)Termination phase: Saturation % 101.11/15.01 % (3435047)Time elapsed: 2.783 s % 101.11/15.01 % (3435047)Peak memory usage: 155 MB % 101.11/15.01 % (3435047)Instructions burned: 5202 (million) % 101.11/15.01 % (3435070)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3208553706:i=667:av=off:fsr=off_2961 on theBenchmark for (2961ds/667Mi) % 101.11/15.01 % (3435070)Instruction limit reached! % 101.11/15.01 % (3435070)------------------------------ % 101.11/15.01 % (3435070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.11/15.01 % (3435070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.11/15.01 % (3435070)CaDiCaL version: 2.1.3 % 101.11/15.01 % (3435070)Termination reason: Instruction limit % 101.11/15.01 % (3435070)Termination phase: Saturation % 101.11/15.01 % (3435070)Time elapsed: 0.306 s % 101.11/15.01 % (3435070)Peak memory usage: 102 MB % 101.11/15.01 % (3435070)Instructions burned: 667 (million) % 101.11/15.01 % (3435072)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=2699062986:s2a=on:i=185:s2at=1.8:fdi=4_2956 on theBenchmark for (2956ds/185Mi) % 101.11/15.01 % (3435072)Instruction limit reached! % 101.11/15.01 % (3435072)------------------------------ % 101.11/15.01 % (3435072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.11/15.01 % (3435072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.11/15.01 % (3435072)CaDiCaL version: 2.1.3 % 101.11/15.01 % (3435072)Termination reason: Instruction limit % 101.11/15.01 % (3435072)Termination phase: Saturation % 101.11/15.01 % (3435072)Time elapsed: 0.072 s % 101.11/15.01 % (3435072)Peak memory usage: 90 MB % 101.11/15.01 % (3435072)Instructions burned: 185 (million) % 101.11/15.01 % (3435074)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4072579183:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2954 on theBenchmark for (2954ds/193Mi) % 101.11/15.01 % (3435074)Instruction limit reached! % 101.11/15.01 % (3435074)------------------------------ % 101.11/15.01 % (3435074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.11/15.01 % (3435074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.11/15.01 % (3435074)CaDiCaL version: 2.1.3 % 101.11/15.01 % (3435074)Termination reason: Instruction limit % 101.11/15.01 % (3435074)Termination phase: Saturation % 101.11/15.01 % (3435074)Time elapsed: 0.097 s % 101.11/15.01 % (3435074)Peak memory usage: 90 MB % 101.11/15.01 % (3435074)Instructions burned: 195 (million) % 101.11/15.01 % (3435076)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3253118430:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2951 on theBenchmark for (2951ds/4850Mi) % 101.11/15.01 % (3435076)Refutation not found, incomplete strategy % 101.11/15.01 % (3435076)------------------------------ % 101.11/15.01 % (3435076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.11/15.01 % (3435076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.11/15.01 % (3435076)CaDiCaL version: 2.1.3 % 101.11/15.01 % (3435076)Termination reason: Refutation not found, incomplete strategy % 101.11/15.01 % (3435076)Time elapsed: 0.065 s % 101.11/15.01 % (3435076)Peak memory usage: 90 MB % 101.11/15.01 % (3435076)Instructions burned: 156 (million) % 101.11/15.01 % (3435076)------------------------------ % 101.11/15.01 % (3435076)------------------------------ % 101.11/15.01 % (3435078)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4056741612:i=12111:sd=1:ss=included_2946 on theBenchmark for (2946ds/12111Mi) % 101.11/15.01 % (3435063)Instruction limit reached! % 101.11/15.01 % (3435063)------------------------------ % 101.11/15.01 % (3435063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.33/19.26 % (3435063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.33/19.26 % (3435063)CaDiCaL version: 2.1.3 % 131.33/19.26 % (3435063)Termination reason: Instruction limit % 131.33/19.26 % (3435063)Termination phase: Saturation % 131.33/19.26 % (3435063)Time elapsed: 3.718 s % 131.33/19.26 % (3435063)Peak memory usage: 190 MB % 131.33/19.26 % (3435063)Instructions burned: 6061 (million) % 131.33/19.26 % (3435080)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2731243260:i=319:kws=precedence:fsr=off_2938 on theBenchmark for (2938ds/319Mi) % 131.33/19.26 % (3435080)Instruction limit reached! % 131.33/19.26 % (3435080)------------------------------ % 131.33/19.26 % (3435080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.33/19.26 % (3435080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.33/19.26 % (3435080)CaDiCaL version: 2.1.3 % 131.33/19.26 % (3435080)Termination reason: Instruction limit % 131.33/19.26 % (3435080)Termination phase: Saturation % 131.33/19.26 % (3435080)Time elapsed: 0.158 s % 131.33/19.26 % (3435080)Peak memory usage: 92 MB % 131.33/19.26 % (3435080)Instructions burned: 321 (million) % 131.33/19.26 % (3435082)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3255949080:i=2064:ep=RST_2935 on theBenchmark for (2935ds/2064Mi) % 131.33/19.26 % (3435082)Instruction limit reached! % 131.33/19.26 % (3435082)------------------------------ % 131.33/19.26 % (3435082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.33/19.26 % (3435082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.33/19.26 % (3435082)CaDiCaL version: 2.1.3 % 131.33/19.26 % (3435082)Termination reason: Instruction limit % 131.33/19.26 % (3435082)Termination phase: Saturation % 131.33/19.26 % (3435082)Time elapsed: 0.845 s % 131.33/19.26 % (3435082)Peak memory usage: 91 MB % 131.33/19.26 % (3435082)Instructions burned: 2066 (million) % 131.33/19.26 % (3435084)dis-1011_128_sil=32000:random_seed=2139660771:i=3706:ep=RST:av=off_2925 on theBenchmark for (2925ds/3706Mi) % 131.33/19.26 % (3435053)Instruction limit reached! % 131.33/19.26 % (3435053)------------------------------ % 131.33/19.26 % (3435053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.33/19.26 % (3435053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.33/19.26 % (3435053)CaDiCaL version: 2.1.3 % 131.33/19.26 % (3435053)Termination reason: Instruction limit % 131.33/19.26 % (3435053)Termination phase: Saturation % 131.33/19.26 % (3435053)Time elapsed: 7.253 s % 131.33/19.26 % (3435053)Peak memory usage: 204 MB % 131.33/19.26 % (3435053)Instructions burned: 13193 (million) % 131.33/19.26 % (3435086)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3267446212:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2911 on theBenchmark for (2911ds/757Mi) % 131.33/19.26 % (3435086)Instruction limit reached! % 131.33/19.26 % (3435086)------------------------------ % 131.33/19.26 % (3435086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.33/19.26 % (3435086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.33/19.26 % (3435086)CaDiCaL version: 2.1.3 % 131.33/19.26 % (3435086)Termination reason: Instruction limit % 131.33/19.26 % (3435086)Termination phase: Saturation % 131.33/19.26 % (3435086)Time elapsed: 0.332 s % 131.33/19.26 % (3435086)Peak memory usage: 91 MB % 131.33/19.26 % (3435086)Instructions burned: 758 (million) % 131.33/19.26 % (3435088)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1062650783:i=13913:ss=axioms:sgt=8_2906 on theBenchmark for (2906ds/13913Mi) % 131.33/19.26 % (3435084)Instruction limit reached! % 131.33/19.26 % (3435084)------------------------------ % 131.33/19.26 % (3435084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.33/19.26 % (3435084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.33/19.26 % (3435084)CaDiCaL version: 2.1.3 % 131.33/19.26 % (3435084)Termination reason: Instruction limit % 131.33/19.26 % (3435084)Termination phase: Saturation % 131.33/19.26 % (3435084)Time elapsed: 1.947 s % 131.33/19.26 % (3435084)Peak memory usage: 97 MB % 131.33/19.26 % (3435084)Instructions burned: 3707 (million) % 131.33/19.26 % (3435090)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=439860389:i=9925:aac=none_2904 on theBenchmark for (2904ds/9925Mi) % 131.33/19.26 % (3435068)Instruction limit reached! % 131.33/19.26 % (3435068)------------------------------ % 131.33/19.26 % (3435068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.58/22.89 % (3435068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.58/22.89 % (3435068)CaDiCaL version: 2.1.3 % 156.58/22.89 % (3435068)Termination reason: Instruction limit % 156.58/22.89 % (3435068)Termination phase: Saturation % 156.58/22.89 % (3435068)Time elapsed: 7.580 s % 156.58/22.89 % (3435068)Peak memory usage: 200 MB % 156.58/22.89 % (3435068)Instructions burned: 14155 (million) % 156.58/22.89 % (3435092)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1048861000:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2894 on theBenchmark for (2894ds/2479Mi) % 156.58/22.89 % (3435078)Instruction limit reached! % 156.58/22.89 % (3435078)------------------------------ % 156.58/22.89 % (3435078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.58/22.89 % (3435078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.58/22.89 % (3435078)CaDiCaL version: 2.1.3 % 156.58/22.89 % (3435078)Termination reason: Instruction limit % 156.58/22.89 % (3435078)Termination phase: Saturation % 156.58/22.89 % (3435078)Time elapsed: 6.201 s % 156.58/22.89 % (3435078)Peak memory usage: 212 MB % 156.58/22.89 % (3435078)Instructions burned: 12111 (million) % 156.58/22.89 % (3435094)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3077011403:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2882 on theBenchmark for (2882ds/440Mi) % 156.58/22.89 % (3435092)Instruction limit reached! % 156.58/22.89 % (3435092)------------------------------ % 156.58/22.89 % (3435092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.58/22.89 % (3435092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.58/22.89 % (3435092)CaDiCaL version: 2.1.3 % 156.58/22.89 % (3435092)Termination reason: Instruction limit % 156.58/22.89 % (3435092)Termination phase: Saturation % 156.58/22.89 % (3435092)Time elapsed: 1.210 s % 156.58/22.89 % (3435092)Peak memory usage: 102 MB % 156.58/22.89 % (3435092)Instructions burned: 2480 (million) % 156.58/22.89 % (3435094)Instruction limit reached! % 156.58/22.89 % (3435094)------------------------------ % 156.58/22.89 % (3435094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.58/22.89 % (3435094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.58/22.89 % (3435094)CaDiCaL version: 2.1.3 % 156.58/22.89 % (3435094)Termination reason: Instruction limit % 156.58/22.89 % (3435094)Termination phase: Saturation % 156.58/22.89 % (3435094)Time elapsed: 0.204 s % 156.58/22.89 % (3435094)Peak memory usage: 93 MB % 156.58/22.89 % (3435094)Instructions burned: 442 (million) % 156.58/22.89 % (3435096)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3217994422:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2880 on theBenchmark for (2880ds/11145Mi) % 156.58/22.89 % (3435097)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=4206005070:cts=off:i=3034:av=off:er=known:fsd=on_2878 on theBenchmark for (2878ds/3034Mi) % 156.58/22.89 % (3435097)Instruction limit reached! % 156.58/22.89 % (3435097)------------------------------ % 156.58/22.89 % (3435097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.58/22.89 % (3435097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.58/22.89 % (3435097)CaDiCaL version: 2.1.3 % 156.58/22.89 % (3435097)Termination reason: Instruction limit % 156.58/22.89 % (3435097)Termination phase: Saturation % 156.58/22.89 % (3435097)Time elapsed: 1.512 s % 156.58/22.89 % (3435097)Peak memory usage: 140 MB % 156.58/22.89 % (3435097)Instructions burned: 3035 (million) % 156.58/22.89 % (3435100)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=310371396:st=2:s2a=on:i=524:s2at=2:ss=axioms_2862 on theBenchmark for (2862ds/524Mi) % 156.58/22.89 % (3435100)Instruction limit reached! % 156.58/22.89 % (3435100)------------------------------ % 156.58/22.89 % (3435100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.58/22.89 % (3435100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.58/22.89 % (3435100)CaDiCaL version: 2.1.3 % 156.58/22.89 % (3435100)Termination reason: Instruction limit % 156.58/22.89 % (3435100)Termination phase: Saturation % 156.58/22.89 % (3435100)Time elapsed: 0.256 s % 156.58/22.89 % (3435100)Peak memory usage: 93 MB % 156.58/22.89 % (3435100)Instructions burned: 524 (million) % 156.58/22.89 % (3435102)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=341684647:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2858 on theBenchmark for (2858ds/1016Mi) % 185.23/26.82 % (3435102)Instruction limit reached! % 185.23/26.82 % (3435102)------------------------------ % 185.23/26.82 % (3435102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.23/26.82 % (3435102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.23/26.82 % (3435102)CaDiCaL version: 2.1.3 % 185.23/26.82 % (3435102)Termination reason: Instruction limit % 185.23/26.82 % (3435102)Termination phase: Saturation % 185.23/26.82 % (3435102)Time elapsed: 0.472 s % 185.23/26.82 % (3435102)Peak memory usage: 93 MB % 185.23/26.82 % (3435102)Instructions burned: 1018 (million) % 185.23/26.82 % (3435090)Instruction limit reached! % 185.23/26.82 % (3435090)------------------------------ % 185.23/26.82 % (3435090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.23/26.82 % (3435090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.23/26.82 % (3435090)CaDiCaL version: 2.1.3 % 185.23/26.82 % (3435090)Termination reason: Instruction limit % 185.23/26.82 % (3435090)Termination phase: Saturation % 185.23/26.82 % (3435090)Time elapsed: 5.086 s % 185.23/26.82 % (3435090)Peak memory usage: 176 MB % 185.23/26.82 % (3435090)Instructions burned: 9927 (million) % 185.23/26.82 % (3435104)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3647842521:i=14123:bd=preordered:ins=4_2851 on theBenchmark for (2851ds/14123Mi) % 185.23/26.82 % (3435105)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3166074055:i=5781:kws=precedence:bd=all:rawr=on_2851 on theBenchmark for (2851ds/5781Mi) % 185.23/26.82 % (3435088)Instruction limit reached! % 185.23/26.82 % (3435088)------------------------------ % 185.23/26.82 % (3435088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.23/26.82 % (3435088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.23/26.82 % (3435088)CaDiCaL version: 2.1.3 % 185.23/26.82 % (3435088)Termination reason: Instruction limit % 185.23/26.82 % (3435088)Termination phase: Saturation % 185.23/26.82 % (3435088)Time elapsed: 7.278 s % 185.23/26.82 % (3435088)Peak memory usage: 191 MB % 185.23/26.82 % (3435088)Instructions burned: 13914 (million) % 185.23/26.82 % (3435108)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=414638422:i=2448:gtgl=5:bd=preordered:gtg=all_2831 on theBenchmark for (2831ds/2448Mi) % 185.23/26.82 % (3435105)Instruction limit reached! % 185.23/26.82 % (3435105)------------------------------ % 185.23/26.82 % (3435105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.23/26.82 % (3435105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.23/26.82 % (3435105)CaDiCaL version: 2.1.3 % 185.23/26.82 % (3435105)Termination reason: Instruction limit % 185.23/26.82 % (3435105)Termination phase: Saturation % 185.23/26.82 % (3435105)Time elapsed: 2.597 s % 185.23/26.82 % (3435105)Peak memory usage: 102 MB % 185.23/26.82 % (3435105)Instructions burned: 5782 (million) % 185.23/26.82 % (3435110)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=486006103:i=3223:kws=precedence:fgj=on:av=off_2823 on theBenchmark for (2823ds/3223Mi) % 185.23/26.82 % (3435096)Instruction limit reached! % 185.23/26.82 % (3435096)------------------------------ % 185.23/26.82 % (3435096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.23/26.82 % (3435096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.23/26.82 % (3435096)CaDiCaL version: 2.1.3 % 185.23/26.82 % (3435096)Termination reason: Instruction limit % 185.23/26.82 % (3435096)Termination phase: Saturation % 185.23/26.82 % (3435096)Time elapsed: 6.311 s % 185.23/26.82 % (3435096)Peak memory usage: 223 MB % 185.23/26.82 % (3435096)Instructions burned: 11146 (million) % 185.23/26.82 % (3435108)Instruction limit reached! % 185.23/26.82 % (3435108)------------------------------ % 185.23/26.82 % (3435108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.23/26.82 % (3435108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.23/26.82 % (3435108)CaDiCaL version: 2.1.3 % 185.23/26.82 % (3435108)Termination reason: Instruction limit % 185.23/26.82 % (3435108)Termination phase: Saturation % 185.23/26.82 % (3435108)Time elapsed: 1.439 s % 185.23/26.82 % (3435108)Peak memory usage: 144 MB % 185.23/26.82 % (3435108)Instructions burned: 2448 (million) % 185.23/26.82 % (3435112)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2605274503:st=5.6:i=2033:sd=3:ss=axioms_2815 on theBenchmark for (2815ds/2033Mi) % 240.68/34.60 % (3435113)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=384865802:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2814 on theBenchmark for (2814ds/2055Mi) % 240.68/34.60 % (3435110)Instruction limit reached! % 240.68/34.60 % (3435110)------------------------------ % 240.68/34.60 % (3435110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.68/34.60 % (3435110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.68/34.60 % (3435110)CaDiCaL version: 2.1.3 % 240.68/34.60 % (3435110)Termination reason: Instruction limit % 240.68/34.60 % (3435110)Termination phase: Saturation % 240.68/34.60 % (3435110)Time elapsed: 1.912 s % 240.68/34.60 % (3435110)Peak memory usage: 152 MB % 240.68/34.60 % (3435110)Instructions burned: 3223 (million) % 240.68/34.60 % (3435112)Instruction limit reached! % 240.68/34.60 % (3435112)------------------------------ % 240.68/34.60 % (3435112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.68/34.60 % (3435112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.68/34.60 % (3435112)CaDiCaL version: 2.1.3 % 240.68/34.60 % (3435112)Termination reason: Instruction limit % 240.68/34.60 % (3435112)Termination phase: Saturation % 240.68/34.60 % (3435112)Time elapsed: 1.173 s % 240.68/34.60 % (3435112)Peak memory usage: 137 MB % 240.68/34.60 % (3435112)Instructions burned: 2034 (million) % 240.68/34.60 % (3435116)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=2961361933:i=21611:sd=3:ss=axioms_2802 on theBenchmark for (2802ds/21611Mi) % 240.68/34.60 % (3435113)Instruction limit reached! % 240.68/34.60 % (3435113)------------------------------ % 240.68/34.60 % (3435113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.68/34.60 % (3435113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.68/34.60 % (3435113)CaDiCaL version: 2.1.3 % 240.68/34.60 % (3435113)Termination reason: Instruction limit % 240.68/34.60 % (3435113)Termination phase: Saturation % 240.68/34.60 % (3435113)Time elapsed: 1.151 s % 240.68/34.60 % (3435113)Peak memory usage: 132 MB % 240.68/34.60 % (3435113)Instructions burned: 2055 (million) % 240.68/34.60 % (3435117)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2267758845:i=4835:sd=13:ss=axioms:sgt=23_2802 on theBenchmark for (2802ds/4835Mi) % 240.68/34.60 % (3435119)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=2143102444:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2800 on theBenchmark for (2800ds/797Mi) % 240.68/34.60 % (3435119)Instruction limit reached! % 240.68/34.60 % (3435119)------------------------------ % 240.68/34.60 % (3435119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.68/34.60 % (3435119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.68/34.60 % (3435119)CaDiCaL version: 2.1.3 % 240.68/34.60 % (3435119)Termination reason: Instruction limit % 240.68/34.60 % (3435119)Termination phase: Saturation % 240.68/34.60 % (3435119)Time elapsed: 0.325 s % 240.68/34.60 % (3435119)Peak memory usage: 89 MB % 240.68/34.60 % (3435119)Instructions burned: 800 (million) % 240.68/34.60 % (3435122)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=266833214:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2795 on theBenchmark for (2795ds/2326Mi) % 240.68/34.60 % (3435122)Instruction limit reached! % 240.68/34.60 % (3435122)------------------------------ % 240.68/34.60 % (3435122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.68/34.60 % (3435122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.68/34.60 % (3435122)CaDiCaL version: 2.1.3 % 240.68/34.60 % (3435122)Termination reason: Instruction limit % 240.68/34.60 % (3435122)Termination phase: Saturation % 240.68/34.60 % (3435122)Time elapsed: 1.174 s % 240.68/34.60 % (3435122)Peak memory usage: 102 MB % 240.68/34.60 % (3435122)Instructions burned: 2326 (million) % 240.68/34.60 % (3435124)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1393967717:i=6038:nm=6_2782 on theBenchmark for (2782ds/6038Mi) % 240.68/34.60 % (3435117)Instruction limit reached! % 240.68/34.60 % (3435117)------------------------------ % 240.68/34.60 % (3435117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.68/34.60 % (3435117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/43.07 % (3435117)CaDiCaL version: 2.1.3 % 300.57/43.07 % (3435117)Termination reason: Instruction limit % 300.57/43.07 % (3435117)Termination phase: Saturation % 300.57/43.07 % (3435117)Time elapsed: 2.279 s % 300.57/43.07 % (3435117)Peak memory usage: 105 MB % 300.57/43.07 % (3435117)Instructions burned: 4836 (million) % 300.57/43.07 % (3435126)lrs+10_1_sil=32000:sp=occurrence:random_seed=1192911569:st=2:i=33334:sd=3:ss=included:sgt=32_2777 on theBenchmark for (2777ds/33334Mi) % 300.57/43.07 % (3435104)Instruction limit reached! % 300.57/43.07 % (3435104)------------------------------ % 300.57/43.07 % (3435104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.57/43.07 % (3435104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/43.07 % (3435104)CaDiCaL version: 2.1.3 % 300.57/43.07 % (3435104)Termination reason: Instruction limit % 300.57/43.07 % (3435104)Termination phase: Saturation % 300.57/43.07 % (3435104)Time elapsed: 7.925 s % 300.57/43.07 % (3435104)Peak memory usage: 197 MB % 300.57/43.07 % (3435104)Instructions burned: 14124 (million) % 300.57/43.07 % (3435128)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=138734966:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2770 on theBenchmark for (2770ds/1008Mi) % 300.57/43.07 % (3435128)Instruction limit reached! % 300.57/43.07 % (3435128)------------------------------ % 300.57/43.07 % (3435128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.57/43.07 % (3435128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/43.07 % (3435128)CaDiCaL version: 2.1.3 % 300.57/43.07 % (3435128)Termination reason: Instruction limit % 300.57/43.07 % (3435128)Termination phase: Saturation % 300.57/43.07 % (3435128)Time elapsed: 0.485 s % 300.57/43.07 % (3435128)Peak memory usage: 96 MB % 300.57/43.07 % (3435128)Instructions burned: 1008 (million) % 300.57/43.07 % (3435130)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=1348693601:i=8327:s2at=5:bd=preordered_2764 on theBenchmark for (2764ds/8327Mi) % 300.57/43.07 % (3435124)Instruction limit reached! % 300.57/43.07 % (3435124)------------------------------ % 300.57/43.07 % (3435124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.57/43.07 % (3435124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/43.07 % (3435124)CaDiCaL version: 2.1.3 % 300.57/43.07 % (3435124)Termination reason: Instruction limit % 300.57/43.07 % (3435124)Termination phase: Saturation % 300.57/43.07 % (3435124)Time elapsed: 2.827 s % 300.57/43.07 % (3435124)Peak memory usage: 149 MB % 300.57/43.07 % (3435124)Instructions burned: 6038 (million) % 300.57/43.07 % (3435132)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=1300579719:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2752 on theBenchmark for (2752ds/1083Mi) % 300.57/43.07 % (3435132)Instruction limit reached! % 300.57/43.07 % (3435132)------------------------------ % 300.57/43.07 % (3435132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.57/43.07 % (3435132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/43.07 % (3435132)CaDiCaL version: 2.1.3 % 300.57/43.07 % (3435132)Termination reason: Instruction limit % 300.57/43.07 % (3435132)Termination phase: Saturation % 300.57/43.07 % (3435132)Time elapsed: 0.396 s % 300.57/43.07 % (3435132)Peak memory usage: 92 MB % 300.57/43.07 % (3435132)Instructions burned: 1085 (million) % 300.57/43.07 % (3435134)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=3044377637:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2747 on theBenchmark for (2747ds/1084Mi) % 300.57/43.07 % (3435134)Instruction limit reached! % 300.57/43.07 % (3435134)------------------------------ % 300.57/43.07 % (3435134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.57/43.07 % (3435134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/43.07 % (3435134)CaDiCaL version: 2.1.3 % 300.57/43.07 % (3435134)Termination reason: Instruction limit % 300.57/43.07 % (3435134)Termination phase: Saturation % 300.57/43.07 % (3435134)Time elapsed: 0.524 s % 300.57/43.07 % (3435134)Peak memory usage: 92 MB % 300.57/43.07 % (3435134)Instructions burned: 1084 (million) % 300.57/43.07 % (3435136)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1557191606:i=6995:s2at=5:gtg=all_2740 on theBenchm % 300.57/43.08 Terminated %------------------------------------------------------------------------------