%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP170-4 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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:09 PM UTC 2026
% Result : Unsatisfiable 133.55s 35.16s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP170-4 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n018.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Sun Sep 20 20:05:49 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.38 % Drodi V4.1.1
% 133.55/35.16 % Refutation found
% 133.55/35.16 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 133.55/35.16 % SZS output start CNFRefutation for theBenchmark
% 133.55/35.16 fof(f1,axiom,(
% 133.55/35.16 (![X]: (multiply(identity,X) = X ))),
% 133.55/35.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 133.55/35.16 fof(f2,axiom,(
% 133.55/35.16 (![X]: (multiply(inverse(X),X) = identity ))),
% 133.55/35.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 133.55/35.16 fof(f3,axiom,(
% 133.55/35.16 (![X,Y,Z]: (multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ))),
% 133.55/35.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 133.55/35.16 fof(f4,axiom,(
% 133.55/35.16 (![X,Y]: (greatest_lower_bound(X,Y) = greatest_lower_bound(Y,X) ))),
% 133.55/35.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 133.55/35.16 fof(f5,axiom,(
% 133.55/35.16 (![X,Y]: (least_upper_bound(X,Y) = least_upper_bound(Y,X) ))),
% 133.55/35.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 133.55/35.16 fof(f7,axiom,(
% 133.55/35.16 (![X,Y,Z]: (least_upper_bound(X,least_upper_bound(Y,Z)) = least_upper_bound(least_upper_bound(X,Y),Z) ))),
% 133.55/35.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 133.55/35.16 fof(f8,axiom,(
% 133.55/35.17 (![X]: (least_upper_bound(X,X) = X ))),
% 133.55/35.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 133.55/35.17 fof(f10,axiom,(
% 133.55/35.17 (![X,Y]: (least_upper_bound(X,greatest_lower_bound(X,Y)) = X ))),
% 133.55/35.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 133.55/35.17 fof(f12,axiom,(
% 133.55/35.17 (![X,Y,Z]: (multiply(X,least_upper_bound(Y,Z)) = least_upper_bound(multiply(X,Y),multiply(X,Z)) ))),
% 133.55/35.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 133.55/35.17 fof(f14,axiom,(
% 133.55/35.17 (![Y,Z,X]: (multiply(least_upper_bound(Y,Z),X) = least_upper_bound(multiply(Y,X),multiply(Z,X)) ))),
% 133.55/35.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 133.55/35.17 fof(f16,hypothesis,(
% 133.55/35.17 least_upper_bound(a,b) = b ),
% 133.55/35.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 133.55/35.17 fof(f17,hypothesis,(
% 133.55/35.17 greatest_lower_bound(c,d) = c ),
% 133.55/35.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 133.55/35.17 fof(f18,negated_conjecture,(
% 133.55/35.17 least_upper_bound(multiply(a,c),multiply(b,d)) != multiply(b,d) ),
% 133.55/35.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 133.55/35.17 fof(f19,plain,(
% 133.55/35.17 ![X0]: (multiply(identity,X0)=X0)),
% 133.55/35.17 inference(cnf_transformation,[status(thm)],[f1])).
% 133.55/35.17 fof(f20,plain,(
% 133.55/35.17 ![X0]: (multiply(inverse(X0),X0)=identity)),
% 133.55/35.17 inference(cnf_transformation,[status(thm)],[f2])).
% 133.55/35.17 fof(f21,plain,(
% 133.55/35.17 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,multiply(X1,X2)))),
% 133.55/35.17 inference(cnf_transformation,[status(thm)],[f3])).
% 133.55/35.17 fof(f22,plain,(
% 133.55/35.17 ![X0,X1]: (greatest_lower_bound(X0,X1)=greatest_lower_bound(X1,X0))),
% 133.55/35.17 inference(cnf_transformation,[status(thm)],[f4])).
% 133.55/35.17 fof(f23,plain,(
% 133.55/35.17 ![X0,X1]: (least_upper_bound(X0,X1)=least_upper_bound(X1,X0))),
% 133.55/35.17 inference(cnf_transformation,[status(thm)],[f5])).
% 133.55/35.17 fof(f25,plain,(
% 133.55/35.17 ![X0,X1,X2]: (least_upper_bound(X0,least_upper_bound(X1,X2))=least_upper_bound(least_upper_bound(X0,X1),X2))),
% 133.55/35.17 inference(cnf_transformation,[status(thm)],[f7])).
% 133.55/35.17 fof(f26,plain,(
% 133.55/35.17 ![X0]: (least_upper_bound(X0,X0)=X0)),
% 133.55/35.17 inference(cnf_transformation,[status(thm)],[f8])).
% 133.55/35.17 fof(f28,plain,(
% 133.55/35.17 ![X0,X1]: (least_upper_bound(X0,greatest_lower_bound(X0,X1))=X0)),
% 133.55/35.17 inference(cnf_transformation,[status(thm)],[f10])).
% 133.55/35.17 fof(f30,plain,(
% 133.55/35.17 ![X0,X1,X2]: (multiply(X0,least_upper_bound(X1,X2))=least_upper_bound(multiply(X0,X1),multiply(X0,X2)))),
% 133.55/35.17 inference(cnf_transformation,[status(thm)],[f12])).
% 133.55/35.17 fof(f32,plain,(
% 133.55/35.17 ![X0,X1,X2]: (multiply(least_upper_bound(X0,X1),X2)=least_upper_bound(multiply(X0,X2),multiply(X1,X2)))),
% 133.55/35.17 inference(cnf_transformation,[status(thm)],[f14])).
% 133.55/35.17 fof(f34,plain,(
% 133.55/35.17 least_upper_bound(a,b)=b),
% 133.55/35.17 inference(cnf_transformation,[status(thm)],[f16])).
% 133.55/35.17 fof(f35,plain,(
% 133.55/35.17 greatest_lower_bound(c,d)=c),
% 133.55/35.17 inference(cnf_transformation,[status(thm)],[f17])).
% 133.55/35.17 fof(f36,plain,(
% 133.55/35.17 ~least_upper_bound(multiply(a,c),multiply(b,d))=multiply(b,d)),
% 133.55/35.17 inference(cnf_transformation,[status(thm)],[f18])).
% 133.55/35.17 fof(f37,definition,(
% 133.55/35.17 sF1_fnc=multiply(a,c)),
% 133.55/35.17 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 133.55/35.17 fof(f38,definition,(
% 133.55/35.17 sF2_fnc=multiply(b,d)),
% 133.55/35.17 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 133.55/35.17 fof(f39,definition,(
% 133.55/35.17 sF0_fnc=least_upper_bound(sF1_fnc,sF2_fnc)),
% 133.55/35.17 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 133.55/35.17 fof(f40,plain,(
% 133.55/35.17 ~sF0_fnc=sF2_fnc),
% 133.55/35.17 inference(definition_folding,[],[f36,f39,f38,f37])).
% 133.55/35.17 fof(f43,plain,(
% 133.55/35.17 ![X0]: (multiply(sF1_fnc,X0)=multiply(a,multiply(c,X0)))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f37,f21])).
% 133.55/35.17 fof(f50,plain,(
% 133.55/35.17 ![X0,X1]: (least_upper_bound(X0,least_upper_bound(X0,X1))=least_upper_bound(X0,X1))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f26,f25])).
% 133.55/35.17 fof(f79,plain,(
% 133.55/35.17 ![X0,X1]: (least_upper_bound(X0,least_upper_bound(X1,X0))=least_upper_bound(X0,X1))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f23,f50])).
% 133.55/35.17 fof(f85,plain,(
% 133.55/35.17 ![X0,X1,X2]: (multiply(X0,least_upper_bound(X1,X2))=least_upper_bound(multiply(X0,X2),multiply(X0,X1)))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f23,f30])).
% 133.55/35.17 fof(f89,plain,(
% 133.55/35.17 ![X0]: (multiply(b,least_upper_bound(d,X0))=least_upper_bound(sF2_fnc,multiply(b,X0)))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f38,f30])).
% 133.55/35.17 fof(f92,plain,(
% 133.55/35.17 ![X0]: (multiply(b,least_upper_bound(X0,d))=least_upper_bound(multiply(b,X0),sF2_fnc))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f38,f30])).
% 133.55/35.17 fof(f105,plain,(
% 133.55/35.17 ![X0]: (multiply(b,least_upper_bound(X0,d))=least_upper_bound(sF2_fnc,multiply(b,X0)))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f23,f92])).
% 133.55/35.17 fof(f114,plain,(
% 133.55/35.17 ![X0,X1]: (multiply(inverse(X0),least_upper_bound(X1,X0))=least_upper_bound(multiply(inverse(X0),X1),identity))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f20,f30])).
% 133.55/35.17 fof(f115,plain,(
% 133.55/35.17 ![X0,X1]: (multiply(inverse(X0),least_upper_bound(X0,X1))=least_upper_bound(identity,multiply(inverse(X0),X1)))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f20,f30])).
% 133.55/35.17 fof(f116,plain,(
% 133.55/35.17 ![X0,X1]: (multiply(identity,X0)=multiply(inverse(X1),multiply(X1,X0)))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f20,f21])).
% 133.55/35.17 fof(f117,plain,(
% 133.55/35.17 ![X0,X1]: (multiply(inverse(X0),least_upper_bound(X1,X0))=least_upper_bound(identity,multiply(inverse(X0),X1)))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f23,f114])).
% 133.55/35.17 fof(f118,plain,(
% 133.55/35.17 ![X0,X1]: (X0=multiply(inverse(X1),multiply(X1,X0)))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f19,f116])).
% 133.55/35.17 fof(f126,plain,(
% 133.55/35.17 ![X0,X1]: (multiply(X0,X1)=multiply(inverse(inverse(X0)),X1))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f118,f118])).
% 133.55/35.17 fof(f127,plain,(
% 133.55/35.17 ![X0]: (X0=multiply(inverse(inverse(X0)),identity))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f20,f118])).
% 133.55/35.17 fof(f129,plain,(
% 133.55/35.17 ![X0,X1,X2]: (X0=multiply(inverse(multiply(X1,X2)),multiply(X1,multiply(X2,X0))))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f21,f118])).
% 133.55/35.17 fof(f135,plain,(
% 133.55/35.17 ![X0]: (X0=multiply(X0,identity))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f126,f127])).
% 133.55/35.17 fof(f145,plain,(
% 133.55/35.17 ![X0,X1]: (multiply(X0,least_upper_bound(identity,X1))=least_upper_bound(X0,multiply(X0,X1)))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f135,f30])).
% 133.55/35.17 fof(f151,plain,(
% 133.55/35.17 ![X0,X1]: (least_upper_bound(X0,greatest_lower_bound(X1,X0))=X0)),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f22,f28])).
% 133.55/35.17 fof(f160,plain,(
% 133.55/35.17 least_upper_bound(d,c)=d),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f35,f151])).
% 133.55/35.17 fof(f168,plain,(
% 133.55/35.17 least_upper_bound(c,d)=d),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f23,f160])).
% 133.55/35.17 fof(f282,plain,(
% 133.55/35.17 ![X0,X1]: (multiply(X0,multiply(inverse(X0),X1))=X1)),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f118,f126])).
% 133.55/35.17 fof(f283,plain,(
% 133.55/35.17 ![X0]: (multiply(X0,inverse(X0))=identity)),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f20,f126])).
% 133.55/35.17 fof(f284,plain,(
% 133.55/35.17 ![X0]: (multiply(X0,identity)=inverse(inverse(X0)))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f135,f126])).
% 133.55/35.17 fof(f295,plain,(
% 133.55/35.17 ![X0]: (X0=inverse(inverse(X0)))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f135,f284])).
% 133.55/35.17 fof(f348,plain,(
% 133.55/35.17 ![X0,X1,X2]: (multiply(least_upper_bound(X0,X1),X2)=least_upper_bound(multiply(X1,X2),multiply(X0,X2)))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f23,f32])).
% 133.55/35.17 fof(f352,plain,(
% 133.55/35.17 ![X0,X1]: (multiply(least_upper_bound(inverse(X0),X1),X0)=least_upper_bound(identity,multiply(X1,X0)))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f20,f32])).
% 133.55/35.17 fof(f353,plain,(
% 133.55/35.17 ![X0,X1]: (multiply(least_upper_bound(identity,X0),X1)=least_upper_bound(X1,multiply(X0,X1)))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f19,f32])).
% 133.55/35.17 fof(f369,plain,(
% 133.55/35.17 ![X0,X1]: (multiply(least_upper_bound(X0,X1),inverse(X1))=least_upper_bound(multiply(X0,inverse(X1)),identity))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f283,f32])).
% 133.55/35.17 fof(f391,plain,(
% 133.55/35.17 ![X0,X1]: (multiply(least_upper_bound(X0,X1),inverse(X1))=least_upper_bound(identity,multiply(X0,inverse(X1))))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f23,f369])).
% 133.55/35.17 fof(f406,plain,(
% 133.55/35.17 ![X0]: (multiply(c,X0)=multiply(inverse(a),multiply(sF1_fnc,X0)))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f43,f118])).
% 133.55/35.17 fof(f883,plain,(
% 133.55/35.17 ![X0,X1]: (least_upper_bound(sF2_fnc,least_upper_bound(multiply(b,X0),X1))=least_upper_bound(multiply(b,least_upper_bound(d,X0)),X1))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f89,f25])).
% 133.55/35.17 fof(f1016,plain,(
% 133.55/35.17 ![X0]: (multiply(inverse(X0),least_upper_bound(identity,X0))=least_upper_bound(inverse(X0),identity))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f20,f145])).
% 133.55/35.17 fof(f1039,plain,(
% 133.55/35.17 ![X0]: (multiply(inverse(X0),least_upper_bound(identity,X0))=least_upper_bound(identity,inverse(X0)))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f23,f1016])).
% 133.55/35.17 fof(f3004,plain,(
% 133.55/35.17 ![X0,X1,X2]: (multiply(X0,least_upper_bound(X1,X2))=multiply(X0,least_upper_bound(X2,X1)))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f30,f85])).
% 133.55/35.17 fof(f4718,plain,(
% 133.55/35.17 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),multiply(X0,least_upper_bound(identity,X1)))=least_upper_bound(identity,multiply(inverse(multiply(X0,X1)),X0)))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f145,f117])).
% 133.55/35.17 fof(f8758,plain,(
% 133.55/35.17 ![X0,X1,X2,X3]: (X0=multiply(inverse(multiply(X1,least_upper_bound(X2,X3))),multiply(X1,multiply(least_upper_bound(X3,X2),X0))))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f3004,f129])).
% 133.55/35.17 fof(f8788,plain,(
% 133.55/35.17 ![X0,X1,X2]: (multiply(inverse(X0),X1)=multiply(inverse(multiply(X2,X0)),multiply(X2,X1)))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f282,f129])).
% 133.55/35.17 fof(f8861,plain,(
% 133.55/35.17 ![X0,X1,X2]: (X0=multiply(inverse(least_upper_bound(X1,X2)),multiply(least_upper_bound(X2,X1),X0)))),
% 133.55/35.17 inference(backward_demodulation,[status(thm)],[f8788,f8758])).
% 133.55/35.17 fof(f8866,plain,(
% 133.55/35.17 ![X0,X1]: (multiply(inverse(X0),least_upper_bound(identity,X0))=least_upper_bound(identity,multiply(inverse(multiply(X1,X0)),X1)))),
% 133.55/35.17 inference(backward_demodulation,[status(thm)],[f8788,f4718])).
% 133.55/35.17 fof(f8889,plain,(
% 133.55/35.17 ![X0,X1]: (least_upper_bound(identity,inverse(X0))=least_upper_bound(identity,multiply(inverse(multiply(X1,X0)),X1)))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f1039,f8866])).
% 133.55/35.17 fof(f8895,plain,(
% 133.55/35.17 ![X0,X1,X2]: (multiply(least_upper_bound(X0,X1),X2)=multiply(least_upper_bound(X1,X0),X2))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f32,f348])).
% 133.55/35.17 fof(f9290,plain,(
% 133.55/35.17 ![X0,X1]: (X0=multiply(inverse(least_upper_bound(inverse(X0),X1)),least_upper_bound(identity,multiply(X1,X0))))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f352,f118])).
% 133.55/35.17 fof(f10624,plain,(
% 133.55/35.17 ![X0,X1,X2,X3]: (multiply(inverse(least_upper_bound(X0,X1)),least_upper_bound(X2,multiply(least_upper_bound(X1,X0),X3)))=least_upper_bound(multiply(inverse(least_upper_bound(X0,X1)),X2),X3))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f8861,f30])).
% 133.55/35.17 fof(f31187,plain,(
% 133.55/35.17 ![X0,X1]: (X0=multiply(inverse(least_upper_bound(inverse(X0),X1)),least_upper_bound(identity,multiply(least_upper_bound(X1,inverse(X0)),X0))))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f79,f9290])).
% 133.55/35.17 fof(f31297,plain,(
% 133.55/35.17 ![X0,X1]: (X0=least_upper_bound(multiply(inverse(least_upper_bound(inverse(X0),X1)),identity),X0))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f10624,f31187])).
% 133.55/35.17 fof(f31298,plain,(
% 133.55/35.17 ![X0,X1]: (X0=least_upper_bound(X0,multiply(inverse(least_upper_bound(inverse(X0),X1)),identity)))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f23,f31297])).
% 133.55/35.17 fof(f31299,plain,(
% 133.55/35.17 ![X0,X1]: (X0=least_upper_bound(X0,inverse(least_upper_bound(inverse(X0),X1))))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f135,f31298])).
% 133.55/35.17 fof(f33553,plain,(
% 133.55/35.17 ![X0,X1]: (X0=least_upper_bound(X0,inverse(multiply(least_upper_bound(identity,X1),inverse(X0)))))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f353,f31299])).
% 133.55/35.17 fof(f33554,plain,(
% 133.55/35.17 ![X0,X1]: (X0=least_upper_bound(X0,inverse(multiply(inverse(X0),least_upper_bound(identity,X1)))))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f145,f31299])).
% 133.55/35.17 fof(f34056,plain,(
% 133.55/35.17 ![X0,X1,X2]: (X0=least_upper_bound(X0,inverse(multiply(multiply(inverse(X1),least_upper_bound(X1,X2)),inverse(X0)))))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f115,f33553])).
% 133.55/35.17 fof(f34172,plain,(
% 133.55/35.17 ![X0,X1,X2]: (X0=least_upper_bound(X0,inverse(multiply(inverse(X1),multiply(least_upper_bound(X1,X2),inverse(X0))))))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f21,f34056])).
% 133.55/35.17 fof(f35044,plain,(
% 133.55/35.17 ![X0,X1,X2]: (X0=least_upper_bound(X0,inverse(multiply(inverse(X0),multiply(least_upper_bound(X1,X2),inverse(X2))))))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f391,f33554])).
% 133.55/35.17 fof(f63772,plain,(
% 133.55/35.17 multiply(c,inverse(sF1_fnc))=multiply(inverse(a),identity)),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f283,f406])).
% 133.55/35.17 fof(f63842,plain,(
% 133.55/35.17 multiply(c,inverse(sF1_fnc))=inverse(a)),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f135,f63772])).
% 133.55/35.17 fof(f64477,plain,(
% 133.55/35.17 inverse(sF1_fnc)=multiply(inverse(c),inverse(a))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f63842,f118])).
% 133.55/35.17 fof(f103038,plain,(
% 133.55/35.17 ![X0]: (X0=least_upper_bound(X0,inverse(multiply(inverse(c),multiply(d,inverse(X0))))))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f168,f34172])).
% 133.55/35.17 fof(f105570,plain,(
% 133.55/35.17 ![X0]: (least_upper_bound(sF2_fnc,least_upper_bound(multiply(b,inverse(multiply(inverse(c),multiply(d,inverse(d))))),X0))=least_upper_bound(multiply(b,d),X0))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f103038,f883])).
% 133.55/35.17 fof(f105898,plain,(
% 133.55/35.17 ![X0]: (least_upper_bound(sF2_fnc,least_upper_bound(multiply(b,inverse(multiply(inverse(c),identity))),X0))=least_upper_bound(multiply(b,d),X0))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f283,f105570])).
% 133.55/35.17 fof(f105899,plain,(
% 133.55/35.17 ![X0]: (least_upper_bound(sF2_fnc,least_upper_bound(multiply(b,inverse(inverse(c))),X0))=least_upper_bound(multiply(b,d),X0))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f135,f105898])).
% 133.55/35.17 fof(f105900,plain,(
% 133.55/35.17 ![X0]: (least_upper_bound(sF2_fnc,least_upper_bound(multiply(b,c),X0))=least_upper_bound(multiply(b,d),X0))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f295,f105899])).
% 133.55/35.17 fof(f105902,plain,(
% 133.55/35.17 ![X0]: (least_upper_bound(sF2_fnc,least_upper_bound(multiply(b,c),X0))=least_upper_bound(sF2_fnc,X0))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f38,f105900])).
% 133.55/35.17 fof(f118065,plain,(
% 133.55/35.17 ![X0,X1,X2]: (multiply(inverse(X0),X0)=least_upper_bound(identity,multiply(inverse(multiply(inverse(inverse(X0)),multiply(least_upper_bound(X1,X2),inverse(X2)))),X0)))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f35044,f352])).
% 133.55/35.17 fof(f118446,plain,(
% 133.55/35.17 ![X0,X1,X2]: (identity=least_upper_bound(identity,multiply(inverse(multiply(inverse(inverse(X0)),multiply(least_upper_bound(X1,X2),inverse(X2)))),X0)))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f20,f118065])).
% 133.55/35.17 fof(f118447,plain,(
% 133.55/35.17 ![X0,X1,X2]: (identity=least_upper_bound(identity,multiply(inverse(multiply(X0,multiply(least_upper_bound(X1,X2),inverse(X2)))),X0)))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f295,f118446])).
% 133.55/35.17 fof(f118449,plain,(
% 133.55/35.17 ![X0,X1]: (identity=least_upper_bound(identity,inverse(multiply(least_upper_bound(X0,X1),inverse(X1)))))),
% 133.55/35.17 inference(forward_demodulation,[status(thm)],[f8889,f118447])).
% 133.55/35.17 fof(f127345,plain,(
% 133.55/35.17 ![X0,X1]: (identity=least_upper_bound(identity,inverse(multiply(least_upper_bound(X0,X1),inverse(X0)))))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f8895,f118449])).
% 133.55/35.17 fof(f128202,plain,(
% 133.55/35.17 identity=least_upper_bound(identity,inverse(multiply(b,inverse(a))))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f34,f127345])).
% 133.55/35.17 fof(f129188,plain,(
% 133.55/35.17 ![X0]: (X0=least_upper_bound(X0,inverse(multiply(inverse(X0),multiply(identity,inverse(inverse(multiply(b,inverse(a)))))))))),
% 133.55/35.17 inference(paramodulation,[status(thm)],[f128202,f35044])).
% 133.55/35.17 fof(f129355,plain,(
% 133.55/35.17 ![X0]: (X0=least_upper_bound(X0,inverse(multiply(inverse(X0),inverse(inverse(multiply(b,inverse(a))))))))),
% 134.89/35.31 inference(forward_demodulation,[status(thm)],[f19,f129188])).
% 134.89/35.31 fof(f129356,plain,(
% 134.89/35.31 ![X0]: (X0=least_upper_bound(X0,inverse(multiply(inverse(X0),multiply(b,inverse(a))))))),
% 134.89/35.31 inference(forward_demodulation,[status(thm)],[f295,f129355])).
% 134.89/35.31 fof(f130881,plain,(
% 134.89/35.31 least_upper_bound(sF2_fnc,multiply(b,c))=least_upper_bound(sF2_fnc,inverse(multiply(inverse(multiply(b,c)),multiply(b,inverse(a)))))),
% 134.89/35.31 inference(paramodulation,[status(thm)],[f129356,f105902])).
% 134.89/35.31 fof(f131141,plain,(
% 134.89/35.31 multiply(b,least_upper_bound(c,d))=least_upper_bound(sF2_fnc,inverse(multiply(inverse(multiply(b,c)),multiply(b,inverse(a)))))),
% 134.89/35.31 inference(forward_demodulation,[status(thm)],[f105,f130881])).
% 134.89/35.31 fof(f131142,plain,(
% 134.89/35.31 multiply(b,d)=least_upper_bound(sF2_fnc,inverse(multiply(inverse(multiply(b,c)),multiply(b,inverse(a)))))),
% 134.89/35.31 inference(forward_demodulation,[status(thm)],[f168,f131141])).
% 134.89/35.31 fof(f131143,plain,(
% 134.89/35.31 sF2_fnc=least_upper_bound(sF2_fnc,inverse(multiply(inverse(multiply(b,c)),multiply(b,inverse(a)))))),
% 134.89/35.31 inference(forward_demodulation,[status(thm)],[f38,f131142])).
% 134.89/35.31 fof(f131144,plain,(
% 134.89/35.31 sF2_fnc=least_upper_bound(sF2_fnc,inverse(multiply(inverse(c),inverse(a))))),
% 134.89/35.31 inference(forward_demodulation,[status(thm)],[f8788,f131143])).
% 134.89/35.31 fof(f131145,plain,(
% 134.89/35.31 sF2_fnc=least_upper_bound(sF2_fnc,inverse(inverse(sF1_fnc)))),
% 134.89/35.31 inference(forward_demodulation,[status(thm)],[f64477,f131144])).
% 134.89/35.31 fof(f131146,plain,(
% 134.89/35.31 sF2_fnc=least_upper_bound(sF2_fnc,sF1_fnc)),
% 134.89/35.31 inference(forward_demodulation,[status(thm)],[f295,f131145])).
% 134.89/35.31 fof(f131147,plain,(
% 134.89/35.31 sF2_fnc=least_upper_bound(sF1_fnc,sF2_fnc)),
% 134.89/35.31 inference(forward_demodulation,[status(thm)],[f23,f131146])).
% 134.89/35.31 fof(f131148,plain,(
% 134.89/35.31 sF2_fnc=sF0_fnc),
% 134.89/35.31 inference(forward_demodulation,[status(thm)],[f39,f131147])).
% 134.89/35.31 fof(f131149,plain,(
% 134.89/35.31 $false),
% 134.89/35.31 inference(forward_subsumption_resolution,[status(thm)],[f131148,f40])).
% 134.89/35.31 % SZS output end CNFRefutation for theBenchmark.p
% 110.38/35.91 % Elapsed time: 30.297620 seconds
% 110.38/35.91 % CPU time: 132.127700 seconds
% 110.38/35.91 % Total memory used: 2.670 GB
% 110.38/35.91 % Net memory used: 2.663 GB
%------------------------------------------------------------------------------