%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : REL047+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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 : Thu Sep 24 02:03:28 PM UTC 2026
% Result : Theorem 134.51s 17.40s
% Output : CNFRefutation 114.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 66
% Number of leaves : 14
% Syntax : Number of formulae : 219 ( 215 unt; 2 def)
% Number of atoms : 227 ( 226 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 13 ( 5 ~; 0 |; 6 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 8 con; 0-2 aty)
% Number of variables : 268 ( 265 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,conjecture,
! [X0,X1,X2] :
( ( join(X0,X2) = X2
& join(X0,X1) = X1 )
=> join(X0,meet(X1,X2)) = meet(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
~ ! [X0,X1,X2] :
( ( join(X0,X2) = X2
& join(X0,X1) = X1 )
=> join(X0,meet(X1,X2)) = meet(X1,X2) ),
inference(negated_conjecture,[status(cth)],[f14]) ).
fof(f16,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f17,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f18,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f19,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f20,plain,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f21,plain,
! [X0] : composition(X0,one) = X0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f23,plain,
! [X0] : converse(converse(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f25,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f26,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f27,plain,
! [X0] : top = join(X0,complement(X0)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f28,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f29,plain,
? [X0,X1,X2] :
( join(X0,meet(X1,X2)) != meet(X1,X2)
& join(X0,X2) = X2
& join(X0,X1) = X1 ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f30,plain,
( join(sK0_skl,meet(sK1_skl,sK2_skl)) != meet(sK1_skl,sK2_skl)
& join(sK0_skl,sK2_skl) = sK2_skl
& join(sK0_skl,sK1_skl) = sK1_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl),skolemize(X2,sK2_skl)],[f29]) ).
fof(f31,plain,
join(sK0_skl,sK1_skl) = sK1_skl,
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f32,plain,
join(sK0_skl,sK2_skl) = sK2_skl,
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f33,plain,
join(sK0_skl,meet(sK1_skl,sK2_skl)) != meet(sK1_skl,sK2_skl),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f34,definition,
sF1_fnc = meet(sK1_skl,sK2_skl),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f35,definition,
sF0_fnc = join(sK0_skl,sF1_fnc),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f36,plain,
sF0_fnc != sF1_fnc,
inference(definition_folding,[],[f33,f35,f34]) ).
fof(f37,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[status(thm)],[f16,f18]) ).
fof(f38,plain,
! [X0,X1] : join(complement(X0),composition(converse(X1),complement(composition(X1,X0)))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f16,f26]) ).
fof(f39,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),X1)),meet(X0,X1)),
inference(backward_demodulation,[status(thm)],[f19,f37]) ).
fof(f40,plain,
! [X0,X1] : X0 = join(meet(X0,X1),complement(join(complement(X0),X1))),
inference(forward_demodulation,[status(thm)],[f16,f39]) ).
fof(f47,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(paramodulation,[status(thm)],[f23,f25]) ).
fof(f48,plain,
! [X0] : meet(X0,complement(X0)) = complement(top),
inference(paramodulation,[status(thm)],[f27,f19]) ).
fof(f49,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X1),complement(X0))),
inference(paramodulation,[status(thm)],[f16,f19]) ).
fof(f51,plain,
! [X0,X1,X2] : meet(join(complement(X0),complement(X1)),X2) = complement(join(meet(X0,X1),complement(X2))),
inference(paramodulation,[status(thm)],[f19,f19]) ).
fof(f52,plain,
! [X0,X1,X2] : meet(X0,join(complement(X1),complement(X2))) = complement(join(complement(X0),meet(X1,X2))),
inference(paramodulation,[status(thm)],[f19,f19]) ).
fof(f55,plain,
zero = complement(top),
inference(forward_demodulation,[status(thm)],[f28,f48]) ).
fof(f57,plain,
! [X0] : meet(X0,top) = complement(join(complement(X0),zero)),
inference(paramodulation,[status(thm)],[f55,f19]) ).
fof(f58,plain,
! [X0] : meet(top,X0) = complement(join(zero,complement(X0))),
inference(paramodulation,[status(thm)],[f55,f19]) ).
fof(f62,plain,
! [X0] : meet(X0,top) = complement(join(zero,complement(X0))),
inference(forward_demodulation,[status(thm)],[f16,f57]) ).
fof(f74,plain,
! [X0,X1] : composition(X0,composition(one,X1)) = composition(X0,X1),
inference(paramodulation,[status(thm)],[f21,f20]) ).
fof(f190,plain,
! [X0] : join(sK0_skl,join(sK2_skl,X0)) = join(sK2_skl,X0),
inference(paramodulation,[status(thm)],[f32,f17]) ).
fof(f191,plain,
! [X0] : join(sK0_skl,join(sF1_fnc,X0)) = join(sF0_fnc,X0),
inference(paramodulation,[status(thm)],[f35,f17]) ).
fof(f192,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(paramodulation,[status(thm)],[f27,f17]) ).
fof(f194,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X1,X0),X2),
inference(paramodulation,[status(thm)],[f16,f17]) ).
fof(f197,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(paramodulation,[status(thm)],[f17,f16]) ).
fof(f206,plain,
join(sK0_skl,top) = join(sK2_skl,complement(sK2_skl)),
inference(paramodulation,[status(thm)],[f27,f190]) ).
fof(f208,plain,
! [X0] : join(sK0_skl,join(X0,sK2_skl)) = join(sK2_skl,X0),
inference(paramodulation,[status(thm)],[f16,f190]) ).
fof(f212,plain,
join(sK0_skl,top) = top,
inference(forward_demodulation,[status(thm)],[f27,f206]) ).
fof(f220,plain,
! [X0] : join(sK0_skl,join(top,X0)) = join(top,X0),
inference(paramodulation,[status(thm)],[f212,f17]) ).
fof(f232,plain,
! [X0,X1] : X0 = join(meet(X0,complement(X1)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f19,f40]) ).
fof(f234,plain,
! [X0] : X0 = join(meet(X0,complement(complement(X0))),complement(top)),
inference(paramodulation,[status(thm)],[f27,f40]) ).
fof(f244,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f16,f232]) ).
fof(f249,plain,
! [X0] : X0 = join(complement(top),meet(X0,complement(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f16,f234]) ).
fof(f250,plain,
! [X0] : X0 = join(zero,meet(X0,complement(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f55,f249]) ).
fof(f254,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(paramodulation,[status(thm)],[f19,f49]) ).
fof(f269,plain,
! [X0,X1] : X0 = join(meet(X0,complement(X1)),meet(X1,X0)),
inference(paramodulation,[status(thm)],[f49,f40]) ).
fof(f292,plain,
! [X0,X1] : X0 = join(meet(X1,X0),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f16,f269]) ).
fof(f322,plain,
! [X0,X1,X2,X3] : meet(join(complement(X0),complement(X1)),join(complement(X2),complement(X3))) = complement(join(meet(X0,X1),meet(X2,X3))),
inference(paramodulation,[status(thm)],[f19,f51]) ).
fof(f360,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(zero,meet(join(complement(X0),complement(X1)),complement(meet(X0,X1)))),
inference(paramodulation,[status(thm)],[f19,f250]) ).
fof(f362,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(zero,meet(complement(meet(X0,X1)),join(complement(X0),complement(X1)))),
inference(forward_demodulation,[status(thm)],[f254,f360]) ).
fof(f366,plain,
sK1_skl = join(sF1_fnc,meet(sK1_skl,complement(sK2_skl))),
inference(paramodulation,[status(thm)],[f34,f244]) ).
fof(f389,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f21,f47]) ).
fof(f408,plain,
! [X0] : X0 = composition(converse(one),X0),
inference(forward_demodulation,[status(thm)],[f23,f389]) ).
fof(f413,plain,
! [X0] : composition(one,X0) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f74,f408]) ).
fof(f415,plain,
! [X0] : join(complement(X0),complement(composition(one,X0))) = complement(X0),
inference(paramodulation,[status(thm)],[f408,f38]) ).
fof(f427,plain,
! [X0] : composition(one,X0) = X0,
inference(forward_demodulation,[status(thm)],[f408,f413]) ).
fof(f428,plain,
! [X0] : join(complement(X0),complement(X0)) = complement(X0),
inference(forward_demodulation,[status(thm)],[f427,f415]) ).
fof(f458,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),meet(X0,X1)) = complement(join(complement(X0),complement(X1))),
inference(paramodulation,[status(thm)],[f19,f428]) ).
fof(f459,plain,
! [X0] : meet(X0,X0) = complement(complement(X0)),
inference(paramodulation,[status(thm)],[f428,f49]) ).
fof(f461,plain,
! [X0] : X0 = join(meet(X0,complement(X0)),complement(complement(X0))),
inference(paramodulation,[status(thm)],[f428,f40]) ).
fof(f463,plain,
! [X0,X1] : join(meet(X0,X1),complement(join(complement(X0),complement(X1)))) = complement(join(complement(X0),complement(X1))),
inference(forward_demodulation,[status(thm)],[f16,f458]) ).
fof(f464,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,X0)) = complement(join(complement(X0),complement(X1))),
inference(forward_demodulation,[status(thm)],[f49,f463]) ).
fof(f465,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,X0)) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f49,f464]) ).
fof(f491,plain,
! [X0] : X0 = join(complement(complement(X0)),meet(X0,complement(X0))),
inference(forward_demodulation,[status(thm)],[f16,f461]) ).
fof(f492,plain,
! [X0] : X0 = join(complement(complement(X0)),zero),
inference(forward_demodulation,[status(thm)],[f28,f491]) ).
fof(f493,plain,
! [X0] : X0 = join(zero,complement(complement(X0))),
inference(forward_demodulation,[status(thm)],[f16,f492]) ).
fof(f553,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(zero,complement(meet(X1,X0))),
inference(paramodulation,[status(thm)],[f49,f493]) ).
fof(f555,plain,
! [X0] : meet(complement(X0),top) = complement(X0),
inference(paramodulation,[status(thm)],[f493,f62]) ).
fof(f558,plain,
! [X0] : meet(top,complement(X0)) = complement(X0),
inference(forward_demodulation,[status(thm)],[f254,f555]) ).
fof(f565,plain,
! [X0] : join(sK0_skl,join(X0,top)) = join(top,X0),
inference(paramodulation,[status(thm)],[f16,f220]) ).
fof(f575,plain,
! [X0,X1] : meet(top,meet(X0,X1)) = complement(join(complement(X0),complement(X1))),
inference(paramodulation,[status(thm)],[f19,f558]) ).
fof(f581,plain,
! [X0] : top = join(complement(X0),complement(join(complement(top),complement(X0)))),
inference(paramodulation,[status(thm)],[f558,f40]) ).
fof(f588,plain,
! [X0,X1] : meet(top,meet(X0,X1)) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f49,f575]) ).
fof(f590,plain,
! [X0] : top = join(complement(X0),meet(X0,top)),
inference(forward_demodulation,[status(thm)],[f49,f581]) ).
fof(f596,plain,
join(sK0_skl,sK1_skl) = join(sF0_fnc,meet(sK1_skl,complement(sK2_skl))),
inference(paramodulation,[status(thm)],[f366,f191]) ).
fof(f598,plain,
sK1_skl = join(sF0_fnc,meet(sK1_skl,complement(sK2_skl))),
inference(forward_demodulation,[status(thm)],[f31,f596]) ).
fof(f715,plain,
! [X0] : join(meet(X0,X0),complement(complement(X0))) = complement(complement(X0)),
inference(paramodulation,[status(thm)],[f459,f428]) ).
fof(f726,plain,
! [X0] : top = join(complement(X0),meet(X0,X0)),
inference(paramodulation,[status(thm)],[f459,f27]) ).
fof(f761,plain,
! [X0,X1] : join(complement(X0),join(meet(X0,X0),X1)) = join(top,X1),
inference(paramodulation,[status(thm)],[f726,f17]) ).
fof(f817,plain,
join(sF0_fnc,sK2_skl) = join(sK2_skl,sF1_fnc),
inference(paramodulation,[status(thm)],[f191,f208]) ).
fof(f829,plain,
join(sK2_skl,sF0_fnc) = join(sK2_skl,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f16,f817]) ).
fof(f939,plain,
! [X0] : meet(X0,join(complement(X0),complement(top))) = complement(top),
inference(paramodulation,[status(thm)],[f590,f52]) ).
fof(f947,plain,
! [X0] : meet(X0,join(complement(X0),zero)) = complement(top),
inference(forward_demodulation,[status(thm)],[f55,f939]) ).
fof(f948,plain,
! [X0] : meet(X0,join(zero,complement(X0))) = complement(top),
inference(forward_demodulation,[status(thm)],[f16,f947]) ).
fof(f949,plain,
! [X0] : meet(X0,join(zero,complement(X0))) = zero,
inference(forward_demodulation,[status(thm)],[f55,f948]) ).
fof(f974,plain,
! [X0] : X0 = join(zero,complement(join(complement(X0),join(zero,complement(X0))))),
inference(paramodulation,[status(thm)],[f949,f40]) ).
fof(f982,plain,
! [X0] : X0 = join(zero,complement(join(zero,join(complement(X0),complement(X0))))),
inference(forward_demodulation,[status(thm)],[f197,f974]) ).
fof(f983,plain,
! [X0] : X0 = join(zero,complement(join(zero,complement(X0)))),
inference(forward_demodulation,[status(thm)],[f428,f982]) ).
fof(f986,plain,
! [X0] : X0 = join(zero,meet(X0,top)),
inference(forward_demodulation,[status(thm)],[f62,f983]) ).
fof(f1003,plain,
! [X0] : X0 = join(zero,meet(top,X0)),
inference(paramodulation,[status(thm)],[f254,f986]) ).
fof(f1011,plain,
! [X0,X1] : meet(X0,X1) = join(zero,meet(X1,X0)),
inference(paramodulation,[status(thm)],[f588,f1003]) ).
fof(f1012,plain,
! [X0] : complement(X0) = join(zero,complement(X0)),
inference(paramodulation,[status(thm)],[f558,f1003]) ).
fof(f1028,plain,
! [X0] : X0 = complement(complement(X0)),
inference(backward_demodulation,[status(thm)],[f1012,f493]) ).
fof(f1030,plain,
! [X0] : meet(X0,top) = complement(complement(X0)),
inference(backward_demodulation,[status(thm)],[f1012,f62]) ).
fof(f1033,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = complement(meet(X1,X0)),
inference(backward_demodulation,[status(thm)],[f1012,f553]) ).
fof(f1044,plain,
! [X0] : meet(top,X0) = complement(complement(X0)),
inference(backward_demodulation,[status(thm)],[f1012,f58]) ).
fof(f1086,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(zero,meet(complement(meet(X0,X1)),complement(meet(X1,X0)))),
inference(backward_demodulation,[status(thm)],[f1033,f362]) ).
fof(f1094,plain,
! [X0,X1,X2,X3] : meet(join(complement(X0),complement(X1)),complement(meet(X2,X3))) = complement(join(meet(X0,X1),meet(X3,X2))),
inference(backward_demodulation,[status(thm)],[f1033,f322]) ).
fof(f1119,plain,
! [X0] : join(meet(X0,X0),complement(complement(X0))) = meet(X0,top),
inference(backward_demodulation,[status(thm)],[f1030,f715]) ).
fof(f1131,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(zero,meet(complement(meet(X1,X0)),complement(meet(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f1033,f1086]) ).
fof(f1134,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(zero,complement(join(meet(X0,X1),meet(X1,X0)))),
inference(backward_demodulation,[status(thm)],[f1135,f1131]) ).
fof(f1135,plain,
! [X0,X1,X2,X3] : meet(complement(meet(X0,X1)),complement(meet(X2,X3))) = complement(join(meet(X1,X0),meet(X3,X2))),
inference(forward_demodulation,[status(thm)],[f1033,f1094]) ).
fof(f1139,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(join(meet(X0,X1),meet(X1,X0))),
inference(forward_demodulation,[status(thm)],[f1012,f1134]) ).
fof(f1140,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f465,f1139]) ).
fof(f1147,plain,
! [X0] : join(meet(X0,X0),meet(top,X0)) = meet(X0,top),
inference(forward_demodulation,[status(thm)],[f1044,f1119]) ).
fof(f1149,plain,
! [X0] : meet(X0,X0) = X0,
inference(backward_demodulation,[status(thm)],[f1028,f459]) ).
fof(f1151,plain,
! [X0] : meet(X0,top) = X0,
inference(backward_demodulation,[status(thm)],[f1028,f1030]) ).
fof(f1173,plain,
! [X0] : X0 = meet(top,X0),
inference(backward_demodulation,[status(thm)],[f1011,f986]) ).
fof(f1193,plain,
! [X0] : join(meet(X0,X0),X0) = meet(X0,top),
inference(backward_demodulation,[status(thm)],[f1173,f1147]) ).
fof(f1207,plain,
! [X0,X1] : join(complement(X0),join(X0,X1)) = join(top,X1),
inference(backward_demodulation,[status(thm)],[f1149,f761]) ).
fof(f1221,plain,
! [X0,X1] : join(X0,join(X1,complement(X0))) = join(top,X1),
inference(forward_demodulation,[status(thm)],[f197,f1207]) ).
fof(f1244,plain,
! [X0] : join(X0,meet(X0,X0)) = meet(X0,top),
inference(forward_demodulation,[status(thm)],[f16,f1193]) ).
fof(f1245,plain,
! [X0] : join(X0,X0) = meet(X0,top),
inference(forward_demodulation,[status(thm)],[f1149,f1244]) ).
fof(f1250,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[status(thm)],[f1151,f1245]) ).
fof(f1292,plain,
! [X0] : X0 = join(X0,complement(join(complement(X0),X0))),
inference(paramodulation,[status(thm)],[f1149,f40]) ).
fof(f1293,plain,
! [X0] : X0 = join(X0,complement(join(X0,complement(X0)))),
inference(forward_demodulation,[status(thm)],[f16,f1292]) ).
fof(f1294,plain,
! [X0] : X0 = join(X0,complement(top)),
inference(forward_demodulation,[status(thm)],[f27,f1293]) ).
fof(f1295,plain,
! [X0] : X0 = join(X0,zero),
inference(forward_demodulation,[status(thm)],[f55,f1294]) ).
fof(f1360,plain,
join(sK0_skl,sF1_fnc) = join(sF0_fnc,sF1_fnc),
inference(paramodulation,[status(thm)],[f1250,f191]) ).
fof(f1371,plain,
! [X0,X1] : join(X0,join(X0,X1)) = join(X0,X1),
inference(paramodulation,[status(thm)],[f1250,f17]) ).
fof(f1384,plain,
sF0_fnc = join(sF0_fnc,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f35,f1360]) ).
fof(f1385,plain,
sF0_fnc = join(sF1_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f16,f1384]) ).
fof(f1434,plain,
! [X0] : X0 = join(zero,X0),
inference(paramodulation,[status(thm)],[f1295,f16]) ).
fof(f1466,plain,
! [X0] : join(sF1_fnc,join(sF0_fnc,X0)) = join(sF0_fnc,X0),
inference(paramodulation,[status(thm)],[f1385,f17]) ).
fof(f1582,plain,
join(sF1_fnc,top) = join(sF0_fnc,complement(sF0_fnc)),
inference(paramodulation,[status(thm)],[f27,f1466]) ).
fof(f1588,plain,
join(top,sF1_fnc) = join(sF0_fnc,complement(sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f16,f1582]) ).
fof(f1589,plain,
join(top,sF1_fnc) = top,
inference(forward_demodulation,[status(thm)],[f27,f1588]) ).
fof(f1696,plain,
! [X0,X1] : X0 = join(meet(X1,X0),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f254,f292]) ).
fof(f1872,plain,
join(sF0_fnc,top) = join(top,sF1_fnc),
inference(paramodulation,[status(thm)],[f191,f565]) ).
fof(f1876,plain,
! [X0,X1] : join(sK0_skl,join(X0,join(X1,top))) = join(top,join(X0,X1)),
inference(paramodulation,[status(thm)],[f17,f565]) ).
fof(f1886,plain,
join(top,sF0_fnc) = join(top,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f16,f1872]) ).
fof(f1887,plain,
join(top,sF0_fnc) = top,
inference(forward_demodulation,[status(thm)],[f1589,f1886]) ).
fof(f1898,plain,
! [X0] : join(top,join(sF0_fnc,X0)) = join(top,X0),
inference(paramodulation,[status(thm)],[f1887,f17]) ).
fof(f2613,plain,
! [X0] : join(X0,top) = join(top,complement(complement(X0))),
inference(paramodulation,[status(thm)],[f27,f192]) ).
fof(f2614,plain,
! [X0] : join(X0,complement(X0)) = join(top,complement(X0)),
inference(paramodulation,[status(thm)],[f1250,f192]) ).
fof(f2634,plain,
! [X0,X1] : X0 = join(meet(X0,join(complement(complement(X0)),X1)),complement(join(top,X1))),
inference(paramodulation,[status(thm)],[f192,f40]) ).
fof(f2648,plain,
! [X0,X1] : X0 = join(complement(join(top,X1)),meet(X0,join(complement(complement(X0)),X1))),
inference(forward_demodulation,[status(thm)],[f16,f2634]) ).
fof(f2649,plain,
! [X0,X1] : X0 = join(complement(join(top,X1)),meet(X0,join(X0,X1))),
inference(forward_demodulation,[status(thm)],[f1028,f2648]) ).
fof(f2681,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[status(thm)],[f27,f2614]) ).
fof(f2718,plain,
! [X0,X1] : join(sK0_skl,join(X0,top)) = join(top,join(X0,X1)),
inference(backward_demodulation,[status(thm)],[f2719,f1876]) ).
fof(f2719,plain,
! [X0] : join(X0,top) = top,
inference(forward_demodulation,[status(thm)],[f2681,f2613]) ).
fof(f2723,plain,
! [X0] : join(top,sF0_fnc) = join(top,X0),
inference(backward_demodulation,[status(thm)],[f2728,f1898]) ).
fof(f2728,plain,
! [X0,X1] : join(top,X0) = join(top,join(X0,X1)),
inference(forward_demodulation,[status(thm)],[f565,f2718]) ).
fof(f2751,plain,
! [X0,X1] : X0 = join(complement(top),meet(X0,join(X0,X1))),
inference(backward_demodulation,[status(thm)],[f2757,f2649]) ).
fof(f2755,plain,
! [X0,X1] : join(X0,join(X1,complement(X0))) = top,
inference(backward_demodulation,[status(thm)],[f2757,f1221]) ).
fof(f2757,plain,
! [X0] : top = join(top,X0),
inference(forward_demodulation,[status(thm)],[f1887,f2723]) ).
fof(f2759,plain,
! [X0,X1] : X0 = join(zero,meet(X0,join(X0,X1))),
inference(forward_demodulation,[status(thm)],[f55,f2751]) ).
fof(f2760,plain,
! [X0,X1] : X0 = meet(X0,join(X0,X1)),
inference(forward_demodulation,[status(thm)],[f1434,f2759]) ).
fof(f3118,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X1),
inference(paramodulation,[status(thm)],[f1696,f2760]) ).
fof(f3148,plain,
! [X0,X1] : X0 = meet(X0,join(X1,X0)),
inference(paramodulation,[status(thm)],[f16,f2760]) ).
fof(f3171,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f254,f3118]) ).
fof(f3543,plain,
meet(sK1_skl,sK2_skl) = meet(sK2_skl,sF1_fnc),
inference(paramodulation,[status(thm)],[f34,f3171]) ).
fof(f3576,plain,
sF1_fnc = meet(sK2_skl,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f34,f3543]) ).
fof(f3666,plain,
sF0_fnc = meet(sF0_fnc,join(sK2_skl,sF1_fnc)),
inference(paramodulation,[status(thm)],[f829,f3148]) ).
fof(f4336,plain,
! [X0,X1] : join(meet(X0,X1),X1) = join(meet(X0,X1),meet(complement(X0),X1)),
inference(paramodulation,[status(thm)],[f1696,f1371]) ).
fof(f4339,plain,
! [X0,X1] : join(meet(X0,X1),X0) = join(meet(X0,X1),meet(X0,complement(X1))),
inference(paramodulation,[status(thm)],[f244,f1371]) ).
fof(f4426,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = join(meet(X0,X1),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f16,f4339]) ).
fof(f4452,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
inference(forward_demodulation,[status(thm)],[f244,f4426]) ).
fof(f4478,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = join(meet(X1,X0),meet(complement(X1),X0)),
inference(forward_demodulation,[status(thm)],[f16,f4336]) ).
fof(f4483,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = X0,
inference(forward_demodulation,[status(thm)],[f1696,f4478]) ).
fof(f4526,plain,
join(sK2_skl,sF1_fnc) = sK2_skl,
inference(paramodulation,[status(thm)],[f3576,f4452]) ).
fof(f4594,plain,
sF0_fnc = meet(sF0_fnc,sK2_skl),
inference(backward_demodulation,[status(thm)],[f4526,f3666]) ).
fof(f4599,plain,
sF0_fnc = meet(sK2_skl,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f254,f4594]) ).
fof(f6286,plain,
! [X0,X1,X2] : join(meet(X0,X1),join(X1,X2)) = join(X1,X2),
inference(paramodulation,[status(thm)],[f4483,f194]) ).
fof(f6432,plain,
! [X0,X1,X2] : join(X0,join(X1,meet(X2,X0))) = join(X0,X1),
inference(forward_demodulation,[status(thm)],[f197,f6286]) ).
fof(f9556,plain,
! [X0,X1] : join(X0,complement(X1)) = complement(meet(X1,complement(X0))),
inference(paramodulation,[status(thm)],[f1028,f1033]) ).
fof(f9561,plain,
! [X0,X1] : join(complement(X0),X1) = complement(meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f1028,f1033]) ).
fof(f9583,plain,
! [X0,X1] : join(X0,complement(meet(X0,X1))) = top,
inference(paramodulation,[status(thm)],[f1033,f2755]) ).
fof(f9904,plain,
! [X0,X1] : top = complement(meet(meet(complement(X0),X1),X0)),
inference(paramodulation,[status(thm)],[f9583,f1033]) ).
fof(f9933,plain,
! [X0,X1] : top = complement(meet(X0,meet(complement(X0),X1))),
inference(forward_demodulation,[status(thm)],[f1140,f9904]) ).
fof(f11763,plain,
! [X0,X1] : meet(X0,meet(complement(X0),X1)) = complement(top),
inference(paramodulation,[status(thm)],[f9933,f1028]) ).
fof(f11791,plain,
! [X0,X1] : meet(X0,meet(complement(X0),X1)) = zero,
inference(forward_demodulation,[status(thm)],[f55,f11763]) ).
fof(f12142,plain,
! [X0,X1] : meet(complement(X0),meet(X0,X1)) = zero,
inference(paramodulation,[status(thm)],[f1028,f11791]) ).
fof(f12358,plain,
meet(complement(sK2_skl),sF0_fnc) = zero,
inference(paramodulation,[status(thm)],[f4599,f12142]) ).
fof(f12359,plain,
meet(complement(sK2_skl),sF1_fnc) = zero,
inference(paramodulation,[status(thm)],[f3576,f12142]) ).
fof(f12483,plain,
meet(sF1_fnc,complement(sK2_skl)) = zero,
inference(forward_demodulation,[status(thm)],[f254,f12359]) ).
fof(f12494,plain,
meet(sF0_fnc,complement(sK2_skl)) = zero,
inference(forward_demodulation,[status(thm)],[f254,f12358]) ).
fof(f12578,plain,
complement(sK2_skl) = join(zero,meet(complement(sK2_skl),complement(sF0_fnc))),
inference(paramodulation,[status(thm)],[f12494,f292]) ).
fof(f12582,plain,
complement(sK2_skl) = meet(complement(sK2_skl),complement(sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f1434,f12578]) ).
fof(f12891,plain,
complement(sK2_skl) = join(zero,meet(complement(sF1_fnc),complement(sK2_skl))),
inference(paramodulation,[status(thm)],[f12483,f1696]) ).
fof(f12907,plain,
complement(sK2_skl) = meet(complement(sF1_fnc),complement(sK2_skl)),
inference(forward_demodulation,[status(thm)],[f1434,f12891]) ).
fof(f12908,plain,
complement(sK2_skl) = meet(complement(sK2_skl),complement(sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f254,f12907]) ).
fof(f50559,plain,
join(complement(sK2_skl),sK1_skl) = join(complement(sK2_skl),sF1_fnc),
inference(paramodulation,[status(thm)],[f366,f6432]) ).
fof(f50562,plain,
join(complement(sK2_skl),sK1_skl) = join(complement(sK2_skl),sF0_fnc),
inference(paramodulation,[status(thm)],[f598,f6432]) ).
fof(f51050,plain,
join(sK1_skl,complement(sK2_skl)) = join(complement(sK2_skl),sF1_fnc),
inference(forward_demodulation,[status(thm)],[f16,f50559]) ).
fof(f51051,plain,
join(sK1_skl,complement(sK2_skl)) = join(sF1_fnc,complement(sK2_skl)),
inference(forward_demodulation,[status(thm)],[f16,f51050]) ).
fof(f51166,plain,
join(sK1_skl,complement(sK2_skl)) = join(complement(sK2_skl),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f16,f50562]) ).
fof(f51167,plain,
join(sK1_skl,complement(sK2_skl)) = join(sF0_fnc,complement(sK2_skl)),
inference(forward_demodulation,[status(thm)],[f16,f51166]) ).
fof(f55612,plain,
! [X0,X1,X2] : join(complement(X0),meet(X1,complement(X2))) = complement(meet(join(X2,complement(X1)),X0)),
inference(paramodulation,[status(thm)],[f9556,f9561]) ).
fof(f59158,plain,
complement(sF0_fnc) = join(meet(sK2_skl,complement(sF0_fnc)),complement(sK2_skl)),
inference(paramodulation,[status(thm)],[f12582,f1696]) ).
fof(f59270,plain,
complement(sF0_fnc) = join(complement(sK2_skl),meet(sK2_skl,complement(sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f16,f59158]) ).
fof(f59271,plain,
complement(sF0_fnc) = complement(meet(join(sF0_fnc,complement(sK2_skl)),sK2_skl)),
inference(forward_demodulation,[status(thm)],[f55612,f59270]) ).
fof(f59272,plain,
complement(sF0_fnc) = complement(meet(sK2_skl,join(sF0_fnc,complement(sK2_skl)))),
inference(forward_demodulation,[status(thm)],[f1140,f59271]) ).
fof(f59273,plain,
complement(sF0_fnc) = complement(meet(sK2_skl,join(sK1_skl,complement(sK2_skl)))),
inference(forward_demodulation,[status(thm)],[f51167,f59272]) ).
fof(f59490,plain,
complement(sF1_fnc) = join(meet(sK2_skl,complement(sF1_fnc)),complement(sK2_skl)),
inference(paramodulation,[status(thm)],[f12908,f1696]) ).
fof(f59556,plain,
complement(sF1_fnc) = join(complement(sK2_skl),meet(sK2_skl,complement(sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f16,f59490]) ).
fof(f59557,plain,
complement(sF1_fnc) = complement(meet(join(sF1_fnc,complement(sK2_skl)),sK2_skl)),
inference(forward_demodulation,[status(thm)],[f55612,f59556]) ).
fof(f59558,plain,
complement(sF1_fnc) = complement(meet(sK2_skl,join(sF1_fnc,complement(sK2_skl)))),
inference(forward_demodulation,[status(thm)],[f1140,f59557]) ).
fof(f59559,plain,
complement(sF0_fnc) = complement(sF1_fnc),
inference(backward_demodulation,[status(thm)],[f59560,f59273]) ).
fof(f59560,plain,
complement(sF1_fnc) = complement(meet(sK2_skl,join(sK1_skl,complement(sK2_skl)))),
inference(forward_demodulation,[status(thm)],[f51051,f59558]) ).
fof(f59706,plain,
sF0_fnc = complement(complement(sF1_fnc)),
inference(paramodulation,[status(thm)],[f59559,f1028]) ).
fof(f59715,plain,
sF0_fnc = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f1028,f59706]) ).
fof(f59716,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f59715,f36]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL047+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n012.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 04:08:36 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Drodi V4.1.1
% 134.51/17.40 % Refutation found
% 134.51/17.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 134.51/17.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.70/17.53 % Elapsed time: 17.168839 seconds
% 12.70/17.53 % CPU time: 135.982470 seconds
% 12.70/17.53 % Total memory used: 632.853 MB
% 12.70/17.53 % Net memory used: 607.342 MB
%------------------------------------------------------------------------------