%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW627_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n009.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:33 PM UTC 2026 % Result : Timeout 300.17s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW627_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 % Computer : n009.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 14:23:00 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/0.22 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 % 4.42/0.91 % (3060217)Will run a generic schedule for satisfiability detection. % 4.42/0.91 % (3060235)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1676458023:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 4.42/0.91 % (3060231)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3140376032:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 4.42/0.91 % (3060233)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=274970990:i=116_2999 on theBenchmark for (2999ds/116Mi) % 4.42/0.91 % (3060232)dis+10_1_sil=32000:sp=arity:random_seed=1671566603:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 4.42/0.91 % (3060234)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=719360375:i=131_2999 on theBenchmark for (2999ds/131Mi) % 4.42/0.91 % (3060229)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1349482667_2999 on theBenchmark for (2999ds/0Mi) % 4.42/0.91 % (3060230)% WARNING: option uhcvi not known. % 4.42/0.91 % (3060229)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.42/0.91 % (3060229)Terminated due to inappropriate strategy. % 4.42/0.91 % (3060229)------------------------------ % 4.42/0.91 % (3060229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.42/0.91 % (3060229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.42/0.91 % (3060229)CaDiCaL version: 2.1.3 % 4.42/0.91 % (3060229)Termination reason: Inappropriate % 4.42/0.91 % (3060229)Time elapsed: 0.005 s % 4.42/0.91 % (3060229)Peak memory usage: 11 MB % 4.42/0.91 % (3060229)Instructions burned: 10 (million) % 4.42/0.91 % (3060229)------------------------------ % 4.42/0.91 % (3060229)------------------------------ % 4.42/0.91 % (3060230)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3270380083:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 4.42/0.91 % (3060246)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=100272774:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 4.42/0.91 % (3060246)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.42/0.91 % (3060246)Terminated due to inappropriate strategy. % 4.42/0.91 % (3060246)------------------------------ % 4.42/0.91 % (3060246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.42/0.91 % (3060246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.42/0.91 % (3060246)CaDiCaL version: 2.1.3 % 4.42/0.91 % (3060246)Termination reason: Inappropriate % 4.42/0.91 % (3060246)Time elapsed: 0.005 s % 4.42/0.91 % (3060246)Peak memory usage: 11 MB % 4.42/0.91 % (3060246)Instructions burned: 9 (million) % 4.42/0.91 % (3060246)------------------------------ % 4.42/0.91 % (3060246)------------------------------ % 4.42/0.91 % (3060254)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2282602889:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 4.42/0.91 % (3060235)Instruction limit reached! % 4.42/0.91 % (3060235)------------------------------ % 4.42/0.91 % (3060235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.42/0.91 % (3060235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.42/0.91 % (3060235)CaDiCaL version: 2.1.3 % 4.42/0.91 % (3060235)Termination reason: Instruction limit % 4.42/0.91 % (3060235)Termination phase: Saturation % 4.42/0.91 % (3060235)Time elapsed: 0.061 s % 4.42/0.91 % (3060235)Peak memory usage: 14 MB % 4.42/0.91 % (3060235)Instructions burned: 162 (million) % 4.42/0.91 % (3060263)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=2433290791:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 4.42/0.91 % (3060232)Instruction limit reached! % 4.42/0.91 % (3060232)------------------------------ % 4.42/0.91 % (3060232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.42/0.91 % (3060232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.42/0.91 % (3060232)CaDiCaL version: 2.1.3 % 4.42/0.91 % (3060232)Termination reason: Instruction limit % 4.42/0.91 % (3060232)Termination phase: Saturation % 4.42/0.91 % (3060232)Time elapsed: 0.069 s % 4.42/0.91 % (3060232)Peak memory usage: 13 MB % 4.42/0.91 % (3060232)Instructions burned: 103 (million) % 4.42/0.91 % (3060233)Instruction limit reached! % 4.42/0.91 % (3060233)------------------------------ % 4.42/0.91 % (3060233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.32/1.33 % (3060233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.32/1.33 % (3060233)CaDiCaL version: 2.1.3 % 7.32/1.33 % (3060233)Termination reason: Instruction limit % 7.32/1.33 % (3060233)Termination phase: Saturation % 7.32/1.33 % (3060233)Time elapsed: 0.076 s % 7.32/1.33 % (3060233)Peak memory usage: 13 MB % 7.32/1.33 % (3060233)Instructions burned: 116 (million) % 7.32/1.33 % (3060234)Instruction limit reached! % 7.32/1.33 % (3060234)------------------------------ % 7.32/1.33 % (3060234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.32/1.33 % (3060234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.32/1.33 % (3060234)CaDiCaL version: 2.1.3 % 7.32/1.33 % (3060234)Termination reason: Instruction limit % 7.32/1.33 % (3060234)Termination phase: Saturation % 7.32/1.33 % (3060234)Time elapsed: 0.086 s % 7.32/1.33 % (3060234)Peak memory usage: 14 MB % 7.32/1.33 % (3060234)Instructions burned: 132 (million) % 7.32/1.33 % (3060268)ott-21_1_sil=16000:fs=off:random_seed=3700993575:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.32/1.33 % (3060269)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1187245562:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.32/1.33 % (3060270)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3018755052:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.32/1.33 % (3060270)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.32/1.33 % (3060270)Terminated due to inappropriate strategy. % 7.32/1.33 % (3060270)------------------------------ % 7.32/1.33 % (3060270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.32/1.33 % (3060270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.32/1.33 % (3060270)CaDiCaL version: 2.1.3 % 7.32/1.33 % (3060270)Termination reason: Inappropriate % 7.32/1.33 % (3060270)Time elapsed: 0.005 s % 7.32/1.33 % (3060270)Peak memory usage: 10 MB % 7.32/1.33 % (3060270)Instructions burned: 8 (million) % 7.32/1.33 % (3060270)------------------------------ % 7.32/1.33 % (3060270)------------------------------ % 7.32/1.33 % (3060277)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2693780629:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.32/1.33 % (3060254)Instruction limit reached! % 7.32/1.33 % (3060254)------------------------------ % 7.32/1.33 % (3060254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.32/1.33 % (3060254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.32/1.33 % (3060254)CaDiCaL version: 2.1.3 % 7.32/1.33 % (3060254)Termination reason: Instruction limit % 7.32/1.33 % (3060254)Termination phase: Saturation % 7.32/1.33 % (3060254)Time elapsed: 0.106 s % 7.32/1.33 % (3060254)Peak memory usage: 13 MB % 7.32/1.33 % (3060254)Instructions burned: 131 (million) % 7.32/1.33 % (3060292)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2051825783:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 7.32/1.33 % (3060292)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.32/1.33 % (3060292)Terminated due to inappropriate strategy. % 7.32/1.33 % (3060292)------------------------------ % 7.32/1.33 % (3060292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.32/1.33 % (3060292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.32/1.33 % (3060292)CaDiCaL version: 2.1.3 % 7.32/1.33 % (3060292)Termination reason: Inappropriate % 7.32/1.33 % (3060292)Time elapsed: 0.005 s % 7.32/1.33 % (3060292)Peak memory usage: 10 MB % 7.32/1.33 % (3060292)Instructions burned: 9 (million) % 7.32/1.33 % (3060292)------------------------------ % 7.32/1.33 % (3060292)------------------------------ % 7.32/1.33 % (3060268)Instruction limit reached! % 7.32/1.33 % (3060268)------------------------------ % 7.32/1.33 % (3060268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.32/1.33 % (3060268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.32/1.33 % (3060268)CaDiCaL version: 2.1.3 % 7.32/1.33 % (3060268)Termination reason: Instruction limit % 7.32/1.33 % (3060268)Termination phase: Saturation % 7.32/1.33 % (3060268)Time elapsed: 0.109 s % 7.32/1.33 % (3060268)Peak memory usage: 13 MB % 7.32/1.33 % (3060268)Instructions burned: 181 (million) % 7.32/1.33 % (3060298)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=1374893609: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) % 25.63/3.93 % (3060302)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=134929958:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 25.63/3.93 % (3060263)Instruction limit reached! % 25.63/3.93 % (3060263)------------------------------ % 25.63/3.93 % (3060263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.63/3.93 % (3060263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.63/3.93 % (3060263)CaDiCaL version: 2.1.3 % 25.63/3.93 % (3060263)Termination reason: Instruction limit % 25.63/3.93 % (3060263)Termination phase: Saturation % 25.63/3.93 % (3060263)Time elapsed: 0.249 s % 25.63/3.93 % (3060263)Peak memory usage: 13 MB % 25.63/3.93 % (3060263)Instructions burned: 685 (million) % 25.63/3.93 % (3060336)fmb+10_1_sil=64000:random_seed=3320169871:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 25.63/3.93 % (3060336)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.63/3.93 % (3060336)Terminated due to inappropriate strategy. % 25.63/3.93 % (3060336)------------------------------ % 25.63/3.93 % (3060336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.63/3.93 % (3060336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.63/3.93 % (3060336)CaDiCaL version: 2.1.3 % 25.63/3.93 % (3060336)Termination reason: Inappropriate % 25.63/3.93 % (3060336)Time elapsed: 0.009 s % 25.63/3.93 % (3060336)Peak memory usage: 10 MB % 25.63/3.93 % (3060336)Instructions burned: 9 (million) % 25.63/3.93 % (3060336)------------------------------ % 25.63/3.93 % (3060336)------------------------------ % 25.63/3.93 % (3060346)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3935533389:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 25.63/3.93 % (3060346)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.63/3.93 % (3060346)Terminated due to inappropriate strategy. % 25.63/3.93 % (3060346)------------------------------ % 25.63/3.93 % (3060346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.63/3.93 % (3060346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.63/3.93 % (3060346)CaDiCaL version: 2.1.3 % 25.63/3.93 % (3060346)Termination reason: Inappropriate % 25.63/3.93 % (3060346)Time elapsed: 0.006 s % 25.63/3.93 % (3060346)Peak memory usage: 11 MB % 25.63/3.93 % (3060346)Instructions burned: 9 (million) % 25.63/3.93 % (3060346)------------------------------ % 25.63/3.93 % (3060346)------------------------------ % 25.63/3.93 % (3060350)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2275920795:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 25.63/3.93 % (3060350)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.63/3.93 % (3060350)Terminated due to inappropriate strategy. % 25.63/3.93 % (3060350)------------------------------ % 25.63/3.93 % (3060350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.63/3.93 % (3060350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.63/3.93 % (3060350)CaDiCaL version: 2.1.3 % 25.63/3.93 % (3060350)Termination reason: Inappropriate % 25.63/3.93 % (3060350)Time elapsed: 0.014 s % 25.63/3.93 % (3060350)Peak memory usage: 10 MB % 25.63/3.93 % (3060350)Instructions burned: 9 (million) % 25.63/3.93 % (3060350)------------------------------ % 25.63/3.93 % (3060350)------------------------------ % 25.63/3.93 % (3060355)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1182606010:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 25.63/3.93 % (3060269)Instruction limit reached! % 25.63/3.93 % (3060269)------------------------------ % 25.63/3.93 % (3060269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.63/3.93 % (3060269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.63/3.93 % (3060269)CaDiCaL version: 2.1.3 % 25.63/3.93 % (3060269)Termination reason: Instruction limit % 25.63/3.93 % (3060269)Termination phase: Saturation % 25.63/3.93 % (3060269)Time elapsed: 0.424 s % 25.63/3.93 % (3060269)Peak memory usage: 14 MB % 25.63/3.93 % (3060269)Instructions burned: 477 (million) % 25.63/3.93 % (3060366)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3698372272:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 25.63/3.93 % (3060277)Instruction limit reached! % 25.63/3.93 % (3060277)------------------------------ % 30.11/4.68 % (3060277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.11/4.68 % (3060277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.11/4.68 % (3060277)CaDiCaL version: 2.1.3 % 30.11/4.68 % (3060277)Termination reason: Instruction limit % 30.11/4.68 % (3060277)Termination phase: Saturation % 30.11/4.68 % (3060277)Time elapsed: 0.506 s % 30.11/4.68 % (3060277)Peak memory usage: 23 MB % 30.11/4.68 % (3060277)Instructions burned: 1181 (million) % 30.11/4.68 % (3060371)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3413182505:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 30.11/4.68 % (3060371)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.11/4.68 % (3060371)Terminated due to inappropriate strategy. % 30.11/4.68 % (3060371)------------------------------ % 30.11/4.68 % (3060371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.11/4.68 % (3060371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.11/4.68 % (3060371)CaDiCaL version: 2.1.3 % 30.11/4.68 % (3060371)Termination reason: Inappropriate % 30.11/4.68 % (3060371)Time elapsed: 0.005 s % 30.11/4.68 % (3060371)Peak memory usage: 11 MB % 30.11/4.68 % (3060371)Instructions burned: 10 (million) % 30.11/4.68 % (3060371)------------------------------ % 30.11/4.68 % (3060371)------------------------------ % 30.11/4.68 % (3060374)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2053742543:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 30.11/4.68 % (3060374)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.11/4.68 % (3060374)Terminated due to inappropriate strategy. % 30.11/4.68 % (3060374)------------------------------ % 30.11/4.68 % (3060374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.11/4.68 % (3060374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.11/4.68 % (3060374)CaDiCaL version: 2.1.3 % 30.11/4.68 % (3060374)Termination reason: Inappropriate % 30.11/4.68 % (3060374)Time elapsed: 0.005 s % 30.11/4.68 % (3060374)Peak memory usage: 10 MB % 30.11/4.68 % (3060374)Instructions burned: 9 (million) % 30.11/4.68 % (3060374)------------------------------ % 30.11/4.68 % (3060374)------------------------------ % 30.11/4.68 % (3060377)ott-2_1_sil=16000:newcnf=on:random_seed=965729474:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 30.11/4.68 % (3060298)Instruction limit reached! % 30.11/4.68 % (3060298)------------------------------ % 30.11/4.68 % (3060298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.11/4.68 % (3060298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.11/4.68 % (3060298)CaDiCaL version: 2.1.3 % 30.11/4.68 % (3060298)Termination reason: Instruction limit % 30.11/4.68 % (3060298)Termination phase: Saturation % 30.11/4.68 % (3060298)Time elapsed: 0.651 s % 30.11/4.68 % (3060298)Peak memory usage: 18 MB % 30.11/4.68 % (3060298)Instructions burned: 692 (million) % 30.11/4.68 % (3060379)ott+10_1_sil=32000:tgt=ground:random_seed=3793422941:i=5114:av=off_2991 on theBenchmark for (2991ds/5114Mi) % 30.11/4.68 % (3060302)Instruction limit reached! % 30.11/4.68 % (3060302)------------------------------ % 30.11/4.68 % (3060302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.11/4.68 % (3060302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.11/4.68 % (3060302)CaDiCaL version: 2.1.3 % 30.11/4.68 % (3060302)Termination reason: Instruction limit % 30.11/4.68 % (3060302)Termination phase: Saturation % 30.11/4.68 % (3060302)Time elapsed: 0.799 s % 30.11/4.68 % (3060302)Peak memory usage: 19 MB % 30.11/4.68 % (3060302)Instructions burned: 879 (million) % 30.11/4.68 % (3060391)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=968115889:i=54282_2989 on theBenchmark for (2989ds/54282Mi) % 30.11/4.68 % (3060391)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.11/4.68 % (3060391)Terminated due to inappropriate strategy. % 30.11/4.68 % (3060391)------------------------------ % 30.11/4.68 % (3060391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.11/4.68 % (3060391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.11/4.68 % (3060391)CaDiCaL version: 2.1.3 % 30.11/4.68 % (3060391)Termination reason: Inappropriate % 30.11/4.68 % (3060391)Time elapsed: 0.007 s % 30.11/4.68 % (3060391)Peak memory usage: 11 MB % 30.11/4.68 % (3060391)Instructions burned: 10 (million) % 94.79/13.68 % (3060391)------------------------------ % 94.79/13.68 % (3060391)------------------------------ % 94.79/13.68 % (3060393)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2688835867:i=3512:aac=none_2989 on theBenchmark for (2989ds/3512Mi) % 94.79/13.68 % (3060377)Instruction limit reached! % 94.79/13.68 % (3060377)------------------------------ % 94.79/13.68 % (3060377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.79/13.68 % (3060377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.79/13.68 % (3060377)CaDiCaL version: 2.1.3 % 94.79/13.68 % (3060377)Termination reason: Instruction limit % 94.79/13.68 % (3060377)Termination phase: Saturation % 94.79/13.68 % (3060377)Time elapsed: 0.456 s % 94.79/13.68 % (3060377)Peak memory usage: 16 MB % 94.79/13.68 % (3060377)Instructions burned: 872 (million) % 94.79/13.68 % (3060395)dis+21_1_sil=32000:sas=cadical:random_seed=2036865328:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 94.79/13.68 % (3060366)Instruction limit reached! % 94.79/13.68 % (3060366)------------------------------ % 94.79/13.68 % (3060366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.79/13.68 % (3060366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.79/13.68 % (3060366)CaDiCaL version: 2.1.3 % 94.79/13.68 % (3060366)Termination reason: Instruction limit % 94.79/13.68 % (3060366)Termination phase: Saturation % 94.79/13.68 % (3060366)Time elapsed: 1.420 s % 94.79/13.68 % (3060366)Peak memory usage: 26 MB % 94.79/13.68 % (3060366)Instructions burned: 1472 (million) % 94.79/13.68 % (3060450)ott+11_1_sil=16000:gs=on:random_seed=2701358781:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2979 on theBenchmark for (2979ds/2251Mi) % 94.79/13.68 % (3060393)Instruction limit reached! % 94.79/13.68 % (3060393)------------------------------ % 94.79/13.68 % (3060393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.79/13.68 % (3060393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.79/13.68 % (3060393)CaDiCaL version: 2.1.3 % 94.79/13.68 % (3060393)Termination reason: Instruction limit % 94.79/13.68 % (3060393)Termination phase: Saturation % 94.79/13.68 % (3060393)Time elapsed: 1.403 s % 94.79/13.68 % (3060393)Peak memory usage: 36 MB % 94.79/13.68 % (3060393)Instructions burned: 3513 (million) % 94.79/13.68 % (3060556)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=719047602:fmbsr=1.6:i=67534_2974 on theBenchmark for (2974ds/67534Mi) % 94.79/13.68 % (3060556)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 94.79/13.68 % (3060556)Terminated due to inappropriate strategy. % 94.79/13.68 % (3060556)------------------------------ % 94.79/13.68 % (3060556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.79/13.68 % (3060556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.79/13.68 % (3060556)CaDiCaL version: 2.1.3 % 94.79/13.68 % (3060556)Termination reason: Inappropriate % 94.79/13.68 % (3060556)Time elapsed: 0.002 s % 94.79/13.68 % (3060556)Peak memory usage: 10 MB % 94.79/13.68 % (3060556)Instructions burned: 9 (million) % 94.79/13.68 % (3060556)------------------------------ % 94.79/13.68 % (3060556)------------------------------ % 94.79/13.68 % (3060560)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1765935550:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2974 on theBenchmark for (2974ds/4591Mi) % 94.79/13.68 % (3060450)Instruction limit reached! % 94.79/13.68 % (3060450)------------------------------ % 94.79/13.68 % (3060450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.79/13.68 % (3060450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.79/13.68 % (3060450)CaDiCaL version: 2.1.3 % 94.79/13.68 % (3060450)Termination reason: Instruction limit % 94.79/13.68 % (3060450)Termination phase: Saturation % 94.79/13.68 % (3060450)Time elapsed: 1.326 s % 94.79/13.68 % (3060450)Peak memory usage: 26 MB % 94.79/13.68 % (3060450)Instructions burned: 2253 (million) % 94.79/13.68 % (3060566)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=236318570:i=29340_2966 on theBenchmark for (2966ds/29340Mi) % 94.79/13.68 % (3060395)Instruction limit reached! % 94.79/13.68 % (3060395)------------------------------ % 94.79/13.68 % (3060395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.79/13.68 % (3060395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.79/13.68 % (3060395)CaDiCaL version: 2.1.3 % 94.79/13.68 % (3060395)Termination reason: Instruction limit % 147.65/21.09 % (3060395)Termination phase: Saturation % 147.65/21.09 % (3060395)Time elapsed: 2.446 s % 147.65/21.09 % (3060395)Peak memory usage: 41 MB % 147.65/21.09 % (3060395)Instructions burned: 3773 (million) % 147.65/21.09 % (3060568)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1279985144:i=5211_2962 on theBenchmark for (2962ds/5211Mi) % 147.65/21.09 % (3060560)Instruction limit reached! % 147.65/21.09 % (3060560)------------------------------ % 147.65/21.09 % (3060560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.65/21.09 % (3060560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.65/21.09 % (3060560)CaDiCaL version: 2.1.3 % 147.65/21.09 % (3060560)Termination reason: Instruction limit % 147.65/21.09 % (3060560)Termination phase: Saturation % 147.65/21.09 % (3060560)Time elapsed: 1.347 s % 147.65/21.09 % (3060560)Peak memory usage: 62 MB % 147.65/21.09 % (3060560)Instructions burned: 4594 (million) % 147.65/21.09 % (3060570)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3755106916:i=5497:nm=2_2960 on theBenchmark for (2960ds/5497Mi) % 147.65/21.09 % (3060570)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 147.65/21.09 % (3060570)Terminated due to inappropriate strategy. % 147.65/21.09 % (3060570)------------------------------ % 147.65/21.09 % (3060570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.65/21.09 % (3060570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.65/21.09 % (3060570)CaDiCaL version: 2.1.3 % 147.65/21.09 % (3060570)Termination reason: Inappropriate % 147.65/21.09 % (3060570)Time elapsed: 0.003 s % 147.65/21.09 % (3060570)Peak memory usage: 11 MB % 147.65/21.09 % (3060570)Instructions burned: 10 (million) % 147.65/21.09 % (3060570)------------------------------ % 147.65/21.09 % (3060570)------------------------------ % 147.65/21.09 % (3060572)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3080619718:fmbsr=2:i=46332_2960 on theBenchmark for (2960ds/46332Mi) % 147.65/21.09 % (3060572)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 147.65/21.09 % (3060572)Terminated due to inappropriate strategy. % 147.65/21.09 % (3060572)------------------------------ % 147.65/21.09 % (3060572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.65/21.09 % (3060572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.65/21.09 % (3060572)CaDiCaL version: 2.1.3 % 147.65/21.09 % (3060572)Termination reason: Inappropriate % 147.65/21.09 % (3060572)Time elapsed: 0.002 s % 147.65/21.09 % (3060572)Peak memory usage: 10 MB % 147.65/21.09 % (3060572)Instructions burned: 9 (million) % 147.65/21.09 % (3060572)------------------------------ % 147.65/21.09 % (3060572)------------------------------ % 147.65/21.09 % (3060574)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1627674929:i=14071_2960 on theBenchmark for (2960ds/14071Mi) % 147.65/21.09 % (3060574)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 147.65/21.09 % (3060574)Terminated due to inappropriate strategy. % 147.65/21.09 % (3060574)------------------------------ % 147.65/21.09 % (3060574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.65/21.09 % (3060574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.65/21.09 % (3060574)CaDiCaL version: 2.1.3 % 147.65/21.09 % (3060574)Termination reason: Inappropriate % 147.65/21.09 % (3060574)Time elapsed: 0.002 s % 147.65/21.09 % (3060574)Peak memory usage: 10 MB % 147.65/21.09 % (3060574)Instructions burned: 9 (million) % 147.65/21.09 % (3060574)------------------------------ % 147.65/21.09 % (3060574)------------------------------ % 147.65/21.09 % (3060576)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2987132201:i=22565:add=on:rawr=on_2960 on theBenchmark for (2960ds/22565Mi) % 147.65/21.09 % (3060355)Instruction limit reached! % 147.65/21.09 % (3060355)------------------------------ % 147.65/21.09 % (3060355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.65/21.09 % (3060355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.65/21.09 % (3060355)CaDiCaL version: 2.1.3 % 147.65/21.09 % (3060355)Termination reason: Instruction limit % 147.65/21.09 % (3060355)Termination phase: Saturation % 147.65/21.09 % (3060355)Time elapsed: 3.467 s % 147.65/21.09 % (3060355)Peak memory usage: 47 MB % 147.65/21.09 % (3060355)Instructions burned: 5132 (million) % 147.65/21.09 % (3060578)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3457230307:i=8173:av=off_2960 on theBenchmark for (2960ds/8173Mi) % 147.65/21.09 % (3060379)Instruction limit reached! % 136.76/21.15 % (3060379)------------------------------ % 136.76/21.15 % (3060379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.76/21.15 % (3060379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.76/21.15 % (3060379)CaDiCaL version: 2.1.3 % 136.76/21.15 % (3060379)Termination reason: Instruction limit % 136.76/21.15 % (3060379)Termination phase: Saturation % 136.76/21.15 % (3060379)Time elapsed: 3.517 s % 136.76/21.15 % (3060379)Peak memory usage: 49 MB % 136.76/21.15 % (3060379)Instructions burned: 5115 (million) % 136.76/21.15 % (3060580)dis+10_16:1_sil=16000:random_seed=3027015503:i=9155:fsr=off_2955 on theBenchmark for (2955ds/9155Mi) % 136.76/21.15 % (3060568)Instruction limit reached! % 136.76/21.15 % (3060568)------------------------------ % 136.76/21.15 % (3060568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.76/21.15 % (3060568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.76/21.15 % (3060568)CaDiCaL version: 2.1.3 % 136.76/21.15 % (3060568)Termination reason: Instruction limit % 136.76/21.15 % (3060568)Termination phase: Saturation % 136.76/21.15 % (3060568)Time elapsed: 2.695 s % 136.76/21.15 % (3060568)Peak memory usage: 44 MB % 136.76/21.15 % (3060568)Instructions burned: 5214 (million) % 136.76/21.15 % (3060582)ott-3_8_sil=64000:random_seed=1249322733:i=20139:bs=on_2935 on theBenchmark for (2935ds/20139Mi) % 136.76/21.15 % (3060576)Instruction limit reached! % 136.76/21.15 % (3060576)------------------------------ % 136.76/21.15 % (3060576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.76/21.15 % (3060576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.76/21.15 % (3060576)CaDiCaL version: 2.1.3 % 136.76/21.15 % (3060576)Termination reason: Instruction limit % 136.76/21.15 % (3060576)Termination phase: Saturation % 136.76/21.15 % (3060576)Time elapsed: 5.248 s % 136.76/21.15 % (3060576)Peak memory usage: 73 MB % 136.76/21.15 % (3060576)Instructions burned: 22566 (million) % 136.76/21.15 % (3060584)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1811884389:fmbsr=2:i=32576_2907 on theBenchmark for (2907ds/32576Mi) % 136.76/21.15 % (3060584)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.76/21.15 % (3060584)Terminated due to inappropriate strategy. % 136.76/21.15 % (3060584)------------------------------ % 136.76/21.15 % (3060584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.76/21.15 % (3060584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.76/21.15 % (3060584)CaDiCaL version: 2.1.3 % 136.76/21.15 % (3060584)Termination reason: Inappropriate % 136.76/21.15 % (3060584)Time elapsed: 0.003 s % 136.76/21.15 % (3060584)Peak memory usage: 11 MB % 136.76/21.15 % (3060584)Instructions burned: 10 (million) % 136.76/21.15 % (3060584)------------------------------ % 136.76/21.15 % (3060584)------------------------------ % 136.76/21.15 % (3060586)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2051107230:i=11404_2907 on theBenchmark for (2907ds/11404Mi) % 136.76/21.15 % (3060578)Instruction limit reached! % 136.76/21.15 % (3060578)------------------------------ % 136.76/21.15 % (3060578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.76/21.15 % (3060578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.76/21.15 % (3060578)CaDiCaL version: 2.1.3 % 136.76/21.15 % (3060578)Termination reason: Instruction limit % 136.76/21.15 % (3060578)Termination phase: Saturation % 136.76/21.15 % (3060578)Time elapsed: 5.259 s % 136.76/21.15 % (3060578)Peak memory usage: 86 MB % 136.76/21.15 % (3060578)Instructions burned: 8173 (million) % 136.76/21.15 % (3060588)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3452219210:i=14134_2907 on theBenchmark for (2907ds/14134Mi) % 136.76/21.15 % (3060580)Instruction limit reached! % 136.76/21.15 % (3060580)------------------------------ % 136.76/21.15 % (3060580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.76/21.15 % (3060580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.76/21.15 % (3060580)CaDiCaL version: 2.1.3 % 136.76/21.15 % (3060580)Termination reason: Instruction limit % 136.76/21.15 % (3060580)Termination phase: Saturation % 136.76/21.15 % (3060580)Time elapsed: 4.984 s % 136.76/21.15 % (3060580)Peak memory usage: 54 MB % 136.76/21.15 % (3060580)Instructions burned: 9156 (million) % 136.76/21.15 % (3060590)dis+33_16_sil=32000:sac=on:random_seed=1985258384:i=15851:nm=0_2905 on theBenchmark for (2905ds/15851Mi) % 136.76/21.15 % (3060586)Instruction limit reached! % 136.76/21.15 % (3060586)------------------------------ % 136.76/21.15 % (3060586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.92/22.91 % (3060586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.92/22.91 % (3060586)CaDiCaL version: 2.1.3 % 160.92/22.91 % (3060586)Termination reason: Instruction limit % 160.92/22.91 % (3060586)Termination phase: Saturation % 160.92/22.91 % (3060586)Time elapsed: 4.210 s % 160.92/22.91 % (3060586)Peak memory usage: 94 MB % 160.92/22.91 % (3060586)Instructions burned: 11405 (million) % 160.92/22.91 % (3060593)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=252911879:avsq=on:i=17627:add=on:amm=off_2865 on theBenchmark for (2865ds/17627Mi) % 160.92/22.91 % (3060566)Instruction limit reached! % 160.92/22.91 % (3060566)------------------------------ % 160.92/22.91 % (3060566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.92/22.91 % (3060566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.92/22.91 % (3060566)CaDiCaL version: 2.1.3 % 160.92/22.91 % (3060566)Termination reason: Instruction limit % 160.92/22.91 % (3060566)Termination phase: Saturation % 160.92/22.91 % (3060566)Time elapsed: 15.857 s % 160.92/22.91 % (3060566)Peak memory usage: 285 MB % 160.92/22.91 % (3060566)Instructions burned: 29340 (million) % 160.92/22.91 % (3060904)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1558208695:s2a=on:i=53295_2806 on theBenchmark for (2806ds/53295Mi) % 160.92/22.91 % (3060588)Instruction limit reached! % 160.92/22.91 % (3060588)------------------------------ % 160.92/22.91 % (3060588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.92/22.91 % (3060588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.92/22.91 % (3060588)CaDiCaL version: 2.1.3 % 160.92/22.91 % (3060588)Termination reason: Instruction limit % 160.92/22.91 % (3060588)Termination phase: Saturation % 160.92/22.91 % (3060588)Time elapsed: 11.030 s % 160.92/22.91 % (3060588)Peak memory usage: 91 MB % 160.92/22.91 % (3060588)Instructions burned: 14134 (million) % 160.92/22.91 % (3061061)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=326602983:i=26857:ins=20_2796 on theBenchmark for (2796ds/26857Mi) % 160.92/22.91 % (3061061)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.92/22.91 % (3061061)Terminated due to inappropriate strategy. % 160.92/22.91 % (3061061)------------------------------ % 160.92/22.91 % (3061061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.92/22.91 % (3061061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.92/22.91 % (3061061)CaDiCaL version: 2.1.3 % 160.92/22.91 % (3061061)Termination reason: Inappropriate % 160.92/22.91 % (3061061)Time elapsed: 0.005 s % 160.92/22.91 % (3061061)Peak memory usage: 10 MB % 160.92/22.91 % (3061061)Instructions burned: 9 (million) % 160.92/22.91 % (3061061)------------------------------ % 160.92/22.91 % (3061061)------------------------------ % 160.92/22.91 % (3061063)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4136128690:i=28120:bs=on:fsr=off_2796 on theBenchmark for (2796ds/28120Mi) % 160.92/22.91 % (3060593)Instruction limit reached! % 160.92/22.91 % (3060593)------------------------------ % 160.92/22.91 % (3060593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.92/22.91 % (3060593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.92/22.91 % (3060593)CaDiCaL version: 2.1.3 % 160.92/22.91 % (3060593)Termination reason: Instruction limit % 160.92/22.91 % (3060593)Termination phase: Saturation % 160.92/22.91 % (3060593)Time elapsed: 7.335 s % 160.92/22.91 % (3060593)Peak memory usage: 331 MB % 160.92/22.91 % (3060593)Instructions burned: 17627 (million) % 160.92/22.91 % (3061065)fmb+10_1_sil=256000:fmbss=7:random_seed=2662466488:fmbsr=1.6:i=182295_2791 on theBenchmark for (2791ds/182295Mi) % 160.92/22.91 % (3061065)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.92/22.91 % (3061065)Terminated due to inappropriate strategy. % 160.92/22.91 % (3061065)------------------------------ % 160.92/22.91 % (3061065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.92/22.91 % (3061065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.92/22.91 % (3061065)CaDiCaL version: 2.1.3 % 160.92/22.91 % (3061065)Termination reason: Inappropriate % 160.92/22.91 % (3061065)Time elapsed: 0.002 s % 160.92/22.91 % (3061065)Peak memory usage: 10 MB % 160.92/22.91 % (3061065)Instructions burned: 9 (million) % 160.92/22.91 % (3061065)------------------------------ % 160.92/22.91 % (3061065)------------------------------ % 160.92/22.91 % (3061067)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1404541941:i=44625:gsp=on_2791 on theBenchmark for (2791ds/44625Mi) % 173.75/24.84 % (3061067)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.75/24.84 % (3061067)Terminated due to inappropriate strategy. % 173.75/24.84 % (3061067)------------------------------ % 173.75/24.84 % (3061067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.75/24.84 % (3061067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.75/24.84 % (3061067)CaDiCaL version: 2.1.3 % 173.75/24.84 % (3061067)Termination reason: Inappropriate % 173.75/24.84 % (3061067)Time elapsed: 0.003 s % 173.75/24.84 % (3061067)Peak memory usage: 11 MB % 173.75/24.84 % (3061067)Instructions burned: 9 (million) % 173.75/24.84 % (3061067)------------------------------ % 173.75/24.84 % (3061067)------------------------------ % 173.75/24.84 % (3061069)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=673357582:i=160505_2791 on theBenchmark for (2791ds/160505Mi) % 173.75/24.84 % (3061069)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.75/24.84 % (3061069)Terminated due to inappropriate strategy. % 173.75/24.84 % (3061069)------------------------------ % 173.75/24.84 % (3061069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.75/24.84 % (3061069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.75/24.84 % (3061069)CaDiCaL version: 2.1.3 % 173.75/24.84 % (3061069)Termination reason: Inappropriate % 173.75/24.84 % (3061069)Time elapsed: 0.002 s % 173.75/24.84 % (3061069)Peak memory usage: 10 MB % 173.75/24.84 % (3061069)Instructions burned: 9 (million) % 173.75/24.84 % (3061069)------------------------------ % 173.75/24.84 % (3061069)------------------------------ % 173.75/24.84 % (3061071)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=52439197:fmbsr=1.3:i=225729_2791 on theBenchmark for (2791ds/225729Mi) % 173.75/24.84 % (3061071)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.75/24.84 % (3061071)Terminated due to inappropriate strategy. % 173.75/24.84 % (3061071)------------------------------ % 173.75/24.84 % (3061071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.75/24.84 % (3061071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.75/24.84 % (3061071)CaDiCaL version: 2.1.3 % 173.75/24.84 % (3061071)Termination reason: Inappropriate % 173.75/24.84 % (3061071)Time elapsed: 0.003 s % 173.75/24.84 % (3061071)Peak memory usage: 10 MB % 173.75/24.84 % (3061071)Instructions burned: 9 (million) % 173.75/24.84 % (3061071)------------------------------ % 173.75/24.84 % (3061071)------------------------------ % 173.75/24.84 % (3060590)Instruction limit reached! % 173.75/24.84 % (3060590)------------------------------ % 173.75/24.84 % (3060590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.75/24.84 % (3060590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.75/24.84 % (3060590)CaDiCaL version: 2.1.3 % 173.75/24.84 % (3060590)Termination reason: Instruction limit % 173.75/24.84 % (3060590)Termination phase: Saturation % 173.75/24.84 % (3060590)Time elapsed: 11.415 s % 173.75/24.84 % (3060590)Peak memory usage: 162 MB % 173.75/24.84 % (3060590)Instructions burned: 15852 (million) % 173.75/24.84 % (3061073)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=873972482:fmbsr=2:i=185024:ins=7_2791 on theBenchmark for (2791ds/185024Mi) % 173.75/24.84 % (3061073)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.75/24.84 % (3061073)Terminated due to inappropriate strategy. % 173.75/24.84 % (3061073)------------------------------ % 173.75/24.84 % (3061073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.75/24.84 % (3061073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.75/24.84 % (3061073)CaDiCaL version: 2.1.3 % 173.75/24.84 % (3061073)Termination reason: Inappropriate % 173.75/24.84 % (3061073)Time elapsed: 0.002 s % 173.75/24.84 % (3061073)Peak memory usage: 10 MB % 173.75/24.84 % (3061073)Instructions burned: 9 (million) % 173.75/24.84 % (3061073)------------------------------ % 173.75/24.84 % (3061073)------------------------------ % 173.75/24.84 % (3061075)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3703702180:rtra=on_2790 on theBenchmark for (2790ds/0Mi) % 173.75/24.84 % (3061075)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.75/24.84 % (3061075)Terminated due to inappropriate strategy. % 173.75/24.84 % (3061075)------------------------------ % 173.75/24.84 % (3061075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.75/24.84 % (3061075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.95/28.46 % (3061075)CaDiCaL version: 2.1.3 % 199.95/28.46 % (3061075)Termination reason: Inappropriate % 199.95/28.46 % (3061075)Time elapsed: 0.003 s % 199.95/28.46 % (3061075)Peak memory usage: 11 MB % 199.95/28.46 % (3061075)Instructions burned: 11 (million) % 199.95/28.46 % (3061075)------------------------------ % 199.95/28.46 % (3061075)------------------------------ % 199.95/28.46 % (3061078)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3570204061:i=176048:add=on:rtra=on:rawr=on_2790 on theBenchmark for (2790ds/176048Mi) % 199.95/28.46 % (3061077)% WARNING: option uhcvi not known. % 199.95/28.46 % (3061077)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3172900422:i=271062:add=off:rtra=on:rawr=on_2790 on theBenchmark for (2790ds/271062Mi) % 199.95/28.46 % (3060582)Instruction limit reached! % 199.95/28.46 % (3060582)------------------------------ % 199.95/28.46 % (3060582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.95/28.46 % (3060582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.95/28.46 % (3060582)CaDiCaL version: 2.1.3 % 199.95/28.46 % (3060582)Termination reason: Instruction limit % 199.95/28.46 % (3060582)Termination phase: Saturation % 199.95/28.46 % (3060582)Time elapsed: 15.408 s % 199.95/28.46 % (3060582)Peak memory usage: 131 MB % 199.95/28.46 % (3060582)Instructions burned: 20140 (million) % 199.95/28.46 % (3061081)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3455300934:i=206:fgj=on:rtra=on_2781 on theBenchmark for (2781ds/206Mi) % 199.95/28.46 % (3061081)Instruction limit reached! % 199.95/28.46 % (3061081)------------------------------ % 199.95/28.46 % (3061081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.95/28.46 % (3061081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.95/28.46 % (3061081)CaDiCaL version: 2.1.3 % 199.95/28.46 % (3061081)Termination reason: Instruction limit % 199.95/28.46 % (3061081)Termination phase: Saturation % 199.95/28.46 % (3061081)Time elapsed: 0.138 s % 199.95/28.46 % (3061081)Peak memory usage: 14 MB % 199.95/28.46 % (3061081)Instructions burned: 206 (million) % 199.95/28.46 % (3061083)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=300756203:i=232:rtra=on_2779 on theBenchmark for (2779ds/232Mi) % 199.95/28.46 % (3061083)Instruction limit reached! % 199.95/28.46 % (3061083)------------------------------ % 199.95/28.46 % (3061083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.95/28.46 % (3061083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.95/28.46 % (3061083)CaDiCaL version: 2.1.3 % 199.95/28.46 % (3061083)Termination reason: Instruction limit % 199.95/28.46 % (3061083)Termination phase: Saturation % 199.95/28.46 % (3061083)Time elapsed: 0.160 s % 199.95/28.46 % (3061083)Peak memory usage: 14 MB % 199.95/28.46 % (3061083)Instructions burned: 233 (million) % 199.95/28.46 % (3061085)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2670058025:i=262:rtra=on_2777 on theBenchmark for (2777ds/262Mi) % 199.95/28.46 % (3061085)Instruction limit reached! % 199.95/28.46 % (3061085)------------------------------ % 199.95/28.46 % (3061085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.95/28.46 % (3061085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.95/28.46 % (3061085)CaDiCaL version: 2.1.3 % 199.95/28.46 % (3061085)Termination reason: Instruction limit % 199.95/28.46 % (3061085)Termination phase: Saturation % 199.95/28.46 % (3061085)Time elapsed: 0.180 s % 199.95/28.46 % (3061085)Peak memory usage: 14 MB % 199.95/28.46 % (3061085)Instructions burned: 263 (million) % 199.95/28.46 % (3061087)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3969864403:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2775 on theBenchmark for (2775ds/318Mi) % 199.95/28.46 % (3061087)Instruction limit reached! % 199.95/28.46 % (3061087)------------------------------ % 199.95/28.46 % (3061087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.95/28.46 % (3061087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.95/28.46 % (3061087)CaDiCaL version: 2.1.3 % 199.95/28.46 % (3061087)Termination reason: Instruction limit % 199.95/28.46 % (3061087)Termination phase: Saturation % 199.95/28.46 % (3061087)Time elapsed: 0.229 s % 199.95/28.46 % (3061087)Peak memory usage: 16 MB % 199.95/28.46 % (3061087)Instructions burned: 318 (million) % 199.95/28.46 % (3061089)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3176519256:i=1428:nm=2:rtra=on_2773 on theBenchmark for (2773ds/1428Mi) % 261.63/39.88 % (3061089)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 261.63/39.88 % (3061089)Terminated due to inappropriate strategy. % 261.63/39.88 % (3061089)------------------------------ % 261.63/39.88 % (3061089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.63/39.88 % (3061089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.63/39.88 % (3061089)CaDiCaL version: 2.1.3 % 261.63/39.88 % (3061089)Termination reason: Inappropriate % 261.63/39.88 % (3061089)Time elapsed: 0.006 s % 261.63/39.88 % (3061089)Peak memory usage: 10 MB % 261.63/39.88 % (3061089)Instructions burned: 10 (million) % 261.63/39.88 % (3061089)------------------------------ % 261.63/39.88 % (3061089)------------------------------ % 261.63/39.88 % (3061091)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1223616135:i=262:bd=preordered:rtra=on:fsd=on_2773 on theBenchmark for (2773ds/262Mi) % 261.63/39.88 % (3061091)Instruction limit reached! % 261.63/39.88 % (3061091)------------------------------ % 261.63/39.88 % (3061091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.63/39.88 % (3061091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.63/39.88 % (3061091)CaDiCaL version: 2.1.3 % 261.63/39.88 % (3061091)Termination reason: Instruction limit % 261.63/39.88 % (3061091)Termination phase: Saturation % 261.63/39.88 % (3061091)Time elapsed: 0.165 s % 261.63/39.88 % (3061091)Peak memory usage: 14 MB % 261.63/39.88 % (3061091)Instructions burned: 263 (million) % 261.63/39.88 % (3061093)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=4274579208:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2771 on theBenchmark for (2771ds/1368Mi) % 261.63/39.88 % (3061093)Instruction limit reached! % 261.63/39.88 % (3061093)------------------------------ % 261.63/39.88 % (3061093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.63/39.88 % (3061093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.63/39.88 % (3061093)CaDiCaL version: 2.1.3 % 261.63/39.88 % (3061093)Termination reason: Instruction limit % 261.63/39.88 % (3061093)Termination phase: Saturation % 261.63/39.88 % (3061093)Time elapsed: 0.781 s % 261.63/39.88 % (3061093)Peak memory usage: 23 MB % 261.63/39.88 % (3061093)Instructions burned: 1368 (million) % 261.63/39.88 % (3061095)ott-21_1_sil=16000:si=on:fs=off:random_seed=2460879771:i=360:av=off:fsr=off:rtra=on_2763 on theBenchmark for (2763ds/360Mi) % 261.63/39.88 % (3061095)Instruction limit reached! % 261.63/39.88 % (3061095)------------------------------ % 261.63/39.88 % (3061095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.63/39.88 % (3061095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.63/39.88 % (3061095)CaDiCaL version: 2.1.3 % 261.63/39.88 % (3061095)Termination reason: Instruction limit % 261.63/39.88 % (3061095)Termination phase: Saturation % 261.63/39.88 % (3061095)Time elapsed: 0.184 s % 261.63/39.88 % (3061095)Peak memory usage: 14 MB % 261.63/39.88 % (3061095)Instructions burned: 360 (million) % 261.63/39.88 % (3061097)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1110157102:i=954:bd=all:rtra=on_2761 on theBenchmark for (2761ds/954Mi) % 261.63/39.88 % (3061097)Instruction limit reached! % 261.63/39.88 % (3061097)------------------------------ % 261.63/39.88 % (3061097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.63/39.88 % (3061097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.63/39.88 % (3061097)CaDiCaL version: 2.1.3 % 261.63/39.88 % (3061097)Termination reason: Instruction limit % 261.63/39.88 % (3061097)Termination phase: Saturation % 261.63/39.88 % (3061097)Time elapsed: 0.676 s % 261.63/39.88 % (3061097)Peak memory usage: 16 MB % 261.63/39.88 % (3061097)Instructions burned: 955 (million) % 261.63/39.88 % (3061099)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2806866036:fmbsr=1.3:i=1730:ins=25:rtra=on_2754 on theBenchmark for (2754ds/1730Mi) % 261.63/39.88 % (3061099)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 261.63/39.88 % (3061099)Terminated due to inappropriate strategy. % 261.63/39.88 % (3061099)------------------------------ % 261.63/39.88 % (3061099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.63/39.88 % (3061099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.63/39.88 % (3061099)CaDiCaL version: 2.1.3 % 261.63/39.88 % (3061099)Termination reason: InapproprTerminated % 300.17/42.54 % Vampire exiting % 300.17/42.54 Terminated %------------------------------------------------------------------------------