%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : HWV062+1 : TPTP v9.3.1. Bugfixed v5.5.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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 11:15:56 AM UTC 2026
% Result : Satisfiable 62.42s 13.94s
% Output : FiniteModel 62.42s
% 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.02 % Problem : HWV062+1 : TPTP v9.3.1. Bugfixed v5.5.1.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 % Computer : n026.cluster.edu
% 0.11/0.42 % Model : x86_64 x86_64
% 0.11/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.42 % Memory : 8046.5625MB
% 0.11/0.42 % OS : Linux 6.8.0-71-generic
% 0.11/0.42 % CPULimit : 300
% 0.11/0.42 % WCLimit : 300
% 0.11/0.42 % DateTime : Sun Sep 27 11:22:27 UTC 2026
% 0.11/0.42 % CPUTime :
% 0.11/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.16/0.46 Running first-order model finding
% 0.16/0.46 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 37.08/9.19 % (2682573)Will run a generic schedule for satisfiability detection.
% 37.08/9.19 % (2682580)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1163463944:i=88024:add=on:rawr=on_2959 on theBenchmark for (2959ds/88024Mi)
% 37.08/9.19 % (2682579)% WARNING: option uhcvi not known.
% 37.08/9.19 % (2682578)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3489893439_2959 on theBenchmark for (2959ds/0Mi)
% 37.08/9.19 % (2682579)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1497572958:i=135531:add=off:rawr=on_2959 on theBenchmark for (2959ds/135531Mi)
% 37.08/9.19 % (2682581)dis+10_1_sil=32000:sp=arity:random_seed=434341094:i=103:fgj=on_2959 on theBenchmark for (2959ds/103Mi)
% 37.08/9.19 % (2682582)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2754855050:i=116_2959 on theBenchmark for (2959ds/116Mi)
% 37.08/9.19 % (2682584)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4017372820:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2959 on theBenchmark for (2959ds/159Mi)
% 37.08/9.19 % (2682583)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1264905680:i=131_2959 on theBenchmark for (2959ds/131Mi)
% 37.08/9.19 % (2682581)Instruction limit reached!
% 37.08/9.19 % (2682581)------------------------------
% 37.08/9.19 % (2682581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.08/9.19 % (2682581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.08/9.19 % (2682581)CaDiCaL version: 2.1.3
% 37.08/9.19 % (2682581)Termination reason: Instruction limit
% 37.08/9.19 % (2682581)Termination phase: Preprocessing 2
% 37.08/9.19 % (2682581)Time elapsed: 0.093 s
% 37.08/9.19 % (2682581)Peak memory usage: 27 MB
% 37.08/9.19 % (2682581)Instructions burned: 103 (million)
% 37.08/9.19 % (2682582)Instruction limit reached!
% 37.08/9.19 % (2682582)------------------------------
% 37.08/9.19 % (2682582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.08/9.19 % (2682582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.08/9.19 % (2682582)CaDiCaL version: 2.1.3
% 37.08/9.19 % (2682582)Termination reason: Instruction limit
% 37.08/9.19 % (2682582)Termination phase: NewCNF
% 37.08/9.19 % (2682582)Time elapsed: 0.102 s
% 37.08/9.19 % (2682582)Peak memory usage: 28 MB
% 37.08/9.19 % (2682582)Instructions burned: 116 (million)
% 37.08/9.19 % (2682583)Instruction limit reached!
% 37.08/9.19 % (2682583)------------------------------
% 37.08/9.19 % (2682583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.08/9.19 % (2682583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.08/9.19 % (2682583)CaDiCaL version: 2.1.3
% 37.08/9.19 % (2682583)Termination reason: Instruction limit
% 37.08/9.19 % (2682583)Termination phase: Naming
% 37.08/9.19 % (2682583)Time elapsed: 0.105 s
% 37.08/9.19 % (2682583)Peak memory usage: 27 MB
% 37.08/9.19 % (2682583)Instructions burned: 133 (million)
% 37.08/9.19 % (2682592)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2480179932:i=714:nm=2_2958 on theBenchmark for (2958ds/714Mi)
% 37.08/9.19 % (2682584)Instruction limit reached!
% 37.08/9.19 % (2682584)------------------------------
% 37.08/9.19 % (2682584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.08/9.19 % (2682584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.08/9.19 % (2682584)CaDiCaL version: 2.1.3
% 37.08/9.19 % (2682584)Termination reason: Instruction limit
% 37.08/9.19 % (2682584)Termination phase: Preprocessing 3
% 37.08/9.19 % (2682584)Time elapsed: 0.119 s
% 37.08/9.19 % (2682584)Peak memory usage: 30 MB
% 37.08/9.19 % (2682584)Instructions burned: 161 (million)
% 37.08/9.19 % (2682593)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3940762572:i=131:bd=preordered:fsd=on_2958 on theBenchmark for (2958ds/131Mi)
% 37.08/9.19 % (2682594)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=3145483624:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2958 on theBenchmark for (2958ds/684Mi)
% 37.08/9.19 % (2682596)ott-21_1_sil=16000:fs=off:random_seed=3217642379:i=180:av=off:fsr=off_2958 on theBenchmark for (2958ds/180Mi)
% 37.08/9.19 % (2682593)Instruction limit reached!
% 37.08/9.19 % (2682593)------------------------------
% 37.08/9.19 % (2682593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.08/9.19 % (2682593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.08/9.19 % (2682593)CaDiCaL version: 2.1.3
% 68.96/13.76 % (2682593)Termination reason: Instruction limit
% 68.96/13.76 % (2682593)Termination phase: Naming
% 68.96/13.76 % (2682593)Time elapsed: 0.110 s
% 68.96/13.76 % (2682593)Peak memory usage: 27 MB
% 68.96/13.76 % (2682593)Instructions burned: 133 (million)
% 68.96/13.76 % (2682600)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2620750077:i=477:bd=all_2957 on theBenchmark for (2957ds/477Mi)
% 68.96/13.76 % (2682596)Instruction limit reached!
% 68.96/13.76 % (2682596)------------------------------
% 68.96/13.76 % (2682596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.96/13.76 % (2682596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/13.76 % (2682596)CaDiCaL version: 2.1.3
% 68.96/13.76 % (2682596)Termination reason: Instruction limit
% 68.96/13.76 % (2682596)Termination phase: Preprocessing 3
% 68.96/13.76 % (2682596)Time elapsed: 0.126 s
% 68.96/13.76 % (2682596)Peak memory usage: 30 MB
% 68.96/13.76 % (2682596)Instructions burned: 181 (million)
% 68.96/13.76 % (2682602)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=213304734:fmbsr=1.3:i=865:ins=25_2956 on theBenchmark for (2956ds/865Mi)
% 68.96/13.76 % (2682592)Instruction limit reached!
% 68.96/13.76 % (2682592)------------------------------
% 68.96/13.76 % (2682592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.96/13.76 % (2682592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/13.76 % (2682592)CaDiCaL version: 2.1.3
% 68.96/13.76 % (2682592)Termination reason: Instruction limit
% 68.96/13.76 % (2682592)Termination phase: Property scanning
% 68.96/13.76 % (2682592)Time elapsed: 0.508 s
% 68.96/13.76 % (2682592)Peak memory usage: 63 MB
% 68.96/13.76 % (2682592)Instructions burned: 714 (million)
% 68.96/13.76 % (2682600)Instruction limit reached!
% 68.96/13.76 % (2682600)------------------------------
% 68.96/13.76 % (2682600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.96/13.76 % (2682600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/13.76 % (2682600)CaDiCaL version: 2.1.3
% 68.96/13.76 % (2682600)Termination reason: Instruction limit
% 68.96/13.76 % (2682600)Termination phase: Preprocessing 3
% 68.96/13.76 % (2682600)Time elapsed: 0.378 s
% 68.96/13.76 % (2682600)Peak memory usage: 53 MB
% 68.96/13.76 % (2682600)Instructions burned: 477 (million)
% 68.96/13.76 % (2682594)Instruction limit reached!
% 68.96/13.76 % (2682594)------------------------------
% 68.96/13.76 % (2682594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.96/13.76 % (2682594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/13.76 % (2682594)CaDiCaL version: 2.1.3
% 68.96/13.76 % (2682594)Termination reason: Instruction limit
% 68.96/13.76 % (2682594)Termination phase: Property scanning
% 68.96/13.76 % (2682594)Time elapsed: 0.510 s
% 68.96/13.76 % (2682594)Peak memory usage: 60 MB
% 68.96/13.76 % (2682594)Instructions burned: 686 (million)
% 68.96/13.76 % (2682604)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=254624268:i=1179_2953 on theBenchmark for (2953ds/1179Mi)
% 68.96/13.76 % (2682605)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4278859261:i=889:ins=1_2953 on theBenchmark for (2953ds/889Mi)
% 68.96/13.76 % (2682606)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=2602200467:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2953 on theBenchmark for (2953ds/692Mi)
% 68.96/13.76 % (2682602)Instruction limit reached!
% 68.96/13.76 % (2682602)------------------------------
% 68.96/13.76 % (2682602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.96/13.76 % (2682602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/13.76 % (2682602)CaDiCaL version: 2.1.3
% 68.96/13.76 % (2682602)Termination reason: Instruction limit
% 68.96/13.76 % (2682602)Termination phase: Finite model building preprocessing
% 68.96/13.76 % (2682602)Time elapsed: 0.571 s
% 68.96/13.76 % (2682602)Peak memory usage: 63 MB
% 68.96/13.76 % (2682602)Instructions burned: 866 (million)
% 68.96/13.76 % (2682610)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=754589682:i=879:kws=inv_precedence:fsr=off_2950 on theBenchmark for (2950ds/879Mi)
% 68.96/13.76 % (2682606)Instruction limit reached!
% 68.96/13.76 % (2682606)------------------------------
% 68.96/13.76 % (2682606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.96/13.76 % (2682606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.42/13.94 % (2682606)CaDiCaL version: 2.1.3
% 62.42/13.94 % (2682606)Termination reason: Instruction limit
% 62.42/13.94 % (2682606)Termination phase: Property scanning
% 62.42/13.94 % (2682606)Time elapsed: 0.508 s
% 62.42/13.94 % (2682606)Peak memory usage: 59 MB
% 62.42/13.94 % (2682606)Instructions burned: 694 (million)
% 62.42/13.94 % (2682612)fmb+10_1_sil=64000:random_seed=84809064:i=22061:nm=2:gsp=on_2947 on theBenchmark for (2947ds/22061Mi)
% 62.42/13.94 % (2682605)Instruction limit reached!
% 62.42/13.94 % (2682605)------------------------------
% 62.42/13.94 % (2682605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.42/13.94 % (2682605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.42/13.94 % (2682605)CaDiCaL version: 2.1.3
% 62.42/13.94 % (2682605)Termination reason: Instruction limit
% 62.42/13.94 % (2682605)Termination phase: Property scanning
% 62.42/13.94 % (2682605)Time elapsed: 0.579 s
% 62.42/13.94 % (2682605)Peak memory usage: 63 MB
% 62.42/13.94 % (2682605)Instructions burned: 889 (million)
% 62.42/13.94 % (2682614)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=821319038:i=9515:nm=5_2947 on theBenchmark for (2947ds/9515Mi)
% 62.42/13.94 % (2682604)Instruction limit reached!
% 62.42/13.94 % (2682604)------------------------------
% 62.42/13.94 % (2682604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.42/13.94 % (2682604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.42/13.94 % (2682604)CaDiCaL version: 2.1.3
% 62.42/13.94 % (2682604)Termination reason: Instruction limit
% 62.42/13.94 % (2682604)Termination phase: Saturation
% 62.42/13.94 % (2682604)Time elapsed: 0.751 s
% 62.42/13.94 % (2682604)Peak memory usage: 71 MB
% 62.42/13.94 % (2682604)Instructions burned: 1180 (million)
% 62.42/13.94 % (2682616)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3064815524:fmbsr=1.7:i=920_2945 on theBenchmark for (2945ds/920Mi)
% 62.42/13.94 % (2682610)Instruction limit reached!
% 62.42/13.94 % (2682610)------------------------------
% 62.42/13.94 % (2682610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.42/13.94 % (2682610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.42/13.94 % (2682610)CaDiCaL version: 2.1.3
% 62.42/13.94 % (2682610)Termination reason: Instruction limit
% 62.42/13.94 % (2682610)Termination phase: Property scanning
% 62.42/13.94 % (2682610)Time elapsed: 0.572 s
% 62.42/13.94 % (2682610)Peak memory usage: 59 MB
% 62.42/13.94 % (2682610)Instructions burned: 880 (million)
% 62.42/13.94 % (2682618)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1841748111:i=5131_2944 on theBenchmark for (2944ds/5131Mi)
% 62.42/13.94 % (2682616)Instruction limit reached!
% 62.42/13.94 % (2682616)------------------------------
% 62.42/13.94 % (2682616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.42/13.94 % (2682616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.42/13.94 % (2682616)CaDiCaL version: 2.1.3
% 62.42/13.94 % (2682616)Termination reason: Instruction limit
% 62.42/13.94 % (2682616)Termination phase: Finite model building preprocessing
% 62.42/13.94 % (2682616)Time elapsed: 0.581 s
% 62.42/13.94 % (2682616)Peak memory usage: 64 MB
% 62.42/13.94 % (2682616)Instructions burned: 921 (million)
% 62.42/13.94 % (2682620)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2113786230:i=1472:ins=7:fdi=8:gsp=on_2939 on theBenchmark for (2939ds/1472Mi)
% 62.42/13.94 % (2682620)Instruction limit reached!
% 62.42/13.94 % (2682620)------------------------------
% 62.42/13.94 % (2682620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.42/13.94 % (2682620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.42/13.94 % (2682620)CaDiCaL version: 2.1.3
% 62.42/13.94 % (2682620)Termination reason: Instruction limit
% 62.42/13.94 % (2682620)Termination phase: Saturation
% 62.42/13.94 % (2682620)Time elapsed: 0.867 s
% 62.42/13.94 % (2682620)Peak memory usage: 73 MB
% 62.42/13.94 % (2682620)Instructions burned: 1473 (million)
% 62.42/13.94 % (2682622)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2937501307:i=6324_2930 on theBenchmark for (2930ds/6324Mi)
% 62.42/13.94 % TRYING [1]
% 62.42/13.94 % TRYING [2]
% 62.42/13.94 % (2682614)Cannot represent all propositional literals internally
% 62.42/13.94 % (2682614)Refutation not found, incomplete strategy
% 62.42/13.94 % (2682614)------------------------------
% 62.42/13.94 % (2682614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.42/13.94 % (2682614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.42/13.94 % (2682614)CaDiCaL version: 2.1.3
% 62.42/13.94 % (2682614)Termination reason: Refutation not found, incomplete strategy
% 62.42/13.94 % (2682614)Time elapsed: 3.402 s
% 62.42/13.94 % (2682614)Peak memory usage: 170 MB
% 62.42/13.94 % (2682614)Instructions burned: 6935 (million)
% 62.42/13.94 % (2682614)------------------------------
% 62.42/13.94 % (2682614)------------------------------
% 62.42/13.94 % (2682624)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1821421507:fmbsr=2.30978:i=2174_2912 on theBenchmark for (2912ds/2174Mi)
% 62.42/13.94 % TRYING [1]
% 62.42/13.94 % (2682618)Instruction limit reached!
% 62.42/13.94 % (2682618)------------------------------
% 62.42/13.94 % (2682618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.42/13.94 % (2682618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.42/13.94 % (2682618)CaDiCaL version: 2.1.3
% 62.42/13.94 % (2682618)Termination reason: Instruction limit
% 62.42/13.94 % (2682618)Termination phase: Saturation
% 62.42/13.94 % (2682618)Time elapsed: 3.564 s
% 62.42/13.94 % (2682618)Peak memory usage: 100 MB
% 62.42/13.94 % (2682618)Instructions burned: 5132 (million)
% 62.42/13.94 % (2682626)ott-2_1_sil=16000:newcnf=on:random_seed=3516733834:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2908 on theBenchmark for (2908ds/869Mi)
% 62.42/13.94 % TRYING [2]
% 62.42/13.94 % (2682626)Instruction limit reached!
% 62.42/13.94 % (2682626)------------------------------
% 62.42/13.94 % (2682626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.42/13.94 % (2682626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.42/13.94 % (2682626)CaDiCaL version: 2.1.3
% 62.42/13.94 % (2682626)Termination reason: Instruction limit
% 62.42/13.94 % (2682626)Termination phase: Property scanning
% 62.42/13.94 % (2682626)Time elapsed: 0.567 s
% 62.42/13.94 % (2682626)Peak memory usage: 59 MB
% 62.42/13.94 % (2682626)Instructions burned: 870 (million)
% 62.42/13.94 % (2682628)ott+10_1_sil=32000:tgt=ground:random_seed=1816480312:i=5114:av=off_2902 on theBenchmark for (2902ds/5114Mi)
% 62.42/13.94 % (2682624)Instruction limit reached!
% 62.42/13.94 % (2682624)------------------------------
% 62.42/13.94 % (2682624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.42/13.94 % (2682624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.42/13.94 % (2682624)CaDiCaL version: 2.1.3
% 62.42/13.94 % (2682624)Termination reason: Instruction limit
% 62.42/13.94 % (2682624)Termination phase: Finite model building preprocessing
% 62.42/13.94 % (2682624)Time elapsed: 1.186 s
% 62.42/13.94 % (2682624)Peak memory usage: 86 MB
% 62.42/13.94 % (2682624)Instructions burned: 2175 (million)
% 62.42/13.94 % (2682630)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3579564278:i=54282_2900 on theBenchmark for (2900ds/54282Mi)
% 62.42/13.94 % (2682622)Instruction limit reached!
% 62.42/13.94 % (2682622)------------------------------
% 62.42/13.94 % (2682622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.42/13.94 % (2682622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.42/13.94 % (2682622)CaDiCaL version: 2.1.3
% 62.42/13.94 % (2682622)Termination reason: Instruction limit
% 62.42/13.94 % (2682622)Termination phase: Finite model building preprocessing
% 62.42/13.94 % (2682622)Time elapsed: 3.204 s
% 62.42/13.94 % (2682622)Peak memory usage: 174 MB
% 62.42/13.94 % (2682622)Instructions burned: 6326 (million)
% 62.42/13.94 % (2682632)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3985568785:i=3512:aac=none_2897 on theBenchmark for (2897ds/3512Mi)
% 62.42/13.94 % Finite Model Found!
% 62.42/13.94 % SZS status Satisfiable for theBenchmark
% 62.42/13.94 % (2682632)Instruction limit reached!
% 62.42/13.94 % (2682632)------------------------------
% 62.42/13.94 % (2682632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.42/13.94 % (2682632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.42/13.94 % (2682632)CaDiCaL version: 2.1.3
% 62.42/13.94 % (2682632)Termination reason: Instruction limit
% 62.42/13.94 % (2682632)Termination phase: Saturation
% 62.42/13.94 % (2682632)Time elapsed: 2.463 s
% 62.42/13.94 % (2682632)Peak memory usage: 98 MB
% 62.42/13.94 % (2682632)Instructions burned: 3513 (million)
% 62.42/13.94 % (2682634)dis+21_1_sil=32000:sas=cadical:random_seed=2370136504:i=3773:amm=off_2872 on theBenchmark for (2872ds/3773Mi)
% 62.42/13.94 % (2682578) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2682573-2682578"...
% 62.42/13.94 % (2682628)Instruction limit reached!
% 62.42/13.94 % (2682628)------------------------------
% 62.42/13.94 % (2682628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.42/13.94 % (2682628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.42/13.94 % (2682628)CaDiCaL version: 2.1.3
% 62.42/13.94 % (2682628)Termination reason: Instruction limit
% 62.42/13.94 % (2682628)Termination phase: Saturation
% 62.42/13.94 % (2682628)Time elapsed: 3.560 s
% 62.42/13.94 % (2682628)Peak memory usage: 113 MB
% 62.42/13.94 % (2682628)Instructions burned: 5116 (million)
% 62.42/13.94 % (2682578)...printing done.
% 62.42/13.94 % (2682636)ott+11_1_sil=16000:gs=on:random_seed=138564759:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2866 on theBenchmark for (2866ds/2251Mi)
% 62.42/13.94 % SZS output start FiniteModel for theBenchmark
% See solution above
% 62.42/13.94 % (2682578)------------------------------
% 62.42/13.94 % (2682578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.42/13.94 % (2682578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.42/13.94 % (2682578)CaDiCaL version: 2.1.3
% 62.42/13.94 % (2682578)Termination reason: Satisfiable
% 62.42/13.94 % (2682578)Time elapsed: 9.237 s
% 62.42/13.94 % (2682578)Peak memory usage: 791 MB
% 62.42/13.94 % (2682578)Instructions burned: 19245 (million)
% 62.42/13.94 % (2682573)Success in time 13.468 s
% 62.42/13.94 % Vampire exiting
%------------------------------------------------------------------------------