%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL042-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 : n007.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 35.09s 4.95s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL042-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.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 04:05:51 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 35.09/4.95 % Refutation found
% 35.09/4.95 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 35.09/4.95 % SZS output start CNFRefutation for theBenchmark
% 35.09/4.95 fof(f1,axiom,(
% 35.09/4.95 (![A,B]: (join(A,B) = join(B,A) ))),
% 35.09/4.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.09/4.95 fof(f2,axiom,(
% 35.09/4.95 (![A,B,C]: (join(A,join(B,C)) = join(join(A,B),C) ))),
% 35.09/4.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.09/4.95 fof(f3,axiom,(
% 35.09/4.95 (![A,B]: (A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))) ))),
% 35.09/4.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.09/4.95 fof(f4,axiom,(
% 35.09/4.95 (![A,B]: (meet(A,B) = complement(join(complement(A),complement(B))) ))),
% 35.09/4.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.09/4.95 fof(f5,axiom,(
% 35.09/4.95 (![A,B,C]: (composition(A,composition(B,C)) = composition(composition(A,B),C) ))),
% 35.09/4.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.09/4.95 fof(f6,axiom,(
% 35.09/4.95 (![A]: (composition(A,one) = A ))),
% 35.09/4.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.09/4.95 fof(f7,axiom,(
% 35.09/4.95 (![A,B,C]: (composition(join(A,B),C) = join(composition(A,C),composition(B,C)) ))),
% 35.09/4.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.09/4.95 fof(f8,axiom,(
% 35.09/4.95 (![A]: (converse(converse(A)) = A ))),
% 35.09/4.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.09/4.95 fof(f9,axiom,(
% 35.09/4.95 (![A,B]: (converse(join(A,B)) = join(converse(A),converse(B)) ))),
% 35.09/4.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.09/4.95 fof(f10,axiom,(
% 35.09/4.95 (![A,B]: (converse(composition(A,B)) = composition(converse(B),converse(A)) ))),
% 35.09/4.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.09/4.95 fof(f11,axiom,(
% 35.09/4.95 (![A,B]: (join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B) ))),
% 35.09/4.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.09/4.95 fof(f12,axiom,(
% 35.09/4.95 (![A]: (top = join(A,complement(A)) ))),
% 35.09/4.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.09/4.95 fof(f13,axiom,(
% 35.09/4.95 (![A]: (zero = meet(A,complement(A)) ))),
% 35.09/4.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.09/4.95 fof(f14,axiom,(
% 35.09/4.95 (![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))) ))),
% 35.09/4.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.09/4.95 fof(f17,negated_conjecture,(
% 35.09/4.95 (![A]: (meet(composition(sk1,A),composition(sk1,complement(A))) = zero ))),
% 35.09/4.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.09/4.95 fof(f18,negated_conjecture,(
% 35.09/4.95 join(composition(converse(sk1),sk1),one) != one ),
% 35.09/4.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.09/4.95 fof(f19,plain,(
% 35.09/4.95 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 35.09/4.95 inference(cnf_transformation,[status(thm)],[f1])).
% 35.09/4.95 fof(f20,plain,(
% 35.09/4.95 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 35.09/4.95 inference(cnf_transformation,[status(thm)],[f2])).
% 35.09/4.95 fof(f21,plain,(
% 35.09/4.95 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 35.09/4.95 inference(cnf_transformation,[status(thm)],[f3])).
% 35.09/4.95 fof(f22,plain,(
% 35.09/4.95 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 35.09/4.95 inference(cnf_transformation,[status(thm)],[f4])).
% 35.09/4.95 fof(f23,plain,(
% 35.09/4.95 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 35.09/4.95 inference(cnf_transformation,[status(thm)],[f5])).
% 35.09/4.95 fof(f24,plain,(
% 35.09/4.95 ![X0]: (composition(X0,one)=X0)),
% 35.09/4.95 inference(cnf_transformation,[status(thm)],[f6])).
% 35.09/4.95 fof(f25,plain,(
% 35.09/4.95 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 35.09/4.95 inference(cnf_transformation,[status(thm)],[f7])).
% 35.09/4.95 fof(f26,plain,(
% 35.09/4.95 ![X0]: (converse(converse(X0))=X0)),
% 35.09/4.95 inference(cnf_transformation,[status(thm)],[f8])).
% 35.09/4.95 fof(f27,plain,(
% 35.09/4.95 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 35.09/4.95 inference(cnf_transformation,[status(thm)],[f9])).
% 35.09/4.95 fof(f28,plain,(
% 35.09/4.95 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 35.09/4.95 inference(cnf_transformation,[status(thm)],[f10])).
% 35.09/4.95 fof(f29,plain,(
% 35.09/4.95 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 35.99/4.95 inference(cnf_transformation,[status(thm)],[f11])).
% 35.99/4.95 fof(f30,plain,(
% 35.99/4.95 ![X0]: (top=join(X0,complement(X0)))),
% 35.99/4.95 inference(cnf_transformation,[status(thm)],[f12])).
% 35.99/4.95 fof(f31,plain,(
% 35.99/4.95 ![X0]: (zero=meet(X0,complement(X0)))),
% 35.99/4.95 inference(cnf_transformation,[status(thm)],[f13])).
% 35.99/4.95 fof(f32,plain,(
% 35.99/4.95 ![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))))),
% 35.99/4.95 inference(cnf_transformation,[status(thm)],[f14])).
% 35.99/4.95 fof(f35,plain,(
% 35.99/4.95 ![X0]: (meet(composition(sk1,X0),composition(sk1,complement(X0)))=zero)),
% 35.99/4.95 inference(cnf_transformation,[status(thm)],[f17])).
% 35.99/4.95 fof(f36,plain,(
% 35.99/4.95 ~join(composition(converse(sk1),sk1),one)=one),
% 35.99/4.95 inference(cnf_transformation,[status(thm)],[f18])).
% 35.99/4.95 fof(f37,definition,(
% 35.99/4.95 sF2_fnc=converse(sk1)),
% 35.99/4.95 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 35.99/4.95 fof(f38,definition,(
% 35.99/4.95 sF1_fnc=composition(sF2_fnc,sk1)),
% 35.99/4.95 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 35.99/4.95 fof(f39,definition,(
% 35.99/4.95 sF0_fnc=join(sF1_fnc,one)),
% 35.99/4.95 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 35.99/4.95 fof(f40,plain,(
% 35.99/4.95 ~sF0_fnc=one),
% 35.99/4.95 inference(definition_folding,[],[f36,f39,f38,f37])).
% 35.99/4.95 fof(f41,plain,(
% 35.99/4.95 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 35.99/4.95 inference(forward_demodulation,[status(thm)],[f19,f21])).
% 35.99/4.95 fof(f42,plain,(
% 35.99/4.95 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 35.99/4.95 inference(backward_demodulation,[status(thm)],[f22,f41])).
% 35.99/4.95 fof(f43,plain,(
% 35.99/4.95 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 35.99/4.95 inference(forward_demodulation,[status(thm)],[f19,f29])).
% 35.99/4.95 fof(f44,plain,(
% 35.99/4.95 sF0_fnc=join(one,sF1_fnc)),
% 35.99/4.95 inference(forward_demodulation,[status(thm)],[f19,f39])).
% 35.99/4.95 fof(f45,plain,(
% 35.99/4.95 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 35.99/4.95 inference(forward_demodulation,[status(thm)],[f19,f42])).
% 35.99/4.95 fof(f46,plain,(
% 35.99/4.95 meet(sk1,composition(sk1,complement(one)))=zero),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f24,f35])).
% 35.99/4.95 fof(f48,plain,(
% 35.99/4.95 converse(sF2_fnc)=sk1),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f37,f26])).
% 35.99/4.95 fof(f54,plain,(
% 35.99/4.95 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f19,f22])).
% 35.99/4.95 fof(f56,plain,(
% 35.99/4.95 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X0,X1),complement(X2))))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f22,f22])).
% 35.99/4.95 fof(f58,plain,(
% 35.99/4.95 ![X0,X1]: (zero=meet(join(complement(X0),complement(X1)),meet(X0,X1)))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f22,f31])).
% 35.99/4.95 fof(f60,plain,(
% 35.99/4.95 ![X0,X1]: (zero=complement(join(meet(X0,X1),complement(meet(X0,X1)))))),
% 35.99/4.95 inference(forward_demodulation,[status(thm)],[f56,f58])).
% 35.99/4.95 fof(f61,plain,(
% 35.99/4.95 zero=complement(top)),
% 35.99/4.95 inference(forward_demodulation,[status(thm)],[f30,f60])).
% 35.99/4.95 fof(f62,plain,(
% 35.99/4.95 ![X0]: (meet(X0,top)=complement(join(complement(X0),zero)))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f61,f22])).
% 35.99/4.95 fof(f63,plain,(
% 35.99/4.95 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f61,f22])).
% 35.99/4.95 fof(f66,plain,(
% 35.99/4.95 ![X0]: (meet(X0,top)=complement(join(zero,complement(X0))))),
% 35.99/4.95 inference(forward_demodulation,[status(thm)],[f19,f62])).
% 35.99/4.95 fof(f69,plain,(
% 35.99/4.95 ![X0]: (composition(sF2_fnc,composition(sk1,X0))=composition(sF1_fnc,X0))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f38,f23])).
% 35.99/4.95 fof(f70,plain,(
% 35.99/4.95 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f24,f23])).
% 35.99/4.95 fof(f84,plain,(
% 35.99/4.95 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f19,f20])).
% 35.99/4.95 fof(f88,plain,(
% 35.99/4.95 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X0),X2))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f19,f20])).
% 35.99/4.95 fof(f96,plain,(
% 35.99/4.95 ![X0]: (converse(composition(X0,sk1))=composition(sF2_fnc,converse(X0)))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f37,f28])).
% 35.99/4.95 fof(f97,plain,(
% 35.99/4.95 ![X0]: (converse(composition(sF2_fnc,X0))=composition(converse(X0),sk1))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f48,f28])).
% 35.99/4.95 fof(f98,plain,(
% 35.99/4.95 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f26,f28])).
% 35.99/4.95 fof(f108,plain,(
% 35.99/4.95 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X1,X2),composition(X0,X2)))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f19,f25])).
% 35.99/4.95 fof(f122,plain,(
% 35.99/4.95 ![X0,X1,X2,X3]: (join(composition(X0,X1),join(composition(X2,X1),X3))=join(composition(join(X0,X2),X1),X3))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f25,f20])).
% 35.99/4.95 fof(f135,plain,(
% 35.99/4.95 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f19,f27])).
% 35.99/4.95 fof(f138,plain,(
% 35.99/4.95 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f26,f27])).
% 35.99/4.95 fof(f140,plain,(
% 35.99/4.95 ![X0]: (converse(join(X0,sF2_fnc))=join(converse(X0),sk1))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f48,f27])).
% 35.99/4.95 fof(f142,plain,(
% 35.99/4.95 ![X0]: (converse(join(X0,sk1))=join(converse(X0),sF2_fnc))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f37,f27])).
% 35.99/4.95 fof(f146,plain,(
% 35.99/4.95 ![X0]: (converse(join(X0,sF2_fnc))=join(sk1,converse(X0)))),
% 35.99/4.95 inference(forward_demodulation,[status(thm)],[f19,f140])).
% 35.99/4.95 fof(f147,plain,(
% 35.99/4.95 ![X0]: (converse(join(X0,sk1))=join(sF2_fnc,converse(X0)))),
% 35.99/4.95 inference(forward_demodulation,[status(thm)],[f19,f142])).
% 35.99/4.95 fof(f153,plain,(
% 35.99/4.95 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f30,f20])).
% 35.99/4.95 fof(f219,plain,(
% 35.99/4.95 converse(composition(sF2_fnc,sk1))=composition(sF2_fnc,sk1)),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f48,f96])).
% 35.99/4.95 fof(f229,plain,(
% 35.99/4.95 converse(sF1_fnc)=composition(sF2_fnc,sk1)),
% 35.99/4.95 inference(forward_demodulation,[status(thm)],[f38,f219])).
% 35.99/4.95 fof(f230,plain,(
% 35.99/4.95 converse(sF1_fnc)=sF1_fnc),
% 35.99/4.95 inference(forward_demodulation,[status(thm)],[f38,f229])).
% 35.99/4.95 fof(f242,plain,(
% 35.99/4.95 ![X0]: (converse(join(X0,sF1_fnc))=join(converse(X0),sF1_fnc))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f230,f27])).
% 35.99/4.95 fof(f247,plain,(
% 35.99/4.95 ![X0]: (converse(join(X0,sF1_fnc))=join(sF1_fnc,converse(X0)))),
% 35.99/4.95 inference(forward_demodulation,[status(thm)],[f19,f242])).
% 35.99/4.95 fof(f293,plain,(
% 35.99/4.95 ![X0,X1]: (converse(join(X0,X1))=converse(join(X1,X0)))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f27,f135])).
% 35.99/4.95 fof(f304,plain,(
% 35.99/4.95 ![X0,X1]: (converse(join(converse(X0),X1))=join(converse(X1),X0))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f26,f135])).
% 35.99/4.95 fof(f314,plain,(
% 35.99/4.95 ![X0,X1]: (join(X0,join(X1,complement(join(X1,X0))))=top)),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f30,f88])).
% 35.99/4.95 fof(f359,plain,(
% 35.99/4.95 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f22,f54])).
% 35.99/4.95 fof(f367,plain,(
% 35.99/4.95 ![X0,X1,X2]: (meet(X0,join(complement(X1),complement(X2)))=complement(join(meet(X1,X2),complement(X0))))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f22,f54])).
% 35.99/4.95 fof(f374,plain,(
% 35.99/4.95 ![X0,X1]: (meet(top,join(complement(X0),complement(X1)))=complement(join(zero,meet(X1,X0))))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f54,f63])).
% 35.99/4.95 fof(f391,plain,(
% 35.99/4.95 ![X0,X1]: (complement(join(meet(X0,X1),complement(top)))=complement(join(zero,meet(X1,X0))))),
% 35.99/4.95 inference(forward_demodulation,[status(thm)],[f367,f374])).
% 35.99/4.95 fof(f392,plain,(
% 35.99/4.95 ![X0,X1]: (complement(join(complement(top),meet(X0,X1)))=complement(join(zero,meet(X1,X0))))),
% 35.99/4.95 inference(forward_demodulation,[status(thm)],[f19,f391])).
% 35.99/4.95 fof(f393,plain,(
% 35.99/4.95 ![X0,X1]: (complement(join(zero,meet(X0,X1)))=complement(join(zero,meet(X1,X0))))),
% 35.99/4.95 inference(forward_demodulation,[status(thm)],[f61,f392])).
% 35.99/4.95 fof(f408,plain,(
% 35.99/4.95 ![X0]: (join(zero,composition(converse(X0),complement(composition(X0,top))))=complement(top))),
% 35.99/4.95 inference(paramodulation,[status(thm)],[f61,f43])).
% 35.99/4.95 fof(f430,plain,(
% 35.99/4.95 ![X0]: (join(zero,composition(converse(X0),complement(composition(X0,top))))=zero)),
% 35.99/4.95 inference(forward_demodulation,[status(thm)],[f61,f408])).
% 35.99/4.96 fof(f457,plain,(
% 35.99/4.96 ![X0]: (join(meet(sF1_fnc,X0),composition(meet(sF2_fnc,composition(X0,converse(sk1))),meet(sk1,composition(converse(sF2_fnc),X0))))=composition(meet(sF2_fnc,composition(X0,converse(sk1))),meet(sk1,composition(converse(sF2_fnc),X0))))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f38,f32])).
% 35.99/4.96 fof(f469,plain,(
% 35.99/4.96 ![X0,X1,X2]: (join(meet(composition(X0,converse(X1)),X2),composition(meet(X0,composition(X2,X1)),meet(converse(X1),composition(converse(X0),X2))))=composition(meet(X0,composition(X2,converse(converse(X1)))),meet(converse(X1),composition(converse(X0),X2))))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f26,f32])).
% 35.99/4.96 fof(f513,plain,(
% 35.99/4.96 ![X0]: (join(meet(sF1_fnc,X0),composition(meet(sF2_fnc,composition(X0,sF2_fnc)),meet(sk1,composition(converse(sF2_fnc),X0))))=composition(meet(sF2_fnc,composition(X0,converse(sk1))),meet(sk1,composition(converse(sF2_fnc),X0))))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f37,f457])).
% 35.99/4.96 fof(f514,plain,(
% 35.99/4.96 ![X0]: (join(meet(sF1_fnc,X0),composition(meet(sF2_fnc,composition(X0,sF2_fnc)),meet(sk1,composition(sk1,X0))))=composition(meet(sF2_fnc,composition(X0,converse(sk1))),meet(sk1,composition(converse(sF2_fnc),X0))))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f48,f513])).
% 35.99/4.96 fof(f515,plain,(
% 35.99/4.96 ![X0]: (join(meet(sF1_fnc,X0),composition(meet(sF2_fnc,composition(X0,sF2_fnc)),meet(sk1,composition(sk1,X0))))=composition(meet(sF2_fnc,composition(X0,sF2_fnc)),meet(sk1,composition(converse(sF2_fnc),X0))))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f37,f514])).
% 35.99/4.96 fof(f516,plain,(
% 35.99/4.96 ![X0]: (join(meet(sF1_fnc,X0),composition(meet(sF2_fnc,composition(X0,sF2_fnc)),meet(sk1,composition(sk1,X0))))=composition(meet(sF2_fnc,composition(X0,sF2_fnc)),meet(sk1,composition(sk1,X0))))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f48,f515])).
% 35.99/4.96 fof(f532,plain,(
% 35.99/4.96 ![X0,X1,X2]: (join(meet(composition(X0,converse(X1)),X2),composition(meet(X0,composition(X2,X1)),meet(converse(X1),composition(converse(X0),X2))))=composition(meet(X0,composition(X2,X1)),meet(converse(X1),composition(converse(X0),X2))))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f26,f469])).
% 35.99/4.96 fof(f562,plain,(
% 35.99/4.96 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f31,f45])).
% 35.99/4.96 fof(f565,plain,(
% 35.99/4.96 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f54,f45])).
% 35.99/4.96 fof(f568,plain,(
% 35.99/4.96 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f30,f45])).
% 35.99/4.96 fof(f581,plain,(
% 35.99/4.96 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f54,f562])).
% 35.99/4.96 fof(f582,plain,(
% 35.99/4.96 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f19,f565])).
% 35.99/4.96 fof(f585,plain,(
% 35.99/4.96 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(X0)))))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f19,f568])).
% 35.99/4.96 fof(f586,plain,(
% 35.99/4.96 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f61,f585])).
% 35.99/4.96 fof(f715,plain,(
% 35.99/4.96 top=join(zero,meet(top,complement(zero)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f61,f586])).
% 35.99/4.96 fof(f738,plain,(
% 35.99/4.96 ![X0,X1]: (X0=join(meet(X1,X0),meet(complement(X1),X0)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f359,f582])).
% 35.99/4.96 fof(f740,plain,(
% 35.99/4.96 ![X0]: (X0=join(meet(top,X0),meet(X0,zero)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f61,f582])).
% 35.99/4.96 fof(f762,plain,(
% 35.99/4.96 ![X0]: (X0=join(meet(X0,top),meet(X0,zero)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f359,f740])).
% 35.99/4.96 fof(f801,plain,(
% 35.99/4.96 ![X0]: (X0=join(meet(X0,top),meet(zero,X0)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f359,f762])).
% 35.99/4.96 fof(f813,plain,(
% 35.99/4.96 complement(zero)=join(meet(complement(zero),top),zero)),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f31,f801])).
% 35.99/4.96 fof(f821,plain,(
% 35.99/4.96 complement(zero)=join(zero,meet(complement(zero),top))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f19,f813])).
% 35.99/4.96 fof(f822,plain,(
% 35.99/4.96 complement(zero)=join(zero,meet(top,complement(zero)))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f359,f821])).
% 35.99/4.96 fof(f824,plain,(
% 35.99/4.96 complement(zero)=top),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f715,f822])).
% 35.99/4.96 fof(f925,plain,(
% 35.99/4.96 ![X0]: (complement(complement(X0))=join(meet(X0,complement(complement(X0))),zero))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f31,f738])).
% 35.99/4.96 fof(f939,plain,(
% 35.99/4.96 ![X0]: (complement(complement(X0))=join(zero,meet(X0,complement(complement(X0)))))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f19,f925])).
% 35.99/4.96 fof(f945,plain,(
% 35.99/4.96 ![X0]: (complement(complement(X0))=X0)),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f586,f939])).
% 35.99/4.96 fof(f1104,plain,(
% 35.99/4.96 ![X0]: (complement(meet(X0,top))=join(zero,complement(X0)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f66,f945])).
% 35.99/4.96 fof(f1105,plain,(
% 35.99/4.96 ![X0,X1]: (complement(meet(X0,X1))=join(complement(X1),complement(X0)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f54,f945])).
% 35.99/4.96 fof(f1106,plain,(
% 35.99/4.96 ![X0,X1]: (complement(meet(X0,X1))=join(complement(X0),complement(X1)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f22,f945])).
% 35.99/4.96 fof(f1113,plain,(
% 35.99/4.96 ![X0,X1]: (meet(X0,complement(X1))=complement(join(X1,complement(X0))))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f945,f54])).
% 35.99/4.96 fof(f1117,plain,(
% 35.99/4.96 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),X1)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f945,f22])).
% 35.99/4.96 fof(f1118,plain,(
% 35.99/4.96 ![X0,X1]: (meet(complement(X0),X1)=complement(join(X0,complement(X1))))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f945,f22])).
% 35.99/4.96 fof(f1254,plain,(
% 35.99/4.96 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f30,f138])).
% 35.99/4.96 fof(f1309,plain,(
% 35.99/4.96 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f24,f98])).
% 35.99/4.96 fof(f1346,plain,(
% 35.99/4.96 ![X0]: (X0=composition(converse(one),X0))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f26,f1309])).
% 35.99/4.96 fof(f1382,plain,(
% 35.99/4.96 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f70,f1346])).
% 35.99/4.96 fof(f1383,plain,(
% 35.99/4.96 one=converse(one)),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f24,f1346])).
% 35.99/4.96 fof(f1384,plain,(
% 35.99/4.96 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1346,f43])).
% 35.99/4.96 fof(f1402,plain,(
% 35.99/4.96 ![X0,X1]: (composition(join(converse(one),X0),X1)=join(X1,composition(X0,X1)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1346,f25])).
% 35.99/4.96 fof(f1416,plain,(
% 35.99/4.96 ![X0]: (composition(one,X0)=X0)),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f1346,f1382])).
% 35.99/4.96 fof(f1420,plain,(
% 35.99/4.96 ![X0]: (complement(meet(X0,composition(one,X0)))=complement(X0))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f1106,f1384])).
% 35.99/4.96 fof(f1421,plain,(
% 35.99/4.96 ![X0]: (complement(meet(X0,X0))=complement(X0))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f1416,f1420])).
% 35.99/4.96 fof(f1472,plain,(
% 35.99/4.96 ![X0,X1]: (composition(join(one,X0),X1)=join(X1,composition(X0,X1)))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f1383,f1402])).
% 35.99/4.96 fof(f1536,plain,(
% 35.99/4.96 converse(join(one,sk1))=join(sF2_fnc,one)),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1383,f147])).
% 35.99/4.96 fof(f1538,plain,(
% 35.99/4.96 converse(join(one,sF2_fnc))=join(sk1,one)),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1383,f146])).
% 35.99/4.96 fof(f1545,plain,(
% 35.99/4.96 ![X0]: (converse(join(X0,one))=join(one,converse(X0)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1383,f135])).
% 35.99/4.96 fof(f1569,plain,(
% 35.99/4.96 converse(join(one,sk1))=join(one,sF2_fnc)),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f19,f1536])).
% 35.99/4.96 fof(f1572,plain,(
% 35.99/4.96 converse(join(one,sF2_fnc))=join(one,sk1)),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f19,f1538])).
% 35.99/4.96 fof(f1603,plain,(
% 35.99/4.96 ![X0]: (complement(complement(X0))=meet(X0,X0))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1421,f945])).
% 35.99/4.96 fof(f1613,plain,(
% 35.99/4.96 ![X0]: (X0=join(zero,X0))),
% 35.99/4.96 inference(backward_demodulation,[status(thm)],[f1617,f581])).
% 35.99/4.96 fof(f1617,plain,(
% 35.99/4.96 ![X0]: (X0=meet(X0,X0))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f945,f1603])).
% 35.99/4.96 fof(f1640,plain,(
% 35.99/4.96 ![X0]: (composition(converse(X0),complement(composition(X0,top)))=zero)),
% 35.99/4.96 inference(backward_demodulation,[status(thm)],[f1613,f430])).
% 35.99/4.96 fof(f1652,plain,(
% 35.99/4.96 ![X0,X1]: (complement(join(zero,meet(X0,X1)))=complement(meet(X1,X0)))),
% 35.99/4.96 inference(backward_demodulation,[status(thm)],[f1613,f393])).
% 35.99/4.96 fof(f1654,plain,(
% 35.99/4.96 ![X0]: (complement(meet(X0,top))=complement(X0))),
% 35.99/4.96 inference(backward_demodulation,[status(thm)],[f1613,f1104])).
% 35.99/4.96 fof(f1661,plain,(
% 35.99/4.96 ![X0,X1]: (complement(meet(X0,X1))=complement(meet(X1,X0)))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f1613,f1652])).
% 35.99/4.96 fof(f1681,plain,(
% 35.99/4.96 ![X0]: (X0=join(X0,zero))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f19,f1613])).
% 35.99/4.96 fof(f1700,plain,(
% 35.99/4.96 ![X0]: (converse(converse(X0))=join(X0,converse(zero)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1681,f138])).
% 35.99/4.96 fof(f1710,plain,(
% 35.99/4.96 ![X0]: (X0=join(X0,converse(zero)))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f26,f1700])).
% 35.99/4.96 fof(f1801,plain,(
% 35.99/4.96 zero=converse(zero)),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1613,f1710])).
% 35.99/4.96 fof(f1902,plain,(
% 35.99/4.96 ![X0]: (complement(complement(X0))=meet(X0,top))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1654,f945])).
% 35.99/4.96 fof(f1923,plain,(
% 35.99/4.96 ![X0]: (X0=meet(X0,top))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f945,f1902])).
% 35.99/4.96 fof(f2510,plain,(
% 35.99/4.96 converse(join(one,sF1_fnc))=join(sF1_fnc,one)),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1383,f247])).
% 35.99/4.96 fof(f2526,plain,(
% 35.99/4.96 converse(sF0_fnc)=join(sF1_fnc,one)),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f44,f2510])).
% 35.99/4.96 fof(f2527,plain,(
% 35.99/4.96 converse(sF0_fnc)=join(one,sF1_fnc)),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f19,f2526])).
% 35.99/4.96 fof(f2528,plain,(
% 35.99/4.96 converse(sF0_fnc)=sF0_fnc),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f44,f2527])).
% 35.99/4.96 fof(f2561,plain,(
% 35.99/4.96 converse(composition(sF2_fnc,sF0_fnc))=composition(sF0_fnc,sk1)),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f2528,f97])).
% 35.99/4.96 fof(f2634,plain,(
% 35.99/4.96 ![X0,X1]: (top=join(meet(X0,X1),complement(meet(X1,X0))))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1661,f30])).
% 35.99/4.96 fof(f4666,plain,(
% 35.99/4.96 ![X0]: (complement(meet(zero,X0))=join(complement(X0),top))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f824,f1105])).
% 35.99/4.96 fof(f4685,plain,(
% 35.99/4.96 ![X0]: (complement(meet(zero,X0))=join(top,complement(X0)))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f19,f4666])).
% 35.99/4.96 fof(f4711,plain,(
% 35.99/4.96 ![X0,X1]: (join(X0,complement(meet(X0,X1)))=join(top,complement(X1)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1106,f153])).
% 35.99/4.96 fof(f4729,plain,(
% 35.99/4.96 ![X0,X1]: (join(X0,complement(meet(X0,X1)))=complement(meet(zero,X1)))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f4685,f4711])).
% 35.99/4.96 fof(f5875,plain,(
% 35.99/4.96 ![X0,X1]: (meet(complement(X0),complement(X1))=complement(join(X0,X1)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f945,f1117])).
% 35.99/4.96 fof(f6079,plain,(
% 35.99/4.96 ![X0]: (join(X0,converse(top))=join(top,converse(complement(converse(complement(X0))))))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1254,f153])).
% 35.99/4.96 fof(f6083,plain,(
% 35.99/4.96 ![X0,X1]: (join(X0,join(converse(complement(converse(X0))),X1))=join(X1,converse(top)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1254,f84])).
% 35.99/4.96 fof(f6086,plain,(
% 35.99/4.96 ![X0,X1]: (join(X0,join(converse(complement(converse(X0))),X1))=join(converse(top),X1))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1254,f20])).
% 35.99/4.96 fof(f7585,plain,(
% 35.99/4.96 composition(join(one,sk1),complement(composition(join(one,sF2_fnc),top)))=zero),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1572,f1640])).
% 35.99/4.96 fof(f7586,plain,(
% 35.99/4.96 composition(join(one,sF2_fnc),complement(composition(join(one,sk1),top)))=zero),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1569,f1640])).
% 35.99/4.96 fof(f7611,plain,(
% 35.99/4.96 composition(sk1,complement(composition(sF2_fnc,top)))=zero),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f48,f1640])).
% 35.99/4.96 fof(f7642,plain,(
% 35.99/4.96 composition(join(one,sk1),complement(join(top,composition(sF2_fnc,top))))=zero),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f1472,f7585])).
% 35.99/4.96 fof(f7643,plain,(
% 35.99/4.96 composition(join(one,sF2_fnc),complement(join(top,composition(sk1,top))))=zero),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f1472,f7586])).
% 35.99/4.96 fof(f9309,plain,(
% 35.99/4.96 join(meet(sF1_fnc,complement(one)),composition(meet(sF2_fnc,composition(complement(one),sF2_fnc)),zero))=composition(meet(sF2_fnc,composition(complement(one),sF2_fnc)),meet(sk1,composition(sk1,complement(one))))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f46,f516])).
% 35.99/4.96 fof(f9344,plain,(
% 35.99/4.96 join(meet(sF1_fnc,complement(one)),composition(meet(sF2_fnc,composition(complement(one),sF2_fnc)),zero))=composition(meet(sF2_fnc,composition(complement(one),sF2_fnc)),zero)),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f46,f9309])).
% 35.99/4.96 fof(f12233,plain,(
% 35.99/4.96 composition(composition(sF0_fnc,sk1),complement(composition(composition(sF2_fnc,sF0_fnc),top)))=zero),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f2561,f1640])).
% 35.99/4.96 fof(f12303,plain,(
% 35.99/4.96 composition(sF0_fnc,composition(sk1,complement(composition(composition(sF2_fnc,sF0_fnc),top))))=zero),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f23,f12233])).
% 35.99/4.96 fof(f12304,plain,(
% 35.99/4.96 composition(sF0_fnc,composition(sk1,complement(composition(sF2_fnc,composition(sF0_fnc,top)))))=zero),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f23,f12303])).
% 35.99/4.96 fof(f12833,plain,(
% 35.99/4.96 ![X0]: (top=join(X0,complement(meet(X0,X0))))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f1617,f2634])).
% 35.99/4.96 fof(f12896,plain,(
% 35.99/4.96 ![X0]: (top=join(top,complement(X0)))),
% 35.99/4.96 inference(backward_demodulation,[status(thm)],[f12897,f4685])).
% 35.99/4.96 fof(f12897,plain,(
% 35.99/4.96 ![X0]: (top=complement(meet(zero,X0)))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f4729,f12833])).
% 35.99/4.96 fof(f12962,plain,(
% 35.99/4.96 ![X0]: (top=join(top,X0))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f945,f12896])).
% 35.99/4.96 fof(f12966,plain,(
% 35.99/4.96 ![X0]: (join(X0,top)=top)),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f12896,f314])).
% 35.99/4.96 fof(f12968,plain,(
% 35.99/4.96 ![X0]: (meet(complement(top),X0)=complement(top))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f12896,f1118])).
% 35.99/4.96 fof(f12969,plain,(
% 35.99/4.96 ![X0]: (meet(X0,complement(top))=complement(top))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f12896,f1113])).
% 35.99/4.96 fof(f12997,plain,(
% 35.99/4.96 ![X0]: (join(X0,converse(top))=top)),
% 35.99/4.96 inference(backward_demodulation,[status(thm)],[f12962,f6079])).
% 35.99/4.96 fof(f13003,plain,(
% 35.99/4.96 composition(join(one,sF2_fnc),complement(top))=zero),
% 35.99/4.96 inference(backward_demodulation,[status(thm)],[f12962,f7643])).
% 35.99/4.96 fof(f13004,plain,(
% 35.99/4.96 composition(join(one,sk1),complement(top))=zero),
% 35.99/4.96 inference(backward_demodulation,[status(thm)],[f12962,f7642])).
% 35.99/4.96 fof(f13106,plain,(
% 35.99/4.96 ![X0]: (meet(zero,X0)=complement(top))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f61,f12968])).
% 35.99/4.96 fof(f13173,plain,(
% 35.99/4.96 ![X0]: (meet(zero,X0)=zero)),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f61,f13106])).
% 35.99/4.96 fof(f13174,plain,(
% 35.99/4.96 ![X0]: (meet(X0,zero)=complement(top))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f61,f12969])).
% 35.99/4.96 fof(f13184,plain,(
% 35.99/4.96 ![X0]: (meet(X0,zero)=zero)),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f61,f13174])).
% 35.99/4.96 fof(f13199,plain,(
% 35.99/4.96 ![X0,X1]: (join(X0,join(converse(complement(converse(X0))),X1))=top)),
% 35.99/4.96 inference(backward_demodulation,[status(thm)],[f12997,f6083])).
% 35.99/4.96 fof(f13200,plain,(
% 35.99/4.96 composition(join(one,sF2_fnc),zero)=zero),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f61,f13003])).
% 35.99/4.96 fof(f13201,plain,(
% 35.99/4.96 join(zero,composition(sF2_fnc,zero))=zero),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f1472,f13200])).
% 35.99/4.96 fof(f13257,plain,(
% 35.99/4.96 composition(sF2_fnc,zero)=zero),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f1613,f13201])).
% 35.99/4.96 fof(f13258,plain,(
% 35.99/4.96 composition(join(one,sk1),zero)=zero),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f61,f13004])).
% 35.99/4.96 fof(f13259,plain,(
% 35.99/4.96 join(zero,composition(sk1,zero))=zero),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f1472,f13258])).
% 35.99/4.96 fof(f13308,plain,(
% 35.99/4.96 composition(sk1,zero)=zero),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f1613,f13259])).
% 35.99/4.96 fof(f13429,plain,(
% 35.99/4.96 ![X0]: (top=join(converse(top),X0))),
% 35.99/4.96 inference(backward_demodulation,[status(thm)],[f13199,f6086])).
% 35.99/4.96 fof(f13864,plain,(
% 35.99/4.96 ![X0]: (converse(top)=join(converse(top),X0))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f12966,f304])).
% 35.99/4.96 fof(f13907,plain,(
% 35.99/4.96 converse(top)=top),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f13429,f13864])).
% 35.99/4.96 fof(f14507,plain,(
% 35.99/4.96 composition(top,complement(composition(top,top)))=zero),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f13907,f1640])).
% 35.99/4.96 fof(f14641,plain,(
% 35.99/4.96 composition(sF2_fnc,zero)=composition(sF1_fnc,zero)),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f13308,f69])).
% 35.99/4.96 fof(f14717,plain,(
% 35.99/4.96 zero=composition(sF1_fnc,zero)),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f13257,f14641])).
% 35.99/4.96 fof(f14958,plain,(
% 35.99/4.96 join(complement(zero),composition(converse(sF1_fnc),complement(zero)))=complement(zero)),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f14717,f43])).
% 35.99/4.96 fof(f15041,plain,(
% 35.99/4.96 composition(join(one,converse(sF1_fnc)),complement(zero))=complement(zero)),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f1472,f14958])).
% 35.99/4.96 fof(f15042,plain,(
% 35.99/4.96 composition(converse(join(sF1_fnc,one)),complement(zero))=complement(zero)),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f1545,f15041])).
% 35.99/4.96 fof(f15043,plain,(
% 35.99/4.96 composition(converse(join(one,sF1_fnc)),complement(zero))=complement(zero)),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f293,f15042])).
% 35.99/4.96 fof(f15044,plain,(
% 35.99/4.96 composition(converse(sF0_fnc),complement(zero))=complement(zero)),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f44,f15043])).
% 35.99/4.96 fof(f15045,plain,(
% 35.99/4.96 composition(sF0_fnc,complement(zero))=complement(zero)),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f2528,f15044])).
% 35.99/4.96 fof(f15046,plain,(
% 35.99/4.96 composition(sF0_fnc,top)=complement(zero)),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f824,f15045])).
% 35.99/4.96 fof(f15049,plain,(
% 35.99/4.96 composition(sF0_fnc,composition(sk1,complement(composition(sF2_fnc,top))))=zero),
% 35.99/4.96 inference(backward_demodulation,[status(thm)],[f15052,f12304])).
% 35.99/4.96 fof(f15052,plain,(
% 35.99/4.96 composition(sF0_fnc,top)=top),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f824,f15046])).
% 35.99/4.96 fof(f15081,plain,(
% 35.99/4.96 composition(sF0_fnc,zero)=zero),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f7611,f15049])).
% 35.99/4.96 fof(f17638,plain,(
% 35.99/4.96 ![X0]: (composition(join(X0,sF0_fnc),top)=join(top,composition(X0,top)))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f15052,f108])).
% 35.99/4.96 fof(f17800,plain,(
% 35.99/4.96 ![X0]: (composition(join(X0,sF0_fnc),top)=top)),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f12962,f17638])).
% 35.99/4.96 fof(f17833,plain,(
% 35.99/4.96 composition(top,top)=top),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f12962,f17800])).
% 35.99/4.96 fof(f17875,plain,(
% 35.99/4.96 composition(top,complement(top))=zero),
% 35.99/4.96 inference(backward_demodulation,[status(thm)],[f17833,f14507])).
% 35.99/4.96 fof(f18021,plain,(
% 35.99/4.96 composition(top,zero)=zero),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f61,f17875])).
% 35.99/4.96 fof(f18034,plain,(
% 35.99/4.96 ![X0]: (join(meet(composition(X0,converse(zero)),top),composition(meet(X0,zero),meet(converse(zero),composition(converse(X0),top))))=composition(meet(X0,composition(top,zero)),meet(converse(zero),composition(converse(X0),top))))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f18021,f532])).
% 35.99/4.96 fof(f18050,plain,(
% 35.99/4.96 ![X0,X1]: (join(composition(X0,zero),join(zero,X1))=join(composition(join(X0,top),zero),X1))),
% 35.99/4.96 inference(paramodulation,[status(thm)],[f18021,f122])).
% 35.99/4.96 fof(f18065,plain,(
% 35.99/4.96 ![X0]: (join(composition(X0,converse(zero)),composition(meet(X0,zero),meet(converse(zero),composition(converse(X0),top))))=composition(meet(X0,composition(top,zero)),meet(converse(zero),composition(converse(X0),top))))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f1923,f18034])).
% 35.99/4.96 fof(f18066,plain,(
% 35.99/4.96 ![X0]: (join(composition(X0,zero),composition(meet(X0,zero),meet(converse(zero),composition(converse(X0),top))))=composition(meet(X0,composition(top,zero)),meet(converse(zero),composition(converse(X0),top))))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f1801,f18065])).
% 35.99/4.96 fof(f18067,plain,(
% 35.99/4.96 ![X0]: (join(composition(X0,zero),composition(zero,meet(converse(zero),composition(converse(X0),top))))=composition(meet(X0,composition(top,zero)),meet(converse(zero),composition(converse(X0),top))))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f13184,f18066])).
% 35.99/4.96 fof(f18068,plain,(
% 35.99/4.96 ![X0]: (join(composition(X0,zero),composition(zero,meet(zero,composition(converse(X0),top))))=composition(meet(X0,composition(top,zero)),meet(converse(zero),composition(converse(X0),top))))),
% 35.99/4.96 inference(forward_demodulation,[status(thm)],[f1801,f18067])).
% 35.99/4.96 fof(f18069,plain,(
% 35.99/4.96 ![X0]: (join(composition(X0,zero),composition(zero,zero))=composition(meet(X0,composition(top,zero)),meet(converse(zero),composition(converse(X0),top))))),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f13173,f18068])).
% 29.40/5.02 fof(f18070,plain,(
% 29.40/5.02 ![X0]: (composition(join(zero,X0),zero)=composition(meet(X0,composition(top,zero)),meet(converse(zero),composition(converse(X0),top))))),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f108,f18069])).
% 29.40/5.02 fof(f18071,plain,(
% 29.40/5.02 ![X0]: (composition(X0,zero)=composition(meet(X0,composition(top,zero)),meet(converse(zero),composition(converse(X0),top))))),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f1613,f18070])).
% 29.40/5.02 fof(f18072,plain,(
% 29.40/5.02 ![X0]: (composition(X0,zero)=composition(meet(X0,zero),meet(converse(zero),composition(converse(X0),top))))),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f18021,f18071])).
% 29.40/5.02 fof(f18073,plain,(
% 29.40/5.02 ![X0]: (composition(X0,zero)=composition(zero,meet(converse(zero),composition(converse(X0),top))))),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f13184,f18072])).
% 29.40/5.02 fof(f18074,plain,(
% 29.40/5.02 ![X0]: (composition(X0,zero)=composition(zero,meet(zero,composition(converse(X0),top))))),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f1801,f18073])).
% 29.40/5.02 fof(f18075,plain,(
% 29.40/5.02 composition(zero,zero)=zero),
% 29.40/5.02 inference(backward_demodulation,[status(thm)],[f18134,f15081])).
% 29.40/5.02 fof(f18115,plain,(
% 29.40/5.02 join(meet(sF1_fnc,complement(one)),composition(meet(sF2_fnc,composition(complement(one),sF2_fnc)),zero))=composition(zero,zero)),
% 29.40/5.02 inference(backward_demodulation,[status(thm)],[f18134,f9344])).
% 29.40/5.02 fof(f18134,plain,(
% 29.40/5.02 ![X0]: (composition(X0,zero)=composition(zero,zero))),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f13173,f18074])).
% 29.40/5.02 fof(f18228,plain,(
% 29.40/5.02 ![X0,X1]: (join(zero,join(X0,composition(X1,zero)))=join(composition(join(X1,top),zero),X0))),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f84,f18050])).
% 29.40/5.02 fof(f18229,plain,(
% 29.40/5.02 ![X0,X1]: (join(X0,composition(X1,zero))=join(composition(join(X1,top),zero),X0))),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f1613,f18228])).
% 29.40/5.02 fof(f18231,plain,(
% 29.40/5.02 ![X0,X1]: (join(X0,composition(X1,zero))=join(composition(zero,zero),X0))),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f18134,f18229])).
% 29.40/5.02 fof(f18396,plain,(
% 29.40/5.02 join(composition(zero,zero),meet(sF1_fnc,complement(one)))=composition(zero,zero)),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f18231,f18115])).
% 29.40/5.02 fof(f18397,plain,(
% 29.40/5.02 join(zero,meet(sF1_fnc,complement(one)))=composition(zero,zero)),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f18075,f18396])).
% 29.40/5.02 fof(f18398,plain,(
% 29.40/5.02 meet(sF1_fnc,complement(one))=composition(zero,zero)),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f1613,f18397])).
% 29.40/5.02 fof(f18399,plain,(
% 29.40/5.02 meet(sF1_fnc,complement(one))=zero),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f18075,f18398])).
% 29.40/5.02 fof(f19172,plain,(
% 29.40/5.02 complement(one)=join(zero,meet(complement(sF1_fnc),complement(one)))),
% 29.40/5.02 inference(paramodulation,[status(thm)],[f18399,f738])).
% 29.40/5.02 fof(f19198,plain,(
% 29.40/5.02 complement(one)=meet(complement(sF1_fnc),complement(one))),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f1613,f19172])).
% 29.40/5.02 fof(f19199,plain,(
% 29.40/5.02 complement(one)=meet(complement(one),complement(sF1_fnc))),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f359,f19198])).
% 29.40/5.02 fof(f19200,plain,(
% 29.40/5.02 complement(one)=complement(join(one,sF1_fnc))),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f5875,f19199])).
% 29.40/5.02 fof(f19206,plain,(
% 29.40/5.02 complement(one)=complement(sF0_fnc)),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f44,f19200])).
% 29.40/5.02 fof(f19371,plain,(
% 29.40/5.02 complement(complement(one))=sF0_fnc),
% 29.40/5.02 inference(paramodulation,[status(thm)],[f19206,f945])).
% 29.40/5.02 fof(f19404,plain,(
% 29.40/5.02 one=sF0_fnc),
% 29.40/5.02 inference(forward_demodulation,[status(thm)],[f945,f19371])).
% 29.40/5.02 fof(f19405,plain,(
% 29.40/5.02 $false),
% 29.40/5.02 inference(forward_subsumption_resolution,[status(thm)],[f19404,f40])).
% 29.40/5.02 % SZS output end CNFRefutation for theBenchmark.p
% 29.40/5.09 % Elapsed time: 4.709727 seconds
% 29.40/5.09 % CPU time: 36.902067 seconds
% 29.40/5.09 % Total memory used: 453.765 MB
% 29.40/5.09 % Net memory used: 447.162 MB
%------------------------------------------------------------------------------