%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT156-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:18 PM UTC 2026
% Result : Unsatisfiable 82.67s 11.03s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT156-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n020.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Sun Sep 20 23:17:17 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.44 % Drodi V4.1.1
% 82.67/11.03 % Refutation found
% 82.67/11.03 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 82.67/11.03 % SZS output start CNFRefutation for theBenchmark
% 82.67/11.03 fof(f1,axiom,(
% 82.67/11.03 (![X]: (meet(X,X) = X ))),
% 82.67/11.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.67/11.03 fof(f2,axiom,(
% 82.67/11.03 (![X]: (join(X,X) = X ))),
% 82.67/11.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.67/11.03 fof(f3,axiom,(
% 82.67/11.03 (![X,Y]: (meet(X,join(X,Y)) = X ))),
% 82.67/11.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.67/11.03 fof(f4,axiom,(
% 82.67/11.03 (![X,Y]: (join(X,meet(X,Y)) = X ))),
% 82.67/11.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.67/11.03 fof(f5,axiom,(
% 82.67/11.03 (![X,Y]: (meet(X,Y) = meet(Y,X) ))),
% 82.67/11.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.67/11.03 fof(f6,axiom,(
% 82.67/11.03 (![X,Y]: (join(X,Y) = join(Y,X) ))),
% 82.67/11.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.67/11.03 fof(f7,axiom,(
% 82.67/11.03 (![X,Y,Z]: (meet(meet(X,Y),Z) = meet(X,meet(Y,Z)) ))),
% 82.67/11.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.67/11.03 fof(f8,axiom,(
% 82.67/11.03 (![X,Y,Z]: (join(join(X,Y),Z) = join(X,join(Y,Z)) ))),
% 82.67/11.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.67/11.04 fof(f9,axiom,(
% 82.67/11.04 (![X,Y,Z,U]: (meet(X,join(Y,meet(Z,join(X,U)))) = meet(X,join(Y,join(meet(X,Z),meet(Z,join(Y,U))))) ))),
% 82.67/11.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.67/11.04 fof(f10,negated_conjecture,(
% 82.67/11.04 meet(a,join(b,meet(a,c))) != meet(a,join(meet(a,join(b,meet(a,c))),meet(c,join(a,b)))) ),
% 82.67/11.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.67/11.04 fof(f11,plain,(
% 82.67/11.04 ![X0]: (meet(X0,X0)=X0)),
% 82.67/11.04 inference(cnf_transformation,[status(thm)],[f1])).
% 82.67/11.04 fof(f12,plain,(
% 82.67/11.04 ![X0]: (join(X0,X0)=X0)),
% 82.67/11.04 inference(cnf_transformation,[status(thm)],[f2])).
% 82.67/11.04 fof(f13,plain,(
% 82.67/11.04 ![X0,X1]: (meet(X0,join(X0,X1))=X0)),
% 82.67/11.04 inference(cnf_transformation,[status(thm)],[f3])).
% 82.67/11.04 fof(f14,plain,(
% 82.67/11.04 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 82.67/11.04 inference(cnf_transformation,[status(thm)],[f4])).
% 82.67/11.04 fof(f15,plain,(
% 82.67/11.04 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 82.67/11.04 inference(cnf_transformation,[status(thm)],[f5])).
% 82.67/11.04 fof(f16,plain,(
% 82.67/11.04 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 82.67/11.04 inference(cnf_transformation,[status(thm)],[f6])).
% 82.67/11.04 fof(f17,plain,(
% 82.67/11.04 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X0,meet(X1,X2)))),
% 82.67/11.04 inference(cnf_transformation,[status(thm)],[f7])).
% 82.67/11.04 fof(f18,plain,(
% 82.67/11.04 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X0,join(X1,X2)))),
% 82.67/11.04 inference(cnf_transformation,[status(thm)],[f8])).
% 82.67/11.04 fof(f19,plain,(
% 82.67/11.04 ![X0,X1,X2,X3]: (meet(X0,join(X1,meet(X2,join(X0,X3))))=meet(X0,join(X1,join(meet(X0,X2),meet(X2,join(X1,X3))))))),
% 82.67/11.04 inference(cnf_transformation,[status(thm)],[f9])).
% 82.67/11.04 fof(f20,plain,(
% 82.67/11.04 ~meet(a,join(b,meet(a,c)))=meet(a,join(meet(a,join(b,meet(a,c))),meet(c,join(a,b))))),
% 82.67/11.04 inference(cnf_transformation,[status(thm)],[f10])).
% 82.67/11.04 fof(f21,definition,(
% 82.67/11.04 sF2_fnc=meet(a,c)),
% 82.67/11.04 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 82.67/11.04 fof(f22,definition,(
% 82.67/11.04 sF1_fnc=join(b,sF2_fnc)),
% 82.67/11.04 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 82.67/11.04 fof(f23,definition,(
% 82.67/11.04 sF0_fnc=meet(a,sF1_fnc)),
% 82.67/11.04 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 82.67/11.04 fof(f24,definition,(
% 82.67/11.04 sF6_fnc=join(b,sF2_fnc)),
% 82.67/11.04 introduced(definition,[new_symbols(definition,[sF6_fnc])],[function_definition])).
% 82.67/11.04 fof(f25,definition,(
% 82.67/11.04 sF5_fnc=meet(a,sF6_fnc)),
% 82.67/11.04 introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition])).
% 82.67/11.04 fof(f26,definition,(
% 82.67/11.04 sF8_fnc=join(a,b)),
% 82.67/11.04 introduced(definition,[new_symbols(definition,[sF8_fnc])],[function_definition])).
% 82.67/11.04 fof(f27,definition,(
% 82.67/11.04 sF7_fnc=meet(c,sF8_fnc)),
% 82.67/11.04 introduced(definition,[new_symbols(definition,[sF7_fnc])],[function_definition])).
% 82.67/11.04 fof(f28,definition,(
% 82.67/11.04 sF4_fnc=join(sF5_fnc,sF7_fnc)),
% 82.67/11.04 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 82.67/11.04 fof(f29,definition,(
% 82.67/11.04 sF3_fnc=meet(a,sF4_fnc)),
% 82.67/11.04 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 82.67/11.04 fof(f30,plain,(
% 82.67/11.04 ~sF0_fnc=sF3_fnc),
% 82.67/11.04 inference(definition_folding,[],[f20,f29,f28,f27,f26,f25,f24,f23,f22,f21])).
% 82.67/11.04 fof(f31,plain,(
% 82.67/11.04 sF6_fnc=sF1_fnc),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f22,f24])).
% 82.67/11.04 fof(f32,plain,(
% 82.67/11.04 sF5_fnc=meet(a,sF1_fnc)),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f31,f25])).
% 82.67/11.04 fof(f33,plain,(
% 82.67/11.04 sF5_fnc=sF0_fnc),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f23,f32])).
% 82.67/11.04 fof(f34,plain,(
% 82.67/11.04 sF4_fnc=join(sF0_fnc,sF7_fnc)),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f33,f28])).
% 82.67/11.04 fof(f35,plain,(
% 82.67/11.04 meet(sF0_fnc,sF4_fnc)=sF0_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f34,f13])).
% 82.67/11.04 fof(f36,plain,(
% 82.67/11.04 meet(a,sF8_fnc)=a),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f26,f13])).
% 82.67/11.04 fof(f37,plain,(
% 82.67/11.04 meet(b,sF1_fnc)=b),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f22,f13])).
% 82.67/11.04 fof(f43,plain,(
% 82.67/11.04 join(a,sF3_fnc)=a),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f29,f14])).
% 82.67/11.04 fof(f45,plain,(
% 82.67/11.04 join(a,sF2_fnc)=a),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f21,f14])).
% 82.67/11.04 fof(f55,plain,(
% 82.67/11.04 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f15,f14])).
% 82.67/11.04 fof(f61,plain,(
% 82.67/11.04 ![X0,X1]: (meet(X0,join(X1,X0))=X0)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f16,f13])).
% 82.67/11.04 fof(f66,plain,(
% 82.67/11.04 join(sF1_fnc,b)=sF1_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f37,f55])).
% 82.67/11.04 fof(f67,plain,(
% 82.67/11.04 join(sF4_fnc,sF0_fnc)=sF4_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f35,f55])).
% 82.67/11.04 fof(f68,plain,(
% 82.67/11.04 join(sF8_fnc,sF7_fnc)=sF8_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f27,f55])).
% 82.67/11.04 fof(f69,plain,(
% 82.67/11.04 join(sF8_fnc,a)=sF8_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f36,f55])).
% 82.67/11.04 fof(f70,plain,(
% 82.67/11.04 join(sF4_fnc,sF3_fnc)=sF4_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f29,f55])).
% 82.67/11.04 fof(f71,plain,(
% 82.67/11.04 join(sF1_fnc,sF0_fnc)=sF1_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f23,f55])).
% 82.67/11.04 fof(f73,plain,(
% 82.67/11.04 ![X0,X1]: (join(join(X0,X1),X0)=join(X0,X1))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f13,f55])).
% 82.67/11.04 fof(f79,plain,(
% 82.67/11.04 ![X0,X1]: (join(X0,join(X1,X0))=join(X0,X1))),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f18,f73])).
% 82.67/11.04 fof(f80,plain,(
% 82.67/11.04 join(b,sF1_fnc)=sF1_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f16,f66])).
% 82.67/11.04 fof(f85,plain,(
% 82.67/11.04 join(sF0_fnc,sF4_fnc)=sF4_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f16,f67])).
% 82.67/11.04 fof(f90,plain,(
% 82.67/11.04 join(sF7_fnc,sF8_fnc)=sF8_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f16,f68])).
% 82.67/11.04 fof(f95,plain,(
% 82.67/11.04 join(a,sF8_fnc)=sF8_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f16,f69])).
% 82.67/11.04 fof(f100,plain,(
% 82.67/11.04 join(sF3_fnc,sF4_fnc)=sF4_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f16,f70])).
% 82.67/11.04 fof(f121,plain,(
% 82.67/11.04 ![X0,X1,X2]: (meet(X0,X1)=meet(X0,meet(X1,join(meet(X0,X1),X2))))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f13,f17])).
% 82.67/11.04 fof(f122,plain,(
% 82.67/11.04 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X1,meet(X2,X0)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f15,f17])).
% 82.67/11.04 fof(f130,plain,(
% 82.67/11.04 ![X0]: (meet(sF7_fnc,X0)=meet(c,meet(sF8_fnc,X0)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f27,f17])).
% 82.67/11.04 fof(f133,plain,(
% 82.67/11.04 ![X0]: (meet(sF0_fnc,X0)=meet(a,meet(sF1_fnc,X0)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f23,f17])).
% 82.67/11.04 fof(f134,plain,(
% 82.67/11.04 ![X0]: (meet(sF2_fnc,X0)=meet(a,meet(c,X0)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f21,f17])).
% 82.67/11.04 fof(f138,plain,(
% 82.67/11.04 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X0,X1)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f11,f17])).
% 82.67/11.04 fof(f149,plain,(
% 82.67/11.04 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X1,join(X2,X0)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f16,f18])).
% 82.67/11.04 fof(f165,plain,(
% 82.67/11.04 ![X0]: (join(sF4_fnc,X0)=join(sF0_fnc,join(sF7_fnc,X0)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f34,f18])).
% 82.67/11.04 fof(f170,plain,(
% 82.67/11.04 ![X0]: (join(sF8_fnc,X0)=join(a,join(b,X0)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f26,f18])).
% 82.67/11.04 fof(f172,plain,(
% 82.67/11.04 ![X0]: (join(sF1_fnc,X0)=join(b,join(sF2_fnc,X0)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f22,f18])).
% 82.67/11.04 fof(f177,plain,(
% 82.67/11.04 ![X0,X1]: (join(X0,X1)=join(X0,join(X0,X1)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f12,f18])).
% 82.67/11.04 fof(f201,plain,(
% 82.67/11.04 ![X0,X1]: (meet(a,join(X0,meet(sF4_fnc,join(a,X1))))=meet(a,join(X0,join(sF3_fnc,meet(sF4_fnc,join(X0,X1))))))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f29,f19])).
% 82.67/11.04 fof(f203,plain,(
% 82.67/11.04 ![X0,X1]: (meet(a,join(X0,meet(c,join(a,X1))))=meet(a,join(X0,join(sF2_fnc,meet(c,join(X0,X1))))))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f21,f19])).
% 82.67/11.04 fof(f216,plain,(
% 82.67/11.04 ![X0,X1]: (meet(X0,join(sF3_fnc,meet(X1,join(X0,sF4_fnc))))=meet(X0,join(sF3_fnc,join(meet(X0,X1),meet(X1,sF4_fnc)))))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f100,f19])).
% 82.67/11.04 fof(f316,plain,(
% 82.67/11.04 ![X0]: (meet(X0,join(sF3_fnc,meet(sF0_fnc,join(X0,sF4_fnc))))=meet(X0,join(sF3_fnc,join(meet(X0,sF0_fnc),sF0_fnc))))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f35,f216])).
% 82.67/11.04 fof(f317,plain,(
% 82.67/11.04 ![X0]: (meet(X0,join(sF3_fnc,meet(a,join(X0,sF4_fnc))))=meet(X0,join(sF3_fnc,join(meet(X0,a),sF3_fnc))))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f29,f216])).
% 82.67/11.04 fof(f355,plain,(
% 82.67/11.04 ![X0]: (meet(X0,join(sF3_fnc,meet(a,join(X0,sF4_fnc))))=meet(X0,join(sF3_fnc,meet(X0,a))))),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f79,f317])).
% 82.67/11.04 fof(f380,plain,(
% 82.67/11.04 meet(sF0_fnc,join(sF3_fnc,meet(a,sF4_fnc)))=meet(sF0_fnc,join(sF3_fnc,meet(sF0_fnc,a)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f85,f355])).
% 82.67/11.04 fof(f397,plain,(
% 82.67/11.04 meet(sF0_fnc,join(sF3_fnc,sF3_fnc))=meet(sF0_fnc,join(sF3_fnc,meet(sF0_fnc,a)))),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f29,f380])).
% 82.67/11.04 fof(f398,plain,(
% 82.67/11.04 meet(sF0_fnc,sF3_fnc)=meet(sF0_fnc,join(sF3_fnc,meet(sF0_fnc,a)))),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f12,f397])).
% 82.67/11.04 fof(f406,plain,(
% 82.67/11.04 meet(sF0_fnc,sF3_fnc)=meet(sF0_fnc,join(sF3_fnc,meet(a,sF0_fnc)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f15,f398])).
% 82.67/11.04 fof(f468,plain,(
% 82.67/11.04 meet(a,sF4_fnc)=meet(a,sF3_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f29,f138])).
% 82.67/11.04 fof(f469,plain,(
% 82.67/11.04 meet(a,sF1_fnc)=meet(a,sF0_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f23,f138])).
% 82.67/11.04 fof(f470,plain,(
% 82.67/11.04 meet(a,c)=meet(a,sF2_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f21,f138])).
% 82.67/11.04 fof(f476,plain,(
% 82.67/11.04 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X1,X0)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f15,f138])).
% 82.67/11.04 fof(f501,plain,(
% 82.67/11.04 sF3_fnc=meet(a,sF3_fnc)),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f29,f468])).
% 82.67/11.04 fof(f502,plain,(
% 82.67/11.04 meet(sF0_fnc,sF3_fnc)=meet(sF0_fnc,join(sF3_fnc,sF0_fnc))),
% 82.67/11.04 inference(backward_demodulation,[status(thm)],[f503,f406])).
% 82.67/11.04 fof(f503,plain,(
% 82.67/11.04 sF0_fnc=meet(a,sF0_fnc)),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f23,f469])).
% 82.67/11.04 fof(f504,plain,(
% 82.67/11.04 sF2_fnc=meet(a,sF2_fnc)),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f21,f470])).
% 82.67/11.04 fof(f523,plain,(
% 82.67/11.04 meet(sF0_fnc,sF3_fnc)=sF0_fnc),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f61,f502])).
% 82.67/11.04 fof(f566,plain,(
% 82.67/11.04 join(sF3_fnc,sF0_fnc)=sF3_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f523,f55])).
% 82.67/11.04 fof(f574,plain,(
% 82.67/11.04 join(sF0_fnc,sF3_fnc)=sF3_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f16,f566])).
% 82.67/11.04 fof(f620,plain,(
% 82.67/11.04 join(b,sF8_fnc)=join(b,a)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f26,f79])).
% 82.67/11.04 fof(f688,plain,(
% 82.67/11.04 ![X0,X1,X2]: (meet(X0,join(X1,join(X2,X0)))=X0)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f18,f61])).
% 82.67/11.04 fof(f707,plain,(
% 82.67/11.04 meet(sF3_fnc,a)=sF3_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f43,f61])).
% 82.67/11.04 fof(f708,plain,(
% 82.67/11.04 meet(b,sF8_fnc)=b),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f26,f61])).
% 82.67/11.04 fof(f711,plain,(
% 82.67/11.04 meet(sF2_fnc,sF1_fnc)=sF2_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f22,f61])).
% 82.67/11.04 fof(f720,plain,(
% 82.67/11.04 ![X0,X1,X2]: (meet(X0,join(X1,meet(X2,join(X0,X2))))=meet(X0,join(X1,join(meet(X0,X2),X2))))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f61,f19])).
% 82.67/11.04 fof(f725,plain,(
% 82.67/11.04 ![X0,X1,X2]: (meet(X0,X1)=meet(X0,meet(join(X2,X0),X1)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f61,f17])).
% 82.67/11.04 fof(f736,plain,(
% 82.67/11.04 ![X0]: (meet(X0,join(sF3_fnc,meet(sF0_fnc,join(X0,sF4_fnc))))=meet(X0,join(sF3_fnc,sF0_fnc)))),
% 82.67/11.04 inference(backward_demodulation,[status(thm)],[f738,f316])).
% 82.67/11.04 fof(f738,plain,(
% 82.67/11.04 ![X0,X1,X2]: (meet(X0,join(X1,X2))=meet(X0,join(X1,join(meet(X0,X2),X2))))),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f61,f720])).
% 82.67/11.04 fof(f746,plain,(
% 82.67/11.04 ![X0]: (meet(X0,join(sF3_fnc,meet(sF0_fnc,join(X0,sF4_fnc))))=meet(X0,sF3_fnc))),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f566,f736])).
% 82.67/11.04 fof(f963,plain,(
% 82.67/11.04 join(sF8_fnc,b)=sF8_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f708,f55])).
% 82.67/11.04 fof(f969,plain,(
% 82.67/11.04 join(b,sF8_fnc)=sF8_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f16,f963])).
% 82.67/11.04 fof(f978,plain,(
% 82.67/11.04 sF8_fnc=join(b,a)),
% 82.67/11.04 inference(backward_demodulation,[status(thm)],[f969,f620])).
% 82.67/11.04 fof(f1001,plain,(
% 82.67/11.04 meet(sF1_fnc,sF2_fnc)=sF2_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f15,f711])).
% 82.67/11.04 fof(f1008,plain,(
% 82.67/11.04 join(sF1_fnc,sF2_fnc)=sF1_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f711,f55])).
% 82.67/11.04 fof(f1157,plain,(
% 82.67/11.04 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X1,X0)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f11,f122])).
% 82.67/11.04 fof(f1342,plain,(
% 82.67/11.04 meet(sF0_fnc,sF2_fnc)=meet(a,sF2_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f1001,f133])).
% 82.67/11.04 fof(f1369,plain,(
% 82.67/11.04 meet(sF0_fnc,sF2_fnc)=sF2_fnc),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f504,f1342])).
% 82.67/11.04 fof(f1402,plain,(
% 82.67/11.04 join(sF0_fnc,sF2_fnc)=sF0_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f1369,f14])).
% 82.67/11.04 fof(f1408,plain,(
% 82.67/11.04 meet(sF2_fnc,sF0_fnc)=sF2_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f1402,f61])).
% 82.67/11.04 fof(f1420,plain,(
% 82.67/11.04 meet(sF2_fnc,join(sF3_fnc,meet(sF0_fnc,join(sF2_fnc,sF4_fnc))))=meet(sF2_fnc,join(sF3_fnc,join(sF2_fnc,meet(sF0_fnc,sF4_fnc))))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f1408,f216])).
% 82.67/11.04 fof(f1430,plain,(
% 82.67/11.04 meet(sF2_fnc,sF3_fnc)=meet(sF2_fnc,join(sF3_fnc,join(sF2_fnc,meet(sF0_fnc,sF4_fnc))))),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f746,f1420])).
% 82.67/11.04 fof(f1431,plain,(
% 82.67/11.04 meet(sF2_fnc,sF3_fnc)=meet(sF2_fnc,join(sF3_fnc,join(sF2_fnc,sF0_fnc)))),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f35,f1430])).
% 82.67/11.04 fof(f1482,plain,(
% 82.67/11.04 meet(sF2_fnc,sF8_fnc)=meet(a,sF7_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f27,f134])).
% 82.67/11.04 fof(f1665,plain,(
% 82.67/11.04 ![X0,X1,X2]: (meet(X0,join(join(X1,X0),X2))=X0)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f16,f688])).
% 82.67/11.04 fof(f1720,plain,(
% 82.67/11.04 ![X0,X1,X2,X3]: (meet(X0,X1)=meet(X1,meet(join(X2,join(X3,X1)),X0)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f688,f122])).
% 82.67/11.04 fof(f1721,plain,(
% 82.67/11.04 ![X0,X1,X2,X3]: (meet(X0,join(X1,join(X2,X0)))=meet(X0,meet(join(X1,join(X2,X0)),join(X0,X3))))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f688,f121])).
% 82.67/11.04 fof(f1730,plain,(
% 82.67/11.04 meet(sF2_fnc,sF3_fnc)=sF2_fnc),
% 82.67/11.04 inference(backward_demodulation,[status(thm)],[f1759,f1431])).
% 82.67/11.04 fof(f1759,plain,(
% 82.67/11.04 ![X0,X1,X2]: (meet(X0,join(X1,join(X0,X2)))=X0)),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f18,f1665])).
% 82.67/11.04 fof(f1774,plain,(
% 82.67/11.04 ![X0,X1,X2,X3]: (X0=meet(X0,meet(join(X1,join(X2,X0)),join(X0,X3))))),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f688,f1721])).
% 82.67/11.04 fof(f1776,plain,(
% 82.67/11.04 ![X0,X1]: (X0=meet(join(X0,X1),X0))),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f1720,f1774])).
% 82.67/11.04 fof(f1798,plain,(
% 82.67/11.04 join(sF3_fnc,sF2_fnc)=sF3_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f1730,f55])).
% 82.67/11.04 fof(f1808,plain,(
% 82.67/11.04 join(sF2_fnc,sF3_fnc)=sF3_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f16,f1798])).
% 82.67/11.04 fof(f1858,plain,(
% 82.67/11.04 sF0_fnc=meet(sF3_fnc,sF0_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f574,f1776])).
% 82.67/11.04 fof(f1862,plain,(
% 82.67/11.04 a=meet(sF8_fnc,a)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f95,f1776])).
% 82.67/11.04 fof(f1875,plain,(
% 82.67/11.04 ![X0,X1]: (X0=meet(join(X1,X0),X0))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f16,f1776])).
% 82.67/11.04 fof(f2336,plain,(
% 82.67/11.04 meet(sF7_fnc,a)=meet(c,a)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f1862,f130])).
% 82.67/11.04 fof(f2403,plain,(
% 82.67/11.04 ![X0,X1,X2]: (X0=meet(join(X1,join(X2,X0)),X0))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f18,f1875])).
% 82.67/11.04 fof(f2521,plain,(
% 82.67/11.04 meet(sF4_fnc,a)=meet(a,sF3_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f29,f1157])).
% 82.67/11.04 fof(f2523,plain,(
% 82.67/11.04 meet(c,a)=meet(a,sF2_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f21,f1157])).
% 82.67/11.04 fof(f2629,plain,(
% 82.67/11.04 meet(sF4_fnc,a)=sF3_fnc),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f501,f2521])).
% 82.67/11.04 fof(f2635,plain,(
% 82.67/11.04 meet(sF7_fnc,a)=sF2_fnc),
% 82.67/11.04 inference(backward_demodulation,[status(thm)],[f2637,f2336])).
% 82.67/11.04 fof(f2637,plain,(
% 82.67/11.04 meet(c,a)=sF2_fnc),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f504,f2523])).
% 82.67/11.04 fof(f2695,plain,(
% 82.67/11.04 meet(a,sF7_fnc)=sF2_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f15,f2635])).
% 82.67/11.04 fof(f2709,plain,(
% 82.67/11.04 join(sF7_fnc,sF2_fnc)=sF7_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f2635,f14])).
% 82.67/11.04 fof(f2714,plain,(
% 82.67/11.04 meet(sF2_fnc,sF8_fnc)=sF2_fnc),
% 82.67/11.04 inference(backward_demodulation,[status(thm)],[f2695,f1482])).
% 82.67/11.04 fof(f2800,plain,(
% 82.67/11.04 join(sF2_fnc,sF7_fnc)=sF7_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f16,f2709])).
% 82.67/11.04 fof(f2842,plain,(
% 82.67/11.04 join(sF8_fnc,sF2_fnc)=sF8_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f2714,f55])).
% 82.67/11.04 fof(f2901,plain,(
% 82.67/11.04 join(sF2_fnc,sF8_fnc)=sF8_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f16,f2842])).
% 82.67/11.04 fof(f3454,plain,(
% 82.67/11.04 ![X0]: (join(X0,sF1_fnc)=join(sF1_fnc,join(sF2_fnc,X0)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f1008,f149])).
% 82.67/11.04 fof(f3456,plain,(
% 82.67/11.04 ![X0]: (join(X0,sF1_fnc)=join(sF1_fnc,join(b,X0)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f66,f149])).
% 82.67/11.04 fof(f3482,plain,(
% 82.67/11.04 ![X0,X1]: (join(X0,X1)=join(X1,join(X1,X0)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f12,f149])).
% 82.67/11.04 fof(f3795,plain,(
% 82.67/11.04 join(sF4_fnc,sF2_fnc)=join(sF0_fnc,sF7_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f2709,f165])).
% 82.67/11.04 fof(f3798,plain,(
% 82.67/11.04 join(sF4_fnc,sF8_fnc)=join(sF0_fnc,sF8_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f90,f165])).
% 82.67/11.04 fof(f3830,plain,(
% 82.67/11.04 join(sF4_fnc,sF2_fnc)=sF4_fnc),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f34,f3795])).
% 82.67/11.04 fof(f3857,plain,(
% 82.67/11.04 join(sF2_fnc,sF4_fnc)=sF4_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f16,f3830])).
% 82.67/11.04 fof(f4096,plain,(
% 82.67/11.04 ![X0]: (sF0_fnc=meet(join(X0,sF3_fnc),sF0_fnc))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f566,f2403])).
% 82.67/11.04 fof(f4216,plain,(
% 82.67/11.04 join(sF2_fnc,sF0_fnc)=join(sF0_fnc,sF0_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f1402,f3482])).
% 82.67/11.04 fof(f4222,plain,(
% 82.67/11.04 join(sF2_fnc,a)=join(a,a)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f45,f3482])).
% 82.67/11.04 fof(f4309,plain,(
% 82.67/11.04 join(sF2_fnc,sF0_fnc)=sF0_fnc),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f12,f4216])).
% 82.67/11.04 fof(f4315,plain,(
% 82.67/11.04 join(sF2_fnc,a)=a),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f12,f4222])).
% 82.67/11.04 fof(f4488,plain,(
% 82.67/11.04 join(sF8_fnc,sF2_fnc)=join(a,sF1_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f22,f170])).
% 82.67/11.04 fof(f4529,plain,(
% 82.67/11.04 sF8_fnc=join(a,sF1_fnc)),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f2842,f4488])).
% 82.67/11.04 fof(f4563,plain,(
% 82.67/11.04 join(sF1_fnc,a)=join(b,a)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f4315,f172])).
% 82.67/11.04 fof(f4564,plain,(
% 82.67/11.04 join(sF1_fnc,sF0_fnc)=join(b,sF0_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f4309,f172])).
% 82.67/11.04 fof(f4566,plain,(
% 82.67/11.04 join(sF1_fnc,sF4_fnc)=join(b,sF4_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f3857,f172])).
% 82.67/11.04 fof(f4567,plain,(
% 82.67/11.04 join(sF1_fnc,sF8_fnc)=join(b,sF8_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f2901,f172])).
% 82.67/11.04 fof(f4568,plain,(
% 82.67/11.04 join(sF1_fnc,sF7_fnc)=join(b,sF7_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f2800,f172])).
% 82.67/11.04 fof(f4569,plain,(
% 82.67/11.04 join(sF1_fnc,sF3_fnc)=join(b,sF3_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f1808,f172])).
% 82.67/11.04 fof(f4610,plain,(
% 82.67/11.04 join(sF1_fnc,a)=sF8_fnc),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f978,f4563])).
% 82.67/11.04 fof(f4611,plain,(
% 82.67/11.04 sF1_fnc=join(b,sF0_fnc)),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f71,f4564])).
% 82.67/11.04 fof(f4614,plain,(
% 82.67/11.04 join(sF1_fnc,sF8_fnc)=sF8_fnc),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f969,f4567])).
% 82.67/11.04 fof(f4657,plain,(
% 82.67/11.04 meet(sF1_fnc,sF8_fnc)=sF1_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f4529,f61])).
% 82.67/11.04 fof(f4710,plain,(
% 82.67/11.04 ![X0,X1]: (meet(X0,join(sF1_fnc,meet(X1,join(X0,a))))=meet(X0,join(sF1_fnc,join(meet(X0,X1),meet(X1,sF8_fnc)))))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f4610,f19])).
% 82.67/11.04 fof(f4733,plain,(
% 82.67/11.04 ![X0,X1]: (meet(X0,join(sF1_fnc,meet(X1,join(X0,sF8_fnc))))=meet(X0,join(sF1_fnc,join(meet(X0,X1),meet(X1,sF8_fnc)))))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f4614,f19])).
% 82.67/11.04 fof(f4740,plain,(
% 82.67/11.04 ![X0,X1]: (meet(X0,join(sF1_fnc,meet(X1,join(X0,sF8_fnc))))=meet(X0,join(sF1_fnc,meet(X1,join(X0,a)))))),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f4710,f4733])).
% 82.67/11.04 fof(f4766,plain,(
% 82.67/11.04 meet(sF0_fnc,sF8_fnc)=meet(a,sF1_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f4657,f133])).
% 82.67/11.04 fof(f4780,plain,(
% 82.67/11.04 meet(sF0_fnc,sF8_fnc)=sF0_fnc),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f23,f4766])).
% 82.67/11.04 fof(f4800,plain,(
% 82.67/11.04 join(sF8_fnc,sF0_fnc)=sF8_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f4780,f55])).
% 82.67/11.04 fof(f4837,plain,(
% 82.67/11.04 join(sF0_fnc,sF8_fnc)=sF8_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f16,f4800])).
% 82.67/11.04 fof(f4857,plain,(
% 82.67/11.04 join(sF4_fnc,sF8_fnc)=sF8_fnc),
% 82.67/11.04 inference(backward_demodulation,[status(thm)],[f4837,f3798])).
% 82.67/11.04 fof(f4900,plain,(
% 82.67/11.04 meet(sF4_fnc,sF8_fnc)=sF4_fnc),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f4857,f13])).
% 82.67/11.04 fof(f5936,plain,(
% 82.67/11.04 join(sF0_fnc,b)=join(b,sF1_fnc)),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f4611,f3482])).
% 82.67/11.04 fof(f5954,plain,(
% 82.67/11.04 join(sF0_fnc,b)=sF1_fnc),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f80,f5936])).
% 82.67/11.04 fof(f5971,plain,(
% 82.67/11.04 ![X0]: (join(X0,sF1_fnc)=join(sF0_fnc,join(b,X0)))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f5954,f149])).
% 82.67/11.04 fof(f7921,plain,(
% 82.67/11.04 join(sF1_fnc,sF4_fnc)=join(sF1_fnc,join(b,sF4_fnc))),
% 82.67/11.04 inference(paramodulation,[status(thm)],[f4566,f177])).
% 82.67/11.04 fof(f7933,plain,(
% 82.67/11.04 join(b,sF4_fnc)=join(sF1_fnc,join(b,sF4_fnc))),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f4566,f7921])).
% 82.67/11.04 fof(f7935,plain,(
% 82.67/11.04 join(b,sF4_fnc)=join(sF4_fnc,sF1_fnc)),
% 82.67/11.04 inference(forward_demodulation,[status(thm)],[f3456,f7933])).
% 83.47/11.06 fof(f7955,plain,(
% 83.47/11.06 join(sF1_fnc,sF7_fnc)=join(sF1_fnc,join(b,sF7_fnc))),
% 83.47/11.06 inference(paramodulation,[status(thm)],[f4568,f177])).
% 83.47/11.06 fof(f7968,plain,(
% 83.47/11.06 join(b,sF7_fnc)=join(sF1_fnc,join(b,sF7_fnc))),
% 83.47/11.06 inference(forward_demodulation,[status(thm)],[f4568,f7955])).
% 83.47/11.06 fof(f7970,plain,(
% 83.47/11.06 join(b,sF7_fnc)=join(sF7_fnc,sF1_fnc)),
% 83.47/11.06 inference(forward_demodulation,[status(thm)],[f3456,f7968])).
% 83.47/11.06 fof(f9781,plain,(
% 83.47/11.06 join(sF4_fnc,sF1_fnc)=join(sF0_fnc,join(b,sF7_fnc))),
% 83.47/11.06 inference(paramodulation,[status(thm)],[f7970,f165])).
% 83.47/11.06 fof(f9808,plain,(
% 83.47/11.06 join(b,sF4_fnc)=join(sF0_fnc,join(b,sF7_fnc))),
% 83.47/11.06 inference(forward_demodulation,[status(thm)],[f7935,f9781])).
% 83.47/11.06 fof(f9810,plain,(
% 83.47/11.06 join(b,sF4_fnc)=join(sF7_fnc,sF1_fnc)),
% 83.47/11.06 inference(forward_demodulation,[status(thm)],[f5971,f9808])).
% 83.47/11.06 fof(f10508,plain,(
% 83.47/11.06 meet(a,join(sF1_fnc,meet(sF4_fnc,join(a,sF8_fnc))))=meet(a,join(sF1_fnc,join(sF3_fnc,meet(sF4_fnc,sF8_fnc))))),
% 83.47/11.06 inference(paramodulation,[status(thm)],[f4614,f201])).
% 83.47/11.06 fof(f10764,plain,(
% 83.47/11.06 meet(a,join(sF1_fnc,meet(sF4_fnc,join(a,a))))=meet(a,join(sF1_fnc,join(sF3_fnc,meet(sF4_fnc,sF8_fnc))))),
% 83.47/11.06 inference(forward_demodulation,[status(thm)],[f4740,f10508])).
% 83.47/11.06 fof(f10765,plain,(
% 83.47/11.06 meet(a,join(sF1_fnc,meet(sF4_fnc,a)))=meet(a,join(sF1_fnc,join(sF3_fnc,meet(sF4_fnc,sF8_fnc))))),
% 83.47/11.06 inference(forward_demodulation,[status(thm)],[f12,f10764])).
% 83.47/11.06 fof(f10766,plain,(
% 83.47/11.06 meet(a,join(sF1_fnc,sF3_fnc))=meet(a,join(sF1_fnc,join(sF3_fnc,meet(sF4_fnc,sF8_fnc))))),
% 83.47/11.06 inference(forward_demodulation,[status(thm)],[f2629,f10765])).
% 83.47/11.06 fof(f10767,plain,(
% 83.47/11.06 meet(a,join(b,sF3_fnc))=meet(a,join(sF1_fnc,join(sF3_fnc,meet(sF4_fnc,sF8_fnc))))),
% 83.47/11.06 inference(forward_demodulation,[status(thm)],[f4569,f10766])).
% 83.47/11.06 fof(f10768,plain,(
% 83.47/11.06 meet(a,join(b,sF3_fnc))=meet(a,join(sF1_fnc,join(sF3_fnc,sF4_fnc)))),
% 83.47/11.06 inference(forward_demodulation,[status(thm)],[f4900,f10767])).
% 83.47/11.06 fof(f10769,plain,(
% 83.47/11.06 meet(a,join(b,sF3_fnc))=meet(a,join(sF1_fnc,sF4_fnc))),
% 83.47/11.06 inference(forward_demodulation,[status(thm)],[f100,f10768])).
% 83.47/11.06 fof(f10772,plain,(
% 83.47/11.06 meet(a,join(b,sF3_fnc))=meet(a,join(b,sF4_fnc))),
% 83.47/11.06 inference(forward_demodulation,[status(thm)],[f4566,f10769])).
% 83.47/11.06 fof(f11720,plain,(
% 83.47/11.06 meet(a,join(sF1_fnc,meet(c,join(a,sF8_fnc))))=meet(a,join(sF1_fnc,join(sF2_fnc,meet(c,sF8_fnc))))),
% 83.47/11.06 inference(paramodulation,[status(thm)],[f4614,f203])).
% 83.47/11.06 fof(f12002,plain,(
% 83.47/11.06 meet(a,join(sF1_fnc,meet(c,join(a,a))))=meet(a,join(sF1_fnc,join(sF2_fnc,meet(c,sF8_fnc))))),
% 83.47/11.06 inference(forward_demodulation,[status(thm)],[f4740,f11720])).
% 83.47/11.06 fof(f12003,plain,(
% 83.47/11.06 meet(a,join(sF1_fnc,meet(c,a)))=meet(a,join(sF1_fnc,join(sF2_fnc,meet(c,sF8_fnc))))),
% 83.47/11.06 inference(forward_demodulation,[status(thm)],[f12,f12002])).
% 83.47/11.06 fof(f12004,plain,(
% 83.47/11.06 meet(a,join(sF1_fnc,sF2_fnc))=meet(a,join(sF1_fnc,join(sF2_fnc,meet(c,sF8_fnc))))),
% 83.47/11.06 inference(forward_demodulation,[status(thm)],[f2637,f12003])).
% 83.47/11.06 fof(f12005,plain,(
% 83.47/11.06 meet(a,sF1_fnc)=meet(a,join(sF1_fnc,join(sF2_fnc,meet(c,sF8_fnc))))),
% 83.47/11.06 inference(forward_demodulation,[status(thm)],[f1008,f12004])).
% 83.47/11.06 fof(f12006,plain,(
% 83.47/11.06 sF0_fnc=meet(a,join(sF1_fnc,join(sF2_fnc,meet(c,sF8_fnc))))),
% 66.49/11.20 inference(forward_demodulation,[status(thm)],[f23,f12005])).
% 66.49/11.20 fof(f12007,plain,(
% 66.49/11.20 sF0_fnc=meet(a,join(meet(c,sF8_fnc),sF1_fnc))),
% 66.49/11.20 inference(forward_demodulation,[status(thm)],[f3454,f12006])).
% 66.49/11.20 fof(f12008,plain,(
% 66.49/11.20 sF0_fnc=meet(a,join(sF7_fnc,sF1_fnc))),
% 66.49/11.20 inference(forward_demodulation,[status(thm)],[f27,f12007])).
% 66.49/11.20 fof(f12009,plain,(
% 66.49/11.20 meet(a,join(b,sF3_fnc))=sF0_fnc),
% 66.49/11.20 inference(backward_demodulation,[status(thm)],[f12010,f10772])).
% 66.49/11.20 fof(f12010,plain,(
% 66.49/11.20 sF0_fnc=meet(a,join(b,sF4_fnc))),
% 66.49/11.20 inference(forward_demodulation,[status(thm)],[f9810,f12008])).
% 66.49/11.20 fof(f15447,plain,(
% 66.49/11.20 meet(join(b,sF3_fnc),a)=meet(join(b,sF3_fnc),sF0_fnc)),
% 66.49/11.20 inference(paramodulation,[status(thm)],[f12009,f476])).
% 66.49/11.20 fof(f15478,plain,(
% 66.49/11.20 meet(join(b,sF3_fnc),a)=sF0_fnc),
% 66.49/11.20 inference(forward_demodulation,[status(thm)],[f4096,f15447])).
% 66.49/11.20 fof(f20606,plain,(
% 66.49/11.20 meet(sF3_fnc,a)=meet(sF3_fnc,sF0_fnc)),
% 66.49/11.20 inference(paramodulation,[status(thm)],[f15478,f725])).
% 66.49/11.20 fof(f20817,plain,(
% 66.49/11.20 sF3_fnc=meet(sF3_fnc,sF0_fnc)),
% 66.49/11.20 inference(forward_demodulation,[status(thm)],[f707,f20606])).
% 66.49/11.20 fof(f20818,plain,(
% 66.49/11.20 sF3_fnc=sF0_fnc),
% 66.49/11.20 inference(forward_demodulation,[status(thm)],[f1858,f20817])).
% 66.49/11.20 fof(f20819,plain,(
% 66.49/11.20 $false),
% 66.49/11.20 inference(forward_subsumption_resolution,[status(thm)],[f20818,f30])).
% 66.49/11.20 % SZS output end CNFRefutation for theBenchmark.p
% 66.49/11.22 % Elapsed time: 10.768738 seconds
% 66.49/11.22 % CPU time: 84.700630 seconds
% 66.49/11.22 % Total memory used: 438.914 MB
% 66.49/11.22 % Net memory used: 432.662 MB
%------------------------------------------------------------------------------