%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL043-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 : n017.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:44 PM UTC 2026
% Result : Unsatisfiable 78.72s 10.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL043-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n017.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 04:03:27 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 78.72/10.32 % Refutation found
% 78.72/10.32 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 78.72/10.32 % SZS output start CNFRefutation for theBenchmark
% 78.72/10.32 fof(f1,axiom,(
% 78.72/10.32 (![A,B]: (join(A,B) = join(B,A) ))),
% 78.72/10.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.72/10.32 fof(f2,axiom,(
% 78.72/10.32 (![A,B,C]: (join(A,join(B,C)) = join(join(A,B),C) ))),
% 78.72/10.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.72/10.32 fof(f3,axiom,(
% 78.72/10.32 (![A,B]: (A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))) ))),
% 78.72/10.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.72/10.32 fof(f4,axiom,(
% 78.72/10.32 (![A,B]: (meet(A,B) = complement(join(complement(A),complement(B))) ))),
% 78.72/10.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.72/10.32 fof(f5,axiom,(
% 78.72/10.32 (![A,B,C]: (composition(A,composition(B,C)) = composition(composition(A,B),C) ))),
% 78.72/10.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.72/10.32 fof(f6,axiom,(
% 78.72/10.32 (![A]: (composition(A,one) = A ))),
% 78.72/10.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.72/10.32 fof(f7,axiom,(
% 78.72/10.32 (![A,B,C]: (composition(join(A,B),C) = join(composition(A,C),composition(B,C)) ))),
% 78.72/10.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.72/10.32 fof(f8,axiom,(
% 78.72/10.32 (![A]: (converse(converse(A)) = A ))),
% 78.72/10.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.72/10.32 fof(f9,axiom,(
% 78.72/10.32 (![A,B]: (converse(join(A,B)) = join(converse(A),converse(B)) ))),
% 78.72/10.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.72/10.32 fof(f10,axiom,(
% 78.72/10.32 (![A,B]: (converse(composition(A,B)) = composition(converse(B),converse(A)) ))),
% 78.72/10.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.72/10.32 fof(f11,axiom,(
% 78.72/10.32 (![A,B]: (join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B) ))),
% 78.72/10.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.72/10.32 fof(f12,axiom,(
% 78.72/10.32 (![A]: (top = join(A,complement(A)) ))),
% 78.72/10.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.72/10.32 fof(f13,axiom,(
% 78.72/10.32 (![A]: (zero = meet(A,complement(A)) ))),
% 78.72/10.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.72/10.32 fof(f14,axiom,(
% 78.72/10.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))) ))),
% 78.72/10.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.72/10.32 fof(f16,axiom,(
% 78.72/10.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) ))),
% 78.72/10.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.72/10.32 fof(f17,negated_conjecture,(
% 78.72/10.32 join(composition(sk1,converse(sk2)),sk3) = sk3 ),
% 78.72/10.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.72/10.32 fof(f18,negated_conjecture,(
% 78.72/10.32 join(composition(complement(sk3),sk2),complement(sk1)) != complement(sk1) ),
% 78.72/10.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.72/10.32 fof(f19,plain,(
% 78.72/10.32 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 78.72/10.32 inference(cnf_transformation,[status(thm)],[f1])).
% 78.72/10.32 fof(f20,plain,(
% 78.72/10.32 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 78.72/10.32 inference(cnf_transformation,[status(thm)],[f2])).
% 78.72/10.32 fof(f21,plain,(
% 78.72/10.32 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 78.72/10.32 inference(cnf_transformation,[status(thm)],[f3])).
% 78.72/10.32 fof(f22,plain,(
% 78.72/10.32 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 78.72/10.32 inference(cnf_transformation,[status(thm)],[f4])).
% 78.72/10.32 fof(f23,plain,(
% 78.72/10.32 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 78.72/10.32 inference(cnf_transformation,[status(thm)],[f5])).
% 78.72/10.32 fof(f24,plain,(
% 78.72/10.32 ![X0]: (composition(X0,one)=X0)),
% 78.72/10.32 inference(cnf_transformation,[status(thm)],[f6])).
% 78.72/10.32 fof(f25,plain,(
% 78.72/10.32 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 78.72/10.32 inference(cnf_transformation,[status(thm)],[f7])).
% 78.72/10.32 fof(f26,plain,(
% 78.72/10.32 ![X0]: (converse(converse(X0))=X0)),
% 78.72/10.32 inference(cnf_transformation,[status(thm)],[f8])).
% 78.72/10.32 fof(f27,plain,(
% 78.72/10.32 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 78.72/10.32 inference(cnf_transformation,[status(thm)],[f9])).
% 78.72/10.32 fof(f28,plain,(
% 78.72/10.32 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 78.72/10.32 inference(cnf_transformation,[status(thm)],[f10])).
% 78.72/10.32 fof(f29,plain,(
% 78.72/10.32 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 78.72/10.32 inference(cnf_transformation,[status(thm)],[f11])).
% 78.72/10.32 fof(f30,plain,(
% 78.72/10.32 ![X0]: (top=join(X0,complement(X0)))),
% 78.72/10.32 inference(cnf_transformation,[status(thm)],[f12])).
% 78.72/10.32 fof(f31,plain,(
% 78.72/10.32 ![X0]: (zero=meet(X0,complement(X0)))),
% 78.72/10.32 inference(cnf_transformation,[status(thm)],[f13])).
% 78.72/10.32 fof(f32,plain,(
% 78.72/10.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))))),
% 78.72/10.32 inference(cnf_transformation,[status(thm)],[f14])).
% 78.72/10.32 fof(f34,plain,(
% 78.72/10.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))),
% 78.72/10.32 inference(cnf_transformation,[status(thm)],[f16])).
% 78.72/10.32 fof(f35,plain,(
% 78.72/10.32 join(composition(sk1,converse(sk2)),sk3)=sk3),
% 78.72/10.32 inference(cnf_transformation,[status(thm)],[f17])).
% 78.72/10.32 fof(f36,plain,(
% 78.72/10.32 ~join(composition(complement(sk3),sk2),complement(sk1))=complement(sk1)),
% 78.72/10.32 inference(cnf_transformation,[status(thm)],[f18])).
% 78.72/10.32 fof(f37,definition,(
% 78.72/10.32 sF2_fnc=complement(sk3)),
% 78.72/10.32 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 78.72/10.32 fof(f38,definition,(
% 78.72/10.32 sF1_fnc=composition(sF2_fnc,sk2)),
% 78.72/10.32 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 78.72/10.32 fof(f39,definition,(
% 78.72/10.32 sF3_fnc=complement(sk1)),
% 78.72/10.32 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 78.72/10.32 fof(f40,definition,(
% 78.72/10.32 sF0_fnc=join(sF1_fnc,sF3_fnc)),
% 78.72/10.32 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 78.72/10.32 fof(f41,plain,(
% 78.72/10.32 ~sF0_fnc=sF3_fnc),
% 78.72/10.32 inference(definition_folding,[],[f36,f40,f39,f38,f37])).
% 78.72/10.32 fof(f42,plain,(
% 78.72/10.32 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f19,f21])).
% 78.72/10.32 fof(f43,plain,(
% 78.72/10.32 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f22,f42])).
% 78.72/10.32 fof(f44,plain,(
% 78.72/10.32 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f19,f29])).
% 78.72/10.32 fof(f45,plain,(
% 78.72/10.32 join(sk3,composition(sk1,converse(sk2)))=sk3),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f19,f35])).
% 78.72/10.32 fof(f46,plain,(
% 78.72/10.32 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f19,f43])).
% 78.72/10.32 fof(f60,plain,(
% 78.72/10.32 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f26,f28])).
% 78.72/10.32 fof(f74,plain,(
% 78.72/10.32 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f19,f22])).
% 78.72/10.32 fof(f76,plain,(
% 78.72/10.32 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X0,X1),complement(X2))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f22,f22])).
% 78.72/10.32 fof(f79,plain,(
% 78.72/10.32 ![X0,X1,X2]: (meet(X0,join(complement(X1),complement(X2)))=complement(join(complement(X0),meet(X1,X2))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f22,f22])).
% 78.72/10.32 fof(f92,plain,(
% 78.72/10.32 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f19,f20])).
% 78.72/10.32 fof(f97,plain,(
% 78.72/10.32 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X0),X2))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f19,f20])).
% 78.72/10.32 fof(f108,plain,(
% 78.72/10.32 ![X0,X1]: (converse(join(X0,converse(X1)))=join(converse(X0),X1))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f26,f27])).
% 78.72/10.32 fof(f128,plain,(
% 78.72/10.32 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X1,X2),composition(X0,X2)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f19,f25])).
% 78.72/10.32 fof(f131,plain,(
% 78.72/10.32 ![X0,X1,X2,X3]: (composition(join(composition(X0,X1),X2),X3)=join(composition(X0,composition(X1,X3)),composition(X2,X3)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f23,f25])).
% 78.72/10.32 fof(f138,plain,(
% 78.72/10.32 ![X0,X1,X2,X3]: (join(composition(X0,X1),join(composition(X2,X1),X3))=join(composition(join(X0,X2),X1),X3))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f25,f20])).
% 78.72/10.32 fof(f168,plain,(
% 78.72/10.32 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f24,f60])).
% 78.72/10.32 fof(f175,plain,(
% 78.72/10.32 ![X0]: (X0=composition(converse(one),X0))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f26,f168])).
% 78.72/10.32 fof(f182,plain,(
% 78.72/10.32 ![X0,X1]: (zero=meet(join(complement(X0),complement(X1)),meet(X0,X1)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f22,f31])).
% 78.72/10.32 fof(f185,plain,(
% 78.72/10.32 ![X0,X1]: (zero=complement(join(meet(X0,X1),complement(meet(X0,X1)))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f76,f182])).
% 78.72/10.32 fof(f186,plain,(
% 78.72/10.32 zero=complement(top)),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f30,f185])).
% 78.72/10.32 fof(f188,plain,(
% 78.72/10.32 ![X0]: (join(zero,composition(converse(X0),complement(composition(X0,top))))=complement(top))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f186,f44])).
% 78.72/10.32 fof(f191,plain,(
% 78.72/10.32 ![X0]: (meet(X0,top)=complement(join(complement(X0),zero)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f186,f22])).
% 78.72/10.32 fof(f192,plain,(
% 78.72/10.32 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f186,f22])).
% 78.72/10.32 fof(f193,plain,(
% 78.72/10.32 ![X0]: (join(zero,composition(converse(X0),complement(composition(X0,top))))=zero)),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f186,f188])).
% 78.72/10.32 fof(f196,plain,(
% 78.72/10.32 ![X0]: (meet(X0,top)=complement(join(zero,complement(X0))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f19,f191])).
% 78.72/10.32 fof(f198,plain,(
% 78.72/10.32 one=converse(one)),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f24,f175])).
% 78.72/10.32 fof(f199,plain,(
% 78.72/10.32 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f175,f44])).
% 78.72/10.32 fof(f207,plain,(
% 78.72/10.32 ![X0]: (X0=composition(one,X0))),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f198,f175])).
% 78.72/10.32 fof(f213,plain,(
% 78.72/10.32 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f207,f199])).
% 78.72/10.32 fof(f249,plain,(
% 78.72/10.32 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f30,f20])).
% 78.72/10.32 fof(f264,plain,(
% 78.72/10.32 ![X0,X1]: (join(meet(X0,X1),complement(join(complement(X0),complement(X1))))=complement(join(complement(X0),complement(X1))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f22,f213])).
% 78.72/10.32 fof(f274,plain,(
% 78.72/10.32 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f213,f22])).
% 78.72/10.32 fof(f285,plain,(
% 78.72/10.32 ![X0,X1]: (join(meet(X0,X1),meet(X0,X1))=complement(join(complement(X0),complement(X1))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f22,f264])).
% 78.72/10.32 fof(f288,plain,(
% 78.72/10.32 ![X0,X1]: (join(meet(X0,X1),meet(X0,X1))=meet(X0,X1))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f22,f285])).
% 78.72/10.32 fof(f344,plain,(
% 78.72/10.32 ![X0]: (join(meet(sF1_fnc,X0),composition(meet(sF2_fnc,composition(X0,converse(sk2))),meet(sk2,composition(converse(sF2_fnc),X0))))=composition(meet(sF2_fnc,composition(X0,converse(sk2))),meet(sk2,composition(converse(sF2_fnc),X0))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f38,f32])).
% 78.72/10.32 fof(f347,plain,(
% 78.72/10.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)))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f28,f32])).
% 78.72/10.32 fof(f374,plain,(
% 78.72/10.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)))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f28,f347])).
% 78.72/10.32 fof(f375,plain,(
% 78.72/10.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)))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f28,f374])).
% 78.72/10.32 fof(f376,plain,(
% 78.72/10.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)))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f28,f375])).
% 78.72/10.32 fof(f462,plain,(
% 78.72/10.32 ![X0,X1,X2,X3]: (join(meet(composition(X0,X1),X2),join(meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2),X3))=join(meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2),X3))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f34,f20])).
% 78.72/10.32 fof(f877,plain,(
% 78.72/10.32 ![X0]: (meet(top,X0)=meet(X0,top))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f196,f192])).
% 78.72/10.32 fof(f949,plain,(
% 78.72/10.32 ![X0]: (X0=join(meet(top,X0),complement(join(complement(X0),top))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f877,f46])).
% 78.72/10.32 fof(f952,plain,(
% 78.72/10.32 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f31,f46])).
% 78.72/10.32 fof(f954,plain,(
% 78.72/10.32 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f22,f46])).
% 78.72/10.32 fof(f969,plain,(
% 78.72/10.32 ![X0]: (sk1=join(meet(sk1,X0),complement(join(sF3_fnc,X0))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f39,f46])).
% 78.72/10.32 fof(f987,plain,(
% 78.72/10.32 ![X0]: (X0=join(meet(top,X0),complement(join(top,complement(X0)))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f19,f949])).
% 78.72/10.32 fof(f990,plain,(
% 78.72/10.32 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f22,f952])).
% 78.72/10.32 fof(f991,plain,(
% 78.72/10.32 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f274,f990])).
% 78.72/10.32 fof(f996,plain,(
% 78.72/10.32 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f19,f954])).
% 78.72/10.32 fof(f1109,plain,(
% 78.72/10.32 ![X0]: (meet(top,complement(X0))=complement(X0))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f991,f192])).
% 78.72/10.32 fof(f1132,plain,(
% 78.72/10.32 ![X0,X1]: (meet(top,meet(X0,X1))=complement(join(complement(X0),complement(X1))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f22,f1109])).
% 78.72/10.32 fof(f1136,plain,(
% 78.72/10.32 ![X0]: (top=join(complement(X0),complement(join(complement(top),complement(X0)))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f1109,f46])).
% 78.72/10.32 fof(f1152,plain,(
% 78.72/10.32 ![X0,X1]: (meet(top,meet(X0,X1))=meet(X0,X1))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f22,f1132])).
% 78.72/10.32 fof(f1156,plain,(
% 78.72/10.32 ![X0]: (top=join(complement(X0),meet(top,X0)))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f22,f1136])).
% 78.72/10.32 fof(f1212,plain,(
% 78.72/10.32 ![X0]: (X0=join(meet(X0,meet(top,X0)),complement(top)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f1156,f46])).
% 78.72/10.32 fof(f1230,plain,(
% 78.72/10.32 ![X0]: (X0=join(complement(top),meet(X0,meet(top,X0))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f19,f1212])).
% 78.72/10.32 fof(f1231,plain,(
% 78.72/10.32 ![X0]: (X0=join(zero,meet(X0,meet(top,X0))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f186,f1230])).
% 78.72/10.32 fof(f1426,plain,(
% 78.72/10.32 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f22,f74])).
% 78.72/10.32 fof(f1445,plain,(
% 78.72/10.32 ![X0,X1]: (meet(join(zero,complement(X0)),X1)=complement(join(complement(X1),meet(X0,top))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f196,f74])).
% 78.72/10.32 fof(f1456,plain,(
% 78.72/10.32 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f74,f46])).
% 78.72/10.32 fof(f1508,plain,(
% 78.72/10.32 ![X0,X1,X2,X3]: (join(meet(composition(X0,X1),X2),join(meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2),X3))=join(meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)),X3))),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f1426,f462])).
% 78.72/10.32 fof(f1546,plain,(
% 78.72/10.32 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f19,f1456])).
% 78.72/10.32 fof(f1615,plain,(
% 78.72/10.32 ![X0,X1,X2,X3]: (join(meet(composition(X0,X1),X2),join(meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)),X3))=join(meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)),X3))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f1426,f1508])).
% 78.72/10.32 fof(f2530,plain,(
% 78.72/10.32 ![X0]: (join(X0,complement(X0))=join(top,complement(X0)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f213,f249])).
% 78.72/10.32 fof(f2533,plain,(
% 78.72/10.32 ![X0]: (join(X0,top)=join(top,complement(complement(X0))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f30,f249])).
% 78.72/10.32 fof(f2556,plain,(
% 78.72/10.32 ![X0,X1]: (X0=join(meet(X0,join(complement(complement(X0)),X1)),complement(join(top,X1))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f249,f46])).
% 78.72/10.32 fof(f2563,plain,(
% 78.72/10.32 ![X0]: (X0=join(meet(top,X0),complement(top)))),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f2564,f987])).
% 78.72/10.32 fof(f2564,plain,(
% 78.72/10.32 ![X0]: (top=join(top,complement(X0)))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f30,f2530])).
% 78.72/10.32 fof(f2569,plain,(
% 78.72/10.32 ![X0]: (join(X0,top)=top)),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f2564,f2533])).
% 78.72/10.32 fof(f2595,plain,(
% 78.72/10.32 ![X0,X1]: (X0=join(complement(join(top,X1)),meet(X0,join(complement(complement(X0)),X1))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f19,f2556])).
% 78.72/10.32 fof(f2604,plain,(
% 78.72/10.32 ![X0]: (X0=join(complement(top),meet(top,X0)))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f19,f2563])).
% 78.72/10.32 fof(f2606,plain,(
% 78.72/10.32 ![X0]: (X0=join(zero,meet(top,X0)))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f186,f2604])).
% 78.72/10.32 fof(f2620,plain,(
% 78.72/10.32 ![X0]: (join(top,X0)=top)),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f19,f2569])).
% 78.72/10.32 fof(f2631,plain,(
% 78.72/10.32 ![X0]: (X0=join(meet(X0,top),complement(top)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f2569,f46])).
% 78.72/10.32 fof(f2647,plain,(
% 78.72/10.32 ![X0,X1]: (join(X0,join(complement(X0),X1))=top)),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f2620,f249])).
% 78.72/10.32 fof(f2669,plain,(
% 78.72/10.32 ![X0,X1]: (X0=join(complement(top),meet(X0,join(complement(complement(X0)),X1))))),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f2620,f2595])).
% 78.72/10.32 fof(f2693,plain,(
% 78.72/10.32 ![X0]: (X0=join(complement(top),meet(X0,top)))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f19,f2631])).
% 78.72/10.32 fof(f2695,plain,(
% 78.72/10.32 ![X0]: (X0=join(zero,meet(X0,top)))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f186,f2693])).
% 78.72/10.32 fof(f2701,plain,(
% 78.72/10.32 ![X0,X1]: (X0=join(zero,meet(X0,join(complement(complement(X0)),X1))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f186,f2669])).
% 78.72/10.32 fof(f2707,plain,(
% 78.72/10.32 ![X0]: (converse(top)=join(converse(top),X0))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f2620,f108])).
% 78.72/10.32 fof(f2732,plain,(
% 78.72/10.32 ![X0,X1]: (meet(X0,X1)=join(zero,meet(X0,X1)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f1152,f2606])).
% 78.72/10.32 fof(f2733,plain,(
% 78.72/10.32 ![X0]: (complement(X0)=join(zero,complement(X0)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f1109,f2606])).
% 78.72/10.32 fof(f2737,plain,(
% 78.72/10.32 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(join(complement(top),meet(X0,X1)))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f79,f2606])).
% 78.72/10.32 fof(f2753,plain,(
% 78.72/10.32 ![X0]: (X0=meet(top,X0))),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f2732,f2606])).
% 78.72/10.32 fof(f2754,plain,(
% 78.72/10.32 ![X0]: (X0=meet(X0,top))),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f2732,f2695])).
% 78.72/10.32 fof(f2756,plain,(
% 78.72/10.32 ![X0]: (X0=meet(X0,meet(top,X0)))),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f2732,f1231])).
% 78.72/10.32 fof(f2772,plain,(
% 78.72/10.32 ![X0,X1]: (X0=meet(X0,join(complement(complement(X0)),X1)))),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f2732,f2701])).
% 78.72/10.32 fof(f2781,plain,(
% 78.72/10.32 ![X0]: (X0=complement(complement(X0)))),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f2733,f991])).
% 78.72/10.32 fof(f2803,plain,(
% 78.72/10.32 ![X0,X1]: (meet(complement(X0),X1)=complement(join(complement(X1),meet(X0,top))))),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f2733,f1445])).
% 78.72/10.32 fof(f2823,plain,(
% 78.72/10.32 ![X0,X1]: (join(complement(X0),complement(X1))=complement(join(complement(top),meet(X0,X1))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f2733,f2737])).
% 78.72/10.32 fof(f2824,plain,(
% 78.72/10.32 ![X0,X1]: (join(complement(X0),complement(X1))=complement(join(zero,meet(X0,X1))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f186,f2823])).
% 78.72/10.32 fof(f2857,plain,(
% 78.72/10.32 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f2732,f2824])).
% 78.72/10.32 fof(f2910,plain,(
% 78.72/10.32 ![X0]: (X0=meet(X0,X0))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f2753,f2756])).
% 78.72/10.32 fof(f3011,plain,(
% 78.72/10.32 ![X0,X1]: (X0=meet(X0,join(X0,X1)))),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f2781,f2772])).
% 78.72/10.32 fof(f3055,plain,(
% 78.72/10.32 ![X0,X1]: (meet(complement(X0),X1)=complement(join(complement(X1),X0)))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f2754,f2803])).
% 78.72/10.32 fof(f3362,plain,(
% 78.72/10.32 ![X0]: (X0=join(X0,meet(X0,complement(X0))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f2910,f1546])).
% 78.72/10.32 fof(f3430,plain,(
% 78.72/10.32 ![X0]: (X0=join(X0,zero))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f31,f3362])).
% 78.72/10.32 fof(f3435,plain,(
% 78.72/10.32 ![X0]: (X0=join(zero,X0))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f19,f3430])).
% 78.72/10.32 fof(f3456,plain,(
% 78.72/10.32 ![X0]: (composition(converse(X0),complement(composition(X0,top)))=zero)),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f3435,f193])).
% 78.72/10.32 fof(f3469,plain,(
% 78.72/10.32 ![X0]: (converse(converse(X0))=join(converse(zero),X0))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f3435,f108])).
% 78.72/10.32 fof(f3475,plain,(
% 78.72/10.32 ![X0]: (X0=join(converse(zero),X0))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f26,f3469])).
% 78.72/10.32 fof(f4013,plain,(
% 78.72/10.32 zero=converse(zero)),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f3430,f3475])).
% 78.72/10.32 fof(f4242,plain,(
% 78.72/10.32 ![X0]: (zero=meet(zero,X0))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f3435,f3011])).
% 78.72/10.32 fof(f4258,plain,(
% 78.72/10.32 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X1))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f1546,f3011])).
% 78.72/10.32 fof(f4259,plain,(
% 78.72/10.32 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X0))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f996,f3011])).
% 78.72/10.32 fof(f4290,plain,(
% 78.72/10.32 ![X0,X1]: (X0=meet(X0,join(X1,X0)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f19,f3011])).
% 78.72/10.32 fof(f4327,plain,(
% 78.72/10.32 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X0,X1)))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f1426,f4258])).
% 78.72/10.32 fof(f4332,plain,(
% 78.72/10.32 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X0,X1)))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f1426,f4259])).
% 78.72/10.32 fof(f4377,plain,(
% 78.72/10.32 ![X0]: (zero=join(meet(X0,zero),zero))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f4242,f1546])).
% 78.72/10.32 fof(f4413,plain,(
% 78.72/10.32 ![X0]: (zero=meet(X0,zero))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f3430,f4377])).
% 78.72/10.32 fof(f4717,plain,(
% 78.72/10.32 converse(top)=top),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f2569,f2707])).
% 78.72/10.32 fof(f6649,plain,(
% 78.72/10.32 ![X0]: (join(X0,meet(top,X0))=meet(top,X0))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f2753,f288])).
% 78.72/10.32 fof(f6709,plain,(
% 78.72/10.32 ![X0]: (join(X0,X0)=meet(top,X0))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f2753,f6649])).
% 78.72/10.32 fof(f6717,plain,(
% 78.72/10.32 ![X0]: (join(X0,X0)=X0)),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f2753,f6709])).
% 78.72/10.32 fof(f6795,plain,(
% 78.72/10.32 ![X0,X1]: (join(X0,join(join(X1,X0),X1))=join(X1,X0))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f92,f6717])).
% 78.72/10.32 fof(f6845,plain,(
% 78.72/10.32 ![X0,X1]: (join(X0,join(X0,join(X1,X1)))=join(X1,X0))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f97,f6795])).
% 78.72/10.32 fof(f6862,plain,(
% 78.72/10.32 ![X0,X1]: (join(X0,join(X0,X1))=join(X1,X0))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f6717,f6845])).
% 78.72/10.32 fof(f6933,plain,(
% 78.72/10.32 ![X0,X1]: (join(meet(X0,X1),X1)=join(meet(X1,complement(X0)),meet(X0,X1)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f1546,f6862])).
% 78.72/10.32 fof(f7122,plain,(
% 78.72/10.32 ![X0,X1]: (join(X0,meet(X1,X0))=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f19,f6933])).
% 78.72/10.32 fof(f7123,plain,(
% 78.72/10.32 ![X0,X1]: (join(X0,meet(X1,X0))=join(meet(X1,X0),meet(X0,complement(X1))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f19,f7122])).
% 78.72/10.32 fof(f7132,plain,(
% 78.72/10.32 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f1546,f7123])).
% 78.72/10.32 fof(f7616,plain,(
% 78.72/10.32 ![X0,X1,X2]: (join(X0,join(meet(X1,X0),X2))=join(X0,X2))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f7132,f20])).
% 78.72/10.32 fof(f9439,plain,(
% 78.72/10.32 ![X0,X1]: (X0=join(meet(X1,X0),meet(complement(X1),X0)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f1426,f1546])).
% 78.72/10.32 fof(f9446,plain,(
% 78.72/10.32 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X1,X0)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f1426,f4332])).
% 78.72/10.32 fof(f9447,plain,(
% 78.72/10.32 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X1,X0)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f1426,f4327])).
% 78.72/10.32 fof(f11538,plain,(
% 78.72/10.32 ![X0,X1]: (join(X0,complement(meet(X0,X1)))=top)),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f2857,f2647])).
% 78.72/10.32 fof(f11953,plain,(
% 78.72/10.32 ![X0,X1]: (complement(meet(X0,meet(complement(X0),X1)))=top)),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f2857,f11538])).
% 78.72/10.32 fof(f12723,plain,(
% 78.72/10.32 ![X0,X1]: (complement(meet(X0,meet(X1,complement(X0))))=top)),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f9447,f11953])).
% 78.72/10.32 fof(f13470,plain,(
% 78.72/10.32 ![X0,X1]: (meet(X0,meet(X1,complement(X0)))=complement(top))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f12723,f2781])).
% 78.72/10.32 fof(f13529,plain,(
% 78.72/10.32 ![X0,X1]: (meet(X0,meet(X1,complement(X0)))=zero)),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f186,f13470])).
% 78.72/10.32 fof(f13561,plain,(
% 78.72/10.32 ![X0,X1]: (meet(complement(X0),meet(X1,X0))=zero)),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f2781,f13529])).
% 78.72/10.32 fof(f13761,plain,(
% 78.72/10.32 ![X0,X1]: (meet(complement(join(X0,X1)),X1)=zero)),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f4290,f13561])).
% 78.72/10.32 fof(f13762,plain,(
% 78.72/10.32 ![X0,X1]: (meet(complement(join(X0,X1)),X0)=zero)),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f3011,f13561])).
% 78.72/10.32 fof(f13808,plain,(
% 78.72/10.32 ![X0,X1]: (meet(X0,complement(join(X1,X0)))=zero)),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f1426,f13761])).
% 78.72/10.32 fof(f13809,plain,(
% 78.72/10.32 ![X0,X1]: (meet(X0,complement(join(X0,X1)))=zero)),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f1426,f13762])).
% 78.72/10.32 fof(f16164,plain,(
% 78.72/10.32 meet(composition(sk1,converse(sk2)),complement(sk3))=zero),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f45,f13808])).
% 78.72/10.32 fof(f16329,plain,(
% 78.72/10.32 meet(complement(sk3),composition(sk1,converse(sk2)))=zero),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f1426,f16164])).
% 78.72/10.32 fof(f16331,plain,(
% 78.72/10.32 meet(sF2_fnc,composition(sk1,converse(sk2)))=zero),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f37,f16329])).
% 78.72/10.32 fof(f16738,plain,(
% 78.72/10.32 ![X0,X1]: (complement(join(X0,X1))=join(zero,meet(complement(X0),complement(join(X0,X1)))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f13809,f9439])).
% 78.72/10.32 fof(f16869,plain,(
% 78.72/10.32 ![X0,X1]: (complement(join(X0,X1))=meet(complement(X0),complement(join(X0,X1))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f3435,f16738])).
% 78.72/10.32 fof(f17451,plain,(
% 78.72/10.32 ![X0,X1]: (meet(complement(X0),complement(X1))=complement(join(X1,X0)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f2781,f3055])).
% 78.72/10.32 fof(f17573,plain,(
% 78.72/10.32 ![X0,X1]: (complement(join(X0,X1))=complement(join(join(X0,X1),X0)))),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f17451,f16869])).
% 78.72/10.32 fof(f17624,plain,(
% 78.72/10.32 ![X0,X1]: (complement(join(X0,X1))=complement(join(X1,join(X0,X0))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f97,f17573])).
% 78.72/10.32 fof(f17625,plain,(
% 78.72/10.32 ![X0,X1]: (complement(join(X0,X1))=complement(join(X1,X0)))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f6717,f17624])).
% 78.72/10.32 fof(f19701,plain,(
% 78.72/10.32 composition(top,complement(composition(top,top)))=zero),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f4717,f3456])).
% 78.72/10.32 fof(f33840,plain,(
% 78.72/10.32 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f24,f1615])).
% 78.72/10.32 fof(f34018,plain,(
% 78.72/10.32 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,meet(X0,composition(X1,converse(one)))),X2))=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f24,f33840])).
% 78.72/10.32 fof(f34019,plain,(
% 78.72/10.32 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,meet(X0,composition(X1,one))),X2))=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f198,f34018])).
% 78.72/10.32 fof(f34020,plain,(
% 78.72/10.32 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,meet(X0,X1)),X2))=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f24,f34019])).
% 78.72/10.32 fof(f34021,plain,(
% 78.72/10.32 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f7616,f34020])).
% 78.72/10.32 fof(f34022,plain,(
% 78.72/10.32 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,meet(X0,composition(X1,converse(one)))),X2))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f24,f34021])).
% 78.72/10.32 fof(f34023,plain,(
% 78.72/10.32 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,meet(X0,composition(X1,one))),X2))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f198,f34022])).
% 78.72/10.32 fof(f34024,plain,(
% 78.72/10.32 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,meet(X0,X1)),X2))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f24,f34023])).
% 78.72/10.32 fof(f34025,plain,(
% 78.72/10.32 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,X0),X2))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f9446,f34024])).
% 78.72/10.32 fof(f45170,plain,(
% 78.72/10.32 join(meet(sF1_fnc,sk1),composition(zero,meet(sk2,composition(converse(sF2_fnc),sk1))))=composition(meet(sF2_fnc,composition(sk1,converse(sk2))),meet(sk2,composition(converse(sF2_fnc),sk1)))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f16331,f344])).
% 78.72/10.32 fof(f45224,plain,(
% 78.72/10.32 join(meet(sk1,sF1_fnc),composition(zero,meet(sk2,composition(converse(sF2_fnc),sk1))))=composition(meet(sF2_fnc,composition(sk1,converse(sk2))),meet(sk2,composition(converse(sF2_fnc),sk1)))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f34025,f45170])).
% 78.72/10.32 fof(f45225,plain,(
% 78.72/10.32 join(meet(sk1,sF1_fnc),composition(zero,meet(sk2,composition(converse(sF2_fnc),sk1))))=composition(zero,meet(sk2,composition(converse(sF2_fnc),sk1)))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f16331,f45224])).
% 78.72/10.32 fof(f52069,plain,(
% 78.72/10.32 ![X0]: (join(meet(composition(complement(composition(top,top)),X0),converse(top)),composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(zero))))=composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(composition(top,complement(composition(top,top)))))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f19701,f376])).
% 78.72/10.32 fof(f52082,plain,(
% 78.72/10.32 ![X0,X1]: (join(composition(X0,complement(composition(top,top))),join(zero,X1))=join(composition(join(X0,top),complement(composition(top,top))),X1))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f19701,f138])).
% 78.72/10.32 fof(f52087,plain,(
% 78.72/10.32 ![X0,X1]: (composition(join(composition(X0,top),X1),complement(composition(top,top)))=join(composition(X0,zero),composition(X1,complement(composition(top,top)))))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f19701,f131])).
% 78.72/10.32 fof(f52088,plain,(
% 78.72/10.32 ![X0]: (composition(join(top,X0),complement(composition(top,top)))=join(composition(X0,complement(composition(top,top))),zero))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f19701,f128])).
% 78.72/10.32 fof(f52096,plain,(
% 78.72/10.32 ![X0]: (composition(top,composition(complement(composition(top,top)),X0))=composition(zero,X0))),
% 78.72/10.32 inference(paramodulation,[status(thm)],[f19701,f23])).
% 78.72/10.32 fof(f52190,plain,(
% 78.72/10.32 ![X0]: (join(meet(converse(top),composition(complement(composition(top,top)),X0)),composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(zero))))=composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(composition(top,complement(composition(top,top)))))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f34025,f52069])).
% 78.72/10.32 fof(f52191,plain,(
% 78.72/10.32 ![X0]: (join(meet(top,composition(complement(composition(top,top)),X0)),composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(zero))))=composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(composition(top,complement(composition(top,top)))))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f4717,f52190])).
% 78.72/10.32 fof(f52192,plain,(
% 78.72/10.32 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(zero))))=composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(composition(top,complement(composition(top,top)))))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f2753,f52191])).
% 78.72/10.32 fof(f52193,plain,(
% 78.72/10.32 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,zero)))=composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(composition(top,complement(composition(top,top)))))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f4013,f52192])).
% 78.72/10.32 fof(f52194,plain,(
% 78.72/10.32 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(meet(complement(composition(top,top)),converse(composition(X0,top))),zero))=composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(composition(top,complement(composition(top,top)))))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f4413,f52193])).
% 78.72/10.32 fof(f52195,plain,(
% 78.72/10.32 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(meet(complement(composition(top,top)),converse(composition(X0,top))),zero))=composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(zero))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f19701,f52194])).
% 78.72/10.32 fof(f52196,plain,(
% 78.72/10.32 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(meet(complement(composition(top,top)),converse(composition(X0,top))),zero))=composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,zero)))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f4013,f52195])).
% 78.72/10.32 fof(f52197,plain,(
% 78.72/10.32 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(meet(complement(composition(top,top)),converse(composition(X0,top))),zero))=composition(meet(complement(composition(top,top)),converse(composition(X0,top))),zero))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f4413,f52196])).
% 78.72/10.32 fof(f52262,plain,(
% 78.72/10.32 ![X0,X1]: (join(zero,join(X0,composition(X1,complement(composition(top,top)))))=join(composition(join(X1,top),complement(composition(top,top))),X0))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f92,f52082])).
% 78.72/10.32 fof(f52263,plain,(
% 78.72/10.32 ![X0,X1]: (join(X0,composition(X1,complement(composition(top,top))))=join(composition(join(X1,top),complement(composition(top,top))),X0))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f3435,f52262])).
% 78.72/10.32 fof(f52264,plain,(
% 78.72/10.32 ![X0,X1]: (join(X0,composition(X1,complement(composition(top,top))))=join(composition(top,complement(composition(top,top))),X0))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f2569,f52263])).
% 78.72/10.32 fof(f52265,plain,(
% 78.72/10.32 ![X0,X1]: (join(X0,composition(X1,complement(composition(top,top))))=join(zero,X0))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f19701,f52264])).
% 78.72/10.32 fof(f52266,plain,(
% 78.72/10.32 ![X0,X1]: (join(X0,composition(X1,complement(composition(top,top))))=X0)),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f3435,f52265])).
% 78.72/10.32 fof(f52279,plain,(
% 78.72/10.32 ![X0,X1]: (composition(join(composition(X0,top),X1),complement(composition(top,top)))=composition(X0,zero))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f52266,f52087])).
% 78.72/10.32 fof(f52280,plain,(
% 78.72/10.32 ![X0]: (composition(top,complement(composition(top,top)))=join(composition(X0,complement(composition(top,top))),zero))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f2620,f52088])).
% 78.72/10.32 fof(f52281,plain,(
% 78.72/10.32 ![X0]: (zero=join(composition(X0,complement(composition(top,top))),zero))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f19701,f52280])).
% 78.72/10.32 fof(f52283,plain,(
% 78.72/10.32 ![X0]: (zero=composition(X0,zero))),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f52289,f52279])).
% 78.72/10.32 fof(f52289,plain,(
% 78.72/10.32 ![X0]: (zero=composition(X0,complement(composition(top,top))))),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f3430,f52281])).
% 78.72/10.32 fof(f52345,plain,(
% 78.72/10.32 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(meet(complement(composition(top,top)),converse(composition(X0,top))),zero))=zero)),
% 78.72/10.32 inference(backward_demodulation,[status(thm)],[f52283,f52197])).
% 78.72/10.32 fof(f52514,plain,(
% 78.72/10.32 ![X0]: (join(composition(complement(composition(top,top)),X0),zero)=zero)),
% 78.72/10.32 inference(forward_demodulation,[status(thm)],[f52283,f52345])).
% 72.05/10.48 fof(f52516,plain,(
% 72.05/10.48 ![X0]: (composition(top,zero)=composition(zero,X0))),
% 72.05/10.48 inference(backward_demodulation,[status(thm)],[f52518,f52096])).
% 72.05/10.48 fof(f52518,plain,(
% 72.05/10.48 ![X0]: (composition(complement(composition(top,top)),X0)=zero)),
% 72.05/10.48 inference(forward_demodulation,[status(thm)],[f3430,f52514])).
% 72.05/10.48 fof(f52803,plain,(
% 72.05/10.48 join(meet(sk1,sF1_fnc),composition(zero,meet(sk2,composition(converse(sF2_fnc),sk1))))=zero),
% 72.05/10.48 inference(backward_demodulation,[status(thm)],[f52814,f45225])).
% 72.05/10.48 fof(f52814,plain,(
% 72.05/10.48 ![X0]: (zero=composition(zero,X0))),
% 72.05/10.48 inference(forward_demodulation,[status(thm)],[f52283,f52516])).
% 72.05/10.48 fof(f52873,plain,(
% 72.05/10.48 join(meet(sk1,sF1_fnc),zero)=zero),
% 72.05/10.48 inference(forward_demodulation,[status(thm)],[f52814,f52803])).
% 72.05/10.48 fof(f52875,plain,(
% 72.05/10.48 meet(sk1,sF1_fnc)=zero),
% 72.05/10.48 inference(forward_demodulation,[status(thm)],[f3430,f52873])).
% 72.05/10.48 fof(f52888,plain,(
% 72.05/10.48 sk1=join(zero,complement(join(sF3_fnc,sF1_fnc)))),
% 72.05/10.48 inference(paramodulation,[status(thm)],[f52875,f969])).
% 72.05/10.48 fof(f52938,plain,(
% 72.05/10.48 sk1=complement(join(sF3_fnc,sF1_fnc))),
% 72.05/10.48 inference(forward_demodulation,[status(thm)],[f3435,f52888])).
% 72.05/10.48 fof(f52939,plain,(
% 72.05/10.48 sk1=complement(join(sF1_fnc,sF3_fnc))),
% 72.05/10.48 inference(forward_demodulation,[status(thm)],[f17625,f52938])).
% 72.05/10.48 fof(f52953,plain,(
% 72.05/10.48 sk1=complement(sF0_fnc)),
% 72.05/10.48 inference(forward_demodulation,[status(thm)],[f40,f52939])).
% 72.05/10.48 fof(f53075,plain,(
% 72.05/10.48 sF0_fnc=complement(sk1)),
% 72.05/10.48 inference(paramodulation,[status(thm)],[f52953,f2781])).
% 72.05/10.48 fof(f53148,plain,(
% 72.05/10.48 sF3_fnc=sF0_fnc),
% 72.05/10.48 inference(backward_demodulation,[status(thm)],[f53075,f39])).
% 72.05/10.48 fof(f53239,plain,(
% 72.05/10.48 $false),
% 72.05/10.48 inference(forward_subsumption_resolution,[status(thm)],[f53148,f41])).
% 72.05/10.48 % SZS output end CNFRefutation for theBenchmark.p
% 12.43/10.53 % Elapsed time: 10.153875 seconds
% 12.43/10.53 % CPU time: 80.231437 seconds
% 12.43/10.53 % Total memory used: 766.612 MB
% 12.43/10.53 % Net memory used: 751.091 MB
%------------------------------------------------------------------------------