%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL004+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 : n003.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:31 PM UTC 2026
% Result : Theorem 4.10s 1.00s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL004+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.10/0.35 % Computer : n003.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 03:59:16 UTC 2026
% 0.14/0.36 % CPUTime :
% 0.14/0.36 % Drodi V4.1.1
% 4.10/1.00 % Refutation found
% 4.10/1.00 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.10/1.00 % SZS output start CNFRefutation for theBenchmark
% 4.10/1.00 fof(f1,axiom,(
% 4.10/1.00 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 4.10/1.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.10/1.00 fof(f2,axiom,(
% 4.10/1.00 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 4.10/1.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.10/1.00 fof(f3,axiom,(
% 4.10/1.00 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 4.10/1.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.10/1.00 fof(f4,axiom,(
% 4.10/1.00 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 4.10/1.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.10/1.00 fof(f6,axiom,(
% 4.10/1.00 (! [X0] : composition(X0,one) = X0 )),
% 4.10/1.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.10/1.00 fof(f8,axiom,(
% 4.10/1.00 (! [X0] : converse(converse(X0)) = X0 )),
% 4.10/1.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.10/1.00 fof(f9,axiom,(
% 4.10/1.00 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 4.10/1.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.10/1.00 fof(f10,axiom,(
% 4.10/1.00 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 4.10/1.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.10/1.00 fof(f11,axiom,(
% 4.10/1.00 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 4.10/1.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.10/1.00 fof(f12,axiom,(
% 4.10/1.00 (! [X0] : top = join(X0,complement(X0)) )),
% 4.10/1.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.10/1.00 fof(f13,axiom,(
% 4.10/1.00 (! [X0] : zero = meet(X0,complement(X0)) )),
% 4.10/1.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.10/1.00 fof(f17,conjecture,(
% 4.10/1.00 (! [X0] : converse(complement(X0)) = complement(converse(X0)) )),
% 4.10/1.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.10/1.00 fof(f18,negated_conjecture,(
% 4.10/1.00 ~((! [X0] : converse(complement(X0)) = complement(converse(X0)) ))),
% 4.10/1.00 inference(negated_conjecture,[status(cth)],[f17])).
% 4.10/1.00 fof(f19,plain,(
% 4.10/1.00 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 4.10/1.00 inference(cnf_transformation,[status(thm)],[f1])).
% 4.10/1.00 fof(f20,plain,(
% 4.10/1.00 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 4.10/1.00 inference(cnf_transformation,[status(thm)],[f2])).
% 4.10/1.00 fof(f21,plain,(
% 4.10/1.00 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 4.10/1.00 inference(cnf_transformation,[status(thm)],[f3])).
% 4.10/1.00 fof(f22,plain,(
% 4.10/1.00 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 4.10/1.00 inference(cnf_transformation,[status(thm)],[f4])).
% 4.10/1.00 fof(f24,plain,(
% 4.10/1.00 ![X0]: (composition(X0,one)=X0)),
% 4.10/1.00 inference(cnf_transformation,[status(thm)],[f6])).
% 4.10/1.00 fof(f26,plain,(
% 4.10/1.00 ![X0]: (converse(converse(X0))=X0)),
% 4.10/1.00 inference(cnf_transformation,[status(thm)],[f8])).
% 4.10/1.00 fof(f27,plain,(
% 4.10/1.00 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 4.10/1.00 inference(cnf_transformation,[status(thm)],[f9])).
% 4.10/1.00 fof(f28,plain,(
% 4.10/1.00 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 4.10/1.00 inference(cnf_transformation,[status(thm)],[f10])).
% 4.10/1.00 fof(f29,plain,(
% 4.10/1.00 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 4.10/1.00 inference(cnf_transformation,[status(thm)],[f11])).
% 4.10/1.00 fof(f30,plain,(
% 4.10/1.00 ![X0]: (top=join(X0,complement(X0)))),
% 4.10/1.00 inference(cnf_transformation,[status(thm)],[f12])).
% 4.10/1.00 fof(f31,plain,(
% 4.10/1.00 ![X0]: (zero=meet(X0,complement(X0)))),
% 4.10/1.00 inference(cnf_transformation,[status(thm)],[f13])).
% 4.10/1.00 fof(f35,plain,(
% 4.10/1.00 (?[X0]: ~converse(complement(X0))=complement(converse(X0)))),
% 4.10/1.00 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 4.10/1.00 fof(f36,plain,(
% 4.10/1.00 ~converse(complement(sK0_skl))=complement(converse(sK0_skl))),
% 4.10/1.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X0,sK0_skl)],[f35])).
% 4.10/1.00 fof(f37,plain,(
% 4.10/1.00 ~converse(complement(sK0_skl))=complement(converse(sK0_skl))),
% 4.10/1.00 inference(cnf_transformation,[status(thm)],[f36])).
% 4.10/1.00 fof(f43,plain,(
% 4.10/1.00 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 4.10/1.00 inference(backward_demodulation,[status(thm)],[f22,f21])).
% 4.10/1.00 fof(f45,plain,(
% 4.10/1.00 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X0,X1),complement(X2))))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f22,f22])).
% 4.10/1.00 fof(f46,plain,(
% 4.10/1.00 ![X0,X1,X2]: (meet(X0,join(complement(X1),complement(X2)))=complement(join(complement(X0),meet(X1,X2))))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f22,f22])).
% 4.10/1.00 fof(f47,plain,(
% 4.10/1.00 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f26,f27])).
% 4.10/1.00 fof(f50,plain,(
% 4.10/1.00 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f26,f28])).
% 4.10/1.00 fof(f66,plain,(
% 4.10/1.00 ![X0,X1]: (join(composition(X0,complement(composition(converse(X0),X1))),complement(X1))=complement(X1))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f26,f29])).
% 4.10/1.00 fof(f199,plain,(
% 4.10/1.00 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f22,f43])).
% 4.10/1.00 fof(f382,plain,(
% 4.10/1.00 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f24,f50])).
% 4.10/1.00 fof(f385,plain,(
% 4.10/1.00 ![X0]: (X0=composition(converse(one),X0))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f26,f382])).
% 4.10/1.00 fof(f388,plain,(
% 4.10/1.00 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f30,f47])).
% 4.10/1.00 fof(f394,plain,(
% 4.10/1.00 ![X0,X1]: (meet(top,X0)=complement(join(meet(X1,complement(X1)),complement(X0))))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f30,f45])).
% 4.10/1.00 fof(f395,plain,(
% 4.10/1.00 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f30,f22])).
% 4.10/1.00 fof(f406,plain,(
% 4.10/1.00 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f31,f394])).
% 4.10/1.00 fof(f407,plain,(
% 4.10/1.00 zero=complement(top)),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f31,f395])).
% 4.10/1.00 fof(f439,plain,(
% 4.10/1.00 one=converse(one)),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f24,f385])).
% 4.10/1.00 fof(f443,plain,(
% 4.10/1.00 ![X0]: (join(composition(one,complement(X0)),complement(X0))=complement(X0))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f385,f66])).
% 4.10/1.00 fof(f452,plain,(
% 4.10/1.00 ![X0]: (X0=composition(one,X0))),
% 4.10/1.00 inference(backward_demodulation,[status(thm)],[f439,f385])).
% 4.10/1.00 fof(f465,plain,(
% 4.10/1.00 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 4.10/1.00 inference(backward_demodulation,[status(thm)],[f452,f443])).
% 4.10/1.00 fof(f533,plain,(
% 4.10/1.00 ![X0,X1]: (meet(X0,join(zero,complement(X1)))=complement(join(complement(X0),meet(top,X1))))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f407,f46])).
% 4.10/1.00 fof(f565,plain,(
% 4.10/1.00 ![X0]: (X0=join(meet(X0,complement(X0)),complement(complement(X0))))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f465,f43])).
% 4.10/1.00 fof(f583,plain,(
% 4.10/1.00 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f31,f565])).
% 4.10/1.00 fof(f586,plain,(
% 4.10/1.00 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(meet(X0,X1))))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f22,f583])).
% 4.10/1.00 fof(f645,plain,(
% 4.10/1.00 ![X0]: (X0=join(meet(X0,converse(complement(converse(complement(X0))))),complement(converse(top))))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f388,f43])).
% 4.10/1.00 fof(f700,plain,(
% 4.10/1.00 ![X0,X1]: (join(X0,join(X1,complement(join(X0,X1))))=top)),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f30,f20])).
% 4.10/1.00 fof(f702,plain,(
% 4.10/1.00 ![X0,X1]: (join(zero,join(complement(complement(X0)),X1))=join(X0,X1))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f583,f20])).
% 4.10/1.00 fof(f715,plain,(
% 4.10/1.00 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f30,f20])).
% 4.10/1.00 fof(f724,plain,(
% 4.10/1.00 ![X0]: (join(zero,complement(complement(X0)))=join(X0,complement(complement(X0))))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f465,f702])).
% 4.10/1.00 fof(f731,plain,(
% 4.10/1.00 ![X0]: (X0=join(X0,complement(complement(X0))))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f583,f724])).
% 4.10/1.00 fof(f742,plain,(
% 4.10/1.00 ![X0]: (converse(converse(X0))=join(X0,converse(complement(complement(converse(X0))))))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f731,f47])).
% 4.10/1.00 fof(f743,plain,(
% 4.10/1.00 ![X0]: (join(zero,complement(complement(X0)))=join(X0,complement(complement(complement(complement(X0))))))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f731,f702])).
% 4.10/1.00 fof(f756,plain,(
% 4.10/1.00 ![X0]: (X0=join(X0,converse(complement(complement(converse(X0))))))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f26,f742])).
% 4.10/1.00 fof(f757,plain,(
% 4.10/1.00 ![X0]: (X0=join(X0,complement(complement(complement(complement(X0))))))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f583,f743])).
% 4.10/1.00 fof(f781,plain,(
% 4.10/1.00 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f27,f19])).
% 4.10/1.00 fof(f817,plain,(
% 4.10/1.00 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f19,f22])).
% 4.10/1.00 fof(f1353,plain,(
% 4.10/1.00 ![X0]: (converse(join(complement(complement(converse(converse(X0)))),X0))=converse(X0))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f756,f781])).
% 4.10/1.00 fof(f1377,plain,(
% 4.10/1.00 ![X0]: (converse(join(complement(complement(X0)),X0))=converse(X0))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f26,f1353])).
% 4.10/1.00 fof(f1410,plain,(
% 4.10/1.00 ![X0]: (converse(top)=join(join(complement(complement(X0)),X0),converse(complement(converse(X0)))))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f1377,f388])).
% 4.10/1.00 fof(f1423,plain,(
% 4.10/1.00 ![X0]: (converse(converse(X0))=join(complement(complement(X0)),X0))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f1377,f26])).
% 4.10/1.00 fof(f1434,plain,(
% 4.10/1.00 ![X0]: (converse(top)=join(complement(complement(X0)),join(X0,converse(complement(converse(X0))))))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f20,f1410])).
% 4.10/1.00 fof(f1435,plain,(
% 4.10/1.00 ![X0]: (converse(top)=join(complement(complement(X0)),converse(top)))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f388,f1434])).
% 4.10/1.00 fof(f1461,plain,(
% 4.10/1.00 ![X0]: (X0=join(complement(complement(X0)),X0))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f26,f1423])).
% 4.10/1.00 fof(f1473,plain,(
% 4.10/1.00 ![X0]: (join(zero,X0)=join(X0,X0))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f1461,f702])).
% 4.10/1.00 fof(f1485,plain,(
% 4.10/1.00 ![X0]: (complement(X0)=join(meet(complement(X0),X0),complement(X0)))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f1461,f43])).
% 4.10/1.00 fof(f1584,plain,(
% 4.10/1.00 ![X0]: (complement(X0)=join(complement(X0),meet(complement(X0),X0)))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f19,f1485])).
% 4.10/1.00 fof(f1624,plain,(
% 4.10/1.00 ![X0]: (join(zero,complement(complement(X0)))=join(X0,meet(complement(complement(X0)),complement(X0))))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f1584,f702])).
% 4.10/1.00 fof(f1650,plain,(
% 4.10/1.00 ![X0]: (X0=join(X0,meet(complement(complement(X0)),complement(X0))))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f583,f1624])).
% 4.10/1.00 fof(f1693,plain,(
% 4.10/1.00 ![X0]: (join(zero,complement(X0))=complement(X0))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f465,f1473])).
% 4.10/1.00 fof(f1718,plain,(
% 4.10/1.00 ![X0]: (X0=join(meet(X0,complement(X0)),complement(join(zero,complement(X0)))))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f1473,f43])).
% 4.10/1.00 fof(f1722,plain,(
% 4.10/1.00 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 4.10/1.00 inference(backward_demodulation,[status(thm)],[f1693,f586])).
% 4.10/1.00 fof(f1724,plain,(
% 4.10/1.00 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),meet(top,X1))))),
% 4.10/1.00 inference(backward_demodulation,[status(thm)],[f1693,f533])).
% 4.10/1.00 fof(f1728,plain,(
% 4.10/1.00 ![X0]: (meet(top,X0)=complement(complement(X0)))),
% 4.10/1.00 inference(backward_demodulation,[status(thm)],[f1693,f406])).
% 4.10/1.00 fof(f1753,plain,(
% 4.10/1.00 ![X0]: (X0=join(zero,complement(join(zero,complement(X0)))))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f31,f1718])).
% 4.10/1.00 fof(f1754,plain,(
% 4.10/1.00 ![X0]: (X0=complement(join(zero,complement(X0))))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f1693,f1753])).
% 4.10/1.00 fof(f1755,plain,(
% 4.10/1.00 ![X0]: (X0=join(X0,complement(complement(X0))))),
% 4.10/1.00 inference(backward_demodulation,[status(thm)],[f1829,f757])).
% 4.10/1.00 fof(f1760,plain,(
% 4.10/1.00 ![X0]: (X0=join(X0,meet(X0,complement(X0))))),
% 4.10/1.00 inference(backward_demodulation,[status(thm)],[f1829,f1650])).
% 4.10/1.00 fof(f1821,plain,(
% 4.10/1.00 ![X0]: (converse(top)=join(X0,converse(top)))),
% 4.10/1.00 inference(backward_demodulation,[status(thm)],[f1829,f1435])).
% 4.10/1.00 fof(f1829,plain,(
% 4.10/1.00 ![X0]: (X0=complement(complement(X0)))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f1693,f1754])).
% 4.10/1.00 fof(f1859,plain,(
% 4.10/1.00 ![X0,X1]: (meet(X0,X1)=complement(complement(meet(X1,X0))))),
% 4.10/1.00 inference(backward_demodulation,[status(thm)],[f1722,f817])).
% 4.10/1.00 fof(f1888,plain,(
% 4.10/1.00 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),X1)))),
% 4.10/1.00 inference(backward_demodulation,[status(thm)],[f1891,f1724])).
% 4.10/1.00 fof(f1891,plain,(
% 4.10/1.00 ![X0]: (meet(top,X0)=X0)),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f1829,f1728])).
% 4.10/1.00 fof(f1904,plain,(
% 4.10/1.00 ![X0]: (join(zero,X0)=X0)),
% 4.10/1.00 inference(backward_demodulation,[status(thm)],[f1911,f1473])).
% 4.10/1.00 fof(f1911,plain,(
% 4.10/1.00 ![X0]: (X0=join(X0,X0))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f1829,f1755])).
% 4.10/1.00 fof(f1925,plain,(
% 4.10/1.00 ![X0]: (X0=join(X0,zero))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f31,f1760])).
% 4.10/1.00 fof(f2077,plain,(
% 4.10/1.00 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f1829,f1859])).
% 4.10/1.00 fof(f2486,plain,(
% 4.10/1.00 ![X0,X1]: (X0=join(meet(complement(X1),X0),meet(X0,X1)))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f2077,f199])).
% 4.10/1.00 fof(f2548,plain,(
% 4.10/1.00 ![X0,X1]: (X0=join(meet(complement(X1),X0),meet(X1,X0)))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f2077,f2486])).
% 4.10/1.00 fof(f2718,plain,(
% 4.10/1.00 ![X0]: (join(X0,converse(top))=join(top,converse(complement(converse(complement(X0))))))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f388,f715])).
% 4.10/1.00 fof(f2721,plain,(
% 4.10/1.00 ![X0,X1]: (join(X0,join(X1,complement(X0)))=join(top,X1))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f19,f715])).
% 4.10/1.00 fof(f2733,plain,(
% 4.10/1.00 ![X0]: (converse(top)=join(top,converse(complement(converse(complement(X0))))))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f1821,f2718])).
% 4.10/1.00 fof(f2937,plain,(
% 4.10/1.00 ![X0]: (join(X0,join(X0,complement(X0)))=top)),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f1911,f700])).
% 4.10/1.00 fof(f2986,plain,(
% 4.10/1.00 converse(top)=top),
% 4.10/1.00 inference(backward_demodulation,[status(thm)],[f2996,f2733])).
% 4.10/1.00 fof(f2996,plain,(
% 4.10/1.00 ![X0]: (join(top,X0)=top)),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f2721,f2937])).
% 4.10/1.00 fof(f3015,plain,(
% 4.10/1.00 ![X0]: (top=join(X0,converse(complement(converse(X0)))))),
% 4.10/1.00 inference(backward_demodulation,[status(thm)],[f2986,f388])).
% 4.10/1.00 fof(f3024,plain,(
% 4.10/1.00 ![X0]: (X0=join(meet(X0,converse(complement(converse(complement(X0))))),complement(top)))),
% 4.10/1.00 inference(backward_demodulation,[status(thm)],[f2986,f645])).
% 4.10/1.00 fof(f3054,plain,(
% 4.10/1.00 ![X0]: (X0=join(meet(X0,converse(complement(converse(complement(X0))))),zero))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f407,f3024])).
% 4.10/1.00 fof(f3055,plain,(
% 4.10/1.00 ![X0]: (X0=meet(X0,converse(complement(converse(complement(X0))))))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f1925,f3054])).
% 4.10/1.00 fof(f3586,plain,(
% 4.10/1.00 ![X0,X1]: (join(X0,complement(X1))=complement(meet(complement(X0),X1)))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f1829,f1722])).
% 4.10/1.00 fof(f3698,plain,(
% 4.10/1.00 ![X0,X1]: (meet(complement(X0),complement(X1))=complement(join(X0,X1)))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f1829,f1888])).
% 4.10/1.00 fof(f3803,plain,(
% 4.10/1.00 ![X0]: (join(X0,complement(converse(complement(converse(complement(complement(X0)))))))=complement(complement(X0)))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f3055,f3586])).
% 4.10/1.00 fof(f3842,plain,(
% 4.10/1.00 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=complement(complement(X0)))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f1829,f3803])).
% 4.10/1.00 fof(f3843,plain,(
% 4.10/1.00 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=X0)),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f1829,f3842])).
% 4.10/1.00 fof(f3890,plain,(
% 4.10/1.00 ![X0]: (converse(converse(X0))=join(X0,converse(complement(converse(complement(converse(converse(X0))))))))),
% 4.10/1.00 inference(paramodulation,[status(thm)],[f3843,f47])).
% 4.10/1.00 fof(f3912,plain,(
% 4.10/1.00 ![X0]: (X0=join(X0,converse(complement(converse(complement(converse(converse(X0))))))))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f26,f3890])).
% 4.10/1.00 fof(f3913,plain,(
% 4.10/1.00 ![X0]: (X0=join(X0,converse(complement(converse(complement(X0))))))),
% 4.10/1.00 inference(forward_demodulation,[status(thm)],[f26,f3912])).
% 4.10/1.00 fof(f3936,plain,(
% 4.10/1.00 ![X0]: (meet(X0,complement(converse(complement(converse(complement(complement(X0)))))))=complement(complement(X0)))),
% 4.20/1.02 inference(paramodulation,[status(thm)],[f3913,f1888])).
% 4.20/1.02 fof(f3957,plain,(
% 4.20/1.02 ![X0]: (meet(X0,complement(converse(complement(converse(X0)))))=complement(complement(X0)))),
% 4.20/1.02 inference(forward_demodulation,[status(thm)],[f1829,f3936])).
% 4.20/1.02 fof(f3958,plain,(
% 4.20/1.02 ![X0]: (meet(X0,complement(converse(complement(converse(X0)))))=X0)),
% 4.20/1.02 inference(forward_demodulation,[status(thm)],[f1829,f3957])).
% 4.20/1.02 fof(f3984,plain,(
% 4.20/1.02 ![X0]: (complement(converse(complement(converse(X0))))=join(meet(complement(X0),complement(converse(complement(converse(X0))))),X0))),
% 4.20/1.02 inference(paramodulation,[status(thm)],[f3958,f2548])).
% 4.20/1.02 fof(f4019,plain,(
% 4.20/1.02 ![X0]: (complement(converse(complement(converse(X0))))=join(complement(join(X0,converse(complement(converse(X0))))),X0))),
% 4.20/1.02 inference(forward_demodulation,[status(thm)],[f3698,f3984])).
% 4.20/1.02 fof(f4020,plain,(
% 4.20/1.02 ![X0]: (complement(converse(complement(converse(X0))))=join(complement(top),X0))),
% 4.20/1.02 inference(forward_demodulation,[status(thm)],[f3015,f4019])).
% 4.20/1.02 fof(f4021,plain,(
% 4.20/1.02 ![X0]: (complement(converse(complement(converse(X0))))=join(zero,X0))),
% 4.20/1.02 inference(forward_demodulation,[status(thm)],[f407,f4020])).
% 4.20/1.02 fof(f4032,plain,(
% 4.20/1.02 ![X0]: (complement(converse(complement(converse(X0))))=X0)),
% 4.20/1.02 inference(forward_demodulation,[status(thm)],[f1904,f4021])).
% 4.20/1.02 fof(f4096,plain,(
% 4.20/1.02 ![X0]: (converse(complement(converse(X0)))=complement(X0))),
% 4.20/1.02 inference(paramodulation,[status(thm)],[f4032,f1829])).
% 4.20/1.02 fof(f4389,plain,(
% 4.20/1.02 ![X0]: (converse(complement(X0))=complement(converse(X0)))),
% 4.20/1.02 inference(paramodulation,[status(thm)],[f26,f4096])).
% 4.20/1.02 fof(f4428,plain,(
% 4.20/1.02 ~complement(converse(sK0_skl))=complement(converse(sK0_skl))),
% 4.20/1.02 inference(backward_demodulation,[status(thm)],[f4389,f37])).
% 4.20/1.02 fof(f4457,plain,(
% 4.20/1.02 $false),
% 4.20/1.02 inference(trivial_equality_resolution,[status(thm)],[f4428])).
% 4.20/1.02 % SZS output end CNFRefutation for theBenchmark.p
% 4.20/1.04 % Elapsed time: 0.668493 seconds
% 4.20/1.04 % CPU time: 5.135491 seconds
% 4.20/1.04 % Total memory used: 125.714 MB
% 4.20/1.04 % Net memory used: 123.658 MB
%------------------------------------------------------------------------------