%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW837_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n003.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:45:03 PM UTC 2026 % Result : Timeout 300.36s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW837_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.18 % Computer : n003.cluster.edu % 0.10/0.18 % Model : x86_64 x86_64 % 0.10/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.18 % Memory : 8046.5625MB % 0.10/0.18 % OS : Linux 6.8.0-71-generic % 0.10/0.18 % CPULimit : 300 % 0.10/0.18 % WCLimit : 300 % 0.10/0.18 % DateTime : Mon Sep 28 14:32:57 UTC 2026 % 0.10/0.19 % CPUTime : % 0.10/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.21 Running first-order model finding % 0.10/0.21 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 % 4.40/0.99 % (1635785)Will run a generic schedule for satisfiability detection. % 4.40/0.99 % (1635793)dis+10_1_sil=32000:sp=arity:random_seed=463375071:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 4.40/0.99 % (1635791)% WARNING: option uhcvi not known. % 4.40/0.99 % (1635790)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3602322294_2999 on theBenchmark for (2999ds/0Mi) % 4.40/0.99 % (1635791)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3937592310:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 4.40/0.99 % (1635792)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2649072275:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 4.40/0.99 % (1635794)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=8576251:i=116_2999 on theBenchmark for (2999ds/116Mi) % 4.40/0.99 % (1635790)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.40/0.99 % (1635790)Terminated due to inappropriate strategy. % 4.40/0.99 % (1635790)------------------------------ % 4.40/0.99 % (1635790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.40/0.99 % (1635796)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3245915297:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 4.40/0.99 % (1635790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.40/0.99 % (1635790)CaDiCaL version: 2.1.3 % 4.40/0.99 % (1635790)Termination reason: Inappropriate % 4.40/0.99 % (1635790)Time elapsed: 0.004 s % 4.40/0.99 % (1635790)Peak memory usage: 11 MB % 4.40/0.99 % (1635790)Instructions burned: 6 (million) % 4.40/0.99 % (1635790)------------------------------ % 4.40/0.99 % (1635790)------------------------------ % 4.40/0.99 % (1635795)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=619786167:i=131_2999 on theBenchmark for (2999ds/131Mi) % 4.40/0.99 % (1635803)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2790385071:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 4.40/0.99 % (1635793)Instruction limit reached! % 4.40/0.99 % (1635793)------------------------------ % 4.40/0.99 % (1635793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.40/0.99 % (1635793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.40/0.99 % (1635793)CaDiCaL version: 2.1.3 % 4.40/0.99 % (1635793)Termination reason: Instruction limit % 4.40/0.99 % (1635793)Termination phase: Saturation % 4.40/0.99 % (1635793)Time elapsed: 0.036 s % 4.40/0.99 % (1635793)Peak memory usage: 13 MB % 4.40/0.99 % (1635793)Instructions burned: 104 (million) % 4.40/0.99 % (1635803)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.40/0.99 % (1635803)Terminated due to inappropriate strategy. % 4.40/0.99 % (1635803)------------------------------ % 4.40/0.99 % (1635803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.40/0.99 % (1635803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.40/0.99 % (1635803)CaDiCaL version: 2.1.3 % 4.40/0.99 % (1635803)Termination reason: Inappropriate % 4.40/0.99 % (1635803)Time elapsed: 0.003 s % 4.40/0.99 % (1635803)Peak memory usage: 11 MB % 4.40/0.99 % (1635803)Instructions burned: 6 (million) % 4.40/0.99 % (1635803)------------------------------ % 4.40/0.99 % (1635803)------------------------------ % 4.40/0.99 % (1635806)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3494315336:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 4.40/0.99 % (1635807)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=1368042239:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 4.40/0.99 % (1635794)Instruction limit reached! % 4.40/0.99 % (1635794)------------------------------ % 4.40/0.99 % (1635794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.40/0.99 % (1635794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.40/0.99 % (1635794)CaDiCaL version: 2.1.3 % 4.40/0.99 % (1635794)Termination reason: Instruction limit % 4.40/0.99 % (1635794)Termination phase: Saturation % 4.40/0.99 % (1635794)Time elapsed: 0.073 s % 4.40/0.99 % (1635794)Peak memory usage: 13 MB % 4.40/0.99 % (1635794)Instructions burned: 117 (million) % 4.40/0.99 % (1635806)Instruction limit reached! % 4.40/0.99 % (1635806)------------------------------ % 4.40/0.99 % (1635806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.66/1.29 % (1635806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.66/1.29 % (1635806)CaDiCaL version: 2.1.3 % 6.66/1.29 % (1635806)Termination reason: Instruction limit % 6.66/1.29 % (1635806)Termination phase: Saturation % 6.66/1.29 % (1635806)Time elapsed: 0.050 s % 6.66/1.29 % (1635806)Peak memory usage: 13 MB % 6.66/1.29 % (1635806)Instructions burned: 133 (million) % 6.66/1.29 % (1635810)ott-21_1_sil=16000:fs=off:random_seed=1084997718:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.66/1.29 % (1635811)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2566574541:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.66/1.29 % (1635796)Instruction limit reached! % 6.66/1.29 % (1635796)------------------------------ % 6.66/1.29 % (1635796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.66/1.29 % (1635796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.66/1.29 % (1635796)CaDiCaL version: 2.1.3 % 6.66/1.29 % (1635796)Termination reason: Instruction limit % 6.66/1.29 % (1635796)Termination phase: Saturation % 6.66/1.29 % (1635796)Time elapsed: 0.109 s % 6.66/1.29 % (1635796)Peak memory usage: 14 MB % 6.66/1.29 % (1635796)Instructions burned: 159 (million) % 6.66/1.29 % (1635814)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3834467105:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.66/1.29 % (1635814)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.66/1.29 % (1635814)Terminated due to inappropriate strategy. % 6.66/1.29 % (1635814)------------------------------ % 6.66/1.29 % (1635814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.66/1.29 % (1635814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.66/1.29 % (1635814)CaDiCaL version: 2.1.3 % 6.66/1.29 % (1635814)Termination reason: Inappropriate % 6.66/1.29 % (1635814)Time elapsed: 0.003 s % 6.66/1.29 % (1635814)Peak memory usage: 10 MB % 6.66/1.29 % (1635814)Instructions burned: 6 (million) % 6.66/1.29 % (1635814)------------------------------ % 6.66/1.29 % (1635814)------------------------------ % 6.66/1.29 % (1635795)Instruction limit reached! % 6.66/1.29 % (1635795)------------------------------ % 6.66/1.29 % (1635795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.66/1.29 % (1635795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.66/1.29 % (1635795)CaDiCaL version: 2.1.3 % 6.66/1.29 % (1635795)Termination reason: Instruction limit % 6.66/1.29 % (1635795)Termination phase: Saturation % 6.66/1.29 % (1635795)Time elapsed: 0.123 s % 6.66/1.29 % (1635795)Peak memory usage: 13 MB % 6.66/1.29 % (1635795)Instructions burned: 131 (million) % 6.66/1.29 % (1635816)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1397606565:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.66/1.29 % (1635817)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=990217475:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.66/1.29 % (1635817)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.66/1.29 % (1635817)Terminated due to inappropriate strategy. % 6.66/1.29 % (1635817)------------------------------ % 6.66/1.29 % (1635817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.66/1.29 % (1635817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.66/1.29 % (1635817)CaDiCaL version: 2.1.3 % 6.66/1.29 % (1635817)Termination reason: Inappropriate % 6.66/1.29 % (1635817)Time elapsed: 0.003 s % 6.66/1.29 % (1635817)Peak memory usage: 11 MB % 6.66/1.29 % (1635817)Instructions burned: 6 (million) % 6.66/1.29 % (1635817)------------------------------ % 6.66/1.29 % (1635817)------------------------------ % 6.66/1.29 % (1635821)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=1009235168:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 6.66/1.29 % (1635810)Instruction limit reached! % 6.66/1.29 % (1635810)------------------------------ % 6.66/1.29 % (1635810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.66/1.29 % (1635810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.66/1.29 % (1635810)CaDiCaL version: 2.1.3 % 6.66/1.29 % (1635810)Termination reason: Instruction limit % 6.66/1.29 % (1635810)Termination phase: Saturation % 28.81/4.32 % (1635810)Time elapsed: 0.104 s % 28.81/4.32 % (1635810)Peak memory usage: 13 MB % 28.81/4.32 % (1635810)Instructions burned: 180 (million) % 28.81/4.32 % (1635830)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=741440925:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 28.81/4.32 % (1635811)Instruction limit reached! % 28.81/4.32 % (1635811)------------------------------ % 28.81/4.32 % (1635811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.81/4.32 % (1635811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.81/4.32 % (1635811)CaDiCaL version: 2.1.3 % 28.81/4.32 % (1635811)Termination reason: Instruction limit % 28.81/4.32 % (1635811)Termination phase: Saturation % 28.81/4.32 % (1635811)Time elapsed: 0.203 s % 28.81/4.32 % (1635811)Peak memory usage: 14 MB % 28.81/4.32 % (1635811)Instructions burned: 478 (million) % 28.81/4.32 % (1635832)fmb+10_1_sil=64000:random_seed=4508093:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 28.81/4.32 % (1635832)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.81/4.32 % (1635832)Terminated due to inappropriate strategy. % 28.81/4.32 % (1635832)------------------------------ % 28.81/4.32 % (1635832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.81/4.32 % (1635832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.81/4.32 % (1635832)CaDiCaL version: 2.1.3 % 28.81/4.32 % (1635832)Termination reason: Inappropriate % 28.81/4.32 % (1635832)Time elapsed: 0.003 s % 28.81/4.32 % (1635832)Peak memory usage: 11 MB % 28.81/4.32 % (1635832)Instructions burned: 6 (million) % 28.81/4.32 % (1635832)------------------------------ % 28.81/4.32 % (1635832)------------------------------ % 28.81/4.32 % (1635834)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3742918302:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 28.81/4.32 % (1635834)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.81/4.32 % (1635834)Terminated due to inappropriate strategy. % 28.81/4.32 % (1635834)------------------------------ % 28.81/4.32 % (1635834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.81/4.32 % (1635834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.81/4.32 % (1635834)CaDiCaL version: 2.1.3 % 28.81/4.32 % (1635834)Termination reason: Inappropriate % 28.81/4.32 % (1635834)Time elapsed: 0.003 s % 28.81/4.32 % (1635834)Peak memory usage: 11 MB % 28.81/4.32 % (1635834)Instructions burned: 6 (million) % 28.81/4.32 % (1635834)------------------------------ % 28.81/4.32 % (1635834)------------------------------ % 28.81/4.32 % (1635836)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2337731208:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 28.81/4.32 % (1635836)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.81/4.32 % (1635836)Terminated due to inappropriate strategy. % 28.81/4.32 % (1635836)------------------------------ % 28.81/4.32 % (1635836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.81/4.32 % (1635836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.81/4.32 % (1635836)CaDiCaL version: 2.1.3 % 28.81/4.32 % (1635836)Termination reason: Inappropriate % 28.81/4.32 % (1635836)Time elapsed: 0.002 s % 28.81/4.32 % (1635836)Peak memory usage: 11 MB % 28.81/4.32 % (1635836)Instructions burned: 6 (million) % 28.81/4.32 % (1635836)------------------------------ % 28.81/4.32 % (1635836)------------------------------ % 28.81/4.32 % (1635842)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2763263648:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 28.81/4.32 % (1635807)Instruction limit reached! % 28.81/4.32 % (1635807)------------------------------ % 28.81/4.32 % (1635807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.81/4.32 % (1635807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.81/4.32 % (1635807)CaDiCaL version: 2.1.3 % 28.81/4.32 % (1635807)Termination reason: Instruction limit % 28.81/4.32 % (1635807)Termination phase: Saturation % 28.81/4.32 % (1635807)Time elapsed: 0.544 s % 28.81/4.32 % (1635807)Peak memory usage: 17 MB % 28.81/4.32 % (1635807)Instructions burned: 684 (million) % 28.81/4.32 % (1635852)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1322628703:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi) % 28.81/4.32 % (1635821)Instruction limit reached! % 28.81/4.32 % (1635821)------------------------------ % 36.17/5.49 % (1635821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.17/5.49 % (1635821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.17/5.49 % (1635821)CaDiCaL version: 2.1.3 % 36.17/5.49 % (1635821)Termination reason: Instruction limit % 36.17/5.49 % (1635821)Termination phase: Saturation % 36.17/5.49 % (1635821)Time elapsed: 0.531 s % 36.17/5.49 % (1635821)Peak memory usage: 19 MB % 36.17/5.49 % (1635821)Instructions burned: 694 (million) % 36.17/5.49 % (1635864)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=895671665:i=6324_2992 on theBenchmark for (2992ds/6324Mi) % 36.17/5.49 % (1635864)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.17/5.49 % (1635864)Terminated due to inappropriate strategy. % 36.17/5.49 % (1635864)------------------------------ % 36.17/5.49 % (1635864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.17/5.49 % (1635864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.17/5.49 % (1635864)CaDiCaL version: 2.1.3 % 36.17/5.49 % (1635864)Termination reason: Inappropriate % 36.17/5.49 % (1635864)Time elapsed: 0.006 s % 36.17/5.49 % (1635864)Peak memory usage: 11 MB % 36.17/5.49 % (1635864)Instructions burned: 6 (million) % 36.17/5.49 % (1635864)------------------------------ % 36.17/5.49 % (1635864)------------------------------ % 36.17/5.49 % (1635868)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2943020327:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi) % 36.17/5.49 % (1635868)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.17/5.49 % (1635868)Terminated due to inappropriate strategy. % 36.17/5.49 % (1635868)------------------------------ % 36.17/5.49 % (1635868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.17/5.49 % (1635868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.17/5.49 % (1635868)CaDiCaL version: 2.1.3 % 36.17/5.49 % (1635868)Termination reason: Inappropriate % 36.17/5.49 % (1635868)Time elapsed: 0.004 s % 36.17/5.49 % (1635868)Peak memory usage: 11 MB % 36.17/5.49 % (1635868)Instructions burned: 6 (million) % 36.17/5.49 % (1635868)------------------------------ % 36.17/5.49 % (1635868)------------------------------ % 36.17/5.49 % (1635870)ott-2_1_sil=16000:newcnf=on:random_seed=2351207653:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2991 on theBenchmark for (2991ds/869Mi) % 36.17/5.49 % (1635816)Instruction limit reached! % 36.17/5.49 % (1635816)------------------------------ % 36.17/5.49 % (1635816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.17/5.49 % (1635816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.17/5.49 % (1635816)CaDiCaL version: 2.1.3 % 36.17/5.49 % (1635816)Termination reason: Instruction limit % 36.17/5.49 % (1635816)Termination phase: Saturation % 36.17/5.49 % (1635816)Time elapsed: 0.787 s % 36.17/5.49 % (1635816)Peak memory usage: 14 MB % 36.17/5.49 % (1635816)Instructions burned: 1180 (million) % 36.17/5.49 % (1635880)ott+10_1_sil=32000:tgt=ground:random_seed=1115440276:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi) % 36.17/5.49 % (1635830)Instruction limit reached! % 36.17/5.49 % (1635830)------------------------------ % 36.17/5.49 % (1635830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.17/5.49 % (1635830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.17/5.49 % (1635830)CaDiCaL version: 2.1.3 % 36.17/5.49 % (1635830)Termination reason: Instruction limit % 36.17/5.49 % (1635830)Termination phase: Saturation % 36.17/5.49 % (1635830)Time elapsed: 0.743 s % 36.17/5.49 % (1635830)Peak memory usage: 19 MB % 36.17/5.49 % (1635830)Instructions burned: 880 (million) % 36.17/5.49 % (1635883)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2780953329:i=54282_2989 on theBenchmark for (2989ds/54282Mi) % 36.17/5.49 % (1635883)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.17/5.49 % (1635883)Terminated due to inappropriate strategy. % 36.17/5.49 % (1635883)------------------------------ % 36.17/5.49 % (1635883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.17/5.49 % (1635883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.17/5.49 % (1635883)CaDiCaL version: 2.1.3 % 36.17/5.49 % (1635883)Termination reason: Inappropriate % 36.17/5.49 % (1635883)Time elapsed: 0.006 s % 36.17/5.49 % (1635883)Peak memory usage: 11 MB % 36.17/5.49 % (1635883)Instructions burned: 6 (million) % 99.80/14.36 % (1635883)------------------------------ % 99.80/14.36 % (1635883)------------------------------ % 99.80/14.36 % (1635888)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=845011027:i=3512:aac=none_2989 on theBenchmark for (2989ds/3512Mi) % 99.80/14.36 % (1635852)Instruction limit reached! % 99.80/14.36 % (1635852)------------------------------ % 99.80/14.36 % (1635852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.80/14.36 % (1635852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.80/14.36 % (1635852)CaDiCaL version: 2.1.3 % 99.80/14.36 % (1635852)Termination reason: Instruction limit % 99.80/14.36 % (1635852)Termination phase: Saturation % 99.80/14.36 % (1635852)Time elapsed: 0.686 s % 99.80/14.36 % (1635852)Peak memory usage: 31 MB % 99.80/14.36 % (1635852)Instructions burned: 1472 (million) % 99.80/14.36 % (1635903)dis+21_1_sil=32000:sas=cadical:random_seed=3262783540:i=3773:amm=off_2986 on theBenchmark for (2986ds/3773Mi) % 99.80/14.36 % (1635870)Instruction limit reached! % 99.80/14.36 % (1635870)------------------------------ % 99.80/14.36 % (1635870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.80/14.36 % (1635870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.80/14.36 % (1635870)CaDiCaL version: 2.1.3 % 99.80/14.36 % (1635870)Termination reason: Instruction limit % 99.80/14.36 % (1635870)Termination phase: Saturation % 99.80/14.36 % (1635870)Time elapsed: 0.723 s % 99.80/14.36 % (1635870)Peak memory usage: 16 MB % 99.80/14.36 % (1635870)Instructions burned: 869 (million) % 99.80/14.36 % (1635917)ott+11_1_sil=16000:gs=on:random_seed=2693009018:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2984 on theBenchmark for (2984ds/2251Mi) % 99.80/14.36 % (1635903)Instruction limit reached! % 99.80/14.36 % (1635903)------------------------------ % 99.80/14.36 % (1635903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.80/14.36 % (1635903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.80/14.36 % (1635903)CaDiCaL version: 2.1.3 % 99.80/14.36 % (1635903)Termination reason: Instruction limit % 99.80/14.36 % (1635903)Termination phase: Saturation % 99.80/14.36 % (1635903)Time elapsed: 1.619 s % 99.80/14.36 % (1635903)Peak memory usage: 38 MB % 99.80/14.36 % (1635903)Instructions burned: 3774 (million) % 99.80/14.36 % (1635958)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3934890076:fmbsr=1.6:i=67534_2969 on theBenchmark for (2969ds/67534Mi) % 99.80/14.36 % (1635958)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 99.80/14.36 % (1635958)Terminated due to inappropriate strategy. % 99.80/14.36 % (1635958)------------------------------ % 99.80/14.36 % (1635958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.80/14.36 % (1635958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.80/14.36 % (1635958)CaDiCaL version: 2.1.3 % 99.80/14.36 % (1635958)Termination reason: Inappropriate % 99.80/14.36 % (1635958)Time elapsed: 0.005 s % 99.80/14.36 % (1635958)Peak memory usage: 11 MB % 99.80/14.36 % (1635958)Instructions burned: 6 (million) % 99.80/14.36 % (1635958)------------------------------ % 99.80/14.36 % (1635958)------------------------------ % 99.80/14.36 % (1635961)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1182938105:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2969 on theBenchmark for (2969ds/4591Mi) % 99.80/14.36 % (1635917)Instruction limit reached! % 99.80/14.36 % (1635917)------------------------------ % 99.80/14.36 % (1635917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.80/14.36 % (1635917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.80/14.36 % (1635917)CaDiCaL version: 2.1.3 % 99.80/14.36 % (1635917)Termination reason: Instruction limit % 99.80/14.36 % (1635917)Termination phase: Saturation % 99.80/14.36 % (1635917)Time elapsed: 2.052 s % 99.80/14.36 % (1635917)Peak memory usage: 28 MB % 99.80/14.36 % (1635917)Instructions burned: 2251 (million) % 99.80/14.36 % (1635976)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2562724285:i=29340_2963 on theBenchmark for (2963ds/29340Mi) % 99.80/14.36 % (1635888)Instruction limit reached! % 99.80/14.36 % (1635888)------------------------------ % 99.80/14.36 % (1635888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.80/14.36 % (1635888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.80/14.36 % (1635888)CaDiCaL version: 2.1.3 % 99.80/14.36 % (1635888)Termination reason: Instruction limit % 148.94/21.26 % (1635888)Termination phase: Saturation % 148.94/21.26 % (1635888)Time elapsed: 2.989 s % 148.94/21.26 % (1635888)Peak memory usage: 32 MB % 148.94/21.26 % (1635888)Instructions burned: 3512 (million) % 148.94/21.26 % (1635989)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3236530378:i=5211_2958 on theBenchmark for (2958ds/5211Mi) % 148.94/21.26 % (1635842)Instruction limit reached! % 148.94/21.26 % (1635842)------------------------------ % 148.94/21.26 % (1635842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.94/21.26 % (1635842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.94/21.26 % (1635842)CaDiCaL version: 2.1.3 % 148.94/21.26 % (1635842)Termination reason: Instruction limit % 148.94/21.26 % (1635842)Termination phase: Saturation % 148.94/21.26 % (1635842)Time elapsed: 4.252 s % 148.94/21.26 % (1635842)Peak memory usage: 41 MB % 148.94/21.26 % (1635842)Instructions burned: 5132 (million) % 148.94/21.26 % (1636003)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2456073258:i=5497:nm=2_2952 on theBenchmark for (2952ds/5497Mi) % 148.94/21.26 % (1636003)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.94/21.26 % (1636003)Terminated due to inappropriate strategy. % 148.94/21.26 % (1636003)------------------------------ % 148.94/21.26 % (1636003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.94/21.26 % (1636003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.94/21.26 % (1636003)CaDiCaL version: 2.1.3 % 148.94/21.26 % (1636003)Termination reason: Inappropriate % 148.94/21.26 % (1636003)Time elapsed: 0.004 s % 148.94/21.26 % (1636003)Peak memory usage: 11 MB % 148.94/21.26 % (1636003)Instructions burned: 6 (million) % 148.94/21.26 % (1636003)------------------------------ % 148.94/21.26 % (1636003)------------------------------ % 148.94/21.26 % (1636005)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3103276420:fmbsr=2:i=46332_2952 on theBenchmark for (2952ds/46332Mi) % 148.94/21.26 % (1636005)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.94/21.26 % (1636005)Terminated due to inappropriate strategy. % 148.94/21.26 % (1636005)------------------------------ % 148.94/21.26 % (1636005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.94/21.27 % (1636005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.94/21.27 % (1636005)CaDiCaL version: 2.1.3 % 148.94/21.27 % (1636005)Termination reason: Inappropriate % 148.94/21.27 % (1636005)Time elapsed: 0.008 s % 148.94/21.27 % (1636005)Peak memory usage: 11 MB % 148.94/21.27 % (1636005)Instructions burned: 6 (million) % 148.94/21.27 % (1636005)------------------------------ % 148.94/21.27 % (1636005)------------------------------ % 148.94/21.27 % (1636008)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1620393525:i=14071_2952 on theBenchmark for (2952ds/14071Mi) % 148.94/21.27 % (1636008)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.94/21.27 % (1636008)Terminated due to inappropriate strategy. % 148.94/21.27 % (1636008)------------------------------ % 148.94/21.27 % (1636008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.94/21.27 % (1636008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.94/21.27 % (1636008)CaDiCaL version: 2.1.3 % 148.94/21.27 % (1636008)Termination reason: Inappropriate % 148.94/21.27 % (1636008)Time elapsed: 0.003 s % 148.94/21.27 % (1636008)Peak memory usage: 11 MB % 148.94/21.27 % (1636008)Instructions burned: 6 (million) % 148.94/21.27 % (1636008)------------------------------ % 148.94/21.27 % (1636008)------------------------------ % 148.94/21.27 % (1636011)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4227213145:i=22565:add=on:rawr=on_2951 on theBenchmark for (2951ds/22565Mi) % 148.94/21.27 % (1635961)Instruction limit reached! % 148.94/21.27 % (1635961)------------------------------ % 148.94/21.27 % (1635961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.94/21.27 % (1635961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.94/21.27 % (1635961)CaDiCaL version: 2.1.3 % 148.94/21.27 % (1635961)Termination reason: Instruction limit % 148.94/21.27 % (1635961)Termination phase: Saturation % 148.94/21.27 % (1635961)Time elapsed: 2.004 s % 148.94/21.27 % (1635961)Peak memory usage: 55 MB % 148.94/21.27 % (1635961)Instructions burned: 4591 (million) % 148.94/21.27 % (1636014)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3671083555:i=8173:av=off_2949 on theBenchmark for (2949ds/8173Mi) % 148.94/21.27 % (1635880)Instruction limit reached! % 150.34/21.45 % (1635880)------------------------------ % 150.34/21.45 % (1635880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.34/21.45 % (1635880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.34/21.45 % (1635880)CaDiCaL version: 2.1.3 % 150.34/21.45 % (1635880)Termination reason: Instruction limit % 150.34/21.45 % (1635880)Termination phase: Saturation % 150.34/21.45 % (1635880)Time elapsed: 4.242 s % 150.34/21.45 % (1635880)Peak memory usage: 38 MB % 150.34/21.45 % (1635880)Instructions burned: 5115 (million) % 150.34/21.45 % (1636082)dis+10_16:1_sil=16000:random_seed=2135000461:i=9155:fsr=off_2947 on theBenchmark for (2947ds/9155Mi) % 150.34/21.45 % (1635989)Instruction limit reached! % 150.34/21.45 % (1635989)------------------------------ % 150.34/21.45 % (1635989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.34/21.45 % (1635989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.34/21.45 % (1635989)CaDiCaL version: 2.1.3 % 150.34/21.45 % (1635989)Termination reason: Instruction limit % 150.34/21.45 % (1635989)Termination phase: Saturation % 150.34/21.45 % (1635989)Time elapsed: 2.926 s % 150.34/21.45 % (1635989)Peak memory usage: 45 MB % 150.34/21.45 % (1635989)Instructions burned: 5213 (million) % 150.34/21.45 % (1636170)ott-3_8_sil=64000:random_seed=1619255863:i=20139:bs=on_2929 on theBenchmark for (2929ds/20139Mi) % 150.34/21.45 % (1636014)Instruction limit reached! % 150.34/21.45 % (1636014)------------------------------ % 150.34/21.45 % (1636014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.34/21.45 % (1636014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.34/21.45 % (1636014)CaDiCaL version: 2.1.3 % 150.34/21.45 % (1636014)Termination reason: Instruction limit % 150.34/21.45 % (1636014)Termination phase: Saturation % 150.34/21.45 % (1636014)Time elapsed: 2.516 s % 150.34/21.45 % (1636014)Peak memory usage: 60 MB % 150.34/21.45 % (1636014)Instructions burned: 8175 (million) % 150.34/21.45 % (1636172)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=41875416:fmbsr=2:i=32576_2923 on theBenchmark for (2923ds/32576Mi) % 150.34/21.45 % (1636172)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.34/21.45 % (1636172)Terminated due to inappropriate strategy. % 150.34/21.45 % (1636172)------------------------------ % 150.34/21.45 % (1636172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.34/21.45 % (1636172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.34/21.45 % (1636172)CaDiCaL version: 2.1.3 % 150.34/21.45 % (1636172)Termination reason: Inappropriate % 150.34/21.45 % (1636172)Time elapsed: 0.002 s % 150.34/21.45 % (1636172)Peak memory usage: 11 MB % 150.34/21.45 % (1636172)Instructions burned: 6 (million) % 150.34/21.45 % (1636172)------------------------------ % 150.34/21.45 % (1636172)------------------------------ % 150.34/21.45 % (1636174)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2002299615:i=11404_2923 on theBenchmark for (2923ds/11404Mi) % 150.34/21.45 % (1636082)Instruction limit reached! % 150.34/21.45 % (1636082)------------------------------ % 150.34/21.45 % (1636082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.34/21.45 % (1636082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.34/21.45 % (1636082)CaDiCaL version: 2.1.3 % 150.34/21.45 % (1636082)Termination reason: Instruction limit % 150.34/21.45 % (1636082)Termination phase: Saturation % 150.34/21.45 % (1636082)Time elapsed: 4.698 s % 150.34/21.45 % (1636082)Peak memory usage: 60 MB % 150.34/21.45 % (1636082)Instructions burned: 9156 (million) % 150.34/21.45 % (1636176)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4087975883:i=14134_2900 on theBenchmark for (2900ds/14134Mi) % 150.34/21.45 % (1636174)Instruction limit reached! % 150.34/21.45 % (1636174)------------------------------ % 150.34/21.45 % (1636174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.34/21.45 % (1636174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.34/21.45 % (1636174)CaDiCaL version: 2.1.3 % 150.34/21.45 % (1636174)Termination reason: Instruction limit % 150.34/21.45 % (1636174)Termination phase: Saturation % 150.34/21.45 % (1636174)Time elapsed: 3.501 s % 150.34/21.45 % (1636174)Peak memory usage: 69 MB % 150.34/21.45 % (1636174)Instructions burned: 11406 (million) % 150.34/21.45 % (1636178)dis+33_16_sil=32000:sac=on:random_seed=2593930241:i=15851:nm=0_2888 on theBenchmark for (2888ds/15851Mi) % 150.34/21.45 % (1636011)Instruction limit reached! % 150.34/21.45 % (1636011)------------------------------ % 150.34/21.45 % (1636011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.93/30.55 % (1636011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.93/30.55 % (1636011)CaDiCaL version: 2.1.3 % 214.93/30.55 % (1636011)Termination reason: Instruction limit % 214.93/30.55 % (1636011)Termination phase: Saturation % 214.93/30.55 % (1636011)Time elapsed: 9.287 s % 214.93/30.55 % (1636011)Peak memory usage: 21 MB % 214.93/30.55 % (1636011)Instructions burned: 22567 (million) % 214.93/30.55 % (1636296)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3520367323:avsq=on:i=17627:add=on:amm=off_2858 on theBenchmark for (2858ds/17627Mi) % 214.93/30.55 % (1636178)Instruction limit reached! % 214.93/30.55 % (1636178)------------------------------ % 214.93/30.55 % (1636178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.93/30.55 % (1636178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.93/30.55 % (1636178)CaDiCaL version: 2.1.3 % 214.93/30.55 % (1636178)Termination reason: Instruction limit % 214.93/30.55 % (1636178)Termination phase: Saturation % 214.93/30.55 % (1636178)Time elapsed: 4.051 s % 214.93/30.55 % (1636178)Peak memory usage: 146 MB % 214.93/30.55 % (1636178)Instructions burned: 15854 (million) % 214.93/30.55 % (1636428)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2286305828:s2a=on:i=53295_2847 on theBenchmark for (2847ds/53295Mi) % 214.93/30.55 % (1636176)Instruction limit reached! % 214.93/30.55 % (1636176)------------------------------ % 214.93/30.55 % (1636176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.93/30.55 % (1636176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.93/30.55 % (1636176)CaDiCaL version: 2.1.3 % 214.93/30.55 % (1636176)Termination reason: Instruction limit % 214.93/30.55 % (1636176)Termination phase: Saturation % 214.93/30.55 % (1636176)Time elapsed: 9.889 s % 214.93/30.55 % (1636176)Peak memory usage: 74 MB % 214.93/30.55 % (1636176)Instructions burned: 14134 (million) % 214.93/30.55 % (1636486)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=700365112:i=26857:ins=20_2800 on theBenchmark for (2800ds/26857Mi) % 214.93/30.55 % (1636486)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 214.93/30.55 % (1636486)Terminated due to inappropriate strategy. % 214.93/30.55 % (1636486)------------------------------ % 214.93/30.55 % (1636486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.93/30.55 % (1636486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.93/30.55 % (1636486)CaDiCaL version: 2.1.3 % 214.93/30.55 % (1636486)Termination reason: Inappropriate % 214.93/30.55 % (1636486)Time elapsed: 0.005 s % 214.93/30.55 % (1636486)Peak memory usage: 11 MB % 214.93/30.55 % (1636486)Instructions burned: 6 (million) % 214.93/30.55 % (1636486)------------------------------ % 214.93/30.55 % (1636486)------------------------------ % 214.93/30.55 % (1636488)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3065572285:i=28120:bs=on:fsr=off_2800 on theBenchmark for (2800ds/28120Mi) % 214.93/30.55 % (1635976)Instruction limit reached! % 214.93/30.55 % (1635976)------------------------------ % 214.93/30.55 % (1635976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.93/30.55 % (1635976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.93/30.55 % (1635976)CaDiCaL version: 2.1.3 % 214.93/30.55 % (1635976)Termination reason: Instruction limit % 214.93/30.55 % (1635976)Termination phase: Saturation % 214.93/30.55 % (1635976)Time elapsed: 17.267 s % 214.93/30.55 % (1635976)Peak memory usage: 70 MB % 214.93/30.55 % (1635976)Instructions burned: 29340 (million) % 214.93/30.55 % (1636493)fmb+10_1_sil=256000:fmbss=7:random_seed=1740410094:fmbsr=1.6:i=182295_2790 on theBenchmark for (2790ds/182295Mi) % 214.93/30.55 % (1636493)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 214.93/30.55 % (1636493)Terminated due to inappropriate strategy. % 214.93/30.55 % (1636493)------------------------------ % 214.93/30.55 % (1636493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.93/30.55 % (1636493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.93/30.55 % (1636493)CaDiCaL version: 2.1.3 % 214.93/30.55 % (1636493)Termination reason: Inappropriate % 214.93/30.55 % (1636493)Time elapsed: 0.004 s % 214.93/30.55 % (1636493)Peak memory usage: 11 MB % 214.93/30.55 % (1636493)Instructions burned: 6 (million) % 214.93/30.55 % (1636493)------------------------------ % 214.93/30.55 % (1636493)------------------------------ % 214.93/30.55 % (1636495)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=556281601:i=44625:gsp=on_2789 on theBenchmark for (2789ds/44625Mi) % 236.44/33.55 % (1636495)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 236.44/33.55 % (1636495)Terminated due to inappropriate strategy. % 236.44/33.55 % (1636495)------------------------------ % 236.44/33.55 % (1636495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.44/33.55 % (1636495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.44/33.55 % (1636495)CaDiCaL version: 2.1.3 % 236.44/33.55 % (1636495)Termination reason: Inappropriate % 236.44/33.55 % (1636495)Time elapsed: 0.004 s % 236.44/33.55 % (1636495)Peak memory usage: 11 MB % 236.44/33.55 % (1636495)Instructions burned: 6 (million) % 236.44/33.55 % (1636495)------------------------------ % 236.44/33.55 % (1636495)------------------------------ % 236.44/33.55 % (1636497)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2408864806:i=160505_2789 on theBenchmark for (2789ds/160505Mi) % 236.44/33.55 % (1636497)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 236.44/33.55 % (1636497)Terminated due to inappropriate strategy. % 236.44/33.55 % (1636497)------------------------------ % 236.44/33.55 % (1636497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.44/33.55 % (1636497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.44/33.55 % (1636497)CaDiCaL version: 2.1.3 % 236.44/33.55 % (1636497)Termination reason: Inappropriate % 236.44/33.55 % (1636497)Time elapsed: 0.004 s % 236.44/33.55 % (1636497)Peak memory usage: 11 MB % 236.44/33.55 % (1636497)Instructions burned: 6 (million) % 236.44/33.55 % (1636497)------------------------------ % 236.44/33.55 % (1636497)------------------------------ % 236.44/33.55 % (1636499)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2622040166:fmbsr=1.3:i=225729_2789 on theBenchmark for (2789ds/225729Mi) % 236.44/33.55 % (1636499)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 236.44/33.55 % (1636499)Terminated due to inappropriate strategy. % 236.44/33.55 % (1636499)------------------------------ % 236.44/33.55 % (1636499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.44/33.55 % (1636499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.44/33.55 % (1636499)CaDiCaL version: 2.1.3 % 236.44/33.55 % (1636499)Termination reason: Inappropriate % 236.44/33.55 % (1636499)Time elapsed: 0.008 s % 236.44/33.55 % (1636499)Peak memory usage: 11 MB % 236.44/33.55 % (1636499)Instructions burned: 6 (million) % 236.44/33.55 % (1636499)------------------------------ % 236.44/33.55 % (1636499)------------------------------ % 236.44/33.55 % (1636501)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3195503694:fmbsr=2:i=185024:ins=7_2788 on theBenchmark for (2788ds/185024Mi) % 236.44/33.55 % (1636501)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 236.44/33.55 % (1636501)Terminated due to inappropriate strategy. % 236.44/33.55 % (1636501)------------------------------ % 236.44/33.55 % (1636501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.44/33.55 % (1636501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.44/33.55 % (1636501)CaDiCaL version: 2.1.3 % 236.44/33.55 % (1636501)Termination reason: Inappropriate % 236.44/33.55 % (1636501)Time elapsed: 0.004 s % 236.44/33.55 % (1636501)Peak memory usage: 11 MB % 236.44/33.55 % (1636501)Instructions burned: 6 (million) % 236.44/33.55 % (1636501)------------------------------ % 236.44/33.55 % (1636501)------------------------------ % 236.44/33.55 % (1636503)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4148324086:rtra=on_2788 on theBenchmark for (2788ds/0Mi) % 236.44/33.55 % (1636503)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 236.44/33.55 % (1636503)Terminated due to inappropriate strategy. % 236.44/33.55 % (1636503)------------------------------ % 236.44/33.55 % (1636503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.44/33.55 % (1636503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.44/33.55 % (1636503)CaDiCaL version: 2.1.3 % 236.44/33.55 % (1636503)Termination reason: Inappropriate % 236.44/33.55 % (1636503)Time elapsed: 0.007 s % 236.44/33.55 % (1636503)Peak memory usage: 10 MB % 236.44/33.55 % (1636503)Instructions burned: 6 (million) % 236.44/33.55 % (1636503)------------------------------ % 236.44/33.55 % (1636503)------------------------------ % 236.44/33.55 % (1636505)% WARNING: option uhcvi not known. % 236.44/33.55 % (1636505)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1547311695:i=271062:add=off:rtra=on:rawr=on_2788 on theBenchmark for (2788ds/271062Mi) % 262.69/37.23 % (1636170)Instruction limit reached! % 262.69/37.23 % (1636170)------------------------------ % 262.69/37.23 % (1636170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.69/37.23 % (1636170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.69/37.23 % (1636170)CaDiCaL version: 2.1.3 % 262.69/37.23 % (1636170)Termination reason: Instruction limit % 262.69/37.23 % (1636170)Termination phase: Saturation % 262.69/37.23 % (1636170)Time elapsed: 14.170 s % 262.69/37.23 % (1636170)Peak memory usage: 143 MB % 262.69/37.23 % (1636170)Instructions burned: 20139 (million) % 262.69/37.23 % (1636507)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=669806560:i=176048:add=on:rtra=on:rawr=on_2787 on theBenchmark for (2787ds/176048Mi) % 262.69/37.23 % (1636296)Instruction limit reached! % 262.69/37.23 % (1636296)------------------------------ % 262.69/37.23 % (1636296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.69/37.23 % (1636296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.69/37.23 % (1636296)CaDiCaL version: 2.1.3 % 262.69/37.23 % (1636296)Termination reason: Instruction limit % 262.69/37.23 % (1636296)Termination phase: Saturation % 262.69/37.23 % (1636296)Time elapsed: 15.141 s % 262.69/37.23 % (1636296)Peak memory usage: 175 MB % 262.69/37.23 % (1636296)Instructions burned: 17628 (million) % 262.69/37.23 % (1636525)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3960683285:i=206:fgj=on:rtra=on_2706 on theBenchmark for (2706ds/206Mi) % 262.69/37.23 % (1636525)Instruction limit reached! % 262.69/37.23 % (1636525)------------------------------ % 262.69/37.23 % (1636525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.69/37.23 % (1636525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.69/37.23 % (1636525)CaDiCaL version: 2.1.3 % 262.69/37.23 % (1636525)Termination reason: Instruction limit % 262.69/37.23 % (1636525)Termination phase: Saturation % 262.69/37.23 % (1636525)Time elapsed: 0.188 s % 262.69/37.23 % (1636525)Peak memory usage: 14 MB % 262.69/37.23 % (1636525)Instructions burned: 207 (million) % 262.69/37.23 % (1636528)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=425802860:i=232:rtra=on_2704 on theBenchmark for (2704ds/232Mi) % 262.69/37.23 % (1636528)Instruction limit reached! % 262.69/37.23 % (1636528)------------------------------ % 262.69/37.23 % (1636528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.69/37.23 % (1636528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.69/37.23 % (1636528)CaDiCaL version: 2.1.3 % 262.69/37.23 % (1636528)Termination reason: Instruction limit % 262.69/37.23 % (1636528)Termination phase: Saturation % 262.69/37.23 % (1636528)Time elapsed: 0.222 s % 262.69/37.23 % (1636528)Peak memory usage: 14 MB % 262.69/37.23 % (1636528)Instructions burned: 233 (million) % 262.69/37.23 % (1636531)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=525538468:i=262:rtra=on_2701 on theBenchmark for (2701ds/262Mi) % 262.69/37.23 % (1636531)Instruction limit reached! % 262.69/37.23 % (1636531)------------------------------ % 262.69/37.23 % (1636531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.69/37.23 % (1636531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.69/37.23 % (1636531)CaDiCaL version: 2.1.3 % 262.69/37.23 % (1636531)Termination reason: Instruction limit % 262.69/37.23 % (1636531)Termination phase: Saturation % 262.69/37.23 % (1636531)Time elapsed: 0.177 s % 262.69/37.23 % (1636531)Peak memory usage: 14 MB % 262.69/37.23 % (1636531)Instructions burned: 264 (million) % 262.69/37.23 % (1636533)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3281496906:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2699 on theBenchmark for (2699ds/318Mi) % 262.69/37.23 % (1636533)Instruction limit reached! % 262.69/37.23 % (1636533)------------------------------ % 262.69/37.23 % (1636533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.69/37.23 % (1636533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.69/37.23 % (1636533)CaDiCaL version: 2.1.3 % 262.69/37.23 % (1636533)Termination reason: Instruction limit % 262.69/37.23 % (1636533)Termination phase: Saturation % 262.69/37.23 % (1636533)Time elapsed: 0.259 s % 262.69/37.23 % (1636533)Peak memory usage: 15 MB % 262.69/37.23 % (1636533)Instructions burned: 318 (million) % 262.69/37.23 % (1636536)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1734858008:i=1428:nm=2:rtra=on_2696 on theBenchmark for (2696ds/1428Mi) % 278.31/39.46 % (1636536)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 278.31/39.46 % (1636536)Terminated due to inappropriate strategy. % 278.31/39.46 % (1636536)------------------------------ % 278.31/39.46 % (1636536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.31/39.46 % (1636536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.31/39.46 % (1636536)CaDiCaL version: 2.1.3 % 278.31/39.46 % (1636536)Termination reason: Inappropriate % 278.31/39.46 % (1636536)Time elapsed: 0.004 s % 278.31/39.46 % (1636536)Peak memory usage: 11 MB % 278.31/39.46 % (1636536)Instructions burned: 6 (million) % 278.31/39.46 % (1636536)------------------------------ % 278.31/39.46 % (1636536)------------------------------ % 278.31/39.46 % (1636538)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=649419288:i=262:bd=preordered:rtra=on:fsd=on_2696 on theBenchmark for (2696ds/262Mi) % 278.31/39.46 % (1636538)Instruction limit reached! % 278.31/39.46 % (1636538)------------------------------ % 278.31/39.46 % (1636538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.31/39.46 % (1636538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.31/39.46 % (1636538)CaDiCaL version: 2.1.3 % 278.31/39.46 % (1636538)Termination reason: Instruction limit % 278.31/39.46 % (1636538)Termination phase: Saturation % 278.31/39.46 % (1636538)Time elapsed: 0.310 s % 278.31/39.46 % (1636538)Peak memory usage: 15 MB % 278.31/39.46 % (1636538)Instructions burned: 273 (million) % 278.31/39.46 % (1636541)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=797817045:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2693 on theBenchmark for (2693ds/1368Mi) % 278.31/39.46 % (1636541)Instruction limit reached! % 278.31/39.46 % (1636541)------------------------------ % 278.31/39.46 % (1636541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.31/39.46 % (1636541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.31/39.46 % (1636541)CaDiCaL version: 2.1.3 % 278.31/39.46 % (1636541)Termination reason: Instruction limit % 278.31/39.46 % (1636541)Termination phase: Saturation % 278.31/39.46 % (1636541)Time elapsed: 1.336 s % 278.31/39.46 % (1636541)Peak memory usage: 21 MB % 278.31/39.46 % (1636541)Instructions burned: 1368 (million) % 278.31/39.46 % (1636545)ott-21_1_sil=16000:si=on:fs=off:random_seed=1290143386:i=360:av=off:fsr=off:rtra=on_2679 on theBenchmark for (2679ds/360Mi) % 278.31/39.46 % (1636545)Instruction limit reached! % 278.31/39.46 % (1636545)------------------------------ % 278.31/39.46 % (1636545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.31/39.46 % (1636545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.31/39.46 % (1636545)CaDiCaL version: 2.1.3 % 278.31/39.46 % (1636545)Termination reason: Instruction limit % 278.31/39.46 % (1636545)Termination phase: Saturation % 278.31/39.46 % (1636545)Time elapsed: 0.255 s % 278.31/39.46 % (1636545)Peak memory usage: 14 MB % 278.31/39.46 % (1636545)Instructions burned: 360 (million) % 278.31/39.46 % (1636548)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2400549528:i=954:bd=all:rtra=on_2676 on theBenchmark for (2676ds/954Mi) % 278.31/39.46 % (1636548)Instruction limit reached! % 278.31/39.46 % (1636548)------------------------------ % 278.31/39.46 % (1636548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.31/39.46 % (1636548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.31/39.46 % (1636548)CaDiCaL version: 2.1.3 % 278.31/39.46 % (1636548)Termination reason: Instruction limit % 278.31/39.46 % (1636548)Termination phase: Saturation % 278.31/39.46 % (1636548)Time elapsed: 0.934 s % 278.31/39.46 % (1636548)Peak memory usage: 16 MB % 278.31/39.46 % (1636548)Instructions burned: 955 (million) % 278.31/39.46 % (1636550)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=404059160:fmbsr=1.3:i=1730:ins=25:rtra=on_2667 on theBenchmark for (2667ds/1730Mi) % 278.31/39.46 % (1636550)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 278.31/39.46 % (1636550)Terminated due to inappropriate strategy. % 278.31/39.46 % (1636550)------------------------------ % 278.31/39.46 % (1636550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.31/39.46 % (1636550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.31/39.46 % (1636550)CaDiCaL version: 2.1.3 % 278.31/39.46 % (1636550)Termination reason: Inappropriate % 278.31/39.46 % (1636550)Terminated % 300.36/42.54 % Vampire exiting %------------------------------------------------------------------------------