%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL050-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:46 PM UTC 2026
% Result : Unsatisfiable 3.17s 0.82s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL050-1 : 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.10/0.36 % Computer : n004.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 04:08:49 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 3.17/0.82 % Refutation found
% 3.17/0.82 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 3.17/0.82 % SZS output start CNFRefutation for theBenchmark
% 3.17/0.82 fof(f1,axiom,(
% 3.17/0.82 (![A,B]: (join(A,B) = join(B,A) ))),
% 3.17/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.17/0.82 fof(f2,axiom,(
% 3.17/0.82 (![A,B,C]: (join(A,join(B,C)) = join(join(A,B),C) ))),
% 3.17/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.17/0.82 fof(f3,axiom,(
% 3.17/0.82 (![A,B]: (A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))) ))),
% 3.17/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.17/0.82 fof(f4,axiom,(
% 3.17/0.82 (![A,B]: (meet(A,B) = complement(join(complement(A),complement(B))) ))),
% 3.17/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.17/0.82 fof(f5,axiom,(
% 3.17/0.82 (![A,B,C]: (composition(A,composition(B,C)) = composition(composition(A,B),C) ))),
% 3.17/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.17/0.82 fof(f6,axiom,(
% 3.17/0.82 (![A]: (composition(A,one) = A ))),
% 3.17/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.17/0.82 fof(f7,axiom,(
% 3.17/0.82 (![A,B,C]: (composition(join(A,B),C) = join(composition(A,C),composition(B,C)) ))),
% 3.17/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.17/0.82 fof(f8,axiom,(
% 3.17/0.82 (![A]: (converse(converse(A)) = A ))),
% 3.17/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.17/0.82 fof(f9,axiom,(
% 3.17/0.82 (![A,B]: (converse(join(A,B)) = join(converse(A),converse(B)) ))),
% 3.17/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.17/0.82 fof(f10,axiom,(
% 3.17/0.82 (![A,B]: (converse(composition(A,B)) = composition(converse(B),converse(A)) ))),
% 3.17/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.17/0.82 fof(f11,axiom,(
% 3.17/0.82 (![A,B]: (join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B) ))),
% 3.17/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.17/0.82 fof(f12,axiom,(
% 3.17/0.82 (![A]: (top = join(A,complement(A)) ))),
% 3.17/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.17/0.82 fof(f13,axiom,(
% 3.17/0.82 (![A]: (zero = meet(A,complement(A)) ))),
% 3.17/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.17/0.82 fof(f14,negated_conjecture,(
% 3.17/0.82 complement(composition(sk1,top)) != composition(complement(composition(sk1,top)),top) ),
% 3.17/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.17/0.82 fof(f15,plain,(
% 3.17/0.82 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 3.17/0.82 inference(cnf_transformation,[status(thm)],[f1])).
% 3.17/0.82 fof(f16,plain,(
% 3.17/0.82 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 3.17/0.82 inference(cnf_transformation,[status(thm)],[f2])).
% 3.17/0.82 fof(f17,plain,(
% 3.17/0.82 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 3.17/0.82 inference(cnf_transformation,[status(thm)],[f3])).
% 3.17/0.82 fof(f18,plain,(
% 3.17/0.82 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 3.17/0.82 inference(cnf_transformation,[status(thm)],[f4])).
% 3.17/0.82 fof(f19,plain,(
% 3.17/0.82 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 3.17/0.82 inference(cnf_transformation,[status(thm)],[f5])).
% 3.17/0.82 fof(f20,plain,(
% 3.17/0.82 ![X0]: (composition(X0,one)=X0)),
% 3.17/0.82 inference(cnf_transformation,[status(thm)],[f6])).
% 3.17/0.82 fof(f21,plain,(
% 3.17/0.82 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 3.17/0.82 inference(cnf_transformation,[status(thm)],[f7])).
% 3.17/0.82 fof(f22,plain,(
% 3.17/0.82 ![X0]: (converse(converse(X0))=X0)),
% 3.17/0.82 inference(cnf_transformation,[status(thm)],[f8])).
% 3.17/0.82 fof(f23,plain,(
% 3.17/0.82 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 3.17/0.82 inference(cnf_transformation,[status(thm)],[f9])).
% 3.17/0.82 fof(f24,plain,(
% 3.17/0.82 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 3.17/0.82 inference(cnf_transformation,[status(thm)],[f10])).
% 3.17/0.82 fof(f25,plain,(
% 3.17/0.82 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 3.17/0.82 inference(cnf_transformation,[status(thm)],[f11])).
% 3.17/0.82 fof(f26,plain,(
% 3.17/0.82 ![X0]: (top=join(X0,complement(X0)))),
% 3.17/0.82 inference(cnf_transformation,[status(thm)],[f12])).
% 3.17/0.82 fof(f27,plain,(
% 3.17/0.82 ![X0]: (zero=meet(X0,complement(X0)))),
% 3.17/0.82 inference(cnf_transformation,[status(thm)],[f13])).
% 3.17/0.82 fof(f28,plain,(
% 3.17/0.82 ~complement(composition(sk1,top))=composition(complement(composition(sk1,top)),top)),
% 3.17/0.82 inference(cnf_transformation,[status(thm)],[f14])).
% 3.17/0.82 fof(f29,definition,(
% 3.17/0.82 sF1_fnc=composition(sk1,top)),
% 3.17/0.82 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 3.17/0.82 fof(f30,definition,(
% 3.17/0.82 sF0_fnc=complement(sF1_fnc)),
% 3.17/0.82 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 3.17/0.82 fof(f31,definition,(
% 3.17/0.82 sF3_fnc=complement(sF1_fnc)),
% 3.17/0.82 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 3.17/0.82 fof(f32,definition,(
% 3.17/0.82 sF2_fnc=composition(sF3_fnc,top)),
% 3.17/0.82 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 3.17/0.82 fof(f33,plain,(
% 3.17/0.82 ~sF0_fnc=sF2_fnc),
% 3.17/0.82 inference(definition_folding,[],[f28,f32,f31,f30,f29])).
% 3.17/0.82 fof(f34,plain,(
% 3.17/0.82 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f17])).
% 3.17/0.82 fof(f35,plain,(
% 3.17/0.82 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f18,f34])).
% 3.17/0.82 fof(f36,plain,(
% 3.17/0.82 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f25])).
% 3.17/0.82 fof(f37,plain,(
% 3.17/0.82 sF3_fnc=sF0_fnc),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f30,f31])).
% 3.17/0.82 fof(f38,plain,(
% 3.17/0.82 sF2_fnc=composition(sF0_fnc,top)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f37,f32])).
% 3.17/0.82 fof(f39,plain,(
% 3.17/0.82 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f35])).
% 3.17/0.82 fof(f40,plain,(
% 3.17/0.82 top=join(sF1_fnc,sF0_fnc)),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f30,f26])).
% 3.17/0.82 fof(f41,plain,(
% 3.17/0.82 top=join(sF0_fnc,sF1_fnc)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f40])).
% 3.17/0.82 fof(f44,plain,(
% 3.17/0.82 ![X0]: (composition(sk1,composition(top,X0))=composition(sF1_fnc,X0))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f29,f19])).
% 3.17/0.82 fof(f54,plain,(
% 3.17/0.82 ![X0]: (sF1_fnc=join(meet(sF1_fnc,X0),complement(join(sF0_fnc,X0))))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f30,f39])).
% 3.17/0.82 fof(f73,plain,(
% 3.17/0.82 ![X0]: (composition(join(sF0_fnc,X0),top)=join(sF2_fnc,composition(X0,top)))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f38,f21])).
% 3.17/0.82 fof(f78,plain,(
% 3.17/0.82 ![X0]: (composition(join(X0,sF0_fnc),top)=join(composition(X0,top),sF2_fnc))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f38,f21])).
% 3.17/0.82 fof(f80,plain,(
% 3.17/0.82 ![X0]: (composition(join(X0,sk1),top)=join(composition(X0,top),sF1_fnc))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f29,f21])).
% 3.17/0.82 fof(f87,plain,(
% 3.17/0.82 ![X0]: (composition(join(X0,sF0_fnc),top)=join(sF2_fnc,composition(X0,top)))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f78])).
% 3.17/0.82 fof(f92,plain,(
% 3.17/0.82 ![X0]: (composition(join(X0,sk1),top)=join(sF1_fnc,composition(X0,top)))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f80])).
% 3.17/0.82 fof(f100,plain,(
% 3.17/0.82 composition(join(sF0_fnc,sF0_fnc),top)=join(sF2_fnc,sF2_fnc)),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f38,f73])).
% 3.17/0.82 fof(f148,plain,(
% 3.17/0.82 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f20,f19])).
% 3.17/0.82 fof(f155,plain,(
% 3.17/0.82 zero=meet(sF1_fnc,sF0_fnc)),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f30,f27])).
% 3.17/0.82 fof(f192,plain,(
% 3.17/0.82 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X1,X2),composition(X0,X2)))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f21,f15])).
% 3.17/0.82 fof(f201,plain,(
% 3.17/0.82 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(X1,complement(X0)))))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f15,f39])).
% 3.17/0.82 fof(f209,plain,(
% 3.17/0.82 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f22,f23])).
% 3.17/0.82 fof(f214,plain,(
% 3.17/0.82 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f22,f24])).
% 3.17/0.82 fof(f228,plain,(
% 3.17/0.82 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f26,f18])).
% 3.17/0.82 fof(f229,plain,(
% 3.17/0.82 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f15,f18])).
% 3.17/0.82 fof(f235,plain,(
% 3.17/0.82 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f18,f39])).
% 3.17/0.82 fof(f238,plain,(
% 3.17/0.82 ![X0,X1,X2]: (join(complement(X0),complement(X1))=join(meet(join(complement(X0),complement(X1)),X2),complement(join(meet(X0,X1),X2))))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f18,f39])).
% 3.17/0.82 fof(f245,plain,(
% 3.17/0.82 zero=complement(top)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f27,f228])).
% 3.17/0.82 fof(f247,plain,(
% 3.17/0.82 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f235])).
% 3.17/0.82 fof(f249,plain,(
% 3.17/0.82 ![X0,X1,X2]: (join(complement(X0),complement(X1))=join(complement(join(meet(X0,X1),X2)),meet(join(complement(X0),complement(X1)),X2)))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f238])).
% 3.17/0.82 fof(f251,plain,(
% 3.17/0.82 ![X0]: (meet(X0,top)=complement(join(complement(X0),zero)))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f245,f18])).
% 3.17/0.82 fof(f252,plain,(
% 3.17/0.82 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f245,f18])).
% 3.17/0.82 fof(f255,plain,(
% 3.17/0.82 top=join(top,zero)),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f245,f26])).
% 3.17/0.82 fof(f256,plain,(
% 3.17/0.82 ![X0]: (meet(X0,top)=complement(join(zero,complement(X0))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f251])).
% 3.17/0.82 fof(f257,plain,(
% 3.17/0.82 top=join(zero,top)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f255])).
% 3.17/0.82 fof(f277,plain,(
% 3.17/0.82 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f15,f16])).
% 3.17/0.82 fof(f296,plain,(
% 3.17/0.82 ![X0]: (join(sF0_fnc,join(sF1_fnc,X0))=join(top,X0))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f41,f16])).
% 3.17/0.82 fof(f297,plain,(
% 3.17/0.82 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f26,f16])).
% 3.17/0.82 fof(f309,plain,(
% 3.17/0.82 ![X0]: (join(sF0_fnc,composition(converse(X0),complement(composition(X0,sF1_fnc))))=complement(sF1_fnc))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f30,f36])).
% 3.17/0.82 fof(f323,plain,(
% 3.17/0.82 ![X0]: (join(sF0_fnc,composition(converse(X0),complement(composition(X0,sF1_fnc))))=sF0_fnc)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f30,f309])).
% 3.17/0.82 fof(f440,plain,(
% 3.17/0.82 meet(top,top)=complement(join(zero,zero))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f245,f256])).
% 3.17/0.82 fof(f542,plain,(
% 3.17/0.82 ![X0]: (meet(top,X0)=meet(X0,top))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f256,f252])).
% 3.17/0.82 fof(f551,plain,(
% 3.17/0.82 ![X0,X1]: (meet(top,join(complement(X0),complement(X1)))=complement(join(zero,meet(X0,X1))))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f18,f252])).
% 3.17/0.82 fof(f593,plain,(
% 3.17/0.82 ![X0]: (top=join(meet(X0,top),meet(top,complement(X0))))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f542,f247])).
% 3.17/0.82 fof(f598,plain,(
% 3.17/0.82 ![X0]: (X0=join(meet(top,X0),complement(join(complement(X0),top))))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f542,f39])).
% 3.17/0.82 fof(f603,plain,(
% 3.17/0.82 ![X0]: (X0=join(meet(top,X0),complement(join(top,complement(X0)))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f598])).
% 3.17/0.82 fof(f636,plain,(
% 3.17/0.82 ![X0]: (join(sF0_fnc,composition(join(X0,sk1),top))=join(top,composition(X0,top)))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f92,f296])).
% 3.17/0.82 fof(f640,plain,(
% 3.17/0.82 ![X0,X1,X2]: (composition(join(X0,X1),X2)=composition(join(X1,X0),X2))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f21,f192])).
% 3.17/0.82 fof(f752,plain,(
% 3.17/0.82 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f20,f214])).
% 3.17/0.82 fof(f771,plain,(
% 3.17/0.82 ![X0]: (X0=composition(converse(one),X0))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f22,f752])).
% 3.17/0.82 fof(f783,plain,(
% 3.17/0.82 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f148,f771])).
% 3.17/0.82 fof(f784,plain,(
% 3.17/0.82 one=converse(one)),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f20,f771])).
% 3.17/0.82 fof(f785,plain,(
% 3.17/0.82 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f771,f36])).
% 3.17/0.82 fof(f794,plain,(
% 3.17/0.82 composition(join(converse(one),sF0_fnc),top)=join(sF2_fnc,top)),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f771,f87])).
% 3.17/0.82 fof(f797,plain,(
% 3.17/0.82 ![X0,X1]: (composition(join(converse(one),X0),X1)=join(composition(X0,X1),X1))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f771,f192])).
% 3.17/0.82 fof(f798,plain,(
% 3.17/0.82 ![X0,X1]: (composition(join(X0,converse(one)),X1)=join(X1,composition(X0,X1)))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f771,f192])).
% 3.17/0.82 fof(f810,plain,(
% 3.17/0.82 ![X0]: (composition(one,X0)=X0)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f771,f783])).
% 3.17/0.82 fof(f812,plain,(
% 3.17/0.82 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f810,f785])).
% 3.17/0.82 fof(f823,plain,(
% 3.17/0.82 composition(join(sF0_fnc,converse(one)),top)=join(sF2_fnc,top)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f640,f794])).
% 3.17/0.82 fof(f824,plain,(
% 3.17/0.82 composition(join(sF0_fnc,one),top)=join(sF2_fnc,top)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f784,f823])).
% 3.17/0.82 fof(f825,plain,(
% 3.17/0.82 composition(join(one,sF0_fnc),top)=join(sF2_fnc,top)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f640,f824])).
% 3.17/0.82 fof(f826,plain,(
% 3.17/0.82 composition(join(one,sF0_fnc),top)=join(top,sF2_fnc)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f825])).
% 3.17/0.82 fof(f833,plain,(
% 3.17/0.82 ![X0,X1]: (composition(join(one,X0),X1)=join(composition(X0,X1),X1))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f784,f797])).
% 3.17/0.82 fof(f834,plain,(
% 3.17/0.82 ![X0]: (join(sF0_fnc,composition(join(X0,sk1),top))=composition(join(one,X0),top))),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f836,f636])).
% 3.17/0.82 fof(f836,plain,(
% 3.17/0.82 ![X0,X1]: (composition(join(one,X0),X1)=join(X1,composition(X0,X1)))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f833])).
% 3.17/0.82 fof(f837,plain,(
% 3.17/0.82 ![X0,X1]: (composition(join(X0,one),X1)=join(X1,composition(X0,X1)))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f784,f798])).
% 3.17/0.82 fof(f910,plain,(
% 3.17/0.82 join(zero,complement(top))=complement(top)),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f245,f812])).
% 3.17/0.82 fof(f911,plain,(
% 3.17/0.82 join(meet(top,top),complement(join(zero,zero)))=complement(join(zero,zero))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f440,f812])).
% 3.17/0.82 fof(f917,plain,(
% 3.17/0.82 join(sF0_fnc,complement(sF1_fnc))=complement(sF1_fnc)),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f30,f812])).
% 3.17/0.82 fof(f919,plain,(
% 3.17/0.82 join(complement(join(zero,zero)),meet(top,top))=complement(join(zero,zero))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f440,f812])).
% 3.17/0.82 fof(f927,plain,(
% 3.17/0.82 ![X0]: (X0=join(meet(X0,complement(X0)),complement(complement(X0))))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f812,f39])).
% 3.17/0.82 fof(f929,plain,(
% 3.17/0.82 join(zero,zero)=complement(top)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f245,f910])).
% 3.17/0.82 fof(f936,plain,(
% 3.17/0.82 join(zero,zero)=zero),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f245,f929])).
% 3.17/0.82 fof(f937,plain,(
% 3.17/0.82 join(meet(top,top),meet(top,top))=complement(join(zero,zero))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f440,f911])).
% 3.17/0.82 fof(f938,plain,(
% 3.17/0.82 join(meet(top,top),meet(top,top))=meet(top,top)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f440,f937])).
% 3.17/0.82 fof(f953,plain,(
% 3.17/0.82 join(sF0_fnc,sF0_fnc)=complement(sF1_fnc)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f30,f917])).
% 3.17/0.82 fof(f960,plain,(
% 3.17/0.82 composition(sF0_fnc,top)=join(sF2_fnc,sF2_fnc)),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f961,f100])).
% 3.17/0.82 fof(f961,plain,(
% 3.17/0.82 join(sF0_fnc,sF0_fnc)=sF0_fnc),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f30,f953])).
% 3.17/0.82 fof(f965,plain,(
% 3.17/0.82 join(meet(top,top),complement(join(zero,zero)))=complement(join(zero,zero))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f919])).
% 3.17/0.82 fof(f966,plain,(
% 3.17/0.82 join(meet(top,top),meet(top,top))=complement(join(zero,zero))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f440,f965])).
% 3.17/0.82 fof(f967,plain,(
% 3.17/0.82 meet(top,top)=complement(join(zero,zero))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f938,f966])).
% 3.17/0.82 fof(f968,plain,(
% 3.17/0.82 meet(top,top)=complement(zero)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f936,f967])).
% 3.17/0.82 fof(f992,plain,(
% 3.17/0.82 ![X0]: (X0=join(complement(complement(X0)),meet(X0,complement(X0))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f927])).
% 3.17/0.82 fof(f993,plain,(
% 3.17/0.82 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f27,f992])).
% 3.17/0.82 fof(f994,plain,(
% 3.17/0.82 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f993])).
% 3.17/0.82 fof(f1013,plain,(
% 3.17/0.82 sF2_fnc=join(sF2_fnc,sF2_fnc)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f38,f960])).
% 3.17/0.82 fof(f1020,plain,(
% 3.17/0.82 ![X0]: (join(sF2_fnc,join(sF2_fnc,X0))=join(sF2_fnc,X0))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f1013,f16])).
% 3.17/0.82 fof(f1021,plain,(
% 3.17/0.82 sF1_fnc=join(meet(sF1_fnc,sF0_fnc),complement(sF0_fnc))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f961,f54])).
% 3.17/0.82 fof(f1023,plain,(
% 3.17/0.82 sF1_fnc=join(complement(sF0_fnc),meet(sF1_fnc,sF0_fnc))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f1021])).
% 3.17/0.82 fof(f1024,plain,(
% 3.17/0.82 sF1_fnc=join(complement(sF0_fnc),zero)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f155,f1023])).
% 3.17/0.82 fof(f1025,plain,(
% 3.17/0.82 sF1_fnc=join(zero,complement(sF0_fnc))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f1024])).
% 3.17/0.82 fof(f1091,plain,(
% 3.17/0.82 ![X0]: (meet(top,complement(X0))=complement(X0))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f994,f252])).
% 3.17/0.82 fof(f1102,plain,(
% 3.17/0.82 ![X0]: (top=join(meet(X0,top),complement(X0)))),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f1091,f593])).
% 3.17/0.82 fof(f1106,plain,(
% 3.17/0.82 ![X0]: (top=join(complement(X0),meet(X0,top)))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f1102])).
% 3.17/0.82 fof(f1112,plain,(
% 3.17/0.82 ![X0,X1]: (meet(top,meet(X0,X1))=complement(join(complement(X0),complement(X1))))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f18,f1091])).
% 3.17/0.82 fof(f1133,plain,(
% 3.17/0.82 ![X0,X1]: (meet(top,meet(X0,X1))=meet(X0,X1))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f18,f1112])).
% 3.17/0.82 fof(f1154,plain,(
% 3.17/0.82 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f18,f201])).
% 3.17/0.82 fof(f1185,plain,(
% 3.17/0.82 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f1154])).
% 3.17/0.82 fof(f1371,plain,(
% 3.17/0.82 join(sF2_fnc,top)=join(sF2_fnc,complement(sF2_fnc))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f26,f1020])).
% 3.17/0.82 fof(f1381,plain,(
% 3.17/0.82 join(top,sF2_fnc)=join(sF2_fnc,complement(sF2_fnc))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f1371])).
% 3.17/0.82 fof(f1382,plain,(
% 3.17/0.82 composition(join(one,sF0_fnc),top)=top),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f1383,f826])).
% 3.17/0.82 fof(f1383,plain,(
% 3.17/0.82 join(top,sF2_fnc)=top),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f26,f1381])).
% 3.17/0.82 fof(f1484,plain,(
% 3.17/0.82 ![X0]: (composition(join(join(one,sF0_fnc),X0),top)=join(composition(X0,top),top))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f1382,f192])).
% 3.17/0.82 fof(f1508,plain,(
% 3.17/0.82 ![X0]: (composition(join(one,join(sF0_fnc,X0)),top)=join(composition(X0,top),top))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f16,f1484])).
% 3.17/0.82 fof(f1509,plain,(
% 3.17/0.82 ![X0]: (composition(join(one,join(sF0_fnc,X0)),top)=join(top,composition(X0,top)))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f1508])).
% 3.17/0.82 fof(f1510,plain,(
% 3.17/0.82 ![X0]: (composition(join(one,join(sF0_fnc,X0)),top)=composition(join(X0,one),top))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f837,f1509])).
% 3.17/0.82 fof(f1540,plain,(
% 3.17/0.82 ![X0]: (X0=join(meet(X0,meet(X0,top)),complement(top)))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f1106,f39])).
% 3.17/0.82 fof(f1553,plain,(
% 3.17/0.82 ![X0]: (X0=join(complement(top),meet(X0,meet(X0,top))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f1540])).
% 3.17/0.82 fof(f1554,plain,(
% 3.17/0.82 ![X0]: (X0=join(zero,meet(X0,meet(X0,top))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f245,f1553])).
% 3.17/0.82 fof(f1558,plain,(
% 3.17/0.82 ![X0]: (X0=join(zero,meet(X0,meet(top,X0))))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f542,f1554])).
% 3.17/0.82 fof(f1804,plain,(
% 3.17/0.82 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(join(meet(X0,X1),top)),meet(top,join(complement(X0),complement(X1)))))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f542,f249])).
% 3.17/0.82 fof(f1900,plain,(
% 3.17/0.82 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(join(top,meet(X0,X1))),meet(top,join(complement(X0),complement(X1)))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f1804])).
% 3.17/0.82 fof(f1901,plain,(
% 3.17/0.82 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(join(top,meet(X0,X1))),complement(join(zero,meet(X0,X1)))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f551,f1900])).
% 3.17/0.82 fof(f1902,plain,(
% 3.17/0.82 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(join(zero,meet(X0,X1))),complement(join(top,meet(X0,X1)))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f1901])).
% 3.17/0.82 fof(f2292,plain,(
% 3.17/0.82 ![X0]: (join(X0,complement(X0))=join(top,complement(X0)))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f812,f297])).
% 3.17/0.82 fof(f2296,plain,(
% 3.17/0.82 ![X0]: (join(X0,top)=join(top,complement(complement(X0))))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f26,f297])).
% 3.17/0.82 fof(f2300,plain,(
% 3.17/0.82 ![X0]: (join(top,join(zero,X0))=join(top,X0))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f245,f297])).
% 3.17/0.82 fof(f2314,plain,(
% 3.17/0.82 ![X0,X1]: (X0=join(meet(X0,join(complement(complement(X0)),X1)),complement(join(top,X1))))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f297,f39])).
% 3.17/0.82 fof(f2326,plain,(
% 3.17/0.82 ![X0]: (X0=join(meet(top,X0),complement(top)))),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f2327,f603])).
% 3.17/0.82 fof(f2327,plain,(
% 3.17/0.82 ![X0]: (top=join(top,complement(X0)))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f26,f2292])).
% 3.17/0.82 fof(f2336,plain,(
% 3.17/0.82 ![X0]: (join(X0,top)=top)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f2327,f2296])).
% 3.17/0.82 fof(f2337,plain,(
% 3.17/0.82 ![X0]: (join(zero,join(X0,top))=join(top,X0))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f277,f2300])).
% 3.17/0.82 fof(f2338,plain,(
% 3.17/0.82 ![X0]: (join(zero,top)=join(top,X0))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f2336,f2337])).
% 3.17/0.82 fof(f2344,plain,(
% 3.17/0.82 ![X0]: (join(sF0_fnc,join(sF1_fnc,X0))=top)),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f2367,f296])).
% 3.17/0.82 fof(f2347,plain,(
% 3.17/0.82 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(join(zero,meet(X0,X1))),complement(top)))),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f2367,f1902])).
% 3.17/0.82 fof(f2367,plain,(
% 3.17/0.82 ![X0]: (top=join(top,X0))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f257,f2338])).
% 3.17/0.82 fof(f2397,plain,(
% 3.17/0.82 ![X0,X1]: (X0=join(complement(join(top,X1)),meet(X0,join(complement(complement(X0)),X1))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f2314])).
% 3.17/0.82 fof(f2398,plain,(
% 3.17/0.82 ![X0,X1]: (X0=join(complement(top),meet(X0,join(complement(complement(X0)),X1))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f2367,f2397])).
% 3.17/0.82 fof(f2399,plain,(
% 3.17/0.82 ![X0,X1]: (X0=join(zero,meet(X0,join(complement(complement(X0)),X1))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f245,f2398])).
% 3.17/0.82 fof(f2414,plain,(
% 3.17/0.82 ![X0]: (X0=join(complement(top),meet(top,X0)))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f2326])).
% 3.17/0.82 fof(f2417,plain,(
% 3.17/0.82 ![X0]: (X0=join(zero,meet(top,X0)))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f245,f2414])).
% 3.17/0.82 fof(f2422,plain,(
% 3.17/0.82 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(top),complement(join(zero,meet(X0,X1)))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f2347])).
% 3.17/0.82 fof(f2423,plain,(
% 3.17/0.82 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(join(zero,meet(X0,X1)))))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f245,f2422])).
% 3.17/0.82 fof(f2502,plain,(
% 3.17/0.82 meet(top,top)=top),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f1558,f2417])).
% 3.17/0.82 fof(f2507,plain,(
% 3.17/0.82 ![X0,X1]: (meet(X0,X1)=join(zero,meet(X0,X1)))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f1133,f2417])).
% 3.17/0.82 fof(f2508,plain,(
% 3.17/0.82 ![X0]: (complement(X0)=join(zero,complement(X0)))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f1091,f2417])).
% 3.17/0.82 fof(f2521,plain,(
% 3.17/0.82 top=complement(zero)),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f2502,f968])).
% 3.17/0.82 fof(f2523,plain,(
% 3.17/0.82 ![X0]: (X0=meet(top,X0))),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f2507,f2417])).
% 3.17/0.82 fof(f2526,plain,(
% 3.17/0.82 ![X0]: (X0=meet(X0,meet(top,X0)))),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f2507,f1558])).
% 3.17/0.82 fof(f2547,plain,(
% 3.17/0.82 ![X0,X1]: (X0=meet(X0,join(complement(complement(X0)),X1)))),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f2507,f2399])).
% 3.17/0.82 fof(f2550,plain,(
% 3.17/0.82 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(meet(X0,X1))))),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f2507,f2423])).
% 3.17/0.82 fof(f2553,plain,(
% 3.17/0.82 ![X0]: (X0=complement(complement(X0)))),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f2508,f994])).
% 3.17/0.82 fof(f2554,plain,(
% 3.17/0.82 sF1_fnc=complement(sF0_fnc)),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f2508,f1025])).
% 3.17/0.82 fof(f2647,plain,(
% 3.17/0.82 ![X0]: (X0=meet(X0,X0))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f2523,f2526])).
% 3.17/0.82 fof(f2723,plain,(
% 3.17/0.82 ![X0,X1]: (meet(X0,X1)=complement(complement(meet(X1,X0))))),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f2724,f229])).
% 3.17/0.82 fof(f2724,plain,(
% 3.17/0.82 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f2508,f2550])).
% 3.17/0.82 fof(f2727,plain,(
% 3.17/0.82 ![X0,X1]: (X0=meet(X0,join(X0,X1)))),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f2553,f2547])).
% 3.17/0.82 fof(f2900,plain,(
% 3.17/0.82 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f2553,f2723])).
% 3.17/0.82 fof(f2917,plain,(
% 3.17/0.82 ![X0]: (X0=join(X0,meet(X0,complement(X0))))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f2647,f1185])).
% 3.17/0.82 fof(f2949,plain,(
% 3.17/0.82 ![X0]: (X0=join(X0,zero))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f27,f2917])).
% 3.17/0.82 fof(f3024,plain,(
% 3.17/0.82 ![X0]: (X0=join(zero,X0))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f15,f2949])).
% 3.17/0.82 fof(f3029,plain,(
% 3.17/0.82 ![X0]: (converse(converse(X0))=join(X0,converse(zero)))),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f2949,f209])).
% 3.17/0.82 fof(f3047,plain,(
% 3.17/0.82 ![X0]: (X0=join(X0,converse(zero)))),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f22,f3029])).
% 3.17/0.82 fof(f3714,plain,(
% 3.17/0.82 ![X0]: (join(sF0_fnc,composition(join(X0,sk1),top))=top)),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f92,f2344])).
% 3.17/0.82 fof(f3733,plain,(
% 3.17/0.82 ![X0]: (top=composition(join(one,X0),top))),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f3714,f834])).
% 3.17/0.82 fof(f3745,plain,(
% 3.17/0.82 ![X0]: (top=composition(join(X0,one),top))),
% 3.17/0.82 inference(backward_demodulation,[status(thm)],[f3733,f1510])).
% 3.17/0.82 fof(f3750,plain,(
% 3.17/0.82 top=composition(top,top)),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f2367,f3745])).
% 3.17/0.82 fof(f3890,plain,(
% 3.17/0.82 composition(sk1,top)=composition(sF1_fnc,top)),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f3750,f44])).
% 3.17/0.82 fof(f3908,plain,(
% 3.17/0.82 sF1_fnc=composition(sF1_fnc,top)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f29,f3890])).
% 3.17/0.82 fof(f3950,plain,(
% 3.17/0.82 composition(join(sF1_fnc,sF0_fnc),top)=join(sF2_fnc,sF1_fnc)),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f3908,f87])).
% 3.17/0.82 fof(f3959,plain,(
% 3.17/0.82 join(complement(top),composition(converse(sF1_fnc),complement(sF1_fnc)))=complement(top)),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f3908,f36])).
% 3.17/0.82 fof(f3967,plain,(
% 3.17/0.82 composition(join(sF0_fnc,sF1_fnc),top)=join(sF2_fnc,sF1_fnc)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f640,f3950])).
% 3.17/0.82 fof(f3968,plain,(
% 3.17/0.82 composition(top,top)=join(sF2_fnc,sF1_fnc)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f41,f3967])).
% 3.17/0.82 fof(f3969,plain,(
% 3.17/0.82 top=join(sF2_fnc,sF1_fnc)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f3750,f3968])).
% 3.17/0.82 fof(f3971,plain,(
% 3.17/0.82 top=join(sF1_fnc,sF2_fnc)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f15,f3969])).
% 3.17/0.82 fof(f3985,plain,(
% 3.17/0.82 join(zero,composition(converse(sF1_fnc),complement(sF1_fnc)))=complement(top)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f245,f3959])).
% 3.17/0.82 fof(f3986,plain,(
% 3.17/0.82 composition(converse(sF1_fnc),complement(sF1_fnc))=complement(top)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f3024,f3985])).
% 3.17/0.82 fof(f3987,plain,(
% 3.17/0.82 composition(converse(sF1_fnc),sF0_fnc)=complement(top)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f30,f3986])).
% 3.17/0.82 fof(f3988,plain,(
% 3.17/0.82 composition(converse(sF1_fnc),sF0_fnc)=zero),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f245,f3987])).
% 3.17/0.82 fof(f4049,plain,(
% 3.17/0.82 zero=converse(zero)),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f3024,f3047])).
% 3.17/0.82 fof(f4143,plain,(
% 3.17/0.82 converse(zero)=composition(converse(sF0_fnc),sF1_fnc)),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f3988,f214])).
% 3.17/0.82 fof(f4157,plain,(
% 3.17/0.82 zero=composition(converse(sF0_fnc),sF1_fnc)),
% 3.17/0.82 inference(forward_demodulation,[status(thm)],[f4049,f4143])).
% 3.17/0.82 fof(f4212,plain,(
% 3.17/0.82 join(sF0_fnc,composition(converse(converse(sF0_fnc)),complement(zero)))=sF0_fnc),
% 3.17/0.82 inference(paramodulation,[status(thm)],[f4157,f323])).
% 3.17/0.84 fof(f4227,plain,(
% 3.17/0.84 join(sF0_fnc,composition(sF0_fnc,complement(zero)))=sF0_fnc),
% 3.17/0.84 inference(forward_demodulation,[status(thm)],[f22,f4212])).
% 3.17/0.84 fof(f4228,plain,(
% 3.17/0.84 join(sF0_fnc,composition(sF0_fnc,top))=sF0_fnc),
% 3.17/0.84 inference(forward_demodulation,[status(thm)],[f2521,f4227])).
% 3.17/0.84 fof(f4229,plain,(
% 3.17/0.84 join(sF0_fnc,sF2_fnc)=sF0_fnc),
% 3.17/0.84 inference(forward_demodulation,[status(thm)],[f38,f4228])).
% 3.17/0.84 fof(f4588,plain,(
% 3.17/0.84 ![X0,X1]: (X0=meet(X0,join(X1,X0)))),
% 3.17/0.84 inference(paramodulation,[status(thm)],[f15,f2727])).
% 3.17/0.84 fof(f4654,plain,(
% 3.17/0.84 sF2_fnc=meet(sF2_fnc,sF0_fnc)),
% 3.17/0.84 inference(paramodulation,[status(thm)],[f4229,f4588])).
% 3.17/0.84 fof(f4688,plain,(
% 3.17/0.84 sF2_fnc=meet(sF0_fnc,sF2_fnc)),
% 3.17/0.84 inference(forward_demodulation,[status(thm)],[f2900,f4654])).
% 3.17/0.84 fof(f4707,plain,(
% 3.17/0.84 sF0_fnc=join(sF2_fnc,complement(join(sF2_fnc,complement(sF0_fnc))))),
% 3.17/0.84 inference(paramodulation,[status(thm)],[f4688,f201])).
% 3.17/0.84 fof(f4723,plain,(
% 3.17/0.84 sF0_fnc=join(sF2_fnc,complement(join(sF2_fnc,sF1_fnc)))),
% 3.17/0.84 inference(forward_demodulation,[status(thm)],[f2554,f4707])).
% 3.17/0.84 fof(f4724,plain,(
% 3.17/0.84 sF0_fnc=join(sF2_fnc,complement(join(sF1_fnc,sF2_fnc)))),
% 3.17/0.84 inference(forward_demodulation,[status(thm)],[f15,f4723])).
% 3.17/0.84 fof(f4725,plain,(
% 3.17/0.84 sF0_fnc=join(sF2_fnc,complement(top))),
% 3.17/0.84 inference(forward_demodulation,[status(thm)],[f3971,f4724])).
% 3.17/0.84 fof(f4726,plain,(
% 3.17/0.84 sF0_fnc=join(sF2_fnc,zero)),
% 3.17/0.84 inference(forward_demodulation,[status(thm)],[f245,f4725])).
% 3.17/0.84 fof(f4727,plain,(
% 3.17/0.84 sF0_fnc=sF2_fnc),
% 3.17/0.84 inference(forward_demodulation,[status(thm)],[f2949,f4726])).
% 3.17/0.84 fof(f4728,plain,(
% 3.17/0.84 $false),
% 3.17/0.84 inference(forward_subsumption_resolution,[status(thm)],[f4727,f33])).
% 3.17/0.84 % SZS output end CNFRefutation for theBenchmark.p
% 3.17/0.85 % Elapsed time: 0.462332 seconds
% 3.17/0.85 % CPU time: 3.457239 seconds
% 3.17/0.85 % Total memory used: 66.395 MB
% 3.17/0.85 % Net memory used: 63.651 MB
%------------------------------------------------------------------------------