%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP180-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n010.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:34 PM UTC 2026
% Result : Unsatisfiable 34.17s 4.77s
% Output : CNFRefutation 34.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 75
% Number of leaves : 14
% Syntax : Number of clauses : 222 ( 222 unt; 0 nHn; 3 RR)
% Number of literals : 222 ( 221 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 427 ( 39 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t10,axiom,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t3,axiom,
multiply(inverse(X1),X1) = identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t35,plain,
multiply(inverse(X1),X1) = identity,
inference(orient,[status(thm)],[t3]) ).
cnf(t44,plain,
multiply(inverse(X1),multiply(X1,X2)) = multiply(identity,X2),
inference(cp,[status(thm)],[t20,t35]) ).
cnf(t2,axiom,
multiply(identity,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t15,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t51450,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(step,[status(thm)],[t44,t15]) ).
cnf(t113,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(orient,[status(thm)],[t51450]) ).
cnf(t114,plain,
X1 = multiply(inverse(inverse(X1)),identity),
inference(cp,[status(thm)],[t113,t35]) ).
cnf(t132,plain,
multiply(inverse(inverse(X1)),identity) = X1,
inference(orient,[status(thm)],[t114]) ).
cnf(t117,plain,
multiply(X1,X2) = multiply(inverse(inverse(X1)),X2),
inference(cp,[status(thm)],[t113,t113]) ).
cnf(t151,plain,
multiply(inverse(inverse(X1)),X2) = multiply(X1,X2),
inference(orient,[status(thm)],[t117]) ).
cnf(t51451,plain,
multiply(X1,identity) = X1,
inference(step,[status(thm)],[t132,t151]) ).
cnf(t158,plain,
multiply(X1,identity) = X1,
inference(rw,[status(thm)],[t51451]) ).
cnf(t159,plain,
multiply(X1,identity) = X1,
inference(orient,[status(thm)],[t158]) ).
cnf(t160,plain,
inverse(inverse(X1)) = multiply(X1,identity),
inference(cp,[status(thm)],[t159,t151]) ).
cnf(t51452,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t160,t159]) ).
cnf(t165,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t51452]) ).
cnf(t167,plain,
identity = multiply(X1,inverse(X1)),
inference(cp,[status(thm)],[t35,t165]) ).
cnf(t168,plain,
multiply(X1,inverse(X1)) = identity,
inference(orient,[status(thm)],[t167]) ).
cnf(t169,plain,
identity = multiply(X1,multiply(X2,inverse(multiply(X1,X2)))),
inference(cp,[status(thm)],[t168,t20]) ).
cnf(t584,plain,
multiply(X1,multiply(X2,inverse(multiply(X1,X2)))) = identity,
inference(orient,[status(thm)],[t169]) ).
cnf(t602,plain,
multiply(X1,inverse(multiply(X2,X1))) = multiply(inverse(X2),identity),
inference(cp,[status(thm)],[t113,t584]) ).
cnf(t51481,plain,
multiply(X1,inverse(multiply(X2,X1))) = inverse(X2),
inference(step,[status(thm)],[t602,t159]) ).
cnf(t616,plain,
multiply(X1,inverse(multiply(X2,X1))) = inverse(X2),
inference(orient,[status(thm)],[t51481]) ).
cnf(t644,plain,
inverse(X1) = multiply(inverse(multiply(X2,X1)),inverse(inverse(X2))),
inference(cp,[status(thm)],[t616,t616]) ).
cnf(t633,plain,
inverse(multiply(X1,X2)) = multiply(inverse(X2),inverse(X1)),
inference(cp,[status(thm)],[t113,t616]) ).
cnf(t647,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t633]) ).
cnf(t51482,plain,
inverse(X1) = inverse(multiply(inverse(X2),multiply(X2,X1))),
inference(step,[status(thm)],[t644,t647]) ).
cnf(t649,plain,
inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(cp,[status(thm)],[t647,t165]) ).
cnf(t685,plain,
inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(orient,[status(thm)],[t649]) ).
cnf(t51483,plain,
inverse(X1) = multiply(inverse(multiply(X2,X1)),X2),
inference(step,[status(thm)],[t51482,t685]) ).
cnf(t705,plain,
multiply(inverse(multiply(X1,X2)),X1) = inverse(X2),
inference(orient,[status(thm)],[t51483]) ).
cnf(t11,axiom,
greatest_lower_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,greatest_lower_bound(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
greatest_lower_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,greatest_lower_bound(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t174,plain,
multiply(X1,greatest_lower_bound(inverse(X1),X2)) = greatest_lower_bound(identity,multiply(X1,X2)),
inference(cp,[status(thm)],[t23,t168]) ).
cnf(t4,axiom,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t71,plain,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t51471,plain,
multiply(X1,greatest_lower_bound(X2,inverse(X1))) = greatest_lower_bound(identity,multiply(X1,X2)),
inference(step,[status(thm)],[t174,t71]) ).
cnf(t471,plain,
multiply(X1,greatest_lower_bound(X2,inverse(X1))) = greatest_lower_bound(identity,multiply(X1,X2)),
inference(orient,[status(thm)],[t51471]) ).
cnf(t707,plain,
inverse(greatest_lower_bound(X1,inverse(X2))) = multiply(inverse(greatest_lower_bound(identity,multiply(X2,X1))),X2),
inference(cp,[status(thm)],[t705,t471]) ).
cnf(t5371,plain,
multiply(inverse(greatest_lower_bound(identity,multiply(X1,X2))),X1) = inverse(greatest_lower_bound(X2,inverse(X1))),
inference(orient,[status(thm)],[t707]) ).
cnf(t12,axiom,
greatest_lower_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(greatest_lower_bound(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t30,plain,
greatest_lower_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(greatest_lower_bound(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t170,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X1)) = greatest_lower_bound(identity,multiply(X2,inverse(X1))),
inference(cp,[status(thm)],[t30,t168]) ).
cnf(t23711,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X1)) = greatest_lower_bound(identity,multiply(X2,inverse(X1))),
inference(orient,[status(thm)],[t170]) ).
cnf(t23908,plain,
inverse(greatest_lower_bound(inverse(X1),inverse(X2))) = multiply(inverse(multiply(greatest_lower_bound(X1,X2),inverse(X1))),X2),
inference(cp,[status(thm)],[t5371,t23711]) ).
cnf(t166,plain,
X1 = multiply(X2,multiply(inverse(X2),X1)),
inference(cp,[status(thm)],[t113,t165]) ).
cnf(t179,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t166]) ).
cnf(t643,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(cp,[status(thm)],[t179,t616]) ).
cnf(t666,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t643]) ).
cnf(t52132,plain,
inverse(greatest_lower_bound(inverse(X1),inverse(X2))) = multiply(multiply(X1,inverse(greatest_lower_bound(X1,X2))),X2),
inference(step,[status(thm)],[t23908,t666]) ).
cnf(t52133,plain,
inverse(greatest_lower_bound(inverse(X1),inverse(X2))) = multiply(X1,multiply(inverse(greatest_lower_bound(X1,X2)),X2)),
inference(step,[status(thm)],[t52132,t20]) ).
cnf(t28529,plain,
multiply(X1,multiply(inverse(greatest_lower_bound(X1,X2)),X2)) = inverse(greatest_lower_bound(inverse(X1),inverse(X2))),
inference(orient,[status(thm)],[t52133]) ).
cnf(t161,plain,
multiply(X1,greatest_lower_bound(identity,X2)) = greatest_lower_bound(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t23,t159]) ).
cnf(t51455,plain,
multiply(X1,greatest_lower_bound(X2,identity)) = greatest_lower_bound(X1,multiply(X1,X2)),
inference(step,[status(thm)],[t161,t71]) ).
cnf(t213,plain,
greatest_lower_bound(X1,multiply(X1,X2)) = multiply(X1,greatest_lower_bound(X2,identity)),
inference(orient,[status(thm)],[t51455]) ).
cnf(t219,plain,
multiply(inverse(X1),greatest_lower_bound(multiply(X1,X2),identity)) = greatest_lower_bound(inverse(X1),X2),
inference(cp,[status(thm)],[t213,t113]) ).
cnf(t51490,plain,
multiply(inverse(X1),greatest_lower_bound(identity,multiply(X1,X2))) = greatest_lower_bound(inverse(X1),X2),
inference(step,[status(thm)],[t219,t71]) ).
cnf(t51491,plain,
multiply(inverse(X1),greatest_lower_bound(identity,multiply(X1,X2))) = greatest_lower_bound(X2,inverse(X1)),
inference(step,[status(thm)],[t51490,t71]) ).
cnf(t1072,plain,
multiply(inverse(X1),greatest_lower_bound(identity,multiply(X1,X2))) = greatest_lower_bound(X2,inverse(X1)),
inference(orient,[status(thm)],[t51491]) ).
cnf(t13,axiom,
least_upper_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,least_upper_bound(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
least_upper_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,least_upper_bound(X2,X3)),
inference(orient,[status(thm)],[t13]) ).
cnf(t176,plain,
multiply(X1,least_upper_bound(inverse(X1),X2)) = least_upper_bound(identity,multiply(X1,X2)),
inference(cp,[status(thm)],[t21,t168]) ).
cnf(t6,axiom,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t45,plain,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t51472,plain,
multiply(X1,least_upper_bound(X2,inverse(X1))) = least_upper_bound(identity,multiply(X1,X2)),
inference(step,[status(thm)],[t176,t45]) ).
cnf(t490,plain,
multiply(X1,least_upper_bound(X2,inverse(X1))) = least_upper_bound(identity,multiply(X1,X2)),
inference(orient,[status(thm)],[t51472]) ).
cnf(t1079,plain,
greatest_lower_bound(least_upper_bound(X1,inverse(X2)),inverse(X2)) = multiply(inverse(X2),greatest_lower_bound(identity,least_upper_bound(identity,multiply(X2,X1)))),
inference(cp,[status(thm)],[t1072,t490]) ).
cnf(t51492,plain,
greatest_lower_bound(inverse(X2),least_upper_bound(X1,inverse(X2))) = multiply(inverse(X2),greatest_lower_bound(identity,least_upper_bound(identity,multiply(X2,X1)))),
inference(step,[status(thm)],[t1079,t71]) ).
cnf(t5,axiom,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t51493,plain,
greatest_lower_bound(inverse(X2),least_upper_bound(X1,inverse(X2))) = multiply(inverse(X2),identity),
inference(step,[status(thm)],[t51492,t19]) ).
cnf(t51494,plain,
greatest_lower_bound(inverse(X2),least_upper_bound(X1,inverse(X2))) = inverse(X2),
inference(step,[status(thm)],[t51493,t159]) ).
cnf(t1126,plain,
greatest_lower_bound(inverse(X1),least_upper_bound(X2,inverse(X1))) = inverse(X1),
inference(orient,[status(thm)],[t51494]) ).
cnf(t7,axiom,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t17,plain,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t14,axiom,
least_upper_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(least_upper_bound(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
least_upper_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(least_upper_bound(X1,X3),X2),
inference(orient,[status(thm)],[t14]) ).
cnf(t38,plain,
multiply(least_upper_bound(inverse(X1),X2),X1) = least_upper_bound(identity,multiply(X2,X1)),
inference(cp,[status(thm)],[t24,t35]) ).
cnf(t51470,plain,
multiply(least_upper_bound(X2,inverse(X1)),X1) = least_upper_bound(identity,multiply(X2,X1)),
inference(step,[status(thm)],[t38,t45]) ).
cnf(t454,plain,
multiply(least_upper_bound(X1,inverse(X2)),X2) = least_upper_bound(identity,multiply(X1,X2)),
inference(orient,[status(thm)],[t51470]) ).
cnf(t1090,plain,
greatest_lower_bound(X1,inverse(least_upper_bound(X2,inverse(X1)))) = multiply(inverse(least_upper_bound(X2,inverse(X1))),greatest_lower_bound(identity,least_upper_bound(identity,multiply(X2,X1)))),
inference(cp,[status(thm)],[t1072,t454]) ).
cnf(t51499,plain,
greatest_lower_bound(X1,inverse(least_upper_bound(X2,inverse(X1)))) = multiply(inverse(least_upper_bound(X2,inverse(X1))),identity),
inference(step,[status(thm)],[t1090,t19]) ).
cnf(t51500,plain,
greatest_lower_bound(X1,inverse(least_upper_bound(X2,inverse(X1)))) = inverse(least_upper_bound(X2,inverse(X1))),
inference(step,[status(thm)],[t51499,t159]) ).
cnf(t1169,plain,
greatest_lower_bound(X1,inverse(least_upper_bound(X2,inverse(X1)))) = inverse(least_upper_bound(X2,inverse(X1))),
inference(orient,[status(thm)],[t51500]) ).
cnf(t1178,plain,
X1 = least_upper_bound(X1,inverse(least_upper_bound(X2,inverse(X1)))),
inference(cp,[status(thm)],[t17,t1169]) ).
cnf(t1184,plain,
least_upper_bound(X1,inverse(least_upper_bound(X2,inverse(X1)))) = X1,
inference(orient,[status(thm)],[t1178]) ).
cnf(t1191,plain,
inverse(X1) = least_upper_bound(inverse(X1),inverse(least_upper_bound(X2,X1))),
inference(cp,[status(thm)],[t1184,t165]) ).
cnf(t51502,plain,
inverse(X1) = least_upper_bound(inverse(X1),inverse(least_upper_bound(X1,X2))),
inference(step,[status(thm)],[t1191,t45]) ).
cnf(t1221,plain,
least_upper_bound(inverse(X1),inverse(least_upper_bound(X1,X2))) = inverse(X1),
inference(orient,[status(thm)],[t51502]) ).
cnf(t1235,plain,
inverse(least_upper_bound(X1,X2)) = greatest_lower_bound(inverse(least_upper_bound(X1,X2)),inverse(X1)),
inference(cp,[status(thm)],[t1126,t1221]) ).
cnf(t51515,plain,
inverse(least_upper_bound(X1,X2)) = greatest_lower_bound(inverse(X1),inverse(least_upper_bound(X1,X2))),
inference(step,[status(thm)],[t1235,t71]) ).
cnf(t1390,plain,
greatest_lower_bound(inverse(X1),inverse(least_upper_bound(X1,X2))) = inverse(least_upper_bound(X1,X2)),
inference(orient,[status(thm)],[t51515]) ).
cnf(t26,plain,
multiply(least_upper_bound(multiply(X1,X2),X3),Y3) = least_upper_bound(multiply(X1,multiply(X2,Y3)),multiply(X3,Y3)),
inference(cp,[status(thm)],[t24,t20]) ).
cnf(t51479,plain,
multiply(least_upper_bound(X3,multiply(X1,X2)),Y3) = least_upper_bound(multiply(X1,multiply(X2,Y3)),multiply(X3,Y3)),
inference(step,[status(thm)],[t26,t45]) ).
cnf(t51480,plain,
multiply(least_upper_bound(X3,multiply(X1,X2)),Y3) = least_upper_bound(multiply(X3,Y3),multiply(X1,multiply(X2,Y3))),
inference(step,[status(thm)],[t51479,t45]) ).
cnf(t539,plain,
least_upper_bound(multiply(X1,X2),multiply(X3,multiply(Y3,X2))) = multiply(least_upper_bound(X1,multiply(X3,Y3)),X2),
inference(orient,[status(thm)],[t51480]) ).
cnf(t569,plain,
multiply(least_upper_bound(X1,multiply(X2,X3)),inverse(X3)) = least_upper_bound(multiply(X1,inverse(X3)),multiply(X2,identity)),
inference(cp,[status(thm)],[t539,t168]) ).
cnf(t52083,plain,
multiply(least_upper_bound(X1,multiply(X2,X3)),inverse(X3)) = least_upper_bound(multiply(X2,identity),multiply(X1,inverse(X3))),
inference(step,[status(thm)],[t569,t45]) ).
cnf(t52084,plain,
multiply(least_upper_bound(X1,multiply(X2,X3)),inverse(X3)) = least_upper_bound(X2,multiply(X1,inverse(X3))),
inference(step,[status(thm)],[t52083,t159]) ).
cnf(t25096,plain,
multiply(least_upper_bound(X1,multiply(X2,X3)),inverse(X3)) = least_upper_bound(X2,multiply(X1,inverse(X3))),
inference(orient,[status(thm)],[t52084]) ).
cnf(t163,plain,
multiply(X1,least_upper_bound(identity,X2)) = least_upper_bound(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t21,t159]) ).
cnf(t51456,plain,
multiply(X1,least_upper_bound(X2,identity)) = least_upper_bound(X1,multiply(X1,X2)),
inference(step,[status(thm)],[t163,t45]) ).
cnf(t225,plain,
least_upper_bound(X1,multiply(X1,X2)) = multiply(X1,least_upper_bound(X2,identity)),
inference(orient,[status(thm)],[t51456]) ).
cnf(t231,plain,
multiply(inverse(X1),least_upper_bound(multiply(X1,X2),identity)) = least_upper_bound(inverse(X1),X2),
inference(cp,[status(thm)],[t225,t113]) ).
cnf(t51520,plain,
multiply(inverse(X1),least_upper_bound(identity,multiply(X1,X2))) = least_upper_bound(inverse(X1),X2),
inference(step,[status(thm)],[t231,t45]) ).
cnf(t51521,plain,
multiply(inverse(X1),least_upper_bound(identity,multiply(X1,X2))) = least_upper_bound(X2,inverse(X1)),
inference(step,[status(thm)],[t51520,t45]) ).
cnf(t1452,plain,
multiply(inverse(X1),least_upper_bound(identity,multiply(X1,X2))) = least_upper_bound(X2,inverse(X1)),
inference(orient,[status(thm)],[t51521]) ).
cnf(t1461,plain,
least_upper_bound(greatest_lower_bound(X1,inverse(X2)),inverse(X2)) = multiply(inverse(X2),least_upper_bound(identity,greatest_lower_bound(identity,multiply(X2,X1)))),
inference(cp,[status(thm)],[t1452,t471]) ).
cnf(t51522,plain,
least_upper_bound(inverse(X2),greatest_lower_bound(X1,inverse(X2))) = multiply(inverse(X2),least_upper_bound(identity,greatest_lower_bound(identity,multiply(X2,X1)))),
inference(step,[status(thm)],[t1461,t45]) ).
cnf(t51523,plain,
least_upper_bound(inverse(X2),greatest_lower_bound(X1,inverse(X2))) = multiply(inverse(X2),identity),
inference(step,[status(thm)],[t51522,t17]) ).
cnf(t51524,plain,
least_upper_bound(inverse(X2),greatest_lower_bound(X1,inverse(X2))) = inverse(X2),
inference(step,[status(thm)],[t51523,t159]) ).
cnf(t1508,plain,
least_upper_bound(inverse(X1),greatest_lower_bound(X2,inverse(X1))) = inverse(X1),
inference(orient,[status(thm)],[t51524]) ).
cnf(t1177,plain,
inverse(least_upper_bound(X1,inverse(inverse(X2)))) = greatest_lower_bound(inverse(X2),inverse(least_upper_bound(X1,X2))),
inference(cp,[status(thm)],[t1169,t165]) ).
cnf(t51503,plain,
inverse(least_upper_bound(X1,X2)) = greatest_lower_bound(inverse(X2),inverse(least_upper_bound(X1,X2))),
inference(step,[status(thm)],[t1177,t165]) ).
cnf(t1243,plain,
greatest_lower_bound(inverse(X1),inverse(least_upper_bound(X2,X1))) = inverse(least_upper_bound(X2,X1)),
inference(orient,[status(thm)],[t51503]) ).
cnf(t1251,plain,
inverse(least_upper_bound(X1,greatest_lower_bound(X1,X2))) = greatest_lower_bound(inverse(greatest_lower_bound(X1,X2)),inverse(X1)),
inference(cp,[status(thm)],[t1243,t17]) ).
cnf(t51508,plain,
inverse(X1) = greatest_lower_bound(inverse(greatest_lower_bound(X1,X2)),inverse(X1)),
inference(step,[status(thm)],[t1251,t17]) ).
cnf(t51509,plain,
inverse(X1) = greatest_lower_bound(inverse(X1),inverse(greatest_lower_bound(X1,X2))),
inference(step,[status(thm)],[t51508,t71]) ).
cnf(t1276,plain,
greatest_lower_bound(inverse(X1),inverse(greatest_lower_bound(X1,X2))) = inverse(X1),
inference(orient,[status(thm)],[t51509]) ).
cnf(t1514,plain,
inverse(greatest_lower_bound(X1,X2)) = least_upper_bound(inverse(greatest_lower_bound(X1,X2)),inverse(X1)),
inference(cp,[status(thm)],[t1508,t1276]) ).
cnf(t51528,plain,
inverse(greatest_lower_bound(X1,X2)) = least_upper_bound(inverse(X1),inverse(greatest_lower_bound(X1,X2))),
inference(step,[status(thm)],[t1514,t45]) ).
cnf(t1547,plain,
least_upper_bound(inverse(X1),inverse(greatest_lower_bound(X1,X2))) = inverse(greatest_lower_bound(X1,X2)),
inference(orient,[status(thm)],[t51528]) ).
cnf(t1565,plain,
least_upper_bound(identity,multiply(greatest_lower_bound(X1,X2),inverse(X1))) = multiply(greatest_lower_bound(X1,X2),inverse(greatest_lower_bound(X1,X2))),
inference(cp,[status(thm)],[t490,t1547]) ).
cnf(t51531,plain,
least_upper_bound(identity,multiply(greatest_lower_bound(X1,X2),inverse(X1))) = identity,
inference(step,[status(thm)],[t1565,t168]) ).
cnf(t1585,plain,
least_upper_bound(identity,multiply(greatest_lower_bound(X1,X2),inverse(X1))) = identity,
inference(orient,[status(thm)],[t51531]) ).
cnf(t1588,plain,
identity = least_upper_bound(identity,multiply(inverse(least_upper_bound(X1,X2)),inverse(inverse(X2)))),
inference(cp,[status(thm)],[t1585,t1243]) ).
cnf(t51537,plain,
identity = least_upper_bound(identity,inverse(multiply(inverse(X2),least_upper_bound(X1,X2)))),
inference(step,[status(thm)],[t1588,t647]) ).
cnf(t51538,plain,
identity = least_upper_bound(identity,multiply(inverse(least_upper_bound(X1,X2)),X2)),
inference(step,[status(thm)],[t51537,t685]) ).
cnf(t1773,plain,
least_upper_bound(identity,multiply(inverse(least_upper_bound(X1,X2)),X2)) = identity,
inference(orient,[status(thm)],[t51538]) ).
cnf(t9,axiom,
least_upper_bound(least_upper_bound(X1,X2),X3) = least_upper_bound(X1,least_upper_bound(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t51444,plain,
least_upper_bound(X3,least_upper_bound(X1,X2)) = least_upper_bound(X1,least_upper_bound(X2,X3)),
inference(step,[status(thm)],[t9,t45]) ).
cnf(t49,plain,
least_upper_bound(X1,least_upper_bound(X2,X3)) = least_upper_bound(X2,least_upper_bound(X3,X1)),
inference(orient,[status(thm)],[t51444]) ).
cnf(t53,plain,
least_upper_bound(greatest_lower_bound(X1,X2),least_upper_bound(X3,X1)) = least_upper_bound(X3,X1),
inference(cp,[status(thm)],[t49,t17]) ).
cnf(t51473,plain,
least_upper_bound(X1,least_upper_bound(greatest_lower_bound(X1,X2),X3)) = least_upper_bound(X3,X1),
inference(step,[status(thm)],[t53,t49]) ).
cnf(t51474,plain,
least_upper_bound(X1,least_upper_bound(X3,greatest_lower_bound(X1,X2))) = least_upper_bound(X3,X1),
inference(step,[status(thm)],[t51473,t45]) ).
cnf(t51475,plain,
least_upper_bound(X1,least_upper_bound(X3,greatest_lower_bound(X1,X2))) = least_upper_bound(X1,X3),
inference(step,[status(thm)],[t51474,t45]) ).
cnf(t509,plain,
least_upper_bound(X1,least_upper_bound(X2,greatest_lower_bound(X1,X3))) = least_upper_bound(X1,X2),
inference(orient,[status(thm)],[t51475]) ).
cnf(t31,plain,
multiply(greatest_lower_bound(identity,X1),X2) = greatest_lower_bound(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t30,t15]) ).
cnf(t51454,plain,
multiply(greatest_lower_bound(X1,identity),X2) = greatest_lower_bound(X2,multiply(X1,X2)),
inference(step,[status(thm)],[t31,t71]) ).
cnf(t201,plain,
greatest_lower_bound(X1,multiply(X2,X1)) = multiply(greatest_lower_bound(X2,identity),X1),
inference(orient,[status(thm)],[t51454]) ).
cnf(t513,plain,
least_upper_bound(X1,X2) = least_upper_bound(X1,least_upper_bound(X2,multiply(greatest_lower_bound(X3,identity),X1))),
inference(cp,[status(thm)],[t509,t201]) ).
cnf(t6049,plain,
least_upper_bound(X1,least_upper_bound(X2,multiply(greatest_lower_bound(X3,identity),X1))) = least_upper_bound(X1,X2),
inference(orient,[status(thm)],[t513]) ).
cnf(t6054,plain,
least_upper_bound(X1,greatest_lower_bound(X2,identity)) = least_upper_bound(X1,multiply(greatest_lower_bound(X2,identity),least_upper_bound(X1,identity))),
inference(cp,[status(thm)],[t6049,t225]) ).
cnf(t46949,plain,
least_upper_bound(X1,multiply(greatest_lower_bound(X2,identity),least_upper_bound(X1,identity))) = least_upper_bound(X1,greatest_lower_bound(X2,identity)),
inference(orient,[status(thm)],[t6054]) ).
cnf(t214,plain,
multiply(X1,greatest_lower_bound(X1,identity)) = multiply(greatest_lower_bound(X1,identity),X1),
inference(cp,[status(thm)],[t213,t201]) ).
cnf(t237,plain,
multiply(greatest_lower_bound(X1,identity),X1) = multiply(X1,greatest_lower_bound(X1,identity)),
inference(orient,[status(thm)],[t214]) ).
cnf(t239,plain,
multiply(greatest_lower_bound(X1,identity),least_upper_bound(X1,identity)) = least_upper_bound(greatest_lower_bound(X1,identity),multiply(X1,greatest_lower_bound(X1,identity))),
inference(cp,[status(thm)],[t225,t237]) ).
cnf(t25,plain,
multiply(least_upper_bound(identity,X1),X2) = least_upper_bound(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t24,t15]) ).
cnf(t51453,plain,
multiply(least_upper_bound(X1,identity),X2) = least_upper_bound(X2,multiply(X1,X2)),
inference(step,[status(thm)],[t25,t45]) ).
cnf(t189,plain,
least_upper_bound(X1,multiply(X2,X1)) = multiply(least_upper_bound(X2,identity),X1),
inference(orient,[status(thm)],[t51453]) ).
cnf(t51598,plain,
multiply(greatest_lower_bound(X1,identity),least_upper_bound(X1,identity)) = multiply(least_upper_bound(X1,identity),greatest_lower_bound(X1,identity)),
inference(step,[status(thm)],[t239,t189]) ).
cnf(t3587,plain,
multiply(greatest_lower_bound(X1,identity),least_upper_bound(X1,identity)) = multiply(least_upper_bound(X1,identity),greatest_lower_bound(X1,identity)),
inference(orient,[status(thm)],[t51598]) ).
cnf(t46952,plain,
least_upper_bound(X1,greatest_lower_bound(X1,identity)) = least_upper_bound(X1,multiply(least_upper_bound(X1,identity),greatest_lower_bound(X1,identity))),
inference(cp,[status(thm)],[t46949,t3587]) ).
cnf(t52285,plain,
X1 = least_upper_bound(X1,multiply(least_upper_bound(X1,identity),greatest_lower_bound(X1,identity))),
inference(step,[status(thm)],[t46952,t17]) ).
cnf(t47007,plain,
least_upper_bound(X1,multiply(least_upper_bound(X1,identity),greatest_lower_bound(X1,identity))) = X1,
inference(orient,[status(thm)],[t52285]) ).
cnf(t47066,plain,
identity = least_upper_bound(identity,multiply(inverse(X1),multiply(least_upper_bound(X1,identity),greatest_lower_bound(X1,identity)))),
inference(cp,[status(thm)],[t1773,t47007]) ).
cnf(t230,plain,
multiply(inverse(X1),least_upper_bound(X1,identity)) = least_upper_bound(inverse(X1),identity),
inference(cp,[status(thm)],[t225,t35]) ).
cnf(t51468,plain,
multiply(inverse(X1),least_upper_bound(X1,identity)) = least_upper_bound(identity,inverse(X1)),
inference(step,[status(thm)],[t230,t45]) ).
cnf(t421,plain,
multiply(inverse(X1),least_upper_bound(X1,identity)) = least_upper_bound(identity,inverse(X1)),
inference(orient,[status(thm)],[t51468]) ).
cnf(t436,plain,
multiply(inverse(X1),multiply(least_upper_bound(X1,identity),X2)) = multiply(least_upper_bound(identity,inverse(X1)),X2),
inference(cp,[status(thm)],[t20,t421]) ).
cnf(t25013,plain,
multiply(inverse(X1),multiply(least_upper_bound(X1,identity),X2)) = multiply(least_upper_bound(identity,inverse(X1)),X2),
inference(orient,[status(thm)],[t436]) ).
cnf(t52286,plain,
identity = least_upper_bound(identity,multiply(least_upper_bound(identity,inverse(X1)),greatest_lower_bound(X1,identity))),
inference(step,[status(thm)],[t47066,t25013]) ).
cnf(t47148,plain,
least_upper_bound(identity,multiply(least_upper_bound(identity,inverse(X1)),greatest_lower_bound(X1,identity))) = identity,
inference(orient,[status(thm)],[t52286]) ).
cnf(t47194,plain,
least_upper_bound(least_upper_bound(identity,inverse(X1)),multiply(identity,inverse(greatest_lower_bound(X1,identity)))) = multiply(identity,inverse(greatest_lower_bound(X1,identity))),
inference(cp,[status(thm)],[t25096,t47148]) ).
cnf(t52290,plain,
least_upper_bound(least_upper_bound(identity,inverse(X1)),inverse(greatest_lower_bound(X1,identity))) = multiply(identity,inverse(greatest_lower_bound(X1,identity))),
inference(step,[status(thm)],[t47194,t15]) ).
cnf(t52291,plain,
least_upper_bound(least_upper_bound(identity,inverse(X1)),inverse(greatest_lower_bound(X1,identity))) = inverse(greatest_lower_bound(X1,identity)),
inference(step,[status(thm)],[t52290,t15]) ).
cnf(t47323,plain,
least_upper_bound(least_upper_bound(identity,inverse(X1)),inverse(greatest_lower_bound(X1,identity))) = inverse(greatest_lower_bound(X1,identity)),
inference(orient,[status(thm)],[t52291]) ).
cnf(t47358,plain,
inverse(least_upper_bound(least_upper_bound(identity,inverse(X1)),inverse(greatest_lower_bound(X1,identity)))) = greatest_lower_bound(inverse(least_upper_bound(identity,inverse(X1))),inverse(inverse(greatest_lower_bound(X1,identity)))),
inference(cp,[status(thm)],[t1390,t47323]) ).
cnf(t52292,plain,
inverse(inverse(greatest_lower_bound(X1,identity))) = greatest_lower_bound(inverse(least_upper_bound(identity,inverse(X1))),inverse(inverse(greatest_lower_bound(X1,identity)))),
inference(step,[status(thm)],[t47358,t47323]) ).
cnf(t52293,plain,
greatest_lower_bound(X1,identity) = greatest_lower_bound(inverse(least_upper_bound(identity,inverse(X1))),inverse(inverse(greatest_lower_bound(X1,identity)))),
inference(step,[status(thm)],[t52292,t165]) ).
cnf(t52294,plain,
greatest_lower_bound(X1,identity) = greatest_lower_bound(inverse(least_upper_bound(identity,inverse(X1))),greatest_lower_bound(X1,identity)),
inference(step,[status(thm)],[t52293,t165]) ).
cnf(t8,axiom,
greatest_lower_bound(greatest_lower_bound(X1,X2),X3) = greatest_lower_bound(X1,greatest_lower_bound(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t51445,plain,
greatest_lower_bound(X3,greatest_lower_bound(X1,X2)) = greatest_lower_bound(X1,greatest_lower_bound(X2,X3)),
inference(step,[status(thm)],[t8,t71]) ).
cnf(t75,plain,
greatest_lower_bound(X1,greatest_lower_bound(X2,X3)) = greatest_lower_bound(X2,greatest_lower_bound(X3,X1)),
inference(orient,[status(thm)],[t51445]) ).
cnf(t52295,plain,
greatest_lower_bound(X1,identity) = greatest_lower_bound(identity,greatest_lower_bound(inverse(least_upper_bound(identity,inverse(X1))),X1)),
inference(step,[status(thm)],[t52294,t75]) ).
cnf(t52296,plain,
greatest_lower_bound(X1,identity) = greatest_lower_bound(X1,greatest_lower_bound(identity,inverse(least_upper_bound(identity,inverse(X1))))),
inference(step,[status(thm)],[t52295,t75]) ).
cnf(t1586,plain,
identity = least_upper_bound(identity,multiply(inverse(least_upper_bound(X1,inverse(X2))),inverse(X2))),
inference(cp,[status(thm)],[t1585,t1169]) ).
cnf(t51535,plain,
identity = least_upper_bound(identity,inverse(multiply(X2,least_upper_bound(X1,inverse(X2))))),
inference(step,[status(thm)],[t1586,t647]) ).
cnf(t51536,plain,
identity = least_upper_bound(identity,inverse(least_upper_bound(identity,multiply(X2,X1)))),
inference(step,[status(thm)],[t51535,t490]) ).
cnf(t1725,plain,
least_upper_bound(identity,inverse(least_upper_bound(identity,multiply(X1,X2)))) = identity,
inference(orient,[status(thm)],[t51536]) ).
cnf(t1732,plain,
identity = least_upper_bound(identity,inverse(least_upper_bound(identity,inverse(X1)))),
inference(cp,[status(thm)],[t1725,t616]) ).
cnf(t1759,plain,
least_upper_bound(identity,inverse(least_upper_bound(identity,inverse(X1)))) = identity,
inference(orient,[status(thm)],[t1732]) ).
cnf(t1763,plain,
inverse(least_upper_bound(identity,inverse(X1))) = greatest_lower_bound(inverse(least_upper_bound(identity,inverse(X1))),identity),
inference(cp,[status(thm)],[t1126,t1759]) ).
cnf(t51557,plain,
inverse(least_upper_bound(identity,inverse(X1))) = greatest_lower_bound(identity,inverse(least_upper_bound(identity,inverse(X1)))),
inference(step,[status(thm)],[t1763,t71]) ).
cnf(t1983,plain,
greatest_lower_bound(identity,inverse(least_upper_bound(identity,inverse(X1)))) = inverse(least_upper_bound(identity,inverse(X1))),
inference(orient,[status(thm)],[t51557]) ).
cnf(t52297,plain,
greatest_lower_bound(X1,identity) = greatest_lower_bound(X1,inverse(least_upper_bound(identity,inverse(X1)))),
inference(step,[status(thm)],[t52296,t1983]) ).
cnf(t52298,plain,
greatest_lower_bound(X1,identity) = inverse(least_upper_bound(identity,inverse(X1))),
inference(step,[status(thm)],[t52297,t1169]) ).
cnf(t47408,plain,
inverse(least_upper_bound(identity,inverse(X1))) = greatest_lower_bound(X1,identity),
inference(orient,[status(thm)],[t52298]) ).
cnf(t47451,plain,
greatest_lower_bound(multiply(X1,inverse(X2)),identity) = inverse(least_upper_bound(identity,multiply(X2,inverse(X1)))),
inference(cp,[status(thm)],[t47408,t666]) ).
cnf(t52391,plain,
greatest_lower_bound(identity,multiply(X1,inverse(X2))) = inverse(least_upper_bound(identity,multiply(X2,inverse(X1)))),
inference(step,[status(thm)],[t47451,t71]) ).
cnf(t52392,plain,
multiply(greatest_lower_bound(X2,X1),inverse(X2)) = inverse(least_upper_bound(identity,multiply(X2,inverse(X1)))),
inference(step,[status(thm)],[t52391,t23711]) ).
cnf(t52393,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X2)) = inverse(least_upper_bound(identity,multiply(X2,inverse(X1)))),
inference(step,[status(thm)],[t52392,t71]) ).
cnf(t172,plain,
multiply(least_upper_bound(X1,X2),inverse(X1)) = least_upper_bound(identity,multiply(X2,inverse(X1))),
inference(cp,[status(thm)],[t24,t168]) ).
cnf(t28916,plain,
multiply(least_upper_bound(X1,X2),inverse(X1)) = least_upper_bound(identity,multiply(X2,inverse(X1))),
inference(orient,[status(thm)],[t172]) ).
cnf(t52394,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X2)) = inverse(multiply(least_upper_bound(X1,X2),inverse(X1))),
inference(step,[status(thm)],[t52393,t28916]) ).
cnf(t52395,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X2)) = multiply(X1,inverse(least_upper_bound(X1,X2))),
inference(step,[status(thm)],[t52394,t666]) ).
cnf(t50661,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X2)) = multiply(X1,inverse(least_upper_bound(X1,X2))),
inference(orient,[status(thm)],[t52395]) ).
cnf(t50868,plain,
inverse(greatest_lower_bound(X1,X2)) = multiply(inverse(X2),inverse(multiply(X1,inverse(least_upper_bound(X1,X2))))),
inference(cp,[status(thm)],[t616,t50661]) ).
cnf(t52396,plain,
inverse(greatest_lower_bound(X1,X2)) = inverse(multiply(multiply(X1,inverse(least_upper_bound(X1,X2))),X2)),
inference(step,[status(thm)],[t50868,t647]) ).
cnf(t52397,plain,
inverse(greatest_lower_bound(X1,X2)) = inverse(multiply(X1,multiply(inverse(least_upper_bound(X1,X2)),X2))),
inference(step,[status(thm)],[t52396,t20]) ).
cnf(t706,plain,
inverse(least_upper_bound(X1,inverse(X2))) = multiply(inverse(least_upper_bound(identity,multiply(X2,X1))),X2),
inference(cp,[status(thm)],[t705,t490]) ).
cnf(t5251,plain,
multiply(inverse(least_upper_bound(identity,multiply(X1,X2))),X1) = inverse(least_upper_bound(X2,inverse(X1))),
inference(orient,[status(thm)],[t706]) ).
cnf(t29133,plain,
inverse(least_upper_bound(inverse(X1),inverse(X2))) = multiply(inverse(multiply(least_upper_bound(X1,X2),inverse(X1))),X2),
inference(cp,[status(thm)],[t5251,t28916]) ).
cnf(t52141,plain,
inverse(least_upper_bound(inverse(X1),inverse(X2))) = multiply(multiply(X1,inverse(least_upper_bound(X1,X2))),X2),
inference(step,[status(thm)],[t29133,t666]) ).
cnf(t52142,plain,
inverse(least_upper_bound(inverse(X1),inverse(X2))) = multiply(X1,multiply(inverse(least_upper_bound(X1,X2)),X2)),
inference(step,[status(thm)],[t52141,t20]) ).
cnf(t29665,plain,
multiply(X1,multiply(inverse(least_upper_bound(X1,X2)),X2)) = inverse(least_upper_bound(inverse(X1),inverse(X2))),
inference(orient,[status(thm)],[t52142]) ).
cnf(t52398,plain,
inverse(greatest_lower_bound(X1,X2)) = inverse(inverse(least_upper_bound(inverse(X1),inverse(X2)))),
inference(step,[status(thm)],[t52397,t29665]) ).
cnf(t52399,plain,
inverse(greatest_lower_bound(X1,X2)) = least_upper_bound(inverse(X1),inverse(X2)),
inference(step,[status(thm)],[t52398,t165]) ).
cnf(t51010,plain,
least_upper_bound(inverse(X1),inverse(X2)) = inverse(greatest_lower_bound(X1,X2)),
inference(orient,[status(thm)],[t52399]) ).
cnf(t51031,plain,
inverse(greatest_lower_bound(inverse(X1),X2)) = least_upper_bound(X1,inverse(X2)),
inference(cp,[status(thm)],[t51010,t165]) ).
cnf(t52421,plain,
inverse(greatest_lower_bound(X2,inverse(X1))) = least_upper_bound(X1,inverse(X2)),
inference(step,[status(thm)],[t51031,t71]) ).
cnf(t51169,plain,
inverse(greatest_lower_bound(X1,inverse(X2))) = least_upper_bound(X2,inverse(X1)),
inference(orient,[status(thm)],[t52421]) ).
cnf(t52426,plain,
multiply(X1,multiply(inverse(greatest_lower_bound(X1,X2)),X2)) = least_upper_bound(X2,inverse(inverse(X1))),
inference(step,[status(thm)],[t28529,t51169]) ).
cnf(t52427,plain,
multiply(X1,multiply(inverse(greatest_lower_bound(X1,X2)),X2)) = least_upper_bound(X2,X1),
inference(step,[status(thm)],[t52426,t165]) ).
cnf(t52428,plain,
multiply(X1,multiply(inverse(greatest_lower_bound(X1,X2)),X2)) = least_upper_bound(X1,X2),
inference(step,[status(thm)],[t52427,t45]) ).
cnf(t51172,plain,
multiply(X1,multiply(inverse(greatest_lower_bound(X1,X2)),X2)) = least_upper_bound(X1,X2),
inference(orient,[status(thm)],[t52428]) ).
cnf(goal_0,negated_conjecture,
multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != least_upper_bound(a,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
least_upper_bound(a,b) != least_upper_bound(a,b),
inference(rw,[status(thm)],[goal_0,t51172]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP180-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n010.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 14:01:12 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 34.17/4.77 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 34.17/4.77 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------