%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : REL006+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 : n014.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:11 PM UTC 2026
% Result : Theorem 7.44s 1.39s
% Output : CNFRefutation 7.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 12
% Syntax : Number of formulae : 135 ( 131 unt; 0 def)
% Number of atoms : 139 ( 138 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 8 ( 4 ~; 0 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 173 ( 171 !; 2 ?)
% 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(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(f9,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
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] :
( meet(converse(X0),X1) = zero
=> meet(X0,converse(X1)) = zero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
~ ! [X0,X1] :
( meet(converse(X0),X1) = zero
=> meet(X0,converse(X1)) = zero ),
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(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(f24,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[status(thm)],[f9]) ).
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] :
( meet(X0,converse(X1)) != zero
& meet(converse(X0),X1) = zero ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f30,plain,
( meet(sK0_skl,converse(sK1_skl)) != zero
& meet(converse(sK0_skl),sK1_skl) = zero ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl)],[f29]) ).
fof(f31,plain,
meet(converse(sK0_skl),sK1_skl) = zero,
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f32,plain,
meet(sK0_skl,converse(sK1_skl)) != zero,
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f36,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[status(thm)],[f16,f18]) ).
fof(f37,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),X1)),meet(X0,X1)),
inference(backward_demodulation,[status(thm)],[f19,f36]) ).
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(meet(X0,X1),complement(join(complement(X0),X1))),
inference(forward_demodulation,[status(thm)],[f16,f37]) ).
fof(f41,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(f43,plain,
! [X0,X1] : zero = meet(join(complement(X0),complement(X1)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f19,f28]) ).
fof(f44,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(paramodulation,[status(thm)],[f23,f24]) ).
fof(f45,plain,
! [X0,X1] : converse(join(X0,converse(X1))) = join(converse(X0),X1),
inference(paramodulation,[status(thm)],[f23,f24]) ).
fof(f47,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(paramodulation,[status(thm)],[f23,f25]) ).
fof(f101,plain,
! [X0] : X0 = join(zero,complement(join(complement(X0),complement(X0)))),
inference(paramodulation,[status(thm)],[f28,f39]) ).
fof(f102,plain,
! [X0,X1] : X0 = join(meet(X0,complement(X1)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f19,f39]) ).
fof(f105,plain,
! [X0] : X0 = join(zero,meet(X0,X0)),
inference(forward_demodulation,[status(thm)],[f19,f101]) ).
fof(f106,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f16,f102]) ).
fof(f108,plain,
converse(sK0_skl) = join(zero,meet(converse(sK0_skl),complement(sK1_skl))),
inference(paramodulation,[status(thm)],[f31,f106]) ).
fof(f109,plain,
! [X0] : X0 = join(zero,meet(X0,complement(complement(X0)))),
inference(paramodulation,[status(thm)],[f28,f106]) ).
fof(f206,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f21,f47]) ).
fof(f208,plain,
! [X0] : X0 = composition(converse(one),X0),
inference(forward_demodulation,[status(thm)],[f23,f206]) ).
fof(f210,plain,
! [X0,X1] : top = join(join(complement(X0),complement(X1)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f19,f27]) ).
fof(f211,plain,
! [X0,X1] : meet(join(complement(X0),complement(X1)),meet(X0,X1)) = complement(top),
inference(paramodulation,[status(thm)],[f27,f41]) ).
fof(f217,plain,
! [X0,X1] : top = join(complement(X0),join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f17,f210]) ).
fof(f218,plain,
zero = complement(top),
inference(forward_demodulation,[status(thm)],[f43,f211]) ).
fof(f241,plain,
one = converse(one),
inference(paramodulation,[status(thm)],[f21,f208]) ).
fof(f247,plain,
! [X0] : join(complement(X0),composition(converse(converse(one)),complement(X0))) = complement(X0),
inference(paramodulation,[status(thm)],[f208,f38]) ).
fof(f248,plain,
! [X0] : X0 = composition(one,X0),
inference(backward_demodulation,[status(thm)],[f241,f208]) ).
fof(f251,plain,
! [X0] : join(complement(X0),composition(one,complement(X0))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f23,f247]) ).
fof(f252,plain,
! [X0] : join(complement(X0),complement(X0)) = complement(X0),
inference(backward_demodulation,[status(thm)],[f248,f251]) ).
fof(f308,plain,
! [X0] : zero = meet(complement(X0),meet(X0,X0)),
inference(paramodulation,[status(thm)],[f252,f43]) ).
fof(f309,plain,
! [X0] : meet(X0,X0) = complement(complement(X0)),
inference(paramodulation,[status(thm)],[f252,f19]) ).
fof(f310,plain,
! [X0] : X0 = join(meet(X0,complement(X0)),complement(complement(X0))),
inference(paramodulation,[status(thm)],[f252,f39]) ).
fof(f327,plain,
! [X0] : X0 = join(complement(complement(X0)),meet(X0,complement(X0))),
inference(forward_demodulation,[status(thm)],[f16,f310]) ).
fof(f328,plain,
! [X0] : X0 = join(complement(complement(X0)),zero),
inference(forward_demodulation,[status(thm)],[f28,f327]) ).
fof(f329,plain,
! [X0] : X0 = join(zero,complement(complement(X0))),
inference(forward_demodulation,[status(thm)],[f16,f328]) ).
fof(f332,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(zero,complement(meet(X0,X1))),
inference(paramodulation,[status(thm)],[f19,f329]) ).
fof(f344,plain,
! [X0] : X0 = join(zero,meet(X0,meet(X0,X0))),
inference(paramodulation,[status(thm)],[f309,f109]) ).
fof(f347,plain,
! [X0] : join(meet(X0,X0),complement(complement(X0))) = complement(complement(X0)),
inference(paramodulation,[status(thm)],[f309,f252]) ).
fof(f454,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X1),complement(X0))),
inference(paramodulation,[status(thm)],[f16,f19]) ).
fof(f476,plain,
converse(sK0_skl) = join(zero,meet(complement(sK1_skl),converse(sK0_skl))),
inference(backward_demodulation,[status(thm)],[f483,f108]) ).
fof(f483,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f19,f454]) ).
fof(f493,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(paramodulation,[status(thm)],[f16,f17]) ).
fof(f651,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f483,f106]) ).
fof(f653,plain,
! [X0,X1] : X0 = join(meet(X1,X0),meet(X0,complement(X1))),
inference(paramodulation,[status(thm)],[f483,f106]) ).
fof(f854,plain,
! [X0] : meet(X0,X0) = join(meet(meet(X0,X0),X0),zero),
inference(paramodulation,[status(thm)],[f308,f651]) ).
fof(f855,plain,
! [X0] : complement(complement(X0)) = join(meet(complement(complement(X0)),X0),zero),
inference(paramodulation,[status(thm)],[f28,f651]) ).
fof(f876,plain,
! [X0] : meet(X0,X0) = join(zero,meet(meet(X0,X0),X0)),
inference(forward_demodulation,[status(thm)],[f16,f854]) ).
fof(f877,plain,
! [X0] : meet(X0,X0) = join(zero,meet(X0,meet(X0,X0))),
inference(forward_demodulation,[status(thm)],[f483,f876]) ).
fof(f883,plain,
! [X0] : X0 = join(zero,X0),
inference(backward_demodulation,[status(thm)],[f901,f105]) ).
fof(f899,plain,
! [X0] : join(X0,complement(complement(X0))) = complement(complement(X0)),
inference(backward_demodulation,[status(thm)],[f901,f347]) ).
fof(f901,plain,
! [X0] : meet(X0,X0) = X0,
inference(forward_demodulation,[status(thm)],[f344,f877]) ).
fof(f902,plain,
! [X0] : complement(complement(X0)) = join(zero,meet(complement(complement(X0)),X0)),
inference(forward_demodulation,[status(thm)],[f16,f855]) ).
fof(f903,plain,
! [X0] : complement(complement(X0)) = join(zero,meet(X0,complement(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f483,f902]) ).
fof(f910,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f109,f903]) ).
fof(f922,plain,
converse(sK0_skl) = meet(complement(sK1_skl),converse(sK0_skl)),
inference(backward_demodulation,[status(thm)],[f883,f476]) ).
fof(f933,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = complement(meet(X0,X1)),
inference(backward_demodulation,[status(thm)],[f883,f332]) ).
fof(f950,plain,
! [X0] : join(X0,X0) = complement(complement(X0)),
inference(forward_demodulation,[status(thm)],[f910,f899]) ).
fof(f954,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[status(thm)],[f910,f950]) ).
fof(f1027,plain,
! [X0,X1] : join(X0,join(X0,X1)) = join(X0,X1),
inference(paramodulation,[status(thm)],[f954,f17]) ).
fof(f1372,plain,
! [X0,X1] : join(meet(X0,X1),X0) = join(meet(X0,X1),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f651,f1027]) ).
fof(f1373,plain,
! [X0,X1] : join(meet(X0,X1),X1) = join(meet(X0,X1),meet(X1,complement(X0))),
inference(paramodulation,[status(thm)],[f653,f1027]) ).
fof(f1381,plain,
! [X0] : join(X0,top) = join(X0,complement(X0)),
inference(paramodulation,[status(thm)],[f27,f1027]) ).
fof(f1398,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = join(meet(X0,X1),meet(complement(X1),X0)),
inference(forward_demodulation,[status(thm)],[f16,f1372]) ).
fof(f1404,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
inference(forward_demodulation,[status(thm)],[f651,f1398]) ).
fof(f1405,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = join(meet(X1,X0),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f16,f1373]) ).
fof(f1407,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = X0,
inference(forward_demodulation,[status(thm)],[f653,f1405]) ).
fof(f1417,plain,
! [X0] : join(X0,top) = top,
inference(forward_demodulation,[status(thm)],[f27,f1381]) ).
fof(f1429,plain,
! [X0] : join(top,X0) = top,
inference(paramodulation,[status(thm)],[f16,f1417]) ).
fof(f1433,plain,
! [X0] : converse(top) = join(X0,converse(top)),
inference(paramodulation,[status(thm)],[f1417,f44]) ).
fof(f1609,plain,
! [X0,X1] : top = join(X0,join(complement(X1),meet(complement(X0),X1))),
inference(paramodulation,[status(thm)],[f910,f217]) ).
fof(f1626,plain,
! [X0,X1] : X0 = join(meet(X0,join(complement(X1),meet(X0,X1))),complement(top)),
inference(paramodulation,[status(thm)],[f217,f39]) ).
fof(f1667,plain,
! [X0,X1] : X0 = join(complement(top),meet(X0,join(complement(X1),meet(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f16,f1626]) ).
fof(f1668,plain,
! [X0,X1] : X0 = join(zero,meet(X0,join(complement(X1),meet(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f218,f1667]) ).
fof(f1669,plain,
! [X0,X1] : X0 = meet(X0,join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f883,f1668]) ).
fof(f1677,plain,
join(complement(sK1_skl),converse(sK0_skl)) = complement(sK1_skl),
inference(paramodulation,[status(thm)],[f922,f1404]) ).
fof(f1693,plain,
converse(complement(sK1_skl)) = join(converse(complement(sK1_skl)),sK0_skl),
inference(paramodulation,[status(thm)],[f1677,f45]) ).
fof(f1698,plain,
converse(complement(sK1_skl)) = join(sK0_skl,converse(complement(sK1_skl))),
inference(forward_demodulation,[status(thm)],[f16,f1693]) ).
fof(f1773,plain,
! [X0,X1] : converse(converse(X0)) = join(X0,converse(meet(X1,converse(X0)))),
inference(paramodulation,[status(thm)],[f1407,f44]) ).
fof(f1780,plain,
! [X0,X1] : X0 = join(X0,converse(meet(X1,converse(X0)))),
inference(forward_demodulation,[status(thm)],[f23,f1773]) ).
fof(f1784,plain,
converse(top) = top,
inference(paramodulation,[status(thm)],[f1429,f1433]) ).
fof(f2540,plain,
! [X0,X1] : join(join(complement(X0),meet(X1,X0)),X1) = join(complement(X0),meet(X1,X0)),
inference(paramodulation,[status(thm)],[f1669,f1407]) ).
fof(f2575,plain,
! [X0,X1] : join(complement(X0),join(meet(X1,X0),X1)) = join(complement(X0),meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f17,f2540]) ).
fof(f2576,plain,
! [X0,X1] : join(complement(X0),join(X1,meet(X1,X0))) = join(complement(X0),meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f16,f2575]) ).
fof(f2577,plain,
! [X0,X1] : X0 = meet(X0,join(complement(X1),X0)),
inference(backward_demodulation,[status(thm)],[f2584,f1669]) ).
fof(f2578,plain,
! [X0,X1] : top = join(complement(X0),join(complement(X1),X0)),
inference(backward_demodulation,[status(thm)],[f2584,f217]) ).
fof(f2581,plain,
! [X0,X1] : top = join(X0,join(complement(X1),complement(X0))),
inference(backward_demodulation,[status(thm)],[f2584,f1609]) ).
fof(f2584,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f1404,f2576]) ).
fof(f2591,plain,
! [X0,X1] : top = join(X0,join(complement(X0),complement(X1))),
inference(forward_demodulation,[status(thm)],[f493,f2578]) ).
fof(f2592,plain,
! [X0,X1] : top = join(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f933,f2591]) ).
fof(f2597,plain,
! [X0,X1] : top = join(X0,complement(meet(X1,X0))),
inference(forward_demodulation,[status(thm)],[f933,f2581]) ).
fof(f2821,plain,
! [X0,X1] : X0 = meet(X0,join(X1,X0)),
inference(paramodulation,[status(thm)],[f910,f2577]) ).
fof(f2918,plain,
! [X0,X1] : X0 = meet(X0,join(X0,X1)),
inference(paramodulation,[status(thm)],[f16,f2821]) ).
fof(f2986,plain,
sK0_skl = meet(sK0_skl,converse(complement(sK1_skl))),
inference(paramodulation,[status(thm)],[f1698,f2918]) ).
fof(f3187,plain,
top = join(converse(complement(sK1_skl)),complement(sK0_skl)),
inference(paramodulation,[status(thm)],[f2986,f2597]) ).
fof(f3198,plain,
top = join(complement(sK0_skl),converse(complement(sK1_skl))),
inference(forward_demodulation,[status(thm)],[f16,f3187]) ).
fof(f4259,plain,
converse(top) = join(converse(complement(sK0_skl)),complement(sK1_skl)),
inference(paramodulation,[status(thm)],[f3198,f45]) ).
fof(f4272,plain,
top = join(converse(complement(sK0_skl)),complement(sK1_skl)),
inference(forward_demodulation,[status(thm)],[f1784,f4259]) ).
fof(f4273,plain,
top = join(complement(sK1_skl),converse(complement(sK0_skl))),
inference(forward_demodulation,[status(thm)],[f16,f4272]) ).
fof(f4286,plain,
sK1_skl = join(meet(sK1_skl,converse(complement(sK0_skl))),complement(top)),
inference(paramodulation,[status(thm)],[f4273,f39]) ).
fof(f4297,plain,
sK1_skl = join(complement(top),meet(sK1_skl,converse(complement(sK0_skl)))),
inference(forward_demodulation,[status(thm)],[f16,f4286]) ).
fof(f4298,plain,
sK1_skl = join(zero,meet(sK1_skl,converse(complement(sK0_skl)))),
inference(forward_demodulation,[status(thm)],[f218,f4297]) ).
fof(f4299,plain,
sK1_skl = meet(sK1_skl,converse(complement(sK0_skl))),
inference(forward_demodulation,[status(thm)],[f883,f4298]) ).
fof(f4312,plain,
complement(sK0_skl) = join(complement(sK0_skl),converse(sK1_skl)),
inference(paramodulation,[status(thm)],[f4299,f1780]) ).
fof(f4338,plain,
converse(sK1_skl) = meet(converse(sK1_skl),complement(sK0_skl)),
inference(paramodulation,[status(thm)],[f4312,f2821]) ).
fof(f4347,plain,
converse(sK1_skl) = meet(complement(sK0_skl),converse(sK1_skl)),
inference(forward_demodulation,[status(thm)],[f483,f4338]) ).
fof(f4358,plain,
top = join(complement(sK0_skl),complement(converse(sK1_skl))),
inference(paramodulation,[status(thm)],[f4347,f2592]) ).
fof(f4372,plain,
top = complement(meet(sK0_skl,converse(sK1_skl))),
inference(forward_demodulation,[status(thm)],[f933,f4358]) ).
fof(f4437,plain,
complement(top) = meet(sK0_skl,converse(sK1_skl)),
inference(paramodulation,[status(thm)],[f4372,f910]) ).
fof(f4464,plain,
zero = meet(sK0_skl,converse(sK1_skl)),
inference(forward_demodulation,[status(thm)],[f218,f4437]) ).
fof(f4465,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f4464,f32]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL006+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.35 % Computer : n014.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 03:57:50 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 7.44/1.39 % Refutation found
% 7.44/1.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.44/1.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.44/1.45 % Elapsed time: 1.082781 seconds
% 7.44/1.45 % CPU time: 8.050749 seconds
% 7.44/1.45 % Total memory used: 90.053 MB
% 7.44/1.45 % Net memory used: 87.601 MB
%------------------------------------------------------------------------------