%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL047-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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:03:45 PM UTC 2026
% Result : Unsatisfiable 256.60s 32.71s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL047-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n002.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 04:11:31 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 256.60/32.71 % Refutation found
% 256.60/32.71 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 256.60/32.71 % SZS output start CNFRefutation for theBenchmark
% 256.60/32.71 fof(f1,axiom,(
% 256.60/32.71 (![A,B]: (join(A,B) = join(B,A) ))),
% 256.60/32.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 256.60/32.71 fof(f2,axiom,(
% 256.60/32.71 (![A,B,C]: (join(A,join(B,C)) = join(join(A,B),C) ))),
% 256.60/32.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 256.60/32.71 fof(f3,axiom,(
% 256.60/32.71 (![A,B]: (A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))) ))),
% 256.60/32.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 256.60/32.71 fof(f4,axiom,(
% 256.60/32.71 (![A,B]: (meet(A,B) = complement(join(complement(A),complement(B))) ))),
% 256.60/32.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 256.60/32.71 fof(f5,axiom,(
% 256.60/32.71 (![A,B,C]: (composition(A,composition(B,C)) = composition(composition(A,B),C) ))),
% 256.60/32.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 256.60/32.71 fof(f6,axiom,(
% 256.60/32.71 (![A]: (composition(A,one) = A ))),
% 256.60/32.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 256.60/32.71 fof(f8,axiom,(
% 256.60/32.71 (![A]: (converse(converse(A)) = A ))),
% 256.60/32.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 256.60/32.71 fof(f10,axiom,(
% 256.60/32.71 (![A,B]: (converse(composition(A,B)) = composition(converse(B),converse(A)) ))),
% 256.60/32.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 256.60/32.71 fof(f11,axiom,(
% 256.60/32.71 (![A,B]: (join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B) ))),
% 256.60/32.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 256.60/32.71 fof(f12,axiom,(
% 256.60/32.71 (![A]: (top = join(A,complement(A)) ))),
% 256.60/32.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 256.60/32.71 fof(f13,axiom,(
% 256.60/32.71 (![A]: (zero = meet(A,complement(A)) ))),
% 256.60/32.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 256.60/32.71 fof(f14,negated_conjecture,(
% 256.60/32.71 join(sk1,sk2) = sk2 ),
% 256.60/32.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 256.60/32.71 fof(f15,negated_conjecture,(
% 256.60/32.71 join(sk1,sk3) = sk3 ),
% 256.60/32.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 256.60/32.71 fof(f16,negated_conjecture,(
% 256.60/32.71 join(sk1,meet(sk2,sk3)) != meet(sk2,sk3) ),
% 256.60/32.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 256.60/32.71 fof(f17,plain,(
% 256.60/32.71 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 256.60/32.71 inference(cnf_transformation,[status(thm)],[f1])).
% 256.60/32.71 fof(f18,plain,(
% 256.60/32.71 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 256.60/32.71 inference(cnf_transformation,[status(thm)],[f2])).
% 256.60/32.71 fof(f19,plain,(
% 256.60/32.71 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 256.60/32.71 inference(cnf_transformation,[status(thm)],[f3])).
% 256.60/32.71 fof(f20,plain,(
% 256.60/32.71 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 256.60/32.71 inference(cnf_transformation,[status(thm)],[f4])).
% 256.60/32.71 fof(f21,plain,(
% 256.60/32.71 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 256.60/32.71 inference(cnf_transformation,[status(thm)],[f5])).
% 256.60/32.71 fof(f22,plain,(
% 256.60/32.71 ![X0]: (composition(X0,one)=X0)),
% 256.60/32.71 inference(cnf_transformation,[status(thm)],[f6])).
% 256.60/32.71 fof(f24,plain,(
% 256.60/32.71 ![X0]: (converse(converse(X0))=X0)),
% 256.60/32.71 inference(cnf_transformation,[status(thm)],[f8])).
% 256.60/32.71 fof(f26,plain,(
% 256.60/32.71 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 256.60/32.71 inference(cnf_transformation,[status(thm)],[f10])).
% 256.60/32.71 fof(f27,plain,(
% 256.60/32.71 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 256.60/32.71 inference(cnf_transformation,[status(thm)],[f11])).
% 256.60/32.71 fof(f28,plain,(
% 256.60/32.71 ![X0]: (top=join(X0,complement(X0)))),
% 256.60/32.71 inference(cnf_transformation,[status(thm)],[f12])).
% 256.60/32.71 fof(f29,plain,(
% 256.60/32.71 ![X0]: (zero=meet(X0,complement(X0)))),
% 256.60/32.71 inference(cnf_transformation,[status(thm)],[f13])).
% 256.60/32.71 fof(f30,plain,(
% 256.60/32.71 join(sk1,sk2)=sk2),
% 256.60/32.71 inference(cnf_transformation,[status(thm)],[f14])).
% 256.60/32.71 fof(f31,plain,(
% 256.60/32.71 join(sk1,sk3)=sk3),
% 256.60/32.71 inference(cnf_transformation,[status(thm)],[f15])).
% 256.60/32.71 fof(f32,plain,(
% 256.60/32.71 ~join(sk1,meet(sk2,sk3))=meet(sk2,sk3)),
% 256.60/32.71 inference(cnf_transformation,[status(thm)],[f16])).
% 256.60/32.71 fof(f33,definition,(
% 256.60/32.71 sF1_fnc=meet(sk2,sk3)),
% 256.60/32.71 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 256.60/32.71 fof(f34,definition,(
% 256.60/32.71 sF0_fnc=join(sk1,sF1_fnc)),
% 256.60/32.71 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 256.60/32.71 fof(f35,plain,(
% 256.60/32.71 ~sF0_fnc=sF1_fnc),
% 256.60/32.71 inference(definition_folding,[],[f32,f34,f33])).
% 256.60/32.71 fof(f36,plain,(
% 256.60/32.71 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f17,f19])).
% 256.60/32.71 fof(f37,plain,(
% 256.60/32.71 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 256.60/32.71 inference(backward_demodulation,[status(thm)],[f20,f36])).
% 256.60/32.71 fof(f38,plain,(
% 256.60/32.71 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f17,f27])).
% 256.60/32.71 fof(f39,plain,(
% 256.60/32.71 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f17,f37])).
% 256.60/32.71 fof(f45,plain,(
% 256.60/32.71 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f17,f18])).
% 256.60/32.71 fof(f55,plain,(
% 256.60/32.71 ![X0]: (join(sk1,join(sk3,X0))=join(sk3,X0))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f31,f18])).
% 256.60/32.71 fof(f56,plain,(
% 256.60/32.71 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f17,f20])).
% 256.60/32.71 fof(f58,plain,(
% 256.60/32.71 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X0,X1),complement(X2))))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f20,f20])).
% 256.60/32.71 fof(f61,plain,(
% 256.60/32.71 ![X0]: (join(sk1,join(sF1_fnc,X0))=join(sF0_fnc,X0))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f34,f18])).
% 256.60/32.71 fof(f63,plain,(
% 256.60/32.71 ![X0,X1]: (top=join(join(complement(X0),complement(X1)),meet(X0,X1)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f20,f28])).
% 256.60/32.71 fof(f64,plain,(
% 256.60/32.71 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f28,f20])).
% 256.60/32.71 fof(f66,plain,(
% 256.60/32.71 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f28,f18])).
% 256.60/32.71 fof(f67,plain,(
% 256.60/32.71 ![X0,X1]: (top=join(complement(X0),join(complement(X1),meet(X0,X1))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f18,f63])).
% 256.60/32.71 fof(f68,plain,(
% 256.60/32.71 zero=complement(top)),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f29,f64])).
% 256.60/32.71 fof(f76,plain,(
% 256.60/32.71 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f22,f21])).
% 256.60/32.71 fof(f91,plain,(
% 256.60/32.71 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f24,f26])).
% 256.60/32.71 fof(f129,plain,(
% 256.60/32.71 ![X0]: (join(sk1,join(X0,sk3))=join(sk3,X0))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f17,f55])).
% 256.60/32.71 fof(f156,plain,(
% 256.60/32.71 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f20,f56])).
% 256.60/32.71 fof(f169,plain,(
% 256.60/32.71 ![X0,X1,X2]: (meet(X0,join(complement(X1),complement(X2)))=complement(join(complement(X0),meet(X2,X1))))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f56,f20])).
% 256.60/32.71 fof(f211,plain,(
% 256.60/32.71 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f29,f39])).
% 256.60/32.71 fof(f214,plain,(
% 256.60/32.71 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f56,f39])).
% 256.60/32.71 fof(f215,plain,(
% 256.60/32.71 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f20,f39])).
% 256.60/32.71 fof(f217,plain,(
% 256.60/32.71 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f28,f39])).
% 256.60/32.71 fof(f224,plain,(
% 256.60/32.71 ![X0,X1,X2]: (join(meet(X0,X1),join(complement(join(complement(X0),X1)),X2))=join(X0,X2))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f39,f18])).
% 256.60/32.71 fof(f229,plain,(
% 256.60/32.71 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f56,f211])).
% 256.60/32.71 fof(f230,plain,(
% 256.60/32.71 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f17,f214])).
% 256.60/32.71 fof(f231,plain,(
% 256.60/32.71 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f17,f215])).
% 256.60/32.71 fof(f233,plain,(
% 256.60/32.71 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(X0)))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f17,f217])).
% 256.60/32.71 fof(f234,plain,(
% 256.60/32.71 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f68,f233])).
% 256.60/32.71 fof(f238,plain,(
% 256.60/32.71 top=join(zero,meet(top,complement(zero)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f68,f234])).
% 256.60/32.71 fof(f240,plain,(
% 256.60/32.71 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,meet(join(complement(X0),complement(X1)),complement(meet(X1,X0)))))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f56,f234])).
% 256.60/32.71 fof(f244,plain,(
% 256.60/32.71 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,meet(complement(meet(X1,X0)),join(complement(X0),complement(X1)))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f156,f240])).
% 256.60/32.71 fof(f252,plain,(
% 256.60/32.71 ![X0,X1]: (X0=join(meet(X1,X0),meet(complement(X1),X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f156,f230])).
% 256.60/32.71 fof(f254,plain,(
% 256.60/32.71 ![X0]: (X0=join(meet(top,X0),meet(X0,zero)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f68,f230])).
% 256.60/32.71 fof(f268,plain,(
% 256.60/32.71 ![X0]: (X0=join(meet(X0,top),meet(X0,zero)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f156,f254])).
% 256.60/32.71 fof(f271,plain,(
% 256.60/32.71 ![X0]: (X0=join(meet(top,X0),meet(zero,X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f156,f254])).
% 256.60/32.71 fof(f286,plain,(
% 256.60/32.71 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X2,X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f17,f45])).
% 256.60/32.71 fof(f302,plain,(
% 256.60/32.71 ![X0]: (join(X0,sF0_fnc)=join(sF1_fnc,join(X0,sk1)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f34,f45])).
% 256.60/32.71 fof(f308,plain,(
% 256.60/32.71 ![X0,X1]: (join(X0,top)=join(complement(X1),join(X0,X1)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f28,f45])).
% 256.60/32.71 fof(f309,plain,(
% 256.60/32.71 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X1,join(X0,X2)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f17,f45])).
% 256.60/32.71 fof(f337,plain,(
% 256.60/32.71 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X1,X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f17,f45])).
% 256.60/32.71 fof(f339,plain,(
% 256.60/32.71 ![X0,X1]: (join(sk1,join(X0,join(sF1_fnc,X1)))=join(sF0_fnc,join(X1,X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f45,f61])).
% 256.60/32.71 fof(f340,plain,(
% 256.60/32.71 ![X0,X1]: (join(sk1,join(X0,join(sk3,X1)))=join(sk3,join(X1,X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f45,f55])).
% 256.60/32.71 fof(f379,plain,(
% 256.60/32.71 ![X0]: (join(X0,sF0_fnc)=join(sk1,join(sF1_fnc,X0)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f45,f302])).
% 256.60/32.71 fof(f384,plain,(
% 256.60/32.71 ![X0,X1]: (join(X0,top)=join(X1,join(complement(X1),X0)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f45,f308])).
% 256.60/32.71 fof(f431,plain,(
% 256.60/32.71 ![X0]: (X0=join(meet(X0,top),meet(zero,X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f156,f268])).
% 256.60/32.71 fof(f440,plain,(
% 256.60/32.71 ![X0]: (X0=join(meet(zero,X0),meet(X0,top)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f17,f431])).
% 256.60/32.71 fof(f444,plain,(
% 256.60/32.71 complement(zero)=join(meet(complement(zero),top),zero)),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f29,f431])).
% 256.60/32.71 fof(f453,plain,(
% 256.60/32.71 complement(zero)=join(zero,meet(complement(zero),top))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f17,f444])).
% 256.60/32.71 fof(f454,plain,(
% 256.60/32.71 complement(zero)=join(zero,meet(top,complement(zero)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f156,f453])).
% 256.60/32.71 fof(f456,plain,(
% 256.60/32.71 complement(zero)=top),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f238,f454])).
% 256.60/32.71 fof(f459,plain,(
% 256.60/32.71 ![X0]: (zero=join(meet(zero,X0),complement(join(top,X0))))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f456,f39])).
% 256.60/32.71 fof(f603,plain,(
% 256.60/32.71 sk2=join(sF1_fnc,meet(sk2,complement(sk3)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f33,f231])).
% 256.60/32.71 fof(f608,plain,(
% 256.60/32.71 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f156,f231])).
% 256.60/32.71 fof(f634,plain,(
% 256.60/32.71 ![X0]: (complement(complement(X0))=join(meet(X0,complement(complement(X0))),zero))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f29,f252])).
% 256.60/32.71 fof(f650,plain,(
% 256.60/32.71 ![X0]: (complement(complement(X0))=join(zero,meet(X0,complement(complement(X0)))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f17,f634])).
% 256.60/32.71 fof(f656,plain,(
% 256.60/32.71 ![X0]: (complement(complement(X0))=X0)),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f234,f650])).
% 256.60/32.71 fof(f663,plain,(
% 256.60/32.71 ![X0,X1]: (meet(join(complement(X0),complement(X1)),join(complement(X0),X1))=complement(X0))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f39,f58])).
% 256.60/32.71 fof(f687,plain,(
% 256.60/32.71 ![X0,X1,X2,X3]: (meet(X0,join(meet(X1,X2),complement(X3)))=complement(join(complement(X0),meet(join(complement(X1),complement(X2)),X3))))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f58,f20])).
% 256.60/32.71 fof(f690,plain,(
% 256.60/32.71 ![X0,X1]: (meet(join(complement(X0),X1),join(complement(X0),complement(X1)))=complement(X0))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f156,f663])).
% 256.60/32.71 fof(f707,plain,(
% 256.60/32.71 ![X0,X1,X2,X3]: (meet(X0,join(meet(X1,X2),complement(X3)))=meet(X0,join(complement(X3),complement(join(complement(X1),complement(X2))))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f169,f687])).
% 256.60/32.71 fof(f708,plain,(
% 256.60/32.71 ![X0,X1,X2,X3]: (meet(X0,join(meet(X1,X2),complement(X3)))=meet(X0,join(complement(X3),meet(X2,X1))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f56,f707])).
% 256.60/32.71 fof(f716,plain,(
% 256.60/32.71 ![X0,X1]: (complement(meet(X0,X1))=join(complement(X1),complement(X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f56,f656])).
% 256.60/32.71 fof(f717,plain,(
% 256.60/32.71 ![X0,X1]: (complement(meet(X0,X1))=join(complement(X0),complement(X1)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f20,f656])).
% 256.60/32.71 fof(f718,plain,(
% 256.60/32.71 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),complement(X2))=complement(join(meet(X0,X1),X2)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f656,f58])).
% 256.60/32.71 fof(f724,plain,(
% 256.60/32.71 ![X0,X1]: (meet(complement(X0),X1)=complement(join(complement(X1),X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f656,f56])).
% 256.60/32.71 fof(f759,plain,(
% 256.60/32.71 ![X0,X1]: (meet(join(complement(X0),X1),complement(meet(X1,X0)))=complement(X0))),
% 256.60/32.71 inference(backward_demodulation,[status(thm)],[f716,f690])).
% 256.60/32.71 fof(f767,plain,(
% 256.60/32.71 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,meet(complement(meet(X1,X0)),complement(meet(X1,X0)))))),
% 256.60/32.71 inference(backward_demodulation,[status(thm)],[f716,f244])).
% 256.60/32.71 fof(f783,plain,(
% 256.60/32.71 ![X0,X1,X2]: (meet(complement(meet(X0,X1)),complement(X2))=complement(join(meet(X0,X1),X2)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f717,f718])).
% 256.60/32.71 fof(f793,plain,(
% 256.60/32.71 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(complement(X1),X0),X2))=join(X0,X2))),
% 256.60/32.71 inference(backward_demodulation,[status(thm)],[f724,f224])).
% 256.60/32.71 fof(f819,plain,(
% 256.60/32.71 ![X0,X1]: (meet(complement(meet(X0,X1)),join(complement(X1),X0))=complement(X1))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f156,f759])).
% 256.60/32.71 fof(f824,plain,(
% 256.60/32.71 ![X0,X1]: (complement(meet(X0,X1))=join(zero,meet(complement(meet(X1,X0)),complement(meet(X1,X0)))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f717,f767])).
% 256.60/32.71 fof(f825,plain,(
% 256.60/32.71 ![X0,X1]: (complement(meet(X0,X1))=complement(meet(X1,X0)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f229,f824])).
% 256.60/32.71 fof(f885,plain,(
% 256.60/32.71 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f22,f91])).
% 256.60/32.71 fof(f900,plain,(
% 256.60/32.71 ![X0]: (X0=composition(converse(one),X0))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f24,f885])).
% 256.60/32.71 fof(f1052,plain,(
% 256.60/32.71 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f76,f900])).
% 256.60/32.71 fof(f1054,plain,(
% 256.60/32.71 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f900,f38])).
% 256.60/32.71 fof(f1067,plain,(
% 256.60/32.71 ![X0]: (composition(one,X0)=X0)),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f900,f1052])).
% 256.60/32.71 fof(f1069,plain,(
% 256.60/32.71 ![X0]: (complement(meet(X0,composition(one,X0)))=complement(X0))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f717,f1054])).
% 256.60/32.71 fof(f1070,plain,(
% 256.60/32.71 ![X0]: (complement(meet(X0,X0))=complement(X0))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f1067,f1069])).
% 256.60/32.71 fof(f1110,plain,(
% 256.60/32.71 ![X0]: (complement(complement(X0))=meet(X0,X0))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f1070,f656])).
% 256.60/32.71 fof(f1118,plain,(
% 256.60/32.71 ![X0]: (X0=join(zero,X0))),
% 256.60/32.71 inference(backward_demodulation,[status(thm)],[f1122,f229])).
% 256.60/32.71 fof(f1122,plain,(
% 256.60/32.71 ![X0]: (X0=meet(X0,X0))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f656,f1110])).
% 256.60/32.71 fof(f1218,plain,(
% 256.60/32.71 ![X0]: (top=join(complement(X0),join(complement(X0),X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f1122,f67])).
% 256.60/32.71 fof(f1219,plain,(
% 256.60/32.71 ![X0]: (X0=join(X0,meet(complement(X0),X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f1122,f252])).
% 256.60/32.71 fof(f1256,plain,(
% 256.60/32.71 ![X0]: (top=join(complement(X0),join(X0,complement(X0))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f45,f1218])).
% 256.60/32.71 fof(f1257,plain,(
% 256.60/32.71 ![X0]: (top=join(X0,join(complement(X0),complement(X0))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f45,f1256])).
% 256.60/32.71 fof(f1258,plain,(
% 256.60/32.71 ![X0]: (top=join(complement(X0),top))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f384,f1257])).
% 256.60/32.71 fof(f1259,plain,(
% 256.60/32.71 ![X0]: (top=join(top,complement(X0)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f17,f1258])).
% 256.60/32.71 fof(f1260,plain,(
% 256.60/32.71 ![X0]: (X0=join(X0,meet(X0,complement(X0))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f156,f1219])).
% 256.60/32.71 fof(f1263,plain,(
% 256.60/32.71 ![X0]: (X0=join(X0,zero))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f29,f1260])).
% 256.60/32.71 fof(f1320,plain,(
% 256.60/32.71 ![X0]: (top=join(top,X0))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f656,f1259])).
% 256.60/32.71 fof(f1345,plain,(
% 256.60/32.71 ![X0]: (zero=join(meet(zero,X0),complement(top)))),
% 256.60/32.71 inference(backward_demodulation,[status(thm)],[f1320,f459])).
% 256.60/32.71 fof(f1347,plain,(
% 256.60/32.71 ![X0,X1]: (join(X0,join(complement(X0),X1))=top)),
% 256.60/32.71 inference(backward_demodulation,[status(thm)],[f1320,f66])).
% 256.60/32.71 fof(f1361,plain,(
% 256.60/32.71 ![X0]: (zero=join(complement(top),meet(zero,X0)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f17,f1345])).
% 256.60/32.71 fof(f1362,plain,(
% 256.60/32.71 ![X0]: (zero=join(zero,meet(zero,X0)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f68,f1361])).
% 256.60/32.71 fof(f1363,plain,(
% 256.60/32.71 ![X0]: (X0=join(meet(top,X0),zero))),
% 256.60/32.71 inference(backward_demodulation,[status(thm)],[f1376,f271])).
% 256.60/32.71 fof(f1364,plain,(
% 256.60/32.71 ![X0]: (X0=join(zero,meet(X0,top)))),
% 256.60/32.71 inference(backward_demodulation,[status(thm)],[f1376,f440])).
% 256.60/32.71 fof(f1376,plain,(
% 256.60/32.71 ![X0]: (zero=meet(zero,X0))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f1118,f1362])).
% 256.60/32.71 fof(f1390,plain,(
% 256.60/32.71 ![X0]: (X0=meet(top,X0))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f1263,f1363])).
% 256.60/32.71 fof(f1397,plain,(
% 256.60/32.71 ![X0]: (X0=meet(X0,top))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f1118,f1364])).
% 256.60/32.71 fof(f2881,plain,(
% 256.60/32.71 join(sF0_fnc,sk3)=join(sk3,sF1_fnc)),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f61,f129])).
% 256.60/32.71 fof(f2903,plain,(
% 256.60/32.71 join(sk3,sF0_fnc)=join(sk3,sF1_fnc)),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f17,f2881])).
% 256.60/32.71 fof(f3635,plain,(
% 256.60/32.71 join(meet(sk2,complement(sk3)),sF0_fnc)=join(sk1,sk2)),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f603,f379])).
% 256.60/32.71 fof(f3643,plain,(
% 256.60/32.71 join(sF0_fnc,meet(sk2,complement(sk3)))=join(sk1,sk2)),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f17,f3635])).
% 256.60/32.71 fof(f3644,plain,(
% 256.60/32.71 join(sF0_fnc,meet(sk2,complement(sk3)))=sk2),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f30,f3643])).
% 256.60/32.71 fof(f3702,plain,(
% 256.60/32.71 ![X0,X1]: (complement(meet(X0,complement(X1)))=join(X1,complement(X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f656,f716])).
% 256.60/32.71 fof(f3714,plain,(
% 256.60/32.71 ![X0,X1]: (join(X0,complement(meet(X1,X0)))=top)),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f716,f1347])).
% 256.60/32.71 fof(f4113,plain,(
% 256.60/32.71 ![X0,X1]: (complement(meet(meet(X0,complement(X1)),X1))=top)),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f716,f3714])).
% 256.60/32.71 fof(f4160,plain,(
% 256.60/32.71 ![X0,X1]: (complement(meet(X0,meet(X1,complement(X0))))=top)),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f825,f4113])).
% 256.60/32.71 fof(f4878,plain,(
% 256.60/32.71 ![X0,X1]: (complement(top)=meet(X0,meet(X1,complement(X0))))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f4160,f656])).
% 256.60/32.71 fof(f4912,plain,(
% 256.60/32.71 ![X0,X1]: (zero=meet(X0,meet(X1,complement(X0))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f68,f4878])).
% 256.60/32.71 fof(f4941,plain,(
% 256.60/32.71 ![X0,X1]: (zero=meet(complement(X0),meet(X1,X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f656,f4912])).
% 256.60/32.71 fof(f4956,plain,(
% 256.60/32.71 ![X0,X1]: (X0=join(zero,meet(complement(meet(X1,complement(X0))),X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f4912,f608])).
% 256.60/32.71 fof(f4981,plain,(
% 256.60/32.71 ![X0,X1]: (X0=meet(complement(meet(X1,complement(X0))),X0))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f1118,f4956])).
% 256.60/32.71 fof(f4982,plain,(
% 256.60/32.71 ![X0,X1]: (X0=meet(X0,complement(meet(X1,complement(X0)))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f156,f4981])).
% 256.60/32.71 fof(f4983,plain,(
% 256.60/32.71 ![X0,X1]: (X0=meet(X0,join(X0,complement(X1))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f3702,f4982])).
% 256.60/32.71 fof(f4997,plain,(
% 256.60/32.71 zero=meet(complement(sk3),sF1_fnc)),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f33,f4941])).
% 256.60/32.71 fof(f5003,plain,(
% 256.60/32.71 ![X0,X1]: (zero=meet(complement(X0),meet(X0,X1)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f156,f4941])).
% 256.60/32.71 fof(f5015,plain,(
% 256.60/32.71 zero=meet(sF1_fnc,complement(sk3))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f156,f4997])).
% 256.60/32.71 fof(f5043,plain,(
% 256.60/32.71 complement(sk3)=join(zero,meet(complement(sF1_fnc),complement(sk3)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f5015,f252])).
% 256.60/32.71 fof(f5059,plain,(
% 256.60/32.71 complement(sk3)=meet(complement(sF1_fnc),complement(sk3))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f1118,f5043])).
% 256.60/32.71 fof(f5060,plain,(
% 256.60/32.71 complement(sk3)=meet(complement(sk3),complement(sF1_fnc))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f156,f5059])).
% 256.60/32.71 fof(f5278,plain,(
% 256.60/32.71 ![X0,X1]: (complement(X0)=join(zero,meet(complement(meet(X0,X1)),complement(X0))))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f5003,f608])).
% 256.60/32.71 fof(f5298,plain,(
% 256.60/32.71 ![X0,X1]: (complement(X0)=meet(complement(meet(X0,X1)),complement(X0)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f1118,f5278])).
% 256.60/32.71 fof(f5299,plain,(
% 256.60/32.71 ![X0,X1]: (complement(X0)=meet(complement(X0),complement(meet(X0,X1))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f156,f5298])).
% 256.60/32.71 fof(f6025,plain,(
% 256.60/32.71 ![X0,X1]: (X0=meet(X0,join(X0,X1)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f656,f4983])).
% 256.60/32.71 fof(f7299,plain,(
% 256.60/32.71 ![X0]: (sk1=meet(sk1,join(sk3,X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f55,f6025])).
% 256.60/32.71 fof(f7923,plain,(
% 256.60/32.71 ![X0,X1]: (join(meet(X0,X1),X0)=join(X0,meet(complement(complement(X1)),X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f252,f793])).
% 256.60/32.71 fof(f8056,plain,(
% 256.60/32.71 ![X0,X1]: (join(X0,meet(X0,X1))=join(X0,meet(complement(complement(X1)),X0)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f17,f7923])).
% 256.60/32.71 fof(f8057,plain,(
% 256.60/32.71 ![X0,X1]: (join(X0,meet(X0,X1))=join(X0,meet(X1,X0)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f656,f8056])).
% 256.60/32.71 fof(f8838,plain,(
% 256.60/32.71 ![X0]: (zero=meet(complement(join(sk3,X0)),sk1))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f7299,f4941])).
% 256.60/32.71 fof(f8872,plain,(
% 256.60/32.71 ![X0]: (zero=meet(sk1,complement(join(sk3,X0))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f156,f8838])).
% 256.60/32.71 fof(f11325,plain,(
% 256.60/32.71 ![X0]: (complement(join(sk3,X0))=join(zero,meet(complement(sk1),complement(join(sk3,X0)))))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f8872,f252])).
% 256.60/32.71 fof(f11411,plain,(
% 256.60/32.71 ![X0]: (complement(join(sk3,X0))=meet(complement(sk1),complement(join(sk3,X0))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f1118,f11325])).
% 256.60/32.71 fof(f17099,plain,(
% 256.60/32.71 ![X0,X1]: (complement(meet(X0,complement(X1)))=join(complement(X0),X1))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f656,f717])).
% 256.60/32.71 fof(f17201,plain,(
% 256.60/32.71 ![X0,X1]: (meet(complement(X0),complement(X1))=complement(join(X1,X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f656,f724])).
% 256.60/32.71 fof(f17295,plain,(
% 256.60/32.71 ![X0]: (complement(join(sk3,X0))=complement(join(join(sk3,X0),sk1)))),
% 256.60/32.71 inference(backward_demodulation,[status(thm)],[f17201,f11411])).
% 256.60/32.71 fof(f17305,plain,(
% 256.60/32.71 complement(sk3)=complement(join(sF1_fnc,sk3))),
% 256.60/32.71 inference(backward_demodulation,[status(thm)],[f17201,f5060])).
% 256.60/32.71 fof(f17306,plain,(
% 256.60/32.71 ![X0,X1,X2]: (complement(join(X0,meet(X1,X2)))=complement(join(meet(X1,X2),X0)))),
% 256.60/32.71 inference(backward_demodulation,[status(thm)],[f17201,f783])).
% 256.60/32.71 fof(f17314,plain,(
% 256.60/32.71 ![X0,X1]: (complement(X0)=complement(join(meet(X0,X1),X0)))),
% 256.60/32.71 inference(backward_demodulation,[status(thm)],[f17201,f5299])).
% 256.60/32.71 fof(f17373,plain,(
% 256.60/32.71 ![X0]: (complement(join(sk3,X0))=complement(join(X0,join(sk1,sk3))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f286,f17295])).
% 256.60/32.71 fof(f17374,plain,(
% 256.60/32.71 ![X0]: (complement(join(sk3,X0))=complement(join(X0,sk3)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f31,f17373])).
% 256.60/32.71 fof(f17388,plain,(
% 256.60/32.71 complement(sk3)=complement(join(sk3,sF1_fnc))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f17374,f17305])).
% 256.60/32.71 fof(f17389,plain,(
% 256.60/32.71 complement(sk3)=complement(join(sk3,sF0_fnc))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f2903,f17388])).
% 256.60/32.71 fof(f17394,plain,(
% 256.60/32.71 ![X0,X1]: (complement(X0)=complement(join(X0,meet(X0,X1))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f17306,f17314])).
% 256.60/32.71 fof(f20255,plain,(
% 256.60/32.71 complement(complement(sk3))=join(sk3,sF0_fnc)),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f17389,f656])).
% 256.60/32.71 fof(f20282,plain,(
% 256.60/32.71 sk3=join(sk3,sF1_fnc)),
% 256.60/32.71 inference(backward_demodulation,[status(thm)],[f20301,f2903])).
% 256.60/32.71 fof(f20301,plain,(
% 256.60/32.71 sk3=join(sk3,sF0_fnc)),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f656,f20255])).
% 256.60/32.71 fof(f20346,plain,(
% 256.60/32.71 ![X0]: (join(sk3,X0)=join(sF1_fnc,join(X0,sk3)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f20282,f286])).
% 256.60/32.71 fof(f20367,plain,(
% 256.60/32.71 ![X0]: (join(sk3,X0)=join(sk3,join(sF1_fnc,X0)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f45,f20346])).
% 256.60/32.71 fof(f22254,plain,(
% 256.60/32.71 ![X0]: (join(sk3,X0)=join(sF0_fnc,join(X0,sk3)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f20301,f286])).
% 256.60/32.71 fof(f22276,plain,(
% 256.60/32.71 ![X0]: (join(sk3,X0)=join(sk3,join(sF0_fnc,X0)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f45,f22254])).
% 256.60/32.71 fof(f26447,plain,(
% 256.60/32.71 ![X0]: (join(sk3,join(sF1_fnc,X0))=join(sF0_fnc,join(X0,sk3)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f55,f339])).
% 256.60/32.71 fof(f26598,plain,(
% 256.60/32.71 ![X0]: (join(sk3,X0)=join(sF0_fnc,join(X0,sk3)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f20367,f26447])).
% 256.60/32.71 fof(f26599,plain,(
% 256.60/32.71 ![X0]: (join(sk3,X0)=join(sk3,join(X0,sF0_fnc)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f337,f26598])).
% 256.60/32.71 fof(f27548,plain,(
% 256.60/32.71 ![X0]: (join(sF0_fnc,join(sk3,X0))=join(sk3,join(X0,sF1_fnc)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f61,f340])).
% 256.60/32.71 fof(f27714,plain,(
% 256.60/32.71 ![X0]: (join(sk3,join(sF0_fnc,X0))=join(sk3,join(X0,sF1_fnc)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f309,f27548])).
% 256.60/32.71 fof(f27715,plain,(
% 256.60/32.71 ![X0]: (join(sk3,X0)=join(sk3,join(X0,sF1_fnc)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f22276,f27714])).
% 256.60/32.71 fof(f28244,plain,(
% 256.60/32.71 ![X0,X1]: (complement(complement(X0))=join(X0,meet(X0,X1)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f17394,f656])).
% 256.60/32.71 fof(f28325,plain,(
% 256.60/32.71 ![X0,X1]: (X0=join(X0,meet(X1,X0)))),
% 256.60/32.71 inference(backward_demodulation,[status(thm)],[f28326,f8057])).
% 256.60/32.71 fof(f28326,plain,(
% 256.60/32.71 ![X0,X1]: (X0=join(X0,meet(X0,X1)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f656,f28244])).
% 256.60/32.71 fof(f28965,plain,(
% 256.60/32.71 ![X0,X1,X2]: (join(X0,X1)=join(meet(X0,X2),join(X1,X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f28326,f286])).
% 256.60/32.71 fof(f29022,plain,(
% 256.60/32.71 ![X0,X1,X2]: (join(X0,X1)=join(X0,join(X1,meet(X0,X2))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f337,f28965])).
% 256.60/32.71 fof(f29785,plain,(
% 256.60/32.71 ![X0,X1,X2]: (join(X0,X1)=join(meet(X2,X0),join(X1,X0)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f28325,f286])).
% 256.60/32.71 fof(f29883,plain,(
% 256.60/32.71 ![X0,X1,X2]: (join(X0,X1)=join(X0,join(X1,meet(X2,X0))))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f337,f29785])).
% 256.60/32.71 fof(f55625,plain,(
% 256.60/32.71 ![X0,X1,X2]: (meet(X0,join(X1,complement(X2)))=meet(X0,join(complement(X2),meet(X1,top))))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f1390,f708])).
% 256.60/32.71 fof(f55655,plain,(
% 256.60/32.71 ![X0,X1,X2,X3,X4]: (meet(X0,join(meet(X1,X2),complement(meet(X3,X4))))=meet(X0,join(complement(meet(X4,X3)),meet(X2,X1))))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f825,f708])).
% 256.60/32.71 fof(f56246,plain,(
% 256.60/32.71 ![X0,X1,X2]: (meet(X0,join(X1,complement(X2)))=meet(X0,join(complement(X2),X1)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f1397,f55625])).
% 256.60/32.71 fof(f71555,plain,(
% 256.60/32.71 ![X0,X1]: (meet(complement(meet(X0,complement(X1))),join(X1,X0))=complement(complement(X1)))),
% 256.60/32.71 inference(paramodulation,[status(thm)],[f656,f819])).
% 256.60/32.71 fof(f72164,plain,(
% 256.60/32.71 ![X0,X1]: (meet(join(X0,X1),complement(meet(X1,complement(X0))))=complement(complement(X0)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f156,f71555])).
% 256.60/32.71 fof(f72165,plain,(
% 256.60/32.71 ![X0,X1]: (meet(join(X0,X1),join(complement(X1),X0))=complement(complement(X0)))),
% 256.60/32.71 inference(forward_demodulation,[status(thm)],[f17099,f72164])).
% 256.60/32.71 fof(f72167,plain,(
% 256.60/32.71 ![X0,X1]: (meet(join(X0,X1),join(complement(X1),X0))=X0)),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f656,f72165])).
% 194.26/33.01 fof(f72442,plain,(
% 194.26/33.01 meet(sk2,join(complement(meet(sk2,complement(sk3))),sF1_fnc))=sF1_fnc),
% 194.26/33.01 inference(paramodulation,[status(thm)],[f603,f72167])).
% 194.26/33.01 fof(f72499,plain,(
% 194.26/33.01 ![X0,X1]: (meet(X0,join(complement(meet(complement(X1),X0)),meet(X0,X1)))=meet(X0,X1))),
% 194.26/33.01 inference(paramodulation,[status(thm)],[f608,f72167])).
% 194.26/33.01 fof(f72500,plain,(
% 194.26/33.01 ![X0,X1]: (meet(X0,join(complement(meet(complement(X1),X0)),meet(X1,X0)))=meet(X1,X0))),
% 194.26/33.01 inference(paramodulation,[status(thm)],[f252,f72167])).
% 194.26/33.01 fof(f72504,plain,(
% 194.26/33.01 meet(sk2,join(complement(meet(sk2,complement(sk3))),sF0_fnc))=sF0_fnc),
% 194.26/33.01 inference(paramodulation,[status(thm)],[f3644,f72167])).
% 194.26/33.01 fof(f72723,plain,(
% 194.26/33.01 meet(sk2,join(sF1_fnc,complement(meet(sk2,complement(sk3)))))=sF1_fnc),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f56246,f72442])).
% 194.26/33.01 fof(f72724,plain,(
% 194.26/33.01 meet(sk2,join(sF1_fnc,join(complement(sk2),sk3)))=sF1_fnc),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f17099,f72723])).
% 194.26/33.01 fof(f72725,plain,(
% 194.26/33.01 meet(sk2,join(sk3,join(complement(sk2),sF1_fnc)))=sF1_fnc),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f337,f72724])).
% 194.26/33.01 fof(f72726,plain,(
% 194.26/33.01 meet(sk2,join(sk3,complement(sk2)))=sF1_fnc),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f27715,f72725])).
% 194.26/33.01 fof(f72839,plain,(
% 194.26/33.01 ![X0,X1]: (meet(X0,join(meet(X1,X0),complement(meet(X0,complement(X1)))))=meet(X0,X1))),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f55655,f72499])).
% 194.26/33.01 fof(f72840,plain,(
% 194.26/33.01 ![X0,X1]: (meet(X0,join(meet(X1,X0),join(complement(X0),X1)))=meet(X0,X1))),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f17099,f72839])).
% 194.26/33.01 fof(f72841,plain,(
% 194.26/33.01 ![X0,X1]: (meet(X0,join(X1,join(complement(X0),meet(X1,X0))))=meet(X0,X1))),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f337,f72840])).
% 194.26/33.01 fof(f72842,plain,(
% 194.26/33.01 meet(sk2,sk3)=sF1_fnc),
% 194.26/33.01 inference(backward_demodulation,[status(thm)],[f72850,f72726])).
% 194.26/33.01 fof(f72850,plain,(
% 194.26/33.01 ![X0,X1]: (meet(X0,join(X1,complement(X0)))=meet(X0,X1))),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f29022,f72841])).
% 194.26/33.01 fof(f72851,plain,(
% 194.26/33.01 ![X0,X1]: (meet(X0,join(meet(X0,X1),complement(meet(X0,complement(X1)))))=meet(X1,X0))),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f55655,f72500])).
% 194.26/33.01 fof(f72852,plain,(
% 194.26/33.01 ![X0,X1]: (meet(X0,join(meet(X0,X1),join(complement(X0),X1)))=meet(X1,X0))),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f17099,f72851])).
% 194.26/33.01 fof(f72853,plain,(
% 194.26/33.01 ![X0,X1]: (meet(X0,join(X1,join(complement(X0),meet(X0,X1))))=meet(X1,X0))),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f337,f72852])).
% 194.26/33.01 fof(f72854,plain,(
% 194.26/33.01 ![X0,X1]: (meet(X0,join(X1,complement(X0)))=meet(X1,X0))),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f29883,f72853])).
% 194.26/33.01 fof(f72871,plain,(
% 194.26/33.01 meet(sk2,join(sF0_fnc,complement(meet(sk2,complement(sk3)))))=sF0_fnc),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f56246,f72504])).
% 194.26/33.01 fof(f72872,plain,(
% 194.26/33.01 meet(sk2,join(sF0_fnc,join(complement(sk2),sk3)))=sF0_fnc),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f17099,f72871])).
% 194.26/33.01 fof(f72873,plain,(
% 194.26/33.01 meet(sk2,join(sk3,join(complement(sk2),sF0_fnc)))=sF0_fnc),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f337,f72872])).
% 194.26/33.01 fof(f72874,plain,(
% 194.26/33.01 meet(sk2,join(sk3,complement(sk2)))=sF0_fnc),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f26599,f72873])).
% 194.26/33.01 fof(f72875,plain,(
% 194.26/33.01 meet(sk3,sk2)=sF0_fnc),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f72854,f72874])).
% 194.26/33.01 fof(f72877,plain,(
% 194.26/33.01 meet(sk2,sk3)=sF0_fnc),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f156,f72875])).
% 194.26/33.01 fof(f73174,plain,(
% 194.26/33.01 sF0_fnc=sF1_fnc),
% 194.26/33.01 inference(forward_demodulation,[status(thm)],[f72877,f72842])).
% 194.26/33.01 fof(f73175,plain,(
% 194.26/33.01 $false),
% 194.26/33.01 inference(forward_subsumption_resolution,[status(thm)],[f73174,f35])).
% 194.26/33.01 % SZS output end CNFRefutation for theBenchmark.p
% 194.26/33.01 % Elapsed time: 32.627249 seconds
% 194.26/33.01 % CPU time: 258.693064 seconds
% 194.26/33.01 % Total memory used: 1.100 GB
% 194.26/33.01 % Net memory used: 1.068 GB
%------------------------------------------------------------------------------