%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : HWV063+1 : TPTP v9.3.1. Bugfixed v5.5.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/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 11:16:16 AM UTC 2026
% Result : Satisfiable 139.58s 29.92s
% Output : FiniteModel 139.58s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff('declare_$i1',type,
'fmb_$i_1': $i ).
tff('declare_$i2',type,
'fmb_$i_2': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] :
( ( X = 'fmb_$i_1' )
| ( X = 'fmb_$i_2' ) ) ).
tff('distinct_domain_$i',axiom,
'fmb_$i_1' != 'fmb_$i_2' ).
tff(declare_true,type,
true: $i ).
tff(true_definition,axiom,
true = 'fmb_$i_1' ).
tff(declare_false,type,
false: $i ).
tff(false_definition,axiom,
false = 'fmb_$i_2' ).
tff(declare_p,type,
p: $i > $o ).
tff(predicate_p,axiom,
( p('fmb_$i_1')
& ~ p('fmb_$i_2') ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV063+1 : TPTP v9.3.1. Bugfixed v5.5.1.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.16/0.42 % Computer : n009.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Sun Sep 27 11:20:15 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.25/0.49 Running first-order model finding
% 0.25/0.49 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
% 74.61/16.45 % (1879882)Will run a generic schedule for satisfiability detection.
% 74.61/16.45 % (1879909)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1743914518:i=131_2936 on theBenchmark for (2936ds/131Mi)
% 74.61/16.45 % (1879905)% WARNING: option uhcvi not known.
% 74.61/16.45 % (1879905)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3851290522:i=135531:add=off:rawr=on_2936 on theBenchmark for (2936ds/135531Mi)
% 74.61/16.45 % (1879904)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4068831615_2936 on theBenchmark for (2936ds/0Mi)
% 74.61/16.45 % (1879907)dis+10_1_sil=32000:sp=arity:random_seed=968568962:i=103:fgj=on_2936 on theBenchmark for (2936ds/103Mi)
% 74.61/16.45 % (1879910)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2417099720:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2936 on theBenchmark for (2936ds/159Mi)
% 74.61/16.45 % (1879906)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3865060232:i=88024:add=on:rawr=on_2936 on theBenchmark for (2936ds/88024Mi)
% 74.61/16.45 % (1879908)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3619964299:i=116_2936 on theBenchmark for (2936ds/116Mi)
% 74.61/16.45 % (1879909)Instruction limit reached!
% 74.61/16.45 % (1879909)------------------------------
% 74.61/16.45 % (1879909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 74.61/16.45 % (1879909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.61/16.45 % (1879909)CaDiCaL version: 2.1.3
% 74.61/16.45 % (1879909)Termination reason: Instruction limit
% 74.61/16.45 % (1879909)Termination phase: Preprocessing 1
% 74.61/16.45 % (1879909)Time elapsed: 0.109 s
% 74.61/16.45 % (1879909)Peak memory usage: 44 MB
% 74.61/16.45 % (1879909)Instructions burned: 131 (million)
% 74.61/16.45 % (1879918)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3803189805:i=714:nm=2_2935 on theBenchmark for (2935ds/714Mi)
% 74.61/16.45 % (1879907)Instruction limit reached!
% 74.61/16.45 % (1879907)------------------------------
% 74.61/16.45 % (1879907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 74.61/16.45 % (1879907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.61/16.45 % (1879907)CaDiCaL version: 2.1.3
% 74.61/16.45 % (1879907)Termination reason: Instruction limit
% 74.61/16.45 % (1879907)Termination phase: Preprocessing 1
% 74.61/16.45 % (1879907)Time elapsed: 0.164 s
% 74.61/16.45 % (1879907)Peak memory usage: 43 MB
% 74.61/16.45 % (1879907)Instructions burned: 103 (million)
% 74.61/16.45 % (1879908)Instruction limit reached!
% 74.61/16.45 % (1879908)------------------------------
% 74.61/16.45 % (1879908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 74.61/16.45 % (1879908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.61/16.45 % (1879908)CaDiCaL version: 2.1.3
% 74.61/16.45 % (1879908)Termination reason: Instruction limit
% 74.61/16.45 % (1879908)Termination phase: Unused predicate definition removal
% 74.61/16.45 % (1879908)Time elapsed: 0.182 s
% 74.61/16.45 % (1879908)Peak memory usage: 43 MB
% 74.61/16.45 % (1879908)Instructions burned: 116 (million)
% 74.61/16.45 % (1879920)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1453367622:i=131:bd=preordered:fsd=on_2934 on theBenchmark for (2934ds/131Mi)
% 74.61/16.45 % (1879910)Instruction limit reached!
% 74.61/16.45 % (1879910)------------------------------
% 74.61/16.45 % (1879910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 74.61/16.45 % (1879910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.61/16.45 % (1879910)CaDiCaL version: 2.1.3
% 74.61/16.45 % (1879910)Termination reason: Instruction limit
% 74.61/16.45 % (1879910)Termination phase: Unused predicate definition removal
% 74.61/16.45 % (1879910)Time elapsed: 0.241 s
% 74.61/16.45 % (1879910)Peak memory usage: 43 MB
% 74.61/16.45 % (1879910)Instructions burned: 159 (million)
% 74.61/16.45 % (1879921)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=2761239637:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2934 on theBenchmark for (2934ds/684Mi)
% 74.61/16.45 % (1879924)ott-21_1_sil=16000:fs=off:random_seed=2181166221:i=180:av=off:fsr=off_2933 on theBenchmark for (2933ds/180Mi)
% 74.61/16.45 % (1879920)Instruction limit reached!
% 74.61/16.45 % (1879920)------------------------------
% 74.61/16.45 % (1879920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 74.61/16.45 % (1879920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.32/19.67 % (1879920)CaDiCaL version: 2.1.3
% 97.32/19.67 % (1879920)Termination reason: Instruction limit
% 97.32/19.67 % (1879920)Termination phase: Preprocessing 1
% 97.32/19.67 % (1879920)Time elapsed: 0.176 s
% 97.32/19.67 % (1879920)Peak memory usage: 43 MB
% 97.32/19.67 % (1879920)Instructions burned: 131 (million)
% 97.32/19.67 % (1879928)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1488002376:i=477:bd=all_2932 on theBenchmark for (2932ds/477Mi)
% 97.32/19.67 % (1879924)Instruction limit reached!
% 97.32/19.67 % (1879924)------------------------------
% 97.32/19.67 % (1879924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.32/19.67 % (1879924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.32/19.67 % (1879924)CaDiCaL version: 2.1.3
% 97.32/19.67 % (1879924)Termination reason: Instruction limit
% 97.32/19.67 % (1879924)Termination phase: Preprocessing 2
% 97.32/19.67 % (1879924)Time elapsed: 0.289 s
% 97.32/19.67 % (1879924)Peak memory usage: 43 MB
% 97.32/19.67 % (1879924)Instructions burned: 180 (million)
% 97.32/19.67 % (1879931)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1804884045:fmbsr=1.3:i=865:ins=25_2930 on theBenchmark for (2930ds/865Mi)
% 97.32/19.67 % (1879918)Instruction limit reached!
% 97.32/19.67 % (1879918)------------------------------
% 97.32/19.67 % (1879918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.32/19.67 % (1879918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.32/19.67 % (1879918)CaDiCaL version: 2.1.3
% 97.32/19.67 % (1879918)Termination reason: Instruction limit
% 97.32/19.67 % (1879918)Termination phase: Preprocessing 3
% 97.32/19.67 % (1879918)Time elapsed: 0.644 s
% 97.32/19.67 % (1879918)Peak memory usage: 72 MB
% 97.32/19.67 % (1879918)Instructions burned: 714 (million)
% 97.32/19.67 % (1879933)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=919726951:i=1179_2928 on theBenchmark for (2928ds/1179Mi)
% 97.32/19.67 % (1879921)Instruction limit reached!
% 97.32/19.67 % (1879921)------------------------------
% 97.32/19.67 % (1879921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.32/19.67 % (1879921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.32/19.67 % (1879921)CaDiCaL version: 2.1.3
% 97.32/19.67 % (1879921)Termination reason: Instruction limit
% 97.32/19.67 % (1879921)Termination phase: NewCNF
% 97.32/19.67 % (1879921)Time elapsed: 0.874 s
% 97.32/19.67 % (1879921)Peak memory usage: 58 MB
% 97.32/19.67 % (1879921)Instructions burned: 684 (million)
% 97.32/19.67 % (1879928)Instruction limit reached!
% 97.32/19.67 % (1879928)------------------------------
% 97.32/19.67 % (1879928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.32/19.67 % (1879928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.32/19.67 % (1879928)CaDiCaL version: 2.1.3
% 97.32/19.67 % (1879928)Termination reason: Instruction limit
% 97.32/19.67 % (1879928)Termination phase: Preprocessing 3
% 97.32/19.67 % (1879928)Time elapsed: 0.726 s
% 97.32/19.67 % (1879928)Peak memory usage: 62 MB
% 97.32/19.67 % (1879928)Instructions burned: 477 (million)
% 97.32/19.67 % (1879935)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=825075588:i=889:ins=1_2924 on theBenchmark for (2924ds/889Mi)
% 97.32/19.67 % (1879936)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=558441158:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2924 on theBenchmark for (2924ds/692Mi)
% 97.32/19.67 % (1879933)Instruction limit reached!
% 97.32/19.67 % (1879933)------------------------------
% 97.32/19.67 % (1879933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.32/19.67 % (1879933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.32/19.67 % (1879933)CaDiCaL version: 2.1.3
% 97.32/19.67 % (1879933)Termination reason: Instruction limit
% 97.32/19.67 % (1879933)Termination phase: Property scanning
% 97.32/19.67 % (1879933)Time elapsed: 1.013 s
% 97.32/19.67 % (1879933)Peak memory usage: 114 MB
% 97.32/19.67 % (1879933)Instructions burned: 1180 (million)
% 97.32/19.67 % (1879931)Instruction limit reached!
% 97.32/19.67 % (1879931)------------------------------
% 97.32/19.67 % (1879931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.32/19.67 % (1879931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.32/19.67 % (1879931)CaDiCaL version: 2.1.3
% 97.32/19.67 % (1879931)Termination reason: Instruction limit
% 97.32/19.67 % (1879931)Termination phase: Preprocessing 3
% 144.14/26.23 % (1879931)Time elapsed: 1.191 s
% 144.14/26.23 % (1879931)Peak memory usage: 90 MB
% 144.14/26.23 % (1879931)Instructions burned: 865 (million)
% 144.14/26.23 % (1879939)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2755877575:i=879:kws=inv_precedence:fsr=off_2917 on theBenchmark for (2917ds/879Mi)
% 144.14/26.23 % (1879940)fmb+10_1_sil=64000:random_seed=3472307257:i=22061:nm=2:gsp=on_2917 on theBenchmark for (2917ds/22061Mi)
% 144.14/26.23 % (1879936)Instruction limit reached!
% 144.14/26.23 % (1879936)------------------------------
% 144.14/26.23 % (1879936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.14/26.23 % (1879936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.14/26.23 % (1879936)CaDiCaL version: 2.1.3
% 144.14/26.23 % (1879936)Termination reason: Instruction limit
% 144.14/26.23 % (1879936)Termination phase: NewCNF
% 144.14/26.23 % (1879936)Time elapsed: 0.805 s
% 144.14/26.23 % (1879936)Peak memory usage: 60 MB
% 144.14/26.23 % (1879936)Instructions burned: 692 (million)
% 144.14/26.23 % (1879943)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3079900570:i=9515:nm=5_2915 on theBenchmark for (2915ds/9515Mi)
% 144.14/26.23 % (1879935)Instruction limit reached!
% 144.14/26.23 % (1879935)------------------------------
% 144.14/26.23 % (1879935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.14/26.23 % (1879935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.14/26.23 % (1879935)CaDiCaL version: 2.1.3
% 144.14/26.23 % (1879935)Termination reason: Instruction limit
% 144.14/26.23 % (1879935)Termination phase: Preprocessing 3
% 144.14/26.23 % (1879935)Time elapsed: 1.304 s
% 144.14/26.23 % (1879935)Peak memory usage: 90 MB
% 144.14/26.23 % (1879935)Instructions burned: 889 (million)
% 144.14/26.23 % (1879946)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1970356074:fmbsr=1.7:i=920_2911 on theBenchmark for (2911ds/920Mi)
% 144.14/26.23 % (1879939)Instruction limit reached!
% 144.14/26.23 % (1879939)------------------------------
% 144.14/26.23 % (1879939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.14/26.23 % (1879939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.14/26.23 % (1879939)CaDiCaL version: 2.1.3
% 144.14/26.23 % (1879939)Termination reason: Instruction limit
% 144.14/26.23 % (1879939)Termination phase: NewCNF
% 144.14/26.23 % (1879939)Time elapsed: 1.075 s
% 144.14/26.23 % (1879939)Peak memory usage: 90 MB
% 144.14/26.23 % (1879939)Instructions burned: 879 (million)
% 144.14/26.23 % (1879951)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1686503286:i=5131_2906 on theBenchmark for (2906ds/5131Mi)
% 144.14/26.23 % (1879946)Instruction limit reached!
% 144.14/26.23 % (1879946)------------------------------
% 144.14/26.23 % (1879946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.14/26.23 % (1879946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.14/26.23 % (1879946)CaDiCaL version: 2.1.3
% 144.14/26.23 % (1879946)Termination reason: Instruction limit
% 144.14/26.23 % (1879946)Termination phase: Preprocessing 3
% 144.14/26.23 % (1879946)Time elapsed: 1.366 s
% 144.14/26.23 % (1879946)Peak memory usage: 93 MB
% 144.14/26.23 % (1879946)Instructions burned: 920 (million)
% 144.14/26.23 % (1879954)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2643465170:i=1472:ins=7:fdi=8:gsp=on_2896 on theBenchmark for (2896ds/1472Mi)
% 144.14/26.23 % (1879954)Instruction limit reached!
% 144.14/26.23 % (1879954)------------------------------
% 144.14/26.23 % (1879954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.14/26.23 % (1879954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.14/26.23 % (1879954)CaDiCaL version: 2.1.3
% 144.14/26.23 % (1879954)Termination reason: Instruction limit
% 144.14/26.23 % (1879954)Termination phase: Property scanning
% 144.14/26.23 % (1879954)Time elapsed: 1.907 s
% 144.14/26.23 % (1879954)Peak memory usage: 114 MB
% 144.14/26.23 % (1879954)Instructions burned: 1473 (million)
% 144.14/26.23 % (1879959)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2753834838:i=6324_2876 on theBenchmark for (2876ds/6324Mi)
% 144.14/26.23 % TRYING [1]
% 144.14/26.23 % (1879951)Instruction limit reached!
% 144.14/26.23 % (1879951)------------------------------
% 144.14/26.23 % (1879951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.14/26.23 % (1879951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.14/26.23 % (1879951)CaDiCaL version: 2.1.3
% 144.14/26.23 % (1879951)Termination reason: Instruction limit
% 139.58/29.92 % (1879951)Termination phase: Saturation
% 139.58/29.92 % (1879951)Time elapsed: 6.561 s
% 139.58/29.92 % (1879951)Peak memory usage: 137 MB
% 139.58/29.92 % (1879951)Instructions burned: 5132 (million)
% 139.58/29.92 % (1879983)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3785861047:fmbsr=2.30978:i=2174_2840 on theBenchmark for (2840ds/2174Mi)
% 139.58/29.92 % TRYING [2]
% 139.58/29.92 % (1879943)Instruction limit reached!
% 139.58/29.92 % (1879943)------------------------------
% 139.58/29.92 % (1879943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.58/29.92 % (1879943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.58/29.92 % (1879943)CaDiCaL version: 2.1.3
% 139.58/29.92 % (1879943)Termination reason: Instruction limit
% 139.58/29.92 % (1879943)Termination phase: Finite model building preprocessing
% 139.58/29.92 % (1879943)Time elapsed: 8.160 s
% 139.58/29.92 % (1879943)Peak memory usage: 289 MB
% 139.58/29.92 % (1879943)Instructions burned: 9516 (million)
% 139.58/29.92 % (1880118)ott-2_1_sil=16000:newcnf=on:random_seed=2967668643:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2833 on theBenchmark for (2833ds/869Mi)
% 139.58/29.92 % (1879959)Instruction limit reached!
% 139.58/29.92 % (1879959)------------------------------
% 139.58/29.92 % (1879959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.58/29.92 % (1879959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.58/29.92 % (1879959)CaDiCaL version: 2.1.3
% 139.58/29.92 % (1879959)Termination reason: Instruction limit
% 139.58/29.92 % (1879959)Termination phase: Finite model building preprocessing
% 139.58/29.92 % (1879959)Time elapsed: 4.918 s
% 139.58/29.92 % (1879959)Peak memory usage: 208 MB
% 139.58/29.92 % (1879959)Instructions burned: 6324 (million)
% 139.58/29.92 % (1880120)ott+10_1_sil=32000:tgt=ground:random_seed=4135106200:i=5114:av=off_2826 on theBenchmark for (2826ds/5114Mi)
% 139.58/29.92 % (1880118)Instruction limit reached!
% 139.58/29.92 % (1880118)------------------------------
% 139.58/29.92 % (1880118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.58/29.92 % (1880118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.58/29.92 % (1880118)CaDiCaL version: 2.1.3
% 139.58/29.92 % (1880118)Termination reason: Instruction limit
% 139.58/29.92 % (1880118)Termination phase: NewCNF
% 139.58/29.92 % (1880118)Time elapsed: 0.670 s
% 139.58/29.92 % (1880118)Peak memory usage: 90 MB
% 139.58/29.92 % (1880118)Instructions burned: 870 (million)
% 139.58/29.92 % (1880122)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1053389042:i=54282_2826 on theBenchmark for (2826ds/54282Mi)
% 139.58/29.92 % (1879983)Instruction limit reached!
% 139.58/29.92 % (1879983)------------------------------
% 139.58/29.92 % (1879983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.58/29.92 % (1879983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.58/29.92 % (1879983)CaDiCaL version: 2.1.3
% 139.58/29.92 % (1879983)Termination reason: Instruction limit
% 139.58/29.92 % (1879983)Termination phase: Finite model building preprocessing
% 139.58/29.92 % (1879983)Time elapsed: 1.421 s
% 139.58/29.92 % (1879983)Peak memory usage: 115 MB
% 139.58/29.92 % (1879983)Instructions burned: 2175 (million)
% 139.58/29.92 % (1880124)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=351647934:i=3512:aac=none_2825 on theBenchmark for (2825ds/3512Mi)
% 139.58/29.92 % (1879940)Instruction limit reached!
% 139.58/29.92 % (1879940)------------------------------
% 139.58/29.92 % (1879940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.58/29.92 % (1879940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.58/29.92 % (1879940)CaDiCaL version: 2.1.3
% 139.58/29.92 % (1879940)Termination reason: Instruction limit
% 139.58/29.92 % (1879940)Termination phase: Finite model building constraint generation
% 139.58/29.92 % (1879940)Time elapsed: 9.250 s
% 139.58/29.92 % (1879940)Peak memory usage: 785 MB
% 139.58/29.92 % (1879940)Instructions burned: 22064 (million)
% 139.58/29.92 % TRYING [1]
% 139.58/29.92 % (1880126)dis+21_1_sil=32000:sas=cadical:random_seed=3343959789:i=3773:amm=off_2824 on theBenchmark for (2824ds/3773Mi)
% 139.58/29.92 % TRYING [2]
% 139.58/29.92 % (1880126)Instruction limit reached!
% 139.58/29.92 % (1880126)------------------------------
% 139.58/29.92 % (1880126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.58/29.92 % (1880126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.58/29.92 % (1880126)CaDiCaL version: 2.1.3
% 139.58/29.92 % (1880126)Termination reason: Instruction limit
% 139.58/29.92 % (1880126)Termination phase: Saturation
% 139.58/29.92 % (1880126)Time elapsed: 1.591 s
% 139.58/29.92 % (1880126)Peak memory usage: 143 MB
% 139.58/29.92 % (1880126)Instructions burned: 3773 (million)
% 139.58/29.92 % (1880128)ott+11_1_sil=16000:gs=on:random_seed=1101262864:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2808 on theBenchmark for (2808ds/2251Mi)
% 139.58/29.92 % (1880124)Instruction limit reached!
% 139.58/29.92 % (1880124)------------------------------
% 139.58/29.92 % (1880124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.58/29.92 % (1880124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.58/29.92 % (1880124)CaDiCaL version: 2.1.3
% 139.58/29.92 % (1880124)Termination reason: Instruction limit
% 139.58/29.92 % (1880124)Termination phase: Saturation
% 139.58/29.92 % (1880124)Time elapsed: 2.427 s
% 139.58/29.92 % (1880124)Peak memory usage: 138 MB
% 139.58/29.92 % (1880124)Instructions burned: 3512 (million)
% 139.58/29.92 % (1880130)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2171664448:fmbsr=1.6:i=67534_2801 on theBenchmark for (2801ds/67534Mi)
% 139.58/29.92 % (1880128)Instruction limit reached!
% 139.58/29.92 % (1880128)------------------------------
% 139.58/29.92 % (1880128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.58/29.92 % (1880128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.58/29.92 % (1880128)CaDiCaL version: 2.1.3
% 139.58/29.92 % (1880128)Termination reason: Instruction limit
% 139.58/29.92 % (1880128)Termination phase: Saturation
% 139.58/29.92 % (1880128)Time elapsed: 0.925 s
% 139.58/29.92 % (1880128)Peak memory usage: 128 MB
% 139.58/29.92 % (1880128)Instructions burned: 2252 (million)
% 139.58/29.92 % (1880132)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=579999114:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2798 on theBenchmark for (2798ds/4591Mi)
% 139.58/29.92 % (1880120)Instruction limit reached!
% 139.58/29.92 % (1880120)------------------------------
% 139.58/29.92 % (1880120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.58/29.92 % (1880120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.58/29.92 % (1880120)CaDiCaL version: 2.1.3
% 139.58/29.92 % (1880120)Termination reason: Instruction limit
% 139.58/29.92 % (1880120)Termination phase: Saturation
% 139.58/29.92 % (1880120)Time elapsed: 3.668 s
% 139.58/29.92 % (1880120)Peak memory usage: 169 MB
% 139.58/29.92 % (1880120)Instructions burned: 5114 (million)
% 139.58/29.92 % (1880134)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2017533954:i=29340_2789 on theBenchmark for (2789ds/29340Mi)
% 139.58/29.92 % (1880132)Instruction limit reached!
% 139.58/29.92 % (1880132)------------------------------
% 139.58/29.92 % (1880132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.58/29.92 % (1880132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.58/29.92 % (1880132)CaDiCaL version: 2.1.3
% 139.58/29.92 % (1880132)Termination reason: Instruction limit
% 139.58/29.92 % (1880132)Termination phase: Saturation
% 139.58/29.92 % (1880132)Time elapsed: 1.793 s
% 139.58/29.92 % (1880132)Peak memory usage: 164 MB
% 139.58/29.92 % (1880132)Instructions burned: 4591 (million)
% 139.58/29.92 % (1880136)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3890094717:i=5211_2780 on theBenchmark for (2780ds/5211Mi)
% 139.58/29.92 % (1880136)Instruction limit reached!
% 139.58/29.92 % (1880136)------------------------------
% 139.58/29.92 % (1880136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.58/29.92 % (1880136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.58/29.92 % (1880136)CaDiCaL version: 2.1.3
% 139.58/29.92 % (1880136)Termination reason: Instruction limit
% 139.58/29.92 % (1880136)Termination phase: Saturation
% 139.58/29.92 % (1880136)Time elapsed: 1.875 s
% 139.58/29.92 % (1880136)Peak memory usage: 209 MB
% 139.58/29.92 % (1880136)Instructions burned: 5216 (million)
% 139.58/29.92 % (1880138)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3733781170:i=5497:nm=2_2761 on theBenchmark for (2761ds/5497Mi)
% 139.58/29.92 % TRYING [1]
% 139.58/29.92 % TRYING [2]
% 139.58/29.92 % (1880138)Instruction limit reached!
% 139.58/29.92 % (1880138)------------------------------
% 139.58/29.92 % (1880138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.58/29.92 % (1880138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.58/29.92 % (1880138)CaDiCaL version: 2.1.3
% 139.58/29.92 % (1880138)Termination reason: Instruction limit
% 139.58/29.92 % (1880138)Termination phase: Finite model building preprocessing
% 139.58/29.92 % (1880138)Time elapsed: 1.860 s
% 139.58/29.92 % (1880138)Peak memory usage: 192 MB
% 139.58/29.92 % (1880138)Instructions burned: 5501 (million)
% 139.58/29.92 % (1880140)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2013426649:fmbsr=2:i=46332_2742 on theBenchmark for (2742ds/46332Mi)
% 139.58/29.92 % Finite Model Found!
% 139.58/29.92 % SZS status Satisfiable for theBenchmark
% 139.58/29.92 % (1879904) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1879882-1879904"...
% 139.58/29.92 % (1879904)...printing done.
% 139.58/29.92 % SZS output start FiniteModel for theBenchmark
% See solution above
% 139.58/29.92 % (1879904)------------------------------
% 139.58/29.92 % (1879904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 139.58/29.92 % (1879904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.58/29.92 % (1879904)CaDiCaL version: 2.1.3
% 139.58/29.92 % (1879904)Termination reason: Satisfiable
% 139.58/29.92 % (1879904)Time elapsed: 22.652 s
% 139.58/29.92 % (1879904)Peak memory usage: 1549 MB
% 139.58/29.92 % (1879904)Instructions burned: 38314 (million)
% 139.58/29.92 % (1879882)Success in time 29.414 s
% 139.58/29.92 % Vampire exiting
%------------------------------------------------------------------------------