%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT023-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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 01:03:09 PM UTC 2026
% Result : Unsatisfiable 143.38s 33.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT023-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n009.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 : Sun Sep 20 23:06:57 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 143.38/33.42 % Refutation found
% 143.38/33.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 143.38/33.42 % SZS output start CNFRefutation for theBenchmark
% 143.38/33.42 fof(f1,axiom,(
% 143.38/33.42 (![X]: (meet(X,X) = X ))),
% 143.38/33.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 143.38/33.42 fof(f2,axiom,(
% 143.38/33.42 (![X]: (join(X,X) = X ))),
% 143.38/33.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 143.38/33.42 fof(f3,axiom,(
% 143.38/33.42 (![X,Y]: (meet(X,Y) = meet(Y,X) ))),
% 143.38/33.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 143.38/33.42 fof(f4,axiom,(
% 143.38/33.42 (![X,Y]: (join(X,Y) = join(Y,X) ))),
% 143.38/33.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 143.38/33.42 fof(f5,axiom,(
% 143.38/33.42 (![X,Y,Z]: (meet(meet(X,Y),Z) = meet(X,meet(Y,Z)) ))),
% 143.38/33.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 143.38/33.42 fof(f6,axiom,(
% 143.38/33.42 (![X,Y,Z]: (join(join(X,Y),Z) = join(X,join(Y,Z)) ))),
% 143.38/33.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 143.38/33.42 fof(f7,axiom,(
% 143.38/33.42 (![X,Y,Z]: (join(meet(X,join(Y,Z)),meet(X,Y)) = meet(X,join(Y,Z)) ))),
% 143.38/33.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 143.38/33.42 fof(f8,axiom,(
% 143.38/33.42 (![X,Y,Z]: (meet(join(X,meet(Y,Z)),join(X,Y)) = join(X,meet(Y,Z)) ))),
% 143.38/33.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 143.38/33.42 fof(f9,hypothesis,(
% 143.38/33.42 (![X,Y,Z]: (join(meet(join(X,Y),Z),Y) = join(meet(join(Z,Y),X),Y) ))),
% 143.38/33.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 143.38/33.42 fof(f10,negated_conjecture,(
% 143.38/33.42 meet(a,join(b,meet(a,c))) != join(meet(a,b),meet(a,c)) ),
% 143.38/33.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 143.38/33.42 fof(f11,plain,(
% 143.38/33.42 ![X0]: (meet(X0,X0)=X0)),
% 143.38/33.42 inference(cnf_transformation,[status(thm)],[f1])).
% 143.38/33.42 fof(f12,plain,(
% 143.38/33.42 ![X0]: (join(X0,X0)=X0)),
% 143.38/33.42 inference(cnf_transformation,[status(thm)],[f2])).
% 143.38/33.42 fof(f13,plain,(
% 143.38/33.42 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 143.38/33.42 inference(cnf_transformation,[status(thm)],[f3])).
% 143.38/33.42 fof(f14,plain,(
% 143.38/33.42 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 143.38/33.42 inference(cnf_transformation,[status(thm)],[f4])).
% 143.38/33.42 fof(f15,plain,(
% 143.38/33.42 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X0,meet(X1,X2)))),
% 143.38/33.42 inference(cnf_transformation,[status(thm)],[f5])).
% 143.38/33.42 fof(f16,plain,(
% 143.38/33.42 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X0,join(X1,X2)))),
% 143.38/33.42 inference(cnf_transformation,[status(thm)],[f6])).
% 143.38/33.42 fof(f17,plain,(
% 143.38/33.42 ![X0,X1,X2]: (join(meet(X0,join(X1,X2)),meet(X0,X1))=meet(X0,join(X1,X2)))),
% 143.38/33.42 inference(cnf_transformation,[status(thm)],[f7])).
% 143.38/33.42 fof(f18,plain,(
% 143.38/33.42 ![X0,X1,X2]: (meet(join(X0,meet(X1,X2)),join(X0,X1))=join(X0,meet(X1,X2)))),
% 143.38/33.42 inference(cnf_transformation,[status(thm)],[f8])).
% 143.38/33.42 fof(f19,plain,(
% 143.38/33.42 ![X0,X1,X2]: (join(meet(join(X0,X1),X2),X1)=join(meet(join(X2,X1),X0),X1))),
% 143.38/33.42 inference(cnf_transformation,[status(thm)],[f9])).
% 143.38/33.42 fof(f20,plain,(
% 143.38/33.42 ~meet(a,join(b,meet(a,c)))=join(meet(a,b),meet(a,c))),
% 143.38/33.42 inference(cnf_transformation,[status(thm)],[f10])).
% 143.38/33.42 fof(f21,definition,(
% 143.38/33.42 sF2_fnc=meet(a,c)),
% 143.38/33.42 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 143.38/33.42 fof(f22,definition,(
% 143.38/33.42 sF1_fnc=join(b,sF2_fnc)),
% 143.38/33.42 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 143.38/33.42 fof(f23,definition,(
% 143.38/33.42 sF0_fnc=meet(a,sF1_fnc)),
% 143.38/33.42 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 143.38/33.43 fof(f24,definition,(
% 143.38/33.43 sF4_fnc=meet(a,b)),
% 143.38/33.43 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 143.38/33.43 fof(f25,definition,(
% 143.38/33.43 sF3_fnc=join(sF4_fnc,sF2_fnc)),
% 143.38/33.43 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 143.38/33.43 fof(f26,plain,(
% 143.38/33.43 ~sF0_fnc=sF3_fnc),
% 143.38/33.43 inference(definition_folding,[],[f20,f25,f24,f23,f22,f21])).
% 143.38/33.43 fof(f27,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,join(X1,X2)))=meet(X0,join(X1,X2)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f14,f17])).
% 143.38/33.43 fof(f28,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,meet(X1,X2)))=join(X0,meet(X1,X2)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f13,f18])).
% 143.38/33.43 fof(f29,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,meet(join(X1,X0),X2))=join(meet(join(X2,X0),X1),X0))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f14,f19])).
% 143.38/33.43 fof(f30,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,meet(join(X1,X0),X2))=join(X0,meet(join(X2,X0),X1)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f14,f29])).
% 143.38/33.43 fof(f31,plain,(
% 143.38/33.43 sF2_fnc=meet(c,a)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f13,f21])).
% 143.38/33.43 fof(f32,plain,(
% 143.38/33.43 sF4_fnc=meet(b,a)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f13,f24])).
% 143.38/33.43 fof(f33,plain,(
% 143.38/33.43 sF3_fnc=join(sF2_fnc,sF4_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f14,f25])).
% 143.38/33.43 fof(f42,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X1,join(X2,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f14,f16])).
% 143.38/33.43 fof(f47,plain,(
% 143.38/33.43 ![X0]: (join(sF1_fnc,X0)=join(b,join(sF2_fnc,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f22,f16])).
% 143.38/33.43 fof(f48,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X0,X2)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f14,f16])).
% 143.38/33.43 fof(f50,plain,(
% 143.38/33.43 ![X0,X1]: (join(X0,X1)=join(X0,join(X0,X1)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f12,f16])).
% 143.38/33.43 fof(f58,plain,(
% 143.38/33.43 join(sF2_fnc,sF4_fnc)=join(sF2_fnc,sF3_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f33,f50])).
% 143.38/33.43 fof(f59,plain,(
% 143.38/33.43 join(b,sF2_fnc)=join(b,sF1_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f22,f50])).
% 143.38/33.43 fof(f61,plain,(
% 143.38/33.43 ![X0,X1]: (join(X0,X1)=join(X0,join(X1,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f14,f50])).
% 143.38/33.43 fof(f70,plain,(
% 143.38/33.43 sF3_fnc=join(sF2_fnc,sF3_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f33,f58])).
% 143.38/33.43 fof(f71,plain,(
% 143.38/33.43 sF1_fnc=join(b,sF1_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f22,f59])).
% 143.38/33.43 fof(f85,plain,(
% 143.38/33.43 join(sF4_fnc,sF2_fnc)=join(sF4_fnc,sF3_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f33,f61])).
% 143.38/33.43 fof(f87,plain,(
% 143.38/33.43 join(sF2_fnc,b)=join(sF2_fnc,sF1_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f22,f61])).
% 143.38/33.43 fof(f101,plain,(
% 143.38/33.43 join(sF2_fnc,sF4_fnc)=join(sF4_fnc,sF3_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f14,f85])).
% 143.38/33.43 fof(f102,plain,(
% 143.38/33.43 sF3_fnc=join(sF4_fnc,sF3_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f33,f101])).
% 143.38/33.43 fof(f103,plain,(
% 143.38/33.43 sF3_fnc=join(sF3_fnc,sF4_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f14,f102])).
% 143.38/33.43 fof(f106,plain,(
% 143.38/33.43 join(b,sF2_fnc)=join(sF2_fnc,sF1_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f14,f87])).
% 143.38/33.43 fof(f107,plain,(
% 143.38/33.43 sF1_fnc=join(sF2_fnc,sF1_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f22,f106])).
% 143.38/33.43 fof(f108,plain,(
% 143.38/33.43 sF1_fnc=join(sF1_fnc,sF2_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f14,f107])).
% 143.38/33.43 fof(f131,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X1,meet(X2,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f13,f15])).
% 143.38/33.43 fof(f135,plain,(
% 143.38/33.43 ![X0]: (meet(sF4_fnc,X0)=meet(b,meet(a,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f32,f15])).
% 143.38/33.43 fof(f137,plain,(
% 143.38/33.43 ![X0]: (meet(sF2_fnc,X0)=meet(c,meet(a,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f31,f15])).
% 143.38/33.43 fof(f138,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X1,meet(X0,X2)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f13,f15])).
% 143.38/33.43 fof(f140,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X0,X1)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f11,f15])).
% 143.38/33.43 fof(f149,plain,(
% 143.38/33.43 meet(a,sF1_fnc)=meet(a,sF0_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f23,f140])).
% 143.38/33.43 fof(f152,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X1,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f13,f140])).
% 143.38/33.43 fof(f162,plain,(
% 143.38/33.43 sF0_fnc=meet(a,sF0_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f23,f149])).
% 143.38/33.43 fof(f169,plain,(
% 143.38/33.43 ![X0,X1,X2,X3]: (join(meet(X0,meet(X1,X2)),meet(meet(X0,X1),join(X2,X3)))=meet(meet(X0,X1),join(X2,X3)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f15,f27])).
% 143.38/33.43 fof(f171,plain,(
% 143.38/33.43 ![X0]: (join(sF0_fnc,meet(a,join(sF1_fnc,X0)))=meet(a,join(sF1_fnc,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f23,f27])).
% 143.38/33.43 fof(f174,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,join(X0,X2)))=meet(X1,join(X0,X2)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f13,f27])).
% 143.38/33.43 fof(f176,plain,(
% 143.38/33.43 ![X0,X1]: (join(X0,meet(X0,join(X0,X1)))=meet(X0,join(X0,X1)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f11,f27])).
% 143.38/33.43 fof(f178,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(meet(X0,X1),meet(join(X1,X2),X0))=meet(X0,join(X1,X2)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f13,f27])).
% 143.38/33.43 fof(f180,plain,(
% 143.38/33.43 ![X0,X1]: (join(meet(join(X0,X1),X0),join(X0,X1))=meet(join(X0,X1),join(X0,X1)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f11,f27])).
% 143.38/33.43 fof(f191,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,join(X2,X1)))=meet(X0,join(X1,X2)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f14,f27])).
% 143.38/33.43 fof(f197,plain,(
% 143.38/33.43 ![X0,X1,X2,X3]: (join(meet(X0,meet(X1,X2)),meet(X0,meet(X1,join(X2,X3))))=meet(meet(X0,X1),join(X2,X3)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f15,f169])).
% 143.38/33.43 fof(f198,plain,(
% 143.38/33.43 ![X0,X1,X2,X3]: (join(meet(X0,meet(X1,X2)),meet(X0,meet(X1,join(X2,X3))))=meet(X0,meet(X1,join(X2,X3))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f15,f197])).
% 143.38/33.43 fof(f201,plain,(
% 143.38/33.43 ![X0,X1]: (join(join(X0,X1),meet(join(X0,X1),X0))=meet(join(X0,X1),join(X0,X1)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f14,f180])).
% 143.38/33.43 fof(f202,plain,(
% 143.38/33.43 ![X0,X1]: (join(X0,join(X1,meet(join(X0,X1),X0)))=meet(join(X0,X1),join(X0,X1)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f16,f201])).
% 143.38/33.43 fof(f203,plain,(
% 143.38/33.43 ![X0,X1]: (join(X0,join(X1,meet(X0,join(X0,X1))))=meet(join(X0,X1),join(X0,X1)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f13,f202])).
% 143.38/33.43 fof(f204,plain,(
% 143.38/33.43 ![X0,X1]: (join(X0,join(X1,meet(X0,join(X0,X1))))=join(X0,X1))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f11,f203])).
% 143.38/33.43 fof(f223,plain,(
% 143.38/33.43 ![X0]: (meet(sF3_fnc,join(sF2_fnc,meet(sF4_fnc,X0)))=join(sF2_fnc,meet(sF4_fnc,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f33,f28])).
% 143.38/33.43 fof(f228,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(join(X0,X1),join(X1,meet(X0,X2)))=join(X1,meet(X0,X2)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f14,f28])).
% 143.38/33.43 fof(f230,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,join(X0,meet(X0,X1)))=join(X0,meet(X0,X1)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f12,f28])).
% 143.38/33.43 fof(f238,plain,(
% 143.38/33.43 ![X0]: (meet(join(X0,b),join(X0,sF4_fnc))=join(X0,meet(b,a)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f32,f28])).
% 143.38/33.43 fof(f240,plain,(
% 143.38/33.43 ![X0]: (meet(join(X0,c),join(X0,sF2_fnc))=join(X0,meet(c,a)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f31,f28])).
% 143.38/33.43 fof(f242,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,meet(X2,X1)))=join(X0,meet(X1,X2)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f13,f28])).
% 143.38/33.43 fof(f265,plain,(
% 143.38/33.43 ![X0]: (meet(join(X0,b),join(X0,sF4_fnc))=join(X0,sF4_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f32,f238])).
% 143.38/33.43 fof(f267,plain,(
% 143.38/33.43 ![X0]: (meet(join(X0,c),join(X0,sF2_fnc))=join(X0,sF2_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f31,f240])).
% 143.38/33.43 fof(f298,plain,(
% 143.38/33.43 meet(sF1_fnc,a)=meet(sF1_fnc,sF0_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f23,f152])).
% 143.38/33.43 fof(f300,plain,(
% 143.38/33.43 meet(a,c)=meet(a,sF2_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f31,f152])).
% 143.38/33.43 fof(f322,plain,(
% 143.38/33.43 meet(a,sF1_fnc)=meet(sF1_fnc,sF0_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f13,f298])).
% 143.38/33.43 fof(f323,plain,(
% 143.38/33.43 sF0_fnc=meet(sF1_fnc,sF0_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f23,f322])).
% 143.38/33.43 fof(f324,plain,(
% 143.38/33.43 sF0_fnc=meet(sF0_fnc,sF1_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f13,f323])).
% 143.38/33.43 fof(f327,plain,(
% 143.38/33.43 meet(c,a)=meet(a,sF2_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f13,f300])).
% 143.38/33.43 fof(f328,plain,(
% 143.38/33.43 sF2_fnc=meet(a,sF2_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f31,f327])).
% 143.38/33.43 fof(f481,plain,(
% 143.38/33.43 join(sF1_fnc,sF4_fnc)=join(b,sF3_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f33,f47])).
% 143.38/33.43 fof(f542,plain,(
% 143.38/33.43 meet(sF4_fnc,sF2_fnc)=meet(b,sF2_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f328,f135])).
% 143.38/33.43 fof(f544,plain,(
% 143.38/33.43 meet(sF4_fnc,sF0_fnc)=meet(b,sF0_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f162,f135])).
% 143.38/33.43 fof(f545,plain,(
% 143.38/33.43 meet(sF4_fnc,sF1_fnc)=meet(b,sF0_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f23,f135])).
% 143.38/33.43 fof(f559,plain,(
% 143.38/33.43 meet(sF2_fnc,sF4_fnc)=meet(b,sF2_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f13,f542])).
% 143.38/33.43 fof(f561,plain,(
% 143.38/33.43 meet(sF0_fnc,sF4_fnc)=meet(b,sF0_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f13,f544])).
% 143.38/33.43 fof(f562,plain,(
% 143.38/33.43 meet(sF1_fnc,sF4_fnc)=meet(b,sF0_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f13,f545])).
% 143.38/33.43 fof(f627,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,meet(X1,join(X2,X0)))=join(X0,meet(join(X1,X0),X2)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f13,f30])).
% 143.38/33.43 fof(f881,plain,(
% 143.38/33.43 ![X0]: (join(X0,sF1_fnc)=join(sF1_fnc,join(sF2_fnc,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f108,f42])).
% 143.38/33.43 fof(f883,plain,(
% 143.38/33.43 ![X0]: (join(X0,sF3_fnc)=join(sF3_fnc,join(sF4_fnc,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f103,f42])).
% 143.38/33.43 fof(f888,plain,(
% 143.38/33.43 ![X0]: (join(X0,sF3_fnc)=join(sF2_fnc,join(sF4_fnc,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f33,f42])).
% 143.38/33.43 fof(f901,plain,(
% 143.38/33.43 ![X0,X1]: (join(X0,X1)=join(X1,join(X1,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f12,f42])).
% 143.38/33.43 fof(f912,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X2,X0),X1))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f14,f42])).
% 143.38/33.43 fof(f936,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X1,join(X0,X2)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f14,f42])).
% 143.38/33.43 fof(f938,plain,(
% 143.38/33.43 ![X0,X1]: (join(X0,join(X1,X0))=join(X1,X0))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f12,f42])).
% 143.38/33.43 fof(f975,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X0,join(X2,join(X0,X1))))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f42,f50])).
% 143.38/33.43 fof(f1076,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X0,join(join(X0,X1),X2))))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f50,f48])).
% 143.38/33.43 fof(f1130,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X0,join(X1,join(join(X1,X0),X2))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f48,f1076])).
% 143.38/33.43 fof(f1131,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X0,join(X1,join(X0,join(X1,X2)))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f48,f1130])).
% 143.38/33.43 fof(f1132,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X0,join(join(X1,X2),X1)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f975,f1131])).
% 143.38/33.43 fof(f1133,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X0,join(X2,join(X1,X1))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f48,f1132])).
% 143.38/33.43 fof(f1134,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X0,join(X2,X1)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f12,f1133])).
% 143.38/33.43 fof(f1394,plain,(
% 143.38/33.43 meet(sF2_fnc,sF0_fnc)=meet(c,sF0_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f162,f137])).
% 143.38/33.43 fof(f1395,plain,(
% 143.38/33.43 meet(sF2_fnc,sF1_fnc)=meet(c,sF0_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f23,f137])).
% 143.38/33.43 fof(f1414,plain,(
% 143.38/33.43 meet(sF0_fnc,sF2_fnc)=meet(c,sF0_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f13,f1394])).
% 143.38/33.43 fof(f1415,plain,(
% 143.38/33.43 meet(sF1_fnc,sF2_fnc)=meet(c,sF0_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f13,f1395])).
% 143.38/33.43 fof(f1510,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X2,join(X0,join(X1,X2))))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f42,f901])).
% 143.38/33.43 fof(f1522,plain,(
% 143.38/33.43 ![X0]: (join(sF1_fnc,join(sF2_fnc,X0))=join(b,join(X0,sF2_fnc)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f901,f47])).
% 143.38/33.43 fof(f1533,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,join(X2,X1)))=meet(X0,join(X1,join(X1,X2))))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f901,f27])).
% 143.38/33.43 fof(f1589,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X1,join(X0,X2))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f48,f1510])).
% 143.38/33.43 fof(f1604,plain,(
% 143.38/33.43 ![X0]: (join(X0,sF1_fnc)=join(b,join(X0,sF2_fnc)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f881,f1522])).
% 143.38/33.43 fof(f1619,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(X0,join(X1,X2))=meet(X0,join(X1,join(X1,X2))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f191,f1533])).
% 143.38/33.43 fof(f1620,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(X0,join(X1,X2))=meet(X0,join(X2,X1)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f901,f1619])).
% 143.38/33.43 fof(f2199,plain,(
% 143.38/33.43 ![X0]: (meet(X0,sF0_fnc)=meet(a,meet(sF1_fnc,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f23,f131])).
% 143.38/33.43 fof(f2211,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X1,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f11,f131])).
% 143.38/33.43 fof(f2226,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(meet(X2,X0),X1))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f13,f131])).
% 143.38/33.43 fof(f2262,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X1,X0))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f11,f131])).
% 143.38/33.43 fof(f2312,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X0,meet(X2,meet(X0,X1))))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f131,f140])).
% 143.38/33.43 fof(f2442,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X1,meet(X0,meet(meet(X0,X1),X2))))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f140,f138])).
% 143.38/33.43 fof(f2501,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X0,meet(X1,meet(meet(X1,X0),X2))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f138,f2442])).
% 143.38/33.43 fof(f2502,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X0,meet(X1,meet(X0,meet(X1,X2)))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f138,f2501])).
% 143.38/33.43 fof(f2503,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X0,meet(meet(X1,X2),X1)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f2312,f2502])).
% 143.38/33.43 fof(f2504,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X0,meet(X2,meet(X1,X1))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f138,f2503])).
% 143.38/33.43 fof(f2505,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X0,meet(X2,X1)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f11,f2504])).
% 143.38/33.43 fof(f3025,plain,(
% 143.38/33.43 ![X0]: (join(join(sF4_fnc,X0),sF3_fnc)=join(sF2_fnc,join(X0,sF4_fnc)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f901,f888])).
% 143.38/33.43 fof(f3060,plain,(
% 143.38/33.43 ![X0]: (join(X0,join(sF4_fnc,sF3_fnc))=join(sF2_fnc,join(X0,sF4_fnc)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f48,f3025])).
% 143.38/33.43 fof(f3061,plain,(
% 143.38/33.43 ![X0]: (join(X0,join(sF3_fnc,sF4_fnc))=join(sF2_fnc,join(X0,sF4_fnc)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f1134,f3060])).
% 143.38/33.43 fof(f3062,plain,(
% 143.38/33.43 ![X0]: (join(X0,sF3_fnc)=join(sF2_fnc,join(X0,sF4_fnc)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f103,f3061])).
% 143.38/33.43 fof(f3251,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X2,meet(X0,meet(X1,X2))))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f131,f2211])).
% 143.38/33.43 fof(f3278,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,meet(X2,X1)))=join(X0,meet(X1,meet(X1,X2))))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f2211,f28])).
% 143.38/33.43 fof(f3358,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X2,meet(X1,meet(X0,X2))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f138,f3251])).
% 143.38/33.43 fof(f3393,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(X0,meet(X1,meet(X1,X2))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f242,f3278])).
% 143.38/33.43 fof(f3394,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(X0,meet(X2,X1)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f2211,f3393])).
% 143.38/33.43 fof(f3508,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(X0,meet(X1,meet(X2,meet(X0,X1))))=meet(X2,meet(X0,X1)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f15,f2262])).
% 143.38/33.43 fof(f3598,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(X0,meet(X0,meet(X1,X2)))=meet(X1,meet(X0,X2)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f3358,f3508])).
% 143.38/33.43 fof(f3599,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X0,meet(X2,X1)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f2211,f3598])).
% 143.38/33.43 fof(f3730,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,join(X1,join(X2,join(X0,X1))))=join(X2,join(X0,X1)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f16,f938])).
% 143.38/33.43 fof(f3836,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,join(X0,join(X1,X2)))=join(X1,join(X0,X2)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f1589,f3730])).
% 143.38/33.43 fof(f3837,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X0,join(X2,X1)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f901,f3836])).
% 143.38/33.43 fof(f4676,plain,(
% 143.38/33.43 ![X0,X1,X2,X3]: (join(meet(X0,meet(X1,X2)),meet(X0,meet(X1,join(X2,X3))))=meet(X0,meet(X1,join(X2,join(X3,X2)))))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f61,f198])).
% 143.38/33.43 fof(f4833,plain,(
% 143.38/33.43 ![X0,X1,X2,X3]: (meet(X0,meet(X1,join(X2,X3)))=meet(X0,meet(X1,join(X2,join(X3,X2)))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f198,f4676])).
% 143.38/33.43 fof(f4834,plain,(
% 143.38/33.43 ![X0,X1,X2,X3]: (meet(X0,meet(X1,join(X2,X3)))=meet(X0,meet(X1,join(X3,X2))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f938,f4833])).
% 143.38/33.43 fof(f4936,plain,(
% 143.38/33.43 join(sF0_fnc,meet(a,join(b,sF3_fnc)))=meet(a,join(sF1_fnc,sF4_fnc))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f481,f171])).
% 143.38/33.43 fof(f4968,plain,(
% 143.38/33.43 join(sF0_fnc,meet(a,join(b,sF3_fnc)))=meet(a,join(b,sF3_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f481,f4936])).
% 143.38/33.43 fof(f6645,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(join(X0,X1),X2)=meet(X2,join(X1,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f13,f1620])).
% 143.38/33.43 fof(f6700,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(join(X0,X1),X2)=meet(X2,meet(X2,join(X1,X0))))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f1620,f2211])).
% 143.38/33.43 fof(f6705,plain,(
% 143.38/33.43 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(X0,meet(X1,join(X2,X3))))=join(X0,meet(X1,join(X3,X2))))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f1620,f28])).
% 143.38/33.43 fof(f6815,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(join(X0,X1),X2)=meet(join(X1,X0),X2))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f2211,f6700])).
% 143.38/33.43 fof(f6817,plain,(
% 143.38/33.43 ![X0,X1,X2,X3]: (join(X0,meet(X1,join(X2,X3)))=join(X0,meet(X1,join(X3,X2))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f28,f6705])).
% 143.38/33.43 fof(f8600,plain,(
% 143.38/33.43 ![X0,X1]: (join(meet(X0,X1),meet(X1,X0))=meet(X1,join(X0,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f12,f174])).
% 143.38/33.43 fof(f8809,plain,(
% 143.38/33.43 ![X0,X1]: (join(meet(X0,X1),meet(X1,X0))=meet(X1,X0))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f12,f8600])).
% 143.38/33.43 fof(f8836,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,meet(join(meet(X0,X1),X2),X0)))=meet(meet(X0,X1),join(meet(X0,X1),X2)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f2226,f176])).
% 143.38/33.43 fof(f8916,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,join(X1,meet(X0,join(X0,X2))))=join(X1,meet(X0,join(X0,X2))))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f176,f936])).
% 143.38/33.43 fof(f8945,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,meet(X0,join(meet(X0,X1),X2))))=meet(meet(X0,X1),join(meet(X0,X1),X2)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f2505,f8836])).
% 143.38/33.43 fof(f8946,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,meet(X0,join(meet(X0,X1),X2))))=meet(X1,meet(join(meet(X0,X1),X2),X0)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f2226,f8945])).
% 143.38/33.43 fof(f8947,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,meet(X0,join(meet(X0,X1),X2))))=meet(X1,meet(X0,join(meet(X0,X1),X2))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f2505,f8946])).
% 143.38/33.43 fof(f9112,plain,(
% 143.38/33.43 ![X0,X1]: (join(X0,meet(X1,join(X1,X0)))=join(X1,X0))),
% 143.38/33.43 inference(backward_demodulation,[status(thm)],[f8916,f204])).
% 143.38/33.43 fof(f10118,plain,(
% 143.38/33.43 ![X0,X1,X2,X3]: (join(X0,join(X1,meet(X2,X3)))=join(join(X1,X0),meet(X3,X2)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f48,f3394])).
% 143.38/33.43 fof(f10124,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(X2,meet(X1,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f14,f3394])).
% 143.38/33.43 fof(f10126,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,X1)=join(meet(X0,X1),meet(X1,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f12,f3394])).
% 143.38/33.43 fof(f10259,plain,(
% 143.38/33.43 ![X0,X1,X2,X3]: (join(X0,join(X1,meet(X2,X3)))=join(X0,join(meet(X3,X2),X1)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f912,f10118])).
% 143.38/33.43 fof(f10770,plain,(
% 143.38/33.43 ![X0,X1,X2,X3]: (meet(X0,join(X1,join(X2,X3)))=meet(X0,join(X2,join(X1,X3))))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f3837,f1620])).
% 143.38/33.43 fof(f11323,plain,(
% 143.38/33.43 ![X0,X1,X2,X3]: (meet(X0,meet(X1,join(X2,X3)))=meet(meet(X0,X1),join(X3,X2)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f131,f6645])).
% 143.38/33.43 fof(f11397,plain,(
% 143.38/33.43 ![X0,X1]: (meet(join(X0,X1),join(X1,X0))=join(X1,X0))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f11,f6645])).
% 143.38/33.43 fof(f11458,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(X0,meet(join(X1,X0),X2))=join(X0,meet(X1,join(X0,X2))))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f6645,f30])).
% 143.38/33.43 fof(f11537,plain,(
% 143.38/33.43 ![X0,X1,X2,X3]: (meet(X0,meet(X1,join(X2,X3)))=meet(X0,meet(join(X3,X2),X1)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f3599,f11323])).
% 143.38/33.43 fof(f13578,plain,(
% 143.38/33.43 ![X0,X1]: (join(meet(X0,X1),meet(join(X0,meet(X0,X1)),X1))=meet(X0,join(X1,meet(X0,X1))))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f30,f178])).
% 143.38/33.43 fof(f13767,plain,(
% 143.38/33.43 ![X0,X1]: (join(meet(X0,X1),meet(X1,join(X0,meet(X0,X1))))=meet(X0,join(X1,meet(X0,X1))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f3394,f13578])).
% 143.38/33.43 fof(f13768,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,join(X1,meet(X1,X0)))=meet(X1,join(X0,meet(X1,X0))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f174,f13767])).
% 143.38/33.43 fof(f15698,plain,(
% 143.38/33.43 meet(join(sF1_fnc,c),sF1_fnc)=join(sF1_fnc,sF2_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f108,f267])).
% 143.38/33.43 fof(f15746,plain,(
% 143.38/33.43 meet(join(c,sF1_fnc),sF1_fnc)=join(sF1_fnc,sF2_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f6815,f15698])).
% 143.38/33.43 fof(f15747,plain,(
% 143.38/33.43 meet(sF1_fnc,join(sF1_fnc,c))=join(sF1_fnc,sF2_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f6645,f15746])).
% 143.38/33.43 fof(f15748,plain,(
% 143.38/33.43 meet(sF1_fnc,join(c,sF1_fnc))=join(sF1_fnc,sF2_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f1620,f15747])).
% 143.38/33.43 fof(f15749,plain,(
% 143.38/33.43 meet(sF1_fnc,join(c,sF1_fnc))=sF1_fnc),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f108,f15748])).
% 143.38/33.43 fof(f15918,plain,(
% 143.38/33.43 meet(join(c,sF1_fnc),sF0_fnc)=meet(a,sF1_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f15749,f2199])).
% 143.38/33.43 fof(f15943,plain,(
% 143.38/33.43 meet(sF0_fnc,join(sF1_fnc,c))=meet(a,sF1_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f6645,f15918])).
% 143.38/33.43 fof(f15944,plain,(
% 143.38/33.43 meet(sF0_fnc,join(c,sF1_fnc))=meet(a,sF1_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f1620,f15943])).
% 143.38/33.43 fof(f15945,plain,(
% 143.38/33.43 meet(sF0_fnc,join(c,sF1_fnc))=sF0_fnc),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f23,f15944])).
% 143.38/33.43 fof(f15993,plain,(
% 143.38/33.43 join(meet(c,sF0_fnc),sF0_fnc)=meet(sF0_fnc,join(c,sF1_fnc))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f15945,f174])).
% 143.38/33.43 fof(f16020,plain,(
% 143.38/33.43 join(sF0_fnc,meet(c,sF0_fnc))=meet(sF0_fnc,join(c,sF1_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f14,f15993])).
% 143.38/33.43 fof(f16021,plain,(
% 143.38/33.43 join(sF0_fnc,meet(c,sF0_fnc))=sF0_fnc),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f15945,f16020])).
% 143.38/33.43 fof(f16232,plain,(
% 143.38/33.43 meet(join(sF0_fnc,c),sF0_fnc)=join(sF0_fnc,meet(c,sF0_fnc))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f16021,f28])).
% 143.38/33.43 fof(f16264,plain,(
% 143.38/33.43 meet(join(c,sF0_fnc),sF0_fnc)=join(sF0_fnc,meet(c,sF0_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f6815,f16232])).
% 143.38/33.43 fof(f16265,plain,(
% 143.38/33.43 meet(sF0_fnc,join(sF0_fnc,c))=join(sF0_fnc,meet(c,sF0_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f6645,f16264])).
% 143.38/33.43 fof(f16266,plain,(
% 143.38/33.43 meet(sF0_fnc,join(c,sF0_fnc))=join(sF0_fnc,meet(c,sF0_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f1620,f16265])).
% 143.38/33.43 fof(f16267,plain,(
% 143.38/33.43 meet(sF0_fnc,join(c,sF0_fnc))=sF0_fnc),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f16021,f16266])).
% 143.38/33.43 fof(f16921,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(meet(X0,X1),meet(join(X2,meet(X0,X1)),meet(X1,X0)))=join(meet(X0,X1),meet(meet(X0,X1),X2)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f8809,f30])).
% 143.38/33.43 fof(f17630,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(meet(X0,X1),meet(meet(X1,X0),join(X2,meet(X0,X1))))=join(meet(X0,X1),meet(meet(X0,X1),X2)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f3394,f16921])).
% 143.38/33.43 fof(f17631,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,meet(join(X2,meet(X0,X1)),X0)))=join(meet(X0,X1),meet(meet(X0,X1),X2)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f3599,f17630])).
% 143.38/33.43 fof(f17632,plain,(
% 143.38/33.43 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,meet(X0,join(meet(X0,X1),X2))))=join(meet(X0,X1),meet(meet(X0,X1),X2)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f11537,f17631])).
% 143.38/33.43 fof(f17633,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(X0,meet(X1,join(meet(X1,X0),X2)))=join(meet(X1,X0),meet(meet(X1,X0),X2)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f8947,f17632])).
% 143.38/33.43 fof(f17648,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(X0,meet(X1,join(meet(X1,X0),X2)))=join(meet(X1,X0),meet(X1,meet(X2,X0))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f3599,f17633])).
% 143.38/33.43 fof(f19624,plain,(
% 143.38/33.43 ![X0,X1]: (join(X0,meet(X1,join(X0,X1)))=join(X1,X0))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f1620,f9112])).
% 143.38/33.43 fof(f19668,plain,(
% 143.38/33.43 join(sF4_fnc,meet(sF2_fnc,sF3_fnc))=join(sF2_fnc,sF4_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f33,f9112])).
% 143.38/33.43 fof(f19679,plain,(
% 143.38/33.43 join(sF2_fnc,meet(b,sF1_fnc))=join(b,sF2_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f22,f9112])).
% 143.38/33.43 fof(f19958,plain,(
% 143.38/33.43 join(sF4_fnc,meet(sF2_fnc,sF3_fnc))=sF3_fnc),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f33,f19668])).
% 143.38/33.43 fof(f20001,plain,(
% 143.38/33.43 join(sF2_fnc,meet(b,sF1_fnc))=sF1_fnc),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f22,f19679])).
% 143.38/33.43 fof(f20403,plain,(
% 143.38/33.43 join(sF2_fnc,meet(sF2_fnc,sF1_fnc))=meet(sF2_fnc,join(sF2_fnc,meet(b,sF1_fnc)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f20001,f176])).
% 143.38/33.43 fof(f20468,plain,(
% 143.38/33.43 join(sF2_fnc,meet(sF1_fnc,sF2_fnc))=meet(sF2_fnc,join(sF2_fnc,meet(b,sF1_fnc)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f3394,f20403])).
% 143.38/33.43 fof(f20469,plain,(
% 143.38/33.43 join(sF2_fnc,meet(c,sF0_fnc))=meet(sF2_fnc,join(sF2_fnc,meet(b,sF1_fnc)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f1415,f20468])).
% 143.38/33.43 fof(f20470,plain,(
% 143.38/33.43 join(sF2_fnc,meet(c,sF0_fnc))=meet(sF2_fnc,sF1_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f20001,f20469])).
% 143.38/33.43 fof(f20471,plain,(
% 143.38/33.43 join(sF2_fnc,meet(c,sF0_fnc))=meet(sF1_fnc,sF2_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f13,f20470])).
% 143.38/33.43 fof(f20473,plain,(
% 143.38/33.43 join(sF2_fnc,meet(c,sF0_fnc))=meet(c,sF0_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f1415,f20471])).
% 143.38/33.43 fof(f21294,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,meet(X0,X1))=join(meet(X0,X1),meet(meet(X0,X1),X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f140,f10126])).
% 143.38/33.43 fof(f21701,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,X1)=join(meet(X1,X0),meet(meet(X1,X0),X1)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f2211,f21294])).
% 143.38/33.43 fof(f21702,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,X1)=join(meet(X1,X0),meet(X1,meet(X1,X0))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f3394,f21701])).
% 143.38/33.43 fof(f21703,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X1,join(meet(X1,X0),X1))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f17648,f21702])).
% 143.38/33.43 fof(f21704,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X1,join(X1,meet(X1,X0)))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f4834,f21703])).
% 143.38/33.43 fof(f21705,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,X1)=meet(X1,join(X0,meet(X1,X0))))),
% 143.38/33.43 inference(backward_demodulation,[status(thm)],[f21707,f13768])).
% 143.38/33.43 fof(f21707,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,X1)=meet(X0,join(X1,meet(X1,X0))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f230,f21704])).
% 143.38/33.43 fof(f24746,plain,(
% 143.38/33.43 join(sF1_fnc,meet(sF2_fnc,sF1_fnc))=join(sF2_fnc,sF1_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f108,f19624])).
% 143.38/33.43 fof(f24854,plain,(
% 143.38/33.43 ![X0,X1]: (join(meet(X0,join(X1,X0)),join(X0,X1))=join(X1,meet(X0,join(X1,X0))))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f19624,f938])).
% 143.38/33.43 fof(f25009,plain,(
% 143.38/33.43 join(sF1_fnc,meet(sF1_fnc,sF2_fnc))=join(sF2_fnc,sF1_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f3394,f24746])).
% 143.38/33.43 fof(f25010,plain,(
% 143.38/33.43 join(sF1_fnc,meet(c,sF0_fnc))=join(sF2_fnc,sF1_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f1415,f25009])).
% 143.38/33.43 fof(f25011,plain,(
% 143.38/33.43 join(sF1_fnc,meet(c,sF0_fnc))=join(sF1_fnc,sF2_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f14,f25010])).
% 143.38/33.43 fof(f25012,plain,(
% 143.38/33.43 join(sF1_fnc,meet(c,sF0_fnc))=sF1_fnc),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f108,f25011])).
% 143.38/33.43 fof(f25311,plain,(
% 143.38/33.43 ![X0,X1]: (join(join(X0,X1),meet(join(X1,X0),X0))=join(X1,meet(X0,join(X1,X0))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f10124,f24854])).
% 143.38/33.43 fof(f25312,plain,(
% 143.38/33.43 ![X0,X1]: (join(X0,join(meet(join(X1,X0),X0),X1))=join(X1,meet(X0,join(X1,X0))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f3837,f25311])).
% 143.38/33.43 fof(f25313,plain,(
% 143.38/33.43 ![X0,X1]: (join(X0,join(X1,meet(X0,join(X1,X0))))=join(X1,meet(X0,join(X1,X0))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f10259,f25312])).
% 143.38/33.43 fof(f25314,plain,(
% 143.38/33.43 ![X0,X1]: (join(X0,join(X0,X1))=join(X1,meet(X0,join(X1,X0))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f19624,f25313])).
% 143.38/33.43 fof(f25315,plain,(
% 143.38/33.43 ![X0,X1]: (join(X0,X1)=join(X0,meet(X1,join(X0,X1))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f901,f25314])).
% 143.38/33.43 fof(f26592,plain,(
% 143.38/33.43 meet(sF4_fnc,sF1_fnc)=meet(sF4_fnc,join(sF1_fnc,meet(b,sF0_fnc)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f562,f21707])).
% 143.38/33.43 fof(f26800,plain,(
% 143.38/33.43 meet(sF1_fnc,sF4_fnc)=meet(sF4_fnc,join(sF1_fnc,meet(b,sF0_fnc)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f13,f26592])).
% 143.38/33.43 fof(f26801,plain,(
% 143.38/33.43 meet(b,sF0_fnc)=meet(sF4_fnc,join(sF1_fnc,meet(b,sF0_fnc)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f562,f26800])).
% 143.38/33.43 fof(f28868,plain,(
% 143.38/33.43 ![X0]: (meet(sF1_fnc,join(sF1_fnc,meet(b,X0)))=join(sF1_fnc,meet(b,X0)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f71,f228])).
% 143.38/33.43 fof(f28932,plain,(
% 143.38/33.43 ![X0,X1,X2]: (meet(join(X0,X1),join(X1,meet(X2,X0)))=join(X1,meet(X0,X2)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f3394,f228])).
% 143.38/33.43 fof(f30420,plain,(
% 143.38/33.43 meet(join(sF1_fnc,b),join(b,sF3_fnc))=join(sF1_fnc,sF4_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f481,f265])).
% 143.38/33.43 fof(f30421,plain,(
% 143.38/33.43 meet(join(sF3_fnc,b),sF3_fnc)=join(sF3_fnc,sF4_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f103,f265])).
% 143.38/33.43 fof(f30427,plain,(
% 143.38/33.43 meet(join(sF2_fnc,b),sF3_fnc)=join(sF2_fnc,sF4_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f33,f265])).
% 143.38/33.43 fof(f30501,plain,(
% 143.38/33.43 meet(join(b,sF1_fnc),join(b,sF3_fnc))=join(sF1_fnc,sF4_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f6815,f30420])).
% 143.38/33.43 fof(f30502,plain,(
% 143.38/33.43 meet(sF1_fnc,join(b,sF3_fnc))=join(sF1_fnc,sF4_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f71,f30501])).
% 143.38/33.43 fof(f30505,plain,(
% 143.38/33.43 meet(sF1_fnc,join(b,sF3_fnc))=join(b,sF3_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f481,f30502])).
% 143.38/33.43 fof(f30506,plain,(
% 143.38/33.43 meet(join(b,sF3_fnc),sF3_fnc)=join(sF3_fnc,sF4_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f6815,f30421])).
% 143.38/33.43 fof(f30507,plain,(
% 143.38/33.43 meet(sF3_fnc,join(sF3_fnc,b))=join(sF3_fnc,sF4_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f6645,f30506])).
% 143.38/33.43 fof(f30508,plain,(
% 143.38/33.43 meet(sF3_fnc,join(b,sF3_fnc))=join(sF3_fnc,sF4_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f1620,f30507])).
% 143.38/33.43 fof(f30510,plain,(
% 143.38/33.43 meet(sF3_fnc,join(b,sF3_fnc))=sF3_fnc),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f103,f30508])).
% 143.38/33.43 fof(f30522,plain,(
% 143.38/33.43 meet(join(b,sF2_fnc),sF3_fnc)=join(sF2_fnc,sF4_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f6815,f30427])).
% 143.38/33.43 fof(f30523,plain,(
% 143.38/33.43 meet(sF3_fnc,join(sF2_fnc,b))=join(sF2_fnc,sF4_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f6645,f30522])).
% 143.38/33.43 fof(f30524,plain,(
% 143.38/33.43 meet(sF3_fnc,join(b,sF2_fnc))=join(sF2_fnc,sF4_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f1620,f30523])).
% 143.38/33.43 fof(f30525,plain,(
% 143.38/33.43 meet(sF3_fnc,sF1_fnc)=join(sF2_fnc,sF4_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f22,f30524])).
% 143.38/33.43 fof(f30526,plain,(
% 143.38/33.43 meet(sF1_fnc,sF3_fnc)=join(sF2_fnc,sF4_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f13,f30525])).
% 143.38/33.43 fof(f30527,plain,(
% 143.38/33.43 meet(sF1_fnc,sF3_fnc)=sF3_fnc),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f33,f30526])).
% 143.38/33.43 fof(f30679,plain,(
% 143.38/33.43 meet(sF3_fnc,sF0_fnc)=meet(a,sF3_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f30527,f2199])).
% 143.38/33.43 fof(f30711,plain,(
% 143.38/33.43 meet(sF0_fnc,sF3_fnc)=meet(a,sF3_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f13,f30679])).
% 143.38/33.43 fof(f30767,plain,(
% 143.38/33.43 ![X0]: (meet(meet(a,sF3_fnc),X0)=meet(sF0_fnc,meet(X0,sF3_fnc)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f30711,f3599])).
% 143.38/33.43 fof(f30818,plain,(
% 143.38/33.43 ![X0]: (meet(a,meet(X0,sF3_fnc))=meet(sF0_fnc,meet(X0,sF3_fnc)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f3599,f30767])).
% 143.38/33.43 fof(f31380,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,join(X1,X0))=meet(join(X1,X0),join(X0,meet(join(X0,X0),X1))))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f30,f21705])).
% 143.38/33.43 fof(f31570,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,join(X1,X0))=join(X0,meet(X1,join(X0,X0))))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f28932,f31380])).
% 143.38/33.43 fof(f31593,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,join(X1,X0))=join(X0,meet(X1,X0)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f12,f31570])).
% 143.38/33.43 fof(f34175,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,join(X0,meet(X1,X0)))=join(X0,meet(X0,X1)))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f3394,f230])).
% 143.38/33.43 fof(f34190,plain,(
% 143.38/33.43 meet(sF1_fnc,join(sF1_fnc,meet(b,sF0_fnc)))=join(sF1_fnc,meet(sF1_fnc,sF4_fnc))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f562,f230])).
% 143.38/33.43 fof(f34193,plain,(
% 143.38/33.43 meet(sF2_fnc,join(sF2_fnc,meet(b,sF2_fnc)))=join(sF2_fnc,meet(sF2_fnc,sF4_fnc))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f559,f230])).
% 143.38/33.43 fof(f34490,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,meet(X0,join(X1,X0)))=join(X0,meet(X0,X1)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f31593,f34175])).
% 143.38/33.43 fof(f34491,plain,(
% 143.38/33.43 ![X0,X1]: (meet(join(X0,X1),X1)=join(X1,meet(X1,X0)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f2211,f34490])).
% 143.38/33.43 fof(f34574,plain,(
% 143.38/33.43 ![X0,X1]: (meet(X0,join(X0,X1))=join(X0,meet(X0,X1)))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f6645,f34491])).
% 143.38/33.43 fof(f34634,plain,(
% 143.38/33.43 join(sF1_fnc,meet(b,sF0_fnc))=join(sF1_fnc,meet(sF1_fnc,sF4_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f28868,f34190])).
% 143.38/33.43 fof(f34635,plain,(
% 143.38/33.43 join(sF1_fnc,meet(b,sF0_fnc))=meet(sF1_fnc,join(sF1_fnc,sF4_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f34574,f34634])).
% 143.38/33.43 fof(f34636,plain,(
% 143.38/33.43 join(sF1_fnc,meet(b,sF0_fnc))=meet(sF1_fnc,join(b,sF3_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f481,f34635])).
% 143.38/33.43 fof(f34637,plain,(
% 143.38/33.43 meet(b,sF0_fnc)=meet(sF4_fnc,join(b,sF3_fnc))),
% 143.38/33.43 inference(backward_demodulation,[status(thm)],[f34638,f26801])).
% 143.38/33.43 fof(f34638,plain,(
% 143.38/33.43 join(sF1_fnc,meet(b,sF0_fnc))=join(b,sF3_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f30505,f34636])).
% 143.38/33.43 fof(f34645,plain,(
% 143.38/33.43 meet(sF2_fnc,meet(sF2_fnc,join(b,sF2_fnc)))=join(sF2_fnc,meet(sF2_fnc,sF4_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f31593,f34193])).
% 143.38/33.43 fof(f34646,plain,(
% 143.38/33.43 meet(join(b,sF2_fnc),sF2_fnc)=join(sF2_fnc,meet(sF2_fnc,sF4_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f2211,f34645])).
% 143.38/33.43 fof(f34647,plain,(
% 143.38/33.43 meet(sF2_fnc,join(sF2_fnc,b))=join(sF2_fnc,meet(sF2_fnc,sF4_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f6645,f34646])).
% 143.38/33.43 fof(f34648,plain,(
% 143.38/33.43 meet(sF2_fnc,join(b,sF2_fnc))=join(sF2_fnc,meet(sF2_fnc,sF4_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f1620,f34647])).
% 143.38/33.43 fof(f34649,plain,(
% 143.38/33.43 meet(sF2_fnc,sF1_fnc)=join(sF2_fnc,meet(sF2_fnc,sF4_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f22,f34648])).
% 143.38/33.43 fof(f34650,plain,(
% 143.38/33.43 meet(sF1_fnc,sF2_fnc)=join(sF2_fnc,meet(sF2_fnc,sF4_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f13,f34649])).
% 143.38/33.43 fof(f34651,plain,(
% 143.38/33.43 meet(c,sF0_fnc)=join(sF2_fnc,meet(sF2_fnc,sF4_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f1415,f34650])).
% 143.38/33.43 fof(f34652,plain,(
% 143.38/33.43 meet(c,sF0_fnc)=meet(sF2_fnc,join(sF2_fnc,sF4_fnc))),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f34574,f34651])).
% 143.38/33.43 fof(f34653,plain,(
% 143.38/33.43 join(sF4_fnc,meet(c,sF0_fnc))=sF3_fnc),
% 143.38/33.43 inference(backward_demodulation,[status(thm)],[f34681,f19958])).
% 143.38/33.43 fof(f34681,plain,(
% 143.38/33.43 meet(c,sF0_fnc)=meet(sF2_fnc,sF3_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f33,f34652])).
% 143.38/33.43 fof(f36958,plain,(
% 143.38/33.43 join(meet(c,sF0_fnc),sF3_fnc)=join(sF2_fnc,sF3_fnc)),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f34653,f888])).
% 143.38/33.43 fof(f37005,plain,(
% 143.38/33.43 join(sF3_fnc,meet(sF0_fnc,c))=join(sF2_fnc,sF3_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f10124,f36958])).
% 143.38/33.43 fof(f37006,plain,(
% 143.38/33.43 join(sF3_fnc,meet(c,sF0_fnc))=join(sF2_fnc,sF3_fnc)),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f3394,f37005])).
% 143.38/33.43 fof(f37007,plain,(
% 143.38/33.43 join(sF3_fnc,meet(c,sF0_fnc))=sF3_fnc),
% 143.38/33.43 inference(forward_demodulation,[status(thm)],[f70,f37006])).
% 143.38/33.43 fof(f37623,plain,(
% 143.38/33.43 meet(sF4_fnc,join(sF1_fnc,sF4_fnc))=join(sF4_fnc,meet(b,sF0_fnc))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f562,f31593])).
% 143.38/33.43 fof(f37628,plain,(
% 143.38/33.43 meet(sF3_fnc,join(sF0_fnc,sF3_fnc))=join(sF3_fnc,meet(a,sF3_fnc))),
% 143.38/33.43 inference(paramodulation,[status(thm)],[f30711,f31593])).
% 143.38/33.44 fof(f37637,plain,(
% 143.38/33.44 meet(sF2_fnc,join(sF0_fnc,sF2_fnc))=join(sF2_fnc,meet(c,sF0_fnc))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f1414,f31593])).
% 143.38/33.44 fof(f37642,plain,(
% 143.38/33.44 meet(sF4_fnc,join(sF0_fnc,sF4_fnc))=join(sF4_fnc,meet(b,sF0_fnc))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f561,f31593])).
% 143.38/33.44 fof(f37643,plain,(
% 143.38/33.44 meet(sF1_fnc,join(sF0_fnc,sF1_fnc))=join(sF1_fnc,sF0_fnc)),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f324,f31593])).
% 143.38/33.44 fof(f37752,plain,(
% 143.38/33.44 ![X0,X1]: (meet(join(X0,X1),meet(X0,join(X1,X0)))=join(X0,meet(X1,X0)))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f31593,f28])).
% 143.38/33.44 fof(f37907,plain,(
% 143.38/33.44 meet(sF4_fnc,join(b,sF3_fnc))=join(sF4_fnc,meet(b,sF0_fnc))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f481,f37623])).
% 143.38/33.44 fof(f37910,plain,(
% 143.38/33.44 meet(b,sF0_fnc)=join(sF4_fnc,meet(b,sF0_fnc))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f34637,f37907])).
% 143.38/33.44 fof(f37932,plain,(
% 143.38/33.44 meet(sF3_fnc,join(sF0_fnc,sF3_fnc))=meet(sF3_fnc,join(a,sF3_fnc))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f31593,f37628])).
% 143.38/33.44 fof(f37975,plain,(
% 143.38/33.44 meet(sF2_fnc,join(sF0_fnc,sF2_fnc))=meet(c,sF0_fnc)),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f20473,f37637])).
% 143.38/33.44 fof(f37994,plain,(
% 143.38/33.44 meet(sF4_fnc,join(sF0_fnc,sF4_fnc))=meet(b,sF0_fnc)),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f37910,f37642])).
% 143.38/33.44 fof(f37996,plain,(
% 143.38/33.44 meet(sF1_fnc,join(sF0_fnc,sF1_fnc))=join(sF0_fnc,sF1_fnc)),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f14,f37643])).
% 143.38/33.44 fof(f38436,plain,(
% 143.38/33.44 ![X0,X1]: (meet(X0,meet(join(X1,X0),join(X0,X1)))=join(X0,meet(X1,X0)))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f131,f37752])).
% 143.38/33.44 fof(f38437,plain,(
% 143.38/33.44 ![X0,X1]: (meet(X0,join(X0,X1))=join(X0,meet(X1,X0)))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f11397,f38436])).
% 143.38/33.44 fof(f45932,plain,(
% 143.38/33.44 meet(join(sF4_fnc,sF0_fnc),sF3_fnc)=join(sF4_fnc,meet(sF0_fnc,c))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f34653,f242])).
% 143.38/33.44 fof(f45945,plain,(
% 143.38/33.44 meet(join(sF1_fnc,sF0_fnc),sF1_fnc)=join(sF1_fnc,meet(sF0_fnc,c))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f25012,f242])).
% 143.38/33.44 fof(f45946,plain,(
% 143.38/33.44 meet(join(sF3_fnc,sF0_fnc),sF3_fnc)=join(sF3_fnc,meet(sF0_fnc,c))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f37007,f242])).
% 143.38/33.44 fof(f46310,plain,(
% 143.38/33.44 meet(join(sF0_fnc,sF4_fnc),sF3_fnc)=join(sF4_fnc,meet(sF0_fnc,c))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f6815,f45932])).
% 143.38/33.44 fof(f46311,plain,(
% 143.38/33.44 meet(sF3_fnc,join(sF4_fnc,sF0_fnc))=join(sF4_fnc,meet(sF0_fnc,c))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f6645,f46310])).
% 143.38/33.44 fof(f46312,plain,(
% 143.38/33.44 meet(sF3_fnc,join(sF0_fnc,sF4_fnc))=join(sF4_fnc,meet(sF0_fnc,c))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f1620,f46311])).
% 143.38/33.44 fof(f46313,plain,(
% 143.38/33.44 meet(sF3_fnc,join(sF0_fnc,sF4_fnc))=join(sF4_fnc,meet(c,sF0_fnc))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f3394,f46312])).
% 143.38/33.44 fof(f46314,plain,(
% 143.38/33.44 meet(sF3_fnc,join(sF0_fnc,sF4_fnc))=sF3_fnc),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f34653,f46313])).
% 143.38/33.44 fof(f46376,plain,(
% 143.38/33.44 meet(join(sF0_fnc,sF1_fnc),sF1_fnc)=join(sF1_fnc,meet(sF0_fnc,c))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f6815,f45945])).
% 143.38/33.44 fof(f46377,plain,(
% 143.38/33.44 meet(sF1_fnc,join(sF1_fnc,sF0_fnc))=join(sF1_fnc,meet(sF0_fnc,c))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f6645,f46376])).
% 143.38/33.44 fof(f46378,plain,(
% 143.38/33.44 meet(sF1_fnc,join(sF0_fnc,sF1_fnc))=join(sF1_fnc,meet(sF0_fnc,c))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f1620,f46377])).
% 143.38/33.44 fof(f46379,plain,(
% 143.38/33.44 join(sF0_fnc,sF1_fnc)=join(sF1_fnc,meet(sF0_fnc,c))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f37996,f46378])).
% 143.38/33.44 fof(f46380,plain,(
% 143.38/33.44 join(sF0_fnc,sF1_fnc)=join(sF1_fnc,meet(c,sF0_fnc))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f3394,f46379])).
% 143.38/33.44 fof(f46401,plain,(
% 143.38/33.44 join(sF0_fnc,sF1_fnc)=sF1_fnc),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f25012,f46380])).
% 143.38/33.44 fof(f46402,plain,(
% 143.38/33.44 meet(join(sF0_fnc,sF3_fnc),sF3_fnc)=join(sF3_fnc,meet(sF0_fnc,c))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f6815,f45946])).
% 143.38/33.44 fof(f46403,plain,(
% 143.38/33.44 meet(sF3_fnc,join(sF3_fnc,sF0_fnc))=join(sF3_fnc,meet(sF0_fnc,c))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f6645,f46402])).
% 143.38/33.44 fof(f46404,plain,(
% 143.38/33.44 meet(sF3_fnc,join(sF0_fnc,sF3_fnc))=join(sF3_fnc,meet(sF0_fnc,c))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f1620,f46403])).
% 143.38/33.44 fof(f46405,plain,(
% 143.38/33.44 meet(sF3_fnc,join(a,sF3_fnc))=join(sF3_fnc,meet(sF0_fnc,c))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f37932,f46404])).
% 143.38/33.44 fof(f46406,plain,(
% 143.38/33.44 meet(sF3_fnc,join(a,sF3_fnc))=join(sF3_fnc,meet(c,sF0_fnc))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f3394,f46405])).
% 143.38/33.44 fof(f46407,plain,(
% 143.38/33.44 meet(sF3_fnc,join(sF0_fnc,sF3_fnc))=sF3_fnc),
% 143.38/33.44 inference(backward_demodulation,[status(thm)],[f46408,f37932])).
% 143.38/33.44 fof(f46408,plain,(
% 143.38/33.44 meet(sF3_fnc,join(a,sF3_fnc))=sF3_fnc),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f37007,f46406])).
% 143.38/33.44 fof(f49867,plain,(
% 143.38/33.44 ![X0]: (join(sF3_fnc,meet(join(sF0_fnc,sF4_fnc),join(sF3_fnc,X0)))=meet(join(sF0_fnc,sF4_fnc),join(sF3_fnc,X0)))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f46314,f174])).
% 143.38/33.44 fof(f49868,plain,(
% 143.38/33.44 ![X0]: (meet(join(sF0_fnc,sF4_fnc),meet(X0,sF3_fnc))=meet(sF3_fnc,X0))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f46314,f2226])).
% 143.38/33.44 fof(f49983,plain,(
% 143.38/33.44 ![X0]: (meet(sF3_fnc,meet(join(sF0_fnc,sF4_fnc),X0))=meet(sF3_fnc,X0))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f131,f49868])).
% 143.38/33.44 fof(f50408,plain,(
% 143.38/33.44 ![X0]: (join(sF3_fnc,meet(join(sF0_fnc,sF3_fnc),join(sF3_fnc,X0)))=meet(join(sF0_fnc,sF3_fnc),join(sF3_fnc,X0)))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f46407,f174])).
% 143.38/33.44 fof(f50517,plain,(
% 143.38/33.44 ![X0]: (join(sF3_fnc,meet(sF0_fnc,join(sF3_fnc,join(sF3_fnc,X0))))=meet(join(sF0_fnc,sF3_fnc),join(sF3_fnc,X0)))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f11458,f50408])).
% 143.38/33.44 fof(f50518,plain,(
% 143.38/33.44 ![X0]: (join(sF3_fnc,meet(sF0_fnc,join(X0,sF3_fnc)))=meet(join(sF0_fnc,sF3_fnc),join(sF3_fnc,X0)))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f901,f50517])).
% 143.38/33.44 fof(f59462,plain,(
% 143.38/33.44 meet(join(b,sF3_fnc),sF0_fnc)=meet(a,join(b,sF3_fnc))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f30505,f2199])).
% 143.38/33.44 fof(f59508,plain,(
% 143.38/33.44 meet(sF0_fnc,join(sF3_fnc,b))=meet(a,join(b,sF3_fnc))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f6645,f59462])).
% 143.38/33.44 fof(f59510,plain,(
% 143.38/33.44 meet(sF0_fnc,join(b,sF3_fnc))=meet(a,join(b,sF3_fnc))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f1620,f59508])).
% 143.38/33.44 fof(f60819,plain,(
% 143.38/33.44 meet(sF3_fnc,join(sF2_fnc,meet(b,sF0_fnc)))=join(sF2_fnc,meet(sF4_fnc,join(b,sF3_fnc)))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f34637,f223])).
% 143.38/33.44 fof(f60866,plain,(
% 143.38/33.44 meet(sF3_fnc,join(sF2_fnc,meet(b,sF0_fnc)))=join(sF2_fnc,meet(b,sF0_fnc))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f34637,f60819])).
% 143.38/33.44 fof(f61257,plain,(
% 143.38/33.44 join(meet(b,sF0_fnc),sF3_fnc)=join(sF2_fnc,meet(b,sF0_fnc))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f37910,f888])).
% 143.38/33.44 fof(f61318,plain,(
% 143.38/33.44 join(sF3_fnc,meet(sF0_fnc,b))=join(sF2_fnc,meet(b,sF0_fnc))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f10124,f61257])).
% 143.38/33.44 fof(f61321,plain,(
% 143.38/33.44 join(sF3_fnc,meet(b,sF0_fnc))=join(sF2_fnc,meet(b,sF0_fnc))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f3394,f61318])).
% 143.38/33.44 fof(f62362,plain,(
% 143.38/33.44 join(sF0_fnc,sF2_fnc)=join(sF0_fnc,meet(c,sF0_fnc))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f37975,f25315])).
% 143.38/33.44 fof(f62423,plain,(
% 143.38/33.44 join(sF0_fnc,sF2_fnc)=meet(sF0_fnc,join(sF0_fnc,c))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f38437,f62362])).
% 143.38/33.44 fof(f62424,plain,(
% 143.38/33.44 join(sF0_fnc,sF2_fnc)=meet(sF0_fnc,join(c,sF0_fnc))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f1620,f62423])).
% 143.38/33.44 fof(f62431,plain,(
% 143.38/33.44 join(sF0_fnc,sF2_fnc)=sF0_fnc),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f16267,f62424])).
% 143.38/33.44 fof(f62632,plain,(
% 143.38/33.44 join(sF0_fnc,sF1_fnc)=join(b,sF0_fnc)),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f62431,f1604])).
% 143.38/33.44 fof(f62699,plain,(
% 143.38/33.44 sF1_fnc=join(b,sF0_fnc)),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f46401,f62632])).
% 143.38/33.44 fof(f63339,plain,(
% 143.38/33.44 ![X0,X1]: (join(meet(join(X0,sF4_fnc),X1),sF3_fnc)=join(sF2_fnc,join(sF4_fnc,meet(X0,join(X1,sF4_fnc)))))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f627,f888])).
% 143.38/33.44 fof(f63975,plain,(
% 143.38/33.44 ![X0,X1]: (join(sF3_fnc,meet(X0,join(X1,sF4_fnc)))=join(sF2_fnc,join(sF4_fnc,meet(X1,join(X0,sF4_fnc)))))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f10124,f63339])).
% 143.38/33.44 fof(f63976,plain,(
% 143.38/33.44 ![X0,X1]: (join(sF3_fnc,meet(X0,join(X1,sF4_fnc)))=join(meet(X1,join(X0,sF4_fnc)),sF3_fnc))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f888,f63975])).
% 143.38/33.44 fof(f63977,plain,(
% 143.38/33.44 ![X0]: (join(sF3_fnc,meet(sF0_fnc,join(join(sF3_fnc,X0),sF4_fnc)))=meet(join(sF0_fnc,sF4_fnc),join(sF3_fnc,X0)))),
% 143.38/33.44 inference(backward_demodulation,[status(thm)],[f63989,f49867])).
% 143.38/33.44 fof(f63989,plain,(
% 143.38/33.44 ![X0,X1]: (join(sF3_fnc,meet(X0,join(X1,sF4_fnc)))=join(sF3_fnc,meet(join(X0,sF4_fnc),X1)))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f10124,f63976])).
% 143.38/33.44 fof(f64342,plain,(
% 143.38/33.44 ![X0]: (join(sF3_fnc,meet(sF0_fnc,join(sF4_fnc,join(sF3_fnc,X0))))=meet(join(sF0_fnc,sF4_fnc),join(sF3_fnc,X0)))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f6817,f63977])).
% 143.38/33.44 fof(f64343,plain,(
% 143.38/33.44 ![X0]: (join(sF3_fnc,meet(sF0_fnc,join(sF3_fnc,join(sF4_fnc,X0))))=meet(join(sF0_fnc,sF4_fnc),join(sF3_fnc,X0)))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f10770,f64342])).
% 143.38/33.44 fof(f64344,plain,(
% 143.38/33.44 ![X0]: (join(sF3_fnc,meet(sF0_fnc,join(X0,sF3_fnc)))=meet(join(sF0_fnc,sF4_fnc),join(sF3_fnc,X0)))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f883,f64343])).
% 143.38/33.44 fof(f64345,plain,(
% 143.38/33.44 ![X0]: (meet(join(sF0_fnc,sF3_fnc),join(sF3_fnc,X0))=meet(join(sF0_fnc,sF4_fnc),join(sF3_fnc,X0)))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f50518,f64344])).
% 143.38/33.44 fof(f70580,plain,(
% 143.38/33.44 join(sF0_fnc,sF4_fnc)=join(sF0_fnc,meet(b,sF0_fnc))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f37994,f25315])).
% 143.38/33.44 fof(f70656,plain,(
% 143.38/33.44 join(sF0_fnc,sF4_fnc)=meet(sF0_fnc,join(sF0_fnc,b))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f38437,f70580])).
% 143.38/33.44 fof(f70657,plain,(
% 143.38/33.44 join(sF0_fnc,sF4_fnc)=meet(sF0_fnc,join(b,sF0_fnc))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f1620,f70656])).
% 143.38/33.44 fof(f70658,plain,(
% 143.38/33.44 join(sF0_fnc,sF4_fnc)=meet(sF0_fnc,sF1_fnc)),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f62699,f70657])).
% 143.38/33.44 fof(f70662,plain,(
% 143.38/33.44 ![X0]: (meet(join(sF0_fnc,sF3_fnc),join(sF3_fnc,X0))=meet(sF0_fnc,join(sF3_fnc,X0)))),
% 143.38/33.44 inference(backward_demodulation,[status(thm)],[f70671,f64345])).
% 143.38/33.44 fof(f70663,plain,(
% 143.38/33.44 ![X0]: (meet(sF3_fnc,meet(sF0_fnc,X0))=meet(sF3_fnc,X0))),
% 143.38/33.44 inference(backward_demodulation,[status(thm)],[f70671,f49983])).
% 143.38/33.44 fof(f70671,plain,(
% 143.38/33.44 join(sF0_fnc,sF4_fnc)=sF0_fnc),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f324,f70658])).
% 143.38/33.44 fof(f70870,plain,(
% 143.38/33.44 ![X0]: (join(sF3_fnc,meet(sF0_fnc,join(X0,sF3_fnc)))=meet(sF0_fnc,join(sF3_fnc,X0)))),
% 143.38/33.44 inference(backward_demodulation,[status(thm)],[f70662,f50518])).
% 143.38/33.44 fof(f70872,plain,(
% 143.38/33.44 ![X0]: (meet(a,meet(X0,sF3_fnc))=meet(sF3_fnc,X0))),
% 143.38/33.44 inference(backward_demodulation,[status(thm)],[f70873,f30818])).
% 143.38/33.44 fof(f70873,plain,(
% 143.38/33.44 ![X0]: (meet(sF0_fnc,meet(X0,sF3_fnc))=meet(sF3_fnc,X0))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f131,f70663])).
% 143.38/33.44 fof(f71792,plain,(
% 143.38/33.44 join(sF0_fnc,sF3_fnc)=join(sF2_fnc,sF0_fnc)),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f70671,f3062])).
% 143.38/33.44 fof(f71850,plain,(
% 143.38/33.44 join(sF0_fnc,sF3_fnc)=join(sF0_fnc,sF2_fnc)),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f14,f71792])).
% 143.38/33.44 fof(f71857,plain,(
% 143.38/33.44 join(sF0_fnc,sF3_fnc)=sF0_fnc),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f62431,f71850])).
% 143.38/33.44 fof(f71979,plain,(
% 143.38/33.44 ![X0]: (join(sF3_fnc,meet(sF0_fnc,join(X0,sF3_fnc)))=join(sF3_fnc,meet(sF0_fnc,X0)))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f71857,f627])).
% 143.38/33.44 fof(f71988,plain,(
% 143.38/33.44 ![X0]: (meet(sF0_fnc,join(sF3_fnc,meet(sF0_fnc,X0)))=join(sF3_fnc,meet(sF0_fnc,X0)))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f71857,f228])).
% 143.38/33.44 fof(f72019,plain,(
% 143.38/33.44 ![X0]: (join(sF3_fnc,meet(join(X0,sF3_fnc),sF0_fnc))=join(sF3_fnc,meet(sF0_fnc,X0)))),
% 143.38/33.44 inference(paramodulation,[status(thm)],[f71857,f30])).
% 143.38/33.44 fof(f72041,plain,(
% 143.38/33.44 ![X0]: (meet(sF0_fnc,join(sF3_fnc,X0))=join(sF3_fnc,meet(sF0_fnc,X0)))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f70870,f71979])).
% 143.38/33.44 fof(f72062,plain,(
% 143.38/33.44 ![X0]: (meet(sF0_fnc,meet(sF0_fnc,join(sF3_fnc,X0)))=join(sF3_fnc,meet(sF0_fnc,X0)))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f72041,f71988])).
% 143.38/33.44 fof(f72063,plain,(
% 143.38/33.44 ![X0]: (meet(join(sF3_fnc,X0),sF0_fnc)=join(sF3_fnc,meet(sF0_fnc,X0)))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f2211,f72062])).
% 143.38/33.44 fof(f72064,plain,(
% 143.38/33.44 ![X0]: (meet(sF0_fnc,join(X0,sF3_fnc))=join(sF3_fnc,meet(sF0_fnc,X0)))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f6645,f72063])).
% 143.38/33.44 fof(f72122,plain,(
% 143.38/33.44 ![X0]: (join(sF3_fnc,meet(X0,join(sF0_fnc,sF3_fnc)))=join(sF3_fnc,meet(sF0_fnc,X0)))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f627,f72019])).
% 143.38/33.44 fof(f72123,plain,(
% 143.38/33.44 ![X0]: (join(sF3_fnc,meet(X0,sF0_fnc))=join(sF3_fnc,meet(sF0_fnc,X0)))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f71857,f72122])).
% 143.38/33.44 fof(f72125,plain,(
% 143.38/33.44 meet(sF0_fnc,join(b,sF3_fnc))=join(sF2_fnc,meet(b,sF0_fnc))),
% 143.38/33.44 inference(backward_demodulation,[status(thm)],[f72127,f61321])).
% 143.38/33.44 fof(f72127,plain,(
% 143.38/33.44 ![X0]: (join(sF3_fnc,meet(X0,sF0_fnc))=meet(sF0_fnc,join(X0,sF3_fnc)))),
% 143.38/33.44 inference(forward_demodulation,[status(thm)],[f72064,f72123])).
% 143.38/33.44 fof(f72137,plain,(
% 143.38/33.44 meet(sF3_fnc,join(sF2_fnc,meet(b,sF0_fnc)))=meet(a,join(b,sF3_fnc))),
% 143.38/33.44 inference(backward_demodulation,[status(thm)],[f72138,f60866])).
% 144.14/33.50 fof(f72138,plain,(
% 144.14/33.50 meet(a,join(b,sF3_fnc))=join(sF2_fnc,meet(b,sF0_fnc))),
% 144.14/33.50 inference(forward_demodulation,[status(thm)],[f59510,f72125])).
% 144.14/33.50 fof(f72152,plain,(
% 144.14/33.50 meet(sF3_fnc,meet(a,join(b,sF3_fnc)))=meet(a,join(b,sF3_fnc))),
% 144.14/33.50 inference(forward_demodulation,[status(thm)],[f72138,f72137])).
% 144.14/33.50 fof(f72153,plain,(
% 144.14/33.50 meet(a,meet(join(b,sF3_fnc),sF3_fnc))=meet(a,join(b,sF3_fnc))),
% 144.14/33.50 inference(forward_demodulation,[status(thm)],[f131,f72152])).
% 144.14/33.50 fof(f72154,plain,(
% 144.14/33.50 meet(sF3_fnc,join(b,sF3_fnc))=meet(a,join(b,sF3_fnc))),
% 144.14/33.50 inference(forward_demodulation,[status(thm)],[f70872,f72153])).
% 144.14/33.50 fof(f72157,plain,(
% 144.14/33.50 join(sF0_fnc,meet(a,join(b,sF3_fnc)))=sF3_fnc),
% 144.14/33.50 inference(backward_demodulation,[status(thm)],[f72158,f4968])).
% 144.14/33.50 fof(f72158,plain,(
% 144.14/33.50 sF3_fnc=meet(a,join(b,sF3_fnc))),
% 144.14/33.50 inference(forward_demodulation,[status(thm)],[f30510,f72154])).
% 144.14/33.50 fof(f72159,plain,(
% 144.14/33.50 join(sF0_fnc,sF3_fnc)=sF3_fnc),
% 144.14/33.50 inference(forward_demodulation,[status(thm)],[f72158,f72157])).
% 144.14/33.50 fof(f72160,plain,(
% 144.14/33.50 sF0_fnc=sF3_fnc),
% 144.14/33.50 inference(forward_demodulation,[status(thm)],[f71857,f72159])).
% 144.14/33.50 fof(f72161,plain,(
% 144.14/33.50 $false),
% 144.14/33.50 inference(forward_subsumption_resolution,[status(thm)],[f72160,f26])).
% 144.14/33.50 % SZS output end CNFRefutation for theBenchmark.p
% 145.86/45.53 % Elapsed time: 44.954653 seconds
% 145.86/45.53 % CPU time: 271.679217 seconds
% 145.86/45.53 % Total memory used: 72.994 GB
% 145.86/45.53 % Net memory used: 72.986 GB
%------------------------------------------------------------------------------