%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW744_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:42 PM UTC 2026 % Result : Timeout 300.31s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW744_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 % Computer : n017.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 14:24:06 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.88/0.88 % (3593062)Will run a generic schedule for satisfiability detection. % 3.88/0.88 % (3593069)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1874817179:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.88/0.88 % (3593068)% WARNING: option uhcvi not known. % 3.88/0.88 % (3593067)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=133751441_2999 on theBenchmark for (2999ds/0Mi) % 3.88/0.88 % (3593068)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2651581797:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.88/0.88 % (3593070)dis+10_1_sil=32000:sp=arity:random_seed=3509104931:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.88/0.88 % (3593072)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1322405486:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.88/0.88 % (3593073)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=47135650:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.88/0.88 % (3593071)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=145598555:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.88/0.88 % (3593070)Instruction limit reached! % 3.88/0.88 % (3593070)------------------------------ % 3.88/0.88 % (3593070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.88/0.88 % (3593070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.88/0.88 % (3593070)CaDiCaL version: 2.1.3 % 3.88/0.88 % (3593070)Termination reason: Instruction limit % 3.88/0.88 % (3593070)Termination phase: Saturation % 3.88/0.88 % (3593070)Time elapsed: 0.051 s % 3.88/0.88 % (3593070)Peak memory usage: 15 MB % 3.88/0.88 % (3593070)Instructions burned: 103 (million) % 3.88/0.88 % (3593071)Instruction limit reached! % 3.88/0.88 % (3593071)------------------------------ % 3.88/0.88 % (3593071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.88/0.88 % (3593071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.88/0.88 % (3593071)CaDiCaL version: 2.1.3 % 3.88/0.88 % (3593071)Termination reason: Instruction limit % 3.88/0.88 % (3593071)Termination phase: Blocked clause elimination % 3.88/0.88 % (3593071)Time elapsed: 0.056 s % 3.88/0.88 % (3593071)Peak memory usage: 12 MB % 3.88/0.88 % (3593071)Instructions burned: 123 (million) % 3.88/0.88 % (3593072)Instruction limit reached! % 3.88/0.88 % (3593072)------------------------------ % 3.88/0.88 % (3593072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.88/0.88 % (3593072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.88/0.88 % (3593072)CaDiCaL version: 2.1.3 % 3.88/0.88 % (3593072)Termination reason: Instruction limit % 3.88/0.88 % (3593072)Termination phase: Saturation % 3.88/0.88 % (3593072)Time elapsed: 0.067 s % 3.88/0.88 % (3593072)Peak memory usage: 16 MB % 3.88/0.88 % (3593072)Instructions burned: 131 (million) % 3.88/0.88 % (3593105)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=130640617:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 3.88/0.88 % (3593109)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4260925268:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 3.88/0.88 % (3593073)Instruction limit reached! % 3.88/0.88 % (3593073)------------------------------ % 3.88/0.88 % (3593073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.88/0.88 % (3593073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.88/0.88 % (3593073)CaDiCaL version: 2.1.3 % 3.88/0.88 % (3593073)Termination reason: Instruction limit % 3.88/0.88 % (3593073)Termination phase: Saturation % 3.88/0.88 % (3593073)Time elapsed: 0.083 s % 3.88/0.88 % (3593073)Peak memory usage: 16 MB % 3.88/0.88 % (3593073)Instructions burned: 159 (million) % 3.88/0.88 % (3593116)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=1898773016:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 3.88/0.88 % (3593105)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.88/0.88 % (3593105)Terminated due to inappropriate strategy. % 3.88/0.88 % (3593105)------------------------------ % 3.88/0.88 % (3593105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.88/0.88 % (3593105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.88/0.88 % (3593105)CaDiCaL version: 2.1.3 % 6.49/1.25 % (3593105)Termination reason: Inappropriate % 6.49/1.25 % (3593105)Time elapsed: 0.023 s % 6.49/1.25 % (3593105)Peak memory usage: 12 MB % 6.49/1.25 % (3593105)Instructions burned: 53 (million) % 6.49/1.25 % (3593067)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.49/1.25 % (3593067)Terminated due to inappropriate strategy. % 6.49/1.25 % (3593067)------------------------------ % 6.49/1.25 % (3593067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.49/1.25 % (3593067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.49/1.25 % (3593067)CaDiCaL version: 2.1.3 % 6.49/1.25 % (3593067)Termination reason: Inappropriate % 6.49/1.25 % (3593067)Time elapsed: 0.098 s % 6.49/1.25 % (3593067)Peak memory usage: 13 MB % 6.49/1.25 % (3593067)Instructions burned: 203 (million) % 6.49/1.25 % (3593105)------------------------------ % 6.49/1.25 % (3593105)------------------------------ % 6.49/1.25 % (3593067)------------------------------ % 6.49/1.25 % (3593067)------------------------------ % 6.49/1.25 % (3593128)ott-21_1_sil=16000:fs=off:random_seed=2746133773:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.49/1.25 % (3593132)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3879753277:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.49/1.25 % (3593134)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4018717624:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.49/1.25 % (3593109)Instruction limit reached! % 6.49/1.25 % (3593109)------------------------------ % 6.49/1.25 % (3593109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.49/1.25 % (3593109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.49/1.25 % (3593109)CaDiCaL version: 2.1.3 % 6.49/1.25 % (3593109)Termination reason: Instruction limit % 6.49/1.25 % (3593109)Termination phase: Blocked clause elimination % 6.49/1.25 % (3593109)Time elapsed: 0.061 s % 6.49/1.25 % (3593109)Peak memory usage: 12 MB % 6.49/1.25 % (3593109)Instructions burned: 131 (million) % 6.49/1.25 % (3593134)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.49/1.25 % (3593134)Terminated due to inappropriate strategy. % 6.49/1.25 % (3593134)------------------------------ % 6.49/1.25 % (3593134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.49/1.25 % (3593134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.49/1.25 % (3593134)CaDiCaL version: 2.1.3 % 6.49/1.25 % (3593134)Termination reason: Inappropriate % 6.49/1.25 % (3593134)Time elapsed: 0.032 s % 6.49/1.25 % (3593134)Peak memory usage: 13 MB % 6.49/1.25 % (3593134)Instructions burned: 70 (million) % 6.49/1.25 % (3593134)------------------------------ % 6.49/1.25 % (3593134)------------------------------ % 6.49/1.25 % (3593140)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=939601594:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.49/1.25 % (3593141)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1388610647:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 6.49/1.25 % (3593128)Instruction limit reached! % 6.49/1.25 % (3593128)------------------------------ % 6.49/1.25 % (3593128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.49/1.25 % (3593128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.49/1.25 % (3593128)CaDiCaL version: 2.1.3 % 6.49/1.25 % (3593128)Termination reason: Instruction limit % 6.49/1.25 % (3593128)Termination phase: Saturation % 6.49/1.25 % (3593128)Time elapsed: 0.086 s % 6.49/1.25 % (3593128)Peak memory usage: 14 MB % 6.49/1.25 % (3593128)Instructions burned: 181 (million) % 6.49/1.25 % (3593141)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.49/1.25 % (3593141)Terminated due to inappropriate strategy. % 6.49/1.25 % (3593141)------------------------------ % 6.49/1.25 % (3593141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.49/1.25 % (3593141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.49/1.25 % (3593141)CaDiCaL version: 2.1.3 % 6.49/1.25 % (3593141)Termination reason: Inappropriate % 6.49/1.25 % (3593141)Time elapsed: 0.025 s % 6.49/1.25 % (3593141)Peak memory usage: 12 MB % 6.49/1.25 % (3593141)Instructions burned: 58 (million) % 6.49/1.25 % (3593141)------------------------------ % 6.49/1.25 % (3593141)------------------------------ % 6.49/1.25 % (3593144)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=2371973828:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 22.03/3.48 % (3593145)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3672300941:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.03/3.48 % (3593132)Instruction limit reached! % 22.03/3.48 % (3593132)------------------------------ % 22.03/3.48 % (3593132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.03/3.48 % (3593132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.03/3.48 % (3593132)CaDiCaL version: 2.1.3 % 22.03/3.48 % (3593132)Termination reason: Instruction limit % 22.03/3.48 % (3593132)Termination phase: Saturation % 22.03/3.48 % (3593132)Time elapsed: 0.262 s % 22.03/3.48 % (3593132)Peak memory usage: 16 MB % 22.03/3.48 % (3593132)Instructions burned: 478 (million) % 22.03/3.48 % (3593148)fmb+10_1_sil=64000:random_seed=2656726431:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 22.03/3.48 % (3593148)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.03/3.48 % (3593148)Terminated due to inappropriate strategy. % 22.03/3.48 % (3593148)------------------------------ % 22.03/3.48 % (3593148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.03/3.48 % (3593148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.03/3.48 % (3593148)CaDiCaL version: 2.1.3 % 22.03/3.48 % (3593148)Termination reason: Inappropriate % 22.03/3.48 % (3593148)Time elapsed: 0.024 s % 22.03/3.48 % (3593148)Peak memory usage: 12 MB % 22.03/3.48 % (3593148)Instructions burned: 57 (million) % 22.03/3.48 % (3593148)------------------------------ % 22.03/3.48 % (3593148)------------------------------ % 22.03/3.48 % (3593150)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1705005649:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 22.03/3.48 % (3593150)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.03/3.48 % (3593150)Terminated due to inappropriate strategy. % 22.03/3.48 % (3593150)------------------------------ % 22.03/3.48 % (3593150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.03/3.48 % (3593150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.03/3.48 % (3593150)CaDiCaL version: 2.1.3 % 22.03/3.48 % (3593150)Termination reason: Inappropriate % 22.03/3.48 % (3593150)Time elapsed: 0.023 s % 22.03/3.48 % (3593150)Peak memory usage: 11 MB % 22.03/3.48 % (3593150)Instructions burned: 54 (million) % 22.03/3.48 % (3593150)------------------------------ % 22.03/3.48 % (3593150)------------------------------ % 22.03/3.48 % (3593116)Instruction limit reached! % 22.03/3.48 % (3593116)------------------------------ % 22.03/3.48 % (3593116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.03/3.48 % (3593116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.03/3.48 % (3593116)CaDiCaL version: 2.1.3 % 22.03/3.48 % (3593116)Termination reason: Instruction limit % 22.03/3.48 % (3593116)Termination phase: Saturation % 22.03/3.48 % (3593116)Time elapsed: 0.383 s % 22.03/3.48 % (3593116)Peak memory usage: 20 MB % 22.03/3.48 % (3593116)Instructions burned: 684 (million) % 22.03/3.48 % (3593152)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=181473216:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 22.03/3.48 % (3593153)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1771302621:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 22.03/3.48 % (3593152)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.03/3.48 % (3593152)Terminated due to inappropriate strategy. % 22.03/3.48 % (3593152)------------------------------ % 22.03/3.48 % (3593152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.03/3.48 % (3593152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.03/3.48 % (3593152)CaDiCaL version: 2.1.3 % 22.03/3.48 % (3593152)Termination reason: Inappropriate % 22.03/3.48 % (3593152)Time elapsed: 0.024 s % 22.03/3.48 % (3593152)Peak memory usage: 11 MB % 22.03/3.48 % (3593152)Instructions burned: 58 (million) % 22.03/3.48 % (3593152)------------------------------ % 22.03/3.48 % (3593152)------------------------------ % 22.03/3.48 % (3593156)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1234061727:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 22.03/3.48 % (3593145)Instruction limit reached! % 27.56/4.16 % (3593145)------------------------------ % 27.56/4.16 % (3593145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.56/4.16 % (3593145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.56/4.16 % (3593145)CaDiCaL version: 2.1.3 % 27.56/4.16 % (3593145)Termination reason: Instruction limit % 27.56/4.16 % (3593145)Termination phase: Saturation % 27.56/4.16 % (3593145)Time elapsed: 0.381 s % 27.56/4.16 % (3593145)Peak memory usage: 20 MB % 27.56/4.16 % (3593145)Instructions burned: 879 (million) % 27.56/4.16 % (3593144)Instruction limit reached! % 27.56/4.16 % (3593144)------------------------------ % 27.56/4.16 % (3593144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.56/4.16 % (3593144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.56/4.16 % (3593144)CaDiCaL version: 2.1.3 % 27.56/4.16 % (3593144)Termination reason: Instruction limit % 27.56/4.16 % (3593144)Termination phase: Saturation % 27.56/4.16 % (3593144)Time elapsed: 0.410 s % 27.56/4.16 % (3593144)Peak memory usage: 21 MB % 27.56/4.16 % (3593144)Instructions burned: 693 (million) % 27.56/4.16 % (3593158)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3435752896:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 27.56/4.16 % (3593160)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2170243804:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 27.56/4.16 % (3593160)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.56/4.16 % (3593160)Terminated due to inappropriate strategy. % 27.56/4.16 % (3593160)------------------------------ % 27.56/4.16 % (3593160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.56/4.16 % (3593160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.56/4.16 % (3593160)CaDiCaL version: 2.1.3 % 27.56/4.16 % (3593160)Termination reason: Inappropriate % 27.56/4.16 % (3593160)Time elapsed: 0.024 s % 27.56/4.16 % (3593160)Peak memory usage: 11 MB % 27.56/4.16 % (3593160)Instructions burned: 58 (million) % 27.56/4.16 % (3593160)------------------------------ % 27.56/4.16 % (3593160)------------------------------ % 27.56/4.16 % (3593162)ott-2_1_sil=16000:newcnf=on:random_seed=1429711576:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 27.56/4.16 % (3593158)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.56/4.16 % (3593158)Terminated due to inappropriate strategy. % 27.56/4.16 % (3593158)------------------------------ % 27.56/4.16 % (3593158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.56/4.16 % (3593158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.56/4.16 % (3593158)CaDiCaL version: 2.1.3 % 27.56/4.16 % (3593158)Termination reason: Inappropriate % 27.56/4.16 % (3593158)Time elapsed: 0.095 s % 27.56/4.16 % (3593158)Peak memory usage: 13 MB % 27.56/4.16 % (3593158)Instructions burned: 201 (million) % 27.56/4.16 % (3593158)------------------------------ % 27.56/4.16 % (3593158)------------------------------ % 27.56/4.16 % (3593164)ott+10_1_sil=32000:tgt=ground:random_seed=4185259689:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 27.56/4.16 % (3593140)Instruction limit reached! % 27.56/4.16 % (3593140)------------------------------ % 27.56/4.16 % (3593140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.56/4.16 % (3593140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.56/4.16 % (3593140)CaDiCaL version: 2.1.3 % 27.56/4.16 % (3593140)Termination reason: Instruction limit % 27.56/4.16 % (3593140)Termination phase: Saturation % 27.56/4.16 % (3593140)Time elapsed: 0.694 s % 27.56/4.16 % (3593140)Peak memory usage: 23 MB % 27.56/4.16 % (3593140)Instructions burned: 1180 (million) % 27.56/4.16 % (3593166)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2838025354:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 27.56/4.16 % (3593166)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.56/4.16 % (3593166)Terminated due to inappropriate strategy. % 27.56/4.16 % (3593166)------------------------------ % 27.56/4.16 % (3593166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.56/4.16 % (3593166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.56/4.16 % (3593166)CaDiCaL version: 2.1.3 % 27.56/4.16 % (3593166)Termination reason: Inappropriate % 27.56/4.16 % (3593166)Time elapsed: 0.095 s % 27.56/4.16 % (3593166)Peak memory usage: 12 MB % 120.38/17.25 % (3593166)Instructions burned: 203 (million) % 120.38/17.25 % (3593166)------------------------------ % 120.38/17.25 % (3593166)------------------------------ % 120.38/17.25 % (3593168)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2153119383:i=3512:aac=none_2989 on theBenchmark for (2989ds/3512Mi) % 120.38/17.25 % (3593162)Instruction limit reached! % 120.38/17.25 % (3593162)------------------------------ % 120.38/17.25 % (3593162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.38/17.25 % (3593162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.38/17.25 % (3593162)CaDiCaL version: 2.1.3 % 120.38/17.25 % (3593162)Termination reason: Instruction limit % 120.38/17.25 % (3593162)Termination phase: Saturation % 120.38/17.25 % (3593162)Time elapsed: 0.482 s % 120.38/17.25 % (3593162)Peak memory usage: 22 MB % 120.38/17.25 % (3593162)Instructions burned: 869 (million) % 120.38/17.25 % (3593170)dis+21_1_sil=32000:sas=cadical:random_seed=2977530668:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 120.38/17.25 % (3593156)Instruction limit reached! % 120.38/17.25 % (3593156)------------------------------ % 120.38/17.25 % (3593156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.38/17.25 % (3593156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.38/17.25 % (3593156)CaDiCaL version: 2.1.3 % 120.38/17.25 % (3593156)Termination reason: Instruction limit % 120.38/17.25 % (3593156)Termination phase: Saturation % 120.38/17.25 % (3593156)Time elapsed: 0.740 s % 120.38/17.25 % (3593156)Peak memory usage: 25 MB % 120.38/17.25 % (3593156)Instructions burned: 1474 (million) % 120.38/17.25 % (3593172)ott+11_1_sil=16000:gs=on:random_seed=4017462671:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 120.38/17.25 % (3593172)Instruction limit reached! % 120.38/17.25 % (3593172)------------------------------ % 120.38/17.25 % (3593172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.38/17.25 % (3593172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.38/17.25 % (3593172)CaDiCaL version: 2.1.3 % 120.38/17.25 % (3593172)Termination reason: Instruction limit % 120.38/17.25 % (3593172)Termination phase: Saturation % 120.38/17.25 % (3593172)Time elapsed: 1.258 s % 120.38/17.25 % (3593172)Peak memory usage: 29 MB % 120.38/17.25 % (3593172)Instructions burned: 2253 (million) % 120.38/17.25 % (3593174)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2530527452:fmbsr=1.6:i=67534_2973 on theBenchmark for (2973ds/67534Mi) % 120.38/17.25 % (3593174)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 120.38/17.25 % (3593174)Terminated due to inappropriate strategy. % 120.38/17.25 % (3593174)------------------------------ % 120.38/17.25 % (3593174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.38/17.25 % (3593174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.38/17.25 % (3593174)CaDiCaL version: 2.1.3 % 120.38/17.25 % (3593174)Termination reason: Inappropriate % 120.38/17.25 % (3593174)Time elapsed: 0.024 s % 120.38/17.25 % (3593174)Peak memory usage: 11 MB % 120.38/17.25 % (3593174)Instructions burned: 58 (million) % 120.38/17.25 % (3593174)------------------------------ % 120.38/17.25 % (3593174)------------------------------ % 120.38/17.25 % (3593176)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2208640972:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2973 on theBenchmark for (2973ds/4591Mi) % 120.38/17.25 % (3593168)Instruction limit reached! % 120.38/17.25 % (3593168)------------------------------ % 120.38/17.25 % (3593168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.38/17.25 % (3593168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.38/17.25 % (3593168)CaDiCaL version: 2.1.3 % 120.38/17.25 % (3593168)Termination reason: Instruction limit % 120.38/17.25 % (3593168)Termination phase: Saturation % 120.38/17.25 % (3593168)Time elapsed: 1.790 s % 120.38/17.25 % (3593168)Peak memory usage: 33 MB % 120.38/17.25 % (3593168)Instructions burned: 3514 (million) % 120.38/17.25 % (3593178)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4239782799:i=29340_2971 on theBenchmark for (2971ds/29340Mi) % 120.38/17.25 % (3593170)Instruction limit reached! % 120.38/17.25 % (3593170)------------------------------ % 120.38/17.25 % (3593170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.38/17.25 % (3593170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.38/17.25 % (3593170)CaDiCaL version: 2.1.3 % 142.17/20.36 % (3593170)Termination reason: Instruction limit % 142.17/20.36 % (3593170)Termination phase: Saturation % 142.17/20.36 % (3593170)Time elapsed: 2.006 s % 142.17/20.36 % (3593170)Peak memory usage: 36 MB % 142.17/20.36 % (3593170)Instructions burned: 3773 (million) % 142.17/20.36 % (3593153)Instruction limit reached! % 142.17/20.36 % (3593153)------------------------------ % 142.17/20.36 % (3593153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.17/20.36 % (3593153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.17/20.36 % (3593153)CaDiCaL version: 2.1.3 % 142.17/20.36 % (3593153)Termination reason: Instruction limit % 142.17/20.36 % (3593153)Termination phase: Saturation % 142.17/20.36 % (3593153)Time elapsed: 2.713 s % 142.17/20.36 % (3593153)Peak memory usage: 44 MB % 142.17/20.36 % (3593153)Instructions burned: 5132 (million) % 142.17/20.36 % (3593180)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2094089659:i=5211_2967 on theBenchmark for (2967ds/5211Mi) % 142.17/20.36 % (3593181)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2636885517:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 142.17/20.36 % (3593181)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 142.17/20.36 % (3593181)Terminated due to inappropriate strategy. % 142.17/20.36 % (3593181)------------------------------ % 142.17/20.36 % (3593181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.17/20.36 % (3593181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.17/20.36 % (3593181)CaDiCaL version: 2.1.3 % 142.17/20.36 % (3593181)Termination reason: Inappropriate % 142.17/20.36 % (3593181)Time elapsed: 0.058 s % 142.17/20.36 % (3593181)Peak memory usage: 13 MB % 142.17/20.36 % (3593181)Instructions burned: 124 (million) % 142.17/20.36 % (3593181)------------------------------ % 142.17/20.36 % (3593181)------------------------------ % 142.17/20.36 % (3593184)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=241597400:fmbsr=2:i=46332_2966 on theBenchmark for (2966ds/46332Mi) % 142.17/20.36 % (3593184)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 142.17/20.36 % (3593184)Terminated due to inappropriate strategy. % 142.17/20.36 % (3593184)------------------------------ % 142.17/20.36 % (3593184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.17/20.36 % (3593184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.17/20.36 % (3593184)CaDiCaL version: 2.1.3 % 142.17/20.36 % (3593184)Termination reason: Inappropriate % 142.17/20.36 % (3593184)Time elapsed: 0.024 s % 142.17/20.36 % (3593184)Peak memory usage: 11 MB % 142.17/20.36 % (3593184)Instructions burned: 58 (million) % 142.17/20.36 % (3593184)------------------------------ % 142.17/20.36 % (3593184)------------------------------ % 142.17/20.36 % (3593186)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2527650861:i=14071_2966 on theBenchmark for (2966ds/14071Mi) % 142.17/20.36 % (3593186)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 142.17/20.36 % (3593186)Terminated due to inappropriate strategy. % 142.17/20.36 % (3593186)------------------------------ % 142.17/20.36 % (3593186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.17/20.36 % (3593186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.17/20.36 % (3593186)CaDiCaL version: 2.1.3 % 142.17/20.36 % (3593186)Termination reason: Inappropriate % 142.17/20.36 % (3593186)Time elapsed: 0.025 s % 142.17/20.36 % (3593186)Peak memory usage: 11 MB % 142.17/20.36 % (3593186)Instructions burned: 58 (million) % 142.17/20.36 % (3593186)------------------------------ % 142.17/20.36 % (3593186)------------------------------ % 142.17/20.36 % (3593188)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2055024026:i=22565:add=on:rawr=on_2965 on theBenchmark for (2965ds/22565Mi) % 142.17/20.36 % (3593164)Instruction limit reached! % 142.17/20.36 % (3593164)------------------------------ % 142.17/20.36 % (3593164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.17/20.36 % (3593164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.17/20.36 % (3593164)CaDiCaL version: 2.1.3 % 142.17/20.36 % (3593164)Termination reason: Instruction limit % 142.17/20.36 % (3593164)Termination phase: Saturation % 142.17/20.36 % (3593164)Time elapsed: 3.114 s % 142.17/20.36 % (3593164)Peak memory usage: 34 MB % 142.17/20.36 % (3593164)Instructions burned: 5114 (million) % 142.17/20.36 % (3593190)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1217614334:i=8173:av=off_2960 on theBenchmark for (2960ds/8173Mi) % 143.93/20.67 % (3593176)Instruction limit reached! % 143.93/20.67 % (3593176)------------------------------ % 143.93/20.67 % (3593176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.93/20.67 % (3593176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.93/20.67 % (3593176)CaDiCaL version: 2.1.3 % 143.93/20.67 % (3593176)Termination reason: Instruction limit % 143.93/20.67 % (3593176)Termination phase: Saturation % 143.93/20.67 % (3593176)Time elapsed: 2.453 s % 143.93/20.67 % (3593176)Peak memory usage: 44 MB % 143.93/20.67 % (3593176)Instructions burned: 4592 (million) % 143.93/20.67 % (3593192)dis+10_16:1_sil=16000:random_seed=3499980097:i=9155:fsr=off_2948 on theBenchmark for (2948ds/9155Mi) % 143.93/20.67 % (3593180)Instruction limit reached! % 143.93/20.67 % (3593180)------------------------------ % 143.93/20.67 % (3593180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.93/20.67 % (3593180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.93/20.67 % (3593180)CaDiCaL version: 2.1.3 % 143.93/20.67 % (3593180)Termination reason: Instruction limit % 143.93/20.67 % (3593180)Termination phase: Saturation % 143.93/20.67 % (3593180)Time elapsed: 2.477 s % 143.93/20.67 % (3593180)Peak memory usage: 47 MB % 143.93/20.67 % (3593180)Instructions burned: 5213 (million) % 143.93/20.67 % (3593194)ott-3_8_sil=64000:random_seed=3512881051:i=20139:bs=on_2942 on theBenchmark for (2942ds/20139Mi) % 143.93/20.67 % (3593190)Instruction limit reached! % 143.93/20.67 % (3593190)------------------------------ % 143.93/20.67 % (3593190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.93/20.67 % (3593190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.93/20.67 % (3593190)CaDiCaL version: 2.1.3 % 143.93/20.67 % (3593190)Termination reason: Instruction limit % 143.93/20.67 % (3593190)Termination phase: Saturation % 143.93/20.67 % (3593190)Time elapsed: 5.084 s % 143.93/20.67 % (3593190)Peak memory usage: 48 MB % 143.93/20.67 % (3593190)Instructions burned: 8173 (million) % 143.93/20.67 % (3593197)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=21468326:fmbsr=2:i=32576_2909 on theBenchmark for (2909ds/32576Mi) % 143.93/20.67 % (3593197)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.93/20.67 % (3593197)Terminated due to inappropriate strategy. % 143.93/20.67 % (3593197)------------------------------ % 143.93/20.67 % (3593197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.93/20.67 % (3593197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.93/20.67 % (3593197)CaDiCaL version: 2.1.3 % 143.93/20.67 % (3593197)Termination reason: Inappropriate % 143.93/20.67 % (3593197)Time elapsed: 0.094 s % 143.93/20.67 % (3593197)Peak memory usage: 12 MB % 143.93/20.67 % (3593197)Instructions burned: 201 (million) % 143.93/20.67 % (3593197)------------------------------ % 143.93/20.67 % (3593197)------------------------------ % 143.93/20.67 % (3593199)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1019730002:i=11404_2908 on theBenchmark for (2908ds/11404Mi) % 143.93/20.67 % (3593192)Instruction limit reached! % 143.93/20.67 % (3593192)------------------------------ % 143.93/20.67 % (3593192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.93/20.67 % (3593192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.93/20.67 % (3593192)CaDiCaL version: 2.1.3 % 143.93/20.67 % (3593192)Termination reason: Instruction limit % 143.93/20.67 % (3593192)Termination phase: Saturation % 143.93/20.67 % (3593192)Time elapsed: 4.821 s % 143.93/20.67 % (3593192)Peak memory usage: 57 MB % 143.93/20.67 % (3593192)Instructions burned: 9155 (million) % 143.93/20.67 % (3593201)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2742347772:i=14134_2900 on theBenchmark for (2900ds/14134Mi) % 143.93/20.67 % (3593188)Instruction limit reached! % 143.93/20.67 % (3593188)------------------------------ % 143.93/20.67 % (3593188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.93/20.67 % (3593188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.93/20.67 % (3593188)CaDiCaL version: 2.1.3 % 143.93/20.67 % (3593188)Termination reason: Instruction limit % 143.93/20.67 % (3593188)Termination phase: Saturation % 143.93/20.67 % (3593188)Time elapsed: 9.067 s % 143.93/20.67 % (3593188)Peak memory usage: 28 MB % 143.93/20.67 % (3593188)Instructions burned: 22566 (million) % 143.93/20.67 % (3593203)dis+33_16_sil=32000:sac=on:random_seed=605655171:i=15851:nm=0_2874 on theBenchmark for (2874ds/15851Mi) % 143.93/20.67 % (3593194)Instruction limit reached! % 143.93/20.67 % (3593194)------------------------------ % 192.65/27.48 % (3593194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.65/27.48 % (3593194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.65/27.48 % (3593194)CaDiCaL version: 2.1.3 % 192.65/27.48 % (3593194)Termination reason: Instruction limit % 192.65/27.48 % (3593194)Termination phase: Saturation % 192.65/27.48 % (3593194)Time elapsed: 11.246 s % 192.65/27.48 % (3593194)Peak memory usage: 55 MB % 192.65/27.48 % (3593194)Instructions burned: 20140 (million) % 192.65/27.48 % (3593676)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2842020585:avsq=on:i=17627:add=on:amm=off_2829 on theBenchmark for (2829ds/17627Mi) % 192.65/27.48 % (3593199)Instruction limit reached! % 192.65/27.48 % (3593199)------------------------------ % 192.65/27.48 % (3593199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.65/27.48 % (3593199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.65/27.48 % (3593199)CaDiCaL version: 2.1.3 % 192.65/27.48 % (3593199)Termination reason: Instruction limit % 192.65/27.48 % (3593199)Termination phase: Saturation % 192.65/27.48 % (3593199)Time elapsed: 8.113 s % 192.65/27.48 % (3593199)Peak memory usage: 51 MB % 192.65/27.48 % (3593199)Instructions burned: 11406 (million) % 192.65/27.48 % (3593678)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1981129073:s2a=on:i=53295_2827 on theBenchmark for (2827ds/53295Mi) % 192.65/27.48 % (3593201)Instruction limit reached! % 192.65/27.48 % (3593201)------------------------------ % 192.65/27.48 % (3593201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.65/27.48 % (3593201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.65/27.48 % (3593201)CaDiCaL version: 2.1.3 % 192.65/27.48 % (3593201)Termination reason: Instruction limit % 192.65/27.48 % (3593201)Termination phase: Saturation % 192.65/27.48 % (3593201)Time elapsed: 9.783 s % 192.65/27.48 % (3593201)Peak memory usage: 59 MB % 192.65/27.48 % (3593201)Instructions burned: 14134 (million) % 192.65/27.48 % (3593681)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2878429807:i=26857:ins=20_2802 on theBenchmark for (2802ds/26857Mi) % 192.65/27.48 % (3593681)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.65/27.48 % (3593681)Terminated due to inappropriate strategy. % 192.65/27.48 % (3593681)------------------------------ % 192.65/27.48 % (3593681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.65/27.48 % (3593681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.65/27.48 % (3593681)CaDiCaL version: 2.1.3 % 192.65/27.48 % (3593681)Termination reason: Inappropriate % 192.65/27.48 % (3593681)Time elapsed: 0.025 s % 192.65/27.48 % (3593681)Peak memory usage: 12 MB % 192.65/27.48 % (3593681)Instructions burned: 58 (million) % 192.65/27.48 % (3593681)------------------------------ % 192.65/27.48 % (3593681)------------------------------ % 192.65/27.48 % (3593683)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3801629060:i=28120:bs=on:fsr=off_2801 on theBenchmark for (2801ds/28120Mi) % 192.65/27.48 % (3593178)Instruction limit reached! % 192.65/27.48 % (3593178)------------------------------ % 192.65/27.48 % (3593178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.65/27.48 % (3593178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.65/27.48 % (3593178)CaDiCaL version: 2.1.3 % 192.65/27.48 % (3593178)Termination reason: Instruction limit % 192.65/27.48 % (3593178)Termination phase: Saturation % 192.65/27.48 % (3593178)Time elapsed: 17.190 s % 192.65/27.48 % (3593178)Peak memory usage: 86 MB % 192.65/27.48 % (3593178)Instructions burned: 29340 (million) % 192.65/27.48 % (3593685)fmb+10_1_sil=256000:fmbss=7:random_seed=1578324619:fmbsr=1.6:i=182295_2799 on theBenchmark for (2799ds/182295Mi) % 192.65/27.48 % (3593685)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.65/27.48 % (3593685)Terminated due to inappropriate strategy. % 192.65/27.48 % (3593685)------------------------------ % 192.65/27.48 % (3593685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.65/27.48 % (3593685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.65/27.48 % (3593685)CaDiCaL version: 2.1.3 % 192.65/27.48 % (3593685)Termination reason: Inappropriate % 192.65/27.48 % (3593685)Time elapsed: 0.025 s % 192.65/27.48 % (3593685)Peak memory usage: 12 MB % 192.65/27.48 % (3593685)Instructions burned: 58 (million) % 192.65/27.48 % (3593685)------------------------------ % 192.65/27.48 % (3593685)------------------------------ % 192.65/27.48 % (3593687)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=4099544505:i=44625:gsp=on_2798 on theBenchmark for (2798ds/44625Mi) % 205.57/29.29 % (3593687)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.57/29.29 % (3593687)Terminated due to inappropriate strategy. % 205.57/29.29 % (3593687)------------------------------ % 205.57/29.29 % (3593687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.57/29.29 % (3593687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.57/29.29 % (3593687)CaDiCaL version: 2.1.3 % 205.57/29.29 % (3593687)Termination reason: Inappropriate % 205.57/29.29 % (3593687)Time elapsed: 0.037 s % 205.57/29.29 % (3593687)Peak memory usage: 12 MB % 205.57/29.29 % (3593687)Instructions burned: 87 (million) % 205.57/29.29 % (3593687)------------------------------ % 205.57/29.29 % (3593687)------------------------------ % 205.57/29.29 % (3593689)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3686846627:i=160505_2798 on theBenchmark for (2798ds/160505Mi) % 205.57/29.29 % (3593689)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.57/29.29 % (3593689)Terminated due to inappropriate strategy. % 205.57/29.29 % (3593689)------------------------------ % 205.57/29.29 % (3593689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.57/29.29 % (3593689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.57/29.29 % (3593689)CaDiCaL version: 2.1.3 % 205.57/29.29 % (3593689)Termination reason: Inappropriate % 205.57/29.29 % (3593689)Time elapsed: 0.025 s % 205.57/29.29 % (3593689)Peak memory usage: 12 MB % 205.57/29.29 % (3593689)Instructions burned: 58 (million) % 205.57/29.29 % (3593689)------------------------------ % 205.57/29.29 % (3593689)------------------------------ % 205.57/29.29 % (3593691)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1741592806:fmbsr=1.3:i=225729_2797 on theBenchmark for (2797ds/225729Mi) % 205.57/29.29 % (3593691)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.57/29.29 % (3593691)Terminated due to inappropriate strategy. % 205.57/29.29 % (3593691)------------------------------ % 205.57/29.29 % (3593691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.57/29.29 % (3593691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.57/29.29 % (3593691)CaDiCaL version: 2.1.3 % 205.57/29.29 % (3593691)Termination reason: Inappropriate % 205.57/29.29 % (3593691)Time elapsed: 0.025 s % 205.57/29.29 % (3593691)Peak memory usage: 11 MB % 205.57/29.29 % (3593691)Instructions burned: 58 (million) % 205.57/29.29 % (3593691)------------------------------ % 205.57/29.29 % (3593691)------------------------------ % 205.57/29.29 % (3593693)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1695570274:fmbsr=2:i=185024:ins=7_2797 on theBenchmark for (2797ds/185024Mi) % 205.57/29.29 % (3593693)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.57/29.29 % (3593693)Terminated due to inappropriate strategy. % 205.57/29.29 % (3593693)------------------------------ % 205.57/29.29 % (3593693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.57/29.29 % (3593693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.57/29.29 % (3593693)CaDiCaL version: 2.1.3 % 205.57/29.29 % (3593693)Termination reason: Inappropriate % 205.57/29.29 % (3593693)Time elapsed: 0.025 s % 205.57/29.29 % (3593693)Peak memory usage: 11 MB % 205.57/29.29 % (3593693)Instructions burned: 58 (million) % 205.57/29.29 % (3593693)------------------------------ % 205.57/29.29 % (3593693)------------------------------ % 205.57/29.29 % (3593695)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1482745762:rtra=on_2796 on theBenchmark for (2796ds/0Mi) % 205.57/29.29 % (3593695)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.57/29.29 % (3593695)Terminated due to inappropriate strategy. % 205.57/29.29 % (3593695)------------------------------ % 205.57/29.29 % (3593695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.57/29.29 % (3593695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.57/29.29 % (3593695)CaDiCaL version: 2.1.3 % 205.57/29.29 % (3593695)Termination reason: Inappropriate % 205.57/29.29 % (3593695)Time elapsed: 0.084 s % 205.57/29.29 % (3593695)Peak memory usage: 13 MB % 205.57/29.29 % (3593695)Instructions burned: 172 (million) % 205.57/29.29 % (3593695)------------------------------ % 205.57/29.29 % (3593695)------------------------------ % 205.57/29.29 % (3593697)% WARNING: option uhcvi not known. % 205.57/29.29 % (3593697)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2293001791:i=271062:add=off:rtra=on:rawr=on_2795 on theBenchmark for (2795ds/271062Mi) % 224.01/31.81 % (3593069)Instruction limit reached! % 224.01/31.81 % (3593069)------------------------------ % 224.01/31.81 % (3593069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.01/31.81 % (3593069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.01/31.81 % (3593069)CaDiCaL version: 2.1.3 % 224.01/31.81 % (3593069)Termination reason: Instruction limit % 224.01/31.81 % (3593069)Termination phase: Saturation % 224.01/31.81 % (3593069)Time elapsed: 22.325 s % 224.01/31.81 % (3593069)Peak memory usage: 1081 MB % 224.01/31.81 % (3593069)Instructions burned: 88025 (million) % 224.01/31.81 % (3593699)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1605883108:i=176048:add=on:rtra=on:rawr=on_2775 on theBenchmark for (2775ds/176048Mi) % 224.01/31.81 % (3593676)Instruction limit reached! % 224.01/31.81 % (3593676)------------------------------ % 224.01/31.81 % (3593676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.01/31.81 % (3593676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.01/31.81 % (3593676)CaDiCaL version: 2.1.3 % 224.01/31.81 % (3593676)Termination reason: Instruction limit % 224.01/31.81 % (3593676)Termination phase: Saturation % 224.01/31.81 % (3593676)Time elapsed: 9.519 s % 224.01/31.81 % (3593676)Peak memory usage: 259 MB % 224.01/31.81 % (3593676)Instructions burned: 17627 (million) % 224.01/31.81 % (3593701)dis+10_1_sil=32000:si=on:sp=arity:random_seed=625408340:i=206:fgj=on:rtra=on_2734 on theBenchmark for (2734ds/206Mi) % 224.01/31.81 % (3593701)Instruction limit reached! % 224.01/31.81 % (3593701)------------------------------ % 224.01/31.81 % (3593701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.01/31.81 % (3593701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.01/31.81 % (3593701)CaDiCaL version: 2.1.3 % 224.01/31.81 % (3593701)Termination reason: Instruction limit % 224.01/31.81 % (3593701)Termination phase: Saturation % 224.01/31.81 % (3593701)Time elapsed: 0.111 s % 224.01/31.81 % (3593701)Peak memory usage: 16 MB % 224.01/31.81 % (3593701)Instructions burned: 206 (million) % 224.01/31.81 % (3593703)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=734730076:i=232:rtra=on_2732 on theBenchmark for (2732ds/232Mi) % 224.01/31.81 % (3593703)Instruction limit reached! % 224.01/31.81 % (3593703)------------------------------ % 224.01/31.81 % (3593703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.01/31.81 % (3593703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.01/31.81 % (3593703)CaDiCaL version: 2.1.3 % 224.01/31.81 % (3593703)Termination reason: Instruction limit % 224.01/31.81 % (3593703)Termination phase: Blocked clause elimination % 224.01/31.81 % (3593703)Time elapsed: 0.110 s % 224.01/31.81 % (3593703)Peak memory usage: 13 MB % 224.01/31.81 % (3593703)Instructions burned: 233 (million) % 224.01/31.81 % (3593705)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2783646597:i=262:rtra=on_2731 on theBenchmark for (2731ds/262Mi) % 224.01/31.81 % (3593705)Instruction limit reached! % 224.01/31.81 % (3593705)------------------------------ % 224.01/31.81 % (3593705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.01/31.81 % (3593705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.01/31.81 % (3593705)CaDiCaL version: 2.1.3 % 224.01/31.81 % (3593705)Termination reason: Instruction limit % 224.01/31.81 % (3593705)Termination phase: Saturation % 224.01/31.81 % (3593705)Time elapsed: 0.145 s % 224.01/31.81 % (3593705)Peak memory usage: 17 MB % 224.01/31.81 % (3593705)Instructions burned: 262 (million) % 224.01/31.81 % (3593707)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3351278492:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2729 on theBenchmark for (2729ds/318Mi) % 224.01/31.81 % (3593707)Instruction limit reached! % 224.01/31.81 % (3593707)------------------------------ % 224.01/31.81 % (3593707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.01/31.81 % (3593707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.01/31.81 % (3593707)CaDiCaL version: 2.1.3 % 224.01/31.81 % (3593707)Termination reason: Instruction limit % 224.01/31.81 % (3593707)Termination phase: Saturation % 224.01/31.81 % (3593707)Time elapsed: 0.186 s % 224.01/31.81 % (3593707)Peak memory usage: 18 MB % 224.01/31.81 % (3593707)Instructions burned: 318 (million) % 224.01/31.81 % (3593709)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=610311435:i=1428:nm=2:rtra=on_2727 on theBenchmark for (2727ds/1428Mi) % 228.20/32.48 % (3593709)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 228.20/32.48 % (3593709)Terminated due to inappropriate strategy. % 228.20/32.48 % (3593709)------------------------------ % 228.20/32.48 % (3593709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.20/32.48 % (3593709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.20/32.48 % (3593709)CaDiCaL version: 2.1.3 % 228.20/32.48 % (3593709)Termination reason: Inappropriate % 228.20/32.48 % (3593709)Time elapsed: 0.025 s % 228.20/32.48 % (3593709)Peak memory usage: 12 MB % 228.20/32.48 % (3593709)Instructions burned: 55 (million) % 228.20/32.48 % (3593709)------------------------------ % 228.20/32.48 % (3593709)------------------------------ % 228.20/32.48 % (3593711)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2310238540:i=262:bd=preordered:rtra=on:fsd=on_2727 on theBenchmark for (2727ds/262Mi) % 228.20/32.48 % (3593711)Instruction limit reached! % 228.20/32.48 % (3593711)------------------------------ % 228.20/32.48 % (3593711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.20/32.48 % (3593711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.20/32.48 % (3593711)CaDiCaL version: 2.1.3 % 228.20/32.48 % (3593711)Termination reason: Instruction limit % 228.20/32.48 % (3593711)Termination phase: Saturation % 228.20/32.48 % (3593711)Time elapsed: 0.138 s % 228.20/32.48 % (3593711)Peak memory usage: 17 MB % 228.20/32.48 % (3593711)Instructions burned: 262 (million) % 228.20/32.48 % (3593713)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=24699141:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2725 on theBenchmark for (2725ds/1368Mi) % 228.20/32.48 % (3593713)Instruction limit reached! % 228.20/32.48 % (3593713)------------------------------ % 228.20/32.48 % (3593713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.20/32.48 % (3593713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.20/32.48 % (3593713)CaDiCaL version: 2.1.3 % 228.20/32.48 % (3593713)Termination reason: Instruction limit % 228.20/32.48 % (3593713)Termination phase: Saturation % 228.20/32.48 % (3593713)Time elapsed: 0.768 s % 228.20/32.48 % (3593713)Peak memory usage: 31 MB % 228.20/32.48 % (3593713)Instructions burned: 1369 (million) % 228.20/32.48 % (3593715)ott-21_1_sil=16000:si=on:fs=off:random_seed=560518278:i=360:av=off:fsr=off:rtra=on_2717 on theBenchmark for (2717ds/360Mi) % 228.20/32.48 % (3593715)Instruction limit reached! % 228.20/32.48 % (3593715)------------------------------ % 228.20/32.48 % (3593715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.20/32.48 % (3593715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.20/32.48 % (3593715)CaDiCaL version: 2.1.3 % 228.20/32.48 % (3593715)Termination reason: Instruction limit % 228.20/32.48 % (3593715)Termination phase: Saturation % 228.20/32.48 % (3593715)Time elapsed: 0.170 s % 228.20/32.48 % (3593715)Peak memory usage: 15 MB % 228.20/32.48 % (3593715)Instructions burned: 361 (million) % 228.20/32.48 % (3593719)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3687051460:i=954:bd=all:rtra=on_2715 on theBenchmark for (2715ds/954Mi) % 228.20/32.48 % (3593719)Instruction limit reached! % 228.20/32.48 % (3593719)------------------------------ % 228.20/32.48 % (3593719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.20/32.48 % (3593719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.20/32.48 % (3593719)CaDiCaL version: 2.1.3 % 228.20/32.48 % (3593719)Termination reason: Instruction limit % 228.20/32.48 % (3593719)Termination phase: Saturation % 228.20/32.48 % (3593719)Time elapsed: 0.563 s % 228.20/32.48 % (3593719)Peak memory usage: 18 MB % 228.20/32.48 % (3593719)Instructions burned: 955 (million) % 228.20/32.48 % (3593851)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1852897774:fmbsr=1.3:i=1730:ins=25:rtra=on_2709 on theBenchmark for (2709ds/1730Mi) % 228.20/32.48 % (3593851)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 228.20/32.48 % (3593851)Terminated due to inappropriate strategy. % 228.20/32.48 % (3593851)------------------------------ % 228.20/32.48 % (3593851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.20/32.48 % (3593851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.20/32.48 % (3593851)CaDiCaL version: 2.1.3 % 265.79/37.80 % (3593851)Termination reason: Inappropriate % 265.79/37.80 % (3593851)Time elapsed: 0.034 s % 265.79/37.80 % (3593851)Peak memory usage: 13 MB % 265.79/37.80 % (3593851)Instructions burned: 74 (million) % 265.79/37.80 % (3593851)------------------------------ % 265.79/37.80 % (3593851)------------------------------ % 265.79/37.80 % (3593853)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1235950711:i=2358:rtra=on_2709 on theBenchmark for (2709ds/2358Mi) % 265.79/37.80 % (3593203)Instruction limit reached! % 265.79/37.80 % (3593203)------------------------------ % 265.79/37.80 % (3593203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.79/37.80 % (3593203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.79/37.80 % (3593203)CaDiCaL version: 2.1.3 % 265.79/37.80 % (3593203)Termination reason: Instruction limit % 265.79/37.80 % (3593203)Termination phase: Clausification % 265.79/37.80 % (3593203)Time elapsed: 16.796 s % 265.79/37.80 % (3593203)Peak memory usage: 8626 MB % 265.79/37.80 % (3593203)Instructions burned: 15851 (million) % 265.79/37.80 % (3593979)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3263855207:i=1778:ins=1:rtra=on_2695 on theBenchmark for (2695ds/1778Mi) % 266.41/37.80 % (3593979)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 266.41/37.80 % (3593979)Terminated due to inappropriate strategy. % 266.41/37.80 % (3593979)------------------------------ % 266.41/37.80 % (3593979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.41/37.80 % (3593979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.41/37.80 % (3593979)CaDiCaL version: 2.1.3 % 266.41/37.80 % (3593979)Termination reason: Inappropriate % 266.41/37.80 % (3593979)Time elapsed: 0.052 s % 266.41/37.80 % (3593979)Peak memory usage: 12 MB % 266.41/37.80 % (3593979)Instructions burned: 61 (million) % 266.41/37.80 % (3593979)------------------------------ % 266.41/37.80 % (3593979)------------------------------ % 266.41/37.80 % (3593987)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=2483728188:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2694 on theBenchmark for (2694ds/1384Mi) % 266.41/37.80 % (3593853)Instruction limit reached! % 266.41/37.80 % (3593853)------------------------------ % 266.41/37.80 % (3593853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.41/37.80 % (3593853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.41/37.80 % (3593853)CaDiCaL version: 2.1.3 % 266.41/37.80 % (3593853)Termination reason: Instruction limit % 266.41/37.80 % (3593853)Termination phase: Saturation % 266.41/37.80 % (3593853)Time elapsed: 1.584 s % 266.41/37.80 % (3593853)Peak memory usage: 29 MB % 266.41/37.80 % (3593853)Instructions burned: 2359 (million) % 266.41/37.80 % (3593989)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3951959366:i=1758:kws=inv_precedence:fsr=off:rtra=on_2693 on theBenchmark for (2693ds/1758Mi) % 266.41/37.80 % (3593989)Instruction limit reached! % 266.41/37.80 % (3593989)------------------------------ % 266.41/37.80 % (3593989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.41/37.80 % (3593989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.41/37.80 % (3593989)CaDiCaL version: 2.1.3 % 266.41/37.80 % (3593989)Termination reason: Instruction limit % 266.41/37.80 % (3593989)Termination phase: Saturation % 266.41/37.80 % (3593989)Time elapsed: 0.836 s % 266.41/37.80 % (3593989)Peak memory usage: 23 MB % 266.41/37.80 % (3593989)Instructions burned: 1759 (million) % 266.41/37.80 % (3593991)fmb+10_1_sil=64000:si=on:random_seed=2804928679:i=44122:nm=2:rtra=on:gsp=on_2684 on theBenchmark for (2684ds/44122Mi) % 266.41/37.80 % (3593991)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 266.41/37.80 % (3593991)Terminated due to inappropriate strategy. % 266.41/37.80 % (3593991)------------------------------ % 266.41/37.80 % (3593991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.41/37.80 % (3593991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.41/37.80 % (3593991)CaDiCaL version: 2.1.3 % 266.41/37.80 % (3593991)Termination reason: Inappropriate % 266.41/37.80 % (3593991)Time elapsed: 0.026 s % 266.41/37.80 % (3593991)Peak memory usage: 12 MB % 266.41/37.80 % (3593991)Instructions burned: 60 (million) % 266.41/37.80 % (3593991)------------------------------ % 266.41/37.80 % (3593991)------------------------------ % 266.41/37.80 % (3593987)Instruction limit reacheTerminated % 300.31/42.63 % Vampire exiting % 300.31/42.63 Terminated %------------------------------------------------------------------------------