%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL034-2 : 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 : n010.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:42 PM UTC 2026
% Result : Unsatisfiable 219.30s 28.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL034-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n010.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 04:05:24 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.47 % Drodi V4.1.1
% 219.30/28.32 % Refutation found
% 219.30/28.32 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 219.30/28.32 % SZS output start CNFRefutation for theBenchmark
% 219.30/28.32 fof(f1,axiom,(
% 219.30/28.32 (![A,B]: (join(A,B) = join(B,A) ))),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f2,axiom,(
% 219.30/28.32 (![A,B,C]: (join(A,join(B,C)) = join(join(A,B),C) ))),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f3,axiom,(
% 219.30/28.32 (![A,B]: (A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))) ))),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f4,axiom,(
% 219.30/28.32 (![A,B]: (meet(A,B) = complement(join(complement(A),complement(B))) ))),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f5,axiom,(
% 219.30/28.32 (![A,B,C]: (composition(A,composition(B,C)) = composition(composition(A,B),C) ))),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f6,axiom,(
% 219.30/28.32 (![A]: (composition(A,one) = A ))),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f7,axiom,(
% 219.30/28.32 (![A,B,C]: (composition(join(A,B),C) = join(composition(A,C),composition(B,C)) ))),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f8,axiom,(
% 219.30/28.32 (![A]: (converse(converse(A)) = A ))),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f9,axiom,(
% 219.30/28.32 (![A,B]: (converse(join(A,B)) = join(converse(A),converse(B)) ))),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f10,axiom,(
% 219.30/28.32 (![A,B]: (converse(composition(A,B)) = composition(converse(B),converse(A)) ))),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f11,axiom,(
% 219.30/28.32 (![A,B]: (join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B) ))),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f12,axiom,(
% 219.30/28.32 (![A]: (top = join(A,complement(A)) ))),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f13,axiom,(
% 219.30/28.32 (![A]: (zero = meet(A,complement(A)) ))),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f14,axiom,(
% 219.30/28.32 (![A,B,C]: (join(meet(composition(A,B),C),composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C)))) = composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C))) ))),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f15,axiom,(
% 219.30/28.32 (![A,B,C]: (join(meet(composition(A,B),C),meet(composition(A,meet(B,composition(converse(A),C))),C)) = meet(composition(A,meet(B,composition(converse(A),C))),C) ))),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f16,axiom,(
% 219.30/28.32 (![A,B,C]: (join(meet(composition(A,B),C),meet(composition(meet(A,composition(C,converse(B))),B),C)) = meet(composition(meet(A,composition(C,converse(B))),B),C) ))),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f17,negated_conjecture,(
% 219.30/28.32 composition(sk1,top) = sk1 ),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f18,negated_conjecture,(
% 219.30/28.32 join(composition(sk2,meet(sk1,sk3)),composition(meet(sk2,converse(sk1)),meet(sk1,sk3))) != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)) ),
% 219.30/28.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.30/28.32 fof(f19,plain,(
% 219.30/28.32 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f1])).
% 219.30/28.32 fof(f20,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f2])).
% 219.30/28.32 fof(f21,plain,(
% 219.30/28.32 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f3])).
% 219.30/28.32 fof(f22,plain,(
% 219.30/28.32 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f4])).
% 219.30/28.32 fof(f23,plain,(
% 219.30/28.32 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f5])).
% 219.30/28.32 fof(f24,plain,(
% 219.30/28.32 ![X0]: (composition(X0,one)=X0)),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f6])).
% 219.30/28.32 fof(f25,plain,(
% 219.30/28.32 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f7])).
% 219.30/28.32 fof(f26,plain,(
% 219.30/28.32 ![X0]: (converse(converse(X0))=X0)),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f8])).
% 219.30/28.32 fof(f27,plain,(
% 219.30/28.32 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f9])).
% 219.30/28.32 fof(f28,plain,(
% 219.30/28.32 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f10])).
% 219.30/28.32 fof(f29,plain,(
% 219.30/28.32 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f11])).
% 219.30/28.32 fof(f30,plain,(
% 219.30/28.32 ![X0]: (top=join(X0,complement(X0)))),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f12])).
% 219.30/28.32 fof(f31,plain,(
% 219.30/28.32 ![X0]: (zero=meet(X0,complement(X0)))),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f13])).
% 219.30/28.32 fof(f32,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))))=composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))))),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f14])).
% 219.30/28.32 fof(f33,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2))=meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2))),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f15])).
% 219.30/28.32 fof(f34,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2))=meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2))),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f16])).
% 219.30/28.32 fof(f35,plain,(
% 219.30/28.32 composition(sk1,top)=sk1),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f17])).
% 219.30/28.32 fof(f36,plain,(
% 219.30/28.32 ~join(composition(sk2,meet(sk1,sk3)),composition(meet(sk2,converse(sk1)),meet(sk1,sk3)))=composition(meet(sk2,converse(sk1)),meet(sk1,sk3))),
% 219.30/28.32 inference(cnf_transformation,[status(thm)],[f18])).
% 219.30/28.32 fof(f37,definition,(
% 219.30/28.32 sF2_fnc=meet(sk1,sk3)),
% 219.30/28.32 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 219.30/28.32 fof(f38,definition,(
% 219.30/28.32 sF1_fnc=composition(sk2,sF2_fnc)),
% 219.30/28.32 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 219.30/28.32 fof(f39,definition,(
% 219.30/28.32 sF5_fnc=converse(sk1)),
% 219.30/28.32 introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition])).
% 219.30/28.32 fof(f40,definition,(
% 219.30/28.32 sF4_fnc=meet(sk2,sF5_fnc)),
% 219.30/28.32 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 219.30/28.32 fof(f41,definition,(
% 219.30/28.32 sF3_fnc=composition(sF4_fnc,sF2_fnc)),
% 219.30/28.32 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 219.30/28.32 fof(f42,definition,(
% 219.30/28.32 sF0_fnc=join(sF1_fnc,sF3_fnc)),
% 219.30/28.32 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 219.30/28.32 fof(f43,definition,(
% 219.30/28.32 sF7_fnc=meet(sk2,sF5_fnc)),
% 219.30/28.32 introduced(definition,[new_symbols(definition,[sF7_fnc])],[function_definition])).
% 219.30/28.32 fof(f44,definition,(
% 219.30/28.32 sF6_fnc=composition(sF7_fnc,sF2_fnc)),
% 219.30/28.32 introduced(definition,[new_symbols(definition,[sF6_fnc])],[function_definition])).
% 219.30/28.32 fof(f45,plain,(
% 219.30/28.32 ~sF0_fnc=sF6_fnc),
% 219.30/28.32 inference(definition_folding,[],[f36,f44,f43,f42,f41,f40,f39,f38,f37])).
% 219.30/28.32 fof(f46,plain,(
% 219.30/28.32 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f19,f21])).
% 219.30/28.32 fof(f47,plain,(
% 219.30/28.32 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 219.30/28.32 inference(backward_demodulation,[status(thm)],[f22,f46])).
% 219.30/28.32 fof(f48,plain,(
% 219.30/28.32 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f19,f29])).
% 219.30/28.32 fof(f49,plain,(
% 219.30/28.32 sF7_fnc=sF4_fnc),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f40,f43])).
% 219.30/28.32 fof(f50,plain,(
% 219.30/28.32 sF6_fnc=composition(sF4_fnc,sF2_fnc)),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f49,f44])).
% 219.30/28.32 fof(f51,plain,(
% 219.30/28.32 sF6_fnc=sF3_fnc),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f41,f50])).
% 219.30/28.32 fof(f52,plain,(
% 219.30/28.32 ~sF0_fnc=sF3_fnc),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f51,f45])).
% 219.30/28.32 fof(f53,plain,(
% 219.30/28.32 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f19,f47])).
% 219.30/28.32 fof(f55,plain,(
% 219.30/28.32 converse(sF5_fnc)=sk1),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f39,f26])).
% 219.30/28.32 fof(f62,plain,(
% 219.30/28.32 ![X0]: (composition(sF4_fnc,composition(sF2_fnc,X0))=composition(sF3_fnc,X0))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f41,f23])).
% 219.30/28.32 fof(f63,plain,(
% 219.30/28.32 ![X0]: (composition(sk2,composition(sF2_fnc,X0))=composition(sF1_fnc,X0))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f38,f23])).
% 219.30/28.32 fof(f80,plain,(
% 219.30/28.32 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f26,f28])).
% 219.30/28.32 fof(f83,plain,(
% 219.30/28.32 ![X0,X1]: (join(X0,join(X1,complement(join(X0,X1))))=top)),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f30,f20])).
% 219.30/28.32 fof(f84,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f19,f20])).
% 219.30/28.32 fof(f88,plain,(
% 219.30/28.32 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f30,f20])).
% 219.30/28.32 fof(f89,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X0),X2))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f19,f20])).
% 219.30/28.32 fof(f96,plain,(
% 219.30/28.32 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X1,X2),composition(X0,X2)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f19,f25])).
% 219.30/28.32 fof(f103,plain,(
% 219.30/28.32 ![X0]: (composition(join(sk2,X0),sF2_fnc)=join(sF1_fnc,composition(X0,sF2_fnc)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f38,f25])).
% 219.30/28.32 fof(f105,plain,(
% 219.30/28.32 ![X0]: (composition(join(sk1,X0),top)=join(sk1,composition(X0,top)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f35,f25])).
% 219.30/28.32 fof(f107,plain,(
% 219.30/28.32 ![X0,X1,X2,X3]: (composition(join(X0,composition(X1,X2)),X3)=join(composition(X0,X3),composition(X1,composition(X2,X3))))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f23,f25])).
% 219.30/28.32 fof(f108,plain,(
% 219.30/28.32 ![X0,X1]: (composition(join(X0,sF4_fnc),composition(sF2_fnc,X1))=join(composition(X0,composition(sF2_fnc,X1)),composition(sF3_fnc,X1)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f62,f25])).
% 219.30/28.32 fof(f114,plain,(
% 219.30/28.32 ![X0,X1,X2,X3]: (join(composition(X0,X1),join(composition(X2,X1),X3))=join(composition(join(X0,X2),X1),X3))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f25,f20])).
% 219.30/28.32 fof(f120,plain,(
% 219.30/28.32 ![X0,X1]: (composition(join(X0,sF4_fnc),composition(sF2_fnc,X1))=join(composition(sF3_fnc,X1),composition(X0,composition(sF2_fnc,X1))))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f19,f108])).
% 219.30/28.32 fof(f121,plain,(
% 219.30/28.32 ![X0,X1]: (composition(join(X0,sF4_fnc),composition(sF2_fnc,X1))=composition(join(sF3_fnc,composition(X0,sF2_fnc)),X1))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f107,f120])).
% 219.30/28.32 fof(f136,plain,(
% 219.30/28.32 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f24,f23])).
% 219.30/28.32 fof(f163,plain,(
% 219.30/28.32 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f30,f22])).
% 219.30/28.32 fof(f164,plain,(
% 219.30/28.32 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f19,f22])).
% 219.30/28.32 fof(f166,plain,(
% 219.30/28.32 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X0,X1),complement(X2))))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f22,f22])).
% 219.30/28.32 fof(f167,plain,(
% 219.30/28.32 ![X0,X1,X2]: (meet(X0,join(complement(X1),complement(X2)))=complement(join(complement(X0),meet(X1,X2))))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f22,f22])).
% 219.30/28.32 fof(f170,plain,(
% 219.30/28.32 zero=complement(top)),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f31,f163])).
% 219.30/28.32 fof(f176,plain,(
% 219.30/28.32 zero=meet(top,zero)),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f170,f31])).
% 219.30/28.32 fof(f217,plain,(
% 219.30/28.32 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f19,f27])).
% 219.30/28.32 fof(f220,plain,(
% 219.30/28.32 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f26,f27])).
% 219.30/28.32 fof(f222,plain,(
% 219.30/28.32 ![X0]: (converse(join(X0,sF5_fnc))=join(converse(X0),sk1))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f55,f27])).
% 219.30/28.32 fof(f223,plain,(
% 219.30/28.32 ![X0,X1]: (converse(join(X0,converse(X1)))=join(converse(X0),X1))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f26,f27])).
% 219.30/28.32 fof(f228,plain,(
% 219.30/28.32 ![X0]: (converse(join(X0,sF5_fnc))=join(sk1,converse(X0)))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f19,f222])).
% 219.30/28.32 fof(f240,plain,(
% 219.30/28.32 ![X0,X1]: (join(X0,join(X1,complement(X0)))=join(top,X1))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f19,f88])).
% 219.30/28.32 fof(f289,plain,(
% 219.30/28.32 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f22,f164])).
% 219.30/28.32 fof(f305,plain,(
% 219.30/28.32 zero=meet(zero,top)),
% 219.30/28.32 inference(backward_demodulation,[status(thm)],[f289,f176])).
% 219.30/28.32 fof(f306,plain,(
% 219.30/28.32 sF2_fnc=meet(sk3,sk1)),
% 219.30/28.32 inference(backward_demodulation,[status(thm)],[f289,f37])).
% 219.30/28.32 fof(f307,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2))=meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)))),
% 219.30/28.32 inference(backward_demodulation,[status(thm)],[f289,f34])).
% 219.30/28.32 fof(f308,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2))=meet(X2,composition(X0,meet(X1,composition(converse(X0),X2)))))),
% 219.30/28.32 inference(backward_demodulation,[status(thm)],[f289,f33])).
% 219.30/28.32 fof(f316,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)))=meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f289,f307])).
% 219.30/28.32 fof(f317,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(X2,composition(X0,meet(X1,composition(converse(X0),X2)))))=meet(X2,composition(X0,meet(X1,composition(converse(X0),X2)))))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f289,f308])).
% 219.30/28.32 fof(f318,plain,(
% 219.30/28.32 ![X0]: (join(zero,composition(converse(X0),complement(composition(X0,top))))=complement(top))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f170,f48])).
% 219.30/28.32 fof(f328,plain,(
% 219.30/28.32 ![X0,X1]: (join(complement(converse(X0)),composition(converse(converse(X1)),complement(converse(composition(X0,X1)))))=complement(converse(X0)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f28,f48])).
% 219.30/28.32 fof(f338,plain,(
% 219.30/28.32 ![X0]: (join(complement(one),composition(converse(X0),complement(X0)))=complement(one))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f24,f48])).
% 219.30/28.32 fof(f341,plain,(
% 219.30/28.32 ![X0]: (join(zero,composition(converse(X0),complement(composition(X0,top))))=zero)),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f170,f318])).
% 219.30/28.32 fof(f350,plain,(
% 219.30/28.32 ![X0,X1]: (join(complement(converse(X0)),composition(X1,complement(converse(composition(X0,X1)))))=complement(converse(X0)))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f26,f328])).
% 219.30/28.32 fof(f373,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(meet(composition(X0,X1),converse(X2)),composition(meet(X0,converse(composition(X1,X2))),meet(X1,composition(converse(X0),converse(X2)))))=composition(meet(X0,composition(converse(X2),converse(X1))),meet(X1,composition(converse(X0),converse(X2)))))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f28,f32])).
% 219.30/28.32 fof(f418,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(meet(composition(X0,X1),converse(X2)),composition(meet(X0,converse(composition(X1,X2))),meet(X1,converse(composition(X2,X0)))))=composition(meet(X0,composition(converse(X2),converse(X1))),meet(X1,composition(converse(X0),converse(X2)))))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f28,f373])).
% 219.30/28.32 fof(f419,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(meet(composition(X0,X1),converse(X2)),composition(meet(X0,converse(composition(X1,X2))),meet(X1,converse(composition(X2,X0)))))=composition(meet(X0,converse(composition(X1,X2))),meet(X1,composition(converse(X0),converse(X2)))))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f28,f418])).
% 219.30/28.32 fof(f420,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(meet(composition(X0,X1),converse(X2)),composition(meet(X0,converse(composition(X1,X2))),meet(X1,converse(composition(X2,X0)))))=composition(meet(X0,converse(composition(X1,X2))),meet(X1,converse(composition(X2,X0)))))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f28,f419])).
% 219.30/28.32 fof(f454,plain,(
% 219.30/28.32 zero=join(zero,complement(join(complement(zero),top)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f305,f53])).
% 219.30/28.32 fof(f456,plain,(
% 219.30/28.32 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f31,f53])).
% 219.30/28.32 fof(f457,plain,(
% 219.30/28.32 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f164,f53])).
% 219.30/28.32 fof(f458,plain,(
% 219.30/28.32 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f22,f53])).
% 219.30/28.32 fof(f461,plain,(
% 219.30/28.32 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f30,f53])).
% 219.30/28.32 fof(f469,plain,(
% 219.30/28.32 zero=join(zero,complement(join(top,complement(zero))))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f19,f454])).
% 219.30/28.32 fof(f471,plain,(
% 219.30/28.32 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f164,f456])).
% 219.30/28.32 fof(f472,plain,(
% 219.30/28.32 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f19,f457])).
% 219.30/28.32 fof(f473,plain,(
% 219.30/28.32 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f19,f458])).
% 219.30/28.32 fof(f476,plain,(
% 219.30/28.32 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(X0)))))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f19,f461])).
% 219.30/28.32 fof(f477,plain,(
% 219.30/28.32 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f170,f476])).
% 219.30/28.32 fof(f559,plain,(
% 219.30/28.32 top=join(zero,meet(top,complement(zero)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f170,f477])).
% 219.30/28.32 fof(f569,plain,(
% 219.30/28.32 sk1=join(sF2_fnc,meet(sk1,complement(sk3)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f306,f472])).
% 219.30/28.32 fof(f576,plain,(
% 219.30/28.32 ![X0,X1]: (X0=join(meet(X1,X0),meet(complement(X1),X0)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f289,f472])).
% 219.30/28.32 fof(f578,plain,(
% 219.30/28.32 ![X0]: (X0=join(meet(top,X0),meet(X0,zero)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f170,f472])).
% 219.30/28.32 fof(f592,plain,(
% 219.30/28.32 ![X0]: (X0=join(meet(top,X0),meet(zero,X0)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f289,f578])).
% 219.30/28.32 fof(f602,plain,(
% 219.30/28.32 ![X0]: (X0=join(meet(zero,X0),meet(top,X0)))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f19,f592])).
% 219.30/28.32 fof(f629,plain,(
% 219.30/28.32 complement(zero)=join(zero,meet(top,complement(zero)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f31,f602])).
% 219.30/28.32 fof(f638,plain,(
% 219.30/28.32 zero=join(zero,complement(join(top,top)))),
% 219.30/28.32 inference(backward_demodulation,[status(thm)],[f639,f469])).
% 219.30/28.32 fof(f639,plain,(
% 219.30/28.32 complement(zero)=top),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f559,f629])).
% 219.30/28.32 fof(f645,plain,(
% 219.30/28.32 ![X0]: (zero=join(meet(zero,X0),complement(join(top,X0))))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f639,f53])).
% 219.30/28.32 fof(f702,plain,(
% 219.30/28.32 sk2=join(sF4_fnc,meet(sk2,complement(sF5_fnc)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f40,f473])).
% 219.30/28.32 fof(f707,plain,(
% 219.30/28.32 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f289,f473])).
% 219.30/28.32 fof(f750,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(meet(composition(X0,converse(X1)),X2),meet(X2,composition(meet(X0,composition(X2,X1)),converse(X1))))=meet(X2,composition(meet(X0,composition(X2,converse(converse(X1)))),converse(X1))))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f26,f316])).
% 219.30/28.32 fof(f779,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(meet(composition(X0,converse(X1)),X2),meet(X2,composition(meet(X0,composition(X2,X1)),converse(X1))))=meet(X2,composition(meet(X0,composition(X2,X1)),converse(X1))))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f26,f750])).
% 219.30/28.32 fof(f809,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(meet(composition(converse(X0),X1),X2),meet(X2,composition(converse(X0),meet(X1,composition(X0,X2)))))=meet(X2,composition(converse(X0),meet(X1,composition(converse(converse(X0)),X2)))))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f26,f317])).
% 219.30/28.32 fof(f845,plain,(
% 219.30/28.32 ![X0,X1,X2]: (join(meet(composition(converse(X0),X1),X2),meet(X2,composition(converse(X0),meet(X1,composition(X0,X2)))))=meet(X2,composition(converse(X0),meet(X1,composition(X0,X2)))))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f26,f809])).
% 219.30/28.32 fof(f854,plain,(
% 219.30/28.32 ![X0]: (complement(complement(X0))=join(meet(X0,complement(complement(X0))),zero))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f31,f576])).
% 219.30/28.32 fof(f867,plain,(
% 219.30/28.32 ![X0]: (complement(complement(X0))=join(zero,meet(X0,complement(complement(X0)))))),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f19,f854])).
% 219.30/28.32 fof(f876,plain,(
% 219.30/28.32 ![X0]: (complement(complement(X0))=X0)),
% 219.30/28.32 inference(forward_demodulation,[status(thm)],[f477,f867])).
% 219.30/28.32 fof(f885,plain,(
% 219.30/28.32 ![X0,X1]: (complement(meet(X0,X1))=join(complement(X1),complement(X0)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f164,f876])).
% 219.30/28.32 fof(f886,plain,(
% 219.30/28.32 ![X0,X1]: (complement(meet(X0,X1))=join(complement(X0),complement(X1)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f22,f876])).
% 219.30/28.32 fof(f892,plain,(
% 219.30/28.32 ![X0,X1]: (meet(complement(X0),X1)=complement(join(complement(X1),X0)))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f876,f164])).
% 219.30/28.32 fof(f893,plain,(
% 219.30/28.32 ![X0,X1]: (meet(X0,complement(X1))=complement(join(X1,complement(X0))))),
% 219.30/28.32 inference(paramodulation,[status(thm)],[f876,f164])).
% 219.30/28.32 fof(f895,plain,(
% 219.30/28.33 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),X1)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f876,f22])).
% 219.30/28.33 fof(f896,plain,(
% 219.30/28.33 ![X0,X1]: (meet(complement(X0),X1)=complement(join(X0,complement(X1))))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f876,f22])).
% 219.30/28.33 fof(f913,plain,(
% 219.30/28.33 ![X0,X1,X2]: (meet(X0,complement(meet(X1,X2)))=complement(join(complement(X0),meet(X2,X1))))),
% 219.30/28.33 inference(backward_demodulation,[status(thm)],[f885,f167])).
% 219.30/28.33 fof(f914,plain,(
% 219.30/28.33 ![X0,X1,X2]: (meet(complement(meet(X0,X1)),X2)=complement(join(meet(X1,X0),complement(X2))))),
% 219.30/28.33 inference(backward_demodulation,[status(thm)],[f885,f166])).
% 219.30/28.33 fof(f946,plain,(
% 219.30/28.33 ![X0,X1,X2]: (meet(X0,complement(meet(X1,X2)))=meet(X0,complement(meet(X2,X1))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f895,f913])).
% 219.30/28.33 fof(f947,plain,(
% 219.30/28.33 ![X0,X1,X2]: (meet(complement(meet(X0,X1)),X2)=meet(complement(meet(X1,X0)),X2))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f896,f914])).
% 219.30/28.33 fof(f1171,plain,(
% 219.30/28.33 ![X0,X1]: (converse(join(X0,X1))=converse(join(X1,X0)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f27,f217])).
% 219.30/28.33 fof(f1180,plain,(
% 219.30/28.33 ![X0,X1]: (converse(join(X0,converse(X1)))=join(X1,converse(X0)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f26,f217])).
% 219.30/28.33 fof(f1201,plain,(
% 219.30/28.33 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f24,f80])).
% 219.30/28.33 fof(f1238,plain,(
% 219.30/28.33 ![X0]: (X0=composition(converse(one),X0))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f26,f1201])).
% 219.30/28.33 fof(f1276,plain,(
% 219.30/28.33 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f136,f1238])).
% 219.30/28.33 fof(f1277,plain,(
% 219.30/28.33 one=converse(one)),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f24,f1238])).
% 219.30/28.33 fof(f1278,plain,(
% 219.30/28.33 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f1238,f48])).
% 219.30/28.33 fof(f1296,plain,(
% 219.30/28.33 ![X0,X1]: (composition(join(converse(one),X0),X1)=join(X1,composition(X0,X1)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f1238,f25])).
% 219.30/28.33 fof(f1309,plain,(
% 219.30/28.33 ![X0]: (composition(one,X0)=X0)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f1238,f1276])).
% 219.30/28.33 fof(f1313,plain,(
% 219.30/28.33 ![X0]: (complement(meet(X0,composition(one,X0)))=complement(X0))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f886,f1278])).
% 219.30/28.33 fof(f1314,plain,(
% 219.30/28.33 ![X0]: (complement(meet(X0,X0))=complement(X0))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f1309,f1313])).
% 219.30/28.33 fof(f1365,plain,(
% 219.30/28.33 ![X0,X1]: (composition(join(one,X0),X1)=join(X1,composition(X0,X1)))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f1277,f1296])).
% 219.30/28.33 fof(f1492,plain,(
% 219.30/28.33 ![X0]: (complement(complement(X0))=meet(X0,X0))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f1314,f876])).
% 219.30/28.33 fof(f1502,plain,(
% 219.30/28.33 ![X0]: (X0=join(zero,X0))),
% 219.30/28.33 inference(backward_demodulation,[status(thm)],[f1505,f471])).
% 219.30/28.33 fof(f1505,plain,(
% 219.30/28.33 ![X0]: (X0=meet(X0,X0))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f876,f1492])).
% 219.30/28.33 fof(f1532,plain,(
% 219.30/28.33 ![X0]: (composition(converse(X0),complement(composition(X0,top)))=zero)),
% 219.30/28.33 inference(backward_demodulation,[status(thm)],[f1502,f341])).
% 219.30/28.33 fof(f1536,plain,(
% 219.30/28.33 zero=complement(join(top,top))),
% 219.30/28.33 inference(backward_demodulation,[status(thm)],[f1502,f638])).
% 219.30/28.33 fof(f1542,plain,(
% 219.30/28.33 ![X0]: (X0=join(X0,zero))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f19,f1502])).
% 219.30/28.33 fof(f1882,plain,(
% 219.30/28.33 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X2,X0)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f19,f84])).
% 219.30/28.33 fof(f2112,plain,(
% 219.30/28.33 join(top,join(top,zero))=top),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f1536,f83])).
% 219.30/28.33 fof(f2122,plain,(
% 219.30/28.33 join(top,join(zero,top))=top),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f84,f2112])).
% 219.30/28.33 fof(f2123,plain,(
% 219.30/28.33 join(zero,join(top,top))=top),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f84,f2122])).
% 219.30/28.33 fof(f2125,plain,(
% 219.30/28.33 join(top,top)=top),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f1502,f2123])).
% 219.30/28.33 fof(f2150,plain,(
% 219.30/28.33 ![X0]: (join(X0,top)=join(top,join(X0,top)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f2125,f84])).
% 219.30/28.33 fof(f2372,plain,(
% 219.30/28.33 ![X0,X1]: (complement(meet(X0,complement(X1)))=join(X1,complement(X0)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f876,f885])).
% 219.30/28.33 fof(f2374,plain,(
% 219.30/28.33 ![X0]: (complement(meet(X0,top))=join(zero,complement(X0)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f170,f885])).
% 219.30/28.33 fof(f2390,plain,(
% 219.30/28.33 ![X0]: (complement(meet(X0,top))=complement(X0))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f1502,f2374])).
% 219.30/28.33 fof(f2559,plain,(
% 219.30/28.33 ![X0,X1,X2]: (composition(join(X0,X1),X2)=composition(join(X1,X0),X2))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f25,f96])).
% 219.30/28.33 fof(f2674,plain,(
% 219.30/28.33 ![X0]: (complement(complement(X0))=meet(X0,top))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f2390,f876])).
% 219.30/28.33 fof(f2710,plain,(
% 219.30/28.33 ![X0]: (X0=meet(X0,top))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f876,f2674])).
% 219.30/28.33 fof(f2745,plain,(
% 219.30/28.33 ![X0]: (X0=meet(top,X0))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f289,f2710])).
% 219.30/28.33 fof(f2984,plain,(
% 219.30/28.33 ![X0,X1]: (complement(meet(complement(X0),X1))=join(X0,complement(X1)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f876,f886])).
% 219.30/28.33 fof(f2987,plain,(
% 219.30/28.33 ![X0,X1]: (complement(meet(X0,complement(X1)))=join(complement(X0),X1))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f876,f886])).
% 219.30/28.33 fof(f3076,plain,(
% 219.30/28.33 ![X0,X1]: (meet(complement(X0),complement(X1))=complement(join(X1,X0)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f876,f893])).
% 219.30/28.33 fof(f3117,plain,(
% 219.30/28.33 ![X0,X1]: (meet(complement(join(X0,complement(complement(X1)))),X1)=complement(join(top,X0)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f240,f892])).
% 219.30/28.33 fof(f3171,plain,(
% 219.30/28.33 ![X0,X1]: (meet(X0,complement(join(X1,complement(complement(X0)))))=complement(join(top,X1)))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f289,f3117])).
% 219.30/28.33 fof(f3172,plain,(
% 219.30/28.33 ![X0,X1]: (meet(X0,meet(complement(X0),complement(X1)))=complement(join(top,X1)))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f893,f3171])).
% 219.30/28.33 fof(f3173,plain,(
% 219.30/28.33 ![X0,X1]: (meet(X0,complement(join(X1,X0)))=complement(join(top,X1)))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f3076,f3172])).
% 219.30/28.33 fof(f3333,plain,(
% 219.30/28.33 ![X0,X1]: (meet(complement(X0),complement(X1))=complement(join(X0,X1)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f876,f896])).
% 219.30/28.33 fof(f3378,plain,(
% 219.30/28.33 ![X0]: (converse(converse(X0))=join(converse(zero),X0))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f1502,f223])).
% 219.30/28.33 fof(f3425,plain,(
% 219.30/28.33 ![X0]: (X0=join(converse(zero),X0))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f26,f3378])).
% 219.30/28.33 fof(f3470,plain,(
% 219.30/28.33 zero=converse(zero)),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f1542,f3425])).
% 219.30/28.33 fof(f4733,plain,(
% 219.30/28.33 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f30,f220])).
% 219.30/28.33 fof(f6627,plain,(
% 219.30/28.33 ![X0]: (complement(complement(X0))=join(X0,complement(complement(X0))))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f1505,f2372])).
% 219.30/28.33 fof(f6664,plain,(
% 219.30/28.33 ![X0]: (X0=join(X0,complement(complement(X0))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f876,f6627])).
% 219.30/28.33 fof(f6684,plain,(
% 219.30/28.33 ![X0]: (X0=join(X0,X0))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f876,f6664])).
% 219.30/28.33 fof(f6791,plain,(
% 219.30/28.33 ![X0,X1]: (join(X0,X1)=join(X0,join(X1,X0)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f6684,f1882])).
% 219.30/28.33 fof(f6792,plain,(
% 219.30/28.33 ![X0,X1]: (join(X0,join(X0,X1))=join(X0,X1))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f6684,f89])).
% 219.30/28.33 fof(f6795,plain,(
% 219.30/28.33 ![X0]: (join(X0,join(X0,complement(X0)))=top)),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f6684,f83])).
% 219.30/28.33 fof(f6852,plain,(
% 219.30/28.33 ![X0]: (join(X0,top)=join(top,X0))),
% 219.30/28.33 inference(backward_demodulation,[status(thm)],[f6791,f2150])).
% 219.30/28.33 fof(f6941,plain,(
% 219.30/28.33 ![X0,X1]: (meet(X0,complement(join(X1,X0)))=complement(top))),
% 219.30/28.33 inference(backward_demodulation,[status(thm)],[f6959,f3173])).
% 219.30/28.33 fof(f6956,plain,(
% 219.30/28.33 ![X0]: (zero=join(meet(zero,X0),complement(top)))),
% 219.30/28.33 inference(backward_demodulation,[status(thm)],[f6959,f645])).
% 219.30/28.33 fof(f6959,plain,(
% 219.30/28.33 ![X0]: (join(top,X0)=top)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f240,f6795])).
% 219.30/28.33 fof(f6985,plain,(
% 219.30/28.33 ![X0]: (join(X0,top)=top)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f6959,f6852])).
% 219.30/28.33 fof(f7024,plain,(
% 219.30/28.33 ![X0,X1]: (meet(X0,complement(join(X1,X0)))=zero)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f170,f6941])).
% 219.30/28.33 fof(f7029,plain,(
% 219.30/28.33 ![X0]: (zero=join(complement(top),meet(zero,X0)))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f19,f6956])).
% 219.30/28.33 fof(f7030,plain,(
% 219.30/28.33 ![X0]: (zero=join(zero,meet(zero,X0)))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f170,f7029])).
% 219.30/28.33 fof(f7077,plain,(
% 219.30/28.33 ![X0]: (zero=meet(zero,X0))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f1502,f7030])).
% 219.30/28.33 fof(f7922,plain,(
% 219.30/28.33 ![X0]: (zero=meet(X0,zero))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f289,f7077])).
% 219.30/28.33 fof(f8029,plain,(
% 219.30/28.33 ![X0]: (converse(top)=join(X0,converse(top)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f6959,f1180])).
% 219.30/28.33 fof(f8320,plain,(
% 219.30/28.33 join(complement(converse(sk1)),composition(top,complement(converse(sk1))))=complement(converse(sk1))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f35,f350])).
% 219.30/28.33 fof(f8427,plain,(
% 219.30/28.33 composition(join(one,top),complement(converse(sk1)))=complement(converse(sk1))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f1365,f8320])).
% 219.30/28.33 fof(f8428,plain,(
% 219.30/28.33 composition(top,complement(converse(sk1)))=complement(converse(sk1))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f6985,f8427])).
% 219.30/28.33 fof(f8429,plain,(
% 219.30/28.33 composition(top,complement(sF5_fnc))=complement(converse(sk1))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f39,f8428])).
% 219.30/28.33 fof(f8430,plain,(
% 219.30/28.33 composition(top,complement(sF5_fnc))=complement(sF5_fnc)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f39,f8429])).
% 219.30/28.33 fof(f9743,plain,(
% 219.30/28.33 converse(top)=top),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f6959,f8029])).
% 219.30/28.33 fof(f9808,plain,(
% 219.30/28.33 ![X0]: (top=join(X0,converse(complement(converse(X0)))))),
% 219.30/28.33 inference(backward_demodulation,[status(thm)],[f9743,f4733])).
% 219.30/28.33 fof(f9940,plain,(
% 219.30/28.33 composition(top,complement(composition(top,top)))=zero),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f9743,f1532])).
% 219.30/28.33 fof(f9946,plain,(
% 219.30/28.33 ![X0]: (converse(composition(top,X0))=composition(converse(X0),top))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f9743,f80])).
% 219.30/28.33 fof(f10205,plain,(
% 219.30/28.33 ![X0]: (meet(composition(converse(X0),complement(X0)),complement(complement(one)))=zero)),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f338,f7024])).
% 219.30/28.33 fof(f10232,plain,(
% 219.30/28.33 ![X0]: (meet(complement(complement(one)),composition(converse(X0),complement(X0)))=zero)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f289,f10205])).
% 219.30/28.33 fof(f10233,plain,(
% 219.30/28.33 ![X0]: (meet(one,composition(converse(X0),complement(X0)))=zero)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f876,f10232])).
% 219.30/28.33 fof(f13018,plain,(
% 219.30/28.33 join(sF4_fnc,sk2)=join(sF4_fnc,meet(sk2,complement(sF5_fnc)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f702,f6792])).
% 219.30/28.33 fof(f13021,plain,(
% 219.30/28.33 join(sF2_fnc,sk1)=join(sF2_fnc,meet(sk1,complement(sk3)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f569,f6792])).
% 219.30/28.33 fof(f13044,plain,(
% 219.30/28.33 ![X0,X1]: (join(meet(X0,X1),X1)=join(meet(X0,X1),meet(complement(X0),X1)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f576,f6792])).
% 219.30/28.33 fof(f13163,plain,(
% 219.30/28.33 join(sk2,sF4_fnc)=join(sF4_fnc,meet(sk2,complement(sF5_fnc)))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f19,f13018])).
% 219.30/28.33 fof(f13165,plain,(
% 219.30/28.33 join(sk2,sF4_fnc)=sk2),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f702,f13163])).
% 219.30/28.33 fof(f13171,plain,(
% 219.30/28.33 join(sk1,sF2_fnc)=join(sF2_fnc,meet(sk1,complement(sk3)))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f19,f13021])).
% 219.30/28.33 fof(f13173,plain,(
% 219.30/28.33 join(sk1,sF2_fnc)=sk1),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f569,f13171])).
% 219.30/28.33 fof(f13209,plain,(
% 219.30/28.33 ![X0,X1]: (join(X0,meet(X1,X0))=join(meet(X1,X0),meet(complement(X1),X0)))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f19,f13044])).
% 219.30/28.33 fof(f13211,plain,(
% 219.30/28.33 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f576,f13209])).
% 219.30/28.33 fof(f13397,plain,(
% 219.30/28.33 composition(sk1,top)=join(sk1,composition(sF2_fnc,top))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f13173,f105])).
% 219.30/28.33 fof(f13412,plain,(
% 219.30/28.33 sk1=join(sk1,composition(sF2_fnc,top))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f35,f13397])).
% 219.30/28.33 fof(f13419,plain,(
% 219.30/28.33 composition(sk2,sF2_fnc)=join(sF1_fnc,composition(sF4_fnc,sF2_fnc))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f13165,f103])).
% 219.30/28.33 fof(f13435,plain,(
% 219.30/28.33 sF1_fnc=join(sF1_fnc,composition(sF4_fnc,sF2_fnc))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f38,f13419])).
% 219.30/28.33 fof(f13436,plain,(
% 219.30/28.33 sF1_fnc=join(sF1_fnc,sF3_fnc)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f41,f13435])).
% 219.30/28.33 fof(f13450,plain,(
% 219.30/28.33 ![X0]: (composition(sk2,composition(sF2_fnc,X0))=composition(sF0_fnc,X0))),
% 219.30/28.33 inference(backward_demodulation,[status(thm)],[f13552,f63])).
% 219.30/28.33 fof(f13552,plain,(
% 219.30/28.33 sF1_fnc=sF0_fnc),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f42,f13436])).
% 219.30/28.33 fof(f13817,plain,(
% 219.30/28.33 ![X0,X1,X2]: (join(meet(X0,X1),join(X1,X2))=join(X1,X2))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f13211,f89])).
% 219.30/28.33 fof(f13881,plain,(
% 219.30/28.33 ![X0,X1,X2]: (join(X0,join(X1,meet(X2,X0)))=join(X0,X1))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f84,f13817])).
% 219.30/28.33 fof(f16295,plain,(
% 219.30/28.33 meet(composition(sF2_fnc,top),complement(sk1))=zero),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f13412,f7024])).
% 219.30/28.33 fof(f16308,plain,(
% 219.30/28.33 meet(complement(sk1),composition(sF2_fnc,top))=zero),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f289,f16295])).
% 219.30/28.33 fof(f16949,plain,(
% 219.30/28.33 composition(top,top)=join(sk1,composition(converse(complement(converse(sk1))),top))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f9808,f105])).
% 219.30/28.33 fof(f17086,plain,(
% 219.30/28.33 composition(top,top)=join(sk1,converse(composition(top,complement(converse(sk1)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f9946,f16949])).
% 219.30/28.33 fof(f17087,plain,(
% 219.30/28.33 composition(top,top)=converse(join(composition(top,complement(converse(sk1))),sF5_fnc))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f228,f17086])).
% 219.30/28.33 fof(f17088,plain,(
% 219.30/28.33 composition(top,top)=converse(join(sF5_fnc,composition(top,complement(converse(sk1)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f1171,f17087])).
% 219.30/28.33 fof(f17089,plain,(
% 219.30/28.33 composition(top,top)=converse(join(sF5_fnc,composition(top,complement(sF5_fnc))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f39,f17088])).
% 219.30/28.33 fof(f17090,plain,(
% 219.30/28.33 composition(top,top)=converse(join(sF5_fnc,complement(sF5_fnc)))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f8430,f17089])).
% 219.30/28.33 fof(f17091,plain,(
% 219.30/28.33 composition(top,top)=converse(top)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f30,f17090])).
% 219.30/28.33 fof(f17093,plain,(
% 219.30/28.33 composition(top,complement(top))=zero),
% 219.30/28.33 inference(backward_demodulation,[status(thm)],[f17103,f9940])).
% 219.30/28.33 fof(f17103,plain,(
% 219.30/28.33 composition(top,top)=top),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f9743,f17091])).
% 219.30/28.33 fof(f17149,plain,(
% 219.30/28.33 composition(top,zero)=zero),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f170,f17093])).
% 219.30/28.33 fof(f17156,plain,(
% 219.30/28.33 ![X0]: (join(meet(composition(zero,X0),converse(top)),composition(meet(zero,converse(composition(X0,top))),meet(X0,converse(zero))))=composition(meet(zero,converse(composition(X0,top))),meet(X0,converse(composition(top,zero)))))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f17149,f420])).
% 219.30/28.33 fof(f17169,plain,(
% 219.30/28.33 ![X0,X1]: (join(composition(X0,zero),join(zero,X1))=join(composition(join(X0,top),zero),X1))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f17149,f114])).
% 219.30/28.33 fof(f17175,plain,(
% 219.30/28.33 ![X0]: (composition(join(top,X0),zero)=join(composition(X0,zero),zero))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f17149,f96])).
% 219.30/28.33 fof(f17197,plain,(
% 219.30/28.33 ![X0]: (join(meet(converse(top),composition(zero,X0)),composition(meet(zero,converse(composition(X0,top))),meet(X0,converse(zero))))=composition(meet(zero,converse(composition(X0,top))),meet(X0,converse(composition(top,zero)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f289,f17156])).
% 219.30/28.33 fof(f17198,plain,(
% 219.30/28.33 ![X0]: (join(meet(top,composition(zero,X0)),composition(meet(zero,converse(composition(X0,top))),meet(X0,converse(zero))))=composition(meet(zero,converse(composition(X0,top))),meet(X0,converse(composition(top,zero)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f9743,f17197])).
% 219.30/28.33 fof(f17199,plain,(
% 219.30/28.33 ![X0]: (join(composition(zero,X0),composition(meet(zero,converse(composition(X0,top))),meet(X0,converse(zero))))=composition(meet(zero,converse(composition(X0,top))),meet(X0,converse(composition(top,zero)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f2745,f17198])).
% 219.30/28.33 fof(f17200,plain,(
% 219.30/28.33 ![X0]: (join(composition(zero,X0),composition(zero,meet(X0,converse(zero))))=composition(meet(zero,converse(composition(X0,top))),meet(X0,converse(composition(top,zero)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f7077,f17199])).
% 219.30/28.33 fof(f17201,plain,(
% 219.30/28.33 ![X0]: (join(composition(zero,X0),composition(zero,meet(X0,zero)))=composition(meet(zero,converse(composition(X0,top))),meet(X0,converse(composition(top,zero)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f3470,f17200])).
% 219.30/28.33 fof(f17202,plain,(
% 219.30/28.33 ![X0]: (join(composition(zero,X0),composition(zero,zero))=composition(meet(zero,converse(composition(X0,top))),meet(X0,converse(composition(top,zero)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f7922,f17201])).
% 219.30/28.33 fof(f17203,plain,(
% 219.30/28.33 ![X0]: (join(composition(zero,X0),composition(zero,zero))=composition(zero,meet(X0,converse(composition(top,zero)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f7077,f17202])).
% 219.30/28.33 fof(f17204,plain,(
% 219.30/28.33 ![X0]: (join(composition(zero,X0),composition(zero,zero))=composition(zero,meet(X0,converse(zero))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f17149,f17203])).
% 219.30/28.33 fof(f17205,plain,(
% 219.30/28.33 ![X0]: (join(composition(zero,X0),composition(zero,zero))=composition(zero,meet(X0,zero)))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f3470,f17204])).
% 219.30/28.33 fof(f17206,plain,(
% 219.30/28.33 ![X0]: (join(composition(zero,X0),composition(zero,zero))=composition(zero,zero))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f7922,f17205])).
% 219.30/28.33 fof(f17294,plain,(
% 219.30/28.33 ![X0,X1]: (join(zero,join(X0,composition(X1,zero)))=join(composition(join(X1,top),zero),X0))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f84,f17169])).
% 219.30/28.33 fof(f17295,plain,(
% 219.30/28.33 ![X0,X1]: (join(X0,composition(X1,zero))=join(composition(join(X1,top),zero),X0))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f1502,f17294])).
% 219.30/28.33 fof(f17296,plain,(
% 219.30/28.33 ![X0,X1]: (join(X0,composition(X1,zero))=join(composition(top,zero),X0))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f6985,f17295])).
% 219.30/28.33 fof(f17297,plain,(
% 219.30/28.33 ![X0,X1]: (join(X0,composition(X1,zero))=join(zero,X0))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f17149,f17296])).
% 219.30/28.33 fof(f17298,plain,(
% 219.30/28.33 ![X0]: (composition(zero,X0)=composition(zero,zero))),
% 219.30/28.33 inference(backward_demodulation,[status(thm)],[f17319,f17206])).
% 219.30/28.33 fof(f17319,plain,(
% 219.30/28.33 ![X0,X1]: (join(X0,composition(X1,zero))=X0)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f1502,f17297])).
% 219.30/28.33 fof(f17346,plain,(
% 219.30/28.33 ![X0]: (composition(top,zero)=join(composition(X0,zero),zero))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f6959,f17175])).
% 219.30/28.33 fof(f17347,plain,(
% 219.30/28.33 ![X0]: (zero=join(composition(X0,zero),zero))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f17149,f17346])).
% 219.30/28.33 fof(f17379,plain,(
% 219.30/28.33 ![X0]: (zero=composition(X0,zero))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f1542,f17347])).
% 219.30/28.33 fof(f17447,plain,(
% 219.30/28.33 ![X0]: (composition(zero,X0)=zero)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f17379,f17298])).
% 219.30/28.33 fof(f57115,plain,(
% 219.30/28.33 ![X0,X1,X2]: (complement(meet(complement(X0),complement(meet(X1,X2))))=join(X0,complement(complement(meet(X2,X1)))))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f946,f2984])).
% 219.30/28.33 fof(f57303,plain,(
% 219.30/28.33 ![X0,X1,X2]: (join(X0,complement(complement(meet(X1,X2))))=join(X0,complement(complement(meet(X2,X1)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f2984,f57115])).
% 219.30/28.33 fof(f57304,plain,(
% 219.30/28.33 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(X0,complement(complement(meet(X2,X1)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f876,f57303])).
% 219.30/28.33 fof(f57305,plain,(
% 219.30/28.33 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(X0,meet(X2,X1)))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f876,f57304])).
% 219.30/28.33 fof(f57654,plain,(
% 219.30/28.33 ![X0,X1,X2]: (complement(meet(complement(meet(X0,X1)),complement(X2)))=join(complement(complement(meet(X1,X0))),X2))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f947,f2987])).
% 219.30/28.33 fof(f57994,plain,(
% 219.30/28.33 ![X0,X1,X2]: (join(meet(X0,X1),complement(complement(X2)))=join(complement(complement(meet(X1,X0))),X2))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f2984,f57654])).
% 219.30/28.33 fof(f57995,plain,(
% 219.30/28.33 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(complement(complement(meet(X1,X0))),X2))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f876,f57994])).
% 219.30/28.33 fof(f57996,plain,(
% 219.30/28.33 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,X0),X2))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f876,f57995])).
% 219.30/28.33 fof(f61583,plain,(
% 219.30/28.33 ![X0]: (join(meet(composition(one,converse(complement(X0))),converse(X0)),meet(converse(X0),composition(zero,converse(complement(X0)))))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f10233,f779])).
% 219.30/28.33 fof(f61721,plain,(
% 219.30/28.33 ![X0]: (join(meet(converse(X0),composition(zero,converse(complement(X0)))),meet(composition(one,converse(complement(X0))),converse(X0)))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f19,f61583])).
% 219.30/28.33 fof(f61722,plain,(
% 219.30/28.33 ![X0]: (join(meet(converse(X0),composition(zero,converse(complement(X0)))),meet(converse(X0),composition(one,converse(complement(X0)))))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f57305,f61721])).
% 219.30/28.33 fof(f61723,plain,(
% 219.30/28.33 ![X0]: (join(meet(converse(X0),composition(one,converse(complement(X0)))),meet(converse(X0),composition(zero,converse(complement(X0)))))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f19,f61722])).
% 219.30/28.33 fof(f61724,plain,(
% 219.30/28.33 ![X0]: (join(meet(converse(X0),converse(complement(X0))),meet(converse(X0),composition(zero,converse(complement(X0)))))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f1309,f61723])).
% 219.30/28.33 fof(f61725,plain,(
% 219.30/28.33 ![X0]: (join(meet(converse(X0),converse(complement(X0))),meet(converse(X0),zero))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f17447,f61724])).
% 219.30/28.33 fof(f61726,plain,(
% 219.30/28.33 ![X0]: (join(meet(converse(X0),zero),meet(converse(X0),converse(complement(X0))))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f19,f61725])).
% 219.30/28.33 fof(f61727,plain,(
% 219.30/28.33 ![X0]: (join(meet(zero,converse(X0)),meet(converse(X0),converse(complement(X0))))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f57996,f61726])).
% 219.30/28.33 fof(f61728,plain,(
% 219.30/28.33 ![X0]: (join(zero,meet(converse(X0),converse(complement(X0))))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f7077,f61727])).
% 219.30/28.33 fof(f61729,plain,(
% 219.30/28.33 ![X0]: (meet(converse(X0),converse(complement(X0)))=meet(converse(X0),composition(meet(one,composition(converse(X0),complement(X0))),converse(complement(X0)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f1502,f61728])).
% 219.30/28.33 fof(f61730,plain,(
% 219.30/28.33 ![X0]: (meet(converse(X0),converse(complement(X0)))=meet(converse(X0),composition(zero,converse(complement(X0)))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f10233,f61729])).
% 219.30/28.33 fof(f61731,plain,(
% 219.30/28.33 ![X0]: (meet(converse(X0),converse(complement(X0)))=meet(converse(X0),zero))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f17447,f61730])).
% 219.30/28.33 fof(f61732,plain,(
% 219.30/28.33 ![X0]: (meet(converse(X0),converse(complement(X0)))=zero)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f7922,f61731])).
% 219.30/28.33 fof(f61815,plain,(
% 219.30/28.33 ![X0]: (meet(X0,converse(complement(converse(X0))))=zero)),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f26,f61732])).
% 219.30/28.33 fof(f62269,plain,(
% 219.30/28.33 ![X0]: (X0=join(zero,meet(complement(converse(complement(converse(X0)))),X0)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f61815,f707])).
% 219.30/28.33 fof(f62338,plain,(
% 219.30/28.33 ![X0]: (X0=meet(complement(converse(complement(converse(X0)))),X0))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f1502,f62269])).
% 219.30/28.33 fof(f62339,plain,(
% 219.30/28.33 ![X0]: (X0=meet(X0,complement(converse(complement(converse(X0))))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f289,f62338])).
% 219.30/28.33 fof(f62452,plain,(
% 219.30/28.33 ![X0]: (complement(converse(complement(converse(X0))))=join(X0,meet(complement(X0),complement(converse(complement(converse(X0)))))))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f62339,f576])).
% 219.30/28.33 fof(f62565,plain,(
% 219.30/28.33 ![X0]: (complement(converse(complement(converse(X0))))=join(X0,complement(join(X0,converse(complement(converse(X0)))))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f3333,f62452])).
% 219.30/28.33 fof(f62566,plain,(
% 219.30/28.33 ![X0]: (complement(converse(complement(converse(X0))))=join(X0,complement(top)))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f9808,f62565])).
% 219.30/28.33 fof(f62567,plain,(
% 219.30/28.33 ![X0]: (complement(converse(complement(converse(X0))))=join(X0,zero))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f170,f62566])).
% 219.30/28.33 fof(f62590,plain,(
% 219.30/28.33 ![X0]: (complement(converse(complement(converse(X0))))=X0)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f1542,f62567])).
% 219.30/28.33 fof(f62695,plain,(
% 219.30/28.33 ![X0]: (complement(converse(complement(X0)))=converse(X0))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f26,f62590])).
% 219.30/28.33 fof(f62972,plain,(
% 219.30/28.33 ![X0]: (complement(converse(X0))=converse(complement(X0)))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f876,f62695])).
% 219.30/28.33 fof(f88692,plain,(
% 219.30/28.33 join(complement(sF5_fnc),sk2)=join(complement(sF5_fnc),sF4_fnc)),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f702,f13881])).
% 219.30/28.33 fof(f89066,plain,(
% 219.30/28.33 join(sk2,complement(sF5_fnc))=join(complement(sF5_fnc),sF4_fnc)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f19,f88692])).
% 219.30/28.33 fof(f89067,plain,(
% 219.30/28.33 join(sk2,complement(sF5_fnc))=join(sF4_fnc,complement(sF5_fnc))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f19,f89066])).
% 219.30/28.33 fof(f93755,plain,(
% 219.30/28.33 join(meet(composition(converse(sF2_fnc),complement(sk1)),top),meet(top,composition(converse(sF2_fnc),zero)))=meet(top,composition(converse(sF2_fnc),meet(complement(sk1),composition(sF2_fnc,top))))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f16308,f845])).
% 219.30/28.33 fof(f93816,plain,(
% 219.30/28.33 join(meet(top,composition(converse(sF2_fnc),zero)),meet(composition(converse(sF2_fnc),complement(sk1)),top))=meet(top,composition(converse(sF2_fnc),meet(complement(sk1),composition(sF2_fnc,top))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f19,f93755])).
% 219.30/28.33 fof(f93817,plain,(
% 219.30/28.33 join(meet(top,composition(converse(sF2_fnc),zero)),meet(top,composition(converse(sF2_fnc),complement(sk1))))=meet(top,composition(converse(sF2_fnc),meet(complement(sk1),composition(sF2_fnc,top))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f57305,f93816])).
% 219.30/28.33 fof(f93818,plain,(
% 219.30/28.33 join(composition(converse(sF2_fnc),zero),meet(top,composition(converse(sF2_fnc),complement(sk1))))=meet(top,composition(converse(sF2_fnc),meet(complement(sk1),composition(sF2_fnc,top))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f2745,f93817])).
% 219.30/28.33 fof(f93819,plain,(
% 219.30/28.33 join(zero,meet(top,composition(converse(sF2_fnc),complement(sk1))))=meet(top,composition(converse(sF2_fnc),meet(complement(sk1),composition(sF2_fnc,top))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f17379,f93818])).
% 219.30/28.33 fof(f93820,plain,(
% 219.30/28.33 meet(top,composition(converse(sF2_fnc),complement(sk1)))=meet(top,composition(converse(sF2_fnc),meet(complement(sk1),composition(sF2_fnc,top))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f1502,f93819])).
% 219.30/28.33 fof(f93821,plain,(
% 219.30/28.33 composition(converse(sF2_fnc),complement(sk1))=meet(top,composition(converse(sF2_fnc),meet(complement(sk1),composition(sF2_fnc,top))))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f2745,f93820])).
% 219.30/28.33 fof(f93822,plain,(
% 219.30/28.33 composition(converse(sF2_fnc),complement(sk1))=composition(converse(sF2_fnc),meet(complement(sk1),composition(sF2_fnc,top)))),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f2745,f93821])).
% 219.30/28.33 fof(f93823,plain,(
% 219.30/28.33 composition(converse(sF2_fnc),complement(sk1))=composition(converse(sF2_fnc),zero)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f16308,f93822])).
% 219.30/28.33 fof(f93824,plain,(
% 219.30/28.33 composition(converse(sF2_fnc),complement(sk1))=zero),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f17379,f93823])).
% 219.30/28.33 fof(f93945,plain,(
% 219.30/28.33 converse(zero)=composition(converse(complement(sk1)),sF2_fnc)),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f93824,f80])).
% 219.30/28.33 fof(f94054,plain,(
% 219.30/28.33 zero=composition(converse(complement(sk1)),sF2_fnc)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f3470,f93945])).
% 219.30/28.33 fof(f94055,plain,(
% 219.30/28.33 zero=composition(complement(converse(sk1)),sF2_fnc)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f62972,f94054])).
% 219.30/28.33 fof(f94056,plain,(
% 219.30/28.33 zero=composition(complement(sF5_fnc),sF2_fnc)),
% 219.30/28.33 inference(forward_demodulation,[status(thm)],[f39,f94055])).
% 219.30/28.33 fof(f95511,plain,(
% 219.30/28.33 ![X0]: (composition(join(complement(sF5_fnc),sF4_fnc),composition(sF2_fnc,X0))=composition(join(sF3_fnc,zero),X0))),
% 219.30/28.33 inference(paramodulation,[status(thm)],[f94056,f121])).
% 219.30/28.33 fof(f95565,plain,(
% 219.30/28.33 ![X0]: (composition(complement(sF5_fnc),composition(sF2_fnc,X0))=composition(zero,X0))),
% 219.30/28.34 inference(paramodulation,[status(thm)],[f94056,f23])).
% 219.30/28.34 fof(f95566,plain,(
% 219.30/28.34 ![X0]: (composition(join(sF4_fnc,complement(sF5_fnc)),composition(sF2_fnc,X0))=composition(join(sF3_fnc,zero),X0))),
% 219.30/28.34 inference(forward_demodulation,[status(thm)],[f2559,f95511])).
% 219.30/28.34 fof(f95567,plain,(
% 219.30/28.34 ![X0]: (composition(join(sk2,complement(sF5_fnc)),composition(sF2_fnc,X0))=composition(join(sF3_fnc,zero),X0))),
% 219.30/28.34 inference(forward_demodulation,[status(thm)],[f89067,f95566])).
% 219.30/28.34 fof(f95568,plain,(
% 219.30/28.34 ![X0]: (composition(join(sk2,complement(sF5_fnc)),composition(sF2_fnc,X0))=composition(join(zero,sF3_fnc),X0))),
% 219.30/28.34 inference(forward_demodulation,[status(thm)],[f2559,f95567])).
% 219.30/28.34 fof(f95569,plain,(
% 219.30/28.34 ![X0]: (composition(join(sk2,complement(sF5_fnc)),composition(sF2_fnc,X0))=composition(sF3_fnc,X0))),
% 219.30/28.34 inference(forward_demodulation,[status(thm)],[f1502,f95568])).
% 219.30/28.34 fof(f95787,plain,(
% 219.30/28.34 ![X0]: (composition(complement(sF5_fnc),composition(sF2_fnc,X0))=zero)),
% 219.30/28.34 inference(forward_demodulation,[status(thm)],[f17447,f95565])).
% 219.30/28.34 fof(f95948,plain,(
% 219.30/28.34 ![X0,X1]: (composition(join(X0,complement(sF5_fnc)),composition(sF2_fnc,X1))=join(zero,composition(X0,composition(sF2_fnc,X1))))),
% 219.30/28.34 inference(paramodulation,[status(thm)],[f95787,f96])).
% 219.30/28.34 fof(f96229,plain,(
% 219.30/28.34 ![X0]: (composition(sk2,composition(sF2_fnc,X0))=composition(sF3_fnc,X0))),
% 219.30/28.34 inference(backward_demodulation,[status(thm)],[f96231,f95569])).
% 219.30/28.34 fof(f96231,plain,(
% 219.30/28.34 ![X0,X1]: (composition(join(X0,complement(sF5_fnc)),composition(sF2_fnc,X1))=composition(X0,composition(sF2_fnc,X1)))),
% 219.30/28.34 inference(forward_demodulation,[status(thm)],[f1502,f95948])).
% 219.30/28.34 fof(f96246,plain,(
% 219.30/28.34 ![X0]: (composition(sF4_fnc,composition(sF2_fnc,X0))=composition(sF0_fnc,X0))),
% 219.30/28.34 inference(backward_demodulation,[status(thm)],[f96318,f62])).
% 219.30/28.34 fof(f96318,plain,(
% 219.30/28.34 ![X0]: (composition(sF0_fnc,X0)=composition(sF3_fnc,X0))),
% 219.30/28.34 inference(forward_demodulation,[status(thm)],[f13450,f96229])).
% 219.30/28.34 fof(f96936,plain,(
% 219.30/28.34 composition(sF4_fnc,sF2_fnc)=composition(sF0_fnc,one)),
% 219.30/28.34 inference(paramodulation,[status(thm)],[f24,f96246])).
% 176.61/28.69 fof(f97003,plain,(
% 176.61/28.69 sF3_fnc=composition(sF0_fnc,one)),
% 176.61/28.69 inference(forward_demodulation,[status(thm)],[f41,f96936])).
% 176.61/28.69 fof(f97004,plain,(
% 176.61/28.69 sF3_fnc=sF0_fnc),
% 176.61/28.69 inference(forward_demodulation,[status(thm)],[f24,f97003])).
% 176.61/28.69 fof(f97005,plain,(
% 176.61/28.69 $false),
% 176.61/28.69 inference(forward_subsumption_resolution,[status(thm)],[f97004,f52])).
% 176.61/28.69 % SZS output end CNFRefutation for theBenchmark.p
% 42.96/28.90 % Elapsed time: 28.396448 seconds
% 42.96/28.90 % CPU time: 223.515829 seconds
% 42.96/28.90 % Total memory used: 1.343 GB
% 42.96/28.90 % Net memory used: 1.323 GB
%------------------------------------------------------------------------------