%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX120_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n019.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:46:31 PM UTC 2026 % Result : Timeout 296.01s 42.14s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWX120_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.13/0.26 % Computer : n019.cluster.edu % 0.13/0.26 % Model : x86_64 x86_64 % 0.13/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.26 % Memory : 8046.5625MB % 0.13/0.26 % OS : Linux 6.8.0-71-generic % 0.13/0.26 % CPULimit : 300 % 0.13/0.26 % WCLimit : 300 % 0.13/0.26 % DateTime : Mon Sep 28 15:02:19 UTC 2026 % 0.13/0.27 % CPUTime : % 0.13/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.25/0.30 Running first-order model finding % 0.25/0.30 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 % 6.06/1.18 % (4069487)Will run a generic schedule for satisfiability detection. % 6.06/1.18 % (4069499)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4001645248:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.06/1.18 % (4069494)% WARNING: option uhcvi not known. % 6.06/1.18 % (4069498)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1608032774:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.06/1.18 % (4069495)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3731972594:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.06/1.18 % (4069496)dis+10_1_sil=32000:sp=arity:random_seed=2923505209:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.06/1.18 % (4069493)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4186330720_2999 on theBenchmark for (2999ds/0Mi) % 6.06/1.18 % (4069494)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2212442653:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.06/1.18 % (4069493)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.06/1.18 % (4069493)Terminated due to inappropriate strategy. % 6.06/1.18 % (4069493)------------------------------ % 6.06/1.18 % (4069493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.06/1.18 % (4069493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.06/1.18 % (4069493)CaDiCaL version: 2.1.3 % 6.06/1.18 % (4069493)Termination reason: Inappropriate % 6.06/1.18 % (4069493)Time elapsed: 0.004 s % 6.06/1.18 % (4069493)Peak memory usage: 11 MB % 6.06/1.18 % (4069493)Instructions burned: 3 (million) % 6.06/1.18 % (4069493)------------------------------ % 6.06/1.18 % (4069493)------------------------------ % 6.06/1.18 % (4069497)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2276893149:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.06/1.18 % (4069507)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2907001505:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.06/1.18 % (4069507)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.06/1.18 % (4069507)Terminated due to inappropriate strategy. % 6.06/1.18 % (4069507)------------------------------ % 6.06/1.18 % (4069507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.06/1.18 % (4069507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.06/1.18 % (4069507)CaDiCaL version: 2.1.3 % 6.06/1.18 % (4069507)Termination reason: Inappropriate % 6.06/1.18 % (4069507)Time elapsed: 0.002 s % 6.06/1.18 % (4069507)Peak memory usage: 11 MB % 6.06/1.18 % (4069507)Instructions burned: 3 (million) % 6.06/1.18 % (4069507)------------------------------ % 6.06/1.18 % (4069507)------------------------------ % 6.06/1.18 % (4069510)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2057003366:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.06/1.18 % (4069499)Instruction limit reached! % 6.06/1.18 % (4069499)------------------------------ % 6.06/1.18 % (4069499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.06/1.18 % (4069499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.06/1.18 % (4069499)CaDiCaL version: 2.1.3 % 6.06/1.18 % (4069499)Termination reason: Instruction limit % 6.06/1.18 % (4069499)Termination phase: Saturation % 6.06/1.18 % (4069499)Time elapsed: 0.086 s % 6.06/1.18 % (4069499)Peak memory usage: 14 MB % 6.06/1.18 % (4069499)Instructions burned: 160 (million) % 6.06/1.18 % (4069514)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=4290921241:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.06/1.18 % (4069496)Instruction limit reached! % 6.06/1.18 % (4069496)------------------------------ % 6.06/1.18 % (4069496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.06/1.18 % (4069496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.06/1.18 % (4069496)CaDiCaL version: 2.1.3 % 6.06/1.18 % (4069496)Termination reason: Instruction limit % 6.06/1.18 % (4069496)Termination phase: Saturation % 6.06/1.18 % (4069496)Time elapsed: 0.108 s % 6.06/1.18 % (4069496)Peak memory usage: 13 MB % 6.06/1.18 % (4069496)Instructions burned: 104 (million) % 6.06/1.18 % (4069498)Instruction limit reached! % 6.06/1.18 % (4069498)------------------------------ % 6.06/1.18 % (4069498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.70/1.68 % (4069498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.70/1.68 % (4069498)CaDiCaL version: 2.1.3 % 8.70/1.68 % (4069498)Termination reason: Instruction limit % 8.70/1.68 % (4069498)Termination phase: Saturation % 8.70/1.68 % (4069498)Time elapsed: 0.128 s % 8.70/1.68 % (4069498)Peak memory usage: 13 MB % 8.70/1.68 % (4069498)Instructions burned: 131 (million) % 8.70/1.68 % (4069517)ott-21_1_sil=16000:fs=off:random_seed=2938363243:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.70/1.68 % (4069497)Instruction limit reached! % 8.70/1.68 % (4069497)------------------------------ % 8.70/1.68 % (4069497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.70/1.68 % (4069497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.70/1.68 % (4069497)CaDiCaL version: 2.1.3 % 8.70/1.68 % (4069497)Termination reason: Instruction limit % 8.70/1.68 % (4069497)Termination phase: Saturation % 8.70/1.68 % (4069497)Time elapsed: 0.135 s % 8.70/1.68 % (4069497)Peak memory usage: 13 MB % 8.70/1.68 % (4069497)Instructions burned: 117 (million) % 8.70/1.68 % (4069518)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3018336532:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.70/1.68 % (4069522)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1152191070:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 8.70/1.68 % (4069522)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.70/1.68 % (4069522)Terminated due to inappropriate strategy. % 8.70/1.68 % (4069522)------------------------------ % 8.70/1.68 % (4069522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.70/1.68 % (4069522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.70/1.68 % (4069522)CaDiCaL version: 2.1.3 % 8.70/1.68 % (4069522)Termination reason: Inappropriate % 8.70/1.68 % (4069522)Time elapsed: 0.002 s % 8.70/1.68 % (4069522)Peak memory usage: 10 MB % 8.70/1.68 % (4069522)Instructions burned: 2 (million) % 8.70/1.68 % (4069522)------------------------------ % 8.70/1.68 % (4069522)------------------------------ % 8.70/1.68 % (4069510)Instruction limit reached! % 8.70/1.68 % (4069510)------------------------------ % 8.70/1.68 % (4069510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.70/1.68 % (4069510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.70/1.68 % (4069510)CaDiCaL version: 2.1.3 % 8.70/1.68 % (4069510)Termination reason: Instruction limit % 8.70/1.68 % (4069510)Termination phase: Saturation % 8.70/1.68 % (4069510)Time elapsed: 0.126 s % 8.70/1.68 % (4069510)Peak memory usage: 13 MB % 8.70/1.68 % (4069510)Instructions burned: 131 (million) % 8.70/1.68 % (4069527)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1163853411:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 8.70/1.68 % (4069528)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2879154829:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 8.70/1.68 % (4069528)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.70/1.68 % (4069528)Terminated due to inappropriate strategy. % 8.70/1.68 % (4069528)------------------------------ % 8.70/1.68 % (4069528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.70/1.68 % (4069528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.70/1.68 % (4069528)CaDiCaL version: 2.1.3 % 8.70/1.68 % (4069528)Termination reason: Inappropriate % 8.70/1.68 % (4069528)Time elapsed: 0.003 s % 8.70/1.68 % (4069528)Peak memory usage: 10 MB % 8.70/1.68 % (4069528)Instructions burned: 3 (million) % 8.70/1.68 % (4069528)------------------------------ % 8.70/1.68 % (4069528)------------------------------ % 8.70/1.68 % (4069533)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=1145494444: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) % 8.70/1.68 % (4069517)Instruction limit reached! % 8.70/1.68 % (4069517)------------------------------ % 8.70/1.68 % (4069517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.70/1.68 % (4069517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.70/1.68 % (4069517)CaDiCaL version: 2.1.3 % 8.70/1.68 % (4069517)Termination reason: Instruction limit % 8.70/1.68 % (4069517)Termination phase: Saturation % 31.03/4.79 % (4069517)Time elapsed: 0.156 s % 31.03/4.79 % (4069517)Peak memory usage: 12 MB % 31.03/4.79 % (4069517)Instructions burned: 181 (million) % 31.03/4.79 % (4069538)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3797594094:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 31.03/4.79 % (4069514)Instruction limit reached! % 31.03/4.79 % (4069514)------------------------------ % 31.03/4.79 % (4069514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.03/4.79 % (4069514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.03/4.79 % (4069514)CaDiCaL version: 2.1.3 % 31.03/4.79 % (4069514)Termination reason: Instruction limit % 31.03/4.79 % (4069514)Termination phase: Saturation % 31.03/4.79 % (4069514)Time elapsed: 0.355 s % 31.03/4.79 % (4069514)Peak memory usage: 18 MB % 31.03/4.79 % (4069514)Instructions burned: 685 (million) % 31.03/4.79 % (4069550)fmb+10_1_sil=64000:random_seed=2195971361:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 31.03/4.79 % (4069550)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.03/4.79 % (4069550)Terminated due to inappropriate strategy. % 31.03/4.79 % (4069550)------------------------------ % 31.03/4.79 % (4069550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.03/4.79 % (4069550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.03/4.79 % (4069550)CaDiCaL version: 2.1.3 % 31.03/4.79 % (4069550)Termination reason: Inappropriate % 31.03/4.79 % (4069550)Time elapsed: 0.003 s % 31.03/4.79 % (4069550)Peak memory usage: 10 MB % 31.03/4.79 % (4069550)Instructions burned: 3 (million) % 31.03/4.79 % (4069550)------------------------------ % 31.03/4.79 % (4069550)------------------------------ % 31.03/4.79 % (4069552)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2760095626:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 31.03/4.79 % (4069552)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.03/4.79 % (4069552)Terminated due to inappropriate strategy. % 31.03/4.79 % (4069552)------------------------------ % 31.03/4.79 % (4069552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.03/4.79 % (4069552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.03/4.79 % (4069552)CaDiCaL version: 2.1.3 % 31.03/4.79 % (4069552)Termination reason: Inappropriate % 31.03/4.79 % (4069552)Time elapsed: 0.001 s % 31.03/4.79 % (4069552)Peak memory usage: 10 MB % 31.03/4.79 % (4069552)Instructions burned: 3 (million) % 31.03/4.79 % (4069552)------------------------------ % 31.03/4.79 % (4069552)------------------------------ % 31.03/4.79 % (4069555)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=63137792:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 31.03/4.79 % (4069555)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.03/4.79 % (4069555)Terminated due to inappropriate strategy. % 31.03/4.79 % (4069555)------------------------------ % 31.03/4.79 % (4069555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.03/4.79 % (4069555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.03/4.79 % (4069555)CaDiCaL version: 2.1.3 % 31.03/4.79 % (4069555)Termination reason: Inappropriate % 31.03/4.79 % (4069555)Time elapsed: 0.001 s % 31.03/4.79 % (4069555)Peak memory usage: 10 MB % 31.03/4.79 % (4069555)Instructions burned: 3 (million) % 31.03/4.79 % (4069555)------------------------------ % 31.03/4.79 % (4069555)------------------------------ % 31.03/4.79 % (4069557)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3756028982:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 31.03/4.79 % (4069518)Instruction limit reached! % 31.03/4.79 % (4069518)------------------------------ % 31.03/4.79 % (4069518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.03/4.79 % (4069518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.03/4.79 % (4069518)CaDiCaL version: 2.1.3 % 31.03/4.79 % (4069518)Termination reason: Instruction limit % 31.03/4.79 % (4069518)Termination phase: Saturation % 31.03/4.79 % (4069518)Time elapsed: 0.486 s % 31.03/4.79 % (4069518)Peak memory usage: 14 MB % 31.03/4.79 % (4069518)Instructions burned: 477 (million) % 31.03/4.79 % (4069561)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1482395572:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi) % 31.03/4.79 % (4069533)Instruction limit reached! % 31.03/4.79 % (4069533)------------------------------ % 42.06/6.27 % (4069533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.06/6.27 % (4069533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.06/6.27 % (4069533)CaDiCaL version: 2.1.3 % 42.06/6.27 % (4069533)Termination reason: Instruction limit % 42.06/6.27 % (4069533)Termination phase: Saturation % 42.06/6.27 % (4069533)Time elapsed: 0.580 s % 42.06/6.27 % (4069533)Peak memory usage: 17 MB % 42.06/6.27 % (4069533)Instructions burned: 692 (million) % 42.06/6.27 % (4069571)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=72345443:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 42.06/6.27 % (4069571)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 42.06/6.27 % (4069571)Terminated due to inappropriate strategy. % 42.06/6.27 % (4069571)------------------------------ % 42.06/6.27 % (4069571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.06/6.27 % (4069571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.06/6.27 % (4069571)CaDiCaL version: 2.1.3 % 42.06/6.27 % (4069571)Termination reason: Inappropriate % 42.06/6.27 % (4069571)Time elapsed: 0.004 s % 42.06/6.27 % (4069571)Peak memory usage: 11 MB % 42.06/6.27 % (4069571)Instructions burned: 3 (million) % 42.06/6.27 % (4069571)------------------------------ % 42.06/6.27 % (4069571)------------------------------ % 42.06/6.27 % (4069574)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=905977526:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 42.06/6.27 % (4069574)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 42.06/6.27 % (4069574)Terminated due to inappropriate strategy. % 42.06/6.27 % (4069574)------------------------------ % 42.06/6.27 % (4069574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.06/6.27 % (4069574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.06/6.27 % (4069574)CaDiCaL version: 2.1.3 % 42.06/6.27 % (4069574)Termination reason: Inappropriate % 42.06/6.27 % (4069574)Time elapsed: 0.003 s % 42.06/6.27 % (4069574)Peak memory usage: 10 MB % 42.06/6.27 % (4069574)Instructions burned: 3 (million) % 42.06/6.27 % (4069574)------------------------------ % 42.06/6.27 % (4069574)------------------------------ % 42.06/6.27 % (4069578)ott-2_1_sil=16000:newcnf=on:random_seed=1794397076:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 42.06/6.27 % (4069538)Instruction limit reached! % 42.06/6.27 % (4069538)------------------------------ % 42.06/6.27 % (4069538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.06/6.27 % (4069538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.06/6.27 % (4069538)CaDiCaL version: 2.1.3 % 42.06/6.27 % (4069538)Termination reason: Instruction limit % 42.06/6.27 % (4069538)Termination phase: Saturation % 42.06/6.27 % (4069538)Time elapsed: 0.734 s % 42.06/6.27 % (4069538)Peak memory usage: 19 MB % 42.06/6.27 % (4069538)Instructions burned: 879 (million) % 42.06/6.27 % (4069584)ott+10_1_sil=32000:tgt=ground:random_seed=3499867575:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 42.06/6.27 % (4069527)Instruction limit reached! % 42.06/6.27 % (4069527)------------------------------ % 42.06/6.27 % (4069527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.06/6.27 % (4069527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.06/6.27 % (4069527)CaDiCaL version: 2.1.3 % 42.06/6.27 % (4069527)Termination reason: Instruction limit % 42.06/6.27 % (4069527)Termination phase: Saturation % 42.06/6.27 % (4069527)Time elapsed: 1.079 s % 42.06/6.27 % (4069527)Peak memory usage: 19 MB % 42.06/6.27 % (4069527)Instructions burned: 1179 (million) % 42.06/6.27 % (4069593)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4175029319:i=54282_2986 on theBenchmark for (2986ds/54282Mi) % 42.06/6.27 % (4069593)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 42.06/6.27 % (4069593)Terminated due to inappropriate strategy. % 42.06/6.27 % (4069593)------------------------------ % 42.06/6.27 % (4069593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.06/6.27 % (4069593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.06/6.27 % (4069593)CaDiCaL version: 2.1.3 % 42.06/6.27 % (4069593)Termination reason: Inappropriate % 42.06/6.27 % (4069593)Time elapsed: 0.004 s % 42.06/6.27 % (4069593)Peak memory usage: 11 MB % 42.06/6.27 % (4069593)Instructions burned: 3 (million) % 150.70/21.53 % (4069593)------------------------------ % 150.70/21.53 % (4069593)------------------------------ % 150.70/21.53 % (4069596)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3816482052:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi) % 150.70/21.53 % (4069578)Instruction limit reached! % 150.70/21.53 % (4069578)------------------------------ % 150.70/21.53 % (4069578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.70/21.53 % (4069578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.70/21.53 % (4069578)CaDiCaL version: 2.1.3 % 150.70/21.53 % (4069578)Termination reason: Instruction limit % 150.70/21.53 % (4069578)Termination phase: Saturation % 150.70/21.53 % (4069578)Time elapsed: 0.865 s % 150.70/21.53 % (4069578)Peak memory usage: 19 MB % 150.70/21.53 % (4069578)Instructions burned: 869 (million) % 150.70/21.53 % (4069612)dis+21_1_sil=32000:sas=cadical:random_seed=2985714557:i=3773:amm=off_2981 on theBenchmark for (2981ds/3773Mi) % 150.70/21.53 % (4069561)Instruction limit reached! % 150.70/21.53 % (4069561)------------------------------ % 150.70/21.53 % (4069561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.70/21.53 % (4069561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.70/21.53 % (4069561)CaDiCaL version: 2.1.3 % 150.70/21.53 % (4069561)Termination reason: Instruction limit % 150.70/21.53 % (4069561)Termination phase: Saturation % 150.70/21.53 % (4069561)Time elapsed: 1.418 s % 150.70/21.53 % (4069561)Peak memory usage: 29 MB % 150.70/21.53 % (4069561)Instructions burned: 1472 (million) % 150.70/21.53 % (4069623)ott+11_1_sil=16000:gs=on:random_seed=3160601077:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi) % 150.70/21.53 % (4069557)Instruction limit reached! % 150.70/21.53 % (4069557)------------------------------ % 150.70/21.53 % (4069557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.70/21.53 % (4069557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.70/21.53 % (4069557)CaDiCaL version: 2.1.3 % 150.70/21.53 % (4069557)Termination reason: Instruction limit % 150.70/21.53 % (4069557)Termination phase: Saturation % 150.70/21.53 % (4069557)Time elapsed: 2.091 s % 150.70/21.53 % (4069557)Peak memory usage: 42 MB % 150.70/21.53 % (4069557)Instructions burned: 5132 (million) % 150.70/21.53 % (4069636)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3643323924:fmbsr=1.6:i=67534_2973 on theBenchmark for (2973ds/67534Mi) % 150.70/21.53 % (4069636)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.70/21.53 % (4069636)Terminated due to inappropriate strategy. % 150.70/21.53 % (4069636)------------------------------ % 150.70/21.53 % (4069636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.70/21.53 % (4069636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.70/21.53 % (4069636)CaDiCaL version: 2.1.3 % 150.70/21.53 % (4069636)Termination reason: Inappropriate % 150.70/21.53 % (4069636)Time elapsed: 0.003 s % 150.70/21.53 % (4069636)Peak memory usage: 10 MB % 150.70/21.53 % (4069636)Instructions burned: 3 (million) % 150.70/21.53 % (4069636)------------------------------ % 150.70/21.53 % (4069636)------------------------------ % 150.70/21.53 % (4069638)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2375963947:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2972 on theBenchmark for (2972ds/4591Mi) % 150.70/21.53 % (4069623)Instruction limit reached! % 150.70/21.53 % (4069623)------------------------------ % 150.70/21.53 % (4069623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.70/21.53 % (4069623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.70/21.53 % (4069623)CaDiCaL version: 2.1.3 % 150.70/21.53 % (4069623)Termination reason: Instruction limit % 150.70/21.53 % (4069623)Termination phase: Saturation % 150.70/21.53 % (4069623)Time elapsed: 2.015 s % 150.70/21.53 % (4069623)Peak memory usage: 23 MB % 150.70/21.53 % (4069623)Instructions burned: 2252 (million) % 150.70/21.53 % (4069675)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1414699036:i=29340_2957 on theBenchmark for (2957ds/29340Mi) % 150.70/21.53 % (4069584)Instruction limit reached! % 150.70/21.53 % (4069584)------------------------------ % 150.70/21.53 % (4069584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.70/21.53 % (4069584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.70/21.53 % (4069584)CaDiCaL version: 2.1.3 % 150.70/21.53 % (4069584)Termination reason: Instruction limit % 206.20/29.38 % (4069584)Termination phase: Saturation % 206.20/29.38 % (4069584)Time elapsed: 3.352 s % 206.20/29.38 % (4069584)Peak memory usage: 33 MB % 206.20/29.38 % (4069584)Instructions burned: 5114 (million) % 206.20/29.38 % (4069596)Instruction limit reached! % 206.20/29.38 % (4069596)------------------------------ % 206.20/29.38 % (4069596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.20/29.38 % (4069596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.20/29.38 % (4069596)CaDiCaL version: 2.1.3 % 206.20/29.38 % (4069596)Termination reason: Instruction limit % 206.20/29.38 % (4069596)Termination phase: Saturation % 206.20/29.38 % (4069596)Time elapsed: 3.080 s % 206.20/29.38 % (4069596)Peak memory usage: 36 MB % 206.20/29.38 % (4069596)Instructions burned: 3513 (million) % 206.20/29.38 % (4069680)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1496285448:i=5211_2955 on theBenchmark for (2955ds/5211Mi) % 206.20/29.38 % (4069681)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1704928104:i=5497:nm=2_2955 on theBenchmark for (2955ds/5497Mi) % 206.20/29.38 % (4069681)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 206.20/29.38 % (4069681)Terminated due to inappropriate strategy. % 206.20/29.38 % (4069681)------------------------------ % 206.20/29.38 % (4069681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.20/29.38 % (4069681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.20/29.38 % (4069681)CaDiCaL version: 2.1.3 % 206.20/29.38 % (4069681)Termination reason: Inappropriate % 206.20/29.38 % (4069681)Time elapsed: 0.004 s % 206.20/29.38 % (4069681)Peak memory usage: 11 MB % 206.20/29.38 % (4069681)Instructions burned: 3 (million) % 206.20/29.38 % (4069681)------------------------------ % 206.20/29.38 % (4069681)------------------------------ % 206.20/29.38 % (4069685)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1302956825:fmbsr=2:i=46332_2954 on theBenchmark for (2954ds/46332Mi) % 206.20/29.38 % (4069685)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 206.20/29.38 % (4069685)Terminated due to inappropriate strategy. % 206.20/29.38 % (4069685)------------------------------ % 206.20/29.38 % (4069685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.20/29.38 % (4069685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.20/29.38 % (4069685)CaDiCaL version: 2.1.3 % 206.20/29.38 % (4069685)Termination reason: Inappropriate % 206.20/29.38 % (4069685)Time elapsed: 0.004 s % 206.20/29.38 % (4069685)Peak memory usage: 11 MB % 206.20/29.38 % (4069685)Instructions burned: 3 (million) % 206.20/29.38 % (4069685)------------------------------ % 206.20/29.38 % (4069685)------------------------------ % 206.20/29.38 % (4069687)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1768524877:i=14071_2954 on theBenchmark for (2954ds/14071Mi) % 206.20/29.38 % (4069687)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 206.20/29.38 % (4069687)Terminated due to inappropriate strategy. % 206.20/29.38 % (4069687)------------------------------ % 206.20/29.38 % (4069687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.20/29.38 % (4069687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.20/29.38 % (4069687)CaDiCaL version: 2.1.3 % 206.20/29.38 % (4069687)Termination reason: Inappropriate % 206.20/29.38 % (4069687)Time elapsed: 0.004 s % 206.20/29.38 % (4069687)Peak memory usage: 10 MB % 206.20/29.38 % (4069687)Instructions burned: 3 (million) % 206.20/29.38 % (4069687)------------------------------ % 206.20/29.38 % (4069687)------------------------------ % 206.20/29.38 % (4069689)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2105355218:i=22565:add=on:rawr=on_2953 on theBenchmark for (2953ds/22565Mi) % 206.20/29.38 % (4069612)Instruction limit reached! % 206.20/29.38 % (4069612)------------------------------ % 206.20/29.38 % (4069612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.20/29.38 % (4069612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.20/29.38 % (4069612)CaDiCaL version: 2.1.3 % 206.20/29.38 % (4069612)Termination reason: Instruction limit % 206.20/29.38 % (4069612)Termination phase: Saturation % 206.20/29.38 % (4069612)Time elapsed: 3.233 s % 206.20/29.38 % (4069612)Peak memory usage: 33 MB % 206.20/29.38 % (4069612)Instructions burned: 3774 (million) % 206.20/29.38 % (4069697)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1095772084:i=8173:av=off_2948 on theBenchmark for (2948ds/8173Mi) % 206.20/29.38 % (4069638)Instruction limit reached! % 207.63/29.54 % (4069638)------------------------------ % 207.63/29.54 % (4069638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.63/29.54 % (4069638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.63/29.54 % (4069638)CaDiCaL version: 2.1.3 % 207.63/29.54 % (4069638)Termination reason: Instruction limit % 207.63/29.54 % (4069638)Termination phase: Saturation % 207.63/29.54 % (4069638)Time elapsed: 3.209 s % 207.63/29.54 % (4069638)Peak memory usage: 33 MB % 207.63/29.54 % (4069638)Instructions burned: 4591 (million) % 207.63/29.54 % (4069711)dis+10_16:1_sil=16000:random_seed=4044092350:i=9155:fsr=off_2940 on theBenchmark for (2940ds/9155Mi) % 207.63/29.54 % (4069680)Instruction limit reached! % 207.63/29.54 % (4069680)------------------------------ % 207.63/29.54 % (4069680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.63/29.54 % (4069680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.63/29.54 % (4069680)CaDiCaL version: 2.1.3 % 207.63/29.54 % (4069680)Termination reason: Instruction limit % 207.63/29.54 % (4069680)Termination phase: Saturation % 207.63/29.54 % (4069680)Time elapsed: 2.455 s % 207.63/29.54 % (4069680)Peak memory usage: 46 MB % 207.63/29.54 % (4069680)Instructions burned: 5212 (million) % 207.63/29.54 % (4069731)ott-3_8_sil=64000:random_seed=969186490:i=20139:bs=on_2930 on theBenchmark for (2930ds/20139Mi) % 207.63/29.54 % (4069697)Instruction limit reached! % 207.63/29.54 % (4069697)------------------------------ % 207.63/29.54 % (4069697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.63/29.54 % (4069697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.63/29.54 % (4069697)CaDiCaL version: 2.1.3 % 207.63/29.54 % (4069697)Termination reason: Instruction limit % 207.63/29.54 % (4069697)Termination phase: Saturation % 207.63/29.54 % (4069697)Time elapsed: 7.936 s % 207.63/29.54 % (4069697)Peak memory usage: 47 MB % 207.63/29.54 % (4069697)Instructions burned: 8173 (million) % 207.63/29.54 % (4069763)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4247279029:fmbsr=2:i=32576_2869 on theBenchmark for (2869ds/32576Mi) % 207.63/29.54 % (4069763)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 207.63/29.54 % (4069763)Terminated due to inappropriate strategy. % 207.63/29.54 % (4069763)------------------------------ % 207.63/29.54 % (4069763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.63/29.54 % (4069763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.63/29.54 % (4069763)CaDiCaL version: 2.1.3 % 207.63/29.54 % (4069763)Termination reason: Inappropriate % 207.63/29.54 % (4069763)Time elapsed: 0.003 s % 207.63/29.54 % (4069763)Peak memory usage: 11 MB % 207.63/29.54 % (4069763)Instructions burned: 3 (million) % 207.63/29.54 % (4069763)------------------------------ % 207.63/29.54 % (4069763)------------------------------ % 207.63/29.54 % (4069766)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1351156920:i=11404_2868 on theBenchmark for (2868ds/11404Mi) % 207.63/29.54 % (4069711)Instruction limit reached! % 207.63/29.54 % (4069711)------------------------------ % 207.63/29.54 % (4069711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.63/29.54 % (4069711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.63/29.54 % (4069711)CaDiCaL version: 2.1.3 % 207.63/29.54 % (4069711)Termination reason: Instruction limit % 207.63/29.54 % (4069711)Termination phase: Saturation % 207.63/29.54 % (4069711)Time elapsed: 8.001 s % 207.63/29.54 % (4069711)Peak memory usage: 53 MB % 207.63/29.54 % (4069711)Instructions burned: 9156 (million) % 207.63/29.54 % (4069772)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1980788846:i=14134_2860 on theBenchmark for (2860ds/14134Mi) % 207.63/29.54 % (4069731)Instruction limit reached! % 207.63/29.54 % (4069731)------------------------------ % 207.63/29.54 % (4069731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.63/29.54 % (4069731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.63/29.54 % (4069731)CaDiCaL version: 2.1.3 % 207.63/29.54 % (4069731)Termination reason: Instruction limit % 207.63/29.54 % (4069731)Termination phase: Saturation % 207.63/29.54 % (4069731)Time elapsed: 11.783 s % 207.63/29.54 % (4069731)Peak memory usage: 98 MB % 207.63/29.54 % (4069731)Instructions burned: 20140 (million) % 207.63/29.54 % (4069785)dis+33_16_sil=32000:sac=on:random_seed=186378876:i=15851:nm=0_2812 on theBenchmark for (2812ds/15851Mi) % 207.63/29.54 % (4069689)Instruction limit reached! % 207.63/29.54 % (4069689)------------------------------ % 207.63/29.54 % (4069689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.67/38.75 % (4069689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.67/38.75 % (4069689)CaDiCaL version: 2.1.3 % 272.67/38.75 % (4069689)Termination reason: Instruction limit % 272.67/38.75 % (4069689)Termination phase: Saturation % 272.67/38.75 % (4069689)Time elapsed: 16.556 s % 272.67/38.75 % (4069689)Peak memory usage: 198 MB % 272.67/38.75 % (4069689)Instructions burned: 22567 (million) % 272.67/38.75 % (4069789)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2196207529:avsq=on:i=17627:add=on:amm=off_2787 on theBenchmark for (2787ds/17627Mi) % 272.67/38.75 % (4069766)Instruction limit reached! % 272.67/38.75 % (4069766)------------------------------ % 272.67/38.75 % (4069766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.67/38.75 % (4069766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.67/38.75 % (4069766)CaDiCaL version: 2.1.3 % 272.67/38.75 % (4069766)Termination reason: Instruction limit % 272.67/38.75 % (4069766)Termination phase: Saturation % 272.67/38.75 % (4069766)Time elapsed: 11.605 s % 272.67/38.75 % (4069766)Peak memory usage: 61 MB % 272.67/38.75 % (4069766)Instructions burned: 11404 (million) % 272.67/38.75 % (4069799)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2225583763:s2a=on:i=53295_2752 on theBenchmark for (2752ds/53295Mi) % 272.67/38.75 % (4069785)Instruction limit reached! % 272.67/38.75 % (4069785)------------------------------ % 272.67/38.75 % (4069785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.67/38.75 % (4069785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.67/38.75 % (4069785)CaDiCaL version: 2.1.3 % 272.67/38.75 % (4069785)Termination reason: Instruction limit % 272.67/38.75 % (4069785)Termination phase: Saturation % 272.67/38.75 % (4069785)Time elapsed: 7.954 s % 272.67/38.75 % (4069785)Peak memory usage: 134 MB % 272.67/38.75 % (4069785)Instructions burned: 15851 (million) % 272.67/38.75 % (4069803)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=182954859:i=26857:ins=20_2732 on theBenchmark for (2732ds/26857Mi) % 272.67/38.75 % (4069803)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.67/38.75 % (4069803)Terminated due to inappropriate strategy. % 272.67/38.75 % (4069803)------------------------------ % 272.67/38.75 % (4069803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.67/38.75 % (4069803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.67/38.75 % (4069803)CaDiCaL version: 2.1.3 % 272.67/38.75 % (4069803)Termination reason: Inappropriate % 272.67/38.75 % (4069803)Time elapsed: 0.002 s % 272.67/38.75 % (4069803)Peak memory usage: 10 MB % 272.67/38.75 % (4069803)Instructions burned: 3 (million) % 272.67/38.75 % (4069803)------------------------------ % 272.67/38.75 % (4069803)------------------------------ % 272.67/38.75 % (4069805)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=801580772:i=28120:bs=on:fsr=off_2731 on theBenchmark for (2731ds/28120Mi) % 272.67/38.75 % (4069772)Instruction limit reached! % 272.67/38.75 % (4069772)------------------------------ % 272.67/38.75 % (4069772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.67/38.75 % (4069772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.67/38.75 % (4069772)CaDiCaL version: 2.1.3 % 272.67/38.75 % (4069772)Termination reason: Instruction limit % 272.67/38.75 % (4069772)Termination phase: Saturation % 272.67/38.75 % (4069772)Time elapsed: 14.975 s % 272.67/38.75 % (4069772)Peak memory usage: 73 MB % 272.67/38.75 % (4069772)Instructions burned: 14134 (million) % 272.67/38.75 % (4069811)fmb+10_1_sil=256000:fmbss=7:random_seed=2236678248:fmbsr=1.6:i=182295_2709 on theBenchmark for (2709ds/182295Mi) % 272.67/38.75 % (4069811)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.67/38.75 % (4069811)Terminated due to inappropriate strategy. % 272.67/38.75 % (4069811)------------------------------ % 272.67/38.75 % (4069811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.67/38.75 % (4069811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.67/38.75 % (4069811)CaDiCaL version: 2.1.3 % 272.67/38.75 % (4069811)Termination reason: Inappropriate % 272.67/38.75 % (4069811)Time elapsed: 0.003 s % 272.67/38.75 % (4069811)Peak memory usage: 11 MB % 272.67/38.75 % (4069811)Instructions burned: 3 (million) % 272.67/38.75 % (4069811)------------------------------ % 272.67/38.75 % (4069811)------------------------------ % 272.67/38.75 % (4069813)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1820094466:i=44625:gsp=on_2709 on theBenchmark for (2709ds/44625Mi) % 285.12/40.50 % (4069813)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 285.12/40.50 % (4069813)Terminated due to inappropriate strategy. % 285.12/40.50 % (4069813)------------------------------ % 285.12/40.50 % (4069813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.12/40.50 % (4069813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.12/40.50 % (4069813)CaDiCaL version: 2.1.3 % 285.12/40.50 % (4069813)Termination reason: Inappropriate % 285.12/40.50 % (4069813)Time elapsed: 0.005 s % 285.12/40.50 % (4069813)Peak memory usage: 11 MB % 285.12/40.50 % (4069813)Instructions burned: 3 (million) % 285.12/40.50 % (4069813)------------------------------ % 285.12/40.50 % (4069813)------------------------------ % 285.12/40.50 % (4069815)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2006057763:i=160505_2709 on theBenchmark for (2709ds/160505Mi) % 285.12/40.50 % (4069815)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 285.12/40.50 % (4069815)Terminated due to inappropriate strategy. % 285.12/40.50 % (4069815)------------------------------ % 285.12/40.50 % (4069815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.12/40.50 % (4069815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.12/40.50 % (4069815)CaDiCaL version: 2.1.3 % 285.12/40.50 % (4069815)Termination reason: Inappropriate % 285.12/40.50 % (4069815)Time elapsed: 0.003 s % 285.12/40.50 % (4069815)Peak memory usage: 10 MB % 285.12/40.50 % (4069815)Instructions burned: 3 (million) % 285.12/40.50 % (4069815)------------------------------ % 285.12/40.50 % (4069815)------------------------------ % 285.12/40.50 % (4069817)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2364286162:fmbsr=1.3:i=225729_2708 on theBenchmark for (2708ds/225729Mi) % 285.12/40.50 % (4069817)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 285.12/40.50 % (4069817)Terminated due to inappropriate strategy. % 285.12/40.50 % (4069817)------------------------------ % 285.12/40.50 % (4069817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.12/40.50 % (4069817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.12/40.50 % (4069817)CaDiCaL version: 2.1.3 % 285.12/40.50 % (4069817)Termination reason: Inappropriate % 285.12/40.50 % (4069817)Time elapsed: 0.003 s % 285.12/40.50 % (4069817)Peak memory usage: 11 MB % 285.12/40.50 % (4069817)Instructions burned: 3 (million) % 285.12/40.50 % (4069817)------------------------------ % 285.12/40.50 % (4069817)------------------------------ % 285.12/40.50 % (4069819)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=406491389:fmbsr=2:i=185024:ins=7_2708 on theBenchmark for (2708ds/185024Mi) % 285.12/40.50 % (4069819)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 285.12/40.50 % (4069819)Terminated due to inappropriate strategy. % 285.12/40.50 % (4069819)------------------------------ % 285.12/40.50 % (4069819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.12/40.50 % (4069819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.12/40.50 % (4069819)CaDiCaL version: 2.1.3 % 285.12/40.50 % (4069819)Termination reason: Inappropriate % 285.12/40.50 % (4069819)Time elapsed: 0.003 s % 285.12/40.50 % (4069819)Peak memory usage: 11 MB % 285.12/40.50 % (4069819)Instructions burned: 3 (million) % 285.12/40.50 % (4069819)------------------------------ % 285.12/40.50 % (4069819)------------------------------ % 285.12/40.50 % (4069821)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=994321109:rtra=on_2708 on theBenchmark for (2708ds/0Mi) % 285.12/40.50 % (4069821)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 285.12/40.50 % (4069821)Terminated due to inappropriate strategy. % 285.12/40.50 % (4069821)------------------------------ % 285.12/40.50 % (4069821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.12/40.50 % (4069821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.12/40.50 % (4069821)CaDiCaL version: 2.1.3 % 285.12/40.50 % (4069821)Termination reason: Inappropriate % 285.12/40.50 % (4069821)Time elapsed: 0.003 s % 285.12/40.50 % (4069821)Peak memory usage: 11 MB % 285.12/40.50 % (4069821)Instructions burned: 4 (million) % 285.12/40.50 % (4069821)------------------------------ % 285.12/40.50 % (4069821)------------------------------ % 285.12/40.50 % (4069823)% WARNING: option uhcvi not known. % 285.12/40.50 % (4069823)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1266480792:i=271062:add=off:rtra=on:rawr=on_2707 on theBenchmark for (2707ds/271062Mi) % 296.01/42.14 % (4069675)Instruction limit reached! % 296.01/42.14 % (4069675)------------------------------ % 296.01/42.14 % (4069675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.01/42.14 % (4069675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.01/42.14 % (4069675)CaDiCaL version: 2.1.3 % 296.01/42.14 % (4069675)Termination reason: Instruction limit % 296.01/42.14 % (4069675)Termination phase: Saturation % 296.01/42.14 % (4069675)Time elapsed: 25.331 s % 296.01/42.14 % (4069675)Peak memory usage: 114 MB % 296.01/42.14 % (4069675)Instructions burned: 29340 (million) % 296.01/42.14 % (4069825)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1374103456:i=176048:add=on:rtra=on:rawr=on_2704 on theBenchmark for (2704ds/176048Mi) % 296.01/42.14 % (4069789)Instruction limit reached! % 296.01/42.14 % (4069789)------------------------------ % 296.01/42.14 % (4069789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.01/42.14 % (4069789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.01/42.14 % (4069789)CaDiCaL version: 2.1.3 % 296.01/42.14 % (4069789)Termination reason: Instruction limit % 296.01/42.14 % (4069789)Termination phase: Saturation % 296.01/42.14 % (4069789)Time elapsed: 15.880 s % 296.01/42.14 % (4069789)Peak memory usage: 211 MB % 296.01/42.14 % (4069789)Instructions burned: 17627 (million) % 296.01/42.14 % (4069842)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3414757868:i=206:fgj=on:rtra=on_2627 on theBenchmark for (2627ds/206Mi) % 296.01/42.14 % (4069842)Instruction limit reached! % 296.01/42.14 % (4069842)------------------------------ % 296.01/42.14 % (4069842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.01/42.14 % (4069842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.01/42.14 % (4069842)CaDiCaL version: 2.1.3 % 296.01/42.14 % (4069842)Termination reason: Instruction limit % 296.01/42.14 % (4069842)Termination phase: Saturation % 296.01/42.14 % (4069842)Time elapsed: 0.214 s % 296.01/42.14 % (4069842)Peak memory usage: 14 MB % 296.01/42.14 % (4069842)Instructions burned: 206 (million) % 296.01/42.14 % (4069844)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1730871293:i=232:rtra=on_2625 on theBenchmark for (2625ds/232Mi) % 296.01/42.14 % (4069844)Instruction limit reached! % 296.01/42.14 % (4069844)------------------------------ % 296.01/42.14 % (4069844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.01/42.14 % (4069844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.01/42.14 % (4069844)CaDiCaL version: 2.1.3 % 296.01/42.14 % (4069844)Termination reason: Instruction limit % 296.01/42.14 % (4069844)Termination phase: Saturation % 296.01/42.14 % (4069844)Time elapsed: 0.218 s % 296.01/42.14 % (4069844)Peak memory usage: 14 MB % 296.01/42.14 % (4069844)Instructions burned: 233 (million) % 296.01/42.14 % (4069847)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3656378450:i=262:rtra=on_2622 on theBenchmark for (2622ds/262Mi) % 296.01/42.14 % (4069847)Instruction limit reached! % 296.01/42.14 % (4069847)------------------------------ % 296.01/42.14 % (4069847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.01/42.14 % (4069847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.01/42.14 % (4069847)CaDiCaL version: 2.1.3 % 296.01/42.14 % (4069847)Termination reason: Instruction limit % 296.01/42.14 % (4069847)Termination phase: Saturation % 296.01/42.14 % (4069847)Time elapsed: 0.278 s % 296.01/42.14 % (4069847)Peak memory usage: 14 MB % 296.01/42.14 % (4069847)Instructions burned: 262 (million) % 296.01/42.14 % (4069849)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2324837134:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2619 on theBenchmark for (2619ds/318Mi) % 296.01/42.14 % (4069849)Instruction limit reached! % 296.01/42.14 % (4069849)------------------------------ % 296.01/42.14 % (4069849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.01/42.14 % (4069849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.01/42.14 % (4069849)CaDiCaL version: 2.1.3 % 296.01/42.14 % (4069849)Termination reason: Instruction limit % 296.01/42.14 % (4069849)Termination phase: Saturation % 296.01/42.14 % (4069849)Time elapsed: 0.350 s % 296.01/42.14 % (4069849)Peak memory usage: 16 MB % 296.01/42.14 % (4069849)Instructions burned: 318 (million) % 296.01/42.14 % (4069851)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1614535584:i=1428:nm=2:rtra=onTerminated % 300.08/42.63 % Vampire exiting % 300.08/42.63 Terminated %------------------------------------------------------------------------------