%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : REL043+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:26 PM UTC 2026
% Result : Theorem 15.39s 2.59s
% Output : CNFRefutation 15.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 14
% Syntax : Number of formulae : 149 ( 145 unt; 0 def)
% Number of atoms : 153 ( 152 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 9 ( 5 ~; 0 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 209 ( 206 !; 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(f6,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
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,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,conjecture,
! [X0,X1,X2] :
( join(composition(X0,converse(X1)),X2) = X2
=> join(composition(complement(X2),X1),complement(X0)) = complement(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
~ ! [X0,X1,X2] :
( join(composition(X0,converse(X1)),X2) = X2
=> join(composition(complement(X2),X1),complement(X0)) = complement(X0) ),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f19,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f20,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f21,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f22,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f24,plain,
! [X0] : composition(X0,one) = X0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f25,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f26,plain,
! [X0] : converse(converse(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f27,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f28,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f29,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f30,plain,
! [X0] : top = join(X0,complement(X0)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f31,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f32,plain,
! [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))),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f35,plain,
? [X0,X1,X2] :
( join(composition(complement(X2),X1),complement(X0)) != complement(X0)
& join(composition(X0,converse(X1)),X2) = X2 ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f36,plain,
( join(composition(complement(sK2_skl),sK1_skl),complement(sK0_skl)) != complement(sK0_skl)
& join(composition(sK0_skl,converse(sK1_skl)),sK2_skl) = sK2_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)],[f35]) ).
fof(f37,plain,
join(composition(sK0_skl,converse(sK1_skl)),sK2_skl) = sK2_skl,
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f38,plain,
join(composition(complement(sK2_skl),sK1_skl),complement(sK0_skl)) != complement(sK0_skl),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f44,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[status(thm)],[f19,f21]) ).
fof(f45,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),X1)),meet(X0,X1)),
inference(backward_demodulation,[status(thm)],[f22,f44]) ).
fof(f46,plain,
! [X0,X1] : join(complement(X0),composition(converse(X1),complement(composition(X1,X0)))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f19,f29]) ).
fof(f47,plain,
join(sK2_skl,composition(sK0_skl,converse(sK1_skl))) = sK2_skl,
inference(forward_demodulation,[status(thm)],[f19,f37]) ).
fof(f48,plain,
join(complement(sK0_skl),composition(complement(sK2_skl),sK1_skl)) != complement(sK0_skl),
inference(forward_demodulation,[status(thm)],[f19,f38]) ).
fof(f49,plain,
! [X0,X1] : X0 = join(meet(X0,X1),complement(join(complement(X0),X1))),
inference(forward_demodulation,[status(thm)],[f19,f45]) ).
fof(f58,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X1),complement(X0))),
inference(paramodulation,[status(thm)],[f19,f22]) ).
fof(f64,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f22,f58]) ).
fof(f68,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(paramodulation,[status(thm)],[f19,f20]) ).
fof(f72,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X1,X0),X2),
inference(paramodulation,[status(thm)],[f19,f20]) ).
fof(f78,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(forward_demodulation,[status(thm)],[f20,f72]) ).
fof(f85,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(paramodulation,[status(thm)],[f26,f28]) ).
fof(f102,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(paramodulation,[status(thm)],[f26,f27]) ).
fof(f225,plain,
! [X0,X1] : X0 = join(meet(X0,complement(X1)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f22,f49]) ).
fof(f230,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f19,f225]) ).
fof(f232,plain,
! [X0,X1] : X0 = join(meet(X1,X0),meet(X0,complement(X1))),
inference(paramodulation,[status(thm)],[f64,f230]) ).
fof(f234,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f64,f230]) ).
fof(f242,plain,
! [X0,X1] : X0 = join(meet(X1,X0),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f64,f232]) ).
fof(f304,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f24,f85]) ).
fof(f310,plain,
! [X0] : X0 = composition(converse(one),X0),
inference(forward_demodulation,[status(thm)],[f26,f304]) ).
fof(f314,plain,
one = converse(one),
inference(paramodulation,[status(thm)],[f24,f310]) ).
fof(f315,plain,
! [X0] : join(complement(X0),complement(composition(one,X0))) = complement(X0),
inference(paramodulation,[status(thm)],[f310,f46]) ).
fof(f322,plain,
! [X0,X1] : composition(join(converse(one),X0),X1) = join(X1,composition(X0,X1)),
inference(paramodulation,[status(thm)],[f310,f25]) ).
fof(f324,plain,
! [X0] : X0 = composition(one,X0),
inference(backward_demodulation,[status(thm)],[f314,f310]) ).
fof(f331,plain,
! [X0,X1] : composition(join(one,X0),X1) = join(X1,composition(X0,X1)),
inference(forward_demodulation,[status(thm)],[f314,f322]) ).
fof(f332,plain,
! [X0] : join(complement(X0),complement(X0)) = complement(X0),
inference(backward_demodulation,[status(thm)],[f324,f315]) ).
fof(f347,plain,
! [X0] : converse(join(one,X0)) = join(one,converse(X0)),
inference(paramodulation,[status(thm)],[f314,f102]) ).
fof(f366,plain,
! [X0] : meet(X0,complement(X0)) = complement(top),
inference(paramodulation,[status(thm)],[f30,f22]) ).
fof(f367,plain,
! [X0] : X0 = join(meet(X0,complement(complement(X0))),complement(top)),
inference(paramodulation,[status(thm)],[f30,f49]) ).
fof(f370,plain,
zero = complement(top),
inference(forward_demodulation,[status(thm)],[f31,f366]) ).
fof(f371,plain,
! [X0] : X0 = join(complement(top),meet(X0,complement(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f19,f367]) ).
fof(f372,plain,
! [X0] : X0 = join(zero,meet(X0,complement(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f370,f371]) ).
fof(f374,plain,
! [X0] : join(zero,composition(converse(X0),complement(composition(X0,top)))) = complement(top),
inference(paramodulation,[status(thm)],[f370,f46]) ).
fof(f382,plain,
! [X0] : join(zero,composition(converse(X0),complement(composition(X0,top)))) = zero,
inference(forward_demodulation,[status(thm)],[f370,f374]) ).
fof(f388,plain,
! [X0] : complement(complement(X0)) = join(meet(X0,complement(complement(X0))),zero),
inference(paramodulation,[status(thm)],[f31,f242]) ).
fof(f390,plain,
! [X0] : X0 = join(meet(X0,X0),zero),
inference(paramodulation,[status(thm)],[f31,f232]) ).
fof(f398,plain,
! [X0] : complement(complement(X0)) = join(zero,meet(X0,complement(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f19,f388]) ).
fof(f401,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f372,f398]) ).
fof(f405,plain,
! [X0] : X0 = join(zero,meet(X0,X0)),
inference(forward_demodulation,[status(thm)],[f19,f390]) ).
fof(f410,plain,
complement(zero) = top,
inference(paramodulation,[status(thm)],[f370,f401]) ).
fof(f411,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(X1)),
inference(paramodulation,[status(thm)],[f22,f401]) ).
fof(f420,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(complement(X0),X1)),
inference(paramodulation,[status(thm)],[f401,f22]) ).
fof(f421,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(X0,complement(X1))),
inference(paramodulation,[status(thm)],[f401,f22]) ).
fof(f424,plain,
! [X0] : complement(meet(X0,X0)) = complement(X0),
inference(backward_demodulation,[status(thm)],[f411,f332]) ).
fof(f474,plain,
! [X0] : complement(complement(X0)) = meet(X0,X0),
inference(paramodulation,[status(thm)],[f424,f401]) ).
fof(f483,plain,
! [X0] : X0 = join(zero,X0),
inference(backward_demodulation,[status(thm)],[f485,f405]) ).
fof(f485,plain,
! [X0] : X0 = meet(X0,X0),
inference(forward_demodulation,[status(thm)],[f401,f474]) ).
fof(f506,plain,
! [X0] : composition(converse(X0),complement(composition(X0,top))) = zero,
inference(backward_demodulation,[status(thm)],[f483,f382]) ).
fof(f514,plain,
! [X0] : X0 = join(X0,meet(complement(X0),X0)),
inference(paramodulation,[status(thm)],[f485,f242]) ).
fof(f532,plain,
! [X0] : X0 = join(X0,meet(X0,complement(X0))),
inference(forward_demodulation,[status(thm)],[f64,f514]) ).
fof(f534,plain,
! [X0] : X0 = join(X0,zero),
inference(forward_demodulation,[status(thm)],[f31,f532]) ).
fof(f553,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(zero)),
inference(paramodulation,[status(thm)],[f534,f102]) ).
fof(f560,plain,
! [X0] : X0 = join(X0,converse(zero)),
inference(forward_demodulation,[status(thm)],[f26,f553]) ).
fof(f561,plain,
zero = converse(zero),
inference(paramodulation,[status(thm)],[f483,f560]) ).
fof(f1363,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X0,join(X2,X1)),
inference(paramodulation,[status(thm)],[f68,f78]) ).
fof(f1403,plain,
! [X0,X1] : join(X0,top) = join(X1,join(X0,complement(X1))),
inference(paramodulation,[status(thm)],[f30,f78]) ).
fof(f1820,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),complement(X0)),
inference(paramodulation,[status(thm)],[f19,f411]) ).
fof(f1822,plain,
! [X0] : complement(meet(zero,X0)) = join(top,complement(X0)),
inference(paramodulation,[status(thm)],[f410,f411]) ).
fof(f1823,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(X1)),
inference(paramodulation,[status(thm)],[f401,f411]) ).
fof(f1826,plain,
! [X0,X1] : complement(meet(X0,complement(X1))) = join(complement(X0),X1),
inference(paramodulation,[status(thm)],[f401,f411]) ).
fof(f1827,plain,
! [X0] : complement(meet(X0,top)) = join(complement(X0),zero),
inference(paramodulation,[status(thm)],[f370,f411]) ).
fof(f1839,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f411,f1820]) ).
fof(f1843,plain,
! [X0] : complement(meet(X0,top)) = complement(X0),
inference(forward_demodulation,[status(thm)],[f534,f1827]) ).
fof(f1861,plain,
! [X0] : complement(complement(X0)) = meet(X0,top),
inference(paramodulation,[status(thm)],[f1843,f401]) ).
fof(f1888,plain,
! [X0] : X0 = meet(X0,top),
inference(forward_demodulation,[status(thm)],[f401,f1861]) ).
fof(f2079,plain,
! [X0,X1] : top = join(meet(X0,X1),complement(meet(X1,X0))),
inference(paramodulation,[status(thm)],[f1839,f30]) ).
fof(f2172,plain,
! [X0] : meet(zero,complement(X0)) = complement(join(top,X0)),
inference(paramodulation,[status(thm)],[f410,f420]) ).
fof(f2173,plain,
! [X0,X1] : meet(complement(X0),complement(X1)) = complement(join(X0,X1)),
inference(paramodulation,[status(thm)],[f401,f420]) ).
fof(f2321,plain,
! [X0] : composition(join(one,converse(X0)),complement(composition(join(one,X0),top))) = zero,
inference(paramodulation,[status(thm)],[f347,f506]) ).
fof(f2342,plain,
! [X0] : composition(join(one,converse(X0)),complement(join(top,composition(X0,top)))) = zero,
inference(forward_demodulation,[status(thm)],[f331,f2321]) ).
fof(f2343,plain,
! [X0] : composition(join(one,converse(X0)),meet(zero,complement(composition(X0,top)))) = zero,
inference(forward_demodulation,[status(thm)],[f2172,f2342]) ).
fof(f3595,plain,
! [X0] : zero = meet(meet(zero,X0),join(top,complement(X0))),
inference(paramodulation,[status(thm)],[f1822,f31]) ).
fof(f3863,plain,
! [X0] : complement(complement(X0)) = join(X0,complement(complement(X0))),
inference(paramodulation,[status(thm)],[f485,f1823]) ).
fof(f3902,plain,
! [X0] : X0 = join(X0,complement(complement(X0))),
inference(forward_demodulation,[status(thm)],[f401,f3863]) ).
fof(f3913,plain,
! [X0] : X0 = join(X0,X0),
inference(forward_demodulation,[status(thm)],[f401,f3902]) ).
fof(f3983,plain,
! [X0] : join(complement(X0),top) = join(X0,complement(X0)),
inference(paramodulation,[status(thm)],[f3913,f1403]) ).
fof(f3985,plain,
! [X0,X1] : join(X0,join(X1,X0)) = join(X1,X0),
inference(paramodulation,[status(thm)],[f3913,f78]) ).
fof(f4020,plain,
! [X0] : join(top,complement(X0)) = join(X0,complement(X0)),
inference(forward_demodulation,[status(thm)],[f19,f3983]) ).
fof(f4029,plain,
! [X0] : zero = meet(meet(zero,X0),top),
inference(backward_demodulation,[status(thm)],[f4033,f3595]) ).
fof(f4033,plain,
! [X0] : join(top,complement(X0)) = top,
inference(forward_demodulation,[status(thm)],[f30,f4020]) ).
fof(f4068,plain,
! [X0] : composition(join(one,converse(X0)),zero) = zero,
inference(backward_demodulation,[status(thm)],[f4108,f2343]) ).
fof(f4108,plain,
! [X0] : zero = meet(zero,X0),
inference(forward_demodulation,[status(thm)],[f1888,f4029]) ).
fof(f4119,plain,
! [X0] : join(zero,composition(converse(X0),zero)) = zero,
inference(forward_demodulation,[status(thm)],[f331,f4068]) ).
fof(f4127,plain,
! [X0] : composition(converse(X0),zero) = zero,
inference(forward_demodulation,[status(thm)],[f483,f4119]) ).
fof(f4478,plain,
! [X0] : converse(zero) = composition(converse(zero),X0),
inference(paramodulation,[status(thm)],[f4127,f85]) ).
fof(f4521,plain,
! [X0] : zero = composition(converse(zero),X0),
inference(forward_demodulation,[status(thm)],[f561,f4478]) ).
fof(f4540,plain,
! [X0] : zero = composition(zero,X0),
inference(forward_demodulation,[status(thm)],[f561,f4521]) ).
fof(f4722,plain,
! [X0,X1] : join(meet(complement(X0),X1),X1) = join(meet(X0,X1),meet(complement(X0),X1)),
inference(paramodulation,[status(thm)],[f242,f3985]) ).
fof(f4785,plain,
! [X0,X1] : join(X0,meet(complement(X1),X0)) = join(meet(X1,X0),meet(complement(X1),X0)),
inference(forward_demodulation,[status(thm)],[f19,f4722]) ).
fof(f4786,plain,
! [X0,X1] : join(X0,meet(complement(X1),X0)) = X0,
inference(forward_demodulation,[status(thm)],[f242,f4785]) ).
fof(f4891,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = X0,
inference(paramodulation,[status(thm)],[f401,f4786]) ).
fof(f4950,plain,
! [X0,X1,X2] : join(X0,join(X1,meet(X2,X0))) = join(X1,X0),
inference(paramodulation,[status(thm)],[f4891,f78]) ).
fof(f6507,plain,
! [X0,X1] : top = join(meet(X0,complement(X1)),join(X1,complement(X0))),
inference(paramodulation,[status(thm)],[f1823,f2079]) ).
fof(f6561,plain,
! [X0,X1] : top = join(X0,join(meet(X1,complement(X0)),complement(X1))),
inference(forward_demodulation,[status(thm)],[f78,f6507]) ).
fof(f6562,plain,
! [X0,X1] : top = join(X0,join(complement(X1),meet(X1,complement(X0)))),
inference(forward_demodulation,[status(thm)],[f1363,f6561]) ).
fof(f7949,plain,
! [X0,X1] : join(complement(X0),X1) = join(meet(X0,X1),complement(X0)),
inference(paramodulation,[status(thm)],[f232,f4950]) ).
fof(f8024,plain,
! [X0,X1] : top = join(X0,join(complement(X1),complement(X0))),
inference(backward_demodulation,[status(thm)],[f8025,f6562]) ).
fof(f8025,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f19,f7949]) ).
fof(f8084,plain,
! [X0,X1] : top = join(X0,complement(meet(X1,X0))),
inference(forward_demodulation,[status(thm)],[f411,f8024]) ).
fof(f8122,plain,
! [X0,X1] : meet(complement(X0),meet(X1,X0)) = complement(top),
inference(paramodulation,[status(thm)],[f8084,f421]) ).
fof(f8170,plain,
! [X0,X1] : meet(complement(X0),meet(X1,X0)) = zero,
inference(forward_demodulation,[status(thm)],[f370,f8122]) ).
fof(f8193,plain,
! [X0,X1] : meet(complement(complement(X0)),complement(join(X1,X0))) = zero,
inference(paramodulation,[status(thm)],[f2173,f8170]) ).
fof(f8229,plain,
! [X0,X1] : complement(join(complement(X0),join(X1,X0))) = zero,
inference(forward_demodulation,[status(thm)],[f2173,f8193]) ).
fof(f8230,plain,
! [X0,X1] : meet(X0,complement(join(X1,X0))) = zero,
inference(forward_demodulation,[status(thm)],[f420,f8229]) ).
fof(f8928,plain,
meet(composition(sK0_skl,converse(sK1_skl)),complement(sK2_skl)) = zero,
inference(paramodulation,[status(thm)],[f47,f8230]) ).
fof(f9014,plain,
meet(complement(sK2_skl),composition(sK0_skl,converse(sK1_skl))) = zero,
inference(forward_demodulation,[status(thm)],[f64,f8928]) ).
fof(f9963,plain,
join(meet(composition(complement(sK2_skl),sK1_skl),sK0_skl),composition(zero,meet(sK1_skl,composition(converse(complement(sK2_skl)),sK0_skl)))) = composition(meet(complement(sK2_skl),composition(sK0_skl,converse(sK1_skl))),meet(sK1_skl,composition(converse(complement(sK2_skl)),sK0_skl))),
inference(paramodulation,[status(thm)],[f9014,f32]) ).
fof(f9986,plain,
join(meet(sK0_skl,composition(complement(sK2_skl),sK1_skl)),composition(zero,meet(sK1_skl,composition(converse(complement(sK2_skl)),sK0_skl)))) = composition(meet(complement(sK2_skl),composition(sK0_skl,converse(sK1_skl))),meet(sK1_skl,composition(converse(complement(sK2_skl)),sK0_skl))),
inference(forward_demodulation,[status(thm)],[f64,f9963]) ).
fof(f9987,plain,
join(meet(sK0_skl,composition(complement(sK2_skl),sK1_skl)),zero) = composition(meet(complement(sK2_skl),composition(sK0_skl,converse(sK1_skl))),meet(sK1_skl,composition(converse(complement(sK2_skl)),sK0_skl))),
inference(forward_demodulation,[status(thm)],[f4540,f9986]) ).
fof(f9988,plain,
meet(sK0_skl,composition(complement(sK2_skl),sK1_skl)) = composition(meet(complement(sK2_skl),composition(sK0_skl,converse(sK1_skl))),meet(sK1_skl,composition(converse(complement(sK2_skl)),sK0_skl))),
inference(forward_demodulation,[status(thm)],[f534,f9987]) ).
fof(f9989,plain,
meet(sK0_skl,composition(complement(sK2_skl),sK1_skl)) = composition(zero,meet(sK1_skl,composition(converse(complement(sK2_skl)),sK0_skl))),
inference(forward_demodulation,[status(thm)],[f9014,f9988]) ).
fof(f9990,plain,
meet(sK0_skl,composition(complement(sK2_skl),sK1_skl)) = zero,
inference(forward_demodulation,[status(thm)],[f4540,f9989]) ).
fof(f10038,plain,
sK0_skl = join(zero,meet(complement(composition(complement(sK2_skl),sK1_skl)),sK0_skl)),
inference(paramodulation,[status(thm)],[f9990,f234]) ).
fof(f10062,plain,
sK0_skl = meet(complement(composition(complement(sK2_skl),sK1_skl)),sK0_skl),
inference(forward_demodulation,[status(thm)],[f483,f10038]) ).
fof(f10063,plain,
sK0_skl = meet(sK0_skl,complement(composition(complement(sK2_skl),sK1_skl))),
inference(forward_demodulation,[status(thm)],[f64,f10062]) ).
fof(f10100,plain,
complement(sK0_skl) = join(complement(sK0_skl),composition(complement(sK2_skl),sK1_skl)),
inference(paramodulation,[status(thm)],[f10063,f1826]) ).
fof(f10122,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f10100,f48]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : REL043+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.43 % Computer : n026.cluster.edu
% 0.19/0.43 % Model : x86_64 x86_64
% 0.19/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.43 % Memory : 8046.5625MB
% 0.19/0.43 % OS : Linux 6.8.0-71-generic
% 0.19/0.43 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Mon Sep 21 04:10:52 UTC 2026
% 0.19/0.44 % CPUTime :
% 0.19/0.45 % Drodi V4.1.1
% 15.39/2.59 % Refutation found
% 15.39/2.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.39/2.59 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.22/2.68 % Elapsed time: 2.227416 seconds
% 1.22/2.68 % CPU time: 17.171508 seconds
% 1.22/2.68 % Total memory used: 186.264 MB
% 1.22/2.68 % Net memory used: 174.777 MB
%------------------------------------------------------------------------------