%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX214+1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n026.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:45 PM UTC 2026 % Result : Timeout 300.01s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWX214+1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n026.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 15:14:41 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/0.22 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 % 14.65/2.30 % (3927529)Will run a generic schedule for satisfiability detection. % 14.65/2.30 % (3927537)dis+10_1_sil=32000:sp=arity:random_seed=2631058569:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 14.65/2.30 % (3927535)% WARNING: option uhcvi not known. % 14.65/2.30 % (3927534)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2470108459_2999 on theBenchmark for (2999ds/0Mi) % 14.65/2.30 % (3927535)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1822714455:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 14.65/2.30 % (3927536)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2117453278:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 14.65/2.30 % (3927538)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2389089156:i=116_2999 on theBenchmark for (2999ds/116Mi) % 14.65/2.30 % (3927539)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=479916118:i=131_2999 on theBenchmark for (2999ds/131Mi) % 14.65/2.30 % (3927540)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=378205953:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 14.65/2.30 % Detected minimum model sizes of [3] % 14.65/2.30 % Detected maximum model sizes of [max] % 14.65/2.30 % TRYING [3] % 14.65/2.30 % TRYING [4] % 14.65/2.30 % (3927537)Instruction limit reached! % 14.65/2.30 % (3927537)------------------------------ % 14.65/2.30 % (3927537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.65/2.30 % (3927537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.65/2.30 % (3927537)CaDiCaL version: 2.1.3 % 14.65/2.30 % (3927537)Termination reason: Instruction limit % 14.65/2.30 % (3927537)Termination phase: Saturation % 14.65/2.30 % (3927537)Time elapsed: 0.032 s % 14.65/2.30 % (3927537)Peak memory usage: 12 MB % 14.65/2.30 % (3927537)Instructions burned: 106 (million) % 14.65/2.30 % TRYING [5] % 14.65/2.30 % (3927548)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3908726973:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 14.65/2.30 % Detected minimum model sizes of [3] % 14.65/2.30 % Detected maximum model sizes of [max] % 14.65/2.30 % TRYING [3] % 14.65/2.30 % TRYING [4] % 14.65/2.30 % TRYING [5] % 14.65/2.30 % (3927538)Instruction limit reached! % 14.65/2.30 % (3927538)------------------------------ % 14.65/2.30 % (3927538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.65/2.30 % (3927538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.65/2.30 % (3927538)CaDiCaL version: 2.1.3 % 14.65/2.30 % (3927538)Termination reason: Instruction limit % 14.65/2.30 % (3927538)Termination phase: Saturation % 14.65/2.30 % (3927538)Time elapsed: 0.061 s % 14.65/2.30 % (3927538)Peak memory usage: 12 MB % 14.65/2.30 % (3927538)Instructions burned: 116 (million) % 14.65/2.30 % (3927539)Instruction limit reached! % 14.65/2.30 % (3927539)------------------------------ % 14.65/2.30 % (3927539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.65/2.30 % (3927539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.65/2.30 % (3927539)CaDiCaL version: 2.1.3 % 14.65/2.30 % (3927539)Termination reason: Instruction limit % 14.65/2.30 % (3927539)Termination phase: Saturation % 14.65/2.30 % (3927539)Time elapsed: 0.072 s % 14.65/2.30 % (3927539)Peak memory usage: 12 MB % 14.65/2.30 % (3927539)Instructions burned: 132 (million) % 14.65/2.30 % (3927550)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2106212170:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 14.65/2.30 % TRYING [6] % 14.65/2.30 % TRYING [6] % 14.65/2.30 % (3927551)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=3464610118:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 14.65/2.30 % (3927540)Instruction limit reached! % 14.65/2.30 % (3927540)------------------------------ % 14.65/2.30 % (3927540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.65/2.30 % (3927540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.65/2.30 % (3927540)CaDiCaL version: 2.1.3 % 14.65/2.30 % (3927540)Termination reason: Instruction limit % 14.65/2.30 % (3927540)Termination phase: Saturation % 14.65/2.30 % (3927540)Time elapsed: 0.097 s % 14.65/2.30 % (3927540)Peak memory usage: 14 MB % 14.65/2.30 % (3927540)Instructions burned: 159 (million) % 14.65/2.30 % (3927554)ott-21_1_sil=16000:fs=off:random_seed=1051877284:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 14.65/2.30 % (3927550)Instruction limit reached! % 32.35/5.03 % (3927550)------------------------------ % 32.35/5.03 % (3927550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.35/5.03 % (3927550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.35/5.03 % (3927550)CaDiCaL version: 2.1.3 % 32.35/5.03 % (3927550)Termination reason: Instruction limit % 32.35/5.03 % (3927550)Termination phase: Saturation % 32.35/5.03 % (3927550)Time elapsed: 0.069 s % 32.35/5.03 % (3927550)Peak memory usage: 12 MB % 32.35/5.03 % (3927550)Instructions burned: 133 (million) % 32.35/5.03 % (3927556)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=786322597:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 32.35/5.03 % (3927548)Instruction limit reached! % 32.35/5.03 % (3927548)------------------------------ % 32.35/5.03 % (3927548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.35/5.03 % (3927548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.35/5.03 % (3927548)CaDiCaL version: 2.1.3 % 32.35/5.03 % (3927548)Termination reason: Instruction limit % 32.35/5.03 % (3927548)Termination phase: Finite model building constraint generation % 32.35/5.03 % (3927548)Time elapsed: 0.153 s % 32.35/5.03 % (3927548)Peak memory usage: 35 MB % 32.35/5.03 % (3927548)Instructions burned: 720 (million) % 32.35/5.03 % (3927558)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3116612327:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 32.35/5.03 % Detected minimum model sizes of [3] % 32.35/5.03 % Detected maximum model sizes of [max] % 32.35/5.03 % TRYING [3] % 32.35/5.03 % TRYING [4] % 32.35/5.03 % TRYING [7] % 32.35/5.03 % (3927554)Instruction limit reached! % 32.35/5.03 % (3927554)------------------------------ % 32.35/5.03 % (3927554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.35/5.03 % (3927554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.35/5.03 % (3927554)CaDiCaL version: 2.1.3 % 32.35/5.03 % (3927554)Termination reason: Instruction limit % 32.35/5.03 % (3927554)Termination phase: Saturation % 32.35/5.03 % (3927554)Time elapsed: 0.098 s % 32.35/5.03 % (3927554)Peak memory usage: 12 MB % 32.35/5.03 % (3927554)Instructions burned: 180 (million) % 32.35/5.03 % TRYING [5] % 32.35/5.03 % (3927560)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2330608928:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 32.35/5.03 % TRYING [6] % 32.35/5.03 % (3927558)Instruction limit reached! % 32.35/5.03 % (3927558)------------------------------ % 32.35/5.03 % (3927558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.35/5.03 % (3927558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.35/5.03 % (3927558)CaDiCaL version: 2.1.3 % 32.35/5.03 % (3927558)Termination reason: Instruction limit % 32.35/5.03 % (3927558)Termination phase: Finite model building SAT solving % 32.35/5.03 % (3927558)Time elapsed: 0.177 s % 32.35/5.03 % (3927558)Peak memory usage: 28 MB % 32.35/5.03 % (3927558)Instructions burned: 869 (million) % 32.35/5.03 % (3927562)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1169542449:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 32.35/5.03 % (3927556)Instruction limit reached! % 32.35/5.03 % (3927556)------------------------------ % 32.35/5.03 % (3927556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.35/5.03 % (3927556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.35/5.03 % (3927556)CaDiCaL version: 2.1.3 % 32.35/5.03 % (3927556)Termination reason: Instruction limit % 32.35/5.03 % (3927556)Termination phase: Saturation % 32.35/5.03 % (3927556)Time elapsed: 0.268 s % 32.35/5.03 % (3927556)Peak memory usage: 14 MB % 32.35/5.03 % (3927556)Instructions burned: 477 (million) % 32.35/5.03 % (3927551)Instruction limit reached! % 32.35/5.03 % (3927551)------------------------------ % 32.35/5.03 % (3927551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.35/5.03 % (3927551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.35/5.03 % (3927551)CaDiCaL version: 2.1.3 % 32.35/5.03 % (3927551)Termination reason: Instruction limit % 32.35/5.03 % (3927551)Termination phase: Saturation % 32.35/5.03 % (3927551)Time elapsed: 0.352 s % 32.35/5.03 % (3927551)Peak memory usage: 17 MB % 32.35/5.03 % (3927551)Instructions burned: 686 (million) % 32.35/5.03 % TRYING [8] % 32.35/5.03 % (3927564)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=2160046110:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi) % 63.59/9.26 % (3927565)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2284764796:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi) % 63.59/9.26 % TRYING [14] % 63.59/9.26 % (3927562)Instruction limit reached! % 63.59/9.26 % (3927562)------------------------------ % 63.59/9.26 % (3927562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.59/9.26 % (3927562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.59/9.26 % (3927562)CaDiCaL version: 2.1.3 % 63.59/9.26 % (3927562)Termination reason: Instruction limit % 63.59/9.26 % (3927562)Termination phase: Finite model building constraint generation % 63.59/9.26 % (3927562)Time elapsed: 0.192 s % 63.59/9.26 % (3927562)Peak memory usage: 86 MB % 63.59/9.26 % (3927562)Instructions burned: 889 (million) % 63.59/9.26 % (3927568)fmb+10_1_sil=64000:random_seed=3233067742:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 63.59/9.26 % Detected minimum model sizes of [3] % 63.59/9.26 % Detected maximum model sizes of [max] % 63.59/9.26 % TRYING [3] % 63.59/9.26 % TRYING [4] % 63.59/9.26 % TRYING [5] % 63.59/9.26 % TRYING [6] % 63.59/9.26 % TRYING [7] % 63.59/9.26 % (3927564)Instruction limit reached! % 63.59/9.26 % (3927564)------------------------------ % 63.59/9.26 % (3927564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.59/9.26 % (3927564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.59/9.26 % (3927564)CaDiCaL version: 2.1.3 % 63.59/9.26 % (3927564)Termination reason: Instruction limit % 63.59/9.26 % (3927564)Termination phase: Saturation % 63.59/9.26 % (3927564)Time elapsed: 0.398 s % 63.59/9.26 % (3927564)Peak memory usage: 22 MB % 63.59/9.26 % (3927564)Instructions burned: 692 (million) % 63.59/9.26 % (3927570)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1486605552:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi) % 63.59/9.26 % Detected minimum model sizes of [3] % 63.59/9.26 % Detected maximum model sizes of [max] % 63.59/9.26 % TRYING [20] % 63.59/9.26 % (3927560)Instruction limit reached! % 63.59/9.26 % (3927560)------------------------------ % 63.59/9.26 % (3927560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.59/9.26 % (3927560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.59/9.26 % (3927560)CaDiCaL version: 2.1.3 % 63.59/9.26 % (3927560)Termination reason: Instruction limit % 63.59/9.26 % (3927560)Termination phase: Saturation % 63.59/9.26 % (3927560)Time elapsed: 0.653 s % 63.59/9.26 % (3927560)Peak memory usage: 19 MB % 63.59/9.26 % (3927560)Instructions burned: 1180 (million) % 63.59/9.26 % TRYING [9] % 63.59/9.26 % (3927572)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=967980923:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 63.59/9.26 % Detected minimum model sizes of [3] % 63.59/9.26 % Detected maximum model sizes of [max] % 63.59/9.26 % TRYING [8] % 63.59/9.26 % (3927565)Instruction limit reached! % 63.59/9.26 % (3927565)------------------------------ % 63.59/9.26 % (3927565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.59/9.26 % (3927565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.59/9.26 % (3927565)CaDiCaL version: 2.1.3 % 63.59/9.26 % (3927565)Termination reason: Instruction limit % 63.59/9.26 % (3927565)Termination phase: Saturation % 63.59/9.26 % (3927565)Time elapsed: 0.465 s % 63.59/9.26 % (3927565)Peak memory usage: 17 MB % 63.59/9.26 % (3927565)Instructions burned: 880 (million) % 63.59/9.26 % (3927574)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=646460455:i=5131_2990 on theBenchmark for (2990ds/5131Mi) % 63.59/9.26 % TRYING [8] % 63.59/9.26 % (3927572)Instruction limit reached! % 63.59/9.26 % (3927572)------------------------------ % 63.59/9.26 % (3927572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.59/9.26 % (3927572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.59/9.26 % (3927572)CaDiCaL version: 2.1.3 % 63.59/9.26 % (3927572)Termination reason: Instruction limit % 63.59/9.26 % (3927572)Termination phase: Finite model building constraint generation % 63.59/9.26 % (3927572)Time elapsed: 0.355 s % 63.59/9.26 % (3927572)Peak memory usage: 71 MB % 63.59/9.26 % (3927572)Instructions burned: 921 (million) % 63.59/9.26 % (3927576)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2173265636:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi) % 63.59/9.26 % TRYING [10] % 63.59/9.26 % TRYING [9] % 63.59/9.26 % (3927576)Instruction limit reached! % 63.59/9.26 % (3927576)------------------------------ % 63.59/9.26 % (3927576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.79/27.17 % (3927576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.79/27.17 % (3927576)CaDiCaL version: 2.1.3 % 190.79/27.17 % (3927576)Termination reason: Instruction limit % 190.79/27.17 % (3927576)Termination phase: Saturation % 190.79/27.17 % (3927576)Time elapsed: 0.739 s % 190.79/27.17 % (3927576)Peak memory usage: 29 MB % 190.79/27.17 % (3927576)Instructions burned: 1474 (million) % 190.79/27.17 % (3927578)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=144748092:i=6324_2979 on theBenchmark for (2979ds/6324Mi) % 190.79/27.17 % Detected minimum model sizes of [3] % 190.79/27.17 % Detected maximum model sizes of [max] % 190.79/27.17 % TRYING [77] % 190.79/27.17 % TRYING [11] % 190.79/27.17 % TRYING [10] % 190.79/27.17 % (3927574)Instruction limit reached! % 190.79/27.17 % (3927574)------------------------------ % 190.79/27.17 % (3927574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.79/27.17 % (3927574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.79/27.17 % (3927574)CaDiCaL version: 2.1.3 % 190.79/27.17 % (3927574)Termination reason: Instruction limit % 190.79/27.17 % (3927574)Termination phase: Saturation % 190.79/27.17 % (3927574)Time elapsed: 2.496 s % 190.79/27.17 % (3927574)Peak memory usage: 32 MB % 190.79/27.17 % (3927574)Instructions burned: 5131 (million) % 190.79/27.17 % (3927581)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1045907894:fmbsr=2.30978:i=2174_2965 on theBenchmark for (2965ds/2174Mi) % 190.79/27.17 % Detected minimum model sizes of [3] % 190.79/27.17 % Detected maximum model sizes of [max] % 190.79/27.17 % TRYING [16] % 190.79/27.17 % (3927581)Instruction limit reached! % 190.79/27.17 % (3927581)------------------------------ % 190.79/27.17 % (3927581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.79/27.17 % (3927581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.79/27.17 % (3927581)CaDiCaL version: 2.1.3 % 190.79/27.17 % (3927581)Termination reason: Instruction limit % 190.79/27.17 % (3927581)Termination phase: Finite model building constraint generation % 190.79/27.17 % (3927581)Time elapsed: 0.744 s % 190.79/27.17 % (3927581)Peak memory usage: 135 MB % 190.79/27.17 % (3927581)Instructions burned: 2175 (million) % 190.79/27.17 % (3927583)ott-2_1_sil=16000:newcnf=on:random_seed=2850615004:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi) % 190.79/27.17 % (3927570)Instruction limit reached! % 190.79/27.17 % (3927570)------------------------------ % 190.79/27.17 % (3927570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.79/27.17 % (3927570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.79/27.17 % (3927570)CaDiCaL version: 2.1.3 % 190.79/27.17 % (3927570)Termination reason: Instruction limit % 190.79/27.17 % (3927570)Termination phase: Finite model building constraint generation % 190.79/27.17 % (3927570)Time elapsed: 3.411 s % 190.79/27.17 % (3927570)Peak memory usage: 637 MB % 190.79/27.17 % (3927570)Instructions burned: 9517 (million) % 190.79/27.17 % (3927585)ott+10_1_sil=32000:tgt=ground:random_seed=1388202890:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi) % 190.79/27.17 % (3927578)Instruction limit reached! % 190.79/27.17 % (3927578)------------------------------ % 190.79/27.17 % (3927578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.79/27.17 % (3927578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.79/27.17 % (3927578)CaDiCaL version: 2.1.3 % 190.79/27.17 % (3927578)Termination reason: Instruction limit % 190.79/27.17 % (3927578)Termination phase: Finite model building constraint generation % 190.79/27.17 % (3927578)Time elapsed: 2.397 s % 190.79/27.17 % (3927578)Peak memory usage: 523 MB % 190.79/27.17 % (3927578)Instructions burned: 6326 (million) % 190.79/27.17 % (3927587)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1658158097:i=54282_2954 on theBenchmark for (2954ds/54282Mi) % 190.79/27.17 % Detected minimum model sizes of [3] % 190.79/27.17 % Detected maximum model sizes of [max] % 190.79/27.17 % TRYING [3] % 190.79/27.17 % TRYING [4] % 190.79/27.17 % TRYING [5] % 190.79/27.17 % TRYING [6] % 190.79/27.17 % (3927583)Instruction limit reached! % 190.79/27.17 % (3927583)------------------------------ % 190.79/27.17 % (3927583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.79/27.17 % (3927583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.79/27.17 % (3927583)CaDiCaL version: 2.1.3 % 190.79/27.17 % (3927583)Termination reason: Instruction limit % 190.79/27.17 % (3927583)Termination phase: Saturation % 190.79/27.17 % (3927583)Time elapsed: 0.486 s % 190.79/27.17 % (3927583)Peak memory usage: 16 MB % 190.79/27.17 % (3927583)Instructions burned: 870 (million) % 190.79/27.17 % TRYING [7] % 190.79/27.17 % (3927589)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3352465592:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi) % 278.49/39.52 % TRYING [8] % 278.49/39.52 % TRYING [12] % 278.49/39.52 % TRYING [9] % 278.49/39.52 % (3927568)Instruction limit reached! % 278.49/39.52 % (3927568)------------------------------ % 278.49/39.52 % (3927568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.49/39.52 % (3927568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.49/39.52 % (3927568)CaDiCaL version: 2.1.3 % 278.49/39.52 % (3927568)Termination reason: Instruction limit % 278.49/39.52 % (3927568)Termination phase: Finite model building SAT solving % 278.49/39.52 % (3927568)Time elapsed: 4.984 s % 278.49/39.52 % (3927568)Peak memory usage: 222 MB % 278.49/39.52 % (3927568)Instructions burned: 22062 (million) % 278.49/39.52 % (3927591)dis+21_1_sil=32000:sas=cadical:random_seed=2901933632:i=3773:amm=off_2943 on theBenchmark for (2943ds/3773Mi) % 278.49/39.52 % TRYING [10] % 278.49/39.52 % (3927589)Instruction limit reached! % 278.49/39.52 % (3927589)------------------------------ % 278.49/39.52 % (3927589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.49/39.52 % (3927589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.49/39.52 % (3927589)CaDiCaL version: 2.1.3 % 278.49/39.52 % (3927589)Termination reason: Instruction limit % 278.49/39.52 % (3927589)Termination phase: Saturation % 278.49/39.52 % (3927589)Time elapsed: 1.806 s % 278.49/39.52 % (3927589)Peak memory usage: 35 MB % 278.49/39.52 % (3927589)Instructions burned: 3512 (million) % 278.49/39.52 % (3927593)ott+11_1_sil=16000:gs=on:random_seed=2681864691:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2933 on theBenchmark for (2933ds/2251Mi) % 278.49/39.52 % (3927591)Instruction limit reached! % 278.49/39.52 % (3927591)------------------------------ % 278.49/39.52 % (3927591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.49/39.52 % (3927591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.49/39.52 % (3927591)CaDiCaL version: 2.1.3 % 278.49/39.52 % (3927591)Termination reason: Instruction limit % 278.49/39.52 % (3927591)Termination phase: Saturation % 278.49/39.52 % (3927591)Time elapsed: 1.031 s % 278.49/39.52 % (3927591)Peak memory usage: 30 MB % 278.49/39.52 % (3927591)Instructions burned: 3773 (million) % 278.49/39.52 % (3927595)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=395165314:fmbsr=1.6:i=67534_2933 on theBenchmark for (2933ds/67534Mi) % 278.49/39.52 % Detected minimum model sizes of [3] % 278.49/39.52 % Detected maximum model sizes of [max] % 278.49/39.52 % TRYING [7] % 278.49/39.52 % (3927585)Instruction limit reached! % 278.49/39.52 % (3927585)------------------------------ % 278.49/39.52 % (3927585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.49/39.52 % (3927585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.49/39.52 % (3927585)CaDiCaL version: 2.1.3 % 278.49/39.52 % (3927585)Termination reason: Instruction limit % 278.49/39.52 % (3927585)Termination phase: Saturation % 278.49/39.52 % (3927585)Time elapsed: 2.813 s % 278.49/39.52 % (3927585)Peak memory usage: 42 MB % 278.49/39.52 % (3927585)Instructions burned: 5115 (million) % 278.49/39.52 % (3927597)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1913969353:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2927 on theBenchmark for (2927ds/4591Mi) % 278.49/39.52 % TRYING [8] % 278.49/39.52 % (3927593)Instruction limit reached! % 278.49/39.52 % (3927593)------------------------------ % 278.49/39.52 % (3927593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.49/39.52 % (3927593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.49/39.52 % (3927593)CaDiCaL version: 2.1.3 % 278.49/39.52 % (3927593)Termination reason: Instruction limit % 278.49/39.52 % (3927593)Termination phase: Saturation % 278.49/39.52 % (3927593)Time elapsed: 0.935 s % 278.49/39.52 % (3927593)Peak memory usage: 14 MB % 278.49/39.52 % (3927593)Instructions burned: 2254 (million) % 278.49/39.52 % (3927599)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1942329763:i=29340_2924 on theBenchmark for (2924ds/29340Mi) % 278.49/39.52 % TRYING [11] % 278.49/39.52 % TRYING [13] % 278.49/39.52 % (3927597)Instruction limit reached! % 278.49/39.52 % (3927597)------------------------------ % 278.49/39.52 % (3927597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.49/39.52 % (3927597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.49/39.52 % (3927597)CaDiCaL version: 2.1.3 % 278.49/39.52 % (3927597)Termination reason: Instruction limit % 278.49/39.52 % (3927597)Termination phase: Saturation % 300.01/42.63 % (3927597)Time elapsed: 1.759 s % 300.01/42.63 % (3927597)Peak memory usage: 29 MB % 300.01/42.63 % (3927597)Instructions burned: 4594 (million) % 300.01/42.63 % (3927601)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2141230556:i=5211_2909 on theBenchmark for (2909ds/5211Mi) % 300.01/42.63 % TRYING [12] % 300.01/42.63 % TRYING [9] % 300.01/42.63 % (3927601)Instruction limit reached! % 300.01/42.63 % (3927601)------------------------------ % 300.01/42.63 % (3927601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.63 % (3927601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.63 % (3927601)CaDiCaL version: 2.1.3 % 300.01/42.63 % (3927601)Termination reason: Instruction limit % 300.01/42.63 % (3927601)Termination phase: Saturation % 300.01/42.63 % (3927601)Time elapsed: 2.663 s % 300.01/42.63 % (3927601)Peak memory usage: 43 MB % 300.01/42.63 % (3927601)Instructions burned: 5212 (million) % 300.01/42.63 % (3927603)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2660297018:i=5497:nm=2_2882 on theBenchmark for (2882ds/5497Mi) % 300.01/42.63 % Detected minimum model sizes of [3] % 300.01/42.63 % Detected maximum model sizes of [max] % 300.01/42.63 % TRYING [17] % 300.01/42.63 % TRYING [14] % 300.01/42.63 % TRYING [13] % 300.01/42.63 % (3927603)Instruction limit reached! % 300.01/42.63 % (3927603)------------------------------ % 300.01/42.63 % (3927603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.63 % (3927603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.63 % (3927603)CaDiCaL version: 2.1.3 % 300.01/42.63 % (3927603)Termination reason: Instruction limit % 300.01/42.63 % (3927603)Termination phase: Finite model building constraint generation % 300.01/42.63 % (3927603)Time elapsed: 1.934 s % 300.01/42.63 % (3927603)Peak memory usage: 372 MB % 300.01/42.63 % (3927603)Instructions burned: 5498 (million) % 300.01/42.63 % (3927606)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2954950617:fmbsr=2:i=46332_2862 on theBenchmark for (2862ds/46332Mi) % 300.01/42.63 % Detected minimum model sizes of [3] % 300.01/42.63 % Detected maximum model sizes of [max] % 300.01/42.63 % TRYING [15] % 300.01/42.63 % TRYING [10] % 300.01/42.63 % TRYING [14] % 300.01/42.63 % TRYING [15] % 300.01/42.63 % (3927599)Instruction limit reached! % 300.01/42.63 % (3927599)------------------------------ % 300.01/42.63 % (3927599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.63 % (3927599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.63 % (3927599)CaDiCaL version: 2.1.3 % 300.01/42.63 % (3927599)Termination reason: Instruction limit % 300.01/42.63 % (3927599)Termination phase: Saturation % 300.01/42.63 % (3927599)Time elapsed: 14.084 s % 300.01/42.63 % (3927599)Peak memory usage: 263 MB % 300.01/42.63 % (3927599)Instructions burned: 29341 (million) % 300.01/42.63 % (3927608)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1319634252:i=14071_2783 on theBenchmark for (2783ds/14071Mi) % 300.01/42.63 % Detected minimum model sizes of [3] % 300.01/42.63 % Detected maximum model sizes of [max] % 300.01/42.63 % TRYING [12] % 300.01/42.63 % TRYING [15] % 300.01/42.63 % (3927587)Instruction limit reached! % 300.01/42.63 % (3927587)------------------------------ % 300.01/42.63 % (3927587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.63 % (3927587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.63 % (3927587)CaDiCaL version: 2.1.3 % 300.01/42.63 % (3927587)Termination reason: Instruction limit % 300.01/42.63 % (3927587)Termination phase: Finite model building constraint generation % 300.01/42.63 % (3927587)Time elapsed: 19.384 s % 300.01/42.63 % (3927587)Peak memory usage: 1022 MB % 300.01/42.63 % (3927587)Instructions burned: 54285 (million) % 300.01/42.63 % (3927610)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3884605038:i=22565:add=on:rawr=on_2759 on theBenchmark for (2759ds/22565Mi) % 300.01/42.63 % (3927595)Instruction limit reached! % 300.01/42.63 % (3927595)------------------------------ % 300.01/42.63 % (3927595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.63 % (3927595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.63 % (3927595)CaDiCaL version: 2.1.3 % 300.01/42.63 % (3927595)Termination reason: Instruction limit % 300.01/42.63 % (3927595)Termination phase: Finite model building SAT solving % 300.01/42.63 % (3927595)Time elapsed: 17.778 s % 300.01/42.63 % (3927595)Peak memory usage: 242 MB % 300.01/42.63 % (3927595)Instructions burned: 67538 (million) % 300.01/42.63 % (3927612)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2022098221:i=8173:av=off_2755 on theBenchmark for (2755ds/8173Mi) % 300.01/42.63 % TRYING [13] % 300.01/42.63 % (3927612)Inst % 300.01/42.63 Terminated % 300.01/42.63 % Vampire exiting % 300.01/42.64 Terminated %------------------------------------------------------------------------------