%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL007-1 : 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 : n003.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:32 PM UTC 2026
% Result : Unsatisfiable 22.33s 3.28s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL007-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 03:59:31 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 22.33/3.28 % Refutation found
% 22.33/3.28 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 22.33/3.28 % SZS output start CNFRefutation for theBenchmark
% 22.33/3.28 fof(f1,axiom,(
% 22.33/3.28 (![A,B]: (join(A,B) = join(B,A) ))),
% 22.33/3.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.33/3.28 fof(f2,axiom,(
% 22.33/3.28 (![A,B,C]: (join(A,join(B,C)) = join(join(A,B),C) ))),
% 22.33/3.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.33/3.28 fof(f3,axiom,(
% 22.33/3.28 (![A,B]: (A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))) ))),
% 22.33/3.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.33/3.28 fof(f4,axiom,(
% 22.33/3.28 (![A,B]: (meet(A,B) = complement(join(complement(A),complement(B))) ))),
% 22.33/3.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.33/3.28 fof(f6,axiom,(
% 22.33/3.28 (![A]: (composition(A,one) = A ))),
% 22.33/3.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.33/3.28 fof(f8,axiom,(
% 22.33/3.28 (![A]: (converse(converse(A)) = A ))),
% 22.33/3.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.33/3.28 fof(f9,axiom,(
% 22.33/3.28 (![A,B]: (converse(join(A,B)) = join(converse(A),converse(B)) ))),
% 22.33/3.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.33/3.28 fof(f10,axiom,(
% 22.33/3.28 (![A,B]: (converse(composition(A,B)) = composition(converse(B),converse(A)) ))),
% 22.33/3.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.33/3.28 fof(f11,axiom,(
% 22.33/3.28 (![A,B]: (join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B) ))),
% 22.33/3.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.33/3.28 fof(f12,axiom,(
% 22.33/3.28 (![A]: (top = join(A,complement(A)) ))),
% 22.33/3.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.33/3.28 fof(f13,axiom,(
% 22.33/3.28 (![A]: (zero = meet(A,complement(A)) ))),
% 22.33/3.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.33/3.28 fof(f14,negated_conjecture,(
% 22.33/3.28 meet(sk1,converse(sk2)) = zero ),
% 22.33/3.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.33/3.28 fof(f15,negated_conjecture,(
% 22.33/3.28 meet(converse(sk1),sk2) != zero ),
% 22.33/3.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.33/3.28 fof(f16,plain,(
% 22.33/3.28 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 22.33/3.28 inference(cnf_transformation,[status(thm)],[f1])).
% 22.33/3.28 fof(f17,plain,(
% 22.33/3.28 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 22.33/3.28 inference(cnf_transformation,[status(thm)],[f2])).
% 22.33/3.28 fof(f18,plain,(
% 22.33/3.28 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 22.33/3.28 inference(cnf_transformation,[status(thm)],[f3])).
% 22.33/3.28 fof(f19,plain,(
% 22.33/3.28 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 22.33/3.28 inference(cnf_transformation,[status(thm)],[f4])).
% 22.33/3.28 fof(f21,plain,(
% 22.33/3.28 ![X0]: (composition(X0,one)=X0)),
% 22.33/3.28 inference(cnf_transformation,[status(thm)],[f6])).
% 22.33/3.28 fof(f23,plain,(
% 22.33/3.28 ![X0]: (converse(converse(X0))=X0)),
% 22.33/3.28 inference(cnf_transformation,[status(thm)],[f8])).
% 22.33/3.28 fof(f24,plain,(
% 22.33/3.28 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 22.33/3.28 inference(cnf_transformation,[status(thm)],[f9])).
% 22.33/3.28 fof(f25,plain,(
% 22.33/3.28 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 22.33/3.28 inference(cnf_transformation,[status(thm)],[f10])).
% 22.33/3.28 fof(f26,plain,(
% 22.33/3.28 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 22.33/3.28 inference(cnf_transformation,[status(thm)],[f11])).
% 22.33/3.28 fof(f27,plain,(
% 22.33/3.28 ![X0]: (top=join(X0,complement(X0)))),
% 22.33/3.28 inference(cnf_transformation,[status(thm)],[f12])).
% 22.33/3.28 fof(f28,plain,(
% 22.33/3.28 ![X0]: (zero=meet(X0,complement(X0)))),
% 22.33/3.28 inference(cnf_transformation,[status(thm)],[f13])).
% 22.33/3.28 fof(f29,plain,(
% 22.33/3.28 meet(sk1,converse(sk2))=zero),
% 22.33/3.28 inference(cnf_transformation,[status(thm)],[f14])).
% 22.33/3.28 fof(f30,plain,(
% 22.33/3.28 ~meet(converse(sk1),sk2)=zero),
% 22.33/3.28 inference(cnf_transformation,[status(thm)],[f15])).
% 22.33/3.28 fof(f34,plain,(
% 22.33/3.28 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f16,f18])).
% 22.33/3.28 fof(f35,plain,(
% 22.33/3.28 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 22.33/3.28 inference(backward_demodulation,[status(thm)],[f19,f34])).
% 22.33/3.28 fof(f36,plain,(
% 22.33/3.28 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f16,f26])).
% 22.33/3.28 fof(f37,plain,(
% 22.33/3.28 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f16,f35])).
% 22.33/3.28 fof(f39,plain,(
% 22.33/3.28 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X0,X1),complement(X2))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f19,f19])).
% 22.33/3.28 fof(f41,plain,(
% 22.33/3.28 ![X0,X1]: (zero=meet(join(complement(X0),complement(X1)),meet(X0,X1)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f19,f28])).
% 22.33/3.28 fof(f42,plain,(
% 22.33/3.28 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f23,f24])).
% 22.33/3.28 fof(f43,plain,(
% 22.33/3.28 ![X0,X1]: (converse(join(X0,converse(X1)))=join(converse(X0),X1))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f23,f24])).
% 22.33/3.28 fof(f45,plain,(
% 22.33/3.28 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f23,f25])).
% 22.33/3.28 fof(f46,plain,(
% 22.33/3.28 sk1=join(zero,complement(join(complement(sk1),converse(sk2))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f29,f37])).
% 22.33/3.28 fof(f47,plain,(
% 22.33/3.28 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f28,f37])).
% 22.33/3.28 fof(f48,plain,(
% 22.33/3.28 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f19,f37])).
% 22.33/3.28 fof(f50,plain,(
% 22.33/3.28 sk1=join(zero,complement(join(converse(sk2),complement(sk1))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f16,f46])).
% 22.33/3.28 fof(f51,plain,(
% 22.33/3.28 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f19,f47])).
% 22.33/3.28 fof(f52,plain,(
% 22.33/3.28 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f16,f48])).
% 22.33/3.28 fof(f139,plain,(
% 22.33/3.28 ![X0,X1,X2]: (join(meet(X0,X1),composition(converse(X2),complement(composition(X2,join(complement(X0),complement(X1))))))=complement(join(complement(X0),complement(X1))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f19,f36])).
% 22.33/3.28 fof(f144,plain,(
% 22.33/3.28 ![X0,X1]: (join(complement(X0),composition(X1,complement(composition(converse(X1),X0))))=complement(X0))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f23,f36])).
% 22.33/3.28 fof(f147,plain,(
% 22.33/3.28 ![X0,X1,X2]: (join(meet(X0,X1),composition(converse(X2),complement(composition(X2,join(complement(X0),complement(X1))))))=meet(X0,X1))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f19,f139])).
% 22.33/3.28 fof(f169,plain,(
% 22.33/3.28 ![X0,X1]: (join(zero,composition(converse(X0),complement(composition(X0,join(complement(X1),complement(complement(X1)))))))=meet(X1,complement(X1)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f28,f147])).
% 22.33/3.28 fof(f178,plain,(
% 22.33/3.28 ![X0,X1]: (join(zero,composition(converse(X0),complement(composition(X0,top))))=meet(X1,complement(X1)))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f27,f169])).
% 22.33/3.28 fof(f179,plain,(
% 22.33/3.28 ![X0]: (join(zero,composition(converse(X0),complement(composition(X0,top))))=zero)),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f28,f178])).
% 22.33/3.28 fof(f240,plain,(
% 22.33/3.28 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f21,f45])).
% 22.33/3.28 fof(f242,plain,(
% 22.33/3.28 ![X0]: (X0=composition(converse(one),X0))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f23,f240])).
% 22.33/3.28 fof(f245,plain,(
% 22.33/3.28 ![X0,X1]: (top=join(join(complement(X0),complement(X1)),meet(X0,X1)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f19,f27])).
% 22.33/3.28 fof(f246,plain,(
% 22.33/3.28 ![X0,X1]: (meet(join(complement(X0),complement(X1)),meet(X0,X1))=complement(top))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f27,f39])).
% 22.33/3.28 fof(f247,plain,(
% 22.33/3.28 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f27,f42])).
% 22.33/3.28 fof(f253,plain,(
% 22.33/3.28 ![X0,X1]: (top=join(complement(X0),join(complement(X1),meet(X0,X1))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f17,f245])).
% 22.33/3.28 fof(f254,plain,(
% 22.33/3.28 zero=complement(top)),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f41,f246])).
% 22.33/3.28 fof(f281,plain,(
% 22.33/3.28 one=converse(one)),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f21,f242])).
% 22.33/3.28 fof(f286,plain,(
% 22.33/3.28 ![X0]: (join(complement(X0),composition(one,complement(X0)))=complement(X0))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f242,f144])).
% 22.33/3.28 fof(f289,plain,(
% 22.33/3.28 join(zero,composition(converse(converse(one)),complement(top)))=zero),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f242,f179])).
% 22.33/3.28 fof(f294,plain,(
% 22.33/3.28 ![X0]: (X0=composition(one,X0))),
% 22.33/3.28 inference(backward_demodulation,[status(thm)],[f281,f242])).
% 22.33/3.28 fof(f295,plain,(
% 22.33/3.28 join(zero,composition(one,complement(top)))=zero),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f23,f289])).
% 22.33/3.28 fof(f296,plain,(
% 22.33/3.28 join(zero,composition(one,zero))=zero),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f254,f295])).
% 22.33/3.28 fof(f304,plain,(
% 22.33/3.28 join(zero,zero)=zero),
% 22.33/3.28 inference(backward_demodulation,[status(thm)],[f294,f296])).
% 22.33/3.28 fof(f305,plain,(
% 22.33/3.28 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 22.33/3.28 inference(backward_demodulation,[status(thm)],[f294,f286])).
% 22.33/3.28 fof(f368,plain,(
% 22.33/3.28 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f305,f19])).
% 22.33/3.28 fof(f369,plain,(
% 22.33/3.28 ![X0]: (X0=join(meet(X0,complement(X0)),complement(complement(X0))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f305,f37])).
% 22.33/3.28 fof(f390,plain,(
% 22.33/3.28 ![X0]: (X0=join(complement(complement(X0)),meet(X0,complement(X0))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f16,f369])).
% 22.33/3.28 fof(f391,plain,(
% 22.33/3.28 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f28,f390])).
% 22.33/3.28 fof(f392,plain,(
% 22.33/3.28 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f16,f391])).
% 22.33/3.28 fof(f396,plain,(
% 22.33/3.28 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(meet(X0,X1))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f19,f392])).
% 22.33/3.28 fof(f418,plain,(
% 22.33/3.28 ![X0]: (join(zero,join(zero,X0))=join(zero,X0))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f304,f17])).
% 22.33/3.28 fof(f426,plain,(
% 22.33/3.28 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f27,f17])).
% 22.33/3.28 fof(f443,plain,(
% 22.33/3.28 ![X0]: (X0=join(meet(X0,converse(complement(converse(complement(X0))))),complement(converse(top))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f247,f37])).
% 22.33/3.28 fof(f445,plain,(
% 22.33/3.28 ![X0,X1]: (join(X0,join(converse(complement(converse(X0))),X1))=join(converse(top),X1))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f247,f17])).
% 22.33/3.28 fof(f459,plain,(
% 22.33/3.28 ![X0]: (X0=join(complement(converse(top)),meet(X0,converse(complement(converse(complement(X0)))))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f16,f443])).
% 22.33/3.28 fof(f492,plain,(
% 22.33/3.28 ![X0]: (join(meet(X0,X0),complement(complement(X0)))=complement(complement(X0)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f368,f305])).
% 22.33/3.28 fof(f493,plain,(
% 22.33/3.28 ![X0]: (top=join(complement(X0),meet(X0,X0)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f368,f27])).
% 22.33/3.28 fof(f554,plain,(
% 22.33/3.28 ![X0,X1]: (join(complement(X0),join(meet(X0,X0),X1))=join(top,X1))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f493,f17])).
% 22.33/3.28 fof(f604,plain,(
% 22.33/3.28 ![X0]: (join(zero,X0)=join(zero,complement(complement(X0))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f392,f418])).
% 22.33/3.28 fof(f608,plain,(
% 22.33/3.28 ![X0]: (join(zero,X0)=join(zero,meet(X0,X0)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f51,f418])).
% 22.33/3.28 fof(f613,plain,(
% 22.33/3.28 ![X0]: (X0=complement(complement(X0)))),
% 22.33/3.28 inference(backward_demodulation,[status(thm)],[f647,f392])).
% 22.33/3.28 fof(f640,plain,(
% 22.33/3.28 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 22.33/3.28 inference(backward_demodulation,[status(thm)],[f647,f396])).
% 22.33/3.28 fof(f641,plain,(
% 22.33/3.28 sk1=complement(join(converse(sk2),complement(sk1)))),
% 22.33/3.28 inference(backward_demodulation,[status(thm)],[f647,f50])).
% 22.33/3.28 fof(f647,plain,(
% 22.33/3.28 ![X0]: (join(zero,X0)=X0)),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f392,f604])).
% 22.33/3.28 fof(f652,plain,(
% 22.33/3.28 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f647,f608])).
% 22.33/3.28 fof(f660,plain,(
% 22.33/3.28 ![X0,X1]: (join(complement(X0),join(X0,X1))=join(top,X1))),
% 22.33/3.28 inference(backward_demodulation,[status(thm)],[f675,f554])).
% 22.33/3.28 fof(f670,plain,(
% 22.33/3.28 ![X0]: (join(X0,complement(complement(X0)))=complement(complement(X0)))),
% 22.33/3.28 inference(backward_demodulation,[status(thm)],[f675,f492])).
% 22.33/3.28 fof(f675,plain,(
% 22.33/3.28 ![X0]: (X0=meet(X0,X0))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f647,f652])).
% 22.33/3.28 fof(f758,plain,(
% 22.33/3.28 ![X0]: (join(X0,X0)=complement(complement(X0)))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f613,f670])).
% 22.33/3.28 fof(f760,plain,(
% 22.33/3.28 ![X0]: (join(X0,X0)=X0)),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f613,f758])).
% 22.33/3.28 fof(f796,plain,(
% 22.33/3.28 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f17,f16])).
% 22.33/3.28 fof(f797,plain,(
% 22.33/3.28 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f24,f16])).
% 22.33/3.28 fof(f816,plain,(
% 22.33/3.28 ![X0,X1]: (join(X0,join(X1,complement(X0)))=join(top,X1))),
% 22.33/3.28 inference(backward_demodulation,[status(thm)],[f796,f660])).
% 22.33/3.28 fof(f888,plain,(
% 22.33/3.28 top=join(join(converse(sk2),complement(sk1)),sk1)),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f641,f27])).
% 22.33/3.28 fof(f894,plain,(
% 22.33/3.28 top=join(converse(sk2),join(complement(sk1),sk1))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f17,f888])).
% 22.33/3.28 fof(f895,plain,(
% 22.33/3.28 top=join(sk1,join(converse(sk2),complement(sk1)))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f796,f894])).
% 22.33/3.28 fof(f896,plain,(
% 22.33/3.28 top=join(top,converse(sk2))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f816,f895])).
% 22.33/3.28 fof(f949,plain,(
% 22.33/3.28 converse(top)=join(converse(top),sk2)),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f896,f43])).
% 22.33/3.28 fof(f951,plain,(
% 22.33/3.28 converse(top)=join(sk2,converse(top))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f16,f949])).
% 22.33/3.28 fof(f953,plain,(
% 22.33/3.28 ![X0]: (X0=join(X0,meet(X0,complement(X0))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f675,f52])).
% 22.33/3.28 fof(f959,plain,(
% 22.33/3.28 ![X0]: (X0=join(X0,zero))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f28,f953])).
% 22.33/3.28 fof(f1022,plain,(
% 22.33/3.28 ![X0]: (converse(converse(X0))=join(converse(zero),X0))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f647,f43])).
% 22.33/3.28 fof(f1026,plain,(
% 22.33/3.28 ![X0]: (X0=join(converse(zero),X0))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f23,f1022])).
% 22.33/3.28 fof(f1072,plain,(
% 22.33/3.28 ![X0,X1]: (join(X0,join(X0,X1))=join(X0,X1))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f760,f17])).
% 22.33/3.28 fof(f1085,plain,(
% 22.33/3.28 zero=converse(zero)),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f959,f1026])).
% 22.33/3.28 fof(f1199,plain,(
% 22.33/3.28 ![X0,X1]: (X0=join(meet(X0,join(complement(X1),meet(X0,X1))),complement(top)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f253,f37])).
% 22.33/3.28 fof(f1230,plain,(
% 22.33/3.28 ![X0,X1]: (X0=join(complement(top),meet(X0,join(complement(X1),meet(X0,X1)))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f16,f1199])).
% 22.33/3.28 fof(f1231,plain,(
% 22.33/3.28 ![X0,X1]: (X0=join(zero,meet(X0,join(complement(X1),meet(X0,X1)))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f254,f1230])).
% 22.33/3.28 fof(f1232,plain,(
% 22.33/3.28 ![X0,X1]: (X0=meet(X0,join(complement(X1),meet(X0,X1))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f647,f1231])).
% 22.33/3.28 fof(f1313,plain,(
% 22.33/3.28 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X1,X0)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f16,f640])).
% 22.33/3.28 fof(f1315,plain,(
% 22.33/3.28 ![X0,X1]: (join(X0,complement(X1))=complement(meet(complement(X0),X1)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f613,f640])).
% 22.33/3.28 fof(f1318,plain,(
% 22.33/3.28 ![X0,X1]: (join(complement(X0),X1)=complement(meet(X0,complement(X1))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f613,f640])).
% 22.33/3.28 fof(f1365,plain,(
% 22.33/3.28 ![X0]: (join(X0,converse(top))=join(top,converse(complement(converse(complement(X0))))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f247,f426])).
% 22.33/3.28 fof(f1367,plain,(
% 22.33/3.28 ![X0]: (join(X0,complement(X0))=join(top,complement(X0)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f760,f426])).
% 22.33/3.28 fof(f1392,plain,(
% 22.33/3.28 ![X0]: (top=join(top,complement(X0)))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f27,f1367])).
% 22.33/3.28 fof(f1402,plain,(
% 22.33/3.28 ![X0]: (top=join(top,X0))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f613,f1392])).
% 22.33/3.28 fof(f1410,plain,(
% 22.33/3.28 ![X0]: (join(X0,converse(top))=top)),
% 22.33/3.28 inference(backward_demodulation,[status(thm)],[f1402,f1365])).
% 22.33/3.28 fof(f1430,plain,(
% 22.33/3.28 converse(top)=top),
% 22.33/3.28 inference(backward_demodulation,[status(thm)],[f1410,f951])).
% 22.33/3.28 fof(f1453,plain,(
% 22.33/3.28 ![X0,X1]: (join(X0,join(converse(complement(converse(X0))),X1))=join(top,X1))),
% 22.33/3.28 inference(backward_demodulation,[status(thm)],[f1430,f445])).
% 22.33/3.28 fof(f1454,plain,(
% 22.33/3.28 ![X0]: (X0=join(complement(top),meet(X0,converse(complement(converse(complement(X0)))))))),
% 22.33/3.28 inference(backward_demodulation,[status(thm)],[f1430,f459])).
% 22.33/3.28 fof(f1458,plain,(
% 22.33/3.28 ![X0,X1]: (join(X0,join(converse(complement(converse(X0))),X1))=top)),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f1402,f1453])).
% 22.33/3.28 fof(f1459,plain,(
% 22.33/3.28 ![X0]: (X0=join(zero,meet(X0,converse(complement(converse(complement(X0)))))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f254,f1454])).
% 22.33/3.28 fof(f1460,plain,(
% 22.33/3.28 ![X0]: (X0=meet(X0,converse(complement(converse(complement(X0))))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f647,f1459])).
% 22.33/3.28 fof(f1924,plain,(
% 22.33/3.28 ![X0,X1]: (join(meet(X0,X1),X0)=join(meet(X0,X1),meet(X0,complement(X1))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f52,f1072])).
% 22.33/3.28 fof(f1969,plain,(
% 22.33/3.28 ![X0,X1]: (join(X0,meet(X0,X1))=join(meet(X0,X1),meet(X0,complement(X1))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f16,f1924])).
% 22.33/3.28 fof(f1982,plain,(
% 22.33/3.28 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f52,f1969])).
% 22.33/3.28 fof(f2318,plain,(
% 22.33/3.28 ![X0,X1]: (X0=join(meet(X0,join(converse(complement(converse(complement(X0)))),X1)),complement(top)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f1458,f37])).
% 22.33/3.28 fof(f2352,plain,(
% 22.33/3.28 ![X0,X1]: (X0=join(complement(top),meet(X0,join(converse(complement(converse(complement(X0)))),X1))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f16,f2318])).
% 22.33/3.28 fof(f2353,plain,(
% 22.33/3.28 ![X0,X1]: (X0=join(zero,meet(X0,join(converse(complement(converse(complement(X0)))),X1))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f254,f2352])).
% 22.33/3.28 fof(f2354,plain,(
% 22.33/3.28 ![X0,X1]: (X0=meet(X0,join(converse(complement(converse(complement(X0)))),X1)))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f647,f2353])).
% 22.33/3.28 fof(f2377,plain,(
% 22.33/3.28 ![X0,X1]: (complement(X0)=meet(complement(X0),join(converse(complement(converse(X0))),X1)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f613,f2354])).
% 22.33/3.28 fof(f2410,plain,(
% 22.33/3.28 ![X0]: (complement(X0)=meet(complement(X0),converse(complement(converse(X0)))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f1982,f2377])).
% 22.33/3.28 fof(f2768,plain,(
% 22.33/3.28 ![X0,X1]: (X0=join(meet(X0,complement(X1)),complement(complement(meet(X1,X0)))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f1313,f37])).
% 22.33/3.28 fof(f2787,plain,(
% 22.33/3.28 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f613,f2768])).
% 22.33/3.28 fof(f2788,plain,(
% 22.33/3.28 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f16,f2787])).
% 22.33/3.28 fof(f2827,plain,(
% 22.33/3.28 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),X1)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f1318,f613])).
% 22.33/3.28 fof(f2917,plain,(
% 22.33/3.28 ![X0,X1]: (X0=join(meet(complement(X1),X0),meet(X0,X1)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f613,f2788])).
% 22.33/3.28 fof(f2922,plain,(
% 22.33/3.28 ![X0,X1]: (join(meet(X0,X1),X1)=join(meet(X0,X1),meet(X1,complement(X0))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f2788,f1072])).
% 22.33/3.28 fof(f2951,plain,(
% 22.33/3.28 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f16,f2917])).
% 22.33/3.28 fof(f2958,plain,(
% 22.33/3.28 ![X0,X1]: (join(X0,meet(X1,X0))=join(meet(X1,X0),meet(X0,complement(X1))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f16,f2922])).
% 22.33/3.28 fof(f2962,plain,(
% 22.33/3.28 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f2788,f2958])).
% 22.33/3.28 fof(f3017,plain,(
% 22.33/3.28 ![X0,X1]: (join(join(complement(X0),meet(X1,X0)),X1)=join(complement(X0),meet(X1,X0)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f1232,f2962])).
% 22.33/3.28 fof(f3049,plain,(
% 22.33/3.28 ![X0,X1]: (join(complement(X0),join(meet(X1,X0),X1))=join(complement(X0),meet(X1,X0)))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f17,f3017])).
% 22.33/3.28 fof(f3050,plain,(
% 22.33/3.28 ![X0,X1]: (join(complement(X0),join(X1,meet(X1,X0)))=join(complement(X0),meet(X1,X0)))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f16,f3049])).
% 22.33/3.28 fof(f3054,plain,(
% 22.33/3.28 ![X0,X1]: (join(complement(X0),X1)=join(complement(X0),meet(X1,X0)))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f1982,f3050])).
% 22.33/3.28 fof(f3210,plain,(
% 22.33/3.28 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=complement(complement(X0)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f2410,f1315])).
% 22.33/3.28 fof(f3251,plain,(
% 22.33/3.28 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=X0)),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f613,f3210])).
% 22.33/3.28 fof(f3324,plain,(
% 22.33/3.28 ![X0]: (converse(converse(X0))=join(X0,converse(complement(converse(complement(converse(converse(X0))))))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f3251,f42])).
% 22.33/3.28 fof(f3354,plain,(
% 22.33/3.28 ![X0]: (X0=join(X0,converse(complement(converse(complement(converse(converse(X0))))))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f23,f3324])).
% 22.33/3.28 fof(f3355,plain,(
% 22.33/3.28 ![X0]: (X0=join(X0,converse(complement(converse(complement(X0))))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f23,f3354])).
% 22.33/3.28 fof(f5195,plain,(
% 22.33/3.28 ![X0,X1]: (meet(X0,complement(complement(X1)))=complement(complement(meet(X1,X0))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f1313,f2827])).
% 22.33/3.28 fof(f5261,plain,(
% 22.33/3.28 ![X0,X1]: (meet(X0,X1)=complement(complement(meet(X1,X0))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f613,f5195])).
% 22.33/3.28 fof(f5265,plain,(
% 22.33/3.28 ~meet(sk2,converse(sk1))=zero),
% 22.33/3.28 inference(backward_demodulation,[status(thm)],[f5296,f30])).
% 22.33/3.28 fof(f5296,plain,(
% 22.33/3.28 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f613,f5261])).
% 22.33/3.28 fof(f7200,plain,(
% 22.33/3.28 ![X0]: (converse(complement(converse(complement(complement(X0)))))=join(meet(converse(complement(converse(complement(complement(X0))))),X0),complement(X0)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f1460,f2951])).
% 22.33/3.28 fof(f7229,plain,(
% 22.33/3.28 ![X0]: (converse(complement(converse(X0)))=join(meet(converse(complement(converse(complement(complement(X0))))),X0),complement(X0)))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f613,f7200])).
% 22.33/3.28 fof(f7230,plain,(
% 22.33/3.28 ![X0]: (converse(complement(converse(X0)))=join(complement(X0),meet(converse(complement(converse(complement(complement(X0))))),X0)))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f16,f7229])).
% 22.33/3.28 fof(f7231,plain,(
% 22.33/3.28 ![X0]: (converse(complement(converse(X0)))=join(complement(X0),converse(complement(converse(complement(complement(X0)))))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f3054,f7230])).
% 22.33/3.28 fof(f7313,plain,(
% 22.33/3.28 ![X0]: (converse(complement(converse(X0)))=complement(X0))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f3355,f7231])).
% 22.33/3.28 fof(f7433,plain,(
% 22.33/3.28 ![X0]: (converse(complement(X0))=complement(converse(X0)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f23,f7313])).
% 22.33/3.28 fof(f7917,plain,(
% 22.33/3.28 ![X0,X1]: (join(complement(X0),converse(complement(X1)))=complement(meet(converse(X1),X0)))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f7433,f1313])).
% 22.33/3.28 fof(f14501,plain,(
% 22.33/3.28 ![X0,X1]: (join(converse(complement(X0)),converse(complement(X1)))=complement(meet(converse(X1),converse(X0))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f7433,f7917])).
% 22.33/3.28 fof(f14557,plain,(
% 22.33/3.28 ![X0,X1]: (converse(join(complement(X0),complement(X1)))=complement(meet(converse(X0),converse(X1))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f797,f14501])).
% 22.33/3.28 fof(f14558,plain,(
% 22.33/3.28 ![X0,X1]: (converse(complement(meet(X0,X1)))=complement(meet(converse(X1),converse(X0))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f1313,f14557])).
% 22.33/3.28 fof(f15061,plain,(
% 22.33/3.28 ![X0,X1]: (meet(converse(X0),converse(X1))=complement(converse(complement(meet(X1,X0)))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f14558,f613])).
% 22.33/3.28 fof(f15141,plain,(
% 22.33/3.28 ![X0,X1]: (meet(converse(X0),converse(X1))=converse(complement(complement(meet(X1,X0)))))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f7433,f15061])).
% 22.33/3.28 fof(f15217,plain,(
% 22.33/3.28 ![X0,X1]: (meet(converse(X0),converse(X1))=converse(meet(X1,X0)))),
% 22.33/3.28 inference(forward_demodulation,[status(thm)],[f613,f15141])).
% 22.33/3.28 fof(f15324,plain,(
% 22.33/3.28 ![X0,X1]: (meet(X0,converse(X1))=converse(meet(X1,converse(X0))))),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f23,f15217])).
% 22.33/3.28 fof(f15557,plain,(
% 22.33/3.28 meet(sk2,converse(sk1))=converse(zero)),
% 22.33/3.28 inference(paramodulation,[status(thm)],[f29,f15324])).
% 21.75/3.34 fof(f15601,plain,(
% 21.75/3.34 meet(sk2,converse(sk1))=zero),
% 21.75/3.34 inference(forward_demodulation,[status(thm)],[f1085,f15557])).
% 21.75/3.34 fof(f15602,plain,(
% 21.75/3.34 $false),
% 21.75/3.34 inference(forward_subsumption_resolution,[status(thm)],[f15601,f5265])).
% 21.75/3.34 % SZS output end CNFRefutation for theBenchmark.p
% 21.75/3.37 % Elapsed time: 2.985981 seconds
% 21.75/3.37 % CPU time: 23.524094 seconds
% 21.75/3.37 % Total memory used: 264.035 MB
% 21.75/3.37 % Net memory used: 257.344 MB
%------------------------------------------------------------------------------