%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM899_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/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 12:26:01 PM UTC 2026 % Result : Timeout 300.21s 43.16s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : NUM899_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.05/0.52 % Computer : n012.cluster.edu % 0.05/0.52 % Model : x86_64 x86_64 % 0.05/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.05/0.52 % Memory : 8046.5625MB % 0.05/0.52 % OS : Linux 6.8.0-71-generic % 0.05/0.52 % CPULimit : 300 % 0.05/0.52 % WCLimit : 300 % 0.05/0.52 % DateTime : Sun Sep 27 21:38:37 UTC 2026 % 0.05/0.52 % CPUTime : % 0.05/0.52 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.54 Running first-order model finding % 0.09/0.54 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.09/0.89 % (2768974)Will run a generic schedule for satisfiability detection. % 0.09/0.89 % (2768996)% WARNING: option uhcvi not known. % 0.09/0.89 % (2768997)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4026656144:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 0.09/0.89 % (2768995)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1962888160_2999 on theBenchmark for (2999ds/0Mi) % 0.09/0.89 % (2769000)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=982379179:i=131_2999 on theBenchmark for (2999ds/131Mi) % 0.09/0.89 % (2769001)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3706993922:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 0.09/0.89 % (2768996)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3668271193:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 0.09/0.89 % (2768998)dis+10_1_sil=32000:sp=arity:random_seed=3734732734:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 0.09/0.89 % (2768995)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 0.09/0.89 % (2768995)Terminated due to inappropriate strategy. % 0.09/0.89 % (2768995)------------------------------ % 0.09/0.89 % (2768995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.09/0.89 % (2768995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.09/0.89 % (2768995)CaDiCaL version: 2.1.3 % 0.09/0.89 % (2768995)Termination reason: Inappropriate % 0.09/0.89 % (2768995)Time elapsed: 0.0000 s % 0.09/0.89 % (2768995)Peak memory usage: 10 MB % 0.09/0.89 % (2768999)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4234977540:i=116_2999 on theBenchmark for (2999ds/116Mi) % 0.09/0.89 % (2768995)------------------------------ % 0.09/0.89 % (2768995)------------------------------ % 0.09/0.89 % (2769012)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2732315654:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 0.09/0.89 % (2769012)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 0.09/0.89 % (2769012)Terminated due to inappropriate strategy. % 0.09/0.89 % (2769012)------------------------------ % 0.09/0.89 % (2769012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.09/0.89 % (2769012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.09/0.89 % (2769012)CaDiCaL version: 2.1.3 % 0.09/0.89 % (2769012)Termination reason: Inappropriate % 0.09/0.89 % (2769012)Time elapsed: 0.0000 s % 0.09/0.89 % (2769012)Peak memory usage: 10 MB % 0.09/0.89 % (2769012)------------------------------ % 0.09/0.89 % (2769012)------------------------------ % 0.09/0.89 % (2769017)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1852648062:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 0.09/0.89 % (2768998)Instruction limit reached! % 0.09/0.89 % (2768998)------------------------------ % 0.09/0.89 % (2768998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.09/0.89 % (2768998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.09/0.89 % (2768998)CaDiCaL version: 2.1.3 % 0.09/0.89 % (2768998)Termination reason: Instruction limit % 0.09/0.89 % (2768998)Termination phase: Saturation % 0.09/0.89 % (2768998)Time elapsed: 0.036 s % 0.09/0.89 % (2768998)Peak memory usage: 12 MB % 0.09/0.89 % (2768998)Instructions burned: 103 (million) % 0.09/0.89 % (2768999)Instruction limit reached! % 0.09/0.89 % (2768999)------------------------------ % 0.09/0.89 % (2768999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.09/0.89 % (2768999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.09/0.89 % (2768999)CaDiCaL version: 2.1.3 % 0.09/0.89 % (2768999)Termination reason: Instruction limit % 0.09/0.89 % (2768999)Termination phase: Saturation % 0.09/0.89 % (2768999)Time elapsed: 0.039 s % 0.09/0.89 % (2768999)Peak memory usage: 12 MB % 0.09/0.89 % (2768999)Instructions burned: 118 (million) % 0.09/0.89 % (2769000)Instruction limit reached! % 0.09/0.89 % (2769000)------------------------------ % 0.09/0.89 % (2769000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.09/0.89 % (2769000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.09/0.89 % (2769000)CaDiCaL version: 2.1.3 % 0.09/0.89 % (2769000)Termination reason: Instruction limit % 0.09/0.89 % (2769000)Termination phase: Saturation % 0.09/0.89 % (2769000)Time elapsed: 0.043 s % 3.82/1.19 % (2769000)Peak memory usage: 12 MB % 3.82/1.19 % (2769000)Instructions burned: 132 (million) % 3.82/1.19 % (2769020)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=1857992073:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.82/1.19 % (2769021)ott-21_1_sil=16000:fs=off:random_seed=3460760513:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.82/1.19 % (2769022)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3109687222:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 3.82/1.19 % (2769001)Instruction limit reached! % 3.82/1.19 % (2769001)------------------------------ % 3.82/1.19 % (2769001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.82/1.19 % (2769001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/1.19 % (2769001)CaDiCaL version: 2.1.3 % 3.82/1.19 % (2769001)Termination reason: Instruction limit % 3.82/1.19 % (2769001)Termination phase: Saturation % 3.82/1.19 % (2769001)Time elapsed: 0.064 s % 3.82/1.19 % (2769001)Peak memory usage: 13 MB % 3.82/1.19 % (2769001)Instructions burned: 159 (million) % 3.82/1.19 % (2769017)Instruction limit reached! % 3.82/1.19 % (2769017)------------------------------ % 3.82/1.19 % (2769017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.82/1.19 % (2769017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/1.19 % (2769017)CaDiCaL version: 2.1.3 % 3.82/1.19 % (2769017)Termination reason: Instruction limit % 3.82/1.19 % (2769017)Termination phase: Saturation % 3.82/1.19 % (2769017)Time elapsed: 0.050 s % 3.82/1.19 % (2769017)Peak memory usage: 12 MB % 3.82/1.19 % (2769017)Instructions burned: 133 (million) % 3.82/1.19 % (2769026)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1008790915:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi) % 3.82/1.19 % (2769026)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.82/1.19 % (2769026)Terminated due to inappropriate strategy. % 3.82/1.19 % (2769026)------------------------------ % 3.82/1.19 % (2769026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.82/1.19 % (2769026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/1.19 % (2769026)CaDiCaL version: 2.1.3 % 3.82/1.19 % (2769026)Termination reason: Inappropriate % 3.82/1.19 % (2769026)Time elapsed: 0.0000 s % 3.82/1.19 % (2769026)Peak memory usage: 10 MB % 3.82/1.19 % (2769026)------------------------------ % 3.82/1.19 % (2769026)------------------------------ % 3.82/1.19 % (2769028)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=807914733:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 3.82/1.19 % (2769029)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1134457335:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 3.82/1.19 % (2769029)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.82/1.19 % (2769029)Terminated due to inappropriate strategy. % 3.82/1.19 % (2769029)------------------------------ % 3.82/1.19 % (2769029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.82/1.19 % (2769029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/1.19 % (2769029)CaDiCaL version: 2.1.3 % 3.82/1.19 % (2769029)Termination reason: Inappropriate % 3.82/1.19 % (2769029)Time elapsed: 0.0000 s % 3.82/1.19 % (2769029)Peak memory usage: 10 MB % 3.82/1.19 % (2769029)------------------------------ % 3.82/1.19 % (2769029)------------------------------ % 3.82/1.19 % (2769021)Instruction limit reached! % 3.82/1.19 % (2769021)------------------------------ % 3.82/1.19 % (2769021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.82/1.19 % (2769021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/1.19 % (2769021)CaDiCaL version: 2.1.3 % 3.82/1.19 % (2769021)Termination reason: Instruction limit % 3.82/1.19 % (2769021)Termination phase: Saturation % 3.82/1.19 % (2769021)Time elapsed: 0.044 s % 3.82/1.19 % (2769021)Peak memory usage: 12 MB % 3.82/1.19 % (2769021)Instructions burned: 180 (million) % 3.82/1.19 % (2769032)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=3002541929: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.82/1.19 % (2769033)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=923079689:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 12.02/2.33 % (2769022)Instruction limit reached! % 12.02/2.33 % (2769022)------------------------------ % 12.02/2.33 % (2769022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.02/2.33 % (2769022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.02/2.33 % (2769022)CaDiCaL version: 2.1.3 % 12.02/2.33 % (2769022)Termination reason: Instruction limit % 12.02/2.33 % (2769022)Termination phase: Saturation % 12.02/2.33 % (2769022)Time elapsed: 0.164 s % 12.02/2.33 % (2769022)Peak memory usage: 15 MB % 12.02/2.33 % (2769022)Instructions burned: 478 (million) % 12.02/2.33 % (2769036)fmb+10_1_sil=64000:random_seed=2741144022:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 12.02/2.33 % (2769036)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 12.02/2.33 % (2769036)Terminated due to inappropriate strategy. % 12.02/2.33 % (2769036)------------------------------ % 12.02/2.33 % (2769036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.02/2.33 % (2769036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.02/2.33 % (2769036)CaDiCaL version: 2.1.3 % 12.02/2.33 % (2769036)Termination reason: Inappropriate % 12.02/2.33 % (2769036)Time elapsed: 0.0000 s % 12.02/2.33 % (2769036)Peak memory usage: 10 MB % 12.02/2.33 % (2769036)------------------------------ % 12.02/2.33 % (2769036)------------------------------ % 12.02/2.33 % (2769038)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1525184817:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 12.02/2.33 % (2769038)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 12.02/2.33 % (2769038)Terminated due to inappropriate strategy. % 12.02/2.33 % (2769038)------------------------------ % 12.02/2.33 % (2769038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.02/2.33 % (2769038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.02/2.33 % (2769038)CaDiCaL version: 2.1.3 % 12.02/2.33 % (2769038)Termination reason: Inappropriate % 12.02/2.33 % (2769038)Time elapsed: 0.0000 s % 12.02/2.33 % (2769038)Peak memory usage: 10 MB % 12.02/2.33 % (2769038)------------------------------ % 12.02/2.33 % (2769038)------------------------------ % 12.02/2.33 % (2769040)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3115347039:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 12.02/2.33 % (2769040)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 12.02/2.33 % (2769040)Terminated due to inappropriate strategy. % 12.02/2.33 % (2769040)------------------------------ % 12.02/2.33 % (2769040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.02/2.33 % (2769040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.02/2.33 % (2769040)CaDiCaL version: 2.1.3 % 12.02/2.33 % (2769040)Termination reason: Inappropriate % 12.02/2.33 % (2769040)Time elapsed: 0.0000 s % 12.02/2.33 % (2769040)Peak memory usage: 10 MB % 12.02/2.33 % (2769040)------------------------------ % 12.02/2.33 % (2769040)------------------------------ % 12.02/2.33 % (2769042)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3421452504:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 12.02/2.33 % (2769020)Instruction limit reached! % 12.02/2.33 % (2769020)------------------------------ % 12.02/2.33 % (2769020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.02/2.33 % (2769020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.02/2.33 % (2769020)CaDiCaL version: 2.1.3 % 12.02/2.33 % (2769020)Termination reason: Instruction limit % 12.02/2.33 % (2769020)Termination phase: Saturation % 12.02/2.33 % (2769020)Time elapsed: 0.231 s % 12.02/2.33 % (2769020)Peak memory usage: 16 MB % 12.02/2.33 % (2769020)Instructions burned: 687 (million) % 12.02/2.33 % (2769044)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1989073311:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 12.02/2.33 % (2769032)Instruction limit reached! % 12.02/2.33 % (2769032)------------------------------ % 12.02/2.33 % (2769032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.02/2.33 % (2769032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.02/2.33 % (2769032)CaDiCaL version: 2.1.3 % 12.02/2.33 % (2769032)Termination reason: Instruction limit % 18.52/3.29 % (2769032)Termination phase: Saturation % 18.52/3.29 % (2769032)Time elapsed: 0.211 s % 18.52/3.29 % (2769032)Peak memory usage: 16 MB % 18.52/3.29 % (2769032)Instructions burned: 693 (million) % 18.52/3.29 % (2769046)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3498603732:i=6324_2996 on theBenchmark for (2996ds/6324Mi) % 18.52/3.29 % (2769046)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.52/3.29 % (2769046)Terminated due to inappropriate strategy. % 18.52/3.29 % (2769046)------------------------------ % 18.52/3.29 % (2769046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.52/3.29 % (2769046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.52/3.29 % (2769046)CaDiCaL version: 2.1.3 % 18.52/3.29 % (2769046)Termination reason: Inappropriate % 18.52/3.29 % (2769046)Time elapsed: 0.0000 s % 18.52/3.29 % (2769046)Peak memory usage: 10 MB % 18.52/3.29 % (2769046)------------------------------ % 18.52/3.29 % (2769046)------------------------------ % 18.52/3.29 % (2769048)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3586630557:fmbsr=2.30978:i=2174_2996 on theBenchmark for (2996ds/2174Mi) % 18.52/3.29 % (2769048)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.52/3.29 % (2769048)Terminated due to inappropriate strategy. % 18.52/3.29 % (2769048)------------------------------ % 18.52/3.29 % (2769048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.52/3.29 % (2769048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.52/3.29 % (2769048)CaDiCaL version: 2.1.3 % 18.52/3.29 % (2769048)Termination reason: Inappropriate % 18.52/3.29 % (2769048)Time elapsed: 0.0000 s % 18.52/3.29 % (2769048)Peak memory usage: 10 MB % 18.52/3.29 % (2769048)------------------------------ % 18.52/3.29 % (2769048)------------------------------ % 18.52/3.29 % (2769050)ott-2_1_sil=16000:newcnf=on:random_seed=783841853:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2996 on theBenchmark for (2996ds/869Mi) % 18.52/3.29 % (2769033)Instruction limit reached! % 18.52/3.29 % (2769033)------------------------------ % 18.52/3.29 % (2769033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.52/3.29 % (2769033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.52/3.29 % (2769033)CaDiCaL version: 2.1.3 % 18.52/3.29 % (2769033)Termination reason: Instruction limit % 18.52/3.29 % (2769033)Termination phase: Saturation % 18.52/3.29 % (2769033)Time elapsed: 0.275 s % 18.52/3.29 % (2769033)Peak memory usage: 18 MB % 18.52/3.29 % (2769033)Instructions burned: 880 (million) % 18.52/3.29 % (2769052)ott+10_1_sil=32000:tgt=ground:random_seed=468224477:i=5114:av=off_2995 on theBenchmark for (2995ds/5114Mi) % 18.52/3.29 % (2769028)Instruction limit reached! % 18.52/3.29 % (2769028)------------------------------ % 18.52/3.29 % (2769028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.52/3.29 % (2769028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.52/3.29 % (2769028)CaDiCaL version: 2.1.3 % 18.52/3.29 % (2769028)Termination reason: Instruction limit % 18.52/3.29 % (2769028)Termination phase: Saturation % 18.52/3.29 % (2769028)Time elapsed: 0.402 s % 18.52/3.29 % (2769028)Peak memory usage: 17 MB % 18.52/3.29 % (2769028)Instructions burned: 1181 (million) % 18.52/3.29 % (2769054)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1788791611:i=54282_2994 on theBenchmark for (2994ds/54282Mi) % 18.52/3.29 % (2769054)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.52/3.29 % (2769054)Terminated due to inappropriate strategy. % 18.52/3.29 % (2769054)------------------------------ % 18.52/3.29 % (2769054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.52/3.29 % (2769054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.52/3.29 % (2769054)CaDiCaL version: 2.1.3 % 18.52/3.29 % (2769054)Termination reason: Inappropriate % 18.52/3.29 % (2769054)Time elapsed: 0.0000 s % 18.52/3.29 % (2769054)Peak memory usage: 10 MB % 18.52/3.29 % (2769054)------------------------------ % 18.52/3.29 % (2769054)------------------------------ % 18.52/3.29 % (2769056)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=199967936:i=3512:aac=none_2994 on theBenchmark for (2994ds/3512Mi) % 18.52/3.29 % (2769050)Instruction limit reached! % 18.52/3.29 % (2769050)------------------------------ % 18.52/3.29 % (2769050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.52/3.29 % (2769050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.84/9.84 % (2769050)CaDiCaL version: 2.1.3 % 64.84/9.84 % (2769050)Termination reason: Instruction limit % 64.84/9.84 % (2769050)Termination phase: Saturation % 64.84/9.84 % (2769050)Time elapsed: 0.267 s % 64.84/9.84 % (2769050)Peak memory usage: 16 MB % 64.84/9.84 % (2769050)Instructions burned: 869 (million) % 64.84/9.84 % (2769058)dis+21_1_sil=32000:sas=cadical:random_seed=775060646:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi) % 64.84/9.84 % (2769044)Instruction limit reached! % 64.84/9.84 % (2769044)------------------------------ % 64.84/9.84 % (2769044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.84/9.84 % (2769044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.84/9.84 % (2769044)CaDiCaL version: 2.1.3 % 64.84/9.84 % (2769044)Termination reason: Instruction limit % 64.84/9.84 % (2769044)Termination phase: Saturation % 64.84/9.84 % (2769044)Time elapsed: 0.395 s % 64.84/9.84 % (2769044)Peak memory usage: 26 MB % 64.84/9.84 % (2769044)Instructions burned: 1474 (million) % 64.84/9.84 % (2769060)ott+11_1_sil=16000:gs=on:random_seed=1107566248:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2992 on theBenchmark for (2992ds/2251Mi) % 64.84/9.84 % (2769060)Instruction limit reached! % 64.84/9.84 % (2769060)------------------------------ % 64.84/9.84 % (2769060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.84/9.84 % (2769060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.84/9.84 % (2769060)CaDiCaL version: 2.1.3 % 64.84/9.84 % (2769060)Termination reason: Instruction limit % 64.84/9.84 % (2769060)Termination phase: Saturation % 64.84/9.84 % (2769060)Time elapsed: 0.676 s % 64.84/9.84 % (2769060)Peak memory usage: 22 MB % 64.84/9.84 % (2769060)Instructions burned: 2254 (million) % 64.84/9.84 % (2769062)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=988287449:fmbsr=1.6:i=67534_2985 on theBenchmark for (2985ds/67534Mi) % 64.84/9.84 % (2769062)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 64.84/9.84 % (2769062)Terminated due to inappropriate strategy. % 64.84/9.84 % (2769062)------------------------------ % 64.84/9.84 % (2769062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.84/9.84 % (2769062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.84/9.84 % (2769062)CaDiCaL version: 2.1.3 % 64.84/9.84 % (2769062)Termination reason: Inappropriate % 64.84/9.84 % (2769062)Time elapsed: 0.0000 s % 64.84/9.84 % (2769062)Peak memory usage: 10 MB % 64.84/9.84 % (2769062)------------------------------ % 64.84/9.84 % (2769062)------------------------------ % 64.84/9.84 % (2769064)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=742455464:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2985 on theBenchmark for (2985ds/4591Mi) % 64.84/9.84 % (2769056)Instruction limit reached! % 64.84/9.84 % (2769056)------------------------------ % 64.84/9.84 % (2769056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.84/9.84 % (2769056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.84/9.84 % (2769056)CaDiCaL version: 2.1.3 % 64.84/9.84 % (2769056)Termination reason: Instruction limit % 64.84/9.84 % (2769056)Termination phase: Saturation % 64.84/9.84 % (2769056)Time elapsed: 1.012 s % 64.84/9.84 % (2769056)Peak memory usage: 33 MB % 64.84/9.84 % (2769056)Instructions burned: 3514 (million) % 64.84/9.84 % (2769066)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2630987109:i=29340_2984 on theBenchmark for (2984ds/29340Mi) % 64.84/9.84 % (2769058)Instruction limit reached! % 64.84/9.84 % (2769058)------------------------------ % 64.84/9.84 % (2769058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.84/9.84 % (2769058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.84/9.84 % (2769058)CaDiCaL version: 2.1.3 % 64.84/9.84 % (2769058)Termination reason: Instruction limit % 64.84/9.84 % (2769058)Termination phase: Saturation % 64.84/9.84 % (2769058)Time elapsed: 1.125 s % 64.84/9.84 % (2769058)Peak memory usage: 33 MB % 64.84/9.84 % (2769058)Instructions burned: 3775 (million) % 64.84/9.84 % (2769042)Instruction limit reached! % 64.84/9.84 % (2769042)------------------------------ % 64.84/9.84 % (2769042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.84/9.84 % (2769042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.84/9.84 % (2769042)CaDiCaL version: 2.1.3 % 73.70/11.09 % (2769042)Termination reason: Instruction limit % 73.70/11.09 % (2769042)Termination phase: Saturation % 73.70/11.09 % (2769042)Time elapsed: 1.486 s % 73.70/11.09 % (2769042)Peak memory usage: 46 MB % 73.70/11.09 % (2769042)Instructions burned: 5134 (million) % 73.70/11.09 % (2769068)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3026762715:i=5211_2982 on theBenchmark for (2982ds/5211Mi) % 73.70/11.09 % (2769069)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2162521343:i=5497:nm=2_2982 on theBenchmark for (2982ds/5497Mi) % 73.70/11.09 % (2769069)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 73.70/11.09 % (2769069)Terminated due to inappropriate strategy. % 73.70/11.09 % (2769069)------------------------------ % 73.70/11.09 % (2769069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.70/11.09 % (2769069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.70/11.09 % (2769069)CaDiCaL version: 2.1.3 % 73.70/11.09 % (2769069)Termination reason: Inappropriate % 73.70/11.09 % (2769069)Time elapsed: 0.0000 s % 73.70/11.09 % (2769069)Peak memory usage: 10 MB % 73.70/11.09 % (2769069)------------------------------ % 73.70/11.09 % (2769069)------------------------------ % 73.70/11.09 % (2769072)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3946456272:fmbsr=2:i=46332_2981 on theBenchmark for (2981ds/46332Mi) % 73.70/11.09 % (2769072)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 73.70/11.09 % (2769072)Terminated due to inappropriate strategy. % 73.70/11.09 % (2769072)------------------------------ % 73.70/11.09 % (2769072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.70/11.09 % (2769072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.70/11.09 % (2769072)CaDiCaL version: 2.1.3 % 73.70/11.09 % (2769072)Termination reason: Inappropriate % 73.70/11.09 % (2769072)Time elapsed: 0.0000 s % 73.70/11.09 % (2769072)Peak memory usage: 10 MB % 73.70/11.09 % (2769072)------------------------------ % 73.70/11.09 % (2769072)------------------------------ % 73.70/11.09 % (2769074)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=598791477:i=14071_2981 on theBenchmark for (2981ds/14071Mi) % 73.70/11.09 % (2769074)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 73.70/11.09 % (2769074)Terminated due to inappropriate strategy. % 73.70/11.09 % (2769074)------------------------------ % 73.70/11.09 % (2769074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.70/11.09 % (2769074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.70/11.09 % (2769074)CaDiCaL version: 2.1.3 % 73.70/11.09 % (2769074)Termination reason: Inappropriate % 73.70/11.09 % (2769074)Time elapsed: 0.0000 s % 73.70/11.09 % (2769074)Peak memory usage: 10 MB % 73.70/11.09 % (2769074)------------------------------ % 73.70/11.09 % (2769074)------------------------------ % 73.70/11.09 % (2769076)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2006919220:i=22565:add=on:rawr=on_2981 on theBenchmark for (2981ds/22565Mi) % 73.70/11.09 % (2769052)Instruction limit reached! % 73.70/11.09 % (2769052)------------------------------ % 73.70/11.09 % (2769052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.70/11.09 % (2769052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.70/11.09 % (2769052)CaDiCaL version: 2.1.3 % 73.70/11.09 % (2769052)Termination reason: Instruction limit % 73.70/11.09 % (2769052)Termination phase: Saturation % 73.70/11.09 % (2769052)Time elapsed: 1.754 s % 73.70/11.09 % (2769052)Peak memory usage: 32 MB % 73.70/11.09 % (2769052)Instructions burned: 5115 (million) % 73.70/11.09 % (2769078)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1801142727:i=8173:av=off_2978 on theBenchmark for (2978ds/8173Mi) % 73.70/11.09 % (2769064)Instruction limit reached! % 73.70/11.09 % (2769064)------------------------------ % 73.70/11.09 % (2769064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.70/11.09 % (2769064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.70/11.09 % (2769064)CaDiCaL version: 2.1.3 % 73.70/11.09 % (2769064)Termination reason: Instruction limit % 73.70/11.09 % (2769064)Termination phase: Saturation % 73.70/11.09 % (2769064)Time elapsed: 1.295 s % 73.70/11.09 % (2769064)Peak memory usage: 41 MB % 73.70/11.09 % (2769064)Instructions burned: 4591 (million) % 73.70/11.09 % (2769080)dis+10_16:1_sil=16000:random_seed=3844600313:i=9155:fsr=off_2972 on theBenchmark for (2972ds/9155Mi) % 95.57/14.19 % (2769068)Instruction limit reached! % 95.57/14.19 % (2769068)------------------------------ % 95.57/14.19 % (2769068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.57/14.19 % (2769068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.57/14.19 % (2769068)CaDiCaL version: 2.1.3 % 95.57/14.19 % (2769068)Termination reason: Instruction limit % 95.57/14.19 % (2769068)Termination phase: Saturation % 95.57/14.19 % (2769068)Time elapsed: 1.476 s % 95.57/14.19 % (2769068)Peak memory usage: 56 MB % 95.57/14.19 % (2769068)Instructions burned: 5212 (million) % 95.57/14.19 % (2769082)ott-3_8_sil=64000:random_seed=1138397734:i=20139:bs=on_2967 on theBenchmark for (2967ds/20139Mi) % 95.57/14.19 % (2769078)Instruction limit reached! % 95.57/14.19 % (2769078)------------------------------ % 95.57/14.19 % (2769078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.57/14.19 % (2769078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.57/14.19 % (2769078)CaDiCaL version: 2.1.3 % 95.57/14.19 % (2769078)Termination reason: Instruction limit % 95.57/14.19 % (2769078)Termination phase: Saturation % 95.57/14.19 % (2769078)Time elapsed: 2.898 s % 95.57/14.19 % (2769078)Peak memory usage: 45 MB % 95.57/14.19 % (2769078)Instructions burned: 8173 (million) % 95.57/14.19 % (2769084)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1240006181:fmbsr=2:i=32576_2948 on theBenchmark for (2948ds/32576Mi) % 95.57/14.19 % (2769084)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 95.57/14.19 % (2769084)Terminated due to inappropriate strategy. % 95.57/14.19 % (2769084)------------------------------ % 95.57/14.19 % (2769084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.57/14.19 % (2769084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.57/14.19 % (2769084)CaDiCaL version: 2.1.3 % 95.57/14.19 % (2769084)Termination reason: Inappropriate % 95.57/14.19 % (2769084)Time elapsed: 0.0000 s % 95.57/14.19 % (2769084)Peak memory usage: 10 MB % 95.57/14.19 % (2769084)------------------------------ % 95.57/14.19 % (2769084)------------------------------ % 95.57/14.19 % (2769086)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=82325241:i=11404_2948 on theBenchmark for (2948ds/11404Mi) % 95.57/14.19 % (2769080)Instruction limit reached! % 95.57/14.19 % (2769080)------------------------------ % 95.57/14.19 % (2769080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.57/14.19 % (2769080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.57/14.19 % (2769080)CaDiCaL version: 2.1.3 % 95.57/14.19 % (2769080)Termination reason: Instruction limit % 95.57/14.19 % (2769080)Termination phase: Saturation % 95.57/14.19 % (2769080)Time elapsed: 2.631 s % 95.57/14.19 % (2769080)Peak memory usage: 56 MB % 95.57/14.19 % (2769080)Instructions burned: 9158 (million) % 95.57/14.19 % (2769088)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3054915793:i=14134_2946 on theBenchmark for (2946ds/14134Mi) % 95.57/14.19 % (2769076)Instruction limit reached! % 95.57/14.19 % (2769076)------------------------------ % 95.57/14.19 % (2769076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.57/14.19 % (2769076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.57/14.19 % (2769076)CaDiCaL version: 2.1.3 % 95.57/14.19 % (2769076)Termination reason: Instruction limit % 95.57/14.19 % (2769076)Termination phase: Saturation % 95.57/14.20 % (2769076)Time elapsed: 4.970 s % 95.57/14.20 % (2769076)Peak memory usage: 67 MB % 95.57/14.20 % (2769076)Instructions burned: 22565 (million) % 95.57/14.20 % (2769090)dis+33_16_sil=32000:sac=on:random_seed=3235696537:i=15851:nm=0_2931 on theBenchmark for (2931ds/15851Mi) % 95.57/14.20 % (2769066)Instruction limit reached! % 95.57/14.20 % (2769066)------------------------------ % 95.57/14.20 % (2769066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.57/14.20 % (2769066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.57/14.20 % (2769066)CaDiCaL version: 2.1.3 % 95.57/14.20 % (2769066)Termination reason: Instruction limit % 95.57/14.20 % (2769066)Termination phase: Saturation % 95.57/14.20 % (2769066)Time elapsed: 7.398 s % 95.57/14.20 % (2769066)Peak memory usage: 71 MB % 95.57/14.20 % (2769066)Instructions burned: 29343 (million) % 95.57/14.20 % (2769092)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2227504482:avsq=on:i=17627:add=on:amm=off_2910 on theBenchmark for (2910ds/17627Mi) % 95.57/14.20 % (2769086)Instruction limit reached! % 95.57/14.20 % (2769086)------------------------------ % 99.62/14.75 % (2769086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.62/14.75 % (2769086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.62/14.75 % (2769086)CaDiCaL version: 2.1.3 % 99.62/14.75 % (2769086)Termination reason: Instruction limit % 99.62/14.75 % (2769086)Termination phase: Saturation % 99.62/14.75 % (2769086)Time elapsed: 4.172 s % 99.62/14.75 % (2769086)Peak memory usage: 49 MB % 99.62/14.75 % (2769086)Instructions burned: 11404 (million) % 99.62/14.75 % (2769094)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2795677051:s2a=on:i=53295_2907 on theBenchmark for (2907ds/53295Mi) % 99.62/14.75 % (2769082)Instruction limit reached! % 99.62/14.75 % (2769082)------------------------------ % 99.62/14.75 % (2769082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.62/14.75 % (2769082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.62/14.75 % (2769082)CaDiCaL version: 2.1.3 % 99.62/14.75 % (2769082)Termination reason: Instruction limit % 99.62/14.75 % (2769082)Termination phase: Saturation % 99.62/14.75 % (2769082)Time elapsed: 6.560 s % 99.62/14.75 % (2769082)Peak memory usage: 66 MB % 99.62/14.75 % (2769082)Instructions burned: 20141 (million) % 99.62/14.75 % (2769096)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4208183236:i=26857:ins=20_2901 on theBenchmark for (2901ds/26857Mi) % 99.62/14.75 % (2769096)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 99.62/14.75 % (2769096)Terminated due to inappropriate strategy. % 99.62/14.75 % (2769096)------------------------------ % 99.62/14.75 % (2769096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.62/14.75 % (2769096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.62/14.75 % (2769096)CaDiCaL version: 2.1.3 % 99.62/14.75 % (2769096)Termination reason: Inappropriate % 99.62/14.75 % (2769096)Time elapsed: 0.0000 s % 99.62/14.75 % (2769096)Peak memory usage: 10 MB % 99.62/14.75 % (2769096)------------------------------ % 99.62/14.75 % (2769096)------------------------------ % 99.62/14.75 % (2769098)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2150672190:i=28120:bs=on:fsr=off_2901 on theBenchmark for (2901ds/28120Mi) % 99.62/14.75 % (2769088)Instruction limit reached! % 99.62/14.75 % (2769088)------------------------------ % 99.62/14.75 % (2769088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.62/14.75 % (2769088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.62/14.75 % (2769088)CaDiCaL version: 2.1.3 % 99.62/14.75 % (2769088)Termination reason: Instruction limit % 99.62/14.75 % (2769088)Termination phase: Saturation % 99.62/14.75 % (2769088)Time elapsed: 5.105 s % 99.62/14.75 % (2769088)Peak memory usage: 55 MB % 99.62/14.75 % (2769088)Instructions burned: 14136 (million) % 99.62/14.75 % (2769100)fmb+10_1_sil=256000:fmbss=7:random_seed=3260165598:fmbsr=1.6:i=182295_2894 on theBenchmark for (2894ds/182295Mi) % 99.62/14.75 % (2769100)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 99.62/14.75 % (2769100)Terminated due to inappropriate strategy. % 99.62/14.75 % (2769100)------------------------------ % 99.62/14.75 % (2769100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.62/14.75 % (2769100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.62/14.75 % (2769100)CaDiCaL version: 2.1.3 % 99.62/14.75 % (2769100)Termination reason: Inappropriate % 99.62/14.75 % (2769100)Time elapsed: 0.0000 s % 99.62/14.75 % (2769100)Peak memory usage: 10 MB % 99.62/14.75 % (2769100)------------------------------ % 99.62/14.75 % (2769100)------------------------------ % 99.62/14.75 % (2769102)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2031983938:i=44625:gsp=on_2894 on theBenchmark for (2894ds/44625Mi) % 99.62/14.75 % (2769102)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 99.62/14.75 % (2769102)Terminated due to inappropriate strategy. % 99.62/14.75 % (2769102)------------------------------ % 99.62/14.75 % (2769102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.62/14.75 % (2769102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.62/14.75 % (2769102)CaDiCaL version: 2.1.3 % 99.62/14.75 % (2769102)Termination reason: Inappropriate % 99.62/14.75 % (2769102)Time elapsed: 0.0000 s % 99.62/14.75 % (2769102)Peak memory usage: 10 MB % 99.62/14.75 % (2769102)------------------------------ % 99.62/14.75 % (2769102)------------------------------ % 99.62/14.75 % (2769104)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2458256555:i=160505_2894 on theBenchmark for (2894ds/160505Mi) % 112.39/16.53 % (2769104)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 112.39/16.53 % (2769104)Terminated due to inappropriate strategy. % 112.39/16.53 % (2769104)------------------------------ % 112.39/16.53 % (2769104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.39/16.53 % (2769104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.39/16.53 % (2769104)CaDiCaL version: 2.1.3 % 112.39/16.53 % (2769104)Termination reason: Inappropriate % 112.39/16.53 % (2769104)Time elapsed: 0.0000 s % 112.39/16.53 % (2769104)Peak memory usage: 10 MB % 112.39/16.53 % (2769104)------------------------------ % 112.39/16.53 % (2769104)------------------------------ % 112.39/16.53 % (2769106)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3216993664:fmbsr=1.3:i=225729_2894 on theBenchmark for (2894ds/225729Mi) % 112.39/16.53 % (2769106)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 112.39/16.53 % (2769106)Terminated due to inappropriate strategy. % 112.39/16.53 % (2769106)------------------------------ % 112.39/16.54 % (2769106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.39/16.54 % (2769106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.39/16.54 % (2769106)CaDiCaL version: 2.1.3 % 112.39/16.54 % (2769106)Termination reason: Inappropriate % 112.39/16.54 % (2769106)Time elapsed: 0.0000 s % 112.39/16.54 % (2769106)Peak memory usage: 10 MB % 112.39/16.54 % (2769106)------------------------------ % 112.39/16.54 % (2769106)------------------------------ % 112.39/16.54 % (2769108)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=790655966:fmbsr=2:i=185024:ins=7_2894 on theBenchmark for (2894ds/185024Mi) % 112.39/16.54 % (2769108)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 112.39/16.54 % (2769108)Terminated due to inappropriate strategy. % 112.39/16.54 % (2769108)------------------------------ % 112.39/16.54 % (2769108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.39/16.54 % (2769108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.39/16.54 % (2769108)CaDiCaL version: 2.1.3 % 112.39/16.54 % (2769108)Termination reason: Inappropriate % 112.39/16.54 % (2769108)Time elapsed: 0.0000 s % 112.39/16.54 % (2769108)Peak memory usage: 10 MB % 112.39/16.54 % (2769108)------------------------------ % 112.39/16.54 % (2769108)------------------------------ % 112.39/16.54 % (2769110)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3821086633:rtra=on_2894 on theBenchmark for (2894ds/0Mi) % 112.39/16.54 % (2769110)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 112.39/16.54 % (2769110)Terminated due to inappropriate strategy. % 112.39/16.54 % (2769110)------------------------------ % 112.39/16.54 % (2769110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.39/16.54 % (2769110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.39/16.54 % (2769110)CaDiCaL version: 2.1.3 % 112.39/16.54 % (2769110)Termination reason: Inappropriate % 112.39/16.54 % (2769110)Time elapsed: 0.0000 s % 112.39/16.54 % (2769110)Peak memory usage: 10 MB % 112.39/16.54 % (2769110)------------------------------ % 112.39/16.54 % (2769110)------------------------------ % 112.39/16.54 % (2769112)% WARNING: option uhcvi not known. % 112.39/16.54 % (2769112)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2413626068:i=271062:add=off:rtra=on:rawr=on_2894 on theBenchmark for (2894ds/271062Mi) % 112.39/16.54 % (2769090)Instruction limit reached! % 112.39/16.54 % (2769090)------------------------------ % 112.39/16.54 % (2769090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.39/16.54 % (2769090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.39/16.54 % (2769090)CaDiCaL version: 2.1.3 % 112.39/16.54 % (2769090)Termination reason: Instruction limit % 112.39/16.54 % (2769090)Termination phase: Saturation % 112.39/16.54 % (2769090)Time elapsed: 4.687 s % 112.39/16.54 % (2769090)Peak memory usage: 128 MB % 112.39/16.54 % (2769090)Instructions burned: 15852 (million) % 112.39/16.54 % (2769208)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2851077380:i=176048:add=on:rtra=on:rawr=on_2884 on theBenchmark for (2884ds/176048Mi) % 112.39/16.54 % (2769092)Instruction limit reached! % 112.39/16.54 % (2769092)------------------------------ % 112.39/16.54 % (2769092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.71/17.46 % (2769092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.71/17.46 % (2769092)CaDiCaL version: 2.1.3 % 118.71/17.46 % (2769092)Termination reason: Instruction limit % 118.71/17.46 % (2769092)Termination phase: Saturation % 118.71/17.46 % (2769092)Time elapsed: 4.662 s % 118.71/17.46 % (2769092)Peak memory usage: 128 MB % 118.71/17.46 % (2769092)Instructions burned: 17629 (million) % 118.71/17.46 % (2769529)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1106590444:i=206:fgj=on:rtra=on_2863 on theBenchmark for (2863ds/206Mi) % 118.71/17.46 % (2769529)Instruction limit reached! % 118.71/17.46 % (2769529)------------------------------ % 118.71/17.46 % (2769529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.71/17.46 % (2769529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.71/17.46 % (2769529)CaDiCaL version: 2.1.3 % 118.71/17.46 % (2769529)Termination reason: Instruction limit % 118.71/17.46 % (2769529)Termination phase: Saturation % 118.71/17.46 % (2769529)Time elapsed: 0.072 s % 118.71/17.46 % (2769529)Peak memory usage: 13 MB % 118.71/17.46 % (2769529)Instructions burned: 208 (million) % 118.71/17.46 % (2769531)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4284702231:i=232:rtra=on_2862 on theBenchmark for (2862ds/232Mi) % 118.71/17.46 % (2769531)Instruction limit reached! % 118.71/17.46 % (2769531)------------------------------ % 118.71/17.46 % (2769531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.71/17.46 % (2769531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.71/17.46 % (2769531)CaDiCaL version: 2.1.3 % 118.71/17.46 % (2769531)Termination reason: Instruction limit % 118.71/17.46 % (2769531)Termination phase: Saturation % 118.71/17.46 % (2769531)Time elapsed: 0.080 s % 118.71/17.46 % (2769531)Peak memory usage: 13 MB % 118.71/17.46 % (2769531)Instructions burned: 234 (million) % 118.71/17.46 % (2769533)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1472996142:i=262:rtra=on_2861 on theBenchmark for (2861ds/262Mi) % 118.71/17.46 % (2769533)Instruction limit reached! % 118.71/17.46 % (2769533)------------------------------ % 118.71/17.46 % (2769533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.71/17.46 % (2769533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.71/17.46 % (2769533)CaDiCaL version: 2.1.3 % 118.71/17.46 % (2769533)Termination reason: Instruction limit % 118.71/17.46 % (2769533)Termination phase: Saturation % 118.71/17.46 % (2769533)Time elapsed: 0.088 s % 118.71/17.46 % (2769533)Peak memory usage: 13 MB % 118.71/17.46 % (2769533)Instructions burned: 263 (million) % 118.71/17.46 % (2769535)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3544752860:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2860 on theBenchmark for (2860ds/318Mi) % 118.71/17.46 % (2769535)Instruction limit reached! % 118.71/17.46 % (2769535)------------------------------ % 118.71/17.46 % (2769535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.71/17.46 % (2769535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.71/17.46 % (2769535)CaDiCaL version: 2.1.3 % 118.71/17.46 % (2769535)Termination reason: Instruction limit % 118.71/17.46 % (2769535)Termination phase: Saturation % 118.71/17.46 % (2769535)Time elapsed: 0.126 s % 118.71/17.46 % (2769535)Peak memory usage: 15 MB % 118.71/17.46 % (2769535)Instructions burned: 318 (million) % 118.71/17.46 % (2769537)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3740721675:i=1428:nm=2:rtra=on_2859 on theBenchmark for (2859ds/1428Mi) % 118.71/17.46 % (2769537)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 118.71/17.46 % (2769537)Terminated due to inappropriate strategy. % 118.71/17.46 % (2769537)------------------------------ % 118.71/17.46 % (2769537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.71/17.46 % (2769537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.71/17.46 % (2769537)CaDiCaL version: 2.1.3 % 118.71/17.46 % (2769537)Termination reason: Inappropriate % 118.71/17.46 % (2769537)Time elapsed: 0.0000 s % 118.71/17.46 % (2769537)Peak memory usage: 10 MB % 118.71/17.46 % (2769537)------------------------------ % 118.71/17.46 % (2769537)------------------------------ % 118.71/17.46 % (2769539)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=298925810:i=262:bd=preordered:rtra=on:fsd=on_2859 on theBenchmark for (2859ds/262Mi) % 118.71/17.46 % (2769539)Instruction limit reached! % 118.71/17.46 % (2769539)------------------------------ % 118.71/17.46 % (2769539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.00/20.78 % (2769539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.00/20.78 % (2769539)CaDiCaL version: 2.1.3 % 142.00/20.78 % (2769539)Termination reason: Instruction limit % 142.00/20.78 % (2769539)Termination phase: Saturation % 142.00/20.78 % (2769539)Time elapsed: 0.095 s % 142.00/20.78 % (2769539)Peak memory usage: 13 MB % 142.00/20.78 % (2769539)Instructions burned: 262 (million) % 142.00/20.78 % (2769541)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=990121079:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2857 on theBenchmark for (2857ds/1368Mi) % 142.00/20.78 % (2769541)Instruction limit reached! % 142.00/20.78 % (2769541)------------------------------ % 142.00/20.78 % (2769541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.00/20.78 % (2769541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.00/20.78 % (2769541)CaDiCaL version: 2.1.3 % 142.00/20.78 % (2769541)Termination reason: Instruction limit % 142.00/20.78 % (2769541)Termination phase: Saturation % 142.00/20.78 % (2769541)Time elapsed: 0.430 s % 142.00/20.78 % (2769541)Peak memory usage: 23 MB % 142.00/20.78 % (2769541)Instructions burned: 1369 (million) % 142.00/20.78 % (2769543)ott-21_1_sil=16000:si=on:fs=off:random_seed=44439178:i=360:av=off:fsr=off:rtra=on_2853 on theBenchmark for (2853ds/360Mi) % 142.00/20.78 % (2769543)Instruction limit reached! % 142.00/20.78 % (2769543)------------------------------ % 142.00/20.78 % (2769543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.00/20.78 % (2769543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.00/20.78 % (2769543)CaDiCaL version: 2.1.3 % 142.00/20.78 % (2769543)Termination reason: Instruction limit % 142.00/20.78 % (2769543)Termination phase: Saturation % 142.00/20.78 % (2769543)Time elapsed: 0.088 s % 142.00/20.78 % (2769543)Peak memory usage: 12 MB % 142.00/20.78 % (2769543)Instructions burned: 362 (million) % 142.00/20.78 % (2769545)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4261678148:i=954:bd=all:rtra=on_2852 on theBenchmark for (2852ds/954Mi) % 142.00/20.78 % (2769545)Instruction limit reached! % 142.00/20.78 % (2769545)------------------------------ % 142.00/20.78 % (2769545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.00/20.78 % (2769545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.00/20.78 % (2769545)CaDiCaL version: 2.1.3 % 142.00/20.78 % (2769545)Termination reason: Instruction limit % 142.00/20.78 % (2769545)Termination phase: Saturation % 142.00/20.78 % (2769545)Time elapsed: 0.350 s % 142.00/20.78 % (2769545)Peak memory usage: 17 MB % 142.00/20.78 % (2769545)Instructions burned: 955 (million) % 142.00/20.78 % (2769547)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3485806580:fmbsr=1.3:i=1730:ins=25:rtra=on_2848 on theBenchmark for (2848ds/1730Mi) % 142.00/20.78 % (2769547)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 142.00/20.78 % (2769547)Terminated due to inappropriate strategy. % 142.00/20.78 % (2769547)------------------------------ % 142.00/20.78 % (2769547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.00/20.78 % (2769547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.00/20.78 % (2769547)CaDiCaL version: 2.1.3 % 142.00/20.78 % (2769547)Termination reason: Inappropriate % 142.00/20.78 % (2769547)Time elapsed: 0.0000 s % 142.00/20.78 % (2769547)Peak memory usage: 10 MB % 142.00/20.78 % (2769547)------------------------------ % 142.00/20.78 % (2769547)------------------------------ % 142.00/20.78 % (2769549)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1449467537:i=2358:rtra=on_2848 on theBenchmark for (2848ds/2358Mi) % 142.00/20.78 % (2769549)Instruction limit reached! % 142.00/20.78 % (2769549)------------------------------ % 142.00/20.78 % (2769549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.00/20.78 % (2769549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.00/20.78 % (2769549)CaDiCaL version: 2.1.3 % 142.00/20.78 % (2769549)Termination reason: Instruction limit % 142.00/20.78 % (2769549)Termination phase: Saturation % 142.00/20.78 % (2769549)Time elapsed: 0.835 s % 142.00/20.78 % (2769549)Peak memory usage: 21 MB % 142.00/20.78 % (2769549)Instructions burned: 2360 (million) % 142.00/20.78 % (2769551)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3991714395:i=1778:ins=1:rtra=on_2840 on theBenchmark for (2840ds/1778Mi) % 142.00/20.78 % (2769551)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.98/23.17 % (2769551)Terminated due to inappropriate strategy. % 158.98/23.17 % (2769551)------------------------------ % 158.98/23.17 % (2769551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.98/23.17 % (2769551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.98/23.17 % (2769551)CaDiCaL version: 2.1.3 % 158.98/23.17 % (2769551)Termination reason: Inappropriate % 158.98/23.17 % (2769551)Time elapsed: 0.0000 s % 158.98/23.17 % (2769551)Peak memory usage: 10 MB % 158.98/23.17 % (2769551)------------------------------ % 158.98/23.17 % (2769551)------------------------------ % 158.98/23.17 % (2769553)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=1323335578:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2840 on theBenchmark for (2840ds/1384Mi) % 158.98/23.17 % (2769553)Instruction limit reached! % 158.98/23.17 % (2769553)------------------------------ % 158.98/23.17 % (2769553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.98/23.17 % (2769553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.98/23.17 % (2769553)CaDiCaL version: 2.1.3 % 158.98/23.17 % (2769553)Termination reason: Instruction limit % 158.98/23.17 % (2769553)Termination phase: Saturation % 158.98/23.17 % (2769553)Time elapsed: 0.433 s % 158.98/23.17 % (2769553)Peak memory usage: 20 MB % 158.98/23.17 % (2769553)Instructions burned: 1385 (million) % 158.98/23.17 % (2769555)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=4282261865:i=1758:kws=inv_precedence:fsr=off:rtra=on_2835 on theBenchmark for (2835ds/1758Mi) % 158.98/23.17 % (2769098)Instruction limit reached! % 158.98/23.17 % (2769098)------------------------------ % 158.98/23.17 % (2769098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.98/23.17 % (2769098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.98/23.17 % (2769098)CaDiCaL version: 2.1.3 % 158.98/23.17 % (2769098)Termination reason: Instruction limit % 158.98/23.17 % (2769098)Termination phase: Saturation % 158.98/23.17 % (2769098)Time elapsed: 7.0000 s % 158.98/23.17 % (2769098)Peak memory usage: 31 MB % 158.98/23.17 % (2769098)Instructions burned: 28121 (million) % 158.98/23.17 % (2769557)fmb+10_1_sil=64000:si=on:random_seed=1777104693:i=44122:nm=2:rtra=on:gsp=on_2831 on theBenchmark for (2831ds/44122Mi) % 158.98/23.17 % (2769557)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.98/23.17 % (2769557)Terminated due to inappropriate strategy. % 158.98/23.17 % (2769557)------------------------------ % 158.98/23.17 % (2769557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.98/23.17 % (2769557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.98/23.17 % (2769557)CaDiCaL version: 2.1.3 % 158.98/23.17 % (2769557)Termination reason: Inappropriate % 158.98/23.17 % (2769557)Time elapsed: 0.0000 s % 158.98/23.17 % (2769557)Peak memory usage: 10 MB % 158.98/23.17 % (2769557)------------------------------ % 158.98/23.17 % (2769557)------------------------------ % 158.98/23.17 % (2769559)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1838303879:i=19030:nm=5:rtra=on_2831 on theBenchmark for (2831ds/19030Mi) % 158.98/23.17 % (2769559)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.98/23.17 % (2769559)Terminated due to inappropriate strategy. % 158.98/23.17 % (2769559)------------------------------ % 158.98/23.17 % (2769559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.98/23.17 % (2769559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.98/23.17 % (2769559)CaDiCaL version: 2.1.3 % 158.98/23.17 % (2769559)Termination reason: Inappropriate % 158.98/23.17 % (2769559)Time elapsed: 0.0000 s % 158.98/23.17 % (2769559)Peak memory usage: 10 MB % 158.98/23.17 % (2769559)------------------------------ % 158.98/23.17 % (2769559)------------------------------ % 158.98/23.17 % (2769561)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=126207127:fmbsr=1.7:i=1840:rtra=on_2830 on theBenchmark for (2830ds/1840Mi) % 158.98/23.17 % (2769561)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.98/23.17 % (2769561)Terminated due to inappropriate strategy. % 158.98/23.17 % (2769561)------------------------------ % 158.98/23.17 % (2769561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.98/23.17 % (2769561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.14/25.41 % (2769561)CaDiCaL version: 2.1.3 % 175.14/25.41 % (2769561)Termination reason: Inappropriate % 175.14/25.41 % (2769561)Time elapsed: 0.0000 s % 175.14/25.41 % (2769561)Peak memory usage: 10 MB % 175.14/25.41 % (2769561)------------------------------ % 175.14/25.41 % (2769561)------------------------------ % 175.14/25.41 % (2769563)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2601594586:i=10262:rtra=on_2830 on theBenchmark for (2830ds/10262Mi) % 175.14/25.41 % (2769555)Instruction limit reached! % 175.14/25.41 % (2769555)------------------------------ % 175.14/25.41 % (2769555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.14/25.41 % (2769555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.14/25.41 % (2769555)CaDiCaL version: 2.1.3 % 175.14/25.41 % (2769555)Termination reason: Instruction limit % 175.14/25.41 % (2769555)Termination phase: Saturation % 175.14/25.41 % (2769555)Time elapsed: 0.562 s % 175.14/25.41 % (2769555)Peak memory usage: 27 MB % 175.14/25.41 % (2769555)Instructions burned: 1759 (million) % 175.14/25.41 % (2769565)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2513740294:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2829 on theBenchmark for (2829ds/2944Mi) % 175.14/25.41 % (2769565)Instruction limit reached! % 175.14/25.41 % (2769565)------------------------------ % 175.14/25.41 % (2769565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.14/25.41 % (2769565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.14/25.41 % (2769565)CaDiCaL version: 2.1.3 % 175.14/25.41 % (2769565)Termination reason: Instruction limit % 175.14/25.41 % (2769565)Termination phase: Saturation % 175.14/25.41 % (2769565)Time elapsed: 0.777 s % 175.14/25.41 % (2769565)Peak memory usage: 32 MB % 175.14/25.41 % (2769565)Instructions burned: 2944 (million) % 175.14/25.41 % (2769567)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3024776610:i=12648:rtra=on_2821 on theBenchmark for (2821ds/12648Mi) % 175.14/25.41 % (2769567)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 175.14/25.41 % (2769567)Terminated due to inappropriate strategy. % 175.14/25.41 % (2769567)------------------------------ % 175.14/25.41 % (2769567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.14/25.41 % (2769567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.14/25.41 % (2769567)CaDiCaL version: 2.1.3 % 175.14/25.41 % (2769567)Termination reason: Inappropriate % 175.14/25.41 % (2769567)Time elapsed: 0.0000 s % 175.14/25.41 % (2769567)Peak memory usage: 10 MB % 175.14/25.41 % (2769567)------------------------------ % 175.14/25.41 % (2769567)------------------------------ % 175.14/25.41 % (2769569)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3112045062:fmbsr=2.30978:i=4348:rtra=on_2821 on theBenchmark for (2821ds/4348Mi) % 175.14/25.41 % (2769569)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 175.14/25.41 % (2769569)Terminated due to inappropriate strategy. % 175.14/25.41 % (2769569)------------------------------ % 175.14/25.41 % (2769569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.14/25.41 % (2769569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.14/25.41 % (2769569)CaDiCaL version: 2.1.3 % 175.14/25.41 % (2769569)Termination reason: Inappropriate % 175.14/25.41 % (2769569)Time elapsed: 0.0000 s % 175.14/25.41 % (2769569)Peak memory usage: 10 MB % 175.14/25.41 % (2769569)------------------------------ % 175.14/25.41 % (2769569)------------------------------ % 175.14/25.41 % (2769571)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3257482599:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2821 on theBenchmark for (2821ds/1738Mi) % 175.14/25.41 % (2769571)Instruction limit reached! % 175.14/25.41 % (2769571)------------------------------ % 175.14/25.41 % (2769571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.14/25.41 % (2769571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.14/25.41 % (2769571)CaDiCaL version: 2.1.3 % 175.14/25.41 % (2769571)Termination reason: Instruction limit % 175.14/25.41 % (2769571)Termination phase: Saturation % 175.14/25.41 % (2769571)Time elapsed: 0.638 s % 175.14/25.41 % (2769571)Peak memory usage: 22 MB % 175.14/25.41 % (2769571)Instructions burned: 1739 (million) % 175.14/25.41 % (2769573)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3950263597:i=10228:av=off:rtra=on_2815 on theBenchmark for (2815ds/10228Mi) % 175.14/25.41 % (2769563)Instruction limit reached! % 259.81/37.49 % (2769563)------------------------------ % 259.81/37.49 % (2769563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.81/37.49 % (2769563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.81/37.49 % (2769563)CaDiCaL version: 2.1.3 % 259.81/37.49 % (2769563)Termination reason: Instruction limit % 259.81/37.49 % (2769563)Termination phase: Saturation % 259.81/37.49 % (2769563)Time elapsed: 3.306 s % 259.81/37.49 % (2769563)Peak memory usage: 68 MB % 259.81/37.49 % (2769563)Instructions burned: 10265 (million) % 259.81/37.49 % (2769575)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=2618371809:i=108564:rtra=on_2797 on theBenchmark for (2797ds/108564Mi) % 259.81/37.49 % (2769575)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 259.81/37.49 % (2769575)Terminated due to inappropriate strategy. % 259.81/37.49 % (2769575)------------------------------ % 259.81/37.49 % (2769575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.81/37.49 % (2769575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.81/37.49 % (2769575)CaDiCaL version: 2.1.3 % 259.81/37.49 % (2769575)Termination reason: Inappropriate % 259.81/37.49 % (2769575)Time elapsed: 0.0000 s % 259.81/37.49 % (2769575)Peak memory usage: 10 MB % 259.81/37.49 % (2769575)------------------------------ % 259.81/37.49 % (2769575)------------------------------ % 259.81/37.49 % (2769577)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1034245116:i=7024:aac=none:rtra=on_2797 on theBenchmark for (2797ds/7024Mi) % 259.81/37.49 % (2769094)Instruction limit reached! % 259.81/37.49 % (2769094)------------------------------ % 259.81/37.49 % (2769094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.81/37.49 % (2769094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.81/37.49 % (2769094)CaDiCaL version: 2.1.3 % 259.81/37.49 % (2769094)Termination reason: Instruction limit % 259.81/37.49 % (2769094)Termination phase: Saturation % 259.81/37.49 % (2769094)Time elapsed: 13.115 s % 259.81/37.49 % (2769094)Peak memory usage: 142 MB % 259.81/37.49 % (2769094)Instructions burned: 53296 (million) % 259.81/37.49 % (2769579)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=824285128:i=7546:rtra=on:amm=off_2775 on theBenchmark for (2775ds/7546Mi) % 259.81/37.49 % (2769577)Instruction limit reached! % 259.81/37.49 % (2769577)------------------------------ % 259.81/37.49 % (2769577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.81/37.49 % (2769577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.81/37.49 % (2769577)CaDiCaL version: 2.1.3 % 259.81/37.49 % (2769577)Termination reason: Instruction limit % 259.81/37.49 % (2769577)Termination phase: Saturation % 259.81/37.49 % (2769577)Time elapsed: 2.221 s % 259.81/37.49 % (2769577)Peak memory usage: 50 MB % 259.81/37.49 % (2769577)Instructions burned: 7025 (million) % 259.81/37.49 % (2769581)ott+11_1_sil=16000:si=on:gs=on:random_seed=150179900:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2775 on theBenchmark for (2775ds/4502Mi) % 259.81/37.49 % (2769573)Instruction limit reached! % 259.81/37.49 % (2769573)------------------------------ % 259.81/37.49 % (2769573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.81/37.49 % (2769573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.81/37.49 % (2769573)CaDiCaL version: 2.1.3 % 259.81/37.49 % (2769573)Termination reason: Instruction limit % 259.81/37.49 % (2769573)Termination phase: Saturation % 259.81/37.49 % (2769573)Time elapsed: 4.102 s % 259.81/37.49 % (2769573)Peak memory usage: 43 MB % 259.81/37.49 % (2769573)Instructions burned: 10228 (million) % 259.81/37.49 % (2769583)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=2972976044:fmbsr=1.6:i=135068:rtra=on_2773 on theBenchmark for (2773ds/135068Mi) % 259.81/37.49 % (2769583)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 259.81/37.49 % (2769583)Terminated due to inappropriate strategy. % 259.81/37.49 % (2769583)------------------------------ % 259.81/37.49 % (2769583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.81/37.49 % (2769583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.81/37.49 % (2769583)CaDiCaL version: 2.1.3 % 259.81/37.49 % (2769583)Termination reason: Inappropriate % 259.81/37.49 % (2769583)Time elapsed: 0.0000 s % 259.81/37.49 % (2769583)Peak memory usage: 10 MB % 259.81/37.49 % (2769583)------------------------------ % 259.81/37.49 % (2769583)------------------------------ % 259.81/37.49 % (276958Terminated % 300.21/43.16 % Vampire exiting %------------------------------------------------------------------------------