%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL012-2 : 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 : n002.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 18.98s 2.91s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL012-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n002.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:16 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 18.98/2.91 % Refutation found
% 18.98/2.91 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 18.98/2.91 % SZS output start CNFRefutation for theBenchmark
% 18.98/2.91 fof(f1,axiom,(
% 18.98/2.91 (![A,B]: (join(A,B) = join(B,A) ))),
% 18.98/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.98/2.91 fof(f2,axiom,(
% 18.98/2.91 (![A,B,C]: (join(A,join(B,C)) = join(join(A,B),C) ))),
% 18.98/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.98/2.91 fof(f3,axiom,(
% 18.98/2.91 (![A,B]: (A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))) ))),
% 18.98/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.98/2.91 fof(f4,axiom,(
% 18.98/2.91 (![A,B]: (meet(A,B) = complement(join(complement(A),complement(B))) ))),
% 18.98/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.98/2.91 fof(f6,axiom,(
% 18.98/2.91 (![A]: (composition(A,one) = A ))),
% 18.98/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.98/2.91 fof(f8,axiom,(
% 18.98/2.91 (![A]: (converse(converse(A)) = A ))),
% 18.98/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.98/2.91 fof(f9,axiom,(
% 18.98/2.91 (![A,B]: (converse(join(A,B)) = join(converse(A),converse(B)) ))),
% 18.98/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.98/2.91 fof(f10,axiom,(
% 18.98/2.91 (![A,B]: (converse(composition(A,B)) = composition(converse(B),converse(A)) ))),
% 18.98/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.98/2.91 fof(f11,axiom,(
% 18.98/2.91 (![A,B]: (join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B) ))),
% 18.98/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.98/2.91 fof(f12,axiom,(
% 18.98/2.91 (![A]: (top = join(A,complement(A)) ))),
% 18.98/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.98/2.91 fof(f13,axiom,(
% 18.98/2.91 (![A]: (zero = meet(A,complement(A)) ))),
% 18.98/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.98/2.91 fof(f17,negated_conjecture,(
% 18.98/2.91 join(composition(complement(composition(sk1,sk2)),converse(sk2)),complement(sk1)) != complement(sk1) ),
% 18.98/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.98/2.91 fof(f18,plain,(
% 18.98/2.91 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 18.98/2.91 inference(cnf_transformation,[status(thm)],[f1])).
% 18.98/2.91 fof(f19,plain,(
% 18.98/2.91 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 18.98/2.91 inference(cnf_transformation,[status(thm)],[f2])).
% 18.98/2.91 fof(f20,plain,(
% 18.98/2.91 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 18.98/2.91 inference(cnf_transformation,[status(thm)],[f3])).
% 18.98/2.91 fof(f21,plain,(
% 18.98/2.91 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 18.98/2.91 inference(cnf_transformation,[status(thm)],[f4])).
% 18.98/2.91 fof(f23,plain,(
% 18.98/2.91 ![X0]: (composition(X0,one)=X0)),
% 18.98/2.91 inference(cnf_transformation,[status(thm)],[f6])).
% 18.98/2.91 fof(f25,plain,(
% 18.98/2.91 ![X0]: (converse(converse(X0))=X0)),
% 18.98/2.91 inference(cnf_transformation,[status(thm)],[f8])).
% 18.98/2.91 fof(f26,plain,(
% 18.98/2.91 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 18.98/2.91 inference(cnf_transformation,[status(thm)],[f9])).
% 18.98/2.91 fof(f27,plain,(
% 18.98/2.91 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 18.98/2.91 inference(cnf_transformation,[status(thm)],[f10])).
% 18.98/2.91 fof(f28,plain,(
% 18.98/2.91 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 18.98/2.91 inference(cnf_transformation,[status(thm)],[f11])).
% 18.98/2.91 fof(f29,plain,(
% 18.98/2.91 ![X0]: (top=join(X0,complement(X0)))),
% 18.98/2.91 inference(cnf_transformation,[status(thm)],[f12])).
% 18.98/2.91 fof(f30,plain,(
% 18.98/2.91 ![X0]: (zero=meet(X0,complement(X0)))),
% 18.98/2.91 inference(cnf_transformation,[status(thm)],[f13])).
% 18.98/2.91 fof(f34,plain,(
% 18.98/2.91 ~join(composition(complement(composition(sk1,sk2)),converse(sk2)),complement(sk1))=complement(sk1)),
% 18.98/2.91 inference(cnf_transformation,[status(thm)],[f17])).
% 18.98/2.91 fof(f42,plain,(
% 18.98/2.91 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f18,f20])).
% 18.98/2.91 fof(f43,plain,(
% 18.98/2.91 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 18.98/2.91 inference(backward_demodulation,[status(thm)],[f21,f42])).
% 18.98/2.91 fof(f44,plain,(
% 18.98/2.91 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f18,f28])).
% 18.98/2.91 fof(f45,plain,(
% 18.98/2.91 ~join(complement(sk1),composition(complement(composition(sk1,sk2)),converse(sk2)))=complement(sk1)),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f18,f34])).
% 18.98/2.91 fof(f46,plain,(
% 18.98/2.91 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f18,f43])).
% 18.98/2.91 fof(f55,plain,(
% 18.98/2.91 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f18,f21])).
% 18.98/2.91 fof(f59,plain,(
% 18.98/2.91 ![X0,X1]: (converse(composition(X0,converse(X1)))=composition(X1,converse(X0)))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f25,f27])).
% 18.98/2.91 fof(f60,plain,(
% 18.98/2.91 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f25,f27])).
% 18.98/2.91 fof(f65,plain,(
% 18.98/2.91 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X0),X2))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f18,f19])).
% 18.98/2.91 fof(f83,plain,(
% 18.98/2.91 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f21,f55])).
% 18.98/2.91 fof(f101,plain,(
% 18.98/2.91 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f18,f26])).
% 18.98/2.91 fof(f183,plain,(
% 18.98/2.91 ![X0,X1]: (converse(join(converse(X0),X1))=join(converse(X1),X0))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f25,f101])).
% 18.98/2.91 fof(f291,plain,(
% 18.98/2.91 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f55,f46])).
% 18.98/2.91 fof(f299,plain,(
% 18.98/2.91 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f18,f291])).
% 18.98/2.91 fof(f306,plain,(
% 18.98/2.91 ![X0,X1]: (X0=join(meet(X1,X0),meet(complement(X1),X0)))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f83,f299])).
% 18.98/2.91 fof(f348,plain,(
% 18.98/2.91 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f23,f60])).
% 18.98/2.91 fof(f354,plain,(
% 18.98/2.91 ![X0]: (X0=composition(converse(one),X0))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f25,f348])).
% 18.98/2.91 fof(f359,plain,(
% 18.98/2.91 ![X0]: (X0=join(meet(X0,X0),zero))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f30,f299])).
% 18.98/2.91 fof(f364,plain,(
% 18.98/2.91 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f18,f359])).
% 18.98/2.91 fof(f367,plain,(
% 18.98/2.91 one=converse(one)),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f23,f354])).
% 18.98/2.91 fof(f368,plain,(
% 18.98/2.91 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f354,f44])).
% 18.98/2.91 fof(f377,plain,(
% 18.98/2.91 ![X0]: (X0=composition(one,X0))),
% 18.98/2.91 inference(backward_demodulation,[status(thm)],[f367,f354])).
% 18.98/2.91 fof(f385,plain,(
% 18.98/2.91 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 18.98/2.91 inference(backward_demodulation,[status(thm)],[f377,f368])).
% 18.98/2.91 fof(f429,plain,(
% 18.98/2.91 ![X0]: (converse(top)=join(converse(complement(converse(X0))),X0))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f29,f183])).
% 18.98/2.91 fof(f433,plain,(
% 18.98/2.91 ![X0]: (meet(complement(X0),X0)=complement(top))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f29,f55])).
% 18.98/2.91 fof(f435,plain,(
% 18.98/2.91 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f29,f46])).
% 18.98/2.91 fof(f440,plain,(
% 18.98/2.91 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f18,f429])).
% 18.98/2.91 fof(f441,plain,(
% 18.98/2.91 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f83,f433])).
% 18.98/2.91 fof(f442,plain,(
% 18.98/2.91 zero=complement(top)),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f30,f441])).
% 18.98/2.91 fof(f444,plain,(
% 18.98/2.91 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(X0)))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f18,f435])).
% 18.98/2.91 fof(f445,plain,(
% 18.98/2.91 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f442,f444])).
% 18.98/2.91 fof(f453,plain,(
% 18.98/2.91 ![X0]: (meet(X0,top)=complement(join(zero,complement(X0))))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f442,f55])).
% 18.98/2.91 fof(f468,plain,(
% 18.98/2.91 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f385,f55])).
% 18.98/2.91 fof(f470,plain,(
% 18.98/2.91 ![X0]: (X0=join(meet(X0,complement(X0)),complement(complement(X0))))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f385,f46])).
% 18.98/2.91 fof(f488,plain,(
% 18.98/2.91 ![X0]: (X0=join(complement(complement(X0)),meet(X0,complement(X0))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f18,f470])).
% 18.98/2.91 fof(f489,plain,(
% 18.98/2.91 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f30,f488])).
% 18.98/2.91 fof(f490,plain,(
% 18.98/2.91 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f18,f489])).
% 18.98/2.91 fof(f495,plain,(
% 18.98/2.91 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(meet(X0,X1))))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f21,f490])).
% 18.98/2.91 fof(f509,plain,(
% 18.98/2.91 ![X0]: (join(meet(X0,X0),complement(complement(X0)))=complement(complement(X0)))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f468,f385])).
% 18.98/2.91 fof(f511,plain,(
% 18.98/2.91 ![X0]: (zero=meet(complement(X0),meet(X0,X0)))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f468,f30])).
% 18.98/2.91 fof(f512,plain,(
% 18.98/2.91 ![X0,X1]: (join(meet(X0,X0),composition(converse(X1),complement(composition(X1,complement(X0)))))=complement(complement(X0)))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f468,f44])).
% 18.98/2.91 fof(f548,plain,(
% 18.98/2.91 ![X0]: (X0=join(zero,meet(X0,meet(X0,X0))))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f468,f445])).
% 18.98/2.91 fof(f589,plain,(
% 18.98/2.91 ![X0]: (meet(X0,X0)=join(meet(X0,meet(X0,X0)),zero))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f511,f306])).
% 18.98/2.91 fof(f590,plain,(
% 18.98/2.91 ![X0]: (complement(complement(X0))=join(meet(X0,complement(complement(X0))),zero))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f30,f306])).
% 18.98/2.91 fof(f604,plain,(
% 18.98/2.91 ![X0]: (meet(X0,X0)=join(zero,meet(X0,meet(X0,X0))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f18,f589])).
% 18.98/2.91 fof(f607,plain,(
% 18.98/2.91 ![X0]: (X0=join(zero,X0))),
% 18.98/2.91 inference(backward_demodulation,[status(thm)],[f622,f364])).
% 18.98/2.91 fof(f617,plain,(
% 18.98/2.91 ![X0,X1]: (join(X0,composition(converse(X1),complement(composition(X1,complement(X0)))))=complement(complement(X0)))),
% 18.98/2.91 inference(backward_demodulation,[status(thm)],[f622,f512])).
% 18.98/2.91 fof(f619,plain,(
% 18.98/2.91 ![X0]: (join(X0,complement(complement(X0)))=complement(complement(X0)))),
% 18.98/2.91 inference(backward_demodulation,[status(thm)],[f622,f509])).
% 18.98/2.91 fof(f622,plain,(
% 18.98/2.91 ![X0]: (meet(X0,X0)=X0)),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f548,f604])).
% 18.98/2.91 fof(f623,plain,(
% 18.98/2.91 ![X0]: (complement(complement(X0))=join(zero,meet(X0,complement(complement(X0)))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f18,f590])).
% 18.98/2.91 fof(f629,plain,(
% 18.98/2.91 ![X0]: (complement(complement(X0))=X0)),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f445,f623])).
% 18.98/2.91 fof(f638,plain,(
% 18.98/2.91 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 18.98/2.91 inference(backward_demodulation,[status(thm)],[f607,f495])).
% 18.98/2.91 fof(f640,plain,(
% 18.98/2.91 ![X0]: (meet(X0,top)=complement(complement(X0)))),
% 18.98/2.91 inference(backward_demodulation,[status(thm)],[f607,f453])).
% 18.98/2.91 fof(f660,plain,(
% 18.98/2.91 ![X0,X1]: (join(X0,composition(converse(X1),complement(composition(X1,complement(X0)))))=X0)),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f629,f617])).
% 18.98/2.91 fof(f662,plain,(
% 18.98/2.91 ![X0]: (join(X0,X0)=complement(complement(X0)))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f629,f619])).
% 18.98/2.91 fof(f666,plain,(
% 18.98/2.91 ![X0]: (join(X0,X0)=X0)),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f629,f662])).
% 18.98/2.91 fof(f695,plain,(
% 18.98/2.91 ![X0]: (meet(X0,top)=X0)),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f629,f640])).
% 18.98/2.91 fof(f1087,plain,(
% 18.98/2.91 ![X0,X1]: (join(X0,join(X0,X1))=join(X0,X1))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f666,f65])).
% 18.98/2.91 fof(f1333,plain,(
% 18.98/2.91 ![X0,X1]: (join(meet(X0,X1),X1)=join(meet(X0,X1),meet(complement(X0),X1)))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f306,f1087])).
% 18.98/2.91 fof(f1365,plain,(
% 18.98/2.91 ![X0,X1]: (join(X0,meet(X1,X0))=join(meet(X1,X0),meet(complement(X1),X0)))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f18,f1333])).
% 18.98/2.91 fof(f1368,plain,(
% 18.98/2.91 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f306,f1365])).
% 18.98/2.91 fof(f1418,plain,(
% 18.98/2.91 ![X0]: (join(top,X0)=top)),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f695,f1368])).
% 18.98/2.91 fof(f1424,plain,(
% 18.98/2.91 ![X0,X1]: (converse(converse(X0))=join(converse(meet(X1,converse(X0))),X0))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f1368,f183])).
% 18.98/2.91 fof(f1441,plain,(
% 18.98/2.91 ![X0,X1]: (X0=join(converse(meet(X1,converse(X0))),X0))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f25,f1424])).
% 18.98/2.91 fof(f1442,plain,(
% 18.98/2.91 ![X0,X1]: (X0=join(X0,converse(meet(X1,converse(X0)))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f18,f1441])).
% 18.98/2.91 fof(f2586,plain,(
% 18.98/2.91 converse(top)=top),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f1418,f440])).
% 18.98/2.91 fof(f2610,plain,(
% 18.98/2.91 ![X0]: (X0=join(meet(X0,converse(complement(converse(complement(X0))))),complement(converse(top))))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f440,f46])).
% 18.98/2.91 fof(f2679,plain,(
% 18.98/2.91 ![X0]: (X0=join(complement(converse(top)),meet(X0,converse(complement(converse(complement(X0)))))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f18,f2610])).
% 18.98/2.91 fof(f2680,plain,(
% 18.98/2.91 ![X0]: (X0=join(complement(top),meet(X0,converse(complement(converse(complement(X0)))))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f2586,f2679])).
% 18.98/2.91 fof(f2681,plain,(
% 18.98/2.91 ![X0]: (X0=join(zero,meet(X0,converse(complement(converse(complement(X0)))))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f442,f2680])).
% 18.98/2.91 fof(f2682,plain,(
% 18.98/2.91 ![X0]: (X0=meet(X0,converse(complement(converse(complement(X0))))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f607,f2681])).
% 18.98/2.91 fof(f2779,plain,(
% 18.98/2.91 ![X0]: (complement(converse(complement(X0)))=join(complement(converse(complement(X0))),converse(X0)))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f2682,f1442])).
% 18.98/2.91 fof(f2814,plain,(
% 18.98/2.91 ![X0]: (complement(converse(complement(X0)))=join(converse(X0),complement(converse(complement(X0)))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f18,f2779])).
% 18.98/2.91 fof(f2988,plain,(
% 18.98/2.91 ![X0,X1]: (join(X0,complement(X1))=complement(meet(complement(X0),X1)))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f629,f638])).
% 18.98/2.91 fof(f3851,plain,(
% 18.98/2.91 ![X0]: (join(X0,complement(converse(complement(converse(complement(complement(X0)))))))=complement(complement(X0)))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f2682,f2988])).
% 18.98/2.91 fof(f3881,plain,(
% 18.98/2.91 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=complement(complement(X0)))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f629,f3851])).
% 18.98/2.91 fof(f3882,plain,(
% 18.98/2.91 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=X0)),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f629,f3881])).
% 18.98/2.91 fof(f3947,plain,(
% 18.98/2.91 ![X0]: (join(converse(X0),complement(converse(complement(X0))))=converse(X0))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f25,f3882])).
% 18.98/2.91 fof(f3978,plain,(
% 18.98/2.91 ![X0]: (complement(converse(complement(X0)))=converse(X0))),
% 18.98/2.91 inference(backward_demodulation,[status(thm)],[f3947,f2814])).
% 18.98/2.91 fof(f4088,plain,(
% 18.98/2.91 ![X0]: (complement(converse(X0))=converse(complement(X0)))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f629,f3978])).
% 18.98/2.91 fof(f4190,plain,(
% 18.98/2.91 ![X0,X1]: (converse(composition(X0,complement(converse(X1))))=composition(complement(X1),converse(X0)))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f4088,f59])).
% 18.98/2.91 fof(f4195,plain,(
% 18.98/2.91 ![X0,X1]: (converse(composition(complement(X0),X1))=composition(converse(X1),complement(converse(X0))))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f4088,f27])).
% 18.98/2.91 fof(f9023,plain,(
% 18.98/2.91 ![X0,X1]: (join(X0,composition(X1,complement(composition(converse(X1),complement(X0)))))=X0)),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f25,f660])).
% 18.98/2.91 fof(f12687,plain,(
% 18.98/2.91 ![X0,X1]: (converse(converse(X0))=join(converse(composition(X1,complement(composition(converse(X1),complement(converse(X0)))))),X0))),
% 18.98/2.91 inference(paramodulation,[status(thm)],[f9023,f183])).
% 18.98/2.91 fof(f12752,plain,(
% 18.98/2.91 ![X0,X1]: (X0=join(converse(composition(X1,complement(composition(converse(X1),complement(converse(X0)))))),X0))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f25,f12687])).
% 18.98/2.91 fof(f12753,plain,(
% 18.98/2.91 ![X0,X1]: (X0=join(X0,converse(composition(X1,complement(composition(converse(X1),complement(converse(X0))))))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f18,f12752])).
% 18.98/2.91 fof(f12754,plain,(
% 18.98/2.91 ![X0,X1]: (X0=join(X0,converse(composition(X1,complement(converse(composition(complement(X0),X1)))))))),
% 18.98/2.91 inference(forward_demodulation,[status(thm)],[f4195,f12753])).
% 18.98/2.97 fof(f12755,plain,(
% 18.98/2.97 ![X0,X1]: (X0=join(X0,composition(complement(composition(complement(X0),X1)),converse(X1))))),
% 18.98/2.97 inference(forward_demodulation,[status(thm)],[f4190,f12754])).
% 18.98/2.97 fof(f15743,plain,(
% 18.98/2.97 ![X0,X1]: (complement(X0)=join(complement(X0),composition(complement(composition(X0,X1)),converse(X1))))),
% 18.98/2.97 inference(paramodulation,[status(thm)],[f629,f12755])).
% 18.98/2.97 fof(f15831,plain,(
% 18.98/2.97 ~complement(sk1)=complement(sk1)),
% 18.98/2.97 inference(backward_demodulation,[status(thm)],[f15743,f45])).
% 18.98/2.97 fof(f15917,plain,(
% 18.98/2.97 $false),
% 18.98/2.97 inference(trivial_equality_resolution,[status(thm)],[f15831])).
% 18.98/2.97 % SZS output end CNFRefutation for theBenchmark.p
% 2.90/3.00 % Elapsed time: 2.613323 seconds
% 2.90/3.00 % CPU time: 20.418246 seconds
% 2.90/3.00 % Total memory used: 270.652 MB
% 2.90/3.00 % Net memory used: 266.094 MB
%------------------------------------------------------------------------------