%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW578_2 : TPTP v9.3.1. Released v6.1.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:28 PM UTC 2026 % Result : Timeout 300.58s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW578_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.23 % Computer : n017.cluster.edu % 0.11/0.23 % Model : x86_64 x86_64 % 0.11/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.23 % Memory : 8046.5625MB % 0.11/0.23 % OS : Linux 6.8.0-71-generic % 0.11/0.23 % CPULimit : 300 % 0.11/0.23 % WCLimit : 300 % 0.11/0.23 % DateTime : Mon Sep 28 14:15:21 UTC 2026 % 0.11/0.23 % CPUTime : % 0.11/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.26/0.28 Running first-order model finding % 0.26/0.28 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 % 5.09/1.09 % (3582441)Will run a generic schedule for satisfiability detection. % 5.09/1.09 % (3582446)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3858990916_2999 on theBenchmark for (2999ds/0Mi) % 5.09/1.09 % (3582448)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3361878847:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 5.09/1.09 % (3582446)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.09/1.09 % (3582446)Terminated due to inappropriate strategy. % 5.09/1.09 % (3582446)------------------------------ % 5.09/1.09 % (3582446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.09/1.09 % (3582446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.09/1.09 % (3582446)CaDiCaL version: 2.1.3 % 5.09/1.09 % (3582446)Termination reason: Inappropriate % 5.09/1.09 % (3582446)Time elapsed: 0.005 s % 5.09/1.09 % (3582446)Peak memory usage: 11 MB % 5.09/1.09 % (3582446)Instructions burned: 13 (million) % 5.09/1.09 % (3582446)------------------------------ % 5.09/1.09 % (3582446)------------------------------ % 5.09/1.09 % (3582447)% WARNING: option uhcvi not known. % 5.09/1.09 % (3582451)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1264592258:i=131_2999 on theBenchmark for (2999ds/131Mi) % 5.09/1.09 % (3582449)dis+10_1_sil=32000:sp=arity:random_seed=3909272395:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 5.09/1.09 % (3582450)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2744162875:i=116_2999 on theBenchmark for (2999ds/116Mi) % 5.09/1.09 % (3582452)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2718912902:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 5.09/1.09 % (3582447)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2029379340:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 5.09/1.09 % (3582456)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=663761827:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 5.09/1.09 % (3582456)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.09/1.09 % (3582456)Terminated due to inappropriate strategy. % 5.09/1.09 % (3582456)------------------------------ % 5.09/1.09 % (3582456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.09/1.09 % (3582456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.09/1.09 % (3582456)CaDiCaL version: 2.1.3 % 5.09/1.09 % (3582456)Termination reason: Inappropriate % 5.09/1.09 % (3582456)Time elapsed: 0.003 s % 5.09/1.09 % (3582456)Peak memory usage: 10 MB % 5.09/1.09 % (3582456)Instructions burned: 10 (million) % 5.09/1.09 % (3582456)------------------------------ % 5.09/1.09 % (3582456)------------------------------ % 5.09/1.09 % (3582463)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=468306236:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 5.09/1.09 % (3582463)Instruction limit reached! % 5.09/1.09 % (3582463)------------------------------ % 5.09/1.09 % (3582463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.09/1.09 % (3582463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.09/1.09 % (3582463)CaDiCaL version: 2.1.3 % 5.09/1.09 % (3582463)Termination reason: Instruction limit % 5.09/1.09 % (3582463)Termination phase: Saturation % 5.09/1.09 % (3582463)Time elapsed: 0.050 s % 5.09/1.09 % (3582463)Peak memory usage: 13 MB % 5.09/1.09 % (3582463)Instructions burned: 131 (million) % 5.09/1.09 % (3582465)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=1834811766:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.09/1.09 % (3582450)Instruction limit reached! % 5.09/1.09 % (3582450)------------------------------ % 5.09/1.09 % (3582450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.09/1.09 % (3582450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.09/1.09 % (3582450)CaDiCaL version: 2.1.3 % 5.09/1.09 % (3582450)Termination reason: Instruction limit % 5.09/1.09 % (3582450)Termination phase: Saturation % 5.09/1.09 % (3582450)Time elapsed: 0.105 s % 5.09/1.09 % (3582450)Peak memory usage: 13 MB % 5.09/1.09 % (3582450)Instructions burned: 116 (million) % 5.09/1.09 % (3582449)Instruction limit reached! % 5.09/1.09 % (3582449)------------------------------ % 5.09/1.09 % (3582449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.09/1.59 % (3582449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.09/1.59 % (3582449)CaDiCaL version: 2.1.3 % 8.09/1.59 % (3582449)Termination reason: Instruction limit % 8.09/1.59 % (3582449)Termination phase: Saturation % 8.09/1.59 % (3582449)Time elapsed: 0.108 s % 8.09/1.59 % (3582449)Peak memory usage: 13 MB % 8.09/1.59 % (3582449)Instructions burned: 103 (million) % 8.09/1.59 % (3582468)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=744105114:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.09/1.59 % (3582451)Instruction limit reached! % 8.09/1.59 % (3582451)------------------------------ % 8.09/1.59 % (3582451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.09/1.59 % (3582451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.09/1.59 % (3582451)CaDiCaL version: 2.1.3 % 8.09/1.59 % (3582451)Termination reason: Instruction limit % 8.09/1.59 % (3582451)Termination phase: Saturation % 8.09/1.59 % (3582451)Time elapsed: 0.137 s % 8.09/1.59 % (3582451)Peak memory usage: 13 MB % 8.09/1.59 % (3582451)Instructions burned: 132 (million) % 8.09/1.59 % (3582467)ott-21_1_sil=16000:fs=off:random_seed=981148393:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.09/1.59 % (3582471)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=94572039:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 8.09/1.59 % (3582471)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.09/1.59 % (3582471)Terminated due to inappropriate strategy. % 8.09/1.59 % (3582471)------------------------------ % 8.09/1.59 % (3582471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.09/1.59 % (3582471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.09/1.59 % (3582471)CaDiCaL version: 2.1.3 % 8.09/1.59 % (3582471)Termination reason: Inappropriate % 8.09/1.59 % (3582471)Time elapsed: 0.008 s % 8.09/1.59 % (3582471)Peak memory usage: 11 MB % 8.09/1.59 % (3582471)Instructions burned: 10 (million) % 8.09/1.59 % (3582471)------------------------------ % 8.09/1.59 % (3582471)------------------------------ % 8.09/1.59 % (3582452)Instruction limit reached! % 8.09/1.59 % (3582452)------------------------------ % 8.09/1.59 % (3582452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.09/1.59 % (3582452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.09/1.59 % (3582452)CaDiCaL version: 2.1.3 % 8.09/1.59 % (3582452)Termination reason: Instruction limit % 8.09/1.59 % (3582452)Termination phase: Saturation % 8.09/1.59 % (3582452)Time elapsed: 0.183 s % 8.09/1.59 % (3582452)Peak memory usage: 14 MB % 8.09/1.59 % (3582452)Instructions burned: 161 (million) % 8.09/1.59 % (3582474)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3163647696:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 8.09/1.59 % (3582475)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3085933006:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 8.09/1.59 % (3582475)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.09/1.59 % (3582475)Terminated due to inappropriate strategy. % 8.09/1.59 % (3582475)------------------------------ % 8.09/1.59 % (3582475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.09/1.59 % (3582475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.09/1.59 % (3582475)CaDiCaL version: 2.1.3 % 8.09/1.59 % (3582475)Termination reason: Inappropriate % 8.09/1.59 % (3582475)Time elapsed: 0.011 s % 8.09/1.59 % (3582475)Peak memory usage: 10 MB % 8.09/1.59 % (3582475)Instructions burned: 10 (million) % 8.09/1.59 % (3582475)------------------------------ % 8.09/1.59 % (3582475)------------------------------ % 8.09/1.59 % (3582478)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=141282196: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) % 8.09/1.59 % (3582467)Instruction limit reached! % 8.09/1.59 % (3582467)------------------------------ % 8.09/1.59 % (3582467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.09/1.59 % (3582467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.09/1.59 % (3582467)CaDiCaL version: 2.1.3 % 8.09/1.59 % (3582467)Termination reason: Instruction limit % 8.09/1.59 % (3582467)Termination phase: Saturation % 32.94/5.03 % (3582467)Time elapsed: 0.163 s % 32.94/5.03 % (3582467)Peak memory usage: 12 MB % 32.94/5.03 % (3582467)Instructions burned: 181 (million) % 32.94/5.03 % (3582481)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2672785602:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 32.94/5.03 % (3582468)Instruction limit reached! % 32.94/5.03 % (3582468)------------------------------ % 32.94/5.03 % (3582468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.94/5.03 % (3582468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.94/5.03 % (3582468)CaDiCaL version: 2.1.3 % 32.94/5.03 % (3582468)Termination reason: Instruction limit % 32.94/5.03 % (3582468)Termination phase: Saturation % 32.94/5.03 % (3582468)Time elapsed: 0.426 s % 32.94/5.03 % (3582468)Peak memory usage: 14 MB % 32.94/5.03 % (3582468)Instructions burned: 477 (million) % 32.94/5.03 % (3582485)fmb+10_1_sil=64000:random_seed=1784785230:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 32.94/5.03 % (3582485)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 32.94/5.03 % (3582485)Terminated due to inappropriate strategy. % 32.94/5.03 % (3582485)------------------------------ % 32.94/5.03 % (3582485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.94/5.03 % (3582485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.94/5.03 % (3582485)CaDiCaL version: 2.1.3 % 32.94/5.03 % (3582485)Termination reason: Inappropriate % 32.94/5.03 % (3582485)Time elapsed: 0.010 s % 32.94/5.03 % (3582485)Peak memory usage: 10 MB % 32.94/5.03 % (3582485)Instructions burned: 10 (million) % 32.94/5.03 % (3582485)------------------------------ % 32.94/5.03 % (3582485)------------------------------ % 32.94/5.03 % (3582487)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2588741342:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi) % 32.94/5.03 % (3582487)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 32.94/5.03 % (3582487)Terminated due to inappropriate strategy. % 32.94/5.03 % (3582487)------------------------------ % 32.94/5.03 % (3582487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.94/5.03 % (3582487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.94/5.03 % (3582487)CaDiCaL version: 2.1.3 % 32.94/5.03 % (3582487)Termination reason: Inappropriate % 32.94/5.03 % (3582487)Time elapsed: 0.007 s % 32.94/5.03 % (3582487)Peak memory usage: 11 MB % 32.94/5.03 % (3582487)Instructions burned: 10 (million) % 32.94/5.03 % (3582487)------------------------------ % 32.94/5.03 % (3582487)------------------------------ % 32.94/5.03 % (3582465)Instruction limit reached! % 32.94/5.03 % (3582465)------------------------------ % 32.94/5.03 % (3582465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.94/5.03 % (3582465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.94/5.03 % (3582465)CaDiCaL version: 2.1.3 % 32.94/5.03 % (3582465)Termination reason: Instruction limit % 32.94/5.03 % (3582465)Termination phase: Saturation % 32.94/5.03 % (3582465)Time elapsed: 0.554 s % 32.94/5.03 % (3582465)Peak memory usage: 17 MB % 32.94/5.03 % (3582465)Instructions burned: 684 (million) % 32.94/5.03 % (3582490)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=271357197:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 32.94/5.03 % (3582490)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 32.94/5.03 % (3582490)Terminated due to inappropriate strategy. % 32.94/5.03 % (3582490)------------------------------ % 32.94/5.03 % (3582490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.94/5.03 % (3582490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.94/5.03 % (3582490)CaDiCaL version: 2.1.3 % 32.94/5.03 % (3582490)Termination reason: Inappropriate % 32.94/5.03 % (3582490)Time elapsed: 0.006 s % 32.94/5.03 % (3582490)Peak memory usage: 11 MB % 32.94/5.03 % (3582490)Instructions burned: 10 (million) % 32.94/5.03 % (3582490)------------------------------ % 32.94/5.03 % (3582490)------------------------------ % 32.94/5.03 % (3582491)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1947890228:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 32.94/5.03 % (3582493)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4181177543:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi) % 32.94/5.03 % (3582474)Instruction limit reached! % 32.94/5.03 % (3582474)------------------------------ % 41.63/6.18 % (3582474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.63/6.18 % (3582474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.63/6.18 % (3582474)CaDiCaL version: 2.1.3 % 41.63/6.18 % (3582474)Termination reason: Instruction limit % 41.63/6.18 % (3582474)Termination phase: Saturation % 41.63/6.18 % (3582474)Time elapsed: 0.567 s % 41.63/6.18 % (3582474)Peak memory usage: 17 MB % 41.63/6.18 % (3582474)Instructions burned: 1180 (million) % 41.63/6.18 % (3582497)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=997143563:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 41.63/6.18 % (3582497)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.63/6.18 % (3582497)Terminated due to inappropriate strategy. % 41.63/6.18 % (3582497)------------------------------ % 41.63/6.18 % (3582497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.63/6.18 % (3582497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.63/6.18 % (3582497)CaDiCaL version: 2.1.3 % 41.63/6.18 % (3582497)Termination reason: Inappropriate % 41.63/6.18 % (3582497)Time elapsed: 0.006 s % 41.63/6.18 % (3582497)Peak memory usage: 11 MB % 41.63/6.18 % (3582497)Instructions burned: 13 (million) % 41.63/6.18 % (3582497)------------------------------ % 41.63/6.18 % (3582497)------------------------------ % 41.63/6.18 % (3582499)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=353564900:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi) % 41.63/6.18 % (3582499)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.63/6.18 % (3582499)Terminated due to inappropriate strategy. % 41.63/6.18 % (3582499)------------------------------ % 41.63/6.18 % (3582499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.63/6.18 % (3582499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.63/6.18 % (3582499)CaDiCaL version: 2.1.3 % 41.63/6.18 % (3582499)Termination reason: Inappropriate % 41.63/6.18 % (3582499)Time elapsed: 0.006 s % 41.63/6.18 % (3582499)Peak memory usage: 10 MB % 41.63/6.18 % (3582499)Instructions burned: 10 (million) % 41.63/6.18 % (3582499)------------------------------ % 41.63/6.18 % (3582499)------------------------------ % 41.63/6.18 % (3582502)ott-2_1_sil=16000:newcnf=on:random_seed=1858633303:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2991 on theBenchmark for (2991ds/869Mi) % 41.63/6.18 % (3582478)Instruction limit reached! % 41.63/6.18 % (3582478)------------------------------ % 41.63/6.18 % (3582478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.63/6.18 % (3582478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.63/6.18 % (3582478)CaDiCaL version: 2.1.3 % 41.63/6.18 % (3582478)Termination reason: Instruction limit % 41.63/6.18 % (3582478)Termination phase: Saturation % 41.63/6.18 % (3582478)Time elapsed: 0.670 s % 41.63/6.18 % (3582478)Peak memory usage: 19 MB % 41.63/6.18 % (3582478)Instructions burned: 692 (million) % 41.63/6.18 % (3582504)ott+10_1_sil=32000:tgt=ground:random_seed=1959867324:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi) % 41.63/6.18 % (3582481)Instruction limit reached! % 41.63/6.18 % (3582481)------------------------------ % 41.63/6.18 % (3582481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.63/6.18 % (3582481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.63/6.18 % (3582481)CaDiCaL version: 2.1.3 % 41.63/6.18 % (3582481)Termination reason: Instruction limit % 41.63/6.18 % (3582481)Termination phase: Saturation % 41.63/6.18 % (3582481)Time elapsed: 0.869 s % 41.63/6.18 % (3582481)Peak memory usage: 19 MB % 41.63/6.18 % (3582481)Instructions burned: 879 (million) % 41.63/6.18 % (3582507)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4026657015:i=54282_2987 on theBenchmark for (2987ds/54282Mi) % 41.63/6.18 % (3582507)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.63/6.18 % (3582507)Terminated due to inappropriate strategy. % 41.63/6.18 % (3582507)------------------------------ % 41.63/6.18 % (3582507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.63/6.18 % (3582507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.63/6.18 % (3582507)CaDiCaL version: 2.1.3 % 41.63/6.18 % (3582507)Termination reason: Inappropriate % 41.63/6.18 % (3582507)Time elapsed: 0.013 s % 41.63/6.18 % (3582507)Peak memory usage: 11 MB % 41.63/6.18 % (3582507)Instructions burned: 13 (million) % 131.67/18.99 % (3582507)------------------------------ % 131.67/18.99 % (3582507)------------------------------ % 131.67/18.99 % (3582510)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3088595419:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi) % 131.67/18.99 % (3582502)Instruction limit reached! % 131.67/18.99 % (3582502)------------------------------ % 131.67/18.99 % (3582502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.67/18.99 % (3582502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.67/18.99 % (3582502)CaDiCaL version: 2.1.3 % 131.67/18.99 % (3582502)Termination reason: Instruction limit % 131.67/18.99 % (3582502)Termination phase: Saturation % 131.67/18.99 % (3582502)Time elapsed: 0.482 s % 131.67/18.99 % (3582502)Peak memory usage: 16 MB % 131.67/18.99 % (3582502)Instructions burned: 870 (million) % 131.67/18.99 % (3582512)dis+21_1_sil=32000:sas=cadical:random_seed=1042814985:i=3773:amm=off_2986 on theBenchmark for (2986ds/3773Mi) % 131.67/18.99 % (3582493)Instruction limit reached! % 131.67/18.99 % (3582493)------------------------------ % 131.67/18.99 % (3582493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.67/18.99 % (3582493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.67/18.99 % (3582493)CaDiCaL version: 2.1.3 % 131.67/18.99 % (3582493)Termination reason: Instruction limit % 131.67/18.99 % (3582493)Termination phase: Saturation % 131.67/18.99 % (3582493)Time elapsed: 1.426 s % 131.67/18.99 % (3582493)Peak memory usage: 24 MB % 131.67/18.99 % (3582493)Instructions burned: 1473 (million) % 131.67/18.99 % (3582517)ott+11_1_sil=16000:gs=on:random_seed=2516945191:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi) % 131.67/18.99 % (3582512)Instruction limit reached! % 131.67/18.99 % (3582512)------------------------------ % 131.67/18.99 % (3582512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.67/18.99 % (3582512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.67/18.99 % (3582512)CaDiCaL version: 2.1.3 % 131.67/18.99 % (3582512)Termination reason: Instruction limit % 131.67/18.99 % (3582512)Termination phase: Saturation % 131.67/18.99 % (3582512)Time elapsed: 1.964 s % 131.67/18.99 % (3582512)Peak memory usage: 27 MB % 131.67/18.99 % (3582512)Instructions burned: 3774 (million) % 131.67/18.99 % (3582525)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1492929875:fmbsr=1.6:i=67534_2966 on theBenchmark for (2966ds/67534Mi) % 131.67/18.99 % (3582525)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 131.67/18.99 % (3582525)Terminated due to inappropriate strategy. % 131.67/18.99 % (3582525)------------------------------ % 131.67/18.99 % (3582525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.67/18.99 % (3582525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.67/18.99 % (3582525)CaDiCaL version: 2.1.3 % 131.67/18.99 % (3582525)Termination reason: Inappropriate % 131.67/18.99 % (3582525)Time elapsed: 0.005 s % 131.67/18.99 % (3582525)Peak memory usage: 11 MB % 131.67/18.99 % (3582525)Instructions burned: 10 (million) % 131.67/18.99 % (3582525)------------------------------ % 131.67/18.99 % (3582525)------------------------------ % 131.67/18.99 % (3582527)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2883832347:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2966 on theBenchmark for (2966ds/4591Mi) % 131.67/18.99 % (3582517)Instruction limit reached! % 131.67/18.99 % (3582517)------------------------------ % 131.67/18.99 % (3582517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.67/18.99 % (3582517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.67/18.99 % (3582517)CaDiCaL version: 2.1.3 % 131.67/18.99 % (3582517)Termination reason: Instruction limit % 131.67/18.99 % (3582517)Termination phase: Saturation % 131.67/18.99 % (3582517)Time elapsed: 1.944 s % 131.67/18.99 % (3582517)Peak memory usage: 16 MB % 131.67/18.99 % (3582517)Instructions burned: 2251 (million) % 131.67/18.99 % (3582529)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3193879957:i=29340_2958 on theBenchmark for (2958ds/29340Mi) % 131.67/18.99 % (3582510)Instruction limit reached! % 131.67/18.99 % (3582510)------------------------------ % 131.67/18.99 % (3582510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.67/18.99 % (3582510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.67/18.99 % (3582510)CaDiCaL version: 2.1.3 % 131.67/18.99 % (3582510)Termination reason: Instruction limit % 164.26/23.43 % (3582510)Termination phase: Saturation % 164.26/23.43 % (3582510)Time elapsed: 3.414 s % 164.26/23.43 % (3582510)Peak memory usage: 32 MB % 164.26/23.43 % (3582510)Instructions burned: 3512 (million) % 164.26/23.43 % (3582533)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=724839480:i=5211_2952 on theBenchmark for (2952ds/5211Mi) % 164.26/23.43 % (3582491)Instruction limit reached! % 164.26/23.43 % (3582491)------------------------------ % 164.26/23.43 % (3582491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.26/23.43 % (3582491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.26/23.43 % (3582491)CaDiCaL version: 2.1.3 % 164.26/23.43 % (3582491)Termination reason: Instruction limit % 164.26/23.43 % (3582491)Termination phase: Saturation % 164.26/23.43 % (3582491)Time elapsed: 4.586 s % 164.26/23.43 % (3582491)Peak memory usage: 26 MB % 164.26/23.43 % (3582491)Instructions burned: 5132 (million) % 164.26/23.43 % (3582537)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1964838681:i=5497:nm=2_2946 on theBenchmark for (2946ds/5497Mi) % 164.26/23.43 % (3582537)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 164.26/23.43 % (3582537)Terminated due to inappropriate strategy. % 164.26/23.43 % (3582537)------------------------------ % 164.26/23.43 % (3582537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.26/23.43 % (3582537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.26/23.43 % (3582537)CaDiCaL version: 2.1.3 % 164.26/23.43 % (3582537)Termination reason: Inappropriate % 164.26/23.43 % (3582537)Time elapsed: 0.009 s % 164.26/23.43 % (3582537)Peak memory usage: 11 MB % 164.26/23.43 % (3582537)Instructions burned: 12 (million) % 164.26/23.43 % (3582537)------------------------------ % 164.26/23.43 % (3582537)------------------------------ % 164.26/23.43 % (3582540)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3618122395:fmbsr=2:i=46332_2946 on theBenchmark for (2946ds/46332Mi) % 164.26/23.43 % (3582540)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 164.26/23.43 % (3582540)Terminated due to inappropriate strategy. % 164.26/23.43 % (3582540)------------------------------ % 164.26/23.43 % (3582540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.26/23.43 % (3582540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.26/23.43 % (3582540)CaDiCaL version: 2.1.3 % 164.26/23.43 % (3582540)Termination reason: Inappropriate % 164.26/23.43 % (3582540)Time elapsed: 0.008 s % 164.26/23.43 % (3582540)Peak memory usage: 11 MB % 164.26/23.43 % (3582540)Instructions burned: 10 (million) % 164.26/23.43 % (3582540)------------------------------ % 164.26/23.43 % (3582540)------------------------------ % 164.26/23.43 % (3582542)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=588376957:i=14071_2946 on theBenchmark for (2946ds/14071Mi) % 164.26/23.43 % (3582542)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 164.26/23.43 % (3582542)Terminated due to inappropriate strategy. % 164.26/23.43 % (3582542)------------------------------ % 164.26/23.43 % (3582542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.26/23.43 % (3582542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.26/23.43 % (3582542)CaDiCaL version: 2.1.3 % 164.26/23.43 % (3582542)Termination reason: Inappropriate % 164.26/23.43 % (3582542)Time elapsed: 0.010 s % 164.26/23.43 % (3582542)Peak memory usage: 11 MB % 164.26/23.43 % (3582542)Instructions burned: 10 (million) % 164.26/23.43 % (3582542)------------------------------ % 164.26/23.43 % (3582542)------------------------------ % 164.26/23.43 % (3582544)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2807451689:i=22565:add=on:rawr=on_2945 on theBenchmark for (2945ds/22565Mi) % 164.26/23.43 % (3582527)Instruction limit reached! % 164.26/23.43 % (3582527)------------------------------ % 164.26/23.43 % (3582527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.26/23.43 % (3582527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.26/23.43 % (3582527)CaDiCaL version: 2.1.3 % 164.26/23.43 % (3582527)Termination reason: Instruction limit % 164.26/23.43 % (3582527)Termination phase: Saturation % 164.26/23.43 % (3582527)Time elapsed: 2.239 s % 164.26/23.43 % (3582527)Peak memory usage: 42 MB % 164.26/23.43 % (3582527)Instructions burned: 4592 (million) % 164.26/23.43 % (3582547)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=253310464:i=8173:av=off_2943 on theBenchmark for (2943ds/8173Mi) % 164.26/23.43 % (3582504)Instruction limit reached! % 164.98/23.57 % (3582504)------------------------------ % 164.98/23.57 % (3582504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.98/23.57 % (3582504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.98/23.57 % (3582504)CaDiCaL version: 2.1.3 % 164.98/23.57 % (3582504)Termination reason: Instruction limit % 164.98/23.57 % (3582504)Termination phase: Saturation % 164.98/23.57 % (3582504)Time elapsed: 4.866 s % 164.98/23.57 % (3582504)Peak memory usage: 40 MB % 164.98/23.57 % (3582504)Instructions burned: 5115 (million) % 164.98/23.57 % (3582551)dis+10_16:1_sil=16000:random_seed=2415989573:i=9155:fsr=off_2941 on theBenchmark for (2941ds/9155Mi) % 164.98/23.57 % (3582533)Instruction limit reached! % 164.98/23.57 % (3582533)------------------------------ % 164.98/23.57 % (3582533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.98/23.57 % (3582533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.98/23.57 % (3582533)CaDiCaL version: 2.1.3 % 164.98/23.57 % (3582533)Termination reason: Instruction limit % 164.98/23.57 % (3582533)Termination phase: Saturation % 164.98/23.57 % (3582533)Time elapsed: 4.677 s % 164.98/23.57 % (3582533)Peak memory usage: 58 MB % 164.98/23.57 % (3582533)Instructions burned: 5211 (million) % 164.98/23.57 % (3582576)ott-3_8_sil=64000:random_seed=1807094426:i=20139:bs=on_2905 on theBenchmark for (2905ds/20139Mi) % 164.98/23.57 % (3582547)Instruction limit reached! % 164.98/23.57 % (3582547)------------------------------ % 164.98/23.57 % (3582547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.98/23.57 % (3582547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.98/23.57 % (3582547)CaDiCaL version: 2.1.3 % 164.98/23.57 % (3582547)Termination reason: Instruction limit % 164.98/23.57 % (3582547)Termination phase: Saturation % 164.98/23.57 % (3582547)Time elapsed: 4.394 s % 164.98/23.57 % (3582547)Peak memory usage: 77 MB % 164.98/23.57 % (3582547)Instructions burned: 8174 (million) % 164.98/23.57 % (3582580)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2881633395:fmbsr=2:i=32576_2899 on theBenchmark for (2899ds/32576Mi) % 164.98/23.57 % (3582580)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 164.98/23.57 % (3582580)Terminated due to inappropriate strategy. % 164.98/23.57 % (3582580)------------------------------ % 164.98/23.57 % (3582580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.98/23.57 % (3582580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.98/23.57 % (3582580)CaDiCaL version: 2.1.3 % 164.98/23.57 % (3582580)Termination reason: Inappropriate % 164.98/23.57 % (3582580)Time elapsed: 0.006 s % 164.98/23.57 % (3582580)Peak memory usage: 11 MB % 164.98/23.57 % (3582580)Instructions burned: 13 (million) % 164.98/23.57 % (3582580)------------------------------ % 164.98/23.57 % (3582580)------------------------------ % 164.98/23.57 % (3582582)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3275913094:i=11404_2899 on theBenchmark for (2899ds/11404Mi) % 164.98/23.57 % (3582551)Instruction limit reached! % 164.98/23.57 % (3582551)------------------------------ % 164.98/23.57 % (3582551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.98/23.57 % (3582551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.98/23.57 % (3582551)CaDiCaL version: 2.1.3 % 164.98/23.57 % (3582551)Termination reason: Instruction limit % 164.98/23.57 % (3582551)Termination phase: Saturation % 164.98/23.57 % (3582551)Time elapsed: 7.857 s % 164.98/23.57 % (3582551)Peak memory usage: 54 MB % 164.98/23.57 % (3582551)Instructions burned: 9155 (million) % 164.98/23.57 % (3582620)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1849015037:i=14134_2862 on theBenchmark for (2862ds/14134Mi) % 164.98/23.57 % (3582576)Instruction limit reached! % 164.98/23.57 % (3582576)------------------------------ % 164.98/23.57 % (3582576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.98/23.57 % (3582576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.98/23.57 % (3582576)CaDiCaL version: 2.1.3 % 164.98/23.57 % (3582576)Termination reason: Instruction limit % 164.98/23.57 % (3582576)Termination phase: Saturation % 164.98/23.57 % (3582576)Time elapsed: 8.458 s % 164.98/23.57 % (3582576)Peak memory usage: 117 MB % 164.98/23.57 % (3582576)Instructions burned: 20141 (million) % 164.98/23.57 % (3582763)dis+33_16_sil=32000:sac=on:random_seed=903274851:i=15851:nm=0_2820 on theBenchmark for (2820ds/15851Mi) % 164.98/23.57 % (3582582)Instruction limit reached! % 164.98/23.57 % (3582582)------------------------------ % 164.98/23.57 % (3582582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.22/26.87 % (3582582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.22/26.87 % (3582582)CaDiCaL version: 2.1.3 % 188.22/26.87 % (3582582)Termination reason: Instruction limit % 188.22/26.87 % (3582582)Termination phase: Saturation % 188.22/26.87 % (3582582)Time elapsed: 8.554 s % 188.22/26.87 % (3582582)Peak memory usage: 60 MB % 188.22/26.87 % (3582582)Instructions burned: 11405 (million) % 188.22/26.87 % (3582765)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1019614281:avsq=on:i=17627:add=on:amm=off_2812 on theBenchmark for (2812ds/17627Mi) % 188.22/26.87 % (3582763)Instruction limit reached! % 188.22/26.87 % (3582763)------------------------------ % 188.22/26.87 % (3582763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.22/26.87 % (3582763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.22/26.87 % (3582763)CaDiCaL version: 2.1.3 % 188.22/26.87 % (3582763)Termination reason: Instruction limit % 188.22/26.87 % (3582763)Termination phase: Saturation % 188.22/26.87 % (3582763)Time elapsed: 4.323 s % 188.22/26.87 % (3582763)Peak memory usage: 144 MB % 188.22/26.87 % (3582763)Instructions burned: 15852 (million) % 188.22/26.87 % (3582767)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3907582005:s2a=on:i=53295_2776 on theBenchmark for (2776ds/53295Mi) % 188.22/26.87 % (3582620)Instruction limit reached! % 188.22/26.87 % (3582620)------------------------------ % 188.22/26.87 % (3582620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.22/26.87 % (3582620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.22/26.87 % (3582620)CaDiCaL version: 2.1.3 % 188.22/26.87 % (3582620)Termination reason: Instruction limit % 188.22/26.87 % (3582620)Termination phase: Saturation % 188.22/26.87 % (3582620)Time elapsed: 8.894 s % 188.22/26.87 % (3582620)Peak memory usage: 79 MB % 188.22/26.87 % (3582620)Instructions burned: 14134 (million) % 188.22/26.87 % (3582769)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=236065627:i=26857:ins=20_2772 on theBenchmark for (2772ds/26857Mi) % 188.22/26.87 % (3582769)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 188.22/26.87 % (3582769)Terminated due to inappropriate strategy. % 188.22/26.87 % (3582769)------------------------------ % 188.22/26.87 % (3582769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.22/26.87 % (3582769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.22/26.87 % (3582769)CaDiCaL version: 2.1.3 % 188.22/26.87 % (3582769)Termination reason: Inappropriate % 188.22/26.87 % (3582769)Time elapsed: 0.005 s % 188.22/26.87 % (3582769)Peak memory usage: 10 MB % 188.22/26.87 % (3582769)Instructions burned: 10 (million) % 188.22/26.87 % (3582769)------------------------------ % 188.22/26.87 % (3582769)------------------------------ % 188.22/26.87 % (3582771)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3475047956:i=28120:bs=on:fsr=off_2772 on theBenchmark for (2772ds/28120Mi) % 188.22/26.87 % (3582529)Instruction limit reached! % 188.22/26.87 % (3582529)------------------------------ % 188.22/26.87 % (3582529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.22/26.87 % (3582529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.22/26.87 % (3582529)CaDiCaL version: 2.1.3 % 188.22/26.87 % (3582529)Termination reason: Instruction limit % 188.22/26.87 % (3582529)Termination phase: Saturation % 188.22/26.87 % (3582529)Time elapsed: 18.939 s % 188.22/26.87 % (3582529)Peak memory usage: 76 MB % 188.22/26.87 % (3582529)Instructions burned: 29341 (million) % 188.22/26.87 % (3582773)fmb+10_1_sil=256000:fmbss=7:random_seed=4037360540:fmbsr=1.6:i=182295_2769 on theBenchmark for (2769ds/182295Mi) % 188.22/26.87 % (3582773)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 188.22/26.87 % (3582773)Terminated due to inappropriate strategy. % 188.22/26.87 % (3582773)------------------------------ % 188.22/26.87 % (3582773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.22/26.87 % (3582773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.22/26.87 % (3582773)CaDiCaL version: 2.1.3 % 188.22/26.87 % (3582773)Termination reason: Inappropriate % 188.22/26.87 % (3582773)Time elapsed: 0.005 s % 188.22/26.87 % (3582773)Peak memory usage: 10 MB % 188.22/26.87 % (3582773)Instructions burned: 10 (million) % 188.22/26.87 % (3582773)------------------------------ % 188.22/26.87 % (3582773)------------------------------ % 188.22/26.87 % (3582775)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2021912978:i=44625:gsp=on_2768 on theBenchmark for (2768ds/44625Mi) % 201.90/28.71 % (3582775)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 201.90/28.71 % (3582775)Terminated due to inappropriate strategy. % 201.90/28.71 % (3582775)------------------------------ % 201.90/28.71 % (3582775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.90/28.71 % (3582775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.90/28.71 % (3582775)CaDiCaL version: 2.1.3 % 201.90/28.71 % (3582775)Termination reason: Inappropriate % 201.90/28.71 % (3582775)Time elapsed: 0.015 s % 201.90/28.71 % (3582775)Peak memory usage: 11 MB % 201.90/28.71 % (3582775)Instructions burned: 35 (million) % 201.90/28.71 % (3582775)------------------------------ % 201.90/28.71 % (3582775)------------------------------ % 201.90/28.71 % (3582777)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3248947985:i=160505_2768 on theBenchmark for (2768ds/160505Mi) % 201.90/28.71 % (3582777)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 201.90/28.71 % (3582777)Terminated due to inappropriate strategy. % 201.90/28.71 % (3582777)------------------------------ % 201.90/28.71 % (3582777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.90/28.71 % (3582777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.90/28.71 % (3582777)CaDiCaL version: 2.1.3 % 201.90/28.71 % (3582777)Termination reason: Inappropriate % 201.90/28.71 % (3582777)Time elapsed: 0.005 s % 201.90/28.71 % (3582777)Peak memory usage: 10 MB % 201.90/28.71 % (3582777)Instructions burned: 10 (million) % 201.90/28.71 % (3582777)------------------------------ % 201.90/28.71 % (3582777)------------------------------ % 201.90/28.71 % (3582779)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3141058998:fmbsr=1.3:i=225729_2768 on theBenchmark for (2768ds/225729Mi) % 201.90/28.71 % (3582779)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 201.90/28.71 % (3582779)Terminated due to inappropriate strategy. % 201.90/28.71 % (3582779)------------------------------ % 201.90/28.71 % (3582779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.90/28.71 % (3582779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.90/28.71 % (3582779)CaDiCaL version: 2.1.3 % 201.90/28.71 % (3582779)Termination reason: Inappropriate % 201.90/28.71 % (3582779)Time elapsed: 0.006 s % 201.90/28.71 % (3582779)Peak memory usage: 11 MB % 201.90/28.71 % (3582779)Instructions burned: 10 (million) % 201.90/28.71 % (3582779)------------------------------ % 201.90/28.71 % (3582779)------------------------------ % 201.90/28.71 % (3582781)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=348355949:fmbsr=2:i=185024:ins=7_2767 on theBenchmark for (2767ds/185024Mi) % 201.90/28.71 % (3582781)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 201.90/28.71 % (3582781)Terminated due to inappropriate strategy. % 201.90/28.71 % (3582781)------------------------------ % 201.90/28.71 % (3582781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.90/28.71 % (3582781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.90/28.71 % (3582781)CaDiCaL version: 2.1.3 % 201.90/28.71 % (3582781)Termination reason: Inappropriate % 201.90/28.71 % (3582781)Time elapsed: 0.005 s % 201.90/28.71 % (3582781)Peak memory usage: 11 MB % 201.90/28.71 % (3582781)Instructions burned: 10 (million) % 201.90/28.71 % (3582781)------------------------------ % 201.90/28.71 % (3582781)------------------------------ % 201.90/28.71 % (3582783)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1233493159:rtra=on_2767 on theBenchmark for (2767ds/0Mi) % 201.90/28.71 % (3582783)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 201.90/28.71 % (3582783)Terminated due to inappropriate strategy. % 201.90/28.71 % (3582783)------------------------------ % 201.90/28.71 % (3582783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.90/28.71 % (3582783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.90/28.71 % (3582783)CaDiCaL version: 2.1.3 % 201.90/28.71 % (3582783)Termination reason: Inappropriate % 201.90/28.71 % (3582783)Time elapsed: 0.007 s % 201.90/28.71 % (3582783)Peak memory usage: 11 MB % 201.90/28.71 % (3582783)Instructions burned: 13 (million) % 201.90/28.71 % (3582783)------------------------------ % 201.90/28.71 % (3582783)------------------------------ % 201.90/28.71 % (3582785)% WARNING: option uhcvi not known. % 201.90/28.71 % (3582785)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2970982169:i=271062:add=off:rtra=on:rawr=on_2767 on theBenchmark for (2767ds/271062Mi) % 227.45/32.32 % (3582544)Instruction limit reached! % 227.45/32.32 % (3582544)------------------------------ % 227.45/32.32 % (3582544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.45/32.32 % (3582544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.45/32.32 % (3582544)CaDiCaL version: 2.1.3 % 227.45/32.32 % (3582544)Termination reason: Instruction limit % 227.45/32.32 % (3582544)Termination phase: Saturation % 227.45/32.32 % (3582544)Time elapsed: 18.276 s % 227.45/32.32 % (3582544)Peak memory usage: 98 MB % 227.45/32.32 % (3582544)Instructions burned: 22566 (million) % 227.45/32.32 % (3582787)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4283925760:i=176048:add=on:rtra=on:rawr=on_2762 on theBenchmark for (2762ds/176048Mi) % 227.45/32.32 % (3582765)Instruction limit reached! % 227.45/32.32 % (3582765)------------------------------ % 227.45/32.32 % (3582765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.45/32.32 % (3582765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.45/32.32 % (3582765)CaDiCaL version: 2.1.3 % 227.45/32.32 % (3582765)Termination reason: Instruction limit % 227.45/32.32 % (3582765)Termination phase: Saturation % 227.45/32.32 % (3582765)Time elapsed: 7.081 s % 227.45/32.32 % (3582765)Peak memory usage: 67 MB % 227.45/32.32 % (3582765)Instructions burned: 17630 (million) % 227.45/32.32 % (3582789)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4120496479:i=206:fgj=on:rtra=on_2741 on theBenchmark for (2741ds/206Mi) % 227.45/32.32 % (3582789)Instruction limit reached! % 227.45/32.32 % (3582789)------------------------------ % 227.45/32.32 % (3582789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.45/32.32 % (3582789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.45/32.32 % (3582789)CaDiCaL version: 2.1.3 % 227.45/32.32 % (3582789)Termination reason: Instruction limit % 227.45/32.32 % (3582789)Termination phase: Saturation % 227.45/32.32 % (3582789)Time elapsed: 0.131 s % 227.45/32.32 % (3582789)Peak memory usage: 13 MB % 227.45/32.32 % (3582789)Instructions burned: 206 (million) % 227.45/32.32 % (3582791)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1053786115:i=232:rtra=on_2740 on theBenchmark for (2740ds/232Mi) % 227.45/32.32 % (3582791)Instruction limit reached! % 227.45/32.32 % (3582791)------------------------------ % 227.45/32.32 % (3582791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.45/32.32 % (3582791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.45/32.32 % (3582791)CaDiCaL version: 2.1.3 % 227.45/32.32 % (3582791)Termination reason: Instruction limit % 227.45/32.32 % (3582791)Termination phase: Saturation % 227.45/32.32 % (3582791)Time elapsed: 0.133 s % 227.45/32.32 % (3582791)Peak memory usage: 14 MB % 227.45/32.32 % (3582791)Instructions burned: 233 (million) % 227.45/32.32 % (3582793)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=549229552:i=262:rtra=on_2738 on theBenchmark for (2738ds/262Mi) % 227.45/32.32 % (3582793)Instruction limit reached! % 227.45/32.32 % (3582793)------------------------------ % 227.45/32.32 % (3582793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.45/32.32 % (3582793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.45/32.32 % (3582793)CaDiCaL version: 2.1.3 % 227.45/32.32 % (3582793)Termination reason: Instruction limit % 227.45/32.32 % (3582793)Termination phase: Saturation % 227.45/32.32 % (3582793)Time elapsed: 0.174 s % 227.45/32.32 % (3582793)Peak memory usage: 15 MB % 227.45/32.32 % (3582793)Instructions burned: 262 (million) % 227.45/32.32 % (3582795)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=631574887:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2736 on theBenchmark for (2736ds/318Mi) % 227.45/32.32 % (3582795)Instruction limit reached! % 227.45/32.32 % (3582795)------------------------------ % 227.45/32.32 % (3582795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.45/32.32 % (3582795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.45/32.32 % (3582795)CaDiCaL version: 2.1.3 % 227.45/32.32 % (3582795)Termination reason: Instruction limit % 227.45/32.32 % (3582795)Termination phase: Saturation % 227.45/32.32 % (3582795)Time elapsed: 0.229 s % 227.45/32.32 % (3582795)Peak memory usage: 15 MB % 227.45/32.32 % (3582795)Instructions burned: 319 (million) % 227.45/32.32 % (3582797)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2932931512:i=1428:nm=2:rtra=on_2734 on theBenchmark for (2734ds/1428Mi) % 253.74/36.04 % (3582797)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 253.74/36.04 % (3582797)Terminated due to inappropriate strategy. % 253.74/36.04 % (3582797)------------------------------ % 253.74/36.04 % (3582797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.74/36.04 % (3582797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.74/36.04 % (3582797)CaDiCaL version: 2.1.3 % 253.74/36.04 % (3582797)Termination reason: Inappropriate % 253.74/36.04 % (3582797)Time elapsed: 0.006 s % 253.74/36.04 % (3582797)Peak memory usage: 10 MB % 253.74/36.04 % (3582797)Instructions burned: 10 (million) % 253.74/36.04 % (3582797)------------------------------ % 253.74/36.04 % (3582797)------------------------------ % 253.74/36.04 % (3582799)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=836686089:i=262:bd=preordered:rtra=on:fsd=on_2734 on theBenchmark for (2734ds/262Mi) % 253.74/36.04 % (3582799)Instruction limit reached! % 253.74/36.04 % (3582799)------------------------------ % 253.74/36.04 % (3582799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.74/36.04 % (3582799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.74/36.04 % (3582799)CaDiCaL version: 2.1.3 % 253.74/36.04 % (3582799)Termination reason: Instruction limit % 253.74/36.04 % (3582799)Termination phase: Saturation % 253.74/36.04 % (3582799)Time elapsed: 0.171 s % 253.74/36.04 % (3582799)Peak memory usage: 14 MB % 253.74/36.04 % (3582799)Instructions burned: 263 (million) % 253.74/36.04 % (3582801)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=605389195:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2732 on theBenchmark for (2732ds/1368Mi) % 253.74/36.04 % (3582801)Instruction limit reached! % 253.74/36.04 % (3582801)------------------------------ % 253.74/36.04 % (3582801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.74/36.04 % (3582801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.74/36.04 % (3582801)CaDiCaL version: 2.1.3 % 253.74/36.04 % (3582801)Termination reason: Instruction limit % 253.74/36.04 % (3582801)Termination phase: Saturation % 253.74/36.04 % (3582801)Time elapsed: 0.690 s % 253.74/36.04 % (3582801)Peak memory usage: 19 MB % 253.74/36.04 % (3582801)Instructions burned: 1368 (million) % 253.74/36.04 % (3582803)ott-21_1_sil=16000:si=on:fs=off:random_seed=4112242126:i=360:av=off:fsr=off:rtra=on_2725 on theBenchmark for (2725ds/360Mi) % 253.74/36.04 % (3582803)Instruction limit reached! % 253.74/36.04 % (3582803)------------------------------ % 253.74/36.04 % (3582803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.74/36.04 % (3582803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.74/36.04 % (3582803)CaDiCaL version: 2.1.3 % 253.74/36.04 % (3582803)Termination reason: Instruction limit % 253.74/36.04 % (3582803)Termination phase: Saturation % 253.74/36.04 % (3582803)Time elapsed: 0.183 s % 253.74/36.04 % (3582803)Peak memory usage: 13 MB % 253.74/36.04 % (3582803)Instructions burned: 362 (million) % 253.74/36.04 % (3582805)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2233390335:i=954:bd=all:rtra=on_2723 on theBenchmark for (2723ds/954Mi) % 253.74/36.04 % (3582805)Instruction limit reached! % 253.74/36.04 % (3582805)------------------------------ % 253.74/36.04 % (3582805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.74/36.04 % (3582805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.74/36.04 % (3582805)CaDiCaL version: 2.1.3 % 253.74/36.04 % (3582805)Termination reason: Instruction limit % 253.74/36.04 % (3582805)Termination phase: Saturation % 253.74/36.04 % (3582805)Time elapsed: 0.676 s % 253.74/36.04 % (3582805)Peak memory usage: 17 MB % 253.74/36.04 % (3582805)Instructions burned: 955 (million) % 253.74/36.04 % (3582807)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2666827729:fmbsr=1.3:i=1730:ins=25:rtra=on_2716 on theBenchmark for (2716ds/1730Mi) % 253.74/36.04 % (3582807)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 253.74/36.04 % (3582807)Terminated due to inappropriate strategy. % 253.74/36.04 % (3582807)------------------------------ % 253.74/36.04 % (3582807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.74/36.04 % (3582807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.74/36.04 % (3582807)CaDiCaL version: 2.1.3 % 253.74/36.04 % (3582807)Termination reason: Inappropriate % 269.39/40.82 % (3582807)Time elapsed: 0.006 s % 269.39/40.82 % (3582807)Peak memory usage: 10 MB % 269.39/40.82 % (3582807)Instructions burned: 11 (million) % 269.39/40.82 % (3582807)------------------------------ % 269.39/40.82 % (3582807)------------------------------ % 269.39/40.82 % (3582809)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1817953488:i=2358:rtra=on_2715 on theBenchmark for (2715ds/2358Mi) % 269.39/40.82 % (3582809)Instruction limit reached! % 269.39/40.82 % (3582809)------------------------------ % 269.39/40.82 % (3582809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.39/40.82 % (3582809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.39/40.82 % (3582809)CaDiCaL version: 2.1.3 % 269.39/40.82 % (3582809)Termination reason: Instruction limit % 269.39/40.82 % (3582809)Termination phase: Saturation % 269.39/40.82 % (3582809)Time elapsed: 1.576 s % 269.39/40.82 % (3582809)Peak memory usage: 26 MB % 269.39/40.82 % (3582809)Instructions burned: 2359 (million) % 269.39/40.82 % (3582873)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2891424865:i=1778:ins=1:rtra=on_2699 on theBenchmark for (2699ds/1778Mi) % 269.39/40.82 % (3582873)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.39/40.82 % (3582873)Terminated due to inappropriate strategy. % 269.39/40.82 % (3582873)------------------------------ % 269.39/40.82 % (3582873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.39/40.82 % (3582873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.39/40.82 % (3582873)CaDiCaL version: 2.1.3 % 269.39/40.82 % (3582873)Termination reason: Inappropriate % 269.39/40.82 % (3582873)Time elapsed: 0.006 s % 269.39/40.82 % (3582873)Peak memory usage: 11 MB % 269.39/40.82 % (3582873)Instructions burned: 11 (million) % 269.39/40.82 % (3582873)------------------------------ % 269.39/40.82 % (3582873)------------------------------ % 269.39/40.82 % (3582875)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=1496289616:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2699 on theBenchmark for (2699ds/1384Mi) % 269.39/40.82 % (3582875)Instruction limit reached! % 269.39/40.82 % (3582875)------------------------------ % 269.39/40.82 % (3582875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.39/40.82 % (3582875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.39/40.82 % (3582875)CaDiCaL version: 2.1.3 % 269.39/40.82 % (3582875)Termination reason: Instruction limit % 269.39/40.82 % (3582875)Termination phase: Saturation % 269.39/40.82 % (3582875)Time elapsed: 0.827 s % 269.39/40.82 % (3582875)Peak memory usage: 22 MB % 269.39/40.82 % (3582875)Instructions burned: 1385 (million) % 269.39/40.82 % (3582877)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3156463738:i=1758:kws=inv_precedence:fsr=off:rtra=on_2691 on theBenchmark for (2691ds/1758Mi) % 269.39/40.82 % (3582877)Instruction limit reached! % 269.39/40.82 % (3582877)------------------------------ % 269.39/40.82 % (3582877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.39/40.82 % (3582877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.39/40.82 % (3582877)CaDiCaL version: 2.1.3 % 269.39/40.82 % (3582877)Termination reason: Instruction limit % 269.39/40.82 % (3582877)Termination phase: Saturation % 269.39/40.82 % (3582877)Time elapsed: 1.063 s % 269.39/40.82 % (3582877)Peak memory usage: 25 MB % 269.39/40.82 % (3582877)Instructions burned: 1759 (million) % 269.39/40.82 % (3582879)fmb+10_1_sil=64000:si=on:random_seed=774164535:i=44122:nm=2:rtra=on:gsp=on_2680 on theBenchmark for (2680ds/44122Mi) % 269.39/40.82 % (3582879)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.39/40.82 % (3582879)Terminated due to inappropriate strategy. % 269.39/40.82 % (3582879)------------------------------ % 269.39/40.82 % (3582879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.39/40.82 % (3582879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.39/40.82 % (3582879)CaDiCaL version: 2.1.3 % 269.39/40.82 % (3582879)Termination reason: Inappropriate % 269.39/40.82 % (3582879)Time elapsed: 0.006 s % 269.39/40.82 % (3582879)Peak memory usage: 10 MB % 269.39/40.82 % (3582879)Instructions burned: 11 (million) % 269.39/40.82 % (3582879)------------------------------ % 269.39/40.82 % (3582879)------------------------------ % 269.39/40.82 % (3582881)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1969739315:i=19030:nm=5:rtra=on_2679 on theBenchmark for (2679ds/19030Mi) % 300.58/42.64 % (3582881)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.58/42.64 % (3582881)Terminated due to inappropriate strategy. % 300.58/42.64 % (3582881)------------------------------ % 300.58/42.64 % (3582881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.58/42.64 % (3582881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/42.64 % (3582881)CaDiCaL version: 2.1.3 % 300.58/42.64 % (3582881)Termination reason: Inappropriate % 300.58/42.64 % (3582881)Time elapsed: 0.006 s % 300.58/42.64 % (3582881)Peak memory usage: 11 MB % 300.58/42.64 % (3582881)Instructions burned: 10 (million) % 300.58/42.64 % (3582881)------------------------------ % 300.58/42.64 % (3582881)------------------------------ % 300.58/42.64 % (3582883)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=95880214:fmbsr=1.7:i=1840:rtra=on_2679 on theBenchmark for (2679ds/1840Mi) % 300.58/42.64 % (3582883)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.58/42.64 % (3582883)Terminated due to inappropriate strategy. % 300.58/42.64 % (3582883)------------------------------ % 300.58/42.64 % (3582883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.58/42.64 % (3582883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/42.64 % (3582883)CaDiCaL version: 2.1.3 % 300.58/42.64 % (3582883)Termination reason: Inappropriate % 300.58/42.64 % (3582883)Time elapsed: 0.006 s % 300.58/42.64 % (3582883)Peak memory usage: 10 MB % 300.58/42.64 % (3582883)Instructions burned: 11 (million) % 300.58/42.64 % (3582883)------------------------------ % 300.58/42.64 % (3582883)------------------------------ % 300.58/42.64 % (3582885)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3585156508:i=10262:rtra=on_2679 on theBenchmark for (2679ds/10262Mi) % 300.58/42.64 % (3582767)Instruction limit reached! % 300.58/42.64 % (3582767)------------------------------ % 300.58/42.64 % (3582767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.58/42.64 % (3582767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/42.64 % (3582767)CaDiCaL version: 2.1.3 % 300.58/42.64 % (3582767)Termination reason: Instruction limit % 300.58/42.64 % (3582767)Termination phase: Saturation % 300.58/42.64 % (3582767)Time elapsed: 12.409 s % 300.58/42.64 % (3582767)Peak memory usage: 134 MB % 300.58/42.64 % (3582767)Instructions burned: 53298 (million) % 300.58/42.64 % (3582887)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1626102191:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2652 on theBenchmark for (2652ds/2944Mi) % 300.58/42.64 % (3582887)Instruction limit reached! % 300.58/42.64 % (3582887)------------------------------ % 300.58/42.64 % (3582887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.58/42.64 % (3582887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/42.64 % (3582887)CaDiCaL version: 2.1.3 % 300.58/42.64 % (3582887)Termination reason: Instruction limit % 300.58/42.64 % (3582887)Termination phase: Saturation % 300.58/42.64 % (3582887)Time elapsed: 0.955 s % 300.58/42.64 % (3582887)Peak memory usage: 34 MB % 300.58/42.64 % (3582887)Instructions burned: 2947 (million) % 300.58/42.64 % (3582889)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3732369617:i=12648:rtra=on_2642 on theBenchmark for (2642ds/12648Mi) % 300.58/42.64 % (3582889)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.58/42.64 % (3582889)Terminated due to inappropriate strategy. % 300.58/42.64 % (3582889)------------------------------ % 300.58/42.64 % (3582889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.58/42.64 % (3582889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/42.64 % (3582889)CaDiCaL version: 2.1.3 % 300.58/42.64 % (3582889)Termination reason: Inappropriate % 300.58/42.64 % (3582889)Time elapsed: 0.004 s % 300.58/42.64 % (3582889)Peak memory usage: 11 MB % 300.58/42.64 % (3582889)Instructions burned: 13 (million) % 300.58/42.64 % (3582889)------------------------------ % 300.58/42.64 % (3582889)------------------------------ % 300.58/42.64 % (3582891)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2132089594:fmbsr=2.30978:i=4348:rtra=on_2642 on theBenchmark for (2642ds/4348Mi) % 300.58/42.64 % (3582891)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.58/42.64 % (3582891)Terminated due to inappropriate strategy. % 300.58/42.64 % (3582891)-------------------------- % 300.58/42.64 Terminated % 300.58/42.64 % Vampire exiting % 300.58/42.64 Terminated %------------------------------------------------------------------------------