%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : REL004+3 : 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 : n008.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:12 PM UTC 2026
% Result : Theorem 6.74s 1.44s
% Output : Refutation 6.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 14
% Syntax : Number of formulae : 135 ( 135 unt; 0 def)
% Number of atoms : 135 ( 134 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 170 ( 169 !; 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(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,axiom,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+1.ax',dedekind_law) ).
fof(f17,conjecture,
! [X0] : converse(complement(X0)) = complement(converse(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f18,negated_conjecture,
~ ! [X0] : converse(complement(X0)) = complement(converse(X0)),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f19,plain,
? [X0] : converse(complement(X0)) != complement(converse(X0)),
inference(ennf_transformation,[],[f18]) ).
fof(f20,plain,
converse(complement(sK0)) != complement(converse(sK0)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[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(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(f34,plain,
! [X2,X0,X1] : composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))) = join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))),
inference(cnf_transformation,[],[f14]) ).
fof(f37,plain,
converse(complement(sK0)) != complement(converse(sK0)),
inference(cnf_transformation,[],[f20]) ).
fof(f38,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f33,f24]) ).
fof(f39,plain,
! [X2,X0,X1] : composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),complement(join(complement(X1),complement(composition(converse(X0),X2))))) = join(complement(join(complement(composition(X0,X1)),complement(X2))),composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),complement(join(complement(X1),complement(composition(converse(X0),X2)))))),
inference(definition_unfolding,[],[f34,f24,f24,f24,f24,f24]) ).
fof(f42,plain,
zero = complement(top),
inference(forward_demodulation,[],[f38,f32]) ).
fof(f44,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[],[f29,f28]) ).
fof(f51,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[],[f30,f28]) ).
fof(f55,plain,
! [X0] : join(X0,converse(complement(converse(X0)))) = converse(top),
inference(superposition,[],[f44,f32]) ).
fof(f207,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f51,f26]) ).
fof(f223,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f207,f28]) ).
fof(f228,plain,
one = converse(one),
inference(superposition,[],[f223,f26]) ).
fof(f235,plain,
! [X0] : composition(one,X0) = X0,
inference(superposition,[],[f223,f228]) ).
fof(f439,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f22,f32]) ).
fof(f440,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f22,f21]) ).
fof(f448,plain,
! [X0,X1] : top = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f22,f32]) ).
fof(f479,plain,
! [X0,X1] : join(top,X0) = join(X1,join(X0,complement(X1))),
inference(superposition,[],[f439,f21]) ).
fof(f501,plain,
! [X0,X1] : top = join(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f448,f21]) ).
fof(f1007,plain,
! [X0,X1] : join(top,X1) = join(complement(X0),join(X0,X1)),
inference(superposition,[],[f440,f32]) ).
fof(f1227,plain,
! [X0,X1] : join(top,X0) = join(complement(X1),join(X0,X1)),
inference(superposition,[],[f1007,f21]) ).
fof(f1268,plain,
! [X0] : join(top,X0) = join(top,complement(complement(X0))),
inference(superposition,[],[f1007,f479]) ).
fof(f3987,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(converse(one),X1),X0),
inference(superposition,[],[f27,f223]) ).
fof(f4017,plain,
! [X0,X1] : composition(join(one,X1),X0) = join(X0,composition(X1,X0)),
inference(forward_demodulation,[],[f3987,f228]) ).
fof(f4676,plain,
! [X0] : composition(top,X0) = join(X0,composition(complement(one),X0)),
inference(superposition,[],[f4017,f32]) ).
fof(f8630,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(converse(X0),complement(composition(X0,X1)))),
inference(forward_demodulation,[],[f31,f21]) ).
fof(f12683,plain,
! [X0] : complement(one) = join(complement(one),composition(converse(X0),complement(X0))),
inference(superposition,[],[f8630,f26]) ).
fof(f12698,plain,
! [X0] : complement(X0) = join(complement(X0),complement(composition(one,X0))),
inference(superposition,[],[f8630,f223]) ).
fof(f12744,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(forward_demodulation,[],[f12698,f235]) ).
fof(f12793,plain,
zero = join(zero,zero),
inference(superposition,[],[f12744,f42]) ).
fof(f12816,plain,
! [X0] : top = join(complement(X0),join(complement(X0),complement(complement(X0)))),
inference(superposition,[],[f501,f12744]) ).
fof(f12835,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[],[f12816,f479]) ).
fof(f12885,plain,
! [X0] : join(zero,X0) = join(zero,join(zero,X0)),
inference(superposition,[],[f22,f12793]) ).
fof(f12977,plain,
! [X0] : top = join(top,X0),
inference(superposition,[],[f12835,f1268]) ).
fof(f13108,plain,
top = composition(top,top),
inference(superposition,[],[f12977,f4676]) ).
fof(f13109,plain,
top = converse(top),
inference(superposition,[],[f12977,f55]) ).
fof(f13445,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(superposition,[],[f8630,f13108]) ).
fof(f13451,plain,
complement(top) = composition(join(one,converse(top)),complement(top)),
inference(forward_demodulation,[],[f13445,f4017]) ).
fof(f13454,plain,
zero = composition(join(one,converse(top)),zero),
inference(forward_demodulation,[],[f13451,f42]) ).
fof(f13456,plain,
zero = join(zero,composition(converse(top),zero)),
inference(forward_demodulation,[],[f13454,f4017]) ).
fof(f13457,plain,
zero = join(zero,composition(top,zero)),
inference(forward_demodulation,[],[f13456,f13109]) ).
fof(f13711,plain,
composition(top,zero) = join(zero,composition(top,zero)),
inference(superposition,[],[f12885,f4676]) ).
fof(f13811,plain,
zero = composition(top,zero),
inference(forward_demodulation,[],[f13711,f13457]) ).
fof(f13828,plain,
! [X0] : join(zero,composition(X0,zero)) = composition(join(top,X0),zero),
inference(superposition,[],[f27,f13811]) ).
fof(f13830,plain,
! [X0] : join(zero,composition(X0,zero)) = composition(top,zero),
inference(forward_demodulation,[],[f13828,f12977]) ).
fof(f13833,plain,
! [X0] : zero = join(zero,composition(X0,zero)),
inference(forward_demodulation,[],[f13830,f13811]) ).
fof(f15231,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f23,f21]) ).
fof(f16520,plain,
! [X0] : join(complement(join(complement(X0),complement(X0))),complement(top)) = X0,
inference(superposition,[],[f15231,f32]) ).
fof(f16526,plain,
! [X0,X1] : join(join(complement(X0),X1),X0) = join(top,complement(join(complement(X0),complement(X1)))),
inference(superposition,[],[f439,f15231]) ).
fof(f16564,plain,
! [X0,X1] : top = join(join(complement(X0),X1),X0),
inference(forward_demodulation,[],[f16526,f12835]) ).
fof(f16568,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(X0)))) = X0,
inference(forward_demodulation,[],[f16520,f21]) ).
fof(f16617,plain,
! [X0,X1] : top = join(X0,join(complement(X0),X1)),
inference(forward_demodulation,[],[f16564,f21]) ).
fof(f16621,plain,
! [X0] : join(complement(top),complement(complement(X0))) = X0,
inference(forward_demodulation,[],[f16568,f12744]) ).
fof(f16656,plain,
! [X0] : join(zero,complement(complement(X0))) = X0,
inference(forward_demodulation,[],[f16621,f42]) ).
fof(f16716,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f12885,f16656]) ).
fof(f16781,plain,
! [X0] : complement(complement(X0)) = X0,
inference(superposition,[],[f16716,f16656]) ).
fof(f16783,plain,
! [X0] : zero = composition(X0,zero),
inference(superposition,[],[f16716,f13833]) ).
fof(f16921,plain,
converse(top) = converse(complement(converse(zero))),
inference(superposition,[],[f55,f16716]) ).
fof(f16946,plain,
top = converse(complement(converse(zero))),
inference(forward_demodulation,[],[f16921,f13109]) ).
fof(f17513,plain,
converse(top) = complement(converse(zero)),
inference(superposition,[],[f28,f16946]) ).
fof(f17544,plain,
top = complement(converse(zero)),
inference(forward_demodulation,[],[f17513,f13109]) ).
fof(f17616,plain,
complement(top) = converse(zero),
inference(superposition,[],[f16781,f17544]) ).
fof(f17617,plain,
zero = converse(zero),
inference(forward_demodulation,[],[f17616,f42]) ).
fof(f17689,plain,
! [X0] : converse(composition(zero,X0)) = composition(converse(X0),zero),
inference(superposition,[],[f51,f17617]) ).
fof(f17706,plain,
! [X0] : zero = converse(composition(zero,X0)),
inference(forward_demodulation,[],[f17689,f16783]) ).
fof(f17779,plain,
! [X0] : converse(zero) = composition(zero,X0),
inference(superposition,[],[f28,f17706]) ).
fof(f17812,plain,
! [X0] : zero = composition(zero,X0),
inference(forward_demodulation,[],[f17779,f17617]) ).
fof(f17974,plain,
! [X0,X1] : top = join(X1,join(X0,complement(X1))),
inference(superposition,[],[f16617,f21]) ).
fof(f18073,plain,
! [X0,X1] : join(complement(top),complement(join(complement(X0),complement(join(complement(complement(X0)),X1))))) = X0,
inference(superposition,[],[f15231,f16617]) ).
fof(f18149,plain,
! [X0,X1] : join(complement(top),complement(join(complement(X0),complement(join(X0,X1))))) = X0,
inference(forward_demodulation,[],[f18073,f16781]) ).
fof(f18214,plain,
! [X0,X1] : join(zero,complement(join(complement(X0),complement(join(X0,X1))))) = X0,
inference(forward_demodulation,[],[f18149,f42]) ).
fof(f18240,plain,
! [X0,X1] : complement(join(complement(X0),complement(join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f18214,f16716]) ).
fof(f18363,plain,
! [X0,X1] : join(complement(top),complement(join(complement(X0),complement(join(X1,complement(complement(X0))))))) = X0,
inference(superposition,[],[f15231,f17974]) ).
fof(f18436,plain,
! [X0,X1] : join(complement(top),complement(join(complement(X0),complement(join(X1,X0))))) = X0,
inference(forward_demodulation,[],[f18363,f16781]) ).
fof(f18500,plain,
! [X0,X1] : join(zero,complement(join(complement(X0),complement(join(X1,X0))))) = X0,
inference(forward_demodulation,[],[f18436,f42]) ).
fof(f18526,plain,
! [X0,X1] : complement(join(complement(X0),complement(join(X1,X0)))) = X0,
inference(forward_demodulation,[],[f18500,f16716]) ).
fof(f24968,plain,
! [X0,X1] : join(zero,complement(X0)) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f16656,f18240]) ).
fof(f24986,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f24968,f16716]) ).
fof(f26464,plain,
! [X0,X1] : join(zero,complement(X0)) = join(complement(X0),complement(join(X1,X0))),
inference(superposition,[],[f16656,f18526]) ).
fof(f26488,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f26464,f16716]) ).
fof(f44889,plain,
! [X0,X1] : complement(one) = join(complement(one),composition(converse(join(complement(X0),complement(join(X0,X1)))),X0)),
inference(superposition,[],[f12683,f18240]) ).
fof(f44977,plain,
! [X0] : complement(one) = join(complement(one),composition(converse(complement(X0)),X0)),
inference(forward_demodulation,[],[f44889,f24986]) ).
fof(f47380,plain,
! [X0] : join(top,complement(one)) = join(complement(composition(converse(complement(X0)),X0)),complement(one)),
inference(superposition,[],[f1227,f44977]) ).
fof(f47408,plain,
! [X0] : join(top,complement(one)) = join(complement(one),complement(composition(converse(complement(X0)),X0))),
inference(forward_demodulation,[],[f47380,f21]) ).
fof(f47441,plain,
! [X0] : top = join(complement(one),complement(composition(converse(complement(X0)),X0))),
inference(forward_demodulation,[],[f47408,f12835]) ).
fof(f49933,plain,
! [X0] : composition(complement(top),complement(join(complement(X0),complement(composition(converse(one),converse(complement(converse(X0)))))))) = join(complement(join(complement(composition(one,X0)),complement(converse(complement(converse(X0)))))),composition(complement(top),complement(join(complement(X0),complement(composition(converse(one),converse(complement(converse(X0))))))))),
inference(superposition,[],[f39,f47441]) ).
fof(f50022,plain,
! [X0] : composition(complement(top),complement(join(complement(X0),complement(converse(composition(complement(converse(X0)),one)))))) = join(complement(join(complement(composition(one,X0)),complement(converse(complement(converse(X0)))))),composition(complement(top),complement(join(complement(X0),complement(converse(composition(complement(converse(X0)),one))))))),
inference(forward_demodulation,[],[f49933,f30]) ).
fof(f50070,plain,
! [X0] : composition(complement(top),complement(join(complement(X0),complement(converse(complement(converse(X0))))))) = join(complement(join(complement(composition(one,X0)),complement(converse(complement(converse(X0)))))),composition(complement(top),complement(join(complement(X0),complement(converse(complement(converse(X0)))))))),
inference(forward_demodulation,[],[f50022,f26]) ).
fof(f50097,plain,
! [X0] : composition(zero,complement(join(complement(X0),complement(converse(complement(converse(X0))))))) = join(complement(join(complement(composition(one,X0)),complement(converse(complement(converse(X0)))))),composition(zero,complement(join(complement(X0),complement(converse(complement(converse(X0)))))))),
inference(forward_demodulation,[],[f50070,f42]) ).
fof(f50115,plain,
! [X0] : zero = join(complement(join(complement(composition(one,X0)),complement(converse(complement(converse(X0)))))),zero),
inference(forward_demodulation,[],[f50097,f17812]) ).
fof(f50127,plain,
! [X0] : zero = join(zero,complement(join(complement(composition(one,X0)),complement(converse(complement(converse(X0))))))),
inference(forward_demodulation,[],[f50115,f21]) ).
fof(f50136,plain,
! [X0] : zero = complement(join(complement(composition(one,X0)),complement(converse(complement(converse(X0)))))),
inference(forward_demodulation,[],[f50127,f16716]) ).
fof(f50143,plain,
! [X0] : zero = complement(join(complement(X0),complement(converse(complement(converse(X0)))))),
inference(forward_demodulation,[],[f50136,f235]) ).
fof(f52302,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(complement(converse(complement(converse(X0)))))))) = X0,
inference(superposition,[],[f15231,f50143]) ).
fof(f52499,plain,
! [X0] : complement(join(complement(X0),complement(complement(converse(complement(converse(X0))))))) = X0,
inference(forward_demodulation,[],[f52302,f16716]) ).
fof(f52591,plain,
! [X0] : complement(join(complement(X0),converse(complement(converse(X0))))) = X0,
inference(forward_demodulation,[],[f52499,f16781]) ).
fof(f53075,plain,
! [X0] : complement(X0) = join(complement(X0),converse(complement(converse(X0)))),
inference(superposition,[],[f16781,f52591]) ).
fof(f53903,plain,
! [X0] : join(X0,converse(complement(converse(complement(X0))))) = X0,
inference(superposition,[],[f53075,f16781]) ).
fof(f54184,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(converse(complement(converse(complement(converse(X0))))))),
inference(superposition,[],[f44,f53903]) ).
fof(f54228,plain,
! [X0] : converse(converse(X0)) = join(X0,complement(converse(complement(converse(X0))))),
inference(forward_demodulation,[],[f54184,f28]) ).
fof(f54304,plain,
! [X0] : join(X0,complement(converse(complement(converse(X0))))) = X0,
inference(forward_demodulation,[],[f54228,f28]) ).
fof(f54435,plain,
! [X0] : complement(complement(converse(complement(converse(X0))))) = join(complement(complement(converse(complement(converse(X0))))),complement(X0)),
inference(superposition,[],[f26488,f54304]) ).
fof(f54551,plain,
! [X0] : complement(complement(converse(complement(converse(X0))))) = join(complement(X0),complement(complement(converse(complement(converse(X0)))))),
inference(forward_demodulation,[],[f54435,f21]) ).
fof(f54623,plain,
! [X0] : converse(complement(converse(X0))) = join(complement(X0),converse(complement(converse(X0)))),
inference(forward_demodulation,[],[f54551,f16781]) ).
fof(f54648,plain,
! [X0] : complement(X0) = converse(complement(converse(X0))),
inference(forward_demodulation,[],[f54623,f53075]) ).
fof(f54688,plain,
! [X0] : converse(complement(X0)) = complement(converse(X0)),
inference(superposition,[],[f54648,f28]) ).
fof(f54980,plain,
complement(converse(sK0)) != complement(converse(sK0)),
inference(superposition,[],[f37,f54688]) ).
fof(f55037,plain,
$false,
inference(trivial_inequality_removal,[],[f54980]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL004+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n008.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 22:50:40 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 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
% 6.74/1.44 % (1691689)Will run a generic schedule for satisfiability detection.
% 6.74/1.44 % (1691695)% WARNING: option uhcvi not known.
% 6.74/1.44 % (1691695)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1078204228:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.74/1.44 % (1691694)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3180637325_2999 on theBenchmark for (2999ds/0Mi)
% 6.74/1.44 % (1691696)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3260611902:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.74/1.44 % (1691699)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3339788057:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.74/1.44 % (1691697)dis+10_1_sil=32000:sp=arity:random_seed=619045397:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.74/1.44 % (1691698)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=114866738:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.74/1.44 % (1691700)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1465039290:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.74/1.44 % TRYING [1]
% 6.74/1.44 % TRYING [2]
% 6.74/1.44 % TRYING [3]
% 6.74/1.44 % TRYING [4]
% 6.74/1.44 % (1691697)Instruction limit reached!
% 6.74/1.44 % (1691697)------------------------------
% 6.74/1.44 % (1691697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1691697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1691697)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1691697)Termination reason: Instruction limit
% 6.74/1.44 % (1691697)Termination phase: Saturation
% 6.74/1.44 % (1691697)Time elapsed: 0.060 s
% 6.74/1.44 % (1691697)Peak memory usage: 13 MB
% 6.74/1.44 % (1691697)Instructions burned: 104 (million)
% 6.74/1.44 % (1691698)Instruction limit reached!
% 6.74/1.44 % (1691698)------------------------------
% 6.74/1.44 % (1691698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1691698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1691698)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1691698)Termination reason: Instruction limit
% 6.74/1.44 % (1691698)Termination phase: Saturation
% 6.74/1.44 % (1691698)Time elapsed: 0.070 s
% 6.74/1.44 % (1691698)Peak memory usage: 13 MB
% 6.74/1.44 % (1691698)Instructions burned: 117 (million)
% 6.74/1.44 % (1691699)Instruction limit reached!
% 6.74/1.44 % (1691699)------------------------------
% 6.74/1.44 % (1691699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1691699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1691699)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1691699)Termination reason: Instruction limit
% 6.74/1.44 % (1691699)Termination phase: Saturation
% 6.74/1.44 % (1691699)Time elapsed: 0.080 s
% 6.74/1.44 % (1691699)Peak memory usage: 13 MB
% 6.74/1.44 % (1691699)Instructions burned: 137 (million)
% 6.74/1.44 % (1691708)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3215675375:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.74/1.44 % (1691709)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1008985200:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 6.74/1.44 % TRYING [1]
% 6.74/1.44 % TRYING [2]
% 6.74/1.44 % (1691700)Instruction limit reached!
% 6.74/1.44 % (1691700)------------------------------
% 6.74/1.44 % (1691700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1691700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1691700)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1691700)Termination reason: Instruction limit
% 6.74/1.44 % (1691700)Termination phase: Saturation
% 6.74/1.44 % (1691700)Time elapsed: 0.096 s
% 6.74/1.44 % (1691700)Peak memory usage: 13 MB
% 6.74/1.44 % (1691700)Instructions burned: 160 (million)
% 6.74/1.44 % TRYING [3]
% 6.74/1.44 % (1691710)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=2166415468:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.74/1.44 % (1691713)ott-21_1_sil=16000:fs=off:random_seed=7990370:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.74/1.44 % TRYING [4]
% 6.74/1.44 % (1691709)Instruction limit reached!
% 6.74/1.44 % (1691709)------------------------------
% 6.74/1.44 % (1691709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1691709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1691709)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1691709)Termination reason: Instruction limit
% 6.74/1.44 % (1691709)Termination phase: Saturation
% 6.74/1.44 % (1691709)Time elapsed: 0.084 s
% 6.74/1.44 % (1691709)Peak memory usage: 13 MB
% 6.74/1.44 % (1691709)Instructions burned: 132 (million)
% 6.74/1.44 % (1691716)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=361629749:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 6.74/1.44 % (1691713)Instruction limit reached!
% 6.74/1.44 % (1691713)------------------------------
% 6.74/1.44 % (1691713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1691713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1691713)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1691713)Termination reason: Instruction limit
% 6.74/1.44 % (1691713)Termination phase: Saturation
% 6.74/1.44 % (1691713)Time elapsed: 0.085 s
% 6.74/1.44 % (1691713)Peak memory usage: 12 MB
% 6.74/1.44 % (1691713)Instructions burned: 181 (million)
% 6.74/1.44 % TRYING [5]
% 6.74/1.44 % (1691718)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=731010672:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 6.74/1.44 % TRYING [1]
% 6.74/1.44 % TRYING [2]
% 6.74/1.44 % TRYING [3]
% 6.74/1.44 % TRYING [5]
% 6.74/1.44 % TRYING [4]
% 6.74/1.44 % (1691708)Instruction limit reached!
% 6.74/1.44 % (1691708)------------------------------
% 6.74/1.44 % (1691708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1691708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1691708)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1691708)Termination reason: Instruction limit
% 6.74/1.44 % (1691708)Termination phase: Finite model building constraint generation
% 6.74/1.44 % (1691708)Time elapsed: 0.282 s
% 6.74/1.44 % (1691708)Peak memory usage: 28 MB
% 6.74/1.44 % (1691708)Instructions burned: 717 (million)
% 6.74/1.44 % (1691720)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3375502552:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 6.74/1.44 % (1691710)Instruction limit reached!
% 6.74/1.44 % (1691710)------------------------------
% 6.74/1.44 % (1691710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1691710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1691710)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1691710)Termination reason: Instruction limit
% 6.74/1.44 % (1691710)Termination phase: Saturation
% 6.74/1.44 % (1691710)Time elapsed: 0.318 s
% 6.74/1.44 % (1691710)Peak memory usage: 16 MB
% 6.74/1.44 % (1691710)Instructions burned: 686 (million)
% 6.74/1.44 % (1691722)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2904860624:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 6.74/1.44 % (1691716)Instruction limit reached!
% 6.74/1.44 % (1691716)------------------------------
% 6.74/1.44 % (1691716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1691716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1691716)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1691716)Termination reason: Instruction limit
% 6.74/1.44 % (1691716)Termination phase: Saturation
% 6.74/1.44 % (1691716)Time elapsed: 0.257 s
% 6.74/1.44 % (1691716)Peak memory usage: 16 MB
% 6.74/1.44 % (1691716)Instructions burned: 477 (million)
% 6.74/1.44 % (1691724)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=724923222: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)
% 6.74/1.44 % (1691718)Instruction limit reached!
% 6.74/1.44 % (1691718)------------------------------
% 6.74/1.44 % (1691718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1691718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1691718)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1691718)Termination reason: Instruction limit
% 6.74/1.44 % (1691718)Termination phase: Finite model building SAT solving
% 6.74/1.44 % (1691718)Time elapsed: 0.306 s
% 6.74/1.44 % (1691718)Peak memory usage: 23 MB
% 6.74/1.44 % (1691718)Instructions burned: 865 (million)
% 6.74/1.44 % (1691726)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=546505422:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 6.74/1.44 % (1691722)Instruction limit reached!
% 6.74/1.44 % (1691722)------------------------------
% 6.74/1.44 % (1691722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1691722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1691722)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1691722)Termination reason: Instruction limit
% 6.74/1.44 % (1691722)Termination phase: Finite model building constraint generation
% 6.74/1.44 % (1691722)Time elapsed: 0.405 s
% 6.74/1.44 % (1691722)Peak memory usage: 106 MB
% 6.74/1.44 % (1691722)Instructions burned: 891 (million)
% 6.74/1.44 % (1691724)Instruction limit reached!
% 6.74/1.44 % (1691724)------------------------------
% 6.74/1.44 % (1691724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1691724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1691724)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1691724)Termination reason: Instruction limit
% 6.74/1.44 % (1691724)Termination phase: Saturation
% 6.74/1.44 % (1691724)Time elapsed: 0.393 s
% 6.74/1.44 % (1691724)Peak memory usage: 18 MB
% 6.74/1.44 % (1691724)Instructions burned: 693 (million)
% 6.74/1.44 % (1691728)fmb+10_1_sil=64000:random_seed=368197718:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 6.74/1.44 % TRYING [1]
% 6.74/1.44 % TRYING [2]
% 6.74/1.44 % (1691729)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1792893542:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 6.74/1.44 % TRYING [20]
% 6.74/1.44 % TRYING [3]
% 6.74/1.44 % TRYING [6]
% 6.74/1.44 % TRYING [4]
% 6.74/1.44 % (1691696) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1691689-1691696"...
% 6.74/1.44 % (1691696)...printing done.
% 6.74/1.44 % (1691696)Refutation found. Thanks to Tanya!
% 6.74/1.44 % SZS status Theorem for theBenchmark
% 6.74/1.44 % SZS output start Proof for theBenchmark
% See solution above
% 6.74/1.44 % (1691696)------------------------------
% 6.74/1.44 % (1691696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1691696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1691696)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1691696)Termination reason: Refutation
% 6.74/1.44 % (1691696)Time elapsed: 0.971 s
% 6.74/1.44 % (1691696)Peak memory usage: 26 MB
% 6.74/1.44 % (1691696)Instructions burned: 1932 (million)
% 6.74/1.44 % (1691689)Success in time 1.02 s
% 6.74/1.44 % Vampire exiting
%------------------------------------------------------------------------------