%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC458_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n020.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:06:01 PM UTC 2026 % Result : Timeout 300.13s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC458_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.06/0.18 % Computer : n020.cluster.edu % 0.06/0.18 % Model : x86_64 x86_64 % 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.18 % Memory : 8046.5625MB % 0.06/0.18 % OS : Linux 6.8.0-71-generic % 0.06/0.18 % CPULimit : 300 % 0.06/0.18 % WCLimit : 300 % 0.06/0.18 % DateTime : Mon Sep 28 09:40:19 UTC 2026 % 0.06/0.18 % CPUTime : % 0.06/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.06/0.21 Running first-order model finding % 0.06/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.86/0.81 % (56710)Will run a generic schedule for satisfiability detection. % 3.86/0.81 % (56716)% WARNING: option uhcvi not known. % 3.86/0.81 % (56715)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1870909320_2999 on theBenchmark for (2999ds/0Mi) % 3.86/0.81 % (56718)dis+10_1_sil=32000:sp=arity:random_seed=599442054:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.86/0.81 % (56719)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2938443466:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.86/0.81 % (56717)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2181664324:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.86/0.81 % (56720)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=325374743:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.86/0.81 % (56721)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1126605612:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.86/0.81 % (56716)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1463473893:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.86/0.81 % (56715)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.86/0.81 % (56715)Terminated due to inappropriate strategy. % 3.86/0.81 % (56715)------------------------------ % 3.86/0.81 % (56715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.86/0.81 % (56715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.86/0.81 % (56715)CaDiCaL version: 2.1.3 % 3.86/0.81 % (56715)Termination reason: Inappropriate % 3.86/0.81 % (56715)Time elapsed: 0.001 s % 3.86/0.81 % (56715)Peak memory usage: 10 MB % 3.86/0.81 % (56715)Instructions burned: 2 (million) % 3.86/0.81 % (56715)------------------------------ % 3.86/0.81 % (56715)------------------------------ % 3.86/0.81 % (56729)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3298846591:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.86/0.81 % (56729)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.86/0.81 % (56729)Terminated due to inappropriate strategy. % 3.86/0.81 % (56729)------------------------------ % 3.86/0.81 % (56729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.86/0.81 % (56729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.86/0.81 % (56729)CaDiCaL version: 2.1.3 % 3.86/0.81 % (56729)Termination reason: Inappropriate % 3.86/0.81 % (56729)Time elapsed: 0.001 s % 3.86/0.81 % (56729)Peak memory usage: 11 MB % 3.86/0.81 % (56729)Instructions burned: 2 (million) % 3.86/0.81 % (56729)------------------------------ % 3.86/0.81 % (56729)------------------------------ % 3.86/0.81 % (56731)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2111788385:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.86/0.81 % (56718)Instruction limit reached! % 3.86/0.81 % (56718)------------------------------ % 3.86/0.81 % (56718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.86/0.81 % (56718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.86/0.81 % (56718)CaDiCaL version: 2.1.3 % 3.86/0.81 % (56718)Termination reason: Instruction limit % 3.86/0.81 % (56718)Termination phase: Saturation % 3.86/0.81 % (56718)Time elapsed: 0.063 s % 3.86/0.81 % (56718)Peak memory usage: 12 MB % 3.86/0.81 % (56718)Instructions burned: 104 (million) % 3.86/0.81 % (56719)Instruction limit reached! % 3.86/0.81 % (56719)------------------------------ % 3.86/0.81 % (56719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.86/0.81 % (56719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.86/0.81 % (56719)CaDiCaL version: 2.1.3 % 3.86/0.81 % (56719)Termination reason: Instruction limit % 3.86/0.81 % (56719)Termination phase: Saturation % 3.86/0.81 % (56719)Time elapsed: 0.069 s % 3.86/0.81 % (56719)Peak memory usage: 12 MB % 3.86/0.81 % (56719)Instructions burned: 116 (million) % 3.86/0.81 % (56720)Instruction limit reached! % 3.86/0.81 % (56720)------------------------------ % 3.86/0.81 % (56720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.86/0.81 % (56720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.86/0.81 % (56720)CaDiCaL version: 2.1.3 % 3.86/0.81 % (56720)Termination reason: Instruction limit % 3.86/0.81 % (56720)Termination phase: Saturation % 3.86/0.81 % (56720)Time elapsed: 0.078 s % 3.86/0.81 % (56720)Peak memory usage: 13 MB % 7.46/1.35 % (56720)Instructions burned: 132 (million) % 7.46/1.35 % (56733)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=583392512:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.46/1.35 % (56734)ott-21_1_sil=16000:fs=off:random_seed=2820375133:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 7.46/1.35 % (56735)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1841821037:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.46/1.35 % (56721)Instruction limit reached! % 7.46/1.35 % (56721)------------------------------ % 7.46/1.35 % (56721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.46/1.35 % (56721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.46/1.35 % (56721)CaDiCaL version: 2.1.3 % 7.46/1.35 % (56721)Termination reason: Instruction limit % 7.46/1.35 % (56721)Termination phase: Saturation % 7.46/1.35 % (56721)Time elapsed: 0.104 s % 7.46/1.35 % (56721)Peak memory usage: 13 MB % 7.46/1.35 % (56721)Instructions burned: 159 (million) % 7.46/1.35 % (56739)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3660140972:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.46/1.35 % (56739)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.46/1.35 % (56739)Terminated due to inappropriate strategy. % 7.46/1.35 % (56739)------------------------------ % 7.46/1.35 % (56739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.46/1.35 % (56739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.46/1.35 % (56739)CaDiCaL version: 2.1.3 % 7.46/1.35 % (56739)Termination reason: Inappropriate % 7.46/1.35 % (56739)Time elapsed: 0.001 s % 7.46/1.35 % (56739)Peak memory usage: 10 MB % 7.46/1.35 % (56739)Instructions burned: 2 (million) % 7.46/1.35 % (56739)------------------------------ % 7.46/1.35 % (56739)------------------------------ % 7.46/1.35 % (56731)Instruction limit reached! % 7.46/1.35 % (56731)------------------------------ % 7.46/1.35 % (56731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.46/1.35 % (56731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.46/1.35 % (56731)CaDiCaL version: 2.1.3 % 7.46/1.35 % (56731)Termination reason: Instruction limit % 7.46/1.35 % (56731)Termination phase: Saturation % 7.46/1.35 % (56731)Time elapsed: 0.083 s % 7.46/1.35 % (56731)Peak memory usage: 12 MB % 7.46/1.35 % (56731)Instructions burned: 132 (million) % 7.46/1.35 % (56741)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1888387438:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.46/1.35 % (56742)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2326484676:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 7.46/1.35 % (56742)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.46/1.35 % (56742)Terminated due to inappropriate strategy. % 7.46/1.35 % (56742)------------------------------ % 7.46/1.35 % (56742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.46/1.35 % (56742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.46/1.35 % (56742)CaDiCaL version: 2.1.3 % 7.46/1.35 % (56742)Termination reason: Inappropriate % 7.46/1.35 % (56742)Time elapsed: 0.001 s % 7.46/1.35 % (56742)Peak memory usage: 10 MB % 7.46/1.35 % (56742)Instructions burned: 2 (million) % 7.46/1.35 % (56742)------------------------------ % 7.46/1.35 % (56742)------------------------------ % 7.46/1.35 % (56745)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=3922745031: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) % 7.46/1.35 % (56734)Instruction limit reached! % 7.46/1.35 % (56734)------------------------------ % 7.46/1.35 % (56734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.46/1.35 % (56734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.46/1.35 % (56734)CaDiCaL version: 2.1.3 % 7.46/1.35 % (56734)Termination reason: Instruction limit % 7.46/1.35 % (56734)Termination phase: Saturation % 7.46/1.35 % (56734)Time elapsed: 0.082 s % 7.46/1.35 % (56734)Peak memory usage: 12 MB % 7.46/1.35 % (56734)Instructions burned: 182 (million) % 7.46/1.35 % (56747)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4116271756:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 21.88/3.32 % (56735)Instruction limit reached! % 21.88/3.32 % (56735)------------------------------ % 21.88/3.32 % (56735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.88/3.32 % (56735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.88/3.32 % (56735)CaDiCaL version: 2.1.3 % 21.88/3.32 % (56735)Termination reason: Instruction limit % 21.88/3.32 % (56735)Termination phase: Saturation % 21.88/3.32 % (56735)Time elapsed: 0.215 s % 21.88/3.32 % (56735)Peak memory usage: 12 MB % 21.88/3.32 % (56735)Instructions burned: 479 (million) % 21.88/3.32 % (56749)fmb+10_1_sil=64000:random_seed=3352522991:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 21.88/3.32 % (56749)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.88/3.32 % (56749)Terminated due to inappropriate strategy. % 21.88/3.32 % (56749)------------------------------ % 21.88/3.32 % (56749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.88/3.32 % (56749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.88/3.32 % (56749)CaDiCaL version: 2.1.3 % 21.88/3.32 % (56749)Termination reason: Inappropriate % 21.88/3.32 % (56749)Time elapsed: 0.001 s % 21.88/3.32 % (56749)Peak memory usage: 11 MB % 21.88/3.32 % (56749)Instructions burned: 2 (million) % 21.88/3.32 % (56749)------------------------------ % 21.88/3.32 % (56749)------------------------------ % 21.88/3.32 % (56751)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3659537783:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 21.88/3.32 % (56751)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.88/3.32 % (56751)Terminated due to inappropriate strategy. % 21.88/3.32 % (56751)------------------------------ % 21.88/3.32 % (56751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.88/3.32 % (56751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.88/3.32 % (56751)CaDiCaL version: 2.1.3 % 21.88/3.32 % (56751)Termination reason: Inappropriate % 21.88/3.32 % (56751)Time elapsed: 0.001 s % 21.88/3.32 % (56751)Peak memory usage: 10 MB % 21.88/3.32 % (56751)Instructions burned: 2 (million) % 21.88/3.32 % (56751)------------------------------ % 21.88/3.32 % (56751)------------------------------ % 21.88/3.32 % (56753)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3263350361:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 21.88/3.32 % (56753)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.88/3.32 % (56753)Terminated due to inappropriate strategy. % 21.88/3.32 % (56753)------------------------------ % 21.88/3.32 % (56753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.88/3.32 % (56753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.88/3.32 % (56753)CaDiCaL version: 2.1.3 % 21.88/3.32 % (56753)Termination reason: Inappropriate % 21.88/3.32 % (56753)Time elapsed: 0.001 s % 21.88/3.32 % (56753)Peak memory usage: 10 MB % 21.88/3.32 % (56753)Instructions burned: 2 (million) % 21.88/3.32 % (56753)------------------------------ % 21.88/3.32 % (56753)------------------------------ % 21.88/3.32 % (56755)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3204027240:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 21.88/3.32 % (56733)Instruction limit reached! % 21.88/3.32 % (56733)------------------------------ % 21.88/3.32 % (56733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.88/3.32 % (56733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.88/3.32 % (56733)CaDiCaL version: 2.1.3 % 21.88/3.32 % (56733)Termination reason: Instruction limit % 21.88/3.32 % (56733)Termination phase: Saturation % 21.88/3.32 % (56733)Time elapsed: 0.362 s % 21.88/3.32 % (56733)Peak memory usage: 16 MB % 21.88/3.32 % (56733)Instructions burned: 686 (million) % 21.88/3.32 % (56757)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4240282043:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 21.88/3.32 % (56745)Instruction limit reached! % 21.88/3.32 % (56745)------------------------------ % 21.88/3.32 % (56745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.88/3.32 % (56745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.88/3.32 % (56745)CaDiCaL version: 2.1.3 % 21.88/3.32 % (56745)Termination reason: Instruction limit % 21.88/3.32 % (56745)Termination phase: Saturation % 21.88/3.32 % (56745)Time elapsed: 0.403 s % 21.88/3.32 % (56745)Peak memory usage: 19 MB % 38.93/5.70 % (56745)Instructions burned: 694 (million) % 38.93/5.70 % (56759)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2341138129:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 38.93/5.70 % (56759)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.93/5.70 % (56759)Terminated due to inappropriate strategy. % 38.93/5.70 % (56759)------------------------------ % 38.93/5.70 % (56759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.93/5.70 % (56759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.93/5.70 % (56759)CaDiCaL version: 2.1.3 % 38.93/5.70 % (56759)Termination reason: Inappropriate % 38.93/5.70 % (56759)Time elapsed: 0.001 s % 38.93/5.70 % (56759)Peak memory usage: 10 MB % 38.93/5.70 % (56759)Instructions burned: 2 (million) % 38.93/5.70 % (56759)------------------------------ % 38.93/5.70 % (56759)------------------------------ % 38.93/5.70 % (56761)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3021321057:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 38.93/5.70 % (56761)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.93/5.70 % (56761)Terminated due to inappropriate strategy. % 38.93/5.70 % (56761)------------------------------ % 38.93/5.70 % (56761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.93/5.70 % (56761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.93/5.70 % (56761)CaDiCaL version: 2.1.3 % 38.93/5.70 % (56761)Termination reason: Inappropriate % 38.93/5.70 % (56761)Time elapsed: 0.001 s % 38.93/5.70 % (56761)Peak memory usage: 10 MB % 38.93/5.70 % (56761)Instructions burned: 2 (million) % 38.93/5.70 % (56761)------------------------------ % 38.93/5.70 % (56761)------------------------------ % 38.93/5.70 % (56763)ott-2_1_sil=16000:newcnf=on:random_seed=1168456828:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 38.93/5.70 % (56747)Instruction limit reached! % 38.93/5.70 % (56747)------------------------------ % 38.93/5.70 % (56747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.93/5.70 % (56747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.93/5.70 % (56747)CaDiCaL version: 2.1.3 % 38.93/5.70 % (56747)Termination reason: Instruction limit % 38.93/5.70 % (56747)Termination phase: Saturation % 38.93/5.70 % (56747)Time elapsed: 0.491 s % 38.93/5.70 % (56747)Peak memory usage: 19 MB % 38.93/5.70 % (56747)Instructions burned: 880 (million) % 38.93/5.70 % (56765)ott+10_1_sil=32000:tgt=ground:random_seed=112003283:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 38.93/5.70 % (56741)Instruction limit reached! % 38.93/5.70 % (56741)------------------------------ % 38.93/5.70 % (56741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.93/5.70 % (56741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.93/5.70 % (56741)CaDiCaL version: 2.1.3 % 38.93/5.70 % (56741)Termination reason: Instruction limit % 38.93/5.70 % (56741)Termination phase: Saturation % 38.93/5.70 % (56741)Time elapsed: 0.659 s % 38.93/5.70 % (56741)Peak memory usage: 19 MB % 38.93/5.70 % (56741)Instructions burned: 1181 (million) % 38.93/5.70 % (56767)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2628548823:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 38.93/5.70 % (56767)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.93/5.70 % (56767)Terminated due to inappropriate strategy. % 38.93/5.70 % (56767)------------------------------ % 38.93/5.70 % (56767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.93/5.70 % (56767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.93/5.70 % (56767)CaDiCaL version: 2.1.3 % 38.93/5.70 % (56767)Termination reason: Inappropriate % 38.93/5.70 % (56767)Time elapsed: 0.001 s % 38.93/5.70 % (56767)Peak memory usage: 10 MB % 38.93/5.70 % (56767)Instructions burned: 2 (million) % 38.93/5.70 % (56767)------------------------------ % 38.93/5.70 % (56767)------------------------------ % 38.93/5.70 % (56769)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2871457866:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 38.93/5.70 % (56763)Instruction limit reached! % 38.93/5.70 % (56763)------------------------------ % 38.93/5.70 % (56763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.93/5.70 % (56763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.93/5.70 % (56763)CaDiCaL version: 2.1.3 % 105.14/15.05 % (56763)Termination reason: Instruction limit % 105.14/15.05 % (56763)Termination phase: Saturation % 105.14/15.05 % (56763)Time elapsed: 0.472 s % 105.14/15.05 % (56763)Peak memory usage: 15 MB % 105.14/15.05 % (56763)Instructions burned: 869 (million) % 105.14/15.05 % (56771)dis+21_1_sil=32000:sas=cadical:random_seed=2648351214:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 105.14/15.05 % (56757)Instruction limit reached! % 105.14/15.05 % (56757)------------------------------ % 105.14/15.05 % (56757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.14/15.05 % (56757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.14/15.05 % (56757)CaDiCaL version: 2.1.3 % 105.14/15.05 % (56757)Termination reason: Instruction limit % 105.14/15.05 % (56757)Termination phase: Saturation % 105.14/15.05 % (56757)Time elapsed: 0.903 s % 105.14/15.05 % (56757)Peak memory usage: 26 MB % 105.14/15.05 % (56757)Instructions burned: 1472 (million) % 105.14/15.05 % (56773)ott+11_1_sil=16000:gs=on:random_seed=1078081768:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 105.14/15.05 % (56755)Instruction limit reached! % 105.14/15.05 % (56755)------------------------------ % 105.14/15.05 % (56755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.14/15.05 % (56755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.14/15.05 % (56755)CaDiCaL version: 2.1.3 % 105.14/15.05 % (56755)Termination reason: Instruction limit % 105.14/15.05 % (56755)Termination phase: Saturation % 105.14/15.05 % (56755)Time elapsed: 1.449 s % 105.14/15.05 % (56755)Peak memory usage: 40 MB % 105.14/15.05 % (56755)Instructions burned: 5133 (million) % 105.14/15.05 % (56775)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3884160031:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 105.14/15.05 % (56775)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 105.14/15.05 % (56775)Terminated due to inappropriate strategy. % 105.14/15.05 % (56775)------------------------------ % 105.14/15.05 % (56775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.14/15.05 % (56775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.14/15.05 % (56775)CaDiCaL version: 2.1.3 % 105.14/15.05 % (56775)Termination reason: Inappropriate % 105.14/15.05 % (56775)Time elapsed: 0.0000 s % 105.14/15.05 % (56775)Peak memory usage: 10 MB % 105.14/15.05 % (56775)Instructions burned: 2 (million) % 105.14/15.05 % (56775)------------------------------ % 105.14/15.05 % (56775)------------------------------ % 105.14/15.05 % (56777)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1432993882:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 105.14/15.05 % (56773)Instruction limit reached! % 105.14/15.05 % (56773)------------------------------ % 105.14/15.05 % (56773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.14/15.05 % (56773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.14/15.05 % (56773)CaDiCaL version: 2.1.3 % 105.14/15.05 % (56773)Termination reason: Instruction limit % 105.14/15.05 % (56773)Termination phase: Saturation % 105.14/15.05 % (56773)Time elapsed: 1.202 s % 105.14/15.05 % (56773)Peak memory usage: 21 MB % 105.14/15.05 % (56773)Instructions burned: 2253 (million) % 105.14/15.05 % (56779)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1988008376:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 105.14/15.05 % (56769)Instruction limit reached! % 105.14/15.05 % (56769)------------------------------ % 105.14/15.05 % (56769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.14/15.05 % (56769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.14/15.05 % (56769)CaDiCaL version: 2.1.3 % 105.14/15.05 % (56769)Termination reason: Instruction limit % 105.14/15.05 % (56769)Termination phase: Saturation % 105.14/15.05 % (56769)Time elapsed: 1.850 s % 105.14/15.05 % (56769)Peak memory usage: 36 MB % 105.14/15.05 % (56769)Instructions burned: 3512 (million) % 105.14/15.05 % (56781)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4113863050:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 105.14/15.05 % (56777)Instruction limit reached! % 105.14/15.05 % (56777)------------------------------ % 105.14/15.05 % (56777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.14/15.05 % (56777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.14/15.05 % (56777)CaDiCaL version: 2.1.3 % 105.14/15.05 % (56777)Termination reason: Instruction limit % 118.01/16.93 % (56777)Termination phase: Saturation % 118.01/16.93 % (56777)Time elapsed: 1.205 s % 118.01/16.93 % (56777)Peak memory usage: 54 MB % 118.01/16.93 % (56777)Instructions burned: 4591 (million) % 118.01/16.93 % (56783)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=624413542:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 118.01/16.93 % (56783)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 118.01/16.93 % (56783)Terminated due to inappropriate strategy. % 118.01/16.93 % (56783)------------------------------ % 118.01/16.93 % (56783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.01/16.93 % (56783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.01/16.93 % (56783)CaDiCaL version: 2.1.3 % 118.01/16.93 % (56783)Termination reason: Inappropriate % 118.01/16.93 % (56783)Time elapsed: 0.0000 s % 118.01/16.93 % (56783)Peak memory usage: 10 MB % 118.01/16.93 % (56783)Instructions burned: 2 (million) % 118.01/16.93 % (56783)------------------------------ % 118.01/16.93 % (56783)------------------------------ % 118.01/16.93 % (56785)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3957321:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 118.01/16.93 % (56785)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 118.01/16.93 % (56785)Terminated due to inappropriate strategy. % 118.01/16.93 % (56785)------------------------------ % 118.01/16.93 % (56785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.01/16.93 % (56785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.01/16.93 % (56785)CaDiCaL version: 2.1.3 % 118.01/16.93 % (56785)Termination reason: Inappropriate % 118.01/16.93 % (56785)Time elapsed: 0.0000 s % 118.01/16.93 % (56785)Peak memory usage: 10 MB % 118.01/16.93 % (56785)Instructions burned: 2 (million) % 118.01/16.93 % (56785)------------------------------ % 118.01/16.93 % (56785)------------------------------ % 118.01/16.93 % (56787)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=574019879:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 118.01/16.93 % (56787)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 118.01/16.93 % (56787)Terminated due to inappropriate strategy. % 118.01/16.93 % (56787)------------------------------ % 118.01/16.93 % (56787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.01/16.93 % (56787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.01/16.93 % (56787)CaDiCaL version: 2.1.3 % 118.01/16.93 % (56787)Termination reason: Inappropriate % 118.01/16.93 % (56787)Time elapsed: 0.0000 s % 118.01/16.93 % (56787)Peak memory usage: 10 MB % 118.01/16.93 % (56787)Instructions burned: 2 (million) % 118.01/16.93 % (56787)------------------------------ % 118.01/16.93 % (56787)------------------------------ % 118.01/16.93 % (56789)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2638141130:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 118.01/16.93 % (56771)Instruction limit reached! % 118.01/16.93 % (56771)------------------------------ % 118.01/16.93 % (56771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.01/16.93 % (56771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.01/16.93 % (56771)CaDiCaL version: 2.1.3 % 118.01/16.93 % (56771)Termination reason: Instruction limit % 118.01/16.93 % (56771)Termination phase: Saturation % 118.01/16.93 % (56771)Time elapsed: 2.035 s % 118.01/16.93 % (56771)Peak memory usage: 31 MB % 118.01/16.93 % (56771)Instructions burned: 3773 (million) % 118.01/16.93 % (56791)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3331847359:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 118.01/16.93 % (56765)Instruction limit reached! % 118.01/16.93 % (56765)------------------------------ % 118.01/16.93 % (56765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.01/16.93 % (56765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.01/16.93 % (56765)CaDiCaL version: 2.1.3 % 118.01/16.93 % (56765)Termination reason: Instruction limit % 118.01/16.93 % (56765)Termination phase: Saturation % 118.01/16.93 % (56765)Time elapsed: 3.218 s % 118.01/16.93 % (56765)Peak memory usage: 36 MB % 118.01/16.93 % (56765)Instructions burned: 5115 (million) % 118.01/16.93 % (56793)dis+10_16:1_sil=16000:random_seed=3698365499:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi) % 118.01/16.93 % (56781)Instruction limit reached! % 118.01/16.93 % (56781)------------------------------ % 118.01/16.93 % (56781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.01/16.93 % (56781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.45/17.22 % (56781)CaDiCaL version: 2.1.3 % 120.45/17.22 % (56781)Termination reason: Instruction limit % 120.45/17.22 % (56781)Termination phase: Saturation % 120.45/17.22 % (56781)Time elapsed: 2.736 s % 120.45/17.22 % (56781)Peak memory usage: 55 MB % 120.45/17.22 % (56781)Instructions burned: 5212 (million) % 120.45/17.22 % (56795)ott-3_8_sil=64000:random_seed=1554699450:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi) % 120.45/17.22 % (56789)Instruction limit reached! % 120.45/17.22 % (56789)------------------------------ % 120.45/17.22 % (56789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.45/17.22 % (56789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.45/17.22 % (56789)CaDiCaL version: 2.1.3 % 120.45/17.22 % (56789)Termination reason: Instruction limit % 120.45/17.22 % (56789)Termination phase: Saturation % 120.45/17.22 % (56789)Time elapsed: 4.805 s % 120.45/17.22 % (56789)Peak memory usage: 82 MB % 120.45/17.22 % (56789)Instructions burned: 22571 (million) % 120.45/17.22 % (56797)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3810445599:fmbsr=2:i=32576_2920 on theBenchmark for (2920ds/32576Mi) % 120.45/17.22 % (56797)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 120.45/17.22 % (56797)Terminated due to inappropriate strategy. % 120.45/17.22 % (56797)------------------------------ % 120.45/17.22 % (56797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.45/17.22 % (56797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.45/17.22 % (56797)CaDiCaL version: 2.1.3 % 120.45/17.22 % (56797)Termination reason: Inappropriate % 120.45/17.22 % (56797)Time elapsed: 0.0000 s % 120.45/17.22 % (56797)Peak memory usage: 10 MB % 120.45/17.22 % (56797)Instructions burned: 2 (million) % 120.45/17.22 % (56797)------------------------------ % 120.45/17.22 % (56797)------------------------------ % 120.45/17.22 % (56799)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3389586243:i=11404_2920 on theBenchmark for (2920ds/11404Mi) % 120.45/17.22 % (56791)Instruction limit reached! % 120.45/17.22 % (56791)------------------------------ % 120.45/17.22 % (56791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.45/17.22 % (56791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.45/17.22 % (56791)CaDiCaL version: 2.1.3 % 120.45/17.22 % (56791)Termination reason: Instruction limit % 120.45/17.22 % (56791)Termination phase: Saturation % 120.45/17.22 % (56791)Time elapsed: 5.033 s % 120.45/17.22 % (56791)Peak memory usage: 55 MB % 120.45/17.22 % (56791)Instructions burned: 8173 (million) % 120.45/17.22 % (56801)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=608194205:i=14134_2917 on theBenchmark for (2917ds/14134Mi) % 120.45/17.22 % (56793)Instruction limit reached! % 120.45/17.22 % (56793)------------------------------ % 120.45/17.22 % (56793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.45/17.22 % (56793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.45/17.22 % (56793)CaDiCaL version: 2.1.3 % 120.45/17.22 % (56793)Termination reason: Instruction limit % 120.45/17.22 % (56793)Termination phase: Saturation % 120.45/17.22 % (56793)Time elapsed: 4.617 s % 120.45/17.22 % (56793)Peak memory usage: 52 MB % 120.45/17.22 % (56793)Instructions burned: 9156 (million) % 120.45/17.22 % (56803)dis+33_16_sil=32000:sac=on:random_seed=4244631566:i=15851:nm=0_2914 on theBenchmark for (2914ds/15851Mi) % 120.45/17.22 % (56799)Instruction limit reached! % 120.45/17.22 % (56799)------------------------------ % 120.45/17.22 % (56799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.45/17.22 % (56799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.45/17.22 % (56799)CaDiCaL version: 2.1.3 % 120.45/17.22 % (56799)Termination reason: Instruction limit % 120.45/17.22 % (56799)Termination phase: Saturation % 120.45/17.22 % (56799)Time elapsed: 3.818 s % 120.45/17.22 % (56799)Peak memory usage: 63 MB % 120.45/17.22 % (56799)Instructions burned: 11405 (million) % 120.45/17.22 % (56805)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2541563827:avsq=on:i=17627:add=on:amm=off_2881 on theBenchmark for (2881ds/17627Mi) % 120.45/17.22 % (56779)Instruction limit reached! % 120.45/17.22 % (56779)------------------------------ % 120.45/17.22 % (56779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.45/17.22 % (56779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.45/17.22 % (56779)CaDiCaL version: 2.1.3 % 120.45/17.22 % (56779)Termination reason: Instruction limit % 120.45/17.22 % (56779)Termination phase: Saturation % 127.19/18.14 % (56779)Time elapsed: 12.193 s % 127.19/18.14 % (56779)Peak memory usage: 125 MB % 127.19/18.14 % (56779)Instructions burned: 29343 (million) % 127.19/18.14 % (56808)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3586335044:s2a=on:i=53295_2851 on theBenchmark for (2851ds/53295Mi) % 127.19/18.14 % (56803)Instruction limit reached! % 127.19/18.14 % (56803)------------------------------ % 127.19/18.14 % (56803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.19/18.14 % (56803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.19/18.14 % (56803)CaDiCaL version: 2.1.3 % 127.19/18.14 % (56803)Termination reason: Instruction limit % 127.19/18.14 % (56803)Termination phase: Saturation % 127.19/18.14 % (56803)Time elapsed: 7.625 s % 127.19/18.14 % (56803)Peak memory usage: 163 MB % 127.19/18.14 % (56803)Instructions burned: 15851 (million) % 127.19/18.14 % (56810)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1344688334:i=26857:ins=20_2837 on theBenchmark for (2837ds/26857Mi) % 127.19/18.14 % (56810)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.19/18.14 % (56810)Terminated due to inappropriate strategy. % 127.19/18.14 % (56810)------------------------------ % 127.19/18.14 % (56810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.19/18.14 % (56810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.19/18.14 % (56810)CaDiCaL version: 2.1.3 % 127.19/18.14 % (56810)Termination reason: Inappropriate % 127.19/18.14 % (56810)Time elapsed: 0.001 s % 127.19/18.14 % (56810)Peak memory usage: 10 MB % 127.19/18.14 % (56810)Instructions burned: 2 (million) % 127.19/18.14 % (56810)------------------------------ % 127.19/18.14 % (56810)------------------------------ % 127.19/18.14 % (56812)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2365707632:i=28120:bs=on:fsr=off_2837 on theBenchmark for (2837ds/28120Mi) % 127.19/18.14 % (56805)Instruction limit reached! % 127.19/18.14 % (56805)------------------------------ % 127.19/18.14 % (56805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.19/18.14 % (56805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.19/18.14 % (56805)CaDiCaL version: 2.1.3 % 127.19/18.14 % (56805)Termination reason: Instruction limit % 127.19/18.14 % (56805)Termination phase: Saturation % 127.19/18.14 % (56805)Time elapsed: 4.850 s % 127.19/18.14 % (56805)Peak memory usage: 115 MB % 127.19/18.14 % (56805)Instructions burned: 17630 (million) % 127.19/18.14 % (56814)fmb+10_1_sil=256000:fmbss=7:random_seed=3637003721:fmbsr=1.6:i=182295_2833 on theBenchmark for (2833ds/182295Mi) % 127.19/18.14 % (56814)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.19/18.14 % (56814)Terminated due to inappropriate strategy. % 127.19/18.14 % (56814)------------------------------ % 127.19/18.14 % (56814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.19/18.14 % (56814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.19/18.14 % (56814)CaDiCaL version: 2.1.3 % 127.19/18.14 % (56814)Termination reason: Inappropriate % 127.19/18.14 % (56814)Time elapsed: 0.0000 s % 127.19/18.14 % (56814)Peak memory usage: 10 MB % 127.19/18.14 % (56814)Instructions burned: 2 (million) % 127.19/18.14 % (56814)------------------------------ % 127.19/18.14 % (56814)------------------------------ % 127.19/18.14 % (56816)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2260169938:i=44625:gsp=on_2833 on theBenchmark for (2833ds/44625Mi) % 127.19/18.14 % (56816)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.19/18.14 % (56816)Terminated due to inappropriate strategy. % 127.19/18.14 % (56816)------------------------------ % 127.19/18.14 % (56816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.19/18.14 % (56816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.19/18.14 % (56816)CaDiCaL version: 2.1.3 % 127.19/18.14 % (56816)Termination reason: Inappropriate % 127.19/18.14 % (56816)Time elapsed: 0.0000 s % 127.19/18.14 % (56816)Peak memory usage: 11 MB % 127.19/18.14 % (56816)Instructions burned: 2 (million) % 127.19/18.14 % (56816)------------------------------ % 127.19/18.14 % (56816)------------------------------ % 127.19/18.14 % (56818)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2669678158:i=160505_2832 on theBenchmark for (2832ds/160505Mi) % 127.19/18.14 % (56818)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.19/18.14 % (56818)Terminated due to inappropriate strategy. % 127.19/18.14 % (56818)------------------------------ % 127.19/18.14 % (56818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.74/21.05 % (56818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.74/21.05 % (56818)CaDiCaL version: 2.1.3 % 147.74/21.05 % (56818)Termination reason: Inappropriate % 147.74/21.05 % (56818)Time elapsed: 0.0000 s % 147.74/21.05 % (56818)Peak memory usage: 10 MB % 147.74/21.05 % (56818)Instructions burned: 2 (million) % 147.74/21.05 % (56818)------------------------------ % 147.74/21.05 % (56818)------------------------------ % 147.74/21.05 % (56820)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=183107608:fmbsr=1.3:i=225729_2832 on theBenchmark for (2832ds/225729Mi) % 147.74/21.05 % (56820)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 147.74/21.05 % (56820)Terminated due to inappropriate strategy. % 147.74/21.05 % (56820)------------------------------ % 147.74/21.05 % (56820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.74/21.05 % (56820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.74/21.05 % (56820)CaDiCaL version: 2.1.3 % 147.74/21.05 % (56820)Termination reason: Inappropriate % 147.74/21.05 % (56820)Time elapsed: 0.001 s % 147.74/21.05 % (56820)Peak memory usage: 10 MB % 147.74/21.05 % (56820)Instructions burned: 2 (million) % 147.74/21.05 % (56820)------------------------------ % 147.74/21.05 % (56820)------------------------------ % 147.74/21.05 % (56822)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3343789298:fmbsr=2:i=185024:ins=7_2832 on theBenchmark for (2832ds/185024Mi) % 147.74/21.05 % (56822)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 147.74/21.05 % (56822)Terminated due to inappropriate strategy. % 147.74/21.05 % (56822)------------------------------ % 147.74/21.05 % (56822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.74/21.05 % (56822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.74/21.05 % (56822)CaDiCaL version: 2.1.3 % 147.74/21.05 % (56822)Termination reason: Inappropriate % 147.74/21.05 % (56822)Time elapsed: 0.0000 s % 147.74/21.05 % (56822)Peak memory usage: 11 MB % 147.74/21.05 % (56822)Instructions burned: 2 (million) % 147.74/21.05 % (56822)------------------------------ % 147.74/21.05 % (56822)------------------------------ % 147.74/21.05 % (56824)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2287038065:rtra=on_2832 on theBenchmark for (2832ds/0Mi) % 147.74/21.05 % (56824)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 147.74/21.05 % (56824)Terminated due to inappropriate strategy. % 147.74/21.05 % (56824)------------------------------ % 147.74/21.05 % (56824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.74/21.05 % (56824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.74/21.05 % (56824)CaDiCaL version: 2.1.3 % 147.74/21.05 % (56824)Termination reason: Inappropriate % 147.74/21.05 % (56824)Time elapsed: 0.0000 s % 147.74/21.05 % (56824)Peak memory usage: 10 MB % 147.74/21.05 % (56824)Instructions burned: 2 (million) % 147.74/21.05 % (56824)------------------------------ % 147.74/21.05 % (56824)------------------------------ % 147.74/21.05 % (56826)% WARNING: option uhcvi not known. % 147.74/21.05 % (56826)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1175138279:i=271062:add=off:rtra=on:rawr=on_2832 on theBenchmark for (2832ds/271062Mi) % 147.74/21.05 % (56795)Instruction limit reached! % 147.74/21.05 % (56795)------------------------------ % 147.74/21.05 % (56795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.74/21.05 % (56795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.74/21.05 % (56795)CaDiCaL version: 2.1.3 % 147.74/21.05 % (56795)Termination reason: Instruction limit % 147.74/21.05 % (56795)Termination phase: Saturation % 147.74/21.05 % (56795)Time elapsed: 11.387 s % 147.74/21.05 % (56795)Peak memory usage: 66 MB % 147.74/21.05 % (56795)Instructions burned: 20140 (million) % 147.74/21.05 % (56828)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3702931647:i=176048:add=on:rtra=on:rawr=on_2830 on theBenchmark for (2830ds/176048Mi) % 147.74/21.05 % (56801)Instruction limit reached! % 147.74/21.05 % (56801)------------------------------ % 147.74/21.05 % (56801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.74/21.05 % (56801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.74/21.05 % (56801)CaDiCaL version: 2.1.3 % 147.74/21.05 % (56801)Termination reason: Instruction limit % 147.74/21.05 % (56801)Termination phase: Saturation % 147.74/21.05 % (56801)Time elapsed: 8.742 s % 161.01/23.02 % (56801)Peak memory usage: 80 MB % 161.01/23.02 % (56801)Instructions burned: 14134 (million) % 161.01/23.02 % (56830)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3889318034:i=206:fgj=on:rtra=on_2829 on theBenchmark for (2829ds/206Mi) % 161.01/23.02 % (56830)Instruction limit reached! % 161.01/23.02 % (56830)------------------------------ % 161.01/23.02 % (56830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.01/23.02 % (56830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.01/23.02 % (56830)CaDiCaL version: 2.1.3 % 161.01/23.02 % (56830)Termination reason: Instruction limit % 161.01/23.02 % (56830)Termination phase: Saturation % 161.01/23.02 % (56830)Time elapsed: 0.120 s % 161.01/23.02 % (56830)Peak memory usage: 13 MB % 161.01/23.02 % (56830)Instructions burned: 208 (million) % 161.01/23.02 % (56832)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3822033639:i=232:rtra=on_2828 on theBenchmark for (2828ds/232Mi) % 161.01/23.02 % (56832)Instruction limit reached! % 161.01/23.02 % (56832)------------------------------ % 161.01/23.02 % (56832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.01/23.02 % (56832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.01/23.02 % (56832)CaDiCaL version: 2.1.3 % 161.01/23.02 % (56832)Termination reason: Instruction limit % 161.01/23.02 % (56832)Termination phase: Saturation % 161.01/23.02 % (56832)Time elapsed: 0.144 s % 161.01/23.02 % (56832)Peak memory usage: 13 MB % 161.01/23.02 % (56832)Instructions burned: 233 (million) % 161.01/23.02 % (56834)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2680032620:i=262:rtra=on_2826 on theBenchmark for (2826ds/262Mi) % 161.01/23.02 % (56834)Instruction limit reached! % 161.01/23.02 % (56834)------------------------------ % 161.01/23.02 % (56834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.01/23.02 % (56834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.01/23.02 % (56834)CaDiCaL version: 2.1.3 % 161.01/23.02 % (56834)Termination reason: Instruction limit % 161.01/23.02 % (56834)Termination phase: Saturation % 161.01/23.02 % (56834)Time elapsed: 0.141 s % 161.01/23.02 % (56834)Peak memory usage: 14 MB % 161.01/23.02 % (56834)Instructions burned: 266 (million) % 161.01/23.02 % (56836)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=78492756:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2825 on theBenchmark for (2825ds/318Mi) % 161.01/23.02 % (56836)Instruction limit reached! % 161.01/23.02 % (56836)------------------------------ % 161.01/23.02 % (56836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.01/23.02 % (56836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.01/23.02 % (56836)CaDiCaL version: 2.1.3 % 161.01/23.02 % (56836)Termination reason: Instruction limit % 161.01/23.02 % (56836)Termination phase: Saturation % 161.01/23.02 % (56836)Time elapsed: 0.208 s % 161.01/23.02 % (56836)Peak memory usage: 15 MB % 161.01/23.02 % (56836)Instructions burned: 319 (million) % 161.01/23.02 % (56838)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=684451367:i=1428:nm=2:rtra=on_2822 on theBenchmark for (2822ds/1428Mi) % 161.01/23.02 % (56838)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 161.01/23.02 % (56838)Terminated due to inappropriate strategy. % 161.01/23.02 % (56838)------------------------------ % 161.01/23.02 % (56838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.01/23.02 % (56838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.01/23.02 % (56838)CaDiCaL version: 2.1.3 % 161.01/23.02 % (56838)Termination reason: Inappropriate % 161.01/23.02 % (56838)Time elapsed: 0.001 s % 161.01/23.02 % (56838)Peak memory usage: 10 MB % 161.01/23.02 % (56838)Instructions burned: 2 (million) % 161.01/23.02 % (56838)------------------------------ % 161.01/23.02 % (56838)------------------------------ % 161.01/23.02 % (56840)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2976433170:i=262:bd=preordered:rtra=on:fsd=on_2822 on theBenchmark for (2822ds/262Mi) % 161.01/23.02 % (56840)Instruction limit reached! % 161.01/23.02 % (56840)------------------------------ % 161.01/23.02 % (56840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.01/23.02 % (56840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.01/23.02 % (56840)CaDiCaL version: 2.1.3 % 161.01/23.02 % (56840)Termination reason: Instruction limit % 161.01/23.02 % (56840)Termination phase: Saturation % 161.01/23.02 % (56840)Time elapsed: 0.166 s % 161.01/23.02 % (56840)Peak memory usage: 14 MB % 161.01/23.02 % (56840)Instructions burned: 264 (million) % 213.31/30.33 % (56842)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=3676202963:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2820 on theBenchmark for (2820ds/1368Mi) % 213.31/30.33 % (56842)Instruction limit reached! % 213.31/30.33 % (56842)------------------------------ % 213.31/30.33 % (56842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.31/30.33 % (56842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.31/30.33 % (56842)CaDiCaL version: 2.1.3 % 213.31/30.33 % (56842)Termination reason: Instruction limit % 213.31/30.33 % (56842)Termination phase: Saturation % 213.31/30.33 % (56842)Time elapsed: 0.739 s % 213.31/30.33 % (56842)Peak memory usage: 21 MB % 213.31/30.33 % (56842)Instructions burned: 1369 (million) % 213.31/30.33 % (56844)ott-21_1_sil=16000:si=on:fs=off:random_seed=3865484859:i=360:av=off:fsr=off:rtra=on_2813 on theBenchmark for (2813ds/360Mi) % 213.31/30.33 % (56844)Instruction limit reached! % 213.31/30.33 % (56844)------------------------------ % 213.31/30.33 % (56844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.31/30.33 % (56844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.31/30.33 % (56844)CaDiCaL version: 2.1.3 % 213.31/30.33 % (56844)Termination reason: Instruction limit % 213.31/30.33 % (56844)Termination phase: Saturation % 213.31/30.33 % (56844)Time elapsed: 0.160 s % 213.31/30.33 % (56844)Peak memory usage: 13 MB % 213.31/30.33 % (56844)Instructions burned: 361 (million) % 213.31/30.33 % (56846)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1973352064:i=954:bd=all:rtra=on_2811 on theBenchmark for (2811ds/954Mi) % 213.31/30.33 % (56846)Instruction limit reached! % 213.31/30.33 % (56846)------------------------------ % 213.31/30.33 % (56846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.31/30.33 % (56846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.31/30.33 % (56846)CaDiCaL version: 2.1.3 % 213.31/30.33 % (56846)Termination reason: Instruction limit % 213.31/30.33 % (56846)Termination phase: Saturation % 213.31/30.33 % (56846)Time elapsed: 0.582 s % 213.31/30.33 % (56846)Peak memory usage: 17 MB % 213.31/30.33 % (56846)Instructions burned: 955 (million) % 213.31/30.33 % (56848)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1952879969:fmbsr=1.3:i=1730:ins=25:rtra=on_2805 on theBenchmark for (2805ds/1730Mi) % 213.31/30.33 % (56848)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.31/30.33 % (56848)Terminated due to inappropriate strategy. % 213.31/30.33 % (56848)------------------------------ % 213.31/30.33 % (56848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.31/30.33 % (56848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.31/30.33 % (56848)CaDiCaL version: 2.1.3 % 213.31/30.33 % (56848)Termination reason: Inappropriate % 213.31/30.33 % (56848)Time elapsed: 0.001 s % 213.31/30.33 % (56848)Peak memory usage: 10 MB % 213.31/30.33 % (56848)Instructions burned: 2 (million) % 213.31/30.33 % (56848)------------------------------ % 213.31/30.33 % (56848)------------------------------ % 213.31/30.33 % (56850)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2646346735:i=2358:rtra=on_2805 on theBenchmark for (2805ds/2358Mi) % 213.31/30.33 % (56850)Instruction limit reached! % 213.31/30.33 % (56850)------------------------------ % 213.31/30.33 % (56850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.31/30.33 % (56850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.31/30.33 % (56850)CaDiCaL version: 2.1.3 % 213.31/30.33 % (56850)Termination reason: Instruction limit % 213.31/30.33 % (56850)Termination phase: Saturation % 213.31/30.33 % (56850)Time elapsed: 1.303 s % 213.31/30.33 % (56850)Peak memory usage: 23 MB % 213.31/30.33 % (56850)Instructions burned: 2358 (million) % 213.31/30.33 % (56852)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=571489298:i=1778:ins=1:rtra=on_2791 on theBenchmark for (2791ds/1778Mi) % 213.31/30.33 % (56852)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.31/30.33 % (56852)Terminated due to inappropriate strategy. % 213.31/30.33 % (56852)------------------------------ % 213.31/30.33 % (56852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.31/30.33 % (56852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.31/30.33 % (56852)CaDiCaL version: 2.1.3 % 213.31/30.33 % (56852)Termination reason: Inappropriate % 213.31/30.33 % (56852)Time elapsed: 0.001 s % 272.68/38.77 % (56852)Peak memory usage: 11 MB % 272.68/38.77 % (56852)Instructions burned: 2 (million) % 272.68/38.77 % (56852)------------------------------ % 272.68/38.77 % (56852)------------------------------ % 272.68/38.77 % (56854)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=1771168413:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2791 on theBenchmark for (2791ds/1384Mi) % 272.68/38.77 % (56854)Instruction limit reached! % 272.68/38.77 % (56854)------------------------------ % 272.68/38.77 % (56854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.68/38.77 % (56854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.68/38.77 % (56854)CaDiCaL version: 2.1.3 % 272.68/38.77 % (56854)Termination reason: Instruction limit % 272.68/38.77 % (56854)Termination phase: Saturation % 272.68/38.77 % (56854)Time elapsed: 0.838 s % 272.68/38.77 % (56854)Peak memory usage: 28 MB % 272.68/38.77 % (56854)Instructions burned: 1385 (million) % 272.68/38.77 % (56856)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=894120624:i=1758:kws=inv_precedence:fsr=off:rtra=on_2783 on theBenchmark for (2783ds/1758Mi) % 272.68/38.77 % (56856)Instruction limit reached! % 272.68/38.77 % (56856)------------------------------ % 272.68/38.77 % (56856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.68/38.77 % (56856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.68/38.77 % (56856)CaDiCaL version: 2.1.3 % 272.68/38.77 % (56856)Termination reason: Instruction limit % 272.68/38.77 % (56856)Termination phase: Saturation % 272.68/38.77 % (56856)Time elapsed: 1.002 s % 272.68/38.77 % (56856)Peak memory usage: 28 MB % 272.68/38.77 % (56856)Instructions burned: 1759 (million) % 272.68/38.77 % (56858)fmb+10_1_sil=64000:si=on:random_seed=2582713930:i=44122:nm=2:rtra=on:gsp=on_2772 on theBenchmark for (2772ds/44122Mi) % 272.68/38.77 % (56858)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.68/38.77 % (56858)Terminated due to inappropriate strategy. % 272.68/38.77 % (56858)------------------------------ % 272.68/38.77 % (56858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.68/38.77 % (56858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.68/38.77 % (56858)CaDiCaL version: 2.1.3 % 272.68/38.77 % (56858)Termination reason: Inappropriate % 272.68/38.77 % (56858)Time elapsed: 0.001 s % 272.68/38.77 % (56858)Peak memory usage: 10 MB % 272.68/38.77 % (56858)Instructions burned: 2 (million) % 272.68/38.77 % (56858)------------------------------ % 272.68/38.77 % (56858)------------------------------ % 272.68/38.77 % (56860)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=271986592:i=19030:nm=5:rtra=on_2772 on theBenchmark for (2772ds/19030Mi) % 272.68/38.77 % (56860)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.68/38.77 % (56860)Terminated due to inappropriate strategy. % 272.68/38.77 % (56860)------------------------------ % 272.68/38.77 % (56860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.68/38.77 % (56860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.68/38.77 % (56860)CaDiCaL version: 2.1.3 % 272.68/38.77 % (56860)Termination reason: Inappropriate % 272.68/38.77 % (56860)Time elapsed: 0.001 s % 272.68/38.77 % (56860)Peak memory usage: 10 MB % 272.68/38.77 % (56860)Instructions burned: 2 (million) % 272.68/38.77 % (56860)------------------------------ % 272.68/38.77 % (56860)------------------------------ % 272.68/38.77 % (56862)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1065974789:fmbsr=1.7:i=1840:rtra=on_2772 on theBenchmark for (2772ds/1840Mi) % 272.68/38.77 % (56862)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.68/38.77 % (56862)Terminated due to inappropriate strategy. % 272.68/38.77 % (56862)------------------------------ % 272.68/38.77 % (56862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.68/38.77 % (56862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.68/38.77 % (56862)CaDiCaL version: 2.1.3 % 272.68/38.77 % (56862)Termination reason: Inappropriate % 272.68/38.77 % (56862)Time elapsed: 0.001 s % 272.68/38.77 % (56862)Peak memory usage: 10 MB % 272.68/38.77 % (56862)Instructions burned: 2 (million) % 272.68/38.77 % (56862)------------------------------ % 272.68/38.77 % (56862)------------------------------ % 272.68/38.77 % (56864)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2233761261:i=10262:rTerminated % 300.13/42.54 % Vampire exiting %------------------------------------------------------------------------------