%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP167-1 : 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 : n015.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:08 PM UTC 2026
% Result : Unsatisfiable 62.07s 8.21s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP167-1 : 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/0.35 % Computer : n015.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 20:06:35 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 62.07/8.21 % Refutation found
% 62.07/8.21 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 62.07/8.21 % SZS output start CNFRefutation for theBenchmark
% 62.07/8.21 fof(f1,axiom,(
% 62.07/8.21 (![X]: (multiply(identity,X) = X ))),
% 62.07/8.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.07/8.21 fof(f2,axiom,(
% 62.07/8.21 (![X]: (multiply(inverse(X),X) = identity ))),
% 62.07/8.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.07/8.21 fof(f3,axiom,(
% 62.07/8.21 (![X,Y,Z]: (multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ))),
% 62.07/8.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.07/8.21 fof(f4,axiom,(
% 62.07/8.21 (![X,Y]: (greatest_lower_bound(X,Y) = greatest_lower_bound(Y,X) ))),
% 62.07/8.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.07/8.21 fof(f5,axiom,(
% 62.07/8.21 (![X,Y]: (least_upper_bound(X,Y) = least_upper_bound(Y,X) ))),
% 62.07/8.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.07/8.21 fof(f6,axiom,(
% 62.07/8.21 (![X,Y,Z]: (greatest_lower_bound(X,greatest_lower_bound(Y,Z)) = greatest_lower_bound(greatest_lower_bound(X,Y),Z) ))),
% 62.07/8.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.07/8.21 fof(f10,axiom,(
% 62.07/8.21 (![X,Y]: (least_upper_bound(X,greatest_lower_bound(X,Y)) = X ))),
% 62.07/8.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.07/8.21 fof(f11,axiom,(
% 62.07/8.21 (![X,Y]: (greatest_lower_bound(X,least_upper_bound(X,Y)) = X ))),
% 62.07/8.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.07/8.21 fof(f12,axiom,(
% 62.07/8.21 (![X,Y,Z]: (multiply(X,least_upper_bound(Y,Z)) = least_upper_bound(multiply(X,Y),multiply(X,Z)) ))),
% 62.07/8.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.07/8.21 fof(f13,axiom,(
% 62.07/8.21 (![X,Y,Z]: (multiply(X,greatest_lower_bound(Y,Z)) = greatest_lower_bound(multiply(X,Y),multiply(X,Z)) ))),
% 62.07/8.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.07/8.21 fof(f14,axiom,(
% 62.07/8.21 (![Y,Z,X]: (multiply(least_upper_bound(Y,Z),X) = least_upper_bound(multiply(Y,X),multiply(Z,X)) ))),
% 62.07/8.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.07/8.21 fof(f15,axiom,(
% 62.07/8.21 (![Y,Z,X]: (multiply(greatest_lower_bound(Y,Z),X) = greatest_lower_bound(multiply(Y,X),multiply(Z,X)) ))),
% 62.07/8.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.07/8.21 fof(f16,axiom,(
% 62.07/8.21 (![X]: (positive_part(X) = least_upper_bound(X,identity) ))),
% 62.07/8.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.07/8.21 fof(f17,axiom,(
% 62.07/8.21 (![X]: (negative_part(X) = greatest_lower_bound(X,identity) ))),
% 62.07/8.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.07/8.21 fof(f18,axiom,(
% 62.07/8.21 (![X,Y,Z]: (least_upper_bound(X,greatest_lower_bound(Y,Z)) = greatest_lower_bound(least_upper_bound(X,Y),least_upper_bound(X,Z)) ))),
% 62.07/8.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.07/8.21 fof(f19,axiom,(
% 62.07/8.21 (![X,Y,Z]: (greatest_lower_bound(X,least_upper_bound(Y,Z)) = least_upper_bound(greatest_lower_bound(X,Y),greatest_lower_bound(X,Z)) ))),
% 62.07/8.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.07/8.21 fof(f20,negated_conjecture,(
% 62.07/8.21 a != multiply(positive_part(a),negative_part(a)) ),
% 62.07/8.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.07/8.21 fof(f21,plain,(
% 62.07/8.21 ![X0]: (multiply(identity,X0)=X0)),
% 62.07/8.21 inference(cnf_transformation,[status(thm)],[f1])).
% 62.07/8.21 fof(f22,plain,(
% 62.07/8.21 ![X0]: (multiply(inverse(X0),X0)=identity)),
% 62.07/8.21 inference(cnf_transformation,[status(thm)],[f2])).
% 62.07/8.21 fof(f23,plain,(
% 62.07/8.21 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,multiply(X1,X2)))),
% 62.07/8.21 inference(cnf_transformation,[status(thm)],[f3])).
% 62.07/8.21 fof(f24,plain,(
% 62.07/8.21 ![X0,X1]: (greatest_lower_bound(X0,X1)=greatest_lower_bound(X1,X0))),
% 62.07/8.21 inference(cnf_transformation,[status(thm)],[f4])).
% 62.07/8.21 fof(f25,plain,(
% 62.07/8.21 ![X0,X1]: (least_upper_bound(X0,X1)=least_upper_bound(X1,X0))),
% 62.07/8.21 inference(cnf_transformation,[status(thm)],[f5])).
% 62.07/8.21 fof(f26,plain,(
% 62.07/8.21 ![X0,X1,X2]: (greatest_lower_bound(X0,greatest_lower_bound(X1,X2))=greatest_lower_bound(greatest_lower_bound(X0,X1),X2))),
% 62.07/8.21 inference(cnf_transformation,[status(thm)],[f6])).
% 62.07/8.21 fof(f30,plain,(
% 62.07/8.21 ![X0,X1]: (least_upper_bound(X0,greatest_lower_bound(X0,X1))=X0)),
% 62.07/8.21 inference(cnf_transformation,[status(thm)],[f10])).
% 62.07/8.21 fof(f31,plain,(
% 62.07/8.21 ![X0,X1]: (greatest_lower_bound(X0,least_upper_bound(X0,X1))=X0)),
% 62.07/8.21 inference(cnf_transformation,[status(thm)],[f11])).
% 62.07/8.21 fof(f32,plain,(
% 62.07/8.21 ![X0,X1,X2]: (multiply(X0,least_upper_bound(X1,X2))=least_upper_bound(multiply(X0,X1),multiply(X0,X2)))),
% 62.07/8.21 inference(cnf_transformation,[status(thm)],[f12])).
% 62.07/8.21 fof(f33,plain,(
% 62.07/8.21 ![X0,X1,X2]: (multiply(X0,greatest_lower_bound(X1,X2))=greatest_lower_bound(multiply(X0,X1),multiply(X0,X2)))),
% 62.07/8.21 inference(cnf_transformation,[status(thm)],[f13])).
% 62.07/8.21 fof(f34,plain,(
% 62.07/8.21 ![X0,X1,X2]: (multiply(least_upper_bound(X0,X1),X2)=least_upper_bound(multiply(X0,X2),multiply(X1,X2)))),
% 62.07/8.21 inference(cnf_transformation,[status(thm)],[f14])).
% 62.07/8.21 fof(f35,plain,(
% 62.07/8.21 ![X0,X1,X2]: (multiply(greatest_lower_bound(X0,X1),X2)=greatest_lower_bound(multiply(X0,X2),multiply(X1,X2)))),
% 62.07/8.21 inference(cnf_transformation,[status(thm)],[f15])).
% 62.07/8.21 fof(f36,plain,(
% 62.07/8.21 ![X0]: (positive_part(X0)=least_upper_bound(X0,identity))),
% 62.07/8.21 inference(cnf_transformation,[status(thm)],[f16])).
% 62.07/8.21 fof(f37,plain,(
% 62.07/8.21 ![X0]: (negative_part(X0)=greatest_lower_bound(X0,identity))),
% 62.07/8.21 inference(cnf_transformation,[status(thm)],[f17])).
% 62.07/8.21 fof(f38,plain,(
% 62.07/8.21 ![X0,X1,X2]: (least_upper_bound(X0,greatest_lower_bound(X1,X2))=greatest_lower_bound(least_upper_bound(X0,X1),least_upper_bound(X0,X2)))),
% 62.07/8.21 inference(cnf_transformation,[status(thm)],[f18])).
% 62.07/8.21 fof(f39,plain,(
% 62.07/8.21 ![X0,X1,X2]: (greatest_lower_bound(X0,least_upper_bound(X1,X2))=least_upper_bound(greatest_lower_bound(X0,X1),greatest_lower_bound(X0,X2)))),
% 62.07/8.21 inference(cnf_transformation,[status(thm)],[f19])).
% 62.07/8.21 fof(f40,plain,(
% 62.07/8.21 ~a=multiply(positive_part(a),negative_part(a))),
% 62.07/8.21 inference(cnf_transformation,[status(thm)],[f20])).
% 62.07/8.21 fof(f1010,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(greatest_lower_bound(X0,identity),X1)=greatest_lower_bound(multiply(X0,X1),X1))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f21,f35])).
% 62.07/8.21 fof(f1012,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(least_upper_bound(X0,identity),X1)=least_upper_bound(multiply(X0,X1),X1))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f21,f34])).
% 62.07/8.21 fof(f1470,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(negative_part(X0),X1)=greatest_lower_bound(multiply(X0,X1),X1))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f37,f1010])).
% 62.07/8.21 fof(f1472,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(negative_part(X0),X1)=greatest_lower_bound(X1,multiply(X0,X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f24,f1470])).
% 62.07/8.21 fof(f1474,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(positive_part(X0),X1)=least_upper_bound(multiply(X0,X1),X1))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f36,f1012])).
% 62.07/8.21 fof(f1476,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(positive_part(X0),X1)=least_upper_bound(X1,multiply(X0,X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f25,f1474])).
% 62.07/8.21 fof(f3164,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(greatest_lower_bound(X0,inverse(X1)),X1)=greatest_lower_bound(multiply(X0,X1),identity))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f22,f35])).
% 62.07/8.21 fof(f3168,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(inverse(X0),greatest_lower_bound(X1,X0))=greatest_lower_bound(multiply(inverse(X0),X1),identity))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f22,f33])).
% 62.07/8.21 fof(f3172,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(identity,X0)=multiply(inverse(X1),multiply(X1,X0)))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f22,f23])).
% 62.07/8.21 fof(f3185,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(greatest_lower_bound(X0,inverse(X1)),X1)=negative_part(multiply(X0,X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f37,f3164])).
% 62.07/8.21 fof(f3190,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(inverse(X0),greatest_lower_bound(X1,X0))=negative_part(multiply(inverse(X0),X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f37,f3168])).
% 62.07/8.21 fof(f3192,plain,(
% 62.07/8.21 ![X0,X1]: (X0=multiply(inverse(X1),multiply(X1,X0)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f21,f3172])).
% 62.07/8.21 fof(f3197,plain,(
% 62.07/8.21 ![X0]: (negative_part(X0)=greatest_lower_bound(identity,X0))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f37,f24])).
% 62.07/8.21 fof(f3247,plain,(
% 62.07/8.21 ![X0]: (positive_part(X0)=least_upper_bound(identity,X0))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f36,f25])).
% 62.07/8.21 fof(f3376,plain,(
% 62.07/8.21 ![X0]: (greatest_lower_bound(X0,positive_part(X0))=X0)),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f36,f31])).
% 62.07/8.21 fof(f3395,plain,(
% 62.07/8.21 ![X0]: (negative_part(least_upper_bound(identity,X0))=identity)),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f31,f3197])).
% 62.07/8.21 fof(f3403,plain,(
% 62.07/8.21 ![X0]: (least_upper_bound(identity,negative_part(X0))=identity)),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f3197,f30])).
% 62.07/8.21 fof(f3408,plain,(
% 62.07/8.21 ![X0]: (negative_part(positive_part(X0))=identity)),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3247,f3395])).
% 62.07/8.21 fof(f3410,plain,(
% 62.07/8.21 ![X0]: (positive_part(negative_part(X0))=identity)),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3247,f3403])).
% 62.07/8.21 fof(f3420,plain,(
% 62.07/8.21 ![X0]: (greatest_lower_bound(negative_part(X0),identity)=negative_part(X0))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f3410,f3376])).
% 62.07/8.21 fof(f3421,plain,(
% 62.07/8.21 ![X0]: (negative_part(negative_part(X0))=negative_part(X0))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f37,f3420])).
% 62.07/8.21 fof(f3424,plain,(
% 62.07/8.21 ![X0,X1]: (greatest_lower_bound(X0,greatest_lower_bound(X1,identity))=negative_part(greatest_lower_bound(X0,X1)))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f37,f26])).
% 62.07/8.21 fof(f3429,plain,(
% 62.07/8.21 ![X0,X1]: (greatest_lower_bound(identity,greatest_lower_bound(X0,X1))=greatest_lower_bound(negative_part(X0),X1))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f3197,f26])).
% 62.07/8.21 fof(f3450,plain,(
% 62.07/8.21 ![X0,X1]: (greatest_lower_bound(X0,negative_part(X1))=negative_part(greatest_lower_bound(X0,X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f37,f3424])).
% 62.07/8.21 fof(f3453,plain,(
% 62.07/8.21 ![X0,X1]: (negative_part(greatest_lower_bound(X0,X1))=greatest_lower_bound(negative_part(X0),X1))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3197,f3429])).
% 62.07/8.21 fof(f3454,plain,(
% 62.07/8.21 ![X0,X1]: (greatest_lower_bound(X0,negative_part(X1))=greatest_lower_bound(negative_part(X0),X1))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3450,f3453])).
% 62.07/8.21 fof(f3516,plain,(
% 62.07/8.21 ![X0,X1]: (least_upper_bound(X0,greatest_lower_bound(identity,X1))=greatest_lower_bound(positive_part(X0),least_upper_bound(X0,X1)))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f36,f38])).
% 62.07/8.21 fof(f3547,plain,(
% 62.07/8.21 ![X0,X1]: (least_upper_bound(X0,negative_part(X1))=greatest_lower_bound(positive_part(X0),least_upper_bound(X0,X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3197,f3516])).
% 62.07/8.21 fof(f3572,plain,(
% 62.07/8.21 ![X0,X1]: (least_upper_bound(identity,greatest_lower_bound(X0,X1))=greatest_lower_bound(least_upper_bound(identity,X0),positive_part(X1)))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f3247,f38])).
% 62.07/8.21 fof(f3581,plain,(
% 62.07/8.21 ![X0,X1]: (positive_part(greatest_lower_bound(X0,X1))=greatest_lower_bound(least_upper_bound(identity,X0),positive_part(X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3247,f3572])).
% 62.07/8.21 fof(f3582,plain,(
% 62.07/8.21 ![X0,X1]: (positive_part(greatest_lower_bound(X0,X1))=greatest_lower_bound(positive_part(X0),positive_part(X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3247,f3581])).
% 62.07/8.21 fof(f3600,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(X0,X1)=multiply(inverse(inverse(X0)),X1))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f3192,f3192])).
% 62.07/8.21 fof(f3601,plain,(
% 62.07/8.21 ![X0]: (X0=multiply(inverse(inverse(X0)),identity))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f22,f3192])).
% 62.07/8.21 fof(f3644,plain,(
% 62.07/8.21 ![X0]: (X0=multiply(X0,identity))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3600,f3601])).
% 62.07/8.21 fof(f3716,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(X0,greatest_lower_bound(X1,identity))=greatest_lower_bound(multiply(X0,X1),X0))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f3644,f33])).
% 62.07/8.21 fof(f3718,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(X0,least_upper_bound(X1,identity))=least_upper_bound(multiply(X0,X1),X0))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f3644,f32])).
% 62.07/8.21 fof(f3738,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(X0,negative_part(X1))=greatest_lower_bound(multiply(X0,X1),X0))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f37,f3716])).
% 62.07/8.21 fof(f3750,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(X0,negative_part(X1))=greatest_lower_bound(X0,multiply(X0,X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f24,f3738])).
% 62.07/8.21 fof(f3752,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(X0,positive_part(X1))=least_upper_bound(multiply(X0,X1),X0))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f36,f3718])).
% 62.07/8.21 fof(f3763,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(X0,positive_part(X1))=least_upper_bound(X0,multiply(X0,X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f25,f3752])).
% 62.07/8.21 fof(f3777,plain,(
% 62.07/8.21 ![X0]: (multiply(negative_part(inverse(X0)),X0)=greatest_lower_bound(X0,identity))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f22,f1472])).
% 62.07/8.21 fof(f3793,plain,(
% 62.07/8.21 ![X0]: (multiply(negative_part(inverse(X0)),X0)=negative_part(X0))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f37,f3777])).
% 62.07/8.21 fof(f3853,plain,(
% 62.07/8.21 ![X0]: (X0=multiply(inverse(negative_part(inverse(X0))),negative_part(X0)))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f3793,f3192])).
% 62.07/8.21 fof(f4126,plain,(
% 62.07/8.21 ![X0]: (multiply(X0,inverse(X0))=identity)),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f22,f3600])).
% 62.07/8.21 fof(f4127,plain,(
% 62.07/8.21 ![X0]: (multiply(X0,identity)=inverse(inverse(X0)))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f3644,f3600])).
% 62.07/8.21 fof(f4164,plain,(
% 62.07/8.21 ![X0]: (X0=inverse(inverse(X0)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3644,f4127])).
% 62.07/8.21 fof(f4210,plain,(
% 62.07/8.21 ![X0]: (multiply(positive_part(inverse(X0)),X0)=least_upper_bound(X0,identity))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f22,f1476])).
% 62.07/8.21 fof(f4231,plain,(
% 62.07/8.21 ![X0]: (multiply(positive_part(inverse(X0)),X0)=positive_part(X0))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f36,f4210])).
% 62.07/8.21 fof(f4319,plain,(
% 62.07/8.21 ![X0]: (multiply(negative_part(X0),inverse(X0))=negative_part(inverse(X0)))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f4164,f3793])).
% 62.07/8.21 fof(f4426,plain,(
% 62.07/8.21 ![X0]: (multiply(positive_part(X0),inverse(X0))=least_upper_bound(inverse(X0),identity))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f4126,f1476])).
% 62.07/8.21 fof(f4446,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(X0,greatest_lower_bound(inverse(X0),X1))=greatest_lower_bound(identity,multiply(X0,X1)))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f4126,f33])).
% 62.07/8.21 fof(f4450,plain,(
% 62.07/8.21 ![X0]: (multiply(positive_part(X0),inverse(X0))=positive_part(inverse(X0)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f36,f4426])).
% 62.07/8.21 fof(f4476,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(X0,greatest_lower_bound(inverse(X0),X1))=negative_part(multiply(X0,X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3197,f4446])).
% 62.07/8.21 fof(f4796,plain,(
% 62.07/8.21 ![X0]: (X0=multiply(inverse(positive_part(inverse(X0))),positive_part(X0)))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f4231,f3192])).
% 62.07/8.21 fof(f5187,plain,(
% 62.07/8.21 ![X0]: (multiply(X0,negative_part(X0))=multiply(negative_part(X0),X0))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f1472,f3750])).
% 62.07/8.21 fof(f5196,plain,(
% 62.07/8.21 ![X0]: (multiply(X0,negative_part(inverse(X0)))=greatest_lower_bound(X0,identity))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f4126,f3750])).
% 62.07/8.21 fof(f5239,plain,(
% 62.07/8.21 ![X0]: (multiply(X0,negative_part(inverse(X0)))=negative_part(X0))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f37,f5196])).
% 62.07/8.21 fof(f5273,plain,(
% 62.07/8.21 ![X0]: (multiply(positive_part(X0),negative_part(inverse(X0)))=least_upper_bound(negative_part(inverse(X0)),negative_part(X0)))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f5239,f1476])).
% 62.07/8.21 fof(f5292,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(X0,greatest_lower_bound(X1,negative_part(inverse(X0))))=greatest_lower_bound(multiply(X0,X1),negative_part(X0)))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f5239,f33])).
% 62.07/8.21 fof(f5293,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(X0,greatest_lower_bound(negative_part(inverse(X0)),X1))=greatest_lower_bound(negative_part(X0),multiply(X0,X1)))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f5239,f33])).
% 62.07/8.21 fof(f5302,plain,(
% 62.07/8.21 ![X0]: (multiply(positive_part(X0),negative_part(inverse(X0)))=least_upper_bound(negative_part(X0),negative_part(inverse(X0))))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f25,f5273])).
% 62.07/8.21 fof(f5316,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(X0,greatest_lower_bound(X1,negative_part(inverse(X0))))=greatest_lower_bound(negative_part(X0),multiply(X0,X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f24,f5292])).
% 62.07/8.21 fof(f5317,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(X0,greatest_lower_bound(X1,negative_part(inverse(X0))))=greatest_lower_bound(X0,negative_part(multiply(X0,X1))))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3454,f5316])).
% 62.07/8.21 fof(f5318,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(X0,greatest_lower_bound(inverse(X0),negative_part(X1)))=greatest_lower_bound(negative_part(X0),multiply(X0,X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3454,f5293])).
% 62.07/8.21 fof(f5319,plain,(
% 62.07/8.21 ![X0,X1]: (negative_part(multiply(X0,negative_part(X1)))=greatest_lower_bound(negative_part(X0),multiply(X0,X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f4476,f5318])).
% 62.07/8.21 fof(f5320,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(X0,greatest_lower_bound(X1,negative_part(inverse(X0))))=negative_part(multiply(X0,negative_part(X1))))),
% 62.07/8.21 inference(backward_demodulation,[status(thm)],[f5322,f5317])).
% 62.07/8.21 fof(f5322,plain,(
% 62.07/8.21 ![X0,X1]: (negative_part(multiply(X0,negative_part(X1)))=greatest_lower_bound(X0,negative_part(multiply(X0,X1))))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3454,f5319])).
% 62.07/8.21 fof(f5334,plain,(
% 62.07/8.21 ![X0,X1]: (greatest_lower_bound(identity,least_upper_bound(X0,X1))=least_upper_bound(negative_part(X0),greatest_lower_bound(identity,X1)))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f3197,f39])).
% 62.07/8.21 fof(f5398,plain,(
% 62.07/8.21 ![X0,X1]: (negative_part(least_upper_bound(X0,X1))=least_upper_bound(negative_part(X0),greatest_lower_bound(identity,X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3197,f5334])).
% 62.07/8.21 fof(f5399,plain,(
% 62.07/8.21 ![X0]: (multiply(positive_part(X0),negative_part(inverse(X0)))=negative_part(least_upper_bound(X0,inverse(X0))))),
% 62.07/8.21 inference(backward_demodulation,[status(thm)],[f5401,f5302])).
% 62.07/8.21 fof(f5401,plain,(
% 62.07/8.21 ![X0,X1]: (negative_part(least_upper_bound(X0,X1))=least_upper_bound(negative_part(X0),negative_part(X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3197,f5398])).
% 62.07/8.21 fof(f5728,plain,(
% 62.07/8.21 ![X0]: (multiply(negative_part(X0),positive_part(X0))=least_upper_bound(negative_part(X0),multiply(X0,negative_part(X0))))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f5187,f3763])).
% 62.07/8.21 fof(f5736,plain,(
% 62.07/8.21 ![X0]: (multiply(X0,positive_part(inverse(X0)))=least_upper_bound(X0,identity))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f4126,f3763])).
% 62.07/8.21 fof(f5806,plain,(
% 62.07/8.21 ![X0]: (multiply(negative_part(X0),positive_part(X0))=multiply(positive_part(X0),negative_part(X0)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f1476,f5728])).
% 62.07/8.21 fof(f5813,plain,(
% 62.07/8.21 ![X0]: (multiply(X0,positive_part(inverse(X0)))=positive_part(X0))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f36,f5736])).
% 62.07/8.21 fof(f5868,plain,(
% 62.07/8.21 ![X0]: (multiply(negative_part(X0),positive_part(inverse(X0)))=greatest_lower_bound(positive_part(inverse(X0)),positive_part(X0)))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f5813,f1472])).
% 62.07/8.21 fof(f5902,plain,(
% 62.07/8.21 ![X0]: (multiply(negative_part(X0),positive_part(inverse(X0)))=greatest_lower_bound(positive_part(X0),positive_part(inverse(X0))))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f24,f5868])).
% 62.07/8.21 fof(f5903,plain,(
% 62.07/8.21 ![X0]: (multiply(negative_part(X0),positive_part(inverse(X0)))=positive_part(greatest_lower_bound(X0,inverse(X0))))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3582,f5902])).
% 62.07/8.21 fof(f6018,plain,(
% 62.07/8.21 ![X0]: (positive_part(X0)=multiply(inverse(negative_part(inverse(positive_part(X0)))),identity))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f3408,f3853])).
% 62.07/8.21 fof(f6021,plain,(
% 62.07/8.21 ![X0]: (multiply(inverse(negative_part(inverse(X0))),positive_part(negative_part(X0)))=least_upper_bound(inverse(negative_part(inverse(X0))),X0))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f3853,f3763])).
% 62.07/8.21 fof(f6047,plain,(
% 62.07/8.21 ![X0]: (positive_part(X0)=inverse(negative_part(inverse(positive_part(X0)))))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3644,f6018])).
% 62.07/8.21 fof(f6051,plain,(
% 62.07/8.21 ![X0]: (multiply(inverse(negative_part(inverse(X0))),identity)=least_upper_bound(inverse(negative_part(inverse(X0))),X0))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3410,f6021])).
% 62.07/8.21 fof(f6052,plain,(
% 62.07/8.21 ![X0]: (inverse(negative_part(inverse(X0)))=least_upper_bound(inverse(negative_part(inverse(X0))),X0))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f3644,f6051])).
% 62.07/8.21 fof(f6053,plain,(
% 62.07/8.21 ![X0]: (inverse(negative_part(inverse(X0)))=least_upper_bound(X0,inverse(negative_part(inverse(X0)))))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f25,f6052])).
% 62.07/8.21 fof(f6171,plain,(
% 62.07/8.21 ![X0,X1]: (multiply(positive_part(X0),greatest_lower_bound(X1,negative_part(inverse(positive_part(X0)))))=negative_part(multiply(inverse(negative_part(inverse(positive_part(X0)))),X1)))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f6047,f3190])).
% 62.07/8.21 fof(f6199,plain,(
% 62.07/8.21 ![X0,X1]: (negative_part(multiply(positive_part(X0),negative_part(X1)))=negative_part(multiply(inverse(negative_part(inverse(positive_part(X0)))),X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f5320,f6171])).
% 62.07/8.21 fof(f6200,plain,(
% 62.07/8.21 ![X0,X1]: (negative_part(multiply(positive_part(X0),negative_part(X1)))=negative_part(multiply(positive_part(X0),X1)))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f6047,f6199])).
% 62.07/8.21 fof(f6295,plain,(
% 62.07/8.21 ![X0]: (multiply(negative_part(X0),inverse(negative_part(X0)))=negative_part(inverse(negative_part(X0))))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f3421,f4319])).
% 62.07/8.21 fof(f6300,plain,(
% 62.07/8.21 ![X0]: (multiply(negative_part(X0),positive_part(inverse(X0)))=least_upper_bound(negative_part(X0),negative_part(inverse(X0))))),
% 62.07/8.21 inference(paramodulation,[status(thm)],[f4319,f3763])).
% 62.07/8.21 fof(f6330,plain,(
% 62.07/8.21 ![X0]: (identity=negative_part(inverse(negative_part(X0))))),
% 62.07/8.21 inference(forward_demodulation,[status(thm)],[f4126,f6295])).
% 62.07/8.22 fof(f6340,plain,(
% 62.07/8.22 ![X0]: (positive_part(greatest_lower_bound(X0,inverse(X0)))=least_upper_bound(negative_part(X0),negative_part(inverse(X0))))),
% 62.07/8.22 inference(forward_demodulation,[status(thm)],[f5903,f6300])).
% 62.07/8.22 fof(f6342,plain,(
% 62.07/8.22 ![X0]: (multiply(positive_part(X0),negative_part(inverse(X0)))=positive_part(greatest_lower_bound(X0,inverse(X0))))),
% 62.07/8.22 inference(backward_demodulation,[status(thm)],[f6343,f5399])).
% 62.07/8.22 fof(f6343,plain,(
% 62.07/8.22 ![X0]: (positive_part(greatest_lower_bound(X0,inverse(X0)))=negative_part(least_upper_bound(X0,inverse(X0))))),
% 62.07/8.22 inference(forward_demodulation,[status(thm)],[f5401,f6340])).
% 62.07/8.22 fof(f31562,plain,(
% 62.07/8.22 ![X0]: (least_upper_bound(X0,negative_part(inverse(negative_part(inverse(X0)))))=greatest_lower_bound(positive_part(X0),inverse(negative_part(inverse(X0)))))),
% 62.07/8.22 inference(paramodulation,[status(thm)],[f6053,f3547])).
% 62.07/8.22 fof(f31761,plain,(
% 62.07/8.22 ![X0]: (least_upper_bound(X0,identity)=greatest_lower_bound(positive_part(X0),inverse(negative_part(inverse(X0)))))),
% 62.07/8.22 inference(forward_demodulation,[status(thm)],[f6330,f31562])).
% 62.07/8.22 fof(f31762,plain,(
% 62.07/8.22 ![X0]: (positive_part(X0)=greatest_lower_bound(positive_part(X0),inverse(negative_part(inverse(X0)))))),
% 62.07/8.22 inference(forward_demodulation,[status(thm)],[f36,f31761])).
% 62.07/8.22 fof(f32466,plain,(
% 62.07/8.22 ![X0]: (multiply(positive_part(X0),negative_part(inverse(X0)))=negative_part(multiply(positive_part(X0),negative_part(inverse(X0)))))),
% 62.07/8.22 inference(paramodulation,[status(thm)],[f31762,f3185])).
% 62.07/8.22 fof(f32550,plain,(
% 62.07/8.22 ![X0]: (positive_part(greatest_lower_bound(X0,inverse(X0)))=negative_part(multiply(positive_part(X0),negative_part(inverse(X0)))))),
% 62.07/8.22 inference(forward_demodulation,[status(thm)],[f6342,f32466])).
% 62.07/8.22 fof(f32551,plain,(
% 62.07/8.22 ![X0]: (positive_part(greatest_lower_bound(X0,inverse(X0)))=negative_part(multiply(positive_part(X0),inverse(X0))))),
% 62.07/8.22 inference(forward_demodulation,[status(thm)],[f6200,f32550])).
% 62.07/8.22 fof(f32552,plain,(
% 62.07/8.22 ![X0]: (positive_part(greatest_lower_bound(X0,inverse(X0)))=negative_part(positive_part(inverse(X0))))),
% 62.07/8.22 inference(forward_demodulation,[status(thm)],[f4450,f32551])).
% 62.07/8.22 fof(f32553,plain,(
% 62.07/8.22 ![X0]: (multiply(positive_part(X0),negative_part(inverse(X0)))=identity)),
% 62.07/8.22 inference(backward_demodulation,[status(thm)],[f32558,f6342])).
% 62.07/8.22 fof(f32558,plain,(
% 62.07/8.22 ![X0]: (positive_part(greatest_lower_bound(X0,inverse(X0)))=identity)),
% 62.07/8.22 inference(forward_demodulation,[status(thm)],[f3408,f32552])).
% 62.07/8.22 fof(f32667,plain,(
% 62.07/8.22 ![X0]: (negative_part(inverse(X0))=multiply(inverse(positive_part(X0)),identity))),
% 62.07/8.22 inference(paramodulation,[status(thm)],[f32553,f3192])).
% 62.07/8.22 fof(f32786,plain,(
% 62.07/8.22 ![X0]: (X0=multiply(negative_part(inverse(inverse(X0))),positive_part(X0)))),
% 62.07/8.22 inference(backward_demodulation,[status(thm)],[f33041,f4796])).
% 62.07/8.22 fof(f33041,plain,(
% 62.07/8.22 ![X0]: (negative_part(inverse(X0))=inverse(positive_part(X0)))),
% 62.07/8.22 inference(forward_demodulation,[status(thm)],[f3644,f32667])).
% 62.07/8.22 fof(f33080,plain,(
% 62.07/8.22 ![X0]: (X0=multiply(positive_part(X0),negative_part(X0)))),
% 62.07/8.22 inference(backward_demodulation,[status(thm)],[f33081,f5806])).
% 62.07/8.22 fof(f33081,plain,(
% 62.07/8.22 ![X0]: (X0=multiply(negative_part(X0),positive_part(X0)))),
% 58.93/8.32 inference(forward_demodulation,[status(thm)],[f4164,f32786])).
% 58.93/8.32 fof(f33584,plain,(
% 58.93/8.32 ~a=a),
% 58.93/8.32 inference(backward_demodulation,[status(thm)],[f33080,f40])).
% 58.93/8.32 fof(f33702,plain,(
% 58.93/8.32 $false),
% 58.93/8.32 inference(trivial_equality_resolution,[status(thm)],[f33584])).
% 58.93/8.32 % SZS output end CNFRefutation for theBenchmark.p
% 4.10/8.41 % Elapsed time: 8.043626 seconds
% 4.10/8.41 % CPU time: 63.566345 seconds
% 4.10/8.41 % Total memory used: 775.267 MB
% 4.10/8.41 % Net memory used: 762.297 MB
%------------------------------------------------------------------------------