%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL011+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 : n002.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:33 PM UTC 2026
% Result : Theorem 15.50s 2.35s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL011+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n002.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 04:01:35 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.35 % Drodi V4.1.1
% 15.50/2.35 % Refutation found
% 15.50/2.35 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.50/2.35 % SZS output start CNFRefutation for theBenchmark
% 15.50/2.35 fof(f1,axiom,(
% 15.50/2.35 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 15.50/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.50/2.35 fof(f2,axiom,(
% 15.50/2.35 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 15.50/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.50/2.35 fof(f3,axiom,(
% 15.50/2.35 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 15.50/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.50/2.35 fof(f4,axiom,(
% 15.50/2.35 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 15.50/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.50/2.35 fof(f6,axiom,(
% 15.50/2.35 (! [X0] : composition(X0,one) = X0 )),
% 15.50/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.50/2.35 fof(f7,axiom,(
% 15.50/2.35 (! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) )),
% 15.50/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.50/2.35 fof(f8,axiom,(
% 15.50/2.35 (! [X0] : converse(converse(X0)) = X0 )),
% 15.50/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.50/2.35 fof(f9,axiom,(
% 15.50/2.35 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 15.50/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.50/2.35 fof(f10,axiom,(
% 15.50/2.35 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 15.50/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.50/2.35 fof(f11,axiom,(
% 15.50/2.35 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 15.50/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.50/2.35 fof(f12,axiom,(
% 15.50/2.35 (! [X0] : top = join(X0,complement(X0)) )),
% 15.50/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.50/2.35 fof(f13,axiom,(
% 15.50/2.35 (! [X0] : zero = meet(X0,complement(X0)) )),
% 15.50/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.50/2.35 fof(f14,axiom,(
% 15.50/2.35 (! [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))) )),
% 15.50/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.50/2.35 fof(f17,conjecture,(
% 15.50/2.35 (! [X0,X1,X2] :( meet(X0,composition(converse(X1),X2)) = zero=> meet(composition(X1,X0),X2) = zero ) )),
% 15.50/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.50/2.35 fof(f18,negated_conjecture,(
% 15.50/2.35 ~((! [X0,X1,X2] :( meet(X0,composition(converse(X1),X2)) = zero=> meet(composition(X1,X0),X2) = zero ) ))),
% 15.50/2.35 inference(negated_conjecture,[status(cth)],[f17])).
% 15.50/2.35 fof(f19,plain,(
% 15.50/2.35 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 15.50/2.35 inference(cnf_transformation,[status(thm)],[f1])).
% 15.50/2.35 fof(f20,plain,(
% 15.50/2.35 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 15.50/2.35 inference(cnf_transformation,[status(thm)],[f2])).
% 15.50/2.35 fof(f21,plain,(
% 15.50/2.35 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 15.50/2.35 inference(cnf_transformation,[status(thm)],[f3])).
% 15.50/2.35 fof(f22,plain,(
% 15.50/2.35 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 15.50/2.35 inference(cnf_transformation,[status(thm)],[f4])).
% 15.50/2.35 fof(f24,plain,(
% 15.50/2.35 ![X0]: (composition(X0,one)=X0)),
% 15.50/2.35 inference(cnf_transformation,[status(thm)],[f6])).
% 15.50/2.35 fof(f25,plain,(
% 15.50/2.35 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 15.50/2.35 inference(cnf_transformation,[status(thm)],[f7])).
% 15.50/2.35 fof(f26,plain,(
% 15.50/2.35 ![X0]: (converse(converse(X0))=X0)),
% 15.50/2.35 inference(cnf_transformation,[status(thm)],[f8])).
% 15.50/2.35 fof(f27,plain,(
% 15.50/2.35 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 15.50/2.35 inference(cnf_transformation,[status(thm)],[f9])).
% 15.50/2.35 fof(f28,plain,(
% 15.50/2.35 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 15.50/2.35 inference(cnf_transformation,[status(thm)],[f10])).
% 15.50/2.35 fof(f29,plain,(
% 15.50/2.35 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 15.50/2.35 inference(cnf_transformation,[status(thm)],[f11])).
% 15.50/2.35 fof(f30,plain,(
% 15.50/2.35 ![X0]: (top=join(X0,complement(X0)))),
% 15.50/2.35 inference(cnf_transformation,[status(thm)],[f12])).
% 15.50/2.35 fof(f31,plain,(
% 15.50/2.35 ![X0]: (zero=meet(X0,complement(X0)))),
% 15.50/2.35 inference(cnf_transformation,[status(thm)],[f13])).
% 15.50/2.35 fof(f32,plain,(
% 15.50/2.35 ![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))))),
% 15.50/2.35 inference(cnf_transformation,[status(thm)],[f14])).
% 15.50/2.35 fof(f35,plain,(
% 15.50/2.35 (?[X0,X1,X2]: (meet(X0,composition(converse(X1),X2))=zero&~meet(composition(X1,X0),X2)=zero))),
% 15.50/2.35 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 15.50/2.35 fof(f36,plain,(
% 15.50/2.35 (meet(sK0_skl,composition(converse(sK1_skl),sK2_skl))=zero&~meet(composition(sK1_skl,sK0_skl),sK2_skl)=zero)),
% 15.50/2.35 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)],[f35])).
% 15.50/2.35 fof(f37,plain,(
% 15.50/2.35 meet(sK0_skl,composition(converse(sK1_skl),sK2_skl))=zero),
% 15.50/2.35 inference(cnf_transformation,[status(thm)],[f36])).
% 15.50/2.35 fof(f38,plain,(
% 15.50/2.35 ~meet(composition(sK1_skl,sK0_skl),sK2_skl)=zero),
% 15.50/2.35 inference(cnf_transformation,[status(thm)],[f36])).
% 15.50/2.35 fof(f42,plain,(
% 15.50/2.35 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 15.50/2.35 inference(forward_demodulation,[status(thm)],[f19,f21])).
% 15.50/2.35 fof(f43,plain,(
% 15.50/2.35 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 15.50/2.35 inference(backward_demodulation,[status(thm)],[f22,f42])).
% 15.50/2.35 fof(f44,plain,(
% 15.50/2.35 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 15.50/2.35 inference(forward_demodulation,[status(thm)],[f19,f29])).
% 15.50/2.35 fof(f45,plain,(
% 15.50/2.35 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 15.50/2.35 inference(forward_demodulation,[status(thm)],[f19,f43])).
% 15.50/2.35 fof(f50,plain,(
% 15.50/2.35 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 15.50/2.35 inference(paramodulation,[status(thm)],[f26,f27])).
% 15.50/2.35 fof(f53,plain,(
% 15.50/2.35 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f26,f28])).
% 15.50/2.36 fof(f409,plain,(
% 15.50/2.36 join(meet(composition(sK1_skl,sK0_skl),sK2_skl),composition(meet(sK1_skl,composition(sK2_skl,converse(sK0_skl))),zero))=composition(meet(sK1_skl,composition(sK2_skl,converse(sK0_skl))),meet(sK0_skl,composition(converse(sK1_skl),sK2_skl)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f37,f32])).
% 15.50/2.36 fof(f453,plain,(
% 15.50/2.36 join(meet(composition(sK1_skl,sK0_skl),sK2_skl),composition(meet(sK1_skl,composition(sK2_skl,converse(sK0_skl))),zero))=composition(meet(sK1_skl,composition(sK2_skl,converse(sK0_skl))),zero)),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f37,f409])).
% 15.50/2.36 fof(f528,plain,(
% 15.50/2.36 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f30,f50])).
% 15.50/2.36 fof(f540,plain,(
% 15.50/2.36 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f24,f53])).
% 15.50/2.36 fof(f551,plain,(
% 15.50/2.36 ![X0]: (X0=composition(converse(one),X0))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f26,f540])).
% 15.50/2.36 fof(f552,plain,(
% 15.50/2.36 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f30,f22])).
% 15.50/2.36 fof(f557,plain,(
% 15.50/2.36 zero=complement(top)),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f31,f552])).
% 15.50/2.36 fof(f560,plain,(
% 15.50/2.36 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f557,f22])).
% 15.50/2.36 fof(f561,plain,(
% 15.50/2.36 top=join(top,zero)),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f557,f30])).
% 15.50/2.36 fof(f564,plain,(
% 15.50/2.36 top=join(zero,top)),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f19,f561])).
% 15.50/2.36 fof(f568,plain,(
% 15.50/2.36 one=converse(one)),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f24,f551])).
% 15.50/2.36 fof(f586,plain,(
% 15.50/2.36 ![X0]: (X0=composition(one,X0))),
% 15.50/2.36 inference(backward_demodulation,[status(thm)],[f568,f551])).
% 15.50/2.36 fof(f681,plain,(
% 15.50/2.36 ![X0]: (top=join(join(zero,complement(X0)),meet(top,X0)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f560,f30])).
% 15.50/2.36 fof(f690,plain,(
% 15.50/2.36 ![X0]: (top=join(zero,join(complement(X0),meet(top,X0))))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f20,f681])).
% 15.50/2.36 fof(f736,plain,(
% 15.50/2.36 ![X0]: (converse(join(one,X0))=join(one,converse(X0)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f568,f50])).
% 15.50/2.36 fof(f800,plain,(
% 15.50/2.36 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f31,f45])).
% 15.50/2.36 fof(f802,plain,(
% 15.50/2.36 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f30,f45])).
% 15.50/2.36 fof(f811,plain,(
% 15.50/2.36 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f22,f800])).
% 15.50/2.36 fof(f813,plain,(
% 15.50/2.36 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(X0)))))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f19,f802])).
% 15.50/2.36 fof(f814,plain,(
% 15.50/2.36 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f557,f813])).
% 15.50/2.36 fof(f876,plain,(
% 15.50/2.36 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f27,f19])).
% 15.50/2.36 fof(f886,plain,(
% 15.50/2.36 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f19,f22])).
% 15.50/2.36 fof(f938,plain,(
% 15.50/2.36 ![X0,X1]: (join(X0,join(X1,complement(join(X0,X1))))=top)),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f30,f20])).
% 15.50/2.36 fof(f942,plain,(
% 15.50/2.36 ![X0,X1]: (join(zero,join(meet(X0,complement(complement(X0))),X1))=join(X0,X1))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f814,f20])).
% 15.50/2.36 fof(f943,plain,(
% 15.50/2.36 ![X0,X1]: (join(zero,join(meet(X0,X0),X1))=join(X0,X1))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f811,f20])).
% 15.50/2.36 fof(f953,plain,(
% 15.50/2.36 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f30,f20])).
% 15.50/2.36 fof(f970,plain,(
% 15.50/2.36 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X1,X2),composition(X0,X2)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f19,f25])).
% 15.50/2.36 fof(f980,plain,(
% 15.50/2.36 ![X0,X1]: (composition(join(X0,one),X1)=join(composition(X0,X1),X1))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f586,f25])).
% 15.50/2.36 fof(f1002,plain,(
% 15.50/2.36 ![X0,X1]: (composition(join(X0,one),X1)=join(X1,composition(X0,X1)))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f19,f980])).
% 15.50/2.36 fof(f1021,plain,(
% 15.50/2.36 ![X0]: (join(meet(composition(sK1_skl,sK0_skl),sK2_skl),join(composition(meet(sK1_skl,composition(sK2_skl,converse(sK0_skl))),zero),X0))=join(composition(meet(sK1_skl,composition(sK2_skl,converse(sK0_skl))),zero),X0))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f453,f20])).
% 15.50/2.36 fof(f1113,plain,(
% 15.50/2.36 ![X0]: (join(zero,top)=join(X0,complement(meet(X0,X0))))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f30,f943])).
% 15.50/2.36 fof(f1114,plain,(
% 15.50/2.36 ![X0,X1]: (join(zero,join(X0,meet(X1,X1)))=join(X1,X0))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f19,f943])).
% 15.50/2.36 fof(f1130,plain,(
% 15.50/2.36 ![X0]: (top=join(X0,complement(meet(X0,X0))))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f564,f1113])).
% 15.50/2.36 fof(f1151,plain,(
% 15.50/2.36 ![X0,X1]: (converse(join(X0,X1))=converse(join(X1,X0)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f27,f876])).
% 15.50/2.36 fof(f1299,plain,(
% 15.50/2.36 ![X0,X1]: (join(X0,meet(X1,complement(complement(X1))))=join(X1,meet(X0,X0)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f1114,f942])).
% 15.50/2.36 fof(f1308,plain,(
% 15.50/2.36 ![X0,X1]: (join(zero,join(X0,meet(X1,complement(complement(X1)))))=join(X1,X0))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f19,f942])).
% 15.50/2.36 fof(f1320,plain,(
% 15.50/2.36 ![X0]: (X0=join(X0,meet(zero,zero)))),
% 15.50/2.36 inference(backward_demodulation,[status(thm)],[f1299,f814])).
% 15.50/2.36 fof(f1363,plain,(
% 15.50/2.36 top=join(top,complement(complement(complement(top))))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f690,f1308])).
% 15.50/2.36 fof(f1378,plain,(
% 15.50/2.36 top=join(top,complement(complement(zero)))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f557,f1363])).
% 15.50/2.36 fof(f1390,plain,(
% 15.50/2.36 ![X0]: (join(top,join(complement(complement(zero)),X0))=join(top,X0))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f1378,f20])).
% 15.50/2.36 fof(f1792,plain,(
% 15.50/2.36 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f22,f886])).
% 15.50/2.36 fof(f1809,plain,(
% 15.50/2.36 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f886,f45])).
% 15.50/2.36 fof(f1831,plain,(
% 15.50/2.36 ~meet(sK2_skl,composition(sK1_skl,sK0_skl))=zero),
% 15.50/2.36 inference(backward_demodulation,[status(thm)],[f1792,f38])).
% 15.50/2.36 fof(f1878,plain,(
% 15.50/2.36 ![X0]: (join(meet(sK2_skl,composition(sK1_skl,sK0_skl)),join(composition(meet(sK1_skl,composition(sK2_skl,converse(sK0_skl))),zero),X0))=join(composition(meet(sK1_skl,composition(sK2_skl,converse(sK0_skl))),zero),X0))),
% 15.50/2.36 inference(backward_demodulation,[status(thm)],[f1792,f1021])).
% 15.50/2.36 fof(f1916,plain,(
% 15.50/2.36 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f19,f1809])).
% 15.50/2.36 fof(f2051,plain,(
% 15.50/2.36 ![X0,X1]: (join(X0,join(top,X1))=join(top,join(complement(complement(X0)),X1)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f953,f953])).
% 15.50/2.36 fof(f2053,plain,(
% 15.50/2.36 ![X0]: (join(X0,converse(top))=join(top,converse(complement(converse(complement(X0))))))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f528,f953])).
% 15.50/2.36 fof(f2070,plain,(
% 15.50/2.36 ![X0,X1]: (X0=join(meet(X0,join(complement(complement(X0)),X1)),complement(join(top,X1))))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f953,f45])).
% 15.50/2.36 fof(f2091,plain,(
% 15.50/2.36 ![X0]: (join(zero,join(top,X0))=join(top,X0))),
% 15.50/2.36 inference(backward_demodulation,[status(thm)],[f2051,f1390])).
% 15.50/2.36 fof(f2113,plain,(
% 15.50/2.36 ![X0,X1]: (X0=join(complement(join(top,X1)),meet(X0,join(complement(complement(X0)),X1))))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f19,f2070])).
% 15.50/2.36 fof(f2133,plain,(
% 15.50/2.36 ![X0,X1]: (X0=join(meet(X1,X0),meet(complement(X1),X0)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f1792,f1916])).
% 15.50/2.36 fof(f2155,plain,(
% 15.50/2.36 ![X0]: (complement(complement(X0))=join(meet(X0,complement(complement(X0))),zero))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f31,f2133])).
% 15.50/2.36 fof(f2173,plain,(
% 15.50/2.36 ![X0]: (complement(complement(X0))=join(zero,meet(X0,complement(complement(X0)))))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f19,f2155])).
% 15.50/2.36 fof(f2174,plain,(
% 15.50/2.36 ![X0]: (complement(complement(X0))=join(X0,meet(zero,zero)))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f1299,f2173])).
% 15.50/2.36 fof(f2200,plain,(
% 15.50/2.36 ![X0,X1]: (X0=join(complement(join(top,X1)),meet(X0,join(X0,X1))))),
% 15.50/2.36 inference(backward_demodulation,[status(thm)],[f2212,f2113])).
% 15.50/2.36 fof(f2212,plain,(
% 15.50/2.36 ![X0]: (complement(complement(X0))=X0)),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f1320,f2174])).
% 15.50/2.36 fof(f2268,plain,(
% 15.50/2.36 complement(zero)=top),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f557,f2212])).
% 15.50/2.36 fof(f2272,plain,(
% 15.50/2.36 ![X0,X1]: (complement(meet(X0,X1))=join(complement(X1),complement(X0)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f886,f2212])).
% 15.50/2.36 fof(f2642,plain,(
% 15.50/2.36 join(zero,converse(top))=join(top,converse(complement(converse(top))))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f528,f2091])).
% 15.50/2.36 fof(f2664,plain,(
% 15.50/2.36 join(zero,converse(top))=converse(top)),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f528,f2642])).
% 15.50/2.36 fof(f2753,plain,(
% 15.50/2.36 ![X0]: (complement(meet(zero,X0))=join(complement(X0),top))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f2268,f2272])).
% 15.50/2.36 fof(f2756,plain,(
% 15.50/2.36 ![X0,X1]: (join(X0,complement(meet(X1,X0)))=join(top,complement(X1)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f2272,f953])).
% 15.50/2.36 fof(f2780,plain,(
% 15.50/2.36 ![X0]: (complement(meet(zero,X0))=join(top,complement(X0)))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f19,f2753])).
% 15.50/2.36 fof(f2783,plain,(
% 15.50/2.36 ![X0]: (top=complement(meet(zero,X0)))),
% 15.50/2.36 inference(backward_demodulation,[status(thm)],[f2784,f1130])).
% 15.50/2.36 fof(f2784,plain,(
% 15.50/2.36 ![X0,X1]: (join(X0,complement(meet(X1,X0)))=complement(meet(zero,X1)))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f2780,f2756])).
% 15.50/2.36 fof(f2804,plain,(
% 15.50/2.36 ![X0]: (top=join(top,complement(X0)))),
% 15.50/2.36 inference(backward_demodulation,[status(thm)],[f2783,f2780])).
% 15.50/2.36 fof(f2809,plain,(
% 15.50/2.36 ![X0]: (top=join(top,X0))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f2212,f2804])).
% 15.50/2.36 fof(f2827,plain,(
% 15.50/2.36 ![X0]: (join(X0,converse(top))=top)),
% 15.50/2.36 inference(backward_demodulation,[status(thm)],[f2809,f2053])).
% 15.50/2.36 fof(f2847,plain,(
% 15.50/2.36 ![X0,X1]: (X0=join(complement(top),meet(X0,join(X0,X1))))),
% 15.50/2.36 inference(backward_demodulation,[status(thm)],[f2809,f2200])).
% 15.50/2.36 fof(f2862,plain,(
% 15.50/2.36 top=converse(top)),
% 15.50/2.36 inference(backward_demodulation,[status(thm)],[f2827,f2664])).
% 15.50/2.36 fof(f2870,plain,(
% 15.50/2.36 ![X0,X1]: (X0=join(zero,meet(X0,join(X0,X1))))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f557,f2847])).
% 15.50/2.36 fof(f2871,plain,(
% 15.50/2.36 ![X0]: (top=join(X0,converse(complement(converse(X0)))))),
% 15.50/2.36 inference(backward_demodulation,[status(thm)],[f2862,f528])).
% 15.50/2.36 fof(f3255,plain,(
% 15.50/2.36 ![X0]: (join(meet(sK2_skl,composition(sK1_skl,sK0_skl)),composition(join(meet(sK1_skl,composition(sK2_skl,converse(sK0_skl))),X0),zero))=join(composition(meet(sK1_skl,composition(sK2_skl,converse(sK0_skl))),zero),composition(X0,zero)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f25,f1878])).
% 15.50/2.36 fof(f3266,plain,(
% 15.50/2.36 ![X0]: (join(meet(sK2_skl,composition(sK1_skl,sK0_skl)),composition(join(meet(sK1_skl,composition(sK2_skl,converse(sK0_skl))),X0),zero))=composition(join(meet(sK1_skl,composition(sK2_skl,converse(sK0_skl))),X0),zero))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f25,f3255])).
% 15.50/2.36 fof(f3287,plain,(
% 15.50/2.36 ![X0]: (join(meet(sK2_skl,composition(sK1_skl,sK0_skl)),composition(top,zero))=composition(join(meet(sK1_skl,composition(sK2_skl,converse(sK0_skl))),join(X0,complement(join(meet(sK1_skl,composition(sK2_skl,converse(sK0_skl))),X0)))),zero))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f938,f3266])).
% 15.50/2.36 fof(f3303,plain,(
% 15.50/2.36 ![X0]: (join(composition(top,zero),meet(sK2_skl,composition(sK1_skl,sK0_skl)))=composition(join(meet(sK1_skl,composition(sK2_skl,converse(sK0_skl))),join(X0,complement(join(meet(sK1_skl,composition(sK2_skl,converse(sK0_skl))),X0)))),zero))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f19,f3287])).
% 15.50/2.36 fof(f3304,plain,(
% 15.50/2.36 join(composition(top,zero),meet(sK2_skl,composition(sK1_skl,sK0_skl)))=composition(top,zero)),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f938,f3303])).
% 15.50/2.36 fof(f3364,plain,(
% 15.50/2.36 ![X0]: (complement(top)=meet(zero,X0))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f2783,f2212])).
% 15.50/2.36 fof(f3365,plain,(
% 15.50/2.36 ![X0,X1]: (X0=join(meet(meet(zero,X1),X0),meet(top,X0)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f2783,f2133])).
% 15.50/2.36 fof(f3380,plain,(
% 15.50/2.36 ![X0]: (X0=join(X0,zero))),
% 15.50/2.36 inference(backward_demodulation,[status(thm)],[f3392,f1320])).
% 15.50/2.36 fof(f3392,plain,(
% 15.50/2.36 ![X0]: (zero=meet(zero,X0))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f557,f3364])).
% 15.50/2.36 fof(f3393,plain,(
% 15.50/2.36 ![X0,X1]: (X0=join(meet(top,X0),meet(meet(zero,X1),X0)))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f19,f3365])).
% 15.50/2.36 fof(f3394,plain,(
% 15.50/2.36 ![X0]: (X0=join(meet(top,X0),meet(zero,X0)))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f3392,f3393])).
% 15.50/2.36 fof(f3395,plain,(
% 15.50/2.36 ![X0]: (X0=join(meet(zero,X0),meet(top,X0)))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f19,f3394])).
% 15.50/2.36 fof(f3399,plain,(
% 15.50/2.36 ![X0]: (X0=join(zero,meet(top,X0)))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f3392,f3395])).
% 15.50/2.36 fof(f3434,plain,(
% 15.50/2.36 ![X0]: (X0=join(zero,X0))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f19,f3380])).
% 15.50/2.36 fof(f3483,plain,(
% 15.50/2.36 ![X0]: (X0=meet(top,X0))),
% 15.50/2.36 inference(backward_demodulation,[status(thm)],[f3434,f3399])).
% 15.50/2.36 fof(f3487,plain,(
% 15.50/2.36 ![X0,X1]: (X0=meet(X0,join(X0,X1)))),
% 15.50/2.36 inference(backward_demodulation,[status(thm)],[f3434,f2870])).
% 15.50/2.36 fof(f4809,plain,(
% 15.50/2.36 ![X0,X1,X2]: (composition(X0,X1)=meet(composition(X0,X1),composition(join(X0,X2),X1)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f25,f3487])).
% 15.50/2.36 fof(f10078,plain,(
% 15.50/2.36 ![X0,X1,X2]: (composition(join(X0,X1),X2)=composition(join(X1,X0),X2))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f25,f970])).
% 15.50/2.36 fof(f10932,plain,(
% 15.50/2.36 ![X0,X1]: (composition(X0,X1)=meet(composition(X0,X1),composition(top,X1)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f2871,f4809])).
% 15.50/2.36 fof(f11122,plain,(
% 15.50/2.36 ![X0]: (composition(one,X0)=meet(X0,composition(top,X0)))),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f586,f10932])).
% 15.50/2.36 fof(f11171,plain,(
% 15.50/2.36 ![X0]: (X0=meet(X0,composition(top,X0)))),
% 15.50/2.36 inference(forward_demodulation,[status(thm)],[f586,f11122])).
% 15.50/2.36 fof(f11295,plain,(
% 15.50/2.36 top=composition(top,top)),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f3483,f11171])).
% 15.50/2.36 fof(f11496,plain,(
% 15.50/2.36 join(complement(top),composition(converse(top),complement(top)))=complement(top)),
% 15.50/2.36 inference(paramodulation,[status(thm)],[f11295,f44])).
% 15.50/2.41 fof(f11686,plain,(
% 15.50/2.41 composition(join(converse(top),one),complement(top))=complement(top)),
% 15.50/2.41 inference(forward_demodulation,[status(thm)],[f1002,f11496])).
% 15.50/2.41 fof(f11687,plain,(
% 15.50/2.41 composition(join(one,converse(top)),complement(top))=complement(top)),
% 15.50/2.41 inference(forward_demodulation,[status(thm)],[f10078,f11686])).
% 15.50/2.41 fof(f11688,plain,(
% 15.50/2.41 composition(converse(join(one,top)),complement(top))=complement(top)),
% 15.50/2.41 inference(forward_demodulation,[status(thm)],[f736,f11687])).
% 15.50/2.41 fof(f11689,plain,(
% 15.50/2.41 composition(converse(join(top,one)),complement(top))=complement(top)),
% 15.50/2.41 inference(forward_demodulation,[status(thm)],[f1151,f11688])).
% 15.50/2.41 fof(f11690,plain,(
% 15.50/2.41 composition(converse(top),complement(top))=complement(top)),
% 15.50/2.41 inference(forward_demodulation,[status(thm)],[f2809,f11689])).
% 15.50/2.41 fof(f11691,plain,(
% 15.50/2.41 composition(top,complement(top))=complement(top)),
% 15.50/2.41 inference(forward_demodulation,[status(thm)],[f2862,f11690])).
% 15.50/2.41 fof(f11692,plain,(
% 15.50/2.41 composition(top,zero)=complement(top)),
% 15.50/2.41 inference(forward_demodulation,[status(thm)],[f557,f11691])).
% 15.50/2.41 fof(f11697,plain,(
% 15.50/2.41 join(composition(top,zero),meet(sK2_skl,composition(sK1_skl,sK0_skl)))=zero),
% 15.50/2.41 inference(backward_demodulation,[status(thm)],[f11698,f3304])).
% 15.50/2.41 fof(f11698,plain,(
% 15.50/2.41 composition(top,zero)=zero),
% 15.50/2.41 inference(forward_demodulation,[status(thm)],[f557,f11692])).
% 15.50/2.41 fof(f11748,plain,(
% 15.50/2.41 join(zero,meet(sK2_skl,composition(sK1_skl,sK0_skl)))=zero),
% 15.50/2.41 inference(forward_demodulation,[status(thm)],[f11698,f11697])).
% 15.50/2.41 fof(f11749,plain,(
% 15.50/2.41 meet(sK2_skl,composition(sK1_skl,sK0_skl))=zero),
% 15.50/2.41 inference(forward_demodulation,[status(thm)],[f3434,f11748])).
% 15.50/2.41 fof(f11750,plain,(
% 15.50/2.41 $false),
% 15.50/2.41 inference(forward_subsumption_resolution,[status(thm)],[f11749,f1831])).
% 15.50/2.41 % SZS output end CNFRefutation for theBenchmark.p
% 15.50/2.43 % Elapsed time: 2.070745 seconds
% 15.50/2.43 % CPU time: 16.203984 seconds
% 15.50/2.43 % Total memory used: 285.275 MB
% 15.50/2.43 % Net memory used: 280.803 MB
%------------------------------------------------------------------------------