%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP167-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:32:55 PM UTC 2026
% Result : Unsatisfiable 136.12s 32.85s
% Output : CNFRefutation 65.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 17
% Syntax : Number of formulae : 143 ( 143 unt; 0 def)
% Number of atoms : 143 ( 142 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-2 aty)
% Number of variables : 243 ( 243 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : multiply(identity,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X] : multiply(inverse(X),X) = identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y,Z] : multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] : greatest_lower_bound(X,Y) = greatest_lower_bound(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y] : least_upper_bound(X,Y) = least_upper_bound(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y,Z] : greatest_lower_bound(X,greatest_lower_bound(Y,Z)) = greatest_lower_bound(greatest_lower_bound(X,Y),Z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,Y] : least_upper_bound(X,greatest_lower_bound(X,Y)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,Y] : greatest_lower_bound(X,least_upper_bound(X,Y)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X,Y,Z] : multiply(X,least_upper_bound(Y,Z)) = least_upper_bound(multiply(X,Y),multiply(X,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X,Y,Z] : multiply(X,greatest_lower_bound(Y,Z)) = greatest_lower_bound(multiply(X,Y),multiply(X,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [Y,Z,X] : multiply(least_upper_bound(Y,Z),X) = least_upper_bound(multiply(Y,X),multiply(Z,X)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [Y,Z,X] : multiply(greatest_lower_bound(Y,Z),X) = greatest_lower_bound(multiply(Y,X),multiply(Z,X)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X] : positive_part(X) = least_upper_bound(X,identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [X] : negative_part(X) = greatest_lower_bound(X,identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [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)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [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)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
a != multiply(positive_part(a),negative_part(a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,plain,
! [X0] : multiply(identity,X0) = X0,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f22,plain,
! [X0] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f23,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f24,plain,
! [X0,X1] : greatest_lower_bound(X0,X1) = greatest_lower_bound(X1,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f25,plain,
! [X0,X1] : least_upper_bound(X0,X1) = least_upper_bound(X1,X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f26,plain,
! [X0,X1,X2] : greatest_lower_bound(X0,greatest_lower_bound(X1,X2)) = greatest_lower_bound(greatest_lower_bound(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f30,plain,
! [X0,X1] : least_upper_bound(X0,greatest_lower_bound(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f31,plain,
! [X0,X1] : greatest_lower_bound(X0,least_upper_bound(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f32,plain,
! [X0,X1,X2] : multiply(X0,least_upper_bound(X1,X2)) = least_upper_bound(multiply(X0,X1),multiply(X0,X2)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f33,plain,
! [X0,X1,X2] : multiply(X0,greatest_lower_bound(X1,X2)) = greatest_lower_bound(multiply(X0,X1),multiply(X0,X2)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f34,plain,
! [X0,X1,X2] : multiply(least_upper_bound(X0,X1),X2) = least_upper_bound(multiply(X0,X2),multiply(X1,X2)),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f35,plain,
! [X0,X1,X2] : multiply(greatest_lower_bound(X0,X1),X2) = greatest_lower_bound(multiply(X0,X2),multiply(X1,X2)),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f36,plain,
! [X0] : positive_part(X0) = least_upper_bound(X0,identity),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f37,plain,
! [X0] : negative_part(X0) = greatest_lower_bound(X0,identity),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f38,plain,
! [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)),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f39,plain,
! [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)),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f40,plain,
a != multiply(positive_part(a),negative_part(a)),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f66,plain,
! [X0,X1,X2,X3] : multiply(least_upper_bound(X0,multiply(X1,X2)),X3) = least_upper_bound(multiply(X0,X3),multiply(X1,multiply(X2,X3))),
inference(paramodulation,[status(thm)],[f23,f34]) ).
fof(f309,plain,
! [X0] : greatest_lower_bound(X0,positive_part(X0)) = X0,
inference(paramodulation,[status(thm)],[f36,f31]) ).
fof(f349,plain,
! [X0,X1] : multiply(greatest_lower_bound(X0,identity),X1) = greatest_lower_bound(multiply(X0,X1),X1),
inference(paramodulation,[status(thm)],[f21,f35]) ).
fof(f449,plain,
! [X0,X1] : multiply(negative_part(X0),X1) = greatest_lower_bound(multiply(X0,X1),X1),
inference(forward_demodulation,[status(thm)],[f37,f349]) ).
fof(f451,plain,
! [X0,X1] : multiply(negative_part(X0),X1) = greatest_lower_bound(X1,multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f24,f449]) ).
fof(f649,plain,
! [X0,X1] : multiply(negative_part(X0),multiply(X0,X1)) = multiply(X0,greatest_lower_bound(X1,multiply(X0,X1))),
inference(paramodulation,[status(thm)],[f33,f451]) ).
fof(f656,plain,
! [X0,X1] : multiply(negative_part(X0),multiply(X0,X1)) = multiply(X0,multiply(negative_part(X0),X1)),
inference(forward_demodulation,[status(thm)],[f451,f649]) ).
fof(f676,plain,
! [X0] : multiply(negative_part(inverse(X0)),X0) = greatest_lower_bound(X0,identity),
inference(paramodulation,[status(thm)],[f22,f451]) ).
fof(f693,plain,
! [X0,X1] : multiply(inverse(X0),greatest_lower_bound(X1,X0)) = greatest_lower_bound(multiply(inverse(X0),X1),identity),
inference(paramodulation,[status(thm)],[f22,f33]) ).
fof(f695,plain,
! [X0,X1] : multiply(inverse(X0),least_upper_bound(X1,X0)) = least_upper_bound(multiply(inverse(X0),X1),identity),
inference(paramodulation,[status(thm)],[f22,f32]) ).
fof(f697,plain,
! [X0,X1] : multiply(identity,X0) = multiply(inverse(X1),multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f22,f23]) ).
fof(f703,plain,
! [X0] : multiply(negative_part(inverse(X0)),X0) = negative_part(X0),
inference(forward_demodulation,[status(thm)],[f37,f676]) ).
fof(f716,plain,
! [X0,X1] : multiply(inverse(X0),greatest_lower_bound(X1,X0)) = negative_part(multiply(inverse(X0),X1)),
inference(forward_demodulation,[status(thm)],[f37,f693]) ).
fof(f717,plain,
! [X0,X1] : multiply(inverse(X0),least_upper_bound(X1,X0)) = positive_part(multiply(inverse(X0),X1)),
inference(forward_demodulation,[status(thm)],[f36,f695]) ).
fof(f718,plain,
! [X0,X1] : X0 = multiply(inverse(X1),multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f21,f697]) ).
fof(f723,plain,
! [X0] : negative_part(X0) = greatest_lower_bound(identity,X0),
inference(paramodulation,[status(thm)],[f37,f24]) ).
fof(f773,plain,
! [X0] : positive_part(X0) = least_upper_bound(identity,X0),
inference(paramodulation,[status(thm)],[f36,f25]) ).
fof(f869,plain,
! [X0,X1,X2] : greatest_lower_bound(X0,greatest_lower_bound(multiply(X1,X0),X2)) = greatest_lower_bound(multiply(negative_part(X1),X0),X2),
inference(paramodulation,[status(thm)],[f451,f26]) ).
fof(f872,plain,
! [X0,X1] : greatest_lower_bound(X0,greatest_lower_bound(identity,X1)) = greatest_lower_bound(negative_part(X0),X1),
inference(paramodulation,[status(thm)],[f37,f26]) ).
fof(f887,plain,
! [X0,X1] : greatest_lower_bound(X0,negative_part(X1)) = greatest_lower_bound(negative_part(X0),X1),
inference(forward_demodulation,[status(thm)],[f723,f872]) ).
fof(f894,plain,
! [X0] : positive_part(greatest_lower_bound(identity,X0)) = identity,
inference(paramodulation,[status(thm)],[f30,f773]) ).
fof(f905,plain,
! [X0] : greatest_lower_bound(identity,positive_part(X0)) = identity,
inference(paramodulation,[status(thm)],[f773,f31]) ).
fof(f908,plain,
! [X0] : positive_part(negative_part(X0)) = identity,
inference(forward_demodulation,[status(thm)],[f723,f894]) ).
fof(f910,plain,
! [X0] : negative_part(positive_part(X0)) = identity,
inference(forward_demodulation,[status(thm)],[f723,f905]) ).
fof(f912,plain,
! [X0] : greatest_lower_bound(negative_part(X0),identity) = negative_part(X0),
inference(paramodulation,[status(thm)],[f908,f309]) ).
fof(f913,plain,
! [X0] : negative_part(negative_part(X0)) = negative_part(X0),
inference(forward_demodulation,[status(thm)],[f37,f912]) ).
fof(f993,plain,
! [X0] : negative_part(multiply(X0,identity)) = multiply(negative_part(X0),identity),
inference(paramodulation,[status(thm)],[f451,f723]) ).
fof(f1062,plain,
! [X0,X1] : greatest_lower_bound(positive_part(X0),negative_part(X1)) = greatest_lower_bound(identity,X1),
inference(paramodulation,[status(thm)],[f910,f887]) ).
fof(f1080,plain,
! [X0,X1] : greatest_lower_bound(positive_part(X0),negative_part(X1)) = negative_part(X1),
inference(forward_demodulation,[status(thm)],[f723,f1062]) ).
fof(f1230,plain,
! [X0,X1] : multiply(inverse(negative_part(X0)),negative_part(X0)) = negative_part(multiply(inverse(negative_part(X0)),positive_part(X1))),
inference(paramodulation,[status(thm)],[f1080,f716]) ).
fof(f1232,plain,
! [X0] : multiply(inverse(X0),negative_part(X0)) = negative_part(multiply(inverse(X0),identity)),
inference(paramodulation,[status(thm)],[f723,f716]) ).
fof(f1268,plain,
! [X0,X1] : identity = negative_part(multiply(inverse(negative_part(X0)),positive_part(X1))),
inference(forward_demodulation,[status(thm)],[f22,f1230]) ).
fof(f1269,plain,
! [X0] : multiply(inverse(X0),negative_part(X0)) = multiply(negative_part(inverse(X0)),identity),
inference(forward_demodulation,[status(thm)],[f993,f1232]) ).
fof(f1675,plain,
! [X0,X1] : multiply(X0,X1) = multiply(inverse(inverse(X0)),X1),
inference(paramodulation,[status(thm)],[f718,f718]) ).
fof(f1677,plain,
! [X0] : X0 = multiply(inverse(inverse(X0)),identity),
inference(paramodulation,[status(thm)],[f22,f718]) ).
fof(f1686,plain,
! [X0,X1,X2] : multiply(least_upper_bound(X0,multiply(inverse(X1),X1)),X2) = least_upper_bound(multiply(X0,X2),X2),
inference(paramodulation,[status(thm)],[f718,f66]) ).
fof(f1713,plain,
! [X0] : multiply(inverse(X0),negative_part(X0)) = negative_part(inverse(X0)),
inference(backward_demodulation,[status(thm)],[f1731,f1269]) ).
fof(f1731,plain,
! [X0] : X0 = multiply(X0,identity),
inference(forward_demodulation,[status(thm)],[f1675,f1677]) ).
fof(f1747,plain,
! [X0,X1] : multiply(least_upper_bound(X0,identity),X1) = least_upper_bound(multiply(X0,X1),X1),
inference(forward_demodulation,[status(thm)],[f22,f1686]) ).
fof(f1748,plain,
! [X0,X1] : multiply(positive_part(X0),X1) = least_upper_bound(multiply(X0,X1),X1),
inference(forward_demodulation,[status(thm)],[f36,f1747]) ).
fof(f1750,plain,
! [X0,X1] : multiply(positive_part(X0),X1) = least_upper_bound(X1,multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f25,f1748]) ).
fof(f1829,plain,
! [X0,X1] : multiply(X0,greatest_lower_bound(X1,identity)) = greatest_lower_bound(multiply(X0,X1),X0),
inference(paramodulation,[status(thm)],[f1731,f33]) ).
fof(f1831,plain,
! [X0,X1] : multiply(X0,least_upper_bound(X1,identity)) = least_upper_bound(multiply(X0,X1),X0),
inference(paramodulation,[status(thm)],[f1731,f32]) ).
fof(f1861,plain,
! [X0,X1] : multiply(X0,negative_part(X1)) = greatest_lower_bound(multiply(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f37,f1829]) ).
fof(f1863,plain,
! [X0,X1] : multiply(X0,negative_part(X1)) = greatest_lower_bound(X0,multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f24,f1861]) ).
fof(f1865,plain,
! [X0,X1] : multiply(X0,positive_part(X1)) = least_upper_bound(multiply(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f36,f1831]) ).
fof(f1868,plain,
! [X0,X1] : multiply(X0,positive_part(X1)) = least_upper_bound(X0,multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f25,f1865]) ).
fof(f2007,plain,
! [X0,X1] : least_upper_bound(identity,greatest_lower_bound(X0,X1)) = greatest_lower_bound(positive_part(X0),least_upper_bound(identity,X1)),
inference(paramodulation,[status(thm)],[f773,f38]) ).
fof(f2021,plain,
! [X0,X1] : least_upper_bound(X0,greatest_lower_bound(identity,X1)) = greatest_lower_bound(positive_part(X0),least_upper_bound(X0,X1)),
inference(paramodulation,[status(thm)],[f36,f38]) ).
fof(f2059,plain,
! [X0,X1] : positive_part(greatest_lower_bound(X0,X1)) = greatest_lower_bound(positive_part(X0),least_upper_bound(identity,X1)),
inference(forward_demodulation,[status(thm)],[f773,f2007]) ).
fof(f2060,plain,
! [X0,X1] : positive_part(greatest_lower_bound(X0,X1)) = greatest_lower_bound(positive_part(X0),positive_part(X1)),
inference(forward_demodulation,[status(thm)],[f773,f2059]) ).
fof(f2076,plain,
! [X0,X1] : least_upper_bound(X0,negative_part(X1)) = greatest_lower_bound(positive_part(X0),least_upper_bound(X0,X1)),
inference(forward_demodulation,[status(thm)],[f723,f2021]) ).
fof(f2126,plain,
! [X0,X1] : greatest_lower_bound(identity,least_upper_bound(X0,X1)) = least_upper_bound(negative_part(X0),greatest_lower_bound(identity,X1)),
inference(paramodulation,[status(thm)],[f723,f39]) ).
fof(f2130,plain,
! [X0,X1,X2,X3] : greatest_lower_bound(multiply(X0,X1),least_upper_bound(multiply(X2,X1),X3)) = least_upper_bound(multiply(greatest_lower_bound(X0,X2),X1),greatest_lower_bound(multiply(X0,X1),X3)),
inference(paramodulation,[status(thm)],[f35,f39]) ).
fof(f2182,plain,
! [X0,X1] : negative_part(least_upper_bound(X0,X1)) = least_upper_bound(negative_part(X0),greatest_lower_bound(identity,X1)),
inference(forward_demodulation,[status(thm)],[f723,f2126]) ).
fof(f2184,plain,
! [X0,X1] : negative_part(least_upper_bound(X0,X1)) = least_upper_bound(negative_part(X0),negative_part(X1)),
inference(forward_demodulation,[status(thm)],[f723,f2182]) ).
fof(f2311,plain,
! [X0] : X0 = multiply(inverse(negative_part(inverse(X0))),negative_part(X0)),
inference(paramodulation,[status(thm)],[f703,f718]) ).
fof(f2455,plain,
! [X0] : multiply(inverse(X0),positive_part(X0)) = positive_part(multiply(inverse(X0),identity)),
inference(paramodulation,[status(thm)],[f773,f717]) ).
fof(f2501,plain,
! [X0] : multiply(inverse(X0),positive_part(X0)) = positive_part(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f1731,f2455]) ).
fof(f2529,plain,
! [X0] : multiply(inverse(negative_part(X0)),negative_part(X0)) = negative_part(inverse(negative_part(X0))),
inference(paramodulation,[status(thm)],[f913,f1713]) ).
fof(f2530,plain,
! [X0] : multiply(inverse(positive_part(X0)),identity) = negative_part(inverse(positive_part(X0))),
inference(paramodulation,[status(thm)],[f910,f1713]) ).
fof(f2532,plain,
! [X0] : negative_part(X0) = multiply(inverse(inverse(X0)),negative_part(inverse(X0))),
inference(paramodulation,[status(thm)],[f1713,f718]) ).
fof(f2561,plain,
! [X0] : identity = negative_part(inverse(negative_part(X0))),
inference(forward_demodulation,[status(thm)],[f22,f2529]) ).
fof(f2563,plain,
! [X0] : inverse(positive_part(X0)) = negative_part(inverse(positive_part(X0))),
inference(forward_demodulation,[status(thm)],[f1731,f2530]) ).
fof(f2566,plain,
! [X0] : negative_part(X0) = negative_part(inverse(inverse(X0))),
inference(forward_demodulation,[status(thm)],[f1713,f2532]) ).
fof(f3607,plain,
! [X0] : inverse(inverse(X0)) = multiply(inverse(negative_part(inverse(inverse(inverse(X0))))),negative_part(X0)),
inference(paramodulation,[status(thm)],[f2566,f2311]) ).
fof(f3643,plain,
! [X0] : inverse(inverse(X0)) = multiply(inverse(negative_part(inverse(X0))),negative_part(X0)),
inference(forward_demodulation,[status(thm)],[f2566,f3607]) ).
fof(f3654,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f2311,f3643]) ).
fof(f3879,plain,
! [X0] : multiply(X0,positive_part(inverse(X0))) = positive_part(inverse(inverse(X0))),
inference(paramodulation,[status(thm)],[f3654,f2501]) ).
fof(f3888,plain,
! [X0] : multiply(negative_part(inverse(X0)),positive_part(X0)) = greatest_lower_bound(positive_part(X0),positive_part(inverse(X0))),
inference(paramodulation,[status(thm)],[f2501,f451]) ).
fof(f3910,plain,
! [X0] : multiply(X0,positive_part(inverse(X0))) = positive_part(X0),
inference(forward_demodulation,[status(thm)],[f3654,f3879]) ).
fof(f3926,plain,
! [X0] : multiply(negative_part(inverse(X0)),positive_part(X0)) = positive_part(greatest_lower_bound(X0,inverse(X0))),
inference(forward_demodulation,[status(thm)],[f2060,f3888]) ).
fof(f5208,plain,
! [X0,X1] : identity = negative_part(multiply(inverse(inverse(positive_part(X0))),positive_part(X1))),
inference(paramodulation,[status(thm)],[f2563,f1268]) ).
fof(f5237,plain,
! [X0,X1] : identity = negative_part(multiply(positive_part(X0),positive_part(X1))),
inference(forward_demodulation,[status(thm)],[f3654,f5208]) ).
fof(f5483,plain,
! [X0,X1,X2] : greatest_lower_bound(positive_part(X0),greatest_lower_bound(positive_part(X1),X2)) = greatest_lower_bound(positive_part(greatest_lower_bound(X0,X1)),X2),
inference(paramodulation,[status(thm)],[f2060,f26]) ).
fof(f5622,plain,
! [X0,X1,X2] : negative_part(least_upper_bound(multiply(positive_part(X0),positive_part(X1)),X2)) = least_upper_bound(identity,negative_part(X2)),
inference(paramodulation,[status(thm)],[f5237,f2184]) ).
fof(f5658,plain,
! [X0,X1,X2] : negative_part(least_upper_bound(multiply(positive_part(X0),positive_part(X1)),X2)) = positive_part(negative_part(X2)),
inference(forward_demodulation,[status(thm)],[f773,f5622]) ).
fof(f5659,plain,
! [X0,X1,X2] : negative_part(least_upper_bound(multiply(positive_part(X0),positive_part(X1)),X2)) = identity,
inference(forward_demodulation,[status(thm)],[f908,f5658]) ).
fof(f6306,plain,
! [X0] : multiply(X0,negative_part(X0)) = multiply(negative_part(X0),X0),
inference(paramodulation,[status(thm)],[f451,f1863]) ).
fof(f6577,plain,
! [X0] : multiply(negative_part(X0),positive_part(X0)) = least_upper_bound(negative_part(X0),multiply(X0,negative_part(X0))),
inference(paramodulation,[status(thm)],[f6306,f1868]) ).
fof(f6586,plain,
! [X0] : multiply(inverse(negative_part(inverse(X0))),positive_part(negative_part(X0))) = least_upper_bound(inverse(negative_part(inverse(X0))),X0),
inference(paramodulation,[status(thm)],[f2311,f1868]) ).
fof(f6667,plain,
! [X0] : multiply(negative_part(X0),positive_part(X0)) = multiply(positive_part(X0),negative_part(X0)),
inference(forward_demodulation,[status(thm)],[f1750,f6577]) ).
fof(f6676,plain,
! [X0] : multiply(inverse(negative_part(inverse(X0))),identity) = least_upper_bound(inverse(negative_part(inverse(X0))),X0),
inference(forward_demodulation,[status(thm)],[f908,f6586]) ).
fof(f6677,plain,
! [X0] : inverse(negative_part(inverse(X0))) = least_upper_bound(inverse(negative_part(inverse(X0))),X0),
inference(forward_demodulation,[status(thm)],[f1731,f6676]) ).
fof(f6678,plain,
! [X0] : inverse(negative_part(inverse(X0))) = least_upper_bound(X0,inverse(negative_part(inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f25,f6677]) ).
fof(f16687,plain,
! [X0] : least_upper_bound(X0,negative_part(inverse(negative_part(inverse(X0))))) = greatest_lower_bound(positive_part(X0),inverse(negative_part(inverse(X0)))),
inference(paramodulation,[status(thm)],[f6678,f2076]) ).
fof(f16757,plain,
! [X0] : least_upper_bound(X0,identity) = greatest_lower_bound(positive_part(X0),inverse(negative_part(inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f2561,f16687]) ).
fof(f16758,plain,
! [X0] : positive_part(X0) = greatest_lower_bound(positive_part(X0),inverse(negative_part(inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f36,f16757]) ).
fof(f16810,plain,
! [X0] : multiply(inverse(inverse(negative_part(inverse(X0)))),positive_part(X0)) = negative_part(multiply(inverse(inverse(negative_part(inverse(X0)))),positive_part(X0))),
inference(paramodulation,[status(thm)],[f16758,f716]) ).
fof(f16882,plain,
! [X0] : multiply(negative_part(inverse(X0)),positive_part(X0)) = negative_part(multiply(inverse(inverse(negative_part(inverse(X0)))),positive_part(X0))),
inference(forward_demodulation,[status(thm)],[f3654,f16810]) ).
fof(f16883,plain,
! [X0] : positive_part(greatest_lower_bound(X0,inverse(X0))) = negative_part(multiply(inverse(inverse(negative_part(inverse(X0)))),positive_part(X0))),
inference(forward_demodulation,[status(thm)],[f3926,f16882]) ).
fof(f16884,plain,
! [X0] : positive_part(greatest_lower_bound(X0,inverse(X0))) = negative_part(multiply(negative_part(inverse(X0)),positive_part(X0))),
inference(forward_demodulation,[status(thm)],[f3654,f16883]) ).
fof(f16885,plain,
! [X0] : positive_part(greatest_lower_bound(X0,inverse(X0))) = negative_part(positive_part(greatest_lower_bound(X0,inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f3926,f16884]) ).
fof(f16889,plain,
! [X0] : positive_part(greatest_lower_bound(X0,inverse(X0))) = identity,
inference(forward_demodulation,[status(thm)],[f910,f16885]) ).
fof(f22781,plain,
! [X0,X1,X2] : greatest_lower_bound(multiply(X0,X1),least_upper_bound(multiply(positive_part(X0),X1),X2)) = least_upper_bound(multiply(X0,X1),greatest_lower_bound(multiply(X0,X1),X2)),
inference(paramodulation,[status(thm)],[f309,f2130]) ).
fof(f22983,plain,
! [X0,X1,X2] : greatest_lower_bound(multiply(X0,X1),least_upper_bound(multiply(positive_part(X0),X1),X2)) = multiply(X0,X1),
inference(forward_demodulation,[status(thm)],[f30,f22781]) ).
fof(f23272,plain,
! [X0] : multiply(negative_part(X0),positive_part(X0)) = multiply(X0,multiply(negative_part(X0),positive_part(inverse(X0)))),
inference(paramodulation,[status(thm)],[f3910,f656]) ).
fof(f23431,plain,
! [X0] : multiply(positive_part(X0),negative_part(X0)) = multiply(X0,multiply(negative_part(X0),positive_part(inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f6667,f23272]) ).
fof(f56198,plain,
! [X0,X1] : greatest_lower_bound(positive_part(X0),greatest_lower_bound(positive_part(inverse(X0)),X1)) = greatest_lower_bound(multiply(negative_part(inverse(X0)),positive_part(X0)),X1),
inference(paramodulation,[status(thm)],[f2501,f869]) ).
fof(f56481,plain,
! [X0,X1] : greatest_lower_bound(positive_part(greatest_lower_bound(X0,inverse(X0))),X1) = greatest_lower_bound(multiply(negative_part(inverse(X0)),positive_part(X0)),X1),
inference(forward_demodulation,[status(thm)],[f5483,f56198]) ).
fof(f56482,plain,
! [X0,X1] : greatest_lower_bound(identity,X0) = greatest_lower_bound(multiply(negative_part(inverse(X1)),positive_part(X1)),X0),
inference(forward_demodulation,[status(thm)],[f16889,f56481]) ).
fof(f56484,plain,
! [X0,X1] : negative_part(X0) = greatest_lower_bound(multiply(negative_part(inverse(X1)),positive_part(X1)),X0),
inference(forward_demodulation,[status(thm)],[f723,f56482]) ).
fof(f58076,plain,
! [X0,X1] : negative_part(least_upper_bound(multiply(positive_part(negative_part(inverse(X0))),positive_part(X0)),X1)) = multiply(negative_part(inverse(X0)),positive_part(X0)),
inference(paramodulation,[status(thm)],[f22983,f56484]) ).
fof(f58280,plain,
! [X0] : identity = multiply(negative_part(inverse(X0)),positive_part(X0)),
inference(forward_demodulation,[status(thm)],[f5659,f58076]) ).
fof(f58697,plain,
! [X0] : identity = multiply(negative_part(X0),positive_part(inverse(X0))),
inference(paramodulation,[status(thm)],[f3654,f58280]) ).
fof(f58801,plain,
! [X0] : multiply(positive_part(X0),negative_part(X0)) = multiply(X0,identity),
inference(backward_demodulation,[status(thm)],[f58697,f23431]) ).
fof(f59134,plain,
a != a,
inference(backward_demodulation,[status(thm)],[f59214,f40]) ).
fof(f59214,plain,
! [X0] : multiply(positive_part(X0),negative_part(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f1731,f58801]) ).
fof(f59336,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f59134]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP167-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.14/15.66 % CPULimit : 300
% 0.14/15.66 % WCLimit : 300
% 0.14/15.66 % DateTime : Sun Sep 20 20:04:18 UTC 2026
% 0.14/15.66 % CPUTime :
% 0.14/15.67 % Drodi V4.1.1
% 136.12/32.85 % Refutation found
% 136.12/32.85 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 136.12/32.85 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.20/34.29 % Elapsed time: 18.618056 seconds
% 6.20/34.29 % CPU time: 139.767058 seconds
% 6.20/34.29 % Total memory used: 959.269 MB
% 6.20/34.29 % Net memory used: 892.235 MB
%------------------------------------------------------------------------------