%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL005-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:03:31 PM UTC 2026
% Result : Unsatisfiable 77.04s 10.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL005-1 : 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.54 % Computer : n019.cluster.edu
% 0.10/0.54 % Model : x86_64 x86_64
% 0.10/0.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.54 % Memory : 8046.5625MB
% 0.10/0.54 % OS : Linux 6.8.0-71-generic
% 0.10/0.54 % CPULimit : 300
% 0.10/0.54 % WCLimit : 300
% 0.10/0.54 % DateTime : Mon Sep 21 03:57:51 UTC 2026
% 0.10/0.54 % CPUTime :
% 0.10/0.55 % Drodi V4.1.1
% 77.04/10.43 % Refutation found
% 77.04/10.43 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 77.04/10.43 % SZS output start CNFRefutation for theBenchmark
% 77.04/10.43 fof(f1,axiom,(
% 77.04/10.43 (![A,B]: (join(A,B) = join(B,A) ))),
% 77.04/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.04/10.43 fof(f2,axiom,(
% 77.04/10.43 (![A,B,C]: (join(A,join(B,C)) = join(join(A,B),C) ))),
% 77.04/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.04/10.43 fof(f3,axiom,(
% 77.04/10.43 (![A,B]: (A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))) ))),
% 77.04/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.04/10.43 fof(f4,axiom,(
% 77.04/10.43 (![A,B]: (meet(A,B) = complement(join(complement(A),complement(B))) ))),
% 77.04/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.04/10.43 fof(f6,axiom,(
% 77.04/10.43 (![A]: (composition(A,one) = A ))),
% 77.04/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.04/10.43 fof(f8,axiom,(
% 77.04/10.43 (![A]: (converse(converse(A)) = A ))),
% 77.04/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.04/10.43 fof(f9,axiom,(
% 77.04/10.43 (![A,B]: (converse(join(A,B)) = join(converse(A),converse(B)) ))),
% 77.04/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.04/10.43 fof(f10,axiom,(
% 77.04/10.43 (![A,B]: (converse(composition(A,B)) = composition(converse(B),converse(A)) ))),
% 77.04/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.04/10.43 fof(f11,axiom,(
% 77.04/10.43 (![A,B]: (join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B) ))),
% 77.04/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.04/10.43 fof(f12,axiom,(
% 77.04/10.43 (![A]: (top = join(A,complement(A)) ))),
% 77.04/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.04/10.43 fof(f13,axiom,(
% 77.04/10.43 (![A]: (zero = meet(A,complement(A)) ))),
% 77.04/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.04/10.43 fof(f14,negated_conjecture,(
% 77.04/10.43 converse(meet(sk1,sk2)) != meet(converse(sk1),converse(sk2)) ),
% 77.04/10.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 77.04/10.43 fof(f15,plain,(
% 77.04/10.43 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 77.04/10.43 inference(cnf_transformation,[status(thm)],[f1])).
% 77.04/10.43 fof(f16,plain,(
% 77.04/10.43 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 77.04/10.43 inference(cnf_transformation,[status(thm)],[f2])).
% 77.04/10.43 fof(f17,plain,(
% 77.04/10.43 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 77.04/10.43 inference(cnf_transformation,[status(thm)],[f3])).
% 77.04/10.43 fof(f18,plain,(
% 77.04/10.43 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 77.04/10.43 inference(cnf_transformation,[status(thm)],[f4])).
% 77.04/10.43 fof(f20,plain,(
% 77.04/10.43 ![X0]: (composition(X0,one)=X0)),
% 77.04/10.43 inference(cnf_transformation,[status(thm)],[f6])).
% 77.04/10.43 fof(f22,plain,(
% 77.04/10.43 ![X0]: (converse(converse(X0))=X0)),
% 77.04/10.43 inference(cnf_transformation,[status(thm)],[f8])).
% 77.04/10.43 fof(f23,plain,(
% 77.04/10.43 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 77.04/10.43 inference(cnf_transformation,[status(thm)],[f9])).
% 77.04/10.43 fof(f24,plain,(
% 77.04/10.43 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 77.04/10.43 inference(cnf_transformation,[status(thm)],[f10])).
% 77.04/10.43 fof(f25,plain,(
% 77.04/10.43 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 77.04/10.43 inference(cnf_transformation,[status(thm)],[f11])).
% 77.04/10.43 fof(f26,plain,(
% 77.04/10.43 ![X0]: (top=join(X0,complement(X0)))),
% 77.04/10.43 inference(cnf_transformation,[status(thm)],[f12])).
% 77.04/10.43 fof(f27,plain,(
% 77.04/10.43 ![X0]: (zero=meet(X0,complement(X0)))),
% 77.04/10.43 inference(cnf_transformation,[status(thm)],[f13])).
% 77.04/10.43 fof(f28,plain,(
% 77.04/10.43 ~converse(meet(sk1,sk2))=meet(converse(sk1),converse(sk2))),
% 77.04/10.43 inference(cnf_transformation,[status(thm)],[f14])).
% 77.04/10.43 fof(f35,plain,(
% 77.04/10.43 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 77.04/10.43 inference(forward_demodulation,[status(thm)],[f15,f17])).
% 77.04/10.43 fof(f36,plain,(
% 77.04/10.43 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 77.04/10.43 inference(backward_demodulation,[status(thm)],[f18,f35])).
% 77.04/10.43 fof(f37,plain,(
% 77.04/10.43 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 77.04/10.43 inference(forward_demodulation,[status(thm)],[f15,f25])).
% 77.04/10.43 fof(f38,plain,(
% 77.04/10.43 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 77.04/10.43 inference(forward_demodulation,[status(thm)],[f15,f36])).
% 77.04/10.44 fof(f41,plain,(
% 77.04/10.44 ![X0,X1,X2]: (meet(X0,join(complement(X1),complement(X2)))=complement(join(complement(X0),meet(X1,X2))))),
% 77.04/10.44 inference(paramodulation,[status(thm)],[f18,f18])).
% 77.04/10.44 fof(f42,plain,(
% 77.04/10.44 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 77.04/10.44 inference(paramodulation,[status(thm)],[f22,f23])).
% 77.04/10.44 fof(f43,plain,(
% 77.04/10.44 ![X0,X1]: (converse(join(X0,converse(X1)))=join(converse(X0),X1))),
% 77.04/10.44 inference(paramodulation,[status(thm)],[f22,f23])).
% 77.04/10.44 fof(f45,plain,(
% 77.04/10.44 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 77.04/10.44 inference(paramodulation,[status(thm)],[f22,f24])).
% 77.04/10.44 fof(f62,plain,(
% 77.04/10.44 ![X0,X1]: (join(complement(X0),composition(X1,complement(composition(converse(X1),X0))))=complement(X0))),
% 77.04/10.44 inference(paramodulation,[status(thm)],[f22,f37])).
% 77.04/10.44 fof(f66,plain,(
% 77.04/10.44 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 77.04/10.44 inference(paramodulation,[status(thm)],[f18,f38])).
% 77.04/10.44 fof(f69,plain,(
% 77.04/10.44 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 77.04/10.44 inference(forward_demodulation,[status(thm)],[f15,f66])).
% 77.04/10.44 fof(f145,plain,(
% 77.04/10.44 ![X0,X1,X2]: (join(meet(X0,X1),composition(X2,complement(composition(converse(X2),join(complement(X0),complement(X1))))))=complement(join(complement(X0),complement(X1))))),
% 77.04/10.44 inference(paramodulation,[status(thm)],[f18,f62])).
% 77.04/10.44 fof(f153,plain,(
% 77.04/10.44 ![X0,X1,X2]: (join(meet(X0,X1),composition(X2,complement(composition(converse(X2),join(complement(X0),complement(X1))))))=meet(X0,X1))),
% 77.04/10.44 inference(forward_demodulation,[status(thm)],[f18,f145])).
% 77.04/10.44 fof(f300,plain,(
% 77.04/10.44 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 77.04/10.44 inference(paramodulation,[status(thm)],[f20,f45])).
% 77.04/10.44 fof(f304,plain,(
% 77.04/10.44 ![X0]: (X0=composition(converse(one),X0))),
% 77.04/10.44 inference(forward_demodulation,[status(thm)],[f22,f300])).
% 77.04/10.44 fof(f309,plain,(
% 77.04/10.44 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 77.04/10.44 inference(paramodulation,[status(thm)],[f26,f42])).
% 77.04/10.44 fof(f316,plain,(
% 77.04/10.44 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 77.04/10.44 inference(paramodulation,[status(thm)],[f26,f18])).
% 77.04/10.45 fof(f334,plain,(
% 77.04/10.45 zero=complement(top)),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f27,f316])).
% 77.04/10.45 fof(f337,plain,(
% 77.04/10.45 top=join(top,zero)),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f334,f26])).
% 77.04/10.45 fof(f436,plain,(
% 77.04/10.45 one=converse(one)),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f20,f304])).
% 77.04/10.45 fof(f440,plain,(
% 77.04/10.45 ![X0,X1]: (join(meet(X0,X1),composition(one,complement(join(complement(X0),complement(X1)))))=meet(X0,X1))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f304,f153])).
% 77.04/10.45 fof(f445,plain,(
% 77.04/10.45 ![X0]: (join(complement(X0),composition(one,complement(X0)))=complement(X0))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f304,f62])).
% 77.04/10.45 fof(f463,plain,(
% 77.04/10.45 ![X0]: (X0=composition(one,X0))),
% 77.04/10.45 inference(backward_demodulation,[status(thm)],[f436,f304])).
% 77.04/10.45 fof(f464,plain,(
% 77.04/10.45 ![X0,X1]: (join(meet(X0,X1),composition(one,meet(X0,X1)))=meet(X0,X1))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f18,f440])).
% 77.04/10.45 fof(f486,plain,(
% 77.04/10.45 ![X0,X1]: (join(meet(X0,X1),meet(X0,X1))=meet(X0,X1))),
% 77.04/10.45 inference(backward_demodulation,[status(thm)],[f463,f464])).
% 77.04/10.45 fof(f493,plain,(
% 77.04/10.45 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 77.04/10.45 inference(backward_demodulation,[status(thm)],[f463,f445])).
% 77.04/10.45 fof(f597,plain,(
% 77.04/10.45 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f493,f18])).
% 77.04/10.45 fof(f598,plain,(
% 77.04/10.45 ![X0]: (X0=join(meet(X0,complement(X0)),complement(complement(X0))))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f493,f38])).
% 77.04/10.45 fof(f619,plain,(
% 77.04/10.45 ![X0]: (X0=join(complement(complement(X0)),meet(X0,complement(X0))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f598])).
% 77.04/10.45 fof(f620,plain,(
% 77.04/10.45 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f27,f619])).
% 77.04/10.45 fof(f621,plain,(
% 77.04/10.45 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f620])).
% 77.04/10.45 fof(f625,plain,(
% 77.04/10.45 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(meet(X0,X1))))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f18,f621])).
% 77.04/10.45 fof(f644,plain,(
% 77.04/10.45 ![X0]: (join(complement(complement(X0)),meet(X0,X0))=complement(complement(X0)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f597,f493])).
% 77.04/10.45 fof(f647,plain,(
% 77.04/10.45 ![X0]: (top=join(complement(X0),meet(X0,X0)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f597,f26])).
% 77.04/10.45 fof(f847,plain,(
% 77.04/10.45 ![X0]: (join(meet(X0,X0),complement(complement(X0)))=meet(X0,X0))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f597,f486])).
% 77.04/10.45 fof(f914,plain,(
% 77.04/10.45 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f15,f18])).
% 77.04/10.45 fof(f915,plain,(
% 77.04/10.45 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(X1,complement(X0)))))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f15,f38])).
% 77.04/10.45 fof(f916,plain,(
% 77.04/10.45 ![X0,X1]: (converse(join(converse(X0),X1))=join(converse(X1),X0))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f15,f43])).
% 77.04/10.45 fof(f932,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,join(X1,complement(join(X0,X1))))=top)),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f26,f16])).
% 77.04/10.45 fof(f933,plain,(
% 77.04/10.45 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f15,f16])).
% 77.04/10.45 fof(f936,plain,(
% 77.04/10.45 ![X0,X1]: (join(zero,join(complement(complement(X0)),X1))=join(X0,X1))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f621,f16])).
% 77.04/10.45 fof(f946,plain,(
% 77.04/10.45 ![X0,X1,X2]: (join(meet(X0,X1),join(complement(join(complement(X0),X1)),X2))=join(X0,X2))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f38,f16])).
% 77.04/10.45 fof(f947,plain,(
% 77.04/10.45 ![X0,X1]: (join(complement(X0),join(meet(X0,X0),X1))=join(top,X1))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f647,f16])).
% 77.04/10.45 fof(f952,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,join(converse(complement(converse(X0))),X1))=join(converse(top),X1))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f309,f16])).
% 77.04/10.45 fof(f1311,plain,(
% 77.04/10.45 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f18,f915])).
% 77.04/10.45 fof(f1317,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,complement(X1))=join(meet(join(X0,complement(X1)),meet(X1,X0)),complement(X1)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f915,f915])).
% 77.04/10.45 fof(f1341,plain,(
% 77.04/10.45 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f1311])).
% 77.04/10.45 fof(f1350,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,complement(X1))=join(complement(X1),meet(join(X0,complement(X1)),meet(X1,X0))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f1317])).
% 77.04/10.45 fof(f1367,plain,(
% 77.04/10.45 ![X0,X1]: (X0=join(meet(complement(X1),X0),meet(X0,meet(X1,X1))))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f597,f1341])).
% 77.04/10.45 fof(f1468,plain,(
% 77.04/10.45 ![X0]: (join(zero,complement(complement(X0)))=join(X0,meet(X0,X0)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f644,f936])).
% 77.04/10.45 fof(f1470,plain,(
% 77.04/10.45 ![X0]: (join(zero,top)=join(X0,meet(complement(X0),complement(X0))))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f647,f936])).
% 77.04/10.45 fof(f1471,plain,(
% 77.04/10.45 ![X0]: (join(zero,complement(complement(X0)))=join(X0,complement(complement(X0))))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f493,f936])).
% 77.04/10.45 fof(f1487,plain,(
% 77.04/10.45 ![X0]: (X0=join(X0,meet(X0,X0)))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f621,f1468])).
% 77.04/10.45 fof(f1489,plain,(
% 77.04/10.45 ![X0]: (join(top,zero)=join(X0,meet(complement(X0),complement(X0))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f1470])).
% 77.04/10.45 fof(f1490,plain,(
% 77.04/10.45 ![X0]: (top=join(X0,meet(complement(X0),complement(X0))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f337,f1489])).
% 77.04/10.45 fof(f1491,plain,(
% 77.04/10.45 ![X0]: (top=join(X0,complement(complement(complement(X0)))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f597,f1490])).
% 77.04/10.45 fof(f1492,plain,(
% 77.04/10.45 ![X0]: (X0=join(X0,complement(complement(X0))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f621,f1471])).
% 77.04/10.45 fof(f1511,plain,(
% 77.04/10.45 ![X0]: (meet(X0,join(complement(complement(X0)),complement(complement(X0))))=complement(complement(X0)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f1487,f41])).
% 77.04/10.45 fof(f1521,plain,(
% 77.04/10.45 ![X0]: (meet(X0,complement(complement(X0)))=complement(complement(X0)))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f493,f1511])).
% 77.04/10.45 fof(f1546,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,join(complement(complement(X0)),X1))=join(X0,X1))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f1492,f16])).
% 77.04/10.45 fof(f1585,plain,(
% 77.04/10.45 ![X0]: (meet(X0,complement(complement(complement(X0))))=complement(top))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f1491,f18])).
% 77.04/10.45 fof(f1586,plain,(
% 77.04/10.45 ![X0]: (X0=join(meet(X0,complement(complement(complement(complement(X0))))),complement(top)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f1491,f38])).
% 77.04/10.45 fof(f1587,plain,(
% 77.04/10.45 ![X0]: (complement(complement(X0))=join(meet(complement(complement(X0)),X0),complement(top)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f1491,f915])).
% 77.04/10.45 fof(f1606,plain,(
% 77.04/10.45 ![X0]: (meet(X0,complement(complement(complement(X0))))=zero)),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f334,f1585])).
% 77.04/10.45 fof(f1607,plain,(
% 77.04/10.45 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(complement(complement(X0)))))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f1586])).
% 77.04/10.45 fof(f1608,plain,(
% 77.04/10.45 ![X0]: (X0=join(zero,meet(X0,complement(complement(complement(complement(X0)))))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f334,f1607])).
% 77.04/10.45 fof(f1609,plain,(
% 77.04/10.45 ![X0]: (complement(complement(X0))=join(complement(top),meet(complement(complement(X0)),X0)))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f1587])).
% 77.04/10.45 fof(f1610,plain,(
% 77.04/10.45 ![X0]: (complement(complement(X0))=join(zero,meet(complement(complement(X0)),X0)))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f334,f1609])).
% 77.04/10.45 fof(f2110,plain,(
% 77.04/10.45 ![X0]: (X0=join(meet(complement(complement(X0)),X0),zero))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f1606,f1341])).
% 77.04/10.45 fof(f2113,plain,(
% 77.04/10.45 ![X0]: (complement(complement(complement(X0)))=join(zero,meet(complement(complement(complement(X0))),complement(X0))))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f1606,f1341])).
% 77.04/10.45 fof(f2135,plain,(
% 77.04/10.45 ![X0]: (complement(complement(X0))=X0)),
% 77.04/10.45 inference(backward_demodulation,[status(thm)],[f2136,f1610])).
% 77.04/10.45 fof(f2136,plain,(
% 77.04/10.45 ![X0]: (X0=join(zero,meet(complement(complement(X0)),X0)))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f2110])).
% 77.04/10.45 fof(f2152,plain,(
% 77.04/10.45 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 77.04/10.45 inference(backward_demodulation,[status(thm)],[f2164,f1608])).
% 77.04/10.45 fof(f2164,plain,(
% 77.04/10.45 ![X0]: (complement(complement(complement(X0)))=complement(X0))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f2136,f2113])).
% 77.04/10.45 fof(f2203,plain,(
% 77.04/10.45 ![X0]: (join(meet(X0,X0),X0)=meet(X0,X0))),
% 77.04/10.45 inference(backward_demodulation,[status(thm)],[f2135,f847])).
% 77.04/10.45 fof(f2230,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,join(X0,X1))=join(X0,X1))),
% 77.04/10.45 inference(backward_demodulation,[status(thm)],[f2135,f1546])).
% 77.04/10.45 fof(f2250,plain,(
% 77.04/10.45 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f1521,f2152])).
% 77.04/10.45 fof(f2255,plain,(
% 77.04/10.45 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 77.04/10.45 inference(backward_demodulation,[status(thm)],[f2284,f625])).
% 77.04/10.45 fof(f2284,plain,(
% 77.04/10.45 ![X0]: (X0=join(zero,X0))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f2135,f2250])).
% 77.04/10.45 fof(f2307,plain,(
% 77.04/10.45 ![X0]: (join(X0,meet(X0,X0))=meet(X0,X0))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f2203])).
% 77.04/10.45 fof(f2320,plain,(
% 77.04/10.45 ![X0,X1]: (X0=join(meet(complement(X1),X0),meet(X0,X1)))),
% 77.04/10.45 inference(backward_demodulation,[status(thm)],[f2345,f1367])).
% 77.04/10.45 fof(f2322,plain,(
% 77.04/10.45 ![X0,X1]: (join(complement(X0),join(X0,X1))=join(top,X1))),
% 77.04/10.45 inference(backward_demodulation,[status(thm)],[f2345,f947])).
% 77.04/10.45 fof(f2345,plain,(
% 77.04/10.45 ![X0]: (X0=meet(X0,X0))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f1487,f2307])).
% 77.04/10.45 fof(f2437,plain,(
% 77.04/10.45 ![X0,X1]: (meet(X0,X1)=complement(complement(meet(X1,X0))))),
% 77.04/10.45 inference(backward_demodulation,[status(thm)],[f2255,f914])).
% 77.04/10.45 fof(f2563,plain,(
% 77.04/10.45 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f2320])).
% 77.04/10.45 fof(f2564,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,join(X1,complement(X0)))=join(top,X1))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f933,f2322])).
% 77.04/10.45 fof(f2622,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,complement(X1))=join(complement(X1),meet(meet(X1,X0),join(X0,complement(X1)))))),
% 77.04/10.45 inference(backward_demodulation,[status(thm)],[f2623,f1350])).
% 77.04/10.45 fof(f2623,plain,(
% 77.04/10.45 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f2135,f2437])).
% 77.04/10.45 fof(f2645,plain,(
% 77.04/10.45 ![X0]: (X0=join(X0,meet(X0,complement(X0))))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f2345,f1341])).
% 77.04/10.45 fof(f2658,plain,(
% 77.04/10.45 ![X0]: (X0=join(X0,zero))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f27,f2645])).
% 77.04/10.45 fof(f2876,plain,(
% 77.04/10.45 ![X0,X1]: (join(meet(X0,X1),X1)=join(meet(X0,X1),meet(X1,complement(X0))))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f1341,f2230])).
% 77.04/10.45 fof(f2877,plain,(
% 77.04/10.45 ![X0,X1]: (join(meet(X0,X1),X0)=join(meet(X0,X1),meet(X0,complement(X1))))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f69,f2230])).
% 77.04/10.45 fof(f2888,plain,(
% 77.04/10.45 ![X0]: (join(X0,top)=join(X0,complement(X0)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f26,f2230])).
% 77.04/10.45 fof(f2903,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,meet(X1,X0))=join(meet(X1,X0),meet(X0,complement(X1))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f2876])).
% 77.04/10.45 fof(f2906,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f1341,f2903])).
% 77.04/10.45 fof(f2907,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,meet(X0,X1))=join(meet(X0,X1),meet(X0,complement(X1))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f2877])).
% 77.04/10.45 fof(f2921,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f69,f2907])).
% 77.04/10.45 fof(f2938,plain,(
% 77.04/10.45 ![X0]: (join(X0,top)=top)),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f26,f2888])).
% 77.04/10.45 fof(f2988,plain,(
% 77.04/10.45 ![X0]: (join(top,X0)=top)),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f15,f2938])).
% 77.04/10.45 fof(f3014,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,join(X1,complement(X0)))=top)),
% 77.04/10.45 inference(backward_demodulation,[status(thm)],[f2988,f2564])).
% 77.04/10.45 fof(f3055,plain,(
% 77.04/10.45 converse(top)=top),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f309,f2988])).
% 77.04/10.45 fof(f3073,plain,(
% 77.04/10.45 ![X0]: (top=join(X0,converse(complement(converse(X0)))))),
% 77.04/10.45 inference(backward_demodulation,[status(thm)],[f3055,f309])).
% 77.04/10.45 fof(f3077,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,join(converse(complement(converse(X0))),X1))=join(top,X1))),
% 77.04/10.45 inference(backward_demodulation,[status(thm)],[f3055,f952])).
% 77.04/10.45 fof(f3096,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,join(converse(complement(converse(X0))),X1))=top)),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f2988,f3077])).
% 77.04/10.45 fof(f3278,plain,(
% 77.04/10.45 ![X0,X1]: (X0=join(meet(X0,join(X1,complement(join(complement(X0),X1)))),complement(top)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f932,f38])).
% 77.04/10.45 fof(f3313,plain,(
% 77.04/10.45 ![X0,X1]: (X0=join(complement(top),meet(X0,join(X1,complement(join(complement(X0),X1))))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f3278])).
% 77.04/10.45 fof(f3314,plain,(
% 77.04/10.45 ![X0,X1]: (X0=join(zero,meet(X0,join(X1,complement(join(complement(X0),X1))))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f334,f3313])).
% 77.04/10.45 fof(f3315,plain,(
% 77.04/10.45 ![X0,X1]: (X0=meet(X0,join(X1,complement(join(complement(X0),X1)))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f2284,f3314])).
% 77.04/10.45 fof(f3340,plain,(
% 77.04/10.45 ![X0,X1]: (X0=join(meet(X0,join(X1,complement(complement(X0)))),complement(top)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f3014,f38])).
% 77.04/10.45 fof(f3355,plain,(
% 77.04/10.45 ![X0,X1]: (X0=join(complement(top),meet(X0,join(X1,complement(complement(X0))))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f3340])).
% 77.04/10.45 fof(f3356,plain,(
% 77.04/10.45 ![X0,X1]: (X0=join(zero,meet(X0,join(X1,complement(complement(X0))))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f334,f3355])).
% 77.04/10.45 fof(f3357,plain,(
% 77.04/10.45 ![X0,X1]: (X0=meet(X0,join(X1,complement(complement(X0)))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f2284,f3356])).
% 77.04/10.45 fof(f3358,plain,(
% 77.04/10.45 ![X0,X1]: (X0=meet(X0,join(X1,X0)))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f2135,f3357])).
% 77.04/10.45 fof(f3383,plain,(
% 77.04/10.45 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X1))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f2906,f3358])).
% 77.04/10.45 fof(f3391,plain,(
% 77.04/10.45 ![X0,X1]: (X0=meet(X0,join(X0,X1)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f15,f3358])).
% 77.04/10.45 fof(f3413,plain,(
% 77.04/10.45 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X0,X1)))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f2623,f3383])).
% 77.04/10.45 fof(f3512,plain,(
% 77.04/10.45 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X1,X0)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f2623,f3413])).
% 77.04/10.45 fof(f3635,plain,(
% 77.04/10.45 ![X0,X1,X2]: (meet(X0,X1)=meet(meet(X0,X1),join(X0,X2)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f946,f3391])).
% 77.04/10.45 fof(f4156,plain,(
% 77.04/10.45 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X1,X0)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f15,f2255])).
% 77.04/10.45 fof(f4158,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,complement(X1))=complement(meet(complement(X0),X1)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f2135,f2255])).
% 77.04/10.45 fof(f4161,plain,(
% 77.04/10.45 ![X0,X1]: (join(complement(X0),X1)=complement(meet(X0,complement(X1))))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f2135,f2255])).
% 77.04/10.45 fof(f5499,plain,(
% 77.04/10.45 ![X0,X1,X2]: (meet(X0,meet(X0,X1))=meet(meet(X1,X0),join(X0,X2)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f3512,f3635])).
% 77.04/10.45 fof(f5576,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,complement(X1))=join(complement(X1),meet(X1,X0)))),
% 77.04/10.45 inference(backward_demodulation,[status(thm)],[f5577,f2622])).
% 77.04/10.45 fof(f5577,plain,(
% 77.04/10.45 ![X0,X1,X2]: (meet(X0,X1)=meet(meet(X0,X1),join(X1,X2)))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f3512,f5499])).
% 77.04/10.45 fof(f5644,plain,(
% 77.04/10.45 ![X0,X1]: (join(complement(X0),X1)=complement(meet(complement(X1),X0)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f2135,f4156])).
% 77.04/10.45 fof(f5742,plain,(
% 77.04/10.45 ![X0,X1]: (complement(join(X0,complement(X1)))=meet(complement(X0),X1))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f4158,f2135])).
% 77.04/10.45 fof(f5846,plain,(
% 77.04/10.45 ![X0,X1]: (complement(join(complement(X0),X1))=meet(X0,complement(X1)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f4161,f2135])).
% 77.04/10.45 fof(f5919,plain,(
% 77.04/10.45 ![X0,X1]: (X0=meet(X0,join(X1,meet(X0,complement(X1)))))),
% 77.04/10.45 inference(backward_demodulation,[status(thm)],[f5846,f3315])).
% 77.04/10.45 fof(f5982,plain,(
% 77.04/10.45 ![X0,X1]: (join(join(X0,meet(X1,complement(X0))),X1)=join(X0,meet(X1,complement(X0))))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f5919,f2906])).
% 77.04/10.45 fof(f6022,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,join(meet(X1,complement(X0)),X1))=join(X0,meet(X1,complement(X0))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f16,f5982])).
% 77.04/10.45 fof(f6023,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,join(X1,meet(X1,complement(X0))))=join(X0,meet(X1,complement(X0))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f6022])).
% 77.04/10.45 fof(f6033,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,X1)=join(X0,meet(X1,complement(X0))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f2921,f6023])).
% 77.04/10.45 fof(f6050,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,X1)=join(X0,meet(complement(X0),X1)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f2623,f6033])).
% 77.04/10.45 fof(f7582,plain,(
% 77.04/10.45 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X2,X0)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f15,f933])).
% 77.04/10.45 fof(f8374,plain,(
% 77.04/10.45 ![X0,X1]: (complement(join(complement(X0),X1))=meet(complement(X1),X0))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f5644,f2135])).
% 77.04/10.45 fof(f8621,plain,(
% 77.04/10.45 ![X0,X1]: (complement(join(X0,X1))=meet(complement(X0),complement(X1)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f2135,f5742])).
% 77.04/10.45 fof(f10887,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,complement(X1))=join(X0,complement(join(X0,X1))))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f8621,f6050])).
% 77.04/10.45 fof(f15794,plain,(
% 77.04/10.45 ![X0,X1]: (join(meet(X0,X1),complement(X0))=join(complement(X0),meet(X1,X0)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f3512,f5576])).
% 77.04/10.45 fof(f15942,plain,(
% 77.04/10.45 ![X0,X1]: (join(complement(X0),meet(X0,X1))=join(complement(X0),meet(X1,X0)))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f15794])).
% 77.04/10.45 fof(f15943,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,complement(X1))=join(complement(X1),meet(X0,X1)))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f5576,f15942])).
% 77.04/10.45 fof(f17624,plain,(
% 77.04/10.45 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=join(X0,complement(top)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f3073,f10887])).
% 77.04/10.45 fof(f17632,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,complement(join(converse(complement(converse(X0))),X1)))=join(X0,complement(top)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f3096,f10887])).
% 77.04/10.45 fof(f17855,plain,(
% 77.04/10.45 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=join(X0,zero))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f334,f17624])).
% 77.04/10.45 fof(f17856,plain,(
% 77.04/10.45 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=X0)),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f2658,f17855])).
% 77.04/10.45 fof(f17867,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,complement(join(converse(complement(converse(X0))),X1)))=join(X0,zero))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f334,f17632])).
% 77.04/10.45 fof(f17868,plain,(
% 77.04/10.45 ![X0,X1]: (join(X0,complement(join(converse(complement(converse(X0))),X1)))=X0)),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f2658,f17867])).
% 77.04/10.45 fof(f18038,plain,(
% 77.04/10.45 ![X0]: (converse(converse(X0))=join(converse(complement(converse(complement(converse(converse(X0)))))),X0))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f17856,f916])).
% 77.04/10.45 fof(f18119,plain,(
% 77.04/10.45 ![X0]: (X0=join(converse(complement(converse(complement(converse(converse(X0)))))),X0))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f22,f18038])).
% 77.04/10.45 fof(f18120,plain,(
% 77.04/10.45 ![X0]: (X0=join(X0,converse(complement(converse(complement(converse(converse(X0))))))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f18119])).
% 77.04/10.45 fof(f18122,plain,(
% 77.04/10.45 ![X0]: (X0=join(X0,converse(complement(converse(complement(X0))))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f22,f18120])).
% 77.04/10.45 fof(f19067,plain,(
% 77.04/10.45 ![X0,X1]: (complement(complement(X0))=meet(complement(complement(join(converse(complement(converse(complement(X0)))),X1))),X0))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f17868,f8374])).
% 77.04/10.45 fof(f19165,plain,(
% 77.04/10.45 ![X0,X1]: (X0=meet(complement(complement(join(converse(complement(converse(complement(X0)))),X1))),X0))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f2135,f19067])).
% 77.04/10.45 fof(f19166,plain,(
% 77.04/10.45 ![X0,X1]: (X0=meet(X0,complement(complement(join(converse(complement(converse(complement(X0)))),X1)))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f2623,f19165])).
% 77.04/10.45 fof(f19168,plain,(
% 77.04/10.45 ![X0,X1]: (X0=meet(X0,join(converse(complement(converse(complement(X0)))),X1)))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f2135,f19166])).
% 77.04/10.45 fof(f20050,plain,(
% 77.04/10.45 ![X0,X1]: (join(converse(complement(converse(complement(complement(X0))))),X1)=join(meet(join(converse(complement(converse(complement(complement(X0))))),X1),X0),complement(X0)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f19168,f2563])).
% 77.04/10.45 fof(f20117,plain,(
% 77.04/10.45 ![X0,X1]: (join(converse(complement(converse(X0))),X1)=join(meet(join(converse(complement(converse(complement(complement(X0))))),X1),X0),complement(X0)))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f2135,f20050])).
% 77.04/10.45 fof(f20118,plain,(
% 77.04/10.45 ![X0,X1]: (join(converse(complement(converse(X0))),X1)=join(complement(X0),meet(join(converse(complement(converse(complement(complement(X0))))),X1),X0)))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15,f20117])).
% 77.04/10.45 fof(f20119,plain,(
% 77.04/10.45 ![X0,X1]: (join(converse(complement(converse(X0))),X1)=join(join(converse(complement(converse(complement(complement(X0))))),X1),complement(X0)))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f15943,f20118])).
% 77.04/10.45 fof(f20120,plain,(
% 77.04/10.45 ![X0,X1]: (join(converse(complement(converse(X0))),X1)=join(X1,join(complement(X0),converse(complement(converse(complement(complement(X0))))))))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f7582,f20119])).
% 77.04/10.45 fof(f20155,plain,(
% 77.04/10.45 ![X0,X1]: (join(converse(complement(converse(X0))),X1)=join(X1,complement(X0)))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f18122,f20120])).
% 77.04/10.45 fof(f20345,plain,(
% 77.04/10.45 ![X0]: (converse(complement(converse(X0)))=join(zero,complement(X0)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f2658,f20155])).
% 77.04/10.45 fof(f20373,plain,(
% 77.04/10.45 ![X0,X1]: (converse(join(X0,complement(X1)))=join(complement(converse(X1)),converse(X0)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f20155,f42])).
% 77.04/10.45 fof(f20610,plain,(
% 77.04/10.45 ![X0]: (converse(complement(converse(X0)))=complement(X0))),
% 77.04/10.45 inference(forward_demodulation,[status(thm)],[f2284,f20345])).
% 77.04/10.45 fof(f21247,plain,(
% 77.04/10.45 ![X0]: (converse(complement(X0))=complement(converse(X0)))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f22,f20610])).
% 77.04/10.45 fof(f21496,plain,(
% 77.04/10.45 ![X0,X1]: (converse(meet(complement(X0),X1))=complement(converse(join(X0,complement(X1)))))),
% 77.04/10.45 inference(paramodulation,[status(thm)],[f5742,f21247])).
% 77.04/10.58 fof(f31524,plain,(
% 77.04/10.58 ![X0,X1]: (complement(converse(join(X0,complement(X1))))=meet(complement(converse(X0)),converse(X1)))),
% 77.04/10.58 inference(paramodulation,[status(thm)],[f20373,f8374])).
% 77.04/10.58 fof(f31633,plain,(
% 77.04/10.58 ![X0,X1]: (converse(meet(complement(X0),X1))=meet(complement(converse(X0)),converse(X1)))),
% 77.04/10.58 inference(forward_demodulation,[status(thm)],[f21496,f31524])).
% 77.04/10.58 fof(f34261,plain,(
% 77.04/10.58 ![X0,X1]: (converse(meet(complement(complement(X0)),X1))=meet(complement(complement(converse(X0))),converse(X1)))),
% 77.04/10.58 inference(paramodulation,[status(thm)],[f21247,f31633])).
% 77.04/10.58 fof(f34363,plain,(
% 77.04/10.58 ![X0,X1]: (converse(meet(X0,X1))=meet(complement(complement(converse(X0))),converse(X1)))),
% 77.04/10.58 inference(forward_demodulation,[status(thm)],[f2135,f34261])).
% 77.04/10.58 fof(f34364,plain,(
% 77.04/10.58 ~converse(meet(sk1,sk2))=converse(meet(sk1,sk2))),
% 77.04/10.58 inference(backward_demodulation,[status(thm)],[f34405,f28])).
% 77.04/10.58 fof(f34405,plain,(
% 77.04/10.58 ![X0,X1]: (converse(meet(X0,X1))=meet(converse(X0),converse(X1)))),
% 77.04/10.58 inference(forward_demodulation,[status(thm)],[f2135,f34363])).
% 77.04/10.58 fof(f34594,plain,(
% 77.04/10.58 $false),
% 77.04/10.58 inference(trivial_equality_resolution,[status(thm)],[f34364])).
% 77.04/10.58 % SZS output end CNFRefutation for theBenchmark.p
% 25.10/10.64 % Elapsed time: 10.079593 seconds
% 25.10/10.64 % CPU time: 79.341761 seconds
% 25.10/10.64 % Total memory used: 465.385 MB
% 25.10/10.64 % Net memory used: 455.460 MB
%------------------------------------------------------------------------------