%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : REL007+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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:12 PM UTC 2026
% Result : Theorem 0.22s 6.41s
% Output : CNFRefutation 0.22s
% 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 : 9 ( 5 ~; 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/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,conjecture,
! [X0,X1] :
( meet(X0,converse(X1)) = zero
=> meet(converse(X0),X1) = zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
~ ! [X0,X1] :
( meet(X0,converse(X1)) = zero
=> meet(converse(X0),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(converse(X0),X1) != zero
& meet(X0,converse(X1)) = zero ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f30,plain,
( meet(converse(sK0_skl),sK1_skl) != zero
& meet(sK0_skl,converse(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(sK0_skl,converse(sK1_skl)) = zero,
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f32,plain,
meet(converse(sK0_skl),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(f100,plain,
sK0_skl = join(zero,complement(join(complement(sK0_skl),converse(sK1_skl)))),
inference(paramodulation,[status(thm)],[f31,f39]) ).
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(f104,plain,
! [X0] : X0 = join(zero,meet(X0,X0)),
inference(forward_demodulation,[status(thm)],[f19,f101]) ).
fof(f105,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f16,f102]) ).
fof(f108,plain,
! [X0] : X0 = join(zero,meet(X0,complement(complement(X0)))),
inference(paramodulation,[status(thm)],[f28,f105]) ).
fof(f203,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f21,f47]) ).
fof(f205,plain,
! [X0] : X0 = composition(converse(one),X0),
inference(forward_demodulation,[status(thm)],[f23,f203]) ).
fof(f207,plain,
! [X0,X1] : top = join(join(complement(X0),complement(X1)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f19,f27]) ).
fof(f208,plain,
! [X0,X1] : meet(join(complement(X0),complement(X1)),meet(X0,X1)) = complement(top),
inference(paramodulation,[status(thm)],[f27,f41]) ).
fof(f214,plain,
! [X0,X1] : top = join(complement(X0),join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f17,f207]) ).
fof(f215,plain,
zero = complement(top),
inference(forward_demodulation,[status(thm)],[f43,f208]) ).
fof(f238,plain,
one = converse(one),
inference(paramodulation,[status(thm)],[f21,f205]) ).
fof(f244,plain,
! [X0] : join(complement(X0),composition(converse(converse(one)),complement(X0))) = complement(X0),
inference(paramodulation,[status(thm)],[f205,f38]) ).
fof(f245,plain,
! [X0] : X0 = composition(one,X0),
inference(backward_demodulation,[status(thm)],[f238,f205]) ).
fof(f248,plain,
! [X0] : join(complement(X0),composition(one,complement(X0))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f23,f244]) ).
fof(f249,plain,
! [X0] : join(complement(X0),complement(X0)) = complement(X0),
inference(backward_demodulation,[status(thm)],[f245,f248]) ).
fof(f305,plain,
! [X0] : zero = meet(complement(X0),meet(X0,X0)),
inference(paramodulation,[status(thm)],[f249,f43]) ).
fof(f306,plain,
! [X0] : meet(X0,X0) = complement(complement(X0)),
inference(paramodulation,[status(thm)],[f249,f19]) ).
fof(f307,plain,
! [X0] : X0 = join(meet(X0,complement(X0)),complement(complement(X0))),
inference(paramodulation,[status(thm)],[f249,f39]) ).
fof(f324,plain,
! [X0] : X0 = join(complement(complement(X0)),meet(X0,complement(X0))),
inference(forward_demodulation,[status(thm)],[f16,f307]) ).
fof(f325,plain,
! [X0] : X0 = join(complement(complement(X0)),zero),
inference(forward_demodulation,[status(thm)],[f28,f324]) ).
fof(f326,plain,
! [X0] : X0 = join(zero,complement(complement(X0))),
inference(forward_demodulation,[status(thm)],[f16,f325]) ).
fof(f329,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(zero,complement(meet(X0,X1))),
inference(paramodulation,[status(thm)],[f19,f326]) ).
fof(f341,plain,
! [X0] : X0 = join(zero,meet(X0,meet(X0,X0))),
inference(paramodulation,[status(thm)],[f306,f108]) ).
fof(f344,plain,
! [X0] : join(meet(X0,X0),complement(complement(X0))) = complement(complement(X0)),
inference(paramodulation,[status(thm)],[f306,f249]) ).
fof(f451,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X1),complement(X0))),
inference(paramodulation,[status(thm)],[f16,f19]) ).
fof(f471,plain,
meet(sK1_skl,converse(sK0_skl)) != zero,
inference(backward_demodulation,[status(thm)],[f479,f32]) ).
fof(f479,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f19,f451]) ).
fof(f489,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(paramodulation,[status(thm)],[f16,f17]) ).
fof(f664,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f479,f105]) ).
fof(f666,plain,
! [X0,X1] : X0 = join(meet(X1,X0),meet(X0,complement(X1))),
inference(paramodulation,[status(thm)],[f479,f105]) ).
fof(f867,plain,
! [X0] : meet(X0,X0) = join(meet(meet(X0,X0),X0),zero),
inference(paramodulation,[status(thm)],[f305,f664]) ).
fof(f868,plain,
! [X0] : complement(complement(X0)) = join(meet(complement(complement(X0)),X0),zero),
inference(paramodulation,[status(thm)],[f28,f664]) ).
fof(f889,plain,
! [X0] : meet(X0,X0) = join(zero,meet(meet(X0,X0),X0)),
inference(forward_demodulation,[status(thm)],[f16,f867]) ).
fof(f890,plain,
! [X0] : meet(X0,X0) = join(zero,meet(X0,meet(X0,X0))),
inference(forward_demodulation,[status(thm)],[f479,f889]) ).
fof(f896,plain,
! [X0] : X0 = join(zero,X0),
inference(backward_demodulation,[status(thm)],[f914,f104]) ).
fof(f912,plain,
! [X0] : join(X0,complement(complement(X0))) = complement(complement(X0)),
inference(backward_demodulation,[status(thm)],[f914,f344]) ).
fof(f914,plain,
! [X0] : meet(X0,X0) = X0,
inference(forward_demodulation,[status(thm)],[f341,f890]) ).
fof(f915,plain,
! [X0] : complement(complement(X0)) = join(zero,meet(complement(complement(X0)),X0)),
inference(forward_demodulation,[status(thm)],[f16,f868]) ).
fof(f916,plain,
! [X0] : complement(complement(X0)) = join(zero,meet(X0,complement(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f479,f915]) ).
fof(f924,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f108,f916]) ).
fof(f933,plain,
sK0_skl = complement(join(complement(sK0_skl),converse(sK1_skl))),
inference(backward_demodulation,[status(thm)],[f896,f100]) ).
fof(f944,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = complement(meet(X0,X1)),
inference(backward_demodulation,[status(thm)],[f896,f329]) ).
fof(f961,plain,
! [X0] : join(X0,X0) = complement(complement(X0)),
inference(forward_demodulation,[status(thm)],[f924,f912]) ).
fof(f965,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[status(thm)],[f924,f961]) ).
fof(f1040,plain,
! [X0,X1] : join(X0,join(X0,X1)) = join(X0,X1),
inference(paramodulation,[status(thm)],[f965,f17]) ).
fof(f1414,plain,
! [X0,X1] : join(meet(X0,X1),X0) = join(meet(X0,X1),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f664,f1040]) ).
fof(f1415,plain,
! [X0,X1] : join(meet(X0,X1),X1) = join(meet(X0,X1),meet(X1,complement(X0))),
inference(paramodulation,[status(thm)],[f666,f1040]) ).
fof(f1423,plain,
! [X0] : join(X0,top) = join(X0,complement(X0)),
inference(paramodulation,[status(thm)],[f27,f1040]) ).
fof(f1445,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = join(meet(X0,X1),meet(complement(X1),X0)),
inference(forward_demodulation,[status(thm)],[f16,f1414]) ).
fof(f1451,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
inference(forward_demodulation,[status(thm)],[f664,f1445]) ).
fof(f1452,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = join(meet(X1,X0),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f16,f1415]) ).
fof(f1454,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = X0,
inference(forward_demodulation,[status(thm)],[f666,f1452]) ).
fof(f1464,plain,
! [X0] : join(X0,top) = top,
inference(forward_demodulation,[status(thm)],[f27,f1423]) ).
fof(f1477,plain,
! [X0] : join(top,X0) = top,
inference(paramodulation,[status(thm)],[f16,f1464]) ).
fof(f1481,plain,
! [X0] : converse(top) = join(X0,converse(top)),
inference(paramodulation,[status(thm)],[f1464,f44]) ).
fof(f1649,plain,
! [X0,X1] : top = join(X0,join(complement(X1),meet(complement(X0),X1))),
inference(paramodulation,[status(thm)],[f924,f214]) ).
fof(f1665,plain,
! [X0,X1] : X0 = join(meet(X0,join(complement(X1),meet(X0,X1))),complement(top)),
inference(paramodulation,[status(thm)],[f214,f39]) ).
fof(f1705,plain,
! [X0,X1] : X0 = join(complement(top),meet(X0,join(complement(X1),meet(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f16,f1665]) ).
fof(f1706,plain,
! [X0,X1] : X0 = join(zero,meet(X0,join(complement(X1),meet(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f215,f1705]) ).
fof(f1707,plain,
! [X0,X1] : X0 = meet(X0,join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f896,f1706]) ).
fof(f1731,plain,
complement(sK0_skl) = join(complement(sK0_skl),converse(sK1_skl)),
inference(paramodulation,[status(thm)],[f933,f924]) ).
fof(f1767,plain,
converse(complement(sK0_skl)) = join(converse(complement(sK0_skl)),sK1_skl),
inference(paramodulation,[status(thm)],[f1731,f45]) ).
fof(f1773,plain,
converse(complement(sK0_skl)) = join(sK1_skl,converse(complement(sK0_skl))),
inference(forward_demodulation,[status(thm)],[f16,f1767]) ).
fof(f1895,plain,
! [X0,X1] : converse(converse(X0)) = join(X0,converse(meet(X1,converse(X0)))),
inference(paramodulation,[status(thm)],[f1454,f44]) ).
fof(f1909,plain,
! [X0,X1] : X0 = join(X0,converse(meet(X1,converse(X0)))),
inference(forward_demodulation,[status(thm)],[f23,f1895]) ).
fof(f1913,plain,
converse(top) = top,
inference(paramodulation,[status(thm)],[f1477,f1481]) ).
fof(f2666,plain,
! [X0,X1] : join(join(complement(X0),meet(X1,X0)),X1) = join(complement(X0),meet(X1,X0)),
inference(paramodulation,[status(thm)],[f1707,f1454]) ).
fof(f2702,plain,
! [X0,X1] : join(complement(X0),join(meet(X1,X0),X1)) = join(complement(X0),meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f17,f2666]) ).
fof(f2703,plain,
! [X0,X1] : join(complement(X0),join(X1,meet(X1,X0))) = join(complement(X0),meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f16,f2702]) ).
fof(f2704,plain,
! [X0,X1] : X0 = meet(X0,join(complement(X1),X0)),
inference(backward_demodulation,[status(thm)],[f2711,f1707]) ).
fof(f2705,plain,
! [X0,X1] : top = join(complement(X0),join(complement(X1),X0)),
inference(backward_demodulation,[status(thm)],[f2711,f214]) ).
fof(f2708,plain,
! [X0,X1] : top = join(X0,join(complement(X1),complement(X0))),
inference(backward_demodulation,[status(thm)],[f2711,f1649]) ).
fof(f2711,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f1451,f2703]) ).
fof(f2718,plain,
! [X0,X1] : top = join(X0,join(complement(X0),complement(X1))),
inference(forward_demodulation,[status(thm)],[f489,f2705]) ).
fof(f2719,plain,
! [X0,X1] : top = join(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f944,f2718]) ).
fof(f2724,plain,
! [X0,X1] : top = join(X0,complement(meet(X1,X0))),
inference(forward_demodulation,[status(thm)],[f944,f2708]) ).
fof(f2748,plain,
! [X0,X1] : X0 = meet(X0,join(X1,X0)),
inference(paramodulation,[status(thm)],[f924,f2704]) ).
fof(f2835,plain,
! [X0,X1] : X0 = meet(X0,join(X0,X1)),
inference(paramodulation,[status(thm)],[f16,f2748]) ).
fof(f2897,plain,
sK1_skl = meet(sK1_skl,converse(complement(sK0_skl))),
inference(paramodulation,[status(thm)],[f1773,f2835]) ).
fof(f3145,plain,
top = join(converse(complement(sK0_skl)),complement(sK1_skl)),
inference(paramodulation,[status(thm)],[f2897,f2724]) ).
fof(f3179,plain,
top = join(complement(sK1_skl),converse(complement(sK0_skl))),
inference(forward_demodulation,[status(thm)],[f16,f3145]) ).
fof(f4371,plain,
converse(top) = join(converse(complement(sK1_skl)),complement(sK0_skl)),
inference(paramodulation,[status(thm)],[f3179,f45]) ).
fof(f4384,plain,
top = join(converse(complement(sK1_skl)),complement(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f1913,f4371]) ).
fof(f4385,plain,
top = join(complement(sK0_skl),converse(complement(sK1_skl))),
inference(forward_demodulation,[status(thm)],[f16,f4384]) ).
fof(f4398,plain,
sK0_skl = join(meet(sK0_skl,converse(complement(sK1_skl))),complement(top)),
inference(paramodulation,[status(thm)],[f4385,f39]) ).
fof(f4409,plain,
sK0_skl = join(complement(top),meet(sK0_skl,converse(complement(sK1_skl)))),
inference(forward_demodulation,[status(thm)],[f16,f4398]) ).
fof(f4410,plain,
sK0_skl = join(zero,meet(sK0_skl,converse(complement(sK1_skl)))),
inference(forward_demodulation,[status(thm)],[f215,f4409]) ).
fof(f4411,plain,
sK0_skl = meet(sK0_skl,converse(complement(sK1_skl))),
inference(forward_demodulation,[status(thm)],[f896,f4410]) ).
fof(f4424,plain,
complement(sK1_skl) = join(complement(sK1_skl),converse(sK0_skl)),
inference(paramodulation,[status(thm)],[f4411,f1909]) ).
fof(f4452,plain,
converse(sK0_skl) = meet(converse(sK0_skl),complement(sK1_skl)),
inference(paramodulation,[status(thm)],[f4424,f2748]) ).
fof(f4461,plain,
converse(sK0_skl) = meet(complement(sK1_skl),converse(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f479,f4452]) ).
fof(f4471,plain,
top = join(complement(sK1_skl),complement(converse(sK0_skl))),
inference(paramodulation,[status(thm)],[f4461,f2719]) ).
fof(f4484,plain,
top = complement(meet(sK1_skl,converse(sK0_skl))),
inference(forward_demodulation,[status(thm)],[f944,f4471]) ).
fof(f4668,plain,
complement(top) = meet(sK1_skl,converse(sK0_skl)),
inference(paramodulation,[status(thm)],[f4484,f924]) ).
fof(f4696,plain,
zero = meet(sK1_skl,converse(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f215,f4668]) ).
fof(f4697,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f4696,f471]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL007+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/5.50 % Computer : n017.cluster.edu
% 0.17/5.50 % Model : x86_64 x86_64
% 0.17/5.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.50 % Memory : 8046.5625MB
% 0.17/5.50 % OS : Linux 6.8.0-71-generic
% 0.05/5.50 % CPULimit : 300
% 0.05/5.50 % WCLimit : 300
% 0.05/5.50 % DateTime : Mon Sep 21 03:53:16 UTC 2026
% 0.05/5.50 % CPUTime :
% 0.05/5.51 % Drodi V4.1.1
% 0.22/6.41 % Refutation found
% 0.22/6.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.22/6.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.84/6.46 % Elapsed time: 0.943441 seconds
% 6.84/6.46 % CPU time: 7.170337 seconds
% 6.84/6.46 % Total memory used: 86.698 MB
% 6.84/6.46 % Net memory used: 84.333 MB
%------------------------------------------------------------------------------