%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL043+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:03:44 PM UTC 2026
% Result : Theorem 26.32s 3.78s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL043+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n006.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 04:07:57 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.36 % Drodi V4.1.1
% 26.32/3.78 % Refutation found
% 26.32/3.78 % SZS status Theorem for theBenchmark: Theorem is valid
% 26.32/3.78 % SZS output start CNFRefutation for theBenchmark
% 26.32/3.78 fof(f1,axiom,(
% 26.32/3.78 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 26.32/3.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.32/3.78 fof(f2,axiom,(
% 26.32/3.78 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 26.32/3.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.32/3.78 fof(f3,axiom,(
% 26.32/3.78 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 26.32/3.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.32/3.78 fof(f4,axiom,(
% 26.32/3.78 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 26.32/3.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.32/3.78 fof(f6,axiom,(
% 26.32/3.78 (! [X0] : composition(X0,one) = X0 )),
% 26.32/3.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.32/3.78 fof(f7,axiom,(
% 26.32/3.78 (! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) )),
% 26.32/3.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.32/3.78 fof(f8,axiom,(
% 26.32/3.78 (! [X0] : converse(converse(X0)) = X0 )),
% 26.32/3.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.32/3.78 fof(f9,axiom,(
% 26.32/3.78 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 26.32/3.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.32/3.78 fof(f10,axiom,(
% 26.32/3.78 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 26.32/3.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.32/3.78 fof(f11,axiom,(
% 26.32/3.78 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 26.32/3.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.32/3.78 fof(f12,axiom,(
% 26.32/3.78 (! [X0] : top = join(X0,complement(X0)) )),
% 26.32/3.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.32/3.78 fof(f13,axiom,(
% 26.32/3.78 (! [X0] : zero = meet(X0,complement(X0)) )),
% 26.32/3.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.32/3.78 fof(f16,axiom,(
% 26.32/3.78 (! [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) )),
% 26.32/3.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.32/3.78 fof(f17,conjecture,(
% 26.32/3.78 (! [X0,X1,X2] :( join(composition(X0,converse(X1)),X2) = X2=> join(composition(complement(X2),X1),complement(X0)) = complement(X0) ) )),
% 26.32/3.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.32/3.78 fof(f18,negated_conjecture,(
% 26.32/3.78 ~((! [X0,X1,X2] :( join(composition(X0,converse(X1)),X2) = X2=> join(composition(complement(X2),X1),complement(X0)) = complement(X0) ) ))),
% 26.32/3.78 inference(negated_conjecture,[status(cth)],[f17])).
% 26.32/3.78 fof(f19,plain,(
% 26.32/3.78 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 26.32/3.78 inference(cnf_transformation,[status(thm)],[f1])).
% 26.32/3.78 fof(f20,plain,(
% 26.32/3.78 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 26.32/3.78 inference(cnf_transformation,[status(thm)],[f2])).
% 26.32/3.78 fof(f21,plain,(
% 26.32/3.78 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 26.32/3.78 inference(cnf_transformation,[status(thm)],[f3])).
% 26.32/3.78 fof(f22,plain,(
% 26.32/3.78 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 26.32/3.78 inference(cnf_transformation,[status(thm)],[f4])).
% 26.32/3.78 fof(f24,plain,(
% 26.32/3.78 ![X0]: (composition(X0,one)=X0)),
% 26.32/3.78 inference(cnf_transformation,[status(thm)],[f6])).
% 26.32/3.78 fof(f25,plain,(
% 26.32/3.78 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 26.32/3.78 inference(cnf_transformation,[status(thm)],[f7])).
% 26.32/3.78 fof(f26,plain,(
% 26.32/3.78 ![X0]: (converse(converse(X0))=X0)),
% 26.32/3.78 inference(cnf_transformation,[status(thm)],[f8])).
% 26.32/3.78 fof(f27,plain,(
% 26.32/3.78 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 26.32/3.78 inference(cnf_transformation,[status(thm)],[f9])).
% 26.32/3.78 fof(f28,plain,(
% 26.32/3.78 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 26.32/3.78 inference(cnf_transformation,[status(thm)],[f10])).
% 26.32/3.78 fof(f29,plain,(
% 26.32/3.78 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 26.32/3.78 inference(cnf_transformation,[status(thm)],[f11])).
% 26.32/3.78 fof(f30,plain,(
% 26.32/3.78 ![X0]: (top=join(X0,complement(X0)))),
% 26.32/3.78 inference(cnf_transformation,[status(thm)],[f12])).
% 26.32/3.78 fof(f31,plain,(
% 26.32/3.78 ![X0]: (zero=meet(X0,complement(X0)))),
% 26.32/3.78 inference(cnf_transformation,[status(thm)],[f13])).
% 26.32/3.78 fof(f34,plain,(
% 26.32/3.78 ![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))),
% 26.32/3.78 inference(cnf_transformation,[status(thm)],[f16])).
% 26.32/3.78 fof(f35,plain,(
% 26.32/3.78 (?[X0,X1,X2]: (join(composition(X0,converse(X1)),X2)=X2&~join(composition(complement(X2),X1),complement(X0))=complement(X0)))),
% 26.32/3.78 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 26.32/3.78 fof(f36,plain,(
% 26.32/3.78 (join(composition(sK0_skl,converse(sK1_skl)),sK2_skl)=sK2_skl&~join(composition(complement(sK2_skl),sK1_skl),complement(sK0_skl))=complement(sK0_skl))),
% 26.32/3.78 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])).
% 26.32/3.78 fof(f37,plain,(
% 26.32/3.78 join(composition(sK0_skl,converse(sK1_skl)),sK2_skl)=sK2_skl),
% 26.32/3.78 inference(cnf_transformation,[status(thm)],[f36])).
% 26.32/3.78 fof(f38,plain,(
% 26.32/3.78 ~join(composition(complement(sK2_skl),sK1_skl),complement(sK0_skl))=complement(sK0_skl)),
% 26.32/3.78 inference(cnf_transformation,[status(thm)],[f36])).
% 26.32/3.78 fof(f44,plain,(
% 26.32/3.78 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f22,f21])).
% 26.32/3.78 fof(f53,plain,(
% 26.32/3.78 ~join(complement(sK0_skl),composition(complement(sK2_skl),sK1_skl))=complement(sK0_skl)),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f19,f38])).
% 26.32/3.78 fof(f56,plain,(
% 26.32/3.78 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f19,f20])).
% 26.32/3.78 fof(f61,plain,(
% 26.32/3.78 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X0),X2))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f19,f20])).
% 26.32/3.78 fof(f70,plain,(
% 26.32/3.78 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f19,f22])).
% 26.32/3.78 fof(f75,plain,(
% 26.32/3.78 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f26,f28])).
% 26.32/3.78 fof(f90,plain,(
% 26.32/3.78 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f22,f70])).
% 26.32/3.78 fof(f99,plain,(
% 26.32/3.78 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X1,X0),complement(X2))))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f70,f22])).
% 26.32/3.78 fof(f104,plain,(
% 26.32/3.78 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f19,f27])).
% 26.32/3.78 fof(f107,plain,(
% 26.32/3.78 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f26,f27])).
% 26.32/3.78 fof(f109,plain,(
% 26.32/3.78 ![X0,X1]: (converse(join(X0,converse(X1)))=join(converse(X0),X1))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f26,f27])).
% 26.32/3.78 fof(f187,plain,(
% 26.32/3.78 ![X0,X1]: (converse(join(converse(X0),X1))=join(converse(X1),X0))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f26,f104])).
% 26.32/3.78 fof(f239,plain,(
% 26.32/3.78 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X1,X2),composition(X0,X2)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f19,f25])).
% 26.32/3.78 fof(f260,plain,(
% 26.32/3.78 ![X0,X1]: (join(composition(converse(converse(X0)),complement(converse(composition(X1,X0)))),complement(converse(X1)))=complement(converse(X1)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f28,f29])).
% 26.32/3.78 fof(f272,plain,(
% 26.32/3.78 ![X0,X1]: (join(composition(X0,complement(converse(composition(X1,X0)))),complement(converse(X1)))=complement(converse(X1)))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f26,f260])).
% 26.32/3.78 fof(f276,plain,(
% 26.32/3.78 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f24,f75])).
% 26.32/3.78 fof(f282,plain,(
% 26.32/3.78 ![X0]: (X0=composition(converse(one),X0))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f26,f276])).
% 26.32/3.78 fof(f285,plain,(
% 26.32/3.78 ![X0,X1]: (zero=meet(join(complement(X0),complement(X1)),meet(X1,X0)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f70,f31])).
% 26.32/3.78 fof(f287,plain,(
% 26.32/3.78 ![X0,X1]: (zero=complement(join(meet(X0,X1),complement(meet(X0,X1)))))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f99,f285])).
% 26.32/3.78 fof(f288,plain,(
% 26.32/3.78 zero=complement(top)),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f30,f287])).
% 26.32/3.78 fof(f292,plain,(
% 26.32/3.78 ![X0]: (meet(top,X0)=complement(join(complement(X0),zero)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f288,f70])).
% 26.32/3.78 fof(f294,plain,(
% 26.32/3.78 ![X0]: (meet(X0,top)=complement(join(complement(X0),zero)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f288,f22])).
% 26.32/3.78 fof(f295,plain,(
% 26.32/3.78 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f288,f22])).
% 26.32/3.78 fof(f298,plain,(
% 26.32/3.78 one=converse(one)),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f24,f282])).
% 26.32/3.78 fof(f304,plain,(
% 26.32/3.78 ![X0]: (join(composition(converse(converse(one)),complement(X0)),complement(X0))=complement(X0))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f282,f29])).
% 26.32/3.78 fof(f305,plain,(
% 26.32/3.78 ![X0,X1]: (composition(join(X0,converse(one)),X1)=join(composition(X0,X1),X1))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f282,f25])).
% 26.32/3.78 fof(f308,plain,(
% 26.32/3.78 ![X0]: (X0=composition(one,X0))),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f298,f282])).
% 26.32/3.78 fof(f311,plain,(
% 26.32/3.78 ![X0]: (join(composition(one,complement(X0)),complement(X0))=complement(X0))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f26,f304])).
% 26.32/3.78 fof(f312,plain,(
% 26.32/3.78 ![X0,X1]: (composition(join(X0,one),X1)=join(composition(X0,X1),X1))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f298,f305])).
% 26.32/3.78 fof(f314,plain,(
% 26.32/3.78 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f308,f311])).
% 26.32/3.78 fof(f351,plain,(
% 26.32/3.78 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f30,f107])).
% 26.32/3.78 fof(f356,plain,(
% 26.32/3.78 ![X0,X1]: (join(complement(X0),join(X0,X1))=join(top,X1))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f30,f61])).
% 26.32/3.78 fof(f375,plain,(
% 26.32/3.78 ![X0,X1]: (join(meet(X0,X1),complement(join(complement(X0),complement(X1))))=complement(join(complement(X0),complement(X1))))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f22,f314])).
% 26.32/3.78 fof(f379,plain,(
% 26.32/3.78 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f314,f70])).
% 26.32/3.78 fof(f387,plain,(
% 26.32/3.78 ![X0,X1]: (join(meet(X0,X1),meet(X1,X0))=complement(join(complement(X0),complement(X1))))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f70,f375])).
% 26.32/3.78 fof(f388,plain,(
% 26.32/3.78 ![X0,X1]: (join(meet(X0,X1),meet(X1,X0))=meet(X1,X0))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f70,f387])).
% 26.32/3.78 fof(f467,plain,(
% 26.32/3.78 ![X0,X1]: (meet(X0,join(zero,complement(X1)))=complement(join(complement(X0),meet(top,X1))))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f295,f22])).
% 26.32/3.78 fof(f468,plain,(
% 26.32/3.78 ![X0,X1]: (meet(join(zero,complement(X0)),X1)=complement(join(meet(top,X0),complement(X1))))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f295,f22])).
% 26.32/3.78 fof(f494,plain,(
% 26.32/3.78 ![X0]: (converse(converse(top))=join(converse(converse(complement(converse(converse(X0))))),X0))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f351,f187])).
% 26.32/3.78 fof(f515,plain,(
% 26.32/3.78 ![X0]: (top=join(converse(converse(complement(converse(converse(X0))))),X0))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f26,f494])).
% 26.32/3.78 fof(f516,plain,(
% 26.32/3.78 ![X0]: (top=join(complement(converse(converse(X0))),X0))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f26,f515])).
% 26.32/3.78 fof(f519,plain,(
% 26.32/3.78 ![X0]: (top=join(complement(X0),X0))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f26,f516])).
% 26.32/3.78 fof(f552,plain,(
% 26.32/3.78 ![X0]: (join(complement(complement(X0)),complement(X0))=join(top,complement(X0)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f314,f356])).
% 26.32/3.78 fof(f553,plain,(
% 26.32/3.78 ![X0]: (join(complement(complement(X0)),top)=join(top,X0))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f519,f356])).
% 26.32/3.78 fof(f561,plain,(
% 26.32/3.78 join(complement(composition(sK0_skl,converse(sK1_skl))),sK2_skl)=join(top,sK2_skl)),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f37,f356])).
% 26.32/3.78 fof(f563,plain,(
% 26.32/3.78 ![X0]: (join(complement(X0),converse(top))=join(top,converse(complement(converse(X0)))))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f351,f356])).
% 26.32/3.78 fof(f564,plain,(
% 26.32/3.78 ![X0]: (join(complement(X0),top)=join(top,complement(X0)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f30,f356])).
% 26.32/3.78 fof(f573,plain,(
% 26.32/3.78 ![X0]: (top=join(top,complement(X0)))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f519,f552])).
% 26.32/3.78 fof(f577,plain,(
% 26.32/3.78 ![X0]: (top=join(top,X0))),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f579,f553])).
% 26.32/3.78 fof(f579,plain,(
% 26.32/3.78 ![X0]: (join(complement(X0),top)=top)),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f573,f564])).
% 26.32/3.78 fof(f586,plain,(
% 26.32/3.78 join(complement(composition(sK0_skl,converse(sK1_skl))),sK2_skl)=top),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f577,f561])).
% 26.32/3.78 fof(f589,plain,(
% 26.32/3.78 ![X0]: (join(complement(X0),converse(top))=top)),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f577,f563])).
% 26.32/3.78 fof(f839,plain,(
% 26.32/3.78 join(sK2_skl,complement(composition(sK0_skl,converse(sK1_skl))))=top),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f19,f586])).
% 26.32/3.78 fof(f842,plain,(
% 26.32/3.78 ![X0]: (join(complement(composition(sK0_skl,converse(sK1_skl))),join(sK2_skl,X0))=join(top,X0))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f586,f20])).
% 26.32/3.78 fof(f846,plain,(
% 26.32/3.78 ![X0]: (join(complement(composition(sK0_skl,converse(sK1_skl))),join(sK2_skl,X0))=top)),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f577,f842])).
% 26.32/3.78 fof(f851,plain,(
% 26.32/3.78 ![X0]: (join(join(sK2_skl,X0),complement(composition(sK0_skl,converse(sK1_skl))))=top)),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f19,f846])).
% 26.32/3.78 fof(f863,plain,(
% 26.32/3.78 ![X0]: (join(X0,join(sK2_skl,complement(composition(sK0_skl,converse(sK1_skl)))))=top)),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f61,f851])).
% 26.32/3.78 fof(f867,plain,(
% 26.32/3.78 ![X0]: (join(X0,top)=top)),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f839,f863])).
% 26.32/3.78 fof(f885,plain,(
% 26.32/3.78 ![X0]: (converse(top)=join(X0,converse(top)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f867,f107])).
% 26.32/3.78 fof(f898,plain,(
% 26.32/3.78 converse(top)=top),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f885,f589])).
% 26.32/3.78 fof(f1137,plain,(
% 26.32/3.78 ![X0,X1]: (join(meet(X0,X1),meet(X0,X1))=meet(X1,X0))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f90,f388])).
% 26.32/3.78 fof(f1219,plain,(
% 26.32/3.78 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f31,f44])).
% 26.32/3.78 fof(f1220,plain,(
% 26.32/3.78 ![X0]: (X0=join(complement(complement(X0)),complement(join(complement(X0),X0))))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f379,f44])).
% 26.32/3.78 fof(f1221,plain,(
% 26.32/3.78 ![X0,X1]: (X0=join(meet(X1,X0),complement(join(complement(X0),X1))))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f90,f44])).
% 26.32/3.78 fof(f1223,plain,(
% 26.32/3.78 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f70,f44])).
% 26.32/3.78 fof(f1224,plain,(
% 26.32/3.78 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f22,f44])).
% 26.32/3.78 fof(f1230,plain,(
% 26.32/3.78 ![X0]: (X0=join(meet(X0,top),complement(top)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f867,f44])).
% 26.32/3.78 fof(f1232,plain,(
% 26.32/3.78 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(X1,complement(X0)))))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f19,f44])).
% 26.32/3.78 fof(f1239,plain,(
% 26.32/3.78 ![X0,X1,X2]: (join(meet(X0,X1),join(complement(join(complement(X0),X1)),X2))=join(X0,X2))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f44,f20])).
% 26.32/3.78 fof(f1240,plain,(
% 26.32/3.78 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f70,f1219])).
% 26.32/3.78 fof(f1241,plain,(
% 26.32/3.78 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f379,f1240])).
% 26.32/3.78 fof(f1242,plain,(
% 26.32/3.78 ![X0]: (X0=join(complement(complement(X0)),complement(top)))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f519,f1220])).
% 26.32/3.78 fof(f1243,plain,(
% 26.32/3.78 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f288,f1242])).
% 26.32/3.78 fof(f1250,plain,(
% 26.32/3.78 ![X0]: (X0=join(meet(X0,top),zero))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f288,f1230])).
% 26.32/3.78 fof(f1258,plain,(
% 26.32/3.78 ![X0]: (meet(top,complement(X0))=complement(X0))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f1241,f295])).
% 26.32/3.78 fof(f1283,plain,(
% 26.32/3.78 ![X0]: (join(meet(top,complement(X0)),complement(X0))=meet(complement(X0),top))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f1258,f1137])).
% 26.32/3.78 fof(f1297,plain,(
% 26.32/3.78 ![X0]: (join(complement(X0),complement(X0))=meet(complement(X0),top))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f1258,f1283])).
% 26.32/3.78 fof(f1298,plain,(
% 26.32/3.78 ![X0]: (complement(X0)=meet(complement(X0),top))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f314,f1297])).
% 26.32/3.78 fof(f1321,plain,(
% 26.32/3.78 ![X0]: (complement(X0)=join(complement(X0),complement(join(complement(complement(X0)),top))))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f1298,f44])).
% 26.32/3.78 fof(f1337,plain,(
% 26.32/3.78 ![X0]: (complement(X0)=join(complement(X0),complement(top)))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f867,f1321])).
% 26.32/3.78 fof(f1338,plain,(
% 26.32/3.78 ![X0]: (X0=complement(complement(X0)))),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f1343,f1243])).
% 26.32/3.78 fof(f1341,plain,(
% 26.32/3.78 ![X0]: (meet(X0,top)=complement(complement(X0)))),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f1343,f294])).
% 26.32/3.78 fof(f1342,plain,(
% 26.32/3.78 ![X0]: (meet(top,X0)=complement(complement(X0)))),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f1343,f292])).
% 26.32/3.78 fof(f1343,plain,(
% 26.32/3.78 ![X0]: (complement(X0)=join(complement(X0),zero))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f288,f1337])).
% 26.32/3.78 fof(f1360,plain,(
% 26.32/3.78 ![X0]: (X0=join(zero,X0))),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f1338,f1241])).
% 26.32/3.78 fof(f1361,plain,(
% 26.32/3.78 ![X0]: (meet(X0,X0)=X0)),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f1338,f379])).
% 26.32/3.78 fof(f1398,plain,(
% 26.32/3.78 ![X0]: (X0=join(X0,zero))),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f1400,f1250])).
% 26.32/3.78 fof(f1400,plain,(
% 26.32/3.78 ![X0]: (meet(X0,top)=X0)),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f1338,f1341])).
% 26.32/3.78 fof(f1412,plain,(
% 26.32/3.78 ![X0,X1]: (meet(join(zero,complement(X0)),X1)=complement(join(X0,complement(X1))))),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f1420,f468])).
% 26.32/3.78 fof(f1413,plain,(
% 26.32/3.78 ![X0,X1]: (meet(X0,join(zero,complement(X1)))=complement(join(complement(X0),X1)))),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f1420,f467])).
% 26.32/3.78 fof(f1420,plain,(
% 26.32/3.78 ![X0]: (meet(top,X0)=X0)),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f1338,f1342])).
% 26.32/3.78 fof(f1468,plain,(
% 26.32/3.78 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f1469,f1232])).
% 26.32/3.78 fof(f1469,plain,(
% 26.32/3.78 ![X0,X1]: (meet(complement(X0),X1)=complement(join(X0,complement(X1))))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f1360,f1412])).
% 26.32/3.78 fof(f1475,plain,(
% 26.32/3.78 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X0,complement(X1)),X2))=join(X0,X2))),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f1478,f1239])).
% 26.32/3.78 fof(f1477,plain,(
% 26.32/3.78 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 26.32/3.78 inference(backward_demodulation,[status(thm)],[f1478,f1221])).
% 26.32/3.78 fof(f1478,plain,(
% 26.32/3.78 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),X1)))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f1360,f1413])).
% 26.32/3.78 fof(f1524,plain,(
% 26.32/3.78 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X2,X0)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f19,f56])).
% 26.32/3.78 fof(f1691,plain,(
% 26.32/3.78 ![X0]: (join(meet(X0,X0),X0)=meet(X0,X0))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f1361,f1137])).
% 26.32/3.78 fof(f1722,plain,(
% 26.32/3.78 ![X0]: (join(X0,X0)=meet(X0,X0))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f1361,f1691])).
% 26.32/3.78 fof(f1726,plain,(
% 26.32/3.78 ![X0]: (join(X0,X0)=X0)),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f1361,f1722])).
% 26.32/3.78 fof(f1812,plain,(
% 26.32/3.78 ![X0]: (converse(converse(X0))=join(converse(zero),X0))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f1360,f109])).
% 26.32/3.78 fof(f1821,plain,(
% 26.32/3.78 ![X0]: (X0=join(converse(zero),X0))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f26,f1812])).
% 26.32/3.78 fof(f1907,plain,(
% 26.32/3.78 ![X0,X1]: (join(X0,join(join(X1,X0),X1))=join(X1,X0))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f56,f1726])).
% 26.32/3.78 fof(f1931,plain,(
% 26.32/3.78 ![X0,X1]: (join(X0,join(X0,join(X1,X1)))=join(X1,X0))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f61,f1907])).
% 26.32/3.78 fof(f1938,plain,(
% 26.32/3.78 ![X0,X1]: (join(X0,join(X0,X1))=join(X1,X0))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f1726,f1931])).
% 26.32/3.78 fof(f1955,plain,(
% 26.32/3.78 zero=converse(zero)),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f1398,f1821])).
% 26.32/3.78 fof(f2042,plain,(
% 26.32/3.78 ![X0,X1]: (X0=join(meet(complement(X1),X0),meet(X1,X0)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f90,f1223])).
% 26.32/3.78 fof(f2121,plain,(
% 26.32/3.78 ![X0,X1]: (X0=join(meet(complement(X1),X0),meet(X0,X1)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f90,f1224])).
% 26.32/3.78 fof(f2168,plain,(
% 26.32/3.78 ![X0,X1]: (X0=join(meet(X1,X0),meet(complement(X1),X0)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f90,f1477])).
% 26.32/3.78 fof(f2738,plain,(
% 26.32/3.78 ![X0]: (meet(complement(top),X0)=complement(top))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f577,f1469])).
% 26.32/3.78 fof(f2745,plain,(
% 26.32/3.78 meet(complement(sK2_skl),composition(sK0_skl,converse(sK1_skl)))=complement(top)),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f839,f1469])).
% 26.32/3.78 fof(f2777,plain,(
% 26.32/3.78 ![X0]: (meet(zero,X0)=complement(top))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f288,f2738])).
% 26.32/3.78 fof(f2783,plain,(
% 26.32/3.78 ![X0]: (meet(zero,X0)=zero)),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f288,f2777])).
% 26.32/3.78 fof(f2792,plain,(
% 26.32/3.78 meet(complement(sK2_skl),composition(sK0_skl,converse(sK1_skl)))=zero),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f288,f2745])).
% 26.32/3.78 fof(f3225,plain,(
% 26.32/3.78 ![X0,X1]: (join(meet(X0,X1),X1)=join(meet(complement(X0),X1),meet(X0,X1)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f2168,f1938])).
% 26.32/3.78 fof(f3226,plain,(
% 26.32/3.78 ![X0,X1]: (join(meet(X0,X1),X0)=join(meet(complement(X1),X0),meet(X0,X1)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f1468,f1938])).
% 26.32/3.78 fof(f3292,plain,(
% 26.32/3.78 ![X0,X1]: (join(meet(X0,X1),X1)=X1)),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f2042,f3225])).
% 26.32/3.78 fof(f3294,plain,(
% 26.32/3.78 ![X0,X1]: (join(meet(X0,X1),X0)=X0)),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f2121,f3226])).
% 26.32/3.78 fof(f3373,plain,(
% 26.32/3.78 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f19,f3292])).
% 26.32/3.78 fof(f3414,plain,(
% 26.32/3.78 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f19,f3294])).
% 26.32/3.78 fof(f3439,plain,(
% 26.32/3.78 ![X0,X1,X2]: (join(meet(X0,X1),join(X0,X2))=join(X0,X2))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f3294,f20])).
% 26.32/3.78 fof(f3478,plain,(
% 26.32/3.78 ![X0,X1,X2]: (join(X0,X1)=join(meet(X2,X1),join(X0,X1)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f3373,f56])).
% 26.32/3.78 fof(f5237,plain,(
% 26.32/3.78 ![X0,X1,X2]: (join(X0,X1)=join(meet(X0,X2),join(X1,X0)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f3414,f1524])).
% 26.32/3.78 fof(f8326,plain,(
% 26.32/3.78 ![X0,X1]: (join(meet(X0,complement(X1)),X1)=join(X0,X1))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f3478,f1475])).
% 26.32/3.78 fof(f8550,plain,(
% 26.32/3.78 ![X0,X1]: (join(X0,meet(X1,complement(X0)))=join(X1,X0))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f19,f8326])).
% 26.32/3.78 fof(f8701,plain,(
% 26.32/3.78 ![X0,X1,X2]: (join(meet(X0,X1),join(X2,X0))=join(X0,meet(X2,complement(X0))))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f8550,f3439])).
% 26.32/3.78 fof(f8746,plain,(
% 26.32/3.78 ![X0,X1]: (join(X0,X1)=join(X0,meet(X1,complement(X0))))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f5237,f8701])).
% 26.32/3.78 fof(f9106,plain,(
% 26.32/3.78 ![X0,X1]: (join(complement(X0),X1)=join(complement(X0),meet(X1,X0)))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f1338,f8746])).
% 26.32/3.78 fof(f10764,plain,(
% 26.32/3.78 ![X0]: (composition(top,X0)=join(composition(top,X0),X0))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f577,f312])).
% 26.32/3.78 fof(f11301,plain,(
% 26.32/3.78 composition(top,top)=top),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f867,f10764])).
% 26.32/3.78 fof(f11381,plain,(
% 26.32/3.78 join(composition(top,complement(converse(top))),complement(converse(top)))=complement(converse(top))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f11301,f272])).
% 26.32/3.78 fof(f11399,plain,(
% 26.32/3.78 composition(top,complement(converse(top)))=complement(converse(top))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f10764,f11381])).
% 26.32/3.78 fof(f11400,plain,(
% 26.32/3.78 composition(top,complement(top))=complement(converse(top))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f898,f11399])).
% 26.32/3.78 fof(f11401,plain,(
% 26.32/3.78 composition(top,zero)=complement(converse(top))),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f288,f11400])).
% 26.32/3.78 fof(f11402,plain,(
% 26.32/3.78 composition(top,zero)=complement(top)),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f898,f11401])).
% 26.32/3.78 fof(f11403,plain,(
% 26.32/3.78 composition(top,zero)=zero),
% 26.32/3.78 inference(forward_demodulation,[status(thm)],[f288,f11402])).
% 26.32/3.78 fof(f11470,plain,(
% 26.32/3.78 ![X0]: (composition(join(top,X0),zero)=join(composition(X0,zero),zero))),
% 26.32/3.78 inference(paramodulation,[status(thm)],[f11403,f239])).
% 26.32/3.85 fof(f11518,plain,(
% 26.32/3.85 ![X0]: (composition(top,zero)=join(composition(X0,zero),zero))),
% 26.32/3.85 inference(forward_demodulation,[status(thm)],[f577,f11470])).
% 26.32/3.85 fof(f11519,plain,(
% 26.32/3.85 ![X0]: (zero=join(composition(X0,zero),zero))),
% 26.32/3.85 inference(forward_demodulation,[status(thm)],[f11403,f11518])).
% 26.32/3.85 fof(f11544,plain,(
% 26.32/3.85 ![X0]: (zero=composition(X0,zero))),
% 26.32/3.85 inference(forward_demodulation,[status(thm)],[f1398,f11519])).
% 26.32/3.85 fof(f11648,plain,(
% 26.32/3.85 ![X0]: (converse(zero)=composition(converse(zero),X0))),
% 26.32/3.85 inference(paramodulation,[status(thm)],[f11544,f75])).
% 26.32/3.85 fof(f11692,plain,(
% 26.32/3.85 ![X0]: (zero=composition(converse(zero),X0))),
% 26.32/3.85 inference(forward_demodulation,[status(thm)],[f1955,f11648])).
% 26.32/3.85 fof(f11722,plain,(
% 26.32/3.85 ![X0]: (zero=composition(zero,X0))),
% 26.32/3.85 inference(forward_demodulation,[status(thm)],[f1955,f11692])).
% 26.32/3.85 fof(f13384,plain,(
% 26.32/3.85 join(meet(composition(complement(sK2_skl),sK1_skl),sK0_skl),meet(composition(zero,sK1_skl),sK0_skl))=meet(composition(meet(complement(sK2_skl),composition(sK0_skl,converse(sK1_skl))),sK1_skl),sK0_skl)),
% 26.32/3.85 inference(paramodulation,[status(thm)],[f2792,f34])).
% 26.32/3.85 fof(f13434,plain,(
% 26.32/3.85 join(meet(composition(complement(sK2_skl),sK1_skl),sK0_skl),meet(zero,sK0_skl))=meet(composition(meet(complement(sK2_skl),composition(sK0_skl,converse(sK1_skl))),sK1_skl),sK0_skl)),
% 26.32/3.85 inference(forward_demodulation,[status(thm)],[f11722,f13384])).
% 26.32/3.85 fof(f13435,plain,(
% 26.32/3.85 join(meet(composition(complement(sK2_skl),sK1_skl),sK0_skl),zero)=meet(composition(meet(complement(sK2_skl),composition(sK0_skl,converse(sK1_skl))),sK1_skl),sK0_skl)),
% 26.32/3.85 inference(forward_demodulation,[status(thm)],[f2783,f13434])).
% 26.32/3.85 fof(f13436,plain,(
% 26.32/3.85 meet(composition(complement(sK2_skl),sK1_skl),sK0_skl)=meet(composition(meet(complement(sK2_skl),composition(sK0_skl,converse(sK1_skl))),sK1_skl),sK0_skl)),
% 26.32/3.85 inference(forward_demodulation,[status(thm)],[f1398,f13435])).
% 26.32/3.85 fof(f13437,plain,(
% 26.32/3.85 meet(composition(complement(sK2_skl),sK1_skl),sK0_skl)=meet(composition(zero,sK1_skl),sK0_skl)),
% 26.32/3.85 inference(forward_demodulation,[status(thm)],[f2792,f13436])).
% 26.32/3.85 fof(f13438,plain,(
% 26.32/3.85 meet(composition(complement(sK2_skl),sK1_skl),sK0_skl)=meet(zero,sK0_skl)),
% 26.32/3.85 inference(forward_demodulation,[status(thm)],[f11722,f13437])).
% 26.32/3.85 fof(f13439,plain,(
% 26.32/3.85 meet(composition(complement(sK2_skl),sK1_skl),sK0_skl)=zero),
% 26.32/3.85 inference(forward_demodulation,[status(thm)],[f2783,f13438])).
% 26.32/3.85 fof(f13494,plain,(
% 26.32/3.85 join(complement(sK0_skl),composition(complement(sK2_skl),sK1_skl))=join(complement(sK0_skl),zero)),
% 26.32/3.85 inference(paramodulation,[status(thm)],[f13439,f9106])).
% 26.32/3.85 fof(f13534,plain,(
% 26.32/3.85 join(complement(sK0_skl),composition(complement(sK2_skl),sK1_skl))=complement(sK0_skl)),
% 26.32/3.85 inference(forward_demodulation,[status(thm)],[f1398,f13494])).
% 26.32/3.85 fof(f13535,plain,(
% 26.32/3.85 $false),
% 26.32/3.85 inference(forward_subsumption_resolution,[status(thm)],[f13534,f53])).
% 26.32/3.85 % SZS output end CNFRefutation for theBenchmark.p
% 26.32/3.89 % Elapsed time: 3.523376 seconds
% 26.32/3.89 % CPU time: 27.568494 seconds
% 26.32/3.89 % Total memory used: 272.337 MB
% 26.32/3.89 % Net memory used: 267.509 MB
%------------------------------------------------------------------------------