%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP186-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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 12:36:13 PM UTC 2026
% Result : Unsatisfiable 167.34s 40.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP186-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.57 % Computer : n017.cluster.edu
% 0.20/0.57 % Model : x86_64 x86_64
% 0.20/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.57 % Memory : 8046.5625MB
% 0.20/0.57 % OS : Linux 6.8.0-71-generic
% 0.20/0.57 % CPULimit : 300
% 0.20/0.57 % WCLimit : 300
% 0.20/0.57 % DateTime : Sun Sep 20 20:00:41 UTC 2026
% 0.20/0.58 % CPUTime :
% 0.20/0.59 % Drodi V4.1.1
% 167.34/40.32 % Refutation found
% 167.34/40.32 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 167.34/40.32 % SZS output start CNFRefutation for theBenchmark
% 167.34/40.32 fof(f1,axiom,(
% 167.34/40.32 (![X]: (multiply(identity,X) = X ))),
% 167.34/40.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 167.34/40.32 fof(f2,axiom,(
% 167.34/40.32 (![X]: (multiply(inverse(X),X) = identity ))),
% 167.34/40.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 167.34/40.32 fof(f3,axiom,(
% 167.34/40.32 (![X,Y,Z]: (multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ))),
% 167.34/40.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 167.34/40.32 fof(f4,axiom,(
% 167.34/40.32 (![X,Y]: (greatest_lower_bound(X,Y) = greatest_lower_bound(Y,X) ))),
% 167.34/40.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 167.34/40.32 fof(f5,axiom,(
% 167.34/40.32 (![X,Y]: (least_upper_bound(X,Y) = least_upper_bound(Y,X) ))),
% 167.34/40.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 167.34/40.32 fof(f6,axiom,(
% 167.34/40.32 (![X,Y,Z]: (greatest_lower_bound(X,greatest_lower_bound(Y,Z)) = greatest_lower_bound(greatest_lower_bound(X,Y),Z) ))),
% 167.34/40.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 167.34/40.32 fof(f7,axiom,(
% 167.34/40.32 (![X,Y,Z]: (least_upper_bound(X,least_upper_bound(Y,Z)) = least_upper_bound(least_upper_bound(X,Y),Z) ))),
% 167.34/40.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 167.34/40.32 fof(f10,axiom,(
% 167.34/40.32 (![X,Y]: (least_upper_bound(X,greatest_lower_bound(X,Y)) = X ))),
% 167.34/40.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 167.34/40.32 fof(f11,axiom,(
% 167.34/40.32 (![X,Y]: (greatest_lower_bound(X,least_upper_bound(X,Y)) = X ))),
% 167.34/40.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 167.34/40.32 fof(f12,axiom,(
% 167.34/40.32 (![X,Y,Z]: (multiply(X,least_upper_bound(Y,Z)) = least_upper_bound(multiply(X,Y),multiply(X,Z)) ))),
% 167.34/40.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 167.34/40.32 fof(f13,axiom,(
% 167.34/40.32 (![X,Y,Z]: (multiply(X,greatest_lower_bound(Y,Z)) = greatest_lower_bound(multiply(X,Y),multiply(X,Z)) ))),
% 167.34/40.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 167.34/40.32 fof(f14,axiom,(
% 167.34/40.32 (![Y,Z,X]: (multiply(least_upper_bound(Y,Z),X) = least_upper_bound(multiply(Y,X),multiply(Z,X)) ))),
% 167.34/40.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 167.34/40.32 fof(f15,axiom,(
% 167.34/40.32 (![Y,Z,X]: (multiply(greatest_lower_bound(Y,Z),X) = greatest_lower_bound(multiply(Y,X),multiply(Z,X)) ))),
% 167.34/40.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 167.34/40.32 fof(f16,negated_conjecture,(
% 167.34/40.32 least_upper_bound(multiply(a,b),identity) != multiply(a,inverse(greatest_lower_bound(a,inverse(b)))) ),
% 167.34/40.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 167.34/40.32 fof(f17,plain,(
% 167.34/40.32 ![X0]: (multiply(identity,X0)=X0)),
% 167.34/40.32 inference(cnf_transformation,[status(thm)],[f1])).
% 167.34/40.32 fof(f18,plain,(
% 167.34/40.32 ![X0]: (multiply(inverse(X0),X0)=identity)),
% 167.34/40.32 inference(cnf_transformation,[status(thm)],[f2])).
% 167.34/40.32 fof(f19,plain,(
% 167.34/40.32 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,multiply(X1,X2)))),
% 167.34/40.32 inference(cnf_transformation,[status(thm)],[f3])).
% 167.34/40.32 fof(f20,plain,(
% 167.34/40.32 ![X0,X1]: (greatest_lower_bound(X0,X1)=greatest_lower_bound(X1,X0))),
% 167.34/40.32 inference(cnf_transformation,[status(thm)],[f4])).
% 167.34/40.32 fof(f21,plain,(
% 167.34/40.32 ![X0,X1]: (least_upper_bound(X0,X1)=least_upper_bound(X1,X0))),
% 167.34/40.32 inference(cnf_transformation,[status(thm)],[f5])).
% 167.34/40.32 fof(f22,plain,(
% 167.34/40.32 ![X0,X1,X2]: (greatest_lower_bound(X0,greatest_lower_bound(X1,X2))=greatest_lower_bound(greatest_lower_bound(X0,X1),X2))),
% 167.34/40.32 inference(cnf_transformation,[status(thm)],[f6])).
% 167.34/40.32 fof(f23,plain,(
% 167.34/40.32 ![X0,X1,X2]: (least_upper_bound(X0,least_upper_bound(X1,X2))=least_upper_bound(least_upper_bound(X0,X1),X2))),
% 167.34/40.32 inference(cnf_transformation,[status(thm)],[f7])).
% 167.34/40.32 fof(f26,plain,(
% 167.34/40.32 ![X0,X1]: (least_upper_bound(X0,greatest_lower_bound(X0,X1))=X0)),
% 167.34/40.32 inference(cnf_transformation,[status(thm)],[f10])).
% 167.34/40.32 fof(f27,plain,(
% 167.34/40.32 ![X0,X1]: (greatest_lower_bound(X0,least_upper_bound(X0,X1))=X0)),
% 167.34/40.32 inference(cnf_transformation,[status(thm)],[f11])).
% 167.34/40.32 fof(f28,plain,(
% 167.34/40.32 ![X0,X1,X2]: (multiply(X0,least_upper_bound(X1,X2))=least_upper_bound(multiply(X0,X1),multiply(X0,X2)))),
% 167.34/40.32 inference(cnf_transformation,[status(thm)],[f12])).
% 167.34/40.32 fof(f29,plain,(
% 167.34/40.32 ![X0,X1,X2]: (multiply(X0,greatest_lower_bound(X1,X2))=greatest_lower_bound(multiply(X0,X1),multiply(X0,X2)))),
% 167.34/40.32 inference(cnf_transformation,[status(thm)],[f13])).
% 167.34/40.32 fof(f30,plain,(
% 167.34/40.32 ![X0,X1,X2]: (multiply(least_upper_bound(X0,X1),X2)=least_upper_bound(multiply(X0,X2),multiply(X1,X2)))),
% 167.34/40.32 inference(cnf_transformation,[status(thm)],[f14])).
% 167.34/40.32 fof(f31,plain,(
% 167.34/40.32 ![X0,X1,X2]: (multiply(greatest_lower_bound(X0,X1),X2)=greatest_lower_bound(multiply(X0,X2),multiply(X1,X2)))),
% 167.34/40.32 inference(cnf_transformation,[status(thm)],[f15])).
% 167.34/40.32 fof(f32,plain,(
% 167.34/40.32 ~least_upper_bound(multiply(a,b),identity)=multiply(a,inverse(greatest_lower_bound(a,inverse(b))))),
% 167.34/40.32 inference(cnf_transformation,[status(thm)],[f16])).
% 167.34/40.32 fof(f33,definition,(
% 167.34/40.32 sF1_fnc=multiply(a,b)),
% 167.34/40.32 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 167.34/40.32 fof(f34,definition,(
% 167.34/40.32 sF0_fnc=least_upper_bound(sF1_fnc,identity)),
% 167.34/40.32 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 167.34/40.32 fof(f35,definition,(
% 167.34/40.32 sF5_fnc=inverse(b)),
% 167.34/40.32 introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition])).
% 167.34/40.32 fof(f36,definition,(
% 167.34/40.32 sF4_fnc=greatest_lower_bound(a,sF5_fnc)),
% 167.34/40.32 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 167.34/40.32 fof(f37,definition,(
% 167.34/40.32 sF3_fnc=inverse(sF4_fnc)),
% 167.34/40.32 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 167.34/40.32 fof(f38,definition,(
% 167.34/40.32 sF2_fnc=multiply(a,sF3_fnc)),
% 167.34/40.32 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 167.34/40.32 fof(f39,plain,(
% 167.34/40.32 ~sF0_fnc=sF2_fnc),
% 167.34/40.32 inference(definition_folding,[],[f32,f38,f37,f36,f35,f34,f33])).
% 167.34/40.32 fof(f40,plain,(
% 167.34/40.32 sF0_fnc=least_upper_bound(identity,sF1_fnc)),
% 167.34/40.32 inference(forward_demodulation,[status(thm)],[f21,f34])).
% 167.34/40.32 fof(f41,plain,(
% 167.34/40.32 multiply(sF3_fnc,sF4_fnc)=identity),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f37,f18])).
% 167.34/40.32 fof(f42,plain,(
% 167.34/40.32 multiply(sF5_fnc,b)=identity),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f35,f18])).
% 167.34/40.32 fof(f43,plain,(
% 167.34/40.32 least_upper_bound(a,sF4_fnc)=a),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f36,f26])).
% 167.34/40.32 fof(f46,plain,(
% 167.34/40.32 greatest_lower_bound(identity,sF0_fnc)=identity),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f40,f27])).
% 167.34/40.32 fof(f55,plain,(
% 167.34/40.32 ![X0,X1]: (least_upper_bound(X0,greatest_lower_bound(X1,X0))=X0)),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f20,f26])).
% 167.34/40.32 fof(f59,plain,(
% 167.34/40.32 least_upper_bound(sF5_fnc,sF4_fnc)=sF5_fnc),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f36,f55])).
% 167.34/40.32 fof(f60,plain,(
% 167.34/40.32 ![X0,X1]: (least_upper_bound(least_upper_bound(X0,X1),X0)=least_upper_bound(X0,X1))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f27,f55])).
% 167.34/40.32 fof(f67,plain,(
% 167.34/40.32 least_upper_bound(sF4_fnc,sF5_fnc)=sF5_fnc),
% 167.34/40.32 inference(forward_demodulation,[status(thm)],[f21,f59])).
% 167.34/40.32 fof(f68,plain,(
% 167.34/40.32 ![X0,X1]: (least_upper_bound(X0,least_upper_bound(X1,X0))=least_upper_bound(X0,X1))),
% 167.34/40.32 inference(forward_demodulation,[status(thm)],[f23,f60])).
% 167.34/40.32 fof(f70,plain,(
% 167.34/40.32 ![X0]: (multiply(identity,X0)=multiply(sF5_fnc,multiply(b,X0)))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f42,f19])).
% 167.34/40.32 fof(f71,plain,(
% 167.34/40.32 ![X0]: (multiply(identity,X0)=multiply(sF3_fnc,multiply(sF4_fnc,X0)))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f41,f19])).
% 167.34/40.32 fof(f72,plain,(
% 167.34/40.32 ![X0,X1]: (multiply(identity,X0)=multiply(inverse(X1),multiply(X1,X0)))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f18,f19])).
% 167.34/40.32 fof(f74,plain,(
% 167.34/40.32 ![X0]: (multiply(sF2_fnc,X0)=multiply(a,multiply(sF3_fnc,X0)))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f38,f19])).
% 167.34/40.32 fof(f75,plain,(
% 167.34/40.32 ![X0]: (multiply(sF1_fnc,X0)=multiply(a,multiply(b,X0)))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f33,f19])).
% 167.34/40.32 fof(f78,plain,(
% 167.34/40.32 ![X0]: (X0=multiply(sF5_fnc,multiply(b,X0)))),
% 167.34/40.32 inference(forward_demodulation,[status(thm)],[f17,f70])).
% 167.34/40.32 fof(f79,plain,(
% 167.34/40.32 ![X0]: (X0=multiply(sF3_fnc,multiply(sF4_fnc,X0)))),
% 167.34/40.32 inference(forward_demodulation,[status(thm)],[f17,f71])).
% 167.34/40.32 fof(f80,plain,(
% 167.34/40.32 ![X0,X1]: (X0=multiply(inverse(X1),multiply(X1,X0)))),
% 167.34/40.32 inference(forward_demodulation,[status(thm)],[f17,f72])).
% 167.34/40.32 fof(f85,plain,(
% 167.34/40.32 ![X0,X1]: (greatest_lower_bound(X0,least_upper_bound(X1,X0))=X0)),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f21,f27])).
% 167.34/40.32 fof(f96,plain,(
% 167.34/40.32 greatest_lower_bound(sF1_fnc,sF0_fnc)=sF1_fnc),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f40,f85])).
% 167.34/40.32 fof(f97,plain,(
% 167.34/40.32 ![X0,X1]: (greatest_lower_bound(greatest_lower_bound(X0,X1),X1)=greatest_lower_bound(X0,X1))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f55,f85])).
% 167.34/40.32 fof(f103,plain,(
% 167.34/40.32 ![X0,X1]: (least_upper_bound(least_upper_bound(X0,X1),X1)=least_upper_bound(X0,X1))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f85,f55])).
% 167.34/40.32 fof(f106,plain,(
% 167.34/40.32 greatest_lower_bound(sF0_fnc,sF1_fnc)=sF1_fnc),
% 167.34/40.32 inference(forward_demodulation,[status(thm)],[f20,f96])).
% 167.34/40.32 fof(f107,plain,(
% 167.34/40.32 ![X0,X1]: (greatest_lower_bound(X0,greatest_lower_bound(X1,X0))=greatest_lower_bound(X1,X0))),
% 167.34/40.32 inference(forward_demodulation,[status(thm)],[f20,f97])).
% 167.34/40.32 fof(f109,plain,(
% 167.34/40.32 ![X0,X1]: (least_upper_bound(X0,least_upper_bound(X1,X0))=least_upper_bound(X1,X0))),
% 167.34/40.32 inference(forward_demodulation,[status(thm)],[f21,f103])).
% 167.34/40.32 fof(f124,plain,(
% 167.34/40.32 ![X0]: (multiply(b,X0)=multiply(inverse(sF5_fnc),X0))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f78,f80])).
% 167.34/40.32 fof(f126,plain,(
% 167.34/40.32 ![X0]: (multiply(sF4_fnc,X0)=multiply(inverse(sF3_fnc),X0))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f79,f80])).
% 167.34/40.32 fof(f128,plain,(
% 167.34/40.32 ![X0,X1]: (multiply(X0,X1)=multiply(inverse(inverse(X0)),X1))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f80,f80])).
% 167.34/40.32 fof(f129,plain,(
% 167.34/40.32 ![X0]: (X0=multiply(inverse(inverse(X0)),identity))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f18,f80])).
% 167.34/40.32 fof(f138,plain,(
% 167.34/40.32 ![X0]: (X0=multiply(X0,identity))),
% 167.34/40.32 inference(forward_demodulation,[status(thm)],[f128,f129])).
% 167.34/40.32 fof(f192,plain,(
% 167.34/40.32 ![X0,X1]: (greatest_lower_bound(X0,greatest_lower_bound(X0,X1))=greatest_lower_bound(X1,X0))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f20,f107])).
% 167.34/40.32 fof(f202,plain,(
% 167.34/40.32 ![X0]: (multiply(b,multiply(sF5_fnc,X0))=X0)),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f80,f124])).
% 167.34/40.32 fof(f204,plain,(
% 167.34/40.32 multiply(b,identity)=inverse(sF5_fnc)),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f138,f124])).
% 167.34/40.32 fof(f211,plain,(
% 167.34/40.32 b=inverse(sF5_fnc)),
% 167.34/40.32 inference(forward_demodulation,[status(thm)],[f138,f204])).
% 167.34/40.32 fof(f220,plain,(
% 167.34/40.32 ![X0,X1,X2]: (greatest_lower_bound(X0,greatest_lower_bound(X1,X2))=greatest_lower_bound(X2,greatest_lower_bound(X0,X1)))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f20,f22])).
% 167.34/40.32 fof(f231,plain,(
% 167.34/40.32 ![X0,X1,X2]: (greatest_lower_bound(X0,greatest_lower_bound(least_upper_bound(X0,X1),X2))=greatest_lower_bound(X0,X2))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f27,f22])).
% 167.34/40.32 fof(f255,plain,(
% 167.34/40.32 ![X0,X1,X2]: (least_upper_bound(X0,least_upper_bound(X1,X2))=least_upper_bound(X2,least_upper_bound(X0,X1)))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f21,f23])).
% 167.34/40.32 fof(f264,plain,(
% 167.34/40.32 ![X0,X1,X2]: (least_upper_bound(X0,least_upper_bound(least_upper_bound(X1,X0),X2))=least_upper_bound(least_upper_bound(X0,X1),X2))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f68,f23])).
% 167.34/40.32 fof(f283,plain,(
% 167.34/40.32 ![X0,X1,X2]: (least_upper_bound(X0,least_upper_bound(X1,least_upper_bound(X0,X2)))=least_upper_bound(least_upper_bound(X0,X1),X2))),
% 167.34/40.32 inference(forward_demodulation,[status(thm)],[f23,f264])).
% 167.34/40.32 fof(f284,plain,(
% 167.34/40.32 ![X0,X1,X2]: (least_upper_bound(X0,least_upper_bound(X1,least_upper_bound(X0,X2)))=least_upper_bound(X0,least_upper_bound(X1,X2)))),
% 167.34/40.32 inference(forward_demodulation,[status(thm)],[f23,f283])).
% 167.34/40.32 fof(f288,plain,(
% 167.34/40.32 ![X0,X1,X2]: (multiply(X0,least_upper_bound(X1,X2))=least_upper_bound(multiply(X0,X2),multiply(X0,X1)))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f21,f28])).
% 167.34/40.32 fof(f299,plain,(
% 167.34/40.32 ![X0,X1]: (multiply(inverse(X0),least_upper_bound(X0,X1))=least_upper_bound(identity,multiply(inverse(X0),X1)))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f18,f28])).
% 167.34/40.32 fof(f301,plain,(
% 167.34/40.32 ![X0]: (multiply(a,least_upper_bound(sF3_fnc,X0))=least_upper_bound(sF2_fnc,multiply(a,X0)))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f38,f28])).
% 167.34/40.32 fof(f312,plain,(
% 167.34/40.32 ![X0,X1]: (multiply(inverse(X0),least_upper_bound(X1,X0))=least_upper_bound(multiply(inverse(X0),X1),identity))),
% 167.34/40.32 inference(paramodulation,[status(thm)],[f18,f28])).
% 167.34/40.32 fof(f335,plain,(
% 167.34/40.32 ![X0,X1]: (multiply(inverse(X0),least_upper_bound(X1,X0))=least_upper_bound(identity,multiply(inverse(X0),X1)))),
% 167.34/40.32 inference(forward_demodulation,[status(thm)],[f21,f312])).
% 167.34/40.32 fof(f361,plain,(
% 167.34/40.32 ![X0]: (multiply(sF4_fnc,multiply(sF3_fnc,X0))=X0)),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f80,f126])).
% 167.34/40.33 fof(f362,plain,(
% 167.34/40.33 multiply(sF4_fnc,sF3_fnc)=identity),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f18,f126])).
% 167.34/40.33 fof(f363,plain,(
% 167.34/40.33 multiply(sF4_fnc,identity)=inverse(sF3_fnc)),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f138,f126])).
% 167.34/40.33 fof(f372,plain,(
% 167.34/40.33 sF4_fnc=inverse(sF3_fnc)),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f138,f363])).
% 167.34/40.33 fof(f399,plain,(
% 167.34/40.33 ![X0]: (multiply(sF2_fnc,multiply(sF4_fnc,X0))=multiply(a,X0))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f79,f74])).
% 167.34/40.33 fof(f474,plain,(
% 167.34/40.33 ![X0,X1]: (least_upper_bound(X0,least_upper_bound(X0,X1))=least_upper_bound(X1,X0))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f21,f109])).
% 167.34/40.33 fof(f526,plain,(
% 167.34/40.33 ![X0,X1]: (least_upper_bound(greatest_lower_bound(X0,X1),greatest_lower_bound(X1,X0))=greatest_lower_bound(X0,X1))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f192,f55])).
% 167.34/40.33 fof(f616,plain,(
% 167.34/40.33 ![X0,X1]: (multiply(X0,multiply(inverse(X0),X1))=X1)),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f80,f128])).
% 167.34/40.33 fof(f617,plain,(
% 167.34/40.33 ![X0]: (multiply(X0,inverse(X0))=identity)),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f18,f128])).
% 167.34/40.33 fof(f618,plain,(
% 167.34/40.33 ![X0]: (multiply(X0,identity)=inverse(inverse(X0)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f138,f128])).
% 167.34/40.33 fof(f632,plain,(
% 167.34/40.33 ![X0]: (X0=inverse(inverse(X0)))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f138,f618])).
% 167.34/40.33 fof(f650,plain,(
% 167.34/40.33 ![X0,X1]: (multiply(X0,multiply(X1,inverse(multiply(X0,X1))))=identity)),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f19,f617])).
% 167.34/40.33 fof(f774,plain,(
% 167.34/40.33 ![X0,X1,X2]: (least_upper_bound(X0,least_upper_bound(X1,least_upper_bound(least_upper_bound(X0,X1),X2)))=least_upper_bound(X2,least_upper_bound(X0,X1)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f23,f474])).
% 167.34/40.33 fof(f804,plain,(
% 167.34/40.33 ![X0,X1,X2]: (least_upper_bound(X0,least_upper_bound(X1,least_upper_bound(X0,least_upper_bound(X1,X2))))=least_upper_bound(X2,least_upper_bound(X0,X1)))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f23,f774])).
% 167.34/40.33 fof(f805,plain,(
% 167.34/40.33 ![X0,X1,X2]: (least_upper_bound(X0,least_upper_bound(X1,least_upper_bound(X1,X2)))=least_upper_bound(X2,least_upper_bound(X0,X1)))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f284,f804])).
% 167.34/40.33 fof(f806,plain,(
% 167.34/40.33 ![X0,X1,X2]: (least_upper_bound(X0,least_upper_bound(X1,X2))=least_upper_bound(X1,least_upper_bound(X0,X2)))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f474,f805])).
% 167.34/40.33 fof(f865,plain,(
% 167.34/40.33 ![X0,X1]: (multiply(inverse(X0),greatest_lower_bound(X0,X1))=greatest_lower_bound(identity,multiply(inverse(X0),X1)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f18,f29])).
% 167.34/40.33 fof(f868,plain,(
% 167.34/40.33 ![X0]: (multiply(a,greatest_lower_bound(sF3_fnc,X0))=greatest_lower_bound(sF2_fnc,multiply(a,X0)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f38,f29])).
% 167.34/40.33 fof(f872,plain,(
% 167.34/40.33 ![X0,X1]: (multiply(X0,greatest_lower_bound(identity,X1))=greatest_lower_bound(X0,multiply(X0,X1)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f138,f29])).
% 167.34/40.33 fof(f886,plain,(
% 167.34/40.33 ![X0,X1,X2]: (multiply(inverse(X0),greatest_lower_bound(X1,multiply(X0,X2)))=greatest_lower_bound(multiply(inverse(X0),X1),X2))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f80,f29])).
% 167.34/40.33 fof(f955,plain,(
% 167.34/40.33 ![X0,X1]: (multiply(least_upper_bound(identity,X0),X1)=least_upper_bound(X1,multiply(X0,X1)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f17,f30])).
% 167.34/40.33 fof(f960,plain,(
% 167.34/40.33 ![X0,X1]: (multiply(least_upper_bound(X0,X1),inverse(X0))=least_upper_bound(identity,multiply(X1,inverse(X0))))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f617,f30])).
% 167.34/40.33 fof(f1601,plain,(
% 167.34/40.33 ![X0,X1,X2,X3]: (multiply(greatest_lower_bound(multiply(X0,X1),X2),X3)=greatest_lower_bound(multiply(X0,multiply(X1,X3)),multiply(X2,X3)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f19,f31])).
% 167.34/40.33 fof(f1612,plain,(
% 167.34/40.33 ![X0,X1]: (multiply(greatest_lower_bound(identity,X0),X1)=greatest_lower_bound(X1,multiply(X0,X1)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f17,f31])).
% 167.34/40.33 fof(f1615,plain,(
% 167.34/40.33 ![X0]: (multiply(greatest_lower_bound(a,X0),sF3_fnc)=greatest_lower_bound(sF2_fnc,multiply(X0,sF3_fnc)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f38,f31])).
% 167.34/40.33 fof(f1616,plain,(
% 167.34/40.33 ![X0]: (multiply(greatest_lower_bound(a,X0),b)=greatest_lower_bound(sF1_fnc,multiply(X0,b)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f33,f31])).
% 167.34/40.33 fof(f1882,plain,(
% 167.34/40.33 ![X0,X1,X2]: (greatest_lower_bound(X0,X1)=greatest_lower_bound(least_upper_bound(X1,X2),greatest_lower_bound(X0,X1)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f27,f220])).
% 167.34/40.33 fof(f1996,plain,(
% 167.34/40.33 ![X0,X1,X2]: (greatest_lower_bound(X0,X1)=greatest_lower_bound(X1,greatest_lower_bound(least_upper_bound(X1,X2),X0)))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f220,f1882])).
% 167.34/40.33 fof(f4404,plain,(
% 167.34/40.33 ![X0,X1]: (multiply(X0,inverse(multiply(X1,X0)))=multiply(inverse(X1),identity))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f650,f80])).
% 167.34/40.33 fof(f4495,plain,(
% 167.34/40.33 ![X0,X1]: (multiply(X0,inverse(multiply(X1,X0)))=inverse(X1))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f138,f4404])).
% 167.34/40.33 fof(f4528,plain,(
% 167.34/40.33 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),inverse(inverse(X0)))=inverse(X1))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f4495,f4495])).
% 167.34/40.33 fof(f4536,plain,(
% 167.34/40.33 ![X0]: (multiply(b,inverse(X0))=inverse(multiply(X0,sF5_fnc)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f4495,f202])).
% 167.34/40.33 fof(f4538,plain,(
% 167.34/40.33 ![X0]: (multiply(sF4_fnc,inverse(X0))=inverse(multiply(X0,sF3_fnc)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f4495,f361])).
% 167.34/40.33 fof(f4539,plain,(
% 167.34/40.33 ![X0,X1]: (multiply(X0,inverse(X1))=inverse(multiply(X1,inverse(X0))))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f4495,f616])).
% 167.34/40.33 fof(f4549,plain,(
% 167.34/40.33 ![X0,X1]: (inverse(multiply(X0,X1))=multiply(inverse(X1),inverse(X0)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f4495,f80])).
% 167.34/40.33 fof(f4595,plain,(
% 167.34/40.33 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),X0)=inverse(X1))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f632,f4528])).
% 167.34/40.33 fof(f4609,plain,(
% 167.34/40.33 ![X0]: (multiply(inverse(X0),sF4_fnc)=inverse(multiply(sF3_fnc,X0)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f361,f4595])).
% 167.34/40.33 fof(f7433,plain,(
% 167.34/40.33 ![X0]: (least_upper_bound(X0,sF0_fnc)=least_upper_bound(sF1_fnc,least_upper_bound(X0,identity)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f40,f255])).
% 167.34/40.33 fof(f7660,plain,(
% 167.34/40.33 ![X0]: (least_upper_bound(X0,sF0_fnc)=least_upper_bound(identity,least_upper_bound(sF1_fnc,X0)))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f255,f7433])).
% 167.34/40.33 fof(f11585,plain,(
% 167.34/40.33 ![X0,X1,X2]: (multiply(X0,least_upper_bound(X1,multiply(inverse(X0),X2)))=least_upper_bound(X2,multiply(X0,X1)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f616,f288])).
% 167.34/40.33 fof(f14623,plain,(
% 167.34/40.33 ![X0,X1]: (multiply(inverse(least_upper_bound(identity,multiply(inverse(X0),X1))),inverse(X0))=inverse(least_upper_bound(X0,X1)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f299,f4595])).
% 167.34/40.33 fof(f14738,plain,(
% 167.34/40.33 ![X0,X1]: (inverse(multiply(X0,least_upper_bound(identity,multiply(inverse(X0),X1))))=inverse(least_upper_bound(X0,X1)))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f4549,f14623])).
% 167.34/40.33 fof(f14739,plain,(
% 167.34/40.33 ![X0,X1]: (inverse(least_upper_bound(X0,multiply(X1,identity)))=inverse(least_upper_bound(X1,X0)))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f11585,f14738])).
% 167.34/40.33 fof(f14740,plain,(
% 167.34/40.33 ![X0,X1]: (inverse(least_upper_bound(X0,X1))=inverse(least_upper_bound(X1,X0)))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f138,f14739])).
% 167.34/40.33 fof(f14866,plain,(
% 167.34/40.33 multiply(inverse(sF5_fnc),sF5_fnc)=least_upper_bound(identity,multiply(inverse(sF5_fnc),sF4_fnc))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f67,f335])).
% 167.34/40.33 fof(f14943,plain,(
% 167.34/40.33 identity=least_upper_bound(identity,multiply(inverse(sF5_fnc),sF4_fnc))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f18,f14866])).
% 167.34/40.33 fof(f14944,plain,(
% 167.34/40.33 identity=least_upper_bound(identity,inverse(multiply(sF3_fnc,sF5_fnc)))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f4609,f14943])).
% 167.34/40.33 fof(f15771,plain,(
% 167.34/40.33 ![X0,X1]: (inverse(greatest_lower_bound(X0,X1))=inverse(least_upper_bound(greatest_lower_bound(X1,X0),greatest_lower_bound(X0,X1))))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f526,f14740])).
% 167.34/40.33 fof(f15802,plain,(
% 167.34/40.33 ![X0,X1]: (multiply(least_upper_bound(X0,X1),inverse(least_upper_bound(X1,X0)))=identity)),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f14740,f617])).
% 167.34/40.33 fof(f15815,plain,(
% 167.34/40.33 ![X0,X1]: (inverse(greatest_lower_bound(X0,X1))=inverse(greatest_lower_bound(X1,X0)))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f526,f15771])).
% 167.34/40.33 fof(f15858,plain,(
% 167.34/40.33 ![X0,X1]: (multiply(greatest_lower_bound(X0,X1),inverse(greatest_lower_bound(X1,X0)))=identity)),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f15815,f617])).
% 167.34/40.33 fof(f19816,plain,(
% 167.34/40.33 multiply(b,sF4_fnc)=inverse(multiply(sF3_fnc,sF5_fnc))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f372,f4536])).
% 167.34/40.33 fof(f19849,plain,(
% 167.34/40.33 identity=least_upper_bound(identity,multiply(b,sF4_fnc))),
% 167.34/40.33 inference(backward_demodulation,[status(thm)],[f19816,f14944])).
% 167.34/40.33 fof(f20013,plain,(
% 167.34/40.33 ![X0,X1,X2]: (multiply(least_upper_bound(X0,X1),inverse(X2))=inverse(multiply(X2,inverse(least_upper_bound(X1,X0)))))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f14740,f4539])).
% 167.34/40.33 fof(f20052,plain,(
% 167.34/40.33 ![X0,X1,X2]: (multiply(least_upper_bound(X0,X1),inverse(X2))=multiply(least_upper_bound(X1,X0),inverse(X2)))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f4539,f20013])).
% 167.34/40.33 fof(f28114,plain,(
% 167.34/40.33 multiply(least_upper_bound(sF4_fnc,a),inverse(a))=identity),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f43,f15802])).
% 167.34/40.33 fof(f28453,plain,(
% 167.34/40.33 multiply(least_upper_bound(a,sF4_fnc),inverse(a))=identity),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f20052,f28114])).
% 167.34/40.33 fof(f28454,plain,(
% 167.34/40.33 least_upper_bound(identity,multiply(sF4_fnc,inverse(a)))=identity),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f960,f28453])).
% 167.34/40.33 fof(f28455,plain,(
% 167.34/40.33 least_upper_bound(identity,inverse(multiply(a,sF3_fnc)))=identity),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f4538,f28454])).
% 167.34/40.33 fof(f28456,plain,(
% 167.34/40.33 least_upper_bound(identity,inverse(sF2_fnc))=identity),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f38,f28455])).
% 167.34/40.33 fof(f28597,plain,(
% 167.34/40.33 multiply(inverse(inverse(sF2_fnc)),identity)=least_upper_bound(identity,multiply(inverse(inverse(sF2_fnc)),identity))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f28456,f335])).
% 167.34/40.33 fof(f28644,plain,(
% 167.34/40.33 inverse(inverse(sF2_fnc))=least_upper_bound(identity,multiply(inverse(inverse(sF2_fnc)),identity))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f138,f28597])).
% 167.34/40.33 fof(f28645,plain,(
% 167.34/40.33 sF2_fnc=least_upper_bound(identity,multiply(inverse(inverse(sF2_fnc)),identity))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f632,f28644])).
% 167.34/40.33 fof(f28646,plain,(
% 167.34/40.33 sF2_fnc=least_upper_bound(identity,inverse(inverse(sF2_fnc)))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f138,f28645])).
% 167.34/40.33 fof(f28647,plain,(
% 167.34/40.33 sF2_fnc=least_upper_bound(identity,sF2_fnc)),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f632,f28646])).
% 167.34/40.33 fof(f28673,plain,(
% 167.34/40.33 ![X0]: (least_upper_bound(identity,least_upper_bound(X0,sF2_fnc))=least_upper_bound(X0,sF2_fnc))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f28647,f806])).
% 167.34/40.33 fof(f35624,plain,(
% 167.34/40.33 least_upper_bound(sF2_fnc,sF0_fnc)=least_upper_bound(sF1_fnc,sF2_fnc)),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f7660,f28673])).
% 167.34/40.33 fof(f35704,plain,(
% 167.34/40.33 least_upper_bound(sF0_fnc,sF2_fnc)=least_upper_bound(sF1_fnc,sF2_fnc)),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f21,f35624])).
% 167.34/40.33 fof(f37052,plain,(
% 167.34/40.33 ![X0]: (multiply(identity,X0)=least_upper_bound(X0,multiply(multiply(b,sF4_fnc),X0)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f19849,f955])).
% 167.34/40.33 fof(f37236,plain,(
% 167.34/40.33 ![X0]: (X0=least_upper_bound(X0,multiply(multiply(b,sF4_fnc),X0)))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f17,f37052])).
% 167.34/40.33 fof(f37237,plain,(
% 167.34/40.33 ![X0]: (X0=least_upper_bound(X0,multiply(b,multiply(sF4_fnc,X0))))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f19,f37236])).
% 167.34/40.33 fof(f38839,plain,(
% 167.34/40.33 multiply(a,sF3_fnc)=least_upper_bound(sF2_fnc,multiply(a,multiply(b,multiply(sF4_fnc,sF3_fnc))))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f37237,f301])).
% 167.34/40.33 fof(f38945,plain,(
% 167.34/40.33 sF2_fnc=least_upper_bound(sF2_fnc,multiply(a,multiply(b,multiply(sF4_fnc,sF3_fnc))))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f38,f38839])).
% 167.34/40.33 fof(f38946,plain,(
% 167.34/40.33 sF2_fnc=least_upper_bound(sF2_fnc,multiply(sF1_fnc,multiply(sF4_fnc,sF3_fnc)))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f75,f38945])).
% 167.34/40.33 fof(f38947,plain,(
% 167.34/40.33 sF2_fnc=least_upper_bound(sF2_fnc,multiply(sF1_fnc,identity))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f362,f38946])).
% 167.34/40.33 fof(f38948,plain,(
% 167.34/40.33 sF2_fnc=least_upper_bound(sF2_fnc,sF1_fnc)),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f138,f38947])).
% 167.34/40.33 fof(f38949,plain,(
% 167.34/40.33 least_upper_bound(sF0_fnc,sF2_fnc)=sF2_fnc),
% 167.34/40.33 inference(backward_demodulation,[status(thm)],[f38950,f35704])).
% 167.34/40.33 fof(f38950,plain,(
% 167.34/40.33 sF2_fnc=least_upper_bound(sF1_fnc,sF2_fnc)),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f21,f38948])).
% 167.34/40.33 fof(f39505,plain,(
% 167.34/40.33 ![X0]: (greatest_lower_bound(X0,sF0_fnc)=greatest_lower_bound(sF0_fnc,greatest_lower_bound(sF2_fnc,X0)))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f38949,f1996])).
% 167.34/40.33 fof(f39515,plain,(
% 167.34/40.33 ![X0]: (greatest_lower_bound(sF0_fnc,greatest_lower_bound(sF2_fnc,X0))=greatest_lower_bound(sF0_fnc,X0))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f38949,f231])).
% 167.34/40.33 fof(f45917,plain,(
% 167.34/40.33 multiply(sF4_fnc,sF3_fnc)=greatest_lower_bound(sF2_fnc,multiply(sF5_fnc,sF3_fnc))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f36,f1615])).
% 167.34/40.33 fof(f46002,plain,(
% 167.34/40.33 identity=greatest_lower_bound(sF2_fnc,multiply(sF5_fnc,sF3_fnc))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f362,f45917])).
% 167.34/40.33 fof(f48573,plain,(
% 167.34/40.33 ![X0,X1,X2]: (multiply(greatest_lower_bound(multiply(X0,X1),X2),inverse(X1))=greatest_lower_bound(multiply(X0,identity),multiply(X2,inverse(X1))))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f617,f1601])).
% 167.34/40.33 fof(f48734,plain,(
% 167.34/40.33 ![X0,X1,X2]: (multiply(greatest_lower_bound(multiply(X0,X1),X2),inverse(X1))=greatest_lower_bound(X0,multiply(X2,inverse(X1))))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f138,f48573])).
% 167.34/40.33 fof(f54012,plain,(
% 167.34/40.33 multiply(sF4_fnc,b)=greatest_lower_bound(sF1_fnc,multiply(sF5_fnc,b))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f36,f1616])).
% 167.34/40.33 fof(f54104,plain,(
% 167.34/40.33 multiply(sF4_fnc,b)=greatest_lower_bound(sF1_fnc,identity)),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f42,f54012])).
% 167.34/40.33 fof(f54151,plain,(
% 167.34/40.33 multiply(sF4_fnc,b)=greatest_lower_bound(identity,sF1_fnc)),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f20,f54104])).
% 167.34/40.33 fof(f54835,plain,(
% 167.34/40.33 multiply(sF2_fnc,greatest_lower_bound(identity,sF1_fnc))=multiply(a,b)),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f54151,f399])).
% 167.34/40.33 fof(f54872,plain,(
% 167.34/40.33 greatest_lower_bound(sF2_fnc,multiply(sF2_fnc,sF1_fnc))=multiply(a,b)),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f872,f54835])).
% 167.34/40.33 fof(f54873,plain,(
% 167.34/40.33 greatest_lower_bound(sF2_fnc,multiply(sF2_fnc,sF1_fnc))=sF1_fnc),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f33,f54872])).
% 167.34/40.33 fof(f55047,plain,(
% 167.34/40.33 multiply(greatest_lower_bound(multiply(sF2_fnc,sF1_fnc),sF2_fnc),inverse(sF1_fnc))=identity),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f54873,f15858])).
% 167.34/40.33 fof(f55087,plain,(
% 167.34/40.33 greatest_lower_bound(sF2_fnc,multiply(sF2_fnc,inverse(sF1_fnc)))=identity),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f48734,f55047])).
% 167.34/40.33 fof(f73420,plain,(
% 167.34/40.33 greatest_lower_bound(multiply(sF5_fnc,sF3_fnc),sF0_fnc)=greatest_lower_bound(sF0_fnc,identity)),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f46002,f39505])).
% 167.34/40.33 fof(f73577,plain,(
% 167.34/40.33 greatest_lower_bound(sF0_fnc,multiply(sF5_fnc,sF3_fnc))=greatest_lower_bound(sF0_fnc,identity)),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f20,f73420])).
% 167.34/40.33 fof(f73578,plain,(
% 167.34/40.33 greatest_lower_bound(sF0_fnc,multiply(sF5_fnc,sF3_fnc))=greatest_lower_bound(identity,sF0_fnc)),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f20,f73577])).
% 167.34/40.33 fof(f73579,plain,(
% 167.34/40.33 greatest_lower_bound(sF0_fnc,multiply(sF5_fnc,sF3_fnc))=identity),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f46,f73578])).
% 167.34/40.33 fof(f79155,plain,(
% 167.34/40.33 multiply(inverse(sF2_fnc),identity)=greatest_lower_bound(identity,multiply(inverse(sF2_fnc),multiply(sF2_fnc,inverse(sF1_fnc))))),
% 167.34/40.33 inference(paramodulation,[status(thm)],[f55087,f865])).
% 167.34/40.33 fof(f79235,plain,(
% 167.34/40.33 inverse(sF2_fnc)=greatest_lower_bound(identity,multiply(inverse(sF2_fnc),multiply(sF2_fnc,inverse(sF1_fnc))))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f138,f79155])).
% 167.34/40.33 fof(f79239,plain,(
% 167.34/40.33 inverse(sF2_fnc)=greatest_lower_bound(identity,inverse(sF1_fnc))),
% 167.34/40.33 inference(forward_demodulation,[status(thm)],[f80,f79235])).
% 146.15/40.54 fof(f79309,plain,(
% 146.15/40.54 ![X0]: (multiply(inverse(sF2_fnc),X0)=greatest_lower_bound(X0,multiply(inverse(sF1_fnc),X0)))),
% 146.15/40.54 inference(paramodulation,[status(thm)],[f79239,f1612])).
% 146.15/40.54 fof(f92646,plain,(
% 146.15/40.54 multiply(inverse(sF5_fnc),identity)=greatest_lower_bound(multiply(inverse(sF5_fnc),sF0_fnc),sF3_fnc)),
% 146.15/40.54 inference(paramodulation,[status(thm)],[f73579,f886])).
% 146.15/40.54 fof(f92994,plain,(
% 146.15/40.54 inverse(sF5_fnc)=greatest_lower_bound(multiply(inverse(sF5_fnc),sF0_fnc),sF3_fnc)),
% 146.15/40.54 inference(forward_demodulation,[status(thm)],[f138,f92646])).
% 146.15/40.54 fof(f92995,plain,(
% 146.15/40.54 b=greatest_lower_bound(multiply(inverse(sF5_fnc),sF0_fnc),sF3_fnc)),
% 146.15/40.54 inference(forward_demodulation,[status(thm)],[f211,f92994])).
% 146.15/40.54 fof(f92996,plain,(
% 146.15/40.54 b=greatest_lower_bound(sF3_fnc,multiply(inverse(sF5_fnc),sF0_fnc))),
% 146.15/40.54 inference(forward_demodulation,[status(thm)],[f20,f92995])).
% 146.15/40.54 fof(f92997,plain,(
% 146.15/40.54 b=greatest_lower_bound(sF3_fnc,multiply(b,sF0_fnc))),
% 146.15/40.54 inference(forward_demodulation,[status(thm)],[f211,f92996])).
% 146.15/40.54 fof(f94106,plain,(
% 146.15/40.54 multiply(a,b)=greatest_lower_bound(sF2_fnc,multiply(a,multiply(b,sF0_fnc)))),
% 146.15/40.54 inference(paramodulation,[status(thm)],[f92997,f868])).
% 146.15/40.54 fof(f94155,plain,(
% 146.15/40.54 sF1_fnc=greatest_lower_bound(sF2_fnc,multiply(a,multiply(b,sF0_fnc)))),
% 146.15/40.54 inference(forward_demodulation,[status(thm)],[f33,f94106])).
% 146.15/40.54 fof(f94156,plain,(
% 146.15/40.54 sF1_fnc=greatest_lower_bound(sF2_fnc,multiply(sF1_fnc,sF0_fnc))),
% 146.15/40.54 inference(forward_demodulation,[status(thm)],[f75,f94155])).
% 146.15/40.54 fof(f94358,plain,(
% 146.15/40.54 greatest_lower_bound(sF0_fnc,sF1_fnc)=greatest_lower_bound(sF0_fnc,multiply(sF1_fnc,sF0_fnc))),
% 146.15/40.54 inference(paramodulation,[status(thm)],[f94156,f39515])).
% 146.15/40.54 fof(f94409,plain,(
% 146.15/40.54 sF1_fnc=greatest_lower_bound(sF0_fnc,multiply(sF1_fnc,sF0_fnc))),
% 146.15/40.54 inference(forward_demodulation,[status(thm)],[f106,f94358])).
% 146.15/40.54 fof(f94595,plain,(
% 146.15/40.54 multiply(inverse(sF1_fnc),sF1_fnc)=greatest_lower_bound(multiply(inverse(sF1_fnc),sF0_fnc),sF0_fnc)),
% 146.15/40.54 inference(paramodulation,[status(thm)],[f94409,f886])).
% 146.15/40.54 fof(f94642,plain,(
% 146.15/40.54 identity=greatest_lower_bound(multiply(inverse(sF1_fnc),sF0_fnc),sF0_fnc)),
% 146.15/40.54 inference(forward_demodulation,[status(thm)],[f18,f94595])).
% 146.15/40.54 fof(f94643,plain,(
% 146.15/40.54 identity=greatest_lower_bound(sF0_fnc,multiply(inverse(sF1_fnc),sF0_fnc))),
% 146.15/40.54 inference(forward_demodulation,[status(thm)],[f20,f94642])).
% 146.15/40.54 fof(f94645,plain,(
% 146.15/40.54 identity=multiply(inverse(sF2_fnc),sF0_fnc)),
% 146.15/40.54 inference(forward_demodulation,[status(thm)],[f79309,f94643])).
% 146.15/40.54 fof(f95156,plain,(
% 146.15/40.54 multiply(sF2_fnc,identity)=sF0_fnc),
% 146.15/40.54 inference(paramodulation,[status(thm)],[f94645,f616])).
% 146.15/40.54 fof(f95200,plain,(
% 146.15/40.54 sF2_fnc=sF0_fnc),
% 146.15/40.54 inference(forward_demodulation,[status(thm)],[f138,f95156])).
% 146.15/40.54 fof(f95201,plain,(
% 146.15/40.54 $false),
% 146.15/40.54 inference(forward_subsumption_resolution,[status(thm)],[f95200,f39])).
% 146.15/40.54 % SZS output end CNFRefutation for theBenchmark.p
% 173.10/41.11 % Elapsed time: 40.510303 seconds
% 173.10/41.11 % CPU time: 319.131641 seconds
% 173.10/41.11 % Total memory used: 58.481 GB
% 173.10/41.11 % Net memory used: 58.463 GB
%------------------------------------------------------------------------------