%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL034+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 : n001.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:42 PM UTC 2026
% Result : Theorem 226.41s 29.14s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL034+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.44 % Computer : n001.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Mon Sep 21 04:10:58 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.46 % Drodi V4.1.1
% 226.41/29.14 % Refutation found
% 226.41/29.14 % SZS status Theorem for theBenchmark: Theorem is valid
% 226.41/29.14 % SZS output start CNFRefutation for theBenchmark
% 226.41/29.14 fof(f1,axiom,(
% 226.41/29.14 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 226.41/29.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 226.41/29.14 fof(f2,axiom,(
% 226.41/29.14 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 226.41/29.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 226.41/29.14 fof(f3,axiom,(
% 226.41/29.14 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 226.41/29.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 226.41/29.14 fof(f4,axiom,(
% 226.41/29.14 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 226.41/29.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 226.41/29.14 fof(f5,axiom,(
% 226.41/29.14 (! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2) )),
% 226.41/29.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 226.41/29.14 fof(f6,axiom,(
% 226.41/29.14 (! [X0] : composition(X0,one) = X0 )),
% 226.41/29.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 226.41/29.14 fof(f7,axiom,(
% 226.41/29.14 (! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) )),
% 226.41/29.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 226.41/29.14 fof(f8,axiom,(
% 226.41/29.14 (! [X0] : converse(converse(X0)) = X0 )),
% 226.41/29.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 226.41/29.14 fof(f9,axiom,(
% 226.41/29.14 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 226.41/29.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 226.41/29.14 fof(f10,axiom,(
% 226.41/29.14 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 226.41/29.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 226.41/29.14 fof(f11,axiom,(
% 226.41/29.14 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 226.41/29.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 226.41/29.14 fof(f12,axiom,(
% 226.41/29.14 (! [X0] : top = join(X0,complement(X0)) )),
% 226.41/29.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 226.41/29.14 fof(f13,axiom,(
% 226.41/29.14 (! [X0] : zero = meet(X0,complement(X0)) )),
% 226.41/29.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 226.41/29.14 fof(f15,axiom,(
% 226.41/29.14 (! [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) )),
% 226.41/29.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 226.41/29.14 fof(f16,axiom,(
% 226.41/29.14 (! [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) )),
% 226.41/29.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 226.41/29.14 fof(f17,conjecture,(
% 226.41/29.14 (! [X0,X1,X2] :( composition(X0,top) = X0=> join(composition(X1,meet(X0,X2)),composition(meet(X1,converse(X0)),meet(X0,X2))) = composition(meet(X1,converse(X0)),meet(X0,X2)) ) )),
% 226.41/29.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 226.41/29.14 fof(f18,negated_conjecture,(
% 226.41/29.14 ~((! [X0,X1,X2] :( composition(X0,top) = X0=> join(composition(X1,meet(X0,X2)),composition(meet(X1,converse(X0)),meet(X0,X2))) = composition(meet(X1,converse(X0)),meet(X0,X2)) ) ))),
% 226.41/29.14 inference(negated_conjecture,[status(cth)],[f17])).
% 226.41/29.14 fof(f19,plain,(
% 226.41/29.14 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 226.41/29.14 inference(cnf_transformation,[status(thm)],[f1])).
% 226.41/29.14 fof(f20,plain,(
% 226.41/29.14 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 226.41/29.14 inference(cnf_transformation,[status(thm)],[f2])).
% 226.41/29.14 fof(f21,plain,(
% 226.41/29.14 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 226.41/29.14 inference(cnf_transformation,[status(thm)],[f3])).
% 226.41/29.14 fof(f22,plain,(
% 226.41/29.14 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 226.41/29.14 inference(cnf_transformation,[status(thm)],[f4])).
% 226.41/29.14 fof(f23,plain,(
% 226.41/29.14 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 226.41/29.14 inference(cnf_transformation,[status(thm)],[f5])).
% 226.41/29.14 fof(f24,plain,(
% 226.41/29.14 ![X0]: (composition(X0,one)=X0)),
% 226.41/29.14 inference(cnf_transformation,[status(thm)],[f6])).
% 226.41/29.14 fof(f25,plain,(
% 226.41/29.14 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 226.41/29.14 inference(cnf_transformation,[status(thm)],[f7])).
% 226.41/29.14 fof(f26,plain,(
% 226.41/29.14 ![X0]: (converse(converse(X0))=X0)),
% 226.41/29.14 inference(cnf_transformation,[status(thm)],[f8])).
% 226.41/29.14 fof(f27,plain,(
% 226.41/29.14 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 226.41/29.14 inference(cnf_transformation,[status(thm)],[f9])).
% 226.41/29.14 fof(f28,plain,(
% 226.41/29.14 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 226.41/29.14 inference(cnf_transformation,[status(thm)],[f10])).
% 226.41/29.14 fof(f29,plain,(
% 226.41/29.14 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 226.41/29.14 inference(cnf_transformation,[status(thm)],[f11])).
% 226.41/29.14 fof(f30,plain,(
% 226.41/29.14 ![X0]: (top=join(X0,complement(X0)))),
% 226.41/29.14 inference(cnf_transformation,[status(thm)],[f12])).
% 226.41/29.14 fof(f31,plain,(
% 226.41/29.14 ![X0]: (zero=meet(X0,complement(X0)))),
% 226.41/29.14 inference(cnf_transformation,[status(thm)],[f13])).
% 226.41/29.14 fof(f33,plain,(
% 226.41/29.14 ![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))),
% 226.41/29.14 inference(cnf_transformation,[status(thm)],[f15])).
% 226.41/29.14 fof(f34,plain,(
% 226.41/29.14 ![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))),
% 226.41/29.14 inference(cnf_transformation,[status(thm)],[f16])).
% 226.41/29.14 fof(f35,plain,(
% 226.41/29.14 (?[X0,X1,X2]: (composition(X0,top)=X0&~join(composition(X1,meet(X0,X2)),composition(meet(X1,converse(X0)),meet(X0,X2)))=composition(meet(X1,converse(X0)),meet(X0,X2))))),
% 226.41/29.14 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 226.41/29.14 fof(f36,plain,(
% 226.41/29.14 ?[X0]: (composition(X0,top)=X0&(?[X1,X2]: ~join(composition(X1,meet(X0,X2)),composition(meet(X1,converse(X0)),meet(X0,X2)))=composition(meet(X1,converse(X0)),meet(X0,X2))))),
% 226.41/29.14 inference(miniscoping,[status(thm)],[f35])).
% 226.41/29.14 fof(f37,plain,(
% 226.41/29.14 (composition(sK0_skl,top)=sK0_skl&~join(composition(sK1_skl,meet(sK0_skl,sK2_skl)),composition(meet(sK1_skl,converse(sK0_skl)),meet(sK0_skl,sK2_skl)))=composition(meet(sK1_skl,converse(sK0_skl)),meet(sK0_skl,sK2_skl)))),
% 226.41/29.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl),skolemize(X2,sK2_skl)],[f36])).
% 226.41/29.14 fof(f38,plain,(
% 226.41/29.14 composition(sK0_skl,top)=sK0_skl),
% 226.41/29.14 inference(cnf_transformation,[status(thm)],[f37])).
% 226.41/29.14 fof(f39,plain,(
% 226.41/29.14 ~join(composition(sK1_skl,meet(sK0_skl,sK2_skl)),composition(meet(sK1_skl,converse(sK0_skl)),meet(sK0_skl,sK2_skl)))=composition(meet(sK1_skl,converse(sK0_skl)),meet(sK0_skl,sK2_skl))),
% 226.41/29.14 inference(cnf_transformation,[status(thm)],[f37])).
% 226.41/29.14 fof(f40,definition,(
% 226.41/29.14 sF2_fnc=meet(sK0_skl,sK2_skl)),
% 226.41/29.14 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 226.41/29.14 fof(f41,definition,(
% 226.41/29.14 sF1_fnc=composition(sK1_skl,sF2_fnc)),
% 226.41/29.14 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 226.41/29.14 fof(f42,definition,(
% 226.41/29.14 sF5_fnc=converse(sK0_skl)),
% 226.41/29.14 introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition])).
% 226.41/29.14 fof(f43,definition,(
% 226.41/29.14 sF4_fnc=meet(sK1_skl,sF5_fnc)),
% 226.41/29.14 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 226.41/29.14 fof(f44,definition,(
% 226.41/29.14 sF3_fnc=composition(sF4_fnc,sF2_fnc)),
% 226.41/29.14 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 226.41/29.14 fof(f45,definition,(
% 226.41/29.14 sF0_fnc=join(sF1_fnc,sF3_fnc)),
% 226.41/29.14 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 226.41/29.14 fof(f46,definition,(
% 226.41/29.14 sF7_fnc=meet(sK1_skl,sF5_fnc)),
% 226.41/29.14 introduced(definition,[new_symbols(definition,[sF7_fnc])],[function_definition])).
% 226.41/29.14 fof(f47,definition,(
% 226.41/29.14 sF6_fnc=composition(sF7_fnc,sF2_fnc)),
% 226.41/29.14 introduced(definition,[new_symbols(definition,[sF6_fnc])],[function_definition])).
% 226.41/29.14 fof(f48,plain,(
% 226.41/29.14 ~sF0_fnc=sF6_fnc),
% 226.41/29.14 inference(definition_folding,[],[f39,f47,f46,f45,f44,f43,f42,f41,f40])).
% 226.41/29.14 fof(f49,plain,(
% 226.41/29.14 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f19,f21])).
% 226.41/29.14 fof(f50,plain,(
% 226.41/29.14 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 226.41/29.14 inference(backward_demodulation,[status(thm)],[f22,f49])).
% 226.41/29.14 fof(f51,plain,(
% 226.41/29.14 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f19,f29])).
% 226.41/29.14 fof(f52,plain,(
% 226.41/29.14 sF7_fnc=sF4_fnc),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f43,f46])).
% 226.41/29.14 fof(f53,plain,(
% 226.41/29.14 sF6_fnc=composition(sF4_fnc,sF2_fnc)),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f52,f47])).
% 226.41/29.14 fof(f54,plain,(
% 226.41/29.14 sF6_fnc=sF3_fnc),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f44,f53])).
% 226.41/29.14 fof(f55,plain,(
% 226.41/29.14 ~sF0_fnc=sF3_fnc),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f54,f48])).
% 226.41/29.14 fof(f56,plain,(
% 226.41/29.14 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f19,f50])).
% 226.41/29.14 fof(f65,plain,(
% 226.41/29.14 ![X0]: (composition(sF4_fnc,composition(sF2_fnc,X0))=composition(sF3_fnc,X0))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f44,f23])).
% 226.41/29.14 fof(f66,plain,(
% 226.41/29.14 ![X0]: (composition(sK1_skl,composition(sF2_fnc,X0))=composition(sF1_fnc,X0))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f41,f23])).
% 226.41/29.14 fof(f73,plain,(
% 226.41/29.14 ![X0,X1]: (join(X0,join(X1,complement(join(X0,X1))))=top)),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f30,f20])).
% 226.41/29.14 fof(f74,plain,(
% 226.41/29.14 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f19,f20])).
% 226.41/29.14 fof(f78,plain,(
% 226.41/29.14 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f30,f20])).
% 226.41/29.14 fof(f79,plain,(
% 226.41/29.14 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X0),X2))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f19,f20])).
% 226.41/29.14 fof(f86,plain,(
% 226.41/29.14 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X1,X2),composition(X0,X2)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f19,f25])).
% 226.41/29.14 fof(f89,plain,(
% 226.41/29.14 ![X0,X1]: (composition(join(sF4_fnc,X0),composition(sF2_fnc,X1))=join(composition(sF3_fnc,X1),composition(X0,composition(sF2_fnc,X1))))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f65,f25])).
% 226.41/29.14 fof(f91,plain,(
% 226.41/29.14 ![X0]: (composition(join(sK1_skl,X0),sF2_fnc)=join(sF1_fnc,composition(X0,sF2_fnc)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f41,f25])).
% 226.41/29.14 fof(f92,plain,(
% 226.41/29.14 ![X0]: (composition(join(sK0_skl,X0),top)=join(sK0_skl,composition(X0,top)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f38,f25])).
% 226.41/29.14 fof(f93,plain,(
% 226.41/29.14 ![X0,X1,X2,X3]: (composition(join(X0,composition(X1,X2)),X3)=join(composition(X0,X3),composition(X1,composition(X2,X3))))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f23,f25])).
% 226.41/29.14 fof(f101,plain,(
% 226.41/29.14 ![X0,X1]: (composition(join(sF4_fnc,X0),composition(sF2_fnc,X1))=composition(join(sF3_fnc,composition(X0,sF2_fnc)),X1))),
% 226.41/29.14 inference(backward_demodulation,[status(thm)],[f93,f89])).
% 226.41/29.14 fof(f112,plain,(
% 226.41/29.14 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f24,f23])).
% 226.41/29.14 fof(f133,plain,(
% 226.41/29.14 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f30,f22])).
% 226.41/29.14 fof(f134,plain,(
% 226.41/29.14 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f19,f22])).
% 226.41/29.14 fof(f136,plain,(
% 226.41/29.14 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X0,X1),complement(X2))))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f22,f22])).
% 226.41/29.14 fof(f140,plain,(
% 226.41/29.14 zero=complement(top)),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f31,f133])).
% 226.41/29.14 fof(f185,plain,(
% 226.41/29.14 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f26,f28])).
% 226.41/29.14 fof(f186,plain,(
% 226.41/29.14 ![X0]: (converse(composition(sK0_skl,X0))=composition(converse(X0),sF5_fnc))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f42,f28])).
% 226.41/29.14 fof(f188,plain,(
% 226.41/29.14 ![X0,X1,X2]: (composition(join(converse(X0),X1),converse(X2))=join(converse(composition(X2,X0)),composition(X1,converse(X2))))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f28,f25])).
% 226.41/29.14 fof(f196,plain,(
% 226.41/29.14 ![X0,X1]: (converse(join(X0,converse(X1)))=join(converse(X0),X1))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f26,f27])).
% 226.41/29.14 fof(f237,plain,(
% 226.41/29.14 ![X0,X1]: (join(complement(converse(X0)),composition(converse(converse(X1)),complement(converse(composition(X0,X1)))))=complement(converse(X0)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f28,f51])).
% 226.41/29.14 fof(f244,plain,(
% 226.41/29.14 join(complement(top),composition(converse(sK0_skl),complement(sK0_skl)))=complement(top)),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f38,f51])).
% 226.41/29.14 fof(f246,plain,(
% 226.41/29.14 ![X0]: (join(complement(one),composition(converse(X0),complement(X0)))=complement(one))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f24,f51])).
% 226.41/29.14 fof(f252,plain,(
% 226.41/29.14 ![X0,X1]: (join(complement(converse(X0)),composition(X1,complement(converse(composition(X0,X1)))))=complement(converse(X0)))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f26,f237])).
% 226.41/29.14 fof(f254,plain,(
% 226.41/29.14 join(zero,composition(converse(sK0_skl),complement(sK0_skl)))=complement(top)),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f140,f244])).
% 226.41/29.14 fof(f255,plain,(
% 226.41/29.14 join(zero,composition(sF5_fnc,complement(sK0_skl)))=complement(top)),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f42,f254])).
% 226.41/29.14 fof(f256,plain,(
% 226.41/29.14 join(zero,composition(sF5_fnc,complement(sK0_skl)))=zero),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f140,f255])).
% 226.41/29.14 fof(f318,plain,(
% 226.41/29.14 ![X0,X1,X2]: (join(meet(composition(X0,X1),converse(X2)),meet(composition(X0,meet(X1,converse(composition(X2,X0)))),converse(X2)))=meet(composition(X0,meet(X1,composition(converse(X0),converse(X2)))),converse(X2)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f28,f33])).
% 226.41/29.14 fof(f322,plain,(
% 226.41/29.14 ![X0,X1,X2]: (join(meet(composition(converse(X0),X1),X2),meet(composition(converse(X0),meet(X1,composition(X0,X2))),X2))=meet(composition(converse(X0),meet(X1,composition(converse(converse(X0)),X2))),X2))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f26,f33])).
% 226.41/29.14 fof(f324,plain,(
% 226.41/29.14 ![X0,X1,X2,X3]: (join(meet(composition(X0,X1),X2),join(meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2),X3))=join(meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2),X3))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f33,f20])).
% 226.41/29.14 fof(f335,plain,(
% 226.41/29.14 ![X0,X1,X2]: (join(meet(composition(X0,X1),converse(X2)),meet(composition(X0,meet(X1,converse(composition(X2,X0)))),converse(X2)))=meet(composition(X0,meet(X1,converse(composition(X2,X0)))),converse(X2)))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f28,f318])).
% 226.41/29.14 fof(f339,plain,(
% 226.41/29.14 ![X0,X1,X2]: (join(meet(composition(converse(X0),X1),X2),meet(composition(converse(X0),meet(X1,composition(X0,X2))),X2))=meet(composition(converse(X0),meet(X1,composition(X0,X2))),X2))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f26,f322])).
% 226.41/29.14 fof(f592,plain,(
% 226.41/29.14 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f22,f134])).
% 226.41/29.14 fof(f626,plain,(
% 226.41/29.14 ![X0,X1,X2]: (join(meet(composition(converse(X0),X1),X2),meet(composition(converse(X0),meet(X1,composition(X0,X2))),X2))=meet(X2,composition(converse(X0),meet(X1,composition(X0,X2)))))),
% 226.41/29.14 inference(backward_demodulation,[status(thm)],[f592,f339])).
% 226.41/29.14 fof(f634,plain,(
% 226.41/29.14 ![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)))),
% 226.41/29.14 inference(backward_demodulation,[status(thm)],[f592,f34])).
% 226.41/29.14 fof(f637,plain,(
% 226.41/29.14 ![X0,X1,X2]: (join(meet(composition(X0,X1),converse(X2)),meet(composition(X0,meet(X1,converse(composition(X2,X0)))),converse(X2)))=meet(converse(X2),composition(X0,meet(X1,converse(composition(X2,X0))))))),
% 226.41/29.14 inference(backward_demodulation,[status(thm)],[f592,f335])).
% 226.41/29.14 fof(f641,plain,(
% 226.41/29.14 ![X0,X1,X2,X3]: (join(meet(composition(X0,X1),X2),join(meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2),X3))=join(meet(X2,composition(X0,meet(X1,composition(converse(X0),X2)))),X3))),
% 226.41/29.14 inference(backward_demodulation,[status(thm)],[f592,f324])).
% 226.41/29.14 fof(f671,plain,(
% 226.41/29.14 ![X0,X1,X2]: (join(meet(composition(converse(X0),X1),X2),meet(X2,composition(converse(X0),meet(X1,composition(X0,X2)))))=meet(X2,composition(converse(X0),meet(X1,composition(X0,X2)))))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f592,f626])).
% 226.41/29.14 fof(f679,plain,(
% 226.41/29.14 ![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)))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f592,f634])).
% 226.41/29.14 fof(f682,plain,(
% 226.41/29.14 ![X0,X1,X2]: (join(meet(composition(X0,X1),converse(X2)),meet(converse(X2),composition(X0,meet(X1,converse(composition(X2,X0))))))=meet(converse(X2),composition(X0,meet(X1,converse(composition(X2,X0))))))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f592,f637])).
% 226.41/29.14 fof(f687,plain,(
% 226.41/29.14 ![X0,X1,X2,X3]: (join(meet(composition(X0,X1),X2),join(meet(X2,composition(X0,meet(X1,composition(converse(X0),X2)))),X3))=join(meet(X2,composition(X0,meet(X1,composition(converse(X0),X2)))),X3))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f592,f641])).
% 226.41/29.14 fof(f707,plain,(
% 226.41/29.14 converse(sK0_skl)=composition(converse(top),sF5_fnc)),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f38,f186])).
% 226.41/29.14 fof(f726,plain,(
% 226.41/29.14 sF5_fnc=composition(converse(top),sF5_fnc)),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f42,f707])).
% 226.41/29.14 fof(f751,plain,(
% 226.41/29.14 ![X0]: (composition(converse(top),composition(sF5_fnc,X0))=composition(sF5_fnc,X0))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f726,f23])).
% 226.41/29.14 fof(f765,plain,(
% 226.41/29.14 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f31,f56])).
% 226.41/29.14 fof(f768,plain,(
% 226.41/29.14 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f134,f56])).
% 226.41/29.14 fof(f769,plain,(
% 226.41/29.14 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f22,f56])).
% 226.41/29.14 fof(f771,plain,(
% 226.41/29.14 ![X0,X1]: (X0=join(meet(X0,join(complement(complement(X0)),X1)),complement(join(top,X1))))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f78,f56])).
% 226.41/29.14 fof(f772,plain,(
% 226.41/29.14 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f30,f56])).
% 226.41/29.14 fof(f786,plain,(
% 226.41/29.14 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f134,f765])).
% 226.41/29.14 fof(f787,plain,(
% 226.41/29.14 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f19,f768])).
% 226.41/29.14 fof(f788,plain,(
% 226.41/29.14 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f19,f769])).
% 226.41/29.14 fof(f790,plain,(
% 226.41/29.14 ![X0,X1]: (X0=join(complement(join(top,X1)),meet(X0,join(complement(complement(X0)),X1))))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f19,f771])).
% 226.41/29.14 fof(f791,plain,(
% 226.41/29.14 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(X0)))))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f19,f772])).
% 226.41/29.14 fof(f792,plain,(
% 226.41/29.14 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f140,f791])).
% 226.41/29.14 fof(f917,plain,(
% 226.41/29.14 top=join(zero,meet(top,complement(zero)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f140,f792])).
% 226.41/29.14 fof(f937,plain,(
% 226.41/29.14 ![X0,X1]: (X0=join(meet(X1,X0),meet(complement(X1),X0)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f592,f787])).
% 226.41/29.14 fof(f939,plain,(
% 226.41/29.14 ![X0]: (X0=join(meet(top,X0),meet(X0,zero)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f140,f787])).
% 226.41/29.14 fof(f957,plain,(
% 226.41/29.14 ![X0]: (X0=join(meet(X0,top),meet(X0,zero)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f592,f939])).
% 226.41/29.14 fof(f994,plain,(
% 226.41/29.14 ![X0]: (X0=join(meet(X0,top),meet(zero,X0)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f592,f957])).
% 226.41/29.14 fof(f1004,plain,(
% 226.41/29.14 complement(zero)=join(meet(complement(zero),top),zero)),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f31,f994])).
% 226.41/29.14 fof(f1011,plain,(
% 226.41/29.14 complement(zero)=join(zero,meet(complement(zero),top))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f19,f1004])).
% 226.41/29.14 fof(f1012,plain,(
% 226.41/29.14 complement(zero)=join(zero,meet(top,complement(zero)))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f592,f1011])).
% 226.41/29.14 fof(f1016,plain,(
% 226.41/29.14 complement(zero)=top),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f917,f1012])).
% 226.41/29.14 fof(f1019,plain,(
% 226.41/29.14 ![X0]: (zero=join(meet(zero,X0),complement(join(top,X0))))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f1016,f56])).
% 226.41/29.14 fof(f1080,plain,(
% 226.41/29.14 sK1_skl=join(sF4_fnc,meet(sK1_skl,complement(sF5_fnc)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f43,f788])).
% 226.41/29.14 fof(f1081,plain,(
% 226.41/29.14 sK0_skl=join(sF2_fnc,meet(sK0_skl,complement(sK2_skl)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f40,f788])).
% 226.41/29.14 fof(f1086,plain,(
% 226.41/29.14 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f592,f788])).
% 226.41/29.14 fof(f1112,plain,(
% 226.41/29.14 ![X0]: (complement(complement(X0))=join(meet(X0,complement(complement(X0))),zero))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f31,f937])).
% 226.41/29.14 fof(f1127,plain,(
% 226.41/29.14 ![X0]: (complement(complement(X0))=join(zero,meet(X0,complement(complement(X0)))))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f19,f1112])).
% 226.41/29.14 fof(f1133,plain,(
% 226.41/29.14 ![X0,X1]: (X0=join(complement(join(top,X1)),meet(X0,join(X0,X1))))),
% 226.41/29.14 inference(backward_demodulation,[status(thm)],[f1137,f790])).
% 226.41/29.14 fof(f1137,plain,(
% 226.41/29.14 ![X0]: (complement(complement(X0))=X0)),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f792,f1127])).
% 226.41/29.14 fof(f1150,plain,(
% 226.41/29.14 ![X0,X1]: (complement(meet(X0,X1))=join(complement(X1),complement(X0)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f134,f1137])).
% 226.41/29.14 fof(f1151,plain,(
% 226.41/29.14 ![X0,X1]: (complement(meet(X0,X1))=join(complement(X0),complement(X1)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f22,f1137])).
% 226.41/29.14 fof(f1157,plain,(
% 226.41/29.14 ![X0,X1]: (meet(X0,complement(X1))=complement(join(X1,complement(X0))))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f1137,f134])).
% 226.41/29.14 fof(f1163,plain,(
% 226.41/29.14 ![X0,X1]: (meet(complement(X0),X1)=complement(join(X0,complement(X1))))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f1137,f22])).
% 226.41/29.14 fof(f1183,plain,(
% 226.41/29.14 ![X0,X1,X2]: (meet(complement(meet(X0,X1)),X2)=complement(join(meet(X1,X0),complement(X2))))),
% 226.41/29.14 inference(backward_demodulation,[status(thm)],[f1150,f136])).
% 226.41/29.14 fof(f1225,plain,(
% 226.41/29.14 ![X0,X1,X2]: (meet(complement(meet(X0,X1)),X2)=meet(complement(meet(X1,X0)),X2))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f1163,f1183])).
% 226.41/29.14 fof(f1262,plain,(
% 226.41/29.14 ![X0,X1,X2]: (join(meet(composition(X0,converse(X1)),X2),meet(X2,composition(meet(X0,composition(X2,X1)),converse(X1))))=meet(X2,composition(meet(X0,composition(X2,converse(converse(X1)))),converse(X1))))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f26,f679])).
% 226.41/29.14 fof(f1290,plain,(
% 226.41/29.14 ![X0,X1,X2]: (join(meet(composition(X0,converse(X1)),X2),meet(X2,composition(meet(X0,composition(X2,X1)),converse(X1))))=meet(X2,composition(meet(X0,composition(X2,X1)),converse(X1))))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f26,f1262])).
% 226.41/29.14 fof(f1556,plain,(
% 226.41/29.14 ![X0]: (join(zero,join(composition(sF5_fnc,complement(sK0_skl)),X0))=join(X0,zero))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f256,f74])).
% 226.41/29.14 fof(f2089,plain,(
% 226.41/29.14 ![X0,X1,X2]: (composition(join(X0,X1),X2)=composition(join(X1,X0),X2))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f25,f86])).
% 226.41/29.14 fof(f2204,plain,(
% 226.41/29.14 ![X0,X1]: (complement(meet(X0,complement(X1)))=join(X1,complement(X0)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f1137,f1150])).
% 226.41/29.14 fof(f2213,plain,(
% 226.41/29.14 ![X0,X1]: (join(X0,complement(meet(X1,X0)))=join(top,complement(X1)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f1150,f78])).
% 226.41/29.14 fof(f2367,plain,(
% 226.41/29.14 ![X0,X1]: (meet(complement(X0),complement(X1))=complement(join(X1,X0)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f1137,f1157])).
% 226.41/29.14 fof(f2368,plain,(
% 226.41/29.14 ![X0]: (meet(zero,complement(X0))=complement(join(X0,top)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f1016,f1157])).
% 226.41/29.14 fof(f2469,plain,(
% 226.41/29.14 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f24,f185])).
% 226.41/29.14 fof(f2518,plain,(
% 226.41/29.14 ![X0]: (X0=composition(converse(one),X0))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f26,f2469])).
% 226.41/29.14 fof(f2566,plain,(
% 226.41/29.14 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f112,f2518])).
% 226.41/29.14 fof(f2567,plain,(
% 226.41/29.14 one=converse(one)),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f24,f2518])).
% 226.41/29.14 fof(f2568,plain,(
% 226.41/29.14 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f2518,f51])).
% 226.41/29.14 fof(f2582,plain,(
% 226.41/29.14 ![X0,X1]: (composition(join(X0,converse(one)),X1)=join(X1,composition(X0,X1)))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f2518,f86])).
% 226.41/29.14 fof(f2609,plain,(
% 226.41/29.14 ![X0]: (composition(one,X0)=X0)),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f2518,f2566])).
% 226.41/29.14 fof(f2619,plain,(
% 226.41/29.14 ![X0]: (complement(meet(X0,composition(one,X0)))=complement(X0))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f1151,f2568])).
% 226.41/29.14 fof(f2620,plain,(
% 226.41/29.14 ![X0]: (complement(meet(X0,X0))=complement(X0))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f2609,f2619])).
% 226.41/29.14 fof(f2657,plain,(
% 226.41/29.14 ![X0,X1]: (composition(join(X0,one),X1)=join(X1,composition(X0,X1)))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f2567,f2582])).
% 226.41/29.14 fof(f2823,plain,(
% 226.41/29.14 ![X0]: (complement(complement(X0))=meet(X0,X0))),
% 226.41/29.14 inference(paramodulation,[status(thm)],[f2620,f1137])).
% 226.41/29.14 fof(f2871,plain,(
% 226.41/29.14 ![X0]: (X0=join(zero,X0))),
% 226.41/29.14 inference(backward_demodulation,[status(thm)],[f2883,f786])).
% 226.41/29.14 fof(f2883,plain,(
% 226.41/29.14 ![X0]: (X0=meet(X0,X0))),
% 226.41/29.14 inference(forward_demodulation,[status(thm)],[f1137,f2823])).
% 226.41/29.14 fof(f2936,plain,(
% 226.41/29.14 composition(sF5_fnc,complement(sK0_skl))=zero),
% 226.41/29.16 inference(backward_demodulation,[status(thm)],[f2871,f256])).
% 226.41/29.16 fof(f2942,plain,(
% 226.41/29.16 ![X0]: (join(composition(sF5_fnc,complement(sK0_skl)),X0)=join(X0,zero))),
% 226.41/29.16 inference(backward_demodulation,[status(thm)],[f2871,f1556])).
% 226.41/29.16 fof(f2988,plain,(
% 226.41/29.16 ![X0]: (join(zero,X0)=join(X0,zero))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2936,f2942])).
% 226.41/29.16 fof(f2994,plain,(
% 226.41/29.16 ![X0]: (X0=join(X0,zero))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2871,f2988])).
% 226.41/29.16 fof(f3144,plain,(
% 226.41/29.16 ![X0]: (converse(converse(X0))=join(converse(zero),X0))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f2871,f196])).
% 226.41/29.16 fof(f3153,plain,(
% 226.41/29.16 ![X0]: (meet(X0,complement(zero))=complement(complement(X0)))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f2871,f1157])).
% 226.41/29.16 fof(f3167,plain,(
% 226.41/29.16 ![X0]: (X0=join(converse(zero),X0))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f26,f3144])).
% 226.41/29.16 fof(f3174,plain,(
% 226.41/29.16 ![X0]: (meet(X0,top)=complement(complement(X0)))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f1016,f3153])).
% 226.41/29.16 fof(f3177,plain,(
% 226.41/29.16 ![X0]: (X0=join(X0,meet(X0,zero)))),
% 226.41/29.16 inference(backward_demodulation,[status(thm)],[f3201,f957])).
% 226.41/29.16 fof(f3201,plain,(
% 226.41/29.16 ![X0]: (meet(X0,top)=X0)),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f1137,f3174])).
% 226.41/29.16 fof(f3220,plain,(
% 226.41/29.16 ![X0]: (meet(top,X0)=X0)),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f592,f3201])).
% 226.41/29.16 fof(f3742,plain,(
% 226.41/29.16 zero=converse(zero)),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f2994,f3167])).
% 226.41/29.16 fof(f3857,plain,(
% 226.41/29.16 ![X0]: (join(X0,complement(X0))=join(top,meet(complement(X0),zero)))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f3177,f78])).
% 226.41/29.16 fof(f3876,plain,(
% 226.41/29.16 ![X0]: (top=join(top,meet(complement(X0),zero)))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f30,f3857])).
% 226.41/29.16 fof(f3877,plain,(
% 226.41/29.16 ![X0]: (top=join(top,meet(zero,complement(X0))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f592,f3876])).
% 226.41/29.16 fof(f3878,plain,(
% 226.41/29.16 ![X0]: (top=join(top,complement(join(X0,top))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2368,f3877])).
% 226.41/29.16 fof(f4213,plain,(
% 226.41/29.16 ![X0]: (join(X0,top)=top)),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f3878,f73])).
% 226.41/29.16 fof(f4217,plain,(
% 226.41/29.16 ![X0,X1]: (join(top,join(complement(join(X0,top)),X1))=join(X1,top))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f3878,f74])).
% 226.41/29.16 fof(f4245,plain,(
% 226.41/29.16 ![X0]: (join(top,join(complement(top),X0))=join(X0,top))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f4213,f4217])).
% 226.41/29.16 fof(f4246,plain,(
% 226.41/29.16 ![X0]: (join(top,X0)=join(X0,top))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f78,f4245])).
% 226.41/29.16 fof(f4258,plain,(
% 226.41/29.16 ![X0,X1]: (join(X0,complement(meet(X1,X0)))=top)),
% 226.41/29.16 inference(backward_demodulation,[status(thm)],[f4309,f2213])).
% 226.41/29.16 fof(f4305,plain,(
% 226.41/29.16 ![X0,X1]: (X0=join(complement(top),meet(X0,join(X0,X1))))),
% 226.41/29.16 inference(backward_demodulation,[status(thm)],[f4309,f1133])).
% 226.41/29.16 fof(f4306,plain,(
% 226.41/29.16 ![X0]: (zero=join(meet(zero,X0),complement(top)))),
% 226.41/29.16 inference(backward_demodulation,[status(thm)],[f4309,f1019])).
% 226.41/29.16 fof(f4309,plain,(
% 226.41/29.16 ![X0]: (join(top,X0)=top)),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f4213,f4246])).
% 226.41/29.16 fof(f4323,plain,(
% 226.41/29.16 ![X0,X1]: (X0=join(zero,meet(X0,join(X0,X1))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f140,f4305])).
% 226.41/29.16 fof(f4324,plain,(
% 226.41/29.16 ![X0,X1]: (X0=meet(X0,join(X0,X1)))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2871,f4323])).
% 226.41/29.16 fof(f4325,plain,(
% 226.41/29.16 ![X0]: (zero=join(complement(top),meet(zero,X0)))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f19,f4306])).
% 226.41/29.16 fof(f4326,plain,(
% 226.41/29.16 ![X0]: (zero=join(zero,meet(zero,X0)))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f140,f4325])).
% 226.41/29.16 fof(f4350,plain,(
% 226.41/29.16 ![X0]: (zero=meet(zero,X0))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2871,f4326])).
% 226.41/29.16 fof(f4397,plain,(
% 226.41/29.16 ![X0]: (zero=meet(X0,zero))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f592,f4350])).
% 226.41/29.16 fof(f4506,plain,(
% 226.41/29.16 ![X0]: (converse(top)=join(converse(top),X0))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f4309,f196])).
% 226.41/29.16 fof(f5294,plain,(
% 226.41/29.16 sF4_fnc=meet(sF4_fnc,sK1_skl)),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f1080,f4324])).
% 226.41/29.16 fof(f5296,plain,(
% 226.41/29.16 sF2_fnc=meet(sF2_fnc,sK0_skl)),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f1081,f4324])).
% 226.41/29.16 fof(f5304,plain,(
% 226.41/29.16 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X0))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f1086,f4324])).
% 226.41/29.16 fof(f5305,plain,(
% 226.41/29.16 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X1))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f937,f4324])).
% 226.41/29.16 fof(f5308,plain,(
% 226.41/29.16 ![X0,X1]: (complement(X0)=meet(complement(X0),complement(meet(X0,X1))))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f1151,f4324])).
% 226.41/29.16 fof(f5332,plain,(
% 226.41/29.16 ![X0,X1]: (X0=meet(X0,join(X1,X0)))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f19,f4324])).
% 226.41/29.16 fof(f5345,plain,(
% 226.41/29.16 sF4_fnc=meet(sK1_skl,sF4_fnc)),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f592,f5294])).
% 226.41/29.16 fof(f5346,plain,(
% 226.41/29.16 sF2_fnc=meet(sK0_skl,sF2_fnc)),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f592,f5296])).
% 226.41/29.16 fof(f5348,plain,(
% 226.41/29.16 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X0,X1)))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f592,f5304])).
% 226.41/29.16 fof(f5352,plain,(
% 226.41/29.16 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X0,X1)))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f592,f5305])).
% 226.41/29.16 fof(f5355,plain,(
% 226.41/29.16 ![X0,X1]: (complement(X0)=complement(join(meet(X0,X1),X0)))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2367,f5308])).
% 226.41/29.16 fof(f5356,plain,(
% 226.41/29.16 ![X0,X1]: (complement(X0)=complement(join(X0,meet(X0,X1))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f19,f5355])).
% 226.41/29.16 fof(f5425,plain,(
% 226.41/29.16 ![X0,X1]: (converse(X0)=meet(converse(X0),converse(join(X1,X0))))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f27,f5332])).
% 226.41/29.16 fof(f5484,plain,(
% 226.41/29.16 converse(top)=top),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f4213,f4506])).
% 226.41/29.16 fof(f5542,plain,(
% 226.41/29.16 ![X0]: (composition(top,composition(sF5_fnc,X0))=composition(sF5_fnc,X0))),
% 226.41/29.16 inference(backward_demodulation,[status(thm)],[f5484,f751])).
% 226.41/29.16 fof(f5626,plain,(
% 226.41/29.16 ![X0]: (converse(composition(top,X0))=composition(converse(X0),top))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f5484,f185])).
% 226.41/29.16 fof(f6042,plain,(
% 226.41/29.16 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X1,X0)))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f592,f5348])).
% 226.41/29.16 fof(f6093,plain,(
% 226.41/29.16 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X1,X0)))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f592,f5352])).
% 226.41/29.16 fof(f7323,plain,(
% 226.41/29.16 ![X0,X1]: (complement(complement(X0))=join(X0,meet(X0,X1)))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f5356,f1137])).
% 226.41/29.16 fof(f7378,plain,(
% 226.41/29.16 ![X0,X1]: (X0=join(X0,meet(X0,X1)))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f1137,f7323])).
% 226.41/29.16 fof(f7629,plain,(
% 226.41/29.16 sK1_skl=join(sK1_skl,sF4_fnc)),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f5345,f7378])).
% 226.41/29.16 fof(f7631,plain,(
% 226.41/29.16 sK0_skl=join(sK0_skl,sF2_fnc)),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f5346,f7378])).
% 226.41/29.16 fof(f7633,plain,(
% 226.41/29.16 ![X0,X1]: (X0=join(X0,meet(X1,X0)))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f6093,f7378])).
% 226.41/29.16 fof(f7663,plain,(
% 226.41/29.16 ![X0,X1,X2]: (join(X0,join(meet(X0,X1),X2))=join(X2,X0))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f7378,f74])).
% 226.41/29.16 fof(f7700,plain,(
% 226.41/29.16 composition(sK1_skl,sF2_fnc)=join(sF1_fnc,composition(sF4_fnc,sF2_fnc))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f7629,f91])).
% 226.41/29.16 fof(f7709,plain,(
% 226.41/29.16 sF1_fnc=join(sF1_fnc,composition(sF4_fnc,sF2_fnc))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f41,f7700])).
% 226.41/29.16 fof(f7710,plain,(
% 226.41/29.16 sF1_fnc=join(sF1_fnc,sF3_fnc)),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f44,f7709])).
% 226.41/29.16 fof(f7724,plain,(
% 226.41/29.16 ![X0]: (composition(sK1_skl,composition(sF2_fnc,X0))=composition(sF0_fnc,X0))),
% 226.41/29.16 inference(backward_demodulation,[status(thm)],[f7800,f66])).
% 226.41/29.16 fof(f7800,plain,(
% 226.41/29.16 sF1_fnc=sF0_fnc),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f45,f7710])).
% 226.41/29.16 fof(f7827,plain,(
% 226.41/29.16 composition(sK0_skl,top)=join(sK0_skl,composition(sF2_fnc,top))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f7631,f92])).
% 226.41/29.16 fof(f7836,plain,(
% 226.41/29.16 sK0_skl=join(sK0_skl,composition(sF2_fnc,top))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f38,f7827])).
% 226.41/29.16 fof(f8231,plain,(
% 226.41/29.16 ![X0,X1,X2]: (join(meet(X0,X1),join(X1,X2))=join(X1,X2))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f7633,f79])).
% 226.41/29.16 fof(f8235,plain,(
% 226.41/29.16 ![X0,X1,X2]: (join(X0,join(meet(X1,X0),X2))=join(X0,X2))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f7633,f20])).
% 226.41/29.16 fof(f8254,plain,(
% 226.41/29.16 ![X0,X1,X2]: (join(X0,join(X1,meet(X2,X0)))=join(X0,X1))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f74,f8231])).
% 226.41/29.16 fof(f8578,plain,(
% 226.41/29.16 ![X0,X1]: (meet(meet(X0,X1),complement(X1))=complement(top))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f4258,f1157])).
% 226.41/29.16 fof(f8611,plain,(
% 226.41/29.16 ![X0,X1]: (meet(complement(X0),meet(X1,X0))=complement(top))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f592,f8578])).
% 226.41/29.16 fof(f8614,plain,(
% 226.41/29.16 ![X0,X1]: (meet(complement(X0),meet(X1,X0))=zero)),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f140,f8611])).
% 226.41/29.16 fof(f9998,plain,(
% 226.41/29.16 ![X0,X1]: (meet(complement(join(X0,X1)),X1)=zero)),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f5332,f8614])).
% 226.41/29.16 fof(f10041,plain,(
% 226.41/29.16 ![X0,X1]: (meet(X0,complement(join(X1,X0)))=zero)),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f592,f9998])).
% 226.41/29.16 fof(f10253,plain,(
% 226.41/29.16 meet(composition(sF2_fnc,top),complement(sK0_skl))=zero),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f7836,f10041])).
% 226.41/29.16 fof(f10281,plain,(
% 226.41/29.16 ![X0]: (meet(composition(converse(X0),complement(X0)),complement(complement(one)))=zero)),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f246,f10041])).
% 226.41/29.16 fof(f10364,plain,(
% 226.41/29.16 meet(complement(sK0_skl),composition(sF2_fnc,top))=zero),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f592,f10253])).
% 226.41/29.16 fof(f10390,plain,(
% 226.41/29.16 ![X0]: (meet(complement(complement(one)),composition(converse(X0),complement(X0)))=zero)),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f592,f10281])).
% 226.41/29.16 fof(f10391,plain,(
% 226.41/29.16 ![X0]: (meet(one,composition(converse(X0),complement(X0)))=zero)),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f1137,f10390])).
% 226.41/29.16 fof(f21647,plain,(
% 226.41/29.16 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,composition(one,meet(X0,composition(converse(one),X1)))),X2))=join(meet(X1,composition(one,meet(X0,composition(converse(one),X1)))),X2))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f2609,f687])).
% 226.41/29.16 fof(f21778,plain,(
% 226.41/29.16 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,meet(X0,composition(converse(one),X1))),X2))=join(meet(X1,composition(one,meet(X0,composition(converse(one),X1)))),X2))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2609,f21647])).
% 226.41/29.16 fof(f21779,plain,(
% 226.41/29.16 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,meet(X0,composition(one,X1))),X2))=join(meet(X1,composition(one,meet(X0,composition(converse(one),X1)))),X2))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2567,f21778])).
% 226.41/29.16 fof(f21780,plain,(
% 226.41/29.16 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,meet(X0,X1)),X2))=join(meet(X1,composition(one,meet(X0,composition(converse(one),X1)))),X2))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2609,f21779])).
% 226.41/29.16 fof(f21781,plain,(
% 226.41/29.16 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,composition(one,meet(X0,composition(converse(one),X1)))),X2))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f8235,f21780])).
% 226.41/29.16 fof(f21782,plain,(
% 226.41/29.16 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,meet(X0,composition(converse(one),X1))),X2))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2609,f21781])).
% 226.41/29.16 fof(f21783,plain,(
% 226.41/29.16 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,meet(X0,composition(one,X1))),X2))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2567,f21782])).
% 226.41/29.16 fof(f21784,plain,(
% 226.41/29.16 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,meet(X0,X1)),X2))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2609,f21783])).
% 226.41/29.16 fof(f21785,plain,(
% 226.41/29.16 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,X0),X2))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f6042,f21784])).
% 226.41/29.16 fof(f22631,plain,(
% 226.41/29.16 composition(top,zero)=composition(sF5_fnc,complement(sK0_skl))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f2936,f5542])).
% 226.41/29.16 fof(f22694,plain,(
% 226.41/29.16 composition(top,zero)=zero),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2936,f22631])).
% 226.41/29.16 fof(f23113,plain,(
% 226.41/29.16 ![X0]: (join(meet(composition(zero,X0),converse(top)),meet(converse(top),composition(zero,meet(X0,converse(zero)))))=meet(converse(top),composition(zero,meet(X0,converse(composition(top,zero))))))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f22694,f682])).
% 226.41/29.16 fof(f23136,plain,(
% 226.41/29.16 join(complement(converse(top)),composition(zero,complement(converse(zero))))=complement(converse(top))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f22694,f252])).
% 226.41/29.16 fof(f23164,plain,(
% 226.41/29.16 ![X0]: (join(meet(converse(top),composition(zero,X0)),meet(converse(top),composition(zero,meet(X0,converse(zero)))))=meet(converse(top),composition(zero,meet(X0,converse(composition(top,zero))))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f21785,f23113])).
% 226.41/29.16 fof(f23165,plain,(
% 226.41/29.16 ![X0]: (join(meet(top,composition(zero,X0)),meet(converse(top),composition(zero,meet(X0,converse(zero)))))=meet(converse(top),composition(zero,meet(X0,converse(composition(top,zero))))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f5484,f23164])).
% 226.41/29.16 fof(f23166,plain,(
% 226.41/29.16 ![X0]: (join(composition(zero,X0),meet(converse(top),composition(zero,meet(X0,converse(zero)))))=meet(converse(top),composition(zero,meet(X0,converse(composition(top,zero))))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f3220,f23165])).
% 226.41/29.16 fof(f23167,plain,(
% 226.41/29.16 ![X0]: (join(composition(zero,X0),meet(top,composition(zero,meet(X0,converse(zero)))))=meet(converse(top),composition(zero,meet(X0,converse(composition(top,zero))))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f5484,f23166])).
% 226.41/29.16 fof(f23168,plain,(
% 226.41/29.16 ![X0]: (join(composition(zero,X0),composition(zero,meet(X0,converse(zero))))=meet(converse(top),composition(zero,meet(X0,converse(composition(top,zero))))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f3220,f23167])).
% 226.41/29.16 fof(f23169,plain,(
% 226.41/29.16 ![X0]: (join(composition(zero,X0),composition(zero,meet(X0,zero)))=meet(converse(top),composition(zero,meet(X0,converse(composition(top,zero))))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f3742,f23168])).
% 226.41/29.16 fof(f23170,plain,(
% 226.41/29.16 ![X0]: (join(composition(zero,X0),composition(zero,zero))=meet(converse(top),composition(zero,meet(X0,converse(composition(top,zero))))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f4397,f23169])).
% 226.41/29.16 fof(f23171,plain,(
% 226.41/29.16 ![X0]: (join(composition(zero,X0),composition(zero,zero))=meet(top,composition(zero,meet(X0,converse(composition(top,zero))))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f5484,f23170])).
% 226.41/29.16 fof(f23172,plain,(
% 226.41/29.16 ![X0]: (join(composition(zero,X0),composition(zero,zero))=composition(zero,meet(X0,converse(composition(top,zero)))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f3220,f23171])).
% 226.41/29.16 fof(f23173,plain,(
% 226.41/29.16 ![X0]: (join(composition(zero,X0),composition(zero,zero))=composition(zero,meet(X0,composition(converse(zero),top))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f5626,f23172])).
% 226.41/29.16 fof(f23174,plain,(
% 226.41/29.16 ![X0]: (join(composition(zero,X0),composition(zero,zero))=composition(zero,meet(X0,composition(zero,top))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f3742,f23173])).
% 226.41/29.16 fof(f23318,plain,(
% 226.41/29.16 join(complement(top),composition(zero,complement(converse(zero))))=complement(converse(top))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f5484,f23136])).
% 226.41/29.16 fof(f23319,plain,(
% 226.41/29.16 join(zero,composition(zero,complement(converse(zero))))=complement(converse(top))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f140,f23318])).
% 226.41/29.16 fof(f23320,plain,(
% 226.41/29.16 composition(zero,complement(converse(zero)))=complement(converse(top))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2871,f23319])).
% 226.41/29.16 fof(f23321,plain,(
% 226.41/29.16 composition(zero,complement(zero))=complement(converse(top))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f3742,f23320])).
% 226.41/29.16 fof(f23322,plain,(
% 226.41/29.16 composition(zero,top)=complement(converse(top))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f1016,f23321])).
% 226.41/29.16 fof(f23323,plain,(
% 226.41/29.16 composition(zero,top)=complement(top)),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f5484,f23322])).
% 226.41/29.16 fof(f23326,plain,(
% 226.41/29.16 ![X0]: (join(composition(zero,X0),composition(zero,zero))=composition(zero,meet(X0,zero)))),
% 226.41/29.16 inference(backward_demodulation,[status(thm)],[f23334,f23174])).
% 226.41/29.16 fof(f23334,plain,(
% 226.41/29.16 composition(zero,top)=zero),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f140,f23323])).
% 226.41/29.16 fof(f23424,plain,(
% 226.41/29.16 ![X0]: (join(composition(zero,X0),composition(zero,zero))=composition(zero,zero))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f4397,f23326])).
% 226.41/29.16 fof(f23466,plain,(
% 226.41/29.16 ![X0]: (composition(join(converse(top),X0),converse(zero))=join(converse(zero),composition(X0,converse(zero))))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f23334,f188])).
% 226.41/29.16 fof(f23649,plain,(
% 226.41/29.16 ![X0]: (composition(join(top,X0),converse(zero))=join(converse(zero),composition(X0,converse(zero))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f5484,f23466])).
% 226.41/29.16 fof(f23650,plain,(
% 226.41/29.16 ![X0]: (composition(top,converse(zero))=join(converse(zero),composition(X0,converse(zero))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f4309,f23649])).
% 226.41/29.16 fof(f23651,plain,(
% 226.41/29.16 ![X0]: (composition(top,zero)=join(converse(zero),composition(X0,converse(zero))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f3742,f23650])).
% 226.41/29.16 fof(f23652,plain,(
% 226.41/29.16 ![X0]: (zero=join(converse(zero),composition(X0,converse(zero))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f22694,f23651])).
% 226.41/29.16 fof(f23653,plain,(
% 226.41/29.16 ![X0]: (zero=composition(join(X0,one),converse(zero)))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2657,f23652])).
% 226.41/29.16 fof(f23654,plain,(
% 226.41/29.16 ![X0]: (zero=composition(join(X0,one),zero))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f3742,f23653])).
% 226.41/29.16 fof(f23655,plain,(
% 226.41/29.16 ![X0]: (zero=join(zero,composition(X0,zero)))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2657,f23654])).
% 226.41/29.16 fof(f23661,plain,(
% 226.41/29.16 ![X0]: (join(composition(zero,X0),composition(zero,zero))=zero)),
% 226.41/29.16 inference(backward_demodulation,[status(thm)],[f23692,f23424])).
% 226.41/29.16 fof(f23692,plain,(
% 226.41/29.16 ![X0]: (zero=composition(X0,zero))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2871,f23655])).
% 226.41/29.16 fof(f23745,plain,(
% 226.41/29.16 ![X0]: (join(composition(zero,X0),zero)=zero)),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f23692,f23661])).
% 226.41/29.16 fof(f23780,plain,(
% 226.41/29.16 ![X0]: (composition(zero,X0)=zero)),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2994,f23745])).
% 226.41/29.16 fof(f51950,plain,(
% 226.41/29.16 ![X0,X1,X2]: (complement(meet(complement(meet(X0,X1)),complement(X2)))=join(X2,complement(complement(meet(X1,X0)))))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f1225,f2204])).
% 226.41/29.16 fof(f52038,plain,(
% 226.41/29.16 ![X0,X1,X2]: (join(X0,complement(complement(meet(X1,X2))))=join(X0,complement(complement(meet(X2,X1)))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f2204,f51950])).
% 226.41/29.16 fof(f52039,plain,(
% 226.41/29.16 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(X0,complement(complement(meet(X2,X1)))))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f1137,f52038])).
% 226.41/29.16 fof(f52040,plain,(
% 226.41/29.16 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(X0,meet(X2,X1)))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f1137,f52039])).
% 226.41/29.16 fof(f63124,plain,(
% 226.41/29.16 ![X0,X1]: (join(X0,X1)=join(meet(complement(X0),X1),X0))),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f937,f7663])).
% 226.41/29.16 fof(f63441,plain,(
% 226.41/29.16 ![X0,X1]: (join(X0,X1)=join(X0,meet(complement(X0),X1)))),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f19,f63124])).
% 226.41/29.16 fof(f66163,plain,(
% 226.41/29.16 join(complement(sF5_fnc),sK1_skl)=join(complement(sF5_fnc),sF4_fnc)),
% 226.41/29.16 inference(paramodulation,[status(thm)],[f1080,f8254])).
% 226.41/29.16 fof(f66459,plain,(
% 226.41/29.16 join(sK1_skl,complement(sF5_fnc))=join(complement(sF5_fnc),sF4_fnc)),
% 226.41/29.16 inference(forward_demodulation,[status(thm)],[f19,f66163])).
% 226.41/29.16 fof(f66460,plain,(
% 226.41/29.18 join(sK1_skl,complement(sF5_fnc))=join(sF4_fnc,complement(sF5_fnc))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f19,f66459])).
% 226.41/29.18 fof(f72523,plain,(
% 226.41/29.18 join(meet(composition(converse(sF2_fnc),complement(sK0_skl)),top),meet(top,composition(converse(sF2_fnc),zero)))=meet(top,composition(converse(sF2_fnc),meet(complement(sK0_skl),composition(sF2_fnc,top))))),
% 226.41/29.18 inference(paramodulation,[status(thm)],[f10364,f671])).
% 226.41/29.18 fof(f72592,plain,(
% 226.41/29.18 join(meet(top,composition(converse(sF2_fnc),zero)),meet(composition(converse(sF2_fnc),complement(sK0_skl)),top))=meet(top,composition(converse(sF2_fnc),meet(complement(sK0_skl),composition(sF2_fnc,top))))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f19,f72523])).
% 226.41/29.18 fof(f72593,plain,(
% 226.41/29.18 join(meet(top,composition(converse(sF2_fnc),zero)),meet(top,composition(converse(sF2_fnc),complement(sK0_skl))))=meet(top,composition(converse(sF2_fnc),meet(complement(sK0_skl),composition(sF2_fnc,top))))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f52040,f72592])).
% 226.41/29.18 fof(f72594,plain,(
% 226.41/29.18 join(composition(converse(sF2_fnc),zero),meet(top,composition(converse(sF2_fnc),complement(sK0_skl))))=meet(top,composition(converse(sF2_fnc),meet(complement(sK0_skl),composition(sF2_fnc,top))))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f3220,f72593])).
% 226.41/29.18 fof(f72595,plain,(
% 226.41/29.18 join(zero,meet(top,composition(converse(sF2_fnc),complement(sK0_skl))))=meet(top,composition(converse(sF2_fnc),meet(complement(sK0_skl),composition(sF2_fnc,top))))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f23692,f72594])).
% 226.41/29.18 fof(f72596,plain,(
% 226.41/29.18 meet(top,composition(converse(sF2_fnc),complement(sK0_skl)))=meet(top,composition(converse(sF2_fnc),meet(complement(sK0_skl),composition(sF2_fnc,top))))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f2871,f72595])).
% 226.41/29.18 fof(f72597,plain,(
% 226.41/29.18 composition(converse(sF2_fnc),complement(sK0_skl))=meet(top,composition(converse(sF2_fnc),meet(complement(sK0_skl),composition(sF2_fnc,top))))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f3220,f72596])).
% 226.41/29.18 fof(f72598,plain,(
% 226.41/29.18 composition(converse(sF2_fnc),complement(sK0_skl))=composition(converse(sF2_fnc),meet(complement(sK0_skl),composition(sF2_fnc,top)))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f3220,f72597])).
% 226.41/29.18 fof(f72599,plain,(
% 226.41/29.18 composition(converse(sF2_fnc),complement(sK0_skl))=composition(converse(sF2_fnc),zero)),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f10364,f72598])).
% 226.41/29.18 fof(f72600,plain,(
% 226.41/29.18 composition(converse(sF2_fnc),complement(sK0_skl))=zero),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f23692,f72599])).
% 226.41/29.18 fof(f72723,plain,(
% 226.41/29.18 converse(zero)=composition(converse(complement(sK0_skl)),sF2_fnc)),
% 226.41/29.18 inference(paramodulation,[status(thm)],[f72600,f185])).
% 226.41/29.18 fof(f72834,plain,(
% 226.41/29.18 zero=composition(converse(complement(sK0_skl)),sF2_fnc)),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f3742,f72723])).
% 226.41/29.18 fof(f73983,plain,(
% 226.41/29.18 ![X0]: (composition(join(sF4_fnc,converse(complement(sK0_skl))),composition(sF2_fnc,X0))=composition(join(sF3_fnc,zero),X0))),
% 226.41/29.18 inference(paramodulation,[status(thm)],[f72834,f101])).
% 226.41/29.18 fof(f74040,plain,(
% 226.41/29.18 ![X0]: (composition(converse(complement(sK0_skl)),composition(sF2_fnc,X0))=composition(zero,X0))),
% 226.41/29.18 inference(paramodulation,[status(thm)],[f72834,f23])).
% 226.41/29.18 fof(f74097,plain,(
% 226.41/29.18 ![X0]: (composition(join(sF4_fnc,converse(complement(sK0_skl))),composition(sF2_fnc,X0))=composition(join(zero,sF3_fnc),X0))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f2089,f73983])).
% 226.41/29.18 fof(f74098,plain,(
% 226.41/29.18 ![X0]: (composition(join(sF4_fnc,converse(complement(sK0_skl))),composition(sF2_fnc,X0))=composition(sF3_fnc,X0))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f2871,f74097])).
% 226.41/29.18 fof(f74313,plain,(
% 226.41/29.18 ![X0]: (composition(converse(complement(sK0_skl)),composition(sF2_fnc,X0))=zero)),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f23780,f74040])).
% 226.41/29.18 fof(f75288,plain,(
% 226.41/29.18 ![X0]: (join(meet(composition(one,converse(complement(X0))),converse(X0)),meet(converse(X0),composition(zero,converse(complement(X0)))))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 226.41/29.18 inference(paramodulation,[status(thm)],[f10391,f1290])).
% 226.41/29.18 fof(f75435,plain,(
% 226.41/29.18 ![X0]: (join(meet(converse(X0),composition(zero,converse(complement(X0)))),meet(composition(one,converse(complement(X0))),converse(X0)))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f19,f75288])).
% 226.41/29.18 fof(f75436,plain,(
% 226.41/29.18 ![X0]: (join(meet(converse(X0),composition(zero,converse(complement(X0)))),meet(converse(X0),composition(one,converse(complement(X0)))))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f52040,f75435])).
% 226.41/29.18 fof(f75437,plain,(
% 226.41/29.18 ![X0]: (join(meet(converse(X0),composition(one,converse(complement(X0)))),meet(converse(X0),composition(zero,converse(complement(X0)))))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f19,f75436])).
% 226.41/29.18 fof(f75438,plain,(
% 226.41/29.18 ![X0]: (join(meet(converse(X0),converse(complement(X0))),meet(converse(X0),composition(zero,converse(complement(X0)))))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f2609,f75437])).
% 226.41/29.18 fof(f75439,plain,(
% 226.41/29.18 ![X0]: (join(meet(converse(X0),converse(complement(X0))),meet(converse(X0),zero))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f23780,f75438])).
% 226.41/29.18 fof(f75440,plain,(
% 226.41/29.18 ![X0]: (join(meet(converse(X0),zero),meet(converse(X0),converse(complement(X0))))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f19,f75439])).
% 226.41/29.18 fof(f75441,plain,(
% 226.41/29.18 ![X0]: (join(meet(zero,converse(X0)),meet(converse(X0),converse(complement(X0))))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f21785,f75440])).
% 226.41/29.18 fof(f75442,plain,(
% 226.41/29.18 ![X0]: (join(zero,meet(converse(X0),converse(complement(X0))))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f4350,f75441])).
% 226.41/29.18 fof(f75443,plain,(
% 226.41/29.18 ![X0]: (meet(converse(X0),converse(complement(X0)))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f2871,f75442])).
% 226.41/29.18 fof(f75444,plain,(
% 226.41/29.18 ![X0]: (meet(converse(X0),converse(complement(X0)))=meet(converse(X0),composition(zero,converse(complement(X0)))))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f10391,f75443])).
% 226.41/29.18 fof(f75445,plain,(
% 226.41/29.18 ![X0]: (meet(converse(X0),converse(complement(X0)))=meet(converse(X0),zero))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f23780,f75444])).
% 226.41/29.18 fof(f75446,plain,(
% 226.41/29.18 ![X0]: (meet(converse(X0),converse(complement(X0)))=zero)),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f4397,f75445])).
% 226.41/29.18 fof(f75586,plain,(
% 226.41/29.18 ![X0]: (meet(X0,converse(complement(converse(X0))))=zero)),
% 226.41/29.18 inference(paramodulation,[status(thm)],[f26,f75446])).
% 226.41/29.18 fof(f75651,plain,(
% 226.41/29.18 ![X0]: (converse(X0)=join(zero,meet(complement(converse(complement(X0))),converse(X0))))),
% 226.41/29.18 inference(paramodulation,[status(thm)],[f75446,f1086])).
% 226.41/29.18 fof(f75761,plain,(
% 226.41/29.18 ![X0]: (converse(X0)=meet(complement(converse(complement(X0))),converse(X0)))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f2871,f75651])).
% 226.41/29.18 fof(f75763,plain,(
% 226.41/29.18 ![X0]: (converse(X0)=meet(converse(X0),complement(converse(complement(X0)))))),
% 226.41/29.18 inference(forward_demodulation,[status(thm)],[f592,f75761])).
% 226.41/29.18 fof(f76130,plain,(
% 226.41/29.18 ![X0]: (join(X0,converse(complement(converse(complement(X0)))))=join(X0,zero))),
% 226.41/29.18 inference(paramodulation,[status(thm)],[f75586,f63441])).
% 226.41/29.18 fof(f76224,plain,(
% 226.41/29.18 ![X0]: (join(X0,converse(complement(converse(complement(X0)))))=X0)),
% 90.54/29.65 inference(forward_demodulation,[status(thm)],[f2994,f76130])).
% 90.54/29.65 fof(f76419,plain,(
% 90.54/29.65 ![X0]: (converse(converse(complement(converse(complement(X0)))))=meet(converse(converse(complement(converse(complement(X0))))),converse(X0)))),
% 90.54/29.65 inference(paramodulation,[status(thm)],[f76224,f5425])).
% 90.54/29.65 fof(f76520,plain,(
% 90.54/29.65 ![X0]: (complement(converse(complement(X0)))=meet(converse(converse(complement(converse(complement(X0))))),converse(X0)))),
% 90.54/29.65 inference(forward_demodulation,[status(thm)],[f26,f76419])).
% 90.54/29.65 fof(f76521,plain,(
% 90.54/29.65 ![X0]: (complement(converse(complement(X0)))=meet(converse(X0),converse(converse(complement(converse(complement(X0)))))))),
% 90.54/29.65 inference(forward_demodulation,[status(thm)],[f592,f76520])).
% 90.54/29.65 fof(f76522,plain,(
% 90.54/29.65 ![X0]: (complement(converse(complement(X0)))=meet(converse(X0),complement(converse(complement(X0)))))),
% 90.54/29.65 inference(forward_demodulation,[status(thm)],[f26,f76521])).
% 90.54/29.65 fof(f76558,plain,(
% 90.54/29.65 ![X0]: (complement(converse(complement(X0)))=converse(X0))),
% 90.54/29.65 inference(forward_demodulation,[status(thm)],[f75763,f76522])).
% 90.54/29.65 fof(f77343,plain,(
% 90.54/29.65 ![X0]: (complement(converse(X0))=converse(complement(X0)))),
% 90.54/29.65 inference(paramodulation,[status(thm)],[f1137,f76558])).
% 90.54/29.65 fof(f77566,plain,(
% 90.54/29.65 ![X0]: (composition(complement(converse(sK0_skl)),composition(sF2_fnc,X0))=zero)),
% 90.54/29.65 inference(backward_demodulation,[status(thm)],[f77343,f74313])).
% 90.54/29.65 fof(f77570,plain,(
% 90.54/29.65 ![X0]: (composition(join(sF4_fnc,complement(converse(sK0_skl))),composition(sF2_fnc,X0))=composition(sF3_fnc,X0))),
% 90.54/29.65 inference(backward_demodulation,[status(thm)],[f77343,f74098])).
% 90.54/29.65 fof(f78005,plain,(
% 90.54/29.65 ![X0]: (composition(complement(sF5_fnc),composition(sF2_fnc,X0))=zero)),
% 90.54/29.65 inference(forward_demodulation,[status(thm)],[f42,f77566])).
% 90.54/29.65 fof(f78009,plain,(
% 90.54/29.65 ![X0]: (composition(join(sF4_fnc,complement(sF5_fnc)),composition(sF2_fnc,X0))=composition(sF3_fnc,X0))),
% 90.54/29.65 inference(forward_demodulation,[status(thm)],[f42,f77570])).
% 90.54/29.65 fof(f78010,plain,(
% 90.54/29.65 ![X0]: (composition(join(sK1_skl,complement(sF5_fnc)),composition(sF2_fnc,X0))=composition(sF3_fnc,X0))),
% 90.54/29.65 inference(forward_demodulation,[status(thm)],[f66460,f78009])).
% 90.54/29.65 fof(f78762,plain,(
% 90.54/29.65 ![X0,X1]: (composition(join(X0,complement(sF5_fnc)),composition(sF2_fnc,X1))=join(zero,composition(X0,composition(sF2_fnc,X1))))),
% 90.54/29.65 inference(paramodulation,[status(thm)],[f78005,f86])).
% 90.54/29.65 fof(f79039,plain,(
% 90.54/29.65 ![X0]: (composition(sK1_skl,composition(sF2_fnc,X0))=composition(sF3_fnc,X0))),
% 90.54/29.65 inference(backward_demodulation,[status(thm)],[f79041,f78010])).
% 90.54/29.65 fof(f79041,plain,(
% 90.54/29.65 ![X0,X1]: (composition(join(X0,complement(sF5_fnc)),composition(sF2_fnc,X1))=composition(X0,composition(sF2_fnc,X1)))),
% 90.54/29.65 inference(forward_demodulation,[status(thm)],[f2871,f78762])).
% 90.54/29.65 fof(f79174,plain,(
% 90.54/29.65 ![X0]: (composition(sF0_fnc,X0)=composition(sF3_fnc,X0))),
% 90.54/29.65 inference(forward_demodulation,[status(thm)],[f7724,f79039])).
% 90.54/29.65 fof(f79336,plain,(
% 90.54/29.65 composition(sF0_fnc,one)=sF3_fnc),
% 90.54/29.65 inference(paramodulation,[status(thm)],[f24,f79174])).
% 90.54/29.65 fof(f79464,plain,(
% 90.54/29.65 sF0_fnc=sF3_fnc),
% 90.54/29.65 inference(forward_demodulation,[status(thm)],[f24,f79336])).
% 90.54/29.65 fof(f79465,plain,(
% 90.54/29.65 $false),
% 90.54/29.65 inference(forward_subsumption_resolution,[status(thm)],[f79464,f55])).
% 90.54/29.65 % SZS output end CNFRefutation for theBenchmark.p
% 41.68/29.77 % Elapsed time: 29.293603 seconds
% 41.68/29.77 % CPU time: 229.923144 seconds
% 41.68/29.77 % Total memory used: 1.364 GB
% 41.68/29.77 % Net memory used: 1.340 GB
%------------------------------------------------------------------------------