%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW085_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n016.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:39:22 PM UTC 2026 % Result : Timeout 300.03s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW085_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n016.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 13:16:18 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.60/0.87 % (3613937)Will run a generic schedule for satisfiability detection. % 3.60/0.87 % (3613948)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=166547351:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.60/0.87 % (3613943)% WARNING: option uhcvi not known. % 3.60/0.87 % (3613943)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2019307167:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.60/0.87 % (3613945)dis+10_1_sil=32000:sp=arity:random_seed=1818533637:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.60/0.87 % (3613944)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2954134544:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.60/0.87 % (3613942)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2439754730_2999 on theBenchmark for (2999ds/0Mi) % 3.60/0.87 % (3613947)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2167960338:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.60/0.87 % (3613946)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=842745908:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.60/0.87 % (3613948)Instruction limit reached! % 3.60/0.87 % (3613948)------------------------------ % 3.60/0.87 % (3613948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.60/0.87 % (3613948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.60/0.87 % (3613948)CaDiCaL version: 2.1.3 % 3.60/0.87 % (3613948)Termination reason: Instruction limit % 3.60/0.87 % (3613948)Termination phase: Saturation % 3.60/0.87 % (3613948)Time elapsed: 0.035 s % 3.60/0.87 % (3613948)Peak memory usage: 16 MB % 3.60/0.87 % (3613948)Instructions burned: 163 (million) % 3.60/0.87 % (3613956)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=408485571:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.60/0.87 % (3613942)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.60/0.87 % (3613942)Terminated due to inappropriate strategy. % 3.60/0.87 % (3613942)------------------------------ % 3.60/0.87 % (3613942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.60/0.87 % (3613942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.60/0.87 % (3613942)CaDiCaL version: 2.1.3 % 3.60/0.87 % (3613942)Termination reason: Inappropriate % 3.60/0.87 % (3613942)Time elapsed: 0.044 s % 3.60/0.87 % (3613942)Peak memory usage: 14 MB % 3.60/0.87 % (3613942)Instructions burned: 99 (million) % 3.60/0.87 % (3613942)------------------------------ % 3.60/0.87 % (3613942)------------------------------ % 3.60/0.87 % (3613945)Instruction limit reached! % 3.60/0.87 % (3613945)------------------------------ % 3.60/0.87 % (3613945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.60/0.87 % (3613945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.60/0.87 % (3613945)CaDiCaL version: 2.1.3 % 3.60/0.87 % (3613945)Termination reason: Instruction limit % 3.60/0.87 % (3613945)Termination phase: Saturation % 3.60/0.87 % (3613945)Time elapsed: 0.047 s % 3.60/0.87 % (3613945)Peak memory usage: 15 MB % 3.60/0.87 % (3613945)Instructions burned: 103 (million) % 3.60/0.87 % (3613946)Instruction limit reached! % 3.60/0.87 % (3613946)------------------------------ % 3.60/0.87 % (3613946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.60/0.87 % (3613946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.60/0.87 % (3613946)CaDiCaL version: 2.1.3 % 3.60/0.87 % (3613946)Termination reason: Instruction limit % 3.60/0.87 % (3613946)Termination phase: Saturation % 3.60/0.87 % (3613946)Time elapsed: 0.058 s % 3.60/0.87 % (3613946)Peak memory usage: 16 MB % 3.60/0.87 % (3613946)Instructions burned: 118 (million) % 3.60/0.87 % (3613947)Instruction limit reached! % 3.60/0.87 % (3613947)------------------------------ % 3.60/0.87 % (3613947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.60/0.87 % (3613947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.60/0.87 % (3613947)CaDiCaL version: 2.1.3 % 3.60/0.87 % (3613947)Termination reason: Instruction limit % 3.60/0.87 % (3613947)Termination phase: Saturation % 3.60/0.87 % (3613947)Time elapsed: 0.059 s % 3.60/0.87 % (3613947)Peak memory usage: 15 MB % 3.60/0.87 % (3613947)Instructions burned: 134 (million) % 3.60/0.87 % (3613958)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4127764874:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 5.70/1.12 % (3613959)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=2089937530:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.70/1.12 % (3613961)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1249934089:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.70/1.12 % (3613960)ott-21_1_sil=16000:fs=off:random_seed=1620530245:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.70/1.12 % (3613956)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.70/1.12 % (3613956)Terminated due to inappropriate strategy. % 5.70/1.12 % (3613956)------------------------------ % 5.70/1.12 % (3613956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.70/1.12 % (3613956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.70/1.12 % (3613956)CaDiCaL version: 2.1.3 % 5.70/1.12 % (3613956)Termination reason: Inappropriate % 5.70/1.12 % (3613956)Time elapsed: 0.042 s % 5.70/1.12 % (3613956)Peak memory usage: 14 MB % 5.70/1.12 % (3613956)Instructions burned: 99 (million) % 5.70/1.12 % (3613956)------------------------------ % 5.70/1.12 % (3613956)------------------------------ % 5.70/1.12 % (3613966)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2055612650:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.70/1.12 % (3613958)Instruction limit reached! % 5.70/1.12 % (3613958)------------------------------ % 5.70/1.12 % (3613958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.70/1.12 % (3613958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.70/1.12 % (3613958)CaDiCaL version: 2.1.3 % 5.70/1.12 % (3613958)Termination reason: Instruction limit % 5.70/1.12 % (3613958)Termination phase: Saturation % 5.70/1.12 % (3613958)Time elapsed: 0.059 s % 5.70/1.12 % (3613958)Peak memory usage: 16 MB % 5.70/1.12 % (3613958)Instructions burned: 134 (million) % 5.70/1.12 % (3613975)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1540756148:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.70/1.12 % (3613966)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.70/1.12 % (3613966)Terminated due to inappropriate strategy. % 5.70/1.12 % (3613966)------------------------------ % 5.70/1.12 % (3613966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.70/1.12 % (3613966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.70/1.12 % (3613966)CaDiCaL version: 2.1.3 % 5.70/1.12 % (3613966)Termination reason: Inappropriate % 5.70/1.12 % (3613966)Time elapsed: 0.044 s % 5.70/1.12 % (3613966)Peak memory usage: 14 MB % 5.70/1.12 % (3613966)Instructions burned: 98 (million) % 5.70/1.12 % (3613966)------------------------------ % 5.70/1.12 % (3613966)------------------------------ % 5.70/1.12 % (3613960)Instruction limit reached! % 5.70/1.12 % (3613960)------------------------------ % 5.70/1.12 % (3613960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.70/1.12 % (3613960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.70/1.12 % (3613960)CaDiCaL version: 2.1.3 % 5.70/1.12 % (3613960)Termination reason: Instruction limit % 5.70/1.12 % (3613960)Termination phase: Saturation % 5.70/1.12 % (3613960)Time elapsed: 0.085 s % 5.70/1.12 % (3613960)Peak memory usage: 15 MB % 5.70/1.12 % (3613960)Instructions burned: 181 (million) % 5.70/1.12 % (3613979)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1651432924:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 5.70/1.12 % (3613985)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=615891849:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 5.70/1.12 % (3613979)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.70/1.12 % (3613979)Terminated due to inappropriate strategy. % 5.70/1.12 % (3613979)------------------------------ % 5.70/1.12 % (3613979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.70/1.12 % (3613979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.70/1.12 % (3613979)CaDiCaL version: 2.1.3 % 5.70/1.12 % (3613979)Termination reason: Inappropriate % 5.70/1.12 % (3613979)Time elapsed: 0.060 s % 5.70/1.12 % (3613979)Peak memory usage: 16 MB % 23.04/3.52 % (3613979)Instructions burned: 136 (million) % 23.04/3.52 % (3613979)------------------------------ % 23.04/3.52 % (3613979)------------------------------ % 23.04/3.52 % (3613959)Instruction limit reached! % 23.04/3.52 % (3613959)------------------------------ % 23.04/3.52 % (3613959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.04/3.52 % (3613959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.04/3.52 % (3613959)CaDiCaL version: 2.1.3 % 23.04/3.52 % (3613959)Termination reason: Instruction limit % 23.04/3.52 % (3613959)Termination phase: Saturation % 23.04/3.52 % (3613959)Time elapsed: 0.181 s % 23.04/3.52 % (3613959)Peak memory usage: 20 MB % 23.04/3.52 % (3613959)Instructions burned: 686 (million) % 23.04/3.52 % (3614007)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=315384650:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 23.04/3.52 % (3614013)fmb+10_1_sil=64000:random_seed=2564415381:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 23.04/3.52 % (3614013)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.04/3.52 % (3614013)Terminated due to inappropriate strategy. % 23.04/3.52 % (3614013)------------------------------ % 23.04/3.52 % (3614013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.04/3.52 % (3614013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.04/3.52 % (3614013)CaDiCaL version: 2.1.3 % 23.04/3.52 % (3614013)Termination reason: Inappropriate % 23.04/3.52 % (3614013)Time elapsed: 0.025 s % 23.04/3.52 % (3614013)Peak memory usage: 14 MB % 23.04/3.52 % (3614013)Instructions burned: 109 (million) % 23.04/3.52 % (3614013)------------------------------ % 23.04/3.52 % (3614013)------------------------------ % 23.04/3.52 % (3614035)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3381483930:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 23.04/3.52 % (3613961)Instruction limit reached! % 23.04/3.52 % (3613961)------------------------------ % 23.04/3.52 % (3613961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.04/3.52 % (3613961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.04/3.52 % (3613961)CaDiCaL version: 2.1.3 % 23.04/3.52 % (3613961)Termination reason: Instruction limit % 23.04/3.52 % (3613961)Termination phase: Saturation % 23.04/3.52 % (3613961)Time elapsed: 0.248 s % 23.04/3.52 % (3613961)Peak memory usage: 17 MB % 23.04/3.52 % (3613961)Instructions burned: 478 (million) % 23.04/3.52 % (3614035)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.04/3.52 % (3614035)Terminated due to inappropriate strategy. % 23.04/3.52 % (3614035)------------------------------ % 23.04/3.52 % (3614035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.04/3.52 % (3614035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.04/3.52 % (3614035)CaDiCaL version: 2.1.3 % 23.04/3.52 % (3614035)Termination reason: Inappropriate % 23.04/3.52 % (3614035)Time elapsed: 0.030 s % 23.04/3.52 % (3614035)Peak memory usage: 14 MB % 23.04/3.52 % (3614035)Instructions burned: 99 (million) % 23.04/3.52 % (3614035)------------------------------ % 23.04/3.52 % (3614035)------------------------------ % 23.04/3.52 % (3614048)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3606680804:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 23.04/3.52 % (3614046)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=267423153:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 23.04/3.52 % (3614046)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.04/3.52 % (3614046)Terminated due to inappropriate strategy. % 23.04/3.52 % (3614046)------------------------------ % 23.04/3.52 % (3614046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.04/3.52 % (3614046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.04/3.52 % (3614046)CaDiCaL version: 2.1.3 % 23.04/3.52 % (3614046)Termination reason: Inappropriate % 23.04/3.52 % (3614046)Time elapsed: 0.044 s % 23.04/3.52 % (3614046)Peak memory usage: 14 MB % 23.04/3.52 % (3614046)Instructions burned: 99 (million) % 23.04/3.52 % (3614046)------------------------------ % 23.04/3.52 % (3614046)------------------------------ % 23.04/3.52 % (3614067)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3988095524:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 23.04/3.52 % (3613985)Instruction limit reached! % 23.04/3.52 % (3613985)------------------------------ % 25.43/4.03 % (3613985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.43/4.03 % (3613985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.03 % (3613985)CaDiCaL version: 2.1.3 % 25.43/4.03 % (3613985)Termination reason: Instruction limit % 25.43/4.03 % (3613985)Termination phase: Saturation % 25.43/4.03 % (3613985)Time elapsed: 0.400 s % 25.43/4.03 % (3613985)Peak memory usage: 23 MB % 25.43/4.03 % (3613985)Instructions burned: 693 (million) % 25.43/4.03 % (3614112)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=681186792:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 25.43/4.03 % (3613975)Instruction limit reached! % 25.43/4.03 % (3613975)------------------------------ % 25.43/4.03 % (3613975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.43/4.03 % (3613975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.03 % (3613975)CaDiCaL version: 2.1.3 % 25.43/4.03 % (3613975)Termination reason: Instruction limit % 25.43/4.03 % (3613975)Termination phase: Saturation % 25.43/4.03 % (3613975)Time elapsed: 0.547 s % 25.43/4.03 % (3613975)Peak memory usage: 20 MB % 25.43/4.03 % (3613975)Instructions burned: 1181 (million) % 25.43/4.03 % (3614112)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.43/4.03 % (3614112)Terminated due to inappropriate strategy. % 25.43/4.03 % (3614112)------------------------------ % 25.43/4.03 % (3614112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.43/4.03 % (3614112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.03 % (3614112)CaDiCaL version: 2.1.3 % 25.43/4.03 % (3614112)Termination reason: Inappropriate % 25.43/4.03 % (3614112)Time elapsed: 0.080 s % 25.43/4.03 % (3614112)Peak memory usage: 14 MB % 25.43/4.03 % (3614112)Instructions burned: 99 (million) % 25.43/4.03 % (3614112)------------------------------ % 25.43/4.03 % (3614112)------------------------------ % 25.43/4.03 % (3614118)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2548794604:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi) % 25.43/4.03 % (3614119)ott-2_1_sil=16000:newcnf=on:random_seed=2755566324:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 25.43/4.03 % (3614118)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.43/4.03 % (3614118)Terminated due to inappropriate strategy. % 25.43/4.03 % (3614118)------------------------------ % 25.43/4.03 % (3614118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.43/4.03 % (3614118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.03 % (3614118)CaDiCaL version: 2.1.3 % 25.43/4.03 % (3614118)Termination reason: Inappropriate % 25.43/4.03 % (3614118)Time elapsed: 0.042 s % 25.43/4.03 % (3614118)Peak memory usage: 14 MB % 25.43/4.03 % (3614118)Instructions burned: 99 (million) % 25.43/4.03 % (3614118)------------------------------ % 25.43/4.03 % (3614118)------------------------------ % 25.43/4.03 % (3614007)Instruction limit reached! % 25.43/4.03 % (3614007)------------------------------ % 25.43/4.03 % (3614007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.43/4.03 % (3614007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.03 % (3614007)CaDiCaL version: 2.1.3 % 25.43/4.03 % (3614007)Termination reason: Instruction limit % 25.43/4.03 % (3614007)Termination phase: Saturation % 25.43/4.03 % (3614007)Time elapsed: 0.516 s % 25.43/4.03 % (3614007)Peak memory usage: 22 MB % 25.43/4.03 % (3614007)Instructions burned: 880 (million) % 25.43/4.03 % (3614123)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3338625120:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 25.43/4.03 % (3614122)ott+10_1_sil=32000:tgt=ground:random_seed=3933355972:i=5114:av=off_2991 on theBenchmark for (2991ds/5114Mi) % 25.43/4.03 % (3614123)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.43/4.03 % (3614123)Terminated due to inappropriate strategy. % 25.43/4.03 % (3614123)------------------------------ % 25.43/4.03 % (3614123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.43/4.03 % (3614123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.03 % (3614123)CaDiCaL version: 2.1.3 % 25.43/4.03 % (3614123)Termination reason: Inappropriate % 25.43/4.03 % (3614123)Time elapsed: 0.042 s % 25.43/4.03 % (3614123)Peak memory usage: 14 MB % 25.43/4.03 % (3614123)Instructions burned: 99 (million) % 91.85/13.29 % (3614123)------------------------------ % 91.85/13.29 % (3614123)------------------------------ % 91.85/13.29 % (3614126)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4171670612:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 91.85/13.29 % (3614067)Instruction limit reached! % 91.85/13.29 % (3614067)------------------------------ % 91.85/13.29 % (3614067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.85/13.29 % (3614067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.85/13.29 % (3614067)CaDiCaL version: 2.1.3 % 91.85/13.29 % (3614067)Termination reason: Instruction limit % 91.85/13.29 % (3614067)Termination phase: Saturation % 91.85/13.29 % (3614067)Time elapsed: 0.535 s % 91.85/13.29 % (3614067)Peak memory usage: 17 MB % 91.85/13.29 % (3614067)Instructions burned: 1474 (million) % 91.85/13.29 % (3614128)dis+21_1_sil=32000:sas=cadical:random_seed=3514546529:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 91.85/13.29 % (3614119)Instruction limit reached! % 91.85/13.29 % (3614119)------------------------------ % 91.85/13.29 % (3614119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.85/13.29 % (3614119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.85/13.29 % (3614119)CaDiCaL version: 2.1.3 % 91.85/13.29 % (3614119)Termination reason: Instruction limit % 91.85/13.29 % (3614119)Termination phase: Saturation % 91.85/13.29 % (3614119)Time elapsed: 0.478 s % 91.85/13.29 % (3614119)Peak memory usage: 21 MB % 91.85/13.29 % (3614119)Instructions burned: 870 (million) % 91.85/13.29 % (3614130)ott+11_1_sil=16000:gs=on:random_seed=3039682057:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 91.85/13.29 % (3614048)Instruction limit reached! % 91.85/13.29 % (3614048)------------------------------ % 91.85/13.29 % (3614048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.85/13.29 % (3614048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.85/13.29 % (3614048)CaDiCaL version: 2.1.3 % 91.85/13.29 % (3614048)Termination reason: Instruction limit % 91.85/13.29 % (3614048)Termination phase: Saturation % 91.85/13.29 % (3614048)Time elapsed: 1.705 s % 91.85/13.29 % (3614048)Peak memory usage: 44 MB % 91.85/13.29 % (3614048)Instructions burned: 5133 (million) % 91.85/13.29 % (3614182)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4171518228:fmbsr=1.6:i=67534_2978 on theBenchmark for (2978ds/67534Mi) % 91.85/13.29 % (3614182)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 91.85/13.29 % (3614182)Terminated due to inappropriate strategy. % 91.85/13.29 % (3614182)------------------------------ % 91.85/13.29 % (3614182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.85/13.29 % (3614182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.85/13.29 % (3614182)CaDiCaL version: 2.1.3 % 91.85/13.29 % (3614182)Termination reason: Inappropriate % 91.85/13.29 % (3614182)Time elapsed: 0.058 s % 91.85/13.29 % (3614182)Peak memory usage: 14 MB % 91.85/13.29 % (3614182)Instructions burned: 133 (million) % 91.85/13.29 % (3614182)------------------------------ % 91.85/13.29 % (3614182)------------------------------ % 91.85/13.29 % (3614186)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1363650403:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2978 on theBenchmark for (2978ds/4591Mi) % 91.85/13.29 % (3614130)Instruction limit reached! % 91.85/13.29 % (3614130)------------------------------ % 91.85/13.29 % (3614130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.85/13.29 % (3614130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.85/13.29 % (3614130)CaDiCaL version: 2.1.3 % 91.85/13.29 % (3614130)Termination reason: Instruction limit % 91.85/13.29 % (3614130)Termination phase: Saturation % 91.85/13.29 % (3614130)Time elapsed: 1.479 s % 91.85/13.29 % (3614130)Peak memory usage: 21 MB % 91.85/13.29 % (3614130)Instructions burned: 2251 (million) % 91.85/13.29 % (3614219)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=56833013:i=29340_2972 on theBenchmark for (2972ds/29340Mi) % 91.85/13.29 % (3614126)Instruction limit reached! % 91.85/13.29 % (3614126)------------------------------ % 91.85/13.29 % (3614126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.85/13.29 % (3614126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.85/13.29 % (3614126)CaDiCaL version: 2.1.3 % 91.85/13.29 % (3614126)Termination reason: Instruction limit % 117.38/16.85 % (3614126)Termination phase: Saturation % 117.38/16.85 % (3614126)Time elapsed: 2.380 s % 117.38/16.85 % (3614126)Peak memory usage: 27 MB % 117.38/16.85 % (3614126)Instructions burned: 3513 (million) % 117.38/16.85 % (3614230)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1811904623:i=5211_2967 on theBenchmark for (2967ds/5211Mi) % 117.38/16.85 % (3614128)Instruction limit reached! % 117.38/16.85 % (3614128)------------------------------ % 117.38/16.85 % (3614128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.38/16.85 % (3614128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.38/16.85 % (3614128)CaDiCaL version: 2.1.3 % 117.38/16.85 % (3614128)Termination reason: Instruction limit % 117.38/16.85 % (3614128)Termination phase: Saturation % 117.38/16.85 % (3614128)Time elapsed: 2.503 s % 117.38/16.85 % (3614128)Peak memory usage: 27 MB % 117.38/16.85 % (3614128)Instructions burned: 3773 (million) % 117.38/16.85 % (3614233)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2457962216:i=5497:nm=2_2964 on theBenchmark for (2964ds/5497Mi) % 117.38/16.85 % (3614233)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.38/16.85 % (3614233)Terminated due to inappropriate strategy. % 117.38/16.85 % (3614233)------------------------------ % 117.38/16.85 % (3614233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.38/16.85 % (3614233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.38/16.85 % (3614233)CaDiCaL version: 2.1.3 % 117.38/16.85 % (3614233)Termination reason: Inappropriate % 117.38/16.85 % (3614233)Time elapsed: 0.041 s % 117.38/16.85 % (3614233)Peak memory usage: 14 MB % 117.38/16.85 % (3614233)Instructions burned: 99 (million) % 117.38/16.85 % (3614233)------------------------------ % 117.38/16.85 % (3614233)------------------------------ % 117.38/16.85 % (3614235)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1404905250:fmbsr=2:i=46332_2964 on theBenchmark for (2964ds/46332Mi) % 117.38/16.85 % (3614235)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.38/16.85 % (3614235)Terminated due to inappropriate strategy. % 117.38/16.85 % (3614235)------------------------------ % 117.38/16.85 % (3614235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.38/16.85 % (3614235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.38/16.85 % (3614235)CaDiCaL version: 2.1.3 % 117.38/16.85 % (3614235)Termination reason: Inappropriate % 117.38/16.85 % (3614235)Time elapsed: 0.056 s % 117.38/16.85 % (3614235)Peak memory usage: 14 MB % 117.38/16.85 % (3614235)Instructions burned: 137 (million) % 117.38/16.85 % (3614235)------------------------------ % 117.38/16.85 % (3614235)------------------------------ % 117.38/16.85 % (3614242)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3563460716:i=14071_2963 on theBenchmark for (2963ds/14071Mi) % 117.38/16.85 % (3614242)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.38/16.85 % (3614242)Terminated due to inappropriate strategy. % 117.38/16.85 % (3614242)------------------------------ % 117.38/16.85 % (3614242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.38/16.85 % (3614242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.38/16.85 % (3614242)CaDiCaL version: 2.1.3 % 117.38/16.85 % (3614242)Termination reason: Inappropriate % 117.38/16.85 % (3614242)Time elapsed: 0.057 s % 117.38/16.85 % (3614242)Peak memory usage: 14 MB % 117.38/16.85 % (3614242)Instructions burned: 137 (million) % 117.38/16.85 % (3614242)------------------------------ % 117.38/16.85 % (3614242)------------------------------ % 117.38/16.85 % (3614266)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=633946162:i=22565:add=on:rawr=on_2962 on theBenchmark for (2962ds/22565Mi) % 117.38/16.85 % (3614186)Instruction limit reached! % 117.38/16.85 % (3614186)------------------------------ % 117.38/16.85 % (3614186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.38/16.85 % (3614186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.38/16.85 % (3614186)CaDiCaL version: 2.1.3 % 117.38/16.85 % (3614186)Termination reason: Instruction limit % 117.38/16.85 % (3614186)Termination phase: Saturation % 117.38/16.85 % (3614186)Time elapsed: 1.568 s % 117.38/16.85 % (3614186)Peak memory usage: 42 MB % 117.38/16.85 % (3614186)Instructions burned: 4594 (million) % 117.38/16.85 % (3614280)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1412838878:i=8173:av=off_2962 on theBenchmark for (2962ds/8173Mi) % 120.18/17.23 % (3614122)Instruction limit reached! % 120.18/17.23 % (3614122)------------------------------ % 120.18/17.23 % (3614122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.18/17.23 % (3614122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.18/17.23 % (3614122)CaDiCaL version: 2.1.3 % 120.18/17.23 % (3614122)Termination reason: Instruction limit % 120.18/17.23 % (3614122)Termination phase: Saturation % 120.18/17.23 % (3614122)Time elapsed: 3.628 s % 120.18/17.23 % (3614122)Peak memory usage: 33 MB % 120.18/17.23 % (3614122)Instructions burned: 5115 (million) % 120.18/17.23 % (3614282)dis+10_16:1_sil=16000:random_seed=461591673:i=9155:fsr=off_2955 on theBenchmark for (2955ds/9155Mi) % 120.18/17.23 % (3614280)Instruction limit reached! % 120.18/17.23 % (3614280)------------------------------ % 120.18/17.23 % (3614280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.18/17.23 % (3614280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.18/17.23 % (3614280)CaDiCaL version: 2.1.3 % 120.18/17.23 % (3614280)Termination reason: Instruction limit % 120.18/17.23 % (3614280)Termination phase: Saturation % 120.18/17.23 % (3614280)Time elapsed: 1.762 s % 120.18/17.23 % (3614280)Peak memory usage: 37 MB % 120.18/17.23 % (3614280)Instructions burned: 8174 (million) % 120.18/17.23 % (3614284)ott-3_8_sil=64000:random_seed=969349454:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 120.18/17.23 % (3614230)Instruction limit reached! % 120.18/17.23 % (3614230)------------------------------ % 120.18/17.23 % (3614230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.18/17.23 % (3614230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.18/17.23 % (3614230)CaDiCaL version: 2.1.3 % 120.18/17.23 % (3614230)Termination reason: Instruction limit % 120.18/17.23 % (3614230)Termination phase: Saturation % 120.18/17.23 % (3614230)Time elapsed: 2.782 s % 120.18/17.23 % (3614230)Peak memory usage: 52 MB % 120.18/17.23 % (3614230)Instructions burned: 5211 (million) % 120.18/17.23 % (3614286)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1402005595:fmbsr=2:i=32576_2939 on theBenchmark for (2939ds/32576Mi) % 120.18/17.23 % (3614286)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 120.18/17.23 % (3614286)Terminated due to inappropriate strategy. % 120.18/17.23 % (3614286)------------------------------ % 120.18/17.23 % (3614286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.18/17.23 % (3614286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.18/17.23 % (3614286)CaDiCaL version: 2.1.3 % 120.18/17.23 % (3614286)Termination reason: Inappropriate % 120.18/17.23 % (3614286)Time elapsed: 0.055 s % 120.18/17.23 % (3614286)Peak memory usage: 14 MB % 120.18/17.23 % (3614286)Instructions burned: 133 (million) % 120.18/17.23 % (3614286)------------------------------ % 120.18/17.23 % (3614286)------------------------------ % 120.18/17.23 % (3614288)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=830130621:i=11404_2938 on theBenchmark for (2938ds/11404Mi) % 120.18/17.23 % (3614282)Instruction limit reached! % 120.18/17.23 % (3614282)------------------------------ % 120.18/17.23 % (3614282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.18/17.23 % (3614282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.18/17.23 % (3614282)CaDiCaL version: 2.1.3 % 120.18/17.23 % (3614282)Termination reason: Instruction limit % 120.18/17.23 % (3614282)Termination phase: Saturation % 120.18/17.23 % (3614282)Time elapsed: 4.692 s % 120.18/17.23 % (3614282)Peak memory usage: 57 MB % 120.18/17.23 % (3614282)Instructions burned: 9155 (million) % 120.18/17.23 % (3614290)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1730409796:i=14134_2908 on theBenchmark for (2908ds/14134Mi) % 120.18/17.23 % (3614284)Instruction limit reached! % 120.18/17.23 % (3614284)------------------------------ % 120.18/17.23 % (3614284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.18/17.23 % (3614284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.18/17.23 % (3614284)CaDiCaL version: 2.1.3 % 120.18/17.23 % (3614284)Termination reason: Instruction limit % 120.18/17.23 % (3614284)Termination phase: Saturation % 120.18/17.23 % (3614284)Time elapsed: 5.241 s % 120.18/17.23 % (3614284)Peak memory usage: 61 MB % 120.18/17.23 % (3614284)Instructions burned: 20140 (million) % 120.18/17.23 % (3614292)dis+33_16_sil=32000:sac=on:random_seed=878510665:i=15851:nm=0_2891 on theBenchmark for (2891ds/15851Mi) % 120.18/17.23 % (3614266)Instruction limit reached! % 120.18/17.23 % (3614266)------------------------------ % 120.18/17.23 % (3614266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.06/20.77 % (3614266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.06/20.77 % (3614266)CaDiCaL version: 2.1.3 % 145.06/20.77 % (3614266)Termination reason: Instruction limit % 145.06/20.77 % (3614266)Termination phase: Saturation % 145.06/20.77 % (3614266)Time elapsed: 9.290 s % 145.06/20.77 % (3614266)Peak memory usage: 63 MB % 145.06/20.77 % (3614266)Instructions burned: 22567 (million) % 145.06/20.77 % (3614294)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=50596738:avsq=on:i=17627:add=on:amm=off_2869 on theBenchmark for (2869ds/17627Mi) % 145.06/20.77 % (3614288)Instruction limit reached! % 145.06/20.77 % (3614288)------------------------------ % 145.06/20.77 % (3614288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.06/20.77 % (3614288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.06/20.77 % (3614288)CaDiCaL version: 2.1.3 % 145.06/20.77 % (3614288)Termination reason: Instruction limit % 145.06/20.77 % (3614288)Termination phase: Saturation % 145.06/20.77 % (3614288)Time elapsed: 7.265 s % 145.06/20.77 % (3614288)Peak memory usage: 49 MB % 145.06/20.77 % (3614288)Instructions burned: 11404 (million) % 145.06/20.77 % (3614296)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2302616892:s2a=on:i=53295_2865 on theBenchmark for (2865ds/53295Mi) % 145.06/20.77 % (3614292)Instruction limit reached! % 145.06/20.77 % (3614292)------------------------------ % 145.06/20.77 % (3614292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.06/20.77 % (3614292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.06/20.77 % (3614292)CaDiCaL version: 2.1.3 % 145.06/20.77 % (3614292)Termination reason: Instruction limit % 145.06/20.77 % (3614292)Termination phase: Saturation % 145.06/20.77 % (3614292)Time elapsed: 3.575 s % 145.06/20.77 % (3614292)Peak memory usage: 34 MB % 145.06/20.77 % (3614292)Instructions burned: 15852 (million) % 145.06/20.77 % (3614411)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1518449105:i=26857:ins=20_2855 on theBenchmark for (2855ds/26857Mi) % 145.06/20.77 % (3614411)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 145.06/20.77 % (3614411)Terminated due to inappropriate strategy. % 145.06/20.77 % (3614411)------------------------------ % 145.06/20.77 % (3614411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.06/20.77 % (3614411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.06/20.77 % (3614411)CaDiCaL version: 2.1.3 % 145.06/20.77 % (3614411)Termination reason: Inappropriate % 145.06/20.77 % (3614411)Time elapsed: 0.023 s % 145.06/20.77 % (3614411)Peak memory usage: 14 MB % 145.06/20.77 % (3614411)Instructions burned: 99 (million) % 145.06/20.77 % (3614411)------------------------------ % 145.06/20.77 % (3614411)------------------------------ % 145.06/20.77 % (3614413)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4015375870:i=28120:bs=on:fsr=off_2855 on theBenchmark for (2855ds/28120Mi) % 145.06/20.77 % (3614219)Instruction limit reached! % 145.06/20.77 % (3614219)------------------------------ % 145.06/20.77 % (3614219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.06/20.77 % (3614219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.06/20.77 % (3614219)CaDiCaL version: 2.1.3 % 145.06/20.77 % (3614219)Termination reason: Instruction limit % 145.06/20.77 % (3614219)Termination phase: Saturation % 145.06/20.77 % (3614219)Time elapsed: 13.733 s % 145.06/20.77 % (3614219)Peak memory usage: 43 MB % 145.06/20.77 % (3614219)Instructions burned: 29340 (million) % 145.06/20.77 % (3614415)fmb+10_1_sil=256000:fmbss=7:random_seed=2315602228:fmbsr=1.6:i=182295_2834 on theBenchmark for (2834ds/182295Mi) % 145.06/20.77 % (3614415)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 145.06/20.77 % (3614415)Terminated due to inappropriate strategy. % 145.06/20.77 % (3614415)------------------------------ % 145.06/20.77 % (3614415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.06/20.77 % (3614415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.06/20.77 % (3614415)CaDiCaL version: 2.1.3 % 145.06/20.77 % (3614415)Termination reason: Inappropriate % 145.06/20.77 % (3614415)Time elapsed: 0.042 s % 145.06/20.77 % (3614415)Peak memory usage: 14 MB % 145.06/20.77 % (3614415)Instructions burned: 99 (million) % 145.06/20.77 % (3614415)------------------------------ % 145.06/20.77 % (3614415)------------------------------ % 145.06/20.77 % (3614417)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2284978062:i=44625:gsp=on_2833 on theBenchmark for (2833ds/44625Mi) % 151.92/21.76 % (3614417)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.92/21.76 % (3614417)Terminated due to inappropriate strategy. % 151.92/21.76 % (3614417)------------------------------ % 151.92/21.76 % (3614417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.92/21.76 % (3614417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.92/21.76 % (3614417)CaDiCaL version: 2.1.3 % 151.92/21.76 % (3614417)Termination reason: Inappropriate % 151.92/21.76 % (3614417)Time elapsed: 0.048 s % 151.92/21.76 % (3614417)Peak memory usage: 15 MB % 151.92/21.76 % (3614417)Instructions burned: 104 (million) % 151.92/21.76 % (3614417)------------------------------ % 151.92/21.76 % (3614417)------------------------------ % 151.92/21.76 % (3614419)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2875516021:i=160505_2833 on theBenchmark for (2833ds/160505Mi) % 151.92/21.76 % (3614419)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.92/21.76 % (3614419)Terminated due to inappropriate strategy. % 151.92/21.76 % (3614419)------------------------------ % 151.92/21.76 % (3614419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.92/21.76 % (3614419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.92/21.76 % (3614419)CaDiCaL version: 2.1.3 % 151.92/21.76 % (3614419)Termination reason: Inappropriate % 151.92/21.76 % (3614419)Time elapsed: 0.043 s % 151.92/21.76 % (3614419)Peak memory usage: 14 MB % 151.92/21.76 % (3614419)Instructions burned: 99 (million) % 151.92/21.76 % (3614419)------------------------------ % 151.92/21.76 % (3614419)------------------------------ % 151.92/21.76 % (3614421)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1972322088:fmbsr=1.3:i=225729_2832 on theBenchmark for (2832ds/225729Mi) % 151.92/21.76 % (3614421)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.92/21.76 % (3614421)Terminated due to inappropriate strategy. % 151.92/21.76 % (3614421)------------------------------ % 151.92/21.76 % (3614421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.92/21.76 % (3614421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.92/21.76 % (3614421)CaDiCaL version: 2.1.3 % 151.92/21.76 % (3614421)Termination reason: Inappropriate % 151.92/21.76 % (3614421)Time elapsed: 0.062 s % 151.92/21.76 % (3614421)Peak memory usage: 14 MB % 151.92/21.76 % (3614421)Instructions burned: 137 (million) % 151.92/21.76 % (3614421)------------------------------ % 151.92/21.76 % (3614421)------------------------------ % 151.92/21.76 % (3614423)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=923476805:fmbsr=2:i=185024:ins=7_2831 on theBenchmark for (2831ds/185024Mi) % 151.92/21.76 % (3614423)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.92/21.76 % (3614423)Terminated due to inappropriate strategy. % 151.92/21.76 % (3614423)------------------------------ % 151.92/21.76 % (3614423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.92/21.76 % (3614423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.92/21.76 % (3614423)CaDiCaL version: 2.1.3 % 151.92/21.76 % (3614423)Termination reason: Inappropriate % 151.92/21.76 % (3614423)Time elapsed: 0.058 s % 151.92/21.76 % (3614423)Peak memory usage: 14 MB % 151.92/21.76 % (3614423)Instructions burned: 137 (million) % 151.92/21.76 % (3614423)------------------------------ % 151.92/21.76 % (3614423)------------------------------ % 151.92/21.76 % (3614425)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2229365261:rtra=on_2830 on theBenchmark for (2830ds/0Mi) % 151.92/21.76 % (3614425)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.92/21.76 % (3614425)Terminated due to inappropriate strategy. % 151.92/21.76 % (3614425)------------------------------ % 151.92/21.76 % (3614425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.92/21.76 % (3614425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.92/21.76 % (3614425)CaDiCaL version: 2.1.3 % 151.92/21.76 % (3614425)Termination reason: Inappropriate % 151.92/21.76 % (3614425)Time elapsed: 0.056 s % 151.92/21.76 % (3614425)Peak memory usage: 16 MB % 151.92/21.76 % (3614425)Instructions burned: 115 (million) % 151.92/21.76 % (3614425)------------------------------ % 151.92/21.76 % (3614425)------------------------------ % 151.92/21.76 % (3614427)% WARNING: option uhcvi not known. % 151.92/21.76 % (3614427)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3617504407:i=271062:add=off:rtra=on:rawr=on_2830 on theBenchmark for (2830ds/271062Mi) % 160.33/22.96 % (3614290)Instruction limit reached! % 160.33/22.96 % (3614290)------------------------------ % 160.33/22.96 % (3614290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.33/22.96 % (3614290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.33/22.96 % (3614290)CaDiCaL version: 2.1.3 % 160.33/22.96 % (3614290)Termination reason: Instruction limit % 160.33/22.96 % (3614290)Termination phase: Saturation % 160.33/22.96 % (3614290)Time elapsed: 8.483 s % 160.33/22.96 % (3614290)Peak memory usage: 53 MB % 160.33/22.96 % (3614290)Instructions burned: 14135 (million) % 160.33/22.96 % (3614429)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=927667686:i=176048:add=on:rtra=on:rawr=on_2822 on theBenchmark for (2822ds/176048Mi) % 160.33/22.96 % (3614413)Instruction limit reached! % 160.33/22.96 % (3614413)------------------------------ % 160.33/22.96 % (3614413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.33/22.96 % (3614413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.33/22.96 % (3614413)CaDiCaL version: 2.1.3 % 160.33/22.96 % (3614413)Termination reason: Instruction limit % 160.33/22.96 % (3614413)Termination phase: Saturation % 160.33/22.96 % (3614413)Time elapsed: 5.757 s % 160.33/22.96 % (3614413)Peak memory usage: 27 MB % 160.33/22.96 % (3614413)Instructions burned: 28128 (million) % 160.33/22.96 % (3614431)dis+10_1_sil=32000:si=on:sp=arity:random_seed=77492943:i=206:fgj=on:rtra=on_2797 on theBenchmark for (2797ds/206Mi) % 160.33/22.96 % (3614431)Instruction limit reached! % 160.33/22.96 % (3614431)------------------------------ % 160.33/22.96 % (3614431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.33/22.96 % (3614431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.33/22.96 % (3614431)CaDiCaL version: 2.1.3 % 160.33/22.96 % (3614431)Termination reason: Instruction limit % 160.33/22.96 % (3614431)Termination phase: Saturation % 160.33/22.96 % (3614431)Time elapsed: 0.056 s % 160.33/22.96 % (3614431)Peak memory usage: 18 MB % 160.33/22.96 % (3614431)Instructions burned: 207 (million) % 160.33/22.96 % (3614433)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3419692790:i=232:rtra=on_2797 on theBenchmark for (2797ds/232Mi) % 160.33/22.96 % (3614433)Instruction limit reached! % 160.33/22.96 % (3614433)------------------------------ % 160.33/22.96 % (3614433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.33/22.96 % (3614433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.33/22.96 % (3614433)CaDiCaL version: 2.1.3 % 160.33/22.96 % (3614433)Termination reason: Instruction limit % 160.33/22.96 % (3614433)Termination phase: Saturation % 160.33/22.96 % (3614433)Time elapsed: 0.060 s % 160.33/22.96 % (3614433)Peak memory usage: 18 MB % 160.33/22.96 % (3614433)Instructions burned: 236 (million) % 160.33/22.96 % (3614435)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1501176047:i=262:rtra=on_2796 on theBenchmark for (2796ds/262Mi) % 160.33/22.96 % (3614435)Instruction limit reached! % 160.33/22.96 % (3614435)------------------------------ % 160.33/22.96 % (3614435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.33/22.96 % (3614435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.33/22.96 % (3614435)CaDiCaL version: 2.1.3 % 160.33/22.97 % (3614435)Termination reason: Instruction limit % 160.33/22.97 % (3614435)Termination phase: Saturation % 160.33/22.97 % (3614435)Time elapsed: 0.062 s % 160.33/22.97 % (3614435)Peak memory usage: 17 MB % 160.33/22.97 % (3614435)Instructions burned: 264 (million) % 160.33/22.97 % (3614437)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3557497157:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2795 on theBenchmark for (2795ds/318Mi) % 160.33/22.97 % (3614437)Instruction limit reached! % 160.33/22.97 % (3614437)------------------------------ % 160.33/22.97 % (3614437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.33/22.97 % (3614437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.33/22.97 % (3614437)CaDiCaL version: 2.1.3 % 160.33/22.97 % (3614437)Termination reason: Instruction limit % 160.33/22.97 % (3614437)Termination phase: Saturation % 160.33/22.97 % (3614437)Time elapsed: 0.089 s % 160.33/22.97 % (3614437)Peak memory usage: 20 MB % 160.33/22.97 % (3614437)Instructions burned: 319 (million) % 160.33/22.97 % (3614439)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=691533280:i=1428:nm=2:rtra=on_2794 on theBenchmark for (2794ds/1428Mi) % 179.13/25.55 % (3614439)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 179.13/25.55 % (3614439)Terminated due to inappropriate strategy. % 179.13/25.55 % (3614439)------------------------------ % 179.13/25.55 % (3614439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.13/25.55 % (3614439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.13/25.55 % (3614439)CaDiCaL version: 2.1.3 % 179.13/25.55 % (3614439)Termination reason: Inappropriate % 179.13/25.55 % (3614439)Time elapsed: 0.030 s % 179.13/25.55 % (3614439)Peak memory usage: 16 MB % 179.13/25.55 % (3614439)Instructions burned: 115 (million) % 179.13/25.55 % (3614439)------------------------------ % 179.13/25.55 % (3614439)------------------------------ % 179.13/25.55 % (3614441)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=955412608:i=262:bd=preordered:rtra=on:fsd=on_2794 on theBenchmark for (2794ds/262Mi) % 179.13/25.55 % (3614441)Instruction limit reached! % 179.13/25.55 % (3614441)------------------------------ % 179.13/25.55 % (3614441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.13/25.55 % (3614441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.13/25.55 % (3614441)CaDiCaL version: 2.1.3 % 179.13/25.55 % (3614441)Termination reason: Instruction limit % 179.13/25.55 % (3614441)Termination phase: Saturation % 179.13/25.55 % (3614441)Time elapsed: 0.102 s % 179.13/25.55 % (3614441)Peak memory usage: 18 MB % 179.13/25.55 % (3614441)Instructions burned: 266 (million) % 179.13/25.55 % (3614443)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=3371634119:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2793 on theBenchmark for (2793ds/1368Mi) % 179.13/25.55 % (3614443)Instruction limit reached! % 179.13/25.55 % (3614443)------------------------------ % 179.13/25.55 % (3614443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.13/25.55 % (3614443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.13/25.55 % (3614443)CaDiCaL version: 2.1.3 % 179.13/25.55 % (3614443)Termination reason: Instruction limit % 179.13/25.55 % (3614443)Termination phase: Saturation % 179.13/25.55 % (3614443)Time elapsed: 0.374 s % 179.13/25.55 % (3614443)Peak memory usage: 23 MB % 179.13/25.55 % (3614443)Instructions burned: 1372 (million) % 179.13/25.55 % (3614445)ott-21_1_sil=16000:si=on:fs=off:random_seed=3237166005:i=360:av=off:fsr=off:rtra=on_2789 on theBenchmark for (2789ds/360Mi) % 179.13/25.55 % (3614445)Instruction limit reached! % 179.13/25.55 % (3614445)------------------------------ % 179.13/25.55 % (3614445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.13/25.55 % (3614445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.13/25.55 % (3614445)CaDiCaL version: 2.1.3 % 179.13/25.55 % (3614445)Termination reason: Instruction limit % 179.13/25.55 % (3614445)Termination phase: Saturation % 179.13/25.55 % (3614445)Time elapsed: 0.097 s % 179.13/25.55 % (3614445)Peak memory usage: 17 MB % 179.13/25.55 % (3614445)Instructions burned: 363 (million) % 179.13/25.55 % (3614447)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3356469004:i=954:bd=all:rtra=on_2788 on theBenchmark for (2788ds/954Mi) % 179.13/25.55 % (3614447)Instruction limit reached! % 179.13/25.55 % (3614447)------------------------------ % 179.13/25.55 % (3614447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.13/25.55 % (3614447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.13/25.55 % (3614447)CaDiCaL version: 2.1.3 % 179.13/25.55 % (3614447)Termination reason: Instruction limit % 179.13/25.55 % (3614447)Termination phase: Saturation % 179.13/25.55 % (3614447)Time elapsed: 0.283 s % 179.13/25.55 % (3614447)Peak memory usage: 21 MB % 179.13/25.55 % (3614447)Instructions burned: 955 (million) % 179.13/25.55 % (3614449)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1071289804:fmbsr=1.3:i=1730:ins=25:rtra=on_2785 on theBenchmark for (2785ds/1730Mi) % 179.13/25.55 % (3614449)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 179.13/25.55 % (3614449)Terminated due to inappropriate strategy. % 179.13/25.55 % (3614449)------------------------------ % 179.13/25.55 % (3614449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.13/25.55 % (3614449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.13/25.55 % (3614449)CaDiCaL version: 2.1.3 % 179.13/25.55 % (3614449)Termination reason: Inappropriate % 216.79/30.86 % (3614449)Time elapsed: 0.030 s % 216.79/30.86 % (3614449)Peak memory usage: 16 MB % 216.79/30.86 % (3614449)Instructions burned: 114 (million) % 216.79/30.86 % (3614449)------------------------------ % 216.79/30.86 % (3614449)------------------------------ % 216.79/30.86 % (3614451)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3059256998:i=2358:rtra=on_2784 on theBenchmark for (2784ds/2358Mi) % 216.79/30.86 % (3614451)Instruction limit reached! % 216.79/30.86 % (3614451)------------------------------ % 216.79/30.86 % (3614451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.79/30.86 % (3614451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.79/30.86 % (3614451)CaDiCaL version: 2.1.3 % 216.79/30.86 % (3614451)Termination reason: Instruction limit % 216.79/30.86 % (3614451)Termination phase: Saturation % 216.79/30.86 % (3614451)Time elapsed: 0.700 s % 216.79/30.86 % (3614451)Peak memory usage: 27 MB % 216.79/30.86 % (3614451)Instructions burned: 2360 (million) % 216.79/30.86 % (3614453)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2762784114:i=1778:ins=1:rtra=on_2777 on theBenchmark for (2777ds/1778Mi) % 216.79/30.86 % (3614453)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 216.79/30.86 % (3614453)Terminated due to inappropriate strategy. % 216.79/30.86 % (3614453)------------------------------ % 216.79/30.86 % (3614453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.79/30.86 % (3614453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.79/30.86 % (3614453)CaDiCaL version: 2.1.3 % 216.79/30.86 % (3614453)Termination reason: Inappropriate % 216.79/30.86 % (3614453)Time elapsed: 0.040 s % 216.79/30.86 % (3614453)Peak memory usage: 18 MB % 216.79/30.86 % (3614453)Instructions burned: 155 (million) % 216.79/30.86 % (3614453)------------------------------ % 216.79/30.86 % (3614453)------------------------------ % 216.79/30.86 % (3614455)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=479515185:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2776 on theBenchmark for (2776ds/1384Mi) % 216.79/30.86 % (3614294)Instruction limit reached! % 216.79/30.86 % (3614294)------------------------------ % 216.79/30.86 % (3614294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.79/30.86 % (3614294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.79/30.86 % (3614294)CaDiCaL version: 2.1.3 % 216.79/30.86 % (3614294)Termination reason: Instruction limit % 216.79/30.86 % (3614294)Termination phase: Saturation % 216.79/30.86 % (3614294)Time elapsed: 9.553 s % 216.79/30.86 % (3614294)Peak memory usage: 103 MB % 216.79/30.86 % (3614294)Instructions burned: 17629 (million) % 216.79/30.86 % (3614457)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1247689419:i=1758:kws=inv_precedence:fsr=off:rtra=on_2773 on theBenchmark for (2773ds/1758Mi) % 216.79/30.86 % (3614455)Instruction limit reached! % 216.79/30.86 % (3614455)------------------------------ % 216.79/30.86 % (3614455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.79/30.86 % (3614455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.79/30.86 % (3614455)CaDiCaL version: 2.1.3 % 216.79/30.86 % (3614455)Termination reason: Instruction limit % 216.79/30.86 % (3614455)Termination phase: Saturation % 216.79/30.86 % (3614455)Time elapsed: 0.364 s % 216.79/30.86 % (3614455)Peak memory usage: 24 MB % 216.79/30.86 % (3614455)Instructions burned: 1385 (million) % 216.79/30.86 % (3614459)fmb+10_1_sil=64000:si=on:random_seed=3331912066:i=44122:nm=2:rtra=on:gsp=on_2773 on theBenchmark for (2773ds/44122Mi) % 216.79/30.86 % (3614459)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 216.79/30.86 % (3614459)Terminated due to inappropriate strategy. % 216.79/30.86 % (3614459)------------------------------ % 216.79/30.86 % (3614459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.79/30.86 % (3614459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.79/30.86 % (3614459)CaDiCaL version: 2.1.3 % 216.79/30.86 % (3614459)Termination reason: Inappropriate % 216.79/30.86 % (3614459)Time elapsed: 0.032 s % 216.79/30.86 % (3614459)Peak memory usage: 16 MB % 216.79/30.86 % (3614459)Instructions burned: 125 (million) % 216.79/30.86 % (3614459)------------------------------ % 216.79/30.86 % (3614459)------------------------------ % 216.79/30.86 % (3614461)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=523267344:i=19030:nm=5:Terminated % 300.03/42.54 % Vampire exiting % 300.03/42.54 Terminated %------------------------------------------------------------------------------