%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP184-4 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n002.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 : Fri Sep 25 01:25:36 PM UTC 2026
% Result : Unsatisfiable 9.83s 2.14s
% Output : CNFRefutation 9.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 16
% Syntax : Number of clauses : 99 ( 99 unt; 0 nHn; 52 RR)
% Number of literals : 99 ( 98 equ; 10 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 79 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t8,axiom,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t115,plain,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t20,axiom,
sFlat0 = least_upper_bound(a,identity),
introduced(definition) ).
cnf(t2196,plain,
sFlat0 = least_upper_bound(identity,a),
inference(step,[status(thm)],[t20,t115]) ).
cnf(t134,plain,
least_upper_bound(identity,a) = sFlat0,
inference(orient,[status(thm)],[t2196]) ).
cnf(t11,axiom,
least_upper_bound(inverse(X1),inverse(X2)) = inverse(greatest_lower_bound(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t129,plain,
least_upper_bound(inverse(X1),inverse(X2)) = inverse(greatest_lower_bound(X1,X2)),
inference(orient,[status(thm)],[t11]) ).
cnf(t0,axiom,
inverse(identity) = identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t146,plain,
inverse(identity) = identity,
inference(orient,[status(thm)],[t0]) ).
cnf(t148,plain,
inverse(greatest_lower_bound(X1,identity)) = least_upper_bound(inverse(X1),identity),
inference(cp,[status(thm)],[t129,t146]) ).
cnf(t2215,plain,
inverse(greatest_lower_bound(X1,identity)) = least_upper_bound(identity,inverse(X1)),
inference(step,[status(thm)],[t148,t115]) ).
cnf(t369,plain,
inverse(greatest_lower_bound(X1,identity)) = least_upper_bound(identity,inverse(X1)),
inference(orient,[status(thm)],[t2215]) ).
cnf(t147,plain,
inverse(greatest_lower_bound(identity,X1)) = least_upper_bound(identity,inverse(X1)),
inference(cp,[status(thm)],[t129,t146]) ).
cnf(t351,plain,
inverse(greatest_lower_bound(identity,X1)) = least_upper_bound(identity,inverse(X1)),
inference(orient,[status(thm)],[t147]) ).
cnf(t21,axiom,
sFlat1 = greatest_lower_bound(a,identity),
introduced(definition) ).
cnf(t6,axiom,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t90,plain,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t2195,plain,
sFlat1 = greatest_lower_bound(identity,a),
inference(step,[status(thm)],[t21,t90]) ).
cnf(t112,plain,
greatest_lower_bound(identity,a) = sFlat1,
inference(orient,[status(thm)],[t2195]) ).
cnf(t353,plain,
least_upper_bound(identity,inverse(a)) = inverse(sFlat1),
inference(cp,[status(thm)],[t351,t112]) ).
cnf(t22,axiom,
sFlat2 = inverse(greatest_lower_bound(a,identity)),
introduced(definition) ).
cnf(t2197,plain,
sFlat2 = inverse(greatest_lower_bound(identity,a)),
inference(step,[status(thm)],[t22,t90]) ).
cnf(t2198,plain,
sFlat2 = inverse(sFlat1),
inference(step,[status(thm)],[t2197,t112]) ).
cnf(t137,plain,
inverse(sFlat1) = sFlat2,
inference(orient,[status(thm)],[t2198]) ).
cnf(t2214,plain,
least_upper_bound(identity,inverse(a)) = sFlat2,
inference(step,[status(thm)],[t353,t137]) ).
cnf(t365,plain,
least_upper_bound(identity,inverse(a)) = sFlat2,
inference(orient,[status(thm)],[t2214]) ).
cnf(t12,axiom,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t67,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t12]) ).
cnf(t142,plain,
inverse(multiply(X1,sFlat1)) = multiply(sFlat2,inverse(X1)),
inference(cp,[status(thm)],[t67,t137]) ).
cnf(t331,plain,
inverse(multiply(X1,sFlat1)) = multiply(sFlat2,inverse(X1)),
inference(orient,[status(thm)],[t142]) ).
cnf(t17,axiom,
greatest_lower_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(greatest_lower_bound(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t35,plain,
greatest_lower_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(greatest_lower_bound(X1,X3),X2),
inference(orient,[status(thm)],[t17]) ).
cnf(t4,axiom,
multiply(identity,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t25,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t36,plain,
multiply(greatest_lower_bound(identity,X1),X2) = greatest_lower_bound(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t35,t25]) ).
cnf(t317,plain,
greatest_lower_bound(X1,multiply(X2,X1)) = multiply(greatest_lower_bound(identity,X2),X1),
inference(orient,[status(thm)],[t36]) ).
cnf(t2,axiom,
inverse(inverse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t30,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t145,plain,
sFlat1 = inverse(sFlat2),
inference(cp,[status(thm)],[t30,t137]) ).
cnf(t153,plain,
inverse(sFlat2) = sFlat1,
inference(orient,[status(thm)],[t145]) ).
cnf(t159,plain,
inverse(multiply(sFlat2,X1)) = multiply(inverse(X1),sFlat1),
inference(cp,[status(thm)],[t67,t153]) ).
cnf(t479,plain,
inverse(multiply(sFlat2,X1)) = multiply(inverse(X1),sFlat1),
inference(orient,[status(thm)],[t159]) ).
cnf(t19,axiom,
least_upper_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(least_upper_bound(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t41,plain,
least_upper_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(least_upper_bound(X1,X3),X2),
inference(orient,[status(thm)],[t19]) ).
cnf(t5,axiom,
multiply(inverse(X1),X1) = identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t56,plain,
multiply(inverse(X1),X1) = identity,
inference(orient,[status(thm)],[t5]) ).
cnf(t59,plain,
multiply(least_upper_bound(X1,inverse(X2)),X2) = least_upper_bound(multiply(X1,X2),identity),
inference(cp,[status(thm)],[t41,t56]) ).
cnf(t2279,plain,
multiply(least_upper_bound(X1,inverse(X2)),X2) = least_upper_bound(identity,multiply(X1,X2)),
inference(step,[status(thm)],[t59,t115]) ).
cnf(t1870,plain,
multiply(least_upper_bound(X1,inverse(X2)),X2) = least_upper_bound(identity,multiply(X1,X2)),
inference(orient,[status(thm)],[t2279]) ).
cnf(t1880,plain,
least_upper_bound(identity,multiply(identity,a)) = multiply(sFlat2,a),
inference(cp,[status(thm)],[t1870,t365]) ).
cnf(t2280,plain,
least_upper_bound(identity,a) = multiply(sFlat2,a),
inference(step,[status(thm)],[t1880,t25]) ).
cnf(t2281,plain,
sFlat0 = multiply(sFlat2,a),
inference(step,[status(thm)],[t2280,t134]) ).
cnf(t1927,plain,
multiply(sFlat2,a) = sFlat0,
inference(orient,[status(thm)],[t2281]) ).
cnf(t1932,plain,
multiply(inverse(a),sFlat1) = inverse(sFlat0),
inference(cp,[status(thm)],[t479,t1927]) ).
cnf(t2021,plain,
multiply(inverse(a),sFlat1) = inverse(sFlat0),
inference(orient,[status(thm)],[t1932]) ).
cnf(t2022,plain,
multiply(greatest_lower_bound(identity,inverse(a)),sFlat1) = greatest_lower_bound(sFlat1,inverse(sFlat0)),
inference(cp,[status(thm)],[t317,t2021]) ).
cnf(t10,axiom,
greatest_lower_bound(inverse(X1),inverse(X2)) = inverse(least_upper_bound(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t106,plain,
greatest_lower_bound(inverse(X1),inverse(X2)) = inverse(least_upper_bound(X1,X2)),
inference(orient,[status(thm)],[t10]) ).
cnf(t149,plain,
inverse(least_upper_bound(identity,X1)) = greatest_lower_bound(identity,inverse(X1)),
inference(cp,[status(thm)],[t106,t146]) ).
cnf(t390,plain,
inverse(least_upper_bound(identity,X1)) = greatest_lower_bound(identity,inverse(X1)),
inference(orient,[status(thm)],[t149]) ).
cnf(t392,plain,
greatest_lower_bound(identity,inverse(a)) = inverse(sFlat0),
inference(cp,[status(thm)],[t390,t134]) ).
cnf(t402,plain,
greatest_lower_bound(identity,inverse(a)) = inverse(sFlat0),
inference(orient,[status(thm)],[t392]) ).
cnf(t2321,plain,
multiply(inverse(sFlat0),sFlat1) = greatest_lower_bound(sFlat1,inverse(sFlat0)),
inference(step,[status(thm)],[t2022,t402]) ).
cnf(t15,axiom,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t31,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t15]) ).
cnf(t57,plain,
identity = multiply(X1,inverse(X1)),
inference(cp,[status(thm)],[t56,t30]) ).
cnf(t191,plain,
multiply(X1,inverse(X1)) = identity,
inference(orient,[status(thm)],[t57]) ).
cnf(t201,plain,
multiply(X1,multiply(inverse(X1),X2)) = multiply(identity,X2),
inference(cp,[status(thm)],[t31,t191]) ).
cnf(t2268,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(step,[status(thm)],[t201,t25]) ).
cnf(t1390,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t2268]) ).
cnf(t1392,plain,
inverse(X1) = multiply(X2,inverse(multiply(X1,X2))),
inference(cp,[status(thm)],[t1390,t67]) ).
cnf(t1758,plain,
multiply(X1,inverse(multiply(X2,X1))) = inverse(X2),
inference(orient,[status(thm)],[t1392]) ).
cnf(t1945,plain,
inverse(sFlat2) = multiply(a,inverse(sFlat0)),
inference(cp,[status(thm)],[t1758,t1927]) ).
cnf(t2283,plain,
sFlat1 = multiply(a,inverse(sFlat0)),
inference(step,[status(thm)],[t1945,t153]) ).
cnf(t1961,plain,
multiply(a,inverse(sFlat0)) = sFlat1,
inference(orient,[status(thm)],[t2283]) ).
cnf(t1964,plain,
multiply(greatest_lower_bound(identity,a),inverse(sFlat0)) = greatest_lower_bound(inverse(sFlat0),sFlat1),
inference(cp,[status(thm)],[t317,t1961]) ).
cnf(t2302,plain,
multiply(sFlat1,inverse(sFlat0)) = greatest_lower_bound(inverse(sFlat0),sFlat1),
inference(step,[status(thm)],[t1964,t112]) ).
cnf(t2303,plain,
multiply(sFlat1,inverse(sFlat0)) = greatest_lower_bound(sFlat1,inverse(sFlat0)),
inference(step,[status(thm)],[t2302,t90]) ).
cnf(t2084,plain,
greatest_lower_bound(sFlat1,inverse(sFlat0)) = multiply(sFlat1,inverse(sFlat0)),
inference(orient,[status(thm)],[t2303]) ).
cnf(t2322,plain,
multiply(inverse(sFlat0),sFlat1) = multiply(sFlat1,inverse(sFlat0)),
inference(step,[status(thm)],[t2321,t2084]) ).
cnf(t2157,plain,
multiply(inverse(sFlat0),sFlat1) = multiply(sFlat1,inverse(sFlat0)),
inference(orient,[status(thm)],[t2322]) ).
cnf(t2162,plain,
multiply(sFlat2,inverse(inverse(sFlat0))) = inverse(multiply(sFlat1,inverse(sFlat0))),
inference(cp,[status(thm)],[t331,t2157]) ).
cnf(t2323,plain,
multiply(sFlat2,sFlat0) = inverse(multiply(sFlat1,inverse(sFlat0))),
inference(step,[status(thm)],[t2162,t30]) ).
cnf(t143,plain,
inverse(multiply(sFlat1,X1)) = multiply(inverse(X1),sFlat2),
inference(cp,[status(thm)],[t67,t137]) ).
cnf(t341,plain,
inverse(multiply(sFlat1,X1)) = multiply(inverse(X1),sFlat2),
inference(orient,[status(thm)],[t143]) ).
cnf(t2324,plain,
multiply(sFlat2,sFlat0) = multiply(inverse(inverse(sFlat0)),sFlat2),
inference(step,[status(thm)],[t2323,t341]) ).
cnf(t2325,plain,
multiply(sFlat2,sFlat0) = multiply(sFlat0,sFlat2),
inference(step,[status(thm)],[t2324,t30]) ).
cnf(t2177,plain,
multiply(sFlat2,sFlat0) = multiply(sFlat0,sFlat2),
inference(orient,[status(thm)],[t2325]) ).
cnf(goal_0,negated_conjecture,
multiply(least_upper_bound(a,identity),inverse(greatest_lower_bound(a,identity))) != multiply(inverse(greatest_lower_bound(a,identity)),least_upper_bound(a,identity)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(least_upper_bound(identity,a),inverse(greatest_lower_bound(a,identity))) != multiply(inverse(greatest_lower_bound(a,identity)),least_upper_bound(a,identity)),
inference(rw,[status(thm)],[goal_0,t115]) ).
cnf(g0_1,plain,
multiply(sFlat0,inverse(greatest_lower_bound(a,identity))) != multiply(inverse(greatest_lower_bound(a,identity)),least_upper_bound(a,identity)),
inference(rw,[status(thm)],[g0_0,t134]) ).
cnf(g0_2,plain,
multiply(sFlat0,least_upper_bound(identity,inverse(a))) != multiply(inverse(greatest_lower_bound(a,identity)),least_upper_bound(a,identity)),
inference(rw,[status(thm)],[g0_1,t369]) ).
cnf(g0_3,plain,
multiply(sFlat0,sFlat2) != multiply(inverse(greatest_lower_bound(a,identity)),least_upper_bound(a,identity)),
inference(rw,[status(thm)],[g0_2,t365]) ).
cnf(g0_4,plain,
multiply(sFlat0,sFlat2) != multiply(least_upper_bound(identity,inverse(a)),least_upper_bound(a,identity)),
inference(rw,[status(thm)],[g0_3,t369]) ).
cnf(g0_5,plain,
multiply(sFlat0,sFlat2) != multiply(sFlat2,least_upper_bound(a,identity)),
inference(rw,[status(thm)],[g0_4,t365]) ).
cnf(g0_6,plain,
multiply(sFlat0,sFlat2) != multiply(sFlat2,least_upper_bound(identity,a)),
inference(rw,[status(thm)],[g0_5,t115]) ).
cnf(g0_7,plain,
multiply(sFlat0,sFlat2) != multiply(sFlat2,sFlat0),
inference(rw,[status(thm)],[g0_6,t134]) ).
cnf(g0_8,plain,
multiply(sFlat0,sFlat2) != multiply(sFlat0,sFlat2),
inference(rw,[status(thm)],[g0_7,t2177]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP184-4 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.12/0.79 % Computer : n002.cluster.edu
% 0.12/0.79 % Model : x86_64 x86_64
% 0.12/0.79 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.79 % Memory : 8046.5625MB
% 0.12/0.79 % OS : Linux 6.8.0-71-generic
% 0.12/0.79 % CPULimit : 300
% 0.12/0.79 % WCLimit : 300
% 0.12/0.79 % DateTime : Wed Sep 23 14:05:51 UTC 2026
% 0.12/0.79 % CPUTime :
% 0.12/0.79 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 9.83/2.14 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.83/2.14 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------