%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : REL005+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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:13 PM UTC 2026
% Result : Theorem 40.45s 13.51s
% Output : Refutation 40.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 15
% Syntax : Number of formulae : 178 ( 178 unt; 0 def)
% Number of atoms : 178 ( 177 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 9 ( 9 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 269 ( 267 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/REL001+0.ax',composition_associativity) ).
fof(f6,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/REL001+0.ax',composition_distributivity) ).
fof(f8,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',converse_idempotence) ).
fof(f9,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',converse_additivity) ).
fof(f10,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/REL001+0.ax',converse_cancellativity) ).
fof(f12,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',def_top) ).
fof(f13,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',def_zero) ).
fof(f16,axiom,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2)) = meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+1.ax',modular_law_2) ).
fof(f17,conjecture,
! [X0,X1] : converse(meet(X0,X1)) = meet(converse(X0),converse(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f18,negated_conjecture,
~ ! [X0,X1] : converse(meet(X0,X1)) = meet(converse(X0),converse(X1)),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f19,plain,
? [X0,X1] : converse(meet(X0,X1)) != meet(converse(X0),converse(X1)),
inference(ennf_transformation,[],[f18]) ).
fof(f20,plain,
converse(meet(sK0,sK1)) != meet(converse(sK0),converse(sK1)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f19]) ).
fof(f21,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f22,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[],[f2]) ).
fof(f23,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f24,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = meet(X0,X1),
inference(cnf_transformation,[],[f4]) ).
fof(f25,plain,
! [X2,X0,X1] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f26,plain,
! [X0] : composition(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f27,plain,
! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
fof(f28,plain,
! [X0] : converse(converse(X0)) = X0,
inference(cnf_transformation,[],[f8]) ).
fof(f29,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[],[f9]) ).
fof(f30,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[],[f10]) ).
fof(f31,plain,
! [X0,X1] : complement(X1) = join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)),
inference(cnf_transformation,[],[f11]) ).
fof(f32,plain,
! [X0] : top = join(X0,complement(X0)),
inference(cnf_transformation,[],[f12]) ).
fof(f33,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(cnf_transformation,[],[f13]) ).
fof(f36,plain,
! [X2,X0,X1] : meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2) = join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2)),
inference(cnf_transformation,[],[f16]) ).
fof(f37,plain,
converse(meet(sK0,sK1)) != meet(converse(sK0),converse(sK1)),
inference(cnf_transformation,[],[f20]) ).
fof(f38,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f33,f24]) ).
fof(f41,plain,
! [X2,X0,X1] : complement(join(complement(composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),X1)),complement(X2))) = join(complement(join(complement(composition(X0,X1)),complement(X2))),complement(join(complement(composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),X1)),complement(X2)))),
inference(definition_unfolding,[],[f36,f24,f24,f24,f24,f24]) ).
fof(f42,plain,
converse(complement(join(complement(sK0),complement(sK1)))) != complement(join(complement(converse(sK0)),complement(converse(sK1)))),
inference(definition_unfolding,[],[f37,f24,f24]) ).
fof(f43,plain,
! [X0,X1] : join(X0,complement(X0)) = join(X1,complement(X1)),
inference(superposition,[],[f32,f32]) ).
fof(f46,plain,
zero = complement(top),
inference(superposition,[],[f38,f32]) ).
fof(f59,plain,
! [X0] : zero = complement(join(X0,complement(X0))),
inference(superposition,[],[f38,f43]) ).
fof(f66,plain,
! [X0] : complement(top) = complement(join(X0,complement(X0))),
inference(superposition,[],[f59,f46]) ).
fof(f96,plain,
! [X0] : top = join(top,complement(join(X0,complement(X0)))),
inference(superposition,[],[f32,f66]) ).
fof(f211,plain,
! [X0] : join(converse(X0),converse(complement(X0))) = converse(top),
inference(superposition,[],[f29,f32]) ).
fof(f225,plain,
! [X0] : converse(top) = join(X0,converse(complement(converse(X0)))),
inference(superposition,[],[f211,f28]) ).
fof(f268,plain,
! [X0] : converse(X0) = composition(converse(one),converse(X0)),
inference(superposition,[],[f30,f26]) ).
fof(f276,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(superposition,[],[f268,f28]) ).
fof(f281,plain,
one = converse(one),
inference(superposition,[],[f276,f26]) ).
fof(f285,plain,
! [X0] : composition(one,X0) = X0,
inference(superposition,[],[f276,f281]) ).
fof(f330,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f22,f32]) ).
fof(f331,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f22,f21]) ).
fof(f343,plain,
! [X0,X1] : top = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f22,f32]) ).
fof(f344,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X1,join(X2,X0)),
inference(superposition,[],[f22,f21]) ).
fof(f434,plain,
! [X0,X1] : join(top,X0) = join(X1,join(X0,complement(X1))),
inference(superposition,[],[f330,f21]) ).
fof(f441,plain,
! [X0] : join(X0,top) = join(top,complement(complement(X0))),
inference(superposition,[],[f330,f32]) ).
fof(f522,plain,
! [X0] : join(top,X0) = join(top,complement(complement(X0))),
inference(superposition,[],[f441,f21]) ).
fof(f532,plain,
! [X0] : join(X0,top) = join(complement(complement(X0)),top),
inference(superposition,[],[f441,f21]) ).
fof(f571,plain,
! [X0] : join(top,X0) = join(complement(complement(X0)),top),
inference(superposition,[],[f522,f21]) ).
fof(f788,plain,
! [X0,X1] : join(X1,join(X0,complement(X1))) = join(X0,top),
inference(superposition,[],[f434,f21]) ).
fof(f1724,plain,
! [X0,X1] : join(top,X1) = join(complement(X0),join(X0,X1)),
inference(superposition,[],[f331,f32]) ).
fof(f1753,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(superposition,[],[f331,f22]) ).
fof(f1934,plain,
! [X0,X1] : join(top,X0) = join(complement(X1),join(X0,X1)),
inference(superposition,[],[f1724,f21]) ).
fof(f2792,plain,
! [X0,X1] : composition(top,X1) = join(composition(X0,X1),composition(complement(X0),X1)),
inference(superposition,[],[f27,f32]) ).
fof(f3251,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X2,X0)),
inference(superposition,[],[f344,f21]) ).
fof(f4589,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(join(X1,X2),X0),
inference(superposition,[],[f3251,f21]) ).
fof(f8655,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(converse(X0),complement(composition(X0,X1)))),
inference(forward_demodulation,[],[f31,f21]) ).
fof(f11269,plain,
! [X0,X1] : zero = join(zero,composition(converse(X1),complement(composition(X1,join(complement(X0),complement(complement(X0))))))),
inference(superposition,[],[f8655,f38]) ).
fof(f11290,plain,
! [X0] : complement(X0) = join(complement(X0),complement(composition(one,X0))),
inference(superposition,[],[f8655,f276]) ).
fof(f11293,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(X0),join(composition(converse(X1),complement(composition(X1,X0))),X2)),
inference(superposition,[],[f22,f8655]) ).
fof(f11343,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(forward_demodulation,[],[f11290,f285]) ).
fof(f11358,plain,
! [X0,X1] : complement(top) = join(complement(top),composition(converse(X1),complement(composition(X1,join(complement(X0),complement(complement(X0))))))),
inference(forward_demodulation,[],[f11269,f46]) ).
fof(f11388,plain,
! [X0] : join(X0,complement(X0)) = join(complement(X0),top),
inference(superposition,[],[f788,f11343]) ).
fof(f11483,plain,
! [X0] : top = join(complement(X0),join(top,complement(join(X0,complement(X0))))),
inference(superposition,[],[f343,f11388]) ).
fof(f11529,plain,
! [X0] : top = join(complement(X0),top),
inference(forward_demodulation,[],[f11483,f96]) ).
fof(f11588,plain,
! [X0] : top = join(top,X0),
inference(superposition,[],[f11529,f571]) ).
fof(f11589,plain,
! [X0] : top = join(X0,top),
inference(superposition,[],[f11529,f532]) ).
fof(f11720,plain,
top = converse(top),
inference(superposition,[],[f11588,f225]) ).
fof(f12125,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f23,f21]) ).
fof(f13797,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(join(complement(join(complement(X0),X1)),join(complement(X0),complement(X1)))),complement(X0)),
inference(superposition,[],[f12125,f12125]) ).
fof(f13801,plain,
! [X0] : join(complement(join(complement(X0),complement(X0))),complement(top)) = X0,
inference(superposition,[],[f12125,f32]) ).
fof(f13816,plain,
! [X0,X1] : converse(X0) = join(converse(complement(join(complement(X0),X1))),converse(complement(join(complement(X0),complement(X1))))),
inference(superposition,[],[f29,f12125]) ).
fof(f13871,plain,
! [X0] : join(complement(complement(X0)),complement(top)) = X0,
inference(forward_demodulation,[],[f13801,f11343]) ).
fof(f13875,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(join(complement(X0),X1)),join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f13797,f21]) ).
fof(f13937,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(X0),join(complement(X1),complement(join(complement(X0),X1)))))),
inference(forward_demodulation,[],[f13875,f344]) ).
fof(f13976,plain,
! [X0] : join(complement(top),complement(complement(X0))) = X0,
inference(superposition,[],[f13871,f21]) ).
fof(f13979,plain,
! [X0] : complement(X0) = join(complement(join(complement(complement(X0)),top)),complement(X0)),
inference(superposition,[],[f12125,f13871]) ).
fof(f14043,plain,
! [X0] : complement(X0) = join(complement(X0),complement(join(complement(complement(X0)),top))),
inference(forward_demodulation,[],[f13979,f21]) ).
fof(f14061,plain,
! [X0] : complement(X0) = join(complement(X0),complement(top)),
inference(forward_demodulation,[],[f14043,f11589]) ).
fof(f14522,plain,
! [X0] : complement(complement(X0)) = X0,
inference(superposition,[],[f14061,f13871]) ).
fof(f14618,plain,
! [X0] : join(X0,complement(top)) = X0,
inference(superposition,[],[f13871,f14522]) ).
fof(f14619,plain,
! [X0] : join(complement(top),X0) = X0,
inference(superposition,[],[f13976,f14522]) ).
fof(f14664,plain,
! [X0] : join(X0,X0) = X0,
inference(superposition,[],[f11343,f14522]) ).
fof(f14752,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(superposition,[],[f22,f14664]) ).
fof(f14769,plain,
! [X0] : join(complement(X0),X0) = join(top,X0),
inference(superposition,[],[f1934,f14664]) ).
fof(f14846,plain,
! [X0] : join(X0,complement(X0)) = join(top,X0),
inference(forward_demodulation,[],[f14769,f21]) ).
fof(f14871,plain,
! [X0,X1] : join(X1,complement(join(X0,complement(X0)))) = X1,
inference(superposition,[],[f14618,f32]) ).
fof(f15013,plain,
! [X0,X1] : join(complement(join(X0,complement(X0))),X1) = X1,
inference(superposition,[],[f14619,f32]) ).
fof(f15917,plain,
! [X0,X1] : join(X0,complement(X0)) = join(top,X1),
inference(superposition,[],[f14846,f43]) ).
fof(f17477,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),X0) = X0,
inference(superposition,[],[f14752,f12125]) ).
fof(f17660,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f17477,f21]) ).
fof(f19320,plain,
! [X2,X0,X1] : complement(join(complement(X2),complement(composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),X1)))) = join(complement(join(complement(composition(X0,X1)),complement(X2))),complement(join(complement(X2),complement(composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),X1))))),
inference(forward_demodulation,[],[f41,f21]) ).
fof(f20177,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f17660,f14522]) ).
fof(f20208,plain,
! [X0,X1] : join(X1,complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f17660,f21]) ).
fof(f20281,plain,
! [X0,X1] : join(top,X0) = join(join(complement(X0),X1),X0),
inference(superposition,[],[f434,f17660]) ).
fof(f20355,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X0),
inference(forward_demodulation,[],[f20281,f21]) ).
fof(f21559,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(superposition,[],[f20208,f14522]) ).
fof(f32030,plain,
! [X2,X0,X1] : join(join(top,X0),X1) = join(join(X1,X0),join(complement(X0),X2)),
inference(superposition,[],[f4589,f20355]) ).
fof(f32197,plain,
! [X2,X0,X1] : join(join(top,X0),X1) = join(complement(X0),join(join(X1,X0),X2)),
inference(forward_demodulation,[],[f32030,f1753]) ).
fof(f32380,plain,
! [X2,X0,X1] : join(join(top,X0),X1) = join(complement(X0),join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f32197,f22]) ).
fof(f32459,plain,
! [X2,X0,X1] : join(top,join(X0,X1)) = join(complement(X0),join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f32380,f22]) ).
fof(f32490,plain,
! [X2,X0,X1] : top = join(complement(X0),join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f32459,f11588]) ).
fof(f35487,plain,
! [X0,X1] : join(top,composition(complement(X1),X0)) = join(complement(composition(X1,X0)),composition(top,X0)),
inference(superposition,[],[f1724,f2792]) ).
fof(f35522,plain,
! [X0,X1] : top = join(complement(composition(X1,X0)),composition(top,X0)),
inference(forward_demodulation,[],[f35487,f11588]) ).
fof(f35758,plain,
! [X0] : top = join(complement(X0),composition(top,X0)),
inference(superposition,[],[f35522,f276]) ).
fof(f35961,plain,
top = composition(top,top),
inference(superposition,[],[f35758,f14619]) ).
fof(f35967,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(composition(top,X0))))) = X0,
inference(superposition,[],[f12125,f35758]) ).
fof(f36038,plain,
! [X0] : complement(join(complement(X0),complement(composition(top,X0)))) = X0,
inference(forward_demodulation,[],[f35967,f14619]) ).
fof(f36142,plain,
! [X0] : complement(join(complement(X0),complement(composition(complement(join(complement(top),complement(composition(X0,converse(top))))),top)))) = join(complement(join(complement(top),complement(X0))),complement(join(complement(X0),complement(composition(complement(join(complement(top),complement(composition(X0,converse(top))))),top))))),
inference(superposition,[],[f19320,f35961]) ).
fof(f36144,plain,
! [X0] : complement(join(complement(X0),complement(composition(complement(complement(composition(X0,converse(top)))),top)))) = join(complement(join(complement(top),complement(X0))),complement(join(complement(X0),complement(composition(complement(complement(composition(X0,converse(top)))),top))))),
inference(forward_demodulation,[],[f36142,f14619]) ).
fof(f36161,plain,
! [X0] : complement(join(complement(X0),complement(composition(composition(X0,converse(top)),top)))) = join(complement(join(complement(top),complement(X0))),complement(join(complement(X0),complement(composition(composition(X0,converse(top)),top))))),
inference(forward_demodulation,[],[f36144,f14522]) ).
fof(f36172,plain,
! [X0] : complement(join(complement(X0),complement(composition(X0,composition(converse(top),top))))) = join(complement(join(complement(top),complement(X0))),complement(join(complement(X0),complement(composition(X0,composition(converse(top),top)))))),
inference(forward_demodulation,[],[f36161,f25]) ).
fof(f36177,plain,
! [X0] : complement(join(complement(X0),complement(composition(X0,composition(top,top))))) = join(complement(join(complement(top),complement(X0))),complement(join(complement(X0),complement(composition(X0,composition(top,top)))))),
inference(forward_demodulation,[],[f36172,f11720]) ).
fof(f36180,plain,
! [X0] : complement(join(complement(X0),complement(composition(X0,top)))) = join(complement(join(complement(top),complement(X0))),complement(join(complement(X0),complement(composition(X0,top))))),
inference(forward_demodulation,[],[f36177,f35961]) ).
fof(f36183,plain,
! [X0] : complement(join(complement(X0),complement(composition(X0,top)))) = join(complement(complement(X0)),complement(join(complement(X0),complement(composition(X0,top))))),
inference(forward_demodulation,[],[f36180,f14619]) ).
fof(f36186,plain,
! [X0] : complement(complement(X0)) = complement(join(complement(X0),complement(composition(X0,top)))),
inference(forward_demodulation,[],[f36183,f20177]) ).
fof(f36188,plain,
! [X0] : complement(join(complement(X0),complement(composition(X0,top)))) = X0,
inference(forward_demodulation,[],[f36186,f14522]) ).
fof(f38316,plain,
! [X0] : composition(top,X0) = join(composition(top,X0),X0),
inference(superposition,[],[f20208,f36038]) ).
fof(f38501,plain,
! [X0] : composition(top,X0) = join(X0,composition(top,X0)),
inference(forward_demodulation,[],[f38316,f21]) ).
fof(f38696,plain,
! [X0] : join(X0,complement(X0)) = composition(top,top),
inference(superposition,[],[f38501,f15917]) ).
fof(f38976,plain,
! [X0] : converse(join(X0,complement(X0))) = composition(converse(top),converse(top)),
inference(superposition,[],[f30,f38696]) ).
fof(f38989,plain,
! [X0] : converse(join(X0,complement(X0))) = composition(top,top),
inference(forward_demodulation,[],[f38976,f11720]) ).
fof(f39110,plain,
! [X0] : join(converse(X0),converse(complement(X0))) = composition(top,top),
inference(forward_demodulation,[],[f38989,f29]) ).
fof(f40620,plain,
! [X0] : composition(X0,top) = join(composition(X0,top),X0),
inference(superposition,[],[f20208,f36188]) ).
fof(f40814,plain,
! [X0] : composition(X0,top) = join(X0,composition(X0,top)),
inference(forward_demodulation,[],[f40620,f21]) ).
fof(f56515,plain,
! [X0,X1] : top = join(complement(X0),join(X1,composition(X0,top))),
inference(superposition,[],[f32490,f40814]) ).
fof(f67788,plain,
! [X0,X1] : top = join(complement(top),join(X1,join(converse(X0),converse(complement(X0))))),
inference(superposition,[],[f56515,f39110]) ).
fof(f67808,plain,
! [X0,X1] : top = join(X1,join(converse(X0),converse(complement(X0)))),
inference(forward_demodulation,[],[f67788,f14619]) ).
fof(f76627,plain,
! [X0] : top = join(X0,join(one,converse(complement(one)))),
inference(superposition,[],[f67808,f281]) ).
fof(f77603,plain,
top = join(one,converse(complement(one))),
inference(superposition,[],[f76627,f14619]) ).
fof(f79904,plain,
! [X0,X1] : complement(top) = composition(converse(X1),complement(composition(X1,join(complement(X0),complement(complement(X0)))))),
inference(forward_demodulation,[],[f11358,f14619]) ).
fof(f79905,plain,
! [X0,X1] : complement(top) = composition(converse(X1),complement(composition(X1,join(complement(X0),X0)))),
inference(forward_demodulation,[],[f79904,f14522]) ).
fof(f79906,plain,
! [X0,X1] : complement(top) = composition(converse(X1),complement(composition(X1,join(X0,complement(X0))))),
inference(forward_demodulation,[],[f79905,f21]) ).
fof(f79907,plain,
! [X0,X1] : composition(converse(X1),complement(composition(X1,join(X0,complement(X0))))) = complement(join(one,converse(complement(one)))),
inference(forward_demodulation,[],[f79906,f77603]) ).
fof(f80091,plain,
! [X0,X1] : join(complement(join(X0,complement(X0))),X1) = join(complement(join(X0,complement(X0))),join(complement(join(one,converse(complement(one)))),X1)),
inference(superposition,[],[f11293,f79907]) ).
fof(f80367,plain,
! [X0,X1] : join(complement(join(X0,complement(X0))),X1) = join(complement(join(one,converse(complement(one)))),X1),
inference(forward_demodulation,[],[f80091,f15013]) ).
fof(f80550,plain,
! [X1] : join(complement(join(one,converse(complement(one)))),X1) = X1,
inference(forward_demodulation,[],[f80367,f15013]) ).
fof(f80988,plain,
! [X0] : converse(join(one,converse(complement(one)))) = join(converse(complement(X0)),converse(complement(join(complement(join(one,converse(complement(one)))),complement(X0))))),
inference(superposition,[],[f13816,f80550]) ).
fof(f81400,plain,
! [X0] : join(converse(complement(X0)),converse(complement(complement(X0)))) = converse(join(one,converse(complement(one)))),
inference(forward_demodulation,[],[f80988,f80550]) ).
fof(f81566,plain,
! [X0] : join(converse(complement(X0)),converse(complement(complement(X0)))) = join(converse(one),converse(converse(complement(one)))),
inference(forward_demodulation,[],[f81400,f29]) ).
fof(f81675,plain,
! [X0] : join(converse(complement(X0)),converse(complement(complement(X0)))) = join(converse(one),complement(one)),
inference(forward_demodulation,[],[f81566,f28]) ).
fof(f81752,plain,
! [X0] : join(converse(complement(X0)),converse(complement(complement(X0)))) = join(complement(one),converse(one)),
inference(forward_demodulation,[],[f81675,f21]) ).
fof(f81810,plain,
! [X0] : join(converse(complement(X0)),converse(complement(complement(X0)))) = join(complement(one),one),
inference(forward_demodulation,[],[f81752,f281]) ).
fof(f81844,plain,
! [X0] : join(converse(complement(X0)),converse(complement(complement(X0)))) = join(one,complement(one)),
inference(forward_demodulation,[],[f81810,f21]) ).
fof(f81861,plain,
! [X0] : join(converse(complement(X0)),converse(X0)) = join(one,complement(one)),
inference(forward_demodulation,[],[f81844,f14522]) ).
fof(f81871,plain,
! [X0] : join(converse(X0),converse(complement(X0))) = join(one,complement(one)),
inference(forward_demodulation,[],[f81861,f21]) ).
fof(f87539,plain,
! [X0] : join(X0,converse(complement(converse(X0)))) = join(one,complement(one)),
inference(superposition,[],[f81871,f28]) ).
fof(f87598,plain,
! [X0,X1] : join(X0,complement(X0)) = join(converse(X1),converse(complement(X1))),
inference(superposition,[],[f81871,f43]) ).
fof(f91072,plain,
! [X0,X1] : join(complement(join(complement(X1),complement(X1))),complement(join(converse(X0),converse(complement(X0))))) = X1,
inference(superposition,[],[f12125,f87598]) ).
fof(f91277,plain,
! [X0,X1] : join(complement(complement(X1)),complement(join(converse(X0),converse(complement(X0))))) = X1,
inference(forward_demodulation,[],[f91072,f14664]) ).
fof(f91468,plain,
! [X0,X1] : join(X1,complement(join(converse(X0),converse(complement(X0))))) = X1,
inference(forward_demodulation,[],[f91277,f14522]) ).
fof(f120736,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[],[f13937,f21559]) ).
fof(f121147,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,complement(X1)))),
inference(superposition,[],[f120736,f14522]) ).
fof(f121815,plain,
! [X0,X1] : join(X1,complement(X0)) = join(X1,complement(join(X1,X0))),
inference(superposition,[],[f121147,f14522]) ).
fof(f122678,plain,
! [X0] : join(X0,complement(join(one,complement(one)))) = join(X0,complement(converse(complement(converse(X0))))),
inference(superposition,[],[f121815,f87539]) ).
fof(f122842,plain,
! [X0] : converse(X0) = join(converse(X0),complement(converse(complement(X0)))),
inference(superposition,[],[f121815,f91468]) ).
fof(f123247,plain,
! [X0] : join(X0,complement(converse(complement(converse(X0))))) = X0,
inference(forward_demodulation,[],[f122678,f14871]) ).
fof(f124181,plain,
! [X0] : converse(converse(X0)) = join(converse(converse(X0)),converse(complement(converse(complement(X0))))),
inference(superposition,[],[f29,f122842]) ).
fof(f124236,plain,
! [X0] : join(X0,converse(complement(converse(complement(X0))))) = X0,
inference(forward_demodulation,[],[f124181,f28]) ).
fof(f124655,plain,
! [X0] : complement(converse(complement(converse(complement(X0))))) = join(complement(converse(complement(converse(complement(X0))))),complement(X0)),
inference(superposition,[],[f21559,f124236]) ).
fof(f124710,plain,
! [X0] : complement(converse(complement(converse(complement(X0))))) = join(complement(X0),complement(converse(complement(converse(complement(X0)))))),
inference(forward_demodulation,[],[f124655,f21]) ).
fof(f124787,plain,
! [X0] : complement(X0) = complement(converse(complement(converse(complement(X0))))),
inference(forward_demodulation,[],[f124710,f123247]) ).
fof(f125029,plain,
! [X0,X1] : join(converse(complement(join(complement(X0),X1))),converse(complement(join(complement(X0),complement(X1))))) = converse(converse(complement(converse(complement(X0))))),
inference(superposition,[],[f13816,f124787]) ).
fof(f125294,plain,
! [X0,X1] : complement(converse(complement(X0))) = join(converse(complement(join(complement(X0),X1))),converse(complement(join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f125029,f28]) ).
fof(f125473,plain,
! [X0] : converse(X0) = complement(converse(complement(X0))),
inference(forward_demodulation,[],[f125294,f13816]) ).
fof(f126810,plain,
! [X0] : converse(complement(X0)) = complement(converse(X0)),
inference(superposition,[],[f125473,f14522]) ).
fof(f128405,plain,
complement(join(complement(converse(sK0)),complement(converse(sK1)))) != complement(converse(join(complement(sK0),complement(sK1)))),
inference(superposition,[],[f42,f126810]) ).
fof(f128632,plain,
complement(join(complement(converse(sK0)),complement(converse(sK1)))) != complement(join(converse(complement(sK0)),converse(complement(sK1)))),
inference(forward_demodulation,[],[f128405,f29]) ).
fof(f128750,plain,
complement(join(complement(converse(sK0)),complement(converse(sK1)))) != complement(join(converse(complement(sK0)),complement(converse(sK1)))),
inference(forward_demodulation,[],[f128632,f126810]) ).
fof(f128838,plain,
complement(join(complement(converse(sK0)),complement(converse(sK1)))) != complement(join(complement(converse(sK0)),complement(converse(sK1)))),
inference(forward_demodulation,[],[f128750,f126810]) ).
fof(f128839,plain,
$false,
inference(trivial_inequality_removal,[],[f128838]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL005+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.21/5.48 % Computer : n016.cluster.edu
% 0.21/5.48 % Model : x86_64 x86_64
% 0.21/5.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/5.48 % Memory : 8046.5625MB
% 0.21/5.48 % OS : Linux 6.8.0-71-generic
% 0.21/5.48 % CPULimit : 300
% 0.21/5.48 % WCLimit : 300
% 0.21/5.48 % DateTime : Sun Sep 27 22:54:53 UTC 2026
% 0.21/5.49 % CPUTime :
% 0.21/5.49 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.25/5.52 Running first-order model finding
% 0.25/5.52 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.10/7.58 % (3076888)Will run a generic schedule for satisfiability detection.
% 14.10/7.58 % (3076894)% WARNING: option uhcvi not known.
% 14.10/7.58 % (3076896)dis+10_1_sil=32000:sp=arity:random_seed=459091345:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.10/7.58 % (3076893)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1082694582_2999 on theBenchmark for (2999ds/0Mi)
% 14.10/7.58 % (3076894)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1656377719:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.10/7.58 % (3076895)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2321232802:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.10/7.58 % (3076897)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2740491564:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.10/7.58 % (3076898)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2970593519:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.10/7.58 % (3076899)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=358912700:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.10/7.58 % TRYING [1]
% 14.10/7.58 % TRYING [2]
% 14.10/7.58 % TRYING [3]
% 14.10/7.58 % TRYING [4]
% 14.10/7.58 % (3076896)Instruction limit reached!
% 14.10/7.58 % (3076896)------------------------------
% 14.10/7.58 % (3076896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.10/7.58 % (3076896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.10/7.58 % (3076896)CaDiCaL version: 2.1.3
% 14.10/7.58 % (3076896)Termination reason: Instruction limit
% 14.10/7.58 % (3076896)Termination phase: Saturation
% 14.10/7.58 % (3076896)Time elapsed: 0.059 s
% 14.10/7.58 % (3076896)Peak memory usage: 13 MB
% 14.10/7.58 % (3076896)Instructions burned: 104 (million)
% 14.10/7.58 % (3076897)Instruction limit reached!
% 14.10/7.58 % (3076897)------------------------------
% 14.10/7.58 % (3076897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.10/7.58 % (3076897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.10/7.58 % (3076897)CaDiCaL version: 2.1.3
% 14.10/7.58 % (3076897)Termination reason: Instruction limit
% 14.10/7.58 % (3076897)Termination phase: Saturation
% 14.10/7.59 % (3076897)Time elapsed: 0.069 s
% 14.10/7.59 % (3076897)Peak memory usage: 13 MB
% 14.10/7.59 % (3076897)Instructions burned: 116 (million)
% 14.10/7.59 % (3076898)Instruction limit reached!
% 14.10/7.59 % (3076898)------------------------------
% 14.10/7.59 % (3076898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.10/7.59 % (3076898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.10/7.59 % (3076898)CaDiCaL version: 2.1.3
% 14.10/7.59 % (3076898)Termination reason: Instruction limit
% 14.10/7.59 % (3076898)Termination phase: Saturation
% 14.10/7.59 % (3076898)Time elapsed: 0.076 s
% 14.10/7.59 % (3076898)Peak memory usage: 13 MB
% 14.10/7.59 % (3076898)Instructions burned: 131 (million)
% 14.10/7.59 % (3076907)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1434715168:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.10/7.59 % TRYING [1]
% 14.10/7.59 % TRYING [2]
% 14.10/7.59 % (3076908)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=627618920:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.10/7.59 % TRYING [3]
% 14.10/7.59 % (3076909)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=284580118:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.10/7.59 % (3076899)Instruction limit reached!
% 14.10/7.59 % (3076899)------------------------------
% 14.10/7.59 % (3076899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.10/7.59 % (3076899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.10/7.59 % (3076899)CaDiCaL version: 2.1.3
% 14.10/7.59 % (3076899)Termination reason: Instruction limit
% 14.10/7.59 % (3076899)Termination phase: Saturation
% 14.10/7.59 % (3076899)Time elapsed: 0.095 s
% 14.10/7.59 % (3076899)Peak memory usage: 13 MB
% 14.10/7.59 % (3076899)Instructions burned: 160 (million)
% 14.10/7.59 % (3076913)ott-21_1_sil=16000:fs=off:random_seed=878307877:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.10/7.59 % TRYING [4]
% 14.10/7.59 % (3076908)Instruction limit reached!
% 14.10/7.59 % (3076908)------------------------------
% 14.10/7.59 % (3076908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.10/7.59 % (3076908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.96/10.36 % (3076908)CaDiCaL version: 2.1.3
% 33.96/10.36 % (3076908)Termination reason: Instruction limit
% 33.96/10.36 % (3076908)Termination phase: Saturation
% 33.96/10.36 % (3076908)Time elapsed: 0.082 s
% 33.96/10.36 % (3076908)Peak memory usage: 13 MB
% 33.96/10.36 % (3076908)Instructions burned: 131 (million)
% 33.96/10.36 % (3076915)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=474210581:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 33.96/10.36 % (3076913)Instruction limit reached!
% 33.96/10.36 % (3076913)------------------------------
% 33.96/10.36 % (3076913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.96/10.36 % (3076913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.96/10.36 % (3076913)CaDiCaL version: 2.1.3
% 33.96/10.36 % (3076913)Termination reason: Instruction limit
% 33.96/10.36 % (3076913)Termination phase: Saturation
% 33.96/10.36 % (3076913)Time elapsed: 0.084 s
% 33.96/10.36 % (3076913)Peak memory usage: 12 MB
% 33.96/10.36 % (3076913)Instructions burned: 182 (million)
% 33.96/10.36 % (3076917)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3989344779:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 33.96/10.36 % TRYING [1]
% 33.96/10.36 % TRYING [2]
% 33.96/10.36 % TRYING [5]
% 33.96/10.36 % TRYING [3]
% 33.96/10.36 % TRYING [4]
% 33.96/10.36 % TRYING [5]
% 33.96/10.36 % (3076907)Instruction limit reached!
% 33.96/10.36 % (3076907)------------------------------
% 33.96/10.36 % (3076907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.96/10.36 % (3076907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.96/10.36 % (3076907)CaDiCaL version: 2.1.3
% 33.96/10.36 % (3076907)Termination reason: Instruction limit
% 33.96/10.36 % (3076907)Termination phase: Finite model building constraint generation
% 33.96/10.36 % (3076907)Time elapsed: 0.281 s
% 33.96/10.36 % (3076907)Peak memory usage: 28 MB
% 33.96/10.36 % (3076907)Instructions burned: 717 (million)
% 33.96/10.36 % (3076917)Instruction limit reached!
% 33.96/10.36 % (3076917)------------------------------
% 33.96/10.36 % (3076917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.96/10.36 % (3076917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.96/10.36 % (3076917)CaDiCaL version: 2.1.3
% 33.96/10.36 % (3076917)Termination reason: Instruction limit
% 33.96/10.36 % (3076917)Termination phase: Finite model building SAT solving
% 33.96/10.36 % (3076917)Time elapsed: 0.161 s
% 33.96/10.36 % (3076917)Peak memory usage: 24 MB
% 33.96/10.36 % (3076917)Instructions burned: 871 (million)
% 33.96/10.36 % (3076919)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1424708748:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 33.96/10.36 % (3076920)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4161552014:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 33.96/10.36 % (3076909)Instruction limit reached!
% 33.96/10.36 % (3076909)------------------------------
% 33.96/10.36 % (3076909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.96/10.36 % (3076909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.96/10.36 % (3076909)CaDiCaL version: 2.1.3
% 33.96/10.36 % (3076909)Termination reason: Instruction limit
% 33.96/10.36 % (3076909)Termination phase: Saturation
% 33.96/10.36 % (3076909)Time elapsed: 0.352 s
% 33.96/10.36 % (3076909)Peak memory usage: 18 MB
% 33.96/10.36 % (3076909)Instructions burned: 685 (million)
% 33.96/10.36 % (3076915)Instruction limit reached!
% 33.96/10.36 % (3076915)------------------------------
% 33.96/10.36 % (3076915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.96/10.36 % (3076915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.96/10.36 % (3076915)CaDiCaL version: 2.1.3
% 33.96/10.36 % (3076915)Termination reason: Instruction limit
% 33.96/10.36 % (3076915)Termination phase: Saturation
% 33.96/10.36 % (3076915)Time elapsed: 0.259 s
% 33.96/10.36 % (3076915)Peak memory usage: 16 MB
% 33.96/10.36 % (3076915)Instructions burned: 479 (million)
% 33.96/10.36 % (3076923)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=305009007: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)
% 33.96/10.36 % (3076924)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3406491550:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 33.96/10.36 % (3076920)Instruction limit reached!
% 33.96/10.36 % (3076920)------------------------------
% 40.45/13.51 % (3076920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/13.51 % (3076920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/13.51 % (3076920)CaDiCaL version: 2.1.3
% 40.45/13.51 % (3076920)Termination reason: Instruction limit
% 40.45/13.51 % (3076920)Termination phase: Finite model building constraint generation
% 40.45/13.51 % (3076920)Time elapsed: 0.235 s
% 40.45/13.51 % (3076920)Peak memory usage: 106 MB
% 40.45/13.51 % (3076920)Instructions burned: 892 (million)
% 40.45/13.51 % (3076927)fmb+10_1_sil=64000:random_seed=1229010093:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 40.45/13.51 % TRYING [1]
% 40.45/13.51 % TRYING [2]
% 40.45/13.51 % TRYING [3]
% 40.45/13.51 % TRYING [4]
% 40.45/13.51 % TRYING [5]
% 40.45/13.51 % (3076923)Instruction limit reached!
% 40.45/13.51 % (3076923)------------------------------
% 40.45/13.51 % (3076923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/13.51 % (3076923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/13.51 % (3076923)CaDiCaL version: 2.1.3
% 40.45/13.51 % (3076923)Termination reason: Instruction limit
% 40.45/13.51 % (3076923)Termination phase: Saturation
% 40.45/13.51 % (3076923)Time elapsed: 0.405 s
% 40.45/13.51 % (3076923)Peak memory usage: 19 MB
% 40.45/13.51 % (3076923)Instructions burned: 694 (million)
% 40.45/13.51 % (3076929)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3694831636:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 40.45/13.51 % TRYING [20]
% 40.45/13.51 % TRYING [6]
% 40.45/13.51 % (3076924)Instruction limit reached!
% 40.45/13.51 % (3076924)------------------------------
% 40.45/13.51 % (3076924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/13.51 % (3076924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/13.51 % (3076924)CaDiCaL version: 2.1.3
% 40.45/13.51 % (3076924)Termination reason: Instruction limit
% 40.45/13.51 % (3076924)Termination phase: Saturation
% 40.45/13.51 % (3076924)Time elapsed: 0.460 s
% 40.45/13.51 % (3076924)Peak memory usage: 18 MB
% 40.45/13.51 % (3076924)Instructions burned: 879 (million)
% 40.45/13.51 % (3076931)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3197499411:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 40.45/13.51 % TRYING [8]
% 40.45/13.51 % (3076919)Instruction limit reached!
% 40.45/13.51 % (3076919)------------------------------
% 40.45/13.51 % (3076919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/13.51 % (3076919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/13.51 % (3076919)CaDiCaL version: 2.1.3
% 40.45/13.51 % (3076919)Termination reason: Instruction limit
% 40.45/13.51 % (3076919)Termination phase: Saturation
% 40.45/13.51 % (3076919)Time elapsed: 0.603 s
% 40.45/13.51 % (3076919)Peak memory usage: 21 MB
% 40.45/13.51 % (3076919)Instructions burned: 1180 (million)
% 40.45/13.51 % (3076933)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2992980005:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 40.45/13.51 % (3076931)Instruction limit reached!
% 40.45/13.51 % (3076931)------------------------------
% 40.45/13.51 % (3076931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/13.51 % (3076931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/13.51 % (3076931)CaDiCaL version: 2.1.3
% 40.45/13.51 % (3076931)Termination reason: Instruction limit
% 40.45/13.51 % (3076931)Termination phase: Finite model building constraint generation
% 40.45/13.51 % (3076931)Time elapsed: 0.321 s
% 40.45/13.51 % (3076931)Peak memory usage: 75 MB
% 40.45/13.51 % (3076931)Instructions burned: 923 (million)
% 40.45/13.51 % (3076935)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2799529421:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 40.45/13.51 % TRYING [6]
% 40.45/13.51 % (3076935)Instruction limit reached!
% 40.45/13.51 % (3076935)------------------------------
% 40.45/13.51 % (3076935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/13.51 % (3076935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/13.51 % (3076935)CaDiCaL version: 2.1.3
% 40.45/13.51 % (3076935)Termination reason: Instruction limit
% 40.45/13.51 % (3076935)Termination phase: Saturation
% 40.45/13.51 % (3076935)Time elapsed: 0.703 s
% 40.45/13.51 % (3076935)Peak memory usage: 24 MB
% 40.45/13.51 % (3076935)Instructions burned: 1473 (million)
% 40.45/13.51 % (3076937)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=304278705:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 40.45/13.51 % (3076937)Cannot represent all propositional literals internally
% 40.45/13.51 % (3076937)Refutation not found, incomplete strategy
% 40.45/13.51 % (3076937)------------------------------
% 40.45/13.51 % (3076937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/13.51 % (3076937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/13.51 % (3076937)CaDiCaL version: 2.1.3
% 40.45/13.51 % (3076937)Termination reason: Refutation not found, incomplete strategy
% 40.45/13.51 % (3076937)Time elapsed: 0.008 s
% 40.45/13.51 % (3076937)Peak memory usage: 10 MB
% 40.45/13.51 % (3076937)Instructions burned: 14 (million)
% 40.45/13.51 % (3076937)------------------------------
% 40.45/13.51 % (3076937)------------------------------
% 40.45/13.51 % (3076939)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1597972499:fmbsr=2.30978:i=2174_2979 on theBenchmark for (2979ds/2174Mi)
% 40.45/13.51 % TRYING [16]
% 40.45/13.51 % (3076939)Instruction limit reached!
% 40.45/13.51 % (3076939)------------------------------
% 40.45/13.51 % (3076939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/13.51 % (3076939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/13.51 % (3076939)CaDiCaL version: 2.1.3
% 40.45/13.51 % (3076939)Termination reason: Instruction limit
% 40.45/13.51 % (3076939)Termination phase: Finite model building constraint generation
% 40.45/13.51 % (3076939)Time elapsed: 0.734 s
% 40.45/13.51 % (3076939)Peak memory usage: 132 MB
% 40.45/13.51 % (3076939)Instructions burned: 2175 (million)
% 40.45/13.51 % (3076941)ott-2_1_sil=16000:newcnf=on:random_seed=3439326114:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2971 on theBenchmark for (2971ds/869Mi)
% 40.45/13.51 % (3076941)Instruction limit reached!
% 40.45/13.51 % (3076941)------------------------------
% 40.45/13.51 % (3076941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/13.51 % (3076941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/13.51 % (3076941)CaDiCaL version: 2.1.3
% 40.45/13.51 % (3076941)Termination reason: Instruction limit
% 40.45/13.51 % (3076941)Termination phase: Saturation
% 40.45/13.51 % (3076941)Time elapsed: 0.510 s
% 40.45/13.51 % (3076941)Peak memory usage: 20 MB
% 40.45/13.51 % (3076941)Instructions burned: 869 (million)
% 40.45/13.51 % (3076943)ott+10_1_sil=32000:tgt=ground:random_seed=729206178:i=5114:av=off_2966 on theBenchmark for (2966ds/5114Mi)
% 40.45/13.51 % TRYING [7]
% 40.45/13.51 % (3076933)Instruction limit reached!
% 40.45/13.51 % (3076933)------------------------------
% 40.45/13.51 % (3076933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/13.51 % (3076933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/13.51 % (3076933)CaDiCaL version: 2.1.3
% 40.45/13.51 % (3076933)Termination reason: Instruction limit
% 40.45/13.51 % (3076933)Termination phase: Saturation
% 40.45/13.51 % (3076933)Time elapsed: 2.760 s
% 40.45/13.51 % (3076933)Peak memory usage: 56 MB
% 40.45/13.51 % (3076933)Instructions burned: 5133 (million)
% 40.45/13.51 % (3076945)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2210993143:i=54282_2961 on theBenchmark for (2961ds/54282Mi)
% 40.45/13.51 % TRYING [1]
% 40.45/13.51 % TRYING [2]
% 40.45/13.51 % TRYING [3]
% 40.45/13.51 % TRYING [4]
% 40.45/13.51 % TRYING [7]
% 40.45/13.51 % TRYING [5]
% 40.45/13.51 % (3076929)Instruction limit reached!
% 40.45/13.51 % (3076929)------------------------------
% 40.45/13.51 % (3076929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/13.51 % (3076929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/13.51 % (3076929)CaDiCaL version: 2.1.3
% 40.45/13.51 % (3076929)Termination reason: Instruction limit
% 40.45/13.51 % (3076929)Termination phase: Finite model building constraint generation
% 40.45/13.51 % (3076929)Time elapsed: 3.376 s
% 40.45/13.51 % (3076929)Peak memory usage: 675 MB
% 40.45/13.51 % (3076929)Instructions burned: 9515 (million)
% 40.45/13.51 % (3076947)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4270785914:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi)
% 40.45/13.51 % TRYING [6]
% 40.45/13.51 % (3076927)Instruction limit reached!
% 40.45/13.51 % (3076927)------------------------------
% 40.45/13.51 % (3076927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/13.51 % (3076927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/13.51 % (3076927)CaDiCaL version: 2.1.3
% 40.45/13.51 % (3076927)Termination reason: Instruction limit
% 40.45/13.51 % (3076927)Termination phase: Finite model building constraint generation
% 40.45/13.51 % (3076927)Time elapsed: 4.165 s
% 40.45/13.51 % (3076927)Peak memory usage: 252 MB
% 40.45/13.51 % (3076927)Instructions burned: 22064 (million)
% 40.45/13.51 % (3076949)dis+21_1_sil=32000:sas=cadical:random_seed=2793736052:i=3773:amm=off_2951 on theBenchmark for (2951ds/3773Mi)
% 40.45/13.51 % (3076949)Instruction limit reached!
% 40.45/13.51 % (3076949)------------------------------
% 40.45/13.51 % (3076949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/13.51 % (3076949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/13.51 % (3076949)CaDiCaL version: 2.1.3
% 40.45/13.51 % (3076949)Termination reason: Instruction limit
% 40.45/13.51 % (3076949)Termination phase: Saturation
% 40.45/13.51 % (3076949)Time elapsed: 1.064 s
% 40.45/13.51 % (3076949)Peak memory usage: 42 MB
% 40.45/13.51 % (3076949)Instructions burned: 3774 (million)
% 40.45/13.51 % (3076951)ott+11_1_sil=16000:gs=on:random_seed=4274034922:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2940 on theBenchmark for (2940ds/2251Mi)
% 40.45/13.51 % (3076947)Instruction limit reached!
% 40.45/13.51 % (3076947)------------------------------
% 40.45/13.51 % (3076947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/13.51 % (3076947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/13.51 % (3076947)CaDiCaL version: 2.1.3
% 40.45/13.51 % (3076947)Termination reason: Instruction limit
% 40.45/13.51 % (3076947)Termination phase: Saturation
% 40.45/13.51 % (3076947)Time elapsed: 1.845 s
% 40.45/13.51 % (3076947)Peak memory usage: 40 MB
% 40.45/13.51 % (3076947)Instructions burned: 3513 (million)
% 40.45/13.51 % (3076953)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=439187255:fmbsr=1.6:i=67534_2937 on theBenchmark for (2937ds/67534Mi)
% 40.45/13.51 % TRYING [7]
% 40.45/13.51 % (3076943)Instruction limit reached!
% 40.45/13.51 % (3076943)------------------------------
% 40.45/13.51 % (3076943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/13.51 % (3076943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/13.51 % (3076943)CaDiCaL version: 2.1.3
% 40.45/13.51 % (3076943)Termination reason: Instruction limit
% 40.45/13.51 % (3076943)Termination phase: Saturation
% 40.45/13.51 % (3076943)Time elapsed: 2.978 s
% 40.45/13.51 % (3076943)Peak memory usage: 65 MB
% 40.45/13.51 % (3076943)Instructions burned: 5114 (million)
% 40.45/13.51 % (3076955)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3807911269:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2936 on theBenchmark for (2936ds/4591Mi)
% 40.45/13.51 % (3076951)Instruction limit reached!
% 40.45/13.51 % (3076951)------------------------------
% 40.45/13.51 % (3076951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/13.51 % (3076951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/13.51 % (3076951)CaDiCaL version: 2.1.3
% 40.45/13.51 % (3076951)Termination reason: Instruction limit
% 40.45/13.51 % (3076951)Termination phase: Saturation
% 40.45/13.51 % (3076951)Time elapsed: 0.688 s
% 40.45/13.51 % (3076951)Peak memory usage: 29 MB
% 40.45/13.51 % (3076951)Instructions burned: 2253 (million)
% 40.45/13.51 % (3076957)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=144867262:i=29340_2933 on theBenchmark for (2933ds/29340Mi)
% 40.45/13.51 % TRYING [7]
% 40.45/13.51 % (3076957) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3076888-3076957"...
% 40.45/13.51 % (3076957)...printing done.
% 40.45/13.51 % (3076957)Refutation found. Thanks to Tanya!
% 40.45/13.51 % SZS status Theorem for theBenchmark
% 40.45/13.51 % SZS output start Proof for theBenchmark
% See solution above
% 40.45/13.51 % (3076957)------------------------------
% 40.45/13.51 % (3076957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/13.51 % (3076957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/13.51 % (3076957)CaDiCaL version: 2.1.3
% 40.45/13.51 % (3076957)Termination reason: Refutation
% 40.45/13.51 % (3076957)Time elapsed: 1.272 s
% 40.45/13.51 % (3076957)Peak memory usage: 40 MB
% 40.45/13.51 % (3076957)Instructions burned: 4617 (million)
% 40.45/13.51 % (3076888)Success in time 7.984 s
% 40.45/13.51 % Vampire exiting
%------------------------------------------------------------------------------