%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW603_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:30 PM UTC 2026 % Result : Timeout 300.16s 42.73s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWW603_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.00/0.11 % Computer : n012.cluster.edu % 0.00/0.11 % Model : x86_64 x86_64 % 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.11 % Memory : 8046.5625MB % 0.00/0.11 % OS : Linux 6.8.0-71-generic % 0.00/0.11 % CPULimit : 300 % 0.00/0.11 % WCLimit : 300 % 0.00/0.11 % DateTime : Mon Sep 28 14:20:49 UTC 2026 % 0.00/0.11 % CPUTime : % 0.00/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.12 Running first-order model finding % 0.09/0.12 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.03/0.45 % (3405986)Will run a generic schedule for satisfiability detection. % 2.03/0.45 % (3405992)% WARNING: option uhcvi not known. % 2.03/0.45 % (3405994)dis+10_1_sil=32000:sp=arity:random_seed=2608045829:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.03/0.45 % (3405991)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3381316516_2999 on theBenchmark for (2999ds/0Mi) % 2.03/0.45 % (3405992)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3901943345:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.03/0.45 % (3405993)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2804712095:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.03/0.45 % (3405997)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1501570200:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.03/0.45 % (3405995)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2591638255:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.03/0.45 % (3405996)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=104785451:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.03/0.45 % (3405991)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.03/0.45 % (3405991)Terminated due to inappropriate strategy. % 2.03/0.45 % (3405991)------------------------------ % 2.03/0.45 % (3405991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.03/0.45 % (3405991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.03/0.45 % (3405991)CaDiCaL version: 2.1.3 % 2.03/0.45 % (3405991)Termination reason: Inappropriate % 2.03/0.45 % (3405991)Time elapsed: 0.002 s % 2.03/0.45 % (3405991)Peak memory usage: 11 MB % 2.03/0.45 % (3405991)Instructions burned: 6 (million) % 2.03/0.45 % (3405991)------------------------------ % 2.03/0.45 % (3405991)------------------------------ % 2.03/0.45 % (3406005)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3520646651:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.03/0.45 % (3406005)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.03/0.45 % (3406005)Terminated due to inappropriate strategy. % 2.03/0.45 % (3406005)------------------------------ % 2.03/0.45 % (3406005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.03/0.45 % (3406005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.03/0.45 % (3406005)CaDiCaL version: 2.1.3 % 2.03/0.45 % (3406005)Termination reason: Inappropriate % 2.03/0.45 % (3406005)Time elapsed: 0.001 s % 2.03/0.45 % (3406005)Peak memory usage: 10 MB % 2.03/0.45 % (3406005)Instructions burned: 5 (million) % 2.03/0.45 % (3406005)------------------------------ % 2.03/0.45 % (3406005)------------------------------ % 2.03/0.45 % (3406007)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3467712905:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.03/0.45 % (3405994)Instruction limit reached! % 2.03/0.45 % (3405994)------------------------------ % 2.03/0.45 % (3405994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.03/0.45 % (3405994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.03/0.45 % (3405994)CaDiCaL version: 2.1.3 % 2.03/0.45 % (3405994)Termination reason: Instruction limit % 2.03/0.45 % (3405994)Termination phase: Saturation % 2.03/0.45 % (3405994)Time elapsed: 0.034 s % 2.03/0.45 % (3405994)Peak memory usage: 12 MB % 2.03/0.45 % (3405994)Instructions burned: 103 (million) % 2.03/0.45 % (3405995)Instruction limit reached! % 2.03/0.45 % (3405995)------------------------------ % 2.03/0.45 % (3405995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.03/0.45 % (3405995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.03/0.45 % (3405995)CaDiCaL version: 2.1.3 % 2.03/0.45 % (3405995)Termination reason: Instruction limit % 2.03/0.45 % (3405995)Termination phase: Saturation % 2.03/0.45 % (3405995)Time elapsed: 0.039 s % 2.03/0.45 % (3405995)Peak memory usage: 13 MB % 2.03/0.45 % (3405995)Instructions burned: 117 (million) % 2.03/0.45 % (3406009)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=403384003:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 2.03/0.45 % (3405996)Instruction limit reached! % 2.03/0.45 % (3405996)------------------------------ % 2.03/0.45 % (3405996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.27/0.63 % (3405996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.27/0.63 % (3405996)CaDiCaL version: 2.1.3 % 3.27/0.63 % (3405996)Termination reason: Instruction limit % 3.27/0.63 % (3405996)Termination phase: Saturation % 3.27/0.63 % (3405996)Time elapsed: 0.047 s % 3.27/0.63 % (3405996)Peak memory usage: 13 MB % 3.27/0.63 % (3405996)Instructions burned: 132 (million) % 3.27/0.63 % (3405997)Instruction limit reached! % 3.27/0.63 % (3405997)------------------------------ % 3.27/0.63 % (3405997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.27/0.63 % (3405997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.27/0.63 % (3405997)CaDiCaL version: 2.1.3 % 3.27/0.63 % (3405997)Termination reason: Instruction limit % 3.27/0.63 % (3405997)Termination phase: Saturation % 3.27/0.63 % (3405997)Time elapsed: 0.049 s % 3.27/0.63 % (3405997)Peak memory usage: 13 MB % 3.27/0.63 % (3405997)Instructions burned: 162 (million) % 3.27/0.63 % (3406010)ott-21_1_sil=16000:fs=off:random_seed=1807980844:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.27/0.63 % (3406012)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3173246579:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 3.27/0.63 % (3406013)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=783628535:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi) % 3.27/0.63 % (3406013)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.27/0.63 % (3406013)Terminated due to inappropriate strategy. % 3.27/0.63 % (3406013)------------------------------ % 3.27/0.63 % (3406013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.27/0.63 % (3406013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.27/0.63 % (3406013)CaDiCaL version: 2.1.3 % 3.27/0.63 % (3406013)Termination reason: Inappropriate % 3.27/0.63 % (3406013)Time elapsed: 0.001 s % 3.27/0.63 % (3406013)Peak memory usage: 10 MB % 3.27/0.63 % (3406013)Instructions burned: 5 (million) % 3.27/0.63 % (3406013)------------------------------ % 3.27/0.63 % (3406013)------------------------------ % 3.27/0.63 % (3406017)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1918094540:i=1179_2999 on theBenchmark for (2999ds/1179Mi) % 3.27/0.63 % (3406007)Instruction limit reached! % 3.27/0.63 % (3406007)------------------------------ % 3.27/0.63 % (3406007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.27/0.63 % (3406007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.27/0.63 % (3406007)CaDiCaL version: 2.1.3 % 3.27/0.63 % (3406007)Termination reason: Instruction limit % 3.27/0.63 % (3406007)Termination phase: Saturation % 3.27/0.63 % (3406007)Time elapsed: 0.047 s % 3.27/0.63 % (3406007)Peak memory usage: 13 MB % 3.27/0.63 % (3406007)Instructions burned: 132 (million) % 3.27/0.63 % (3406019)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4273574791:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 3.27/0.63 % (3406019)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.27/0.63 % (3406019)Terminated due to inappropriate strategy. % 3.27/0.63 % (3406019)------------------------------ % 3.27/0.63 % (3406019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.27/0.63 % (3406019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.27/0.63 % (3406019)CaDiCaL version: 2.1.3 % 3.27/0.63 % (3406019)Termination reason: Inappropriate % 3.27/0.63 % (3406019)Time elapsed: 0.001 s % 3.27/0.63 % (3406019)Peak memory usage: 10 MB % 3.27/0.63 % (3406019)Instructions burned: 5 (million) % 3.27/0.63 % (3406019)------------------------------ % 3.27/0.63 % (3406019)------------------------------ % 3.27/0.63 % (3406021)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=1913633350: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) % 3.27/0.63 % (3406010)Instruction limit reached! % 3.27/0.63 % (3406010)------------------------------ % 3.27/0.63 % (3406010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.27/0.63 % (3406010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.27/0.63 % (3406010)CaDiCaL version: 2.1.3 % 3.27/0.63 % (3406010)Termination reason: Instruction limit % 3.27/0.63 % (3406010)Termination phase: Saturation % 11.88/1.97 % (3406010)Time elapsed: 0.054 s % 11.88/1.97 % (3406010)Peak memory usage: 13 MB % 11.88/1.97 % (3406010)Instructions burned: 185 (million) % 11.88/1.97 % (3406023)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=915507619:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 11.88/1.97 % (3406012)Instruction limit reached! % 11.88/1.97 % (3406012)------------------------------ % 11.88/1.97 % (3406012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.88/1.97 % (3406012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/1.97 % (3406012)CaDiCaL version: 2.1.3 % 11.88/1.97 % (3406012)Termination reason: Instruction limit % 11.88/1.97 % (3406012)Termination phase: Saturation % 11.88/1.97 % (3406012)Time elapsed: 0.156 s % 11.88/1.97 % (3406012)Peak memory usage: 14 MB % 11.88/1.97 % (3406012)Instructions burned: 479 (million) % 11.88/1.97 % (3406025)fmb+10_1_sil=64000:random_seed=497434490:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 11.88/1.97 % (3406025)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.88/1.97 % (3406025)Terminated due to inappropriate strategy. % 11.88/1.97 % (3406025)------------------------------ % 11.88/1.97 % (3406025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.88/1.97 % (3406025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/1.97 % (3406025)CaDiCaL version: 2.1.3 % 11.88/1.97 % (3406025)Termination reason: Inappropriate % 11.88/1.97 % (3406025)Time elapsed: 0.002 s % 11.88/1.97 % (3406025)Peak memory usage: 10 MB % 11.88/1.97 % (3406025)Instructions burned: 6 (million) % 11.88/1.97 % (3406025)------------------------------ % 11.88/1.97 % (3406025)------------------------------ % 11.88/1.97 % (3406027)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2870000602:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 11.88/1.97 % (3406027)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.88/1.97 % (3406027)Terminated due to inappropriate strategy. % 11.88/1.97 % (3406027)------------------------------ % 11.88/1.97 % (3406027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.88/1.97 % (3406027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/1.97 % (3406027)CaDiCaL version: 2.1.3 % 11.88/1.97 % (3406027)Termination reason: Inappropriate % 11.88/1.97 % (3406027)Time elapsed: 0.001 s % 11.88/1.97 % (3406027)Peak memory usage: 10 MB % 11.88/1.97 % (3406027)Instructions burned: 5 (million) % 11.88/1.97 % (3406027)------------------------------ % 11.88/1.97 % (3406027)------------------------------ % 11.88/1.97 % (3406029)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3017912108:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 11.88/1.97 % (3406029)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.88/1.97 % (3406029)Terminated due to inappropriate strategy. % 11.88/1.97 % (3406029)------------------------------ % 11.88/1.97 % (3406029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.88/1.97 % (3406029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/1.97 % (3406029)CaDiCaL version: 2.1.3 % 11.88/1.97 % (3406029)Termination reason: Inappropriate % 11.88/1.97 % (3406029)Time elapsed: 0.001 s % 11.88/1.97 % (3406029)Peak memory usage: 10 MB % 11.88/1.97 % (3406029)Instructions burned: 5 (million) % 11.88/1.97 % (3406029)------------------------------ % 11.88/1.97 % (3406029)------------------------------ % 11.88/1.97 % (3406031)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3142489264:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 11.88/1.97 % (3406009)Instruction limit reached! % 11.88/1.97 % (3406009)------------------------------ % 11.88/1.97 % (3406009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.88/1.97 % (3406009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/1.97 % (3406009)CaDiCaL version: 2.1.3 % 11.88/1.97 % (3406009)Termination reason: Instruction limit % 11.88/1.97 % (3406009)Termination phase: Saturation % 11.88/1.97 % (3406009)Time elapsed: 0.227 s % 11.88/1.97 % (3406009)Peak memory usage: 17 MB % 11.88/1.97 % (3406009)Instructions burned: 684 (million) % 11.88/1.97 % (3406033)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=146207171:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 11.88/1.97 % (3406021)Instruction limit reached! % 11.88/1.97 % (3406021)------------------------------ % 17.98/2.94 % (3406021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.98/2.94 % (3406021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.98/2.94 % (3406021)CaDiCaL version: 2.1.3 % 17.98/2.94 % (3406021)Termination reason: Instruction limit % 17.98/2.94 % (3406021)Termination phase: Saturation % 17.98/2.94 % (3406021)Time elapsed: 0.199 s % 17.98/2.94 % (3406021)Peak memory usage: 20 MB % 17.98/2.94 % (3406021)Instructions burned: 692 (million) % 17.98/2.94 % (3406035)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3110028902:i=6324_2996 on theBenchmark for (2996ds/6324Mi) % 17.98/2.94 % (3406035)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.98/2.94 % (3406035)Terminated due to inappropriate strategy. % 17.98/2.94 % (3406035)------------------------------ % 17.98/2.94 % (3406035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.98/2.94 % (3406035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.98/2.94 % (3406035)CaDiCaL version: 2.1.3 % 17.98/2.94 % (3406035)Termination reason: Inappropriate % 17.98/2.94 % (3406035)Time elapsed: 0.002 s % 17.98/2.94 % (3406035)Peak memory usage: 11 MB % 17.98/2.94 % (3406035)Instructions burned: 6 (million) % 17.98/2.94 % (3406035)------------------------------ % 17.98/2.94 % (3406035)------------------------------ % 17.98/2.94 % (3406037)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1661429812:fmbsr=2.30978:i=2174_2996 on theBenchmark for (2996ds/2174Mi) % 17.98/2.94 % (3406037)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.98/2.94 % (3406037)Terminated due to inappropriate strategy. % 17.98/2.94 % (3406037)------------------------------ % 17.98/2.94 % (3406037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.98/2.94 % (3406037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.98/2.94 % (3406037)CaDiCaL version: 2.1.3 % 17.98/2.94 % (3406037)Termination reason: Inappropriate % 17.98/2.94 % (3406037)Time elapsed: 0.001 s % 17.98/2.94 % (3406037)Peak memory usage: 10 MB % 17.98/2.94 % (3406037)Instructions burned: 5 (million) % 17.98/2.94 % (3406037)------------------------------ % 17.98/2.94 % (3406037)------------------------------ % 17.98/2.94 % (3406039)ott-2_1_sil=16000:newcnf=on:random_seed=124286628:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2996 on theBenchmark for (2996ds/869Mi) % 17.98/2.94 % (3406023)Instruction limit reached! % 17.98/2.94 % (3406023)------------------------------ % 17.98/2.94 % (3406023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.98/2.94 % (3406023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.98/2.94 % (3406023)CaDiCaL version: 2.1.3 % 17.98/2.94 % (3406023)Termination reason: Instruction limit % 17.98/2.94 % (3406023)Termination phase: Saturation % 17.98/2.94 % (3406023)Time elapsed: 0.281 s % 17.98/2.94 % (3406023)Peak memory usage: 18 MB % 17.98/2.94 % (3406023)Instructions burned: 881 (million) % 17.98/2.94 % (3406041)ott+10_1_sil=32000:tgt=ground:random_seed=3871999682:i=5114:av=off_2995 on theBenchmark for (2995ds/5114Mi) % 17.98/2.94 % (3406017)Instruction limit reached! % 17.98/2.94 % (3406017)------------------------------ % 17.98/2.94 % (3406017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.98/2.94 % (3406017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.98/2.94 % (3406017)CaDiCaL version: 2.1.3 % 17.98/2.94 % (3406017)Termination reason: Instruction limit % 17.98/2.94 % (3406017)Termination phase: Saturation % 17.98/2.94 % (3406017)Time elapsed: 0.388 s % 17.98/2.94 % (3406017)Peak memory usage: 21 MB % 17.98/2.94 % (3406017)Instructions burned: 1179 (million) % 17.98/2.94 % (3406043)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3407561606:i=54282_2995 on theBenchmark for (2995ds/54282Mi) % 17.98/2.94 % (3406043)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.98/2.94 % (3406043)Terminated due to inappropriate strategy. % 17.98/2.94 % (3406043)------------------------------ % 17.98/2.94 % (3406043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.98/2.94 % (3406043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.98/2.94 % (3406043)CaDiCaL version: 2.1.3 % 17.98/2.94 % (3406043)Termination reason: Inappropriate % 17.98/2.94 % (3406043)Time elapsed: 0.002 s % 17.98/2.94 % (3406043)Peak memory usage: 11 MB % 17.98/2.94 % (3406043)Instructions burned: 6 (million) % 58.21/8.43 % (3406043)------------------------------ % 58.21/8.43 % (3406043)------------------------------ % 58.21/8.43 % (3406045)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=377293061:i=3512:aac=none_2994 on theBenchmark for (2994ds/3512Mi) % 58.21/8.43 % (3406039)Instruction limit reached! % 58.21/8.43 % (3406039)------------------------------ % 58.21/8.43 % (3406039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.21/8.43 % (3406039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.21/8.43 % (3406039)CaDiCaL version: 2.1.3 % 58.21/8.43 % (3406039)Termination reason: Instruction limit % 58.21/8.43 % (3406039)Termination phase: Saturation % 58.21/8.43 % (3406039)Time elapsed: 0.284 s % 58.21/8.43 % (3406039)Peak memory usage: 18 MB % 58.21/8.43 % (3406039)Instructions burned: 870 (million) % 58.21/8.43 % (3406047)dis+21_1_sil=32000:sas=cadical:random_seed=424037598:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi) % 58.21/8.43 % (3406033)Instruction limit reached! % 58.21/8.43 % (3406033)------------------------------ % 58.21/8.43 % (3406033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.21/8.43 % (3406033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.21/8.43 % (3406033)CaDiCaL version: 2.1.3 % 58.21/8.43 % (3406033)Termination reason: Instruction limit % 58.21/8.43 % (3406033)Termination phase: Saturation % 58.21/8.43 % (3406033)Time elapsed: 0.380 s % 58.21/8.43 % (3406033)Peak memory usage: 21 MB % 58.21/8.43 % (3406033)Instructions burned: 1473 (million) % 58.21/8.43 % (3406049)ott+11_1_sil=16000:gs=on:random_seed=550809190:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2993 on theBenchmark for (2993ds/2251Mi) % 58.21/8.43 % (3406049)Instruction limit reached! % 58.21/8.43 % (3406049)------------------------------ % 58.21/8.43 % (3406049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.21/8.43 % (3406049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.21/8.43 % (3406049)CaDiCaL version: 2.1.3 % 58.21/8.43 % (3406049)Termination reason: Instruction limit % 58.21/8.43 % (3406049)Termination phase: Saturation % 58.21/8.43 % (3406049)Time elapsed: 0.703 s % 58.21/8.43 % (3406049)Peak memory usage: 22 MB % 58.21/8.43 % (3406049)Instructions burned: 2254 (million) % 58.21/8.43 % (3406051)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3148197426:fmbsr=1.6:i=67534_2985 on theBenchmark for (2985ds/67534Mi) % 58.21/8.43 % (3406051)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 58.21/8.43 % (3406051)Terminated due to inappropriate strategy. % 58.21/8.43 % (3406051)------------------------------ % 58.21/8.43 % (3406051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.21/8.43 % (3406051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.21/8.43 % (3406051)CaDiCaL version: 2.1.3 % 58.21/8.43 % (3406051)Termination reason: Inappropriate % 58.21/8.43 % (3406051)Time elapsed: 0.002 s % 58.21/8.43 % (3406051)Peak memory usage: 11 MB % 58.21/8.43 % (3406051)Instructions burned: 5 (million) % 58.21/8.43 % (3406051)------------------------------ % 58.21/8.43 % (3406051)------------------------------ % 58.21/8.43 % (3406053)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3762002116:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2985 on theBenchmark for (2985ds/4591Mi) % 58.21/8.43 % (3406045)Instruction limit reached! % 58.21/8.43 % (3406045)------------------------------ % 58.21/8.43 % (3406045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.21/8.43 % (3406045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.21/8.43 % (3406045)CaDiCaL version: 2.1.3 % 58.21/8.43 % (3406045)Termination reason: Instruction limit % 58.21/8.43 % (3406045)Termination phase: Saturation % 58.21/8.43 % (3406045)Time elapsed: 1.118 s % 58.21/8.43 % (3406045)Peak memory usage: 45 MB % 58.21/8.43 % (3406045)Instructions burned: 3513 (million) % 58.21/8.43 % (3406055)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2206015814:i=29340_2983 on theBenchmark for (2983ds/29340Mi) % 58.21/8.43 % (3406047)Instruction limit reached! % 58.21/8.43 % (3406047)------------------------------ % 58.21/8.43 % (3406047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.21/8.43 % (3406047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.21/8.43 % (3406047)CaDiCaL version: 2.1.3 % 58.21/8.43 % (3406047)Termination reason: Instruction limit % 73.03/10.58 % (3406047)Termination phase: Saturation % 73.03/10.58 % (3406047)Time elapsed: 1.183 s % 73.03/10.58 % (3406047)Peak memory usage: 33 MB % 73.03/10.58 % (3406047)Instructions burned: 3775 (million) % 73.03/10.58 % (3406057)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2338358154:i=5211_2981 on theBenchmark for (2981ds/5211Mi) % 73.03/10.58 % (3406031)Instruction limit reached! % 73.03/10.58 % (3406031)------------------------------ % 73.03/10.58 % (3406031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.03/10.58 % (3406031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.03/10.58 % (3406031)CaDiCaL version: 2.1.3 % 73.03/10.58 % (3406031)Termination reason: Instruction limit % 73.03/10.58 % (3406031)Termination phase: Saturation % 73.03/10.58 % (3406031)Time elapsed: 1.571 s % 73.03/10.58 % (3406031)Peak memory usage: 43 MB % 73.03/10.58 % (3406031)Instructions burned: 5131 (million) % 73.03/10.58 % (3406059)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=585868275:i=5497:nm=2_2981 on theBenchmark for (2981ds/5497Mi) % 73.03/10.58 % (3406059)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 73.03/10.58 % (3406059)Terminated due to inappropriate strategy. % 73.03/10.58 % (3406059)------------------------------ % 73.03/10.58 % (3406059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.03/10.58 % (3406059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.03/10.58 % (3406059)CaDiCaL version: 2.1.3 % 73.03/10.58 % (3406059)Termination reason: Inappropriate % 73.03/10.58 % (3406059)Time elapsed: 0.002 s % 73.03/10.58 % (3406059)Peak memory usage: 11 MB % 73.03/10.58 % (3406059)Instructions burned: 6 (million) % 73.03/10.58 % (3406059)------------------------------ % 73.03/10.58 % (3406059)------------------------------ % 73.03/10.58 % (3406061)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=820314262:fmbsr=2:i=46332_2981 on theBenchmark for (2981ds/46332Mi) % 73.03/10.58 % (3406061)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 73.03/10.58 % (3406061)Terminated due to inappropriate strategy. % 73.03/10.58 % (3406061)------------------------------ % 73.03/10.58 % (3406061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.03/10.58 % (3406061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.03/10.58 % (3406061)CaDiCaL version: 2.1.3 % 73.03/10.58 % (3406061)Termination reason: Inappropriate % 73.03/10.58 % (3406061)Time elapsed: 0.002 s % 73.03/10.58 % (3406061)Peak memory usage: 11 MB % 73.03/10.58 % (3406061)Instructions burned: 6 (million) % 73.03/10.58 % (3406061)------------------------------ % 73.03/10.58 % (3406061)------------------------------ % 73.03/10.58 % (3406063)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3418170904:i=14071_2981 on theBenchmark for (2981ds/14071Mi) % 73.03/10.58 % (3406063)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 73.03/10.58 % (3406063)Terminated due to inappropriate strategy. % 73.03/10.58 % (3406063)------------------------------ % 73.03/10.58 % (3406063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.03/10.58 % (3406063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.03/10.58 % (3406063)CaDiCaL version: 2.1.3 % 73.03/10.58 % (3406063)Termination reason: Inappropriate % 73.03/10.58 % (3406063)Time elapsed: 0.002 s % 73.03/10.58 % (3406063)Peak memory usage: 11 MB % 73.03/10.58 % (3406063)Instructions burned: 6 (million) % 73.03/10.58 % (3406063)------------------------------ % 73.03/10.58 % (3406063)------------------------------ % 73.03/10.58 % (3406065)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=62577024:i=22565:add=on:rawr=on_2980 on theBenchmark for (2980ds/22565Mi) % 73.03/10.58 % (3406041)Instruction limit reached! % 73.03/10.58 % (3406041)------------------------------ % 73.03/10.58 % (3406041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.03/10.58 % (3406041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.03/10.58 % (3406041)CaDiCaL version: 2.1.3 % 73.03/10.58 % (3406041)Termination reason: Instruction limit % 73.03/10.58 % (3406041)Termination phase: Saturation % 73.03/10.58 % (3406041)Time elapsed: 1.769 s % 73.03/10.58 % (3406041)Peak memory usage: 36 MB % 73.03/10.58 % (3406041)Instructions burned: 5114 (million) % 73.03/10.58 % (3406067)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1461987492:i=8173:av=off_2977 on theBenchmark for (2977ds/8173Mi) % 73.03/10.58 % (3406053)Instruction limit reached! % 73.73/10.64 % (3406053)------------------------------ % 73.73/10.64 % (3406053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.73/10.64 % (3406053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.73/10.64 % (3406053)CaDiCaL version: 2.1.3 % 73.73/10.64 % (3406053)Termination reason: Instruction limit % 73.73/10.64 % (3406053)Termination phase: Saturation % 73.73/10.64 % (3406053)Time elapsed: 1.377 s % 73.73/10.64 % (3406053)Peak memory usage: 72 MB % 73.73/10.64 % (3406053)Instructions burned: 4594 (million) % 73.73/10.64 % (3406069)dis+10_16:1_sil=16000:random_seed=2008863064:i=9155:fsr=off_2971 on theBenchmark for (2971ds/9155Mi) % 73.73/10.64 % (3406057)Instruction limit reached! % 73.73/10.64 % (3406057)------------------------------ % 73.73/10.64 % (3406057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.73/10.64 % (3406057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.73/10.64 % (3406057)CaDiCaL version: 2.1.3 % 73.73/10.64 % (3406057)Termination reason: Instruction limit % 73.73/10.64 % (3406057)Termination phase: Saturation % 73.73/10.64 % (3406057)Time elapsed: 1.416 s % 73.73/10.64 % (3406057)Peak memory usage: 43 MB % 73.73/10.64 % (3406057)Instructions burned: 5214 (million) % 73.73/10.64 % (3406071)ott-3_8_sil=64000:random_seed=847837422:i=20139:bs=on_2967 on theBenchmark for (2967ds/20139Mi) % 73.73/10.64 % (3406067)Instruction limit reached! % 73.73/10.64 % (3406067)------------------------------ % 73.73/10.64 % (3406067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.73/10.64 % (3406067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.73/10.64 % (3406067)CaDiCaL version: 2.1.3 % 73.73/10.64 % (3406067)Termination reason: Instruction limit % 73.73/10.64 % (3406067)Termination phase: Saturation % 73.73/10.64 % (3406067)Time elapsed: 2.802 s % 73.73/10.64 % (3406067)Peak memory usage: 70 MB % 73.73/10.64 % (3406067)Instructions burned: 8173 (million) % 73.73/10.64 % (3406073)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4066452724:fmbsr=2:i=32576_2949 on theBenchmark for (2949ds/32576Mi) % 73.73/10.64 % (3406073)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 73.73/10.64 % (3406073)Terminated due to inappropriate strategy. % 73.73/10.64 % (3406073)------------------------------ % 73.73/10.64 % (3406073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.73/10.64 % (3406073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.73/10.64 % (3406073)CaDiCaL version: 2.1.3 % 73.73/10.64 % (3406073)Termination reason: Inappropriate % 73.73/10.64 % (3406073)Time elapsed: 0.002 s % 73.73/10.64 % (3406073)Peak memory usage: 11 MB % 73.73/10.64 % (3406073)Instructions burned: 6 (million) % 73.73/10.64 % (3406073)------------------------------ % 73.73/10.64 % (3406073)------------------------------ % 73.73/10.64 % (3406075)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1857061805:i=11404_2949 on theBenchmark for (2949ds/11404Mi) % 73.73/10.64 % (3406069)Instruction limit reached! % 73.73/10.64 % (3406069)------------------------------ % 73.73/10.64 % (3406069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.73/10.64 % (3406069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.73/10.64 % (3406069)CaDiCaL version: 2.1.3 % 73.73/10.64 % (3406069)Termination reason: Instruction limit % 73.73/10.64 % (3406069)Termination phase: Saturation % 73.73/10.64 % (3406069)Time elapsed: 2.569 s % 73.73/10.64 % (3406069)Peak memory usage: 55 MB % 73.73/10.64 % (3406069)Instructions burned: 9156 (million) % 73.73/10.64 % (3406077)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1197133650:i=14134_2946 on theBenchmark for (2946ds/14134Mi) % 73.73/10.64 % (3406065)Instruction limit reached! % 73.73/10.64 % (3406065)------------------------------ % 73.73/10.64 % (3406065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.73/10.64 % (3406065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.73/10.64 % (3406065)CaDiCaL version: 2.1.3 % 73.73/10.64 % (3406065)Termination reason: Instruction limit % 73.73/10.64 % (3406065)Termination phase: Saturation % 73.73/10.64 % (3406065)Time elapsed: 5.295 s % 73.73/10.64 % (3406065)Peak memory usage: 69 MB % 73.73/10.64 % (3406065)Instructions burned: 22565 (million) % 73.73/10.64 % (3406079)dis+33_16_sil=32000:sac=on:random_seed=3245310016:i=15851:nm=0_2927 on theBenchmark for (2927ds/15851Mi) % 73.73/10.64 % (3406055)Instruction limit reached! % 73.73/10.64 % (3406055)------------------------------ % 73.73/10.64 % (3406055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.43/13.17 % (3406055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.43/13.17 % (3406055)CaDiCaL version: 2.1.3 % 91.43/13.17 % (3406055)Termination reason: Instruction limit % 91.43/13.17 % (3406055)Termination phase: Saturation % 91.43/13.17 % (3406055)Time elapsed: 6.655 s % 91.43/13.17 % (3406055)Peak memory usage: 173 MB % 91.43/13.17 % (3406055)Instructions burned: 29340 (million) % 91.43/13.17 % (3406081)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=683241910:avsq=on:i=17627:add=on:amm=off_2916 on theBenchmark for (2916ds/17627Mi) % 91.43/13.17 % (3406075)Instruction limit reached! % 91.43/13.17 % (3406075)------------------------------ % 91.43/13.17 % (3406075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.43/13.17 % (3406075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.43/13.17 % (3406075)CaDiCaL version: 2.1.3 % 91.43/13.17 % (3406075)Termination reason: Instruction limit % 91.43/13.17 % (3406075)Termination phase: Saturation % 91.43/13.17 % (3406075)Time elapsed: 3.999 s % 91.43/13.17 % (3406075)Peak memory usage: 72 MB % 91.43/13.17 % (3406075)Instructions burned: 11404 (million) % 91.43/13.17 % (3406083)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=314280980:s2a=on:i=53295_2909 on theBenchmark for (2909ds/53295Mi) % 91.43/13.17 % (3406071)Instruction limit reached! % 91.43/13.17 % (3406071)------------------------------ % 91.43/13.17 % (3406071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.43/13.17 % (3406071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.43/13.17 % (3406071)CaDiCaL version: 2.1.3 % 91.43/13.17 % (3406071)Termination reason: Instruction limit % 91.43/13.17 % (3406071)Termination phase: Saturation % 91.43/13.17 % (3406071)Time elapsed: 6.487 s % 91.43/13.17 % (3406071)Peak memory usage: 86 MB % 91.43/13.17 % (3406071)Instructions burned: 20142 (million) % 91.43/13.17 % (3406085)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=660158149:i=26857:ins=20_2902 on theBenchmark for (2902ds/26857Mi) % 91.43/13.17 % (3406085)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 91.43/13.17 % (3406085)Terminated due to inappropriate strategy. % 91.43/13.17 % (3406085)------------------------------ % 91.43/13.17 % (3406085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.43/13.17 % (3406085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.43/13.17 % (3406085)CaDiCaL version: 2.1.3 % 91.43/13.17 % (3406085)Termination reason: Inappropriate % 91.43/13.17 % (3406085)Time elapsed: 0.002 s % 91.43/13.17 % (3406085)Peak memory usage: 10 MB % 91.43/13.17 % (3406085)Instructions burned: 5 (million) % 91.43/13.17 % (3406085)------------------------------ % 91.43/13.17 % (3406085)------------------------------ % 91.43/13.17 % (3406087)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=319015318:i=28120:bs=on:fsr=off_2902 on theBenchmark for (2902ds/28120Mi) % 91.43/13.17 % (3406077)Instruction limit reached! % 91.43/13.17 % (3406077)------------------------------ % 91.43/13.17 % (3406077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.43/13.17 % (3406077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.43/13.17 % (3406077)CaDiCaL version: 2.1.3 % 91.43/13.17 % (3406077)Termination reason: Instruction limit % 91.43/13.17 % (3406077)Termination phase: Saturation % 91.43/13.17 % (3406077)Time elapsed: 5.008 s % 91.43/13.17 % (3406077)Peak memory usage: 87 MB % 91.43/13.17 % (3406077)Instructions burned: 14134 (million) % 91.43/13.17 % (3406089)fmb+10_1_sil=256000:fmbss=7:random_seed=2668505820:fmbsr=1.6:i=182295_2895 on theBenchmark for (2895ds/182295Mi) % 91.43/13.17 % (3406089)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 91.43/13.17 % (3406089)Terminated due to inappropriate strategy. % 91.43/13.17 % (3406089)------------------------------ % 91.43/13.17 % (3406089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.43/13.17 % (3406089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.43/13.17 % (3406089)CaDiCaL version: 2.1.3 % 91.43/13.17 % (3406089)Termination reason: Inappropriate % 91.43/13.17 % (3406089)Time elapsed: 0.002 s % 91.43/13.17 % (3406089)Peak memory usage: 10 MB % 91.43/13.17 % (3406089)Instructions burned: 5 (million) % 91.43/13.17 % (3406089)------------------------------ % 91.43/13.17 % (3406089)------------------------------ % 91.43/13.17 % (3406091)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3470863371:i=44625:gsp=on_2895 on theBenchmark for (2895ds/44625Mi) % 99.13/14.25 % (3406091)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 99.13/14.25 % (3406091)Terminated due to inappropriate strategy. % 99.13/14.25 % (3406091)------------------------------ % 99.13/14.25 % (3406091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.13/14.25 % (3406091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.13/14.25 % (3406091)CaDiCaL version: 2.1.3 % 99.13/14.25 % (3406091)Termination reason: Inappropriate % 99.13/14.25 % (3406091)Time elapsed: 0.002 s % 99.13/14.25 % (3406091)Peak memory usage: 11 MB % 99.13/14.25 % (3406091)Instructions burned: 6 (million) % 99.13/14.25 % (3406091)------------------------------ % 99.13/14.25 % (3406091)------------------------------ % 99.13/14.25 % (3406093)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2172036562:i=160505_2895 on theBenchmark for (2895ds/160505Mi) % 99.13/14.25 % (3406093)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 99.13/14.25 % (3406093)Terminated due to inappropriate strategy. % 99.13/14.25 % (3406093)------------------------------ % 99.13/14.25 % (3406093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.13/14.25 % (3406093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.13/14.25 % (3406093)CaDiCaL version: 2.1.3 % 99.13/14.25 % (3406093)Termination reason: Inappropriate % 99.13/14.25 % (3406093)Time elapsed: 0.001 s % 99.13/14.25 % (3406093)Peak memory usage: 10 MB % 99.13/14.25 % (3406093)Instructions burned: 5 (million) % 99.13/14.25 % (3406093)------------------------------ % 99.13/14.25 % (3406093)------------------------------ % 99.13/14.25 % (3406095)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1288940744:fmbsr=1.3:i=225729_2895 on theBenchmark for (2895ds/225729Mi) % 99.13/14.25 % (3406095)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 99.13/14.25 % (3406095)Terminated due to inappropriate strategy. % 99.13/14.25 % (3406095)------------------------------ % 99.13/14.25 % (3406095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.13/14.25 % (3406095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.13/14.25 % (3406095)CaDiCaL version: 2.1.3 % 99.13/14.25 % (3406095)Termination reason: Inappropriate % 99.13/14.25 % (3406095)Time elapsed: 0.002 s % 99.13/14.25 % (3406095)Peak memory usage: 11 MB % 99.13/14.25 % (3406095)Instructions burned: 6 (million) % 99.13/14.25 % (3406095)------------------------------ % 99.13/14.25 % (3406095)------------------------------ % 99.13/14.25 % (3406097)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1062935802:fmbsr=2:i=185024:ins=7_2895 on theBenchmark for (2895ds/185024Mi) % 99.13/14.25 % (3406097)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 99.13/14.25 % (3406097)Terminated due to inappropriate strategy. % 99.13/14.25 % (3406097)------------------------------ % 99.13/14.25 % (3406097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.13/14.25 % (3406097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.13/14.25 % (3406097)CaDiCaL version: 2.1.3 % 99.13/14.25 % (3406097)Termination reason: Inappropriate % 99.13/14.25 % (3406097)Time elapsed: 0.002 s % 99.13/14.25 % (3406097)Peak memory usage: 11 MB % 99.13/14.25 % (3406097)Instructions burned: 6 (million) % 99.13/14.25 % (3406097)------------------------------ % 99.13/14.25 % (3406097)------------------------------ % 99.13/14.25 % (3406099)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2458997354:rtra=on_2895 on theBenchmark for (2895ds/0Mi) % 99.13/14.25 % (3406099)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 99.13/14.25 % (3406099)Terminated due to inappropriate strategy. % 99.13/14.25 % (3406099)------------------------------ % 99.13/14.25 % (3406099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.13/14.25 % (3406099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.13/14.25 % (3406099)CaDiCaL version: 2.1.3 % 99.13/14.25 % (3406099)Termination reason: Inappropriate % 99.13/14.25 % (3406099)Time elapsed: 0.002 s % 99.13/14.25 % (3406099)Peak memory usage: 11 MB % 99.13/14.25 % (3406099)Instructions burned: 7 (million) % 99.13/14.25 % (3406099)------------------------------ % 99.13/14.25 % (3406099)------------------------------ % 99.13/14.25 % (3406101)% WARNING: option uhcvi not known. % 99.13/14.25 % (3406101)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2816558780:i=271062:add=off:rtra=on:rawr=on_2894 on theBenchmark for (2894ds/271062Mi) % 112.64/16.17 % (3406079)Instruction limit reached! % 112.64/16.17 % (3406079)------------------------------ % 112.64/16.17 % (3406079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.64/16.17 % (3406079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.64/16.17 % (3406079)CaDiCaL version: 2.1.3 % 112.64/16.17 % (3406079)Termination reason: Instruction limit % 112.64/16.17 % (3406079)Termination phase: Saturation % 112.64/16.17 % (3406079)Time elapsed: 3.759 s % 112.64/16.17 % (3406079)Peak memory usage: 210 MB % 112.64/16.17 % (3406079)Instructions burned: 15854 (million) % 112.64/16.17 % (3406103)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1042538759:i=176048:add=on:rtra=on:rawr=on_2889 on theBenchmark for (2889ds/176048Mi) % 112.64/16.17 % (3406081)Instruction limit reached! % 112.64/16.17 % (3406081)------------------------------ % 112.64/16.17 % (3406081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.64/16.17 % (3406081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.64/16.17 % (3406081)CaDiCaL version: 2.1.3 % 112.64/16.17 % (3406081)Termination reason: Instruction limit % 112.64/16.17 % (3406081)Termination phase: Saturation % 112.64/16.17 % (3406081)Time elapsed: 4.305 s % 112.64/16.17 % (3406081)Peak memory usage: 88 MB % 112.64/16.17 % (3406081)Instructions burned: 17631 (million) % 112.64/16.17 % (3406105)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2692529151:i=206:fgj=on:rtra=on_2873 on theBenchmark for (2873ds/206Mi) % 112.64/16.17 % (3406105)Instruction limit reached! % 112.64/16.17 % (3406105)------------------------------ % 112.64/16.17 % (3406105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.64/16.17 % (3406105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.64/16.17 % (3406105)CaDiCaL version: 2.1.3 % 112.64/16.17 % (3406105)Termination reason: Instruction limit % 112.64/16.17 % (3406105)Termination phase: Saturation % 112.64/16.17 % (3406105)Time elapsed: 0.072 s % 112.64/16.17 % (3406105)Peak memory usage: 13 MB % 112.64/16.17 % (3406105)Instructions burned: 207 (million) % 112.64/16.17 % (3406107)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3200774044:i=232:rtra=on_2872 on theBenchmark for (2872ds/232Mi) % 112.64/16.17 % (3406107)Instruction limit reached! % 112.64/16.17 % (3406107)------------------------------ % 112.64/16.17 % (3406107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.64/16.17 % (3406107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.64/16.17 % (3406107)CaDiCaL version: 2.1.3 % 112.64/16.17 % (3406107)Termination reason: Instruction limit % 112.64/16.17 % (3406107)Termination phase: Saturation % 112.64/16.17 % (3406107)Time elapsed: 0.081 s % 112.64/16.17 % (3406107)Peak memory usage: 14 MB % 112.64/16.17 % (3406107)Instructions burned: 233 (million) % 112.64/16.17 % (3406109)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1944396658:i=262:rtra=on_2871 on theBenchmark for (2871ds/262Mi) % 112.64/16.17 % (3406109)Instruction limit reached! % 112.64/16.17 % (3406109)------------------------------ % 112.64/16.17 % (3406109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.64/16.17 % (3406109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.64/16.17 % (3406109)CaDiCaL version: 2.1.3 % 112.64/16.17 % (3406109)Termination reason: Instruction limit % 112.64/16.17 % (3406109)Termination phase: Saturation % 112.64/16.17 % (3406109)Time elapsed: 0.092 s % 112.64/16.17 % (3406109)Peak memory usage: 15 MB % 112.64/16.17 % (3406109)Instructions burned: 264 (million) % 112.64/16.17 % (3406111)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1153141470:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2870 on theBenchmark for (2870ds/318Mi) % 112.64/16.17 % (3406111)Instruction limit reached! % 112.64/16.17 % (3406111)------------------------------ % 112.64/16.17 % (3406111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.64/16.17 % (3406111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.64/16.17 % (3406111)CaDiCaL version: 2.1.3 % 112.64/16.17 % (3406111)Termination reason: Instruction limit % 112.64/16.17 % (3406111)Termination phase: Saturation % 112.64/16.17 % (3406111)Time elapsed: 0.096 s % 112.64/16.17 % (3406111)Peak memory usage: 16 MB % 112.64/16.17 % (3406111)Instructions burned: 319 (million) % 112.64/16.17 % (3406113)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=836861559:i=1428:nm=2:rtra=on_2869 on theBenchmark for (2869ds/1428Mi) % 123.09/17.65 % (3406113)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.09/17.65 % (3406113)Terminated due to inappropriate strategy. % 123.09/17.65 % (3406113)------------------------------ % 123.09/17.65 % (3406113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.09/17.65 % (3406113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.09/17.65 % (3406113)CaDiCaL version: 2.1.3 % 123.09/17.65 % (3406113)Termination reason: Inappropriate % 123.09/17.65 % (3406113)Time elapsed: 0.002 s % 123.09/17.65 % (3406113)Peak memory usage: 10 MB % 123.09/17.65 % (3406113)Instructions burned: 6 (million) % 123.09/17.65 % (3406113)------------------------------ % 123.09/17.65 % (3406113)------------------------------ % 123.09/17.65 % (3406115)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=19055313:i=262:bd=preordered:rtra=on:fsd=on_2869 on theBenchmark for (2869ds/262Mi) % 123.09/17.65 % (3406115)Instruction limit reached! % 123.09/17.65 % (3406115)------------------------------ % 123.09/17.65 % (3406115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.09/17.65 % (3406115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.09/17.65 % (3406115)CaDiCaL version: 2.1.3 % 123.09/17.65 % (3406115)Termination reason: Instruction limit % 123.09/17.65 % (3406115)Termination phase: Saturation % 123.09/17.65 % (3406115)Time elapsed: 0.100 s % 123.09/17.65 % (3406115)Peak memory usage: 15 MB % 123.09/17.65 % (3406115)Instructions burned: 264 (million) % 123.09/17.65 % (3406117)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=2162364977:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2868 on theBenchmark for (2868ds/1368Mi) % 123.09/17.65 % (3406117)Instruction limit reached! % 123.09/17.65 % (3406117)------------------------------ % 123.09/17.65 % (3406117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.09/17.65 % (3406117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.09/17.65 % (3406117)CaDiCaL version: 2.1.3 % 123.09/17.65 % (3406117)Termination reason: Instruction limit % 123.09/17.65 % (3406117)Termination phase: Saturation % 123.09/17.65 % (3406117)Time elapsed: 0.479 s % 123.09/17.65 % (3406117)Peak memory usage: 23 MB % 123.09/17.65 % (3406117)Instructions burned: 1370 (million) % 123.09/17.65 % (3406119)ott-21_1_sil=16000:si=on:fs=off:random_seed=1979989907:i=360:av=off:fsr=off:rtra=on_2863 on theBenchmark for (2863ds/360Mi) % 123.09/17.65 % (3406119)Instruction limit reached! % 123.09/17.65 % (3406119)------------------------------ % 123.09/17.65 % (3406119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.09/17.65 % (3406119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.09/17.65 % (3406119)CaDiCaL version: 2.1.3 % 123.09/17.65 % (3406119)Termination reason: Instruction limit % 123.09/17.65 % (3406119)Termination phase: Saturation % 123.09/17.65 % (3406119)Time elapsed: 0.095 s % 123.09/17.65 % (3406119)Peak memory usage: 13 MB % 123.09/17.65 % (3406119)Instructions burned: 363 (million) % 123.09/17.65 % (3406121)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4277211923:i=954:bd=all:rtra=on_2862 on theBenchmark for (2862ds/954Mi) % 123.09/17.65 % (3406121)Instruction limit reached! % 123.09/17.65 % (3406121)------------------------------ % 123.09/17.65 % (3406121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.09/17.65 % (3406121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.09/17.65 % (3406121)CaDiCaL version: 2.1.3 % 123.09/17.65 % (3406121)Termination reason: Instruction limit % 123.09/17.65 % (3406121)Termination phase: Saturation % 123.09/17.65 % (3406121)Time elapsed: 0.341 s % 123.09/17.65 % (3406121)Peak memory usage: 16 MB % 123.09/17.65 % (3406121)Instructions burned: 957 (million) % 123.09/17.65 % (3406124)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3024671964:fmbsr=1.3:i=1730:ins=25:rtra=on_2858 on theBenchmark for (2858ds/1730Mi) % 123.09/17.65 % (3406124)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.09/17.65 % (3406124)Terminated due to inappropriate strategy. % 123.09/17.65 % (3406124)------------------------------ % 123.09/17.65 % (3406124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.09/17.65 % (3406124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.09/17.65 % (3406124)CaDiCaL version: 2.1.3 % 123.09/17.65 % (3406124)Termination reason: Inappropriate % 123.09/17.65 % (3406124)Time elapsed: 0.002 s % 149.89/21.49 % (3406124)Peak memory usage: 10 MB % 149.89/21.49 % (3406124)Instructions burned: 6 (million) % 149.89/21.49 % (3406124)------------------------------ % 149.89/21.49 % (3406124)------------------------------ % 149.89/21.49 % (3406126)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2711657519:i=2358:rtra=on_2858 on theBenchmark for (2858ds/2358Mi) % 149.89/21.49 % (3406126)Instruction limit reached! % 149.89/21.49 % (3406126)------------------------------ % 149.89/21.49 % (3406126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.89/21.49 % (3406126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.89/21.49 % (3406126)CaDiCaL version: 2.1.3 % 149.89/21.49 % (3406126)Termination reason: Instruction limit % 149.89/21.49 % (3406126)Termination phase: Saturation % 149.89/21.49 % (3406126)Time elapsed: 0.839 s % 149.89/21.49 % (3406126)Peak memory usage: 30 MB % 149.89/21.49 % (3406126)Instructions burned: 2359 (million) % 149.89/21.49 % (3406173)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2100569202:i=1778:ins=1:rtra=on_2850 on theBenchmark for (2850ds/1778Mi) % 149.89/21.49 % (3406173)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.89/21.49 % (3406173)Terminated due to inappropriate strategy. % 149.89/21.49 % (3406173)------------------------------ % 149.89/21.49 % (3406173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.89/21.49 % (3406173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.89/21.49 % (3406173)CaDiCaL version: 2.1.3 % 149.89/21.49 % (3406173)Termination reason: Inappropriate % 149.89/21.49 % (3406173)Time elapsed: 0.002 s % 149.89/21.49 % (3406173)Peak memory usage: 10 MB % 149.89/21.49 % (3406173)Instructions burned: 6 (million) % 149.89/21.49 % (3406173)------------------------------ % 149.89/21.49 % (3406173)------------------------------ % 149.89/21.49 % (3406175)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=1419558142:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2850 on theBenchmark for (2850ds/1384Mi) % 149.89/21.49 % (3406175)Instruction limit reached! % 149.89/21.49 % (3406175)------------------------------ % 149.89/21.49 % (3406175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.89/21.49 % (3406175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.89/21.49 % (3406175)CaDiCaL version: 2.1.3 % 149.89/21.49 % (3406175)Termination reason: Instruction limit % 149.89/21.49 % (3406175)Termination phase: Saturation % 149.89/21.49 % (3406175)Time elapsed: 0.457 s % 149.89/21.49 % (3406175)Peak memory usage: 25 MB % 149.89/21.49 % (3406175)Instructions burned: 1386 (million) % 149.89/21.49 % (3406177)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=4011910348:i=1758:kws=inv_precedence:fsr=off:rtra=on_2845 on theBenchmark for (2845ds/1758Mi) % 149.89/21.49 % (3406177)Instruction limit reached! % 149.89/21.49 % (3406177)------------------------------ % 149.89/21.49 % (3406177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.89/21.49 % (3406177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.89/21.49 % (3406177)CaDiCaL version: 2.1.3 % 149.89/21.49 % (3406177)Termination reason: Instruction limit % 149.89/21.49 % (3406177)Termination phase: Saturation % 149.89/21.49 % (3406177)Time elapsed: 0.549 s % 149.89/21.49 % (3406177)Peak memory usage: 27 MB % 149.89/21.49 % (3406177)Instructions burned: 1759 (million) % 149.89/21.49 % (3406179)fmb+10_1_sil=64000:si=on:random_seed=2568145765:i=44122:nm=2:rtra=on:gsp=on_2839 on theBenchmark for (2839ds/44122Mi) % 149.89/21.49 % (3406179)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.89/21.49 % (3406179)Terminated due to inappropriate strategy. % 149.89/21.49 % (3406179)------------------------------ % 149.89/21.49 % (3406179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.89/21.49 % (3406179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.89/21.49 % (3406179)CaDiCaL version: 2.1.3 % 149.89/21.49 % (3406179)Termination reason: Inappropriate % 149.89/21.49 % (3406179)Time elapsed: 0.002 s % 149.89/21.49 % (3406179)Peak memory usage: 10 MB % 149.89/21.49 % (3406179)Instructions burned: 6 (million) % 149.89/21.49 % (3406179)------------------------------ % 149.89/21.49 % (3406179)------------------------------ % 149.89/21.49 % (3406181)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=127730526:i=19030:nm=5:rtra=on_2839 on theBenchmark for (2839ds/19030Mi) % 158.11/22.89 % (3406181)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.11/22.89 % (3406181)Terminated due to inappropriate strategy. % 158.11/22.89 % (3406181)------------------------------ % 158.11/22.89 % (3406181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.11/22.89 % (3406181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.11/22.89 % (3406181)CaDiCaL version: 2.1.3 % 158.11/22.89 % (3406181)Termination reason: Inappropriate % 158.11/22.89 % (3406181)Time elapsed: 0.002 s % 158.11/22.89 % (3406181)Peak memory usage: 10 MB % 158.11/22.89 % (3406181)Instructions burned: 6 (million) % 158.11/22.89 % (3406181)------------------------------ % 158.11/22.89 % (3406181)------------------------------ % 158.11/22.89 % (3406183)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3678888982:fmbsr=1.7:i=1840:rtra=on_2839 on theBenchmark for (2839ds/1840Mi) % 158.11/22.89 % (3406183)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.11/22.89 % (3406183)Terminated due to inappropriate strategy. % 158.11/22.89 % (3406183)------------------------------ % 158.11/22.89 % (3406183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.11/22.89 % (3406183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.11/22.89 % (3406183)CaDiCaL version: 2.1.3 % 158.11/22.89 % (3406183)Termination reason: Inappropriate % 158.11/22.89 % (3406183)Time elapsed: 0.002 s % 158.11/22.89 % (3406183)Peak memory usage: 10 MB % 158.11/22.89 % (3406183)Instructions burned: 6 (million) % 158.11/22.89 % (3406183)------------------------------ % 158.11/22.89 % (3406183)------------------------------ % 158.11/22.89 % (3406185)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=4226567651:i=10262:rtra=on_2839 on theBenchmark for (2839ds/10262Mi) % 158.11/22.89 % (3406087)Instruction limit reached! % 158.11/22.89 % (3406087)------------------------------ % 158.11/22.89 % (3406087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.11/22.89 % (3406087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.11/22.89 % (3406087)CaDiCaL version: 2.1.3 % 158.11/22.89 % (3406087)Termination reason: Instruction limit % 158.11/22.89 % (3406087)Termination phase: Saturation % 158.11/22.89 % (3406087)Time elapsed: 7.015 s % 158.11/22.89 % (3406087)Peak memory usage: 38 MB % 158.11/22.89 % (3406087)Instructions burned: 28122 (million) % 158.11/22.89 % (3406187)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3656127777:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2831 on theBenchmark for (2831ds/2944Mi) % 158.11/22.89 % (3406187)Instruction limit reached! % 158.11/22.89 % (3406187)------------------------------ % 158.11/22.89 % (3406187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.11/22.89 % (3406187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.11/22.89 % (3406187)CaDiCaL version: 2.1.3 % 158.11/22.89 % (3406187)Termination reason: Instruction limit % 158.11/22.89 % (3406187)Termination phase: Saturation % 158.11/22.89 % (3406187)Time elapsed: 0.666 s % 158.11/22.89 % (3406187)Peak memory usage: 16 MB % 158.11/22.89 % (3406187)Instructions burned: 2947 (million) % 158.11/22.89 % (3406189)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=971897885:i=12648:rtra=on_2825 on theBenchmark for (2825ds/12648Mi) % 158.11/22.89 % (3406189)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.11/22.89 % (3406189)Terminated due to inappropriate strategy. % 158.11/22.89 % (3406189)------------------------------ % 158.11/22.89 % (3406189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.11/22.89 % (3406189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.11/22.89 % (3406189)CaDiCaL version: 2.1.3 % 158.11/22.89 % (3406189)Termination reason: Inappropriate % 158.11/22.89 % (3406189)Time elapsed: 0.002 s % 158.11/22.89 % (3406189)Peak memory usage: 11 MB % 158.11/22.89 % (3406189)Instructions burned: 7 (million) % 158.11/22.89 % (3406189)------------------------------ % 158.11/22.89 % (3406189)------------------------------ % 158.11/22.89 % (3406191)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2259224954:fmbsr=2.30978:i=4348:rtra=on_2824 on theBenchmark for (2824ds/4348Mi) % 158.11/22.89 % (3406191)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.11/22.89 % (3406191)Terminated due to inappropriate strategy. % 158.11/22.89 % (3406191)------------------------------ % 158.11/22.89 % (3406191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.81/31.62 % (3406191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.81/31.62 % (3406191)CaDiCaL version: 2.1.3 % 221.81/31.62 % (3406191)Termination reason: Inappropriate % 221.81/31.62 % (3406191)Time elapsed: 0.002 s % 221.81/31.62 % (3406191)Peak memory usage: 10 MB % 221.81/31.62 % (3406191)Instructions burned: 6 (million) % 221.81/31.62 % (3406191)------------------------------ % 221.81/31.62 % (3406191)------------------------------ % 221.81/31.62 % (3406193)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=4020226249:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2824 on theBenchmark for (2824ds/1738Mi) % 221.81/31.62 % (3406193)Instruction limit reached! % 221.81/31.62 % (3406193)------------------------------ % 221.81/31.62 % (3406193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.81/31.62 % (3406193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.81/31.62 % (3406193)CaDiCaL version: 2.1.3 % 221.81/31.62 % (3406193)Termination reason: Instruction limit % 221.81/31.62 % (3406193)Termination phase: Saturation % 221.81/31.62 % (3406193)Time elapsed: 0.617 s % 221.81/31.62 % (3406193)Peak memory usage: 23 MB % 221.81/31.62 % (3406193)Instructions burned: 1738 (million) % 221.81/31.62 % (3406195)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=105244436:i=10228:av=off:rtra=on_2818 on theBenchmark for (2818ds/10228Mi) % 221.81/31.62 % (3405993)Instruction limit reached! % 221.81/31.62 % (3405993)------------------------------ % 221.81/31.62 % (3405993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.81/31.62 % (3405993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.81/31.62 % (3405993)CaDiCaL version: 2.1.3 % 221.81/31.62 % (3405993)Termination reason: Instruction limit % 221.81/31.62 % (3405993)Termination phase: Saturation % 221.81/31.62 % (3405993)Time elapsed: 18.961 s % 221.81/31.62 % (3405993)Peak memory usage: 272 MB % 221.81/31.62 % (3405993)Instructions burned: 88026 (million) % 221.81/31.62 % (3406197)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1523656045:i=108564:rtra=on_2809 on theBenchmark for (2809ds/108564Mi) % 221.81/31.62 % (3406197)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 221.81/31.62 % (3406197)Terminated due to inappropriate strategy. % 221.81/31.62 % (3406197)------------------------------ % 221.81/31.62 % (3406197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.81/31.62 % (3406197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.81/31.62 % (3406197)CaDiCaL version: 2.1.3 % 221.81/31.62 % (3406197)Termination reason: Inappropriate % 221.81/31.62 % (3406197)Time elapsed: 0.002 s % 221.81/31.62 % (3406197)Peak memory usage: 11 MB % 221.81/31.62 % (3406197)Instructions burned: 7 (million) % 221.81/31.62 % (3406197)------------------------------ % 221.81/31.62 % (3406197)------------------------------ % 221.81/31.62 % (3406199)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1188252045:i=7024:aac=none:rtra=on_2809 on theBenchmark for (2809ds/7024Mi) % 221.81/31.62 % (3406185)Instruction limit reached! % 221.81/31.62 % (3406185)------------------------------ % 221.81/31.62 % (3406185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.81/31.62 % (3406185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.81/31.62 % (3406185)CaDiCaL version: 2.1.3 % 221.81/31.62 % (3406185)Termination reason: Instruction limit % 221.81/31.62 % (3406185)Termination phase: Saturation % 221.81/31.62 % (3406185)Time elapsed: 3.356 s % 221.81/31.62 % (3406185)Peak memory usage: 69 MB % 221.81/31.62 % (3406185)Instructions burned: 10262 (million) % 221.81/31.62 % (3406201)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=2038537932:i=7546:rtra=on:amm=off_2805 on theBenchmark for (2805ds/7546Mi) % 221.81/31.62 % (3406199)Instruction limit reached! % 221.81/31.62 % (3406199)------------------------------ % 221.81/31.62 % (3406199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.81/31.62 % (3406199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.81/31.62 % (3406199)CaDiCaL version: 2.1.3 % 221.81/31.62 % (3406199)Termination reason: Instruction limit % 221.81/31.62 % (3406199)Termination phase: Saturation % 221.81/31.62 % (3406199)Time elapsed: 2.308 s % 221.81/31.62 % (3406199)Peak memory usage: 51 MB % 221.81/31.62 % (3406199)Instructions burned: 7027 (million) % 221.81/31.62 % (3406203)ott+11_1_sil=16000:si=on:gs=on:random_seed=3306686417:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2786 on theBenchmark for (2786ds/4502Mi) % 300.16/42.73 % (3406201)Instruction limit reached! % 300.16/42.73 % (3406201)------------------------------ % 300.16/42.73 % (3406201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.16/42.73 % (3406201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.16/42.73 % (3406201)CaDiCaL version: 2.1.3 % 300.16/42.73 % (3406201)Termination reason: Instruction limit % 300.16/42.73 % (3406201)Termination phase: Saturation % 300.16/42.73 % (3406201)Time elapsed: 2.435 s % 300.16/42.73 % (3406201)Peak memory usage: 51 MB % 300.16/42.73 % (3406201)Instructions burned: 7546 (million) % 300.16/42.73 % (3406205)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=210095054:fmbsr=1.6:i=135068:rtra=on_2781 on theBenchmark for (2781ds/135068Mi) % 300.16/42.73 % (3406205)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.16/42.73 % (3406205)Terminated due to inappropriate strategy. % 300.16/42.73 % (3406205)------------------------------ % 300.16/42.73 % (3406205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.16/42.73 % (3406205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.16/42.73 % (3406205)CaDiCaL version: 2.1.3 % 300.16/42.73 % (3406205)Termination reason: Inappropriate % 300.16/42.73 % (3406205)Time elapsed: 0.002 s % 300.16/42.73 % (3406205)Peak memory usage: 11 MB % 300.16/42.73 % (3406205)Instructions burned: 6 (million) % 300.16/42.73 % (3406205)------------------------------ % 300.16/42.73 % (3406205)------------------------------ % 300.16/42.73 % (3406207)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3016120171:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2781 on theBenchmark for (2781ds/9182Mi) % 300.16/42.73 % (3406195)Instruction limit reached! % 300.16/42.73 % (3406195)------------------------------ % 300.16/42.73 % (3406195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.16/42.73 % (3406195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.16/42.73 % (3406195)CaDiCaL version: 2.1.3 % 300.16/42.73 % (3406195)Termination reason: Instruction limit % 300.16/42.73 % (3406195)Termination phase: Saturation % 300.16/42.73 % (3406195)Time elapsed: 3.879 s % 300.16/42.73 % (3406195)Peak memory usage: 59 MB % 300.16/42.73 % (3406195)Instructions burned: 10228 (million) % 300.16/42.73 % (3406209)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=2787817351:i=58680:rtra=on_2779 on theBenchmark for (2779ds/58680Mi) % 300.16/42.73 % (3406083)Instruction limit reached! % 300.16/42.73 % (3406083)------------------------------ % 300.16/42.73 % (3406083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.16/42.73 % (3406083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.16/42.73 % (3406083)CaDiCaL version: 2.1.3 % 300.16/42.73 % (3406083)Termination reason: Instruction limit % 300.16/42.73 % (3406083)Termination phase: Saturation % 300.16/42.73 % (3406083)Time elapsed: 13.289 s % 300.16/42.73 % (3406083)Peak memory usage: 459 MB % 300.16/42.73 % (3406083)Instructions burned: 53297 (million) % 300.16/42.73 % (3406211)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=4038474736:i=10422:rtra=on_2776 on theBenchmark for (2776ds/10422Mi) % 300.16/42.73 % (3406203)Instruction limit reached! % 300.16/42.73 % (3406203)------------------------------ % 300.16/42.73 % (3406203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.16/42.73 % (3406203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.16/42.73 % (3406203)CaDiCaL version: 2.1.3 % 300.16/42.73 % (3406203)Termination reason: Instruction limit % 300.16/42.73 % (3406203)Termination phase: Saturation % 300.16/42.73 % (3406203)Time elapsed: 1.386 s % 300.16/42.73 % (3406203)Peak memory usage: 35 MB % 300.16/42.73 % (3406203)Instructions burned: 4505 (million) % 300.16/42.73 % (3406213)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=1119562833:i=10994:nm=2:rtra=on_2772 on theBenchmark for (2772ds/10994Mi) % 300.16/42.73 % (3406213)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.16/42.73 % (3406213)Terminated due to inappropriate strategy. % 300.16/42.73 % (3406213)------------------------------ % 300.16/42.73 % (3406213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.16/42.73 % (3406213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.16/42.73 % (3406213)CaDiCaL version: 2.1.3 % 300.16/42.73 % (3406213)Termination reason: Inappropriate % 300.16/42.73 % (3406213)Time elapsed: 0.002 s % 300.16/42.73 % Terminated % 300.16/42.74 % Vampire exiting %------------------------------------------------------------------------------