%------------------------------------------------------------------------------
% 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/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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 : Theorem 46.79s 6.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL006+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n009.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:58 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.48 % Drodi V4.1.1
% 46.79/6.53 % Refutation found
% 46.79/6.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 46.79/6.53 % SZS output start CNFRefutation for theBenchmark
% 46.79/6.53 fof(f1,axiom,(
% 46.79/6.53 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 46.79/6.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.79/6.53 fof(f2,axiom,(
% 46.79/6.53 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 46.79/6.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.79/6.53 fof(f3,axiom,(
% 46.79/6.53 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 46.79/6.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.79/6.53 fof(f4,axiom,(
% 46.79/6.53 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 46.79/6.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.79/6.53 fof(f6,axiom,(
% 46.79/6.53 (! [X0] : composition(X0,one) = X0 )),
% 46.79/6.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.79/6.53 fof(f8,axiom,(
% 46.79/6.53 (! [X0] : converse(converse(X0)) = X0 )),
% 46.79/6.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.79/6.53 fof(f9,axiom,(
% 46.79/6.53 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 46.79/6.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.79/6.53 fof(f10,axiom,(
% 46.79/6.53 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 46.79/6.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.79/6.53 fof(f11,axiom,(
% 46.79/6.53 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 46.79/6.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.79/6.53 fof(f12,axiom,(
% 46.79/6.53 (! [X0] : top = join(X0,complement(X0)) )),
% 46.79/6.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.79/6.53 fof(f13,axiom,(
% 46.79/6.53 (! [X0] : zero = meet(X0,complement(X0)) )),
% 46.79/6.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.79/6.53 fof(f14,conjecture,(
% 46.79/6.53 (! [X0,X1] :( meet(converse(X0),X1) = zero=> meet(X0,converse(X1)) = zero ) )),
% 46.79/6.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.79/6.53 fof(f15,negated_conjecture,(
% 46.79/6.53 ~((! [X0,X1] :( meet(converse(X0),X1) = zero=> meet(X0,converse(X1)) = zero ) ))),
% 46.79/6.53 inference(negated_conjecture,[status(cth)],[f14])).
% 46.79/6.53 fof(f16,plain,(
% 46.79/6.53 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 46.79/6.53 inference(cnf_transformation,[status(thm)],[f1])).
% 46.79/6.53 fof(f17,plain,(
% 46.79/6.53 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 46.79/6.53 inference(cnf_transformation,[status(thm)],[f2])).
% 46.79/6.53 fof(f18,plain,(
% 46.79/6.53 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 46.79/6.53 inference(cnf_transformation,[status(thm)],[f3])).
% 46.79/6.53 fof(f19,plain,(
% 46.79/6.53 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 46.79/6.53 inference(cnf_transformation,[status(thm)],[f4])).
% 46.79/6.53 fof(f21,plain,(
% 46.79/6.53 ![X0]: (composition(X0,one)=X0)),
% 46.79/6.53 inference(cnf_transformation,[status(thm)],[f6])).
% 46.79/6.53 fof(f23,plain,(
% 46.79/6.53 ![X0]: (converse(converse(X0))=X0)),
% 46.79/6.53 inference(cnf_transformation,[status(thm)],[f8])).
% 46.79/6.53 fof(f24,plain,(
% 46.79/6.53 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 46.79/6.53 inference(cnf_transformation,[status(thm)],[f9])).
% 46.79/6.53 fof(f25,plain,(
% 46.79/6.53 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 46.79/6.53 inference(cnf_transformation,[status(thm)],[f10])).
% 46.79/6.53 fof(f26,plain,(
% 46.79/6.53 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 46.79/6.53 inference(cnf_transformation,[status(thm)],[f11])).
% 46.79/6.53 fof(f27,plain,(
% 46.79/6.53 ![X0]: (top=join(X0,complement(X0)))),
% 46.79/6.53 inference(cnf_transformation,[status(thm)],[f12])).
% 46.79/6.53 fof(f28,plain,(
% 46.79/6.53 ![X0]: (zero=meet(X0,complement(X0)))),
% 46.79/6.53 inference(cnf_transformation,[status(thm)],[f13])).
% 46.79/6.53 fof(f29,plain,(
% 46.79/6.53 (?[X0,X1]: (meet(converse(X0),X1)=zero&~meet(X0,converse(X1))=zero))),
% 46.79/6.53 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 46.79/6.53 fof(f30,plain,(
% 46.79/6.53 (meet(converse(sK0_skl),sK1_skl)=zero&~meet(sK0_skl,converse(sK1_skl))=zero)),
% 46.79/6.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl)],[f29])).
% 46.79/6.53 fof(f31,plain,(
% 46.79/6.53 meet(converse(sK0_skl),sK1_skl)=zero),
% 46.79/6.53 inference(cnf_transformation,[status(thm)],[f30])).
% 46.79/6.53 fof(f32,plain,(
% 46.79/6.53 ~meet(sK0_skl,converse(sK1_skl))=zero),
% 46.79/6.53 inference(cnf_transformation,[status(thm)],[f30])).
% 46.79/6.53 fof(f36,plain,(
% 46.79/6.53 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f19,f18])).
% 46.79/6.53 fof(f38,plain,(
% 46.79/6.53 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X0,X1),complement(X2))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f19,f19])).
% 46.79/6.53 fof(f40,plain,(
% 46.79/6.53 ![X0,X1]: (zero=meet(join(complement(X0),complement(X1)),meet(X0,X1)))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f19,f28])).
% 46.79/6.53 fof(f41,plain,(
% 46.79/6.53 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f23,f24])).
% 46.79/6.53 fof(f42,plain,(
% 46.79/6.53 ![X0,X1]: (converse(join(X0,converse(X1)))=join(converse(X0),X1))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f23,f24])).
% 46.79/6.53 fof(f44,plain,(
% 46.79/6.53 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f23,f25])).
% 46.79/6.53 fof(f125,plain,(
% 46.79/6.53 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f19,f36])).
% 46.79/6.53 fof(f126,plain,(
% 46.79/6.53 ![X0,X1,X2]: (join(complement(X0),complement(X1))=join(meet(join(complement(X0),complement(X1)),X2),complement(join(meet(X0,X1),X2))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f19,f36])).
% 46.79/6.53 fof(f142,plain,(
% 46.79/6.53 ![X0]: (meet(join(complement(converse(sK0_skl)),complement(sK1_skl)),X0)=complement(join(zero,complement(X0))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f31,f38])).
% 46.79/6.53 fof(f143,plain,(
% 46.79/6.53 ![X0,X1]: (meet(join(complement(X0),complement(complement(X0))),X1)=complement(join(zero,complement(X1))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f28,f38])).
% 46.79/6.53 fof(f151,plain,(
% 46.79/6.53 ![X0]: (meet(join(complement(converse(sK0_skl)),complement(sK1_skl)),X0)=meet(top,X0))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f152,f142])).
% 46.79/6.53 fof(f152,plain,(
% 46.79/6.53 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f27,f143])).
% 46.79/6.53 fof(f156,plain,(
% 46.79/6.53 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f21,f44])).
% 46.79/6.53 fof(f158,plain,(
% 46.79/6.53 ![X0]: (X0=composition(converse(one),X0))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f23,f156])).
% 46.79/6.53 fof(f168,plain,(
% 46.79/6.53 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(complement(X2),meet(X0,X1))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f16,f38])).
% 46.79/6.53 fof(f172,plain,(
% 46.79/6.53 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(X1,complement(X0)))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f16,f36])).
% 46.79/6.53 fof(f183,plain,(
% 46.79/6.53 ![X0,X1]: (meet(join(complement(X0),complement(X1)),meet(X0,X1))=complement(top))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f27,f38])).
% 46.79/6.53 fof(f184,plain,(
% 46.79/6.53 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f27,f41])).
% 46.79/6.53 fof(f186,plain,(
% 46.79/6.53 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f27,f36])).
% 46.79/6.53 fof(f189,plain,(
% 46.79/6.53 zero=complement(top)),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f40,f183])).
% 46.79/6.53 fof(f191,plain,(
% 46.79/6.53 ![X0]: (X0=join(meet(X0,complement(complement(X0))),zero))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f189,f186])).
% 46.79/6.53 fof(f195,plain,(
% 46.79/6.53 ![X0]: (top=join(meet(top,X0),complement(join(zero,X0))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f189,f36])).
% 46.79/6.53 fof(f196,plain,(
% 46.79/6.53 ![X0]: (meet(X0,top)=complement(join(complement(X0),zero)))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f189,f19])).
% 46.79/6.53 fof(f198,plain,(
% 46.79/6.53 zero=meet(top,zero)),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f189,f28])).
% 46.79/6.53 fof(f201,plain,(
% 46.79/6.53 one=converse(one)),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f21,f158])).
% 46.79/6.53 fof(f207,plain,(
% 46.79/6.53 ![X0]: (join(composition(converse(converse(one)),complement(X0)),complement(X0))=complement(X0))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f158,f26])).
% 46.79/6.53 fof(f208,plain,(
% 46.79/6.53 ![X0]: (X0=composition(one,X0))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f201,f158])).
% 46.79/6.53 fof(f211,plain,(
% 46.79/6.53 ![X0]: (join(composition(one,complement(X0)),complement(X0))=complement(X0))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f23,f207])).
% 46.79/6.53 fof(f212,plain,(
% 46.79/6.53 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f208,f211])).
% 46.79/6.53 fof(f253,plain,(
% 46.79/6.53 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f212,f19])).
% 46.79/6.53 fof(f254,plain,(
% 46.79/6.53 ![X0]: (X0=join(meet(X0,complement(X0)),complement(complement(X0))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f212,f36])).
% 46.79/6.53 fof(f268,plain,(
% 46.79/6.53 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f28,f254])).
% 46.79/6.53 fof(f270,plain,(
% 46.79/6.53 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f16,f17])).
% 46.79/6.53 fof(f279,plain,(
% 46.79/6.53 ![X0,X1,X2]: (join(meet(X0,X1),join(complement(join(complement(X0),X1)),X2))=join(X0,X2))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f36,f17])).
% 46.79/6.53 fof(f329,plain,(
% 46.79/6.53 ![X0]: (join(complement(converse(sK0_skl)),complement(sK1_skl))=join(meet(top,X0),complement(join(complement(join(complement(converse(sK0_skl)),complement(sK1_skl))),X0))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f151,f36])).
% 46.79/6.53 fof(f337,plain,(
% 46.79/6.53 ![X0]: (join(complement(converse(sK0_skl)),complement(sK1_skl))=join(meet(top,X0),complement(join(meet(converse(sK0_skl),sK1_skl),X0))))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f19,f329])).
% 46.79/6.53 fof(f338,plain,(
% 46.79/6.53 ![X0]: (join(complement(converse(sK0_skl)),complement(sK1_skl))=join(meet(top,X0),complement(join(zero,X0))))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f31,f337])).
% 46.79/6.53 fof(f341,plain,(
% 46.79/6.53 join(complement(converse(sK0_skl)),complement(sK1_skl))=top),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f195,f338])).
% 46.79/6.53 fof(f343,plain,(
% 46.79/6.53 join(complement(sK1_skl),complement(converse(sK0_skl)))=top),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f16,f341])).
% 46.79/6.53 fof(f353,plain,(
% 46.79/6.53 meet(sK1_skl,converse(sK0_skl))=complement(top)),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f343,f19])).
% 46.79/6.53 fof(f356,plain,(
% 46.79/6.53 meet(sK1_skl,converse(sK0_skl))=zero),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f189,f353])).
% 46.79/6.53 fof(f366,plain,(
% 46.79/6.53 ![X0]: (join(meet(X0,X0),complement(complement(X0)))=complement(complement(X0)))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f253,f212])).
% 46.79/6.53 fof(f367,plain,(
% 46.79/6.53 ![X0]: (top=join(complement(X0),meet(X0,X0)))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f253,f27])).
% 46.79/6.53 fof(f371,plain,(
% 46.79/6.53 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),meet(X1,X1))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f253,f19])).
% 46.79/6.53 fof(f375,plain,(
% 46.79/6.53 ![X0,X1]: (meet(X0,complement(X1))=meet(join(complement(X1),complement(X1)),X0))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f168,f371])).
% 46.79/6.53 fof(f376,plain,(
% 46.79/6.53 ![X0,X1]: (meet(X0,complement(X1))=meet(complement(X1),X0))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f212,f375])).
% 46.79/6.53 fof(f411,plain,(
% 46.79/6.53 ![X0,X1]: (join(complement(X0),join(meet(X0,X0),X1))=join(top,X1))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f367,f17])).
% 46.79/6.53 fof(f434,plain,(
% 46.79/6.53 ![X0]: (meet(X0,zero)=meet(complement(top),X0))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f189,f376])).
% 46.79/6.53 fof(f439,plain,(
% 46.79/6.53 ![X0,X1]: (meet(X0,complement(complement(X1)))=meet(meet(X1,X1),X0))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f253,f376])).
% 46.79/6.53 fof(f444,plain,(
% 46.79/6.53 ![X0,X1]: (X0=join(meet(complement(X1),X0),complement(join(complement(X0),complement(X1)))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f376,f36])).
% 46.79/6.53 fof(f447,plain,(
% 46.79/6.53 ![X0]: (meet(X0,zero)=meet(zero,X0))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f189,f434])).
% 46.79/6.53 fof(f454,plain,(
% 46.79/6.53 ![X0,X1]: (X0=join(meet(complement(X1),X0),meet(X0,X1)))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f19,f444])).
% 46.79/6.53 fof(f569,plain,(
% 46.79/6.53 ![X0]: (X0=join(meet(zero,X0),complement(join(complement(X0),zero))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f447,f36])).
% 46.79/6.53 fof(f573,plain,(
% 46.79/6.53 ![X0]: (zero=join(meet(X0,zero),complement(join(complement(zero),X0))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f447,f36])).
% 46.79/6.53 fof(f576,plain,(
% 46.79/6.53 ![X0]: (X0=join(meet(zero,X0),meet(X0,top)))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f196,f569])).
% 46.79/6.53 fof(f604,plain,(
% 46.79/6.53 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f16,f125])).
% 46.79/6.53 fof(f646,plain,(
% 46.79/6.53 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f16,f454])).
% 46.79/6.53 fof(f664,plain,(
% 46.79/6.53 sK1_skl=join(meet(complement(converse(sK0_skl)),sK1_skl),zero)),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f356,f454])).
% 46.79/6.53 fof(f670,plain,(
% 46.79/6.53 ![X0]: (X0=join(meet(complement(complement(X0)),X0),zero))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f28,f454])).
% 46.79/6.53 fof(f683,plain,(
% 46.79/6.53 complement(zero)=join(zero,meet(complement(zero),top))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f28,f576])).
% 46.79/6.53 fof(f710,plain,(
% 46.79/6.53 ![X0]: (X0=join(complement(complement(X0)),meet(X0,complement(X0))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f253,f604])).
% 46.79/6.53 fof(f723,plain,(
% 46.79/6.53 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f28,f710])).
% 46.79/6.53 fof(f782,plain,(
% 46.79/6.53 ![X0,X1,X2]: (meet(join(complement(join(complement(X0),complement(X1))),complement(X2)),join(meet(X0,X1),X2))=complement(join(complement(X0),complement(X1))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f126,f38])).
% 46.79/6.53 fof(f843,plain,(
% 46.79/6.53 ![X0,X1,X2]: (meet(join(meet(X0,X1),complement(X2)),join(meet(X0,X1),X2))=complement(join(complement(X0),complement(X1))))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f19,f782])).
% 46.79/6.53 fof(f844,plain,(
% 46.79/6.53 ![X0,X1,X2]: (meet(join(meet(X0,X1),complement(X2)),join(meet(X0,X1),X2))=meet(X0,X1))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f19,f843])).
% 46.79/6.53 fof(f926,plain,(
% 46.79/6.53 join(complement(complement(converse(sK0_skl))),complement(sK1_skl))=join(meet(join(complement(complement(converse(sK0_skl))),complement(sK1_skl)),zero),complement(sK1_skl))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f664,f126])).
% 46.79/6.53 fof(f953,plain,(
% 46.79/6.53 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(meet(X0,X1)),zero))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f19,f723])).
% 46.79/6.53 fof(f980,plain,(
% 46.79/6.53 top=join(zero,meet(complement(zero),top))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f198,f646])).
% 46.79/6.53 fof(f990,plain,(
% 46.79/6.53 ![X0]: (complement(complement(X0))=join(meet(complement(complement(X0)),X0),zero))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f28,f646])).
% 46.79/6.53 fof(f1003,plain,(
% 46.79/6.53 complement(zero)=top),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f980,f683])).
% 46.79/6.53 fof(f1005,plain,(
% 46.79/6.53 ![X0]: (X0=join(X0,zero))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f1043,f723])).
% 46.79/6.53 fof(f1007,plain,(
% 46.79/6.53 ![X0]: (X0=join(meet(X0,X0),zero))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f1043,f191])).
% 46.79/6.53 fof(f1008,plain,(
% 46.79/6.53 ![X0]: (X0=join(zero,X0))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f1043,f268])).
% 46.79/6.53 fof(f1011,plain,(
% 46.79/6.53 join(complement(complement(converse(sK0_skl))),complement(sK1_skl))=join(meet(join(converse(sK0_skl),complement(sK1_skl)),zero),complement(sK1_skl))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f1043,f926])).
% 46.79/6.53 fof(f1036,plain,(
% 46.79/6.53 ![X0,X1]: (meet(X0,X1)=meet(meet(X1,X1),X0))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f1043,f439])).
% 46.79/6.53 fof(f1040,plain,(
% 46.79/6.53 ![X0]: (join(meet(X0,X0),complement(complement(X0)))=X0)),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f1043,f366])).
% 46.79/6.53 fof(f1043,plain,(
% 46.79/6.53 ![X0]: (complement(complement(X0))=X0)),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f670,f990])).
% 46.79/6.53 fof(f1058,plain,(
% 46.79/6.53 ![X0]: (zero=join(meet(X0,zero),complement(join(top,X0))))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f1003,f573])).
% 46.79/6.53 fof(f1081,plain,(
% 46.79/6.53 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f1005,f953])).
% 46.79/6.53 fof(f1084,plain,(
% 46.79/6.53 ![X0]: (meet(X0,top)=complement(complement(X0)))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f1005,f196])).
% 46.79/6.53 fof(f1087,plain,(
% 46.79/6.53 ![X0]: (top=join(complement(X0),X0))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f1114,f367])).
% 46.79/6.53 fof(f1110,plain,(
% 46.79/6.53 ![X0,X1]: (join(complement(X0),join(X0,X1))=join(top,X1))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f1114,f411])).
% 46.79/6.53 fof(f1114,plain,(
% 46.79/6.53 ![X0]: (X0=meet(X0,X0))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f1005,f1007])).
% 46.79/6.53 fof(f1144,plain,(
% 46.79/6.53 join(converse(sK0_skl),complement(sK1_skl))=join(meet(join(converse(sK0_skl),complement(sK1_skl)),zero),complement(sK1_skl))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f1043,f1011])).
% 46.79/6.53 fof(f1166,plain,(
% 46.79/6.53 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f1114,f1036])).
% 46.79/6.53 fof(f1169,plain,(
% 46.79/6.53 ![X0]: (join(X0,complement(complement(X0)))=X0)),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f1114,f1040])).
% 46.79/6.53 fof(f1173,plain,(
% 46.79/6.53 ![X0]: (join(X0,X0)=X0)),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f1043,f1169])).
% 46.79/6.53 fof(f1260,plain,(
% 46.79/6.53 ![X0]: (meet(X0,top)=X0)),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f1043,f1084])).
% 46.79/6.53 fof(f1374,plain,(
% 46.79/6.53 ![X0,X1]: (join(X0,join(X0,X1))=join(X0,X1))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f1173,f17])).
% 46.79/6.53 fof(f1403,plain,(
% 46.79/6.53 ![X0]: (zero=join(meet(zero,X0),complement(join(top,X0))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f1003,f36])).
% 46.79/6.53 fof(f1416,plain,(
% 46.79/6.53 ![X0]: (converse(converse(X0))=join(X0,converse(zero)))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f1005,f41])).
% 46.79/6.53 fof(f1422,plain,(
% 46.79/6.53 ![X0]: (X0=join(X0,converse(zero)))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f23,f1416])).
% 46.79/6.53 fof(f1602,plain,(
% 46.79/6.53 ![X0]: (converse(top)=join(converse(complement(converse(X0))),X0))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f1087,f42])).
% 46.79/6.53 fof(f1608,plain,(
% 46.79/6.53 zero=converse(zero)),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f1008,f1422])).
% 46.79/6.53 fof(f1763,plain,(
% 46.79/6.53 ![X0]: (zero=join(meet(zero,X0),complement(join(X0,top))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f1003,f172])).
% 46.79/6.53 fof(f1983,plain,(
% 46.79/6.53 ![X0,X1]: (join(meet(X0,X1),X0)=join(meet(X0,X1),meet(complement(X1),X0)))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f646,f1374])).
% 46.79/6.53 fof(f1994,plain,(
% 46.79/6.53 ![X0]: (join(X0,top)=join(X0,complement(X0)))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f27,f1374])).
% 46.79/6.53 fof(f2027,plain,(
% 46.79/6.53 ![X0,X1]: (join(meet(X0,X1),X0)=X0)),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f646,f1983])).
% 46.79/6.53 fof(f2045,plain,(
% 46.79/6.53 ![X0]: (zero=join(meet(zero,X0),complement(top)))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f2046,f1763])).
% 46.79/6.53 fof(f2046,plain,(
% 46.79/6.53 ![X0]: (join(X0,top)=top)),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f27,f1994])).
% 46.79/6.53 fof(f2057,plain,(
% 46.79/6.53 ![X0]: (zero=join(meet(zero,X0),zero))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f189,f2045])).
% 46.79/6.53 fof(f2065,plain,(
% 46.79/6.53 ![X0]: (zero=join(zero,complement(join(top,X0))))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f2067,f1403])).
% 46.79/6.53 fof(f2067,plain,(
% 46.79/6.53 ![X0]: (zero=meet(zero,X0))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f1005,f2057])).
% 46.79/6.53 fof(f2072,plain,(
% 46.79/6.53 ![X0]: (zero=join(meet(X0,zero),zero))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f2073,f1058])).
% 46.79/6.53 fof(f2073,plain,(
% 46.79/6.53 ![X0]: (zero=complement(join(top,X0)))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f1008,f2065])).
% 46.79/6.53 fof(f2078,plain,(
% 46.79/6.53 join(converse(sK0_skl),complement(sK1_skl))=join(zero,complement(sK1_skl))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f2084,f1144])).
% 46.79/6.53 fof(f2084,plain,(
% 46.79/6.53 ![X0]: (zero=meet(X0,zero))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f1005,f2072])).
% 46.79/6.53 fof(f2088,plain,(
% 46.79/6.53 join(converse(sK0_skl),complement(sK1_skl))=complement(sK1_skl)),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f1008,f2078])).
% 46.79/6.53 fof(f2096,plain,(
% 46.79/6.53 ![X0]: (join(top,X0)=top)),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f16,f2046])).
% 46.79/6.53 fof(f2100,plain,(
% 46.79/6.53 ![X0]: (converse(top)=join(X0,converse(top)))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f2046,f41])).
% 46.79/6.53 fof(f2119,plain,(
% 46.79/6.53 ![X0,X1]: (join(complement(X0),join(X0,X1))=top)),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f2096,f1110])).
% 46.79/6.53 fof(f2236,plain,(
% 46.79/6.53 ![X0,X1]: (join(meet(X0,X1),X1)=X1)),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f1166,f2027])).
% 46.79/6.53 fof(f2332,plain,(
% 46.79/6.53 ![X0,X1]: (join(meet(X0,X1),complement(join(complement(X0),X1)))=join(X0,complement(join(complement(X0),X1))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f1173,f279])).
% 46.79/6.53 fof(f2382,plain,(
% 46.79/6.53 ![X0,X1]: (X0=join(X0,complement(join(complement(X0),X1))))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f36,f2332])).
% 46.79/6.53 fof(f2470,plain,(
% 46.79/6.53 ![X0,X1]: (converse(converse(X0))=join(converse(meet(X1,converse(X0))),X0))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f2236,f42])).
% 46.79/6.53 fof(f2476,plain,(
% 46.79/6.53 ![X0,X1]: (X0=join(converse(meet(X1,converse(X0))),X0))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f23,f2470])).
% 46.79/6.53 fof(f2616,plain,(
% 46.79/6.53 converse(top)=top),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f2096,f2100])).
% 46.79/6.53 fof(f2649,plain,(
% 46.79/6.53 ![X0]: (top=join(converse(complement(converse(X0))),X0))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f2616,f1602])).
% 46.79/6.53 fof(f2650,plain,(
% 46.79/6.53 ![X0]: (top=join(X0,converse(complement(converse(X0)))))),
% 46.79/6.53 inference(backward_demodulation,[status(thm)],[f2616,f184])).
% 46.79/6.53 fof(f2754,plain,(
% 46.79/6.53 ![X0,X1]: (join(complement(meet(X0,X1)),X1)=top)),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f2236,f2119])).
% 46.79/6.53 fof(f2769,plain,(
% 46.79/6.53 ![X0,X1,X2]: (join(meet(X0,join(X0,X1)),join(complement(top),X2))=join(X0,X2))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f2119,f279])).
% 46.79/6.53 fof(f2790,plain,(
% 46.79/6.53 ![X0,X1,X2]: (join(meet(X0,join(X0,X1)),join(zero,X2))=join(X0,X2))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f189,f2769])).
% 46.79/6.53 fof(f2791,plain,(
% 46.79/6.53 ![X0,X1,X2]: (join(meet(X0,join(X0,X1)),X2)=join(X0,X2))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f1008,f2790])).
% 46.79/6.53 fof(f3361,plain,(
% 46.79/6.53 ![X0,X1]: (join(X0,join(X0,X1))=join(X1,X0))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f1173,f270])).
% 46.79/6.53 fof(f3718,plain,(
% 46.79/6.53 converse(complement(sK1_skl))=join(sK0_skl,converse(complement(sK1_skl)))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f2088,f41])).
% 46.79/6.53 fof(f4639,plain,(
% 46.79/6.53 ![X0,X1]: (X0=join(X0,complement(join(X1,complement(X0)))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f3361,f2382])).
% 46.79/6.53 fof(f4654,plain,(
% 46.79/6.53 ![X0,X1]: (complement(X0)=join(complement(X0),complement(join(X0,X1))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f1043,f2382])).
% 46.79/6.53 fof(f4702,plain,(
% 46.79/6.53 ![X0,X1]: (complement(X0)=complement(meet(X0,join(X0,X1))))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f1081,f4654])).
% 46.79/6.53 fof(f5232,plain,(
% 46.79/6.53 ![X0]: (X0=join(meet(X0,converse(complement(converse(complement(X0))))),complement(top)))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f2649,f172])).
% 46.79/6.53 fof(f5276,plain,(
% 46.79/6.53 ![X0]: (X0=join(meet(X0,converse(complement(converse(complement(X0))))),zero))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f189,f5232])).
% 46.79/6.53 fof(f5277,plain,(
% 46.79/6.53 ![X0]: (X0=meet(X0,converse(complement(converse(complement(X0))))))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f1005,f5276])).
% 46.79/6.53 fof(f5913,plain,(
% 46.79/6.53 ![X0,X1,X2]: (meet(X0,join(X0,X1))=join(meet(X0,join(X0,X1)),complement(join(X2,complement(X0)))))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f4702,f4639])).
% 46.79/6.53 fof(f5967,plain,(
% 46.79/6.53 ![X0,X1,X2]: (meet(X0,join(X0,X1))=join(X0,complement(join(X2,complement(X0)))))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f2791,f5913])).
% 46.79/6.53 fof(f5970,plain,(
% 46.79/6.53 ![X0,X1]: (meet(X0,join(X0,X1))=X0)),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f4639,f5967])).
% 46.79/6.53 fof(f6035,plain,(
% 46.79/6.53 ![X0,X1]: (meet(meet(X0,X1),X0)=meet(X0,X1))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f646,f5970])).
% 46.79/6.53 fof(f6039,plain,(
% 46.79/6.53 ![X0,X1]: (meet(meet(X0,X1),X1)=meet(X0,X1))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f2236,f5970])).
% 46.79/6.53 fof(f6059,plain,(
% 46.79/6.53 ![X0,X1,X2]: (meet(X0,join(X1,join(X2,X0)))=X0)),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f270,f5970])).
% 46.79/6.53 fof(f6617,plain,(
% 46.79/6.53 meet(sK0_skl,converse(complement(sK1_skl)))=sK0_skl),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f3718,f5970])).
% 46.79/6.53 fof(f6710,plain,(
% 46.79/6.53 ![X0,X1]: (meet(meet(X0,X1),X1)=meet(X1,X0))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f1166,f6035])).
% 46.79/6.53 fof(f6759,plain,(
% 46.79/6.53 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X1,X0))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f1166,f6039])).
% 46.79/6.53 fof(f7226,plain,(
% 46.79/6.53 ![X0,X1,X2]: (meet(X0,join(X1,join(X2,X0)))=meet(join(X1,join(X2,X0)),X0))),
% 46.79/6.53 inference(paramodulation,[status(thm)],[f6059,f6710])).
% 46.79/6.53 fof(f7282,plain,(
% 46.79/6.53 ![X0,X1,X2]: (X0=meet(join(X1,join(X2,X0)),X0))),
% 46.79/6.53 inference(forward_demodulation,[status(thm)],[f6059,f7226])).
% 46.79/6.53 fof(f7961,plain,(
% 46.79/6.53 ![X0,X1]: (meet(X0,meet(X0,X1))=meet(X1,X0))),
% 43.09/6.63 inference(paramodulation,[status(thm)],[f1166,f6759])).
% 43.09/6.63 fof(f10306,plain,(
% 43.09/6.63 ![X0]: (complement(converse(complement(X0)))=join(converse(X0),complement(converse(complement(X0)))))),
% 43.09/6.63 inference(paramodulation,[status(thm)],[f5277,f2476])).
% 43.09/6.63 fof(f10311,plain,(
% 43.09/6.63 ![X0]: (meet(X0,X0)=meet(converse(complement(converse(complement(X0)))),X0))),
% 43.09/6.63 inference(paramodulation,[status(thm)],[f5277,f7961])).
% 43.09/6.63 fof(f10355,plain,(
% 43.09/6.63 ![X0]: (X0=meet(converse(complement(converse(complement(X0)))),X0))),
% 43.09/6.63 inference(forward_demodulation,[status(thm)],[f1114,f10311])).
% 43.09/6.63 fof(f15551,plain,(
% 43.09/6.63 ![X0,X1]: (top=complement(meet(meet(X0,complement(X1)),X1)))),
% 43.09/6.63 inference(paramodulation,[status(thm)],[f2754,f1081])).
% 43.09/6.63 fof(f15739,plain,(
% 43.09/6.63 ![X0,X1]: (meet(meet(X0,complement(X1)),X1)=meet(converse(complement(converse(top))),meet(meet(X0,complement(X1)),X1)))),
% 43.09/6.63 inference(paramodulation,[status(thm)],[f15551,f10355])).
% 43.09/6.63 fof(f15791,plain,(
% 43.09/6.63 ![X0,X1]: (meet(meet(X0,complement(X1)),X1)=meet(converse(complement(top)),meet(meet(X0,complement(X1)),X1)))),
% 43.09/6.63 inference(forward_demodulation,[status(thm)],[f2616,f15739])).
% 43.09/6.63 fof(f15792,plain,(
% 43.09/6.63 ![X0,X1]: (meet(meet(X0,complement(X1)),X1)=meet(converse(zero),meet(meet(X0,complement(X1)),X1)))),
% 43.09/6.63 inference(forward_demodulation,[status(thm)],[f189,f15791])).
% 43.09/6.63 fof(f15793,plain,(
% 43.09/6.63 ![X0,X1]: (meet(meet(X0,complement(X1)),X1)=meet(zero,meet(meet(X0,complement(X1)),X1)))),
% 43.09/6.63 inference(forward_demodulation,[status(thm)],[f1608,f15792])).
% 43.09/6.63 fof(f15797,plain,(
% 43.09/6.63 ![X0,X1]: (meet(meet(X0,complement(X1)),X1)=zero)),
% 43.09/6.63 inference(forward_demodulation,[status(thm)],[f2067,f15793])).
% 43.09/6.63 fof(f15866,plain,(
% 43.09/6.63 ![X0,X1]: (meet(meet(X0,X1),complement(X1))=zero)),
% 43.09/6.63 inference(paramodulation,[status(thm)],[f1043,f15797])).
% 43.09/6.63 fof(f16316,plain,(
% 43.09/6.63 meet(sK0_skl,complement(converse(complement(sK1_skl))))=zero),
% 43.09/6.63 inference(paramodulation,[status(thm)],[f6617,f15866])).
% 43.09/6.63 fof(f35617,plain,(
% 43.09/6.63 ![X0,X1,X2,X3]: (meet(join(X0,complement(X1)),join(meet(join(X2,join(X3,X0)),X0),X1))=meet(join(X2,join(X3,X0)),X0))),
% 43.09/6.63 inference(paramodulation,[status(thm)],[f7282,f844])).
% 43.09/6.63 fof(f35911,plain,(
% 43.09/6.63 ![X0,X1,X2,X3]: (meet(join(X0,complement(X1)),join(X0,X1))=meet(join(X2,join(X3,X0)),X0))),
% 43.09/6.63 inference(forward_demodulation,[status(thm)],[f7282,f35617])).
% 43.09/6.63 fof(f35916,plain,(
% 43.09/6.63 ![X0,X1]: (meet(join(X0,complement(X1)),join(X0,X1))=X0)),
% 43.09/6.63 inference(forward_demodulation,[status(thm)],[f7282,f35911])).
% 43.09/6.63 fof(f38386,plain,(
% 43.09/6.63 ![X0]: (meet(join(X0,complement(converse(complement(converse(X0))))),top)=X0)),
% 43.09/6.63 inference(paramodulation,[status(thm)],[f2650,f35916])).
% 43.09/6.63 fof(f38641,plain,(
% 43.09/6.63 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=X0)),
% 43.09/6.63 inference(forward_demodulation,[status(thm)],[f1260,f38386])).
% 43.09/6.63 fof(f43021,plain,(
% 43.09/6.63 ![X0]: (join(converse(X0),complement(converse(complement(X0))))=converse(X0))),
% 43.09/6.63 inference(paramodulation,[status(thm)],[f23,f38641])).
% 43.09/6.63 fof(f43124,plain,(
% 43.09/6.63 ![X0]: (complement(converse(complement(X0)))=converse(X0))),
% 43.09/6.63 inference(backward_demodulation,[status(thm)],[f43021,f10306])).
% 43.09/6.63 fof(f43182,plain,(
% 43.09/6.63 meet(sK0_skl,converse(sK1_skl))=zero),
% 43.09/6.63 inference(backward_demodulation,[status(thm)],[f43124,f16316])).
% 43.09/6.63 fof(f43250,plain,(
% 43.09/6.63 $false),
% 43.09/6.63 inference(forward_subsumption_resolution,[status(thm)],[f43182,f32])).
% 43.09/6.63 % SZS output end CNFRefutation for theBenchmark.p
% 17.85/6.68 % Elapsed time: 6.197459 seconds
% 17.85/6.68 % CPU time: 48.404179 seconds
% 17.85/6.68 % Total memory used: 301.780 MB
% 17.85/6.68 % Net memory used: 295.106 MB
%------------------------------------------------------------------------------