%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL024+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 : n019.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:37 PM UTC 2026
% Result : Theorem 37.74s 5.26s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : REL024+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n019.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 04:01:36 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.45 % Drodi V4.1.1
% 37.74/5.26 % Refutation found
% 37.74/5.26 % SZS status Theorem for theBenchmark: Theorem is valid
% 37.74/5.26 % SZS output start CNFRefutation for theBenchmark
% 37.74/5.26 fof(f1,axiom,(
% 37.74/5.26 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 37.74/5.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.74/5.26 fof(f2,axiom,(
% 37.74/5.26 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 37.74/5.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.74/5.26 fof(f3,axiom,(
% 37.74/5.26 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 37.74/5.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.74/5.26 fof(f4,axiom,(
% 37.74/5.26 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 37.74/5.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.74/5.26 fof(f6,axiom,(
% 37.74/5.26 (! [X0] : composition(X0,one) = X0 )),
% 37.74/5.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.74/5.26 fof(f7,axiom,(
% 37.74/5.26 (! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) )),
% 37.74/5.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.74/5.26 fof(f8,axiom,(
% 37.74/5.26 (! [X0] : converse(converse(X0)) = X0 )),
% 37.74/5.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.74/5.26 fof(f9,axiom,(
% 37.74/5.26 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 37.74/5.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.74/5.26 fof(f10,axiom,(
% 37.74/5.26 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 37.74/5.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.74/5.26 fof(f11,axiom,(
% 37.74/5.26 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 37.74/5.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.74/5.26 fof(f12,axiom,(
% 37.74/5.26 (! [X0] : top = join(X0,complement(X0)) )),
% 37.74/5.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.74/5.26 fof(f13,axiom,(
% 37.74/5.26 (! [X0] : zero = meet(X0,complement(X0)) )),
% 37.74/5.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.74/5.26 fof(f14,conjecture,(
% 37.74/5.26 (! [X0,X1,X2] : join(composition(meet(X0,converse(X1)),meet(X1,X2)),composition(meet(X0,converse(X1)),X2)) = composition(meet(X0,converse(X1)),X2) )),
% 37.74/5.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.74/5.26 fof(f15,negated_conjecture,(
% 37.74/5.26 ~((! [X0,X1,X2] : join(composition(meet(X0,converse(X1)),meet(X1,X2)),composition(meet(X0,converse(X1)),X2)) = composition(meet(X0,converse(X1)),X2) ))),
% 37.74/5.26 inference(negated_conjecture,[status(cth)],[f14])).
% 37.74/5.26 fof(f16,plain,(
% 37.74/5.26 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 37.74/5.26 inference(cnf_transformation,[status(thm)],[f1])).
% 37.74/5.26 fof(f17,plain,(
% 37.74/5.26 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 37.74/5.26 inference(cnf_transformation,[status(thm)],[f2])).
% 37.74/5.26 fof(f18,plain,(
% 37.74/5.26 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 37.74/5.26 inference(cnf_transformation,[status(thm)],[f3])).
% 37.74/5.26 fof(f19,plain,(
% 37.74/5.26 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 37.74/5.26 inference(cnf_transformation,[status(thm)],[f4])).
% 37.74/5.26 fof(f21,plain,(
% 37.74/5.26 ![X0]: (composition(X0,one)=X0)),
% 37.74/5.26 inference(cnf_transformation,[status(thm)],[f6])).
% 37.74/5.26 fof(f22,plain,(
% 37.74/5.26 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 37.74/5.26 inference(cnf_transformation,[status(thm)],[f7])).
% 37.74/5.26 fof(f23,plain,(
% 37.74/5.26 ![X0]: (converse(converse(X0))=X0)),
% 37.74/5.26 inference(cnf_transformation,[status(thm)],[f8])).
% 37.74/5.26 fof(f24,plain,(
% 37.74/5.26 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 37.74/5.26 inference(cnf_transformation,[status(thm)],[f9])).
% 37.74/5.26 fof(f25,plain,(
% 37.74/5.26 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 37.74/5.26 inference(cnf_transformation,[status(thm)],[f10])).
% 37.74/5.26 fof(f26,plain,(
% 37.74/5.26 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 37.74/5.26 inference(cnf_transformation,[status(thm)],[f11])).
% 37.74/5.26 fof(f27,plain,(
% 37.74/5.26 ![X0]: (top=join(X0,complement(X0)))),
% 37.74/5.26 inference(cnf_transformation,[status(thm)],[f12])).
% 37.74/5.26 fof(f28,plain,(
% 37.74/5.26 ![X0]: (zero=meet(X0,complement(X0)))),
% 37.74/5.26 inference(cnf_transformation,[status(thm)],[f13])).
% 37.74/5.26 fof(f29,plain,(
% 37.74/5.26 (?[X0,X1,X2]: ~join(composition(meet(X0,converse(X1)),meet(X1,X2)),composition(meet(X0,converse(X1)),X2))=composition(meet(X0,converse(X1)),X2))),
% 37.74/5.26 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 37.74/5.26 fof(f30,plain,(
% 37.74/5.26 ~join(composition(meet(sK0_skl,converse(sK1_skl)),meet(sK1_skl,sK2_skl)),composition(meet(sK0_skl,converse(sK1_skl)),sK2_skl))=composition(meet(sK0_skl,converse(sK1_skl)),sK2_skl)),
% 37.74/5.26 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)],[f29])).
% 37.74/5.26 fof(f31,plain,(
% 37.74/5.26 ~join(composition(meet(sK0_skl,converse(sK1_skl)),meet(sK1_skl,sK2_skl)),composition(meet(sK0_skl,converse(sK1_skl)),sK2_skl))=composition(meet(sK0_skl,converse(sK1_skl)),sK2_skl)),
% 37.74/5.26 inference(cnf_transformation,[status(thm)],[f30])).
% 37.74/5.26 fof(f42,plain,(
% 37.74/5.26 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 37.74/5.26 inference(forward_demodulation,[status(thm)],[f16,f18])).
% 37.74/5.26 fof(f43,plain,(
% 37.74/5.26 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 37.74/5.26 inference(backward_demodulation,[status(thm)],[f19,f42])).
% 37.74/5.26 fof(f44,plain,(
% 37.74/5.26 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 37.74/5.26 inference(forward_demodulation,[status(thm)],[f16,f26])).
% 37.74/5.26 fof(f45,plain,(
% 37.74/5.26 ~join(composition(meet(sK0_skl,converse(sK1_skl)),sK2_skl),composition(meet(sK0_skl,converse(sK1_skl)),meet(sK1_skl,sK2_skl)))=composition(meet(sK0_skl,converse(sK1_skl)),sK2_skl)),
% 37.74/5.26 inference(forward_demodulation,[status(thm)],[f16,f31])).
% 37.74/5.26 fof(f46,plain,(
% 37.74/5.26 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 37.74/5.26 inference(forward_demodulation,[status(thm)],[f16,f43])).
% 37.74/5.26 fof(f55,plain,(
% 37.74/5.26 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 37.74/5.26 inference(paramodulation,[status(thm)],[f16,f19])).
% 37.74/5.26 fof(f59,plain,(
% 37.74/5.26 ![X0,X1]: (converse(composition(X0,converse(X1)))=composition(X1,converse(X0)))),
% 37.74/5.26 inference(paramodulation,[status(thm)],[f23,f25])).
% 37.74/5.26 fof(f60,plain,(
% 37.74/5.26 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f23,f25])).
% 37.74/5.27 fof(f62,plain,(
% 37.74/5.27 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f16,f17])).
% 37.74/5.27 fof(f65,plain,(
% 37.74/5.27 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X0),X2))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f16,f17])).
% 37.74/5.27 fof(f83,plain,(
% 37.74/5.27 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f19,f55])).
% 37.74/5.27 fof(f97,plain,(
% 37.74/5.27 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f16,f24])).
% 37.74/5.27 fof(f99,plain,(
% 37.74/5.27 ![X0,X1,X2]: (converse(join(composition(converse(X0),X1),X2))=join(composition(converse(X1),X0),converse(X2)))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f60,f24])).
% 37.74/5.27 fof(f179,plain,(
% 37.74/5.27 ![X0,X1]: (converse(join(converse(X0),X1))=join(converse(X1),X0))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f23,f97])).
% 37.74/5.27 fof(f287,plain,(
% 37.74/5.27 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f55,f46])).
% 37.74/5.27 fof(f295,plain,(
% 37.74/5.27 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f16,f287])).
% 37.74/5.27 fof(f302,plain,(
% 37.74/5.27 ![X0,X1]: (X0=join(meet(X1,X0),meet(complement(X1),X0)))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f83,f295])).
% 37.74/5.27 fof(f315,plain,(
% 37.74/5.27 ![X0,X1,X2]: (composition(join(X0,converse(X1)),converse(X2))=join(composition(X0,converse(X2)),converse(composition(X2,X1))))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f25,f22])).
% 37.74/5.27 fof(f344,plain,(
% 37.74/5.27 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f21,f60])).
% 37.74/5.27 fof(f350,plain,(
% 37.74/5.27 ![X0]: (X0=composition(converse(one),X0))),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f23,f344])).
% 37.74/5.27 fof(f363,plain,(
% 37.74/5.27 one=converse(one)),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f21,f350])).
% 37.74/5.27 fof(f364,plain,(
% 37.74/5.27 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f350,f44])).
% 37.74/5.27 fof(f373,plain,(
% 37.74/5.27 ![X0]: (X0=composition(one,X0))),
% 37.74/5.27 inference(backward_demodulation,[status(thm)],[f363,f350])).
% 37.74/5.27 fof(f381,plain,(
% 37.74/5.27 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 37.74/5.27 inference(backward_demodulation,[status(thm)],[f373,f364])).
% 37.74/5.27 fof(f429,plain,(
% 37.74/5.27 ![X0]: (meet(complement(X0),X0)=complement(top))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f27,f55])).
% 37.74/5.27 fof(f431,plain,(
% 37.74/5.27 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f27,f46])).
% 37.74/5.27 fof(f437,plain,(
% 37.74/5.27 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f83,f429])).
% 37.74/5.27 fof(f438,plain,(
% 37.74/5.27 zero=complement(top)),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f28,f437])).
% 37.74/5.27 fof(f440,plain,(
% 37.74/5.27 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(X0)))))),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f16,f431])).
% 37.74/5.27 fof(f441,plain,(
% 37.74/5.27 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f438,f440])).
% 37.74/5.27 fof(f469,plain,(
% 37.74/5.27 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f381,f55])).
% 37.74/5.27 fof(f510,plain,(
% 37.74/5.27 ![X0]: (join(meet(X0,X0),complement(complement(X0)))=complement(complement(X0)))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f469,f381])).
% 37.74/5.27 fof(f511,plain,(
% 37.74/5.27 ![X0]: (top=join(complement(X0),meet(X0,X0)))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f469,f27])).
% 37.74/5.27 fof(f512,plain,(
% 37.74/5.27 ![X0]: (zero=meet(complement(X0),meet(X0,X0)))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f469,f28])).
% 37.74/5.27 fof(f566,plain,(
% 37.74/5.27 ![X0]: (X0=join(meet(X0,meet(X0,X0)),complement(top)))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f511,f46])).
% 37.74/5.27 fof(f575,plain,(
% 37.74/5.27 ![X0]: (X0=join(complement(top),meet(X0,meet(X0,X0))))),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f16,f566])).
% 37.74/5.27 fof(f576,plain,(
% 37.74/5.27 ![X0]: (X0=join(zero,meet(X0,meet(X0,X0))))),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f438,f575])).
% 37.74/5.27 fof(f828,plain,(
% 37.74/5.27 ![X0]: (meet(X0,X0)=join(meet(X0,meet(X0,X0)),zero))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f512,f302])).
% 37.74/5.27 fof(f829,plain,(
% 37.74/5.27 ![X0]: (complement(complement(X0))=join(meet(X0,complement(complement(X0))),zero))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f28,f302])).
% 37.74/5.27 fof(f850,plain,(
% 37.74/5.27 ![X0]: (meet(X0,X0)=join(zero,meet(X0,meet(X0,X0))))),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f16,f828])).
% 37.74/5.27 fof(f872,plain,(
% 37.74/5.27 ![X0]: (join(X0,complement(complement(X0)))=complement(complement(X0)))),
% 37.74/5.27 inference(backward_demodulation,[status(thm)],[f875,f510])).
% 37.74/5.27 fof(f875,plain,(
% 37.74/5.27 ![X0]: (meet(X0,X0)=X0)),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f576,f850])).
% 37.74/5.27 fof(f876,plain,(
% 37.74/5.27 ![X0]: (complement(complement(X0))=join(zero,meet(X0,complement(complement(X0)))))),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f16,f829])).
% 37.74/5.27 fof(f882,plain,(
% 37.74/5.27 ![X0]: (complement(complement(X0))=X0)),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f441,f876])).
% 37.74/5.27 fof(f924,plain,(
% 37.74/5.27 ![X0]: (join(X0,X0)=complement(complement(X0)))),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f882,f872])).
% 37.74/5.27 fof(f928,plain,(
% 37.74/5.27 ![X0]: (join(X0,X0)=X0)),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f882,f924])).
% 37.74/5.27 fof(f1254,plain,(
% 37.74/5.27 ![X0,X1]: (join(X0,join(join(X1,X0),X1))=join(X1,X0))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f62,f928])).
% 37.74/5.27 fof(f1272,plain,(
% 37.74/5.27 ![X0,X1]: (join(X0,join(X0,join(X1,X1)))=join(X1,X0))),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f65,f1254])).
% 37.74/5.27 fof(f1275,plain,(
% 37.74/5.27 ![X0,X1]: (join(X0,join(X0,X1))=join(X1,X0))),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f928,f1272])).
% 37.74/5.27 fof(f1510,plain,(
% 37.74/5.27 ![X0,X1]: (join(meet(X0,X1),X1)=join(meet(complement(X0),X1),meet(X0,X1)))),
% 37.74/5.27 inference(paramodulation,[status(thm)],[f302,f1275])).
% 37.74/5.27 fof(f1559,plain,(
% 37.74/5.27 ![X0,X1]: (join(X0,meet(X1,X0))=join(meet(complement(X1),X0),meet(X1,X0)))),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f16,f1510])).
% 37.74/5.27 fof(f1560,plain,(
% 37.74/5.27 ![X0,X1]: (join(X0,meet(X1,X0))=join(meet(X1,X0),meet(complement(X1),X0)))),
% 37.74/5.27 inference(forward_demodulation,[status(thm)],[f16,f1559])).
% 37.74/5.27 fof(f1562,plain,(
% 37.74/5.27 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 29.87/5.34 inference(forward_demodulation,[status(thm)],[f302,f1560])).
% 29.87/5.34 fof(f13842,plain,(
% 29.87/5.34 ![X0,X1,X2]: (converse(composition(join(converse(X0),converse(X1)),converse(X2)))=join(composition(converse(converse(X2)),X0),converse(converse(composition(X2,X1)))))),
% 29.87/5.34 inference(paramodulation,[status(thm)],[f315,f99])).
% 29.87/5.34 fof(f13927,plain,(
% 29.87/5.34 ![X0,X1,X2]: (composition(X0,converse(join(converse(X1),converse(X2))))=join(composition(converse(converse(X0)),X1),converse(converse(composition(X0,X2)))))),
% 29.87/5.34 inference(forward_demodulation,[status(thm)],[f59,f13842])).
% 29.87/5.34 fof(f13928,plain,(
% 29.87/5.34 ![X0,X1,X2]: (composition(X0,join(converse(converse(X1)),X2))=join(composition(converse(converse(X0)),X2),converse(converse(composition(X0,X1)))))),
% 29.87/5.34 inference(forward_demodulation,[status(thm)],[f179,f13927])).
% 29.87/5.34 fof(f13929,plain,(
% 29.87/5.34 ![X0,X1,X2]: (composition(X0,join(X1,X2))=join(composition(converse(converse(X0)),X2),converse(converse(composition(X0,X1)))))),
% 29.87/5.34 inference(forward_demodulation,[status(thm)],[f23,f13928])).
% 29.87/5.34 fof(f13930,plain,(
% 29.87/5.34 ![X0,X1,X2]: (composition(X0,join(X1,X2))=join(composition(X0,X2),converse(converse(composition(X0,X1)))))),
% 29.87/5.34 inference(forward_demodulation,[status(thm)],[f23,f13929])).
% 29.87/5.34 fof(f13931,plain,(
% 29.87/5.34 ~composition(meet(sK0_skl,converse(sK1_skl)),join(meet(sK1_skl,sK2_skl),sK2_skl))=composition(meet(sK0_skl,converse(sK1_skl)),sK2_skl)),
% 29.87/5.34 inference(backward_demodulation,[status(thm)],[f13937,f45])).
% 29.87/5.34 fof(f13937,plain,(
% 29.87/5.34 ![X0,X1,X2]: (composition(X0,join(X1,X2))=join(composition(X0,X2),composition(X0,X1)))),
% 29.87/5.34 inference(forward_demodulation,[status(thm)],[f23,f13930])).
% 29.87/5.34 fof(f14060,plain,(
% 29.87/5.34 ~composition(meet(sK0_skl,converse(sK1_skl)),join(sK2_skl,meet(sK1_skl,sK2_skl)))=composition(meet(sK0_skl,converse(sK1_skl)),sK2_skl)),
% 29.87/5.34 inference(forward_demodulation,[status(thm)],[f16,f13931])).
% 29.87/5.34 fof(f14061,plain,(
% 29.87/5.34 ~composition(meet(sK0_skl,converse(sK1_skl)),sK2_skl)=composition(meet(sK0_skl,converse(sK1_skl)),sK2_skl)),
% 29.87/5.34 inference(forward_demodulation,[status(thm)],[f1562,f14060])).
% 29.87/5.34 fof(f14062,plain,(
% 29.87/5.34 $false),
% 29.87/5.34 inference(trivial_equality_resolution,[status(thm)],[f14061])).
% 29.87/5.34 % SZS output end CNFRefutation for theBenchmark.p
% 29.87/5.37 % Elapsed time: 4.908618 seconds
% 29.87/5.37 % CPU time: 38.534800 seconds
% 29.87/5.37 % Total memory used: 239.534 MB
% 29.87/5.37 % Net memory used: 233.979 MB
%------------------------------------------------------------------------------