%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC430_1 : TPTP v9.3.1. Bugfixed v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/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:06:00 PM UTC 2026 % Result : Timeout 300.20s 42.73s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWC430_1 : TPTP v9.3.1. Bugfixed v9.1.0. % 0.00/0.02 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.00/0.10 % Computer : n012.cluster.edu % 0.00/0.10 % Model : x86_64 x86_64 % 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.10 % Memory : 8046.5625MB % 0.00/0.10 % OS : Linux 6.8.0-71-generic % 0.00/0.10 % CPULimit : 300 % 0.00/0.10 % WCLimit : 300 % 0.00/0.10 % DateTime : Mon Sep 28 09:36:49 UTC 2026 % 0.00/0.10 % CPUTime : % 0.00/0.10 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.11 Running first-order model finding % 0.08/0.12 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 % 2.13/0.46 % (3260751)Will run a generic schedule for satisfiability detection. % 2.13/0.46 % (3260757)% WARNING: option uhcvi not known. % 2.13/0.46 % (3260756)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=812722673_2999 on theBenchmark for (2999ds/0Mi) % 2.13/0.46 % (3260757)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1675503376:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.13/0.46 % (3260758)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1645056677:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.13/0.46 % (3260759)dis+10_1_sil=32000:sp=arity:random_seed=2719931298:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.13/0.46 % (3260760)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4033232277:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.13/0.46 % (3260761)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1072054991:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.13/0.46 % (3260762)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=973423864:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.13/0.46 % (3260756)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.13/0.46 % (3260756)Terminated due to inappropriate strategy. % 2.13/0.46 % (3260756)------------------------------ % 2.13/0.46 % (3260756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.13/0.46 % (3260756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.13/0.46 % (3260756)CaDiCaL version: 2.1.3 % 2.13/0.46 % (3260756)Termination reason: Inappropriate % 2.13/0.46 % (3260756)Time elapsed: 0.0000 s % 2.13/0.46 % (3260756)Peak memory usage: 10 MB % 2.13/0.46 % (3260756)Instructions burned: 1 (million) % 2.13/0.46 % (3260756)------------------------------ % 2.13/0.46 % (3260756)------------------------------ % 2.13/0.46 % (3260770)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=917933980:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.13/0.46 % (3260770)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.13/0.46 % (3260770)Terminated due to inappropriate strategy. % 2.13/0.46 % (3260770)------------------------------ % 2.13/0.46 % (3260770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.13/0.46 % (3260770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.13/0.46 % (3260770)CaDiCaL version: 2.1.3 % 2.13/0.46 % (3260770)Termination reason: Inappropriate % 2.13/0.46 % (3260770)Time elapsed: 0.0000 s % 2.13/0.46 % (3260770)Peak memory usage: 10 MB % 2.13/0.46 % (3260770)Instructions burned: 1 (million) % 2.13/0.46 % (3260770)------------------------------ % 2.13/0.46 % (3260770)------------------------------ % 2.13/0.46 % (3260772)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1903629142:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.13/0.46 % (3260759)Instruction limit reached! % 2.13/0.46 % (3260759)------------------------------ % 2.13/0.46 % (3260759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.13/0.46 % (3260759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.13/0.46 % (3260759)CaDiCaL version: 2.1.3 % 2.13/0.46 % (3260759)Termination reason: Instruction limit % 2.13/0.46 % (3260759)Termination phase: Saturation % 2.13/0.46 % (3260759)Time elapsed: 0.035 s % 2.13/0.46 % (3260759)Peak memory usage: 12 MB % 2.13/0.46 % (3260759)Instructions burned: 104 (million) % 2.13/0.46 % (3260760)Instruction limit reached! % 2.13/0.46 % (3260760)------------------------------ % 2.13/0.46 % (3260760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.13/0.46 % (3260760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.13/0.46 % (3260760)CaDiCaL version: 2.1.3 % 2.13/0.46 % (3260760)Termination reason: Instruction limit % 2.13/0.46 % (3260760)Termination phase: Saturation % 2.13/0.46 % (3260760)Time elapsed: 0.039 s % 2.13/0.46 % (3260760)Peak memory usage: 12 MB % 2.13/0.46 % (3260760)Instructions burned: 119 (million) % 2.13/0.46 % (3260761)Instruction limit reached! % 2.13/0.46 % (3260761)------------------------------ % 2.13/0.46 % (3260761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.13/0.46 % (3260761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.13/0.46 % (3260761)CaDiCaL version: 2.1.3 % 2.13/0.46 % (3260761)Termination reason: Instruction limit % 2.13/0.53 % (3260761)Termination phase: Saturation % 2.13/0.53 % (3260761)Time elapsed: 0.044 s % 2.13/0.53 % (3260761)Peak memory usage: 13 MB % 2.13/0.53 % (3260761)Instructions burned: 134 (million) % 2.13/0.53 % (3260774)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=738339753:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 2.13/0.53 % (3260775)ott-21_1_sil=16000:fs=off:random_seed=2088020249:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 2.13/0.53 % (3260776)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3565056889:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 2.13/0.53 % (3260762)Instruction limit reached! % 2.13/0.53 % (3260762)------------------------------ % 2.13/0.53 % (3260762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.13/0.53 % (3260762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.13/0.53 % (3260762)CaDiCaL version: 2.1.3 % 2.13/0.53 % (3260762)Termination reason: Instruction limit % 2.13/0.53 % (3260762)Termination phase: Saturation % 2.13/0.53 % (3260762)Time elapsed: 0.055 s % 2.13/0.53 % (3260762)Peak memory usage: 13 MB % 2.13/0.53 % (3260762)Instructions burned: 159 (million) % 2.13/0.53 % (3260780)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3095391678:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi) % 2.13/0.53 % (3260780)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.13/0.53 % (3260780)Terminated due to inappropriate strategy. % 2.13/0.53 % (3260780)------------------------------ % 2.13/0.53 % (3260780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.13/0.53 % (3260780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.13/0.53 % (3260780)CaDiCaL version: 2.1.3 % 2.13/0.53 % (3260780)Termination reason: Inappropriate % 2.13/0.53 % (3260780)Time elapsed: 0.0000 s % 2.13/0.53 % (3260780)Peak memory usage: 10 MB % 2.13/0.53 % (3260780)Instructions burned: 1 (million) % 2.13/0.53 % (3260780)------------------------------ % 2.13/0.53 % (3260780)------------------------------ % 2.13/0.53 % (3260772)Instruction limit reached! % 2.13/0.53 % (3260772)------------------------------ % 2.13/0.53 % (3260772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.13/0.53 % (3260772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.13/0.53 % (3260772)CaDiCaL version: 2.1.3 % 2.13/0.53 % (3260772)Termination reason: Instruction limit % 2.13/0.53 % (3260772)Termination phase: Saturation % 2.13/0.53 % (3260772)Time elapsed: 0.046 s % 2.13/0.53 % (3260772)Peak memory usage: 12 MB % 2.13/0.53 % (3260772)Instructions burned: 131 (million) % 2.13/0.53 % (3260782)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1678556316:i=1179_2999 on theBenchmark for (2999ds/1179Mi) % 2.13/0.53 % (3260783)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3845354798:i=889:ins=1_2999 on theBenchmark for (2999ds/889Mi) % 2.13/0.53 % (3260783)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.13/0.53 % (3260783)Terminated due to inappropriate strategy. % 2.13/0.53 % (3260783)------------------------------ % 2.13/0.53 % (3260783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.13/0.53 % (3260783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.13/0.53 % (3260783)CaDiCaL version: 2.1.3 % 2.13/0.53 % (3260783)Termination reason: Inappropriate % 2.13/0.53 % (3260783)Time elapsed: 0.0000 s % 2.13/0.53 % (3260783)Peak memory usage: 10 MB % 2.13/0.53 % (3260783)Instructions burned: 1 (million) % 2.13/0.53 % (3260783)------------------------------ % 2.13/0.53 % (3260783)------------------------------ % 2.13/0.53 % (3260786)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=3011952062: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) % 2.13/0.53 % (3260775)Instruction limit reached! % 2.13/0.53 % (3260775)------------------------------ % 2.13/0.53 % (3260775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.13/0.53 % (3260775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.13/0.53 % (3260775)CaDiCaL version: 2.1.3 % 2.13/0.53 % (3260775)Termination reason: Instruction limit % 2.13/0.53 % (3260775)Termination phase: Saturation % 11.27/1.87 % (3260775)Time elapsed: 0.043 s % 11.27/1.87 % (3260775)Peak memory usage: 12 MB % 11.27/1.87 % (3260775)Instructions burned: 181 (million) % 11.27/1.87 % (3260788)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=740441036:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 11.27/1.87 % (3260776)Instruction limit reached! % 11.27/1.87 % (3260776)------------------------------ % 11.27/1.87 % (3260776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.27/1.87 % (3260776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.27/1.87 % (3260776)CaDiCaL version: 2.1.3 % 11.27/1.87 % (3260776)Termination reason: Instruction limit % 11.27/1.87 % (3260776)Termination phase: Saturation % 11.27/1.87 % (3260776)Time elapsed: 0.163 s % 11.27/1.87 % (3260776)Peak memory usage: 14 MB % 11.27/1.87 % (3260776)Instructions burned: 477 (million) % 11.27/1.87 % (3260790)fmb+10_1_sil=64000:random_seed=3115410863:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 11.27/1.87 % (3260790)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.27/1.87 % (3260790)Terminated due to inappropriate strategy. % 11.27/1.87 % (3260790)------------------------------ % 11.27/1.87 % (3260790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.27/1.87 % (3260790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.27/1.87 % (3260790)CaDiCaL version: 2.1.3 % 11.27/1.87 % (3260790)Termination reason: Inappropriate % 11.27/1.87 % (3260790)Time elapsed: 0.0000 s % 11.27/1.87 % (3260790)Peak memory usage: 11 MB % 11.27/1.87 % (3260790)Instructions burned: 1 (million) % 11.27/1.87 % (3260790)------------------------------ % 11.27/1.87 % (3260790)------------------------------ % 11.27/1.87 % (3260792)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1127111402:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 11.27/1.87 % (3260792)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.27/1.87 % (3260792)Terminated due to inappropriate strategy. % 11.27/1.87 % (3260792)------------------------------ % 11.27/1.87 % (3260792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.27/1.87 % (3260792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.27/1.87 % (3260792)CaDiCaL version: 2.1.3 % 11.27/1.87 % (3260792)Termination reason: Inappropriate % 11.27/1.87 % (3260792)Time elapsed: 0.0000 s % 11.27/1.87 % (3260792)Peak memory usage: 10 MB % 11.27/1.87 % (3260792)Instructions burned: 1 (million) % 11.27/1.87 % (3260792)------------------------------ % 11.27/1.87 % (3260792)------------------------------ % 11.27/1.87 % (3260774)Instruction limit reached! % 11.27/1.87 % (3260774)------------------------------ % 11.27/1.87 % (3260774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.27/1.87 % (3260774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.27/1.87 % (3260774)CaDiCaL version: 2.1.3 % 11.27/1.87 % (3260774)Termination reason: Instruction limit % 11.27/1.87 % (3260774)Termination phase: Saturation % 11.27/1.87 % (3260774)Time elapsed: 0.202 s % 11.27/1.87 % (3260774)Peak memory usage: 16 MB % 11.27/1.87 % (3260774)Instructions burned: 688 (million) % 11.27/1.87 % (3260794)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2758734527:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 11.27/1.87 % (3260794)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.27/1.87 % (3260794)Terminated due to inappropriate strategy. % 11.27/1.87 % (3260794)------------------------------ % 11.27/1.87 % (3260794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.27/1.87 % (3260794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.27/1.87 % (3260794)CaDiCaL version: 2.1.3 % 11.27/1.87 % (3260794)Termination reason: Inappropriate % 11.27/1.87 % (3260794)Time elapsed: 0.0000 s % 11.27/1.87 % (3260794)Peak memory usage: 10 MB % 11.27/1.87 % (3260794)Instructions burned: 1 (million) % 11.27/1.87 % (3260794)------------------------------ % 11.27/1.87 % (3260794)------------------------------ % 11.27/1.87 % (3260795)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1650833916:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 11.27/1.87 % (3260797)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1697295986:i=1472:ins=7:fdi=8:gsp=on_2997 on theBenchmark for (2997ds/1472Mi) % 11.27/1.87 % (3260786)Instruction limit reached! % 11.27/1.87 % (3260786)------------------------------ % 17.66/2.76 % (3260786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.66/2.76 % (3260786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.66/2.76 % (3260786)CaDiCaL version: 2.1.3 % 17.66/2.76 % (3260786)Termination reason: Instruction limit % 17.66/2.76 % (3260786)Termination phase: Saturation % 17.66/2.76 % (3260786)Time elapsed: 0.224 s % 17.66/2.76 % (3260786)Peak memory usage: 17 MB % 17.66/2.76 % (3260786)Instructions burned: 693 (million) % 17.66/2.76 % (3260800)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3477305529:i=6324_2996 on theBenchmark for (2996ds/6324Mi) % 17.66/2.76 % (3260800)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.66/2.76 % (3260800)Terminated due to inappropriate strategy. % 17.66/2.76 % (3260800)------------------------------ % 17.66/2.76 % (3260800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.66/2.76 % (3260800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.66/2.76 % (3260800)CaDiCaL version: 2.1.3 % 17.66/2.76 % (3260800)Termination reason: Inappropriate % 17.66/2.76 % (3260800)Time elapsed: 0.0000 s % 17.66/2.76 % (3260800)Peak memory usage: 10 MB % 17.66/2.76 % (3260800)Instructions burned: 1 (million) % 17.66/2.76 % (3260800)------------------------------ % 17.66/2.76 % (3260800)------------------------------ % 17.66/2.76 % (3260802)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1325586732:fmbsr=2.30978:i=2174_2996 on theBenchmark for (2996ds/2174Mi) % 17.66/2.76 % (3260802)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.66/2.76 % (3260802)Terminated due to inappropriate strategy. % 17.66/2.76 % (3260802)------------------------------ % 17.66/2.76 % (3260802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.66/2.76 % (3260802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.66/2.76 % (3260802)CaDiCaL version: 2.1.3 % 17.66/2.76 % (3260802)Termination reason: Inappropriate % 17.66/2.76 % (3260802)Time elapsed: 0.0000 s % 17.66/2.76 % (3260802)Peak memory usage: 10 MB % 17.66/2.76 % (3260802)Instructions burned: 1 (million) % 17.66/2.76 % (3260802)------------------------------ % 17.66/2.76 % (3260802)------------------------------ % 17.66/2.76 % (3260804)ott-2_1_sil=16000:newcnf=on:random_seed=3689028837:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2996 on theBenchmark for (2996ds/869Mi) % 17.66/2.76 % (3260782)Instruction limit reached! % 17.66/2.76 % (3260782)------------------------------ % 17.66/2.76 % (3260782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.66/2.76 % (3260782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.66/2.76 % (3260782)CaDiCaL version: 2.1.3 % 17.66/2.76 % (3260782)Termination reason: Instruction limit % 17.66/2.76 % (3260782)Termination phase: Saturation % 17.66/2.76 % (3260782)Time elapsed: 0.284 s % 17.66/2.76 % (3260782)Peak memory usage: 17 MB % 17.66/2.76 % (3260782)Instructions burned: 1184 (million) % 17.66/2.76 % (3260788)Instruction limit reached! % 17.66/2.76 % (3260788)------------------------------ % 17.66/2.76 % (3260788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.66/2.76 % (3260788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.66/2.76 % (3260788)CaDiCaL version: 2.1.3 % 17.66/2.76 % (3260788)Termination reason: Instruction limit % 17.66/2.76 % (3260788)Termination phase: Saturation % 17.66/2.76 % (3260788)Time elapsed: 0.266 s % 17.66/2.76 % (3260788)Peak memory usage: 17 MB % 17.66/2.76 % (3260788)Instructions burned: 879 (million) % 17.66/2.76 % (3260806)ott+10_1_sil=32000:tgt=ground:random_seed=3674799969:i=5114:av=off_2996 on theBenchmark for (2996ds/5114Mi) % 17.66/2.76 % (3260807)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=72605311:i=54282_2996 on theBenchmark for (2996ds/54282Mi) % 17.66/2.76 % (3260807)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.66/2.76 % (3260807)Terminated due to inappropriate strategy. % 17.66/2.76 % (3260807)------------------------------ % 17.66/2.76 % (3260807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.66/2.76 % (3260807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.66/2.76 % (3260807)CaDiCaL version: 2.1.3 % 17.66/2.76 % (3260807)Termination reason: Inappropriate % 17.66/2.76 % (3260807)Time elapsed: 0.0000 s % 17.66/2.76 % (3260807)Peak memory usage: 11 MB % 17.66/2.76 % (3260807)Instructions burned: 1 (million) % 54.75/8.00 % (3260807)------------------------------ % 54.75/8.00 % (3260807)------------------------------ % 54.75/8.00 % (3260810)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=907995078:i=3512:aac=none_2995 on theBenchmark for (2995ds/3512Mi) % 54.75/8.00 % (3260804)Instruction limit reached! % 54.75/8.00 % (3260804)------------------------------ % 54.75/8.00 % (3260804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.75/8.00 % (3260804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.75/8.00 % (3260804)CaDiCaL version: 2.1.3 % 54.75/8.00 % (3260804)Termination reason: Instruction limit % 54.75/8.00 % (3260804)Termination phase: Saturation % 54.75/8.00 % (3260804)Time elapsed: 0.272 s % 54.75/8.00 % (3260804)Peak memory usage: 15 MB % 54.75/8.00 % (3260804)Instructions burned: 872 (million) % 54.75/8.00 % (3260812)dis+21_1_sil=32000:sas=cadical:random_seed=3632427485:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi) % 54.75/8.00 % (3260797)Instruction limit reached! % 54.75/8.00 % (3260797)------------------------------ % 54.75/8.00 % (3260797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.75/8.00 % (3260797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.75/8.00 % (3260797)CaDiCaL version: 2.1.3 % 54.75/8.00 % (3260797)Termination reason: Instruction limit % 54.75/8.00 % (3260797)Termination phase: Saturation % 54.75/8.00 % (3260797)Time elapsed: 0.499 s % 54.75/8.00 % (3260797)Peak memory usage: 26 MB % 54.75/8.00 % (3260797)Instructions burned: 1473 (million) % 54.75/8.00 % (3260814)ott+11_1_sil=16000:gs=on:random_seed=2485173819:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2992 on theBenchmark for (2992ds/2251Mi) % 54.75/8.00 % (3260810)Instruction limit reached! % 54.75/8.00 % (3260810)------------------------------ % 54.75/8.00 % (3260810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.75/8.00 % (3260810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.75/8.00 % (3260810)CaDiCaL version: 2.1.3 % 54.75/8.00 % (3260810)Termination reason: Instruction limit % 54.75/8.00 % (3260810)Termination phase: Saturation % 54.75/8.00 % (3260810)Time elapsed: 0.966 s % 54.75/8.00 % (3260810)Peak memory usage: 29 MB % 54.75/8.00 % (3260810)Instructions burned: 3513 (million) % 54.75/8.00 % (3260816)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2616318782:fmbsr=1.6:i=67534_2986 on theBenchmark for (2986ds/67534Mi) % 54.75/8.00 % (3260816)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 54.75/8.00 % (3260816)Terminated due to inappropriate strategy. % 54.75/8.00 % (3260816)------------------------------ % 54.75/8.00 % (3260816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.75/8.00 % (3260816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.75/8.00 % (3260816)CaDiCaL version: 2.1.3 % 54.75/8.00 % (3260816)Termination reason: Inappropriate % 54.75/8.00 % (3260816)Time elapsed: 0.0000 s % 54.75/8.00 % (3260816)Peak memory usage: 10 MB % 54.75/8.00 % (3260816)Instructions burned: 1 (million) % 54.75/8.00 % (3260816)------------------------------ % 54.75/8.00 % (3260816)------------------------------ % 54.75/8.00 % (3260818)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=542192317:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2986 on theBenchmark for (2986ds/4591Mi) % 54.75/8.00 % (3260814)Instruction limit reached! % 54.75/8.00 % (3260814)------------------------------ % 54.75/8.00 % (3260814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.75/8.00 % (3260814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.75/8.00 % (3260814)CaDiCaL version: 2.1.3 % 54.75/8.00 % (3260814)Termination reason: Instruction limit % 54.75/8.00 % (3260814)Termination phase: Saturation % 54.75/8.00 % (3260814)Time elapsed: 0.674 s % 54.75/8.00 % (3260814)Peak memory usage: 24 MB % 54.75/8.00 % (3260814)Instructions burned: 2252 (million) % 54.75/8.00 % (3260820)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1796144249:i=29340_2985 on theBenchmark for (2985ds/29340Mi) % 54.75/8.00 % (3260812)Instruction limit reached! % 54.75/8.00 % (3260812)------------------------------ % 54.75/8.00 % (3260812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.75/8.00 % (3260812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.75/8.00 % (3260812)CaDiCaL version: 2.1.3 % 54.75/8.00 % (3260812)Termination reason: Instruction limit % 70.98/10.21 % (3260812)Termination phase: Saturation % 70.98/10.21 % (3260812)Time elapsed: 1.090 s % 70.98/10.21 % (3260812)Peak memory usage: 31 MB % 70.98/10.21 % (3260812)Instructions burned: 3777 (million) % 70.98/10.21 % (3260822)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3723530107:i=5211_2982 on theBenchmark for (2982ds/5211Mi) % 70.98/10.21 % (3260795)Instruction limit reached! % 70.98/10.21 % (3260795)------------------------------ % 70.98/10.21 % (3260795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.98/10.21 % (3260795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.98/10.21 % (3260795)CaDiCaL version: 2.1.3 % 70.98/10.21 % (3260795)Termination reason: Instruction limit % 70.98/10.21 % (3260795)Termination phase: Saturation % 70.98/10.21 % (3260795)Time elapsed: 1.499 s % 70.98/10.21 % (3260795)Peak memory usage: 42 MB % 70.98/10.21 % (3260795)Instructions burned: 5134 (million) % 70.98/10.21 % (3260824)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3102795943:i=5497:nm=2_2982 on theBenchmark for (2982ds/5497Mi) % 70.98/10.21 % (3260824)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 70.98/10.21 % (3260824)Terminated due to inappropriate strategy. % 70.98/10.21 % (3260824)------------------------------ % 70.98/10.21 % (3260824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.98/10.21 % (3260824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.98/10.21 % (3260824)CaDiCaL version: 2.1.3 % 70.98/10.21 % (3260824)Termination reason: Inappropriate % 70.98/10.21 % (3260824)Time elapsed: 0.0000 s % 70.98/10.21 % (3260824)Peak memory usage: 10 MB % 70.98/10.21 % (3260824)Instructions burned: 1 (million) % 70.98/10.21 % (3260824)------------------------------ % 70.98/10.21 % (3260824)------------------------------ % 70.98/10.21 % (3260826)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3944171759:fmbsr=2:i=46332_2982 on theBenchmark for (2982ds/46332Mi) % 70.98/10.21 % (3260826)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 70.98/10.21 % (3260826)Terminated due to inappropriate strategy. % 70.98/10.21 % (3260826)------------------------------ % 70.98/10.21 % (3260826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.98/10.21 % (3260826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.98/10.21 % (3260826)CaDiCaL version: 2.1.3 % 70.98/10.21 % (3260826)Termination reason: Inappropriate % 70.98/10.21 % (3260826)Time elapsed: 0.0000 s % 70.98/10.21 % (3260826)Peak memory usage: 10 MB % 70.98/10.21 % (3260826)Instructions burned: 1 (million) % 70.98/10.21 % (3260826)------------------------------ % 70.98/10.21 % (3260826)------------------------------ % 70.98/10.21 % (3260828)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3554951152:i=14071_2981 on theBenchmark for (2981ds/14071Mi) % 70.98/10.21 % (3260828)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 70.98/10.21 % (3260828)Terminated due to inappropriate strategy. % 70.98/10.21 % (3260828)------------------------------ % 70.98/10.21 % (3260828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.98/10.21 % (3260828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.98/10.21 % (3260828)CaDiCaL version: 2.1.3 % 70.98/10.21 % (3260828)Termination reason: Inappropriate % 70.98/10.21 % (3260828)Time elapsed: 0.0000 s % 70.98/10.21 % (3260828)Peak memory usage: 10 MB % 70.98/10.21 % (3260828)Instructions burned: 1 (million) % 70.98/10.21 % (3260828)------------------------------ % 70.98/10.21 % (3260828)------------------------------ % 70.98/10.21 % (3260830)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2888484203:i=22565:add=on:rawr=on_2981 on theBenchmark for (2981ds/22565Mi) % 70.98/10.21 % (3260806)Instruction limit reached! % 70.98/10.21 % (3260806)------------------------------ % 70.98/10.21 % (3260806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.98/10.21 % (3260806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.98/10.21 % (3260806)CaDiCaL version: 2.1.3 % 70.98/10.21 % (3260806)Termination reason: Instruction limit % 70.98/10.21 % (3260806)Termination phase: Saturation % 70.98/10.21 % (3260806)Time elapsed: 1.755 s % 70.98/10.21 % (3260806)Peak memory usage: 33 MB % 70.98/10.21 % (3260806)Instructions burned: 5114 (million) % 70.98/10.21 % (3260832)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=61885297:i=8173:av=off_2978 on theBenchmark for (2978ds/8173Mi) % 70.98/10.21 % (3260818)Instruction limit reached! % 70.98/10.27 % (3260818)------------------------------ % 70.98/10.27 % (3260818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.98/10.27 % (3260818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.98/10.27 % (3260818)CaDiCaL version: 2.1.3 % 70.98/10.27 % (3260818)Termination reason: Instruction limit % 70.98/10.27 % (3260818)Termination phase: Saturation % 70.98/10.27 % (3260818)Time elapsed: 1.235 s % 70.98/10.27 % (3260818)Peak memory usage: 37 MB % 70.98/10.27 % (3260818)Instructions burned: 4595 (million) % 70.98/10.27 % (3260834)dis+10_16:1_sil=16000:random_seed=2607106718:i=9155:fsr=off_2973 on theBenchmark for (2973ds/9155Mi) % 70.98/10.27 % (3260822)Instruction limit reached! % 70.98/10.27 % (3260822)------------------------------ % 70.98/10.27 % (3260822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.98/10.27 % (3260822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.98/10.27 % (3260822)CaDiCaL version: 2.1.3 % 70.98/10.27 % (3260822)Termination reason: Instruction limit % 70.98/10.27 % (3260822)Termination phase: Saturation % 70.98/10.27 % (3260822)Time elapsed: 1.445 s % 70.98/10.27 % (3260822)Peak memory usage: 43 MB % 70.98/10.27 % (3260822)Instructions burned: 5213 (million) % 70.98/10.27 % (3260836)ott-3_8_sil=64000:random_seed=3498529602:i=20139:bs=on_2967 on theBenchmark for (2967ds/20139Mi) % 70.98/10.27 % (3260832)Instruction limit reached! % 70.98/10.27 % (3260832)------------------------------ % 70.98/10.27 % (3260832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.98/10.27 % (3260832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.98/10.27 % (3260832)CaDiCaL version: 2.1.3 % 70.98/10.27 % (3260832)Termination reason: Instruction limit % 70.98/10.27 % (3260832)Termination phase: Saturation % 70.98/10.27 % (3260832)Time elapsed: 2.802 s % 70.98/10.27 % (3260832)Peak memory usage: 54 MB % 70.98/10.27 % (3260832)Instructions burned: 8173 (million) % 70.98/10.27 % (3260838)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2103422406:fmbsr=2:i=32576_2950 on theBenchmark for (2950ds/32576Mi) % 70.98/10.27 % (3260838)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 70.98/10.27 % (3260838)Terminated due to inappropriate strategy. % 70.98/10.27 % (3260838)------------------------------ % 70.98/10.27 % (3260838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.98/10.27 % (3260838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.98/10.27 % (3260838)CaDiCaL version: 2.1.3 % 70.98/10.27 % (3260838)Termination reason: Inappropriate % 70.98/10.27 % (3260838)Time elapsed: 0.0000 s % 70.98/10.27 % (3260838)Peak memory usage: 10 MB % 70.98/10.27 % (3260838)Instructions burned: 1 (million) % 70.98/10.27 % (3260838)------------------------------ % 70.98/10.27 % (3260838)------------------------------ % 70.98/10.27 % (3260840)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1428438865:i=11404_2950 on theBenchmark for (2950ds/11404Mi) % 70.98/10.27 % (3260834)Instruction limit reached! % 70.98/10.27 % (3260834)------------------------------ % 70.98/10.27 % (3260834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.98/10.27 % (3260834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.98/10.27 % (3260834)CaDiCaL version: 2.1.3 % 70.98/10.27 % (3260834)Termination reason: Instruction limit % 70.98/10.27 % (3260834)Termination phase: Saturation % 70.98/10.27 % (3260834)Time elapsed: 2.520 s % 70.98/10.27 % (3260834)Peak memory usage: 52 MB % 70.98/10.27 % (3260834)Instructions burned: 9155 (million) % 70.98/10.27 % (3260842)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=87108054:i=14134_2948 on theBenchmark for (2948ds/14134Mi) % 70.98/10.27 % (3260830)Instruction limit reached! % 70.98/10.27 % (3260830)------------------------------ % 70.98/10.27 % (3260830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.98/10.27 % (3260830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.98/10.27 % (3260830)CaDiCaL version: 2.1.3 % 70.98/10.27 % (3260830)Termination reason: Instruction limit % 70.98/10.27 % (3260830)Termination phase: Saturation % 70.98/10.27 % (3260830)Time elapsed: 4.879 s % 70.98/10.27 % (3260830)Peak memory usage: 111 MB % 70.98/10.27 % (3260830)Instructions burned: 22567 (million) % 70.98/10.27 % (3260844)dis+33_16_sil=32000:sac=on:random_seed=1451284209:i=15851:nm=0_2932 on theBenchmark for (2932ds/15851Mi) % 70.98/10.27 % (3260820)Instruction limit reached! % 70.98/10.27 % (3260820)------------------------------ % 70.98/10.27 % (3260820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.57/13.12 % (3260820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.57/13.12 % (3260820)CaDiCaL version: 2.1.3 % 91.57/13.12 % (3260820)Termination reason: Instruction limit % 91.57/13.12 % (3260820)Termination phase: Saturation % 91.57/13.12 % (3260820)Time elapsed: 6.391 s % 91.57/13.12 % (3260820)Peak memory usage: 118 MB % 91.57/13.12 % (3260820)Instructions burned: 29343 (million) % 91.57/13.12 % (3260846)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=999892391:avsq=on:i=17627:add=on:amm=off_2921 on theBenchmark for (2921ds/17627Mi) % 91.57/13.12 % (3260840)Instruction limit reached! % 91.57/13.12 % (3260840)------------------------------ % 91.57/13.12 % (3260840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.57/13.12 % (3260840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.57/13.12 % (3260840)CaDiCaL version: 2.1.3 % 91.57/13.12 % (3260840)Termination reason: Instruction limit % 91.57/13.12 % (3260840)Termination phase: Saturation % 91.57/13.12 % (3260840)Time elapsed: 3.925 s % 91.57/13.12 % (3260840)Peak memory usage: 62 MB % 91.57/13.12 % (3260840)Instructions burned: 11405 (million) % 91.57/13.12 % (3260848)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3423764331:s2a=on:i=53295_2910 on theBenchmark for (2910ds/53295Mi) % 91.57/13.12 % (3260836)Instruction limit reached! % 91.57/13.12 % (3260836)------------------------------ % 91.57/13.12 % (3260836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.57/13.12 % (3260836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.57/13.12 % (3260836)CaDiCaL version: 2.1.3 % 91.57/13.12 % (3260836)Termination reason: Instruction limit % 91.57/13.12 % (3260836)Termination phase: Saturation % 91.57/13.12 % (3260836)Time elapsed: 5.953 s % 91.57/13.12 % (3260836)Peak memory usage: 58 MB % 91.57/13.12 % (3260836)Instructions burned: 20139 (million) % 91.57/13.12 % (3260850)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=844004857:i=26857:ins=20_2908 on theBenchmark for (2908ds/26857Mi) % 91.57/13.12 % (3260850)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 91.57/13.12 % (3260850)Terminated due to inappropriate strategy. % 91.57/13.12 % (3260850)------------------------------ % 91.57/13.12 % (3260850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.57/13.12 % (3260850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.57/13.12 % (3260850)CaDiCaL version: 2.1.3 % 91.57/13.12 % (3260850)Termination reason: Inappropriate % 91.57/13.12 % (3260850)Time elapsed: 0.0000 s % 91.57/13.12 % (3260850)Peak memory usage: 10 MB % 91.57/13.12 % (3260850)Instructions burned: 1 (million) % 91.57/13.12 % (3260850)------------------------------ % 91.57/13.12 % (3260850)------------------------------ % 91.57/13.12 % (3260852)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2871191960:i=28120:bs=on:fsr=off_2908 on theBenchmark for (2908ds/28120Mi) % 91.57/13.12 % (3260842)Instruction limit reached! % 91.57/13.12 % (3260842)------------------------------ % 91.57/13.12 % (3260842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.57/13.12 % (3260842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.57/13.12 % (3260842)CaDiCaL version: 2.1.3 % 91.57/13.12 % (3260842)Termination reason: Instruction limit % 91.57/13.12 % (3260842)Termination phase: Saturation % 91.57/13.12 % (3260842)Time elapsed: 4.875 s % 91.57/13.12 % (3260842)Peak memory usage: 75 MB % 91.57/13.12 % (3260842)Instructions burned: 14136 (million) % 91.57/13.12 % (3260854)fmb+10_1_sil=256000:fmbss=7:random_seed=3614083626:fmbsr=1.6:i=182295_2899 on theBenchmark for (2899ds/182295Mi) % 91.57/13.12 % (3260854)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 91.57/13.12 % (3260854)Terminated due to inappropriate strategy. % 91.57/13.12 % (3260854)------------------------------ % 91.57/13.12 % (3260854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.57/13.12 % (3260854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.57/13.12 % (3260854)CaDiCaL version: 2.1.3 % 91.57/13.12 % (3260854)Termination reason: Inappropriate % 91.57/13.12 % (3260854)Time elapsed: 0.0000 s % 91.57/13.12 % (3260854)Peak memory usage: 10 MB % 91.57/13.12 % (3260854)Instructions burned: 1 (million) % 91.57/13.12 % (3260854)------------------------------ % 91.57/13.12 % (3260854)------------------------------ % 91.57/13.12 % (3260856)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2917067146:i=44625:gsp=on_2899 on theBenchmark for (2899ds/44625Mi) % 97.90/14.10 % (3260856)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 97.90/14.10 % (3260856)Terminated due to inappropriate strategy. % 97.90/14.10 % (3260856)------------------------------ % 97.90/14.10 % (3260856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.90/14.10 % (3260856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.90/14.10 % (3260856)CaDiCaL version: 2.1.3 % 97.90/14.10 % (3260856)Termination reason: Inappropriate % 97.90/14.10 % (3260856)Time elapsed: 0.0000 s % 97.90/14.10 % (3260856)Peak memory usage: 10 MB % 97.90/14.10 % (3260856)Instructions burned: 1 (million) % 97.90/14.10 % (3260856)------------------------------ % 97.90/14.10 % (3260856)------------------------------ % 97.90/14.10 % (3260858)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2775895601:i=160505_2899 on theBenchmark for (2899ds/160505Mi) % 97.90/14.10 % (3260858)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 97.90/14.10 % (3260858)Terminated due to inappropriate strategy. % 97.90/14.10 % (3260858)------------------------------ % 97.90/14.10 % (3260858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.90/14.10 % (3260858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.90/14.10 % (3260858)CaDiCaL version: 2.1.3 % 97.90/14.10 % (3260858)Termination reason: Inappropriate % 97.90/14.10 % (3260858)Time elapsed: 0.0000 s % 97.90/14.10 % (3260858)Peak memory usage: 10 MB % 97.90/14.10 % (3260858)Instructions burned: 1 (million) % 97.90/14.10 % (3260858)------------------------------ % 97.90/14.10 % (3260858)------------------------------ % 97.90/14.10 % (3260860)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1621324705:fmbsr=1.3:i=225729_2898 on theBenchmark for (2898ds/225729Mi) % 97.90/14.10 % (3260860)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 97.90/14.10 % (3260860)Terminated due to inappropriate strategy. % 97.90/14.10 % (3260860)------------------------------ % 97.90/14.10 % (3260860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.90/14.10 % (3260860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.90/14.10 % (3260860)CaDiCaL version: 2.1.3 % 97.90/14.10 % (3260860)Termination reason: Inappropriate % 97.90/14.10 % (3260860)Time elapsed: 0.0000 s % 97.90/14.10 % (3260860)Peak memory usage: 10 MB % 97.90/14.10 % (3260860)Instructions burned: 1 (million) % 97.90/14.10 % (3260860)------------------------------ % 97.90/14.10 % (3260860)------------------------------ % 97.90/14.10 % (3260862)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2315379181:fmbsr=2:i=185024:ins=7_2898 on theBenchmark for (2898ds/185024Mi) % 97.90/14.10 % (3260862)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 97.90/14.10 % (3260862)Terminated due to inappropriate strategy. % 97.90/14.10 % (3260862)------------------------------ % 97.90/14.10 % (3260862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.90/14.10 % (3260862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.90/14.10 % (3260862)CaDiCaL version: 2.1.3 % 97.90/14.10 % (3260862)Termination reason: Inappropriate % 97.90/14.10 % (3260862)Time elapsed: 0.0000 s % 97.90/14.10 % (3260862)Peak memory usage: 10 MB % 97.90/14.10 % (3260862)Instructions burned: 1 (million) % 97.90/14.10 % (3260862)------------------------------ % 97.90/14.10 % (3260862)------------------------------ % 97.90/14.10 % (3260864)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1012444649:rtra=on_2898 on theBenchmark for (2898ds/0Mi) % 97.90/14.10 % (3260864)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 97.90/14.10 % (3260864)Terminated due to inappropriate strategy. % 97.90/14.10 % (3260864)------------------------------ % 97.90/14.10 % (3260864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.90/14.10 % (3260864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.90/14.10 % (3260864)CaDiCaL version: 2.1.3 % 97.90/14.10 % (3260864)Termination reason: Inappropriate % 97.90/14.10 % (3260864)Time elapsed: 0.0000 s % 97.90/14.10 % (3260864)Peak memory usage: 10 MB % 97.90/14.10 % (3260864)Instructions burned: 1 (million) % 97.90/14.10 % (3260864)------------------------------ % 97.90/14.10 % (3260864)------------------------------ % 97.90/14.10 % (3260866)% WARNING: option uhcvi not known. % 97.90/14.10 % (3260866)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1557239562:i=271062:add=off:rtra=on:rawr=on_2898 on theBenchmark for (2898ds/271062Mi) % 108.53/15.66 % (3260844)Instruction limit reached! % 108.53/15.66 % (3260844)------------------------------ % 108.53/15.66 % (3260844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.53/15.66 % (3260844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.53/15.66 % (3260844)CaDiCaL version: 2.1.3 % 108.53/15.66 % (3260844)Termination reason: Instruction limit % 108.53/15.66 % (3260844)Termination phase: Saturation % 108.53/15.66 % (3260844)Time elapsed: 4.451 s % 108.53/15.66 % (3260844)Peak memory usage: 133 MB % 108.53/15.66 % (3260844)Instructions burned: 15854 (million) % 108.53/15.66 % (3260868)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1360041947:i=176048:add=on:rtra=on:rawr=on_2888 on theBenchmark for (2888ds/176048Mi) % 108.53/15.66 % (3260846)Instruction limit reached! % 108.53/15.66 % (3260846)------------------------------ % 108.53/15.66 % (3260846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.53/15.66 % (3260846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.53/15.66 % (3260846)CaDiCaL version: 2.1.3 % 108.53/15.66 % (3260846)Termination reason: Instruction limit % 108.53/15.66 % (3260846)Termination phase: Saturation % 108.53/15.66 % (3260846)Time elapsed: 4.682 s % 108.53/15.66 % (3260846)Peak memory usage: 130 MB % 108.53/15.66 % (3260846)Instructions burned: 17629 (million) % 108.53/15.66 % (3260870)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1858576477:i=206:fgj=on:rtra=on_2874 on theBenchmark for (2874ds/206Mi) % 108.53/15.66 % (3260870)Instruction limit reached! % 108.53/15.66 % (3260870)------------------------------ % 108.53/15.66 % (3260870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.53/15.66 % (3260870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.53/15.66 % (3260870)CaDiCaL version: 2.1.3 % 108.53/15.66 % (3260870)Termination reason: Instruction limit % 108.53/15.66 % (3260870)Termination phase: Saturation % 108.53/15.66 % (3260870)Time elapsed: 0.068 s % 108.53/15.66 % (3260870)Peak memory usage: 13 MB % 108.53/15.66 % (3260870)Instructions burned: 206 (million) % 108.53/15.66 % (3260872)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1089133306:i=232:rtra=on_2873 on theBenchmark for (2873ds/232Mi) % 108.53/15.66 % (3260872)Instruction limit reached! % 108.53/15.66 % (3260872)------------------------------ % 108.53/15.66 % (3260872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.53/15.66 % (3260872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.53/15.66 % (3260872)CaDiCaL version: 2.1.3 % 108.53/15.66 % (3260872)Termination reason: Instruction limit % 108.53/15.66 % (3260872)Termination phase: Saturation % 108.53/15.66 % (3260872)Time elapsed: 0.080 s % 108.53/15.66 % (3260872)Peak memory usage: 13 MB % 108.53/15.66 % (3260872)Instructions burned: 235 (million) % 108.53/15.66 % (3260874)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2961942313:i=262:rtra=on_2872 on theBenchmark for (2872ds/262Mi) % 108.53/15.66 % (3260874)Instruction limit reached! % 108.53/15.66 % (3260874)------------------------------ % 108.53/15.66 % (3260874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.53/15.66 % (3260874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.53/15.66 % (3260874)CaDiCaL version: 2.1.3 % 108.53/15.66 % (3260874)Termination reason: Instruction limit % 108.53/15.66 % (3260874)Termination phase: Saturation % 108.53/15.66 % (3260874)Time elapsed: 0.084 s % 108.53/15.66 % (3260874)Peak memory usage: 14 MB % 108.53/15.66 % (3260874)Instructions burned: 265 (million) % 108.53/15.66 % (3260876)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3374503619:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2871 on theBenchmark for (2871ds/318Mi) % 108.53/15.66 % (3260876)Instruction limit reached! % 108.53/15.66 % (3260876)------------------------------ % 108.53/15.66 % (3260876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.53/15.66 % (3260876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.53/15.66 % (3260876)CaDiCaL version: 2.1.3 % 108.53/15.66 % (3260876)Termination reason: Instruction limit % 108.53/15.66 % (3260876)Termination phase: Saturation % 108.53/15.66 % (3260876)Time elapsed: 0.119 s % 108.53/15.66 % (3260876)Peak memory usage: 15 MB % 108.53/15.66 % (3260876)Instructions burned: 319 (million) % 108.53/15.66 % (3260878)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2446975792:i=1428:nm=2:rtra=on_2870 on theBenchmark for (2870ds/1428Mi) % 117.50/16.83 % (3260878)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.50/16.83 % (3260878)Terminated due to inappropriate strategy. % 117.50/16.83 % (3260878)------------------------------ % 117.50/16.83 % (3260878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.50/16.83 % (3260878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.50/16.83 % (3260878)CaDiCaL version: 2.1.3 % 117.50/16.83 % (3260878)Termination reason: Inappropriate % 117.50/16.83 % (3260878)Time elapsed: 0.0000 s % 117.50/16.83 % (3260878)Peak memory usage: 10 MB % 117.50/16.83 % (3260878)Instructions burned: 1 (million) % 117.50/16.83 % (3260878)------------------------------ % 117.50/16.83 % (3260878)------------------------------ % 117.50/16.83 % (3260880)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2632566928:i=262:bd=preordered:rtra=on:fsd=on_2870 on theBenchmark for (2870ds/262Mi) % 117.50/16.83 % (3260880)Instruction limit reached! % 117.50/16.83 % (3260880)------------------------------ % 117.50/16.83 % (3260880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.50/16.83 % (3260880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.50/16.83 % (3260880)CaDiCaL version: 2.1.3 % 117.50/16.83 % (3260880)Termination reason: Instruction limit % 117.50/16.83 % (3260880)Termination phase: Saturation % 117.50/16.83 % (3260880)Time elapsed: 0.089 s % 117.50/16.83 % (3260880)Peak memory usage: 14 MB % 117.50/16.83 % (3260880)Instructions burned: 263 (million) % 117.50/16.83 % (3260882)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=423592121:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2869 on theBenchmark for (2869ds/1368Mi) % 117.50/16.83 % (3260882)Instruction limit reached! % 117.50/16.83 % (3260882)------------------------------ % 117.50/16.83 % (3260882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.50/16.83 % (3260882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.50/16.83 % (3260882)CaDiCaL version: 2.1.3 % 117.50/16.83 % (3260882)Termination reason: Instruction limit % 117.50/16.83 % (3260882)Termination phase: Saturation % 117.50/16.83 % (3260882)Time elapsed: 0.416 s % 117.50/16.83 % (3260882)Peak memory usage: 21 MB % 117.50/16.83 % (3260882)Instructions burned: 1370 (million) % 117.50/16.83 % (3260884)ott-21_1_sil=16000:si=on:fs=off:random_seed=768579735:i=360:av=off:fsr=off:rtra=on_2864 on theBenchmark for (2864ds/360Mi) % 117.50/16.83 % (3260884)Instruction limit reached! % 117.50/16.83 % (3260884)------------------------------ % 117.50/16.83 % (3260884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.50/16.83 % (3260884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.50/16.83 % (3260884)CaDiCaL version: 2.1.3 % 117.50/16.83 % (3260884)Termination reason: Instruction limit % 117.50/16.83 % (3260884)Termination phase: Saturation % 117.50/16.83 % (3260884)Time elapsed: 0.086 s % 117.50/16.83 % (3260884)Peak memory usage: 13 MB % 117.50/16.83 % (3260884)Instructions burned: 363 (million) % 117.50/16.83 % (3260886)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2592055790:i=954:bd=all:rtra=on_2863 on theBenchmark for (2863ds/954Mi) % 117.50/16.83 % (3260886)Instruction limit reached! % 117.50/16.83 % (3260886)------------------------------ % 117.50/16.83 % (3260886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.50/16.83 % (3260886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.50/16.83 % (3260886)CaDiCaL version: 2.1.3 % 117.50/16.83 % (3260886)Termination reason: Instruction limit % 117.50/16.83 % (3260886)Termination phase: Saturation % 117.50/16.83 % (3260886)Time elapsed: 0.329 s % 117.50/16.83 % (3260886)Peak memory usage: 17 MB % 117.50/16.83 % (3260886)Instructions burned: 955 (million) % 117.50/16.83 % (3260888)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2371709145:fmbsr=1.3:i=1730:ins=25:rtra=on_2860 on theBenchmark for (2860ds/1730Mi) % 117.50/16.83 % (3260888)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.50/16.83 % (3260888)Terminated due to inappropriate strategy. % 117.50/16.83 % (3260888)------------------------------ % 117.50/16.83 % (3260888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.50/16.83 % (3260888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.50/16.83 % (3260888)CaDiCaL version: 2.1.3 % 117.50/16.83 % (3260888)Termination reason: Inappropriate % 147.28/21.11 % (3260888)Time elapsed: 0.0000 s % 147.28/21.11 % (3260888)Peak memory usage: 10 MB % 147.28/21.11 % (3260888)Instructions burned: 1 (million) % 147.28/21.11 % (3260888)------------------------------ % 147.28/21.11 % (3260888)------------------------------ % 147.28/21.11 % (3260890)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1698715349:i=2358:rtra=on_2860 on theBenchmark for (2860ds/2358Mi) % 147.28/21.11 % (3260890)Instruction limit reached! % 147.28/21.11 % (3260890)------------------------------ % 147.28/21.11 % (3260890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.28/21.11 % (3260890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.28/21.11 % (3260890)CaDiCaL version: 2.1.3 % 147.28/21.11 % (3260890)Termination reason: Instruction limit % 147.28/21.11 % (3260890)Termination phase: Saturation % 147.28/21.11 % (3260890)Time elapsed: 0.546 s % 147.28/21.11 % (3260890)Peak memory usage: 18 MB % 147.28/21.11 % (3260890)Instructions burned: 2361 (million) % 147.28/21.11 % (3260892)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1614267915:i=1778:ins=1:rtra=on_2854 on theBenchmark for (2854ds/1778Mi) % 147.28/21.11 % (3260892)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 147.28/21.11 % (3260892)Terminated due to inappropriate strategy. % 147.28/21.11 % (3260892)------------------------------ % 147.28/21.11 % (3260892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.28/21.11 % (3260892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.28/21.11 % (3260892)CaDiCaL version: 2.1.3 % 147.28/21.11 % (3260892)Termination reason: Inappropriate % 147.28/21.11 % (3260892)Time elapsed: 0.0000 s % 147.28/21.11 % (3260892)Peak memory usage: 10 MB % 147.28/21.11 % (3260892)Instructions burned: 1 (million) % 147.28/21.11 % (3260892)------------------------------ % 147.28/21.11 % (3260892)------------------------------ % 147.28/21.11 % (3260894)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=1351327010:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2854 on theBenchmark for (2854ds/1384Mi) % 147.28/21.11 % (3260894)Instruction limit reached! % 147.28/21.11 % (3260894)------------------------------ % 147.28/21.11 % (3260894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.28/21.11 % (3260894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.28/21.11 % (3260894)CaDiCaL version: 2.1.3 % 147.28/21.11 % (3260894)Termination reason: Instruction limit % 147.28/21.11 % (3260894)Termination phase: Saturation % 147.28/21.11 % (3260894)Time elapsed: 0.400 s % 147.28/21.11 % (3260894)Peak memory usage: 19 MB % 147.28/21.11 % (3260894)Instructions burned: 1384 (million) % 147.28/21.11 % (3260896)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3788258075:i=1758:kws=inv_precedence:fsr=off:rtra=on_2850 on theBenchmark for (2850ds/1758Mi) % 147.28/21.11 % (3260896)Instruction limit reached! % 147.28/21.11 % (3260896)------------------------------ % 147.28/21.11 % (3260896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.28/21.11 % (3260896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.28/21.11 % (3260896)CaDiCaL version: 2.1.3 % 147.28/21.11 % (3260896)Termination reason: Instruction limit % 147.28/21.11 % (3260896)Termination phase: Saturation % 147.28/21.11 % (3260896)Time elapsed: 0.539 s % 147.28/21.11 % (3260896)Peak memory usage: 22 MB % 147.28/21.11 % (3260896)Instructions burned: 1760 (million) % 147.28/21.11 % (3260898)fmb+10_1_sil=64000:si=on:random_seed=1627322971:i=44122:nm=2:rtra=on:gsp=on_2844 on theBenchmark for (2844ds/44122Mi) % 147.28/21.11 % (3260898)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 147.28/21.11 % (3260898)Terminated due to inappropriate strategy. % 147.28/21.11 % (3260898)------------------------------ % 147.28/21.11 % (3260898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.28/21.11 % (3260898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.28/21.11 % (3260898)CaDiCaL version: 2.1.3 % 147.28/21.11 % (3260898)Termination reason: Inappropriate % 147.28/21.11 % (3260898)Time elapsed: 0.0000 s % 147.28/21.11 % (3260898)Peak memory usage: 10 MB % 147.28/21.11 % (3260898)Instructions burned: 1 (million) % 147.28/21.11 % (3260898)------------------------------ % 147.28/21.11 % (3260898)------------------------------ % 147.28/21.11 % (3260900)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3979653146:i=19030:nm=5:rtra=on_2844 on theBenchmark for (2844ds/19030Mi) % 157.26/22.59 % (3260900)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.26/22.59 % (3260900)Terminated due to inappropriate strategy. % 157.26/22.59 % (3260900)------------------------------ % 157.26/22.59 % (3260900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.26/22.59 % (3260900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.26/22.59 % (3260900)CaDiCaL version: 2.1.3 % 157.26/22.59 % (3260900)Termination reason: Inappropriate % 157.26/22.59 % (3260900)Time elapsed: 0.0000 s % 157.26/22.59 % (3260900)Peak memory usage: 10 MB % 157.26/22.59 % (3260900)Instructions burned: 1 (million) % 157.26/22.59 % (3260900)------------------------------ % 157.26/22.59 % (3260900)------------------------------ % 157.26/22.59 % (3260902)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1346566649:fmbsr=1.7:i=1840:rtra=on_2844 on theBenchmark for (2844ds/1840Mi) % 157.26/22.59 % (3260902)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.26/22.59 % (3260902)Terminated due to inappropriate strategy. % 157.26/22.59 % (3260902)------------------------------ % 157.26/22.59 % (3260902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.26/22.59 % (3260902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.26/22.59 % (3260902)CaDiCaL version: 2.1.3 % 157.26/22.59 % (3260902)Termination reason: Inappropriate % 157.26/22.59 % (3260902)Time elapsed: 0.0000 s % 157.26/22.59 % (3260902)Peak memory usage: 10 MB % 157.26/22.59 % (3260902)Instructions burned: 1 (million) % 157.26/22.59 % (3260902)------------------------------ % 157.26/22.59 % (3260902)------------------------------ % 157.26/22.59 % (3260904)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2971099105:i=10262:rtra=on_2844 on theBenchmark for (2844ds/10262Mi) % 157.26/22.59 % (3260852)Instruction limit reached! % 157.26/22.59 % (3260852)------------------------------ % 157.26/22.59 % (3260852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.26/22.59 % (3260852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.26/22.59 % (3260852)CaDiCaL version: 2.1.3 % 157.26/22.59 % (3260852)Termination reason: Instruction limit % 157.26/22.59 % (3260852)Termination phase: Saturation % 157.26/22.59 % (3260852)Time elapsed: 6.452 s % 157.26/22.59 % (3260852)Peak memory usage: 27 MB % 157.26/22.59 % (3260852)Instructions burned: 28120 (million) % 157.26/22.59 % (3260906)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3136539349:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2843 on theBenchmark for (2843ds/2944Mi) % 157.26/22.59 % (3260906)Instruction limit reached! % 157.26/22.59 % (3260906)------------------------------ % 157.26/22.59 % (3260906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.26/22.59 % (3260906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.26/22.59 % (3260906)CaDiCaL version: 2.1.3 % 157.26/22.59 % (3260906)Termination reason: Instruction limit % 157.26/22.59 % (3260906)Termination phase: Saturation % 157.26/22.59 % (3260906)Time elapsed: 1.021 s % 157.26/22.59 % (3260906)Peak memory usage: 29 MB % 157.26/22.59 % (3260906)Instructions burned: 2945 (million) % 157.26/22.59 % (3260908)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3386684675:i=12648:rtra=on_2833 on theBenchmark for (2833ds/12648Mi) % 157.26/22.59 % (3260908)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.26/22.59 % (3260908)Terminated due to inappropriate strategy. % 157.26/22.59 % (3260908)------------------------------ % 157.26/22.59 % (3260908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.26/22.59 % (3260908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.26/22.59 % (3260908)CaDiCaL version: 2.1.3 % 157.26/22.59 % (3260908)Termination reason: Inappropriate % 157.26/22.59 % (3260908)Time elapsed: 0.0000 s % 157.26/22.59 % (3260908)Peak memory usage: 11 MB % 157.26/22.59 % (3260908)Instructions burned: 1 (million) % 157.26/22.59 % (3260908)------------------------------ % 157.26/22.59 % (3260908)------------------------------ % 157.26/22.59 % (3260910)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3045099719:fmbsr=2.30978:i=4348:rtra=on_2832 on theBenchmark for (2832ds/4348Mi) % 157.26/22.59 % (3260910)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.26/22.59 % (3260910)Terminated due to inappropriate strategy. % 157.26/22.59 % (3260910)------------------------------ % 213.68/30.55 % (3260910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.68/30.55 % (3260910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.68/30.55 % (3260910)CaDiCaL version: 2.1.3 % 213.68/30.55 % (3260910)Termination reason: Inappropriate % 213.68/30.55 % (3260910)Time elapsed: 0.0000 s % 213.68/30.55 % (3260910)Peak memory usage: 10 MB % 213.68/30.55 % (3260910)Instructions burned: 1 (million) % 213.68/30.55 % (3260910)------------------------------ % 213.68/30.55 % (3260910)------------------------------ % 213.68/30.55 % (3260912)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1317214163:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2832 on theBenchmark for (2832ds/1738Mi) % 213.68/30.55 % (3260912)Instruction limit reached! % 213.68/30.55 % (3260912)------------------------------ % 213.68/30.55 % (3260912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.68/30.55 % (3260912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.68/30.55 % (3260912)CaDiCaL version: 2.1.3 % 213.68/30.55 % (3260912)Termination reason: Instruction limit % 213.68/30.55 % (3260912)Termination phase: Saturation % 213.68/30.55 % (3260912)Time elapsed: 0.597 s % 213.68/30.55 % (3260912)Peak memory usage: 23 MB % 213.68/30.55 % (3260912)Instructions burned: 1740 (million) % 213.68/30.55 % (3260914)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2058825659:i=10228:av=off:rtra=on_2826 on theBenchmark for (2826ds/10228Mi) % 213.68/30.55 % (3260758)Instruction limit reached! % 213.68/30.55 % (3260758)------------------------------ % 213.68/30.55 % (3260758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.68/30.55 % (3260758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.68/30.55 % (3260758)CaDiCaL version: 2.1.3 % 213.68/30.55 % (3260758)Termination reason: Instruction limit % 213.68/30.55 % (3260758)Termination phase: Saturation % 213.68/30.55 % (3260758)Time elapsed: 18.733 s % 213.68/30.55 % (3260758)Peak memory usage: 134 MB % 213.68/30.55 % (3260758)Instructions burned: 88030 (million) % 213.68/30.55 % (3260916)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=110548472:i=108564:rtra=on_2812 on theBenchmark for (2812ds/108564Mi) % 213.68/30.55 % (3260916)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.68/30.55 % (3260916)Terminated due to inappropriate strategy. % 213.68/30.55 % (3260916)------------------------------ % 213.68/30.55 % (3260916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.68/30.55 % (3260916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.68/30.55 % (3260916)CaDiCaL version: 2.1.3 % 213.68/30.55 % (3260916)Termination reason: Inappropriate % 213.68/30.55 % (3260916)Time elapsed: 0.0000 s % 213.68/30.55 % (3260916)Peak memory usage: 10 MB % 213.68/30.55 % (3260916)Instructions burned: 1 (million) % 213.68/30.55 % (3260916)------------------------------ % 213.68/30.55 % (3260916)------------------------------ % 213.68/30.55 % (3260918)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2485854379:i=7024:aac=none:rtra=on_2812 on theBenchmark for (2812ds/7024Mi) % 213.68/30.55 % (3260904)Instruction limit reached! % 213.68/30.55 % (3260904)------------------------------ % 213.68/30.55 % (3260904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.68/30.55 % (3260904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.68/30.55 % (3260904)CaDiCaL version: 2.1.3 % 213.68/30.55 % (3260904)Termination reason: Instruction limit % 213.68/30.55 % (3260904)Termination phase: Saturation % 213.68/30.55 % (3260904)Time elapsed: 3.238 s % 213.68/30.55 % (3260904)Peak memory usage: 69 MB % 213.68/30.55 % (3260904)Instructions burned: 10263 (million) % 213.68/30.55 % (3260920)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3271526913:i=7546:rtra=on:amm=off_2811 on theBenchmark for (2811ds/7546Mi) % 213.68/30.55 % (3260918)Instruction limit reached! % 213.68/30.55 % (3260918)------------------------------ % 213.68/30.55 % (3260918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.68/30.55 % (3260918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.68/30.55 % (3260918)CaDiCaL version: 2.1.3 % 213.68/30.55 % (3260918)Termination reason: Instruction limit % 213.68/30.55 % (3260918)Termination phase: Saturation % 213.68/30.55 % (3260918)Time elapsed: 2.179 s % 213.68/30.55 % (3260918)Peak memory usage: 49 MB % 213.68/30.55 % (3260918)Instructions burned: 7027 (million) % 213.68/30.55 % (3260922)ott+11_1_sil=16000:si=on:gs=on:random_seed=2963398392:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2790 on theBenchmark for (2790ds/4502Mi) % 246.48/40.92 % (3260920)Instruction limit reached! % 246.48/40.92 % (3260920)------------------------------ % 246.48/40.92 % (3260920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.48/40.92 % (3260920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.48/40.92 % (3260920)CaDiCaL version: 2.1.3 % 246.48/40.92 % (3260920)Termination reason: Instruction limit % 246.48/40.92 % (3260920)Termination phase: Saturation % 246.48/40.92 % (3260920)Time elapsed: 2.369 s % 246.48/40.92 % (3260920)Peak memory usage: 48 MB % 246.48/40.92 % (3260920)Instructions burned: 7547 (million) % 246.48/40.92 % (3260924)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=1866734676:fmbsr=1.6:i=135068:rtra=on_2788 on theBenchmark for (2788ds/135068Mi) % 246.48/40.92 % (3260924)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 246.48/40.92 % (3260924)Terminated due to inappropriate strategy. % 246.48/40.92 % (3260924)------------------------------ % 246.48/40.92 % (3260924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.48/40.92 % (3260924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.48/40.92 % (3260924)CaDiCaL version: 2.1.3 % 246.48/40.92 % (3260924)Termination reason: Inappropriate % 246.48/40.92 % (3260924)Time elapsed: 0.0000 s % 246.48/40.92 % (3260924)Peak memory usage: 10 MB % 246.48/40.92 % (3260924)Instructions burned: 1 (million) % 246.48/40.92 % (3260924)------------------------------ % 246.48/40.92 % (3260924)------------------------------ % 246.48/40.92 % (3260914)Instruction limit reached! % 246.48/40.92 % (3260914)------------------------------ % 246.48/40.92 % (3260914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.48/40.92 % (3260914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.48/40.92 % (3260914)CaDiCaL version: 2.1.3 % 246.48/40.92 % (3260914)Termination reason: Instruction limit % 246.48/40.92 % (3260914)Termination phase: Saturation % 246.48/40.92 % (3260914)Time elapsed: 3.868 s % 246.48/40.92 % (3260914)Peak memory usage: 52 MB % 246.48/40.92 % (3260914)Instructions burned: 10230 (million) % 246.48/40.92 % (3260926)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2331634836:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2788 on theBenchmark for (2788ds/9182Mi) % 246.48/40.92 % (3260927)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=177743495:i=58680:rtra=on_2787 on theBenchmark for (2787ds/58680Mi) % 246.48/40.92 % (3260848)Instruction limit reached! % 246.48/40.92 % (3260848)------------------------------ % 246.48/40.92 % (3260848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.48/40.92 % (3260848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.48/40.92 % (3260848)CaDiCaL version: 2.1.3 % 246.48/40.92 % (3260848)Termination reason: Instruction limit % 246.48/40.92 % (3260848)Termination phase: Saturation % 246.48/40.92 % (3260848)Time elapsed: 12.934 s % 246.48/40.92 % (3260848)Peak memory usage: 358 MB % 246.48/40.92 % (3260848)Instructions burned: 53297 (million) % 246.48/40.92 % (3260930)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=628179800:i=10422:rtra=on_2781 on theBenchmark for (2781ds/10422Mi) % 246.48/40.92 % (3260922)Instruction limit reached! % 246.48/40.92 % (3260922)------------------------------ % 246.48/40.92 % (3260922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.48/40.92 % (3260922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.48/40.92 % (3260922)CaDiCaL version: 2.1.3 % 246.48/40.92 % (3260922)Termination reason: Instruction limit % 246.48/40.92 % (3260922)Termination phase: Saturation % 246.48/40.92 % (3260922)Time elapsed: 1.472 s % 246.48/40.92 % (3260922)Peak memory usage: 32 MB % 246.48/40.92 % (3260922)Instructions burned: 4503 (million) % 246.48/40.92 % (3260932)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=600060048:i=10994:nm=2:rtra=on_2775 on theBenchmark for (2775ds/10994Mi) % 246.48/40.92 % (3260932)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 246.48/40.92 % (3260932)Terminated due to inappropriate strategy. % 246.48/40.92 % (3260932)------------------------------ % 246.48/40.92 % (3260932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.48/40.92 % (3260932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.48/40.92 % (3260932)CaDiCaL version: 2.1.3 % 246.48/40.92 % (3260932)Termination reason: InappropriTerminated % 300.20/42.73 % Vampire exiting %------------------------------------------------------------------------------