%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW596_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 : n001.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:30 PM UTC 2026 % Result : Timeout 300.35s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW596_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.18 % Computer : n001.cluster.edu % 0.09/0.18 % Model : x86_64 x86_64 % 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.18 % Memory : 8046.5625MB % 0.09/0.18 % OS : Linux 6.8.0-71-generic % 0.09/0.18 % CPULimit : 300 % 0.09/0.18 % WCLimit : 300 % 0.09/0.18 % DateTime : Mon Sep 28 14:27:03 UTC 2026 % 0.09/0.18 % CPUTime : % 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.21 Running first-order model finding % 0.09/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.33/0.71 % (379694)Will run a generic schedule for satisfiability detection. % 3.33/0.71 % (379699)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3414157378_2999 on theBenchmark for (2999ds/0Mi) % 3.33/0.71 % (379699)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.33/0.71 % (379699)Terminated due to inappropriate strategy. % 3.33/0.71 % (379699)------------------------------ % 3.33/0.71 % (379699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.33/0.71 % (379699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.33/0.71 % (379699)CaDiCaL version: 2.1.3 % 3.33/0.71 % (379699)Termination reason: Inappropriate % 3.33/0.71 % (379699)Time elapsed: 0.001 s % 3.33/0.71 % (379699)Peak memory usage: 11 MB % 3.33/0.71 % (379699)Instructions burned: 4 (million) % 3.33/0.71 % (379700)% WARNING: option uhcvi not known. % 3.33/0.71 % (379699)------------------------------ % 3.33/0.71 % (379699)------------------------------ % 3.33/0.71 % (379702)dis+10_1_sil=32000:sp=arity:random_seed=864310251:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.33/0.71 % (379701)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2227361890:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.33/0.71 % (379700)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=851761355:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.33/0.71 % (379703)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1909368666:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.33/0.71 % (379704)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1521510366:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.33/0.71 % (379705)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1123003560:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.33/0.71 % (379707)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1776966696:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.33/0.71 % (379707)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.33/0.71 % (379707)Terminated due to inappropriate strategy. % 3.33/0.71 % (379707)------------------------------ % 3.33/0.71 % (379707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.33/0.71 % (379707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.33/0.71 % (379707)CaDiCaL version: 2.1.3 % 3.33/0.71 % (379707)Termination reason: Inappropriate % 3.33/0.71 % (379707)Time elapsed: 0.001 s % 3.33/0.71 % (379707)Peak memory usage: 11 MB % 3.33/0.71 % (379707)Instructions burned: 4 (million) % 3.33/0.71 % (379707)------------------------------ % 3.33/0.71 % (379707)------------------------------ % 3.33/0.71 % (379715)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=298684089:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.33/0.71 % (379702)Instruction limit reached! % 3.33/0.71 % (379702)------------------------------ % 3.33/0.71 % (379702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.33/0.71 % (379702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.33/0.71 % (379702)CaDiCaL version: 2.1.3 % 3.33/0.71 % (379702)Termination reason: Instruction limit % 3.33/0.71 % (379702)Termination phase: Saturation % 3.33/0.71 % (379702)Time elapsed: 0.059 s % 3.33/0.71 % (379702)Peak memory usage: 12 MB % 3.33/0.71 % (379702)Instructions burned: 104 (million) % 3.33/0.71 % (379715)Instruction limit reached! % 3.33/0.71 % (379715)------------------------------ % 3.33/0.71 % (379715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.33/0.71 % (379715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.33/0.71 % (379715)CaDiCaL version: 2.1.3 % 3.33/0.71 % (379715)Termination reason: Instruction limit % 3.33/0.71 % (379715)Termination phase: Saturation % 3.33/0.71 % (379715)Time elapsed: 0.045 s % 3.33/0.71 % (379715)Peak memory usage: 13 MB % 3.33/0.71 % (379715)Instructions burned: 133 (million) % 3.33/0.71 % (379703)Instruction limit reached! % 3.33/0.71 % (379703)------------------------------ % 3.33/0.71 % (379703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.33/0.71 % (379703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.33/0.71 % (379703)CaDiCaL version: 2.1.3 % 3.33/0.71 % (379703)Termination reason: Instruction limit % 3.33/0.71 % (379703)Termination phase: Saturation % 6.89/1.26 % (379703)Time elapsed: 0.068 s % 6.89/1.26 % (379703)Peak memory usage: 13 MB % 6.89/1.26 % (379703)Instructions burned: 117 (million) % 6.89/1.26 % (379718)ott-21_1_sil=16000:fs=off:random_seed=408100007:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 6.89/1.26 % (379704)Instruction limit reached! % 6.89/1.26 % (379704)------------------------------ % 6.89/1.26 % (379704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.89/1.26 % (379704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.89/1.26 % (379704)CaDiCaL version: 2.1.3 % 6.89/1.26 % (379704)Termination reason: Instruction limit % 6.89/1.26 % (379704)Termination phase: Saturation % 6.89/1.26 % (379704)Time elapsed: 0.076 s % 6.89/1.26 % (379704)Peak memory usage: 13 MB % 6.89/1.26 % (379704)Instructions burned: 131 (million) % 6.89/1.26 % (379717)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=2690009537:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 6.89/1.26 % (379719)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3635074486:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 6.89/1.26 % (379721)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=680080581:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.89/1.26 % (379721)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.89/1.26 % (379721)Terminated due to inappropriate strategy. % 6.89/1.26 % (379721)------------------------------ % 6.89/1.26 % (379721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.89/1.26 % (379721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.89/1.26 % (379721)CaDiCaL version: 2.1.3 % 6.89/1.26 % (379721)Termination reason: Inappropriate % 6.89/1.26 % (379721)Time elapsed: 0.002 s % 6.89/1.26 % (379721)Peak memory usage: 10 MB % 6.89/1.26 % (379721)Instructions burned: 3 (million) % 6.89/1.26 % (379721)------------------------------ % 6.89/1.26 % (379721)------------------------------ % 6.89/1.26 % (379705)Instruction limit reached! % 6.89/1.26 % (379705)------------------------------ % 6.89/1.26 % (379705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.89/1.26 % (379705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.89/1.26 % (379705)CaDiCaL version: 2.1.3 % 6.89/1.26 % (379705)Termination reason: Instruction limit % 6.89/1.26 % (379705)Termination phase: Saturation % 6.89/1.26 % (379705)Time elapsed: 0.107 s % 6.89/1.26 % (379705)Peak memory usage: 14 MB % 6.89/1.26 % (379705)Instructions burned: 160 (million) % 6.89/1.26 % (379725)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=126173332:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.89/1.26 % (379718)Instruction limit reached! % 6.89/1.26 % (379718)------------------------------ % 6.89/1.26 % (379718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.89/1.26 % (379718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.89/1.26 % (379718)CaDiCaL version: 2.1.3 % 6.89/1.26 % (379718)Termination reason: Instruction limit % 6.89/1.26 % (379718)Termination phase: Saturation % 6.89/1.26 % (379718)Time elapsed: 0.050 s % 6.89/1.26 % (379718)Peak memory usage: 12 MB % 6.89/1.26 % (379718)Instructions burned: 183 (million) % 6.89/1.26 % (379726)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2879226588:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.89/1.26 % (379726)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.89/1.26 % (379726)Terminated due to inappropriate strategy. % 6.89/1.26 % (379726)------------------------------ % 6.89/1.26 % (379726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.89/1.26 % (379726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.89/1.26 % (379726)CaDiCaL version: 2.1.3 % 6.89/1.26 % (379726)Termination reason: Inappropriate % 6.89/1.26 % (379726)Time elapsed: 0.002 s % 6.89/1.26 % (379726)Peak memory usage: 10 MB % 6.89/1.26 % (379726)Instructions burned: 4 (million) % 6.89/1.26 % (379726)------------------------------ % 6.89/1.26 % (379726)------------------------------ % 6.89/1.26 % (379728)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=1638601238:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 21.19/3.25 % (379730)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1164076453:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 21.19/3.25 % (379728)Instruction limit reached! % 21.19/3.25 % (379728)------------------------------ % 21.19/3.25 % (379728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.19/3.25 % (379728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.19/3.25 % (379728)CaDiCaL version: 2.1.3 % 21.19/3.25 % (379728)Termination reason: Instruction limit % 21.19/3.25 % (379728)Termination phase: Saturation % 21.19/3.25 % (379728)Time elapsed: 0.182 s % 21.19/3.25 % (379728)Peak memory usage: 16 MB % 21.19/3.25 % (379728)Instructions burned: 695 (million) % 21.19/3.25 % (379733)fmb+10_1_sil=64000:random_seed=1794310751:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 21.19/3.25 % (379733)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.19/3.25 % (379733)Terminated due to inappropriate strategy. % 21.19/3.25 % (379733)------------------------------ % 21.19/3.25 % (379733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.19/3.25 % (379733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.19/3.25 % (379733)CaDiCaL version: 2.1.3 % 21.19/3.25 % (379733)Termination reason: Inappropriate % 21.19/3.25 % (379733)Time elapsed: 0.001 s % 21.19/3.25 % (379733)Peak memory usage: 11 MB % 21.19/3.25 % (379733)Instructions burned: 4 (million) % 21.19/3.25 % (379733)------------------------------ % 21.19/3.25 % (379733)------------------------------ % 21.19/3.25 % (379735)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3068139017:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 21.19/3.25 % (379735)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.19/3.25 % (379735)Terminated due to inappropriate strategy. % 21.19/3.25 % (379735)------------------------------ % 21.19/3.25 % (379735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.19/3.25 % (379735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.19/3.25 % (379735)CaDiCaL version: 2.1.3 % 21.19/3.25 % (379735)Termination reason: Inappropriate % 21.19/3.25 % (379735)Time elapsed: 0.002 s % 21.19/3.25 % (379735)Peak memory usage: 10 MB % 21.19/3.25 % (379735)Instructions burned: 4 (million) % 21.19/3.25 % (379735)------------------------------ % 21.19/3.25 % (379735)------------------------------ % 21.19/3.25 % (379737)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=578836002:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 21.19/3.25 % (379737)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.19/3.25 % (379737)Terminated due to inappropriate strategy. % 21.19/3.25 % (379737)------------------------------ % 21.19/3.25 % (379737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.19/3.25 % (379737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.19/3.25 % (379737)CaDiCaL version: 2.1.3 % 21.19/3.25 % (379737)Termination reason: Inappropriate % 21.19/3.25 % (379737)Time elapsed: 0.002 s % 21.19/3.25 % (379737)Peak memory usage: 10 MB % 21.19/3.25 % (379737)Instructions burned: 4 (million) % 21.19/3.25 % (379737)------------------------------ % 21.19/3.25 % (379737)------------------------------ % 21.19/3.25 % (379739)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3612999730:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 21.19/3.25 % (379719)Instruction limit reached! % 21.19/3.25 % (379719)------------------------------ % 21.19/3.25 % (379719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.19/3.25 % (379719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.19/3.25 % (379719)CaDiCaL version: 2.1.3 % 21.19/3.25 % (379719)Termination reason: Instruction limit % 21.19/3.25 % (379719)Termination phase: Saturation % 21.19/3.25 % (379719)Time elapsed: 0.306 s % 21.19/3.25 % (379719)Peak memory usage: 14 MB % 21.19/3.25 % (379719)Instructions burned: 478 (million) % 21.19/3.25 % (379741)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=659441635:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 21.19/3.25 % (379717)Instruction limit reached! % 21.19/3.25 % (379717)------------------------------ % 21.19/3.25 % (379717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.19/3.25 % (379717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.03/3.92 % (379717)CaDiCaL version: 2.1.3 % 25.03/3.92 % (379717)Termination reason: Instruction limit % 25.03/3.92 % (379717)Termination phase: Saturation % 25.03/3.92 % (379717)Time elapsed: 0.383 s % 25.03/3.92 % (379717)Peak memory usage: 17 MB % 25.03/3.92 % (379717)Instructions burned: 685 (million) % 25.03/3.92 % (379743)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4162984436:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 25.03/3.92 % (379743)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.03/3.92 % (379743)Terminated due to inappropriate strategy. % 25.03/3.92 % (379743)------------------------------ % 25.03/3.92 % (379743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.03/3.92 % (379743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.03/3.92 % (379743)CaDiCaL version: 2.1.3 % 25.03/3.92 % (379743)Termination reason: Inappropriate % 25.03/3.92 % (379743)Time elapsed: 0.002 s % 25.03/3.92 % (379743)Peak memory usage: 11 MB % 25.03/3.92 % (379743)Instructions burned: 4 (million) % 25.03/3.92 % (379743)------------------------------ % 25.03/3.92 % (379743)------------------------------ % 25.03/3.92 % (379745)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3199195427:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 25.03/3.92 % (379745)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.03/3.92 % (379745)Terminated due to inappropriate strategy. % 25.03/3.92 % (379745)------------------------------ % 25.03/3.92 % (379745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.03/3.92 % (379745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.03/3.92 % (379745)CaDiCaL version: 2.1.3 % 25.03/3.92 % (379745)Termination reason: Inappropriate % 25.03/3.92 % (379745)Time elapsed: 0.002 s % 25.03/3.92 % (379745)Peak memory usage: 10 MB % 25.03/3.92 % (379745)Instructions burned: 4 (million) % 25.03/3.92 % (379745)------------------------------ % 25.03/3.92 % (379745)------------------------------ % 25.03/3.92 % (379747)ott-2_1_sil=16000:newcnf=on:random_seed=2904217867:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 25.03/3.92 % (379730)Instruction limit reached! % 25.03/3.92 % (379730)------------------------------ % 25.03/3.92 % (379730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.03/3.92 % (379730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.03/3.92 % (379730)CaDiCaL version: 2.1.3 % 25.03/3.92 % (379730)Termination reason: Instruction limit % 25.03/3.92 % (379730)Termination phase: Saturation % 25.03/3.92 % (379730)Time elapsed: 0.502 s % 25.03/3.92 % (379730)Peak memory usage: 20 MB % 25.03/3.92 % (379730)Instructions burned: 880 (million) % 25.03/3.92 % (379749)ott+10_1_sil=32000:tgt=ground:random_seed=4020912826:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 25.03/3.92 % (379725)Instruction limit reached! % 25.03/3.92 % (379725)------------------------------ % 25.03/3.92 % (379725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.03/3.92 % (379725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.03/3.92 % (379725)CaDiCaL version: 2.1.3 % 25.03/3.92 % (379725)Termination reason: Instruction limit % 25.03/3.92 % (379725)Termination phase: Saturation % 25.03/3.92 % (379725)Time elapsed: 0.690 s % 25.03/3.92 % (379725)Peak memory usage: 20 MB % 25.03/3.92 % (379725)Instructions burned: 1180 (million) % 25.03/3.92 % (379751)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=125689444:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 25.03/3.92 % (379751)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.03/3.92 % (379751)Terminated due to inappropriate strategy. % 25.03/3.92 % (379751)------------------------------ % 25.03/3.92 % (379751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.03/3.92 % (379751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.03/3.92 % (379751)CaDiCaL version: 2.1.3 % 25.03/3.92 % (379751)Termination reason: Inappropriate % 25.03/3.92 % (379751)Time elapsed: 0.002 s % 25.03/3.92 % (379751)Peak memory usage: 11 MB % 25.03/3.92 % (379751)Instructions burned: 4 (million) % 25.03/3.92 % (379751)------------------------------ % 25.03/3.92 % (379751)------------------------------ % 25.03/3.92 % (379753)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3304784853:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 25.03/3.92 % (379747)Instruction limit reached! % 89.32/12.86 % (379747)------------------------------ % 89.32/12.86 % (379747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.32/12.86 % (379747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.32/12.86 % (379747)CaDiCaL version: 2.1.3 % 89.32/12.86 % (379747)Termination reason: Instruction limit % 89.32/12.86 % (379747)Termination phase: Saturation % 89.32/12.86 % (379747)Time elapsed: 0.486 s % 89.32/12.86 % (379747)Peak memory usage: 15 MB % 89.32/12.86 % (379747)Instructions burned: 870 (million) % 89.32/12.86 % (379755)dis+21_1_sil=32000:sas=cadical:random_seed=3800020296:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 89.32/12.86 % (379741)Instruction limit reached! % 89.32/12.86 % (379741)------------------------------ % 89.32/12.86 % (379741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.32/12.86 % (379741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.32/12.86 % (379741)CaDiCaL version: 2.1.3 % 89.32/12.86 % (379741)Termination reason: Instruction limit % 89.32/12.86 % (379741)Termination phase: Saturation % 89.32/12.86 % (379741)Time elapsed: 0.736 s % 89.32/12.86 % (379741)Peak memory usage: 24 MB % 89.32/12.86 % (379741)Instructions burned: 1474 (million) % 89.32/12.86 % (379757)ott+11_1_sil=16000:gs=on:random_seed=1276936492:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 89.32/12.86 % (379739)Instruction limit reached! % 89.32/12.86 % (379739)------------------------------ % 89.32/12.86 % (379739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.32/12.86 % (379739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.32/12.86 % (379739)CaDiCaL version: 2.1.3 % 89.32/12.86 % (379739)Termination reason: Instruction limit % 89.32/12.86 % (379739)Termination phase: Saturation % 89.32/12.86 % (379739)Time elapsed: 1.396 s % 89.32/12.86 % (379739)Peak memory usage: 31 MB % 89.32/12.86 % (379739)Instructions burned: 5135 (million) % 89.32/12.86 % (379759)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3923110920:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 89.32/12.86 % (379759)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 89.32/12.86 % (379759)Terminated due to inappropriate strategy. % 89.32/12.86 % (379759)------------------------------ % 89.32/12.86 % (379759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.32/12.86 % (379759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.32/12.86 % (379759)CaDiCaL version: 2.1.3 % 89.32/12.86 % (379759)Termination reason: Inappropriate % 89.32/12.86 % (379759)Time elapsed: 0.001 s % 89.32/12.86 % (379759)Peak memory usage: 10 MB % 89.32/12.86 % (379759)Instructions burned: 4 (million) % 89.32/12.86 % (379759)------------------------------ % 89.32/12.86 % (379759)------------------------------ % 89.32/12.86 % (379761)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=659418609:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 89.32/12.86 % (379757)Instruction limit reached! % 89.32/12.86 % (379757)------------------------------ % 89.32/12.86 % (379757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.32/12.86 % (379757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.32/12.86 % (379757)CaDiCaL version: 2.1.3 % 89.32/12.86 % (379757)Termination reason: Instruction limit % 89.32/12.86 % (379757)Termination phase: Saturation % 89.32/12.86 % (379757)Time elapsed: 1.099 s % 89.32/12.86 % (379757)Peak memory usage: 15 MB % 89.32/12.86 % (379757)Instructions burned: 2252 (million) % 89.32/12.86 % (379763)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1636684191:i=29340_2976 on theBenchmark for (2976ds/29340Mi) % 89.32/12.86 % (379753)Instruction limit reached! % 89.32/12.86 % (379753)------------------------------ % 89.32/12.86 % (379753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.32/12.86 % (379753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.32/12.86 % (379753)CaDiCaL version: 2.1.3 % 89.32/12.86 % (379753)Termination reason: Instruction limit % 89.32/12.86 % (379753)Termination phase: Saturation % 89.32/12.86 % (379753)Time elapsed: 1.890 s % 89.32/12.86 % (379753)Peak memory usage: 26 MB % 89.32/12.86 % (379753)Instructions burned: 3512 (million) % 89.32/12.86 % (379765)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1923122354:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 89.32/12.86 % (379755)Instruction limit reached! % 110.76/17.08 % (379755)------------------------------ % 110.76/17.08 % (379755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.76/17.08 % (379755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.76/17.08 % (379755)CaDiCaL version: 2.1.3 % 110.76/17.08 % (379755)Termination reason: Instruction limit % 110.76/17.08 % (379755)Termination phase: Saturation % 110.76/17.08 % (379755)Time elapsed: 1.965 s % 110.76/17.08 % (379755)Peak memory usage: 26 MB % 110.76/17.08 % (379755)Instructions burned: 3774 (million) % 110.76/17.08 % (379767)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1502313232:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 110.76/17.08 % (379767)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 110.76/17.08 % (379767)Terminated due to inappropriate strategy. % 110.76/17.08 % (379767)------------------------------ % 110.76/17.08 % (379767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.76/17.08 % (379767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.76/17.08 % (379767)CaDiCaL version: 2.1.3 % 110.76/17.08 % (379767)Termination reason: Inappropriate % 110.76/17.08 % (379767)Time elapsed: 0.002 s % 110.76/17.08 % (379767)Peak memory usage: 11 MB % 110.76/17.08 % (379767)Instructions burned: 4 (million) % 110.76/17.08 % (379767)------------------------------ % 110.76/17.08 % (379767)------------------------------ % 110.76/17.08 % (379769)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1416672742:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 110.76/17.08 % (379769)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 110.76/17.08 % (379769)Terminated due to inappropriate strategy. % 110.76/17.08 % (379769)------------------------------ % 110.76/17.08 % (379769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.76/17.08 % (379769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.76/17.08 % (379769)CaDiCaL version: 2.1.3 % 110.76/17.08 % (379769)Termination reason: Inappropriate % 110.76/17.08 % (379769)Time elapsed: 0.002 s % 110.76/17.08 % (379769)Peak memory usage: 10 MB % 110.76/17.08 % (379769)Instructions burned: 4 (million) % 110.76/17.08 % (379769)------------------------------ % 110.76/17.08 % (379769)------------------------------ % 110.76/17.08 % (379771)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2053303:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 110.76/17.08 % (379771)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 110.76/17.08 % (379771)Terminated due to inappropriate strategy. % 110.76/17.08 % (379771)------------------------------ % 110.76/17.08 % (379771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.76/17.08 % (379771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.76/17.08 % (379771)CaDiCaL version: 2.1.3 % 110.76/17.08 % (379771)Termination reason: Inappropriate % 110.76/17.08 % (379771)Time elapsed: 0.002 s % 110.76/17.08 % (379771)Peak memory usage: 11 MB % 110.76/17.08 % (379771)Instructions burned: 4 (million) % 110.76/17.08 % (379771)------------------------------ % 110.76/17.08 % (379771)------------------------------ % 110.76/17.08 % (379773)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2412108538:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 110.76/17.08 % (379761)Instruction limit reached! % 110.76/17.08 % (379761)------------------------------ % 110.76/17.08 % (379761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.76/17.08 % (379761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.76/17.08 % (379761)CaDiCaL version: 2.1.3 % 110.76/17.08 % (379761)Termination reason: Instruction limit % 110.76/17.08 % (379761)Termination phase: Saturation % 110.76/17.08 % (379761)Time elapsed: 1.278 s % 110.76/17.08 % (379761)Peak memory usage: 29 MB % 110.76/17.08 % (379761)Instructions burned: 4591 (million) % 110.76/17.08 % (379775)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3423399907:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 110.76/17.08 % (379749)Instruction limit reached! % 110.76/17.08 % (379749)------------------------------ % 110.76/17.08 % (379749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.76/17.08 % (379749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.76/17.08 % (379749)CaDiCaL version: 2.1.3 % 110.76/17.08 % (379749)Termination reason: Instruction limit % 110.76/17.08 % (379749)Termination phase: Saturation % 110.76/17.08 % (379749)Time elapsed: 2.997 s % 128.36/18.38 % (379749)Peak memory usage: 36 MB % 128.36/18.38 % (379749)Instructions burned: 5114 (million) % 128.36/18.38 % (379778)dis+10_16:1_sil=16000:random_seed=3252351673:i=9155:fsr=off_2962 on theBenchmark for (2962ds/9155Mi) % 128.36/18.38 % (379765)Instruction limit reached! % 128.36/18.38 % (379765)------------------------------ % 128.36/18.38 % (379765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.36/18.38 % (379765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.36/18.38 % (379765)CaDiCaL version: 2.1.3 % 128.36/18.38 % (379765)Termination reason: Instruction limit % 128.36/18.38 % (379765)Termination phase: Saturation % 128.36/18.38 % (379765)Time elapsed: 2.656 s % 128.36/18.38 % (379765)Peak memory usage: 41 MB % 128.36/18.38 % (379765)Instructions burned: 5212 (million) % 128.36/18.38 % (379780)ott-3_8_sil=64000:random_seed=2823950968:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi) % 128.36/18.38 % (379775)Instruction limit reached! % 128.36/18.38 % (379775)------------------------------ % 128.36/18.38 % (379775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.36/18.38 % (379775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.36/18.38 % (379775)CaDiCaL version: 2.1.3 % 128.36/18.38 % (379775)Termination reason: Instruction limit % 128.36/18.38 % (379775)Termination phase: Saturation % 128.36/18.38 % (379775)Time elapsed: 2.729 s % 128.36/18.38 % (379775)Peak memory usage: 54 MB % 128.36/18.38 % (379775)Instructions burned: 8176 (million) % 128.36/18.38 % (379782)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1121759058:fmbsr=2:i=32576_2941 on theBenchmark for (2941ds/32576Mi) % 128.36/18.38 % (379782)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 128.36/18.38 % (379782)Terminated due to inappropriate strategy. % 128.36/18.38 % (379782)------------------------------ % 128.36/18.38 % (379782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.36/18.38 % (379782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.36/18.38 % (379782)CaDiCaL version: 2.1.3 % 128.36/18.38 % (379782)Termination reason: Inappropriate % 128.36/18.38 % (379782)Time elapsed: 0.001 s % 128.36/18.38 % (379782)Peak memory usage: 11 MB % 128.36/18.38 % (379782)Instructions burned: 4 (million) % 128.36/18.38 % (379782)------------------------------ % 128.36/18.38 % (379782)------------------------------ % 128.36/18.38 % (379784)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1426056264:i=11404_2941 on theBenchmark for (2941ds/11404Mi) % 128.36/18.38 % (379778)Instruction limit reached! % 128.36/18.38 % (379778)------------------------------ % 128.36/18.38 % (379778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.36/18.38 % (379778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.36/18.38 % (379778)CaDiCaL version: 2.1.3 % 128.36/18.38 % (379778)Termination reason: Instruction limit % 128.36/18.38 % (379778)Termination phase: Saturation % 128.36/18.38 % (379778)Time elapsed: 4.598 s % 128.36/18.38 % (379778)Peak memory usage: 37 MB % 128.36/18.38 % (379778)Instructions burned: 9155 (million) % 128.36/18.38 % (379786)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4281571541:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 128.36/18.38 % (379784)Instruction limit reached! % 128.36/18.38 % (379784)------------------------------ % 128.36/18.38 % (379784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.36/18.38 % (379784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.36/18.38 % (379784)CaDiCaL version: 2.1.3 % 128.36/18.38 % (379784)Termination reason: Instruction limit % 128.36/18.38 % (379784)Termination phase: Saturation % 128.36/18.38 % (379784)Time elapsed: 3.750 s % 128.36/18.38 % (379784)Peak memory usage: 51 MB % 128.36/18.38 % (379784)Instructions burned: 11404 (million) % 128.36/18.38 % (379788)dis+33_16_sil=32000:sac=on:random_seed=1142802140:i=15851:nm=0_2903 on theBenchmark for (2903ds/15851Mi) % 128.36/18.38 % (379773)Instruction limit reached! % 128.36/18.38 % (379773)------------------------------ % 128.36/18.38 % (379773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.36/18.38 % (379773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.36/18.38 % (379773)CaDiCaL version: 2.1.3 % 128.36/18.38 % (379773)Termination reason: Instruction limit % 128.36/18.38 % (379773)Termination phase: Saturation % 128.36/18.38 % (379773)Time elapsed: 9.492 s % 128.36/18.38 % (379773)Peak memory usage: 42 MB % 128.36/18.38 % (379773)Instructions burned: 22565 (million) % 128.36/18.38 % (379790)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3681969563:avsq=on:i=17627:add=on:amm=off_2873 on theBenchmark for (2873ds/17627Mi) % 177.35/25.22 % (379788)Instruction limit reached! % 177.35/25.22 % (379788)------------------------------ % 177.35/25.22 % (379788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.35/25.22 % (379788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.35/25.22 % (379788)CaDiCaL version: 2.1.3 % 177.35/25.22 % (379788)Termination reason: Instruction limit % 177.35/25.22 % (379788)Termination phase: Saturation % 177.35/25.22 % (379788)Time elapsed: 4.643 s % 177.35/25.22 % (379788)Peak memory usage: 130 MB % 177.35/25.22 % (379788)Instructions burned: 15852 (million) % 177.35/25.22 % (379794)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1101529169:s2a=on:i=53295_2856 on theBenchmark for (2856ds/53295Mi) % 177.35/25.22 % (379763)Instruction limit reached! % 177.35/25.22 % (379763)------------------------------ % 177.35/25.22 % (379763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.35/25.22 % (379763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.35/25.22 % (379763)CaDiCaL version: 2.1.3 % 177.35/25.22 % (379763)Termination reason: Instruction limit % 177.35/25.22 % (379763)Termination phase: Saturation % 177.35/25.22 % (379763)Time elapsed: 14.057 s % 177.35/25.22 % (379763)Peak memory usage: 169 MB % 177.35/25.22 % (379763)Instructions burned: 29342 (million) % 177.35/25.22 % (379842)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=871770085:i=26857:ins=20_2835 on theBenchmark for (2835ds/26857Mi) % 177.35/25.22 % (379842)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.35/25.22 % (379842)Terminated due to inappropriate strategy. % 177.35/25.22 % (379842)------------------------------ % 177.35/25.22 % (379842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.35/25.22 % (379842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.35/25.22 % (379842)CaDiCaL version: 2.1.3 % 177.35/25.22 % (379842)Termination reason: Inappropriate % 177.35/25.22 % (379842)Time elapsed: 0.002 s % 177.35/25.22 % (379842)Peak memory usage: 10 MB % 177.35/25.22 % (379842)Instructions burned: 4 (million) % 177.35/25.22 % (379842)------------------------------ % 177.35/25.22 % (379842)------------------------------ % 177.35/25.22 % (379844)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1693269986:i=28120:bs=on:fsr=off_2835 on theBenchmark for (2835ds/28120Mi) % 177.35/25.22 % (379786)Instruction limit reached! % 177.35/25.22 % (379786)------------------------------ % 177.35/25.22 % (379786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.35/25.22 % (379786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.35/25.22 % (379786)CaDiCaL version: 2.1.3 % 177.35/25.22 % (379786)Termination reason: Instruction limit % 177.35/25.22 % (379786)Termination phase: Saturation % 177.35/25.22 % (379786)Time elapsed: 8.462 s % 177.35/25.22 % (379786)Peak memory usage: 62 MB % 177.35/25.22 % (379786)Instructions burned: 14135 (million) % 177.35/25.22 % (379846)fmb+10_1_sil=256000:fmbss=7:random_seed=1362655264:fmbsr=1.6:i=182295_2831 on theBenchmark for (2831ds/182295Mi) % 177.35/25.22 % (379846)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.35/25.22 % (379846)Terminated due to inappropriate strategy. % 177.35/25.22 % (379846)------------------------------ % 177.35/25.22 % (379846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.35/25.22 % (379846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.35/25.22 % (379846)CaDiCaL version: 2.1.3 % 177.35/25.22 % (379846)Termination reason: Inappropriate % 177.35/25.22 % (379846)Time elapsed: 0.002 s % 177.35/25.22 % (379846)Peak memory usage: 11 MB % 177.35/25.22 % (379846)Instructions burned: 4 (million) % 177.35/25.22 % (379846)------------------------------ % 177.35/25.22 % (379846)------------------------------ % 177.35/25.22 % (379848)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=298359687:i=44625:gsp=on_2831 on theBenchmark for (2831ds/44625Mi) % 177.35/25.22 % (379848)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.35/25.22 % (379848)Terminated due to inappropriate strategy. % 177.35/25.22 % (379848)------------------------------ % 177.35/25.22 % (379848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.35/25.22 % (379848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.35/25.22 % (379848)CaDiCaL version: 2.1.3 % 177.35/25.22 % (379848)Termination reason: Inappropriate % 187.02/26.64 % (379848)Time elapsed: 0.002 s % 187.02/26.64 % (379848)Peak memory usage: 10 MB % 187.02/26.64 % (379848)Instructions burned: 4 (million) % 187.02/26.64 % (379848)------------------------------ % 187.02/26.64 % (379848)------------------------------ % 187.02/26.64 % (379850)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=191778637:i=160505_2831 on theBenchmark for (2831ds/160505Mi) % 187.02/26.64 % (379850)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.02/26.64 % (379850)Terminated due to inappropriate strategy. % 187.02/26.64 % (379850)------------------------------ % 187.02/26.64 % (379850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.02/26.64 % (379850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.02/26.64 % (379850)CaDiCaL version: 2.1.3 % 187.02/26.64 % (379850)Termination reason: Inappropriate % 187.02/26.64 % (379850)Time elapsed: 0.002 s % 187.02/26.64 % (379850)Peak memory usage: 10 MB % 187.02/26.64 % (379850)Instructions burned: 4 (million) % 187.02/26.64 % (379850)------------------------------ % 187.02/26.64 % (379850)------------------------------ % 187.02/26.64 % (379852)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2015795274:fmbsr=1.3:i=225729_2831 on theBenchmark for (2831ds/225729Mi) % 187.02/26.64 % (379852)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.02/26.64 % (379852)Terminated due to inappropriate strategy. % 187.02/26.64 % (379852)------------------------------ % 187.02/26.64 % (379852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.02/26.64 % (379852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.02/26.64 % (379852)CaDiCaL version: 2.1.3 % 187.02/26.64 % (379852)Termination reason: Inappropriate % 187.02/26.64 % (379852)Time elapsed: 0.002 s % 187.02/26.64 % (379852)Peak memory usage: 10 MB % 187.02/26.64 % (379852)Instructions burned: 4 (million) % 187.02/26.64 % (379852)------------------------------ % 187.02/26.64 % (379852)------------------------------ % 187.02/26.64 % (379854)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4004332658:fmbsr=2:i=185024:ins=7_2830 on theBenchmark for (2830ds/185024Mi) % 187.02/26.64 % (379854)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.02/26.64 % (379854)Terminated due to inappropriate strategy. % 187.02/26.64 % (379854)------------------------------ % 187.02/26.64 % (379854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.02/26.64 % (379854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.02/26.64 % (379854)CaDiCaL version: 2.1.3 % 187.02/26.64 % (379854)Termination reason: Inappropriate % 187.02/26.64 % (379854)Time elapsed: 0.002 s % 187.02/26.64 % (379854)Peak memory usage: 10 MB % 187.02/26.64 % (379854)Instructions burned: 4 (million) % 187.02/26.64 % (379854)------------------------------ % 187.02/26.64 % (379854)------------------------------ % 187.02/26.64 % (379856)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4267274771:rtra=on_2830 on theBenchmark for (2830ds/0Mi) % 187.02/26.64 % (379856)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.02/26.64 % (379856)Terminated due to inappropriate strategy. % 187.02/26.64 % (379856)------------------------------ % 187.02/26.64 % (379856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.02/26.64 % (379856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.02/26.64 % (379856)CaDiCaL version: 2.1.3 % 187.02/26.64 % (379856)Termination reason: Inappropriate % 187.02/26.64 % (379856)Time elapsed: 0.003 s % 187.02/26.64 % (379856)Peak memory usage: 11 MB % 187.02/26.64 % (379856)Instructions burned: 5 (million) % 187.02/26.64 % (379856)------------------------------ % 187.02/26.64 % (379856)------------------------------ % 187.02/26.64 % (379858)% WARNING: option uhcvi not known. % 187.02/26.64 % (379858)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=365676247:i=271062:add=off:rtra=on:rawr=on_2830 on theBenchmark for (2830ds/271062Mi) % 187.02/26.64 % (379780)Instruction limit reached! % 187.02/26.64 % (379780)------------------------------ % 187.02/26.64 % (379780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.02/26.64 % (379780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.02/26.64 % (379780)CaDiCaL version: 2.1.3 % 187.02/26.64 % (379780)Termination reason: Instruction limit % 187.02/26.64 % (379780)Termination phase: Saturation % 187.02/26.64 % (379780)Time elapsed: 12.659 s % 187.02/26.64 % (379780)Peak memory usage: 64 MB % 187.02/26.64 % (379780)Instructions burned: 20140 (million) % 187.02/26.64 % (379860)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2283214788:i=176048:add=on:rtra=on:rawr=on_2818 on theBenchmark for (2818ds/176048Mi) % 196.22/27.91 % (379790)Instruction limit reached! % 196.22/27.91 % (379790)------------------------------ % 196.22/27.91 % (379790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.22/27.91 % (379790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.22/27.91 % (379790)CaDiCaL version: 2.1.3 % 196.22/27.91 % (379790)Termination reason: Instruction limit % 196.22/27.91 % (379790)Termination phase: Saturation % 196.22/27.91 % (379790)Time elapsed: 11.586 s % 196.22/27.91 % (379790)Peak memory usage: 81 MB % 196.22/27.91 % (379790)Instructions burned: 17628 (million) % 196.22/27.91 % (379863)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2158246361:i=206:fgj=on:rtra=on_2757 on theBenchmark for (2757ds/206Mi) % 196.22/27.91 % (379863)Instruction limit reached! % 196.22/27.91 % (379863)------------------------------ % 196.22/27.91 % (379863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.22/27.91 % (379863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.22/27.91 % (379863)CaDiCaL version: 2.1.3 % 196.22/27.91 % (379863)Termination reason: Instruction limit % 196.22/27.91 % (379863)Termination phase: Saturation % 196.22/27.91 % (379863)Time elapsed: 0.126 s % 196.22/27.91 % (379863)Peak memory usage: 13 MB % 196.22/27.91 % (379863)Instructions burned: 207 (million) % 196.22/27.91 % (379865)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1696484895:i=232:rtra=on_2756 on theBenchmark for (2756ds/232Mi) % 196.22/27.91 % (379865)Instruction limit reached! % 196.22/27.91 % (379865)------------------------------ % 196.22/27.91 % (379865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.22/27.91 % (379865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.22/27.91 % (379865)CaDiCaL version: 2.1.3 % 196.22/27.91 % (379865)Termination reason: Instruction limit % 196.22/27.91 % (379865)Termination phase: Saturation % 196.22/27.91 % (379865)Time elapsed: 0.146 s % 196.22/27.91 % (379865)Peak memory usage: 14 MB % 196.22/27.91 % (379865)Instructions burned: 233 (million) % 196.22/27.91 % (379867)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3997529426:i=262:rtra=on_2754 on theBenchmark for (2754ds/262Mi) % 196.22/27.91 % (379867)Instruction limit reached! % 196.22/27.91 % (379867)------------------------------ % 196.22/27.91 % (379867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.22/27.91 % (379867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.22/27.91 % (379867)CaDiCaL version: 2.1.3 % 196.22/27.91 % (379867)Termination reason: Instruction limit % 196.22/27.91 % (379867)Termination phase: Saturation % 196.22/27.91 % (379867)Time elapsed: 0.164 s % 196.22/27.91 % (379867)Peak memory usage: 13 MB % 196.22/27.91 % (379867)Instructions burned: 263 (million) % 196.22/27.91 % (379869)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1476871871:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2752 on theBenchmark for (2752ds/318Mi) % 196.22/27.91 % (379869)Instruction limit reached! % 196.22/27.91 % (379869)------------------------------ % 196.22/27.91 % (379869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.22/27.91 % (379869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.22/27.91 % (379869)CaDiCaL version: 2.1.3 % 196.22/27.91 % (379869)Termination reason: Instruction limit % 196.22/27.91 % (379869)Termination phase: Saturation % 196.22/27.91 % (379869)Time elapsed: 0.220 s % 196.22/27.91 % (379869)Peak memory usage: 16 MB % 196.22/27.91 % (379869)Instructions burned: 319 (million) % 196.22/27.91 % (379871)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=362789080:i=1428:nm=2:rtra=on_2750 on theBenchmark for (2750ds/1428Mi) % 196.22/27.91 % (379871)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 196.22/27.91 % (379871)Terminated due to inappropriate strategy. % 196.22/27.91 % (379871)------------------------------ % 196.22/27.91 % (379871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.22/27.91 % (379871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.22/27.91 % (379871)CaDiCaL version: 2.1.3 % 196.22/27.91 % (379871)Termination reason: Inappropriate % 196.22/27.91 % (379871)Time elapsed: 0.003 s % 196.22/27.91 % (379871)Peak memory usage: 10 MB % 196.22/27.91 % (379871)Instructions burned: 4 (million) % 196.22/27.91 % (379871)------------------------------ % 196.22/27.91 % (379871)------------------------------ % 214.24/30.47 % (379873)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=4101428831:i=262:bd=preordered:rtra=on:fsd=on_2749 on theBenchmark for (2749ds/262Mi) % 214.24/30.47 % (379873)Instruction limit reached! % 214.24/30.47 % (379873)------------------------------ % 214.24/30.47 % (379873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.24/30.47 % (379873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.24/30.47 % (379873)CaDiCaL version: 2.1.3 % 214.24/30.47 % (379873)Termination reason: Instruction limit % 214.24/30.47 % (379873)Termination phase: Saturation % 214.24/30.47 % (379873)Time elapsed: 0.162 s % 214.24/30.47 % (379873)Peak memory usage: 13 MB % 214.24/30.47 % (379873)Instructions burned: 262 (million) % 214.24/30.47 % (379875)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=3793888589:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2748 on theBenchmark for (2748ds/1368Mi) % 214.24/30.47 % (379844)Instruction limit reached! % 214.24/30.47 % (379844)------------------------------ % 214.24/30.47 % (379844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.24/30.47 % (379844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.24/30.47 % (379844)CaDiCaL version: 2.1.3 % 214.24/30.47 % (379844)Termination reason: Instruction limit % 214.24/30.47 % (379844)Termination phase: Saturation % 214.24/30.47 % (379844)Time elapsed: 9.112 s % 214.24/30.47 % (379844)Peak memory usage: 17 MB % 214.24/30.47 % (379844)Instructions burned: 28121 (million) % 214.24/30.47 % (379877)ott-21_1_sil=16000:si=on:fs=off:random_seed=2370098236:i=360:av=off:fsr=off:rtra=on_2744 on theBenchmark for (2744ds/360Mi) % 214.24/30.47 % (379877)Instruction limit reached! % 214.24/30.47 % (379877)------------------------------ % 214.24/30.47 % (379877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.24/30.47 % (379877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.24/30.47 % (379877)CaDiCaL version: 2.1.3 % 214.24/30.47 % (379877)Termination reason: Instruction limit % 214.24/30.47 % (379877)Termination phase: Saturation % 214.24/30.47 % (379877)Time elapsed: 0.180 s % 214.24/30.47 % (379877)Peak memory usage: 13 MB % 214.24/30.47 % (379877)Instructions burned: 362 (million) % 214.24/30.47 % (379879)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2604600618:i=954:bd=all:rtra=on_2742 on theBenchmark for (2742ds/954Mi) % 214.24/30.47 % (379875)Instruction limit reached! % 214.24/30.47 % (379875)------------------------------ % 214.24/30.47 % (379875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.24/30.47 % (379875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.24/30.47 % (379875)CaDiCaL version: 2.1.3 % 214.24/30.47 % (379875)Termination reason: Instruction limit % 214.24/30.47 % (379875)Termination phase: Saturation % 214.24/30.47 % (379875)Time elapsed: 0.848 s % 214.24/30.47 % (379875)Peak memory usage: 24 MB % 214.24/30.47 % (379875)Instructions burned: 1369 (million) % 214.24/30.47 % (379881)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2610286789:fmbsr=1.3:i=1730:ins=25:rtra=on_2739 on theBenchmark for (2739ds/1730Mi) % 214.24/30.47 % (379881)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 214.24/30.47 % (379881)Terminated due to inappropriate strategy. % 214.24/30.47 % (379881)------------------------------ % 214.24/30.47 % (379881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.24/30.47 % (379881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.24/30.47 % (379881)CaDiCaL version: 2.1.3 % 214.24/30.47 % (379881)Termination reason: Inappropriate % 214.24/30.47 % (379881)Time elapsed: 0.002 s % 214.24/30.47 % (379881)Peak memory usage: 10 MB % 214.24/30.47 % (379881)Instructions burned: 4 (million) % 214.24/30.47 % (379881)------------------------------ % 214.24/30.47 % (379881)------------------------------ % 214.24/30.47 % (379883)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2381662375:i=2358:rtra=on_2739 on theBenchmark for (2739ds/2358Mi) % 214.24/30.47 % (379879)Instruction limit reached! % 214.24/30.47 % (379879)------------------------------ % 214.24/30.47 % (379879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.24/30.47 % (379879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.24/30.47 % (379879)CaDiCaL version: 2.1.3 % 214.24/30.47 % (379879)Termination reason: Instruction limit % 214.24/30.47 % (379879)Termination phase: Saturation % 269.79/38.30 % (379879)Time elapsed: 0.637 s % 269.79/38.30 % (379879)Peak memory usage: 16 MB % 269.79/38.30 % (379879)Instructions burned: 955 (million) % 269.79/38.30 % (379885)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1111520460:i=1778:ins=1:rtra=on_2735 on theBenchmark for (2735ds/1778Mi) % 269.79/38.30 % (379885)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.79/38.30 % (379885)Terminated due to inappropriate strategy. % 269.79/38.30 % (379885)------------------------------ % 269.79/38.30 % (379885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.79/38.30 % (379885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.79/38.30 % (379885)CaDiCaL version: 2.1.3 % 269.79/38.30 % (379885)Termination reason: Inappropriate % 269.79/38.30 % (379885)Time elapsed: 0.003 s % 269.79/38.30 % (379885)Peak memory usage: 10 MB % 269.79/38.30 % (379885)Instructions burned: 4 (million) % 269.79/38.30 % (379885)------------------------------ % 269.79/38.30 % (379885)------------------------------ % 269.79/38.30 % (379887)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3741153560:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2735 on theBenchmark for (2735ds/1384Mi) % 269.79/38.30 % (379887)Instruction limit reached! % 269.79/38.30 % (379887)------------------------------ % 269.79/38.30 % (379887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.79/38.30 % (379887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.79/38.30 % (379887)CaDiCaL version: 2.1.3 % 269.79/38.30 % (379887)Termination reason: Instruction limit % 269.79/38.30 % (379887)Termination phase: Saturation % 269.79/38.30 % (379887)Time elapsed: 0.908 s % 269.79/38.30 % (379887)Peak memory usage: 24 MB % 269.79/38.30 % (379887)Instructions burned: 1385 (million) % 269.79/38.30 % (379889)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2100718724:i=1758:kws=inv_precedence:fsr=off:rtra=on_2726 on theBenchmark for (2726ds/1758Mi) % 269.79/38.30 % (379883)Instruction limit reached! % 269.79/38.30 % (379883)------------------------------ % 269.79/38.30 % (379883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.79/38.30 % (379883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.79/38.30 % (379883)CaDiCaL version: 2.1.3 % 269.79/38.30 % (379883)Termination reason: Instruction limit % 269.79/38.30 % (379883)Termination phase: Saturation % 269.79/38.30 % (379883)Time elapsed: 1.502 s % 269.79/38.30 % (379883)Peak memory usage: 26 MB % 269.79/38.30 % (379883)Instructions burned: 2358 (million) % 269.79/38.30 % (379891)fmb+10_1_sil=64000:si=on:random_seed=595619871:i=44122:nm=2:rtra=on:gsp=on_2723 on theBenchmark for (2723ds/44122Mi) % 269.79/38.30 % (379891)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.79/38.30 % (379891)Terminated due to inappropriate strategy. % 269.79/38.30 % (379891)------------------------------ % 269.79/38.30 % (379891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.79/38.30 % (379891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.79/38.30 % (379891)CaDiCaL version: 2.1.3 % 269.79/38.30 % (379891)Termination reason: Inappropriate % 269.79/38.30 % (379891)Time elapsed: 0.003 s % 269.79/38.30 % (379891)Peak memory usage: 10 MB % 269.79/38.30 % (379891)Instructions burned: 5 (million) % 269.79/38.30 % (379891)------------------------------ % 269.79/38.30 % (379891)------------------------------ % 269.79/38.30 % (379893)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2082678200:i=19030:nm=5:rtra=on_2723 on theBenchmark for (2723ds/19030Mi) % 269.79/38.30 % (379893)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.79/38.30 % (379893)Terminated due to inappropriate strategy. % 269.79/38.30 % (379893)------------------------------ % 269.79/38.30 % (379893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.79/38.30 % (379893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.79/38.30 % (379893)CaDiCaL version: 2.1.3 % 269.79/38.30 % (379893)Termination reason: Inappropriate % 269.79/38.30 % (379893)Time elapsed: 0.003 s % 269.79/38.30 % (379893)Peak memory usage: 10 MB % 269.79/38.30 % (379893)Instructions burned: 4 (million) % 269.79/38.30 % (379893)------------------------------ % 269.79/38.30 % (379893)------------------------------ % 269.79/38.30 % (379895)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2198236465:fmbsr=1.7:i=1840:rtra=on_2723 on thTerminated % 300.35/42.54 % Vampire exiting % 300.35/42.54 Terminated %------------------------------------------------------------------------------