%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC459_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n009.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:02 PM UTC 2026 % Result : Timeout 300.67s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC459_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 % Computer : n009.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 09:39:30 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.88/0.84 % (2915383)Will run a generic schedule for satisfiability detection. % 3.88/0.84 % (2915391)dis+10_1_sil=32000:sp=arity:random_seed=4204979898:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.88/0.84 % (2915389)% WARNING: option uhcvi not known. % 3.88/0.84 % (2915388)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=864940479_2999 on theBenchmark for (2999ds/0Mi) % 3.88/0.84 % (2915389)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2351606427:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.88/0.84 % (2915390)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1219515284:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.88/0.84 % (2915392)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2463881591:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.88/0.84 % (2915393)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3951760511:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.88/0.84 % (2915394)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=559007279:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.88/0.84 % (2915388)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.88/0.84 % (2915388)Terminated due to inappropriate strategy. % 3.88/0.84 % (2915388)------------------------------ % 3.88/0.84 % (2915388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.88/0.84 % (2915388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.88/0.84 % (2915388)CaDiCaL version: 2.1.3 % 3.88/0.84 % (2915388)Termination reason: Inappropriate % 3.88/0.84 % (2915388)Time elapsed: 0.001 s % 3.88/0.84 % (2915388)Peak memory usage: 10 MB % 3.88/0.84 % (2915388)------------------------------ % 3.88/0.84 % (2915388)------------------------------ % 3.88/0.84 % (2915402)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3011433448:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.88/0.84 % (2915402)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.88/0.84 % (2915402)Terminated due to inappropriate strategy. % 3.88/0.84 % (2915402)------------------------------ % 3.88/0.84 % (2915402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.88/0.84 % (2915402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.88/0.84 % (2915402)CaDiCaL version: 2.1.3 % 3.88/0.84 % (2915402)Termination reason: Inappropriate % 3.88/0.84 % (2915402)Time elapsed: 0.001 s % 3.88/0.84 % (2915402)Peak memory usage: 10 MB % 3.88/0.84 % (2915402)------------------------------ % 3.88/0.84 % (2915402)------------------------------ % 3.88/0.84 % (2915391)Instruction limit reached! % 3.88/0.84 % (2915391)------------------------------ % 3.88/0.84 % (2915391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.88/0.84 % (2915391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.88/0.84 % (2915391)CaDiCaL version: 2.1.3 % 3.88/0.84 % (2915391)Termination reason: Instruction limit % 3.88/0.84 % (2915391)Termination phase: Saturation % 3.88/0.84 % (2915391)Time elapsed: 0.036 s % 3.88/0.84 % (2915391)Peak memory usage: 12 MB % 3.88/0.84 % (2915391)Instructions burned: 106 (million) % 3.88/0.84 % (2915405)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=1600140815:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.88/0.84 % (2915404)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2629698818:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.88/0.84 % (2915392)Instruction limit reached! % 3.88/0.84 % (2915392)------------------------------ % 3.88/0.84 % (2915392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.88/0.84 % (2915392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.88/0.84 % (2915392)CaDiCaL version: 2.1.3 % 3.88/0.84 % (2915392)Termination reason: Instruction limit % 3.88/0.84 % (2915392)Termination phase: Saturation % 3.88/0.84 % (2915392)Time elapsed: 0.073 s % 3.88/0.84 % (2915392)Peak memory usage: 12 MB % 3.88/0.84 % (2915392)Instructions burned: 117 (million) % 3.88/0.84 % (2915393)Instruction limit reached! % 3.88/0.84 % (2915393)------------------------------ % 3.88/0.84 % (2915393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.88/0.84 % (2915393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.41/1.39 % (2915393)CaDiCaL version: 2.1.3 % 7.41/1.39 % (2915393)Termination reason: Instruction limit % 7.41/1.39 % (2915393)Termination phase: Saturation % 7.41/1.39 % (2915393)Time elapsed: 0.081 s % 7.41/1.39 % (2915393)Peak memory usage: 13 MB % 7.41/1.39 % (2915393)Instructions burned: 131 (million) % 7.41/1.39 % (2915408)ott-21_1_sil=16000:fs=off:random_seed=2586466147:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.41/1.39 % (2915409)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=835171910:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.41/1.39 % (2915394)Instruction limit reached! % 7.41/1.39 % (2915394)------------------------------ % 7.41/1.39 % (2915394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.41/1.39 % (2915394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.41/1.39 % (2915394)CaDiCaL version: 2.1.3 % 7.41/1.39 % (2915394)Termination reason: Instruction limit % 7.41/1.39 % (2915394)Termination phase: Saturation % 7.41/1.39 % (2915394)Time elapsed: 0.113 s % 7.41/1.39 % (2915394)Peak memory usage: 13 MB % 7.41/1.39 % (2915394)Instructions burned: 160 (million) % 7.41/1.39 % (2915412)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2445906014:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.41/1.39 % (2915412)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.41/1.39 % (2915412)Terminated due to inappropriate strategy. % 7.41/1.39 % (2915412)------------------------------ % 7.41/1.39 % (2915412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.41/1.39 % (2915412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.41/1.39 % (2915412)CaDiCaL version: 2.1.3 % 7.41/1.39 % (2915412)Termination reason: Inappropriate % 7.41/1.39 % (2915412)Time elapsed: 0.001 s % 7.41/1.39 % (2915412)Peak memory usage: 10 MB % 7.41/1.39 % (2915412)------------------------------ % 7.41/1.39 % (2915412)------------------------------ % 7.41/1.39 % (2915404)Instruction limit reached! % 7.41/1.39 % (2915404)------------------------------ % 7.41/1.39 % (2915404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.41/1.39 % (2915404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.41/1.39 % (2915404)CaDiCaL version: 2.1.3 % 7.41/1.39 % (2915404)Termination reason: Instruction limit % 7.41/1.39 % (2915404)Termination phase: Saturation % 7.41/1.39 % (2915404)Time elapsed: 0.094 s % 7.41/1.39 % (2915404)Peak memory usage: 13 MB % 7.41/1.39 % (2915404)Instructions burned: 132 (million) % 7.41/1.39 % (2915414)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2268166318:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.41/1.39 % (2915415)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1590126977:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 7.41/1.39 % (2915415)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.41/1.39 % (2915415)Terminated due to inappropriate strategy. % 7.41/1.39 % (2915415)------------------------------ % 7.41/1.39 % (2915415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.41/1.39 % (2915415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.41/1.39 % (2915415)CaDiCaL version: 2.1.3 % 7.41/1.39 % (2915415)Termination reason: Inappropriate % 7.41/1.39 % (2915415)Time elapsed: 0.001 s % 7.41/1.39 % (2915415)Peak memory usage: 10 MB % 7.41/1.39 % (2915415)------------------------------ % 7.41/1.39 % (2915415)------------------------------ % 7.41/1.39 % (2915408)Instruction limit reached! % 7.41/1.39 % (2915408)------------------------------ % 7.41/1.39 % (2915408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.41/1.39 % (2915408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.41/1.39 % (2915408)CaDiCaL version: 2.1.3 % 7.41/1.39 % (2915408)Termination reason: Instruction limit % 7.41/1.39 % (2915408)Termination phase: Saturation % 7.41/1.39 % (2915408)Time elapsed: 0.079 s % 7.41/1.39 % (2915408)Peak memory usage: 12 MB % 7.41/1.39 % (2915408)Instructions burned: 182 (million) % 7.41/1.39 % (2915418)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=1395222367: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.41/1.39 % (2915419)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1412808492:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.49/3.18 % (2915405)Instruction limit reached! % 20.49/3.18 % (2915405)------------------------------ % 20.49/3.18 % (2915405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.49/3.18 % (2915405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.49/3.18 % (2915405)CaDiCaL version: 2.1.3 % 20.49/3.18 % (2915405)Termination reason: Instruction limit % 20.49/3.18 % (2915405)Termination phase: Saturation % 20.49/3.18 % (2915405)Time elapsed: 0.182 s % 20.49/3.18 % (2915405)Peak memory usage: 16 MB % 20.49/3.18 % (2915405)Instructions burned: 684 (million) % 20.49/3.18 % (2915422)fmb+10_1_sil=64000:random_seed=1393856043:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 20.49/3.18 % (2915422)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.49/3.18 % (2915422)Terminated due to inappropriate strategy. % 20.49/3.18 % (2915422)------------------------------ % 20.49/3.18 % (2915422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.49/3.18 % (2915422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.49/3.18 % (2915422)CaDiCaL version: 2.1.3 % 20.49/3.18 % (2915422)Termination reason: Inappropriate % 20.49/3.18 % (2915422)Time elapsed: 0.0000 s % 20.49/3.18 % (2915422)Peak memory usage: 10 MB % 20.49/3.18 % (2915422)------------------------------ % 20.49/3.18 % (2915422)------------------------------ % 20.49/3.18 % (2915424)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4102500378:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 20.49/3.18 % (2915424)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.49/3.18 % (2915424)Terminated due to inappropriate strategy. % 20.49/3.18 % (2915424)------------------------------ % 20.49/3.18 % (2915424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.49/3.18 % (2915424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.49/3.18 % (2915424)CaDiCaL version: 2.1.3 % 20.49/3.18 % (2915424)Termination reason: Inappropriate % 20.49/3.18 % (2915424)Time elapsed: 0.0000 s % 20.49/3.18 % (2915424)Peak memory usage: 10 MB % 20.49/3.18 % (2915424)------------------------------ % 20.49/3.18 % (2915424)------------------------------ % 20.49/3.18 % (2915426)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2924199887:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 20.49/3.18 % (2915426)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.49/3.18 % (2915426)Terminated due to inappropriate strategy. % 20.49/3.18 % (2915426)------------------------------ % 20.49/3.18 % (2915426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.49/3.18 % (2915426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.49/3.18 % (2915426)CaDiCaL version: 2.1.3 % 20.49/3.18 % (2915426)Termination reason: Inappropriate % 20.49/3.18 % (2915426)Time elapsed: 0.0000 s % 20.49/3.18 % (2915426)Peak memory usage: 10 MB % 20.49/3.18 % (2915426)------------------------------ % 20.49/3.18 % (2915426)------------------------------ % 20.49/3.18 % (2915428)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3044269836:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 20.49/3.18 % (2915409)Instruction limit reached! % 20.49/3.18 % (2915409)------------------------------ % 20.49/3.18 % (2915409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.49/3.18 % (2915409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.49/3.18 % (2915409)CaDiCaL version: 2.1.3 % 20.49/3.18 % (2915409)Termination reason: Instruction limit % 20.49/3.18 % (2915409)Termination phase: Saturation % 20.49/3.18 % (2915409)Time elapsed: 0.289 s % 20.49/3.18 % (2915409)Peak memory usage: 14 MB % 20.49/3.18 % (2915409)Instructions burned: 477 (million) % 20.49/3.18 % (2915430)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1491490800:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 20.49/3.18 % (2915418)Instruction limit reached! % 20.49/3.18 % (2915418)------------------------------ % 20.49/3.18 % (2915418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.49/3.18 % (2915418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.49/3.18 % (2915418)CaDiCaL version: 2.1.3 % 20.49/3.18 % (2915418)Termination reason: Instruction limit % 28.09/4.21 % (2915418)Termination phase: Saturation % 28.09/4.21 % (2915418)Time elapsed: 0.399 s % 28.09/4.21 % (2915418)Peak memory usage: 16 MB % 28.09/4.21 % (2915418)Instructions burned: 693 (million) % 28.09/4.21 % (2915432)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2328252452:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 28.09/4.21 % (2915432)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.09/4.21 % (2915432)Terminated due to inappropriate strategy. % 28.09/4.21 % (2915432)------------------------------ % 28.09/4.21 % (2915432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.09/4.21 % (2915432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.09/4.21 % (2915432)CaDiCaL version: 2.1.3 % 28.09/4.21 % (2915432)Termination reason: Inappropriate % 28.09/4.21 % (2915432)Time elapsed: 0.001 s % 28.09/4.21 % (2915432)Peak memory usage: 10 MB % 28.09/4.21 % (2915432)------------------------------ % 28.09/4.21 % (2915432)------------------------------ % 28.09/4.21 % (2915434)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2824260860:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 28.09/4.21 % (2915434)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.09/4.21 % (2915434)Terminated due to inappropriate strategy. % 28.09/4.21 % (2915434)------------------------------ % 28.09/4.21 % (2915434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.09/4.21 % (2915434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.09/4.21 % (2915434)CaDiCaL version: 2.1.3 % 28.09/4.21 % (2915434)Termination reason: Inappropriate % 28.09/4.21 % (2915434)Time elapsed: 0.001 s % 28.09/4.21 % (2915434)Peak memory usage: 10 MB % 28.09/4.21 % (2915434)------------------------------ % 28.09/4.21 % (2915434)------------------------------ % 28.09/4.21 % (2915436)ott-2_1_sil=16000:newcnf=on:random_seed=153619063:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 28.09/4.21 % (2915419)Instruction limit reached! % 28.09/4.21 % (2915419)------------------------------ % 28.09/4.21 % (2915419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.09/4.21 % (2915419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.09/4.21 % (2915419)CaDiCaL version: 2.1.3 % 28.09/4.21 % (2915419)Termination reason: Instruction limit % 28.09/4.21 % (2915419)Termination phase: Saturation % 28.09/4.21 % (2915419)Time elapsed: 0.499 s % 28.09/4.21 % (2915419)Peak memory usage: 19 MB % 28.09/4.21 % (2915419)Instructions burned: 879 (million) % 28.09/4.21 % (2915438)ott+10_1_sil=32000:tgt=ground:random_seed=1572305704:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 28.09/4.21 % (2915414)Instruction limit reached! % 28.09/4.21 % (2915414)------------------------------ % 28.09/4.21 % (2915414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.09/4.21 % (2915414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.09/4.21 % (2915414)CaDiCaL version: 2.1.3 % 28.09/4.21 % (2915414)Termination reason: Instruction limit % 28.09/4.21 % (2915414)Termination phase: Saturation % 28.09/4.21 % (2915414)Time elapsed: 0.736 s % 28.09/4.21 % (2915414)Peak memory usage: 18 MB % 28.09/4.21 % (2915414)Instructions burned: 1179 (million) % 28.09/4.21 % (2915440)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3596398189:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 28.09/4.21 % (2915440)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.09/4.21 % (2915440)Terminated due to inappropriate strategy. % 28.09/4.21 % (2915440)------------------------------ % 28.09/4.21 % (2915440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.09/4.21 % (2915440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.09/4.21 % (2915440)CaDiCaL version: 2.1.3 % 28.09/4.21 % (2915440)Termination reason: Inappropriate % 28.09/4.21 % (2915440)Time elapsed: 0.001 s % 28.09/4.21 % (2915440)Peak memory usage: 10 MB % 28.09/4.21 % (2915440)------------------------------ % 28.09/4.21 % (2915440)------------------------------ % 28.09/4.21 % (2915442)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1758477313:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 28.09/4.21 % (2915430)Instruction limit reached! % 28.09/4.21 % (2915430)------------------------------ % 28.09/4.21 % (2915430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.09/4.21 % (2915430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.90/12.25 % (2915430)CaDiCaL version: 2.1.3 % 84.90/12.25 % (2915430)Termination reason: Instruction limit % 84.90/12.25 % (2915430)Termination phase: Saturation % 84.90/12.25 % (2915430)Time elapsed: 0.708 s % 84.90/12.25 % (2915430)Peak memory usage: 22 MB % 84.90/12.25 % (2915430)Instructions burned: 1474 (million) % 84.90/12.25 % (2915444)dis+21_1_sil=32000:sas=cadical:random_seed=3054896810:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 84.90/12.25 % (2915436)Instruction limit reached! % 84.90/12.25 % (2915436)------------------------------ % 84.90/12.25 % (2915436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.90/12.25 % (2915436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.90/12.25 % (2915436)CaDiCaL version: 2.1.3 % 84.90/12.25 % (2915436)Termination reason: Instruction limit % 84.90/12.25 % (2915436)Termination phase: Saturation % 84.90/12.25 % (2915436)Time elapsed: 0.537 s % 84.90/12.25 % (2915436)Peak memory usage: 15 MB % 84.90/12.25 % (2915436)Instructions burned: 870 (million) % 84.90/12.25 % (2915446)ott+11_1_sil=16000:gs=on:random_seed=4246450080:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 84.90/12.25 % (2915428)Instruction limit reached! % 84.90/12.25 % (2915428)------------------------------ % 84.90/12.25 % (2915428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.90/12.25 % (2915428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.90/12.25 % (2915428)CaDiCaL version: 2.1.3 % 84.90/12.25 % (2915428)Termination reason: Instruction limit % 84.90/12.25 % (2915428)Termination phase: Saturation % 84.90/12.25 % (2915428)Time elapsed: 1.469 s % 84.90/12.25 % (2915428)Peak memory usage: 41 MB % 84.90/12.25 % (2915428)Instructions burned: 5132 (million) % 84.90/12.25 % (2915448)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=377582187:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 84.90/12.25 % (2915448)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 84.90/12.25 % (2915448)Terminated due to inappropriate strategy. % 84.90/12.25 % (2915448)------------------------------ % 84.90/12.25 % (2915448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.90/12.25 % (2915448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.90/12.25 % (2915448)CaDiCaL version: 2.1.3 % 84.90/12.25 % (2915448)Termination reason: Inappropriate % 84.90/12.25 % (2915448)Time elapsed: 0.0000 s % 84.90/12.25 % (2915448)Peak memory usage: 11 MB % 84.90/12.25 % (2915448)Instructions burned: 1 (million) % 84.90/12.25 % (2915448)------------------------------ % 84.90/12.25 % (2915448)------------------------------ % 84.90/12.25 % (2915450)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3641231362:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 84.90/12.25 % (2915446)Instruction limit reached! % 84.90/12.25 % (2915446)------------------------------ % 84.90/12.25 % (2915446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.90/12.25 % (2915446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.90/12.25 % (2915446)CaDiCaL version: 2.1.3 % 84.90/12.25 % (2915446)Termination reason: Instruction limit % 84.90/12.25 % (2915446)Termination phase: Saturation % 84.90/12.25 % (2915446)Time elapsed: 1.222 s % 84.90/12.25 % (2915446)Peak memory usage: 24 MB % 84.90/12.25 % (2915446)Instructions burned: 2252 (million) % 84.90/12.25 % (2915452)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=43071253:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 84.90/12.25 % (2915442)Instruction limit reached! % 84.90/12.25 % (2915442)------------------------------ % 84.90/12.25 % (2915442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.90/12.25 % (2915442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.90/12.25 % (2915442)CaDiCaL version: 2.1.3 % 84.90/12.25 % (2915442)Termination reason: Instruction limit % 84.90/12.25 % (2915442)Termination phase: Saturation % 84.90/12.25 % (2915442)Time elapsed: 1.856 s % 84.90/12.25 % (2915442)Peak memory usage: 35 MB % 84.90/12.25 % (2915442)Instructions burned: 3512 (million) % 84.90/12.25 % (2915454)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4038914323:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 84.90/12.25 % (2915450)Instruction limit reached! % 84.90/12.25 % (2915450)------------------------------ % 84.90/12.25 % (2915450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.61/16.67 % (2915450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.61/16.67 % (2915450)CaDiCaL version: 2.1.3 % 115.61/16.67 % (2915450)Termination reason: Instruction limit % 115.61/16.67 % (2915450)Termination phase: Saturation % 115.61/16.67 % (2915450)Time elapsed: 1.149 s % 115.61/16.67 % (2915450)Peak memory usage: 46 MB % 115.61/16.67 % (2915450)Instructions burned: 4595 (million) % 115.61/16.67 % (2915456)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1909479322:i=5497:nm=2_2970 on theBenchmark for (2970ds/5497Mi) % 115.61/16.67 % (2915456)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 115.61/16.67 % (2915456)Terminated due to inappropriate strategy. % 115.61/16.67 % (2915456)------------------------------ % 115.61/16.67 % (2915456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.61/16.67 % (2915456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.61/16.67 % (2915456)CaDiCaL version: 2.1.3 % 115.61/16.67 % (2915456)Termination reason: Inappropriate % 115.61/16.67 % (2915456)Time elapsed: 0.0000 s % 115.61/16.67 % (2915456)Peak memory usage: 10 MB % 115.61/16.67 % (2915456)------------------------------ % 115.61/16.67 % (2915456)------------------------------ % 115.61/16.67 % (2915458)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=162069702:fmbsr=2:i=46332_2970 on theBenchmark for (2970ds/46332Mi) % 115.61/16.67 % (2915458)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 115.61/16.67 % (2915458)Terminated due to inappropriate strategy. % 115.61/16.67 % (2915458)------------------------------ % 115.61/16.67 % (2915458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.61/16.67 % (2915458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.61/16.67 % (2915458)CaDiCaL version: 2.1.3 % 115.61/16.67 % (2915458)Termination reason: Inappropriate % 115.61/16.67 % (2915458)Time elapsed: 0.0000 s % 115.61/16.67 % (2915458)Peak memory usage: 10 MB % 115.61/16.67 % (2915458)Instructions burned: 1 (million) % 115.61/16.67 % (2915458)------------------------------ % 115.61/16.67 % (2915458)------------------------------ % 115.61/16.67 % (2915460)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=55638917:i=14071_2970 on theBenchmark for (2970ds/14071Mi) % 115.61/16.67 % (2915460)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 115.61/16.67 % (2915460)Terminated due to inappropriate strategy. % 115.61/16.67 % (2915460)------------------------------ % 115.61/16.67 % (2915460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.61/16.67 % (2915460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.61/16.67 % (2915460)CaDiCaL version: 2.1.3 % 115.61/16.67 % (2915460)Termination reason: Inappropriate % 115.61/16.67 % (2915460)Time elapsed: 0.0000 s % 115.61/16.67 % (2915460)Peak memory usage: 10 MB % 115.61/16.67 % (2915460)Instructions burned: 1 (million) % 115.61/16.67 % (2915460)------------------------------ % 115.61/16.67 % (2915460)------------------------------ % 115.61/16.67 % (2915462)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3750796759:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 115.61/16.67 % (2915444)Instruction limit reached! % 115.61/16.67 % (2915444)------------------------------ % 115.61/16.67 % (2915444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.61/16.67 % (2915444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.61/16.67 % (2915444)CaDiCaL version: 2.1.3 % 115.61/16.67 % (2915444)Termination reason: Instruction limit % 115.61/16.67 % (2915444)Termination phase: Saturation % 115.61/16.67 % (2915444)Time elapsed: 2.028 s % 115.61/16.67 % (2915444)Peak memory usage: 31 MB % 115.61/16.67 % (2915444)Instructions burned: 3774 (million) % 115.61/16.67 % (2915464)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=946014454:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 115.61/16.67 % (2915438)Instruction limit reached! % 115.61/16.67 % (2915438)------------------------------ % 115.61/16.67 % (2915438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.61/16.67 % (2915438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.61/16.67 % (2915438)CaDiCaL version: 2.1.3 % 115.61/16.67 % (2915438)Termination reason: Instruction limit % 115.61/16.67 % (2915438)Termination phase: Saturation % 115.61/16.67 % (2915438)Time elapsed: 3.229 s % 115.61/16.67 % (2915438)Peak memory usage: 39 MB % 115.61/16.67 % (2915438)Instructions burned: 5115 (million) % 116.24/16.75 % (2915466)dis+10_16:1_sil=16000:random_seed=822032950:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi) % 116.24/16.75 % (2915454)Instruction limit reached! % 116.24/16.75 % (2915454)------------------------------ % 116.24/16.75 % (2915454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.24/16.75 % (2915454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.24/16.75 % (2915454)CaDiCaL version: 2.1.3 % 116.24/16.75 % (2915454)Termination reason: Instruction limit % 116.24/16.75 % (2915454)Termination phase: Saturation % 116.24/16.75 % (2915454)Time elapsed: 2.747 s % 116.24/16.75 % (2915454)Peak memory usage: 49 MB % 116.24/16.75 % (2915454)Instructions burned: 5212 (million) % 116.24/16.75 % (2915468)ott-3_8_sil=64000:random_seed=3760493490:i=20139:bs=on_2943 on theBenchmark for (2943ds/20139Mi) % 116.24/16.75 % (2915462)Instruction limit reached! % 116.24/16.75 % (2915462)------------------------------ % 116.24/16.75 % (2915462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.24/16.75 % (2915462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.24/16.75 % (2915462)CaDiCaL version: 2.1.3 % 116.24/16.75 % (2915462)Termination reason: Instruction limit % 116.24/16.75 % (2915462)Termination phase: Saturation % 116.24/16.75 % (2915462)Time elapsed: 5.164 s % 116.24/16.75 % (2915462)Peak memory usage: 75 MB % 116.24/16.75 % (2915462)Instructions burned: 22567 (million) % 116.24/16.75 % (2915470)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2601118103:fmbsr=2:i=32576_2918 on theBenchmark for (2918ds/32576Mi) % 116.24/16.75 % (2915470)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.24/16.75 % (2915470)Terminated due to inappropriate strategy. % 116.24/16.75 % (2915470)------------------------------ % 116.24/16.75 % (2915470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.24/16.75 % (2915470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.24/16.75 % (2915470)CaDiCaL version: 2.1.3 % 116.24/16.75 % (2915470)Termination reason: Inappropriate % 116.24/16.75 % (2915470)Time elapsed: 0.0000 s % 116.24/16.75 % (2915470)Peak memory usage: 10 MB % 116.24/16.75 % (2915470)Instructions burned: 1 (million) % 116.24/16.75 % (2915470)------------------------------ % 116.24/16.75 % (2915470)------------------------------ % 116.24/16.75 % (2915472)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2500469002:i=11404_2918 on theBenchmark for (2918ds/11404Mi) % 116.24/16.75 % (2915464)Instruction limit reached! % 116.24/16.75 % (2915464)------------------------------ % 116.24/16.75 % (2915464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.24/16.75 % (2915464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.24/16.75 % (2915464)CaDiCaL version: 2.1.3 % 116.24/16.75 % (2915464)Termination reason: Instruction limit % 116.24/16.75 % (2915464)Termination phase: Saturation % 116.24/16.75 % (2915464)Time elapsed: 5.039 s % 116.24/16.75 % (2915464)Peak memory usage: 51 MB % 116.24/16.75 % (2915464)Instructions burned: 8173 (million) % 116.24/16.75 % (2915474)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2180763680:i=14134_2917 on theBenchmark for (2917ds/14134Mi) % 116.24/16.75 % (2915466)Instruction limit reached! % 116.24/16.75 % (2915466)------------------------------ % 116.24/16.75 % (2915466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.24/16.75 % (2915466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.24/16.75 % (2915466)CaDiCaL version: 2.1.3 % 116.24/16.75 % (2915466)Termination reason: Instruction limit % 116.24/16.75 % (2915466)Termination phase: Saturation % 116.24/16.75 % (2915466)Time elapsed: 4.595 s % 116.24/16.75 % (2915466)Peak memory usage: 52 MB % 116.24/16.75 % (2915466)Instructions burned: 9156 (million) % 116.24/16.75 % (2915476)dis+33_16_sil=32000:sac=on:random_seed=538914694:i=15851:nm=0_2913 on theBenchmark for (2913ds/15851Mi) % 116.24/16.75 % (2915472)Instruction limit reached! % 116.24/16.75 % (2915472)------------------------------ % 116.24/16.75 % (2915472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.24/16.75 % (2915472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.24/16.75 % (2915472)CaDiCaL version: 2.1.3 % 116.24/16.75 % (2915472)Termination reason: Instruction limit % 116.24/16.75 % (2915472)Termination phase: Saturation % 116.24/16.75 % (2915472)Time elapsed: 3.816 s % 116.24/16.75 % (2915472)Peak memory usage: 71 MB % 116.24/16.75 % (2915472)Instructions burned: 11406 (million) % 116.24/16.75 % (2915598)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3227520364:avsq=on:i=17627:add=on:amm=off_2879 on theBenchmark for (2879ds/17627Mi) % 126.29/18.10 % (2915452)Instruction limit reached! % 126.29/18.10 % (2915452)------------------------------ % 126.29/18.10 % (2915452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.29/18.10 % (2915452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.29/18.10 % (2915452)CaDiCaL version: 2.1.3 % 126.29/18.10 % (2915452)Termination reason: Instruction limit % 126.29/18.10 % (2915452)Termination phase: Saturation % 126.29/18.10 % (2915452)Time elapsed: 12.798 s % 126.29/18.10 % (2915452)Peak memory usage: 168 MB % 126.29/18.10 % (2915452)Instructions burned: 29340 (million) % 126.29/18.10 % (2915960)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2077302882:s2a=on:i=53295_2847 on theBenchmark for (2847ds/53295Mi) % 126.29/18.10 % (2915476)Instruction limit reached! % 126.29/18.10 % (2915476)------------------------------ % 126.29/18.10 % (2915476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.29/18.10 % (2915476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.29/18.10 % (2915476)CaDiCaL version: 2.1.3 % 126.29/18.10 % (2915476)Termination reason: Instruction limit % 126.29/18.10 % (2915476)Termination phase: Saturation % 126.29/18.10 % (2915476)Time elapsed: 7.172 s % 126.29/18.10 % (2915476)Peak memory usage: 205 MB % 126.29/18.10 % (2915476)Instructions burned: 15853 (million) % 126.29/18.10 % (2915962)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1576230439:i=26857:ins=20_2841 on theBenchmark for (2841ds/26857Mi) % 126.29/18.10 % (2915962)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.29/18.10 % (2915962)Terminated due to inappropriate strategy. % 126.29/18.10 % (2915962)------------------------------ % 126.29/18.10 % (2915962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.29/18.10 % (2915962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.29/18.10 % (2915962)CaDiCaL version: 2.1.3 % 126.29/18.10 % (2915962)Termination reason: Inappropriate % 126.29/18.10 % (2915962)Time elapsed: 0.001 s % 126.29/18.10 % (2915962)Peak memory usage: 10 MB % 126.29/18.10 % (2915962)------------------------------ % 126.29/18.10 % (2915962)------------------------------ % 126.29/18.10 % (2915964)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=902443077:i=28120:bs=on:fsr=off_2841 on theBenchmark for (2841ds/28120Mi) % 126.29/18.10 % (2915598)Instruction limit reached! % 126.29/18.10 % (2915598)------------------------------ % 126.29/18.10 % (2915598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.29/18.10 % (2915598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.29/18.10 % (2915598)CaDiCaL version: 2.1.3 % 126.29/18.10 % (2915598)Termination reason: Instruction limit % 126.29/18.10 % (2915598)Termination phase: Saturation % 126.29/18.10 % (2915598)Time elapsed: 4.378 s % 126.29/18.10 % (2915598)Peak memory usage: 234 MB % 126.29/18.10 % (2915598)Instructions burned: 17630 (million) % 126.29/18.10 % (2915966)fmb+10_1_sil=256000:fmbss=7:random_seed=3405457373:fmbsr=1.6:i=182295_2835 on theBenchmark for (2835ds/182295Mi) % 126.29/18.10 % (2915966)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.29/18.10 % (2915966)Terminated due to inappropriate strategy. % 126.29/18.10 % (2915966)------------------------------ % 126.29/18.10 % (2915966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.29/18.10 % (2915966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.29/18.10 % (2915966)CaDiCaL version: 2.1.3 % 126.29/18.10 % (2915966)Termination reason: Inappropriate % 126.29/18.10 % (2915966)Time elapsed: 0.0000 s % 126.29/18.10 % (2915966)Peak memory usage: 10 MB % 126.29/18.10 % (2915966)------------------------------ % 126.29/18.10 % (2915966)------------------------------ % 126.29/18.10 % (2915968)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2765220781:i=44625:gsp=on_2835 on theBenchmark for (2835ds/44625Mi) % 126.29/18.10 % (2915968)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.29/18.10 % (2915968)Terminated due to inappropriate strategy. % 126.29/18.10 % (2915968)------------------------------ % 126.29/18.10 % (2915968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.29/18.10 % (2915968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.29/18.10 % (2915968)CaDiCaL version: 2.1.3 % 126.29/18.10 % (2915968)Termination reason: Inappropriate % 126.29/18.10 % (2915968)Time elapsed: 0.0000 s % 150.19/21.42 % (2915968)Peak memory usage: 10 MB % 150.19/21.42 % (2915968)------------------------------ % 150.19/21.42 % (2915968)------------------------------ % 150.19/21.42 % (2915970)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2130338746:i=160505_2835 on theBenchmark for (2835ds/160505Mi) % 150.19/21.42 % (2915970)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.19/21.42 % (2915970)Terminated due to inappropriate strategy. % 150.19/21.42 % (2915970)------------------------------ % 150.19/21.42 % (2915970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.19/21.42 % (2915970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.19/21.42 % (2915970)CaDiCaL version: 2.1.3 % 150.19/21.42 % (2915970)Termination reason: Inappropriate % 150.19/21.42 % (2915970)Time elapsed: 0.001 s % 150.19/21.42 % (2915970)Peak memory usage: 10 MB % 150.19/21.42 % (2915970)------------------------------ % 150.19/21.42 % (2915970)------------------------------ % 150.19/21.42 % (2915468)Instruction limit reached! % 150.19/21.42 % (2915468)------------------------------ % 150.19/21.42 % (2915468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.19/21.42 % (2915468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.19/21.42 % (2915468)CaDiCaL version: 2.1.3 % 150.19/21.42 % (2915468)Termination reason: Instruction limit % 150.19/21.42 % (2915468)Termination phase: Saturation % 150.19/21.42 % (2915468)Time elapsed: 10.855 s % 150.19/21.42 % (2915468)Peak memory usage: 56 MB % 150.19/21.42 % (2915468)Instructions burned: 20141 (million) % 150.19/21.42 % (2915972)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1787495431:fmbsr=1.3:i=225729_2835 on theBenchmark for (2835ds/225729Mi) % 150.19/21.42 % (2915972)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.19/21.42 % (2915972)Terminated due to inappropriate strategy. % 150.19/21.42 % (2915972)------------------------------ % 150.19/21.42 % (2915972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.19/21.42 % (2915972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.19/21.42 % (2915972)CaDiCaL version: 2.1.3 % 150.19/21.42 % (2915972)Termination reason: Inappropriate % 150.19/21.42 % (2915972)Time elapsed: 0.0000 s % 150.19/21.42 % (2915972)Peak memory usage: 11 MB % 150.19/21.42 % (2915972)Instructions burned: 1 (million) % 150.19/21.42 % (2915972)------------------------------ % 150.19/21.42 % (2915972)------------------------------ % 150.19/21.42 % (2915975)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3511941922:rtra=on_2835 on theBenchmark for (2835ds/0Mi) % 150.19/21.42 % (2915975)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.19/21.42 % (2915975)Terminated due to inappropriate strategy. % 150.19/21.42 % (2915975)------------------------------ % 150.19/21.42 % (2915975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.19/21.42 % (2915975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.19/21.42 % (2915975)CaDiCaL version: 2.1.3 % 150.19/21.42 % (2915975)Termination reason: Inappropriate % 150.19/21.42 % (2915975)Time elapsed: 0.0000 s % 150.19/21.42 % (2915975)Peak memory usage: 10 MB % 150.19/21.42 % (2915975)------------------------------ % 150.19/21.42 % (2915975)------------------------------ % 150.19/21.42 % (2915974)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=814533327:fmbsr=2:i=185024:ins=7_2835 on theBenchmark for (2835ds/185024Mi) % 150.19/21.42 % (2915974)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.19/21.42 % (2915974)Terminated due to inappropriate strategy. % 150.19/21.42 % (2915974)------------------------------ % 150.19/21.42 % (2915974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.19/21.42 % (2915974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.19/21.42 % (2915974)CaDiCaL version: 2.1.3 % 150.19/21.42 % (2915974)Termination reason: Inappropriate % 150.19/21.42 % (2915974)Time elapsed: 0.001 s % 150.19/21.42 % (2915974)Peak memory usage: 10 MB % 150.19/21.42 % (2915974)Instructions burned: 1 (million) % 150.19/21.42 % (2915974)------------------------------ % 150.19/21.42 % (2915974)------------------------------ % 150.19/21.42 % (2915977)% WARNING: option uhcvi not known. % 150.19/21.42 % (2915977)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2852496637:i=271062:add=off:rtra=on:rawr=on_2835 on theBenchmark for (2835ds/271062Mi) % 150.19/21.42 % (2915979)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2679129185:i=176048:add=on:rtra=on:rawr=on_2834 on theBenchmark for (2834ds/176048Mi) % 163.65/23.34 % (2915474)Instruction limit reached! % 163.65/23.34 % (2915474)------------------------------ % 163.65/23.34 % (2915474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.65/23.34 % (2915474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.65/23.34 % (2915474)CaDiCaL version: 2.1.3 % 163.65/23.34 % (2915474)Termination reason: Instruction limit % 163.65/23.34 % (2915474)Termination phase: Saturation % 163.65/23.34 % (2915474)Time elapsed: 8.789 s % 163.65/23.34 % (2915474)Peak memory usage: 72 MB % 163.65/23.34 % (2915474)Instructions burned: 14134 (million) % 163.65/23.34 % (2915982)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3347156166:i=206:fgj=on:rtra=on_2829 on theBenchmark for (2829ds/206Mi) % 163.65/23.34 % (2915982)Instruction limit reached! % 163.65/23.34 % (2915982)------------------------------ % 163.65/23.34 % (2915982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.65/23.34 % (2915982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.65/23.34 % (2915982)CaDiCaL version: 2.1.3 % 163.65/23.34 % (2915982)Termination reason: Instruction limit % 163.65/23.34 % (2915982)Termination phase: Saturation % 163.65/23.34 % (2915982)Time elapsed: 0.127 s % 163.65/23.34 % (2915982)Peak memory usage: 13 MB % 163.65/23.34 % (2915982)Instructions burned: 206 (million) % 163.65/23.34 % (2915984)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4135995092:i=232:rtra=on_2827 on theBenchmark for (2827ds/232Mi) % 163.65/23.34 % (2915984)Instruction limit reached! % 163.65/23.34 % (2915984)------------------------------ % 163.65/23.34 % (2915984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.65/23.34 % (2915984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.65/23.34 % (2915984)CaDiCaL version: 2.1.3 % 163.65/23.34 % (2915984)Termination reason: Instruction limit % 163.65/23.34 % (2915984)Termination phase: Saturation % 163.65/23.34 % (2915984)Time elapsed: 0.149 s % 163.65/23.34 % (2915984)Peak memory usage: 13 MB % 163.65/23.34 % (2915984)Instructions burned: 233 (million) % 163.65/23.34 % (2915986)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2744576004:i=262:rtra=on_2825 on theBenchmark for (2825ds/262Mi) % 163.65/23.34 % (2915986)Instruction limit reached! % 163.65/23.34 % (2915986)------------------------------ % 163.65/23.34 % (2915986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.65/23.34 % (2915986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.65/23.34 % (2915986)CaDiCaL version: 2.1.3 % 163.65/23.34 % (2915986)Termination reason: Instruction limit % 163.65/23.34 % (2915986)Termination phase: Saturation % 163.65/23.34 % (2915986)Time elapsed: 0.161 s % 163.65/23.34 % (2915986)Peak memory usage: 13 MB % 163.65/23.34 % (2915986)Instructions burned: 262 (million) % 163.65/23.34 % (2915988)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=826420306:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2824 on theBenchmark for (2824ds/318Mi) % 163.65/23.34 % (2915988)Instruction limit reached! % 163.65/23.34 % (2915988)------------------------------ % 163.65/23.34 % (2915988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.65/23.34 % (2915988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.65/23.34 % (2915988)CaDiCaL version: 2.1.3 % 163.65/23.34 % (2915988)Termination reason: Instruction limit % 163.65/23.34 % (2915988)Termination phase: Saturation % 163.65/23.34 % (2915988)Time elapsed: 0.216 s % 163.65/23.34 % (2915988)Peak memory usage: 15 MB % 163.65/23.34 % (2915988)Instructions burned: 319 (million) % 163.65/23.34 % (2915990)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2304395888:i=1428:nm=2:rtra=on_2821 on theBenchmark for (2821ds/1428Mi) % 163.65/23.34 % (2915990)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 163.65/23.34 % (2915990)Terminated due to inappropriate strategy. % 163.65/23.34 % (2915990)------------------------------ % 163.65/23.34 % (2915990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.65/23.34 % (2915990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.65/23.34 % (2915990)CaDiCaL version: 2.1.3 % 163.65/23.34 % (2915990)Termination reason: Inappropriate % 163.65/23.34 % (2915990)Time elapsed: 0.001 s % 163.65/23.34 % (2915990)Peak memory usage: 10 MB % 163.65/23.34 % (2915990)------------------------------ % 163.65/23.34 % (2915990)------------------------------ % 163.65/23.34 % (2915992)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1828206955:i=262:bd=preordered:rtra=on:fsd=on_2821 on theBenchmark for (2821ds/262Mi) % 206.17/29.30 % (2915992)Instruction limit reached! % 206.17/29.30 % (2915992)------------------------------ % 206.17/29.30 % (2915992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.17/29.30 % (2915992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.17/29.30 % (2915992)CaDiCaL version: 2.1.3 % 206.17/29.30 % (2915992)Termination reason: Instruction limit % 206.17/29.30 % (2915992)Termination phase: Saturation % 206.17/29.30 % (2915992)Time elapsed: 0.177 s % 206.17/29.30 % (2915992)Peak memory usage: 14 MB % 206.17/29.30 % (2915992)Instructions burned: 263 (million) % 206.17/29.30 % (2915994)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=1147851577:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2819 on theBenchmark for (2819ds/1368Mi) % 206.17/29.30 % (2915994)Instruction limit reached! % 206.17/29.30 % (2915994)------------------------------ % 206.17/29.30 % (2915994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.17/29.30 % (2915994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.17/29.30 % (2915994)CaDiCaL version: 2.1.3 % 206.17/29.30 % (2915994)Termination reason: Instruction limit % 206.17/29.30 % (2915994)Termination phase: Saturation % 206.17/29.30 % (2915994)Time elapsed: 0.714 s % 206.17/29.30 % (2915994)Peak memory usage: 22 MB % 206.17/29.30 % (2915994)Instructions burned: 1369 (million) % 206.17/29.30 % (2915996)ott-21_1_sil=16000:si=on:fs=off:random_seed=3433841043:i=360:av=off:fsr=off:rtra=on_2812 on theBenchmark for (2812ds/360Mi) % 206.17/29.30 % (2915996)Instruction limit reached! % 206.17/29.30 % (2915996)------------------------------ % 206.17/29.30 % (2915996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.17/29.30 % (2915996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.17/29.30 % (2915996)CaDiCaL version: 2.1.3 % 206.17/29.30 % (2915996)Termination reason: Instruction limit % 206.17/29.30 % (2915996)Termination phase: Saturation % 206.17/29.30 % (2915996)Time elapsed: 0.160 s % 206.17/29.30 % (2915996)Peak memory usage: 13 MB % 206.17/29.30 % (2915996)Instructions burned: 360 (million) % 206.17/29.30 % (2915998)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1824154453:i=954:bd=all:rtra=on_2810 on theBenchmark for (2810ds/954Mi) % 206.17/29.30 % (2915998)Instruction limit reached! % 206.17/29.30 % (2915998)------------------------------ % 206.17/29.30 % (2915998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.17/29.30 % (2915998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.17/29.30 % (2915998)CaDiCaL version: 2.1.3 % 206.17/29.30 % (2915998)Termination reason: Instruction limit % 206.17/29.30 % (2915998)Termination phase: Saturation % 206.17/29.30 % (2915998)Time elapsed: 0.598 s % 206.17/29.30 % (2915998)Peak memory usage: 16 MB % 206.17/29.30 % (2915998)Instructions burned: 955 (million) % 206.17/29.30 % (2916000)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3944296955:fmbsr=1.3:i=1730:ins=25:rtra=on_2804 on theBenchmark for (2804ds/1730Mi) % 206.17/29.30 % (2916000)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 206.17/29.30 % (2916000)Terminated due to inappropriate strategy. % 206.17/29.30 % (2916000)------------------------------ % 206.17/29.30 % (2916000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.17/29.30 % (2916000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.17/29.30 % (2916000)CaDiCaL version: 2.1.3 % 206.17/29.30 % (2916000)Termination reason: Inappropriate % 206.17/29.30 % (2916000)Time elapsed: 0.001 s % 206.17/29.30 % (2916000)Peak memory usage: 10 MB % 206.17/29.30 % (2916000)------------------------------ % 206.17/29.30 % (2916000)------------------------------ % 206.17/29.30 % (2916002)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=740277589:i=2358:rtra=on_2803 on theBenchmark for (2803ds/2358Mi) % 206.17/29.30 % (2916002)Instruction limit reached! % 206.17/29.30 % (2916002)------------------------------ % 206.17/29.30 % (2916002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.17/29.30 % (2916002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.17/29.30 % (2916002)CaDiCaL version: 2.1.3 % 206.17/29.30 % (2916002)Termination reason: Instruction limit % 206.17/29.30 % (2916002)Termination phase: Saturation % 206.17/29.30 % (2916002)Time elapsed: 1.559 s % 272.99/38.79 % (2916002)Peak memory usage: 27 MB % 272.99/38.79 % (2916002)Instructions burned: 2359 (million) % 272.99/38.79 % (2916004)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4034901697:i=1778:ins=1:rtra=on_2788 on theBenchmark for (2788ds/1778Mi) % 272.99/38.79 % (2916004)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.99/38.79 % (2916004)Terminated due to inappropriate strategy. % 272.99/38.79 % (2916004)------------------------------ % 272.99/38.79 % (2916004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.99/38.79 % (2916004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.99/38.79 % (2916004)CaDiCaL version: 2.1.3 % 272.99/38.79 % (2916004)Termination reason: Inappropriate % 272.99/38.79 % (2916004)Time elapsed: 0.001 s % 272.99/38.79 % (2916004)Peak memory usage: 10 MB % 272.99/38.79 % (2916004)------------------------------ % 272.99/38.79 % (2916004)------------------------------ % 272.99/38.79 % (2916006)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=1669696163:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2787 on theBenchmark for (2787ds/1384Mi) % 272.99/38.79 % (2916006)Instruction limit reached! % 272.99/38.79 % (2916006)------------------------------ % 272.99/38.79 % (2916006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.99/38.79 % (2916006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.99/38.79 % (2916006)CaDiCaL version: 2.1.3 % 272.99/38.79 % (2916006)Termination reason: Instruction limit % 272.99/38.79 % (2916006)Termination phase: Saturation % 272.99/38.79 % (2916006)Time elapsed: 0.792 s % 272.99/38.79 % (2916006)Peak memory usage: 23 MB % 272.99/38.79 % (2916006)Instructions burned: 1385 (million) % 272.99/38.79 % (2916008)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2262732826:i=1758:kws=inv_precedence:fsr=off:rtra=on_2779 on theBenchmark for (2779ds/1758Mi) % 272.99/38.79 % (2916008)Instruction limit reached! % 272.99/38.79 % (2916008)------------------------------ % 272.99/38.79 % (2916008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.99/38.79 % (2916008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.99/38.79 % (2916008)CaDiCaL version: 2.1.3 % 272.99/38.79 % (2916008)Termination reason: Instruction limit % 272.99/38.79 % (2916008)Termination phase: Saturation % 272.99/38.79 % (2916008)Time elapsed: 0.999 s % 272.99/38.79 % (2916008)Peak memory usage: 26 MB % 272.99/38.79 % (2916008)Instructions burned: 1758 (million) % 272.99/38.79 % (2916010)fmb+10_1_sil=64000:si=on:random_seed=1235805779:i=44122:nm=2:rtra=on:gsp=on_2769 on theBenchmark for (2769ds/44122Mi) % 272.99/38.79 % (2916010)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.99/38.79 % (2916010)Terminated due to inappropriate strategy. % 272.99/38.79 % (2916010)------------------------------ % 272.99/38.79 % (2916010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.99/38.79 % (2916010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.99/38.79 % (2916010)CaDiCaL version: 2.1.3 % 272.99/38.79 % (2916010)Termination reason: Inappropriate % 272.99/38.79 % (2916010)Time elapsed: 0.001 s % 272.99/38.79 % (2916010)Peak memory usage: 10 MB % 272.99/38.79 % (2916010)Instructions burned: 1 (million) % 272.99/38.79 % (2916010)------------------------------ % 272.99/38.79 % (2916010)------------------------------ % 272.99/38.79 % (2916012)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3667189282:i=19030:nm=5:rtra=on_2769 on theBenchmark for (2769ds/19030Mi) % 272.99/38.79 % (2916012)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.99/38.79 % (2916012)Terminated due to inappropriate strategy. % 272.99/38.79 % (2916012)------------------------------ % 272.99/38.79 % (2916012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.99/38.79 % (2916012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.99/38.79 % (2916012)CaDiCaL version: 2.1.3 % 272.99/38.79 % (2916012)Termination reason: Inappropriate % 272.99/38.79 % (2916012)Time elapsed: 0.001 s % 272.99/38.79 % (2916012)Peak memory usage: 10 MB % 272.99/38.79 % (2916012)------------------------------ % 272.99/38.79 % (2916012)------------------------------ % 272.99/38.79 % (2916014)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1315565529:fmbsr=1.7:i=1840:rtra=on_2769 on theBenchmark for (2769ds/1840Mi) % 272.99/38.79 % (2916014)WARNING: trying to run FTerminated % 300.67/42.64 % Vampire exiting %------------------------------------------------------------------------------