%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP167-2 : 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 : n005.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 109.41s 14.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP167-2 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n005.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 20:03:03 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 109.41/14.32 % Refutation found
% 109.41/14.32 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 109.41/14.32 % SZS output start CNFRefutation for theBenchmark
% 109.41/14.32 fof(f1,axiom,(
% 109.41/14.32 (![X]: (multiply(identity,X) = X ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f2,axiom,(
% 109.41/14.32 (![X]: (multiply(inverse(X),X) = identity ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f3,axiom,(
% 109.41/14.32 (![X,Y,Z]: (multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f4,axiom,(
% 109.41/14.32 (![X,Y]: (greatest_lower_bound(X,Y) = greatest_lower_bound(Y,X) ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f5,axiom,(
% 109.41/14.32 (![X,Y]: (least_upper_bound(X,Y) = least_upper_bound(Y,X) ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f7,axiom,(
% 109.41/14.32 (![X,Y,Z]: (least_upper_bound(X,least_upper_bound(Y,Z)) = least_upper_bound(least_upper_bound(X,Y),Z) ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f8,axiom,(
% 109.41/14.32 (![X]: (least_upper_bound(X,X) = X ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f10,axiom,(
% 109.41/14.32 (![X,Y]: (least_upper_bound(X,greatest_lower_bound(X,Y)) = X ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f11,axiom,(
% 109.41/14.32 (![X,Y]: (greatest_lower_bound(X,least_upper_bound(X,Y)) = X ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f12,axiom,(
% 109.41/14.32 (![X,Y,Z]: (multiply(X,least_upper_bound(Y,Z)) = least_upper_bound(multiply(X,Y),multiply(X,Z)) ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f13,axiom,(
% 109.41/14.32 (![X,Y,Z]: (multiply(X,greatest_lower_bound(Y,Z)) = greatest_lower_bound(multiply(X,Y),multiply(X,Z)) ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f14,axiom,(
% 109.41/14.32 (![Y,Z,X]: (multiply(least_upper_bound(Y,Z),X) = least_upper_bound(multiply(Y,X),multiply(Z,X)) ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f15,axiom,(
% 109.41/14.32 (![Y,Z,X]: (multiply(greatest_lower_bound(Y,Z),X) = greatest_lower_bound(multiply(Y,X),multiply(Z,X)) ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f16,axiom,(
% 109.41/14.32 inverse(identity) = identity ),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f17,axiom,(
% 109.41/14.32 (![X]: (inverse(inverse(X)) = X ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f19,axiom,(
% 109.41/14.32 (![X]: (positive_part(X) = least_upper_bound(X,identity) ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f20,axiom,(
% 109.41/14.32 (![X]: (negative_part(X) = greatest_lower_bound(X,identity) ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f21,axiom,(
% 109.41/14.32 (![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)) ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f22,axiom,(
% 109.41/14.32 (![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)) ))),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f23,negated_conjecture,(
% 109.41/14.32 a != multiply(positive_part(a),negative_part(a)) ),
% 109.41/14.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.41/14.32 fof(f24,plain,(
% 109.41/14.32 ![X0]: (multiply(identity,X0)=X0)),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f1])).
% 109.41/14.32 fof(f25,plain,(
% 109.41/14.32 ![X0]: (multiply(inverse(X0),X0)=identity)),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f2])).
% 109.41/14.32 fof(f26,plain,(
% 109.41/14.32 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,multiply(X1,X2)))),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f3])).
% 109.41/14.32 fof(f27,plain,(
% 109.41/14.32 ![X0,X1]: (greatest_lower_bound(X0,X1)=greatest_lower_bound(X1,X0))),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f4])).
% 109.41/14.32 fof(f28,plain,(
% 109.41/14.32 ![X0,X1]: (least_upper_bound(X0,X1)=least_upper_bound(X1,X0))),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f5])).
% 109.41/14.32 fof(f30,plain,(
% 109.41/14.32 ![X0,X1,X2]: (least_upper_bound(X0,least_upper_bound(X1,X2))=least_upper_bound(least_upper_bound(X0,X1),X2))),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f7])).
% 109.41/14.32 fof(f31,plain,(
% 109.41/14.32 ![X0]: (least_upper_bound(X0,X0)=X0)),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f8])).
% 109.41/14.32 fof(f33,plain,(
% 109.41/14.32 ![X0,X1]: (least_upper_bound(X0,greatest_lower_bound(X0,X1))=X0)),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f10])).
% 109.41/14.32 fof(f34,plain,(
% 109.41/14.32 ![X0,X1]: (greatest_lower_bound(X0,least_upper_bound(X0,X1))=X0)),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f11])).
% 109.41/14.32 fof(f35,plain,(
% 109.41/14.32 ![X0,X1,X2]: (multiply(X0,least_upper_bound(X1,X2))=least_upper_bound(multiply(X0,X1),multiply(X0,X2)))),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f12])).
% 109.41/14.32 fof(f36,plain,(
% 109.41/14.32 ![X0,X1,X2]: (multiply(X0,greatest_lower_bound(X1,X2))=greatest_lower_bound(multiply(X0,X1),multiply(X0,X2)))),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f13])).
% 109.41/14.32 fof(f37,plain,(
% 109.41/14.32 ![X0,X1,X2]: (multiply(least_upper_bound(X0,X1),X2)=least_upper_bound(multiply(X0,X2),multiply(X1,X2)))),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f14])).
% 109.41/14.32 fof(f38,plain,(
% 109.41/14.32 ![X0,X1,X2]: (multiply(greatest_lower_bound(X0,X1),X2)=greatest_lower_bound(multiply(X0,X2),multiply(X1,X2)))),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f15])).
% 109.41/14.32 fof(f39,plain,(
% 109.41/14.32 inverse(identity)=identity),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f16])).
% 109.41/14.32 fof(f40,plain,(
% 109.41/14.32 ![X0]: (inverse(inverse(X0))=X0)),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f17])).
% 109.41/14.32 fof(f42,plain,(
% 109.41/14.32 ![X0]: (positive_part(X0)=least_upper_bound(X0,identity))),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f19])).
% 109.41/14.32 fof(f43,plain,(
% 109.41/14.32 ![X0]: (negative_part(X0)=greatest_lower_bound(X0,identity))),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f20])).
% 109.41/14.32 fof(f44,plain,(
% 109.41/14.32 ![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)))),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f21])).
% 109.41/14.32 fof(f45,plain,(
% 109.41/14.32 ![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)))),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f22])).
% 109.41/14.32 fof(f46,plain,(
% 109.41/14.32 ~a=multiply(positive_part(a),negative_part(a))),
% 109.41/14.32 inference(cnf_transformation,[status(thm)],[f23])).
% 109.41/14.32 fof(f67,plain,(
% 109.41/14.32 ![X0,X1]: (multiply(identity,X0)=multiply(inverse(X1),multiply(X1,X0)))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f25,f26])).
% 109.41/14.32 fof(f68,plain,(
% 109.41/14.32 ![X0,X1]: (X0=multiply(inverse(X1),multiply(X1,X0)))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f24,f67])).
% 109.41/14.32 fof(f72,plain,(
% 109.41/14.32 ![X0]: (X0=multiply(inverse(inverse(X0)),identity))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f25,f68])).
% 109.41/14.32 fof(f74,plain,(
% 109.41/14.32 ![X0,X1,X2]: (X0=multiply(inverse(multiply(X1,X2)),multiply(X1,multiply(X2,X0))))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f26,f68])).
% 109.41/14.32 fof(f77,plain,(
% 109.41/14.32 ![X0]: (X0=multiply(X0,identity))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f40,f72])).
% 109.41/14.32 fof(f113,plain,(
% 109.41/14.32 ![X0,X1]: (X0=multiply(inverse(multiply(inverse(multiply(X1,X0)),X1)),identity))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f25,f74])).
% 109.41/14.32 fof(f142,plain,(
% 109.41/14.32 ![X0,X1]: (X0=inverse(multiply(inverse(multiply(X1,X0)),X1)))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f77,f113])).
% 109.41/14.32 fof(f159,plain,(
% 109.41/14.32 ![X0,X1]: (X0=inverse(multiply(X1,inverse(multiply(X0,X1)))))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f142,f142])).
% 109.41/14.32 fof(f307,plain,(
% 109.41/14.32 ![X0]: (negative_part(X0)=greatest_lower_bound(identity,X0))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f43,f27])).
% 109.41/14.32 fof(f314,plain,(
% 109.41/14.32 ![X0,X1]: (least_upper_bound(X0,greatest_lower_bound(X1,X0))=X0)),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f27,f33])).
% 109.41/14.32 fof(f319,plain,(
% 109.41/14.32 ![X0,X1]: (least_upper_bound(least_upper_bound(X0,X1),X0)=least_upper_bound(X0,X1))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f34,f314])).
% 109.41/14.32 fof(f320,plain,(
% 109.41/14.32 ![X0]: (least_upper_bound(identity,negative_part(X0))=identity)),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f43,f314])).
% 109.41/14.32 fof(f327,plain,(
% 109.41/14.32 ![X0,X1]: (least_upper_bound(X0,least_upper_bound(X1,X0))=least_upper_bound(X0,X1))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f30,f319])).
% 109.41/14.32 fof(f371,plain,(
% 109.41/14.32 ![X0]: (least_upper_bound(identity,positive_part(X0))=least_upper_bound(identity,X0))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f42,f327])).
% 109.41/14.32 fof(f384,plain,(
% 109.41/14.32 ![X0]: (least_upper_bound(positive_part(X0),least_upper_bound(identity,X0))=least_upper_bound(positive_part(X0),identity))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f371,f327])).
% 109.41/14.32 fof(f388,plain,(
% 109.41/14.32 ![X0]: (least_upper_bound(positive_part(X0),least_upper_bound(identity,X0))=positive_part(positive_part(X0)))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f42,f384])).
% 109.41/14.32 fof(f470,plain,(
% 109.41/14.32 ![X0,X1]: (inverse(X0)=multiply(X1,inverse(multiply(X0,X1))))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f159,f40])).
% 109.41/14.32 fof(f683,plain,(
% 109.41/14.32 ![X0]: (positive_part(X0)=least_upper_bound(identity,X0))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f42,f28])).
% 109.41/14.32 fof(f689,plain,(
% 109.41/14.32 ![X0]: (least_upper_bound(positive_part(X0),least_upper_bound(X0,identity))=positive_part(positive_part(X0)))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f28,f388])).
% 109.41/14.32 fof(f702,plain,(
% 109.41/14.32 ![X0]: (positive_part(negative_part(X0))=identity)),
% 109.41/14.32 inference(backward_demodulation,[status(thm)],[f683,f320])).
% 109.41/14.32 fof(f709,plain,(
% 109.41/14.32 ![X0]: (least_upper_bound(positive_part(X0),positive_part(X0))=positive_part(positive_part(X0)))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f42,f689])).
% 109.41/14.32 fof(f710,plain,(
% 109.41/14.32 ![X0]: (positive_part(X0)=positive_part(positive_part(X0)))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f31,f709])).
% 109.41/14.32 fof(f4634,plain,(
% 109.41/14.32 ![X0,X1]: (multiply(inverse(X0),least_upper_bound(X0,X1))=least_upper_bound(identity,multiply(inverse(X0),X1)))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f25,f35])).
% 109.41/14.32 fof(f4641,plain,(
% 109.41/14.32 ![X0,X1]: (multiply(X0,least_upper_bound(identity,X1))=least_upper_bound(X0,multiply(X0,X1)))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f77,f35])).
% 109.41/14.32 fof(f4673,plain,(
% 109.41/14.32 ![X0,X1]: (multiply(inverse(X0),least_upper_bound(X0,X1))=positive_part(multiply(inverse(X0),X1)))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f683,f4634])).
% 109.41/14.32 fof(f4679,plain,(
% 109.41/14.32 ![X0,X1]: (multiply(X0,positive_part(X1))=least_upper_bound(X0,multiply(X0,X1)))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f683,f4641])).
% 109.41/14.32 fof(f4727,plain,(
% 109.41/14.32 ![X0,X1]: (multiply(X0,greatest_lower_bound(identity,X1))=greatest_lower_bound(X0,multiply(X0,X1)))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f77,f36])).
% 109.41/14.32 fof(f4764,plain,(
% 109.41/14.32 ![X0,X1]: (multiply(X0,negative_part(X1))=greatest_lower_bound(X0,multiply(X0,X1)))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f307,f4727])).
% 109.41/14.32 fof(f4802,plain,(
% 109.41/14.32 ![X0,X1]: (multiply(least_upper_bound(identity,X0),X1)=least_upper_bound(X1,multiply(X0,X1)))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f24,f37])).
% 109.41/14.32 fof(f4843,plain,(
% 109.41/14.32 ![X0,X1]: (multiply(positive_part(X0),X1)=least_upper_bound(X1,multiply(X0,X1)))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f683,f4802])).
% 109.41/14.32 fof(f4891,plain,(
% 109.41/14.32 ![X0]: (multiply(inverse(X0),negative_part(X0))=greatest_lower_bound(inverse(X0),identity))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f25,f4764])).
% 109.41/14.32 fof(f4925,plain,(
% 109.41/14.32 ![X0]: (multiply(inverse(X0),negative_part(X0))=negative_part(inverse(X0)))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f43,f4891])).
% 109.41/14.32 fof(f5028,plain,(
% 109.41/14.32 ![X0]: (inverse(inverse(X0))=multiply(negative_part(X0),inverse(negative_part(inverse(X0)))))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f4925,f470])).
% 109.41/14.32 fof(f5062,plain,(
% 109.41/14.32 ![X0]: (X0=multiply(negative_part(X0),inverse(negative_part(inverse(X0)))))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f40,f5028])).
% 109.41/14.32 fof(f5208,plain,(
% 109.41/14.32 ![X0]: (multiply(inverse(X0),positive_part(X0))=positive_part(multiply(inverse(X0),identity)))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f42,f4673])).
% 109.41/14.32 fof(f5266,plain,(
% 109.41/14.32 ![X0]: (multiply(inverse(X0),positive_part(X0))=positive_part(inverse(X0)))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f77,f5208])).
% 109.41/14.32 fof(f6710,plain,(
% 109.41/14.32 ![X0]: (multiply(positive_part(X0),X0)=multiply(X0,positive_part(X0)))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f4679,f4843])).
% 109.41/14.32 fof(f6719,plain,(
% 109.41/14.32 ![X0]: (multiply(positive_part(inverse(X0)),negative_part(X0))=least_upper_bound(negative_part(X0),negative_part(inverse(X0))))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f4925,f4843])).
% 109.41/14.32 fof(f6722,plain,(
% 109.41/14.32 ![X0]: (multiply(positive_part(inverse(X0)),X0)=least_upper_bound(X0,identity))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f25,f4843])).
% 109.41/14.32 fof(f6785,plain,(
% 109.41/14.32 ![X0]: (multiply(positive_part(inverse(X0)),X0)=positive_part(X0))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f42,f6722])).
% 109.41/14.32 fof(f6857,plain,(
% 109.41/14.32 ![X0]: (multiply(positive_part(inverse(X0)),negative_part(X0))=greatest_lower_bound(positive_part(inverse(X0)),positive_part(X0)))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f6785,f4764])).
% 109.41/14.32 fof(f6882,plain,(
% 109.41/14.32 ![X0]: (least_upper_bound(negative_part(X0),negative_part(inverse(X0)))=greatest_lower_bound(positive_part(inverse(X0)),positive_part(X0)))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f6719,f6857])).
% 109.41/14.32 fof(f6883,plain,(
% 109.41/14.32 ![X0]: (least_upper_bound(negative_part(X0),negative_part(inverse(X0)))=greatest_lower_bound(positive_part(X0),positive_part(inverse(X0))))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f27,f6882])).
% 109.41/14.32 fof(f6914,plain,(
% 109.41/14.32 ![X0]: (multiply(positive_part(X0),negative_part(X0))=greatest_lower_bound(positive_part(X0),multiply(X0,positive_part(X0))))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f6710,f4764])).
% 109.41/14.32 fof(f8655,plain,(
% 109.41/14.32 ![X0,X1]: (multiply(greatest_lower_bound(identity,X0),X1)=greatest_lower_bound(X1,multiply(X0,X1)))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f24,f38])).
% 109.41/14.32 fof(f8724,plain,(
% 109.41/14.32 ![X0]: (multiply(positive_part(X0),negative_part(X0))=multiply(negative_part(X0),positive_part(X0)))),
% 109.41/14.32 inference(backward_demodulation,[status(thm)],[f8727,f6914])).
% 109.41/14.32 fof(f8727,plain,(
% 109.41/14.32 ![X0,X1]: (multiply(negative_part(X0),X1)=greatest_lower_bound(X1,multiply(X0,X1)))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f307,f8655])).
% 109.41/14.32 fof(f8791,plain,(
% 109.41/14.32 ~a=multiply(negative_part(a),positive_part(a))),
% 109.41/14.32 inference(backward_demodulation,[status(thm)],[f8724,f46])).
% 109.41/14.32 fof(f8807,plain,(
% 109.41/14.32 ![X0,X1]: (least_upper_bound(identity,greatest_lower_bound(X0,X1))=greatest_lower_bound(positive_part(X0),least_upper_bound(identity,X1)))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f683,f44])).
% 109.41/14.32 fof(f8914,plain,(
% 109.41/14.32 ![X0,X1]: (positive_part(greatest_lower_bound(X0,X1))=greatest_lower_bound(positive_part(X0),least_upper_bound(identity,X1)))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f683,f8807])).
% 109.41/14.32 fof(f8929,plain,(
% 109.41/14.32 ![X0]: (least_upper_bound(negative_part(X0),negative_part(inverse(X0)))=positive_part(greatest_lower_bound(X0,inverse(X0))))),
% 109.41/14.32 inference(backward_demodulation,[status(thm)],[f8936,f6883])).
% 109.41/14.32 fof(f8936,plain,(
% 109.41/14.32 ![X0,X1]: (positive_part(greatest_lower_bound(X0,X1))=greatest_lower_bound(positive_part(X0),positive_part(X1)))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f683,f8914])).
% 109.41/14.32 fof(f9135,plain,(
% 109.41/14.32 ![X0,X1]: (greatest_lower_bound(identity,least_upper_bound(X0,X1))=least_upper_bound(negative_part(X0),greatest_lower_bound(identity,X1)))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f307,f45])).
% 109.41/14.32 fof(f9226,plain,(
% 109.41/14.32 ![X0,X1]: (negative_part(least_upper_bound(X0,X1))=least_upper_bound(negative_part(X0),greatest_lower_bound(identity,X1)))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f307,f9135])).
% 109.41/14.32 fof(f9242,plain,(
% 109.41/14.32 ![X0]: (negative_part(least_upper_bound(X0,inverse(X0)))=positive_part(greatest_lower_bound(X0,inverse(X0))))),
% 109.41/14.32 inference(backward_demodulation,[status(thm)],[f9251,f8929])).
% 109.41/14.32 fof(f9251,plain,(
% 109.41/14.32 ![X0,X1]: (negative_part(least_upper_bound(X0,X1))=least_upper_bound(negative_part(X0),negative_part(X1)))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f307,f9226])).
% 109.41/14.32 fof(f10089,plain,(
% 109.41/14.32 ![X0]: (multiply(negative_part(inverse(X0)),positive_part(X0))=greatest_lower_bound(positive_part(X0),positive_part(inverse(X0))))),
% 109.41/14.32 inference(paramodulation,[status(thm)],[f5266,f8727])).
% 109.41/14.32 fof(f10165,plain,(
% 109.41/14.32 ![X0]: (multiply(negative_part(inverse(X0)),positive_part(X0))=positive_part(greatest_lower_bound(X0,inverse(X0))))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f8936,f10089])).
% 109.41/14.32 fof(f10166,plain,(
% 109.41/14.32 ![X0]: (multiply(negative_part(inverse(X0)),positive_part(X0))=negative_part(least_upper_bound(X0,inverse(X0))))),
% 109.41/14.32 inference(forward_demodulation,[status(thm)],[f9242,f10165])).
% 109.41/14.32 fof(f58040,plain,(
% 71.34/14.63 ![X0]: (positive_part(greatest_lower_bound(X0,inverse(X0)))=positive_part(negative_part(least_upper_bound(X0,inverse(X0)))))),
% 71.34/14.63 inference(paramodulation,[status(thm)],[f9242,f710])).
% 71.34/14.63 fof(f58193,plain,(
% 71.34/14.63 ![X0]: (negative_part(least_upper_bound(X0,inverse(X0)))=positive_part(negative_part(least_upper_bound(X0,inverse(X0)))))),
% 71.34/14.63 inference(forward_demodulation,[status(thm)],[f9242,f58040])).
% 71.34/14.63 fof(f58227,plain,(
% 71.34/14.63 ![X0]: (multiply(negative_part(inverse(X0)),positive_part(X0))=identity)),
% 71.34/14.63 inference(backward_demodulation,[status(thm)],[f58230,f10166])).
% 71.34/14.63 fof(f58230,plain,(
% 71.34/14.63 ![X0]: (negative_part(least_upper_bound(X0,inverse(X0)))=identity)),
% 71.34/14.63 inference(forward_demodulation,[status(thm)],[f702,f58193])).
% 71.34/14.63 fof(f58696,plain,(
% 71.34/14.63 ![X0]: (inverse(negative_part(inverse(X0)))=multiply(positive_part(X0),inverse(identity)))),
% 71.34/14.63 inference(paramodulation,[status(thm)],[f58227,f470])).
% 71.34/14.63 fof(f58860,plain,(
% 71.34/14.63 ![X0]: (inverse(negative_part(inverse(X0)))=multiply(positive_part(X0),identity))),
% 71.34/14.63 inference(forward_demodulation,[status(thm)],[f39,f58696])).
% 71.34/14.63 fof(f58869,plain,(
% 71.34/14.63 ![X0]: (X0=multiply(negative_part(X0),positive_part(X0)))),
% 71.34/14.63 inference(backward_demodulation,[status(thm)],[f59088,f5062])).
% 71.34/14.63 fof(f59088,plain,(
% 71.34/14.63 ![X0]: (inverse(negative_part(inverse(X0)))=positive_part(X0))),
% 71.34/14.63 inference(forward_demodulation,[status(thm)],[f77,f58860])).
% 71.34/14.63 fof(f60291,plain,(
% 71.34/14.63 ~a=a),
% 71.34/14.63 inference(backward_demodulation,[status(thm)],[f58869,f8791])).
% 71.34/14.63 fof(f62954,plain,(
% 71.34/14.63 $false),
% 71.34/14.63 inference(trivial_equality_resolution,[status(thm)],[f60291])).
% 71.34/14.63 % SZS output end CNFRefutation for theBenchmark.p
% 71.34/14.70 % Elapsed time: 14.334969 seconds
% 71.34/14.70 % CPU time: 112.992496 seconds
% 71.34/14.70 % Total memory used: 1.026 GB
% 71.34/14.70 % Net memory used: 1.009 GB
%------------------------------------------------------------------------------