%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX118_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n010.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:46:31 PM UTC 2026 % Result : Timeout 300.08s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX118_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n010.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 15:02:32 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/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 % 2.91/0.68 % (1987696)Will run a generic schedule for satisfiability detection. % 2.91/0.68 % (1987710)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2532813155_2999 on theBenchmark for (2999ds/0Mi) % 2.91/0.68 % (1987710)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.91/0.68 % (1987710)Terminated due to inappropriate strategy. % 2.91/0.68 % (1987710)------------------------------ % 2.91/0.68 % (1987710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.91/0.68 % (1987710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.91/0.68 % (1987710)CaDiCaL version: 2.1.3 % 2.91/0.68 % (1987710)Termination reason: Inappropriate % 2.91/0.68 % (1987710)Time elapsed: 0.001 s % 2.91/0.68 % (1987710)Peak memory usage: 10 MB % 2.91/0.68 % (1987710)Instructions burned: 2 (million) % 2.91/0.68 % (1987710)------------------------------ % 2.91/0.68 % (1987710)------------------------------ % 2.91/0.68 % (1987711)% WARNING: option uhcvi not known. % 2.91/0.68 % (1987711)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2645390850:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.91/0.68 % (1987713)dis+10_1_sil=32000:sp=arity:random_seed=2171600664:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.91/0.68 % (1987712)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2280556538:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.91/0.68 % (1987714)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=67062010:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.91/0.68 % (1987716)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1278080595:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.91/0.68 % (1987715)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3073377602:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.91/0.68 % (1987720)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2747519457:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.91/0.68 % (1987720)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.91/0.68 % (1987720)Terminated due to inappropriate strategy. % 2.91/0.68 % (1987720)------------------------------ % 2.91/0.68 % (1987720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.91/0.68 % (1987720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.91/0.68 % (1987720)CaDiCaL version: 2.1.3 % 2.91/0.68 % (1987720)Termination reason: Inappropriate % 2.91/0.68 % (1987720)Time elapsed: 0.0000 s % 2.91/0.68 % (1987720)Peak memory usage: 10 MB % 2.91/0.68 % (1987720)Instructions burned: 2 (million) % 2.91/0.68 % (1987720)------------------------------ % 2.91/0.68 % (1987720)------------------------------ % 2.91/0.68 % (1987732)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1254892466:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.91/0.68 % (1987732)Instruction limit reached! % 2.91/0.68 % (1987732)------------------------------ % 2.91/0.68 % (1987732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.91/0.68 % (1987732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.91/0.68 % (1987732)CaDiCaL version: 2.1.3 % 2.91/0.68 % (1987732)Termination reason: Instruction limit % 2.91/0.68 % (1987732)Termination phase: Saturation % 2.91/0.68 % (1987732)Time elapsed: 0.049 s % 2.91/0.68 % (1987732)Peak memory usage: 13 MB % 2.91/0.68 % (1987732)Instructions burned: 133 (million) % 2.91/0.68 % (1987713)Instruction limit reached! % 2.91/0.68 % (1987713)------------------------------ % 2.91/0.68 % (1987713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.91/0.68 % (1987713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.91/0.68 % (1987713)CaDiCaL version: 2.1.3 % 2.91/0.68 % (1987713)Termination reason: Instruction limit % 2.91/0.68 % (1987713)Termination phase: Saturation % 2.91/0.68 % (1987713)Time elapsed: 0.067 s % 2.91/0.68 % (1987713)Peak memory usage: 13 MB % 2.91/0.68 % (1987713)Instructions burned: 104 (million) % 2.91/0.68 % (1987714)Instruction limit reached! % 2.91/0.68 % (1987714)------------------------------ % 2.91/0.68 % (1987714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.91/0.68 % (1987714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.91/0.68 % (1987714)CaDiCaL version: 2.1.3 % 2.91/0.68 % (1987714)Termination reason: Instruction limit % 6.47/1.15 % (1987714)Termination phase: Saturation % 6.47/1.15 % (1987714)Time elapsed: 0.075 s % 6.47/1.15 % (1987714)Peak memory usage: 13 MB % 6.47/1.15 % (1987714)Instructions burned: 116 (million) % 6.47/1.15 % (1987753)ott-21_1_sil=16000:fs=off:random_seed=3285995712:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 6.47/1.15 % (1987715)Instruction limit reached! % 6.47/1.15 % (1987715)------------------------------ % 6.47/1.15 % (1987715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.47/1.15 % (1987715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.47/1.15 % (1987715)CaDiCaL version: 2.1.3 % 6.47/1.15 % (1987715)Termination reason: Instruction limit % 6.47/1.15 % (1987715)Termination phase: Saturation % 6.47/1.15 % (1987715)Time elapsed: 0.083 s % 6.47/1.15 % (1987715)Peak memory usage: 13 MB % 6.47/1.15 % (1987715)Instructions burned: 131 (million) % 6.47/1.15 % (1987752)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=2956759212:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 6.47/1.15 % (1987755)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2249335511:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.47/1.15 % (1987759)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2510747524:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.47/1.15 % (1987759)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.47/1.15 % (1987759)Terminated due to inappropriate strategy. % 6.47/1.15 % (1987759)------------------------------ % 6.47/1.15 % (1987759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.47/1.15 % (1987759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.47/1.15 % (1987759)CaDiCaL version: 2.1.3 % 6.47/1.15 % (1987759)Termination reason: Inappropriate % 6.47/1.15 % (1987759)Time elapsed: 0.001 s % 6.47/1.15 % (1987759)Peak memory usage: 10 MB % 6.47/1.15 % (1987759)Instructions burned: 1 (million) % 6.47/1.15 % (1987759)------------------------------ % 6.47/1.15 % (1987759)------------------------------ % 6.47/1.15 % (1987716)Instruction limit reached! % 6.47/1.15 % (1987716)------------------------------ % 6.47/1.15 % (1987716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.47/1.15 % (1987716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.47/1.15 % (1987716)CaDiCaL version: 2.1.3 % 6.47/1.15 % (1987716)Termination reason: Instruction limit % 6.47/1.15 % (1987716)Termination phase: Saturation % 6.47/1.15 % (1987716)Time elapsed: 0.114 s % 6.47/1.15 % (1987716)Peak memory usage: 13 MB % 6.47/1.15 % (1987716)Instructions burned: 159 (million) % 6.47/1.15 % (1987753)Instruction limit reached! % 6.47/1.15 % (1987753)------------------------------ % 6.47/1.15 % (1987753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.47/1.15 % (1987753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.47/1.15 % (1987753)CaDiCaL version: 2.1.3 % 6.47/1.15 % (1987753)Termination reason: Instruction limit % 6.47/1.15 % (1987753)Termination phase: Saturation % 6.47/1.15 % (1987753)Time elapsed: 0.045 s % 6.47/1.15 % (1987753)Peak memory usage: 13 MB % 6.47/1.15 % (1987753)Instructions burned: 185 (million) % 6.47/1.15 % (1987770)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1598270814:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.47/1.15 % (1987777)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=3326280173: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) % 6.47/1.15 % (1987775)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1976746773:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.47/1.15 % (1987775)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.47/1.15 % (1987775)Terminated due to inappropriate strategy. % 6.47/1.15 % (1987775)------------------------------ % 6.47/1.15 % (1987775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.47/1.15 % (1987775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.47/1.15 % (1987775)CaDiCaL version: 2.1.3 % 6.47/1.15 % (1987775)Termination reason: Inappropriate % 6.47/1.15 % (1987775)Time elapsed: 0.001 s % 6.47/1.15 % (1987775)Peak memory usage: 10 MB % 19.93/3.04 % (1987775)Instructions burned: 2 (million) % 19.93/3.04 % (1987775)------------------------------ % 19.93/3.04 % (1987775)------------------------------ % 19.93/3.04 % (1987785)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3909514599:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 19.93/3.04 % (1987777)Instruction limit reached! % 19.93/3.04 % (1987777)------------------------------ % 19.93/3.04 % (1987777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.93/3.04 % (1987777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.93/3.04 % (1987777)CaDiCaL version: 2.1.3 % 19.93/3.04 % (1987777)Termination reason: Instruction limit % 19.93/3.04 % (1987777)Termination phase: Saturation % 19.93/3.04 % (1987777)Time elapsed: 0.215 s % 19.93/3.04 % (1987777)Peak memory usage: 17 MB % 19.93/3.04 % (1987777)Instructions burned: 692 (million) % 19.93/3.04 % (1987829)fmb+10_1_sil=64000:random_seed=2007280455:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 19.93/3.04 % (1987829)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.93/3.04 % (1987829)Terminated due to inappropriate strategy. % 19.93/3.04 % (1987829)------------------------------ % 19.93/3.04 % (1987829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.93/3.04 % (1987829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.93/3.04 % (1987829)CaDiCaL version: 2.1.3 % 19.93/3.04 % (1987829)Termination reason: Inappropriate % 19.93/3.04 % (1987829)Time elapsed: 0.001 s % 19.93/3.04 % (1987829)Peak memory usage: 10 MB % 19.93/3.04 % (1987829)Instructions burned: 2 (million) % 19.93/3.04 % (1987829)------------------------------ % 19.93/3.04 % (1987829)------------------------------ % 19.93/3.04 % (1987831)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3291624330:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 19.93/3.04 % (1987831)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.93/3.04 % (1987831)Terminated due to inappropriate strategy. % 19.93/3.04 % (1987831)------------------------------ % 19.93/3.04 % (1987831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.93/3.04 % (1987831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.93/3.04 % (1987831)CaDiCaL version: 2.1.3 % 19.93/3.04 % (1987831)Termination reason: Inappropriate % 19.93/3.04 % (1987831)Time elapsed: 0.0000 s % 19.93/3.04 % (1987831)Peak memory usage: 10 MB % 19.93/3.04 % (1987831)Instructions burned: 2 (million) % 19.93/3.04 % (1987831)------------------------------ % 19.93/3.04 % (1987831)------------------------------ % 19.93/3.04 % (1987833)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=501743352:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 19.93/3.04 % (1987833)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.93/3.04 % (1987833)Terminated due to inappropriate strategy. % 19.93/3.04 % (1987833)------------------------------ % 19.93/3.04 % (1987833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.93/3.04 % (1987833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.93/3.04 % (1987833)CaDiCaL version: 2.1.3 % 19.93/3.04 % (1987833)Termination reason: Inappropriate % 19.93/3.04 % (1987833)Time elapsed: 0.0000 s % 19.93/3.04 % (1987833)Peak memory usage: 10 MB % 19.93/3.04 % (1987833)Instructions burned: 2 (million) % 19.93/3.04 % (1987833)------------------------------ % 19.93/3.04 % (1987833)------------------------------ % 19.93/3.04 % (1987752)Instruction limit reached! % 19.93/3.04 % (1987752)------------------------------ % 19.93/3.04 % (1987752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.93/3.04 % (1987752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.93/3.04 % (1987752)CaDiCaL version: 2.1.3 % 19.93/3.04 % (1987752)Termination reason: Instruction limit % 19.93/3.04 % (1987752)Termination phase: Saturation % 19.93/3.04 % (1987752)Time elapsed: 0.313 s % 19.93/3.04 % (1987752)Peak memory usage: 14 MB % 19.93/3.04 % (1987752)Instructions burned: 685 (million) % 19.93/3.04 % (1987835)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2254541775:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 19.93/3.04 % (1987837)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1300579678:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 19.93/3.04 % (1987755)Instruction limit reached! % 19.93/3.04 % (1987755)------------------------------ % 21.43/3.38 % (1987755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.43/3.38 % (1987755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.43/3.38 % (1987755)CaDiCaL version: 2.1.3 % 21.43/3.38 % (1987755)Termination reason: Instruction limit % 21.43/3.38 % (1987755)Termination phase: Saturation % 21.43/3.38 % (1987755)Time elapsed: 0.327 s % 21.43/3.38 % (1987755)Peak memory usage: 14 MB % 21.43/3.38 % (1987755)Instructions burned: 478 (million) % 21.43/3.38 % (1987839)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2574122989:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 21.43/3.38 % (1987839)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.43/3.38 % (1987839)Terminated due to inappropriate strategy. % 21.43/3.38 % (1987839)------------------------------ % 21.43/3.38 % (1987839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.43/3.38 % (1987839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.43/3.38 % (1987839)CaDiCaL version: 2.1.3 % 21.43/3.38 % (1987839)Termination reason: Inappropriate % 21.43/3.38 % (1987839)Time elapsed: 0.002 s % 21.43/3.38 % (1987839)Peak memory usage: 10 MB % 21.43/3.38 % (1987839)Instructions burned: 2 (million) % 21.43/3.38 % (1987839)------------------------------ % 21.43/3.38 % (1987839)------------------------------ % 21.43/3.38 % (1987841)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=638809173:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 21.43/3.38 % (1987841)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.43/3.38 % (1987841)Terminated due to inappropriate strategy. % 21.43/3.38 % (1987841)------------------------------ % 21.43/3.38 % (1987841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.43/3.38 % (1987841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.43/3.38 % (1987841)CaDiCaL version: 2.1.3 % 21.43/3.38 % (1987841)Termination reason: Inappropriate % 21.43/3.38 % (1987841)Time elapsed: 0.001 s % 21.43/3.38 % (1987841)Peak memory usage: 10 MB % 21.43/3.38 % (1987841)Instructions burned: 2 (million) % 21.43/3.38 % (1987841)------------------------------ % 21.43/3.38 % (1987841)------------------------------ % 21.43/3.38 % (1987843)ott-2_1_sil=16000:newcnf=on:random_seed=3094728949:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi) % 21.43/3.38 % (1987785)Instruction limit reached! % 21.43/3.38 % (1987785)------------------------------ % 21.43/3.38 % (1987785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.43/3.38 % (1987785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.43/3.38 % (1987785)CaDiCaL version: 2.1.3 % 21.43/3.38 % (1987785)Termination reason: Instruction limit % 21.43/3.38 % (1987785)Termination phase: Saturation % 21.43/3.38 % (1987785)Time elapsed: 0.508 s % 21.43/3.38 % (1987785)Peak memory usage: 18 MB % 21.43/3.38 % (1987785)Instructions burned: 879 (million) % 21.43/3.38 % (1987845)ott+10_1_sil=32000:tgt=ground:random_seed=2618388413:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 21.43/3.38 % (1987770)Instruction limit reached! % 21.43/3.38 % (1987770)------------------------------ % 21.43/3.38 % (1987770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.43/3.38 % (1987770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.43/3.38 % (1987770)CaDiCaL version: 2.1.3 % 21.43/3.38 % (1987770)Termination reason: Instruction limit % 21.43/3.38 % (1987770)Termination phase: Saturation % 21.43/3.38 % (1987770)Time elapsed: 0.738 s % 21.43/3.38 % (1987770)Peak memory usage: 21 MB % 21.43/3.38 % (1987770)Instructions burned: 1179 (million) % 21.43/3.38 % (1987847)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1913385542:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 21.43/3.38 % (1987847)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.43/3.38 % (1987847)Terminated due to inappropriate strategy. % 21.43/3.38 % (1987847)------------------------------ % 21.43/3.38 % (1987847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.43/3.38 % (1987847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.43/3.38 % (1987847)CaDiCaL version: 2.1.3 % 21.43/3.38 % (1987847)Termination reason: Inappropriate % 21.43/3.38 % (1987847)Time elapsed: 0.002 s % 21.43/3.38 % (1987847)Peak memory usage: 10 MB % 21.43/3.38 % (1987847)Instructions burned: 2 (million) % 89.26/12.82 % (1987847)------------------------------ % 89.26/12.82 % (1987847)------------------------------ % 89.26/12.82 % (1987849)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3605043419:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 89.26/12.82 % (1987843)Instruction limit reached! % 89.26/12.82 % (1987843)------------------------------ % 89.26/12.82 % (1987843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.26/12.82 % (1987843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.26/12.82 % (1987843)CaDiCaL version: 2.1.3 % 89.26/12.82 % (1987843)Termination reason: Instruction limit % 89.26/12.82 % (1987843)Termination phase: Saturation % 89.26/12.82 % (1987843)Time elapsed: 0.527 s % 89.26/12.82 % (1987843)Peak memory usage: 18 MB % 89.26/12.82 % (1987843)Instructions burned: 870 (million) % 89.26/12.82 % (1987851)dis+21_1_sil=32000:sas=cadical:random_seed=4285264359:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 89.26/12.82 % (1987837)Instruction limit reached! % 89.26/12.82 % (1987837)------------------------------ % 89.26/12.82 % (1987837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.26/12.82 % (1987837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.26/12.82 % (1987837)CaDiCaL version: 2.1.3 % 89.26/12.82 % (1987837)Termination reason: Instruction limit % 89.26/12.82 % (1987837)Termination phase: Saturation % 89.26/12.82 % (1987837)Time elapsed: 0.823 s % 89.26/12.82 % (1987837)Peak memory usage: 24 MB % 89.26/12.82 % (1987837)Instructions burned: 1473 (million) % 89.26/12.82 % (1987853)ott+11_1_sil=16000:gs=on:random_seed=1693895012:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 89.26/12.82 % (1987835)Instruction limit reached! % 89.26/12.82 % (1987835)------------------------------ % 89.26/12.82 % (1987835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.26/12.82 % (1987835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.26/12.82 % (1987835)CaDiCaL version: 2.1.3 % 89.26/12.82 % (1987835)Termination reason: Instruction limit % 89.26/12.82 % (1987835)Termination phase: Saturation % 89.26/12.82 % (1987835)Time elapsed: 1.534 s % 89.26/12.82 % (1987835)Peak memory usage: 47 MB % 89.26/12.82 % (1987835)Instructions burned: 5134 (million) % 89.26/12.82 % (1987855)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3045338412:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 89.26/12.82 % (1987855)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 89.26/12.82 % (1987855)Terminated due to inappropriate strategy. % 89.26/12.82 % (1987855)------------------------------ % 89.26/12.82 % (1987855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.26/12.82 % (1987855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.26/12.82 % (1987855)CaDiCaL version: 2.1.3 % 89.26/12.82 % (1987855)Termination reason: Inappropriate % 89.26/12.82 % (1987855)Time elapsed: 0.001 s % 89.26/12.82 % (1987855)Peak memory usage: 10 MB % 89.26/12.82 % (1987855)Instructions burned: 2 (million) % 89.26/12.82 % (1987855)------------------------------ % 89.26/12.82 % (1987855)------------------------------ % 89.26/12.82 % (1987857)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2208303543:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 89.26/12.82 % (1987853)Instruction limit reached! % 89.26/12.82 % (1987853)------------------------------ % 89.26/12.82 % (1987853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.26/12.82 % (1987853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.26/12.82 % (1987853)CaDiCaL version: 2.1.3 % 89.26/12.82 % (1987853)Termination reason: Instruction limit % 89.26/12.82 % (1987853)Termination phase: Saturation % 89.26/12.82 % (1987853)Time elapsed: 1.356 s % 89.26/12.82 % (1987853)Peak memory usage: 27 MB % 89.26/12.82 % (1987853)Instructions burned: 2251 (million) % 89.26/12.82 % (1987859)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2057527848:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 89.26/12.82 % (1987849)Instruction limit reached! % 89.26/12.82 % (1987849)------------------------------ % 89.26/12.82 % (1987849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.26/12.82 % (1987849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.26/12.82 % (1987849)CaDiCaL version: 2.1.3 % 89.26/12.82 % (1987849)Termination reason: Instruction limit % 121.79/17.49 % (1987849)Termination phase: Saturation % 121.79/17.49 % (1987849)Time elapsed: 1.870 s % 121.79/17.49 % (1987849)Peak memory usage: 32 MB % 121.79/17.49 % (1987849)Instructions burned: 3514 (million) % 121.79/17.49 % (1987861)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=792562257:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 121.79/17.49 % (1987857)Instruction limit reached! % 121.79/17.49 % (1987857)------------------------------ % 121.79/17.49 % (1987857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.79/17.49 % (1987857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.79/17.49 % (1987857)CaDiCaL version: 2.1.3 % 121.79/17.49 % (1987857)Termination reason: Instruction limit % 121.79/17.49 % (1987857)Termination phase: Saturation % 121.79/17.49 % (1987857)Time elapsed: 0.876 s % 121.79/17.49 % (1987857)Peak memory usage: 31 MB % 121.79/17.49 % (1987857)Instructions burned: 4593 (million) % 121.79/17.49 % (1987863)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3130715322:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi) % 121.79/17.49 % (1987863)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.79/17.49 % (1987863)Terminated due to inappropriate strategy. % 121.79/17.49 % (1987863)------------------------------ % 121.79/17.49 % (1987863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.79/17.49 % (1987863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.79/17.49 % (1987863)CaDiCaL version: 2.1.3 % 121.79/17.49 % (1987863)Termination reason: Inappropriate % 121.79/17.49 % (1987863)Time elapsed: 0.001 s % 121.79/17.49 % (1987863)Peak memory usage: 10 MB % 121.79/17.49 % (1987863)Instructions burned: 2 (million) % 121.79/17.49 % (1987863)------------------------------ % 121.79/17.49 % (1987863)------------------------------ % 121.79/17.49 % (1987865)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=520207729:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi) % 121.79/17.49 % (1987865)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.79/17.49 % (1987865)Terminated due to inappropriate strategy. % 121.79/17.49 % (1987865)------------------------------ % 121.79/17.49 % (1987865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.79/17.49 % (1987865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.79/17.49 % (1987865)CaDiCaL version: 2.1.3 % 121.79/17.49 % (1987865)Termination reason: Inappropriate % 121.79/17.49 % (1987865)Time elapsed: 0.001 s % 121.79/17.49 % (1987865)Peak memory usage: 10 MB % 121.79/17.49 % (1987865)Instructions burned: 2 (million) % 121.79/17.49 % (1987865)------------------------------ % 121.79/17.49 % (1987865)------------------------------ % 121.79/17.49 % (1987867)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4015306598:i=14071_2970 on theBenchmark for (2970ds/14071Mi) % 121.79/17.49 % (1987867)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.79/17.49 % (1987867)Terminated due to inappropriate strategy. % 121.79/17.49 % (1987867)------------------------------ % 121.79/17.49 % (1987867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.79/17.49 % (1987867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.79/17.49 % (1987867)CaDiCaL version: 2.1.3 % 121.79/17.49 % (1987867)Termination reason: Inappropriate % 121.79/17.49 % (1987867)Time elapsed: 0.001 s % 121.79/17.49 % (1987867)Peak memory usage: 10 MB % 121.79/17.49 % (1987867)Instructions burned: 2 (million) % 121.79/17.49 % (1987867)------------------------------ % 121.79/17.49 % (1987867)------------------------------ % 121.79/17.49 % (1987869)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=460977454:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 121.79/17.49 % (1987845)Instruction limit reached! % 121.79/17.49 % (1987845)------------------------------ % 121.79/17.49 % (1987845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.79/17.49 % (1987845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.79/17.49 % (1987845)CaDiCaL version: 2.1.3 % 121.79/17.49 % (1987845)Termination reason: Instruction limit % 121.79/17.49 % (1987845)Termination phase: Saturation % 121.79/17.49 % (1987845)Time elapsed: 2.420 s % 121.79/17.49 % (1987845)Peak memory usage: 22 MB % 121.79/17.49 % (1987845)Instructions burned: 5115 (million) % 121.79/17.49 % (1987851)Instruction limit reached! % 121.79/17.49 % (1987851)------------------------------ % 121.79/17.49 % (1987851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.99/17.60 % (1987851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.99/17.60 % (1987851)CaDiCaL version: 2.1.3 % 122.99/17.60 % (1987851)Termination reason: Instruction limit % 122.99/17.60 % (1987851)Termination phase: Saturation % 122.99/17.60 % (1987851)Time elapsed: 2.092 s % 122.99/17.60 % (1987851)Peak memory usage: 34 MB % 122.99/17.60 % (1987851)Instructions burned: 3775 (million) % 122.99/17.60 % (1987871)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=915172224:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 122.99/17.60 % (1987873)dis+10_16:1_sil=16000:random_seed=1122449597:i=9155:fsr=off_2968 on theBenchmark for (2968ds/9155Mi) % 122.99/17.60 % (1987861)Instruction limit reached! % 122.99/17.60 % (1987861)------------------------------ % 122.99/17.60 % (1987861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.99/17.60 % (1987861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.99/17.60 % (1987861)CaDiCaL version: 2.1.3 % 122.99/17.60 % (1987861)Termination reason: Instruction limit % 122.99/17.60 % (1987861)Termination phase: Saturation % 122.99/17.60 % (1987861)Time elapsed: 2.673 s % 122.99/17.60 % (1987861)Peak memory usage: 41 MB % 122.99/17.60 % (1987861)Instructions burned: 5212 (million) % 122.99/17.60 % (1987875)ott-3_8_sil=64000:random_seed=1968132637:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 122.99/17.60 % (1987871)Instruction limit reached! % 122.99/17.60 % (1987871)------------------------------ % 122.99/17.60 % (1987871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.99/17.60 % (1987871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.99/17.60 % (1987871)CaDiCaL version: 2.1.3 % 122.99/17.60 % (1987871)Termination reason: Instruction limit % 122.99/17.60 % (1987871)Termination phase: Saturation % 122.99/17.60 % (1987871)Time elapsed: 4.014 s % 122.99/17.60 % (1987871)Peak memory usage: 46 MB % 122.99/17.60 % (1987871)Instructions burned: 8174 (million) % 122.99/17.60 % (1987878)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1458078132:fmbsr=2:i=32576_2928 on theBenchmark for (2928ds/32576Mi) % 122.99/17.60 % (1987878)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 122.99/17.60 % (1987878)Terminated due to inappropriate strategy. % 122.99/17.60 % (1987878)------------------------------ % 122.99/17.60 % (1987878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.99/17.60 % (1987878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.99/17.60 % (1987878)CaDiCaL version: 2.1.3 % 122.99/17.60 % (1987878)Termination reason: Inappropriate % 122.99/17.60 % (1987878)Time elapsed: 0.002 s % 122.99/17.60 % (1987878)Peak memory usage: 10 MB % 122.99/17.60 % (1987878)Instructions burned: 2 (million) % 122.99/17.60 % (1987878)------------------------------ % 122.99/17.60 % (1987878)------------------------------ % 122.99/17.60 % (1987880)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1709351295:i=11404_2927 on theBenchmark for (2927ds/11404Mi) % 122.99/17.60 % (1987873)Instruction limit reached! % 122.99/17.60 % (1987873)------------------------------ % 122.99/17.60 % (1987873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.99/17.60 % (1987873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.99/17.60 % (1987873)CaDiCaL version: 2.1.3 % 122.99/17.60 % (1987873)Termination reason: Instruction limit % 122.99/17.60 % (1987873)Termination phase: Saturation % 122.99/17.60 % (1987873)Time elapsed: 4.658 s % 122.99/17.60 % (1987873)Peak memory usage: 52 MB % 122.99/17.60 % (1987873)Instructions burned: 9157 (million) % 122.99/17.60 % (1987882)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2084745431:i=14134_2921 on theBenchmark for (2921ds/14134Mi) % 122.99/17.60 % (1987869)Instruction limit reached! % 122.99/17.60 % (1987869)------------------------------ % 122.99/17.60 % (1987869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.99/17.60 % (1987869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.99/17.60 % (1987869)CaDiCaL version: 2.1.3 % 122.99/17.60 % (1987869)Termination reason: Instruction limit % 122.99/17.60 % (1987869)Termination phase: Saturation % 122.99/17.60 % (1987869)Time elapsed: 5.008 s % 122.99/17.60 % (1987869)Peak memory usage: 24 MB % 122.99/17.60 % (1987869)Instructions burned: 22568 (million) % 122.99/17.60 % (1987884)dis+33_16_sil=32000:sac=on:random_seed=2149031458:i=15851:nm=0_2920 on theBenchmark for (2920ds/15851Mi) % 122.99/17.60 % (1987884)Instruction limit reached! % 122.99/17.60 % (1987884)------------------------------ % 122.99/17.60 % (1987884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.00/18.41 % (1987884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.00/18.41 % (1987884)CaDiCaL version: 2.1.3 % 129.00/18.41 % (1987884)Termination reason: Instruction limit % 129.00/18.41 % (1987884)Termination phase: Saturation % 129.00/18.41 % (1987884)Time elapsed: 4.644 s % 129.00/18.41 % (1987884)Peak memory usage: 124 MB % 129.00/18.41 % (1987884)Instructions burned: 15853 (million) % 129.00/18.41 % (1987886)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1528467618:avsq=on:i=17627:add=on:amm=off_2874 on theBenchmark for (2874ds/17627Mi) % 129.00/18.41 % (1987880)Instruction limit reached! % 129.00/18.41 % (1987880)------------------------------ % 129.00/18.41 % (1987880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.00/18.41 % (1987880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.00/18.41 % (1987880)CaDiCaL version: 2.1.3 % 129.00/18.41 % (1987880)Termination reason: Instruction limit % 129.00/18.41 % (1987880)Termination phase: Saturation % 129.00/18.41 % (1987880)Time elapsed: 7.233 s % 129.00/18.41 % (1987880)Peak memory usage: 65 MB % 129.00/18.41 % (1987880)Instructions burned: 11404 (million) % 129.00/18.41 % (1988101)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1767010256:s2a=on:i=53295_2855 on theBenchmark for (2855ds/53295Mi) % 129.00/18.41 % (1987882)Instruction limit reached! % 129.00/18.41 % (1987882)------------------------------ % 129.00/18.41 % (1987882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.00/18.41 % (1987882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.00/18.41 % (1987882)CaDiCaL version: 2.1.3 % 129.00/18.41 % (1987882)Termination reason: Instruction limit % 129.00/18.41 % (1987882)Termination phase: Saturation % 129.00/18.41 % (1987882)Time elapsed: 9.151 s % 129.00/18.41 % (1987882)Peak memory usage: 76 MB % 129.00/18.41 % (1987882)Instructions burned: 14134 (million) % 129.00/18.41 % (1988255)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3054301174:i=26857:ins=20_2829 on theBenchmark for (2829ds/26857Mi) % 129.00/18.41 % (1988255)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.00/18.41 % (1988255)Terminated due to inappropriate strategy. % 129.00/18.41 % (1988255)------------------------------ % 129.00/18.41 % (1988255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.00/18.41 % (1988255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.00/18.41 % (1988255)CaDiCaL version: 2.1.3 % 129.00/18.41 % (1988255)Termination reason: Inappropriate % 129.00/18.41 % (1988255)Time elapsed: 0.002 s % 129.00/18.41 % (1988255)Peak memory usage: 10 MB % 129.00/18.41 % (1988255)Instructions burned: 2 (million) % 129.00/18.41 % (1988255)------------------------------ % 129.00/18.41 % (1988255)------------------------------ % 129.00/18.41 % (1988257)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3504167411:i=28120:bs=on:fsr=off_2829 on theBenchmark for (2829ds/28120Mi) % 129.00/18.41 % (1987875)Instruction limit reached! % 129.00/18.41 % (1987875)------------------------------ % 129.00/18.41 % (1987875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.00/18.41 % (1987875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.00/18.41 % (1987875)CaDiCaL version: 2.1.3 % 129.00/18.41 % (1987875)Termination reason: Instruction limit % 129.00/18.41 % (1987875)Termination phase: Saturation % 129.00/18.41 % (1987875)Time elapsed: 11.680 s % 129.00/18.41 % (1987875)Peak memory usage: 82 MB % 129.00/18.41 % (1987875)Instructions burned: 20139 (million) % 129.00/18.41 % (1988259)fmb+10_1_sil=256000:fmbss=7:random_seed=3952766903:fmbsr=1.6:i=182295_2827 on theBenchmark for (2827ds/182295Mi) % 129.00/18.41 % (1988259)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.00/18.41 % (1988259)Terminated due to inappropriate strategy. % 129.00/18.41 % (1988259)------------------------------ % 129.00/18.41 % (1988259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.00/18.41 % (1988259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.00/18.41 % (1988259)CaDiCaL version: 2.1.3 % 129.00/18.41 % (1988259)Termination reason: Inappropriate % 129.00/18.41 % (1988259)Time elapsed: 0.001 s % 129.00/18.41 % (1988259)Peak memory usage: 10 MB % 129.00/18.41 % (1988259)Instructions burned: 2 (million) % 129.00/18.41 % (1988259)------------------------------ % 129.00/18.41 % (1988259)------------------------------ % 129.00/18.41 % (1988261)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=902473748:i=44625:gsp=on_2827 on theBenchmark for (2827ds/44625Mi) % 141.32/20.14 % (1988261)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 141.32/20.14 % (1988261)Terminated due to inappropriate strategy. % 141.32/20.14 % (1988261)------------------------------ % 141.32/20.14 % (1988261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.32/20.14 % (1988261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.32/20.14 % (1988261)CaDiCaL version: 2.1.3 % 141.32/20.14 % (1988261)Termination reason: Inappropriate % 141.32/20.14 % (1988261)Time elapsed: 0.001 s % 141.32/20.14 % (1988261)Peak memory usage: 10 MB % 141.32/20.14 % (1988261)Instructions burned: 2 (million) % 141.32/20.14 % (1988261)------------------------------ % 141.32/20.14 % (1988261)------------------------------ % 141.32/20.14 % (1988263)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3688451044:i=160505_2827 on theBenchmark for (2827ds/160505Mi) % 141.32/20.14 % (1988263)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 141.32/20.14 % (1988263)Terminated due to inappropriate strategy. % 141.32/20.14 % (1988263)------------------------------ % 141.32/20.14 % (1988263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.32/20.14 % (1988263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.32/20.14 % (1988263)CaDiCaL version: 2.1.3 % 141.32/20.14 % (1988263)Termination reason: Inappropriate % 141.32/20.14 % (1988263)Time elapsed: 0.001 s % 141.32/20.14 % (1988263)Peak memory usage: 10 MB % 141.32/20.14 % (1988263)Instructions burned: 2 (million) % 141.32/20.14 % (1988263)------------------------------ % 141.32/20.14 % (1988263)------------------------------ % 141.32/20.14 % (1988265)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=498477261:fmbsr=1.3:i=225729_2827 on theBenchmark for (2827ds/225729Mi) % 141.32/20.14 % (1988265)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 141.32/20.14 % (1988265)Terminated due to inappropriate strategy. % 141.32/20.14 % (1988265)------------------------------ % 141.32/20.14 % (1988265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.32/20.14 % (1988265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.32/20.14 % (1988265)CaDiCaL version: 2.1.3 % 141.32/20.14 % (1988265)Termination reason: Inappropriate % 141.32/20.14 % (1988265)Time elapsed: 0.002 s % 141.32/20.14 % (1988265)Peak memory usage: 10 MB % 141.32/20.14 % (1988265)Instructions burned: 2 (million) % 141.32/20.14 % (1988265)------------------------------ % 141.32/20.14 % (1988265)------------------------------ % 141.32/20.14 % (1988267)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4229458694:fmbsr=2:i=185024:ins=7_2826 on theBenchmark for (2826ds/185024Mi) % 141.32/20.14 % (1988267)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 141.32/20.14 % (1988267)Terminated due to inappropriate strategy. % 141.32/20.14 % (1988267)------------------------------ % 141.32/20.14 % (1988267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.32/20.14 % (1988267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.32/20.14 % (1988267)CaDiCaL version: 2.1.3 % 141.32/20.14 % (1988267)Termination reason: Inappropriate % 141.32/20.14 % (1988267)Time elapsed: 0.002 s % 141.32/20.14 % (1988267)Peak memory usage: 10 MB % 141.32/20.14 % (1988267)Instructions burned: 2 (million) % 141.32/20.14 % (1988267)------------------------------ % 141.32/20.14 % (1988267)------------------------------ % 141.32/20.14 % (1988269)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1497969447:rtra=on_2826 on theBenchmark for (2826ds/0Mi) % 141.32/20.14 % (1988269)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 141.32/20.14 % (1988269)Terminated due to inappropriate strategy. % 141.32/20.14 % (1988269)------------------------------ % 141.32/20.14 % (1988269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.32/20.14 % (1988269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.32/20.14 % (1988269)CaDiCaL version: 2.1.3 % 141.32/20.14 % (1988269)Termination reason: Inappropriate % 141.32/20.14 % (1988269)Time elapsed: 0.002 s % 141.32/20.14 % (1988269)Peak memory usage: 10 MB % 141.32/20.14 % (1988269)Instructions burned: 2 (million) % 141.32/20.14 % (1988269)------------------------------ % 141.32/20.14 % (1988269)------------------------------ % 141.32/20.14 % (1988271)% WARNING: option uhcvi not known. % 141.32/20.14 % (1988271)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4285979690:i=271062:add=off:rtra=on:rawr=on_2826 on theBenchmark for (2826ds/271062Mi) % 164.48/23.42 % (1987886)Instruction limit reached! % 164.48/23.42 % (1987886)------------------------------ % 164.48/23.42 % (1987886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.48/23.42 % (1987886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.48/23.42 % (1987886)CaDiCaL version: 2.1.3 % 164.48/23.42 % (1987886)Termination reason: Instruction limit % 164.48/23.42 % (1987886)Termination phase: Saturation % 164.48/23.42 % (1987886)Time elapsed: 4.771 s % 164.48/23.42 % (1987886)Peak memory usage: 216 MB % 164.48/23.42 % (1987886)Instructions burned: 17628 (million) % 164.48/23.42 % (1987859)Instruction limit reached! % 164.48/23.42 % (1987859)------------------------------ % 164.48/23.42 % (1987859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.48/23.42 % (1987859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.48/23.42 % (1987859)CaDiCaL version: 2.1.3 % 164.48/23.42 % (1987859)Termination reason: Instruction limit % 164.48/23.42 % (1987859)Termination phase: Saturation % 164.48/23.42 % (1987859)Time elapsed: 14.719 s % 164.48/23.42 % (1987859)Peak memory usage: 112 MB % 164.48/23.42 % (1987859)Instructions burned: 29340 (million) % 164.48/23.42 % (1988273)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2234277473:i=176048:add=on:rtra=on:rawr=on_2826 on theBenchmark for (2826ds/176048Mi) % 164.48/23.42 % (1988275)dis+10_1_sil=32000:si=on:sp=arity:random_seed=608223304:i=206:fgj=on:rtra=on_2825 on theBenchmark for (2825ds/206Mi) % 164.48/23.42 % (1988275)Instruction limit reached! % 164.48/23.42 % (1988275)------------------------------ % 164.48/23.42 % (1988275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.48/23.42 % (1988275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.48/23.42 % (1988275)CaDiCaL version: 2.1.3 % 164.48/23.42 % (1988275)Termination reason: Instruction limit % 164.48/23.42 % (1988275)Termination phase: Saturation % 164.48/23.42 % (1988275)Time elapsed: 0.134 s % 164.48/23.42 % (1988275)Peak memory usage: 14 MB % 164.48/23.42 % (1988275)Instructions burned: 207 (million) % 164.48/23.42 % (1988277)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2030140624:i=232:rtra=on_2824 on theBenchmark for (2824ds/232Mi) % 164.48/23.42 % (1988277)Instruction limit reached! % 164.48/23.42 % (1988277)------------------------------ % 164.48/23.42 % (1988277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.48/23.42 % (1988277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.48/23.42 % (1988277)CaDiCaL version: 2.1.3 % 164.48/23.42 % (1988277)Termination reason: Instruction limit % 164.48/23.42 % (1988277)Termination phase: Saturation % 164.48/23.42 % (1988277)Time elapsed: 0.144 s % 164.48/23.42 % (1988277)Peak memory usage: 13 MB % 164.48/23.42 % (1988277)Instructions burned: 233 (million) % 164.48/23.42 % (1988279)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3071916325:i=262:rtra=on_2822 on theBenchmark for (2822ds/262Mi) % 164.48/23.42 % (1988279)Instruction limit reached! % 164.48/23.42 % (1988279)------------------------------ % 164.48/23.42 % (1988279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.48/23.42 % (1988279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.48/23.42 % (1988279)CaDiCaL version: 2.1.3 % 164.48/23.42 % (1988279)Termination reason: Instruction limit % 164.48/23.42 % (1988279)Termination phase: Saturation % 164.48/23.42 % (1988279)Time elapsed: 0.166 s % 164.48/23.42 % (1988279)Peak memory usage: 14 MB % 164.48/23.42 % (1988279)Instructions burned: 262 (million) % 164.48/23.42 % (1988281)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=4052543466:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2820 on theBenchmark for (2820ds/318Mi) % 164.48/23.42 % (1988281)Instruction limit reached! % 164.48/23.42 % (1988281)------------------------------ % 164.48/23.42 % (1988281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.48/23.42 % (1988281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.48/23.42 % (1988281)CaDiCaL version: 2.1.3 % 164.48/23.42 % (1988281)Termination reason: Instruction limit % 164.48/23.42 % (1988281)Termination phase: Saturation % 164.48/23.42 % (1988281)Time elapsed: 0.224 s % 164.48/23.42 % (1988281)Peak memory usage: 15 MB % 164.48/23.42 % (1988281)Instructions burned: 318 (million) % 164.48/23.42 % (1988283)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=454154212:i=1428:nm=2:rtra=on_2818 on theBenchmark for (2818ds/1428Mi) % 209.04/29.72 % (1988283)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 209.04/29.72 % (1988283)Terminated due to inappropriate strategy. % 209.04/29.72 % (1988283)------------------------------ % 209.04/29.72 % (1988283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.04/29.72 % (1988283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.04/29.72 % (1988283)CaDiCaL version: 2.1.3 % 209.04/29.72 % (1988283)Termination reason: Inappropriate % 209.04/29.72 % (1988283)Time elapsed: 0.002 s % 209.04/29.72 % (1988283)Peak memory usage: 10 MB % 209.04/29.72 % (1988283)Instructions burned: 2 (million) % 209.04/29.72 % (1988283)------------------------------ % 209.04/29.72 % (1988283)------------------------------ % 209.04/29.72 % (1988285)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2256671267:i=262:bd=preordered:rtra=on:fsd=on_2818 on theBenchmark for (2818ds/262Mi) % 209.04/29.72 % (1988285)Instruction limit reached! % 209.04/29.72 % (1988285)------------------------------ % 209.04/29.72 % (1988285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.04/29.72 % (1988285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.04/29.72 % (1988285)CaDiCaL version: 2.1.3 % 209.04/29.72 % (1988285)Termination reason: Instruction limit % 209.04/29.72 % (1988285)Termination phase: Saturation % 209.04/29.72 % (1988285)Time elapsed: 0.173 s % 209.04/29.72 % (1988285)Peak memory usage: 13 MB % 209.04/29.72 % (1988285)Instructions burned: 262 (million) % 209.04/29.72 % (1988287)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=916706666:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2816 on theBenchmark for (2816ds/1368Mi) % 209.04/29.72 % (1988287)Instruction limit reached! % 209.04/29.72 % (1988287)------------------------------ % 209.04/29.72 % (1988287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.04/29.72 % (1988287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.04/29.72 % (1988287)CaDiCaL version: 2.1.3 % 209.04/29.72 % (1988287)Termination reason: Instruction limit % 209.04/29.72 % (1988287)Termination phase: Saturation % 209.04/29.72 % (1988287)Time elapsed: 0.633 s % 209.04/29.72 % (1988287)Peak memory usage: 15 MB % 209.04/29.72 % (1988287)Instructions burned: 1368 (million) % 209.04/29.72 % (1988289)ott-21_1_sil=16000:si=on:fs=off:random_seed=1497953403:i=360:av=off:fsr=off:rtra=on_2809 on theBenchmark for (2809ds/360Mi) % 209.04/29.72 % (1988289)Instruction limit reached! % 209.04/29.72 % (1988289)------------------------------ % 209.04/29.72 % (1988289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.04/29.72 % (1988289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.04/29.72 % (1988289)CaDiCaL version: 2.1.3 % 209.04/29.72 % (1988289)Termination reason: Instruction limit % 209.04/29.72 % (1988289)Termination phase: Saturation % 209.04/29.72 % (1988289)Time elapsed: 0.160 s % 209.04/29.72 % (1988289)Peak memory usage: 13 MB % 209.04/29.72 % (1988289)Instructions burned: 360 (million) % 209.04/29.72 % (1988291)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4108873757:i=954:bd=all:rtra=on_2807 on theBenchmark for (2807ds/954Mi) % 209.04/29.72 % (1988291)Instruction limit reached! % 209.04/29.72 % (1988291)------------------------------ % 209.04/29.72 % (1988291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.04/29.72 % (1988291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.04/29.72 % (1988291)CaDiCaL version: 2.1.3 % 209.04/29.72 % (1988291)Termination reason: Instruction limit % 209.04/29.72 % (1988291)Termination phase: Saturation % 209.04/29.72 % (1988291)Time elapsed: 0.659 s % 209.04/29.72 % (1988291)Peak memory usage: 16 MB % 209.04/29.72 % (1988291)Instructions burned: 954 (million) % 209.04/29.72 % (1988293)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=127218425:fmbsr=1.3:i=1730:ins=25:rtra=on_2801 on theBenchmark for (2801ds/1730Mi) % 209.04/29.72 % (1988293)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 209.04/29.72 % (1988293)Terminated due to inappropriate strategy. % 209.04/29.72 % (1988293)------------------------------ % 209.04/29.72 % (1988293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.04/29.72 % (1988293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.04/29.72 % (1988293)CaDiCaL version: 2.1.3 % 209.04/29.72 % (1988293)Termination reason: Inappropriate % 209.04/29.72 % (1988293)Time elapsed: 0.001 s % 258.21/36.61 % (1988293)Peak memory usage: 10 MB % 258.21/36.61 % (1988293)Instructions burned: 2 (million) % 258.21/36.61 % (1988293)------------------------------ % 258.21/36.61 % (1988293)------------------------------ % 258.21/36.61 % (1988295)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=884412197:i=2358:rtra=on_2800 on theBenchmark for (2800ds/2358Mi) % 258.21/36.61 % (1988295)Instruction limit reached! % 258.21/36.61 % (1988295)------------------------------ % 258.21/36.61 % (1988295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.21/36.61 % (1988295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.21/36.61 % (1988295)CaDiCaL version: 2.1.3 % 258.21/36.61 % (1988295)Termination reason: Instruction limit % 258.21/36.61 % (1988295)Termination phase: Saturation % 258.21/36.61 % (1988295)Time elapsed: 1.282 s % 258.21/36.61 % (1988295)Peak memory usage: 24 MB % 258.21/36.61 % (1988295)Instructions burned: 2359 (million) % 258.21/36.61 % (1988297)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2450068384:i=1778:ins=1:rtra=on_2787 on theBenchmark for (2787ds/1778Mi) % 258.21/36.61 % (1988297)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 258.21/36.61 % (1988297)Terminated due to inappropriate strategy. % 258.21/36.61 % (1988297)------------------------------ % 258.21/36.61 % (1988297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.21/36.61 % (1988297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.21/36.61 % (1988297)CaDiCaL version: 2.1.3 % 258.21/36.61 % (1988297)Termination reason: Inappropriate % 258.21/36.61 % (1988297)Time elapsed: 0.002 s % 258.21/36.61 % (1988297)Peak memory usage: 10 MB % 258.21/36.61 % (1988297)Instructions burned: 2 (million) % 258.21/36.61 % (1988297)------------------------------ % 258.21/36.61 % (1988297)------------------------------ % 258.21/36.61 % (1988299)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=1307014835:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2787 on theBenchmark for (2787ds/1384Mi) % 258.21/36.61 % (1988299)Instruction limit reached! % 258.21/36.61 % (1988299)------------------------------ % 258.21/36.61 % (1988299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.21/36.61 % (1988299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.21/36.61 % (1988299)CaDiCaL version: 2.1.3 % 258.21/36.61 % (1988299)Termination reason: Instruction limit % 258.21/36.61 % (1988299)Termination phase: Saturation % 258.21/36.61 % (1988299)Time elapsed: 0.819 s % 258.21/36.61 % (1988299)Peak memory usage: 21 MB % 258.21/36.61 % (1988299)Instructions burned: 1385 (million) % 258.21/36.61 % (1988301)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=665808110:i=1758:kws=inv_precedence:fsr=off:rtra=on_2779 on theBenchmark for (2779ds/1758Mi) % 258.21/36.61 % (1988301)Instruction limit reached! % 258.21/36.61 % (1988301)------------------------------ % 258.21/36.61 % (1988301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.21/36.61 % (1988301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.21/36.61 % (1988301)CaDiCaL version: 2.1.3 % 258.21/36.61 % (1988301)Termination reason: Instruction limit % 258.21/36.61 % (1988301)Termination phase: Saturation % 258.21/36.61 % (1988301)Time elapsed: 1.037 s % 258.21/36.61 % (1988301)Peak memory usage: 23 MB % 258.21/36.61 % (1988301)Instructions burned: 1758 (million) % 258.21/36.61 % (1988303)fmb+10_1_sil=64000:si=on:random_seed=220686693:i=44122:nm=2:rtra=on:gsp=on_2768 on theBenchmark for (2768ds/44122Mi) % 258.21/36.61 % (1988303)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 258.21/36.61 % (1988303)Terminated due to inappropriate strategy. % 258.21/36.61 % (1988303)------------------------------ % 258.21/36.61 % (1988303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.21/36.61 % (1988303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.21/36.61 % (1988303)CaDiCaL version: 2.1.3 % 258.21/36.61 % (1988303)Termination reason: Inappropriate % 258.21/36.61 % (1988303)Time elapsed: 0.002 s % 258.21/36.61 % (1988303)Peak memory usage: 10 MB % 258.21/36.61 % (1988303)Instructions burned: 2 (million) % 258.21/36.61 % (1988303)------------------------------ % 258.21/36.61 % (1988303)------------------------------ % 258.21/36.61 % (1988305)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=641957977:i=19030:nm=5:rtra=on_2768 on theBenchmark for (2768ds/19030Mi) % 284.46/40.35 % (1988305)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.46/40.35 % (1988305)Terminated due to inappropriate strategy. % 284.46/40.35 % (1988305)------------------------------ % 284.46/40.35 % (1988305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.46/40.35 % (1988305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.46/40.35 % (1988305)CaDiCaL version: 2.1.3 % 284.46/40.35 % (1988305)Termination reason: Inappropriate % 284.46/40.35 % (1988305)Time elapsed: 0.002 s % 284.46/40.35 % (1988305)Peak memory usage: 10 MB % 284.46/40.35 % (1988305)Instructions burned: 2 (million) % 284.46/40.35 % (1988305)------------------------------ % 284.46/40.35 % (1988305)------------------------------ % 284.46/40.35 % (1988307)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=176267288:fmbsr=1.7:i=1840:rtra=on_2768 on theBenchmark for (2768ds/1840Mi) % 284.46/40.35 % (1988307)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.46/40.35 % (1988307)Terminated due to inappropriate strategy. % 284.46/40.35 % (1988307)------------------------------ % 284.46/40.35 % (1988307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.46/40.35 % (1988307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.46/40.35 % (1988307)CaDiCaL version: 2.1.3 % 284.46/40.35 % (1988307)Termination reason: Inappropriate % 284.46/40.35 % (1988307)Time elapsed: 0.002 s % 284.46/40.35 % (1988307)Peak memory usage: 10 MB % 284.46/40.35 % (1988307)Instructions burned: 2 (million) % 284.46/40.35 % (1988307)------------------------------ % 284.46/40.35 % (1988307)------------------------------ % 284.46/40.35 % (1988309)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2409928723:i=10262:rtra=on_2767 on theBenchmark for (2767ds/10262Mi) % 284.46/40.35 % (1988309)Instruction limit reached! % 284.46/40.35 % (1988309)------------------------------ % 284.46/40.35 % (1988309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.46/40.35 % (1988309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.46/40.35 % (1988309)CaDiCaL version: 2.1.3 % 284.46/40.35 % (1988309)Termination reason: Instruction limit % 284.46/40.35 % (1988309)Termination phase: Saturation % 284.46/40.35 % (1988309)Time elapsed: 6.047 s % 284.46/40.35 % (1988309)Peak memory usage: 75 MB % 284.46/40.35 % (1988309)Instructions burned: 10262 (million) % 284.46/40.35 % (1988517)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1157711742:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2707 on theBenchmark for (2707ds/2944Mi) % 284.46/40.35 % (1988257)Instruction limit reached! % 284.46/40.35 % (1988257)------------------------------ % 284.46/40.35 % (1988257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.46/40.35 % (1988257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.46/40.35 % (1988257)CaDiCaL version: 2.1.3 % 284.46/40.35 % (1988257)Termination reason: Instruction limit % 284.46/40.35 % (1988257)Termination phase: Saturation % 284.46/40.35 % (1988257)Time elapsed: 12.377 s % 284.46/40.35 % (1988257)Peak memory usage: 26 MB % 284.46/40.35 % (1988257)Instructions burned: 28120 (million) % 284.46/40.35 % (1988530)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1820767007:i=12648:rtra=on_2705 on theBenchmark for (2705ds/12648Mi) % 284.46/40.35 % (1988530)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.46/40.35 % (1988530)Terminated due to inappropriate strategy. % 284.46/40.35 % (1988530)------------------------------ % 284.46/40.35 % (1988530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.46/40.35 % (1988530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.46/40.35 % (1988530)CaDiCaL version: 2.1.3 % 284.46/40.35 % (1988530)Termination reason: Inappropriate % 284.46/40.35 % (1988530)Time elapsed: 0.002 s % 284.46/40.35 % (1988530)Peak memory usage: 10 MB % 284.46/40.35 % (1988530)Instructions burned: 2 (million) % 284.46/40.35 % (1988530)------------------------------ % 284.46/40.35 % (1988530)------------------------------ % 284.46/40.35 % (1988544)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2777560597:fmbsr=2.30978:i=4348:rtra=on_2705 on theBenchmark for (2705ds/4348Mi) % 284.46/40.35 % (1988544)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.46/40.35 % (1988544)Terminated due to inappropriate strategy. % 284.46/40.35 % (1988544)------------------------------ % 284.46/40.35 % (1988544)VersiTerminated % 300.08/42.54 % Vampire exiting % 300.08/42.54 Terminated %------------------------------------------------------------------------------