%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW667_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n009.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:37 PM UTC 2026 % Result : Timeout 300.10s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW667_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 % Computer : n009.cluster.edu % 0.08/0.22 % Model : x86_64 x86_64 % 0.08/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.22 % Memory : 8046.5625MB % 0.08/0.22 % OS : Linux 6.8.0-71-generic % 0.08/0.22 % CPULimit : 300 % 0.08/0.22 % WCLimit : 300 % 0.08/0.22 % DateTime : Mon Sep 28 14:24:30 UTC 2026 % 0.08/0.22 % CPUTime : % 0.08/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.26 Running first-order model finding % 0.08/0.26 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 % 7.38/1.38 % (3062848)Will run a generic schedule for satisfiability detection. % 7.38/1.38 % (3062859)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3655091791:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.38/1.38 % (3062854)% WARNING: option uhcvi not known. % 7.38/1.38 % (3062854)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2246146644:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.38/1.38 % (3062853)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1127598520_2999 on theBenchmark for (2999ds/0Mi) % 7.38/1.38 % (3062858)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3492022992:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.38/1.38 % (3062857)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3820545144:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.38/1.38 % (3062853)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.38/1.38 % (3062853)Terminated due to inappropriate strategy. % 7.38/1.38 % (3062853)------------------------------ % 7.38/1.38 % (3062853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.38/1.38 % (3062853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.38/1.38 % (3062853)CaDiCaL version: 2.1.3 % 7.38/1.38 % (3062853)Termination reason: Inappropriate % 7.38/1.38 % (3062853)Time elapsed: 0.005 s % 7.38/1.38 % (3062853)Peak memory usage: 11 MB % 7.38/1.38 % (3062853)Instructions burned: 5 (million) % 7.38/1.38 % (3062856)dis+10_1_sil=32000:sp=arity:random_seed=3754450701:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.38/1.38 % (3062855)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=467999530:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.38/1.38 % (3062853)------------------------------ % 7.38/1.38 % (3062853)------------------------------ % 7.38/1.38 % (3062867)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2551383436:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.38/1.38 % (3062867)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.38/1.38 % (3062867)Terminated due to inappropriate strategy. % 7.38/1.38 % (3062867)------------------------------ % 7.38/1.38 % (3062867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.38/1.38 % (3062867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.38/1.38 % (3062867)CaDiCaL version: 2.1.3 % 7.38/1.38 % (3062867)Termination reason: Inappropriate % 7.38/1.38 % (3062867)Time elapsed: 0.005 s % 7.38/1.38 % (3062867)Peak memory usage: 11 MB % 7.38/1.38 % (3062867)Instructions burned: 4 (million) % 7.38/1.38 % (3062867)------------------------------ % 7.38/1.38 % (3062867)------------------------------ % 7.38/1.38 % (3062859)Instruction limit reached! % 7.38/1.38 % (3062859)------------------------------ % 7.38/1.38 % (3062859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.38/1.38 % (3062859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.38/1.38 % (3062859)CaDiCaL version: 2.1.3 % 7.38/1.38 % (3062859)Termination reason: Instruction limit % 7.38/1.38 % (3062859)Termination phase: Saturation % 7.38/1.38 % (3062859)Time elapsed: 0.088 s % 7.38/1.38 % (3062859)Peak memory usage: 13 MB % 7.38/1.38 % (3062859)Instructions burned: 161 (million) % 7.38/1.38 % (3062869)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2991881305:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.38/1.38 % (3062870)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=4094542536:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.38/1.38 % (3062856)Instruction limit reached! % 7.38/1.38 % (3062856)------------------------------ % 7.38/1.38 % (3062856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.38/1.38 % (3062856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.38/1.38 % (3062856)CaDiCaL version: 2.1.3 % 7.38/1.38 % (3062856)Termination reason: Instruction limit % 7.38/1.38 % (3062856)Termination phase: Saturation % 7.38/1.38 % (3062856)Time elapsed: 0.108 s % 7.38/1.38 % (3062856)Peak memory usage: 13 MB % 7.38/1.38 % (3062856)Instructions burned: 103 (million) % 7.38/1.38 % (3062858)Instruction limit reached! % 7.38/1.38 % (3062858)------------------------------ % 7.38/1.38 % (3062858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.34/1.64 % (3062858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.34/1.64 % (3062858)CaDiCaL version: 2.1.3 % 9.34/1.64 % (3062858)Termination reason: Instruction limit % 9.34/1.64 % (3062858)Termination phase: Saturation % 9.34/1.64 % (3062858)Time elapsed: 0.129 s % 9.34/1.64 % (3062858)Peak memory usage: 13 MB % 9.34/1.64 % (3062858)Instructions burned: 131 (million) % 9.34/1.64 % (3062857)Instruction limit reached! % 9.34/1.64 % (3062857)------------------------------ % 9.34/1.64 % (3062857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.34/1.64 % (3062857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.34/1.64 % (3062857)CaDiCaL version: 2.1.3 % 9.34/1.64 % (3062857)Termination reason: Instruction limit % 9.34/1.64 % (3062857)Termination phase: Saturation % 9.34/1.64 % (3062857)Time elapsed: 0.125 s % 9.34/1.64 % (3062857)Peak memory usage: 13 MB % 9.34/1.64 % (3062857)Instructions burned: 116 (million) % 9.34/1.64 % (3062873)ott-21_1_sil=16000:fs=off:random_seed=1409332491:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 9.34/1.64 % (3062875)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1164027072:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 9.34/1.64 % (3062874)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2867585554:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 9.34/1.64 % (3062875)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 9.34/1.64 % (3062875)Terminated due to inappropriate strategy. % 9.34/1.64 % (3062875)------------------------------ % 9.34/1.64 % (3062875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.34/1.64 % (3062875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.34/1.64 % (3062875)CaDiCaL version: 2.1.3 % 9.34/1.64 % (3062875)Termination reason: Inappropriate % 9.34/1.64 % (3062875)Time elapsed: 0.005 s % 9.34/1.64 % (3062875)Peak memory usage: 10 MB % 9.34/1.64 % (3062875)Instructions burned: 4 (million) % 9.34/1.64 % (3062875)------------------------------ % 9.34/1.64 % (3062875)------------------------------ % 9.34/1.64 % (3062879)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=469947723:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 9.34/1.64 % (3062869)Instruction limit reached! % 9.34/1.64 % (3062869)------------------------------ % 9.34/1.64 % (3062869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.34/1.64 % (3062869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.34/1.64 % (3062869)CaDiCaL version: 2.1.3 % 9.34/1.64 % (3062869)Termination reason: Instruction limit % 9.34/1.64 % (3062869)Termination phase: Saturation % 9.34/1.64 % (3062869)Time elapsed: 0.142 s % 9.34/1.64 % (3062869)Peak memory usage: 13 MB % 9.34/1.64 % (3062869)Instructions burned: 131 (million) % 9.34/1.64 % (3062881)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3706218342:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 9.34/1.64 % (3062881)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 9.34/1.64 % (3062881)Terminated due to inappropriate strategy. % 9.34/1.64 % (3062881)------------------------------ % 9.34/1.64 % (3062881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.34/1.64 % (3062881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.34/1.64 % (3062881)CaDiCaL version: 2.1.3 % 9.34/1.64 % (3062881)Termination reason: Inappropriate % 9.34/1.64 % (3062881)Time elapsed: 0.005 s % 9.34/1.64 % (3062881)Peak memory usage: 11 MB % 9.34/1.64 % (3062881)Instructions burned: 4 (million) % 9.34/1.64 % (3062881)------------------------------ % 9.34/1.64 % (3062881)------------------------------ % 9.34/1.64 % (3062873)Instruction limit reached! % 9.34/1.64 % (3062873)------------------------------ % 9.34/1.64 % (3062873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.34/1.64 % (3062873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.34/1.64 % (3062873)CaDiCaL version: 2.1.3 % 9.34/1.64 % (3062873)Termination reason: Instruction limit % 9.34/1.64 % (3062873)Termination phase: Saturation % 9.34/1.64 % (3062873)Time elapsed: 0.172 s % 9.34/1.64 % (3062873)Peak memory usage: 13 MB % 9.34/1.64 % (3062873)Instructions burned: 181 (million) % 9.34/1.64 % (3062883)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=1815016358: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) % 32.47/5.03 % (3062884)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=19720996:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 32.47/5.03 % (3062870)Instruction limit reached! % 32.47/5.03 % (3062870)------------------------------ % 32.47/5.03 % (3062870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.47/5.03 % (3062870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.47/5.03 % (3062870)CaDiCaL version: 2.1.3 % 32.47/5.03 % (3062870)Termination reason: Instruction limit % 32.47/5.03 % (3062870)Termination phase: Saturation % 32.47/5.03 % (3062870)Time elapsed: 0.334 s % 32.47/5.03 % (3062870)Peak memory usage: 16 MB % 32.47/5.03 % (3062870)Instructions burned: 684 (million) % 32.47/5.03 % (3062887)fmb+10_1_sil=64000:random_seed=3564383154:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 32.47/5.03 % (3062887)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 32.47/5.03 % (3062887)Terminated due to inappropriate strategy. % 32.47/5.03 % (3062887)------------------------------ % 32.47/5.03 % (3062887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.47/5.03 % (3062887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.47/5.03 % (3062887)CaDiCaL version: 2.1.3 % 32.47/5.03 % (3062887)Termination reason: Inappropriate % 32.47/5.03 % (3062887)Time elapsed: 0.003 s % 32.47/5.03 % (3062887)Peak memory usage: 11 MB % 32.47/5.03 % (3062887)Instructions burned: 5 (million) % 32.47/5.03 % (3062887)------------------------------ % 32.47/5.03 % (3062887)------------------------------ % 32.47/5.03 % (3062889)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=241790787:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 32.47/5.03 % (3062889)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 32.47/5.03 % (3062889)Terminated due to inappropriate strategy. % 32.47/5.03 % (3062889)------------------------------ % 32.47/5.03 % (3062889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.47/5.03 % (3062889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.47/5.03 % (3062889)CaDiCaL version: 2.1.3 % 32.47/5.03 % (3062889)Termination reason: Inappropriate % 32.47/5.03 % (3062889)Time elapsed: 0.004 s % 32.47/5.03 % (3062889)Peak memory usage: 11 MB % 32.47/5.03 % (3062889)Instructions burned: 4 (million) % 32.47/5.03 % (3062889)------------------------------ % 32.47/5.03 % (3062889)------------------------------ % 32.47/5.03 % (3062891)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2552154978:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 32.47/5.03 % (3062891)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 32.47/5.03 % (3062891)Terminated due to inappropriate strategy. % 32.47/5.03 % (3062891)------------------------------ % 32.47/5.03 % (3062891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.47/5.03 % (3062891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.47/5.03 % (3062891)CaDiCaL version: 2.1.3 % 32.47/5.03 % (3062891)Termination reason: Inappropriate % 32.47/5.03 % (3062891)Time elapsed: 0.003 s % 32.47/5.03 % (3062891)Peak memory usage: 11 MB % 32.47/5.03 % (3062891)Instructions burned: 4 (million) % 32.47/5.03 % (3062891)------------------------------ % 32.47/5.03 % (3062891)------------------------------ % 32.47/5.03 % (3062893)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1821657140:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 32.47/5.03 % (3062874)Instruction limit reached! % 32.47/5.03 % (3062874)------------------------------ % 32.47/5.03 % (3062874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.47/5.03 % (3062874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.47/5.03 % (3062874)CaDiCaL version: 2.1.3 % 32.47/5.03 % (3062874)Termination reason: Instruction limit % 32.47/5.03 % (3062874)Termination phase: Saturation % 32.47/5.03 % (3062874)Time elapsed: 0.509 s % 32.47/5.03 % (3062874)Peak memory usage: 14 MB % 32.47/5.03 % (3062874)Instructions burned: 477 (million) % 32.47/5.03 % (3062895)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3661384276:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 32.47/5.03 % (3062883)Instruction limit reached! % 32.47/5.03 % (3062883)------------------------------ % 43.44/6.54 % (3062883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.44/6.54 % (3062883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.44/6.54 % (3062883)CaDiCaL version: 2.1.3 % 43.44/6.54 % (3062883)Termination reason: Instruction limit % 43.44/6.54 % (3062883)Termination phase: Saturation % 43.44/6.54 % (3062883)Time elapsed: 0.749 s % 43.44/6.54 % (3062883)Peak memory usage: 19 MB % 43.44/6.54 % (3062883)Instructions burned: 693 (million) % 43.44/6.54 % (3062897)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2229147941:i=6324_2988 on theBenchmark for (2988ds/6324Mi) % 43.44/6.54 % (3062897)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.44/6.54 % (3062897)Terminated due to inappropriate strategy. % 43.44/6.54 % (3062897)------------------------------ % 43.44/6.54 % (3062897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.44/6.54 % (3062897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.44/6.54 % (3062897)CaDiCaL version: 2.1.3 % 43.44/6.54 % (3062897)Termination reason: Inappropriate % 43.44/6.54 % (3062897)Time elapsed: 0.007 s % 43.44/6.54 % (3062897)Peak memory usage: 11 MB % 43.44/6.54 % (3062897)Instructions burned: 5 (million) % 43.44/6.54 % (3062897)------------------------------ % 43.44/6.54 % (3062897)------------------------------ % 43.44/6.54 % (3062899)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2466032352:fmbsr=2.30978:i=2174_2988 on theBenchmark for (2988ds/2174Mi) % 43.44/6.54 % (3062899)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.44/6.54 % (3062899)Terminated due to inappropriate strategy. % 43.44/6.54 % (3062899)------------------------------ % 43.44/6.54 % (3062899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.44/6.54 % (3062899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.44/6.54 % (3062899)CaDiCaL version: 2.1.3 % 43.44/6.54 % (3062899)Termination reason: Inappropriate % 43.44/6.54 % (3062899)Time elapsed: 0.003 s % 43.44/6.54 % (3062899)Peak memory usage: 11 MB % 43.44/6.54 % (3062899)Instructions burned: 4 (million) % 43.44/6.54 % (3062899)------------------------------ % 43.44/6.54 % (3062899)------------------------------ % 43.44/6.54 % (3062901)ott-2_1_sil=16000:newcnf=on:random_seed=78400489:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi) % 43.44/6.54 % (3062884)Instruction limit reached! % 43.44/6.54 % (3062884)------------------------------ % 43.44/6.54 % (3062884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.44/6.54 % (3062884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.44/6.54 % (3062884)CaDiCaL version: 2.1.3 % 43.44/6.54 % (3062884)Termination reason: Instruction limit % 43.44/6.54 % (3062884)Termination phase: Saturation % 43.44/6.54 % (3062884)Time elapsed: 0.867 s % 43.44/6.54 % (3062884)Peak memory usage: 20 MB % 43.44/6.54 % (3062884)Instructions burned: 879 (million) % 43.44/6.54 % (3062903)ott+10_1_sil=32000:tgt=ground:random_seed=3342310709:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi) % 43.44/6.54 % (3062879)Instruction limit reached! % 43.44/6.54 % (3062879)------------------------------ % 43.44/6.54 % (3062879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.44/6.54 % (3062879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.44/6.54 % (3062879)CaDiCaL version: 2.1.3 % 43.44/6.54 % (3062879)Termination reason: Instruction limit % 43.44/6.54 % (3062879)Termination phase: Saturation % 43.44/6.54 % (3062879)Time elapsed: 1.066 s % 43.44/6.54 % (3062879)Peak memory usage: 19 MB % 43.44/6.54 % (3062879)Instructions burned: 1179 (million) % 43.44/6.54 % (3062905)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3629835473:i=54282_2986 on theBenchmark for (2986ds/54282Mi) % 43.44/6.54 % (3062905)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.44/6.54 % (3062905)Terminated due to inappropriate strategy. % 43.44/6.54 % (3062905)------------------------------ % 43.44/6.54 % (3062905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.44/6.54 % (3062905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.44/6.54 % (3062905)CaDiCaL version: 2.1.3 % 43.44/6.54 % (3062905)Termination reason: Inappropriate % 43.44/6.54 % (3062905)Time elapsed: 0.006 s % 43.44/6.54 % (3062905)Peak memory usage: 11 MB % 43.44/6.54 % (3062905)Instructions burned: 5 (million) % 146.11/20.82 % (3062905)------------------------------ % 146.11/20.82 % (3062905)------------------------------ % 146.11/20.82 % (3062907)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1266912297:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi) % 146.11/20.82 % (3062895)Instruction limit reached! % 146.11/20.82 % (3062895)------------------------------ % 146.11/20.82 % (3062895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.11/20.82 % (3062895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.11/20.82 % (3062895)CaDiCaL version: 2.1.3 % 146.11/20.82 % (3062895)Termination reason: Instruction limit % 146.11/20.82 % (3062895)Termination phase: Saturation % 146.11/20.82 % (3062895)Time elapsed: 1.289 s % 146.11/20.82 % (3062895)Peak memory usage: 18 MB % 146.11/20.82 % (3062895)Instructions burned: 1472 (million) % 146.11/20.82 % (3062901)Instruction limit reached! % 146.11/20.82 % (3062901)------------------------------ % 146.11/20.82 % (3062901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.11/20.82 % (3062901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.11/20.82 % (3062901)CaDiCaL version: 2.1.3 % 146.11/20.82 % (3062901)Termination reason: Instruction limit % 146.11/20.82 % (3062901)Termination phase: Saturation % 146.11/20.82 % (3062901)Time elapsed: 0.863 s % 146.11/20.82 % (3062901)Peak memory usage: 16 MB % 146.11/20.82 % (3062901)Instructions burned: 869 (million) % 146.11/20.82 % (3062913)dis+21_1_sil=32000:sas=cadical:random_seed=1889396476:i=3773:amm=off_2979 on theBenchmark for (2979ds/3773Mi) % 146.11/20.82 % (3062914)ott+11_1_sil=16000:gs=on:random_seed=3832397000:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2979 on theBenchmark for (2979ds/2251Mi) % 146.11/20.82 % (3062893)Instruction limit reached! % 146.11/20.82 % (3062893)------------------------------ % 146.11/20.82 % (3062893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.11/20.82 % (3062893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.11/20.82 % (3062893)CaDiCaL version: 2.1.3 % 146.11/20.82 % (3062893)Termination reason: Instruction limit % 146.11/20.82 % (3062893)Termination phase: Saturation % 146.11/20.82 % (3062893)Time elapsed: 2.518 s % 146.11/20.82 % (3062893)Peak memory usage: 42 MB % 146.11/20.82 % (3062893)Instructions burned: 5133 (million) % 146.11/20.82 % (3062921)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2700058531:fmbsr=1.6:i=67534_2968 on theBenchmark for (2968ds/67534Mi) % 146.11/20.82 % (3062921)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.11/20.82 % (3062921)Terminated due to inappropriate strategy. % 146.11/20.82 % (3062921)------------------------------ % 146.11/20.82 % (3062921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.11/20.82 % (3062921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.11/20.82 % (3062921)CaDiCaL version: 2.1.3 % 146.11/20.82 % (3062921)Termination reason: Inappropriate % 146.11/20.82 % (3062921)Time elapsed: 0.003 s % 146.11/20.82 % (3062921)Peak memory usage: 11 MB % 146.11/20.82 % (3062921)Instructions burned: 5 (million) % 146.11/20.82 % (3062921)------------------------------ % 146.11/20.82 % (3062921)------------------------------ % 146.11/20.82 % (3062923)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2319073287:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2968 on theBenchmark for (2968ds/4591Mi) % 146.11/20.82 % (3062914)Instruction limit reached! % 146.11/20.82 % (3062914)------------------------------ % 146.11/20.82 % (3062914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.11/20.82 % (3062914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.11/20.82 % (3062914)CaDiCaL version: 2.1.3 % 146.11/20.82 % (3062914)Termination reason: Instruction limit % 146.11/20.82 % (3062914)Termination phase: Saturation % 146.11/20.82 % (3062914)Time elapsed: 1.993 s % 146.11/20.82 % (3062914)Peak memory usage: 17 MB % 146.11/20.82 % (3062914)Instructions burned: 2251 (million) % 146.11/20.82 % (3062925)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3498826978:i=29340_2958 on theBenchmark for (2958ds/29340Mi) % 146.11/20.82 % (3062907)Instruction limit reached! % 146.11/20.82 % (3062907)------------------------------ % 146.11/20.82 % (3062907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.11/20.82 % (3062907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.11/20.82 % (3062907)CaDiCaL version: 2.1.3 % 146.11/20.82 % (3062907)Termination reason: Instruction limit % 205.88/29.22 % (3062907)Termination phase: Saturation % 205.88/29.22 % (3062907)Time elapsed: 3.363 s % 205.88/29.22 % (3062907)Peak memory usage: 33 MB % 205.88/29.22 % (3062907)Instructions burned: 3513 (million) % 205.88/29.22 % (3062929)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2137086385:i=5211_2952 on theBenchmark for (2952ds/5211Mi) % 205.88/29.22 % (3062923)Instruction limit reached! % 205.88/29.22 % (3062923)------------------------------ % 205.88/29.22 % (3062923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.88/29.22 % (3062923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.88/29.22 % (3062923)CaDiCaL version: 2.1.3 % 205.88/29.22 % (3062923)Termination reason: Instruction limit % 205.88/29.22 % (3062923)Termination phase: Saturation % 205.88/29.22 % (3062923)Time elapsed: 2.480 s % 205.88/29.22 % (3062923)Peak memory usage: 89 MB % 205.88/29.22 % (3062923)Instructions burned: 4592 (million) % 205.88/29.22 % (3062931)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2384578981:i=5497:nm=2_2943 on theBenchmark for (2943ds/5497Mi) % 205.88/29.22 % (3062931)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.88/29.22 % (3062931)Terminated due to inappropriate strategy. % 205.88/29.22 % (3062931)------------------------------ % 205.88/29.22 % (3062931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.88/29.22 % (3062931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.88/29.22 % (3062931)CaDiCaL version: 2.1.3 % 205.88/29.22 % (3062931)Termination reason: Inappropriate % 205.88/29.22 % (3062931)Time elapsed: 0.003 s % 205.88/29.22 % (3062931)Peak memory usage: 11 MB % 205.88/29.22 % (3062931)Instructions burned: 5 (million) % 205.88/29.22 % (3062931)------------------------------ % 205.88/29.22 % (3062931)------------------------------ % 205.88/29.22 % (3062913)Instruction limit reached! % 205.88/29.22 % (3062913)------------------------------ % 205.88/29.22 % (3062913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.88/29.22 % (3062913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.88/29.22 % (3062913)CaDiCaL version: 2.1.3 % 205.88/29.22 % (3062913)Termination reason: Instruction limit % 205.88/29.22 % (3062913)Termination phase: Saturation % 205.88/29.22 % (3062913)Time elapsed: 3.625 s % 205.88/29.22 % (3062913)Peak memory usage: 33 MB % 205.88/29.22 % (3062913)Instructions burned: 3776 (million) % 205.88/29.22 % (3062933)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2624982637:fmbsr=2:i=46332_2942 on theBenchmark for (2942ds/46332Mi) % 205.88/29.22 % (3062933)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.88/29.22 % (3062933)Terminated due to inappropriate strategy. % 205.88/29.22 % (3062933)------------------------------ % 205.88/29.22 % (3062933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.88/29.22 % (3062933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.88/29.22 % (3062933)CaDiCaL version: 2.1.3 % 205.88/29.22 % (3062933)Termination reason: Inappropriate % 205.88/29.22 % (3062933)Time elapsed: 0.003 s % 205.88/29.22 % (3062933)Peak memory usage: 10 MB % 205.88/29.22 % (3062933)Instructions burned: 5 (million) % 205.88/29.22 % (3062933)------------------------------ % 205.88/29.22 % (3062933)------------------------------ % 205.88/29.22 % (3062934)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1676773919:i=14071_2942 on theBenchmark for (2942ds/14071Mi) % 205.88/29.22 % (3062934)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.88/29.22 % (3062934)Terminated due to inappropriate strategy. % 205.88/29.22 % (3062934)------------------------------ % 205.88/29.22 % (3062934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.88/29.22 % (3062934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.88/29.22 % (3062934)CaDiCaL version: 2.1.3 % 205.88/29.22 % (3062934)Termination reason: Inappropriate % 205.88/29.22 % (3062934)Time elapsed: 0.005 s % 205.88/29.22 % (3062934)Peak memory usage: 11 MB % 205.88/29.22 % (3062934)Instructions burned: 5 (million) % 205.88/29.22 % (3062934)------------------------------ % 205.88/29.22 % (3062934)------------------------------ % 205.88/29.22 % (3062936)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3344517750:i=22565:add=on:rawr=on_2942 on theBenchmark for (2942ds/22565Mi) % 205.88/29.22 % (3062938)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1490954899:i=8173:av=off_2942 on theBenchmark for (2942ds/8173Mi) % 205.88/29.22 % (3062903)Instruction limit reached! % 206.58/29.34 % (3062903)------------------------------ % 206.58/29.34 % (3062903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.58/29.34 % (3062903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.58/29.34 % (3062903)CaDiCaL version: 2.1.3 % 206.58/29.34 % (3062903)Termination reason: Instruction limit % 206.58/29.34 % (3062903)Termination phase: Saturation % 206.58/29.34 % (3062903)Time elapsed: 4.969 s % 206.58/29.34 % (3062903)Peak memory usage: 41 MB % 206.58/29.34 % (3062903)Instructions burned: 5114 (million) % 206.58/29.34 % (3062943)dis+10_16:1_sil=16000:random_seed=1290626687:i=9155:fsr=off_2937 on theBenchmark for (2937ds/9155Mi) % 206.58/29.34 % (3062929)Instruction limit reached! % 206.58/29.34 % (3062929)------------------------------ % 206.58/29.34 % (3062929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.58/29.34 % (3062929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.58/29.34 % (3062929)CaDiCaL version: 2.1.3 % 206.58/29.34 % (3062929)Termination reason: Instruction limit % 206.58/29.34 % (3062929)Termination phase: Saturation % 206.58/29.34 % (3062929)Time elapsed: 4.389 s % 206.58/29.34 % (3062929)Peak memory usage: 41 MB % 206.58/29.34 % (3062929)Instructions burned: 5211 (million) % 206.58/29.34 % (3062955)ott-3_8_sil=64000:random_seed=3726846552:i=20139:bs=on_2908 on theBenchmark for (2908ds/20139Mi) % 206.58/29.34 % (3062936)Instruction limit reached! % 206.58/29.34 % (3062936)------------------------------ % 206.58/29.34 % (3062936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.58/29.34 % (3062936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.58/29.34 % (3062936)CaDiCaL version: 2.1.3 % 206.58/29.34 % (3062936)Termination reason: Instruction limit % 206.58/29.34 % (3062936)Termination phase: Saturation % 206.58/29.34 % (3062936)Time elapsed: 8.408 s % 206.58/29.34 % (3062936)Peak memory usage: 22 MB % 206.58/29.34 % (3062936)Instructions burned: 22566 (million) % 206.58/29.34 % (3062972)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4196921176:fmbsr=2:i=32576_2858 on theBenchmark for (2858ds/32576Mi) % 206.58/29.34 % (3062972)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 206.58/29.34 % (3062972)Terminated due to inappropriate strategy. % 206.58/29.34 % (3062972)------------------------------ % 206.58/29.34 % (3062972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.58/29.34 % (3062972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.58/29.34 % (3062972)CaDiCaL version: 2.1.3 % 206.58/29.34 % (3062972)Termination reason: Inappropriate % 206.58/29.34 % (3062972)Time elapsed: 0.004 s % 206.58/29.34 % (3062972)Peak memory usage: 11 MB % 206.58/29.34 % (3062972)Instructions burned: 5 (million) % 206.58/29.34 % (3062972)------------------------------ % 206.58/29.34 % (3062972)------------------------------ % 206.58/29.34 % (3062975)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2445925076:i=11404_2857 on theBenchmark for (2857ds/11404Mi) % 206.58/29.34 % (3062938)Instruction limit reached! % 206.58/29.34 % (3062938)------------------------------ % 206.58/29.34 % (3062938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.58/29.34 % (3062938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.58/29.34 % (3062938)CaDiCaL version: 2.1.3 % 206.58/29.34 % (3062938)Termination reason: Instruction limit % 206.58/29.34 % (3062938)Termination phase: Saturation % 206.58/29.34 % (3062938)Time elapsed: 8.467 s % 206.58/29.34 % (3062938)Peak memory usage: 74 MB % 206.58/29.34 % (3062938)Instructions burned: 8173 (million) % 206.58/29.34 % (3062977)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3134669266:i=14134_2857 on theBenchmark for (2857ds/14134Mi) % 206.58/29.34 % (3062943)Instruction limit reached! % 206.58/29.34 % (3062943)------------------------------ % 206.58/29.34 % (3062943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.58/29.34 % (3062943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.58/29.34 % (3062943)CaDiCaL version: 2.1.3 % 206.58/29.34 % (3062943)Termination reason: Instruction limit % 206.58/29.34 % (3062943)Termination phase: Saturation % 206.58/29.34 % (3062943)Time elapsed: 8.204 s % 206.58/29.34 % (3062943)Peak memory usage: 51 MB % 206.58/29.34 % (3062943)Instructions burned: 9155 (million) % 206.58/29.34 % (3062979)dis+33_16_sil=32000:sac=on:random_seed=637718518:i=15851:nm=0_2854 on theBenchmark for (2854ds/15851Mi) % 206.58/29.34 % (3062975)Instruction limit reached! % 206.58/29.34 % (3062975)------------------------------ % 206.58/29.34 % (3062975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.72/31.10 % (3062975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.72/31.10 % (3062975)CaDiCaL version: 2.1.3 % 218.72/31.10 % (3062975)Termination reason: Instruction limit % 218.72/31.10 % (3062975)Termination phase: Saturation % 218.72/31.10 % (3062975)Time elapsed: 6.294 s % 218.72/31.10 % (3062975)Peak memory usage: 67 MB % 218.72/31.10 % (3062975)Instructions burned: 11404 (million) % 218.72/31.10 % (3062986)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4044197982:avsq=on:i=17627:add=on:amm=off_2794 on theBenchmark for (2794ds/17627Mi) % 218.72/31.10 % (3062979)Instruction limit reached! % 218.72/31.10 % (3062979)------------------------------ % 218.72/31.10 % (3062979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.72/31.10 % (3062979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.72/31.10 % (3062979)CaDiCaL version: 2.1.3 % 218.72/31.10 % (3062979)Termination reason: Instruction limit % 218.72/31.10 % (3062979)Termination phase: Saturation % 218.72/31.10 % (3062979)Time elapsed: 13.927 s % 218.72/31.10 % (3062979)Peak memory usage: 123 MB % 218.72/31.10 % (3062979)Instructions burned: 15852 (million) % 218.72/31.10 % (3062996)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4178133884:s2a=on:i=53295_2714 on theBenchmark for (2714ds/53295Mi) % 218.72/31.10 % (3062925)Instruction limit reached! % 218.72/31.10 % (3062925)------------------------------ % 218.72/31.10 % (3062925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.72/31.10 % (3062925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.72/31.10 % (3062925)CaDiCaL version: 2.1.3 % 218.72/31.10 % (3062925)Termination reason: Instruction limit % 218.72/31.10 % (3062925)Termination phase: Saturation % 218.72/31.10 % (3062925)Time elapsed: 24.397 s % 218.72/31.10 % (3062925)Peak memory usage: 239 MB % 218.72/31.10 % (3062925)Instructions burned: 29341 (million) % 218.72/31.10 % (3063015)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3234206009:i=26857:ins=20_2714 on theBenchmark for (2714ds/26857Mi) % 218.72/31.10 % (3063015)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 218.72/31.10 % (3063015)Terminated due to inappropriate strategy. % 218.72/31.10 % (3063015)------------------------------ % 218.72/31.10 % (3063015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.72/31.10 % (3063015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.72/31.10 % (3063015)CaDiCaL version: 2.1.3 % 218.72/31.10 % (3063015)Termination reason: Inappropriate % 218.72/31.10 % (3063015)Time elapsed: 0.003 s % 218.72/31.10 % (3063015)Peak memory usage: 11 MB % 218.72/31.10 % (3063015)Instructions burned: 4 (million) % 218.72/31.10 % (3063015)------------------------------ % 218.72/31.10 % (3063015)------------------------------ % 218.72/31.10 % (3063025)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=338915661:i=28120:bs=on:fsr=off_2713 on theBenchmark for (2713ds/28120Mi) % 218.72/31.10 % (3062977)Instruction limit reached! % 218.72/31.10 % (3062977)------------------------------ % 218.72/31.10 % (3062977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.72/31.10 % (3062977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.72/31.10 % (3062977)CaDiCaL version: 2.1.3 % 218.72/31.10 % (3062977)Termination reason: Instruction limit % 218.72/31.10 % (3062977)Termination phase: Saturation % 218.72/31.10 % (3062977)Time elapsed: 14.569 s % 218.72/31.10 % (3062977)Peak memory usage: 79 MB % 218.72/31.10 % (3062977)Instructions burned: 14135 (million) % 218.72/31.10 % (3063108)fmb+10_1_sil=256000:fmbss=7:random_seed=2512756474:fmbsr=1.6:i=182295_2710 on theBenchmark for (2710ds/182295Mi) % 218.72/31.10 % (3063108)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 218.72/31.10 % (3063108)Terminated due to inappropriate strategy. % 218.72/31.10 % (3063108)------------------------------ % 218.72/31.10 % (3063108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.72/31.10 % (3063108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.72/31.10 % (3063108)CaDiCaL version: 2.1.3 % 218.72/31.10 % (3063108)Termination reason: Inappropriate % 218.72/31.10 % (3063108)Time elapsed: 0.003 s % 218.72/31.10 % (3063108)Peak memory usage: 11 MB % 218.72/31.10 % (3063108)Instructions burned: 4 (million) % 218.72/31.10 % (3063108)------------------------------ % 218.72/31.10 % (3063108)------------------------------ % 218.72/31.10 % (3063110)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1531646809:i=44625:gsp=on_2710 on theBenchmark for (2710ds/44625Mi) % 230.68/32.88 % (3063110)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 230.68/32.88 % (3063110)Terminated due to inappropriate strategy. % 230.68/32.88 % (3063110)------------------------------ % 230.68/32.88 % (3063110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.68/32.88 % (3063110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.68/32.88 % (3063110)CaDiCaL version: 2.1.3 % 230.68/32.88 % (3063110)Termination reason: Inappropriate % 230.68/32.88 % (3063110)Time elapsed: 0.003 s % 230.68/32.88 % (3063110)Peak memory usage: 11 MB % 230.68/32.88 % (3063110)Instructions burned: 5 (million) % 230.68/32.88 % (3063110)------------------------------ % 230.68/32.88 % (3063110)------------------------------ % 230.68/32.88 % (3063112)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3081610531:i=160505_2710 on theBenchmark for (2710ds/160505Mi) % 230.68/32.88 % (3063112)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 230.68/32.88 % (3063112)Terminated due to inappropriate strategy. % 230.68/32.88 % (3063112)------------------------------ % 230.68/32.88 % (3063112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.68/32.88 % (3063112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.68/32.88 % (3063112)CaDiCaL version: 2.1.3 % 230.68/32.88 % (3063112)Termination reason: Inappropriate % 230.68/32.88 % (3063112)Time elapsed: 0.003 s % 230.68/32.88 % (3063112)Peak memory usage: 11 MB % 230.68/32.88 % (3063112)Instructions burned: 4 (million) % 230.68/32.88 % (3063112)------------------------------ % 230.68/32.88 % (3063112)------------------------------ % 230.68/32.88 % (3063114)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1322896627:fmbsr=1.3:i=225729_2710 on theBenchmark for (2710ds/225729Mi) % 230.68/32.88 % (3063114)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 230.68/32.88 % (3063114)Terminated due to inappropriate strategy. % 230.68/32.88 % (3063114)------------------------------ % 230.68/32.88 % (3063114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.68/32.88 % (3063114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.68/32.88 % (3063114)CaDiCaL version: 2.1.3 % 230.68/32.88 % (3063114)Termination reason: Inappropriate % 230.68/32.88 % (3063114)Time elapsed: 0.003 s % 230.68/32.88 % (3063114)Peak memory usage: 11 MB % 230.68/32.88 % (3063114)Instructions burned: 5 (million) % 230.68/32.88 % (3063114)------------------------------ % 230.68/32.88 % (3063114)------------------------------ % 230.68/32.88 % (3063118)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1437686863:fmbsr=2:i=185024:ins=7_2710 on theBenchmark for (2710ds/185024Mi) % 230.68/32.88 % (3063118)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 230.68/32.88 % (3063118)Terminated due to inappropriate strategy. % 230.68/32.88 % (3063118)------------------------------ % 230.68/32.88 % (3063118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.68/32.88 % (3063118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.68/32.88 % (3063118)CaDiCaL version: 2.1.3 % 230.68/32.88 % (3063118)Termination reason: Inappropriate % 230.68/32.88 % (3063118)Time elapsed: 0.003 s % 230.68/32.88 % (3063118)Peak memory usage: 11 MB % 230.68/32.88 % (3063118)Instructions burned: 5 (million) % 230.68/32.88 % (3063118)------------------------------ % 230.68/32.88 % (3063118)------------------------------ % 230.68/32.88 % (3063126)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2838541431:rtra=on_2709 on theBenchmark for (2709ds/0Mi) % 230.68/32.88 % (3063126)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 230.68/32.88 % (3063126)Terminated due to inappropriate strategy. % 230.68/32.88 % (3063126)------------------------------ % 230.68/32.88 % (3063126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.68/32.88 % (3063126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.68/32.88 % (3063126)CaDiCaL version: 2.1.3 % 230.68/32.88 % (3063126)Termination reason: Inappropriate % 230.68/32.88 % (3063126)Time elapsed: 0.003 s % 230.68/32.88 % (3063126)Peak memory usage: 11 MB % 230.68/32.88 % (3063126)Instructions burned: 5 (million) % 230.68/32.88 % (3063126)------------------------------ % 230.68/32.88 % (3063126)------------------------------ % 230.68/32.88 % (3063139)% WARNING: option uhcvi not known. % 230.68/32.88 % (3063139)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1774444323:i=271062:add=off:rtra=on:rawr=on_2709 on theBenchmark for (2709ds/271062Mi) % 256.78/36.42 % (3062986)Instruction limit reached! % 256.78/36.42 % (3062986)------------------------------ % 256.78/36.42 % (3062986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.78/36.42 % (3062986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.78/36.42 % (3062986)CaDiCaL version: 2.1.3 % 256.78/36.42 % (3062986)Termination reason: Instruction limit % 256.78/36.42 % (3062986)Termination phase: Saturation % 256.78/36.42 % (3062986)Time elapsed: 8.559 s % 256.78/36.42 % (3062986)Peak memory usage: 97 MB % 256.78/36.42 % (3062986)Instructions burned: 17629 (million) % 256.78/36.42 % (3063169)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2898732154:i=176048:add=on:rtra=on:rawr=on_2708 on theBenchmark for (2708ds/176048Mi) % 256.78/36.42 % (3062955)Instruction limit reached! % 256.78/36.42 % (3062955)------------------------------ % 256.78/36.42 % (3062955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.78/36.42 % (3062955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.78/36.42 % (3062955)CaDiCaL version: 2.1.3 % 256.78/36.42 % (3062955)Termination reason: Instruction limit % 256.78/36.42 % (3062955)Termination phase: Saturation % 256.78/36.42 % (3062955)Time elapsed: 20.663 s % 256.78/36.42 % (3062955)Peak memory usage: 85 MB % 256.78/36.42 % (3062955)Instructions burned: 20140 (million) % 256.78/36.42 % (3063171)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4278837334:i=206:fgj=on:rtra=on_2700 on theBenchmark for (2700ds/206Mi) % 256.78/36.42 % (3063171)Instruction limit reached! % 256.78/36.42 % (3063171)------------------------------ % 256.78/36.42 % (3063171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.78/36.42 % (3063171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.78/36.42 % (3063171)CaDiCaL version: 2.1.3 % 256.78/36.42 % (3063171)Termination reason: Instruction limit % 256.78/36.42 % (3063171)Termination phase: Saturation % 256.78/36.42 % (3063171)Time elapsed: 0.130 s % 256.78/36.42 % (3063171)Peak memory usage: 14 MB % 256.78/36.42 % (3063171)Instructions burned: 206 (million) % 256.78/36.42 % (3063173)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=957637131:i=232:rtra=on_2698 on theBenchmark for (2698ds/232Mi) % 256.78/36.42 % (3063173)Instruction limit reached! % 256.78/36.42 % (3063173)------------------------------ % 256.78/36.42 % (3063173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.78/36.42 % (3063173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.78/36.42 % (3063173)CaDiCaL version: 2.1.3 % 256.78/36.42 % (3063173)Termination reason: Instruction limit % 256.78/36.42 % (3063173)Termination phase: Saturation % 256.78/36.42 % (3063173)Time elapsed: 0.154 s % 256.78/36.42 % (3063173)Peak memory usage: 14 MB % 256.78/36.42 % (3063173)Instructions burned: 232 (million) % 256.78/36.42 % (3063175)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=4086441165:i=262:rtra=on_2696 on theBenchmark for (2696ds/262Mi) % 256.78/36.42 % (3063175)Instruction limit reached! % 256.78/36.42 % (3063175)------------------------------ % 256.78/36.42 % (3063175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.78/36.42 % (3063175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.78/36.42 % (3063175)CaDiCaL version: 2.1.3 % 256.78/36.42 % (3063175)Termination reason: Instruction limit % 256.78/36.42 % (3063175)Termination phase: Saturation % 256.78/36.42 % (3063175)Time elapsed: 0.166 s % 256.78/36.42 % (3063175)Peak memory usage: 14 MB % 256.78/36.42 % (3063175)Instructions burned: 262 (million) % 256.78/36.42 % (3063177)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1217425447:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2694 on theBenchmark for (2694ds/318Mi) % 256.78/36.42 % (3063177)Instruction limit reached! % 256.78/36.42 % (3063177)------------------------------ % 256.78/36.42 % (3063177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.78/36.42 % (3063177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.78/36.42 % (3063177)CaDiCaL version: 2.1.3 % 256.78/36.42 % (3063177)Termination reason: Instruction limit % 256.78/36.42 % (3063177)Termination phase: Saturation % 256.78/36.42 % (3063177)Time elapsed: 0.205 s % 256.78/36.42 % (3063177)Peak memory usage: 15 MB % 256.78/36.42 % (3063177)Instructions burned: 319 (million) % 256.78/36.42 % (3063179)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3658092635:i=1428:nm=2:rtra=on_26Terminated % 300.10/42.54 % Vampire exiting % 300.10/42.54 Terminated %------------------------------------------------------------------------------