%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW839_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/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:45:03 PM UTC 2026 % Result : Timeout 295.82s 41.94s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW839_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.20 % Computer : n010.cluster.edu % 0.07/0.20 % Model : x86_64 x86_64 % 0.07/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.20 % Memory : 8046.5625MB % 0.07/0.20 % OS : Linux 6.8.0-71-generic % 0.07/0.20 % CPULimit : 300 % 0.07/0.20 % WCLimit : 300 % 0.07/0.20 % DateTime : Mon Sep 28 14:32:54 UTC 2026 % 0.07/0.20 % CPUTime : % 0.07/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.23 Running first-order model finding % 0.07/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.25/0.70 % (1968511)Will run a generic schedule for satisfiability detection. % 3.25/0.70 % (1968521)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=172392618:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.25/0.70 % (1968517)% WARNING: option uhcvi not known. % 3.25/0.70 % (1968517)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2207714860:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.25/0.70 % (1968519)dis+10_1_sil=32000:sp=arity:random_seed=4112873050:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.25/0.70 % (1968518)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1618398338:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.25/0.70 % (1968520)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1577017507:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.25/0.70 % (1968522)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=693134511:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.25/0.70 % (1968516)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=783179163_2999 on theBenchmark for (2999ds/0Mi) % 3.25/0.70 % (1968516)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.25/0.70 % (1968516)Terminated due to inappropriate strategy. % 3.25/0.70 % (1968516)------------------------------ % 3.25/0.70 % (1968516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.25/0.70 % (1968516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.25/0.70 % (1968516)CaDiCaL version: 2.1.3 % 3.25/0.70 % (1968516)Termination reason: Inappropriate % 3.25/0.70 % (1968516)Time elapsed: 0.014 s % 3.25/0.70 % (1968516)Peak memory usage: 11 MB % 3.25/0.70 % (1968516)Instructions burned: 28 (million) % 3.25/0.70 % (1968516)------------------------------ % 3.25/0.70 % (1968516)------------------------------ % 3.25/0.70 % (1968521)Instruction limit reached! % 3.25/0.70 % (1968521)------------------------------ % 3.25/0.70 % (1968521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.25/0.70 % (1968521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.25/0.70 % (1968521)CaDiCaL version: 2.1.3 % 3.25/0.70 % (1968521)Termination reason: Instruction limit % 3.25/0.70 % (1968521)Termination phase: Saturation % 3.25/0.70 % (1968521)Time elapsed: 0.041 s % 3.25/0.70 % (1968521)Peak memory usage: 13 MB % 3.25/0.70 % (1968521)Instructions burned: 134 (million) % 3.25/0.70 % (1968530)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2991847505:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.25/0.70 % (1968531)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=819595271:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.25/0.70 % (1968530)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.25/0.70 % (1968530)Terminated due to inappropriate strategy. % 3.25/0.70 % (1968530)------------------------------ % 3.25/0.70 % (1968530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.25/0.70 % (1968530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.25/0.70 % (1968530)CaDiCaL version: 2.1.3 % 3.25/0.70 % (1968530)Termination reason: Inappropriate % 3.25/0.70 % (1968530)Time elapsed: 0.013 s % 3.25/0.70 % (1968530)Peak memory usage: 11 MB % 3.25/0.70 % (1968530)Instructions burned: 28 (million) % 3.25/0.70 % (1968530)------------------------------ % 3.25/0.70 % (1968530)------------------------------ % 3.25/0.70 % (1968519)Instruction limit reached! % 3.25/0.70 % (1968519)------------------------------ % 3.25/0.70 % (1968519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.25/0.70 % (1968519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.25/0.70 % (1968519)CaDiCaL version: 2.1.3 % 3.25/0.70 % (1968519)Termination reason: Instruction limit % 3.25/0.70 % (1968519)Termination phase: Saturation % 3.25/0.70 % (1968519)Time elapsed: 0.058 s % 3.25/0.70 % (1968519)Peak memory usage: 13 MB % 3.25/0.70 % (1968519)Instructions burned: 104 (million) % 3.25/0.70 % (1968520)Instruction limit reached! % 3.25/0.70 % (1968520)------------------------------ % 3.25/0.70 % (1968520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.25/0.70 % (1968520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.25/0.70 % (1968520)CaDiCaL version: 2.1.3 % 3.25/0.70 % (1968520)Termination reason: Instruction limit % 5.60/1.05 % (1968520)Termination phase: Saturation % 5.60/1.05 % (1968520)Time elapsed: 0.066 s % 5.60/1.05 % (1968520)Peak memory usage: 13 MB % 5.60/1.05 % (1968520)Instructions burned: 118 (million) % 5.60/1.05 % (1968534)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=1186560473:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 5.60/1.05 % (1968535)ott-21_1_sil=16000:fs=off:random_seed=393422394:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 5.60/1.05 % (1968536)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1175265735:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.60/1.05 % (1968531)Instruction limit reached! % 5.60/1.05 % (1968531)------------------------------ % 5.60/1.05 % (1968531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.60/1.05 % (1968531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.05 % (1968531)CaDiCaL version: 2.1.3 % 5.60/1.05 % (1968531)Termination reason: Instruction limit % 5.60/1.05 % (1968531)Termination phase: Saturation % 5.60/1.05 % (1968531)Time elapsed: 0.044 s % 5.60/1.05 % (1968531)Peak memory usage: 14 MB % 5.60/1.05 % (1968531)Instructions burned: 132 (million) % 5.60/1.05 % (1968522)Instruction limit reached! % 5.60/1.05 % (1968522)------------------------------ % 5.60/1.05 % (1968522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.60/1.05 % (1968522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.05 % (1968522)CaDiCaL version: 2.1.3 % 5.60/1.05 % (1968522)Termination reason: Instruction limit % 5.60/1.05 % (1968522)Termination phase: Saturation % 5.60/1.05 % (1968522)Time elapsed: 0.094 s % 5.60/1.05 % (1968522)Peak memory usage: 13 MB % 5.60/1.05 % (1968522)Instructions burned: 160 (million) % 5.60/1.05 % (1968540)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=747679860:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.60/1.05 % (1968540)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.60/1.05 % (1968540)Terminated due to inappropriate strategy. % 5.60/1.05 % (1968540)------------------------------ % 5.60/1.05 % (1968540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.60/1.05 % (1968540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.05 % (1968540)CaDiCaL version: 2.1.3 % 5.60/1.05 % (1968540)Termination reason: Inappropriate % 5.60/1.05 % (1968540)Time elapsed: 0.007 s % 5.60/1.05 % (1968540)Peak memory usage: 11 MB % 5.60/1.05 % (1968540)Instructions burned: 28 (million) % 5.60/1.05 % (1968540)------------------------------ % 5.60/1.05 % (1968540)------------------------------ % 5.60/1.05 % (1968541)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2356569252:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.60/1.05 % (1968543)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2099800048:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.60/1.05 % (1968543)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.60/1.05 % (1968543)Terminated due to inappropriate strategy. % 5.60/1.05 % (1968543)------------------------------ % 5.60/1.05 % (1968543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.60/1.05 % (1968543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.05 % (1968543)CaDiCaL version: 2.1.3 % 5.60/1.05 % (1968543)Termination reason: Inappropriate % 5.60/1.05 % (1968543)Time elapsed: 0.007 s % 5.60/1.05 % (1968543)Peak memory usage: 11 MB % 5.60/1.05 % (1968543)Instructions burned: 28 (million) % 5.60/1.05 % (1968543)------------------------------ % 5.60/1.05 % (1968543)------------------------------ % 5.60/1.05 % (1968546)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=283822115:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 5.60/1.05 % (1968535)Instruction limit reached! % 5.60/1.05 % (1968535)------------------------------ % 5.60/1.05 % (1968535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.60/1.05 % (1968535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.05 % (1968535)CaDiCaL version: 2.1.3 % 5.60/1.05 % (1968535)Termination reason: Instruction limit % 5.60/1.05 % (1968535)Termination phase: Saturation % 16.71/2.79 % (1968535)Time elapsed: 0.082 s % 16.71/2.79 % (1968535)Peak memory usage: 13 MB % 16.71/2.79 % (1968535)Instructions burned: 181 (million) % 16.71/2.79 % (1968548)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4021767980:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 16.71/2.79 % (1968546)Instruction limit reached! % 16.71/2.79 % (1968546)------------------------------ % 16.71/2.79 % (1968546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.71/2.79 % (1968546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.71/2.79 % (1968546)CaDiCaL version: 2.1.3 % 16.71/2.79 % (1968546)Termination reason: Instruction limit % 16.71/2.79 % (1968546)Termination phase: Saturation % 16.71/2.79 % (1968546)Time elapsed: 0.231 s % 16.71/2.79 % (1968546)Peak memory usage: 19 MB % 16.71/2.79 % (1968546)Instructions burned: 694 (million) % 16.71/2.79 % (1968536)Instruction limit reached! % 16.71/2.79 % (1968536)------------------------------ % 16.71/2.79 % (1968536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.71/2.79 % (1968536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.71/2.79 % (1968536)CaDiCaL version: 2.1.3 % 16.71/2.79 % (1968536)Termination reason: Instruction limit % 16.71/2.79 % (1968536)Termination phase: Saturation % 16.71/2.79 % (1968536)Time elapsed: 0.282 s % 16.71/2.79 % (1968536)Peak memory usage: 15 MB % 16.71/2.79 % (1968536)Instructions burned: 478 (million) % 16.71/2.79 % (1968550)fmb+10_1_sil=64000:random_seed=3603200316:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 16.71/2.79 % (1968550)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.71/2.79 % (1968550)Terminated due to inappropriate strategy. % 16.71/2.79 % (1968550)------------------------------ % 16.71/2.79 % (1968550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.71/2.79 % (1968550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.71/2.79 % (1968550)CaDiCaL version: 2.1.3 % 16.71/2.79 % (1968550)Termination reason: Inappropriate % 16.71/2.79 % (1968550)Time elapsed: 0.007 s % 16.71/2.79 % (1968550)Peak memory usage: 11 MB % 16.71/2.79 % (1968550)Instructions burned: 28 (million) % 16.71/2.79 % (1968550)------------------------------ % 16.71/2.79 % (1968550)------------------------------ % 16.71/2.79 % (1968551)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3103525685:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 16.71/2.79 % (1968553)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=736256826:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 16.71/2.79 % (1968551)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.71/2.79 % (1968551)Terminated due to inappropriate strategy. % 16.71/2.79 % (1968551)------------------------------ % 16.71/2.79 % (1968551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.71/2.79 % (1968551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.71/2.79 % (1968551)CaDiCaL version: 2.1.3 % 16.71/2.79 % (1968551)Termination reason: Inappropriate % 16.71/2.79 % (1968551)Time elapsed: 0.013 s % 16.71/2.79 % (1968551)Peak memory usage: 11 MB % 16.71/2.79 % (1968551)Instructions burned: 28 (million) % 16.71/2.79 % (1968551)------------------------------ % 16.71/2.79 % (1968551)------------------------------ % 16.71/2.79 % (1968553)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.71/2.79 % (1968553)Terminated due to inappropriate strategy. % 16.71/2.79 % (1968553)------------------------------ % 16.71/2.79 % (1968553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.71/2.79 % (1968553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.71/2.79 % (1968553)CaDiCaL version: 2.1.3 % 16.71/2.79 % (1968553)Termination reason: Inappropriate % 16.71/2.79 % (1968553)Time elapsed: 0.007 s % 16.71/2.79 % (1968553)Peak memory usage: 11 MB % 16.71/2.79 % (1968553)Instructions burned: 28 (million) % 16.71/2.79 % (1968553)------------------------------ % 16.71/2.79 % (1968553)------------------------------ % 16.71/2.79 % (1968557)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=449367749:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 16.71/2.79 % (1968556)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=695074523:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 16.71/2.79 % (1968534)Instruction limit reached! % 16.71/2.79 % (1968534)------------------------------ % 22.92/3.60 % (1968534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.92/3.60 % (1968534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.92/3.60 % (1968534)CaDiCaL version: 2.1.3 % 22.92/3.60 % (1968534)Termination reason: Instruction limit % 22.92/3.60 % (1968534)Termination phase: Saturation % 22.92/3.60 % (1968534)Time elapsed: 0.350 s % 22.92/3.60 % (1968534)Peak memory usage: 16 MB % 22.92/3.60 % (1968534)Instructions burned: 684 (million) % 22.92/3.60 % (1968560)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2921026639:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 22.92/3.60 % (1968560)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.92/3.60 % (1968560)Terminated due to inappropriate strategy. % 22.92/3.60 % (1968560)------------------------------ % 22.92/3.60 % (1968560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.92/3.60 % (1968560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.92/3.60 % (1968560)CaDiCaL version: 2.1.3 % 22.92/3.60 % (1968560)Termination reason: Inappropriate % 22.92/3.60 % (1968560)Time elapsed: 0.013 s % 22.92/3.60 % (1968560)Peak memory usage: 11 MB % 22.92/3.60 % (1968560)Instructions burned: 28 (million) % 22.92/3.60 % (1968560)------------------------------ % 22.92/3.60 % (1968560)------------------------------ % 22.92/3.60 % (1968562)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2785392979:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 22.92/3.60 % (1968562)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.92/3.60 % (1968562)Terminated due to inappropriate strategy. % 22.92/3.60 % (1968562)------------------------------ % 22.92/3.60 % (1968562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.92/3.60 % (1968562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.92/3.60 % (1968562)CaDiCaL version: 2.1.3 % 22.92/3.60 % (1968562)Termination reason: Inappropriate % 22.92/3.60 % (1968562)Time elapsed: 0.013 s % 22.92/3.60 % (1968562)Peak memory usage: 11 MB % 22.92/3.60 % (1968562)Instructions burned: 28 (million) % 22.92/3.60 % (1968562)------------------------------ % 22.92/3.60 % (1968562)------------------------------ % 22.92/3.60 % (1968564)ott-2_1_sil=16000:newcnf=on:random_seed=1429009028:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 22.92/3.60 % (1968548)Instruction limit reached! % 22.92/3.60 % (1968548)------------------------------ % 22.92/3.60 % (1968548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.92/3.60 % (1968548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.92/3.60 % (1968548)CaDiCaL version: 2.1.3 % 22.92/3.60 % (1968548)Termination reason: Instruction limit % 22.92/3.60 % (1968548)Termination phase: Saturation % 22.92/3.60 % (1968548)Time elapsed: 0.474 s % 22.92/3.60 % (1968548)Peak memory usage: 17 MB % 22.92/3.60 % (1968548)Instructions burned: 879 (million) % 22.92/3.60 % (1968566)ott+10_1_sil=32000:tgt=ground:random_seed=2378038213:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 22.92/3.60 % (1968541)Instruction limit reached! % 22.92/3.60 % (1968541)------------------------------ % 22.92/3.60 % (1968541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.92/3.60 % (1968541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.92/3.60 % (1968541)CaDiCaL version: 2.1.3 % 22.92/3.60 % (1968541)Termination reason: Instruction limit % 22.92/3.60 % (1968541)Termination phase: Saturation % 22.92/3.60 % (1968541)Time elapsed: 0.620 s % 22.92/3.60 % (1968541)Peak memory usage: 21 MB % 22.92/3.60 % (1968541)Instructions burned: 1179 (million) % 22.92/3.60 % (1968568)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1252407085:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 22.92/3.60 % (1968568)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.92/3.60 % (1968568)Terminated due to inappropriate strategy. % 22.92/3.60 % (1968568)------------------------------ % 22.92/3.60 % (1968568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.92/3.60 % (1968568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.92/3.60 % (1968568)CaDiCaL version: 2.1.3 % 22.92/3.60 % (1968568)Termination reason: Inappropriate % 22.92/3.60 % (1968568)Time elapsed: 0.013 s % 22.92/3.60 % (1968568)Peak memory usage: 11 MB % 22.92/3.60 % (1968568)Instructions burned: 28 (million) % 111.25/15.99 % (1968568)------------------------------ % 111.25/15.99 % (1968568)------------------------------ % 111.25/15.99 % (1968570)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2407451005:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 111.25/15.99 % (1968557)Instruction limit reached! % 111.25/15.99 % (1968557)------------------------------ % 111.25/15.99 % (1968557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.25/15.99 % (1968557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.25/15.99 % (1968557)CaDiCaL version: 2.1.3 % 111.25/15.99 % (1968557)Termination reason: Instruction limit % 111.25/15.99 % (1968557)Termination phase: Saturation % 111.25/15.99 % (1968557)Time elapsed: 0.446 s % 111.25/15.99 % (1968557)Peak memory usage: 28 MB % 111.25/15.99 % (1968557)Instructions burned: 1472 (million) % 111.25/15.99 % (1968572)dis+21_1_sil=32000:sas=cadical:random_seed=2102483611:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi) % 111.25/15.99 % (1968564)Instruction limit reached! % 111.25/15.99 % (1968564)------------------------------ % 111.25/15.99 % (1968564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.25/15.99 % (1968564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.25/15.99 % (1968564)CaDiCaL version: 2.1.3 % 111.25/15.99 % (1968564)Termination reason: Instruction limit % 111.25/15.99 % (1968564)Termination phase: Saturation % 111.25/15.99 % (1968564)Time elapsed: 0.472 s % 111.25/15.99 % (1968564)Peak memory usage: 19 MB % 111.25/15.99 % (1968564)Instructions burned: 870 (million) % 111.25/15.99 % (1968574)ott+11_1_sil=16000:gs=on:random_seed=2376133334:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi) % 111.25/15.99 % (1968572)Instruction limit reached! % 111.25/15.99 % (1968572)------------------------------ % 111.25/15.99 % (1968572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.25/15.99 % (1968572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.25/15.99 % (1968572)CaDiCaL version: 2.1.3 % 111.25/15.99 % (1968572)Termination reason: Instruction limit % 111.25/15.99 % (1968572)Termination phase: Saturation % 111.25/15.99 % (1968572)Time elapsed: 0.986 s % 111.25/15.99 % (1968572)Peak memory usage: 33 MB % 111.25/15.99 % (1968572)Instructions burned: 3773 (million) % 111.25/15.99 % (1968576)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3526433771:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 111.25/15.99 % (1968576)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.25/15.99 % (1968576)Terminated due to inappropriate strategy. % 111.25/15.99 % (1968576)------------------------------ % 111.25/15.99 % (1968576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.25/15.99 % (1968576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.25/15.99 % (1968576)CaDiCaL version: 2.1.3 % 111.25/15.99 % (1968576)Termination reason: Inappropriate % 111.25/15.99 % (1968576)Time elapsed: 0.007 s % 111.25/15.99 % (1968576)Peak memory usage: 11 MB % 111.25/15.99 % (1968576)Instructions burned: 28 (million) % 111.25/15.99 % (1968576)------------------------------ % 111.25/15.99 % (1968576)------------------------------ % 111.25/15.99 % (1968578)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=872220507:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 111.25/15.99 % (1968574)Instruction limit reached! % 111.25/15.99 % (1968574)------------------------------ % 111.25/15.99 % (1968574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.25/15.99 % (1968574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.25/15.99 % (1968574)CaDiCaL version: 2.1.3 % 111.25/15.99 % (1968574)Termination reason: Instruction limit % 111.25/15.99 % (1968574)Termination phase: Saturation % 111.25/15.99 % (1968574)Time elapsed: 1.204 s % 111.25/15.99 % (1968574)Peak memory usage: 26 MB % 111.25/15.99 % (1968574)Instructions burned: 2252 (million) % 111.25/15.99 % (1968580)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=422153843:i=29340_2977 on theBenchmark for (2977ds/29340Mi) % 111.25/15.99 % (1968570)Instruction limit reached! % 111.25/15.99 % (1968570)------------------------------ % 111.25/15.99 % (1968570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.25/15.99 % (1968570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.25/15.99 % (1968570)CaDiCaL version: 2.1.3 % 111.25/15.99 % (1968570)Termination reason: Instruction limit % 140.75/20.10 % (1968570)Termination phase: Saturation % 140.75/20.10 % (1968570)Time elapsed: 1.723 s % 140.75/20.10 % (1968570)Peak memory usage: 32 MB % 140.75/20.10 % (1968570)Instructions burned: 3512 (million) % 140.75/20.10 % (1968582)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4165509304:i=5211_2974 on theBenchmark for (2974ds/5211Mi) % 140.75/20.10 % (1968556)Instruction limit reached! % 140.75/20.10 % (1968556)------------------------------ % 140.75/20.10 % (1968556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.75/20.10 % (1968556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.75/20.10 % (1968556)CaDiCaL version: 2.1.3 % 140.75/20.10 % (1968556)Termination reason: Instruction limit % 140.75/20.10 % (1968556)Termination phase: Saturation % 140.75/20.10 % (1968556)Time elapsed: 2.581 s % 140.75/20.10 % (1968556)Peak memory usage: 45 MB % 140.75/20.10 % (1968556)Instructions burned: 5132 (million) % 140.75/20.10 % (1968584)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2744676391:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 140.75/20.10 % (1968584)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 140.75/20.10 % (1968584)Terminated due to inappropriate strategy. % 140.75/20.10 % (1968584)------------------------------ % 140.75/20.10 % (1968584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.75/20.10 % (1968584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.75/20.10 % (1968584)CaDiCaL version: 2.1.3 % 140.75/20.10 % (1968584)Termination reason: Inappropriate % 140.75/20.10 % (1968584)Time elapsed: 0.013 s % 140.75/20.10 % (1968584)Peak memory usage: 11 MB % 140.75/20.10 % (1968584)Instructions burned: 28 (million) % 140.75/20.10 % (1968584)------------------------------ % 140.75/20.10 % (1968584)------------------------------ % 140.75/20.10 % (1968586)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1636227106:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 140.75/20.10 % (1968586)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 140.75/20.10 % (1968586)Terminated due to inappropriate strategy. % 140.75/20.10 % (1968586)------------------------------ % 140.75/20.10 % (1968586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.75/20.10 % (1968586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.75/20.10 % (1968586)CaDiCaL version: 2.1.3 % 140.75/20.10 % (1968586)Termination reason: Inappropriate % 140.75/20.10 % (1968586)Time elapsed: 0.013 s % 140.75/20.10 % (1968586)Peak memory usage: 11 MB % 140.75/20.10 % (1968586)Instructions burned: 28 (million) % 140.75/20.10 % (1968586)------------------------------ % 140.75/20.10 % (1968586)------------------------------ % 140.75/20.10 % (1968588)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=694415642:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 140.75/20.10 % (1968588)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 140.75/20.10 % (1968588)Terminated due to inappropriate strategy. % 140.75/20.10 % (1968588)------------------------------ % 140.75/20.10 % (1968588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.75/20.10 % (1968588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.75/20.10 % (1968588)CaDiCaL version: 2.1.3 % 140.75/20.10 % (1968588)Termination reason: Inappropriate % 140.75/20.10 % (1968588)Time elapsed: 0.013 s % 140.75/20.10 % (1968588)Peak memory usage: 11 MB % 140.75/20.10 % (1968588)Instructions burned: 28 (million) % 140.75/20.10 % (1968588)------------------------------ % 140.75/20.10 % (1968588)------------------------------ % 140.75/20.10 % (1968578)Instruction limit reached! % 140.75/20.10 % (1968578)------------------------------ % 140.75/20.10 % (1968578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.75/20.10 % (1968578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.75/20.10 % (1968578)CaDiCaL version: 2.1.3 % 140.75/20.10 % (1968578)Termination reason: Instruction limit % 140.75/20.10 % (1968578)Termination phase: Saturation % 140.75/20.10 % (1968578)Time elapsed: 1.221 s % 140.75/20.10 % (1968578)Peak memory usage: 39 MB % 140.75/20.10 % (1968578)Instructions burned: 4593 (million) % 140.75/20.10 % (1968591)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1145460762:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 140.75/20.10 % (1968590)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3371395612:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 140.75/20.10 % (1968566)Instruction limit reached! % 143.22/20.40 % (1968566)------------------------------ % 143.22/20.40 % (1968566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.22/20.40 % (1968566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.22/20.40 % (1968566)CaDiCaL version: 2.1.3 % 143.22/20.40 % (1968566)Termination reason: Instruction limit % 143.22/20.40 % (1968566)Termination phase: Saturation % 143.22/20.40 % (1968566)Time elapsed: 2.643 s % 143.22/20.40 % (1968566)Peak memory usage: 43 MB % 143.22/20.40 % (1968566)Instructions burned: 5115 (million) % 143.22/20.40 % (1968594)dis+10_16:1_sil=16000:random_seed=3295316907:i=9155:fsr=off_2966 on theBenchmark for (2966ds/9155Mi) % 143.22/20.40 % (1968582)Instruction limit reached! % 143.22/20.40 % (1968582)------------------------------ % 143.22/20.40 % (1968582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.22/20.40 % (1968582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.22/20.40 % (1968582)CaDiCaL version: 2.1.3 % 143.22/20.40 % (1968582)Termination reason: Instruction limit % 143.22/20.40 % (1968582)Termination phase: Saturation % 143.22/20.40 % (1968582)Time elapsed: 2.685 s % 143.22/20.40 % (1968582)Peak memory usage: 46 MB % 143.22/20.40 % (1968582)Instructions burned: 5212 (million) % 143.22/20.40 % (1968596)ott-3_8_sil=64000:random_seed=3613943474:i=20139:bs=on_2947 on theBenchmark for (2947ds/20139Mi) % 143.22/20.40 % (1968591)Instruction limit reached! % 143.22/20.40 % (1968591)------------------------------ % 143.22/20.40 % (1968591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.22/20.40 % (1968591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.22/20.40 % (1968591)CaDiCaL version: 2.1.3 % 143.22/20.40 % (1968591)Termination reason: Instruction limit % 143.22/20.40 % (1968591)Termination phase: Saturation % 143.22/20.40 % (1968591)Time elapsed: 2.299 s % 143.22/20.40 % (1968591)Peak memory usage: 60 MB % 143.22/20.40 % (1968591)Instructions burned: 8176 (million) % 143.22/20.40 % (1968598)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2272387187:fmbsr=2:i=32576_2945 on theBenchmark for (2945ds/32576Mi) % 143.22/20.40 % (1968598)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.22/20.40 % (1968598)Terminated due to inappropriate strategy. % 143.22/20.40 % (1968598)------------------------------ % 143.22/20.40 % (1968598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.22/20.40 % (1968598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.22/20.40 % (1968598)CaDiCaL version: 2.1.3 % 143.22/20.40 % (1968598)Termination reason: Inappropriate % 143.22/20.40 % (1968598)Time elapsed: 0.007 s % 143.22/20.40 % (1968598)Peak memory usage: 11 MB % 143.22/20.40 % (1968598)Instructions burned: 28 (million) % 143.22/20.40 % (1968598)------------------------------ % 143.22/20.40 % (1968598)------------------------------ % 143.22/20.40 % (1968600)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1860838322:i=11404_2945 on theBenchmark for (2945ds/11404Mi) % 143.22/20.40 % (1968594)Instruction limit reached! % 143.22/20.40 % (1968594)------------------------------ % 143.22/20.40 % (1968594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.22/20.40 % (1968594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.22/20.40 % (1968594)CaDiCaL version: 2.1.3 % 143.22/20.40 % (1968594)Termination reason: Instruction limit % 143.22/20.40 % (1968594)Termination phase: Saturation % 143.22/20.40 % (1968594)Time elapsed: 4.292 s % 143.22/20.40 % (1968594)Peak memory usage: 54 MB % 143.22/20.40 % (1968594)Instructions burned: 9155 (million) % 143.22/20.40 % (1968718)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1243240811:i=14134_2923 on theBenchmark for (2923ds/14134Mi) % 143.22/20.40 % (1968600)Instruction limit reached! % 143.22/20.40 % (1968600)------------------------------ % 143.22/20.40 % (1968600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.22/20.40 % (1968600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.22/20.40 % (1968600)CaDiCaL version: 2.1.3 % 143.22/20.40 % (1968600)Termination reason: Instruction limit % 143.22/20.40 % (1968600)Termination phase: Saturation % 143.22/20.40 % (1968600)Time elapsed: 3.564 s % 143.22/20.40 % (1968600)Peak memory usage: 84 MB % 143.22/20.40 % (1968600)Instructions burned: 11406 (million) % 143.22/20.40 % (1968882)dis+33_16_sil=32000:sac=on:random_seed=3611944658:i=15851:nm=0_2909 on theBenchmark for (2909ds/15851Mi) % 143.22/20.40 % (1968882)Instruction limit reached! % 143.22/20.40 % (1968882)------------------------------ % 143.22/20.40 % (1968882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.79/25.39 % (1968882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.79/25.39 % (1968882)CaDiCaL version: 2.1.3 % 177.79/25.39 % (1968882)Termination reason: Instruction limit % 177.79/25.39 % (1968882)Termination phase: Saturation % 177.79/25.39 % (1968882)Time elapsed: 6.663 s % 177.79/25.39 % (1968882)Peak memory usage: 20 MB % 177.79/25.39 % (1968882)Instructions burned: 15853 (million) % 177.79/25.39 % (1968907)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3716660108:avsq=on:i=17627:add=on:amm=off_2842 on theBenchmark for (2842ds/17627Mi) % 177.79/25.39 % (1968590)Instruction limit reached! % 177.79/25.39 % (1968590)------------------------------ % 177.79/25.39 % (1968590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.79/25.39 % (1968590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.79/25.39 % (1968590)CaDiCaL version: 2.1.3 % 177.79/25.39 % (1968590)Termination reason: Instruction limit % 177.79/25.39 % (1968590)Termination phase: Saturation % 177.79/25.39 % (1968590)Time elapsed: 12.823 s % 177.79/25.39 % (1968590)Peak memory usage: 84 MB % 177.79/25.39 % (1968590)Instructions burned: 22566 (million) % 177.79/25.39 % (1968909)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3296229398:s2a=on:i=53295_2839 on theBenchmark for (2839ds/53295Mi) % 177.79/25.39 % (1968596)Instruction limit reached! % 177.79/25.39 % (1968596)------------------------------ % 177.79/25.39 % (1968596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.79/25.39 % (1968596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.79/25.39 % (1968596)CaDiCaL version: 2.1.3 % 177.79/25.39 % (1968596)Termination reason: Instruction limit % 177.79/25.39 % (1968596)Termination phase: Saturation % 177.79/25.39 % (1968596)Time elapsed: 13.549 s % 177.79/25.39 % (1968596)Peak memory usage: 55 MB % 177.79/25.39 % (1968596)Instructions burned: 20139 (million) % 177.79/25.39 % (1968913)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3779707917:i=26857:ins=20_2811 on theBenchmark for (2811ds/26857Mi) % 177.79/25.39 % (1968913)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.79/25.39 % (1968913)Terminated due to inappropriate strategy. % 177.79/25.39 % (1968913)------------------------------ % 177.79/25.39 % (1968913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.79/25.39 % (1968913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.79/25.39 % (1968913)CaDiCaL version: 2.1.3 % 177.79/25.39 % (1968913)Termination reason: Inappropriate % 177.79/25.39 % (1968913)Time elapsed: 0.016 s % 177.79/25.39 % (1968913)Peak memory usage: 11 MB % 177.79/25.39 % (1968913)Instructions burned: 28 (million) % 177.79/25.39 % (1968913)------------------------------ % 177.79/25.39 % (1968913)------------------------------ % 177.79/25.39 % (1968915)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=704517945:i=28120:bs=on:fsr=off_2811 on theBenchmark for (2811ds/28120Mi) % 177.79/25.39 % (1968718)Instruction limit reached! % 177.79/25.39 % (1968718)------------------------------ % 177.79/25.39 % (1968718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.79/25.39 % (1968718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.79/25.39 % (1968718)CaDiCaL version: 2.1.3 % 177.79/25.39 % (1968718)Termination reason: Instruction limit % 177.79/25.39 % (1968718)Termination phase: Saturation % 177.79/25.39 % (1968718)Time elapsed: 12.034 s % 177.79/25.39 % (1968718)Peak memory usage: 92 MB % 177.79/25.39 % (1968718)Instructions burned: 14134 (million) % 177.79/25.39 % (1968919)fmb+10_1_sil=256000:fmbss=7:random_seed=2628943816:fmbsr=1.6:i=182295_2802 on theBenchmark for (2802ds/182295Mi) % 177.79/25.39 % (1968919)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.79/25.39 % (1968919)Terminated due to inappropriate strategy. % 177.79/25.39 % (1968919)------------------------------ % 177.79/25.39 % (1968919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.79/25.39 % (1968919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.79/25.39 % (1968919)CaDiCaL version: 2.1.3 % 177.79/25.39 % (1968919)Termination reason: Inappropriate % 177.79/25.39 % (1968919)Time elapsed: 0.030 s % 177.79/25.39 % (1968919)Peak memory usage: 11 MB % 177.79/25.39 % (1968919)Instructions burned: 28 (million) % 177.79/25.39 % (1968919)------------------------------ % 177.79/25.39 % (1968919)------------------------------ % 177.79/25.39 % (1968923)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=98714476:i=44625:gsp=on_2801 on theBenchmark for (2801ds/44625Mi) % 190.29/27.14 % (1968923)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.29/27.14 % (1968923)Terminated due to inappropriate strategy. % 190.29/27.14 % (1968923)------------------------------ % 190.29/27.14 % (1968923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.29/27.14 % (1968923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.29/27.14 % (1968923)CaDiCaL version: 2.1.3 % 190.29/27.14 % (1968923)Termination reason: Inappropriate % 190.29/27.14 % (1968923)Time elapsed: 0.028 s % 190.29/27.14 % (1968923)Peak memory usage: 11 MB % 190.29/27.14 % (1968923)Instructions burned: 28 (million) % 190.29/27.14 % (1968923)------------------------------ % 190.29/27.14 % (1968923)------------------------------ % 190.29/27.14 % (1968925)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2352900025:i=160505_2801 on theBenchmark for (2801ds/160505Mi) % 190.29/27.14 % (1968925)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.29/27.14 % (1968925)Terminated due to inappropriate strategy. % 190.29/27.14 % (1968925)------------------------------ % 190.29/27.14 % (1968925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.29/27.14 % (1968925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.29/27.14 % (1968925)CaDiCaL version: 2.1.3 % 190.29/27.14 % (1968925)Termination reason: Inappropriate % 190.29/27.14 % (1968925)Time elapsed: 0.027 s % 190.29/27.14 % (1968925)Peak memory usage: 11 MB % 190.29/27.14 % (1968925)Instructions burned: 28 (million) % 190.29/27.14 % (1968925)------------------------------ % 190.29/27.14 % (1968925)------------------------------ % 190.29/27.14 % (1968927)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4000430434:fmbsr=1.3:i=225729_2800 on theBenchmark for (2800ds/225729Mi) % 190.29/27.14 % (1968927)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.29/27.14 % (1968927)Terminated due to inappropriate strategy. % 190.29/27.14 % (1968927)------------------------------ % 190.29/27.14 % (1968927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.29/27.14 % (1968927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.29/27.14 % (1968927)CaDiCaL version: 2.1.3 % 190.29/27.14 % (1968927)Termination reason: Inappropriate % 190.29/27.14 % (1968927)Time elapsed: 0.028 s % 190.29/27.14 % (1968927)Peak memory usage: 11 MB % 190.29/27.14 % (1968927)Instructions burned: 28 (million) % 190.29/27.14 % (1968927)------------------------------ % 190.29/27.14 % (1968927)------------------------------ % 190.29/27.14 % (1968929)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1710165501:fmbsr=2:i=185024:ins=7_2799 on theBenchmark for (2799ds/185024Mi) % 190.29/27.14 % (1968929)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.29/27.14 % (1968929)Terminated due to inappropriate strategy. % 190.29/27.14 % (1968929)------------------------------ % 190.29/27.14 % (1968929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.29/27.14 % (1968929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.29/27.14 % (1968929)CaDiCaL version: 2.1.3 % 190.29/27.14 % (1968929)Termination reason: Inappropriate % 190.29/27.14 % (1968929)Time elapsed: 0.028 s % 190.29/27.14 % (1968929)Peak memory usage: 11 MB % 190.29/27.14 % (1968929)Instructions burned: 28 (million) % 190.29/27.14 % (1968929)------------------------------ % 190.29/27.14 % (1968929)------------------------------ % 190.29/27.14 % (1968931)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4229507837:rtra=on_2798 on theBenchmark for (2798ds/0Mi) % 190.29/27.14 % (1968931)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.29/27.14 % (1968931)Terminated due to inappropriate strategy. % 190.29/27.14 % (1968931)------------------------------ % 190.29/27.14 % (1968931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.29/27.14 % (1968931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.29/27.14 % (1968931)CaDiCaL version: 2.1.3 % 190.29/27.14 % (1968931)Termination reason: Inappropriate % 190.29/27.14 % (1968931)Time elapsed: 0.016 s % 190.29/27.14 % (1968931)Peak memory usage: 11 MB % 190.29/27.14 % (1968931)Instructions burned: 31 (million) % 190.29/27.14 % (1968931)------------------------------ % 190.29/27.14 % (1968931)------------------------------ % 190.29/27.14 % (1968933)% WARNING: option uhcvi not known. % 190.29/27.14 % (1968933)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4290911941:i=271062:add=off:rtra=on:rawr=on_2798 on theBenchmark for (2798ds/271062Mi) % 221.25/31.42 % (1968580)Instruction limit reached! % 221.25/31.42 % (1968580)------------------------------ % 221.25/31.42 % (1968580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.25/31.42 % (1968580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.25/31.42 % (1968580)CaDiCaL version: 2.1.3 % 221.25/31.42 % (1968580)Termination reason: Instruction limit % 221.25/31.42 % (1968580)Termination phase: Saturation % 221.25/31.42 % (1968580)Time elapsed: 19.061 s % 221.25/31.42 % (1968580)Peak memory usage: 49 MB % 221.25/31.42 % (1968580)Instructions burned: 29341 (million) % 221.25/31.42 % (1968935)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2765886466:i=176048:add=on:rtra=on:rawr=on_2786 on theBenchmark for (2786ds/176048Mi) % 221.25/31.42 % (1968907)Instruction limit reached! % 221.25/31.42 % (1968907)------------------------------ % 221.25/31.42 % (1968907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.25/31.42 % (1968907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.25/31.42 % (1968907)CaDiCaL version: 2.1.3 % 221.25/31.42 % (1968907)Termination reason: Instruction limit % 221.25/31.42 % (1968907)Termination phase: Saturation % 221.25/31.42 % (1968907)Time elapsed: 8.559 s % 221.25/31.42 % (1968907)Peak memory usage: 194 MB % 221.25/31.42 % (1968907)Instructions burned: 17629 (million) % 221.25/31.42 % (1968941)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1425451860:i=206:fgj=on:rtra=on_2756 on theBenchmark for (2756ds/206Mi) % 221.25/31.42 % (1968941)Instruction limit reached! % 221.25/31.42 % (1968941)------------------------------ % 221.25/31.42 % (1968941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.25/31.42 % (1968941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.25/31.42 % (1968941)CaDiCaL version: 2.1.3 % 221.25/31.42 % (1968941)Termination reason: Instruction limit % 221.25/31.42 % (1968941)Termination phase: Saturation % 221.25/31.42 % (1968941)Time elapsed: 0.105 s % 221.25/31.42 % (1968941)Peak memory usage: 14 MB % 221.25/31.42 % (1968941)Instructions burned: 208 (million) % 221.25/31.42 % (1968943)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2630049423:i=232:rtra=on_2754 on theBenchmark for (2754ds/232Mi) % 221.25/31.42 % (1968943)Instruction limit reached! % 221.25/31.42 % (1968943)------------------------------ % 221.25/31.42 % (1968943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.25/31.42 % (1968943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.25/31.42 % (1968943)CaDiCaL version: 2.1.3 % 221.25/31.42 % (1968943)Termination reason: Instruction limit % 221.25/31.42 % (1968943)Termination phase: Saturation % 221.25/31.42 % (1968943)Time elapsed: 0.126 s % 221.25/31.42 % (1968943)Peak memory usage: 15 MB % 221.25/31.42 % (1968943)Instructions burned: 233 (million) % 221.25/31.42 % (1968945)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2928735310:i=262:rtra=on_2753 on theBenchmark for (2753ds/262Mi) % 221.25/31.42 % (1968945)Instruction limit reached! % 221.25/31.42 % (1968945)------------------------------ % 221.25/31.42 % (1968945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.25/31.42 % (1968945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.25/31.42 % (1968945)CaDiCaL version: 2.1.3 % 221.25/31.42 % (1968945)Termination reason: Instruction limit % 221.25/31.42 % (1968945)Termination phase: Saturation % 221.25/31.42 % (1968945)Time elapsed: 0.157 s % 221.25/31.42 % (1968945)Peak memory usage: 15 MB % 221.25/31.42 % (1968945)Instructions burned: 264 (million) % 221.25/31.42 % (1968947)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=525361152:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2751 on theBenchmark for (2751ds/318Mi) % 221.25/31.42 % (1968947)Instruction limit reached! % 221.25/31.42 % (1968947)------------------------------ % 221.25/31.42 % (1968947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.25/31.42 % (1968947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.25/31.42 % (1968947)CaDiCaL version: 2.1.3 % 221.25/31.42 % (1968947)Termination reason: Instruction limit % 221.25/31.42 % (1968947)Termination phase: Saturation % 221.25/31.42 % (1968947)Time elapsed: 0.252 s % 221.25/31.42 % (1968947)Peak memory usage: 15 MB % 221.25/31.42 % (1968947)Instructions burned: 318 (million) % 221.25/31.42 % (1968949)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=626487539:i=1428:nm=2:rtra=on_2748 on theBenchmark for (2748ds/1428Mi) % 295.82/41.94 % (1968949)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 295.82/41.94 % (1968949)Terminated due to inappropriate strategy. % 295.82/41.94 % (1968949)------------------------------ % 295.82/41.94 % (1968949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.82/41.94 % (1968949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.82/41.94 % (1968949)CaDiCaL version: 2.1.3 % 295.82/41.94 % (1968949)Termination reason: Inappropriate % 295.82/41.94 % (1968949)Time elapsed: 0.018 s % 295.82/41.94 % (1968949)Peak memory usage: 11 MB % 295.82/41.94 % (1968949)Instructions burned: 31 (million) % 295.82/41.94 % (1968949)------------------------------ % 295.82/41.94 % (1968949)------------------------------ % 295.82/41.94 % (1968951)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2748152821:i=262:bd=preordered:rtra=on:fsd=on_2748 on theBenchmark for (2748ds/262Mi) % 295.82/41.94 % (1968951)Instruction limit reached! % 295.82/41.94 % (1968951)------------------------------ % 295.82/41.94 % (1968951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.82/41.94 % (1968951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.82/41.94 % (1968951)CaDiCaL version: 2.1.3 % 295.82/41.94 % (1968951)Termination reason: Instruction limit % 295.82/41.94 % (1968951)Termination phase: Saturation % 295.82/41.94 % (1968951)Time elapsed: 0.164 s % 295.82/41.94 % (1968951)Peak memory usage: 16 MB % 295.82/41.94 % (1968951)Instructions burned: 263 (million) % 295.82/41.94 % (1968953)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=915603665:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2746 on theBenchmark for (2746ds/1368Mi) % 295.82/41.94 % (1968953)Instruction limit reached! % 295.82/41.94 % (1968953)------------------------------ % 295.82/41.94 % (1968953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.82/41.94 % (1968953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.82/41.94 % (1968953)CaDiCaL version: 2.1.3 % 295.82/41.94 % (1968953)Termination reason: Instruction limit % 295.82/41.94 % (1968953)Termination phase: Saturation % 295.82/41.94 % (1968953)Time elapsed: 0.760 s % 295.82/41.94 % (1968953)Peak memory usage: 21 MB % 295.82/41.94 % (1968953)Instructions burned: 1368 (million) % 295.82/41.94 % (1968955)ott-21_1_sil=16000:si=on:fs=off:random_seed=3651466532:i=360:av=off:fsr=off:rtra=on_2738 on theBenchmark for (2738ds/360Mi) % 295.82/41.94 % (1968955)Instruction limit reached! % 295.82/41.94 % (1968955)------------------------------ % 295.82/41.94 % (1968955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.82/41.94 % (1968955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.82/41.94 % (1968955)CaDiCaL version: 2.1.3 % 295.82/41.94 % (1968955)Termination reason: Instruction limit % 295.82/41.94 % (1968955)Termination phase: Saturation % 295.82/41.94 % (1968955)Time elapsed: 0.151 s % 295.82/41.94 % (1968955)Peak memory usage: 14 MB % 295.82/41.94 % (1968955)Instructions burned: 361 (million) % 295.82/41.94 % (1968961)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1926621859:i=954:bd=all:rtra=on_2736 on theBenchmark for (2736ds/954Mi) % 295.82/41.94 % (1968961)Instruction limit reached! % 295.82/41.94 % (1968961)------------------------------ % 295.82/41.94 % (1968961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.82/41.94 % (1968961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.82/41.94 % (1968961)CaDiCaL version: 2.1.3 % 295.82/41.94 % (1968961)Termination reason: Instruction limit % 295.82/41.94 % (1968961)Termination phase: Saturation % 295.82/41.94 % (1968961)Time elapsed: 0.514 s % 295.82/41.94 % (1968961)Peak memory usage: 18 MB % 295.82/41.94 % (1968961)Instructions burned: 956 (million) % 295.82/41.94 % (1968963)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1614641661:fmbsr=1.3:i=1730:ins=25:rtra=on_2731 on theBenchmark for (2731ds/1730Mi) % 295.82/41.94 % (1968963)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 295.82/41.94 % (1968963)Terminated due to inappropriate strategy. % 295.82/41.94 % (1968963)------------------------------ % 295.82/41.94 % (1968963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.82/41.94 % (1968963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.82/41.94 % (1968963)CaDiCaL version: 2.1.3 % 295.82/41.94 % (1968963)Termination reason: Terminated % 300.05/42.54 % Vampire exiting % 300.05/42.54 Terminated %------------------------------------------------------------------------------