%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL012+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:34 PM UTC 2026
% Result : Theorem 16.56s 2.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL012+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 04:01:00 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 16.56/2.58 % Refutation found
% 16.56/2.58 % SZS status Theorem for theBenchmark: Theorem is valid
% 16.56/2.58 % SZS output start CNFRefutation for theBenchmark
% 16.56/2.58 fof(f1,axiom,(
% 16.56/2.58 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 16.56/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.56/2.58 fof(f2,axiom,(
% 16.56/2.58 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 16.56/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.56/2.58 fof(f3,axiom,(
% 16.56/2.58 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 16.56/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.56/2.58 fof(f4,axiom,(
% 16.56/2.58 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 16.56/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.56/2.58 fof(f6,axiom,(
% 16.56/2.58 (! [X0] : composition(X0,one) = X0 )),
% 16.56/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.56/2.58 fof(f8,axiom,(
% 16.56/2.58 (! [X0] : converse(converse(X0)) = X0 )),
% 16.56/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.56/2.58 fof(f9,axiom,(
% 16.56/2.58 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 16.56/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.56/2.58 fof(f10,axiom,(
% 16.56/2.58 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 16.56/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.56/2.58 fof(f11,axiom,(
% 16.56/2.58 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 16.56/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.56/2.58 fof(f12,axiom,(
% 16.56/2.58 (! [X0] : top = join(X0,complement(X0)) )),
% 16.56/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.56/2.58 fof(f13,axiom,(
% 16.56/2.58 (! [X0] : zero = meet(X0,complement(X0)) )),
% 16.56/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.56/2.58 fof(f14,conjecture,(
% 16.56/2.58 (! [X0,X1] : join(composition(complement(composition(X0,X1)),converse(X1)),complement(X0)) = complement(X0) )),
% 16.56/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.56/2.58 fof(f15,negated_conjecture,(
% 16.56/2.58 ~((! [X0,X1] : join(composition(complement(composition(X0,X1)),converse(X1)),complement(X0)) = complement(X0) ))),
% 16.56/2.58 inference(negated_conjecture,[status(cth)],[f14])).
% 16.56/2.58 fof(f16,plain,(
% 16.56/2.58 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 16.56/2.58 inference(cnf_transformation,[status(thm)],[f1])).
% 16.56/2.58 fof(f17,plain,(
% 16.56/2.58 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 16.56/2.58 inference(cnf_transformation,[status(thm)],[f2])).
% 16.56/2.58 fof(f18,plain,(
% 16.56/2.58 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 16.56/2.58 inference(cnf_transformation,[status(thm)],[f3])).
% 16.56/2.58 fof(f19,plain,(
% 16.56/2.58 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 16.56/2.58 inference(cnf_transformation,[status(thm)],[f4])).
% 16.56/2.58 fof(f21,plain,(
% 16.56/2.58 ![X0]: (composition(X0,one)=X0)),
% 16.56/2.58 inference(cnf_transformation,[status(thm)],[f6])).
% 16.56/2.58 fof(f23,plain,(
% 16.56/2.58 ![X0]: (converse(converse(X0))=X0)),
% 16.56/2.58 inference(cnf_transformation,[status(thm)],[f8])).
% 16.56/2.58 fof(f24,plain,(
% 16.56/2.58 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 16.56/2.58 inference(cnf_transformation,[status(thm)],[f9])).
% 16.56/2.58 fof(f25,plain,(
% 16.56/2.58 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 16.56/2.58 inference(cnf_transformation,[status(thm)],[f10])).
% 16.56/2.58 fof(f26,plain,(
% 16.56/2.58 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 16.56/2.58 inference(cnf_transformation,[status(thm)],[f11])).
% 16.56/2.58 fof(f27,plain,(
% 16.56/2.58 ![X0]: (top=join(X0,complement(X0)))),
% 16.56/2.58 inference(cnf_transformation,[status(thm)],[f12])).
% 16.56/2.58 fof(f28,plain,(
% 16.56/2.58 ![X0]: (zero=meet(X0,complement(X0)))),
% 16.56/2.58 inference(cnf_transformation,[status(thm)],[f13])).
% 16.56/2.58 fof(f29,plain,(
% 16.56/2.58 (?[X0,X1]: ~join(composition(complement(composition(X0,X1)),converse(X1)),complement(X0))=complement(X0))),
% 16.56/2.58 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 16.56/2.58 fof(f30,plain,(
% 16.56/2.58 ~join(composition(complement(composition(sK0_skl,sK1_skl)),converse(sK1_skl)),complement(sK0_skl))=complement(sK0_skl)),
% 16.56/2.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl)],[f29])).
% 16.56/2.58 fof(f31,plain,(
% 16.56/2.58 ~join(composition(complement(composition(sK0_skl,sK1_skl)),converse(sK1_skl)),complement(sK0_skl))=complement(sK0_skl)),
% 16.56/2.58 inference(cnf_transformation,[status(thm)],[f30])).
% 16.56/2.58 fof(f39,plain,(
% 16.56/2.58 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 16.56/2.58 inference(backward_demodulation,[status(thm)],[f19,f18])).
% 16.56/2.58 fof(f45,plain,(
% 16.56/2.58 ~join(complement(sK0_skl),composition(complement(composition(sK0_skl,sK1_skl)),converse(sK1_skl)))=complement(sK0_skl)),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f16,f31])).
% 16.56/2.58 fof(f50,plain,(
% 16.56/2.58 ![X0,X1]: (converse(composition(X0,converse(X1)))=composition(X1,converse(X0)))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f23,f25])).
% 16.56/2.58 fof(f51,plain,(
% 16.56/2.58 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f23,f25])).
% 16.56/2.58 fof(f53,plain,(
% 16.56/2.58 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f16,f17])).
% 16.56/2.58 fof(f74,plain,(
% 16.56/2.58 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f16,f24])).
% 16.56/2.58 fof(f151,plain,(
% 16.56/2.58 ![X0,X1,X2]: (converse(join(X0,composition(X1,converse(X2))))=join(composition(X2,converse(X1)),converse(X0)))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f50,f74])).
% 16.56/2.58 fof(f156,plain,(
% 16.56/2.58 ![X0,X1]: (converse(join(converse(X0),X1))=join(converse(X1),X0))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f23,f74])).
% 16.56/2.58 fof(f262,plain,(
% 16.56/2.58 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(X1,complement(X0)))))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f16,f39])).
% 16.56/2.58 fof(f265,plain,(
% 16.56/2.58 ![X0,X1,X2]: (join(meet(X0,X1),join(complement(join(complement(X0),X1)),X2))=join(X0,X2))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f39,f17])).
% 16.56/2.58 fof(f314,plain,(
% 16.56/2.58 ![X0,X1]: (join(composition(converse(converse(X0)),complement(converse(composition(X1,X0)))),complement(converse(X1)))=complement(converse(X1)))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f25,f26])).
% 16.56/2.58 fof(f325,plain,(
% 16.56/2.58 ![X0,X1]: (join(composition(X0,complement(converse(composition(X1,X0)))),complement(converse(X1)))=complement(converse(X1)))),
% 16.56/2.58 inference(forward_demodulation,[status(thm)],[f23,f314])).
% 16.56/2.58 fof(f382,plain,(
% 16.56/2.58 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f21,f51])).
% 16.56/2.58 fof(f391,plain,(
% 16.56/2.58 ![X0]: (X0=composition(converse(one),X0))),
% 16.56/2.58 inference(forward_demodulation,[status(thm)],[f23,f382])).
% 16.56/2.58 fof(f406,plain,(
% 16.56/2.58 ![X0]: (converse(top)=join(converse(complement(converse(X0))),X0))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f27,f156])).
% 16.56/2.58 fof(f411,plain,(
% 16.56/2.58 ![X0]: (X0=join(meet(X0,X0),complement(top)))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f27,f262])).
% 16.56/2.58 fof(f413,plain,(
% 16.56/2.58 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f27,f17])).
% 16.56/2.58 fof(f416,plain,(
% 16.56/2.58 one=converse(one)),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f21,f391])).
% 16.56/2.58 fof(f418,plain,(
% 16.56/2.58 ![X0]: (join(complement(composition(one,X0)),complement(X0))=complement(X0))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f391,f26])).
% 16.56/2.58 fof(f430,plain,(
% 16.56/2.58 ![X0]: (X0=composition(one,X0))),
% 16.56/2.58 inference(backward_demodulation,[status(thm)],[f416,f391])).
% 16.56/2.58 fof(f440,plain,(
% 16.56/2.58 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 16.56/2.58 inference(backward_demodulation,[status(thm)],[f430,f418])).
% 16.56/2.58 fof(f497,plain,(
% 16.56/2.58 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f440,f19])).
% 16.56/2.58 fof(f498,plain,(
% 16.56/2.58 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f27,f19])).
% 16.56/2.58 fof(f499,plain,(
% 16.56/2.58 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f16,f19])).
% 16.56/2.58 fof(f514,plain,(
% 16.56/2.58 ![X0]: (X0=join(meet(X0,X0),zero))),
% 16.56/2.58 inference(backward_demodulation,[status(thm)],[f518,f411])).
% 16.56/2.58 fof(f518,plain,(
% 16.56/2.58 zero=complement(top)),
% 16.56/2.58 inference(forward_demodulation,[status(thm)],[f28,f498])).
% 16.56/2.58 fof(f526,plain,(
% 16.56/2.58 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f518,f19])).
% 16.56/2.58 fof(f528,plain,(
% 16.56/2.58 join(complement(top),zero)=complement(top)),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f518,f440])).
% 16.56/2.58 fof(f535,plain,(
% 16.56/2.58 join(zero,zero)=complement(top)),
% 16.56/2.58 inference(forward_demodulation,[status(thm)],[f518,f528])).
% 16.56/2.58 fof(f536,plain,(
% 16.56/2.58 join(zero,zero)=zero),
% 16.56/2.58 inference(forward_demodulation,[status(thm)],[f518,f535])).
% 16.56/2.58 fof(f553,plain,(
% 16.56/2.58 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f497,f514])).
% 16.56/2.58 fof(f563,plain,(
% 16.56/2.58 ![X0]: (top=join(complement(X0),meet(X0,X0)))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f497,f27])).
% 16.56/2.58 fof(f592,plain,(
% 16.56/2.58 ![X0]: (join(X0,zero)=join(zero,join(X0,zero)))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f536,f53])).
% 16.56/2.58 fof(f633,plain,(
% 16.56/2.58 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(X1,top))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f27,f53])).
% 16.56/2.58 fof(f776,plain,(
% 16.56/2.58 ![X0,X1]: (join(meet(X0,X1),complement(join(complement(X0),X1)))=join(X0,complement(join(complement(X0),X1))))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f440,f265])).
% 16.56/2.58 fof(f802,plain,(
% 16.56/2.58 ![X0,X1]: (X0=join(X0,complement(join(complement(X0),X1))))),
% 16.56/2.58 inference(forward_demodulation,[status(thm)],[f39,f776])).
% 16.56/2.58 fof(f819,plain,(
% 16.56/2.58 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(meet(X0,X1)),zero))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f19,f553])).
% 16.56/2.58 fof(f1070,plain,(
% 16.56/2.58 ![X0,X1]: (X0=join(X0,meet(X0,X1)))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f19,f802])).
% 16.56/2.58 fof(f1072,plain,(
% 16.56/2.58 ![X0]: (X0=join(X0,complement(top)))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f563,f802])).
% 16.56/2.58 fof(f1101,plain,(
% 16.56/2.58 ![X0]: (X0=complement(complement(X0)))),
% 16.56/2.58 inference(backward_demodulation,[status(thm)],[f1118,f553])).
% 16.56/2.58 fof(f1109,plain,(
% 16.56/2.58 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 16.56/2.58 inference(backward_demodulation,[status(thm)],[f1118,f819])).
% 16.56/2.58 fof(f1116,plain,(
% 16.56/2.58 ![X0]: (join(X0,zero)=join(zero,X0))),
% 16.56/2.58 inference(backward_demodulation,[status(thm)],[f1118,f592])).
% 16.56/2.58 fof(f1118,plain,(
% 16.56/2.58 ![X0]: (X0=join(X0,zero))),
% 16.56/2.58 inference(forward_demodulation,[status(thm)],[f518,f1072])).
% 16.56/2.58 fof(f1210,plain,(
% 16.56/2.58 ![X0,X1]: (meet(X0,X1)=complement(complement(meet(X1,X0))))),
% 16.56/2.58 inference(backward_demodulation,[status(thm)],[f1109,f499])).
% 16.56/2.58 fof(f1220,plain,(
% 16.56/2.58 ![X0]: (meet(top,X0)=complement(complement(X0)))),
% 16.56/2.58 inference(backward_demodulation,[status(thm)],[f1229,f526])).
% 16.56/2.58 fof(f1229,plain,(
% 16.56/2.58 ![X0]: (X0=join(zero,X0))),
% 16.56/2.58 inference(forward_demodulation,[status(thm)],[f1118,f1116])).
% 16.56/2.58 fof(f1275,plain,(
% 16.56/2.58 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 16.56/2.58 inference(forward_demodulation,[status(thm)],[f1101,f1210])).
% 16.56/2.58 fof(f1281,plain,(
% 16.56/2.58 ![X0]: (meet(top,X0)=X0)),
% 16.56/2.58 inference(forward_demodulation,[status(thm)],[f1101,f1220])).
% 16.56/2.58 fof(f1643,plain,(
% 16.56/2.58 ![X0]: (top=join(top,X0))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f1281,f1070])).
% 16.56/2.58 fof(f1649,plain,(
% 16.56/2.58 ![X0,X1]: (converse(converse(X0))=join(converse(meet(converse(X0),X1)),X0))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f1070,f156])).
% 16.56/2.58 fof(f1665,plain,(
% 16.56/2.58 ![X0,X1]: (join(X0,join(complement(X0),X1))=top)),
% 16.56/2.58 inference(backward_demodulation,[status(thm)],[f1643,f413])).
% 16.56/2.58 fof(f1668,plain,(
% 16.56/2.58 ![X0,X1]: (X0=join(converse(meet(converse(X0),X1)),X0))),
% 16.56/2.58 inference(forward_demodulation,[status(thm)],[f23,f1649])).
% 16.56/2.58 fof(f1677,plain,(
% 16.56/2.58 ![X0]: (top=join(X0,top))),
% 16.56/2.58 inference(backward_demodulation,[status(thm)],[f1665,f633])).
% 16.56/2.58 fof(f2364,plain,(
% 16.56/2.58 ![X0,X1]: (X0=join(converse(meet(X1,converse(X0))),X0))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f1275,f1668])).
% 16.56/2.58 fof(f5219,plain,(
% 16.56/2.58 converse(top)=top),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f1677,f406])).
% 16.56/2.58 fof(f5246,plain,(
% 16.56/2.58 ![X0]: (X0=join(meet(X0,converse(complement(converse(complement(X0))))),complement(converse(top))))),
% 16.56/2.58 inference(paramodulation,[status(thm)],[f406,f262])).
% 16.56/2.58 fof(f5316,plain,(
% 16.56/2.58 ![X0]: (X0=join(meet(X0,converse(complement(converse(complement(X0))))),complement(top)))),
% 16.56/2.58 inference(forward_demodulation,[status(thm)],[f5219,f5246])).
% 16.56/2.58 fof(f5317,plain,(
% 16.56/2.58 ![X0]: (X0=join(meet(X0,converse(complement(converse(complement(X0))))),zero))),
% 16.56/2.58 inference(forward_demodulation,[status(thm)],[f518,f5316])).
% 16.56/2.58 fof(f5318,plain,(
% 16.56/2.58 ![X0]: (X0=meet(X0,converse(complement(converse(complement(X0))))))),
% 17.36/2.67 inference(forward_demodulation,[status(thm)],[f1118,f5317])).
% 17.36/2.67 fof(f5514,plain,(
% 17.36/2.67 ![X0]: (complement(converse(complement(X0)))=join(converse(X0),complement(converse(complement(X0)))))),
% 17.36/2.67 inference(paramodulation,[status(thm)],[f5318,f2364])).
% 17.36/2.67 fof(f6305,plain,(
% 17.36/2.67 ![X0,X1]: (join(X0,complement(X1))=complement(meet(complement(X0),X1)))),
% 17.36/2.67 inference(paramodulation,[status(thm)],[f1101,f1109])).
% 17.36/2.67 fof(f9913,plain,(
% 17.36/2.67 ![X0]: (join(X0,complement(converse(complement(converse(complement(complement(X0)))))))=complement(complement(X0)))),
% 17.36/2.67 inference(paramodulation,[status(thm)],[f5318,f6305])).
% 17.36/2.67 fof(f9967,plain,(
% 17.36/2.67 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=complement(complement(X0)))),
% 17.36/2.67 inference(forward_demodulation,[status(thm)],[f1101,f9913])).
% 17.36/2.67 fof(f9968,plain,(
% 17.36/2.67 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=X0)),
% 17.36/2.67 inference(forward_demodulation,[status(thm)],[f1101,f9967])).
% 17.36/2.67 fof(f10028,plain,(
% 17.36/2.67 ![X0]: (join(converse(X0),complement(converse(complement(X0))))=converse(X0))),
% 17.36/2.67 inference(paramodulation,[status(thm)],[f23,f9968])).
% 17.36/2.67 fof(f10071,plain,(
% 17.36/2.67 ![X0]: (complement(converse(complement(X0)))=converse(X0))),
% 17.36/2.67 inference(backward_demodulation,[status(thm)],[f10028,f5514])).
% 17.36/2.67 fof(f10198,plain,(
% 17.36/2.67 ![X0]: (complement(converse(X0))=converse(complement(X0)))),
% 17.36/2.67 inference(paramodulation,[status(thm)],[f1101,f10071])).
% 17.36/2.67 fof(f10242,plain,(
% 17.36/2.67 ![X0,X1]: (join(composition(X0,converse(complement(composition(X1,X0)))),complement(converse(X1)))=complement(converse(X1)))),
% 17.36/2.67 inference(backward_demodulation,[status(thm)],[f10198,f325])).
% 17.36/2.67 fof(f10331,plain,(
% 17.36/2.67 ![X0,X1]: (join(composition(X0,converse(complement(composition(X1,X0)))),converse(complement(X1)))=complement(converse(X1)))),
% 17.36/2.67 inference(forward_demodulation,[status(thm)],[f10198,f10242])).
% 17.36/2.67 fof(f10332,plain,(
% 17.36/2.67 ![X0,X1]: (converse(join(complement(X0),composition(complement(composition(X0,X1)),converse(X1))))=complement(converse(X0)))),
% 17.36/2.67 inference(forward_demodulation,[status(thm)],[f151,f10331])).
% 17.36/2.67 fof(f10333,plain,(
% 17.36/2.67 ![X0,X1]: (converse(join(complement(X0),composition(complement(composition(X0,X1)),converse(X1))))=converse(complement(X0)))),
% 17.36/2.67 inference(forward_demodulation,[status(thm)],[f10198,f10332])).
% 17.36/2.67 fof(f10921,plain,(
% 17.36/2.67 ![X0,X1]: (converse(converse(complement(X0)))=join(complement(X0),composition(complement(composition(X0,X1)),converse(X1))))),
% 17.36/2.67 inference(paramodulation,[status(thm)],[f10333,f23])).
% 17.36/2.67 fof(f11001,plain,(
% 17.36/2.67 ~complement(sK0_skl)=complement(sK0_skl)),
% 17.36/2.67 inference(backward_demodulation,[status(thm)],[f11015,f45])).
% 17.36/2.67 fof(f11015,plain,(
% 17.36/2.67 ![X0,X1]: (complement(X0)=join(complement(X0),composition(complement(composition(X0,X1)),converse(X1))))),
% 17.36/2.67 inference(forward_demodulation,[status(thm)],[f23,f10921])).
% 17.36/2.67 fof(f11016,plain,(
% 17.36/2.67 $false),
% 17.36/2.67 inference(trivial_equality_resolution,[status(thm)],[f11001])).
% 17.36/2.67 % SZS output end CNFRefutation for theBenchmark.p
% 11.31/13.54 % Elapsed time: 13.168353 seconds
% 11.31/13.54 % CPU time: 102.545611 seconds
% 11.31/13.54 % Total memory used: 58.450 GB
% 11.31/13.54 % Net memory used: 58.448 GB
%------------------------------------------------------------------------------