%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : REL044+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 : n011.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:27 PM UTC 2026
% Result : Theorem 187.44s 24.11s
% Output : CNFRefutation 106.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 13
% Syntax : Number of formulae : 221 ( 217 unt; 0 def)
% Number of atoms : 225 ( 224 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 9 ( 5 ~; 0 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 8 ( 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 : 360 ( 357 !; 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,conjecture,
! [X0,X1,X2] :
( join(composition(complement(X0),X1),complement(X2)) = complement(X2)
=> join(composition(X2,converse(X1)),X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
~ ! [X0,X1,X2] :
( join(composition(complement(X0),X1),complement(X2)) = complement(X2)
=> join(composition(X2,converse(X1)),X0) = X0 ),
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(f22,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[status(thm)],[f7]) ).
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,X2] :
( join(composition(X2,converse(X1)),X0) != X0
& join(composition(complement(X0),X1),complement(X2)) = complement(X2) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f30,plain,
( join(composition(sK2_skl,converse(sK1_skl)),sK0_skl) != sK0_skl
& join(composition(complement(sK0_skl),sK1_skl),complement(sK2_skl)) = complement(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)],[f29]) ).
fof(f31,plain,
join(composition(complement(sK0_skl),sK1_skl),complement(sK2_skl)) = complement(sK2_skl),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f32,plain,
join(composition(sK2_skl,converse(sK1_skl)),sK0_skl) != sK0_skl,
inference(cnf_transformation,[status(thm)],[f30]) ).
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] : X0 = join(complement(join(complement(X0),X1)),meet(X0,X1)),
inference(backward_demodulation,[status(thm)],[f19,f37]) ).
fof(f39,plain,
! [X0,X1] : join(complement(X0),composition(converse(X1),complement(composition(X1,X0)))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f16,f26]) ).
fof(f40,plain,
join(complement(sK2_skl),composition(complement(sK0_skl),sK1_skl)) = complement(sK2_skl),
inference(forward_demodulation,[status(thm)],[f16,f31]) ).
fof(f41,plain,
join(sK0_skl,composition(sK2_skl,converse(sK1_skl))) != sK0_skl,
inference(forward_demodulation,[status(thm)],[f16,f32]) ).
fof(f42,plain,
! [X0,X1] : X0 = join(meet(X0,X1),complement(join(complement(X0),X1))),
inference(forward_demodulation,[status(thm)],[f16,f38]) ).
fof(f48,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(paramodulation,[status(thm)],[f16,f17]) ).
fof(f51,plain,
! [X0] : join(complement(sK2_skl),join(composition(complement(sK0_skl),sK1_skl),X0)) = join(complement(sK2_skl),X0),
inference(paramodulation,[status(thm)],[f40,f17]) ).
fof(f52,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X1,X0),X2),
inference(paramodulation,[status(thm)],[f16,f17]) ).
fof(f58,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(forward_demodulation,[status(thm)],[f17,f52]) ).
fof(f63,plain,
! [X0,X1] : converse(composition(X0,converse(X1))) = composition(X1,converse(X0)),
inference(paramodulation,[status(thm)],[f23,f25]) ).
fof(f64,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(paramodulation,[status(thm)],[f23,f25]) ).
fof(f81,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(paramodulation,[status(thm)],[f23,f24]) ).
fof(f83,plain,
! [X0,X1] : converse(join(X0,converse(X1))) = join(converse(X0),X1),
inference(paramodulation,[status(thm)],[f23,f24]) ).
fof(f112,plain,
! [X0,X1] : X0 = join(meet(X0,X1),complement(join(X1,complement(X0)))),
inference(paramodulation,[status(thm)],[f16,f42]) ).
fof(f114,plain,
! [X0,X1,X2] : join(meet(X0,X1),join(complement(join(complement(X0),X1)),X2)) = join(X0,X2),
inference(paramodulation,[status(thm)],[f42,f17]) ).
fof(f167,plain,
! [X0,X1] : join(complement(X0),composition(X1,complement(composition(converse(X1),X0)))) = complement(X0),
inference(paramodulation,[status(thm)],[f23,f39]) ).
fof(f179,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f21,f64]) ).
fof(f185,plain,
! [X0] : X0 = composition(converse(one),X0),
inference(forward_demodulation,[status(thm)],[f23,f179]) ).
fof(f194,plain,
! [X0] : converse(top) = join(X0,converse(complement(converse(X0)))),
inference(paramodulation,[status(thm)],[f27,f81]) ).
fof(f196,plain,
! [X0] : X0 = join(meet(X0,complement(complement(X0))),complement(top)),
inference(paramodulation,[status(thm)],[f27,f42]) ).
fof(f198,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(paramodulation,[status(thm)],[f27,f17]) ).
fof(f199,plain,
! [X0] : X0 = join(complement(top),meet(X0,complement(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f16,f196]) ).
fof(f202,plain,
one = converse(one),
inference(paramodulation,[status(thm)],[f21,f185]) ).
fof(f203,plain,
! [X0] : join(complement(X0),complement(composition(one,X0))) = complement(X0),
inference(paramodulation,[status(thm)],[f185,f39]) ).
fof(f212,plain,
! [X0] : X0 = composition(one,X0),
inference(backward_demodulation,[status(thm)],[f202,f185]) ).
fof(f220,plain,
! [X0] : join(complement(X0),complement(X0)) = complement(X0),
inference(backward_demodulation,[status(thm)],[f212,f203]) ).
fof(f253,plain,
! [X0] : X0 = join(meet(X0,complement(X0)),complement(complement(X0))),
inference(paramodulation,[status(thm)],[f220,f42]) ).
fof(f256,plain,
! [X0] : X0 = join(complement(complement(X0)),meet(X0,complement(X0))),
inference(forward_demodulation,[status(thm)],[f16,f253]) ).
fof(f257,plain,
! [X0] : X0 = join(complement(complement(X0)),zero),
inference(forward_demodulation,[status(thm)],[f28,f256]) ).
fof(f258,plain,
! [X0] : X0 = join(zero,complement(complement(X0))),
inference(forward_demodulation,[status(thm)],[f16,f257]) ).
fof(f265,plain,
! [X0] : meet(X0,X0) = complement(complement(X0)),
inference(paramodulation,[status(thm)],[f220,f19]) ).
fof(f266,plain,
! [X0] : meet(X0,complement(X0)) = complement(top),
inference(paramodulation,[status(thm)],[f27,f19]) ).
fof(f267,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X1),complement(X0))),
inference(paramodulation,[status(thm)],[f16,f19]) ).
fof(f270,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(f271,plain,
! [X0,X1] : X0 = join(meet(X0,complement(X1)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f19,f42]) ).
fof(f272,plain,
! [X0,X1] : X0 = join(meet(X0,complement(X1)),meet(X1,X0)),
inference(paramodulation,[status(thm)],[f19,f112]) ).
fof(f274,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),meet(X0,X1)) = complement(join(complement(X0),complement(X1))),
inference(paramodulation,[status(thm)],[f19,f220]) ).
fof(f286,plain,
! [X0] : X0 = join(zero,meet(X0,complement(complement(X0)))),
inference(backward_demodulation,[status(thm)],[f287,f199]) ).
fof(f287,plain,
zero = complement(top),
inference(forward_demodulation,[status(thm)],[f28,f266]) ).
fof(f291,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f19,f267]) ).
fof(f293,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f16,f271]) ).
fof(f294,plain,
! [X0,X1] : X0 = join(meet(X1,X0),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f16,f272]) ).
fof(f295,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,f274]) ).
fof(f296,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,X1)) = complement(join(complement(X0),complement(X1))),
inference(forward_demodulation,[status(thm)],[f19,f295]) ).
fof(f297,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,X1)) = meet(X0,X1),
inference(forward_demodulation,[status(thm)],[f19,f296]) ).
fof(f310,plain,
! [X0] : meet(X0,top) = complement(join(complement(X0),zero)),
inference(paramodulation,[status(thm)],[f287,f19]) ).
fof(f320,plain,
! [X0] : meet(X0,top) = complement(join(zero,complement(X0))),
inference(forward_demodulation,[status(thm)],[f16,f310]) ).
fof(f665,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,f286]) ).
fof(f671,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)],[f291,f665]) ).
fof(f672,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(zero,complement(join(complement(complement(meet(X0,X1))),meet(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f270,f671]) ).
fof(f673,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(zero,complement(join(meet(X0,X1),complement(complement(meet(X0,X1)))))),
inference(forward_demodulation,[status(thm)],[f16,f672]) ).
fof(f682,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f291,f293]) ).
fof(f711,plain,
! [X0,X1] : X0 = join(meet(X1,X0),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f291,f294]) ).
fof(f741,plain,
! [X0] : complement(complement(X0)) = join(meet(complement(complement(X0)),X0),zero),
inference(paramodulation,[status(thm)],[f28,f682]) ).
fof(f744,plain,
! [X0] : complement(X0) = join(meet(complement(X0),X0),complement(complement(complement(X0)))),
inference(paramodulation,[status(thm)],[f265,f682]) ).
fof(f758,plain,
! [X0] : complement(complement(X0)) = join(zero,meet(complement(complement(X0)),X0)),
inference(forward_demodulation,[status(thm)],[f16,f741]) ).
fof(f759,plain,
! [X0] : complement(complement(X0)) = join(zero,meet(X0,complement(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f291,f758]) ).
fof(f763,plain,
! [X0] : X0 = join(zero,X0),
inference(backward_demodulation,[status(thm)],[f775,f258]) ).
fof(f764,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(zero,complement(join(meet(X0,X1),meet(X0,X1)))),
inference(backward_demodulation,[status(thm)],[f775,f673]) ).
fof(f775,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f286,f759]) ).
fof(f776,plain,
! [X0] : complement(X0) = join(complement(complement(complement(X0))),meet(complement(X0),X0)),
inference(forward_demodulation,[status(thm)],[f16,f744]) ).
fof(f777,plain,
! [X0] : complement(X0) = join(complement(X0),meet(complement(X0),X0)),
inference(forward_demodulation,[status(thm)],[f775,f776]) ).
fof(f778,plain,
! [X0] : complement(X0) = join(complement(X0),meet(X0,complement(X0))),
inference(forward_demodulation,[status(thm)],[f291,f777]) ).
fof(f779,plain,
! [X0] : complement(X0) = join(complement(X0),zero),
inference(forward_demodulation,[status(thm)],[f28,f778]) ).
fof(f781,plain,
! [X0] : meet(X0,top) = complement(complement(X0)),
inference(backward_demodulation,[status(thm)],[f782,f320]) ).
fof(f782,plain,
! [X0] : complement(X0) = join(zero,complement(X0)),
inference(forward_demodulation,[status(thm)],[f16,f779]) ).
fof(f796,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = complement(join(meet(X0,X1),meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f782,f764]) ).
fof(f805,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = complement(meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f297,f796]) ).
fof(f813,plain,
! [X0] : meet(X0,top) = X0,
inference(forward_demodulation,[status(thm)],[f775,f781]) ).
fof(f825,plain,
complement(zero) = top,
inference(paramodulation,[status(thm)],[f287,f775]) ).
fof(f1006,plain,
! [X0] : meet(top,X0) = X0,
inference(paramodulation,[status(thm)],[f291,f813]) ).
fof(f1014,plain,
! [X0] : X0 = join(X0,complement(join(top,complement(X0)))),
inference(paramodulation,[status(thm)],[f813,f112]) ).
fof(f1200,plain,
zero = complement(join(top,complement(zero))),
inference(paramodulation,[status(thm)],[f763,f1014]) ).
fof(f1219,plain,
zero = complement(join(top,top)),
inference(forward_demodulation,[status(thm)],[f825,f1200]) ).
fof(f1245,plain,
complement(zero) = join(top,top),
inference(paramodulation,[status(thm)],[f1219,f775]) ).
fof(f1257,plain,
top = join(top,top),
inference(forward_demodulation,[status(thm)],[f825,f1245]) ).
fof(f1546,plain,
! [X0,X1] : join(meet(X0,X1),top) = join(X0,complement(complement(join(complement(X0),X1)))),
inference(paramodulation,[status(thm)],[f27,f114]) ).
fof(f1592,plain,
! [X0,X1] : join(top,meet(X0,X1)) = join(X0,complement(complement(join(complement(X0),X1)))),
inference(forward_demodulation,[status(thm)],[f16,f1546]) ).
fof(f1593,plain,
! [X0,X1] : join(top,meet(X0,X1)) = join(X0,join(complement(X0),X1)),
inference(forward_demodulation,[status(thm)],[f775,f1592]) ).
fof(f1594,plain,
! [X0,X1] : join(top,meet(X0,X1)) = join(top,X1),
inference(forward_demodulation,[status(thm)],[f198,f1593]) ).
fof(f1813,plain,
! [X0] : join(top,X0) = join(top,top),
inference(paramodulation,[status(thm)],[f813,f1594]) ).
fof(f1853,plain,
! [X0] : join(top,X0) = top,
inference(forward_demodulation,[status(thm)],[f1257,f1813]) ).
fof(f1980,plain,
! [X0] : join(X0,meet(top,X0)) = meet(top,X0),
inference(paramodulation,[status(thm)],[f1006,f297]) ).
fof(f1984,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,X0)) = meet(X1,X0),
inference(paramodulation,[status(thm)],[f291,f297]) ).
fof(f1997,plain,
! [X0] : join(X0,X0) = meet(top,X0),
inference(forward_demodulation,[status(thm)],[f1006,f1980]) ).
fof(f2000,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[status(thm)],[f1006,f1997]) ).
fof(f2035,plain,
! [X0,X1] : join(meet(X0,X1),complement(join(complement(X0),X1))) = join(X0,complement(join(complement(X0),X1))),
inference(paramodulation,[status(thm)],[f2000,f114]) ).
fof(f2062,plain,
! [X0,X1] : X0 = join(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[status(thm)],[f42,f2035]) ).
fof(f2090,plain,
converse(top) = top,
inference(paramodulation,[status(thm)],[f1853,f194]) ).
fof(f2105,plain,
join(complement(sK2_skl),converse(top)) = join(complement(sK2_skl),converse(complement(converse(composition(complement(sK0_skl),sK1_skl))))),
inference(paramodulation,[status(thm)],[f194,f51]) ).
fof(f2113,plain,
! [X0] : X0 = join(meet(X0,converse(complement(converse(complement(X0))))),complement(converse(top))),
inference(paramodulation,[status(thm)],[f194,f42]) ).
fof(f2150,plain,
join(complement(sK2_skl),top) = join(complement(sK2_skl),converse(complement(converse(composition(complement(sK0_skl),sK1_skl))))),
inference(forward_demodulation,[status(thm)],[f2090,f2105]) ).
fof(f2151,plain,
join(top,complement(sK2_skl)) = join(complement(sK2_skl),converse(complement(converse(composition(complement(sK0_skl),sK1_skl))))),
inference(forward_demodulation,[status(thm)],[f16,f2150]) ).
fof(f2152,plain,
top = join(complement(sK2_skl),converse(complement(converse(composition(complement(sK0_skl),sK1_skl))))),
inference(forward_demodulation,[status(thm)],[f1853,f2151]) ).
fof(f2175,plain,
! [X0] : X0 = join(complement(converse(top)),meet(X0,converse(complement(converse(complement(X0)))))),
inference(forward_demodulation,[status(thm)],[f16,f2113]) ).
fof(f2176,plain,
! [X0] : X0 = join(complement(top),meet(X0,converse(complement(converse(complement(X0)))))),
inference(forward_demodulation,[status(thm)],[f2090,f2175]) ).
fof(f2177,plain,
! [X0] : X0 = join(zero,meet(X0,converse(complement(converse(complement(X0)))))),
inference(forward_demodulation,[status(thm)],[f287,f2176]) ).
fof(f2179,plain,
! [X0] : X0 = meet(X0,converse(complement(converse(complement(X0))))),
inference(forward_demodulation,[status(thm)],[f763,f2177]) ).
fof(f2468,plain,
! [X0,X1] : X0 = join(X0,complement(join(X1,complement(X0)))),
inference(paramodulation,[status(thm)],[f16,f2062]) ).
fof(f2603,plain,
! [X0,X1] : join(X0,complement(X1)) = complement(meet(complement(X0),X1)),
inference(paramodulation,[status(thm)],[f775,f805]) ).
fof(f2606,plain,
! [X0,X1] : join(complement(X0),X1) = complement(meet(X0,complement(X1))),
inference(paramodulation,[status(thm)],[f775,f805]) ).
fof(f2610,plain,
! [X0,X1] : X0 = join(X0,complement(complement(meet(X0,X1)))),
inference(paramodulation,[status(thm)],[f805,f2062]) ).
fof(f2615,plain,
! [X0,X1] : X0 = join(X0,complement(complement(meet(X1,X0)))),
inference(paramodulation,[status(thm)],[f805,f2468]) ).
fof(f2647,plain,
! [X0,X1] : X0 = join(X0,meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f775,f2610]) ).
fof(f2655,plain,
! [X0,X1] : X0 = join(X0,meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f775,f2615]) ).
fof(f2766,plain,
! [X0,X1,X2] : join(X0,join(X1,meet(X0,X2))) = join(X1,X0),
inference(paramodulation,[status(thm)],[f2647,f58]) ).
fof(f2791,plain,
! [X0,X1,X2] : join(X0,X1) = join(X0,join(X1,meet(X2,join(X0,X1)))),
inference(paramodulation,[status(thm)],[f17,f2655]) ).
fof(f2804,plain,
! [X0,X1] : converse(converse(X0)) = join(X0,converse(meet(X1,converse(X0)))),
inference(paramodulation,[status(thm)],[f2655,f81]) ).
fof(f2812,plain,
! [X0,X1,X2] : join(X0,join(X1,meet(X2,X0))) = join(X1,X0),
inference(paramodulation,[status(thm)],[f2655,f58]) ).
fof(f2820,plain,
! [X0,X1] : X0 = join(X0,converse(meet(X1,converse(X0)))),
inference(forward_demodulation,[status(thm)],[f23,f2804]) ).
fof(f2836,plain,
! [X0] : complement(converse(complement(X0))) = join(complement(converse(complement(X0))),converse(X0)),
inference(paramodulation,[status(thm)],[f2179,f2820]) ).
fof(f2865,plain,
! [X0,X1,X2] : join(X0,join(converse(meet(X1,converse(X0))),X2)) = join(X2,X0),
inference(paramodulation,[status(thm)],[f2820,f48]) ).
fof(f2872,plain,
! [X0] : complement(converse(complement(X0))) = join(converse(X0),complement(converse(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f16,f2836]) ).
fof(f3055,plain,
! [X0,X1,X2] : join(meet(X0,X1),join(X2,meet(X1,X0))) = join(X2,meet(X1,X0)),
inference(paramodulation,[status(thm)],[f1984,f58]) ).
fof(f3058,plain,
! [X0,X1,X2] : join(X0,meet(X1,X2)) = join(meet(X1,X2),join(X0,meet(X2,X1))),
inference(paramodulation,[status(thm)],[f1984,f48]) ).
fof(f3084,plain,
! [X0,X1,X2] : join(X0,meet(X1,X2)) = join(X0,meet(X2,X1)),
inference(forward_demodulation,[status(thm)],[f3055,f3058]) ).
fof(f3166,plain,
! [X0] : join(X0,complement(converse(complement(converse(complement(complement(X0))))))) = complement(complement(X0)),
inference(paramodulation,[status(thm)],[f2179,f2603]) ).
fof(f3198,plain,
! [X0] : join(X0,complement(converse(complement(converse(X0))))) = complement(complement(X0)),
inference(forward_demodulation,[status(thm)],[f775,f3166]) ).
fof(f3199,plain,
! [X0] : join(X0,complement(converse(complement(converse(X0))))) = X0,
inference(forward_demodulation,[status(thm)],[f775,f3198]) ).
fof(f3522,plain,
sK2_skl = join(meet(sK2_skl,converse(complement(converse(composition(complement(sK0_skl),sK1_skl))))),complement(top)),
inference(paramodulation,[status(thm)],[f2152,f42]) ).
fof(f3533,plain,
sK2_skl = join(complement(top),meet(sK2_skl,converse(complement(converse(composition(complement(sK0_skl),sK1_skl)))))),
inference(forward_demodulation,[status(thm)],[f16,f3522]) ).
fof(f3534,plain,
sK2_skl = join(zero,meet(sK2_skl,converse(complement(converse(composition(complement(sK0_skl),sK1_skl)))))),
inference(forward_demodulation,[status(thm)],[f287,f3533]) ).
fof(f3536,plain,
sK2_skl = meet(sK2_skl,converse(complement(converse(composition(complement(sK0_skl),sK1_skl))))),
inference(forward_demodulation,[status(thm)],[f763,f3534]) ).
fof(f3547,plain,
converse(complement(converse(composition(complement(sK0_skl),sK1_skl)))) = join(converse(complement(converse(composition(complement(sK0_skl),sK1_skl)))),sK2_skl),
inference(paramodulation,[status(thm)],[f3536,f2655]) ).
fof(f3560,plain,
converse(complement(converse(composition(complement(sK0_skl),sK1_skl)))) = join(sK2_skl,converse(complement(converse(composition(complement(sK0_skl),sK1_skl))))),
inference(forward_demodulation,[status(thm)],[f16,f3547]) ).
fof(f3730,plain,
! [X0] : join(converse(X0),complement(converse(complement(X0)))) = converse(X0),
inference(paramodulation,[status(thm)],[f23,f3199]) ).
fof(f3775,plain,
! [X0] : complement(converse(complement(X0))) = converse(X0),
inference(forward_demodulation,[status(thm)],[f2872,f3730]) ).
fof(f3855,plain,
! [X0] : complement(converse(X0)) = converse(complement(X0)),
inference(paramodulation,[status(thm)],[f775,f3775]) ).
fof(f3893,plain,
converse(complement(converse(composition(complement(sK0_skl),sK1_skl)))) = join(sK2_skl,complement(converse(converse(composition(complement(sK0_skl),sK1_skl))))),
inference(backward_demodulation,[status(thm)],[f3855,f3560]) ).
fof(f3948,plain,
complement(converse(converse(composition(complement(sK0_skl),sK1_skl)))) = join(sK2_skl,complement(converse(converse(composition(complement(sK0_skl),sK1_skl))))),
inference(forward_demodulation,[status(thm)],[f3855,f3893]) ).
fof(f3949,plain,
complement(composition(complement(sK0_skl),sK1_skl)) = join(sK2_skl,complement(converse(converse(composition(complement(sK0_skl),sK1_skl))))),
inference(forward_demodulation,[status(thm)],[f23,f3948]) ).
fof(f3950,plain,
complement(composition(complement(sK0_skl),sK1_skl)) = join(sK2_skl,complement(composition(complement(sK0_skl),sK1_skl))),
inference(forward_demodulation,[status(thm)],[f23,f3949]) ).
fof(f3975,plain,
! [X0,X1] : converse(join(X0,complement(converse(X1)))) = join(converse(X0),complement(X1)),
inference(paramodulation,[status(thm)],[f3855,f83]) ).
fof(f3979,plain,
! [X0,X1] : converse(composition(X0,complement(converse(X1)))) = composition(complement(X1),converse(X0)),
inference(paramodulation,[status(thm)],[f3855,f63]) ).
fof(f3984,plain,
! [X0,X1] : converse(composition(complement(X0),X1)) = composition(converse(X1),complement(converse(X0))),
inference(paramodulation,[status(thm)],[f3855,f25]) ).
fof(f4030,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(X1)),
inference(paramodulation,[status(thm)],[f2606,f775]) ).
fof(f4172,plain,
! [X0,X1] : join(complement(X0),X1) = join(meet(X0,X1),complement(X0)),
inference(paramodulation,[status(thm)],[f711,f2766]) ).
fof(f4216,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f16,f4172]) ).
fof(f4696,plain,
! [X0,X1] : join(X0,composition(X1,complement(composition(converse(X1),complement(X0))))) = complement(complement(X0)),
inference(paramodulation,[status(thm)],[f775,f167]) ).
fof(f4730,plain,
! [X0,X1] : join(X0,composition(X1,complement(composition(converse(X1),complement(X0))))) = X0,
inference(forward_demodulation,[status(thm)],[f775,f4696]) ).
fof(f4761,plain,
! [X0,X1] : complement(complement(X0)) = meet(X0,complement(meet(complement(X0),X1))),
inference(paramodulation,[status(thm)],[f2647,f4030]) ).
fof(f4820,plain,
! [X0,X1] : X0 = meet(X0,complement(meet(complement(X0),X1))),
inference(forward_demodulation,[status(thm)],[f775,f4761]) ).
fof(f4822,plain,
! [X0,X1] : X0 = meet(X0,join(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f2603,f4820]) ).
fof(f4888,plain,
! [X0,X1] : X0 = meet(X0,join(X0,X1)),
inference(paramodulation,[status(thm)],[f775,f4822]) ).
fof(f4943,plain,
! [X0,X1,X2] : composition(X0,X1) = meet(composition(X0,X1),composition(join(X0,X2),X1)),
inference(paramodulation,[status(thm)],[f22,f4888]) ).
fof(f4969,plain,
! [X0,X1] : X0 = meet(X0,join(X1,X0)),
inference(paramodulation,[status(thm)],[f2812,f4888]) ).
fof(f5151,plain,
! [X0,X1,X2] : join(X0,X1) = meet(join(X0,X1),join(X0,join(X2,X1))),
inference(paramodulation,[status(thm)],[f58,f4969]) ).
fof(f6299,plain,
! [X0,X1] : join(complement(complement(X0)),X1) = join(X0,meet(complement(X0),X1)),
inference(paramodulation,[status(thm)],[f775,f4216]) ).
fof(f6314,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(meet(X0,X1))),
inference(paramodulation,[status(thm)],[f4216,f4030]) ).
fof(f6339,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),X1)),
inference(forward_demodulation,[status(thm)],[f775,f6299]) ).
fof(f6356,plain,
! [X0,X1] : meet(X0,complement(X1)) = meet(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f4030,f6314]) ).
fof(f6382,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(X1,complement(X0))),
inference(paramodulation,[status(thm)],[f291,f6339]) ).
fof(f6502,plain,
! [X0,X1,X2] : join(X0,join(X1,meet(X2,complement(X0)))) = join(X1,join(X0,X2)),
inference(paramodulation,[status(thm)],[f6382,f58]) ).
fof(f6637,plain,
! [X0,X1] : meet(X0,complement(complement(X1))) = meet(X0,join(complement(X0),X1)),
inference(paramodulation,[status(thm)],[f2606,f6356]) ).
fof(f6679,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),X1)),
inference(forward_demodulation,[status(thm)],[f775,f6637]) ).
fof(f6792,plain,
! [X0,X1,X2] : meet(X0,join(X1,X2)) = meet(X0,join(X1,join(complement(X0),X2))),
inference(paramodulation,[status(thm)],[f58,f6679]) ).
fof(f12560,plain,
! [X0,X1] : converse(converse(X0)) = join(X0,converse(composition(X1,complement(composition(converse(X1),complement(converse(X0))))))),
inference(paramodulation,[status(thm)],[f4730,f81]) ).
fof(f12615,plain,
! [X0,X1] : X0 = join(X0,converse(composition(X1,complement(composition(converse(X1),complement(converse(X0))))))),
inference(forward_demodulation,[status(thm)],[f23,f12560]) ).
fof(f12616,plain,
! [X0,X1] : X0 = join(X0,converse(composition(X1,complement(converse(composition(complement(X0),X1)))))),
inference(forward_demodulation,[status(thm)],[f3984,f12615]) ).
fof(f12617,plain,
! [X0,X1] : X0 = join(X0,composition(complement(composition(complement(X0),X1)),converse(X1))),
inference(forward_demodulation,[status(thm)],[f3979,f12616]) ).
fof(f12789,plain,
! [X0] : composition(sK2_skl,X0) = meet(composition(sK2_skl,X0),composition(complement(composition(complement(sK0_skl),sK1_skl)),X0)),
inference(paramodulation,[status(thm)],[f3950,f4943]) ).
fof(f16121,plain,
! [X0,X1,X2] : join(X0,meet(X1,join(X0,X2))) = meet(join(X0,meet(X1,join(X0,X2))),join(X0,X2)),
inference(paramodulation,[status(thm)],[f2791,f5151]) ).
fof(f16334,plain,
! [X0,X1,X2] : join(X0,meet(X1,join(X0,X2))) = meet(join(X0,X2),join(X0,meet(X1,join(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f291,f16121]) ).
fof(f25524,plain,
! [X0,X1,X2] : join(X0,join(converse(meet(X1,converse(X0))),X2)) = join(meet(X2,complement(converse(meet(X1,converse(X0))))),X0),
inference(paramodulation,[status(thm)],[f6382,f2865]) ).
fof(f25723,plain,
! [X0,X1,X2] : join(X0,X1) = join(meet(X0,complement(converse(meet(X2,converse(X1))))),X1),
inference(forward_demodulation,[status(thm)],[f2865,f25524]) ).
fof(f25724,plain,
! [X0,X1,X2] : join(X0,X1) = join(X1,meet(X0,complement(converse(meet(X2,converse(X1)))))),
inference(forward_demodulation,[status(thm)],[f16,f25723]) ).
fof(f27833,plain,
! [X0,X1] : converse(complement(meet(X0,converse(X1)))) = join(converse(complement(X0)),complement(X1)),
inference(paramodulation,[status(thm)],[f805,f3975]) ).
fof(f27941,plain,
! [X0,X1] : complement(converse(meet(X0,converse(X1)))) = join(converse(complement(X0)),complement(X1)),
inference(forward_demodulation,[status(thm)],[f3855,f27833]) ).
fof(f27942,plain,
! [X0,X1] : complement(converse(meet(X0,converse(X1)))) = join(complement(converse(X0)),complement(X1)),
inference(forward_demodulation,[status(thm)],[f3855,f27941]) ).
fof(f27946,plain,
! [X0,X1,X2] : join(X0,X1) = join(X1,meet(X0,complement(meet(converse(X2),X1)))),
inference(backward_demodulation,[status(thm)],[f27950,f25724]) ).
fof(f27950,plain,
! [X0,X1] : complement(converse(meet(X0,converse(X1)))) = complement(meet(converse(X0),X1)),
inference(forward_demodulation,[status(thm)],[f805,f27942]) ).
fof(f43068,plain,
! [X0,X1,X2] : join(X0,X1) = join(X1,meet(X0,complement(meet(X2,X1)))),
inference(paramodulation,[status(thm)],[f23,f27946]) ).
fof(f43387,plain,
! [X0,X1,X2] : join(X0,X1) = join(X1,meet(X0,join(X2,complement(X1)))),
inference(paramodulation,[status(thm)],[f2603,f43068]) ).
fof(f56497,plain,
! [X0,X1,X2] : meet(X0,join(X1,meet(X2,complement(complement(X0))))) = meet(X0,join(X1,join(complement(X0),X2))),
inference(paramodulation,[status(thm)],[f6502,f6679]) ).
fof(f56734,plain,
! [X0,X1,X2] : meet(X0,join(X1,meet(X2,X0))) = meet(X0,join(X1,join(complement(X0),X2))),
inference(forward_demodulation,[status(thm)],[f775,f56497]) ).
fof(f56735,plain,
! [X0,X1,X2] : join(X0,meet(X1,join(X0,X2))) = meet(join(X0,X2),join(X0,X1)),
inference(backward_demodulation,[status(thm)],[f56739,f16334]) ).
fof(f56739,plain,
! [X0,X1,X2] : meet(X0,join(X1,meet(X2,X0))) = meet(X0,join(X1,X2)),
inference(forward_demodulation,[status(thm)],[f6792,f56734]) ).
fof(f56908,plain,
! [X0,X1,X2] : join(X0,X1) = join(X0,meet(join(X2,X1),join(X0,X1))),
inference(backward_demodulation,[status(thm)],[f56735,f5151]) ).
fof(f57198,plain,
! [X0,X1,X2] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(X1,X2)),
inference(paramodulation,[status(thm)],[f3084,f56739]) ).
fof(f57560,plain,
! [X0,X1] : meet(composition(sK2_skl,X0),join(X1,composition(sK2_skl,X0))) = meet(composition(sK2_skl,X0),join(X1,composition(complement(composition(complement(sK0_skl),sK1_skl)),X0))),
inference(paramodulation,[status(thm)],[f12789,f57198]) ).
fof(f57735,plain,
! [X0,X1] : composition(sK2_skl,X0) = meet(composition(sK2_skl,X0),join(X1,composition(complement(composition(complement(sK0_skl),sK1_skl)),X0))),
inference(forward_demodulation,[status(thm)],[f4969,f57560]) ).
fof(f58001,plain,
! [X0,X1,X2] : join(meet(X0,X1),meet(complement(X1),X0)) = join(meet(X0,X1),meet(join(X2,meet(complement(X1),X0)),X0)),
inference(paramodulation,[status(thm)],[f682,f56908]) ).
fof(f58526,plain,
! [X0,X1,X2] : X0 = join(meet(X0,X1),meet(join(X2,meet(complement(X1),X0)),X0)),
inference(forward_demodulation,[status(thm)],[f682,f58001]) ).
fof(f58527,plain,
! [X0,X1,X2] : X0 = join(meet(X0,X1),meet(X0,join(X2,meet(complement(X1),X0)))),
inference(forward_demodulation,[status(thm)],[f3084,f58526]) ).
fof(f58528,plain,
! [X0,X1,X2] : X0 = join(meet(X0,X1),meet(X0,join(X2,complement(X1)))),
inference(forward_demodulation,[status(thm)],[f56739,f58527]) ).
fof(f63056,plain,
composition(sK2_skl,converse(sK1_skl)) = meet(composition(sK2_skl,converse(sK1_skl)),sK0_skl),
inference(paramodulation,[status(thm)],[f12617,f57735]) ).
fof(f63121,plain,
composition(sK2_skl,converse(sK1_skl)) = meet(sK0_skl,composition(sK2_skl,converse(sK1_skl))),
inference(forward_demodulation,[status(thm)],[f291,f63056]) ).
fof(f63196,plain,
! [X0] : sK0_skl = join(composition(sK2_skl,converse(sK1_skl)),meet(sK0_skl,join(X0,complement(composition(sK2_skl,converse(sK1_skl)))))),
inference(paramodulation,[status(thm)],[f63121,f58528]) ).
fof(f63228,plain,
sK0_skl = join(sK0_skl,composition(sK2_skl,converse(sK1_skl))),
inference(forward_demodulation,[status(thm)],[f43387,f63196]) ).
fof(f63229,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f63228,f41]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL044+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 04:08:27 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 187.44/24.11 % Refutation found
% 187.44/24.11 % SZS status Theorem for theBenchmark: Theorem is valid
% 187.44/24.11 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 106.46/24.30 % Elapsed time: 23.924896 seconds
% 106.46/24.30 % CPU time: 189.453250 seconds
% 106.46/24.30 % Total memory used: 893.448 MB
% 106.46/24.30 % Net memory used: 855.486 MB
%------------------------------------------------------------------------------