%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL041+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:44 PM UTC 2026
% Result : Theorem 202.25s 26.10s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL041+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n006.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 04:07:27 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.47 % Drodi V4.1.1
% 202.25/26.10 % Refutation found
% 202.25/26.10 % SZS status Theorem for theBenchmark: Theorem is valid
% 202.25/26.10 % SZS output start CNFRefutation for theBenchmark
% 202.25/26.10 fof(f1,axiom,(
% 202.25/26.10 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 202.25/26.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 202.25/26.10 fof(f2,axiom,(
% 202.25/26.10 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 202.25/26.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 202.25/26.10 fof(f3,axiom,(
% 202.25/26.10 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 202.25/26.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 202.25/26.10 fof(f4,axiom,(
% 202.25/26.10 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 202.25/26.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 202.25/26.10 fof(f5,axiom,(
% 202.25/26.10 (! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2) )),
% 202.25/26.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 202.25/26.10 fof(f6,axiom,(
% 202.25/26.10 (! [X0] : composition(X0,one) = X0 )),
% 202.25/26.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 202.25/26.10 fof(f7,axiom,(
% 202.25/26.10 (! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) )),
% 202.25/26.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 202.25/26.10 fof(f8,axiom,(
% 202.25/26.10 (! [X0] : converse(converse(X0)) = X0 )),
% 202.25/26.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 202.25/26.10 fof(f9,axiom,(
% 202.25/26.10 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 202.25/26.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 202.25/26.10 fof(f10,axiom,(
% 202.25/26.10 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 202.25/26.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 202.25/26.10 fof(f11,axiom,(
% 202.25/26.10 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 202.25/26.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 202.25/26.10 fof(f12,axiom,(
% 202.25/26.10 (! [X0] : top = join(X0,complement(X0)) )),
% 202.25/26.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 202.25/26.10 fof(f13,axiom,(
% 202.25/26.10 (! [X0] : zero = meet(X0,complement(X0)) )),
% 202.25/26.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 202.25/26.10 fof(f14,axiom,(
% 202.25/26.10 (! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))) )),
% 202.25/26.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 202.25/26.10 fof(f15,axiom,(
% 202.25/26.10 (! [X0,X1,X2] : join(meet(composition(X0,X1),X2),meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2)) = meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2) )),
% 202.25/26.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 202.25/26.10 fof(f16,axiom,(
% 202.25/26.10 (! [X0,X1,X2] : join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2)) = meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2) )),
% 202.25/26.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 202.25/26.10 fof(f17,conjecture,(
% 202.25/26.10 (! [X0] :( join(composition(converse(X0),X0),one) = one=> (! [X1] : meet(composition(X0,X1),composition(X0,complement(X1))) = zero )) )),
% 202.25/26.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 202.25/26.10 fof(f18,negated_conjecture,(
% 202.25/26.10 ~((! [X0] :( join(composition(converse(X0),X0),one) = one=> (! [X1] : meet(composition(X0,X1),composition(X0,complement(X1))) = zero )) ))),
% 202.25/26.10 inference(negated_conjecture,[status(cth)],[f17])).
% 202.25/26.10 fof(f19,plain,(
% 202.25/26.10 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f1])).
% 202.25/26.10 fof(f20,plain,(
% 202.25/26.10 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f2])).
% 202.25/26.10 fof(f21,plain,(
% 202.25/26.10 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f3])).
% 202.25/26.10 fof(f22,plain,(
% 202.25/26.10 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f4])).
% 202.25/26.10 fof(f23,plain,(
% 202.25/26.10 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f5])).
% 202.25/26.10 fof(f24,plain,(
% 202.25/26.10 ![X0]: (composition(X0,one)=X0)),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f6])).
% 202.25/26.10 fof(f25,plain,(
% 202.25/26.10 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f7])).
% 202.25/26.10 fof(f26,plain,(
% 202.25/26.10 ![X0]: (converse(converse(X0))=X0)),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f8])).
% 202.25/26.10 fof(f27,plain,(
% 202.25/26.10 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f9])).
% 202.25/26.10 fof(f28,plain,(
% 202.25/26.10 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f10])).
% 202.25/26.10 fof(f29,plain,(
% 202.25/26.10 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f11])).
% 202.25/26.10 fof(f30,plain,(
% 202.25/26.10 ![X0]: (top=join(X0,complement(X0)))),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f12])).
% 202.25/26.10 fof(f31,plain,(
% 202.25/26.10 ![X0]: (zero=meet(X0,complement(X0)))),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f13])).
% 202.25/26.10 fof(f32,plain,(
% 202.25/26.10 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))))=composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))))),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f14])).
% 202.25/26.10 fof(f33,plain,(
% 202.25/26.10 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2))=meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2))),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f15])).
% 202.25/26.10 fof(f34,plain,(
% 202.25/26.10 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2))=meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2))),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f16])).
% 202.25/26.10 fof(f35,plain,(
% 202.25/26.10 (?[X0]: (join(composition(converse(X0),X0),one)=one&(?[X1]: ~meet(composition(X0,X1),composition(X0,complement(X1)))=zero)))),
% 202.25/26.10 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 202.25/26.10 fof(f36,plain,(
% 202.25/26.10 (join(composition(converse(sK0_skl),sK0_skl),one)=one&~meet(composition(sK0_skl,sK1_skl),composition(sK0_skl,complement(sK1_skl)))=zero)),
% 202.25/26.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl)],[f35])).
% 202.25/26.10 fof(f37,plain,(
% 202.25/26.10 join(composition(converse(sK0_skl),sK0_skl),one)=one),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f36])).
% 202.25/26.10 fof(f38,plain,(
% 202.25/26.10 ~meet(composition(sK0_skl,sK1_skl),composition(sK0_skl,complement(sK1_skl)))=zero),
% 202.25/26.10 inference(cnf_transformation,[status(thm)],[f36])).
% 202.25/26.10 fof(f39,definition,(
% 202.25/26.10 sF1_fnc=composition(sK0_skl,sK1_skl)),
% 202.25/26.10 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 202.25/26.10 fof(f40,definition,(
% 202.25/26.10 sF3_fnc=complement(sK1_skl)),
% 202.25/26.10 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 202.25/26.10 fof(f41,definition,(
% 202.25/26.10 sF2_fnc=composition(sK0_skl,sF3_fnc)),
% 202.25/26.10 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 202.25/26.10 fof(f42,definition,(
% 202.25/26.10 sF0_fnc=meet(sF1_fnc,sF2_fnc)),
% 202.25/26.10 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 202.25/26.10 fof(f43,plain,(
% 202.25/26.10 ~sF0_fnc=zero),
% 202.25/26.10 inference(definition_folding,[],[f38,f42,f41,f40,f39])).
% 202.25/26.10 fof(f44,plain,(
% 202.25/26.10 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f19,f21])).
% 202.25/26.10 fof(f45,plain,(
% 202.25/26.10 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 202.25/26.10 inference(backward_demodulation,[status(thm)],[f22,f44])).
% 202.25/26.10 fof(f46,plain,(
% 202.25/26.10 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f19,f29])).
% 202.25/26.10 fof(f47,plain,(
% 202.25/26.10 join(one,composition(converse(sK0_skl),sK0_skl))=one),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f19,f37])).
% 202.25/26.10 fof(f48,plain,(
% 202.25/26.10 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f19,f45])).
% 202.25/26.10 fof(f55,plain,(
% 202.25/26.10 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f26,f28])).
% 202.25/26.10 fof(f56,plain,(
% 202.25/26.10 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f19,f22])).
% 202.25/26.10 fof(f58,plain,(
% 202.25/26.10 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X0,X1),complement(X2))))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f22,f22])).
% 202.25/26.10 fof(f59,plain,(
% 202.25/26.10 ![X0,X1,X2]: (meet(X0,join(complement(X1),complement(X2)))=complement(join(complement(X0),meet(X1,X2))))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f22,f22])).
% 202.25/26.10 fof(f60,plain,(
% 202.25/26.10 ![X0,X1]: (zero=meet(join(complement(X0),complement(X1)),meet(X0,X1)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f22,f31])).
% 202.25/26.10 fof(f61,plain,(
% 202.25/26.10 ![X0,X1]: (zero=complement(join(meet(X0,X1),complement(meet(X0,X1)))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f58,f60])).
% 202.25/26.10 fof(f62,plain,(
% 202.25/26.10 zero=complement(top)),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f30,f61])).
% 202.25/26.10 fof(f63,plain,(
% 202.25/26.10 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f19,f20])).
% 202.25/26.10 fof(f77,plain,(
% 202.25/26.10 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f24,f23])).
% 202.25/26.10 fof(f94,plain,(
% 202.25/26.10 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f30,f20])).
% 202.25/26.10 fof(f110,plain,(
% 202.25/26.10 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f19,f27])).
% 202.25/26.10 fof(f113,plain,(
% 202.25/26.10 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f26,f27])).
% 202.25/26.10 fof(f115,plain,(
% 202.25/26.10 ![X0,X1]: (converse(join(X0,converse(X1)))=join(converse(X0),X1))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f26,f27])).
% 202.25/26.10 fof(f126,plain,(
% 202.25/26.10 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f22,f56])).
% 202.25/26.10 fof(f136,plain,(
% 202.25/26.10 ![X0,X1,X2]: (meet(X0,join(complement(X1),complement(X2)))=complement(join(complement(X0),meet(X2,X1))))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f56,f22])).
% 202.25/26.10 fof(f139,plain,(
% 202.25/26.10 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2))=meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)))),
% 202.25/26.10 inference(backward_demodulation,[status(thm)],[f126,f34])).
% 202.25/26.10 fof(f140,plain,(
% 202.25/26.10 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2))=meet(X2,composition(X0,meet(X1,composition(converse(X0),X2)))))),
% 202.25/26.10 inference(backward_demodulation,[status(thm)],[f126,f33])).
% 202.25/26.10 fof(f146,plain,(
% 202.25/26.10 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)))=meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f126,f139])).
% 202.25/26.10 fof(f147,plain,(
% 202.25/26.10 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(X2,composition(X0,meet(X1,composition(converse(X0),X2)))))=meet(X2,composition(X0,meet(X1,composition(converse(X0),X2)))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f126,f140])).
% 202.25/26.10 fof(f158,plain,(
% 202.25/26.10 ![X0,X1]: (converse(join(converse(X0),X1))=join(converse(X1),X0))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f26,f110])).
% 202.25/26.10 fof(f165,plain,(
% 202.25/26.10 ![X0]: (join(X0,top)=join(top,complement(complement(X0))))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f30,f94])).
% 202.25/26.10 fof(f184,plain,(
% 202.25/26.10 ![X0,X1,X2,X3]: (composition(join(X0,composition(X1,X2)),X3)=join(composition(X0,X3),composition(X1,composition(X2,X3))))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f23,f25])).
% 202.25/26.10 fof(f210,plain,(
% 202.25/26.10 ![X0,X1]: (join(complement(converse(X0)),composition(converse(converse(X1)),complement(converse(composition(X0,X1)))))=complement(converse(X0)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f28,f46])).
% 202.25/26.10 fof(f221,plain,(
% 202.25/26.10 ![X0,X1]: (join(complement(converse(X0)),composition(X1,complement(converse(composition(X0,X1)))))=complement(converse(X0)))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f26,f210])).
% 202.25/26.10 fof(f246,plain,(
% 202.25/26.10 ![X0,X1,X2]: (join(meet(composition(converse(X0),X1),X2),composition(meet(converse(X0),composition(X2,converse(X1))),meet(X1,composition(X0,X2))))=composition(meet(converse(X0),composition(X2,converse(X1))),meet(X1,composition(converse(converse(X0)),X2))))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f26,f32])).
% 202.25/26.10 fof(f270,plain,(
% 202.25/26.10 ![X0,X1,X2]: (join(meet(composition(converse(X0),X1),X2),composition(meet(converse(X0),composition(X2,converse(X1))),meet(X1,composition(X0,X2))))=composition(meet(converse(X0),composition(X2,converse(X1))),meet(X1,composition(X0,X2))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f26,f246])).
% 202.25/26.10 fof(f289,plain,(
% 202.25/26.10 zero=meet(sK1_skl,sF3_fnc)),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f40,f31])).
% 202.25/26.10 fof(f296,plain,(
% 202.25/26.10 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f24,f55])).
% 202.25/26.10 fof(f315,plain,(
% 202.25/26.10 ![X0]: (X0=composition(converse(one),X0))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f26,f296])).
% 202.25/26.10 fof(f332,plain,(
% 202.25/26.10 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f77,f315])).
% 202.25/26.10 fof(f333,plain,(
% 202.25/26.10 one=converse(one)),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f24,f315])).
% 202.25/26.10 fof(f334,plain,(
% 202.25/26.10 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f315,f46])).
% 202.25/26.10 fof(f344,plain,(
% 202.25/26.10 ![X0,X1]: (composition(join(X0,converse(one)),X1)=join(composition(X0,X1),X1))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f315,f25])).
% 202.25/26.10 fof(f345,plain,(
% 202.25/26.10 ![X0,X1]: (composition(join(converse(one),X0),X1)=join(X1,composition(X0,X1)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f315,f25])).
% 202.25/26.10 fof(f353,plain,(
% 202.25/26.10 ![X0]: (composition(one,X0)=X0)),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f315,f332])).
% 202.25/26.10 fof(f356,plain,(
% 202.25/26.10 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f353,f334])).
% 202.25/26.10 fof(f378,plain,(
% 202.25/26.10 ![X0,X1]: (composition(join(X0,one),X1)=join(composition(X0,X1),X1))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f333,f344])).
% 202.25/26.10 fof(f380,plain,(
% 202.25/26.10 ![X0,X1]: (composition(join(X0,one),X1)=join(X1,composition(X0,X1)))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f19,f378])).
% 202.25/26.10 fof(f381,plain,(
% 202.25/26.10 ![X0,X1]: (composition(join(one,X0),X1)=join(X1,composition(X0,X1)))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f333,f345])).
% 202.25/26.10 fof(f446,plain,(
% 202.25/26.10 ![X0,X1]: (join(meet(X0,X1),complement(join(complement(X1),complement(X0))))=complement(join(complement(X1),complement(X0))))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f56,f356])).
% 202.25/26.10 fof(f447,plain,(
% 202.25/26.10 ![X0,X1]: (join(meet(X0,X1),complement(join(complement(X0),complement(X1))))=complement(join(complement(X0),complement(X1))))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f22,f356])).
% 202.25/26.10 fof(f451,plain,(
% 202.25/26.10 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f356,f56])).
% 202.25/26.10 fof(f453,plain,(
% 202.25/26.10 ![X0]: (join(X0,complement(X0))=join(top,complement(X0)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f356,f94])).
% 202.25/26.10 fof(f457,plain,(
% 202.25/26.10 ![X0,X1]: (join(meet(X0,X1),meet(X0,X1))=complement(join(complement(X1),complement(X0))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f56,f446])).
% 202.25/26.10 fof(f458,plain,(
% 202.25/26.10 ![X0,X1]: (join(meet(X0,X1),meet(X0,X1))=meet(X0,X1))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f56,f457])).
% 202.25/26.10 fof(f459,plain,(
% 202.25/26.10 ![X0,X1]: (join(meet(X0,X1),meet(X1,X0))=complement(join(complement(X0),complement(X1))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f56,f447])).
% 202.25/26.10 fof(f460,plain,(
% 202.25/26.10 ![X0,X1]: (join(meet(X0,X1),meet(X1,X0))=meet(X1,X0))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f56,f459])).
% 202.25/26.10 fof(f470,plain,(
% 202.25/26.10 ![X0]: (join(X0,top)=top)),
% 202.25/26.10 inference(backward_demodulation,[status(thm)],[f471,f165])).
% 202.25/26.10 fof(f471,plain,(
% 202.25/26.10 ![X0]: (top=join(top,complement(X0)))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f30,f453])).
% 202.25/26.10 fof(f481,plain,(
% 202.25/26.10 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f31,f48])).
% 202.25/26.10 fof(f484,plain,(
% 202.25/26.10 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f56,f48])).
% 202.25/26.10 fof(f485,plain,(
% 202.25/26.10 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f22,f48])).
% 202.25/26.10 fof(f488,plain,(
% 202.25/26.10 ![X0,X1]: (X0=join(meet(X0,join(complement(complement(X0)),X1)),complement(join(top,X1))))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f94,f48])).
% 202.25/26.10 fof(f489,plain,(
% 202.25/26.10 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f30,f48])).
% 202.25/26.10 fof(f497,plain,(
% 202.25/26.10 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f56,f481])).
% 202.25/26.10 fof(f498,plain,(
% 202.25/26.10 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f451,f497])).
% 202.25/26.10 fof(f499,plain,(
% 202.25/26.10 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f19,f484])).
% 202.25/26.10 fof(f500,plain,(
% 202.25/26.10 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f19,f485])).
% 202.25/26.10 fof(f505,plain,(
% 202.25/26.10 ![X0,X1]: (X0=join(complement(join(top,X1)),meet(X0,join(complement(complement(X0)),X1))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f19,f488])).
% 202.25/26.10 fof(f506,plain,(
% 202.25/26.10 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(X0)))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f19,f489])).
% 202.25/26.10 fof(f507,plain,(
% 202.25/26.10 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f62,f506])).
% 202.25/26.10 fof(f513,plain,(
% 202.25/26.10 ![X0]: (join(top,X0)=top)),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f19,f470])).
% 202.25/26.10 fof(f517,plain,(
% 202.25/26.10 ![X0]: (X0=join(meet(X0,top),complement(top)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f470,f48])).
% 202.25/26.10 fof(f527,plain,(
% 202.25/26.10 ![X0,X1]: (X0=join(complement(top),meet(X0,join(complement(complement(X0)),X1))))),
% 202.25/26.10 inference(backward_demodulation,[status(thm)],[f513,f505])).
% 202.25/26.10 fof(f535,plain,(
% 202.25/26.10 ![X0]: (X0=join(complement(top),meet(X0,top)))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f19,f517])).
% 202.25/26.10 fof(f536,plain,(
% 202.25/26.10 ![X0]: (X0=join(zero,meet(X0,top)))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f62,f535])).
% 202.25/26.10 fof(f541,plain,(
% 202.25/26.10 ![X0,X1]: (X0=join(zero,meet(X0,join(complement(complement(X0)),X1))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f62,f527])).
% 202.25/26.10 fof(f576,plain,(
% 202.25/26.10 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(meet(X0,X1))))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f22,f498])).
% 202.25/26.10 fof(f579,plain,(
% 202.25/26.10 ![X0]: (X0=join(zero,meet(top,X0)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f126,f536])).
% 202.25/26.10 fof(f591,plain,(
% 202.25/26.10 top=complement(complement(top))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f579,f507])).
% 202.25/26.10 fof(f592,plain,(
% 202.25/26.10 sK1_skl=join(zero,meet(sK1_skl,complement(sF3_fnc)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f40,f507])).
% 202.25/26.10 fof(f594,plain,(
% 202.25/26.10 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,meet(join(complement(X0),complement(X1)),complement(meet(X0,X1)))))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f22,f507])).
% 202.25/26.10 fof(f597,plain,(
% 202.25/26.10 top=complement(zero)),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f62,f591])).
% 202.25/26.10 fof(f601,plain,(
% 202.25/26.10 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,meet(complement(meet(X0,X1)),join(complement(X0),complement(X1)))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f126,f594])).
% 202.25/26.10 fof(f602,plain,(
% 202.25/26.10 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(join(complement(complement(meet(X0,X1))),meet(X1,X0)))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f136,f601])).
% 202.25/26.10 fof(f603,plain,(
% 202.25/26.10 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(join(meet(X1,X0),complement(complement(meet(X0,X1)))))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f19,f602])).
% 202.25/26.10 fof(f611,plain,(
% 202.25/26.10 ![X0]: (meet(zero,X0)=complement(join(complement(X0),top)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f597,f56])).
% 202.25/26.10 fof(f626,plain,(
% 202.25/26.10 ![X0]: (meet(zero,X0)=complement(top))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f470,f611])).
% 202.25/26.10 fof(f628,plain,(
% 202.25/26.10 ![X0]: (meet(zero,X0)=zero)),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f62,f626])).
% 202.25/26.10 fof(f658,plain,(
% 202.25/26.10 ![X0,X1,X2,X3]: (join(meet(composition(X0,X1),X2),join(meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)),X3))=join(meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)),X3))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f146,f20])).
% 202.25/26.10 fof(f698,plain,(
% 202.25/26.10 ![X0]: (join(meet(sF2_fnc,X0),meet(X0,composition(sK0_skl,meet(sF3_fnc,composition(converse(sK0_skl),X0)))))=meet(X0,composition(sK0_skl,meet(sF3_fnc,composition(converse(sK0_skl),X0)))))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f41,f147])).
% 202.25/26.10 fof(f761,plain,(
% 202.25/26.10 ![X0,X1]: (meet(top,X0)=complement(join(meet(X1,complement(X1)),complement(X0))))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f30,f58])).
% 202.25/26.10 fof(f779,plain,(
% 202.25/26.10 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(join(meet(X0,X1),complement(complement(complement(join(complement(X0),complement(X1)))))))))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f58,f507])).
% 202.25/26.10 fof(f790,plain,(
% 202.25/26.10 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f31,f761])).
% 202.25/26.10 fof(f814,plain,(
% 202.25/26.10 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(join(meet(X0,X1),complement(complement(meet(X1,X0)))))))),
% 202.25/26.10 inference(forward_demodulation,[status(thm)],[f56,f779])).
% 202.25/26.10 fof(f867,plain,(
% 202.25/26.10 ![X0,X1]: (X0=join(meet(X1,X0),meet(complement(X1),X0)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f126,f499])).
% 202.25/26.10 fof(f870,plain,(
% 202.25/26.10 ![X0]: (X0=join(meet(sK1_skl,X0),meet(X0,sF3_fnc)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f40,f499])).
% 202.25/26.10 fof(f894,plain,(
% 202.25/26.10 ![X0]: (X0=join(meet(X0,sK1_skl),meet(X0,sF3_fnc)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f126,f870])).
% 202.25/26.10 fof(f898,plain,(
% 202.25/26.10 ![X0]: (X0=join(meet(sK1_skl,X0),meet(sF3_fnc,X0)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f126,f870])).
% 202.25/26.10 fof(f957,plain,(
% 202.25/26.10 ![X0]: (X0=join(meet(X0,sK1_skl),meet(sF3_fnc,X0)))),
% 202.25/26.10 inference(paramodulation,[status(thm)],[f126,f894])).
% 202.25/26.10 fof(f983,plain,(
% 202.25/26.10 complement(sF3_fnc)=join(meet(sK1_skl,complement(sF3_fnc)),zero)),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f31,f898])).
% 202.25/26.11 fof(f996,plain,(
% 202.25/26.11 complement(sF3_fnc)=join(zero,meet(sK1_skl,complement(sF3_fnc)))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f19,f983])).
% 202.25/26.11 fof(f1004,plain,(
% 202.25/26.11 complement(sF3_fnc)=sK1_skl),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f592,f996])).
% 202.25/26.11 fof(f1023,plain,(
% 202.25/26.11 ![X0,X1]: (meet(X0,top)=complement(join(complement(X0),meet(X1,complement(X1)))))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f30,f59])).
% 202.25/26.11 fof(f1055,plain,(
% 202.25/26.11 ![X0]: (meet(X0,top)=complement(join(complement(X0),zero)))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f31,f1023])).
% 202.25/26.11 fof(f1056,plain,(
% 202.25/26.11 ![X0]: (meet(X0,top)=complement(join(zero,complement(X0))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f19,f1055])).
% 202.25/26.11 fof(f1102,plain,(
% 202.25/26.11 ![X0,X1]: (meet(X0,join(complement(X1),zero))=complement(join(complement(X0),meet(X1,top))))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f62,f59])).
% 202.25/26.11 fof(f1105,plain,(
% 202.25/26.11 ![X0,X1]: (meet(join(complement(X0),zero),X1)=complement(join(meet(X0,top),complement(X1))))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f62,f58])).
% 202.25/26.11 fof(f1119,plain,(
% 202.25/26.11 ![X0,X1]: (meet(X0,join(zero,complement(X1)))=complement(join(complement(X0),meet(X1,top))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f19,f1102])).
% 202.25/26.11 fof(f1122,plain,(
% 202.25/26.11 ![X0,X1]: (meet(join(zero,complement(X0)),X1)=complement(join(meet(X0,top),complement(X1))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f19,f1105])).
% 202.25/26.11 fof(f1260,plain,(
% 202.25/26.11 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f126,f500])).
% 202.25/26.11 fof(f1303,plain,(
% 202.25/26.11 ![X0]: (complement(complement(X0))=join(meet(X0,complement(complement(X0))),zero))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f31,f867])).
% 202.25/26.11 fof(f1304,plain,(
% 202.25/26.11 ![X0]: (complement(X0)=join(meet(X0,complement(X0)),complement(complement(complement(X0)))))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f451,f867])).
% 202.25/26.11 fof(f1324,plain,(
% 202.25/26.11 ![X0]: (complement(complement(X0))=join(zero,meet(X0,complement(complement(X0)))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f19,f1303])).
% 202.25/26.11 fof(f1326,plain,(
% 202.25/26.11 ![X0]: (X0=join(zero,X0))),
% 202.25/26.11 inference(backward_demodulation,[status(thm)],[f1345,f498])).
% 202.25/26.11 fof(f1328,plain,(
% 202.25/26.11 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(join(meet(X0,X1),meet(X1,X0)))))),
% 202.25/26.11 inference(backward_demodulation,[status(thm)],[f1345,f814])).
% 202.25/26.11 fof(f1329,plain,(
% 202.25/26.11 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(join(meet(X1,X0),meet(X0,X1)))))),
% 202.25/26.11 inference(backward_demodulation,[status(thm)],[f1345,f603])).
% 202.25/26.11 fof(f1343,plain,(
% 202.25/26.11 ![X0,X1]: (X0=join(zero,meet(X0,join(X0,X1))))),
% 202.25/26.11 inference(backward_demodulation,[status(thm)],[f1345,f541])).
% 202.25/26.11 fof(f1345,plain,(
% 202.25/26.11 ![X0]: (complement(complement(X0))=X0)),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f507,f1324])).
% 202.25/26.11 fof(f1346,plain,(
% 202.25/26.11 ![X0]: (complement(X0)=join(complement(complement(complement(X0))),meet(X0,complement(X0))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f19,f1304])).
% 202.25/26.11 fof(f1347,plain,(
% 202.25/26.11 ![X0]: (complement(X0)=join(complement(X0),meet(X0,complement(X0))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f1345,f1346])).
% 202.25/26.11 fof(f1348,plain,(
% 202.25/26.11 ![X0]: (complement(X0)=join(complement(X0),zero))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f31,f1347])).
% 202.25/26.11 fof(f1350,plain,(
% 202.25/26.11 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 202.25/26.11 inference(backward_demodulation,[status(thm)],[f1358,f576])).
% 202.25/26.11 fof(f1353,plain,(
% 202.25/26.11 ![X0,X1]: (meet(complement(X0),X1)=complement(join(meet(X0,top),complement(X1))))),
% 202.25/26.11 inference(backward_demodulation,[status(thm)],[f1358,f1122])).
% 202.25/26.11 fof(f1355,plain,(
% 202.25/26.11 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),meet(X1,top))))),
% 202.25/26.11 inference(backward_demodulation,[status(thm)],[f1358,f1119])).
% 202.25/26.11 fof(f1356,plain,(
% 202.25/26.11 ![X0]: (meet(X0,top)=complement(complement(X0)))),
% 202.25/26.11 inference(backward_demodulation,[status(thm)],[f1358,f1056])).
% 202.25/26.11 fof(f1357,plain,(
% 202.25/26.11 ![X0]: (meet(top,X0)=complement(complement(X0)))),
% 202.25/26.11 inference(backward_demodulation,[status(thm)],[f1358,f790])).
% 202.25/26.11 fof(f1358,plain,(
% 202.25/26.11 ![X0]: (complement(X0)=join(zero,complement(X0)))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f19,f1348])).
% 202.25/26.11 fof(f1385,plain,(
% 202.25/26.11 ![X0,X1]: (join(complement(X0),complement(X1))=complement(join(meet(X0,X1),meet(X1,X0))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f1358,f1328])).
% 202.25/26.11 fof(f1386,plain,(
% 202.25/26.11 ![X0,X1,X2]: (meet(X0,complement(meet(X1,X2)))=complement(join(complement(X0),meet(X2,X1))))),
% 202.25/26.11 inference(backward_demodulation,[status(thm)],[f1414,f59])).
% 202.25/26.11 fof(f1414,plain,(
% 202.25/26.11 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X1,X0)))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f460,f1385])).
% 202.25/26.11 fof(f1415,plain,(
% 202.25/26.11 ![X0,X1]: (complement(meet(X0,X1))=join(zero,complement(join(meet(X0,X1),meet(X1,X0)))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f1414,f1329])).
% 202.25/26.11 fof(f1416,plain,(
% 202.25/26.11 ![X0,X1]: (complement(meet(X0,X1))=complement(join(meet(X0,X1),meet(X1,X0))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f1358,f1415])).
% 202.25/26.11 fof(f1417,plain,(
% 202.25/26.11 ![X0,X1]: (complement(meet(X0,X1))=complement(meet(X1,X0)))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f460,f1416])).
% 202.25/26.11 fof(f1442,plain,(
% 202.25/26.11 ![X0,X1]: (X0=meet(X0,join(X0,X1)))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f1326,f1343])).
% 202.25/26.11 fof(f1445,plain,(
% 202.25/26.11 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),X1)))),
% 202.25/26.11 inference(backward_demodulation,[status(thm)],[f1447,f1355])).
% 202.25/26.11 fof(f1446,plain,(
% 202.25/26.11 ![X0,X1]: (meet(complement(X0),X1)=complement(join(X0,complement(X1))))),
% 202.25/26.11 inference(backward_demodulation,[status(thm)],[f1447,f1353])).
% 202.25/26.11 fof(f1447,plain,(
% 202.25/26.11 ![X0]: (meet(X0,top)=X0)),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f1345,f1356])).
% 202.25/26.11 fof(f1450,plain,(
% 202.25/26.11 ![X0]: (meet(top,X0)=X0)),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f1345,f1357])).
% 202.25/26.11 fof(f1520,plain,(
% 202.25/26.11 ![X0,X1,X2]: (meet(X0,complement(meet(X1,X2)))=meet(X0,complement(meet(X2,X1))))),
% 202.25/26.11 inference(backward_demodulation,[status(thm)],[f1445,f1386])).
% 202.25/26.11 fof(f1557,plain,(
% 202.25/26.11 ![X0]: (X0=join(X0,zero))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f19,f1326])).
% 202.25/26.11 fof(f2199,plain,(
% 202.25/26.11 ![X0]: (converse(converse(X0))=join(converse(zero),X0))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f1326,f115])).
% 202.25/26.11 fof(f2228,plain,(
% 202.25/26.11 ![X0]: (X0=join(converse(zero),X0))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f26,f2199])).
% 202.25/26.11 fof(f2254,plain,(
% 202.25/26.11 zero=converse(zero)),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f1557,f2228])).
% 202.25/26.11 fof(f2515,plain,(
% 202.25/26.11 ![X0]: (converse(composition(zero,X0))=composition(converse(X0),zero))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f2254,f55])).
% 202.25/26.11 fof(f2660,plain,(
% 202.25/26.11 ![X0]: (join(X0,meet(top,X0))=meet(top,X0))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f1450,f458])).
% 202.25/26.11 fof(f2679,plain,(
% 202.25/26.11 ![X0]: (join(X0,X0)=meet(top,X0))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f1450,f2660])).
% 202.25/26.11 fof(f2684,plain,(
% 202.25/26.11 ![X0]: (join(X0,X0)=X0)),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f1450,f2679])).
% 202.25/26.11 fof(f2734,plain,(
% 202.25/26.11 ![X0,X1]: (join(X0,X1)=join(X1,join(X0,X1)))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f2684,f63])).
% 202.25/26.11 fof(f2773,plain,(
% 202.25/26.11 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f30,f113])).
% 202.25/26.11 fof(f3547,plain,(
% 202.25/26.11 ![X0,X1]: (join(complement(X0),X1)=complement(meet(complement(X1),X0)))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f1345,f1414])).
% 202.25/26.11 fof(f3602,plain,(
% 202.25/26.11 ![X0,X1]: (join(X0,complement(X1))=complement(meet(complement(X0),X1)))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f1345,f1350])).
% 202.25/26.11 fof(f3652,plain,(
% 202.25/26.11 ![X0]: (meet(sF3_fnc,complement(X0))=complement(join(sK1_skl,X0)))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f1004,f1445])).
% 202.25/26.11 fof(f3718,plain,(
% 202.25/26.11 ![X0,X1,X2]: (join(complement(X0),meet(complement(X1),X2))=complement(meet(join(X1,complement(X2)),X0)))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f1446,f1414])).
% 202.25/26.11 fof(f3776,plain,(
% 202.25/26.11 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X0))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f1260,f1442])).
% 202.25/26.11 fof(f3832,plain,(
% 202.25/26.11 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X0,X1)))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f126,f3776])).
% 202.25/26.11 fof(f4136,plain,(
% 202.25/26.11 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X1,X0)))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f126,f3832])).
% 202.25/26.11 fof(f4439,plain,(
% 202.25/26.11 ![X0,X1]: (join(meet(X0,X1),meet(complement(X1),X0))=join(meet(complement(X1),X0),X0))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f1260,f2734])).
% 202.25/26.11 fof(f4441,plain,(
% 202.25/26.11 ![X0,X1]: (join(meet(X0,X1),meet(X0,complement(X1)))=join(meet(X0,complement(X1)),X0))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f500,f2734])).
% 202.25/26.11 fof(f4544,plain,(
% 202.25/26.11 ![X0,X1]: (X0=join(meet(complement(X1),X0),X0))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f1260,f4439])).
% 202.25/26.11 fof(f4547,plain,(
% 202.25/26.11 ![X0,X1]: (X0=join(X0,meet(complement(X1),X0)))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f19,f4544])).
% 202.25/26.11 fof(f4550,plain,(
% 202.25/26.11 ![X0,X1]: (X0=join(meet(X0,complement(X1)),X0))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f500,f4441])).
% 202.25/26.11 fof(f4555,plain,(
% 202.25/26.11 ![X0,X1]: (X0=join(X0,meet(X0,complement(X1))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f19,f4550])).
% 202.25/26.11 fof(f5132,plain,(
% 202.25/26.11 ![X0]: (complement(X0)=join(meet(complement(X0),sK1_skl),complement(join(sK1_skl,X0))))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f3652,f957])).
% 202.25/26.11 fof(f5161,plain,(
% 202.25/26.11 ![X0]: (complement(X0)=join(complement(join(sK1_skl,X0)),meet(complement(X0),sK1_skl)))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f19,f5132])).
% 202.25/26.11 fof(f5162,plain,(
% 202.25/26.11 ![X0]: (complement(X0)=complement(meet(join(X0,complement(sK1_skl)),join(sK1_skl,X0))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f3718,f5161])).
% 202.25/26.11 fof(f5163,plain,(
% 202.25/26.11 ![X0]: (complement(X0)=complement(meet(join(sK1_skl,X0),join(X0,complement(sK1_skl)))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f1417,f5162])).
% 202.25/26.11 fof(f5164,plain,(
% 202.25/26.11 ![X0]: (complement(X0)=complement(meet(join(sK1_skl,X0),join(X0,sF3_fnc))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f40,f5163])).
% 202.25/26.11 fof(f5317,plain,(
% 202.25/26.11 ![X0,X1]: (X0=join(X0,meet(X0,X1)))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f1345,f4555])).
% 202.25/26.11 fof(f5391,plain,(
% 202.25/26.11 ![X0,X1]: (X0=join(X0,meet(X1,X0)))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f1345,f4547])).
% 202.25/26.11 fof(f5487,plain,(
% 202.25/26.11 ![X0,X1,X2]: (join(X0,join(meet(X0,X1),X2))=join(X2,X0))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f5317,f63])).
% 202.25/26.11 fof(f5581,plain,(
% 202.25/26.11 ![X0,X1,X2]: (join(X0,join(meet(X1,X0),X2))=join(X0,X2))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f5391,f20])).
% 202.25/26.11 fof(f8263,plain,(
% 202.25/26.11 ![X0,X1]: (converse(composition(zero,join(converse(X0),X1)))=composition(join(converse(X1),X0),zero))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f158,f2515])).
% 202.25/26.11 fof(f8304,plain,(
% 202.25/26.11 ![X0,X1]: (composition(join(converse(X0),X1),zero)=join(converse(composition(zero,X0)),composition(X1,zero)))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f2515,f25])).
% 202.25/26.11 fof(f8562,plain,(
% 202.25/26.11 converse(top)=top),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f513,f2773])).
% 202.25/26.11 fof(f8752,plain,(
% 202.25/26.11 ![X0]: (join(complement(top),composition(X0,complement(converse(composition(top,X0)))))=complement(converse(top)))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f8562,f221])).
% 202.25/26.11 fof(f8799,plain,(
% 202.25/26.11 ![X0]: (join(zero,composition(X0,complement(converse(composition(top,X0)))))=complement(converse(top)))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f62,f8752])).
% 202.25/26.11 fof(f8800,plain,(
% 202.25/26.11 ![X0]: (composition(X0,complement(converse(composition(top,X0))))=complement(converse(top)))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f1326,f8799])).
% 202.25/26.11 fof(f8801,plain,(
% 202.25/26.11 ![X0]: (composition(X0,complement(converse(composition(top,X0))))=complement(top))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f8562,f8800])).
% 202.25/26.11 fof(f8802,plain,(
% 202.25/26.11 ![X0]: (composition(X0,complement(converse(composition(top,X0))))=zero)),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f62,f8801])).
% 202.25/26.11 fof(f12217,plain,(
% 202.25/26.11 ![X0,X1]: (join(X0,X1)=join(meet(X1,complement(X0)),X0))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f499,f5487])).
% 202.25/26.11 fof(f12353,plain,(
% 202.25/26.11 ![X0,X1]: (join(X0,X1)=join(X0,meet(X1,complement(X0))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f19,f12217])).
% 202.25/26.11 fof(f22995,plain,(
% 202.25/26.11 ![X0]: (complement(complement(X0))=meet(join(sK1_skl,X0),join(X0,sF3_fnc)))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f5164,f1345])).
% 202.25/26.11 fof(f23159,plain,(
% 202.25/26.11 ![X0]: (X0=meet(join(sK1_skl,X0),join(X0,sF3_fnc)))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f1345,f22995])).
% 202.25/26.11 fof(f23615,plain,(
% 202.25/26.11 ![X0]: (meet(X0,complement(sK1_skl))=meet(join(sK1_skl,X0),join(meet(X0,complement(sK1_skl)),sF3_fnc)))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f12353,f23159])).
% 202.25/26.11 fof(f23708,plain,(
% 202.25/26.11 ![X0]: (meet(X0,sF3_fnc)=meet(join(sK1_skl,X0),join(meet(X0,complement(sK1_skl)),sF3_fnc)))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f40,f23615])).
% 202.25/26.11 fof(f23709,plain,(
% 202.25/26.11 ![X0]: (meet(X0,sF3_fnc)=meet(join(sK1_skl,X0),join(sF3_fnc,meet(X0,complement(sK1_skl)))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f19,f23708])).
% 202.25/26.11 fof(f23710,plain,(
% 202.25/26.11 ![X0]: (meet(X0,sF3_fnc)=meet(join(sK1_skl,X0),join(sF3_fnc,meet(X0,sF3_fnc))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f40,f23709])).
% 202.25/26.11 fof(f23711,plain,(
% 202.25/26.11 ![X0]: (meet(X0,sF3_fnc)=meet(join(sK1_skl,X0),sF3_fnc))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f5391,f23710])).
% 202.25/26.11 fof(f23712,plain,(
% 202.25/26.11 ![X0]: (meet(X0,sF3_fnc)=meet(sF3_fnc,join(sK1_skl,X0)))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f126,f23711])).
% 202.25/26.11 fof(f25336,plain,(
% 202.25/26.11 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f24,f658])).
% 202.25/26.11 fof(f25488,plain,(
% 202.25/26.11 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,meet(X0,composition(X1,converse(one)))),X2))=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f24,f25336])).
% 202.25/26.11 fof(f25489,plain,(
% 202.25/26.11 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,meet(X0,composition(X1,one))),X2))=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f333,f25488])).
% 202.25/26.11 fof(f25490,plain,(
% 202.25/26.11 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,meet(X0,X1)),X2))=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f24,f25489])).
% 202.25/26.11 fof(f25491,plain,(
% 202.25/26.11 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f5581,f25490])).
% 202.25/26.11 fof(f25492,plain,(
% 202.25/26.11 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,meet(X0,composition(X1,converse(one)))),X2))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f24,f25491])).
% 202.25/26.11 fof(f25493,plain,(
% 202.25/26.11 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,meet(X0,composition(X1,one))),X2))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f333,f25492])).
% 202.25/26.11 fof(f25494,plain,(
% 202.25/26.11 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,meet(X0,X1)),X2))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f24,f25493])).
% 202.25/26.11 fof(f25495,plain,(
% 202.25/26.11 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,X0),X2))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f4136,f25494])).
% 202.25/26.11 fof(f34770,plain,(
% 202.25/26.11 ![X0,X1]: (X0=meet(X0,composition(join(X1,one),X0)))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f380,f1442])).
% 202.25/26.11 fof(f38404,plain,(
% 202.25/26.11 ![X0]: (X0=meet(X0,composition(top,X0)))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f513,f34770])).
% 202.25/26.11 fof(f38761,plain,(
% 202.25/26.11 top=composition(top,top)),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f1450,f38404])).
% 202.25/26.11 fof(f39169,plain,(
% 202.25/26.11 ![X0]: (join(meet(composition(converse(top),X0),top),composition(meet(converse(top),composition(top,converse(X0))),meet(X0,top)))=composition(meet(converse(top),composition(top,converse(X0))),meet(X0,composition(top,top))))),
% 202.25/26.11 inference(paramodulation,[status(thm)],[f38761,f270])).
% 202.25/26.11 fof(f39367,plain,(
% 202.25/26.11 ![X0]: (join(meet(top,composition(converse(top),X0)),composition(meet(converse(top),composition(top,converse(X0))),meet(X0,top)))=composition(meet(converse(top),composition(top,converse(X0))),meet(X0,composition(top,top))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f25495,f39169])).
% 202.25/26.11 fof(f39368,plain,(
% 202.25/26.11 ![X0]: (join(composition(converse(top),X0),composition(meet(converse(top),composition(top,converse(X0))),meet(X0,top)))=composition(meet(converse(top),composition(top,converse(X0))),meet(X0,composition(top,top))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f1450,f39367])).
% 202.25/26.11 fof(f39369,plain,(
% 202.25/26.11 ![X0]: (join(composition(top,X0),composition(meet(converse(top),composition(top,converse(X0))),meet(X0,top)))=composition(meet(converse(top),composition(top,converse(X0))),meet(X0,composition(top,top))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f8562,f39368])).
% 202.25/26.11 fof(f39370,plain,(
% 202.25/26.11 ![X0]: (join(composition(top,X0),composition(meet(top,composition(top,converse(X0))),meet(X0,top)))=composition(meet(converse(top),composition(top,converse(X0))),meet(X0,composition(top,top))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f8562,f39369])).
% 202.25/26.11 fof(f39371,plain,(
% 202.25/26.11 ![X0]: (join(composition(top,X0),composition(composition(top,converse(X0)),meet(X0,top)))=composition(meet(converse(top),composition(top,converse(X0))),meet(X0,composition(top,top))))),
% 202.25/26.11 inference(forward_demodulation,[status(thm)],[f1450,f39370])).
% 202.25/26.11 fof(f39372,plain,(
% 202.25/26.11 ![X0]: (join(composition(top,X0),composition(top,composition(converse(X0),meet(X0,top))))=composition(meet(converse(top),composition(top,converse(X0))),meet(X0,composition(top,top))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f23,f39371])).
% 203.02/26.12 fof(f39373,plain,(
% 203.02/26.12 ![X0]: (join(composition(top,X0),composition(top,composition(converse(X0),X0)))=composition(meet(converse(top),composition(top,converse(X0))),meet(X0,composition(top,top))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f1447,f39372])).
% 203.02/26.12 fof(f39374,plain,(
% 203.02/26.12 ![X0]: (composition(join(top,composition(top,converse(X0))),X0)=composition(meet(converse(top),composition(top,converse(X0))),meet(X0,composition(top,top))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f184,f39373])).
% 203.02/26.12 fof(f39375,plain,(
% 203.02/26.12 ![X0]: (composition(top,X0)=composition(meet(converse(top),composition(top,converse(X0))),meet(X0,composition(top,top))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f513,f39374])).
% 203.02/26.12 fof(f39376,plain,(
% 203.02/26.12 ![X0]: (composition(top,X0)=composition(meet(top,composition(top,converse(X0))),meet(X0,composition(top,top))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f8562,f39375])).
% 203.02/26.12 fof(f39377,plain,(
% 203.02/26.12 ![X0]: (composition(top,X0)=composition(composition(top,converse(X0)),meet(X0,composition(top,top))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f1450,f39376])).
% 203.02/26.12 fof(f39378,plain,(
% 203.02/26.12 ![X0]: (composition(top,X0)=composition(top,composition(converse(X0),meet(X0,composition(top,top)))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f23,f39377])).
% 203.02/26.12 fof(f39379,plain,(
% 203.02/26.12 ![X0]: (composition(top,X0)=composition(top,composition(converse(X0),meet(X0,top))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f38761,f39378])).
% 203.02/26.12 fof(f39380,plain,(
% 203.02/26.12 ![X0]: (composition(top,X0)=composition(top,composition(converse(X0),X0)))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f1447,f39379])).
% 203.02/26.12 fof(f41327,plain,(
% 203.02/26.12 ![X0,X1,X2]: (join(X0,complement(complement(meet(X1,X2))))=complement(meet(complement(X0),complement(meet(X2,X1)))))),
% 203.02/26.12 inference(paramodulation,[status(thm)],[f1520,f3602])).
% 203.02/26.12 fof(f41328,plain,(
% 203.02/26.12 ![X0,X1,X2]: (join(complement(complement(meet(X0,X1))),X2)=complement(meet(complement(X2),complement(meet(X1,X0)))))),
% 203.02/26.12 inference(paramodulation,[status(thm)],[f1520,f3547])).
% 203.02/26.12 fof(f41599,plain,(
% 203.02/26.12 ![X0,X1,X2]: (join(X0,meet(X1,X2))=complement(meet(complement(X0),complement(meet(X2,X1)))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f1345,f41327])).
% 203.02/26.12 fof(f41600,plain,(
% 203.02/26.12 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(X0,complement(complement(meet(X2,X1)))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f3602,f41599])).
% 203.02/26.12 fof(f41601,plain,(
% 203.02/26.12 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(X0,meet(X2,X1)))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f1345,f41600])).
% 203.02/26.12 fof(f41602,plain,(
% 203.02/26.12 ![X0,X1,X2]: (join(meet(X0,X1),X2)=complement(meet(complement(X2),complement(meet(X1,X0)))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f1345,f41328])).
% 203.02/26.12 fof(f41603,plain,(
% 203.02/26.12 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(X2,complement(complement(meet(X1,X0)))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f3602,f41602])).
% 203.02/26.12 fof(f41612,plain,(
% 203.02/26.12 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(X2,meet(X1,X0)))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f1345,f41603])).
% 203.02/26.12 fof(f50267,plain,(
% 203.02/26.12 ![X0,X1,X2,X3]: (join(meet(X0,X1),meet(X2,X3))=join(meet(X1,X0),meet(X3,X2)))),
% 203.02/26.12 inference(paramodulation,[status(thm)],[f41612,f41612])).
% 203.02/26.12 fof(f50989,plain,(
% 203.02/26.12 ![X0]: (composition(one,X0)=join(X0,composition(composition(converse(sK0_skl),sK0_skl),X0)))),
% 203.02/26.12 inference(paramodulation,[status(thm)],[f47,f381])).
% 203.02/26.12 fof(f51203,plain,(
% 203.02/26.12 ![X0]: (X0=join(X0,composition(composition(converse(sK0_skl),sK0_skl),X0)))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f353,f50989])).
% 203.02/26.12 fof(f51204,plain,(
% 203.02/26.12 ![X0]: (X0=join(X0,composition(converse(sK0_skl),composition(sK0_skl,X0))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f23,f51203])).
% 203.02/26.12 fof(f58937,plain,(
% 203.02/26.12 ![X0]: (join(complement(converse(top)),composition(composition(converse(X0),X0),complement(converse(composition(top,X0)))))=complement(converse(top)))),
% 203.02/26.12 inference(paramodulation,[status(thm)],[f39380,f221])).
% 203.02/26.12 fof(f59323,plain,(
% 203.02/26.12 ![X0]: (join(complement(top),composition(composition(converse(X0),X0),complement(converse(composition(top,X0)))))=complement(converse(top)))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f8562,f58937])).
% 203.02/26.12 fof(f59324,plain,(
% 203.02/26.12 ![X0]: (join(zero,composition(composition(converse(X0),X0),complement(converse(composition(top,X0)))))=complement(converse(top)))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f62,f59323])).
% 203.02/26.12 fof(f59325,plain,(
% 203.02/26.12 ![X0]: (composition(composition(converse(X0),X0),complement(converse(composition(top,X0))))=complement(converse(top)))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f1326,f59324])).
% 203.02/26.12 fof(f59326,plain,(
% 203.02/26.12 ![X0]: (composition(converse(X0),composition(X0,complement(converse(composition(top,X0)))))=complement(converse(top)))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f23,f59325])).
% 203.02/26.12 fof(f59327,plain,(
% 203.02/26.12 ![X0]: (composition(converse(X0),zero)=complement(converse(top)))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f8802,f59326])).
% 203.02/26.12 fof(f59328,plain,(
% 203.02/26.12 ![X0]: (composition(converse(X0),zero)=complement(top))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f8562,f59327])).
% 203.02/26.12 fof(f59329,plain,(
% 203.02/26.12 ![X0]: (converse(composition(zero,X0))=zero)),
% 203.02/26.12 inference(backward_demodulation,[status(thm)],[f59330,f2515])).
% 203.02/26.12 fof(f59330,plain,(
% 203.02/26.12 ![X0]: (composition(converse(X0),zero)=zero)),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f62,f59328])).
% 203.02/26.12 fof(f59415,plain,(
% 203.02/26.12 ![X0,X1]: (zero=composition(join(converse(X0),X1),zero))),
% 203.02/26.12 inference(backward_demodulation,[status(thm)],[f59329,f8263])).
% 203.02/26.12 fof(f59436,plain,(
% 203.02/26.12 ![X0,X1]: (composition(join(converse(X0),X1),zero)=join(zero,composition(X1,zero)))),
% 203.02/26.12 inference(backward_demodulation,[status(thm)],[f59329,f8304])).
% 203.02/26.12 fof(f59533,plain,(
% 203.02/26.12 ![X0]: (zero=join(zero,composition(X0,zero)))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f59415,f59436])).
% 203.02/26.12 fof(f59918,plain,(
% 203.02/26.12 ![X0]: (zero=composition(X0,zero))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f1326,f59533])).
% 203.02/26.12 fof(f64388,plain,(
% 203.02/26.12 meet(composition(converse(sK0_skl),composition(sK0_skl,sK1_skl)),sF3_fnc)=meet(sF3_fnc,sK1_skl)),
% 203.02/26.12 inference(paramodulation,[status(thm)],[f51204,f23712])).
% 203.02/26.12 fof(f64476,plain,(
% 203.02/26.12 meet(sF3_fnc,composition(converse(sK0_skl),composition(sK0_skl,sK1_skl)))=meet(sF3_fnc,sK1_skl)),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f126,f64388])).
% 203.02/26.12 fof(f64477,plain,(
% 203.02/26.12 meet(sF3_fnc,composition(converse(sK0_skl),sF1_fnc))=meet(sF3_fnc,sK1_skl)),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f39,f64476])).
% 203.02/26.12 fof(f64478,plain,(
% 203.02/26.12 meet(sF3_fnc,composition(converse(sK0_skl),sF1_fnc))=meet(sK1_skl,sF3_fnc)),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f126,f64477])).
% 203.02/26.12 fof(f64479,plain,(
% 203.02/26.12 meet(sF3_fnc,composition(converse(sK0_skl),sF1_fnc))=zero),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f289,f64478])).
% 203.02/26.12 fof(f65080,plain,(
% 203.02/26.12 join(meet(sF2_fnc,sF1_fnc),meet(sF1_fnc,composition(sK0_skl,zero)))=meet(sF1_fnc,composition(sK0_skl,meet(sF3_fnc,composition(converse(sK0_skl),sF1_fnc))))),
% 203.02/26.12 inference(paramodulation,[status(thm)],[f64479,f698])).
% 203.02/26.12 fof(f65149,plain,(
% 203.02/26.12 join(meet(sF1_fnc,sF2_fnc),meet(composition(sK0_skl,zero),sF1_fnc))=meet(sF1_fnc,composition(sK0_skl,meet(sF3_fnc,composition(converse(sK0_skl),sF1_fnc))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f50267,f65080])).
% 203.02/26.12 fof(f65150,plain,(
% 203.02/26.12 join(meet(sF1_fnc,sF2_fnc),meet(sF1_fnc,composition(sK0_skl,zero)))=meet(sF1_fnc,composition(sK0_skl,meet(sF3_fnc,composition(converse(sK0_skl),sF1_fnc))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f41601,f65149])).
% 203.02/26.12 fof(f65151,plain,(
% 203.02/26.12 join(sF0_fnc,meet(sF1_fnc,composition(sK0_skl,zero)))=meet(sF1_fnc,composition(sK0_skl,meet(sF3_fnc,composition(converse(sK0_skl),sF1_fnc))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f42,f65150])).
% 203.02/26.12 fof(f65152,plain,(
% 203.02/26.12 join(sF0_fnc,meet(sF1_fnc,zero))=meet(sF1_fnc,composition(sK0_skl,meet(sF3_fnc,composition(converse(sK0_skl),sF1_fnc))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f59918,f65151])).
% 203.02/26.12 fof(f65153,plain,(
% 203.02/26.12 join(sF0_fnc,meet(zero,sF1_fnc))=meet(sF1_fnc,composition(sK0_skl,meet(sF3_fnc,composition(converse(sK0_skl),sF1_fnc))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f41601,f65152])).
% 203.02/26.12 fof(f65154,plain,(
% 203.02/26.12 join(sF0_fnc,zero)=meet(sF1_fnc,composition(sK0_skl,meet(sF3_fnc,composition(converse(sK0_skl),sF1_fnc))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f628,f65153])).
% 203.02/26.12 fof(f65155,plain,(
% 203.02/26.12 sF0_fnc=meet(sF1_fnc,composition(sK0_skl,meet(sF3_fnc,composition(converse(sK0_skl),sF1_fnc))))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f1557,f65154])).
% 203.02/26.12 fof(f65156,plain,(
% 203.02/26.12 sF0_fnc=meet(sF1_fnc,composition(sK0_skl,zero))),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f64479,f65155])).
% 203.02/26.12 fof(f65157,plain,(
% 203.02/26.12 sF0_fnc=meet(sF1_fnc,zero)),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f59918,f65156])).
% 203.02/26.12 fof(f65158,plain,(
% 203.02/26.12 sF0_fnc=meet(zero,sF1_fnc)),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f126,f65157])).
% 203.02/26.12 fof(f65159,plain,(
% 203.02/26.12 sF0_fnc=zero),
% 203.02/26.12 inference(forward_demodulation,[status(thm)],[f628,f65158])).
% 203.02/26.12 fof(f65160,plain,(
% 138.49/26.35 $false),
% 138.49/26.35 inference(forward_subsumption_resolution,[status(thm)],[f65159,f43])).
% 138.49/26.35 % SZS output end CNFRefutation for theBenchmark.p
% 129.85/26.44 % Elapsed time: 25.967226 seconds
% 129.85/26.44 % CPU time: 205.187395 seconds
% 129.85/26.44 % Total memory used: 1.223 GB
% 129.85/26.44 % Net memory used: 1.203 GB
%------------------------------------------------------------------------------