%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC465_1 : TPTP v9.3.1. Bugfixed v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n010.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:02 PM UTC 2026 % Result : Timeout 300.05s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC465_1 : TPTP v9.3.1. Bugfixed v9.1.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.12/0.27 % Computer : n010.cluster.edu % 0.12/0.27 % Model : x86_64 x86_64 % 0.12/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.27 % Memory : 8046.5625MB % 0.12/0.27 % OS : Linux 6.8.0-71-generic % 0.12/0.27 % CPULimit : 300 % 0.12/0.27 % WCLimit : 300 % 0.12/0.27 % DateTime : Mon Sep 28 09:40:03 UTC 2026 % 0.12/0.27 % CPUTime : % 0.12/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.12/0.30 Running first-order model finding % 0.12/0.31 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 % 5.92/1.16 % (1804083)Will run a generic schedule for satisfiability detection. % 5.92/1.16 % (1804094)dis+10_1_sil=32000:sp=arity:random_seed=2295631293:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi) % 5.92/1.16 % (1804092)% WARNING: option uhcvi not known. % 5.92/1.16 % (1804091)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3890646844_3000 on theBenchmark for (3000ds/0Mi) % 5.92/1.16 % (1804097)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=310734533:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi) % 5.92/1.16 % (1804091)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.92/1.16 % (1804091)Terminated due to inappropriate strategy. % 5.92/1.16 % (1804091)------------------------------ % 5.92/1.16 % (1804091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.92/1.16 % (1804091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.92/1.16 % (1804091)CaDiCaL version: 2.1.3 % 5.92/1.16 % (1804091)Termination reason: Inappropriate % 5.92/1.16 % (1804091)Time elapsed: 0.001 s % 5.92/1.16 % (1804091)Peak memory usage: 11 MB % 5.92/1.16 % (1804091)Instructions burned: 1 (million) % 5.92/1.16 % (1804095)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2032944424:i=116_3000 on theBenchmark for (3000ds/116Mi) % 5.92/1.16 % (1804093)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2851626497:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi) % 5.92/1.16 % (1804091)------------------------------ % 5.92/1.16 % (1804091)------------------------------ % 5.92/1.16 % (1804092)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1432575765:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi) % 5.92/1.16 % (1804096)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1849779455:i=131_3000 on theBenchmark for (3000ds/131Mi) % 5.92/1.16 % (1804094)Instruction limit reached! % 5.92/1.16 % (1804094)------------------------------ % 5.92/1.16 % (1804094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.92/1.16 % (1804094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.92/1.16 % (1804094)CaDiCaL version: 2.1.3 % 5.92/1.16 % (1804094)Termination reason: Instruction limit % 5.92/1.16 % (1804094)Termination phase: Saturation % 5.92/1.16 % (1804094)Time elapsed: 0.050 s % 5.92/1.16 % (1804094)Peak memory usage: 12 MB % 5.92/1.16 % (1804094)Instructions burned: 104 (million) % 5.92/1.16 % (1804108)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=804655180:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 5.92/1.16 % (1804112)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2844336017:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 5.92/1.16 % (1804108)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.92/1.16 % (1804108)Terminated due to inappropriate strategy. % 5.92/1.16 % (1804108)------------------------------ % 5.92/1.16 % (1804108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.92/1.16 % (1804108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.92/1.16 % (1804108)CaDiCaL version: 2.1.3 % 5.92/1.16 % (1804108)Termination reason: Inappropriate % 5.92/1.16 % (1804108)Time elapsed: 0.001 s % 5.92/1.16 % (1804108)Peak memory usage: 10 MB % 5.92/1.16 % (1804108)Instructions burned: 1 (million) % 5.92/1.16 % (1804108)------------------------------ % 5.92/1.16 % (1804108)------------------------------ % 5.92/1.16 % (1804115)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=1115288473:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 5.92/1.16 % (1804096)Instruction limit reached! % 5.92/1.16 % (1804096)------------------------------ % 5.92/1.16 % (1804096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.92/1.16 % (1804096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.92/1.16 % (1804096)CaDiCaL version: 2.1.3 % 5.92/1.16 % (1804096)Termination reason: Instruction limit % 5.92/1.16 % (1804096)Termination phase: Saturation % 5.92/1.16 % (1804096)Time elapsed: 0.084 s % 5.92/1.16 % (1804096)Peak memory usage: 13 MB % 5.92/1.16 % (1804096)Instructions burned: 131 (million) % 5.92/1.16 % (1804095)Instruction limit reached! % 5.92/1.16 % (1804095)------------------------------ % 5.92/1.16 % (1804095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.60/1.67 % (1804095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.60/1.67 % (1804095)CaDiCaL version: 2.1.3 % 8.60/1.67 % (1804095)Termination reason: Instruction limit % 8.60/1.67 % (1804095)Termination phase: Saturation % 8.60/1.67 % (1804095)Time elapsed: 0.105 s % 8.60/1.67 % (1804095)Peak memory usage: 12 MB % 8.60/1.67 % (1804095)Instructions burned: 117 (million) % 8.60/1.67 % (1804117)ott-21_1_sil=16000:fs=off:random_seed=630709390:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.60/1.67 % (1804112)Instruction limit reached! % 8.60/1.67 % (1804112)------------------------------ % 8.60/1.67 % (1804112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.60/1.67 % (1804112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.60/1.67 % (1804112)CaDiCaL version: 2.1.3 % 8.60/1.67 % (1804112)Termination reason: Instruction limit % 8.60/1.67 % (1804112)Termination phase: Saturation % 8.60/1.67 % (1804112)Time elapsed: 0.064 s % 8.60/1.67 % (1804112)Peak memory usage: 12 MB % 8.60/1.67 % (1804112)Instructions burned: 133 (million) % 8.60/1.67 % (1804118)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=471709150:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.60/1.67 % (1804097)Instruction limit reached! % 8.60/1.67 % (1804097)------------------------------ % 8.60/1.67 % (1804097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.60/1.67 % (1804097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.60/1.67 % (1804097)CaDiCaL version: 2.1.3 % 8.60/1.67 % (1804097)Termination reason: Instruction limit % 8.60/1.67 % (1804097)Termination phase: Saturation % 8.60/1.67 % (1804097)Time elapsed: 0.148 s % 8.60/1.67 % (1804097)Peak memory usage: 12 MB % 8.60/1.67 % (1804097)Instructions burned: 159 (million) % 8.60/1.67 % (1804120)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1065401819:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 8.60/1.67 % (1804120)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.60/1.67 % (1804120)Terminated due to inappropriate strategy. % 8.60/1.67 % (1804120)------------------------------ % 8.60/1.67 % (1804120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.60/1.67 % (1804120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.60/1.67 % (1804120)CaDiCaL version: 2.1.3 % 8.60/1.67 % (1804120)Termination reason: Inappropriate % 8.60/1.67 % (1804120)Time elapsed: 0.001 s % 8.60/1.67 % (1804120)Peak memory usage: 11 MB % 8.60/1.67 % (1804120)Instructions burned: 1 (million) % 8.60/1.67 % (1804120)------------------------------ % 8.60/1.67 % (1804120)------------------------------ % 8.60/1.67 % (1804124)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2750097993:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 8.60/1.67 % (1804127)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2170510231:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 8.60/1.67 % (1804127)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.60/1.67 % (1804127)Terminated due to inappropriate strategy. % 8.60/1.67 % (1804127)------------------------------ % 8.60/1.67 % (1804127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.60/1.67 % (1804127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.60/1.67 % (1804127)CaDiCaL version: 2.1.3 % 8.60/1.67 % (1804127)Termination reason: Inappropriate % 8.60/1.67 % (1804127)Time elapsed: 0.001 s % 8.60/1.67 % (1804127)Peak memory usage: 10 MB % 8.60/1.67 % (1804127)Instructions burned: 1 (million) % 8.60/1.67 % (1804127)------------------------------ % 8.60/1.67 % (1804127)------------------------------ % 8.60/1.67 % (1804132)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=3820217054: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) % 8.60/1.67 % (1804117)Instruction limit reached! % 8.60/1.67 % (1804117)------------------------------ % 8.60/1.67 % (1804117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.60/1.67 % (1804117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.60/1.67 % (1804117)CaDiCaL version: 2.1.3 % 8.60/1.67 % (1804117)Termination reason: Instruction limit % 8.60/1.67 % (1804117)Termination phase: Saturation % 30.59/4.75 % (1804117)Time elapsed: 0.140 s % 30.59/4.75 % (1804117)Peak memory usage: 12 MB % 30.59/4.75 % (1804117)Instructions burned: 180 (million) % 30.59/4.75 % (1804138)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2296602634:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 30.59/4.75 % (1804115)Instruction limit reached! % 30.59/4.75 % (1804115)------------------------------ % 30.59/4.75 % (1804115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.59/4.75 % (1804115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.59/4.75 % (1804115)CaDiCaL version: 2.1.3 % 30.59/4.75 % (1804115)Termination reason: Instruction limit % 30.59/4.75 % (1804115)Termination phase: Saturation % 30.59/4.75 % (1804115)Time elapsed: 0.339 s % 30.59/4.75 % (1804115)Peak memory usage: 17 MB % 30.59/4.75 % (1804115)Instructions burned: 686 (million) % 30.59/4.75 % (1804147)fmb+10_1_sil=64000:random_seed=170041073:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 30.59/4.75 % (1804147)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.59/4.75 % (1804147)Terminated due to inappropriate strategy. % 30.59/4.75 % (1804147)------------------------------ % 30.59/4.75 % (1804147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.59/4.75 % (1804147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.59/4.75 % (1804147)CaDiCaL version: 2.1.3 % 30.59/4.75 % (1804147)Termination reason: Inappropriate % 30.59/4.75 % (1804147)Time elapsed: 0.001 s % 30.59/4.75 % (1804147)Peak memory usage: 10 MB % 30.59/4.75 % (1804147)Instructions burned: 1 (million) % 30.59/4.75 % (1804147)------------------------------ % 30.59/4.75 % (1804147)------------------------------ % 30.59/4.75 % (1804151)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=213796751:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 30.59/4.75 % (1804151)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.59/4.75 % (1804151)Terminated due to inappropriate strategy. % 30.59/4.75 % (1804151)------------------------------ % 30.59/4.75 % (1804151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.59/4.75 % (1804151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.59/4.75 % (1804151)CaDiCaL version: 2.1.3 % 30.59/4.75 % (1804151)Termination reason: Inappropriate % 30.59/4.75 % (1804151)Time elapsed: 0.0000 s % 30.59/4.75 % (1804151)Peak memory usage: 10 MB % 30.59/4.75 % (1804151)Instructions burned: 1 (million) % 30.59/4.75 % (1804151)------------------------------ % 30.59/4.75 % (1804151)------------------------------ % 30.59/4.75 % (1804154)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1406965775:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 30.59/4.75 % (1804154)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.59/4.75 % (1804154)Terminated due to inappropriate strategy. % 30.59/4.75 % (1804154)------------------------------ % 30.59/4.75 % (1804154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.59/4.75 % (1804154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.59/4.75 % (1804154)CaDiCaL version: 2.1.3 % 30.59/4.75 % (1804154)Termination reason: Inappropriate % 30.59/4.75 % (1804154)Time elapsed: 0.0000 s % 30.59/4.75 % (1804154)Peak memory usage: 10 MB % 30.59/4.75 % (1804154)Instructions burned: 1 (million) % 30.59/4.75 % (1804154)------------------------------ % 30.59/4.75 % (1804154)------------------------------ % 30.59/4.75 % (1804158)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=219148052:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 30.59/4.75 % (1804118)Instruction limit reached! % 30.59/4.75 % (1804118)------------------------------ % 30.59/4.75 % (1804118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.59/4.75 % (1804118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.59/4.75 % (1804118)CaDiCaL version: 2.1.3 % 30.59/4.75 % (1804118)Termination reason: Instruction limit % 30.59/4.75 % (1804118)Termination phase: Saturation % 30.59/4.75 % (1804118)Time elapsed: 0.442 s % 30.59/4.75 % (1804118)Peak memory usage: 14 MB % 30.59/4.75 % (1804118)Instructions burned: 478 (million) % 30.59/4.75 % (1804162)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=520808084:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi) % 30.59/4.75 % (1804132)Instruction limit reached! % 30.59/4.75 % (1804132)------------------------------ % 42.55/6.39 % (1804132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.55/6.39 % (1804132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.55/6.39 % (1804132)CaDiCaL version: 2.1.3 % 42.55/6.39 % (1804132)Termination reason: Instruction limit % 42.55/6.39 % (1804132)Termination phase: Saturation % 42.55/6.39 % (1804132)Time elapsed: 0.574 s % 42.55/6.39 % (1804132)Peak memory usage: 19 MB % 42.55/6.39 % (1804132)Instructions burned: 693 (million) % 42.55/6.39 % (1804175)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2736516864:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 42.55/6.39 % (1804175)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 42.55/6.39 % (1804175)Terminated due to inappropriate strategy. % 42.55/6.39 % (1804175)------------------------------ % 42.55/6.39 % (1804175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.55/6.39 % (1804175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.55/6.39 % (1804175)CaDiCaL version: 2.1.3 % 42.55/6.39 % (1804175)Termination reason: Inappropriate % 42.55/6.39 % (1804175)Time elapsed: 0.001 s % 42.55/6.39 % (1804175)Peak memory usage: 11 MB % 42.55/6.39 % (1804175)Instructions burned: 1 (million) % 42.55/6.39 % (1804175)------------------------------ % 42.55/6.39 % (1804175)------------------------------ % 42.55/6.39 % (1804177)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2385900192:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi) % 42.55/6.39 % (1804177)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 42.55/6.39 % (1804177)Terminated due to inappropriate strategy. % 42.55/6.39 % (1804177)------------------------------ % 42.55/6.39 % (1804177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.55/6.39 % (1804177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.55/6.39 % (1804177)CaDiCaL version: 2.1.3 % 42.55/6.39 % (1804177)Termination reason: Inappropriate % 42.55/6.39 % (1804177)Time elapsed: 0.001 s % 42.55/6.39 % (1804177)Peak memory usage: 11 MB % 42.55/6.39 % (1804177)Instructions burned: 1 (million) % 42.55/6.39 % (1804177)------------------------------ % 42.55/6.39 % (1804177)------------------------------ % 42.55/6.39 % (1804181)ott-2_1_sil=16000:newcnf=on:random_seed=2022354045:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 42.55/6.39 % (1804138)Instruction limit reached! % 42.55/6.39 % (1804138)------------------------------ % 42.55/6.39 % (1804138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.55/6.39 % (1804138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.55/6.39 % (1804138)CaDiCaL version: 2.1.3 % 42.55/6.39 % (1804138)Termination reason: Instruction limit % 42.55/6.39 % (1804138)Termination phase: Saturation % 42.55/6.39 % (1804138)Time elapsed: 0.735 s % 42.55/6.39 % (1804138)Peak memory usage: 18 MB % 42.55/6.39 % (1804138)Instructions burned: 880 (million) % 42.55/6.39 % (1804189)ott+10_1_sil=32000:tgt=ground:random_seed=703251289:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 42.55/6.39 % (1804124)Instruction limit reached! % 42.55/6.39 % (1804124)------------------------------ % 42.55/6.39 % (1804124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.55/6.39 % (1804124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.55/6.39 % (1804124)CaDiCaL version: 2.1.3 % 42.55/6.39 % (1804124)Termination reason: Instruction limit % 42.55/6.39 % (1804124)Termination phase: Saturation % 42.55/6.39 % (1804124)Time elapsed: 1.102 s % 42.55/6.39 % (1804124)Peak memory usage: 18 MB % 42.55/6.39 % (1804124)Instructions burned: 1179 (million) % 42.55/6.39 % (1804197)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1865040625:i=54282_2986 on theBenchmark for (2986ds/54282Mi) % 42.55/6.39 % (1804197)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 42.55/6.39 % (1804197)Terminated due to inappropriate strategy. % 42.55/6.39 % (1804197)------------------------------ % 42.55/6.39 % (1804197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.55/6.39 % (1804197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.55/6.39 % (1804197)CaDiCaL version: 2.1.3 % 42.55/6.39 % (1804197)Termination reason: Inappropriate % 42.55/6.39 % (1804197)Time elapsed: 0.001 s % 42.55/6.39 % (1804197)Peak memory usage: 11 MB % 42.55/6.39 % (1804197)Instructions burned: 1 (million) % 149.29/21.34 % (1804197)------------------------------ % 149.29/21.34 % (1804197)------------------------------ % 149.29/21.34 % (1804204)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2847084732:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi) % 149.29/21.34 % (1804181)Instruction limit reached! % 149.29/21.34 % (1804181)------------------------------ % 149.29/21.34 % (1804181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.29/21.34 % (1804181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.29/21.34 % (1804181)CaDiCaL version: 2.1.3 % 149.29/21.34 % (1804181)Termination reason: Instruction limit % 149.29/21.34 % (1804181)Termination phase: Saturation % 149.29/21.34 % (1804181)Time elapsed: 0.759 s % 149.29/21.34 % (1804181)Peak memory usage: 16 MB % 149.29/21.34 % (1804181)Instructions burned: 873 (million) % 149.29/21.34 % (1804215)dis+21_1_sil=32000:sas=cadical:random_seed=112314269:i=3773:amm=off_2983 on theBenchmark for (2983ds/3773Mi) % 149.29/21.34 % (1804162)Instruction limit reached! % 149.29/21.34 % (1804162)------------------------------ % 149.29/21.34 % (1804162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.29/21.34 % (1804162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.29/21.34 % (1804162)CaDiCaL version: 2.1.3 % 149.29/21.34 % (1804162)Termination reason: Instruction limit % 149.29/21.34 % (1804162)Termination phase: Saturation % 149.29/21.34 % (1804162)Time elapsed: 1.195 s % 149.29/21.34 % (1804162)Peak memory usage: 24 MB % 149.29/21.34 % (1804162)Instructions burned: 1473 (million) % 149.29/21.34 % (1804219)ott+11_1_sil=16000:gs=on:random_seed=2933006365:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2981 on theBenchmark for (2981ds/2251Mi) % 149.29/21.34 % (1804158)Instruction limit reached! % 149.29/21.34 % (1804158)------------------------------ % 149.29/21.34 % (1804158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.29/21.34 % (1804158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.29/21.34 % (1804158)CaDiCaL version: 2.1.3 % 149.29/21.34 % (1804158)Termination reason: Instruction limit % 149.29/21.34 % (1804158)Termination phase: Saturation % 149.29/21.34 % (1804158)Time elapsed: 2.307 s % 149.29/21.34 % (1804158)Peak memory usage: 41 MB % 149.29/21.34 % (1804158)Instructions burned: 5131 (million) % 149.29/21.34 % (1804248)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2256149312:fmbsr=1.6:i=67534_2971 on theBenchmark for (2971ds/67534Mi) % 149.29/21.34 % (1804248)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.29/21.34 % (1804248)Terminated due to inappropriate strategy. % 149.29/21.34 % (1804248)------------------------------ % 149.29/21.34 % (1804248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.29/21.34 % (1804248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.29/21.34 % (1804248)CaDiCaL version: 2.1.3 % 149.29/21.34 % (1804248)Termination reason: Inappropriate % 149.29/21.34 % (1804248)Time elapsed: 0.001 s % 149.29/21.34 % (1804248)Peak memory usage: 10 MB % 149.29/21.34 % (1804248)Instructions burned: 1 (million) % 149.29/21.34 % (1804248)------------------------------ % 149.29/21.34 % (1804248)------------------------------ % 149.29/21.34 % (1804250)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1260965049:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2971 on theBenchmark for (2971ds/4591Mi) % 149.29/21.34 % (1804219)Instruction limit reached! % 149.29/21.34 % (1804219)------------------------------ % 149.29/21.34 % (1804219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.29/21.34 % (1804219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.29/21.34 % (1804219)CaDiCaL version: 2.1.3 % 149.29/21.34 % (1804219)Termination reason: Instruction limit % 149.29/21.34 % (1804219)Termination phase: Saturation % 149.29/21.34 % (1804219)Time elapsed: 1.920 s % 149.29/21.34 % (1804219)Peak memory usage: 24 MB % 149.29/21.34 % (1804219)Instructions burned: 2252 (million) % 149.29/21.34 % (1804274)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2958945126:i=29340_2961 on theBenchmark for (2961ds/29340Mi) % 149.29/21.34 % (1804204)Instruction limit reached! % 149.29/21.34 % (1804204)------------------------------ % 149.29/21.34 % (1804204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.29/21.34 % (1804204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.29/21.34 % (1804204)CaDiCaL version: 2.1.3 % 149.29/21.34 % (1804204)Termination reason: Instruction limit % 196.27/27.96 % (1804204)Termination phase: Saturation % 196.27/27.96 % (1804204)Time elapsed: 3.040 s % 196.27/27.96 % (1804204)Peak memory usage: 35 MB % 196.27/27.96 % (1804204)Instructions burned: 3512 (million) % 196.27/27.96 % (1804290)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2107782915:i=5211_2955 on theBenchmark for (2955ds/5211Mi) % 196.27/27.96 % (1804250)Instruction limit reached! % 196.27/27.96 % (1804250)------------------------------ % 196.27/27.96 % (1804250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.27/27.96 % (1804250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.27/27.96 % (1804250)CaDiCaL version: 2.1.3 % 196.27/27.96 % (1804250)Termination reason: Instruction limit % 196.27/27.96 % (1804250)Termination phase: Saturation % 196.27/27.96 % (1804250)Time elapsed: 1.919 s % 196.27/27.96 % (1804250)Peak memory usage: 43 MB % 196.27/27.96 % (1804250)Instructions burned: 4591 (million) % 196.27/27.96 % (1804297)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=587787328:i=5497:nm=2_2951 on theBenchmark for (2951ds/5497Mi) % 196.27/27.96 % (1804297)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 196.27/27.96 % (1804297)Terminated due to inappropriate strategy. % 196.27/27.96 % (1804297)------------------------------ % 196.27/27.96 % (1804297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.27/27.96 % (1804297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.27/27.96 % (1804297)CaDiCaL version: 2.1.3 % 196.27/27.96 % (1804297)Termination reason: Inappropriate % 196.27/27.96 % (1804297)Time elapsed: 0.001 s % 196.27/27.96 % (1804297)Peak memory usage: 11 MB % 196.27/27.96 % (1804297)Instructions burned: 1 (million) % 196.27/27.96 % (1804297)------------------------------ % 196.27/27.96 % (1804297)------------------------------ % 196.27/27.96 % (1804299)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3986472594:fmbsr=2:i=46332_2951 on theBenchmark for (2951ds/46332Mi) % 196.27/27.96 % (1804299)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 196.27/27.96 % (1804299)Terminated due to inappropriate strategy. % 196.27/27.96 % (1804299)------------------------------ % 196.27/27.96 % (1804299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.27/27.96 % (1804299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.27/27.96 % (1804299)CaDiCaL version: 2.1.3 % 196.27/27.96 % (1804299)Termination reason: Inappropriate % 196.27/27.96 % (1804299)Time elapsed: 0.001 s % 196.27/27.96 % (1804299)Peak memory usage: 10 MB % 196.27/27.96 % (1804299)Instructions burned: 1 (million) % 196.27/27.96 % (1804299)------------------------------ % 196.27/27.96 % (1804299)------------------------------ % 196.27/27.96 % (1804301)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3467335397:i=14071_2951 on theBenchmark for (2951ds/14071Mi) % 196.27/27.96 % (1804301)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 196.27/27.96 % (1804301)Terminated due to inappropriate strategy. % 196.27/27.96 % (1804301)------------------------------ % 196.27/27.96 % (1804301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.27/27.96 % (1804301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.27/27.96 % (1804301)CaDiCaL version: 2.1.3 % 196.27/27.96 % (1804301)Termination reason: Inappropriate % 196.27/27.96 % (1804301)Time elapsed: 0.001 s % 196.27/27.96 % (1804301)Peak memory usage: 11 MB % 196.27/27.96 % (1804301)Instructions burned: 1 (million) % 196.27/27.96 % (1804301)------------------------------ % 196.27/27.96 % (1804301)------------------------------ % 196.27/27.96 % (1804215)Instruction limit reached! % 196.27/27.96 % (1804215)------------------------------ % 196.27/27.96 % (1804215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.27/27.96 % (1804215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.27/27.96 % (1804215)CaDiCaL version: 2.1.3 % 196.27/27.96 % (1804215)Termination reason: Instruction limit % 196.27/27.96 % (1804215)Termination phase: Saturation % 196.27/27.96 % (1804215)Time elapsed: 3.178 s % 196.27/27.96 % (1804215)Peak memory usage: 31 MB % 196.27/27.96 % (1804215)Instructions burned: 3773 (million) % 196.27/27.96 % (1804303)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3435291265:i=22565:add=on:rawr=on_2951 on theBenchmark for (2951ds/22565Mi) % 196.27/27.96 % (1804305)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=762558337:i=8173:av=off_2951 on theBenchmark for (2951ds/8173Mi) % 196.27/27.96 % (1804189)Instruction limit reached! % 197.34/28.12 % (1804189)------------------------------ % 197.34/28.12 % (1804189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.34/28.12 % (1804189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.34/28.12 % (1804189)CaDiCaL version: 2.1.3 % 197.34/28.12 % (1804189)Termination reason: Instruction limit % 197.34/28.12 % (1804189)Termination phase: Saturation % 197.34/28.12 % (1804189)Time elapsed: 4.973 s % 197.34/28.12 % (1804189)Peak memory usage: 42 MB % 197.34/28.12 % (1804189)Instructions burned: 5114 (million) % 197.34/28.12 % (1804327)dis+10_16:1_sil=16000:random_seed=4114632433:i=9155:fsr=off_2939 on theBenchmark for (2939ds/9155Mi) % 197.34/28.12 % (1804290)Instruction limit reached! % 197.34/28.12 % (1804290)------------------------------ % 197.34/28.12 % (1804290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.34/28.12 % (1804290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.34/28.12 % (1804290)CaDiCaL version: 2.1.3 % 197.34/28.12 % (1804290)Termination reason: Instruction limit % 197.34/28.12 % (1804290)Termination phase: Saturation % 197.34/28.12 % (1804290)Time elapsed: 4.481 s % 197.34/28.12 % (1804290)Peak memory usage: 49 MB % 197.34/28.12 % (1804290)Instructions burned: 5212 (million) % 197.34/28.12 % (1804363)ott-3_8_sil=64000:random_seed=3332984333:i=20139:bs=on_2910 on theBenchmark for (2910ds/20139Mi) % 197.34/28.12 % (1804305)Instruction limit reached! % 197.34/28.12 % (1804305)------------------------------ % 197.34/28.12 % (1804305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.34/28.12 % (1804305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.34/28.12 % (1804305)CaDiCaL version: 2.1.3 % 197.34/28.12 % (1804305)Termination reason: Instruction limit % 197.34/28.12 % (1804305)Termination phase: Saturation % 197.34/28.12 % (1804305)Time elapsed: 8.258 s % 197.34/28.12 % (1804305)Peak memory usage: 51 MB % 197.34/28.12 % (1804305)Instructions burned: 8173 (million) % 197.34/28.12 % (1804385)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2034586601:fmbsr=2:i=32576_2868 on theBenchmark for (2868ds/32576Mi) % 197.34/28.12 % (1804385)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.34/28.12 % (1804385)Terminated due to inappropriate strategy. % 197.34/28.12 % (1804385)------------------------------ % 197.34/28.12 % (1804385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.34/28.12 % (1804385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.34/28.12 % (1804385)CaDiCaL version: 2.1.3 % 197.34/28.12 % (1804385)Termination reason: Inappropriate % 197.34/28.12 % (1804385)Time elapsed: 0.002 s % 197.34/28.12 % (1804385)Peak memory usage: 10 MB % 197.34/28.12 % (1804385)Instructions burned: 1 (million) % 197.34/28.12 % (1804385)------------------------------ % 197.34/28.12 % (1804385)------------------------------ % 197.34/28.12 % (1804388)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3382121410:i=11404_2867 on theBenchmark for (2867ds/11404Mi) % 197.34/28.12 % (1804303)Instruction limit reached! % 197.34/28.12 % (1804303)------------------------------ % 197.34/28.12 % (1804303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.34/28.12 % (1804303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.34/28.12 % (1804303)CaDiCaL version: 2.1.3 % 197.34/28.12 % (1804303)Termination reason: Instruction limit % 197.34/28.12 % (1804303)Termination phase: Saturation % 197.34/28.12 % (1804303)Time elapsed: 8.428 s % 197.34/28.12 % (1804303)Peak memory usage: 29 MB % 197.34/28.12 % (1804303)Instructions burned: 22566 (million) % 197.34/28.12 % (1804390)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=881071528:i=14134_2866 on theBenchmark for (2866ds/14134Mi) % 197.34/28.12 % (1804327)Instruction limit reached! % 197.34/28.12 % (1804327)------------------------------ % 197.34/28.12 % (1804327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.34/28.12 % (1804327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.34/28.12 % (1804327)CaDiCaL version: 2.1.3 % 197.34/28.12 % (1804327)Termination reason: Instruction limit % 197.34/28.12 % (1804327)Termination phase: Saturation % 197.34/28.12 % (1804327)Time elapsed: 7.865 s % 197.34/28.12 % (1804327)Peak memory usage: 52 MB % 197.34/28.12 % (1804327)Instructions burned: 9155 (million) % 197.34/28.12 % (1804393)dis+33_16_sil=32000:sac=on:random_seed=3011527710:i=15851:nm=0_2860 on theBenchmark for (2860ds/15851Mi) % 197.34/28.12 % (1804390)Instruction limit reached! % 197.34/28.12 % (1804390)------------------------------ % 197.34/28.12 % (1804390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.62/29.89 % (1804390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.62/29.89 % (1804390)CaDiCaL version: 2.1.3 % 209.62/29.89 % (1804390)Termination reason: Instruction limit % 209.62/29.89 % (1804390)Termination phase: Saturation % 209.62/29.89 % (1804390)Time elapsed: 7.668 s % 209.62/29.89 % (1804390)Peak memory usage: 73 MB % 209.62/29.89 % (1804390)Instructions burned: 14136 (million) % 209.62/29.89 % (1804412)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1233941536:avsq=on:i=17627:add=on:amm=off_2789 on theBenchmark for (2789ds/17627Mi) % 209.62/29.89 % (1804388)Instruction limit reached! % 209.62/29.89 % (1804388)------------------------------ % 209.62/29.89 % (1804388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.62/29.89 % (1804388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.62/29.89 % (1804388)CaDiCaL version: 2.1.3 % 209.62/29.89 % (1804388)Termination reason: Instruction limit % 209.62/29.89 % (1804388)Termination phase: Saturation % 209.62/29.89 % (1804388)Time elapsed: 11.768 s % 209.62/29.89 % (1804388)Peak memory usage: 71 MB % 209.62/29.89 % (1804388)Instructions burned: 11404 (million) % 209.62/29.89 % (1804419)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4038073920:s2a=on:i=53295_2749 on theBenchmark for (2749ds/53295Mi) % 209.62/29.89 % (1804274)Instruction limit reached! % 209.62/29.89 % (1804274)------------------------------ % 209.62/29.89 % (1804274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.62/29.89 % (1804274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.62/29.89 % (1804274)CaDiCaL version: 2.1.3 % 209.62/29.89 % (1804274)Termination reason: Instruction limit % 209.62/29.89 % (1804274)Termination phase: Saturation % 209.62/29.89 % (1804274)Time elapsed: 22.502 s % 209.62/29.89 % (1804274)Peak memory usage: 169 MB % 209.62/29.89 % (1804274)Instructions burned: 29341 (million) % 209.62/29.89 % (1804426)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=522557410:i=26857:ins=20_2736 on theBenchmark for (2736ds/26857Mi) % 209.62/29.89 % (1804426)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 209.62/29.89 % (1804426)Terminated due to inappropriate strategy. % 209.62/29.89 % (1804426)------------------------------ % 209.62/29.89 % (1804426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.62/29.89 % (1804426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.62/29.89 % (1804426)CaDiCaL version: 2.1.3 % 209.62/29.89 % (1804426)Termination reason: Inappropriate % 209.62/29.89 % (1804426)Time elapsed: 0.001 s % 209.62/29.89 % (1804426)Peak memory usage: 11 MB % 209.62/29.89 % (1804426)Instructions burned: 1 (million) % 209.62/29.89 % (1804426)------------------------------ % 209.62/29.89 % (1804426)------------------------------ % 209.62/29.89 % (1804428)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3290333132:i=28120:bs=on:fsr=off_2735 on theBenchmark for (2735ds/28120Mi) % 209.62/29.89 % (1804393)Instruction limit reached! % 209.62/29.89 % (1804393)------------------------------ % 209.62/29.89 % (1804393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.62/29.89 % (1804393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.62/29.89 % (1804393)CaDiCaL version: 2.1.3 % 209.62/29.89 % (1804393)Termination reason: Instruction limit % 209.62/29.89 % (1804393)Termination phase: Saturation % 209.62/29.89 % (1804393)Time elapsed: 13.495 s % 209.62/29.89 % (1804393)Peak memory usage: 204 MB % 209.62/29.89 % (1804393)Instructions burned: 15851 (million) % 209.62/29.89 % (1804437)fmb+10_1_sil=256000:fmbss=7:random_seed=1982361528:fmbsr=1.6:i=182295_2724 on theBenchmark for (2724ds/182295Mi) % 209.62/29.89 % (1804437)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 209.62/29.89 % (1804437)Terminated due to inappropriate strategy. % 209.62/29.89 % (1804437)------------------------------ % 209.62/29.89 % (1804437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.62/29.89 % (1804437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.62/29.89 % (1804437)CaDiCaL version: 2.1.3 % 209.62/29.89 % (1804437)Termination reason: Inappropriate % 209.62/29.89 % (1804437)Time elapsed: 0.001 s % 209.62/29.89 % (1804437)Peak memory usage: 11 MB % 209.62/29.89 % (1804437)Instructions burned: 1 (million) % 209.62/29.89 % (1804437)------------------------------ % 209.62/29.89 % (1804437)------------------------------ % 209.62/29.89 % (1804439)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1825872251:i=44625:gsp=on_2723 on theBenchmark for (2723ds/44625Mi) % 225.63/32.06 % (1804439)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 225.63/32.06 % (1804439)Terminated due to inappropriate strategy. % 225.63/32.06 % (1804439)------------------------------ % 225.63/32.06 % (1804439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.63/32.06 % (1804439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.63/32.06 % (1804439)CaDiCaL version: 2.1.3 % 225.63/32.06 % (1804439)Termination reason: Inappropriate % 225.63/32.06 % (1804439)Time elapsed: 0.002 s % 225.63/32.06 % (1804439)Peak memory usage: 10 MB % 225.63/32.06 % (1804439)Instructions burned: 1 (million) % 225.63/32.06 % (1804439)------------------------------ % 225.63/32.06 % (1804439)------------------------------ % 225.63/32.06 % (1804441)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1945137344:i=160505_2723 on theBenchmark for (2723ds/160505Mi) % 225.63/32.06 % (1804441)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 225.63/32.06 % (1804441)Terminated due to inappropriate strategy. % 225.63/32.06 % (1804441)------------------------------ % 225.63/32.06 % (1804441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.63/32.06 % (1804441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.63/32.06 % (1804441)CaDiCaL version: 2.1.3 % 225.63/32.06 % (1804441)Termination reason: Inappropriate % 225.63/32.06 % (1804441)Time elapsed: 0.001 s % 225.63/32.06 % (1804441)Peak memory usage: 11 MB % 225.63/32.06 % (1804441)Instructions burned: 1 (million) % 225.63/32.06 % (1804441)------------------------------ % 225.63/32.06 % (1804441)------------------------------ % 225.63/32.06 % (1804443)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2388201688:fmbsr=1.3:i=225729_2723 on theBenchmark for (2723ds/225729Mi) % 225.63/32.06 % (1804443)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 225.63/32.06 % (1804443)Terminated due to inappropriate strategy. % 225.63/32.06 % (1804443)------------------------------ % 225.63/32.06 % (1804443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.63/32.06 % (1804443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.63/32.06 % (1804443)CaDiCaL version: 2.1.3 % 225.63/32.06 % (1804443)Termination reason: Inappropriate % 225.63/32.06 % (1804443)Time elapsed: 0.003 s % 225.63/32.06 % (1804443)Peak memory usage: 11 MB % 225.63/32.06 % (1804443)Instructions burned: 1 (million) % 225.63/32.06 % (1804443)------------------------------ % 225.63/32.06 % (1804443)------------------------------ % 225.63/32.06 % (1804445)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3320550458:fmbsr=2:i=185024:ins=7_2722 on theBenchmark for (2722ds/185024Mi) % 225.63/32.06 % (1804445)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 225.63/32.06 % (1804445)Terminated due to inappropriate strategy. % 225.63/32.06 % (1804445)------------------------------ % 225.63/32.06 % (1804445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.63/32.06 % (1804445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.63/32.06 % (1804445)CaDiCaL version: 2.1.3 % 225.63/32.06 % (1804445)Termination reason: Inappropriate % 225.63/32.06 % (1804445)Time elapsed: 0.002 s % 225.63/32.06 % (1804445)Peak memory usage: 11 MB % 225.63/32.06 % (1804445)Instructions burned: 1 (million) % 225.63/32.06 % (1804445)------------------------------ % 225.63/32.06 % (1804445)------------------------------ % 225.63/32.06 % (1804447)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2336000574:rtra=on_2722 on theBenchmark for (2722ds/0Mi) % 225.63/32.06 % (1804447)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 225.63/32.06 % (1804447)Terminated due to inappropriate strategy. % 225.63/32.06 % (1804447)------------------------------ % 225.63/32.06 % (1804447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.63/32.06 % (1804447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.63/32.06 % (1804447)CaDiCaL version: 2.1.3 % 225.63/32.06 % (1804447)Termination reason: Inappropriate % 225.63/32.06 % (1804447)Time elapsed: 0.001 s % 225.63/32.06 % (1804447)Peak memory usage: 10 MB % 225.63/32.06 % (1804447)Instructions burned: 1 (million) % 225.63/32.06 % (1804447)------------------------------ % 225.63/32.06 % (1804447)------------------------------ % 225.63/32.06 % (1804449)% WARNING: option uhcvi not known. % 225.63/32.06 % (1804449)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2231644914:i=271062:add=off:rtra=on:rawr=on_2722 on theBenchmark for (2722ds/271062Mi) % 265.17/37.66 % (1804363)Instruction limit reached! % 265.17/37.66 % (1804363)------------------------------ % 265.17/37.66 % (1804363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.17/37.66 % (1804363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.17/37.66 % (1804363)CaDiCaL version: 2.1.3 % 265.17/37.66 % (1804363)Termination reason: Instruction limit % 265.17/37.66 % (1804363)Termination phase: Saturation % 265.17/37.66 % (1804363)Time elapsed: 19.458 s % 265.17/37.66 % (1804363)Peak memory usage: 56 MB % 265.17/37.66 % (1804363)Instructions burned: 20139 (million) % 265.17/37.66 % (1804452)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3239084008:i=176048:add=on:rtra=on:rawr=on_2715 on theBenchmark for (2715ds/176048Mi) % 265.17/37.66 % (1804412)Instruction limit reached! % 265.17/37.66 % (1804412)------------------------------ % 265.17/37.66 % (1804412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.17/37.66 % (1804412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.17/37.66 % (1804412)CaDiCaL version: 2.1.3 % 265.17/37.66 % (1804412)Termination reason: Instruction limit % 265.17/37.66 % (1804412)Termination phase: Saturation % 265.17/37.66 % (1804412)Time elapsed: 7.778 s % 265.17/37.66 % (1804412)Peak memory usage: 233 MB % 265.17/37.66 % (1804412)Instructions burned: 17631 (million) % 265.17/37.66 % (1804455)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2286413411:i=206:fgj=on:rtra=on_2711 on theBenchmark for (2711ds/206Mi) % 265.17/37.66 % (1804455)Instruction limit reached! % 265.17/37.66 % (1804455)------------------------------ % 265.17/37.66 % (1804455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.17/37.66 % (1804455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.17/37.66 % (1804455)CaDiCaL version: 2.1.3 % 265.17/37.66 % (1804455)Termination reason: Instruction limit % 265.17/37.66 % (1804455)Termination phase: Saturation % 265.17/37.66 % (1804455)Time elapsed: 0.112 s % 265.17/37.66 % (1804455)Peak memory usage: 14 MB % 265.17/37.66 % (1804455)Instructions burned: 207 (million) % 265.17/37.66 % (1804457)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=965892504:i=232:rtra=on_2710 on theBenchmark for (2710ds/232Mi) % 265.17/37.66 % (1804457)Instruction limit reached! % 265.17/37.66 % (1804457)------------------------------ % 265.17/37.66 % (1804457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.17/37.66 % (1804457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.17/37.66 % (1804457)CaDiCaL version: 2.1.3 % 265.17/37.66 % (1804457)Termination reason: Instruction limit % 265.17/37.66 % (1804457)Termination phase: Saturation % 265.17/37.66 % (1804457)Time elapsed: 0.151 s % 265.17/37.66 % (1804457)Peak memory usage: 13 MB % 265.17/37.66 % (1804457)Instructions burned: 232 (million) % 265.17/37.66 % (1804460)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3788415762:i=262:rtra=on_2708 on theBenchmark for (2708ds/262Mi) % 265.17/37.66 % (1804460)Instruction limit reached! % 265.17/37.66 % (1804460)------------------------------ % 265.17/37.66 % (1804460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.17/37.66 % (1804460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.17/37.66 % (1804460)CaDiCaL version: 2.1.3 % 265.17/37.66 % (1804460)Termination reason: Instruction limit % 265.17/37.66 % (1804460)Termination phase: Saturation % 265.17/37.66 % (1804460)Time elapsed: 0.140 s % 265.17/37.66 % (1804460)Peak memory usage: 14 MB % 265.17/37.66 % (1804460)Instructions burned: 263 (million) % 265.17/37.66 % (1804462)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2847107191:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2706 on theBenchmark for (2706ds/318Mi) % 265.17/37.66 % (1804462)Instruction limit reached! % 265.17/37.66 % (1804462)------------------------------ % 265.17/37.66 % (1804462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.17/37.66 % (1804462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.17/37.66 % (1804462)CaDiCaL version: 2.1.3 % 265.17/37.66 % (1804462)Termination reason: Instruction limit % 265.17/37.66 % (1804462)Termination phase: Saturation % 265.17/37.66 % (1804462)Time elapsed: 0.192 s % 265.17/37.66 % (1804462)Peak memory usage: 15 MB % 265.17/37.66 % (1804462)Instructions burned: 318 (million) % 265.17/37.66 % (1804464)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=715694815:i=1428:nm=2:rtra=on_2704 Terminated % 300.05/42.54 % Vampire exiting % 300.05/42.54 Terminated %------------------------------------------------------------------------------