%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX130_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:46:32 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 : SWX130_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.19 % Computer : n009.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 15:03:00 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.22 Running first-order model finding % 0.07/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.96/0.73 % (3128622)Will run a generic schedule for satisfiability detection. % 2.96/0.73 % (3128627)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3453096897_2999 on theBenchmark for (2999ds/0Mi) % 2.96/0.73 % (3128628)% WARNING: option uhcvi not known. % 2.96/0.73 % (3128627)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.96/0.73 % (3128627)Terminated due to inappropriate strategy. % 2.96/0.73 % (3128627)------------------------------ % 2.96/0.73 % (3128627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.96/0.73 % (3128627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.96/0.73 % (3128627)CaDiCaL version: 2.1.3 % 2.96/0.73 % (3128627)Termination reason: Inappropriate % 2.96/0.73 % (3128627)Time elapsed: 0.007 s % 2.96/0.73 % (3128627)Peak memory usage: 10 MB % 2.96/0.73 % (3128627)Instructions burned: 31 (million) % 2.96/0.73 % (3128628)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2485889730:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.96/0.73 % (3128629)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=843977633:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.96/0.73 % (3128632)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1568720122:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.96/0.73 % (3128630)dis+10_1_sil=32000:sp=arity:random_seed=1878721164:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.96/0.73 % (3128627)------------------------------ % 2.96/0.73 % (3128627)------------------------------ % 2.96/0.73 % (3128631)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1946569364:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.96/0.73 % (3128633)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3196866306:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.96/0.73 % (3128641)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1695339159:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.96/0.73 % (3128641)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.96/0.73 % (3128641)Terminated due to inappropriate strategy. % 2.96/0.73 % (3128641)------------------------------ % 2.96/0.73 % (3128641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.96/0.73 % (3128641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.96/0.73 % (3128641)CaDiCaL version: 2.1.3 % 2.96/0.73 % (3128641)Termination reason: Inappropriate % 2.96/0.73 % (3128641)Time elapsed: 0.012 s % 2.96/0.73 % (3128641)Peak memory usage: 10 MB % 2.96/0.73 % (3128641)Instructions burned: 31 (million) % 2.96/0.73 % (3128641)------------------------------ % 2.96/0.73 % (3128641)------------------------------ % 2.96/0.73 % (3128630)Instruction limit reached! % 2.96/0.73 % (3128630)------------------------------ % 2.96/0.73 % (3128630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.96/0.73 % (3128630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.96/0.73 % (3128630)CaDiCaL version: 2.1.3 % 2.96/0.73 % (3128630)Termination reason: Instruction limit % 2.96/0.73 % (3128630)Termination phase: Saturation % 2.96/0.73 % (3128630)Time elapsed: 0.045 s % 2.96/0.73 % (3128630)Peak memory usage: 12 MB % 2.96/0.73 % (3128630)Instructions burned: 104 (million) % 2.96/0.73 % (3128643)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4038866113:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.96/0.73 % (3128631)Instruction limit reached! % 2.96/0.73 % (3128631)------------------------------ % 2.96/0.73 % (3128631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.96/0.73 % (3128631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.96/0.73 % (3128631)CaDiCaL version: 2.1.3 % 2.96/0.73 % (3128631)Termination reason: Instruction limit % 2.96/0.73 % (3128631)Termination phase: Saturation % 2.96/0.73 % (3128631)Time elapsed: 0.053 s % 2.96/0.73 % (3128631)Peak memory usage: 13 MB % 2.96/0.73 % (3128631)Instructions burned: 120 (million) % 2.96/0.73 % (3128644)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=1881907314:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 2.96/0.73 % (3128632)Instruction limit reached! % 2.96/0.73 % (3128632)------------------------------ % 2.96/0.73 % (3128632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.78/0.90 % (3128632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.78/0.90 % (3128632)CaDiCaL version: 2.1.3 % 3.78/0.90 % (3128632)Termination reason: Instruction limit % 3.78/0.90 % (3128632)Termination phase: Saturation % 3.78/0.90 % (3128632)Time elapsed: 0.060 s % 3.78/0.90 % (3128632)Peak memory usage: 13 MB % 3.78/0.90 % (3128632)Instructions burned: 132 (million) % 3.78/0.90 % (3128646)ott-21_1_sil=16000:fs=off:random_seed=1727507716:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 3.78/0.90 % (3128633)Instruction limit reached! % 3.78/0.90 % (3128633)------------------------------ % 3.78/0.90 % (3128633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.78/0.90 % (3128633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.78/0.90 % (3128633)CaDiCaL version: 2.1.3 % 3.78/0.90 % (3128633)Termination reason: Instruction limit % 3.78/0.90 % (3128633)Termination phase: Saturation % 3.78/0.90 % (3128633)Time elapsed: 0.079 s % 3.78/0.90 % (3128633)Peak memory usage: 14 MB % 3.78/0.90 % (3128633)Instructions burned: 160 (million) % 3.78/0.90 % (3128648)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2746830432:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 3.78/0.90 % (3128651)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3134735919:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 3.78/0.90 % (3128651)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.78/0.90 % (3128651)Terminated due to inappropriate strategy. % 3.78/0.90 % (3128651)------------------------------ % 3.78/0.90 % (3128651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.78/0.90 % (3128651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.78/0.90 % (3128651)CaDiCaL version: 2.1.3 % 3.78/0.90 % (3128651)Termination reason: Inappropriate % 3.78/0.90 % (3128651)Time elapsed: 0.010 s % 3.78/0.90 % (3128651)Peak memory usage: 10 MB % 3.78/0.90 % (3128651)Instructions burned: 23 (million) % 3.78/0.90 % (3128651)------------------------------ % 3.78/0.90 % (3128651)------------------------------ % 3.78/0.90 % (3128643)Instruction limit reached! % 3.78/0.90 % (3128643)------------------------------ % 3.78/0.90 % (3128643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.78/0.90 % (3128643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.78/0.90 % (3128643)CaDiCaL version: 2.1.3 % 3.78/0.90 % (3128643)Termination reason: Instruction limit % 3.78/0.90 % (3128643)Termination phase: Saturation % 3.78/0.90 % (3128643)Time elapsed: 0.058 s % 3.78/0.90 % (3128643)Peak memory usage: 14 MB % 3.78/0.90 % (3128643)Instructions burned: 132 (million) % 3.78/0.90 % (3128653)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1776383372:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 3.78/0.90 % (3128654)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1962310818:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 3.78/0.90 % (3128654)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.78/0.90 % (3128654)Terminated due to inappropriate strategy. % 3.78/0.90 % (3128654)------------------------------ % 3.78/0.90 % (3128654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.78/0.90 % (3128654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.78/0.90 % (3128654)CaDiCaL version: 2.1.3 % 3.78/0.90 % (3128654)Termination reason: Inappropriate % 3.78/0.90 % (3128654)Time elapsed: 0.010 s % 3.78/0.90 % (3128654)Peak memory usage: 10 MB % 3.78/0.90 % (3128654)Instructions burned: 23 (million) % 3.78/0.90 % (3128654)------------------------------ % 3.78/0.90 % (3128654)------------------------------ % 3.78/0.90 % (3128646)Instruction limit reached! % 3.78/0.90 % (3128646)------------------------------ % 3.78/0.90 % (3128646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.78/0.90 % (3128646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.78/0.90 % (3128646)CaDiCaL version: 2.1.3 % 3.78/0.90 % (3128646)Termination reason: Instruction limit % 3.78/0.90 % (3128646)Termination phase: Saturation % 3.78/0.90 % (3128646)Time elapsed: 0.079 s % 3.78/0.90 % (3128646)Peak memory usage: 13 MB % 3.78/0.90 % (3128646)Instructions burned: 180 (million) % 3.78/0.90 % (3128657)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=1077666866: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) % 13.76/2.29 % (3128658)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1598185465:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 13.76/2.29 % (3128644)Instruction limit reached! % 13.76/2.29 % (3128644)------------------------------ % 13.76/2.29 % (3128644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.76/2.29 % (3128644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.76/2.29 % (3128644)CaDiCaL version: 2.1.3 % 13.76/2.29 % (3128644)Termination reason: Instruction limit % 13.76/2.29 % (3128644)Termination phase: Saturation % 13.76/2.29 % (3128644)Time elapsed: 0.168 s % 13.76/2.29 % (3128644)Peak memory usage: 17 MB % 13.76/2.29 % (3128644)Instructions burned: 685 (million) % 13.76/2.29 % (3128661)fmb+10_1_sil=64000:random_seed=3880662600:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 13.76/2.29 % (3128661)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 13.76/2.29 % (3128661)Terminated due to inappropriate strategy. % 13.76/2.29 % (3128661)------------------------------ % 13.76/2.29 % (3128661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.76/2.29 % (3128661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.76/2.29 % (3128661)CaDiCaL version: 2.1.3 % 13.76/2.29 % (3128661)Termination reason: Inappropriate % 13.76/2.29 % (3128661)Time elapsed: 0.007 s % 13.76/2.29 % (3128661)Peak memory usage: 10 MB % 13.76/2.29 % (3128661)Instructions burned: 31 (million) % 13.76/2.29 % (3128661)------------------------------ % 13.76/2.29 % (3128661)------------------------------ % 13.76/2.29 % (3128663)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3123500297:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 13.76/2.29 % (3128663)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 13.76/2.29 % (3128663)Terminated due to inappropriate strategy. % 13.76/2.29 % (3128663)------------------------------ % 13.76/2.29 % (3128663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.76/2.29 % (3128663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.76/2.29 % (3128663)CaDiCaL version: 2.1.3 % 13.76/2.29 % (3128663)Termination reason: Inappropriate % 13.76/2.29 % (3128663)Time elapsed: 0.006 s % 13.76/2.29 % (3128663)Peak memory usage: 10 MB % 13.76/2.29 % (3128663)Instructions burned: 31 (million) % 13.76/2.29 % (3128663)------------------------------ % 13.76/2.29 % (3128663)------------------------------ % 13.76/2.29 % (3128648)Instruction limit reached! % 13.76/2.29 % (3128648)------------------------------ % 13.76/2.29 % (3128648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.76/2.29 % (3128648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.76/2.29 % (3128648)CaDiCaL version: 2.1.3 % 13.76/2.29 % (3128648)Termination reason: Instruction limit % 13.76/2.29 % (3128648)Termination phase: Saturation % 13.76/2.29 % (3128648)Time elapsed: 0.188 s % 13.76/2.29 % (3128648)Peak memory usage: 13 MB % 13.76/2.29 % (3128648)Instructions burned: 478 (million) % 13.76/2.29 % (3128665)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=789676637:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 13.76/2.29 % (3128665)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 13.76/2.29 % (3128665)Terminated due to inappropriate strategy. % 13.76/2.29 % (3128665)------------------------------ % 13.76/2.29 % (3128665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.76/2.29 % (3128665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.76/2.29 % (3128665)CaDiCaL version: 2.1.3 % 13.76/2.29 % (3128665)Termination reason: Inappropriate % 13.76/2.29 % (3128665)Time elapsed: 0.006 s % 13.76/2.29 % (3128665)Peak memory usage: 10 MB % 13.76/2.29 % (3128665)Instructions burned: 31 (million) % 13.76/2.29 % (3128665)------------------------------ % 13.76/2.29 % (3128665)------------------------------ % 13.76/2.29 % (3128666)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2155690578:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 13.76/2.29 % (3128668)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=852620682:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 13.76/2.29 % (3128657)Instruction limit reached! % 13.76/2.29 % (3128657)------------------------------ % 16.77/2.82 % (3128657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.77/2.82 % (3128657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.77/2.82 % (3128657)CaDiCaL version: 2.1.3 % 16.77/2.82 % (3128657)Termination reason: Instruction limit % 16.77/2.82 % (3128657)Termination phase: Saturation % 16.77/2.82 % (3128657)Time elapsed: 0.285 s % 16.77/2.82 % (3128657)Peak memory usage: 15 MB % 16.77/2.82 % (3128657)Instructions burned: 692 (million) % 16.77/2.82 % (3128671)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3698502537:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 16.77/2.82 % (3128671)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.77/2.82 % (3128671)Terminated due to inappropriate strategy. % 16.77/2.82 % (3128671)------------------------------ % 16.77/2.82 % (3128671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.77/2.82 % (3128671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.77/2.82 % (3128671)CaDiCaL version: 2.1.3 % 16.77/2.82 % (3128671)Termination reason: Inappropriate % 16.77/2.82 % (3128671)Time elapsed: 0.013 s % 16.77/2.82 % (3128671)Peak memory usage: 10 MB % 16.77/2.82 % (3128671)Instructions burned: 31 (million) % 16.77/2.82 % (3128671)------------------------------ % 16.77/2.82 % (3128671)------------------------------ % 16.77/2.82 % (3128673)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=614444378:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 16.77/2.82 % (3128673)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.77/2.82 % (3128673)Terminated due to inappropriate strategy. % 16.77/2.82 % (3128673)------------------------------ % 16.77/2.82 % (3128673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.77/2.82 % (3128673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.77/2.82 % (3128673)CaDiCaL version: 2.1.3 % 16.77/2.82 % (3128673)Termination reason: Inappropriate % 16.77/2.82 % (3128673)Time elapsed: 0.012 s % 16.77/2.82 % (3128673)Peak memory usage: 10 MB % 16.77/2.82 % (3128673)Instructions burned: 31 (million) % 16.77/2.82 % (3128673)------------------------------ % 16.77/2.82 % (3128673)------------------------------ % 16.77/2.82 % (3128658)Instruction limit reached! % 16.77/2.82 % (3128658)------------------------------ % 16.77/2.82 % (3128658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.77/2.82 % (3128658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.77/2.82 % (3128658)CaDiCaL version: 2.1.3 % 16.77/2.82 % (3128658)Termination reason: Instruction limit % 16.77/2.82 % (3128658)Termination phase: Saturation % 16.77/2.82 % (3128658)Time elapsed: 0.339 s % 16.77/2.82 % (3128658)Peak memory usage: 14 MB % 16.77/2.82 % (3128658)Instructions burned: 880 (million) % 16.77/2.82 % (3128675)ott-2_1_sil=16000:newcnf=on:random_seed=3301374246:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 16.77/2.82 % (3128676)ott+10_1_sil=32000:tgt=ground:random_seed=2506831951:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi) % 16.77/2.82 % (3128653)Instruction limit reached! % 16.77/2.82 % (3128653)------------------------------ % 16.77/2.82 % (3128653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.77/2.82 % (3128653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.77/2.82 % (3128653)CaDiCaL version: 2.1.3 % 16.77/2.82 % (3128653)Termination reason: Instruction limit % 16.77/2.82 % (3128653)Termination phase: Saturation % 16.77/2.82 % (3128653)Time elapsed: 0.459 s % 16.77/2.82 % (3128653)Peak memory usage: 14 MB % 16.77/2.82 % (3128653)Instructions burned: 1181 (million) % 16.77/2.82 % (3128679)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3583533027:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 16.77/2.82 % (3128679)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.77/2.82 % (3128679)Terminated due to inappropriate strategy. % 16.77/2.82 % (3128679)------------------------------ % 16.77/2.82 % (3128679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.77/2.82 % (3128679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.77/2.82 % (3128679)CaDiCaL version: 2.1.3 % 16.77/2.82 % (3128679)Termination reason: Inappropriate % 16.77/2.82 % (3128679)Time elapsed: 0.014 s % 16.77/2.82 % (3128679)Peak memory usage: 10 MB % 16.77/2.82 % (3128679)Instructions burned: 31 (million) % 74.88/10.83 % (3128679)------------------------------ % 74.88/10.83 % (3128679)------------------------------ % 74.88/10.83 % (3128681)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1514045991:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi) % 74.88/10.83 % (3128668)Instruction limit reached! % 74.88/10.83 % (3128668)------------------------------ % 74.88/10.83 % (3128668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.88/10.83 % (3128668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.88/10.83 % (3128668)CaDiCaL version: 2.1.3 % 74.88/10.83 % (3128668)Termination reason: Instruction limit % 74.88/10.83 % (3128668)Termination phase: Saturation % 74.88/10.83 % (3128668)Time elapsed: 0.411 s % 74.88/10.83 % (3128668)Peak memory usage: 23 MB % 74.88/10.83 % (3128668)Instructions burned: 1475 (million) % 74.88/10.83 % (3128683)dis+21_1_sil=32000:sas=cadical:random_seed=3447397600:i=3773:amm=off_2992 on theBenchmark for (2992ds/3773Mi) % 74.88/10.83 % (3128675)Instruction limit reached! % 74.88/10.83 % (3128675)------------------------------ % 74.88/10.83 % (3128675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.88/10.83 % (3128675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.88/10.83 % (3128675)CaDiCaL version: 2.1.3 % 74.88/10.83 % (3128675)Termination reason: Instruction limit % 74.88/10.83 % (3128675)Termination phase: Saturation % 74.88/10.83 % (3128675)Time elapsed: 0.369 s % 74.88/10.83 % (3128675)Peak memory usage: 16 MB % 74.88/10.83 % (3128675)Instructions burned: 871 (million) % 74.88/10.83 % (3128685)ott+11_1_sil=16000:gs=on:random_seed=1998780625:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2990 on theBenchmark for (2990ds/2251Mi) % 74.88/10.83 % (3128683)Instruction limit reached! % 74.88/10.83 % (3128683)------------------------------ % 74.88/10.83 % (3128683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.88/10.83 % (3128683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.88/10.83 % (3128683)CaDiCaL version: 2.1.3 % 74.88/10.83 % (3128683)Termination reason: Instruction limit % 74.88/10.83 % (3128683)Termination phase: Saturation % 74.88/10.83 % (3128683)Time elapsed: 0.766 s % 74.88/10.83 % (3128683)Peak memory usage: 15 MB % 74.88/10.83 % (3128683)Instructions burned: 3774 (million) % 74.88/10.83 % (3128687)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=315631676:fmbsr=1.6:i=67534_2984 on theBenchmark for (2984ds/67534Mi) % 74.88/10.83 % (3128687)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 74.88/10.83 % (3128687)Terminated due to inappropriate strategy. % 74.88/10.83 % (3128687)------------------------------ % 74.88/10.83 % (3128687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.88/10.83 % (3128687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.88/10.83 % (3128687)CaDiCaL version: 2.1.3 % 74.88/10.83 % (3128687)Termination reason: Inappropriate % 74.88/10.83 % (3128687)Time elapsed: 0.007 s % 74.88/10.83 % (3128687)Peak memory usage: 10 MB % 74.88/10.83 % (3128687)Instructions burned: 31 (million) % 74.88/10.83 % (3128687)------------------------------ % 74.88/10.83 % (3128687)------------------------------ % 74.88/10.83 % (3128689)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2383402719:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2984 on theBenchmark for (2984ds/4591Mi) % 74.88/10.83 % (3128685)Instruction limit reached! % 74.88/10.83 % (3128685)------------------------------ % 74.88/10.83 % (3128685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.88/10.83 % (3128685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.88/10.83 % (3128685)CaDiCaL version: 2.1.3 % 74.88/10.83 % (3128685)Termination reason: Instruction limit % 74.88/10.83 % (3128685)Termination phase: Saturation % 74.88/10.83 % (3128685)Time elapsed: 0.862 s % 74.88/10.83 % (3128685)Peak memory usage: 14 MB % 74.88/10.83 % (3128685)Instructions burned: 2252 (million) % 74.88/10.83 % (3128691)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2061099594:i=29340_2981 on theBenchmark for (2981ds/29340Mi) % 74.88/10.83 % (3128681)Instruction limit reached! % 74.88/10.83 % (3128681)------------------------------ % 74.88/10.83 % (3128681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.88/10.83 % (3128681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.88/10.83 % (3128681)CaDiCaL version: 2.1.3 % 74.88/10.83 % (3128681)Termination reason: Instruction limit % 84.35/12.15 % (3128681)Termination phase: Saturation % 84.35/12.15 % (3128681)Time elapsed: 1.365 s % 84.35/12.15 % (3128681)Peak memory usage: 17 MB % 84.35/12.15 % (3128681)Instructions burned: 3514 (million) % 84.35/12.15 % (3128693)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3917280407:i=5211_2979 on theBenchmark for (2979ds/5211Mi) % 84.35/12.15 % (3128666)Instruction limit reached! % 84.35/12.15 % (3128666)------------------------------ % 84.35/12.15 % (3128666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.35/12.15 % (3128666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.35/12.15 % (3128666)CaDiCaL version: 2.1.3 % 84.35/12.15 % (3128666)Termination reason: Instruction limit % 84.35/12.15 % (3128666)Termination phase: Saturation % 84.35/12.15 % (3128666)Time elapsed: 1.975 s % 84.35/12.15 % (3128666)Peak memory usage: 20 MB % 84.35/12.15 % (3128666)Instructions burned: 5133 (million) % 84.35/12.15 % (3128695)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3954332958:i=5497:nm=2_2976 on theBenchmark for (2976ds/5497Mi) % 84.35/12.15 % (3128695)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 84.35/12.15 % (3128695)Terminated due to inappropriate strategy. % 84.35/12.15 % (3128695)------------------------------ % 84.35/12.15 % (3128695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.35/12.15 % (3128695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.35/12.15 % (3128695)CaDiCaL version: 2.1.3 % 84.35/12.15 % (3128695)Termination reason: Inappropriate % 84.35/12.15 % (3128695)Time elapsed: 0.013 s % 84.35/12.15 % (3128695)Peak memory usage: 10 MB % 84.35/12.15 % (3128695)Instructions burned: 31 (million) % 84.35/12.15 % (3128695)------------------------------ % 84.35/12.15 % (3128695)------------------------------ % 84.35/12.15 % (3128697)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2912863940:fmbsr=2:i=46332_2976 on theBenchmark for (2976ds/46332Mi) % 84.35/12.15 % (3128697)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 84.35/12.15 % (3128697)Terminated due to inappropriate strategy. % 84.35/12.15 % (3128697)------------------------------ % 84.35/12.15 % (3128697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.35/12.16 % (3128697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.35/12.16 % (3128697)CaDiCaL version: 2.1.3 % 84.35/12.16 % (3128697)Termination reason: Inappropriate % 84.35/12.16 % (3128697)Time elapsed: 0.013 s % 84.35/12.16 % (3128697)Peak memory usage: 11 MB % 84.35/12.16 % (3128697)Instructions burned: 31 (million) % 84.35/12.16 % (3128697)------------------------------ % 84.35/12.16 % (3128697)------------------------------ % 84.35/12.16 % (3128699)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3412215834:i=14071_2976 on theBenchmark for (2976ds/14071Mi) % 84.35/12.16 % (3128699)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 84.35/12.16 % (3128699)Terminated due to inappropriate strategy. % 84.35/12.16 % (3128699)------------------------------ % 84.35/12.16 % (3128699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.35/12.16 % (3128699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.35/12.16 % (3128699)CaDiCaL version: 2.1.3 % 84.35/12.16 % (3128699)Termination reason: Inappropriate % 84.35/12.16 % (3128699)Time elapsed: 0.012 s % 84.35/12.16 % (3128699)Peak memory usage: 10 MB % 84.35/12.16 % (3128699)Instructions burned: 31 (million) % 84.35/12.16 % (3128699)------------------------------ % 84.35/12.16 % (3128699)------------------------------ % 84.35/12.16 % (3128701)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1753131743:i=22565:add=on:rawr=on_2975 on theBenchmark for (2975ds/22565Mi) % 84.35/12.16 % (3128676)Instruction limit reached! % 84.35/12.16 % (3128676)------------------------------ % 84.35/12.16 % (3128676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.35/12.16 % (3128676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.35/12.16 % (3128676)CaDiCaL version: 2.1.3 % 84.35/12.16 % (3128676)Termination reason: Instruction limit % 84.35/12.16 % (3128676)Termination phase: Saturation % 84.35/12.16 % (3128676)Time elapsed: 1.987 s % 84.35/12.16 % (3128676)Peak memory usage: 14 MB % 84.35/12.16 % (3128676)Instructions burned: 5116 (million) % 84.35/12.16 % (3128703)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3839962330:i=8173:av=off_2974 on theBenchmark for (2974ds/8173Mi) % 85.51/12.32 % (3128689)Instruction limit reached! % 85.51/12.32 % (3128689)------------------------------ % 85.51/12.32 % (3128689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.51/12.32 % (3128689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.51/12.32 % (3128689)CaDiCaL version: 2.1.3 % 85.51/12.32 % (3128689)Termination reason: Instruction limit % 85.51/12.32 % (3128689)Termination phase: Saturation % 85.51/12.32 % (3128689)Time elapsed: 1.373 s % 85.51/12.32 % (3128689)Peak memory usage: 44 MB % 85.51/12.32 % (3128689)Instructions burned: 4593 (million) % 85.51/12.32 % (3128705)dis+10_16:1_sil=16000:random_seed=2313450786:i=9155:fsr=off_2970 on theBenchmark for (2970ds/9155Mi) % 85.51/12.32 % (3128693)Instruction limit reached! % 85.51/12.32 % (3128693)------------------------------ % 85.51/12.32 % (3128693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.51/12.32 % (3128693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.51/12.32 % (3128693)CaDiCaL version: 2.1.3 % 85.51/12.32 % (3128693)Termination reason: Instruction limit % 85.51/12.32 % (3128693)Termination phase: Saturation % 85.51/12.32 % (3128693)Time elapsed: 2.036 s % 85.51/12.32 % (3128693)Peak memory usage: 22 MB % 85.51/12.32 % (3128693)Instructions burned: 5213 (million) % 85.51/12.32 % (3128707)ott-3_8_sil=64000:random_seed=3407567750:i=20139:bs=on_2958 on theBenchmark for (2958ds/20139Mi) % 85.51/12.32 % (3128705)Instruction limit reached! % 85.51/12.32 % (3128705)------------------------------ % 85.51/12.32 % (3128705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.51/12.32 % (3128705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.51/12.32 % (3128705)CaDiCaL version: 2.1.3 % 85.51/12.32 % (3128705)Termination reason: Instruction limit % 85.51/12.32 % (3128705)Termination phase: Saturation % 85.51/12.32 % (3128705)Time elapsed: 1.882 s % 85.51/12.32 % (3128705)Peak memory usage: 18 MB % 85.51/12.32 % (3128705)Instructions burned: 9160 (million) % 85.51/12.32 % (3128709)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3918863103:fmbsr=2:i=32576_2951 on theBenchmark for (2951ds/32576Mi) % 85.51/12.32 % (3128709)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 85.51/12.32 % (3128709)Terminated due to inappropriate strategy. % 85.51/12.32 % (3128709)------------------------------ % 85.51/12.32 % (3128709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.51/12.32 % (3128709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.51/12.32 % (3128709)CaDiCaL version: 2.1.3 % 85.51/12.32 % (3128709)Termination reason: Inappropriate % 85.51/12.32 % (3128709)Time elapsed: 0.006 s % 85.51/12.32 % (3128709)Peak memory usage: 10 MB % 85.51/12.32 % (3128709)Instructions burned: 31 (million) % 85.51/12.32 % (3128709)------------------------------ % 85.51/12.32 % (3128709)------------------------------ % 85.51/12.32 % (3128711)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1590452379:i=11404_2951 on theBenchmark for (2951ds/11404Mi) % 85.51/12.32 % (3128703)Instruction limit reached! % 85.51/12.32 % (3128703)------------------------------ % 85.51/12.32 % (3128703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.51/12.32 % (3128703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.51/12.32 % (3128703)CaDiCaL version: 2.1.3 % 85.51/12.32 % (3128703)Termination reason: Instruction limit % 85.51/12.32 % (3128703)Termination phase: Saturation % 85.51/12.32 % (3128703)Time elapsed: 3.180 s % 85.51/12.32 % (3128703)Peak memory usage: 15 MB % 85.51/12.32 % (3128703)Instructions burned: 8180 (million) % 85.51/12.32 % (3128713)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=746432236:i=14134_2942 on theBenchmark for (2942ds/14134Mi) % 85.51/12.32 % (3128711)Instruction limit reached! % 85.51/12.32 % (3128711)------------------------------ % 85.51/12.32 % (3128711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.51/12.32 % (3128711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.51/12.32 % (3128711)CaDiCaL version: 2.1.3 % 85.51/12.32 % (3128711)Termination reason: Instruction limit % 85.51/12.32 % (3128711)Termination phase: Saturation % 85.51/12.32 % (3128711)Time elapsed: 2.393 s % 85.51/12.32 % (3128711)Peak memory usage: 15 MB % 85.51/12.32 % (3128711)Instructions burned: 11406 (million) % 85.51/12.32 % (3128715)dis+33_16_sil=32000:sac=on:random_seed=645275960:i=15851:nm=0_2927 on theBenchmark for (2927ds/15851Mi) % 85.51/12.32 % (3128715)Instruction limit reached! % 85.51/12.32 % (3128715)------------------------------ % 85.51/12.32 % (3128715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.56/15.40 % (3128715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.56/15.40 % (3128715)CaDiCaL version: 2.1.3 % 107.56/15.40 % (3128715)Termination reason: Instruction limit % 107.56/15.40 % (3128715)Termination phase: Saturation % 107.56/15.40 % (3128715)Time elapsed: 3.329 s % 107.56/15.40 % (3128715)Peak memory usage: 22 MB % 107.56/15.40 % (3128715)Instructions burned: 15853 (million) % 107.56/15.40 % (3128717)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2378525253:avsq=on:i=17627:add=on:amm=off_2893 on theBenchmark for (2893ds/17627Mi) % 107.56/15.40 % (3128713)Instruction limit reached! % 107.56/15.40 % (3128713)------------------------------ % 107.56/15.40 % (3128713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.56/15.40 % (3128713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.56/15.40 % (3128713)CaDiCaL version: 2.1.3 % 107.56/15.40 % (3128713)Termination reason: Instruction limit % 107.56/15.40 % (3128713)Termination phase: Saturation % 107.56/15.40 % (3128713)Time elapsed: 5.527 s % 107.56/15.40 % (3128713)Peak memory usage: 16 MB % 107.56/15.40 % (3128713)Instructions burned: 14135 (million) % 107.56/15.40 % (3128719)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=766943853:s2a=on:i=53295_2886 on theBenchmark for (2886ds/53295Mi) % 107.56/15.40 % (3128701)Instruction limit reached! % 107.56/15.40 % (3128701)------------------------------ % 107.56/15.40 % (3128701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.56/15.40 % (3128701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.56/15.40 % (3128701)CaDiCaL version: 2.1.3 % 107.56/15.40 % (3128701)Termination reason: Instruction limit % 107.56/15.40 % (3128701)Termination phase: Saturation % 107.56/15.40 % (3128701)Time elapsed: 9.214 s % 107.56/15.40 % (3128701)Peak memory usage: 17 MB % 107.56/15.40 % (3128701)Instructions burned: 22566 (million) % 107.56/15.40 % (3128721)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1654996810:i=26857:ins=20_2883 on theBenchmark for (2883ds/26857Mi) % 107.56/15.40 % (3128721)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 107.56/15.40 % (3128721)Terminated due to inappropriate strategy. % 107.56/15.40 % (3128721)------------------------------ % 107.56/15.40 % (3128721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.56/15.40 % (3128721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.56/15.40 % (3128721)CaDiCaL version: 2.1.3 % 107.56/15.40 % (3128721)Termination reason: Inappropriate % 107.56/15.40 % (3128721)Time elapsed: 0.013 s % 107.56/15.40 % (3128721)Peak memory usage: 10 MB % 107.56/15.40 % (3128721)Instructions burned: 31 (million) % 107.56/15.40 % (3128721)------------------------------ % 107.56/15.40 % (3128721)------------------------------ % 107.56/15.40 % (3128723)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1572255228:i=28120:bs=on:fsr=off_2883 on theBenchmark for (2883ds/28120Mi) % 107.56/15.40 % (3128707)Instruction limit reached! % 107.56/15.40 % (3128707)------------------------------ % 107.56/15.40 % (3128707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.56/15.40 % (3128707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.56/15.40 % (3128707)CaDiCaL version: 2.1.3 % 107.56/15.40 % (3128707)Termination reason: Instruction limit % 107.56/15.40 % (3128707)Termination phase: Saturation % 107.56/15.40 % (3128707)Time elapsed: 7.734 s % 107.56/15.40 % (3128707)Peak memory usage: 19 MB % 107.56/15.40 % (3128707)Instructions burned: 20141 (million) % 107.56/15.40 % (3128725)fmb+10_1_sil=256000:fmbss=7:random_seed=1223865114:fmbsr=1.6:i=182295_2881 on theBenchmark for (2881ds/182295Mi) % 107.56/15.40 % (3128725)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 107.56/15.40 % (3128725)Terminated due to inappropriate strategy. % 107.56/15.40 % (3128725)------------------------------ % 107.56/15.40 % (3128725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.56/15.40 % (3128725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.56/15.40 % (3128725)CaDiCaL version: 2.1.3 % 107.56/15.40 % (3128725)Termination reason: Inappropriate % 107.56/15.40 % (3128725)Time elapsed: 0.013 s % 107.56/15.40 % (3128725)Peak memory usage: 10 MB % 107.56/15.40 % (3128725)Instructions burned: 31 (million) % 107.56/15.40 % (3128725)------------------------------ % 107.56/15.40 % (3128725)------------------------------ % 107.56/15.40 % (3128727)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3982462780:i=44625:gsp=on_2880 on theBenchmark for (2880ds/44625Mi) % 123.85/17.73 % (3128727)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.85/17.73 % (3128727)Terminated due to inappropriate strategy. % 123.85/17.73 % (3128727)------------------------------ % 123.85/17.73 % (3128727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.85/17.73 % (3128727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.85/17.73 % (3128727)CaDiCaL version: 2.1.3 % 123.85/17.73 % (3128727)Termination reason: Inappropriate % 123.85/17.73 % (3128727)Time elapsed: 0.013 s % 123.85/17.73 % (3128727)Peak memory usage: 11 MB % 123.85/17.73 % (3128727)Instructions burned: 31 (million) % 123.85/17.73 % (3128727)------------------------------ % 123.85/17.73 % (3128727)------------------------------ % 123.85/17.73 % (3128729)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1603386677:i=160505_2880 on theBenchmark for (2880ds/160505Mi) % 123.85/17.73 % (3128729)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.85/17.73 % (3128729)Terminated due to inappropriate strategy. % 123.85/17.73 % (3128729)------------------------------ % 123.85/17.73 % (3128729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.85/17.73 % (3128729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.85/17.73 % (3128729)CaDiCaL version: 2.1.3 % 123.85/17.73 % (3128729)Termination reason: Inappropriate % 123.85/17.73 % (3128729)Time elapsed: 0.013 s % 123.85/17.73 % (3128729)Peak memory usage: 10 MB % 123.85/17.73 % (3128729)Instructions burned: 31 (million) % 123.85/17.73 % (3128729)------------------------------ % 123.85/17.73 % (3128729)------------------------------ % 123.85/17.73 % (3128731)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1293318449:fmbsr=1.3:i=225729_2880 on theBenchmark for (2880ds/225729Mi) % 123.85/17.73 % (3128731)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.85/17.73 % (3128731)Terminated due to inappropriate strategy. % 123.85/17.73 % (3128731)------------------------------ % 123.85/17.73 % (3128731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.85/17.73 % (3128731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.85/17.73 % (3128731)CaDiCaL version: 2.1.3 % 123.85/17.73 % (3128731)Termination reason: Inappropriate % 123.85/17.73 % (3128731)Time elapsed: 0.013 s % 123.85/17.73 % (3128731)Peak memory usage: 10 MB % 123.85/17.73 % (3128731)Instructions burned: 31 (million) % 123.85/17.73 % (3128731)------------------------------ % 123.85/17.73 % (3128731)------------------------------ % 123.85/17.73 % (3128733)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2252523802:fmbsr=2:i=185024:ins=7_2879 on theBenchmark for (2879ds/185024Mi) % 123.85/17.73 % (3128733)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.85/17.73 % (3128733)Terminated due to inappropriate strategy. % 123.85/17.73 % (3128733)------------------------------ % 123.85/17.73 % (3128733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.85/17.73 % (3128733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.85/17.73 % (3128733)CaDiCaL version: 2.1.3 % 123.85/17.73 % (3128733)Termination reason: Inappropriate % 123.85/17.73 % (3128733)Time elapsed: 0.013 s % 123.85/17.73 % (3128733)Peak memory usage: 10 MB % 123.85/17.73 % (3128733)Instructions burned: 31 (million) % 123.85/17.73 % (3128733)------------------------------ % 123.85/17.73 % (3128733)------------------------------ % 123.85/17.73 % (3128735)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3402774865:rtra=on_2879 on theBenchmark for (2879ds/0Mi) % 123.85/17.73 % (3128735)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.85/17.73 % (3128735)Terminated due to inappropriate strategy. % 123.85/17.73 % (3128735)------------------------------ % 123.85/17.73 % (3128735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.85/17.73 % (3128735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.85/17.73 % (3128735)CaDiCaL version: 2.1.3 % 123.85/17.73 % (3128735)Termination reason: Inappropriate % 123.85/17.73 % (3128735)Time elapsed: 0.013 s % 123.85/17.73 % (3128735)Peak memory usage: 10 MB % 123.85/17.73 % (3128735)Instructions burned: 31 (million) % 123.85/17.73 % (3128735)------------------------------ % 123.85/17.73 % (3128735)------------------------------ % 123.85/17.73 % (3128737)% WARNING: option uhcvi not known. % 123.85/17.73 % (3128737)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2565619997:i=271062:add=off:rtra=on:rawr=on_2879 on theBenchmark for (2879ds/271062Mi) % 153.73/21.91 % (3128691)Instruction limit reached! % 153.73/21.91 % (3128691)------------------------------ % 153.73/21.91 % (3128691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.73/21.91 % (3128691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.73/21.91 % (3128691)CaDiCaL version: 2.1.3 % 153.73/21.91 % (3128691)Termination reason: Instruction limit % 153.73/21.91 % (3128691)Termination phase: Saturation % 153.73/21.91 % (3128691)Time elapsed: 11.328 s % 153.73/21.91 % (3128691)Peak memory usage: 20 MB % 153.73/21.91 % (3128691)Instructions burned: 29340 (million) % 153.73/21.91 % (3128739)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2798306150:i=176048:add=on:rtra=on:rawr=on_2868 on theBenchmark for (2868ds/176048Mi) % 153.73/21.91 % (3128717)Instruction limit reached! % 153.73/21.91 % (3128717)------------------------------ % 153.73/21.91 % (3128717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.73/21.91 % (3128717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.73/21.91 % (3128717)CaDiCaL version: 2.1.3 % 153.73/21.91 % (3128717)Termination reason: Instruction limit % 153.73/21.91 % (3128717)Termination phase: Saturation % 153.73/21.91 % (3128717)Time elapsed: 4.110 s % 153.73/21.91 % (3128717)Peak memory usage: 98 MB % 153.73/21.91 % (3128717)Instructions burned: 17628 (million) % 153.73/21.91 % (3128982)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3651764567:i=206:fgj=on:rtra=on_2852 on theBenchmark for (2852ds/206Mi) % 153.73/21.91 % (3128982)Instruction limit reached! % 153.73/21.91 % (3128982)------------------------------ % 153.73/21.91 % (3128982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.73/21.91 % (3128982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.73/21.91 % (3128982)CaDiCaL version: 2.1.3 % 153.73/21.91 % (3128982)Termination reason: Instruction limit % 153.73/21.91 % (3128982)Termination phase: Saturation % 153.73/21.91 % (3128982)Time elapsed: 0.046 s % 153.73/21.91 % (3128982)Peak memory usage: 13 MB % 153.73/21.91 % (3128982)Instructions burned: 208 (million) % 153.73/21.91 % (3128996)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3856573818:i=232:rtra=on_2852 on theBenchmark for (2852ds/232Mi) % 153.73/21.91 % (3128996)Instruction limit reached! % 153.73/21.91 % (3128996)------------------------------ % 153.73/21.91 % (3128996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.73/21.91 % (3128996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.73/21.91 % (3128996)CaDiCaL version: 2.1.3 % 153.73/21.91 % (3128996)Termination reason: Instruction limit % 153.73/21.91 % (3128996)Termination phase: Saturation % 153.73/21.91 % (3128996)Time elapsed: 0.083 s % 153.73/21.91 % (3128996)Peak memory usage: 13 MB % 153.73/21.91 % (3128996)Instructions burned: 235 (million) % 153.73/21.91 % (3129021)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1319307433:i=262:rtra=on_2851 on theBenchmark for (2851ds/262Mi) % 153.73/21.91 % (3129021)Instruction limit reached! % 153.73/21.91 % (3129021)------------------------------ % 153.73/21.91 % (3129021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.73/21.91 % (3129021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.73/21.91 % (3129021)CaDiCaL version: 2.1.3 % 153.73/21.91 % (3129021)Termination reason: Instruction limit % 153.73/21.91 % (3129021)Termination phase: Saturation % 153.73/21.91 % (3129021)Time elapsed: 0.100 s % 153.73/21.91 % (3129021)Peak memory usage: 12 MB % 153.73/21.91 % (3129021)Instructions burned: 264 (million) % 153.73/21.91 % (3129032)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=197822325:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2849 on theBenchmark for (2849ds/318Mi) % 153.73/21.91 % (3129032)Instruction limit reached! % 153.73/21.91 % (3129032)------------------------------ % 153.73/21.91 % (3129032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.73/21.91 % (3129032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.73/21.91 % (3129032)CaDiCaL version: 2.1.3 % 153.73/21.91 % (3129032)Termination reason: Instruction limit % 153.73/21.91 % (3129032)Termination phase: Saturation % 153.73/21.91 % (3129032)Time elapsed: 0.128 s % 153.73/21.91 % (3129032)Peak memory usage: 14 MB % 153.73/21.91 % (3129032)Instructions burned: 320 (million) % 153.73/21.91 % (3129043)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2850648096:i=1428:nm=2:rtra=on_2848 on theBenchmark for (2848ds/1428Mi) % 207.32/29.55 % (3129043)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 207.32/29.55 % (3129043)Terminated due to inappropriate strategy. % 207.32/29.55 % (3129043)------------------------------ % 207.32/29.55 % (3129043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.32/29.55 % (3129043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.32/29.55 % (3129043)CaDiCaL version: 2.1.3 % 207.32/29.55 % (3129043)Termination reason: Inappropriate % 207.32/29.55 % (3129043)Time elapsed: 0.014 s % 207.32/29.55 % (3129043)Peak memory usage: 10 MB % 207.32/29.55 % (3129043)Instructions burned: 31 (million) % 207.32/29.55 % (3129043)------------------------------ % 207.32/29.55 % (3129043)------------------------------ % 207.32/29.55 % (3129047)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3701548358:i=262:bd=preordered:rtra=on:fsd=on_2848 on theBenchmark for (2848ds/262Mi) % 207.32/29.55 % (3129047)Instruction limit reached! % 207.32/29.55 % (3129047)------------------------------ % 207.32/29.55 % (3129047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.32/29.55 % (3129047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.32/29.55 % (3129047)CaDiCaL version: 2.1.3 % 207.32/29.55 % (3129047)Termination reason: Instruction limit % 207.32/29.55 % (3129047)Termination phase: Saturation % 207.32/29.55 % (3129047)Time elapsed: 0.170 s % 207.32/29.55 % (3129047)Peak memory usage: 13 MB % 207.32/29.55 % (3129047)Instructions burned: 262 (million) % 207.32/29.55 % (3129051)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=693928848:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2846 on theBenchmark for (2846ds/1368Mi) % 207.32/29.55 % (3129051)Instruction limit reached! % 207.32/29.55 % (3129051)------------------------------ % 207.32/29.55 % (3129051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.32/29.55 % (3129051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.32/29.55 % (3129051)CaDiCaL version: 2.1.3 % 207.32/29.55 % (3129051)Termination reason: Instruction limit % 207.32/29.55 % (3129051)Termination phase: Saturation % 207.32/29.55 % (3129051)Time elapsed: 1.045 s % 207.32/29.55 % (3129051)Peak memory usage: 16 MB % 207.32/29.55 % (3129051)Instructions burned: 1369 (million) % 207.32/29.55 % (3129075)ott-21_1_sil=16000:si=on:fs=off:random_seed=1851015829:i=360:av=off:fsr=off:rtra=on_2835 on theBenchmark for (2835ds/360Mi) % 207.32/29.55 % (3129075)Instruction limit reached! % 207.32/29.55 % (3129075)------------------------------ % 207.32/29.55 % (3129075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.32/29.55 % (3129075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.32/29.55 % (3129075)CaDiCaL version: 2.1.3 % 207.32/29.55 % (3129075)Termination reason: Instruction limit % 207.32/29.55 % (3129075)Termination phase: Saturation % 207.32/29.55 % (3129075)Time elapsed: 0.234 s % 207.32/29.55 % (3129075)Peak memory usage: 12 MB % 207.32/29.55 % (3129075)Instructions burned: 361 (million) % 207.32/29.55 % (3129077)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3592279185:i=954:bd=all:rtra=on_2832 on theBenchmark for (2832ds/954Mi) % 207.32/29.55 % (3129077)Instruction limit reached! % 207.32/29.55 % (3129077)------------------------------ % 207.32/29.55 % (3129077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.32/29.55 % (3129077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.32/29.55 % (3129077)CaDiCaL version: 2.1.3 % 207.32/29.55 % (3129077)Termination reason: Instruction limit % 207.32/29.55 % (3129077)Termination phase: Saturation % 207.32/29.55 % (3129077)Time elapsed: 0.708 s % 207.32/29.55 % (3129077)Peak memory usage: 14 MB % 207.32/29.55 % (3129077)Instructions burned: 955 (million) % 207.32/29.55 % (3129081)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1687483177:fmbsr=1.3:i=1730:ins=25:rtra=on_2825 on theBenchmark for (2825ds/1730Mi) % 207.32/29.55 % (3129081)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 207.32/29.55 % (3129081)Terminated due to inappropriate strategy. % 207.32/29.55 % (3129081)------------------------------ % 207.32/29.55 % (3129081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.32/29.55 % (3129081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.32/29.55 % (3129081)CaDiCaL version: 2.1.3 % 207.32/29.55 % (3129081)Termination reason: Inappropriate % 269.60/38.25 % (3129081)Time elapsed: 0.013 s % 269.60/38.25 % (3129081)Peak memory usage: 10 MB % 269.60/38.25 % (3129081)Instructions burned: 24 (million) % 269.60/38.25 % (3129081)------------------------------ % 269.60/38.25 % (3129081)------------------------------ % 269.60/38.25 % (3129083)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1892395579:i=2358:rtra=on_2824 on theBenchmark for (2824ds/2358Mi) % 269.60/38.25 % (3129083)Instruction limit reached! % 269.60/38.25 % (3129083)------------------------------ % 269.60/38.25 % (3129083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.60/38.25 % (3129083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.60/38.25 % (3129083)CaDiCaL version: 2.1.3 % 269.60/38.25 % (3129083)Termination reason: Instruction limit % 269.60/38.25 % (3129083)Termination phase: Saturation % 269.60/38.25 % (3129083)Time elapsed: 1.640 s % 269.60/38.25 % (3129083)Peak memory usage: 13 MB % 269.60/38.25 % (3129083)Instructions burned: 2358 (million) % 269.60/38.25 % (3129093)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4147718203:i=1778:ins=1:rtra=on_2808 on theBenchmark for (2808ds/1778Mi) % 269.60/38.25 % (3129093)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.60/38.25 % (3129093)Terminated due to inappropriate strategy. % 269.60/38.25 % (3129093)------------------------------ % 269.60/38.25 % (3129093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.60/38.25 % (3129093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.60/38.25 % (3129093)CaDiCaL version: 2.1.3 % 269.60/38.25 % (3129093)Termination reason: Inappropriate % 269.60/38.25 % (3129093)Time elapsed: 0.021 s % 269.60/38.25 % (3129093)Peak memory usage: 10 MB % 269.60/38.25 % (3129093)Instructions burned: 24 (million) % 269.60/38.25 % (3129093)------------------------------ % 269.60/38.25 % (3129093)------------------------------ % 269.60/38.25 % (3129095)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=1129816605:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2807 on theBenchmark for (2807ds/1384Mi) % 269.60/38.25 % (3129095)Instruction limit reached! % 269.60/38.25 % (3129095)------------------------------ % 269.60/38.25 % (3129095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.60/38.25 % (3129095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.60/38.25 % (3129095)CaDiCaL version: 2.1.3 % 269.60/38.25 % (3129095)Termination reason: Instruction limit % 269.60/38.25 % (3129095)Termination phase: Saturation % 269.60/38.25 % (3129095)Time elapsed: 1.020 s % 269.60/38.25 % (3129095)Peak memory usage: 14 MB % 269.60/38.25 % (3129095)Instructions burned: 1385 (million) % 269.60/38.25 % (3129109)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3643130145:i=1758:kws=inv_precedence:fsr=off:rtra=on_2797 on theBenchmark for (2797ds/1758Mi) % 269.60/38.25 % (3129109)Instruction limit reached! % 269.60/38.25 % (3129109)------------------------------ % 269.60/38.25 % (3129109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.60/38.25 % (3129109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.60/38.25 % (3129109)CaDiCaL version: 2.1.3 % 269.60/38.25 % (3129109)Termination reason: Instruction limit % 269.60/38.25 % (3129109)Termination phase: Saturation % 269.60/38.25 % (3129109)Time elapsed: 1.299 s % 269.60/38.25 % (3129109)Peak memory usage: 14 MB % 269.60/38.25 % (3129109)Instructions burned: 1758 (million) % 269.60/38.25 % (3129111)fmb+10_1_sil=64000:si=on:random_seed=1566058184:i=44122:nm=2:rtra=on:gsp=on_2783 on theBenchmark for (2783ds/44122Mi) % 269.60/38.25 % (3129111)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.60/38.25 % (3129111)Terminated due to inappropriate strategy. % 269.60/38.25 % (3129111)------------------------------ % 269.60/38.25 % (3129111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.60/38.25 % (3129111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.60/38.25 % (3129111)CaDiCaL version: 2.1.3 % 269.60/38.25 % (3129111)Termination reason: Inappropriate % 269.60/38.25 % (3129111)Time elapsed: 0.017 s % 269.60/38.25 % (3129111)Peak memory usage: 10 MB % 269.60/38.25 % (3129111)Instructions burned: 31 (million) % 269.60/38.25 % (3129111)------------------------------ % 269.60/38.25 % (3129111)------------------------------ % 269.60/38.25 % (3129113)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2945980006:i=19030:nm=5:rtTerminated % 300.13/42.54 % Vampire exiting % 300.13/42.54 Terminated %------------------------------------------------------------------------------