%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW747_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n001.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:42 PM UTC 2026 % Result : Timeout 288.32s 41.03s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : SWW747_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.24/0.28 % Computer : n001.cluster.edu % 0.24/0.28 % Model : x86_64 x86_64 % 0.24/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.24/0.28 % Memory : 8046.5625MB % 0.24/0.28 % OS : Linux 6.8.0-71-generic % 0.24/0.28 % CPULimit : 300 % 0.24/0.28 % WCLimit : 300 % 0.24/0.28 % DateTime : Mon Sep 28 14:34:48 UTC 2026 % 0.24/0.28 % CPUTime : % 0.24/0.28 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.24/0.31 Running first-order model finding % 0.24/0.31 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 6.09/1.22 % (388887)Will run a generic schedule for satisfiability detection. % 6.09/1.22 % (388892)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=141214487_2999 on theBenchmark for (2999ds/0Mi) % 6.09/1.22 % (388893)% WARNING: option uhcvi not known. % 6.09/1.22 % (388894)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2013851961:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.09/1.22 % (388895)dis+10_1_sil=32000:sp=arity:random_seed=2281130378:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.09/1.22 % (388896)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=759021772:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.09/1.22 % (388898)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1498982533:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.09/1.22 % (388893)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3190089351:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.09/1.22 % (388897)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3319120998:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.09/1.22 % (388895)Instruction limit reached! % 6.09/1.22 % (388895)------------------------------ % 6.09/1.22 % (388895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.09/1.22 % (388895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.09/1.22 % (388895)CaDiCaL version: 2.1.3 % 6.09/1.22 % (388895)Termination reason: Instruction limit % 6.09/1.22 % (388895)Termination phase: Saturation % 6.09/1.22 % (388895)Time elapsed: 0.089 s % 6.09/1.22 % (388895)Peak memory usage: 14 MB % 6.09/1.22 % (388895)Instructions burned: 103 (million) % 6.09/1.22 % (388896)Instruction limit reached! % 6.09/1.22 % (388896)------------------------------ % 6.09/1.22 % (388896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.09/1.22 % (388896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.09/1.22 % (388896)CaDiCaL version: 2.1.3 % 6.09/1.22 % (388896)Termination reason: Instruction limit % 6.09/1.22 % (388896)Termination phase: Blocked clause elimination % 6.09/1.22 % (388896)Time elapsed: 0.097 s % 6.09/1.22 % (388896)Peak memory usage: 13 MB % 6.09/1.22 % (388896)Instructions burned: 116 (million) % 6.09/1.22 % (388897)Instruction limit reached! % 6.09/1.22 % (388897)------------------------------ % 6.09/1.22 % (388897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.09/1.22 % (388897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.09/1.22 % (388897)CaDiCaL version: 2.1.3 % 6.09/1.22 % (388897)Termination reason: Instruction limit % 6.09/1.22 % (388897)Termination phase: Saturation % 6.09/1.22 % (388897)Time elapsed: 0.120 s % 6.09/1.22 % (388897)Peak memory usage: 16 MB % 6.09/1.22 % (388897)Instructions burned: 131 (million) % 6.09/1.22 % (388892)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.09/1.22 % (388892)Terminated due to inappropriate strategy. % 6.09/1.22 % (388892)------------------------------ % 6.09/1.22 % (388892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.09/1.22 % (388892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.09/1.22 % (388892)CaDiCaL version: 2.1.3 % 6.09/1.22 % (388892)Termination reason: Inappropriate % 6.09/1.22 % (388892)Time elapsed: 0.134 s % 6.09/1.22 % (388892)Peak memory usage: 14 MB % 6.09/1.22 % (388892)Instructions burned: 297 (million) % 6.09/1.22 % (388892)------------------------------ % 6.09/1.22 % (388892)------------------------------ % 6.09/1.22 % (388906)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1840857773:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 6.09/1.22 % (388907)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3764552068:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 6.09/1.22 % (388898)Instruction limit reached! % 6.09/1.22 % (388898)------------------------------ % 6.09/1.22 % (388898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.09/1.22 % (388898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.09/1.22 % (388898)CaDiCaL version: 2.1.3 % 6.09/1.22 % (388898)Termination reason: Instruction limit % 6.09/1.22 % (388898)Termination phase: Saturation % 6.09/1.22 % (388898)Time elapsed: 0.143 s % 6.09/1.22 % (388898)Peak memory usage: 17 MB % 6.09/1.22 % (388898)Instructions burned: 160 (million) % 6.09/1.22 % (388908)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=3439204086:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 9.11/1.99 % (388909)ott-21_1_sil=16000:fs=off:random_seed=247493151:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 9.11/1.99 % (388912)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4178796572:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 9.11/1.99 % (388907)Instruction limit reached! % 9.11/1.99 % (388907)------------------------------ % 9.11/1.99 % (388907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.11/1.99 % (388907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.11/1.99 % (388907)CaDiCaL version: 2.1.3 % 9.11/1.99 % (388907)Termination reason: Instruction limit % 9.11/1.99 % (388907)Termination phase: Blocked clause elimination % 9.11/1.99 % (388907)Time elapsed: 0.060 s % 9.11/1.99 % (388907)Peak memory usage: 13 MB % 9.11/1.99 % (388907)Instructions burned: 131 (million) % 9.11/1.99 % (388906)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 9.11/1.99 % (388906)Terminated due to inappropriate strategy. % 9.11/1.99 % (388906)------------------------------ % 9.11/1.99 % (388906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.11/1.99 % (388906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.11/1.99 % (388906)CaDiCaL version: 2.1.3 % 9.11/1.99 % (388906)Termination reason: Inappropriate % 9.11/1.99 % (388906)Time elapsed: 0.066 s % 9.11/1.99 % (388906)Peak memory usage: 13 MB % 9.11/1.99 % (388906)Instructions burned: 77 (million) % 9.11/1.99 % (388906)------------------------------ % 9.11/1.99 % (388906)------------------------------ % 9.11/1.99 % (388916)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1766308968:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 9.11/1.99 % (388917)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2667336458:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 9.11/1.99 % (388916)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 9.11/1.99 % (388916)Terminated due to inappropriate strategy. % 9.11/1.99 % (388916)------------------------------ % 9.11/1.99 % (388916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.11/1.99 % (388916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.11/1.99 % (388916)CaDiCaL version: 2.1.3 % 9.11/1.99 % (388916)Termination reason: Inappropriate % 9.11/1.99 % (388916)Time elapsed: 0.050 s % 9.11/1.99 % (388916)Peak memory usage: 14 MB % 9.11/1.99 % (388916)Instructions burned: 103 (million) % 9.11/1.99 % (388916)------------------------------ % 9.11/1.99 % (388916)------------------------------ % 9.11/1.99 % (388920)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1907722414:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi) % 9.11/1.99 % (388920)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 9.11/1.99 % (388920)Terminated due to inappropriate strategy. % 9.11/1.99 % (388920)------------------------------ % 9.11/1.99 % (388920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.11/1.99 % (388920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.11/1.99 % (388920)CaDiCaL version: 2.1.3 % 9.11/1.99 % (388920)Termination reason: Inappropriate % 9.11/1.99 % (388920)Time elapsed: 0.039 s % 9.11/1.99 % (388920)Peak memory usage: 12 MB % 9.11/1.99 % (388920)Instructions burned: 85 (million) % 9.11/1.99 % (388909)Instruction limit reached! % 9.11/1.99 % (388909)------------------------------ % 9.11/1.99 % (388909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.11/1.99 % (388909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.11/1.99 % (388909)CaDiCaL version: 2.1.3 % 9.11/1.99 % (388909)Termination reason: Instruction limit % 9.11/1.99 % (388909)Termination phase: Saturation % 9.11/1.99 % (388909)Time elapsed: 0.161 s % 9.11/1.99 % (388909)Peak memory usage: 14 MB % 9.11/1.99 % (388909)Instructions burned: 180 (million) % 9.11/1.99 % (388920)------------------------------ % 9.11/1.99 % (388920)------------------------------ % 9.11/1.99 % (388923)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1216484280:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 9.11/1.99 % (388922)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=1537484509:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi) % 33.35/5.08 % (388912)Instruction limit reached! % 33.35/5.08 % (388912)------------------------------ % 33.35/5.08 % (388912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.35/5.08 % (388912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.35/5.08 % (388912)CaDiCaL version: 2.1.3 % 33.35/5.08 % (388912)Termination reason: Instruction limit % 33.35/5.08 % (388912)Termination phase: Saturation % 33.35/5.08 % (388912)Time elapsed: 0.428 s % 33.35/5.08 % (388912)Peak memory usage: 17 MB % 33.35/5.08 % (388912)Instructions burned: 477 (million) % 33.35/5.08 % (388926)fmb+10_1_sil=64000:random_seed=1123038750:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 33.35/5.08 % (388923)Instruction limit reached! % 33.35/5.08 % (388923)------------------------------ % 33.35/5.08 % (388923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.35/5.08 % (388923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.35/5.08 % (388923)CaDiCaL version: 2.1.3 % 33.35/5.08 % (388923)Termination reason: Instruction limit % 33.35/5.08 % (388923)Termination phase: Saturation % 33.35/5.08 % (388923)Time elapsed: 0.344 s % 33.35/5.08 % (388923)Peak memory usage: 20 MB % 33.35/5.08 % (388923)Instructions burned: 880 (million) % 33.35/5.08 % (388928)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=138826390:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 33.35/5.08 % (388926)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 33.35/5.08 % (388926)Terminated due to inappropriate strategy. % 33.35/5.08 % (388926)------------------------------ % 33.35/5.08 % (388926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.35/5.08 % (388926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.35/5.08 % (388926)CaDiCaL version: 2.1.3 % 33.35/5.08 % (388926)Termination reason: Inappropriate % 33.35/5.08 % (388926)Time elapsed: 0.072 s % 33.35/5.08 % (388926)Peak memory usage: 12 MB % 33.35/5.08 % (388926)Instructions burned: 83 (million) % 33.35/5.08 % (388926)------------------------------ % 33.35/5.08 % (388926)------------------------------ % 33.35/5.08 % (388928)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 33.35/5.08 % (388928)Terminated due to inappropriate strategy. % 33.35/5.08 % (388928)------------------------------ % 33.35/5.08 % (388928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.35/5.08 % (388928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.35/5.08 % (388928)CaDiCaL version: 2.1.3 % 33.35/5.08 % (388928)Termination reason: Inappropriate % 33.35/5.08 % (388928)Time elapsed: 0.036 s % 33.35/5.08 % (388928)Peak memory usage: 12 MB % 33.35/5.08 % (388928)Instructions burned: 79 (million) % 33.35/5.08 % (388928)------------------------------ % 33.35/5.08 % (388928)------------------------------ % 33.35/5.08 % (388908)Instruction limit reached! % 33.35/5.08 % (388908)------------------------------ % 33.35/5.08 % (388908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.35/5.08 % (388908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.35/5.08 % (388908)CaDiCaL version: 2.1.3 % 33.35/5.08 % (388908)Termination reason: Instruction limit % 33.35/5.08 % (388908)Termination phase: Saturation % 33.35/5.08 % (388908)Time elapsed: 0.602 s % 33.35/5.08 % (388908)Peak memory usage: 26 MB % 33.35/5.08 % (388908)Instructions burned: 687 (million) % 33.35/5.08 % (388930)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=587701033:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 33.35/5.08 % (388931)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=990201111:i=5131_2991 on theBenchmark for (2991ds/5131Mi) % 33.35/5.08 % (388932)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1048026414:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 33.35/5.08 % (388930)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 33.35/5.08 % (388930)Terminated due to inappropriate strategy. % 33.35/5.08 % (388930)------------------------------ % 33.35/5.08 % (388930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.35/5.08 % (388930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.51/6.21 % (388930)CaDiCaL version: 2.1.3 % 41.51/6.21 % (388930)Termination reason: Inappropriate % 41.51/6.21 % (388930)Time elapsed: 0.070 s % 41.51/6.21 % (388930)Peak memory usage: 12 MB % 41.51/6.21 % (388930)Instructions burned: 84 (million) % 41.51/6.21 % (388930)------------------------------ % 41.51/6.21 % (388930)------------------------------ % 41.51/6.21 % (388936)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4239493614:i=6324_2990 on theBenchmark for (2990ds/6324Mi) % 41.51/6.21 % (388922)Instruction limit reached! % 41.51/6.21 % (388922)------------------------------ % 41.51/6.21 % (388922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.51/6.21 % (388922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.51/6.21 % (388922)CaDiCaL version: 2.1.3 % 41.51/6.21 % (388922)Termination reason: Instruction limit % 41.51/6.21 % (388922)Termination phase: Saturation % 41.51/6.21 % (388922)Time elapsed: 0.601 s % 41.51/6.21 % (388922)Peak memory usage: 23 MB % 41.51/6.21 % (388922)Instructions burned: 693 (million) % 41.51/6.21 % (388938)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2716957389:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 41.51/6.21 % (388936)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.51/6.21 % (388936)Terminated due to inappropriate strategy. % 41.51/6.21 % (388936)------------------------------ % 41.51/6.21 % (388936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.51/6.21 % (388936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.51/6.21 % (388936)CaDiCaL version: 2.1.3 % 41.51/6.21 % (388936)Termination reason: Inappropriate % 41.51/6.21 % (388936)Time elapsed: 0.149 s % 41.51/6.21 % (388936)Peak memory usage: 14 MB % 41.51/6.21 % (388936)Instructions burned: 294 (million) % 41.51/6.21 % (388936)------------------------------ % 41.51/6.21 % (388936)------------------------------ % 41.51/6.21 % (388941)ott-2_1_sil=16000:newcnf=on:random_seed=2890368337:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 41.51/6.21 % (388938)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.51/6.21 % (388938)Terminated due to inappropriate strategy. % 41.51/6.21 % (388938)------------------------------ % 41.51/6.21 % (388938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.51/6.21 % (388938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.51/6.21 % (388938)CaDiCaL version: 2.1.3 % 41.51/6.21 % (388938)Termination reason: Inappropriate % 41.51/6.21 % (388938)Time elapsed: 0.067 s % 41.51/6.21 % (388938)Peak memory usage: 12 MB % 41.51/6.21 % (388938)Instructions burned: 84 (million) % 41.51/6.21 % (388938)------------------------------ % 41.51/6.21 % (388938)------------------------------ % 41.51/6.21 % (388944)ott+10_1_sil=32000:tgt=ground:random_seed=4216661166:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi) % 41.51/6.21 % (388917)Instruction limit reached! % 41.51/6.21 % (388917)------------------------------ % 41.51/6.21 % (388917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.51/6.21 % (388917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.51/6.21 % (388917)CaDiCaL version: 2.1.3 % 41.51/6.21 % (388917)Termination reason: Instruction limit % 41.51/6.21 % (388917)Termination phase: Saturation % 41.51/6.21 % (388917)Time elapsed: 1.139 s % 41.51/6.21 % (388917)Peak memory usage: 25 MB % 41.51/6.21 % (388917)Instructions burned: 1180 (million) % 41.51/6.21 % (388949)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4072829256:i=54282_2985 on theBenchmark for (2985ds/54282Mi) % 41.51/6.21 % (388941)Instruction limit reached! % 41.51/6.21 % (388941)------------------------------ % 41.51/6.21 % (388941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.51/6.21 % (388941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.51/6.21 % (388941)CaDiCaL version: 2.1.3 % 41.51/6.21 % (388941)Termination reason: Instruction limit % 41.51/6.21 % (388941)Termination phase: Saturation % 41.51/6.21 % (388941)Time elapsed: 0.445 s % 41.51/6.21 % (388941)Peak memory usage: 24 MB % 41.51/6.21 % (388941)Instructions burned: 870 (million) % 41.51/6.21 % (388953)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2132846945:i=3512:aac=none_2984 on theBenchmark for (2984ds/3512Mi) % 41.51/6.21 % (388949)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.51/6.21 % (388949)Terminated due to inappropriate strategy. % 158.36/22.70 % (388949)------------------------------ % 158.36/22.70 % (388949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.36/22.70 % (388949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.36/22.70 % (388949)CaDiCaL version: 2.1.3 % 158.36/22.70 % (388949)Termination reason: Inappropriate % 158.36/22.70 % (388949)Time elapsed: 0.191 s % 158.36/22.70 % (388949)Peak memory usage: 14 MB % 158.36/22.70 % (388949)Instructions burned: 296 (million) % 158.36/22.70 % (388949)------------------------------ % 158.36/22.70 % (388949)------------------------------ % 158.36/22.70 % (388955)dis+21_1_sil=32000:sas=cadical:random_seed=4032412850:i=3773:amm=off_2983 on theBenchmark for (2983ds/3773Mi) % 158.36/22.70 % (388932)Instruction limit reached! % 158.36/22.70 % (388932)------------------------------ % 158.36/22.70 % (388932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.36/22.70 % (388932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.36/22.70 % (388932)CaDiCaL version: 2.1.3 % 158.36/22.70 % (388932)Termination reason: Instruction limit % 158.36/22.70 % (388932)Termination phase: Saturation % 158.36/22.70 % (388932)Time elapsed: 1.381 s % 158.36/22.70 % (388932)Peak memory usage: 31 MB % 158.36/22.70 % (388932)Instructions burned: 1472 (million) % 158.36/22.70 % (388962)ott+11_1_sil=16000:gs=on:random_seed=6847300:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2977 on theBenchmark for (2977ds/2251Mi) % 158.36/22.70 % (388955)Instruction limit reached! % 158.36/22.70 % (388955)------------------------------ % 158.36/22.70 % (388955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.36/22.70 % (388955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.36/22.70 % (388955)CaDiCaL version: 2.1.3 % 158.36/22.70 % (388955)Termination reason: Instruction limit % 158.36/22.70 % (388955)Termination phase: Saturation % 158.36/22.70 % (388955)Time elapsed: 1.651 s % 158.36/22.70 % (388955)Peak memory usage: 52 MB % 158.36/22.70 % (388955)Instructions burned: 3774 (million) % 158.36/22.70 % (388966)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=958343153:fmbsr=1.6:i=67534_2966 on theBenchmark for (2966ds/67534Mi) % 158.36/22.70 % (388966)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.36/22.70 % (388966)Terminated due to inappropriate strategy. % 158.36/22.70 % (388966)------------------------------ % 158.36/22.70 % (388966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.36/22.70 % (388966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.36/22.70 % (388966)CaDiCaL version: 2.1.3 % 158.36/22.70 % (388966)Termination reason: Inappropriate % 158.36/22.70 % (388966)Time elapsed: 0.079 s % 158.36/22.70 % (388966)Peak memory usage: 12 MB % 158.36/22.70 % (388966)Instructions burned: 84 (million) % 158.36/22.70 % (388966)------------------------------ % 158.36/22.70 % (388966)------------------------------ % 158.36/22.70 % (388968)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2898619586:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2965 on theBenchmark for (2965ds/4591Mi) % 158.36/22.70 % (388962)Instruction limit reached! % 158.36/22.70 % (388962)------------------------------ % 158.36/22.70 % (388962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.36/22.70 % (388962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.36/22.70 % (388962)CaDiCaL version: 2.1.3 % 158.36/22.70 % (388962)Termination reason: Instruction limit % 158.36/22.70 % (388962)Termination phase: Saturation % 158.36/22.70 % (388962)Time elapsed: 2.172 s % 158.36/22.70 % (388962)Peak memory usage: 32 MB % 158.36/22.70 % (388962)Instructions burned: 2251 (million) % 158.36/22.70 % (388970)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4169952633:i=29340_2955 on theBenchmark for (2955ds/29340Mi) % 158.36/22.70 % (388953)Instruction limit reached! % 158.36/22.70 % (388953)------------------------------ % 158.36/22.70 % (388953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.36/22.70 % (388953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.36/22.70 % (388953)CaDiCaL version: 2.1.3 % 158.36/22.70 % (388953)Termination reason: Instruction limit % 158.36/22.70 % (388953)Termination phase: Saturation % 158.36/22.70 % (388953)Time elapsed: 3.107 s % 158.36/22.70 % (388953)Peak memory usage: 35 MB % 158.36/22.70 % (388953)Instructions burned: 3512 (million) % 158.36/22.70 % (388972)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1426325100:i=5211_2952 on theBenchmark for (2952ds/5211Mi) % 209.77/31.93 % (388931)Instruction limit reached! % 209.77/31.93 % (388931)------------------------------ % 209.77/31.93 % (388931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.77/31.93 % (388931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.77/31.93 % (388931)CaDiCaL version: 2.1.3 % 209.77/31.93 % (388931)Termination reason: Instruction limit % 209.77/31.93 % (388931)Termination phase: Saturation % 209.77/31.93 % (388931)Time elapsed: 4.577 s % 209.77/31.93 % (388931)Peak memory usage: 50 MB % 209.77/31.93 % (388931)Instructions burned: 5131 (million) % 209.77/31.93 % (388976)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2234760643:i=5497:nm=2_2945 on theBenchmark for (2945ds/5497Mi) % 209.77/31.93 % (388976)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 209.77/31.93 % (388976)Terminated due to inappropriate strategy. % 209.77/31.93 % (388976)------------------------------ % 209.77/31.93 % (388976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.77/31.93 % (388976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.77/31.93 % (388976)CaDiCaL version: 2.1.3 % 209.77/31.93 % (388976)Termination reason: Inappropriate % 209.77/31.93 % (388976)Time elapsed: 0.153 s % 209.77/31.93 % (388976)Peak memory usage: 14 MB % 209.77/31.93 % (388976)Instructions burned: 180 (million) % 209.77/31.93 % (388976)------------------------------ % 209.77/31.93 % (388976)------------------------------ % 209.77/31.93 % (388978)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4285595119:fmbsr=2:i=46332_2943 on theBenchmark for (2943ds/46332Mi) % 209.77/31.93 % (388978)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 209.77/31.93 % (388978)Terminated due to inappropriate strategy. % 209.77/31.93 % (388978)------------------------------ % 209.77/31.93 % (388978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.77/31.93 % (388978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.77/31.93 % (388978)CaDiCaL version: 2.1.3 % 209.77/31.93 % (388978)Termination reason: Inappropriate % 209.77/31.93 % (388978)Time elapsed: 0.057 s % 209.77/31.93 % (388978)Peak memory usage: 12 MB % 209.77/31.93 % (388978)Instructions burned: 84 (million) % 209.77/31.93 % (388978)------------------------------ % 209.77/31.93 % (388978)------------------------------ % 209.77/31.93 % (388944)Instruction limit reached! % 209.77/31.93 % (388944)------------------------------ % 209.77/31.93 % (388944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.77/31.93 % (388944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.77/31.93 % (388944)CaDiCaL version: 2.1.3 % 209.77/31.93 % (388944)Termination reason: Instruction limit % 209.77/31.93 % (388944)Termination phase: Saturation % 209.77/31.93 % (388944)Time elapsed: 4.599 s % 209.77/31.93 % (388944)Peak memory usage: 36 MB % 209.77/31.93 % (388944)Instructions burned: 5114 (million) % 209.77/31.93 % (388980)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3381254473:i=14071_2942 on theBenchmark for (2942ds/14071Mi) % 209.77/31.93 % (388982)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1407909185:i=22565:add=on:rawr=on_2942 on theBenchmark for (2942ds/22565Mi) % 209.77/31.93 % (388980)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 209.77/31.93 % (388980)Terminated due to inappropriate strategy. % 209.77/31.93 % (388980)------------------------------ % 209.77/31.93 % (388980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.77/31.93 % (388980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.77/31.93 % (388980)CaDiCaL version: 2.1.3 % 209.77/31.93 % (388980)Termination reason: Inappropriate % 209.77/31.93 % (388980)Time elapsed: 0.080 s % 209.77/31.93 % (388980)Peak memory usage: 12 MB % 209.77/31.93 % (388980)Instructions burned: 84 (million) % 209.77/31.93 % (388980)------------------------------ % 209.77/31.93 % (388980)------------------------------ % 209.77/31.93 % (388968)Instruction limit reached! % 209.77/31.93 % (388968)------------------------------ % 209.77/31.93 % (388968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.77/31.93 % (388968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.77/31.93 % (388968)CaDiCaL version: 2.1.3 % 209.77/31.93 % (388968)Termination reason: Instruction limit % 209.77/31.93 % (388968)Termination phase: Saturation % 209.77/31.93 % (388968)Time elapsed: 2.349 s % 209.77/31.93 % (388968)Peak memory usage: 48 MB % 209.77/31.93 % (388968)Instructions burned: 4592 (million) % 227.06/32.31 % (388984)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=904895425:i=8173:av=off_2941 on theBenchmark for (2941ds/8173Mi) % 227.06/32.31 % (388985)dis+10_16:1_sil=16000:random_seed=911992906:i=9155:fsr=off_2941 on theBenchmark for (2941ds/9155Mi) % 227.06/32.31 % (388972)Instruction limit reached! % 227.06/32.31 % (388972)------------------------------ % 227.06/32.31 % (388972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.06/32.31 % (388972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.06/32.31 % (388972)CaDiCaL version: 2.1.3 % 227.06/32.31 % (388972)Termination reason: Instruction limit % 227.06/32.31 % (388972)Termination phase: Saturation % 227.06/32.31 % (388972)Time elapsed: 3.840 s % 227.06/32.31 % (388972)Peak memory usage: 55 MB % 227.06/32.31 % (388972)Instructions burned: 5211 (million) % 227.06/32.31 % (388992)ott-3_8_sil=64000:random_seed=1178930670:i=20139:bs=on_2913 on theBenchmark for (2913ds/20139Mi) % 227.06/32.31 % (388985)Instruction limit reached! % 227.06/32.31 % (388985)------------------------------ % 227.06/32.31 % (388985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.06/32.31 % (388985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.06/32.31 % (388985)CaDiCaL version: 2.1.3 % 227.06/32.31 % (388985)Termination reason: Instruction limit % 227.06/32.31 % (388985)Termination phase: Saturation % 227.06/32.31 % (388985)Time elapsed: 4.449 s % 227.06/32.31 % (388985)Peak memory usage: 62 MB % 227.06/32.31 % (388985)Instructions burned: 9157 (million) % 227.06/32.31 % (388996)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4230914523:fmbsr=2:i=32576_2896 on theBenchmark for (2896ds/32576Mi) % 227.06/32.31 % (388996)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.06/32.31 % (388996)Terminated due to inappropriate strategy. % 227.06/32.31 % (388996)------------------------------ % 227.06/32.31 % (388996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.06/32.31 % (388996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.06/32.31 % (388996)CaDiCaL version: 2.1.3 % 227.06/32.31 % (388996)Termination reason: Inappropriate % 227.06/32.31 % (388996)Time elapsed: 0.129 s % 227.06/32.31 % (388996)Peak memory usage: 14 MB % 227.06/32.31 % (388996)Instructions burned: 294 (million) % 227.06/32.31 % (388996)------------------------------ % 227.06/32.31 % (388996)------------------------------ % 227.06/32.31 % (388998)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3982981236:i=11404_2894 on theBenchmark for (2894ds/11404Mi) % 227.06/32.31 % (388984)Instruction limit reached! % 227.06/32.31 % (388984)------------------------------ % 227.06/32.31 % (388984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.06/32.31 % (388984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.06/32.31 % (388984)CaDiCaL version: 2.1.3 % 227.06/32.31 % (388984)Termination reason: Instruction limit % 227.06/32.31 % (388984)Termination phase: Saturation % 227.06/32.31 % (388984)Time elapsed: 8.177 s % 227.06/32.31 % (388984)Peak memory usage: 50 MB % 227.06/32.31 % (388984)Instructions burned: 8173 (million) % 227.06/32.31 % (389004)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3001172881:i=14134_2859 on theBenchmark for (2859ds/14134Mi) % 227.06/32.31 % (388998)Instruction limit reached! % 227.06/32.31 % (388998)------------------------------ % 227.06/32.31 % (388998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.06/32.31 % (388998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.06/32.31 % (388998)CaDiCaL version: 2.1.3 % 227.06/32.31 % (388998)Termination reason: Instruction limit % 227.06/32.31 % (388998)Termination phase: Saturation % 227.06/32.31 % (388998)Time elapsed: 6.532 s % 227.06/32.31 % (388998)Peak memory usage: 54 MB % 227.06/32.31 % (388998)Instructions burned: 11405 (million) % 227.06/32.31 % (389008)dis+33_16_sil=32000:sac=on:random_seed=2142773228:i=15851:nm=0_2829 on theBenchmark for (2829ds/15851Mi) % 227.06/32.31 % (388982)Instruction limit reached! % 227.06/32.31 % (388982)------------------------------ % 227.06/32.31 % (388982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.06/32.31 % (388982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.06/32.31 % (388982)CaDiCaL version: 2.1.3 % 227.06/32.31 % (388982)Termination reason: Instruction limit % 227.06/32.31 % (388982)Termination phase: Saturation % 227.06/32.31 % (388982)Time elapsed: 16.509 s % 227.06/32.31 % (388982)Peak memory usage: 95 MB % 227.06/32.31 % (388982)Instructions burned: 22565 (million) % 227.06/32.31 % (389020)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3379374715:avsq=on:i=17627:add=on:amm=off_2776 on theBenchmark for (2776ds/17627Mi) % 252.12/35.84 % (388992)Instruction limit reached! % 252.12/35.84 % (388992)------------------------------ % 252.12/35.84 % (388992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.12/35.84 % (388992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.12/35.84 % (388992)CaDiCaL version: 2.1.3 % 252.12/35.84 % (388992)Termination reason: Instruction limit % 252.12/35.84 % (388992)Termination phase: Saturation % 252.12/35.84 % (388992)Time elapsed: 19.718 s % 252.12/35.84 % (388992)Peak memory usage: 59 MB % 252.12/35.84 % (388992)Instructions burned: 20139 (million) % 252.12/35.84 % (389028)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3998002592:s2a=on:i=53295_2716 on theBenchmark for (2716ds/53295Mi) % 252.12/35.84 % (389004)Instruction limit reached! % 252.12/35.84 % (389004)------------------------------ % 252.12/35.84 % (389004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.12/35.84 % (389004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.12/35.84 % (389004)CaDiCaL version: 2.1.3 % 252.12/35.84 % (389004)Termination reason: Instruction limit % 252.12/35.84 % (389004)Termination phase: Saturation % 252.12/35.84 % (389004)Time elapsed: 14.569 s % 252.12/35.84 % (389004)Peak memory usage: 62 MB % 252.12/35.84 % (389004)Instructions burned: 14134 (million) % 252.12/35.84 % (389031)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=656067158:i=26857:ins=20_2712 on theBenchmark for (2712ds/26857Mi) % 252.12/35.84 % (389031)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.12/35.84 % (389031)Terminated due to inappropriate strategy. % 252.12/35.84 % (389031)------------------------------ % 252.12/35.84 % (389031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.12/35.84 % (389031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.12/35.84 % (389031)CaDiCaL version: 2.1.3 % 252.12/35.84 % (389031)Termination reason: Inappropriate % 252.12/35.84 % (389031)Time elapsed: 0.060 s % 252.12/35.84 % (389031)Peak memory usage: 12 MB % 252.12/35.84 % (389031)Instructions burned: 84 (million) % 252.12/35.84 % (389031)------------------------------ % 252.12/35.84 % (389031)------------------------------ % 252.12/35.84 % (389033)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2425088820:i=28120:bs=on:fsr=off_2711 on theBenchmark for (2711ds/28120Mi) % 252.12/35.84 % (389008)Instruction limit reached! % 252.12/35.84 % (389008)------------------------------ % 252.12/35.84 % (389008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.12/35.84 % (389008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.12/35.84 % (389008)CaDiCaL version: 2.1.3 % 252.12/35.84 % (389008)Termination reason: Instruction limit % 252.12/35.84 % (389008)Termination phase: Clausification % 252.12/35.84 % (389008)Time elapsed: 14.132 s % 252.12/35.84 % (389008)Peak memory usage: 8620 MB % 252.12/35.84 % (389008)Instructions burned: 15851 (million) % 252.12/35.84 % (388970)Instruction limit reached! % 252.12/35.84 % (388970)------------------------------ % 252.12/35.84 % (388970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.12/35.84 % (388970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.12/35.84 % (388970)CaDiCaL version: 2.1.3 % 252.12/35.84 % (388970)Termination reason: Instruction limit % 252.12/35.84 % (388970)Termination phase: Saturation % 252.12/35.84 % (388970)Time elapsed: 27.020 s % 252.12/35.84 % (388970)Peak memory usage: 97 MB % 252.12/35.84 % (388970)Instructions burned: 29341 (million) % 252.12/35.84 % (389086)fmb+10_1_sil=256000:fmbss=7:random_seed=4091289640:fmbsr=1.6:i=182295_2684 on theBenchmark for (2684ds/182295Mi) % 252.12/35.84 % (389086)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.12/35.84 % (389086)Terminated due to inappropriate strategy. % 252.12/35.84 % (389086)------------------------------ % 252.12/35.84 % (389086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.12/35.84 % (389086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.12/35.84 % (389086)CaDiCaL version: 2.1.3 % 252.12/35.84 % (389086)Termination reason: Inappropriate % 252.12/35.84 % (389086)Time elapsed: 0.036 s % 252.12/35.84 % (389086)Peak memory usage: 12 MB % 252.12/35.84 % (389086)Instructions burned: 84 (million) % 252.12/35.84 % (389086)------------------------------ % 252.12/35.84 % (389086)------------------------------ % 252.12/35.84 % (389109)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1420439250:i=44625:gsp=on_2684 on theBenchmark for (2684ds/44625Mi) % 275.06/39.07 % (389109)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 275.06/39.07 % (389109)Terminated due to inappropriate strategy. % 275.06/39.07 % (389109)------------------------------ % 275.06/39.07 % (389109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.06/39.07 % (389109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.06/39.07 % (389109)CaDiCaL version: 2.1.3 % 275.06/39.07 % (389109)Termination reason: Inappropriate % 275.06/39.07 % (389109)Time elapsed: 0.053 s % 275.06/39.07 % (389109)Peak memory usage: 13 MB % 275.06/39.07 % (389109)Instructions burned: 126 (million) % 275.06/39.07 % (389109)------------------------------ % 275.06/39.07 % (389109)------------------------------ % 275.06/39.07 % (389132)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1395618372:i=160505_2683 on theBenchmark for (2683ds/160505Mi) % 275.06/39.07 % (389132)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 275.06/39.07 % (389132)Terminated due to inappropriate strategy. % 275.06/39.07 % (389132)------------------------------ % 275.06/39.07 % (389132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.06/39.07 % (389132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.06/39.07 % (389132)CaDiCaL version: 2.1.3 % 275.06/39.07 % (389132)Termination reason: Inappropriate % 275.06/39.07 % (389132)Time elapsed: 0.037 s % 275.06/39.07 % (389132)Peak memory usage: 12 MB % 275.06/39.07 % (389132)Instructions burned: 84 (million) % 275.06/39.07 % (389132)------------------------------ % 275.06/39.07 % (389132)------------------------------ % 275.06/39.07 % (389143)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4204519722:fmbsr=1.3:i=225729_2682 on theBenchmark for (2682ds/225729Mi) % 275.06/39.07 % (389143)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 275.06/39.07 % (389143)Terminated due to inappropriate strategy. % 275.06/39.07 % (389143)------------------------------ % 275.06/39.07 % (389143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.06/39.07 % (389143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.06/39.07 % (389143)CaDiCaL version: 2.1.3 % 275.06/39.07 % (389143)Termination reason: Inappropriate % 275.06/39.07 % (389143)Time elapsed: 0.036 s % 275.06/39.07 % (389143)Peak memory usage: 12 MB % 275.06/39.07 % (389143)Instructions burned: 84 (million) % 275.06/39.07 % (389143)------------------------------ % 275.06/39.07 % (389143)------------------------------ % 275.06/39.07 % (389145)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1059148437:fmbsr=2:i=185024:ins=7_2682 on theBenchmark for (2682ds/185024Mi) % 275.06/39.07 % (389145)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 275.06/39.07 % (389145)Terminated due to inappropriate strategy. % 275.06/39.07 % (389145)------------------------------ % 275.06/39.07 % (389145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.06/39.07 % (389145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.06/39.07 % (389145)CaDiCaL version: 2.1.3 % 275.06/39.07 % (389145)Termination reason: Inappropriate % 275.06/39.07 % (389145)Time elapsed: 0.037 s % 275.06/39.07 % (389145)Peak memory usage: 12 MB % 275.06/39.07 % (389145)Instructions burned: 84 (million) % 275.06/39.07 % (389145)------------------------------ % 275.06/39.07 % (389145)------------------------------ % 275.06/39.07 % (389147)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1307451837:rtra=on_2681 on theBenchmark for (2681ds/0Mi) % 275.06/39.07 % (389149)% WARNING: option uhcvi not known. % 275.06/39.07 % (389149)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3951968761:i=271062:add=off:rtra=on:rawr=on_2681 on theBenchmark for (2681ds/271062Mi) % 275.06/39.07 % (389147)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 275.06/39.07 % (389147)Terminated due to inappropriate strategy. % 275.06/39.07 % (389147)------------------------------ % 275.06/39.07 % (389147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.06/39.07 % (389147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.06/39.07 % (389147)CaDiCaL version: 2.1.3 % 275.06/39.07 % (389147)Termination reason: Inappropriate % 275.06/39.07 % (389147)Time elapsed: 0.122 s % 275.06/39.07 % (389147)Peak memory usage: 14 MB % 275.06/39.07 % (389147)Instructions burned: 251 (million) % 275.06/39.07 % (389147)------------------------------ % 288.32/41.03 % (389147)------------------------------ % 288.32/41.03 % (389151)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=333979650:i=176048:add=on:rtra=on:rawr=on_2680 on theBenchmark for (2680ds/176048Mi) % 288.32/41.03 % (389020)Instruction limit reached! % 288.32/41.03 % (389020)------------------------------ % 288.32/41.03 % (389020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 288.32/41.03 % (389020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.32/41.03 % (389020)CaDiCaL version: 2.1.3 % 288.32/41.03 % (389020)Termination reason: Instruction limit % 288.32/41.03 % (389020)Termination phase: Saturation % 288.32/41.03 % (389020)Time elapsed: 12.443 s % 288.32/41.03 % (389020)Peak memory usage: 265 MB % 288.32/41.03 % (389020)Instructions burned: 17628 (million) % 288.32/41.03 % (389204)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2868427251:i=206:fgj=on:rtra=on_2651 on theBenchmark for (2651ds/206Mi) % 288.32/41.03 % (389204)Instruction limit reached! % 288.32/41.03 % (389204)------------------------------ % 288.32/41.03 % (389204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 288.32/41.03 % (389204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.32/41.03 % (389204)CaDiCaL version: 2.1.3 % 288.32/41.03 % (389204)Termination reason: Instruction limit % 288.32/41.03 % (389204)Termination phase: Saturation % 288.32/41.03 % (389204)Time elapsed: 0.104 s % 288.32/41.03 % (389204)Peak memory usage: 18 MB % 288.32/41.03 % (389204)Instructions burned: 206 (million) % 288.32/41.03 % (389206)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3332204091:i=232:rtra=on_2650 on theBenchmark for (2650ds/232Mi) % 288.32/41.03 % (389206)Instruction limit reached! % 288.32/41.03 % (389206)------------------------------ % 288.32/41.03 % (389206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 288.32/41.03 % (389206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.32/41.03 % (389206)CaDiCaL version: 2.1.3 % 288.32/41.03 % (389206)Termination reason: Instruction limit % 288.32/41.03 % (389206)Termination phase: Blocked clause elimination % 288.32/41.03 % (389206)Time elapsed: 0.106 s % 288.32/41.03 % (389206)Peak memory usage: 14 MB % 288.32/41.03 % (389206)Instructions burned: 233 (million) % 288.32/41.03 % (389208)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=26827874:i=262:rtra=on_2648 on theBenchmark for (2648ds/262Mi) % 288.32/41.03 % (389208)Instruction limit reached! % 288.32/41.03 % (389208)------------------------------ % 288.32/41.03 % (389208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 288.32/41.03 % (389208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.32/41.03 % (389208)CaDiCaL version: 2.1.3 % 288.32/41.03 % (389208)Termination reason: Instruction limit % 288.32/41.03 % (389208)Termination phase: Saturation % 288.32/41.03 % (389208)Time elapsed: 0.139 s % 288.32/41.03 % (389208)Peak memory usage: 18 MB % 288.32/41.03 % (389208)Instructions burned: 262 (million) % 288.32/41.03 % (389210)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3869973825:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2647 on theBenchmark for (2647ds/318Mi) % 288.32/41.03 % (389210)Instruction limit reached! % 288.32/41.03 % (389210)------------------------------ % 288.32/41.03 % (389210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 288.32/41.03 % (389210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.32/41.03 % (389210)CaDiCaL version: 2.1.3 % 288.32/41.03 % (389210)Termination reason: Instruction limit % 288.32/41.03 % (389210)Termination phase: Saturation % 288.32/41.03 % (389210)Time elapsed: 0.172 s % 288.32/41.03 % (389210)Peak memory usage: 20 MB % 288.32/41.03 % (389210)Instructions burned: 320 (million) % 288.32/41.03 % (389212)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=469552661:i=1428:nm=2:rtra=on_2645 on theBenchmark for (2645ds/1428Mi) % 288.32/41.03 % (389212)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 288.32/41.03 % (389212)Terminated due to inappropriate strategy. % 288.32/41.03 % (389212)------------------------------ % 288.32/41.03 % (389212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 288.32/41.03 % (389212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.32/41.03 % (389212)CaDiCaL version: 2.1.3 % 288.32/41.03 % (389212)Termination reason: Inappropriate % 288.32/41.03 % (389212)Time elapsed: 0.037 s % 288.32/41.03 % (389212)Peak memory usage: 13 MB % 288.32/41.03 % (389212)Instructions burned: 81 (million) % 300.40/42.64 % (389212)------------------------------ % 300.40/42.64 % (389212)------------------------------ % 300.40/42.64 % (389214)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=677413530:i=262:bd=preordered:rtra=on:fsd=on_2644 on theBenchmark for (2644ds/262Mi) % 300.40/42.64 % (389214)Instruction limit reached! % 300.40/42.64 % (389214)------------------------------ % 300.40/42.64 % (389214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.64 % (389214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.64 % (389214)CaDiCaL version: 2.1.3 % 300.40/42.64 % (389214)Termination reason: Instruction limit % 300.40/42.64 % (389214)Termination phase: Property scanning % 300.40/42.64 % (389214)Time elapsed: 0.125 s % 300.40/42.64 % (389214)Peak memory usage: 14 MB % 300.40/42.64 % (389214)Instructions burned: 263 (million) % 300.40/42.64 % (389216)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=1228835918:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2643 on theBenchmark for (2643ds/1368Mi) % 300.40/42.64 % (389216)Instruction limit reached! % 300.40/42.64 % (389216)------------------------------ % 300.40/42.64 % (389216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.64 % (389216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.64 % (389216)CaDiCaL version: 2.1.3 % 300.40/42.64 % (389216)Termination reason: Instruction limit % 300.40/42.64 % (389216)Termination phase: Saturation % 300.40/42.64 % (389216)Time elapsed: 0.735 s % 300.40/42.64 % (389216)Peak memory usage: 27 MB % 300.40/42.64 % (389216)Instructions burned: 1370 (million) % 300.40/42.64 % (389218)ott-21_1_sil=16000:si=on:fs=off:random_seed=1224458875:i=360:av=off:fsr=off:rtra=on_2635 on theBenchmark for (2635ds/360Mi) % 300.40/42.64 % (389218)Instruction limit reached! % 300.40/42.64 % (389218)------------------------------ % 300.40/42.64 % (389218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.64 % (389218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.64 % (389218)CaDiCaL version: 2.1.3 % 300.40/42.64 % (389218)Termination reason: Instruction limit % 300.40/42.64 % (389218)Termination phase: Saturation % 300.40/42.64 % (389218)Time elapsed: 0.175 s % 300.40/42.64 % (389218)Peak memory usage: 16 MB % 300.40/42.64 % (389218)Instructions burned: 361 (million) % 300.40/42.64 % (389220)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=236319833:i=954:bd=all:rtra=on_2633 on theBenchmark for (2633ds/954Mi) % 300.40/42.64 % (389220)Instruction limit reached! % 300.40/42.64 % (389220)------------------------------ % 300.40/42.64 % (389220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.64 % (389220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.64 % (389220)CaDiCaL version: 2.1.3 % 300.40/42.64 % (389220)Termination reason: Instruction limit % 300.40/42.64 % (389220)Termination phase: Saturation % 300.40/42.64 % (389220)Time elapsed: 0.528 s % 300.40/42.64 % (389220)Peak memory usage: 20 MB % 300.40/42.64 % (389220)Instructions burned: 955 (million) % 300.40/42.64 % (389222)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1908227266:fmbsr=1.3:i=1730:ins=25:rtra=on_2628 on theBenchmark for (2628ds/1730Mi) % 300.40/42.64 % (389222)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.40/42.64 % (389222)Terminated due to inappropriate strategy. % 300.40/42.64 % (389222)------------------------------ % 300.40/42.64 % (389222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.64 % (389222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.64 % (389222)CaDiCaL version: 2.1.3 % 300.40/42.64 % (389222)Termination reason: Inappropriate % 300.40/42.64 % (389222)Time elapsed: 0.051 s % 300.40/42.64 % (389222)Peak memory usage: 15 MB % 300.40/42.64 % (389222)Instructions burned: 109 (million) % 300.40/42.64 % (389222)------------------------------ % 300.40/42.64 % (389222)------------------------------ % 300.40/42.64 % (389224)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3861236793:i=2358:rtra=on_2627 on theBenchmark for (2627ds/2358Mi) % 300.40/42.64 % (389224)Instruction limit reached! % 300.40/42.64 % (389224)------------------------------ % 300.40/42.64 % (389224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.64 % (389224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.64 % (389224)CaDiCaL version: 2.1.3 % 300.40/42.64 % (389224)Termination reason: Instruction limit % 300.40/42.64 % (389224)Termination phase: Saturation % 300.40/42.64 % (389224)Time elapsed: 1.481 s % 300.40/42.64 % (389224)Peak memory usage: 32 MB % 300.40/42.64 % (389224)Instructions burned: 2358 (million) % 300.40/42.64 % (389226)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3630903989:i=1778:ins=1:rtra=on_2612 on theBenchmark for (2612ds/1778Mi) % 300.40/42.64 % (389226)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.40/42.64 % (389226)Terminated due to inappropriate strategy. % 300.40/42.64 % (389226)------------------------------ % 300.40/42.64 % (389226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.64 % (389226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.64 % (389226)CaDiCaL version: 2.1.3 % 300.40/42.64 % (389226)Termination reason: Inappropriate % 300.40/42.64 % (389226)Time elapsed: 0.040 s % 300.40/42.64 % (389226)Peak memory usage: 13 MB % 300.40/42.64 % (389226)Instructions burned: 90 (million) % 300.40/42.64 % (389226)------------------------------ % 300.40/42.64 % (389226)------------------------------ % 300.40/42.64 % (389228)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1955946822:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2611 on theBenchmark for (2611ds/1384Mi) % 300.40/42.64 % (389228)Instruction limit reached! % 300.40/42.64 % (389228)------------------------------ % 300.40/42.64 % (389228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.64 % (389228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.64 % (389228)CaDiCaL version: 2.1.3 % 300.40/42.64 % (389228)Termination reason: Instruction limit % 300.40/42.64 % (389228)Termination phase: Saturation % 300.40/42.64 % (389228)Time elapsed: 0.864 s % 300.40/42.64 % (389228)Peak memory usage: 28 MB % 300.40/42.64 % (389228)Instructions burned: 1384 (million) % 300.40/42.64 % (389230)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1168853559:i=1758:kws=inv_precedence:fsr=off:rtra=on_2602 on theBenchmark for (2602ds/1758Mi) % 300.40/42.64 % (389230)Instruction limit reached! % 300.40/42.64 % (389230)------------------------------ % 300.40/42.64 % (389230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.64 % (389230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.64 % (389230)CaDiCaL version: 2.1.3 % 300.40/42.64 % (389230)Termination reason: Instruction limit % 300.40/42.64 % (389230)Termination phase: Saturation % 300.40/42.64 % (389230)Time elapsed: 0.837 s % 300.40/42.64 % (389230)Peak memory usage: 25 MB % 300.40/42.64 % (389230)Instructions burned: 1759 (million) % 300.40/42.64 % (389232)fmb+10_1_sil=64000:si=on:random_seed=1682398186:i=44122:nm=2:rtra=on:gsp=on_2594 on theBenchmark for (2594ds/44122Mi) % 300.40/42.64 % (389232)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.40/42.64 % (389232)Terminated due to inappropriate strategy. % 300.40/42.64 % (389232)------------------------------ % 300.40/42.64 % (389232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.64 % (389232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.64 % (389232)CaDiCaL version: 2.1.3 % 300.40/42.64 % (389232)Termination reason: Inappropriate % 300.40/42.64 % (389232)Time elapsed: 0.039 s % 300.40/42.64 % (389232)Peak memory usage: 13 MB % 300.40/42.64 % (389232)Instructions burned: 87 (million) % 300.40/42.64 % (389232)------------------------------ % 300.40/42.64 % (389232)------------------------------ % 300.40/42.64 % (389234)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3038455419:i=19030:nm=5:rtra=on_2593 on theBenchmark for (2593ds/19030Mi) % 300.40/42.64 % (389234)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.40/42.64 % (389234)Terminated due to inappropriate strategy. % 300.40/42.64 % (389234)------------------------------ % 300.40/42.64 % (389234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.64 % (389234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.64 % (389234)CaDiCaL version: 2.1.3 % 300.40/42.64 % (389234)Termination reason: Inappropriate % 300.40/42.64 % (389234)Time elapsed: 0.037 s % 300.40/42.64 % (389234)Peak memory usage: 13 MB % 300.40/42.64 % (389234)Instructions burned: 83 (million) % 300.40/42.64 % (389234)------------------------------ % 300.40/42.64 % (389234)------------------------------ % 300.40/42.64 % (389236)fmb+1 % 300.40/42.64 Terminated % 300.40/42.64 % Vampire exiting %------------------------------------------------------------------------------