%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT005-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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:07 PM UTC 2026
% Result : Unsatisfiable 144.22s 29.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT005-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/11.21 % Computer : n013.cluster.edu
% 0.11/11.21 % Model : x86_64 x86_64
% 0.11/11.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/11.21 % Memory : 8046.5625MB
% 0.11/11.21 % OS : Linux 6.8.0-71-generic
% 0.11/11.21 % CPULimit : 300
% 0.11/11.21 % WCLimit : 300
% 0.11/11.21 % DateTime : Sun Sep 20 23:05:20 UTC 2026
% 0.11/11.21 % CPUTime :
% 0.11/11.22 % Drodi V4.1.1
% 144.22/29.51 % Refutation found
% 144.22/29.51 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 144.22/29.51 % SZS output start CNFRefutation for theBenchmark
% 144.22/29.51 fof(f1,axiom,(
% 144.22/29.51 (![A,B,C]: (ifeq3(A,A,B,C) = B ))),
% 144.22/29.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.22/29.51 fof(f3,axiom,(
% 144.22/29.51 (![A,B,C]: (ifeq(A,A,B,C) = B ))),
% 144.22/29.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.22/29.51 fof(f4,axiom,(
% 144.22/29.51 (![X]: (meet(X,X) = X ))),
% 144.22/29.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.22/29.51 fof(f5,axiom,(
% 144.22/29.51 (![X]: (join(X,X) = X ))),
% 144.22/29.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.22/29.51 fof(f6,axiom,(
% 144.22/29.51 (![X,Y]: (meet(X,join(X,Y)) = X ))),
% 144.22/29.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.22/29.51 fof(f7,axiom,(
% 144.22/29.51 (![X,Y]: (join(X,meet(X,Y)) = X ))),
% 144.22/29.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.22/29.51 fof(f8,axiom,(
% 144.22/29.51 (![X,Y]: (meet(X,Y) = meet(Y,X) ))),
% 144.22/29.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.22/29.51 fof(f9,axiom,(
% 144.22/29.51 (![X,Y]: (join(X,Y) = join(Y,X) ))),
% 144.22/29.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.22/29.51 fof(f10,axiom,(
% 144.22/29.51 (![X,Y,Z]: (meet(meet(X,Y),Z) = meet(X,meet(Y,Z)) ))),
% 144.22/29.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.22/29.51 fof(f11,axiom,(
% 144.22/29.51 (![X,Y,Z]: (join(join(X,Y),Z) = join(X,join(Y,Z)) ))),
% 144.22/29.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.22/29.51 fof(f12,axiom,(
% 144.22/29.51 (![X]: (meet(X,n0) = n0 ))),
% 144.22/29.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.22/29.51 fof(f13,axiom,(
% 144.22/29.51 (![X]: (join(X,n0) = X ))),
% 144.22/29.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.22/29.51 fof(f16,axiom,(
% 144.22/29.51 (![X,Z,Y]: (ifeq3(meet(X,Z),X,meet(Z,join(X,Y)),join(X,meet(Y,Z))) = join(X,meet(Y,Z)) ))),
% 144.22/29.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.22/29.51 fof(f17,axiom,(
% 144.22/29.51 (![X,Y]: (ifeq(complement(X,Y),true,meet(X,Y),n0) = n0 ))),
% 144.22/29.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.22/29.51 fof(f20,hypothesis,(
% 144.22/29.51 complement(r1,join(a,b)) = true ),
% 144.22/29.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.22/29.51 fof(f21,hypothesis,(
% 144.22/29.51 complement(r2,meet(a,b)) = true ),
% 144.22/29.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.22/29.51 fof(f22,negated_conjecture,(
% 144.22/29.51 r1 != meet(join(r1,meet(r2,b)),join(r1,meet(r2,a))) ),
% 144.22/29.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.22/29.51 fof(f23,plain,(
% 144.22/29.51 ![X0,X1,X2]: (ifeq3(X0,X0,X1,X2)=X1)),
% 144.22/29.51 inference(cnf_transformation,[status(thm)],[f1])).
% 144.22/29.51 fof(f25,plain,(
% 144.22/29.51 ![X0,X1,X2]: (ifeq(X0,X0,X1,X2)=X1)),
% 144.22/29.51 inference(cnf_transformation,[status(thm)],[f3])).
% 144.22/29.51 fof(f26,plain,(
% 144.22/29.51 ![X0]: (meet(X0,X0)=X0)),
% 144.22/29.51 inference(cnf_transformation,[status(thm)],[f4])).
% 144.22/29.51 fof(f27,plain,(
% 144.22/29.51 ![X0]: (join(X0,X0)=X0)),
% 144.22/29.51 inference(cnf_transformation,[status(thm)],[f5])).
% 144.22/29.51 fof(f28,plain,(
% 144.22/29.51 ![X0,X1]: (meet(X0,join(X0,X1))=X0)),
% 144.22/29.51 inference(cnf_transformation,[status(thm)],[f6])).
% 144.22/29.51 fof(f29,plain,(
% 144.22/29.51 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 144.22/29.51 inference(cnf_transformation,[status(thm)],[f7])).
% 144.22/29.51 fof(f30,plain,(
% 144.22/29.51 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 144.22/29.51 inference(cnf_transformation,[status(thm)],[f8])).
% 144.22/29.51 fof(f31,plain,(
% 144.22/29.51 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 144.22/29.51 inference(cnf_transformation,[status(thm)],[f9])).
% 144.22/29.51 fof(f32,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X0,meet(X1,X2)))),
% 144.22/29.51 inference(cnf_transformation,[status(thm)],[f10])).
% 144.22/29.51 fof(f33,plain,(
% 144.22/29.51 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X0,join(X1,X2)))),
% 144.22/29.51 inference(cnf_transformation,[status(thm)],[f11])).
% 144.22/29.51 fof(f34,plain,(
% 144.22/29.51 ![X0]: (meet(X0,n0)=n0)),
% 144.22/29.51 inference(cnf_transformation,[status(thm)],[f12])).
% 144.22/29.51 fof(f35,plain,(
% 144.22/29.51 ![X0]: (join(X0,n0)=X0)),
% 144.22/29.51 inference(cnf_transformation,[status(thm)],[f13])).
% 144.22/29.51 fof(f38,plain,(
% 144.22/29.51 ![X0,X1,X2]: (ifeq3(meet(X0,X1),X0,meet(X1,join(X0,X2)),join(X0,meet(X2,X1)))=join(X0,meet(X2,X1)))),
% 144.22/29.51 inference(cnf_transformation,[status(thm)],[f16])).
% 144.22/29.51 fof(f39,plain,(
% 144.22/29.51 ![X0,X1]: (ifeq(complement(X0,X1),true,meet(X0,X1),n0)=n0)),
% 144.22/29.51 inference(cnf_transformation,[status(thm)],[f17])).
% 144.22/29.51 fof(f42,plain,(
% 144.22/29.51 complement(r1,join(a,b))=true),
% 144.22/29.51 inference(cnf_transformation,[status(thm)],[f20])).
% 144.22/29.51 fof(f43,plain,(
% 144.22/29.51 complement(r2,meet(a,b))=true),
% 144.22/29.51 inference(cnf_transformation,[status(thm)],[f21])).
% 144.22/29.51 fof(f44,plain,(
% 144.22/29.51 ~r1=meet(join(r1,meet(r2,b)),join(r1,meet(r2,a)))),
% 144.22/29.51 inference(cnf_transformation,[status(thm)],[f22])).
% 144.22/29.51 fof(f45,definition,(
% 144.22/29.51 sF2_fnc=meet(r2,b)),
% 144.22/29.51 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 144.22/29.51 fof(f46,definition,(
% 144.22/29.51 sF1_fnc=join(r1,sF2_fnc)),
% 144.22/29.51 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 144.22/29.51 fof(f47,definition,(
% 144.22/29.51 sF4_fnc=meet(r2,a)),
% 144.22/29.51 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 144.22/29.51 fof(f48,definition,(
% 144.22/29.51 sF3_fnc=join(r1,sF4_fnc)),
% 144.22/29.51 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 144.22/29.51 fof(f49,definition,(
% 144.22/29.51 sF0_fnc=meet(sF1_fnc,sF3_fnc)),
% 144.22/29.51 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 144.22/29.51 fof(f50,plain,(
% 144.22/29.51 ~r1=sF0_fnc),
% 144.22/29.51 inference(definition_folding,[],[f44,f49,f48,f47,f46,f45])).
% 144.22/29.51 fof(f51,plain,(
% 144.22/29.51 meet(r1,sF3_fnc)=r1),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f48,f28])).
% 144.22/29.51 fof(f52,plain,(
% 144.22/29.51 meet(r1,sF1_fnc)=r1),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f46,f28])).
% 144.22/29.51 fof(f56,plain,(
% 144.22/29.51 join(sF1_fnc,sF0_fnc)=sF1_fnc),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f49,f29])).
% 144.22/29.51 fof(f69,plain,(
% 144.22/29.51 ![X0]: (meet(r1,X0)=meet(r1,meet(sF3_fnc,X0)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f51,f32])).
% 144.22/29.51 fof(f70,plain,(
% 144.22/29.51 ![X0]: (meet(sF0_fnc,X0)=meet(sF1_fnc,meet(sF3_fnc,X0)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f49,f32])).
% 144.22/29.51 fof(f71,plain,(
% 144.22/29.51 ![X0]: (meet(sF4_fnc,X0)=meet(r2,meet(a,X0)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f47,f32])).
% 144.22/29.51 fof(f72,plain,(
% 144.22/29.51 ![X0]: (meet(sF2_fnc,X0)=meet(r2,meet(b,X0)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f45,f32])).
% 144.22/29.51 fof(f73,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(X0,X1)=meet(X0,meet(join(X0,X2),X1)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f28,f32])).
% 144.22/29.51 fof(f74,plain,(
% 144.22/29.51 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X0,X1)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f26,f32])).
% 144.22/29.51 fof(f113,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X2,meet(X0,X1)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f32,f30])).
% 144.22/29.51 fof(f129,plain,(
% 144.22/29.51 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X1,X0)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f30,f74])).
% 144.22/29.51 fof(f130,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X1,meet(X0,X2)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f30,f32])).
% 144.22/29.51 fof(f131,plain,(
% 144.22/29.51 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f30,f29])).
% 144.22/29.51 fof(f147,plain,(
% 144.22/29.51 ![X0,X1]: (meet(X0,join(X1,X0))=X0)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f31,f28])).
% 144.22/29.51 fof(f150,plain,(
% 144.22/29.51 ![X0]: (join(n0,X0)=X0)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f31,f35])).
% 144.22/29.51 fof(f244,plain,(
% 144.22/29.51 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X1,join(X2,X0)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f31,f33])).
% 144.22/29.51 fof(f260,plain,(
% 144.22/29.51 ![X0,X1,X2]: (join(X0,X1)=join(X0,join(meet(X0,X2),X1)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f29,f33])).
% 144.22/29.51 fof(f261,plain,(
% 144.22/29.51 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X0,X2)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f31,f33])).
% 144.22/29.51 fof(f263,plain,(
% 144.22/29.51 ![X0,X1]: (join(X0,X1)=join(X0,join(X0,X1)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f27,f33])).
% 144.22/29.51 fof(f283,plain,(
% 144.22/29.51 ![X0,X1,X2,X3]: (ifeq3(meet(X0,meet(X1,X2)),meet(X0,X1),meet(X2,join(meet(X0,X1),X3)),join(meet(X0,X1),meet(X3,X2)))=join(meet(X0,X1),meet(X3,X2)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f32,f38])).
% 144.22/29.51 fof(f295,plain,(
% 144.22/29.51 ![X0,X1,X2]: (ifeq3(X0,X0,meet(join(X0,X1),join(X0,X2)),join(X0,meet(X2,join(X0,X1))))=join(X0,meet(X2,join(X0,X1))))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f28,f38])).
% 144.22/29.51 fof(f313,plain,(
% 144.22/29.51 ![X0]: (ifeq3(meet(r1,X0),r1,meet(X0,sF3_fnc),join(r1,meet(sF4_fnc,X0)))=join(r1,meet(sF4_fnc,X0)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f48,f38])).
% 144.22/29.51 fof(f314,plain,(
% 144.22/29.51 ![X0]: (ifeq3(meet(r1,X0),r1,meet(X0,sF1_fnc),join(r1,meet(sF2_fnc,X0)))=join(r1,meet(sF2_fnc,X0)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f46,f38])).
% 144.22/29.51 fof(f327,plain,(
% 144.22/29.51 ![X0,X1]: (ifeq3(meet(meet(X0,X1),X1),meet(X0,X1),meet(X1,join(meet(X0,X1),X0)),meet(X0,X1))=join(meet(X0,X1),meet(X0,X1)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f27,f38])).
% 144.22/29.51 fof(f337,plain,(
% 144.22/29.51 ![X0]: (ifeq3(meet(X0,sF3_fnc),X0,meet(sF3_fnc,join(X0,sF1_fnc)),join(X0,sF0_fnc))=join(X0,meet(sF1_fnc,sF3_fnc)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f49,f38])).
% 144.22/29.51 fof(f360,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,X2))=join(X0,meet(X2,join(X0,X1))))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f23,f295])).
% 144.22/29.51 fof(f402,plain,(
% 144.22/29.51 ![X0,X1]: (ifeq3(meet(X0,meet(X1,X1)),meet(X0,X1),meet(X1,join(meet(X0,X1),X0)),meet(X0,X1))=join(meet(X0,X1),meet(X0,X1)))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f32,f327])).
% 144.22/29.51 fof(f403,plain,(
% 144.22/29.51 ![X0,X1]: (ifeq3(meet(X0,X1),meet(X0,X1),meet(X1,join(meet(X0,X1),X0)),meet(X0,X1))=join(meet(X0,X1),meet(X0,X1)))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f26,f402])).
% 144.22/29.51 fof(f404,plain,(
% 144.22/29.51 ![X0,X1]: (meet(X0,join(meet(X1,X0),X1))=join(meet(X1,X0),meet(X1,X0)))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f23,f403])).
% 144.22/29.51 fof(f405,plain,(
% 144.22/29.51 ![X0,X1]: (meet(X0,join(meet(X1,X0),X1))=meet(X1,X0))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f27,f404])).
% 144.22/29.51 fof(f415,plain,(
% 144.22/29.51 ![X0]: (ifeq3(meet(X0,sF3_fnc),X0,meet(sF3_fnc,join(X0,sF1_fnc)),join(X0,sF0_fnc))=join(X0,sF0_fnc))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f49,f337])).
% 144.22/29.51 fof(f517,plain,(
% 144.22/29.51 meet(sF0_fnc,sF3_fnc)=meet(sF1_fnc,sF3_fnc)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f26,f70])).
% 144.22/29.51 fof(f528,plain,(
% 144.22/29.51 meet(sF0_fnc,sF3_fnc)=sF0_fnc),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f49,f517])).
% 144.22/29.51 fof(f702,plain,(
% 144.22/29.51 ![X0,X1]: (join(X0,X1)=join(X0,join(X1,X0)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f31,f263])).
% 144.22/29.51 fof(f756,plain,(
% 144.22/29.51 join(sF4_fnc,r1)=join(sF4_fnc,sF3_fnc)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f48,f702])).
% 144.22/29.51 fof(f757,plain,(
% 144.22/29.51 join(sF2_fnc,r1)=join(sF2_fnc,sF1_fnc)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f46,f702])).
% 144.22/29.51 fof(f821,plain,(
% 144.22/29.51 join(sF2_fnc,r1)=join(sF1_fnc,sF2_fnc)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f31,f757])).
% 144.22/29.51 fof(f837,plain,(
% 144.22/29.51 join(r1,sF2_fnc)=join(sF1_fnc,sF2_fnc)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f31,f821])).
% 144.22/29.51 fof(f846,plain,(
% 144.22/29.51 join(sF2_fnc,r1)=sF1_fnc),
% 144.22/29.51 inference(backward_demodulation,[status(thm)],[f847,f821])).
% 144.22/29.51 fof(f847,plain,(
% 144.22/29.51 sF1_fnc=join(sF1_fnc,sF2_fnc)),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f46,f837])).
% 144.22/29.51 fof(f859,plain,(
% 144.22/29.51 ifeq(true,true,meet(r1,join(a,b)),n0)=n0),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f42,f39])).
% 144.22/29.51 fof(f860,plain,(
% 144.22/29.51 meet(r1,join(a,b))=n0),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f25,f859])).
% 144.22/29.51 fof(f861,plain,(
% 144.22/29.51 ifeq(true,true,meet(r2,meet(a,b)),n0)=n0),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f43,f39])).
% 144.22/29.51 fof(f862,plain,(
% 144.22/29.51 meet(r2,meet(a,b))=n0),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f25,f861])).
% 144.22/29.51 fof(f863,plain,(
% 144.22/29.51 meet(sF4_fnc,b)=n0),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f71,f862])).
% 144.22/29.51 fof(f939,plain,(
% 144.22/29.51 join(sF4_fnc,r1)=join(sF3_fnc,sF4_fnc)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f31,f756])).
% 144.22/29.51 fof(f956,plain,(
% 144.22/29.51 join(r1,sF4_fnc)=join(sF3_fnc,sF4_fnc)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f31,f939])).
% 144.22/29.51 fof(f959,plain,(
% 144.22/29.51 join(sF4_fnc,r1)=join(sF4_fnc,join(sF3_fnc,sF4_fnc))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f939,f263])).
% 144.22/29.51 fof(f965,plain,(
% 144.22/29.51 join(sF4_fnc,r1)=sF3_fnc),
% 144.22/29.51 inference(backward_demodulation,[status(thm)],[f966,f939])).
% 144.22/29.51 fof(f966,plain,(
% 144.22/29.51 sF3_fnc=join(sF3_fnc,sF4_fnc)),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f48,f956])).
% 144.22/29.51 fof(f970,plain,(
% 144.22/29.51 join(sF3_fnc,sF4_fnc)=join(sF4_fnc,join(sF3_fnc,sF4_fnc))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f939,f959])).
% 144.22/29.51 fof(f971,plain,(
% 144.22/29.51 sF3_fnc=join(sF4_fnc,join(sF3_fnc,sF4_fnc))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f966,f970])).
% 144.22/29.51 fof(f972,plain,(
% 144.22/29.51 sF3_fnc=join(sF4_fnc,sF3_fnc)),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f702,f971])).
% 144.22/29.51 fof(f986,plain,(
% 144.22/29.51 meet(sF4_fnc,sF3_fnc)=sF4_fnc),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f965,f28])).
% 144.22/29.51 fof(f1066,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(X0,join(X1,join(X2,X0)))=X0)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f33,f147])).
% 144.22/29.51 fof(f1103,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(X0,X1)=meet(X0,meet(join(X2,X0),X1)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f147,f32])).
% 144.22/29.51 fof(f2433,plain,(
% 144.22/29.51 meet(join(a,b),r1)=meet(join(a,b),n0)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f860,f129])).
% 144.22/29.51 fof(f2443,plain,(
% 144.22/29.51 meet(sF3_fnc,sF1_fnc)=meet(sF3_fnc,sF0_fnc)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f49,f129])).
% 144.22/29.51 fof(f2512,plain,(
% 144.22/29.51 meet(join(a,b),r1)=n0),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f34,f2433])).
% 144.22/29.51 fof(f2606,plain,(
% 144.22/29.51 meet(r1,sF1_fnc)=meet(r1,meet(sF3_fnc,sF0_fnc))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f2443,f69])).
% 144.22/29.51 fof(f2628,plain,(
% 144.22/29.51 r1=meet(r1,meet(sF3_fnc,sF0_fnc))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f52,f2606])).
% 144.22/29.51 fof(f2629,plain,(
% 144.22/29.51 r1=meet(r1,sF0_fnc)),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f69,f2628])).
% 144.22/29.51 fof(f2657,plain,(
% 144.22/29.51 join(sF0_fnc,r1)=sF0_fnc),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f2629,f131])).
% 144.22/29.51 fof(f2928,plain,(
% 144.22/29.51 ![X0]: (meet(r1,join(X0,sF1_fnc))=r1)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f846,f1066])).
% 144.22/29.51 fof(f2941,plain,(
% 144.22/29.51 ![X0]: (meet(r1,join(X0,sF0_fnc))=r1)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f2657,f1066])).
% 144.22/29.51 fof(f2952,plain,(
% 144.22/29.51 ![X0]: (meet(sF0_fnc,join(X0,sF1_fnc))=sF0_fnc)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f56,f1066])).
% 144.22/29.51 fof(f3337,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X1,meet(X2,X0)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f30,f113])).
% 144.22/29.51 fof(f3404,plain,(
% 144.22/29.51 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X0,X1)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f26,f113])).
% 144.22/29.51 fof(f3446,plain,(
% 144.22/29.51 ![X0]: (meet(sF0_fnc,meet(sF3_fnc,X0))=meet(X0,sF0_fnc))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f528,f113])).
% 144.22/29.51 fof(f3479,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(X0,meet(join(X1,X0),X2))=meet(X2,X0))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f147,f113])).
% 144.22/29.51 fof(f3483,plain,(
% 144.22/29.51 ![X0,X1]: (meet(X0,meet(X0,X1))=meet(X1,X0))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f26,f113])).
% 144.22/29.51 fof(f4456,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(X0,X0)=meet(join(X1,join(X2,X0)),X0))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f1066,f3483])).
% 144.22/29.51 fof(f4457,plain,(
% 144.22/29.51 ![X0,X1]: (meet(X0,X0)=meet(join(X1,X0),X0))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f147,f3483])).
% 144.22/29.51 fof(f4607,plain,(
% 144.22/29.51 ![X0,X1,X2]: (X0=meet(join(X1,join(X2,X0)),X0))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f26,f4456])).
% 144.22/29.51 fof(f4609,plain,(
% 144.22/29.51 ![X0,X1]: (X0=meet(join(X1,X0),X0))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f26,f4457])).
% 144.22/29.51 fof(f4936,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(join(X0,X1),meet(X1,X2))=meet(X2,X1))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f4609,f113])).
% 144.22/29.51 fof(f5337,plain,(
% 144.22/29.51 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(join(X1,X0),join(X0,X2)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f702,f261])).
% 144.22/29.51 fof(f5425,plain,(
% 144.22/29.51 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),join(X1,X2)))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f261,f5337])).
% 144.22/29.51 fof(f5426,plain,(
% 144.22/29.51 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X1,join(X0,join(X1,X2))))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f261,f5425])).
% 144.22/29.51 fof(f5573,plain,(
% 144.22/29.51 ![X0,X1]: (join(join(meet(X0,X1),X0),meet(X0,X1))=join(meet(X0,X1),X0))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f405,f131])).
% 144.22/29.51 fof(f5732,plain,(
% 144.22/29.51 ![X0,X1]: (join(X0,join(meet(X0,X1),meet(X0,X1)))=join(meet(X0,X1),X0))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f261,f5573])).
% 144.22/29.51 fof(f5733,plain,(
% 144.22/29.51 ![X0,X1]: (join(X0,meet(X0,X1))=join(meet(X0,X1),X0))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f260,f5732])).
% 144.22/29.51 fof(f5750,plain,(
% 144.22/29.51 ![X0,X1]: (X0=join(meet(X0,X1),X0))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f29,f5733])).
% 144.22/29.51 fof(f5832,plain,(
% 144.22/29.51 ![X0,X1]: (join(X0,X1)=join(X0,join(X1,join(X0,X1))))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f27,f244])).
% 144.22/29.51 fof(f5885,plain,(
% 144.22/29.51 ![X0,X1]: (join(X0,X1)=join(X1,join(X1,X0)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f27,f244])).
% 144.22/29.51 fof(f6038,plain,(
% 144.22/29.51 ![X0,X1]: (join(X0,X1)=join(X1,join(X0,X1)))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f5426,f5832])).
% 144.22/29.51 fof(f6329,plain,(
% 144.22/29.51 ![X0,X1]: (X0=join(meet(X1,X0),X0))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f3483,f5750])).
% 144.22/29.51 fof(f6330,plain,(
% 144.22/29.51 ![X0,X1,X2]: (X0=join(meet(X1,meet(X2,X0)),X0))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f113,f5750])).
% 144.22/29.51 fof(f6355,plain,(
% 144.22/29.51 ![X0,X1,X2]: (join(X0,X1)=join(meet(X1,X2),join(X1,X0)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f5750,f244])).
% 144.22/29.51 fof(f6584,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(join(X0,X1),X2)=join(meet(X0,X2),meet(join(X0,X1),X2)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f73,f6329])).
% 144.22/29.51 fof(f6613,plain,(
% 144.22/29.51 ![X0,X1,X2]: (join(X0,X1)=join(meet(X2,X1),join(X1,X0)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f6329,f244])).
% 144.22/29.51 fof(f6717,plain,(
% 144.22/29.51 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X2,join(X0,join(X1,X2))))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f244,f5885])).
% 144.22/29.51 fof(f6843,plain,(
% 144.22/29.51 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X1,join(X0,X2))))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f261,f6717])).
% 144.22/29.51 fof(f6882,plain,(
% 144.22/29.51 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X1,join(X2,join(X0,join(X1,X2)))))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f33,f6038])).
% 144.22/29.51 fof(f7000,plain,(
% 144.22/29.51 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X1,join(X1,join(X0,X2))))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f6843,f6882])).
% 144.22/29.51 fof(f7001,plain,(
% 144.22/29.51 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X2),X1))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f5885,f7000])).
% 144.22/29.51 fof(f7174,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X2,meet(X0,meet(X1,X2))))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f32,f3404])).
% 144.22/29.51 fof(f7226,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X1,meet(X2,meet(X0,meet(X1,X2)))))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f3404,f32])).
% 144.22/29.51 fof(f7310,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X2,meet(X1,meet(X0,X2))))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f130,f7174])).
% 144.22/29.51 fof(f7379,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X1,meet(X1,meet(X0,X2))))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f7310,f7226])).
% 144.22/29.51 fof(f7380,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(meet(X0,X2),X1))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f3483,f7379])).
% 144.22/29.51 fof(f8233,plain,(
% 144.22/29.51 ![X0,X1,X2]: (ifeq3(meet(X0,X1),meet(X0,X1),meet(X1,join(meet(X0,X1),X2)),join(meet(X0,X1),meet(X2,X1)))=join(meet(X0,X1),meet(X2,X1)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f26,f283])).
% 144.22/29.51 fof(f8753,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(join(X0,X1),X2)=meet(X2,join(meet(X0,X2),join(X0,X1))))),
% 144.22/29.51 inference(backward_demodulation,[status(thm)],[f8754,f6584])).
% 144.22/29.51 fof(f8754,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),X2))=join(meet(X1,X0),meet(X2,X0)))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f23,f8233])).
% 144.22/29.51 fof(f10060,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(join(X0,X1),X2)=meet(X2,join(X1,X0)))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f6355,f8753])).
% 144.22/29.51 fof(f11213,plain,(
% 144.22/29.51 ![X0]: (sF0_fnc=join(meet(X0,r1),sF0_fnc))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f2629,f6330])).
% 144.22/29.51 fof(f13103,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(meet(X0,X1),meet(X2,X1)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f3404,f3337])).
% 144.22/29.51 fof(f13112,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(X0,X1)=meet(join(X0,X2),meet(X1,X0)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f28,f3337])).
% 144.22/29.51 fof(f13275,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(meet(X2,X0),meet(X1,X0)))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f3337,f13103])).
% 144.22/29.51 fof(f13276,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X0,meet(meet(X1,X0),X2)))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f3337,f13275])).
% 144.22/29.51 fof(f13277,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X0,meet(X0,meet(X2,X1))))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f3337,f13276])).
% 144.22/29.51 fof(f13278,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(meet(X2,X1),X0))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f3483,f13277])).
% 144.22/29.51 fof(f13408,plain,(
% 144.22/29.51 meet(b,r1)=meet(b,n0)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f2512,f1103])).
% 144.22/29.51 fof(f13583,plain,(
% 144.22/29.51 meet(b,r1)=n0),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f34,f13408])).
% 144.22/29.51 fof(f36521,plain,(
% 144.22/29.51 n0=meet(r1,join(b,a))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f2512,f10060])).
% 144.22/29.51 fof(f36542,plain,(
% 144.22/29.51 ![X0,X1,X2]: (meet(X0,join(X1,X2))=meet(X0,join(X2,X1)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f30,f10060])).
% 144.22/29.51 fof(f41521,plain,(
% 144.22/29.51 ifeq3(sF4_fnc,sF4_fnc,meet(sF3_fnc,join(sF4_fnc,sF1_fnc)),join(sF4_fnc,sF0_fnc))=join(sF4_fnc,sF0_fnc)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f986,f415])).
% 144.22/29.51 fof(f41639,plain,(
% 144.22/29.51 meet(sF3_fnc,join(sF4_fnc,sF1_fnc))=join(sF4_fnc,sF0_fnc)),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f23,f41521])).
% 144.22/29.51 fof(f41758,plain,(
% 144.22/29.51 meet(join(b,a),join(b,r1))=join(b,n0)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f36521,f360])).
% 144.22/29.51 fof(f41842,plain,(
% 144.22/29.51 meet(join(b,a),join(b,r1))=b),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f35,f41758])).
% 144.22/29.51 fof(f56436,plain,(
% 144.22/29.51 meet(sF0_fnc,join(sF4_fnc,sF1_fnc))=meet(sF1_fnc,join(sF4_fnc,sF0_fnc))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f41639,f70])).
% 144.22/29.51 fof(f56446,plain,(
% 144.22/29.51 meet(join(sF4_fnc,sF1_fnc),join(sF4_fnc,sF3_fnc))=join(sF4_fnc,join(sF4_fnc,sF0_fnc))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f41639,f360])).
% 144.22/29.51 fof(f56526,plain,(
% 144.22/29.51 sF0_fnc=meet(sF1_fnc,join(sF4_fnc,sF0_fnc))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f2952,f56436])).
% 144.22/29.51 fof(f56543,plain,(
% 144.22/29.51 meet(join(sF4_fnc,sF1_fnc),sF3_fnc)=join(sF4_fnc,join(sF4_fnc,sF0_fnc))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f972,f56446])).
% 144.22/29.51 fof(f56544,plain,(
% 144.22/29.51 meet(join(sF4_fnc,sF1_fnc),sF3_fnc)=join(sF0_fnc,sF4_fnc)),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f5885,f56543])).
% 144.22/29.51 fof(f56730,plain,(
% 144.22/29.51 ![X0]: (meet(join(sF4_fnc,sF0_fnc),sF1_fnc)=meet(join(join(sF4_fnc,sF0_fnc),X0),sF0_fnc))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f56526,f13112])).
% 144.22/29.51 fof(f56816,plain,(
% 144.22/29.51 ![X0]: (meet(join(sF4_fnc,sF0_fnc),sF1_fnc)=meet(join(sF4_fnc,join(X0,sF0_fnc)),sF0_fnc))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f7001,f56730])).
% 144.22/29.51 fof(f56820,plain,(
% 144.22/29.51 meet(join(sF4_fnc,sF0_fnc),sF1_fnc)=sF0_fnc),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f4607,f56816])).
% 144.22/29.51 fof(f56898,plain,(
% 144.22/29.51 ifeq3(meet(r1,join(sF4_fnc,sF0_fnc)),r1,sF0_fnc,join(r1,meet(sF2_fnc,join(sF4_fnc,sF0_fnc))))=join(r1,meet(sF2_fnc,join(sF4_fnc,sF0_fnc)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f56820,f314])).
% 144.22/29.51 fof(f56986,plain,(
% 144.22/29.51 ifeq3(r1,r1,sF0_fnc,join(r1,meet(sF2_fnc,join(sF4_fnc,sF0_fnc))))=join(r1,meet(sF2_fnc,join(sF4_fnc,sF0_fnc)))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f2941,f56898])).
% 144.22/29.51 fof(f56987,plain,(
% 144.22/29.51 sF0_fnc=join(r1,meet(sF2_fnc,join(sF4_fnc,sF0_fnc)))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f23,f56986])).
% 144.22/29.51 fof(f57473,plain,(
% 144.22/29.51 meet(a,join(b,r1))=meet(a,b)),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f41842,f1103])).
% 144.22/29.51 fof(f59270,plain,(
% 144.22/29.51 ifeq3(meet(r1,join(sF4_fnc,sF1_fnc)),r1,join(sF0_fnc,sF4_fnc),join(r1,meet(sF4_fnc,join(sF4_fnc,sF1_fnc))))=join(r1,meet(sF4_fnc,join(sF4_fnc,sF1_fnc)))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f56544,f313])).
% 144.22/29.51 fof(f59274,plain,(
% 144.22/29.51 ![X0]: (meet(X0,meet(sF3_fnc,join(sF4_fnc,sF1_fnc)))=meet(join(sF0_fnc,sF4_fnc),X0))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f56544,f13278])).
% 144.22/29.51 fof(f59366,plain,(
% 144.22/29.51 ifeq3(r1,r1,join(sF0_fnc,sF4_fnc),join(r1,meet(sF4_fnc,join(sF4_fnc,sF1_fnc))))=join(r1,meet(sF4_fnc,join(sF4_fnc,sF1_fnc)))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f2928,f59270])).
% 144.22/29.51 fof(f59367,plain,(
% 144.22/29.51 join(sF0_fnc,sF4_fnc)=join(r1,meet(sF4_fnc,join(sF4_fnc,sF1_fnc)))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f23,f59366])).
% 144.22/29.51 fof(f59368,plain,(
% 144.22/29.51 join(sF0_fnc,sF4_fnc)=join(r1,sF4_fnc)),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f28,f59367])).
% 144.22/29.51 fof(f59431,plain,(
% 144.22/29.51 join(sF0_fnc,sF4_fnc)=sF3_fnc),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f48,f59368])).
% 144.22/29.51 fof(f59441,plain,(
% 144.22/29.51 ![X0]: (meet(X0,join(sF4_fnc,sF0_fnc))=meet(join(sF0_fnc,sF4_fnc),X0))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f41639,f59274])).
% 144.22/29.51 fof(f59447,plain,(
% 144.22/29.51 sF0_fnc=join(r1,meet(sF3_fnc,sF2_fnc))),
% 144.22/29.51 inference(backward_demodulation,[status(thm)],[f59473,f56987])).
% 144.22/29.51 fof(f59473,plain,(
% 144.22/29.51 ![X0]: (meet(X0,join(sF4_fnc,sF0_fnc))=meet(sF3_fnc,X0))),
% 144.22/29.51 inference(forward_demodulation,[status(thm)],[f59431,f59441])).
% 144.22/29.51 fof(f65027,plain,(
% 144.22/29.51 ![X0]: (join(meet(sF3_fnc,sF2_fnc),r1)=join(meet(X0,r1),sF0_fnc))),
% 144.22/29.51 inference(paramodulation,[status(thm)],[f59447,f6613])).
% 144.22/29.51 fof(f65042,plain,(
% 144.22/29.51 ![X0]: (meet(sF0_fnc,meet(meet(sF3_fnc,sF2_fnc),X0))=meet(X0,meet(sF3_fnc,sF2_fnc)))),
% 85.15/29.75 inference(paramodulation,[status(thm)],[f59447,f4936])).
% 85.15/29.75 fof(f65067,plain,(
% 85.15/29.75 ![X0]: (meet(sF3_fnc,sF2_fnc)=meet(join(X0,sF0_fnc),meet(sF3_fnc,sF2_fnc)))),
% 85.15/29.75 inference(paramodulation,[status(thm)],[f59447,f4607])).
% 85.15/29.75 fof(f65127,plain,(
% 85.15/29.75 join(meet(sF3_fnc,sF2_fnc),r1)=sF0_fnc),
% 85.15/29.75 inference(forward_demodulation,[status(thm)],[f11213,f65027])).
% 85.15/29.75 fof(f65142,plain,(
% 85.15/29.75 ![X0]: (meet(sF0_fnc,meet(sF3_fnc,meet(X0,sF2_fnc)))=meet(X0,meet(sF3_fnc,sF2_fnc)))),
% 85.15/29.75 inference(forward_demodulation,[status(thm)],[f7380,f65042])).
% 85.15/29.75 fof(f65143,plain,(
% 85.15/29.75 ![X0]: (meet(meet(X0,sF2_fnc),sF0_fnc)=meet(X0,meet(sF3_fnc,sF2_fnc)))),
% 85.15/29.75 inference(forward_demodulation,[status(thm)],[f3446,f65142])).
% 85.15/29.75 fof(f65147,plain,(
% 85.15/29.75 ![X0]: (meet(X0,meet(sF0_fnc,sF2_fnc))=meet(X0,meet(sF3_fnc,sF2_fnc)))),
% 85.15/29.75 inference(forward_demodulation,[status(thm)],[f7380,f65143])).
% 85.15/29.75 fof(f65194,plain,(
% 85.15/29.75 ![X0]: (meet(sF3_fnc,sF2_fnc)=meet(join(X0,sF0_fnc),meet(sF0_fnc,sF2_fnc)))),
% 85.15/29.75 inference(forward_demodulation,[status(thm)],[f65147,f65067])).
% 85.15/29.75 fof(f65203,plain,(
% 85.15/29.75 join(meet(sF2_fnc,sF0_fnc),r1)=sF0_fnc),
% 85.15/29.75 inference(backward_demodulation,[status(thm)],[f65208,f65127])).
% 85.15/29.75 fof(f65208,plain,(
% 85.15/29.75 meet(sF3_fnc,sF2_fnc)=meet(sF2_fnc,sF0_fnc)),
% 85.15/29.75 inference(forward_demodulation,[status(thm)],[f4936,f65194])).
% 85.15/29.75 fof(f72344,plain,(
% 85.15/29.75 meet(sF4_fnc,join(b,r1))=meet(r2,meet(a,b))),
% 85.15/29.75 inference(paramodulation,[status(thm)],[f57473,f71])).
% 85.15/29.75 fof(f72438,plain,(
% 85.15/29.75 meet(sF4_fnc,join(b,r1))=meet(sF4_fnc,b)),
% 85.15/29.75 inference(forward_demodulation,[status(thm)],[f71,f72344])).
% 85.15/29.75 fof(f72439,plain,(
% 85.15/29.75 meet(sF4_fnc,join(b,r1))=n0),
% 85.15/29.75 inference(forward_demodulation,[status(thm)],[f863,f72438])).
% 85.15/29.75 fof(f73200,plain,(
% 85.15/29.75 meet(sF4_fnc,join(r1,b))=n0),
% 85.15/29.75 inference(paramodulation,[status(thm)],[f36542,f72439])).
% 85.15/29.75 fof(f74041,plain,(
% 85.15/29.75 meet(join(r1,b),join(r1,sF4_fnc))=join(r1,n0)),
% 85.15/29.75 inference(paramodulation,[status(thm)],[f73200,f360])).
% 85.15/29.75 fof(f74160,plain,(
% 85.15/29.75 meet(join(r1,b),sF3_fnc)=join(r1,n0)),
% 85.15/29.75 inference(forward_demodulation,[status(thm)],[f48,f74041])).
% 85.15/29.75 fof(f74163,plain,(
% 85.15/29.75 meet(join(r1,b),sF3_fnc)=r1),
% 85.15/29.75 inference(forward_demodulation,[status(thm)],[f35,f74160])).
% 85.15/29.75 fof(f74328,plain,(
% 85.15/29.75 meet(b,r1)=meet(sF3_fnc,b)),
% 85.15/29.75 inference(paramodulation,[status(thm)],[f74163,f3479])).
% 85.15/29.75 fof(f74431,plain,(
% 85.15/29.75 n0=meet(sF3_fnc,b)),
% 85.15/29.75 inference(forward_demodulation,[status(thm)],[f13583,f74328])).
% 85.15/29.75 fof(f74595,plain,(
% 85.15/29.75 meet(sF0_fnc,b)=meet(sF1_fnc,n0)),
% 85.15/29.75 inference(paramodulation,[status(thm)],[f74431,f70])).
% 85.15/29.75 fof(f74686,plain,(
% 85.15/29.75 meet(sF0_fnc,b)=n0),
% 85.15/29.75 inference(forward_demodulation,[status(thm)],[f34,f74595])).
% 85.15/29.75 fof(f74822,plain,(
% 85.15/29.75 meet(b,sF0_fnc)=n0),
% 85.15/29.75 inference(paramodulation,[status(thm)],[f30,f74686])).
% 85.15/29.75 fof(f75040,plain,(
% 85.15/29.75 meet(sF2_fnc,sF0_fnc)=meet(r2,n0)),
% 85.15/29.75 inference(paramodulation,[status(thm)],[f74822,f72])).
% 85.15/29.75 fof(f75124,plain,(
% 85.15/29.75 join(n0,r1)=sF0_fnc),
% 85.15/29.75 inference(backward_demodulation,[status(thm)],[f75189,f65203])).
% 85.15/29.75 fof(f75189,plain,(
% 85.15/29.75 meet(sF2_fnc,sF0_fnc)=n0),
% 85.15/29.75 inference(forward_demodulation,[status(thm)],[f34,f75040])).
% 85.15/29.75 fof(f75309,plain,(
% 85.15/29.75 r1=sF0_fnc),
% 85.15/29.75 inference(forward_demodulation,[status(thm)],[f150,f75124])).
% 85.15/29.75 fof(f75310,plain,(
% 85.15/29.75 $false),
% 85.15/29.75 inference(forward_subsumption_resolution,[status(thm)],[f75309,f50])).
% 85.15/29.75 % SZS output end CNFRefutation for theBenchmark.p
% 143.08/29.80 % Elapsed time: 18.574851 seconds
% 143.08/29.80 % CPU time: 146.967251 seconds
% 143.08/29.80 % Total memory used: 1.004 GB
% 143.08/29.80 % Net memory used: 988.635 MB
%------------------------------------------------------------------------------