%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW825_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:02 PM UTC 2026 % Result : Timeout 300.27s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW825_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n006.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 14:30:40 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.23 Running first-order model finding % 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.15/0.77 % (4011918)Will run a generic schedule for satisfiability detection. % 3.15/0.77 % (4011926)dis+10_1_sil=32000:sp=arity:random_seed=1309590276:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.15/0.77 % (4011924)% WARNING: option uhcvi not known. % 3.15/0.77 % (4011925)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=160966826:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.15/0.77 % (4011923)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3977345379_2999 on theBenchmark for (2999ds/0Mi) % 3.15/0.77 % (4011924)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1975460304:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.15/0.77 % (4011928)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1153056516:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.15/0.77 % (4011927)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3139040201:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.15/0.77 % (4011929)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1212954702:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.15/0.77 % (4011923)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.15/0.77 % (4011923)Terminated due to inappropriate strategy. % 3.15/0.77 % (4011923)------------------------------ % 3.15/0.77 % (4011923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.15/0.77 % (4011923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.15/0.77 % (4011923)CaDiCaL version: 2.1.3 % 3.15/0.77 % (4011923)Termination reason: Inappropriate % 3.15/0.77 % (4011923)Time elapsed: 0.003 s % 3.15/0.77 % (4011923)Peak memory usage: 11 MB % 3.15/0.77 % (4011923)Instructions burned: 5 (million) % 3.15/0.77 % (4011923)------------------------------ % 3.15/0.77 % (4011923)------------------------------ % 3.15/0.77 % (4011937)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2600639876:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.15/0.77 % (4011937)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.15/0.77 % (4011937)Terminated due to inappropriate strategy. % 3.15/0.77 % (4011937)------------------------------ % 3.15/0.77 % (4011937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.15/0.77 % (4011937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.15/0.77 % (4011937)CaDiCaL version: 2.1.3 % 3.15/0.77 % (4011937)Termination reason: Inappropriate % 3.15/0.77 % (4011937)Time elapsed: 0.003 s % 3.15/0.77 % (4011937)Peak memory usage: 11 MB % 3.15/0.77 % (4011937)Instructions burned: 5 (million) % 3.15/0.77 % (4011937)------------------------------ % 3.15/0.77 % (4011937)------------------------------ % 3.15/0.77 % (4011926)Instruction limit reached! % 3.15/0.77 % (4011926)------------------------------ % 3.15/0.77 % (4011926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.15/0.77 % (4011926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.15/0.77 % (4011926)CaDiCaL version: 2.1.3 % 3.15/0.77 % (4011926)Termination reason: Instruction limit % 3.15/0.77 % (4011926)Termination phase: Saturation % 3.15/0.77 % (4011926)Time elapsed: 0.035 s % 3.15/0.77 % (4011926)Peak memory usage: 13 MB % 3.15/0.77 % (4011926)Instructions burned: 105 (million) % 3.15/0.77 % (4011940)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=1636337182:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.15/0.77 % (4011939)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=18173871:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.15/0.77 % (4011927)Instruction limit reached! % 3.15/0.77 % (4011927)------------------------------ % 3.15/0.77 % (4011927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.15/0.77 % (4011927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.15/0.77 % (4011927)CaDiCaL version: 2.1.3 % 3.15/0.77 % (4011927)Termination reason: Instruction limit % 3.15/0.77 % (4011927)Termination phase: Saturation % 3.15/0.77 % (4011927)Time elapsed: 0.075 s % 3.15/0.77 % (4011927)Peak memory usage: 13 MB % 3.15/0.77 % (4011927)Instructions burned: 117 (million) % 3.15/0.77 % (4011928)Instruction limit reached! % 3.15/0.77 % (4011928)------------------------------ % 3.15/0.77 % (4011928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.13 % (4011928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.13 % (4011928)CaDiCaL version: 2.1.3 % 5.63/1.13 % (4011928)Termination reason: Instruction limit % 5.63/1.13 % (4011928)Termination phase: Saturation % 5.63/1.13 % (4011928)Time elapsed: 0.083 s % 5.63/1.13 % (4011928)Peak memory usage: 13 MB % 5.63/1.13 % (4011928)Instructions burned: 131 (million) % 5.63/1.13 % (4011943)ott-21_1_sil=16000:fs=off:random_seed=3710699884:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.63/1.13 % (4011929)Instruction limit reached! % 5.63/1.13 % (4011929)------------------------------ % 5.63/1.13 % (4011929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.13 % (4011944)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1902389770:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.63/1.13 % (4011929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.13 % (4011929)CaDiCaL version: 2.1.3 % 5.63/1.13 % (4011929)Termination reason: Instruction limit % 5.63/1.13 % (4011929)Termination phase: Saturation % 5.63/1.13 % (4011929)Time elapsed: 0.101 s % 5.63/1.13 % (4011929)Peak memory usage: 13 MB % 5.63/1.13 % (4011929)Instructions burned: 159 (million) % 5.63/1.13 % (4011947)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1295733728:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.63/1.13 % (4011947)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.63/1.13 % (4011947)Terminated due to inappropriate strategy. % 5.63/1.13 % (4011947)------------------------------ % 5.63/1.13 % (4011947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.13 % (4011947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.13 % (4011947)CaDiCaL version: 2.1.3 % 5.63/1.13 % (4011947)Termination reason: Inappropriate % 5.63/1.13 % (4011947)Time elapsed: 0.003 s % 5.63/1.13 % (4011947)Peak memory usage: 11 MB % 5.63/1.13 % (4011947)Instructions burned: 5 (million) % 5.63/1.13 % (4011947)------------------------------ % 5.63/1.13 % (4011947)------------------------------ % 5.63/1.13 % (4011939)Instruction limit reached! % 5.63/1.13 % (4011939)------------------------------ % 5.63/1.13 % (4011939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.13 % (4011939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.13 % (4011939)CaDiCaL version: 2.1.3 % 5.63/1.13 % (4011939)Termination reason: Instruction limit % 5.63/1.13 % (4011939)Termination phase: Saturation % 5.63/1.13 % (4011939)Time elapsed: 0.094 s % 5.63/1.13 % (4011939)Peak memory usage: 14 MB % 5.63/1.13 % (4011939)Instructions burned: 132 (million) % 5.63/1.13 % (4011949)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3259642890:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.63/1.13 % (4011950)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3692315466:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.63/1.13 % (4011950)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.63/1.13 % (4011950)Terminated due to inappropriate strategy. % 5.63/1.13 % (4011950)------------------------------ % 5.63/1.13 % (4011950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.13 % (4011950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.13 % (4011950)CaDiCaL version: 2.1.3 % 5.63/1.13 % (4011950)Termination reason: Inappropriate % 5.63/1.13 % (4011950)Time elapsed: 0.003 s % 5.63/1.13 % (4011950)Peak memory usage: 11 MB % 5.63/1.13 % (4011950)Instructions burned: 5 (million) % 5.63/1.13 % (4011950)------------------------------ % 5.63/1.13 % (4011950)------------------------------ % 5.63/1.13 % (4011953)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=1292040931: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.63/1.13 % (4011943)Instruction limit reached! % 5.63/1.13 % (4011943)------------------------------ % 5.63/1.13 % (4011943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.13 % (4011943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.13 % (4011943)CaDiCaL version: 2.1.3 % 5.63/1.13 % (4011943)Termination reason: Instruction limit % 5.63/1.13 % (4011943)Termination phase: Saturation % 18.08/2.90 % (4011943)Time elapsed: 0.090 s % 18.08/2.90 % (4011943)Peak memory usage: 13 MB % 18.08/2.90 % (4011943)Instructions burned: 181 (million) % 18.08/2.90 % (4011955)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=642340717:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 18.08/2.90 % (4011940)Instruction limit reached! % 18.08/2.90 % (4011940)------------------------------ % 18.08/2.90 % (4011940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.08/2.90 % (4011940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.08/2.90 % (4011940)CaDiCaL version: 2.1.3 % 18.08/2.90 % (4011940)Termination reason: Instruction limit % 18.08/2.90 % (4011940)Termination phase: Saturation % 18.08/2.90 % (4011940)Time elapsed: 0.215 s % 18.08/2.90 % (4011940)Peak memory usage: 17 MB % 18.08/2.90 % (4011940)Instructions burned: 687 (million) % 18.08/2.90 % (4011957)fmb+10_1_sil=64000:random_seed=3892009432:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 18.08/2.90 % (4011957)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.08/2.90 % (4011957)Terminated due to inappropriate strategy. % 18.08/2.90 % (4011957)------------------------------ % 18.08/2.90 % (4011957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.08/2.90 % (4011957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.08/2.90 % (4011957)CaDiCaL version: 2.1.3 % 18.08/2.90 % (4011957)Termination reason: Inappropriate % 18.08/2.90 % (4011957)Time elapsed: 0.003 s % 18.08/2.90 % (4011957)Peak memory usage: 11 MB % 18.08/2.90 % (4011957)Instructions burned: 5 (million) % 18.08/2.90 % (4011957)------------------------------ % 18.08/2.90 % (4011957)------------------------------ % 18.08/2.90 % (4011959)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3150272758:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 18.08/2.90 % (4011959)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.08/2.90 % (4011959)Terminated due to inappropriate strategy. % 18.08/2.90 % (4011959)------------------------------ % 18.08/2.90 % (4011959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.08/2.90 % (4011959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.08/2.90 % (4011959)CaDiCaL version: 2.1.3 % 18.08/2.90 % (4011959)Termination reason: Inappropriate % 18.08/2.90 % (4011959)Time elapsed: 0.003 s % 18.08/2.90 % (4011959)Peak memory usage: 11 MB % 18.08/2.90 % (4011959)Instructions burned: 5 (million) % 18.08/2.90 % (4011959)------------------------------ % 18.08/2.90 % (4011959)------------------------------ % 18.08/2.90 % (4011961)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1206410755:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 18.08/2.90 % (4011961)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.08/2.90 % (4011961)Terminated due to inappropriate strategy. % 18.08/2.90 % (4011961)------------------------------ % 18.08/2.90 % (4011961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.08/2.90 % (4011961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.08/2.90 % (4011961)CaDiCaL version: 2.1.3 % 18.08/2.90 % (4011961)Termination reason: Inappropriate % 18.08/2.90 % (4011961)Time elapsed: 0.003 s % 18.08/2.90 % (4011961)Peak memory usage: 11 MB % 18.08/2.90 % (4011961)Instructions burned: 5 (million) % 18.08/2.90 % (4011961)------------------------------ % 18.08/2.90 % (4011961)------------------------------ % 18.08/2.90 % (4011963)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=157049367:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 18.08/2.90 % (4011944)Instruction limit reached! % 18.08/2.90 % (4011944)------------------------------ % 18.08/2.90 % (4011944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.08/2.90 % (4011944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.08/2.90 % (4011944)CaDiCaL version: 2.1.3 % 18.08/2.90 % (4011944)Termination reason: Instruction limit % 18.08/2.90 % (4011944)Termination phase: Saturation % 18.08/2.90 % (4011944)Time elapsed: 0.307 s % 18.08/2.90 % (4011944)Peak memory usage: 15 MB % 18.08/2.90 % (4011944)Instructions burned: 478 (million) % 18.08/2.90 % (4011965)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1956833941:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 18.08/2.90 % (4011955)Instruction limit reached! % 18.08/2.90 % (4011955)------------------------------ % 23.95/3.73 % (4011955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.95/3.73 % (4011955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.95/3.73 % (4011955)CaDiCaL version: 2.1.3 % 23.95/3.73 % (4011955)Termination reason: Instruction limit % 23.95/3.73 % (4011955)Termination phase: Saturation % 23.95/3.73 % (4011955)Time elapsed: 0.294 s % 23.95/3.73 % (4011955)Peak memory usage: 19 MB % 23.95/3.73 % (4011955)Instructions burned: 882 (million) % 23.95/3.73 % (4011967)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=172455935:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 23.95/3.73 % (4011967)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.95/3.73 % (4011967)Terminated due to inappropriate strategy. % 23.95/3.73 % (4011967)------------------------------ % 23.95/3.73 % (4011967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.95/3.73 % (4011967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.95/3.73 % (4011967)CaDiCaL version: 2.1.3 % 23.95/3.73 % (4011967)Termination reason: Inappropriate % 23.95/3.73 % (4011967)Time elapsed: 0.001 s % 23.95/3.73 % (4011967)Peak memory usage: 11 MB % 23.95/3.73 % (4011967)Instructions burned: 5 (million) % 23.95/3.73 % (4011967)------------------------------ % 23.95/3.73 % (4011967)------------------------------ % 23.95/3.73 % (4011969)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3242571013:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 23.95/3.73 % (4011969)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.95/3.73 % (4011969)Terminated due to inappropriate strategy. % 23.95/3.73 % (4011969)------------------------------ % 23.95/3.73 % (4011969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.95/3.73 % (4011969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.95/3.73 % (4011969)CaDiCaL version: 2.1.3 % 23.95/3.73 % (4011969)Termination reason: Inappropriate % 23.95/3.73 % (4011969)Time elapsed: 0.001 s % 23.95/3.73 % (4011969)Peak memory usage: 11 MB % 23.95/3.73 % (4011969)Instructions burned: 5 (million) % 23.95/3.73 % (4011969)------------------------------ % 23.95/3.73 % (4011969)------------------------------ % 23.95/3.73 % (4011971)ott-2_1_sil=16000:newcnf=on:random_seed=490945244:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 23.95/3.73 % (4011953)Instruction limit reached! % 23.95/3.73 % (4011953)------------------------------ % 23.95/3.73 % (4011953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.95/3.73 % (4011953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.95/3.73 % (4011953)CaDiCaL version: 2.1.3 % 23.95/3.73 % (4011953)Termination reason: Instruction limit % 23.95/3.73 % (4011953)Termination phase: Saturation % 23.95/3.73 % (4011953)Time elapsed: 0.438 s % 23.95/3.73 % (4011953)Peak memory usage: 21 MB % 23.95/3.73 % (4011953)Instructions burned: 692 (million) % 23.95/3.73 % (4011973)ott+10_1_sil=32000:tgt=ground:random_seed=3635629996:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 23.95/3.73 % (4011949)Instruction limit reached! % 23.95/3.73 % (4011949)------------------------------ % 23.95/3.73 % (4011949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.95/3.73 % (4011949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.95/3.73 % (4011949)CaDiCaL version: 2.1.3 % 23.95/3.73 % (4011949)Termination reason: Instruction limit % 23.95/3.73 % (4011949)Termination phase: Saturation % 23.95/3.73 % (4011949)Time elapsed: 0.691 s % 23.95/3.73 % (4011949)Peak memory usage: 21 MB % 23.95/3.73 % (4011949)Instructions burned: 1180 (million) % 23.95/3.73 % (4011975)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1652633173:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 23.95/3.73 % (4011975)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.95/3.73 % (4011975)Terminated due to inappropriate strategy. % 23.95/3.73 % (4011975)------------------------------ % 23.95/3.73 % (4011975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.95/3.73 % (4011975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.95/3.73 % (4011975)CaDiCaL version: 2.1.3 % 23.95/3.73 % (4011975)Termination reason: Inappropriate % 23.95/3.73 % (4011975)Time elapsed: 0.003 s % 23.95/3.73 % (4011975)Peak memory usage: 11 MB % 23.95/3.73 % (4011975)Instructions burned: 5 (million) % 90.81/13.11 % (4011975)------------------------------ % 90.81/13.11 % (4011975)------------------------------ % 90.81/13.11 % (4011971)Instruction limit reached! % 90.81/13.11 % (4011971)------------------------------ % 90.81/13.11 % (4011971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.81/13.11 % (4011971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.81/13.11 % (4011971)CaDiCaL version: 2.1.3 % 90.81/13.11 % (4011971)Termination reason: Instruction limit % 90.81/13.11 % (4011971)Termination phase: Saturation % 90.81/13.11 % (4011971)Time elapsed: 0.315 s % 90.81/13.11 % (4011971)Peak memory usage: 20 MB % 90.81/13.11 % (4011971)Instructions burned: 870 (million) % 90.81/13.11 % (4011978)dis+21_1_sil=32000:sas=cadical:random_seed=3725259965:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 90.81/13.11 % (4011977)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3538774757:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 90.81/13.11 % (4011965)Instruction limit reached! % 90.81/13.11 % (4011965)------------------------------ % 90.81/13.11 % (4011965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.81/13.11 % (4011965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.81/13.11 % (4011965)CaDiCaL version: 2.1.3 % 90.81/13.11 % (4011965)Termination reason: Instruction limit % 90.81/13.11 % (4011965)Termination phase: Saturation % 90.81/13.11 % (4011965)Time elapsed: 0.846 s % 90.81/13.11 % (4011965)Peak memory usage: 26 MB % 90.81/13.11 % (4011965)Instructions burned: 1473 (million) % 90.81/13.11 % (4011981)ott+11_1_sil=16000:gs=on:random_seed=3843164737:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 90.81/13.11 % (4011978)Instruction limit reached! % 90.81/13.11 % (4011978)------------------------------ % 90.81/13.11 % (4011978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.81/13.11 % (4011978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.81/13.11 % (4011978)CaDiCaL version: 2.1.3 % 90.81/13.11 % (4011978)Termination reason: Instruction limit % 90.81/13.11 % (4011978)Termination phase: Saturation % 90.81/13.11 % (4011978)Time elapsed: 1.005 s % 90.81/13.11 % (4011978)Peak memory usage: 34 MB % 90.81/13.11 % (4011978)Instructions burned: 3775 (million) % 90.81/13.11 % (4011983)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3671491619:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 90.81/13.11 % (4011983)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 90.81/13.11 % (4011983)Terminated due to inappropriate strategy. % 90.81/13.11 % (4011983)------------------------------ % 90.81/13.11 % (4011983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.81/13.11 % (4011983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.81/13.11 % (4011983)CaDiCaL version: 2.1.3 % 90.81/13.11 % (4011983)Termination reason: Inappropriate % 90.81/13.11 % (4011983)Time elapsed: 0.001 s % 90.81/13.11 % (4011983)Peak memory usage: 11 MB % 90.81/13.11 % (4011983)Instructions burned: 5 (million) % 90.81/13.11 % (4011983)------------------------------ % 90.81/13.11 % (4011983)------------------------------ % 90.81/13.11 % (4011985)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=736725587:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 90.81/13.11 % (4011981)Instruction limit reached! % 90.81/13.11 % (4011981)------------------------------ % 90.81/13.11 % (4011981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.81/13.11 % (4011981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.81/13.11 % (4011981)CaDiCaL version: 2.1.3 % 90.81/13.11 % (4011981)Termination reason: Instruction limit % 90.81/13.11 % (4011981)Termination phase: Saturation % 90.81/13.11 % (4011981)Time elapsed: 1.267 s % 90.81/13.11 % (4011981)Peak memory usage: 29 MB % 90.81/13.11 % (4011981)Instructions burned: 2252 (million) % 90.81/13.11 % (4011987)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3918437486:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 90.81/13.11 % (4011977)Instruction limit reached! % 90.81/13.11 % (4011977)------------------------------ % 90.81/13.11 % (4011977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.81/13.11 % (4011977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.81/13.11 % (4011977)CaDiCaL version: 2.1.3 % 90.81/13.11 % (4011977)Termination reason: Instruction limit % 95.45/17.05 % (4011977)Termination phase: Saturation % 95.45/17.05 % (4011977)Time elapsed: 1.751 s % 95.45/17.05 % (4011977)Peak memory usage: 33 MB % 95.45/17.05 % (4011977)Instructions burned: 3513 (million) % 95.45/17.05 % (4011989)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3152872461:i=5211_2973 on theBenchmark for (2973ds/5211Mi) % 95.45/17.05 % (4011963)Instruction limit reached! % 95.45/17.05 % (4011963)------------------------------ % 95.45/17.05 % (4011963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.45/17.05 % (4011963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.45/17.05 % (4011963)CaDiCaL version: 2.1.3 % 95.45/17.05 % (4011963)Termination reason: Instruction limit % 95.45/17.05 % (4011963)Termination phase: Saturation % 95.45/17.05 % (4011963)Time elapsed: 2.491 s % 95.45/17.05 % (4011963)Peak memory usage: 39 MB % 95.45/17.05 % (4011963)Instructions burned: 5132 (million) % 95.45/17.05 % (4011991)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2090384965:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi) % 95.45/17.05 % (4011991)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 95.45/17.05 % (4011991)Terminated due to inappropriate strategy. % 95.45/17.05 % (4011991)------------------------------ % 95.45/17.05 % (4011991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.45/17.05 % (4011991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.45/17.05 % (4011991)CaDiCaL version: 2.1.3 % 95.45/17.05 % (4011991)Termination reason: Inappropriate % 95.45/17.05 % (4011991)Time elapsed: 0.003 s % 95.45/17.05 % (4011991)Peak memory usage: 11 MB % 95.45/17.05 % (4011991)Instructions burned: 5 (million) % 95.45/17.05 % (4011991)------------------------------ % 95.45/17.05 % (4011991)------------------------------ % 95.45/17.05 % (4011993)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3697845719:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi) % 95.45/17.05 % (4011993)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 95.45/17.05 % (4011993)Terminated due to inappropriate strategy. % 95.45/17.05 % (4011993)------------------------------ % 95.45/17.05 % (4011993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.45/17.05 % (4011993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.45/17.05 % (4011993)CaDiCaL version: 2.1.3 % 95.45/17.05 % (4011993)Termination reason: Inappropriate % 95.45/17.05 % (4011993)Time elapsed: 0.003 s % 95.45/17.05 % (4011993)Peak memory usage: 11 MB % 95.45/17.05 % (4011993)Instructions burned: 5 (million) % 95.45/17.05 % (4011993)------------------------------ % 95.45/17.05 % (4011993)------------------------------ % 95.45/17.05 % (4011995)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1338571368:i=14071_2970 on theBenchmark for (2970ds/14071Mi) % 95.45/17.05 % (4011995)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 95.45/17.05 % (4011995)Terminated due to inappropriate strategy. % 95.45/17.05 % (4011995)------------------------------ % 95.45/17.05 % (4011995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.45/17.05 % (4011995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.45/17.05 % (4011995)CaDiCaL version: 2.1.3 % 95.45/17.05 % (4011995)Termination reason: Inappropriate % 95.45/17.05 % (4011995)Time elapsed: 0.003 s % 95.45/17.05 % (4011995)Peak memory usage: 11 MB % 95.45/17.05 % (4011995)Instructions burned: 5 (million) % 95.45/17.05 % (4011995)------------------------------ % 95.45/17.05 % (4011995)------------------------------ % 95.45/17.05 % (4011997)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=147350986:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 95.45/17.05 % (4011985)Instruction limit reached! % 95.45/17.05 % (4011985)------------------------------ % 95.45/17.05 % (4011985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.45/17.05 % (4011985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.45/17.05 % (4011985)CaDiCaL version: 2.1.3 % 95.45/17.05 % (4011985)Termination reason: Instruction limit % 95.45/17.05 % (4011985)Termination phase: Saturation % 95.45/17.05 % (4011985)Time elapsed: 1.423 s % 95.45/17.05 % (4011985)Peak memory usage: 43 MB % 95.45/17.05 % (4011985)Instructions burned: 4593 (million) % 95.45/17.05 % (4011999)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1978499306:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 95.45/17.05 % (4011973)Instruction limit reached! % 121.07/17.30 % (4011973)------------------------------ % 121.07/17.30 % (4011973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.07/17.30 % (4011973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.07/17.30 % (4011973)CaDiCaL version: 2.1.3 % 121.07/17.30 % (4011973)Termination reason: Instruction limit % 121.07/17.30 % (4011973)Termination phase: Saturation % 121.07/17.30 % (4011973)Time elapsed: 2.821 s % 121.07/17.30 % (4011973)Peak memory usage: 50 MB % 121.07/17.30 % (4011973)Instructions burned: 5114 (million) % 121.07/17.30 % (4012001)dis+10_16:1_sil=16000:random_seed=2190415733:i=9155:fsr=off_2964 on theBenchmark for (2964ds/9155Mi) % 121.07/17.30 % (4011989)Instruction limit reached! % 121.07/17.30 % (4011989)------------------------------ % 121.07/17.30 % (4011989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.07/17.30 % (4011989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.07/17.30 % (4011989)CaDiCaL version: 2.1.3 % 121.07/17.30 % (4011989)Termination reason: Instruction limit % 121.07/17.30 % (4011989)Termination phase: Saturation % 121.07/17.30 % (4011989)Time elapsed: 2.643 s % 121.07/17.30 % (4011989)Peak memory usage: 48 MB % 121.07/17.30 % (4011989)Instructions burned: 5211 (million) % 121.07/17.30 % (4012003)ott-3_8_sil=64000:random_seed=3626911054:i=20139:bs=on_2946 on theBenchmark for (2946ds/20139Mi) % 121.07/17.30 % (4011999)Instruction limit reached! % 121.07/17.30 % (4011999)------------------------------ % 121.07/17.30 % (4011999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.07/17.30 % (4011999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.07/17.30 % (4011999)CaDiCaL version: 2.1.3 % 121.07/17.30 % (4011999)Termination reason: Instruction limit % 121.07/17.30 % (4011999)Termination phase: Saturation % 121.07/17.30 % (4011999)Time elapsed: 2.368 s % 121.07/17.30 % (4011999)Peak memory usage: 75 MB % 121.07/17.30 % (4011999)Instructions burned: 8175 (million) % 121.07/17.30 % (4012005)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2139370444:fmbsr=2:i=32576_2942 on theBenchmark for (2942ds/32576Mi) % 121.07/17.30 % (4012005)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.07/17.30 % (4012005)Terminated due to inappropriate strategy. % 121.07/17.30 % (4012005)------------------------------ % 121.07/17.30 % (4012005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.07/17.30 % (4012005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.07/17.30 % (4012005)CaDiCaL version: 2.1.3 % 121.07/17.30 % (4012005)Termination reason: Inappropriate % 121.07/17.30 % (4012005)Time elapsed: 0.001 s % 121.07/17.30 % (4012005)Peak memory usage: 11 MB % 121.07/17.30 % (4012005)Instructions burned: 5 (million) % 121.07/17.30 % (4012005)------------------------------ % 121.07/17.30 % (4012005)------------------------------ % 121.07/17.30 % (4012007)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3281623568:i=11404_2942 on theBenchmark for (2942ds/11404Mi) % 121.07/17.30 % (4012001)Instruction limit reached! % 121.07/17.30 % (4012001)------------------------------ % 121.07/17.30 % (4012001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.07/17.30 % (4012001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.07/17.30 % (4012001)CaDiCaL version: 2.1.3 % 121.07/17.30 % (4012001)Termination reason: Instruction limit % 121.07/17.30 % (4012001)Termination phase: Saturation % 121.07/17.30 % (4012001)Time elapsed: 4.615 s % 121.07/17.30 % (4012001)Peak memory usage: 57 MB % 121.07/17.30 % (4012001)Instructions burned: 9156 (million) % 121.07/17.30 % (4012009)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3799781052:i=14134_2918 on theBenchmark for (2918ds/14134Mi) % 121.07/17.30 % (4012007)Instruction limit reached! % 121.07/17.30 % (4012007)------------------------------ % 121.07/17.30 % (4012007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.07/17.30 % (4012007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.07/17.30 % (4012007)CaDiCaL version: 2.1.3 % 121.07/17.30 % (4012007)Termination reason: Instruction limit % 121.07/17.30 % (4012007)Termination phase: Saturation % 121.07/17.30 % (4012007)Time elapsed: 3.395 s % 121.07/17.30 % (4012007)Peak memory usage: 91 MB % 121.07/17.30 % (4012007)Instructions burned: 11404 (million) % 121.07/17.30 % (4012011)dis+33_16_sil=32000:sac=on:random_seed=1906293614:i=15851:nm=0_2908 on theBenchmark for (2908ds/15851Mi) % 121.07/17.30 % (4012011)Instruction limit reached! % 121.07/17.30 % (4012011)------------------------------ % 121.07/17.30 % (4012011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.07/20.44 % (4012011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.07/20.44 % (4012011)CaDiCaL version: 2.1.3 % 143.07/20.44 % (4012011)Termination reason: Instruction limit % 143.07/20.44 % (4012011)Termination phase: Saturation % 143.07/20.44 % (4012011)Time elapsed: 3.675 s % 143.07/20.44 % (4012011)Peak memory usage: 24 MB % 143.07/20.44 % (4012011)Instructions burned: 15854 (million) % 143.07/20.44 % (4012013)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3004804727:avsq=on:i=17627:add=on:amm=off_2871 on theBenchmark for (2871ds/17627Mi) % 143.07/20.44 % (4011997)Instruction limit reached! % 143.07/20.44 % (4011997)------------------------------ % 143.07/20.44 % (4011997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.07/20.44 % (4011997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.07/20.44 % (4011997)CaDiCaL version: 2.1.3 % 143.07/20.44 % (4011997)Termination reason: Instruction limit % 143.07/20.44 % (4011997)Termination phase: Saturation % 143.07/20.44 % (4011997)Time elapsed: 10.812 s % 143.07/20.44 % (4011997)Peak memory usage: 508 MB % 143.07/20.44 % (4011997)Instructions burned: 22566 (million) % 143.07/20.44 % (4012062)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2473302487:s2a=on:i=53295_2861 on theBenchmark for (2861ds/53295Mi) % 143.07/20.44 % (4011987)Instruction limit reached! % 143.07/20.44 % (4011987)------------------------------ % 143.07/20.44 % (4011987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.07/20.44 % (4011987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.07/20.44 % (4011987)CaDiCaL version: 2.1.3 % 143.07/20.44 % (4011987)Termination reason: Instruction limit % 143.07/20.44 % (4011987)Termination phase: Saturation % 143.07/20.44 % (4011987)Time elapsed: 14.028 s % 143.07/20.44 % (4011987)Peak memory usage: 185 MB % 143.07/20.44 % (4011987)Instructions burned: 29342 (million) % 143.07/20.44 % (4012009)Instruction limit reached! % 143.07/20.44 % (4012009)------------------------------ % 143.07/20.44 % (4012009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.07/20.44 % (4012009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.07/20.44 % (4012009)CaDiCaL version: 2.1.3 % 143.07/20.44 % (4012009)Termination reason: Instruction limit % 143.07/20.44 % (4012009)Termination phase: Saturation % 143.07/20.44 % (4012009)Time elapsed: 8.488 s % 143.07/20.44 % (4012009)Peak memory usage: 108 MB % 143.07/20.44 % (4012009)Instructions burned: 14134 (million) % 143.07/20.44 % (4012323)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2223732333:i=28120:bs=on:fsr=off_2833 on theBenchmark for (2833ds/28120Mi) % 143.07/20.44 % (4012322)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=271707606:i=26857:ins=20_2833 on theBenchmark for (2833ds/26857Mi) % 143.07/20.44 % (4012322)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.07/20.44 % (4012322)Terminated due to inappropriate strategy. % 143.07/20.44 % (4012322)------------------------------ % 143.07/20.44 % (4012322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.07/20.44 % (4012322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.07/20.44 % (4012322)CaDiCaL version: 2.1.3 % 143.07/20.44 % (4012322)Termination reason: Inappropriate % 143.07/20.44 % (4012322)Time elapsed: 0.004 s % 143.07/20.44 % (4012322)Peak memory usage: 11 MB % 143.07/20.44 % (4012322)Instructions burned: 5 (million) % 143.07/20.44 % (4012322)------------------------------ % 143.07/20.44 % (4012322)------------------------------ % 143.07/20.44 % (4012328)fmb+10_1_sil=256000:fmbss=7:random_seed=137174403:fmbsr=1.6:i=182295_2832 on theBenchmark for (2832ds/182295Mi) % 143.07/20.44 % (4012328)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.07/20.44 % (4012328)Terminated due to inappropriate strategy. % 143.07/20.44 % (4012328)------------------------------ % 143.07/20.44 % (4012328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.07/20.44 % (4012328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.07/20.44 % (4012328)CaDiCaL version: 2.1.3 % 143.07/20.44 % (4012328)Termination reason: Inappropriate % 143.07/20.44 % (4012328)Time elapsed: 0.004 s % 143.07/20.44 % (4012328)Peak memory usage: 11 MB % 143.07/20.44 % (4012328)Instructions burned: 5 (million) % 143.07/20.44 % (4012328)------------------------------ % 143.07/20.44 % (4012328)------------------------------ % 143.07/20.44 % (4012331)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=983128542:i=44625:gsp=on_2832 on theBenchmark for (2832ds/44625Mi) % 149.97/21.45 % (4012331)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.97/21.45 % (4012331)Terminated due to inappropriate strategy. % 149.97/21.45 % (4012331)------------------------------ % 149.97/21.45 % (4012331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.97/21.45 % (4012331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.97/21.45 % (4012331)CaDiCaL version: 2.1.3 % 149.97/21.45 % (4012331)Termination reason: Inappropriate % 149.97/21.45 % (4012331)Time elapsed: 0.004 s % 149.97/21.45 % (4012331)Peak memory usage: 11 MB % 149.97/21.45 % (4012331)Instructions burned: 5 (million) % 149.97/21.45 % (4012331)------------------------------ % 149.97/21.45 % (4012331)------------------------------ % 149.97/21.45 % (4012335)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1156750594:i=160505_2831 on theBenchmark for (2831ds/160505Mi) % 149.97/21.45 % (4012335)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.97/21.45 % (4012335)Terminated due to inappropriate strategy. % 149.97/21.45 % (4012335)------------------------------ % 149.97/21.45 % (4012335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.97/21.45 % (4012335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.97/21.45 % (4012335)CaDiCaL version: 2.1.3 % 149.97/21.45 % (4012335)Termination reason: Inappropriate % 149.97/21.45 % (4012335)Time elapsed: 0.005 s % 149.97/21.45 % (4012335)Peak memory usage: 11 MB % 149.97/21.45 % (4012335)Instructions burned: 5 (million) % 149.97/21.45 % (4012335)------------------------------ % 149.97/21.45 % (4012335)------------------------------ % 149.97/21.45 % (4012339)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=111056163:fmbsr=1.3:i=225729_2831 on theBenchmark for (2831ds/225729Mi) % 149.97/21.45 % (4012339)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.97/21.45 % (4012339)Terminated due to inappropriate strategy. % 149.97/21.45 % (4012339)------------------------------ % 149.97/21.45 % (4012339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.97/21.45 % (4012339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.97/21.45 % (4012339)CaDiCaL version: 2.1.3 % 149.97/21.45 % (4012339)Termination reason: Inappropriate % 149.97/21.45 % (4012339)Time elapsed: 0.006 s % 149.97/21.45 % (4012339)Peak memory usage: 11 MB % 149.97/21.45 % (4012339)Instructions burned: 5 (million) % 149.97/21.45 % (4012339)------------------------------ % 149.97/21.45 % (4012339)------------------------------ % 149.97/21.45 % (4012344)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3088920997:fmbsr=2:i=185024:ins=7_2830 on theBenchmark for (2830ds/185024Mi) % 149.97/21.45 % (4012344)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.97/21.45 % (4012344)Terminated due to inappropriate strategy. % 149.97/21.45 % (4012344)------------------------------ % 149.97/21.45 % (4012344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.97/21.45 % (4012344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.97/21.45 % (4012344)CaDiCaL version: 2.1.3 % 149.97/21.45 % (4012344)Termination reason: Inappropriate % 149.97/21.45 % (4012344)Time elapsed: 0.006 s % 149.97/21.45 % (4012344)Peak memory usage: 11 MB % 149.97/21.45 % (4012344)Instructions burned: 5 (million) % 149.97/21.45 % (4012344)------------------------------ % 149.97/21.45 % (4012344)------------------------------ % 149.97/21.45 % (4012348)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4079272231:rtra=on_2830 on theBenchmark for (2830ds/0Mi) % 149.97/21.45 % (4012348)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.97/21.45 % (4012348)Terminated due to inappropriate strategy. % 149.97/21.45 % (4012348)------------------------------ % 149.97/21.45 % (4012348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.97/21.45 % (4012348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.97/21.45 % (4012348)CaDiCaL version: 2.1.3 % 149.97/21.45 % (4012348)Termination reason: Inappropriate % 149.97/21.45 % (4012348)Time elapsed: 0.006 s % 149.97/21.45 % (4012348)Peak memory usage: 11 MB % 149.97/21.45 % (4012348)Instructions burned: 5 (million) % 149.97/21.45 % (4012348)------------------------------ % 149.97/21.45 % (4012348)------------------------------ % 149.97/21.45 % (4012351)% WARNING: option uhcvi not known. % 149.97/21.45 % (4012351)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3713325215:i=271062:add=off:rtra=on:rawr=on_2829 on theBenchmark for (2829ds/271062Mi) % 163.73/23.35 % (4012003)Instruction limit reached! % 163.73/23.35 % (4012003)------------------------------ % 163.73/23.35 % (4012003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.73/23.35 % (4012003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.73/23.35 % (4012003)CaDiCaL version: 2.1.3 % 163.73/23.35 % (4012003)Termination reason: Instruction limit % 163.73/23.35 % (4012003)Termination phase: Saturation % 163.73/23.35 % (4012003)Time elapsed: 13.062 s % 163.73/23.35 % (4012003)Peak memory usage: 119 MB % 163.73/23.35 % (4012003)Instructions burned: 20140 (million) % 163.73/23.35 % (4012390)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2821017807:i=176048:add=on:rtra=on:rawr=on_2815 on theBenchmark for (2815ds/176048Mi) % 163.73/23.35 % (4012013)Instruction limit reached! % 163.73/23.35 % (4012013)------------------------------ % 163.73/23.35 % (4012013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.73/23.35 % (4012013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.73/23.35 % (4012013)CaDiCaL version: 2.1.3 % 163.73/23.35 % (4012013)Termination reason: Instruction limit % 163.73/23.35 % (4012013)Termination phase: Saturation % 163.73/23.35 % (4012013)Time elapsed: 6.899 s % 163.73/23.35 % (4012013)Peak memory usage: 196 MB % 163.73/23.35 % (4012013)Instructions burned: 17628 (million) % 163.73/23.35 % (4012432)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2107291460:i=206:fgj=on:rtra=on_2801 on theBenchmark for (2801ds/206Mi) % 163.73/23.35 % (4012432)Instruction limit reached! % 163.73/23.35 % (4012432)------------------------------ % 163.73/23.35 % (4012432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.73/23.35 % (4012432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.73/23.35 % (4012432)CaDiCaL version: 2.1.3 % 163.73/23.35 % (4012432)Termination reason: Instruction limit % 163.73/23.35 % (4012432)Termination phase: Saturation % 163.73/23.35 % (4012432)Time elapsed: 0.070 s % 163.73/23.35 % (4012432)Peak memory usage: 14 MB % 163.73/23.35 % (4012432)Instructions burned: 206 (million) % 163.73/23.35 % (4012465)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=359155786:i=232:rtra=on_2801 on theBenchmark for (2801ds/232Mi) % 163.73/23.35 % (4012465)Instruction limit reached! % 163.73/23.35 % (4012465)------------------------------ % 163.73/23.35 % (4012465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.73/23.35 % (4012465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.73/23.35 % (4012465)CaDiCaL version: 2.1.3 % 163.73/23.35 % (4012465)Termination reason: Instruction limit % 163.73/23.35 % (4012465)Termination phase: Saturation % 163.73/23.35 % (4012465)Time elapsed: 0.080 s % 163.73/23.35 % (4012465)Peak memory usage: 14 MB % 163.73/23.35 % (4012465)Instructions burned: 232 (million) % 163.73/23.35 % (4012502)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1576285653:i=262:rtra=on_2800 on theBenchmark for (2800ds/262Mi) % 163.73/23.35 % (4012502)Instruction limit reached! % 163.73/23.35 % (4012502)------------------------------ % 163.73/23.35 % (4012502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.73/23.35 % (4012502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.73/23.35 % (4012502)CaDiCaL version: 2.1.3 % 163.73/23.35 % (4012502)Termination reason: Instruction limit % 163.73/23.35 % (4012502)Termination phase: Saturation % 163.73/23.35 % (4012502)Time elapsed: 0.081 s % 163.73/23.35 % (4012502)Peak memory usage: 14 MB % 163.73/23.35 % (4012502)Instructions burned: 264 (million) % 163.73/23.35 % (4012525)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2674603083:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2799 on theBenchmark for (2799ds/318Mi) % 163.73/23.35 % (4012525)Instruction limit reached! % 163.73/23.35 % (4012525)------------------------------ % 163.73/23.35 % (4012525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.73/23.35 % (4012525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.73/23.35 % (4012525)CaDiCaL version: 2.1.3 % 163.73/23.35 % (4012525)Termination reason: Instruction limit % 163.73/23.35 % (4012525)Termination phase: Saturation % 163.73/23.35 % (4012525)Time elapsed: 0.109 s % 163.73/23.35 % (4012525)Peak memory usage: 14 MB % 163.73/23.35 % (4012525)Instructions burned: 320 (million) % 163.73/23.35 % (4012542)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2405709812:i=1428:nm=2:rtra=on_2798 on theBenchmark for (2798ds/1428Mi) % 192.81/27.47 % (4012542)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.81/27.47 % (4012542)Terminated due to inappropriate strategy. % 192.81/27.47 % (4012542)------------------------------ % 192.81/27.47 % (4012542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.81/27.47 % (4012542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.81/27.47 % (4012542)CaDiCaL version: 2.1.3 % 192.81/27.47 % (4012542)Termination reason: Inappropriate % 192.81/27.47 % (4012542)Time elapsed: 0.002 s % 192.81/27.47 % (4012542)Peak memory usage: 11 MB % 192.81/27.47 % (4012542)Instructions burned: 5 (million) % 192.81/27.47 % (4012542)------------------------------ % 192.81/27.47 % (4012542)------------------------------ % 192.81/27.47 % (4012553)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=860155549:i=262:bd=preordered:rtra=on:fsd=on_2797 on theBenchmark for (2797ds/262Mi) % 192.81/27.47 % (4012553)Instruction limit reached! % 192.81/27.47 % (4012553)------------------------------ % 192.81/27.47 % (4012553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.81/27.47 % (4012553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.81/27.47 % (4012553)CaDiCaL version: 2.1.3 % 192.81/27.47 % (4012553)Termination reason: Instruction limit % 192.81/27.47 % (4012553)Termination phase: Saturation % 192.81/27.47 % (4012553)Time elapsed: 0.098 s % 192.81/27.47 % (4012553)Peak memory usage: 15 MB % 192.81/27.47 % (4012553)Instructions burned: 263 (million) % 192.81/27.47 % (4012578)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=4234476085:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2796 on theBenchmark for (2796ds/1368Mi) % 192.81/27.47 % (4012578)Instruction limit reached! % 192.81/27.47 % (4012578)------------------------------ % 192.81/27.47 % (4012578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.81/27.47 % (4012578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.81/27.47 % (4012578)CaDiCaL version: 2.1.3 % 192.81/27.47 % (4012578)Termination reason: Instruction limit % 192.81/27.47 % (4012578)Termination phase: Saturation % 192.81/27.47 % (4012578)Time elapsed: 0.437 s % 192.81/27.47 % (4012578)Peak memory usage: 23 MB % 192.81/27.47 % (4012578)Instructions burned: 1370 (million) % 192.81/27.47 % (4012580)ott-21_1_sil=16000:si=on:fs=off:random_seed=3174455355:i=360:av=off:fsr=off:rtra=on_2792 on theBenchmark for (2792ds/360Mi) % 192.81/27.47 % (4012580)Instruction limit reached! % 192.81/27.47 % (4012580)------------------------------ % 192.81/27.47 % (4012580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.81/27.47 % (4012580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.81/27.47 % (4012580)CaDiCaL version: 2.1.3 % 192.81/27.47 % (4012580)Termination reason: Instruction limit % 192.81/27.47 % (4012580)Termination phase: Saturation % 192.81/27.47 % (4012580)Time elapsed: 0.091 s % 192.81/27.47 % (4012580)Peak memory usage: 14 MB % 192.81/27.47 % (4012580)Instructions burned: 363 (million) % 192.81/27.47 % (4012582)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=996862862:i=954:bd=all:rtra=on_2791 on theBenchmark for (2791ds/954Mi) % 192.81/27.47 % (4012582)Instruction limit reached! % 192.81/27.47 % (4012582)------------------------------ % 192.81/27.47 % (4012582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.81/27.47 % (4012582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.81/27.47 % (4012582)CaDiCaL version: 2.1.3 % 192.81/27.47 % (4012582)Termination reason: Instruction limit % 192.81/27.47 % (4012582)Termination phase: Saturation % 192.81/27.47 % (4012582)Time elapsed: 0.327 s % 192.81/27.47 % (4012582)Peak memory usage: 16 MB % 192.81/27.47 % (4012582)Instructions burned: 955 (million) % 192.81/27.47 % (4012584)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1416642849:fmbsr=1.3:i=1730:ins=25:rtra=on_2787 on theBenchmark for (2787ds/1730Mi) % 192.81/27.47 % (4012584)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.81/27.47 % (4012584)Terminated due to inappropriate strategy. % 192.81/27.47 % (4012584)------------------------------ % 192.81/27.47 % (4012584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.81/27.47 % (4012584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.81/27.47 % (4012584)CaDiCaL version: 2.1.3 % 192.81/27.47 % (4012584)Termination reason: Inappropriate % 192.81/27.47 % (4012584)Time elapsed: 0.002 s % 246.15/34.94 % (4012584)Peak memory usage: 11 MB % 246.15/34.94 % (4012584)Instructions burned: 5 (million) % 246.15/34.94 % (4012584)------------------------------ % 246.15/34.94 % (4012584)------------------------------ % 246.15/34.94 % (4012586)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3209853936:i=2358:rtra=on_2787 on theBenchmark for (2787ds/2358Mi) % 246.15/34.94 % (4012586)Instruction limit reached! % 246.15/34.94 % (4012586)------------------------------ % 246.15/34.94 % (4012586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.15/34.94 % (4012586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.15/34.94 % (4012586)CaDiCaL version: 2.1.3 % 246.15/34.94 % (4012586)Termination reason: Instruction limit % 246.15/34.94 % (4012586)Termination phase: Saturation % 246.15/34.94 % (4012586)Time elapsed: 0.779 s % 246.15/34.94 % (4012586)Peak memory usage: 27 MB % 246.15/34.94 % (4012586)Instructions burned: 2361 (million) % 246.15/34.94 % (4012588)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3724048074:i=1778:ins=1:rtra=on_2779 on theBenchmark for (2779ds/1778Mi) % 246.15/34.94 % (4012588)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 246.15/34.94 % (4012588)Terminated due to inappropriate strategy. % 246.15/34.94 % (4012588)------------------------------ % 246.15/34.94 % (4012588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.15/34.94 % (4012588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.15/34.94 % (4012588)CaDiCaL version: 2.1.3 % 246.15/34.94 % (4012588)Termination reason: Inappropriate % 246.15/34.94 % (4012588)Time elapsed: 0.002 s % 246.15/34.94 % (4012588)Peak memory usage: 11 MB % 246.15/34.94 % (4012588)Instructions burned: 5 (million) % 246.15/34.94 % (4012588)------------------------------ % 246.15/34.94 % (4012588)------------------------------ % 246.15/34.94 % (4012590)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=946718385:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2779 on theBenchmark for (2779ds/1384Mi) % 246.15/34.94 % (4012590)Instruction limit reached! % 246.15/34.94 % (4012590)------------------------------ % 246.15/34.94 % (4012590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.15/34.94 % (4012590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.15/34.94 % (4012590)CaDiCaL version: 2.1.3 % 246.15/34.94 % (4012590)Termination reason: Instruction limit % 246.15/34.94 % (4012590)Termination phase: Saturation % 246.15/34.94 % (4012590)Time elapsed: 0.498 s % 246.15/34.94 % (4012590)Peak memory usage: 26 MB % 246.15/34.94 % (4012590)Instructions burned: 1386 (million) % 246.15/34.94 % (4012592)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=159926889:i=1758:kws=inv_precedence:fsr=off:rtra=on_2774 on theBenchmark for (2774ds/1758Mi) % 246.15/34.94 % (4012592)Instruction limit reached! % 246.15/34.94 % (4012592)------------------------------ % 246.15/34.94 % (4012592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.15/34.94 % (4012592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.15/34.94 % (4012592)CaDiCaL version: 2.1.3 % 246.15/34.94 % (4012592)Termination reason: Instruction limit % 246.15/34.94 % (4012592)Termination phase: Saturation % 246.15/34.94 % (4012592)Time elapsed: 0.516 s % 246.15/34.94 % (4012592)Peak memory usage: 24 MB % 246.15/34.94 % (4012592)Instructions burned: 1760 (million) % 246.15/34.94 % (4012594)fmb+10_1_sil=64000:si=on:random_seed=3510367358:i=44122:nm=2:rtra=on:gsp=on_2769 on theBenchmark for (2769ds/44122Mi) % 246.15/34.94 % (4012594)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 246.15/34.94 % (4012594)Terminated due to inappropriate strategy. % 246.15/34.94 % (4012594)------------------------------ % 246.15/34.94 % (4012594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.15/34.94 % (4012594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.15/34.94 % (4012594)CaDiCaL version: 2.1.3 % 246.15/34.94 % (4012594)Termination reason: Inappropriate % 246.15/34.94 % (4012594)Time elapsed: 0.003 s % 246.15/34.94 % (4012594)Peak memory usage: 11 MB % 246.15/34.94 % (4012594)Instructions burned: 5 (million) % 246.15/34.94 % (4012594)------------------------------ % 246.15/34.94 % (4012594)------------------------------ % 246.15/34.94 % (4012596)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3517016759:i=19030:nm=5:rtra=on_2769 on theBenchmark Terminated % 300.27/42.54 Terminated %------------------------------------------------------------------------------