%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC450_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n018.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:06:01 PM UTC 2026 % Result : Timeout 300.58s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC450_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.21 % Computer : n018.cluster.edu % 0.09/0.21 % Model : x86_64 x86_64 % 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.21 % Memory : 8046.5625MB % 0.09/0.21 % OS : Linux 6.8.0-71-generic % 0.09/0.21 % CPULimit : 300 % 0.09/0.21 % WCLimit : 300 % 0.09/0.21 % DateTime : Mon Sep 28 09:40:10 UTC 2026 % 0.09/0.21 % CPUTime : % 0.09/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.24 Running first-order model finding % 0.09/0.24 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.46/0.87 % (3255852)Will run a generic schedule for satisfiability detection. % 3.46/0.87 % (3255861)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2276633348:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.46/0.87 % (3255858)% WARNING: option uhcvi not known. % 3.46/0.87 % (3255857)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3938659543_2999 on theBenchmark for (2999ds/0Mi) % 3.46/0.87 % (3255859)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1599727825:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.46/0.87 % (3255860)dis+10_1_sil=32000:sp=arity:random_seed=602311926:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.46/0.87 % (3255862)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3941658275:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.46/0.87 % (3255863)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=751623296:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.46/0.87 % (3255857)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.46/0.87 % (3255857)Terminated due to inappropriate strategy. % 3.46/0.87 % (3255857)------------------------------ % 3.46/0.87 % (3255857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.46/0.87 % (3255857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.46/0.87 % (3255857)CaDiCaL version: 2.1.3 % 3.46/0.87 % (3255857)Termination reason: Inappropriate % 3.46/0.87 % (3255857)Time elapsed: 0.001 s % 3.46/0.87 % (3255857)Peak memory usage: 10 MB % 3.46/0.87 % (3255857)Instructions burned: 2 (million) % 3.46/0.87 % (3255857)------------------------------ % 3.46/0.87 % (3255857)------------------------------ % 3.46/0.87 % (3255858)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3222071379:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.46/0.87 % (3255870)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3595113763:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.46/0.87 % (3255870)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.46/0.87 % (3255870)Terminated due to inappropriate strategy. % 3.46/0.87 % (3255870)------------------------------ % 3.46/0.87 % (3255870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.46/0.87 % (3255870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.46/0.87 % (3255870)CaDiCaL version: 2.1.3 % 3.46/0.87 % (3255870)Termination reason: Inappropriate % 3.46/0.87 % (3255870)Time elapsed: 0.001 s % 3.46/0.87 % (3255870)Peak memory usage: 10 MB % 3.46/0.87 % (3255870)Instructions burned: 2 (million) % 3.46/0.87 % (3255870)------------------------------ % 3.46/0.87 % (3255870)------------------------------ % 3.46/0.87 % (3255861)Instruction limit reached! % 3.46/0.87 % (3255861)------------------------------ % 3.46/0.87 % (3255861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.46/0.87 % (3255861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.46/0.87 % (3255861)CaDiCaL version: 2.1.3 % 3.46/0.87 % (3255861)Termination reason: Instruction limit % 3.46/0.87 % (3255861)Termination phase: Saturation % 3.46/0.87 % (3255861)Time elapsed: 0.037 s % 3.46/0.87 % (3255861)Peak memory usage: 12 MB % 3.46/0.87 % (3255861)Instructions burned: 118 (million) % 3.46/0.87 % (3255874)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=579525814:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.46/0.87 % (3255873)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3049772002:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.46/0.87 % (3255860)Instruction limit reached! % 3.46/0.87 % (3255860)------------------------------ % 3.46/0.87 % (3255860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.46/0.87 % (3255860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.46/0.87 % (3255860)CaDiCaL version: 2.1.3 % 3.46/0.87 % (3255860)Termination reason: Instruction limit % 3.46/0.87 % (3255860)Termination phase: Saturation % 3.46/0.87 % (3255860)Time elapsed: 0.062 s % 3.46/0.87 % (3255860)Peak memory usage: 12 MB % 3.46/0.87 % (3255860)Instructions burned: 103 (million) % 3.46/0.87 % (3255862)Instruction limit reached! % 3.46/0.87 % (3255862)------------------------------ % 3.46/0.87 % (3255862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.51/1.09 % (3255862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.51/1.09 % (3255862)CaDiCaL version: 2.1.3 % 5.51/1.09 % (3255862)Termination reason: Instruction limit % 5.51/1.09 % (3255862)Termination phase: Saturation % 5.51/1.09 % (3255862)Time elapsed: 0.075 s % 5.51/1.09 % (3255862)Peak memory usage: 13 MB % 5.51/1.09 % (3255862)Instructions burned: 132 (million) % 5.51/1.09 % (3255877)ott-21_1_sil=16000:fs=off:random_seed=3695711385:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 5.51/1.09 % (3255878)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2001065505:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.51/1.09 % (3255863)Instruction limit reached! % 5.51/1.09 % (3255863)------------------------------ % 5.51/1.09 % (3255863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.51/1.09 % (3255863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.51/1.09 % (3255863)CaDiCaL version: 2.1.3 % 5.51/1.09 % (3255863)Termination reason: Instruction limit % 5.51/1.09 % (3255863)Termination phase: Saturation % 5.51/1.09 % (3255863)Time elapsed: 0.101 s % 5.51/1.09 % (3255863)Peak memory usage: 13 MB % 5.51/1.09 % (3255863)Instructions burned: 159 (million) % 5.51/1.09 % (3255873)Instruction limit reached! % 5.51/1.09 % (3255873)------------------------------ % 5.51/1.09 % (3255873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.51/1.09 % (3255873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.51/1.09 % (3255873)CaDiCaL version: 2.1.3 % 5.51/1.09 % (3255873)Termination reason: Instruction limit % 5.51/1.09 % (3255873)Termination phase: Saturation % 5.51/1.09 % (3255873)Time elapsed: 0.078 s % 5.51/1.09 % (3255873)Peak memory usage: 12 MB % 5.51/1.09 % (3255873)Instructions burned: 131 (million) % 5.51/1.09 % (3255881)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3919717455:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.51/1.09 % (3255881)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.51/1.09 % (3255881)Terminated due to inappropriate strategy. % 5.51/1.09 % (3255881)------------------------------ % 5.51/1.09 % (3255881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.51/1.09 % (3255881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.51/1.09 % (3255881)CaDiCaL version: 2.1.3 % 5.51/1.09 % (3255881)Termination reason: Inappropriate % 5.51/1.09 % (3255881)Time elapsed: 0.001 s % 5.51/1.09 % (3255881)Peak memory usage: 10 MB % 5.51/1.09 % (3255881)Instructions burned: 2 (million) % 5.51/1.09 % (3255881)------------------------------ % 5.51/1.09 % (3255881)------------------------------ % 5.51/1.09 % (3255883)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2746854434:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.51/1.09 % (3255884)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1535665145:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.51/1.09 % (3255884)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.51/1.09 % (3255884)Terminated due to inappropriate strategy. % 5.51/1.09 % (3255884)------------------------------ % 5.51/1.09 % (3255884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.51/1.09 % (3255884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.51/1.09 % (3255884)CaDiCaL version: 2.1.3 % 5.51/1.09 % (3255884)Termination reason: Inappropriate % 5.51/1.09 % (3255884)Time elapsed: 0.001 s % 5.51/1.09 % (3255884)Peak memory usage: 10 MB % 5.51/1.09 % (3255884)Instructions burned: 2 (million) % 5.51/1.09 % (3255884)------------------------------ % 5.51/1.09 % (3255884)------------------------------ % 5.51/1.09 % (3255877)Instruction limit reached! % 5.51/1.09 % (3255877)------------------------------ % 5.51/1.09 % (3255877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.51/1.09 % (3255877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.51/1.09 % (3255877)CaDiCaL version: 2.1.3 % 5.51/1.09 % (3255877)Termination reason: Instruction limit % 5.51/1.09 % (3255877)Termination phase: Saturation % 5.51/1.09 % (3255877)Time elapsed: 0.081 s % 5.51/1.09 % (3255877)Peak memory usage: 12 MB % 5.51/1.09 % (3255877)Instructions burned: 180 (million) % 5.51/1.09 % (3255887)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=693772285: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) % 17.27/2.84 % (3255888)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4041015893:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 17.27/2.84 % (3255874)Instruction limit reached! % 17.27/2.84 % (3255874)------------------------------ % 17.27/2.84 % (3255874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.27/2.84 % (3255874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.27/2.84 % (3255874)CaDiCaL version: 2.1.3 % 17.27/2.84 % (3255874)Termination reason: Instruction limit % 17.27/2.84 % (3255874)Termination phase: Saturation % 17.27/2.84 % (3255874)Time elapsed: 0.208 s % 17.27/2.84 % (3255874)Peak memory usage: 18 MB % 17.27/2.84 % (3255874)Instructions burned: 687 (million) % 17.27/2.84 % (3255891)fmb+10_1_sil=64000:random_seed=44280965:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 17.27/2.84 % (3255891)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.27/2.84 % (3255891)Terminated due to inappropriate strategy. % 17.27/2.84 % (3255891)------------------------------ % 17.27/2.84 % (3255891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.27/2.84 % (3255891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.27/2.84 % (3255891)CaDiCaL version: 2.1.3 % 17.27/2.84 % (3255891)Termination reason: Inappropriate % 17.27/2.84 % (3255891)Time elapsed: 0.001 s % 17.27/2.84 % (3255891)Peak memory usage: 11 MB % 17.27/2.84 % (3255891)Instructions burned: 2 (million) % 17.27/2.84 % (3255891)------------------------------ % 17.27/2.84 % (3255891)------------------------------ % 17.27/2.84 % (3255893)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=70293808:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 17.27/2.84 % (3255893)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.27/2.84 % (3255893)Terminated due to inappropriate strategy. % 17.27/2.84 % (3255893)------------------------------ % 17.27/2.84 % (3255893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.27/2.84 % (3255893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.27/2.84 % (3255893)CaDiCaL version: 2.1.3 % 17.27/2.84 % (3255893)Termination reason: Inappropriate % 17.27/2.84 % (3255893)Time elapsed: 0.001 s % 17.27/2.84 % (3255893)Peak memory usage: 10 MB % 17.27/2.84 % (3255893)Instructions burned: 2 (million) % 17.27/2.84 % (3255893)------------------------------ % 17.27/2.84 % (3255893)------------------------------ % 17.27/2.84 % (3255895)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=695106122:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 17.27/2.84 % (3255895)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.27/2.84 % (3255895)Terminated due to inappropriate strategy. % 17.27/2.84 % (3255895)------------------------------ % 17.27/2.84 % (3255895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.27/2.84 % (3255895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.27/2.84 % (3255895)CaDiCaL version: 2.1.3 % 17.27/2.84 % (3255895)Termination reason: Inappropriate % 17.27/2.84 % (3255895)Time elapsed: 0.0000 s % 17.27/2.84 % (3255895)Peak memory usage: 11 MB % 17.27/2.84 % (3255895)Instructions burned: 2 (million) % 17.27/2.84 % (3255895)------------------------------ % 17.27/2.84 % (3255895)------------------------------ % 17.27/2.84 % (3255897)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=810806762:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 17.27/2.84 % (3255878)Instruction limit reached! % 17.27/2.84 % (3255878)------------------------------ % 17.27/2.84 % (3255878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.27/2.84 % (3255878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.27/2.84 % (3255878)CaDiCaL version: 2.1.3 % 17.27/2.84 % (3255878)Termination reason: Instruction limit % 17.27/2.84 % (3255878)Termination phase: Saturation % 17.27/2.84 % (3255878)Time elapsed: 0.219 s % 17.27/2.84 % (3255878)Peak memory usage: 13 MB % 17.27/2.84 % (3255878)Instructions burned: 478 (million) % 17.27/2.84 % (3255899)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3508094122:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 17.27/2.84 % (3255887)Instruction limit reached! % 17.27/2.84 % (3255887)------------------------------ % 26.82/4.10 % (3255887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.82/4.10 % (3255887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.82/4.10 % (3255887)CaDiCaL version: 2.1.3 % 26.82/4.10 % (3255887)Termination reason: Instruction limit % 26.82/4.10 % (3255887)Termination phase: Saturation % 26.82/4.10 % (3255887)Time elapsed: 0.416 s % 26.82/4.10 % (3255887)Peak memory usage: 18 MB % 26.82/4.10 % (3255887)Instructions burned: 693 (million) % 26.82/4.10 % (3255901)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3692934819:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 26.82/4.10 % (3255901)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.82/4.10 % (3255901)Terminated due to inappropriate strategy. % 26.82/4.10 % (3255901)------------------------------ % 26.82/4.10 % (3255901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.82/4.10 % (3255901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.82/4.10 % (3255901)CaDiCaL version: 2.1.3 % 26.82/4.10 % (3255901)Termination reason: Inappropriate % 26.82/4.10 % (3255901)Time elapsed: 0.001 s % 26.82/4.10 % (3255901)Peak memory usage: 10 MB % 26.82/4.10 % (3255901)Instructions burned: 2 (million) % 26.82/4.10 % (3255901)------------------------------ % 26.82/4.10 % (3255901)------------------------------ % 26.82/4.10 % (3255903)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1116600780:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 26.82/4.10 % (3255903)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.82/4.10 % (3255903)Terminated due to inappropriate strategy. % 26.82/4.10 % (3255903)------------------------------ % 26.82/4.10 % (3255903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.82/4.10 % (3255903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.82/4.10 % (3255903)CaDiCaL version: 2.1.3 % 26.82/4.10 % (3255903)Termination reason: Inappropriate % 26.82/4.10 % (3255903)Time elapsed: 0.001 s % 26.82/4.10 % (3255903)Peak memory usage: 10 MB % 26.82/4.10 % (3255903)Instructions burned: 2 (million) % 26.82/4.10 % (3255903)------------------------------ % 26.82/4.10 % (3255903)------------------------------ % 26.82/4.10 % (3255905)ott-2_1_sil=16000:newcnf=on:random_seed=4262114036:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 26.82/4.10 % (3255888)Instruction limit reached! % 26.82/4.10 % (3255888)------------------------------ % 26.82/4.10 % (3255888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.82/4.10 % (3255888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.82/4.10 % (3255888)CaDiCaL version: 2.1.3 % 26.82/4.10 % (3255888)Termination reason: Instruction limit % 26.82/4.10 % (3255888)Termination phase: Saturation % 26.82/4.10 % (3255888)Time elapsed: 0.502 s % 26.82/4.10 % (3255888)Peak memory usage: 19 MB % 26.82/4.10 % (3255888)Instructions burned: 880 (million) % 26.82/4.10 % (3255907)ott+10_1_sil=32000:tgt=ground:random_seed=3141729052:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 26.82/4.10 % (3255883)Instruction limit reached! % 26.82/4.10 % (3255883)------------------------------ % 26.82/4.10 % (3255883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.82/4.10 % (3255883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.82/4.10 % (3255883)CaDiCaL version: 2.1.3 % 26.82/4.10 % (3255883)Termination reason: Instruction limit % 26.82/4.10 % (3255883)Termination phase: Saturation % 26.82/4.10 % (3255883)Time elapsed: 0.637 s % 26.82/4.10 % (3255883)Peak memory usage: 18 MB % 26.82/4.10 % (3255883)Instructions burned: 1180 (million) % 26.82/4.10 % (3255909)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3431998395:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 26.82/4.10 % (3255909)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.82/4.10 % (3255909)Terminated due to inappropriate strategy. % 26.82/4.10 % (3255909)------------------------------ % 26.82/4.10 % (3255909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.82/4.10 % (3255909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.82/4.10 % (3255909)CaDiCaL version: 2.1.3 % 26.82/4.10 % (3255909)Termination reason: Inappropriate % 26.82/4.10 % (3255909)Time elapsed: 0.001 s % 26.82/4.10 % (3255909)Peak memory usage: 10 MB % 26.82/4.10 % (3255909)Instructions burned: 2 (million) % 84.79/12.22 % (3255909)------------------------------ % 84.79/12.22 % (3255909)------------------------------ % 84.79/12.22 % (3255911)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=628443691:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 84.79/12.22 % (3255905)Instruction limit reached! % 84.79/12.22 % (3255905)------------------------------ % 84.79/12.22 % (3255905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.79/12.22 % (3255905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.79/12.22 % (3255905)CaDiCaL version: 2.1.3 % 84.79/12.22 % (3255905)Termination reason: Instruction limit % 84.79/12.22 % (3255905)Termination phase: Saturation % 84.79/12.22 % (3255905)Time elapsed: 0.467 s % 84.79/12.22 % (3255905)Peak memory usage: 17 MB % 84.79/12.22 % (3255905)Instructions burned: 870 (million) % 84.79/12.22 % (3255913)dis+21_1_sil=32000:sas=cadical:random_seed=2537873739:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 84.79/12.22 % (3255899)Instruction limit reached! % 84.79/12.22 % (3255899)------------------------------ % 84.79/12.22 % (3255899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.79/12.22 % (3255899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.79/12.22 % (3255899)CaDiCaL version: 2.1.3 % 84.79/12.22 % (3255899)Termination reason: Instruction limit % 84.79/12.22 % (3255899)Termination phase: Saturation % 84.79/12.22 % (3255899)Time elapsed: 0.877 s % 84.79/12.22 % (3255899)Peak memory usage: 27 MB % 84.79/12.22 % (3255899)Instructions burned: 1473 (million) % 84.79/12.22 % (3255915)ott+11_1_sil=16000:gs=on:random_seed=716854256:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 84.79/12.22 % (3255897)Instruction limit reached! % 84.79/12.22 % (3255897)------------------------------ % 84.79/12.22 % (3255897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.79/12.22 % (3255897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.79/12.22 % (3255897)CaDiCaL version: 2.1.3 % 84.79/12.22 % (3255897)Termination reason: Instruction limit % 84.79/12.22 % (3255897)Termination phase: Saturation % 84.79/12.22 % (3255897)Time elapsed: 1.454 s % 84.79/12.22 % (3255897)Peak memory usage: 42 MB % 84.79/12.22 % (3255897)Instructions burned: 5131 (million) % 84.79/12.22 % (3255917)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3703018156:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 84.79/12.22 % (3255917)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 84.79/12.22 % (3255917)Terminated due to inappropriate strategy. % 84.79/12.22 % (3255917)------------------------------ % 84.79/12.22 % (3255917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.79/12.22 % (3255917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.79/12.22 % (3255917)CaDiCaL version: 2.1.3 % 84.79/12.22 % (3255917)Termination reason: Inappropriate % 84.79/12.22 % (3255917)Time elapsed: 0.001 s % 84.79/12.22 % (3255917)Peak memory usage: 10 MB % 84.79/12.22 % (3255917)Instructions burned: 2 (million) % 84.79/12.22 % (3255917)------------------------------ % 84.79/12.22 % (3255917)------------------------------ % 84.79/12.22 % (3255919)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3692381518:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 84.79/12.22 % (3255915)Instruction limit reached! % 84.79/12.22 % (3255915)------------------------------ % 84.79/12.22 % (3255915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.79/12.22 % (3255915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.79/12.22 % (3255915)CaDiCaL version: 2.1.3 % 84.79/12.22 % (3255915)Termination reason: Instruction limit % 84.79/12.22 % (3255915)Termination phase: Saturation % 84.79/12.22 % (3255915)Time elapsed: 1.230 s % 84.79/12.22 % (3255915)Peak memory usage: 23 MB % 84.79/12.22 % (3255915)Instructions burned: 2252 (million) % 84.79/12.22 % (3255921)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1158483743:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 84.79/12.22 % (3255911)Instruction limit reached! % 84.79/12.22 % (3255911)------------------------------ % 84.79/12.22 % (3255911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.79/12.22 % (3255911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.79/12.22 % (3255911)CaDiCaL version: 2.1.3 % 84.79/12.22 % (3255911)Termination reason: Instruction limit % 119.09/17.11 % (3255911)Termination phase: Saturation % 119.09/17.11 % (3255911)Time elapsed: 1.732 s % 119.09/17.11 % (3255911)Peak memory usage: 27 MB % 119.09/17.11 % (3255911)Instructions burned: 3512 (million) % 119.09/17.11 % (3255923)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1495158762:i=5211_2974 on theBenchmark for (2974ds/5211Mi) % 119.09/17.11 % (3255919)Instruction limit reached! % 119.09/17.11 % (3255919)------------------------------ % 119.09/17.11 % (3255919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.09/17.11 % (3255919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.09/17.11 % (3255919)CaDiCaL version: 2.1.3 % 119.09/17.11 % (3255919)Termination reason: Instruction limit % 119.09/17.11 % (3255919)Termination phase: Saturation % 119.09/17.11 % (3255919)Time elapsed: 1.176 s % 119.09/17.11 % (3255919)Peak memory usage: 34 MB % 119.09/17.11 % (3255919)Instructions burned: 4593 (million) % 119.09/17.11 % (3255925)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=578836520:i=5497:nm=2_2970 on theBenchmark for (2970ds/5497Mi) % 119.09/17.11 % (3255925)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 119.09/17.11 % (3255925)Terminated due to inappropriate strategy. % 119.09/17.11 % (3255925)------------------------------ % 119.09/17.11 % (3255925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.09/17.11 % (3255925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.09/17.11 % (3255925)CaDiCaL version: 2.1.3 % 119.09/17.11 % (3255925)Termination reason: Inappropriate % 119.09/17.11 % (3255925)Time elapsed: 0.001 s % 119.09/17.11 % (3255925)Peak memory usage: 10 MB % 119.09/17.11 % (3255925)Instructions burned: 2 (million) % 119.09/17.11 % (3255925)------------------------------ % 119.09/17.11 % (3255925)------------------------------ % 119.09/17.11 % (3255927)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1191208061:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 119.09/17.11 % (3255927)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 119.09/17.11 % (3255927)Terminated due to inappropriate strategy. % 119.09/17.11 % (3255927)------------------------------ % 119.09/17.11 % (3255927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.09/17.11 % (3255927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.09/17.11 % (3255927)CaDiCaL version: 2.1.3 % 119.09/17.11 % (3255927)Termination reason: Inappropriate % 119.09/17.11 % (3255927)Time elapsed: 0.001 s % 119.09/17.11 % (3255927)Peak memory usage: 10 MB % 119.09/17.11 % (3255927)Instructions burned: 2 (million) % 119.09/17.11 % (3255927)------------------------------ % 119.09/17.11 % (3255927)------------------------------ % 119.09/17.11 % (3255929)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=940747697:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 119.09/17.11 % (3255929)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 119.09/17.11 % (3255929)Terminated due to inappropriate strategy. % 119.09/17.11 % (3255929)------------------------------ % 119.09/17.11 % (3255929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.09/17.11 % (3255929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.09/17.11 % (3255929)CaDiCaL version: 2.1.3 % 119.09/17.11 % (3255929)Termination reason: Inappropriate % 119.09/17.11 % (3255929)Time elapsed: 0.001 s % 119.09/17.11 % (3255929)Peak memory usage: 10 MB % 119.09/17.11 % (3255929)Instructions burned: 2 (million) % 119.09/17.11 % (3255929)------------------------------ % 119.09/17.11 % (3255929)------------------------------ % 119.09/17.11 % (3255931)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3106065389:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi) % 119.09/17.11 % (3255913)Instruction limit reached! % 119.09/17.11 % (3255913)------------------------------ % 119.09/17.11 % (3255913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.09/17.11 % (3255913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.09/17.11 % (3255913)CaDiCaL version: 2.1.3 % 119.09/17.11 % (3255913)Termination reason: Instruction limit % 119.09/17.11 % (3255913)Termination phase: Saturation % 119.09/17.11 % (3255913)Time elapsed: 2.043 s % 119.09/17.11 % (3255913)Peak memory usage: 31 MB % 119.09/17.11 % (3255913)Instructions burned: 3774 (million) % 119.09/17.11 % (3255933)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1241816833:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 119.09/17.11 % (3255907)Instruction limit reached! % 120.24/17.22 % (3255907)------------------------------ % 120.24/17.22 % (3255907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.24/17.22 % (3255907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.24/17.22 % (3255907)CaDiCaL version: 2.1.3 % 120.24/17.22 % (3255907)Termination reason: Instruction limit % 120.24/17.22 % (3255907)Termination phase: Saturation % 120.24/17.22 % (3255907)Time elapsed: 3.108 s % 120.24/17.22 % (3255907)Peak memory usage: 34 MB % 120.24/17.22 % (3255907)Instructions burned: 5114 (million) % 120.24/17.22 % (3255935)dis+10_16:1_sil=16000:random_seed=1622017202:i=9155:fsr=off_2961 on theBenchmark for (2961ds/9155Mi) % 120.24/17.22 % (3255923)Instruction limit reached! % 120.24/17.22 % (3255923)------------------------------ % 120.24/17.22 % (3255923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.24/17.22 % (3255923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.24/17.22 % (3255923)CaDiCaL version: 2.1.3 % 120.24/17.22 % (3255923)Termination reason: Instruction limit % 120.24/17.22 % (3255923)Termination phase: Saturation % 120.24/17.22 % (3255923)Time elapsed: 2.757 s % 120.24/17.22 % (3255923)Peak memory usage: 54 MB % 120.24/17.22 % (3255923)Instructions burned: 5212 (million) % 120.24/17.22 % (3255937)ott-3_8_sil=64000:random_seed=630817184:i=20139:bs=on_2946 on theBenchmark for (2946ds/20139Mi) % 120.24/17.22 % (3255931)Instruction limit reached! % 120.24/17.22 % (3255931)------------------------------ % 120.24/17.22 % (3255931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.24/17.22 % (3255931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.24/17.22 % (3255931)CaDiCaL version: 2.1.3 % 120.24/17.22 % (3255931)Termination reason: Instruction limit % 120.24/17.22 % (3255931)Termination phase: Saturation % 120.24/17.22 % (3255931)Time elapsed: 5.164 s % 120.24/17.22 % (3255931)Peak memory usage: 76 MB % 120.24/17.22 % (3255931)Instructions burned: 22565 (million) % 120.24/17.22 % (3255939)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1387067841:fmbsr=2:i=32576_2917 on theBenchmark for (2917ds/32576Mi) % 120.24/17.22 % (3255939)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 120.24/17.22 % (3255939)Terminated due to inappropriate strategy. % 120.24/17.22 % (3255939)------------------------------ % 120.24/17.22 % (3255939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.24/17.22 % (3255939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.24/17.22 % (3255939)CaDiCaL version: 2.1.3 % 120.24/17.22 % (3255939)Termination reason: Inappropriate % 120.24/17.22 % (3255939)Time elapsed: 0.001 s % 120.24/17.22 % (3255939)Peak memory usage: 10 MB % 120.24/17.22 % (3255939)Instructions burned: 2 (million) % 120.24/17.22 % (3255939)------------------------------ % 120.24/17.22 % (3255939)------------------------------ % 120.24/17.22 % (3255941)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2676634066:i=11404_2917 on theBenchmark for (2917ds/11404Mi) % 120.24/17.22 % (3255933)Instruction limit reached! % 120.24/17.22 % (3255933)------------------------------ % 120.24/17.22 % (3255933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.24/17.22 % (3255933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.24/17.22 % (3255933)CaDiCaL version: 2.1.3 % 120.24/17.22 % (3255933)Termination reason: Instruction limit % 120.24/17.22 % (3255933)Termination phase: Saturation % 120.24/17.22 % (3255933)Time elapsed: 5.014 s % 120.24/17.22 % (3255933)Peak memory usage: 59 MB % 120.24/17.22 % (3255933)Instructions burned: 8175 (million) % 120.24/17.22 % (3255943)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3517525855:i=14134_2917 on theBenchmark for (2917ds/14134Mi) % 120.24/17.22 % (3255935)Instruction limit reached! % 120.24/17.22 % (3255935)------------------------------ % 120.24/17.22 % (3255935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.24/17.22 % (3255935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.24/17.22 % (3255935)CaDiCaL version: 2.1.3 % 120.24/17.22 % (3255935)Termination reason: Instruction limit % 120.24/17.22 % (3255935)Termination phase: Saturation % 120.24/17.22 % (3255935)Time elapsed: 4.623 s % 120.24/17.22 % (3255935)Peak memory usage: 52 MB % 120.24/17.22 % (3255935)Instructions burned: 9157 (million) % 120.24/17.22 % (3255945)dis+33_16_sil=32000:sac=on:random_seed=3768437826:i=15851:nm=0_2915 on theBenchmark for (2915ds/15851Mi) % 120.24/17.22 % (3255941)Instruction limit reached! % 120.24/17.22 % (3255941)------------------------------ % 120.24/17.22 % (3255941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.25/18.21 % (3255941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.25/18.21 % (3255941)CaDiCaL version: 2.1.3 % 127.25/18.21 % (3255941)Termination reason: Instruction limit % 127.25/18.21 % (3255941)Termination phase: Saturation % 127.25/18.21 % (3255941)Time elapsed: 3.737 s % 127.25/18.21 % (3255941)Peak memory usage: 60 MB % 127.25/18.21 % (3255941)Instructions burned: 11406 (million) % 127.25/18.21 % (3255947)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3381793306:avsq=on:i=17627:add=on:amm=off_2880 on theBenchmark for (2880ds/17627Mi) % 127.25/18.21 % (3255921)Instruction limit reached! % 127.25/18.21 % (3255921)------------------------------ % 127.25/18.21 % (3255921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.25/18.21 % (3255921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.25/18.21 % (3255921)CaDiCaL version: 2.1.3 % 127.25/18.21 % (3255921)Termination reason: Instruction limit % 127.25/18.21 % (3255921)Termination phase: Saturation % 127.25/18.21 % (3255921)Time elapsed: 12.630 s % 127.25/18.21 % (3255921)Peak memory usage: 103 MB % 127.25/18.21 % (3255921)Instructions burned: 29341 (million) % 127.25/18.21 % (3255949)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2105446825:s2a=on:i=53295_2848 on theBenchmark for (2848ds/53295Mi) % 127.25/18.21 % (3255945)Instruction limit reached! % 127.25/18.21 % (3255945)------------------------------ % 127.25/18.21 % (3255945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.25/18.21 % (3255945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.25/18.21 % (3255945)CaDiCaL version: 2.1.3 % 127.25/18.21 % (3255945)Termination reason: Instruction limit % 127.25/18.21 % (3255945)Termination phase: Saturation % 127.25/18.21 % (3255945)Time elapsed: 7.276 s % 127.25/18.21 % (3255945)Peak memory usage: 138 MB % 127.25/18.21 % (3255945)Instructions burned: 15851 (million) % 127.25/18.21 % (3255951)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=899668468:i=26857:ins=20_2841 on theBenchmark for (2841ds/26857Mi) % 127.25/18.21 % (3255951)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.25/18.21 % (3255951)Terminated due to inappropriate strategy. % 127.25/18.21 % (3255951)------------------------------ % 127.25/18.21 % (3255951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.25/18.21 % (3255951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.25/18.21 % (3255951)CaDiCaL version: 2.1.3 % 127.25/18.21 % (3255951)Termination reason: Inappropriate % 127.25/18.21 % (3255951)Time elapsed: 0.001 s % 127.25/18.21 % (3255951)Peak memory usage: 10 MB % 127.25/18.21 % (3255951)Instructions burned: 2 (million) % 127.25/18.21 % (3255951)------------------------------ % 127.25/18.21 % (3255951)------------------------------ % 127.25/18.21 % (3255953)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2828525151:i=28120:bs=on:fsr=off_2841 on theBenchmark for (2841ds/28120Mi) % 127.25/18.21 % (3255943)Instruction limit reached! % 127.25/18.21 % (3255943)------------------------------ % 127.25/18.21 % (3255943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.25/18.21 % (3255943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.25/18.21 % (3255943)CaDiCaL version: 2.1.3 % 127.25/18.21 % (3255943)Termination reason: Instruction limit % 127.25/18.21 % (3255943)Termination phase: Saturation % 127.25/18.21 % (3255943)Time elapsed: 8.532 s % 127.25/18.21 % (3255943)Peak memory usage: 78 MB % 127.25/18.21 % (3255943)Instructions burned: 14135 (million) % 127.25/18.21 % (3255955)fmb+10_1_sil=256000:fmbss=7:random_seed=2682427596:fmbsr=1.6:i=182295_2831 on theBenchmark for (2831ds/182295Mi) % 127.25/18.21 % (3255955)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.25/18.21 % (3255955)Terminated due to inappropriate strategy. % 127.25/18.21 % (3255955)------------------------------ % 127.25/18.21 % (3255955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.25/18.21 % (3255955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.25/18.21 % (3255955)CaDiCaL version: 2.1.3 % 127.25/18.21 % (3255955)Termination reason: Inappropriate % 127.25/18.21 % (3255955)Time elapsed: 0.001 s % 127.25/18.21 % (3255955)Peak memory usage: 10 MB % 127.25/18.21 % (3255955)Instructions burned: 2 (million) % 127.25/18.21 % (3255955)------------------------------ % 127.25/18.21 % (3255955)------------------------------ % 127.25/18.21 % (3255957)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2668506531:i=44625:gsp=on_2831 on theBenchmark for (2831ds/44625Mi) % 133.27/19.11 % (3255957)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 133.27/19.11 % (3255957)Terminated due to inappropriate strategy. % 133.27/19.11 % (3255957)------------------------------ % 133.27/19.11 % (3255957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.27/19.11 % (3255957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.27/19.11 % (3255957)CaDiCaL version: 2.1.3 % 133.27/19.11 % (3255957)Termination reason: Inappropriate % 133.27/19.11 % (3255957)Time elapsed: 0.001 s % 133.27/19.11 % (3255957)Peak memory usage: 11 MB % 133.27/19.11 % (3255957)Instructions burned: 2 (million) % 133.27/19.11 % (3255957)------------------------------ % 133.27/19.11 % (3255957)------------------------------ % 133.27/19.11 % (3255959)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3079028375:i=160505_2831 on theBenchmark for (2831ds/160505Mi) % 133.27/19.11 % (3255959)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 133.27/19.11 % (3255959)Terminated due to inappropriate strategy. % 133.27/19.11 % (3255959)------------------------------ % 133.27/19.11 % (3255959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.27/19.11 % (3255959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.27/19.11 % (3255959)CaDiCaL version: 2.1.3 % 133.27/19.11 % (3255959)Termination reason: Inappropriate % 133.27/19.11 % (3255959)Time elapsed: 0.001 s % 133.27/19.11 % (3255959)Peak memory usage: 10 MB % 133.27/19.11 % (3255959)Instructions burned: 2 (million) % 133.27/19.11 % (3255959)------------------------------ % 133.27/19.11 % (3255959)------------------------------ % 133.27/19.11 % (3255961)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1712033131:fmbsr=1.3:i=225729_2831 on theBenchmark for (2831ds/225729Mi) % 133.27/19.11 % (3255961)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 133.27/19.11 % (3255961)Terminated due to inappropriate strategy. % 133.27/19.11 % (3255961)------------------------------ % 133.27/19.11 % (3255961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.27/19.11 % (3255961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.27/19.11 % (3255961)CaDiCaL version: 2.1.3 % 133.27/19.11 % (3255961)Termination reason: Inappropriate % 133.27/19.11 % (3255961)Time elapsed: 0.001 s % 133.27/19.11 % (3255961)Peak memory usage: 10 MB % 133.27/19.11 % (3255961)Instructions burned: 2 (million) % 133.27/19.11 % (3255961)------------------------------ % 133.27/19.11 % (3255961)------------------------------ % 133.27/19.11 % (3255963)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2502658457:fmbsr=2:i=185024:ins=7_2830 on theBenchmark for (2830ds/185024Mi) % 133.27/19.11 % (3255963)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 133.27/19.11 % (3255963)Terminated due to inappropriate strategy. % 133.27/19.11 % (3255963)------------------------------ % 133.27/19.11 % (3255963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.27/19.11 % (3255963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.27/19.11 % (3255963)CaDiCaL version: 2.1.3 % 133.27/19.11 % (3255963)Termination reason: Inappropriate % 133.27/19.11 % (3255963)Time elapsed: 0.001 s % 133.27/19.11 % (3255963)Peak memory usage: 10 MB % 133.27/19.11 % (3255963)Instructions burned: 2 (million) % 133.27/19.11 % (3255963)------------------------------ % 133.27/19.11 % (3255963)------------------------------ % 133.27/19.11 % (3255965)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=71529401:rtra=on_2830 on theBenchmark for (2830ds/0Mi) % 133.27/19.11 % (3255965)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 133.27/19.11 % (3255965)Terminated due to inappropriate strategy. % 133.27/19.11 % (3255965)------------------------------ % 133.27/19.11 % (3255965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.27/19.11 % (3255965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.27/19.11 % (3255965)CaDiCaL version: 2.1.3 % 133.27/19.11 % (3255965)Termination reason: Inappropriate % 133.27/19.11 % (3255965)Time elapsed: 0.001 s % 133.27/19.11 % (3255965)Peak memory usage: 10 MB % 133.27/19.11 % (3255965)Instructions burned: 2 (million) % 133.27/19.11 % (3255965)------------------------------ % 133.27/19.11 % (3255965)------------------------------ % 133.27/19.11 % (3255967)% WARNING: option uhcvi not known. % 133.27/19.11 % (3255967)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=305419091:i=271062:add=off:rtra=on:rawr=on_2830 on theBenchmark for (2830ds/271062Mi) % 145.34/20.87 % (3255937)Instruction limit reached! % 145.34/20.87 % (3255937)------------------------------ % 145.34/20.87 % (3255937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.34/20.87 % (3255937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.34/20.87 % (3255937)CaDiCaL version: 2.1.3 % 145.34/20.87 % (3255937)Termination reason: Instruction limit % 145.34/20.87 % (3255937)Termination phase: Saturation % 145.34/20.87 % (3255937)Time elapsed: 11.902 s % 145.34/20.87 % (3255937)Peak memory usage: 82 MB % 145.34/20.87 % (3255937)Instructions burned: 20139 (million) % 145.34/20.87 % (3255969)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2472962548:i=176048:add=on:rtra=on:rawr=on_2826 on theBenchmark for (2826ds/176048Mi) % 145.34/20.87 % (3255947)Instruction limit reached! % 145.34/20.87 % (3255947)------------------------------ % 145.34/20.87 % (3255947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.34/20.87 % (3255947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.34/20.87 % (3255947)CaDiCaL version: 2.1.3 % 145.34/20.87 % (3255947)Termination reason: Instruction limit % 145.34/20.87 % (3255947)Termination phase: Saturation % 145.34/20.87 % (3255947)Time elapsed: 5.571 s % 145.34/20.87 % (3255947)Peak memory usage: 101 MB % 145.34/20.87 % (3255947)Instructions burned: 17629 (million) % 145.34/20.87 % (3255971)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3874519967:i=206:fgj=on:rtra=on_2824 on theBenchmark for (2824ds/206Mi) % 145.34/20.87 % (3255971)Instruction limit reached! % 145.34/20.87 % (3255971)------------------------------ % 145.34/20.87 % (3255971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.34/20.87 % (3255971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.34/20.87 % (3255971)CaDiCaL version: 2.1.3 % 145.34/20.87 % (3255971)Termination reason: Instruction limit % 145.34/20.87 % (3255971)Termination phase: Saturation % 145.34/20.87 % (3255971)Time elapsed: 0.067 s % 145.34/20.87 % (3255971)Peak memory usage: 13 MB % 145.34/20.87 % (3255971)Instructions burned: 208 (million) % 145.34/20.87 % (3255973)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2653543087:i=232:rtra=on_2823 on theBenchmark for (2823ds/232Mi) % 145.34/20.87 % (3255973)Instruction limit reached! % 145.34/20.87 % (3255973)------------------------------ % 145.34/20.87 % (3255973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.34/20.87 % (3255973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.34/20.87 % (3255973)CaDiCaL version: 2.1.3 % 145.34/20.87 % (3255973)Termination reason: Instruction limit % 145.34/20.87 % (3255973)Termination phase: Saturation % 145.34/20.87 % (3255973)Time elapsed: 0.077 s % 145.34/20.87 % (3255973)Peak memory usage: 13 MB % 145.34/20.87 % (3255973)Instructions burned: 235 (million) % 145.34/20.87 % (3255975)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3768150467:i=262:rtra=on_2822 on theBenchmark for (2822ds/262Mi) % 145.34/20.87 % (3255975)Instruction limit reached! % 145.34/20.87 % (3255975)------------------------------ % 145.34/20.87 % (3255975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.34/20.87 % (3255975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.34/20.87 % (3255975)CaDiCaL version: 2.1.3 % 145.34/20.87 % (3255975)Termination reason: Instruction limit % 145.34/20.87 % (3255975)Termination phase: Saturation % 145.34/20.87 % (3255975)Time elapsed: 0.081 s % 145.34/20.87 % (3255975)Peak memory usage: 14 MB % 145.34/20.87 % (3255975)Instructions burned: 263 (million) % 145.34/20.87 % (3255977)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=4173783385:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2821 on theBenchmark for (2821ds/318Mi) % 145.34/20.87 % (3255977)Instruction limit reached! % 145.34/20.87 % (3255977)------------------------------ % 145.34/20.87 % (3255977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.34/20.87 % (3255977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.34/20.87 % (3255977)CaDiCaL version: 2.1.3 % 145.34/20.87 % (3255977)Termination reason: Instruction limit % 145.34/20.87 % (3255977)Termination phase: Saturation % 145.34/20.87 % (3255977)Time elapsed: 0.113 s % 145.34/20.87 % (3255977)Peak memory usage: 15 MB % 145.34/20.87 % (3255977)Instructions burned: 320 (million) % 145.34/20.87 % (3255979)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2565153813:i=1428:nm=2:rtra=on_2820 on theBenchmark for (2820ds/1428Mi) % 174.06/24.95 % (3255979)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 174.06/24.95 % (3255979)Terminated due to inappropriate strategy. % 174.06/24.95 % (3255979)------------------------------ % 174.06/24.95 % (3255979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.06/24.95 % (3255979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.06/24.95 % (3255979)CaDiCaL version: 2.1.3 % 174.06/24.95 % (3255979)Termination reason: Inappropriate % 174.06/24.95 % (3255979)Time elapsed: 0.001 s % 174.06/24.95 % (3255979)Peak memory usage: 11 MB % 174.06/24.95 % (3255979)Instructions burned: 2 (million) % 174.06/24.95 % (3255979)------------------------------ % 174.06/24.95 % (3255979)------------------------------ % 174.06/24.95 % (3255981)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3459275387:i=262:bd=preordered:rtra=on:fsd=on_2820 on theBenchmark for (2820ds/262Mi) % 174.06/24.95 % (3255981)Instruction limit reached! % 174.06/24.95 % (3255981)------------------------------ % 174.06/24.95 % (3255981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.06/24.95 % (3255981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.06/24.95 % (3255981)CaDiCaL version: 2.1.3 % 174.06/24.95 % (3255981)Termination reason: Instruction limit % 174.06/24.95 % (3255981)Termination phase: Saturation % 174.06/24.95 % (3255981)Time elapsed: 0.121 s % 174.06/24.95 % (3255981)Peak memory usage: 13 MB % 174.06/24.95 % (3255981)Instructions burned: 265 (million) % 174.06/24.95 % (3255983)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=1978559097:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2819 on theBenchmark for (2819ds/1368Mi) % 174.06/24.95 % (3255983)Instruction limit reached! % 174.06/24.95 % (3255983)------------------------------ % 174.06/24.95 % (3255983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.06/24.95 % (3255983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.06/24.95 % (3255983)CaDiCaL version: 2.1.3 % 174.06/24.95 % (3255983)Termination reason: Instruction limit % 174.06/24.95 % (3255983)Termination phase: Saturation % 174.06/24.95 % (3255983)Time elapsed: 0.387 s % 174.06/24.95 % (3255983)Peak memory usage: 20 MB % 174.06/24.95 % (3255983)Instructions burned: 1370 (million) % 174.06/24.95 % (3255985)ott-21_1_sil=16000:si=on:fs=off:random_seed=244205461:i=360:av=off:fsr=off:rtra=on_2815 on theBenchmark for (2815ds/360Mi) % 174.06/24.95 % (3255985)Instruction limit reached! % 174.06/24.95 % (3255985)------------------------------ % 174.06/24.95 % (3255985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.06/24.95 % (3255985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.06/24.95 % (3255985)CaDiCaL version: 2.1.3 % 174.06/24.95 % (3255985)Termination reason: Instruction limit % 174.06/24.95 % (3255985)Termination phase: Saturation % 174.06/24.95 % (3255985)Time elapsed: 0.087 s % 174.06/24.95 % (3255985)Peak memory usage: 13 MB % 174.06/24.95 % (3255985)Instructions burned: 362 (million) % 174.06/24.95 % (3255987)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2893360511:i=954:bd=all:rtra=on_2814 on theBenchmark for (2814ds/954Mi) % 174.06/24.95 % (3255987)Instruction limit reached! % 174.06/24.95 % (3255987)------------------------------ % 174.06/24.95 % (3255987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.06/24.95 % (3255987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.06/24.95 % (3255987)CaDiCaL version: 2.1.3 % 174.06/24.95 % (3255987)Termination reason: Instruction limit % 174.06/24.95 % (3255987)Termination phase: Saturation % 174.06/24.95 % (3255987)Time elapsed: 0.244 s % 174.06/24.95 % (3255987)Peak memory usage: 13 MB % 174.06/24.95 % (3255987)Instructions burned: 956 (million) % 174.06/24.95 % (3255989)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3564197445:fmbsr=1.3:i=1730:ins=25:rtra=on_2811 on theBenchmark for (2811ds/1730Mi) % 174.06/24.95 % (3255989)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 174.06/24.95 % (3255989)Terminated due to inappropriate strategy. % 174.06/24.95 % (3255989)------------------------------ % 174.06/24.95 % (3255989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.06/24.95 % (3255989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.06/24.95 % (3255989)CaDiCaL version: 2.1.3 % 174.06/24.95 % (3255989)Termination reason: Inappropriate % 174.06/24.95 % (3255989)Time elapsed: 0.001 s % 221.08/31.40 % (3255989)Peak memory usage: 10 MB % 221.08/31.40 % (3255989)Instructions burned: 2 (million) % 221.08/31.40 % (3255989)------------------------------ % 221.08/31.40 % (3255989)------------------------------ % 221.08/31.40 % (3255991)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=382125172:i=2358:rtra=on_2811 on theBenchmark for (2811ds/2358Mi) % 221.08/31.40 % (3255991)Instruction limit reached! % 221.08/31.40 % (3255991)------------------------------ % 221.08/31.40 % (3255991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.08/31.40 % (3255991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.08/31.40 % (3255991)CaDiCaL version: 2.1.3 % 221.08/31.40 % (3255991)Termination reason: Instruction limit % 221.08/31.40 % (3255991)Termination phase: Saturation % 221.08/31.40 % (3255991)Time elapsed: 0.697 s % 221.08/31.40 % (3255991)Peak memory usage: 24 MB % 221.08/31.40 % (3255991)Instructions burned: 2363 (million) % 221.08/31.40 % (3255993)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1567159678:i=1778:ins=1:rtra=on_2804 on theBenchmark for (2804ds/1778Mi) % 221.08/31.40 % (3255993)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 221.08/31.40 % (3255993)Terminated due to inappropriate strategy. % 221.08/31.40 % (3255993)------------------------------ % 221.08/31.40 % (3255993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.08/31.40 % (3255993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.08/31.40 % (3255993)CaDiCaL version: 2.1.3 % 221.08/31.40 % (3255993)Termination reason: Inappropriate % 221.08/31.40 % (3255993)Time elapsed: 0.001 s % 221.08/31.40 % (3255993)Peak memory usage: 10 MB % 221.08/31.40 % (3255993)Instructions burned: 2 (million) % 221.08/31.40 % (3255993)------------------------------ % 221.08/31.40 % (3255993)------------------------------ % 221.08/31.40 % (3255995)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=2536037058:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2804 on theBenchmark for (2804ds/1384Mi) % 221.08/31.40 % (3255995)Instruction limit reached! % 221.08/31.40 % (3255995)------------------------------ % 221.08/31.40 % (3255995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.08/31.40 % (3255995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.08/31.40 % (3255995)CaDiCaL version: 2.1.3 % 221.08/31.40 % (3255995)Termination reason: Instruction limit % 221.08/31.40 % (3255995)Termination phase: Saturation % 221.08/31.40 % (3255995)Time elapsed: 0.453 s % 221.08/31.40 % (3255995)Peak memory usage: 23 MB % 221.08/31.40 % (3255995)Instructions burned: 1385 (million) % 221.08/31.40 % (3255997)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3223987138:i=1758:kws=inv_precedence:fsr=off:rtra=on_2799 on theBenchmark for (2799ds/1758Mi) % 221.08/31.40 % (3255997)Instruction limit reached! % 221.08/31.40 % (3255997)------------------------------ % 221.08/31.40 % (3255997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.08/31.40 % (3255997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.08/31.40 % (3255997)CaDiCaL version: 2.1.3 % 221.08/31.40 % (3255997)Termination reason: Instruction limit % 221.08/31.40 % (3255997)Termination phase: Saturation % 221.08/31.40 % (3255997)Time elapsed: 0.530 s % 221.08/31.40 % (3255997)Peak memory usage: 28 MB % 221.08/31.40 % (3255997)Instructions burned: 1759 (million) % 221.08/31.40 % (3255999)fmb+10_1_sil=64000:si=on:random_seed=158906584:i=44122:nm=2:rtra=on:gsp=on_2794 on theBenchmark for (2794ds/44122Mi) % 221.08/31.40 % (3255999)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 221.08/31.40 % (3255999)Terminated due to inappropriate strategy. % 221.08/31.40 % (3255999)------------------------------ % 221.08/31.40 % (3255999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.08/31.40 % (3255999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.08/31.40 % (3255999)CaDiCaL version: 2.1.3 % 221.08/31.40 % (3255999)Termination reason: Inappropriate % 221.08/31.40 % (3255999)Time elapsed: 0.001 s % 221.08/31.40 % (3255999)Peak memory usage: 10 MB % 221.08/31.40 % (3255999)Instructions burned: 2 (million) % 221.08/31.40 % (3255999)------------------------------ % 221.08/31.40 % (3255999)------------------------------ % 221.08/31.40 % (3256001)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=618025333:i=19030:nm=5:rtra=on_2793 on theBenchmark for (2793ds/19030Mi) % 249.21/35.47 % (3256001)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.21/35.47 % (3256001)Terminated due to inappropriate strategy. % 249.21/35.47 % (3256001)------------------------------ % 249.21/35.47 % (3256001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.21/35.47 % (3256001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.21/35.47 % (3256001)CaDiCaL version: 2.1.3 % 249.21/35.47 % (3256001)Termination reason: Inappropriate % 249.21/35.47 % (3256001)Time elapsed: 0.001 s % 249.21/35.47 % (3256001)Peak memory usage: 10 MB % 249.21/35.47 % (3256001)Instructions burned: 2 (million) % 249.21/35.47 % (3256001)------------------------------ % 249.21/35.47 % (3256001)------------------------------ % 249.21/35.47 % (3256003)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2092363800:fmbsr=1.7:i=1840:rtra=on_2793 on theBenchmark for (2793ds/1840Mi) % 249.21/35.47 % (3256003)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.21/35.47 % (3256003)Terminated due to inappropriate strategy. % 249.21/35.47 % (3256003)------------------------------ % 249.21/35.47 % (3256003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.21/35.47 % (3256003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.21/35.47 % (3256003)CaDiCaL version: 2.1.3 % 249.21/35.47 % (3256003)Termination reason: Inappropriate % 249.21/35.47 % (3256003)Time elapsed: 0.001 s % 249.21/35.47 % (3256003)Peak memory usage: 10 MB % 249.21/35.47 % (3256003)Instructions burned: 2 (million) % 249.21/35.47 % (3256003)------------------------------ % 249.21/35.47 % (3256003)------------------------------ % 249.21/35.47 % (3256005)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2783565825:i=10262:rtra=on_2793 on theBenchmark for (2793ds/10262Mi) % 249.21/35.47 % (3256005)Instruction limit reached! % 249.21/35.47 % (3256005)------------------------------ % 249.21/35.47 % (3256005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.21/35.47 % (3256005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.21/35.47 % (3256005)CaDiCaL version: 2.1.3 % 249.21/35.47 % (3256005)Termination reason: Instruction limit % 249.21/35.47 % (3256005)Termination phase: Saturation % 249.21/35.47 % (3256005)Time elapsed: 3.149 s % 249.21/35.47 % (3256005)Peak memory usage: 68 MB % 249.21/35.47 % (3256005)Instructions burned: 10263 (million) % 249.21/35.47 % (3256007)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2821175462:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2762 on theBenchmark for (2762ds/2944Mi) % 249.21/35.47 % (3256007)Instruction limit reached! % 249.21/35.47 % (3256007)------------------------------ % 249.21/35.47 % (3256007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.21/35.47 % (3256007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.21/35.47 % (3256007)CaDiCaL version: 2.1.3 % 249.21/35.47 % (3256007)Termination reason: Instruction limit % 249.21/35.47 % (3256007)Termination phase: Saturation % 249.21/35.47 % (3256007)Time elapsed: 0.867 s % 249.21/35.47 % (3256007)Peak memory usage: 56 MB % 249.21/35.47 % (3256007)Instructions burned: 2946 (million) % 249.21/35.47 % (3256009)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1285714361:i=12648:rtra=on_2753 on theBenchmark for (2753ds/12648Mi) % 249.21/35.47 % (3256009)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.21/35.47 % (3256009)Terminated due to inappropriate strategy. % 249.21/35.47 % (3256009)------------------------------ % 249.21/35.47 % (3256009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.21/35.47 % (3256009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.21/35.47 % (3256009)CaDiCaL version: 2.1.3 % 249.21/35.47 % (3256009)Termination reason: Inappropriate % 249.21/35.47 % (3256009)Time elapsed: 0.001 s % 249.21/35.47 % (3256009)Peak memory usage: 10 MB % 249.21/35.47 % (3256009)Instructions burned: 2 (million) % 249.21/35.47 % (3256009)------------------------------ % 249.21/35.47 % (3256009)------------------------------ % 249.21/35.47 % (3256011)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2707188948:fmbsr=2.30978:i=4348:rtra=on_2753 on theBenchmark for (2753ds/4348Mi) % 249.21/35.47 % (3256011)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.21/35.47 % (3256011)Terminated due to inappropriate strategy. % 249.21/35.47 % (3256011)------------------------------ % 249.21/35.47 % (3256011)Version: VampTerminated % 300.58/42.63 % Vampire exiting %------------------------------------------------------------------------------