%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW611_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n005.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:31 PM UTC 2026 % Result : Timeout 300.73s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW611_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 % Computer : n005.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 14:22:34 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 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 % 3.61/0.89 % (814848)Will run a generic schedule for satisfiability detection. % 3.61/0.89 % (814859)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1530100643:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.61/0.89 % (814854)% WARNING: option uhcvi not known. % 3.61/0.89 % (814853)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2798593300_2999 on theBenchmark for (2999ds/0Mi) % 3.61/0.89 % (814854)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=156669143:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.61/0.89 % (814855)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2749382402:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.61/0.89 % (814856)dis+10_1_sil=32000:sp=arity:random_seed=4055837628:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.61/0.89 % (814857)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2851454347:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.61/0.89 % (814858)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3099172691:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.61/0.89 % (814853)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.61/0.89 % (814853)Terminated due to inappropriate strategy. % 3.61/0.89 % (814853)------------------------------ % 3.61/0.89 % (814853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.89 % (814853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.89 % (814853)CaDiCaL version: 2.1.3 % 3.61/0.89 % (814853)Termination reason: Inappropriate % 3.61/0.89 % (814853)Time elapsed: 0.006 s % 3.61/0.89 % (814853)Peak memory usage: 10 MB % 3.61/0.89 % (814853)Instructions burned: 10 (million) % 3.61/0.89 % (814853)------------------------------ % 3.61/0.89 % (814853)------------------------------ % 3.61/0.89 % (814867)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1183739261:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.61/0.89 % (814867)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.61/0.89 % (814867)Terminated due to inappropriate strategy. % 3.61/0.89 % (814867)------------------------------ % 3.61/0.89 % (814867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.89 % (814867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.89 % (814867)CaDiCaL version: 2.1.3 % 3.61/0.89 % (814867)Termination reason: Inappropriate % 3.61/0.89 % (814867)Time elapsed: 0.004 s % 3.61/0.89 % (814867)Peak memory usage: 10 MB % 3.61/0.89 % (814867)Instructions burned: 8 (million) % 3.61/0.89 % (814867)------------------------------ % 3.61/0.89 % (814867)------------------------------ % 3.61/0.89 % (814859)Instruction limit reached! % 3.61/0.89 % (814859)------------------------------ % 3.61/0.89 % (814859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.89 % (814859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.89 % (814859)CaDiCaL version: 2.1.3 % 3.61/0.89 % (814859)Termination reason: Instruction limit % 3.61/0.89 % (814859)Termination phase: Saturation % 3.61/0.89 % (814859)Time elapsed: 0.059 s % 3.61/0.89 % (814859)Peak memory usage: 13 MB % 3.61/0.89 % (814859)Instructions burned: 160 (million) % 3.61/0.89 % (814869)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1592520762:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.61/0.89 % (814871)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=3330344332:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.61/0.89 % (814856)Instruction limit reached! % 3.61/0.89 % (814856)------------------------------ % 3.61/0.89 % (814856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.89 % (814856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.89 % (814856)CaDiCaL version: 2.1.3 % 3.61/0.89 % (814856)Termination reason: Instruction limit % 3.61/0.89 % (814856)Termination phase: Saturation % 3.61/0.89 % (814856)Time elapsed: 0.067 s % 3.61/0.89 % (814856)Peak memory usage: 12 MB % 3.61/0.89 % (814856)Instructions burned: 104 (million) % 3.61/0.89 % (814858)Instruction limit reached! % 3.61/0.89 % (814858)------------------------------ % 3.61/0.89 % (814858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.97/1.47 % (814858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.97/1.47 % (814858)CaDiCaL version: 2.1.3 % 7.97/1.47 % (814858)Termination reason: Instruction limit % 7.97/1.47 % (814858)Termination phase: Saturation % 7.97/1.47 % (814858)Time elapsed: 0.071 s % 7.97/1.47 % (814858)Peak memory usage: 12 MB % 7.97/1.47 % (814858)Instructions burned: 131 (million) % 7.97/1.47 % (814857)Instruction limit reached! % 7.97/1.47 % (814857)------------------------------ % 7.97/1.47 % (814857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.97/1.47 % (814857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.97/1.47 % (814857)CaDiCaL version: 2.1.3 % 7.97/1.47 % (814857)Termination reason: Instruction limit % 7.97/1.47 % (814857)Termination phase: Saturation % 7.97/1.47 % (814857)Time elapsed: 0.075 s % 7.97/1.47 % (814857)Peak memory usage: 13 MB % 7.97/1.47 % (814857)Instructions burned: 121 (million) % 7.97/1.47 % (814873)ott-21_1_sil=16000:fs=off:random_seed=2504610166:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.97/1.47 % (814874)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3220721992:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.97/1.47 % (814875)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=484024079:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.97/1.47 % (814875)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.97/1.47 % (814875)Terminated due to inappropriate strategy. % 7.97/1.47 % (814875)------------------------------ % 7.97/1.47 % (814875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.97/1.47 % (814875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.97/1.47 % (814875)CaDiCaL version: 2.1.3 % 7.97/1.47 % (814875)Termination reason: Inappropriate % 7.97/1.47 % (814875)Time elapsed: 0.004 s % 7.97/1.47 % (814875)Peak memory usage: 10 MB % 7.97/1.47 % (814875)Instructions burned: 8 (million) % 7.97/1.47 % (814875)------------------------------ % 7.97/1.47 % (814875)------------------------------ % 7.97/1.47 % (814879)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=229945363:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.97/1.47 % (814869)Instruction limit reached! % 7.97/1.47 % (814869)------------------------------ % 7.97/1.47 % (814869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.97/1.47 % (814869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.97/1.47 % (814869)CaDiCaL version: 2.1.3 % 7.97/1.47 % (814869)Termination reason: Instruction limit % 7.97/1.47 % (814869)Termination phase: Saturation % 7.97/1.47 % (814869)Time elapsed: 0.082 s % 7.97/1.47 % (814869)Peak memory usage: 12 MB % 7.97/1.47 % (814869)Instructions burned: 132 (million) % 7.97/1.47 % (814881)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2325072425:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 7.97/1.47 % (814881)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.97/1.47 % (814881)Terminated due to inappropriate strategy. % 7.97/1.47 % (814881)------------------------------ % 7.97/1.47 % (814881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.97/1.47 % (814881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.97/1.47 % (814881)CaDiCaL version: 2.1.3 % 7.97/1.47 % (814881)Termination reason: Inappropriate % 7.97/1.47 % (814881)Time elapsed: 0.005 s % 7.97/1.47 % (814881)Peak memory usage: 10 MB % 7.97/1.47 % (814881)Instructions burned: 8 (million) % 7.97/1.47 % (814881)------------------------------ % 7.97/1.47 % (814881)------------------------------ % 7.97/1.47 % (814883)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=327724122:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 7.97/1.47 % (814873)Instruction limit reached! % 7.97/1.47 % (814873)------------------------------ % 7.97/1.47 % (814873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.97/1.47 % (814873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.97/1.47 % (814873)CaDiCaL version: 2.1.3 % 7.97/1.47 % (814873)Termination reason: Instruction limit % 7.97/1.47 % (814873)Termination phase: Saturation % 7.97/1.47 % (814873)Time elapsed: 0.094 s % 7.97/1.47 % (814873)Peak memory usage: 12 MB % 7.97/1.47 % (814873)Instructions burned: 180 (million) % 21.41/3.30 % (814885)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=300364472:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 21.41/3.30 % (814871)Instruction limit reached! % 21.41/3.30 % (814871)------------------------------ % 21.41/3.30 % (814871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.41/3.30 % (814871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.41/3.30 % (814871)CaDiCaL version: 2.1.3 % 21.41/3.30 % (814871)Termination reason: Instruction limit % 21.41/3.30 % (814871)Termination phase: Saturation % 21.41/3.30 % (814871)Time elapsed: 0.192 s % 21.41/3.30 % (814871)Peak memory usage: 16 MB % 21.41/3.30 % (814871)Instructions burned: 685 (million) % 21.41/3.30 % (814887)fmb+10_1_sil=64000:random_seed=1474782186:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 21.41/3.30 % (814887)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.41/3.30 % (814887)Terminated due to inappropriate strategy. % 21.41/3.30 % (814887)------------------------------ % 21.41/3.30 % (814887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.41/3.30 % (814887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.41/3.30 % (814887)CaDiCaL version: 2.1.3 % 21.41/3.30 % (814887)Termination reason: Inappropriate % 21.41/3.30 % (814887)Time elapsed: 0.002 s % 21.41/3.30 % (814887)Peak memory usage: 11 MB % 21.41/3.30 % (814887)Instructions burned: 9 (million) % 21.41/3.30 % (814887)------------------------------ % 21.41/3.30 % (814887)------------------------------ % 21.41/3.30 % (814889)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1495752875:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 21.41/3.30 % (814889)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.41/3.30 % (814889)Terminated due to inappropriate strategy. % 21.41/3.30 % (814889)------------------------------ % 21.41/3.30 % (814889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.41/3.30 % (814889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.41/3.30 % (814889)CaDiCaL version: 2.1.3 % 21.41/3.30 % (814889)Termination reason: Inappropriate % 21.41/3.30 % (814889)Time elapsed: 0.002 s % 21.41/3.30 % (814889)Peak memory usage: 11 MB % 21.41/3.30 % (814889)Instructions burned: 8 (million) % 21.41/3.30 % (814889)------------------------------ % 21.41/3.30 % (814889)------------------------------ % 21.41/3.30 % (814891)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2105079893:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 21.41/3.30 % (814891)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.41/3.30 % (814891)Terminated due to inappropriate strategy. % 21.41/3.30 % (814891)------------------------------ % 21.41/3.30 % (814891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.41/3.30 % (814891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.41/3.30 % (814891)CaDiCaL version: 2.1.3 % 21.41/3.30 % (814891)Termination reason: Inappropriate % 21.41/3.30 % (814891)Time elapsed: 0.002 s % 21.41/3.30 % (814891)Peak memory usage: 11 MB % 21.41/3.30 % (814891)Instructions burned: 8 (million) % 21.41/3.30 % (814891)------------------------------ % 21.41/3.30 % (814891)------------------------------ % 21.41/3.30 % (814893)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2900038423:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 21.41/3.30 % (814874)Instruction limit reached! % 21.41/3.30 % (814874)------------------------------ % 21.41/3.30 % (814874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.41/3.30 % (814874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.41/3.30 % (814874)CaDiCaL version: 2.1.3 % 21.41/3.30 % (814874)Termination reason: Instruction limit % 21.41/3.30 % (814874)Termination phase: Saturation % 21.41/3.30 % (814874)Time elapsed: 0.307 s % 21.41/3.30 % (814874)Peak memory usage: 14 MB % 21.41/3.30 % (814874)Instructions burned: 477 (million) % 21.41/3.30 % (814895)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2541848495:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 21.41/3.30 % (814883)Instruction limit reached! % 21.41/3.30 % (814883)------------------------------ % 21.41/3.30 % (814883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.41/3.30 % (814883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.08/4.25 % (814883)CaDiCaL version: 2.1.3 % 28.08/4.25 % (814883)Termination reason: Instruction limit % 28.08/4.25 % (814883)Termination phase: Saturation % 28.08/4.25 % (814883)Time elapsed: 0.430 s % 28.08/4.25 % (814883)Peak memory usage: 19 MB % 28.08/4.25 % (814883)Instructions burned: 693 (million) % 28.08/4.25 % (814897)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3437151956:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 28.08/4.25 % (814897)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.08/4.25 % (814897)Terminated due to inappropriate strategy. % 28.08/4.25 % (814897)------------------------------ % 28.08/4.25 % (814897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.08/4.25 % (814897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.08/4.25 % (814897)CaDiCaL version: 2.1.3 % 28.08/4.25 % (814897)Termination reason: Inappropriate % 28.08/4.25 % (814897)Time elapsed: 0.006 s % 28.08/4.25 % (814897)Peak memory usage: 10 MB % 28.08/4.25 % (814897)Instructions burned: 10 (million) % 28.08/4.25 % (814897)------------------------------ % 28.08/4.25 % (814897)------------------------------ % 28.08/4.25 % (814899)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1138338233:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 28.08/4.25 % (814899)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.08/4.25 % (814899)Terminated due to inappropriate strategy. % 28.08/4.25 % (814899)------------------------------ % 28.08/4.25 % (814899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.08/4.25 % (814899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.08/4.25 % (814899)CaDiCaL version: 2.1.3 % 28.08/4.25 % (814899)Termination reason: Inappropriate % 28.08/4.25 % (814899)Time elapsed: 0.005 s % 28.08/4.25 % (814899)Peak memory usage: 10 MB % 28.08/4.25 % (814899)Instructions burned: 8 (million) % 28.08/4.25 % (814899)------------------------------ % 28.08/4.25 % (814899)------------------------------ % 28.08/4.25 % (814901)ott-2_1_sil=16000:newcnf=on:random_seed=527734610:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 28.08/4.25 % (814885)Instruction limit reached! % 28.08/4.25 % (814885)------------------------------ % 28.08/4.25 % (814885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.08/4.25 % (814885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.08/4.25 % (814885)CaDiCaL version: 2.1.3 % 28.08/4.25 % (814885)Termination reason: Instruction limit % 28.08/4.25 % (814885)Termination phase: Saturation % 28.08/4.25 % (814885)Time elapsed: 0.502 s % 28.08/4.25 % (814885)Peak memory usage: 18 MB % 28.08/4.25 % (814885)Instructions burned: 879 (million) % 28.08/4.25 % (814903)ott+10_1_sil=32000:tgt=ground:random_seed=2802357490:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 28.08/4.25 % (814879)Instruction limit reached! % 28.08/4.25 % (814879)------------------------------ % 28.08/4.25 % (814879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.08/4.25 % (814879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.08/4.25 % (814879)CaDiCaL version: 2.1.3 % 28.08/4.25 % (814879)Termination reason: Instruction limit % 28.08/4.25 % (814879)Termination phase: Saturation % 28.08/4.25 % (814879)Time elapsed: 0.732 s % 28.08/4.25 % (814879)Peak memory usage: 21 MB % 28.08/4.25 % (814879)Instructions burned: 1183 (million) % 28.08/4.25 % (814905)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4084833860:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 28.08/4.25 % (814905)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.08/4.25 % (814905)Terminated due to inappropriate strategy. % 28.08/4.25 % (814905)------------------------------ % 28.08/4.25 % (814905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.08/4.25 % (814905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.08/4.25 % (814905)CaDiCaL version: 2.1.3 % 28.08/4.25 % (814905)Termination reason: Inappropriate % 28.08/4.25 % (814905)Time elapsed: 0.006 s % 28.08/4.25 % (814905)Peak memory usage: 10 MB % 28.08/4.25 % (814905)Instructions burned: 10 (million) % 28.08/4.25 % (814905)------------------------------ % 28.08/4.25 % (814905)------------------------------ % 28.08/4.25 % (814907)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2549729209:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 28.08/4.25 % (814901)Instruction limit reached! % 116.87/16.74 % (814901)------------------------------ % 116.87/16.74 % (814901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.87/16.74 % (814901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.87/16.74 % (814901)CaDiCaL version: 2.1.3 % 116.87/16.74 % (814901)Termination reason: Instruction limit % 116.87/16.74 % (814901)Termination phase: Saturation % 116.87/16.74 % (814901)Time elapsed: 0.507 s % 116.87/16.74 % (814901)Peak memory usage: 18 MB % 116.87/16.74 % (814901)Instructions burned: 870 (million) % 116.87/16.74 % (814909)dis+21_1_sil=32000:sas=cadical:random_seed=3438482789:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 116.87/16.74 % (814895)Instruction limit reached! % 116.87/16.74 % (814895)------------------------------ % 116.87/16.74 % (814895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.87/16.74 % (814895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.87/16.74 % (814895)CaDiCaL version: 2.1.3 % 116.87/16.74 % (814895)Termination reason: Instruction limit % 116.87/16.74 % (814895)Termination phase: Saturation % 116.87/16.74 % (814895)Time elapsed: 0.814 s % 116.87/16.74 % (814895)Peak memory usage: 28 MB % 116.87/16.74 % (814895)Instructions burned: 1472 (million) % 116.87/16.74 % (814911)ott+11_1_sil=16000:gs=on:random_seed=3484819518:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 116.87/16.74 % (814893)Instruction limit reached! % 116.87/16.74 % (814893)------------------------------ % 116.87/16.74 % (814893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.87/16.74 % (814893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.87/16.74 % (814893)CaDiCaL version: 2.1.3 % 116.87/16.74 % (814893)Termination reason: Instruction limit % 116.87/16.74 % (814893)Termination phase: Saturation % 116.87/16.74 % (814893)Time elapsed: 1.545 s % 116.87/16.74 % (814893)Peak memory usage: 36 MB % 116.87/16.74 % (814893)Instructions burned: 5131 (million) % 116.87/16.74 % (814913)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2127448334:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 116.87/16.74 % (814913)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.87/16.74 % (814913)Terminated due to inappropriate strategy. % 116.87/16.74 % (814913)------------------------------ % 116.87/16.74 % (814913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.87/16.74 % (814913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.87/16.74 % (814913)CaDiCaL version: 2.1.3 % 116.87/16.74 % (814913)Termination reason: Inappropriate % 116.87/16.74 % (814913)Time elapsed: 0.002 s % 116.87/16.74 % (814913)Peak memory usage: 10 MB % 116.87/16.74 % (814913)Instructions burned: 9 (million) % 116.87/16.74 % (814913)------------------------------ % 116.87/16.74 % (814913)------------------------------ % 116.87/16.74 % (814915)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2813104238:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 116.87/16.74 % (814911)Instruction limit reached! % 116.87/16.74 % (814911)------------------------------ % 116.87/16.74 % (814911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.87/16.74 % (814911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.87/16.74 % (814911)CaDiCaL version: 2.1.3 % 116.87/16.74 % (814911)Termination reason: Instruction limit % 116.87/16.74 % (814911)Termination phase: Saturation % 116.87/16.74 % (814911)Time elapsed: 1.480 s % 116.87/16.74 % (814911)Peak memory usage: 29 MB % 116.87/16.74 % (814911)Instructions burned: 2252 (million) % 116.87/16.74 % (814917)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3681186981:i=29340_2972 on theBenchmark for (2972ds/29340Mi) % 116.87/16.74 % (814915)Instruction limit reached! % 116.87/16.74 % (814915)------------------------------ % 116.87/16.74 % (814915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.87/16.74 % (814915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.87/16.74 % (814915)CaDiCaL version: 2.1.3 % 116.87/16.74 % (814915)Termination reason: Instruction limit % 116.87/16.74 % (814915)Termination phase: Saturation % 116.87/16.74 % (814915)Time elapsed: 1.145 s % 116.87/16.74 % (814915)Peak memory usage: 43 MB % 116.87/16.74 % (814915)Instructions burned: 4593 (million) % 116.87/16.74 % (814907)Instruction limit reached! % 116.87/16.74 % (814907)------------------------------ % 116.87/16.74 % (814907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.79/19.78 % (814907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.79/19.78 % (814907)CaDiCaL version: 2.1.3 % 120.79/19.78 % (814907)Termination reason: Instruction limit % 120.79/19.78 % (814907)Termination phase: Saturation % 120.79/19.78 % (814907)Time elapsed: 2.124 s % 120.79/19.78 % (814907)Peak memory usage: 31 MB % 120.79/19.78 % (814907)Instructions burned: 3513 (million) % 120.79/19.78 % (814919)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3271511769:i=5211_2969 on theBenchmark for (2969ds/5211Mi) % 120.79/19.78 % (814920)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3117123543:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 120.79/19.78 % (814920)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 120.79/19.78 % (814920)Terminated due to inappropriate strategy. % 120.79/19.78 % (814920)------------------------------ % 120.79/19.78 % (814920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.79/19.78 % (814920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.79/19.78 % (814920)CaDiCaL version: 2.1.3 % 120.79/19.78 % (814920)Termination reason: Inappropriate % 120.79/19.78 % (814920)Time elapsed: 0.005 s % 120.79/19.78 % (814920)Peak memory usage: 10 MB % 120.79/19.78 % (814920)Instructions burned: 9 (million) % 120.79/19.78 % (814920)------------------------------ % 120.79/19.78 % (814920)------------------------------ % 120.79/19.78 % (814923)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1957174600:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 120.79/19.78 % (814923)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 120.79/19.78 % (814923)Terminated due to inappropriate strategy. % 120.79/19.78 % (814923)------------------------------ % 120.79/19.78 % (814923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.79/19.78 % (814923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.79/19.78 % (814923)CaDiCaL version: 2.1.3 % 120.79/19.78 % (814923)Termination reason: Inappropriate % 120.79/19.78 % (814923)Time elapsed: 0.005 s % 120.79/19.78 % (814923)Peak memory usage: 10 MB % 120.79/19.78 % (814923)Instructions burned: 9 (million) % 120.79/19.78 % (814923)------------------------------ % 120.79/19.78 % (814923)------------------------------ % 120.79/19.78 % (814925)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=905044670:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 120.79/19.78 % (814925)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 120.79/19.78 % (814925)Terminated due to inappropriate strategy. % 120.79/19.78 % (814925)------------------------------ % 120.79/19.78 % (814925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.79/19.78 % (814925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.79/19.78 % (814925)CaDiCaL version: 2.1.3 % 120.79/19.78 % (814925)Termination reason: Inappropriate % 120.79/19.78 % (814925)Time elapsed: 0.005 s % 120.79/19.78 % (814925)Peak memory usage: 10 MB % 120.79/19.78 % (814925)Instructions burned: 9 (million) % 120.79/19.78 % (814925)------------------------------ % 120.79/19.78 % (814925)------------------------------ % 120.79/19.78 % (814927)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2498200554:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 120.79/19.78 % (814909)Instruction limit reached! % 120.79/19.78 % (814909)------------------------------ % 120.79/19.78 % (814909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.79/19.78 % (814909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.79/19.78 % (814909)CaDiCaL version: 2.1.3 % 120.79/19.78 % (814909)Termination reason: Instruction limit % 120.79/19.78 % (814909)Termination phase: Saturation % 120.79/19.78 % (814909)Time elapsed: 2.232 s % 120.79/19.78 % (814909)Peak memory usage: 28 MB % 120.79/19.78 % (814909)Instructions burned: 3774 (million) % 120.79/19.78 % (814929)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1041224358:i=8173:av=off_2965 on theBenchmark for (2965ds/8173Mi) % 120.79/19.78 % (814903)Instruction limit reached! % 120.79/19.78 % (814903)------------------------------ % 120.79/19.78 % (814903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.79/19.78 % (814903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.79/19.78 % (814903)CaDiCaL version: 2.1.3 % 120.79/19.78 % (814903)Termination reason: Instruction limit % 120.79/19.78 % (814903)Termination phase: Saturation % 120.79/19.78 % (814903)Time elapsed: 3.241 s % 138.90/19.91 % (814903)Peak memory usage: 36 MB % 138.90/19.91 % (814903)Instructions burned: 5114 (million) % 138.90/19.91 % (814931)dis+10_16:1_sil=16000:random_seed=2088395184:i=9155:fsr=off_2959 on theBenchmark for (2959ds/9155Mi) % 138.90/19.91 % (814919)Instruction limit reached! % 138.90/19.91 % (814919)------------------------------ % 138.90/19.91 % (814919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.90/19.91 % (814919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.90/19.91 % (814919)CaDiCaL version: 2.1.3 % 138.90/19.91 % (814919)Termination reason: Instruction limit % 138.90/19.91 % (814919)Termination phase: Saturation % 138.90/19.91 % (814919)Time elapsed: 1.508 s % 138.90/19.91 % (814919)Peak memory usage: 44 MB % 138.90/19.91 % (814919)Instructions burned: 5214 (million) % 138.90/19.91 % (814933)ott-3_8_sil=64000:random_seed=4231103991:i=20139:bs=on_2954 on theBenchmark for (2954ds/20139Mi) % 138.90/19.91 % (814929)Instruction limit reached! % 138.90/19.91 % (814929)------------------------------ % 138.90/19.91 % (814929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.90/19.91 % (814929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.90/19.91 % (814929)CaDiCaL version: 2.1.3 % 138.90/19.91 % (814929)Termination reason: Instruction limit % 138.90/19.91 % (814929)Termination phase: Saturation % 138.90/19.91 % (814929)Time elapsed: 5.484 s % 138.90/19.91 % (814929)Peak memory usage: 71 MB % 138.90/19.91 % (814929)Instructions burned: 8174 (million) % 138.90/19.91 % (814935)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3035971999:fmbsr=2:i=32576_2910 on theBenchmark for (2910ds/32576Mi) % 138.90/19.91 % (814935)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 138.90/19.91 % (814935)Terminated due to inappropriate strategy. % 138.90/19.91 % (814935)------------------------------ % 138.90/19.91 % (814935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.90/19.91 % (814935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.90/19.91 % (814935)CaDiCaL version: 2.1.3 % 138.90/19.91 % (814935)Termination reason: Inappropriate % 138.90/19.91 % (814935)Time elapsed: 0.006 s % 138.90/19.91 % (814935)Peak memory usage: 11 MB % 138.90/19.91 % (814935)Instructions burned: 11 (million) % 138.90/19.91 % (814935)------------------------------ % 138.90/19.91 % (814935)------------------------------ % 138.90/19.91 % (814937)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=711338385:i=11404_2909 on theBenchmark for (2909ds/11404Mi) % 138.90/19.91 % (814931)Instruction limit reached! % 138.90/19.91 % (814931)------------------------------ % 138.90/19.91 % (814931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.90/19.91 % (814931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.90/19.91 % (814931)CaDiCaL version: 2.1.3 % 138.90/19.91 % (814931)Termination reason: Instruction limit % 138.90/19.91 % (814931)Termination phase: Saturation % 138.90/19.91 % (814931)Time elapsed: 5.052 s % 138.90/19.91 % (814931)Peak memory usage: 49 MB % 138.90/19.91 % (814931)Instructions burned: 9155 (million) % 138.90/19.91 % (814939)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2591959397:i=14134_2909 on theBenchmark for (2909ds/14134Mi) % 138.90/19.91 % (814933)Instruction limit reached! % 138.90/19.91 % (814933)------------------------------ % 138.90/19.91 % (814933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.90/19.91 % (814933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.90/19.91 % (814933)CaDiCaL version: 2.1.3 % 138.90/19.91 % (814933)Termination reason: Instruction limit % 138.90/19.91 % (814933)Termination phase: Saturation % 138.90/19.91 % (814933)Time elapsed: 6.978 s % 138.90/19.91 % (814933)Peak memory usage: 125 MB % 138.90/19.91 % (814933)Instructions burned: 20141 (million) % 138.90/19.91 % (815093)dis+33_16_sil=32000:sac=on:random_seed=3184435725:i=15851:nm=0_2884 on theBenchmark for (2884ds/15851Mi) % 138.90/19.91 % (815093)Instruction limit reached! % 138.90/19.91 % (815093)------------------------------ % 138.90/19.91 % (815093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.90/19.91 % (815093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.90/19.91 % (815093)CaDiCaL version: 2.1.3 % 138.90/19.91 % (815093)Termination reason: Instruction limit % 138.90/19.91 % (815093)Termination phase: Saturation % 138.90/19.91 % (815093)Time elapsed: 4.880 s % 138.90/19.91 % (815093)Peak memory usage: 114 MB % 138.90/19.91 % (815093)Instructions burned: 15852 (million) % 138.90/19.91 % (815395)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1559872704:avsq=on:i=17627:add=on:amm=off_2835 on theBenchmark for (2835ds/17627Mi) % 143.04/20.44 % (814937)Instruction limit reached! % 143.04/20.44 % (814937)------------------------------ % 143.04/20.44 % (814937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.04/20.44 % (814937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.04/20.44 % (814937)CaDiCaL version: 2.1.3 % 143.04/20.44 % (814937)Termination reason: Instruction limit % 143.04/20.44 % (814937)Termination phase: Saturation % 143.04/20.44 % (814937)Time elapsed: 8.297 s % 143.04/20.44 % (814937)Peak memory usage: 54 MB % 143.04/20.44 % (814937)Instructions burned: 11405 (million) % 143.04/20.44 % (815397)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1429087724:s2a=on:i=53295_2826 on theBenchmark for (2826ds/53295Mi) % 143.04/20.44 % (814939)Instruction limit reached! % 143.04/20.44 % (814939)------------------------------ % 143.04/20.44 % (814939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.04/20.44 % (814939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.04/20.44 % (814939)CaDiCaL version: 2.1.3 % 143.04/20.44 % (814939)Termination reason: Instruction limit % 143.04/20.44 % (814939)Termination phase: Saturation % 143.04/20.44 % (814939)Time elapsed: 9.840 s % 143.04/20.44 % (814939)Peak memory usage: 57 MB % 143.04/20.44 % (814939)Instructions burned: 14135 (million) % 143.04/20.44 % (815399)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1154428247:i=26857:ins=20_2810 on theBenchmark for (2810ds/26857Mi) % 143.04/20.44 % (815399)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.04/20.44 % (815399)Terminated due to inappropriate strategy. % 143.04/20.44 % (815399)------------------------------ % 143.04/20.44 % (815399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.04/20.44 % (815399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.04/20.44 % (815399)CaDiCaL version: 2.1.3 % 143.04/20.44 % (815399)Termination reason: Inappropriate % 143.04/20.44 % (815399)Time elapsed: 0.005 s % 143.04/20.44 % (815399)Peak memory usage: 10 MB % 143.04/20.44 % (815399)Instructions burned: 9 (million) % 143.04/20.44 % (815399)------------------------------ % 143.04/20.44 % (815399)------------------------------ % 143.04/20.44 % (815401)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3377167841:i=28120:bs=on:fsr=off_2810 on theBenchmark for (2810ds/28120Mi) % 143.04/20.44 % (814917)Instruction limit reached! % 143.04/20.44 % (814917)------------------------------ % 143.04/20.44 % (814917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.04/20.44 % (814917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.04/20.44 % (814917)CaDiCaL version: 2.1.3 % 143.04/20.44 % (814917)Termination reason: Instruction limit % 143.04/20.44 % (814917)Termination phase: Saturation % 143.04/20.44 % (814917)Time elapsed: 16.659 s % 143.04/20.44 % (814917)Peak memory usage: 298 MB % 143.04/20.44 % (814917)Instructions burned: 29342 (million) % 143.04/20.44 % (815403)fmb+10_1_sil=256000:fmbss=7:random_seed=2367932711:fmbsr=1.6:i=182295_2805 on theBenchmark for (2805ds/182295Mi) % 143.04/20.44 % (815403)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.04/20.44 % (815403)Terminated due to inappropriate strategy. % 143.04/20.44 % (815403)------------------------------ % 143.04/20.44 % (815403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.04/20.44 % (815403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.04/20.44 % (815403)CaDiCaL version: 2.1.3 % 143.04/20.44 % (815403)Termination reason: Inappropriate % 143.04/20.44 % (815403)Time elapsed: 0.005 s % 143.04/20.44 % (815403)Peak memory usage: 10 MB % 143.04/20.44 % (815403)Instructions burned: 8 (million) % 143.04/20.44 % (815403)------------------------------ % 143.04/20.44 % (815403)------------------------------ % 143.04/20.44 % (815405)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3049343301:i=44625:gsp=on_2804 on theBenchmark for (2804ds/44625Mi) % 143.04/20.44 % (815405)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.04/20.44 % (815405)Terminated due to inappropriate strategy. % 143.04/20.44 % (815405)------------------------------ % 143.04/20.44 % (815405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.04/20.44 % (815405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.04/20.44 % (815405)CaDiCaL version: 2.1.3 % 143.04/20.44 % (815405)Termination reason: Inappropriate % 155.86/22.28 % (815405)Time elapsed: 0.005 s % 155.86/22.28 % (815405)Peak memory usage: 10 MB % 155.86/22.28 % (815405)Instructions burned: 9 (million) % 155.86/22.28 % (815405)------------------------------ % 155.86/22.28 % (815405)------------------------------ % 155.86/22.28 % (815407)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2573634719:i=160505_2804 on theBenchmark for (2804ds/160505Mi) % 155.86/22.28 % (815407)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.86/22.28 % (815407)Terminated due to inappropriate strategy. % 155.86/22.28 % (815407)------------------------------ % 155.86/22.28 % (815407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.86/22.28 % (815407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.86/22.28 % (815407)CaDiCaL version: 2.1.3 % 155.86/22.28 % (815407)Termination reason: Inappropriate % 155.86/22.28 % (815407)Time elapsed: 0.005 s % 155.86/22.28 % (815407)Peak memory usage: 10 MB % 155.86/22.28 % (815407)Instructions burned: 8 (million) % 155.86/22.28 % (815407)------------------------------ % 155.86/22.28 % (815407)------------------------------ % 155.86/22.28 % (815409)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2817040276:fmbsr=1.3:i=225729_2804 on theBenchmark for (2804ds/225729Mi) % 155.86/22.28 % (815409)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.86/22.28 % (815409)Terminated due to inappropriate strategy. % 155.86/22.28 % (815409)------------------------------ % 155.86/22.28 % (815409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.86/22.28 % (815409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.86/22.28 % (815409)CaDiCaL version: 2.1.3 % 155.86/22.28 % (815409)Termination reason: Inappropriate % 155.86/22.28 % (815409)Time elapsed: 0.005 s % 155.86/22.28 % (815409)Peak memory usage: 10 MB % 155.86/22.28 % (815409)Instructions burned: 9 (million) % 155.86/22.28 % (814927)Instruction limit reached! % 155.86/22.28 % (814927)------------------------------ % 155.86/22.28 % (814927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.86/22.28 % (814927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.86/22.28 % (814927)CaDiCaL version: 2.1.3 % 155.86/22.28 % (814927)Termination reason: Instruction limit % 155.86/22.28 % (814927)Termination phase: Saturation % 155.86/22.28 % (814927)Time elapsed: 16.434 s % 155.86/22.28 % (814927)Peak memory usage: 270 MB % 155.86/22.28 % (814927)Instructions burned: 22566 (million) % 155.86/22.28 % (815409)------------------------------ % 155.86/22.28 % (815409)------------------------------ % 155.86/22.28 % (815411)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3773223473:fmbsr=2:i=185024:ins=7_2804 on theBenchmark for (2804ds/185024Mi) % 155.86/22.28 % (815411)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.86/22.28 % (815411)Terminated due to inappropriate strategy. % 155.86/22.28 % (815411)------------------------------ % 155.86/22.28 % (815411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.86/22.28 % (815411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.86/22.28 % (815411)CaDiCaL version: 2.1.3 % 155.86/22.28 % (815411)Termination reason: Inappropriate % 155.86/22.28 % (815411)Time elapsed: 0.005 s % 155.86/22.28 % (815411)Peak memory usage: 10 MB % 155.86/22.28 % (815411)Instructions burned: 10 (million) % 155.86/22.28 % (815411)------------------------------ % 155.86/22.28 % (815411)------------------------------ % 155.86/22.28 % (815413)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3956697830:rtra=on_2803 on theBenchmark for (2803ds/0Mi) % 155.86/22.28 % (815414)% WARNING: option uhcvi not known. % 155.86/22.28 % (815413)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.86/22.28 % (815413)Terminated due to inappropriate strategy. % 155.86/22.28 % (815413)------------------------------ % 155.86/22.28 % (815413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.86/22.28 % (815413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.86/22.28 % (815413)CaDiCaL version: 2.1.3 % 155.86/22.28 % (815413)Termination reason: Inappropriate % 155.86/22.28 % (815413)Time elapsed: 0.006 s % 155.86/22.28 % (815413)Peak memory usage: 11 MB % 155.86/22.28 % (815413)Instructions burned: 11 (million) % 155.86/22.28 % (815413)------------------------------ % 155.86/22.28 % (815413)------------------------------ % 155.86/22.28 % (815414)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4131892527:i=271062:add=off:rtra=on:rawr=on_2803 on theBenchmark for (2803ds/271062Mi) % 155.86/22.28 % (815416)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1293082483:i=176048:add=on:rtra=on:rawr=on_2803 on theBenchmark for (2803ds/176048Mi) % 164.41/23.41 % (815395)Instruction limit reached! % 164.41/23.41 % (815395)------------------------------ % 164.41/23.41 % (815395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.41/23.41 % (815395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.41/23.41 % (815395)CaDiCaL version: 2.1.3 % 164.41/23.41 % (815395)Termination reason: Instruction limit % 164.41/23.41 % (815395)Termination phase: Saturation % 164.41/23.41 % (815395)Time elapsed: 3.285 s % 164.41/23.41 % (815395)Peak memory usage: 46 MB % 164.41/23.41 % (815395)Instructions burned: 17627 (million) % 164.41/23.41 % (815419)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1280831319:i=206:fgj=on:rtra=on_2802 on theBenchmark for (2802ds/206Mi) % 164.41/23.41 % (815419)Instruction limit reached! % 164.41/23.41 % (815419)------------------------------ % 164.41/23.41 % (815419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.41/23.41 % (815419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.41/23.41 % (815419)CaDiCaL version: 2.1.3 % 164.41/23.41 % (815419)Termination reason: Instruction limit % 164.41/23.41 % (815419)Termination phase: Saturation % 164.41/23.41 % (815419)Time elapsed: 0.072 s % 164.41/23.41 % (815419)Peak memory usage: 14 MB % 164.41/23.41 % (815419)Instructions burned: 208 (million) % 164.41/23.41 % (815421)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3690755475:i=232:rtra=on_2801 on theBenchmark for (2801ds/232Mi) % 164.41/23.41 % (815421)Instruction limit reached! % 164.41/23.41 % (815421)------------------------------ % 164.41/23.41 % (815421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.41/23.41 % (815421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.41/23.41 % (815421)CaDiCaL version: 2.1.3 % 164.41/23.41 % (815421)Termination reason: Instruction limit % 164.41/23.41 % (815421)Termination phase: Saturation % 164.41/23.41 % (815421)Time elapsed: 0.080 s % 164.41/23.41 % (815421)Peak memory usage: 14 MB % 164.41/23.41 % (815421)Instructions burned: 233 (million) % 164.41/23.41 % (815423)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=131215940:i=262:rtra=on_2800 on theBenchmark for (2800ds/262Mi) % 164.41/23.41 % (815423)Instruction limit reached! % 164.41/23.41 % (815423)------------------------------ % 164.41/23.41 % (815423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.41/23.41 % (815423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.41/23.41 % (815423)CaDiCaL version: 2.1.3 % 164.41/23.41 % (815423)Termination reason: Instruction limit % 164.41/23.41 % (815423)Termination phase: Saturation % 164.41/23.41 % (815423)Time elapsed: 0.088 s % 164.41/23.41 % (815423)Peak memory usage: 14 MB % 164.41/23.41 % (815423)Instructions burned: 262 (million) % 164.41/23.41 % (815425)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=4288576019:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2799 on theBenchmark for (2799ds/318Mi) % 164.41/23.41 % (815425)Instruction limit reached! % 164.41/23.41 % (815425)------------------------------ % 164.41/23.41 % (815425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.41/23.41 % (815425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.41/23.41 % (815425)CaDiCaL version: 2.1.3 % 164.41/23.41 % (815425)Termination reason: Instruction limit % 164.41/23.41 % (815425)Termination phase: Saturation % 164.41/23.41 % (815425)Time elapsed: 0.117 s % 164.41/23.41 % (815425)Peak memory usage: 15 MB % 164.41/23.41 % (815425)Instructions burned: 321 (million) % 164.41/23.41 % (815428)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1099149194:i=1428:nm=2:rtra=on_2798 on theBenchmark for (2798ds/1428Mi) % 164.41/23.41 % (815428)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 164.41/23.41 % (815428)Terminated due to inappropriate strategy. % 164.41/23.41 % (815428)------------------------------ % 164.41/23.41 % (815428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.41/23.41 % (815428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.41/23.41 % (815428)CaDiCaL version: 2.1.3 % 164.41/23.41 % (815428)Termination reason: Inappropriate % 164.41/23.41 % (815428)Time elapsed: 0.003 s % 164.41/23.41 % (815428)Peak memory usage: 11 MB % 164.41/23.41 % (815428)Instructions burned: 9 (million) % 164.41/23.41 % (815428)------------------------------ % 198.51/28.27 % (815428)------------------------------ % 198.51/28.27 % (815430)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=662016982:i=262:bd=preordered:rtra=on:fsd=on_2798 on theBenchmark for (2798ds/262Mi) % 198.51/28.27 % (815430)Instruction limit reached! % 198.51/28.27 % (815430)------------------------------ % 198.51/28.27 % (815430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.51/28.27 % (815430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.51/28.27 % (815430)CaDiCaL version: 2.1.3 % 198.51/28.27 % (815430)Termination reason: Instruction limit % 198.51/28.27 % (815430)Termination phase: Saturation % 198.51/28.27 % (815430)Time elapsed: 0.112 s % 198.51/28.27 % (815430)Peak memory usage: 14 MB % 198.51/28.27 % (815430)Instructions burned: 262 (million) % 198.51/28.27 % (815432)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=1935456641:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2796 on theBenchmark for (2796ds/1368Mi) % 198.51/28.27 % (815432)Instruction limit reached! % 198.51/28.27 % (815432)------------------------------ % 198.51/28.27 % (815432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.51/28.27 % (815432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.51/28.27 % (815432)CaDiCaL version: 2.1.3 % 198.51/28.27 % (815432)Termination reason: Instruction limit % 198.51/28.27 % (815432)Termination phase: Saturation % 198.51/28.27 % (815432)Time elapsed: 0.380 s % 198.51/28.27 % (815432)Peak memory usage: 19 MB % 198.51/28.27 % (815432)Instructions burned: 1368 (million) % 198.51/28.27 % (815434)ott-21_1_sil=16000:si=on:fs=off:random_seed=3644211657:i=360:av=off:fsr=off:rtra=on_2792 on theBenchmark for (2792ds/360Mi) % 198.51/28.27 % (815434)Instruction limit reached! % 198.51/28.27 % (815434)------------------------------ % 198.51/28.27 % (815434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.51/28.27 % (815434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.51/28.27 % (815434)CaDiCaL version: 2.1.3 % 198.51/28.27 % (815434)Termination reason: Instruction limit % 198.51/28.27 % (815434)Termination phase: Saturation % 198.51/28.27 % (815434)Time elapsed: 0.100 s % 198.51/28.27 % (815434)Peak memory usage: 14 MB % 198.51/28.27 % (815434)Instructions burned: 364 (million) % 198.51/28.27 % (815436)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=20423085:i=954:bd=all:rtra=on_2791 on theBenchmark for (2791ds/954Mi) % 198.51/28.27 % (815436)Instruction limit reached! % 198.51/28.27 % (815436)------------------------------ % 198.51/28.27 % (815436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.51/28.27 % (815436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.51/28.27 % (815436)CaDiCaL version: 2.1.3 % 198.51/28.27 % (815436)Termination reason: Instruction limit % 198.51/28.27 % (815436)Termination phase: Saturation % 198.51/28.27 % (815436)Time elapsed: 0.348 s % 198.51/28.27 % (815436)Peak memory usage: 16 MB % 198.51/28.27 % (815436)Instructions burned: 955 (million) % 198.51/28.27 % (815438)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=330541027:fmbsr=1.3:i=1730:ins=25:rtra=on_2788 on theBenchmark for (2788ds/1730Mi) % 198.51/28.27 % (815438)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 198.51/28.27 % (815438)Terminated due to inappropriate strategy. % 198.51/28.27 % (815438)------------------------------ % 198.51/28.27 % (815438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.51/28.27 % (815438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.51/28.27 % (815438)CaDiCaL version: 2.1.3 % 198.51/28.27 % (815438)Termination reason: Inappropriate % 198.51/28.27 % (815438)Time elapsed: 0.003 s % 198.51/28.27 % (815438)Peak memory usage: 10 MB % 198.51/28.27 % (815438)Instructions burned: 9 (million) % 198.51/28.27 % (815438)------------------------------ % 198.51/28.27 % (815438)------------------------------ % 198.51/28.27 % (815440)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3900834094:i=2358:rtra=on_2787 on theBenchmark for (2787ds/2358Mi) % 198.51/28.27 % (815440)Instruction limit reached! % 198.51/28.27 % (815440)------------------------------ % 198.51/28.27 % (815440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.51/28.27 % (815440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.51/28.27 % (815440)CaDiCaL version: 2.1.3 % 198.51/28.27 % (815440)Termination reason: Instruction limit % 198.51/28.27 % (815440)Termination phase: Saturation % 260.23/36.99 % (815440)Time elapsed: 0.818 s % 260.23/36.99 % (815440)Peak memory usage: 29 MB % 260.23/36.99 % (815440)Instructions burned: 2360 (million) % 260.23/36.99 % (815442)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1725671960:i=1778:ins=1:rtra=on_2779 on theBenchmark for (2779ds/1778Mi) % 260.23/36.99 % (815442)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 260.23/36.99 % (815442)Terminated due to inappropriate strategy. % 260.23/36.99 % (815442)------------------------------ % 260.23/36.99 % (815442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.23/36.99 % (815442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.23/36.99 % (815442)CaDiCaL version: 2.1.3 % 260.23/36.99 % (815442)Termination reason: Inappropriate % 260.23/36.99 % (815442)Time elapsed: 0.003 s % 260.23/36.99 % (815442)Peak memory usage: 10 MB % 260.23/36.99 % (815442)Instructions burned: 9 (million) % 260.23/36.99 % (815442)------------------------------ % 260.23/36.99 % (815442)------------------------------ % 260.23/36.99 % (815444)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=794319812:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2779 on theBenchmark for (2779ds/1384Mi) % 260.23/36.99 % (815444)Instruction limit reached! % 260.23/36.99 % (815444)------------------------------ % 260.23/36.99 % (815444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.23/36.99 % (815444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.23/36.99 % (815444)CaDiCaL version: 2.1.3 % 260.23/36.99 % (815444)Termination reason: Instruction limit % 260.23/36.99 % (815444)Termination phase: Saturation % 260.23/36.99 % (815444)Time elapsed: 0.499 s % 260.23/36.99 % (815444)Peak memory usage: 25 MB % 260.23/36.99 % (815444)Instructions burned: 1385 (million) % 260.23/36.99 % (815446)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1761606120:i=1758:kws=inv_precedence:fsr=off:rtra=on_2774 on theBenchmark for (2774ds/1758Mi) % 260.23/36.99 % (815446)Instruction limit reached! % 260.23/36.99 % (815446)------------------------------ % 260.23/36.99 % (815446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.23/36.99 % (815446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.23/36.99 % (815446)CaDiCaL version: 2.1.3 % 260.23/36.99 % (815446)Termination reason: Instruction limit % 260.23/36.99 % (815446)Termination phase: Saturation % 260.23/36.99 % (815446)Time elapsed: 0.550 s % 260.23/36.99 % (815446)Peak memory usage: 24 MB % 260.23/36.99 % (815446)Instructions burned: 1761 (million) % 260.23/36.99 % (815448)fmb+10_1_sil=64000:si=on:random_seed=2393117535:i=44122:nm=2:rtra=on:gsp=on_2768 on theBenchmark for (2768ds/44122Mi) % 260.23/36.99 % (815448)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 260.23/36.99 % (815448)Terminated due to inappropriate strategy. % 260.23/36.99 % (815448)------------------------------ % 260.23/36.99 % (815448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.23/36.99 % (815448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.23/36.99 % (815448)CaDiCaL version: 2.1.3 % 260.23/36.99 % (815448)Termination reason: Inappropriate % 260.23/36.99 % (815448)Time elapsed: 0.003 s % 260.23/36.99 % (815448)Peak memory usage: 11 MB % 260.23/36.99 % (815448)Instructions burned: 10 (million) % 260.23/36.99 % (815448)------------------------------ % 260.23/36.99 % (815448)------------------------------ % 260.23/36.99 % (815450)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=450750731:i=19030:nm=5:rtra=on_2768 on theBenchmark for (2768ds/19030Mi) % 260.23/36.99 % (815450)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 260.23/36.99 % (815450)Terminated due to inappropriate strategy. % 260.23/36.99 % (815450)------------------------------ % 260.23/36.99 % (815450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.23/36.99 % (815450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.23/36.99 % (815450)CaDiCaL version: 2.1.3 % 260.23/36.99 % (815450)Termination reason: Inappropriate % 260.23/36.99 % (815450)Time elapsed: 0.003 s % 260.23/36.99 % (815450)Peak memory usage: 11 MB % 260.23/36.99 % (815450)Instructions burned: 9 (million) % 260.23/36.99 % (815450)------------------------------ % 260.23/36.99 % (815450)------------------------------ % 260.23/36.99 % (815452)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2035631770:fmbsr=1.7:i=1840:rtra=on_2768 on theBenchmark for (2768ds/1840Mi) % 300.73/42.64 % (815452)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.73/42.64 % (815452)Terminated due to inappropriate strategy. % 300.73/42.64 % (815452)------------------------------ % 300.73/42.64 % (815452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.73/42.64 % (815452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.73/42.64 % (815452)CaDiCaL version: 2.1.3 % 300.73/42.64 % (815452)Termination reason: Inappropriate % 300.73/42.64 % (815452)Time elapsed: 0.003 s % 300.73/42.64 % (815452)Peak memory usage: 11 MB % 300.73/42.64 % (815452)Instructions burned: 9 (million) % 300.73/42.64 % (815452)------------------------------ % 300.73/42.64 % (815452)------------------------------ % 300.73/42.64 % (815454)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3209874683:i=10262:rtra=on_2768 on theBenchmark for (2768ds/10262Mi) % 300.73/42.64 % (815454)Instruction limit reached! % 300.73/42.64 % (815454)------------------------------ % 300.73/42.64 % (815454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.73/42.64 % (815454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.73/42.64 % (815454)CaDiCaL version: 2.1.3 % 300.73/42.64 % (815454)Termination reason: Instruction limit % 300.73/42.64 % (815454)Termination phase: Saturation % 300.73/42.64 % (815454)Time elapsed: 3.330 s % 300.73/42.64 % (815454)Peak memory usage: 54 MB % 300.73/42.64 % (815454)Instructions burned: 10264 (million) % 300.73/42.64 % (815747)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2001849013:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2734 on theBenchmark for (2734ds/2944Mi) % 300.73/42.64 % (815747)Instruction limit reached! % 300.73/42.64 % (815747)------------------------------ % 300.73/42.64 % (815747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.73/42.64 % (815747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.73/42.64 % (815747)CaDiCaL version: 2.1.3 % 300.73/42.64 % (815747)Termination reason: Instruction limit % 300.73/42.64 % (815747)Termination phase: Saturation % 300.73/42.64 % (815747)Time elapsed: 0.871 s % 300.73/42.64 % (815747)Peak memory usage: 40 MB % 300.73/42.64 % (815747)Instructions burned: 2947 (million) % 300.73/42.64 % (815801)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1301769777:i=12648:rtra=on_2725 on theBenchmark for (2725ds/12648Mi) % 300.73/42.64 % (815801)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.73/42.64 % (815801)Terminated due to inappropriate strategy. % 300.73/42.64 % (815801)------------------------------ % 300.73/42.64 % (815801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.73/42.64 % (815801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.73/42.64 % (815801)CaDiCaL version: 2.1.3 % 300.73/42.64 % (815801)Termination reason: Inappropriate % 300.73/42.64 % (815801)Time elapsed: 0.003 s % 300.73/42.64 % (815801)Peak memory usage: 11 MB % 300.73/42.64 % (815801)Instructions burned: 10 (million) % 300.73/42.64 % (815801)------------------------------ % 300.73/42.64 % (815801)------------------------------ % 300.73/42.64 % (815803)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2714282147:fmbsr=2.30978:i=4348:rtra=on_2725 on theBenchmark for (2725ds/4348Mi) % 300.73/42.64 % (815803)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.73/42.64 % (815803)Terminated due to inappropriate strategy. % 300.73/42.64 % (815803)------------------------------ % 300.73/42.64 % (815803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.73/42.64 % (815803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.73/42.64 % (815803)CaDiCaL version: 2.1.3 % 300.73/42.64 % (815803)Termination reason: Inappropriate % 300.73/42.64 % (815803)Time elapsed: 0.003 s % 300.73/42.64 % (815803)Peak memory usage: 11 MB % 300.73/42.64 % (815803)Instructions burned: 9 (million) % 300.73/42.64 % (815803)------------------------------ % 300.73/42.64 % (815803)------------------------------ % 300.73/42.64 % (815805)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3477779635:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2725 on theBenchmark for (2725ds/1738Mi) % 300.73/42.64 % (815805)Instruction limit reached! % 300.73/42.64 % (815805)------------------------------ % 300.73/42.64 % (815805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.73/42.64 % (815805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c % 300.73/42.64 Terminated % 300.73/42.64 % Vampire exiting % 300.73/42.64 Terminated %------------------------------------------------------------------------------