%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL005+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 : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:03:31 PM UTC 2026
% Result : Theorem 47.58s 6.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL005+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n011.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:57:40 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 47.58/6.42 % Refutation found
% 47.58/6.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 47.58/6.42 % SZS output start CNFRefutation for theBenchmark
% 47.58/6.42 fof(f1,axiom,(
% 47.58/6.42 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 47.58/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 47.58/6.42 fof(f2,axiom,(
% 47.58/6.42 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 47.58/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 47.58/6.42 fof(f3,axiom,(
% 47.58/6.42 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 47.58/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 47.58/6.42 fof(f4,axiom,(
% 47.58/6.42 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 47.58/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 47.58/6.42 fof(f6,axiom,(
% 47.58/6.42 (! [X0] : composition(X0,one) = X0 )),
% 47.58/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 47.58/6.42 fof(f8,axiom,(
% 47.58/6.42 (! [X0] : converse(converse(X0)) = X0 )),
% 47.58/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 47.58/6.42 fof(f9,axiom,(
% 47.58/6.42 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 47.58/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 47.58/6.42 fof(f10,axiom,(
% 47.58/6.42 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 47.58/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 47.58/6.42 fof(f11,axiom,(
% 47.58/6.42 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 47.58/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 47.58/6.42 fof(f12,axiom,(
% 47.58/6.42 (! [X0] : top = join(X0,complement(X0)) )),
% 47.58/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 47.58/6.42 fof(f13,axiom,(
% 47.58/6.42 (! [X0] : zero = meet(X0,complement(X0)) )),
% 47.58/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 47.58/6.42 fof(f14,conjecture,(
% 47.58/6.42 (! [X0,X1] : converse(meet(X0,X1)) = meet(converse(X0),converse(X1)) )),
% 47.58/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 47.58/6.42 fof(f15,negated_conjecture,(
% 47.58/6.42 ~((! [X0,X1] : converse(meet(X0,X1)) = meet(converse(X0),converse(X1)) ))),
% 47.58/6.42 inference(negated_conjecture,[status(cth)],[f14])).
% 47.58/6.42 fof(f16,plain,(
% 47.58/6.42 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 47.58/6.42 inference(cnf_transformation,[status(thm)],[f1])).
% 47.58/6.42 fof(f17,plain,(
% 47.58/6.42 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 47.58/6.42 inference(cnf_transformation,[status(thm)],[f2])).
% 47.58/6.42 fof(f18,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 47.58/6.42 inference(cnf_transformation,[status(thm)],[f3])).
% 47.58/6.42 fof(f19,plain,(
% 47.58/6.42 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 47.58/6.42 inference(cnf_transformation,[status(thm)],[f4])).
% 47.58/6.42 fof(f21,plain,(
% 47.58/6.42 ![X0]: (composition(X0,one)=X0)),
% 47.58/6.42 inference(cnf_transformation,[status(thm)],[f6])).
% 47.58/6.42 fof(f23,plain,(
% 47.58/6.42 ![X0]: (converse(converse(X0))=X0)),
% 47.58/6.42 inference(cnf_transformation,[status(thm)],[f8])).
% 47.58/6.42 fof(f24,plain,(
% 47.58/6.42 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 47.58/6.42 inference(cnf_transformation,[status(thm)],[f9])).
% 47.58/6.42 fof(f25,plain,(
% 47.58/6.42 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 47.58/6.42 inference(cnf_transformation,[status(thm)],[f10])).
% 47.58/6.42 fof(f26,plain,(
% 47.58/6.42 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 47.58/6.42 inference(cnf_transformation,[status(thm)],[f11])).
% 47.58/6.42 fof(f27,plain,(
% 47.58/6.42 ![X0]: (top=join(X0,complement(X0)))),
% 47.58/6.42 inference(cnf_transformation,[status(thm)],[f12])).
% 47.58/6.42 fof(f28,plain,(
% 47.58/6.42 ![X0]: (zero=meet(X0,complement(X0)))),
% 47.58/6.42 inference(cnf_transformation,[status(thm)],[f13])).
% 47.58/6.42 fof(f29,plain,(
% 47.58/6.42 (?[X0,X1]: ~converse(meet(X0,X1))=meet(converse(X0),converse(X1)))),
% 47.58/6.42 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 47.58/6.42 fof(f30,plain,(
% 47.58/6.42 ~converse(meet(sK0_skl,sK1_skl))=meet(converse(sK0_skl),converse(sK1_skl))),
% 47.58/6.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl)],[f29])).
% 47.58/6.42 fof(f31,plain,(
% 47.58/6.42 ~converse(meet(sK0_skl,sK1_skl))=meet(converse(sK0_skl),converse(sK1_skl))),
% 47.58/6.42 inference(cnf_transformation,[status(thm)],[f30])).
% 47.58/6.42 fof(f38,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f18])).
% 47.58/6.42 fof(f39,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 47.58/6.42 inference(backward_demodulation,[status(thm)],[f19,f38])).
% 47.58/6.42 fof(f40,plain,(
% 47.58/6.42 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f26])).
% 47.58/6.42 fof(f41,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f39])).
% 47.58/6.42 fof(f44,plain,(
% 47.58/6.42 ![X0,X1,X2]: (meet(X0,join(complement(X1),complement(X2)))=complement(join(complement(X0),meet(X1,X2))))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f19,f19])).
% 47.58/6.42 fof(f45,plain,(
% 47.58/6.42 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f23,f24])).
% 47.58/6.42 fof(f46,plain,(
% 47.58/6.42 ![X0,X1]: (converse(join(X0,converse(X1)))=join(converse(X0),X1))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f23,f24])).
% 47.58/6.42 fof(f48,plain,(
% 47.58/6.42 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f23,f25])).
% 47.58/6.42 fof(f65,plain,(
% 47.58/6.42 ![X0,X1]: (join(complement(X0),composition(X1,complement(composition(converse(X1),X0))))=complement(X0))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f23,f40])).
% 47.58/6.42 fof(f69,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f19,f41])).
% 47.58/6.42 fof(f72,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f69])).
% 47.58/6.42 fof(f148,plain,(
% 47.58/6.42 ![X0,X1,X2]: (join(meet(X0,X1),composition(X2,complement(composition(converse(X2),join(complement(X0),complement(X1))))))=complement(join(complement(X0),complement(X1))))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f19,f65])).
% 47.58/6.42 fof(f156,plain,(
% 47.58/6.42 ![X0,X1,X2]: (join(meet(X0,X1),composition(X2,complement(composition(converse(X2),join(complement(X0),complement(X1))))))=meet(X0,X1))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f19,f148])).
% 47.58/6.42 fof(f303,plain,(
% 47.58/6.42 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f21,f48])).
% 47.58/6.42 fof(f307,plain,(
% 47.58/6.42 ![X0]: (X0=composition(converse(one),X0))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f23,f303])).
% 47.58/6.42 fof(f312,plain,(
% 47.58/6.42 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f27,f45])).
% 47.58/6.42 fof(f319,plain,(
% 47.58/6.42 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f27,f19])).
% 47.58/6.42 fof(f337,plain,(
% 47.58/6.42 zero=complement(top)),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f28,f319])).
% 47.58/6.42 fof(f340,plain,(
% 47.58/6.42 top=join(top,zero)),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f337,f27])).
% 47.58/6.42 fof(f439,plain,(
% 47.58/6.42 one=converse(one)),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f21,f307])).
% 47.58/6.42 fof(f443,plain,(
% 47.58/6.42 ![X0,X1]: (join(meet(X0,X1),composition(one,complement(join(complement(X0),complement(X1)))))=meet(X0,X1))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f307,f156])).
% 47.58/6.42 fof(f448,plain,(
% 47.58/6.42 ![X0]: (join(complement(X0),composition(one,complement(X0)))=complement(X0))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f307,f65])).
% 47.58/6.42 fof(f466,plain,(
% 47.58/6.42 ![X0]: (X0=composition(one,X0))),
% 47.58/6.42 inference(backward_demodulation,[status(thm)],[f439,f307])).
% 47.58/6.42 fof(f467,plain,(
% 47.58/6.42 ![X0,X1]: (join(meet(X0,X1),composition(one,meet(X0,X1)))=meet(X0,X1))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f19,f443])).
% 47.58/6.42 fof(f489,plain,(
% 47.58/6.42 ![X0,X1]: (join(meet(X0,X1),meet(X0,X1))=meet(X0,X1))),
% 47.58/6.42 inference(backward_demodulation,[status(thm)],[f466,f467])).
% 47.58/6.42 fof(f496,plain,(
% 47.58/6.42 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 47.58/6.42 inference(backward_demodulation,[status(thm)],[f466,f448])).
% 47.58/6.42 fof(f600,plain,(
% 47.58/6.42 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f496,f19])).
% 47.58/6.42 fof(f601,plain,(
% 47.58/6.42 ![X0]: (X0=join(meet(X0,complement(X0)),complement(complement(X0))))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f496,f41])).
% 47.58/6.42 fof(f622,plain,(
% 47.58/6.42 ![X0]: (X0=join(complement(complement(X0)),meet(X0,complement(X0))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f601])).
% 47.58/6.42 fof(f623,plain,(
% 47.58/6.42 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f28,f622])).
% 47.58/6.42 fof(f624,plain,(
% 47.58/6.42 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f623])).
% 47.58/6.42 fof(f628,plain,(
% 47.58/6.42 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(meet(X0,X1))))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f19,f624])).
% 47.58/6.42 fof(f647,plain,(
% 47.58/6.42 ![X0]: (join(complement(complement(X0)),meet(X0,X0))=complement(complement(X0)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f600,f496])).
% 47.58/6.42 fof(f650,plain,(
% 47.58/6.42 ![X0]: (top=join(complement(X0),meet(X0,X0)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f600,f27])).
% 47.58/6.42 fof(f850,plain,(
% 47.58/6.42 ![X0]: (join(meet(X0,X0),complement(complement(X0)))=meet(X0,X0))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f600,f489])).
% 47.58/6.42 fof(f917,plain,(
% 47.58/6.42 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f16,f19])).
% 47.58/6.42 fof(f918,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(X1,complement(X0)))))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f16,f41])).
% 47.58/6.42 fof(f919,plain,(
% 47.58/6.42 ![X0,X1]: (converse(join(converse(X0),X1))=join(converse(X1),X0))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f16,f46])).
% 47.58/6.42 fof(f935,plain,(
% 47.58/6.42 ![X0,X1]: (join(X0,join(X1,complement(join(X0,X1))))=top)),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f27,f17])).
% 47.58/6.42 fof(f936,plain,(
% 47.58/6.42 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f16,f17])).
% 47.58/6.42 fof(f939,plain,(
% 47.58/6.42 ![X0,X1]: (join(zero,join(complement(complement(X0)),X1))=join(X0,X1))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f624,f17])).
% 47.58/6.42 fof(f949,plain,(
% 47.58/6.42 ![X0,X1,X2]: (join(meet(X0,X1),join(complement(join(complement(X0),X1)),X2))=join(X0,X2))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f41,f17])).
% 47.58/6.42 fof(f950,plain,(
% 47.58/6.42 ![X0,X1]: (join(complement(X0),join(meet(X0,X0),X1))=join(top,X1))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f650,f17])).
% 47.58/6.42 fof(f955,plain,(
% 47.58/6.42 ![X0,X1]: (join(X0,join(converse(complement(converse(X0))),X1))=join(converse(top),X1))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f312,f17])).
% 47.58/6.42 fof(f1314,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f19,f918])).
% 47.58/6.42 fof(f1320,plain,(
% 47.58/6.42 ![X0,X1]: (join(X0,complement(X1))=join(meet(join(X0,complement(X1)),meet(X1,X0)),complement(X1)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f918,f918])).
% 47.58/6.42 fof(f1344,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f1314])).
% 47.58/6.42 fof(f1353,plain,(
% 47.58/6.42 ![X0,X1]: (join(X0,complement(X1))=join(complement(X1),meet(join(X0,complement(X1)),meet(X1,X0))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f1320])).
% 47.58/6.42 fof(f1370,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(meet(complement(X1),X0),meet(X0,meet(X1,X1))))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f600,f1344])).
% 47.58/6.42 fof(f1471,plain,(
% 47.58/6.42 ![X0]: (join(zero,complement(complement(X0)))=join(X0,meet(X0,X0)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f647,f939])).
% 47.58/6.42 fof(f1473,plain,(
% 47.58/6.42 ![X0]: (join(zero,top)=join(X0,meet(complement(X0),complement(X0))))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f650,f939])).
% 47.58/6.42 fof(f1474,plain,(
% 47.58/6.42 ![X0]: (join(zero,complement(complement(X0)))=join(X0,complement(complement(X0))))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f496,f939])).
% 47.58/6.42 fof(f1490,plain,(
% 47.58/6.42 ![X0]: (X0=join(X0,meet(X0,X0)))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f624,f1471])).
% 47.58/6.42 fof(f1492,plain,(
% 47.58/6.42 ![X0]: (join(top,zero)=join(X0,meet(complement(X0),complement(X0))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f1473])).
% 47.58/6.42 fof(f1493,plain,(
% 47.58/6.42 ![X0]: (top=join(X0,meet(complement(X0),complement(X0))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f340,f1492])).
% 47.58/6.42 fof(f1494,plain,(
% 47.58/6.42 ![X0]: (top=join(X0,complement(complement(complement(X0)))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f600,f1493])).
% 47.58/6.42 fof(f1495,plain,(
% 47.58/6.42 ![X0]: (X0=join(X0,complement(complement(X0))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f624,f1474])).
% 47.58/6.42 fof(f1514,plain,(
% 47.58/6.42 ![X0]: (meet(X0,join(complement(complement(X0)),complement(complement(X0))))=complement(complement(X0)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f1490,f44])).
% 47.58/6.42 fof(f1524,plain,(
% 47.58/6.42 ![X0]: (meet(X0,complement(complement(X0)))=complement(complement(X0)))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f496,f1514])).
% 47.58/6.42 fof(f1549,plain,(
% 47.58/6.42 ![X0,X1]: (join(X0,join(complement(complement(X0)),X1))=join(X0,X1))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f1495,f17])).
% 47.58/6.42 fof(f1588,plain,(
% 47.58/6.42 ![X0]: (meet(X0,complement(complement(complement(X0))))=complement(top))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f1494,f19])).
% 47.58/6.42 fof(f1589,plain,(
% 47.58/6.42 ![X0]: (X0=join(meet(X0,complement(complement(complement(complement(X0))))),complement(top)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f1494,f41])).
% 47.58/6.42 fof(f1590,plain,(
% 47.58/6.42 ![X0]: (complement(complement(X0))=join(meet(complement(complement(X0)),X0),complement(top)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f1494,f918])).
% 47.58/6.42 fof(f1609,plain,(
% 47.58/6.42 ![X0]: (meet(X0,complement(complement(complement(X0))))=zero)),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f337,f1588])).
% 47.58/6.42 fof(f1610,plain,(
% 47.58/6.42 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(complement(complement(X0)))))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f1589])).
% 47.58/6.42 fof(f1611,plain,(
% 47.58/6.42 ![X0]: (X0=join(zero,meet(X0,complement(complement(complement(complement(X0)))))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f337,f1610])).
% 47.58/6.42 fof(f1612,plain,(
% 47.58/6.42 ![X0]: (complement(complement(X0))=join(complement(top),meet(complement(complement(X0)),X0)))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f1590])).
% 47.58/6.42 fof(f1613,plain,(
% 47.58/6.42 ![X0]: (complement(complement(X0))=join(zero,meet(complement(complement(X0)),X0)))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f337,f1612])).
% 47.58/6.42 fof(f2113,plain,(
% 47.58/6.42 ![X0]: (X0=join(meet(complement(complement(X0)),X0),zero))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f1609,f1344])).
% 47.58/6.42 fof(f2116,plain,(
% 47.58/6.42 ![X0]: (complement(complement(complement(X0)))=join(zero,meet(complement(complement(complement(X0))),complement(X0))))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f1609,f1344])).
% 47.58/6.42 fof(f2138,plain,(
% 47.58/6.42 ![X0]: (complement(complement(X0))=X0)),
% 47.58/6.42 inference(backward_demodulation,[status(thm)],[f2139,f1613])).
% 47.58/6.42 fof(f2139,plain,(
% 47.58/6.42 ![X0]: (X0=join(zero,meet(complement(complement(X0)),X0)))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f2113])).
% 47.58/6.42 fof(f2155,plain,(
% 47.58/6.42 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 47.58/6.42 inference(backward_demodulation,[status(thm)],[f2167,f1611])).
% 47.58/6.42 fof(f2167,plain,(
% 47.58/6.42 ![X0]: (complement(complement(complement(X0)))=complement(X0))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f2139,f2116])).
% 47.58/6.42 fof(f2206,plain,(
% 47.58/6.42 ![X0]: (join(meet(X0,X0),X0)=meet(X0,X0))),
% 47.58/6.42 inference(backward_demodulation,[status(thm)],[f2138,f850])).
% 47.58/6.42 fof(f2233,plain,(
% 47.58/6.42 ![X0,X1]: (join(X0,join(X0,X1))=join(X0,X1))),
% 47.58/6.42 inference(backward_demodulation,[status(thm)],[f2138,f1549])).
% 47.58/6.42 fof(f2253,plain,(
% 47.58/6.42 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f1524,f2155])).
% 47.58/6.42 fof(f2258,plain,(
% 47.58/6.42 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 47.58/6.42 inference(backward_demodulation,[status(thm)],[f2287,f628])).
% 47.58/6.42 fof(f2287,plain,(
% 47.58/6.42 ![X0]: (X0=join(zero,X0))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f2138,f2253])).
% 47.58/6.42 fof(f2310,plain,(
% 47.58/6.42 ![X0]: (join(X0,meet(X0,X0))=meet(X0,X0))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f2206])).
% 47.58/6.42 fof(f2323,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(meet(complement(X1),X0),meet(X0,X1)))),
% 47.58/6.42 inference(backward_demodulation,[status(thm)],[f2348,f1370])).
% 47.58/6.42 fof(f2325,plain,(
% 47.58/6.42 ![X0,X1]: (join(complement(X0),join(X0,X1))=join(top,X1))),
% 47.58/6.42 inference(backward_demodulation,[status(thm)],[f2348,f950])).
% 47.58/6.42 fof(f2348,plain,(
% 47.58/6.42 ![X0]: (X0=meet(X0,X0))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f1490,f2310])).
% 47.58/6.42 fof(f2440,plain,(
% 47.58/6.42 ![X0,X1]: (meet(X0,X1)=complement(complement(meet(X1,X0))))),
% 47.58/6.42 inference(backward_demodulation,[status(thm)],[f2258,f917])).
% 47.58/6.42 fof(f2566,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f2323])).
% 47.58/6.42 fof(f2567,plain,(
% 47.58/6.42 ![X0,X1]: (join(X0,join(X1,complement(X0)))=join(top,X1))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f936,f2325])).
% 47.58/6.42 fof(f2625,plain,(
% 47.58/6.42 ![X0,X1]: (join(X0,complement(X1))=join(complement(X1),meet(meet(X1,X0),join(X0,complement(X1)))))),
% 47.58/6.42 inference(backward_demodulation,[status(thm)],[f2626,f1353])).
% 47.58/6.42 fof(f2626,plain,(
% 47.58/6.42 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f2138,f2440])).
% 47.58/6.42 fof(f2648,plain,(
% 47.58/6.42 ![X0]: (X0=join(X0,meet(X0,complement(X0))))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f2348,f1344])).
% 47.58/6.42 fof(f2661,plain,(
% 47.58/6.42 ![X0]: (X0=join(X0,zero))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f28,f2648])).
% 47.58/6.42 fof(f2879,plain,(
% 47.58/6.42 ![X0,X1]: (join(meet(X0,X1),X1)=join(meet(X0,X1),meet(X1,complement(X0))))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f1344,f2233])).
% 47.58/6.42 fof(f2880,plain,(
% 47.58/6.42 ![X0,X1]: (join(meet(X0,X1),X0)=join(meet(X0,X1),meet(X0,complement(X1))))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f72,f2233])).
% 47.58/6.42 fof(f2891,plain,(
% 47.58/6.42 ![X0]: (join(X0,top)=join(X0,complement(X0)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f27,f2233])).
% 47.58/6.42 fof(f2906,plain,(
% 47.58/6.42 ![X0,X1]: (join(X0,meet(X1,X0))=join(meet(X1,X0),meet(X0,complement(X1))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f2879])).
% 47.58/6.42 fof(f2909,plain,(
% 47.58/6.42 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f1344,f2906])).
% 47.58/6.42 fof(f2910,plain,(
% 47.58/6.42 ![X0,X1]: (join(X0,meet(X0,X1))=join(meet(X0,X1),meet(X0,complement(X1))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f2880])).
% 47.58/6.42 fof(f2924,plain,(
% 47.58/6.42 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f72,f2910])).
% 47.58/6.42 fof(f2941,plain,(
% 47.58/6.42 ![X0]: (join(X0,top)=top)),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f27,f2891])).
% 47.58/6.42 fof(f2991,plain,(
% 47.58/6.42 ![X0]: (join(top,X0)=top)),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f16,f2941])).
% 47.58/6.42 fof(f3017,plain,(
% 47.58/6.42 ![X0,X1]: (join(X0,join(X1,complement(X0)))=top)),
% 47.58/6.42 inference(backward_demodulation,[status(thm)],[f2991,f2567])).
% 47.58/6.42 fof(f3058,plain,(
% 47.58/6.42 converse(top)=top),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f312,f2991])).
% 47.58/6.42 fof(f3076,plain,(
% 47.58/6.42 ![X0]: (top=join(X0,converse(complement(converse(X0)))))),
% 47.58/6.42 inference(backward_demodulation,[status(thm)],[f3058,f312])).
% 47.58/6.42 fof(f3080,plain,(
% 47.58/6.42 ![X0,X1]: (join(X0,join(converse(complement(converse(X0))),X1))=join(top,X1))),
% 47.58/6.42 inference(backward_demodulation,[status(thm)],[f3058,f955])).
% 47.58/6.42 fof(f3099,plain,(
% 47.58/6.42 ![X0,X1]: (join(X0,join(converse(complement(converse(X0))),X1))=top)),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f2991,f3080])).
% 47.58/6.42 fof(f3281,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(meet(X0,join(X1,complement(join(complement(X0),X1)))),complement(top)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f935,f41])).
% 47.58/6.42 fof(f3316,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(complement(top),meet(X0,join(X1,complement(join(complement(X0),X1))))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f3281])).
% 47.58/6.42 fof(f3317,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(zero,meet(X0,join(X1,complement(join(complement(X0),X1))))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f337,f3316])).
% 47.58/6.42 fof(f3318,plain,(
% 47.58/6.42 ![X0,X1]: (X0=meet(X0,join(X1,complement(join(complement(X0),X1)))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f2287,f3317])).
% 47.58/6.42 fof(f3343,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(meet(X0,join(X1,complement(complement(X0)))),complement(top)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f3017,f41])).
% 47.58/6.42 fof(f3358,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(complement(top),meet(X0,join(X1,complement(complement(X0))))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f16,f3343])).
% 47.58/6.42 fof(f3359,plain,(
% 47.58/6.42 ![X0,X1]: (X0=join(zero,meet(X0,join(X1,complement(complement(X0))))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f337,f3358])).
% 47.58/6.42 fof(f3360,plain,(
% 47.58/6.42 ![X0,X1]: (X0=meet(X0,join(X1,complement(complement(X0)))))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f2287,f3359])).
% 47.58/6.42 fof(f3361,plain,(
% 47.58/6.42 ![X0,X1]: (X0=meet(X0,join(X1,X0)))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f2138,f3360])).
% 47.58/6.42 fof(f3386,plain,(
% 47.58/6.42 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X1))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f2909,f3361])).
% 47.58/6.42 fof(f3394,plain,(
% 47.58/6.42 ![X0,X1]: (X0=meet(X0,join(X0,X1)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f16,f3361])).
% 47.58/6.42 fof(f3416,plain,(
% 47.58/6.42 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X0,X1)))),
% 47.58/6.42 inference(forward_demodulation,[status(thm)],[f2626,f3386])).
% 47.58/6.42 fof(f3515,plain,(
% 47.58/6.42 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X1,X0)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f2626,f3416])).
% 47.58/6.42 fof(f3638,plain,(
% 47.58/6.42 ![X0,X1,X2]: (meet(X0,X1)=meet(meet(X0,X1),join(X0,X2)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f949,f3394])).
% 47.58/6.42 fof(f4159,plain,(
% 47.58/6.42 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X1,X0)))),
% 47.58/6.42 inference(paramodulation,[status(thm)],[f16,f2258])).
% 47.58/6.42 fof(f4161,plain,(
% 47.58/6.42 ![X0,X1]: (join(X0,complement(X1))=complement(meet(complement(X0),X1)))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f2138,f2258])).
% 47.58/6.43 fof(f4164,plain,(
% 47.58/6.43 ![X0,X1]: (join(complement(X0),X1)=complement(meet(X0,complement(X1))))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f2138,f2258])).
% 47.58/6.43 fof(f5502,plain,(
% 47.58/6.43 ![X0,X1,X2]: (meet(X0,meet(X0,X1))=meet(meet(X1,X0),join(X0,X2)))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f3515,f3638])).
% 47.58/6.43 fof(f5579,plain,(
% 47.58/6.43 ![X0,X1]: (join(X0,complement(X1))=join(complement(X1),meet(X1,X0)))),
% 47.58/6.43 inference(backward_demodulation,[status(thm)],[f5580,f2625])).
% 47.58/6.43 fof(f5580,plain,(
% 47.58/6.43 ![X0,X1,X2]: (meet(X0,X1)=meet(meet(X0,X1),join(X1,X2)))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f3515,f5502])).
% 47.58/6.43 fof(f5647,plain,(
% 47.58/6.43 ![X0,X1]: (join(complement(X0),X1)=complement(meet(complement(X1),X0)))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f2138,f4159])).
% 47.58/6.43 fof(f5745,plain,(
% 47.58/6.43 ![X0,X1]: (complement(join(X0,complement(X1)))=meet(complement(X0),X1))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f4161,f2138])).
% 47.58/6.43 fof(f5849,plain,(
% 47.58/6.43 ![X0,X1]: (complement(join(complement(X0),X1))=meet(X0,complement(X1)))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f4164,f2138])).
% 47.58/6.43 fof(f5922,plain,(
% 47.58/6.43 ![X0,X1]: (X0=meet(X0,join(X1,meet(X0,complement(X1)))))),
% 47.58/6.43 inference(backward_demodulation,[status(thm)],[f5849,f3318])).
% 47.58/6.43 fof(f5985,plain,(
% 47.58/6.43 ![X0,X1]: (join(join(X0,meet(X1,complement(X0))),X1)=join(X0,meet(X1,complement(X0))))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f5922,f2909])).
% 47.58/6.43 fof(f6025,plain,(
% 47.58/6.43 ![X0,X1]: (join(X0,join(meet(X1,complement(X0)),X1))=join(X0,meet(X1,complement(X0))))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f17,f5985])).
% 47.58/6.43 fof(f6026,plain,(
% 47.58/6.43 ![X0,X1]: (join(X0,join(X1,meet(X1,complement(X0))))=join(X0,meet(X1,complement(X0))))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f16,f6025])).
% 47.58/6.43 fof(f6036,plain,(
% 47.58/6.43 ![X0,X1]: (join(X0,X1)=join(X0,meet(X1,complement(X0))))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f2924,f6026])).
% 47.58/6.43 fof(f6053,plain,(
% 47.58/6.43 ![X0,X1]: (join(X0,X1)=join(X0,meet(complement(X0),X1)))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f2626,f6036])).
% 47.58/6.43 fof(f7585,plain,(
% 47.58/6.43 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X2,X0)))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f16,f936])).
% 47.58/6.43 fof(f8377,plain,(
% 47.58/6.43 ![X0,X1]: (complement(join(complement(X0),X1))=meet(complement(X1),X0))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f5647,f2138])).
% 47.58/6.43 fof(f8624,plain,(
% 47.58/6.43 ![X0,X1]: (complement(join(X0,X1))=meet(complement(X0),complement(X1)))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f2138,f5745])).
% 47.58/6.43 fof(f10890,plain,(
% 47.58/6.43 ![X0,X1]: (join(X0,complement(X1))=join(X0,complement(join(X0,X1))))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f8624,f6053])).
% 47.58/6.43 fof(f15797,plain,(
% 47.58/6.43 ![X0,X1]: (join(meet(X0,X1),complement(X0))=join(complement(X0),meet(X1,X0)))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f3515,f5579])).
% 47.58/6.43 fof(f15945,plain,(
% 47.58/6.43 ![X0,X1]: (join(complement(X0),meet(X0,X1))=join(complement(X0),meet(X1,X0)))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f16,f15797])).
% 47.58/6.43 fof(f15946,plain,(
% 47.58/6.43 ![X0,X1]: (join(X0,complement(X1))=join(complement(X1),meet(X0,X1)))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f5579,f15945])).
% 47.58/6.43 fof(f17627,plain,(
% 47.58/6.43 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=join(X0,complement(top)))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f3076,f10890])).
% 47.58/6.43 fof(f17635,plain,(
% 47.58/6.43 ![X0,X1]: (join(X0,complement(join(converse(complement(converse(X0))),X1)))=join(X0,complement(top)))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f3099,f10890])).
% 47.58/6.43 fof(f17858,plain,(
% 47.58/6.43 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=join(X0,zero))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f337,f17627])).
% 47.58/6.43 fof(f17859,plain,(
% 47.58/6.43 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=X0)),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f2661,f17858])).
% 47.58/6.43 fof(f17870,plain,(
% 47.58/6.43 ![X0,X1]: (join(X0,complement(join(converse(complement(converse(X0))),X1)))=join(X0,zero))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f337,f17635])).
% 47.58/6.43 fof(f17871,plain,(
% 47.58/6.43 ![X0,X1]: (join(X0,complement(join(converse(complement(converse(X0))),X1)))=X0)),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f2661,f17870])).
% 47.58/6.43 fof(f18041,plain,(
% 47.58/6.43 ![X0]: (converse(converse(X0))=join(converse(complement(converse(complement(converse(converse(X0)))))),X0))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f17859,f919])).
% 47.58/6.43 fof(f18122,plain,(
% 47.58/6.43 ![X0]: (X0=join(converse(complement(converse(complement(converse(converse(X0)))))),X0))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f23,f18041])).
% 47.58/6.43 fof(f18123,plain,(
% 47.58/6.43 ![X0]: (X0=join(X0,converse(complement(converse(complement(converse(converse(X0))))))))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f16,f18122])).
% 47.58/6.43 fof(f18125,plain,(
% 47.58/6.43 ![X0]: (X0=join(X0,converse(complement(converse(complement(X0))))))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f23,f18123])).
% 47.58/6.43 fof(f19070,plain,(
% 47.58/6.43 ![X0,X1]: (complement(complement(X0))=meet(complement(complement(join(converse(complement(converse(complement(X0)))),X1))),X0))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f17871,f8377])).
% 47.58/6.43 fof(f19168,plain,(
% 47.58/6.43 ![X0,X1]: (X0=meet(complement(complement(join(converse(complement(converse(complement(X0)))),X1))),X0))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f2138,f19070])).
% 47.58/6.43 fof(f19169,plain,(
% 47.58/6.43 ![X0,X1]: (X0=meet(X0,complement(complement(join(converse(complement(converse(complement(X0)))),X1)))))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f2626,f19168])).
% 47.58/6.43 fof(f19171,plain,(
% 47.58/6.43 ![X0,X1]: (X0=meet(X0,join(converse(complement(converse(complement(X0)))),X1)))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f2138,f19169])).
% 47.58/6.43 fof(f20053,plain,(
% 47.58/6.43 ![X0,X1]: (join(converse(complement(converse(complement(complement(X0))))),X1)=join(meet(join(converse(complement(converse(complement(complement(X0))))),X1),X0),complement(X0)))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f19171,f2566])).
% 47.58/6.43 fof(f20120,plain,(
% 47.58/6.43 ![X0,X1]: (join(converse(complement(converse(X0))),X1)=join(meet(join(converse(complement(converse(complement(complement(X0))))),X1),X0),complement(X0)))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f2138,f20053])).
% 47.58/6.43 fof(f20121,plain,(
% 47.58/6.43 ![X0,X1]: (join(converse(complement(converse(X0))),X1)=join(complement(X0),meet(join(converse(complement(converse(complement(complement(X0))))),X1),X0)))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f16,f20120])).
% 47.58/6.43 fof(f20122,plain,(
% 47.58/6.43 ![X0,X1]: (join(converse(complement(converse(X0))),X1)=join(join(converse(complement(converse(complement(complement(X0))))),X1),complement(X0)))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f15946,f20121])).
% 47.58/6.43 fof(f20123,plain,(
% 47.58/6.43 ![X0,X1]: (join(converse(complement(converse(X0))),X1)=join(X1,join(complement(X0),converse(complement(converse(complement(complement(X0))))))))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f7585,f20122])).
% 47.58/6.43 fof(f20158,plain,(
% 47.58/6.43 ![X0,X1]: (join(converse(complement(converse(X0))),X1)=join(X1,complement(X0)))),
% 47.58/6.43 inference(forward_demodulation,[status(thm)],[f18125,f20123])).
% 47.58/6.43 fof(f20348,plain,(
% 47.58/6.43 ![X0]: (converse(complement(converse(X0)))=join(zero,complement(X0)))),
% 47.58/6.43 inference(paramodulation,[status(thm)],[f2661,f20158])).
% 47.58/6.43 fof(f20376,plain,(
% 47.58/6.43 ![X0,X1]: (converse(join(X0,complement(X1)))=join(complement(converse(X1)),converse(X0)))),
% 47.58/6.53 inference(paramodulation,[status(thm)],[f20158,f45])).
% 47.58/6.53 fof(f20613,plain,(
% 47.58/6.53 ![X0]: (converse(complement(converse(X0)))=complement(X0))),
% 47.58/6.53 inference(forward_demodulation,[status(thm)],[f2287,f20348])).
% 47.58/6.53 fof(f21250,plain,(
% 47.58/6.53 ![X0]: (converse(complement(X0))=complement(converse(X0)))),
% 47.58/6.53 inference(paramodulation,[status(thm)],[f23,f20613])).
% 47.58/6.53 fof(f21499,plain,(
% 47.58/6.53 ![X0,X1]: (converse(meet(complement(X0),X1))=complement(converse(join(X0,complement(X1)))))),
% 47.58/6.53 inference(paramodulation,[status(thm)],[f5745,f21250])).
% 47.58/6.53 fof(f31527,plain,(
% 47.58/6.53 ![X0,X1]: (complement(converse(join(X0,complement(X1))))=meet(complement(converse(X0)),converse(X1)))),
% 47.58/6.53 inference(paramodulation,[status(thm)],[f20376,f8377])).
% 47.58/6.53 fof(f31636,plain,(
% 47.58/6.53 ![X0,X1]: (converse(meet(complement(X0),X1))=meet(complement(converse(X0)),converse(X1)))),
% 47.58/6.53 inference(forward_demodulation,[status(thm)],[f21499,f31527])).
% 47.58/6.53 fof(f34264,plain,(
% 47.58/6.53 ![X0,X1]: (converse(meet(complement(complement(X0)),X1))=meet(complement(complement(converse(X0))),converse(X1)))),
% 47.58/6.53 inference(paramodulation,[status(thm)],[f21250,f31636])).
% 47.58/6.53 fof(f34366,plain,(
% 47.58/6.53 ![X0,X1]: (converse(meet(X0,X1))=meet(complement(complement(converse(X0))),converse(X1)))),
% 47.58/6.53 inference(forward_demodulation,[status(thm)],[f2138,f34264])).
% 47.58/6.53 fof(f34367,plain,(
% 47.58/6.53 ~converse(meet(sK0_skl,sK1_skl))=converse(meet(sK0_skl,sK1_skl))),
% 47.58/6.53 inference(backward_demodulation,[status(thm)],[f34408,f31])).
% 47.58/6.53 fof(f34408,plain,(
% 47.58/6.53 ![X0,X1]: (converse(meet(X0,X1))=meet(converse(X0),converse(X1)))),
% 47.58/6.53 inference(forward_demodulation,[status(thm)],[f2138,f34366])).
% 47.58/6.53 fof(f34597,plain,(
% 47.58/6.53 $false),
% 47.58/6.53 inference(trivial_equality_resolution,[status(thm)],[f34367])).
% 47.58/6.53 % SZS output end CNFRefutation for theBenchmark.p
% 47.58/6.56 % Elapsed time: 6.186312 seconds
% 47.58/6.56 % CPU time: 48.656856 seconds
% 47.58/6.56 % Total memory used: 463.406 MB
% 47.58/6.56 % Net memory used: 453.605 MB
%------------------------------------------------------------------------------