%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : REL050+2 : TPTP v9.3.1. Released v4.0.0.
% 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 12:34:41 PM UTC 2026
% Result : Theorem 23.93s 3.90s
% Output : Refutation 24.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 16
% Syntax : Number of formulae : 180 ( 165 unt; 2 def)
% Number of atoms : 195 ( 175 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 30 ( 15 ~; 11 |; 2 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 240 ( 0 sgn 239 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',maddux1_join_commutativity) ).
fof(f2,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',maddux2_join_associativity) ).
fof(f3,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',maddux3_a_kind_of_de_Morgan) ).
fof(f4,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',maddux4_definiton_of_meet) ).
fof(f5,axiom,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',composition_associativity) ).
fof(f6,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',composition_identity) ).
fof(f7,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',composition_distributivity) ).
fof(f8,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_idempotence) ).
fof(f9,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_additivity) ).
fof(f10,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_multiplicativity) ).
fof(f11,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_cancellativity) ).
fof(f12,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',def_top) ).
fof(f13,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',def_zero) ).
fof(f14,conjecture,
! [X0] :
( join(complement(composition(X0,top)),composition(complement(composition(X0,top)),top)) = composition(complement(composition(X0,top)),top)
& join(composition(complement(composition(X0,top)),top),complement(composition(X0,top))) = complement(composition(X0,top)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f15,negated_conjecture,
~ ! [X0] :
( join(complement(composition(X0,top)),composition(complement(composition(X0,top)),top)) = composition(complement(composition(X0,top)),top)
& join(composition(complement(composition(X0,top)),top),complement(composition(X0,top))) = complement(composition(X0,top)) ),
inference(negated_conjecture,[status(cth)],[f14]) ).
fof(f16,plain,
? [X0] :
( composition(complement(composition(X0,top)),top) != join(complement(composition(X0,top)),composition(complement(composition(X0,top)),top))
| complement(composition(X0,top)) != join(composition(complement(composition(X0,top)),top),complement(composition(X0,top))) ),
inference(ennf_transformation,[],[f15]) ).
fof(f17,plain,
( composition(complement(composition(sK0,top)),top) != join(complement(composition(sK0,top)),composition(complement(composition(sK0,top)),top))
| complement(composition(sK0,top)) != join(composition(complement(composition(sK0,top)),top),complement(composition(sK0,top))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f16]) ).
fof(f18,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f19,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[],[f2]) ).
fof(f20,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f21,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = meet(X0,X1),
inference(cnf_transformation,[],[f4]) ).
fof(f22,plain,
! [X2,X0,X1] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f23,plain,
! [X0] : composition(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f24,plain,
! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
fof(f25,plain,
! [X0] : converse(converse(X0)) = X0,
inference(cnf_transformation,[],[f8]) ).
fof(f26,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[],[f9]) ).
fof(f27,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[],[f10]) ).
fof(f28,plain,
! [X0,X1] : complement(X1) = join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)),
inference(cnf_transformation,[],[f11]) ).
fof(f29,plain,
! [X0] : top = join(X0,complement(X0)),
inference(cnf_transformation,[],[f12]) ).
fof(f30,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(cnf_transformation,[],[f13]) ).
fof(f31,plain,
( composition(complement(composition(sK0,top)),top) != join(complement(composition(sK0,top)),composition(complement(composition(sK0,top)),top))
| complement(composition(sK0,top)) != join(composition(complement(composition(sK0,top)),top),complement(composition(sK0,top))) ),
inference(cnf_transformation,[],[f17]) ).
fof(f32,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f30,f21]) ).
fof(f34,definition,
( spl1_1
<=> complement(composition(sK0,top)) = join(composition(complement(composition(sK0,top)),top),complement(composition(sK0,top))) ),
introduced(definition,[new_symbols(definition,[spl1_1])],[avatar_definition]) ).
fof(f36,plain,
( complement(composition(sK0,top)) != join(composition(complement(composition(sK0,top)),top),complement(composition(sK0,top)))
| spl1_1 ),
inference(avatar_component_clause,[],[f34]) ).
fof(f38,definition,
( spl1_2
<=> composition(complement(composition(sK0,top)),top) = join(complement(composition(sK0,top)),composition(complement(composition(sK0,top)),top)) ),
introduced(definition,[new_symbols(definition,[spl1_2])],[avatar_definition]) ).
fof(f40,plain,
( composition(complement(composition(sK0,top)),top) != join(complement(composition(sK0,top)),composition(complement(composition(sK0,top)),top))
| spl1_2 ),
inference(avatar_component_clause,[],[f38]) ).
fof(f41,plain,
( ~ spl1_1
| ~ spl1_2 ),
inference(avatar_split_clause,[],[f31,f38,f34]) ).
fof(f42,plain,
( complement(composition(sK0,top)) != join(complement(composition(sK0,top)),composition(complement(composition(sK0,top)),top))
| spl1_1 ),
inference(superposition,[],[f36,f18]) ).
fof(f44,plain,
zero = complement(top),
inference(forward_demodulation,[],[f32,f29]) ).
fof(f46,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[],[f26,f25]) ).
fof(f47,plain,
! [X0,X1] : converse(join(X1,converse(X0))) = join(converse(X1),X0),
inference(superposition,[],[f26,f25]) ).
fof(f52,plain,
! [X0,X1] : converse(composition(X1,converse(X0))) = composition(X0,converse(X1)),
inference(superposition,[],[f27,f25]) ).
fof(f53,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[],[f27,f25]) ).
fof(f57,plain,
! [X0] : join(X0,converse(complement(converse(X0)))) = converse(top),
inference(superposition,[],[f46,f29]) ).
fof(f209,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f53,f23]) ).
fof(f225,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f209,f25]) ).
fof(f230,plain,
one = converse(one),
inference(superposition,[],[f225,f23]) ).
fof(f237,plain,
! [X0] : composition(one,X0) = X0,
inference(superposition,[],[f225,f230]) ).
fof(f441,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f19,f29]) ).
fof(f442,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f19,f18]) ).
fof(f448,plain,
! [X2,X0,X1] : join(converse(X0),join(converse(X1),X2)) = join(converse(join(X0,X1)),X2),
inference(superposition,[],[f19,f26]) ).
fof(f450,plain,
! [X0,X1] : top = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f19,f29]) ).
fof(f451,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X1,join(X2,X0)),
inference(superposition,[],[f19,f18]) ).
fof(f481,plain,
! [X0,X1] : join(top,X0) = join(X1,join(X0,complement(X1))),
inference(superposition,[],[f441,f18]) ).
fof(f503,plain,
! [X0,X1] : top = join(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f450,f18]) ).
fof(f1009,plain,
! [X0,X1] : join(top,X1) = join(complement(X0),join(X0,X1)),
inference(superposition,[],[f442,f29]) ).
fof(f1270,plain,
! [X0] : join(top,X0) = join(top,complement(complement(X0))),
inference(superposition,[],[f1009,f481]) ).
fof(f4621,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(converse(one),X1),X0),
inference(superposition,[],[f24,f225]) ).
fof(f4626,plain,
! [X0,X1] : join(composition(X1,X0),X0) = composition(join(X1,converse(one)),X0),
inference(superposition,[],[f24,f225]) ).
fof(f4653,plain,
! [X0,X1] : composition(join(X1,one),X0) = join(composition(X1,X0),X0),
inference(forward_demodulation,[],[f4626,f230]) ).
fof(f4656,plain,
! [X0,X1] : composition(join(one,X1),X0) = join(X0,composition(X1,X0)),
inference(forward_demodulation,[],[f4621,f230]) ).
fof(f4658,plain,
! [X0,X1] : composition(join(X1,one),X0) = join(X0,composition(X1,X0)),
inference(forward_demodulation,[],[f4653,f18]) ).
fof(f4942,plain,
! [X0,X1] : composition(join(one,X0),X1) = composition(join(X0,one),X1),
inference(superposition,[],[f4658,f4656]) ).
fof(f16161,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(converse(X0),complement(composition(X0,X1)))),
inference(forward_demodulation,[],[f28,f18]) ).
fof(f16894,plain,
! [X0,X1] : complement(converse(X0)) = join(complement(converse(X0)),composition(converse(converse(X1)),complement(converse(composition(X0,X1))))),
inference(superposition,[],[f16161,f27]) ).
fof(f16897,plain,
! [X0] : complement(X0) = join(complement(X0),complement(composition(one,X0))),
inference(superposition,[],[f16161,f225]) ).
fof(f16953,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(forward_demodulation,[],[f16897,f237]) ).
fof(f16956,plain,
! [X0,X1] : complement(converse(X0)) = join(complement(converse(X0)),composition(X1,complement(converse(composition(X0,X1))))),
inference(forward_demodulation,[],[f16894,f25]) ).
fof(f17015,plain,
zero = join(zero,zero),
inference(superposition,[],[f16953,f44]) ).
fof(f17044,plain,
! [X0] : top = join(complement(X0),join(complement(X0),complement(complement(X0)))),
inference(superposition,[],[f503,f16953]) ).
fof(f17065,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[],[f17044,f481]) ).
fof(f17126,plain,
! [X0] : join(zero,X0) = join(zero,join(zero,X0)),
inference(superposition,[],[f19,f17015]) ).
fof(f17226,plain,
! [X0] : top = join(top,X0),
inference(superposition,[],[f17065,f1270]) ).
fof(f17376,plain,
! [X0] : top = composition(join(X0,one),top),
inference(superposition,[],[f17226,f4658]) ).
fof(f17378,plain,
top = converse(top),
inference(superposition,[],[f17226,f57]) ).
fof(f17589,plain,
! [X0] : converse(composition(top,X0)) = composition(converse(X0),top),
inference(superposition,[],[f27,f17378]) ).
fof(f17800,plain,
top = composition(top,top),
inference(superposition,[],[f17376,f17226]) ).
fof(f17830,plain,
! [X0] : composition(top,X0) = composition(top,composition(top,X0)),
inference(superposition,[],[f22,f17800]) ).
fof(f18125,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f20,f18]) ).
fof(f19532,plain,
! [X0] : complement(composition(top,X0)) = join(complement(composition(top,X0)),composition(converse(top),complement(composition(top,X0)))),
inference(superposition,[],[f16161,f17830]) ).
fof(f19543,plain,
! [X0] : complement(composition(top,X0)) = composition(join(one,converse(top)),complement(composition(top,X0))),
inference(forward_demodulation,[],[f19532,f4656]) ).
fof(f19550,plain,
! [X0] : complement(composition(top,X0)) = composition(join(one,top),complement(composition(top,X0))),
inference(forward_demodulation,[],[f19543,f17378]) ).
fof(f19556,plain,
! [X0] : complement(composition(top,X0)) = composition(join(top,one),complement(composition(top,X0))),
inference(forward_demodulation,[],[f19550,f4942]) ).
fof(f19559,plain,
! [X0] : complement(composition(top,X0)) = composition(top,complement(composition(top,X0))),
inference(forward_demodulation,[],[f19556,f17226]) ).
fof(f23859,plain,
! [X0,X1] : join(complement(join(X0,complement(X1))),complement(join(complement(X1),complement(X0)))) = X1,
inference(superposition,[],[f18125,f18]) ).
fof(f23900,plain,
! [X0] : join(complement(join(complement(X0),complement(X0))),complement(top)) = X0,
inference(superposition,[],[f18125,f29]) ).
fof(f23903,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),complement(join(complement(X0),complement(X1)))) = X1,
inference(superposition,[],[f18125,f18]) ).
fof(f23909,plain,
! [X0,X1] : join(join(complement(X0),X1),X0) = join(top,complement(join(complement(X0),complement(X1)))),
inference(superposition,[],[f441,f18125]) ).
fof(f23945,plain,
! [X0,X1] : top = join(join(complement(X0),X1),X0),
inference(forward_demodulation,[],[f23909,f17065]) ).
fof(f23952,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(X0)))) = X0,
inference(forward_demodulation,[],[f23900,f18]) ).
fof(f24015,plain,
! [X0,X1] : top = join(X0,join(complement(X0),X1)),
inference(forward_demodulation,[],[f23945,f18]) ).
fof(f24022,plain,
! [X0] : join(complement(top),complement(complement(X0))) = X0,
inference(forward_demodulation,[],[f23952,f16953]) ).
fof(f24070,plain,
! [X0] : join(zero,complement(complement(X0))) = X0,
inference(forward_demodulation,[],[f24022,f44]) ).
fof(f24150,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f17126,f24070]) ).
fof(f24214,plain,
! [X0] : complement(complement(X0)) = X0,
inference(superposition,[],[f24150,f24070]) ).
fof(f24246,plain,
top = complement(zero),
inference(superposition,[],[f24150,f29]) ).
fof(f24644,plain,
! [X0] : join(X0,X0) = X0,
inference(superposition,[],[f16953,f24214]) ).
fof(f24919,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(superposition,[],[f451,f24644]) ).
fof(f25783,plain,
! [X0,X1] : top = join(X1,join(X0,complement(X1))),
inference(superposition,[],[f24015,f18]) ).
fof(f25961,plain,
! [X0,X1] : converse(top) = join(X0,converse(join(complement(converse(X0)),X1))),
inference(superposition,[],[f46,f24015]) ).
fof(f25962,plain,
! [X0,X1] : join(complement(top),complement(join(complement(X0),complement(join(complement(complement(X0)),X1))))) = X0,
inference(superposition,[],[f18125,f24015]) ).
fof(f25975,plain,
! [X0,X1] : join(complement(top),complement(join(complement(X0),complement(join(X0,X1))))) = X0,
inference(forward_demodulation,[],[f25962,f24214]) ).
fof(f25976,plain,
! [X0,X1] : top = join(X0,converse(join(complement(converse(X0)),X1))),
inference(forward_demodulation,[],[f25961,f17378]) ).
fof(f26072,plain,
! [X0,X1] : join(zero,complement(join(complement(X0),complement(join(X0,X1))))) = X0,
inference(forward_demodulation,[],[f25975,f44]) ).
fof(f26114,plain,
! [X0,X1] : complement(join(complement(X0),complement(join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f26072,f24150]) ).
fof(f26330,plain,
! [X0,X1] : join(complement(top),complement(join(complement(X0),complement(join(X1,complement(complement(X0))))))) = X0,
inference(superposition,[],[f18125,f25783]) ).
fof(f26343,plain,
! [X0,X1] : join(complement(top),complement(join(complement(X0),complement(join(X1,X0))))) = X0,
inference(forward_demodulation,[],[f26330,f24214]) ).
fof(f26441,plain,
! [X0,X1] : join(zero,complement(join(complement(X0),complement(join(X1,X0))))) = X0,
inference(forward_demodulation,[],[f26343,f44]) ).
fof(f26487,plain,
! [X0,X1] : complement(join(complement(X0),complement(join(X1,X0)))) = X0,
inference(forward_demodulation,[],[f26441,f24150]) ).
fof(f33251,plain,
! [X0,X1] : top = join(X0,join(converse(complement(converse(X0))),X1)),
inference(superposition,[],[f25976,f47]) ).
fof(f33864,plain,
! [X0,X1] : join(zero,complement(X0)) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f24070,f26114]) ).
fof(f33876,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f33864,f24150]) ).
fof(f36144,plain,
! [X0,X1] : join(zero,complement(X0)) = join(complement(X0),complement(join(X1,X0))),
inference(superposition,[],[f24070,f26487]) ).
fof(f36165,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f36144,f24150]) ).
fof(f37392,plain,
! [X0,X1] : top = join(X1,composition(join(X0,one),converse(complement(converse(X1))))),
inference(superposition,[],[f33251,f4658]) ).
fof(f38073,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(complement(complement(join(X0,X1))),complement(complement(X0)))),
inference(superposition,[],[f26487,f33876]) ).
fof(f38074,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(complement(complement(X0)),complement(complement(join(X0,X1))))),
inference(forward_demodulation,[],[f38073,f18]) ).
fof(f38224,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(complement(complement(X0)),join(X0,X1))),
inference(forward_demodulation,[],[f38074,f24214]) ).
fof(f38320,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X0,join(X1,complement(complement(X0))))),
inference(forward_demodulation,[],[f38224,f451]) ).
fof(f38375,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X0,join(X1,X0))),
inference(forward_demodulation,[],[f38320,f24214]) ).
fof(f38404,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f38375,f24919]) ).
fof(f99032,plain,
! [X0] : top = join(X0,composition(top,converse(complement(converse(X0))))),
inference(superposition,[],[f37392,f17226]) ).
fof(f99668,plain,
! [X0] : converse(top) = join(X0,converse(composition(top,converse(complement(converse(converse(X0))))))),
inference(superposition,[],[f46,f99032]) ).
fof(f99689,plain,
! [X0] : converse(top) = join(X0,composition(complement(converse(converse(X0))),converse(top))),
inference(forward_demodulation,[],[f99668,f52]) ).
fof(f99814,plain,
! [X0] : top = join(X0,composition(complement(converse(converse(X0))),top)),
inference(forward_demodulation,[],[f99689,f17378]) ).
fof(f99890,plain,
! [X0] : top = join(X0,composition(complement(X0),top)),
inference(forward_demodulation,[],[f99814,f25]) ).
fof(f100099,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(composition(complement(complement(X0)),top))))) = X0,
inference(superposition,[],[f18125,f99890]) ).
fof(f100145,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(composition(X0,top))))) = X0,
inference(forward_demodulation,[],[f100099,f24214]) ).
fof(f100260,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(composition(X0,top))))) = X0,
inference(forward_demodulation,[],[f100145,f44]) ).
fof(f100333,plain,
! [X0] : complement(join(complement(X0),complement(composition(X0,top)))) = X0,
inference(forward_demodulation,[],[f100260,f24150]) ).
fof(f102524,plain,
! [X0] : complement(complement(composition(X0,top))) = join(complement(complement(composition(X0,top))),X0),
inference(superposition,[],[f36165,f100333]) ).
fof(f102685,plain,
! [X0] : complement(complement(composition(X0,top))) = join(X0,complement(complement(composition(X0,top)))),
inference(forward_demodulation,[],[f102524,f18]) ).
fof(f102756,plain,
! [X0] : composition(X0,top) = join(X0,composition(X0,top)),
inference(forward_demodulation,[],[f102685,f24214]) ).
fof(f132175,plain,
! [X0,X1] : join(top,converse(X1)) = join(converse(join(X0,X1)),complement(converse(X0))),
inference(superposition,[],[f481,f448]) ).
fof(f132343,plain,
! [X0,X1] : join(top,converse(X1)) = join(complement(converse(X0)),converse(join(X0,X1))),
inference(forward_demodulation,[],[f132175,f18]) ).
fof(f132605,plain,
! [X0,X1] : top = join(complement(converse(X0)),converse(join(X0,X1))),
inference(forward_demodulation,[],[f132343,f17226]) ).
fof(f134729,plain,
! [X0,X1] : top = join(complement(converse(complement(join(complement(X0),X1)))),converse(X0)),
inference(superposition,[],[f132605,f18125]) ).
fof(f135233,plain,
! [X0,X1] : top = join(converse(X0),complement(converse(complement(join(complement(X0),X1))))),
inference(forward_demodulation,[],[f134729,f18]) ).
fof(f151639,plain,
! [X0,X1] : top = join(converse(X1),complement(converse(complement(join(X0,complement(X1)))))),
inference(superposition,[],[f135233,f18]) ).
fof(f198333,plain,
! [X0] : join(complement(converse(top)),complement(join(complement(converse(complement(converse(complement(X0))))),complement(X0)))) = X0,
inference(superposition,[],[f23903,f57]) ).
fof(f198733,plain,
! [X0] : join(complement(converse(top)),complement(join(complement(X0),complement(converse(complement(converse(complement(X0)))))))) = X0,
inference(forward_demodulation,[],[f198333,f38404]) ).
fof(f199045,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(converse(complement(converse(complement(X0)))))))) = X0,
inference(forward_demodulation,[],[f198733,f17378]) ).
fof(f199267,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(converse(complement(converse(complement(X0)))))))) = X0,
inference(forward_demodulation,[],[f199045,f44]) ).
fof(f199439,plain,
! [X0] : complement(join(complement(X0),complement(converse(complement(converse(complement(X0))))))) = X0,
inference(forward_demodulation,[],[f199267,f24150]) ).
fof(f199619,plain,
! [X0] : top = join(converse(converse(complement(converse(complement(X0))))),complement(converse(X0))),
inference(superposition,[],[f151639,f199439]) ).
fof(f199908,plain,
! [X0] : top = join(complement(converse(X0)),converse(converse(complement(converse(complement(X0)))))),
inference(forward_demodulation,[],[f199619,f18]) ).
fof(f199982,plain,
! [X0] : top = join(complement(converse(X0)),complement(converse(complement(X0)))),
inference(forward_demodulation,[],[f199908,f25]) ).
fof(f200044,plain,
! [X0] : top = join(complement(X0),complement(converse(complement(converse(X0))))),
inference(superposition,[],[f199982,f25]) ).
fof(f200557,plain,
! [X0] : top = join(X0,complement(converse(complement(converse(complement(X0)))))),
inference(superposition,[],[f200044,f24214]) ).
fof(f201140,plain,
! [X0] : converse(complement(converse(complement(X0)))) = join(complement(top),complement(join(complement(converse(complement(converse(complement(X0))))),complement(X0)))),
inference(superposition,[],[f23859,f200557]) ).
fof(f201531,plain,
! [X0] : converse(complement(converse(complement(X0)))) = join(complement(top),complement(join(complement(X0),complement(converse(complement(converse(complement(X0)))))))),
inference(forward_demodulation,[],[f201140,f38404]) ).
fof(f201676,plain,
! [X0] : join(complement(top),X0) = converse(complement(converse(complement(X0)))),
inference(forward_demodulation,[],[f201531,f199439]) ).
fof(f201755,plain,
! [X0] : join(zero,X0) = converse(complement(converse(complement(X0)))),
inference(forward_demodulation,[],[f201676,f44]) ).
fof(f201800,plain,
! [X0] : converse(complement(converse(complement(X0)))) = X0,
inference(forward_demodulation,[],[f201755,f24150]) ).
fof(f201843,plain,
! [X0] : complement(X0) = converse(complement(converse(X0))),
inference(superposition,[],[f201800,f24214]) ).
fof(f201908,plain,
! [X0] : converse(X0) = complement(converse(complement(X0))),
inference(superposition,[],[f25,f201800]) ).
fof(f202204,plain,
! [X0] : complement(converse(X0)) = converse(complement(X0)),
inference(superposition,[],[f201843,f25]) ).
fof(f204593,plain,
! [X0] : complement(converse(top)) = join(complement(converse(top)),composition(complement(composition(top,X0)),complement(converse(complement(composition(top,X0)))))),
inference(superposition,[],[f16956,f19559]) ).
fof(f204789,plain,
! [X0] : complement(converse(top)) = join(complement(converse(top)),composition(complement(composition(top,X0)),converse(composition(top,X0)))),
inference(forward_demodulation,[],[f204593,f201908]) ).
fof(f204920,plain,
! [X0] : complement(converse(top)) = join(complement(converse(top)),composition(complement(composition(top,X0)),composition(converse(X0),top))),
inference(forward_demodulation,[],[f204789,f17589]) ).
fof(f205007,plain,
! [X0] : complement(top) = join(complement(top),composition(complement(composition(top,X0)),composition(converse(X0),top))),
inference(forward_demodulation,[],[f204920,f17378]) ).
fof(f205069,plain,
! [X0] : zero = join(zero,composition(complement(composition(top,X0)),composition(converse(X0),top))),
inference(forward_demodulation,[],[f205007,f44]) ).
fof(f205104,plain,
! [X0] : zero = composition(complement(composition(top,X0)),composition(converse(X0),top)),
inference(forward_demodulation,[],[f205069,f24150]) ).
fof(f206941,plain,
! [X0] : zero = composition(complement(composition(top,converse(X0))),composition(X0,top)),
inference(superposition,[],[f205104,f25]) ).
fof(f207614,plain,
! [X0] : complement(composition(X0,top)) = join(complement(composition(X0,top)),composition(converse(complement(composition(top,converse(X0)))),complement(zero))),
inference(superposition,[],[f16161,f206941]) ).
fof(f207638,plain,
! [X0] : complement(composition(X0,top)) = join(complement(composition(X0,top)),composition(converse(complement(composition(top,converse(X0)))),top)),
inference(forward_demodulation,[],[f207614,f24246]) ).
fof(f207691,plain,
! [X0] : complement(composition(X0,top)) = join(complement(composition(X0,top)),composition(complement(converse(composition(top,converse(X0)))),top)),
inference(forward_demodulation,[],[f207638,f202204]) ).
fof(f207730,plain,
! [X0] : complement(composition(X0,top)) = join(complement(composition(X0,top)),composition(complement(composition(X0,converse(top))),top)),
inference(forward_demodulation,[],[f207691,f52]) ).
fof(f207753,plain,
! [X0] : complement(composition(X0,top)) = join(complement(composition(X0,top)),composition(complement(composition(X0,top)),top)),
inference(forward_demodulation,[],[f207730,f17378]) ).
fof(f207761,plain,
! [X0] : complement(composition(X0,top)) = composition(complement(composition(X0,top)),top),
inference(forward_demodulation,[],[f207753,f102756]) ).
fof(f209562,plain,
( complement(composition(sK0,top)) != join(complement(composition(sK0,top)),complement(composition(sK0,top)))
| spl1_1 ),
inference(superposition,[],[f42,f207761]) ).
fof(f209661,plain,
( $false
| spl1_1 ),
inference(forward_subsumption_resolution,[],[f209562,f16953]) ).
fof(f209662,plain,
spl1_1,
inference(avatar_contradiction_clause,[],[f209661]) ).
fof(f209721,plain,
( $false
| spl1_2 ),
inference(forward_subsumption_resolution,[],[f40,f102756]) ).
fof(f209722,plain,
spl1_2,
inference(avatar_contradiction_clause,[],[f209721]) ).
cnf(s15,plain,
( ~ spl1_1
| ~ spl1_2 ),
inference(sat_conversion,[],[f41]) ).
cnf(s19725,plain,
spl1_1,
inference(sat_conversion,[],[f209662]) ).
cnf(s19732,plain,
spl1_2,
inference(sat_conversion,[],[f209722]) ).
cnf(s19733,plain,
$false,
inference(rat,[],[s15,s19732,s19725]) ).
fof(f209724,plain,
$false,
inference(avatar_sat_refutation,[],[s19733]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL050+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.38 % Computer : n026.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 23:00:12 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 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
% 15.41/2.69 % (3307934)Will run a generic schedule for satisfiability detection.
% 15.41/2.69 % (3307952)% WARNING: option uhcvi not known.
% 15.41/2.69 % (3307952)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2851569968:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.41/2.69 % (3307951)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=520903860_2999 on theBenchmark for (2999ds/0Mi)
% 15.41/2.69 % (3307954)dis+10_1_sil=32000:sp=arity:random_seed=488947112:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.41/2.69 % (3307955)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2816706473:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.41/2.69 % (3307956)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2569999391:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.41/2.69 % (3307953)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1202938612:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.41/2.69 % (3307957)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4095551272:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.41/2.69 % TRYING [1]
% 15.41/2.69 % TRYING [2]
% 15.41/2.69 % TRYING [3]
% 15.41/2.69 % TRYING [4]
% 15.41/2.69 % TRYING [5]
% 15.41/2.69 % (3307954)Instruction limit reached!
% 15.41/2.69 % (3307954)------------------------------
% 15.41/2.69 % (3307954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.41/2.69 % (3307954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.41/2.69 % (3307954)CaDiCaL version: 2.1.3
% 15.41/2.69 % (3307954)Termination reason: Instruction limit
% 15.41/2.69 % (3307954)Termination phase: Saturation
% 15.41/2.69 % (3307954)Time elapsed: 0.060 s
% 15.41/2.69 % (3307954)Peak memory usage: 12 MB
% 15.41/2.69 % (3307954)Instructions burned: 104 (million)
% 15.41/2.69 % (3307955)Instruction limit reached!
% 15.41/2.69 % (3307955)------------------------------
% 15.41/2.69 % (3307955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.41/2.69 % (3307955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.41/2.69 % (3307955)CaDiCaL version: 2.1.3
% 15.41/2.69 % (3307955)Termination reason: Instruction limit
% 15.41/2.69 % (3307955)Termination phase: Saturation
% 15.41/2.69 % (3307955)Time elapsed: 0.070 s
% 15.41/2.69 % (3307955)Peak memory usage: 13 MB
% 15.41/2.69 % (3307955)Instructions burned: 116 (million)
% 15.41/2.69 % (3307956)Instruction limit reached!
% 15.41/2.69 % (3307956)------------------------------
% 15.41/2.69 % (3307956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.41/2.69 % (3307956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.41/2.69 % (3307956)CaDiCaL version: 2.1.3
% 15.41/2.69 % (3307956)Termination reason: Instruction limit
% 15.41/2.69 % (3307956)Termination phase: Saturation
% 15.41/2.69 % (3307956)Time elapsed: 0.076 s
% 15.41/2.69 % (3307956)Peak memory usage: 13 MB
% 15.41/2.69 % (3307956)Instructions burned: 133 (million)
% 15.41/2.69 % (3307993)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3534080887:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 15.41/2.69 % TRYING [1]
% 15.41/2.69 % TRYING [2]
% 15.41/2.69 % TRYING [3]
% 15.41/2.69 % (3307998)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1177024936:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.41/2.69 % (3307957)Instruction limit reached!
% 15.41/2.69 % (3307957)------------------------------
% 15.41/2.69 % (3307957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.41/2.69 % (3307957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.41/2.69 % (3307957)CaDiCaL version: 2.1.3
% 15.41/2.69 % (3307957)Termination reason: Instruction limit
% 15.41/2.69 % (3307957)Termination phase: Saturation
% 15.41/2.69 % (3307957)Time elapsed: 0.095 s
% 15.41/2.69 % (3307957)Peak memory usage: 13 MB
% 15.41/2.69 % (3307957)Instructions burned: 159 (million)
% 15.41/2.69 % TRYING [4]
% 15.41/2.69 % (3308004)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=213940710:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.41/2.69 % (3308008)ott-21_1_sil=16000:fs=off:random_seed=3572169238:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.41/2.69 % TRYING [5]
% 15.41/2.69 % (3307998)Instruction limit reached!
% 15.41/2.69 % (3307998)------------------------------
% 15.41/2.69 % (3307998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.90 % (3307998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.90 % (3307998)CaDiCaL version: 2.1.3
% 23.93/3.90 % (3307998)Termination reason: Instruction limit
% 23.93/3.90 % (3307998)Termination phase: Saturation
% 23.93/3.90 % (3307998)Time elapsed: 0.087 s
% 23.93/3.90 % (3307998)Peak memory usage: 13 MB
% 23.93/3.90 % (3307998)Instructions burned: 132 (million)
% 23.93/3.90 % (3308016)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=49127026:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 23.93/3.90 % (3308008)Instruction limit reached!
% 23.93/3.90 % (3308008)------------------------------
% 23.93/3.90 % (3308008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.90 % (3308008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.90 % (3308008)CaDiCaL version: 2.1.3
% 23.93/3.90 % (3308008)Termination reason: Instruction limit
% 23.93/3.90 % (3308008)Termination phase: Saturation
% 23.93/3.90 % (3308008)Time elapsed: 0.082 s
% 23.93/3.90 % (3308008)Peak memory usage: 12 MB
% 23.93/3.90 % (3308008)Instructions burned: 181 (million)
% 23.93/3.90 % (3308018)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2205105430:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 23.93/3.90 % TRYING [1]
% 23.93/3.90 % TRYING [2]
% 23.93/3.90 % TRYING [3]
% 23.93/3.90 % TRYING [6]
% 23.93/3.90 % TRYING [4]
% 23.93/3.90 % TRYING [5]
% 23.93/3.90 % TRYING [6]
% 23.93/3.90 % (3307993)Instruction limit reached!
% 23.93/3.90 % (3307993)------------------------------
% 23.93/3.90 % (3307993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.90 % (3307993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.90 % (3307993)CaDiCaL version: 2.1.3
% 23.93/3.90 % (3307993)Termination reason: Instruction limit
% 23.93/3.90 % (3307993)Termination phase: Finite model building constraint generation
% 23.93/3.90 % (3307993)Time elapsed: 0.348 s
% 23.93/3.90 % (3307993)Peak memory usage: 25 MB
% 23.93/3.90 % (3307993)Instructions burned: 715 (million)
% 23.93/3.90 % (3308004)Instruction limit reached!
% 23.93/3.90 % (3308004)------------------------------
% 23.93/3.90 % (3308004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.90 % (3308004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.90 % (3308004)CaDiCaL version: 2.1.3
% 23.93/3.90 % (3308004)Termination reason: Instruction limit
% 23.93/3.90 % (3308004)Termination phase: Saturation
% 23.93/3.90 % (3308004)Time elapsed: 0.343 s
% 23.93/3.90 % (3308004)Peak memory usage: 18 MB
% 23.93/3.90 % (3308004)Instructions burned: 685 (million)
% 23.93/3.90 % (3308020)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=131646126:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 23.93/3.90 % (3308016)Instruction limit reached!
% 23.93/3.90 % (3308016)------------------------------
% 23.93/3.90 % (3308016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.90 % (3308016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.90 % (3308016)CaDiCaL version: 2.1.3
% 23.93/3.90 % (3308016)Termination reason: Instruction limit
% 23.93/3.90 % (3308016)Termination phase: Saturation
% 23.93/3.90 % (3308016)Time elapsed: 0.260 s
% 23.93/3.90 % (3308016)Peak memory usage: 15 MB
% 23.93/3.90 % (3308016)Instructions burned: 477 (million)
% 23.93/3.90 % (3308021)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1422493032:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 23.93/3.90 % TRYING [6]
% 23.93/3.90 % (3308023)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=599189771: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)
% 23.93/3.90 % TRYING [14]
% 23.93/3.90 % (3308018)Instruction limit reached!
% 23.93/3.90 % (3308018)------------------------------
% 23.93/3.90 % (3308018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.90 % (3308018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.90 % (3308018)CaDiCaL version: 2.1.3
% 23.93/3.90 % (3308018)Termination reason: Instruction limit
% 23.93/3.90 % (3308018)Termination phase: Finite model building SAT solving
% 23.93/3.90 % (3308018)Time elapsed: 0.360 s
% 23.93/3.90 % (3308018)Peak memory usage: 22 MB
% 23.93/3.90 % (3308018)Instructions burned: 866 (million)
% 23.93/3.90 % (3308026)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2739848041:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 23.93/3.90 % (3308021)Instruction limit reached!
% 23.93/3.90 % (3308021)------------------------------
% 23.93/3.90 % (3308021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.90 % (3308021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.90 % (3308021)CaDiCaL version: 2.1.3
% 23.93/3.90 % (3308021)Termination reason: Instruction limit
% 23.93/3.90 % (3308021)Termination phase: Finite model building constraint generation
% 23.93/3.90 % (3308021)Time elapsed: 0.337 s
% 23.93/3.90 % (3308021)Peak memory usage: 82 MB
% 23.93/3.90 % (3308021)Instructions burned: 890 (million)
% 23.93/3.90 % (3308028)fmb+10_1_sil=64000:random_seed=917544475:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 23.93/3.90 % TRYING [1]
% 23.93/3.90 % TRYING [2]
% 23.93/3.90 % TRYING [3]
% 23.93/3.90 % TRYING [4]
% 23.93/3.90 % (3308023)Instruction limit reached!
% 23.93/3.90 % (3308023)------------------------------
% 23.93/3.90 % (3308023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.90 % (3308023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.90 % (3308023)CaDiCaL version: 2.1.3
% 23.93/3.90 % (3308023)Termination reason: Instruction limit
% 23.93/3.90 % (3308023)Termination phase: Saturation
% 23.93/3.90 % (3308023)Time elapsed: 0.396 s
% 23.93/3.90 % (3308023)Peak memory usage: 18 MB
% 23.93/3.90 % (3308023)Instructions burned: 693 (million)
% 23.93/3.90 % (3308030)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3006440097:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 23.93/3.90 % TRYING [20]
% 23.93/3.90 % TRYING [5]
% 23.93/3.90 % TRYING [7]
% 23.93/3.90 % (3308026)Instruction limit reached!
% 23.93/3.90 % (3308026)------------------------------
% 23.93/3.90 % (3308026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.90 % (3308026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.90 % (3308026)CaDiCaL version: 2.1.3
% 23.93/3.90 % (3308026)Termination reason: Instruction limit
% 23.93/3.90 % (3308026)Termination phase: Saturation
% 23.93/3.90 % (3308026)Time elapsed: 0.459 s
% 23.93/3.90 % (3308026)Peak memory usage: 19 MB
% 23.93/3.90 % (3308026)Instructions burned: 880 (million)
% 23.93/3.90 % (3308032)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2193966238:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 23.93/3.90 % TRYING [8]
% 23.93/3.90 % TRYING [6]
% 23.93/3.90 % (3308020)Instruction limit reached!
% 23.93/3.90 % (3308020)------------------------------
% 23.93/3.90 % (3308020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.90 % (3308020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.90 % (3308020)CaDiCaL version: 2.1.3
% 23.93/3.90 % (3308020)Termination reason: Instruction limit
% 23.93/3.90 % (3308020)Termination phase: Saturation
% 23.93/3.90 % (3308020)Time elapsed: 0.675 s
% 23.93/3.90 % (3308020)Peak memory usage: 21 MB
% 23.93/3.90 % (3308020)Instructions burned: 1180 (million)
% 23.93/3.90 % (3308034)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4258987361:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 23.93/3.90 % (3308032)Instruction limit reached!
% 23.93/3.90 % (3308032)------------------------------
% 23.93/3.90 % (3308032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.90 % (3308032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.90 % (3308032)CaDiCaL version: 2.1.3
% 23.93/3.90 % (3308032)Termination reason: Instruction limit
% 23.93/3.90 % (3308032)Termination phase: Finite model building SAT solving
% 23.93/3.90 % (3308032)Time elapsed: 0.374 s
% 23.93/3.90 % (3308032)Peak memory usage: 65 MB
% 23.93/3.90 % (3308032)Instructions burned: 922 (million)
% 23.93/3.90 % (3308036)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3080754626:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi)
% 23.93/3.90 % TRYING [7]
% 23.93/3.90 % (3308036)Instruction limit reached!
% 23.93/3.90 % (3308036)------------------------------
% 23.93/3.90 % (3308036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.90 % (3308036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.90 % (3308036)CaDiCaL version: 2.1.3
% 23.93/3.90 % (3308036)Termination reason: Instruction limit
% 23.93/3.90 % (3308036)Termination phase: Saturation
% 23.93/3.90 % (3308036)Time elapsed: 0.732 s
% 23.93/3.90 % (3308036)Peak memory usage: 25 MB
% 23.93/3.90 % (3308036)Instructions burned: 1474 (million)
% 23.93/3.90 % (3308038)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=225274028:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 23.93/3.90 % TRYING [77]
% 23.93/3.90 % (3307953) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3307934-3307953"...
% 23.93/3.90 % (3307953)...printing done.
% 23.93/3.90 % (3307953)Refutation found. Thanks to Tanya!
% 23.93/3.90 % SZS status Theorem for theBenchmark
% 23.93/3.90 % SZS output start Proof for theBenchmark
% See solution above
% 24.35/3.90 % (3307953)------------------------------
% 24.35/3.90 % (3307953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.35/3.90 % (3307953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.35/3.90 % (3307953)CaDiCaL version: 2.1.3
% 24.35/3.90 % (3307953)Termination reason: Refutation
% 24.35/3.90 % (3307953)Time elapsed: 3.361 s
% 24.35/3.90 % (3307953)Peak memory usage: 63 MB
% 24.35/3.90 % (3307953)Instructions burned: 6349 (million)
% 24.35/3.90 % (3307934)Success in time 3.484 s
% 24.35/3.90 % Vampire exiting
%------------------------------------------------------------------------------