%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX136_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:46:32 PM UTC 2026 % Result : Timeout 300.40s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX136_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 % Computer : n003.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 15:04:57 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.23 Running first-order model finding % 0.09/0.23 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.97/0.79 % (1683587)Will run a generic schedule for satisfiability detection. % 2.97/0.79 % (1683593)% WARNING: option uhcvi not known. % 2.97/0.79 % (1683592)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3515683002_2999 on theBenchmark for (2999ds/0Mi) % 2.97/0.79 % (1683595)dis+10_1_sil=32000:sp=arity:random_seed=1123368580:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.97/0.79 % (1683594)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1533596853:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.97/0.79 % (1683596)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1975888013:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.97/0.79 % (1683593)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3142029335:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.97/0.79 % (1683597)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2037856300:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.97/0.79 % (1683598)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1584946403:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.97/0.79 % (1683595)Instruction limit reached! % 2.97/0.79 % (1683595)------------------------------ % 2.97/0.79 % (1683595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.97/0.79 % (1683595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.97/0.79 % (1683595)CaDiCaL version: 2.1.3 % 2.97/0.79 % (1683595)Termination reason: Instruction limit % 2.97/0.79 % (1683595)Termination phase: Property scanning % 2.97/0.79 % (1683595)Time elapsed: 0.040 s % 2.97/0.79 % (1683595)Peak memory usage: 10 MB % 2.97/0.79 % (1683595)Instructions burned: 105 (million) % 2.97/0.79 % (1683596)Instruction limit reached! % 2.97/0.79 % (1683596)------------------------------ % 2.97/0.79 % (1683596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.97/0.79 % (1683596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.97/0.79 % (1683596)CaDiCaL version: 2.1.3 % 2.97/0.79 % (1683596)Termination reason: Instruction limit % 2.97/0.79 % (1683596)Termination phase: Property scanning % 2.97/0.79 % (1683596)Time elapsed: 0.044 s % 2.97/0.79 % (1683596)Peak memory usage: 10 MB % 2.97/0.79 % (1683596)Instructions burned: 117 (million) % 2.97/0.79 % (1683592)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.97/0.79 % (1683592)Terminated due to inappropriate strategy. % 2.97/0.79 % (1683592)------------------------------ % 2.97/0.79 % (1683592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.97/0.79 % (1683592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.97/0.79 % (1683592)CaDiCaL version: 2.1.3 % 2.97/0.79 % (1683592)Termination reason: Inappropriate % 2.97/0.79 % (1683592)Time elapsed: 0.045 s % 2.97/0.79 % (1683592)Peak memory usage: 10 MB % 2.97/0.79 % (1683592)Instructions burned: 118 (million) % 2.97/0.79 % (1683592)------------------------------ % 2.97/0.79 % (1683592)------------------------------ % 2.97/0.79 % (1683597)Instruction limit reached! % 2.97/0.79 % (1683597)------------------------------ % 2.97/0.79 % (1683597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.97/0.79 % (1683597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.97/0.79 % (1683597)CaDiCaL version: 2.1.3 % 2.97/0.79 % (1683597)Termination reason: Instruction limit % 2.97/0.79 % (1683597)Termination phase: Saturation % 2.97/0.79 % (1683597)Time elapsed: 0.051 s % 2.97/0.79 % (1683597)Peak memory usage: 11 MB % 2.97/0.79 % (1683597)Instructions burned: 133 (million) % 2.97/0.79 % (1683606)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1692912273:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 2.97/0.79 % (1683598)Instruction limit reached! % 2.97/0.79 % (1683598)------------------------------ % 2.97/0.79 % (1683598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.97/0.79 % (1683598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.97/0.79 % (1683598)CaDiCaL version: 2.1.3 % 2.97/0.79 % (1683598)Termination reason: Instruction limit % 2.97/0.79 % (1683598)Termination phase: Saturation % 2.97/0.79 % (1683598)Time elapsed: 0.061 s % 2.97/0.79 % (1683598)Peak memory usage: 12 MB % 2.97/0.79 % (1683598)Instructions burned: 159 (million) % 2.97/0.79 % (1683607)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4079105976:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 4.08/0.98 % (1683608)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=3624736359:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 4.08/0.98 % (1683609)ott-21_1_sil=16000:fs=off:random_seed=2659229207:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 4.08/0.98 % (1683611)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1161654401:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 4.08/0.98 % (1683606)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.08/0.98 % (1683606)Terminated due to inappropriate strategy. % 4.08/0.98 % (1683606)------------------------------ % 4.08/0.98 % (1683606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.08/0.98 % (1683606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.08/0.98 % (1683606)CaDiCaL version: 2.1.3 % 4.08/0.98 % (1683606)Termination reason: Inappropriate % 4.08/0.98 % (1683606)Time elapsed: 0.045 s % 4.08/0.98 % (1683606)Peak memory usage: 11 MB % 4.08/0.98 % (1683606)Instructions burned: 118 (million) % 4.08/0.98 % (1683606)------------------------------ % 4.08/0.98 % (1683606)------------------------------ % 4.08/0.98 % (1683607)Instruction limit reached! % 4.08/0.98 % (1683607)------------------------------ % 4.08/0.98 % (1683607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.08/0.98 % (1683607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.08/0.98 % (1683607)CaDiCaL version: 2.1.3 % 4.08/0.98 % (1683607)Termination reason: Instruction limit % 4.08/0.98 % (1683607)Termination phase: Saturation % 4.08/0.98 % (1683607)Time elapsed: 0.051 s % 4.08/0.98 % (1683607)Peak memory usage: 12 MB % 4.08/0.98 % (1683607)Instructions burned: 131 (million) % 4.08/0.98 % (1683616)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1152264981:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 4.08/0.98 % (1683617)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1629814823:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 4.08/0.98 % (1683609)Instruction limit reached! % 4.08/0.98 % (1683609)------------------------------ % 4.08/0.98 % (1683609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.08/0.98 % (1683609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.08/0.98 % (1683609)CaDiCaL version: 2.1.3 % 4.08/0.98 % (1683609)Termination reason: Instruction limit % 4.08/0.98 % (1683609)Termination phase: Saturation % 4.08/0.98 % (1683609)Time elapsed: 0.069 s % 4.08/0.98 % (1683609)Peak memory usage: 11 MB % 4.08/0.98 % (1683609)Instructions burned: 181 (million) % 4.08/0.98 % (1683616)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.08/0.98 % (1683616)Terminated due to inappropriate strategy. % 4.08/0.98 % (1683616)------------------------------ % 4.08/0.98 % (1683616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.08/0.98 % (1683616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.08/0.98 % (1683616)CaDiCaL version: 2.1.3 % 4.08/0.98 % (1683616)Termination reason: Inappropriate % 4.08/0.98 % (1683616)Time elapsed: 0.034 s % 4.08/0.98 % (1683616)Peak memory usage: 10 MB % 4.08/0.98 % (1683616)Instructions burned: 89 (million) % 4.08/0.98 % (1683620)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1804896026:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 4.08/0.98 % (1683616)------------------------------ % 4.08/0.98 % (1683616)------------------------------ % 4.08/0.98 % (1683622)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=445289846: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) % 4.08/0.98 % (1683620)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.08/0.98 % (1683620)Terminated due to inappropriate strategy. % 4.08/0.98 % (1683620)------------------------------ % 4.08/0.98 % (1683620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.08/0.98 % (1683620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.08/0.98 % (1683620)CaDiCaL version: 2.1.3 % 4.08/0.98 % (1683620)Termination reason: Inappropriate % 4.08/0.98 % (1683620)Time elapsed: 0.035 s % 4.08/0.98 % (1683620)Peak memory usage: 10 MB % 15.96/2.65 % (1683620)Instructions burned: 89 (million) % 15.96/2.65 % (1683620)------------------------------ % 15.96/2.65 % (1683620)------------------------------ % 15.96/2.65 % (1683624)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=493953012:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 15.96/2.65 % (1683611)Instruction limit reached! % 15.96/2.65 % (1683611)------------------------------ % 15.96/2.65 % (1683611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.96/2.65 % (1683611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.96/2.65 % (1683611)CaDiCaL version: 2.1.3 % 15.96/2.65 % (1683611)Termination reason: Instruction limit % 15.96/2.65 % (1683611)Termination phase: Saturation % 15.96/2.65 % (1683611)Time elapsed: 0.184 s % 15.96/2.65 % (1683611)Peak memory usage: 13 MB % 15.96/2.65 % (1683611)Instructions burned: 478 (million) % 15.96/2.65 % (1683626)fmb+10_1_sil=64000:random_seed=720813944:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 15.96/2.65 % (1683626)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 15.96/2.65 % (1683626)Terminated due to inappropriate strategy. % 15.96/2.65 % (1683626)------------------------------ % 15.96/2.65 % (1683626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.96/2.65 % (1683626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.96/2.65 % (1683626)CaDiCaL version: 2.1.3 % 15.96/2.65 % (1683626)Termination reason: Inappropriate % 15.96/2.65 % (1683626)Time elapsed: 0.045 s % 15.96/2.65 % (1683626)Peak memory usage: 11 MB % 15.96/2.65 % (1683626)Instructions burned: 118 (million) % 15.96/2.65 % (1683626)------------------------------ % 15.96/2.65 % (1683626)------------------------------ % 15.96/2.65 % (1683608)Instruction limit reached! % 15.96/2.65 % (1683608)------------------------------ % 15.96/2.65 % (1683608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.96/2.65 % (1683608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.96/2.65 % (1683608)CaDiCaL version: 2.1.3 % 15.96/2.65 % (1683608)Termination reason: Instruction limit % 15.96/2.65 % (1683608)Termination phase: Saturation % 15.96/2.65 % (1683608)Time elapsed: 0.279 s % 15.96/2.65 % (1683608)Peak memory usage: 15 MB % 15.96/2.65 % (1683608)Instructions burned: 685 (million) % 15.96/2.65 % (1683628)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2393327588:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 15.96/2.65 % (1683629)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1569477920:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 15.96/2.65 % (1683628)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 15.96/2.65 % (1683628)Terminated due to inappropriate strategy. % 15.96/2.65 % (1683628)------------------------------ % 15.96/2.65 % (1683628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.96/2.65 % (1683628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.96/2.65 % (1683628)CaDiCaL version: 2.1.3 % 15.96/2.65 % (1683628)Termination reason: Inappropriate % 15.96/2.65 % (1683628)Time elapsed: 0.045 s % 15.96/2.65 % (1683628)Peak memory usage: 10 MB % 15.96/2.65 % (1683628)Instructions burned: 118 (million) % 15.96/2.65 % (1683628)------------------------------ % 15.96/2.65 % (1683628)------------------------------ % 15.96/2.65 % (1683629)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 15.96/2.65 % (1683629)Terminated due to inappropriate strategy. % 15.96/2.65 % (1683629)------------------------------ % 15.96/2.65 % (1683629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.96/2.65 % (1683629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.96/2.65 % (1683629)CaDiCaL version: 2.1.3 % 15.96/2.65 % (1683629)Termination reason: Inappropriate % 15.96/2.65 % (1683629)Time elapsed: 0.045 s % 15.96/2.65 % (1683629)Peak memory usage: 10 MB % 15.96/2.65 % (1683629)Instructions burned: 118 (million) % 15.96/2.65 % (1683629)------------------------------ % 15.96/2.65 % (1683629)------------------------------ % 15.96/2.65 % (1683632)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2808738221:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 15.96/2.65 % (1683633)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=749420355:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 15.96/2.65 % (1683622)Instruction limit reached! % 14.89/2.88 % (1683622)------------------------------ % 14.89/2.88 % (1683622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.89/2.88 % (1683622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.89/2.88 % (1683622)CaDiCaL version: 2.1.3 % 14.89/2.88 % (1683622)Termination reason: Instruction limit % 14.89/2.88 % (1683622)Termination phase: Saturation % 14.89/2.88 % (1683622)Time elapsed: 0.302 s % 14.89/2.88 % (1683622)Peak memory usage: 17 MB % 14.89/2.88 % (1683622)Instructions burned: 693 (million) % 14.89/2.88 % (1683636)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=420038663:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 14.89/2.88 % (1683636)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 14.89/2.88 % (1683636)Terminated due to inappropriate strategy. % 14.89/2.88 % (1683636)------------------------------ % 14.89/2.88 % (1683636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.89/2.88 % (1683636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.89/2.88 % (1683636)CaDiCaL version: 2.1.3 % 14.89/2.88 % (1683636)Termination reason: Inappropriate % 14.89/2.88 % (1683636)Time elapsed: 0.045 s % 14.89/2.88 % (1683636)Peak memory usage: 10 MB % 14.89/2.88 % (1683636)Instructions burned: 118 (million) % 14.89/2.88 % (1683636)------------------------------ % 14.89/2.88 % (1683636)------------------------------ % 14.89/2.88 % (1683624)Instruction limit reached! % 14.89/2.88 % (1683624)------------------------------ % 14.89/2.88 % (1683624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.89/2.88 % (1683624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.89/2.88 % (1683624)CaDiCaL version: 2.1.3 % 14.89/2.88 % (1683624)Termination reason: Instruction limit % 14.89/2.88 % (1683624)Termination phase: Saturation % 14.89/2.88 % (1683624)Time elapsed: 0.334 s % 14.89/2.88 % (1683624)Peak memory usage: 14 MB % 14.89/2.88 % (1683624)Instructions burned: 879 (million) % 14.89/2.88 % (1683638)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3119234439:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 14.89/2.88 % (1683639)ott-2_1_sil=16000:newcnf=on:random_seed=977647697:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 14.89/2.88 % (1683617)Instruction limit reached! % 14.89/2.88 % (1683617)------------------------------ % 14.89/2.88 % (1683617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.89/2.88 % (1683617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.89/2.88 % (1683617)CaDiCaL version: 2.1.3 % 14.89/2.88 % (1683617)Termination reason: Instruction limit % 14.89/2.88 % (1683617)Termination phase: Saturation % 14.89/2.88 % (1683617)Time elapsed: 0.457 s % 14.89/2.88 % (1683617)Peak memory usage: 16 MB % 14.89/2.88 % (1683617)Instructions burned: 1179 (million) % 14.89/2.88 % (1683642)ott+10_1_sil=32000:tgt=ground:random_seed=903990313:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 14.89/2.88 % (1683638)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 14.89/2.88 % (1683638)Terminated due to inappropriate strategy. % 14.89/2.88 % (1683638)------------------------------ % 14.89/2.88 % (1683638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.89/2.88 % (1683638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.89/2.88 % (1683638)CaDiCaL version: 2.1.3 % 14.89/2.88 % (1683638)Termination reason: Inappropriate % 14.89/2.88 % (1683638)Time elapsed: 0.046 s % 14.89/2.88 % (1683638)Peak memory usage: 11 MB % 14.89/2.88 % (1683638)Instructions burned: 118 (million) % 14.89/2.88 % (1683638)------------------------------ % 14.89/2.88 % (1683638)------------------------------ % 14.89/2.88 % (1683644)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3363753180:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 14.89/2.88 % (1683644)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 14.89/2.88 % (1683644)Terminated due to inappropriate strategy. % 14.89/2.88 % (1683644)------------------------------ % 14.89/2.88 % (1683644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.89/2.88 % (1683644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.89/2.88 % (1683644)CaDiCaL version: 2.1.3 % 14.89/2.88 % (1683644)Termination reason: Inappropriate % 14.89/2.88 % (1683644)Time elapsed: 0.045 s % 14.89/2.88 % (1683644)Peak memory usage: 10 MB % 14.89/2.88 % (1683644)Instructions burned: 118 (million) % 83.49/12.08 % (1683644)------------------------------ % 83.49/12.08 % (1683644)------------------------------ % 83.49/12.08 % (1683646)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=336346487:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 83.49/12.08 % (1683639)Instruction limit reached! % 83.49/12.08 % (1683639)------------------------------ % 83.49/12.08 % (1683639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.49/12.08 % (1683639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.49/12.08 % (1683639)CaDiCaL version: 2.1.3 % 83.49/12.08 % (1683639)Termination reason: Instruction limit % 83.49/12.08 % (1683639)Termination phase: Saturation % 83.49/12.08 % (1683639)Time elapsed: 0.374 s % 83.49/12.08 % (1683639)Peak memory usage: 18 MB % 83.49/12.08 % (1683639)Instructions burned: 871 (million) % 83.49/12.08 % (1683648)dis+21_1_sil=32000:sas=cadical:random_seed=3036250657:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 83.49/12.08 % (1683633)Instruction limit reached! % 83.49/12.08 % (1683633)------------------------------ % 83.49/12.08 % (1683633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.49/12.08 % (1683633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.49/12.08 % (1683633)CaDiCaL version: 2.1.3 % 83.49/12.08 % (1683633)Termination reason: Instruction limit % 83.49/12.08 % (1683633)Termination phase: Saturation % 83.49/12.08 % (1683633)Time elapsed: 0.578 s % 83.49/12.08 % (1683633)Peak memory usage: 15 MB % 83.49/12.08 % (1683633)Instructions burned: 1473 (million) % 83.49/12.08 % (1683650)ott+11_1_sil=16000:gs=on:random_seed=2297408802:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi) % 83.49/12.08 % (1683650)Instruction limit reached! % 83.49/12.08 % (1683650)------------------------------ % 83.49/12.08 % (1683650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.49/12.08 % (1683650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.49/12.08 % (1683650)CaDiCaL version: 2.1.3 % 83.49/12.08 % (1683650)Termination reason: Instruction limit % 83.49/12.08 % (1683650)Termination phase: Saturation % 83.49/12.08 % (1683650)Time elapsed: 0.842 s % 83.49/12.08 % (1683650)Peak memory usage: 15 MB % 83.49/12.08 % (1683650)Instructions burned: 2251 (million) % 83.49/12.08 % (1683652)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3896083647:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 83.49/12.08 % (1683652)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 83.49/12.08 % (1683652)Terminated due to inappropriate strategy. % 83.49/12.08 % (1683652)------------------------------ % 83.49/12.08 % (1683652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.49/12.08 % (1683652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.49/12.08 % (1683652)CaDiCaL version: 2.1.3 % 83.49/12.08 % (1683652)Termination reason: Inappropriate % 83.49/12.08 % (1683652)Time elapsed: 0.045 s % 83.49/12.08 % (1683652)Peak memory usage: 10 MB % 83.49/12.08 % (1683652)Instructions burned: 118 (million) % 83.49/12.08 % (1683652)------------------------------ % 83.49/12.08 % (1683652)------------------------------ % 83.49/12.08 % (1683654)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3338611572:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2979 on theBenchmark for (2979ds/4591Mi) % 83.49/12.08 % (1683646)Instruction limit reached! % 83.49/12.08 % (1683646)------------------------------ % 83.49/12.08 % (1683646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.49/12.08 % (1683646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.49/12.08 % (1683646)CaDiCaL version: 2.1.3 % 83.49/12.08 % (1683646)Termination reason: Instruction limit % 83.49/12.08 % (1683646)Termination phase: Saturation % 83.49/12.08 % (1683646)Time elapsed: 1.342 s % 83.49/12.08 % (1683646)Peak memory usage: 15 MB % 83.49/12.08 % (1683646)Instructions burned: 3512 (million) % 83.49/12.08 % (1683656)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3881651452:i=29340_2978 on theBenchmark for (2978ds/29340Mi) % 83.49/12.08 % (1683632)Instruction limit reached! % 83.49/12.08 % (1683632)------------------------------ % 83.49/12.08 % (1683632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.49/12.08 % (1683632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.49/12.08 % (1683632)CaDiCaL version: 2.1.3 % 93.83/13.55 % (1683632)Termination reason: Instruction limit % 93.83/13.55 % (1683632)Termination phase: Saturation % 93.83/13.55 % (1683632)Time elapsed: 1.929 s % 93.83/13.55 % (1683632)Peak memory usage: 15 MB % 93.83/13.55 % (1683632)Instructions burned: 5132 (million) % 93.83/13.55 % (1683658)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=869816063:i=5211_2975 on theBenchmark for (2975ds/5211Mi) % 93.83/13.55 % (1683648)Instruction limit reached! % 93.83/13.55 % (1683648)------------------------------ % 93.83/13.55 % (1683648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.83/13.55 % (1683648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.83/13.55 % (1683648)CaDiCaL version: 2.1.3 % 93.83/13.55 % (1683648)Termination reason: Instruction limit % 93.83/13.55 % (1683648)Termination phase: Saturation % 93.83/13.55 % (1683648)Time elapsed: 1.418 s % 93.83/13.55 % (1683648)Peak memory usage: 15 MB % 93.83/13.55 % (1683648)Instructions burned: 3773 (million) % 93.83/13.55 % (1683660)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=281185937:i=5497:nm=2_2975 on theBenchmark for (2975ds/5497Mi) % 93.83/13.55 % (1683660)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 93.83/13.55 % (1683660)Terminated due to inappropriate strategy. % 93.83/13.55 % (1683660)------------------------------ % 93.83/13.55 % (1683660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.83/13.55 % (1683660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.83/13.55 % (1683660)CaDiCaL version: 2.1.3 % 93.83/13.55 % (1683660)Termination reason: Inappropriate % 93.83/13.55 % (1683660)Time elapsed: 0.045 s % 93.83/13.55 % (1683660)Peak memory usage: 10 MB % 93.83/13.55 % (1683660)Instructions burned: 118 (million) % 93.83/13.55 % (1683660)------------------------------ % 93.83/13.55 % (1683660)------------------------------ % 93.83/13.55 % (1683662)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2405867810:fmbsr=2:i=46332_2974 on theBenchmark for (2974ds/46332Mi) % 93.83/13.55 % (1683642)Instruction limit reached! % 93.83/13.55 % (1683642)------------------------------ % 93.83/13.55 % (1683642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.83/13.55 % (1683642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.83/13.55 % (1683642)CaDiCaL version: 2.1.3 % 93.83/13.55 % (1683642)Termination reason: Instruction limit % 93.83/13.55 % (1683642)Termination phase: Saturation % 93.83/13.55 % (1683642)Time elapsed: 1.881 s % 93.83/13.55 % (1683642)Peak memory usage: 15 MB % 93.83/13.55 % (1683642)Instructions burned: 5115 (million) % 93.83/13.55 % (1683664)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1854306094:i=14071_2974 on theBenchmark for (2974ds/14071Mi) % 93.83/13.55 % (1683662)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 93.83/13.55 % (1683662)Terminated due to inappropriate strategy. % 93.83/13.55 % (1683662)------------------------------ % 93.83/13.55 % (1683662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.83/13.55 % (1683662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.83/13.55 % (1683662)CaDiCaL version: 2.1.3 % 93.83/13.55 % (1683662)Termination reason: Inappropriate % 93.83/13.55 % (1683662)Time elapsed: 0.045 s % 93.83/13.55 % (1683662)Peak memory usage: 10 MB % 93.83/13.55 % (1683662)Instructions burned: 118 (million) % 93.83/13.55 % (1683662)------------------------------ % 93.83/13.55 % (1683662)------------------------------ % 93.83/13.55 % (1683666)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3632482720:i=22565:add=on:rawr=on_2974 on theBenchmark for (2974ds/22565Mi) % 93.83/13.55 % (1683664)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 93.83/13.55 % (1683664)Terminated due to inappropriate strategy. % 93.83/13.55 % (1683664)------------------------------ % 93.83/13.55 % (1683664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.83/13.55 % (1683664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.83/13.55 % (1683664)CaDiCaL version: 2.1.3 % 93.83/13.55 % (1683664)Termination reason: Inappropriate % 93.83/13.55 % (1683664)Time elapsed: 0.045 s % 93.83/13.55 % (1683664)Peak memory usage: 10 MB % 93.83/13.55 % (1683664)Instructions burned: 118 (million) % 93.83/13.55 % (1683664)------------------------------ % 93.83/13.55 % (1683664)------------------------------ % 93.83/13.55 % (1683668)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=372606837:i=8173:av=off_2973 on theBenchmark for (2973ds/8173Mi) % 95.68/13.88 % (1683658)Instruction limit reached! % 95.68/13.88 % (1683658)------------------------------ % 95.68/13.88 % (1683658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.68/13.88 % (1683658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.68/13.88 % (1683658)CaDiCaL version: 2.1.3 % 95.68/13.88 % (1683658)Termination reason: Instruction limit % 95.68/13.88 % (1683658)Termination phase: Saturation % 95.68/13.88 % (1683658)Time elapsed: 1.962 s % 95.68/13.88 % (1683658)Peak memory usage: 17 MB % 95.68/13.88 % (1683658)Instructions burned: 5212 (million) % 95.68/13.88 % (1683670)dis+10_16:1_sil=16000:random_seed=3462164891:i=9155:fsr=off_2955 on theBenchmark for (2955ds/9155Mi) % 95.68/13.88 % (1683654)Instruction limit reached! % 95.68/13.88 % (1683654)------------------------------ % 95.68/13.88 % (1683654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.68/13.88 % (1683654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.68/13.88 % (1683654)CaDiCaL version: 2.1.3 % 95.68/13.88 % (1683654)Termination reason: Instruction limit % 95.68/13.88 % (1683654)Termination phase: Saturation % 95.68/13.88 % (1683654)Time elapsed: 2.446 s % 95.68/13.88 % (1683654)Peak memory usage: 40 MB % 95.68/13.88 % (1683654)Instructions burned: 4593 (million) % 95.68/13.88 % (1683672)ott-3_8_sil=64000:random_seed=14508213:i=20139:bs=on_2955 on theBenchmark for (2955ds/20139Mi) % 95.68/13.88 % (1683668)Instruction limit reached! % 95.68/13.88 % (1683668)------------------------------ % 95.68/13.88 % (1683668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.68/13.88 % (1683668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.68/13.88 % (1683668)CaDiCaL version: 2.1.3 % 95.68/13.88 % (1683668)Termination reason: Instruction limit % 95.68/13.88 % (1683668)Termination phase: Saturation % 95.68/13.88 % (1683668)Time elapsed: 3.048 s % 95.68/13.88 % (1683668)Peak memory usage: 16 MB % 95.68/13.88 % (1683668)Instructions burned: 8173 (million) % 95.68/13.88 % (1683674)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=167772334:fmbsr=2:i=32576_2943 on theBenchmark for (2943ds/32576Mi) % 95.68/13.88 % (1683674)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 95.68/13.88 % (1683674)Terminated due to inappropriate strategy. % 95.68/13.88 % (1683674)------------------------------ % 95.68/13.88 % (1683674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.68/13.88 % (1683674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.68/13.88 % (1683674)CaDiCaL version: 2.1.3 % 95.68/13.88 % (1683674)Termination reason: Inappropriate % 95.68/13.88 % (1683674)Time elapsed: 0.045 s % 95.68/13.88 % (1683674)Peak memory usage: 10 MB % 95.68/13.88 % (1683674)Instructions burned: 118 (million) % 95.68/13.88 % (1683674)------------------------------ % 95.68/13.88 % (1683674)------------------------------ % 95.68/13.88 % (1683676)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3984192910:i=11404_2942 on theBenchmark for (2942ds/11404Mi) % 95.68/13.88 % (1683670)Instruction limit reached! % 95.68/13.88 % (1683670)------------------------------ % 95.68/13.88 % (1683670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.68/13.88 % (1683670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.68/13.88 % (1683670)CaDiCaL version: 2.1.3 % 95.68/13.88 % (1683670)Termination reason: Instruction limit % 95.68/13.88 % (1683670)Termination phase: Saturation % 95.68/13.88 % (1683670)Time elapsed: 3.441 s % 95.68/13.88 % (1683670)Peak memory usage: 17 MB % 95.68/13.88 % (1683670)Instructions burned: 9155 (million) % 95.68/13.88 % (1683678)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2723533996:i=14134_2921 on theBenchmark for (2921ds/14134Mi) % 95.68/13.88 % (1683676)Instruction limit reached! % 95.68/13.88 % (1683676)------------------------------ % 95.68/13.88 % (1683676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.68/13.88 % (1683676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.68/13.88 % (1683676)CaDiCaL version: 2.1.3 % 95.68/13.88 % (1683676)Termination reason: Instruction limit % 95.68/13.88 % (1683676)Termination phase: Saturation % 95.68/13.88 % (1683676)Time elapsed: 4.230 s % 95.68/13.88 % (1683676)Peak memory usage: 16 MB % 95.68/13.88 % (1683676)Instructions burned: 11404 (million) % 95.68/13.88 % (1683681)dis+33_16_sil=32000:sac=on:random_seed=3696462463:i=15851:nm=0_2899 on theBenchmark for (2899ds/15851Mi) % 95.68/13.88 % (1683672)Instruction limit reached! % 95.68/13.88 % (1683672)------------------------------ % 140.89/20.16 % (1683672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.89/20.16 % (1683672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.89/20.16 % (1683672)CaDiCaL version: 2.1.3 % 140.89/20.16 % (1683672)Termination reason: Instruction limit % 140.89/20.16 % (1683672)Termination phase: Saturation % 140.89/20.16 % (1683672)Time elapsed: 7.348 s % 140.89/20.16 % (1683672)Peak memory usage: 18 MB % 140.89/20.16 % (1683672)Instructions burned: 20142 (million) % 140.89/20.16 % (1683683)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1726941519:avsq=on:i=17627:add=on:amm=off_2881 on theBenchmark for (2881ds/17627Mi) % 140.89/20.16 % (1683666)Instruction limit reached! % 140.89/20.16 % (1683666)------------------------------ % 140.89/20.16 % (1683666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.89/20.16 % (1683666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.89/20.16 % (1683666)CaDiCaL version: 2.1.3 % 140.89/20.16 % (1683666)Termination reason: Instruction limit % 140.89/20.16 % (1683666)Termination phase: Saturation % 140.89/20.16 % (1683666)Time elapsed: 9.267 s % 140.89/20.16 % (1683666)Peak memory usage: 17 MB % 140.89/20.16 % (1683666)Instructions burned: 22566 (million) % 140.89/20.16 % (1683685)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2092521740:s2a=on:i=53295_2881 on theBenchmark for (2881ds/53295Mi) % 140.89/20.16 % (1683678)Instruction limit reached! % 140.89/20.16 % (1683678)------------------------------ % 140.89/20.16 % (1683678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.89/20.16 % (1683678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.89/20.16 % (1683678)CaDiCaL version: 2.1.3 % 140.89/20.16 % (1683678)Termination reason: Instruction limit % 140.89/20.16 % (1683678)Termination phase: Saturation % 140.89/20.16 % (1683678)Time elapsed: 5.284 s % 140.89/20.16 % (1683678)Peak memory usage: 16 MB % 140.89/20.16 % (1683678)Instructions burned: 14135 (million) % 140.89/20.16 % (1683687)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=758094649:i=26857:ins=20_2868 on theBenchmark for (2868ds/26857Mi) % 140.89/20.16 % (1683656)Instruction limit reached! % 140.89/20.16 % (1683656)------------------------------ % 140.89/20.16 % (1683656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.89/20.16 % (1683656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.89/20.16 % (1683656)CaDiCaL version: 2.1.3 % 140.89/20.16 % (1683656)Termination reason: Instruction limit % 140.89/20.16 % (1683656)Termination phase: Saturation % 140.89/20.16 % (1683656)Time elapsed: 11.083 s % 140.89/20.16 % (1683656)Peak memory usage: 16 MB % 140.89/20.16 % (1683656)Instructions burned: 29342 (million) % 140.89/20.16 % (1683687)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 140.89/20.16 % (1683687)Terminated due to inappropriate strategy. % 140.89/20.16 % (1683687)------------------------------ % 140.89/20.16 % (1683687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.89/20.16 % (1683687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.89/20.16 % (1683687)CaDiCaL version: 2.1.3 % 140.89/20.16 % (1683687)Termination reason: Inappropriate % 140.89/20.16 % (1683687)Time elapsed: 0.045 s % 140.89/20.16 % (1683687)Peak memory usage: 10 MB % 140.89/20.16 % (1683687)Instructions burned: 118 (million) % 140.89/20.16 % (1683687)------------------------------ % 140.89/20.16 % (1683687)------------------------------ % 140.89/20.16 % (1683689)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1277249791:i=28120:bs=on:fsr=off_2867 on theBenchmark for (2867ds/28120Mi) % 140.89/20.16 % (1683690)fmb+10_1_sil=256000:fmbss=7:random_seed=3922818113:fmbsr=1.6:i=182295_2867 on theBenchmark for (2867ds/182295Mi) % 140.89/20.16 % (1683690)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 140.89/20.16 % (1683690)Terminated due to inappropriate strategy. % 140.89/20.16 % (1683690)------------------------------ % 140.89/20.16 % (1683690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.89/20.16 % (1683690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.89/20.16 % (1683690)CaDiCaL version: 2.1.3 % 140.89/20.16 % (1683690)Termination reason: Inappropriate % 140.89/20.16 % (1683690)Time elapsed: 0.045 s % 140.89/20.16 % (1683690)Peak memory usage: 10 MB % 140.89/20.16 % (1683690)Instructions burned: 118 (million) % 140.89/20.16 % (1683690)------------------------------ % 140.89/20.16 % (1683690)------------------------------ % 140.89/20.16 % (1683693)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1685202034:i=44625:gsp=on_2867 on theBenchmark for (2867ds/44625Mi) % 143.51/20.50 % (1683693)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.51/20.50 % (1683693)Terminated due to inappropriate strategy. % 143.51/20.50 % (1683693)------------------------------ % 143.51/20.50 % (1683693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.51/20.50 % (1683693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.51/20.50 % (1683693)CaDiCaL version: 2.1.3 % 143.51/20.50 % (1683693)Termination reason: Inappropriate % 143.51/20.50 % (1683693)Time elapsed: 0.045 s % 143.51/20.50 % (1683693)Peak memory usage: 11 MB % 143.51/20.50 % (1683693)Instructions burned: 118 (million) % 143.51/20.50 % (1683693)------------------------------ % 143.51/20.50 % (1683693)------------------------------ % 143.51/20.50 % (1683695)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2327239009:i=160505_2866 on theBenchmark for (2866ds/160505Mi) % 143.51/20.50 % (1683695)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.51/20.50 % (1683695)Terminated due to inappropriate strategy. % 143.51/20.50 % (1683695)------------------------------ % 143.51/20.50 % (1683695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.51/20.50 % (1683695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.51/20.50 % (1683695)CaDiCaL version: 2.1.3 % 143.51/20.50 % (1683695)Termination reason: Inappropriate % 143.51/20.50 % (1683695)Time elapsed: 0.045 s % 143.51/20.50 % (1683695)Peak memory usage: 10 MB % 143.51/20.50 % (1683695)Instructions burned: 118 (million) % 143.51/20.50 % (1683695)------------------------------ % 143.51/20.50 % (1683695)------------------------------ % 143.51/20.50 % (1683697)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1659082294:fmbsr=1.3:i=225729_2865 on theBenchmark for (2865ds/225729Mi) % 143.51/20.50 % (1683697)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.51/20.50 % (1683697)Terminated due to inappropriate strategy. % 143.51/20.50 % (1683697)------------------------------ % 143.51/20.50 % (1683697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.51/20.50 % (1683697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.51/20.50 % (1683697)CaDiCaL version: 2.1.3 % 143.51/20.50 % (1683697)Termination reason: Inappropriate % 143.51/20.50 % (1683697)Time elapsed: 0.045 s % 143.51/20.50 % (1683697)Peak memory usage: 10 MB % 143.51/20.50 % (1683697)Instructions burned: 118 (million) % 143.51/20.50 % (1683697)------------------------------ % 143.51/20.50 % (1683697)------------------------------ % 143.51/20.50 % (1683699)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2555810230:fmbsr=2:i=185024:ins=7_2865 on theBenchmark for (2865ds/185024Mi) % 143.51/20.50 % (1683699)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.51/20.50 % (1683699)Terminated due to inappropriate strategy. % 143.51/20.50 % (1683699)------------------------------ % 143.51/20.50 % (1683699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.51/20.50 % (1683699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.51/20.50 % (1683699)CaDiCaL version: 2.1.3 % 143.51/20.50 % (1683699)Termination reason: Inappropriate % 143.51/20.50 % (1683699)Time elapsed: 0.045 s % 143.51/20.50 % (1683699)Peak memory usage: 10 MB % 143.51/20.50 % (1683699)Instructions burned: 118 (million) % 143.51/20.50 % (1683699)------------------------------ % 143.51/20.50 % (1683699)------------------------------ % 143.51/20.50 % (1683701)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1451382661:rtra=on_2864 on theBenchmark for (2864ds/0Mi) % 143.51/20.50 % (1683701)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.51/20.50 % (1683701)Terminated due to inappropriate strategy. % 143.51/20.50 % (1683701)------------------------------ % 143.51/20.50 % (1683701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.51/20.50 % (1683701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.51/20.50 % (1683701)CaDiCaL version: 2.1.3 % 143.51/20.50 % (1683701)Termination reason: Inappropriate % 143.51/20.50 % (1683701)Time elapsed: 0.045 s % 143.51/20.50 % (1683701)Peak memory usage: 10 MB % 143.51/20.50 % (1683701)Instructions burned: 118 (million) % 143.51/20.50 % (1683701)------------------------------ % 143.51/20.50 % (1683701)------------------------------ % 143.51/20.50 % (1683703)% WARNING: option uhcvi not known. % 143.51/20.50 % (1683703)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1190763344:i=271062:add=off:rtra=on:rawr=on_2863 on theBenchmark for (2863ds/271062Mi) % 149.95/21.40 % (1683681)Instruction limit reached! % 149.95/21.40 % (1683681)------------------------------ % 149.95/21.40 % (1683681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.95/21.40 % (1683681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.95/21.40 % (1683681)CaDiCaL version: 2.1.3 % 149.95/21.40 % (1683681)Termination reason: Instruction limit % 149.95/21.40 % (1683681)Termination phase: Saturation % 149.95/21.40 % (1683681)Time elapsed: 6.003 s % 149.95/21.40 % (1683681)Peak memory usage: 20 MB % 149.95/21.40 % (1683681)Instructions burned: 15852 (million) % 149.95/21.40 % (1683705)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=547922741:i=176048:add=on:rtra=on:rawr=on_2839 on theBenchmark for (2839ds/176048Mi) % 149.95/21.40 % (1683683)Instruction limit reached! % 149.95/21.40 % (1683683)------------------------------ % 149.95/21.40 % (1683683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.95/21.40 % (1683683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.95/21.40 % (1683683)CaDiCaL version: 2.1.3 % 149.95/21.40 % (1683683)Termination reason: Instruction limit % 149.95/21.40 % (1683683)Termination phase: Saturation % 149.95/21.40 % (1683683)Time elapsed: 7.521 s % 149.95/21.40 % (1683683)Peak memory usage: 92 MB % 149.95/21.40 % (1683683)Instructions burned: 17630 (million) % 149.95/21.40 % (1683707)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1699857247:i=206:fgj=on:rtra=on_2806 on theBenchmark for (2806ds/206Mi) % 149.95/21.40 % (1683707)Instruction limit reached! % 149.95/21.40 % (1683707)------------------------------ % 149.95/21.40 % (1683707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.95/21.40 % (1683707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.95/21.40 % (1683707)CaDiCaL version: 2.1.3 % 149.95/21.40 % (1683707)Termination reason: Instruction limit % 149.95/21.40 % (1683707)Termination phase: Saturation % 149.95/21.40 % (1683707)Time elapsed: 0.083 s % 149.95/21.40 % (1683707)Peak memory usage: 13 MB % 149.95/21.40 % (1683707)Instructions burned: 208 (million) % 149.95/21.40 % (1683709)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1016792100:i=232:rtra=on_2804 on theBenchmark for (2804ds/232Mi) % 149.95/21.40 % (1683709)Instruction limit reached! % 149.95/21.40 % (1683709)------------------------------ % 149.95/21.40 % (1683709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.95/21.40 % (1683709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.95/21.40 % (1683709)CaDiCaL version: 2.1.3 % 149.95/21.40 % (1683709)Termination reason: Instruction limit % 149.95/21.40 % (1683709)Termination phase: Saturation % 149.95/21.40 % (1683709)Time elapsed: 0.118 s % 149.95/21.40 % (1683709)Peak memory usage: 14 MB % 149.95/21.40 % (1683709)Instructions burned: 232 (million) % 149.95/21.40 % (1683711)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1135104721:i=262:rtra=on_2803 on theBenchmark for (2803ds/262Mi) % 149.95/21.40 % (1683711)Instruction limit reached! % 149.95/21.40 % (1683711)------------------------------ % 149.95/21.40 % (1683711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.95/21.40 % (1683711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.95/21.40 % (1683711)CaDiCaL version: 2.1.3 % 149.95/21.40 % (1683711)Termination reason: Instruction limit % 149.95/21.40 % (1683711)Termination phase: Saturation % 149.95/21.40 % (1683711)Time elapsed: 0.106 s % 149.95/21.40 % (1683711)Peak memory usage: 12 MB % 149.95/21.40 % (1683711)Instructions burned: 273 (million) % 149.95/21.40 % (1683713)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3560520878:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2802 on theBenchmark for (2802ds/318Mi) % 149.95/21.40 % (1683594)Instruction limit reached! % 149.95/21.40 % (1683594)------------------------------ % 149.95/21.40 % (1683594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.95/21.40 % (1683594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.95/21.40 % (1683594)CaDiCaL version: 2.1.3 % 149.95/21.40 % (1683594)Termination reason: Instruction limit % 149.95/21.40 % (1683594)Termination phase: Saturation % 149.95/21.40 % (1683594)Time elapsed: 19.832 s % 149.95/21.40 % (1683594)Peak memory usage: 91 MB % 149.95/21.40 % (1683594)Instructions burned: 88028 (million) % 149.95/21.40 % (1683715)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3005838003:i=1428:nm=2:rtra=on_2800 on theBenchmark for (2800ds/1428Mi) % 154.44/22.13 % (1683713)Instruction limit reached! % 154.44/22.13 % (1683713)------------------------------ % 154.44/22.13 % (1683713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.44/22.13 % (1683713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.44/22.13 % (1683713)CaDiCaL version: 2.1.3 % 154.44/22.13 % (1683713)Termination reason: Instruction limit % 154.44/22.13 % (1683713)Termination phase: Saturation % 154.44/22.13 % (1683713)Time elapsed: 0.137 s % 154.44/22.13 % (1683713)Peak memory usage: 14 MB % 154.44/22.13 % (1683713)Instructions burned: 319 (million) % 154.44/22.13 % (1683717)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3244725094:i=262:bd=preordered:rtra=on:fsd=on_2800 on theBenchmark for (2800ds/262Mi) % 154.44/22.13 % (1683715)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.44/22.13 % (1683715)Terminated due to inappropriate strategy. % 154.44/22.13 % (1683715)------------------------------ % 154.44/22.13 % (1683715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.44/22.13 % (1683715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.44/22.13 % (1683715)CaDiCaL version: 2.1.3 % 154.44/22.13 % (1683715)Termination reason: Inappropriate % 154.44/22.13 % (1683715)Time elapsed: 0.024 s % 154.44/22.13 % (1683715)Peak memory usage: 10 MB % 154.44/22.13 % (1683715)Instructions burned: 118 (million) % 154.44/22.13 % (1683715)------------------------------ % 154.44/22.13 % (1683715)------------------------------ % 154.44/22.13 % (1683719)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=2661994139:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2800 on theBenchmark for (2800ds/1368Mi) % 154.44/22.13 % (1683717)Instruction limit reached! % 154.44/22.13 % (1683717)------------------------------ % 154.44/22.13 % (1683717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.44/22.13 % (1683717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.44/22.13 % (1683717)CaDiCaL version: 2.1.3 % 154.44/22.13 % (1683717)Termination reason: Instruction limit % 154.44/22.13 % (1683717)Termination phase: Saturation % 154.44/22.13 % (1683717)Time elapsed: 0.107 s % 154.44/22.13 % (1683717)Peak memory usage: 14 MB % 154.44/22.13 % (1683717)Instructions burned: 262 (million) % 154.44/22.13 % (1683721)ott-21_1_sil=16000:si=on:fs=off:random_seed=1376888522:i=360:av=off:fsr=off:rtra=on_2799 on theBenchmark for (2799ds/360Mi) % 154.44/22.13 % (1683721)Instruction limit reached! % 154.44/22.13 % (1683721)------------------------------ % 154.44/22.13 % (1683721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.44/22.13 % (1683721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.44/22.13 % (1683721)CaDiCaL version: 2.1.3 % 154.44/22.13 % (1683721)Termination reason: Instruction limit % 154.44/22.13 % (1683721)Termination phase: Saturation % 154.44/22.13 % (1683721)Time elapsed: 0.138 s % 154.44/22.13 % (1683721)Peak memory usage: 12 MB % 154.44/22.13 % (1683721)Instructions burned: 361 (million) % 154.44/22.13 % (1683723)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2388712518:i=954:bd=all:rtra=on_2797 on theBenchmark for (2797ds/954Mi) % 154.44/22.13 % (1683719)Instruction limit reached! % 154.44/22.13 % (1683719)------------------------------ % 154.44/22.13 % (1683719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.44/22.13 % (1683719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.44/22.13 % (1683719)CaDiCaL version: 2.1.3 % 154.44/22.13 % (1683719)Termination reason: Instruction limit % 154.44/22.13 % (1683719)Termination phase: Saturation % 154.44/22.13 % (1683719)Time elapsed: 0.282 s % 154.44/22.13 % (1683719)Peak memory usage: 16 MB % 154.44/22.13 % (1683719)Instructions burned: 1371 (million) % 154.44/22.13 % (1683725)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=963940768:fmbsr=1.3:i=1730:ins=25:rtra=on_2797 on theBenchmark for (2797ds/1730Mi) % 154.44/22.13 % (1683725)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.44/22.13 % (1683725)Terminated due to inappropriate strategy. % 154.44/22.13 % (1683725)------------------------------ % 154.44/22.13 % (1683725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.44/22.13 % (1683725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.44/22.13 % (1683725)CaDiCaL version: 2.1.3 % 177.63/25.39 % (1683725)Termination reason: Inappropriate % 177.63/25.39 % (1683725)Time elapsed: 0.018 s % 177.63/25.39 % (1683725)Peak memory usage: 10 MB % 177.63/25.39 % (1683725)Instructions burned: 90 (million) % 177.63/25.39 % (1683725)------------------------------ % 177.63/25.39 % (1683725)------------------------------ % 177.63/25.39 % (1683727)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=461176738:i=2358:rtra=on_2797 on theBenchmark for (2797ds/2358Mi) % 177.63/25.39 % (1683723)Instruction limit reached! % 177.63/25.39 % (1683723)------------------------------ % 177.63/25.39 % (1683723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.63/25.39 % (1683723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.63/25.39 % (1683723)CaDiCaL version: 2.1.3 % 177.63/25.39 % (1683723)Termination reason: Instruction limit % 177.63/25.39 % (1683723)Termination phase: Saturation % 177.63/25.39 % (1683723)Time elapsed: 0.378 s % 177.63/25.39 % (1683723)Peak memory usage: 14 MB % 177.63/25.39 % (1683723)Instructions burned: 954 (million) % 177.63/25.39 % (1683729)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=424253563:i=1778:ins=1:rtra=on_2793 on theBenchmark for (2793ds/1778Mi) % 177.63/25.39 % (1683729)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.63/25.39 % (1683729)Terminated due to inappropriate strategy. % 177.63/25.39 % (1683729)------------------------------ % 177.63/25.39 % (1683729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.63/25.39 % (1683729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.63/25.39 % (1683729)CaDiCaL version: 2.1.3 % 177.63/25.39 % (1683729)Termination reason: Inappropriate % 177.63/25.39 % (1683729)Time elapsed: 0.035 s % 177.63/25.39 % (1683729)Peak memory usage: 10 MB % 177.63/25.39 % (1683729)Instructions burned: 90 (million) % 177.63/25.39 % (1683729)------------------------------ % 177.63/25.39 % (1683729)------------------------------ % 177.63/25.39 % (1683731)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=517707901:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2793 on theBenchmark for (2793ds/1384Mi) % 177.63/25.39 % (1683727)Instruction limit reached! % 177.63/25.39 % (1683727)------------------------------ % 177.63/25.39 % (1683727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.63/25.39 % (1683727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.63/25.39 % (1683727)CaDiCaL version: 2.1.3 % 177.63/25.39 % (1683727)Termination reason: Instruction limit % 177.63/25.39 % (1683727)Termination phase: Saturation % 177.63/25.39 % (1683727)Time elapsed: 0.471 s % 177.63/25.39 % (1683727)Peak memory usage: 13 MB % 177.63/25.39 % (1683727)Instructions burned: 2359 (million) % 177.63/25.39 % (1683733)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3512392804:i=1758:kws=inv_precedence:fsr=off:rtra=on_2792 on theBenchmark for (2792ds/1758Mi) % 177.63/25.39 % (1683733)Instruction limit reached! % 177.63/25.39 % (1683733)------------------------------ % 177.63/25.39 % (1683733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.63/25.39 % (1683733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.63/25.39 % (1683733)CaDiCaL version: 2.1.3 % 177.63/25.39 % (1683733)Termination reason: Instruction limit % 177.63/25.39 % (1683733)Termination phase: Saturation % 177.63/25.39 % (1683733)Time elapsed: 0.355 s % 177.63/25.39 % (1683733)Peak memory usage: 15 MB % 177.63/25.39 % (1683733)Instructions burned: 1759 (million) % 177.63/25.39 % (1683735)fmb+10_1_sil=64000:si=on:random_seed=179025494:i=44122:nm=2:rtra=on:gsp=on_2788 on theBenchmark for (2788ds/44122Mi) % 177.63/25.39 % (1683735)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.63/25.39 % (1683735)Terminated due to inappropriate strategy. % 177.63/25.39 % (1683735)------------------------------ % 177.63/25.39 % (1683735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.63/25.39 % (1683735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.63/25.39 % (1683735)CaDiCaL version: 2.1.3 % 177.63/25.39 % (1683735)Termination reason: Inappropriate % 177.63/25.39 % (1683735)Time elapsed: 0.024 s % 177.63/25.39 % (1683735)Peak memory usage: 10 MB % 177.63/25.39 % (1683735)Instructions burned: 118 (million) % 177.63/25.39 % (1683735)------------------------------ % 177.63/25.39 % (1683735)------------------------------ % 177.63/25.39 % (1683737)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=202347458:i=19030:nm=5:rtra=on_2788 on theBenchmark for (2788ds/19030Mi) % 198.21/28.29 % (1683737)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 198.21/28.29 % (1683737)Terminated due to inappropriate strategy. % 198.21/28.29 % (1683737)------------------------------ % 198.21/28.29 % (1683737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.21/28.29 % (1683737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.21/28.29 % (1683737)CaDiCaL version: 2.1.3 % 198.21/28.29 % (1683737)Termination reason: Inappropriate % 198.21/28.29 % (1683737)Time elapsed: 0.024 s % 198.21/28.29 % (1683737)Peak memory usage: 10 MB % 198.21/28.29 % (1683737)Instructions burned: 118 (million) % 198.21/28.29 % (1683737)------------------------------ % 198.21/28.29 % (1683737)------------------------------ % 198.21/28.29 % (1683739)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2071128073:fmbsr=1.7:i=1840:rtra=on_2788 on theBenchmark for (2788ds/1840Mi) % 198.21/28.29 % (1683731)Instruction limit reached! % 198.21/28.29 % (1683731)------------------------------ % 198.21/28.29 % (1683731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.21/28.29 % (1683731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.21/28.29 % (1683731)CaDiCaL version: 2.1.3 % 198.21/28.29 % (1683731)Termination reason: Instruction limit % 198.21/28.29 % (1683731)Termination phase: Saturation % 198.21/28.29 % (1683731)Time elapsed: 0.521 s % 198.21/28.29 % (1683731)Peak memory usage: 14 MB % 198.21/28.29 % (1683731)Instructions burned: 1385 (million) % 198.21/28.29 % (1683739)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 198.21/28.29 % (1683739)Terminated due to inappropriate strategy. % 198.21/28.29 % (1683739)------------------------------ % 198.21/28.29 % (1683739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.21/28.29 % (1683739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.21/28.29 % (1683739)CaDiCaL version: 2.1.3 % 198.21/28.29 % (1683739)Termination reason: Inappropriate % 198.21/28.29 % (1683739)Time elapsed: 0.024 s % 198.21/28.29 % (1683739)Peak memory usage: 10 MB % 198.21/28.29 % (1683739)Instructions burned: 118 (million) % 198.21/28.29 % (1683741)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3647939489:i=10262:rtra=on_2787 on theBenchmark for (2787ds/10262Mi) % 198.21/28.29 % (1683739)------------------------------ % 198.21/28.29 % (1683739)------------------------------ % 198.21/28.29 % (1683743)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2979581239:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2787 on theBenchmark for (2787ds/2944Mi) % 198.21/28.29 % (1683743)Instruction limit reached! % 198.21/28.29 % (1683743)------------------------------ % 198.21/28.29 % (1683743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.21/28.29 % (1683743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.21/28.29 % (1683743)CaDiCaL version: 2.1.3 % 198.21/28.29 % (1683743)Termination reason: Instruction limit % 198.21/28.29 % (1683743)Termination phase: Saturation % 198.21/28.29 % (1683743)Time elapsed: 0.588 s % 198.21/28.29 % (1683743)Peak memory usage: 15 MB % 198.21/28.29 % (1683743)Instructions burned: 2948 (million) % 198.21/28.29 % (1683745)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3409650628:i=12648:rtra=on_2781 on theBenchmark for (2781ds/12648Mi) % 198.21/28.29 % (1683745)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 198.21/28.29 % (1683745)Terminated due to inappropriate strategy. % 198.21/28.29 % (1683745)------------------------------ % 198.21/28.29 % (1683745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.21/28.29 % (1683745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.21/28.29 % (1683745)CaDiCaL version: 2.1.3 % 198.21/28.29 % (1683745)Termination reason: Inappropriate % 198.21/28.29 % (1683745)Time elapsed: 0.024 s % 198.21/28.29 % (1683745)Peak memory usage: 10 MB % 198.21/28.29 % (1683745)Instructions burned: 118 (million) % 198.21/28.29 % (1683745)------------------------------ % 198.21/28.29 % (1683745)------------------------------ % 198.21/28.29 % (1683747)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=4155899677:fmbsr=2.30978:i=4348:rtra=on_2781 on theBenchmark for (2781ds/4348Mi) % 198.21/28.29 % (1683747)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 198.21/28.29 % (1683747)Terminated due to inappropriate strategy. % 198.21/28.29 % (1683747)------------------------------ % 272.03/38.62 % (1683747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.03/38.62 % (1683747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.03/38.62 % (1683747)CaDiCaL version: 2.1.3 % 272.03/38.62 % (1683747)Termination reason: Inappropriate % 272.03/38.62 % (1683747)Time elapsed: 0.024 s % 272.03/38.62 % (1683747)Peak memory usage: 10 MB % 272.03/38.62 % (1683747)Instructions burned: 118 (million) % 272.03/38.62 % (1683747)------------------------------ % 272.03/38.62 % (1683747)------------------------------ % 272.03/38.62 % (1683749)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1416049353:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2781 on theBenchmark for (2781ds/1738Mi) % 272.03/38.62 % (1683749)Instruction limit reached! % 272.03/38.62 % (1683749)------------------------------ % 272.03/38.62 % (1683749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.03/38.62 % (1683749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.03/38.62 % (1683749)CaDiCaL version: 2.1.3 % 272.03/38.62 % (1683749)Termination reason: Instruction limit % 272.03/38.62 % (1683749)Termination phase: Saturation % 272.03/38.62 % (1683749)Time elapsed: 0.348 s % 272.03/38.62 % (1683749)Peak memory usage: 14 MB % 272.03/38.62 % (1683749)Instructions burned: 1741 (million) % 272.03/38.62 % (1683751)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1467098079:i=10228:av=off:rtra=on_2777 on theBenchmark for (2777ds/10228Mi) % 272.03/38.62 % (1683689)Instruction limit reached! % 272.03/38.62 % (1683689)------------------------------ % 272.03/38.62 % (1683689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.03/38.62 % (1683689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.03/38.62 % (1683689)CaDiCaL version: 2.1.3 % 272.03/38.62 % (1683689)Termination reason: Instruction limit % 272.03/38.62 % (1683689)Termination phase: Saturation % 272.03/38.62 % (1683689)Time elapsed: 10.431 s % 272.03/38.62 % (1683689)Peak memory usage: 16 MB % 272.03/38.62 % (1683689)Instructions burned: 28123 (million) % 272.03/38.62 % (1683753)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=905176459:i=108564:rtra=on_2763 on theBenchmark for (2763ds/108564Mi) % 272.03/38.62 % (1683753)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.03/38.62 % (1683753)Terminated due to inappropriate strategy. % 272.03/38.62 % (1683753)------------------------------ % 272.03/38.62 % (1683753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.03/38.62 % (1683753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.03/38.62 % (1683753)CaDiCaL version: 2.1.3 % 272.03/38.62 % (1683753)Termination reason: Inappropriate % 272.03/38.62 % (1683753)Time elapsed: 0.045 s % 272.03/38.62 % (1683753)Peak memory usage: 10 MB % 272.03/38.62 % (1683753)Instructions burned: 118 (million) % 272.03/38.62 % (1683753)------------------------------ % 272.03/38.62 % (1683753)------------------------------ % 272.03/38.62 % (1683755)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=540495031:i=7024:aac=none:rtra=on_2762 on theBenchmark for (2762ds/7024Mi) % 272.03/38.62 % (1683751)Instruction limit reached! % 272.03/38.62 % (1683751)------------------------------ % 272.03/38.62 % (1683751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.03/38.62 % (1683751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.03/38.62 % (1683751)CaDiCaL version: 2.1.3 % 272.03/38.62 % (1683751)Termination reason: Instruction limit % 272.03/38.62 % (1683751)Termination phase: Saturation % 272.03/38.62 % (1683751)Time elapsed: 2.045 s % 272.03/38.62 % (1683751)Peak memory usage: 18 MB % 272.03/38.62 % (1683751)Instructions burned: 10229 (million) % 272.03/38.62 % (1683757)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1444789345:i=7546:rtra=on:amm=off_2756 on theBenchmark for (2756ds/7546Mi) % 272.03/38.62 % (1683741)Instruction limit reached! % 272.03/38.62 % (1683741)------------------------------ % 272.03/38.62 % (1683741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.03/38.62 % (1683741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.03/38.62 % (1683741)CaDiCaL version: 2.1.3 % 272.03/38.62 % (1683741)Termination reason: Instruction limit % 272.03/38.62 % (1683741)Termination phase: Saturation % 272.03/38.62 % (1683741)Time elapsed: 3.912 s % 272.03/38.62 % (1683741)Peak memory usage: 18 MB % 272.03/38.62 % (1683741)Instructions burned: 10262 (million) % 272.03/38.62 % (1683759)ott+11_1_sil=16000:si=on:gs=on:random_seed=2567291741:s2a=on:i=4502:s2at=3:kws=inv_arTerminated % 300.40/42.63 % Vampire exiting %------------------------------------------------------------------------------