%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL006-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:32 PM UTC 2026
% Result : Unsatisfiable 19.17s 2.88s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL006-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n018.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 03:59:59 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 19.17/2.88 % Refutation found
% 19.17/2.88 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 19.17/2.88 % SZS output start CNFRefutation for theBenchmark
% 19.17/2.88 fof(f1,axiom,(
% 19.17/2.88 (![A,B]: (join(A,B) = join(B,A) ))),
% 19.17/2.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.17/2.88 fof(f2,axiom,(
% 19.17/2.88 (![A,B,C]: (join(A,join(B,C)) = join(join(A,B),C) ))),
% 19.17/2.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.17/2.88 fof(f3,axiom,(
% 19.17/2.88 (![A,B]: (A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))) ))),
% 19.17/2.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.17/2.88 fof(f4,axiom,(
% 19.17/2.88 (![A,B]: (meet(A,B) = complement(join(complement(A),complement(B))) ))),
% 19.17/2.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.17/2.88 fof(f6,axiom,(
% 19.17/2.88 (![A]: (composition(A,one) = A ))),
% 19.17/2.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.17/2.88 fof(f8,axiom,(
% 19.17/2.88 (![A]: (converse(converse(A)) = A ))),
% 19.17/2.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.17/2.88 fof(f9,axiom,(
% 19.17/2.88 (![A,B]: (converse(join(A,B)) = join(converse(A),converse(B)) ))),
% 19.17/2.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.17/2.88 fof(f10,axiom,(
% 19.17/2.88 (![A,B]: (converse(composition(A,B)) = composition(converse(B),converse(A)) ))),
% 19.17/2.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.17/2.88 fof(f11,axiom,(
% 19.17/2.88 (![A,B]: (join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B) ))),
% 19.17/2.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.17/2.88 fof(f12,axiom,(
% 19.17/2.88 (![A]: (top = join(A,complement(A)) ))),
% 19.17/2.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.17/2.88 fof(f13,axiom,(
% 19.17/2.88 (![A]: (zero = meet(A,complement(A)) ))),
% 19.17/2.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.17/2.88 fof(f14,negated_conjecture,(
% 19.17/2.88 meet(converse(sk1),sk2) = zero ),
% 19.17/2.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.17/2.88 fof(f15,negated_conjecture,(
% 19.17/2.88 meet(sk1,converse(sk2)) != zero ),
% 19.17/2.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.17/2.88 fof(f16,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 19.17/2.88 inference(cnf_transformation,[status(thm)],[f1])).
% 19.17/2.88 fof(f17,plain,(
% 19.17/2.88 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 19.17/2.88 inference(cnf_transformation,[status(thm)],[f2])).
% 19.17/2.88 fof(f18,plain,(
% 19.17/2.88 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 19.17/2.88 inference(cnf_transformation,[status(thm)],[f3])).
% 19.17/2.88 fof(f19,plain,(
% 19.17/2.88 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 19.17/2.88 inference(cnf_transformation,[status(thm)],[f4])).
% 19.17/2.88 fof(f21,plain,(
% 19.17/2.88 ![X0]: (composition(X0,one)=X0)),
% 19.17/2.88 inference(cnf_transformation,[status(thm)],[f6])).
% 19.17/2.88 fof(f23,plain,(
% 19.17/2.88 ![X0]: (converse(converse(X0))=X0)),
% 19.17/2.88 inference(cnf_transformation,[status(thm)],[f8])).
% 19.17/2.88 fof(f24,plain,(
% 19.17/2.88 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 19.17/2.88 inference(cnf_transformation,[status(thm)],[f9])).
% 19.17/2.88 fof(f25,plain,(
% 19.17/2.88 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 19.17/2.88 inference(cnf_transformation,[status(thm)],[f10])).
% 19.17/2.88 fof(f26,plain,(
% 19.17/2.88 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 19.17/2.88 inference(cnf_transformation,[status(thm)],[f11])).
% 19.17/2.88 fof(f27,plain,(
% 19.17/2.88 ![X0]: (top=join(X0,complement(X0)))),
% 19.17/2.88 inference(cnf_transformation,[status(thm)],[f12])).
% 19.17/2.88 fof(f28,plain,(
% 19.17/2.88 ![X0]: (zero=meet(X0,complement(X0)))),
% 19.17/2.88 inference(cnf_transformation,[status(thm)],[f13])).
% 19.17/2.88 fof(f29,plain,(
% 19.17/2.88 meet(converse(sk1),sk2)=zero),
% 19.17/2.88 inference(cnf_transformation,[status(thm)],[f14])).
% 19.17/2.88 fof(f30,plain,(
% 19.17/2.88 ~meet(sk1,converse(sk2))=zero),
% 19.17/2.88 inference(cnf_transformation,[status(thm)],[f15])).
% 19.17/2.88 fof(f34,plain,(
% 19.17/2.88 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f16,f18])).
% 19.17/2.88 fof(f35,plain,(
% 19.17/2.88 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 19.17/2.88 inference(backward_demodulation,[status(thm)],[f19,f34])).
% 19.17/2.88 fof(f36,plain,(
% 19.17/2.88 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f16,f26])).
% 19.17/2.88 fof(f37,plain,(
% 19.17/2.88 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f16,f35])).
% 19.17/2.88 fof(f39,plain,(
% 19.17/2.88 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X0,X1),complement(X2))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f19,f19])).
% 19.17/2.88 fof(f41,plain,(
% 19.17/2.88 ![X0,X1]: (zero=meet(join(complement(X0),complement(X1)),meet(X0,X1)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f19,f28])).
% 19.17/2.88 fof(f42,plain,(
% 19.17/2.88 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f23,f24])).
% 19.17/2.88 fof(f43,plain,(
% 19.17/2.88 ![X0,X1]: (converse(join(X0,converse(X1)))=join(converse(X0),X1))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f23,f24])).
% 19.17/2.88 fof(f45,plain,(
% 19.17/2.88 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f23,f25])).
% 19.17/2.88 fof(f46,plain,(
% 19.17/2.88 converse(sk1)=join(zero,complement(join(complement(converse(sk1)),sk2)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f29,f37])).
% 19.17/2.88 fof(f47,plain,(
% 19.17/2.88 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f28,f37])).
% 19.17/2.88 fof(f48,plain,(
% 19.17/2.88 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f19,f37])).
% 19.17/2.88 fof(f50,plain,(
% 19.17/2.88 converse(sk1)=join(zero,complement(join(sk2,complement(converse(sk1)))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f16,f46])).
% 19.17/2.88 fof(f51,plain,(
% 19.17/2.88 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f19,f47])).
% 19.17/2.88 fof(f52,plain,(
% 19.17/2.88 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f16,f48])).
% 19.17/2.88 fof(f144,plain,(
% 19.17/2.88 ![X0,X1]: (join(complement(X0),composition(X1,complement(composition(converse(X1),X0))))=complement(X0))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f23,f36])).
% 19.17/2.88 fof(f234,plain,(
% 19.17/2.88 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f21,f45])).
% 19.17/2.88 fof(f236,plain,(
% 19.17/2.88 ![X0]: (X0=composition(converse(one),X0))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f23,f234])).
% 19.17/2.88 fof(f239,plain,(
% 19.17/2.88 ![X0,X1]: (top=join(join(complement(X0),complement(X1)),meet(X0,X1)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f19,f27])).
% 19.17/2.88 fof(f240,plain,(
% 19.17/2.88 ![X0,X1]: (meet(join(complement(X0),complement(X1)),meet(X0,X1))=complement(top))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f27,f39])).
% 19.17/2.88 fof(f241,plain,(
% 19.17/2.88 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f27,f42])).
% 19.17/2.88 fof(f247,plain,(
% 19.17/2.88 ![X0,X1]: (top=join(complement(X0),join(complement(X1),meet(X0,X1))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f17,f239])).
% 19.17/2.88 fof(f248,plain,(
% 19.17/2.88 zero=complement(top)),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f41,f240])).
% 19.17/2.88 fof(f275,plain,(
% 19.17/2.88 one=converse(one)),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f21,f236])).
% 19.17/2.88 fof(f279,plain,(
% 19.17/2.88 ![X0]: (join(complement(X0),composition(one,complement(X0)))=complement(X0))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f236,f144])).
% 19.17/2.88 fof(f286,plain,(
% 19.17/2.88 ![X0]: (X0=composition(one,X0))),
% 19.17/2.88 inference(backward_demodulation,[status(thm)],[f275,f236])).
% 19.17/2.88 fof(f294,plain,(
% 19.17/2.88 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 19.17/2.88 inference(backward_demodulation,[status(thm)],[f286,f279])).
% 19.17/2.88 fof(f338,plain,(
% 19.17/2.88 join(zero,complement(top))=complement(top)),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f248,f294])).
% 19.17/2.88 fof(f347,plain,(
% 19.17/2.88 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f294,f19])).
% 19.17/2.88 fof(f348,plain,(
% 19.17/2.88 ![X0]: (X0=join(meet(X0,complement(X0)),complement(complement(X0))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f294,f37])).
% 19.17/2.88 fof(f349,plain,(
% 19.17/2.88 join(zero,zero)=complement(top)),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f248,f338])).
% 19.17/2.88 fof(f350,plain,(
% 19.17/2.88 join(zero,zero)=zero),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f248,f349])).
% 19.17/2.88 fof(f369,plain,(
% 19.17/2.88 ![X0]: (X0=join(complement(complement(X0)),meet(X0,complement(X0))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f16,f348])).
% 19.17/2.88 fof(f370,plain,(
% 19.17/2.88 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f28,f369])).
% 19.17/2.88 fof(f371,plain,(
% 19.17/2.88 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f16,f370])).
% 19.17/2.88 fof(f375,plain,(
% 19.17/2.88 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(meet(X0,X1))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f19,f371])).
% 19.17/2.88 fof(f395,plain,(
% 19.17/2.88 ![X0]: (join(zero,join(zero,X0))=join(zero,X0))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f350,f17])).
% 19.17/2.88 fof(f403,plain,(
% 19.17/2.88 ![X0,X1,X2]: (join(converse(X0),join(converse(X1),X2))=join(converse(join(X0,X1)),X2))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f24,f17])).
% 19.17/2.88 fof(f423,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,join(converse(complement(converse(X0))),X1))=join(converse(top),X1))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f241,f17])).
% 19.17/2.88 fof(f470,plain,(
% 19.17/2.88 ![X0]: (join(meet(X0,X0),complement(complement(X0)))=complement(complement(X0)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f347,f294])).
% 19.17/2.88 fof(f471,plain,(
% 19.17/2.88 ![X0]: (top=join(complement(X0),meet(X0,X0)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f347,f27])).
% 19.17/2.88 fof(f532,plain,(
% 19.17/2.88 ![X0,X1]: (join(complement(X0),join(meet(X0,X0),X1))=join(top,X1))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f471,f17])).
% 19.17/2.88 fof(f583,plain,(
% 19.17/2.88 ![X0]: (join(zero,X0)=join(zero,complement(complement(X0))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f371,f395])).
% 19.17/2.88 fof(f584,plain,(
% 19.17/2.88 join(zero,converse(sk1))=join(zero,complement(join(sk2,complement(converse(sk1)))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f50,f395])).
% 19.17/2.88 fof(f586,plain,(
% 19.17/2.88 ![X0]: (join(zero,X0)=join(zero,meet(X0,X0)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f51,f395])).
% 19.17/2.88 fof(f592,plain,(
% 19.17/2.88 ![X0]: (X0=complement(complement(X0)))),
% 19.17/2.88 inference(backward_demodulation,[status(thm)],[f620,f371])).
% 19.17/2.88 fof(f601,plain,(
% 19.17/2.88 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 19.17/2.88 inference(backward_demodulation,[status(thm)],[f620,f375])).
% 19.17/2.88 fof(f620,plain,(
% 19.17/2.88 ![X0]: (join(zero,X0)=X0)),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f371,f583])).
% 19.17/2.88 fof(f621,plain,(
% 19.17/2.88 converse(sk1)=join(zero,complement(join(sk2,complement(converse(sk1)))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f620,f584])).
% 19.17/2.88 fof(f622,plain,(
% 19.17/2.88 converse(sk1)=complement(join(sk2,complement(converse(sk1))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f620,f621])).
% 19.17/2.88 fof(f625,plain,(
% 19.17/2.88 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f620,f586])).
% 19.17/2.88 fof(f633,plain,(
% 19.17/2.88 ![X0,X1]: (join(complement(X0),join(X0,X1))=join(top,X1))),
% 19.17/2.88 inference(backward_demodulation,[status(thm)],[f648,f532])).
% 19.17/2.88 fof(f643,plain,(
% 19.17/2.88 ![X0]: (join(X0,complement(complement(X0)))=complement(complement(X0)))),
% 19.17/2.88 inference(backward_demodulation,[status(thm)],[f648,f470])).
% 19.17/2.88 fof(f648,plain,(
% 19.17/2.88 ![X0]: (X0=meet(X0,X0))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f620,f625])).
% 19.17/2.88 fof(f733,plain,(
% 19.17/2.88 ![X0]: (join(X0,X0)=complement(complement(X0)))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f592,f643])).
% 19.17/2.88 fof(f735,plain,(
% 19.17/2.88 ![X0]: (join(X0,X0)=X0)),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f592,f733])).
% 19.17/2.88 fof(f765,plain,(
% 19.17/2.88 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f17,f16])).
% 19.17/2.88 fof(f776,plain,(
% 19.17/2.88 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(X1,complement(X0)))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f16,f37])).
% 19.17/2.88 fof(f777,plain,(
% 19.17/2.88 ![X0,X1]: (converse(join(converse(X0),X1))=join(converse(X1),X0))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f16,f43])).
% 19.17/2.88 fof(f785,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,join(X1,complement(X0)))=join(top,X1))),
% 19.17/2.88 inference(backward_demodulation,[status(thm)],[f765,f633])).
% 19.17/2.88 fof(f970,plain,(
% 19.17/2.88 ![X0]: (X0=join(X0,meet(X0,complement(X0))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f648,f52])).
% 19.17/2.88 fof(f975,plain,(
% 19.17/2.88 ![X0]: (X0=join(X0,zero))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f28,f970])).
% 19.17/2.88 fof(f997,plain,(
% 19.17/2.88 join(sk2,complement(converse(sk1)))=complement(converse(sk1))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f622,f592])).
% 19.17/2.88 fof(f1099,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,join(X0,X1))=join(X0,X1))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f735,f17])).
% 19.17/2.88 fof(f1224,plain,(
% 19.17/2.88 ![X0,X1]: (X0=join(meet(X0,join(complement(X1),meet(X0,X1))),complement(top)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f247,f37])).
% 19.17/2.88 fof(f1262,plain,(
% 19.17/2.88 ![X0,X1]: (X0=join(complement(top),meet(X0,join(complement(X1),meet(X0,X1)))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f16,f1224])).
% 19.17/2.88 fof(f1263,plain,(
% 19.17/2.88 ![X0,X1]: (X0=join(zero,meet(X0,join(complement(X1),meet(X0,X1)))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f248,f1262])).
% 19.17/2.88 fof(f1264,plain,(
% 19.17/2.88 ![X0,X1]: (X0=meet(X0,join(complement(X1),meet(X0,X1))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f620,f1263])).
% 19.17/2.88 fof(f1267,plain,(
% 19.17/2.88 ![X0,X1]: (X0=meet(X0,join(X1,meet(X0,complement(X1)))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f592,f1264])).
% 19.17/2.88 fof(f1347,plain,(
% 19.17/2.88 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X1,X0)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f16,f601])).
% 19.17/2.88 fof(f1349,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,complement(X1))=complement(meet(complement(X0),X1)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f592,f601])).
% 19.17/2.88 fof(f1352,plain,(
% 19.17/2.88 ![X0,X1]: (join(complement(X0),X1)=complement(meet(X0,complement(X1))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f592,f601])).
% 19.17/2.88 fof(f1398,plain,(
% 19.17/2.88 ![X0,X1]: (join(meet(X0,X1),X0)=join(meet(X0,X1),meet(X0,complement(X1))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f52,f1099])).
% 19.17/2.88 fof(f1404,plain,(
% 19.17/2.88 ![X0]: (join(X0,top)=join(X0,complement(X0)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f27,f1099])).
% 19.17/2.88 fof(f1406,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,join(X1,X0))=join(X0,X1))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f16,f1099])).
% 19.17/2.88 fof(f1429,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,meet(X0,X1))=join(meet(X0,X1),meet(X0,complement(X1))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f16,f1398])).
% 19.17/2.88 fof(f1438,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f52,f1429])).
% 19.17/2.88 fof(f1446,plain,(
% 19.17/2.88 ![X0]: (join(X0,top)=top)),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f27,f1404])).
% 19.17/2.88 fof(f1458,plain,(
% 19.17/2.88 ![X0]: (join(top,X0)=top)),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f16,f1446])).
% 19.17/2.88 fof(f1480,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,join(X1,complement(X0)))=top)),
% 19.17/2.88 inference(backward_demodulation,[status(thm)],[f1458,f785])).
% 19.17/2.88 fof(f1501,plain,(
% 19.17/2.88 converse(top)=top),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f241,f1458])).
% 19.17/2.88 fof(f1518,plain,(
% 19.17/2.88 ![X0]: (top=join(X0,converse(complement(converse(X0)))))),
% 19.17/2.88 inference(backward_demodulation,[status(thm)],[f1501,f241])).
% 19.17/2.88 fof(f1520,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,join(converse(complement(converse(X0))),X1))=join(top,X1))),
% 19.17/2.88 inference(backward_demodulation,[status(thm)],[f1501,f423])).
% 19.17/2.88 fof(f1529,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,join(converse(complement(converse(X0))),X1))=top)),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f1458,f1520])).
% 19.17/2.88 fof(f1659,plain,(
% 19.17/2.88 ![X0,X1]: (X0=join(meet(X0,join(X1,complement(complement(X0)))),complement(top)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f1480,f37])).
% 19.17/2.88 fof(f1670,plain,(
% 19.17/2.88 ![X0,X1]: (X0=join(complement(top),meet(X0,join(X1,complement(complement(X0))))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f16,f1659])).
% 19.17/2.88 fof(f1671,plain,(
% 19.17/2.88 ![X0,X1]: (X0=join(zero,meet(X0,join(X1,complement(complement(X0))))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f248,f1670])).
% 19.17/2.88 fof(f1672,plain,(
% 19.17/2.88 ![X0,X1]: (X0=meet(X0,join(X1,complement(complement(X0)))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f620,f1671])).
% 19.17/2.88 fof(f1674,plain,(
% 19.17/2.88 ![X0,X1]: (X0=meet(X0,join(X1,X0)))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f592,f1672])).
% 19.17/2.88 fof(f1990,plain,(
% 19.17/2.88 ![X0,X1]: (join(complement(join(complement(X0),X1)),X0)=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f37,f1406])).
% 19.17/2.88 fof(f2028,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,complement(join(complement(X0),X1)))=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f16,f1990])).
% 19.17/2.88 fof(f2029,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,complement(join(complement(X0),X1)))=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f16,f2028])).
% 19.17/2.88 fof(f2030,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,complement(join(complement(X0),X1)))=X0)),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f37,f2029])).
% 19.17/2.88 fof(f2090,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,complement(join(X1,complement(X0))))=X0)),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f16,f2030])).
% 19.17/2.88 fof(f2730,plain,(
% 19.17/2.88 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),X1)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f1352,f592])).
% 19.17/2.88 fof(f2886,plain,(
% 19.17/2.88 ![X0,X1]: (meet(complement(X0),X1)=complement(join(X0,complement(X1))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f1349,f592])).
% 19.17/2.88 fof(f2933,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,meet(complement(X1),X0))=X0)),
% 19.17/2.88 inference(backward_demodulation,[status(thm)],[f2886,f2090])).
% 19.17/2.88 fof(f2934,plain,(
% 19.17/2.88 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 19.17/2.88 inference(backward_demodulation,[status(thm)],[f2886,f776])).
% 19.17/2.88 fof(f2957,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f592,f2933])).
% 19.17/2.88 fof(f3033,plain,(
% 19.17/2.88 ![X0,X1]: (join(join(X0,meet(X1,complement(X0))),X1)=join(X0,meet(X1,complement(X0))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f1267,f2957])).
% 19.17/2.88 fof(f3060,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,join(meet(X1,complement(X0)),X1))=join(X0,meet(X1,complement(X0))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f17,f3033])).
% 19.17/2.88 fof(f3061,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,join(X1,meet(X1,complement(X0))))=join(X0,meet(X1,complement(X0))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f16,f3060])).
% 19.17/2.88 fof(f3065,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,X1)=join(X0,meet(X1,complement(X0))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f1438,f3061])).
% 19.17/2.88 fof(f3192,plain,(
% 19.17/2.88 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f592,f2934])).
% 19.17/2.88 fof(f3220,plain,(
% 19.17/2.88 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f16,f3192])).
% 19.17/2.88 fof(f3242,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,X1)=join(X1,meet(join(X0,X1),complement(X1))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f1674,f3220])).
% 19.17/2.88 fof(f3277,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,X1)=join(X1,join(X0,X1)))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f3065,f3242])).
% 19.17/2.88 fof(f3306,plain,(
% 19.17/2.88 ![X0,X1]: (top=join(converse(join(X0,X1)),complement(converse(X0))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f1480,f403])).
% 19.17/2.88 fof(f3361,plain,(
% 19.17/2.88 ![X0,X1]: (top=join(complement(converse(X0)),converse(join(X0,X1))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f16,f3306])).
% 19.17/2.88 fof(f4128,plain,(
% 19.17/2.88 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X2,join(X0,join(X1,X2))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f17,f3277])).
% 19.17/2.88 fof(f4153,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,join(X1,X0))=join(join(X1,X0),join(X0,X1)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f1406,f3277])).
% 19.17/2.88 fof(f4210,plain,(
% 19.17/2.88 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,join(X1,X2))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f17,f4128])).
% 19.17/2.88 fof(f4274,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,X1)=join(join(X0,X1),join(X1,X0)))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f3277,f4153])).
% 19.17/2.88 fof(f4275,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,X1)=join(X0,join(X1,join(X1,X0))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f17,f4274])).
% 19.17/2.88 fof(f4276,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,X1)=join(X1,join(X1,X0)))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f4210,f4275])).
% 19.17/2.88 fof(f4684,plain,(
% 19.17/2.88 ![X0,X1]: (meet(X0,complement(complement(X1)))=complement(complement(meet(X1,X0))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f1347,f2730])).
% 19.17/2.88 fof(f4700,plain,(
% 19.17/2.88 ![X0,X1]: (meet(X0,complement(join(X1,complement(X0))))=complement(join(X1,complement(X0))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f3277,f2730])).
% 19.17/2.88 fof(f4701,plain,(
% 19.17/2.88 ![X0,X1]: (meet(X0,complement(join(X1,complement(X0))))=complement(join(complement(X0),X1)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f1406,f2730])).
% 19.17/2.88 fof(f4711,plain,(
% 19.17/2.88 ![X0,X1]: (meet(complement(X0),complement(X1))=complement(join(X0,X1)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f592,f2730])).
% 19.17/2.88 fof(f4741,plain,(
% 19.17/2.88 ![X0,X1]: (meet(X0,X1)=complement(complement(meet(X1,X0))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f592,f4684])).
% 19.17/2.88 fof(f4772,plain,(
% 19.17/2.88 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f592,f4741])).
% 19.17/2.88 fof(f4799,plain,(
% 19.17/2.88 ![X0,X1]: (meet(X0,meet(complement(X1),X0))=complement(join(X1,complement(X0))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f2886,f4700])).
% 19.17/2.88 fof(f4800,plain,(
% 19.17/2.88 ![X0,X1]: (meet(X0,meet(complement(X1),X0))=meet(complement(X1),X0))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f2886,f4799])).
% 19.17/2.88 fof(f4801,plain,(
% 19.17/2.88 ![X0,X1]: (meet(X0,meet(complement(X1),X0))=complement(join(complement(X0),X1)))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f2886,f4701])).
% 19.17/2.88 fof(f4802,plain,(
% 19.17/2.88 ![X0,X1]: (meet(complement(X0),X1)=complement(join(complement(X1),X0)))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f4800,f4801])).
% 19.17/2.88 fof(f4951,plain,(
% 19.17/2.88 ![X0,X1]: (X0=join(meet(X1,X0),meet(complement(X1),X0)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f4772,f3220])).
% 19.17/2.88 fof(f4952,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,X1)=join(X0,meet(complement(X0),X1)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f4772,f3065])).
% 19.17/2.88 fof(f5146,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,join(X0,X1))=join(X0,meet(complement(X0),X1)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f4952,f1099])).
% 19.17/2.88 fof(f5191,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,X1)=join(X1,meet(complement(X1),X0)))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f4276,f5146])).
% 19.17/2.88 fof(f5213,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,complement(X1))=join(complement(X1),meet(X1,X0)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f592,f5191])).
% 19.17/2.88 fof(f5584,plain,(
% 19.17/2.88 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X2,X0)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f16,f765])).
% 19.17/2.88 fof(f6979,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,complement(X1))=join(X0,complement(join(X0,X1))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f4711,f4952])).
% 19.17/2.88 fof(f10911,plain,(
% 19.17/2.88 top=join(complement(converse(sk2)),converse(complement(converse(sk1))))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f997,f3361])).
% 19.17/2.88 fof(f12280,plain,(
% 19.17/2.88 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=join(X0,complement(top)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f1518,f6979])).
% 19.17/2.88 fof(f12288,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,complement(join(converse(complement(converse(X0))),X1)))=join(X0,complement(top)))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f1529,f6979])).
% 19.17/2.88 fof(f12496,plain,(
% 19.17/2.88 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=join(X0,zero))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f248,f12280])).
% 19.17/2.88 fof(f12497,plain,(
% 19.17/2.88 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=X0)),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f975,f12496])).
% 19.17/2.88 fof(f12508,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,complement(join(converse(complement(converse(X0))),X1)))=join(X0,zero))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f248,f12288])).
% 19.17/2.88 fof(f12509,plain,(
% 19.17/2.88 ![X0,X1]: (join(X0,complement(join(converse(complement(converse(X0))),X1)))=X0)),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f975,f12508])).
% 19.17/2.88 fof(f12662,plain,(
% 19.17/2.88 ![X0]: (converse(converse(X0))=join(converse(complement(converse(complement(converse(converse(X0)))))),X0))),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f12497,f777])).
% 19.17/2.88 fof(f12724,plain,(
% 19.17/2.88 ![X0]: (X0=join(converse(complement(converse(complement(converse(converse(X0)))))),X0))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f23,f12662])).
% 19.17/2.88 fof(f12725,plain,(
% 19.17/2.88 ![X0]: (X0=join(X0,converse(complement(converse(complement(converse(converse(X0))))))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f16,f12724])).
% 19.17/2.88 fof(f12726,plain,(
% 19.17/2.88 ![X0]: (X0=join(X0,converse(complement(converse(complement(X0))))))),
% 19.17/2.88 inference(forward_demodulation,[status(thm)],[f23,f12725])).
% 19.17/2.88 fof(f14293,plain,(
% 19.17/2.88 meet(complement(converse(complement(converse(sk1)))),converse(sk2))=complement(top)),
% 19.17/2.88 inference(paramodulation,[status(thm)],[f10911,f4802])).
% 19.17/2.88 fof(f14326,plain,(
% 19.17/2.88 meet(converse(sk2),complement(converse(complement(converse(sk1)))))=complement(top)),
% 16.24/2.93 inference(forward_demodulation,[status(thm)],[f4772,f14293])).
% 16.24/2.93 fof(f14327,plain,(
% 16.24/2.93 meet(converse(sk2),complement(converse(complement(converse(sk1)))))=zero),
% 16.24/2.93 inference(forward_demodulation,[status(thm)],[f248,f14326])).
% 16.24/2.93 fof(f17023,plain,(
% 16.24/2.93 ![X0,X1]: (meet(complement(complement(join(converse(complement(converse(complement(X0)))),X1))),X0)=complement(complement(X0)))),
% 16.24/2.93 inference(paramodulation,[status(thm)],[f12509,f4802])).
% 16.24/2.93 fof(f17112,plain,(
% 16.24/2.93 ![X0,X1]: (meet(X0,complement(complement(join(converse(complement(converse(complement(X0)))),X1))))=complement(complement(X0)))),
% 16.24/2.93 inference(forward_demodulation,[status(thm)],[f4772,f17023])).
% 16.24/2.93 fof(f17113,plain,(
% 16.24/2.93 ![X0,X1]: (meet(X0,join(converse(complement(converse(complement(X0)))),X1))=complement(complement(X0)))),
% 16.24/2.93 inference(forward_demodulation,[status(thm)],[f592,f17112])).
% 16.24/2.93 fof(f17115,plain,(
% 16.24/2.93 ![X0,X1]: (meet(X0,join(converse(complement(converse(complement(X0)))),X1))=X0)),
% 16.24/2.93 inference(forward_demodulation,[status(thm)],[f592,f17113])).
% 16.24/2.93 fof(f19104,plain,(
% 16.24/2.93 ![X0,X1]: (join(converse(complement(converse(complement(complement(X0))))),X1)=join(meet(X0,join(converse(complement(converse(complement(complement(X0))))),X1)),complement(X0)))),
% 16.24/2.93 inference(paramodulation,[status(thm)],[f17115,f4951])).
% 16.24/2.93 fof(f19156,plain,(
% 16.24/2.93 ![X0,X1]: (join(converse(complement(converse(X0))),X1)=join(meet(X0,join(converse(complement(converse(complement(complement(X0))))),X1)),complement(X0)))),
% 16.24/2.93 inference(forward_demodulation,[status(thm)],[f592,f19104])).
% 16.24/2.93 fof(f19157,plain,(
% 16.24/2.93 ![X0,X1]: (join(converse(complement(converse(X0))),X1)=join(complement(X0),meet(X0,join(converse(complement(converse(complement(complement(X0))))),X1))))),
% 16.24/2.93 inference(forward_demodulation,[status(thm)],[f16,f19156])).
% 16.24/2.93 fof(f19158,plain,(
% 16.24/2.93 ![X0,X1]: (join(converse(complement(converse(X0))),X1)=join(join(converse(complement(converse(complement(complement(X0))))),X1),complement(X0)))),
% 16.24/2.93 inference(forward_demodulation,[status(thm)],[f5213,f19157])).
% 16.24/2.93 fof(f19159,plain,(
% 16.24/2.93 ![X0,X1]: (join(converse(complement(converse(X0))),X1)=join(X1,join(complement(X0),converse(complement(converse(complement(complement(X0))))))))),
% 16.24/2.93 inference(forward_demodulation,[status(thm)],[f5584,f19158])).
% 16.24/2.93 fof(f19194,plain,(
% 16.24/2.93 ![X0,X1]: (join(converse(complement(converse(X0))),X1)=join(X1,complement(X0)))),
% 16.24/2.93 inference(forward_demodulation,[status(thm)],[f12726,f19159])).
% 16.24/2.93 fof(f19362,plain,(
% 16.24/2.93 ![X0]: (converse(complement(converse(X0)))=join(zero,complement(X0)))),
% 16.24/2.93 inference(paramodulation,[status(thm)],[f975,f19194])).
% 16.24/2.93 fof(f19623,plain,(
% 16.24/2.93 meet(converse(sk2),complement(complement(sk1)))=zero),
% 16.24/2.93 inference(backward_demodulation,[status(thm)],[f19645,f14327])).
% 16.24/2.93 fof(f19645,plain,(
% 16.24/2.93 ![X0]: (converse(complement(converse(X0)))=complement(X0))),
% 16.24/2.93 inference(forward_demodulation,[status(thm)],[f620,f19362])).
% 16.24/2.93 fof(f20125,plain,(
% 16.24/2.93 meet(converse(sk2),sk1)=zero),
% 16.24/2.93 inference(forward_demodulation,[status(thm)],[f592,f19623])).
% 16.24/2.93 fof(f20126,plain,(
% 16.24/2.93 meet(sk1,converse(sk2))=zero),
% 16.24/2.93 inference(forward_demodulation,[status(thm)],[f4772,f20125])).
% 16.24/2.93 fof(f20127,plain,(
% 16.24/2.93 $false),
% 16.24/2.93 inference(forward_subsumption_resolution,[status(thm)],[f20126,f30])).
% 16.24/2.93 % SZS output end CNFRefutation for theBenchmark.p
% 16.24/2.95 % Elapsed time: 2.578963 seconds
% 16.24/2.95 % CPU time: 20.233515 seconds
% 16.24/2.95 % Total memory used: 242.682 MB
% 16.24/2.95 % Net memory used: 236.939 MB
%------------------------------------------------------------------------------