%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW644_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n004.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:35 PM UTC 2026 % Result : Timeout 300.19s 42.53s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW644_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.18 % Computer : n004.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 14:23:37 UTC 2026 % 0.08/0.18 % CPUTime : % 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.21 Running first-order model finding % 0.08/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.70/0.85 % (383656)Will run a generic schedule for satisfiability detection. % 3.70/0.85 % (383667)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3035561336:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.70/0.85 % (383664)dis+10_1_sil=32000:sp=arity:random_seed=3027013857:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.70/0.85 % (383661)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=760215786_2999 on theBenchmark for (2999ds/0Mi) % 3.70/0.85 % (383665)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=148433822:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.70/0.85 % (383663)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=516994317:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.70/0.85 % (383666)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=424107674:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.70/0.85 % (383662)% WARNING: option uhcvi not known. % 3.70/0.85 % (383662)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1611881155:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.70/0.85 % (383661)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.70/0.85 % (383661)Terminated due to inappropriate strategy. % 3.70/0.85 % (383661)------------------------------ % 3.70/0.85 % (383661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.70/0.85 % (383661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.70/0.85 % (383661)CaDiCaL version: 2.1.3 % 3.70/0.85 % (383661)Termination reason: Inappropriate % 3.70/0.85 % (383661)Time elapsed: 0.011 s % 3.70/0.85 % (383661)Peak memory usage: 11 MB % 3.70/0.85 % (383661)Instructions burned: 22 (million) % 3.70/0.85 % (383661)------------------------------ % 3.70/0.85 % (383661)------------------------------ % 3.70/0.85 % (383675)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1294189625:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.70/0.85 % (383675)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.70/0.85 % (383675)Terminated due to inappropriate strategy. % 3.70/0.85 % (383675)------------------------------ % 3.70/0.85 % (383675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.70/0.85 % (383675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.70/0.85 % (383675)CaDiCaL version: 2.1.3 % 3.70/0.85 % (383675)Termination reason: Inappropriate % 3.70/0.85 % (383675)Time elapsed: 0.007 s % 3.70/0.85 % (383675)Peak memory usage: 11 MB % 3.70/0.85 % (383675)Instructions burned: 14 (million) % 3.70/0.85 % (383675)------------------------------ % 3.70/0.85 % (383675)------------------------------ % 3.70/0.85 % (383667)Instruction limit reached! % 3.70/0.85 % (383667)------------------------------ % 3.70/0.85 % (383667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.70/0.85 % (383667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.70/0.85 % (383667)CaDiCaL version: 2.1.3 % 3.70/0.85 % (383667)Termination reason: Instruction limit % 3.70/0.85 % (383667)Termination phase: Saturation % 3.70/0.85 % (383667)Time elapsed: 0.059 s % 3.70/0.85 % (383667)Peak memory usage: 14 MB % 3.70/0.85 % (383667)Instructions burned: 159 (million) % 3.70/0.85 % (383677)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1072595926:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.70/0.85 % (383664)Instruction limit reached! % 3.70/0.85 % (383664)------------------------------ % 3.70/0.85 % (383664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.70/0.85 % (383664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.70/0.85 % (383664)CaDiCaL version: 2.1.3 % 3.70/0.85 % (383664)Termination reason: Instruction limit % 3.70/0.85 % (383664)Termination phase: Saturation % 3.70/0.85 % (383664)Time elapsed: 0.059 s % 3.70/0.85 % (383664)Peak memory usage: 12 MB % 3.70/0.85 % (383664)Instructions burned: 105 (million) % 3.70/0.85 % (383678)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=325762229:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.70/0.85 % (383665)Instruction limit reached! % 3.70/0.85 % (383665)------------------------------ % 3.70/0.85 % (383665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.05/1.41 % (383665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.05/1.41 % (383665)CaDiCaL version: 2.1.3 % 8.05/1.41 % (383665)Termination reason: Instruction limit % 8.05/1.41 % (383665)Termination phase: Saturation % 8.05/1.41 % (383665)Time elapsed: 0.066 s % 8.05/1.41 % (383665)Peak memory usage: 13 MB % 8.05/1.41 % (383665)Instructions burned: 117 (million) % 8.05/1.41 % (383681)ott-21_1_sil=16000:fs=off:random_seed=1630118497:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 8.05/1.41 % (383666)Instruction limit reached! % 8.05/1.41 % (383666)------------------------------ % 8.05/1.41 % (383666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.05/1.41 % (383666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.05/1.41 % (383666)CaDiCaL version: 2.1.3 % 8.05/1.41 % (383666)Termination reason: Instruction limit % 8.05/1.41 % (383666)Termination phase: Saturation % 8.05/1.41 % (383666)Time elapsed: 0.079 s % 8.05/1.41 % (383666)Peak memory usage: 13 MB % 8.05/1.41 % (383666)Instructions burned: 131 (million) % 8.05/1.41 % (383687)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2343633626:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 8.05/1.41 % (383690)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1726906183:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 8.05/1.41 % (383690)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.05/1.41 % (383690)Terminated due to inappropriate strategy. % 8.05/1.41 % (383690)------------------------------ % 8.05/1.41 % (383690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.05/1.41 % (383690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.05/1.41 % (383690)CaDiCaL version: 2.1.3 % 8.05/1.41 % (383690)Termination reason: Inappropriate % 8.05/1.41 % (383690)Time elapsed: 0.008 s % 8.05/1.41 % (383690)Peak memory usage: 10 MB % 8.05/1.41 % (383690)Instructions burned: 17 (million) % 8.05/1.41 % (383690)------------------------------ % 8.05/1.41 % (383690)------------------------------ % 8.05/1.41 % (383707)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3840297864:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 8.05/1.41 % (383677)Instruction limit reached! % 8.05/1.41 % (383677)------------------------------ % 8.05/1.41 % (383677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.05/1.41 % (383677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.05/1.41 % (383677)CaDiCaL version: 2.1.3 % 8.05/1.41 % (383677)Termination reason: Instruction limit % 8.05/1.41 % (383677)Termination phase: Saturation % 8.05/1.41 % (383677)Time elapsed: 0.081 s % 8.05/1.41 % (383677)Peak memory usage: 13 MB % 8.05/1.41 % (383677)Instructions burned: 132 (million) % 8.05/1.41 % (383729)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1901040238:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 8.05/1.41 % (383729)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.05/1.41 % (383729)Terminated due to inappropriate strategy. % 8.05/1.41 % (383729)------------------------------ % 8.05/1.41 % (383729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.05/1.41 % (383729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.05/1.41 % (383729)CaDiCaL version: 2.1.3 % 8.05/1.41 % (383729)Termination reason: Inappropriate % 8.05/1.41 % (383729)Time elapsed: 0.007 s % 8.05/1.41 % (383729)Peak memory usage: 10 MB % 8.05/1.41 % (383729)Instructions burned: 16 (million) % 8.05/1.41 % (383681)Instruction limit reached! % 8.05/1.41 % (383681)------------------------------ % 8.05/1.41 % (383681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.05/1.41 % (383681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.05/1.41 % (383681)CaDiCaL version: 2.1.3 % 8.05/1.41 % (383681)Termination reason: Instruction limit % 8.05/1.41 % (383681)Termination phase: Saturation % 8.05/1.41 % (383681)Time elapsed: 0.090 s % 8.05/1.41 % (383681)Peak memory usage: 12 MB % 8.05/1.41 % (383681)Instructions burned: 180 (million) % 8.05/1.41 % (383729)------------------------------ % 8.05/1.41 % (383729)------------------------------ % 8.05/1.41 % (383738)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=3458375656: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) % 21.60/3.33 % (383739)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1784938993:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 21.60/3.33 % (383678)Instruction limit reached! % 21.60/3.33 % (383678)------------------------------ % 21.60/3.33 % (383678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.60/3.33 % (383678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.60/3.33 % (383678)CaDiCaL version: 2.1.3 % 21.60/3.33 % (383678)Termination reason: Instruction limit % 21.60/3.33 % (383678)Termination phase: Saturation % 21.60/3.33 % (383678)Time elapsed: 0.192 s % 21.60/3.33 % (383678)Peak memory usage: 16 MB % 21.60/3.33 % (383678)Instructions burned: 689 (million) % 21.60/3.33 % (383742)fmb+10_1_sil=64000:random_seed=447367580:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 21.60/3.33 % (383742)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.60/3.33 % (383742)Terminated due to inappropriate strategy. % 21.60/3.33 % (383742)------------------------------ % 21.60/3.33 % (383742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.60/3.33 % (383742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.60/3.33 % (383742)CaDiCaL version: 2.1.3 % 21.60/3.33 % (383742)Termination reason: Inappropriate % 21.60/3.33 % (383742)Time elapsed: 0.004 s % 21.60/3.33 % (383742)Peak memory usage: 11 MB % 21.60/3.33 % (383742)Instructions burned: 15 (million) % 21.60/3.33 % (383742)------------------------------ % 21.60/3.33 % (383742)------------------------------ % 21.60/3.33 % (383744)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2199155408:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 21.60/3.33 % (383744)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.60/3.33 % (383744)Terminated due to inappropriate strategy. % 21.60/3.33 % (383744)------------------------------ % 21.60/3.33 % (383744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.60/3.33 % (383744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.60/3.33 % (383744)CaDiCaL version: 2.1.3 % 21.60/3.33 % (383744)Termination reason: Inappropriate % 21.60/3.33 % (383744)Time elapsed: 0.003 s % 21.60/3.33 % (383744)Peak memory usage: 11 MB % 21.60/3.33 % (383744)Instructions burned: 13 (million) % 21.60/3.33 % (383744)------------------------------ % 21.60/3.33 % (383744)------------------------------ % 21.60/3.33 % (383746)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4277442302:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 21.60/3.33 % (383746)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.60/3.33 % (383746)Terminated due to inappropriate strategy. % 21.60/3.33 % (383746)------------------------------ % 21.60/3.33 % (383746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.60/3.33 % (383746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.60/3.33 % (383746)CaDiCaL version: 2.1.3 % 21.60/3.33 % (383746)Termination reason: Inappropriate % 21.60/3.33 % (383746)Time elapsed: 0.004 s % 21.60/3.33 % (383746)Peak memory usage: 11 MB % 21.60/3.33 % (383746)Instructions burned: 15 (million) % 21.60/3.33 % (383746)------------------------------ % 21.60/3.33 % (383746)------------------------------ % 21.60/3.33 % (383748)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=986737117:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 21.60/3.33 % (383687)Instruction limit reached! % 21.60/3.33 % (383687)------------------------------ % 21.60/3.33 % (383687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.60/3.33 % (383687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.60/3.33 % (383687)CaDiCaL version: 2.1.3 % 21.60/3.33 % (383687)Termination reason: Instruction limit % 21.60/3.33 % (383687)Termination phase: Saturation % 21.60/3.33 % (383687)Time elapsed: 0.262 s % 21.60/3.33 % (383687)Peak memory usage: 13 MB % 21.60/3.33 % (383687)Instructions burned: 478 (million) % 21.60/3.33 % (383750)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=352540884:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 21.60/3.33 % (383738)Instruction limit reached! % 21.60/3.33 % (383738)------------------------------ % 21.60/3.33 % (383738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.60/3.33 % (383738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.70/3.59 % (383738)CaDiCaL version: 2.1.3 % 22.70/3.59 % (383738)Termination reason: Instruction limit % 22.70/3.59 % (383738)Termination phase: Saturation % 22.70/3.59 % (383738)Time elapsed: 0.415 s % 22.70/3.59 % (383738)Peak memory usage: 20 MB % 22.70/3.59 % (383738)Instructions burned: 694 (million) % 22.70/3.59 % (383752)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=968471388:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 22.70/3.59 % (383752)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.70/3.59 % (383752)Terminated due to inappropriate strategy. % 22.70/3.59 % (383752)------------------------------ % 22.70/3.59 % (383752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.70/3.59 % (383752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.70/3.59 % (383752)CaDiCaL version: 2.1.3 % 22.70/3.59 % (383752)Termination reason: Inappropriate % 22.70/3.59 % (383752)Time elapsed: 0.010 s % 22.70/3.59 % (383752)Peak memory usage: 11 MB % 22.70/3.59 % (383752)Instructions burned: 22 (million) % 22.70/3.59 % (383752)------------------------------ % 22.70/3.59 % (383752)------------------------------ % 22.70/3.59 % (383739)Instruction limit reached! % 22.70/3.59 % (383739)------------------------------ % 22.70/3.59 % (383739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.70/3.59 % (383739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.70/3.59 % (383739)CaDiCaL version: 2.1.3 % 22.70/3.59 % (383739)Termination reason: Instruction limit % 22.70/3.59 % (383739)Termination phase: Saturation % 22.70/3.59 % (383739)Time elapsed: 0.456 s % 22.70/3.59 % (383739)Peak memory usage: 17 MB % 22.70/3.59 % (383739)Instructions burned: 879 (million) % 22.70/3.59 % (383754)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=564872389:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 22.70/3.59 % (383754)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.70/3.59 % (383754)Terminated due to inappropriate strategy. % 22.70/3.59 % (383754)------------------------------ % 22.70/3.59 % (383754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.70/3.59 % (383754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.70/3.59 % (383754)CaDiCaL version: 2.1.3 % 22.70/3.59 % (383754)Termination reason: Inappropriate % 22.70/3.59 % (383754)Time elapsed: 0.007 s % 22.70/3.59 % (383754)Peak memory usage: 11 MB % 22.70/3.59 % (383754)Instructions burned: 15 (million) % 22.70/3.59 % (383754)------------------------------ % 22.70/3.59 % (383754)------------------------------ % 22.70/3.59 % (383755)ott-2_1_sil=16000:newcnf=on:random_seed=1653511467:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 22.70/3.59 % (383757)ott+10_1_sil=32000:tgt=ground:random_seed=1505544880:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 22.70/3.59 % (383707)Instruction limit reached! % 22.70/3.59 % (383707)------------------------------ % 22.70/3.59 % (383707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.70/3.59 % (383707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.70/3.59 % (383707)CaDiCaL version: 2.1.3 % 22.70/3.59 % (383707)Termination reason: Instruction limit % 22.70/3.59 % (383707)Termination phase: Saturation % 22.70/3.59 % (383707)Time elapsed: 0.644 s % 22.70/3.59 % (383707)Peak memory usage: 22 MB % 22.70/3.59 % (383707)Instructions burned: 1181 (million) % 22.70/3.59 % (383760)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=70287390:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 22.70/3.59 % (383760)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.70/3.59 % (383760)Terminated due to inappropriate strategy. % 22.70/3.59 % (383760)------------------------------ % 22.70/3.59 % (383760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.70/3.59 % (383760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.70/3.59 % (383760)CaDiCaL version: 2.1.3 % 22.70/3.59 % (383760)Termination reason: Inappropriate % 22.70/3.59 % (383760)Time elapsed: 0.010 s % 22.70/3.59 % (383760)Peak memory usage: 11 MB % 22.70/3.59 % (383760)Instructions burned: 22 (million) % 22.70/3.59 % (383760)------------------------------ % 22.70/3.59 % (383760)------------------------------ % 22.70/3.59 % (383762)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1782228828:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 22.70/3.59 % (383750)Instruction limit reached! % 92.88/13.30 % (383750)------------------------------ % 92.88/13.30 % (383750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.88/13.30 % (383750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.88/13.30 % (383750)CaDiCaL version: 2.1.3 % 92.88/13.30 % (383750)Termination reason: Instruction limit % 92.88/13.30 % (383750)Termination phase: Saturation % 92.88/13.30 % (383750)Time elapsed: 0.795 s % 92.88/13.30 % (383750)Peak memory usage: 21 MB % 92.88/13.30 % (383750)Instructions burned: 1473 (million) % 92.88/13.30 % (383755)Instruction limit reached! % 92.88/13.30 % (383755)------------------------------ % 92.88/13.30 % (383755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.88/13.30 % (383755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.88/13.30 % (383755)CaDiCaL version: 2.1.3 % 92.88/13.30 % (383755)Termination reason: Instruction limit % 92.88/13.30 % (383755)Termination phase: Saturation % 92.88/13.30 % (383755)Time elapsed: 0.501 s % 92.88/13.30 % (383755)Peak memory usage: 16 MB % 92.88/13.30 % (383755)Instructions burned: 870 (million) % 92.88/13.30 % (383764)dis+21_1_sil=32000:sas=cadical:random_seed=2049999327:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 92.88/13.30 % (383765)ott+11_1_sil=16000:gs=on:random_seed=2264768697:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 92.88/13.30 % (383748)Instruction limit reached! % 92.88/13.30 % (383748)------------------------------ % 92.88/13.30 % (383748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.88/13.30 % (383748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.88/13.30 % (383748)CaDiCaL version: 2.1.3 % 92.88/13.30 % (383748)Termination reason: Instruction limit % 92.88/13.30 % (383748)Termination phase: Saturation % 92.88/13.30 % (383748)Time elapsed: 1.439 s % 92.88/13.30 % (383748)Peak memory usage: 37 MB % 92.88/13.30 % (383748)Instructions burned: 5132 (million) % 92.88/13.30 % (383768)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=872421934:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 92.88/13.30 % (383768)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 92.88/13.30 % (383768)Terminated due to inappropriate strategy. % 92.88/13.30 % (383768)------------------------------ % 92.88/13.30 % (383768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.88/13.30 % (383768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.88/13.30 % (383768)CaDiCaL version: 2.1.3 % 92.88/13.30 % (383768)Termination reason: Inappropriate % 92.88/13.30 % (383768)Time elapsed: 0.004 s % 92.88/13.30 % (383768)Peak memory usage: 11 MB % 92.88/13.30 % (383768)Instructions burned: 16 (million) % 92.88/13.30 % (383768)------------------------------ % 92.88/13.30 % (383768)------------------------------ % 92.88/13.30 % (383770)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4049802367:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 92.88/13.30 % (383765)Instruction limit reached! % 92.88/13.30 % (383765)------------------------------ % 92.88/13.30 % (383765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.88/13.30 % (383765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.88/13.30 % (383765)CaDiCaL version: 2.1.3 % 92.88/13.30 % (383765)Termination reason: Instruction limit % 92.88/13.30 % (383765)Termination phase: Saturation % 92.88/13.30 % (383765)Time elapsed: 1.193 s % 92.88/13.30 % (383765)Peak memory usage: 25 MB % 92.88/13.30 % (383765)Instructions burned: 2252 (million) % 92.88/13.30 % (383772)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1912130192:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 92.88/13.30 % (383762)Instruction limit reached! % 92.88/13.30 % (383762)------------------------------ % 92.88/13.30 % (383762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.88/13.30 % (383762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.88/13.30 % (383762)CaDiCaL version: 2.1.3 % 92.88/13.30 % (383762)Termination reason: Instruction limit % 92.88/13.30 % (383762)Termination phase: Saturation % 92.88/13.30 % (383762)Time elapsed: 1.935 s % 92.88/13.30 % (383762)Peak memory usage: 29 MB % 92.88/13.30 % (383762)Instructions burned: 3514 (million) % 92.88/13.30 % (383774)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3409873100:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 92.88/13.30 % (383770)Instruction limit reached! % 113.28/16.17 % (383770)------------------------------ % 113.28/16.17 % (383770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.28/16.17 % (383770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.28/16.17 % (383770)CaDiCaL version: 2.1.3 % 113.28/16.17 % (383770)Termination reason: Instruction limit % 113.28/16.17 % (383770)Termination phase: Saturation % 113.28/16.17 % (383770)Time elapsed: 1.312 s % 113.28/16.17 % (383770)Peak memory usage: 42 MB % 113.28/16.17 % (383770)Instructions burned: 4596 (million) % 113.28/16.17 % (383776)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2489741212:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 113.28/16.17 % (383776)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.28/16.17 % (383776)Terminated due to inappropriate strategy. % 113.28/16.17 % (383776)------------------------------ % 113.28/16.17 % (383776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.28/16.17 % (383776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.28/16.17 % (383776)CaDiCaL version: 2.1.3 % 113.28/16.17 % (383776)Termination reason: Inappropriate % 113.28/16.17 % (383776)Time elapsed: 0.005 s % 113.28/16.17 % (383776)Peak memory usage: 11 MB % 113.28/16.17 % (383776)Instructions burned: 18 (million) % 113.28/16.17 % (383776)------------------------------ % 113.28/16.17 % (383776)------------------------------ % 113.28/16.17 % (383778)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3795524369:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 113.28/16.17 % (383778)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.28/16.17 % (383778)Terminated due to inappropriate strategy. % 113.28/16.17 % (383778)------------------------------ % 113.28/16.17 % (383778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.28/16.17 % (383778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.28/16.17 % (383778)CaDiCaL version: 2.1.3 % 113.28/16.17 % (383778)Termination reason: Inappropriate % 113.28/16.17 % (383778)Time elapsed: 0.004 s % 113.28/16.17 % (383778)Peak memory usage: 11 MB % 113.28/16.17 % (383778)Instructions burned: 16 (million) % 113.28/16.17 % (383778)------------------------------ % 113.28/16.17 % (383778)------------------------------ % 113.28/16.17 % (383780)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=815623452:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 113.28/16.17 % (383780)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.28/16.17 % (383780)Terminated due to inappropriate strategy. % 113.28/16.17 % (383780)------------------------------ % 113.28/16.17 % (383780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.28/16.17 % (383780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.28/16.17 % (383780)CaDiCaL version: 2.1.3 % 113.28/16.17 % (383780)Termination reason: Inappropriate % 113.28/16.17 % (383780)Time elapsed: 0.004 s % 113.28/16.17 % (383780)Peak memory usage: 11 MB % 113.28/16.17 % (383780)Instructions burned: 16 (million) % 113.28/16.17 % (383780)------------------------------ % 113.28/16.17 % (383780)------------------------------ % 113.28/16.17 % (383782)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1559862213:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 113.28/16.17 % (383764)Instruction limit reached! % 113.28/16.17 % (383764)------------------------------ % 113.28/16.17 % (383764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.28/16.17 % (383764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.28/16.17 % (383764)CaDiCaL version: 2.1.3 % 113.28/16.17 % (383764)Termination reason: Instruction limit % 113.28/16.17 % (383764)Termination phase: Saturation % 113.28/16.17 % (383764)Time elapsed: 2.091 s % 113.28/16.17 % (383764)Peak memory usage: 33 MB % 113.28/16.17 % (383764)Instructions burned: 3773 (million) % 113.28/16.17 % (383784)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=499019008:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 113.28/16.17 % (383757)Instruction limit reached! % 113.28/16.17 % (383757)------------------------------ % 113.28/16.17 % (383757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.28/16.17 % (383757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.28/16.17 % (383757)CaDiCaL version: 2.1.3 % 113.28/16.17 % (383757)Termination reason: Instruction limit % 113.28/16.17 % (383757)Termination phase: Saturation % 132.66/18.91 % (383757)Time elapsed: 2.668 s % 132.66/18.91 % (383757)Peak memory usage: 40 MB % 132.66/18.91 % (383757)Instructions burned: 5115 (million) % 132.66/18.91 % (383786)dis+10_16:1_sil=16000:random_seed=2271795191:i=9155:fsr=off_2966 on theBenchmark for (2966ds/9155Mi) % 132.66/18.91 % (383774)Instruction limit reached! % 132.66/18.91 % (383774)------------------------------ % 132.66/18.91 % (383774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.66/18.91 % (383774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.66/18.91 % (383774)CaDiCaL version: 2.1.3 % 132.66/18.91 % (383774)Termination reason: Instruction limit % 132.66/18.91 % (383774)Termination phase: Saturation % 132.66/18.91 % (383774)Time elapsed: 2.680 s % 132.66/18.91 % (383774)Peak memory usage: 57 MB % 132.66/18.91 % (383774)Instructions burned: 5213 (million) % 132.66/18.91 % (383788)ott-3_8_sil=64000:random_seed=1196183269:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi) % 132.66/18.91 % (383786)Instruction limit reached! % 132.66/18.91 % (383786)------------------------------ % 132.66/18.91 % (383786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.66/18.91 % (383786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.66/18.91 % (383786)CaDiCaL version: 2.1.3 % 132.66/18.91 % (383786)Termination reason: Instruction limit % 132.66/18.91 % (383786)Termination phase: Saturation % 132.66/18.91 % (383786)Time elapsed: 4.639 s % 132.66/18.91 % (383786)Peak memory usage: 52 MB % 132.66/18.91 % (383786)Instructions burned: 9156 (million) % 132.66/18.91 % (383790)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1046186094:fmbsr=2:i=32576_2919 on theBenchmark for (2919ds/32576Mi) % 132.66/18.91 % (383790)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.66/18.91 % (383790)Terminated due to inappropriate strategy. % 132.66/18.91 % (383790)------------------------------ % 132.66/18.91 % (383790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.66/18.91 % (383790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.66/18.91 % (383790)CaDiCaL version: 2.1.3 % 132.66/18.91 % (383790)Termination reason: Inappropriate % 132.66/18.91 % (383790)Time elapsed: 0.011 s % 132.66/18.91 % (383790)Peak memory usage: 11 MB % 132.66/18.91 % (383790)Instructions burned: 22 (million) % 132.66/18.91 % (383790)------------------------------ % 132.66/18.91 % (383790)------------------------------ % 132.66/18.91 % (383792)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=235893928:i=11404_2919 on theBenchmark for (2919ds/11404Mi) % 132.66/18.91 % (383782)Instruction limit reached! % 132.66/18.91 % (383782)------------------------------ % 132.66/18.91 % (383782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.66/18.91 % (383782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.66/18.91 % (383782)CaDiCaL version: 2.1.3 % 132.66/18.91 % (383782)Termination reason: Instruction limit % 132.66/18.91 % (383782)Termination phase: Saturation % 132.66/18.91 % (383782)Time elapsed: 5.011 s % 132.66/18.91 % (383782)Peak memory usage: 81 MB % 132.66/18.91 % (383782)Instructions burned: 22568 (million) % 132.66/18.91 % (383794)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=836252940:i=14134_2918 on theBenchmark for (2918ds/14134Mi) % 132.66/18.91 % (383784)Instruction limit reached! % 132.66/18.91 % (383784)------------------------------ % 132.66/18.91 % (383784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.66/18.91 % (383784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.66/18.91 % (383784)CaDiCaL version: 2.1.3 % 132.66/18.91 % (383784)Termination reason: Instruction limit % 132.66/18.91 % (383784)Termination phase: Saturation % 132.66/18.91 % (383784)Time elapsed: 5.132 s % 132.66/18.91 % (383784)Peak memory usage: 54 MB % 132.66/18.91 % (383784)Instructions burned: 8174 (million) % 132.66/18.91 % (383796)dis+33_16_sil=32000:sac=on:random_seed=3680648508:i=15851:nm=0_2915 on theBenchmark for (2915ds/15851Mi) % 132.66/18.91 % (383794)Instruction limit reached! % 132.66/18.91 % (383794)------------------------------ % 132.66/18.91 % (383794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.66/18.91 % (383794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.66/18.91 % (383794)CaDiCaL version: 2.1.3 % 132.66/18.91 % (383794)Termination reason: Instruction limit % 132.66/18.91 % (383794)Termination phase: Saturation % 132.66/18.91 % (383794)Time elapsed: 4.864 s % 132.66/18.91 % (383794)Peak memory usage: 66 MB % 132.66/18.91 % (383794)Instructions burned: 14135 (million) % 132.66/18.91 % (383798)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=933862596:avsq=on:i=17627:add=on:amm=off_2869 on theBenchmark for (2869ds/17627Mi) % 139.63/20.03 % (383772)Instruction limit reached! % 139.63/20.03 % (383772)------------------------------ % 139.63/20.03 % (383772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.63/20.03 % (383772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.63/20.03 % (383772)CaDiCaL version: 2.1.3 % 139.63/20.03 % (383772)Termination reason: Instruction limit % 139.63/20.03 % (383772)Termination phase: Saturation % 139.63/20.03 % (383772)Time elapsed: 11.911 s % 139.63/20.03 % (383772)Peak memory usage: 170 MB % 139.63/20.03 % (383772)Instructions burned: 29341 (million) % 139.63/20.03 % (384046)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2764421159:s2a=on:i=53295_2856 on theBenchmark for (2856ds/53295Mi) % 139.63/20.03 % (383792)Instruction limit reached! % 139.63/20.03 % (383792)------------------------------ % 139.63/20.03 % (383792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.63/20.03 % (383792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.63/20.03 % (383792)CaDiCaL version: 2.1.3 % 139.63/20.03 % (383792)Termination reason: Instruction limit % 139.63/20.03 % (383792)Termination phase: Saturation % 139.63/20.03 % (383792)Time elapsed: 7.400 s % 139.63/20.03 % (383792)Peak memory usage: 63 MB % 139.63/20.03 % (383792)Instructions burned: 11405 (million) % 139.63/20.03 % (384081)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4006866708:i=26857:ins=20_2845 on theBenchmark for (2845ds/26857Mi) % 139.63/20.03 % (384081)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 139.63/20.03 % (384081)Terminated due to inappropriate strategy. % 139.63/20.03 % (384081)------------------------------ % 139.63/20.03 % (384081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.63/20.03 % (384081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.63/20.03 % (384081)CaDiCaL version: 2.1.3 % 139.63/20.03 % (384081)Termination reason: Inappropriate % 139.63/20.03 % (384081)Time elapsed: 0.008 s % 139.63/20.03 % (384081)Peak memory usage: 11 MB % 139.63/20.03 % (384081)Instructions burned: 15 (million) % 139.63/20.03 % (384081)------------------------------ % 139.63/20.03 % (384081)------------------------------ % 139.63/20.03 % (384084)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4277569020:i=28120:bs=on:fsr=off_2844 on theBenchmark for (2844ds/28120Mi) % 139.63/20.03 % (383796)Instruction limit reached! % 139.63/20.03 % (383796)------------------------------ % 139.63/20.03 % (383796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.63/20.03 % (383796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.63/20.03 % (383796)CaDiCaL version: 2.1.3 % 139.63/20.03 % (383796)Termination reason: Instruction limit % 139.63/20.03 % (383796)Termination phase: Saturation % 139.63/20.03 % (383796)Time elapsed: 7.399 s % 139.63/20.03 % (383796)Peak memory usage: 195 MB % 139.63/20.03 % (383796)Instructions burned: 15851 (million) % 139.63/20.03 % (384105)fmb+10_1_sil=256000:fmbss=7:random_seed=3546944506:fmbsr=1.6:i=182295_2840 on theBenchmark for (2840ds/182295Mi) % 139.63/20.03 % (384105)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 139.63/20.03 % (384105)Terminated due to inappropriate strategy. % 139.63/20.03 % (384105)------------------------------ % 139.63/20.03 % (384105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.63/20.03 % (384105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.63/20.03 % (384105)CaDiCaL version: 2.1.3 % 139.63/20.03 % (384105)Termination reason: Inappropriate % 139.63/20.03 % (384105)Time elapsed: 0.004 s % 139.63/20.03 % (384105)Peak memory usage: 11 MB % 139.63/20.03 % (384105)Instructions burned: 15 (million) % 139.63/20.03 % (384105)------------------------------ % 139.63/20.03 % (384105)------------------------------ % 139.63/20.03 % (384108)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3614273792:i=44625:gsp=on_2840 on theBenchmark for (2840ds/44625Mi) % 139.63/20.03 % (384108)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 139.63/20.03 % (384108)Terminated due to inappropriate strategy. % 139.63/20.03 % (384108)------------------------------ % 139.63/20.03 % (384108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.63/20.03 % (384108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.63/20.03 % (384108)CaDiCaL version: 2.1.3 % 139.63/20.03 % (384108)Termination reason: Inappropriate % 161.07/22.95 % (384108)Time elapsed: 0.005 s % 161.07/22.95 % (384108)Peak memory usage: 11 MB % 161.07/22.95 % (384108)Instructions burned: 23 (million) % 161.07/22.95 % (384108)------------------------------ % 161.07/22.95 % (384108)------------------------------ % 161.07/22.95 % (384110)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2145660856:i=160505_2840 on theBenchmark for (2840ds/160505Mi) % 161.07/22.95 % (384110)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 161.07/22.95 % (384110)Terminated due to inappropriate strategy. % 161.07/22.95 % (384110)------------------------------ % 161.07/22.95 % (384110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.07/22.95 % (384110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.07/22.95 % (384110)CaDiCaL version: 2.1.3 % 161.07/22.95 % (384110)Termination reason: Inappropriate % 161.07/22.95 % (384110)Time elapsed: 0.004 s % 161.07/22.95 % (384110)Peak memory usage: 11 MB % 161.07/22.95 % (384110)Instructions burned: 15 (million) % 161.07/22.95 % (384110)------------------------------ % 161.07/22.95 % (384110)------------------------------ % 161.07/22.95 % (384112)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1152464388:fmbsr=1.3:i=225729_2840 on theBenchmark for (2840ds/225729Mi) % 161.07/22.95 % (384112)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 161.07/22.95 % (384112)Terminated due to inappropriate strategy. % 161.07/22.95 % (384112)------------------------------ % 161.07/22.95 % (384112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.07/22.95 % (384112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.07/22.95 % (384112)CaDiCaL version: 2.1.3 % 161.07/22.95 % (384112)Termination reason: Inappropriate % 161.07/22.95 % (384112)Time elapsed: 0.004 s % 161.07/22.95 % (384112)Peak memory usage: 11 MB % 161.07/22.95 % (384112)Instructions burned: 16 (million) % 161.07/22.95 % (384112)------------------------------ % 161.07/22.95 % (384112)------------------------------ % 161.07/22.95 % (384116)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3336507352:fmbsr=2:i=185024:ins=7_2840 on theBenchmark for (2840ds/185024Mi) % 161.07/22.95 % (384116)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 161.07/22.95 % (384116)Terminated due to inappropriate strategy. % 161.07/22.95 % (384116)------------------------------ % 161.07/22.95 % (384116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.07/22.95 % (384116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.07/22.95 % (384116)CaDiCaL version: 2.1.3 % 161.07/22.95 % (384116)Termination reason: Inappropriate % 161.07/22.95 % (384116)Time elapsed: 0.007 s % 161.07/22.95 % (384116)Peak memory usage: 11 MB % 161.07/22.95 % (384116)Instructions burned: 16 (million) % 161.07/22.95 % (384116)------------------------------ % 161.07/22.95 % (384116)------------------------------ % 161.07/22.95 % (384119)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=777193450:rtra=on_2839 on theBenchmark for (2839ds/0Mi) % 161.07/22.95 % (384119)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 161.07/22.95 % (384119)Terminated due to inappropriate strategy. % 161.07/22.95 % (384119)------------------------------ % 161.07/22.95 % (384119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.07/22.95 % (384119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.07/22.95 % (384119)CaDiCaL version: 2.1.3 % 161.07/22.95 % (384119)Termination reason: Inappropriate % 161.07/22.95 % (384119)Time elapsed: 0.017 s % 161.07/22.95 % (384119)Peak memory usage: 11 MB % 161.07/22.95 % (384119)Instructions burned: 21 (million) % 161.07/22.95 % (384119)------------------------------ % 161.07/22.95 % (384119)------------------------------ % 161.07/22.95 % (384123)% WARNING: option uhcvi not known. % 161.07/22.95 % (384123)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1487098032:i=271062:add=off:rtra=on:rawr=on_2839 on theBenchmark for (2839ds/271062Mi) % 161.07/22.95 % (383798)Instruction limit reached! % 161.07/22.95 % (383798)------------------------------ % 161.07/22.95 % (383798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.07/22.95 % (383798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.07/22.95 % (383798)CaDiCaL version: 2.1.3 % 161.07/22.95 % (383798)Termination reason: Instruction limit % 161.07/22.95 % (383798)Termination phase: Saturation % 161.07/22.95 % (383798)Time elapsed: 5.611 s % 161.07/22.95 % (383798)Peak memory usage: 233 MB % 161.07/22.95 % (383798)Instructions burned: 17629 (million) % 174.54/24.88 % (384319)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2809009180:i=176048:add=on:rtra=on:rawr=on_2812 on theBenchmark for (2812ds/176048Mi) % 174.54/24.88 % (383788)Instruction limit reached! % 174.54/24.88 % (383788)------------------------------ % 174.54/24.88 % (383788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.54/24.88 % (383788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.54/24.88 % (383788)CaDiCaL version: 2.1.3 % 174.54/24.88 % (383788)Termination reason: Instruction limit % 174.54/24.88 % (383788)Termination phase: Saturation % 174.54/24.88 % (383788)Time elapsed: 13.561 s % 174.54/24.88 % (383788)Peak memory usage: 80 MB % 174.54/24.88 % (383788)Instructions burned: 20139 (million) % 174.54/24.88 % (384321)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2255549806:i=206:fgj=on:rtra=on_2809 on theBenchmark for (2809ds/206Mi) % 174.54/24.88 % (384321)Instruction limit reached! % 174.54/24.88 % (384321)------------------------------ % 174.54/24.88 % (384321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.54/24.88 % (384321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.54/24.88 % (384321)CaDiCaL version: 2.1.3 % 174.54/24.88 % (384321)Termination reason: Instruction limit % 174.54/24.88 % (384321)Termination phase: Saturation % 174.54/24.88 % (384321)Time elapsed: 0.118 s % 174.54/24.88 % (384321)Peak memory usage: 13 MB % 174.54/24.88 % (384321)Instructions burned: 206 (million) % 174.54/24.88 % (384323)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1153693808:i=232:rtra=on_2807 on theBenchmark for (2807ds/232Mi) % 174.54/24.88 % (384323)Instruction limit reached! % 174.54/24.88 % (384323)------------------------------ % 174.54/24.88 % (384323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.54/24.88 % (384323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.54/24.88 % (384323)CaDiCaL version: 2.1.3 % 174.54/24.88 % (384323)Termination reason: Instruction limit % 174.54/24.88 % (384323)Termination phase: Saturation % 174.54/24.88 % (384323)Time elapsed: 0.138 s % 174.54/24.88 % (384323)Peak memory usage: 14 MB % 174.54/24.88 % (384323)Instructions burned: 232 (million) % 174.54/24.88 % (384325)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2888896471:i=262:rtra=on_2806 on theBenchmark for (2806ds/262Mi) % 174.54/24.88 % (384325)Instruction limit reached! % 174.54/24.88 % (384325)------------------------------ % 174.54/24.88 % (384325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.54/24.88 % (384325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.54/24.88 % (384325)CaDiCaL version: 2.1.3 % 174.54/24.88 % (384325)Termination reason: Instruction limit % 174.54/24.88 % (384325)Termination phase: Saturation % 174.54/24.88 % (384325)Time elapsed: 0.156 s % 174.54/24.88 % (384325)Peak memory usage: 14 MB % 174.54/24.88 % (384325)Instructions burned: 263 (million) % 174.54/24.88 % (384327)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3813893184:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2804 on theBenchmark for (2804ds/318Mi) % 174.54/24.88 % (384327)Instruction limit reached! % 174.54/24.88 % (384327)------------------------------ % 174.54/24.88 % (384327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.54/24.88 % (384327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.54/24.88 % (384327)CaDiCaL version: 2.1.3 % 174.54/24.88 % (384327)Termination reason: Instruction limit % 174.54/24.88 % (384327)Termination phase: Saturation % 174.54/24.88 % (384327)Time elapsed: 0.213 s % 174.54/24.88 % (384327)Peak memory usage: 15 MB % 174.54/24.88 % (384327)Instructions burned: 318 (million) % 174.54/24.88 % (384329)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1156224928:i=1428:nm=2:rtra=on_2802 on theBenchmark for (2802ds/1428Mi) % 174.54/24.88 % (384329)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 174.54/24.88 % (384329)Terminated due to inappropriate strategy. % 174.54/24.88 % (384329)------------------------------ % 174.54/24.88 % (384329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.54/24.88 % (384329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.54/24.88 % (384329)CaDiCaL version: 2.1.3 % 174.54/24.88 % (384329)Termination reason: Inappropriate % 174.54/24.88 % (384329)Time elapsed: 0.008 s % 174.54/24.88 % (384329)Peak memory usage: 11 MB % 174.54/24.88 % (384329)Instructions burned: 14 (million) % 174.54/24.88 % (384329)------------------------------ % 222.81/31.60 % (384329)------------------------------ % 222.81/31.60 % (384331)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3344645702:i=262:bd=preordered:rtra=on:fsd=on_2801 on theBenchmark for (2801ds/262Mi) % 222.81/31.60 % (384331)Instruction limit reached! % 222.81/31.60 % (384331)------------------------------ % 222.81/31.60 % (384331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.81/31.60 % (384331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.81/31.60 % (384331)CaDiCaL version: 2.1.3 % 222.81/31.60 % (384331)Termination reason: Instruction limit % 222.81/31.60 % (384331)Termination phase: Saturation % 222.81/31.60 % (384331)Time elapsed: 0.170 s % 222.81/31.60 % (384331)Peak memory usage: 15 MB % 222.81/31.60 % (384331)Instructions burned: 263 (million) % 222.81/31.60 % (384333)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=2403790782:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2799 on theBenchmark for (2799ds/1368Mi) % 222.81/31.60 % (384333)Instruction limit reached! % 222.81/31.60 % (384333)------------------------------ % 222.81/31.60 % (384333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.81/31.60 % (384333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.81/31.60 % (384333)CaDiCaL version: 2.1.3 % 222.81/31.60 % (384333)Termination reason: Instruction limit % 222.81/31.60 % (384333)Termination phase: Saturation % 222.81/31.60 % (384333)Time elapsed: 0.692 s % 222.81/31.60 % (384333)Peak memory usage: 20 MB % 222.81/31.60 % (384333)Instructions burned: 1369 (million) % 222.81/31.60 % (384335)ott-21_1_sil=16000:si=on:fs=off:random_seed=2069631747:i=360:av=off:fsr=off:rtra=on_2792 on theBenchmark for (2792ds/360Mi) % 222.81/31.60 % (384335)Instruction limit reached! % 222.81/31.60 % (384335)------------------------------ % 222.81/31.60 % (384335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.81/31.60 % (384335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.81/31.60 % (384335)CaDiCaL version: 2.1.3 % 222.81/31.60 % (384335)Termination reason: Instruction limit % 222.81/31.60 % (384335)Termination phase: Saturation % 222.81/31.60 % (384335)Time elapsed: 0.169 s % 222.81/31.60 % (384335)Peak memory usage: 13 MB % 222.81/31.60 % (384335)Instructions burned: 361 (million) % 222.81/31.60 % (384338)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1800929101:i=954:bd=all:rtra=on_2790 on theBenchmark for (2790ds/954Mi) % 222.81/31.60 % (384338)Instruction limit reached! % 222.81/31.60 % (384338)------------------------------ % 222.81/31.60 % (384338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.81/31.60 % (384338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.81/31.60 % (384338)CaDiCaL version: 2.1.3 % 222.81/31.60 % (384338)Termination reason: Instruction limit % 222.81/31.60 % (384338)Termination phase: Saturation % 222.81/31.60 % (384338)Time elapsed: 0.499 s % 222.81/31.60 % (384338)Peak memory usage: 14 MB % 222.81/31.60 % (384338)Instructions burned: 954 (million) % 222.81/31.60 % (384340)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1477748701:fmbsr=1.3:i=1730:ins=25:rtra=on_2785 on theBenchmark for (2785ds/1730Mi) % 222.81/31.60 % (384340)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.81/31.60 % (384340)Terminated due to inappropriate strategy. % 222.81/31.60 % (384340)------------------------------ % 222.81/31.60 % (384340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.81/31.60 % (384340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.81/31.60 % (384340)CaDiCaL version: 2.1.3 % 222.81/31.60 % (384340)Termination reason: Inappropriate % 222.81/31.60 % (384340)Time elapsed: 0.009 s % 222.81/31.60 % (384340)Peak memory usage: 10 MB % 222.81/31.60 % (384340)Instructions burned: 18 (million) % 222.81/31.60 % (384340)------------------------------ % 222.81/31.60 % (384340)------------------------------ % 222.81/31.60 % (384342)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2102817921:i=2358:rtra=on_2785 on theBenchmark for (2785ds/2358Mi) % 222.81/31.60 % (384342)Instruction limit reached! % 222.81/31.60 % (384342)------------------------------ % 222.81/31.60 % (384342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.81/31.60 % (384342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.81/31.60 % (384342)CaDiCaL version: 2.1.3 % 222.81/31.60 % (384342)Termination reason: Instruction limit % 222.81/31.60 % (384342)Termination phase: Saturation % 264.69/37.56 % (384342)Time elapsed: 1.257 s % 264.69/37.56 % (384342)Peak memory usage: 25 MB % 264.69/37.56 % (384342)Instructions burned: 2359 (million) % 264.69/37.56 % (384344)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1644847794:i=1778:ins=1:rtra=on_2772 on theBenchmark for (2772ds/1778Mi) % 264.69/37.56 % (384344)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 264.69/37.56 % (384344)Terminated due to inappropriate strategy. % 264.69/37.56 % (384344)------------------------------ % 264.69/37.56 % (384344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.69/37.56 % (384344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.69/37.56 % (384344)CaDiCaL version: 2.1.3 % 264.69/37.56 % (384344)Termination reason: Inappropriate % 264.69/37.56 % (384344)Time elapsed: 0.008 s % 264.69/37.56 % (384344)Peak memory usage: 10 MB % 264.69/37.56 % (384344)Instructions burned: 16 (million) % 264.69/37.56 % (384344)------------------------------ % 264.69/37.56 % (384344)------------------------------ % 264.69/37.56 % (384346)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=249209037:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2772 on theBenchmark for (2772ds/1384Mi) % 264.69/37.56 % (384346)Instruction limit reached! % 264.69/37.56 % (384346)------------------------------ % 264.69/37.56 % (384346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.69/37.56 % (384346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.69/37.56 % (384346)CaDiCaL version: 2.1.3 % 264.69/37.56 % (384346)Termination reason: Instruction limit % 264.69/37.56 % (384346)Termination phase: Saturation % 264.69/37.56 % (384346)Time elapsed: 0.824 s % 264.69/37.56 % (384346)Peak memory usage: 25 MB % 264.69/37.56 % (384346)Instructions burned: 1385 (million) % 264.69/37.56 % (384348)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1183847201:i=1758:kws=inv_precedence:fsr=off:rtra=on_2763 on theBenchmark for (2763ds/1758Mi) % 264.69/37.56 % (384348)Instruction limit reached! % 264.69/37.56 % (384348)------------------------------ % 264.69/37.56 % (384348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.69/37.56 % (384348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.69/37.56 % (384348)CaDiCaL version: 2.1.3 % 264.69/37.56 % (384348)Termination reason: Instruction limit % 264.69/37.56 % (384348)Termination phase: Saturation % 264.69/37.56 % (384348)Time elapsed: 0.959 s % 264.69/37.56 % (384348)Peak memory usage: 22 MB % 264.69/37.56 % (384348)Instructions burned: 1760 (million) % 264.69/37.56 % (384350)fmb+10_1_sil=64000:si=on:random_seed=2307535271:i=44122:nm=2:rtra=on:gsp=on_2754 on theBenchmark for (2754ds/44122Mi) % 264.69/37.56 % (384350)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 264.69/37.56 % (384350)Terminated due to inappropriate strategy. % 264.69/37.56 % (384350)------------------------------ % 264.69/37.56 % (384350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.69/37.56 % (384350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.69/37.56 % (384350)CaDiCaL version: 2.1.3 % 264.69/37.56 % (384350)Termination reason: Inappropriate % 264.69/37.56 % (384350)Time elapsed: 0.008 s % 264.69/37.56 % (384350)Peak memory usage: 11 MB % 264.69/37.56 % (384350)Instructions burned: 16 (million) % 264.69/37.56 % (384350)------------------------------ % 264.69/37.56 % (384350)------------------------------ % 264.69/37.56 % (384352)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3116186270:i=19030:nm=5:rtra=on_2753 on theBenchmark for (2753ds/19030Mi) % 264.69/37.56 % (384352)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 264.69/37.56 % (384352)Terminated due to inappropriate strategy. % 264.69/37.56 % (384352)------------------------------ % 264.69/37.56 % (384352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.69/37.56 % (384352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.69/37.56 % (384352)CaDiCaL version: 2.1.3 % 264.69/37.56 % (384352)Termination reason: Inappropriate % 264.69/37.56 % (384352)Time elapsed: 0.007 s % 264.69/37.56 % (384352)Peak memory usage: 11 MB % 264.69/37.56 % (384352)Instructions burned: 14 (million) % 264.69/37.56 % (384352)------------------------------ % 264.69/37.56 % (384352)------------------------------ % 264.69/37.56 % (384354)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2543697130:fmbsr=1.7:i=1840:rtra=on_2753 on theBenchmark for (2753ds/1840Mi) % 282.62/40.03 % (384354)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 282.62/40.03 % (384354)Terminated due to inappropriate strategy. % 282.62/40.03 % (384354)------------------------------ % 282.62/40.03 % (384354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.62/40.03 % (384354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.62/40.03 % (384354)CaDiCaL version: 2.1.3 % 282.62/40.03 % (384354)Termination reason: Inappropriate % 282.62/40.03 % (384354)Time elapsed: 0.008 s % 282.62/40.03 % (384354)Peak memory usage: 11 MB % 282.62/40.03 % (384354)Instructions burned: 16 (million) % 282.62/40.03 % (384354)------------------------------ % 282.62/40.03 % (384354)------------------------------ % 282.62/40.03 % (384356)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3796108573:i=10262:rtra=on_2753 on theBenchmark for (2753ds/10262Mi) % 282.62/40.03 % (384084)Instruction limit reached! % 282.62/40.03 % (384084)------------------------------ % 282.62/40.03 % (384084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.62/40.03 % (384084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.62/40.03 % (384084)CaDiCaL version: 2.1.3 % 282.62/40.03 % (384084)Termination reason: Instruction limit % 282.62/40.03 % (384084)Termination phase: Saturation % 282.62/40.03 % (384084)Time elapsed: 14.981 s % 282.62/40.03 % (384084)Peak memory usage: 31 MB % 282.62/40.03 % (384084)Instructions burned: 28120 (million) % 282.62/40.03 % (384701)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1857707339:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2694 on theBenchmark for (2694ds/2944Mi) % 282.62/40.03 % (384356)Instruction limit reached! % 282.62/40.03 % (384356)------------------------------ % 282.62/40.03 % (384356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.62/40.03 % (384356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.62/40.03 % (384356)CaDiCaL version: 2.1.3 % 282.62/40.03 % (384356)Termination reason: Instruction limit % 282.62/40.03 % (384356)Termination phase: Saturation % 282.62/40.03 % (384356)Time elapsed: 5.940 s % 282.62/40.03 % (384356)Peak memory usage: 59 MB % 282.62/40.03 % (384356)Instructions burned: 10263 (million) % 282.62/40.03 % (384703)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=90179943:i=12648:rtra=on_2693 on theBenchmark for (2693ds/12648Mi) % 282.62/40.03 % (384703)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 282.62/40.03 % (384703)Terminated due to inappropriate strategy. % 282.62/40.03 % (384703)------------------------------ % 282.62/40.03 % (384703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.62/40.03 % (384703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.62/40.03 % (384703)CaDiCaL version: 2.1.3 % 282.62/40.03 % (384703)Termination reason: Inappropriate % 282.62/40.03 % (384703)Time elapsed: 0.011 s % 282.62/40.03 % (384703)Peak memory usage: 11 MB % 282.62/40.03 % (384703)Instructions burned: 22 (million) % 282.62/40.03 % (384703)------------------------------ % 282.62/40.03 % (384703)------------------------------ % 282.62/40.03 % (384705)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3037943364:fmbsr=2.30978:i=4348:rtra=on_2693 on theBenchmark for (2693ds/4348Mi) % 282.62/40.03 % (384705)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 282.62/40.03 % (384705)Terminated due to inappropriate strategy. % 282.62/40.03 % (384705)------------------------------ % 282.62/40.03 % (384705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.62/40.03 % (384705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.62/40.03 % (384705)CaDiCaL version: 2.1.3 % 282.62/40.03 % (384705)Termination reason: Inappropriate % 282.62/40.03 % (384705)Time elapsed: 0.008 s % 282.62/40.03 % (384705)Peak memory usage: 11 MB % 282.62/40.03 % (384705)Instructions burned: 16 (million) % 282.62/40.03 % (384705)------------------------------ % 282.62/40.03 % (384705)------------------------------ % 282.62/40.03 % (384707)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3039159700:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2692 on theBenchmark for (2692ds/1738Mi) % 282.62/40.03 % (384707)Instruction limit reached! % 282.62/40.03 % (384707)------------------------------ % 282.62/40.03 % (384707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.62/40.03 % (384707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.19/42.53 % (384707)CaDiCaL version: 2.1.3 % 300.19/42.53 % (384707)Termination reason: Instruction limit % 300.19/42.53 % (384707)Termination phase: Saturation % 300.19/42.53 % (384707)Time elapsed: 0.658 s % 300.19/42.53 % (384707)Peak memory usage: 14 MB % 300.19/42.53 % (384707)Instructions burned: 1739 (million) % 300.19/42.53 % (384709)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2569177838:i=10228:av=off:rtra=on_2686 on theBenchmark for (2686ds/10228Mi) % 300.19/42.53 % (384701)Instruction limit reached! % 300.19/42.53 % (384701)------------------------------ % 300.19/42.53 % (384701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.19/42.53 % (384701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.19/42.53 % (384701)CaDiCaL version: 2.1.3 % 300.19/42.53 % (384701)Termination reason: Instruction limit % 300.19/42.53 % (384701)Termination phase: Saturation % 300.19/42.53 % (384701)Time elapsed: 1.534 s % 300.19/42.53 % (384701)Peak memory usage: 35 MB % 300.19/42.53 % (384701)Instructions burned: 2945 (million) % 300.19/42.53 % (384711)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3972284952:i=108564:rtra=on_2679 on theBenchmark for (2679ds/108564Mi) % 300.19/42.53 % (384711)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.19/42.53 % (384711)Terminated due to inappropriate strategy. % 300.19/42.53 % (384711)------------------------------ % 300.19/42.53 % (384711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.19/42.53 % (384711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.19/42.53 % (384711)CaDiCaL version: 2.1.3 % 300.19/42.53 % (384711)Termination reason: Inappropriate % 300.19/42.53 % (384711)Time elapsed: 0.011 s % 300.19/42.53 % (384711)Peak memory usage: 11 MB % 300.19/42.53 % (384711)Instructions burned: 21 (million) % 300.19/42.53 % (384711)------------------------------ % 300.19/42.53 % (384711)------------------------------ % 300.19/42.53 % (384713)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=738321293:i=7024:aac=none:rtra=on_2678 on theBenchmark for (2678ds/7024Mi) % 300.19/42.53 % (383663)Instruction limit reached! % 300.19/42.53 % (383663)------------------------------ % 300.19/42.53 % (383663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.19/42.53 % (383663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.19/42.53 % (383663)CaDiCaL version: 2.1.3 % 300.19/42.53 % (383663)Termination reason: Instruction limit % 300.19/42.53 % (383663)Termination phase: Saturation % 300.19/42.53 % (383663)Time elapsed: 35.354 s % 300.19/42.53 % (383663)Peak memory usage: 138 MB % 300.19/42.53 % (383663)Instructions burned: 88025 (million) % 300.19/42.53 % (384715)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=4025883105:i=7546:rtra=on:amm=off_2646 on theBenchmark for (2646ds/7546Mi) % 300.19/42.53 % (384713)Instruction limit reached! % 300.19/42.53 % (384713)------------------------------ % 300.19/42.53 % (384713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.19/42.53 % (384713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.19/42.53 % (384713)CaDiCaL version: 2.1.3 % 300.19/42.53 % (384713)Termination reason: Instruction limit % 300.19/42.53 % (384713)Termination phase: Saturation % 300.19/42.53 % (384713)Time elapsed: 4.086 s % 300.19/42.53 % (384713)Peak memory usage: 46 MB % 300.19/42.53 % (384713)Instructions burned: 7025 (million) % 300.19/42.53 % (384717)ott+11_1_sil=16000:si=on:gs=on:random_seed=3820053314:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2637 on theBenchmark for (2637ds/4502Mi) % 300.19/42.53 % (384709)Instruction limit reached! % 300.19/42.53 % (384709)------------------------------ % 300.19/42.53 % (384709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.19/42.53 % (384709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.19/42.53 % (384709)CaDiCaL version: 2.1.3 % 300.19/42.53 % (384709)Termination reason: Instruction limit % 300.19/42.53 % (384709)Termination phase: Saturation % 300.19/42.53 % (384709)Time elapsed: 5.902 s % 300.19/42.53 % (384709)Peak memory usage: 57 MB % 300.19/42.53 % (384709)Instructions burned: 10229 (million) % 300.19/42.53 % (384719)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=3293500142:fmbsr=1.6:i=135068:rtra=on_2626 on theBenchmark for (2626ds/135068Mi) % 300.19/42.53 % (384719)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.19/42.53 % (384719)Terminated due to inappropriate strategy. % 300.19/42.53 % (384719)------------------------------ % 300.19/42.53 % (384719 % 300.19/42.54 Terminated % 300.19/42.54 % Vampire exiting % 300.19/42.54 Terminated %------------------------------------------------------------------------------