%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV020-1 : TPTP v9.3.1. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n026.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:20:00 PM UTC 2026 % Result : Timeout 300.52s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV020-1 : TPTP v9.3.1. Released v2.5.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 % Computer : n026.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 09:46:12 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.65/1.25 % (3736188)Will run a generic schedule for satisfiability detection. % 6.65/1.25 % (3736197)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=778360096:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.65/1.25 % (3736194)% WARNING: option uhcvi not known. % 6.65/1.25 % (3736193)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=279572551_2999 on theBenchmark for (2999ds/0Mi) % 6.65/1.25 % (3736194)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2812230515:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.65/1.25 % (3736195)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2854771742:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.65/1.25 % (3736196)dis+10_1_sil=32000:sp=arity:random_seed=2775586065:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.65/1.25 % (3736198)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1776547097:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.65/1.25 % (3736199)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=128594896:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.65/1.26 % TRYING [1] % 6.65/1.26 % TRYING [2] % 6.65/1.26 % TRYING [3] % 6.65/1.26 % TRYING [4] % 6.65/1.26 % TRYING [5] % 6.65/1.26 % TRYING [6] % 6.65/1.26 % TRYING [7] % 6.65/1.26 % TRYING [8] % 6.65/1.26 % TRYING [9] % 6.65/1.26 % TRYING [10] % 6.65/1.26 % TRYING [11] % 6.65/1.26 % TRYING [12] % 6.65/1.26 % TRYING [13] % 6.65/1.26 % (3736197)Instruction limit reached! % 6.65/1.26 % (3736197)------------------------------ % 6.65/1.26 % (3736197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.65/1.26 % (3736197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.26 % (3736197)CaDiCaL version: 2.1.3 % 6.65/1.26 % (3736197)Termination reason: Instruction limit % 6.65/1.26 % (3736197)Termination phase: Saturation % 6.65/1.26 % (3736197)Time elapsed: 0.036 s % 6.65/1.26 % (3736197)Peak memory usage: 11 MB % 6.65/1.26 % (3736197)Instructions burned: 117 (million) % 6.65/1.26 % TRYING [14] % 6.65/1.26 % (3736207)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=941721905:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.65/1.26 % TRYING [1] % 6.65/1.26 % TRYING [2] % 6.65/1.26 % TRYING [3] % 6.65/1.26 % TRYING [4] % 6.65/1.26 % TRYING [5] % 6.65/1.26 % TRYING [6] % 6.65/1.26 % TRYING [7] % 6.65/1.26 % TRYING [8] % 6.65/1.26 % TRYING [9] % 6.65/1.26 % TRYING [15] % 6.65/1.26 % TRYING [10] % 6.65/1.26 % TRYING [11] % 6.65/1.26 % TRYING [12] % 6.65/1.26 % TRYING [13] % 6.65/1.26 % TRYING [16] % 6.65/1.26 % (3736196)Instruction limit reached! % 6.65/1.26 % (3736196)------------------------------ % 6.65/1.26 % (3736196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.65/1.26 % (3736196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.26 % (3736196)CaDiCaL version: 2.1.3 % 6.65/1.26 % (3736196)Termination reason: Instruction limit % 6.65/1.26 % (3736196)Termination phase: Saturation % 6.65/1.26 % (3736196)Time elapsed: 0.057 s % 6.65/1.26 % (3736196)Peak memory usage: 11 MB % 6.65/1.26 % (3736196)Instructions burned: 104 (million) % 6.65/1.26 % TRYING [14] % 6.65/1.26 % TRYING [15] % 6.65/1.26 % (3736198)Instruction limit reached! % 6.65/1.26 % (3736198)------------------------------ % 6.65/1.26 % (3736198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.65/1.26 % (3736198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.26 % (3736198)CaDiCaL version: 2.1.3 % 6.65/1.26 % (3736198)Termination reason: Instruction limit % 6.65/1.26 % (3736198)Termination phase: Saturation % 6.65/1.26 % (3736198)Time elapsed: 0.068 s % 6.65/1.26 % (3736198)Peak memory usage: 11 MB % 6.65/1.26 % (3736198)Instructions burned: 132 (million) % 6.65/1.26 % TRYING [17] % 6.65/1.26 % TRYING [16] % 6.65/1.26 % (3736209)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4149380391:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.65/1.26 % TRYING [17] % 6.65/1.26 % TRYING [18] % 6.65/1.26 % (3736210)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1315618782:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.65/1.26 % (3736199)Instruction limit reached! % 6.65/1.26 % (3736199)------------------------------ % 6.65/1.26 % (3736199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.65/1.26 % (3736199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.26 % (3736199)CaDiCaL version: 2.1.3 % 6.65/1.26 % (3736199)Termination reason: Instruction limit % 6.65/1.26 % (3736199)Termination phase: Saturation % 6.65/1.26 % (3736199)Time elapsed: 0.090 s % 6.65/1.26 % (3736199)Peak memory usage: 12 MB % 31.33/4.76 % (3736199)Instructions burned: 159 (million) % 31.33/4.76 % TRYING [18] % 31.33/4.76 % TRYING [19] % 31.33/4.76 % TRYING [19] % 31.33/4.76 % (3736213)ott-21_1_sil=16000:fs=off:random_seed=3841527728:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 31.33/4.76 % TRYING [20] % 31.33/4.76 % TRYING [20] % 31.33/4.76 % TRYING [21] % 31.33/4.76 % (3736209)Instruction limit reached! % 31.33/4.76 % (3736209)------------------------------ % 31.33/4.76 % (3736209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.33/4.76 % (3736209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.33/4.76 % (3736209)CaDiCaL version: 2.1.3 % 31.33/4.76 % (3736209)Termination reason: Instruction limit % 31.33/4.76 % (3736209)Termination phase: Saturation % 31.33/4.76 % (3736209)Time elapsed: 0.068 s % 31.33/4.76 % (3736209)Peak memory usage: 11 MB % 31.33/4.76 % (3736209)Instructions burned: 131 (million) % 31.33/4.76 % TRYING [22] % 31.33/4.76 % TRYING [21] % 31.33/4.76 % (3736207)Instruction limit reached! % 31.33/4.76 % (3736207)------------------------------ % 31.33/4.76 % (3736207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.33/4.76 % (3736207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.33/4.76 % (3736207)CaDiCaL version: 2.1.3 % 31.33/4.76 % (3736207)Termination reason: Instruction limit % 31.33/4.76 % (3736207)Termination phase: Finite model building constraint generation % 31.33/4.76 % (3736207)Time elapsed: 0.124 s % 31.33/4.76 % (3736207)Peak memory usage: 17 MB % 31.33/4.76 % (3736207)Instructions burned: 716 (million) % 31.33/4.76 % (3736215)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3522743730:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 31.33/4.76 % (3736216)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4123431132:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 31.33/4.76 % TRYING [1] % 31.33/4.76 % TRYING [2] % 31.33/4.76 % TRYING [3] % 31.33/4.76 % TRYING [4] % 31.33/4.76 % TRYING [5] % 31.33/4.76 % TRYING [6] % 31.33/4.76 % TRYING [7] % 31.33/4.76 % TRYING [8] % 31.33/4.76 % TRYING [9] % 31.33/4.76 % TRYING [10] % 31.33/4.76 % TRYING [11] % 31.33/4.76 % TRYING [22] % 31.33/4.76 % TRYING [12] % 31.33/4.76 % (3736213)Instruction limit reached! % 31.33/4.76 % (3736213)------------------------------ % 31.33/4.76 % (3736213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.33/4.76 % (3736213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.33/4.76 % (3736213)CaDiCaL version: 2.1.3 % 31.33/4.76 % (3736213)Termination reason: Instruction limit % 31.33/4.76 % (3736213)Termination phase: Saturation % 31.33/4.76 % (3736213)Time elapsed: 0.084 s % 31.33/4.76 % (3736213)Peak memory usage: 12 MB % 31.33/4.76 % (3736213)Instructions burned: 180 (million) % 31.33/4.76 % TRYING [13] % 31.33/4.76 % TRYING [14] % 31.33/4.76 % (3736219)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=99046040:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 31.33/4.76 % TRYING [15] % 31.33/4.76 % TRYING [23] % 31.33/4.76 % TRYING [16] % 31.33/4.76 % TRYING [17] % 31.33/4.76 % TRYING [18] % 31.33/4.76 % TRYING [24] % 31.33/4.76 % TRYING [19] % 31.33/4.76 % TRYING [25] % 31.33/4.76 % TRYING [20] % 31.33/4.76 % (3736216)Instruction limit reached! % 31.33/4.76 % (3736216)------------------------------ % 31.33/4.76 % (3736216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.33/4.76 % (3736216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.33/4.76 % (3736216)CaDiCaL version: 2.1.3 % 31.33/4.76 % (3736216)Termination reason: Instruction limit % 31.33/4.76 % (3736216)Termination phase: Finite model building SAT solving % 31.33/4.76 % (3736216)Time elapsed: 0.158 s % 31.33/4.76 % (3736216)Peak memory usage: 14 MB % 31.33/4.76 % (3736216)Instructions burned: 868 (million) % 31.33/4.76 % (3736221)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3502895841:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi) % 31.33/4.76 % TRYING [14] % 31.33/4.76 % TRYING [15] % 31.33/4.76 % TRYING [26] % 31.33/4.76 % TRYING [16] % 31.33/4.76 % TRYING [17] % 31.33/4.76 % TRYING [18] % 31.33/4.76 % (3736215)Instruction limit reached! % 31.33/4.76 % (3736215)------------------------------ % 31.33/4.76 % (3736215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.33/4.76 % (3736215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.33/4.76 % (3736215)CaDiCaL version: 2.1.3 % 31.33/4.76 % (3736215)Termination reason: Instruction limit % 31.33/4.76 % (3736215)Termination phase: Saturation % 31.33/4.76 % (3736215)Time elapsed: 0.256 s % 31.33/4.76 % (3736215)Peak memory usage: 12 MB % 31.33/4.76 % (3736215)Instructions burned: 477 (million) % 31.33/4.76 % TRYING [27] % 31.33/4.76 % TRYING [19] % 31.33/4.76 % (3736210)Instruction limit reached! % 31.33/4.76 % (3736210)------------------------------ % 31.33/4.76 % (3736210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.68/6.60 % (3736210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.68/6.60 % (3736210)CaDiCaL version: 2.1.3 % 44.68/6.60 % (3736210)Termination reason: Instruction limit % 44.68/6.60 % (3736210)Termination phase: Saturation % 44.68/6.60 % (3736210)Time elapsed: 0.351 s % 44.68/6.60 % (3736210)Peak memory usage: 13 MB % 44.68/6.60 % (3736210)Instructions burned: 686 (million) % 44.68/6.60 % (3736223)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=205423332:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi) % 44.68/6.60 % TRYING [20] % 44.68/6.60 % (3736225)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=304752562:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi) % 44.68/6.60 % TRYING [21] % 44.68/6.60 % TRYING [28] % 44.68/6.60 % (3736221)Instruction limit reached! % 44.68/6.60 % (3736221)------------------------------ % 44.68/6.60 % (3736221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.68/6.60 % (3736221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.68/6.60 % (3736221)CaDiCaL version: 2.1.3 % 44.68/6.60 % (3736221)Termination reason: Instruction limit % 44.68/6.60 % (3736221)Termination phase: Finite model building SAT solving % 44.68/6.60 % (3736221)Time elapsed: 0.159 s % 44.68/6.60 % (3736221)Peak memory usage: 14 MB % 44.68/6.60 % (3736221)Instructions burned: 890 (million) % 44.68/6.60 % (3736227)fmb+10_1_sil=64000:random_seed=965216897:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 44.68/6.60 % TRYING [1] % 44.68/6.60 % TRYING [2] % 44.68/6.60 % TRYING [3] % 44.68/6.60 % TRYING [4] % 44.68/6.60 % TRYING [5] % 44.68/6.60 % TRYING [6] % 44.68/6.60 % TRYING [7] % 44.68/6.60 % TRYING [8] % 44.68/6.60 % TRYING [9] % 44.68/6.60 % TRYING [10] % 44.68/6.60 % TRYING [11] % 44.68/6.60 % TRYING [12] % 44.68/6.60 % TRYING [13] % 44.68/6.60 % TRYING [14] % 44.68/6.60 % TRYING [15] % 44.68/6.60 % TRYING [29] % 44.68/6.60 % TRYING [16] % 44.68/6.60 % TRYING [17] % 44.68/6.60 % TRYING [18] % 44.68/6.60 % TRYING [19] % 44.68/6.60 % TRYING [30] % 44.68/6.60 % TRYING [20] % 44.68/6.60 % TRYING [21] % 44.68/6.60 % TRYING [22] % 44.68/6.60 % TRYING [31] % 44.68/6.60 % TRYING [23] % 44.68/6.60 % (3736223)Instruction limit reached! % 44.68/6.60 % (3736223)------------------------------ % 44.68/6.60 % (3736223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.68/6.60 % (3736223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.68/6.60 % (3736223)CaDiCaL version: 2.1.3 % 44.68/6.60 % (3736223)Termination reason: Instruction limit % 44.68/6.60 % (3736223)Termination phase: Saturation % 44.68/6.60 % (3736223)Time elapsed: 0.362 s % 44.68/6.60 % (3736223)Peak memory usage: 14 MB % 44.68/6.60 % (3736223)Instructions burned: 693 (million) % 44.68/6.60 % (3736229)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2723413638:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi) % 44.68/6.60 % TRYING [24] % 44.68/6.60 % TRYING [20] % 44.68/6.60 % TRYING [32] % 44.68/6.60 % (3736219)Instruction limit reached! % 44.68/6.60 % (3736219)------------------------------ % 44.68/6.60 % (3736219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.68/6.60 % (3736219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.68/6.60 % (3736219)CaDiCaL version: 2.1.3 % 44.68/6.60 % (3736219)Termination reason: Instruction limit % 44.68/6.60 % (3736219)Termination phase: Saturation % 44.68/6.60 % (3736219)Time elapsed: 0.624 s % 44.68/6.60 % (3736219)Peak memory usage: 14 MB % 44.68/6.60 % (3736219)Instructions burned: 1181 (million) % 44.68/6.60 % TRYING [21] % 44.68/6.60 % (3736231)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2805345788:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi) % 44.68/6.60 % TRYING [8] % 44.68/6.60 % TRYING [9] % 44.68/6.60 % TRYING [10] % 44.68/6.60 % TRYING [11] % 44.68/6.60 % TRYING [12] % 44.68/6.60 % TRYING [13] % 44.68/6.60 % TRYING [22] % 44.68/6.60 % TRYING [25] % 44.68/6.60 % TRYING [14] % 44.68/6.60 % (3736225)Instruction limit reached! % 44.68/6.60 % (3736225)------------------------------ % 44.68/6.60 % (3736225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.68/6.60 % (3736225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.68/6.60 % (3736225)CaDiCaL version: 2.1.3 % 44.68/6.60 % (3736225)Termination reason: Instruction limit % 44.68/6.60 % (3736225)Termination phase: Saturation % 44.68/6.60 % (3736225)Time elapsed: 0.438 s % 44.68/6.60 % (3736225)Peak memory usage: 13 MB % 44.68/6.60 % (3736225)Instructions burned: 880 (million) % 44.68/6.60 % TRYING [15] % 44.68/6.60 % TRYING [16] % 44.68/6.60 % (3736233)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1944784464:i=5131_2990 on theBenchmark for (2990ds/5131Mi) % 44.68/6.60 % TRYING [23] % 44.68/6.60 % TRYING [17] % 44.68/6.60 % TRYING [18] % 44.68/6.60 % TRYING [33] % 44.68/6.60 % TRYING [26] % 44.68/6.60 % TRYING [19] % 44.68/6.60 % TRYING [24] % 44.68/6.60 % TRYING [20] % 70.71/10.29 % TRYING [25] % 70.71/10.29 % TRYING [21] % 70.71/10.29 % TRYING [27] % 70.71/10.29 % TRYING [22] % 70.71/10.29 % TRYING [26] % 70.71/10.29 % TRYING [34] % 70.71/10.29 % TRYING [23] % 70.71/10.29 % TRYING [24] % 70.71/10.29 % TRYING [27] % 70.71/10.29 % TRYING [28] % 70.71/10.29 % (3736231)Instruction limit reached! % 70.71/10.29 % (3736231)------------------------------ % 70.71/10.29 % (3736231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.71/10.29 % (3736231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.71/10.29 % (3736231)CaDiCaL version: 2.1.3 % 70.71/10.29 % (3736231)Termination reason: Instruction limit % 70.71/10.29 % (3736231)Termination phase: Finite model building constraint generation % 70.71/10.29 % (3736231)Time elapsed: 0.312 s % 70.71/10.29 % (3736231)Peak memory usage: 20 MB % 70.71/10.29 % (3736231)Instructions burned: 923 (million) % 70.71/10.29 % (3736235)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=177343284:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi) % 70.71/10.29 % TRYING [28] % 70.71/10.29 % TRYING [35] % 70.71/10.29 % TRYING [29] % 70.71/10.29 % TRYING [29] % 70.71/10.29 % TRYING [30] % 70.71/10.29 % TRYING [36] % 70.71/10.29 % TRYING [30] % 70.71/10.29 % TRYING [31] % 70.71/10.29 % TRYING [31] % 70.71/10.29 % TRYING [37] % 70.71/10.29 % TRYING [32] % 70.71/10.29 % TRYING [33] % 70.71/10.29 % TRYING [32] % 70.71/10.29 % TRYING [38] % 70.71/10.29 % TRYING [34] % 70.71/10.29 % TRYING [39] % 70.71/10.29 % TRYING [33] % 70.71/10.29 % TRYING [35] % 70.71/10.29 % TRYING [36] % 70.71/10.29 % TRYING [34] % 70.71/10.29 % TRYING [40] % 70.71/10.29 % (3736235)Instruction limit reached! % 70.71/10.29 % (3736235)------------------------------ % 70.71/10.29 % (3736235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.71/10.29 % (3736235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.71/10.29 % (3736235)CaDiCaL version: 2.1.3 % 70.71/10.29 % (3736235)Termination reason: Instruction limit % 70.71/10.29 % (3736235)Termination phase: Saturation % 70.71/10.29 % (3736235)Time elapsed: 0.953 s % 70.71/10.29 % (3736235)Peak memory usage: 39 MB % 70.71/10.29 % (3736235)Instructions burned: 1473 (million) % 70.71/10.29 % (3736237)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2756396541:i=6324_2978 on theBenchmark for (2978ds/6324Mi) % 70.71/10.29 % TRYING [77] % 70.71/10.29 % TRYING [37] % 70.71/10.29 % TRYING [41] % 70.71/10.29 % TRYING [35] % 70.71/10.29 % TRYING [38] % 70.71/10.29 % TRYING [42] % 70.71/10.29 % TRYING [39] % 70.71/10.29 % TRYING [36] % 70.71/10.29 % TRYING [40] % 70.71/10.29 % TRYING [43] % 70.71/10.29 % TRYING [37] % 70.71/10.29 % TRYING [41] % 70.71/10.29 % TRYING [44] % 70.71/10.29 % TRYING [38] % 70.71/10.29 % TRYING [42] % 70.71/10.29 % TRYING [45] % 70.71/10.29 % (3736233)Instruction limit reached! % 70.71/10.29 % (3736233)------------------------------ % 70.71/10.29 % (3736233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.71/10.29 % (3736233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.71/10.29 % (3736233)CaDiCaL version: 2.1.3 % 70.71/10.29 % (3736233)Termination reason: Instruction limit % 70.71/10.29 % (3736233)Termination phase: Saturation % 70.71/10.29 % (3736233)Time elapsed: 2.448 s % 70.71/10.29 % (3736233)Peak memory usage: 16 MB % 70.71/10.29 % (3736233)Instructions burned: 5132 (million) % 70.71/10.29 % (3736239)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3278310908:fmbsr=2.30978:i=2174_2965 on theBenchmark for (2965ds/2174Mi) % 70.71/10.29 % TRYING [16] % 70.71/10.29 % TRYING [43] % 70.71/10.29 % TRYING [39] % 70.71/10.29 % TRYING [46] % 70.71/10.29 % TRYING [44] % 70.71/10.29 % TRYING [40] % 70.71/10.29 % TRYING [47] % 70.71/10.29 % TRYING [78] % 70.71/10.29 % TRYING [45] % 70.71/10.29 % (3736229)Instruction limit reached! % 70.71/10.29 % (3736229)------------------------------ % 70.71/10.29 % (3736229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.71/10.29 % (3736229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.71/10.29 % (3736229)CaDiCaL version: 2.1.3 % 70.71/10.29 % (3736229)Termination reason: Instruction limit % 70.71/10.29 % (3736229)Termination phase: Finite model building constraint generation % 70.71/10.29 % (3736229)Time elapsed: 3.242 s % 70.71/10.29 % (3736229)Peak memory usage: 67 MB % 70.71/10.29 % (3736229)Instructions burned: 9515 (million) % 70.71/10.29 % (3736241)ott-2_1_sil=16000:newcnf=on:random_seed=1323401257:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2958 on theBenchmark for (2958ds/869Mi) % 70.71/10.29 % TRYING [48] % 70.71/10.29 % TRYING [41] % 70.71/10.29 % (3736227)Instruction limit reached! % 70.71/10.29 % (3736227)------------------------------ % 70.71/10.29 % (3736227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.71/10.29 % (3736227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.71/10.29 % (3736227)CaDiCaL version: 2.1.3 % 70.71/10.29 % (3736227)Termination reason: Instruction limit % 70.71/10.29 % (3736227)Termination phase: Finite model building SAT solving % 70.71/10.29 % (3736227)Time elapsed: 3.979 s % 70.71/10.29 % (3736227)Peak memory usage: 45 MB % 70.71/10.29 % (3736227)Instructions burned: 22067 (million) % 153.70/22.02 % (3736243)ott+10_1_sil=32000:tgt=ground:random_seed=2873534094:i=5114:av=off_2954 on theBenchmark for (2954ds/5114Mi) % 153.70/22.02 % (3736241)Instruction limit reached! % 153.70/22.02 % (3736241)------------------------------ % 153.70/22.02 % (3736241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.70/22.02 % (3736241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.70/22.02 % (3736241)CaDiCaL version: 2.1.3 % 153.70/22.02 % (3736241)Termination reason: Instruction limit % 153.70/22.02 % (3736241)Termination phase: Saturation % 153.70/22.02 % (3736241)Time elapsed: 0.446 s % 153.70/22.02 % (3736241)Peak memory usage: 12 MB % 153.70/22.02 % (3736241)Instructions burned: 871 (million) % 153.70/22.02 % (3736245)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2388821287:i=54282_2954 on theBenchmark for (2954ds/54282Mi) % 153.70/22.02 % TRYING [1] % 153.70/22.02 % TRYING [2] % 153.70/22.02 % TRYING [3] % 153.70/22.02 % TRYING [4] % 153.70/22.02 % TRYING [5] % 153.70/22.02 % TRYING [6] % 153.70/22.02 % TRYING [7] % 153.70/22.02 % TRYING [8] % 153.70/22.02 % TRYING [9] % 153.70/22.02 % TRYING [10] % 153.70/22.02 % TRYING [11] % 153.70/22.02 % (3736239)Instruction limit reached! % 153.70/22.02 % (3736239)------------------------------ % 153.70/22.02 % (3736239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.70/22.02 % (3736239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.70/22.02 % (3736239)CaDiCaL version: 2.1.3 % 153.70/22.02 % (3736239)Termination reason: Instruction limit % 153.70/22.02 % (3736239)Termination phase: Finite model building SAT solving % 153.70/22.02 % (3736239)Time elapsed: 1.188 s % 153.70/22.02 % (3736239)Peak memory usage: 65 MB % 153.70/22.02 % (3736239)Instructions burned: 2174 (million) % 153.70/22.02 % TRYING [12] % 153.70/22.02 % TRYING [13] % 153.70/22.02 % TRYING [14] % 153.70/22.02 % (3736247)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2250695623:i=3512:aac=none_2953 on theBenchmark for (2953ds/3512Mi) % 153.70/22.02 % TRYING [15] % 153.70/22.02 % TRYING [16] % 153.70/22.02 % TRYING [17] % 153.70/22.02 % TRYING [18] % 153.70/22.02 % TRYING [19] % 153.70/22.02 % (3736237)Instruction limit reached! % 153.70/22.02 % (3736237)------------------------------ % 153.70/22.02 % (3736237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.70/22.02 % (3736237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.70/22.02 % (3736237)CaDiCaL version: 2.1.3 % 153.70/22.02 % (3736237)Termination reason: Instruction limit % 153.70/22.02 % (3736237)Termination phase: Finite model building constraint generation % 153.70/22.02 % (3736237)Time elapsed: 2.505 s % 153.70/22.02 % (3736237)Peak memory usage: 266 MB % 153.70/22.02 % (3736237)Instructions burned: 6326 (million) % 153.70/22.02 % TRYING [20] % 153.70/22.02 % TRYING [21] % 153.70/22.02 % (3736249)dis+21_1_sil=32000:sas=cadical:random_seed=3553996269:i=3773:amm=off_2952 on theBenchmark for (2952ds/3773Mi) % 153.70/22.02 % TRYING [49] % 153.70/22.02 % TRYING [22] % 153.70/22.02 % TRYING [23] % 153.70/22.02 % TRYING [24] % 153.70/22.02 % TRYING [25] % 153.70/22.02 % TRYING [26] % 153.70/22.02 % TRYING [27] % 153.70/22.02 % TRYING [28] % 153.70/22.02 % TRYING [29] % 153.70/22.02 % TRYING [50] % 153.70/22.02 % TRYING [30] % 153.70/22.02 % TRYING [31] % 153.70/22.02 % TRYING [32] % 153.70/22.02 % TRYING [33] % 153.70/22.02 % TRYING [51] % 153.70/22.02 % TRYING [34] % 153.70/22.02 % TRYING [35] % 153.70/22.02 % (3736243)Instruction limit reached! % 153.70/22.02 % (3736243)------------------------------ % 153.70/22.02 % (3736243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.70/22.02 % (3736243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.70/22.02 % (3736243)CaDiCaL version: 2.1.3 % 153.70/22.02 % (3736243)Termination reason: Instruction limit % 153.70/22.02 % (3736243)Termination phase: Saturation % 153.70/22.02 % (3736243)Time elapsed: 1.357 s % 153.70/22.02 % (3736243)Peak memory usage: 18 MB % 153.70/22.02 % (3736243)Instructions burned: 5116 (million) % 153.70/22.02 % (3736251)ott+11_1_sil=16000:gs=on:random_seed=932482314:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2940 on theBenchmark for (2940ds/2251Mi) % 153.70/22.02 % TRYING [36] % 153.70/22.02 % TRYING [52] % 153.70/22.02 % TRYING [37] % 153.70/22.02 % TRYING [38] % 153.70/22.02 % (3736247)Instruction limit reached! % 153.70/22.02 % (3736247)------------------------------ % 153.70/22.02 % (3736247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.70/22.02 % (3736247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.70/22.02 % (3736247)CaDiCaL version: 2.1.3 % 153.70/22.02 % (3736247)Termination reason: Instruction limit % 153.70/22.02 % (3736247)Termination phase: Saturation % 153.70/22.02 % (3736247)Time elapsed: 1.701 s % 153.70/22.02 % (3736247)Peak memory usage: 14 MB % 153.70/22.02 % (3736247)Instructions burned: 3514 (million) % 153.70/22.02 % (3736253)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=392950929:fmbsr=1.6:i=67534_2936 on theBenchmark for (2936ds/67534Mi) % 153.70/22.02 % TRYING [7] % 153.70/22.02 % TRYING [8] % 153.70/22.02 % TRYING [9] % 226.75/32.25 % TRYING [10] % 226.75/32.25 % TRYING [11] % 226.75/32.25 % TRYING [12] % 226.75/32.25 % TRYING [13] % 226.75/32.25 % (3736251)Instruction limit reached! % 226.75/32.25 % (3736251)------------------------------ % 226.75/32.25 % (3736251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.75/32.25 % (3736251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.75/32.25 % (3736251)CaDiCaL version: 2.1.3 % 226.75/32.25 % (3736251)Termination reason: Instruction limit % 226.75/32.25 % (3736251)Termination phase: Saturation % 226.75/32.25 % (3736251)Time elapsed: 0.496 s % 226.75/32.25 % (3736251)Peak memory usage: 13 MB % 226.75/32.25 % (3736251)Instructions burned: 2253 (million) % 226.75/32.25 % (3736256)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2097769023:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2935 on theBenchmark for (2935ds/4591Mi) % 226.75/32.25 % TRYING [39] % 226.75/32.25 % TRYING [14] % 226.75/32.25 % TRYING [15] % 226.75/32.25 % TRYING [16] % 226.75/32.25 % TRYING [53] % 226.75/32.25 % TRYING [17] % 226.75/32.25 % TRYING [18] % 226.75/32.25 % TRYING [19] % 226.75/32.25 % TRYING [40] % 226.75/32.25 % TRYING [20] % 226.75/32.25 % (3736249)Instruction limit reached! % 226.75/32.25 % (3736249)------------------------------ % 226.75/32.25 % (3736249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.75/32.25 % (3736249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.75/32.25 % (3736249)CaDiCaL version: 2.1.3 % 226.75/32.25 % (3736249)Termination reason: Instruction limit % 226.75/32.25 % (3736249)Termination phase: Saturation % 226.75/32.25 % (3736249)Time elapsed: 1.958 s % 226.75/32.25 % (3736249)Peak memory usage: 17 MB % 226.75/32.25 % (3736249)Instructions burned: 3774 (million) % 226.75/32.25 % (3736258)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1595921986:i=29340_2932 on theBenchmark for (2932ds/29340Mi) % 226.75/32.25 % TRYING [21] % 226.75/32.25 % TRYING [22] % 226.75/32.25 % TRYING [41] % 226.75/32.25 % TRYING [23] % 226.75/32.25 % TRYING [24] % 226.75/32.25 % TRYING [54] % 226.75/32.25 % TRYING [42] % 226.75/32.25 % TRYING [25] % 226.75/32.25 % TRYING [26] % 226.75/32.25 % TRYING [43] % 226.75/32.25 % TRYING [27] % 226.75/32.25 % TRYING [55] % 226.75/32.25 % (3736256)Instruction limit reached! % 226.75/32.25 % (3736256)------------------------------ % 226.75/32.25 % (3736256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.75/32.25 % (3736256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.75/32.25 % (3736256)CaDiCaL version: 2.1.3 % 226.75/32.25 % (3736256)Termination reason: Instruction limit % 226.75/32.25 % (3736256)Termination phase: Saturation % 226.75/32.25 % (3736256)Time elapsed: 1.170 s % 226.75/32.25 % (3736256)Peak memory usage: 57 MB % 226.75/32.25 % (3736256)Instructions burned: 4594 (million) % 226.75/32.25 % TRYING [44] % 226.75/32.25 % (3736260)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2755188842:i=5211_2924 on theBenchmark for (2924ds/5211Mi) % 226.75/32.25 % TRYING [28] % 226.75/32.25 % TRYING [29] % 226.75/32.25 % TRYING [45] % 226.75/32.25 % TRYING [30] % 226.75/32.25 % TRYING [56] % 226.75/32.25 % TRYING [46] % 226.75/32.25 % TRYING [31] % 226.75/32.25 % TRYING [47] % 226.75/32.25 % TRYING [32] % 226.75/32.25 % TRYING [57] % 226.75/32.25 % TRYING [48] % 226.75/32.25 % TRYING [33] % 226.75/32.25 % (3736260)Instruction limit reached! % 226.75/32.25 % (3736260)------------------------------ % 226.75/32.25 % (3736260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.75/32.25 % (3736260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.75/32.25 % (3736260)CaDiCaL version: 2.1.3 % 226.75/32.25 % (3736260)Termination reason: Instruction limit % 226.75/32.25 % (3736260)Termination phase: Saturation % 226.75/32.25 % (3736260)Time elapsed: 1.410 s % 226.75/32.25 % (3736260)Peak memory usage: 23 MB % 226.75/32.25 % (3736260)Instructions burned: 5212 (million) % 226.75/32.25 % (3736262)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3946546964:i=5497:nm=2_2909 on theBenchmark for (2909ds/5497Mi) % 226.75/32.25 % TRYING [17] % 226.75/32.25 % TRYING [18] % 226.75/32.25 % TRYING [19] % 226.75/32.25 % TRYING [20] % 226.75/32.25 % TRYING [21] % 226.75/32.25 % TRYING [22] % 226.75/32.25 % TRYING [23] % 226.75/32.25 % TRYING [24] % 226.75/32.25 % TRYING [25] % 226.75/32.25 % TRYING [26] % 226.75/32.25 % TRYING [27] % 226.75/32.25 % TRYING [28] % 226.75/32.25 % TRYING [49] % 226.75/32.25 % TRYING [29] % 226.75/32.25 % TRYING [58] % 226.75/32.25 % TRYING [34] % 226.75/32.25 % TRYING [30] % 226.75/32.25 % TRYING [31] % 226.75/32.25 % TRYING [32] % 226.75/32.25 % TRYING [33] % 226.75/32.25 % TRYING [34] % 226.75/32.25 % TRYING [35] % 226.75/32.25 % TRYING [50] % 226.75/32.25 % TRYING [35] % 226.75/32.25 % TRYING [36] % 226.75/32.25 % TRYING [37] % 226.75/32.25 % TRYING [38] % 226.75/32.25 % TRYING [59] % 226.75/32.25 % TRYING [39] % 226.75/32.25 % (3736262)Instruction limit reached! % 226.75/32.25 % (3736262)------------------------------ % 226.75/32.25 % (3736262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.75/32.25 % (3736262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.75/32.25 % (3736262)CaDiCaL version: 2.1.3 % 226.75/32.25 % (3736262)Termination reason: Instruction limit % 226.75/32.25 % (3736262)Termination phase: Finite model building constraint generation % 226.75/32.25 % (3736262)Time elapsed: 1.025 s % 300.52/42.63 % (3736262)Peak memory usage: 43 MB % 300.52/42.63 % (3736262)Instructions burned: 5501 (million) % 300.52/42.63 % (3736264)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3665565903:fmbsr=2:i=46332_2899 on theBenchmark for (2899ds/46332Mi) % 300.52/42.63 % TRYING [15] % 300.52/42.63 % TRYING [16] % 300.52/42.63 % TRYING [17] % 300.52/42.63 % TRYING [18] % 300.52/42.63 % TRYING [51] % 300.52/42.63 % TRYING [19] % 300.52/42.63 % TRYING [20] % 300.52/42.63 % TRYING [21] % 300.52/42.63 % TRYING [22] % 300.52/42.63 % TRYING [36] % 300.52/42.63 % TRYING [23] % 300.52/42.63 % TRYING [24] % 300.52/42.63 % TRYING [25] % 300.52/42.63 % TRYING [26] % 300.52/42.63 % TRYING [27] % 300.52/42.63 % TRYING [28] % 300.52/42.63 % TRYING [29] % 300.52/42.63 % TRYING [30] % 300.52/42.63 % TRYING [31] % 300.52/42.63 % TRYING [52] % 300.52/42.63 % TRYING [32] % 300.52/42.63 % TRYING [33] % 300.52/42.63 % TRYING [60] % 300.52/42.63 % TRYING [37] % 300.52/42.63 % TRYING [34] % 300.52/42.63 % TRYING [35] % 300.52/42.63 % TRYING [36] % 300.52/42.63 % TRYING [37] % 300.52/42.63 % TRYING [53] % 300.52/42.63 % TRYING [38] % 300.52/42.63 % TRYING [38] % 300.52/42.63 % TRYING [39] % 300.52/42.63 % TRYING [40] % 300.52/42.63 % TRYING [61] % 300.52/42.63 % TRYING [41] % 300.52/42.63 % TRYING [54] % 300.52/42.63 % TRYING [42] % 300.52/42.63 % TRYING [39] % 300.52/42.63 % TRYING [43] % 300.52/42.63 % TRYING [44] % 300.52/42.63 % TRYING [55] % 300.52/42.63 % TRYING [45] % 300.52/42.63 % TRYING [62] % 300.52/42.63 % TRYING [46] % 300.52/42.63 % TRYING [40] % 300.52/42.63 % TRYING [47] % 300.52/42.63 % TRYING [56] % 300.52/42.63 % TRYING [48] % 300.52/42.63 % TRYING [63] % 300.52/42.63 % TRYING [49] % 300.52/42.63 % TRYING [41] % 300.52/42.63 % TRYING [57] % 300.52/42.63 % TRYING [50] % 300.52/42.63 % TRYING [51] % 300.52/42.63 % TRYING [64] % 300.52/42.63 % TRYING [58] % 300.52/42.63 % TRYING [52] % 300.52/42.63 % TRYING [42] % 300.52/42.63 % TRYING [53] % 300.52/42.63 % TRYING [59] % 300.52/42.63 % TRYING [54] % 300.52/42.63 % TRYING [65] % 300.52/42.63 % TRYING [43] % 300.52/42.63 % TRYING [55] % 300.52/42.63 % TRYING [60] % 300.52/42.63 % TRYING [56] % 300.52/42.63 % TRYING [66] % 300.52/42.63 % TRYING [44] % 300.52/42.63 % TRYING [57] % 300.52/42.63 % TRYING [61] % 300.52/42.63 % TRYING [58] % 300.52/42.63 % TRYING [59] % 300.52/42.63 % TRYING [67] % 300.52/42.63 % TRYING [45] % 300.52/42.63 % TRYING [62] % 300.52/42.63 % TRYING [60] % 300.52/42.63 % TRYING [61] % 300.52/42.63 % TRYING [63] % 300.52/42.63 % TRYING [68] % 300.52/42.63 % TRYING [46] % 300.52/42.63 % TRYING [62] % 300.52/42.63 % TRYING [64] % 300.52/42.63 % TRYING [63] % 300.52/42.63 % TRYING [69] % 300.52/42.63 % (3736264)Instruction limit reached! % 300.52/42.63 % (3736264)------------------------------ % 300.52/42.63 % (3736264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.52/42.63 % (3736264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.52/42.63 % (3736264)CaDiCaL version: 2.1.3 % 300.52/42.63 % (3736264)Termination reason: Instruction limit % 300.52/42.63 % (3736264)Termination phase: Finite model building constraint generation % 300.52/42.63 % (3736264)Time elapsed: 8.955 s % 300.52/42.63 % (3736264)Peak memory usage: 160 MB % 300.52/42.63 % (3736264)Instructions burned: 46334 (million) % 300.52/42.63 % TRYING [47] % 300.52/42.63 % (3736266)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3108447428:i=14071_2809 on theBenchmark for (2809ds/14071Mi) % 300.52/42.64 % TRYING [12] % 300.52/42.64 % TRYING [13] % 300.52/42.64 % TRYING [14] % 300.52/42.64 % TRYING [15] % 300.52/42.64 % TRYING [16] % 300.52/42.64 % TRYING [17] % 300.52/42.64 % TRYING [18] % 300.52/42.64 % TRYING [19] % 300.52/42.64 % TRYING [20] % 300.52/42.64 % TRYING [21] % 300.52/42.64 % TRYING [22] % 300.52/42.64 % TRYING [23] % 300.52/42.64 % TRYING [24] % 300.52/42.64 % TRYING [25] % 300.52/42.64 % TRYING [26] % 300.52/42.64 % TRYING [27] % 300.52/42.64 % TRYING [65] % 300.52/42.64 % TRYING [28] % 300.52/42.64 % TRYING [29] % 300.52/42.64 % TRYING [30] % 300.52/42.64 % TRYING [31] % 300.52/42.64 % TRYING [32] % 300.52/42.64 % TRYING [33] % 300.52/42.64 % TRYING [34] % 300.52/42.64 % TRYING [35] % 300.52/42.64 % TRYING [70] % 300.52/42.64 % TRYING [36] % 300.52/42.64 % TRYING [37] % 300.52/42.64 % TRYING [38] % 300.52/42.64 % TRYING [39] % 300.52/42.64 % TRYING [40] % 300.52/42.64 % TRYING [66] % 300.52/42.64 % TRYING [48] % 300.52/42.64 % TRYING [41] % 300.52/42.64 % TRYING [42] % 300.52/42.64 % TRYING [43] % 300.52/42.64 % TRYING [44] % 300.52/42.64 % TRYING [71] % 300.52/42.64 % TRYING [45] % 300.52/42.64 % TRYING [46] % 300.52/42.64 % TRYING [67] % 300.52/42.64 % TRYING [47] % 300.52/42.64 % TRYING [48] % 300.52/42.64 % TRYING [49] % 300.52/42.64 % (3736258)Instruction limit reached! % 300.52/42.64 % (3736258)------------------------------ % 300.52/42.64 % (3736258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.52/42.64 % (3736258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.52/42.64 % (3736258)CaDiCaL version: 2.1.3 % 300.52/42.64 % (3736258)Termination reason: Instruction limit % 300.52/42.64 % (3736258)Termination phase: Saturation % 300.52/42.64 % (3736258)Time elapsed: 15.025 s % 300.52/42.64 % (3736258)Peak memory usage: 55 MB % 300.52/42.64 % (3736258)Instructions burned: 29342 (million) % 300.52/42.64 % (3736266)Instruction limit reached! % 300.52/42.64 % (3736266)------------------------------ % 300.52/42.64 % (3736266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.52/42.64 % (3736266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.52/42.64 % (3736266)CaDiCaL version: 2.1.3 % 300.52/42.64 % (3736266)Termination reason: Instruction limit % 300.52/42.64 % (3736266)Termination phase: Finite model building constraint generation % 300.52/42.64 % (3736266)Time elapsed: 2.725 s % 300.52/42.64 % (3736266)Peak memory usage: 81 MB % 300.52/42.64 % (3736266)Instructions burned: 14076 (million) % 300.52/42.64 % (3736268)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3585943516:i=22565:add=on:rawr=on_2782 on theBenchmark for (2782ds/22565Mi) % 300.52/42.64 % (3736269)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2851701990:i=8173:av=off % 300.52/42.64 Terminated % 300.52/42.64 % Vampire exiting % 300.52/42.64 Terminated %------------------------------------------------------------------------------