%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV651-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n019.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:26:11 PM UTC 2026 % Result : Timeout 296.73s 42.23s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV651-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.23 % Computer : n019.cluster.edu % 0.08/0.23 % Model : x86_64 x86_64 % 0.08/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.23 % Memory : 8046.5625MB % 0.08/0.23 % OS : Linux 6.8.0-71-generic % 0.08/0.23 % CPULimit : 300 % 0.08/0.23 % WCLimit : 300 % 0.08/0.23 % DateTime : Mon Sep 28 12:09:33 UTC 2026 % 0.08/0.23 % CPUTime : % 0.08/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.24/0.28 Running first-order model finding % 0.24/0.28 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 % 26.66/4.19 % (3961314)Will run a generic schedule for satisfiability detection. % 26.66/4.19 % (3961320)% WARNING: option uhcvi not known. % 26.66/4.19 % (3961320)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2647473699:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi) % 26.66/4.19 % (3961319)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1678295195_2998 on theBenchmark for (2998ds/0Mi) % 26.66/4.19 % (3961322)dis+10_1_sil=32000:sp=arity:random_seed=3176247080:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi) % 26.66/4.19 % (3961324)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2843040277:i=131_2998 on theBenchmark for (2998ds/131Mi) % 26.66/4.19 % (3961323)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=263571877:i=116_2998 on theBenchmark for (2998ds/116Mi) % 26.66/4.19 % (3961321)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1299470632:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi) % 26.66/4.19 % (3961325)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2138648943:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi) % 26.66/4.19 % (3961322)Instruction limit reached! % 26.66/4.19 % (3961322)------------------------------ % 26.66/4.19 % (3961322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.66/4.19 % (3961322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.66/4.19 % (3961322)CaDiCaL version: 2.1.3 % 26.66/4.19 % (3961322)Termination reason: Instruction limit % 26.66/4.19 % (3961322)Termination phase: Saturation % 26.66/4.19 % (3961322)Time elapsed: 0.107 s % 26.66/4.19 % (3961322)Peak memory usage: 14 MB % 26.66/4.19 % (3961322)Instructions burned: 103 (million) % 26.66/4.19 % (3961323)Instruction limit reached! % 26.66/4.19 % (3961323)------------------------------ % 26.66/4.19 % (3961323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.66/4.19 % (3961323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.66/4.19 % (3961323)CaDiCaL version: 2.1.3 % 26.66/4.19 % (3961323)Termination reason: Instruction limit % 26.66/4.19 % (3961323)Termination phase: Saturation % 26.66/4.19 % (3961323)Time elapsed: 0.112 s % 26.66/4.19 % (3961323)Peak memory usage: 14 MB % 26.66/4.19 % (3961323)Instructions burned: 116 (million) % 26.66/4.19 % (3961324)Instruction limit reached! % 26.66/4.19 % (3961324)------------------------------ % 26.66/4.19 % (3961324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.66/4.19 % (3961324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.66/4.19 % (3961324)CaDiCaL version: 2.1.3 % 26.66/4.19 % (3961324)Termination reason: Instruction limit % 26.66/4.19 % (3961324)Termination phase: Saturation % 26.66/4.19 % (3961324)Time elapsed: 0.133 s % 26.66/4.19 % (3961324)Peak memory usage: 14 MB % 26.66/4.19 % (3961324)Instructions burned: 131 (million) % 26.66/4.19 % (3961333)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2854402607:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi) % 26.66/4.19 % (3961334)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2054594252:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi) % 26.66/4.19 % (3961325)Instruction limit reached! % 26.66/4.19 % (3961325)------------------------------ % 26.66/4.19 % (3961325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.66/4.19 % (3961325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.66/4.19 % (3961325)CaDiCaL version: 2.1.3 % 26.66/4.19 % (3961325)Termination reason: Instruction limit % 26.66/4.19 % (3961325)Termination phase: Saturation % 26.66/4.19 % (3961325)Time elapsed: 0.170 s % 26.66/4.19 % (3961325)Peak memory usage: 16 MB % 26.66/4.19 % (3961325)Instructions burned: 160 (million) % 26.66/4.19 % (3961335)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=1944844316:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi) % 26.66/4.19 % (3961339)ott-21_1_sil=16000:fs=off:random_seed=2823812682:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi) % 26.66/4.19 % (3961334)Instruction limit reached! % 26.66/4.19 % (3961334)------------------------------ % 26.66/4.19 % (3961334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.66/4.19 % (3961334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.66/4.19 % (3961334)CaDiCaL version: 2.1.3 % 73.48/10.84 % (3961334)Termination reason: Instruction limit % 73.48/10.84 % (3961334)Termination phase: Saturation % 73.48/10.84 % (3961334)Time elapsed: 0.129 s % 73.48/10.84 % (3961334)Peak memory usage: 14 MB % 73.48/10.84 % (3961334)Instructions burned: 132 (million) % 73.48/10.84 % (3961339)Instruction limit reached! % 73.48/10.84 % (3961339)------------------------------ % 73.48/10.84 % (3961339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.48/10.84 % (3961339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.48/10.84 % (3961339)CaDiCaL version: 2.1.3 % 73.48/10.84 % (3961339)Termination reason: Instruction limit % 73.48/10.84 % (3961339)Termination phase: Saturation % 73.48/10.84 % (3961339)Time elapsed: 0.109 s % 73.48/10.84 % (3961339)Peak memory usage: 14 MB % 73.48/10.84 % (3961339)Instructions burned: 180 (million) % 73.48/10.84 % (3961343)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1587903562:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi) % 73.48/10.84 % (3961344)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=877309373:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi) % 73.48/10.84 % (3961333)Instruction limit reached! % 73.48/10.84 % (3961333)------------------------------ % 73.48/10.84 % (3961333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.48/10.84 % (3961333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.48/10.84 % (3961333)CaDiCaL version: 2.1.3 % 73.48/10.84 % (3961333)Termination reason: Instruction limit % 73.48/10.84 % (3961333)Termination phase: Finite model building preprocessing % 73.48/10.84 % (3961333)Time elapsed: 0.628 s % 73.48/10.84 % (3961333)Peak memory usage: 21 MB % 73.48/10.84 % (3961333)Instructions burned: 714 (million) % 73.48/10.84 % (3961343)Instruction limit reached! % 73.48/10.84 % (3961343)------------------------------ % 73.48/10.84 % (3961343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.48/10.84 % (3961343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.48/10.84 % (3961343)CaDiCaL version: 2.1.3 % 73.48/10.84 % (3961343)Termination reason: Instruction limit % 73.48/10.84 % (3961343)Termination phase: Saturation % 73.48/10.84 % (3961343)Time elapsed: 0.493 s % 73.48/10.84 % (3961343)Peak memory usage: 16 MB % 73.48/10.84 % (3961343)Instructions burned: 477 (million) % 73.48/10.85 % (3961347)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1426286418:i=1179_2990 on theBenchmark for (2990ds/1179Mi) % 73.48/10.85 % (3961348)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1631420331:i=889:ins=1_2990 on theBenchmark for (2990ds/889Mi) % 73.48/10.85 % (3961335)Instruction limit reached! % 73.48/10.85 % (3961335)------------------------------ % 73.48/10.85 % (3961335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.48/10.85 % (3961335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.48/10.85 % (3961335)CaDiCaL version: 2.1.3 % 73.48/10.85 % (3961335)Termination reason: Instruction limit % 73.48/10.85 % (3961335)Termination phase: Saturation % 73.48/10.85 % (3961335)Time elapsed: 0.698 s % 73.48/10.85 % (3961335)Peak memory usage: 18 MB % 73.48/10.85 % (3961335)Instructions burned: 685 (million) % 73.48/10.85 % (3961351)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=3807022700:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2989 on theBenchmark for (2989ds/692Mi) % 73.48/10.85 % TRYING [1] % 73.48/10.85 % TRYING [2] % 73.48/10.85 % (3961344)Instruction limit reached! % 73.48/10.85 % (3961344)------------------------------ % 73.48/10.85 % (3961344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.48/10.85 % (3961344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.48/10.85 % (3961344)CaDiCaL version: 2.1.3 % 73.48/10.85 % (3961344)Termination reason: Instruction limit % 73.48/10.85 % (3961344)Termination phase: Finite model building preprocessing % 73.48/10.85 % (3961344)Time elapsed: 0.751 s % 73.48/10.85 % (3961344)Peak memory usage: 25 MB % 73.48/10.85 % (3961344)Instructions burned: 865 (million) % 73.48/10.85 % (3961355)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1167187103:i=879:kws=inv_precedence:fsr=off_2987 on theBenchmark for (2987ds/879Mi) % 73.48/10.85 % (3961351)Instruction limit reached! % 73.48/10.85 % (3961351)------------------------------ % 73.48/10.85 % (3961351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.48/10.85 % (3961351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.35/24.96 % (3961351)CaDiCaL version: 2.1.3 % 173.35/24.96 % (3961351)Termination reason: Instruction limit % 173.35/24.96 % (3961351)Termination phase: Saturation % 173.35/24.96 % (3961351)Time elapsed: 0.738 s % 173.35/24.96 % (3961351)Peak memory usage: 20 MB % 173.35/24.96 % (3961351)Instructions burned: 692 (million) % 173.35/24.96 % (3961348)Instruction limit reached! % 173.35/24.96 % (3961348)------------------------------ % 173.35/24.96 % (3961348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.35/24.96 % (3961348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.35/24.96 % (3961348)CaDiCaL version: 2.1.3 % 173.35/24.96 % (3961348)Termination reason: Instruction limit % 173.35/24.96 % (3961348)Termination phase: Finite model building preprocessing % 173.35/24.96 % (3961348)Time elapsed: 0.819 s % 173.35/24.96 % (3961348)Peak memory usage: 28 MB % 173.35/24.96 % (3961348)Instructions burned: 889 (million) % 173.35/24.96 % TRYING [3] % 173.35/24.96 % (3961357)fmb+10_1_sil=64000:random_seed=3961740946:i=22061:nm=2:gsp=on_2981 on theBenchmark for (2981ds/22061Mi) % 173.35/24.96 % (3961358)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2229976387:i=9515:nm=5_2981 on theBenchmark for (2981ds/9515Mi) % 173.35/24.96 % (3961355)Instruction limit reached! % 173.35/24.96 % (3961355)------------------------------ % 173.35/24.96 % (3961355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.35/24.96 % (3961355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.35/24.96 % (3961355)CaDiCaL version: 2.1.3 % 173.35/24.96 % (3961355)Termination reason: Instruction limit % 173.35/24.96 % (3961355)Termination phase: Saturation % 173.35/24.96 % (3961355)Time elapsed: 0.760 s % 173.35/24.96 % (3961355)Peak memory usage: 20 MB % 173.35/24.96 % (3961355)Instructions burned: 879 (million) % 173.35/24.96 % (3961361)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=922110078:fmbsr=1.7:i=920_2979 on theBenchmark for (2979ds/920Mi) % 173.35/24.96 % (3961347)Instruction limit reached! % 173.35/24.96 % (3961347)------------------------------ % 173.35/24.96 % (3961347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.35/24.96 % (3961347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.35/24.96 % (3961347)CaDiCaL version: 2.1.3 % 173.35/24.96 % (3961347)Termination reason: Instruction limit % 173.35/24.96 % (3961347)Termination phase: Saturation % 173.35/24.96 % (3961347)Time elapsed: 1.184 s % 173.35/24.96 % (3961347)Peak memory usage: 23 MB % 173.35/24.96 % (3961347)Instructions burned: 1179 (million) % 173.35/24.96 % (3961363)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3391731093:i=5131_2978 on theBenchmark for (2978ds/5131Mi) % 173.35/24.96 % (3961358)Cannot represent all propositional literals internally % 173.35/24.96 % (3961358)Refutation not found, incomplete strategy % 173.35/24.96 % (3961358)------------------------------ % 173.35/24.96 % (3961358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.35/24.96 % (3961358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.35/24.96 % (3961358)CaDiCaL version: 2.1.3 % 173.35/24.96 % (3961358)Termination reason: Refutation not found, incomplete strategy % 173.35/24.96 % (3961358)Time elapsed: 0.982 s % 173.35/24.96 % (3961358)Peak memory usage: 29 MB % 173.35/24.96 % (3961358)Instructions burned: 1093 (million) % 173.35/24.96 % (3961358)------------------------------ % 173.35/24.96 % (3961358)------------------------------ % 173.35/24.96 % TRYING [1] % 173.35/24.96 % (3961365)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1022131914:i=1472:ins=7:fdi=8:gsp=on_2971 on theBenchmark for (2971ds/1472Mi) % 173.35/24.96 % (3961361)Instruction limit reached! % 173.35/24.96 % (3961361)------------------------------ % 173.35/24.96 % (3961361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.35/24.96 % (3961361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.35/24.96 % (3961361)CaDiCaL version: 2.1.3 % 173.35/24.96 % (3961361)Termination reason: Instruction limit % 173.35/24.96 % (3961361)Termination phase: Finite model building preprocessing % 173.35/24.96 % (3961361)Time elapsed: 0.835 s % 173.35/24.96 % (3961361)Peak memory usage: 29 MB % 173.35/24.96 % (3961361)Instructions burned: 921 (million) % 173.35/24.96 % (3961367)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1024324858:i=6324_2970 on theBenchmark for (2970ds/6324Mi) % 173.35/24.96 % TRYING [2] % 173.35/24.96 % (3961367)Cannot represent all propositional literals internally % 173.35/24.96 % (3961367)Refutation not found, incomplete strategy % 173.35/24.96 % (3961367)------------------------------ % 296.73/42.23 % (3961367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.73/42.23 % (3961367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.73/42.23 % (3961367)CaDiCaL version: 2.1.3 % 296.73/42.23 % (3961367)Termination reason: Refutation not found, incomplete strategy % 296.73/42.23 % (3961367)Time elapsed: 0.943 s % 296.73/42.23 % (3961367)Peak memory usage: 30 MB % 296.73/42.23 % (3961367)Instructions burned: 1140 (million) % 296.73/42.23 % (3961367)------------------------------ % 296.73/42.23 % (3961367)------------------------------ % 296.73/42.23 % (3961369)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=841628796:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi) % 296.73/42.23 % (3961365)Instruction limit reached! % 296.73/42.23 % (3961365)------------------------------ % 296.73/42.23 % (3961365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.73/42.23 % (3961365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.73/42.23 % (3961365)CaDiCaL version: 2.1.3 % 296.73/42.23 % (3961365)Termination reason: Instruction limit % 296.73/42.23 % (3961365)Termination phase: Saturation % 296.73/42.23 % (3961365)Time elapsed: 1.399 s % 296.73/42.23 % (3961365)Peak memory usage: 27 MB % 296.73/42.23 % (3961365)Instructions burned: 1472 (million) % 296.73/42.23 % (3961371)ott-2_1_sil=16000:newcnf=on:random_seed=1693195258:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi) % 296.73/42.23 % (3961371)Instruction limit reached! % 296.73/42.23 % (3961371)------------------------------ % 296.73/42.23 % (3961371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.73/42.23 % (3961371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.73/42.23 % (3961371)CaDiCaL version: 2.1.3 % 296.73/42.23 % (3961371)Termination reason: Instruction limit % 296.73/42.23 % (3961371)Termination phase: Saturation % 296.73/42.23 % (3961371)Time elapsed: 0.894 s % 296.73/42.23 % (3961371)Peak memory usage: 20 MB % 296.73/42.23 % (3961371)Instructions burned: 869 (million) % 296.73/42.23 % (3961373)ott+10_1_sil=32000:tgt=ground:random_seed=2160513192:i=5114:av=off_2947 on theBenchmark for (2947ds/5114Mi) % 296.73/42.23 % TRYING [3] % 296.73/42.23 % (3961369)Instruction limit reached! % 296.73/42.23 % (3961369)------------------------------ % 296.73/42.23 % (3961369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.73/42.23 % (3961369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.73/42.23 % (3961369)CaDiCaL version: 2.1.3 % 296.73/42.23 % (3961369)Termination reason: Instruction limit % 296.73/42.23 % (3961369)Termination phase: Finite model building preprocessing % 296.73/42.23 % (3961369)Time elapsed: 1.888 s % 296.73/42.23 % (3961369)Peak memory usage: 31 MB % 296.73/42.23 % (3961369)Instructions burned: 2174 (million) % 296.73/42.23 % (3961375)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2160976403:i=54282_2941 on theBenchmark for (2941ds/54282Mi) % 296.73/42.23 % TRYING [4] % 296.73/42.23 % TRYING [1] % 296.73/42.23 % TRYING [2] % 296.73/42.23 % (3961363)Instruction limit reached! % 296.73/42.23 % (3961363)------------------------------ % 296.73/42.23 % (3961363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.73/42.23 % (3961363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.73/42.23 % (3961363)CaDiCaL version: 2.1.3 % 296.73/42.23 % (3961363)Termination reason: Instruction limit % 296.73/42.23 % (3961363)Termination phase: Saturation % 296.73/42.23 % (3961363)Time elapsed: 4.763 s % 296.73/42.23 % (3961363)Peak memory usage: 41 MB % 296.73/42.23 % (3961363)Instructions burned: 5131 (million) % 296.73/42.23 % (3961377)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=357165869:i=3512:aac=none_2930 on theBenchmark for (2930ds/3512Mi) % 296.73/42.23 % TRYING [3] % 296.73/42.23 % (3961377)Instruction limit reached! % 296.73/42.23 % (3961377)------------------------------ % 296.73/42.23 % (3961377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.73/42.23 % (3961377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.73/42.23 % (3961377)CaDiCaL version: 2.1.3 % 296.73/42.23 % (3961377)Termination reason: Instruction limit % 296.73/42.23 % (3961377)Termination phase: Saturation % 296.73/42.23 % (3961377)Time elapsed: 3.196 s % 296.73/42.23 % (3961377)Peak memory usage: 34 MB % 296.73/42.23 % (3961377)Instructions burned: 3512 (million) % 296.73/42.23 % (3961379)dis+21_1_sil=32000:sas=cadical:random_seed=2128099404:i=3773:amm=off_2897 on theBenchmark for (2897ds/3773Mi) % 296.73/42.23 % (3961373)Instruction limit reached! % 296.73/42.23 % (3961373)------------------------------ % 296.73/42.23 % (3961373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.83 % (3961373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.83 % (3961373)CaDiCaL version: 2.1.3 % 300.42/42.83 % (3961373)Termination reason: Instruction limit % 300.42/42.83 % (3961373)Termination phase: Saturation % 300.42/42.83 % (3961373)Time elapsed: 5.306 s % 300.42/42.83 % (3961373)Peak memory usage: 41 MB % 300.42/42.83 % (3961373)Instructions burned: 5115 (million) % 300.42/42.83 % (3961381)ott+11_1_sil=16000:gs=on:random_seed=212117044:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2894 on theBenchmark for (2894ds/2251Mi) % 300.42/42.83 % TRYING [4] % 300.42/42.83 % (3961381)Instruction limit reached! % 300.42/42.83 % (3961381)------------------------------ % 300.42/42.83 % (3961381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.83 % (3961381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.83 % (3961381)CaDiCaL version: 2.1.3 % 300.42/42.83 % (3961381)Termination reason: Instruction limit % 300.42/42.83 % (3961381)Termination phase: Saturation % 300.42/42.83 % (3961381)Time elapsed: 2.224 s % 300.42/42.83 % (3961381)Peak memory usage: 26 MB % 300.42/42.83 % (3961381)Instructions burned: 2251 (million) % 300.42/42.83 % (3961385)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3385833787:fmbsr=1.6:i=67534_2871 on theBenchmark for (2871ds/67534Mi) % 300.42/42.83 % (3961379)Instruction limit reached! % 300.42/42.83 % (3961379)------------------------------ % 300.42/42.83 % (3961379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.83 % (3961379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.83 % (3961379)CaDiCaL version: 2.1.3 % 300.42/42.83 % (3961379)Termination reason: Instruction limit % 300.42/42.83 % (3961379)Termination phase: Saturation % 300.42/42.83 % (3961379)Time elapsed: 3.578 s % 300.42/42.83 % (3961379)Peak memory usage: 36 MB % 300.42/42.83 % (3961379)Instructions burned: 3773 (million) % 300.42/42.83 % (3961387)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1971420295:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2861 on theBenchmark for (2861ds/4591Mi) % 300.42/42.83 % (3961387)Instruction limit reached! % 300.42/42.83 % (3961387)------------------------------ % 300.42/42.83 % (3961387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.83 % (3961387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.83 % (3961387)CaDiCaL version: 2.1.3 % 300.42/42.83 % (3961387)Termination reason: Instruction limit % 300.42/42.83 % (3961387)Termination phase: Saturation % 300.42/42.83 % (3961387)Time elapsed: 3.951 s % 300.42/42.83 % (3961387)Peak memory usage: 41 MB % 300.42/42.83 % (3961387)Instructions burned: 4591 (million) % 300.42/42.83 % (3961389)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3102953376:i=29340_2821 on theBenchmark for (2821ds/29340Mi) % 300.42/42.83 % TRYING [4] % 300.42/42.83 % (3961357)Instruction limit reached! % 300.42/42.83 % (3961357)------------------------------ % 300.42/42.83 % (3961357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.83 % (3961357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.83 % (3961357)CaDiCaL version: 2.1.3 % 300.42/42.83 % (3961357)Termination reason: Instruction limit % 300.42/42.83 % (3961357)Termination phase: Finite model building constraint generation % 300.42/42.83 % (3961357)Time elapsed: 17.412 s % 300.42/42.83 % (3961357)Peak memory usage: 382 MB % 300.42/42.83 % (3961357)Instructions burned: 22062 (million) % 300.42/42.83 % (3961393)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3551500319:i=5211_2806 on theBenchmark for (2806ds/5211Mi) % 300.42/42.83 % (3961393)Instruction limit reached! % 300.42/42.83 % (3961393)------------------------------ % 300.42/42.83 % (3961393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.83 % (3961393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.83 % (3961393)CaDiCaL version: 2.1.3 % 300.42/42.83 % (3961393)Termination reason: Instruction limit % 300.42/42.83 % (3961393)Termination phase: Saturation % 300.42/42.83 % (3961393)Time elapsed: 4.481 s % 300.42/42.83 % (3961393)Peak memory usage: 44 MB % 300.42/42.83 % (3961393)Instructions burned: 5211 (million) % 300.42/42.83 % (3961397)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3940983259:i=5497:nm=2_2761 on theBenchmark for (2761ds/5497Mi) % 300.42/42.83 % (3961397)Cannot represent all propositional literals internally % 300.42/42.83 % (3961397)Refutation not found, incomplete strategy % 300.42/42.84 % (3961397)------------------------------ % 300.42/42.84 % (3961397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.84 % (3961397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.84 % (3961397)CaDiCaL version: 2.1.3 % 300.42/42.84 % (3961397)Termination reason: Refutation not found, incomplete strategy % 300.42/42.84 % (3961397)Time elapsed: 0.768 s % 300.42/42.84 % (3961397)Peak memory usage: 30 MB % 300.42/42.84 % (3961397)Instructions burned: 1140 (million) % 300.42/42.84 % (3961397)------------------------------ % 300.42/42.84 % (3961397)------------------------------ % 300.42/42.84 % (3961399)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=130365626:fmbsr=2:i=46332_2753 on theBenchmark for (2753ds/46332Mi) % 300.42/42.84 % (3961399)Cannot represent all propositional literals internally % 300.42/42.84 % (3961399)Refutation not found, incomplete strategy % 300.42/42.84 % (3961399)------------------------------ % 300.42/42.84 % (3961399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.84 % (3961399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.84 % (3961399)CaDiCaL version: 2.1.3 % 300.42/42.84 % (3961399)Termination reason: Refutation not found, incomplete strategy % 300.42/42.84 % (3961399)Time elapsed: 1.003 s % 300.42/42.84 % (3961399)Peak memory usage: 27 MB % 300.42/42.84 % (3961399)Instructions burned: 1154 (million) % 300.42/42.84 % (3961399)------------------------------ % 300.42/42.84 % (3961399)------------------------------ % 300.42/42.84 % (3961401)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=254975594:i=14071_2742 on theBenchmark for (2742ds/14071Mi) % 300.42/42.84 % TRYING [12] % 300.42/42.84 % TRYING [7] % 300.42/42.84 % (3961401)Instruction limit reached! % 300.42/42.84 % (3961401)------------------------------ % 300.42/42.84 % (3961401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.84 % (3961401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.84 % (3961401)CaDiCaL version: 2.1.3 % 300.42/42.84 % (3961401)Termination reason: Instruction limit % 300.42/42.84 % (3961401)Termination phase: Finite model building constraint generation % 300.42/42.84 % (3961401)Time elapsed: 6.134 s % 300.42/42.84 % (3961401)Peak memory usage: 914 MB % 300.42/42.84 % (3961401)Instructions burned: 14074 (million) % 300.42/42.84 % (3961561)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2179144332:i=22565:add=on:rawr=on_2679 on theBenchmark for (2679ds/22565Mi) % 300.42/42.84 % TRYING [5] % 300.42/42.84 % TRYING [5] % 300.42/42.84 % (3961389)Instruction limit reached! % 300.42/42.84 % (3961389)------------------------------ % 300.42/42.84 % (3961389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.84 % (3961389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.84 % (3961389)CaDiCaL version: 2.1.3 % 300.42/42.84 % (3961389)Termination reason: Instruction limit % 300.42/42.84 % (3961389)Termination phase: Saturation % 300.42/42.84 % (3961389)Time elapsed: 18.798 s % 300.42/42.84 % (3961389)Peak memory usage: 181 MB % 300.42/42.84 % (3961389)Instructions burned: 29341 (million) % 300.42/42.84 % (3961563)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3334681089:i=8173:av=off_2633 on theBenchmark for (2633ds/8173Mi) % 300.42/42.84 % (3961375)Instruction limit reached! % 300.42/42.84 % (3961375)------------------------------ % 300.42/42.84 % (3961375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.84 % (3961375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.84 % (3961375)CaDiCaL version: 2.1.3 % 300.42/42.84 % (3961375)Termination reason: Instruction limit % 300.42/42.84 % (3961375)Termination phase: Finite model building constraint generation % 300.42/42.84 % (3961375)Time elapsed: 34.433 s % 300.42/42.84 % (3961375)Peak memory usage: 1707 MB % 300.42/42.84 % (3961375)Instructions burned: 54285 (million) % 300.42/42.84 % (3961565)dis+10_16:1_sil=16000:random_seed=119349711:i=9155:fsr=off_2594 on theBenchmark for (2594ds/9155Mi) % 300.42/42.84 % (3961563)Instruction limit reached! % 300.42/42.84 % (3961563)------------------------------ % 300.42/42.84 % (3961563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.84 % (3961563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.84 % (3961563)CaDiCaL version: 2.1.3 % 300.42/42.84 % (3961563)Termination reason: Instruction limit % 300.42/42.84 % (3961563)Termination phase: Saturation % 300.42/42.84 % (3961563)Time elapsed: 5.267 s % 300.42/42.84 % (3961563)Peak m % 300.42/42.84 Terminated % 300.42/42.84 % Vampire exiting %------------------------------------------------------------------------------