%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW742_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n011.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:42 PM UTC 2026 % Result : Timeout 292.15s 41.47s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW742_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.21 % Computer : n011.cluster.edu % 0.09/0.21 % Model : x86_64 x86_64 % 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.21 % Memory : 8046.5625MB % 0.09/0.21 % OS : Linux 6.8.0-71-generic % 0.09/0.21 % CPULimit : 300 % 0.09/0.21 % WCLimit : 300 % 0.09/0.21 % DateTime : Mon Sep 28 14:29:01 UTC 2026 % 0.09/0.21 % CPUTime : % 0.09/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.24 Running first-order model finding % 0.09/0.24 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.08/0.79 % (3424557)Will run a generic schedule for satisfiability detection. % 3.08/0.79 % (3424567)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3090819138:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.08/0.79 % (3424563)% WARNING: option uhcvi not known. % 3.08/0.79 % (3424562)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3432601395_2999 on theBenchmark for (2999ds/0Mi) % 3.08/0.79 % (3424565)dis+10_1_sil=32000:sp=arity:random_seed=2405278146:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.08/0.79 % (3424563)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3817788733:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.08/0.79 % (3424564)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3105116271:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.08/0.79 % (3424566)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2973844214:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.08/0.79 % (3424568)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=707615767:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.08/0.79 % (3424567)Instruction limit reached! % 3.08/0.79 % (3424567)------------------------------ % 3.08/0.79 % (3424567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.08/0.79 % (3424567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.08/0.79 % (3424567)CaDiCaL version: 2.1.3 % 3.08/0.79 % (3424567)Termination reason: Instruction limit % 3.08/0.79 % (3424567)Termination phase: Saturation % 3.08/0.79 % (3424567)Time elapsed: 0.040 s % 3.08/0.79 % (3424567)Peak memory usage: 15 MB % 3.08/0.79 % (3424567)Instructions burned: 135 (million) % 3.08/0.79 % (3424576)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1362829612:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.08/0.79 % (3424576)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.08/0.79 % (3424576)Terminated due to inappropriate strategy. % 3.08/0.79 % (3424576)------------------------------ % 3.08/0.79 % (3424576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.08/0.79 % (3424576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.08/0.79 % (3424576)CaDiCaL version: 2.1.3 % 3.08/0.79 % (3424576)Termination reason: Inappropriate % 3.08/0.79 % (3424576)Time elapsed: 0.008 s % 3.08/0.79 % (3424576)Peak memory usage: 11 MB % 3.08/0.79 % (3424576)Instructions burned: 32 (million) % 3.08/0.79 % (3424562)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.08/0.79 % (3424562)Terminated due to inappropriate strategy. % 3.08/0.79 % (3424562)------------------------------ % 3.08/0.79 % (3424562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.08/0.79 % (3424562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.08/0.79 % (3424562)CaDiCaL version: 2.1.3 % 3.08/0.79 % (3424562)Termination reason: Inappropriate % 3.08/0.79 % (3424562)Time elapsed: 0.053 s % 3.08/0.79 % (3424562)Peak memory usage: 12 MB % 3.08/0.79 % (3424562)Instructions burned: 112 (million) % 3.08/0.79 % (3424576)------------------------------ % 3.08/0.79 % (3424576)------------------------------ % 3.08/0.79 % (3424562)------------------------------ % 3.08/0.79 % (3424562)------------------------------ % 3.08/0.79 % (3424565)Instruction limit reached! % 3.08/0.79 % (3424565)------------------------------ % 3.08/0.79 % (3424565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.08/0.79 % (3424566)Instruction limit reached! % 3.08/0.79 % (3424566)------------------------------ % 3.08/0.79 % (3424566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.08/0.79 % (3424565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.08/0.79 % (3424566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.08/0.79 % (3424565)CaDiCaL version: 2.1.3 % 3.08/0.79 % (3424565)Termination reason: Instruction limit % 3.08/0.79 % (3424565)Termination phase: Saturation % 3.08/0.79 % (3424565)Time elapsed: 0.055 s % 3.08/0.79 % (3424565)Peak memory usage: 14 MB % 3.08/0.79 % (3424565)Instructions burned: 104 (million) % 3.08/0.79 % (3424566)CaDiCaL version: 2.1.3 % 3.08/0.79 % (3424566)Termination reason: Instruction limit % 3.08/0.79 % (3424566)Termination phase: Blocked clause elimination % 3.08/0.79 % (3424566)Time elapsed: 0.054 s % 3.08/0.79 % (3424566)Peak memory usage: 12 MB % 4.22/0.99 % (3424566)Instructions burned: 117 (million) % 4.22/0.99 % (3424578)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1623786372:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 4.22/0.99 % (3424579)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=225041605:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 4.22/0.99 % (3424581)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=36722972:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 4.22/0.99 % (3424580)ott-21_1_sil=16000:fs=off:random_seed=276262806:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 4.22/0.99 % (3424568)Instruction limit reached! % 4.22/0.99 % (3424568)------------------------------ % 4.22/0.99 % (3424568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.22/0.99 % (3424568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.22/0.99 % (3424568)CaDiCaL version: 2.1.3 % 4.22/0.99 % (3424568)Termination reason: Instruction limit % 4.22/0.99 % (3424568)Termination phase: Saturation % 4.22/0.99 % (3424568)Time elapsed: 0.090 s % 4.22/0.99 % (3424568)Peak memory usage: 15 MB % 4.22/0.99 % (3424568)Instructions burned: 159 (million) % 4.22/0.99 % (3424578)Instruction limit reached! % 4.22/0.99 % (3424578)------------------------------ % 4.22/0.99 % (3424578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.22/0.99 % (3424578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.22/0.99 % (3424578)CaDiCaL version: 2.1.3 % 4.22/0.99 % (3424578)Termination reason: Instruction limit % 4.22/0.99 % (3424578)Termination phase: Saturation % 4.22/0.99 % (3424578)Time elapsed: 0.034 s % 4.22/0.99 % (3424578)Peak memory usage: 14 MB % 4.22/0.99 % (3424578)Instructions burned: 133 (million) % 4.22/0.99 % (3424587)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2843972952:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 4.22/0.99 % (3424586)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1659856291:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 4.22/0.99 % (3424586)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.22/0.99 % (3424586)Terminated due to inappropriate strategy. % 4.22/0.99 % (3424586)------------------------------ % 4.22/0.99 % (3424586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.22/0.99 % (3424586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.22/0.99 % (3424586)CaDiCaL version: 2.1.3 % 4.22/0.99 % (3424586)Termination reason: Inappropriate % 4.22/0.99 % (3424586)Time elapsed: 0.022 s % 4.22/0.99 % (3424586)Peak memory usage: 12 MB % 4.22/0.99 % (3424586)Instructions burned: 49 (million) % 4.22/0.99 % (3424586)------------------------------ % 4.22/0.99 % (3424586)------------------------------ % 4.22/0.99 % (3424590)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=934311531:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 4.22/0.99 % (3424580)Instruction limit reached! % 4.22/0.99 % (3424580)------------------------------ % 4.22/0.99 % (3424580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.22/0.99 % (3424580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.22/0.99 % (3424580)CaDiCaL version: 2.1.3 % 4.22/0.99 % (3424580)Termination reason: Instruction limit % 4.22/0.99 % (3424580)Termination phase: Saturation % 4.22/0.99 % (3424580)Time elapsed: 0.086 s % 4.22/0.99 % (3424580)Peak memory usage: 14 MB % 4.22/0.99 % (3424580)Instructions burned: 180 (million) % 4.22/0.99 % (3424590)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.22/0.99 % (3424590)Terminated due to inappropriate strategy. % 4.22/0.99 % (3424590)------------------------------ % 4.22/0.99 % (3424590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.22/0.99 % (3424590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.22/0.99 % (3424590)CaDiCaL version: 2.1.3 % 4.22/0.99 % (3424590)Termination reason: Inappropriate % 4.22/0.99 % (3424590)Time elapsed: 0.017 s % 4.22/0.99 % (3424590)Peak memory usage: 11 MB % 4.22/0.99 % (3424590)Instructions burned: 35 (million) % 4.22/0.99 % (3424590)------------------------------ % 4.22/0.99 % (3424590)------------------------------ % 4.22/0.99 % (3424592)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=646321299:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 17.44/2.87 % (3424593)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1203194982:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 17.44/2.87 % (3424581)Instruction limit reached! % 17.44/2.87 % (3424581)------------------------------ % 17.44/2.87 % (3424581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.44/2.87 % (3424581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.44/2.87 % (3424581)CaDiCaL version: 2.1.3 % 17.44/2.87 % (3424581)Termination reason: Instruction limit % 17.44/2.87 % (3424581)Termination phase: Saturation % 17.44/2.87 % (3424581)Time elapsed: 0.270 s % 17.44/2.87 % (3424581)Peak memory usage: 16 MB % 17.44/2.87 % (3424581)Instructions burned: 478 (million) % 17.44/2.87 % (3424596)fmb+10_1_sil=64000:random_seed=4137544488:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 17.44/2.87 % (3424596)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.44/2.87 % (3424596)Terminated due to inappropriate strategy. % 17.44/2.87 % (3424596)------------------------------ % 17.44/2.87 % (3424596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.44/2.87 % (3424596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.44/2.87 % (3424596)CaDiCaL version: 2.1.3 % 17.44/2.87 % (3424596)Termination reason: Inappropriate % 17.44/2.87 % (3424596)Time elapsed: 0.015 s % 17.44/2.87 % (3424596)Peak memory usage: 11 MB % 17.44/2.87 % (3424596)Instructions burned: 35 (million) % 17.44/2.87 % (3424596)------------------------------ % 17.44/2.87 % (3424596)------------------------------ % 17.44/2.87 % (3424598)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4286470123:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 17.44/2.87 % (3424598)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.44/2.87 % (3424598)Terminated due to inappropriate strategy. % 17.44/2.87 % (3424598)------------------------------ % 17.44/2.87 % (3424598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.44/2.87 % (3424598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.44/2.87 % (3424598)CaDiCaL version: 2.1.3 % 17.44/2.87 % (3424598)Termination reason: Inappropriate % 17.44/2.87 % (3424598)Time elapsed: 0.014 s % 17.44/2.87 % (3424598)Peak memory usage: 11 MB % 17.44/2.87 % (3424598)Instructions burned: 33 (million) % 17.44/2.87 % (3424598)------------------------------ % 17.44/2.87 % (3424598)------------------------------ % 17.44/2.87 % (3424600)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1601359917:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 17.44/2.87 % (3424600)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.44/2.87 % (3424600)Terminated due to inappropriate strategy. % 17.44/2.87 % (3424600)------------------------------ % 17.44/2.87 % (3424600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.44/2.87 % (3424600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.44/2.87 % (3424600)CaDiCaL version: 2.1.3 % 17.44/2.87 % (3424600)Termination reason: Inappropriate % 17.44/2.87 % (3424600)Time elapsed: 0.015 s % 17.44/2.87 % (3424600)Peak memory usage: 11 MB % 17.44/2.87 % (3424600)Instructions burned: 35 (million) % 17.44/2.87 % (3424600)------------------------------ % 17.44/2.87 % (3424600)------------------------------ % 17.44/2.87 % (3424579)Instruction limit reached! % 17.44/2.87 % (3424579)------------------------------ % 17.44/2.87 % (3424579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.44/2.87 % (3424579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.44/2.87 % (3424579)CaDiCaL version: 2.1.3 % 17.44/2.87 % (3424579)Termination reason: Instruction limit % 17.44/2.87 % (3424579)Termination phase: Saturation % 17.44/2.87 % (3424579)Time elapsed: 0.395 s % 17.44/2.87 % (3424579)Peak memory usage: 19 MB % 17.44/2.87 % (3424579)Instructions burned: 684 (million) % 17.44/2.87 % (3424602)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1414623445:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 17.44/2.87 % (3424603)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1179787763:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 17.44/2.87 % (3424587)Instruction limit reached! % 23.68/3.69 % (3424587)------------------------------ % 23.68/3.69 % (3424587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.68/3.69 % (3424587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.68/3.69 % (3424587)CaDiCaL version: 2.1.3 % 23.68/3.69 % (3424587)Termination reason: Instruction limit % 23.68/3.69 % (3424587)Termination phase: Saturation % 23.68/3.69 % (3424587)Time elapsed: 0.382 s % 23.68/3.69 % (3424587)Peak memory usage: 20 MB % 23.68/3.69 % (3424587)Instructions burned: 1180 (million) % 23.68/3.69 % (3424606)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2581071826:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 23.68/3.69 % (3424606)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.68/3.69 % (3424606)Terminated due to inappropriate strategy. % 23.68/3.69 % (3424606)------------------------------ % 23.68/3.69 % (3424606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.68/3.69 % (3424606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.68/3.69 % (3424606)CaDiCaL version: 2.1.3 % 23.68/3.69 % (3424606)Termination reason: Inappropriate % 23.68/3.69 % (3424606)Time elapsed: 0.028 s % 23.68/3.69 % (3424606)Peak memory usage: 12 MB % 23.68/3.69 % (3424606)Instructions burned: 111 (million) % 23.68/3.69 % (3424606)------------------------------ % 23.68/3.69 % (3424606)------------------------------ % 23.68/3.69 % (3424608)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4182368213:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 23.68/3.69 % (3424608)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.68/3.69 % (3424608)Terminated due to inappropriate strategy. % 23.68/3.69 % (3424608)------------------------------ % 23.68/3.69 % (3424608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.68/3.69 % (3424608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.68/3.69 % (3424608)CaDiCaL version: 2.1.3 % 23.68/3.69 % (3424608)Termination reason: Inappropriate % 23.68/3.69 % (3424608)Time elapsed: 0.028 s % 23.68/3.69 % (3424608)Peak memory usage: 11 MB % 23.68/3.69 % (3424608)Instructions burned: 35 (million) % 23.68/3.69 % (3424608)------------------------------ % 23.68/3.70 % (3424608)------------------------------ % 23.68/3.70 % (3424610)ott-2_1_sil=16000:newcnf=on:random_seed=882139422:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 23.68/3.70 % (3424592)Instruction limit reached! % 23.68/3.70 % (3424592)------------------------------ % 23.68/3.70 % (3424592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.68/3.70 % (3424592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.68/3.70 % (3424592)CaDiCaL version: 2.1.3 % 23.68/3.70 % (3424592)Termination reason: Instruction limit % 23.68/3.70 % (3424592)Termination phase: Saturation % 23.68/3.70 % (3424592)Time elapsed: 0.403 s % 23.68/3.70 % (3424592)Peak memory usage: 20 MB % 23.68/3.70 % (3424592)Instructions burned: 693 (million) % 23.68/3.70 % (3424612)ott+10_1_sil=32000:tgt=ground:random_seed=480289956:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 23.68/3.70 % (3424593)Instruction limit reached! % 23.68/3.70 % (3424593)------------------------------ % 23.68/3.70 % (3424593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.68/3.70 % (3424593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.68/3.70 % (3424593)CaDiCaL version: 2.1.3 % 23.68/3.70 % (3424593)Termination reason: Instruction limit % 23.68/3.70 % (3424593)Termination phase: Saturation % 23.68/3.70 % (3424593)Time elapsed: 0.425 s % 23.68/3.70 % (3424593)Peak memory usage: 21 MB % 23.68/3.70 % (3424593)Instructions burned: 879 (million) % 23.68/3.70 % (3424614)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3157599107:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 23.68/3.70 % (3424614)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.68/3.70 % (3424614)Terminated due to inappropriate strategy. % 23.68/3.70 % (3424614)------------------------------ % 23.68/3.70 % (3424614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.68/3.70 % (3424614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.68/3.70 % (3424614)CaDiCaL version: 2.1.3 % 23.68/3.70 % (3424614)Termination reason: Inappropriate % 23.68/3.70 % (3424614)Time elapsed: 0.053 s % 23.68/3.70 % (3424614)Peak memory usage: 12 MB % 23.68/3.70 % (3424614)Instructions burned: 112 (million) % 89.69/12.98 % (3424614)------------------------------ % 89.69/12.98 % (3424614)------------------------------ % 89.69/12.98 % (3424616)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1383304829:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 89.69/12.98 % (3424610)Instruction limit reached! % 89.69/12.98 % (3424610)------------------------------ % 89.69/12.98 % (3424610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.69/12.98 % (3424610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.69/12.98 % (3424610)CaDiCaL version: 2.1.3 % 89.69/12.98 % (3424610)Termination reason: Instruction limit % 89.69/12.98 % (3424610)Termination phase: Saturation % 89.69/12.98 % (3424610)Time elapsed: 0.269 s % 89.69/12.98 % (3424610)Peak memory usage: 20 MB % 89.69/12.98 % (3424610)Instructions burned: 870 (million) % 89.69/12.98 % (3424618)dis+21_1_sil=32000:sas=cadical:random_seed=1913259548:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 89.69/12.98 % (3424603)Instruction limit reached! % 89.69/12.98 % (3424603)------------------------------ % 89.69/12.98 % (3424603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.69/12.98 % (3424603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.69/12.98 % (3424603)CaDiCaL version: 2.1.3 % 89.69/12.98 % (3424603)Termination reason: Instruction limit % 89.69/12.98 % (3424603)Termination phase: Saturation % 89.69/12.98 % (3424603)Time elapsed: 0.697 s % 89.69/12.98 % (3424603)Peak memory usage: 25 MB % 89.69/12.98 % (3424603)Instructions burned: 1474 (million) % 89.69/12.98 % (3424620)ott+11_1_sil=16000:gs=on:random_seed=2871380404:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 89.69/12.98 % (3424618)Instruction limit reached! % 89.69/12.98 % (3424618)------------------------------ % 89.69/12.98 % (3424618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.69/12.98 % (3424618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.69/12.98 % (3424618)CaDiCaL version: 2.1.3 % 89.69/12.98 % (3424618)Termination reason: Instruction limit % 89.69/12.98 % (3424618)Termination phase: Saturation % 89.69/12.98 % (3424618)Time elapsed: 1.093 s % 89.69/12.98 % (3424618)Peak memory usage: 34 MB % 89.69/12.98 % (3424618)Instructions burned: 3773 (million) % 89.69/12.98 % (3424622)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2083751041:fmbsr=1.6:i=67534_2979 on theBenchmark for (2979ds/67534Mi) % 89.69/12.98 % (3424622)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 89.69/12.98 % (3424622)Terminated due to inappropriate strategy. % 89.69/12.98 % (3424622)------------------------------ % 89.69/12.98 % (3424622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.69/12.98 % (3424622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.69/12.98 % (3424622)CaDiCaL version: 2.1.3 % 89.69/12.98 % (3424622)Termination reason: Inappropriate % 89.69/12.98 % (3424622)Time elapsed: 0.008 s % 89.69/12.98 % (3424622)Peak memory usage: 11 MB % 89.69/12.98 % (3424622)Instructions burned: 35 (million) % 89.69/12.98 % (3424622)------------------------------ % 89.69/12.98 % (3424622)------------------------------ % 89.69/12.98 % (3424624)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=702186437:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2979 on theBenchmark for (2979ds/4591Mi) % 89.69/12.98 % (3424620)Instruction limit reached! % 89.69/12.98 % (3424620)------------------------------ % 89.69/12.98 % (3424620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.69/12.98 % (3424620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.69/12.98 % (3424620)CaDiCaL version: 2.1.3 % 89.69/12.98 % (3424620)Termination reason: Instruction limit % 89.69/12.98 % (3424620)Termination phase: Saturation % 89.69/12.98 % (3424620)Time elapsed: 1.254 s % 89.69/12.98 % (3424620)Peak memory usage: 27 MB % 89.69/12.98 % (3424620)Instructions burned: 2251 (million) % 89.69/12.98 % (3424626)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=753572392:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 89.69/12.98 % (3424616)Instruction limit reached! % 89.69/12.98 % (3424616)------------------------------ % 89.69/12.98 % (3424616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.69/12.98 % (3424616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.69/12.98 % (3424616)CaDiCaL version: 2.1.3 % 135.85/19.41 % (3424616)Termination reason: Instruction limit % 135.85/19.41 % (3424616)Termination phase: Saturation % 135.85/19.41 % (3424616)Time elapsed: 1.858 s % 135.85/19.41 % (3424616)Peak memory usage: 31 MB % 135.85/19.41 % (3424616)Instructions burned: 3512 (million) % 135.85/19.41 % (3424628)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3875047142:i=5211_2973 on theBenchmark for (2973ds/5211Mi) % 135.85/19.41 % (3424602)Instruction limit reached! % 135.85/19.41 % (3424602)------------------------------ % 135.85/19.41 % (3424602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.85/19.41 % (3424602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.85/19.41 % (3424602)CaDiCaL version: 2.1.3 % 135.85/19.41 % (3424602)Termination reason: Instruction limit % 135.85/19.41 % (3424602)Termination phase: Saturation % 135.85/19.41 % (3424602)Time elapsed: 2.735 s % 135.85/19.41 % (3424602)Peak memory usage: 42 MB % 135.85/19.41 % (3424602)Instructions burned: 5131 (million) % 135.85/19.41 % (3424630)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1733227056:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 135.85/19.41 % (3424630)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.85/19.41 % (3424630)Terminated due to inappropriate strategy. % 135.85/19.41 % (3424630)------------------------------ % 135.85/19.41 % (3424630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.85/19.41 % (3424630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.85/19.41 % (3424630)CaDiCaL version: 2.1.3 % 135.85/19.41 % (3424630)Termination reason: Inappropriate % 135.85/19.41 % (3424630)Time elapsed: 0.033 s % 135.85/19.41 % (3424630)Peak memory usage: 12 MB % 135.85/19.41 % (3424630)Instructions burned: 71 (million) % 135.85/19.41 % (3424630)------------------------------ % 135.85/19.41 % (3424630)------------------------------ % 135.85/19.41 % (3424632)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1051965399:fmbsr=2:i=46332_2966 on theBenchmark for (2966ds/46332Mi) % 135.85/19.41 % (3424632)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.85/19.41 % (3424632)Terminated due to inappropriate strategy. % 135.85/19.41 % (3424632)------------------------------ % 135.85/19.41 % (3424632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.85/19.41 % (3424632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.85/19.41 % (3424632)CaDiCaL version: 2.1.3 % 135.85/19.41 % (3424632)Termination reason: Inappropriate % 135.85/19.41 % (3424632)Time elapsed: 0.015 s % 135.85/19.41 % (3424632)Peak memory usage: 11 MB % 135.85/19.41 % (3424632)Instructions burned: 35 (million) % 135.85/19.41 % (3424632)------------------------------ % 135.85/19.41 % (3424632)------------------------------ % 135.85/19.41 % (3424634)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1554438232:i=14071_2966 on theBenchmark for (2966ds/14071Mi) % 135.85/19.41 % (3424634)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.85/19.41 % (3424634)Terminated due to inappropriate strategy. % 135.85/19.41 % (3424634)------------------------------ % 135.85/19.41 % (3424634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.85/19.41 % (3424634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.85/19.41 % (3424634)CaDiCaL version: 2.1.3 % 135.85/19.41 % (3424634)Termination reason: Inappropriate % 135.85/19.41 % (3424634)Time elapsed: 0.015 s % 135.85/19.41 % (3424634)Peak memory usage: 11 MB % 135.85/19.41 % (3424634)Instructions burned: 35 (million) % 135.85/19.41 % (3424634)------------------------------ % 135.85/19.41 % (3424634)------------------------------ % 135.85/19.41 % (3424636)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3193220335:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi) % 135.85/19.41 % (3424624)Instruction limit reached! % 135.85/19.41 % (3424624)------------------------------ % 135.85/19.41 % (3424624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.85/19.41 % (3424624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.85/19.41 % (3424624)CaDiCaL version: 2.1.3 % 135.85/19.41 % (3424624)Termination reason: Instruction limit % 135.85/19.41 % (3424624)Termination phase: Saturation % 135.85/19.41 % (3424624)Time elapsed: 1.394 s % 135.85/19.41 % (3424624)Peak memory usage: 46 MB % 135.85/19.41 % (3424624)Instructions burned: 4594 (million) % 135.85/19.41 % (3424638)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1376790744:i=8173:av=off_2965 on theBenchmark for (2965ds/8173Mi) % 137.93/19.78 % (3424612)Instruction limit reached! % 137.93/19.78 % (3424612)------------------------------ % 137.93/19.78 % (3424612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.93/19.78 % (3424612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.93/19.78 % (3424612)CaDiCaL version: 2.1.3 % 137.93/19.78 % (3424612)Termination reason: Instruction limit % 137.93/19.78 % (3424612)Termination phase: Saturation % 137.93/19.78 % (3424612)Time elapsed: 3.176 s % 137.93/19.78 % (3424612)Peak memory usage: 31 MB % 137.93/19.78 % (3424612)Instructions burned: 5115 (million) % 137.93/19.78 % (3424640)dis+10_16:1_sil=16000:random_seed=802397986:i=9155:fsr=off_2961 on theBenchmark for (2961ds/9155Mi) % 137.93/19.78 % (3424628)Instruction limit reached! % 137.93/19.78 % (3424628)------------------------------ % 137.93/19.78 % (3424628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.93/19.78 % (3424628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.93/19.78 % (3424628)CaDiCaL version: 2.1.3 % 137.93/19.78 % (3424628)Termination reason: Instruction limit % 137.93/19.78 % (3424628)Termination phase: Saturation % 137.93/19.78 % (3424628)Time elapsed: 2.697 s % 137.93/19.78 % (3424628)Peak memory usage: 47 MB % 137.93/19.78 % (3424628)Instructions burned: 5212 (million) % 137.93/19.78 % (3424642)ott-3_8_sil=64000:random_seed=3720213728:i=20139:bs=on_2946 on theBenchmark for (2946ds/20139Mi) % 137.93/19.78 % (3424638)Instruction limit reached! % 137.93/19.78 % (3424638)------------------------------ % 137.93/19.78 % (3424638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.93/19.78 % (3424638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.93/19.78 % (3424638)CaDiCaL version: 2.1.3 % 137.93/19.78 % (3424638)Termination reason: Instruction limit % 137.93/19.78 % (3424638)Termination phase: Saturation % 137.93/19.78 % (3424638)Time elapsed: 2.765 s % 137.93/19.78 % (3424638)Peak memory usage: 47 MB % 137.93/19.78 % (3424638)Instructions burned: 8174 (million) % 137.93/19.78 % (3424644)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2144650323:fmbsr=2:i=32576_2937 on theBenchmark for (2937ds/32576Mi) % 137.93/19.78 % (3424644)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 137.93/19.78 % (3424644)Terminated due to inappropriate strategy. % 137.93/19.78 % (3424644)------------------------------ % 137.93/19.78 % (3424644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.93/19.78 % (3424644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.93/19.78 % (3424644)CaDiCaL version: 2.1.3 % 137.93/19.78 % (3424644)Termination reason: Inappropriate % 137.93/19.78 % (3424644)Time elapsed: 0.028 s % 137.93/19.78 % (3424644)Peak memory usage: 12 MB % 137.93/19.78 % (3424644)Instructions burned: 112 (million) % 137.93/19.78 % (3424644)------------------------------ % 137.93/19.78 % (3424644)------------------------------ % 137.93/19.78 % (3424646)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2789113052:i=11404_2937 on theBenchmark for (2937ds/11404Mi) % 137.93/19.78 % (3424640)Instruction limit reached! % 137.93/19.78 % (3424640)------------------------------ % 137.93/19.78 % (3424640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.93/19.78 % (3424640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.93/19.78 % (3424640)CaDiCaL version: 2.1.3 % 137.93/19.78 % (3424640)Termination reason: Instruction limit % 137.93/19.78 % (3424640)Termination phase: Saturation % 137.93/19.78 % (3424640)Time elapsed: 4.819 s % 137.93/19.78 % (3424640)Peak memory usage: 56 MB % 137.93/19.78 % (3424640)Instructions burned: 9155 (million) % 137.93/19.78 % (3424648)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1187150314:i=14134_2913 on theBenchmark for (2913ds/14134Mi) % 137.93/19.78 % (3424646)Instruction limit reached! % 137.93/19.78 % (3424646)------------------------------ % 137.93/19.78 % (3424646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.93/19.78 % (3424646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.93/19.78 % (3424646)CaDiCaL version: 2.1.3 % 137.93/19.78 % (3424646)Termination reason: Instruction limit % 137.93/19.78 % (3424646)Termination phase: Saturation % 137.93/19.78 % (3424646)Time elapsed: 4.072 s % 137.93/19.78 % (3424646)Peak memory usage: 48 MB % 137.93/19.78 % (3424646)Instructions burned: 11404 (million) % 137.93/19.78 % (3424650)dis+33_16_sil=32000:sac=on:random_seed=145189474:i=15851:nm=0_2896 on theBenchmark for (2896ds/15851Mi) % 137.93/19.78 % (3424636)Instruction limit reached! % 137.93/19.78 % (3424636)------------------------------ % 137.93/19.78 % (3424636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.57/27.42 % (3424636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.57/27.42 % (3424636)CaDiCaL version: 2.1.3 % 192.57/27.42 % (3424636)Termination reason: Instruction limit % 192.57/27.42 % (3424636)Termination phase: Saturation % 192.57/27.42 % (3424636)Time elapsed: 9.329 s % 192.57/27.42 % (3424636)Peak memory usage: 77 MB % 192.57/27.42 % (3424636)Instructions burned: 22566 (million) % 192.57/27.42 % (3424652)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=166839996:avsq=on:i=17627:add=on:amm=off_2872 on theBenchmark for (2872ds/17627Mi) % 192.57/27.42 % (3424642)Instruction limit reached! % 192.57/27.42 % (3424642)------------------------------ % 192.57/27.42 % (3424642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.57/27.42 % (3424642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.57/27.42 % (3424642)CaDiCaL version: 2.1.3 % 192.57/27.42 % (3424642)Termination reason: Instruction limit % 192.57/27.42 % (3424642)Termination phase: Saturation % 192.57/27.42 % (3424642)Time elapsed: 11.061 s % 192.57/27.42 % (3424642)Peak memory usage: 59 MB % 192.57/27.42 % (3424642)Instructions burned: 20139 (million) % 192.57/27.42 % (3424928)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1872954262:s2a=on:i=53295_2835 on theBenchmark for (2835ds/53295Mi) % 192.57/27.42 % (3424626)Instruction limit reached! % 192.57/27.42 % (3424626)------------------------------ % 192.57/27.42 % (3424626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.57/27.42 % (3424626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.57/27.42 % (3424626)CaDiCaL version: 2.1.3 % 192.57/27.42 % (3424626)Termination reason: Instruction limit % 192.57/27.42 % (3424626)Termination phase: Saturation % 192.57/27.42 % (3424626)Time elapsed: 14.099 s % 192.57/27.42 % (3424626)Peak memory usage: 155 MB % 192.57/27.42 % (3424626)Instructions burned: 29341 (million) % 192.57/27.42 % (3424936)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1354529470:i=26857:ins=20_2833 on theBenchmark for (2833ds/26857Mi) % 192.57/27.42 % (3424936)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.57/27.42 % (3424936)Terminated due to inappropriate strategy. % 192.57/27.42 % (3424936)------------------------------ % 192.57/27.42 % (3424936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.57/27.42 % (3424936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.57/27.42 % (3424936)CaDiCaL version: 2.1.3 % 192.57/27.42 % (3424936)Termination reason: Inappropriate % 192.57/27.42 % (3424936)Time elapsed: 0.017 s % 192.57/27.42 % (3424936)Peak memory usage: 11 MB % 192.57/27.42 % (3424936)Instructions burned: 35 (million) % 192.57/27.42 % (3424936)------------------------------ % 192.57/27.42 % (3424936)------------------------------ % 192.57/27.42 % (3424942)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1483908730:i=28120:bs=on:fsr=off_2832 on theBenchmark for (2832ds/28120Mi) % 192.57/27.42 % (3424648)Instruction limit reached! % 192.57/27.42 % (3424648)------------------------------ % 192.57/27.42 % (3424648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.57/27.42 % (3424648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.57/27.42 % (3424648)CaDiCaL version: 2.1.3 % 192.57/27.42 % (3424648)Termination reason: Instruction limit % 192.57/27.42 % (3424648)Termination phase: Saturation % 192.57/27.42 % (3424648)Time elapsed: 10.341 s % 192.57/27.42 % (3424648)Peak memory usage: 56 MB % 192.57/27.42 % (3424648)Instructions burned: 14135 (million) % 192.57/27.42 % (3425019)fmb+10_1_sil=256000:fmbss=7:random_seed=676779101:fmbsr=1.6:i=182295_2809 on theBenchmark for (2809ds/182295Mi) % 192.57/27.42 % (3425019)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.57/27.42 % (3425019)Terminated due to inappropriate strategy. % 192.57/27.42 % (3425019)------------------------------ % 192.57/27.42 % (3425019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.57/27.42 % (3425019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.57/27.42 % (3425019)CaDiCaL version: 2.1.3 % 192.57/27.42 % (3425019)Termination reason: Inappropriate % 192.57/27.42 % (3425019)Time elapsed: 0.028 s % 192.57/27.42 % (3425019)Peak memory usage: 11 MB % 192.57/27.42 % (3425019)Instructions burned: 35 (million) % 192.57/27.42 % (3425019)------------------------------ % 192.57/27.42 % (3425019)------------------------------ % 192.57/27.42 % (3425022)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2296089961:i=44625:gsp=on_2808 on theBenchmark for (2808ds/44625Mi) % 205.48/29.21 % (3425022)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.48/29.21 % (3425022)Terminated due to inappropriate strategy. % 205.48/29.21 % (3425022)------------------------------ % 205.48/29.21 % (3425022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.48/29.21 % (3425022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.48/29.21 % (3425022)CaDiCaL version: 2.1.3 % 205.48/29.21 % (3425022)Termination reason: Inappropriate % 205.48/29.21 % (3425022)Time elapsed: 0.035 s % 205.48/29.21 % (3425022)Peak memory usage: 11 MB % 205.48/29.21 % (3425022)Instructions burned: 51 (million) % 205.48/29.21 % (3425022)------------------------------ % 205.48/29.21 % (3425022)------------------------------ % 205.48/29.21 % (3425027)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4294218036:i=160505_2808 on theBenchmark for (2808ds/160505Mi) % 205.48/29.21 % (3425027)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.48/29.21 % (3425027)Terminated due to inappropriate strategy. % 205.48/29.21 % (3425027)------------------------------ % 205.48/29.21 % (3425027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.48/29.21 % (3425027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.48/29.21 % (3425027)CaDiCaL version: 2.1.3 % 205.48/29.21 % (3425027)Termination reason: Inappropriate % 205.48/29.21 % (3425027)Time elapsed: 0.016 s % 205.48/29.21 % (3425027)Peak memory usage: 11 MB % 205.48/29.21 % (3425027)Instructions burned: 35 (million) % 205.48/29.21 % (3425027)------------------------------ % 205.48/29.21 % (3425027)------------------------------ % 205.48/29.21 % (3425030)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1003152668:fmbsr=1.3:i=225729_2807 on theBenchmark for (2807ds/225729Mi) % 205.48/29.21 % (3425030)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.48/29.21 % (3425030)Terminated due to inappropriate strategy. % 205.48/29.21 % (3425030)------------------------------ % 205.48/29.21 % (3425030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.48/29.21 % (3425030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.48/29.21 % (3425030)CaDiCaL version: 2.1.3 % 205.48/29.21 % (3425030)Termination reason: Inappropriate % 205.48/29.21 % (3425030)Time elapsed: 0.026 s % 205.48/29.21 % (3425030)Peak memory usage: 11 MB % 205.48/29.21 % (3425030)Instructions burned: 35 (million) % 205.48/29.21 % (3425030)------------------------------ % 205.48/29.21 % (3425030)------------------------------ % 205.48/29.21 % (3425035)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1782640963:fmbsr=2:i=185024:ins=7_2806 on theBenchmark for (2806ds/185024Mi) % 205.48/29.21 % (3425035)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.48/29.21 % (3425035)Terminated due to inappropriate strategy. % 205.48/29.21 % (3425035)------------------------------ % 205.48/29.21 % (3425035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.48/29.21 % (3425035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.48/29.21 % (3425035)CaDiCaL version: 2.1.3 % 205.48/29.21 % (3425035)Termination reason: Inappropriate % 205.48/29.21 % (3425035)Time elapsed: 0.025 s % 205.48/29.21 % (3425035)Peak memory usage: 11 MB % 205.48/29.21 % (3425035)Instructions burned: 35 (million) % 205.48/29.21 % (3425035)------------------------------ % 205.48/29.21 % (3425035)------------------------------ % 205.48/29.21 % (3425037)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=909334200:rtra=on_2806 on theBenchmark for (2806ds/0Mi) % 205.48/29.21 % (3425037)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.48/29.21 % (3425037)Terminated due to inappropriate strategy. % 205.48/29.21 % (3425037)------------------------------ % 205.48/29.21 % (3425037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.48/29.21 % (3425037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.48/29.21 % (3425037)CaDiCaL version: 2.1.3 % 205.48/29.21 % (3425037)Termination reason: Inappropriate % 205.48/29.21 % (3425037)Time elapsed: 0.076 s % 205.48/29.21 % (3425037)Peak memory usage: 12 MB % 205.48/29.21 % (3425037)Instructions burned: 98 (million) % 205.48/29.21 % (3425037)------------------------------ % 205.48/29.21 % (3425037)------------------------------ % 205.48/29.21 % (3425043)% WARNING: option uhcvi not known. % 205.48/29.21 % (3425043)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=824169390:i=271062:add=off:rtra=on:rawr=on_2804 on theBenchmark for (2804ds/271062Mi) % 232.78/33.08 % (3424650)Instruction limit reached! % 232.78/33.08 % (3424650)------------------------------ % 232.78/33.08 % (3424650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.78/33.08 % (3424650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.78/33.08 % (3424650)CaDiCaL version: 2.1.3 % 232.78/33.08 % (3424650)Termination reason: Instruction limit % 232.78/33.08 % (3424650)Termination phase: Clausification % 232.78/33.08 % (3424650)Time elapsed: 10.781 s % 232.78/33.08 % (3424650)Peak memory usage: 8630 MB % 232.78/33.08 % (3424650)Instructions burned: 15852 (million) % 232.78/33.08 % (3425096)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3372475765:i=176048:add=on:rtra=on:rawr=on_2777 on theBenchmark for (2777ds/176048Mi) % 232.78/33.08 % (3424652)Instruction limit reached! % 232.78/33.08 % (3424652)------------------------------ % 232.78/33.08 % (3424652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.78/33.08 % (3424652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.78/33.08 % (3424652)CaDiCaL version: 2.1.3 % 232.78/33.08 % (3424652)Termination reason: Instruction limit % 232.78/33.08 % (3424652)Termination phase: Saturation % 232.78/33.08 % (3424652)Time elapsed: 13.605 s % 232.78/33.08 % (3424652)Peak memory usage: 252 MB % 232.78/33.08 % (3424652)Instructions burned: 17627 (million) % 232.78/33.08 % (3425140)dis+10_1_sil=32000:si=on:sp=arity:random_seed=340842382:i=206:fgj=on:rtra=on_2735 on theBenchmark for (2735ds/206Mi) % 232.78/33.08 % (3425140)Instruction limit reached! % 232.78/33.08 % (3425140)------------------------------ % 232.78/33.08 % (3425140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.78/33.08 % (3425140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.78/33.08 % (3425140)CaDiCaL version: 2.1.3 % 232.78/33.08 % (3425140)Termination reason: Instruction limit % 232.78/33.08 % (3425140)Termination phase: Saturation % 232.78/33.08 % (3425140)Time elapsed: 0.199 s % 232.78/33.08 % (3425140)Peak memory usage: 16 MB % 232.78/33.08 % (3425140)Instructions burned: 206 (million) % 232.78/33.08 % (3425143)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4111017872:i=232:rtra=on_2733 on theBenchmark for (2733ds/232Mi) % 232.78/33.08 % (3425143)Instruction limit reached! % 232.78/33.08 % (3425143)------------------------------ % 232.78/33.08 % (3425143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.78/33.08 % (3425143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.78/33.08 % (3425143)CaDiCaL version: 2.1.3 % 232.78/33.08 % (3425143)Termination reason: Instruction limit % 232.78/33.08 % (3425143)Termination phase: Blocked clause elimination % 232.78/33.08 % (3425143)Time elapsed: 0.181 s % 232.78/33.08 % (3425143)Peak memory usage: 12 MB % 232.78/33.08 % (3425143)Instructions burned: 232 (million) % 232.78/33.08 % (3425145)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2757383224:i=262:rtra=on_2731 on theBenchmark for (2731ds/262Mi) % 232.78/33.08 % (3425145)Instruction limit reached! % 232.78/33.08 % (3425145)------------------------------ % 232.78/33.08 % (3425145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.78/33.08 % (3425145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.78/33.08 % (3425145)CaDiCaL version: 2.1.3 % 232.78/33.08 % (3425145)Termination reason: Instruction limit % 232.78/33.08 % (3425145)Termination phase: Saturation % 232.78/33.08 % (3425145)Time elapsed: 0.099 s % 232.78/33.08 % (3425145)Peak memory usage: 17 MB % 232.78/33.08 % (3425145)Instructions burned: 264 (million) % 232.78/33.08 % (3425148)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2037964512:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2730 on theBenchmark for (2730ds/318Mi) % 232.78/33.08 % (3425148)Instruction limit reached! % 232.78/33.08 % (3425148)------------------------------ % 232.78/33.08 % (3425148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.78/33.08 % (3425148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.78/33.08 % (3425148)CaDiCaL version: 2.1.3 % 232.78/33.08 % (3425148)Termination reason: Instruction limit % 232.78/33.08 % (3425148)Termination phase: Saturation % 232.78/33.08 % (3425148)Time elapsed: 0.167 s % 232.78/33.08 % (3425148)Peak memory usage: 17 MB % 232.78/33.08 % (3425148)Instructions burned: 319 (million) % 232.78/33.08 % (3425151)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2965922193:i=1428:nm=2:rtra=on_2728 on theBenchmark for (2728ds/1428Mi) % 292.15/41.47 % (3425151)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 292.15/41.47 % (3425151)Terminated due to inappropriate strategy. % 292.15/41.47 % (3425151)------------------------------ % 292.15/41.47 % (3425151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.15/41.47 % (3425151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.15/41.47 % (3425151)CaDiCaL version: 2.1.3 % 292.15/41.47 % (3425151)Termination reason: Inappropriate % 292.15/41.47 % (3425151)Time elapsed: 0.009 s % 292.15/41.47 % (3425151)Peak memory usage: 11 MB % 292.15/41.47 % (3425151)Instructions burned: 34 (million) % 292.15/41.47 % (3425151)------------------------------ % 292.15/41.47 % (3425151)------------------------------ % 292.15/41.47 % (3425153)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2801199279:i=262:bd=preordered:rtra=on:fsd=on_2728 on theBenchmark for (2728ds/262Mi) % 292.15/41.47 % (3425153)Instruction limit reached! % 292.15/41.47 % (3425153)------------------------------ % 292.15/41.47 % (3425153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.15/41.47 % (3425153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.15/41.47 % (3425153)CaDiCaL version: 2.1.3 % 292.15/41.47 % (3425153)Termination reason: Instruction limit % 292.15/41.47 % (3425153)Termination phase: Saturation % 292.15/41.47 % (3425153)Time elapsed: 0.105 s % 292.15/41.47 % (3425153)Peak memory usage: 15 MB % 292.15/41.47 % (3425153)Instructions burned: 262 (million) % 292.15/41.47 % (3425156)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=634652642:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2727 on theBenchmark for (2727ds/1368Mi) % 292.15/41.47 % (3425156)Instruction limit reached! % 292.15/41.47 % (3425156)------------------------------ % 292.15/41.47 % (3425156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.15/41.47 % (3425156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.15/41.47 % (3425156)CaDiCaL version: 2.1.3 % 292.15/41.47 % (3425156)Termination reason: Instruction limit % 292.15/41.47 % (3425156)Termination phase: Saturation % 292.15/41.47 % (3425156)Time elapsed: 0.762 s % 292.15/41.47 % (3425156)Peak memory usage: 28 MB % 292.15/41.47 % (3425156)Instructions burned: 1370 (million) % 292.15/41.47 % (3425161)ott-21_1_sil=16000:si=on:fs=off:random_seed=3407584645:i=360:av=off:fsr=off:rtra=on_2719 on theBenchmark for (2719ds/360Mi) % 292.15/41.47 % (3425161)Instruction limit reached! % 292.15/41.47 % (3425161)------------------------------ % 292.15/41.47 % (3425161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.15/41.47 % (3425161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.15/41.47 % (3425161)CaDiCaL version: 2.1.3 % 292.15/41.47 % (3425161)Termination reason: Instruction limit % 292.15/41.47 % (3425161)Termination phase: Saturation % 292.15/41.47 % (3425161)Time elapsed: 0.189 s % 292.15/41.47 % (3425161)Peak memory usage: 14 MB % 292.15/41.47 % (3425161)Instructions burned: 361 (million) % 292.15/41.47 % (3425163)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=910613349:i=954:bd=all:rtra=on_2716 on theBenchmark for (2716ds/954Mi) % 292.15/41.47 % (3425163)Instruction limit reached! % 292.15/41.47 % (3425163)------------------------------ % 292.15/41.47 % (3425163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.15/41.47 % (3425163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.15/41.47 % (3425163)CaDiCaL version: 2.1.3 % 292.15/41.47 % (3425163)Termination reason: Instruction limit % 292.15/41.47 % (3425163)Termination phase: Saturation % 292.15/41.47 % (3425163)Time elapsed: 0.526 s % 292.15/41.47 % (3425163)Peak memory usage: 18 MB % 292.15/41.47 % (3425163)Instructions burned: 954 (million) % 292.15/41.47 % (3425166)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=135821933:fmbsr=1.3:i=1730:ins=25:rtra=on_2711 on theBenchmark for (2711ds/1730Mi) % 292.15/41.47 % (3425166)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 292.15/41.47 % (3425166)Terminated due to inappropriate strategy. % 292.15/41.47 % (3425166)------------------------------ % 292.15/41.47 % (3425166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.15/41.47 % (3425166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.15/41.47 % (3425166)CaDiCaL versTerminated % 300.04/42.54 % Vampire exiting % 300.04/42.54 Terminated %------------------------------------------------------------------------------