%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP180-2 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n001.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 35.64s 5.06s
% Output : CNFRefutation 35.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 89
% Number of leaves : 17
% Syntax : Number of clauses : 280 ( 280 unt; 0 nHn; 5 RR)
% Number of literals : 280 ( 279 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 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 : 495 ( 43 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t10,axiom,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t50,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t10]) ).
cnf(t2,axiom,
inverse(inverse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t53,plain,
inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(cp,[status(thm)],[t50,t23]) ).
cnf(t182,plain,
inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(orient,[status(thm)],[t53]) ).
cnf(t13,axiom,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t13]) ).
cnf(t5,axiom,
multiply(inverse(X1),X1) = identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t39,plain,
multiply(inverse(X1),X1) = identity,
inference(orient,[status(thm)],[t5]) ).
cnf(t49,plain,
multiply(inverse(X1),multiply(X1,X2)) = multiply(identity,X2),
inference(cp,[status(thm)],[t24,t39]) ).
cnf(t4,axiom,
multiply(identity,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t18,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t52805,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(step,[status(thm)],[t49,t18]) ).
cnf(t155,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(orient,[status(thm)],[t52805]) ).
cnf(t183,plain,
multiply(inverse(multiply(X1,X2)),X1) = inverse(X2),
inference(cp,[status(thm)],[t182,t155]) ).
cnf(t203,plain,
multiply(inverse(multiply(X1,X2)),X1) = inverse(X2),
inference(orient,[status(thm)],[t183]) ).
cnf(t14,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(t27,plain,
greatest_lower_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,greatest_lower_bound(X2,X3)),
inference(orient,[status(thm)],[t14]) ).
cnf(t40,plain,
identity = multiply(X1,inverse(X1)),
inference(cp,[status(thm)],[t39,t23]) ).
cnf(t118,plain,
multiply(X1,inverse(X1)) = identity,
inference(orient,[status(thm)],[t40]) ).
cnf(t124,plain,
multiply(X1,greatest_lower_bound(inverse(X1),X2)) = greatest_lower_bound(identity,multiply(X1,X2)),
inference(cp,[status(thm)],[t27,t118]) ).
cnf(t6,axiom,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t89,plain,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t52825,plain,
multiply(X1,greatest_lower_bound(X2,inverse(X1))) = greatest_lower_bound(identity,multiply(X1,X2)),
inference(step,[status(thm)],[t124,t89]) ).
cnf(t568,plain,
multiply(X1,greatest_lower_bound(X2,inverse(X1))) = greatest_lower_bound(identity,multiply(X1,X2)),
inference(orient,[status(thm)],[t52825]) ).
cnf(t589,plain,
inverse(greatest_lower_bound(X1,inverse(X2))) = multiply(inverse(greatest_lower_bound(identity,multiply(X2,X1))),X2),
inference(cp,[status(thm)],[t203,t568]) ).
cnf(t5265,plain,
multiply(inverse(greatest_lower_bound(identity,multiply(X1,X2))),X1) = inverse(greatest_lower_bound(X2,inverse(X1))),
inference(orient,[status(thm)],[t589]) ).
cnf(t15,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(t34,plain,
greatest_lower_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(greatest_lower_bound(X1,X3),X2),
inference(orient,[status(thm)],[t15]) ).
cnf(t120,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X1)) = greatest_lower_bound(identity,multiply(X2,inverse(X1))),
inference(cp,[status(thm)],[t34,t118]) ).
cnf(t23677,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X1)) = greatest_lower_bound(identity,multiply(X2,inverse(X1))),
inference(orient,[status(thm)],[t120]) ).
cnf(t23876,plain,
inverse(greatest_lower_bound(inverse(X1),inverse(X2))) = multiply(inverse(multiply(greatest_lower_bound(X1,X2),inverse(X1))),X2),
inference(cp,[status(thm)],[t5265,t23677]) ).
cnf(t52,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(cp,[status(thm)],[t50,t23]) ).
cnf(t177,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t52]) ).
cnf(t53517,plain,
inverse(greatest_lower_bound(inverse(X1),inverse(X2))) = multiply(multiply(X1,inverse(greatest_lower_bound(X1,X2))),X2),
inference(step,[status(thm)],[t23876,t177]) ).
cnf(t53518,plain,
inverse(greatest_lower_bound(inverse(X1),inverse(X2))) = multiply(X1,multiply(inverse(greatest_lower_bound(X1,X2)),X2)),
inference(step,[status(thm)],[t53517,t24]) ).
cnf(t29958,plain,
multiply(X1,multiply(inverse(greatest_lower_bound(X1,X2)),X2)) = inverse(greatest_lower_bound(inverse(X1),inverse(X2))),
inference(orient,[status(thm)],[t53518]) ).
cnf(t128,plain,
multiply(X1,multiply(inverse(X1),X2)) = multiply(identity,X2),
inference(cp,[status(thm)],[t24,t118]) ).
cnf(t52806,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(step,[status(thm)],[t128,t18]) ).
cnf(t166,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t52806]) ).
cnf(t168,plain,
inverse(X1) = multiply(X2,inverse(multiply(X1,X2))),
inference(cp,[status(thm)],[t166,t50]) ).
cnf(t190,plain,
multiply(X1,inverse(multiply(X2,X1))) = inverse(X2),
inference(orient,[status(thm)],[t168]) ).
cnf(t0,axiom,
inverse(identity) = identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t115,plain,
inverse(identity) = identity,
inference(orient,[status(thm)],[t0]) ).
cnf(t116,plain,
inverse(multiply(X1,identity)) = multiply(identity,inverse(X1)),
inference(cp,[status(thm)],[t50,t115]) ).
cnf(t52799,plain,
inverse(multiply(X1,identity)) = inverse(X1),
inference(step,[status(thm)],[t116,t18]) ).
cnf(t129,plain,
inverse(multiply(X1,identity)) = inverse(X1),
inference(orient,[status(thm)],[t52799]) ).
cnf(t133,plain,
multiply(X1,identity) = inverse(inverse(X1)),
inference(cp,[status(thm)],[t23,t129]) ).
cnf(t52800,plain,
multiply(X1,identity) = X1,
inference(step,[status(thm)],[t133,t23]) ).
cnf(t134,plain,
multiply(X1,identity) = X1,
inference(orient,[status(thm)],[t52800]) ).
cnf(t135,plain,
multiply(X1,greatest_lower_bound(identity,X2)) = greatest_lower_bound(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t27,t134]) ).
cnf(t52809,plain,
multiply(X1,greatest_lower_bound(X2,identity)) = greatest_lower_bound(X1,multiply(X1,X2)),
inference(step,[status(thm)],[t135,t89]) ).
cnf(t244,plain,
greatest_lower_bound(X1,multiply(X1,X2)) = multiply(X1,greatest_lower_bound(X2,identity)),
inference(orient,[status(thm)],[t52809]) ).
cnf(t252,plain,
multiply(inverse(X1),greatest_lower_bound(multiply(X1,X2),identity)) = greatest_lower_bound(inverse(X1),X2),
inference(cp,[status(thm)],[t244,t155]) ).
cnf(t52900,plain,
multiply(inverse(X1),greatest_lower_bound(identity,multiply(X1,X2))) = greatest_lower_bound(inverse(X1),X2),
inference(step,[status(thm)],[t252,t89]) ).
cnf(t52901,plain,
multiply(inverse(X1),greatest_lower_bound(identity,multiply(X1,X2))) = greatest_lower_bound(X2,inverse(X1)),
inference(step,[status(thm)],[t52900,t89]) ).
cnf(t2065,plain,
multiply(inverse(X1),greatest_lower_bound(identity,multiply(X1,X2))) = greatest_lower_bound(X2,inverse(X1)),
inference(orient,[status(thm)],[t52901]) ).
cnf(t16,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(t25,plain,
least_upper_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,least_upper_bound(X2,X3)),
inference(orient,[status(thm)],[t16]) ).
cnf(t126,plain,
multiply(X1,least_upper_bound(inverse(X1),X2)) = least_upper_bound(identity,multiply(X1,X2)),
inference(cp,[status(thm)],[t25,t118]) ).
cnf(t8,axiom,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t63,plain,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t52826,plain,
multiply(X1,least_upper_bound(X2,inverse(X1))) = least_upper_bound(identity,multiply(X1,X2)),
inference(step,[status(thm)],[t126,t63]) ).
cnf(t592,plain,
multiply(X1,least_upper_bound(X2,inverse(X1))) = least_upper_bound(identity,multiply(X1,X2)),
inference(orient,[status(thm)],[t52826]) ).
cnf(t2074,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)],[t2065,t592]) ).
cnf(t52902,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)],[t2074,t89]) ).
cnf(t7,axiom,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t52903,plain,
greatest_lower_bound(inverse(X2),least_upper_bound(X1,inverse(X2))) = multiply(inverse(X2),identity),
inference(step,[status(thm)],[t52902,t22]) ).
cnf(t52904,plain,
greatest_lower_bound(inverse(X2),least_upper_bound(X1,inverse(X2))) = inverse(X2),
inference(step,[status(thm)],[t52903,t134]) ).
cnf(t2136,plain,
greatest_lower_bound(inverse(X1),least_upper_bound(X2,inverse(X1))) = inverse(X1),
inference(orient,[status(thm)],[t52904]) ).
cnf(t9,axiom,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t17,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(t28,plain,
least_upper_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(least_upper_bound(X1,X3),X2),
inference(orient,[status(thm)],[t17]) ).
cnf(t43,plain,
multiply(least_upper_bound(inverse(X1),X2),X1) = least_upper_bound(identity,multiply(X2,X1)),
inference(cp,[status(thm)],[t28,t39]) ).
cnf(t52824,plain,
multiply(least_upper_bound(X2,inverse(X1)),X1) = least_upper_bound(identity,multiply(X2,X1)),
inference(step,[status(thm)],[t43,t63]) ).
cnf(t546,plain,
multiply(least_upper_bound(X1,inverse(X2)),X2) = least_upper_bound(identity,multiply(X1,X2)),
inference(orient,[status(thm)],[t52824]) ).
cnf(t2090,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)],[t2065,t546]) ).
cnf(t52905,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)],[t2090,t22]) ).
cnf(t52906,plain,
greatest_lower_bound(X1,inverse(least_upper_bound(X2,inverse(X1)))) = inverse(least_upper_bound(X2,inverse(X1))),
inference(step,[status(thm)],[t52905,t134]) ).
cnf(t2155,plain,
greatest_lower_bound(X1,inverse(least_upper_bound(X2,inverse(X1)))) = inverse(least_upper_bound(X2,inverse(X1))),
inference(orient,[status(thm)],[t52906]) ).
cnf(t2168,plain,
X1 = least_upper_bound(X1,inverse(least_upper_bound(X2,inverse(X1)))),
inference(cp,[status(thm)],[t20,t2155]) ).
cnf(t2177,plain,
least_upper_bound(X1,inverse(least_upper_bound(X2,inverse(X1)))) = X1,
inference(orient,[status(thm)],[t2168]) ).
cnf(t2188,plain,
inverse(X1) = least_upper_bound(inverse(X1),inverse(least_upper_bound(X2,X1))),
inference(cp,[status(thm)],[t2177,t23]) ).
cnf(t52907,plain,
inverse(X1) = least_upper_bound(inverse(X1),inverse(least_upper_bound(X1,X2))),
inference(step,[status(thm)],[t2188,t63]) ).
cnf(t2198,plain,
least_upper_bound(inverse(X1),inverse(least_upper_bound(X1,X2))) = inverse(X1),
inference(orient,[status(thm)],[t52907]) ).
cnf(t2213,plain,
inverse(least_upper_bound(X1,X2)) = greatest_lower_bound(inverse(least_upper_bound(X1,X2)),inverse(X1)),
inference(cp,[status(thm)],[t2136,t2198]) ).
cnf(t52914,plain,
inverse(least_upper_bound(X1,X2)) = greatest_lower_bound(inverse(X1),inverse(least_upper_bound(X1,X2))),
inference(step,[status(thm)],[t2213,t89]) ).
cnf(t2338,plain,
greatest_lower_bound(inverse(X1),inverse(least_upper_bound(X1,X2))) = inverse(least_upper_bound(X1,X2)),
inference(orient,[status(thm)],[t52914]) ).
cnf(t30,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)],[t28,t24]) ).
cnf(t52827,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)],[t30,t63]) ).
cnf(t52828,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)],[t52827,t63]) ).
cnf(t616,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)],[t52828]) ).
cnf(t650,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)],[t616,t118]) ).
cnf(t53473,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)],[t650,t63]) ).
cnf(t53474,plain,
multiply(least_upper_bound(X1,multiply(X2,X3)),inverse(X3)) = least_upper_bound(X2,multiply(X1,inverse(X3))),
inference(step,[status(thm)],[t53473,t134]) ).
cnf(t26487,plain,
multiply(least_upper_bound(X1,multiply(X2,X3)),inverse(X3)) = least_upper_bound(X2,multiply(X1,inverse(X3))),
inference(orient,[status(thm)],[t53474]) ).
cnf(t137,plain,
multiply(X1,least_upper_bound(identity,X2)) = least_upper_bound(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t25,t134]) ).
cnf(t52810,plain,
multiply(X1,least_upper_bound(X2,identity)) = least_upper_bound(X1,multiply(X1,X2)),
inference(step,[status(thm)],[t137,t63]) ).
cnf(t259,plain,
least_upper_bound(X1,multiply(X1,X2)) = multiply(X1,least_upper_bound(X2,identity)),
inference(orient,[status(thm)],[t52810]) ).
cnf(t267,plain,
multiply(inverse(X1),least_upper_bound(multiply(X1,X2),identity)) = least_upper_bound(inverse(X1),X2),
inference(cp,[status(thm)],[t259,t155]) ).
cnf(t52924,plain,
multiply(inverse(X1),least_upper_bound(identity,multiply(X1,X2))) = least_upper_bound(inverse(X1),X2),
inference(step,[status(thm)],[t267,t63]) ).
cnf(t52925,plain,
multiply(inverse(X1),least_upper_bound(identity,multiply(X1,X2))) = least_upper_bound(X2,inverse(X1)),
inference(step,[status(thm)],[t52924,t63]) ).
cnf(t2569,plain,
multiply(inverse(X1),least_upper_bound(identity,multiply(X1,X2))) = least_upper_bound(X2,inverse(X1)),
inference(orient,[status(thm)],[t52925]) ).
cnf(t2582,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)],[t2569,t568]) ).
cnf(t52926,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)],[t2582,t63]) ).
cnf(t52927,plain,
least_upper_bound(inverse(X2),greatest_lower_bound(X1,inverse(X2))) = multiply(inverse(X2),identity),
inference(step,[status(thm)],[t52926,t20]) ).
cnf(t52928,plain,
least_upper_bound(inverse(X2),greatest_lower_bound(X1,inverse(X2))) = inverse(X2),
inference(step,[status(thm)],[t52927,t134]) ).
cnf(t2646,plain,
least_upper_bound(inverse(X1),greatest_lower_bound(X2,inverse(X1))) = inverse(X1),
inference(orient,[status(thm)],[t52928]) ).
cnf(t35,plain,
multiply(greatest_lower_bound(identity,X1),X2) = greatest_lower_bound(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t34,t18]) ).
cnf(t52808,plain,
multiply(greatest_lower_bound(X1,identity),X2) = greatest_lower_bound(X2,multiply(X1,X2)),
inference(step,[status(thm)],[t35,t89]) ).
cnf(t229,plain,
greatest_lower_bound(X1,multiply(X2,X1)) = multiply(greatest_lower_bound(X2,identity),X1),
inference(orient,[status(thm)],[t52808]) ).
cnf(t235,plain,
multiply(greatest_lower_bound(inverse(multiply(X1,X2)),identity),X1) = greatest_lower_bound(X1,inverse(X2)),
inference(cp,[status(thm)],[t229,t203]) ).
cnf(t52851,plain,
multiply(greatest_lower_bound(identity,inverse(multiply(X1,X2))),X1) = greatest_lower_bound(X1,inverse(X2)),
inference(step,[status(thm)],[t235,t89]) ).
cnf(t1324,plain,
multiply(greatest_lower_bound(identity,inverse(multiply(X1,X2))),X1) = greatest_lower_bound(X1,inverse(X2)),
inference(orient,[status(thm)],[t52851]) ).
cnf(t249,plain,
multiply(X1,greatest_lower_bound(inverse(multiply(X2,X1)),identity)) = greatest_lower_bound(X1,inverse(X2)),
inference(cp,[status(thm)],[t244,t190]) ).
cnf(t52861,plain,
multiply(X1,greatest_lower_bound(identity,inverse(multiply(X2,X1)))) = greatest_lower_bound(X1,inverse(X2)),
inference(step,[status(thm)],[t249,t89]) ).
cnf(t1480,plain,
multiply(X1,greatest_lower_bound(identity,inverse(multiply(X2,X1)))) = greatest_lower_bound(X1,inverse(X2)),
inference(orient,[status(thm)],[t52861]) ).
cnf(t1529,plain,
greatest_lower_bound(identity,inverse(multiply(X1,inverse(X2)))) = multiply(X2,greatest_lower_bound(inverse(X2),inverse(X1))),
inference(cp,[status(thm)],[t166,t1480]) ).
cnf(t52889,plain,
greatest_lower_bound(identity,multiply(X2,inverse(X1))) = multiply(X2,greatest_lower_bound(inverse(X2),inverse(X1))),
inference(step,[status(thm)],[t1529,t177]) ).
cnf(t1821,plain,
multiply(X1,greatest_lower_bound(inverse(X1),inverse(X2))) = greatest_lower_bound(identity,multiply(X1,inverse(X2))),
inference(orient,[status(thm)],[t52889]) ).
cnf(t1858,plain,
greatest_lower_bound(X1,inverse(greatest_lower_bound(inverse(X1),inverse(X2)))) = multiply(greatest_lower_bound(identity,inverse(greatest_lower_bound(identity,multiply(X1,inverse(X2))))),X1),
inference(cp,[status(thm)],[t1324,t1821]) ).
cnf(t1519,plain,
greatest_lower_bound(identity,inverse(multiply(X1,X2))) = multiply(inverse(X2),greatest_lower_bound(X2,inverse(X1))),
inference(cp,[status(thm)],[t155,t1480]) ).
cnf(t1546,plain,
multiply(inverse(X1),greatest_lower_bound(X1,inverse(X2))) = greatest_lower_bound(identity,inverse(multiply(X2,X1))),
inference(orient,[status(thm)],[t1519]) ).
cnf(t29,plain,
multiply(least_upper_bound(identity,X1),X2) = least_upper_bound(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t28,t18]) ).
cnf(t52807,plain,
multiply(least_upper_bound(X1,identity),X2) = least_upper_bound(X2,multiply(X1,X2)),
inference(step,[status(thm)],[t29,t63]) ).
cnf(t214,plain,
least_upper_bound(X1,multiply(X2,X1)) = multiply(least_upper_bound(X2,identity),X1),
inference(orient,[status(thm)],[t52807]) ).
cnf(t220,plain,
multiply(least_upper_bound(inverse(multiply(X1,X2)),identity),X1) = least_upper_bound(X1,inverse(X2)),
inference(cp,[status(thm)],[t214,t203]) ).
cnf(t52841,plain,
multiply(least_upper_bound(identity,inverse(multiply(X1,X2))),X1) = least_upper_bound(X1,inverse(X2)),
inference(step,[status(thm)],[t220,t63]) ).
cnf(t1176,plain,
multiply(least_upper_bound(identity,inverse(multiply(X1,X2))),X1) = least_upper_bound(X1,inverse(X2)),
inference(orient,[status(thm)],[t52841]) ).
cnf(t251,plain,
multiply(inverse(X1),greatest_lower_bound(X1,identity)) = greatest_lower_bound(inverse(X1),identity),
inference(cp,[status(thm)],[t244,t39]) ).
cnf(t52821,plain,
multiply(inverse(X1),greatest_lower_bound(X1,identity)) = greatest_lower_bound(identity,inverse(X1)),
inference(step,[status(thm)],[t251,t89]) ).
cnf(t484,plain,
multiply(inverse(X1),greatest_lower_bound(X1,identity)) = greatest_lower_bound(identity,inverse(X1)),
inference(orient,[status(thm)],[t52821]) ).
cnf(t503,plain,
multiply(inverse(greatest_lower_bound(X1,identity)),X1) = inverse(greatest_lower_bound(identity,inverse(X1))),
inference(cp,[status(thm)],[t182,t484]) ).
cnf(t711,plain,
multiply(inverse(greatest_lower_bound(X1,identity)),X1) = inverse(greatest_lower_bound(identity,inverse(X1))),
inference(orient,[status(thm)],[t503]) ).
cnf(t1190,plain,
least_upper_bound(inverse(greatest_lower_bound(X1,identity)),inverse(X1)) = multiply(least_upper_bound(identity,inverse(inverse(greatest_lower_bound(identity,inverse(X1))))),inverse(greatest_lower_bound(X1,identity))),
inference(cp,[status(thm)],[t1176,t711]) ).
cnf(t52842,plain,
least_upper_bound(inverse(X1),inverse(greatest_lower_bound(X1,identity))) = multiply(least_upper_bound(identity,inverse(inverse(greatest_lower_bound(identity,inverse(X1))))),inverse(greatest_lower_bound(X1,identity))),
inference(step,[status(thm)],[t1190,t63]) ).
cnf(t52843,plain,
least_upper_bound(inverse(X1),inverse(greatest_lower_bound(X1,identity))) = multiply(least_upper_bound(identity,greatest_lower_bound(identity,inverse(X1))),inverse(greatest_lower_bound(X1,identity))),
inference(step,[status(thm)],[t52842,t23]) ).
cnf(t52844,plain,
least_upper_bound(inverse(X1),inverse(greatest_lower_bound(X1,identity))) = multiply(identity,inverse(greatest_lower_bound(X1,identity))),
inference(step,[status(thm)],[t52843,t20]) ).
cnf(t52845,plain,
least_upper_bound(inverse(X1),inverse(greatest_lower_bound(X1,identity))) = inverse(greatest_lower_bound(X1,identity)),
inference(step,[status(thm)],[t52844,t18]) ).
cnf(t1236,plain,
least_upper_bound(inverse(X1),inverse(greatest_lower_bound(X1,identity))) = inverse(greatest_lower_bound(X1,identity)),
inference(orient,[status(thm)],[t52845]) ).
cnf(t1242,plain,
inverse(X1) = greatest_lower_bound(inverse(X1),inverse(greatest_lower_bound(X1,identity))),
inference(cp,[status(thm)],[t22,t1236]) ).
cnf(t1246,plain,
greatest_lower_bound(inverse(X1),inverse(greatest_lower_bound(X1,identity))) = inverse(X1),
inference(orient,[status(thm)],[t1242]) ).
cnf(t1553,plain,
greatest_lower_bound(identity,inverse(multiply(greatest_lower_bound(X1,identity),inverse(X1)))) = multiply(inverse(inverse(X1)),inverse(X1)),
inference(cp,[status(thm)],[t1546,t1246]) ).
cnf(t52864,plain,
greatest_lower_bound(identity,multiply(X1,inverse(greatest_lower_bound(X1,identity)))) = multiply(inverse(inverse(X1)),inverse(X1)),
inference(step,[status(thm)],[t1553,t177]) ).
cnf(t232,plain,
multiply(greatest_lower_bound(X1,identity),inverse(X1)) = greatest_lower_bound(inverse(X1),identity),
inference(cp,[status(thm)],[t229,t118]) ).
cnf(t52820,plain,
multiply(greatest_lower_bound(X1,identity),inverse(X1)) = greatest_lower_bound(identity,inverse(X1)),
inference(step,[status(thm)],[t232,t89]) ).
cnf(t463,plain,
multiply(greatest_lower_bound(X1,identity),inverse(X1)) = greatest_lower_bound(identity,inverse(X1)),
inference(orient,[status(thm)],[t52820]) ).
cnf(t483,plain,
multiply(X1,inverse(greatest_lower_bound(X1,identity))) = inverse(greatest_lower_bound(identity,inverse(X1))),
inference(cp,[status(thm)],[t177,t463]) ).
cnf(t689,plain,
multiply(X1,inverse(greatest_lower_bound(X1,identity))) = inverse(greatest_lower_bound(identity,inverse(X1))),
inference(orient,[status(thm)],[t483]) ).
cnf(t52865,plain,
greatest_lower_bound(identity,inverse(greatest_lower_bound(identity,inverse(X1)))) = multiply(inverse(inverse(X1)),inverse(X1)),
inference(step,[status(thm)],[t52864,t689]) ).
cnf(t52866,plain,
greatest_lower_bound(identity,inverse(greatest_lower_bound(identity,inverse(X1)))) = inverse(multiply(X1,inverse(X1))),
inference(step,[status(thm)],[t52865,t50]) ).
cnf(t52867,plain,
greatest_lower_bound(identity,inverse(greatest_lower_bound(identity,inverse(X1)))) = multiply(X1,inverse(X1)),
inference(step,[status(thm)],[t52866,t177]) ).
cnf(t52868,plain,
greatest_lower_bound(identity,inverse(greatest_lower_bound(identity,inverse(X1)))) = identity,
inference(step,[status(thm)],[t52867,t118]) ).
cnf(t1595,plain,
greatest_lower_bound(identity,inverse(greatest_lower_bound(identity,inverse(X1)))) = identity,
inference(orient,[status(thm)],[t52868]) ).
cnf(t1596,plain,
identity = greatest_lower_bound(identity,inverse(greatest_lower_bound(identity,multiply(X1,inverse(X2))))),
inference(cp,[status(thm)],[t1595,t177]) ).
cnf(t1657,plain,
greatest_lower_bound(identity,inverse(greatest_lower_bound(identity,multiply(X1,inverse(X2))))) = identity,
inference(orient,[status(thm)],[t1596]) ).
cnf(t52890,plain,
greatest_lower_bound(X1,inverse(greatest_lower_bound(inverse(X1),inverse(X2)))) = multiply(identity,X1),
inference(step,[status(thm)],[t1858,t1657]) ).
cnf(t52891,plain,
greatest_lower_bound(X1,inverse(greatest_lower_bound(inverse(X1),inverse(X2)))) = X1,
inference(step,[status(thm)],[t52890,t18]) ).
cnf(t1863,plain,
greatest_lower_bound(X1,inverse(greatest_lower_bound(inverse(X1),inverse(X2)))) = X1,
inference(orient,[status(thm)],[t52891]) ).
cnf(t1873,plain,
X1 = greatest_lower_bound(X1,inverse(greatest_lower_bound(inverse(X1),X2))),
inference(cp,[status(thm)],[t1863,t23]) ).
cnf(t52892,plain,
X1 = greatest_lower_bound(X1,inverse(greatest_lower_bound(X2,inverse(X1)))),
inference(step,[status(thm)],[t1873,t89]) ).
cnf(t1886,plain,
greatest_lower_bound(X1,inverse(greatest_lower_bound(X2,inverse(X1)))) = X1,
inference(orient,[status(thm)],[t52892]) ).
cnf(t1898,plain,
inverse(X1) = greatest_lower_bound(inverse(X1),inverse(greatest_lower_bound(X2,X1))),
inference(cp,[status(thm)],[t1886,t23]) ).
cnf(t52895,plain,
inverse(X1) = greatest_lower_bound(inverse(X1),inverse(greatest_lower_bound(X1,X2))),
inference(step,[status(thm)],[t1898,t89]) ).
cnf(t2008,plain,
greatest_lower_bound(inverse(X1),inverse(greatest_lower_bound(X1,X2))) = inverse(X1),
inference(orient,[status(thm)],[t52895]) ).
cnf(t2653,plain,
inverse(greatest_lower_bound(X1,X2)) = least_upper_bound(inverse(greatest_lower_bound(X1,X2)),inverse(X1)),
inference(cp,[status(thm)],[t2646,t2008]) ).
cnf(t52929,plain,
inverse(greatest_lower_bound(X1,X2)) = least_upper_bound(inverse(X1),inverse(greatest_lower_bound(X1,X2))),
inference(step,[status(thm)],[t2653,t63]) ).
cnf(t2667,plain,
least_upper_bound(inverse(X1),inverse(greatest_lower_bound(X1,X2))) = inverse(greatest_lower_bound(X1,X2)),
inference(orient,[status(thm)],[t52929]) ).
cnf(t2688,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)],[t592,t2667]) ).
cnf(t52932,plain,
least_upper_bound(identity,multiply(greatest_lower_bound(X1,X2),inverse(X1))) = identity,
inference(step,[status(thm)],[t2688,t118]) ).
cnf(t2711,plain,
least_upper_bound(identity,multiply(greatest_lower_bound(X1,X2),inverse(X1))) = identity,
inference(orient,[status(thm)],[t52932]) ).
cnf(t2167,plain,
inverse(least_upper_bound(X1,inverse(inverse(X2)))) = greatest_lower_bound(inverse(X2),inverse(least_upper_bound(X1,X2))),
inference(cp,[status(thm)],[t2155,t23]) ).
cnf(t52910,plain,
inverse(least_upper_bound(X1,X2)) = greatest_lower_bound(inverse(X2),inverse(least_upper_bound(X1,X2))),
inference(step,[status(thm)],[t2167,t23]) ).
cnf(t2250,plain,
greatest_lower_bound(inverse(X1),inverse(least_upper_bound(X2,X1))) = inverse(least_upper_bound(X2,X1)),
inference(orient,[status(thm)],[t52910]) ).
cnf(t2713,plain,
identity = least_upper_bound(identity,multiply(inverse(least_upper_bound(X1,X2)),inverse(inverse(X2)))),
inference(cp,[status(thm)],[t2711,t2250]) ).
cnf(t52934,plain,
identity = least_upper_bound(identity,inverse(multiply(inverse(X2),least_upper_bound(X1,X2)))),
inference(step,[status(thm)],[t2713,t50]) ).
cnf(t52935,plain,
identity = least_upper_bound(identity,multiply(inverse(least_upper_bound(X1,X2)),X2)),
inference(step,[status(thm)],[t52934,t182]) ).
cnf(t2762,plain,
least_upper_bound(identity,multiply(inverse(least_upper_bound(X1,X2)),X2)) = identity,
inference(orient,[status(thm)],[t52935]) ).
cnf(t12,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(t52797,plain,
least_upper_bound(X3,least_upper_bound(X1,X2)) = least_upper_bound(X1,least_upper_bound(X2,X3)),
inference(step,[status(thm)],[t12,t63]) ).
cnf(t67,plain,
least_upper_bound(X1,least_upper_bound(X2,X3)) = least_upper_bound(X2,least_upper_bound(X3,X1)),
inference(orient,[status(thm)],[t52797]) ).
cnf(t71,plain,
least_upper_bound(greatest_lower_bound(X1,X2),least_upper_bound(X3,X1)) = least_upper_bound(X3,X1),
inference(cp,[status(thm)],[t67,t20]) ).
cnf(t52829,plain,
least_upper_bound(X1,least_upper_bound(greatest_lower_bound(X1,X2),X3)) = least_upper_bound(X3,X1),
inference(step,[status(thm)],[t71,t67]) ).
cnf(t52830,plain,
least_upper_bound(X1,least_upper_bound(X3,greatest_lower_bound(X1,X2))) = least_upper_bound(X3,X1),
inference(step,[status(thm)],[t52829,t63]) ).
cnf(t52831,plain,
least_upper_bound(X1,least_upper_bound(X3,greatest_lower_bound(X1,X2))) = least_upper_bound(X1,X3),
inference(step,[status(thm)],[t52830,t63]) ).
cnf(t757,plain,
least_upper_bound(X1,least_upper_bound(X2,greatest_lower_bound(X1,X3))) = least_upper_bound(X1,X2),
inference(orient,[status(thm)],[t52831]) ).
cnf(t761,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)],[t757,t229]) ).
cnf(t6176,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)],[t761]) ).
cnf(t6181,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)],[t6176,t259]) ).
cnf(t48198,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)],[t6181]) ).
cnf(t245,plain,
multiply(X1,greatest_lower_bound(X1,identity)) = multiply(greatest_lower_bound(X1,identity),X1),
inference(cp,[status(thm)],[t244,t229]) ).
cnf(t274,plain,
multiply(greatest_lower_bound(X1,identity),X1) = multiply(X1,greatest_lower_bound(X1,identity)),
inference(orient,[status(thm)],[t245]) ).
cnf(t276,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)],[t259,t274]) ).
cnf(t52974,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)],[t276,t214]) ).
cnf(t4151,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)],[t52974]) ).
cnf(t48201,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)],[t48198,t4151]) ).
cnf(t53662,plain,
X1 = least_upper_bound(X1,multiply(least_upper_bound(X1,identity),greatest_lower_bound(X1,identity))),
inference(step,[status(thm)],[t48201,t20]) ).
cnf(t48255,plain,
least_upper_bound(X1,multiply(least_upper_bound(X1,identity),greatest_lower_bound(X1,identity))) = X1,
inference(orient,[status(thm)],[t53662]) ).
cnf(t48315,plain,
identity = least_upper_bound(identity,multiply(inverse(X1),multiply(least_upper_bound(X1,identity),greatest_lower_bound(X1,identity)))),
inference(cp,[status(thm)],[t2762,t48255]) ).
cnf(t266,plain,
multiply(inverse(X1),least_upper_bound(X1,identity)) = least_upper_bound(inverse(X1),identity),
inference(cp,[status(thm)],[t259,t39]) ).
cnf(t52822,plain,
multiply(inverse(X1),least_upper_bound(X1,identity)) = least_upper_bound(identity,inverse(X1)),
inference(step,[status(thm)],[t266,t63]) ).
cnf(t504,plain,
multiply(inverse(X1),least_upper_bound(X1,identity)) = least_upper_bound(identity,inverse(X1)),
inference(orient,[status(thm)],[t52822]) ).
cnf(t521,plain,
multiply(inverse(X1),multiply(least_upper_bound(X1,identity),X2)) = multiply(least_upper_bound(identity,inverse(X1)),X2),
inference(cp,[status(thm)],[t24,t504]) ).
cnf(t26398,plain,
multiply(inverse(X1),multiply(least_upper_bound(X1,identity),X2)) = multiply(least_upper_bound(identity,inverse(X1)),X2),
inference(orient,[status(thm)],[t521]) ).
cnf(t53663,plain,
identity = least_upper_bound(identity,multiply(least_upper_bound(identity,inverse(X1)),greatest_lower_bound(X1,identity))),
inference(step,[status(thm)],[t48315,t26398]) ).
cnf(t48396,plain,
least_upper_bound(identity,multiply(least_upper_bound(identity,inverse(X1)),greatest_lower_bound(X1,identity))) = identity,
inference(orient,[status(thm)],[t53663]) ).
cnf(t48442,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)],[t26487,t48396]) ).
cnf(t53667,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)],[t48442,t18]) ).
cnf(t53668,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)],[t53667,t18]) ).
cnf(t48570,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)],[t53668]) ).
cnf(t48605,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)],[t2338,t48570]) ).
cnf(t53669,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)],[t48605,t48570]) ).
cnf(t53670,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)],[t53669,t23]) ).
cnf(t53671,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)],[t53670,t23]) ).
cnf(t11,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(t52798,plain,
greatest_lower_bound(X3,greatest_lower_bound(X1,X2)) = greatest_lower_bound(X1,greatest_lower_bound(X2,X3)),
inference(step,[status(thm)],[t11,t89]) ).
cnf(t93,plain,
greatest_lower_bound(X1,greatest_lower_bound(X2,X3)) = greatest_lower_bound(X2,greatest_lower_bound(X3,X1)),
inference(orient,[status(thm)],[t52798]) ).
cnf(t53672,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)],[t53671,t93]) ).
cnf(t53673,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)],[t53672,t93]) ).
cnf(t523,plain,
multiply(inverse(least_upper_bound(X1,identity)),X1) = inverse(least_upper_bound(identity,inverse(X1))),
inference(cp,[status(thm)],[t182,t504]) ).
cnf(t734,plain,
multiply(inverse(least_upper_bound(X1,identity)),X1) = inverse(least_upper_bound(identity,inverse(X1))),
inference(orient,[status(thm)],[t523]) ).
cnf(t1338,plain,
greatest_lower_bound(inverse(least_upper_bound(X1,identity)),inverse(X1)) = multiply(greatest_lower_bound(identity,inverse(inverse(least_upper_bound(identity,inverse(X1))))),inverse(least_upper_bound(X1,identity))),
inference(cp,[status(thm)],[t1324,t734]) ).
cnf(t52852,plain,
greatest_lower_bound(inverse(X1),inverse(least_upper_bound(X1,identity))) = multiply(greatest_lower_bound(identity,inverse(inverse(least_upper_bound(identity,inverse(X1))))),inverse(least_upper_bound(X1,identity))),
inference(step,[status(thm)],[t1338,t89]) ).
cnf(t52853,plain,
greatest_lower_bound(inverse(X1),inverse(least_upper_bound(X1,identity))) = multiply(greatest_lower_bound(identity,least_upper_bound(identity,inverse(X1))),inverse(least_upper_bound(X1,identity))),
inference(step,[status(thm)],[t52852,t23]) ).
cnf(t52854,plain,
greatest_lower_bound(inverse(X1),inverse(least_upper_bound(X1,identity))) = multiply(identity,inverse(least_upper_bound(X1,identity))),
inference(step,[status(thm)],[t52853,t22]) ).
cnf(t52855,plain,
greatest_lower_bound(inverse(X1),inverse(least_upper_bound(X1,identity))) = inverse(least_upper_bound(X1,identity)),
inference(step,[status(thm)],[t52854,t18]) ).
cnf(t1388,plain,
greatest_lower_bound(inverse(X1),inverse(least_upper_bound(X1,identity))) = inverse(least_upper_bound(X1,identity)),
inference(orient,[status(thm)],[t52855]) ).
cnf(t1554,plain,
greatest_lower_bound(identity,inverse(multiply(least_upper_bound(X1,identity),inverse(X1)))) = multiply(inverse(inverse(X1)),inverse(least_upper_bound(X1,identity))),
inference(cp,[status(thm)],[t1546,t1388]) ).
cnf(t52872,plain,
greatest_lower_bound(identity,multiply(X1,inverse(least_upper_bound(X1,identity)))) = multiply(inverse(inverse(X1)),inverse(least_upper_bound(X1,identity))),
inference(step,[status(thm)],[t1554,t177]) ).
cnf(t217,plain,
multiply(least_upper_bound(X1,identity),inverse(X1)) = least_upper_bound(inverse(X1),identity),
inference(cp,[status(thm)],[t214,t118]) ).
cnf(t52819,plain,
multiply(least_upper_bound(X1,identity),inverse(X1)) = least_upper_bound(identity,inverse(X1)),
inference(step,[status(thm)],[t217,t63]) ).
cnf(t442,plain,
multiply(least_upper_bound(X1,identity),inverse(X1)) = least_upper_bound(identity,inverse(X1)),
inference(orient,[status(thm)],[t52819]) ).
cnf(t462,plain,
multiply(X1,inverse(least_upper_bound(X1,identity))) = inverse(least_upper_bound(identity,inverse(X1))),
inference(cp,[status(thm)],[t177,t442]) ).
cnf(t667,plain,
multiply(X1,inverse(least_upper_bound(X1,identity))) = inverse(least_upper_bound(identity,inverse(X1))),
inference(orient,[status(thm)],[t462]) ).
cnf(t52873,plain,
greatest_lower_bound(identity,inverse(least_upper_bound(identity,inverse(X1)))) = multiply(inverse(inverse(X1)),inverse(least_upper_bound(X1,identity))),
inference(step,[status(thm)],[t52872,t667]) ).
cnf(t52874,plain,
greatest_lower_bound(identity,inverse(least_upper_bound(identity,inverse(X1)))) = inverse(multiply(least_upper_bound(X1,identity),inverse(X1))),
inference(step,[status(thm)],[t52873,t50]) ).
cnf(t52875,plain,
greatest_lower_bound(identity,inverse(least_upper_bound(identity,inverse(X1)))) = multiply(X1,inverse(least_upper_bound(X1,identity))),
inference(step,[status(thm)],[t52874,t177]) ).
cnf(t52876,plain,
greatest_lower_bound(identity,inverse(least_upper_bound(identity,inverse(X1)))) = inverse(least_upper_bound(identity,inverse(X1))),
inference(step,[status(thm)],[t52875,t667]) ).
cnf(t1630,plain,
greatest_lower_bound(identity,inverse(least_upper_bound(identity,inverse(X1)))) = inverse(least_upper_bound(identity,inverse(X1))),
inference(orient,[status(thm)],[t52876]) ).
cnf(t53674,plain,
greatest_lower_bound(X1,identity) = greatest_lower_bound(X1,inverse(least_upper_bound(identity,inverse(X1)))),
inference(step,[status(thm)],[t53673,t1630]) ).
cnf(t1392,plain,
inverse(least_upper_bound(inverse(X1),identity)) = greatest_lower_bound(X1,inverse(least_upper_bound(inverse(X1),identity))),
inference(cp,[status(thm)],[t1388,t23]) ).
cnf(t52858,plain,
inverse(least_upper_bound(identity,inverse(X1))) = greatest_lower_bound(X1,inverse(least_upper_bound(inverse(X1),identity))),
inference(step,[status(thm)],[t1392,t63]) ).
cnf(t52859,plain,
inverse(least_upper_bound(identity,inverse(X1))) = greatest_lower_bound(X1,inverse(least_upper_bound(identity,inverse(X1)))),
inference(step,[status(thm)],[t52858,t63]) ).
cnf(t1417,plain,
greatest_lower_bound(X1,inverse(least_upper_bound(identity,inverse(X1)))) = inverse(least_upper_bound(identity,inverse(X1))),
inference(orient,[status(thm)],[t52859]) ).
cnf(t53675,plain,
greatest_lower_bound(X1,identity) = inverse(least_upper_bound(identity,inverse(X1))),
inference(step,[status(thm)],[t53674,t1417]) ).
cnf(t48655,plain,
inverse(least_upper_bound(identity,inverse(X1))) = greatest_lower_bound(X1,identity),
inference(orient,[status(thm)],[t53675]) ).
cnf(t48698,plain,
greatest_lower_bound(multiply(X1,inverse(X2)),identity) = inverse(least_upper_bound(identity,multiply(X2,inverse(X1)))),
inference(cp,[status(thm)],[t48655,t177]) ).
cnf(t53768,plain,
greatest_lower_bound(identity,multiply(X1,inverse(X2))) = inverse(least_upper_bound(identity,multiply(X2,inverse(X1)))),
inference(step,[status(thm)],[t48698,t89]) ).
cnf(t53769,plain,
multiply(greatest_lower_bound(X2,X1),inverse(X2)) = inverse(least_upper_bound(identity,multiply(X2,inverse(X1)))),
inference(step,[status(thm)],[t53768,t23677]) ).
cnf(t53770,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X2)) = inverse(least_upper_bound(identity,multiply(X2,inverse(X1)))),
inference(step,[status(thm)],[t53769,t89]) ).
cnf(t122,plain,
multiply(least_upper_bound(X1,X2),inverse(X1)) = least_upper_bound(identity,multiply(X2,inverse(X1))),
inference(cp,[status(thm)],[t28,t118]) ).
cnf(t28868,plain,
multiply(least_upper_bound(X1,X2),inverse(X1)) = least_upper_bound(identity,multiply(X2,inverse(X1))),
inference(orient,[status(thm)],[t122]) ).
cnf(t53771,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X2)) = inverse(multiply(least_upper_bound(X1,X2),inverse(X1))),
inference(step,[status(thm)],[t53770,t28868]) ).
cnf(t53772,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X2)) = multiply(X1,inverse(least_upper_bound(X1,X2))),
inference(step,[status(thm)],[t53771,t177]) ).
cnf(t51985,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X2)) = multiply(X1,inverse(least_upper_bound(X1,X2))),
inference(orient,[status(thm)],[t53772]) ).
cnf(t52203,plain,
inverse(greatest_lower_bound(X1,X2)) = multiply(inverse(X2),inverse(multiply(X1,inverse(least_upper_bound(X1,X2))))),
inference(cp,[status(thm)],[t190,t51985]) ).
cnf(t53773,plain,
inverse(greatest_lower_bound(X1,X2)) = inverse(multiply(multiply(X1,inverse(least_upper_bound(X1,X2))),X2)),
inference(step,[status(thm)],[t52203,t50]) ).
cnf(t53774,plain,
inverse(greatest_lower_bound(X1,X2)) = inverse(multiply(X1,multiply(inverse(least_upper_bound(X1,X2)),X2))),
inference(step,[status(thm)],[t53773,t24]) ).
cnf(t613,plain,
inverse(least_upper_bound(X1,inverse(X2))) = multiply(inverse(least_upper_bound(identity,multiply(X2,X1))),X2),
inference(cp,[status(thm)],[t203,t592]) ).
cnf(t5385,plain,
multiply(inverse(least_upper_bound(identity,multiply(X1,X2))),X1) = inverse(least_upper_bound(X2,inverse(X1))),
inference(orient,[status(thm)],[t613]) ).
cnf(t29085,plain,
inverse(least_upper_bound(inverse(X1),inverse(X2))) = multiply(inverse(multiply(least_upper_bound(X1,X2),inverse(X1))),X2),
inference(cp,[status(thm)],[t5385,t28868]) ).
cnf(t53519,plain,
inverse(least_upper_bound(inverse(X1),inverse(X2))) = multiply(multiply(X1,inverse(least_upper_bound(X1,X2))),X2),
inference(step,[status(thm)],[t29085,t177]) ).
cnf(t53520,plain,
inverse(least_upper_bound(inverse(X1),inverse(X2))) = multiply(X1,multiply(inverse(least_upper_bound(X1,X2)),X2)),
inference(step,[status(thm)],[t53519,t24]) ).
cnf(t30197,plain,
multiply(X1,multiply(inverse(least_upper_bound(X1,X2)),X2)) = inverse(least_upper_bound(inverse(X1),inverse(X2))),
inference(orient,[status(thm)],[t53520]) ).
cnf(t53775,plain,
inverse(greatest_lower_bound(X1,X2)) = inverse(inverse(least_upper_bound(inverse(X1),inverse(X2)))),
inference(step,[status(thm)],[t53774,t30197]) ).
cnf(t53776,plain,
inverse(greatest_lower_bound(X1,X2)) = least_upper_bound(inverse(X1),inverse(X2)),
inference(step,[status(thm)],[t53775,t23]) ).
cnf(t52356,plain,
least_upper_bound(inverse(X1),inverse(X2)) = inverse(greatest_lower_bound(X1,X2)),
inference(orient,[status(thm)],[t53776]) ).
cnf(t52376,plain,
inverse(greatest_lower_bound(inverse(X1),X2)) = least_upper_bound(X1,inverse(X2)),
inference(cp,[status(thm)],[t52356,t23]) ).
cnf(t53798,plain,
inverse(greatest_lower_bound(X2,inverse(X1))) = least_upper_bound(X1,inverse(X2)),
inference(step,[status(thm)],[t52376,t89]) ).
cnf(t52515,plain,
inverse(greatest_lower_bound(X1,inverse(X2))) = least_upper_bound(X2,inverse(X1)),
inference(orient,[status(thm)],[t53798]) ).
cnf(t53803,plain,
multiply(X1,multiply(inverse(greatest_lower_bound(X1,X2)),X2)) = least_upper_bound(X2,inverse(inverse(X1))),
inference(step,[status(thm)],[t29958,t52515]) ).
cnf(t53804,plain,
multiply(X1,multiply(inverse(greatest_lower_bound(X1,X2)),X2)) = least_upper_bound(X2,X1),
inference(step,[status(thm)],[t53803,t23]) ).
cnf(t53805,plain,
multiply(X1,multiply(inverse(greatest_lower_bound(X1,X2)),X2)) = least_upper_bound(X1,X2),
inference(step,[status(thm)],[t53804,t63]) ).
cnf(t52518,plain,
multiply(X1,multiply(inverse(greatest_lower_bound(X1,X2)),X2)) = least_upper_bound(X1,X2),
inference(orient,[status(thm)],[t53805]) ).
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,t52518]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP180-2 : 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.38 % Computer : n001.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Wed Sep 23 14:06:20 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 35.64/5.06 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 35.64/5.06 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------