%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL045-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 : n008.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:45 PM UTC 2026
% Result : Unsatisfiable 136.84s 33.73s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL045-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/16.21 % Computer : n008.cluster.edu
% 0.10/16.21 % Model : x86_64 x86_64
% 0.10/16.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/16.21 % Memory : 8046.5625MB
% 0.10/16.21 % OS : Linux 6.8.0-71-generic
% 0.10/16.21 % CPULimit : 300
% 0.10/16.21 % WCLimit : 300
% 0.10/16.21 % DateTime : Mon Sep 21 04:09:29 UTC 2026
% 0.10/16.21 % CPUTime :
% 0.10/16.22 % Drodi V4.1.1
% 136.84/33.73 % Refutation found
% 136.84/33.73 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 136.84/33.73 % SZS output start CNFRefutation for theBenchmark
% 136.84/33.73 fof(f1,axiom,(
% 136.84/33.73 (![A,B]: (join(A,B) = join(B,A) ))),
% 136.84/33.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 136.84/33.73 fof(f2,axiom,(
% 136.84/33.73 (![A,B,C]: (join(A,join(B,C)) = join(join(A,B),C) ))),
% 136.84/33.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 136.84/33.73 fof(f3,axiom,(
% 136.84/33.73 (![A,B]: (A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))) ))),
% 136.84/33.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 136.84/33.73 fof(f4,axiom,(
% 136.84/33.73 (![A,B]: (meet(A,B) = complement(join(complement(A),complement(B))) ))),
% 136.84/33.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 136.84/33.73 fof(f5,axiom,(
% 136.84/33.73 (![A,B,C]: (composition(A,composition(B,C)) = composition(composition(A,B),C) ))),
% 136.84/33.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 136.84/33.73 fof(f6,axiom,(
% 136.84/33.73 (![A]: (composition(A,one) = A ))),
% 136.84/33.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 136.84/33.73 fof(f7,axiom,(
% 136.84/33.73 (![A,B,C]: (composition(join(A,B),C) = join(composition(A,C),composition(B,C)) ))),
% 136.84/33.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 136.84/33.73 fof(f8,axiom,(
% 136.84/33.73 (![A]: (converse(converse(A)) = A ))),
% 136.84/33.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 136.84/33.73 fof(f9,axiom,(
% 136.84/33.73 (![A,B]: (converse(join(A,B)) = join(converse(A),converse(B)) ))),
% 136.84/33.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 136.84/33.73 fof(f10,axiom,(
% 136.84/33.73 (![A,B]: (converse(composition(A,B)) = composition(converse(B),converse(A)) ))),
% 136.84/33.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 136.84/33.73 fof(f11,axiom,(
% 136.84/33.73 (![A,B]: (join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B) ))),
% 136.84/33.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 136.84/33.73 fof(f12,axiom,(
% 136.84/33.73 (![A]: (top = join(A,complement(A)) ))),
% 136.84/33.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 136.84/33.73 fof(f13,axiom,(
% 136.84/33.73 (![A]: (zero = meet(A,complement(A)) ))),
% 136.84/33.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 136.84/33.73 fof(f14,axiom,(
% 136.84/33.73 (![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))) ))),
% 136.84/33.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 136.84/33.73 fof(f17,negated_conjecture,(
% 136.84/33.73 join(sk1,composition(composition(sk1,converse(sk1)),sk1)) != composition(composition(sk1,converse(sk1)),sk1) ),
% 136.84/33.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 136.84/33.73 fof(f18,plain,(
% 136.84/33.73 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 136.84/33.73 inference(cnf_transformation,[status(thm)],[f1])).
% 136.84/33.73 fof(f19,plain,(
% 136.84/33.73 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 136.84/33.73 inference(cnf_transformation,[status(thm)],[f2])).
% 136.84/33.73 fof(f20,plain,(
% 136.84/33.73 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 136.84/33.73 inference(cnf_transformation,[status(thm)],[f3])).
% 136.84/33.73 fof(f21,plain,(
% 136.84/33.73 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 136.84/33.73 inference(cnf_transformation,[status(thm)],[f4])).
% 136.84/33.73 fof(f22,plain,(
% 136.84/33.73 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 136.84/33.73 inference(cnf_transformation,[status(thm)],[f5])).
% 136.84/33.73 fof(f23,plain,(
% 136.84/33.73 ![X0]: (composition(X0,one)=X0)),
% 136.84/33.73 inference(cnf_transformation,[status(thm)],[f6])).
% 136.84/33.73 fof(f24,plain,(
% 136.84/33.73 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 136.84/33.73 inference(cnf_transformation,[status(thm)],[f7])).
% 136.84/33.73 fof(f25,plain,(
% 136.84/33.73 ![X0]: (converse(converse(X0))=X0)),
% 136.84/33.73 inference(cnf_transformation,[status(thm)],[f8])).
% 136.84/33.73 fof(f26,plain,(
% 136.84/33.73 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 136.84/33.73 inference(cnf_transformation,[status(thm)],[f9])).
% 136.84/33.73 fof(f27,plain,(
% 136.84/33.73 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 136.84/33.73 inference(cnf_transformation,[status(thm)],[f10])).
% 136.84/33.73 fof(f28,plain,(
% 136.84/33.73 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 136.84/33.73 inference(cnf_transformation,[status(thm)],[f11])).
% 136.84/33.73 fof(f29,plain,(
% 136.84/33.73 ![X0]: (top=join(X0,complement(X0)))),
% 136.84/33.73 inference(cnf_transformation,[status(thm)],[f12])).
% 136.84/33.73 fof(f30,plain,(
% 136.84/33.73 ![X0]: (zero=meet(X0,complement(X0)))),
% 136.84/33.73 inference(cnf_transformation,[status(thm)],[f13])).
% 136.84/33.73 fof(f31,plain,(
% 136.84/33.73 ![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))))),
% 136.84/33.73 inference(cnf_transformation,[status(thm)],[f14])).
% 136.84/33.73 fof(f34,plain,(
% 136.84/33.73 ~join(sk1,composition(composition(sk1,converse(sk1)),sk1))=composition(composition(sk1,converse(sk1)),sk1)),
% 136.84/33.73 inference(cnf_transformation,[status(thm)],[f17])).
% 136.84/33.73 fof(f42,plain,(
% 136.84/33.73 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 136.84/33.73 inference(backward_demodulation,[status(thm)],[f21,f20])).
% 136.84/33.73 fof(f43,plain,(
% 136.84/33.73 ~join(sk1,composition(sk1,composition(converse(sk1),sk1)))=composition(composition(sk1,converse(sk1)),sk1)),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f22,f34])).
% 136.84/33.73 fof(f44,plain,(
% 136.84/33.73 ~join(sk1,composition(sk1,composition(converse(sk1),sk1)))=composition(sk1,composition(converse(sk1),sk1))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f22,f43])).
% 136.84/33.73 fof(f50,plain,(
% 136.84/33.73 ![X0,X1]: (join(X0,join(X1,complement(join(X0,X1))))=top)),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f29,f19])).
% 136.84/33.73 fof(f51,plain,(
% 136.84/33.73 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f18,f19])).
% 136.84/33.73 fof(f54,plain,(
% 136.84/33.73 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f29,f19])).
% 136.84/33.73 fof(f55,plain,(
% 136.84/33.73 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X0),X2))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f18,f19])).
% 136.84/33.73 fof(f62,plain,(
% 136.84/33.73 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f29,f21])).
% 136.84/33.73 fof(f63,plain,(
% 136.84/33.73 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f18,f21])).
% 136.84/33.73 fof(f69,plain,(
% 136.84/33.73 zero=complement(top)),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f30,f62])).
% 136.84/33.73 fof(f72,plain,(
% 136.84/33.73 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f69,f21])).
% 136.84/33.73 fof(f74,plain,(
% 136.84/33.73 top=join(top,zero)),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f69,f29])).
% 136.84/33.73 fof(f75,plain,(
% 136.84/33.73 ![X0]: (join(top,join(zero,X0))=join(top,X0))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f74,f19])).
% 136.84/33.73 fof(f78,plain,(
% 136.84/33.73 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f23,f22])).
% 136.84/33.73 fof(f93,plain,(
% 136.84/33.73 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f25,f26])).
% 136.84/33.73 fof(f98,plain,(
% 136.84/33.73 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X1,X2),composition(X0,X2)))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f18,f24])).
% 136.84/33.73 fof(f100,plain,(
% 136.84/33.73 ![X0,X1,X2,X3]: (composition(join(composition(X0,X1),X2),X3)=join(composition(X0,composition(X1,X3)),composition(X2,X3)))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f22,f24])).
% 136.84/33.73 fof(f116,plain,(
% 136.84/33.73 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f25,f27])).
% 136.84/33.73 fof(f210,plain,(
% 136.84/33.73 ![X0]: (join(X0,top)=join(top,complement(complement(X0))))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f29,f54])).
% 136.84/33.73 fof(f244,plain,(
% 136.84/33.73 ![X0]: (join(zero,join(top,X0))=join(top,X0))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f74,f55])).
% 136.84/33.73 fof(f251,plain,(
% 136.84/33.73 ![X0,X1]: (join(complement(X0),join(X0,X1))=join(top,X1))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f29,f55])).
% 136.84/33.73 fof(f318,plain,(
% 136.84/33.73 ![X0]: (join(composition(converse(X0),complement(composition(X0,top))),zero)=complement(top))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f69,f28])).
% 136.84/33.73 fof(f322,plain,(
% 136.84/33.73 ![X0,X1,X2]: (join(composition(converse(X0),complement(composition(X0,X1))),join(complement(X1),X2))=join(X2,complement(X1)))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f28,f51])).
% 136.84/33.73 fof(f324,plain,(
% 136.84/33.73 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),join(complement(X1),complement(complement(X1))))=top)),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f28,f50])).
% 136.84/33.73 fof(f329,plain,(
% 136.84/33.73 ![X0]: (join(composition(converse(X0),complement(composition(X0,top))),zero)=zero)),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f69,f318])).
% 136.84/33.73 fof(f332,plain,(
% 136.84/33.73 ![X0]: (join(complement(complement(X0)),complement(X0))=top)),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f322,f324])).
% 136.84/33.73 fof(f350,plain,(
% 136.84/33.73 join(complement(zero),complement(top))=top),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f69,f332])).
% 136.84/33.73 fof(f366,plain,(
% 136.84/33.73 join(complement(zero),zero)=top),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f69,f350])).
% 136.84/33.73 fof(f379,plain,(
% 136.84/33.73 join(zero,top)=join(top,zero)),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f366,f54])).
% 136.84/33.73 fof(f387,plain,(
% 136.84/33.73 join(zero,top)=top),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f74,f379])).
% 136.84/33.73 fof(f394,plain,(
% 136.84/33.73 ![X0]: (join(zero,join(top,X0))=join(X0,top))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f387,f51])).
% 136.84/33.73 fof(f408,plain,(
% 136.84/33.73 ![X0,X1]: (join(meet(X0,X1),composition(meet(X0,composition(X1,converse(one))),meet(one,composition(converse(X0),X1))))=composition(meet(X0,composition(X1,converse(one))),meet(one,composition(converse(X0),X1))))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f23,f31])).
% 136.84/33.73 fof(f529,plain,(
% 136.84/33.73 ![X0,X1]: (join(join(zero,X0),join(top,X1))=join(join(top,X0),X1))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f75,f55])).
% 136.84/33.73 fof(f538,plain,(
% 136.84/33.73 ![X0,X1]: (join(X0,join(zero,join(top,X1)))=join(join(top,X0),X1))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f55,f529])).
% 136.84/33.73 fof(f539,plain,(
% 136.84/33.73 ![X0,X1]: (join(X0,join(X1,top))=join(join(top,X0),X1))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f394,f538])).
% 136.84/33.73 fof(f540,plain,(
% 136.84/33.73 ![X0,X1]: (join(X0,join(X1,top))=join(X0,join(top,X1)))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f55,f539])).
% 136.84/33.73 fof(f838,plain,(
% 136.84/33.73 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f23,f116])).
% 136.84/33.73 fof(f864,plain,(
% 136.84/33.73 ![X0]: (X0=composition(converse(one),X0))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f25,f838])).
% 136.84/33.73 fof(f889,plain,(
% 136.84/33.73 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f78,f864])).
% 136.84/33.73 fof(f890,plain,(
% 136.84/33.73 one=converse(one)),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f23,f864])).
% 136.84/33.73 fof(f891,plain,(
% 136.84/33.73 ![X0]: (join(complement(composition(one,X0)),complement(X0))=complement(X0))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f864,f28])).
% 136.84/33.73 fof(f915,plain,(
% 136.84/33.73 ![X0]: (composition(one,X0)=X0)),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f864,f889])).
% 136.84/33.73 fof(f917,plain,(
% 136.84/33.73 ![X0,X1]: (join(meet(X0,X1),composition(meet(X0,composition(X1,converse(one))),meet(one,composition(converse(X0),X1))))=composition(meet(X0,composition(X1,one)),meet(one,composition(converse(X0),X1))))),
% 136.84/33.73 inference(backward_demodulation,[status(thm)],[f890,f408])).
% 136.84/33.73 fof(f918,plain,(
% 136.84/33.73 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f915,f891])).
% 136.84/33.73 fof(f967,plain,(
% 136.84/33.73 ![X0,X1]: (join(meet(X0,X1),composition(meet(X0,composition(X1,one)),meet(one,composition(converse(X0),X1))))=composition(meet(X0,composition(X1,one)),meet(one,composition(converse(X0),X1))))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f890,f917])).
% 136.84/33.73 fof(f968,plain,(
% 136.84/33.73 ![X0,X1]: (join(meet(X0,X1),composition(meet(X0,X1),meet(one,composition(converse(X0),X1))))=composition(meet(X0,composition(X1,one)),meet(one,composition(converse(X0),X1))))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f23,f967])).
% 136.84/33.73 fof(f969,plain,(
% 136.84/33.73 ![X0,X1]: (join(meet(X0,X1),composition(meet(X0,X1),meet(one,composition(converse(X0),X1))))=composition(meet(X0,X1),meet(one,composition(converse(X0),X1))))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f23,f968])).
% 136.84/33.73 fof(f1111,plain,(
% 136.84/33.73 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f918,f63])).
% 136.84/33.73 fof(f1113,plain,(
% 136.84/33.73 ![X0]: (join(X0,complement(X0))=join(top,complement(X0)))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f918,f54])).
% 136.84/33.73 fof(f1143,plain,(
% 136.84/33.73 ![X0]: (join(X0,top)=top)),
% 136.84/33.73 inference(backward_demodulation,[status(thm)],[f1144,f210])).
% 136.84/33.73 fof(f1144,plain,(
% 136.84/33.73 ![X0]: (top=join(top,complement(X0)))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f29,f1113])).
% 136.84/33.73 fof(f1149,plain,(
% 136.84/33.73 ![X0,X1]: (join(X0,top)=join(X0,join(top,X1)))),
% 136.84/33.73 inference(backward_demodulation,[status(thm)],[f1143,f540])).
% 136.84/33.73 fof(f1159,plain,(
% 136.84/33.73 ![X0]: (top=join(top,X0))),
% 136.84/33.73 inference(backward_demodulation,[status(thm)],[f1165,f244])).
% 136.84/33.73 fof(f1165,plain,(
% 136.84/33.73 ![X0,X1]: (top=join(X0,join(top,X1)))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f1143,f1149])).
% 136.84/33.73 fof(f1185,plain,(
% 136.84/33.73 ![X0,X1]: (join(complement(X0),join(X0,X1))=top)),
% 136.84/33.73 inference(backward_demodulation,[status(thm)],[f1159,f251])).
% 136.84/33.73 fof(f1194,plain,(
% 136.84/33.73 ![X0]: (converse(top)=join(X0,converse(top)))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f1143,f93])).
% 136.84/33.73 fof(f1512,plain,(
% 136.84/33.73 converse(top)=top),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f1159,f1194])).
% 136.84/33.73 fof(f1631,plain,(
% 136.84/33.73 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f30,f42])).
% 136.84/33.73 fof(f1632,plain,(
% 136.84/33.73 ![X0]: (X0=join(complement(complement(X0)),complement(join(complement(X0),X0))))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f1111,f42])).
% 136.84/33.73 fof(f1636,plain,(
% 136.84/33.73 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f63,f42])).
% 136.84/33.73 fof(f1637,plain,(
% 136.84/33.73 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f21,f42])).
% 136.84/33.73 fof(f1662,plain,(
% 136.84/33.73 ![X0,X1,X2]: (join(meet(X0,X1),join(complement(join(complement(X0),X1)),X2))=join(X2,X0))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f42,f51])).
% 136.84/33.73 fof(f1664,plain,(
% 136.84/33.73 ![X0,X1]: (join(meet(X0,X1),join(complement(join(complement(X0),X1)),complement(X0)))=top)),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f42,f50])).
% 136.84/33.73 fof(f1673,plain,(
% 136.84/33.73 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f63,f1631])).
% 136.84/33.73 fof(f1692,plain,(
% 136.84/33.73 ![X0]: (X0=join(complement(complement(X0)),complement(top)))),
% 136.84/33.73 inference(backward_demodulation,[status(thm)],[f1694,f1632])).
% 136.84/33.73 fof(f1694,plain,(
% 136.84/33.73 ![X0]: (join(complement(X0),X0)=top)),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f1662,f1664])).
% 136.84/33.73 fof(f1696,plain,(
% 136.84/33.73 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f69,f1692])).
% 136.84/33.73 fof(f1745,plain,(
% 136.84/33.73 ![X0]: (join(complement(zero),X0)=top)),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f1673,f1185])).
% 136.84/33.73 fof(f1786,plain,(
% 136.84/33.73 ![X0]: (meet(X0,zero)=complement(top))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f1745,f63])).
% 136.84/33.73 fof(f1822,plain,(
% 136.84/33.73 ![X0]: (meet(X0,zero)=zero)),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f69,f1786])).
% 136.84/33.73 fof(f2103,plain,(
% 136.84/33.73 ![X0]: (complement(X0)=join(meet(complement(X0),zero),complement(X0)))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f1696,f42])).
% 136.84/33.73 fof(f2114,plain,(
% 136.84/33.73 ![X0]: (join(zero,complement(complement(X0)))=X0)),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f1696,f18])).
% 136.84/33.73 fof(f2122,plain,(
% 136.84/33.73 ![X0]: (meet(top,X0)=complement(complement(X0)))),
% 136.84/33.73 inference(backward_demodulation,[status(thm)],[f2144,f72])).
% 136.84/33.73 fof(f2144,plain,(
% 136.84/33.73 ![X0]: (complement(X0)=join(zero,complement(X0)))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f1822,f2103])).
% 136.84/33.73 fof(f2146,plain,(
% 136.84/33.73 ![X0]: (X0=join(X0,zero))),
% 136.84/33.73 inference(backward_demodulation,[status(thm)],[f2171,f1696])).
% 136.84/33.73 fof(f2171,plain,(
% 136.84/33.73 ![X0]: (complement(complement(X0))=X0)),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f2144,f2114])).
% 136.84/33.73 fof(f2201,plain,(
% 136.84/33.73 ![X0]: (meet(top,X0)=X0)),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f2171,f2122])).
% 136.84/33.73 fof(f2280,plain,(
% 136.84/33.73 ![X0]: (composition(converse(X0),complement(composition(X0,top)))=zero)),
% 136.84/33.73 inference(backward_demodulation,[status(thm)],[f2146,f329])).
% 136.84/33.73 fof(f7612,plain,(
% 136.84/33.73 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f18,f1636])).
% 136.84/33.73 fof(f7719,plain,(
% 136.84/33.73 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f18,f1637])).
% 136.84/33.73 fof(f20454,plain,(
% 136.84/33.73 composition(top,complement(composition(top,top)))=zero),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f1512,f2280])).
% 136.84/33.73 fof(f48447,plain,(
% 136.84/33.73 ![X0]: (join(meet(X0,complement(composition(X0,top))),composition(meet(X0,complement(composition(X0,top))),meet(one,zero)))=composition(meet(X0,complement(composition(X0,top))),meet(one,composition(converse(X0),complement(composition(X0,top))))))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f2280,f969])).
% 136.84/33.73 fof(f48764,plain,(
% 136.84/33.73 ![X0]: (join(meet(X0,complement(composition(X0,top))),composition(meet(X0,complement(composition(X0,top))),zero))=composition(meet(X0,complement(composition(X0,top))),meet(one,composition(converse(X0),complement(composition(X0,top))))))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f1822,f48447])).
% 136.84/33.73 fof(f48765,plain,(
% 136.84/33.73 ![X0]: (join(meet(X0,complement(composition(X0,top))),composition(meet(X0,complement(composition(X0,top))),zero))=composition(meet(X0,complement(composition(X0,top))),meet(one,zero)))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f2280,f48764])).
% 136.84/33.73 fof(f48766,plain,(
% 136.84/33.73 ![X0]: (join(meet(X0,complement(composition(X0,top))),composition(meet(X0,complement(composition(X0,top))),zero))=composition(meet(X0,complement(composition(X0,top))),zero))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f1822,f48765])).
% 136.84/33.73 fof(f59333,plain,(
% 136.84/33.73 ![X0,X1]: (composition(join(composition(X0,top),X1),complement(composition(top,top)))=join(composition(X0,zero),composition(X1,complement(composition(top,top)))))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f20454,f100])).
% 136.84/33.73 fof(f59334,plain,(
% 136.84/33.73 ![X0]: (composition(join(top,X0),complement(composition(top,top)))=join(composition(X0,complement(composition(top,top))),zero))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f20454,f98])).
% 136.84/33.73 fof(f59579,plain,(
% 136.84/33.73 ![X0]: (composition(top,complement(composition(top,top)))=join(composition(X0,complement(composition(top,top))),zero))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f1159,f59334])).
% 136.84/33.73 fof(f59580,plain,(
% 136.84/33.73 ![X0]: (zero=join(composition(X0,complement(composition(top,top))),zero))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f20454,f59579])).
% 136.84/33.73 fof(f59582,plain,(
% 136.84/33.73 ![X0,X1]: (zero=join(composition(X0,zero),composition(X1,complement(composition(top,top)))))),
% 136.84/33.73 inference(backward_demodulation,[status(thm)],[f59588,f59333])).
% 136.84/33.73 fof(f59588,plain,(
% 136.84/33.73 ![X0]: (zero=composition(X0,complement(composition(top,top))))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f2146,f59580])).
% 136.84/33.73 fof(f59608,plain,(
% 136.84/33.73 ![X0]: (zero=join(composition(X0,zero),zero))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f59588,f59582])).
% 136.84/33.73 fof(f59649,plain,(
% 136.84/33.73 ![X0]: (join(meet(X0,complement(composition(X0,top))),composition(meet(X0,complement(composition(X0,top))),zero))=zero)),
% 136.84/33.73 inference(backward_demodulation,[status(thm)],[f59806,f48766])).
% 136.84/33.73 fof(f59806,plain,(
% 136.84/33.73 ![X0]: (zero=composition(X0,zero))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f2146,f59608])).
% 136.84/33.73 fof(f59916,plain,(
% 136.84/33.73 ![X0]: (join(meet(X0,complement(composition(X0,top))),zero)=zero)),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f59806,f59649])).
% 136.84/33.73 fof(f59917,plain,(
% 136.84/33.73 ![X0]: (meet(X0,complement(composition(X0,top)))=zero)),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f2146,f59916])).
% 136.84/33.73 fof(f62002,plain,(
% 136.84/33.73 ![X0]: (X0=join(meet(X0,composition(X0,top)),zero))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f59917,f7719])).
% 136.84/33.73 fof(f62003,plain,(
% 136.84/33.73 ![X0]: (X0=join(meet(composition(X0,top),X0),zero))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f59917,f7612])).
% 136.84/33.73 fof(f62116,plain,(
% 136.84/33.73 ![X0]: (X0=meet(X0,composition(X0,top)))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f2146,f62002])).
% 136.84/33.73 fof(f62117,plain,(
% 136.84/33.73 ![X0]: (X0=meet(composition(X0,top),X0))),
% 136.84/33.73 inference(forward_demodulation,[status(thm)],[f2146,f62003])).
% 136.84/33.73 fof(f63010,plain,(
% 136.84/33.73 ![X0]: (join(X0,composition(meet(X0,composition(X0,converse(top))),meet(top,composition(converse(X0),X0))))=composition(meet(X0,composition(X0,converse(top))),meet(top,composition(converse(X0),X0))))),
% 136.84/33.73 inference(paramodulation,[status(thm)],[f62117,f31])).
% 136.84/33.73 fof(f63217,plain,(
% 136.84/33.73 ![X0]: (join(X0,composition(meet(X0,composition(X0,top)),meet(top,composition(converse(X0),X0))))=composition(meet(X0,composition(X0,converse(top))),meet(top,composition(converse(X0),X0))))),
% 62.05/34.04 inference(forward_demodulation,[status(thm)],[f1512,f63010])).
% 62.05/34.04 fof(f63218,plain,(
% 62.05/34.04 ![X0]: (join(X0,composition(X0,meet(top,composition(converse(X0),X0))))=composition(meet(X0,composition(X0,converse(top))),meet(top,composition(converse(X0),X0))))),
% 62.05/34.04 inference(forward_demodulation,[status(thm)],[f62116,f63217])).
% 62.05/34.04 fof(f63219,plain,(
% 62.05/34.04 ![X0]: (join(X0,composition(X0,composition(converse(X0),X0)))=composition(meet(X0,composition(X0,converse(top))),meet(top,composition(converse(X0),X0))))),
% 62.05/34.04 inference(forward_demodulation,[status(thm)],[f2201,f63218])).
% 62.05/34.04 fof(f63220,plain,(
% 62.05/34.04 ![X0]: (join(X0,composition(X0,composition(converse(X0),X0)))=composition(meet(X0,composition(X0,top)),meet(top,composition(converse(X0),X0))))),
% 62.05/34.04 inference(forward_demodulation,[status(thm)],[f1512,f63219])).
% 62.05/34.04 fof(f63221,plain,(
% 62.05/34.04 ![X0]: (join(X0,composition(X0,composition(converse(X0),X0)))=composition(X0,meet(top,composition(converse(X0),X0))))),
% 62.05/34.04 inference(forward_demodulation,[status(thm)],[f62116,f63220])).
% 62.05/34.04 fof(f63222,plain,(
% 62.05/34.04 ~composition(sk1,composition(converse(sk1),sk1))=composition(sk1,composition(converse(sk1),sk1))),
% 62.05/34.04 inference(backward_demodulation,[status(thm)],[f63223,f44])).
% 62.05/34.04 fof(f63223,plain,(
% 62.05/34.04 ![X0]: (join(X0,composition(X0,composition(converse(X0),X0)))=composition(X0,composition(converse(X0),X0)))),
% 62.05/34.04 inference(forward_demodulation,[status(thm)],[f2201,f63221])).
% 62.05/34.04 fof(f63412,plain,(
% 62.05/34.04 $false),
% 62.05/34.04 inference(trivial_equality_resolution,[status(thm)],[f63222])).
% 62.05/34.04 % SZS output end CNFRefutation for theBenchmark.p
% 62.05/34.06 % Elapsed time: 17.827600 seconds
% 62.05/34.06 % CPU time: 140.787187 seconds
% 62.05/34.06 % Total memory used: 869.382 MB
% 62.05/34.06 % Net memory used: 855.143 MB
%------------------------------------------------------------------------------