%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC428_1 : TPTP v9.3.1. Bugfixed v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:06:00 PM UTC 2026 % Result : Timeout 300.10s 42.53s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC428_1 : TPTP v9.3.1. Bugfixed v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n020.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 09:37:49 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.21 Running first-order model finding % 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.23/0.80 % (55500)Will run a generic schedule for satisfiability detection. % 3.23/0.80 % (55509)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=941601147:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.23/0.80 % (55506)% WARNING: option uhcvi not known. % 3.23/0.80 % (55505)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3650138122_2999 on theBenchmark for (2999ds/0Mi) % 3.23/0.80 % (55506)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3678822962:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.23/0.80 % (55508)dis+10_1_sil=32000:sp=arity:random_seed=1075153911:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.23/0.80 % (55507)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=482549377:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.23/0.80 % (55510)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=436436674:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.23/0.80 % (55511)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4288146199:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.23/0.80 % (55505)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.23/0.80 % (55505)Terminated due to inappropriate strategy. % 3.23/0.80 % (55505)------------------------------ % 3.23/0.80 % (55505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.23/0.80 % (55505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.23/0.80 % (55505)CaDiCaL version: 2.1.3 % 3.23/0.80 % (55505)Termination reason: Inappropriate % 3.23/0.80 % (55505)Time elapsed: 0.001 s % 3.23/0.80 % (55505)Peak memory usage: 10 MB % 3.23/0.80 % (55505)Instructions burned: 1 (million) % 3.23/0.80 % (55505)------------------------------ % 3.23/0.80 % (55505)------------------------------ % 3.23/0.80 % (55519)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2281612086:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.23/0.80 % (55519)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.23/0.80 % (55519)Terminated due to inappropriate strategy. % 3.23/0.80 % (55519)------------------------------ % 3.23/0.80 % (55519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.23/0.80 % (55519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.23/0.80 % (55519)CaDiCaL version: 2.1.3 % 3.23/0.80 % (55519)Termination reason: Inappropriate % 3.23/0.80 % (55519)Time elapsed: 0.001 s % 3.23/0.80 % (55519)Peak memory usage: 10 MB % 3.23/0.80 % (55519)Instructions burned: 1 (million) % 3.23/0.80 % (55519)------------------------------ % 3.23/0.80 % (55519)------------------------------ % 3.23/0.80 % (55509)Instruction limit reached! % 3.23/0.80 % (55509)------------------------------ % 3.23/0.80 % (55509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.23/0.80 % (55509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.23/0.80 % (55509)CaDiCaL version: 2.1.3 % 3.23/0.80 % (55509)Termination reason: Instruction limit % 3.23/0.80 % (55509)Termination phase: Saturation % 3.23/0.80 % (55509)Time elapsed: 0.039 s % 3.23/0.80 % (55509)Peak memory usage: 12 MB % 3.23/0.80 % (55509)Instructions burned: 118 (million) % 3.23/0.80 % (55522)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=523074555:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.23/0.80 % (55521)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4243805818:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.23/0.80 % (55508)Instruction limit reached! % 3.23/0.80 % (55508)------------------------------ % 3.23/0.80 % (55508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.23/0.80 % (55508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.23/0.80 % (55508)CaDiCaL version: 2.1.3 % 3.23/0.80 % (55508)Termination reason: Instruction limit % 3.23/0.80 % (55508)Termination phase: Saturation % 3.23/0.80 % (55508)Time elapsed: 0.065 s % 3.23/0.80 % (55508)Peak memory usage: 12 MB % 3.23/0.80 % (55508)Instructions burned: 105 (million) % 3.23/0.80 % (55510)Instruction limit reached! % 3.23/0.80 % (55510)------------------------------ % 3.23/0.80 % (55510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.23/0.80 % (55510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/1.35 % (55510)CaDiCaL version: 2.1.3 % 7.42/1.35 % (55510)Termination reason: Instruction limit % 7.42/1.35 % (55510)Termination phase: Saturation % 7.42/1.35 % (55510)Time elapsed: 0.082 s % 7.42/1.35 % (55510)Peak memory usage: 13 MB % 7.42/1.35 % (55510)Instructions burned: 134 (million) % 7.42/1.35 % (55525)ott-21_1_sil=16000:fs=off:random_seed=1679429178:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 7.42/1.35 % (55526)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1784993811:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.42/1.35 % (55511)Instruction limit reached! % 7.42/1.35 % (55511)------------------------------ % 7.42/1.35 % (55511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.42/1.35 % (55511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/1.35 % (55511)CaDiCaL version: 2.1.3 % 7.42/1.35 % (55511)Termination reason: Instruction limit % 7.42/1.35 % (55511)Termination phase: Saturation % 7.42/1.35 % (55511)Time elapsed: 0.106 s % 7.42/1.35 % (55511)Peak memory usage: 13 MB % 7.42/1.35 % (55511)Instructions burned: 159 (million) % 7.42/1.35 % (55521)Instruction limit reached! % 7.42/1.35 % (55521)------------------------------ % 7.42/1.35 % (55521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.42/1.35 % (55521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/1.35 % (55521)CaDiCaL version: 2.1.3 % 7.42/1.35 % (55521)Termination reason: Instruction limit % 7.42/1.35 % (55521)Termination phase: Saturation % 7.42/1.35 % (55521)Time elapsed: 0.082 s % 7.42/1.35 % (55521)Peak memory usage: 12 MB % 7.42/1.35 % (55521)Instructions burned: 133 (million) % 7.42/1.35 % (55529)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2345389642:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.42/1.35 % (55529)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.42/1.35 % (55529)Terminated due to inappropriate strategy. % 7.42/1.35 % (55529)------------------------------ % 7.42/1.35 % (55529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.42/1.35 % (55529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/1.35 % (55529)CaDiCaL version: 2.1.3 % 7.42/1.35 % (55529)Termination reason: Inappropriate % 7.42/1.35 % (55529)Time elapsed: 0.001 s % 7.42/1.35 % (55529)Peak memory usage: 10 MB % 7.42/1.35 % (55529)Instructions burned: 1 (million) % 7.42/1.35 % (55529)------------------------------ % 7.42/1.35 % (55529)------------------------------ % 7.42/1.35 % (55530)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1539212223:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.42/1.35 % (55532)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3880758429:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 7.42/1.35 % (55532)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.42/1.35 % (55532)Terminated due to inappropriate strategy. % 7.42/1.35 % (55532)------------------------------ % 7.42/1.35 % (55532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.42/1.35 % (55532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/1.35 % (55532)CaDiCaL version: 2.1.3 % 7.42/1.35 % (55532)Termination reason: Inappropriate % 7.42/1.35 % (55532)Time elapsed: 0.001 s % 7.42/1.35 % (55532)Peak memory usage: 10 MB % 7.42/1.35 % (55532)Instructions burned: 1 (million) % 7.42/1.35 % (55532)------------------------------ % 7.42/1.35 % (55532)------------------------------ % 7.42/1.35 % (55525)Instruction limit reached! % 7.42/1.35 % (55525)------------------------------ % 7.42/1.35 % (55525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.42/1.35 % (55525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/1.35 % (55525)CaDiCaL version: 2.1.3 % 7.42/1.35 % (55525)Termination reason: Instruction limit % 7.42/1.35 % (55525)Termination phase: Saturation % 7.42/1.35 % (55525)Time elapsed: 0.080 s % 7.42/1.35 % (55525)Peak memory usage: 12 MB % 7.42/1.35 % (55525)Instructions burned: 180 (million) % 7.42/1.35 % (55535)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=2045744734: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) % 7.42/1.35 % (55536)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3779086172:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 21.85/3.31 % (55522)Instruction limit reached! % 21.85/3.31 % (55522)------------------------------ % 21.85/3.31 % (55522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.31 % (55522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.85/3.31 % (55522)CaDiCaL version: 2.1.3 % 21.85/3.31 % (55522)Termination reason: Instruction limit % 21.85/3.31 % (55522)Termination phase: Saturation % 21.85/3.31 % (55522)Time elapsed: 0.202 s % 21.85/3.31 % (55522)Peak memory usage: 16 MB % 21.85/3.31 % (55522)Instructions burned: 687 (million) % 21.85/3.31 % (55539)fmb+10_1_sil=64000:random_seed=3631061070:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 21.85/3.31 % (55539)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.85/3.31 % (55539)Terminated due to inappropriate strategy. % 21.85/3.31 % (55539)------------------------------ % 21.85/3.31 % (55539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.31 % (55539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.85/3.31 % (55539)CaDiCaL version: 2.1.3 % 21.85/3.31 % (55539)Termination reason: Inappropriate % 21.85/3.31 % (55539)Time elapsed: 0.001 s % 21.85/3.31 % (55539)Peak memory usage: 11 MB % 21.85/3.31 % (55539)Instructions burned: 1 (million) % 21.85/3.31 % (55539)------------------------------ % 21.85/3.31 % (55539)------------------------------ % 21.85/3.31 % (55541)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1114060916:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 21.85/3.31 % (55541)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.85/3.31 % (55541)Terminated due to inappropriate strategy. % 21.85/3.31 % (55541)------------------------------ % 21.85/3.31 % (55541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.31 % (55541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.85/3.31 % (55541)CaDiCaL version: 2.1.3 % 21.85/3.31 % (55541)Termination reason: Inappropriate % 21.85/3.31 % (55541)Time elapsed: 0.0000 s % 21.85/3.31 % (55541)Peak memory usage: 10 MB % 21.85/3.31 % (55541)Instructions burned: 1 (million) % 21.85/3.31 % (55541)------------------------------ % 21.85/3.31 % (55541)------------------------------ % 21.85/3.31 % (55543)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1573551150:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 21.85/3.31 % (55543)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.85/3.31 % (55543)Terminated due to inappropriate strategy. % 21.85/3.31 % (55543)------------------------------ % 21.85/3.31 % (55543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.31 % (55543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.85/3.31 % (55543)CaDiCaL version: 2.1.3 % 21.85/3.31 % (55543)Termination reason: Inappropriate % 21.85/3.31 % (55543)Time elapsed: 0.0000 s % 21.85/3.31 % (55543)Peak memory usage: 11 MB % 21.85/3.31 % (55543)Instructions burned: 1 (million) % 21.85/3.31 % (55543)------------------------------ % 21.85/3.31 % (55543)------------------------------ % 21.85/3.31 % (55545)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2395558926:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 21.85/3.31 % (55526)Instruction limit reached! % 21.85/3.31 % (55526)------------------------------ % 21.85/3.31 % (55526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.31 % (55526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.85/3.31 % (55526)CaDiCaL version: 2.1.3 % 21.85/3.31 % (55526)Termination reason: Instruction limit % 21.85/3.31 % (55526)Termination phase: Saturation % 21.85/3.31 % (55526)Time elapsed: 0.305 s % 21.85/3.31 % (55526)Peak memory usage: 14 MB % 21.85/3.31 % (55526)Instructions burned: 478 (million) % 21.85/3.31 % (55547)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2786911656:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 21.85/3.31 % (55535)Instruction limit reached! % 21.85/3.31 % (55535)------------------------------ % 21.85/3.31 % (55535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.31 % (55535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.85/3.31 % (55535)CaDiCaL version: 2.1.3 % 21.85/3.31 % (55535)Termination reason: Instruction limit % 21.85/3.31 % (55535)Termination phase: Saturation % 21.85/3.31 % (55535)Time elapsed: 0.377 s % 21.85/3.31 % (55535)Peak memory usage: 18 MB % 36.77/5.44 % (55535)Instructions burned: 692 (million) % 36.77/5.44 % (55549)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=682047819:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 36.77/5.44 % (55549)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.77/5.44 % (55549)Terminated due to inappropriate strategy. % 36.77/5.44 % (55549)------------------------------ % 36.77/5.44 % (55549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.77/5.44 % (55549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.77/5.44 % (55549)CaDiCaL version: 2.1.3 % 36.77/5.44 % (55549)Termination reason: Inappropriate % 36.77/5.44 % (55549)Time elapsed: 0.001 s % 36.77/5.44 % (55549)Peak memory usage: 10 MB % 36.77/5.44 % (55549)Instructions burned: 1 (million) % 36.77/5.44 % (55549)------------------------------ % 36.77/5.44 % (55549)------------------------------ % 36.77/5.44 % (55551)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=883541889:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 36.77/5.44 % (55551)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.77/5.44 % (55551)Terminated due to inappropriate strategy. % 36.77/5.44 % (55551)------------------------------ % 36.77/5.44 % (55551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.77/5.44 % (55551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.77/5.44 % (55551)CaDiCaL version: 2.1.3 % 36.77/5.44 % (55551)Termination reason: Inappropriate % 36.77/5.44 % (55551)Time elapsed: 0.001 s % 36.77/5.44 % (55551)Peak memory usage: 10 MB % 36.77/5.44 % (55551)Instructions burned: 1 (million) % 36.77/5.44 % (55551)------------------------------ % 36.77/5.44 % (55551)------------------------------ % 36.77/5.44 % (55553)ott-2_1_sil=16000:newcnf=on:random_seed=894901011:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 36.77/5.44 % (55536)Instruction limit reached! % 36.77/5.44 % (55536)------------------------------ % 36.77/5.44 % (55536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.77/5.44 % (55536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.77/5.44 % (55536)CaDiCaL version: 2.1.3 % 36.77/5.44 % (55536)Termination reason: Instruction limit % 36.77/5.44 % (55536)Termination phase: Saturation % 36.77/5.44 % (55536)Time elapsed: 0.490 s % 36.77/5.44 % (55536)Peak memory usage: 19 MB % 36.77/5.44 % (55536)Instructions burned: 881 (million) % 36.77/5.44 % (55555)ott+10_1_sil=32000:tgt=ground:random_seed=1097869880:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 36.77/5.44 % (55530)Instruction limit reached! % 36.77/5.44 % (55530)------------------------------ % 36.77/5.44 % (55530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.77/5.44 % (55530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.77/5.44 % (55530)CaDiCaL version: 2.1.3 % 36.77/5.44 % (55530)Termination reason: Instruction limit % 36.77/5.44 % (55530)Termination phase: Saturation % 36.77/5.44 % (55530)Time elapsed: 0.619 s % 36.77/5.44 % (55530)Peak memory usage: 18 MB % 36.77/5.44 % (55530)Instructions burned: 1181 (million) % 36.77/5.44 % (55557)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4086240275:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 36.77/5.44 % (55557)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.77/5.44 % (55557)Terminated due to inappropriate strategy. % 36.77/5.44 % (55557)------------------------------ % 36.77/5.44 % (55557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.77/5.44 % (55557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.77/5.44 % (55557)CaDiCaL version: 2.1.3 % 36.77/5.44 % (55557)Termination reason: Inappropriate % 36.77/5.44 % (55557)Time elapsed: 0.001 s % 36.77/5.44 % (55557)Peak memory usage: 11 MB % 36.77/5.44 % (55557)Instructions burned: 1 (million) % 36.77/5.44 % (55557)------------------------------ % 36.77/5.44 % (55557)------------------------------ % 36.77/5.44 % (55559)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=663471971:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 36.77/5.44 % (55553)Instruction limit reached! % 36.77/5.44 % (55553)------------------------------ % 36.77/5.44 % (55553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.77/5.44 % (55553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.77/5.44 % (55553)CaDiCaL version: 2.1.3 % 102.06/14.65 % (55553)Termination reason: Instruction limit % 102.06/14.65 % (55553)Termination phase: Saturation % 102.06/14.65 % (55553)Time elapsed: 0.491 s % 102.06/14.65 % (55553)Peak memory usage: 18 MB % 102.06/14.65 % (55553)Instructions burned: 869 (million) % 102.06/14.65 % (55561)dis+21_1_sil=32000:sas=cadical:random_seed=2274839571:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 102.06/14.65 % (55547)Instruction limit reached! % 102.06/14.65 % (55547)------------------------------ % 102.06/14.65 % (55547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.06/14.65 % (55547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.06/14.65 % (55547)CaDiCaL version: 2.1.3 % 102.06/14.65 % (55547)Termination reason: Instruction limit % 102.06/14.65 % (55547)Termination phase: Saturation % 102.06/14.65 % (55547)Time elapsed: 0.868 s % 102.06/14.65 % (55547)Peak memory usage: 28 MB % 102.06/14.65 % (55547)Instructions burned: 1473 (million) % 102.06/14.65 % (55563)ott+11_1_sil=16000:gs=on:random_seed=1185638886:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 102.06/14.65 % (55545)Instruction limit reached! % 102.06/14.65 % (55545)------------------------------ % 102.06/14.65 % (55545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.06/14.65 % (55545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.06/14.65 % (55545)CaDiCaL version: 2.1.3 % 102.06/14.65 % (55545)Termination reason: Instruction limit % 102.06/14.65 % (55545)Termination phase: Saturation % 102.06/14.65 % (55545)Time elapsed: 1.473 s % 102.06/14.65 % (55545)Peak memory usage: 43 MB % 102.06/14.65 % (55545)Instructions burned: 5134 (million) % 102.06/14.65 % (55565)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=333703523:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 102.06/14.65 % (55565)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 102.06/14.65 % (55565)Terminated due to inappropriate strategy. % 102.06/14.65 % (55565)------------------------------ % 102.06/14.65 % (55565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.06/14.65 % (55565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.06/14.65 % (55565)CaDiCaL version: 2.1.3 % 102.06/14.65 % (55565)Termination reason: Inappropriate % 102.06/14.65 % (55565)Time elapsed: 0.001 s % 102.06/14.65 % (55565)Peak memory usage: 10 MB % 102.06/14.65 % (55565)Instructions burned: 1 (million) % 102.06/14.65 % (55565)------------------------------ % 102.06/14.65 % (55565)------------------------------ % 102.06/14.65 % (55567)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3619063287:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 102.06/14.65 % (55563)Instruction limit reached! % 102.06/14.65 % (55563)------------------------------ % 102.06/14.65 % (55563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.06/14.65 % (55563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.06/14.65 % (55563)CaDiCaL version: 2.1.3 % 102.06/14.65 % (55563)Termination reason: Instruction limit % 102.06/14.65 % (55563)Termination phase: Saturation % 102.06/14.65 % (55563)Time elapsed: 1.213 s % 102.06/14.65 % (55563)Peak memory usage: 22 MB % 102.06/14.65 % (55563)Instructions burned: 2251 (million) % 102.06/14.65 % (55569)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4233927944:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 102.06/14.65 % (55559)Instruction limit reached! % 102.06/14.65 % (55559)------------------------------ % 102.06/14.65 % (55559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.06/14.65 % (55559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.06/14.65 % (55559)CaDiCaL version: 2.1.3 % 102.06/14.65 % (55559)Termination reason: Instruction limit % 102.06/14.65 % (55559)Termination phase: Saturation % 102.06/14.65 % (55559)Time elapsed: 1.873 s % 102.06/14.65 % (55559)Peak memory usage: 37 MB % 102.06/14.65 % (55559)Instructions burned: 3513 (million) % 102.06/14.65 % (55571)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1039966820:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 102.06/14.65 % (55567)Instruction limit reached! % 102.06/14.65 % (55567)------------------------------ % 102.06/14.65 % (55567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.06/14.65 % (55567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.06/14.65 % (55567)CaDiCaL version: 2.1.3 % 102.06/14.65 % (55567)Termination reason: Instruction limit % 102.06/14.65 % (55567)Termination phase: Saturation % 114.85/16.41 % (55567)Time elapsed: 1.227 s % 114.85/16.41 % (55567)Peak memory usage: 44 MB % 114.85/16.41 % (55567)Instructions burned: 4592 (million) % 114.85/16.41 % (55573)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=66292462:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 114.85/16.41 % (55573)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 114.85/16.41 % (55573)Terminated due to inappropriate strategy. % 114.85/16.41 % (55573)------------------------------ % 114.85/16.41 % (55573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.85/16.41 % (55573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.85/16.41 % (55573)CaDiCaL version: 2.1.3 % 114.85/16.41 % (55573)Termination reason: Inappropriate % 114.85/16.41 % (55573)Time elapsed: 0.0000 s % 114.85/16.41 % (55573)Peak memory usage: 10 MB % 114.85/16.41 % (55573)Instructions burned: 1 (million) % 114.85/16.41 % (55573)------------------------------ % 114.85/16.41 % (55573)------------------------------ % 114.85/16.41 % (55575)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4189785563:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 114.85/16.41 % (55575)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 114.85/16.41 % (55575)Terminated due to inappropriate strategy. % 114.85/16.41 % (55575)------------------------------ % 114.85/16.41 % (55575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.85/16.41 % (55575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.85/16.41 % (55575)CaDiCaL version: 2.1.3 % 114.85/16.41 % (55575)Termination reason: Inappropriate % 114.85/16.41 % (55575)Time elapsed: 0.0000 s % 114.85/16.41 % (55575)Peak memory usage: 10 MB % 114.85/16.41 % (55575)Instructions burned: 1 (million) % 114.85/16.41 % (55575)------------------------------ % 114.85/16.41 % (55575)------------------------------ % 114.85/16.41 % (55577)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=341927440:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 114.85/16.41 % (55577)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 114.85/16.41 % (55577)Terminated due to inappropriate strategy. % 114.85/16.41 % (55577)------------------------------ % 114.85/16.41 % (55577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.85/16.41 % (55577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.85/16.41 % (55577)CaDiCaL version: 2.1.3 % 114.85/16.41 % (55577)Termination reason: Inappropriate % 114.85/16.41 % (55577)Time elapsed: 0.0000 s % 114.85/16.41 % (55577)Peak memory usage: 10 MB % 114.85/16.41 % (55577)Instructions burned: 1 (million) % 114.85/16.41 % (55577)------------------------------ % 114.85/16.41 % (55577)------------------------------ % 114.85/16.41 % (55579)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=891107244:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 114.85/16.41 % (55561)Instruction limit reached! % 114.85/16.41 % (55561)------------------------------ % 114.85/16.41 % (55561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.85/16.41 % (55561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.85/16.41 % (55561)CaDiCaL version: 2.1.3 % 114.85/16.41 % (55561)Termination reason: Instruction limit % 114.85/16.41 % (55561)Termination phase: Saturation % 114.85/16.41 % (55561)Time elapsed: 2.049 s % 114.85/16.41 % (55561)Peak memory usage: 32 MB % 114.85/16.41 % (55561)Instructions burned: 3773 (million) % 114.85/16.41 % (55581)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2829417776:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 114.85/16.41 % (55555)Instruction limit reached! % 114.85/16.41 % (55555)------------------------------ % 114.85/16.41 % (55555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.85/16.41 % (55555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.85/16.41 % (55555)CaDiCaL version: 2.1.3 % 114.85/16.41 % (55555)Termination reason: Instruction limit % 114.85/16.41 % (55555)Termination phase: Saturation % 114.85/16.41 % (55555)Time elapsed: 3.208 s % 114.85/16.41 % (55555)Peak memory usage: 34 MB % 114.85/16.41 % (55555)Instructions burned: 5114 (million) % 114.85/16.41 % (55583)dis+10_16:1_sil=16000:random_seed=1150967714:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi) % 114.85/16.41 % (55571)Instruction limit reached! % 114.85/16.41 % (55571)------------------------------ % 114.85/16.41 % (55571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.85/16.41 % (55571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.88/18.82 % (55571)CaDiCaL version: 2.1.3 % 131.88/18.82 % (55571)Termination reason: Instruction limit % 131.88/18.82 % (55571)Termination phase: Saturation % 131.88/18.82 % (55571)Time elapsed: 2.492 s % 131.88/18.82 % (55571)Peak memory usage: 42 MB % 131.88/18.82 % (55571)Instructions burned: 5212 (million) % 131.88/18.82 % (55585)ott-3_8_sil=64000:random_seed=3861277142:i=20139:bs=on_2947 on theBenchmark for (2947ds/20139Mi) % 131.88/18.82 % (55581)Instruction limit reached! % 131.88/18.82 % (55581)------------------------------ % 131.88/18.82 % (55581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.88/18.82 % (55581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.88/18.82 % (55581)CaDiCaL version: 2.1.3 % 131.88/18.82 % (55581)Termination reason: Instruction limit % 131.88/18.82 % (55581)Termination phase: Saturation % 131.88/18.82 % (55581)Time elapsed: 5.049 s % 131.88/18.82 % (55581)Peak memory usage: 55 MB % 131.88/18.82 % (55581)Instructions burned: 8174 (million) % 131.88/18.82 % (55587)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=218452992:fmbsr=2:i=32576_2917 on theBenchmark for (2917ds/32576Mi) % 131.88/18.82 % (55587)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 131.88/18.82 % (55587)Terminated due to inappropriate strategy. % 131.88/18.82 % (55587)------------------------------ % 131.88/18.82 % (55587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.88/18.82 % (55587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.88/18.82 % (55587)CaDiCaL version: 2.1.3 % 131.88/18.82 % (55587)Termination reason: Inappropriate % 131.88/18.82 % (55587)Time elapsed: 0.001 s % 131.88/18.82 % (55587)Peak memory usage: 10 MB % 131.88/18.82 % (55587)Instructions burned: 1 (million) % 131.88/18.82 % (55587)------------------------------ % 131.88/18.82 % (55587)------------------------------ % 131.88/18.82 % (55589)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3705966811:i=11404_2917 on theBenchmark for (2917ds/11404Mi) % 131.88/18.82 % (55579)Instruction limit reached! % 131.88/18.82 % (55579)------------------------------ % 131.88/18.82 % (55579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.88/18.82 % (55579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.88/18.82 % (55579)CaDiCaL version: 2.1.3 % 131.88/18.82 % (55579)Termination reason: Instruction limit % 131.88/18.82 % (55579)Termination phase: Saturation % 131.88/18.82 % (55579)Time elapsed: 5.235 s % 131.88/18.82 % (55579)Peak memory usage: 74 MB % 131.88/18.82 % (55579)Instructions burned: 22566 (million) % 131.88/18.82 % (55591)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2687028319:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 131.88/18.82 % (55583)Instruction limit reached! % 131.88/18.82 % (55583)------------------------------ % 131.88/18.82 % (55583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.88/18.82 % (55583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.88/18.82 % (55583)CaDiCaL version: 2.1.3 % 131.88/18.82 % (55583)Termination reason: Instruction limit % 131.88/18.82 % (55583)Termination phase: Saturation % 131.88/18.82 % (55583)Time elapsed: 4.636 s % 131.88/18.82 % (55583)Peak memory usage: 52 MB % 131.88/18.82 % (55583)Instructions burned: 9156 (million) % 131.88/18.82 % (55593)dis+33_16_sil=32000:sac=on:random_seed=3233785020:i=15851:nm=0_2914 on theBenchmark for (2914ds/15851Mi) % 131.88/18.82 % (55591)Instruction limit reached! % 131.88/18.82 % (55591)------------------------------ % 131.88/18.82 % (55591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.88/18.82 % (55591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.88/18.82 % (55591)CaDiCaL version: 2.1.3 % 131.88/18.82 % (55591)Termination reason: Instruction limit % 131.88/18.82 % (55591)Termination phase: Saturation % 131.88/18.82 % (55591)Time elapsed: 4.738 s % 131.88/18.82 % (55591)Peak memory usage: 73 MB % 131.88/18.82 % (55591)Instructions burned: 14136 (million) % 131.88/18.82 % (55595)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=116367592:avsq=on:i=17627:add=on:amm=off_2868 on theBenchmark for (2868ds/17627Mi) % 131.88/18.82 % (55569)Instruction limit reached! % 131.88/18.82 % (55569)------------------------------ % 131.88/18.82 % (55569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.88/18.82 % (55569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.88/18.82 % (55569)CaDiCaL version: 2.1.3 % 131.88/18.82 % (55569)Termination reason: Instruction limit % 131.88/18.82 % (55569)Termination phase: Saturation % 135.38/19.35 % (55569)Time elapsed: 11.852 s % 135.38/19.35 % (55569)Peak memory usage: 117 MB % 135.38/19.35 % (55569)Instructions burned: 29342 (million) % 135.38/19.35 % (55597)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3191756952:s2a=on:i=53295_2855 on theBenchmark for (2855ds/53295Mi) % 135.38/19.35 % (55589)Instruction limit reached! % 135.38/19.35 % (55589)------------------------------ % 135.38/19.35 % (55589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.38/19.35 % (55589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.38/19.35 % (55589)CaDiCaL version: 2.1.3 % 135.38/19.35 % (55589)Termination reason: Instruction limit % 135.38/19.35 % (55589)Termination phase: Saturation % 135.38/19.35 % (55589)Time elapsed: 7.106 s % 135.38/19.35 % (55589)Peak memory usage: 62 MB % 135.38/19.35 % (55589)Instructions burned: 11404 (million) % 135.38/19.35 % (55599)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1197508970:i=26857:ins=20_2845 on theBenchmark for (2845ds/26857Mi) % 135.38/19.35 % (55599)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.38/19.35 % (55599)Terminated due to inappropriate strategy. % 135.38/19.35 % (55599)------------------------------ % 135.38/19.35 % (55599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.38/19.35 % (55599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.38/19.35 % (55599)CaDiCaL version: 2.1.3 % 135.38/19.35 % (55599)Termination reason: Inappropriate % 135.38/19.35 % (55599)Time elapsed: 0.001 s % 135.38/19.35 % (55599)Peak memory usage: 10 MB % 135.38/19.35 % (55599)Instructions burned: 1 (million) % 135.38/19.35 % (55599)------------------------------ % 135.38/19.35 % (55599)------------------------------ % 135.38/19.35 % (55601)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=693043432:i=28120:bs=on:fsr=off_2845 on theBenchmark for (2845ds/28120Mi) % 135.38/19.35 % (55593)Instruction limit reached! % 135.38/19.35 % (55593)------------------------------ % 135.38/19.35 % (55593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.38/19.35 % (55593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.38/19.35 % (55593)CaDiCaL version: 2.1.3 % 135.38/19.35 % (55593)Termination reason: Instruction limit % 135.38/19.35 % (55593)Termination phase: Saturation % 135.38/19.35 % (55593)Time elapsed: 7.486 s % 135.38/19.35 % (55593)Peak memory usage: 170 MB % 135.38/19.35 % (55593)Instructions burned: 15852 (million) % 135.38/19.35 % (55603)fmb+10_1_sil=256000:fmbss=7:random_seed=3456040685:fmbsr=1.6:i=182295_2838 on theBenchmark for (2838ds/182295Mi) % 135.38/19.35 % (55603)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.38/19.35 % (55603)Terminated due to inappropriate strategy. % 135.38/19.35 % (55603)------------------------------ % 135.38/19.35 % (55603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.38/19.35 % (55603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.38/19.35 % (55603)CaDiCaL version: 2.1.3 % 135.38/19.35 % (55603)Termination reason: Inappropriate % 135.38/19.35 % (55603)Time elapsed: 0.001 s % 135.38/19.35 % (55603)Peak memory usage: 10 MB % 135.38/19.35 % (55603)Instructions burned: 1 (million) % 135.38/19.35 % (55603)------------------------------ % 135.38/19.35 % (55603)------------------------------ % 135.38/19.35 % (55605)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2319177526:i=44625:gsp=on_2838 on theBenchmark for (2838ds/44625Mi) % 135.38/19.35 % (55605)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.38/19.35 % (55605)Terminated due to inappropriate strategy. % 135.38/19.35 % (55605)------------------------------ % 135.38/19.35 % (55605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.38/19.35 % (55605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.38/19.35 % (55605)CaDiCaL version: 2.1.3 % 135.38/19.35 % (55605)Termination reason: Inappropriate % 135.38/19.35 % (55605)Time elapsed: 0.001 s % 135.38/19.35 % (55605)Peak memory usage: 10 MB % 135.38/19.35 % (55605)Instructions burned: 1 (million) % 135.38/19.35 % (55605)------------------------------ % 135.38/19.35 % (55605)------------------------------ % 135.38/19.35 % (55607)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1211308266:i=160505_2838 on theBenchmark for (2838ds/160505Mi) % 135.38/19.35 % (55607)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.38/19.35 % (55607)Terminated due to inappropriate strategy. % 135.38/19.35 % (55607)------------------------------ % 135.38/19.35 % (55607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.53/20.82 % (55607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.53/20.82 % (55607)CaDiCaL version: 2.1.3 % 145.53/20.82 % (55607)Termination reason: Inappropriate % 145.53/20.82 % (55607)Time elapsed: 0.001 s % 145.53/20.82 % (55607)Peak memory usage: 10 MB % 145.53/20.82 % (55607)Instructions burned: 1 (million) % 145.53/20.82 % (55607)------------------------------ % 145.53/20.82 % (55607)------------------------------ % 145.53/20.82 % (55609)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1230901596:fmbsr=1.3:i=225729_2838 on theBenchmark for (2838ds/225729Mi) % 145.53/20.82 % (55609)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 145.53/20.82 % (55609)Terminated due to inappropriate strategy. % 145.53/20.82 % (55609)------------------------------ % 145.53/20.82 % (55609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.53/20.82 % (55609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.53/20.82 % (55609)CaDiCaL version: 2.1.3 % 145.53/20.82 % (55609)Termination reason: Inappropriate % 145.53/20.82 % (55609)Time elapsed: 0.001 s % 145.53/20.82 % (55609)Peak memory usage: 10 MB % 145.53/20.82 % (55609)Instructions burned: 1 (million) % 145.53/20.82 % (55609)------------------------------ % 145.53/20.82 % (55609)------------------------------ % 145.53/20.82 % (55611)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2804546846:fmbsr=2:i=185024:ins=7_2837 on theBenchmark for (2837ds/185024Mi) % 145.53/20.82 % (55611)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 145.53/20.82 % (55611)Terminated due to inappropriate strategy. % 145.53/20.82 % (55611)------------------------------ % 145.53/20.82 % (55611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.53/20.82 % (55611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.53/20.82 % (55611)CaDiCaL version: 2.1.3 % 145.53/20.82 % (55611)Termination reason: Inappropriate % 145.53/20.82 % (55611)Time elapsed: 0.001 s % 145.53/20.82 % (55611)Peak memory usage: 10 MB % 145.53/20.82 % (55611)Instructions burned: 1 (million) % 145.53/20.82 % (55611)------------------------------ % 145.53/20.82 % (55611)------------------------------ % 145.53/20.82 % (55613)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4282941361:rtra=on_2837 on theBenchmark for (2837ds/0Mi) % 145.53/20.82 % (55613)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 145.53/20.82 % (55613)Terminated due to inappropriate strategy. % 145.53/20.82 % (55613)------------------------------ % 145.53/20.82 % (55613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.53/20.82 % (55613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.53/20.82 % (55613)CaDiCaL version: 2.1.3 % 145.53/20.82 % (55613)Termination reason: Inappropriate % 145.53/20.82 % (55613)Time elapsed: 0.001 s % 145.53/20.82 % (55613)Peak memory usage: 10 MB % 145.53/20.82 % (55613)Instructions burned: 1 (million) % 145.53/20.82 % (55613)------------------------------ % 145.53/20.82 % (55613)------------------------------ % 145.53/20.82 % (55585)Instruction limit reached! % 145.53/20.82 % (55585)------------------------------ % 145.53/20.82 % (55585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.53/20.82 % (55585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.53/20.82 % (55585)CaDiCaL version: 2.1.3 % 145.53/20.82 % (55585)Termination reason: Instruction limit % 145.53/20.82 % (55585)Termination phase: Saturation % 145.53/20.82 % (55585)Time elapsed: 11.019 s % 145.53/20.82 % (55585)Peak memory usage: 66 MB % 145.53/20.82 % (55585)Instructions burned: 20139 (million) % 145.53/20.82 % (55615)% WARNING: option uhcvi not known. % 145.53/20.82 % (55615)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2657508238:i=271062:add=off:rtra=on:rawr=on_2837 on theBenchmark for (2837ds/271062Mi) % 145.53/20.82 % (55616)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2586642394:i=176048:add=on:rtra=on:rawr=on_2837 on theBenchmark for (2837ds/176048Mi) % 145.53/20.82 % (55595)Instruction limit reached! % 145.53/20.82 % (55595)------------------------------ % 145.53/20.82 % (55595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.53/20.82 % (55595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.53/20.82 % (55595)CaDiCaL version: 2.1.3 % 145.53/20.82 % (55595)Termination reason: Instruction limit % 145.53/20.82 % (55595)Termination phase: Saturation % 145.53/20.82 % (55595)Time elapsed: 5.462 s % 153.19/21.84 % (55595)Peak memory usage: 147 MB % 153.19/21.84 % (55595)Instructions burned: 17628 (million) % 153.19/21.84 % (55619)dis+10_1_sil=32000:si=on:sp=arity:random_seed=940156732:i=206:fgj=on:rtra=on_2813 on theBenchmark for (2813ds/206Mi) % 153.19/21.84 % (55619)Instruction limit reached! % 153.19/21.84 % (55619)------------------------------ % 153.19/21.84 % (55619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.19/21.84 % (55619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.19/21.84 % (55619)CaDiCaL version: 2.1.3 % 153.19/21.84 % (55619)Termination reason: Instruction limit % 153.19/21.84 % (55619)Termination phase: Saturation % 153.19/21.84 % (55619)Time elapsed: 0.066 s % 153.19/21.84 % (55619)Peak memory usage: 13 MB % 153.19/21.84 % (55619)Instructions burned: 207 (million) % 153.19/21.84 % (55621)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1278028066:i=232:rtra=on_2813 on theBenchmark for (2813ds/232Mi) % 153.19/21.84 % (55621)Instruction limit reached! % 153.19/21.84 % (55621)------------------------------ % 153.19/21.84 % (55621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.19/21.84 % (55621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.19/21.84 % (55621)CaDiCaL version: 2.1.3 % 153.19/21.84 % (55621)Termination reason: Instruction limit % 153.19/21.84 % (55621)Termination phase: Saturation % 153.19/21.84 % (55621)Time elapsed: 0.078 s % 153.19/21.84 % (55621)Peak memory usage: 13 MB % 153.19/21.84 % (55621)Instructions burned: 234 (million) % 153.19/21.84 % (55623)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1067989143:i=262:rtra=on_2812 on theBenchmark for (2812ds/262Mi) % 153.19/21.84 % (55623)Instruction limit reached! % 153.19/21.84 % (55623)------------------------------ % 153.19/21.84 % (55623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.19/21.84 % (55623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.19/21.84 % (55623)CaDiCaL version: 2.1.3 % 153.19/21.84 % (55623)Termination reason: Instruction limit % 153.19/21.84 % (55623)Termination phase: Saturation % 153.19/21.84 % (55623)Time elapsed: 0.085 s % 153.19/21.84 % (55623)Peak memory usage: 14 MB % 153.19/21.84 % (55623)Instructions burned: 263 (million) % 153.19/21.84 % (55625)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1087419407:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2811 on theBenchmark for (2811ds/318Mi) % 153.19/21.84 % (55625)Instruction limit reached! % 153.19/21.84 % (55625)------------------------------ % 153.19/21.84 % (55625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.19/21.84 % (55625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.19/21.84 % (55625)CaDiCaL version: 2.1.3 % 153.19/21.84 % (55625)Termination reason: Instruction limit % 153.19/21.84 % (55625)Termination phase: Saturation % 153.19/21.84 % (55625)Time elapsed: 0.123 s % 153.19/21.84 % (55625)Peak memory usage: 15 MB % 153.19/21.84 % (55625)Instructions burned: 320 (million) % 153.19/21.84 % (55627)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1581981360:i=1428:nm=2:rtra=on_2809 on theBenchmark for (2809ds/1428Mi) % 153.19/21.84 % (55627)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 153.19/21.84 % (55627)Terminated due to inappropriate strategy. % 153.19/21.84 % (55627)------------------------------ % 153.19/21.84 % (55627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.19/21.84 % (55627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.19/21.84 % (55627)CaDiCaL version: 2.1.3 % 153.19/21.84 % (55627)Termination reason: Inappropriate % 153.19/21.84 % (55627)Time elapsed: 0.0000 s % 153.19/21.84 % (55627)Peak memory usage: 10 MB % 153.19/21.84 % (55627)Instructions burned: 1 (million) % 153.19/21.84 % (55627)------------------------------ % 153.19/21.84 % (55627)------------------------------ % 153.19/21.84 % (55629)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2683585044:i=262:bd=preordered:rtra=on:fsd=on_2809 on theBenchmark for (2809ds/262Mi) % 153.19/21.84 % (55629)Instruction limit reached! % 153.19/21.84 % (55629)------------------------------ % 153.19/21.84 % (55629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.19/21.84 % (55629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.19/21.84 % (55629)CaDiCaL version: 2.1.3 % 153.19/21.84 % (55629)Termination reason: Instruction limit % 153.19/21.84 % (55629)Termination phase: Saturation % 153.19/21.84 % (55629)Time elapsed: 0.085 s % 153.19/21.84 % (55629)Peak memory usage: 13 MB % 153.19/21.84 % (55629)Instructions burned: 262 (million) % 199.29/28.34 % (55631)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=1722387447:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2808 on theBenchmark for (2808ds/1368Mi) % 199.29/28.34 % (55631)Instruction limit reached! % 199.29/28.34 % (55631)------------------------------ % 199.29/28.34 % (55631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.29/28.34 % (55631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.29/28.34 % (55631)CaDiCaL version: 2.1.3 % 199.29/28.34 % (55631)Termination reason: Instruction limit % 199.29/28.34 % (55631)Termination phase: Saturation % 199.29/28.34 % (55631)Time elapsed: 0.410 s % 199.29/28.34 % (55631)Peak memory usage: 21 MB % 199.29/28.34 % (55631)Instructions burned: 1368 (million) % 199.29/28.34 % (55633)ott-21_1_sil=16000:si=on:fs=off:random_seed=75967239:i=360:av=off:fsr=off:rtra=on_2804 on theBenchmark for (2804ds/360Mi) % 199.29/28.34 % (55633)Instruction limit reached! % 199.29/28.34 % (55633)------------------------------ % 199.29/28.34 % (55633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.29/28.34 % (55633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.29/28.34 % (55633)CaDiCaL version: 2.1.3 % 199.29/28.34 % (55633)Termination reason: Instruction limit % 199.29/28.34 % (55633)Termination phase: Saturation % 199.29/28.34 % (55633)Time elapsed: 0.085 s % 199.29/28.34 % (55633)Peak memory usage: 13 MB % 199.29/28.34 % (55633)Instructions burned: 363 (million) % 199.29/28.34 % (55635)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=942181948:i=954:bd=all:rtra=on_2803 on theBenchmark for (2803ds/954Mi) % 199.29/28.34 % (55635)Instruction limit reached! % 199.29/28.34 % (55635)------------------------------ % 199.29/28.34 % (55635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.29/28.34 % (55635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.29/28.34 % (55635)CaDiCaL version: 2.1.3 % 199.29/28.34 % (55635)Termination reason: Instruction limit % 199.29/28.34 % (55635)Termination phase: Saturation % 199.29/28.34 % (55635)Time elapsed: 0.332 s % 199.29/28.34 % (55635)Peak memory usage: 16 MB % 199.29/28.34 % (55635)Instructions burned: 954 (million) % 199.29/28.34 % (55637)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3699195318:fmbsr=1.3:i=1730:ins=25:rtra=on_2800 on theBenchmark for (2800ds/1730Mi) % 199.29/28.34 % (55637)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 199.29/28.34 % (55637)Terminated due to inappropriate strategy. % 199.29/28.34 % (55637)------------------------------ % 199.29/28.34 % (55637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.29/28.34 % (55637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.29/28.34 % (55637)CaDiCaL version: 2.1.3 % 199.29/28.34 % (55637)Termination reason: Inappropriate % 199.29/28.34 % (55637)Time elapsed: 0.0000 s % 199.29/28.34 % (55637)Peak memory usage: 10 MB % 199.29/28.34 % (55637)Instructions burned: 1 (million) % 199.29/28.34 % (55637)------------------------------ % 199.29/28.34 % (55637)------------------------------ % 199.29/28.34 % (55639)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2146767400:i=2358:rtra=on_2799 on theBenchmark for (2799ds/2358Mi) % 199.29/28.34 % (55639)Instruction limit reached! % 199.29/28.34 % (55639)------------------------------ % 199.29/28.34 % (55639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.29/28.34 % (55639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.29/28.34 % (55639)CaDiCaL version: 2.1.3 % 199.29/28.34 % (55639)Termination reason: Instruction limit % 199.29/28.34 % (55639)Termination phase: Saturation % 199.29/28.34 % (55639)Time elapsed: 0.567 s % 199.29/28.34 % (55639)Peak memory usage: 25 MB % 199.29/28.34 % (55639)Instructions burned: 2362 (million) % 199.29/28.34 % (55641)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3194431272:i=1778:ins=1:rtra=on_2794 on theBenchmark for (2794ds/1778Mi) % 199.29/28.34 % (55641)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 199.29/28.34 % (55641)Terminated due to inappropriate strategy. % 199.29/28.34 % (55641)------------------------------ % 199.29/28.34 % (55641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.29/28.34 % (55641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.29/28.34 % (55641)CaDiCaL version: 2.1.3 % 199.29/28.34 % (55641)Termination reason: Inappropriate % 199.29/28.34 % (55641)Time elapsed: 0.0000 s % 246.16/34.99 % (55641)Peak memory usage: 10 MB % 246.16/34.99 % (55641)Instructions burned: 1 (million) % 246.16/34.99 % (55641)------------------------------ % 246.16/34.99 % (55641)------------------------------ % 246.16/34.99 % (55643)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=4145611977:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2794 on theBenchmark for (2794ds/1384Mi) % 246.16/34.99 % (55643)Instruction limit reached! % 246.16/34.99 % (55643)------------------------------ % 246.16/34.99 % (55643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.16/34.99 % (55643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.16/34.99 % (55643)CaDiCaL version: 2.1.3 % 246.16/34.99 % (55643)Termination reason: Instruction limit % 246.16/34.99 % (55643)Termination phase: Saturation % 246.16/34.99 % (55643)Time elapsed: 0.419 s % 246.16/34.99 % (55643)Peak memory usage: 32 MB % 246.16/34.99 % (55643)Instructions burned: 1386 (million) % 246.16/34.99 % (55645)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=4114765364:i=1758:kws=inv_precedence:fsr=off:rtra=on_2789 on theBenchmark for (2789ds/1758Mi) % 246.16/34.99 % (55645)Instruction limit reached! % 246.16/34.99 % (55645)------------------------------ % 246.16/34.99 % (55645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.16/34.99 % (55645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.16/34.99 % (55645)CaDiCaL version: 2.1.3 % 246.16/34.99 % (55645)Termination reason: Instruction limit % 246.16/34.99 % (55645)Termination phase: Saturation % 246.16/34.99 % (55645)Time elapsed: 0.531 s % 246.16/34.99 % (55645)Peak memory usage: 25 MB % 246.16/34.99 % (55645)Instructions burned: 1758 (million) % 246.16/34.99 % (55647)fmb+10_1_sil=64000:si=on:random_seed=3558021026:i=44122:nm=2:rtra=on:gsp=on_2784 on theBenchmark for (2784ds/44122Mi) % 246.16/34.99 % (55647)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 246.16/34.99 % (55647)Terminated due to inappropriate strategy. % 246.16/34.99 % (55647)------------------------------ % 246.16/34.99 % (55647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.16/34.99 % (55647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.16/34.99 % (55647)CaDiCaL version: 2.1.3 % 246.16/34.99 % (55647)Termination reason: Inappropriate % 246.16/34.99 % (55647)Time elapsed: 0.0000 s % 246.16/34.99 % (55647)Peak memory usage: 11 MB % 246.16/34.99 % (55647)Instructions burned: 1 (million) % 246.16/34.99 % (55647)------------------------------ % 246.16/34.99 % (55647)------------------------------ % 246.16/34.99 % (55649)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3657797334:i=19030:nm=5:rtra=on_2784 on theBenchmark for (2784ds/19030Mi) % 246.16/34.99 % (55649)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 246.16/34.99 % (55649)Terminated due to inappropriate strategy. % 246.16/34.99 % (55649)------------------------------ % 246.16/34.99 % (55649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.16/34.99 % (55649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.16/34.99 % (55649)CaDiCaL version: 2.1.3 % 246.16/34.99 % (55649)Termination reason: Inappropriate % 246.16/34.99 % (55649)Time elapsed: 0.0000 s % 246.16/34.99 % (55649)Peak memory usage: 10 MB % 246.16/34.99 % (55649)Instructions burned: 1 (million) % 246.16/34.99 % (55649)------------------------------ % 246.16/34.99 % (55649)------------------------------ % 246.16/34.99 % (55651)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=741067645:fmbsr=1.7:i=1840:rtra=on_2783 on theBenchmark for (2783ds/1840Mi) % 246.16/34.99 % (55651)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 246.16/34.99 % (55651)Terminated due to inappropriate strategy. % 246.16/34.99 % (55651)------------------------------ % 246.16/34.99 % (55651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.16/34.99 % (55651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.16/34.99 % (55651)CaDiCaL version: 2.1.3 % 246.16/34.99 % (55651)Termination reason: Inappropriate % 246.16/34.99 % (55651)Time elapsed: 0.0000 s % 246.16/34.99 % (55651)Peak memory usage: 10 MB % 246.16/34.99 % (55651)Instructions burned: 1 (million) % 246.16/34.99 % (55651)------------------------------ % 246.16/34.99 % (55651)------------------------------ % 246.16/34.99 % (55653)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1408571980:i=10262:rtra=on_2783 on theBenchmark for (2783ds/10262Mi) % 266.74/37.85 % (55653)Instruction limit reached! % 266.74/37.85 % (55653)------------------------------ % 266.74/37.85 % (55653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.74/37.85 % (55653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.74/37.85 % (55653)CaDiCaL version: 2.1.3 % 266.74/37.85 % (55653)Termination reason: Instruction limit % 266.74/37.85 % (55653)Termination phase: Saturation % 266.74/37.85 % (55653)Time elapsed: 3.188 s % 266.74/37.85 % (55653)Peak memory usage: 69 MB % 266.74/37.85 % (55653)Instructions burned: 10263 (million) % 266.74/37.85 % (55655)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=969073330:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2751 on theBenchmark for (2751ds/2944Mi) % 266.74/37.85 % (55655)Instruction limit reached! % 266.74/37.85 % (55655)------------------------------ % 266.74/37.85 % (55655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.74/37.85 % (55655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.74/37.85 % (55655)CaDiCaL version: 2.1.3 % 266.74/37.85 % (55655)Termination reason: Instruction limit % 266.74/37.85 % (55655)Termination phase: Saturation % 266.74/37.85 % (55655)Time elapsed: 0.955 s % 266.74/37.85 % (55655)Peak memory usage: 41 MB % 266.74/37.85 % (55655)Instructions burned: 2945 (million) % 266.74/37.85 % (55657)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=852084472:i=12648:rtra=on_2742 on theBenchmark for (2742ds/12648Mi) % 266.74/37.85 % (55657)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 266.74/37.85 % (55657)Terminated due to inappropriate strategy. % 266.74/37.85 % (55657)------------------------------ % 266.74/37.85 % (55657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.74/37.85 % (55657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.74/37.85 % (55657)CaDiCaL version: 2.1.3 % 266.74/37.85 % (55657)Termination reason: Inappropriate % 266.74/37.85 % (55657)Time elapsed: 0.0000 s % 266.74/37.85 % (55657)Peak memory usage: 11 MB % 266.74/37.85 % (55657)Instructions burned: 1 (million) % 266.74/37.85 % (55657)------------------------------ % 266.74/37.85 % (55657)------------------------------ % 266.74/37.85 % (55659)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2588659668:fmbsr=2.30978:i=4348:rtra=on_2741 on theBenchmark for (2741ds/4348Mi) % 266.74/37.85 % (55659)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 266.74/37.85 % (55659)Terminated due to inappropriate strategy. % 266.74/37.85 % (55659)------------------------------ % 266.74/37.85 % (55659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.74/37.85 % (55659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.74/37.85 % (55659)CaDiCaL version: 2.1.3 % 266.74/37.85 % (55659)Termination reason: Inappropriate % 266.74/37.85 % (55659)Time elapsed: 0.0000 s % 266.74/37.85 % (55659)Peak memory usage: 10 MB % 266.74/37.85 % (55659)Instructions burned: 1 (million) % 266.74/37.85 % (55659)------------------------------ % 266.74/37.85 % (55659)------------------------------ % 266.74/37.85 % (55661)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3534580070:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2741 on theBenchmark for (2741ds/1738Mi) % 266.74/37.85 % (55661)Instruction limit reached! % 266.74/37.85 % (55661)------------------------------ % 266.74/37.85 % (55661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.74/37.85 % (55661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.74/37.85 % (55661)CaDiCaL version: 2.1.3 % 266.74/37.85 % (55661)Termination reason: Instruction limit % 266.74/37.85 % (55661)Termination phase: Saturation % 266.74/37.85 % (55661)Time elapsed: 0.592 s % 266.74/37.85 % (55661)Peak memory usage: 24 MB % 266.74/37.85 % (55661)Instructions burned: 1739 (million) % 266.74/37.85 % (55663)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2619936319:i=10228:av=off:rtra=on_2735 on theBenchmark for (2735ds/10228Mi) % 266.74/37.85 % (55601)Instruction limit reached! % 266.74/37.85 % (55601)------------------------------ % 266.74/37.85 % (55601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.74/37.85 % (55601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.74/37.85 % (55601)CaDiCaL version: 2.1.3 % 266.74/37.85 % (55601)Termination reason: Instruction limit % 266.74/37.85 % (55601)Termination phase: Saturation % 266.74/37.85 % (55601)Time elapsed: 12.648 s % 266.74/37.85 % (55601)Peak memory usage: 31 MB % 266.74/37.85 % (55601)ITerminated % 300.10/42.53 % Vampire exiting %------------------------------------------------------------------------------