%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP183-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 : n003.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:35 PM UTC 2026
% Result : Unsatisfiable 40.64s 5.78s
% Output : CNFRefutation 40.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 81
% Number of leaves : 14
% Syntax : Number of clauses : 248 ( 248 unt; 0 nHn; 6 RR)
% Number of literals : 248 ( 247 equ; 3 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 : 6 ( 6 usr; 2 con; 0-2 aty)
% Number of variables : 445 ( 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(t55916,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)],[t55916]) ).
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(t55917,plain,
multiply(X1,identity) = X1,
inference(step,[status(thm)],[t132,t151]) ).
cnf(t158,plain,
multiply(X1,identity) = X1,
inference(rw,[status(thm)],[t55917]) ).
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(t55918,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t160,t159]) ).
cnf(t165,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t55918]) ).
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(t161,plain,
multiply(X1,greatest_lower_bound(identity,X2)) = greatest_lower_bound(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t23,t159]) ).
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(t55921,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)],[t55921]) ).
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(t55956,plain,
multiply(inverse(X1),greatest_lower_bound(identity,multiply(X1,X2))) = greatest_lower_bound(inverse(X1),X2),
inference(step,[status(thm)],[t219,t71]) ).
cnf(t55957,plain,
multiply(inverse(X1),greatest_lower_bound(identity,multiply(X1,X2))) = greatest_lower_bound(X2,inverse(X1)),
inference(step,[status(thm)],[t55956,t71]) ).
cnf(t1072,plain,
multiply(inverse(X1),greatest_lower_bound(identity,multiply(X1,X2))) = greatest_lower_bound(X2,inverse(X1)),
inference(orient,[status(thm)],[t55957]) ).
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(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(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(t55938,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)],[t55938]) ).
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(t55958,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(t55959,plain,
greatest_lower_bound(inverse(X2),least_upper_bound(X1,inverse(X2))) = multiply(inverse(X2),identity),
inference(step,[status(thm)],[t55958,t19]) ).
cnf(t55960,plain,
greatest_lower_bound(inverse(X2),least_upper_bound(X1,inverse(X2))) = inverse(X2),
inference(step,[status(thm)],[t55959,t159]) ).
cnf(t1126,plain,
greatest_lower_bound(inverse(X1),least_upper_bound(X2,inverse(X1))) = inverse(X1),
inference(orient,[status(thm)],[t55960]) ).
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(t55936,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)],[t55936]) ).
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(t55965,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(t55966,plain,
greatest_lower_bound(X1,inverse(least_upper_bound(X2,inverse(X1)))) = inverse(least_upper_bound(X2,inverse(X1))),
inference(step,[status(thm)],[t55965,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)],[t55966]) ).
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(t55968,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)],[t55968]) ).
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(t55981,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)],[t55981]) ).
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(t55945,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(t55946,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)],[t55945,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)],[t55946]) ).
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(t56549,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(t56550,plain,
multiply(least_upper_bound(X1,multiply(X2,X3)),inverse(X3)) = least_upper_bound(X2,multiply(X1,inverse(X3))),
inference(step,[status(thm)],[t56549,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)],[t56550]) ).
cnf(t163,plain,
multiply(X1,least_upper_bound(identity,X2)) = least_upper_bound(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t21,t159]) ).
cnf(t55922,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)],[t55922]) ).
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(t55986,plain,
multiply(inverse(X1),least_upper_bound(identity,multiply(X1,X2))) = least_upper_bound(inverse(X1),X2),
inference(step,[status(thm)],[t231,t45]) ).
cnf(t55987,plain,
multiply(inverse(X1),least_upper_bound(identity,multiply(X1,X2))) = least_upper_bound(X2,inverse(X1)),
inference(step,[status(thm)],[t55986,t45]) ).
cnf(t1452,plain,
multiply(inverse(X1),least_upper_bound(identity,multiply(X1,X2))) = least_upper_bound(X2,inverse(X1)),
inference(orient,[status(thm)],[t55987]) ).
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(t55937,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)],[t55937]) ).
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(t55988,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(t55989,plain,
least_upper_bound(inverse(X2),greatest_lower_bound(X1,inverse(X2))) = multiply(inverse(X2),identity),
inference(step,[status(thm)],[t55988,t17]) ).
cnf(t55990,plain,
least_upper_bound(inverse(X2),greatest_lower_bound(X1,inverse(X2))) = inverse(X2),
inference(step,[status(thm)],[t55989,t159]) ).
cnf(t1508,plain,
least_upper_bound(inverse(X1),greatest_lower_bound(X2,inverse(X1))) = inverse(X1),
inference(orient,[status(thm)],[t55990]) ).
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(t55969,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)],[t55969]) ).
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(t55974,plain,
inverse(X1) = greatest_lower_bound(inverse(greatest_lower_bound(X1,X2)),inverse(X1)),
inference(step,[status(thm)],[t1251,t17]) ).
cnf(t55975,plain,
inverse(X1) = greatest_lower_bound(inverse(X1),inverse(greatest_lower_bound(X1,X2))),
inference(step,[status(thm)],[t55974,t71]) ).
cnf(t1276,plain,
greatest_lower_bound(inverse(X1),inverse(greatest_lower_bound(X1,X2))) = inverse(X1),
inference(orient,[status(thm)],[t55975]) ).
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(t55994,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)],[t55994]) ).
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(t55997,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)],[t55997]) ).
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(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(t55947,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)],[t55947]) ).
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(t56003,plain,
identity = least_upper_bound(identity,inverse(multiply(inverse(X2),least_upper_bound(X1,X2)))),
inference(step,[status(thm)],[t1588,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(t56004,plain,
identity = least_upper_bound(identity,multiply(inverse(least_upper_bound(X1,X2)),X2)),
inference(step,[status(thm)],[t56003,t685]) ).
cnf(t1773,plain,
least_upper_bound(identity,multiply(inverse(least_upper_bound(X1,X2)),X2)) = identity,
inference(orient,[status(thm)],[t56004]) ).
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(t55910,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)],[t55910]) ).
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(t55939,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(t55940,plain,
least_upper_bound(X1,least_upper_bound(X3,greatest_lower_bound(X1,X2))) = least_upper_bound(X3,X1),
inference(step,[status(thm)],[t55939,t45]) ).
cnf(t55941,plain,
least_upper_bound(X1,least_upper_bound(X3,greatest_lower_bound(X1,X2))) = least_upper_bound(X1,X3),
inference(step,[status(thm)],[t55940,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)],[t55941]) ).
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(t31,plain,
multiply(greatest_lower_bound(identity,X1),X2) = greatest_lower_bound(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t30,t15]) ).
cnf(t55920,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)],[t55920]) ).
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(t55919,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)],[t55919]) ).
cnf(t56064,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)],[t56064]) ).
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(t56751,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)],[t56751]) ).
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(t55934,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)],[t55934]) ).
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(t56752,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)],[t56752]) ).
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(t56756,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(t56757,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)],[t56756,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)],[t56757]) ).
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(t56758,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(t56759,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)],[t56758,t165]) ).
cnf(t56760,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)],[t56759,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(t55911,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)],[t55911]) ).
cnf(t56761,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)],[t56760,t75]) ).
cnf(t56762,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)],[t56761,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(t56001,plain,
identity = least_upper_bound(identity,inverse(multiply(X2,least_upper_bound(X1,inverse(X2))))),
inference(step,[status(thm)],[t1586,t647]) ).
cnf(t56002,plain,
identity = least_upper_bound(identity,inverse(least_upper_bound(identity,multiply(X2,X1)))),
inference(step,[status(thm)],[t56001,t490]) ).
cnf(t1725,plain,
least_upper_bound(identity,inverse(least_upper_bound(identity,multiply(X1,X2)))) = identity,
inference(orient,[status(thm)],[t56002]) ).
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(t56023,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)],[t56023]) ).
cnf(t56763,plain,
greatest_lower_bound(X1,identity) = greatest_lower_bound(X1,inverse(least_upper_bound(identity,inverse(X1)))),
inference(step,[status(thm)],[t56762,t1983]) ).
cnf(t56764,plain,
greatest_lower_bound(X1,identity) = inverse(least_upper_bound(identity,inverse(X1))),
inference(step,[status(thm)],[t56763,t1169]) ).
cnf(t47408,plain,
inverse(least_upper_bound(identity,inverse(X1))) = greatest_lower_bound(X1,identity),
inference(orient,[status(thm)],[t56764]) ).
cnf(t47463,plain,
least_upper_bound(identity,inverse(X1)) = inverse(greatest_lower_bound(X1,identity)),
inference(cp,[status(thm)],[t165,t47408]) ).
cnf(t47971,plain,
inverse(greatest_lower_bound(X1,identity)) = least_upper_bound(identity,inverse(X1)),
inference(orient,[status(thm)],[t47463]) ).
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(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(t56857,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(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(t56858,plain,
multiply(greatest_lower_bound(X2,X1),inverse(X2)) = inverse(least_upper_bound(identity,multiply(X2,inverse(X1)))),
inference(step,[status(thm)],[t56857,t23711]) ).
cnf(t56859,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X2)) = inverse(least_upper_bound(identity,multiply(X2,inverse(X1)))),
inference(step,[status(thm)],[t56858,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(t56860,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X2)) = inverse(multiply(least_upper_bound(X1,X2),inverse(X1))),
inference(step,[status(thm)],[t56859,t28916]) ).
cnf(t56861,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X2)) = multiply(X1,inverse(least_upper_bound(X1,X2))),
inference(step,[status(thm)],[t56860,t666]) ).
cnf(t50661,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X2)) = multiply(X1,inverse(least_upper_bound(X1,X2))),
inference(orient,[status(thm)],[t56861]) ).
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(t56862,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(t56863,plain,
inverse(greatest_lower_bound(X1,X2)) = inverse(multiply(X1,multiply(inverse(least_upper_bound(X1,X2)),X2))),
inference(step,[status(thm)],[t56862,t20]) ).
cnf(t644,plain,
inverse(X1) = multiply(inverse(multiply(X2,X1)),inverse(inverse(X2))),
inference(cp,[status(thm)],[t616,t616]) ).
cnf(t55948,plain,
inverse(X1) = inverse(multiply(inverse(X2),multiply(X2,X1))),
inference(step,[status(thm)],[t644,t647]) ).
cnf(t55949,plain,
inverse(X1) = multiply(inverse(multiply(X2,X1)),X2),
inference(step,[status(thm)],[t55948,t685]) ).
cnf(t705,plain,
multiply(inverse(multiply(X1,X2)),X1) = inverse(X2),
inference(orient,[status(thm)],[t55949]) ).
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(t56607,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(t56608,plain,
inverse(least_upper_bound(inverse(X1),inverse(X2))) = multiply(X1,multiply(inverse(least_upper_bound(X1,X2)),X2)),
inference(step,[status(thm)],[t56607,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)],[t56608]) ).
cnf(t56864,plain,
inverse(greatest_lower_bound(X1,X2)) = inverse(inverse(least_upper_bound(inverse(X1),inverse(X2)))),
inference(step,[status(thm)],[t56863,t29665]) ).
cnf(t56865,plain,
inverse(greatest_lower_bound(X1,X2)) = least_upper_bound(inverse(X1),inverse(X2)),
inference(step,[status(thm)],[t56864,t165]) ).
cnf(t51010,plain,
least_upper_bound(inverse(X1),inverse(X2)) = inverse(greatest_lower_bound(X1,X2)),
inference(orient,[status(thm)],[t56865]) ).
cnf(t51031,plain,
inverse(greatest_lower_bound(inverse(X1),X2)) = least_upper_bound(X1,inverse(X2)),
inference(cp,[status(thm)],[t51010,t165]) ).
cnf(t56887,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)],[t56887]) ).
cnf(t51230,plain,
greatest_lower_bound(X1,inverse(X2)) = inverse(least_upper_bound(X2,inverse(X1))),
inference(cp,[status(thm)],[t165,t51169]) ).
cnf(t51444,plain,
inverse(least_upper_bound(X1,inverse(X2))) = greatest_lower_bound(X2,inverse(X1)),
inference(orient,[status(thm)],[t51230]) ).
cnf(t47455,plain,
greatest_lower_bound(inverse(X1),identity) = inverse(least_upper_bound(identity,X1)),
inference(cp,[status(thm)],[t47408,t165]) ).
cnf(t56782,plain,
greatest_lower_bound(identity,inverse(X1)) = inverse(least_upper_bound(identity,X1)),
inference(step,[status(thm)],[t47455,t71]) ).
cnf(t56783,plain,
greatest_lower_bound(identity,inverse(X1)) = inverse(least_upper_bound(X1,identity)),
inference(step,[status(thm)],[t56782,t45]) ).
cnf(t47723,plain,
inverse(least_upper_bound(X1,identity)) = greatest_lower_bound(identity,inverse(X1)),
inference(orient,[status(thm)],[t56783]) ).
cnf(t51470,plain,
greatest_lower_bound(least_upper_bound(X1,identity),inverse(X2)) = inverse(least_upper_bound(X2,greatest_lower_bound(identity,inverse(X1)))),
inference(cp,[status(thm)],[t51444,t47723]) ).
cnf(t56971,plain,
greatest_lower_bound(inverse(X2),least_upper_bound(X1,identity)) = inverse(least_upper_bound(X2,greatest_lower_bound(identity,inverse(X1)))),
inference(step,[status(thm)],[t51470,t71]) ).
cnf(t55555,plain,
inverse(least_upper_bound(X1,greatest_lower_bound(identity,inverse(X2)))) = greatest_lower_bound(inverse(X1),least_upper_bound(X2,identity)),
inference(orient,[status(thm)],[t56971]) ).
cnf(t193,plain,
multiply(least_upper_bound(X1,identity),inverse(X1)) = least_upper_bound(inverse(X1),identity),
inference(cp,[status(thm)],[t189,t168]) ).
cnf(t55931,plain,
multiply(least_upper_bound(X1,identity),inverse(X1)) = least_upper_bound(identity,inverse(X1)),
inference(step,[status(thm)],[t193,t45]) ).
cnf(t371,plain,
multiply(least_upper_bound(X1,identity),inverse(X1)) = least_upper_bound(identity,inverse(X1)),
inference(orient,[status(thm)],[t55931]) ).
cnf(t669,plain,
multiply(X1,inverse(least_upper_bound(X1,identity))) = inverse(least_upper_bound(identity,inverse(X1))),
inference(cp,[status(thm)],[t666,t371]) ).
cnf(t731,plain,
multiply(X1,inverse(least_upper_bound(X1,identity))) = inverse(least_upper_bound(identity,inverse(X1))),
inference(orient,[status(thm)],[t669]) ).
cnf(t738,plain,
multiply(least_upper_bound(X1,identity),inverse(least_upper_bound(X1,identity))) = least_upper_bound(inverse(least_upper_bound(X1,identity)),inverse(least_upper_bound(identity,inverse(X1)))),
inference(cp,[status(thm)],[t189,t731]) ).
cnf(t56102,plain,
identity = least_upper_bound(inverse(least_upper_bound(X1,identity)),inverse(least_upper_bound(identity,inverse(X1)))),
inference(step,[status(thm)],[t738,t168]) ).
cnf(t6501,plain,
least_upper_bound(inverse(least_upper_bound(X1,identity)),inverse(least_upper_bound(identity,inverse(X1)))) = identity,
inference(orient,[status(thm)],[t56102]) ).
cnf(t56774,plain,
least_upper_bound(inverse(least_upper_bound(X1,identity)),greatest_lower_bound(X1,identity)) = identity,
inference(step,[status(thm)],[t6501,t47408]) ).
cnf(t47717,plain,
least_upper_bound(inverse(least_upper_bound(X1,identity)),greatest_lower_bound(X1,identity)) = identity,
inference(rw,[status(thm)],[t56774]) ).
cnf(t56843,plain,
least_upper_bound(greatest_lower_bound(X1,identity),inverse(least_upper_bound(X1,identity))) = identity,
inference(step,[status(thm)],[t47717,t45]) ).
cnf(t56844,plain,
least_upper_bound(greatest_lower_bound(X1,identity),greatest_lower_bound(identity,inverse(X1))) = identity,
inference(step,[status(thm)],[t56843,t47723]) ).
cnf(t49590,plain,
least_upper_bound(greatest_lower_bound(X1,identity),greatest_lower_bound(identity,inverse(X1))) = identity,
inference(orient,[status(thm)],[t56844]) ).
cnf(t55561,plain,
greatest_lower_bound(inverse(greatest_lower_bound(X1,identity)),least_upper_bound(X1,identity)) = inverse(identity),
inference(cp,[status(thm)],[t55555,t49590]) ).
cnf(t56972,plain,
greatest_lower_bound(least_upper_bound(X1,identity),inverse(greatest_lower_bound(X1,identity))) = inverse(identity),
inference(step,[status(thm)],[t55561,t71]) ).
cnf(t56973,plain,
greatest_lower_bound(least_upper_bound(X1,identity),least_upper_bound(identity,inverse(X1))) = inverse(identity),
inference(step,[status(thm)],[t56972,t47971]) ).
cnf(t115,plain,
X1 = multiply(inverse(identity),X1),
inference(cp,[status(thm)],[t113,t15]) ).
cnf(t126,plain,
multiply(inverse(identity),X1) = X1,
inference(orient,[status(thm)],[t115]) ).
cnf(t127,plain,
X1 = multiply(inverse(inverse(identity)),X1),
inference(cp,[status(thm)],[t113,t126]) ).
cnf(t143,plain,
multiply(inverse(inverse(identity)),X1) = X1,
inference(orient,[status(thm)],[t127]) ).
cnf(t144,plain,
inverse(identity) = identity,
inference(cp,[status(thm)],[t143,t35]) ).
cnf(t150,plain,
inverse(identity) = identity,
inference(orient,[status(thm)],[t144]) ).
cnf(t56974,plain,
greatest_lower_bound(least_upper_bound(X1,identity),least_upper_bound(identity,inverse(X1))) = identity,
inference(step,[status(thm)],[t56973,t150]) ).
cnf(t55821,plain,
greatest_lower_bound(least_upper_bound(X1,identity),least_upper_bound(identity,inverse(X1))) = identity,
inference(orient,[status(thm)],[t56974]) ).
cnf(goal_0,negated_conjecture,
greatest_lower_bound(least_upper_bound(a,identity),inverse(greatest_lower_bound(a,identity))) != identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
greatest_lower_bound(least_upper_bound(a,identity),least_upper_bound(identity,inverse(a))) != identity,
inference(rw,[status(thm)],[goal_0,t47971]) ).
cnf(g0_1,plain,
identity != identity,
inference(rw,[status(thm)],[g0_0,t55821]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP183-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.13/0.36 % Computer : n003.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8046.5625MB
% 0.13/0.36 % OS : Linux 6.8.0-71-generic
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Wed Sep 23 14:03:49 UTC 2026
% 0.13/0.37 % CPUTime :
% 0.13/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 40.64/5.78 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 40.64/5.78 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------