%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL045+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 : n015.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:45 PM UTC 2026
% Result : Theorem 132.00s 17.23s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL045+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.15/0.39 % Computer : n015.cluster.edu
% 0.15/0.39 % Model : x86_64 x86_64
% 0.15/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.39 % Memory : 8046.5625MB
% 0.15/0.39 % OS : Linux 6.8.0-71-generic
% 0.15/0.39 % CPULimit : 300
% 0.15/0.39 % WCLimit : 300
% 0.15/0.39 % DateTime : Mon Sep 21 04:11:36 UTC 2026
% 0.15/0.40 % CPUTime :
% 0.15/0.40 % Drodi V4.1.1
% 132.00/17.23 % Refutation found
% 132.00/17.23 % SZS status Theorem for theBenchmark: Theorem is valid
% 132.00/17.23 % SZS output start CNFRefutation for theBenchmark
% 132.00/17.23 fof(f1,axiom,(
% 132.00/17.23 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 132.00/17.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.00/17.23 fof(f2,axiom,(
% 132.00/17.23 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 132.00/17.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.00/17.23 fof(f3,axiom,(
% 132.00/17.23 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 132.00/17.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.00/17.23 fof(f4,axiom,(
% 132.00/17.23 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 132.00/17.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.00/17.23 fof(f5,axiom,(
% 132.00/17.23 (! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2) )),
% 132.00/17.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.00/17.23 fof(f6,axiom,(
% 132.00/17.23 (! [X0] : composition(X0,one) = X0 )),
% 132.00/17.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.00/17.23 fof(f7,axiom,(
% 132.00/17.23 (! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) )),
% 132.00/17.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.00/17.23 fof(f8,axiom,(
% 132.00/17.23 (! [X0] : converse(converse(X0)) = X0 )),
% 132.00/17.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.00/17.23 fof(f9,axiom,(
% 132.00/17.23 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 132.00/17.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.00/17.23 fof(f10,axiom,(
% 132.00/17.23 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 132.00/17.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.00/17.23 fof(f11,axiom,(
% 132.00/17.23 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 132.00/17.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.00/17.23 fof(f12,axiom,(
% 132.00/17.23 (! [X0] : top = join(X0,complement(X0)) )),
% 132.00/17.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.00/17.23 fof(f13,axiom,(
% 132.00/17.23 (! [X0] : zero = meet(X0,complement(X0)) )),
% 132.00/17.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.00/17.23 fof(f14,axiom,(
% 132.00/17.23 (! [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))) )),
% 132.00/17.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.00/17.23 fof(f15,axiom,(
% 132.00/17.23 (! [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) )),
% 132.00/17.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.00/17.23 fof(f16,axiom,(
% 132.00/17.23 (! [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) )),
% 132.00/17.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.00/17.23 fof(f17,conjecture,(
% 132.00/17.23 (! [X0] : join(X0,composition(composition(X0,converse(X0)),X0)) = composition(composition(X0,converse(X0)),X0) )),
% 132.00/17.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.00/17.23 fof(f18,negated_conjecture,(
% 132.00/17.23 ~((! [X0] : join(X0,composition(composition(X0,converse(X0)),X0)) = composition(composition(X0,converse(X0)),X0) ))),
% 132.00/17.23 inference(negated_conjecture,[status(cth)],[f17])).
% 132.00/17.23 fof(f19,plain,(
% 132.00/17.23 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 132.00/17.23 inference(cnf_transformation,[status(thm)],[f1])).
% 132.00/17.23 fof(f20,plain,(
% 132.00/17.23 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 132.00/17.23 inference(cnf_transformation,[status(thm)],[f2])).
% 132.00/17.23 fof(f21,plain,(
% 132.00/17.23 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 132.00/17.23 inference(cnf_transformation,[status(thm)],[f3])).
% 132.00/17.23 fof(f22,plain,(
% 132.00/17.23 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 132.00/17.23 inference(cnf_transformation,[status(thm)],[f4])).
% 132.00/17.23 fof(f23,plain,(
% 132.00/17.23 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 132.00/17.23 inference(cnf_transformation,[status(thm)],[f5])).
% 132.00/17.23 fof(f24,plain,(
% 132.00/17.23 ![X0]: (composition(X0,one)=X0)),
% 132.00/17.23 inference(cnf_transformation,[status(thm)],[f6])).
% 132.00/17.23 fof(f25,plain,(
% 132.00/17.23 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 132.00/17.23 inference(cnf_transformation,[status(thm)],[f7])).
% 132.00/17.23 fof(f26,plain,(
% 132.00/17.23 ![X0]: (converse(converse(X0))=X0)),
% 132.00/17.23 inference(cnf_transformation,[status(thm)],[f8])).
% 132.00/17.23 fof(f27,plain,(
% 132.00/17.23 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 132.00/17.23 inference(cnf_transformation,[status(thm)],[f9])).
% 132.00/17.23 fof(f28,plain,(
% 132.00/17.23 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 132.00/17.23 inference(cnf_transformation,[status(thm)],[f10])).
% 132.00/17.23 fof(f29,plain,(
% 132.00/17.23 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 132.00/17.23 inference(cnf_transformation,[status(thm)],[f11])).
% 132.00/17.23 fof(f30,plain,(
% 132.00/17.23 ![X0]: (top=join(X0,complement(X0)))),
% 132.00/17.23 inference(cnf_transformation,[status(thm)],[f12])).
% 132.00/17.23 fof(f31,plain,(
% 132.00/17.23 ![X0]: (zero=meet(X0,complement(X0)))),
% 132.00/17.23 inference(cnf_transformation,[status(thm)],[f13])).
% 132.00/17.23 fof(f32,plain,(
% 132.00/17.23 ![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))))),
% 132.00/17.23 inference(cnf_transformation,[status(thm)],[f14])).
% 132.00/17.23 fof(f33,plain,(
% 132.00/17.23 ![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))),
% 132.00/17.23 inference(cnf_transformation,[status(thm)],[f15])).
% 132.00/17.23 fof(f34,plain,(
% 132.00/17.23 ![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))),
% 132.00/17.23 inference(cnf_transformation,[status(thm)],[f16])).
% 132.00/17.23 fof(f35,plain,(
% 132.00/17.23 (?[X0]: ~join(X0,composition(composition(X0,converse(X0)),X0))=composition(composition(X0,converse(X0)),X0))),
% 132.00/17.23 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 132.00/17.23 fof(f36,plain,(
% 132.00/17.23 ~join(sK0_skl,composition(composition(sK0_skl,converse(sK0_skl)),sK0_skl))=composition(composition(sK0_skl,converse(sK0_skl)),sK0_skl)),
% 132.00/17.23 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X0,sK0_skl)],[f35])).
% 132.00/17.23 fof(f37,plain,(
% 132.00/17.23 ~join(sK0_skl,composition(composition(sK0_skl,converse(sK0_skl)),sK0_skl))=composition(composition(sK0_skl,converse(sK0_skl)),sK0_skl)),
% 132.00/17.23 inference(cnf_transformation,[status(thm)],[f36])).
% 132.00/17.23 fof(f45,plain,(
% 132.00/17.23 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 132.00/17.23 inference(backward_demodulation,[status(thm)],[f22,f21])).
% 132.00/17.23 fof(f46,plain,(
% 132.00/17.23 ~join(sK0_skl,composition(sK0_skl,composition(converse(sK0_skl),sK0_skl)))=composition(composition(sK0_skl,converse(sK0_skl)),sK0_skl)),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f23,f37])).
% 132.00/17.23 fof(f47,plain,(
% 132.00/17.23 ~join(sK0_skl,composition(sK0_skl,composition(converse(sK0_skl),sK0_skl)))=composition(sK0_skl,composition(converse(sK0_skl),sK0_skl))),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f23,f46])).
% 132.00/17.23 fof(f53,plain,(
% 132.00/17.23 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f19,f20])).
% 132.00/17.23 fof(f65,plain,(
% 132.00/17.23 ![X0,X1]: (converse(composition(X0,converse(X1)))=composition(X1,converse(X0)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f26,f28])).
% 132.00/17.23 fof(f66,plain,(
% 132.00/17.23 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f26,f28])).
% 132.00/17.23 fof(f83,plain,(
% 132.00/17.23 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f26,f27])).
% 132.00/17.23 fof(f110,plain,(
% 132.00/17.23 ![X0,X1]: (converse(join(X0,converse(X1)))=join(X1,converse(X0)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f19,f83])).
% 132.00/17.23 fof(f127,plain,(
% 132.00/17.23 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X1,X2),composition(X0,X2)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f19,f25])).
% 132.00/17.23 fof(f130,plain,(
% 132.00/17.23 ![X0,X1,X2,X3]: (composition(join(composition(X0,X1),X2),X3)=join(composition(X0,composition(X1,X3)),composition(X2,X3)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f23,f25])).
% 132.00/17.23 fof(f142,plain,(
% 132.00/17.23 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X2,X0)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f19,f53])).
% 132.00/17.23 fof(f144,plain,(
% 132.00/17.23 ![X0,X1,X2,X3]: (join(X0,composition(join(X1,X2),X3))=join(composition(X2,X3),join(X0,composition(X1,X3))))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f25,f53])).
% 132.00/17.23 fof(f204,plain,(
% 132.00/17.23 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f24,f66])).
% 132.00/17.23 fof(f208,plain,(
% 132.00/17.23 ![X0]: (X0=composition(converse(one),X0))),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f26,f204])).
% 132.00/17.23 fof(f212,plain,(
% 132.00/17.23 one=converse(one)),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f24,f208])).
% 132.00/17.23 fof(f219,plain,(
% 132.00/17.23 ![X0]: (X0=composition(one,X0))),
% 132.00/17.23 inference(backward_demodulation,[status(thm)],[f212,f208])).
% 132.00/17.23 fof(f240,plain,(
% 132.00/17.23 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f30,f83])).
% 132.00/17.23 fof(f243,plain,(
% 132.00/17.23 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(X1,top))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f30,f53])).
% 132.00/17.23 fof(f244,plain,(
% 132.00/17.23 ![X0,X1]: (join(X0,top)=join(complement(X1),join(X0,X1)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f30,f53])).
% 132.00/17.23 fof(f247,plain,(
% 132.00/17.23 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f30,f22])).
% 132.00/17.23 fof(f248,plain,(
% 132.00/17.23 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f19,f22])).
% 132.00/17.23 fof(f250,plain,(
% 132.00/17.23 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X0,X1),complement(X2))))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f22,f22])).
% 132.00/17.23 fof(f254,plain,(
% 132.00/17.23 zero=complement(top)),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f31,f247])).
% 132.00/17.23 fof(f259,plain,(
% 132.00/17.23 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f254,f22])).
% 132.00/17.23 fof(f260,plain,(
% 132.00/17.23 top=join(top,zero)),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f254,f30])).
% 132.00/17.23 fof(f264,plain,(
% 132.00/17.23 ![X0]: (join(composition(one,complement(composition(one,X0))),complement(X0))=complement(X0))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f212,f29])).
% 132.00/17.23 fof(f272,plain,(
% 132.00/17.23 ![X0]: (join(composition(converse(X0),complement(composition(X0,top))),zero)=complement(top))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f254,f29])).
% 132.00/17.23 fof(f280,plain,(
% 132.00/17.23 ![X0]: (join(complement(composition(one,X0)),complement(X0))=complement(X0))),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f219,f264])).
% 132.00/17.23 fof(f281,plain,(
% 132.00/17.23 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f219,f280])).
% 132.00/17.23 fof(f287,plain,(
% 132.00/17.23 ![X0]: (join(composition(converse(X0),complement(composition(X0,top))),zero)=zero)),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f254,f272])).
% 132.00/17.23 fof(f360,plain,(
% 132.00/17.23 ![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)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f28,f33])).
% 132.00/17.23 fof(f388,plain,(
% 132.00/17.23 ![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)))),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f28,f360])).
% 132.00/17.23 fof(f408,plain,(
% 132.00/17.23 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f281,f22])).
% 132.00/17.23 fof(f933,plain,(
% 132.00/17.23 ![X0]: (join(top,X0)=join(zero,join(X0,top)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f260,f142])).
% 132.00/17.23 fof(f1039,plain,(
% 132.00/17.23 ![X0]: (converse(converse(top))=join(complement(converse(X0)),converse(X0)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f240,f110])).
% 132.00/17.23 fof(f1069,plain,(
% 132.00/17.23 ![X0]: (top=join(complement(converse(X0)),converse(X0)))),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f26,f1039])).
% 132.00/17.23 fof(f1080,plain,(
% 132.00/17.23 ![X0]: (top=join(complement(X0),converse(converse(X0))))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f26,f1069])).
% 132.00/17.23 fof(f1110,plain,(
% 132.00/17.23 ![X0]: (top=join(complement(X0),X0))),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f26,f1080])).
% 132.00/17.23 fof(f1124,plain,(
% 132.00/17.23 top=join(zero,top)),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f254,f1110])).
% 132.00/17.23 fof(f1126,plain,(
% 132.00/17.23 ![X0]: (meet(complement(X0),X0)=complement(top))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f1110,f22])).
% 132.00/17.23 fof(f1139,plain,(
% 132.00/17.23 ![X0]: (meet(complement(X0),X0)=zero)),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f254,f1126])).
% 132.00/17.23 fof(f1169,plain,(
% 132.00/17.23 ![X0]: (join(X0,complement(X0))=join(complement(X0),top))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f281,f243])).
% 132.00/17.23 fof(f1171,plain,(
% 132.00/17.23 ![X0]: (join(X0,converse(top))=join(converse(complement(converse(complement(X0)))),top))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f240,f243])).
% 132.00/17.23 fof(f1172,plain,(
% 132.00/17.23 ![X0]: (join(X0,top)=join(complement(complement(X0)),top))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f30,f243])).
% 132.00/17.23 fof(f1196,plain,(
% 132.00/17.23 ![X0]: (top=join(complement(X0),top))),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f30,f1169])).
% 132.00/17.23 fof(f1199,plain,(
% 132.00/17.23 ![X0]: (join(X0,converse(top))=top)),
% 132.00/17.23 inference(backward_demodulation,[status(thm)],[f1216,f1171])).
% 132.00/17.23 fof(f1214,plain,(
% 132.00/17.23 ![X0]: (join(top,X0)=join(zero,top))),
% 132.00/17.23 inference(backward_demodulation,[status(thm)],[f1216,f933])).
% 132.00/17.23 fof(f1215,plain,(
% 132.00/17.23 ![X0,X1]: (top=join(complement(X0),join(X1,X0)))),
% 132.00/17.23 inference(backward_demodulation,[status(thm)],[f1216,f244])).
% 132.00/17.23 fof(f1216,plain,(
% 132.00/17.23 ![X0]: (join(X0,top)=top)),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f1196,f1172])).
% 132.00/17.23 fof(f1289,plain,(
% 132.00/17.23 ![X0]: (join(top,X0)=top)),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f1124,f1214])).
% 132.00/17.23 fof(f1299,plain,(
% 132.00/17.23 ![X0,X1,X2]: (join(meet(converse(composition(X0,X1)),X2),meet(composition(meet(converse(X1),composition(X2,converse(converse(X0)))),converse(X0)),X2))=meet(composition(meet(converse(X1),composition(X2,converse(converse(X0)))),converse(X0)),X2))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f28,f34])).
% 132.00/17.23 fof(f1325,plain,(
% 132.00/17.23 ![X0,X1,X2]: (join(meet(converse(composition(X0,X1)),X2),meet(composition(meet(converse(X1),composition(X2,X0)),converse(X0)),X2))=meet(composition(meet(converse(X1),composition(X2,converse(converse(X0)))),converse(X0)),X2))),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f26,f1299])).
% 132.00/17.23 fof(f1326,plain,(
% 132.00/17.23 ![X0,X1,X2]: (join(meet(converse(composition(X0,X1)),X2),meet(composition(meet(converse(X1),composition(X2,X0)),converse(X0)),X2))=meet(composition(meet(converse(X1),composition(X2,X0)),converse(X0)),X2))),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f26,f1325])).
% 132.00/17.23 fof(f1358,plain,(
% 132.00/17.23 ![X0]: (complement(X0)=join(zero,complement(join(complement(complement(X0)),X0))))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f1139,f45])).
% 132.00/17.23 fof(f1360,plain,(
% 132.00/17.23 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f31,f45])).
% 132.00/17.23 fof(f1361,plain,(
% 132.00/17.23 ![X0]: (X0=join(complement(complement(X0)),complement(join(complement(X0),X0))))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f408,f45])).
% 132.00/17.23 fof(f1362,plain,(
% 132.00/17.23 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f22,f45])).
% 132.00/17.23 fof(f1366,plain,(
% 132.00/17.23 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f30,f45])).
% 132.00/17.23 fof(f1370,plain,(
% 132.00/17.23 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(X1,complement(X0)))))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f19,f45])).
% 132.00/17.23 fof(f1385,plain,(
% 132.00/17.23 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f22,f1360])).
% 132.00/17.23 fof(f1386,plain,(
% 132.00/17.23 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f408,f1385])).
% 132.00/17.23 fof(f1387,plain,(
% 132.00/17.23 ![X0]: (X0=join(complement(complement(X0)),complement(top)))),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f1110,f1361])).
% 132.00/17.23 fof(f1388,plain,(
% 132.00/17.23 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f254,f1387])).
% 132.00/17.23 fof(f1392,plain,(
% 132.00/17.23 ![X0]: (X0=join(meet(X0,complement(complement(X0))),zero))),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f254,f1366])).
% 132.00/17.23 fof(f1439,plain,(
% 132.00/17.23 ![X0]: (X0=join(meet(X0,top),complement(top)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f1216,f45])).
% 132.00/17.23 fof(f1442,plain,(
% 132.00/17.23 ![X0]: (converse(top)=join(X0,converse(top)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f1216,f83])).
% 132.00/17.23 fof(f1457,plain,(
% 132.00/17.23 ![X0]: (X0=join(meet(X0,top),zero))),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f254,f1439])).
% 132.00/17.23 fof(f1471,plain,(
% 132.00/17.23 converse(top)=top),
% 132.00/17.23 inference(forward_demodulation,[status(thm)],[f1199,f1442])).
% 132.00/17.23 fof(f1494,plain,(
% 132.00/17.23 ![X0]: (converse(composition(X0,top))=composition(top,converse(X0)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f1471,f65])).
% 132.00/17.23 fof(f1624,plain,(
% 132.00/17.23 ![X0]: (complement(X0)=join(meet(complement(X0),zero),complement(X0)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f1388,f45])).
% 132.00/17.23 fof(f1634,plain,(
% 132.00/17.23 ![X0]: (X0=join(zero,meet(X0,top)))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f19,f1457])).
% 132.00/17.23 fof(f2006,plain,(
% 132.00/17.23 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f19,f1362])).
% 132.00/17.23 fof(f2213,plain,(
% 132.00/17.23 ![X0]: (top=join(complement(zero),X0))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f1388,f1215])).
% 132.00/17.23 fof(f2439,plain,(
% 132.00/17.23 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f22,f248])).
% 132.00/17.23 fof(f2445,plain,(
% 132.00/17.23 ![X0]: (meet(X0,top)=complement(join(zero,complement(X0))))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f254,f248])).
% 132.00/17.23 fof(f2504,plain,(
% 132.00/17.23 ![X0,X1]: (meet(join(complement(X0),zero),X1)=complement(join(meet(X0,top),complement(X1))))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f254,f250])).
% 132.00/17.23 fof(f2566,plain,(
% 132.00/17.23 top=complement(zero)),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f281,f2213])).
% 132.00/17.23 fof(f2581,plain,(
% 132.00/17.23 ![X0]: (meet(X0,zero)=complement(top))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f2213,f248])).
% 132.00/17.23 fof(f2583,plain,(
% 132.00/17.23 ![X0]: (meet(zero,X0)=complement(top))),
% 132.00/17.23 inference(paramodulation,[status(thm)],[f2213,f22])).
% 132.00/17.23 fof(f2623,plain,(
% 132.00/17.23 ![X0]: (complement(X0)=join(zero,complement(X0)))),
% 132.00/17.23 inference(backward_demodulation,[status(thm)],[f2632,f1624])).
% 132.00/17.24 fof(f2632,plain,(
% 132.00/17.24 ![X0]: (meet(X0,zero)=zero)),
% 132.00/17.24 inference(forward_demodulation,[status(thm)],[f254,f2581])).
% 132.00/17.24 fof(f2635,plain,(
% 132.00/17.24 ![X0]: (meet(zero,X0)=zero)),
% 132.00/17.24 inference(forward_demodulation,[status(thm)],[f254,f2583])).
% 132.00/17.24 fof(f2662,plain,(
% 132.00/17.24 ![X0]: (X0=complement(complement(X0)))),
% 132.00/17.24 inference(backward_demodulation,[status(thm)],[f2623,f1386])).
% 132.00/17.24 fof(f2669,plain,(
% 132.00/17.24 ![X0]: (complement(X0)=complement(join(complement(complement(X0)),X0)))),
% 132.00/17.24 inference(backward_demodulation,[status(thm)],[f2623,f1358])).
% 132.00/17.24 fof(f2671,plain,(
% 132.00/17.24 ![X0]: (meet(X0,top)=complement(complement(X0)))),
% 132.00/17.24 inference(backward_demodulation,[status(thm)],[f2623,f2445])).
% 132.00/17.24 fof(f2672,plain,(
% 132.00/17.24 ![X0]: (meet(top,X0)=complement(complement(X0)))),
% 132.00/17.24 inference(backward_demodulation,[status(thm)],[f2623,f259])).
% 132.00/17.24 fof(f2679,plain,(
% 132.00/17.24 ![X0]: (X0=join(meet(X0,X0),zero))),
% 132.00/17.24 inference(backward_demodulation,[status(thm)],[f2662,f1392])).
% 132.00/17.24 fof(f2750,plain,(
% 132.00/17.24 ![X0]: (complement(X0)=complement(join(X0,X0)))),
% 132.00/17.24 inference(forward_demodulation,[status(thm)],[f2662,f2669])).
% 132.00/17.24 fof(f2753,plain,(
% 132.00/17.24 ![X0]: (X0=join(zero,X0))),
% 132.00/17.24 inference(backward_demodulation,[status(thm)],[f2765,f1634])).
% 132.00/17.24 fof(f2755,plain,(
% 132.00/17.24 ![X0,X1]: (meet(join(complement(X0),zero),X1)=complement(join(X0,complement(X1))))),
% 132.00/17.24 inference(backward_demodulation,[status(thm)],[f2765,f2504])).
% 132.00/17.24 fof(f2765,plain,(
% 132.00/17.24 ![X0]: (meet(X0,top)=X0)),
% 132.00/17.24 inference(forward_demodulation,[status(thm)],[f2662,f2671])).
% 132.00/17.24 fof(f2766,plain,(
% 132.00/17.24 ![X0]: (meet(top,X0)=X0)),
% 132.00/17.24 inference(forward_demodulation,[status(thm)],[f2662,f2672])).
% 132.00/17.24 fof(f2777,plain,(
% 132.00/17.24 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 132.00/17.24 inference(forward_demodulation,[status(thm)],[f408,f2679])).
% 132.00/17.24 fof(f2784,plain,(
% 132.00/17.24 ![X0]: (composition(converse(X0),complement(composition(X0,top)))=zero)),
% 132.00/17.24 inference(backward_demodulation,[status(thm)],[f2789,f287])).
% 132.00/17.24 fof(f2789,plain,(
% 132.00/17.24 ![X0]: (X0=join(X0,zero))),
% 132.00/17.24 inference(forward_demodulation,[status(thm)],[f2662,f2777])).
% 132.00/17.24 fof(f2874,plain,(
% 132.00/17.24 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 132.00/17.24 inference(backward_demodulation,[status(thm)],[f2875,f1370])).
% 132.00/17.24 fof(f2875,plain,(
% 132.00/17.24 ![X0,X1]: (meet(complement(X0),X1)=complement(join(X0,complement(X1))))),
% 132.00/17.24 inference(forward_demodulation,[status(thm)],[f2789,f2755])).
% 132.00/17.24 fof(f3160,plain,(
% 132.00/17.24 ![X0]: (converse(converse(X0))=join(X0,converse(zero)))),
% 132.00/17.24 inference(paramodulation,[status(thm)],[f2789,f83])).
% 132.00/17.24 fof(f3182,plain,(
% 132.00/17.24 ![X0]: (X0=join(X0,converse(zero)))),
% 132.00/17.24 inference(forward_demodulation,[status(thm)],[f26,f3160])).
% 132.00/17.24 fof(f3334,plain,(
% 132.00/17.24 zero=converse(zero)),
% 132.00/17.24 inference(paramodulation,[status(thm)],[f2753,f3182])).
% 132.00/17.24 fof(f3482,plain,(
% 132.00/17.24 ![X0]: (join(X0,X0)=complement(complement(X0)))),
% 132.00/17.24 inference(paramodulation,[status(thm)],[f2750,f2662])).
% 132.00/17.24 fof(f3510,plain,(
% 132.00/17.24 ![X0]: (join(X0,X0)=X0)),
% 132.00/17.24 inference(forward_demodulation,[status(thm)],[f2662,f3482])).
% 132.00/17.24 fof(f3533,plain,(
% 132.00/17.24 ![X0,X1]: (join(X0,join(join(X1,X0),X1))=join(X1,X0))),
% 132.00/17.24 inference(paramodulation,[status(thm)],[f142,f3510])).
% 132.00/17.24 fof(f3539,plain,(
% 132.00/17.24 ![X0,X1]: (join(X0,join(join(X1,X0),X1))=join(X1,X0))),
% 132.00/17.24 inference(paramodulation,[status(thm)],[f53,f3510])).
% 132.00/17.24 fof(f3569,plain,(
% 132.00/17.24 ![X0,X1]: (join(X0,join(X0,join(X1,X1)))=join(X1,X0))),
% 132.00/17.24 inference(forward_demodulation,[status(thm)],[f142,f3533])).
% 132.00/17.24 fof(f3574,plain,(
% 132.00/17.24 ![X0,X1]: (join(X0,join(X0,X1))=join(X1,X0))),
% 132.00/17.24 inference(forward_demodulation,[status(thm)],[f3510,f3569])).
% 132.00/17.24 fof(f3577,plain,(
% 132.00/17.24 ![X0,X1]: (join(X0,join(X0,join(X1,X1)))=join(X1,X0))),
% 132.00/17.24 inference(forward_demodulation,[status(thm)],[f142,f3539])).
% 132.00/17.24 fof(f3578,plain,(
% 132.00/17.24 ![X0,X1]: (join(join(X0,X0),X1)=join(X0,X1))),
% 132.00/17.24 inference(forward_demodulation,[status(thm)],[f3574,f3577])).
% 132.00/17.24 fof(f3582,plain,(
% 132.00/17.24 ![X0,X1]: (join(X0,join(X1,X0))=join(X0,X1))),
% 132.00/17.24 inference(forward_demodulation,[status(thm)],[f142,f3578])).
% 132.00/17.24 fof(f5502,plain,(
% 132.00/17.24 ![X0,X1]: (join(meet(X0,X1),X0)=join(meet(X0,X1),meet(X0,complement(X1))))),
% 132.00/17.24 inference(paramodulation,[status(thm)],[f1362,f3582])).
% 132.00/17.24 fof(f5626,plain,(
% 132.00/17.24 ![X0,X1]: (join(meet(X0,X1),X0)=X0)),
% 132.00/17.24 inference(forward_demodulation,[status(thm)],[f2006,f5502])).
% 132.00/17.24 fof(f5780,plain,(
% 132.00/17.24 ![X0,X1]: (join(meet(X0,X1),X1)=X1)),
% 132.00/17.24 inference(paramodulation,[status(thm)],[f2439,f5626])).
% 132.00/17.24 fof(f5825,plain,(
% 132.00/17.24 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 132.00/17.24 inference(paramodulation,[status(thm)],[f19,f5780])).
% 132.00/17.24 fof(f10835,plain,(
% 132.00/17.24 ![X0,X1]: (X0=join(meet(X1,X0),meet(complement(X1),X0)))),
% 132.00/17.24 inference(paramodulation,[status(thm)],[f2439,f2874])).
% 132.00/17.24 fof(f23859,plain,(
% 132.00/17.24 converse(composition(top,top))=composition(top,top)),
% 132.00/17.24 inference(paramodulation,[status(thm)],[f1471,f1494])).
% 132.00/17.24 fof(f27095,plain,(
% 132.00/17.24 composition(top,complement(composition(top,top)))=zero),
% 132.00/17.24 inference(paramodulation,[status(thm)],[f1471,f2784])).
% 132.00/17.24 fof(f89940,plain,(
% 132.00/17.24 ![X0]: (join(meet(composition(top,top),X0),meet(composition(meet(converse(top),composition(X0,top)),converse(top)),X0))=meet(composition(meet(converse(top),composition(X0,top)),converse(top)),X0))),
% 132.00/17.24 inference(paramodulation,[status(thm)],[f23859,f1326])).
% 132.00/17.24 fof(f90065,plain,(
% 132.00/17.24 ![X0]: (join(meet(composition(top,top),X0),meet(composition(meet(top,composition(X0,top)),converse(top)),X0))=meet(composition(meet(converse(top),composition(X0,top)),converse(top)),X0))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f1471,f89940])).
% 132.00/17.25 fof(f90066,plain,(
% 132.00/17.25 ![X0]: (join(meet(composition(top,top),X0),meet(composition(composition(X0,top),converse(top)),X0))=meet(composition(meet(converse(top),composition(X0,top)),converse(top)),X0))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f2766,f90065])).
% 132.00/17.25 fof(f90067,plain,(
% 132.00/17.25 ![X0]: (join(meet(composition(top,top),X0),meet(composition(X0,composition(top,converse(top))),X0))=meet(composition(meet(converse(top),composition(X0,top)),converse(top)),X0))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f23,f90066])).
% 132.00/17.25 fof(f90068,plain,(
% 132.00/17.25 ![X0]: (join(meet(composition(top,top),X0),meet(composition(X0,converse(composition(top,top))),X0))=meet(composition(meet(converse(top),composition(X0,top)),converse(top)),X0))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f1494,f90067])).
% 132.00/17.25 fof(f90069,plain,(
% 132.00/17.25 ![X0]: (join(meet(composition(top,top),X0),meet(composition(X0,composition(top,top)),X0))=meet(composition(meet(converse(top),composition(X0,top)),converse(top)),X0))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f23859,f90068])).
% 132.00/17.25 fof(f90070,plain,(
% 132.00/17.25 ![X0]: (join(meet(composition(top,top),X0),meet(composition(X0,composition(top,top)),X0))=meet(composition(meet(top,composition(X0,top)),converse(top)),X0))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f1471,f90069])).
% 132.00/17.25 fof(f90071,plain,(
% 132.00/17.25 ![X0]: (join(meet(composition(top,top),X0),meet(composition(X0,composition(top,top)),X0))=meet(composition(composition(X0,top),converse(top)),X0))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f2766,f90070])).
% 132.00/17.25 fof(f90072,plain,(
% 132.00/17.25 ![X0]: (join(meet(composition(top,top),X0),meet(composition(X0,composition(top,top)),X0))=meet(composition(X0,composition(top,converse(top))),X0))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f23,f90071])).
% 132.00/17.25 fof(f90073,plain,(
% 132.00/17.25 ![X0]: (join(meet(composition(top,top),X0),meet(composition(X0,composition(top,top)),X0))=meet(composition(X0,converse(composition(top,top))),X0))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f1494,f90072])).
% 132.00/17.25 fof(f90074,plain,(
% 132.00/17.25 ![X0]: (join(meet(composition(top,top),X0),meet(composition(X0,composition(top,top)),X0))=meet(composition(X0,composition(top,top)),X0))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f23859,f90073])).
% 132.00/17.25 fof(f95166,plain,(
% 132.00/17.25 ![X0,X1]: (join(X0,composition(join(X1,top),complement(composition(top,top))))=join(zero,join(X0,composition(X1,complement(composition(top,top))))))),
% 132.00/17.25 inference(paramodulation,[status(thm)],[f27095,f144])).
% 132.00/17.25 fof(f95183,plain,(
% 132.00/17.25 ![X0]: (join(meet(composition(complement(composition(top,top)),X0),converse(top)),meet(composition(complement(composition(top,top)),meet(X0,converse(zero))),converse(top)))=meet(composition(complement(composition(top,top)),meet(X0,converse(composition(top,complement(composition(top,top)))))),converse(top)))),
% 132.00/17.25 inference(paramodulation,[status(thm)],[f27095,f388])).
% 132.00/17.25 fof(f95214,plain,(
% 132.00/17.25 ![X0,X1]: (composition(join(composition(X0,top),X1),complement(composition(top,top)))=join(composition(X0,zero),composition(X1,complement(composition(top,top)))))),
% 132.00/17.25 inference(paramodulation,[status(thm)],[f27095,f130])).
% 132.00/17.25 fof(f95215,plain,(
% 132.00/17.25 ![X0]: (composition(join(top,X0),complement(composition(top,top)))=join(composition(X0,complement(composition(top,top))),zero))),
% 132.00/17.25 inference(paramodulation,[status(thm)],[f27095,f127])).
% 132.00/17.25 fof(f95258,plain,(
% 132.00/17.25 ![X0,X1]: (join(X0,composition(top,complement(composition(top,top))))=join(zero,join(X0,composition(X1,complement(composition(top,top))))))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f1216,f95166])).
% 132.00/17.25 fof(f95259,plain,(
% 132.00/17.25 ![X0,X1]: (join(X0,zero)=join(zero,join(X0,composition(X1,complement(composition(top,top))))))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f27095,f95258])).
% 132.00/17.25 fof(f95260,plain,(
% 132.00/17.25 ![X0,X1]: (X0=join(zero,join(X0,composition(X1,complement(composition(top,top))))))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f2789,f95259])).
% 132.00/17.25 fof(f95261,plain,(
% 132.00/17.25 ![X0,X1]: (X0=join(X0,composition(X1,complement(composition(top,top)))))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f2753,f95260])).
% 132.00/17.25 fof(f95321,plain,(
% 132.00/17.25 ![X0]: (join(meet(composition(complement(composition(top,top)),X0),top),meet(composition(complement(composition(top,top)),meet(X0,converse(zero))),converse(top)))=meet(composition(complement(composition(top,top)),meet(X0,converse(composition(top,complement(composition(top,top)))))),converse(top)))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f1471,f95183])).
% 132.00/17.25 fof(f95322,plain,(
% 132.00/17.25 ![X0]: (join(composition(complement(composition(top,top)),X0),meet(composition(complement(composition(top,top)),meet(X0,converse(zero))),converse(top)))=meet(composition(complement(composition(top,top)),meet(X0,converse(composition(top,complement(composition(top,top)))))),converse(top)))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f2765,f95321])).
% 132.00/17.25 fof(f95323,plain,(
% 132.00/17.25 ![X0]: (join(composition(complement(composition(top,top)),X0),meet(composition(complement(composition(top,top)),meet(X0,zero)),converse(top)))=meet(composition(complement(composition(top,top)),meet(X0,converse(composition(top,complement(composition(top,top)))))),converse(top)))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f3334,f95322])).
% 132.00/17.25 fof(f95324,plain,(
% 132.00/17.25 ![X0]: (join(composition(complement(composition(top,top)),X0),meet(composition(complement(composition(top,top)),zero),converse(top)))=meet(composition(complement(composition(top,top)),meet(X0,converse(composition(top,complement(composition(top,top)))))),converse(top)))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f2632,f95323])).
% 132.00/17.25 fof(f95325,plain,(
% 132.00/17.25 ![X0]: (join(composition(complement(composition(top,top)),X0),meet(composition(complement(composition(top,top)),zero),top))=meet(composition(complement(composition(top,top)),meet(X0,converse(composition(top,complement(composition(top,top)))))),converse(top)))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f1471,f95324])).
% 132.00/17.25 fof(f95326,plain,(
% 132.00/17.25 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(complement(composition(top,top)),zero))=meet(composition(complement(composition(top,top)),meet(X0,converse(composition(top,complement(composition(top,top)))))),converse(top)))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f2765,f95325])).
% 132.00/17.25 fof(f95327,plain,(
% 132.00/17.25 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(complement(composition(top,top)),zero))=meet(composition(complement(composition(top,top)),meet(X0,converse(zero))),converse(top)))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f27095,f95326])).
% 132.00/17.25 fof(f95328,plain,(
% 132.00/17.25 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(complement(composition(top,top)),zero))=meet(composition(complement(composition(top,top)),meet(X0,zero)),converse(top)))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f3334,f95327])).
% 132.00/17.25 fof(f95329,plain,(
% 132.00/17.25 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(complement(composition(top,top)),zero))=meet(composition(complement(composition(top,top)),zero),converse(top)))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f2632,f95328])).
% 132.00/17.25 fof(f95330,plain,(
% 132.00/17.25 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(complement(composition(top,top)),zero))=meet(composition(complement(composition(top,top)),zero),top))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f1471,f95329])).
% 132.00/17.25 fof(f95331,plain,(
% 132.00/17.25 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(complement(composition(top,top)),zero))=composition(complement(composition(top,top)),zero))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f2765,f95330])).
% 132.00/17.25 fof(f95470,plain,(
% 132.00/17.25 ![X0,X1]: (composition(join(composition(X0,top),X1),complement(composition(top,top)))=composition(X0,zero))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f95261,f95214])).
% 132.00/17.25 fof(f95471,plain,(
% 132.00/17.25 ![X0]: (composition(top,complement(composition(top,top)))=join(composition(X0,complement(composition(top,top))),zero))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f1289,f95215])).
% 132.00/17.25 fof(f95472,plain,(
% 132.00/17.25 ![X0]: (zero=join(composition(X0,complement(composition(top,top))),zero))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f27095,f95471])).
% 132.00/17.25 fof(f95475,plain,(
% 132.00/17.25 ![X0]: (zero=composition(X0,zero))),
% 132.00/17.25 inference(backward_demodulation,[status(thm)],[f95482,f95470])).
% 132.00/17.25 fof(f95482,plain,(
% 132.00/17.25 ![X0]: (zero=composition(X0,complement(composition(top,top))))),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f2789,f95472])).
% 132.00/17.25 fof(f95665,plain,(
% 132.00/17.25 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(complement(composition(top,top)),zero))=zero)),
% 132.00/17.25 inference(backward_demodulation,[status(thm)],[f95475,f95331])).
% 132.00/17.25 fof(f96210,plain,(
% 132.00/17.25 ![X0]: (join(composition(complement(composition(top,top)),X0),zero)=zero)),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f95475,f95665])).
% 132.00/17.25 fof(f96215,plain,(
% 132.00/17.25 ![X0]: (composition(complement(composition(top,top)),X0)=zero)),
% 132.00/17.25 inference(forward_demodulation,[status(thm)],[f2789,f96210])).
% 132.00/17.25 fof(f102249,plain,(
% 132.00/17.25 complement(composition(top,top))=zero),
% 132.00/17.25 inference(paramodulation,[status(thm)],[f24,f96215])).
% 132.00/17.25 fof(f103728,plain,(
% 125.28/17.39 ![X0]: (X0=join(meet(composition(top,top),X0),meet(zero,X0)))),
% 125.28/17.39 inference(paramodulation,[status(thm)],[f102249,f10835])).
% 125.28/17.39 fof(f103742,plain,(
% 125.28/17.39 composition(top,top)=complement(zero)),
% 125.28/17.39 inference(paramodulation,[status(thm)],[f102249,f2662])).
% 125.28/17.39 fof(f103843,plain,(
% 125.28/17.39 ![X0]: (X0=join(meet(composition(top,top),X0),zero))),
% 125.28/17.39 inference(forward_demodulation,[status(thm)],[f2635,f103728])).
% 125.28/17.39 fof(f103863,plain,(
% 125.28/17.39 ![X0]: (join(X0,meet(composition(X0,composition(top,top)),X0))=meet(composition(X0,composition(top,top)),X0))),
% 125.28/17.39 inference(backward_demodulation,[status(thm)],[f103864,f90074])).
% 125.28/17.39 fof(f103864,plain,(
% 125.28/17.39 ![X0]: (X0=meet(composition(top,top),X0))),
% 125.28/17.39 inference(forward_demodulation,[status(thm)],[f2789,f103843])).
% 125.28/17.39 fof(f103923,plain,(
% 125.28/17.39 composition(top,top)=top),
% 125.28/17.39 inference(forward_demodulation,[status(thm)],[f2566,f103742])).
% 125.28/17.39 fof(f104046,plain,(
% 125.28/17.39 ![X0]: (X0=meet(composition(X0,composition(top,top)),X0))),
% 125.28/17.39 inference(forward_demodulation,[status(thm)],[f5825,f103863])).
% 125.28/17.39 fof(f104047,plain,(
% 125.28/17.39 ![X0]: (X0=meet(composition(X0,top),X0))),
% 125.28/17.39 inference(forward_demodulation,[status(thm)],[f103923,f104046])).
% 125.28/17.39 fof(f104696,plain,(
% 125.28/17.39 ![X0]: (X0=meet(X0,composition(X0,top)))),
% 125.28/17.39 inference(paramodulation,[status(thm)],[f2439,f104047])).
% 125.28/17.39 fof(f104719,plain,(
% 125.28/17.39 ![X0]: (join(X0,composition(meet(X0,composition(X0,converse(top))),meet(top,composition(converse(X0),X0))))=composition(meet(X0,composition(X0,converse(top))),meet(top,composition(converse(X0),X0))))),
% 125.28/17.39 inference(paramodulation,[status(thm)],[f104047,f32])).
% 125.28/17.39 fof(f104927,plain,(
% 125.28/17.39 ![X0]: (join(X0,composition(meet(X0,composition(X0,top)),meet(top,composition(converse(X0),X0))))=composition(meet(X0,composition(X0,converse(top))),meet(top,composition(converse(X0),X0))))),
% 125.28/17.39 inference(forward_demodulation,[status(thm)],[f1471,f104719])).
% 125.28/17.39 fof(f104928,plain,(
% 125.28/17.39 ![X0]: (join(X0,composition(X0,meet(top,composition(converse(X0),X0))))=composition(meet(X0,composition(X0,converse(top))),meet(top,composition(converse(X0),X0))))),
% 125.28/17.39 inference(forward_demodulation,[status(thm)],[f104696,f104927])).
% 125.28/17.39 fof(f104929,plain,(
% 125.28/17.39 ![X0]: (join(X0,composition(X0,composition(converse(X0),X0)))=composition(meet(X0,composition(X0,converse(top))),meet(top,composition(converse(X0),X0))))),
% 125.28/17.39 inference(forward_demodulation,[status(thm)],[f2766,f104928])).
% 125.28/17.39 fof(f104930,plain,(
% 125.28/17.39 ![X0]: (join(X0,composition(X0,composition(converse(X0),X0)))=composition(meet(X0,composition(X0,top)),meet(top,composition(converse(X0),X0))))),
% 125.28/17.39 inference(forward_demodulation,[status(thm)],[f1471,f104929])).
% 125.28/17.39 fof(f104931,plain,(
% 125.28/17.39 ![X0]: (join(X0,composition(X0,composition(converse(X0),X0)))=composition(X0,meet(top,composition(converse(X0),X0))))),
% 125.28/17.39 inference(forward_demodulation,[status(thm)],[f104696,f104930])).
% 125.28/17.39 fof(f104932,plain,(
% 125.28/17.39 ~composition(sK0_skl,composition(converse(sK0_skl),sK0_skl))=composition(sK0_skl,composition(converse(sK0_skl),sK0_skl))),
% 125.28/17.39 inference(backward_demodulation,[status(thm)],[f104933,f47])).
% 125.28/17.39 fof(f104933,plain,(
% 125.28/17.39 ![X0]: (join(X0,composition(X0,composition(converse(X0),X0)))=composition(X0,composition(converse(X0),X0)))),
% 125.28/17.39 inference(forward_demodulation,[status(thm)],[f2766,f104931])).
% 125.28/17.39 fof(f105168,plain,(
% 125.28/17.39 $false),
% 125.28/17.39 inference(trivial_equality_resolution,[status(thm)],[f104932])).
% 125.28/17.39 % SZS output end CNFRefutation for theBenchmark.p
% 25.48/17.57 % Elapsed time: 17.153702 seconds
% 25.48/17.57 % CPU time: 134.843839 seconds
% 25.48/17.57 % Total memory used: 805.489 MB
% 25.48/17.57 % Net memory used: 790.380 MB
%------------------------------------------------------------------------------