%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX123_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n016.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:31 PM UTC 2026 % Result : Timeout 300.10s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWX123_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.18 % Computer : n016.cluster.edu % 0.07/0.18 % Model : x86_64 x86_64 % 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.18 % Memory : 8046.5625MB % 0.07/0.18 % OS : Linux 6.8.0-71-generic % 0.07/0.18 % CPULimit : 300 % 0.07/0.18 % WCLimit : 300 % 0.07/0.18 % DateTime : Mon Sep 28 15:07:19 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.21 Running first-order model finding % 0.07/0.21 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 % 2.35/0.61 % (3689913)Will run a generic schedule for satisfiability detection. % 2.35/0.61 % (3689922)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=776343792:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.35/0.61 % (3689919)% WARNING: option uhcvi not known. % 2.35/0.61 % (3689918)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=336361240_2999 on theBenchmark for (2999ds/0Mi) % 2.35/0.61 % (3689920)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1675918328:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.35/0.61 % (3689919)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1806921463:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.35/0.61 % (3689921)dis+10_1_sil=32000:sp=arity:random_seed=2009321959:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.35/0.61 % (3689923)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4141370921:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.35/0.61 % (3689924)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2181968551:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.35/0.61 % (3689918)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.35/0.61 % (3689918)Terminated due to inappropriate strategy. % 2.35/0.61 % (3689918)------------------------------ % 2.35/0.61 % (3689918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.35/0.61 % (3689918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.35/0.61 % (3689918)CaDiCaL version: 2.1.3 % 2.35/0.61 % (3689918)Termination reason: Inappropriate % 2.35/0.61 % (3689918)Time elapsed: 0.007 s % 2.35/0.61 % (3689918)Peak memory usage: 10 MB % 2.35/0.61 % (3689918)Instructions burned: 16 (million) % 2.35/0.61 % (3689918)------------------------------ % 2.35/0.61 % (3689918)------------------------------ % 2.35/0.61 % (3689922)Instruction limit reached! % 2.35/0.61 % (3689922)------------------------------ % 2.35/0.61 % (3689922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.35/0.61 % (3689922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.35/0.61 % (3689922)CaDiCaL version: 2.1.3 % 2.35/0.61 % (3689922)Termination reason: Instruction limit % 2.35/0.61 % (3689922)Termination phase: Saturation % 2.35/0.61 % (3689922)Time elapsed: 0.028 s % 2.35/0.61 % (3689922)Peak memory usage: 13 MB % 2.35/0.61 % (3689922)Instructions burned: 120 (million) % 2.35/0.61 % (3689932)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4039309194:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.35/0.61 % (3689934)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2239374118:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.35/0.61 % (3689932)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.35/0.61 % (3689932)Terminated due to inappropriate strategy. % 2.35/0.61 % (3689932)------------------------------ % 2.35/0.61 % (3689932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.35/0.61 % (3689932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.35/0.61 % (3689932)CaDiCaL version: 2.1.3 % 2.35/0.61 % (3689932)Termination reason: Inappropriate % 2.35/0.61 % (3689932)Time elapsed: 0.007 s % 2.35/0.61 % (3689932)Peak memory usage: 10 MB % 2.35/0.61 % (3689932)Instructions burned: 16 (million) % 2.35/0.61 % (3689932)------------------------------ % 2.35/0.61 % (3689932)------------------------------ % 2.35/0.61 % (3689921)Instruction limit reached! % 2.35/0.61 % (3689921)------------------------------ % 2.35/0.61 % (3689921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.35/0.61 % (3689921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.35/0.61 % (3689921)CaDiCaL version: 2.1.3 % 2.35/0.61 % (3689921)Termination reason: Instruction limit % 2.35/0.61 % (3689921)Termination phase: Saturation % 2.35/0.61 % (3689921)Time elapsed: 0.044 s % 2.35/0.61 % (3689921)Peak memory usage: 12 MB % 2.35/0.61 % (3689921)Instructions burned: 105 (million) % 2.35/0.61 % (3689937)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=2047834112:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 2.35/0.61 % (3689923)Instruction limit reached! % 2.35/0.61 % (3689923)------------------------------ % 2.35/0.61 % (3689923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.08/0.78 % (3689923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.08/0.78 % (3689923)CaDiCaL version: 2.1.3 % 3.08/0.78 % (3689923)Termination reason: Instruction limit % 3.08/0.78 % (3689923)Termination phase: Saturation % 3.08/0.78 % (3689923)Time elapsed: 0.057 s % 3.08/0.78 % (3689923)Peak memory usage: 13 MB % 3.08/0.78 % (3689923)Instructions burned: 132 (million) % 3.08/0.78 % (3689934)Instruction limit reached! % 3.08/0.78 % (3689934)------------------------------ % 3.08/0.78 % (3689934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.08/0.78 % (3689934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.08/0.78 % (3689934)CaDiCaL version: 2.1.3 % 3.08/0.78 % (3689938)ott-21_1_sil=16000:fs=off:random_seed=547722584:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.08/0.78 % (3689934)Termination reason: Instruction limit % 3.08/0.78 % (3689934)Termination phase: Saturation % 3.08/0.78 % (3689934)Time elapsed: 0.031 s % 3.08/0.78 % (3689934)Peak memory usage: 13 MB % 3.08/0.78 % (3689934)Instructions burned: 134 (million) % 3.08/0.78 % (3689942)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4146357851:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 3.08/0.78 % (3689940)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=616077245:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 3.08/0.78 % (3689942)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.08/0.78 % (3689942)Terminated due to inappropriate strategy. % 3.08/0.78 % (3689942)------------------------------ % 3.08/0.78 % (3689942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.08/0.78 % (3689942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.08/0.78 % (3689942)CaDiCaL version: 2.1.3 % 3.08/0.78 % (3689942)Termination reason: Inappropriate % 3.08/0.78 % (3689942)Time elapsed: 0.003 s % 3.08/0.78 % (3689942)Peak memory usage: 10 MB % 3.08/0.78 % (3689942)Instructions burned: 12 (million) % 3.08/0.78 % (3689942)------------------------------ % 3.08/0.78 % (3689942)------------------------------ % 3.08/0.78 % (3689924)Instruction limit reached! % 3.08/0.78 % (3689924)------------------------------ % 3.08/0.78 % (3689924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.08/0.78 % (3689924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.08/0.78 % (3689924)CaDiCaL version: 2.1.3 % 3.08/0.78 % (3689924)Termination reason: Instruction limit % 3.08/0.78 % (3689924)Termination phase: Saturation % 3.08/0.78 % (3689924)Time elapsed: 0.079 s % 3.08/0.78 % (3689924)Peak memory usage: 13 MB % 3.08/0.78 % (3689924)Instructions burned: 161 (million) % 3.08/0.78 % (3689945)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4128858374:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 3.08/0.78 % (3689946)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=462215761:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 3.08/0.78 % (3689946)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.08/0.78 % (3689946)Terminated due to inappropriate strategy. % 3.08/0.78 % (3689946)------------------------------ % 3.08/0.78 % (3689946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.08/0.78 % (3689946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.08/0.78 % (3689946)CaDiCaL version: 2.1.3 % 3.08/0.78 % (3689946)Termination reason: Inappropriate % 3.08/0.78 % (3689946)Time elapsed: 0.005 s % 3.08/0.78 % (3689946)Peak memory usage: 10 MB % 3.08/0.78 % (3689946)Instructions burned: 12 (million) % 3.08/0.78 % (3689946)------------------------------ % 3.08/0.78 % (3689946)------------------------------ % 3.08/0.78 % (3689949)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=2959563504: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.08/0.78 % (3689938)Instruction limit reached! % 3.08/0.78 % (3689938)------------------------------ % 3.08/0.78 % (3689938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.08/0.78 % (3689938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.08/0.78 % (3689938)CaDiCaL version: 2.1.3 % 3.08/0.78 % (3689938)Termination reason: Instruction limit % 3.08/0.78 % (3689938)Termination phase: Saturation % 13.93/2.25 % (3689938)Time elapsed: 0.073 s % 13.93/2.25 % (3689938)Peak memory usage: 13 MB % 13.93/2.25 % (3689938)Instructions burned: 180 (million) % 13.93/2.25 % (3689951)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2215086002:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 13.93/2.25 % (3689940)Instruction limit reached! % 13.93/2.25 % (3689940)------------------------------ % 13.93/2.25 % (3689940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.93/2.25 % (3689940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.93/2.25 % (3689940)CaDiCaL version: 2.1.3 % 13.93/2.25 % (3689940)Termination reason: Instruction limit % 13.93/2.25 % (3689940)Termination phase: Saturation % 13.93/2.25 % (3689940)Time elapsed: 0.186 s % 13.93/2.25 % (3689940)Peak memory usage: 13 MB % 13.93/2.25 % (3689940)Instructions burned: 479 (million) % 13.93/2.25 % (3689953)fmb+10_1_sil=64000:random_seed=605845883:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 13.93/2.25 % (3689953)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 13.93/2.25 % (3689953)Terminated due to inappropriate strategy. % 13.93/2.25 % (3689953)------------------------------ % 13.93/2.25 % (3689953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.93/2.25 % (3689953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.93/2.25 % (3689953)CaDiCaL version: 2.1.3 % 13.93/2.25 % (3689953)Termination reason: Inappropriate % 13.93/2.25 % (3689953)Time elapsed: 0.007 s % 13.93/2.25 % (3689953)Peak memory usage: 10 MB % 13.93/2.25 % (3689953)Instructions burned: 16 (million) % 13.93/2.25 % (3689953)------------------------------ % 13.93/2.25 % (3689953)------------------------------ % 13.93/2.25 % (3689955)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3243211133:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 13.93/2.25 % (3689955)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 13.93/2.25 % (3689955)Terminated due to inappropriate strategy. % 13.93/2.25 % (3689955)------------------------------ % 13.93/2.25 % (3689955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.93/2.25 % (3689955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.93/2.25 % (3689955)CaDiCaL version: 2.1.3 % 13.93/2.25 % (3689955)Termination reason: Inappropriate % 13.93/2.25 % (3689955)Time elapsed: 0.007 s % 13.93/2.25 % (3689955)Peak memory usage: 11 MB % 13.93/2.25 % (3689955)Instructions burned: 16 (million) % 13.93/2.25 % (3689955)------------------------------ % 13.93/2.25 % (3689955)------------------------------ % 13.93/2.25 % (3689945)Instruction limit reached! % 13.93/2.25 % (3689945)------------------------------ % 13.93/2.25 % (3689945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.93/2.25 % (3689945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.93/2.25 % (3689945)CaDiCaL version: 2.1.3 % 13.93/2.25 % (3689945)Termination reason: Instruction limit % 13.93/2.25 % (3689945)Termination phase: Saturation % 13.93/2.25 % (3689945)Time elapsed: 0.240 s % 13.93/2.25 % (3689945)Peak memory usage: 13 MB % 13.93/2.25 % (3689945)Instructions burned: 1183 (million) % 13.93/2.25 % (3689957)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3677661469:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 13.93/2.25 % (3689958)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=817651442:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 13.93/2.25 % (3689937)Instruction limit reached! % 13.93/2.25 % (3689937)------------------------------ % 13.93/2.25 % (3689937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.93/2.25 % (3689937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.93/2.25 % (3689937)CaDiCaL version: 2.1.3 % 13.93/2.25 % (3689937)Termination reason: Instruction limit % 13.93/2.25 % (3689937)Termination phase: Saturation % 13.93/2.25 % (3689937)Time elapsed: 0.285 s % 13.93/2.25 % (3689937)Peak memory usage: 15 MB % 13.93/2.25 % (3689937)Instructions burned: 684 (million) % 13.93/2.25 % (3689957)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 13.93/2.25 % (3689957)Terminated due to inappropriate strategy. % 13.93/2.25 % (3689957)------------------------------ % 13.93/2.25 % (3689957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.93/2.25 % (3689957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.85/3.07 % (3689957)CaDiCaL version: 2.1.3 % 19.85/3.07 % (3689957)Termination reason: Inappropriate % 19.85/3.07 % (3689957)Time elapsed: 0.007 s % 19.85/3.07 % (3689957)Peak memory usage: 10 MB % 19.85/3.07 % (3689957)Instructions burned: 16 (million) % 19.85/3.07 % (3689957)------------------------------ % 19.85/3.07 % (3689957)------------------------------ % 19.85/3.07 % (3689961)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2276795807:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 19.85/3.07 % (3689962)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3504964068:i=6324_2996 on theBenchmark for (2996ds/6324Mi) % 19.85/3.07 % (3689962)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.85/3.07 % (3689962)Terminated due to inappropriate strategy. % 19.85/3.07 % (3689962)------------------------------ % 19.85/3.07 % (3689962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.85/3.07 % (3689962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.85/3.07 % (3689962)CaDiCaL version: 2.1.3 % 19.85/3.07 % (3689962)Termination reason: Inappropriate % 19.85/3.07 % (3689962)Time elapsed: 0.007 s % 19.85/3.07 % (3689962)Peak memory usage: 10 MB % 19.85/3.07 % (3689962)Instructions burned: 16 (million) % 19.85/3.07 % (3689962)------------------------------ % 19.85/3.07 % (3689962)------------------------------ % 19.85/3.07 % (3689965)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=90379203:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 19.85/3.07 % (3689965)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.85/3.07 % (3689965)Terminated due to inappropriate strategy. % 19.85/3.07 % (3689965)------------------------------ % 19.85/3.07 % (3689965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.85/3.07 % (3689965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.85/3.07 % (3689965)CaDiCaL version: 2.1.3 % 19.85/3.07 % (3689965)Termination reason: Inappropriate % 19.85/3.07 % (3689965)Time elapsed: 0.007 s % 19.85/3.07 % (3689965)Peak memory usage: 10 MB % 19.85/3.07 % (3689965)Instructions burned: 16 (million) % 19.85/3.07 % (3689965)------------------------------ % 19.85/3.07 % (3689965)------------------------------ % 19.85/3.07 % (3689949)Instruction limit reached! % 19.85/3.07 % (3689949)------------------------------ % 19.85/3.07 % (3689949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.85/3.07 % (3689949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.85/3.07 % (3689949)CaDiCaL version: 2.1.3 % 19.85/3.07 % (3689949)Termination reason: Instruction limit % 19.85/3.07 % (3689949)Termination phase: Saturation % 19.85/3.07 % (3689949)Time elapsed: 0.284 s % 19.85/3.07 % (3689949)Peak memory usage: 14 MB % 19.85/3.07 % (3689949)Instructions burned: 693 (million) % 19.85/3.07 % (3689967)ott-2_1_sil=16000:newcnf=on:random_seed=3539329611:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi) % 19.85/3.07 % (3689968)ott+10_1_sil=32000:tgt=ground:random_seed=167718669:i=5114:av=off_2995 on theBenchmark for (2995ds/5114Mi) % 19.85/3.07 % (3689951)Instruction limit reached! % 19.85/3.07 % (3689951)------------------------------ % 19.85/3.07 % (3689951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.85/3.07 % (3689951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.85/3.07 % (3689951)CaDiCaL version: 2.1.3 % 19.85/3.07 % (3689951)Termination reason: Instruction limit % 19.85/3.07 % (3689951)Termination phase: Saturation % 19.85/3.07 % (3689951)Time elapsed: 0.334 s % 19.85/3.07 % (3689951)Peak memory usage: 13 MB % 19.85/3.07 % (3689951)Instructions burned: 881 (million) % 19.85/3.07 % (3689971)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1994037426:i=54282_2994 on theBenchmark for (2994ds/54282Mi) % 19.85/3.07 % (3689971)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.85/3.07 % (3689971)Terminated due to inappropriate strategy. % 19.85/3.07 % (3689971)------------------------------ % 19.85/3.07 % (3689971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.85/3.07 % (3689971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.85/3.07 % (3689971)CaDiCaL version: 2.1.3 % 19.85/3.07 % (3689971)Termination reason: Inappropriate % 19.85/3.07 % (3689971)Time elapsed: 0.007 s % 19.85/3.07 % (3689971)Peak memory usage: 10 MB % 19.85/3.07 % (3689971)Instructions burned: 16 (million) % 73.55/10.61 % (3689971)------------------------------ % 73.55/10.61 % (3689971)------------------------------ % 73.55/10.61 % (3689973)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4073390127:i=3512:aac=none_2994 on theBenchmark for (2994ds/3512Mi) % 73.55/10.61 % (3689967)Instruction limit reached! % 73.55/10.61 % (3689967)------------------------------ % 73.55/10.61 % (3689967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.55/10.61 % (3689967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.55/10.61 % (3689967)CaDiCaL version: 2.1.3 % 73.55/10.61 % (3689967)Termination reason: Instruction limit % 73.55/10.61 % (3689967)Termination phase: Saturation % 73.55/10.61 % (3689967)Time elapsed: 0.347 s % 73.55/10.61 % (3689967)Peak memory usage: 14 MB % 73.55/10.61 % (3689967)Instructions burned: 870 (million) % 73.55/10.61 % (3689975)dis+21_1_sil=32000:sas=cadical:random_seed=795321486:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 73.55/10.61 % (3689961)Instruction limit reached! % 73.55/10.61 % (3689961)------------------------------ % 73.55/10.61 % (3689961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.55/10.61 % (3689961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.55/10.61 % (3689961)CaDiCaL version: 2.1.3 % 73.55/10.61 % (3689961)Termination reason: Instruction limit % 73.55/10.61 % (3689961)Termination phase: Saturation % 73.55/10.61 % (3689961)Time elapsed: 0.766 s % 73.55/10.61 % (3689961)Peak memory usage: 24 MB % 73.55/10.61 % (3689961)Instructions burned: 1473 (million) % 73.55/10.61 % (3689977)ott+11_1_sil=16000:gs=on:random_seed=4108061990:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 73.55/10.61 % (3689958)Instruction limit reached! % 73.55/10.61 % (3689958)------------------------------ % 73.55/10.61 % (3689958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.55/10.61 % (3689958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.55/10.61 % (3689958)CaDiCaL version: 2.1.3 % 73.55/10.61 % (3689958)Termination reason: Instruction limit % 73.55/10.61 % (3689958)Termination phase: Saturation % 73.55/10.61 % (3689958)Time elapsed: 1.062 s % 73.55/10.61 % (3689958)Peak memory usage: 19 MB % 73.55/10.61 % (3689958)Instructions burned: 5131 (million) % 73.55/10.61 % (3689979)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2707746376:fmbsr=1.6:i=67534_2985 on theBenchmark for (2985ds/67534Mi) % 73.55/10.61 % (3689979)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 73.55/10.61 % (3689979)Terminated due to inappropriate strategy. % 73.55/10.61 % (3689979)------------------------------ % 73.55/10.61 % (3689979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.55/10.61 % (3689979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.55/10.61 % (3689979)CaDiCaL version: 2.1.3 % 73.55/10.61 % (3689979)Termination reason: Inappropriate % 73.55/10.61 % (3689979)Time elapsed: 0.003 s % 73.55/10.61 % (3689979)Peak memory usage: 10 MB % 73.55/10.61 % (3689979)Instructions burned: 16 (million) % 73.55/10.61 % (3689979)------------------------------ % 73.55/10.61 % (3689979)------------------------------ % 73.55/10.61 % (3689981)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3425577950:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2985 on theBenchmark for (2985ds/4591Mi) % 73.55/10.61 % (3689973)Instruction limit reached! % 73.55/10.61 % (3689973)------------------------------ % 73.55/10.61 % (3689973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.55/10.61 % (3689973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.55/10.61 % (3689973)CaDiCaL version: 2.1.3 % 73.55/10.61 % (3689973)Termination reason: Instruction limit % 73.55/10.61 % (3689973)Termination phase: Saturation % 73.55/10.61 % (3689973)Time elapsed: 1.357 s % 73.55/10.61 % (3689973)Peak memory usage: 17 MB % 73.55/10.61 % (3689973)Instructions burned: 3513 (million) % 73.55/10.61 % (3689983)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2933215588:i=29340_2980 on theBenchmark for (2980ds/29340Mi) % 73.55/10.61 % (3689977)Instruction limit reached! % 73.55/10.61 % (3689977)------------------------------ % 73.55/10.61 % (3689977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.55/10.61 % (3689977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.55/10.61 % (3689977)CaDiCaL version: 2.1.3 % 73.55/10.61 % (3689977)Termination reason: Instruction limit % 83.72/12.04 % (3689977)Termination phase: Saturation % 83.72/12.04 % (3689977)Time elapsed: 0.838 s % 83.72/12.04 % (3689977)Peak memory usage: 13 MB % 83.72/12.04 % (3689977)Instructions burned: 2252 (million) % 83.72/12.04 % (3689985)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3036509185:i=5211_2979 on theBenchmark for (2979ds/5211Mi) % 83.72/12.04 % (3689975)Instruction limit reached! % 83.72/12.04 % (3689975)------------------------------ % 83.72/12.04 % (3689975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.72/12.04 % (3689975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.72/12.04 % (3689975)CaDiCaL version: 2.1.3 % 83.72/12.04 % (3689975)Termination reason: Instruction limit % 83.72/12.04 % (3689975)Termination phase: Saturation % 83.72/12.04 % (3689975)Time elapsed: 1.433 s % 83.72/12.04 % (3689975)Peak memory usage: 16 MB % 83.72/12.04 % (3689975)Instructions burned: 3774 (million) % 83.72/12.04 % (3689987)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=634558419:i=5497:nm=2_2977 on theBenchmark for (2977ds/5497Mi) % 83.72/12.04 % (3689987)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 83.72/12.04 % (3689987)Terminated due to inappropriate strategy. % 83.72/12.04 % (3689987)------------------------------ % 83.72/12.04 % (3689987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.72/12.04 % (3689987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.72/12.04 % (3689987)CaDiCaL version: 2.1.3 % 83.72/12.04 % (3689987)Termination reason: Inappropriate % 83.72/12.04 % (3689987)Time elapsed: 0.007 s % 83.72/12.04 % (3689987)Peak memory usage: 10 MB % 83.72/12.04 % (3689987)Instructions burned: 16 (million) % 83.72/12.04 % (3689987)------------------------------ % 83.72/12.04 % (3689987)------------------------------ % 83.72/12.04 % (3689989)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=95853058:fmbsr=2:i=46332_2977 on theBenchmark for (2977ds/46332Mi) % 83.72/12.04 % (3689989)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 83.72/12.04 % (3689989)Terminated due to inappropriate strategy. % 83.72/12.04 % (3689989)------------------------------ % 83.72/12.04 % (3689989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.72/12.04 % (3689989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.72/12.04 % (3689989)CaDiCaL version: 2.1.3 % 83.72/12.04 % (3689989)Termination reason: Inappropriate % 83.72/12.04 % (3689989)Time elapsed: 0.007 s % 83.72/12.04 % (3689989)Peak memory usage: 10 MB % 83.72/12.04 % (3689989)Instructions burned: 16 (million) % 83.72/12.04 % (3689989)------------------------------ % 83.72/12.04 % (3689989)------------------------------ % 83.72/12.04 % (3689991)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1192335303:i=14071_2976 on theBenchmark for (2976ds/14071Mi) % 83.72/12.04 % (3689991)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 83.72/12.04 % (3689991)Terminated due to inappropriate strategy. % 83.72/12.04 % (3689991)------------------------------ % 83.72/12.04 % (3689991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.72/12.04 % (3689991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.72/12.04 % (3689991)CaDiCaL version: 2.1.3 % 83.72/12.04 % (3689991)Termination reason: Inappropriate % 83.72/12.04 % (3689991)Time elapsed: 0.007 s % 83.72/12.04 % (3689991)Peak memory usage: 10 MB % 83.72/12.04 % (3689991)Instructions burned: 16 (million) % 83.72/12.04 % (3689991)------------------------------ % 83.72/12.04 % (3689991)------------------------------ % 83.72/12.04 % (3689993)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2160103798:i=22565:add=on:rawr=on_2976 on theBenchmark for (2976ds/22565Mi) % 83.72/12.04 % (3689968)Instruction limit reached! % 83.72/12.04 % (3689968)------------------------------ % 83.72/12.04 % (3689968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.72/12.04 % (3689968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.72/12.04 % (3689968)CaDiCaL version: 2.1.3 % 83.72/12.04 % (3689968)Termination reason: Instruction limit % 83.72/12.04 % (3689968)Termination phase: Saturation % 83.72/12.04 % (3689968)Time elapsed: 1.957 s % 83.72/12.04 % (3689968)Peak memory usage: 14 MB % 83.72/12.04 % (3689968)Instructions burned: 5115 (million) % 83.72/12.04 % (3689995)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3090778781:i=8173:av=off_2975 on theBenchmark for (2975ds/8173Mi) % 83.72/12.04 % (3689981)Instruction limit reached! % 84.43/12.18 % (3689981)------------------------------ % 84.43/12.18 % (3689981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.43/12.18 % (3689981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.43/12.18 % (3689981)CaDiCaL version: 2.1.3 % 84.43/12.18 % (3689981)Termination reason: Instruction limit % 84.43/12.18 % (3689981)Termination phase: Saturation % 84.43/12.18 % (3689981)Time elapsed: 1.379 s % 84.43/12.18 % (3689981)Peak memory usage: 45 MB % 84.43/12.18 % (3689981)Instructions burned: 4593 (million) % 84.43/12.18 % (3689997)dis+10_16:1_sil=16000:random_seed=3864997123:i=9155:fsr=off_2971 on theBenchmark for (2971ds/9155Mi) % 84.43/12.18 % (3689985)Instruction limit reached! % 84.43/12.18 % (3689985)------------------------------ % 84.43/12.18 % (3689985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.43/12.18 % (3689985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.43/12.18 % (3689985)CaDiCaL version: 2.1.3 % 84.43/12.18 % (3689985)Termination reason: Instruction limit % 84.43/12.18 % (3689985)Termination phase: Saturation % 84.43/12.18 % (3689985)Time elapsed: 1.981 s % 84.43/12.18 % (3689985)Peak memory usage: 21 MB % 84.43/12.18 % (3689985)Instructions burned: 5211 (million) % 84.43/12.18 % (3689999)ott-3_8_sil=64000:random_seed=1052263605:i=20139:bs=on_2959 on theBenchmark for (2959ds/20139Mi) % 84.43/12.18 % (3689997)Instruction limit reached! % 84.43/12.18 % (3689997)------------------------------ % 84.43/12.18 % (3689997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.43/12.18 % (3689997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.43/12.18 % (3689997)CaDiCaL version: 2.1.3 % 84.43/12.18 % (3689997)Termination reason: Instruction limit % 84.43/12.18 % (3689997)Termination phase: Saturation % 84.43/12.18 % (3689997)Time elapsed: 1.830 s % 84.43/12.18 % (3689997)Peak memory usage: 18 MB % 84.43/12.18 % (3689997)Instructions burned: 9159 (million) % 84.43/12.18 % (3690001)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3498156202:fmbsr=2:i=32576_2953 on theBenchmark for (2953ds/32576Mi) % 84.43/12.18 % (3690001)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 84.43/12.18 % (3690001)Terminated due to inappropriate strategy. % 84.43/12.18 % (3690001)------------------------------ % 84.43/12.18 % (3690001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.43/12.18 % (3690001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.43/12.18 % (3690001)CaDiCaL version: 2.1.3 % 84.43/12.18 % (3690001)Termination reason: Inappropriate % 84.43/12.18 % (3690001)Time elapsed: 0.003 s % 84.43/12.18 % (3690001)Peak memory usage: 10 MB % 84.43/12.18 % (3690001)Instructions burned: 16 (million) % 84.43/12.18 % (3690001)------------------------------ % 84.43/12.18 % (3690001)------------------------------ % 84.43/12.18 % (3690003)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1169035503:i=11404_2952 on theBenchmark for (2952ds/11404Mi) % 84.43/12.18 % (3689995)Instruction limit reached! % 84.43/12.18 % (3689995)------------------------------ % 84.43/12.18 % (3689995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.43/12.18 % (3689995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.43/12.18 % (3689995)CaDiCaL version: 2.1.3 % 84.43/12.18 % (3689995)Termination reason: Instruction limit % 84.43/12.18 % (3689995)Termination phase: Saturation % 84.43/12.18 % (3689995)Time elapsed: 3.150 s % 84.43/12.18 % (3689995)Peak memory usage: 16 MB % 84.43/12.18 % (3689995)Instructions burned: 8175 (million) % 84.43/12.18 % (3690005)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=123610764:i=14134_2944 on theBenchmark for (2944ds/14134Mi) % 84.43/12.18 % (3690003)Instruction limit reached! % 84.43/12.18 % (3690003)------------------------------ % 84.43/12.18 % (3690003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.43/12.18 % (3690003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.43/12.18 % (3690003)CaDiCaL version: 2.1.3 % 84.43/12.18 % (3690003)Termination reason: Instruction limit % 84.43/12.18 % (3690003)Termination phase: Saturation % 84.43/12.18 % (3690003)Time elapsed: 2.358 s % 84.43/12.18 % (3690003)Peak memory usage: 17 MB % 84.43/12.18 % (3690003)Instructions burned: 11406 (million) % 84.43/12.18 % (3690007)dis+33_16_sil=32000:sac=on:random_seed=217428547:i=15851:nm=0_2929 on theBenchmark for (2929ds/15851Mi) % 84.43/12.18 % (3690007)Instruction limit reached! % 84.43/12.18 % (3690007)------------------------------ % 84.43/12.18 % (3690007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.13/15.30 % (3690007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.13/15.30 % (3690007)CaDiCaL version: 2.1.3 % 106.13/15.30 % (3690007)Termination reason: Instruction limit % 106.13/15.30 % (3690007)Termination phase: Saturation % 106.13/15.30 % (3690007)Time elapsed: 3.290 s % 106.13/15.30 % (3690007)Peak memory usage: 25 MB % 106.13/15.30 % (3690007)Instructions burned: 15856 (million) % 106.13/15.30 % (3690009)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2830028537:avsq=on:i=17627:add=on:amm=off_2896 on theBenchmark for (2896ds/17627Mi) % 106.13/15.30 % (3690005)Instruction limit reached! % 106.13/15.30 % (3690005)------------------------------ % 106.13/15.30 % (3690005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.13/15.30 % (3690005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.13/15.30 % (3690005)CaDiCaL version: 2.1.3 % 106.13/15.30 % (3690005)Termination reason: Instruction limit % 106.13/15.30 % (3690005)Termination phase: Saturation % 106.13/15.30 % (3690005)Time elapsed: 5.491 s % 106.13/15.30 % (3690005)Peak memory usage: 18 MB % 106.13/15.30 % (3690005)Instructions burned: 14137 (million) % 106.13/15.30 % (3690011)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4212856958:s2a=on:i=53295_2888 on theBenchmark for (2888ds/53295Mi) % 106.13/15.30 % (3689993)Instruction limit reached! % 106.13/15.30 % (3689993)------------------------------ % 106.13/15.30 % (3689993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.13/15.30 % (3689993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.13/15.30 % (3689993)CaDiCaL version: 2.1.3 % 106.13/15.30 % (3689993)Termination reason: Instruction limit % 106.13/15.30 % (3689993)Termination phase: Saturation % 106.13/15.30 % (3689993)Time elapsed: 9.123 s % 106.13/15.30 % (3689993)Peak memory usage: 17 MB % 106.13/15.30 % (3689993)Instructions burned: 22568 (million) % 106.13/15.30 % (3690013)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3901105080:i=26857:ins=20_2885 on theBenchmark for (2885ds/26857Mi) % 106.13/15.30 % (3690013)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 106.13/15.30 % (3690013)Terminated due to inappropriate strategy. % 106.13/15.30 % (3690013)------------------------------ % 106.13/15.30 % (3690013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.13/15.30 % (3690013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.13/15.30 % (3690013)CaDiCaL version: 2.1.3 % 106.13/15.30 % (3690013)Termination reason: Inappropriate % 106.13/15.30 % (3690013)Time elapsed: 0.007 s % 106.13/15.30 % (3690013)Peak memory usage: 10 MB % 106.13/15.30 % (3690013)Instructions burned: 16 (million) % 106.13/15.30 % (3690013)------------------------------ % 106.13/15.30 % (3690013)------------------------------ % 106.13/15.30 % (3690015)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=446573634:i=28120:bs=on:fsr=off_2884 on theBenchmark for (2884ds/28120Mi) % 106.13/15.30 % (3689999)Instruction limit reached! % 106.13/15.30 % (3689999)------------------------------ % 106.13/15.30 % (3689999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.13/15.30 % (3689999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.13/15.30 % (3689999)CaDiCaL version: 2.1.3 % 106.13/15.30 % (3689999)Termination reason: Instruction limit % 106.13/15.30 % (3689999)Termination phase: Saturation % 106.13/15.30 % (3689999)Time elapsed: 7.720 s % 106.13/15.30 % (3689999)Peak memory usage: 22 MB % 106.13/15.30 % (3689999)Instructions burned: 20140 (million) % 106.13/15.30 % (3690017)fmb+10_1_sil=256000:fmbss=7:random_seed=1976662211:fmbsr=1.6:i=182295_2882 on theBenchmark for (2882ds/182295Mi) % 106.13/15.30 % (3690017)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 106.13/15.30 % (3690017)Terminated due to inappropriate strategy. % 106.13/15.30 % (3690017)------------------------------ % 106.13/15.30 % (3690017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.13/15.30 % (3690017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.13/15.30 % (3690017)CaDiCaL version: 2.1.3 % 106.13/15.30 % (3690017)Termination reason: Inappropriate % 106.13/15.30 % (3690017)Time elapsed: 0.007 s % 106.13/15.30 % (3690017)Peak memory usage: 10 MB % 106.13/15.30 % (3690017)Instructions burned: 16 (million) % 106.13/15.30 % (3690017)------------------------------ % 106.13/15.30 % (3690017)------------------------------ % 106.13/15.30 % (3690019)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1111031748:i=44625:gsp=on_2882 on theBenchmark for (2882ds/44625Mi) % 111.02/15.98 % (3690019)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.02/15.98 % (3690019)Terminated due to inappropriate strategy. % 111.02/15.98 % (3690019)------------------------------ % 111.02/15.98 % (3690019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.02/15.98 % (3690019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.02/15.98 % (3690019)CaDiCaL version: 2.1.3 % 111.02/15.98 % (3690019)Termination reason: Inappropriate % 111.02/15.98 % (3690019)Time elapsed: 0.007 s % 111.02/15.98 % (3690019)Peak memory usage: 11 MB % 111.02/15.98 % (3690019)Instructions burned: 16 (million) % 111.02/15.98 % (3690019)------------------------------ % 111.02/15.98 % (3690019)------------------------------ % 111.02/15.98 % (3690021)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3298589404:i=160505_2881 on theBenchmark for (2881ds/160505Mi) % 111.02/15.98 % (3690021)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.02/15.98 % (3690021)Terminated due to inappropriate strategy. % 111.02/15.98 % (3690021)------------------------------ % 111.02/15.98 % (3690021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.02/15.98 % (3690021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.02/15.98 % (3690021)CaDiCaL version: 2.1.3 % 111.02/15.98 % (3690021)Termination reason: Inappropriate % 111.02/15.98 % (3690021)Time elapsed: 0.007 s % 111.02/15.98 % (3690021)Peak memory usage: 10 MB % 111.02/15.98 % (3690021)Instructions burned: 16 (million) % 111.02/15.98 % (3690021)------------------------------ % 111.02/15.98 % (3690021)------------------------------ % 111.02/15.98 % (3690023)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1081436895:fmbsr=1.3:i=225729_2881 on theBenchmark for (2881ds/225729Mi) % 111.02/15.98 % (3690023)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.02/15.98 % (3690023)Terminated due to inappropriate strategy. % 111.02/15.98 % (3690023)------------------------------ % 111.02/15.98 % (3690023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.02/15.98 % (3690023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.02/15.98 % (3690023)CaDiCaL version: 2.1.3 % 111.02/15.98 % (3690023)Termination reason: Inappropriate % 111.02/15.98 % (3690023)Time elapsed: 0.007 s % 111.02/15.98 % (3690023)Peak memory usage: 10 MB % 111.02/15.98 % (3690023)Instructions burned: 16 (million) % 111.02/15.98 % (3690023)------------------------------ % 111.02/15.98 % (3690023)------------------------------ % 111.02/15.98 % (3690025)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3182045149:fmbsr=2:i=185024:ins=7_2881 on theBenchmark for (2881ds/185024Mi) % 111.02/15.98 % (3690025)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.02/15.98 % (3690025)Terminated due to inappropriate strategy. % 111.02/15.98 % (3690025)------------------------------ % 111.02/15.98 % (3690025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.02/15.98 % (3690025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.02/15.98 % (3690025)CaDiCaL version: 2.1.3 % 111.02/15.98 % (3690025)Termination reason: Inappropriate % 111.02/15.98 % (3690025)Time elapsed: 0.007 s % 111.02/15.98 % (3690025)Peak memory usage: 10 MB % 111.02/15.98 % (3690025)Instructions burned: 16 (million) % 111.02/15.98 % (3690025)------------------------------ % 111.02/15.98 % (3690025)------------------------------ % 111.02/15.98 % (3690027)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1091370448:rtra=on_2880 on theBenchmark for (2880ds/0Mi) % 111.02/15.98 % (3690027)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.02/15.98 % (3690027)Terminated due to inappropriate strategy. % 111.02/15.98 % (3690027)------------------------------ % 111.02/15.98 % (3690027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.02/15.98 % (3690027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.02/15.98 % (3690027)CaDiCaL version: 2.1.3 % 111.02/15.98 % (3690027)Termination reason: Inappropriate % 111.02/15.98 % (3690027)Time elapsed: 0.007 s % 111.02/15.98 % (3690027)Peak memory usage: 11 MB % 111.02/15.98 % (3690027)Instructions burned: 16 (million) % 111.02/15.98 % (3690027)------------------------------ % 111.02/15.98 % (3690027)------------------------------ % 111.02/15.98 % (3690029)% WARNING: option uhcvi not known. % 111.02/15.98 % (3690029)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2046817113:i=271062:add=off:rtra=on:rawr=on_2880 on theBenchmark for (2880ds/271062Mi) % 119.89/17.19 % (3689983)Instruction limit reached! % 119.89/17.19 % (3689983)------------------------------ % 119.89/17.19 % (3689983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.89/17.19 % (3689983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.89/17.19 % (3689983)CaDiCaL version: 2.1.3 % 119.89/17.19 % (3689983)Termination reason: Instruction limit % 119.89/17.19 % (3689983)Termination phase: Saturation % 119.89/17.19 % (3689983)Time elapsed: 11.083 s % 119.89/17.19 % (3689983)Peak memory usage: 25 MB % 119.89/17.19 % (3689983)Instructions burned: 29341 (million) % 119.89/17.19 % (3690031)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1158778452:i=176048:add=on:rtra=on:rawr=on_2869 on theBenchmark for (2869ds/176048Mi) % 119.89/17.19 % (3690009)Instruction limit reached! % 119.89/17.19 % (3690009)------------------------------ % 119.89/17.19 % (3690009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.89/17.19 % (3690009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.89/17.19 % (3690009)CaDiCaL version: 2.1.3 % 119.89/17.19 % (3690009)Termination reason: Instruction limit % 119.89/17.19 % (3690009)Termination phase: Saturation % 119.89/17.19 % (3690009)Time elapsed: 4.389 s % 119.89/17.19 % (3690009)Peak memory usage: 161 MB % 119.89/17.19 % (3690009)Instructions burned: 17631 (million) % 119.89/17.19 % (3690392)dis+10_1_sil=32000:si=on:sp=arity:random_seed=470271110:i=206:fgj=on:rtra=on_2852 on theBenchmark for (2852ds/206Mi) % 119.89/17.19 % (3690392)Instruction limit reached! % 119.89/17.19 % (3690392)------------------------------ % 119.89/17.19 % (3690392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.89/17.19 % (3690392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.89/17.19 % (3690392)CaDiCaL version: 2.1.3 % 119.89/17.19 % (3690392)Termination reason: Instruction limit % 119.89/17.19 % (3690392)Termination phase: Saturation % 119.89/17.19 % (3690392)Time elapsed: 0.044 s % 119.89/17.19 % (3690392)Peak memory usage: 13 MB % 119.89/17.19 % (3690392)Instructions burned: 207 (million) % 119.89/17.19 % (3690394)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2395869835:i=232:rtra=on_2851 on theBenchmark for (2851ds/232Mi) % 119.89/17.19 % (3690394)Instruction limit reached! % 119.89/17.19 % (3690394)------------------------------ % 119.89/17.19 % (3690394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.89/17.19 % (3690394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.89/17.19 % (3690394)CaDiCaL version: 2.1.3 % 119.89/17.19 % (3690394)Termination reason: Instruction limit % 119.89/17.19 % (3690394)Termination phase: Saturation % 119.89/17.19 % (3690394)Time elapsed: 0.050 s % 119.89/17.19 % (3690394)Peak memory usage: 13 MB % 119.89/17.19 % (3690394)Instructions burned: 235 (million) % 119.89/17.19 % (3690396)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2860173529:i=262:rtra=on_2850 on theBenchmark for (2850ds/262Mi) % 119.89/17.19 % (3690396)Instruction limit reached! % 119.89/17.19 % (3690396)------------------------------ % 119.89/17.19 % (3690396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.89/17.19 % (3690396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.89/17.19 % (3690396)CaDiCaL version: 2.1.3 % 119.89/17.19 % (3690396)Termination reason: Instruction limit % 119.89/17.19 % (3690396)Termination phase: Saturation % 119.89/17.19 % (3690396)Time elapsed: 0.054 s % 119.89/17.19 % (3690396)Peak memory usage: 12 MB % 119.89/17.19 % (3690396)Instructions burned: 266 (million) % 119.89/17.19 % (3690398)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3304757001:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2850 on theBenchmark for (2850ds/318Mi) % 119.89/17.19 % (3690398)Instruction limit reached! % 119.89/17.19 % (3690398)------------------------------ % 119.89/17.19 % (3690398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.89/17.19 % (3690398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.89/17.19 % (3690398)CaDiCaL version: 2.1.3 % 119.89/17.19 % (3690398)Termination reason: Instruction limit % 119.89/17.19 % (3690398)Termination phase: Saturation % 119.89/17.19 % (3690398)Time elapsed: 0.071 s % 119.89/17.19 % (3690398)Peak memory usage: 13 MB % 119.89/17.19 % (3690398)Instructions burned: 321 (million) % 119.89/17.19 % (3690400)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1713458966:i=1428:nm=2:rtra=on_2849 on theBenchmark for (2849ds/1428Mi) % 141.18/20.18 % (3690400)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 141.18/20.18 % (3690400)Terminated due to inappropriate strategy. % 141.18/20.18 % (3690400)------------------------------ % 141.18/20.18 % (3690400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.18/20.18 % (3690400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.18/20.18 % (3690400)CaDiCaL version: 2.1.3 % 141.18/20.18 % (3690400)Termination reason: Inappropriate % 141.18/20.18 % (3690400)Time elapsed: 0.003 s % 141.18/20.18 % (3690400)Peak memory usage: 10 MB % 141.18/20.18 % (3690400)Instructions burned: 17 (million) % 141.18/20.18 % (3690400)------------------------------ % 141.18/20.18 % (3690400)------------------------------ % 141.18/20.18 % (3690402)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=882846295:i=262:bd=preordered:rtra=on:fsd=on_2849 on theBenchmark for (2849ds/262Mi) % 141.18/20.18 % (3690402)Instruction limit reached! % 141.18/20.18 % (3690402)------------------------------ % 141.18/20.18 % (3690402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.18/20.18 % (3690402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.18/20.18 % (3690402)CaDiCaL version: 2.1.3 % 141.18/20.18 % (3690402)Termination reason: Instruction limit % 141.18/20.18 % (3690402)Termination phase: Saturation % 141.18/20.18 % (3690402)Time elapsed: 0.055 s % 141.18/20.18 % (3690402)Peak memory usage: 13 MB % 141.18/20.18 % (3690402)Instructions burned: 267 (million) % 141.18/20.18 % (3690404)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=829742298:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2848 on theBenchmark for (2848ds/1368Mi) % 141.18/20.18 % (3690404)Instruction limit reached! % 141.18/20.18 % (3690404)------------------------------ % 141.18/20.18 % (3690404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.18/20.18 % (3690404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.18/20.18 % (3690404)CaDiCaL version: 2.1.3 % 141.18/20.18 % (3690404)Termination reason: Instruction limit % 141.18/20.18 % (3690404)Termination phase: Saturation % 141.18/20.18 % (3690404)Time elapsed: 0.303 s % 141.18/20.18 % (3690404)Peak memory usage: 17 MB % 141.18/20.18 % (3690404)Instructions burned: 1369 (million) % 141.18/20.18 % (3690406)ott-21_1_sil=16000:si=on:fs=off:random_seed=2029733895:i=360:av=off:fsr=off:rtra=on_2845 on theBenchmark for (2845ds/360Mi) % 141.18/20.18 % (3690406)Instruction limit reached! % 141.18/20.18 % (3690406)------------------------------ % 141.18/20.18 % (3690406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.18/20.18 % (3690406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.18/20.18 % (3690406)CaDiCaL version: 2.1.3 % 141.18/20.18 % (3690406)Termination reason: Instruction limit % 141.18/20.18 % (3690406)Termination phase: Saturation % 141.18/20.18 % (3690406)Time elapsed: 0.074 s % 141.18/20.18 % (3690406)Peak memory usage: 12 MB % 141.18/20.18 % (3690406)Instructions burned: 364 (million) % 141.18/20.18 % (3690408)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=564478192:i=954:bd=all:rtra=on_2844 on theBenchmark for (2844ds/954Mi) % 141.18/20.18 % (3690408)Instruction limit reached! % 141.18/20.18 % (3690408)------------------------------ % 141.18/20.18 % (3690408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.18/20.18 % (3690408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.18/20.18 % (3690408)CaDiCaL version: 2.1.3 % 141.18/20.18 % (3690408)Termination reason: Instruction limit % 141.18/20.18 % (3690408)Termination phase: Saturation % 141.18/20.18 % (3690408)Time elapsed: 0.194 s % 141.18/20.18 % (3690408)Peak memory usage: 13 MB % 141.18/20.18 % (3690408)Instructions burned: 959 (million) % 141.18/20.18 % (3690410)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=480136203:fmbsr=1.3:i=1730:ins=25:rtra=on_2842 on theBenchmark for (2842ds/1730Mi) % 141.18/20.18 % (3690410)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 141.18/20.18 % (3690410)Terminated due to inappropriate strategy. % 141.18/20.18 % (3690410)------------------------------ % 141.18/20.18 % (3690410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.18/20.18 % (3690410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.18/20.18 % (3690410)CaDiCaL version: 2.1.3 % 141.18/20.18 % (3690410)Termination reason: Inappropriate % 169.57/24.16 % (3690410)Time elapsed: 0.003 s % 169.57/24.16 % (3690410)Peak memory usage: 10 MB % 169.57/24.16 % (3690410)Instructions burned: 12 (million) % 169.57/24.16 % (3690410)------------------------------ % 169.57/24.16 % (3690410)------------------------------ % 169.57/24.16 % (3690412)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3589907922:i=2358:rtra=on_2842 on theBenchmark for (2842ds/2358Mi) % 169.57/24.16 % (3690412)Instruction limit reached! % 169.57/24.16 % (3690412)------------------------------ % 169.57/24.16 % (3690412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.57/24.16 % (3690412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.57/24.16 % (3690412)CaDiCaL version: 2.1.3 % 169.57/24.16 % (3690412)Termination reason: Instruction limit % 169.57/24.16 % (3690412)Termination phase: Saturation % 169.57/24.16 % (3690412)Time elapsed: 0.482 s % 169.57/24.16 % (3690412)Peak memory usage: 13 MB % 169.57/24.16 % (3690412)Instructions burned: 2360 (million) % 169.57/24.16 % (3690414)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4022002865:i=1778:ins=1:rtra=on_2837 on theBenchmark for (2837ds/1778Mi) % 169.57/24.16 % (3690414)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.57/24.16 % (3690414)Terminated due to inappropriate strategy. % 169.57/24.16 % (3690414)------------------------------ % 169.57/24.16 % (3690414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.57/24.16 % (3690414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.57/24.16 % (3690414)CaDiCaL version: 2.1.3 % 169.57/24.16 % (3690414)Termination reason: Inappropriate % 169.57/24.16 % (3690414)Time elapsed: 0.003 s % 169.57/24.16 % (3690414)Peak memory usage: 10 MB % 169.57/24.16 % (3690414)Instructions burned: 12 (million) % 169.57/24.16 % (3690414)------------------------------ % 169.57/24.16 % (3690414)------------------------------ % 169.57/24.16 % (3690416)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=2167412390:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2837 on theBenchmark for (2837ds/1384Mi) % 169.57/24.16 % (3690416)Instruction limit reached! % 169.57/24.16 % (3690416)------------------------------ % 169.57/24.16 % (3690416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.57/24.16 % (3690416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.57/24.16 % (3690416)CaDiCaL version: 2.1.3 % 169.57/24.16 % (3690416)Termination reason: Instruction limit % 169.57/24.16 % (3690416)Termination phase: Saturation % 169.57/24.16 % (3690416)Time elapsed: 0.292 s % 169.57/24.16 % (3690416)Peak memory usage: 15 MB % 169.57/24.16 % (3690416)Instructions burned: 1387 (million) % 169.57/24.16 % (3690418)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3485333940:i=1758:kws=inv_precedence:fsr=off:rtra=on_2834 on theBenchmark for (2834ds/1758Mi) % 169.57/24.16 % (3690418)Instruction limit reached! % 169.57/24.16 % (3690418)------------------------------ % 169.57/24.16 % (3690418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.57/24.16 % (3690418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.57/24.16 % (3690418)CaDiCaL version: 2.1.3 % 169.57/24.16 % (3690418)Termination reason: Instruction limit % 169.57/24.16 % (3690418)Termination phase: Saturation % 169.57/24.16 % (3690418)Time elapsed: 0.356 s % 169.57/24.16 % (3690418)Peak memory usage: 16 MB % 169.57/24.16 % (3690418)Instructions burned: 1762 (million) % 169.57/24.16 % (3690420)fmb+10_1_sil=64000:si=on:random_seed=2118729648:i=44122:nm=2:rtra=on:gsp=on_2830 on theBenchmark for (2830ds/44122Mi) % 169.57/24.16 % (3690420)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.57/24.16 % (3690420)Terminated due to inappropriate strategy. % 169.57/24.16 % (3690420)------------------------------ % 169.57/24.16 % (3690420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.57/24.16 % (3690420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.57/24.16 % (3690420)CaDiCaL version: 2.1.3 % 169.57/24.16 % (3690420)Termination reason: Inappropriate % 169.57/24.16 % (3690420)Time elapsed: 0.004 s % 169.57/24.16 % (3690420)Peak memory usage: 10 MB % 169.57/24.16 % (3690420)Instructions burned: 16 (million) % 169.57/24.16 % (3690420)------------------------------ % 169.57/24.16 % (3690420)------------------------------ % 169.57/24.16 % (3690422)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2648576248:i=19030:nm=5:rtra=on_2830 on theBenchmark for (2830ds/19030Mi) % 211.44/30.05 % (3690422)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 211.44/30.05 % (3690422)Terminated due to inappropriate strategy. % 211.44/30.05 % (3690422)------------------------------ % 211.44/30.05 % (3690422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.44/30.05 % (3690422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.44/30.05 % (3690422)CaDiCaL version: 2.1.3 % 211.44/30.05 % (3690422)Termination reason: Inappropriate % 211.44/30.05 % (3690422)Time elapsed: 0.003 s % 211.44/30.05 % (3690422)Peak memory usage: 10 MB % 211.44/30.05 % (3690422)Instructions burned: 16 (million) % 211.44/30.05 % (3690422)------------------------------ % 211.44/30.05 % (3690422)------------------------------ % 211.44/30.05 % (3690424)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=4220798573:fmbsr=1.7:i=1840:rtra=on_2830 on theBenchmark for (2830ds/1840Mi) % 211.44/30.05 % (3690424)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 211.44/30.05 % (3690424)Terminated due to inappropriate strategy. % 211.44/30.05 % (3690424)------------------------------ % 211.44/30.05 % (3690424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.44/30.05 % (3690424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.44/30.05 % (3690424)CaDiCaL version: 2.1.3 % 211.44/30.05 % (3690424)Termination reason: Inappropriate % 211.44/30.05 % (3690424)Time elapsed: 0.003 s % 211.44/30.05 % (3690424)Peak memory usage: 10 MB % 211.44/30.05 % (3690424)Instructions burned: 16 (million) % 211.44/30.05 % (3690424)------------------------------ % 211.44/30.05 % (3690424)------------------------------ % 211.44/30.05 % (3690426)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3456412497:i=10262:rtra=on_2830 on theBenchmark for (2830ds/10262Mi) % 211.44/30.05 % (3690426)Instruction limit reached! % 211.44/30.05 % (3690426)------------------------------ % 211.44/30.05 % (3690426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.44/30.05 % (3690426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.44/30.05 % (3690426)CaDiCaL version: 2.1.3 % 211.44/30.05 % (3690426)Termination reason: Instruction limit % 211.44/30.06 % (3690426)Termination phase: Saturation % 211.44/30.06 % (3690426)Time elapsed: 2.167 s % 211.44/30.06 % (3690426)Peak memory usage: 22 MB % 211.44/30.06 % (3690426)Instructions burned: 10263 (million) % 211.44/30.06 % (3690428)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2001350892:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2808 on theBenchmark for (2808ds/2944Mi) % 211.44/30.06 % (3690428)Instruction limit reached! % 211.44/30.06 % (3690428)------------------------------ % 211.44/30.06 % (3690428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.44/30.06 % (3690428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.44/30.06 % (3690428)CaDiCaL version: 2.1.3 % 211.44/30.06 % (3690428)Termination reason: Instruction limit % 211.44/30.06 % (3690428)Termination phase: Saturation % 211.44/30.06 % (3690428)Time elapsed: 0.746 s % 211.44/30.06 % (3690428)Peak memory usage: 31 MB % 211.44/30.06 % (3690428)Instructions burned: 2949 (million) % 211.44/30.06 % (3690430)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3304529696:i=12648:rtra=on_2800 on theBenchmark for (2800ds/12648Mi) % 211.44/30.06 % (3690430)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 211.44/30.06 % (3690430)Terminated due to inappropriate strategy. % 211.44/30.06 % (3690430)------------------------------ % 211.44/30.06 % (3690430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.44/30.06 % (3690430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.44/30.06 % (3690430)CaDiCaL version: 2.1.3 % 211.44/30.06 % (3690430)Termination reason: Inappropriate % 211.44/30.06 % (3690430)Time elapsed: 0.003 s % 211.44/30.06 % (3690430)Peak memory usage: 11 MB % 211.44/30.06 % (3690430)Instructions burned: 16 (million) % 211.44/30.06 % (3690430)------------------------------ % 211.44/30.06 % (3690430)------------------------------ % 211.44/30.06 % (3690432)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1967208136:fmbsr=2.30978:i=4348:rtra=on_2800 on theBenchmark for (2800ds/4348Mi) % 211.44/30.06 % (3690432)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 211.44/30.06 % (3690432)Terminated due to inappropriate strategy. % 211.44/30.06 % (3690432)-----------------------------Terminated % 300.10/42.54 % Vampire exiting % 300.10/42.54 Terminated %------------------------------------------------------------------------------