%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW590_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n008.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:29 PM UTC 2026 % Result : Timeout 297.11s 42.13s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWW590_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.22/0.27 % Computer : n008.cluster.edu % 0.22/0.27 % Model : x86_64 x86_64 % 0.22/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.22/0.27 % Memory : 8046.5625MB % 0.22/0.27 % OS : Linux 6.8.0-71-generic % 0.22/0.27 % CPULimit : 300 % 0.22/0.27 % WCLimit : 300 % 0.22/0.27 % DateTime : Mon Sep 28 14:20:54 UTC 2026 % 0.22/0.28 % CPUTime : % 0.22/0.28 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.22/0.31 Running first-order model finding % 0.22/0.31 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 7.08/1.35 % (2283068)Will run a generic schedule for satisfiability detection. % 7.08/1.35 % (2283074)% WARNING: option uhcvi not known. % 7.08/1.35 % (2283076)dis+10_1_sil=32000:sp=arity:random_seed=244162336:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.08/1.35 % (2283074)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=346068665:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.08/1.35 % (2283078)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1138722389:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.08/1.35 % (2283073)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2736716586_2999 on theBenchmark for (2999ds/0Mi) % 7.08/1.35 % (2283079)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2827442848:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.08/1.35 % (2283075)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2025323011:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.08/1.35 % (2283077)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=838148916:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.08/1.35 % (2283073)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.08/1.35 % (2283073)Terminated due to inappropriate strategy. % 7.08/1.35 % (2283073)------------------------------ % 7.08/1.35 % (2283073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.08/1.35 % (2283073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.08/1.35 % (2283073)CaDiCaL version: 2.1.3 % 7.08/1.35 % (2283073)Termination reason: Inappropriate % 7.08/1.35 % (2283073)Time elapsed: 0.005 s % 7.08/1.35 % (2283073)Peak memory usage: 11 MB % 7.08/1.35 % (2283073)Instructions burned: 4 (million) % 7.08/1.35 % (2283073)------------------------------ % 7.08/1.35 % (2283073)------------------------------ % 7.08/1.35 % (2283087)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3183049048:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.08/1.35 % (2283076)Instruction limit reached! % 7.08/1.35 % (2283076)------------------------------ % 7.08/1.35 % (2283076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.08/1.35 % (2283076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.08/1.35 % (2283076)CaDiCaL version: 2.1.3 % 7.08/1.35 % (2283076)Termination reason: Instruction limit % 7.08/1.35 % (2283076)Termination phase: Saturation % 7.08/1.35 % (2283076)Time elapsed: 0.059 s % 7.08/1.35 % (2283076)Peak memory usage: 13 MB % 7.08/1.35 % (2283076)Instructions burned: 104 (million) % 7.08/1.35 % (2283087)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.08/1.35 % (2283087)Terminated due to inappropriate strategy. % 7.08/1.35 % (2283087)------------------------------ % 7.08/1.35 % (2283087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.08/1.35 % (2283087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.08/1.35 % (2283087)CaDiCaL version: 2.1.3 % 7.08/1.35 % (2283087)Termination reason: Inappropriate % 7.08/1.35 % (2283087)Time elapsed: 0.005 s % 7.08/1.35 % (2283087)Peak memory usage: 10 MB % 7.08/1.35 % (2283087)Instructions burned: 4 (million) % 7.08/1.35 % (2283087)------------------------------ % 7.08/1.35 % (2283087)------------------------------ % 7.08/1.35 % (2283089)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2067605960:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.08/1.35 % (2283090)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=3431125984:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.08/1.35 % (2283077)Instruction limit reached! % 7.08/1.35 % (2283077)------------------------------ % 7.08/1.35 % (2283077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.08/1.35 % (2283077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.08/1.35 % (2283077)CaDiCaL version: 2.1.3 % 7.08/1.35 % (2283077)Termination reason: Instruction limit % 7.08/1.35 % (2283077)Termination phase: Saturation % 7.08/1.35 % (2283077)Time elapsed: 0.113 s % 7.08/1.35 % (2283077)Peak memory usage: 13 MB % 7.08/1.35 % (2283077)Instructions burned: 117 (million) % 7.08/1.35 % (2283078)Instruction limit reached! % 7.08/1.35 % (2283078)------------------------------ % 7.08/1.35 % (2283078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.99/1.84 % (2283078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.99/1.84 % (2283078)CaDiCaL version: 2.1.3 % 9.99/1.84 % (2283078)Termination reason: Instruction limit % 9.99/1.84 % (2283078)Termination phase: Saturation % 9.99/1.84 % (2283078)Time elapsed: 0.126 s % 9.99/1.84 % (2283078)Peak memory usage: 13 MB % 9.99/1.84 % (2283078)Instructions burned: 131 (million) % 9.99/1.84 % (2283094)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3776792670:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 9.99/1.84 % (2283093)ott-21_1_sil=16000:fs=off:random_seed=3245431825:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 9.99/1.84 % (2283079)Instruction limit reached! % 9.99/1.84 % (2283079)------------------------------ % 9.99/1.84 % (2283079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.99/1.84 % (2283079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.99/1.84 % (2283079)CaDiCaL version: 2.1.3 % 9.99/1.84 % (2283079)Termination reason: Instruction limit % 9.99/1.84 % (2283079)Termination phase: Saturation % 9.99/1.84 % (2283079)Time elapsed: 0.184 s % 9.99/1.84 % (2283079)Peak memory usage: 13 MB % 9.99/1.84 % (2283079)Instructions burned: 159 (million) % 9.99/1.84 % (2283089)Instruction limit reached! % 9.99/1.84 % (2283089)------------------------------ % 9.99/1.84 % (2283089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.99/1.84 % (2283089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.99/1.84 % (2283089)CaDiCaL version: 2.1.3 % 9.99/1.84 % (2283089)Termination reason: Instruction limit % 9.99/1.84 % (2283089)Termination phase: Saturation % 9.99/1.84 % (2283089)Time elapsed: 0.146 s % 9.99/1.84 % (2283089)Peak memory usage: 12 MB % 9.99/1.84 % (2283089)Instructions burned: 131 (million) % 9.99/1.84 % (2283097)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4107779774:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 9.99/1.84 % (2283097)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 9.99/1.84 % (2283097)Terminated due to inappropriate strategy. % 9.99/1.84 % (2283097)------------------------------ % 9.99/1.84 % (2283097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.99/1.84 % (2283097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.99/1.84 % (2283097)CaDiCaL version: 2.1.3 % 9.99/1.84 % (2283097)Termination reason: Inappropriate % 9.99/1.84 % (2283097)Time elapsed: 0.005 s % 9.99/1.84 % (2283097)Peak memory usage: 10 MB % 9.99/1.84 % (2283097)Instructions burned: 4 (million) % 9.99/1.84 % (2283097)------------------------------ % 9.99/1.84 % (2283097)------------------------------ % 9.99/1.84 % (2283098)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2429666435:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 9.99/1.84 % (2283100)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1998503393:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 9.99/1.84 % (2283100)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 9.99/1.84 % (2283100)Terminated due to inappropriate strategy. % 9.99/1.84 % (2283100)------------------------------ % 9.99/1.84 % (2283100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.99/1.84 % (2283100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.99/1.84 % (2283100)CaDiCaL version: 2.1.3 % 9.99/1.84 % (2283100)Termination reason: Inappropriate % 9.99/1.84 % (2283100)Time elapsed: 0.003 s % 9.99/1.84 % (2283100)Peak memory usage: 11 MB % 9.99/1.84 % (2283100)Instructions burned: 4 (million) % 9.99/1.84 % (2283100)------------------------------ % 9.99/1.84 % (2283100)------------------------------ % 9.99/1.84 % (2283103)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=2106993152: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) % 9.99/1.84 % (2283093)Instruction limit reached! % 9.99/1.84 % (2283093)------------------------------ % 9.99/1.84 % (2283093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.99/1.84 % (2283093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.99/1.84 % (2283093)CaDiCaL version: 2.1.3 % 9.99/1.84 % (2283093)Termination reason: Instruction limit % 9.99/1.84 % (2283093)Termination phase: Saturation % 34.82/5.20 % (2283093)Time elapsed: 0.159 s % 34.82/5.20 % (2283093)Peak memory usage: 12 MB % 34.82/5.20 % (2283093)Instructions burned: 180 (million) % 34.82/5.20 % (2283105)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=699402203:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 34.82/5.20 % (2283090)Instruction limit reached! % 34.82/5.20 % (2283090)------------------------------ % 34.82/5.20 % (2283090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.82/5.20 % (2283090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.82/5.20 % (2283090)CaDiCaL version: 2.1.3 % 34.82/5.20 % (2283090)Termination reason: Instruction limit % 34.82/5.20 % (2283090)Termination phase: Saturation % 34.82/5.20 % (2283090)Time elapsed: 0.361 s % 34.82/5.20 % (2283090)Peak memory usage: 17 MB % 34.82/5.20 % (2283090)Instructions burned: 685 (million) % 34.82/5.20 % (2283107)fmb+10_1_sil=64000:random_seed=955878007:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 34.82/5.20 % (2283107)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 34.82/5.20 % (2283107)Terminated due to inappropriate strategy. % 34.82/5.20 % (2283107)------------------------------ % 34.82/5.20 % (2283107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.82/5.20 % (2283107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.82/5.20 % (2283107)CaDiCaL version: 2.1.3 % 34.82/5.20 % (2283107)Termination reason: Inappropriate % 34.82/5.20 % (2283107)Time elapsed: 0.005 s % 34.82/5.20 % (2283107)Peak memory usage: 11 MB % 34.82/5.20 % (2283107)Instructions burned: 4 (million) % 34.82/5.20 % (2283107)------------------------------ % 34.82/5.20 % (2283107)------------------------------ % 34.82/5.20 % (2283109)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1699472664:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 34.82/5.20 % (2283109)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 34.82/5.20 % (2283109)Terminated due to inappropriate strategy. % 34.82/5.20 % (2283109)------------------------------ % 34.82/5.20 % (2283109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.82/5.20 % (2283109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.82/5.20 % (2283109)CaDiCaL version: 2.1.3 % 34.82/5.20 % (2283109)Termination reason: Inappropriate % 34.82/5.20 % (2283109)Time elapsed: 0.003 s % 34.82/5.20 % (2283109)Peak memory usage: 10 MB % 34.82/5.20 % (2283109)Instructions burned: 4 (million) % 34.82/5.20 % (2283109)------------------------------ % 34.82/5.20 % (2283109)------------------------------ % 34.82/5.20 % (2283111)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=12242904:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 34.82/5.20 % (2283111)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 34.82/5.20 % (2283111)Terminated due to inappropriate strategy. % 34.82/5.20 % (2283111)------------------------------ % 34.82/5.20 % (2283111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.82/5.20 % (2283111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.82/5.20 % (2283111)CaDiCaL version: 2.1.3 % 34.82/5.20 % (2283111)Termination reason: Inappropriate % 34.82/5.20 % (2283111)Time elapsed: 0.003 s % 34.82/5.20 % (2283111)Peak memory usage: 11 MB % 34.82/5.20 % (2283111)Instructions burned: 4 (million) % 34.82/5.20 % (2283111)------------------------------ % 34.82/5.20 % (2283111)------------------------------ % 34.82/5.20 % (2283113)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2695702247:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 34.82/5.20 % (2283094)Instruction limit reached! % 34.82/5.20 % (2283094)------------------------------ % 34.82/5.20 % (2283094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.82/5.20 % (2283094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.82/5.20 % (2283094)CaDiCaL version: 2.1.3 % 34.82/5.20 % (2283094)Termination reason: Instruction limit % 34.82/5.20 % (2283094)Termination phase: Saturation % 34.82/5.20 % (2283094)Time elapsed: 0.467 s % 34.82/5.20 % (2283094)Peak memory usage: 13 MB % 34.82/5.20 % (2283094)Instructions burned: 477 (million) % 34.82/5.20 % (2283115)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3289899639:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi) % 34.82/5.20 % (2283103)Instruction limit reached! % 34.82/5.20 % (2283103)------------------------------ % 41.89/6.30 % (2283103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.89/6.30 % (2283103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.89/6.30 % (2283103)CaDiCaL version: 2.1.3 % 41.89/6.30 % (2283103)Termination reason: Instruction limit % 41.89/6.30 % (2283103)Termination phase: Saturation % 41.89/6.30 % (2283103)Time elapsed: 0.715 s % 41.89/6.30 % (2283103)Peak memory usage: 19 MB % 41.89/6.30 % (2283103)Instructions burned: 693 (million) % 41.89/6.30 % (2283117)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=169894839:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 41.89/6.30 % (2283117)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.89/6.30 % (2283117)Terminated due to inappropriate strategy. % 41.89/6.30 % (2283117)------------------------------ % 41.89/6.30 % (2283117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.89/6.30 % (2283117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.89/6.30 % (2283117)CaDiCaL version: 2.1.3 % 41.89/6.30 % (2283117)Termination reason: Inappropriate % 41.89/6.30 % (2283117)Time elapsed: 0.004 s % 41.89/6.30 % (2283117)Peak memory usage: 11 MB % 41.89/6.30 % (2283117)Instructions burned: 4 (million) % 41.89/6.30 % (2283117)------------------------------ % 41.89/6.30 % (2283117)------------------------------ % 41.89/6.30 % (2283119)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2033497799:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 41.89/6.30 % (2283119)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.89/6.30 % (2283119)Terminated due to inappropriate strategy. % 41.89/6.30 % (2283119)------------------------------ % 41.89/6.30 % (2283119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.89/6.30 % (2283119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.89/6.30 % (2283119)CaDiCaL version: 2.1.3 % 41.89/6.30 % (2283119)Termination reason: Inappropriate % 41.89/6.30 % (2283119)Time elapsed: 0.003 s % 41.89/6.30 % (2283119)Peak memory usage: 11 MB % 41.89/6.30 % (2283119)Instructions burned: 4 (million) % 41.89/6.30 % (2283119)------------------------------ % 41.89/6.30 % (2283119)------------------------------ % 41.89/6.30 % (2283121)ott-2_1_sil=16000:newcnf=on:random_seed=3013888413:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 41.89/6.30 % (2283105)Instruction limit reached! % 41.89/6.30 % (2283105)------------------------------ % 41.89/6.30 % (2283105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.89/6.30 % (2283105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.89/6.30 % (2283105)CaDiCaL version: 2.1.3 % 41.89/6.30 % (2283105)Termination reason: Instruction limit % 41.89/6.30 % (2283105)Termination phase: Saturation % 41.89/6.30 % (2283105)Time elapsed: 0.816 s % 41.89/6.30 % (2283105)Peak memory usage: 19 MB % 41.89/6.30 % (2283105)Instructions burned: 879 (million) % 41.89/6.30 % (2283123)ott+10_1_sil=32000:tgt=ground:random_seed=827885198:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi) % 41.89/6.30 % (2283098)Instruction limit reached! % 41.89/6.30 % (2283098)------------------------------ % 41.89/6.30 % (2283098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.89/6.30 % (2283098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.89/6.30 % (2283098)CaDiCaL version: 2.1.3 % 41.89/6.30 % (2283098)Termination reason: Instruction limit % 41.89/6.30 % (2283098)Termination phase: Saturation % 41.89/6.30 % (2283098)Time elapsed: 1.190 s % 41.89/6.30 % (2283098)Peak memory usage: 20 MB % 41.89/6.30 % (2283098)Instructions burned: 1179 (million) % 41.89/6.30 % (2283125)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1843632967:i=54282_2985 on theBenchmark for (2985ds/54282Mi) % 41.89/6.30 % (2283125)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.89/6.30 % (2283125)Terminated due to inappropriate strategy. % 41.89/6.30 % (2283125)------------------------------ % 41.89/6.30 % (2283125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.89/6.30 % (2283125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.89/6.30 % (2283125)CaDiCaL version: 2.1.3 % 41.89/6.30 % (2283125)Termination reason: Inappropriate % 41.89/6.30 % (2283125)Time elapsed: 0.005 s % 41.89/6.30 % (2283125)Peak memory usage: 11 MB % 41.89/6.30 % (2283125)Instructions burned: 4 (million) % 130.78/18.77 % (2283125)------------------------------ % 130.78/18.77 % (2283125)------------------------------ % 130.78/18.77 % (2283127)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3346491549:i=3512:aac=none_2984 on theBenchmark for (2984ds/3512Mi) % 130.78/18.77 % (2283121)Instruction limit reached! % 130.78/18.77 % (2283121)------------------------------ % 130.78/18.77 % (2283121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.78/18.77 % (2283121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.78/18.77 % (2283121)CaDiCaL version: 2.1.3 % 130.78/18.77 % (2283121)Termination reason: Instruction limit % 130.78/18.77 % (2283121)Termination phase: Saturation % 130.78/18.77 % (2283121)Time elapsed: 0.910 s % 130.78/18.77 % (2283121)Peak memory usage: 18 MB % 130.78/18.77 % (2283121)Instructions burned: 869 (million) % 130.78/18.77 % (2283129)dis+21_1_sil=32000:sas=cadical:random_seed=917270868:i=3773:amm=off_2979 on theBenchmark for (2979ds/3773Mi) % 130.78/18.77 % (2283115)Instruction limit reached! % 130.78/18.77 % (2283115)------------------------------ % 130.78/18.77 % (2283115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.78/18.77 % (2283115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.78/18.77 % (2283115)CaDiCaL version: 2.1.3 % 130.78/18.77 % (2283115)Termination reason: Instruction limit % 130.78/18.77 % (2283115)Termination phase: Saturation % 130.78/18.77 % (2283115)Time elapsed: 1.420 s % 130.78/18.77 % (2283115)Peak memory usage: 25 MB % 130.78/18.77 % (2283115)Instructions burned: 1472 (million) % 130.78/18.77 % (2283133)ott+11_1_sil=16000:gs=on:random_seed=1116406196:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi) % 130.78/18.77 % (2283113)Instruction limit reached! % 130.78/18.77 % (2283113)------------------------------ % 130.78/18.77 % (2283113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.78/18.77 % (2283113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.78/18.77 % (2283113)CaDiCaL version: 2.1.3 % 130.78/18.77 % (2283113)Termination reason: Instruction limit % 130.78/18.77 % (2283113)Termination phase: Saturation % 130.78/18.77 % (2283113)Time elapsed: 2.582 s % 130.78/18.77 % (2283113)Peak memory usage: 42 MB % 130.78/18.77 % (2283113)Instructions burned: 5131 (million) % 130.78/18.77 % (2283135)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=751920013:fmbsr=1.6:i=67534_2968 on theBenchmark for (2968ds/67534Mi) % 130.78/18.77 % (2283135)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.78/18.77 % (2283135)Terminated due to inappropriate strategy. % 130.78/18.77 % (2283135)------------------------------ % 130.78/18.77 % (2283135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.78/18.77 % (2283135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.78/18.77 % (2283135)CaDiCaL version: 2.1.3 % 130.78/18.77 % (2283135)Termination reason: Inappropriate % 130.78/18.77 % (2283135)Time elapsed: 0.002 s % 130.78/18.77 % (2283135)Peak memory usage: 10 MB % 130.78/18.77 % (2283135)Instructions burned: 4 (million) % 130.78/18.77 % (2283135)------------------------------ % 130.78/18.77 % (2283135)------------------------------ % 130.78/18.77 % (2283137)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1506688767:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2968 on theBenchmark for (2968ds/4591Mi) % 130.78/18.77 % (2283133)Instruction limit reached! % 130.78/18.77 % (2283133)------------------------------ % 130.78/18.77 % (2283133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.78/18.77 % (2283133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.78/18.77 % (2283133)CaDiCaL version: 2.1.3 % 130.78/18.77 % (2283133)Termination reason: Instruction limit % 130.78/18.77 % (2283133)Termination phase: Saturation % 130.78/18.77 % (2283133)Time elapsed: 1.938 s % 130.78/18.77 % (2283133)Peak memory usage: 18 MB % 130.78/18.77 % (2283133)Instructions burned: 2251 (million) % 130.78/18.77 % (2283139)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3160224203:i=29340_2959 on theBenchmark for (2959ds/29340Mi) % 130.78/18.77 % (2283127)Instruction limit reached! % 130.78/18.77 % (2283127)------------------------------ % 130.78/18.77 % (2283127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.78/18.77 % (2283127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.78/18.77 % (2283127)CaDiCaL version: 2.1.3 % 130.78/18.77 % (2283127)Termination reason: Instruction limit % 162.72/23.30 % (2283127)Termination phase: Saturation % 162.72/23.30 % (2283127)Time elapsed: 3.333 s % 162.72/23.30 % (2283127)Peak memory usage: 33 MB % 162.72/23.30 % (2283127)Instructions burned: 3513 (million) % 162.72/23.30 % (2283141)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=968565314:i=5211_2951 on theBenchmark for (2951ds/5211Mi) % 162.72/23.30 % (2283137)Instruction limit reached! % 162.72/23.30 % (2283137)------------------------------ % 162.72/23.30 % (2283137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.72/23.30 % (2283137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.72/23.30 % (2283137)CaDiCaL version: 2.1.3 % 162.72/23.30 % (2283137)Termination reason: Instruction limit % 162.72/23.30 % (2283137)Termination phase: Saturation % 162.72/23.30 % (2283137)Time elapsed: 2.153 s % 162.72/23.30 % (2283137)Peak memory usage: 38 MB % 162.72/23.30 % (2283137)Instructions burned: 4594 (million) % 162.72/23.30 % (2283145)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1841316032:i=5497:nm=2_2946 on theBenchmark for (2946ds/5497Mi) % 162.72/23.30 % (2283145)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 162.72/23.30 % (2283145)Terminated due to inappropriate strategy. % 162.72/23.30 % (2283145)------------------------------ % 162.72/23.30 % (2283145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.72/23.30 % (2283145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.72/23.30 % (2283145)CaDiCaL version: 2.1.3 % 162.72/23.30 % (2283145)Termination reason: Inappropriate % 162.72/23.30 % (2283145)Time elapsed: 0.003 s % 162.72/23.30 % (2283145)Peak memory usage: 10 MB % 162.72/23.30 % (2283145)Instructions burned: 4 (million) % 162.72/23.30 % (2283145)------------------------------ % 162.72/23.30 % (2283145)------------------------------ % 162.72/23.30 % (2283147)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3264296430:fmbsr=2:i=46332_2946 on theBenchmark for (2946ds/46332Mi) % 162.72/23.30 % (2283147)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 162.72/23.30 % (2283147)Terminated due to inappropriate strategy. % 162.72/23.30 % (2283147)------------------------------ % 162.72/23.30 % (2283147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.72/23.30 % (2283147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.72/23.30 % (2283147)CaDiCaL version: 2.1.3 % 162.72/23.30 % (2283147)Termination reason: Inappropriate % 162.72/23.30 % (2283147)Time elapsed: 0.002 s % 162.72/23.30 % (2283147)Peak memory usage: 10 MB % 162.72/23.30 % (2283147)Instructions burned: 4 (million) % 162.72/23.30 % (2283147)------------------------------ % 162.72/23.30 % (2283147)------------------------------ % 162.72/23.30 % (2283149)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1479825501:i=14071_2945 on theBenchmark for (2945ds/14071Mi) % 162.72/23.30 % (2283149)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 162.72/23.30 % (2283149)Terminated due to inappropriate strategy. % 162.72/23.30 % (2283149)------------------------------ % 162.72/23.30 % (2283149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.72/23.30 % (2283149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.72/23.30 % (2283149)CaDiCaL version: 2.1.3 % 162.72/23.30 % (2283149)Termination reason: Inappropriate % 162.72/23.30 % (2283149)Time elapsed: 0.003 s % 162.72/23.30 % (2283149)Peak memory usage: 11 MB % 162.72/23.30 % (2283149)Instructions burned: 4 (million) % 162.72/23.30 % (2283149)------------------------------ % 162.72/23.30 % (2283149)------------------------------ % 162.72/23.30 % (2283151)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1857199661:i=22565:add=on:rawr=on_2945 on theBenchmark for (2945ds/22565Mi) % 162.72/23.30 % (2283129)Instruction limit reached! % 162.72/23.30 % (2283129)------------------------------ % 162.72/23.30 % (2283129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.72/23.30 % (2283129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.72/23.30 % (2283129)CaDiCaL version: 2.1.3 % 162.72/23.30 % (2283129)Termination reason: Instruction limit % 162.72/23.30 % (2283129)Termination phase: Saturation % 162.72/23.30 % (2283129)Time elapsed: 3.546 s % 162.72/23.30 % (2283129)Peak memory usage: 32 MB % 162.72/23.30 % (2283129)Instructions burned: 3774 (million) % 162.72/23.30 % (2283153)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2834334284:i=8173:av=off_2943 on theBenchmark for (2943ds/8173Mi) % 162.72/23.30 % (2283123)Instruction limit reached! % 164.16/23.41 % (2283123)------------------------------ % 164.16/23.41 % (2283123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.16/23.41 % (2283123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.16/23.41 % (2283123)CaDiCaL version: 2.1.3 % 164.16/23.41 % (2283123)Termination reason: Instruction limit % 164.16/23.41 % (2283123)Termination phase: Saturation % 164.16/23.41 % (2283123)Time elapsed: 4.769 s % 164.16/23.41 % (2283123)Peak memory usage: 34 MB % 164.16/23.41 % (2283123)Instructions burned: 5114 (million) % 164.16/23.41 % (2283159)dis+10_16:1_sil=16000:random_seed=2191359679:i=9155:fsr=off_2940 on theBenchmark for (2940ds/9155Mi) % 164.16/23.41 % (2283141)Instruction limit reached! % 164.16/23.41 % (2283141)------------------------------ % 164.16/23.41 % (2283141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.16/23.41 % (2283141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.16/23.41 % (2283141)CaDiCaL version: 2.1.3 % 164.16/23.41 % (2283141)Termination reason: Instruction limit % 164.16/23.41 % (2283141)Termination phase: Saturation % 164.16/23.41 % (2283141)Time elapsed: 4.738 s % 164.16/23.41 % (2283141)Peak memory usage: 53 MB % 164.16/23.41 % (2283141)Instructions burned: 5211 (million) % 164.16/23.41 % (2283163)ott-3_8_sil=64000:random_seed=2685274:i=20139:bs=on_2903 on theBenchmark for (2903ds/20139Mi) % 164.16/23.41 % (2283153)Instruction limit reached! % 164.16/23.41 % (2283153)------------------------------ % 164.16/23.41 % (2283153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.16/23.41 % (2283153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.16/23.41 % (2283153)CaDiCaL version: 2.1.3 % 164.16/23.41 % (2283153)Termination reason: Instruction limit % 164.16/23.41 % (2283153)Termination phase: Saturation % 164.16/23.41 % (2283153)Time elapsed: 7.875 s % 164.16/23.41 % (2283153)Peak memory usage: 60 MB % 164.16/23.41 % (2283153)Instructions burned: 8174 (million) % 164.16/23.41 % (2283217)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3036977654:fmbsr=2:i=32576_2864 on theBenchmark for (2864ds/32576Mi) % 164.16/23.41 % (2283217)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 164.16/23.41 % (2283217)Terminated due to inappropriate strategy. % 164.16/23.41 % (2283217)------------------------------ % 164.16/23.41 % (2283217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.16/23.41 % (2283217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.16/23.41 % (2283217)CaDiCaL version: 2.1.3 % 164.16/23.41 % (2283217)Termination reason: Inappropriate % 164.16/23.41 % (2283217)Time elapsed: 0.003 s % 164.16/23.41 % (2283217)Peak memory usage: 11 MB % 164.16/23.41 % (2283217)Instructions burned: 5 (million) % 164.16/23.41 % (2283217)------------------------------ % 164.16/23.41 % (2283217)------------------------------ % 164.16/23.41 % (2283219)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3776043242:i=11404_2864 on theBenchmark for (2864ds/11404Mi) % 164.16/23.41 % (2283151)Instruction limit reached! % 164.16/23.41 % (2283151)------------------------------ % 164.16/23.41 % (2283151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.16/23.41 % (2283151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.16/23.41 % (2283151)CaDiCaL version: 2.1.3 % 164.16/23.41 % (2283151)Termination reason: Instruction limit % 164.16/23.41 % (2283151)Termination phase: Saturation % 164.16/23.41 % (2283151)Time elapsed: 8.146 s % 164.16/23.41 % (2283151)Peak memory usage: 23 MB % 164.16/23.41 % (2283151)Instructions burned: 22568 (million) % 164.16/23.41 % (2283221)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3395455673:i=14134_2863 on theBenchmark for (2863ds/14134Mi) % 164.16/23.41 % (2283159)Instruction limit reached! % 164.16/23.41 % (2283159)------------------------------ % 164.16/23.41 % (2283159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.16/23.41 % (2283159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.16/23.41 % (2283159)CaDiCaL version: 2.1.3 % 164.16/23.41 % (2283159)Termination reason: Instruction limit % 164.16/23.41 % (2283159)Termination phase: Saturation % 164.16/23.41 % (2283159)Time elapsed: 7.698 s % 164.16/23.41 % (2283159)Peak memory usage: 51 MB % 164.16/23.41 % (2283159)Instructions burned: 9156 (million) % 164.16/23.41 % (2283223)dis+33_16_sil=32000:sac=on:random_seed=3578729976:i=15851:nm=0_2862 on theBenchmark for (2862ds/15851Mi) % 164.16/23.41 % (2283221)Instruction limit reached! % 164.16/23.41 % (2283221)------------------------------ % 164.16/23.41 % (2283221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.63/25.30 % (2283221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.63/25.30 % (2283221)CaDiCaL version: 2.1.3 % 177.63/25.30 % (2283221)Termination reason: Instruction limit % 177.63/25.30 % (2283221)Termination phase: Saturation % 177.63/25.30 % (2283221)Time elapsed: 4.830 s % 177.63/25.30 % (2283221)Peak memory usage: 84 MB % 177.63/25.30 % (2283221)Instructions burned: 14135 (million) % 177.63/25.30 % (2283226)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3413163663:avsq=on:i=17627:add=on:amm=off_2815 on theBenchmark for (2815ds/17627Mi) % 177.63/25.30 % (2283219)Instruction limit reached! % 177.63/25.30 % (2283219)------------------------------ % 177.63/25.30 % (2283219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.63/25.30 % (2283219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.63/25.30 % (2283219)CaDiCaL version: 2.1.3 % 177.63/25.30 % (2283219)Termination reason: Instruction limit % 177.63/25.30 % (2283219)Termination phase: Saturation % 177.63/25.30 % (2283219)Time elapsed: 7.285 s % 177.63/25.30 % (2283219)Peak memory usage: 82 MB % 177.63/25.30 % (2283219)Instructions burned: 11405 (million) % 177.63/25.30 % (2283228)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4221254707:s2a=on:i=53295_2791 on theBenchmark for (2791ds/53295Mi) % 177.63/25.30 % (2283226)Instruction limit reached! % 177.63/25.30 % (2283226)------------------------------ % 177.63/25.30 % (2283226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.63/25.30 % (2283226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.63/25.30 % (2283226)CaDiCaL version: 2.1.3 % 177.63/25.30 % (2283226)Termination reason: Instruction limit % 177.63/25.30 % (2283226)Termination phase: Saturation % 177.63/25.30 % (2283226)Time elapsed: 3.965 s % 177.63/25.30 % (2283226)Peak memory usage: 108 MB % 177.63/25.30 % (2283226)Instructions burned: 17632 (million) % 177.63/25.30 % (2283230)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=16608672:i=26857:ins=20_2775 on theBenchmark for (2775ds/26857Mi) % 177.63/25.30 % (2283230)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.63/25.30 % (2283230)Terminated due to inappropriate strategy. % 177.63/25.30 % (2283230)------------------------------ % 177.63/25.30 % (2283230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.63/25.30 % (2283230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.63/25.30 % (2283230)CaDiCaL version: 2.1.3 % 177.63/25.30 % (2283230)Termination reason: Inappropriate % 177.63/25.30 % (2283230)Time elapsed: 0.001 s % 177.63/25.30 % (2283230)Peak memory usage: 10 MB % 177.63/25.30 % (2283230)Instructions burned: 4 (million) % 177.63/25.30 % (2283230)------------------------------ % 177.63/25.30 % (2283230)------------------------------ % 177.63/25.30 % (2283232)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=49348097:i=28120:bs=on:fsr=off_2775 on theBenchmark for (2775ds/28120Mi) % 177.63/25.30 % (2283139)Instruction limit reached! % 177.63/25.30 % (2283139)------------------------------ % 177.63/25.30 % (2283139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.63/25.30 % (2283139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.63/25.30 % (2283139)CaDiCaL version: 2.1.3 % 177.63/25.30 % (2283139)Termination reason: Instruction limit % 177.63/25.30 % (2283139)Termination phase: Saturation % 177.63/25.30 % (2283139)Time elapsed: 18.813 s % 177.63/25.30 % (2283139)Peak memory usage: 118 MB % 177.63/25.30 % (2283139)Instructions burned: 29340 (million) % 177.63/25.30 % (2283234)fmb+10_1_sil=256000:fmbss=7:random_seed=3280994533:fmbsr=1.6:i=182295_2770 on theBenchmark for (2770ds/182295Mi) % 177.63/25.30 % (2283234)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.63/25.30 % (2283234)Terminated due to inappropriate strategy. % 177.63/25.30 % (2283234)------------------------------ % 177.63/25.30 % (2283234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.63/25.30 % (2283234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.63/25.30 % (2283234)CaDiCaL version: 2.1.3 % 177.63/25.30 % (2283234)Termination reason: Inappropriate % 177.63/25.30 % (2283234)Time elapsed: 0.002 s % 177.63/25.30 % (2283234)Peak memory usage: 10 MB % 177.63/25.30 % (2283234)Instructions burned: 4 (million) % 177.63/25.30 % (2283234)------------------------------ % 177.63/25.30 % (2283234)------------------------------ % 177.63/25.30 % (2283236)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=526253882:i=44625:gsp=on_2770 on theBenchmark for (2770ds/44625Mi) % 190.68/27.19 % (2283236)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.68/27.19 % (2283236)Terminated due to inappropriate strategy. % 190.68/27.19 % (2283236)------------------------------ % 190.68/27.19 % (2283236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.68/27.19 % (2283236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.68/27.19 % (2283236)CaDiCaL version: 2.1.3 % 190.68/27.19 % (2283236)Termination reason: Inappropriate % 190.68/27.19 % (2283236)Time elapsed: 0.003 s % 190.68/27.19 % (2283236)Peak memory usage: 11 MB % 190.68/27.19 % (2283236)Instructions burned: 4 (million) % 190.68/27.19 % (2283236)------------------------------ % 190.68/27.19 % (2283236)------------------------------ % 190.68/27.19 % (2283238)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1358078013:i=160505_2770 on theBenchmark for (2770ds/160505Mi) % 190.68/27.19 % (2283238)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.68/27.19 % (2283238)Terminated due to inappropriate strategy. % 190.68/27.19 % (2283238)------------------------------ % 190.68/27.19 % (2283238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.68/27.19 % (2283238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.68/27.19 % (2283238)CaDiCaL version: 2.1.3 % 190.68/27.19 % (2283238)Termination reason: Inappropriate % 190.68/27.19 % (2283238)Time elapsed: 0.002 s % 190.68/27.19 % (2283238)Peak memory usage: 10 MB % 190.68/27.19 % (2283238)Instructions burned: 4 (million) % 190.68/27.19 % (2283238)------------------------------ % 190.68/27.19 % (2283238)------------------------------ % 190.68/27.19 % (2283240)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2882557681:fmbsr=1.3:i=225729_2769 on theBenchmark for (2769ds/225729Mi) % 190.68/27.19 % (2283240)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.68/27.19 % (2283240)Terminated due to inappropriate strategy. % 190.68/27.19 % (2283240)------------------------------ % 190.68/27.19 % (2283240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.68/27.19 % (2283240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.68/27.19 % (2283240)CaDiCaL version: 2.1.3 % 190.68/27.19 % (2283240)Termination reason: Inappropriate % 190.68/27.19 % (2283240)Time elapsed: 0.002 s % 190.68/27.19 % (2283240)Peak memory usage: 10 MB % 190.68/27.19 % (2283240)Instructions burned: 4 (million) % 190.68/27.19 % (2283240)------------------------------ % 190.68/27.19 % (2283240)------------------------------ % 190.68/27.19 % (2283242)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1531846107:fmbsr=2:i=185024:ins=7_2769 on theBenchmark for (2769ds/185024Mi) % 190.68/27.19 % (2283242)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.68/27.19 % (2283242)Terminated due to inappropriate strategy. % 190.68/27.19 % (2283242)------------------------------ % 190.68/27.19 % (2283242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.68/27.19 % (2283242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.68/27.19 % (2283242)CaDiCaL version: 2.1.3 % 190.68/27.19 % (2283242)Termination reason: Inappropriate % 190.68/27.19 % (2283242)Time elapsed: 0.002 s % 190.68/27.19 % (2283242)Peak memory usage: 10 MB % 190.68/27.19 % (2283242)Instructions burned: 4 (million) % 190.68/27.19 % (2283242)------------------------------ % 190.68/27.19 % (2283242)------------------------------ % 190.68/27.19 % (2283244)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3918584984:rtra=on_2769 on theBenchmark for (2769ds/0Mi) % 190.68/27.19 % (2283244)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.68/27.19 % (2283244)Terminated due to inappropriate strategy. % 190.68/27.19 % (2283244)------------------------------ % 190.68/27.19 % (2283244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.68/27.19 % (2283244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.68/27.19 % (2283244)CaDiCaL version: 2.1.3 % 190.68/27.19 % (2283244)Termination reason: Inappropriate % 190.68/27.19 % (2283244)Time elapsed: 0.003 s % 190.68/27.19 % (2283244)Peak memory usage: 11 MB % 190.68/27.19 % (2283244)Instructions burned: 5 (million) % 190.68/27.19 % (2283244)------------------------------ % 190.68/27.19 % (2283244)------------------------------ % 190.68/27.19 % (2283246)% WARNING: option uhcvi not known. % 190.68/27.19 % (2283246)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=17161507:i=271062:add=off:rtra=on:rawr=on_2769 on theBenchmark for (2769ds/271062Mi) % 213.82/30.44 % (2283223)Instruction limit reached! % 213.82/30.44 % (2283223)------------------------------ % 213.82/30.44 % (2283223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.82/30.44 % (2283223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.82/30.44 % (2283223)CaDiCaL version: 2.1.3 % 213.82/30.44 % (2283223)Termination reason: Instruction limit % 213.82/30.44 % (2283223)Termination phase: Saturation % 213.82/30.44 % (2283223)Time elapsed: 9.463 s % 213.82/30.44 % (2283223)Peak memory usage: 101 MB % 213.82/30.44 % (2283223)Instructions burned: 15852 (million) % 213.82/30.44 % (2283248)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4006915308:i=176048:add=on:rtra=on:rawr=on_2767 on theBenchmark for (2767ds/176048Mi) % 213.82/30.44 % (2283163)Instruction limit reached! % 213.82/30.44 % (2283163)------------------------------ % 213.82/30.44 % (2283163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.82/30.44 % (2283163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.82/30.44 % (2283163)CaDiCaL version: 2.1.3 % 213.82/30.44 % (2283163)Termination reason: Instruction limit % 213.82/30.44 % (2283163)Termination phase: Saturation % 213.82/30.44 % (2283163)Time elapsed: 14.521 s % 213.82/30.44 % (2283163)Peak memory usage: 121 MB % 213.82/30.44 % (2283163)Instructions burned: 20140 (million) % 213.82/30.44 % (2283250)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4075568322:i=206:fgj=on:rtra=on_2757 on theBenchmark for (2757ds/206Mi) % 213.82/30.44 % (2283250)Instruction limit reached! % 213.82/30.44 % (2283250)------------------------------ % 213.82/30.44 % (2283250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.82/30.44 % (2283250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.82/30.44 % (2283250)CaDiCaL version: 2.1.3 % 213.82/30.44 % (2283250)Termination reason: Instruction limit % 213.82/30.44 % (2283250)Termination phase: Saturation % 213.82/30.44 % (2283250)Time elapsed: 0.130 s % 213.82/30.44 % (2283250)Peak memory usage: 13 MB % 213.82/30.44 % (2283250)Instructions burned: 207 (million) % 213.82/30.44 % (2283252)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1951735653:i=232:rtra=on_2756 on theBenchmark for (2756ds/232Mi) % 213.82/30.44 % (2283252)Instruction limit reached! % 213.82/30.44 % (2283252)------------------------------ % 213.82/30.44 % (2283252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.82/30.44 % (2283252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.82/30.44 % (2283252)CaDiCaL version: 2.1.3 % 213.82/30.44 % (2283252)Termination reason: Instruction limit % 213.82/30.44 % (2283252)Termination phase: Saturation % 213.82/30.44 % (2283252)Time elapsed: 0.150 s % 213.82/30.44 % (2283252)Peak memory usage: 14 MB % 213.82/30.44 % (2283252)Instructions burned: 233 (million) % 213.82/30.44 % (2283254)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2337133887:i=262:rtra=on_2754 on theBenchmark for (2754ds/262Mi) % 213.82/30.44 % (2283254)Instruction limit reached! % 213.82/30.44 % (2283254)------------------------------ % 213.82/30.44 % (2283254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.82/30.44 % (2283254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.82/30.44 % (2283254)CaDiCaL version: 2.1.3 % 213.82/30.44 % (2283254)Termination reason: Instruction limit % 213.82/30.44 % (2283254)Termination phase: Saturation % 213.82/30.44 % (2283254)Time elapsed: 0.166 s % 213.82/30.44 % (2283254)Peak memory usage: 14 MB % 213.82/30.44 % (2283254)Instructions burned: 262 (million) % 213.82/30.44 % (2283256)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3303688406:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2752 on theBenchmark for (2752ds/318Mi) % 213.82/30.44 % (2283256)Instruction limit reached! % 213.82/30.44 % (2283256)------------------------------ % 213.82/30.44 % (2283256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.82/30.44 % (2283256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.82/30.44 % (2283256)CaDiCaL version: 2.1.3 % 213.82/30.44 % (2283256)Termination reason: Instruction limit % 213.82/30.44 % (2283256)Termination phase: Saturation % 213.82/30.44 % (2283256)Time elapsed: 0.222 s % 213.82/30.44 % (2283256)Peak memory usage: 15 MB % 213.82/30.44 % (2283256)Instructions burned: 318 (million) % 213.82/30.44 % (2283258)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2150719493:i=1428:nm=2:rtra=on_2750 on theBenchmark for (2750ds/1428Mi) % 223.78/31.84 % (2283258)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 223.78/31.84 % (2283258)Terminated due to inappropriate strategy. % 223.78/31.84 % (2283258)------------------------------ % 223.78/31.84 % (2283258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.78/31.84 % (2283258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.78/31.84 % (2283258)CaDiCaL version: 2.1.3 % 223.78/31.84 % (2283258)Termination reason: Inappropriate % 223.78/31.84 % (2283258)Time elapsed: 0.003 s % 223.78/31.84 % (2283258)Peak memory usage: 10 MB % 223.78/31.84 % (2283258)Instructions burned: 4 (million) % 223.78/31.84 % (2283258)------------------------------ % 223.78/31.84 % (2283258)------------------------------ % 223.78/31.84 % (2283260)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=4109896050:i=262:bd=preordered:rtra=on:fsd=on_2750 on theBenchmark for (2750ds/262Mi) % 223.78/31.84 % (2283260)Instruction limit reached! % 223.78/31.84 % (2283260)------------------------------ % 223.78/31.84 % (2283260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.78/31.84 % (2283260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.78/31.84 % (2283260)CaDiCaL version: 2.1.3 % 223.78/31.84 % (2283260)Termination reason: Instruction limit % 223.78/31.84 % (2283260)Termination phase: Saturation % 223.78/31.84 % (2283260)Time elapsed: 0.160 s % 223.78/31.84 % (2283260)Peak memory usage: 13 MB % 223.78/31.84 % (2283260)Instructions burned: 262 (million) % 223.78/31.84 % (2283262)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=3307135819:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2748 on theBenchmark for (2748ds/1368Mi) % 223.78/31.84 % (2283262)Instruction limit reached! % 223.78/31.84 % (2283262)------------------------------ % 223.78/31.84 % (2283262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.78/31.84 % (2283262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.78/31.84 % (2283262)CaDiCaL version: 2.1.3 % 223.78/31.84 % (2283262)Termination reason: Instruction limit % 223.78/31.84 % (2283262)Termination phase: Saturation % 223.78/31.84 % (2283262)Time elapsed: 0.824 s % 223.78/31.84 % (2283262)Peak memory usage: 24 MB % 223.78/31.84 % (2283262)Instructions burned: 1369 (million) % 223.78/31.84 % (2283264)ott-21_1_sil=16000:si=on:fs=off:random_seed=3658008547:i=360:av=off:fsr=off:rtra=on_2739 on theBenchmark for (2739ds/360Mi) % 223.78/31.84 % (2283264)Instruction limit reached! % 223.78/31.84 % (2283264)------------------------------ % 223.78/31.84 % (2283264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.78/31.84 % (2283264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.78/31.84 % (2283264)CaDiCaL version: 2.1.3 % 223.78/31.84 % (2283264)Termination reason: Instruction limit % 223.78/31.84 % (2283264)Termination phase: Saturation % 223.78/31.84 % (2283264)Time elapsed: 0.173 s % 223.78/31.84 % (2283264)Peak memory usage: 13 MB % 223.78/31.84 % (2283264)Instructions burned: 361 (million) % 223.78/31.84 % (2283266)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3941640585:i=954:bd=all:rtra=on_2737 on theBenchmark for (2737ds/954Mi) % 223.78/31.84 % (2283266)Instruction limit reached! % 223.78/31.84 % (2283266)------------------------------ % 223.78/31.84 % (2283266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.78/31.84 % (2283266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.78/31.84 % (2283266)CaDiCaL version: 2.1.3 % 223.78/31.84 % (2283266)Termination reason: Instruction limit % 223.78/31.84 % (2283266)Termination phase: Saturation % 223.78/31.84 % (2283266)Time elapsed: 0.620 s % 223.78/31.84 % (2283266)Peak memory usage: 16 MB % 223.78/31.84 % (2283266)Instructions burned: 955 (million) % 223.78/31.84 % (2283268)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2795072858:fmbsr=1.3:i=1730:ins=25:rtra=on_2731 on theBenchmark for (2731ds/1730Mi) % 223.78/31.84 % (2283268)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 223.78/31.84 % (2283268)Terminated due to inappropriate strategy. % 223.78/31.84 % (2283268)------------------------------ % 223.78/31.84 % (2283268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.78/31.84 % (2283268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.78/31.84 % (2283268)CaDiCaL version: 2.1.3 % 223.78/31.84 % (2283268)Termination reason: Inappropriate % 223.78/31.84 % (2283268)Time elapsed: 0.003 s % 279.51/39.78 % (2283268)Peak memory usage: 10 MB % 279.51/39.78 % (2283268)Instructions burned: 4 (million) % 279.51/39.78 % (2283268)------------------------------ % 279.51/39.78 % (2283268)------------------------------ % 279.51/39.78 % (2283270)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4268172731:i=2358:rtra=on_2731 on theBenchmark for (2731ds/2358Mi) % 279.51/39.78 % (2283270)Instruction limit reached! % 279.51/39.78 % (2283270)------------------------------ % 279.51/39.78 % (2283270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.51/39.78 % (2283270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.51/39.78 % (2283270)CaDiCaL version: 2.1.3 % 279.51/39.78 % (2283270)Termination reason: Instruction limit % 279.51/39.78 % (2283270)Termination phase: Saturation % 279.51/39.78 % (2283270)Time elapsed: 1.500 s % 279.51/39.78 % (2283270)Peak memory usage: 25 MB % 279.51/39.78 % (2283270)Instructions burned: 2358 (million) % 279.51/39.78 % (2283272)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=278579675:i=1778:ins=1:rtra=on_2716 on theBenchmark for (2716ds/1778Mi) % 279.51/39.78 % (2283272)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.51/39.78 % (2283272)Terminated due to inappropriate strategy. % 279.51/39.78 % (2283272)------------------------------ % 279.51/39.78 % (2283272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.51/39.78 % (2283272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.51/39.78 % (2283272)CaDiCaL version: 2.1.3 % 279.51/39.78 % (2283272)Termination reason: Inappropriate % 279.51/39.78 % (2283272)Time elapsed: 0.003 s % 279.51/39.78 % (2283272)Peak memory usage: 10 MB % 279.51/39.78 % (2283272)Instructions burned: 5 (million) % 279.51/39.78 % (2283272)------------------------------ % 279.51/39.78 % (2283272)------------------------------ % 279.51/39.78 % (2283274)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=380001908:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2715 on theBenchmark for (2715ds/1384Mi) % 279.51/39.78 % (2283274)Instruction limit reached! % 279.51/39.78 % (2283274)------------------------------ % 279.51/39.78 % (2283274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.51/39.78 % (2283274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.51/39.78 % (2283274)CaDiCaL version: 2.1.3 % 279.51/39.78 % (2283274)Termination reason: Instruction limit % 279.51/39.78 % (2283274)Termination phase: Saturation % 279.51/39.78 % (2283274)Time elapsed: 0.629 s % 279.51/39.78 % (2283274)Peak memory usage: 19 MB % 279.51/39.78 % (2283274)Instructions burned: 1384 (million) % 279.51/39.78 % (2283276)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1288302645:i=1758:kws=inv_precedence:fsr=off:rtra=on_2709 on theBenchmark for (2709ds/1758Mi) % 279.51/39.78 % (2283276)Instruction limit reached! % 279.51/39.78 % (2283276)------------------------------ % 279.51/39.78 % (2283276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.51/39.78 % (2283276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.51/39.78 % (2283276)CaDiCaL version: 2.1.3 % 279.51/39.78 % (2283276)Termination reason: Instruction limit % 279.51/39.78 % (2283276)Termination phase: Saturation % 279.51/39.78 % (2283276)Time elapsed: 0.994 s % 279.51/39.78 % (2283276)Peak memory usage: 25 MB % 279.51/39.78 % (2283276)Instructions burned: 1760 (million) % 279.51/39.78 % (2283278)fmb+10_1_sil=64000:si=on:random_seed=3080782257:i=44122:nm=2:rtra=on:gsp=on_2699 on theBenchmark for (2699ds/44122Mi) % 279.51/39.78 % (2283278)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.51/39.78 % (2283278)Terminated due to inappropriate strategy. % 279.51/39.78 % (2283278)------------------------------ % 279.51/39.78 % (2283278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.51/39.78 % (2283278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.51/39.78 % (2283278)CaDiCaL version: 2.1.3 % 279.51/39.78 % (2283278)Termination reason: Inappropriate % 279.51/39.78 % (2283278)Time elapsed: 0.003 s % 279.51/39.78 % (2283278)Peak memory usage: 10 MB % 279.51/39.78 % (2283278)Instructions burned: 5 (million) % 279.51/39.78 % (2283278)------------------------------ % 279.51/39.78 % (2283278)------------------------------ % 279.51/39.78 % (2283280)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1492554688:i=19030:nm=5:rtra=on_2698 on theBenchmark for (2698ds/19030Mi) % 297.11/42.13 % (2283280)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 297.11/42.13 % (2283280)Terminated due to inappropriate strategy. % 297.11/42.13 % (2283280)------------------------------ % 297.11/42.13 % (2283280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.11/42.13 % (2283280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.11/42.13 % (2283280)CaDiCaL version: 2.1.3 % 297.11/42.13 % (2283280)Termination reason: Inappropriate % 297.11/42.13 % (2283280)Time elapsed: 0.003 s % 297.11/42.13 % (2283280)Peak memory usage: 10 MB % 297.11/42.13 % (2283280)Instructions burned: 4 (million) % 297.11/42.13 % (2283280)------------------------------ % 297.11/42.13 % (2283280)------------------------------ % 297.11/42.13 % (2283282)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1091172003:fmbsr=1.7:i=1840:rtra=on_2698 on theBenchmark for (2698ds/1840Mi) % 297.11/42.13 % (2283282)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 297.11/42.13 % (2283282)Terminated due to inappropriate strategy. % 297.11/42.13 % (2283282)------------------------------ % 297.11/42.13 % (2283282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.11/42.13 % (2283282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.11/42.13 % (2283282)CaDiCaL version: 2.1.3 % 297.11/42.13 % (2283282)Termination reason: Inappropriate % 297.11/42.13 % (2283282)Time elapsed: 0.003 s % 297.11/42.13 % (2283282)Peak memory usage: 10 MB % 297.11/42.13 % (2283282)Instructions burned: 5 (million) % 297.11/42.13 % (2283282)------------------------------ % 297.11/42.13 % (2283282)------------------------------ % 297.11/42.13 % (2283284)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1271302455:i=10262:rtra=on_2698 on theBenchmark for (2698ds/10262Mi) % 297.11/42.13 % (2283232)Instruction limit reached! % 297.11/42.13 % (2283232)------------------------------ % 297.11/42.13 % (2283232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.11/42.13 % (2283232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.11/42.13 % (2283232)CaDiCaL version: 2.1.3 % 297.11/42.13 % (2283232)Termination reason: Instruction limit % 297.11/42.13 % (2283232)Termination phase: Saturation % 297.11/42.13 % (2283232)Time elapsed: 8.073 s % 297.11/42.13 % (2283232)Peak memory usage: 73 MB % 297.11/42.13 % (2283232)Instructions burned: 28123 (million) % 297.11/42.13 % (2283286)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1632648301:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2694 on theBenchmark for (2694ds/2944Mi) % 297.11/42.13 % (2283286)Instruction limit reached! % 297.11/42.13 % (2283286)------------------------------ % 297.11/42.13 % (2283286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.11/42.13 % (2283286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.11/42.13 % (2283286)CaDiCaL version: 2.1.3 % 297.11/42.13 % (2283286)Termination reason: Instruction limit % 297.11/42.13 % (2283286)Termination phase: Saturation % 297.11/42.13 % (2283286)Time elapsed: 0.914 s % 297.11/42.13 % (2283286)Peak memory usage: 36 MB % 297.11/42.13 % (2283286)Instructions burned: 2947 (million) % 297.11/42.13 % (2283288)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2916531954:i=12648:rtra=on_2685 on theBenchmark for (2685ds/12648Mi) % 297.11/42.13 % (2283288)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 297.11/42.13 % (2283288)Terminated due to inappropriate strategy. % 297.11/42.13 % (2283288)------------------------------ % 297.11/42.13 % (2283288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.11/42.13 % (2283288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.11/42.13 % (2283288)CaDiCaL version: 2.1.3 % 297.11/42.13 % (2283288)Termination reason: Inappropriate % 297.11/42.13 % (2283288)Time elapsed: 0.001 s % 297.11/42.13 % (2283288)Peak memory usage: 11 MB % 297.11/42.13 % (2283288)Instructions burned: 5 (million) % 297.11/42.13 % (2283288)------------------------------ % 297.11/42.13 % (2283288)------------------------------ % 297.11/42.13 % (2283290)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2987271130:fmbsr=2.30978:i=4348:rtra=on_2685 on theBenchmark for (2685ds/4348Mi) % 297.11/42.13 % (2283290)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 297.11/42.13 % (2283290)Terminated due to inappropriate strategy. % 297.11/42.13 % (2283290)------------------------------ % 297.11/42.13 % (2283290)Version: VampiTerminated % 300.02/42.63 % Vampire exiting % 300.02/42.64 Terminated %------------------------------------------------------------------------------