%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC460_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:06:02 PM UTC 2026 % Result : Timeout 300.11s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC460_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.18 % Computer : n011.cluster.edu % 0.07/0.18 % Model : x86_64 x86_64 % 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.18 % Memory : 8046.5625MB % 0.07/0.18 % OS : Linux 6.8.0-71-generic % 0.07/0.18 % CPULimit : 300 % 0.07/0.18 % WCLimit : 300 % 0.07/0.18 % DateTime : Mon Sep 28 09:39:31 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.21 Running first-order model finding % 0.07/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.63/0.83 % (3275750)Will run a generic schedule for satisfiability detection. % 3.63/0.83 % (3275761)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1531331587:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.63/0.83 % (3275756)% WARNING: option uhcvi not known. % 3.63/0.83 % (3275757)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3870793182:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.63/0.83 % (3275755)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3085359543_2999 on theBenchmark for (2999ds/0Mi) % 3.63/0.83 % (3275756)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4170700789:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.63/0.83 % (3275758)dis+10_1_sil=32000:sp=arity:random_seed=2109534229:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.63/0.83 % (3275759)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=569684321:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.63/0.83 % (3275760)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=921567985:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.63/0.83 % (3275755)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.63/0.83 % (3275755)Terminated due to inappropriate strategy. % 3.63/0.83 % (3275755)------------------------------ % 3.63/0.83 % (3275755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.63/0.83 % (3275755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.63/0.83 % (3275755)CaDiCaL version: 2.1.3 % 3.63/0.83 % (3275755)Termination reason: Inappropriate % 3.63/0.83 % (3275755)Time elapsed: 0.001 s % 3.63/0.83 % (3275755)Peak memory usage: 10 MB % 3.63/0.83 % (3275755)Instructions burned: 1 (million) % 3.63/0.83 % (3275755)------------------------------ % 3.63/0.83 % (3275755)------------------------------ % 3.63/0.83 % (3275769)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3810136268:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.63/0.83 % (3275769)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.63/0.83 % (3275769)Terminated due to inappropriate strategy. % 3.63/0.83 % (3275769)------------------------------ % 3.63/0.83 % (3275769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.63/0.83 % (3275769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.63/0.83 % (3275769)CaDiCaL version: 2.1.3 % 3.63/0.83 % (3275769)Termination reason: Inappropriate % 3.63/0.83 % (3275769)Time elapsed: 0.001 s % 3.63/0.83 % (3275769)Peak memory usage: 11 MB % 3.63/0.83 % (3275769)Instructions burned: 1 (million) % 3.63/0.83 % (3275769)------------------------------ % 3.63/0.83 % (3275769)------------------------------ % 3.63/0.83 % (3275771)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1783345832:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.63/0.83 % (3275761)Instruction limit reached! % 3.63/0.83 % (3275761)------------------------------ % 3.63/0.83 % (3275761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.63/0.83 % (3275761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.63/0.83 % (3275761)CaDiCaL version: 2.1.3 % 3.63/0.83 % (3275761)Termination reason: Instruction limit % 3.63/0.83 % (3275761)Termination phase: Saturation % 3.63/0.83 % (3275761)Time elapsed: 0.059 s % 3.63/0.83 % (3275761)Peak memory usage: 13 MB % 3.63/0.83 % (3275761)Instructions burned: 160 (million) % 3.63/0.83 % (3275773)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=2558695026:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.63/0.83 % (3275758)Instruction limit reached! % 3.63/0.83 % (3275758)------------------------------ % 3.63/0.83 % (3275758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.63/0.83 % (3275758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.63/0.83 % (3275758)CaDiCaL version: 2.1.3 % 3.63/0.83 % (3275758)Termination reason: Instruction limit % 3.63/0.83 % (3275758)Termination phase: Saturation % 3.63/0.83 % (3275758)Time elapsed: 0.065 s % 3.63/0.83 % (3275758)Peak memory usage: 13 MB % 3.63/0.83 % (3275758)Instructions burned: 103 (million) % 3.63/0.83 % (3275759)Instruction limit reached! % 3.63/0.83 % (3275759)------------------------------ % 3.63/0.83 % (3275759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.79/1.09 % (3275759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.79/1.09 % (3275759)CaDiCaL version: 2.1.3 % 5.79/1.09 % (3275759)Termination reason: Instruction limit % 5.79/1.09 % (3275759)Termination phase: Saturation % 5.79/1.09 % (3275759)Time elapsed: 0.074 s % 5.79/1.09 % (3275759)Peak memory usage: 12 MB % 5.79/1.09 % (3275759)Instructions burned: 117 (million) % 5.79/1.09 % (3275760)Instruction limit reached! % 5.79/1.09 % (3275760)------------------------------ % 5.79/1.09 % (3275760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.79/1.09 % (3275760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.79/1.09 % (3275760)CaDiCaL version: 2.1.3 % 5.79/1.09 % (3275760)Termination reason: Instruction limit % 5.79/1.09 % (3275760)Termination phase: Saturation % 5.79/1.09 % (3275760)Time elapsed: 0.082 s % 5.79/1.09 % (3275760)Peak memory usage: 13 MB % 5.79/1.09 % (3275760)Instructions burned: 131 (million) % 5.79/1.09 % (3275775)ott-21_1_sil=16000:fs=off:random_seed=2140472229:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 5.79/1.09 % (3275776)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=409069570:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.79/1.09 % (3275777)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2090660288:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.79/1.09 % (3275777)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.79/1.09 % (3275777)Terminated due to inappropriate strategy. % 5.79/1.09 % (3275777)------------------------------ % 5.79/1.09 % (3275777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.79/1.09 % (3275777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.79/1.09 % (3275777)CaDiCaL version: 2.1.3 % 5.79/1.09 % (3275777)Termination reason: Inappropriate % 5.79/1.09 % (3275777)Time elapsed: 0.001 s % 5.79/1.09 % (3275777)Peak memory usage: 10 MB % 5.79/1.09 % (3275777)Instructions burned: 1 (million) % 5.79/1.09 % (3275777)------------------------------ % 5.79/1.09 % (3275777)------------------------------ % 5.79/1.09 % (3275771)Instruction limit reached! % 5.79/1.09 % (3275771)------------------------------ % 5.79/1.09 % (3275771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.79/1.09 % (3275771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.79/1.09 % (3275771)CaDiCaL version: 2.1.3 % 5.79/1.09 % (3275771)Termination reason: Instruction limit % 5.79/1.09 % (3275771)Termination phase: Saturation % 5.79/1.09 % (3275771)Time elapsed: 0.079 s % 5.79/1.09 % (3275771)Peak memory usage: 12 MB % 5.79/1.09 % (3275771)Instructions burned: 131 (million) % 5.79/1.09 % (3275781)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1234365026:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.79/1.09 % (3275783)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1101341927:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.79/1.09 % (3275783)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.79/1.09 % (3275783)Terminated due to inappropriate strategy. % 5.79/1.09 % (3275783)------------------------------ % 5.79/1.09 % (3275783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.79/1.09 % (3275783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.79/1.09 % (3275783)CaDiCaL version: 2.1.3 % 5.79/1.09 % (3275783)Termination reason: Inappropriate % 5.79/1.09 % (3275783)Time elapsed: 0.001 s % 5.79/1.09 % (3275783)Peak memory usage: 10 MB % 5.79/1.09 % (3275783)Instructions burned: 1 (million) % 5.79/1.09 % (3275783)------------------------------ % 5.79/1.09 % (3275783)------------------------------ % 5.79/1.09 % (3275785)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=3126669735:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 5.79/1.09 % (3275775)Instruction limit reached! % 5.79/1.09 % (3275775)------------------------------ % 5.79/1.09 % (3275775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.79/1.09 % (3275775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.79/1.09 % (3275775)CaDiCaL version: 2.1.3 % 5.79/1.09 % (3275775)Termination reason: Instruction limit % 5.79/1.09 % (3275775)Termination phase: Saturation % 16.95/2.75 % (3275775)Time elapsed: 0.081 s % 16.95/2.75 % (3275775)Peak memory usage: 12 MB % 16.95/2.75 % (3275775)Instructions burned: 181 (million) % 16.95/2.75 % (3275787)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2669733388:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 16.95/2.75 % (3275773)Instruction limit reached! % 16.95/2.75 % (3275773)------------------------------ % 16.95/2.75 % (3275773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.95/2.75 % (3275773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.95/2.75 % (3275773)CaDiCaL version: 2.1.3 % 16.95/2.75 % (3275773)Termination reason: Instruction limit % 16.95/2.75 % (3275773)Termination phase: Saturation % 16.95/2.75 % (3275773)Time elapsed: 0.198 s % 16.95/2.75 % (3275773)Peak memory usage: 17 MB % 16.95/2.75 % (3275773)Instructions burned: 687 (million) % 16.95/2.75 % (3275789)fmb+10_1_sil=64000:random_seed=3443963367:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 16.95/2.75 % (3275789)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.95/2.75 % (3275789)Terminated due to inappropriate strategy. % 16.95/2.75 % (3275789)------------------------------ % 16.95/2.75 % (3275789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.95/2.75 % (3275789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.95/2.75 % (3275789)CaDiCaL version: 2.1.3 % 16.95/2.75 % (3275789)Termination reason: Inappropriate % 16.95/2.75 % (3275789)Time elapsed: 0.0000 s % 16.95/2.75 % (3275789)Peak memory usage: 10 MB % 16.95/2.75 % (3275789)Instructions burned: 1 (million) % 16.95/2.75 % (3275789)------------------------------ % 16.95/2.75 % (3275789)------------------------------ % 16.95/2.75 % (3275791)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2374534818:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 16.95/2.75 % (3275791)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.95/2.75 % (3275791)Terminated due to inappropriate strategy. % 16.95/2.75 % (3275791)------------------------------ % 16.95/2.75 % (3275791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.95/2.75 % (3275791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.95/2.75 % (3275791)CaDiCaL version: 2.1.3 % 16.95/2.75 % (3275791)Termination reason: Inappropriate % 16.95/2.75 % (3275791)Time elapsed: 0.0000 s % 16.95/2.75 % (3275791)Peak memory usage: 10 MB % 16.95/2.75 % (3275791)Instructions burned: 1 (million) % 16.95/2.75 % (3275791)------------------------------ % 16.95/2.75 % (3275791)------------------------------ % 16.95/2.75 % (3275793)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1869782513:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 16.95/2.75 % (3275793)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.95/2.75 % (3275793)Terminated due to inappropriate strategy. % 16.95/2.75 % (3275793)------------------------------ % 16.95/2.75 % (3275793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.95/2.75 % (3275793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.95/2.75 % (3275793)CaDiCaL version: 2.1.3 % 16.95/2.75 % (3275793)Termination reason: Inappropriate % 16.95/2.75 % (3275793)Time elapsed: 0.0000 s % 16.95/2.75 % (3275793)Peak memory usage: 11 MB % 16.95/2.75 % (3275793)Instructions burned: 1 (million) % 16.95/2.75 % (3275793)------------------------------ % 16.95/2.75 % (3275793)------------------------------ % 16.95/2.75 % (3275776)Instruction limit reached! % 16.95/2.75 % (3275776)------------------------------ % 16.95/2.75 % (3275776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.95/2.75 % (3275776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.95/2.75 % (3275776)CaDiCaL version: 2.1.3 % 16.95/2.75 % (3275776)Termination reason: Instruction limit % 16.95/2.75 % (3275776)Termination phase: Saturation % 16.95/2.75 % (3275776)Time elapsed: 0.215 s % 16.95/2.75 % (3275776)Peak memory usage: 12 MB % 16.95/2.75 % (3275776)Instructions burned: 479 (million) % 16.95/2.75 % (3275795)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=49875254:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 16.95/2.75 % (3275796)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2690362320:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 16.95/2.75 % (3275785)Instruction limit reached! % 16.95/2.75 % (3275785)------------------------------ % 28.25/4.21 % (3275785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.25/4.21 % (3275785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.25/4.21 % (3275785)CaDiCaL version: 2.1.3 % 28.25/4.21 % (3275785)Termination reason: Instruction limit % 28.25/4.21 % (3275785)Termination phase: Saturation % 28.25/4.21 % (3275785)Time elapsed: 0.419 s % 28.25/4.21 % (3275785)Peak memory usage: 18 MB % 28.25/4.21 % (3275785)Instructions burned: 693 (million) % 28.25/4.21 % (3275799)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=153419696:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 28.25/4.21 % (3275799)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.25/4.21 % (3275799)Terminated due to inappropriate strategy. % 28.25/4.21 % (3275799)------------------------------ % 28.25/4.21 % (3275799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.25/4.21 % (3275799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.25/4.21 % (3275799)CaDiCaL version: 2.1.3 % 28.25/4.21 % (3275799)Termination reason: Inappropriate % 28.25/4.21 % (3275799)Time elapsed: 0.001 s % 28.25/4.21 % (3275799)Peak memory usage: 10 MB % 28.25/4.21 % (3275799)Instructions burned: 1 (million) % 28.25/4.21 % (3275799)------------------------------ % 28.25/4.21 % (3275799)------------------------------ % 28.25/4.21 % (3275801)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3643960528:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 28.25/4.21 % (3275801)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.25/4.21 % (3275801)Terminated due to inappropriate strategy. % 28.25/4.21 % (3275801)------------------------------ % 28.25/4.21 % (3275801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.25/4.21 % (3275801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.25/4.21 % (3275801)CaDiCaL version: 2.1.3 % 28.25/4.21 % (3275801)Termination reason: Inappropriate % 28.25/4.21 % (3275801)Time elapsed: 0.001 s % 28.25/4.21 % (3275801)Peak memory usage: 10 MB % 28.25/4.21 % (3275801)Instructions burned: 1 (million) % 28.25/4.21 % (3275801)------------------------------ % 28.25/4.21 % (3275801)------------------------------ % 28.25/4.21 % (3275803)ott-2_1_sil=16000:newcnf=on:random_seed=3430276884:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 28.25/4.21 % (3275787)Instruction limit reached! % 28.25/4.21 % (3275787)------------------------------ % 28.25/4.21 % (3275787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.25/4.21 % (3275787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.25/4.21 % (3275787)CaDiCaL version: 2.1.3 % 28.25/4.21 % (3275787)Termination reason: Instruction limit % 28.25/4.21 % (3275787)Termination phase: Saturation % 28.25/4.21 % (3275787)Time elapsed: 0.504 s % 28.25/4.21 % (3275787)Peak memory usage: 19 MB % 28.25/4.21 % (3275787)Instructions burned: 879 (million) % 28.25/4.21 % (3275805)ott+10_1_sil=32000:tgt=ground:random_seed=3477197691:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 28.25/4.21 % (3275781)Instruction limit reached! % 28.25/4.21 % (3275781)------------------------------ % 28.25/4.21 % (3275781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.25/4.21 % (3275781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.25/4.21 % (3275781)CaDiCaL version: 2.1.3 % 28.25/4.21 % (3275781)Termination reason: Instruction limit % 28.25/4.21 % (3275781)Termination phase: Saturation % 28.25/4.21 % (3275781)Time elapsed: 0.698 s % 28.25/4.21 % (3275781)Peak memory usage: 19 MB % 28.25/4.21 % (3275781)Instructions burned: 1180 (million) % 28.25/4.21 % (3275807)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=449630672:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 28.25/4.21 % (3275807)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.25/4.21 % (3275807)Terminated due to inappropriate strategy. % 28.25/4.21 % (3275807)------------------------------ % 28.25/4.21 % (3275807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.25/4.21 % (3275807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.25/4.21 % (3275807)CaDiCaL version: 2.1.3 % 28.25/4.21 % (3275807)Termination reason: Inappropriate % 28.25/4.21 % (3275807)Time elapsed: 0.001 s % 28.25/4.21 % (3275807)Peak memory usage: 10 MB % 28.25/4.21 % (3275807)Instructions burned: 1 (million) % 93.55/13.48 % (3275807)------------------------------ % 93.55/13.48 % (3275807)------------------------------ % 93.55/13.48 % (3275809)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3015890177:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 93.55/13.48 % (3275803)Instruction limit reached! % 93.55/13.48 % (3275803)------------------------------ % 93.55/13.48 % (3275803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.55/13.48 % (3275803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.55/13.48 % (3275803)CaDiCaL version: 2.1.3 % 93.55/13.48 % (3275803)Termination reason: Instruction limit % 93.55/13.48 % (3275803)Termination phase: Saturation % 93.55/13.48 % (3275803)Time elapsed: 0.499 s % 93.55/13.48 % (3275803)Peak memory usage: 15 MB % 93.55/13.48 % (3275803)Instructions burned: 870 (million) % 93.55/13.48 % (3275811)dis+21_1_sil=32000:sas=cadical:random_seed=2437738244:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 93.55/13.48 % (3275796)Instruction limit reached! % 93.55/13.48 % (3275796)------------------------------ % 93.55/13.48 % (3275796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.55/13.48 % (3275796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.55/13.48 % (3275796)CaDiCaL version: 2.1.3 % 93.55/13.48 % (3275796)Termination reason: Instruction limit % 93.55/13.48 % (3275796)Termination phase: Saturation % 93.55/13.48 % (3275796)Time elapsed: 0.884 s % 93.55/13.48 % (3275796)Peak memory usage: 27 MB % 93.55/13.48 % (3275796)Instructions burned: 1472 (million) % 93.55/13.48 % (3275813)ott+11_1_sil=16000:gs=on:random_seed=3767242351:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 93.55/13.48 % (3275795)Instruction limit reached! % 93.55/13.48 % (3275795)------------------------------ % 93.55/13.48 % (3275795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.55/13.48 % (3275795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.55/13.48 % (3275795)CaDiCaL version: 2.1.3 % 93.55/13.48 % (3275795)Termination reason: Instruction limit % 93.55/13.48 % (3275795)Termination phase: Saturation % 93.55/13.48 % (3275795)Time elapsed: 1.476 s % 93.55/13.48 % (3275795)Peak memory usage: 41 MB % 93.55/13.48 % (3275795)Instructions burned: 5133 (million) % 93.55/13.48 % (3275815)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2231855498:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 93.55/13.48 % (3275815)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 93.55/13.48 % (3275815)Terminated due to inappropriate strategy. % 93.55/13.48 % (3275815)------------------------------ % 93.55/13.48 % (3275815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.55/13.48 % (3275815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.55/13.48 % (3275815)CaDiCaL version: 2.1.3 % 93.55/13.48 % (3275815)Termination reason: Inappropriate % 93.55/13.48 % (3275815)Time elapsed: 0.0000 s % 93.55/13.48 % (3275815)Peak memory usage: 10 MB % 93.55/13.48 % (3275815)Instructions burned: 2 (million) % 93.55/13.48 % (3275815)------------------------------ % 93.55/13.48 % (3275815)------------------------------ % 93.55/13.48 % (3275817)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2981768300:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 93.55/13.48 % (3275813)Instruction limit reached! % 93.55/13.48 % (3275813)------------------------------ % 93.55/13.48 % (3275813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.55/13.48 % (3275813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.55/13.48 % (3275813)CaDiCaL version: 2.1.3 % 93.55/13.48 % (3275813)Termination reason: Instruction limit % 93.55/13.48 % (3275813)Termination phase: Saturation % 93.55/13.48 % (3275813)Time elapsed: 1.231 s % 93.55/13.48 % (3275813)Peak memory usage: 23 MB % 93.55/13.48 % (3275813)Instructions burned: 2252 (million) % 93.55/13.48 % (3275819)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=321071157:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 93.55/13.48 % (3275809)Instruction limit reached! % 93.55/13.48 % (3275809)------------------------------ % 93.55/13.48 % (3275809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.55/13.48 % (3275809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.55/13.48 % (3275809)CaDiCaL version: 2.1.3 % 93.55/13.48 % (3275809)Termination reason: Instruction limit % 112.23/16.13 % (3275809)Termination phase: Saturation % 112.23/16.13 % (3275809)Time elapsed: 1.640 s % 112.23/16.13 % (3275809)Peak memory usage: 26 MB % 112.23/16.13 % (3275809)Instructions burned: 3514 (million) % 112.23/16.13 % (3275821)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1120554056:i=5211_2974 on theBenchmark for (2974ds/5211Mi) % 112.23/16.13 % (3275817)Instruction limit reached! % 112.23/16.13 % (3275817)------------------------------ % 112.23/16.13 % (3275817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.23/16.13 % (3275817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.23/16.13 % (3275817)CaDiCaL version: 2.1.3 % 112.23/16.13 % (3275817)Termination reason: Instruction limit % 112.23/16.13 % (3275817)Termination phase: Saturation % 112.23/16.13 % (3275817)Time elapsed: 1.311 s % 112.23/16.13 % (3275817)Peak memory usage: 45 MB % 112.23/16.13 % (3275817)Instructions burned: 4592 (million) % 112.23/16.13 % (3275823)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2213838815:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 112.23/16.13 % (3275823)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 112.23/16.13 % (3275823)Terminated due to inappropriate strategy. % 112.23/16.13 % (3275823)------------------------------ % 112.23/16.13 % (3275823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.23/16.13 % (3275823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.23/16.13 % (3275823)CaDiCaL version: 2.1.3 % 112.23/16.13 % (3275823)Termination reason: Inappropriate % 112.23/16.13 % (3275823)Time elapsed: 0.0000 s % 112.23/16.13 % (3275823)Peak memory usage: 10 MB % 112.23/16.13 % (3275823)Instructions burned: 1 (million) % 112.23/16.13 % (3275823)------------------------------ % 112.23/16.13 % (3275823)------------------------------ % 112.23/16.13 % (3275825)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=995836655:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 112.23/16.13 % (3275825)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 112.23/16.13 % (3275825)Terminated due to inappropriate strategy. % 112.23/16.13 % (3275825)------------------------------ % 112.23/16.13 % (3275825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.23/16.13 % (3275825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.23/16.13 % (3275825)CaDiCaL version: 2.1.3 % 112.23/16.13 % (3275825)Termination reason: Inappropriate % 112.23/16.13 % (3275825)Time elapsed: 0.001 s % 112.23/16.13 % (3275825)Peak memory usage: 11 MB % 112.23/16.13 % (3275825)Instructions burned: 2 (million) % 112.23/16.13 % (3275825)------------------------------ % 112.23/16.13 % (3275825)------------------------------ % 112.23/16.13 % (3275827)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3098404540:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 112.23/16.13 % (3275827)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 112.23/16.13 % (3275827)Terminated due to inappropriate strategy. % 112.23/16.13 % (3275827)------------------------------ % 112.23/16.13 % (3275827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.23/16.13 % (3275827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.23/16.13 % (3275827)CaDiCaL version: 2.1.3 % 112.23/16.13 % (3275827)Termination reason: Inappropriate % 112.23/16.13 % (3275827)Time elapsed: 0.001 s % 112.23/16.13 % (3275827)Peak memory usage: 10 MB % 112.23/16.13 % (3275827)Instructions burned: 2 (million) % 112.23/16.13 % (3275827)------------------------------ % 112.23/16.13 % (3275827)------------------------------ % 112.23/16.13 % (3275829)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=6172788:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi) % 112.23/16.13 % (3275811)Instruction limit reached! % 112.23/16.13 % (3275811)------------------------------ % 112.23/16.13 % (3275811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.23/16.13 % (3275811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.23/16.13 % (3275811)CaDiCaL version: 2.1.3 % 112.23/16.13 % (3275811)Termination reason: Instruction limit % 112.23/16.13 % (3275811)Termination phase: Saturation % 112.23/16.13 % (3275811)Time elapsed: 2.052 s % 112.23/16.13 % (3275811)Peak memory usage: 32 MB % 112.23/16.13 % (3275811)Instructions burned: 3774 (million) % 112.23/16.13 % (3275831)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=830318164:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 112.23/16.13 % (3275805)Instruction limit reached! % 113.41/16.24 % (3275805)------------------------------ % 113.41/16.24 % (3275805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.41/16.24 % (3275805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.41/16.24 % (3275805)CaDiCaL version: 2.1.3 % 113.41/16.24 % (3275805)Termination reason: Instruction limit % 113.41/16.24 % (3275805)Termination phase: Saturation % 113.41/16.24 % (3275805)Time elapsed: 3.253 s % 113.41/16.24 % (3275805)Peak memory usage: 35 MB % 113.41/16.24 % (3275805)Instructions burned: 5115 (million) % 113.41/16.24 % (3275833)dis+10_16:1_sil=16000:random_seed=587256141:i=9155:fsr=off_2959 on theBenchmark for (2959ds/9155Mi) % 113.41/16.24 % (3275821)Instruction limit reached! % 113.41/16.24 % (3275821)------------------------------ % 113.41/16.24 % (3275821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.41/16.24 % (3275821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.41/16.24 % (3275821)CaDiCaL version: 2.1.3 % 113.41/16.24 % (3275821)Termination reason: Instruction limit % 113.41/16.24 % (3275821)Termination phase: Saturation % 113.41/16.24 % (3275821)Time elapsed: 2.477 s % 113.41/16.24 % (3275821)Peak memory usage: 35 MB % 113.41/16.24 % (3275821)Instructions burned: 5212 (million) % 113.41/16.24 % (3275835)ott-3_8_sil=64000:random_seed=2175442224:i=20139:bs=on_2949 on theBenchmark for (2949ds/20139Mi) % 113.41/16.24 % (3275831)Instruction limit reached! % 113.41/16.24 % (3275831)------------------------------ % 113.41/16.24 % (3275831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.41/16.24 % (3275831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.41/16.24 % (3275831)CaDiCaL version: 2.1.3 % 113.41/16.24 % (3275831)Termination reason: Instruction limit % 113.41/16.24 % (3275831)Termination phase: Saturation % 113.41/16.24 % (3275831)Time elapsed: 5.125 s % 113.41/16.24 % (3275831)Peak memory usage: 56 MB % 113.41/16.24 % (3275831)Instructions burned: 8174 (million) % 113.41/16.24 % (3275837)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=253773846:fmbsr=2:i=32576_2915 on theBenchmark for (2915ds/32576Mi) % 113.41/16.24 % (3275837)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.41/16.24 % (3275837)Terminated due to inappropriate strategy. % 113.41/16.24 % (3275837)------------------------------ % 113.41/16.24 % (3275837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.41/16.24 % (3275837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.41/16.24 % (3275837)CaDiCaL version: 2.1.3 % 113.41/16.24 % (3275837)Termination reason: Inappropriate % 113.41/16.24 % (3275837)Time elapsed: 0.001 s % 113.41/16.24 % (3275837)Peak memory usage: 10 MB % 113.41/16.24 % (3275837)Instructions burned: 2 (million) % 113.41/16.24 % (3275837)------------------------------ % 113.41/16.24 % (3275837)------------------------------ % 113.41/16.24 % (3275839)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3370751427:i=11404_2915 on theBenchmark for (2915ds/11404Mi) % 113.41/16.24 % (3275829)Instruction limit reached! % 113.41/16.24 % (3275829)------------------------------ % 113.41/16.24 % (3275829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.41/16.24 % (3275829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.41/16.24 % (3275829)CaDiCaL version: 2.1.3 % 113.41/16.24 % (3275829)Termination reason: Instruction limit % 113.41/16.24 % (3275829)Termination phase: Saturation % 113.41/16.24 % (3275829)Time elapsed: 5.221 s % 113.41/16.24 % (3275829)Peak memory usage: 71 MB % 113.41/16.24 % (3275829)Instructions burned: 22567 (million) % 113.41/16.24 % (3275841)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=269426242:i=14134_2915 on theBenchmark for (2915ds/14134Mi) % 113.41/16.24 % (3275833)Instruction limit reached! % 113.41/16.24 % (3275833)------------------------------ % 113.41/16.24 % (3275833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.41/16.24 % (3275833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.41/16.24 % (3275833)CaDiCaL version: 2.1.3 % 113.41/16.24 % (3275833)Termination reason: Instruction limit % 113.41/16.24 % (3275833)Termination phase: Saturation % 113.41/16.24 % (3275833)Time elapsed: 4.659 s % 113.41/16.24 % (3275833)Peak memory usage: 52 MB % 113.41/16.24 % (3275833)Instructions burned: 9156 (million) % 113.41/16.24 % (3275843)dis+33_16_sil=32000:sac=on:random_seed=398993193:i=15851:nm=0_2913 on theBenchmark for (2913ds/15851Mi) % 113.41/16.24 % (3275841)Instruction limit reached! % 113.41/16.24 % (3275841)------------------------------ % 113.41/16.24 % (3275841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.54/19.10 % (3275841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.54/19.10 % (3275841)CaDiCaL version: 2.1.3 % 133.54/19.10 % (3275841)Termination reason: Instruction limit % 133.54/19.10 % (3275841)Termination phase: Saturation % 133.54/19.10 % (3275841)Time elapsed: 4.790 s % 133.54/19.10 % (3275841)Peak memory usage: 78 MB % 133.54/19.10 % (3275841)Instructions burned: 14136 (million) % 133.54/19.10 % (3275845)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=645387698:avsq=on:i=17627:add=on:amm=off_2867 on theBenchmark for (2867ds/17627Mi) % 133.54/19.10 % (3275819)Instruction limit reached! % 133.54/19.10 % (3275819)------------------------------ % 133.54/19.10 % (3275819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.54/19.10 % (3275819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.54/19.10 % (3275819)CaDiCaL version: 2.1.3 % 133.54/19.10 % (3275819)Termination reason: Instruction limit % 133.54/19.10 % (3275819)Termination phase: Saturation % 133.54/19.10 % (3275819)Time elapsed: 11.853 s % 133.54/19.10 % (3275819)Peak memory usage: 131 MB % 133.54/19.10 % (3275819)Instructions burned: 29342 (million) % 133.54/19.10 % (3275847)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=716047466:s2a=on:i=53295_2856 on theBenchmark for (2856ds/53295Mi) % 133.54/19.10 % (3275839)Instruction limit reached! % 133.54/19.10 % (3275839)------------------------------ % 133.54/19.10 % (3275839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.54/19.10 % (3275839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.54/19.10 % (3275839)CaDiCaL version: 2.1.3 % 133.54/19.10 % (3275839)Termination reason: Instruction limit % 133.54/19.10 % (3275839)Termination phase: Saturation % 133.54/19.10 % (3275839)Time elapsed: 7.184 s % 133.54/19.10 % (3275839)Peak memory usage: 62 MB % 133.54/19.10 % (3275839)Instructions burned: 11404 (million) % 133.54/19.10 % (3275849)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1384932506:i=26857:ins=20_2843 on theBenchmark for (2843ds/26857Mi) % 133.54/19.10 % (3275849)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 133.54/19.10 % (3275849)Terminated due to inappropriate strategy. % 133.54/19.10 % (3275849)------------------------------ % 133.54/19.10 % (3275849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.54/19.10 % (3275849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.54/19.10 % (3275849)CaDiCaL version: 2.1.3 % 133.54/19.10 % (3275849)Termination reason: Inappropriate % 133.54/19.10 % (3275849)Time elapsed: 0.001 s % 133.54/19.10 % (3275849)Peak memory usage: 10 MB % 133.54/19.10 % (3275849)Instructions burned: 1 (million) % 133.54/19.10 % (3275849)------------------------------ % 133.54/19.10 % (3275849)------------------------------ % 133.54/19.10 % (3275851)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3170716873:i=28120:bs=on:fsr=off_2843 on theBenchmark for (2843ds/28120Mi) % 133.54/19.10 % (3275843)Instruction limit reached! % 133.54/19.10 % (3275843)------------------------------ % 133.54/19.10 % (3275843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.54/19.10 % (3275843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.54/19.10 % (3275843)CaDiCaL version: 2.1.3 % 133.54/19.10 % (3275843)Termination reason: Instruction limit % 133.54/19.10 % (3275843)Termination phase: Saturation % 133.54/19.10 % (3275843)Time elapsed: 7.152 s % 133.54/19.10 % (3275843)Peak memory usage: 127 MB % 133.54/19.10 % (3275843)Instructions burned: 15853 (million) % 133.54/19.10 % (3275853)fmb+10_1_sil=256000:fmbss=7:random_seed=878479913:fmbsr=1.6:i=182295_2841 on theBenchmark for (2841ds/182295Mi) % 133.54/19.10 % (3275853)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 133.54/19.10 % (3275853)Terminated due to inappropriate strategy. % 133.54/19.10 % (3275853)------------------------------ % 133.54/19.10 % (3275853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.54/19.10 % (3275853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.54/19.10 % (3275853)CaDiCaL version: 2.1.3 % 133.54/19.10 % (3275853)Termination reason: Inappropriate % 133.54/19.10 % (3275853)Time elapsed: 0.001 s % 133.54/19.10 % (3275853)Peak memory usage: 10 MB % 133.54/19.10 % (3275853)Instructions burned: 1 (million) % 133.54/19.10 % (3275853)------------------------------ % 133.54/19.10 % (3275853)------------------------------ % 133.54/19.10 % (3275855)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1147310013:i=44625:gsp=on_2841 on theBenchmark for (2841ds/44625Mi) % 139.51/20.01 % (3275855)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 139.51/20.01 % (3275855)Terminated due to inappropriate strategy. % 139.51/20.01 % (3275855)------------------------------ % 139.51/20.01 % (3275855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.51/20.01 % (3275855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.51/20.01 % (3275855)CaDiCaL version: 2.1.3 % 139.51/20.01 % (3275855)Termination reason: Inappropriate % 139.51/20.01 % (3275855)Time elapsed: 0.001 s % 139.51/20.01 % (3275855)Peak memory usage: 11 MB % 139.51/20.01 % (3275855)Instructions burned: 1 (million) % 139.51/20.01 % (3275855)------------------------------ % 139.51/20.01 % (3275855)------------------------------ % 139.51/20.01 % (3275857)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1198113317:i=160505_2840 on theBenchmark for (2840ds/160505Mi) % 139.51/20.01 % (3275857)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 139.51/20.01 % (3275857)Terminated due to inappropriate strategy. % 139.51/20.01 % (3275857)------------------------------ % 139.51/20.01 % (3275857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.51/20.01 % (3275857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.51/20.01 % (3275857)CaDiCaL version: 2.1.3 % 139.51/20.01 % (3275857)Termination reason: Inappropriate % 139.51/20.01 % (3275857)Time elapsed: 0.001 s % 139.51/20.01 % (3275857)Peak memory usage: 11 MB % 139.51/20.01 % (3275857)Instructions burned: 1 (million) % 139.51/20.01 % (3275857)------------------------------ % 139.51/20.01 % (3275857)------------------------------ % 139.51/20.01 % (3275859)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3194193646:fmbsr=1.3:i=225729_2840 on theBenchmark for (2840ds/225729Mi) % 139.51/20.01 % (3275859)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 139.51/20.01 % (3275859)Terminated due to inappropriate strategy. % 139.51/20.01 % (3275859)------------------------------ % 139.51/20.01 % (3275859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.51/20.01 % (3275859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.51/20.01 % (3275859)CaDiCaL version: 2.1.3 % 139.51/20.01 % (3275859)Termination reason: Inappropriate % 139.51/20.01 % (3275859)Time elapsed: 0.001 s % 139.51/20.01 % (3275859)Peak memory usage: 10 MB % 139.51/20.01 % (3275859)Instructions burned: 2 (million) % 139.51/20.01 % (3275859)------------------------------ % 139.51/20.01 % (3275859)------------------------------ % 139.51/20.01 % (3275861)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3376633610:fmbsr=2:i=185024:ins=7_2840 on theBenchmark for (2840ds/185024Mi) % 139.51/20.01 % (3275861)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 139.51/20.01 % (3275861)Terminated due to inappropriate strategy. % 139.51/20.01 % (3275861)------------------------------ % 139.51/20.01 % (3275861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.51/20.01 % (3275861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.51/20.01 % (3275861)CaDiCaL version: 2.1.3 % 139.51/20.01 % (3275861)Termination reason: Inappropriate % 139.51/20.01 % (3275861)Time elapsed: 0.001 s % 139.51/20.01 % (3275861)Peak memory usage: 11 MB % 139.51/20.01 % (3275861)Instructions burned: 2 (million) % 139.51/20.01 % (3275861)------------------------------ % 139.51/20.01 % (3275861)------------------------------ % 139.51/20.01 % (3275863)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=789502908:rtra=on_2840 on theBenchmark for (2840ds/0Mi) % 139.51/20.01 % (3275863)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 139.51/20.01 % (3275863)Terminated due to inappropriate strategy. % 139.51/20.01 % (3275863)------------------------------ % 139.51/20.01 % (3275863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.51/20.01 % (3275863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.51/20.01 % (3275863)CaDiCaL version: 2.1.3 % 139.51/20.01 % (3275863)Termination reason: Inappropriate % 139.51/20.01 % (3275863)Time elapsed: 0.001 s % 139.51/20.01 % (3275863)Peak memory usage: 10 MB % 139.51/20.01 % (3275863)Instructions burned: 1 (million) % 139.51/20.01 % (3275863)------------------------------ % 139.51/20.01 % (3275863)------------------------------ % 139.51/20.01 % (3275865)% WARNING: option uhcvi not known. % 139.51/20.01 % (3275865)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3509058939:i=271062:add=off:rtra=on:rawr=on_2839 on theBenchmark for (2839ds/271062Mi) % 151.93/21.73 % (3275835)Instruction limit reached! % 151.93/21.73 % (3275835)------------------------------ % 151.93/21.73 % (3275835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.93/21.73 % (3275835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.93/21.73 % (3275835)CaDiCaL version: 2.1.3 % 151.93/21.73 % (3275835)Termination reason: Instruction limit % 151.93/21.73 % (3275835)Termination phase: Saturation % 151.93/21.73 % (3275835)Time elapsed: 11.420 s % 151.93/21.73 % (3275835)Peak memory usage: 65 MB % 151.93/21.73 % (3275835)Instructions burned: 20140 (million) % 151.93/21.73 % (3275867)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3716303542:i=176048:add=on:rtra=on:rawr=on_2835 on theBenchmark for (2835ds/176048Mi) % 151.93/21.73 % (3275845)Instruction limit reached! % 151.93/21.73 % (3275845)------------------------------ % 151.93/21.73 % (3275845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.93/21.73 % (3275845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.93/21.73 % (3275845)CaDiCaL version: 2.1.3 % 151.93/21.73 % (3275845)Termination reason: Instruction limit % 151.93/21.73 % (3275845)Termination phase: Saturation % 151.93/21.73 % (3275845)Time elapsed: 5.195 s % 151.93/21.73 % (3275845)Peak memory usage: 94 MB % 151.93/21.73 % (3275845)Instructions burned: 17630 (million) % 151.93/21.73 % (3275870)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1482834825:i=206:fgj=on:rtra=on_2815 on theBenchmark for (2815ds/206Mi) % 151.93/21.73 % (3275870)Instruction limit reached! % 151.93/21.73 % (3275870)------------------------------ % 151.93/21.73 % (3275870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.93/21.73 % (3275870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.93/21.73 % (3275870)CaDiCaL version: 2.1.3 % 151.93/21.73 % (3275870)Termination reason: Instruction limit % 151.93/21.73 % (3275870)Termination phase: Saturation % 151.93/21.73 % (3275870)Time elapsed: 0.067 s % 151.93/21.73 % (3275870)Peak memory usage: 13 MB % 151.93/21.73 % (3275870)Instructions burned: 207 (million) % 151.93/21.73 % (3275872)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=177269349:i=232:rtra=on_2814 on theBenchmark for (2814ds/232Mi) % 151.93/21.73 % (3275872)Instruction limit reached! % 151.93/21.73 % (3275872)------------------------------ % 151.93/21.73 % (3275872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.93/21.73 % (3275872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.93/21.73 % (3275872)CaDiCaL version: 2.1.3 % 151.93/21.73 % (3275872)Termination reason: Instruction limit % 151.93/21.73 % (3275872)Termination phase: Saturation % 151.93/21.73 % (3275872)Time elapsed: 0.078 s % 151.93/21.73 % (3275872)Peak memory usage: 13 MB % 151.93/21.73 % (3275872)Instructions burned: 232 (million) % 151.93/21.73 % (3275874)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=614437788:i=262:rtra=on_2813 on theBenchmark for (2813ds/262Mi) % 151.93/21.73 % (3275874)Instruction limit reached! % 151.93/21.73 % (3275874)------------------------------ % 151.93/21.73 % (3275874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.93/21.73 % (3275874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.93/21.73 % (3275874)CaDiCaL version: 2.1.3 % 151.93/21.73 % (3275874)Termination reason: Instruction limit % 151.93/21.73 % (3275874)Termination phase: Saturation % 151.93/21.73 % (3275874)Time elapsed: 0.085 s % 151.93/21.73 % (3275874)Peak memory usage: 14 MB % 151.93/21.73 % (3275874)Instructions burned: 263 (million) % 151.93/21.73 % (3275876)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=659747711:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2812 on theBenchmark for (2812ds/318Mi) % 151.93/21.73 % (3275876)Instruction limit reached! % 151.93/21.73 % (3275876)------------------------------ % 151.93/21.73 % (3275876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.93/21.73 % (3275876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.93/21.73 % (3275876)CaDiCaL version: 2.1.3 % 151.93/21.73 % (3275876)Termination reason: Instruction limit % 151.93/21.73 % (3275876)Termination phase: Saturation % 151.93/21.73 % (3275876)Time elapsed: 0.114 s % 151.93/21.73 % (3275876)Peak memory usage: 15 MB % 151.93/21.73 % (3275876)Instructions burned: 319 (million) % 151.93/21.73 % (3275878)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2461121441:i=1428:nm=2:rtra=on_2811 on theBenchmark for (2811ds/1428Mi) % 181.37/25.98 % (3275878)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 181.37/25.98 % (3275878)Terminated due to inappropriate strategy. % 181.37/25.98 % (3275878)------------------------------ % 181.37/25.98 % (3275878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.37/25.98 % (3275878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.37/25.98 % (3275878)CaDiCaL version: 2.1.3 % 181.37/25.98 % (3275878)Termination reason: Inappropriate % 181.37/25.98 % (3275878)Time elapsed: 0.0000 s % 181.37/25.98 % (3275878)Peak memory usage: 10 MB % 181.37/25.98 % (3275878)Instructions burned: 2 (million) % 181.37/25.98 % (3275878)------------------------------ % 181.37/25.98 % (3275878)------------------------------ % 181.37/25.98 % (3275880)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3921601390:i=262:bd=preordered:rtra=on:fsd=on_2811 on theBenchmark for (2811ds/262Mi) % 181.37/25.98 % (3275880)Instruction limit reached! % 181.37/25.98 % (3275880)------------------------------ % 181.37/25.98 % (3275880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.37/25.98 % (3275880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.37/25.98 % (3275880)CaDiCaL version: 2.1.3 % 181.37/25.98 % (3275880)Termination reason: Instruction limit % 181.37/25.98 % (3275880)Termination phase: Saturation % 181.37/25.98 % (3275880)Time elapsed: 0.083 s % 181.37/25.98 % (3275880)Peak memory usage: 13 MB % 181.37/25.98 % (3275880)Instructions burned: 264 (million) % 181.37/25.98 % (3275882)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=1599028236:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2810 on theBenchmark for (2810ds/1368Mi) % 181.37/25.98 % (3275882)Instruction limit reached! % 181.37/25.98 % (3275882)------------------------------ % 181.37/25.98 % (3275882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.37/25.98 % (3275882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.37/25.98 % (3275882)CaDiCaL version: 2.1.3 % 181.37/25.98 % (3275882)Termination reason: Instruction limit % 181.37/25.98 % (3275882)Termination phase: Saturation % 181.37/25.98 % (3275882)Time elapsed: 0.398 s % 181.37/25.98 % (3275882)Peak memory usage: 23 MB % 181.37/25.98 % (3275882)Instructions burned: 1369 (million) % 181.37/25.98 % (3275884)ott-21_1_sil=16000:si=on:fs=off:random_seed=295636747:i=360:av=off:fsr=off:rtra=on_2806 on theBenchmark for (2806ds/360Mi) % 181.37/25.98 % (3275884)Instruction limit reached! % 181.37/25.98 % (3275884)------------------------------ % 181.37/25.98 % (3275884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.37/25.98 % (3275884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.37/25.98 % (3275884)CaDiCaL version: 2.1.3 % 181.37/25.98 % (3275884)Termination reason: Instruction limit % 181.37/25.98 % (3275884)Termination phase: Saturation % 181.37/25.98 % (3275884)Time elapsed: 0.087 s % 181.37/25.98 % (3275884)Peak memory usage: 13 MB % 181.37/25.98 % (3275884)Instructions burned: 363 (million) % 181.37/25.98 % (3275886)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2202223049:i=954:bd=all:rtra=on_2805 on theBenchmark for (2805ds/954Mi) % 181.37/25.98 % (3275886)Instruction limit reached! % 181.37/25.98 % (3275886)------------------------------ % 181.37/25.98 % (3275886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.37/25.98 % (3275886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.37/25.98 % (3275886)CaDiCaL version: 2.1.3 % 181.37/25.98 % (3275886)Termination reason: Instruction limit % 181.37/25.98 % (3275886)Termination phase: Saturation % 181.37/25.98 % (3275886)Time elapsed: 0.281 s % 181.37/25.98 % (3275886)Peak memory usage: 14 MB % 181.37/25.98 % (3275886)Instructions burned: 958 (million) % 181.37/25.98 % (3275888)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2003821758:fmbsr=1.3:i=1730:ins=25:rtra=on_2802 on theBenchmark for (2802ds/1730Mi) % 181.37/25.98 % (3275888)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 181.37/25.98 % (3275888)Terminated due to inappropriate strategy. % 181.37/25.98 % (3275888)------------------------------ % 181.37/25.98 % (3275888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.37/25.98 % (3275888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.37/25.98 % (3275888)CaDiCaL version: 2.1.3 % 181.37/25.98 % (3275888)Termination reason: Inappropriate % 181.37/25.98 % (3275888)Time elapsed: 0.0000 s % 227.00/32.28 % (3275888)Peak memory usage: 10 MB % 227.00/32.28 % (3275888)Instructions burned: 1 (million) % 227.00/32.28 % (3275888)------------------------------ % 227.00/32.28 % (3275888)------------------------------ % 227.00/32.28 % (3275890)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3587654818:i=2358:rtra=on_2802 on theBenchmark for (2802ds/2358Mi) % 227.00/32.28 % (3275890)Instruction limit reached! % 227.00/32.28 % (3275890)------------------------------ % 227.00/32.28 % (3275890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.00/32.28 % (3275890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.00/32.28 % (3275890)CaDiCaL version: 2.1.3 % 227.00/32.28 % (3275890)Termination reason: Instruction limit % 227.00/32.28 % (3275890)Termination phase: Saturation % 227.00/32.28 % (3275890)Time elapsed: 0.654 s % 227.00/32.28 % (3275890)Peak memory usage: 20 MB % 227.00/32.28 % (3275890)Instructions burned: 2361 (million) % 227.00/32.28 % (3275892)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3895456273:i=1778:ins=1:rtra=on_2795 on theBenchmark for (2795ds/1778Mi) % 227.00/32.28 % (3275892)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.00/32.28 % (3275892)Terminated due to inappropriate strategy. % 227.00/32.28 % (3275892)------------------------------ % 227.00/32.28 % (3275892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.00/32.28 % (3275892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.00/32.28 % (3275892)CaDiCaL version: 2.1.3 % 227.00/32.28 % (3275892)Termination reason: Inappropriate % 227.00/32.28 % (3275892)Time elapsed: 0.0000 s % 227.00/32.28 % (3275892)Peak memory usage: 10 MB % 227.00/32.28 % (3275892)Instructions burned: 1 (million) % 227.00/32.28 % (3275892)------------------------------ % 227.00/32.28 % (3275892)------------------------------ % 227.00/32.28 % (3275894)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=2618026277:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2795 on theBenchmark for (2795ds/1384Mi) % 227.00/32.28 % (3275894)Instruction limit reached! % 227.00/32.28 % (3275894)------------------------------ % 227.00/32.28 % (3275894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.00/32.28 % (3275894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.00/32.28 % (3275894)CaDiCaL version: 2.1.3 % 227.00/32.28 % (3275894)Termination reason: Instruction limit % 227.00/32.28 % (3275894)Termination phase: Saturation % 227.00/32.28 % (3275894)Time elapsed: 0.437 s % 227.00/32.28 % (3275894)Peak memory usage: 27 MB % 227.00/32.28 % (3275894)Instructions burned: 1386 (million) % 227.00/32.28 % (3275896)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=334741034:i=1758:kws=inv_precedence:fsr=off:rtra=on_2790 on theBenchmark for (2790ds/1758Mi) % 227.00/32.28 % (3275896)Instruction limit reached! % 227.00/32.28 % (3275896)------------------------------ % 227.00/32.28 % (3275896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.00/32.28 % (3275896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.00/32.28 % (3275896)CaDiCaL version: 2.1.3 % 227.00/32.28 % (3275896)Termination reason: Instruction limit % 227.00/32.28 % (3275896)Termination phase: Saturation % 227.00/32.28 % (3275896)Time elapsed: 0.555 s % 227.00/32.28 % (3275896)Peak memory usage: 28 MB % 227.00/32.28 % (3275896)Instructions burned: 1760 (million) % 227.00/32.28 % (3275898)fmb+10_1_sil=64000:si=on:random_seed=1424006781:i=44122:nm=2:rtra=on:gsp=on_2785 on theBenchmark for (2785ds/44122Mi) % 227.00/32.28 % (3275898)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.00/32.28 % (3275898)Terminated due to inappropriate strategy. % 227.00/32.28 % (3275898)------------------------------ % 227.00/32.28 % (3275898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.00/32.28 % (3275898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.00/32.28 % (3275898)CaDiCaL version: 2.1.3 % 227.00/32.28 % (3275898)Termination reason: Inappropriate % 227.00/32.28 % (3275898)Time elapsed: 0.001 s % 227.00/32.28 % (3275898)Peak memory usage: 10 MB % 227.00/32.28 % (3275898)Instructions burned: 2 (million) % 227.00/32.28 % (3275898)------------------------------ % 227.00/32.28 % (3275898)------------------------------ % 227.00/32.28 % (3275900)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=4081487832:i=19030:nm=5:rtra=on_2784 on theBenchmark for (2784ds/19030Mi) % 268.79/38.51 % (3275900)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 268.79/38.51 % (3275900)Terminated due to inappropriate strategy. % 268.79/38.51 % (3275900)------------------------------ % 268.79/38.51 % (3275900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.79/38.51 % (3275900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.79/38.51 % (3275900)CaDiCaL version: 2.1.3 % 268.79/38.51 % (3275900)Termination reason: Inappropriate % 268.79/38.51 % (3275900)Time elapsed: 0.0000 s % 268.79/38.51 % (3275900)Peak memory usage: 10 MB % 268.79/38.51 % (3275900)Instructions burned: 1 (million) % 268.79/38.51 % (3275900)------------------------------ % 268.79/38.51 % (3275900)------------------------------ % 268.79/38.51 % (3275902)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1446042626:fmbsr=1.7:i=1840:rtra=on_2784 on theBenchmark for (2784ds/1840Mi) % 268.79/38.51 % (3275902)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 268.79/38.51 % (3275902)Terminated due to inappropriate strategy. % 268.79/38.51 % (3275902)------------------------------ % 268.79/38.51 % (3275902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.79/38.51 % (3275902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.79/38.51 % (3275902)CaDiCaL version: 2.1.3 % 268.79/38.51 % (3275902)Termination reason: Inappropriate % 268.79/38.51 % (3275902)Time elapsed: 0.001 s % 268.79/38.51 % (3275902)Peak memory usage: 11 MB % 268.79/38.51 % (3275902)Instructions burned: 1 (million) % 268.79/38.51 % (3275902)------------------------------ % 268.79/38.51 % (3275902)------------------------------ % 268.79/38.51 % (3275904)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=4157794855:i=10262:rtra=on_2784 on theBenchmark for (2784ds/10262Mi) % 268.79/38.51 % (3275904)Instruction limit reached! % 268.79/38.51 % (3275904)------------------------------ % 268.79/38.51 % (3275904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.79/38.51 % (3275904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.79/38.51 % (3275904)CaDiCaL version: 2.1.3 % 268.79/38.51 % (3275904)Termination reason: Instruction limit % 268.79/38.51 % (3275904)Termination phase: Saturation % 268.79/38.51 % (3275904)Time elapsed: 3.225 s % 268.79/38.51 % (3275904)Peak memory usage: 68 MB % 268.79/38.51 % (3275904)Instructions burned: 10268 (million) % 268.79/38.51 % (3275906)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=196595888:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2752 on theBenchmark for (2752ds/2944Mi) % 268.79/38.51 % (3275906)Instruction limit reached! % 268.79/38.51 % (3275906)------------------------------ % 268.79/38.51 % (3275906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.79/38.51 % (3275906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.79/38.51 % (3275906)CaDiCaL version: 2.1.3 % 268.79/38.51 % (3275906)Termination reason: Instruction limit % 268.79/38.51 % (3275906)Termination phase: Saturation % 268.79/38.51 % (3275906)Time elapsed: 0.937 s % 268.79/38.51 % (3275906)Peak memory usage: 40 MB % 268.79/38.51 % (3275906)Instructions burned: 2947 (million) % 268.79/38.51 % (3275908)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3740980331:i=12648:rtra=on_2742 on theBenchmark for (2742ds/12648Mi) % 268.79/38.51 % (3275908)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 268.79/38.51 % (3275908)Terminated due to inappropriate strategy. % 268.79/38.51 % (3275908)------------------------------ % 268.79/38.51 % (3275908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.79/38.51 % (3275908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.79/38.51 % (3275908)CaDiCaL version: 2.1.3 % 268.79/38.51 % (3275908)Termination reason: Inappropriate % 268.79/38.51 % (3275908)Time elapsed: 0.0000 s % 268.79/38.51 % (3275908)Peak memory usage: 10 MB % 268.79/38.51 % (3275908)Instructions burned: 1 (million) % 268.79/38.51 % (3275908)------------------------------ % 268.79/38.51 % (3275908)------------------------------ % 268.79/38.51 % (3275910)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1287557547:fmbsr=2.30978:i=4348:rtra=on_2742 on theBenchmark for (2742ds/4348Mi) % 268.79/38.51 % (3275910)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 268.79/38.51 % (3275910)Terminated due to inappropriate strategy. % 268.79/38.51 % (3275910)------------------------------ % 268.79/38.51 % (3275910)Version: Terminated % 300.11/42.54 % Vampire exiting %------------------------------------------------------------------------------