%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT257-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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:48:05 AM UTC 2026
% Result : Unsatisfiable 59.40s 9.03s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 15
% Syntax : Number of formulae : 71 ( 67 unt; 3 def)
% Number of atoms : 77 ( 76 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 16 ( 10 ~; 6 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 53 ( 53 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/LAT001-0.ax',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/LAT001-0.ax',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox/benchmark/Axioms/LAT001-0.ax',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/Axioms/LAT001-0.ax',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/LAT001-0.ax',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/LAT001-0.ax',associativity_of_join) ).
fof(f9,axiom,
! [X0] : join(X0,complement(X0)) = one,
file('/export/starexec/sandbox/benchmark/Axioms/LAT001-4.ax',complement_join) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = zero,
file('/export/starexec/sandbox/benchmark/Axioms/LAT001-4.ax',complement_meet) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != one
| meet(X0,X1) != zero
| complement(X0) = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/LAT001-4.ax',meet_join_complement) ).
fof(f12,axiom,
! [X2,X0,X1] : meet(X0,join(meet(X1,join(X0,X2)),meet(X2,join(X0,X1)))) = join(meet(X0,X1),meet(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equation_H82) ).
fof(f13,axiom,
meet(b,a) = a,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_distributivity_hypothesis) ).
fof(f14,plain,
a = meet(b,a),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
join(complement(b),complement(a)) != complement(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f16,plain,
complement(a) != join(complement(b),complement(a)),
inference(reorient_equations,[],[f15]) ).
fof(f17,definition,
sF0 = complement(a),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f18,plain,
complement(a) = sF0,
inference(reorient_equations,[],[f17]) ).
fof(f19,definition,
sF1 = complement(b),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f20,plain,
complement(b) = sF1,
inference(reorient_equations,[],[f19]) ).
fof(f21,definition,
sF2 = join(sF1,sF0),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f22,plain,
join(sF1,sF0) = sF2,
inference(reorient_equations,[],[f21]) ).
fof(f23,plain,
sF0 != sF2,
inference(definition_folding,[],[f16,f22,f18,f20,f18]) ).
fof(f24,plain,
sF2 = join(sF0,sF1),
inference(forward_demodulation,[],[f22,f6]) ).
fof(f25,plain,
one = join(a,sF0),
inference(superposition,[],[f9,f18]) ).
fof(f26,plain,
one = join(b,sF1),
inference(superposition,[],[f9,f20]) ).
fof(f27,plain,
zero = meet(a,sF0),
inference(superposition,[],[f10,f18]) ).
fof(f28,plain,
zero = meet(b,sF1),
inference(superposition,[],[f10,f20]) ).
fof(f30,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f33,plain,
sF0 = meet(sF0,sF2),
inference(superposition,[],[f3,f24]) ).
fof(f35,plain,
b = join(b,a),
inference(superposition,[],[f4,f14]) ).
fof(f37,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f41,plain,
b = join(a,b),
inference(forward_demodulation,[],[f35,f6]) ).
fof(f42,plain,
a = meet(a,b),
inference(superposition,[],[f3,f41]) ).
fof(f48,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f51,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f55,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f30]) ).
fof(f66,plain,
! [X0] : meet(zero,X0) = meet(a,meet(sF0,X0)),
inference(superposition,[],[f7,f27]) ).
fof(f88,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f102,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f113,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f37]) ).
fof(f132,plain,
! [X0] : meet(a,X0) = meet(a,meet(b,X0)),
inference(superposition,[],[f7,f42]) ).
fof(f136,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X1,X0)) = meet(X1,join(meet(X2,join(X0,X1)),meet(X0,join(X1,X2)))),
inference(superposition,[],[f12,f6]) ).
fof(f276,plain,
sF2 = join(sF2,sF0),
inference(superposition,[],[f48,f33]) ).
fof(f286,plain,
sF2 = join(sF0,sF2),
inference(forward_demodulation,[],[f276,f6]) ).
fof(f309,plain,
! [X0] : zero = meet(zero,X0),
inference(superposition,[],[f51,f37]) ).
fof(f358,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f51,f55]) ).
fof(f1668,plain,
! [X0,X1] : join(X0,one) = join(X0,complement(meet(X0,X1))),
inference(superposition,[],[f88,f9]) ).
fof(f1706,plain,
! [X0,X1] : one = join(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f1668,f358]) ).
fof(f2007,plain,
! [X0] : join(a,join(sF0,X0)) = join(X0,one),
inference(superposition,[],[f102,f25]) ).
fof(f2106,plain,
! [X0] : one = join(a,join(sF0,X0)),
inference(forward_demodulation,[],[f2007,f358]) ).
fof(f4209,plain,
! [X0] : join(meet(b,sF1),meet(b,X0)) = meet(b,join(meet(sF1,join(X0,b)),meet(X0,one))),
inference(superposition,[],[f136,f26]) ).
fof(f4321,plain,
! [X0] : join(meet(b,sF1),meet(b,X0)) = meet(b,join(meet(X0,one),meet(sF1,join(X0,b)))),
inference(forward_demodulation,[],[f4209,f6]) ).
fof(f4416,plain,
! [X0] : join(meet(b,sF1),meet(b,X0)) = meet(b,join(X0,meet(sF1,join(X0,b)))),
inference(forward_demodulation,[],[f4321,f30]) ).
fof(f4493,plain,
! [X0] : join(zero,meet(b,X0)) = meet(b,join(X0,meet(sF1,join(X0,b)))),
inference(forward_demodulation,[],[f4416,f28]) ).
fof(f4555,plain,
! [X0] : meet(b,X0) = meet(b,join(X0,meet(sF1,join(X0,b)))),
inference(forward_demodulation,[],[f4493,f113]) ).
fof(f6214,plain,
one = join(a,sF2),
inference(superposition,[],[f2106,f286]) ).
fof(f7063,plain,
( one != one
| zero != meet(a,sF2)
| complement(a) = sF2 ),
inference(superposition,[],[f11,f6214]) ).
fof(f7089,plain,
( zero != meet(a,sF2)
| complement(a) = sF2 ),
inference(trivial_inequality_removal,[],[f7063]) ).
fof(f7108,plain,
( sF0 = sF2
| zero != meet(a,sF2) ),
inference(forward_demodulation,[],[f7089,f18]) ).
fof(f7121,plain,
zero != meet(a,sF2),
inference(forward_subsumption_resolution,[],[f7108,f23]) ).
fof(f20521,plain,
one = join(b,complement(a)),
inference(superposition,[],[f1706,f14]) ).
fof(f20658,plain,
one = join(b,sF0),
inference(forward_demodulation,[],[f20521,f18]) ).
fof(f20694,plain,
one = join(sF0,b),
inference(forward_demodulation,[],[f20658,f6]) ).
fof(f129344,plain,
meet(b,sF0) = meet(b,join(sF0,meet(sF1,one))),
inference(superposition,[],[f4555,f20694]) ).
fof(f129532,plain,
meet(b,sF0) = meet(b,join(sF0,meet(one,sF1))),
inference(forward_demodulation,[],[f129344,f5]) ).
fof(f129596,plain,
meet(b,sF0) = meet(b,join(sF0,sF1)),
inference(forward_demodulation,[],[f129532,f55]) ).
fof(f129637,plain,
meet(b,sF2) = meet(b,sF0),
inference(forward_demodulation,[],[f129596,f24]) ).
fof(f129662,plain,
meet(sF0,b) = meet(b,sF2),
inference(forward_demodulation,[],[f129637,f5]) ).
fof(f129713,plain,
meet(a,meet(sF0,b)) = meet(a,sF2),
inference(superposition,[],[f132,f129662]) ).
fof(f129826,plain,
meet(zero,b) = meet(a,sF2),
inference(forward_demodulation,[],[f129713,f66]) ).
fof(f129854,plain,
zero = meet(a,sF2),
inference(forward_demodulation,[],[f129826,f309]) ).
fof(f129869,plain,
$false,
inference(forward_subsumption_resolution,[],[f129854,f7121]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT257-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 14:14:46 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.40 Running first-order model finding
% 0.10/0.40 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
% 20.69/3.52 % (3606612)Will run a generic schedule for satisfiability detection.
% 20.69/3.52 % (3606623)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=627036965:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 20.69/3.52 % (3606618)% WARNING: option uhcvi not known.
% 20.69/3.52 % (3606619)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2180851944:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 20.69/3.52 % (3606617)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1550723444_2999 on theBenchmark for (2999ds/0Mi)
% 20.69/3.52 % (3606618)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=445271089:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 20.69/3.52 % (3606620)dis+10_1_sil=32000:sp=arity:random_seed=745700625:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 20.69/3.52 % (3606621)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3811811099:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 20.69/3.52 % TRYING [1]
% 20.69/3.52 % TRYING [2]
% 20.69/3.52 % TRYING [3]
% 20.69/3.52 % (3606622)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=138058512:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 20.69/3.52 % TRYING [4]
% 20.69/3.52 % TRYING [5]
% 20.69/3.52 % (3606623)Instruction limit reached!
% 20.69/3.52 % (3606623)------------------------------
% 20.69/3.52 % (3606623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.69/3.52 % (3606623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.69/3.52 % (3606623)CaDiCaL version: 2.1.3
% 20.69/3.52 % (3606623)Termination reason: Instruction limit
% 20.69/3.52 % (3606623)Termination phase: Saturation
% 20.69/3.52 % (3606623)Time elapsed: 0.050 s
% 20.69/3.52 % (3606623)Peak memory usage: 12 MB
% 20.69/3.52 % (3606623)Instructions burned: 160 (million)
% 20.69/3.52 % (3606631)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1646016609:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 20.69/3.52 % TRYING [1]
% 20.69/3.52 % TRYING [2]
% 20.69/3.52 % TRYING [3]
% 20.69/3.52 % (3606620)Instruction limit reached!
% 20.69/3.52 % (3606620)------------------------------
% 20.69/3.52 % (3606620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.69/3.52 % (3606620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.69/3.52 % (3606620)CaDiCaL version: 2.1.3
% 20.69/3.52 % (3606620)Termination reason: Instruction limit
% 20.69/3.52 % (3606620)Termination phase: Saturation
% 20.69/3.52 % (3606620)Time elapsed: 0.057 s
% 20.69/3.52 % (3606620)Peak memory usage: 12 MB
% 20.69/3.52 % (3606620)Instructions burned: 104 (million)
% 20.69/3.52 % TRYING [4]
% 20.69/3.52 % (3606621)Instruction limit reached!
% 20.69/3.52 % (3606621)------------------------------
% 20.69/3.52 % (3606621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.69/3.52 % (3606621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.69/3.52 % (3606621)CaDiCaL version: 2.1.3
% 20.69/3.52 % (3606621)Termination reason: Instruction limit
% 20.69/3.52 % (3606621)Termination phase: Saturation
% 20.69/3.52 % (3606621)Time elapsed: 0.067 s
% 20.69/3.52 % (3606621)Peak memory usage: 12 MB
% 20.69/3.52 % (3606621)Instructions burned: 117 (million)
% 20.69/3.52 % TRYING [5]
% 20.69/3.52 % (3606633)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2068357740:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 20.69/3.52 % (3606634)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=599987936:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 20.69/3.52 % TRYING [6]
% 20.69/3.52 % TRYING [6]
% 20.69/3.52 % (3606622)Instruction limit reached!
% 20.69/3.52 % (3606622)------------------------------
% 20.69/3.52 % (3606622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.69/3.52 % (3606622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.69/3.52 % (3606622)CaDiCaL version: 2.1.3
% 20.69/3.52 % (3606622)Termination reason: Instruction limit
% 20.69/3.52 % (3606622)Termination phase: Saturation
% 20.69/3.52 % (3606622)Time elapsed: 0.140 s
% 20.69/3.52 % (3606622)Peak memory usage: 12 MB
% 20.69/3.52 % (3606622)Instructions burned: 131 (million)
% 20.69/3.52 % (3606633)Instruction limit reached!
% 20.69/3.52 % (3606633)------------------------------
% 20.69/3.52 % (3606633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.69/3.52 % (3606633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.33/6.79 % (3606633)CaDiCaL version: 2.1.3
% 43.33/6.79 % (3606633)Termination reason: Instruction limit
% 43.33/6.79 % (3606633)Termination phase: Saturation
% 43.33/6.79 % (3606633)Time elapsed: 0.082 s
% 43.33/6.79 % (3606633)Peak memory usage: 13 MB
% 43.33/6.79 % (3606633)Instructions burned: 132 (million)
% 43.33/6.79 % (3606637)ott-21_1_sil=16000:fs=off:random_seed=3353256710:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 43.33/6.79 % (3606638)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1304127369:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 43.33/6.79 % (3606631)Instruction limit reached!
% 43.33/6.79 % (3606631)------------------------------
% 43.33/6.79 % (3606631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.33/6.79 % (3606631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.33/6.79 % (3606631)CaDiCaL version: 2.1.3
% 43.33/6.79 % (3606631)Termination reason: Instruction limit
% 43.33/6.79 % (3606631)Termination phase: Finite model building SAT solving
% 43.33/6.79 % (3606631)Time elapsed: 0.154 s
% 43.33/6.79 % (3606631)Peak memory usage: 36 MB
% 43.33/6.79 % (3606631)Instructions burned: 716 (million)
% 43.33/6.79 % (3606641)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1028362707:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 43.33/6.79 % TRYING [1]
% 43.33/6.79 % TRYING [2]
% 43.33/6.79 % TRYING [3]
% 43.33/6.79 % TRYING [4]
% 43.33/6.79 % TRYING [5]
% 43.33/6.79 % (3606637)Instruction limit reached!
% 43.33/6.79 % (3606637)------------------------------
% 43.33/6.79 % (3606637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.33/6.79 % (3606637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.33/6.79 % (3606637)CaDiCaL version: 2.1.3
% 43.33/6.79 % (3606637)Termination reason: Instruction limit
% 43.33/6.79 % (3606637)Termination phase: Saturation
% 43.33/6.79 % (3606637)Time elapsed: 0.123 s
% 43.33/6.79 % (3606637)Peak memory usage: 12 MB
% 43.33/6.79 % (3606637)Instructions burned: 180 (million)
% 43.33/6.79 % TRYING [7]
% 43.33/6.79 % (3606651)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3692487901:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 43.33/6.79 % TRYING [6]
% 43.33/6.79 % (3606634)Instruction limit reached!
% 43.33/6.79 % (3606634)------------------------------
% 43.33/6.79 % (3606634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.33/6.79 % (3606634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.33/6.79 % (3606634)CaDiCaL version: 2.1.3
% 43.33/6.79 % (3606634)Termination reason: Instruction limit
% 43.33/6.79 % (3606634)Termination phase: Saturation
% 43.33/6.79 % (3606634)Time elapsed: 0.392 s
% 43.33/6.79 % (3606634)Peak memory usage: 17 MB
% 43.33/6.79 % (3606634)Instructions burned: 684 (million)
% 43.33/6.79 % (3606641)Instruction limit reached!
% 43.33/6.79 % (3606641)------------------------------
% 43.33/6.79 % (3606641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.33/6.79 % (3606641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.33/6.79 % (3606641)CaDiCaL version: 2.1.3
% 43.33/6.79 % (3606641)Termination reason: Instruction limit
% 43.33/6.79 % (3606641)Termination phase: Finite model building constraint generation
% 43.33/6.79 % (3606641)Time elapsed: 0.272 s
% 43.33/6.79 % (3606641)Peak memory usage: 23 MB
% 43.33/6.79 % (3606641)Instructions burned: 873 (million)
% 43.33/6.79 % (3606655)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=333933174:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 43.33/6.79 % (3606658)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=3705657744:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 43.33/6.79 % (3606638)Instruction limit reached!
% 43.33/6.79 % (3606638)------------------------------
% 43.33/6.79 % (3606638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.33/6.79 % (3606638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.33/6.79 % (3606638)CaDiCaL version: 2.1.3
% 43.33/6.79 % (3606638)Termination reason: Instruction limit
% 43.33/6.79 % (3606638)Termination phase: Saturation
% 43.33/6.79 % (3606638)Time elapsed: 0.365 s
% 43.33/6.79 % (3606638)Peak memory usage: 15 MB
% 43.33/6.79 % (3606638)Instructions burned: 477 (million)
% 43.33/6.79 % (3606664)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=29923492:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 43.33/6.79 % TRYING [14]
% 59.40/9.03 % (3606655)Instruction limit reached!
% 59.40/9.03 % (3606655)------------------------------
% 59.40/9.03 % (3606655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.40/9.03 % (3606655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.40/9.03 % (3606655)CaDiCaL version: 2.1.3
% 59.40/9.03 % (3606655)Termination reason: Instruction limit
% 59.40/9.03 % (3606655)Termination phase: Finite model building constraint generation
% 59.40/9.03 % (3606655)Time elapsed: 0.353 s
% 59.40/9.03 % (3606655)Peak memory usage: 85 MB
% 59.40/9.03 % (3606655)Instructions burned: 893 (million)
% 59.40/9.03 % (3606670)fmb+10_1_sil=64000:random_seed=124000860:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 59.40/9.03 % TRYING [1]
% 59.40/9.03 % TRYING [2]
% 59.40/9.03 % TRYING [3]
% 59.40/9.03 % TRYING [4]
% 59.40/9.03 % TRYING [5]
% 59.40/9.03 % TRYING [6]
% 59.40/9.03 % (3606658)Instruction limit reached!
% 59.40/9.03 % (3606658)------------------------------
% 59.40/9.03 % (3606658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.40/9.03 % (3606658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.40/9.03 % (3606658)CaDiCaL version: 2.1.3
% 59.40/9.03 % (3606658)Termination reason: Instruction limit
% 59.40/9.03 % (3606658)Termination phase: Saturation
% 59.40/9.03 % (3606658)Time elapsed: 0.626 s
% 59.40/9.03 % (3606658)Peak memory usage: 17 MB
% 59.40/9.03 % (3606658)Instructions burned: 692 (million)
% 59.40/9.03 % (3606677)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2810769874:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi)
% 59.40/9.03 % TRYING [20]
% 59.40/9.03 % TRYING [8]
% 59.40/9.03 % (3606664)Instruction limit reached!
% 59.40/9.03 % (3606664)------------------------------
% 59.40/9.03 % (3606664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.40/9.03 % (3606664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.40/9.03 % (3606664)CaDiCaL version: 2.1.3
% 59.40/9.03 % (3606664)Termination reason: Instruction limit
% 59.40/9.03 % (3606664)Termination phase: Saturation
% 59.40/9.03 % (3606664)Time elapsed: 0.697 s
% 59.40/9.03 % (3606664)Peak memory usage: 18 MB
% 59.40/9.03 % (3606664)Instructions burned: 879 (million)
% 59.40/9.03 % (3606682)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=612280737:fmbsr=1.7:i=920_2986 on theBenchmark for (2986ds/920Mi)
% 59.40/9.03 % TRYING [8]
% 59.40/9.03 % (3606651)Instruction limit reached!
% 59.40/9.03 % (3606651)------------------------------
% 59.40/9.03 % (3606651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.40/9.03 % (3606651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.40/9.03 % (3606651)CaDiCaL version: 2.1.3
% 59.40/9.03 % (3606651)Termination reason: Instruction limit
% 59.40/9.03 % (3606651)Termination phase: Saturation
% 59.40/9.03 % (3606651)Time elapsed: 1.107 s
% 59.40/9.03 % (3606651)Peak memory usage: 21 MB
% 59.40/9.03 % (3606651)Instructions burned: 1179 (million)
% 59.40/9.03 % (3606687)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=931654695:i=5131_2985 on theBenchmark for (2985ds/5131Mi)
% 59.40/9.03 % TRYING [7]
% 59.40/9.03 % (3606682)Instruction limit reached!
% 59.40/9.03 % (3606682)------------------------------
% 59.40/9.03 % (3606682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.40/9.03 % (3606682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.40/9.03 % (3606682)CaDiCaL version: 2.1.3
% 59.40/9.03 % (3606682)Termination reason: Instruction limit
% 59.40/9.03 % (3606682)Termination phase: Finite model building constraint generation
% 59.40/9.03 % (3606682)Time elapsed: 0.497 s
% 59.40/9.03 % (3606682)Peak memory usage: 66 MB
% 59.40/9.03 % (3606682)Instructions burned: 921 (million)
% 59.40/9.03 % (3606695)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2822603996:i=1472:ins=7:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/1472Mi)
% 59.40/9.03 % TRYING [9]
% 59.40/9.03 % (3606695)Instruction limit reached!
% 59.40/9.03 % (3606695)------------------------------
% 59.40/9.03 % (3606695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.40/9.03 % (3606695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.40/9.03 % (3606695)CaDiCaL version: 2.1.3
% 59.40/9.03 % (3606695)Termination reason: Instruction limit
% 59.40/9.03 % (3606695)Termination phase: Saturation
% 59.40/9.03 % (3606695)Time elapsed: 1.225 s
% 59.40/9.03 % (3606695)Peak memory usage: 28 MB
% 59.40/9.03 % (3606695)Instructions burned: 1473 (million)
% 59.40/9.03 % TRYING [8]
% 59.40/9.03 % (3606706)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=190177231:i=6324_2969 on theBenchmark for (2969ds/6324Mi)
% 59.40/9.03 % TRYING [77]
% 59.40/9.03 % TRYING [9]
% 59.40/9.03 % (3606687)Instruction limit reached!
% 59.40/9.03 % (3606687)------------------------------
% 59.40/9.03 % (3606687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.40/9.03 % (3606687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.40/9.03 % (3606687)CaDiCaL version: 2.1.3
% 59.40/9.03 % (3606687)Termination reason: Instruction limit
% 59.40/9.03 % (3606687)Termination phase: Saturation
% 59.40/9.03 % (3606687)Time elapsed: 3.631 s
% 59.40/9.03 % (3606687)Peak memory usage: 58 MB
% 59.40/9.03 % (3606687)Instructions burned: 5133 (million)
% 59.40/9.03 % (3606861)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1855232666:fmbsr=2.30978:i=2174_2948 on theBenchmark for (2948ds/2174Mi)
% 59.40/9.03 % TRYING [16]
% 59.40/9.03 % (3606706)Instruction limit reached!
% 59.40/9.03 % (3606706)------------------------------
% 59.40/9.03 % (3606706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.40/9.03 % (3606706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.40/9.03 % (3606706)CaDiCaL version: 2.1.3
% 59.40/9.03 % (3606706)Termination reason: Instruction limit
% 59.40/9.03 % (3606706)Termination phase: Finite model building constraint generation
% 59.40/9.03 % (3606706)Time elapsed: 2.328 s
% 59.40/9.03 % (3606706)Peak memory usage: 420 MB
% 59.40/9.03 % (3606706)Instructions burned: 6324 (million)
% 59.40/9.03 % (3606863)ott-2_1_sil=16000:newcnf=on:random_seed=3141760929:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2945 on theBenchmark for (2945ds/869Mi)
% 59.40/9.03 % (3606677)Instruction limit reached!
% 59.40/9.03 % (3606677)------------------------------
% 59.40/9.03 % (3606677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.40/9.03 % (3606677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.40/9.03 % (3606677)CaDiCaL version: 2.1.3
% 59.40/9.03 % (3606677)Termination reason: Instruction limit
% 59.40/9.03 % (3606677)Termination phase: Finite model building constraint generation
% 59.40/9.03 % (3606677)Time elapsed: 4.396 s
% 59.40/9.03 % (3606677)Peak memory usage: 671 MB
% 59.40/9.03 % (3606677)Instructions burned: 9518 (million)
% 59.40/9.03 % (3606865)ott+10_1_sil=32000:tgt=ground:random_seed=3138065104:i=5114:av=off_2942 on theBenchmark for (2942ds/5114Mi)
% 59.40/9.03 % (3606861)Instruction limit reached!
% 59.40/9.03 % (3606861)------------------------------
% 59.40/9.03 % (3606861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.40/9.03 % (3606861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.40/9.03 % (3606861)CaDiCaL version: 2.1.3
% 59.40/9.03 % (3606861)Termination reason: Instruction limit
% 59.40/9.03 % (3606861)Termination phase: Finite model building constraint generation
% 59.40/9.03 % (3606861)Time elapsed: 0.733 s
% 59.40/9.03 % (3606861)Peak memory usage: 132 MB
% 59.40/9.03 % (3606861)Instructions burned: 2176 (million)
% 59.40/9.03 % (3606867)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2774576098:i=54282_2940 on theBenchmark for (2940ds/54282Mi)
% 59.40/9.03 % TRYING [1]
% 59.40/9.03 % TRYING [2]
% 59.40/9.03 % TRYING [3]
% 59.40/9.03 % TRYING [4]
% 59.40/9.03 % TRYING [5]
% 59.40/9.03 % (3606863)Instruction limit reached!
% 59.40/9.03 % (3606863)------------------------------
% 59.40/9.03 % (3606863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.40/9.03 % (3606863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.40/9.03 % (3606863)CaDiCaL version: 2.1.3
% 59.40/9.03 % (3606863)Termination reason: Instruction limit
% 59.40/9.03 % (3606863)Termination phase: Saturation
% 59.40/9.03 % (3606863)Time elapsed: 0.479 s
% 59.40/9.03 % (3606863)Peak memory usage: 17 MB
% 59.40/9.03 % (3606863)Instructions burned: 869 (million)
% 59.40/9.03 % TRYING [6]
% 59.40/9.03 % (3606869)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1794504769:i=3512:aac=none_2940 on theBenchmark for (2940ds/3512Mi)
% 59.40/9.03 % TRYING [7]
% 59.40/9.03 % (3606670)Instruction limit reached!
% 59.40/9.03 % (3606670)------------------------------
% 59.40/9.03 % (3606670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.40/9.03 % (3606670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.40/9.03 % (3606670)CaDiCaL version: 2.1.3
% 59.40/9.03 % (3606670)Termination reason: Instruction limit
% 59.40/9.03 % (3606670)Termination phase: Finite model building SAT solving
% 59.40/9.03 % (3606670)Time elapsed: 5.477 s
% 59.40/9.03 % (3606670)Peak memory usage: 202 MB
% 59.40/9.03 % (3606670)Instructions burned: 22062 (million)
% 59.40/9.03 % (3606871)dis+21_1_sil=32000:sas=cadical:random_seed=54913411:i=3773:amm=off_2936 on theBenchmark for (2936ds/3773Mi)
% 59.40/9.03 % TRYING [8]
% 59.40/9.03 % (3606871)Instruction limit reached!
% 59.40/9.03 % (3606871)------------------------------
% 59.40/9.03 % (3606871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.40/9.03 % (3606871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.40/9.03 % (3606871)CaDiCaL version: 2.1.3
% 59.40/9.03 % (3606871)Termination reason: Instruction limit
% 59.40/9.03 % (3606871)Termination phase: Saturation
% 59.40/9.03 % (3606871)Time elapsed: 1.079 s
% 59.40/9.03 % (3606871)Peak memory usage: 42 MB
% 59.40/9.03 % (3606871)Instructions burned: 3775 (million)
% 59.40/9.03 % (3606873)ott+11_1_sil=16000:gs=on:random_seed=2953484752:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2925 on theBenchmark for (2925ds/2251Mi)
% 59.40/9.03 % TRYING [9]
% 59.40/9.03 % (3606869)Instruction limit reached!
% 59.40/9.03 % (3606869)------------------------------
% 59.40/9.03 % (3606869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.40/9.03 % (3606869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.40/9.03 % (3606869)CaDiCaL version: 2.1.3
% 59.40/9.03 % (3606869)Termination reason: Instruction limit
% 59.40/9.03 % (3606869)Termination phase: Saturation
% 59.40/9.03 % (3606869)Time elapsed: 1.890 s
% 59.40/9.03 % (3606869)Peak memory usage: 42 MB
% 59.40/9.03 % (3606869)Instructions burned: 3512 (million)
% 59.40/9.03 % (3606875)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2857437114:fmbsr=1.6:i=67534_2920 on theBenchmark for (2920ds/67534Mi)
% 59.40/9.03 % TRYING [7]
% 59.40/9.03 % (3606873)Instruction limit reached!
% 59.40/9.03 % (3606873)------------------------------
% 59.40/9.03 % (3606873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.40/9.03 % (3606873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.40/9.03 % (3606873)CaDiCaL version: 2.1.3
% 59.40/9.03 % (3606873)Termination reason: Instruction limit
% 59.40/9.03 % (3606873)Termination phase: Saturation
% 59.40/9.03 % (3606873)Time elapsed: 0.740 s
% 59.40/9.03 % (3606873)Peak memory usage: 30 MB
% 59.40/9.03 % (3606873)Instructions burned: 2251 (million)
% 59.40/9.03 % (3606877)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=759938904:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2917 on theBenchmark for (2917ds/4591Mi)
% 59.40/9.03 % (3606865) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3606612-3606865"...
% 59.40/9.03 % (3606865)...printing done.
% 59.40/9.03 % (3606865)Refutation found. Thanks to Tanya!
% 59.40/9.03 % SZS status Unsatisfiable for theBenchmark
% 59.40/9.03 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/9.03 % (3606865)------------------------------
% 0.17/9.03 % (3606865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/9.03 % (3606865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/9.03 % (3606865)CaDiCaL version: 2.1.3
% 0.17/9.03 % (3606865)Termination reason: Refutation
% 0.17/9.03 % (3606865)Time elapsed: 2.856 s
% 0.17/9.03 % (3606865)Peak memory usage: 50 MB
% 0.17/9.03 % (3606865)Instructions burned: 4691 (million)
% 0.17/9.03 % (3606612)Success in time 8.626 s
% 0.17/9.03 % Vampire exiting
%------------------------------------------------------------------------------