%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL004-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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:31 PM UTC 2026
% Result : Unsatisfiable 6.34s 1.35s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL004-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n013.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 03:57:06 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.47 % Drodi V4.1.1
% 6.34/1.35 % Refutation found
% 6.34/1.35 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 6.34/1.35 % SZS output start CNFRefutation for theBenchmark
% 6.34/1.35 fof(f1,axiom,(
% 6.34/1.35 (![A,B]: (join(A,B) = join(B,A) ))),
% 6.34/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.34/1.35 fof(f2,axiom,(
% 6.34/1.35 (![A,B,C]: (join(A,join(B,C)) = join(join(A,B),C) ))),
% 6.34/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.34/1.35 fof(f3,axiom,(
% 6.34/1.35 (![A,B]: (A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))) ))),
% 6.34/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.34/1.35 fof(f4,axiom,(
% 6.34/1.35 (![A,B]: (meet(A,B) = complement(join(complement(A),complement(B))) ))),
% 6.34/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.34/1.35 fof(f6,axiom,(
% 6.34/1.35 (![A]: (composition(A,one) = A ))),
% 6.34/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.34/1.35 fof(f8,axiom,(
% 6.34/1.35 (![A]: (converse(converse(A)) = A ))),
% 6.34/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.34/1.35 fof(f9,axiom,(
% 6.34/1.35 (![A,B]: (converse(join(A,B)) = join(converse(A),converse(B)) ))),
% 6.34/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.34/1.35 fof(f10,axiom,(
% 6.34/1.35 (![A,B]: (converse(composition(A,B)) = composition(converse(B),converse(A)) ))),
% 6.34/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.34/1.35 fof(f11,axiom,(
% 6.34/1.35 (![A,B]: (join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B) ))),
% 6.34/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.34/1.35 fof(f12,axiom,(
% 6.34/1.35 (![A]: (top = join(A,complement(A)) ))),
% 6.34/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.34/1.35 fof(f13,axiom,(
% 6.34/1.35 (![A]: (zero = meet(A,complement(A)) ))),
% 6.34/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.34/1.35 fof(f17,negated_conjecture,(
% 6.34/1.35 converse(complement(sk1)) != complement(converse(sk1)) ),
% 6.34/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.34/1.35 fof(f18,plain,(
% 6.34/1.35 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 6.34/1.35 inference(cnf_transformation,[status(thm)],[f1])).
% 6.34/1.35 fof(f19,plain,(
% 6.34/1.35 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 6.34/1.35 inference(cnf_transformation,[status(thm)],[f2])).
% 6.34/1.35 fof(f20,plain,(
% 6.34/1.35 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 6.34/1.35 inference(cnf_transformation,[status(thm)],[f3])).
% 6.34/1.35 fof(f21,plain,(
% 6.34/1.35 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 6.34/1.35 inference(cnf_transformation,[status(thm)],[f4])).
% 6.34/1.35 fof(f23,plain,(
% 6.34/1.35 ![X0]: (composition(X0,one)=X0)),
% 6.34/1.35 inference(cnf_transformation,[status(thm)],[f6])).
% 6.34/1.35 fof(f25,plain,(
% 6.34/1.35 ![X0]: (converse(converse(X0))=X0)),
% 6.34/1.35 inference(cnf_transformation,[status(thm)],[f8])).
% 6.34/1.35 fof(f26,plain,(
% 6.34/1.35 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 6.34/1.35 inference(cnf_transformation,[status(thm)],[f9])).
% 6.34/1.35 fof(f27,plain,(
% 6.34/1.35 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 6.34/1.35 inference(cnf_transformation,[status(thm)],[f10])).
% 6.34/1.35 fof(f28,plain,(
% 6.34/1.35 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 6.34/1.35 inference(cnf_transformation,[status(thm)],[f11])).
% 6.34/1.35 fof(f29,plain,(
% 6.34/1.35 ![X0]: (top=join(X0,complement(X0)))),
% 6.34/1.35 inference(cnf_transformation,[status(thm)],[f12])).
% 6.34/1.35 fof(f30,plain,(
% 6.34/1.35 ![X0]: (zero=meet(X0,complement(X0)))),
% 6.34/1.35 inference(cnf_transformation,[status(thm)],[f13])).
% 6.34/1.35 fof(f34,plain,(
% 6.34/1.35 ~converse(complement(sk1))=complement(converse(sk1))),
% 6.34/1.35 inference(cnf_transformation,[status(thm)],[f17])).
% 6.34/1.35 fof(f40,plain,(
% 6.34/1.35 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 6.34/1.35 inference(backward_demodulation,[status(thm)],[f21,f20])).
% 6.34/1.35 fof(f42,plain,(
% 6.34/1.35 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X0,X1),complement(X2))))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f21,f21])).
% 6.34/1.35 fof(f43,plain,(
% 6.34/1.35 ![X0,X1,X2]: (meet(X0,join(complement(X1),complement(X2)))=complement(join(complement(X0),meet(X1,X2))))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f21,f21])).
% 6.34/1.35 fof(f44,plain,(
% 6.34/1.35 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f25,f26])).
% 6.34/1.35 fof(f47,plain,(
% 6.34/1.35 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f25,f27])).
% 6.34/1.35 fof(f63,plain,(
% 6.34/1.35 ![X0,X1]: (join(composition(X0,complement(composition(converse(X0),X1))),complement(X1))=complement(X1))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f25,f28])).
% 6.34/1.35 fof(f196,plain,(
% 6.34/1.35 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f21,f40])).
% 6.34/1.35 fof(f379,plain,(
% 6.34/1.35 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f23,f47])).
% 6.34/1.35 fof(f382,plain,(
% 6.34/1.35 ![X0]: (X0=composition(converse(one),X0))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f25,f379])).
% 6.34/1.35 fof(f385,plain,(
% 6.34/1.35 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f29,f44])).
% 6.34/1.35 fof(f391,plain,(
% 6.34/1.35 ![X0,X1]: (meet(top,X0)=complement(join(meet(X1,complement(X1)),complement(X0))))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f29,f42])).
% 6.34/1.35 fof(f392,plain,(
% 6.34/1.35 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f29,f21])).
% 6.34/1.35 fof(f403,plain,(
% 6.34/1.35 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f30,f391])).
% 6.34/1.35 fof(f404,plain,(
% 6.34/1.35 zero=complement(top)),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f30,f392])).
% 6.34/1.35 fof(f436,plain,(
% 6.34/1.35 one=converse(one)),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f23,f382])).
% 6.34/1.35 fof(f440,plain,(
% 6.34/1.35 ![X0]: (join(composition(one,complement(X0)),complement(X0))=complement(X0))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f382,f63])).
% 6.34/1.35 fof(f449,plain,(
% 6.34/1.35 ![X0]: (X0=composition(one,X0))),
% 6.34/1.35 inference(backward_demodulation,[status(thm)],[f436,f382])).
% 6.34/1.35 fof(f462,plain,(
% 6.34/1.35 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 6.34/1.35 inference(backward_demodulation,[status(thm)],[f449,f440])).
% 6.34/1.35 fof(f530,plain,(
% 6.34/1.35 ![X0,X1]: (meet(X0,join(zero,complement(X1)))=complement(join(complement(X0),meet(top,X1))))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f404,f43])).
% 6.34/1.35 fof(f562,plain,(
% 6.34/1.35 ![X0]: (X0=join(meet(X0,complement(X0)),complement(complement(X0))))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f462,f40])).
% 6.34/1.35 fof(f580,plain,(
% 6.34/1.35 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f30,f562])).
% 6.34/1.35 fof(f583,plain,(
% 6.34/1.35 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(meet(X0,X1))))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f21,f580])).
% 6.34/1.35 fof(f642,plain,(
% 6.34/1.35 ![X0]: (X0=join(meet(X0,converse(complement(converse(complement(X0))))),complement(converse(top))))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f385,f40])).
% 6.34/1.35 fof(f697,plain,(
% 6.34/1.35 ![X0,X1]: (join(X0,join(X1,complement(join(X0,X1))))=top)),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f29,f19])).
% 6.34/1.35 fof(f699,plain,(
% 6.34/1.35 ![X0,X1]: (join(zero,join(complement(complement(X0)),X1))=join(X0,X1))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f580,f19])).
% 6.34/1.35 fof(f712,plain,(
% 6.34/1.35 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f29,f19])).
% 6.34/1.35 fof(f721,plain,(
% 6.34/1.35 ![X0]: (join(zero,complement(complement(X0)))=join(X0,complement(complement(X0))))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f462,f699])).
% 6.34/1.35 fof(f728,plain,(
% 6.34/1.35 ![X0]: (X0=join(X0,complement(complement(X0))))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f580,f721])).
% 6.34/1.35 fof(f739,plain,(
% 6.34/1.35 ![X0]: (converse(converse(X0))=join(X0,converse(complement(complement(converse(X0))))))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f728,f44])).
% 6.34/1.35 fof(f740,plain,(
% 6.34/1.35 ![X0]: (join(zero,complement(complement(X0)))=join(X0,complement(complement(complement(complement(X0))))))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f728,f699])).
% 6.34/1.35 fof(f753,plain,(
% 6.34/1.35 ![X0]: (X0=join(X0,converse(complement(complement(converse(X0))))))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f25,f739])).
% 6.34/1.35 fof(f754,plain,(
% 6.34/1.35 ![X0]: (X0=join(X0,complement(complement(complement(complement(X0))))))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f580,f740])).
% 6.34/1.35 fof(f778,plain,(
% 6.34/1.35 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f26,f18])).
% 6.34/1.35 fof(f814,plain,(
% 6.34/1.35 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f18,f21])).
% 6.34/1.35 fof(f1350,plain,(
% 6.34/1.35 ![X0]: (converse(join(complement(complement(converse(converse(X0)))),X0))=converse(X0))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f753,f778])).
% 6.34/1.35 fof(f1374,plain,(
% 6.34/1.35 ![X0]: (converse(join(complement(complement(X0)),X0))=converse(X0))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f25,f1350])).
% 6.34/1.35 fof(f1407,plain,(
% 6.34/1.35 ![X0]: (converse(top)=join(join(complement(complement(X0)),X0),converse(complement(converse(X0)))))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f1374,f385])).
% 6.34/1.35 fof(f1420,plain,(
% 6.34/1.35 ![X0]: (converse(converse(X0))=join(complement(complement(X0)),X0))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f1374,f25])).
% 6.34/1.35 fof(f1431,plain,(
% 6.34/1.35 ![X0]: (converse(top)=join(complement(complement(X0)),join(X0,converse(complement(converse(X0))))))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f19,f1407])).
% 6.34/1.35 fof(f1432,plain,(
% 6.34/1.35 ![X0]: (converse(top)=join(complement(complement(X0)),converse(top)))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f385,f1431])).
% 6.34/1.35 fof(f1458,plain,(
% 6.34/1.35 ![X0]: (X0=join(complement(complement(X0)),X0))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f25,f1420])).
% 6.34/1.35 fof(f1470,plain,(
% 6.34/1.35 ![X0]: (join(zero,X0)=join(X0,X0))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f1458,f699])).
% 6.34/1.35 fof(f1482,plain,(
% 6.34/1.35 ![X0]: (complement(X0)=join(meet(complement(X0),X0),complement(X0)))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f1458,f40])).
% 6.34/1.35 fof(f1581,plain,(
% 6.34/1.35 ![X0]: (complement(X0)=join(complement(X0),meet(complement(X0),X0)))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f18,f1482])).
% 6.34/1.35 fof(f1621,plain,(
% 6.34/1.35 ![X0]: (join(zero,complement(complement(X0)))=join(X0,meet(complement(complement(X0)),complement(X0))))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f1581,f699])).
% 6.34/1.35 fof(f1647,plain,(
% 6.34/1.35 ![X0]: (X0=join(X0,meet(complement(complement(X0)),complement(X0))))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f580,f1621])).
% 6.34/1.35 fof(f1690,plain,(
% 6.34/1.35 ![X0]: (join(zero,complement(X0))=complement(X0))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f462,f1470])).
% 6.34/1.35 fof(f1715,plain,(
% 6.34/1.35 ![X0]: (X0=join(meet(X0,complement(X0)),complement(join(zero,complement(X0)))))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f1470,f40])).
% 6.34/1.35 fof(f1719,plain,(
% 6.34/1.35 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 6.34/1.35 inference(backward_demodulation,[status(thm)],[f1690,f583])).
% 6.34/1.35 fof(f1721,plain,(
% 6.34/1.35 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),meet(top,X1))))),
% 6.34/1.35 inference(backward_demodulation,[status(thm)],[f1690,f530])).
% 6.34/1.35 fof(f1725,plain,(
% 6.34/1.35 ![X0]: (meet(top,X0)=complement(complement(X0)))),
% 6.34/1.35 inference(backward_demodulation,[status(thm)],[f1690,f403])).
% 6.34/1.35 fof(f1750,plain,(
% 6.34/1.35 ![X0]: (X0=join(zero,complement(join(zero,complement(X0)))))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f30,f1715])).
% 6.34/1.35 fof(f1751,plain,(
% 6.34/1.35 ![X0]: (X0=complement(join(zero,complement(X0))))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f1690,f1750])).
% 6.34/1.35 fof(f1752,plain,(
% 6.34/1.35 ![X0]: (X0=join(X0,complement(complement(X0))))),
% 6.34/1.35 inference(backward_demodulation,[status(thm)],[f1826,f754])).
% 6.34/1.35 fof(f1757,plain,(
% 6.34/1.35 ![X0]: (X0=join(X0,meet(X0,complement(X0))))),
% 6.34/1.35 inference(backward_demodulation,[status(thm)],[f1826,f1647])).
% 6.34/1.35 fof(f1818,plain,(
% 6.34/1.35 ![X0]: (converse(top)=join(X0,converse(top)))),
% 6.34/1.35 inference(backward_demodulation,[status(thm)],[f1826,f1432])).
% 6.34/1.35 fof(f1826,plain,(
% 6.34/1.35 ![X0]: (X0=complement(complement(X0)))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f1690,f1751])).
% 6.34/1.35 fof(f1856,plain,(
% 6.34/1.35 ![X0,X1]: (meet(X0,X1)=complement(complement(meet(X1,X0))))),
% 6.34/1.35 inference(backward_demodulation,[status(thm)],[f1719,f814])).
% 6.34/1.35 fof(f1885,plain,(
% 6.34/1.35 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),X1)))),
% 6.34/1.35 inference(backward_demodulation,[status(thm)],[f1888,f1721])).
% 6.34/1.35 fof(f1888,plain,(
% 6.34/1.35 ![X0]: (meet(top,X0)=X0)),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f1826,f1725])).
% 6.34/1.35 fof(f1901,plain,(
% 6.34/1.35 ![X0]: (join(zero,X0)=X0)),
% 6.34/1.35 inference(backward_demodulation,[status(thm)],[f1908,f1470])).
% 6.34/1.35 fof(f1908,plain,(
% 6.34/1.35 ![X0]: (X0=join(X0,X0))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f1826,f1752])).
% 6.34/1.35 fof(f1922,plain,(
% 6.34/1.35 ![X0]: (X0=join(X0,zero))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f30,f1757])).
% 6.34/1.35 fof(f2074,plain,(
% 6.34/1.35 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f1826,f1856])).
% 6.34/1.35 fof(f2483,plain,(
% 6.34/1.35 ![X0,X1]: (X0=join(meet(complement(X1),X0),meet(X0,X1)))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f2074,f196])).
% 6.34/1.35 fof(f2545,plain,(
% 6.34/1.35 ![X0,X1]: (X0=join(meet(complement(X1),X0),meet(X1,X0)))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f2074,f2483])).
% 6.34/1.35 fof(f2715,plain,(
% 6.34/1.35 ![X0]: (join(X0,converse(top))=join(top,converse(complement(converse(complement(X0))))))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f385,f712])).
% 6.34/1.35 fof(f2718,plain,(
% 6.34/1.35 ![X0,X1]: (join(X0,join(X1,complement(X0)))=join(top,X1))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f18,f712])).
% 6.34/1.35 fof(f2730,plain,(
% 6.34/1.35 ![X0]: (converse(top)=join(top,converse(complement(converse(complement(X0))))))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f1818,f2715])).
% 6.34/1.35 fof(f2934,plain,(
% 6.34/1.35 ![X0]: (join(X0,join(X0,complement(X0)))=top)),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f1908,f697])).
% 6.34/1.35 fof(f2983,plain,(
% 6.34/1.35 converse(top)=top),
% 6.34/1.35 inference(backward_demodulation,[status(thm)],[f2993,f2730])).
% 6.34/1.35 fof(f2993,plain,(
% 6.34/1.35 ![X0]: (join(top,X0)=top)),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f2718,f2934])).
% 6.34/1.35 fof(f3012,plain,(
% 6.34/1.35 ![X0]: (top=join(X0,converse(complement(converse(X0)))))),
% 6.34/1.35 inference(backward_demodulation,[status(thm)],[f2983,f385])).
% 6.34/1.35 fof(f3021,plain,(
% 6.34/1.35 ![X0]: (X0=join(meet(X0,converse(complement(converse(complement(X0))))),complement(top)))),
% 6.34/1.35 inference(backward_demodulation,[status(thm)],[f2983,f642])).
% 6.34/1.35 fof(f3051,plain,(
% 6.34/1.35 ![X0]: (X0=join(meet(X0,converse(complement(converse(complement(X0))))),zero))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f404,f3021])).
% 6.34/1.35 fof(f3052,plain,(
% 6.34/1.35 ![X0]: (X0=meet(X0,converse(complement(converse(complement(X0))))))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f1922,f3051])).
% 6.34/1.35 fof(f3583,plain,(
% 6.34/1.35 ![X0,X1]: (join(X0,complement(X1))=complement(meet(complement(X0),X1)))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f1826,f1719])).
% 6.34/1.35 fof(f3695,plain,(
% 6.34/1.35 ![X0,X1]: (meet(complement(X0),complement(X1))=complement(join(X0,X1)))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f1826,f1885])).
% 6.34/1.35 fof(f3800,plain,(
% 6.34/1.35 ![X0]: (join(X0,complement(converse(complement(converse(complement(complement(X0)))))))=complement(complement(X0)))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f3052,f3583])).
% 6.34/1.35 fof(f3839,plain,(
% 6.34/1.35 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=complement(complement(X0)))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f1826,f3800])).
% 6.34/1.35 fof(f3840,plain,(
% 6.34/1.35 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=X0)),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f1826,f3839])).
% 6.34/1.35 fof(f3887,plain,(
% 6.34/1.35 ![X0]: (converse(converse(X0))=join(X0,converse(complement(converse(complement(converse(converse(X0))))))))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f3840,f44])).
% 6.34/1.35 fof(f3909,plain,(
% 6.34/1.35 ![X0]: (X0=join(X0,converse(complement(converse(complement(converse(converse(X0))))))))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f25,f3887])).
% 6.34/1.35 fof(f3910,plain,(
% 6.34/1.35 ![X0]: (X0=join(X0,converse(complement(converse(complement(X0))))))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f25,f3909])).
% 6.34/1.35 fof(f3933,plain,(
% 6.34/1.35 ![X0]: (meet(X0,complement(converse(complement(converse(complement(complement(X0)))))))=complement(complement(X0)))),
% 6.34/1.35 inference(paramodulation,[status(thm)],[f3910,f1885])).
% 6.34/1.35 fof(f3954,plain,(
% 6.34/1.35 ![X0]: (meet(X0,complement(converse(complement(converse(X0)))))=complement(complement(X0)))),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f1826,f3933])).
% 6.34/1.35 fof(f3955,plain,(
% 6.34/1.35 ![X0]: (meet(X0,complement(converse(complement(converse(X0)))))=X0)),
% 6.34/1.35 inference(forward_demodulation,[status(thm)],[f1826,f3954])).
% 6.34/1.35 fof(f3981,plain,(
% 6.34/1.35 ![X0]: (complement(converse(complement(converse(X0))))=join(meet(complement(X0),complement(converse(complement(converse(X0))))),X0))),
% 6.34/1.38 inference(paramodulation,[status(thm)],[f3955,f2545])).
% 6.34/1.38 fof(f4016,plain,(
% 6.34/1.38 ![X0]: (complement(converse(complement(converse(X0))))=join(complement(join(X0,converse(complement(converse(X0))))),X0))),
% 6.34/1.38 inference(forward_demodulation,[status(thm)],[f3695,f3981])).
% 6.34/1.38 fof(f4017,plain,(
% 6.34/1.38 ![X0]: (complement(converse(complement(converse(X0))))=join(complement(top),X0))),
% 6.34/1.38 inference(forward_demodulation,[status(thm)],[f3012,f4016])).
% 6.34/1.38 fof(f4018,plain,(
% 6.34/1.38 ![X0]: (complement(converse(complement(converse(X0))))=join(zero,X0))),
% 6.34/1.38 inference(forward_demodulation,[status(thm)],[f404,f4017])).
% 6.34/1.38 fof(f4029,plain,(
% 6.34/1.38 ![X0]: (complement(converse(complement(converse(X0))))=X0)),
% 6.34/1.38 inference(forward_demodulation,[status(thm)],[f1901,f4018])).
% 6.34/1.38 fof(f4093,plain,(
% 6.34/1.38 ![X0]: (converse(complement(converse(X0)))=complement(X0))),
% 6.34/1.38 inference(paramodulation,[status(thm)],[f4029,f1826])).
% 6.34/1.38 fof(f4386,plain,(
% 6.34/1.38 ![X0]: (converse(complement(X0))=complement(converse(X0)))),
% 6.34/1.38 inference(paramodulation,[status(thm)],[f25,f4093])).
% 6.34/1.38 fof(f4425,plain,(
% 6.34/1.38 ~complement(converse(sk1))=complement(converse(sk1))),
% 6.34/1.38 inference(backward_demodulation,[status(thm)],[f4386,f34])).
% 6.34/1.38 fof(f4454,plain,(
% 6.34/1.38 $false),
% 6.34/1.38 inference(trivial_equality_resolution,[status(thm)],[f4425])).
% 6.34/1.38 % SZS output end CNFRefutation for theBenchmark.p
% 6.34/1.40 % Elapsed time: 0.918297 seconds
% 6.34/1.40 % CPU time: 6.951323 seconds
% 6.34/1.40 % Total memory used: 138.385 MB
% 6.34/1.40 % Net memory used: 133.805 MB
%------------------------------------------------------------------------------