%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW662_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n010.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:36 PM UTC 2026 % Result : Timeout 300.14s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW662_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n010.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:24:32 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.66/0.86 % (1956406)Will run a generic schedule for satisfiability detection. % 3.66/0.86 % (1956430)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4018245901:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.66/0.86 % (1956427)% WARNING: option uhcvi not known. % 3.66/0.86 % (1956427)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2046557218:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.66/0.86 % (1956428)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2243307562:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.66/0.86 % (1956426)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1181185562_2999 on theBenchmark for (2999ds/0Mi) % 3.66/0.86 % (1956429)dis+10_1_sil=32000:sp=arity:random_seed=4169497113:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.66/0.86 % (1956432)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2556841017:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.66/0.86 % (1956433)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2012746255:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.66/0.86 % (1956426)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.66/0.86 % (1956426)Terminated due to inappropriate strategy. % 3.66/0.86 % (1956426)------------------------------ % 3.66/0.86 % (1956426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.66/0.86 % (1956426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.66/0.86 % (1956426)CaDiCaL version: 2.1.3 % 3.66/0.86 % (1956426)Termination reason: Inappropriate % 3.66/0.86 % (1956426)Time elapsed: 0.003 s % 3.66/0.86 % (1956426)Peak memory usage: 11 MB % 3.66/0.86 % (1956426)Instructions burned: 4 (million) % 3.66/0.86 % (1956426)------------------------------ % 3.66/0.86 % (1956426)------------------------------ % 3.66/0.86 % (1956447)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1201609120:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.66/0.86 % (1956447)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.66/0.86 % (1956447)Terminated due to inappropriate strategy. % 3.66/0.86 % (1956447)------------------------------ % 3.66/0.86 % (1956447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.66/0.86 % (1956447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.66/0.86 % (1956447)CaDiCaL version: 2.1.3 % 3.66/0.86 % (1956447)Termination reason: Inappropriate % 3.66/0.86 % (1956447)Time elapsed: 0.002 s % 3.66/0.86 % (1956447)Peak memory usage: 10 MB % 3.66/0.86 % (1956447)Instructions burned: 4 (million) % 3.66/0.86 % (1956447)------------------------------ % 3.66/0.86 % (1956447)------------------------------ % 3.66/0.86 % (1956430)Instruction limit reached! % 3.66/0.86 % (1956430)------------------------------ % 3.66/0.86 % (1956430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.66/0.86 % (1956430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.66/0.86 % (1956430)CaDiCaL version: 2.1.3 % 3.66/0.86 % (1956430)Termination reason: Instruction limit % 3.66/0.86 % (1956430)Termination phase: Saturation % 3.66/0.86 % (1956430)Time elapsed: 0.043 s % 3.66/0.86 % (1956430)Peak memory usage: 13 MB % 3.66/0.86 % (1956430)Instructions burned: 118 (million) % 3.66/0.86 % (1956462)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=2201357859:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.66/0.86 % (1956457)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4041654930:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.66/0.86 % (1956429)Instruction limit reached! % 3.66/0.86 % (1956429)------------------------------ % 3.66/0.86 % (1956429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.66/0.86 % (1956429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.66/0.86 % (1956429)CaDiCaL version: 2.1.3 % 3.66/0.86 % (1956429)Termination reason: Instruction limit % 3.66/0.86 % (1956429)Termination phase: Saturation % 3.66/0.86 % (1956429)Time elapsed: 0.067 s % 3.66/0.86 % (1956429)Peak memory usage: 13 MB % 3.66/0.86 % (1956429)Instructions burned: 104 (million) % 3.66/0.86 % (1956432)Instruction limit reached! % 3.66/0.86 % (1956432)------------------------------ % 3.66/0.86 % (1956432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.32/1.17 % (1956432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.17 % (1956432)CaDiCaL version: 2.1.3 % 6.32/1.17 % (1956432)Termination reason: Instruction limit % 6.32/1.17 % (1956432)Termination phase: Saturation % 6.32/1.17 % (1956432)Time elapsed: 0.083 s % 6.32/1.17 % (1956432)Peak memory usage: 13 MB % 6.32/1.17 % (1956432)Instructions burned: 131 (million) % 6.32/1.17 % (1956474)ott-21_1_sil=16000:fs=off:random_seed=979373628:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.32/1.17 % (1956480)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=500769224:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.32/1.17 % (1956433)Instruction limit reached! % 6.32/1.17 % (1956433)------------------------------ % 6.32/1.17 % (1956433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.32/1.17 % (1956433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.17 % (1956433)CaDiCaL version: 2.1.3 % 6.32/1.17 % (1956433)Termination reason: Instruction limit % 6.32/1.17 % (1956433)Termination phase: Saturation % 6.32/1.17 % (1956433)Time elapsed: 0.109 s % 6.32/1.17 % (1956433)Peak memory usage: 13 MB % 6.32/1.17 % (1956433)Instructions burned: 159 (million) % 6.32/1.17 % (1956494)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=750520817:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.32/1.17 % (1956494)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.32/1.17 % (1956494)Terminated due to inappropriate strategy. % 6.32/1.17 % (1956494)------------------------------ % 6.32/1.17 % (1956494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.32/1.17 % (1956494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.17 % (1956494)CaDiCaL version: 2.1.3 % 6.32/1.17 % (1956494)Termination reason: Inappropriate % 6.32/1.17 % (1956494)Time elapsed: 0.002 s % 6.32/1.17 % (1956494)Peak memory usage: 10 MB % 6.32/1.17 % (1956494)Instructions burned: 4 (million) % 6.32/1.17 % (1956457)Instruction limit reached! % 6.32/1.17 % (1956457)------------------------------ % 6.32/1.17 % (1956457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.32/1.17 % (1956457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.17 % (1956457)CaDiCaL version: 2.1.3 % 6.32/1.17 % (1956457)Termination reason: Instruction limit % 6.32/1.17 % (1956457)Termination phase: Saturation % 6.32/1.17 % (1956457)Time elapsed: 0.086 s % 6.32/1.17 % (1956457)Peak memory usage: 13 MB % 6.32/1.17 % (1956457)Instructions burned: 131 (million) % 6.32/1.17 % (1956494)------------------------------ % 6.32/1.17 % (1956494)------------------------------ % 6.32/1.17 % (1956501)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=423656374:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.32/1.17 % (1956500)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3941273603:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.32/1.17 % (1956501)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.32/1.17 % (1956501)Terminated due to inappropriate strategy. % 6.32/1.17 % (1956501)------------------------------ % 6.32/1.17 % (1956501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.32/1.17 % (1956501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.17 % (1956501)CaDiCaL version: 2.1.3 % 6.32/1.17 % (1956501)Termination reason: Inappropriate % 6.32/1.17 % (1956501)Time elapsed: 0.002 s % 6.32/1.17 % (1956501)Peak memory usage: 10 MB % 6.32/1.17 % (1956501)Instructions burned: 4 (million) % 6.32/1.17 % (1956501)------------------------------ % 6.32/1.17 % (1956501)------------------------------ % 6.32/1.17 % (1956519)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=1751844320:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 6.32/1.17 % (1956474)Instruction limit reached! % 6.32/1.17 % (1956474)------------------------------ % 6.32/1.17 % (1956474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.32/1.17 % (1956474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.17 % (1956474)CaDiCaL version: 2.1.3 % 6.32/1.17 % (1956474)Termination reason: Instruction limit % 6.32/1.17 % (1956474)Termination phase: Saturation % 20.52/3.14 % (1956474)Time elapsed: 0.094 s % 20.52/3.14 % (1956474)Peak memory usage: 13 MB % 20.52/3.14 % (1956474)Instructions burned: 180 (million) % 20.52/3.14 % (1956538)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1199478664:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.52/3.14 % (1956462)Instruction limit reached! % 20.52/3.14 % (1956462)------------------------------ % 20.52/3.14 % (1956462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.52/3.14 % (1956462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.52/3.14 % (1956462)CaDiCaL version: 2.1.3 % 20.52/3.14 % (1956462)Termination reason: Instruction limit % 20.52/3.14 % (1956462)Termination phase: Saturation % 20.52/3.14 % (1956462)Time elapsed: 0.234 s % 20.52/3.14 % (1956462)Peak memory usage: 18 MB % 20.52/3.14 % (1956462)Instructions burned: 686 (million) % 20.52/3.14 % (1956546)fmb+10_1_sil=64000:random_seed=728579162:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 20.52/3.14 % (1956546)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.52/3.14 % (1956546)Terminated due to inappropriate strategy. % 20.52/3.14 % (1956546)------------------------------ % 20.52/3.14 % (1956546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.52/3.14 % (1956546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.52/3.14 % (1956546)CaDiCaL version: 2.1.3 % 20.52/3.14 % (1956546)Termination reason: Inappropriate % 20.52/3.14 % (1956546)Time elapsed: 0.001 s % 20.52/3.14 % (1956546)Peak memory usage: 10 MB % 20.52/3.14 % (1956546)Instructions burned: 4 (million) % 20.52/3.14 % (1956546)------------------------------ % 20.52/3.14 % (1956546)------------------------------ % 20.52/3.14 % (1956548)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3524752108:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 20.52/3.14 % (1956548)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.52/3.14 % (1956548)Terminated due to inappropriate strategy. % 20.52/3.14 % (1956548)------------------------------ % 20.52/3.14 % (1956548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.52/3.14 % (1956548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.52/3.14 % (1956548)CaDiCaL version: 2.1.3 % 20.52/3.14 % (1956548)Termination reason: Inappropriate % 20.52/3.14 % (1956548)Time elapsed: 0.001 s % 20.52/3.14 % (1956548)Peak memory usage: 10 MB % 20.52/3.14 % (1956548)Instructions burned: 4 (million) % 20.52/3.14 % (1956548)------------------------------ % 20.52/3.14 % (1956548)------------------------------ % 20.52/3.14 % (1956550)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2778923709:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 20.52/3.14 % (1956550)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.52/3.14 % (1956550)Terminated due to inappropriate strategy. % 20.52/3.14 % (1956550)------------------------------ % 20.52/3.14 % (1956550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.52/3.14 % (1956550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.52/3.14 % (1956550)CaDiCaL version: 2.1.3 % 20.52/3.14 % (1956550)Termination reason: Inappropriate % 20.52/3.14 % (1956550)Time elapsed: 0.001 s % 20.52/3.14 % (1956550)Peak memory usage: 10 MB % 20.52/3.14 % (1956550)Instructions burned: 4 (million) % 20.52/3.14 % (1956550)------------------------------ % 20.52/3.14 % (1956550)------------------------------ % 20.52/3.14 % (1956552)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1987189445:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 20.52/3.14 % (1956480)Instruction limit reached! % 20.52/3.14 % (1956480)------------------------------ % 20.52/3.14 % (1956480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.52/3.14 % (1956480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.52/3.14 % (1956480)CaDiCaL version: 2.1.3 % 20.52/3.14 % (1956480)Termination reason: Instruction limit % 20.52/3.14 % (1956480)Termination phase: Saturation % 20.52/3.14 % (1956480)Time elapsed: 0.292 s % 20.52/3.14 % (1956480)Peak memory usage: 13 MB % 20.52/3.14 % (1956480)Instructions burned: 478 (million) % 20.52/3.14 % (1956554)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=454819601:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 20.52/3.14 % (1956519)Instruction limit reached! % 20.52/3.14 % (1956519)------------------------------ % 26.89/4.05 % (1956519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.89/4.05 % (1956519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.89/4.05 % (1956519)CaDiCaL version: 2.1.3 % 26.89/4.05 % (1956519)Termination reason: Instruction limit % 26.89/4.05 % (1956519)Termination phase: Saturation % 26.89/4.05 % (1956519)Time elapsed: 0.411 s % 26.89/4.05 % (1956519)Peak memory usage: 18 MB % 26.89/4.05 % (1956519)Instructions burned: 692 (million) % 26.89/4.05 % (1956556)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3783514285:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 26.89/4.05 % (1956556)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.89/4.05 % (1956556)Terminated due to inappropriate strategy. % 26.89/4.05 % (1956556)------------------------------ % 26.89/4.05 % (1956556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.89/4.05 % (1956556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.89/4.05 % (1956556)CaDiCaL version: 2.1.3 % 26.89/4.05 % (1956556)Termination reason: Inappropriate % 26.89/4.05 % (1956556)Time elapsed: 0.003 s % 26.89/4.05 % (1956556)Peak memory usage: 11 MB % 26.89/4.05 % (1956556)Instructions burned: 4 (million) % 26.89/4.05 % (1956556)------------------------------ % 26.89/4.05 % (1956556)------------------------------ % 26.89/4.05 % (1956558)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3580927232:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 26.89/4.05 % (1956558)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.89/4.05 % (1956558)Terminated due to inappropriate strategy. % 26.89/4.05 % (1956558)------------------------------ % 26.89/4.05 % (1956558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.89/4.05 % (1956558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.89/4.05 % (1956558)CaDiCaL version: 2.1.3 % 26.89/4.05 % (1956558)Termination reason: Inappropriate % 26.89/4.05 % (1956558)Time elapsed: 0.003 s % 26.89/4.05 % (1956558)Peak memory usage: 10 MB % 26.89/4.05 % (1956558)Instructions burned: 4 (million) % 26.89/4.05 % (1956558)------------------------------ % 26.89/4.05 % (1956558)------------------------------ % 26.89/4.05 % (1956560)ott-2_1_sil=16000:newcnf=on:random_seed=3557887048:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 26.89/4.05 % (1956538)Instruction limit reached! % 26.89/4.05 % (1956538)------------------------------ % 26.89/4.05 % (1956538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.89/4.05 % (1956538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.89/4.05 % (1956538)CaDiCaL version: 2.1.3 % 26.89/4.05 % (1956538)Termination reason: Instruction limit % 26.89/4.05 % (1956538)Termination phase: Saturation % 26.89/4.05 % (1956538)Time elapsed: 0.520 s % 26.89/4.05 % (1956538)Peak memory usage: 19 MB % 26.89/4.05 % (1956538)Instructions burned: 880 (million) % 26.89/4.05 % (1956562)ott+10_1_sil=32000:tgt=ground:random_seed=1850289086:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 26.89/4.05 % (1956500)Instruction limit reached! % 26.89/4.05 % (1956500)------------------------------ % 26.89/4.05 % (1956500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.89/4.05 % (1956500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.89/4.05 % (1956500)CaDiCaL version: 2.1.3 % 26.89/4.05 % (1956500)Termination reason: Instruction limit % 26.89/4.05 % (1956500)Termination phase: Saturation % 26.89/4.05 % (1956500)Time elapsed: 0.716 s % 26.89/4.05 % (1956500)Peak memory usage: 22 MB % 26.89/4.05 % (1956500)Instructions burned: 1180 (million) % 26.89/4.05 % (1956564)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=767913100:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 26.89/4.05 % (1956564)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.89/4.05 % (1956564)Terminated due to inappropriate strategy. % 26.89/4.05 % (1956564)------------------------------ % 26.89/4.05 % (1956564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.89/4.05 % (1956564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.89/4.05 % (1956564)CaDiCaL version: 2.1.3 % 26.89/4.05 % (1956564)Termination reason: Inappropriate % 26.89/4.05 % (1956564)Time elapsed: 0.003 s % 26.89/4.05 % (1956564)Peak memory usage: 11 MB % 26.89/4.05 % (1956564)Instructions burned: 4 (million) % 112.80/16.18 % (1956564)------------------------------ % 112.80/16.18 % (1956564)------------------------------ % 112.80/16.18 % (1956566)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3271127680:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 112.80/16.18 % (1956560)Instruction limit reached! % 112.80/16.18 % (1956560)------------------------------ % 112.80/16.18 % (1956560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.80/16.18 % (1956560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.80/16.18 % (1956560)CaDiCaL version: 2.1.3 % 112.80/16.18 % (1956560)Termination reason: Instruction limit % 112.80/16.18 % (1956560)Termination phase: Saturation % 112.80/16.18 % (1956560)Time elapsed: 0.519 s % 112.80/16.18 % (1956560)Peak memory usage: 16 MB % 112.80/16.18 % (1956560)Instructions burned: 869 (million) % 112.80/16.18 % (1956568)dis+21_1_sil=32000:sas=cadical:random_seed=3756410977:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 112.80/16.18 % (1956554)Instruction limit reached! % 112.80/16.18 % (1956554)------------------------------ % 112.80/16.18 % (1956554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.80/16.18 % (1956554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.80/16.18 % (1956554)CaDiCaL version: 2.1.3 % 112.80/16.18 % (1956554)Termination reason: Instruction limit % 112.80/16.18 % (1956554)Termination phase: Saturation % 112.80/16.18 % (1956554)Time elapsed: 0.828 s % 112.80/16.18 % (1956554)Peak memory usage: 28 MB % 112.80/16.18 % (1956554)Instructions burned: 1472 (million) % 112.80/16.18 % (1956570)ott+11_1_sil=16000:gs=on:random_seed=2337703967:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 112.80/16.18 % (1956552)Instruction limit reached! % 112.80/16.18 % (1956552)------------------------------ % 112.80/16.18 % (1956552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.80/16.18 % (1956552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.80/16.18 % (1956552)CaDiCaL version: 2.1.3 % 112.80/16.18 % (1956552)Termination reason: Instruction limit % 112.80/16.18 % (1956552)Termination phase: Saturation % 112.80/16.18 % (1956552)Time elapsed: 1.456 s % 112.80/16.18 % (1956552)Peak memory usage: 35 MB % 112.80/16.18 % (1956552)Instructions burned: 5135 (million) % 112.80/16.18 % (1956572)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3136442948:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 112.80/16.18 % (1956572)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 112.80/16.18 % (1956572)Terminated due to inappropriate strategy. % 112.80/16.18 % (1956572)------------------------------ % 112.80/16.18 % (1956572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.80/16.18 % (1956572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.80/16.18 % (1956572)CaDiCaL version: 2.1.3 % 112.80/16.18 % (1956572)Termination reason: Inappropriate % 112.80/16.18 % (1956572)Time elapsed: 0.001 s % 112.80/16.18 % (1956572)Peak memory usage: 11 MB % 112.80/16.18 % (1956572)Instructions burned: 4 (million) % 112.80/16.18 % (1956572)------------------------------ % 112.80/16.18 % (1956572)------------------------------ % 112.80/16.18 % (1956574)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2427496871:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 112.80/16.18 % (1956570)Instruction limit reached! % 112.80/16.18 % (1956570)------------------------------ % 112.80/16.18 % (1956570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.80/16.18 % (1956570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.80/16.18 % (1956570)CaDiCaL version: 2.1.3 % 112.80/16.18 % (1956570)Termination reason: Instruction limit % 112.80/16.18 % (1956570)Termination phase: Saturation % 112.80/16.18 % (1956570)Time elapsed: 1.081 s % 112.80/16.18 % (1956570)Peak memory usage: 16 MB % 112.80/16.18 % (1956570)Instructions burned: 2253 (million) % 112.80/16.18 % (1956576)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1414576488:i=29340_2976 on theBenchmark for (2976ds/29340Mi) % 112.80/16.18 % (1956566)Instruction limit reached! % 112.80/16.18 % (1956566)------------------------------ % 112.80/16.18 % (1956566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.80/16.18 % (1956566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.80/16.18 % (1956566)CaDiCaL version: 2.1.3 % 112.80/16.18 % (1956566)Termination reason: Instruction limit % 127.46/18.20 % (1956566)Termination phase: Saturation % 127.46/18.20 % (1956566)Time elapsed: 1.952 s % 127.46/18.20 % (1956566)Peak memory usage: 32 MB % 127.46/18.20 % (1956566)Instructions burned: 3514 (million) % 127.46/18.20 % (1956578)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=352837857:i=5211_2970 on theBenchmark for (2970ds/5211Mi) % 127.46/18.20 % (1956574)Instruction limit reached! % 127.46/18.20 % (1956574)------------------------------ % 127.46/18.20 % (1956574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.46/18.20 % (1956574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.46/18.20 % (1956574)CaDiCaL version: 2.1.3 % 127.46/18.20 % (1956574)Termination reason: Instruction limit % 127.46/18.20 % (1956574)Termination phase: Saturation % 127.46/18.20 % (1956574)Time elapsed: 1.422 s % 127.46/18.20 % (1956574)Peak memory usage: 63 MB % 127.46/18.20 % (1956574)Instructions burned: 4593 (million) % 127.46/18.20 % (1956580)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2734182726:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 127.46/18.20 % (1956580)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.46/18.20 % (1956580)Terminated due to inappropriate strategy. % 127.46/18.20 % (1956580)------------------------------ % 127.46/18.20 % (1956580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.46/18.20 % (1956580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.46/18.20 % (1956580)CaDiCaL version: 2.1.3 % 127.46/18.20 % (1956580)Termination reason: Inappropriate % 127.46/18.20 % (1956580)Time elapsed: 0.001 s % 127.46/18.20 % (1956580)Peak memory usage: 11 MB % 127.46/18.20 % (1956580)Instructions burned: 4 (million) % 127.46/18.20 % (1956580)------------------------------ % 127.46/18.20 % (1956580)------------------------------ % 127.46/18.20 % (1956582)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3717412764:fmbsr=2:i=46332_2966 on theBenchmark for (2966ds/46332Mi) % 127.46/18.20 % (1956582)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.46/18.20 % (1956582)Terminated due to inappropriate strategy. % 127.46/18.20 % (1956582)------------------------------ % 127.46/18.20 % (1956582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.46/18.20 % (1956582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.46/18.20 % (1956582)CaDiCaL version: 2.1.3 % 127.46/18.20 % (1956582)Termination reason: Inappropriate % 127.46/18.20 % (1956582)Time elapsed: 0.001 s % 127.46/18.20 % (1956582)Peak memory usage: 11 MB % 127.46/18.20 % (1956582)Instructions burned: 4 (million) % 127.46/18.20 % (1956582)------------------------------ % 127.46/18.20 % (1956582)------------------------------ % 127.46/18.20 % (1956584)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1350190275:i=14071_2966 on theBenchmark for (2966ds/14071Mi) % 127.46/18.20 % (1956584)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.46/18.20 % (1956584)Terminated due to inappropriate strategy. % 127.46/18.20 % (1956584)------------------------------ % 127.46/18.20 % (1956584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.46/18.20 % (1956584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.46/18.20 % (1956584)CaDiCaL version: 2.1.3 % 127.46/18.20 % (1956584)Termination reason: Inappropriate % 127.46/18.20 % (1956584)Time elapsed: 0.001 s % 127.46/18.20 % (1956584)Peak memory usage: 11 MB % 127.46/18.20 % (1956584)Instructions burned: 4 (million) % 127.46/18.20 % (1956584)------------------------------ % 127.46/18.20 % (1956584)------------------------------ % 127.46/18.20 % (1956586)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=816993493:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi) % 127.46/18.20 % (1956568)Instruction limit reached! % 127.46/18.20 % (1956568)------------------------------ % 127.46/18.20 % (1956568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.46/18.20 % (1956568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.46/18.20 % (1956568)CaDiCaL version: 2.1.3 % 127.46/18.20 % (1956568)Termination reason: Instruction limit % 127.46/18.20 % (1956568)Termination phase: Saturation % 127.46/18.20 % (1956568)Time elapsed: 2.104 s % 127.46/18.20 % (1956568)Peak memory usage: 31 MB % 127.46/18.20 % (1956568)Instructions burned: 3773 (million) % 127.46/18.20 % (1956588)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1384139212:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 127.46/18.20 % (1956562)Instruction limit reached! % 128.17/18.32 % (1956562)------------------------------ % 128.17/18.32 % (1956562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.17/18.32 % (1956562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.17/18.32 % (1956562)CaDiCaL version: 2.1.3 % 128.17/18.32 % (1956562)Termination reason: Instruction limit % 128.17/18.32 % (1956562)Termination phase: Saturation % 128.17/18.32 % (1956562)Time elapsed: 3.028 s % 128.17/18.32 % (1956562)Peak memory usage: 37 MB % 128.17/18.32 % (1956562)Instructions burned: 5114 (million) % 128.17/18.32 % (1956590)dis+10_16:1_sil=16000:random_seed=1185249002:i=9155:fsr=off_2961 on theBenchmark for (2961ds/9155Mi) % 128.17/18.32 % (1956578)Instruction limit reached! % 128.17/18.32 % (1956578)------------------------------ % 128.17/18.32 % (1956578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.17/18.32 % (1956578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.17/18.32 % (1956578)CaDiCaL version: 2.1.3 % 128.17/18.32 % (1956578)Termination reason: Instruction limit % 128.17/18.32 % (1956578)Termination phase: Saturation % 128.17/18.32 % (1956578)Time elapsed: 2.797 s % 128.17/18.32 % (1956578)Peak memory usage: 54 MB % 128.17/18.32 % (1956578)Instructions burned: 5212 (million) % 128.17/18.32 % (1956592)ott-3_8_sil=64000:random_seed=603726934:i=20139:bs=on_2942 on theBenchmark for (2942ds/20139Mi) % 128.17/18.32 % (1956588)Instruction limit reached! % 128.17/18.32 % (1956588)------------------------------ % 128.17/18.32 % (1956588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.17/18.32 % (1956588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.17/18.32 % (1956588)CaDiCaL version: 2.1.3 % 128.17/18.32 % (1956588)Termination reason: Instruction limit % 128.17/18.32 % (1956588)Termination phase: Saturation % 128.17/18.32 % (1956588)Time elapsed: 5.037 s % 128.17/18.32 % (1956588)Peak memory usage: 63 MB % 128.17/18.32 % (1956588)Instructions burned: 8174 (million) % 128.17/18.32 % (1956594)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=266646456:fmbsr=2:i=32576_2915 on theBenchmark for (2915ds/32576Mi) % 128.17/18.32 % (1956594)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 128.17/18.32 % (1956594)Terminated due to inappropriate strategy. % 128.17/18.32 % (1956594)------------------------------ % 128.17/18.32 % (1956594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.17/18.32 % (1956594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.17/18.32 % (1956594)CaDiCaL version: 2.1.3 % 128.17/18.32 % (1956594)Termination reason: Inappropriate % 128.17/18.32 % (1956594)Time elapsed: 0.003 s % 128.17/18.32 % (1956594)Peak memory usage: 11 MB % 128.17/18.32 % (1956594)Instructions burned: 4 (million) % 128.17/18.32 % (1956594)------------------------------ % 128.17/18.32 % (1956594)------------------------------ % 128.17/18.32 % (1956596)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=22566664:i=11404_2915 on theBenchmark for (2915ds/11404Mi) % 128.17/18.32 % (1956590)Instruction limit reached! % 128.17/18.32 % (1956590)------------------------------ % 128.17/18.32 % (1956590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.17/18.32 % (1956590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.17/18.32 % (1956590)CaDiCaL version: 2.1.3 % 128.17/18.32 % (1956590)Termination reason: Instruction limit % 128.17/18.32 % (1956590)Termination phase: Saturation % 128.17/18.32 % (1956590)Time elapsed: 4.965 s % 128.17/18.32 % (1956590)Peak memory usage: 54 MB % 128.17/18.32 % (1956590)Instructions burned: 9156 (million) % 128.17/18.32 % (1956598)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3292225844:i=14134_2911 on theBenchmark for (2911ds/14134Mi) % 128.17/18.32 % (1956586)Instruction limit reached! % 128.17/18.32 % (1956586)------------------------------ % 128.17/18.32 % (1956586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.17/18.32 % (1956586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.17/18.32 % (1956586)CaDiCaL version: 2.1.3 % 128.17/18.32 % (1956586)Termination reason: Instruction limit % 128.17/18.32 % (1956586)Termination phase: Saturation % 128.17/18.32 % (1956586)Time elapsed: 8.192 s % 128.17/18.32 % (1956586)Peak memory usage: 113 MB % 128.17/18.32 % (1956586)Instructions burned: 22566 (million) % 128.17/18.32 % (1956600)dis+33_16_sil=32000:sac=on:random_seed=1888305252:i=15851:nm=0_2884 on theBenchmark for (2884ds/15851Mi) % 128.17/18.32 % (1956596)Instruction limit reached! % 128.17/18.32 % (1956596)------------------------------ % 128.17/18.32 % (1956596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.02/28.15 % (1956596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.02/28.15 % (1956596)CaDiCaL version: 2.1.3 % 198.02/28.15 % (1956596)Termination reason: Instruction limit % 198.02/28.15 % (1956596)Termination phase: Saturation % 198.02/28.15 % (1956596)Time elapsed: 7.491 s % 198.02/28.15 % (1956596)Peak memory usage: 81 MB % 198.02/28.15 % (1956596)Instructions burned: 11404 (million) % 198.02/28.15 % (1956961)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3944302370:avsq=on:i=17627:add=on:amm=off_2840 on theBenchmark for (2840ds/17627Mi) % 198.02/28.15 % (1956600)Instruction limit reached! % 198.02/28.15 % (1956600)------------------------------ % 198.02/28.15 % (1956600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.02/28.15 % (1956600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.02/28.15 % (1956600)CaDiCaL version: 2.1.3 % 198.02/28.15 % (1956600)Termination reason: Instruction limit % 198.02/28.15 % (1956600)Termination phase: Saturation % 198.02/28.15 % (1956600)Time elapsed: 4.540 s % 198.02/28.15 % (1956600)Peak memory usage: 117 MB % 198.02/28.15 % (1956600)Instructions burned: 15853 (million) % 198.02/28.15 % (1956963)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1598837946:s2a=on:i=53295_2838 on theBenchmark for (2838ds/53295Mi) % 198.02/28.15 % (1956576)Instruction limit reached! % 198.02/28.15 % (1956576)------------------------------ % 198.02/28.15 % (1956576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.02/28.15 % (1956576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.02/28.15 % (1956576)CaDiCaL version: 2.1.3 % 198.02/28.15 % (1956576)Termination reason: Instruction limit % 198.02/28.15 % (1956576)Termination phase: Saturation % 198.02/28.15 % (1956576)Time elapsed: 13.784 s % 198.02/28.15 % (1956576)Peak memory usage: 302 MB % 198.02/28.15 % (1956576)Instructions burned: 29340 (million) % 198.02/28.15 % (1956965)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1086625282:i=26857:ins=20_2837 on theBenchmark for (2837ds/26857Mi) % 198.02/28.15 % (1956965)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 198.02/28.15 % (1956965)Terminated due to inappropriate strategy. % 198.02/28.15 % (1956965)------------------------------ % 198.02/28.15 % (1956965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.02/28.15 % (1956965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.02/28.15 % (1956965)CaDiCaL version: 2.1.3 % 198.02/28.15 % (1956965)Termination reason: Inappropriate % 198.02/28.15 % (1956965)Time elapsed: 0.003 s % 198.02/28.15 % (1956965)Peak memory usage: 11 MB % 198.02/28.15 % (1956965)Instructions burned: 4 (million) % 198.02/28.15 % (1956965)------------------------------ % 198.02/28.15 % (1956965)------------------------------ % 198.02/28.15 % (1956967)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3273285599:i=28120:bs=on:fsr=off_2837 on theBenchmark for (2837ds/28120Mi) % 198.02/28.15 % (1956598)Instruction limit reached! % 198.02/28.15 % (1956598)------------------------------ % 198.02/28.15 % (1956598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.02/28.15 % (1956598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.02/28.15 % (1956598)CaDiCaL version: 2.1.3 % 198.02/28.15 % (1956598)Termination reason: Instruction limit % 198.02/28.15 % (1956598)Termination phase: Saturation % 198.02/28.15 % (1956598)Time elapsed: 9.082 s % 198.02/28.15 % (1956598)Peak memory usage: 85 MB % 198.02/28.15 % (1956598)Instructions burned: 14134 (million) % 198.02/28.15 % (1956969)fmb+10_1_sil=256000:fmbss=7:random_seed=2944285479:fmbsr=1.6:i=182295_2820 on theBenchmark for (2820ds/182295Mi) % 198.02/28.15 % (1956969)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 198.02/28.15 % (1956969)Terminated due to inappropriate strategy. % 198.02/28.15 % (1956969)------------------------------ % 198.02/28.15 % (1956969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.02/28.15 % (1956969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.02/28.15 % (1956969)CaDiCaL version: 2.1.3 % 198.02/28.15 % (1956969)Termination reason: Inappropriate % 198.02/28.15 % (1956969)Time elapsed: 0.003 s % 198.02/28.15 % (1956969)Peak memory usage: 10 MB % 198.02/28.15 % (1956969)Instructions burned: 4 (million) % 198.02/28.15 % (1956969)------------------------------ % 198.02/28.15 % (1956969)------------------------------ % 198.02/28.15 % (1956971)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2528549913:i=44625:gsp=on_2820 on theBenchmark for (2820ds/44625Mi) % 204.37/29.05 % (1956971)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 204.37/29.05 % (1956971)Terminated due to inappropriate strategy. % 204.37/29.05 % (1956971)------------------------------ % 204.37/29.05 % (1956971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.37/29.05 % (1956971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.37/29.05 % (1956971)CaDiCaL version: 2.1.3 % 204.37/29.05 % (1956971)Termination reason: Inappropriate % 204.37/29.05 % (1956971)Time elapsed: 0.003 s % 204.37/29.05 % (1956971)Peak memory usage: 11 MB % 204.37/29.05 % (1956971)Instructions burned: 4 (million) % 204.37/29.05 % (1956971)------------------------------ % 204.37/29.05 % (1956971)------------------------------ % 204.37/29.05 % (1956973)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2954645608:i=160505_2820 on theBenchmark for (2820ds/160505Mi) % 204.37/29.05 % (1956973)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 204.37/29.05 % (1956973)Terminated due to inappropriate strategy. % 204.37/29.05 % (1956973)------------------------------ % 204.37/29.05 % (1956973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.37/29.05 % (1956973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.37/29.05 % (1956973)CaDiCaL version: 2.1.3 % 204.37/29.05 % (1956973)Termination reason: Inappropriate % 204.37/29.05 % (1956973)Time elapsed: 0.003 s % 204.37/29.05 % (1956973)Peak memory usage: 10 MB % 204.37/29.05 % (1956973)Instructions burned: 4 (million) % 204.37/29.05 % (1956973)------------------------------ % 204.37/29.05 % (1956973)------------------------------ % 204.37/29.05 % (1956975)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1293192373:fmbsr=1.3:i=225729_2820 on theBenchmark for (2820ds/225729Mi) % 204.37/29.05 % (1956975)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 204.37/29.05 % (1956975)Terminated due to inappropriate strategy. % 204.37/29.05 % (1956975)------------------------------ % 204.37/29.05 % (1956975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.37/29.05 % (1956975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.37/29.05 % (1956975)CaDiCaL version: 2.1.3 % 204.37/29.05 % (1956975)Termination reason: Inappropriate % 204.37/29.05 % (1956975)Time elapsed: 0.003 s % 204.37/29.05 % (1956975)Peak memory usage: 11 MB % 204.37/29.05 % (1956975)Instructions burned: 4 (million) % 204.37/29.05 % (1956975)------------------------------ % 204.37/29.05 % (1956975)------------------------------ % 204.37/29.05 % (1956977)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1926224685:fmbsr=2:i=185024:ins=7_2819 on theBenchmark for (2819ds/185024Mi) % 204.37/29.05 % (1956977)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 204.37/29.05 % (1956977)Terminated due to inappropriate strategy. % 204.37/29.05 % (1956977)------------------------------ % 204.37/29.05 % (1956977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.37/29.05 % (1956977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.37/29.05 % (1956977)CaDiCaL version: 2.1.3 % 204.37/29.05 % (1956977)Termination reason: Inappropriate % 204.37/29.05 % (1956977)Time elapsed: 0.003 s % 204.37/29.05 % (1956977)Peak memory usage: 11 MB % 204.37/29.05 % (1956977)Instructions burned: 4 (million) % 204.37/29.05 % (1956977)------------------------------ % 204.37/29.05 % (1956977)------------------------------ % 204.37/29.05 % (1956979)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2861401508:rtra=on_2819 on theBenchmark for (2819ds/0Mi) % 204.37/29.05 % (1956979)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 204.37/29.05 % (1956979)Terminated due to inappropriate strategy. % 204.37/29.05 % (1956979)------------------------------ % 204.37/29.05 % (1956979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.37/29.05 % (1956979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.37/29.05 % (1956979)CaDiCaL version: 2.1.3 % 204.37/29.05 % (1956979)Termination reason: Inappropriate % 204.37/29.05 % (1956979)Time elapsed: 0.003 s % 204.37/29.05 % (1956979)Peak memory usage: 11 MB % 204.37/29.05 % (1956979)Instructions burned: 5 (million) % 204.37/29.05 % (1956979)------------------------------ % 204.37/29.05 % (1956979)------------------------------ % 204.37/29.05 % (1956981)% WARNING: option uhcvi not known. % 204.37/29.05 % (1956981)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4073827396:i=271062:add=off:rtra=on:rawr=on_2819 on theBenchmark for (2819ds/271062Mi) % 212.65/30.24 % (1956592)Instruction limit reached! % 212.65/30.24 % (1956592)------------------------------ % 212.65/30.24 % (1956592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.65/30.24 % (1956592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.65/30.24 % (1956592)CaDiCaL version: 2.1.3 % 212.65/30.24 % (1956592)Termination reason: Instruction limit % 212.65/30.24 % (1956592)Termination phase: Saturation % 212.65/30.24 % (1956592)Time elapsed: 12.573 s % 212.65/30.24 % (1956592)Peak memory usage: 94 MB % 212.65/30.24 % (1956592)Instructions burned: 20139 (million) % 212.65/30.24 % (1956983)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2613374717:i=176048:add=on:rtra=on:rawr=on_2816 on theBenchmark for (2816ds/176048Mi) % 212.65/30.24 % (1956961)Instruction limit reached! % 212.65/30.24 % (1956961)------------------------------ % 212.65/30.24 % (1956961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.65/30.24 % (1956961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.65/30.24 % (1956961)CaDiCaL version: 2.1.3 % 212.65/30.24 % (1956961)Termination reason: Instruction limit % 212.65/30.24 % (1956961)Termination phase: Saturation % 212.65/30.24 % (1956961)Time elapsed: 11.145 s % 212.65/30.24 % (1956961)Peak memory usage: 144 MB % 212.65/30.24 % (1956961)Instructions burned: 17627 (million) % 212.65/30.24 % (1956985)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4106706484:i=206:fgj=on:rtra=on_2728 on theBenchmark for (2728ds/206Mi) % 212.65/30.24 % (1956985)Instruction limit reached! % 212.65/30.24 % (1956985)------------------------------ % 212.65/30.24 % (1956985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.65/30.24 % (1956985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.65/30.24 % (1956985)CaDiCaL version: 2.1.3 % 212.65/30.24 % (1956985)Termination reason: Instruction limit % 212.65/30.24 % (1956985)Termination phase: Saturation % 212.65/30.24 % (1956985)Time elapsed: 0.130 s % 212.65/30.24 % (1956985)Peak memory usage: 13 MB % 212.65/30.24 % (1956985)Instructions burned: 207 (million) % 212.65/30.24 % (1956987)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3507001910:i=232:rtra=on_2727 on theBenchmark for (2727ds/232Mi) % 212.65/30.24 % (1956987)Instruction limit reached! % 212.65/30.24 % (1956987)------------------------------ % 212.65/30.24 % (1956987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.65/30.24 % (1956987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.65/30.24 % (1956987)CaDiCaL version: 2.1.3 % 212.65/30.24 % (1956987)Termination reason: Instruction limit % 212.65/30.24 % (1956987)Termination phase: Saturation % 212.65/30.24 % (1956987)Time elapsed: 0.152 s % 212.65/30.24 % (1956987)Peak memory usage: 14 MB % 212.65/30.24 % (1956987)Instructions burned: 232 (million) % 212.65/30.24 % (1956989)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=4170135524:i=262:rtra=on_2725 on theBenchmark for (2725ds/262Mi) % 212.65/30.24 % (1956989)Instruction limit reached! % 212.65/30.24 % (1956989)------------------------------ % 212.65/30.24 % (1956989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.65/30.24 % (1956989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.65/30.24 % (1956989)CaDiCaL version: 2.1.3 % 212.65/30.24 % (1956989)Termination reason: Instruction limit % 212.65/30.24 % (1956989)Termination phase: Saturation % 212.65/30.24 % (1956989)Time elapsed: 0.169 s % 212.65/30.24 % (1956989)Peak memory usage: 14 MB % 212.65/30.24 % (1956989)Instructions burned: 263 (million) % 212.65/30.24 % (1956991)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3891323587:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2723 on theBenchmark for (2723ds/318Mi) % 212.65/30.24 % (1956991)Instruction limit reached! % 212.65/30.24 % (1956991)------------------------------ % 212.65/30.24 % (1956991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.65/30.24 % (1956991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.65/30.24 % (1956991)CaDiCaL version: 2.1.3 % 212.65/30.24 % (1956991)Termination reason: Instruction limit % 212.65/30.24 % (1956991)Termination phase: Saturation % 212.65/30.24 % (1956991)Time elapsed: 0.222 s % 212.65/30.24 % (1956991)Peak memory usage: 15 MB % 212.65/30.24 % (1956991)Instructions burned: 319 (million) % 212.65/30.24 % (1956993)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2487751178:i=1428:nm=2:rtra=on_2721 on theBenchmark for (2721ds/1428Mi) % 224.75/32.02 % (1956993)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 224.75/32.02 % (1956993)Terminated due to inappropriate strategy. % 224.75/32.02 % (1956993)------------------------------ % 224.75/32.02 % (1956993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.75/32.02 % (1956993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.75/32.02 % (1956993)CaDiCaL version: 2.1.3 % 224.75/32.02 % (1956993)Termination reason: Inappropriate % 224.75/32.02 % (1956993)Time elapsed: 0.003 s % 224.75/32.02 % (1956993)Peak memory usage: 10 MB % 224.75/32.02 % (1956993)Instructions burned: 5 (million) % 224.75/32.02 % (1956993)------------------------------ % 224.75/32.02 % (1956993)------------------------------ % 224.75/32.02 % (1956995)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=897778515:i=262:bd=preordered:rtra=on:fsd=on_2720 on theBenchmark for (2720ds/262Mi) % 224.75/32.02 % (1956995)Instruction limit reached! % 224.75/32.02 % (1956995)------------------------------ % 224.75/32.02 % (1956995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.75/32.02 % (1956995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.75/32.02 % (1956995)CaDiCaL version: 2.1.3 % 224.75/32.02 % (1956995)Termination reason: Instruction limit % 224.75/32.02 % (1956995)Termination phase: Saturation % 224.75/32.02 % (1956995)Time elapsed: 0.166 s % 224.75/32.02 % (1956995)Peak memory usage: 13 MB % 224.75/32.02 % (1956995)Instructions burned: 263 (million) % 224.75/32.02 % (1956997)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=1306648407:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2718 on theBenchmark for (2718ds/1368Mi) % 224.75/32.02 % (1956963)Instruction limit reached! % 224.75/32.02 % (1956963)------------------------------ % 224.75/32.02 % (1956963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.75/32.02 % (1956963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.75/32.02 % (1956963)CaDiCaL version: 2.1.3 % 224.75/32.02 % (1956963)Termination reason: Instruction limit % 224.75/32.02 % (1956963)Termination phase: Saturation % 224.75/32.02 % (1956963)Time elapsed: 12.192 s % 224.75/32.02 % (1956963)Peak memory usage: 512 MB % 224.75/32.02 % (1956963)Instructions burned: 53296 (million) % 224.75/32.02 % (1956999)ott-21_1_sil=16000:si=on:fs=off:random_seed=2298618795:i=360:av=off:fsr=off:rtra=on_2716 on theBenchmark for (2716ds/360Mi) % 224.75/32.02 % (1956999)Instruction limit reached! % 224.75/32.02 % (1956999)------------------------------ % 224.75/32.02 % (1956999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.75/32.02 % (1956999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.75/32.02 % (1956999)CaDiCaL version: 2.1.3 % 224.75/32.02 % (1956999)Termination reason: Instruction limit % 224.75/32.02 % (1956999)Termination phase: Saturation % 224.75/32.02 % (1956999)Time elapsed: 0.091 s % 224.75/32.02 % (1956999)Peak memory usage: 13 MB % 224.75/32.02 % (1956999)Instructions burned: 362 (million) % 224.75/32.02 % (1957001)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=127893088:i=954:bd=all:rtra=on_2715 on theBenchmark for (2715ds/954Mi) % 224.75/32.02 % (1957001)Instruction limit reached! % 224.75/32.02 % (1957001)------------------------------ % 224.75/32.02 % (1957001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.75/32.02 % (1957001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.75/32.02 % (1957001)CaDiCaL version: 2.1.3 % 224.75/32.02 % (1957001)Termination reason: Instruction limit % 224.75/32.02 % (1957001)Termination phase: Saturation % 224.75/32.02 % (1957001)Time elapsed: 0.342 s % 224.75/32.02 % (1957001)Peak memory usage: 16 MB % 224.75/32.02 % (1957001)Instructions burned: 955 (million) % 224.75/32.02 % (1957003)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=455966047:fmbsr=1.3:i=1730:ins=25:rtra=on_2711 on theBenchmark for (2711ds/1730Mi) % 224.75/32.02 % (1957003)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 224.75/32.02 % (1957003)Terminated due to inappropriate strategy. % 224.75/32.02 % (1957003)------------------------------ % 224.75/32.02 % (1957003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.75/32.02 % (1957003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.75/32.02 % (1957003)CaDiCaL version: 2.1.3 % 224.75/32.02 % (1957003)Termination reason: Inappropriate % 224.75/32.02 % (1957003)Time elapsed: 0.001 s % 285.26/40.44 % (1957003)Peak memory usage: 10 MB % 285.26/40.44 % (1957003)Instructions burned: 5 (million) % 285.26/40.44 % (1957003)------------------------------ % 285.26/40.44 % (1957003)------------------------------ % 285.26/40.44 % (1957005)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3954873993:i=2358:rtra=on_2711 on theBenchmark for (2711ds/2358Mi) % 285.26/40.44 % (1956997)Instruction limit reached! % 285.26/40.44 % (1956997)------------------------------ % 285.26/40.44 % (1956997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.26/40.44 % (1956997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.26/40.44 % (1956997)CaDiCaL version: 2.1.3 % 285.26/40.44 % (1956997)Termination reason: Instruction limit % 285.26/40.44 % (1956997)Termination phase: Saturation % 285.26/40.44 % (1956997)Time elapsed: 0.888 s % 285.26/40.44 % (1956997)Peak memory usage: 25 MB % 285.26/40.44 % (1956997)Instructions burned: 1369 (million) % 285.26/40.44 % (1957053)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3688566417:i=1778:ins=1:rtra=on_2709 on theBenchmark for (2709ds/1778Mi) % 285.26/40.44 % (1957053)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 285.26/40.44 % (1957053)Terminated due to inappropriate strategy. % 285.26/40.44 % (1957053)------------------------------ % 285.26/40.44 % (1957053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.26/40.44 % (1957053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.26/40.44 % (1957053)CaDiCaL version: 2.1.3 % 285.26/40.44 % (1957053)Termination reason: Inappropriate % 285.26/40.44 % (1957053)Time elapsed: 0.003 s % 285.26/40.44 % (1957053)Peak memory usage: 10 MB % 285.26/40.44 % (1957053)Instructions burned: 5 (million) % 285.26/40.44 % (1957053)------------------------------ % 285.26/40.44 % (1957053)------------------------------ % 285.26/40.44 % (1957065)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=1877389869:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2709 on theBenchmark for (2709ds/1384Mi) % 285.26/40.44 % (1957005)Instruction limit reached! % 285.26/40.44 % (1957005)------------------------------ % 285.26/40.44 % (1957005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.26/40.44 % (1957005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.26/40.44 % (1957005)CaDiCaL version: 2.1.3 % 285.26/40.44 % (1957005)Termination reason: Instruction limit % 285.26/40.44 % (1957005)Termination phase: Saturation % 285.26/40.44 % (1957005)Time elapsed: 0.813 s % 285.26/40.44 % (1957005)Peak memory usage: 27 MB % 285.26/40.44 % (1957005)Instructions burned: 2360 (million) % 285.26/40.44 % (1957164)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1114108855:i=1758:kws=inv_precedence:fsr=off:rtra=on_2703 on theBenchmark for (2703ds/1758Mi) % 285.26/40.44 % (1957065)Instruction limit reached! % 285.26/40.44 % (1957065)------------------------------ % 285.26/40.44 % (1957065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.26/40.44 % (1957065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.26/40.44 % (1957065)CaDiCaL version: 2.1.3 % 285.26/40.44 % (1957065)Termination reason: Instruction limit % 285.26/40.44 % (1957065)Termination phase: Saturation % 285.26/40.44 % (1957065)Time elapsed: 0.897 s % 285.26/40.44 % (1957065)Peak memory usage: 23 MB % 285.26/40.44 % (1957065)Instructions burned: 1385 (million) % 285.26/40.44 % (1957254)fmb+10_1_sil=64000:si=on:random_seed=3400901372:i=44122:nm=2:rtra=on:gsp=on_2700 on theBenchmark for (2700ds/44122Mi) % 285.26/40.44 % (1957254)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 285.26/40.44 % (1957254)Terminated due to inappropriate strategy. % 285.26/40.44 % (1957254)------------------------------ % 285.26/40.44 % (1957254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.26/40.44 % (1957254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.26/40.44 % (1957254)CaDiCaL version: 2.1.3 % 285.26/40.44 % (1957254)Termination reason: Inappropriate % 285.26/40.44 % (1957254)Time elapsed: 0.003 s % 285.26/40.44 % (1957254)Peak memory usage: 10 MB % 285.26/40.44 % (1957254)Instructions burned: 5 (million) % 285.26/40.44 % (1957254)------------------------------ % 285.26/40.44 % (1957254)------------------------------ % 285.26/40.44 % (1957259)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3183817735:i=19030:nm=5:rtra=on_2700 on theBenchmTerminated % 300.14/42.54 % Vampire exiting % 300.14/42.54 Terminated %------------------------------------------------------------------------------