%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW844_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n001.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:03 PM UTC 2026 % Result : Timeout 300.49s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW844_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.19 % Computer : n001.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.20 % CPULimit : 300 % 0.07/0.20 % WCLimit : 300 % 0.07/0.20 % DateTime : Mon Sep 28 14:37:33 UTC 2026 % 0.07/0.20 % CPUTime : % 0.07/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.23 Running first-order model finding % 0.07/0.23 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 % 4.36/0.91 % (394755)Will run a generic schedule for satisfiability detection. % 4.36/0.91 % (394762)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3558331997:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 4.36/0.91 % (394761)% WARNING: option uhcvi not known. % 4.36/0.91 % (394760)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=732519467_2999 on theBenchmark for (2999ds/0Mi) % 4.36/0.91 % (394761)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2577810147:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 4.36/0.91 % (394763)dis+10_1_sil=32000:sp=arity:random_seed=4209153461:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 4.36/0.91 % (394764)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3189168595:i=116_2999 on theBenchmark for (2999ds/116Mi) % 4.36/0.91 % (394765)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1571649206:i=131_2999 on theBenchmark for (2999ds/131Mi) % 4.36/0.91 % (394766)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=543219290:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 4.36/0.91 % (394760)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.36/0.91 % (394760)Terminated due to inappropriate strategy. % 4.36/0.91 % (394760)------------------------------ % 4.36/0.91 % (394760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.36/0.91 % (394760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.36/0.91 % (394760)CaDiCaL version: 2.1.3 % 4.36/0.91 % (394760)Termination reason: Inappropriate % 4.36/0.91 % (394760)Time elapsed: 0.029 s % 4.36/0.91 % (394760)Peak memory usage: 12 MB % 4.36/0.91 % (394760)Instructions burned: 65 (million) % 4.36/0.91 % (394760)------------------------------ % 4.36/0.91 % (394760)------------------------------ % 4.36/0.91 % (394774)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3505148566:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 4.36/0.91 % (394763)Instruction limit reached! % 4.36/0.91 % (394763)------------------------------ % 4.36/0.91 % (394763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.36/0.91 % (394763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.36/0.91 % (394763)CaDiCaL version: 2.1.3 % 4.36/0.91 % (394763)Termination reason: Instruction limit % 4.36/0.91 % (394763)Termination phase: Saturation % 4.36/0.91 % (394763)Time elapsed: 0.052 s % 4.36/0.91 % (394763)Peak memory usage: 13 MB % 4.36/0.91 % (394763)Instructions burned: 103 (million) % 4.36/0.91 % (394764)Instruction limit reached! % 4.36/0.91 % (394764)------------------------------ % 4.36/0.91 % (394764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.36/0.91 % (394764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.36/0.91 % (394764)CaDiCaL version: 2.1.3 % 4.36/0.91 % (394764)Termination reason: Instruction limit % 4.36/0.91 % (394764)Termination phase: Saturation % 4.36/0.91 % (394764)Time elapsed: 0.060 s % 4.36/0.91 % (394764)Peak memory usage: 14 MB % 4.36/0.91 % (394764)Instructions burned: 117 (million) % 4.36/0.91 % (394765)Instruction limit reached! % 4.36/0.91 % (394765)------------------------------ % 4.36/0.91 % (394765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.36/0.92 % (394765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.36/0.92 % (394765)CaDiCaL version: 2.1.3 % 4.36/0.92 % (394765)Termination reason: Instruction limit % 4.36/0.92 % (394765)Termination phase: Saturation % 4.36/0.92 % (394765)Time elapsed: 0.067 s % 4.36/0.92 % (394765)Peak memory usage: 14 MB % 4.36/0.92 % (394765)Instructions burned: 131 (million) % 4.36/0.92 % (394776)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1150003384:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 4.36/0.92 % (394777)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=1297611425:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 4.36/0.92 % (394774)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.36/0.92 % (394774)Terminated due to inappropriate strategy. % 4.36/0.92 % (394774)------------------------------ % 4.36/0.92 % (394774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.36/0.92 % (394774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.50 % (394774)CaDiCaL version: 2.1.3 % 7.98/1.50 % (394774)Termination reason: Inappropriate % 7.98/1.50 % (394774)Time elapsed: 0.030 s % 7.98/1.50 % (394774)Peak memory usage: 12 MB % 7.98/1.50 % (394774)Instructions burned: 64 (million) % 7.98/1.50 % (394774)------------------------------ % 7.98/1.50 % (394774)------------------------------ % 7.98/1.50 % (394778)ott-21_1_sil=16000:fs=off:random_seed=2611140343:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.98/1.50 % (394766)Instruction limit reached! % 7.98/1.50 % (394766)------------------------------ % 7.98/1.50 % (394766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.98/1.50 % (394766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.50 % (394766)CaDiCaL version: 2.1.3 % 7.98/1.50 % (394766)Termination reason: Instruction limit % 7.98/1.50 % (394766)Termination phase: Saturation % 7.98/1.50 % (394766)Time elapsed: 0.091 s % 7.98/1.50 % (394766)Peak memory usage: 14 MB % 7.98/1.50 % (394766)Instructions burned: 159 (million) % 7.98/1.50 % (394781)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3437692705:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.98/1.50 % (394783)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1409643397:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.98/1.50 % (394783)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.98/1.50 % (394783)Terminated due to inappropriate strategy. % 7.98/1.50 % (394783)------------------------------ % 7.98/1.50 % (394783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.98/1.50 % (394783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.50 % (394783)CaDiCaL version: 2.1.3 % 7.98/1.50 % (394783)Termination reason: Inappropriate % 7.98/1.50 % (394783)Time elapsed: 0.029 s % 7.98/1.50 % (394783)Peak memory usage: 12 MB % 7.98/1.50 % (394783)Instructions burned: 64 (million) % 7.98/1.50 % (394783)------------------------------ % 7.98/1.50 % (394783)------------------------------ % 7.98/1.50 % (394776)Instruction limit reached! % 7.98/1.50 % (394776)------------------------------ % 7.98/1.50 % (394776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.98/1.50 % (394776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.50 % (394776)CaDiCaL version: 2.1.3 % 7.98/1.50 % (394776)Termination reason: Instruction limit % 7.98/1.50 % (394776)Termination phase: Saturation % 7.98/1.50 % (394776)Time elapsed: 0.071 s % 7.98/1.50 % (394776)Peak memory usage: 14 MB % 7.98/1.50 % (394776)Instructions burned: 132 (million) % 7.98/1.50 % (394786)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=86744498:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 7.98/1.50 % (394787)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2200528211:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 7.98/1.50 % (394778)Instruction limit reached! % 7.98/1.50 % (394778)------------------------------ % 7.98/1.50 % (394778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.98/1.50 % (394778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.50 % (394778)CaDiCaL version: 2.1.3 % 7.98/1.50 % (394778)Termination reason: Instruction limit % 7.98/1.50 % (394778)Termination phase: Saturation % 7.98/1.50 % (394778)Time elapsed: 0.084 s % 7.98/1.50 % (394778)Peak memory usage: 14 MB % 7.98/1.50 % (394778)Instructions burned: 182 (million) % 7.98/1.50 % (394790)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=1918277739:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 7.98/1.50 % (394787)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.98/1.50 % (394787)Terminated due to inappropriate strategy. % 7.98/1.50 % (394787)------------------------------ % 7.98/1.50 % (394787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.98/1.50 % (394787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.50 % (394787)CaDiCaL version: 2.1.3 % 7.98/1.50 % (394787)Termination reason: Inappropriate % 7.98/1.50 % (394787)Time elapsed: 0.029 s % 7.98/1.50 % (394787)Peak memory usage: 12 MB % 7.98/1.50 % (394787)Instructions burned: 64 (million) % 7.98/1.50 % (394787)------------------------------ % 7.98/1.50 % (394787)------------------------------ % 22.56/3.54 % (394792)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2366573013:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.56/3.54 % (394781)Instruction limit reached! % 22.56/3.54 % (394781)------------------------------ % 22.56/3.54 % (394781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.56/3.54 % (394781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.56/3.54 % (394781)CaDiCaL version: 2.1.3 % 22.56/3.54 % (394781)Termination reason: Instruction limit % 22.56/3.54 % (394781)Termination phase: Saturation % 22.56/3.54 % (394781)Time elapsed: 0.278 s % 22.56/3.54 % (394781)Peak memory usage: 16 MB % 22.56/3.54 % (394781)Instructions burned: 478 (million) % 22.56/3.54 % (394794)fmb+10_1_sil=64000:random_seed=150718003:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 22.56/3.54 % (394794)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.56/3.54 % (394794)Terminated due to inappropriate strategy. % 22.56/3.54 % (394794)------------------------------ % 22.56/3.54 % (394794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.56/3.54 % (394794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.56/3.54 % (394794)CaDiCaL version: 2.1.3 % 22.56/3.54 % (394794)Termination reason: Inappropriate % 22.56/3.54 % (394794)Time elapsed: 0.029 s % 22.56/3.54 % (394794)Peak memory usage: 12 MB % 22.56/3.54 % (394794)Instructions burned: 65 (million) % 22.56/3.54 % (394794)------------------------------ % 22.56/3.54 % (394794)------------------------------ % 22.56/3.54 % (394796)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3708327190:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 22.56/3.54 % (394777)Instruction limit reached! % 22.56/3.54 % (394777)------------------------------ % 22.56/3.54 % (394777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.56/3.54 % (394777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.56/3.54 % (394777)CaDiCaL version: 2.1.3 % 22.56/3.54 % (394777)Termination reason: Instruction limit % 22.56/3.54 % (394777)Termination phase: Saturation % 22.56/3.54 % (394777)Time elapsed: 0.384 s % 22.56/3.54 % (394777)Peak memory usage: 17 MB % 22.56/3.54 % (394777)Instructions burned: 684 (million) % 22.56/3.54 % (394796)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.56/3.54 % (394796)Terminated due to inappropriate strategy. % 22.56/3.54 % (394796)------------------------------ % 22.56/3.54 % (394796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.56/3.54 % (394796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.56/3.54 % (394796)CaDiCaL version: 2.1.3 % 22.56/3.54 % (394796)Termination reason: Inappropriate % 22.56/3.54 % (394796)Time elapsed: 0.029 s % 22.56/3.54 % (394796)Peak memory usage: 12 MB % 22.56/3.54 % (394796)Instructions burned: 64 (million) % 22.56/3.54 % (394798)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=193763220:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 22.56/3.54 % (394796)------------------------------ % 22.56/3.54 % (394796)------------------------------ % 22.56/3.54 % (394800)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=168513294:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 22.56/3.54 % (394798)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.56/3.54 % (394798)Terminated due to inappropriate strategy. % 22.56/3.54 % (394798)------------------------------ % 22.56/3.54 % (394798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.56/3.54 % (394798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.56/3.54 % (394798)CaDiCaL version: 2.1.3 % 22.56/3.54 % (394798)Termination reason: Inappropriate % 22.56/3.54 % (394798)Time elapsed: 0.029 s % 22.56/3.54 % (394798)Peak memory usage: 12 MB % 22.56/3.54 % (394798)Instructions burned: 64 (million) % 22.56/3.54 % (394798)------------------------------ % 22.56/3.54 % (394798)------------------------------ % 22.56/3.54 % (394802)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2314212122:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 22.56/3.54 % (394790)Instruction limit reached! % 22.56/3.54 % (394790)------------------------------ % 22.56/3.54 % (394790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.56/3.54 % (394790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.40/4.81 % (394790)CaDiCaL version: 2.1.3 % 31.40/4.81 % (394790)Termination reason: Instruction limit % 31.40/4.81 % (394790)Termination phase: Saturation % 31.40/4.81 % (394790)Time elapsed: 0.424 s % 31.40/4.81 % (394790)Peak memory usage: 19 MB % 31.40/4.81 % (394790)Instructions burned: 693 (million) % 31.40/4.81 % (394804)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3408016545:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 31.40/4.81 % (394804)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.40/4.81 % (394804)Terminated due to inappropriate strategy. % 31.40/4.81 % (394804)------------------------------ % 31.40/4.81 % (394804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.40/4.81 % (394804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.40/4.81 % (394804)CaDiCaL version: 2.1.3 % 31.40/4.81 % (394804)Termination reason: Inappropriate % 31.40/4.81 % (394804)Time elapsed: 0.029 s % 31.40/4.81 % (394804)Peak memory usage: 12 MB % 31.40/4.81 % (394804)Instructions burned: 65 (million) % 31.40/4.81 % (394804)------------------------------ % 31.40/4.81 % (394804)------------------------------ % 31.40/4.81 % (394806)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3186196498:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi) % 31.40/4.81 % (394792)Instruction limit reached! % 31.40/4.81 % (394792)------------------------------ % 31.40/4.81 % (394792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.40/4.81 % (394792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.40/4.81 % (394792)CaDiCaL version: 2.1.3 % 31.40/4.81 % (394792)Termination reason: Instruction limit % 31.40/4.81 % (394792)Termination phase: Saturation % 31.40/4.81 % (394792)Time elapsed: 0.480 s % 31.40/4.81 % (394792)Peak memory usage: 19 MB % 31.40/4.81 % (394792)Instructions burned: 880 (million) % 31.40/4.81 % (394808)ott-2_1_sil=16000:newcnf=on:random_seed=676206789:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 31.40/4.81 % (394806)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.40/4.81 % (394806)Terminated due to inappropriate strategy. % 31.40/4.81 % (394806)------------------------------ % 31.40/4.81 % (394806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.40/4.81 % (394806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.40/4.81 % (394806)CaDiCaL version: 2.1.3 % 31.40/4.81 % (394806)Termination reason: Inappropriate % 31.40/4.81 % (394806)Time elapsed: 0.029 s % 31.40/4.81 % (394806)Peak memory usage: 12 MB % 31.40/4.81 % (394806)Instructions burned: 64 (million) % 31.40/4.81 % (394806)------------------------------ % 31.40/4.81 % (394806)------------------------------ % 31.40/4.81 % (394810)ott+10_1_sil=32000:tgt=ground:random_seed=1061217818:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 31.40/4.81 % (394786)Instruction limit reached! % 31.40/4.81 % (394786)------------------------------ % 31.40/4.81 % (394786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.40/4.81 % (394786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.40/4.81 % (394786)CaDiCaL version: 2.1.3 % 31.40/4.81 % (394786)Termination reason: Instruction limit % 31.40/4.81 % (394786)Termination phase: Saturation % 31.40/4.81 % (394786)Time elapsed: 0.656 s % 31.40/4.81 % (394786)Peak memory usage: 24 MB % 31.40/4.81 % (394786)Instructions burned: 1180 (million) % 31.40/4.81 % (394812)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1480778505:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 31.40/4.81 % (394812)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.40/4.81 % (394812)Terminated due to inappropriate strategy. % 31.40/4.81 % (394812)------------------------------ % 31.40/4.81 % (394812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.40/4.81 % (394812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.40/4.81 % (394812)CaDiCaL version: 2.1.3 % 31.40/4.81 % (394812)Termination reason: Inappropriate % 31.40/4.81 % (394812)Time elapsed: 0.029 s % 31.40/4.81 % (394812)Peak memory usage: 12 MB % 31.40/4.81 % (394812)Instructions burned: 65 (million) % 31.40/4.81 % (394812)------------------------------ % 31.40/4.81 % (394812)------------------------------ % 31.40/4.81 % (394814)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=613899602:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 31.40/4.81 % (394808)Instruction limit reached! % 108.14/15.55 % (394808)------------------------------ % 108.14/15.55 % (394808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.14/15.55 % (394808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.14/15.55 % (394808)CaDiCaL version: 2.1.3 % 108.14/15.55 % (394808)Termination reason: Instruction limit % 108.14/15.55 % (394808)Termination phase: Saturation % 108.14/15.55 % (394808)Time elapsed: 0.486 s % 108.14/15.55 % (394808)Peak memory usage: 20 MB % 108.14/15.55 % (394808)Instructions burned: 871 (million) % 108.14/15.55 % (394816)dis+21_1_sil=32000:sas=cadical:random_seed=971168011:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 108.14/15.55 % (394802)Instruction limit reached! % 108.14/15.55 % (394802)------------------------------ % 108.14/15.55 % (394802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.14/15.55 % (394802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.14/15.55 % (394802)CaDiCaL version: 2.1.3 % 108.14/15.55 % (394802)Termination reason: Instruction limit % 108.14/15.55 % (394802)Termination phase: Saturation % 108.14/15.55 % (394802)Time elapsed: 0.792 s % 108.14/15.55 % (394802)Peak memory usage: 32 MB % 108.14/15.55 % (394802)Instructions burned: 1472 (million) % 108.14/15.55 % (394818)ott+11_1_sil=16000:gs=on:random_seed=3610263886:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 108.14/15.55 % (394818)Instruction limit reached! % 108.14/15.55 % (394818)------------------------------ % 108.14/15.55 % (394818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.14/15.55 % (394818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.14/15.55 % (394818)CaDiCaL version: 2.1.3 % 108.14/15.55 % (394818)Termination reason: Instruction limit % 108.14/15.55 % (394818)Termination phase: Saturation % 108.14/15.55 % (394818)Time elapsed: 1.270 s % 108.14/15.55 % (394818)Peak memory usage: 31 MB % 108.14/15.55 % (394818)Instructions burned: 2253 (million) % 108.14/15.55 % (394820)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2477522171:fmbsr=1.6:i=67534_2973 on theBenchmark for (2973ds/67534Mi) % 108.14/15.55 % (394820)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 108.14/15.55 % (394820)Terminated due to inappropriate strategy. % 108.14/15.55 % (394820)------------------------------ % 108.14/15.55 % (394820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.14/15.55 % (394820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.14/15.55 % (394820)CaDiCaL version: 2.1.3 % 108.14/15.55 % (394820)Termination reason: Inappropriate % 108.14/15.55 % (394820)Time elapsed: 0.029 s % 108.14/15.55 % (394820)Peak memory usage: 12 MB % 108.14/15.55 % (394820)Instructions burned: 64 (million) % 108.14/15.55 % (394820)------------------------------ % 108.14/15.55 % (394820)------------------------------ % 108.14/15.55 % (394822)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4229570033:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2972 on theBenchmark for (2972ds/4591Mi) % 108.14/15.55 % (394814)Instruction limit reached! % 108.14/15.55 % (394814)------------------------------ % 108.14/15.55 % (394814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.14/15.55 % (394814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.14/15.55 % (394814)CaDiCaL version: 2.1.3 % 108.14/15.55 % (394814)Termination reason: Instruction limit % 108.14/15.55 % (394814)Termination phase: Saturation % 108.14/15.55 % (394814)Time elapsed: 1.878 s % 108.14/15.55 % (394814)Peak memory usage: 38 MB % 108.14/15.55 % (394814)Instructions burned: 3513 (million) % 108.14/15.55 % (394824)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=308183499:i=29340_2971 on theBenchmark for (2971ds/29340Mi) % 108.14/15.55 % (394800)Instruction limit reached! % 108.14/15.55 % (394800)------------------------------ % 108.14/15.55 % (394800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.14/15.55 % (394800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.14/15.55 % (394800)CaDiCaL version: 2.1.3 % 108.14/15.55 % (394800)Termination reason: Instruction limit % 108.14/15.55 % (394800)Termination phase: Saturation % 108.14/15.55 % (394800)Time elapsed: 2.720 s % 108.14/15.55 % (394800)Peak memory usage: 48 MB % 108.14/15.55 % (394800)Instructions burned: 5132 (million) % 108.14/15.55 % (394816)Instruction limit reached! % 108.14/15.55 % (394816)------------------------------ % 108.14/15.55 % (394816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.08/18.08 % (394816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.08/18.08 % (394816)CaDiCaL version: 2.1.3 % 126.08/18.08 % (394816)Termination reason: Instruction limit % 126.08/18.08 % (394816)Termination phase: Saturation % 126.08/18.08 % (394816)Time elapsed: 2.018 s % 126.08/18.08 % (394816)Peak memory usage: 40 MB % 126.08/18.08 % (394816)Instructions burned: 3773 (million) % 126.08/18.08 % (394826)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2009957783:i=5211_2967 on theBenchmark for (2967ds/5211Mi) % 126.08/18.08 % (394827)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=321157499:i=5497:nm=2_2966 on theBenchmark for (2966ds/5497Mi) % 126.08/18.08 % (394827)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.08/18.08 % (394827)Terminated due to inappropriate strategy. % 126.08/18.08 % (394827)------------------------------ % 126.08/18.08 % (394827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.08/18.08 % (394827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.08/18.08 % (394827)CaDiCaL version: 2.1.3 % 126.08/18.08 % (394827)Termination reason: Inappropriate % 126.08/18.08 % (394827)Time elapsed: 0.029 s % 126.08/18.08 % (394827)Peak memory usage: 12 MB % 126.08/18.08 % (394827)Instructions burned: 65 (million) % 126.08/18.08 % (394827)------------------------------ % 126.08/18.08 % (394827)------------------------------ % 126.08/18.08 % (394830)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1293928861:fmbsr=2:i=46332_2966 on theBenchmark for (2966ds/46332Mi) % 126.08/18.08 % (394830)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.08/18.08 % (394830)Terminated due to inappropriate strategy. % 126.08/18.08 % (394830)------------------------------ % 126.08/18.08 % (394830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.08/18.08 % (394830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.08/18.08 % (394830)CaDiCaL version: 2.1.3 % 126.08/18.08 % (394830)Termination reason: Inappropriate % 126.08/18.08 % (394830)Time elapsed: 0.029 s % 126.08/18.08 % (394830)Peak memory usage: 12 MB % 126.08/18.08 % (394830)Instructions burned: 64 (million) % 126.08/18.08 % (394830)------------------------------ % 126.08/18.08 % (394830)------------------------------ % 126.08/18.08 % (394832)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=637389525:i=14071_2965 on theBenchmark for (2965ds/14071Mi) % 126.08/18.08 % (394832)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.08/18.08 % (394832)Terminated due to inappropriate strategy. % 126.08/18.08 % (394832)------------------------------ % 126.08/18.08 % (394832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.08/18.08 % (394832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.08/18.08 % (394832)CaDiCaL version: 2.1.3 % 126.08/18.08 % (394832)Termination reason: Inappropriate % 126.08/18.08 % (394832)Time elapsed: 0.029 s % 126.08/18.08 % (394832)Peak memory usage: 12 MB % 126.08/18.08 % (394832)Instructions burned: 64 (million) % 126.08/18.08 % (394832)------------------------------ % 126.08/18.08 % (394832)------------------------------ % 126.08/18.08 % (394834)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2228574594:i=22565:add=on:rawr=on_2965 on theBenchmark for (2965ds/22565Mi) % 126.08/18.08 % (394810)Instruction limit reached! % 126.08/18.08 % (394810)------------------------------ % 126.08/18.08 % (394810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.08/18.08 % (394810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.08/18.08 % (394810)CaDiCaL version: 2.1.3 % 126.08/18.08 % (394810)Termination reason: Instruction limit % 126.08/18.08 % (394810)Termination phase: Saturation % 126.08/18.08 % (394810)Time elapsed: 2.969 s % 126.08/18.08 % (394810)Peak memory usage: 55 MB % 126.08/18.08 % (394810)Instructions burned: 5114 (million) % 126.08/18.08 % (394836)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2090387866:i=8173:av=off_2962 on theBenchmark for (2962ds/8173Mi) % 126.08/18.08 % (394822)Instruction limit reached! % 126.08/18.08 % (394822)------------------------------ % 126.08/18.08 % (394822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.08/18.08 % (394822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.08/18.08 % (394822)CaDiCaL version: 2.1.3 % 126.08/18.08 % (394822)Termination reason: Instruction limit % 126.08/18.08 % (394822)Termination phase: Saturation % 138.68/19.83 % (394822)Time elapsed: 1.817 s % 138.68/19.83 % (394822)Peak memory usage: 33 MB % 138.68/19.83 % (394822)Instructions burned: 4593 (million) % 138.68/19.83 % (394840)dis+10_16:1_sil=16000:random_seed=1163154445:i=9155:fsr=off_2954 on theBenchmark for (2954ds/9155Mi) % 138.68/19.83 % (394826)Instruction limit reached! % 138.68/19.83 % (394826)------------------------------ % 138.68/19.83 % (394826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.68/19.83 % (394826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.68/19.83 % (394826)CaDiCaL version: 2.1.3 % 138.68/19.83 % (394826)Termination reason: Instruction limit % 138.68/19.83 % (394826)Termination phase: Saturation % 138.68/19.83 % (394826)Time elapsed: 2.831 s % 138.68/19.83 % (394826)Peak memory usage: 49 MB % 138.68/19.83 % (394826)Instructions burned: 5212 (million) % 138.68/19.83 % (394842)ott-3_8_sil=64000:random_seed=3766256102:i=20139:bs=on_2938 on theBenchmark for (2938ds/20139Mi) % 138.68/19.83 % (394836)Instruction limit reached! % 138.68/19.83 % (394836)------------------------------ % 138.68/19.83 % (394836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.68/19.83 % (394836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.68/19.83 % (394836)CaDiCaL version: 2.1.3 % 138.68/19.83 % (394836)Termination reason: Instruction limit % 138.68/19.83 % (394836)Termination phase: Saturation % 138.68/19.83 % (394836)Time elapsed: 4.738 s % 138.68/19.83 % (394836)Peak memory usage: 79 MB % 138.68/19.83 % (394836)Instructions burned: 8173 (million) % 138.68/19.83 % (394844)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=895919635:fmbsr=2:i=32576_2914 on theBenchmark for (2914ds/32576Mi) % 138.68/19.83 % (394844)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 138.68/19.83 % (394844)Terminated due to inappropriate strategy. % 138.68/19.83 % (394844)------------------------------ % 138.68/19.83 % (394844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.68/19.83 % (394844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.68/19.83 % (394844)CaDiCaL version: 2.1.3 % 138.68/19.83 % (394844)Termination reason: Inappropriate % 138.68/19.83 % (394844)Time elapsed: 0.029 s % 138.68/19.83 % (394844)Peak memory usage: 12 MB % 138.68/19.83 % (394844)Instructions burned: 65 (million) % 138.68/19.83 % (394844)------------------------------ % 138.68/19.83 % (394844)------------------------------ % 138.68/19.83 % (394846)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1867725064:i=11404_2914 on theBenchmark for (2914ds/11404Mi) % 138.68/19.83 % (394840)Instruction limit reached! % 138.68/19.83 % (394840)------------------------------ % 138.68/19.83 % (394840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.68/19.83 % (394840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.68/19.83 % (394840)CaDiCaL version: 2.1.3 % 138.68/19.83 % (394840)Termination reason: Instruction limit % 138.68/19.83 % (394840)Termination phase: Saturation % 138.68/19.83 % (394840)Time elapsed: 4.734 s % 138.68/19.83 % (394840)Peak memory usage: 59 MB % 138.68/19.83 % (394840)Instructions burned: 9155 (million) % 138.68/19.83 % (394848)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3695522370:i=14134_2906 on theBenchmark for (2906ds/14134Mi) % 138.68/19.83 % (394834)Instruction limit reached! % 138.68/19.83 % (394834)------------------------------ % 138.68/19.83 % (394834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.68/19.83 % (394834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.68/19.83 % (394834)CaDiCaL version: 2.1.3 % 138.68/19.83 % (394834)Termination reason: Instruction limit % 138.68/19.83 % (394834)Termination phase: Saturation % 138.68/19.83 % (394834)Time elapsed: 9.579 s % 138.68/19.83 % (394834)Peak memory usage: 71 MB % 138.68/19.83 % (394834)Instructions burned: 22565 (million) % 138.68/19.83 % (394850)dis+33_16_sil=32000:sac=on:random_seed=2295695219:i=15851:nm=0_2869 on theBenchmark for (2869ds/15851Mi) % 138.68/19.83 % (394846)Instruction limit reached! % 138.68/19.83 % (394846)------------------------------ % 138.68/19.83 % (394846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.68/19.83 % (394846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.68/19.83 % (394846)CaDiCaL version: 2.1.3 % 138.68/19.83 % (394846)Termination reason: Instruction limit % 138.68/19.83 % (394846)Termination phase: Saturation % 138.68/19.83 % (394846)Time elapsed: 6.662 s % 138.68/19.83 % (394846)Peak memory usage: 95 MB % 138.68/19.83 % (394846)Instructions burned: 11405 (million) % 138.68/19.83 % (394914)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4231644013:avsq=on:i=17627:add=on:amm=off_2847 on theBenchmark for (2847ds/17627Mi) % 145.72/20.80 % (394824)Instruction limit reached! % 145.72/20.80 % (394824)------------------------------ % 145.72/20.80 % (394824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.72/20.80 % (394824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.72/20.80 % (394824)CaDiCaL version: 2.1.3 % 145.72/20.80 % (394824)Termination reason: Instruction limit % 145.72/20.80 % (394824)Termination phase: Saturation % 145.72/20.80 % (394824)Time elapsed: 12.695 s % 145.72/20.80 % (394824)Peak memory usage: 36 MB % 145.72/20.80 % (394824)Instructions burned: 29341 (million) % 145.72/20.80 % (394842)Instruction limit reached! % 145.72/20.80 % (394842)------------------------------ % 145.72/20.80 % (394842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.72/20.80 % (394842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.72/20.80 % (394842)CaDiCaL version: 2.1.3 % 145.72/20.80 % (394842)Termination reason: Instruction limit % 145.72/20.80 % (394842)Termination phase: Saturation % 145.72/20.80 % (394842)Time elapsed: 9.387 s % 145.72/20.81 % (394842)Peak memory usage: 79 MB % 145.72/20.81 % (394842)Instructions burned: 20140 (million) % 145.72/20.81 % (394916)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3290747335:s2a=on:i=53295_2844 on theBenchmark for (2844ds/53295Mi) % 145.72/20.81 % (394917)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1388397003:i=26857:ins=20_2844 on theBenchmark for (2844ds/26857Mi) % 145.72/20.81 % (394917)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 145.72/20.81 % (394917)Terminated due to inappropriate strategy. % 145.72/20.81 % (394917)------------------------------ % 145.72/20.81 % (394917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.72/20.81 % (394917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.72/20.81 % (394917)CaDiCaL version: 2.1.3 % 145.72/20.81 % (394917)Termination reason: Inappropriate % 145.72/20.81 % (394917)Time elapsed: 0.029 s % 145.72/20.81 % (394917)Peak memory usage: 12 MB % 145.72/20.81 % (394917)Instructions burned: 65 (million) % 145.72/20.81 % (394917)------------------------------ % 145.72/20.81 % (394917)------------------------------ % 145.72/20.81 % (394920)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4123328313:i=28120:bs=on:fsr=off_2843 on theBenchmark for (2843ds/28120Mi) % 145.72/20.81 % (394848)Instruction limit reached! % 145.72/20.81 % (394848)------------------------------ % 145.72/20.81 % (394848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.72/20.81 % (394848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.72/20.81 % (394848)CaDiCaL version: 2.1.3 % 145.72/20.81 % (394848)Termination reason: Instruction limit % 145.72/20.81 % (394848)Termination phase: Saturation % 145.72/20.81 % (394848)Time elapsed: 8.366 s % 145.72/20.81 % (394848)Peak memory usage: 106 MB % 145.72/20.81 % (394848)Instructions burned: 14135 (million) % 145.72/20.81 % (394922)fmb+10_1_sil=256000:fmbss=7:random_seed=201958268:fmbsr=1.6:i=182295_2822 on theBenchmark for (2822ds/182295Mi) % 145.72/20.81 % (394922)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 145.72/20.81 % (394922)Terminated due to inappropriate strategy. % 145.72/20.81 % (394922)------------------------------ % 145.72/20.81 % (394922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.72/20.81 % (394922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.72/20.81 % (394922)CaDiCaL version: 2.1.3 % 145.72/20.81 % (394922)Termination reason: Inappropriate % 145.72/20.81 % (394922)Time elapsed: 0.029 s % 145.72/20.81 % (394922)Peak memory usage: 12 MB % 145.72/20.81 % (394922)Instructions burned: 64 (million) % 145.72/20.81 % (394922)------------------------------ % 145.72/20.81 % (394922)------------------------------ % 145.72/20.81 % (394924)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3706777760:i=44625:gsp=on_2822 on theBenchmark for (2822ds/44625Mi) % 145.72/20.81 % (394924)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 145.72/20.81 % (394924)Terminated due to inappropriate strategy. % 145.72/20.81 % (394924)------------------------------ % 145.72/20.81 % (394924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.72/20.81 % (394924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.72/20.81 % (394924)CaDiCaL version: 2.1.3 % 145.72/20.81 % (394924)Termination reason: Inappropriate % 167.79/23.96 % (394924)Time elapsed: 0.029 s % 167.79/23.96 % (394924)Peak memory usage: 12 MB % 167.79/23.96 % (394924)Instructions burned: 64 (million) % 167.79/23.96 % (394924)------------------------------ % 167.79/23.96 % (394924)------------------------------ % 167.79/23.96 % (394926)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=314841413:i=160505_2821 on theBenchmark for (2821ds/160505Mi) % 167.79/23.96 % (394926)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.79/23.96 % (394926)Terminated due to inappropriate strategy. % 167.79/23.96 % (394926)------------------------------ % 167.79/23.96 % (394926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.79/23.96 % (394926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.79/23.96 % (394926)CaDiCaL version: 2.1.3 % 167.79/23.96 % (394926)Termination reason: Inappropriate % 167.79/23.96 % (394926)Time elapsed: 0.029 s % 167.79/23.96 % (394926)Peak memory usage: 12 MB % 167.79/23.96 % (394926)Instructions burned: 64 (million) % 167.79/23.96 % (394926)------------------------------ % 167.79/23.96 % (394926)------------------------------ % 167.79/23.96 % (394928)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1148132691:fmbsr=1.3:i=225729_2821 on theBenchmark for (2821ds/225729Mi) % 167.79/23.96 % (394928)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.79/23.96 % (394928)Terminated due to inappropriate strategy. % 167.79/23.96 % (394928)------------------------------ % 167.79/23.96 % (394928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.79/23.96 % (394928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.79/23.96 % (394928)CaDiCaL version: 2.1.3 % 167.79/23.96 % (394928)Termination reason: Inappropriate % 167.79/23.96 % (394928)Time elapsed: 0.029 s % 167.79/23.96 % (394928)Peak memory usage: 12 MB % 167.79/23.96 % (394928)Instructions burned: 64 (million) % 167.79/23.96 % (394928)------------------------------ % 167.79/23.96 % (394928)------------------------------ % 167.79/23.96 % (394930)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1379934228:fmbsr=2:i=185024:ins=7_2820 on theBenchmark for (2820ds/185024Mi) % 167.79/23.96 % (394930)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.79/23.96 % (394930)Terminated due to inappropriate strategy. % 167.79/23.96 % (394930)------------------------------ % 167.79/23.96 % (394930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.79/23.96 % (394930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.79/23.96 % (394930)CaDiCaL version: 2.1.3 % 167.79/23.96 % (394930)Termination reason: Inappropriate % 167.79/23.96 % (394930)Time elapsed: 0.029 s % 167.79/23.96 % (394930)Peak memory usage: 12 MB % 167.79/23.96 % (394930)Instructions burned: 65 (million) % 167.79/23.96 % (394930)------------------------------ % 167.79/23.96 % (394930)------------------------------ % 167.79/23.96 % (394932)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2095855932:rtra=on_2820 on theBenchmark for (2820ds/0Mi) % 167.79/23.96 % (394932)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.79/23.96 % (394932)Terminated due to inappropriate strategy. % 167.79/23.96 % (394932)------------------------------ % 167.79/23.96 % (394932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.79/23.96 % (394932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.79/23.96 % (394932)CaDiCaL version: 2.1.3 % 167.79/23.96 % (394932)Termination reason: Inappropriate % 167.79/23.96 % (394932)Time elapsed: 0.034 s % 167.79/23.96 % (394932)Peak memory usage: 12 MB % 167.79/23.96 % (394932)Instructions burned: 70 (million) % 167.79/23.96 % (394932)------------------------------ % 167.79/23.96 % (394932)------------------------------ % 167.79/23.96 % (394934)% WARNING: option uhcvi not known. % 167.79/23.96 % (394934)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4041257221:i=271062:add=off:rtra=on:rawr=on_2819 on theBenchmark for (2819ds/271062Mi) % 167.79/23.96 % (394762)Instruction limit reached! % 167.79/23.96 % (394762)------------------------------ % 167.79/23.96 % (394762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.79/23.96 % (394762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.79/23.96 % (394762)CaDiCaL version: 2.1.3 % 167.79/23.96 % (394762)Termination reason: Instruction limit % 167.79/23.96 % (394762)Termination phase: Saturation % 167.79/23.96 % (394762)Time elapsed: 19.536 s % 167.79/23.96 % (394762)Peak memory usage: 35 MB % 167.79/23.96 % (394762)Instructions burned: 88029 (million) % 182.92/26.11 % (394936)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2454081214:i=176048:add=on:rtra=on:rawr=on_2804 on theBenchmark for (2804ds/176048Mi) % 182.92/26.11 % (394850)Instruction limit reached! % 182.92/26.11 % (394850)------------------------------ % 182.92/26.11 % (394850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.92/26.11 % (394850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.92/26.11 % (394850)CaDiCaL version: 2.1.3 % 182.92/26.11 % (394850)Termination reason: Instruction limit % 182.92/26.11 % (394850)Termination phase: Saturation % 182.92/26.11 % (394850)Time elapsed: 6.738 s % 182.92/26.11 % (394850)Peak memory usage: 19 MB % 182.92/26.11 % (394850)Instructions burned: 15853 (million) % 182.92/26.11 % (394938)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4153052894:i=206:fgj=on:rtra=on_2801 on theBenchmark for (2801ds/206Mi) % 182.92/26.11 % (394938)Instruction limit reached! % 182.92/26.11 % (394938)------------------------------ % 182.92/26.11 % (394938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.92/26.11 % (394938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.92/26.11 % (394938)CaDiCaL version: 2.1.3 % 182.92/26.11 % (394938)Termination reason: Instruction limit % 182.92/26.11 % (394938)Termination phase: Saturation % 182.92/26.11 % (394938)Time elapsed: 0.117 s % 182.92/26.11 % (394938)Peak memory usage: 15 MB % 182.92/26.11 % (394938)Instructions burned: 207 (million) % 182.92/26.11 % (394940)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1713582760:i=232:rtra=on_2800 on theBenchmark for (2800ds/232Mi) % 182.92/26.11 % (394940)Instruction limit reached! % 182.92/26.11 % (394940)------------------------------ % 182.92/26.11 % (394940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.92/26.11 % (394940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.92/26.11 % (394940)CaDiCaL version: 2.1.3 % 182.92/26.11 % (394940)Termination reason: Instruction limit % 182.92/26.11 % (394940)Termination phase: Saturation % 182.92/26.11 % (394940)Time elapsed: 0.137 s % 182.92/26.11 % (394940)Peak memory usage: 15 MB % 182.92/26.11 % (394940)Instructions burned: 233 (million) % 182.92/26.11 % (394942)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2714307735:i=262:rtra=on_2798 on theBenchmark for (2798ds/262Mi) % 182.92/26.11 % (394942)Instruction limit reached! % 182.92/26.11 % (394942)------------------------------ % 182.92/26.11 % (394942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.92/26.11 % (394942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.92/26.11 % (394942)CaDiCaL version: 2.1.3 % 182.92/26.11 % (394942)Termination reason: Instruction limit % 182.92/26.11 % (394942)Termination phase: Saturation % 182.92/26.11 % (394942)Time elapsed: 0.151 s % 182.92/26.11 % (394942)Peak memory usage: 16 MB % 182.92/26.11 % (394942)Instructions burned: 264 (million) % 182.92/26.11 % (394944)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=986528998:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2797 on theBenchmark for (2797ds/318Mi) % 182.92/26.11 % (394944)Instruction limit reached! % 182.92/26.11 % (394944)------------------------------ % 182.92/26.11 % (394944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.92/26.11 % (394944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.92/26.11 % (394944)CaDiCaL version: 2.1.3 % 182.92/26.11 % (394944)Termination reason: Instruction limit % 182.92/26.11 % (394944)Termination phase: Saturation % 182.92/26.11 % (394944)Time elapsed: 0.196 s % 182.92/26.11 % (394944)Peak memory usage: 16 MB % 182.92/26.11 % (394944)Instructions burned: 319 (million) % 182.92/26.11 % (394946)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2059453991:i=1428:nm=2:rtra=on_2794 on theBenchmark for (2794ds/1428Mi) % 182.92/26.11 % (394946)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 182.92/26.11 % (394946)Terminated due to inappropriate strategy. % 182.92/26.11 % (394946)------------------------------ % 182.92/26.11 % (394946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.92/26.11 % (394946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.92/26.11 % (394946)CaDiCaL version: 2.1.3 % 182.92/26.11 % (394946)Termination reason: Inappropriate % 182.92/26.11 % (394946)Time elapsed: 0.033 s % 182.92/26.11 % (394946)Peak memory usage: 12 MB % 182.92/26.11 % (394946)Instructions burned: 70 (million) % 182.92/26.11 % (394946)------------------------------ % 204.20/29.08 % (394946)------------------------------ % 204.20/29.08 % (394948)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=224685727:i=262:bd=preordered:rtra=on:fsd=on_2794 on theBenchmark for (2794ds/262Mi) % 204.20/29.08 % (394948)Instruction limit reached! % 204.20/29.08 % (394948)------------------------------ % 204.20/29.08 % (394948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.20/29.08 % (394948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.20/29.08 % (394948)CaDiCaL version: 2.1.3 % 204.20/29.08 % (394948)Termination reason: Instruction limit % 204.20/29.08 % (394948)Termination phase: Saturation % 204.20/29.08 % (394948)Time elapsed: 0.165 s % 204.20/29.08 % (394948)Peak memory usage: 16 MB % 204.20/29.08 % (394948)Instructions burned: 262 (million) % 204.20/29.08 % (394950)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=2538543087:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2792 on theBenchmark for (2792ds/1368Mi) % 204.20/29.08 % (394950)Instruction limit reached! % 204.20/29.08 % (394950)------------------------------ % 204.20/29.08 % (394950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.20/29.08 % (394950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.20/29.08 % (394950)CaDiCaL version: 2.1.3 % 204.20/29.08 % (394950)Termination reason: Instruction limit % 204.20/29.08 % (394950)Termination phase: Saturation % 204.20/29.08 % (394950)Time elapsed: 0.743 s % 204.20/29.08 % (394950)Peak memory usage: 28 MB % 204.20/29.08 % (394950)Instructions burned: 1369 (million) % 204.20/29.08 % (394952)ott-21_1_sil=16000:si=on:fs=off:random_seed=2938975080:i=360:av=off:fsr=off:rtra=on_2784 on theBenchmark for (2784ds/360Mi) % 204.20/29.08 % (394952)Instruction limit reached! % 204.20/29.08 % (394952)------------------------------ % 204.20/29.08 % (394952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.20/29.08 % (394952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.20/29.08 % (394952)CaDiCaL version: 2.1.3 % 204.20/29.08 % (394952)Termination reason: Instruction limit % 204.20/29.08 % (394952)Termination phase: Saturation % 204.20/29.08 % (394952)Time elapsed: 0.173 s % 204.20/29.08 % (394952)Peak memory usage: 15 MB % 204.20/29.08 % (394952)Instructions burned: 361 (million) % 204.20/29.08 % (394954)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3013031712:i=954:bd=all:rtra=on_2782 on theBenchmark for (2782ds/954Mi) % 204.20/29.08 % (394954)Instruction limit reached! % 204.20/29.08 % (394954)------------------------------ % 204.20/29.08 % (394954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.20/29.08 % (394954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.20/29.08 % (394954)CaDiCaL version: 2.1.3 % 204.20/29.08 % (394954)Termination reason: Instruction limit % 204.20/29.08 % (394954)Termination phase: Saturation % 204.20/29.08 % (394954)Time elapsed: 0.556 s % 204.20/29.08 % (394954)Peak memory usage: 19 MB % 204.20/29.08 % (394954)Instructions burned: 955 (million) % 204.20/29.08 % (394956)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=982967265:fmbsr=1.3:i=1730:ins=25:rtra=on_2777 on theBenchmark for (2777ds/1730Mi) % 204.20/29.08 % (394956)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 204.20/29.08 % (394956)Terminated due to inappropriate strategy. % 204.20/29.08 % (394956)------------------------------ % 204.20/29.08 % (394956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.20/29.08 % (394956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.20/29.08 % (394956)CaDiCaL version: 2.1.3 % 204.20/29.08 % (394956)Termination reason: Inappropriate % 204.20/29.08 % (394956)Time elapsed: 0.034 s % 204.20/29.08 % (394956)Peak memory usage: 12 MB % 204.20/29.08 % (394956)Instructions burned: 70 (million) % 204.20/29.08 % (394956)------------------------------ % 204.20/29.08 % (394956)------------------------------ % 204.20/29.08 % (394958)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2496655739:i=2358:rtra=on_2776 on theBenchmark for (2776ds/2358Mi) % 204.20/29.08 % (394958)Instruction limit reached! % 204.20/29.08 % (394958)------------------------------ % 204.20/29.08 % (394958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.20/29.08 % (394958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.20/29.08 % (394958)CaDiCaL version: 2.1.3 % 204.20/29.08 % (394958)Termination reason: Instruction limit % 204.20/29.08 % (394958)Termination phase: Saturation % 249.42/35.47 % (394958)Time elapsed: 1.350 s % 249.42/35.47 % (394958)Peak memory usage: 33 MB % 249.42/35.47 % (394958)Instructions burned: 2359 (million) % 249.42/35.47 % (394960)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2646820874:i=1778:ins=1:rtra=on_2762 on theBenchmark for (2762ds/1778Mi) % 249.42/35.47 % (394960)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.42/35.47 % (394960)Terminated due to inappropriate strategy. % 249.42/35.47 % (394960)------------------------------ % 249.42/35.47 % (394960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.42/35.47 % (394960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.42/35.47 % (394960)CaDiCaL version: 2.1.3 % 249.42/35.47 % (394960)Termination reason: Inappropriate % 249.42/35.47 % (394960)Time elapsed: 0.034 s % 249.42/35.47 % (394960)Peak memory usage: 12 MB % 249.42/35.47 % (394960)Instructions burned: 70 (million) % 249.42/35.47 % (394960)------------------------------ % 249.42/35.47 % (394960)------------------------------ % 249.42/35.47 % (394962)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=931416290:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2762 on theBenchmark for (2762ds/1384Mi) % 249.42/35.47 % (394962)Instruction limit reached! % 249.42/35.47 % (394962)------------------------------ % 249.42/35.47 % (394962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.42/35.47 % (394962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.42/35.47 % (394962)CaDiCaL version: 2.1.3 % 249.42/35.47 % (394962)Termination reason: Instruction limit % 249.42/35.47 % (394962)Termination phase: Saturation % 249.42/35.47 % (394962)Time elapsed: 0.931 s % 249.42/35.47 % (394962)Peak memory usage: 28 MB % 249.42/35.47 % (394962)Instructions burned: 1385 (million) % 249.42/35.47 % (394964)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3514325035:i=1758:kws=inv_precedence:fsr=off:rtra=on_2752 on theBenchmark for (2752ds/1758Mi) % 249.42/35.47 % (394964)Instruction limit reached! % 249.42/35.47 % (394964)------------------------------ % 249.42/35.47 % (394964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.42/35.47 % (394964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.42/35.47 % (394964)CaDiCaL version: 2.1.3 % 249.42/35.47 % (394964)Termination reason: Instruction limit % 249.42/35.47 % (394964)Termination phase: Saturation % 249.42/35.47 % (394964)Time elapsed: 0.978 s % 249.42/35.47 % (394964)Peak memory usage: 24 MB % 249.42/35.47 % (394964)Instructions burned: 1759 (million) % 249.42/35.47 % (394966)fmb+10_1_sil=64000:si=on:random_seed=113965378:i=44122:nm=2:rtra=on:gsp=on_2742 on theBenchmark for (2742ds/44122Mi) % 249.42/35.47 % (394966)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.42/35.47 % (394966)Terminated due to inappropriate strategy. % 249.42/35.47 % (394966)------------------------------ % 249.42/35.47 % (394966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.42/35.47 % (394966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.42/35.47 % (394966)CaDiCaL version: 2.1.3 % 249.42/35.47 % (394966)Termination reason: Inappropriate % 249.42/35.47 % (394966)Time elapsed: 0.034 s % 249.42/35.47 % (394966)Peak memory usage: 12 MB % 249.42/35.47 % (394966)Instructions burned: 70 (million) % 249.42/35.47 % (394966)------------------------------ % 249.42/35.47 % (394966)------------------------------ % 249.42/35.47 % (394968)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2862550037:i=19030:nm=5:rtra=on_2742 on theBenchmark for (2742ds/19030Mi) % 249.42/35.47 % (394968)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.42/35.47 % (394968)Terminated due to inappropriate strategy. % 249.42/35.47 % (394968)------------------------------ % 249.42/35.47 % (394968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.42/35.47 % (394968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.42/35.47 % (394968)CaDiCaL version: 2.1.3 % 249.42/35.47 % (394968)Termination reason: Inappropriate % 249.42/35.47 % (394968)Time elapsed: 0.034 s % 249.42/35.47 % (394968)Peak memory usage: 13 MB % 249.42/35.47 % (394968)Instructions burned: 70 (million) % 249.42/35.47 % (394968)------------------------------ % 249.42/35.47 % (394968)------------------------------ % 249.42/35.47 % (394970)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3516272921:fmbsr=1.7:i=1840:rtra=on_2741 on theBenchmark for (2741ds/1840Mi) % 275.19/39.07 % (394970)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 275.19/39.07 % (394970)Terminated due to inappropriate strategy. % 275.19/39.07 % (394970)------------------------------ % 275.19/39.07 % (394970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.19/39.07 % (394970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.19/39.07 % (394970)CaDiCaL version: 2.1.3 % 275.19/39.07 % (394970)Termination reason: Inappropriate % 275.19/39.07 % (394970)Time elapsed: 0.034 s % 275.19/39.07 % (394970)Peak memory usage: 12 MB % 275.19/39.07 % (394970)Instructions burned: 70 (million) % 275.19/39.07 % (394970)------------------------------ % 275.19/39.07 % (394970)------------------------------ % 275.19/39.07 % (394972)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1748081830:i=10262:rtra=on_2740 on theBenchmark for (2740ds/10262Mi) % 275.19/39.07 % (394914)Instruction limit reached! % 275.19/39.07 % (394914)------------------------------ % 275.19/39.07 % (394914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.19/39.07 % (394914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.19/39.07 % (394914)CaDiCaL version: 2.1.3 % 275.19/39.07 % (394914)Termination reason: Instruction limit % 275.19/39.07 % (394914)Termination phase: Saturation % 275.19/39.07 % (394914)Time elapsed: 10.937 s % 275.19/39.07 % (394914)Peak memory usage: 188 MB % 275.19/39.07 % (394914)Instructions burned: 17627 (million) % 275.19/39.07 % (394974)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=610754257:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2737 on theBenchmark for (2737ds/2944Mi) % 275.19/39.07 % (394974)Instruction limit reached! % 275.19/39.07 % (394974)------------------------------ % 275.19/39.07 % (394974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.19/39.07 % (394974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.19/39.07 % (394974)CaDiCaL version: 2.1.3 % 275.19/39.07 % (394974)Termination reason: Instruction limit % 275.19/39.07 % (394974)Termination phase: Saturation % 275.19/39.07 % (394974)Time elapsed: 1.535 s % 275.19/39.07 % (394974)Peak memory usage: 42 MB % 275.19/39.07 % (394974)Instructions burned: 2944 (million) % 275.19/39.07 % (394978)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3609360173:i=12648:rtra=on_2721 on theBenchmark for (2721ds/12648Mi) % 275.19/39.07 % (394978)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 275.19/39.07 % (394978)Terminated due to inappropriate strategy. % 275.19/39.07 % (394978)------------------------------ % 275.19/39.07 % (394978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.19/39.07 % (394978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.19/39.07 % (394978)CaDiCaL version: 2.1.3 % 275.19/39.07 % (394978)Termination reason: Inappropriate % 275.19/39.07 % (394978)Time elapsed: 0.034 s % 275.19/39.07 % (394978)Peak memory usage: 12 MB % 275.19/39.07 % (394978)Instructions burned: 70 (million) % 275.19/39.07 % (394978)------------------------------ % 275.19/39.07 % (394978)------------------------------ % 275.19/39.07 % (394980)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=4015628163:fmbsr=2.30978:i=4348:rtra=on_2721 on theBenchmark for (2721ds/4348Mi) % 275.19/39.07 % (394980)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 275.19/39.07 % (394980)Terminated due to inappropriate strategy. % 275.19/39.07 % (394980)------------------------------ % 275.19/39.07 % (394980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.19/39.07 % (394980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.19/39.07 % (394980)CaDiCaL version: 2.1.3 % 275.19/39.07 % (394980)Termination reason: Inappropriate % 275.19/39.07 % (394980)Time elapsed: 0.034 s % 275.19/39.07 % (394980)Peak memory usage: 12 MB % 275.19/39.07 % (394980)Instructions burned: 70 (million) % 275.19/39.07 % (394980)------------------------------ % 275.19/39.07 % (394980)------------------------------ % 275.19/39.07 % (394982)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1041577864:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2720 on theBenchmark for (2720ds/1738Mi) % 275.19/39.07 % (394982)Instruction limit reached! % 275.19/39.07 % (394982)------------------------------ % 275.19/39.07 % (394982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.19/39.07 % (394982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.63 % (394982)CaDiCaL version: 2.1.3 % 300.49/42.63 % (394982)Termination reason: Instruction limit % 300.49/42.63 % (394982)Termination phase: Saturation % 300.49/42.63 % (394982)Time elapsed: 0.881 s % 300.49/42.63 % (394982)Peak memory usage: 17 MB % 300.49/42.63 % (394982)Instructions burned: 1739 (million) % 300.49/42.63 % (394984)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2216815009:i=10228:av=off:rtra=on_2711 on theBenchmark for (2711ds/10228Mi) % 300.49/42.63 % (394920)Instruction limit reached! % 300.49/42.63 % (394920)------------------------------ % 300.49/42.63 % (394920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.63 % (394920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.63 % (394920)CaDiCaL version: 2.1.3 % 300.49/42.63 % (394920)Termination reason: Instruction limit % 300.49/42.63 % (394920)Termination phase: Saturation % 300.49/42.63 % (394920)Time elapsed: 14.677 s % 300.49/42.63 % (394920)Peak memory usage: 105 MB % 300.49/42.63 % (394920)Instructions burned: 28120 (million) % 300.49/42.63 % (394986)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1916719132:i=108564:rtra=on_2696 on theBenchmark for (2696ds/108564Mi) % 300.49/42.63 % (394986)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.49/42.63 % (394986)Terminated due to inappropriate strategy. % 300.49/42.63 % (394986)------------------------------ % 300.49/42.63 % (394986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.63 % (394986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.63 % (394986)CaDiCaL version: 2.1.3 % 300.49/42.63 % (394986)Termination reason: Inappropriate % 300.49/42.63 % (394986)Time elapsed: 0.035 s % 300.49/42.63 % (394986)Peak memory usage: 12 MB % 300.49/42.63 % (394986)Instructions burned: 70 (million) % 300.49/42.63 % (394986)------------------------------ % 300.49/42.63 % (394986)------------------------------ % 300.49/42.63 % (394988)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=4197738571:i=7024:aac=none:rtra=on_2696 on theBenchmark for (2696ds/7024Mi) % 300.49/42.63 % (394972)Instruction limit reached! % 300.49/42.63 % (394972)------------------------------ % 300.49/42.63 % (394972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.64 % (394972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.64 % (394972)CaDiCaL version: 2.1.3 % 300.49/42.64 % (394972)Termination reason: Instruction limit % 300.49/42.64 % (394972)Termination phase: Saturation % 300.49/42.64 % (394972)Time elapsed: 5.677 s % 300.49/42.64 % (394972)Peak memory usage: 80 MB % 300.49/42.64 % (394972)Instructions burned: 10263 (million) % 300.49/42.64 % (394990)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=927190830:i=7546:rtra=on:amm=off_2683 on theBenchmark for (2683ds/7546Mi) % 300.49/42.64 % (394988)Instruction limit reached! % 300.49/42.64 % (394988)------------------------------ % 300.49/42.64 % (394988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.64 % (394988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.64 % (394988)CaDiCaL version: 2.1.3 % 300.49/42.64 % (394988)Termination reason: Instruction limit % 300.49/42.64 % (394988)Termination phase: Saturation % 300.49/42.64 % (394988)Time elapsed: 3.801 s % 300.49/42.64 % (394988)Peak memory usage: 61 MB % 300.49/42.64 % (394988)Instructions burned: 7025 (million) % 300.49/42.64 % (394992)ott+11_1_sil=16000:si=on:gs=on:random_seed=1609036119:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2657 on theBenchmark for (2657ds/4502Mi) % 300.49/42.64 % (394984)Instruction limit reached! % 300.49/42.64 % (394984)------------------------------ % 300.49/42.64 % (394984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.64 % (394984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.64 % (394984)CaDiCaL version: 2.1.3 % 300.49/42.64 % (394984)Termination reason: Instruction limit % 300.49/42.64 % (394984)Termination phase: Saturation % 300.49/42.64 % (394984)Time elapsed: 6.301 s % 300.49/42.64 % (394984)Peak memory usage: 81 MB % 300.49/42.64 % (394984)Instructions burned: 10229 (million) % 300.49/42.64 % (394994)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=745734431:fmbsr=1.6:i=135068:rtra=on_2648 on theBenchmark for (2648ds/135068Mi) % 300.49/42.64 % (394994)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.49/42.64 % (394994)Terminated due to inappropriate strategy. % 300.49/42.64 % (394994)------------------------------ % 300.49/42.64 % (394994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.64 % (394994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.64 % (394994)CaDiCaL version: 2.1.3 % 300.49/42.64 % (394994)Termination reason: Inappropriate % 300.49/42.64 % (394994)Time elapsed: 0.034 s % 300.49/42.64 % (394994)Peak memory usage: 12 MB % 300.49/42.64 % (394994)Instructions burned: 70 (million) % 300.49/42.64 % (394994)------------------------------ % 300.49/42.64 % (394994)------------------------------ % 300.49/42.64 % (394996)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3723493103:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2647 on theBenchmark for (2647ds/9182Mi) % 300.49/42.64 % (394990)Instruction limit reached! % 300.49/42.64 % (394990)------------------------------ % 300.49/42.64 % (394990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.64 % (394990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.64 % (394990)CaDiCaL version: 2.1.3 % 300.49/42.64 % (394990)Termination reason: Instruction limit % 300.49/42.64 % (394990)Termination phase: Saturation % 300.49/42.64 % (394990)Time elapsed: 4.164 s % 300.49/42.64 % (394990)Peak memory usage: 65 MB % 300.49/42.64 % (394990)Instructions burned: 7548 (million) % 300.49/42.64 % (394998)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=2903969718:i=58680:rtra=on_2641 on theBenchmark for (2641ds/58680Mi) % 300.49/42.64 % (394992)Instruction limit reached! % 300.49/42.64 % (394992)------------------------------ % 300.49/42.64 % (394992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.64 % (394992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.64 % (394992)CaDiCaL version: 2.1.3 % 300.49/42.64 % (394992)Termination reason: Instruction limit % 300.49/42.64 % (394992)Termination phase: Saturation % 300.49/42.64 % (394992)Time elapsed: 2.408 s % 300.49/42.64 % (394992)Peak memory usage: 41 MB % 300.49/42.64 % (394992)Instructions burned: 4502 (million) % 300.49/42.64 % (395000)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=1062386317:i=10422:rtra=on_2633 on theBenchmark for (2633ds/10422Mi) % 300.49/42.64 % (394916)Instruction limit reached! % 300.49/42.64 % (394916)------------------------------ % 300.49/42.64 % (394916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.64 % (394916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.64 % (394916)CaDiCaL version: 2.1.3 % 300.49/42.64 % (394916)Termination reason: Instruction limit % 300.49/42.64 % (394916)Termination phase: Saturation % 300.49/42.64 % (394916)Time elapsed: 23.099 s % 300.49/42.64 % (394916)Peak memory usage: 370 MB % 300.49/42.64 % (394916)Instructions burned: 53296 (million) % 300.49/42.64 % (395002)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=2116331987:i=10994:nm=2:rtra=on_2612 on theBenchmark for (2612ds/10994Mi) % 300.49/42.64 % (395002)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.49/42.64 % (395002)Terminated due to inappropriate strategy. % 300.49/42.64 % (395002)------------------------------ % 300.49/42.64 % (395002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.64 % (395002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.64 % (395002)CaDiCaL version: 2.1.3 % 300.49/42.64 % (395002)Termination reason: Inappropriate % 300.49/42.64 % (395002)Time elapsed: 0.033 s % 300.49/42.64 % (395002)Peak memory usage: 12 MB % 300.49/42.64 % (395002)Instructions burned: 70 (million) % 300.49/42.64 % (395002)------------------------------ % 300.49/42.64 % (395002)------------------------------ % 300.49/42.64 % (395004)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:si=on:fmbss=15:random_seed=1293772886:fmbsr=2:i=92664:rtra=on_2612 on theBenchmark for (2612ds/92664Mi) % 300.49/42.64 % (395004)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.49/42.64 % (395004)Terminated due to inappropriate strategy. % 300.49/42.64 % (395004)------------------------------ % 300.49/42.64 % (395004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.64 % (395004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.64 % (395004)CaDiCaL version: 2.1.3 % 300.49/42.64 % (395004)Termination reason: Inappropriate % 300.49/42.64 % (395004)Time elapsed: 0.034 s % 300.49/42.64 % (395004)Peak memory usage: 12 MB % 300.49/42.64 % (395004)Instructions burned: 70 (million) % 300.49/42.64 % (395004)------------------------------ % 300.49/42.64 % % 300.49/42.64 Terminated % 300.49/42.64 % Vampire exiting % 300.49/42.64 Terminated %------------------------------------------------------------------------------