%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV249-1 : TPTP v9.3.1. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n016.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:35 PM UTC 2026 % Result : Timeout 300.21s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV249-1 : TPTP v9.3.1. Released v3.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n016.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 10:22:34 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/0.22 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 % 8.28/1.57 % (3530769)Will run a generic schedule for satisfiability detection. % 8.28/1.57 % (3530780)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=968168146:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.28/1.57 % (3530775)% WARNING: option uhcvi not known. % 8.28/1.57 % (3530774)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4239564180_2999 on theBenchmark for (2999ds/0Mi) % 8.28/1.57 % (3530775)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1591241541:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.28/1.57 % (3530778)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1489796295:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.28/1.57 % (3530776)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2321015262:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.28/1.57 % (3530777)dis+10_1_sil=32000:sp=arity:random_seed=764376835:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.28/1.57 % (3530779)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3685078569:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.28/1.57 % (3530780)Instruction limit reached! % 8.28/1.57 % (3530780)------------------------------ % 8.28/1.57 % (3530780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.28/1.57 % (3530780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.28/1.57 % (3530780)CaDiCaL version: 2.1.3 % 8.28/1.57 % (3530780)Termination reason: Instruction limit % 8.28/1.57 % (3530780)Termination phase: Saturation % 8.28/1.57 % (3530780)Time elapsed: 0.052 s % 8.28/1.57 % (3530780)Peak memory usage: 16 MB % 8.28/1.57 % (3530780)Instructions burned: 161 (million) % 8.28/1.57 % (3530788)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2740763382:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 8.28/1.57 % (3530777)Instruction limit reached! % 8.28/1.57 % (3530777)------------------------------ % 8.28/1.57 % (3530777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.28/1.57 % (3530777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.28/1.57 % (3530777)CaDiCaL version: 2.1.3 % 8.28/1.57 % (3530777)Termination reason: Instruction limit % 8.28/1.57 % (3530777)Termination phase: Saturation % 8.28/1.57 % (3530777)Time elapsed: 0.062 s % 8.28/1.57 % (3530777)Peak memory usage: 15 MB % 8.28/1.57 % (3530777)Instructions burned: 103 (million) % 8.28/1.57 % (3530778)Instruction limit reached! % 8.28/1.57 % (3530778)------------------------------ % 8.28/1.57 % (3530778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.28/1.57 % (3530778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.28/1.57 % (3530778)CaDiCaL version: 2.1.3 % 8.28/1.57 % (3530778)Termination reason: Instruction limit % 8.28/1.57 % (3530778)Termination phase: Saturation % 8.28/1.57 % (3530778)Time elapsed: 0.064 s % 8.28/1.57 % (3530778)Peak memory usage: 15 MB % 8.28/1.57 % (3530778)Instructions burned: 116 (million) % 8.28/1.57 % (3530779)Instruction limit reached! % 8.28/1.57 % (3530779)------------------------------ % 8.28/1.57 % (3530779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.28/1.57 % (3530779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.28/1.57 % (3530779)CaDiCaL version: 2.1.3 % 8.28/1.57 % (3530779)Termination reason: Instruction limit % 8.28/1.57 % (3530779)Termination phase: Saturation % 8.28/1.57 % (3530779)Time elapsed: 0.078 s % 8.28/1.57 % (3530779)Peak memory usage: 16 MB % 8.28/1.57 % (3530779)Instructions burned: 132 (million) % 8.28/1.57 % (3530790)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3344861752:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 8.28/1.57 % (3530791)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=2503123305:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 8.28/1.57 % (3530792)ott-21_1_sil=16000:fs=off:random_seed=2939004215:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.28/1.57 % (3530790)Instruction limit reached! % 8.28/1.57 % (3530790)------------------------------ % 8.28/1.57 % (3530790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.28/1.57 % (3530790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.28/1.57 % (3530790)CaDiCaL version: 2.1.3 % 41.94/6.29 % (3530790)Termination reason: Instruction limit % 41.94/6.29 % (3530790)Termination phase: Saturation % 41.94/6.29 % (3530790)Time elapsed: 0.081 s % 41.94/6.29 % (3530790)Peak memory usage: 16 MB % 41.94/6.29 % (3530790)Instructions burned: 131 (million) % 41.94/6.29 % (3530796)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=398081763:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 41.94/6.29 % (3530792)Instruction limit reached! % 41.94/6.29 % (3530792)------------------------------ % 41.94/6.29 % (3530792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.94/6.29 % (3530792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.94/6.29 % (3530792)CaDiCaL version: 2.1.3 % 41.94/6.29 % (3530792)Termination reason: Instruction limit % 41.94/6.29 % (3530792)Termination phase: Saturation % 41.94/6.29 % (3530792)Time elapsed: 0.095 s % 41.94/6.29 % (3530792)Peak memory usage: 16 MB % 41.94/6.29 % (3530792)Instructions burned: 182 (million) % 41.94/6.29 % TRYING [1] % 41.94/6.29 % (3530798)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=932303269:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 41.94/6.29 % TRYING [2] % 41.94/6.29 % (3530788)Instruction limit reached! % 41.94/6.29 % (3530788)------------------------------ % 41.94/6.29 % (3530788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.94/6.29 % (3530788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.94/6.29 % (3530788)CaDiCaL version: 2.1.3 % 41.94/6.29 % (3530788)Termination reason: Instruction limit % 41.94/6.29 % (3530788)Termination phase: Finite model building constraint generation % 41.94/6.29 % (3530788)Time elapsed: 0.181 s % 41.94/6.29 % (3530788)Peak memory usage: 26 MB % 41.94/6.29 % (3530788)Instructions burned: 717 (million) % 41.94/6.29 % (3530800)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=298705801:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 41.94/6.29 % TRYING [1] % 41.94/6.29 % TRYING [2] % 41.94/6.29 % (3530796)Instruction limit reached! % 41.94/6.29 % (3530796)------------------------------ % 41.94/6.29 % (3530796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.94/6.29 % (3530796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.94/6.29 % (3530796)CaDiCaL version: 2.1.3 % 41.94/6.29 % (3530796)Termination reason: Instruction limit % 41.94/6.29 % (3530796)Termination phase: Saturation % 41.94/6.29 % (3530796)Time elapsed: 0.294 s % 41.94/6.29 % (3530796)Peak memory usage: 17 MB % 41.94/6.29 % (3530796)Instructions burned: 477 (million) % 41.94/6.29 % (3530791)Instruction limit reached! % 41.94/6.29 % (3530791)------------------------------ % 41.94/6.29 % (3530791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.94/6.29 % (3530791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.94/6.29 % (3530791)CaDiCaL version: 2.1.3 % 41.94/6.29 % (3530791)Termination reason: Instruction limit % 41.94/6.29 % (3530791)Termination phase: Saturation % 41.94/6.29 % (3530791)Time elapsed: 0.400 s % 41.94/6.29 % (3530791)Peak memory usage: 21 MB % 41.94/6.29 % (3530791)Instructions burned: 684 (million) % 41.94/6.29 % (3530802)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3780315733:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 41.94/6.29 % (3530803)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=1512694141: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) % 41.94/6.29 % TRYING [1] % 41.94/6.29 % (3530798)Instruction limit reached! % 41.94/6.29 % (3530798)------------------------------ % 41.94/6.29 % (3530798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.94/6.29 % (3530798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.94/6.29 % (3530798)CaDiCaL version: 2.1.3 % 41.94/6.29 % (3530798)Termination reason: Instruction limit % 41.94/6.29 % (3530798)Termination phase: Finite model building constraint generation % 41.94/6.29 % (3530798)Time elapsed: 0.426 s % 41.94/6.29 % (3530798)Peak memory usage: 44 MB % 41.94/6.29 % (3530798)Instructions burned: 865 (million) % 41.94/6.29 % (3530800)Instruction limit reached! % 41.94/6.29 % (3530800)------------------------------ % 41.94/6.29 % (3530800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.94/6.29 % (3530800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.94/6.29 % (3530800)CaDiCaL version: 2.1.3 % 41.94/6.29 % (3530800)Termination reason: Instruction limit % 70.32/10.22 % (3530800)Termination phase: Saturation % 70.32/10.22 % (3530800)Time elapsed: 0.410 s % 70.32/10.22 % (3530800)Peak memory usage: 28 MB % 70.32/10.22 % (3530800)Instructions burned: 1181 (million) % 70.32/10.22 % (3530806)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3740335331:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi) % 70.32/10.22 % (3530807)fmb+10_1_sil=64000:random_seed=3314074271:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 70.32/10.22 % (3530802)Cannot represent all propositional literals internally % 70.32/10.22 % (3530802)Refutation not found, incomplete strategy % 70.32/10.22 % (3530802)------------------------------ % 70.32/10.22 % (3530802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.32/10.22 % (3530802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.32/10.22 % (3530802)CaDiCaL version: 2.1.3 % 70.32/10.22 % (3530802)Termination reason: Refutation not found, incomplete strategy % 70.32/10.22 % (3530802)Time elapsed: 0.297 s % 70.32/10.22 % (3530802)Peak memory usage: 23 MB % 70.32/10.22 % (3530802)Instructions burned: 595 (million) % 70.32/10.22 % (3530802)------------------------------ % 70.32/10.22 % (3530802)------------------------------ % 70.32/10.22 % (3530810)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3129812210:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 70.32/10.22 % TRYING [1] % 70.32/10.22 % (3530803)Instruction limit reached! % 70.32/10.22 % (3530803)------------------------------ % 70.32/10.22 % (3530803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.32/10.22 % (3530803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.32/10.22 % (3530803)CaDiCaL version: 2.1.3 % 70.32/10.22 % (3530803)Termination reason: Instruction limit % 70.32/10.22 % (3530803)Termination phase: Saturation % 70.32/10.22 % (3530803)Time elapsed: 0.418 s % 70.32/10.22 % (3530803)Peak memory usage: 22 MB % 70.32/10.22 % (3530803)Instructions burned: 693 (million) % 70.32/10.22 % (3530812)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2182870504:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi) % 70.32/10.22 % (3530806)Instruction limit reached! % 70.32/10.22 % (3530806)------------------------------ % 70.32/10.22 % (3530806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.32/10.22 % (3530806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.32/10.22 % (3530806)CaDiCaL version: 2.1.3 % 70.32/10.22 % (3530806)Termination reason: Instruction limit % 70.32/10.22 % (3530806)Termination phase: Saturation % 70.32/10.22 % (3530806)Time elapsed: 0.436 s % 70.32/10.22 % (3530806)Peak memory usage: 21 MB % 70.32/10.22 % (3530806)Instructions burned: 880 (million) % 70.32/10.22 % (3530810)Cannot represent all propositional literals internally % 70.32/10.22 % (3530810)Refutation not found, incomplete strategy % 70.32/10.22 % (3530810)------------------------------ % 70.32/10.22 % (3530810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.32/10.22 % (3530810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.32/10.22 % (3530810)CaDiCaL version: 2.1.3 % 70.32/10.22 % (3530810)Termination reason: Refutation not found, incomplete strategy % 70.32/10.22 % (3530810)Time elapsed: 0.298 s % 70.32/10.22 % (3530810)Peak memory usage: 23 MB % 70.32/10.22 % (3530810)Instructions burned: 591 (million) % 70.32/10.22 % (3530814)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1876430961:i=5131_2987 on theBenchmark for (2987ds/5131Mi) % 70.32/10.22 % (3530810)------------------------------ % 70.32/10.22 % (3530810)------------------------------ % 70.32/10.22 % TRYING [2] % 70.32/10.22 % (3530816)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2591419160:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi) % 70.32/10.22 % (3530812)Cannot represent all propositional literals internally % 70.32/10.22 % (3530812)Refutation not found, incomplete strategy % 70.32/10.22 % (3530812)------------------------------ % 70.32/10.22 % (3530812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.32/10.22 % (3530812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.32/10.22 % (3530812)CaDiCaL version: 2.1.3 % 70.32/10.22 % (3530812)Termination reason: Refutation not found, incomplete strategy % 70.32/10.22 % (3530812)Time elapsed: 0.293 s % 70.32/10.22 % (3530812)Peak memory usage: 23 MB % 70.32/10.22 % (3530812)Instructions burned: 591 (million) % 70.32/10.22 % (3530812)------------------------------ % 70.32/10.22 % (3530812)------------------------------ % 81.68/11.82 % (3530818)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2790967709:i=6324_2986 on theBenchmark for (2986ds/6324Mi) % 81.68/11.82 % (3530818)Cannot represent all propositional literals internally % 81.68/11.82 % (3530818)Refutation not found, incomplete strategy % 81.68/11.82 % (3530818)------------------------------ % 81.68/11.82 % (3530818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.68/11.82 % (3530818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.68/11.82 % (3530818)CaDiCaL version: 2.1.3 % 81.68/11.82 % (3530818)Termination reason: Refutation not found, incomplete strategy % 81.68/11.82 % (3530818)Time elapsed: 0.305 s % 81.68/11.82 % (3530818)Peak memory usage: 24 MB % 81.68/11.82 % (3530818)Instructions burned: 611 (million) % 81.68/11.82 % (3530818)------------------------------ % 81.68/11.82 % (3530818)------------------------------ % 81.68/11.82 % (3530820)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3550645612:fmbsr=2.30978:i=2174_2983 on theBenchmark for (2983ds/2174Mi) % 81.68/11.82 % (3530816)Instruction limit reached! % 81.68/11.82 % (3530816)------------------------------ % 81.68/11.82 % (3530816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.68/11.82 % (3530816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.68/11.82 % (3530816)CaDiCaL version: 2.1.3 % 81.68/11.82 % (3530816)Termination reason: Instruction limit % 81.68/11.82 % (3530816)Termination phase: Saturation % 81.68/11.82 % (3530816)Time elapsed: 0.879 s % 81.68/11.82 % (3530816)Peak memory usage: 34 MB % 81.68/11.82 % (3530816)Instructions burned: 1472 (million) % 81.68/11.82 % (3530822)ott-2_1_sil=16000:newcnf=on:random_seed=713724455:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2978 on theBenchmark for (2978ds/869Mi) % 81.68/11.82 % (3530822)Instruction limit reached! % 81.68/11.82 % (3530822)------------------------------ % 81.68/11.82 % (3530822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.68/11.82 % (3530822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.68/11.82 % (3530822)CaDiCaL version: 2.1.3 % 81.68/11.82 % (3530822)Termination reason: Instruction limit % 81.68/11.82 % (3530822)Termination phase: Saturation % 81.68/11.82 % (3530822)Time elapsed: 0.521 s % 81.68/11.82 % (3530822)Peak memory usage: 21 MB % 81.68/11.82 % (3530822)Instructions burned: 869 (million) % 81.68/11.82 % (3530824)ott+10_1_sil=32000:tgt=ground:random_seed=869380241:i=5114:av=off_2973 on theBenchmark for (2973ds/5114Mi) % 81.68/11.82 % (3530820)Instruction limit reached! % 81.68/11.82 % (3530820)------------------------------ % 81.68/11.82 % (3530820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.68/11.82 % (3530820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.68/11.82 % (3530820)CaDiCaL version: 2.1.3 % 81.68/11.82 % (3530820)Termination reason: Instruction limit % 81.68/11.82 % (3530820)Termination phase: Finite model building preprocessing % 81.68/11.82 % (3530820)Time elapsed: 1.104 s % 81.68/11.82 % (3530820)Peak memory usage: 42 MB % 81.68/11.82 % (3530820)Instructions burned: 2176 (million) % 81.68/11.82 % (3530826)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=896738650:i=54282_2971 on theBenchmark for (2971ds/54282Mi) % 81.68/11.82 % TRYING [1] % 81.68/11.82 % TRYING [2] % 81.68/11.82 % (3530814)Instruction limit reached! % 81.68/11.82 % (3530814)------------------------------ % 81.68/11.82 % (3530814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.68/11.82 % (3530814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.68/11.82 % (3530814)CaDiCaL version: 2.1.3 % 81.68/11.82 % (3530814)Termination reason: Instruction limit % 81.68/11.82 % (3530814)Termination phase: Saturation % 81.68/11.82 % (3530814)Time elapsed: 3.122 s % 81.68/11.82 % (3530814)Peak memory usage: 50 MB % 81.68/11.82 % (3530814)Instructions burned: 5133 (million) % 81.68/11.82 % (3530829)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3186465630:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi) % 81.68/11.82 % (3530824)Instruction limit reached! % 81.68/11.82 % (3530824)------------------------------ % 81.68/11.82 % (3530824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.68/11.82 % (3530824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.68/11.82 % (3530824)CaDiCaL version: 2.1.3 % 81.68/11.82 % (3530824)Termination reason: Instruction limit % 81.68/11.82 % (3530824)Termination phase: Saturation % 81.68/11.82 % (3530824)Time elapsed: 3.365 s % 81.68/11.82 % (3530824)Peak memory usage: 63 MB % 81.68/11.82 % (3530824)Instructions burned: 5115 (million) % 152.63/21.85 % (3530831)dis+21_1_sil=32000:sas=cadical:random_seed=2790957929:i=3773:amm=off_2939 on theBenchmark for (2939ds/3773Mi) % 152.63/21.85 % (3530829)Instruction limit reached! % 152.63/21.85 % (3530829)------------------------------ % 152.63/21.85 % (3530829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.63/21.85 % (3530829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.63/21.85 % (3530829)CaDiCaL version: 2.1.3 % 152.63/21.85 % (3530829)Termination reason: Instruction limit % 152.63/21.85 % (3530829)Termination phase: Saturation % 152.63/21.85 % (3530829)Time elapsed: 2.218 s % 152.63/21.85 % (3530829)Peak memory usage: 41 MB % 152.63/21.85 % (3530829)Instructions burned: 3513 (million) % 152.63/21.85 % (3530833)ott+11_1_sil=16000:gs=on:random_seed=718978807:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2934 on theBenchmark for (2934ds/2251Mi) % 152.63/21.85 % (3530774)Cannot represent all propositional literals internally % 152.63/21.85 % (3530833)Instruction limit reached! % 152.63/21.85 % (3530833)------------------------------ % 152.63/21.85 % (3530833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.63/21.85 % (3530833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.63/21.85 % (3530833)CaDiCaL version: 2.1.3 % 152.63/21.85 % (3530833)Termination reason: Instruction limit % 152.63/21.85 % (3530833)Termination phase: Saturation % 152.63/21.85 % (3530833)Time elapsed: 1.402 s % 152.63/21.85 % (3530833)Peak memory usage: 36 MB % 152.63/21.85 % (3530833)Instructions burned: 2251 (million) % 152.63/21.85 % (3530835)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2916321810:fmbsr=1.6:i=67534_2919 on theBenchmark for (2919ds/67534Mi) % 152.63/21.85 % (3530835)Cannot represent all propositional literals internally % 152.63/21.85 % (3530835)Refutation not found, incomplete strategy % 152.63/21.85 % (3530835)------------------------------ % 152.63/21.85 % (3530835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.63/21.85 % (3530835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.63/21.85 % (3530835)CaDiCaL version: 2.1.3 % 152.63/21.85 % (3530835)Termination reason: Refutation not found, incomplete strategy % 152.63/21.85 % (3530835)Time elapsed: 0.302 s % 152.63/21.85 % (3530835)Peak memory usage: 22 MB % 152.63/21.85 % (3530835)Instructions burned: 618 (million) % 152.63/21.85 % (3530835)------------------------------ % 152.63/21.85 % (3530835)------------------------------ % 152.63/21.85 % (3530837)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=190979:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2916 on theBenchmark for (2916ds/4591Mi) % 152.63/21.85 % (3530831)Instruction limit reached! % 152.63/21.85 % (3530831)------------------------------ % 152.63/21.85 % (3530831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.63/21.85 % (3530831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.63/21.85 % (3530831)CaDiCaL version: 2.1.3 % 152.63/21.85 % (3530831)Termination reason: Instruction limit % 152.63/21.85 % (3530831)Termination phase: Saturation % 152.63/21.85 % (3530831)Time elapsed: 2.383 s % 152.63/21.85 % (3530831)Peak memory usage: 45 MB % 152.63/21.85 % (3530831)Instructions burned: 3776 (million) % 152.63/21.85 % (3530839)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4201957988:i=29340_2915 on theBenchmark for (2915ds/29340Mi) % 152.63/21.85 % (3530774)Refutation not found, incomplete strategy % 152.63/21.85 % (3530774)------------------------------ % 152.63/21.85 % (3530774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.63/21.85 % (3530774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.63/21.85 % (3530774)CaDiCaL version: 2.1.3 % 152.63/21.85 % (3530774)Termination reason: Refutation not found, incomplete strategy % 152.63/21.85 % (3530774)Time elapsed: 8.827 s % 152.63/21.85 % (3530774)Peak memory usage: 979 MB % 152.63/21.85 % (3530774)Instructions burned: 14725 (million) % 152.63/21.85 % (3530774)------------------------------ % 152.63/21.85 % (3530774)------------------------------ % 152.63/21.85 % (3530841)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3473184416:i=5211_2909 on theBenchmark for (2909ds/5211Mi) % 152.63/21.85 % (3530807)Instruction limit reached! % 152.63/21.85 % (3530807)------------------------------ % 152.63/21.85 % (3530807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.63/21.85 % (3530807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.76/25.84 % (3530807)CaDiCaL version: 2.1.3 % 180.76/25.84 % (3530807)Termination reason: Instruction limit % 180.76/25.84 % (3530807)Termination phase: Finite model building SAT solving % 180.76/25.84 % (3530807)Time elapsed: 9.219 s % 180.76/25.84 % (3530807)Peak memory usage: 738 MB % 180.76/25.84 % (3530807)Instructions burned: 22062 (million) % 180.76/25.84 % (3530843)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=459842570:i=5497:nm=2_2899 on theBenchmark for (2899ds/5497Mi) % 180.76/25.84 % (3530843)Cannot represent all propositional literals internally % 180.76/25.84 % (3530843)Refutation not found, incomplete strategy % 180.76/25.84 % (3530843)------------------------------ % 180.76/25.84 % (3530843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.76/25.84 % (3530843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.76/25.84 % (3530843)CaDiCaL version: 2.1.3 % 180.76/25.84 % (3530843)Termination reason: Refutation not found, incomplete strategy % 180.76/25.84 % (3530843)Time elapsed: 0.164 s % 180.76/25.84 % (3530843)Peak memory usage: 24 MB % 180.76/25.84 % (3530843)Instructions burned: 611 (million) % 180.76/25.84 % (3530843)------------------------------ % 180.76/25.84 % (3530843)------------------------------ % 180.76/25.84 % (3530845)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2875211499:fmbsr=2:i=46332_2897 on theBenchmark for (2897ds/46332Mi) % 180.76/25.84 % (3530845)Cannot represent all propositional literals internally % 180.76/25.84 % (3530845)Refutation not found, incomplete strategy % 180.76/25.84 % (3530845)------------------------------ % 180.76/25.84 % (3530845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.76/25.84 % (3530845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.76/25.84 % (3530845)CaDiCaL version: 2.1.3 % 180.76/25.84 % (3530845)Termination reason: Refutation not found, incomplete strategy % 180.76/25.84 % (3530845)Time elapsed: 0.160 s % 180.76/25.84 % (3530845)Peak memory usage: 22 MB % 180.76/25.84 % (3530845)Instructions burned: 618 (million) % 180.76/25.84 % (3530845)------------------------------ % 180.76/25.84 % (3530845)------------------------------ % 180.76/25.84 % (3530847)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3437836648:i=14071_2895 on theBenchmark for (2895ds/14071Mi) % 180.76/25.84 % (3530837)Instruction limit reached! % 180.76/25.84 % (3530837)------------------------------ % 180.76/25.84 % (3530837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.76/25.84 % (3530837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.76/25.84 % (3530837)CaDiCaL version: 2.1.3 % 180.76/25.84 % (3530837)Termination reason: Instruction limit % 180.76/25.84 % (3530837)Termination phase: Saturation % 180.76/25.84 % (3530837)Time elapsed: 2.063 s % 180.76/25.84 % (3530837)Peak memory usage: 42 MB % 180.76/25.84 % (3530837)Instructions burned: 4593 (million) % 180.76/25.84 % (3530849)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3869059483:i=22565:add=on:rawr=on_2895 on theBenchmark for (2895ds/22565Mi) % 180.76/25.84 % (3530847)Cannot represent all propositional literals internally % 180.76/25.84 % (3530847)Refutation not found, incomplete strategy % 180.76/25.84 % (3530847)------------------------------ % 180.76/25.84 % (3530847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.76/25.84 % (3530847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.76/25.84 % (3530847)CaDiCaL version: 2.1.3 % 180.76/25.84 % (3530847)Termination reason: Refutation not found, incomplete strategy % 180.76/25.84 % (3530847)Time elapsed: 0.158 s % 180.76/25.84 % (3530847)Peak memory usage: 23 MB % 180.76/25.84 % (3530847)Instructions burned: 592 (million) % 180.76/25.84 % (3530847)------------------------------ % 180.76/25.84 % (3530847)------------------------------ % 180.76/25.84 % (3530851)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1395812027:i=8173:av=off_2894 on theBenchmark for (2894ds/8173Mi) % 180.76/25.84 % (3530826)Cannot represent all propositional literals internally % 180.76/25.84 % (3530841)Instruction limit reached! % 180.76/25.84 % (3530841)------------------------------ % 180.76/25.84 % (3530841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.76/25.84 % (3530841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.76/25.84 % (3530841)CaDiCaL version: 2.1.3 % 180.76/25.84 % (3530841)Termination reason: Instruction limit % 180.76/25.84 % (3530841)Termination phase: Saturation % 180.76/25.84 % (3530841)Time elapsed: 2.537 s % 180.76/25.84 % (3530841)Peak memory usage: 44 MB % 180.76/25.84 % (3530841)Instructions burned: 5213 (million) % 217.21/30.95 % (3530853)dis+10_16:1_sil=16000:random_seed=4033935984:i=9155:fsr=off_2884 on theBenchmark for (2884ds/9155Mi) % 217.21/30.95 % (3530826)Refutation not found, incomplete strategy % 217.21/30.95 % (3530826)------------------------------ % 217.21/30.95 % (3530826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.21/30.95 % (3530826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.21/30.95 % (3530826)CaDiCaL version: 2.1.3 % 217.21/30.95 % (3530826)Termination reason: Refutation not found, incomplete strategy % 217.21/30.95 % (3530826)Time elapsed: 8.811 s % 217.21/30.95 % (3530826)Peak memory usage: 979 MB % 217.21/30.95 % (3530826)Instructions burned: 14725 (million) % 217.21/30.95 % (3530826)------------------------------ % 217.21/30.95 % (3530826)------------------------------ % 217.21/30.95 % (3530855)ott-3_8_sil=64000:random_seed=691876018:i=20139:bs=on_2882 on theBenchmark for (2882ds/20139Mi) % 217.21/30.95 % (3530851)Instruction limit reached! % 217.21/30.95 % (3530851)------------------------------ % 217.21/30.95 % (3530851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.21/30.95 % (3530851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.21/30.95 % (3530851)CaDiCaL version: 2.1.3 % 217.21/30.95 % (3530851)Termination reason: Instruction limit % 217.21/30.95 % (3530851)Termination phase: Saturation % 217.21/30.95 % (3530851)Time elapsed: 2.982 s % 217.21/30.95 % (3530851)Peak memory usage: 105 MB % 217.21/30.95 % (3530851)Instructions burned: 8174 (million) % 217.21/30.95 % (3530857)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3761686734:fmbsr=2:i=32576_2864 on theBenchmark for (2864ds/32576Mi) % 217.21/30.95 % (3530857)Cannot represent all propositional literals internally % 217.21/30.95 % (3530857)Refutation not found, incomplete strategy % 217.21/30.95 % (3530857)------------------------------ % 217.21/30.95 % (3530857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.21/30.95 % (3530857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.21/30.95 % (3530857)CaDiCaL version: 2.1.3 % 217.21/30.95 % (3530857)Termination reason: Refutation not found, incomplete strategy % 217.21/30.95 % (3530857)Time elapsed: 0.162 s % 217.21/30.95 % (3530857)Peak memory usage: 24 MB % 217.21/30.95 % (3530857)Instructions burned: 611 (million) % 217.21/30.95 % (3530857)------------------------------ % 217.21/30.95 % (3530857)------------------------------ % 217.21/30.95 % (3530859)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1397375287:i=11404_2862 on theBenchmark for (2862ds/11404Mi) % 217.21/30.95 % (3530853)Instruction limit reached! % 217.21/30.95 % (3530853)------------------------------ % 217.21/30.95 % (3530853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.21/30.95 % (3530853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.21/30.95 % (3530853)CaDiCaL version: 2.1.3 % 217.21/30.95 % (3530853)Termination reason: Instruction limit % 217.21/30.95 % (3530853)Termination phase: Saturation % 217.21/30.95 % (3530853)Time elapsed: 5.173 s % 217.21/30.95 % (3530853)Peak memory usage: 91 MB % 217.21/30.95 % (3530853)Instructions burned: 9156 (million) % 217.21/30.95 % (3530861)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=368648612:i=14134_2832 on theBenchmark for (2832ds/14134Mi) % 217.21/30.95 % (3530859)Instruction limit reached! % 217.21/30.95 % (3530859)------------------------------ % 217.21/30.95 % (3530859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.21/30.95 % (3530859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.21/30.95 % (3530859)CaDiCaL version: 2.1.3 % 217.21/30.95 % (3530859)Termination reason: Instruction limit % 217.21/30.95 % (3530859)Termination phase: Saturation % 217.21/30.95 % (3530859)Time elapsed: 4.081 s % 217.21/30.95 % (3530859)Peak memory usage: 163 MB % 217.21/30.95 % (3530859)Instructions burned: 11404 (million) % 217.21/30.95 % (3530863)dis+33_16_sil=32000:sac=on:random_seed=1350877630:i=15851:nm=0_2821 on theBenchmark for (2821ds/15851Mi) % 217.21/30.95 % (3530849)Instruction limit reached! % 217.21/30.95 % (3530849)------------------------------ % 217.21/30.95 % (3530849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.21/30.95 % (3530849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.21/30.95 % (3530849)CaDiCaL version: 2.1.3 % 217.21/30.95 % (3530849)Termination reason: Instruction limit % 217.21/30.95 % (3530849)Termination phase: Saturation % 217.21/30.95 % (3530849)Time elapsed: 11.121 s % 217.21/30.95 % (3530849)Peak memory usage: 219 MB % 217.21/30.95 % (3530849)Instructions burned: 22566 (million) % 217.21/30.95 % (3530865)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2157063676:avsq=on:i=17627:add=on:amm=off_2783 on theBenchmark for (2783ds/17627Mi) % 251.69/35.89 % (3530839)Instruction limit reached! % 251.69/35.89 % (3530839)------------------------------ % 251.69/35.89 % (3530839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.69/35.89 % (3530839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.69/35.89 % (3530839)CaDiCaL version: 2.1.3 % 251.69/35.89 % (3530839)Termination reason: Instruction limit % 251.69/35.89 % (3530839)Termination phase: Saturation % 251.69/35.89 % (3530839)Time elapsed: 13.442 s % 251.69/35.89 % (3530839)Peak memory usage: 446 MB % 251.69/35.89 % (3530839)Instructions burned: 29341 (million) % 251.69/35.89 % (3530867)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2919193036:s2a=on:i=53295_2780 on theBenchmark for (2780ds/53295Mi) % 251.69/35.89 % (3530863)Instruction limit reached! % 251.69/35.89 % (3530863)------------------------------ % 251.69/35.89 % (3530863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.69/35.89 % (3530863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.69/35.89 % (3530863)CaDiCaL version: 2.1.3 % 251.69/35.89 % (3530863)Termination reason: Instruction limit % 251.69/35.89 % (3530863)Termination phase: Saturation % 251.69/35.89 % (3530863)Time elapsed: 4.451 s % 251.69/35.89 % (3530863)Peak memory usage: 173 MB % 251.69/35.89 % (3530863)Instructions burned: 15851 (million) % 251.69/35.89 % (3530869)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3390929356:i=26857:ins=20_2776 on theBenchmark for (2776ds/26857Mi) % 251.69/35.89 % (3530869)Cannot represent all propositional literals internally % 251.69/35.89 % (3530869)Refutation not found, incomplete strategy % 251.69/35.89 % (3530869)------------------------------ % 251.69/35.89 % (3530869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.69/35.89 % (3530869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.69/35.89 % (3530869)CaDiCaL version: 2.1.3 % 251.69/35.89 % (3530869)Termination reason: Refutation not found, incomplete strategy % 251.69/35.89 % (3530869)Time elapsed: 0.158 s % 251.69/35.89 % (3530869)Peak memory usage: 23 MB % 251.69/35.89 % (3530869)Instructions burned: 591 (million) % 251.69/35.89 % (3530869)------------------------------ % 251.69/35.89 % (3530869)------------------------------ % 251.69/35.89 % (3530871)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2488248900:i=28120:bs=on:fsr=off_2774 on theBenchmark for (2774ds/28120Mi) % 251.69/35.89 % (3530855)Instruction limit reached! % 251.69/35.89 % (3530855)------------------------------ % 251.69/35.89 % (3530855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.69/35.89 % (3530855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.69/35.89 % (3530855)CaDiCaL version: 2.1.3 % 251.69/35.89 % (3530855)Termination reason: Instruction limit % 251.69/35.89 % (3530855)Termination phase: Saturation % 251.69/35.89 % (3530855)Time elapsed: 13.203 s % 251.69/35.89 % (3530855)Peak memory usage: 115 MB % 251.69/35.89 % (3530855)Instructions burned: 20139 (million) % 251.69/35.89 % (3530873)fmb+10_1_sil=256000:fmbss=7:random_seed=3188080795:fmbsr=1.6:i=182295_2750 on theBenchmark for (2750ds/182295Mi) % 251.69/35.89 % (3530873)Cannot represent all propositional literals internally % 251.69/35.89 % (3530873)Refutation not found, incomplete strategy % 251.69/35.89 % (3530873)------------------------------ % 251.69/35.89 % (3530873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.69/35.89 % (3530873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.69/35.89 % (3530873)CaDiCaL version: 2.1.3 % 251.69/35.89 % (3530873)Termination reason: Refutation not found, incomplete strategy % 251.69/35.89 % (3530873)Time elapsed: 0.294 s % 251.69/35.89 % (3530873)Peak memory usage: 23 MB % 251.69/35.89 % (3530873)Instructions burned: 591 (million) % 251.69/35.89 % (3530873)------------------------------ % 251.69/35.89 % (3530873)------------------------------ % 251.69/35.89 % (3530875)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3521057866:i=44625:gsp=on_2747 on theBenchmark for (2747ds/44625Mi) % 251.69/35.89 % (3530875)Cannot represent all propositional literals internally % 251.69/35.89 % (3530875)Refutation not found, incomplete strategy % 251.69/35.89 % (3530875)------------------------------ % 251.69/35.89 % (3530875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.69/35.89 % (3530875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.01/37.42 % (3530875)CaDiCaL version: 2.1.3 % 252.01/37.42 % (3530875)Termination reason: Refutation not found, incomplete strategy % 252.01/37.42 % (3530875)Time elapsed: 0.297 s % 252.01/37.42 % (3530875)Peak memory usage: 23 MB % 252.01/37.42 % (3530875)Instructions burned: 598 (million) % 252.01/37.42 % (3530875)------------------------------ % 252.01/37.42 % (3530875)------------------------------ % 252.01/37.42 % (3530877)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4173894409:i=160505_2743 on theBenchmark for (2743ds/160505Mi) % 252.01/37.42 % (3530861)Instruction limit reached! % 252.01/37.42 % (3530861)------------------------------ % 252.01/37.42 % (3530861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.01/37.42 % (3530861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.01/37.42 % (3530861)CaDiCaL version: 2.1.3 % 252.01/37.42 % (3530861)Termination reason: Instruction limit % 252.01/37.42 % (3530861)Termination phase: Saturation % 252.01/37.42 % (3530861)Time elapsed: 8.820 s % 252.01/37.42 % (3530861)Peak memory usage: 115 MB % 252.01/37.42 % (3530861)Instructions burned: 14135 (million) % 252.01/37.42 % (3530879)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=163593161:fmbsr=1.3:i=225729_2743 on theBenchmark for (2743ds/225729Mi) % 252.01/37.42 % (3530877)Cannot represent all propositional literals internally % 252.01/37.42 % (3530877)Refutation not found, incomplete strategy % 252.01/37.42 % (3530877)------------------------------ % 252.01/37.42 % (3530877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.01/37.42 % (3530877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.01/37.42 % (3530877)CaDiCaL version: 2.1.3 % 252.01/37.42 % (3530877)Termination reason: Refutation not found, incomplete strategy % 252.01/37.42 % (3530877)Time elapsed: 0.295 s % 252.01/37.42 % (3530877)Peak memory usage: 23 MB % 252.01/37.42 % (3530877)Instructions burned: 591 (million) % 252.01/37.42 % (3530877)------------------------------ % 252.01/37.42 % (3530877)------------------------------ % 252.01/37.42 % (3530881)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2469006792:fmbsr=2:i=185024:ins=7_2740 on theBenchmark for (2740ds/185024Mi) % 252.01/37.42 % (3530879)Cannot represent all propositional literals internally % 252.01/37.42 % (3530879)Refutation not found, incomplete strategy % 252.01/37.42 % (3530879)------------------------------ % 252.01/37.42 % (3530879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.01/37.42 % (3530879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.01/37.42 % (3530879)CaDiCaL version: 2.1.3 % 252.01/37.42 % (3530879)Termination reason: Refutation not found, incomplete strategy % 252.01/37.42 % (3530879)Time elapsed: 0.294 s % 252.01/37.42 % (3530879)Peak memory usage: 23 MB % 252.01/37.42 % (3530879)Instructions burned: 592 (million) % 252.01/37.42 % (3530879)------------------------------ % 252.01/37.42 % (3530879)------------------------------ % 252.01/37.42 % (3530883)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2049268221:rtra=on_2740 on theBenchmark for (2740ds/0Mi) % 252.01/37.42 % (3530881)Cannot represent all propositional literals internally % 252.01/37.42 % (3530881)Refutation not found, incomplete strategy % 252.01/37.42 % (3530881)------------------------------ % 252.01/37.42 % (3530881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.01/37.42 % (3530881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.01/37.42 % (3530881)CaDiCaL version: 2.1.3 % 252.01/37.42 % (3530881)Termination reason: Refutation not found, incomplete strategy % 252.01/37.42 % (3530881)Time elapsed: 0.295 s % 252.01/37.42 % (3530881)Peak memory usage: 23 MB % 252.01/37.42 % (3530881)Instructions burned: 592 (million) % 252.01/37.42 % (3530881)------------------------------ % 252.01/37.42 % (3530881)------------------------------ % 252.01/37.42 % (3530885)% WARNING: option uhcvi not known. % 252.01/37.42 % (3530885)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2957473163:i=271062:add=off:rtra=on:rawr=on_2737 on theBenchmark for (2737ds/271062Mi) % 252.01/37.42 % TRYING [1] % 252.01/37.42 % TRYING [2] % 252.01/37.42 % (3530865)Instruction limit reached! % 252.01/37.42 % (3530865)------------------------------ % 252.01/37.42 % (3530865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.01/37.42 % (3530865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.01/37.42 % (3530865)CaDiCaL version: 2.1.3 % 252.01/37.42 % (3530865)Termination reason: Instruction limit % 252.01/37.42 % (3530865)Termination phase: Saturation % 252.01/37.42 % (3530865)Time elapsed: 9.103 s % 252.01/37.42 % (3530865)Peak memory usage: 120 MB % 252.01/37.42 % (3530865)Instructions burned: 17630 (million) % 272.89/38.93 % (3530887)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3462549564:i=176048:add=on:rtra=on:rawr=on_2692 on theBenchmark for (2692ds/176048Mi) % 272.89/38.93 % (3530871)Instruction limit reached! % 272.89/38.93 % (3530871)------------------------------ % 272.89/38.93 % (3530871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.89/38.93 % (3530871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.89/38.93 % (3530871)CaDiCaL version: 2.1.3 % 272.89/38.93 % (3530871)Termination reason: Instruction limit % 272.89/38.93 % (3530871)Termination phase: Saturation % 272.89/38.93 % (3530871)Time elapsed: 12.324 s % 272.89/38.93 % (3530871)Peak memory usage: 855 MB % 272.89/38.93 % (3530871)Instructions burned: 28120 (million) % 272.89/38.93 % (3530889)dis+10_1_sil=32000:si=on:sp=arity:random_seed=787797329:i=206:fgj=on:rtra=on_2650 on theBenchmark for (2650ds/206Mi) % 272.89/38.93 % (3530889)Instruction limit reached! % 272.89/38.93 % (3530889)------------------------------ % 272.89/38.93 % (3530889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.89/38.93 % (3530889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.89/38.93 % (3530889)CaDiCaL version: 2.1.3 % 272.89/38.93 % (3530889)Termination reason: Instruction limit % 272.89/38.93 % (3530889)Termination phase: Saturation % 272.89/38.93 % (3530889)Time elapsed: 0.073 s % 272.89/38.93 % (3530889)Peak memory usage: 17 MB % 272.89/38.93 % (3530889)Instructions burned: 206 (million) % 272.89/38.93 % (3530891)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2974361513:i=232:rtra=on_2650 on theBenchmark for (2650ds/232Mi) % 272.89/38.93 % (3530891)Instruction limit reached! % 272.89/38.93 % (3530891)------------------------------ % 272.89/38.93 % (3530891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.89/38.93 % (3530891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.89/38.93 % (3530891)CaDiCaL version: 2.1.3 % 272.89/38.93 % (3530891)Termination reason: Instruction limit % 272.89/38.93 % (3530891)Termination phase: Saturation % 272.89/38.93 % (3530891)Time elapsed: 0.078 s % 272.89/38.93 % (3530891)Peak memory usage: 17 MB % 272.89/38.93 % (3530891)Instructions burned: 232 (million) % 272.89/38.93 % (3530893)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=97040043:i=262:rtra=on_2649 on theBenchmark for (2649ds/262Mi) % 272.89/38.93 % (3530893)Instruction limit reached! % 272.89/38.93 % (3530893)------------------------------ % 272.89/38.93 % (3530893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.89/38.93 % (3530893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.89/38.93 % (3530893)CaDiCaL version: 2.1.3 % 272.89/38.93 % (3530893)Termination reason: Instruction limit % 272.89/38.93 % (3530893)Termination phase: Saturation % 272.89/38.93 % (3530893)Time elapsed: 0.091 s % 272.89/38.93 % (3530893)Peak memory usage: 18 MB % 272.89/38.93 % (3530893)Instructions burned: 265 (million) % 272.89/38.93 % (3530895)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=4205075687:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2648 on theBenchmark for (2648ds/318Mi) % 272.89/38.93 % (3530895)Instruction limit reached! % 272.89/38.93 % (3530895)------------------------------ % 272.89/38.93 % (3530895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.89/38.93 % (3530895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.89/38.93 % (3530895)CaDiCaL version: 2.1.3 % 272.89/38.93 % (3530895)Termination reason: Instruction limit % 272.89/38.93 % (3530895)Termination phase: Saturation % 272.89/38.93 % (3530895)Time elapsed: 0.117 s % 272.89/38.93 % (3530895)Peak memory usage: 19 MB % 272.89/38.93 % (3530895)Instructions burned: 320 (million) % 272.89/38.93 % (3530897)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3382040173:i=1428:nm=2:rtra=on_2646 on theBenchmark for (2646ds/1428Mi) % 272.89/38.93 % TRYING [1] % 272.89/38.93 % TRYING [2] % 272.89/38.93 % (3530897)Instruction limit reached! % 272.89/38.93 % (3530897)------------------------------ % 272.89/38.93 % (3530897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.89/38.93 % (3530897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.89/38.93 % (3530897)CaDiCaL version: 2.1.3 % 272.89/38.93 % (3530897)Termination reason: Instruction limit % 272.89/38.93 % (3530897)Termination phase: Finite model building constraint generation % 272.89/38.93 % (3530897)Time elapsed: 0.337 s % 272.89/38.93 % (3530897)Peak memory usage: 62 MB % 300.21/42.63 % (3530897)Instructions burned: 1433 (million) % 300.21/42.63 % (3530899)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=4147087553:i=262:bd=preordered:rtra=on:fsd=on_2643 on theBenchmark for (2643ds/262Mi) % 300.21/42.63 % (3530899)Instruction limit reached! % 300.21/42.63 % (3530899)------------------------------ % 300.21/42.63 % (3530899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.21/42.63 % (3530899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.21/42.63 % (3530899)CaDiCaL version: 2.1.3 % 300.21/42.63 % (3530899)Termination reason: Instruction limit % 300.21/42.63 % (3530899)Termination phase: Saturation % 300.21/42.63 % (3530899)Time elapsed: 0.100 s % 300.21/42.63 % (3530899)Peak memory usage: 17 MB % 300.21/42.63 % (3530899)Instructions burned: 262 (million) % 300.21/42.63 % (3530901)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1773842234:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2642 on theBenchmark for (2642ds/1368Mi) % 300.21/42.63 % (3530883)Cannot represent all propositional literals internally % 300.21/42.63 % (3530901)Instruction limit reached! % 300.21/42.63 % (3530901)------------------------------ % 300.21/42.63 % (3530901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.21/42.63 % (3530901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.21/42.63 % (3530901)CaDiCaL version: 2.1.3 % 300.21/42.63 % (3530901)Termination reason: Instruction limit % 300.21/42.63 % (3530901)Termination phase: Saturation % 300.21/42.63 % (3530901)Time elapsed: 0.448 s % 300.21/42.63 % (3530901)Peak memory usage: 26 MB % 300.21/42.63 % (3530901)Instructions burned: 1369 (million) % 300.21/42.63 % (3530903)ott-21_1_sil=16000:si=on:fs=off:random_seed=1742522853:i=360:av=off:fsr=off:rtra=on_2637 on theBenchmark for (2637ds/360Mi) % 300.21/42.63 % (3530903)Instruction limit reached! % 300.21/42.63 % (3530903)------------------------------ % 300.21/42.63 % (3530903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.21/42.63 % (3530903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.21/42.63 % (3530903)CaDiCaL version: 2.1.3 % 300.21/42.63 % (3530903)Termination reason: Instruction limit % 300.21/42.63 % (3530903)Termination phase: Saturation % 300.21/42.63 % (3530903)Time elapsed: 0.114 s % 300.21/42.63 % (3530903)Peak memory usage: 18 MB % 300.21/42.63 % (3530903)Instructions burned: 360 (million) % 300.21/42.63 % (3530905)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1564887655:i=954:bd=all:rtra=on_2636 on theBenchmark for (2636ds/954Mi) % 300.21/42.63 % (3530905)Instruction limit reached! % 300.21/42.63 % (3530905)------------------------------ % 300.21/42.63 % (3530905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.21/42.63 % (3530905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.21/42.63 % (3530905)CaDiCaL version: 2.1.3 % 300.21/42.63 % (3530905)Termination reason: Instruction limit % 300.21/42.63 % (3530905)Termination phase: Saturation % 300.21/42.63 % (3530905)Time elapsed: 0.329 s % 300.21/42.63 % (3530905)Peak memory usage: 18 MB % 300.21/42.63 % (3530905)Instructions burned: 954 (million) % 300.21/42.63 % (3530907)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2795079167:fmbsr=1.3:i=1730:ins=25:rtra=on_2632 on theBenchmark for (2632ds/1730Mi) % 300.21/42.63 % TRYING [1] % 300.21/42.63 % (3530883)Refutation not found, incomplete strategy % 300.21/42.63 % (3530883)------------------------------ % 300.21/42.63 % (3530883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.21/42.63 % (3530883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.21/42.63 % (3530883)CaDiCaL version: 2.1.3 % 300.21/42.63 % (3530883)Termination reason: Refutation not found, incomplete strategy % 300.21/42.63 % (3530883)Time elapsed: 11.152 s % 300.21/42.63 % (3530883)Peak memory usage: 940 MB % 300.21/42.63 % (3530883)Instructions burned: 15118 (million) % 300.21/42.63 % (3530883)------------------------------ % 300.21/42.63 % (3530883)------------------------------ % 300.21/42.63 % (3530907)Instruction limit reached! % 300.21/42.63 % (3530907)------------------------------ % 300.21/42.63 % (3530907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.21/42.63 % (3530907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.21/42.63 % (3530907)CaDiCaL version: 2.1.3 % 300.21/42.63 % (3530907)Termination reason: Instruction limit % 300.21/42.63 % (3530907)Termination phase: Finite model building constraint generation % 300.21/42.63 % % 300.21/42.63 Terminated % 300.21/42.63 % Vampire exiting % 300.21/42.64 Terminated %------------------------------------------------------------------------------