%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW635_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:34 PM UTC 2026 % Result : Timeout 300.13s 42.73s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWW635_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.11 % Computer : n012.cluster.edu % 0.06/0.11 % Model : x86_64 x86_64 % 0.06/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.11 % Memory : 8046.5625MB % 0.06/0.11 % OS : Linux 6.8.0-71-generic % 0.06/0.11 % CPULimit : 300 % 0.06/0.11 % WCLimit : 300 % 0.06/0.11 % DateTime : Mon Sep 28 14:23:04 UTC 2026 % 0.06/0.12 % CPUTime : % 0.06/0.12 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.13 Running first-order model finding % 0.06/0.13 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 % 1.91/0.49 % (3409085)Will run a generic schedule for satisfiability detection. % 1.91/0.49 % (3409098)% WARNING: option uhcvi not known. % 1.91/0.49 % (3409098)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=798422884:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 1.91/0.49 % (3409102)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=248081138:i=131_2999 on theBenchmark for (2999ds/131Mi) % 1.91/0.49 % (3409101)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=346103384:i=116_2999 on theBenchmark for (2999ds/116Mi) % 1.91/0.49 % (3409097)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1239779387_2999 on theBenchmark for (2999ds/0Mi) % 1.91/0.49 % (3409099)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2463225825:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 1.91/0.49 % (3409100)dis+10_1_sil=32000:sp=arity:random_seed=2618376277:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 1.91/0.49 % (3409103)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2671959449:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 1.91/0.49 % (3409097)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 1.91/0.49 % (3409097)Terminated due to inappropriate strategy. % 1.91/0.49 % (3409097)------------------------------ % 1.91/0.49 % (3409097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.91/0.49 % (3409097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.91/0.49 % (3409097)CaDiCaL version: 2.1.3 % 1.91/0.49 % (3409097)Termination reason: Inappropriate % 1.91/0.49 % (3409097)Time elapsed: 0.003 s % 1.91/0.49 % (3409097)Peak memory usage: 11 MB % 1.91/0.49 % (3409097)Instructions burned: 13 (million) % 1.91/0.49 % (3409097)------------------------------ % 1.91/0.49 % (3409097)------------------------------ % 1.91/0.49 % (3409121)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4012264034:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 1.91/0.49 % (3409121)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 1.91/0.49 % (3409121)Terminated due to inappropriate strategy. % 1.91/0.49 % (3409121)------------------------------ % 1.91/0.49 % (3409121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.91/0.49 % (3409121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.91/0.49 % (3409121)CaDiCaL version: 2.1.3 % 1.91/0.49 % (3409121)Termination reason: Inappropriate % 1.91/0.49 % (3409121)Time elapsed: 0.003 s % 1.91/0.49 % (3409121)Peak memory usage: 10 MB % 1.91/0.49 % (3409121)Instructions burned: 11 (million) % 1.91/0.49 % (3409121)------------------------------ % 1.91/0.49 % (3409121)------------------------------ % 1.91/0.49 % (3409132)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4226879131:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 1.91/0.49 % (3409100)Instruction limit reached! % 1.91/0.49 % (3409100)------------------------------ % 1.91/0.49 % (3409100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.91/0.49 % (3409100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.91/0.49 % (3409100)CaDiCaL version: 2.1.3 % 1.91/0.49 % (3409100)Termination reason: Instruction limit % 1.91/0.49 % (3409100)Termination phase: Saturation % 1.91/0.49 % (3409100)Time elapsed: 0.036 s % 1.91/0.49 % (3409100)Peak memory usage: 13 MB % 1.91/0.49 % (3409100)Instructions burned: 105 (million) % 1.91/0.49 % (3409101)Instruction limit reached! % 1.91/0.49 % (3409101)------------------------------ % 1.91/0.49 % (3409101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.91/0.49 % (3409101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.91/0.49 % (3409101)CaDiCaL version: 2.1.3 % 1.91/0.49 % (3409101)Termination reason: Instruction limit % 1.91/0.49 % (3409101)Termination phase: Saturation % 1.91/0.49 % (3409101)Time elapsed: 0.039 s % 1.91/0.49 % (3409101)Peak memory usage: 13 MB % 1.91/0.49 % (3409101)Instructions burned: 118 (million) % 1.91/0.49 % (3409102)Instruction limit reached! % 1.91/0.49 % (3409102)------------------------------ % 1.91/0.49 % (3409102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.91/0.49 % (3409102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.91/0.49 % (3409102)CaDiCaL version: 2.1.3 % 1.91/0.49 % (3409102)Termination reason: Instruction limit % 3.08/0.64 % (3409102)Termination phase: Saturation % 3.08/0.64 % (3409102)Time elapsed: 0.045 s % 3.08/0.64 % (3409102)Peak memory usage: 13 MB % 3.08/0.64 % (3409102)Instructions burned: 131 (million) % 3.08/0.64 % (3409146)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=2735132037:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.08/0.64 % (3409148)ott-21_1_sil=16000:fs=off:random_seed=3674908776:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.08/0.64 % (3409103)Instruction limit reached! % 3.08/0.64 % (3409103)------------------------------ % 3.08/0.64 % (3409103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.08/0.64 % (3409103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.08/0.64 % (3409103)CaDiCaL version: 2.1.3 % 3.08/0.64 % (3409103)Termination reason: Instruction limit % 3.08/0.64 % (3409103)Termination phase: Saturation % 3.08/0.64 % (3409103)Time elapsed: 0.054 s % 3.08/0.64 % (3409103)Peak memory usage: 13 MB % 3.08/0.64 % (3409103)Instructions burned: 159 (million) % 3.08/0.64 % (3409151)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3335212364:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 3.08/0.64 % (3409155)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=234841688:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi) % 3.08/0.64 % (3409155)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.08/0.64 % (3409155)Terminated due to inappropriate strategy. % 3.08/0.64 % (3409155)------------------------------ % 3.08/0.64 % (3409155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.08/0.64 % (3409155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.08/0.64 % (3409155)CaDiCaL version: 2.1.3 % 3.08/0.64 % (3409155)Termination reason: Inappropriate % 3.08/0.64 % (3409155)Time elapsed: 0.003 s % 3.08/0.64 % (3409155)Peak memory usage: 10 MB % 3.08/0.64 % (3409155)Instructions burned: 10 (million) % 3.08/0.64 % (3409155)------------------------------ % 3.08/0.64 % (3409155)------------------------------ % 3.08/0.64 % (3409132)Instruction limit reached! % 3.08/0.64 % (3409132)------------------------------ % 3.08/0.64 % (3409132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.08/0.64 % (3409132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.08/0.64 % (3409132)CaDiCaL version: 2.1.3 % 3.08/0.64 % (3409132)Termination reason: Instruction limit % 3.08/0.64 % (3409132)Termination phase: Saturation % 3.08/0.64 % (3409132)Time elapsed: 0.046 s % 3.08/0.64 % (3409132)Peak memory usage: 13 MB % 3.08/0.64 % (3409132)Instructions burned: 132 (million) % 3.08/0.64 % (3409161)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2557644092:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 3.08/0.64 % (3409162)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1094177424:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 3.08/0.64 % (3409162)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.08/0.64 % (3409162)Terminated due to inappropriate strategy. % 3.08/0.64 % (3409162)------------------------------ % 3.08/0.64 % (3409162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.08/0.64 % (3409162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.08/0.64 % (3409162)CaDiCaL version: 2.1.3 % 3.08/0.64 % (3409162)Termination reason: Inappropriate % 3.08/0.64 % (3409162)Time elapsed: 0.003 s % 3.08/0.64 % (3409162)Peak memory usage: 10 MB % 3.08/0.64 % (3409162)Instructions burned: 10 (million) % 3.08/0.64 % (3409162)------------------------------ % 3.08/0.64 % (3409162)------------------------------ % 3.08/0.64 % (3409165)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=517336835: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.64 % (3409148)Instruction limit reached! % 3.08/0.64 % (3409148)------------------------------ % 3.08/0.64 % (3409148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.08/0.64 % (3409148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.08/0.64 % (3409148)CaDiCaL version: 2.1.3 % 3.08/0.64 % (3409148)Termination reason: Instruction limit % 3.08/0.64 % (3409148)Termination phase: Saturation % 11.93/1.97 % (3409148)Time elapsed: 0.052 s % 11.93/1.97 % (3409148)Peak memory usage: 13 MB % 11.93/1.97 % (3409148)Instructions burned: 180 (million) % 11.93/1.97 % (3409167)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1850779605:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 11.93/1.97 % (3409151)Instruction limit reached! % 11.93/1.97 % (3409151)------------------------------ % 11.93/1.97 % (3409151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.93/1.97 % (3409151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.93/1.97 % (3409151)CaDiCaL version: 2.1.3 % 11.93/1.97 % (3409151)Termination reason: Instruction limit % 11.93/1.97 % (3409151)Termination phase: Saturation % 11.93/1.97 % (3409151)Time elapsed: 0.176 s % 11.93/1.97 % (3409151)Peak memory usage: 14 MB % 11.93/1.97 % (3409151)Instructions burned: 479 (million) % 11.93/1.97 % (3409146)Instruction limit reached! % 11.93/1.97 % (3409146)------------------------------ % 11.93/1.97 % (3409146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.93/1.97 % (3409146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.93/1.97 % (3409146)CaDiCaL version: 2.1.3 % 11.93/1.97 % (3409146)Termination reason: Instruction limit % 11.93/1.97 % (3409146)Termination phase: Saturation % 11.93/1.97 % (3409146)Time elapsed: 0.186 s % 11.93/1.97 % (3409146)Peak memory usage: 15 MB % 11.93/1.97 % (3409146)Instructions burned: 688 (million) % 11.93/1.97 % (3409169)fmb+10_1_sil=64000:random_seed=3383832733:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 11.93/1.97 % (3409170)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3321485099:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 11.93/1.97 % (3409169)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.93/1.97 % (3409169)Terminated due to inappropriate strategy. % 11.93/1.97 % (3409169)------------------------------ % 11.93/1.97 % (3409169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.93/1.97 % (3409169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.93/1.97 % (3409169)CaDiCaL version: 2.1.3 % 11.93/1.97 % (3409169)Termination reason: Inappropriate % 11.93/1.97 % (3409169)Time elapsed: 0.003 s % 11.93/1.97 % (3409169)Peak memory usage: 10 MB % 11.93/1.97 % (3409169)Instructions burned: 11 (million) % 11.93/1.97 % (3409169)------------------------------ % 11.93/1.97 % (3409169)------------------------------ % 11.93/1.97 % (3409170)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.93/1.97 % (3409170)Terminated due to inappropriate strategy. % 11.93/1.97 % (3409170)------------------------------ % 11.93/1.97 % (3409170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.93/1.97 % (3409170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.93/1.97 % (3409170)CaDiCaL version: 2.1.3 % 11.93/1.97 % (3409170)Termination reason: Inappropriate % 11.93/1.97 % (3409170)Time elapsed: 0.003 s % 11.93/1.97 % (3409170)Peak memory usage: 10 MB % 11.93/1.97 % (3409170)Instructions burned: 10 (million) % 11.93/1.97 % (3409170)------------------------------ % 11.93/1.97 % (3409170)------------------------------ % 11.93/1.97 % (3409173)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2853094635:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 11.93/1.97 % (3409174)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2884110513:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 11.93/1.97 % (3409173)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.93/1.97 % (3409173)Terminated due to inappropriate strategy. % 11.93/1.97 % (3409173)------------------------------ % 11.93/1.97 % (3409173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.93/1.97 % (3409173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.93/1.97 % (3409173)CaDiCaL version: 2.1.3 % 11.93/1.97 % (3409173)Termination reason: Inappropriate % 11.93/1.97 % (3409173)Time elapsed: 0.003 s % 11.93/1.97 % (3409173)Peak memory usage: 10 MB % 11.93/1.97 % (3409173)Instructions burned: 10 (million) % 11.93/1.97 % (3409173)------------------------------ % 11.93/1.97 % (3409173)------------------------------ % 11.93/1.97 % (3409177)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1636540258:i=1472:ins=7:fdi=8:gsp=on_2997 on theBenchmark for (2997ds/1472Mi) % 11.93/1.97 % (3409165)Instruction limit reached! % 11.93/1.97 % (3409165)------------------------------ % 17.40/2.88 % (3409165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.40/2.88 % (3409165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.40/2.88 % (3409165)CaDiCaL version: 2.1.3 % 17.40/2.88 % (3409165)Termination reason: Instruction limit % 17.40/2.88 % (3409165)Termination phase: Saturation % 17.40/2.88 % (3409165)Time elapsed: 0.220 s % 17.40/2.88 % (3409165)Peak memory usage: 20 MB % 17.40/2.88 % (3409165)Instructions burned: 693 (million) % 17.40/2.88 % (3409179)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=830634976:i=6324_2996 on theBenchmark for (2996ds/6324Mi) % 17.40/2.88 % (3409179)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.40/2.88 % (3409179)Terminated due to inappropriate strategy. % 17.40/2.88 % (3409179)------------------------------ % 17.40/2.88 % (3409179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.40/2.88 % (3409179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.40/2.88 % (3409179)CaDiCaL version: 2.1.3 % 17.40/2.88 % (3409179)Termination reason: Inappropriate % 17.40/2.88 % (3409179)Time elapsed: 0.004 s % 17.40/2.88 % (3409179)Peak memory usage: 11 MB % 17.40/2.88 % (3409179)Instructions burned: 12 (million) % 17.40/2.88 % (3409179)------------------------------ % 17.40/2.88 % (3409179)------------------------------ % 17.40/2.88 % (3409181)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3550773881:fmbsr=2.30978:i=2174_2996 on theBenchmark for (2996ds/2174Mi) % 17.40/2.88 % (3409181)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.40/2.88 % (3409181)Terminated due to inappropriate strategy. % 17.40/2.88 % (3409181)------------------------------ % 17.40/2.88 % (3409181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.40/2.88 % (3409181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.40/2.88 % (3409181)CaDiCaL version: 2.1.3 % 17.40/2.88 % (3409181)Termination reason: Inappropriate % 17.40/2.88 % (3409181)Time elapsed: 0.003 s % 17.40/2.88 % (3409181)Peak memory usage: 10 MB % 17.40/2.88 % (3409181)Instructions burned: 10 (million) % 17.40/2.88 % (3409181)------------------------------ % 17.40/2.88 % (3409181)------------------------------ % 17.40/2.88 % (3409183)ott-2_1_sil=16000:newcnf=on:random_seed=3087807646:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2996 on theBenchmark for (2996ds/869Mi) % 17.40/2.88 % (3409167)Instruction limit reached! % 17.40/2.88 % (3409167)------------------------------ % 17.40/2.88 % (3409167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.40/2.88 % (3409167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.40/2.88 % (3409167)CaDiCaL version: 2.1.3 % 17.40/2.88 % (3409167)Termination reason: Instruction limit % 17.40/2.88 % (3409167)Termination phase: Saturation % 17.40/2.88 % (3409167)Time elapsed: 0.269 s % 17.40/2.88 % (3409167)Peak memory usage: 19 MB % 17.40/2.88 % (3409167)Instructions burned: 883 (million) % 17.40/2.88 % (3409185)ott+10_1_sil=32000:tgt=ground:random_seed=3680695749:i=5114:av=off_2995 on theBenchmark for (2995ds/5114Mi) % 17.40/2.88 % (3409161)Instruction limit reached! % 17.40/2.88 % (3409161)------------------------------ % 17.40/2.88 % (3409161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.40/2.88 % (3409161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.40/2.88 % (3409161)CaDiCaL version: 2.1.3 % 17.40/2.88 % (3409161)Termination reason: Instruction limit % 17.40/2.88 % (3409161)Termination phase: Saturation % 17.40/2.88 % (3409161)Time elapsed: 0.378 s % 17.40/2.88 % (3409161)Peak memory usage: 21 MB % 17.40/2.88 % (3409161)Instructions burned: 1179 (million) % 17.40/2.88 % (3409187)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2064363831:i=54282_2995 on theBenchmark for (2995ds/54282Mi) % 17.40/2.88 % (3409187)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.40/2.88 % (3409187)Terminated due to inappropriate strategy. % 17.40/2.88 % (3409187)------------------------------ % 17.40/2.88 % (3409187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.40/2.88 % (3409187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.40/2.88 % (3409187)CaDiCaL version: 2.1.3 % 17.40/2.88 % (3409187)Termination reason: Inappropriate % 17.40/2.88 % (3409187)Time elapsed: 0.004 s % 17.40/2.88 % (3409187)Peak memory usage: 11 MB % 17.40/2.88 % (3409187)Instructions burned: 13 (million) % 72.23/10.42 % (3409187)------------------------------ % 72.23/10.42 % (3409187)------------------------------ % 72.23/10.42 % (3409189)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=617190414:i=3512:aac=none_2994 on theBenchmark for (2994ds/3512Mi) % 72.23/10.42 % (3409183)Instruction limit reached! % 72.23/10.42 % (3409183)------------------------------ % 72.23/10.42 % (3409183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.23/10.42 % (3409183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.23/10.42 % (3409183)CaDiCaL version: 2.1.3 % 72.23/10.42 % (3409183)Termination reason: Instruction limit % 72.23/10.42 % (3409183)Termination phase: Saturation % 72.23/10.42 % (3409183)Time elapsed: 0.286 s % 72.23/10.42 % (3409183)Peak memory usage: 16 MB % 72.23/10.42 % (3409183)Instructions burned: 871 (million) % 72.23/10.42 % (3409191)dis+21_1_sil=32000:sas=cadical:random_seed=3240904178:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi) % 72.23/10.42 % (3409177)Instruction limit reached! % 72.23/10.42 % (3409177)------------------------------ % 72.23/10.42 % (3409177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.23/10.42 % (3409177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.23/10.42 % (3409177)CaDiCaL version: 2.1.3 % 72.23/10.42 % (3409177)Termination reason: Instruction limit % 72.23/10.42 % (3409177)Termination phase: Saturation % 72.23/10.42 % (3409177)Time elapsed: 0.468 s % 72.23/10.42 % (3409177)Peak memory usage: 29 MB % 72.23/10.42 % (3409177)Instructions burned: 1474 (million) % 72.23/10.42 % (3409193)ott+11_1_sil=16000:gs=on:random_seed=2656481012:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2992 on theBenchmark for (2992ds/2251Mi) % 72.23/10.42 % (3409193)Instruction limit reached! % 72.23/10.42 % (3409193)------------------------------ % 72.23/10.42 % (3409193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.23/10.42 % (3409193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.23/10.42 % (3409193)CaDiCaL version: 2.1.3 % 72.23/10.42 % (3409193)Termination reason: Instruction limit % 72.23/10.42 % (3409193)Termination phase: Saturation % 72.23/10.42 % (3409193)Time elapsed: 0.758 s % 72.23/10.42 % (3409193)Peak memory usage: 24 MB % 72.23/10.42 % (3409193)Instructions burned: 2254 (million) % 72.23/10.42 % (3409195)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=406288051:fmbsr=1.6:i=67534_2984 on theBenchmark for (2984ds/67534Mi) % 72.23/10.42 % (3409195)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 72.23/10.42 % (3409195)Terminated due to inappropriate strategy. % 72.23/10.42 % (3409195)------------------------------ % 72.23/10.42 % (3409195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.23/10.42 % (3409195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.23/10.42 % (3409195)CaDiCaL version: 2.1.3 % 72.23/10.42 % (3409195)Termination reason: Inappropriate % 72.23/10.42 % (3409195)Time elapsed: 0.003 s % 72.23/10.42 % (3409195)Peak memory usage: 10 MB % 72.23/10.42 % (3409195)Instructions burned: 11 (million) % 72.23/10.42 % (3409195)------------------------------ % 72.23/10.42 % (3409195)------------------------------ % 72.23/10.42 % (3409197)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=165565483:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2984 on theBenchmark for (2984ds/4591Mi) % 72.23/10.42 % (3409189)Instruction limit reached! % 72.23/10.42 % (3409189)------------------------------ % 72.23/10.42 % (3409189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.23/10.42 % (3409189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.23/10.42 % (3409189)CaDiCaL version: 2.1.3 % 72.23/10.42 % (3409189)Termination reason: Instruction limit % 72.23/10.42 % (3409189)Termination phase: Saturation % 72.23/10.42 % (3409189)Time elapsed: 1.084 s % 72.23/10.42 % (3409189)Peak memory usage: 28 MB % 72.23/10.42 % (3409189)Instructions burned: 3512 (million) % 72.23/10.42 % (3409199)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2330029989:i=29340_2983 on theBenchmark for (2983ds/29340Mi) % 72.23/10.42 % (3409174)Instruction limit reached! % 72.23/10.42 % (3409174)------------------------------ % 72.23/10.42 % (3409174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.23/10.42 % (3409174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.23/10.42 % (3409174)CaDiCaL version: 2.1.3 % 72.23/10.42 % (3409174)Termination reason: Instruction limit % 74.12/10.82 % (3409174)Termination phase: Saturation % 74.12/10.82 % (3409174)Time elapsed: 1.542 s % 74.12/10.82 % (3409174)Peak memory usage: 32 MB % 74.12/10.82 % (3409174)Instructions burned: 5131 (million) % 74.12/10.82 % (3409201)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4137247771:i=5211_2981 on theBenchmark for (2981ds/5211Mi) % 74.12/10.82 % (3409191)Instruction limit reached! % 74.12/10.82 % (3409191)------------------------------ % 74.12/10.82 % (3409191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.12/10.82 % (3409191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.12/10.82 % (3409191)CaDiCaL version: 2.1.3 % 74.12/10.82 % (3409191)Termination reason: Instruction limit % 74.12/10.82 % (3409191)Termination phase: Saturation % 74.12/10.82 % (3409191)Time elapsed: 1.178 s % 74.12/10.82 % (3409191)Peak memory usage: 32 MB % 74.12/10.82 % (3409191)Instructions burned: 3775 (million) % 74.12/10.82 % (3409203)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3031158493:i=5497:nm=2_2981 on theBenchmark for (2981ds/5497Mi) % 74.12/10.82 % (3409203)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 74.12/10.82 % (3409203)Terminated due to inappropriate strategy. % 74.12/10.82 % (3409203)------------------------------ % 74.12/10.82 % (3409203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.12/10.82 % (3409203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.12/10.82 % (3409203)CaDiCaL version: 2.1.3 % 74.12/10.82 % (3409203)Termination reason: Inappropriate % 74.12/10.82 % (3409203)Time elapsed: 0.004 s % 74.12/10.82 % (3409203)Peak memory usage: 11 MB % 74.12/10.82 % (3409203)Instructions burned: 13 (million) % 74.12/10.82 % (3409203)------------------------------ % 74.12/10.82 % (3409203)------------------------------ % 74.12/10.82 % (3409205)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1887518911:fmbsr=2:i=46332_2981 on theBenchmark for (2981ds/46332Mi) % 74.12/10.82 % (3409205)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 74.12/10.82 % (3409205)Terminated due to inappropriate strategy. % 74.12/10.82 % (3409205)------------------------------ % 74.12/10.82 % (3409205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.12/10.82 % (3409205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.12/10.82 % (3409205)CaDiCaL version: 2.1.3 % 74.12/10.82 % (3409205)Termination reason: Inappropriate % 74.12/10.82 % (3409205)Time elapsed: 0.003 s % 74.12/10.82 % (3409205)Peak memory usage: 11 MB % 74.12/10.82 % (3409205)Instructions burned: 11 (million) % 74.12/10.82 % (3409205)------------------------------ % 74.12/10.82 % (3409205)------------------------------ % 74.12/10.82 % (3409207)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=97581704:i=14071_2980 on theBenchmark for (2980ds/14071Mi) % 74.12/10.82 % (3409207)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 74.12/10.82 % (3409207)Terminated due to inappropriate strategy. % 74.12/10.82 % (3409207)------------------------------ % 74.12/10.82 % (3409207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.12/10.82 % (3409207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.12/10.82 % (3409207)CaDiCaL version: 2.1.3 % 74.12/10.82 % (3409207)Termination reason: Inappropriate % 74.12/10.82 % (3409207)Time elapsed: 0.003 s % 74.12/10.82 % (3409207)Peak memory usage: 11 MB % 74.12/10.82 % (3409207)Instructions burned: 11 (million) % 74.12/10.82 % (3409207)------------------------------ % 74.12/10.82 % (3409207)------------------------------ % 74.12/10.82 % (3409209)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2105431225:i=22565:add=on:rawr=on_2980 on theBenchmark for (2980ds/22565Mi) % 74.12/10.82 % (3409185)Instruction limit reached! % 74.12/10.82 % (3409185)------------------------------ % 74.12/10.82 % (3409185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.12/10.82 % (3409185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.12/10.82 % (3409185)CaDiCaL version: 2.1.3 % 74.12/10.82 % (3409185)Termination reason: Instruction limit % 74.12/10.82 % (3409185)Termination phase: Saturation % 74.12/10.82 % (3409185)Time elapsed: 1.727 s % 74.12/10.82 % (3409185)Peak memory usage: 46 MB % 74.12/10.82 % (3409185)Instructions burned: 5116 (million) % 74.12/10.82 % (3409211)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2961534208:i=8173:av=off_2978 on theBenchmark for (2978ds/8173Mi) % 74.12/10.82 % (3409197)Instruction limit reached! % 74.50/10.90 % (3409197)------------------------------ % 74.50/10.90 % (3409197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.50/10.90 % (3409197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.50/10.90 % (3409197)CaDiCaL version: 2.1.3 % 74.50/10.90 % (3409197)Termination reason: Instruction limit % 74.50/10.90 % (3409197)Termination phase: Saturation % 74.50/10.90 % (3409197)Time elapsed: 1.171 s % 74.50/10.90 % (3409197)Peak memory usage: 38 MB % 74.50/10.90 % (3409197)Instructions burned: 4594 (million) % 74.50/10.90 % (3409213)dis+10_16:1_sil=16000:random_seed=1083263415:i=9155:fsr=off_2972 on theBenchmark for (2972ds/9155Mi) % 74.50/10.90 % (3409201)Instruction limit reached! % 74.50/10.90 % (3409201)------------------------------ % 74.50/10.90 % (3409201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.50/10.90 % (3409201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.50/10.90 % (3409201)CaDiCaL version: 2.1.3 % 74.50/10.90 % (3409201)Termination reason: Instruction limit % 74.50/10.90 % (3409201)Termination phase: Saturation % 74.50/10.90 % (3409201)Time elapsed: 1.443 s % 74.50/10.90 % (3409201)Peak memory usage: 45 MB % 74.50/10.90 % (3409201)Instructions burned: 5214 (million) % 74.50/10.90 % (3409215)ott-3_8_sil=64000:random_seed=1944844626:i=20139:bs=on_2967 on theBenchmark for (2967ds/20139Mi) % 74.50/10.90 % (3409211)Instruction limit reached! % 74.50/10.90 % (3409211)------------------------------ % 74.50/10.90 % (3409211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.50/10.90 % (3409211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.50/10.90 % (3409211)CaDiCaL version: 2.1.3 % 74.50/10.90 % (3409211)Termination reason: Instruction limit % 74.50/10.90 % (3409211)Termination phase: Saturation % 74.50/10.90 % (3409211)Time elapsed: 2.997 s % 74.50/10.90 % (3409211)Peak memory usage: 84 MB % 74.50/10.90 % (3409211)Instructions burned: 8173 (million) % 74.50/10.90 % (3409217)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2885782122:fmbsr=2:i=32576_2948 on theBenchmark for (2948ds/32576Mi) % 74.50/10.90 % (3409217)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 74.50/10.90 % (3409217)Terminated due to inappropriate strategy. % 74.50/10.90 % (3409217)------------------------------ % 74.50/10.90 % (3409217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.50/10.90 % (3409217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.50/10.90 % (3409217)CaDiCaL version: 2.1.3 % 74.50/10.90 % (3409217)Termination reason: Inappropriate % 74.50/10.90 % (3409217)Time elapsed: 0.004 s % 74.50/10.90 % (3409217)Peak memory usage: 11 MB % 74.50/10.90 % (3409217)Instructions burned: 13 (million) % 74.50/10.90 % (3409217)------------------------------ % 74.50/10.90 % (3409217)------------------------------ % 74.50/10.90 % (3409219)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2137131243:i=11404_2948 on theBenchmark for (2948ds/11404Mi) % 74.50/10.90 % (3409213)Instruction limit reached! % 74.50/10.90 % (3409213)------------------------------ % 74.50/10.90 % (3409213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.50/10.90 % (3409213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.50/10.90 % (3409213)CaDiCaL version: 2.1.3 % 74.50/10.90 % (3409213)Termination reason: Instruction limit % 74.50/10.90 % (3409213)Termination phase: Saturation % 74.50/10.90 % (3409213)Time elapsed: 2.664 s % 74.50/10.90 % (3409213)Peak memory usage: 58 MB % 74.50/10.90 % (3409213)Instructions burned: 9156 (million) % 74.50/10.90 % (3409221)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=805181702:i=14134_2945 on theBenchmark for (2945ds/14134Mi) % 74.50/10.90 % (3409219)Instruction limit reached! % 74.50/10.90 % (3409219)------------------------------ % 74.50/10.90 % (3409219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.50/10.90 % (3409219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.50/10.90 % (3409219)CaDiCaL version: 2.1.3 % 74.50/10.90 % (3409219)Termination reason: Instruction limit % 74.50/10.90 % (3409219)Termination phase: Saturation % 74.50/10.90 % (3409219)Time elapsed: 4.115 s % 74.50/10.90 % (3409219)Peak memory usage: 80 MB % 74.50/10.90 % (3409219)Instructions burned: 11405 (million) % 74.50/10.90 % (3409223)dis+33_16_sil=32000:sac=on:random_seed=4060310241:i=15851:nm=0_2906 on theBenchmark for (2906ds/15851Mi) % 74.50/10.90 % (3409199)Instruction limit reached! % 74.50/10.90 % (3409199)------------------------------ % 74.50/10.90 % (3409199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.23/14.89 % (3409199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.23/14.89 % (3409199)CaDiCaL version: 2.1.3 % 103.23/14.89 % (3409199)Termination reason: Instruction limit % 103.23/14.89 % (3409199)Termination phase: Saturation % 103.23/14.89 % (3409199)Time elapsed: 8.665 s % 103.23/14.89 % (3409199)Peak memory usage: 276 MB % 103.23/14.89 % (3409199)Instructions burned: 29342 (million) % 103.23/14.89 % (3409209)Instruction limit reached! % 103.23/14.89 % (3409209)------------------------------ % 103.23/14.89 % (3409209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.23/14.89 % (3409209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.23/14.89 % (3409209)CaDiCaL version: 2.1.3 % 103.23/14.89 % (3409209)Termination reason: Instruction limit % 103.23/14.89 % (3409209)Termination phase: Saturation % 103.23/14.89 % (3409209)Time elapsed: 8.367 s % 103.23/14.89 % (3409209)Peak memory usage: 109 MB % 103.23/14.89 % (3409209)Instructions burned: 22565 (million) % 103.23/14.89 % (3409225)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2006128924:avsq=on:i=17627:add=on:amm=off_2896 on theBenchmark for (2896ds/17627Mi) % 103.23/14.89 % (3409226)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3639354638:s2a=on:i=53295_2896 on theBenchmark for (2896ds/53295Mi) % 103.23/14.89 % (3409221)Instruction limit reached! % 103.23/14.89 % (3409221)------------------------------ % 103.23/14.89 % (3409221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.23/14.89 % (3409221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.23/14.89 % (3409221)CaDiCaL version: 2.1.3 % 103.23/14.89 % (3409221)Termination reason: Instruction limit % 103.23/14.89 % (3409221)Termination phase: Saturation % 103.23/14.89 % (3409221)Time elapsed: 4.923 s % 103.23/14.89 % (3409221)Peak memory usage: 82 MB % 103.23/14.89 % (3409221)Instructions burned: 14136 (million) % 103.23/14.89 % (3409229)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=206164347:i=26857:ins=20_2896 on theBenchmark for (2896ds/26857Mi) % 103.23/14.89 % (3409229)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 103.23/14.89 % (3409229)Terminated due to inappropriate strategy. % 103.23/14.89 % (3409229)------------------------------ % 103.23/14.89 % (3409229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.23/14.89 % (3409229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.23/14.89 % (3409229)CaDiCaL version: 2.1.3 % 103.23/14.89 % (3409229)Termination reason: Inappropriate % 103.23/14.89 % (3409229)Time elapsed: 0.003 s % 103.23/14.89 % (3409229)Peak memory usage: 10 MB % 103.23/14.89 % (3409229)Instructions burned: 10 (million) % 103.23/14.89 % (3409229)------------------------------ % 103.23/14.89 % (3409229)------------------------------ % 103.23/14.89 % (3409231)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1553657215:i=28120:bs=on:fsr=off_2896 on theBenchmark for (2896ds/28120Mi) % 103.23/14.89 % (3409215)Instruction limit reached! % 103.23/14.89 % (3409215)------------------------------ % 103.23/14.89 % (3409215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.23/14.89 % (3409215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.23/14.89 % (3409215)CaDiCaL version: 2.1.3 % 103.23/14.89 % (3409215)Termination reason: Instruction limit % 103.23/14.89 % (3409215)Termination phase: Saturation % 103.23/14.89 % (3409215)Time elapsed: 7.341 s % 103.23/14.89 % (3409215)Peak memory usage: 107 MB % 103.23/14.89 % (3409215)Instructions burned: 20141 (million) % 103.23/14.89 % (3409233)fmb+10_1_sil=256000:fmbss=7:random_seed=80871350:fmbsr=1.6:i=182295_2893 on theBenchmark for (2893ds/182295Mi) % 103.23/14.89 % (3409233)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 103.23/14.89 % (3409233)Terminated due to inappropriate strategy. % 103.23/14.89 % (3409233)------------------------------ % 103.23/14.89 % (3409233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.23/14.89 % (3409233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.23/14.89 % (3409233)CaDiCaL version: 2.1.3 % 103.23/14.89 % (3409233)Termination reason: Inappropriate % 103.23/14.89 % (3409233)Time elapsed: 0.003 s % 103.23/14.89 % (3409233)Peak memory usage: 10 MB % 103.23/14.89 % (3409233)Instructions burned: 10 (million) % 103.23/14.89 % (3409233)------------------------------ % 103.23/14.89 % (3409233)------------------------------ % 103.23/14.89 % (3409235)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1978140980:i=44625:gsp=on_2893 on theBenchmark for (2893ds/44625Mi) % 111.93/16.10 % (3409235)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.93/16.10 % (3409235)Terminated due to inappropriate strategy. % 111.93/16.10 % (3409235)------------------------------ % 111.93/16.10 % (3409235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.93/16.10 % (3409235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.93/16.10 % (3409235)CaDiCaL version: 2.1.3 % 111.93/16.10 % (3409235)Termination reason: Inappropriate % 111.93/16.10 % (3409235)Time elapsed: 0.003 s % 111.93/16.10 % (3409235)Peak memory usage: 11 MB % 111.93/16.10 % (3409235)Instructions burned: 11 (million) % 111.93/16.10 % (3409235)------------------------------ % 111.93/16.10 % (3409235)------------------------------ % 111.93/16.10 % (3409237)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1088228410:i=160505_2893 on theBenchmark for (2893ds/160505Mi) % 111.93/16.10 % (3409237)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.93/16.10 % (3409237)Terminated due to inappropriate strategy. % 111.93/16.10 % (3409237)------------------------------ % 111.93/16.10 % (3409237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.93/16.10 % (3409237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.93/16.10 % (3409237)CaDiCaL version: 2.1.3 % 111.93/16.10 % (3409237)Termination reason: Inappropriate % 111.93/16.10 % (3409237)Time elapsed: 0.003 s % 111.93/16.10 % (3409237)Peak memory usage: 11 MB % 111.93/16.10 % (3409237)Instructions burned: 10 (million) % 111.93/16.10 % (3409237)------------------------------ % 111.93/16.10 % (3409237)------------------------------ % 111.93/16.10 % (3409239)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1682011207:fmbsr=1.3:i=225729_2892 on theBenchmark for (2892ds/225729Mi) % 111.93/16.10 % (3409239)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.93/16.10 % (3409239)Terminated due to inappropriate strategy. % 111.93/16.10 % (3409239)------------------------------ % 111.93/16.10 % (3409239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.93/16.10 % (3409239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.93/16.10 % (3409239)CaDiCaL version: 2.1.3 % 111.93/16.10 % (3409239)Termination reason: Inappropriate % 111.93/16.10 % (3409239)Time elapsed: 0.003 s % 111.93/16.10 % (3409239)Peak memory usage: 11 MB % 111.93/16.10 % (3409239)Instructions burned: 11 (million) % 111.93/16.10 % (3409239)------------------------------ % 111.93/16.10 % (3409239)------------------------------ % 111.93/16.10 % (3409241)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=306265031:fmbsr=2:i=185024:ins=7_2892 on theBenchmark for (2892ds/185024Mi) % 111.93/16.10 % (3409241)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.93/16.10 % (3409241)Terminated due to inappropriate strategy. % 111.93/16.10 % (3409241)------------------------------ % 111.93/16.10 % (3409241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.93/16.10 % (3409241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.93/16.10 % (3409241)CaDiCaL version: 2.1.3 % 111.93/16.10 % (3409241)Termination reason: Inappropriate % 111.93/16.10 % (3409241)Time elapsed: 0.003 s % 111.93/16.10 % (3409241)Peak memory usage: 11 MB % 111.93/16.10 % (3409241)Instructions burned: 11 (million) % 111.93/16.10 % (3409241)------------------------------ % 111.93/16.10 % (3409241)------------------------------ % 111.93/16.10 % (3409243)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1845435865:rtra=on_2892 on theBenchmark for (2892ds/0Mi) % 111.93/16.10 % (3409243)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.93/16.10 % (3409243)Terminated due to inappropriate strategy. % 111.93/16.10 % (3409243)------------------------------ % 111.93/16.10 % (3409243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.93/16.10 % (3409243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.93/16.10 % (3409243)CaDiCaL version: 2.1.3 % 111.93/16.10 % (3409243)Termination reason: Inappropriate % 111.93/16.10 % (3409243)Time elapsed: 0.004 s % 111.93/16.10 % (3409243)Peak memory usage: 11 MB % 111.93/16.10 % (3409243)Instructions burned: 13 (million) % 111.93/16.10 % (3409243)------------------------------ % 111.93/16.10 % (3409243)------------------------------ % 111.93/16.10 % (3409245)% WARNING: option uhcvi not known. % 111.93/16.10 % (3409245)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3816532187:i=271062:add=off:rtra=on:rawr=on_2892 on theBenchmark for (2892ds/271062Mi) % 133.03/19.02 % (3409225)Instruction limit reached! % 133.03/19.02 % (3409225)------------------------------ % 133.03/19.02 % (3409225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.03/19.02 % (3409225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.03/19.02 % (3409225)CaDiCaL version: 2.1.3 % 133.03/19.02 % (3409225)Termination reason: Instruction limit % 133.03/19.02 % (3409225)Termination phase: Saturation % 133.03/19.02 % (3409225)Time elapsed: 2.840 s % 133.03/19.02 % (3409225)Peak memory usage: 36 MB % 133.03/19.02 % (3409225)Instructions burned: 17635 (million) % 133.03/19.02 % (3409247)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2481517790:i=176048:add=on:rtra=on:rawr=on_2868 on theBenchmark for (2868ds/176048Mi) % 133.03/19.02 % (3409223)Instruction limit reached! % 133.03/19.02 % (3409223)------------------------------ % 133.03/19.02 % (3409223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.03/19.02 % (3409223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.03/19.02 % (3409223)CaDiCaL version: 2.1.3 % 133.03/19.02 % (3409223)Termination reason: Instruction limit % 133.03/19.02 % (3409223)Termination phase: Saturation % 133.03/19.02 % (3409223)Time elapsed: 4.984 s % 133.03/19.02 % (3409223)Peak memory usage: 129 MB % 133.03/19.02 % (3409223)Instructions burned: 15852 (million) % 133.03/19.02 % (3409381)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3186720154:i=206:fgj=on:rtra=on_2856 on theBenchmark for (2856ds/206Mi) % 133.03/19.02 % (3409381)Instruction limit reached! % 133.03/19.02 % (3409381)------------------------------ % 133.03/19.02 % (3409381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.03/19.02 % (3409381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.03/19.02 % (3409381)CaDiCaL version: 2.1.3 % 133.03/19.02 % (3409381)Termination reason: Instruction limit % 133.03/19.02 % (3409381)Termination phase: Saturation % 133.03/19.02 % (3409381)Time elapsed: 0.075 s % 133.03/19.02 % (3409381)Peak memory usage: 13 MB % 133.03/19.02 % (3409381)Instructions burned: 208 (million) % 133.03/19.02 % (3409383)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3876895957:i=232:rtra=on_2855 on theBenchmark for (2855ds/232Mi) % 133.03/19.02 % (3409383)Instruction limit reached! % 133.03/19.02 % (3409383)------------------------------ % 133.03/19.02 % (3409383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.03/19.02 % (3409383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.03/19.02 % (3409383)CaDiCaL version: 2.1.3 % 133.03/19.02 % (3409383)Termination reason: Instruction limit % 133.03/19.02 % (3409383)Termination phase: Saturation % 133.03/19.02 % (3409383)Time elapsed: 0.080 s % 133.03/19.02 % (3409383)Peak memory usage: 14 MB % 133.03/19.02 % (3409383)Instructions burned: 233 (million) % 133.03/19.02 % (3409385)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=4062858459:i=262:rtra=on_2854 on theBenchmark for (2854ds/262Mi) % 133.03/19.02 % (3409385)Instruction limit reached! % 133.03/19.02 % (3409385)------------------------------ % 133.03/19.02 % (3409385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.03/19.02 % (3409385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.03/19.02 % (3409385)CaDiCaL version: 2.1.3 % 133.03/19.02 % (3409385)Termination reason: Instruction limit % 133.03/19.02 % (3409385)Termination phase: Saturation % 133.03/19.02 % (3409385)Time elapsed: 0.090 s % 133.03/19.02 % (3409385)Peak memory usage: 14 MB % 133.03/19.02 % (3409385)Instructions burned: 264 (million) % 133.03/19.02 % (3409387)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=385172750:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2853 on theBenchmark for (2853ds/318Mi) % 133.03/19.02 % (3409387)Instruction limit reached! % 133.03/19.02 % (3409387)------------------------------ % 133.03/19.02 % (3409387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.03/19.02 % (3409387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.03/19.02 % (3409387)CaDiCaL version: 2.1.3 % 133.03/19.02 % (3409387)Termination reason: Instruction limit % 133.03/19.02 % (3409387)Termination phase: Saturation % 133.03/19.02 % (3409387)Time elapsed: 0.109 s % 133.03/19.02 % (3409387)Peak memory usage: 15 MB % 133.03/19.02 % (3409387)Instructions burned: 318 (million) % 133.03/19.02 % (3409425)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=284786949:i=1428:nm=2:rtra=on_2852 on theBenchmark for (2852ds/1428Mi) % 165.38/23.61 % (3409425)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 165.38/23.61 % (3409425)Terminated due to inappropriate strategy. % 165.38/23.61 % (3409425)------------------------------ % 165.38/23.61 % (3409425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.38/23.61 % (3409425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.38/23.61 % (3409425)CaDiCaL version: 2.1.3 % 165.38/23.61 % (3409425)Termination reason: Inappropriate % 165.38/23.61 % (3409425)Time elapsed: 0.003 s % 165.38/23.61 % (3409425)Peak memory usage: 10 MB % 165.38/23.61 % (3409425)Instructions burned: 11 (million) % 165.38/23.61 % (3409425)------------------------------ % 165.38/23.61 % (3409425)------------------------------ % 165.38/23.61 % (3409435)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=109412473:i=262:bd=preordered:rtra=on:fsd=on_2852 on theBenchmark for (2852ds/262Mi) % 165.38/23.61 % (3409435)Instruction limit reached! % 165.38/23.61 % (3409435)------------------------------ % 165.38/23.61 % (3409435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.38/23.61 % (3409435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.38/23.61 % (3409435)CaDiCaL version: 2.1.3 % 165.38/23.61 % (3409435)Termination reason: Instruction limit % 165.38/23.61 % (3409435)Termination phase: Saturation % 165.38/23.61 % (3409435)Time elapsed: 0.098 s % 165.38/23.61 % (3409435)Peak memory usage: 14 MB % 165.38/23.61 % (3409435)Instructions burned: 262 (million) % 165.38/23.61 % (3409478)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=3558925361:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2851 on theBenchmark for (2851ds/1368Mi) % 165.38/23.61 % (3409478)Instruction limit reached! % 165.38/23.61 % (3409478)------------------------------ % 165.38/23.61 % (3409478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.38/23.61 % (3409478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.38/23.61 % (3409478)CaDiCaL version: 2.1.3 % 165.38/23.61 % (3409478)Termination reason: Instruction limit % 165.38/23.61 % (3409478)Termination phase: Saturation % 165.38/23.61 % (3409478)Time elapsed: 0.373 s % 165.38/23.61 % (3409478)Peak memory usage: 19 MB % 165.38/23.61 % (3409478)Instructions burned: 1371 (million) % 165.38/23.61 % (3409525)ott-21_1_sil=16000:si=on:fs=off:random_seed=1769041265:i=360:av=off:fsr=off:rtra=on_2847 on theBenchmark for (2847ds/360Mi) % 165.38/23.61 % (3409525)Instruction limit reached! % 165.38/23.61 % (3409525)------------------------------ % 165.38/23.61 % (3409525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.38/23.61 % (3409525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.38/23.61 % (3409525)CaDiCaL version: 2.1.3 % 165.38/23.61 % (3409525)Termination reason: Instruction limit % 165.38/23.61 % (3409525)Termination phase: Saturation % 165.38/23.61 % (3409525)Time elapsed: 0.106 s % 165.38/23.61 % (3409525)Peak memory usage: 14 MB % 165.38/23.61 % (3409525)Instructions burned: 361 (million) % 165.38/23.61 % (3409535)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1491131264:i=954:bd=all:rtra=on_2846 on theBenchmark for (2846ds/954Mi) % 165.38/23.61 % (3409535)Instruction limit reached! % 165.38/23.61 % (3409535)------------------------------ % 165.38/23.61 % (3409535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.38/23.61 % (3409535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.38/23.61 % (3409535)CaDiCaL version: 2.1.3 % 165.38/23.61 % (3409535)Termination reason: Instruction limit % 165.38/23.61 % (3409535)Termination phase: Saturation % 165.38/23.61 % (3409535)Time elapsed: 0.518 s % 165.38/23.61 % (3409535)Peak memory usage: 16 MB % 165.38/23.61 % (3409535)Instructions burned: 956 (million) % 165.38/23.61 % (3409569)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=4090197878:fmbsr=1.3:i=1730:ins=25:rtra=on_2840 on theBenchmark for (2840ds/1730Mi) % 165.38/23.61 % (3409569)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 165.38/23.61 % (3409569)Terminated due to inappropriate strategy. % 165.38/23.61 % (3409569)------------------------------ % 165.38/23.61 % (3409569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.38/23.61 % (3409569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.38/23.61 % (3409569)CaDiCaL version: 2.1.3 % 165.38/23.61 % (3409569)Termination reason: Inappropriate % 186.54/26.64 % (3409569)Time elapsed: 0.003 s % 186.54/26.64 % (3409569)Peak memory usage: 10 MB % 186.54/26.64 % (3409569)Instructions burned: 11 (million) % 186.54/26.64 % (3409569)------------------------------ % 186.54/26.64 % (3409569)------------------------------ % 186.54/26.64 % (3409574)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=249554569:i=2358:rtra=on_2840 on theBenchmark for (2840ds/2358Mi) % 186.54/26.64 % (3409574)Instruction limit reached! % 186.54/26.64 % (3409574)------------------------------ % 186.54/26.64 % (3409574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.54/26.64 % (3409574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.54/26.64 % (3409574)CaDiCaL version: 2.1.3 % 186.54/26.64 % (3409574)Termination reason: Instruction limit % 186.54/26.64 % (3409574)Termination phase: Saturation % 186.54/26.64 % (3409574)Time elapsed: 1.148 s % 186.54/26.64 % (3409574)Peak memory usage: 27 MB % 186.54/26.64 % (3409574)Instructions burned: 2358 (million) % 186.54/26.64 % (3409636)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1584222128:i=1778:ins=1:rtra=on_2828 on theBenchmark for (2828ds/1778Mi) % 186.54/26.64 % (3409636)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 186.54/26.64 % (3409636)Terminated due to inappropriate strategy. % 186.54/26.64 % (3409636)------------------------------ % 186.54/26.64 % (3409636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.54/26.64 % (3409636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.54/26.64 % (3409636)CaDiCaL version: 2.1.3 % 186.54/26.64 % (3409636)Termination reason: Inappropriate % 186.54/26.64 % (3409636)Time elapsed: 0.005 s % 186.54/26.64 % (3409636)Peak memory usage: 10 MB % 186.54/26.64 % (3409636)Instructions burned: 11 (million) % 186.54/26.64 % (3409636)------------------------------ % 186.54/26.64 % (3409636)------------------------------ % 186.54/26.64 % (3409639)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=1612933384:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2828 on theBenchmark for (2828ds/1384Mi) % 186.54/26.64 % (3409639)Instruction limit reached! % 186.54/26.64 % (3409639)------------------------------ % 186.54/26.64 % (3409639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.54/26.64 % (3409639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.54/26.64 % (3409639)CaDiCaL version: 2.1.3 % 186.54/26.64 % (3409639)Termination reason: Instruction limit % 186.54/26.64 % (3409639)Termination phase: Saturation % 186.54/26.64 % (3409639)Time elapsed: 0.781 s % 186.54/26.64 % (3409639)Peak memory usage: 25 MB % 186.54/26.64 % (3409639)Instructions burned: 1386 (million) % 186.54/26.64 % (3409672)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1257431375:i=1758:kws=inv_precedence:fsr=off:rtra=on_2820 on theBenchmark for (2820ds/1758Mi) % 186.54/26.64 % (3409672)Instruction limit reached! % 186.54/26.64 % (3409672)------------------------------ % 186.54/26.64 % (3409672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.54/26.64 % (3409672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.54/26.64 % (3409672)CaDiCaL version: 2.1.3 % 186.54/26.64 % (3409672)Termination reason: Instruction limit % 186.54/26.64 % (3409672)Termination phase: Saturation % 186.54/26.64 % (3409672)Time elapsed: 0.782 s % 186.54/26.64 % (3409672)Peak memory usage: 23 MB % 186.54/26.64 % (3409672)Instructions burned: 1760 (million) % 186.54/26.64 % (3409698)fmb+10_1_sil=64000:si=on:random_seed=1905894814:i=44122:nm=2:rtra=on:gsp=on_2811 on theBenchmark for (2811ds/44122Mi) % 186.54/26.64 % (3409698)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 186.54/26.64 % (3409698)Terminated due to inappropriate strategy. % 186.54/26.64 % (3409698)------------------------------ % 186.54/26.64 % (3409698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.54/26.64 % (3409698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.54/26.64 % (3409698)CaDiCaL version: 2.1.3 % 186.54/26.64 % (3409698)Termination reason: Inappropriate % 186.54/26.64 % (3409698)Time elapsed: 0.007 s % 186.54/26.64 % (3409698)Peak memory usage: 10 MB % 186.54/26.64 % (3409698)Instructions burned: 12 (million) % 186.54/26.64 % (3409698)------------------------------ % 186.54/26.64 % (3409698)------------------------------ % 186.54/26.64 % (3409702)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2405626292:i=19030:nm=5:rtra=on_2811 on theBenchmark for (2811ds/19030Mi) % 185.50/29.14 % (3409702)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.50/29.14 % (3409702)Terminated due to inappropriate strategy. % 185.50/29.14 % (3409702)------------------------------ % 185.50/29.14 % (3409702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.50/29.14 % (3409702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.50/29.14 % (3409702)CaDiCaL version: 2.1.3 % 185.50/29.14 % (3409702)Termination reason: Inappropriate % 185.50/29.14 % (3409702)Time elapsed: 0.006 s % 185.50/29.14 % (3409702)Peak memory usage: 10 MB % 185.50/29.14 % (3409702)Instructions burned: 11 (million) % 185.50/29.14 % (3409702)------------------------------ % 185.50/29.14 % (3409702)------------------------------ % 185.50/29.14 % (3409705)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2495497695:fmbsr=1.7:i=1840:rtra=on_2811 on theBenchmark for (2811ds/1840Mi) % 185.50/29.14 % (3409705)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.50/29.14 % (3409705)Terminated due to inappropriate strategy. % 185.50/29.14 % (3409705)------------------------------ % 185.50/29.14 % (3409705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.50/29.14 % (3409705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.50/29.14 % (3409705)CaDiCaL version: 2.1.3 % 185.50/29.14 % (3409705)Termination reason: Inappropriate % 185.50/29.14 % (3409705)Time elapsed: 0.004 s % 185.50/29.14 % (3409705)Peak memory usage: 11 MB % 185.50/29.14 % (3409705)Instructions burned: 11 (million) % 185.50/29.14 % (3409705)------------------------------ % 185.50/29.14 % (3409705)------------------------------ % 185.50/29.14 % (3409709)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2920288419:i=10262:rtra=on_2810 on theBenchmark for (2810ds/10262Mi) % 185.50/29.14 % (3409231)Instruction limit reached! % 185.50/29.14 % (3409231)------------------------------ % 185.50/29.14 % (3409231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.50/29.14 % (3409231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.50/29.14 % (3409231)CaDiCaL version: 2.1.3 % 185.50/29.14 % (3409231)Termination reason: Instruction limit % 185.50/29.14 % (3409231)Termination phase: Saturation % 185.50/29.14 % (3409231)Time elapsed: 11.797 s % 185.50/29.14 % (3409231)Peak memory usage: 106 MB % 185.50/29.14 % (3409231)Instructions burned: 28120 (million) % 185.50/29.14 % (3409763)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2513860833:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2777 on theBenchmark for (2777ds/2944Mi) % 185.50/29.14 % (3409763)Instruction limit reached! % 185.50/29.14 % (3409763)------------------------------ % 185.50/29.14 % (3409763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.50/29.14 % (3409763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.50/29.14 % (3409763)CaDiCaL version: 2.1.3 % 185.50/29.14 % (3409763)Termination reason: Instruction limit % 185.50/29.14 % (3409763)Termination phase: Saturation % 185.50/29.14 % (3409763)Time elapsed: 1.193 s % 185.50/29.14 % (3409763)Peak memory usage: 46 MB % 185.50/29.14 % (3409763)Instructions burned: 2945 (million) % 185.50/29.14 % (3409874)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2724452501:i=12648:rtra=on_2765 on theBenchmark for (2765ds/12648Mi) % 185.50/29.14 % (3409874)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.50/29.14 % (3409874)Terminated due to inappropriate strategy. % 185.50/29.14 % (3409874)------------------------------ % 185.50/29.14 % (3409874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.50/29.14 % (3409874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.50/29.14 % (3409874)CaDiCaL version: 2.1.3 % 185.50/29.14 % (3409874)Termination reason: Inappropriate % 185.50/29.14 % (3409874)Time elapsed: 0.004 s % 185.50/29.14 % (3409874)Peak memory usage: 11 MB % 185.50/29.14 % (3409874)Instructions burned: 13 (million) % 185.50/29.14 % (3409874)------------------------------ % 185.50/29.14 % (3409874)------------------------------ % 185.50/29.14 % (3409876)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=9298622:fmbsr=2.30978:i=4348:rtra=on_2765 on theBenchmark for (2765ds/4348Mi) % 185.50/29.14 % (3409876)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.50/29.14 % (3409876)Terminated due to inappropriate strategy. % 185.50/29.14 % (3409876)------------------------------ % 258.33/36.82 % (3409876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.33/36.82 % (3409876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.33/36.82 % (3409876)CaDiCaL version: 2.1.3 % 258.33/36.82 % (3409876)Termination reason: Inappropriate % 258.33/36.82 % (3409876)Time elapsed: 0.003 s % 258.33/36.82 % (3409876)Peak memory usage: 10 MB % 258.33/36.82 % (3409876)Instructions burned: 11 (million) % 258.33/36.82 % (3409876)------------------------------ % 258.33/36.82 % (3409876)------------------------------ % 258.33/36.82 % (3409878)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3122510242:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2765 on theBenchmark for (2765ds/1738Mi) % 258.33/36.82 % (3409709)Instruction limit reached! % 258.33/36.82 % (3409709)------------------------------ % 258.33/36.82 % (3409709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.33/36.82 % (3409709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.33/36.82 % (3409709)CaDiCaL version: 2.1.3 % 258.33/36.82 % (3409709)Termination reason: Instruction limit % 258.33/36.82 % (3409709)Termination phase: Saturation % 258.33/36.82 % (3409709)Time elapsed: 4.750 s % 258.33/36.82 % (3409709)Peak memory usage: 51 MB % 258.33/36.82 % (3409709)Instructions burned: 10263 (million) % 258.33/36.82 % (3409927)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1255226602:i=10228:av=off:rtra=on_2762 on theBenchmark for (2762ds/10228Mi) % 258.33/36.82 % (3409878)Instruction limit reached! % 258.33/36.82 % (3409878)------------------------------ % 258.33/36.82 % (3409878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.33/36.82 % (3409878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.33/36.82 % (3409878)CaDiCaL version: 2.1.3 % 258.33/36.82 % (3409878)Termination reason: Instruction limit % 258.33/36.82 % (3409878)Termination phase: Saturation % 258.33/36.82 % (3409878)Time elapsed: 0.622 s % 258.33/36.82 % (3409878)Peak memory usage: 22 MB % 258.33/36.82 % (3409878)Instructions burned: 1739 (million) % 258.33/36.82 % (3409929)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3473019618:i=108564:rtra=on_2758 on theBenchmark for (2758ds/108564Mi) % 258.33/36.82 % (3409929)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 258.33/36.82 % (3409929)Terminated due to inappropriate strategy. % 258.33/36.82 % (3409929)------------------------------ % 258.33/36.82 % (3409929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.33/36.82 % (3409929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.33/36.82 % (3409929)CaDiCaL version: 2.1.3 % 258.33/36.82 % (3409929)Termination reason: Inappropriate % 258.33/36.82 % (3409929)Time elapsed: 0.004 s % 258.33/36.82 % (3409929)Peak memory usage: 11 MB % 258.33/36.82 % (3409929)Instructions burned: 14 (million) % 258.33/36.82 % (3409929)------------------------------ % 258.33/36.82 % (3409929)------------------------------ % 258.33/36.82 % (3409931)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1959792880:i=7024:aac=none:rtra=on_2758 on theBenchmark for (2758ds/7024Mi) % 258.33/36.82 % (3409099)Instruction limit reached! % 258.33/36.82 % (3409099)------------------------------ % 258.33/36.82 % (3409099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.33/36.82 % (3409099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.33/36.82 % (3409099)CaDiCaL version: 2.1.3 % 258.33/36.82 % (3409099)Termination reason: Instruction limit % 258.33/36.82 % (3409099)Termination phase: Saturation % 258.33/36.82 % (3409099)Time elapsed: 25.218 s % 258.33/36.82 % (3409099)Peak memory usage: 569 MB % 258.33/36.82 % (3409099)Instructions burned: 88024 (million) % 258.33/36.82 % (3409933)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=911231197:i=7546:rtra=on:amm=off_2746 on theBenchmark for (2746ds/7546Mi) % 258.33/36.82 % (3409931)Instruction limit reached! % 258.33/36.82 % (3409931)------------------------------ % 258.33/36.82 % (3409931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.33/36.82 % (3409931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.33/36.82 % (3409931)CaDiCaL version: 2.1.3 % 258.33/36.82 % (3409931)Termination reason: Instruction limit % 258.33/36.82 % (3409931)Termination phase: Saturation % 258.33/36.82 % (3409931)Time elapsed: 2.344 s % 258.33/36.82 % (3409931)Peak memory usage: 46 MB % 258.33/36.82 % (3409931)Instructions burned: 7025 (million) % 258.33/36.82 % (3409935)ott+11_1_sil=16000:si=on:gs=on:random_seed=977478637:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=oTerminated % 300.13/42.73 % Vampire exiting %------------------------------------------------------------------------------