%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL019+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 : n016.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:36 PM UTC 2026
% Result : Theorem 230.81s 29.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL019+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.17/0.44 % Computer : n016.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 04:05:07 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.45 % Drodi V4.1.1
% 230.81/29.70 % Refutation found
% 230.81/29.70 % SZS status Theorem for theBenchmark: Theorem is valid
% 230.81/29.70 % SZS output start CNFRefutation for theBenchmark
% 230.81/29.70 fof(f1,axiom,(
% 230.81/29.70 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 230.81/29.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 230.81/29.70 fof(f2,axiom,(
% 230.81/29.70 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 230.81/29.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 230.81/29.70 fof(f3,axiom,(
% 230.81/29.70 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 230.81/29.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 230.81/29.70 fof(f4,axiom,(
% 230.81/29.70 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 230.81/29.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 230.81/29.70 fof(f5,axiom,(
% 230.81/29.70 (! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2) )),
% 230.81/29.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 230.81/29.70 fof(f6,axiom,(
% 230.81/29.70 (! [X0] : composition(X0,one) = X0 )),
% 230.81/29.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 230.81/29.70 fof(f7,axiom,(
% 230.81/29.70 (! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) )),
% 230.81/29.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 230.81/29.70 fof(f8,axiom,(
% 230.81/29.70 (! [X0] : converse(converse(X0)) = X0 )),
% 230.81/29.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 230.81/29.70 fof(f9,axiom,(
% 230.81/29.70 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 230.81/29.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 230.81/29.70 fof(f10,axiom,(
% 230.81/29.70 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 230.81/29.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 230.81/29.70 fof(f11,axiom,(
% 230.81/29.70 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 230.81/29.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 230.81/29.70 fof(f12,axiom,(
% 230.81/29.70 (! [X0] : top = join(X0,complement(X0)) )),
% 230.81/29.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 230.81/29.70 fof(f13,axiom,(
% 230.81/29.70 (! [X0] : zero = meet(X0,complement(X0)) )),
% 230.81/29.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 230.81/29.70 fof(f14,conjecture,(
% 230.81/29.70 (! [X0,X1] :( ( composition(X0,top) = X0& composition(X1,top) = X1 )=> composition(meet(X0,X1),top) = meet(X0,X1) ) )),
% 230.81/29.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 230.81/29.70 fof(f15,negated_conjecture,(
% 230.81/29.70 ~((! [X0,X1] :( ( composition(X0,top) = X0& composition(X1,top) = X1 )=> composition(meet(X0,X1),top) = meet(X0,X1) ) ))),
% 230.81/29.70 inference(negated_conjecture,[status(cth)],[f14])).
% 230.81/29.70 fof(f16,plain,(
% 230.81/29.70 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 230.81/29.70 inference(cnf_transformation,[status(thm)],[f1])).
% 230.81/29.70 fof(f17,plain,(
% 230.81/29.70 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 230.81/29.70 inference(cnf_transformation,[status(thm)],[f2])).
% 230.81/29.70 fof(f18,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 230.81/29.70 inference(cnf_transformation,[status(thm)],[f3])).
% 230.81/29.70 fof(f19,plain,(
% 230.81/29.70 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 230.81/29.70 inference(cnf_transformation,[status(thm)],[f4])).
% 230.81/29.70 fof(f20,plain,(
% 230.81/29.70 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 230.81/29.70 inference(cnf_transformation,[status(thm)],[f5])).
% 230.81/29.70 fof(f21,plain,(
% 230.81/29.70 ![X0]: (composition(X0,one)=X0)),
% 230.81/29.70 inference(cnf_transformation,[status(thm)],[f6])).
% 230.81/29.70 fof(f22,plain,(
% 230.81/29.70 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 230.81/29.70 inference(cnf_transformation,[status(thm)],[f7])).
% 230.81/29.70 fof(f23,plain,(
% 230.81/29.70 ![X0]: (converse(converse(X0))=X0)),
% 230.81/29.70 inference(cnf_transformation,[status(thm)],[f8])).
% 230.81/29.70 fof(f24,plain,(
% 230.81/29.70 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 230.81/29.70 inference(cnf_transformation,[status(thm)],[f9])).
% 230.81/29.70 fof(f25,plain,(
% 230.81/29.70 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 230.81/29.70 inference(cnf_transformation,[status(thm)],[f10])).
% 230.81/29.70 fof(f26,plain,(
% 230.81/29.70 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 230.81/29.70 inference(cnf_transformation,[status(thm)],[f11])).
% 230.81/29.70 fof(f27,plain,(
% 230.81/29.70 ![X0]: (top=join(X0,complement(X0)))),
% 230.81/29.70 inference(cnf_transformation,[status(thm)],[f12])).
% 230.81/29.70 fof(f28,plain,(
% 230.81/29.70 ![X0]: (zero=meet(X0,complement(X0)))),
% 230.81/29.70 inference(cnf_transformation,[status(thm)],[f13])).
% 230.81/29.70 fof(f29,plain,(
% 230.81/29.70 (?[X0,X1]: ((composition(X0,top)=X0&composition(X1,top)=X1)&~composition(meet(X0,X1),top)=meet(X0,X1)))),
% 230.81/29.70 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 230.81/29.70 fof(f30,plain,(
% 230.81/29.70 ((composition(sK0_skl,top)=sK0_skl&composition(sK1_skl,top)=sK1_skl)&~composition(meet(sK0_skl,sK1_skl),top)=meet(sK0_skl,sK1_skl))),
% 230.81/29.70 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl)],[f29])).
% 230.81/29.70 fof(f31,plain,(
% 230.81/29.70 composition(sK0_skl,top)=sK0_skl),
% 230.81/29.70 inference(cnf_transformation,[status(thm)],[f30])).
% 230.81/29.70 fof(f32,plain,(
% 230.81/29.70 composition(sK1_skl,top)=sK1_skl),
% 230.81/29.70 inference(cnf_transformation,[status(thm)],[f30])).
% 230.81/29.70 fof(f33,plain,(
% 230.81/29.70 ~composition(meet(sK0_skl,sK1_skl),top)=meet(sK0_skl,sK1_skl)),
% 230.81/29.70 inference(cnf_transformation,[status(thm)],[f30])).
% 230.81/29.70 fof(f34,definition,(
% 230.81/29.70 sF1_fnc=meet(sK0_skl,sK1_skl)),
% 230.81/29.70 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 230.81/29.70 fof(f35,definition,(
% 230.81/29.70 sF0_fnc=composition(sF1_fnc,top)),
% 230.81/29.70 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 230.81/29.70 fof(f36,plain,(
% 230.81/29.70 ~sF0_fnc=sF1_fnc),
% 230.81/29.70 inference(definition_folding,[],[f33,f35,f34])).
% 230.81/29.70 fof(f37,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f16,f18])).
% 230.81/29.70 fof(f38,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f19,f37])).
% 230.81/29.70 fof(f39,plain,(
% 230.81/29.70 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f16,f26])).
% 230.81/29.70 fof(f40,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f16,f38])).
% 230.81/29.70 fof(f41,plain,(
% 230.81/29.70 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f27,f19])).
% 230.81/29.70 fof(f42,plain,(
% 230.81/29.70 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X0,X1),complement(X2))))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f19,f19])).
% 230.81/29.70 fof(f43,plain,(
% 230.81/29.70 ![X0,X1,X2]: (meet(X0,join(complement(X1),complement(X2)))=complement(join(complement(X0),meet(X1,X2))))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f19,f19])).
% 230.81/29.70 fof(f44,plain,(
% 230.81/29.70 ![X0,X1]: (top=join(join(complement(X0),complement(X1)),meet(X0,X1)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f19,f27])).
% 230.81/29.70 fof(f45,plain,(
% 230.81/29.70 zero=complement(top)),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f28,f41])).
% 230.81/29.70 fof(f46,plain,(
% 230.81/29.70 ![X0,X1]: (top=join(complement(X0),join(complement(X1),meet(X0,X1))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f17,f44])).
% 230.81/29.70 fof(f47,plain,(
% 230.81/29.70 ![X0]: (meet(X0,top)=complement(join(complement(X0),zero)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f45,f19])).
% 230.81/29.70 fof(f48,plain,(
% 230.81/29.70 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f45,f19])).
% 230.81/29.70 fof(f49,plain,(
% 230.81/29.70 top=join(top,zero)),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f45,f27])).
% 230.81/29.70 fof(f50,plain,(
% 230.81/29.70 ![X0]: (meet(X0,top)=complement(join(zero,complement(X0))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f16,f47])).
% 230.81/29.70 fof(f51,plain,(
% 230.81/29.70 top=join(zero,top)),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f16,f49])).
% 230.81/29.70 fof(f53,plain,(
% 230.81/29.70 ![X0]: (composition(sF1_fnc,composition(top,X0))=composition(sF0_fnc,X0))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f35,f20])).
% 230.81/29.70 fof(f90,plain,(
% 230.81/29.70 ![X0]: (meet(top,X0)=meet(X0,top))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f50,f48])).
% 230.81/29.70 fof(f116,plain,(
% 230.81/29.70 sK0_skl=join(sF1_fnc,complement(join(complement(sK0_skl),sK1_skl)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f34,f40])).
% 230.81/29.70 fof(f117,plain,(
% 230.81/29.70 ![X0]: (X0=join(meet(top,X0),complement(join(complement(X0),top))))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f90,f40])).
% 230.81/29.70 fof(f118,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f19,f40])).
% 230.81/29.70 fof(f119,plain,(
% 230.81/29.70 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f27,f40])).
% 230.81/29.70 fof(f124,plain,(
% 230.81/29.70 ![X0,X1,X2]: (join(complement(X0),complement(X1))=join(meet(join(complement(X0),complement(X1)),X2),complement(join(meet(X0,X1),X2))))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f19,f40])).
% 230.81/29.70 fof(f127,plain,(
% 230.81/29.70 sK0_skl=join(sF1_fnc,complement(join(sK1_skl,complement(sK0_skl))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f16,f116])).
% 230.81/29.70 fof(f128,plain,(
% 230.81/29.70 ![X0]: (X0=join(meet(top,X0),complement(join(top,complement(X0)))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f16,f117])).
% 230.81/29.70 fof(f129,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f16,f118])).
% 230.81/29.70 fof(f130,plain,(
% 230.81/29.70 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(X0)))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f16,f119])).
% 230.81/29.70 fof(f131,plain,(
% 230.81/29.70 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f45,f130])).
% 230.81/29.70 fof(f132,plain,(
% 230.81/29.70 ![X0,X1,X2]: (join(complement(X0),complement(X1))=join(complement(join(meet(X0,X1),X2)),meet(join(complement(X0),complement(X1)),X2)))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f16,f124])).
% 230.81/29.70 fof(f137,plain,(
% 230.81/29.70 ![X0]: (composition(join(sK1_skl,X0),top)=join(sK1_skl,composition(X0,top)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f32,f22])).
% 230.81/29.70 fof(f139,plain,(
% 230.81/29.70 ![X0]: (composition(join(sK0_skl,X0),top)=join(sK0_skl,composition(X0,top)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f31,f22])).
% 230.81/29.70 fof(f142,plain,(
% 230.81/29.70 ![X0]: (composition(join(X0,sF1_fnc),top)=join(composition(X0,top),sF0_fnc))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f35,f22])).
% 230.81/29.70 fof(f154,plain,(
% 230.81/29.70 ![X0]: (composition(join(X0,sF1_fnc),top)=join(sF0_fnc,composition(X0,top)))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f16,f142])).
% 230.81/29.70 fof(f181,plain,(
% 230.81/29.70 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),join(zero,complement(X2)))=complement(join(meet(X0,X1),meet(X2,top))))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f50,f42])).
% 230.81/29.70 fof(f213,plain,(
% 230.81/29.70 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f21,f20])).
% 230.81/29.70 fof(f239,plain,(
% 230.81/29.70 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f16,f19])).
% 230.81/29.70 fof(f266,plain,(
% 230.81/29.70 top=join(zero,meet(top,complement(zero)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f45,f131])).
% 230.81/29.70 fof(f272,plain,(
% 230.81/29.70 ![X0,X1]: (converse(composition(X0,converse(X1)))=composition(X1,converse(X0)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f23,f25])).
% 230.81/29.70 fof(f273,plain,(
% 230.81/29.70 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f23,f25])).
% 230.81/29.70 fof(f277,plain,(
% 230.81/29.70 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f16,f24])).
% 230.81/29.70 fof(f279,plain,(
% 230.81/29.70 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f23,f24])).
% 230.81/29.70 fof(f350,plain,(
% 230.81/29.70 ![X0,X1]: (converse(join(X0,X1))=converse(join(X1,X0)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f24,f277])).
% 230.81/29.70 fof(f356,plain,(
% 230.81/29.70 ![X0,X1]: (converse(join(converse(X0),X1))=join(converse(X1),X0))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f23,f277])).
% 230.81/29.70 fof(f363,plain,(
% 230.81/29.70 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f21,f273])).
% 230.81/29.70 fof(f379,plain,(
% 230.81/29.70 ![X0]: (X0=composition(converse(one),X0))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f23,f363])).
% 230.81/29.70 fof(f389,plain,(
% 230.81/29.70 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f213,f379])).
% 230.81/29.70 fof(f390,plain,(
% 230.81/29.70 one=converse(one)),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f21,f379])).
% 230.81/29.70 fof(f397,plain,(
% 230.81/29.70 ![X0,X1]: (composition(join(converse(one),X0),X1)=join(X1,composition(X0,X1)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f379,f22])).
% 230.81/29.70 fof(f401,plain,(
% 230.81/29.70 ![X0]: (composition(one,X0)=X0)),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f379,f389])).
% 230.81/29.70 fof(f409,plain,(
% 230.81/29.70 ![X0,X1]: (composition(join(one,X0),X1)=join(X1,composition(X0,X1)))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f390,f397])).
% 230.81/29.70 fof(f411,plain,(
% 230.81/29.70 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f16,f17])).
% 230.81/29.70 fof(f421,plain,(
% 230.81/29.70 ![X0,X1,X2]: (join(meet(X0,X1),join(complement(join(complement(X0),X1)),X2))=join(X0,X2))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f40,f17])).
% 230.81/29.70 fof(f425,plain,(
% 230.81/29.70 ![X0]: (join(zero,join(top,X0))=join(top,X0))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f51,f17])).
% 230.81/29.70 fof(f426,plain,(
% 230.81/29.70 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f27,f17])).
% 230.81/29.70 fof(f427,plain,(
% 230.81/29.70 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X0),X2))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f16,f17])).
% 230.81/29.70 fof(f542,plain,(
% 230.81/29.70 ![X0]: (join(complement(X0),composition(converse(one),complement(X0)))=complement(X0))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f401,f39])).
% 230.81/29.70 fof(f552,plain,(
% 230.81/29.70 ![X0]: (composition(join(one,converse(one)),complement(X0))=complement(X0))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f409,f542])).
% 230.81/29.70 fof(f553,plain,(
% 230.81/29.70 ![X0]: (composition(join(one,one),complement(X0))=complement(X0))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f390,f552])).
% 230.81/29.70 fof(f556,plain,(
% 230.81/29.70 ![X0]: (join(zero,join(X0,top))=join(top,X0))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f16,f425])).
% 230.81/29.70 fof(f614,plain,(
% 230.81/29.70 ![X0]: (join(X0,top)=join(top,complement(complement(X0))))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f27,f426])).
% 230.81/29.70 fof(f615,plain,(
% 230.81/29.70 ![X0,X1]: (join(X0,join(X1,complement(X0)))=join(top,X1))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f16,f426])).
% 230.81/29.70 fof(f627,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(meet(X0,join(complement(complement(X0)),X1)),complement(join(top,X1))))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f426,f40])).
% 230.81/29.70 fof(f640,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(complement(join(top,X1)),meet(X0,join(complement(complement(X0)),X1))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f16,f627])).
% 230.81/29.70 fof(f671,plain,(
% 230.81/29.70 ![X0]: (join(zero,join(X0,top))=join(top,complement(complement(X0))))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f614,f425])).
% 230.81/29.70 fof(f688,plain,(
% 230.81/29.70 ![X0]: (join(top,X0)=join(top,complement(complement(X0))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f556,f671])).
% 230.81/29.70 fof(f721,plain,(
% 230.81/29.70 ![X0,X1]: (join(join(complement(X0),X1),X0)=join(top,meet(X0,X1)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f40,f615])).
% 230.81/29.70 fof(f737,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(meet(X0,join(X1,complement(complement(X0)))),complement(join(top,X1))))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f615,f40])).
% 230.81/29.70 fof(f746,plain,(
% 230.81/29.70 ![X0,X1]: (join(complement(X0),join(X1,X0))=join(top,meet(X0,X1)))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f17,f721])).
% 230.81/29.70 fof(f747,plain,(
% 230.81/29.70 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,meet(X0,X1)))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f411,f746])).
% 230.81/29.70 fof(f748,plain,(
% 230.81/29.70 ![X0,X1]: (join(top,X0)=join(top,meet(X1,X0)))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f426,f747])).
% 230.81/29.70 fof(f771,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(complement(join(top,X1)),meet(X0,join(X1,complement(complement(X0))))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f16,f737])).
% 230.81/29.70 fof(f805,plain,(
% 230.81/29.70 ![X0]: (top=join(top,meet(X0,complement(X0))))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f426,f46])).
% 230.81/29.70 fof(f824,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(meet(X0,join(complement(X1),meet(X0,X1))),complement(top)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f46,f40])).
% 230.81/29.70 fof(f827,plain,(
% 230.81/29.70 ![X0]: (join(top,X0)=top)),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f836,f688])).
% 230.81/29.70 fof(f828,plain,(
% 230.81/29.70 ![X0]: (join(X0,top)=top)),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f836,f614])).
% 230.81/29.70 fof(f835,plain,(
% 230.81/29.70 ![X0]: (X0=join(meet(top,X0),complement(top)))),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f836,f128])).
% 230.81/29.70 fof(f836,plain,(
% 230.81/29.70 ![X0]: (top=join(top,complement(X0)))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f748,f805])).
% 230.81/29.70 fof(f848,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(complement(top),meet(X0,join(complement(X1),meet(X0,X1)))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f16,f824])).
% 230.81/29.70 fof(f849,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(zero,meet(X0,join(complement(X1),meet(X0,X1)))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f45,f848])).
% 230.81/29.70 fof(f852,plain,(
% 230.81/29.70 ![X0,X1]: (join(X0,join(X1,complement(X0)))=top)),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f827,f615])).
% 230.81/29.70 fof(f872,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(complement(top),meet(X0,join(X1,complement(complement(X0))))))),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f827,f771])).
% 230.81/29.70 fof(f879,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(complement(top),meet(X0,join(complement(complement(X0)),X1))))),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f827,f640])).
% 230.81/29.70 fof(f888,plain,(
% 230.81/29.70 ![X0]: (X0=join(complement(top),meet(top,X0)))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f16,f835])).
% 230.81/29.70 fof(f889,plain,(
% 230.81/29.70 top=complement(zero)),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f891,f266])).
% 230.81/29.70 fof(f891,plain,(
% 230.81/29.70 ![X0]: (X0=join(zero,meet(top,X0)))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f45,f888])).
% 230.81/29.70 fof(f901,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(zero,meet(X0,join(X1,complement(complement(X0))))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f45,f872])).
% 230.81/29.70 fof(f902,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(zero,meet(X0,join(complement(complement(X0)),X1))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f45,f879])).
% 230.81/29.70 fof(f940,plain,(
% 230.81/29.70 ![X0,X1,X2]: (meet(join(meet(X0,X1),X2),join(complement(join(complement(X0),complement(X1))),complement(X2)))=complement(join(complement(X0),complement(X1))))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f132,f43])).
% 230.81/29.70 fof(f1005,plain,(
% 230.81/29.70 ![X0,X1,X2]: (meet(join(meet(X0,X1),X2),join(meet(X0,X1),complement(X2)))=complement(join(complement(X0),complement(X1))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f19,f940])).
% 230.81/29.70 fof(f1006,plain,(
% 230.81/29.70 ![X0,X1,X2]: (meet(join(meet(X0,X1),X2),join(meet(X0,X1),complement(X2)))=meet(X0,X1))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f19,f1005])).
% 230.81/29.70 fof(f1010,plain,(
% 230.81/29.70 ![X0]: (join(complement(X0),composition(one,complement(composition(one,X0))))=complement(X0))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f390,f39])).
% 230.81/29.70 fof(f1013,plain,(
% 230.81/29.70 ![X0]: (converse(join(X0,one))=join(one,converse(X0)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f390,f277])).
% 230.81/29.70 fof(f1020,plain,(
% 230.81/29.70 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f401,f1010])).
% 230.81/29.70 fof(f1021,plain,(
% 230.81/29.70 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f401,f1020])).
% 230.81/29.70 fof(f1034,plain,(
% 230.81/29.70 composition(join(one,one),top)=complement(zero)),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f889,f553])).
% 230.81/29.70 fof(f1045,plain,(
% 230.81/29.70 ![X0]: (meet(zero,X0)=complement(join(top,complement(X0))))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f889,f19])).
% 230.81/29.70 fof(f1058,plain,(
% 230.81/29.70 composition(join(one,one),top)=top),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f889,f1034])).
% 230.81/29.70 fof(f1086,plain,(
% 230.81/29.70 ![X0]: (meet(zero,X0)=complement(top))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f827,f1045])).
% 230.81/29.70 fof(f1091,plain,(
% 230.81/29.70 ![X0]: (meet(zero,X0)=zero)),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f45,f1086])).
% 230.81/29.70 fof(f1271,plain,(
% 230.81/29.70 ![X0]: (composition(join(X0,join(one,one)),top)=join(composition(X0,top),top))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f1058,f22])).
% 230.81/29.70 fof(f1283,plain,(
% 230.81/29.70 ![X0]: (composition(join(X0,join(one,one)),top)=top)),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f828,f1271])).
% 230.81/29.70 fof(f1290,plain,(
% 230.81/29.70 ![X0]: (join(meet(X0,top),complement(join(zero,complement(X0))))=complement(join(zero,complement(X0))))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f50,f1021])).
% 230.81/29.70 fof(f1301,plain,(
% 230.81/29.70 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f1021,f19])).
% 230.81/29.70 fof(f1302,plain,(
% 230.81/29.70 ![X0]: (X0=join(meet(X0,complement(X0)),complement(complement(X0))))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f1021,f40])).
% 230.81/29.70 fof(f1311,plain,(
% 230.81/29.70 ![X0]: (join(meet(X0,top),meet(top,X0))=complement(join(zero,complement(X0))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f48,f1290])).
% 230.81/29.70 fof(f1312,plain,(
% 230.81/29.70 ![X0]: (join(meet(X0,top),meet(top,X0))=meet(top,X0))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f48,f1311])).
% 230.81/29.70 fof(f1341,plain,(
% 230.81/29.70 ![X0]: (X0=join(complement(complement(X0)),meet(X0,complement(X0))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f16,f1302])).
% 230.81/29.70 fof(f1342,plain,(
% 230.81/29.70 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f28,f1341])).
% 230.81/29.70 fof(f1343,plain,(
% 230.81/29.70 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f16,f1342])).
% 230.81/29.70 fof(f1350,plain,(
% 230.81/29.70 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(meet(X0,X1))))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f19,f1343])).
% 230.81/29.70 fof(f1351,plain,(
% 230.81/29.70 ![X0]: (meet(top,complement(X0))=complement(X0))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f1343,f48])).
% 230.81/29.70 fof(f1372,plain,(
% 230.81/29.70 ![X0]: (complement(X0)=join(zero,complement(X0)))),
% 230.81/29.70 inference(paramodulation,[status(thm)],[f1351,f891])).
% 230.81/29.70 fof(f1396,plain,(
% 230.81/29.70 ![X0]: (X0=complement(complement(X0)))),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f1372,f1343])).
% 230.81/29.70 fof(f1397,plain,(
% 230.81/29.70 ![X0]: (meet(top,X0)=complement(complement(X0)))),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f1372,f48])).
% 230.81/29.70 fof(f1398,plain,(
% 230.81/29.70 ![X0]: (meet(X0,top)=complement(complement(X0)))),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f1372,f50])).
% 230.81/29.70 fof(f1399,plain,(
% 230.81/29.70 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f1372,f1350])).
% 230.81/29.70 fof(f1420,plain,(
% 230.81/29.70 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),complement(X2))=complement(join(meet(X0,X1),meet(X2,top))))),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f1372,f181])).
% 230.81/29.70 fof(f1440,plain,(
% 230.81/29.70 ![X0]: (meet(X0,X0)=X0)),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f1396,f1301])).
% 230.81/29.70 fof(f1442,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(zero,meet(X0,join(X0,X1))))),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f1396,f902])).
% 230.81/29.70 fof(f1443,plain,(
% 230.81/29.70 ![X0,X1]: (X0=join(zero,meet(X0,join(X1,X0))))),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f1396,f901])).
% 230.81/29.70 fof(f1448,plain,(
% 230.81/29.70 ![X0]: (X0=join(zero,X0))),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f1461,f891])).
% 230.81/29.70 fof(f1455,plain,(
% 230.81/29.70 ![X0]: (join(meet(X0,top),meet(top,X0))=X0)),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f1461,f1312])).
% 230.81/29.70 fof(f1461,plain,(
% 230.81/29.70 ![X0]: (meet(top,X0)=X0)),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f1396,f1397])).
% 230.81/29.70 fof(f1468,plain,(
% 230.81/29.70 ![X0]: (meet(X0,top)=X0)),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f1396,f1398])).
% 230.81/29.70 fof(f1512,plain,(
% 230.81/29.70 ![X0,X1]: (meet(X0,X1)=complement(complement(meet(X1,X0))))),
% 230.81/29.70 inference(backward_demodulation,[status(thm)],[f1399,f239])).
% 230.81/29.70 fof(f1566,plain,(
% 230.81/29.70 ![X0,X1,X2]: (meet(complement(meet(X0,X1)),complement(X2))=complement(join(meet(X0,X1),meet(X2,top))))),
% 230.81/29.70 inference(forward_demodulation,[status(thm)],[f1399,f1420])).
% 230.81/29.70 fof(f1567,plain,(
% 230.81/29.71 ![X0,X1,X2]: (meet(complement(meet(X0,X1)),complement(X2))=complement(join(meet(X0,X1),X2)))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1468,f1566])).
% 230.81/29.71 fof(f1591,plain,(
% 230.81/29.71 ![X0,X1]: (X0=meet(X0,join(complement(X1),meet(X0,X1))))),
% 230.81/29.71 inference(backward_demodulation,[status(thm)],[f1448,f849])).
% 230.81/29.71 fof(f1592,plain,(
% 230.81/29.71 ![X0,X1]: (X0=meet(X0,join(X1,X0)))),
% 230.81/29.71 inference(backward_demodulation,[status(thm)],[f1448,f1443])).
% 230.81/29.71 fof(f1593,plain,(
% 230.81/29.71 ![X0,X1]: (X0=meet(X0,join(X0,X1)))),
% 230.81/29.71 inference(backward_demodulation,[status(thm)],[f1448,f1442])).
% 230.81/29.71 fof(f1602,plain,(
% 230.81/29.71 ![X0]: (join(X0,meet(top,X0))=X0)),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1468,f1455])).
% 230.81/29.71 fof(f1608,plain,(
% 230.81/29.71 ![X0]: (composition(join(X0,one),top)=top)),
% 230.81/29.71 inference(backward_demodulation,[status(thm)],[f1618,f1283])).
% 230.81/29.71 fof(f1618,plain,(
% 230.81/29.71 ![X0]: (join(X0,X0)=X0)),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1461,f1602])).
% 230.81/29.71 fof(f1671,plain,(
% 230.81/29.71 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1396,f1512])).
% 230.81/29.71 fof(f1691,plain,(
% 230.81/29.71 ![X0]: (X0=join(X0,meet(X0,complement(X0))))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1440,f129])).
% 230.81/29.71 fof(f1699,plain,(
% 230.81/29.71 ![X0]: (X0=join(X0,zero))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f28,f1691])).
% 230.81/29.71 fof(f2001,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,join(X0,X1))=join(X0,X1))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1618,f17])).
% 230.81/29.71 fof(f2141,plain,(
% 230.81/29.71 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X0))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f129,f1593])).
% 230.81/29.71 fof(f2160,plain,(
% 230.81/29.71 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X0,X1)))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1671,f2141])).
% 230.81/29.71 fof(f2174,plain,(
% 230.81/29.71 composition(top,top)=top),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f827,f1608])).
% 230.81/29.71 fof(f2214,plain,(
% 230.81/29.71 composition(sF1_fnc,top)=composition(sF0_fnc,top)),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f2174,f53])).
% 230.81/29.71 fof(f2226,plain,(
% 230.81/29.71 ![X0]: (composition(top,composition(top,X0))=composition(top,X0))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f2174,f20])).
% 230.81/29.71 fof(f2227,plain,(
% 230.81/29.71 sF0_fnc=composition(sF0_fnc,top)),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f35,f2214])).
% 230.81/29.71 fof(f2254,plain,(
% 230.81/29.71 composition(join(sK0_skl,sF0_fnc),top)=join(sK0_skl,sF0_fnc)),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f2227,f139])).
% 230.81/29.71 fof(f2255,plain,(
% 230.81/29.71 composition(join(sK1_skl,sF0_fnc),top)=join(sK1_skl,sF0_fnc)),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f2227,f137])).
% 230.81/29.71 fof(f2262,plain,(
% 230.81/29.71 ![X0]: (composition(join(X0,sF0_fnc),top)=join(composition(X0,top),sF0_fnc))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f2227,f22])).
% 230.81/29.71 fof(f2276,plain,(
% 230.81/29.71 ![X0]: (composition(join(X0,sF1_fnc),top)=composition(join(X0,sF0_fnc),top))),
% 230.81/29.71 inference(backward_demodulation,[status(thm)],[f2277,f154])).
% 230.81/29.71 fof(f2277,plain,(
% 230.81/29.71 ![X0]: (composition(join(X0,sF0_fnc),top)=join(sF0_fnc,composition(X0,top)))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f16,f2262])).
% 230.81/29.71 fof(f2377,plain,(
% 230.81/29.71 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1671,f129])).
% 230.81/29.71 fof(f2379,plain,(
% 230.81/29.71 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1671,f129])).
% 230.81/29.71 fof(f2450,plain,(
% 230.81/29.71 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X1,X0)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1671,f2160])).
% 230.81/29.71 fof(f2511,plain,(
% 230.81/29.71 meet(sK1_skl,sK0_skl)=meet(sK1_skl,sF1_fnc)),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f34,f2450])).
% 230.81/29.71 fof(f2533,plain,(
% 230.81/29.71 meet(sK0_skl,sK1_skl)=meet(sK1_skl,sF1_fnc)),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1671,f2511])).
% 230.81/29.71 fof(f2534,plain,(
% 230.81/29.71 sF1_fnc=meet(sK1_skl,sF1_fnc)),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f34,f2533])).
% 230.81/29.71 fof(f2671,plain,(
% 230.81/29.71 join(sF1_fnc,sK0_skl)=join(sF1_fnc,complement(join(sK1_skl,complement(sK0_skl))))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f127,f2001])).
% 230.81/29.71 fof(f2681,plain,(
% 230.81/29.71 ![X0,X1]: (join(meet(X0,X1),X0)=join(meet(X0,X1),meet(X0,complement(X1))))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f129,f2001])).
% 230.81/29.71 fof(f2690,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,join(X1,X0))=join(X0,X1))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f16,f2001])).
% 230.81/29.71 fof(f2720,plain,(
% 230.81/29.71 join(sK0_skl,sF1_fnc)=join(sF1_fnc,complement(join(sK1_skl,complement(sK0_skl))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f16,f2671])).
% 230.81/29.71 fof(f2721,plain,(
% 230.81/29.71 join(sK0_skl,sF1_fnc)=sK0_skl),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f127,f2720])).
% 230.81/29.71 fof(f2740,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,meet(X0,X1))=join(meet(X0,X1),meet(X0,complement(X1))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f16,f2681])).
% 230.81/29.71 fof(f2744,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f129,f2740])).
% 230.81/29.71 fof(f2771,plain,(
% 230.81/29.71 join(sK1_skl,sF1_fnc)=sK1_skl),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f2534,f2744])).
% 230.81/29.71 fof(f2783,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1671,f2744])).
% 230.81/29.71 fof(f2818,plain,(
% 230.81/29.71 ![X0,X1]: (join(meet(X0,X1),meet(X1,X0))=meet(X0,X1))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f2450,f2783])).
% 230.81/29.71 fof(f2837,plain,(
% 230.81/29.71 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X1))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f2783,f1592])).
% 230.81/29.71 fof(f2844,plain,(
% 230.81/29.71 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X0,X1)))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1671,f2837])).
% 230.81/29.71 fof(f2862,plain,(
% 230.81/29.71 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X1,X0)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1671,f2844])).
% 230.81/29.71 fof(f3004,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,X1)=meet(join(X0,X1),join(X1,X0)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f2690,f1592])).
% 230.81/29.71 fof(f3545,plain,(
% 230.81/29.71 composition(sK0_skl,top)=composition(join(sK0_skl,sF0_fnc),top)),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f2721,f2276])).
% 230.81/29.71 fof(f3547,plain,(
% 230.81/29.71 composition(sK1_skl,top)=composition(join(sK1_skl,sF0_fnc),top)),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f2771,f2276])).
% 230.81/29.71 fof(f3569,plain,(
% 230.81/29.71 sK0_skl=join(sK0_skl,sF0_fnc)),
% 230.81/29.71 inference(backward_demodulation,[status(thm)],[f3570,f2254])).
% 230.81/29.71 fof(f3570,plain,(
% 230.81/29.71 sK0_skl=composition(join(sK0_skl,sF0_fnc),top)),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f31,f3545])).
% 230.81/29.71 fof(f3573,plain,(
% 230.81/29.71 sK1_skl=join(sK1_skl,sF0_fnc)),
% 230.81/29.71 inference(backward_demodulation,[status(thm)],[f3574,f2255])).
% 230.81/29.71 fof(f3574,plain,(
% 230.81/29.71 sK1_skl=composition(join(sK1_skl,sF0_fnc),top)),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f32,f3547])).
% 230.81/29.71 fof(f4439,plain,(
% 230.81/29.71 sK1_skl=join(sF1_fnc,meet(sK1_skl,complement(sK0_skl)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f34,f2379])).
% 230.81/29.71 fof(f4595,plain,(
% 230.81/29.71 ![X0,X1]: (converse(converse(X0))=join(X0,converse(meet(X1,converse(X0)))))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f2783,f279])).
% 230.81/29.71 fof(f4602,plain,(
% 230.81/29.71 ![X0]: (converse(converse(X0))=join(X0,converse(zero)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1699,f279])).
% 230.81/29.71 fof(f4603,plain,(
% 230.81/29.71 ![X0]: (converse(top)=join(X0,converse(top)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f828,f279])).
% 230.81/29.71 fof(f4606,plain,(
% 230.81/29.71 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f27,f279])).
% 230.81/29.71 fof(f4631,plain,(
% 230.81/29.71 ![X0,X1]: (X0=join(X0,converse(meet(X1,converse(X0)))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f23,f4595])).
% 230.81/29.71 fof(f4640,plain,(
% 230.81/29.71 ![X0]: (X0=join(X0,converse(zero)))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f23,f4602])).
% 230.81/29.71 fof(f4762,plain,(
% 230.81/29.71 zero=converse(zero)),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1448,f4640])).
% 230.81/29.71 fof(f5010,plain,(
% 230.81/29.71 converse(top)=top),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f827,f4603])).
% 230.81/29.71 fof(f5039,plain,(
% 230.81/29.71 ![X0]: (top=join(X0,converse(complement(converse(X0)))))),
% 230.81/29.71 inference(backward_demodulation,[status(thm)],[f5010,f4606])).
% 230.81/29.71 fof(f5089,plain,(
% 230.81/29.71 ![X0]: (join(complement(X0),composition(top,complement(composition(top,X0))))=complement(X0))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f5010,f39])).
% 230.81/29.71 fof(f5093,plain,(
% 230.81/29.71 ![X0]: (converse(composition(X0,top))=composition(top,converse(X0)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f5010,f272])).
% 230.81/29.71 fof(f5249,plain,(
% 230.81/29.71 ![X0]: (X0=join(meet(X0,converse(complement(converse(complement(X0))))),complement(top)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f5039,f40])).
% 230.81/29.71 fof(f5290,plain,(
% 230.81/29.71 ![X0]: (X0=join(complement(top),meet(X0,converse(complement(converse(complement(X0)))))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f16,f5249])).
% 230.81/29.71 fof(f5291,plain,(
% 230.81/29.71 ![X0]: (X0=join(zero,meet(X0,converse(complement(converse(complement(X0)))))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f45,f5290])).
% 230.81/29.71 fof(f5292,plain,(
% 230.81/29.71 ![X0]: (X0=meet(X0,converse(complement(converse(complement(X0))))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1448,f5291])).
% 230.81/29.71 fof(f5416,plain,(
% 230.81/29.71 ![X0,X1,X2]: (join(X0,X1)=join(meet(X1,X2),join(X0,X1)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f2744,f411])).
% 230.81/29.71 fof(f5495,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,join(X0,X1))=join(X1,X0))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1618,f411])).
% 230.81/29.71 fof(f5598,plain,(
% 230.81/29.71 ![X0,X1,X2]: (join(X0,X1)=join(X1,join(meet(X1,X2),X0)))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f411,f5416])).
% 230.81/29.71 fof(f6323,plain,(
% 230.81/29.71 ![X0,X1]: (X0=meet(X0,join(X1,meet(X0,complement(X1)))))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1396,f1591])).
% 230.81/29.71 fof(f7148,plain,(
% 230.81/29.71 ![X0,X1]: (top=join(X0,complement(meet(X0,X1))))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f852,f421])).
% 230.81/29.71 fof(f7426,plain,(
% 230.81/29.71 ![X0,X1]: (top=join(X0,complement(meet(X1,X0))))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f2862,f7148])).
% 230.81/29.71 fof(f8292,plain,(
% 230.81/29.71 ![X0]: (complement(converse(complement(X0)))=join(complement(converse(complement(X0))),converse(X0)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f5292,f4631])).
% 230.81/29.71 fof(f8326,plain,(
% 230.81/29.71 ![X0]: (complement(converse(complement(X0)))=join(converse(X0),complement(converse(complement(X0)))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f16,f8292])).
% 230.81/29.71 fof(f8381,plain,(
% 230.81/29.71 ![X0,X1]: (join(join(X0,meet(X1,complement(X0))),X1)=join(X0,meet(X1,complement(X0))))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f6323,f2783])).
% 230.81/29.71 fof(f8413,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,join(meet(X1,complement(X0)),X1))=join(X0,meet(X1,complement(X0))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f17,f8381])).
% 230.81/29.71 fof(f8414,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,join(X1,meet(X1,complement(X0))))=join(X0,meet(X1,complement(X0))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f16,f8413])).
% 230.81/29.71 fof(f8427,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,X1)=join(X0,meet(X1,complement(X0))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f2744,f8414])).
% 230.81/29.71 fof(f8545,plain,(
% 230.81/29.71 ![X0,X1,X2]: (join(meet(X0,X1),join(X1,X2))=join(X1,X2))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f2783,f427])).
% 230.81/29.71 fof(f8691,plain,(
% 230.81/29.71 ![X0,X1,X2]: (join(X0,join(X1,meet(X2,X0)))=join(X0,X1))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f411,f8545])).
% 230.81/29.71 fof(f9568,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,X1)=join(X0,meet(complement(X0),X1)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1671,f8427])).
% 230.81/29.71 fof(f9603,plain,(
% 230.81/29.71 ![X0,X1,X2]: (join(meet(X0,complement(X1)),join(X1,X2))=join(join(X1,X0),X2))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f8427,f427])).
% 230.81/29.71 fof(f9608,plain,(
% 230.81/29.71 ![X0,X1]: (join(meet(X0,complement(X1)),join(X1,X0))=join(meet(X0,complement(X1)),X1))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f8427,f2690])).
% 230.81/29.71 fof(f9658,plain,(
% 230.81/29.71 ![X0,X1,X2]: (join(X0,join(X1,meet(X2,complement(X0))))=join(join(X0,X2),X1))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f411,f9603])).
% 230.81/29.71 fof(f9660,plain,(
% 230.81/29.71 ![X0,X1,X2]: (join(X0,join(X1,meet(X2,complement(X0))))=join(X2,join(X0,X1)))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f427,f9658])).
% 230.81/29.71 fof(f9676,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,join(X1,meet(X1,complement(X0))))=join(meet(X1,complement(X0)),X0))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f411,f9608])).
% 230.81/29.71 fof(f9677,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,join(X1,X0))=join(meet(X0,complement(X1)),X1))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f9660,f9676])).
% 230.81/29.71 fof(f9678,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,X1)=join(meet(X0,complement(X1)),X1))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f2690,f9677])).
% 230.81/29.71 fof(f9679,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,X1)=join(X1,meet(X0,complement(X1))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f16,f9678])).
% 230.81/29.71 fof(f9727,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,X1)=join(X1,meet(complement(X1),X0)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1671,f9679])).
% 230.81/29.71 fof(f10266,plain,(
% 230.81/29.71 ![X0,X1]: (top=complement(meet(X0,meet(X1,complement(X0)))))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f7426,f1399])).
% 230.81/29.71 fof(f10272,plain,(
% 230.81/29.71 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X1,X0)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f16,f1399])).
% 230.81/29.71 fof(f10274,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,complement(X1))=complement(meet(complement(X0),X1)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1396,f1399])).
% 230.81/29.71 fof(f10386,plain,(
% 230.81/29.71 ![X0,X1]: (meet(X0,meet(X1,complement(X0)))=meet(meet(X0,meet(X1,complement(X0))),converse(complement(converse(top)))))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f10266,f5292])).
% 230.81/29.71 fof(f10422,plain,(
% 230.81/29.71 ![X0,X1]: (meet(X0,meet(X1,complement(X0)))=meet(converse(complement(converse(top))),meet(X0,meet(X1,complement(X0)))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1671,f10386])).
% 230.81/29.71 fof(f10423,plain,(
% 230.81/29.71 ![X0,X1]: (meet(X0,meet(X1,complement(X0)))=meet(converse(complement(top)),meet(X0,meet(X1,complement(X0)))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f5010,f10422])).
% 230.81/29.71 fof(f10424,plain,(
% 230.81/29.71 ![X0,X1]: (meet(X0,meet(X1,complement(X0)))=meet(converse(zero),meet(X0,meet(X1,complement(X0)))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f45,f10423])).
% 230.81/29.71 fof(f10425,plain,(
% 230.81/29.71 ![X0,X1]: (meet(X0,meet(X1,complement(X0)))=meet(zero,meet(X0,meet(X1,complement(X0)))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f4762,f10424])).
% 230.81/29.71 fof(f10430,plain,(
% 230.81/29.71 ![X0,X1]: (meet(X0,meet(X1,complement(X0)))=zero)),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1091,f10425])).
% 230.81/29.71 fof(f10486,plain,(
% 230.81/29.71 ![X0,X1]: (meet(complement(X0),meet(X1,X0))=zero)),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1396,f10430])).
% 230.81/29.71 fof(f19090,plain,(
% 230.81/29.71 ![X0]: (join(complement(composition(top,X0)),composition(converse(top),complement(composition(top,X0))))=complement(composition(top,X0)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f2226,f39])).
% 230.81/29.71 fof(f19158,plain,(
% 230.81/29.71 ![X0]: (composition(join(one,converse(top)),complement(composition(top,X0)))=complement(composition(top,X0)))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f409,f19090])).
% 230.81/29.71 fof(f19159,plain,(
% 230.81/29.71 ![X0]: (composition(converse(join(top,one)),complement(composition(top,X0)))=complement(composition(top,X0)))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1013,f19158])).
% 230.81/29.71 fof(f19160,plain,(
% 230.81/29.71 ![X0]: (composition(converse(join(one,top)),complement(composition(top,X0)))=complement(composition(top,X0)))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f350,f19159])).
% 230.81/29.71 fof(f19161,plain,(
% 230.81/29.71 ![X0]: (composition(converse(top),complement(composition(top,X0)))=complement(composition(top,X0)))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f828,f19160])).
% 230.81/29.71 fof(f19164,plain,(
% 230.81/29.71 ![X0]: (join(complement(X0),complement(composition(top,X0)))=complement(X0))),
% 230.81/29.71 inference(backward_demodulation,[status(thm)],[f19165,f5089])).
% 230.81/29.71 fof(f19165,plain,(
% 230.81/29.71 ![X0]: (composition(top,complement(composition(top,X0)))=complement(composition(top,X0)))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f5010,f19161])).
% 230.81/29.71 fof(f19177,plain,(
% 230.81/29.71 ![X0]: (complement(meet(X0,composition(top,X0)))=complement(X0))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1399,f19164])).
% 230.81/29.71 fof(f19213,plain,(
% 230.81/29.71 ![X0]: (meet(X0,composition(top,X0))=complement(complement(X0)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f19177,f1396])).
% 230.81/29.71 fof(f19250,plain,(
% 230.81/29.71 ![X0]: (meet(X0,composition(top,X0))=X0)),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1396,f19213])).
% 230.81/29.71 fof(f19307,plain,(
% 230.81/29.71 ![X0]: (meet(complement(composition(top,X0)),X0)=zero)),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f19250,f10486])).
% 230.81/29.71 fof(f19340,plain,(
% 230.81/29.71 ![X0]: (meet(X0,complement(composition(top,X0)))=zero)),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1671,f19307])).
% 230.81/29.71 fof(f19420,plain,(
% 230.81/29.71 ![X0]: (join(complement(composition(top,complement(X0))),X0)=join(X0,zero))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f19340,f9727])).
% 230.81/29.71 fof(f19467,plain,(
% 230.81/29.71 ![X0]: (join(X0,complement(composition(top,complement(X0))))=join(X0,zero))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f16,f19420])).
% 230.81/29.71 fof(f19468,plain,(
% 230.81/29.71 ![X0]: (join(X0,complement(composition(top,complement(X0))))=X0)),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1699,f19467])).
% 230.81/29.71 fof(f19642,plain,(
% 230.81/29.71 ![X0]: (converse(converse(X0))=join(converse(complement(composition(top,complement(converse(X0))))),X0))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f19468,f356])).
% 230.81/29.71 fof(f19691,plain,(
% 230.81/29.71 ![X0]: (X0=join(converse(complement(composition(top,complement(converse(X0))))),X0))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f23,f19642])).
% 230.81/29.71 fof(f19692,plain,(
% 230.81/29.71 ![X0]: (X0=join(X0,converse(complement(composition(top,complement(converse(X0)))))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f16,f19691])).
% 230.81/29.71 fof(f27726,plain,(
% 230.81/29.71 ![X0,X1]: (join(complement(X0),complement(X1))=meet(join(complement(X0),complement(X1)),complement(meet(X1,X0))))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1399,f3004])).
% 230.81/29.71 fof(f28359,plain,(
% 230.81/29.71 ![X0,X1]: (complement(meet(X0,X1))=meet(join(complement(X0),complement(X1)),complement(meet(X1,X0))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1399,f27726])).
% 230.81/29.71 fof(f28360,plain,(
% 230.81/29.71 ![X0,X1]: (complement(meet(X0,X1))=meet(complement(meet(X1,X0)),join(complement(X0),complement(X1))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1671,f28359])).
% 230.81/29.71 fof(f28361,plain,(
% 230.81/29.71 ![X0,X1]: (complement(meet(X0,X1))=meet(complement(meet(X1,X0)),complement(meet(X0,X1))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1399,f28360])).
% 230.81/29.71 fof(f28362,plain,(
% 230.81/29.71 ![X0,X1]: (complement(meet(X0,X1))=complement(join(meet(X1,X0),meet(X0,X1))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1567,f28361])).
% 230.81/29.71 fof(f28363,plain,(
% 230.81/29.71 ![X0,X1]: (complement(meet(X0,X1))=complement(meet(X1,X0)))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f2818,f28362])).
% 230.81/29.71 fof(f42405,plain,(
% 230.81/29.71 ![X0,X1]: (join(X0,complement(X1))=complement(meet(X1,complement(X0))))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1396,f10272])).
% 230.81/29.71 fof(f42548,plain,(
% 230.81/29.71 ![X0]: (join(X0,complement(converse(complement(converse(complement(complement(X0)))))))=complement(complement(X0)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f5292,f10274])).
% 230.81/29.71 fof(f42644,plain,(
% 230.81/29.71 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=complement(complement(X0)))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1396,f42548])).
% 230.81/29.71 fof(f42645,plain,(
% 230.81/29.71 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=X0)),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1396,f42644])).
% 230.81/29.71 fof(f42774,plain,(
% 230.81/29.71 ![X0]: (join(converse(X0),complement(converse(complement(X0))))=converse(X0))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f23,f42645])).
% 230.81/29.71 fof(f42889,plain,(
% 230.81/29.71 ![X0]: (complement(converse(complement(X0)))=converse(X0))),
% 230.81/29.71 inference(backward_demodulation,[status(thm)],[f42774,f8326])).
% 230.81/29.71 fof(f43124,plain,(
% 230.81/29.71 ![X0]: (complement(converse(X0))=converse(complement(X0)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f1396,f42889])).
% 230.81/29.71 fof(f43269,plain,(
% 230.81/29.71 ![X0]: (X0=join(X0,converse(complement(composition(top,converse(complement(X0)))))))),
% 230.81/29.71 inference(backward_demodulation,[status(thm)],[f43124,f19692])).
% 230.81/29.71 fof(f43573,plain,(
% 230.81/29.71 ![X0]: (X0=join(X0,converse(complement(converse(composition(complement(X0),top))))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f5093,f43269])).
% 230.81/29.71 fof(f43574,plain,(
% 230.81/29.71 ![X0]: (X0=join(X0,converse(converse(complement(composition(complement(X0),top))))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f43124,f43573])).
% 230.81/29.71 fof(f43575,plain,(
% 230.81/29.71 ![X0]: (X0=join(X0,complement(composition(complement(X0),top))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f23,f43574])).
% 230.81/29.71 fof(f46292,plain,(
% 230.81/29.71 ![X0]: (complement(X0)=complement(meet(composition(complement(complement(X0)),top),X0)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f10272,f43575])).
% 230.81/29.71 fof(f46403,plain,(
% 230.81/29.71 ![X0]: (complement(X0)=complement(meet(X0,composition(complement(complement(X0)),top))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f28363,f46292])).
% 230.81/29.71 fof(f46404,plain,(
% 230.81/29.71 ![X0]: (complement(X0)=complement(meet(X0,composition(X0,top))))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f1396,f46403])).
% 230.81/29.71 fof(f46518,plain,(
% 230.81/29.71 complement(sF1_fnc)=complement(meet(sF1_fnc,sF0_fnc))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f35,f46404])).
% 230.81/29.71 fof(f46585,plain,(
% 230.81/29.71 complement(sF1_fnc)=complement(meet(sF0_fnc,sF1_fnc))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f28363,f46518])).
% 230.81/29.71 fof(f46690,plain,(
% 230.81/29.71 ![X0]: (join(meet(sF0_fnc,sF1_fnc),complement(X0))=complement(meet(complement(sF1_fnc),X0)))),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f46585,f10274])).
% 230.81/29.71 fof(f46697,plain,(
% 230.81/29.71 join(meet(sF0_fnc,sF1_fnc),complement(composition(top,complement(sF1_fnc))))=meet(sF0_fnc,sF1_fnc)),
% 230.81/29.71 inference(paramodulation,[status(thm)],[f46585,f19468])).
% 230.81/29.71 fof(f46729,plain,(
% 230.81/29.71 ![X0]: (join(meet(sF0_fnc,sF1_fnc),complement(X0))=join(sF1_fnc,complement(X0)))),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f10274,f46690])).
% 230.81/29.71 fof(f46736,plain,(
% 230.81/29.71 join(sF1_fnc,complement(composition(top,complement(sF1_fnc))))=meet(sF0_fnc,sF1_fnc)),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f46729,f46697])).
% 230.81/29.71 fof(f46748,plain,(
% 230.81/29.71 sF1_fnc=meet(sF0_fnc,sF1_fnc)),
% 230.81/29.71 inference(forward_demodulation,[status(thm)],[f19468,f46736])).
% 230.81/29.71 fof(f46831,plain,(
% 230.81/29.71 ![X0]: (join(X0,sF0_fnc)=join(sF0_fnc,join(sF1_fnc,X0)))),
% 188.24/29.90 inference(paramodulation,[status(thm)],[f46748,f5598])).
% 188.24/29.90 fof(f49127,plain,(
% 188.24/29.90 ![X0,X1]: (meet(X0,join(meet(X0,X1),complement(meet(complement(X1),X0))))=meet(X0,X1))),
% 188.24/29.90 inference(paramodulation,[status(thm)],[f2377,f1006])).
% 188.24/29.90 fof(f49240,plain,(
% 188.24/29.90 ![X0,X1]: (meet(join(X0,X1),join(meet(top,X0),complement(X1)))=meet(top,X0))),
% 188.24/29.90 inference(paramodulation,[status(thm)],[f1461,f1006])).
% 188.24/29.90 fof(f49431,plain,(
% 188.24/29.90 ![X0,X1]: (meet(X0,join(meet(X0,X1),join(X1,complement(X0))))=meet(X0,X1))),
% 188.24/29.90 inference(forward_demodulation,[status(thm)],[f10274,f49127])).
% 188.24/29.90 fof(f49432,plain,(
% 188.24/29.90 ![X0,X1]: (meet(X0,join(X1,join(complement(X0),meet(X0,X1))))=meet(X0,X1))),
% 188.24/29.90 inference(forward_demodulation,[status(thm)],[f411,f49431])).
% 188.24/29.90 fof(f49433,plain,(
% 188.24/29.90 ![X0,X1]: (meet(X0,join(X1,complement(X0)))=meet(X0,X1))),
% 188.24/29.90 inference(forward_demodulation,[status(thm)],[f8691,f49432])).
% 188.24/29.90 fof(f49671,plain,(
% 188.24/29.90 ![X0,X1]: (meet(join(X0,X1),join(X0,complement(X1)))=meet(top,X0))),
% 188.24/29.90 inference(forward_demodulation,[status(thm)],[f1461,f49240])).
% 188.24/29.90 fof(f49678,plain,(
% 188.24/29.90 ![X0,X1]: (meet(join(X0,X1),join(X0,complement(X1)))=X0)),
% 188.24/29.90 inference(forward_demodulation,[status(thm)],[f1461,f49671])).
% 188.24/29.90 fof(f52685,plain,(
% 188.24/29.90 ![X0,X1,X2]: (meet(X0,join(X1,join(X2,complement(X0))))=meet(X0,join(X1,X2)))),
% 188.24/29.90 inference(paramodulation,[status(thm)],[f17,f49433])).
% 188.24/29.90 fof(f60087,plain,(
% 188.24/29.90 ![X0,X1]: (meet(join(X0,X1),join(X0,complement(meet(complement(X0),X1))))=X0)),
% 188.24/29.90 inference(paramodulation,[status(thm)],[f9568,f49678])).
% 188.24/29.90 fof(f60330,plain,(
% 188.24/29.90 ![X0,X1]: (meet(join(X0,X1),join(X0,join(X0,complement(X1))))=X0)),
% 188.24/29.90 inference(forward_demodulation,[status(thm)],[f10274,f60087])).
% 188.24/29.90 fof(f60332,plain,(
% 188.24/29.90 ![X0,X1]: (meet(join(X0,X1),join(complement(X1),X0))=X0)),
% 188.24/29.90 inference(forward_demodulation,[status(thm)],[f5495,f60330])).
% 188.24/29.90 fof(f111042,plain,(
% 188.24/29.90 join(meet(sK1_skl,complement(sK0_skl)),sF0_fnc)=join(sF0_fnc,sK1_skl)),
% 188.24/29.90 inference(paramodulation,[status(thm)],[f4439,f46831])).
% 188.24/29.90 fof(f111211,plain,(
% 188.24/29.90 join(sF0_fnc,meet(sK1_skl,complement(sK0_skl)))=join(sF0_fnc,sK1_skl)),
% 188.24/29.90 inference(forward_demodulation,[status(thm)],[f16,f111042])).
% 188.24/29.90 fof(f111212,plain,(
% 188.24/29.90 join(sF0_fnc,meet(sK1_skl,complement(sK0_skl)))=join(sK1_skl,sF0_fnc)),
% 188.24/29.90 inference(forward_demodulation,[status(thm)],[f16,f111211])).
% 188.24/29.90 fof(f111214,plain,(
% 188.24/29.90 join(sF0_fnc,meet(sK1_skl,complement(sK0_skl)))=sK1_skl),
% 188.24/29.90 inference(forward_demodulation,[status(thm)],[f3573,f111212])).
% 188.24/29.90 fof(f128676,plain,(
% 188.24/29.90 meet(sK1_skl,join(complement(meet(sK1_skl,complement(sK0_skl))),sF0_fnc))=sF0_fnc),
% 188.24/29.90 inference(paramodulation,[status(thm)],[f111214,f60332])).
% 188.24/29.90 fof(f128744,plain,(
% 188.24/29.90 meet(sK1_skl,join(sF0_fnc,complement(meet(sK1_skl,complement(sK0_skl)))))=sF0_fnc),
% 188.24/29.90 inference(forward_demodulation,[status(thm)],[f16,f128676])).
% 188.24/29.90 fof(f128745,plain,(
% 188.24/29.90 meet(sK1_skl,join(sF0_fnc,join(sK0_skl,complement(sK1_skl))))=sF0_fnc),
% 188.24/29.90 inference(forward_demodulation,[status(thm)],[f42405,f128744])).
% 188.24/29.90 fof(f128746,plain,(
% 188.24/29.90 meet(sK1_skl,join(sF0_fnc,sK0_skl))=sF0_fnc),
% 188.24/29.90 inference(forward_demodulation,[status(thm)],[f52685,f128745])).
% 188.24/29.90 fof(f128747,plain,(
% 188.24/29.90 meet(sK1_skl,join(sK0_skl,sF0_fnc))=sF0_fnc),
% 188.24/29.90 inference(forward_demodulation,[status(thm)],[f16,f128746])).
% 188.24/29.90 fof(f128748,plain,(
% 188.24/29.90 meet(sK1_skl,sK0_skl)=sF0_fnc),
% 188.24/29.90 inference(forward_demodulation,[status(thm)],[f3569,f128747])).
% 188.24/29.90 fof(f128749,plain,(
% 188.24/29.90 sF1_fnc=sF0_fnc),
% 188.24/29.90 inference(backward_demodulation,[status(thm)],[f128750,f34])).
% 188.24/29.90 fof(f128750,plain,(
% 188.24/29.90 meet(sK0_skl,sK1_skl)=sF0_fnc),
% 188.24/29.90 inference(forward_demodulation,[status(thm)],[f1671,f128748])).
% 188.24/29.90 fof(f128798,plain,(
% 188.24/29.90 $false),
% 188.24/29.90 inference(forward_subsumption_resolution,[status(thm)],[f128749,f36])).
% 188.24/29.90 % SZS output end CNFRefutation for theBenchmark.p
% 51.70/30.03 % Elapsed time: 29.554210 seconds
% 51.70/30.03 % CPU time: 233.331619 seconds
% 51.70/30.03 % Total memory used: 980.179 MB
% 51.70/30.03 % Net memory used: 957.136 MB
%------------------------------------------------------------------------------