%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL011-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : 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 : Unsatisfiable 38.94s 5.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : REL011-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.45 % Computer : n018.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Mon Sep 21 04:01:01 UTC 2026
% 0.20/0.45 % CPUTime :
% 0.20/0.46 % Drodi V4.1.1
% 38.94/5.48 % Refutation found
% 38.94/5.48 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 38.94/5.48 % SZS output start CNFRefutation for theBenchmark
% 38.94/5.48 fof(f1,axiom,(
% 38.94/5.48 (![A,B]: (join(A,B) = join(B,A) ))),
% 38.94/5.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.94/5.48 fof(f2,axiom,(
% 38.94/5.48 (![A,B,C]: (join(A,join(B,C)) = join(join(A,B),C) ))),
% 38.94/5.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.94/5.48 fof(f3,axiom,(
% 38.94/5.48 (![A,B]: (A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))) ))),
% 38.94/5.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.94/5.48 fof(f4,axiom,(
% 38.94/5.48 (![A,B]: (meet(A,B) = complement(join(complement(A),complement(B))) ))),
% 38.94/5.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.94/5.48 fof(f5,axiom,(
% 38.94/5.48 (![A,B,C]: (composition(A,composition(B,C)) = composition(composition(A,B),C) ))),
% 38.94/5.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.94/5.48 fof(f6,axiom,(
% 38.94/5.48 (![A]: (composition(A,one) = A ))),
% 38.94/5.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.94/5.48 fof(f7,axiom,(
% 38.94/5.48 (![A,B,C]: (composition(join(A,B),C) = join(composition(A,C),composition(B,C)) ))),
% 38.94/5.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.94/5.48 fof(f8,axiom,(
% 38.94/5.48 (![A]: (converse(converse(A)) = A ))),
% 38.94/5.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.94/5.48 fof(f9,axiom,(
% 38.94/5.48 (![A,B]: (converse(join(A,B)) = join(converse(A),converse(B)) ))),
% 38.94/5.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.94/5.48 fof(f10,axiom,(
% 38.94/5.48 (![A,B]: (converse(composition(A,B)) = composition(converse(B),converse(A)) ))),
% 38.94/5.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.94/5.48 fof(f11,axiom,(
% 38.94/5.48 (![A,B]: (join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B) ))),
% 38.94/5.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.94/5.48 fof(f12,axiom,(
% 38.94/5.48 (![A]: (top = join(A,complement(A)) ))),
% 38.94/5.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.94/5.48 fof(f13,axiom,(
% 38.94/5.48 (![A]: (zero = meet(A,complement(A)) ))),
% 38.94/5.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.94/5.48 fof(f14,axiom,(
% 38.94/5.48 (![A,B,C]: (join(meet(composition(A,B),C),composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C)))) = composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C))) ))),
% 38.94/5.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.94/5.48 fof(f17,negated_conjecture,(
% 38.94/5.48 meet(sk1,composition(converse(sk2),sk3)) = zero ),
% 38.94/5.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.94/5.48 fof(f18,negated_conjecture,(
% 38.94/5.48 meet(composition(sk2,sk1),sk3) != zero ),
% 38.94/5.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.94/5.48 fof(f19,plain,(
% 38.94/5.48 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 38.94/5.48 inference(cnf_transformation,[status(thm)],[f1])).
% 38.94/5.48 fof(f20,plain,(
% 38.94/5.48 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 38.94/5.48 inference(cnf_transformation,[status(thm)],[f2])).
% 38.94/5.48 fof(f21,plain,(
% 38.94/5.48 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 38.94/5.48 inference(cnf_transformation,[status(thm)],[f3])).
% 38.94/5.48 fof(f22,plain,(
% 38.94/5.48 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 38.94/5.49 inference(cnf_transformation,[status(thm)],[f4])).
% 38.94/5.49 fof(f23,plain,(
% 38.94/5.49 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 38.94/5.49 inference(cnf_transformation,[status(thm)],[f5])).
% 38.94/5.49 fof(f24,plain,(
% 38.94/5.49 ![X0]: (composition(X0,one)=X0)),
% 38.94/5.49 inference(cnf_transformation,[status(thm)],[f6])).
% 38.94/5.49 fof(f25,plain,(
% 38.94/5.49 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 38.94/5.49 inference(cnf_transformation,[status(thm)],[f7])).
% 38.94/5.49 fof(f26,plain,(
% 38.94/5.49 ![X0]: (converse(converse(X0))=X0)),
% 38.94/5.49 inference(cnf_transformation,[status(thm)],[f8])).
% 38.94/5.49 fof(f27,plain,(
% 38.94/5.49 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 38.94/5.49 inference(cnf_transformation,[status(thm)],[f9])).
% 38.94/5.49 fof(f28,plain,(
% 38.94/5.49 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 38.94/5.49 inference(cnf_transformation,[status(thm)],[f10])).
% 38.94/5.49 fof(f29,plain,(
% 38.94/5.49 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 38.94/5.49 inference(cnf_transformation,[status(thm)],[f11])).
% 38.94/5.49 fof(f30,plain,(
% 38.94/5.49 ![X0]: (top=join(X0,complement(X0)))),
% 38.94/5.49 inference(cnf_transformation,[status(thm)],[f12])).
% 38.94/5.49 fof(f31,plain,(
% 38.94/5.49 ![X0]: (zero=meet(X0,complement(X0)))),
% 38.94/5.49 inference(cnf_transformation,[status(thm)],[f13])).
% 38.94/5.49 fof(f32,plain,(
% 38.94/5.49 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))))=composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))))),
% 38.94/5.49 inference(cnf_transformation,[status(thm)],[f14])).
% 38.94/5.49 fof(f35,plain,(
% 38.94/5.49 meet(sk1,composition(converse(sk2),sk3))=zero),
% 38.94/5.49 inference(cnf_transformation,[status(thm)],[f17])).
% 38.94/5.49 fof(f36,plain,(
% 38.94/5.49 ~meet(composition(sk2,sk1),sk3)=zero),
% 38.94/5.49 inference(cnf_transformation,[status(thm)],[f18])).
% 38.94/5.49 fof(f45,plain,(
% 38.94/5.49 ![X0,X1]: (join(X0,join(X1,complement(join(X0,X1))))=top)),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f30,f20])).
% 38.94/5.49 fof(f49,plain,(
% 38.94/5.49 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f30,f20])).
% 38.94/5.49 fof(f57,plain,(
% 38.94/5.49 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f30,f22])).
% 38.94/5.49 fof(f58,plain,(
% 38.94/5.49 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f19,f22])).
% 38.94/5.49 fof(f64,plain,(
% 38.94/5.49 zero=complement(top)),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f31,f57])).
% 38.94/5.49 fof(f67,plain,(
% 38.94/5.49 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f64,f22])).
% 38.94/5.49 fof(f73,plain,(
% 38.94/5.49 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f24,f23])).
% 38.94/5.49 fof(f88,plain,(
% 38.94/5.49 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f26,f27])).
% 38.94/5.49 fof(f93,plain,(
% 38.94/5.49 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f19,f21])).
% 38.94/5.49 fof(f94,plain,(
% 38.94/5.49 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f22,f93])).
% 38.94/5.49 fof(f95,plain,(
% 38.94/5.49 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f19,f94])).
% 38.94/5.49 fof(f114,plain,(
% 38.94/5.49 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f26,f28])).
% 38.94/5.49 fof(f239,plain,(
% 38.94/5.49 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X1,X2),composition(X0,X2)))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f19,f25])).
% 38.94/5.49 fof(f366,plain,(
% 38.94/5.49 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f19,f29])).
% 38.94/5.49 fof(f368,plain,(
% 38.94/5.49 ![X0,X1,X2]: (join(meet(X0,X1),composition(converse(X2),complement(composition(X2,join(complement(X0),complement(X1))))))=complement(join(complement(X0),complement(X1))))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f22,f366])).
% 38.94/5.49 fof(f382,plain,(
% 38.94/5.49 ![X0,X1,X2]: (join(meet(X0,X1),composition(converse(X2),complement(composition(X2,join(complement(X0),complement(X1))))))=meet(X0,X1))),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f22,f368])).
% 38.94/5.49 fof(f390,plain,(
% 38.94/5.49 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f22,f58])).
% 38.94/5.49 fof(f423,plain,(
% 38.94/5.49 ~meet(sk3,composition(sk2,sk1))=zero),
% 38.94/5.49 inference(backward_demodulation,[status(thm)],[f390,f36])).
% 38.94/5.49 fof(f715,plain,(
% 38.94/5.49 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f24,f114])).
% 38.94/5.49 fof(f739,plain,(
% 38.94/5.49 ![X0]: (X0=composition(converse(one),X0))),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f26,f715])).
% 38.94/5.49 fof(f762,plain,(
% 38.94/5.49 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f73,f739])).
% 38.94/5.49 fof(f780,plain,(
% 38.94/5.49 ![X0]: (composition(one,X0)=X0)),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f739,f762])).
% 38.94/5.49 fof(f810,plain,(
% 38.94/5.49 ![X0]: (join(complement(X0),composition(converse(one),complement(X0)))=complement(X0))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f780,f366])).
% 38.94/5.49 fof(f829,plain,(
% 38.94/5.49 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f739,f810])).
% 38.94/5.49 fof(f936,plain,(
% 38.94/5.49 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f829,f58])).
% 38.94/5.49 fof(f938,plain,(
% 38.94/5.49 ![X0]: (join(X0,complement(X0))=join(top,complement(X0)))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f829,f49])).
% 38.94/5.49 fof(f939,plain,(
% 38.94/5.49 ![X0]: (X0=join(meet(X0,complement(X0)),complement(complement(X0))))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f829,f95])).
% 38.94/5.49 fof(f970,plain,(
% 38.94/5.49 ![X0]: (top=join(top,complement(X0)))),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f30,f938])).
% 38.94/5.49 fof(f971,plain,(
% 38.94/5.49 ![X0]: (X0=join(complement(complement(X0)),meet(X0,complement(X0))))),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f19,f939])).
% 38.94/5.49 fof(f972,plain,(
% 38.94/5.49 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f31,f971])).
% 38.94/5.49 fof(f973,plain,(
% 38.94/5.49 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f19,f972])).
% 38.94/5.49 fof(f1010,plain,(
% 38.94/5.49 join(meet(composition(sk2,sk1),sk3),composition(meet(sk2,composition(sk3,converse(sk1))),zero))=composition(meet(sk2,composition(sk3,converse(sk1))),meet(sk1,composition(converse(sk2),sk3)))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f35,f32])).
% 38.94/5.49 fof(f1015,plain,(
% 38.94/5.49 join(meet(sk3,composition(sk2,sk1)),composition(meet(sk2,composition(sk3,converse(sk1))),zero))=composition(meet(sk2,composition(sk3,converse(sk1))),meet(sk1,composition(converse(sk2),sk3)))),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f390,f1010])).
% 38.94/5.49 fof(f1016,plain,(
% 38.94/5.49 join(meet(sk3,composition(sk2,sk1)),composition(meet(sk2,composition(sk3,converse(sk1))),zero))=composition(meet(sk2,composition(sk3,converse(sk1))),zero)),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f35,f1015])).
% 38.94/5.49 fof(f1023,plain,(
% 38.94/5.49 ![X0]: (join(X0,top)=top)),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f970,f45])).
% 38.94/5.49 fof(f1036,plain,(
% 38.94/5.49 ![X0]: (join(top,X0)=top)),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f19,f1023])).
% 38.94/5.49 fof(f1038,plain,(
% 38.94/5.49 ![X0]: (converse(top)=join(X0,converse(top)))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f1023,f88])).
% 38.94/5.49 fof(f1040,plain,(
% 38.94/5.49 ![X0]: (X0=join(meet(X0,top),complement(top)))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f1023,f95])).
% 38.94/5.49 fof(f1053,plain,(
% 38.94/5.49 ![X0]: (X0=join(complement(top),meet(X0,top)))),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f19,f1040])).
% 38.94/5.49 fof(f1054,plain,(
% 38.94/5.49 ![X0]: (X0=join(zero,meet(X0,top)))),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f64,f1053])).
% 38.94/5.49 fof(f1151,plain,(
% 38.94/5.49 ![X0]: (meet(top,complement(X0))=complement(X0))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f973,f67])).
% 38.94/5.49 fof(f1167,plain,(
% 38.94/5.49 ![X0]: (X0=join(zero,meet(top,X0)))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f390,f1054])).
% 38.94/5.49 fof(f1247,plain,(
% 38.94/5.49 ![X0]: (complement(X0)=join(zero,complement(X0)))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f1151,f1167])).
% 38.94/5.49 fof(f1265,plain,(
% 38.94/5.49 ![X0]: (X0=complement(complement(X0)))),
% 38.94/5.49 inference(backward_demodulation,[status(thm)],[f1247,f973])).
% 38.94/5.49 fof(f1269,plain,(
% 38.94/5.49 complement(zero)=top),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f30,f1247])).
% 38.94/5.49 fof(f1286,plain,(
% 38.94/5.49 ![X0]: (meet(X0,X0)=X0)),
% 38.94/5.49 inference(backward_demodulation,[status(thm)],[f1265,f936])).
% 38.94/5.49 fof(f1291,plain,(
% 38.94/5.49 ![X0]: (complement(complement(X0))=join(zero,X0))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f1265,f1247])).
% 38.94/5.49 fof(f1307,plain,(
% 38.94/5.49 ![X0]: (X0=join(zero,X0))),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f1265,f1291])).
% 38.94/5.49 fof(f1333,plain,(
% 38.94/5.49 ![X0]: (X0=join(X0,complement(join(complement(X0),X0))))),
% 38.94/5.49 inference(paramodulation,[status(thm)],[f1286,f95])).
% 38.94/5.49 fof(f1366,plain,(
% 38.94/5.49 ![X0]: (X0=join(X0,complement(join(X0,complement(X0)))))),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f19,f1333])).
% 38.94/5.49 fof(f1367,plain,(
% 38.94/5.49 ![X0]: (X0=join(X0,complement(top)))),
% 38.94/5.49 inference(forward_demodulation,[status(thm)],[f30,f1366])).
% 38.94/5.49 fof(f1368,plain,(
% 38.94/5.49 ![X0]: (X0=join(X0,zero))),
% 39.72/5.57 inference(forward_demodulation,[status(thm)],[f64,f1367])).
% 39.72/5.57 fof(f1424,plain,(
% 39.72/5.57 ![X0]: (meet(zero,X0)=complement(join(complement(X0),top)))),
% 39.72/5.57 inference(paramodulation,[status(thm)],[f1269,f58])).
% 39.72/5.57 fof(f1438,plain,(
% 39.72/5.57 ![X0]: (meet(zero,X0)=complement(top))),
% 39.72/5.57 inference(forward_demodulation,[status(thm)],[f1023,f1424])).
% 39.72/5.57 fof(f1439,plain,(
% 39.72/5.57 ![X0]: (meet(zero,X0)=zero)),
% 39.72/5.57 inference(forward_demodulation,[status(thm)],[f64,f1438])).
% 39.72/5.57 fof(f1981,plain,(
% 39.72/5.57 converse(top)=top),
% 39.72/5.57 inference(paramodulation,[status(thm)],[f1036,f1038])).
% 39.72/5.57 fof(f5980,plain,(
% 39.72/5.57 ![X0,X1]: (join(zero,composition(converse(X0),complement(composition(X0,join(complement(zero),complement(X1))))))=meet(zero,X1))),
% 39.72/5.57 inference(paramodulation,[status(thm)],[f1439,f382])).
% 39.72/5.57 fof(f6041,plain,(
% 39.72/5.57 ![X0,X1]: (composition(converse(X0),complement(composition(X0,join(complement(zero),complement(X1)))))=meet(zero,X1))),
% 39.72/5.57 inference(forward_demodulation,[status(thm)],[f1307,f5980])).
% 39.72/5.57 fof(f6042,plain,(
% 39.72/5.57 ![X0,X1]: (composition(converse(X0),complement(composition(X0,join(top,complement(X1)))))=meet(zero,X1))),
% 39.72/5.57 inference(forward_demodulation,[status(thm)],[f1269,f6041])).
% 39.72/5.57 fof(f6043,plain,(
% 39.72/5.57 ![X0,X1]: (composition(converse(X0),complement(composition(X0,top)))=meet(zero,X1))),
% 39.72/5.57 inference(forward_demodulation,[status(thm)],[f1036,f6042])).
% 39.72/5.57 fof(f6044,plain,(
% 39.72/5.57 ![X0]: (composition(converse(X0),complement(composition(X0,top)))=zero)),
% 39.72/5.57 inference(forward_demodulation,[status(thm)],[f1439,f6043])).
% 39.72/5.57 fof(f13214,plain,(
% 39.72/5.57 composition(top,complement(composition(top,top)))=zero),
% 39.72/5.57 inference(paramodulation,[status(thm)],[f1981,f6044])).
% 39.72/5.57 fof(f20070,plain,(
% 39.72/5.57 ![X0]: (composition(join(top,X0),complement(composition(top,top)))=join(composition(X0,complement(composition(top,top))),zero))),
% 39.72/5.57 inference(paramodulation,[status(thm)],[f13214,f239])).
% 39.72/5.57 fof(f20244,plain,(
% 39.72/5.57 ![X0]: (composition(top,complement(composition(top,top)))=join(composition(X0,complement(composition(top,top))),zero))),
% 39.72/5.57 inference(forward_demodulation,[status(thm)],[f1036,f20070])).
% 39.72/5.57 fof(f20245,plain,(
% 39.72/5.57 ![X0]: (zero=join(composition(X0,complement(composition(top,top))),zero))),
% 39.72/5.57 inference(forward_demodulation,[status(thm)],[f13214,f20244])).
% 39.72/5.57 fof(f20246,plain,(
% 39.72/5.57 ![X0]: (zero=composition(X0,complement(composition(top,top))))),
% 39.72/5.57 inference(forward_demodulation,[status(thm)],[f1368,f20245])).
% 39.72/5.57 fof(f20271,plain,(
% 39.72/5.57 ![X0,X1]: (zero=composition(X0,composition(X1,complement(composition(top,top)))))),
% 39.72/5.57 inference(paramodulation,[status(thm)],[f23,f20246])).
% 39.72/5.57 fof(f20359,plain,(
% 39.72/5.57 ![X0]: (zero=composition(X0,zero))),
% 39.72/5.57 inference(forward_demodulation,[status(thm)],[f20246,f20271])).
% 39.72/5.57 fof(f20558,plain,(
% 39.72/5.57 join(meet(sk3,composition(sk2,sk1)),composition(meet(sk2,composition(sk3,converse(sk1))),zero))=zero),
% 39.72/5.57 inference(backward_demodulation,[status(thm)],[f20359,f1016])).
% 39.72/5.57 fof(f20648,plain,(
% 39.72/5.57 join(meet(sk3,composition(sk2,sk1)),zero)=zero),
% 39.72/5.57 inference(forward_demodulation,[status(thm)],[f20359,f20558])).
% 39.72/5.57 fof(f20649,plain,(
% 39.72/5.57 meet(sk3,composition(sk2,sk1))=zero),
% 39.72/5.57 inference(forward_demodulation,[status(thm)],[f1368,f20648])).
% 39.72/5.57 fof(f20650,plain,(
% 39.72/5.57 $false),
% 39.72/5.57 inference(forward_subsumption_resolution,[status(thm)],[f20649,f423])).
% 39.72/5.57 % SZS output end CNFRefutation for theBenchmark.p
% 39.72/5.68 % Elapsed time: 5.204074 seconds
% 39.72/5.68 % CPU time: 40.512222 seconds
% 39.72/5.68 % Total memory used: 393.938 MB
% 39.72/5.68 % Net memory used: 387.556 MB
%------------------------------------------------------------------------------