%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW463-1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n010.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:40:03 PM UTC 2026 % Result : Timeout 303.49s 43.06s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW463-1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.21 % Computer : n010.cluster.edu % 0.09/0.21 % Model : x86_64 x86_64 % 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.21 % Memory : 8046.5625MB % 0.09/0.21 % OS : Linux 6.8.0-71-generic % 0.09/0.21 % CPULimit : 300 % 0.09/0.21 % WCLimit : 300 % 0.09/0.21 % DateTime : Mon Sep 28 13:59:47 UTC 2026 % 0.09/0.21 % CPUTime : % 0.09/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.24 Running first-order model finding % 0.09/0.24 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 % 23.81/3.67 % (1935891)Will run a generic schedule for satisfiability detection. % 23.81/3.67 % (1935896)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3596697807_2999 on theBenchmark for (2999ds/0Mi) % 23.81/3.67 % TRYING [1] % 23.81/3.67 % TRYING [2] % 23.81/3.67 % (1935897)% WARNING: option uhcvi not known. % 23.81/3.67 % TRYING [3] % 23.81/3.67 % (1935901)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1263602590:i=131_2999 on theBenchmark for (2999ds/131Mi) % 23.81/3.67 % (1935897)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=284352930:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 23.81/3.67 % (1935898)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3588222258:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 23.81/3.67 % (1935899)dis+10_1_sil=32000:sp=arity:random_seed=256970503:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 23.81/3.67 % (1935900)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3726514149:i=116_2999 on theBenchmark for (2999ds/116Mi) % 23.81/3.67 % (1935902)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4240582265:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 23.81/3.67 % TRYING [4] % 23.81/3.67 % (1935900)Instruction limit reached! % 23.81/3.67 % (1935900)------------------------------ % 23.81/3.67 % (1935900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.81/3.67 % (1935900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.81/3.67 % (1935900)CaDiCaL version: 2.1.3 % 23.81/3.67 % (1935900)Termination reason: Instruction limit % 23.81/3.67 % (1935900)Termination phase: Saturation % 23.81/3.67 % (1935900)Time elapsed: 0.053 s % 23.81/3.67 % (1935900)Peak memory usage: 12 MB % 23.81/3.67 % (1935900)Instructions burned: 118 (million) % 23.81/3.67 % (1935899)Instruction limit reached! % 23.81/3.67 % (1935899)------------------------------ % 23.81/3.67 % (1935899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.81/3.67 % (1935899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.81/3.67 % (1935899)CaDiCaL version: 2.1.3 % 23.81/3.67 % (1935899)Termination reason: Instruction limit % 23.81/3.67 % (1935899)Termination phase: Saturation % 23.81/3.67 % (1935899)Time elapsed: 0.059 s % 23.81/3.67 % (1935899)Peak memory usage: 11 MB % 23.81/3.67 % (1935899)Instructions burned: 103 (million) % 23.81/3.67 % (1935901)Instruction limit reached! % 23.81/3.67 % (1935901)------------------------------ % 23.81/3.67 % (1935901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.81/3.67 % (1935901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.81/3.67 % (1935901)CaDiCaL version: 2.1.3 % 23.81/3.67 % (1935901)Termination reason: Instruction limit % 23.81/3.67 % (1935901)Termination phase: Saturation % 23.81/3.67 % (1935901)Time elapsed: 0.060 s % 23.81/3.67 % (1935901)Peak memory usage: 12 MB % 23.81/3.67 % (1935901)Instructions burned: 139 (million) % 23.81/3.67 % (1935910)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3201052904:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 23.81/3.67 % (1935912)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=2480050875:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 23.81/3.67 % (1935911)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3463661421:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 23.81/3.67 % TRYING [1] % 23.81/3.67 % TRYING [2] % 23.81/3.67 % (1935902)Instruction limit reached! % 23.81/3.67 % (1935902)------------------------------ % 23.81/3.67 % (1935902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.81/3.67 % (1935902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.81/3.67 % (1935902)CaDiCaL version: 2.1.3 % 23.81/3.67 % (1935902)Termination reason: Instruction limit % 23.81/3.67 % (1935902)Termination phase: Saturation % 23.81/3.67 % (1935902)Time elapsed: 0.080 s % 23.81/3.67 % (1935902)Peak memory usage: 12 MB % 23.81/3.67 % (1935902)Instructions burned: 159 (million) % 23.81/3.67 % TRYING [5] % 23.81/3.67 % TRYING [3] % 23.81/3.67 % (1935916)ott-21_1_sil=16000:fs=off:random_seed=2702945780:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 23.81/3.67 % (1935911)Instruction limit reached! % 23.81/3.67 % (1935911)------------------------------ % 23.81/3.67 % (1935911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.81/3.67 % (1935911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.59/6.74 % (1935911)CaDiCaL version: 2.1.3 % 45.59/6.74 % (1935911)Termination reason: Instruction limit % 45.59/6.74 % (1935911)Termination phase: Saturation % 45.59/6.74 % (1935911)Time elapsed: 0.062 s % 45.59/6.74 % (1935911)Peak memory usage: 12 MB % 45.59/6.74 % (1935911)Instructions burned: 133 (million) % 45.59/6.74 % TRYING [4] % 45.59/6.74 % (1935918)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3847967516:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 45.59/6.74 % (1935916)Instruction limit reached! % 45.59/6.74 % (1935916)------------------------------ % 45.59/6.74 % (1935916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.59/6.74 % (1935916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.59/6.74 % (1935916)CaDiCaL version: 2.1.3 % 45.59/6.74 % (1935916)Termination reason: Instruction limit % 45.59/6.74 % (1935916)Termination phase: Saturation % 45.59/6.74 % (1935916)Time elapsed: 0.076 s % 45.59/6.74 % (1935916)Peak memory usage: 11 MB % 45.59/6.74 % (1935916)Instructions burned: 182 (million) % 45.59/6.74 % (1935920)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=988227758:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 45.59/6.74 % TRYING [1] % 45.59/6.74 % TRYING [2] % 45.59/6.74 % TRYING [3] % 45.59/6.74 % TRYING [4] % 45.59/6.74 % (1935912)Instruction limit reached! % 45.59/6.74 % (1935912)------------------------------ % 45.59/6.74 % (1935912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.59/6.74 % (1935912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.59/6.74 % (1935912)CaDiCaL version: 2.1.3 % 45.59/6.74 % (1935912)Termination reason: Instruction limit % 45.59/6.74 % (1935912)Termination phase: Saturation % 45.59/6.74 % (1935912)Time elapsed: 0.313 s % 45.59/6.74 % (1935912)Peak memory usage: 14 MB % 45.59/6.74 % (1935912)Instructions burned: 685 (million) % 45.59/6.74 % (1935918)Instruction limit reached! % 45.59/6.74 % (1935918)------------------------------ % 45.59/6.74 % (1935918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.59/6.74 % (1935918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.59/6.74 % (1935918)CaDiCaL version: 2.1.3 % 45.59/6.74 % (1935918)Termination reason: Instruction limit % 45.59/6.74 % (1935918)Termination phase: Saturation % 45.59/6.74 % (1935918)Time elapsed: 0.234 s % 45.59/6.74 % (1935918)Peak memory usage: 13 MB % 45.59/6.74 % (1935918)Instructions burned: 478 (million) % 45.59/6.74 % (1935922)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3327030486:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 45.59/6.74 % (1935923)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4133019654:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 45.59/6.74 % TRYING [5] % 45.59/6.74 % (1935910)Instruction limit reached! % 45.59/6.74 % (1935910)------------------------------ % 45.59/6.74 % (1935910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.59/6.74 % (1935910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.59/6.74 % (1935910)CaDiCaL version: 2.1.3 % 45.59/6.74 % (1935910)Termination reason: Instruction limit % 45.59/6.74 % (1935910)Termination phase: Finite model building SAT solving % 45.59/6.74 % (1935910)Time elapsed: 0.417 s % 45.59/6.74 % (1935910)Peak memory usage: 19 MB % 45.59/6.74 % (1935910)Instructions burned: 714 (million) % 45.59/6.74 % (1935926)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=4138957954:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi) % 45.59/6.74 % (1935920)Instruction limit reached! % 45.59/6.74 % (1935920)------------------------------ % 45.59/6.74 % (1935920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.59/6.74 % (1935920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.59/6.74 % (1935920)CaDiCaL version: 2.1.3 % 45.59/6.74 % (1935920)Termination reason: Instruction limit % 45.59/6.74 % (1935920)Termination phase: Finite model building SAT solving % 45.59/6.74 % (1935920)Time elapsed: 0.368 s % 45.59/6.74 % (1935920)Peak memory usage: 23 MB % 45.59/6.74 % (1935920)Instructions burned: 867 (million) % 45.59/6.74 % (1935928)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=610853552:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 45.59/6.74 % TRYING [14] % 45.59/6.74 % TRYING [6] % 45.59/6.74 % (1935923)Instruction limit reached! % 45.59/6.74 % (1935923)------------------------------ % 113.87/16.32 % (1935923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.87/16.32 % (1935923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.87/16.32 % (1935923)CaDiCaL version: 2.1.3 % 113.87/16.32 % (1935923)Termination reason: Instruction limit % 113.87/16.32 % (1935923)Termination phase: Finite model building constraint generation % 113.87/16.32 % (1935923)Time elapsed: 0.367 s % 113.87/16.32 % (1935923)Peak memory usage: 91 MB % 113.87/16.32 % (1935923)Instructions burned: 891 (million) % 113.87/16.32 % (1935926)Instruction limit reached! % 113.87/16.32 % (1935926)------------------------------ % 113.87/16.32 % (1935926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.87/16.32 % (1935926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.87/16.32 % (1935926)CaDiCaL version: 2.1.3 % 113.87/16.32 % (1935926)Termination reason: Instruction limit % 113.87/16.32 % (1935926)Termination phase: Saturation % 113.87/16.32 % (1935926)Time elapsed: 0.273 s % 113.87/16.32 % (1935926)Peak memory usage: 13 MB % 113.87/16.32 % (1935926)Instructions burned: 693 (million) % 113.87/16.32 % (1935930)fmb+10_1_sil=64000:random_seed=744171160:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi) % 113.87/16.32 % TRYING [1] % 113.87/16.32 % TRYING [2] % 113.87/16.32 % (1935931)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3611029151:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi) % 113.87/16.32 % TRYING [20] % 113.87/16.32 % TRYING [3] % 113.87/16.32 % TRYING [4] % 113.87/16.32 % (1935922)Instruction limit reached! % 113.87/16.32 % (1935922)------------------------------ % 113.87/16.32 % (1935922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.87/16.32 % (1935922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.87/16.32 % (1935922)CaDiCaL version: 2.1.3 % 113.87/16.32 % (1935922)Termination reason: Instruction limit % 113.87/16.32 % (1935922)Termination phase: Saturation % 113.87/16.32 % (1935922)Time elapsed: 0.500 s % 113.87/16.32 % (1935922)Peak memory usage: 21 MB % 113.87/16.32 % (1935922)Instructions burned: 1180 (million) % 113.87/16.32 % (1935934)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1301851908:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 113.87/16.32 % TRYING [8] % 113.87/16.32 % (1935928)Instruction limit reached! % 113.87/16.32 % (1935928)------------------------------ % 113.87/16.32 % (1935928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.87/16.32 % (1935928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.87/16.32 % (1935928)CaDiCaL version: 2.1.3 % 113.87/16.32 % (1935928)Termination reason: Instruction limit % 113.87/16.32 % (1935928)Termination phase: Saturation % 113.87/16.32 % (1935928)Time elapsed: 0.448 s % 113.87/16.32 % (1935928)Peak memory usage: 17 MB % 113.87/16.32 % (1935928)Instructions burned: 881 (million) % 113.87/16.32 % (1935936)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2802105347:i=5131_2989 on theBenchmark for (2989ds/5131Mi) % 113.87/16.32 % (1935934)Instruction limit reached! % 113.87/16.32 % (1935934)------------------------------ % 113.87/16.32 % (1935934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.87/16.32 % (1935934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.87/16.32 % (1935934)CaDiCaL version: 2.1.3 % 113.87/16.32 % (1935934)Termination reason: Instruction limit % 113.87/16.32 % (1935934)Termination phase: Finite model building constraint generation % 113.87/16.32 % (1935934)Time elapsed: 0.351 s % 113.87/16.32 % (1935934)Peak memory usage: 74 MB % 113.87/16.32 % (1935934)Instructions burned: 921 (million) % 113.87/16.32 % (1935938)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=448778739:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi) % 113.87/16.32 % (1935938)Instruction limit reached! % 113.87/16.32 % (1935938)------------------------------ % 113.87/16.32 % (1935938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.87/16.32 % (1935938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.87/16.32 % (1935938)CaDiCaL version: 2.1.3 % 113.87/16.32 % (1935938)Termination reason: Instruction limit % 113.87/16.32 % (1935938)Termination phase: Saturation % 113.87/16.32 % (1935938)Time elapsed: 0.645 s % 113.87/16.32 % (1935938)Peak memory usage: 22 MB % 113.87/16.32 % (1935938)Instructions burned: 1472 (million) % 113.87/16.32 % (1935940)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3902400280:i=6324_2980 on theBenchmark for (2980ds/6324Mi) % 113.87/16.32 % TRYING [77] % 113.87/16.32 % (1935936)Instruction limit reached! % 113.87/16.32 % (1935936)------------------------------ % 303.49/43.06 % (1935936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.49/43.06 % (1935936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.49/43.06 % (1935936)CaDiCaL version: 2.1.3 % 303.49/43.06 % (1935936)Termination reason: Instruction limit % 303.49/43.06 % (1935936)Termination phase: Saturation % 303.49/43.06 % (1935936)Time elapsed: 2.328 s % 303.49/43.06 % (1935936)Peak memory usage: 34 MB % 303.49/43.06 % (1935936)Instructions burned: 5133 (million) % 303.49/43.06 % (1935942)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1185475968:fmbsr=2.30978:i=2174_2965 on theBenchmark for (2965ds/2174Mi) % 303.49/43.06 % TRYING [16] % 303.49/43.06 % (1935942)Instruction limit reached! % 303.49/43.06 % (1935942)------------------------------ % 303.49/43.06 % (1935942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.49/43.06 % (1935942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.49/43.06 % (1935942)CaDiCaL version: 2.1.3 % 303.49/43.06 % (1935942)Termination reason: Instruction limit % 303.49/43.06 % (1935942)Termination phase: Finite model building constraint generation % 303.49/43.06 % (1935942)Time elapsed: 0.745 s % 303.49/43.06 % (1935942)Peak memory usage: 136 MB % 303.49/43.06 % (1935942)Instructions burned: 2174 (million) % 303.49/43.06 % (1935944)ott-2_1_sil=16000:newcnf=on:random_seed=3184740916:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi) % 303.49/43.06 % (1935931)Instruction limit reached! % 303.49/43.06 % (1935931)------------------------------ % 303.49/43.06 % (1935931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.49/43.06 % (1935931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.49/43.06 % (1935931)CaDiCaL version: 2.1.3 % 303.49/43.06 % (1935931)Termination reason: Instruction limit % 303.49/43.06 % (1935931)Termination phase: Finite model building constraint generation % 303.49/43.06 % (1935931)Time elapsed: 3.404 s % 303.49/43.06 % (1935931)Peak memory usage: 666 MB % 303.49/43.06 % (1935931)Instructions burned: 9516 (million) % 303.49/43.06 % (1935940)Instruction limit reached! % 303.49/43.06 % (1935940)------------------------------ % 303.49/43.06 % (1935940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.49/43.06 % (1935940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.49/43.06 % (1935940)CaDiCaL version: 2.1.3 % 303.49/43.06 % (1935940)Termination reason: Instruction limit % 303.49/43.06 % (1935940)Termination phase: Finite model building constraint generation % 303.49/43.06 % (1935940)Time elapsed: 2.245 s % 303.49/43.06 % (1935940)Peak memory usage: 457 MB % 303.49/43.06 % (1935940)Instructions burned: 6327 (million) % 303.49/43.06 % (1935946)ott+10_1_sil=32000:tgt=ground:random_seed=3166188572:i=5114:av=off_2956 on theBenchmark for (2956ds/5114Mi) % 303.49/43.06 % (1935947)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2270660717:i=54282_2956 on theBenchmark for (2956ds/54282Mi) % 303.49/43.06 % TRYING [1] % 303.49/43.06 % TRYING [2] % 303.49/43.06 % TRYING [3] % 303.49/43.06 % TRYING [4] % 303.49/43.06 % TRYING [5] % 303.49/43.06 % (1935944)Instruction limit reached! % 303.49/43.06 % (1935944)------------------------------ % 303.49/43.06 % (1935944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.49/43.06 % (1935944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.49/43.06 % (1935944)CaDiCaL version: 2.1.3 % 303.49/43.06 % (1935944)Termination reason: Instruction limit % 303.49/43.06 % (1935944)Termination phase: Saturation % 303.49/43.06 % (1935944)Time elapsed: 0.352 s % 303.49/43.06 % (1935944)Peak memory usage: 14 MB % 303.49/43.06 % (1935944)Instructions burned: 871 (million) % 303.49/43.06 % (1935950)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3125539875:i=3512:aac=none_2954 on theBenchmark for (2954ds/3512Mi) % 303.49/43.06 % TRYING [5] % 303.49/43.06 % TRYING [6] % 303.49/43.06 % TRYING [6] % 303.49/43.06 % (1935950)Instruction limit reached! % 303.49/43.06 % (1935950)------------------------------ % 303.49/43.06 % (1935950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.49/43.06 % (1935950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.49/43.06 % (1935950)CaDiCaL version: 2.1.3 % 303.49/43.06 % (1935950)Termination reason: Instruction limit % 303.49/43.06 % (1935950)Termination phase: Saturation % 303.49/43.06 % (1935950)Time elapsed: 1.653 s % 303.49/43.06 % (1935950)Peak memory usage: 27 MB % 303.49/43.06 % (1935950)Instructions burned: 3514 (million) % 303.49/43.06 % (1935952)dis+21_1_sil=32000:sas=cadical:random_seed=826364830:i=3773:amm=off_2937 on theBenchmark for (2937ds/3773Mi) % 303.49/43.06 %Terminated % 303.49/43.07 % Vampire exiting %------------------------------------------------------------------------------