%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW034_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n012.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:38:31 PM UTC 2026 % Result : Timeout 294.15s 42.00s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWW034_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.00/0.11 % Computer : n012.cluster.edu % 0.00/0.11 % Model : x86_64 x86_64 % 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.11 % Memory : 8046.5625MB % 0.00/0.11 % OS : Linux 6.8.0-71-generic % 0.00/0.11 % CPULimit : 300 % 0.00/0.11 % WCLimit : 300 % 0.00/0.11 % DateTime : Mon Sep 28 13:09:19 UTC 2026 % 0.00/0.11 % CPUTime : % 0.00/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.13 Running first-order model finding % 0.09/0.13 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 % 2.80/0.55 % (3364157)Will run a generic schedule for satisfiability detection. % 2.80/0.55 % (3364176)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3256047891_2999 on theBenchmark for (2999ds/0Mi) % 2.80/0.55 % (3364177)% WARNING: option uhcvi not known. % 2.80/0.55 % (3364178)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1346823800:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.80/0.55 % (3364177)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2549126975:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.80/0.55 % (3364179)dis+10_1_sil=32000:sp=arity:random_seed=3198174565:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.80/0.55 % (3364180)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2902731659:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.80/0.55 % (3364182)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=587592667:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.80/0.55 % (3364181)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2708956854:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.80/0.55 % (3364176)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.80/0.55 % (3364176)Terminated due to inappropriate strategy. % 2.80/0.55 % (3364176)------------------------------ % 2.80/0.55 % (3364176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.80/0.55 % (3364176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.80/0.55 % (3364176)CaDiCaL version: 2.1.3 % 2.80/0.55 % (3364176)Termination reason: Inappropriate % 2.80/0.55 % (3364176)Time elapsed: 0.019 s % 2.80/0.55 % (3364176)Peak memory usage: 13 MB % 2.80/0.55 % (3364176)Instructions burned: 78 (million) % 2.80/0.55 % (3364176)------------------------------ % 2.80/0.55 % (3364176)------------------------------ % 2.80/0.55 % (3364191)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=989759266:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.80/0.55 % (3364179)Instruction limit reached! % 2.80/0.55 % (3364179)------------------------------ % 2.80/0.55 % (3364179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.80/0.55 % (3364179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.80/0.55 % (3364179)CaDiCaL version: 2.1.3 % 2.80/0.55 % (3364179)Termination reason: Instruction limit % 2.80/0.55 % (3364179)Termination phase: Saturation % 2.80/0.55 % (3364179)Time elapsed: 0.042 s % 2.80/0.55 % (3364179)Peak memory usage: 15 MB % 2.80/0.55 % (3364179)Instructions burned: 104 (million) % 2.80/0.55 % (3364180)Instruction limit reached! % 2.80/0.55 % (3364180)------------------------------ % 2.80/0.55 % (3364180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.80/0.55 % (3364180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.80/0.55 % (3364180)CaDiCaL version: 2.1.3 % 2.80/0.55 % (3364180)Termination reason: Instruction limit % 2.80/0.55 % (3364180)Termination phase: Saturation % 2.80/0.55 % (3364180)Time elapsed: 0.054 s % 2.80/0.55 % (3364180)Peak memory usage: 15 MB % 2.80/0.55 % (3364180)Instructions burned: 117 (million) % 2.80/0.55 % (3364181)Instruction limit reached! % 2.80/0.55 % (3364181)------------------------------ % 2.80/0.55 % (3364181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.80/0.55 % (3364181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.80/0.55 % (3364181)CaDiCaL version: 2.1.3 % 2.80/0.55 % (3364181)Termination reason: Instruction limit % 2.80/0.55 % (3364181)Termination phase: Saturation % 2.80/0.55 % (3364181)Time elapsed: 0.053 s % 2.80/0.55 % (3364181)Peak memory usage: 14 MB % 2.80/0.55 % (3364181)Instructions burned: 134 (million) % 2.80/0.55 % (3364182)Instruction limit reached! % 2.80/0.55 % (3364182)------------------------------ % 2.80/0.55 % (3364182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.80/0.55 % (3364182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.80/0.55 % (3364182)CaDiCaL version: 2.1.3 % 2.80/0.55 % (3364182)Termination reason: Instruction limit % 2.80/0.55 % (3364182)Termination phase: Saturation % 2.80/0.55 % (3364182)Time elapsed: 0.060 s % 2.80/0.55 % (3364182)Peak memory usage: 15 MB % 2.80/0.55 % (3364182)Instructions burned: 159 (million) % 2.80/0.55 % (3364199)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1176644093:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.28/0.64 % (3364191)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.28/0.64 % (3364191)Terminated due to inappropriate strategy. % 3.28/0.64 % (3364191)------------------------------ % 3.28/0.64 % (3364191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.64 % (3364191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.64 % (3364191)CaDiCaL version: 2.1.3 % 3.28/0.64 % (3364191)Termination reason: Inappropriate % 3.28/0.64 % (3364191)Time elapsed: 0.034 s % 3.28/0.64 % (3364191)Peak memory usage: 13 MB % 3.28/0.64 % (3364191)Instructions burned: 78 (million) % 3.28/0.64 % (3364191)------------------------------ % 3.28/0.64 % (3364191)------------------------------ % 3.28/0.64 % (3364202)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=882726294:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.28/0.64 % (3364203)ott-21_1_sil=16000:fs=off:random_seed=1405253166:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.28/0.64 % (3364205)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2458572094:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 3.28/0.64 % (3364207)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1043262991:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 3.28/0.64 % (3364207)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.28/0.64 % (3364207)Terminated due to inappropriate strategy. % 3.28/0.64 % (3364207)------------------------------ % 3.28/0.64 % (3364207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.64 % (3364207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.64 % (3364207)CaDiCaL version: 2.1.3 % 3.28/0.64 % (3364207)Termination reason: Inappropriate % 3.28/0.64 % (3364207)Time elapsed: 0.019 s % 3.28/0.64 % (3364207)Peak memory usage: 13 MB % 3.28/0.64 % (3364207)Instructions burned: 77 (million) % 3.28/0.64 % (3364207)------------------------------ % 3.28/0.64 % (3364207)------------------------------ % 3.28/0.64 % (3364216)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1363459164:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 3.28/0.64 % (3364199)Instruction limit reached! % 3.28/0.64 % (3364199)------------------------------ % 3.28/0.64 % (3364199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.64 % (3364199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.64 % (3364199)CaDiCaL version: 2.1.3 % 3.28/0.64 % (3364199)Termination reason: Instruction limit % 3.28/0.64 % (3364199)Termination phase: Saturation % 3.28/0.64 % (3364199)Time elapsed: 0.054 s % 3.28/0.64 % (3364199)Peak memory usage: 15 MB % 3.28/0.64 % (3364199)Instructions burned: 131 (million) % 3.28/0.64 % (3364218)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1248743291:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 3.28/0.64 % (3364203)Instruction limit reached! % 3.28/0.64 % (3364203)------------------------------ % 3.28/0.64 % (3364203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.64 % (3364203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.64 % (3364203)CaDiCaL version: 2.1.3 % 3.28/0.64 % (3364203)Termination reason: Instruction limit % 3.28/0.64 % (3364203)Termination phase: Saturation % 3.28/0.64 % (3364203)Time elapsed: 0.083 s % 3.28/0.64 % (3364203)Peak memory usage: 15 MB % 3.28/0.64 % (3364203)Instructions burned: 187 (million) % 3.28/0.64 % (3364225)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=2897416971: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) % 3.28/0.64 % (3364218)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.28/0.64 % (3364218)Terminated due to inappropriate strategy. % 3.28/0.64 % (3364218)------------------------------ % 3.28/0.64 % (3364218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.64 % (3364218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.64 % (3364218)CaDiCaL version: 2.1.3 % 3.28/0.64 % (3364218)Termination reason: Inappropriate % 3.28/0.64 % (3364218)Time elapsed: 0.032 s % 3.28/0.64 % (3364218)Peak memory usage: 15 MB % 9.93/1.65 % (3364218)Instructions burned: 109 (million) % 9.93/1.65 % (3364218)------------------------------ % 9.93/1.65 % (3364218)------------------------------ % 9.93/1.65 % (3364227)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1950487478:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 9.93/1.65 % (3364205)Instruction limit reached! % 9.93/1.65 % (3364205)------------------------------ % 9.93/1.65 % (3364205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.93/1.65 % (3364205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.93/1.65 % (3364205)CaDiCaL version: 2.1.3 % 9.93/1.65 % (3364205)Termination reason: Instruction limit % 9.93/1.65 % (3364205)Termination phase: Saturation % 9.93/1.65 % (3364205)Time elapsed: 0.157 s % 9.93/1.65 % (3364205)Peak memory usage: 16 MB % 9.93/1.65 % (3364205)Instructions burned: 478 (million) % 9.93/1.65 % (3364229)fmb+10_1_sil=64000:random_seed=2518227483:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 9.93/1.65 % (3364229)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 9.93/1.65 % (3364229)Terminated due to inappropriate strategy. % 9.93/1.65 % (3364229)------------------------------ % 9.93/1.65 % (3364229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.93/1.65 % (3364229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.93/1.65 % (3364229)CaDiCaL version: 2.1.3 % 9.93/1.65 % (3364229)Termination reason: Inappropriate % 9.93/1.65 % (3364229)Time elapsed: 0.019 s % 9.93/1.65 % (3364229)Peak memory usage: 13 MB % 9.93/1.65 % (3364229)Instructions burned: 86 (million) % 9.93/1.65 % (3364229)------------------------------ % 9.93/1.65 % (3364229)------------------------------ % 9.93/1.65 % (3364231)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2029985606:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 9.93/1.65 % (3364202)Instruction limit reached! % 9.93/1.65 % (3364202)------------------------------ % 9.93/1.65 % (3364202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.93/1.65 % (3364202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.93/1.65 % (3364202)CaDiCaL version: 2.1.3 % 9.93/1.65 % (3364202)Termination reason: Instruction limit % 9.93/1.65 % (3364202)Termination phase: Saturation % 9.93/1.65 % (3364202)Time elapsed: 0.212 s % 9.93/1.65 % (3364202)Peak memory usage: 18 MB % 9.93/1.65 % (3364202)Instructions burned: 687 (million) % 9.93/1.65 % (3364234)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=851060119:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 9.93/1.65 % (3364231)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 9.93/1.65 % (3364231)Terminated due to inappropriate strategy. % 9.93/1.65 % (3364231)------------------------------ % 9.93/1.65 % (3364231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.93/1.65 % (3364231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.93/1.65 % (3364231)CaDiCaL version: 2.1.3 % 9.93/1.65 % (3364231)Termination reason: Inappropriate % 9.93/1.65 % (3364231)Time elapsed: 0.018 s % 9.93/1.65 % (3364231)Peak memory usage: 13 MB % 9.93/1.65 % (3364231)Instructions burned: 78 (million) % 9.93/1.65 % (3364231)------------------------------ % 9.93/1.65 % (3364231)------------------------------ % 9.93/1.65 % (3364240)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2325514476:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 9.93/1.65 % (3364234)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 9.93/1.65 % (3364234)Terminated due to inappropriate strategy. % 9.93/1.65 % (3364234)------------------------------ % 9.93/1.65 % (3364234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.93/1.65 % (3364234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.93/1.65 % (3364234)CaDiCaL version: 2.1.3 % 9.93/1.65 % (3364234)Termination reason: Inappropriate % 9.93/1.65 % (3364234)Time elapsed: 0.018 s % 9.93/1.65 % (3364234)Peak memory usage: 13 MB % 9.93/1.65 % (3364234)Instructions burned: 78 (million) % 9.93/1.65 % (3364234)------------------------------ % 9.93/1.65 % (3364234)------------------------------ % 9.93/1.65 % (3364247)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=724599367:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 9.93/1.65 % (3364225)Instruction limit reached! % 9.93/1.65 % (3364225)------------------------------ % 14.28/2.23 % (3364225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.28/2.23 % (3364225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.28/2.23 % (3364225)CaDiCaL version: 2.1.3 % 14.28/2.23 % (3364225)Termination reason: Instruction limit % 14.28/2.23 % (3364225)Termination phase: Saturation % 14.28/2.23 % (3364225)Time elapsed: 0.216 s % 14.28/2.23 % (3364225)Peak memory usage: 22 MB % 14.28/2.23 % (3364225)Instructions burned: 692 (million) % 14.28/2.23 % (3364278)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=579428885:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 14.28/2.23 % (3364278)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 14.28/2.23 % (3364278)Terminated due to inappropriate strategy. % 14.28/2.23 % (3364278)------------------------------ % 14.28/2.23 % (3364278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.28/2.23 % (3364278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.28/2.23 % (3364278)CaDiCaL version: 2.1.3 % 14.28/2.23 % (3364278)Termination reason: Inappropriate % 14.28/2.23 % (3364278)Time elapsed: 0.018 s % 14.28/2.23 % (3364278)Peak memory usage: 13 MB % 14.28/2.23 % (3364278)Instructions burned: 78 (million) % 14.28/2.23 % (3364216)Instruction limit reached! % 14.28/2.23 % (3364216)------------------------------ % 14.28/2.23 % (3364216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.28/2.23 % (3364216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.28/2.23 % (3364216)CaDiCaL version: 2.1.3 % 14.28/2.23 % (3364216)Termination reason: Instruction limit % 14.28/2.23 % (3364216)Termination phase: Saturation % 14.28/2.23 % (3364216)Time elapsed: 0.303 s % 14.28/2.23 % (3364216)Peak memory usage: 19 MB % 14.28/2.23 % (3364216)Instructions burned: 1179 (million) % 14.28/2.23 % (3364278)------------------------------ % 14.28/2.23 % (3364278)------------------------------ % 14.28/2.23 % (3364285)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1957797502:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 14.28/2.23 % (3364286)ott-2_1_sil=16000:newcnf=on:random_seed=2230543192:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi) % 14.28/2.23 % (3364227)Instruction limit reached! % 14.28/2.23 % (3364227)------------------------------ % 14.28/2.23 % (3364227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.28/2.23 % (3364227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.28/2.23 % (3364227)CaDiCaL version: 2.1.3 % 14.28/2.23 % (3364227)Termination reason: Instruction limit % 14.28/2.23 % (3364227)Termination phase: Saturation % 14.28/2.23 % (3364227)Time elapsed: 0.259 s % 14.28/2.23 % (3364227)Peak memory usage: 21 MB % 14.28/2.23 % (3364227)Instructions burned: 879 (million) % 14.28/2.23 % (3364285)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 14.28/2.23 % (3364285)Terminated due to inappropriate strategy. % 14.28/2.23 % (3364285)------------------------------ % 14.28/2.23 % (3364285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.28/2.23 % (3364285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.28/2.23 % (3364285)CaDiCaL version: 2.1.3 % 14.28/2.23 % (3364285)Termination reason: Inappropriate % 14.28/2.23 % (3364285)Time elapsed: 0.017 s % 14.28/2.23 % (3364285)Peak memory usage: 13 MB % 14.28/2.23 % (3364285)Instructions burned: 78 (million) % 14.28/2.23 % (3364285)------------------------------ % 14.28/2.23 % (3364285)------------------------------ % 14.28/2.23 % (3364296)ott+10_1_sil=32000:tgt=ground:random_seed=1646703089:i=5114:av=off_2995 on theBenchmark for (2995ds/5114Mi) % 14.28/2.23 % (3364298)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=739716692:i=54282_2995 on theBenchmark for (2995ds/54282Mi) % 14.28/2.23 % (3364298)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 14.28/2.23 % (3364298)Terminated due to inappropriate strategy. % 14.28/2.23 % (3364298)------------------------------ % 14.28/2.23 % (3364298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.28/2.23 % (3364298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.28/2.23 % (3364298)CaDiCaL version: 2.1.3 % 14.28/2.23 % (3364298)Termination reason: Inappropriate % 14.28/2.23 % (3364298)Time elapsed: 0.017 s % 14.28/2.23 % (3364298)Peak memory usage: 13 MB % 14.28/2.23 % (3364298)Instructions burned: 79 (million) % 56.20/8.16 % (3364298)------------------------------ % 56.20/8.16 % (3364298)------------------------------ % 56.20/8.16 % (3364315)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=984125946:i=3512:aac=none_2994 on theBenchmark for (2994ds/3512Mi) % 56.20/8.16 % (3364247)Instruction limit reached! % 56.20/8.16 % (3364247)------------------------------ % 56.20/8.16 % (3364247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.20/8.16 % (3364247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.20/8.16 % (3364247)CaDiCaL version: 2.1.3 % 56.20/8.16 % (3364247)Termination reason: Instruction limit % 56.20/8.16 % (3364247)Termination phase: Saturation % 56.20/8.16 % (3364247)Time elapsed: 0.283 s % 56.20/8.16 % (3364247)Peak memory usage: 18 MB % 56.20/8.16 % (3364247)Instructions burned: 1473 (million) % 56.20/8.16 % (3364342)dis+21_1_sil=32000:sas=cadical:random_seed=255382987:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi) % 56.20/8.16 % (3364286)Instruction limit reached! % 56.20/8.16 % (3364286)------------------------------ % 56.20/8.16 % (3364286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.20/8.16 % (3364286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.20/8.16 % (3364286)CaDiCaL version: 2.1.3 % 56.20/8.16 % (3364286)Termination reason: Instruction limit % 56.20/8.16 % (3364286)Termination phase: Saturation % 56.20/8.16 % (3364286)Time elapsed: 0.248 s % 56.20/8.16 % (3364286)Peak memory usage: 20 MB % 56.20/8.16 % (3364286)Instructions burned: 869 (million) % 56.20/8.16 % (3364358)ott+11_1_sil=16000:gs=on:random_seed=544773854:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2992 on theBenchmark for (2992ds/2251Mi) % 56.20/8.16 % (3364358)Instruction limit reached! % 56.20/8.16 % (3364358)------------------------------ % 56.20/8.16 % (3364358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.20/8.16 % (3364358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.20/8.16 % (3364358)CaDiCaL version: 2.1.3 % 56.20/8.16 % (3364358)Termination reason: Instruction limit % 56.20/8.16 % (3364358)Termination phase: Saturation % 56.20/8.16 % (3364358)Time elapsed: 0.458 s % 56.20/8.16 % (3364358)Peak memory usage: 18 MB % 56.20/8.16 % (3364358)Instructions burned: 2255 (million) % 56.20/8.16 % (3364407)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=204791288:fmbsr=1.6:i=67534_2988 on theBenchmark for (2988ds/67534Mi) % 56.20/8.16 % (3364407)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 56.20/8.16 % (3364407)Terminated due to inappropriate strategy. % 56.20/8.16 % (3364407)------------------------------ % 56.20/8.16 % (3364407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.20/8.16 % (3364407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.20/8.16 % (3364407)CaDiCaL version: 2.1.3 % 56.20/8.16 % (3364407)Termination reason: Inappropriate % 56.20/8.16 % (3364407)Time elapsed: 0.023 s % 56.20/8.16 % (3364407)Peak memory usage: 13 MB % 56.20/8.16 % (3364407)Instructions burned: 106 (million) % 56.20/8.16 % (3364407)------------------------------ % 56.20/8.16 % (3364407)------------------------------ % 56.20/8.16 % (3364409)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=461193496:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2987 on theBenchmark for (2987ds/4591Mi) % 56.20/8.16 % (3364315)Instruction limit reached! % 56.20/8.16 % (3364315)------------------------------ % 56.20/8.16 % (3364315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.20/8.16 % (3364315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.20/8.16 % (3364315)CaDiCaL version: 2.1.3 % 56.20/8.16 % (3364315)Termination reason: Instruction limit % 56.20/8.16 % (3364315)Termination phase: Saturation % 56.20/8.16 % (3364315)Time elapsed: 0.884 s % 56.20/8.16 % (3364315)Peak memory usage: 24 MB % 56.20/8.16 % (3364315)Instructions burned: 3515 (million) % 56.20/8.16 % (3364411)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1570045177:i=29340_2985 on theBenchmark for (2985ds/29340Mi) % 56.20/8.16 % (3364342)Instruction limit reached! % 56.20/8.16 % (3364342)------------------------------ % 56.20/8.16 % (3364342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.20/8.16 % (3364342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.20/8.16 % (3364342)CaDiCaL version: 2.1.3 % 56.20/8.16 % (3364342)Termination reason: Instruction limit % 65.21/9.48 % (3364342)Termination phase: Saturation % 65.21/9.48 % (3364342)Time elapsed: 0.862 s % 65.21/9.48 % (3364342)Peak memory usage: 24 MB % 65.21/9.48 % (3364342)Instructions burned: 3775 (million) % 65.21/9.48 % (3364413)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4091997341:i=5211_2984 on theBenchmark for (2984ds/5211Mi) % 65.21/9.48 % (3364240)Instruction limit reached! % 65.21/9.48 % (3364240)------------------------------ % 65.21/9.48 % (3364240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.21/9.48 % (3364240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.21/9.48 % (3364240)CaDiCaL version: 2.1.3 % 65.21/9.48 % (3364240)Termination reason: Instruction limit % 65.21/9.48 % (3364240)Termination phase: Saturation % 65.21/9.48 % (3364240)Time elapsed: 1.442 s % 65.21/9.48 % (3364240)Peak memory usage: 43 MB % 65.21/9.48 % (3364240)Instructions burned: 5132 (million) % 65.21/9.48 % (3364415)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=853688634:i=5497:nm=2_2982 on theBenchmark for (2982ds/5497Mi) % 65.21/9.48 % (3364415)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 65.21/9.48 % (3364415)Terminated due to inappropriate strategy. % 65.21/9.48 % (3364415)------------------------------ % 65.21/9.48 % (3364415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.21/9.48 % (3364415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.21/9.48 % (3364415)CaDiCaL version: 2.1.3 % 65.21/9.48 % (3364415)Termination reason: Inappropriate % 65.21/9.48 % (3364415)Time elapsed: 0.018 s % 65.21/9.48 % (3364415)Peak memory usage: 13 MB % 65.21/9.48 % (3364415)Instructions burned: 78 (million) % 65.21/9.48 % (3364415)------------------------------ % 65.21/9.48 % (3364415)------------------------------ % 65.21/9.48 % (3364417)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3337537738:fmbsr=2:i=46332_2981 on theBenchmark for (2981ds/46332Mi) % 65.21/9.48 % (3364417)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 65.21/9.48 % (3364417)Terminated due to inappropriate strategy. % 65.21/9.48 % (3364417)------------------------------ % 65.21/9.48 % (3364417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.21/9.48 % (3364417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.21/9.48 % (3364417)CaDiCaL version: 2.1.3 % 65.21/9.48 % (3364417)Termination reason: Inappropriate % 65.21/9.48 % (3364417)Time elapsed: 0.024 s % 65.21/9.48 % (3364417)Peak memory usage: 14 MB % 65.21/9.48 % (3364417)Instructions burned: 110 (million) % 65.21/9.48 % (3364417)------------------------------ % 65.21/9.48 % (3364417)------------------------------ % 65.21/9.48 % (3364419)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2191918088:i=14071_2981 on theBenchmark for (2981ds/14071Mi) % 65.21/9.48 % (3364419)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 65.21/9.48 % (3364419)Terminated due to inappropriate strategy. % 65.21/9.48 % (3364419)------------------------------ % 65.21/9.48 % (3364419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.21/9.48 % (3364419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.21/9.48 % (3364419)CaDiCaL version: 2.1.3 % 65.21/9.48 % (3364419)Termination reason: Inappropriate % 65.21/9.48 % (3364419)Time elapsed: 0.024 s % 65.21/9.48 % (3364419)Peak memory usage: 14 MB % 65.21/9.48 % (3364419)Instructions burned: 110 (million) % 65.21/9.48 % (3364419)------------------------------ % 65.21/9.48 % (3364419)------------------------------ % 65.21/9.48 % (3364421)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1248889345:i=22565:add=on:rawr=on_2981 on theBenchmark for (2981ds/22565Mi) % 65.21/9.48 % (3364296)Instruction limit reached! % 65.21/9.48 % (3364296)------------------------------ % 65.21/9.48 % (3364296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.21/9.48 % (3364296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.21/9.48 % (3364296)CaDiCaL version: 2.1.3 % 65.21/9.48 % (3364296)Termination reason: Instruction limit % 65.21/9.48 % (3364296)Termination phase: Saturation % 65.21/9.48 % (3364296)Time elapsed: 1.594 s % 65.21/9.48 % (3364296)Peak memory usage: 32 MB % 65.21/9.48 % (3364296)Instructions burned: 5114 (million) % 65.21/9.48 % (3364423)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2287663288:i=8173:av=off_2979 on theBenchmark for (2979ds/8173Mi) % 66.62/9.65 % (3364409)Instruction limit reached! % 66.62/9.65 % (3364409)------------------------------ % 66.62/9.65 % (3364409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 66.62/9.65 % (3364409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.62/9.65 % (3364409)CaDiCaL version: 2.1.3 % 66.62/9.65 % (3364409)Termination reason: Instruction limit % 66.62/9.65 % (3364409)Termination phase: Saturation % 66.62/9.65 % (3364409)Time elapsed: 1.262 s % 66.62/9.65 % (3364409)Peak memory usage: 41 MB % 66.62/9.65 % (3364409)Instructions burned: 4594 (million) % 66.62/9.65 % (3364425)dis+10_16:1_sil=16000:random_seed=3478174169:i=9155:fsr=off_2975 on theBenchmark for (2975ds/9155Mi) % 66.62/9.65 % (3364413)Instruction limit reached! % 66.62/9.65 % (3364413)------------------------------ % 66.62/9.65 % (3364413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 66.62/9.65 % (3364413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.62/9.65 % (3364413)CaDiCaL version: 2.1.3 % 66.62/9.65 % (3364413)Termination reason: Instruction limit % 66.62/9.65 % (3364413)Termination phase: Saturation % 66.62/9.65 % (3364413)Time elapsed: 1.494 s % 66.62/9.65 % (3364413)Peak memory usage: 48 MB % 66.62/9.65 % (3364413)Instructions burned: 5215 (million) % 66.62/9.65 % (3364427)ott-3_8_sil=64000:random_seed=599356716:i=20139:bs=on_2969 on theBenchmark for (2969ds/20139Mi) % 66.62/9.65 % (3364423)Instruction limit reached! % 66.62/9.65 % (3364423)------------------------------ % 66.62/9.65 % (3364423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 66.62/9.65 % (3364423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.62/9.65 % (3364423)CaDiCaL version: 2.1.3 % 66.62/9.65 % (3364423)Termination reason: Instruction limit % 66.62/9.65 % (3364423)Termination phase: Saturation % 66.62/9.65 % (3364423)Time elapsed: 1.854 s % 66.62/9.65 % (3364423)Peak memory usage: 34 MB % 66.62/9.65 % (3364423)Instructions burned: 8175 (million) % 66.62/9.65 % (3364429)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=103768236:fmbsr=2:i=32576_2960 on theBenchmark for (2960ds/32576Mi) % 66.62/9.65 % (3364429)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 66.62/9.65 % (3364429)Terminated due to inappropriate strategy. % 66.62/9.65 % (3364429)------------------------------ % 66.62/9.65 % (3364429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 66.62/9.65 % (3364429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.62/9.65 % (3364429)CaDiCaL version: 2.1.3 % 66.62/9.65 % (3364429)Termination reason: Inappropriate % 66.62/9.65 % (3364429)Time elapsed: 0.023 s % 66.62/9.65 % (3364429)Peak memory usage: 13 MB % 66.62/9.65 % (3364429)Instructions burned: 106 (million) % 66.62/9.65 % (3364429)------------------------------ % 66.62/9.65 % (3364429)------------------------------ % 66.62/9.65 % (3364431)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2442092912:i=11404_2960 on theBenchmark for (2960ds/11404Mi) % 66.62/9.65 % (3364425)Instruction limit reached! % 66.62/9.65 % (3364425)------------------------------ % 66.62/9.65 % (3364425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 66.62/9.65 % (3364425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.62/9.65 % (3364425)CaDiCaL version: 2.1.3 % 66.62/9.65 % (3364425)Termination reason: Instruction limit % 66.62/9.65 % (3364425)Termination phase: Saturation % 66.62/9.65 % (3364425)Time elapsed: 2.519 s % 66.62/9.65 % (3364425)Peak memory usage: 55 MB % 66.62/9.65 % (3364425)Instructions burned: 9158 (million) % 66.62/9.65 % (3364433)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1962572255:i=14134_2949 on theBenchmark for (2949ds/14134Mi) % 66.62/9.65 % (3364421)Instruction limit reached! % 66.62/9.65 % (3364421)------------------------------ % 66.62/9.65 % (3364421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 66.62/9.65 % (3364421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.62/9.65 % (3364421)CaDiCaL version: 2.1.3 % 66.62/9.65 % (3364421)Termination reason: Instruction limit % 66.62/9.65 % (3364421)Termination phase: Saturation % 66.62/9.65 % (3364421)Time elapsed: 5.186 s % 66.62/9.65 % (3364421)Peak memory usage: 77 MB % 66.62/9.65 % (3364421)Instructions burned: 22568 (million) % 66.62/9.65 % (3364435)dis+33_16_sil=32000:sac=on:random_seed=2932655202:i=15851:nm=0_2929 on theBenchmark for (2929ds/15851Mi) % 66.62/9.65 % (3364431)Instruction limit reached! % 66.62/9.65 % (3364431)------------------------------ % 66.62/9.65 % (3364431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.18/14.82 % (3364431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.18/14.82 % (3364431)CaDiCaL version: 2.1.3 % 103.18/14.82 % (3364431)Termination reason: Instruction limit % 103.18/14.82 % (3364431)Termination phase: Saturation % 103.18/14.82 % (3364431)Time elapsed: 4.029 s % 103.18/14.82 % (3364431)Peak memory usage: 48 MB % 103.18/14.82 % (3364431)Instructions burned: 11404 (million) % 103.18/14.82 % (3364437)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1506815142:avsq=on:i=17627:add=on:amm=off_2919 on theBenchmark for (2919ds/17627Mi) % 103.18/14.82 % (3364433)Instruction limit reached! % 103.18/14.82 % (3364433)------------------------------ % 103.18/14.82 % (3364433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.18/14.82 % (3364433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.18/14.82 % (3364433)CaDiCaL version: 2.1.3 % 103.18/14.82 % (3364433)Termination reason: Instruction limit % 103.18/14.82 % (3364433)Termination phase: Saturation % 103.18/14.82 % (3364433)Time elapsed: 3.343 s % 103.18/14.82 % (3364433)Peak memory usage: 37 MB % 103.18/14.82 % (3364433)Instructions burned: 14135 (million) % 103.18/14.82 % (3364439)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=201941074:s2a=on:i=53295_2916 on theBenchmark for (2916ds/53295Mi) % 103.18/14.82 % (3364411)Instruction limit reached! % 103.18/14.82 % (3364411)------------------------------ % 103.18/14.82 % (3364411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.18/14.82 % (3364411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.18/14.82 % (3364411)CaDiCaL version: 2.1.3 % 103.18/14.82 % (3364411)Termination reason: Instruction limit % 103.18/14.82 % (3364411)Termination phase: Saturation % 103.18/14.82 % (3364411)Time elapsed: 7.283 s % 103.18/14.82 % (3364411)Peak memory usage: 36 MB % 103.18/14.82 % (3364411)Instructions burned: 29341 (million) % 103.18/14.82 % (3364441)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3143520227:i=26857:ins=20_2912 on theBenchmark for (2912ds/26857Mi) % 103.18/14.82 % (3364441)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 103.18/14.82 % (3364441)Terminated due to inappropriate strategy. % 103.18/14.82 % (3364441)------------------------------ % 103.18/14.82 % (3364441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.18/14.82 % (3364441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.18/14.82 % (3364441)CaDiCaL version: 2.1.3 % 103.18/14.82 % (3364441)Termination reason: Inappropriate % 103.18/14.82 % (3364441)Time elapsed: 0.018 s % 103.18/14.82 % (3364441)Peak memory usage: 13 MB % 103.18/14.82 % (3364441)Instructions burned: 78 (million) % 103.18/14.82 % (3364441)------------------------------ % 103.18/14.82 % (3364441)------------------------------ % 103.18/14.82 % (3364443)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3648571480:i=28120:bs=on:fsr=off_2912 on theBenchmark for (2912ds/28120Mi) % 103.18/14.82 % (3364427)Instruction limit reached! % 103.18/14.82 % (3364427)------------------------------ % 103.18/14.82 % (3364427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.18/14.82 % (3364427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.18/14.82 % (3364427)CaDiCaL version: 2.1.3 % 103.18/14.82 % (3364427)Termination reason: Instruction limit % 103.18/14.82 % (3364427)Termination phase: Saturation % 103.18/14.82 % (3364427)Time elapsed: 6.257 s % 103.18/14.82 % (3364427)Peak memory usage: 58 MB % 103.18/14.82 % (3364427)Instructions burned: 20140 (million) % 103.18/14.82 % (3364445)fmb+10_1_sil=256000:fmbss=7:random_seed=2966083343:fmbsr=1.6:i=182295_2906 on theBenchmark for (2906ds/182295Mi) % 103.18/14.82 % (3364445)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 103.18/14.82 % (3364445)Terminated due to inappropriate strategy. % 103.18/14.82 % (3364445)------------------------------ % 103.18/14.82 % (3364445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.18/14.82 % (3364445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.18/14.82 % (3364445)CaDiCaL version: 2.1.3 % 103.18/14.82 % (3364445)Termination reason: Inappropriate % 103.18/14.82 % (3364445)Time elapsed: 0.018 s % 103.18/14.82 % (3364445)Peak memory usage: 13 MB % 103.18/14.82 % (3364445)Instructions burned: 78 (million) % 103.18/14.82 % (3364445)------------------------------ % 103.18/14.82 % (3364445)------------------------------ % 103.18/14.82 % (3364447)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2796058583:i=44625:gsp=on_2906 on theBenchmark for (2906ds/44625Mi) % 105.95/15.25 % (3364447)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 105.95/15.25 % (3364447)Terminated due to inappropriate strategy. % 105.95/15.25 % (3364447)------------------------------ % 105.95/15.25 % (3364447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.95/15.25 % (3364447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.95/15.25 % (3364447)CaDiCaL version: 2.1.3 % 105.95/15.25 % (3364447)Termination reason: Inappropriate % 105.95/15.25 % (3364447)Time elapsed: 0.020 s % 105.95/15.25 % (3364447)Peak memory usage: 14 MB % 105.95/15.25 % (3364447)Instructions burned: 83 (million) % 105.95/15.25 % (3364447)------------------------------ % 105.95/15.25 % (3364447)------------------------------ % 105.95/15.25 % (3364449)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3614199476:i=160505_2906 on theBenchmark for (2906ds/160505Mi) % 105.95/15.25 % (3364449)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 105.95/15.25 % (3364449)Terminated due to inappropriate strategy. % 105.95/15.25 % (3364449)------------------------------ % 105.95/15.25 % (3364449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.95/15.25 % (3364449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.95/15.25 % (3364449)CaDiCaL version: 2.1.3 % 105.95/15.25 % (3364449)Termination reason: Inappropriate % 105.95/15.25 % (3364449)Time elapsed: 0.018 s % 105.95/15.25 % (3364449)Peak memory usage: 13 MB % 105.95/15.25 % (3364449)Instructions burned: 78 (million) % 105.95/15.25 % (3364449)------------------------------ % 105.95/15.25 % (3364449)------------------------------ % 105.95/15.25 % (3364451)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1827424643:fmbsr=1.3:i=225729_2906 on theBenchmark for (2906ds/225729Mi) % 105.95/15.25 % (3364451)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 105.95/15.25 % (3364451)Terminated due to inappropriate strategy. % 105.95/15.25 % (3364451)------------------------------ % 105.95/15.25 % (3364451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.95/15.25 % (3364451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.95/15.25 % (3364451)CaDiCaL version: 2.1.3 % 105.95/15.25 % (3364451)Termination reason: Inappropriate % 105.95/15.25 % (3364451)Time elapsed: 0.024 s % 105.95/15.25 % (3364451)Peak memory usage: 14 MB % 105.95/15.25 % (3364451)Instructions burned: 110 (million) % 105.95/15.25 % (3364451)------------------------------ % 105.95/15.25 % (3364451)------------------------------ % 105.95/15.25 % (3364453)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3533939228:fmbsr=2:i=185024:ins=7_2905 on theBenchmark for (2905ds/185024Mi) % 105.95/15.25 % (3364453)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 105.95/15.25 % (3364453)Terminated due to inappropriate strategy. % 105.95/15.25 % (3364453)------------------------------ % 105.95/15.25 % (3364453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.95/15.25 % (3364453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.95/15.25 % (3364453)CaDiCaL version: 2.1.3 % 105.95/15.25 % (3364453)Termination reason: Inappropriate % 105.95/15.25 % (3364453)Time elapsed: 0.024 s % 105.95/15.25 % (3364453)Peak memory usage: 14 MB % 105.95/15.25 % (3364453)Instructions burned: 110 (million) % 105.95/15.25 % (3364453)------------------------------ % 105.95/15.25 % (3364453)------------------------------ % 105.95/15.25 % (3364455)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3548696556:rtra=on_2905 on theBenchmark for (2905ds/0Mi) % 105.95/15.25 % (3364455)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 105.95/15.25 % (3364455)Terminated due to inappropriate strategy. % 105.95/15.25 % (3364455)------------------------------ % 105.95/15.25 % (3364455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.95/15.25 % (3364455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.95/15.25 % (3364455)CaDiCaL version: 2.1.3 % 105.95/15.25 % (3364455)Termination reason: Inappropriate % 105.95/15.25 % (3364455)Time elapsed: 0.024 s % 105.95/15.25 % (3364455)Peak memory usage: 15 MB % 105.95/15.25 % (3364455)Instructions burned: 92 (million) % 105.95/15.25 % (3364455)------------------------------ % 105.95/15.25 % (3364455)------------------------------ % 105.95/15.25 % (3364457)% WARNING: option uhcvi not known. % 105.95/15.25 % (3364457)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=598614651:i=271062:add=off:rtra=on:rawr=on_2904 on theBenchmark for (2904ds/271062Mi) % 111.88/16.05 % (3364435)Instruction limit reached! % 111.88/16.05 % (3364435)------------------------------ % 111.88/16.05 % (3364435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.88/16.05 % (3364435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.88/16.05 % (3364435)CaDiCaL version: 2.1.3 % 111.88/16.05 % (3364435)Termination reason: Instruction limit % 111.88/16.05 % (3364435)Termination phase: Saturation % 111.88/16.05 % (3364435)Time elapsed: 3.657 s % 111.88/16.05 % (3364435)Peak memory usage: 35 MB % 111.88/16.05 % (3364435)Instructions burned: 15854 (million) % 111.88/16.05 % (3364459)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2664770585:i=176048:add=on:rtra=on:rawr=on_2892 on theBenchmark for (2892ds/176048Mi) % 111.88/16.05 % (3364437)Instruction limit reached! % 111.88/16.05 % (3364437)------------------------------ % 111.88/16.05 % (3364437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.88/16.05 % (3364437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.88/16.05 % (3364437)CaDiCaL version: 2.1.3 % 111.88/16.05 % (3364437)Termination reason: Instruction limit % 111.88/16.05 % (3364437)Termination phase: Saturation % 111.88/16.05 % (3364437)Time elapsed: 6.384 s % 111.88/16.05 % (3364437)Peak memory usage: 307 MB % 111.88/16.05 % (3364437)Instructions burned: 17627 (million) % 111.88/16.05 % (3364665)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3465997108:i=206:fgj=on:rtra=on_2855 on theBenchmark for (2855ds/206Mi) % 111.88/16.05 % (3364665)Instruction limit reached! % 111.88/16.05 % (3364665)------------------------------ % 111.88/16.05 % (3364665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.88/16.05 % (3364665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.88/16.05 % (3364665)CaDiCaL version: 2.1.3 % 111.88/16.05 % (3364665)Termination reason: Instruction limit % 111.88/16.05 % (3364665)Termination phase: Saturation % 111.88/16.05 % (3364665)Time elapsed: 0.057 s % 111.88/16.05 % (3364665)Peak memory usage: 17 MB % 111.88/16.05 % (3364665)Instructions burned: 207 (million) % 111.88/16.05 % (3364696)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3451421006:i=232:rtra=on_2854 on theBenchmark for (2854ds/232Mi) % 111.88/16.05 % (3364696)Instruction limit reached! % 111.88/16.05 % (3364696)------------------------------ % 111.88/16.05 % (3364696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.88/16.05 % (3364696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.88/16.05 % (3364696)CaDiCaL version: 2.1.3 % 111.88/16.05 % (3364696)Termination reason: Instruction limit % 111.88/16.05 % (3364696)Termination phase: Saturation % 111.88/16.05 % (3364696)Time elapsed: 0.057 s % 111.88/16.05 % (3364696)Peak memory usage: 16 MB % 111.88/16.05 % (3364696)Instructions burned: 234 (million) % 111.88/16.05 % (3364443)Instruction limit reached! % 111.88/16.05 % (3364443)------------------------------ % 111.88/16.05 % (3364443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.88/16.05 % (3364443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.88/16.05 % (3364443)CaDiCaL version: 2.1.3 % 111.88/16.05 % (3364443)Termination reason: Instruction limit % 111.88/16.05 % (3364443)Termination phase: Saturation % 111.88/16.05 % (3364443)Time elapsed: 5.853 s % 111.88/16.05 % (3364443)Peak memory usage: 26 MB % 111.88/16.05 % (3364443)Instructions burned: 28124 (million) % 111.88/16.05 % (3364726)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3641273822:i=262:rtra=on_2854 on theBenchmark for (2854ds/262Mi) % 111.88/16.05 % (3364730)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3176917794:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2853 on theBenchmark for (2853ds/318Mi) % 111.88/16.05 % (3364726)Instruction limit reached! % 111.88/16.05 % (3364726)------------------------------ % 111.88/16.05 % (3364726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.88/16.05 % (3364726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.88/16.05 % (3364726)CaDiCaL version: 2.1.3 % 111.88/16.05 % (3364726)Termination reason: Instruction limit % 111.88/16.05 % (3364726)Termination phase: Saturation % 111.88/16.05 % (3364726)Time elapsed: 0.067 s % 111.88/16.05 % (3364726)Peak memory usage: 17 MB % 111.88/16.05 % (3364726)Instructions burned: 265 (million) % 111.88/16.05 % (3364754)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3698020311:i=1428:nm=2:rtra=on_2853 on theBenchmark for (2853ds/1428Mi) % 120.94/17.38 % (3364730)Instruction limit reached! % 120.94/17.38 % (3364730)------------------------------ % 120.94/17.38 % (3364730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.94/17.38 % (3364730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.94/17.38 % (3364730)CaDiCaL version: 2.1.3 % 120.94/17.38 % (3364730)Termination reason: Instruction limit % 120.94/17.38 % (3364730)Termination phase: Saturation % 120.94/17.38 % (3364730)Time elapsed: 0.090 s % 120.94/17.38 % (3364730)Peak memory usage: 19 MB % 120.94/17.38 % (3364730)Instructions burned: 320 (million) % 120.94/17.38 % (3364754)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 120.94/17.38 % (3364754)Terminated due to inappropriate strategy. % 120.94/17.38 % (3364754)------------------------------ % 120.94/17.38 % (3364754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.94/17.38 % (3364754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.94/17.38 % (3364754)CaDiCaL version: 2.1.3 % 120.94/17.38 % (3364754)Termination reason: Inappropriate % 120.94/17.38 % (3364754)Time elapsed: 0.024 s % 120.94/17.38 % (3364754)Peak memory usage: 15 MB % 120.94/17.38 % (3364754)Instructions burned: 92 (million) % 120.94/17.38 % (3364754)------------------------------ % 120.94/17.38 % (3364754)------------------------------ % 120.94/17.38 % (3364764)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1408989032:i=262:bd=preordered:rtra=on:fsd=on_2852 on theBenchmark for (2852ds/262Mi) % 120.94/17.38 % (3364768)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=1958127187:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2852 on theBenchmark for (2852ds/1368Mi) % 120.94/17.38 % (3364764)Instruction limit reached! % 120.94/17.38 % (3364764)------------------------------ % 120.94/17.38 % (3364764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.94/17.38 % (3364764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.94/17.38 % (3364764)CaDiCaL version: 2.1.3 % 120.94/17.38 % (3364764)Termination reason: Instruction limit % 120.94/17.38 % (3364764)Termination phase: Saturation % 120.94/17.38 % (3364764)Time elapsed: 0.065 s % 120.94/17.38 % (3364764)Peak memory usage: 17 MB % 120.94/17.38 % (3364764)Instructions burned: 266 (million) % 120.94/17.38 % (3364796)ott-21_1_sil=16000:si=on:fs=off:random_seed=2137057356:i=360:av=off:fsr=off:rtra=on_2852 on theBenchmark for (2852ds/360Mi) % 120.94/17.38 % (3364796)Instruction limit reached! % 120.94/17.38 % (3364796)------------------------------ % 120.94/17.38 % (3364796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.94/17.38 % (3364796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.94/17.38 % (3364796)CaDiCaL version: 2.1.3 % 120.94/17.38 % (3364796)Termination reason: Instruction limit % 120.94/17.38 % (3364796)Termination phase: Saturation % 120.94/17.38 % (3364796)Time elapsed: 0.096 s % 120.94/17.38 % (3364796)Peak memory usage: 17 MB % 120.94/17.38 % (3364796)Instructions burned: 364 (million) % 120.94/17.38 % (3364820)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1741969308:i=954:bd=all:rtra=on_2851 on theBenchmark for (2851ds/954Mi) % 120.94/17.38 % (3364768)Instruction limit reached! % 120.94/17.38 % (3364768)------------------------------ % 120.94/17.38 % (3364768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.94/17.38 % (3364768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.94/17.38 % (3364768)CaDiCaL version: 2.1.3 % 120.94/17.38 % (3364768)Termination reason: Instruction limit % 120.94/17.38 % (3364768)Termination phase: Saturation % 120.94/17.38 % (3364768)Time elapsed: 0.357 s % 120.94/17.38 % (3364768)Peak memory usage: 21 MB % 120.94/17.38 % (3364768)Instructions burned: 1369 (million) % 120.94/17.38 % (3364822)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1209401662:fmbsr=1.3:i=1730:ins=25:rtra=on_2849 on theBenchmark for (2849ds/1730Mi) % 120.94/17.38 % (3364822)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 120.94/17.38 % (3364822)Terminated due to inappropriate strategy. % 120.94/17.38 % (3364822)------------------------------ % 120.94/17.38 % (3364822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.94/17.38 % (3364822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.94/17.38 % (3364822)CaDiCaL version: 2.1.3 % 120.94/17.38 % (3364822)Termination reason: Inappropriate % 146.31/20.93 % (3364822)Time elapsed: 0.024 s % 146.31/20.93 % (3364822)Peak memory usage: 15 MB % 146.31/20.93 % (3364822)Instructions burned: 91 (million) % 146.31/20.93 % (3364822)------------------------------ % 146.31/20.93 % (3364822)------------------------------ % 146.31/20.93 % (3364824)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1316390423:i=2358:rtra=on_2848 on theBenchmark for (2848ds/2358Mi) % 146.31/20.93 % (3364820)Instruction limit reached! % 146.31/20.93 % (3364820)------------------------------ % 146.31/20.93 % (3364820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.31/20.93 % (3364820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.31/20.93 % (3364820)CaDiCaL version: 2.1.3 % 146.31/20.93 % (3364820)Termination reason: Instruction limit % 146.31/20.93 % (3364820)Termination phase: Saturation % 146.31/20.93 % (3364820)Time elapsed: 0.288 s % 146.31/20.93 % (3364820)Peak memory usage: 19 MB % 146.31/20.93 % (3364820)Instructions burned: 957 (million) % 146.31/20.93 % (3364826)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1422152588:i=1778:ins=1:rtra=on_2848 on theBenchmark for (2848ds/1778Mi) % 146.31/20.93 % (3364826)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.31/20.93 % (3364826)Terminated due to inappropriate strategy. % 146.31/20.93 % (3364826)------------------------------ % 146.31/20.93 % (3364826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.31/20.93 % (3364826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.31/20.93 % (3364826)CaDiCaL version: 2.1.3 % 146.31/20.93 % (3364826)Termination reason: Inappropriate % 146.31/20.93 % (3364826)Time elapsed: 0.032 s % 146.31/20.93 % (3364826)Peak memory usage: 16 MB % 146.31/20.93 % (3364826)Instructions burned: 123 (million) % 146.31/20.93 % (3364826)------------------------------ % 146.31/20.93 % (3364826)------------------------------ % 146.31/20.93 % (3364828)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=2704910333:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2847 on theBenchmark for (2847ds/1384Mi) % 146.31/20.93 % (3364828)Instruction limit reached! % 146.31/20.93 % (3364828)------------------------------ % 146.31/20.93 % (3364828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.31/20.93 % (3364828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.31/20.93 % (3364828)CaDiCaL version: 2.1.3 % 146.31/20.93 % (3364828)Termination reason: Instruction limit % 146.31/20.93 % (3364828)Termination phase: Saturation % 146.31/20.93 % (3364828)Time elapsed: 0.472 s % 146.31/20.93 % (3364828)Peak memory usage: 28 MB % 146.31/20.93 % (3364828)Instructions burned: 1384 (million) % 146.31/20.93 % (3364830)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=448783141:i=1758:kws=inv_precedence:fsr=off:rtra=on_2842 on theBenchmark for (2842ds/1758Mi) % 146.31/20.93 % (3364824)Instruction limit reached! % 146.31/20.93 % (3364824)------------------------------ % 146.31/20.93 % (3364824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.31/20.93 % (3364824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.31/20.93 % (3364824)CaDiCaL version: 2.1.3 % 146.31/20.93 % (3364824)Termination reason: Instruction limit % 146.31/20.93 % (3364824)Termination phase: Saturation % 146.31/20.93 % (3364824)Time elapsed: 0.736 s % 146.31/20.93 % (3364824)Peak memory usage: 25 MB % 146.31/20.93 % (3364824)Instructions burned: 2360 (million) % 146.31/20.93 % (3364832)fmb+10_1_sil=64000:si=on:random_seed=170178943:i=44122:nm=2:rtra=on:gsp=on_2841 on theBenchmark for (2841ds/44122Mi) % 146.31/20.93 % (3364832)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.31/20.93 % (3364832)Terminated due to inappropriate strategy. % 146.31/20.93 % (3364832)------------------------------ % 146.31/20.93 % (3364832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.31/20.93 % (3364832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.31/20.93 % (3364832)CaDiCaL version: 2.1.3 % 146.31/20.93 % (3364832)Termination reason: Inappropriate % 146.31/20.93 % (3364832)Time elapsed: 0.026 s % 146.31/20.93 % (3364832)Peak memory usage: 15 MB % 146.31/20.93 % (3364832)Instructions burned: 100 (million) % 146.31/20.93 % (3364832)------------------------------ % 146.31/20.93 % (3364832)------------------------------ % 146.31/20.93 % (3364834)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3968898462:i=19030:nm=5:rtra=on_2840 on theBenchmark for (2840ds/19030Mi) % 151.63/21.93 % (3364834)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.63/21.93 % (3364834)Terminated due to inappropriate strategy. % 151.63/21.93 % (3364834)------------------------------ % 151.63/21.93 % (3364834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.63/21.93 % (3364834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.63/21.93 % (3364834)CaDiCaL version: 2.1.3 % 151.63/21.93 % (3364834)Termination reason: Inappropriate % 151.63/21.93 % (3364834)Time elapsed: 0.024 s % 151.63/21.93 % (3364834)Peak memory usage: 15 MB % 151.63/21.93 % (3364834)Instructions burned: 92 (million) % 151.63/21.93 % (3364834)------------------------------ % 151.63/21.93 % (3364834)------------------------------ % 151.63/21.93 % (3364836)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2131489387:fmbsr=1.7:i=1840:rtra=on_2840 on theBenchmark for (2840ds/1840Mi) % 151.63/21.93 % (3364836)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.63/21.93 % (3364836)Terminated due to inappropriate strategy. % 151.63/21.93 % (3364836)------------------------------ % 151.63/21.93 % (3364836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.63/21.93 % (3364836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.63/21.93 % (3364836)CaDiCaL version: 2.1.3 % 151.63/21.93 % (3364836)Termination reason: Inappropriate % 151.63/21.93 % (3364836)Time elapsed: 0.024 s % 151.63/21.93 % (3364836)Peak memory usage: 15 MB % 151.63/21.93 % (3364836)Instructions burned: 92 (million) % 151.63/21.93 % (3364836)------------------------------ % 151.63/21.93 % (3364836)------------------------------ % 151.63/21.93 % (3364838)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3414147804:i=10262:rtra=on_2840 on theBenchmark for (2840ds/10262Mi) % 151.63/21.93 % (3364830)Instruction limit reached! % 151.63/21.93 % (3364830)------------------------------ % 151.63/21.93 % (3364830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.63/21.93 % (3364830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.63/21.93 % (3364830)CaDiCaL version: 2.1.3 % 151.63/21.93 % (3364830)Termination reason: Instruction limit % 151.63/21.93 % (3364830)Termination phase: Saturation % 151.63/21.93 % (3364830)Time elapsed: 0.548 s % 151.63/21.93 % (3364830)Peak memory usage: 28 MB % 151.63/21.93 % (3364830)Instructions burned: 1761 (million) % 151.63/21.93 % (3364840)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3344539968:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2837 on theBenchmark for (2837ds/2944Mi) % 151.63/21.93 % (3364840)Instruction limit reached! % 151.63/21.93 % (3364840)------------------------------ % 151.63/21.93 % (3364840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.63/21.93 % (3364840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.63/21.93 % (3364840)CaDiCaL version: 2.1.3 % 151.63/21.93 % (3364840)Termination reason: Instruction limit % 151.63/21.93 % (3364840)Termination phase: Saturation % 151.63/21.93 % (3364840)Time elapsed: 0.878 s % 151.63/21.93 % (3364840)Peak memory usage: 31 MB % 151.63/21.93 % (3364840)Instructions burned: 2946 (million) % 151.63/21.93 % (3364842)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2325157620:i=12648:rtra=on_2828 on theBenchmark for (2828ds/12648Mi) % 151.63/21.93 % (3364842)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.63/21.93 % (3364842)Terminated due to inappropriate strategy. % 151.63/21.93 % (3364842)------------------------------ % 151.63/21.93 % (3364842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.63/21.93 % (3364842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.63/21.93 % (3364842)CaDiCaL version: 2.1.3 % 151.63/21.93 % (3364842)Termination reason: Inappropriate % 151.63/21.93 % (3364842)Time elapsed: 0.025 s % 151.63/21.93 % (3364842)Peak memory usage: 15 MB % 151.63/21.93 % (3364842)Instructions burned: 92 (million) % 151.63/21.93 % (3364842)------------------------------ % 151.63/21.93 % (3364842)------------------------------ % 151.63/21.93 % (3364844)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1895929932:fmbsr=2.30978:i=4348:rtra=on_2827 on theBenchmark for (2827ds/4348Mi) % 151.63/21.93 % (3364844)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.63/21.93 % (3364844)Terminated due to inappropriate strategy. % 151.63/21.93 % (3364844)------------------------------ % 213.30/30.46 % (3364844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.30/30.46 % (3364844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.30/30.46 % (3364844)CaDiCaL version: 2.1.3 % 213.30/30.46 % (3364844)Termination reason: Inappropriate % 213.30/30.46 % (3364844)Time elapsed: 0.024 s % 213.30/30.46 % (3364844)Peak memory usage: 15 MB % 213.30/30.46 % (3364844)Instructions burned: 92 (million) % 213.30/30.46 % (3364844)------------------------------ % 213.30/30.46 % (3364844)------------------------------ % 213.30/30.46 % (3364846)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3325666779:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2827 on theBenchmark for (2827ds/1738Mi) % 213.30/30.46 % (3364846)Instruction limit reached! % 213.30/30.46 % (3364846)------------------------------ % 213.30/30.46 % (3364846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.30/30.46 % (3364846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.30/30.46 % (3364846)CaDiCaL version: 2.1.3 % 213.30/30.46 % (3364846)Termination reason: Instruction limit % 213.30/30.46 % (3364846)Termination phase: Saturation % 213.30/30.46 % (3364846)Time elapsed: 0.531 s % 213.30/30.46 % (3364846)Peak memory usage: 24 MB % 213.30/30.46 % (3364846)Instructions burned: 1739 (million) % 213.30/30.46 % (3364848)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2130856084:i=10228:av=off:rtra=on_2822 on theBenchmark for (2822ds/10228Mi) % 213.30/30.46 % (3364178)Instruction limit reached! % 213.30/30.46 % (3364178)------------------------------ % 213.30/30.46 % (3364178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.30/30.46 % (3364178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.30/30.46 % (3364178)CaDiCaL version: 2.1.3 % 213.30/30.46 % (3364178)Termination reason: Instruction limit % 213.30/30.46 % (3364178)Termination phase: Saturation % 213.30/30.46 % (3364178)Time elapsed: 18.903 s % 213.30/30.46 % (3364178)Peak memory usage: 436 MB % 213.30/30.46 % (3364178)Instructions burned: 88029 (million) % 213.30/30.46 % (3364850)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1120165378:i=108564:rtra=on_2810 on theBenchmark for (2810ds/108564Mi) % 213.30/30.46 % (3364850)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.30/30.46 % (3364850)Terminated due to inappropriate strategy. % 213.30/30.46 % (3364850)------------------------------ % 213.30/30.46 % (3364850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.30/30.46 % (3364850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.30/30.46 % (3364850)CaDiCaL version: 2.1.3 % 213.30/30.46 % (3364850)Termination reason: Inappropriate % 213.30/30.46 % (3364850)Time elapsed: 0.024 s % 213.30/30.46 % (3364850)Peak memory usage: 15 MB % 213.30/30.46 % (3364850)Instructions burned: 93 (million) % 213.30/30.46 % (3364850)------------------------------ % 213.30/30.46 % (3364850)------------------------------ % 213.30/30.46 % (3364852)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2345974933:i=7024:aac=none:rtra=on_2809 on theBenchmark for (2809ds/7024Mi) % 213.30/30.46 % (3364838)Instruction limit reached! % 213.30/30.46 % (3364838)------------------------------ % 213.30/30.46 % (3364838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.30/30.46 % (3364838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.30/30.46 % (3364838)CaDiCaL version: 2.1.3 % 213.30/30.46 % (3364838)Termination reason: Instruction limit % 213.30/30.46 % (3364838)Termination phase: Saturation % 213.30/30.46 % (3364838)Time elapsed: 3.230 s % 213.30/30.46 % (3364838)Peak memory usage: 71 MB % 213.30/30.46 % (3364838)Instructions burned: 10265 (million) % 213.30/30.46 % (3364854)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1011402801:i=7546:rtra=on:amm=off_2807 on theBenchmark for (2807ds/7546Mi) % 213.30/30.46 % (3364439)Instruction limit reached! % 213.30/30.46 % (3364439)------------------------------ % 213.30/30.46 % (3364439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.30/30.46 % (3364439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.30/30.46 % (3364439)CaDiCaL version: 2.1.3 % 213.30/30.46 % (3364439)Termination reason: Instruction limit % 213.30/30.46 % (3364439)Termination phase: Saturation % 213.30/30.46 % (3364439)Time elapsed: 12.375 s % 213.30/30.46 % (3364439)Peak memory usage: 165 MB % 213.30/30.46 % (3364439)Instructions burned: 53298 (million) % 213.30/30.46 % (3364856)ott+11_1_sil=16000:si=on:gs=on:random_seed=1966643070:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2792 on theBenchmark for (2792ds/4502Mi) % 278.89/39.78 % (3364852)Instruction limit reached! % 278.89/39.78 % (3364852)------------------------------ % 278.89/39.78 % (3364852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.89/39.78 % (3364852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.89/39.78 % (3364852)CaDiCaL version: 2.1.3 % 278.89/39.78 % (3364852)Termination reason: Instruction limit % 278.89/39.78 % (3364852)Termination phase: Saturation % 278.89/39.78 % (3364852)Time elapsed: 1.882 s % 278.89/39.78 % (3364852)Peak memory usage: 32 MB % 278.89/39.78 % (3364852)Instructions burned: 7026 (million) % 278.89/39.78 % (3364858)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=1937728070:fmbsr=1.6:i=135068:rtra=on_2790 on theBenchmark for (2790ds/135068Mi) % 278.89/39.78 % (3364858)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 278.89/39.78 % (3364858)Terminated due to inappropriate strategy. % 278.89/39.78 % (3364858)------------------------------ % 278.89/39.78 % (3364858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.89/39.78 % (3364858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.89/39.78 % (3364858)CaDiCaL version: 2.1.3 % 278.89/39.78 % (3364858)Termination reason: Inappropriate % 278.89/39.78 % (3364858)Time elapsed: 0.030 s % 278.89/39.78 % (3364858)Peak memory usage: 15 MB % 278.89/39.78 % (3364858)Instructions burned: 120 (million) % 278.89/39.78 % (3364858)------------------------------ % 278.89/39.78 % (3364858)------------------------------ % 278.89/39.78 % (3364860)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2663222306:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2790 on theBenchmark for (2790ds/9182Mi) % 278.89/39.78 % (3364854)Instruction limit reached! % 278.89/39.78 % (3364854)------------------------------ % 278.89/39.78 % (3364854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.89/39.78 % (3364854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.89/39.78 % (3364854)CaDiCaL version: 2.1.3 % 278.89/39.78 % (3364854)Termination reason: Instruction limit % 278.89/39.78 % (3364854)Termination phase: Saturation % 278.89/39.78 % (3364854)Time elapsed: 1.858 s % 278.89/39.78 % (3364854)Peak memory usage: 26 MB % 278.89/39.78 % (3364854)Instructions burned: 7548 (million) % 278.89/39.78 % (3364862)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=2098563052:i=58680:rtra=on_2789 on theBenchmark for (2789ds/58680Mi) % 278.89/39.78 % (3364848)Instruction limit reached! % 278.89/39.78 % (3364848)------------------------------ % 278.89/39.78 % (3364848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.89/39.78 % (3364848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.89/39.78 % (3364848)CaDiCaL version: 2.1.3 % 278.89/39.78 % (3364848)Termination reason: Instruction limit % 278.89/39.78 % (3364848)Termination phase: Saturation % 278.89/39.78 % (3364848)Time elapsed: 3.670 s % 278.89/39.78 % (3364848)Peak memory usage: 46 MB % 278.89/39.78 % (3364848)Instructions burned: 10230 (million) % 278.89/39.78 % (3364864)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=1297875852:i=10422:rtra=on_2785 on theBenchmark for (2785ds/10422Mi) % 278.89/39.78 % (3364856)Instruction limit reached! % 278.89/39.78 % (3364856)------------------------------ % 278.89/39.78 % (3364856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.89/39.78 % (3364856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.89/39.78 % (3364856)CaDiCaL version: 2.1.3 % 278.89/39.78 % (3364856)Termination reason: Instruction limit % 278.89/39.78 % (3364856)Termination phase: Saturation % 278.89/39.78 % (3364856)Time elapsed: 0.963 s % 278.89/39.78 % (3364856)Peak memory usage: 23 MB % 278.89/39.78 % (3364856)Instructions burned: 4503 (million) % 278.89/39.78 % (3364866)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=511609996:i=10994:nm=2:rtra=on_2782 on theBenchmark for (2782ds/10994Mi) % 278.89/39.78 % (3364866)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 278.89/39.78 % (3364866)Terminated due to inappropriate strategy. % 278.89/39.78 % (3364866)------------------------------ % 278.89/39.78 % (3364866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.89/39.78 % (3364866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.89/39.78 % (3364866)CaDiCaL version: 2.1.3 % 278.89/39.78 % (3364866)Termination reason: Inappropriate % 294.15/42.00 % (3364866)Time elapsed: 0.024 s % 294.15/42.00 % (3364866)Peak memory usage: 15 MB % 294.15/42.00 % (3364866)Instructions burned: 92 (million) % 294.15/42.00 % (3364866)------------------------------ % 294.15/42.00 % (3364866)------------------------------ % 294.15/42.00 % (3364868)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:si=on:fmbss=15:random_seed=485694461:fmbsr=2:i=92664:rtra=on_2782 on theBenchmark for (2782ds/92664Mi) % 294.15/42.00 % (3364868)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 294.15/42.00 % (3364868)Terminated due to inappropriate strategy. % 294.15/42.00 % (3364868)------------------------------ % 294.15/42.00 % (3364868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 294.15/42.00 % (3364868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.15/42.00 % (3364868)CaDiCaL version: 2.1.3 % 294.15/42.00 % (3364868)Termination reason: Inappropriate % 294.15/42.00 % (3364868)Time elapsed: 0.030 s % 294.15/42.00 % (3364868)Peak memory usage: 15 MB % 294.15/42.00 % (3364868)Instructions burned: 123 (million) % 294.15/42.00 % (3364868)------------------------------ % 294.15/42.00 % (3364868)------------------------------ % 294.15/42.00 % (3364870)fmb+10_1_sil=128000:tgt=full:sas=cadical:si=on:fmbss=12:random_seed=1151989921:i=28142:rtra=on_2781 on theBenchmark for (2781ds/28142Mi) % 294.15/42.00 % (3364870)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 294.15/42.00 % (3364870)Terminated due to inappropriate strategy. % 294.15/42.00 % (3364870)------------------------------ % 294.15/42.00 % (3364870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 294.15/42.00 % (3364870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.15/42.00 % (3364870)CaDiCaL version: 2.1.3 % 294.15/42.00 % (3364870)Termination reason: Inappropriate % 294.15/42.00 % (3364870)Time elapsed: 0.030 s % 294.15/42.00 % (3364870)Peak memory usage: 15 MB % 294.15/42.00 % (3364870)Instructions burned: 123 (million) % 294.15/42.00 % (3364870)------------------------------ % 294.15/42.00 % (3364870)------------------------------ % 294.15/42.00 % (3364872)dis+10_161_sil=128000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1759815852:i=45130:add=on:rtra=on:rawr=on_2781 on theBenchmark for (2781ds/45130Mi) % 294.15/42.00 % (3364860)Instruction limit reached! % 294.15/42.00 % (3364860)------------------------------ % 294.15/42.00 % (3364860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 294.15/42.00 % (3364860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.15/42.00 % (3364860)CaDiCaL version: 2.1.3 % 294.15/42.00 % (3364860)Termination reason: Instruction limit % 294.15/42.00 % (3364860)Termination phase: Saturation % 294.15/42.00 % (3364860)Time elapsed: 2.672 s % 294.15/42.00 % (3364860)Peak memory usage: 69 MB % 294.15/42.00 % (3364860)Instructions burned: 9183 (million) % 294.15/42.00 % (3364874)ott+4_1_sil=16000:si=on:sp=arity:gs=on:random_seed=3357944982:i=16346:av=off:rtra=on_2763 on theBenchmark for (2763ds/16346Mi) % 294.15/42.00 % (3364864)Instruction limit reached! % 294.15/42.00 % (3364864)------------------------------ % 294.15/42.00 % (3364864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 294.15/42.00 % (3364864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.15/42.00 % (3364864)CaDiCaL version: 2.1.3 % 294.15/42.00 % (3364864)Termination reason: Instruction limit % 294.15/42.00 % (3364864)Termination phase: Saturation % 294.15/42.00 % (3364864)Time elapsed: 3.126 s % 294.15/42.00 % (3364864)Peak memory usage: 75 MB % 294.15/42.00 % (3364864)Instructions burned: 10422 (million) % 294.15/42.00 % (3364876)dis+10_16:1_sil=16000:si=on:random_seed=3248640733:i=18310:fsr=off:rtra=on_2753 on theBenchmark for (2753ds/18310Mi) % 294.15/42.00 % (3364874)Instruction limit reached! % 294.15/42.00 % (3364874)------------------------------ % 294.15/42.00 % (3364874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 294.15/42.00 % (3364874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.15/42.00 % (3364874)CaDiCaL version: 2.1.3 % 294.15/42.00 % (3364874)Termination reason: Instruction limit % 294.15/42.00 % (3364874)Termination phase: Saturation % 294.15/42.00 % (3364874)Time elapsed: 5.057 s % 294.15/42.00 % (3364874)Peak memory usage: 93 MB % 294.15/42.00 % (3364874)Instructions burned: 16346 (million) % 294.15/42.00 % (3364878)ott-3_8_sil=64000:si=on:random_seed=474867312:i=40278:bs=on:rtra=on_2712 on theBenchmark for (2712ds/40278Mi) % 294.15/42.00 % (3364876)Instruction limit reached! % 294.15/42.00 % (3364876)------------------------------ % 300.08/42.83 % (3364876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.08/42.83 % (3364876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.08/42.83 % (3364876)CaDiCaL version: 2.1.3 % 300.08/42.83 % (3364876)Termination reason: Instruction limit % 300.08/42.83 % (3364876)Termination phase: Saturation % 300.08/42.83 % (3364876)Time elapsed: 5.696 s % 300.08/42.83 % (3364876)Peak memory usage: 77 MB % 300.08/42.83 % (3364876)Instructions burned: 18311 (million) % 300.08/42.83 % (3365251)fmb+10_1_sil=64000:tgt=ground:sas=cadical:si=on:bce=on:fmbss=9:random_seed=2072916503:fmbsr=2:i=65152:rtra=on_2696 on theBenchmark for (2696ds/65152Mi) % 300.08/42.83 % (3365251)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.08/42.83 % (3365251)Terminated due to inappropriate strategy. % 300.08/42.83 % (3365251)------------------------------ % 300.08/42.83 % (3365251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.08/42.83 % (3365251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.08/42.83 % (3365251)CaDiCaL version: 2.1.3 % 300.08/42.83 % (3365251)Termination reason: Inappropriate % 300.08/42.83 % (3365251)Time elapsed: 0.030 s % 300.08/42.83 % (3365251)Peak memory usage: 15 MB % 300.08/42.83 % (3365251)Instructions burned: 120 (million) % 300.08/42.83 % (3365251)------------------------------ % 300.08/42.83 % (3365251)------------------------------ % 300.08/42.83 % (3365266)ott+10_8:1_sil=16000:si=on:sp=arity:gs=on:random_seed=682612425:i=22808:rtra=on_2696 on theBenchmark for (2696ds/22808Mi) % 300.08/42.83 % (3364872)Instruction limit reached! % 300.08/42.83 % (3364872)------------------------------ % 300.08/42.83 % (3364872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.08/42.83 % (3364872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.08/42.83 % (3364872)CaDiCaL version: 2.1.3 % 300.08/42.83 % (3364872)Termination reason: Instruction limit % 300.08/42.83 % (3364872)Termination phase: Saturation % 300.08/42.83 % (3364872)Time elapsed: 10.361 s % 300.08/42.83 % (3364872)Peak memory usage: 107 MB % 300.08/42.83 % (3364872)Instructions burned: 45134 (million) % 300.08/42.83 % (3365317)ott-11_1_sil=16000:si=on:alpa=false:sac=on:random_seed=591521460:i=28268:rtra=on_2677 on theBenchmark for (2677ds/28268Mi) % 300.08/42.83 % (3364177)Instruction limit reached! % 300.08/42.83 % (3364177)------------------------------ % 300.08/42.83 % (3364177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.08/42.83 % (3364177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.08/42.83 % (3364177)CaDiCaL version: 2.1.3 % 300.08/42.83 % (3364177)Termination reason: Instruction limit % 300.08/42.83 % (3364177)Termination phase: Saturation % 300.08/42.83 % (3364177)Time elapsed: 33.253 s % 300.08/42.83 % (3364177)Peak memory usage: 230 MB % 300.08/42.83 % (3364177)Instructions burned: 135534 (million) % 300.08/42.83 % (3365319)dis+33_16_sil=32000:si=on:sac=on:random_seed=2223286307:i=31702:nm=0:rtra=on_2666 on theBenchmark for (2666ds/31702Mi) % 300.08/42.83 % (3364862)Instruction limit reached! % 300.08/42.83 % (3364862)------------------------------ % 300.08/42.83 % (3364862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.08/42.83 % (3364862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.08/42.83 % (3364862)CaDiCaL version: 2.1.3 % 300.08/42.83 % (3364862)Termination reason: Instruction limit % 300.08/42.83 % (3364862)Termination phase: Saturation % 300.08/42.83 % (3364862)Time elapsed: 16.084 s % 300.08/42.83 % (3364862)Peak memory usage: 80 MB % 300.08/42.83 % (3364862)Instructions burned: 58682 (million) % 300.08/42.83 % (3365321)dis+4_1024_sil=32000:si=on:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3058855388:avsq=on:i=35254:add=on:rtra=on:amm=off_2627 on theBenchmark for (2627ds/35254Mi) % 300.08/42.83 % (3365266)Instruction limit reached! % 300.08/42.83 % (3365266)------------------------------ % 300.08/42.83 % (3365266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.08/42.83 % (3365266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.08/42.83 % (3365266)CaDiCaL version: 2.1.3 % 300.08/42.83 % (3365266)Termination reason: Instruction limit % 300.08/42.83 % (3365266)Termination phase: Saturation % 300.08/42.83 % (3365266)Time elapsed: 9.241 s % 300.08/42.83 % (3365266)Peak memory usage: 95 MB % 300.08/42.83 % (3365266)Instructions burned: 22808 (million) % 300.08/42.83 % (3365323)ott+10_64_anc=all:sil=128000:sas=cadical:si=on:bsr=unit_only:nwc=1:cn=on:random_seed=1647237821:s2a=on:i=106590:rtra=on_2603 on theBenchmark for ( % 300.08/42.83 Terminated % 300.08/42.83 % Vampire exiting %------------------------------------------------------------------------------