%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP187-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 : n014.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:38 PM UTC 2026
% Result : Unsatisfiable 91.82s 13.82s
% Output : CNFRefutation 91.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 74
% Number of leaves : 18
% Syntax : Number of clauses : 414 ( 414 unt; 0 nHn; 214 RR)
% Number of literals : 414 ( 413 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 : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 366 ( 23 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t16,axiom,
sFlat0 = multiply(b,a),
introduced(definition) ).
cnf(t48,plain,
multiply(b,a) = sFlat0,
inference(orient,[status(thm)],[t16]) ).
cnf(t17,axiom,
sFlat1 = multiply(a,b),
introduced(definition) ).
cnf(t38,plain,
multiply(a,b) = sFlat1,
inference(orient,[status(thm)],[t17]) ).
cnf(t11,axiom,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t3,axiom,
multiply(inverse(X1),X1) = identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t58,plain,
multiply(inverse(X1),X1) = identity,
inference(orient,[status(thm)],[t3]) ).
cnf(t67,plain,
multiply(inverse(X1),multiply(X1,X2)) = multiply(identity,X2),
inference(cp,[status(thm)],[t23,t58]) ).
cnf(t2,axiom,
multiply(identity,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t18,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t174599,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(step,[status(thm)],[t67,t18]) ).
cnf(t150,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(orient,[status(thm)],[t174599]) ).
cnf(t160,plain,
multiply(X1,X2) = multiply(inverse(inverse(X1)),X2),
inference(cp,[status(thm)],[t150,t150]) ).
cnf(t241,plain,
multiply(inverse(inverse(X1)),X2) = multiply(X1,X2),
inference(orient,[status(thm)],[t160]) ).
cnf(t242,plain,
multiply(X1,inverse(X1)) = identity,
inference(cp,[status(thm)],[t241,t58]) ).
cnf(t263,plain,
multiply(X1,inverse(X1)) = identity,
inference(orient,[status(thm)],[t242]) ).
cnf(t264,plain,
identity = multiply(X1,multiply(X2,inverse(multiply(X1,X2)))),
inference(cp,[status(thm)],[t263,t23]) ).
cnf(t4890,plain,
multiply(X1,multiply(X2,inverse(multiply(X1,X2)))) = identity,
inference(orient,[status(thm)],[t264]) ).
cnf(t5004,plain,
multiply(X1,inverse(multiply(X2,X1))) = multiply(inverse(X2),identity),
inference(cp,[status(thm)],[t150,t4890]) ).
cnf(t151,plain,
X1 = multiply(inverse(inverse(X1)),identity),
inference(cp,[status(thm)],[t150,t58]) ).
cnf(t197,plain,
multiply(inverse(inverse(X1)),identity) = X1,
inference(orient,[status(thm)],[t151]) ).
cnf(t174600,plain,
multiply(X1,identity) = X1,
inference(step,[status(thm)],[t197,t241]) ).
cnf(t250,plain,
multiply(X1,identity) = X1,
inference(rw,[status(thm)],[t174600]) ).
cnf(t251,plain,
multiply(X1,identity) = X1,
inference(orient,[status(thm)],[t250]) ).
cnf(t174763,plain,
multiply(X1,inverse(multiply(X2,X1))) = inverse(X2),
inference(step,[status(thm)],[t5004,t251]) ).
cnf(t5039,plain,
multiply(X1,inverse(multiply(X2,X1))) = inverse(X2),
inference(orient,[status(thm)],[t174763]) ).
cnf(t12,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(t26,plain,
greatest_lower_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,greatest_lower_bound(X2,X3)),
inference(orient,[status(thm)],[t12]) ).
cnf(t63,plain,
multiply(inverse(X1),greatest_lower_bound(X1,X2)) = greatest_lower_bound(identity,multiply(inverse(X1),X2)),
inference(cp,[status(thm)],[t26,t58]) ).
cnf(t870,plain,
multiply(inverse(X1),greatest_lower_bound(X1,X2)) = greatest_lower_bound(identity,multiply(inverse(X1),X2)),
inference(orient,[status(thm)],[t63]) ).
cnf(t890,plain,
multiply(inverse(X1),greatest_lower_bound(X1,identity)) = greatest_lower_bound(identity,inverse(X1)),
inference(cp,[status(thm)],[t870,t251]) ).
cnf(t1086,plain,
multiply(inverse(X1),greatest_lower_bound(X1,identity)) = greatest_lower_bound(identity,inverse(X1)),
inference(orient,[status(thm)],[t890]) ).
cnf(t5121,plain,
inverse(inverse(X1)) = multiply(greatest_lower_bound(X1,identity),inverse(greatest_lower_bound(identity,inverse(X1)))),
inference(cp,[status(thm)],[t5039,t1086]) ).
cnf(t252,plain,
inverse(inverse(X1)) = multiply(X1,identity),
inference(cp,[status(thm)],[t251,t241]) ).
cnf(t174601,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t252,t251]) ).
cnf(t260,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t174601]) ).
cnf(t175383,plain,
X1 = multiply(greatest_lower_bound(X1,identity),inverse(greatest_lower_bound(identity,inverse(X1)))),
inference(step,[status(thm)],[t5121,t260]) ).
cnf(t78908,plain,
multiply(greatest_lower_bound(X1,identity),inverse(greatest_lower_bound(identity,inverse(X1)))) = X1,
inference(orient,[status(thm)],[t175383]) ).
cnf(t5162,plain,
inverse(multiply(X1,X2)) = multiply(inverse(X2),inverse(X1)),
inference(cp,[status(thm)],[t150,t5039]) ).
cnf(t5198,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t5162]) ).
cnf(t5234,plain,
multiply(inverse(X1),greatest_lower_bound(X1,inverse(X2))) = greatest_lower_bound(identity,inverse(multiply(X2,X1))),
inference(cp,[status(thm)],[t870,t5198]) ).
cnf(t38249,plain,
multiply(inverse(X1),greatest_lower_bound(X1,inverse(X2))) = greatest_lower_bound(identity,inverse(multiply(X2,X1))),
inference(orient,[status(thm)],[t5234]) ).
cnf(t166,plain,
multiply(inverse(X1),greatest_lower_bound(X2,multiply(X1,X3))) = greatest_lower_bound(multiply(inverse(X1),X2),X3),
inference(cp,[status(thm)],[t26,t150]) ).
cnf(t13692,plain,
multiply(inverse(X1),greatest_lower_bound(X2,multiply(X1,X3))) = greatest_lower_bound(multiply(inverse(X1),X2),X3),
inference(orient,[status(thm)],[t166]) ).
cnf(t57,plain,
multiply(b,multiply(a,X1)) = multiply(sFlat0,X1),
inference(cp,[status(thm)],[t23,t48]) ).
cnf(t120,plain,
multiply(b,multiply(a,X1)) = multiply(sFlat0,X1),
inference(orient,[status(thm)],[t57]) ).
cnf(t129,plain,
multiply(b,greatest_lower_bound(multiply(a,X1),X2)) = greatest_lower_bound(multiply(sFlat0,X1),multiply(b,X2)),
inference(cp,[status(thm)],[t26,t120]) ).
cnf(t6841,plain,
greatest_lower_bound(multiply(sFlat0,X1),multiply(b,X2)) = multiply(b,greatest_lower_bound(multiply(a,X1),X2)),
inference(orient,[status(thm)],[t129]) ).
cnf(t6871,plain,
multiply(b,greatest_lower_bound(multiply(a,X1),identity)) = greatest_lower_bound(multiply(sFlat0,X1),b),
inference(cp,[status(thm)],[t6841,t251]) ).
cnf(t4,axiom,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t79,plain,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t174835,plain,
multiply(b,greatest_lower_bound(identity,multiply(a,X1))) = greatest_lower_bound(multiply(sFlat0,X1),b),
inference(step,[status(thm)],[t6871,t79]) ).
cnf(t174836,plain,
multiply(b,greatest_lower_bound(identity,multiply(a,X1))) = greatest_lower_bound(b,multiply(sFlat0,X1)),
inference(step,[status(thm)],[t174835,t79]) ).
cnf(t11228,plain,
multiply(b,greatest_lower_bound(identity,multiply(a,X1))) = greatest_lower_bound(b,multiply(sFlat0,X1)),
inference(orient,[status(thm)],[t174836]) ).
cnf(t13,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(t33,plain,
greatest_lower_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(greatest_lower_bound(X1,X3),X2),
inference(orient,[status(thm)],[t13]) ).
cnf(t269,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X1)) = greatest_lower_bound(identity,multiply(X2,inverse(X1))),
inference(cp,[status(thm)],[t33,t263]) ).
cnf(t2759,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X1)) = greatest_lower_bound(identity,multiply(X2,inverse(X1))),
inference(orient,[status(thm)],[t269]) ).
cnf(t11230,plain,
greatest_lower_bound(b,multiply(sFlat0,inverse(X1))) = multiply(b,multiply(greatest_lower_bound(X1,a),inverse(X1))),
inference(cp,[status(thm)],[t11228,t2759]) ).
cnf(t109311,plain,
multiply(b,multiply(greatest_lower_bound(X1,a),inverse(X1))) = greatest_lower_bound(b,multiply(sFlat0,inverse(X1))),
inference(orient,[status(thm)],[t11230]) ).
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(t80,plain,
greatest_lower_bound(greatest_lower_bound(X1,X2),X3) = greatest_lower_bound(X1,greatest_lower_bound(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t86,plain,
greatest_lower_bound(multiply(X1,X2),greatest_lower_bound(multiply(X1,X3),Y3)) = greatest_lower_bound(multiply(X1,greatest_lower_bound(X2,X3)),Y3),
inference(cp,[status(thm)],[t80,t26]) ).
cnf(t14270,plain,
greatest_lower_bound(multiply(X1,X2),greatest_lower_bound(multiply(X1,X3),Y3)) = greatest_lower_bound(multiply(X1,greatest_lower_bound(X2,X3)),Y3),
inference(orient,[status(thm)],[t86]) ).
cnf(t14458,plain,
greatest_lower_bound(multiply(X1,greatest_lower_bound(X2,X3)),multiply(Y3,X3)) = greatest_lower_bound(multiply(X1,X2),multiply(greatest_lower_bound(X1,Y3),X3)),
inference(cp,[status(thm)],[t14270,t33]) ).
cnf(t163660,plain,
greatest_lower_bound(multiply(X1,greatest_lower_bound(X2,X3)),multiply(Y3,X3)) = greatest_lower_bound(multiply(X1,X2),multiply(greatest_lower_bound(X1,Y3),X3)),
inference(orient,[status(thm)],[t14458]) ).
cnf(t43,plain,
multiply(a,greatest_lower_bound(b,X1)) = greatest_lower_bound(sFlat1,multiply(a,X1)),
inference(cp,[status(thm)],[t26,t38]) ).
cnf(t339,plain,
greatest_lower_bound(sFlat1,multiply(a,X1)) = multiply(a,greatest_lower_bound(b,X1)),
inference(orient,[status(thm)],[t43]) ).
cnf(t343,plain,
multiply(a,greatest_lower_bound(b,identity)) = greatest_lower_bound(sFlat1,a),
inference(cp,[status(thm)],[t339,t251]) ).
cnf(t174608,plain,
multiply(a,greatest_lower_bound(identity,b)) = greatest_lower_bound(sFlat1,a),
inference(step,[status(thm)],[t343,t79]) ).
cnf(t470,plain,
multiply(a,greatest_lower_bound(identity,b)) = greatest_lower_bound(sFlat1,a),
inference(orient,[status(thm)],[t174608]) ).
cnf(t163704,plain,
greatest_lower_bound(multiply(a,identity),multiply(greatest_lower_bound(a,X1),b)) = greatest_lower_bound(greatest_lower_bound(sFlat1,a),multiply(X1,b)),
inference(cp,[status(thm)],[t163660,t470]) ).
cnf(t176087,plain,
greatest_lower_bound(a,multiply(greatest_lower_bound(a,X1),b)) = greatest_lower_bound(greatest_lower_bound(sFlat1,a),multiply(X1,b)),
inference(step,[status(thm)],[t163704,t251]) ).
cnf(t176088,plain,
greatest_lower_bound(a,multiply(greatest_lower_bound(a,X1),b)) = greatest_lower_bound(sFlat1,greatest_lower_bound(a,multiply(X1,b))),
inference(step,[status(thm)],[t176087,t80]) ).
cnf(t166510,plain,
greatest_lower_bound(a,multiply(greatest_lower_bound(a,X1),b)) = greatest_lower_bound(sFlat1,greatest_lower_bound(a,multiply(X1,b))),
inference(orient,[status(thm)],[t176088]) ).
cnf(t34,plain,
multiply(greatest_lower_bound(identity,X1),X2) = greatest_lower_bound(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t33,t18]) ).
cnf(t225,plain,
greatest_lower_bound(X1,multiply(X2,X1)) = multiply(greatest_lower_bound(identity,X2),X1),
inference(orient,[status(thm)],[t34]) ).
cnf(t166563,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(a,multiply(multiply(X1,a),b))) = greatest_lower_bound(a,multiply(multiply(greatest_lower_bound(identity,X1),a),b)),
inference(cp,[status(thm)],[t166510,t225]) ).
cnf(t176096,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(a,multiply(X1,multiply(a,b)))) = greatest_lower_bound(a,multiply(multiply(greatest_lower_bound(identity,X1),a),b)),
inference(step,[status(thm)],[t166563,t23]) ).
cnf(t176097,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(a,multiply(X1,sFlat1))) = greatest_lower_bound(a,multiply(multiply(greatest_lower_bound(identity,X1),a),b)),
inference(step,[status(thm)],[t176096,t38]) ).
cnf(t176098,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(a,multiply(X1,sFlat1))) = greatest_lower_bound(a,multiply(greatest_lower_bound(identity,X1),multiply(a,b))),
inference(step,[status(thm)],[t176097,t23]) ).
cnf(t176099,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(a,multiply(X1,sFlat1))) = greatest_lower_bound(a,multiply(greatest_lower_bound(identity,X1),sFlat1)),
inference(step,[status(thm)],[t176098,t38]) ).
cnf(t168746,plain,
greatest_lower_bound(a,multiply(greatest_lower_bound(identity,X1),sFlat1)) = greatest_lower_bound(sFlat1,greatest_lower_bound(a,multiply(X1,sFlat1))),
inference(orient,[status(thm)],[t176099]) ).
cnf(t5,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)],[t5]) ).
cnf(t10,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(t69,plain,
least_upper_bound(least_upper_bound(X1,X2),X3) = least_upper_bound(X1,least_upper_bound(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t6,axiom,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t68,plain,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t72,plain,
least_upper_bound(X1,least_upper_bound(X2,X3)) = least_upper_bound(X3,least_upper_bound(X1,X2)),
inference(cp,[status(thm)],[t69,t68]) ).
cnf(t144,plain,
least_upper_bound(X1,least_upper_bound(X2,X3)) = least_upper_bound(X3,least_upper_bound(X1,X2)),
inference(orient,[status(thm)],[t72]) ).
cnf(t145,plain,
X1 = greatest_lower_bound(X1,least_upper_bound(X2,least_upper_bound(X3,X1))),
inference(cp,[status(thm)],[t22,t144]) ).
cnf(t1018,plain,
greatest_lower_bound(X1,least_upper_bound(X2,least_upper_bound(X3,X1))) = X1,
inference(orient,[status(thm)],[t145]) ).
cnf(t1,axiom,
least_upper_bound(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
least_upper_bound(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t73,plain,
least_upper_bound(X1,least_upper_bound(X1,X2)) = least_upper_bound(X1,X2),
inference(cp,[status(thm)],[t69,t19]) ).
cnf(t93,plain,
least_upper_bound(X1,least_upper_bound(X1,X2)) = least_upper_bound(X1,X2),
inference(orient,[status(thm)],[t73]) ).
cnf(t1020,plain,
X1 = greatest_lower_bound(X1,least_upper_bound(X2,X1)),
inference(cp,[status(thm)],[t1018,t93]) ).
cnf(t1048,plain,
greatest_lower_bound(X1,least_upper_bound(X2,X1)) = X1,
inference(orient,[status(thm)],[t1020]) ).
cnf(t15,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(t27,plain,
least_upper_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(least_upper_bound(X1,X3),X2),
inference(orient,[status(thm)],[t15]) ).
cnf(t47,plain,
multiply(a,multiply(b,X1)) = multiply(sFlat1,X1),
inference(cp,[status(thm)],[t23,t38]) ).
cnf(t100,plain,
multiply(a,multiply(b,X1)) = multiply(sFlat1,X1),
inference(orient,[status(thm)],[t47]) ).
cnf(t157,plain,
multiply(b,X1) = multiply(inverse(a),multiply(sFlat1,X1)),
inference(cp,[status(thm)],[t150,t100]) ).
cnf(t818,plain,
multiply(inverse(a),multiply(sFlat1,X1)) = multiply(b,X1),
inference(orient,[status(thm)],[t157]) ).
cnf(t820,plain,
multiply(b,inverse(sFlat1)) = multiply(inverse(a),identity),
inference(cp,[status(thm)],[t818,t263]) ).
cnf(t174635,plain,
multiply(b,inverse(sFlat1)) = inverse(a),
inference(step,[status(thm)],[t820,t251]) ).
cnf(t835,plain,
multiply(b,inverse(sFlat1)) = inverse(a),
inference(orient,[status(thm)],[t174635]) ).
cnf(t845,plain,
multiply(least_upper_bound(b,X1),inverse(sFlat1)) = least_upper_bound(inverse(a),multiply(X1,inverse(sFlat1))),
inference(cp,[status(thm)],[t27,t835]) ).
cnf(t31626,plain,
least_upper_bound(inverse(a),multiply(X1,inverse(sFlat1))) = multiply(least_upper_bound(b,X1),inverse(sFlat1)),
inference(orient,[status(thm)],[t845]) ).
cnf(t265,plain,
multiply(greatest_lower_bound(identity,X1),inverse(X1)) = greatest_lower_bound(inverse(X1),identity),
inference(cp,[status(thm)],[t225,t263]) ).
cnf(t174668,plain,
multiply(greatest_lower_bound(identity,X1),inverse(X1)) = greatest_lower_bound(identity,inverse(X1)),
inference(step,[status(thm)],[t265,t79]) ).
cnf(t1738,plain,
multiply(greatest_lower_bound(identity,X1),inverse(X1)) = greatest_lower_bound(identity,inverse(X1)),
inference(orient,[status(thm)],[t174668]) ).
cnf(t1749,plain,
greatest_lower_bound(identity,inverse(X1)) = multiply(greatest_lower_bound(X1,identity),inverse(X1)),
inference(cp,[status(thm)],[t1738,t79]) ).
cnf(t2981,plain,
multiply(greatest_lower_bound(X1,identity),inverse(X1)) = greatest_lower_bound(identity,inverse(X1)),
inference(orient,[status(thm)],[t1749]) ).
cnf(t31648,plain,
multiply(least_upper_bound(b,greatest_lower_bound(sFlat1,identity)),inverse(sFlat1)) = least_upper_bound(inverse(a),greatest_lower_bound(identity,inverse(sFlat1))),
inference(cp,[status(thm)],[t31626,t2981]) ).
cnf(t28,plain,
multiply(least_upper_bound(identity,X1),X2) = least_upper_bound(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t27,t18]) ).
cnf(t208,plain,
least_upper_bound(X1,multiply(X2,X1)) = multiply(least_upper_bound(identity,X2),X1),
inference(orient,[status(thm)],[t28]) ).
cnf(t223,plain,
multiply(least_upper_bound(identity,multiply(X1,X2)),X3) = least_upper_bound(X3,multiply(X1,multiply(X2,X3))),
inference(cp,[status(thm)],[t208,t23]) ).
cnf(t4589,plain,
least_upper_bound(X1,multiply(X2,multiply(X3,X1))) = multiply(least_upper_bound(identity,multiply(X2,X3)),X1),
inference(orient,[status(thm)],[t223]) ).
cnf(t4724,plain,
multiply(least_upper_bound(identity,multiply(X1,a)),b) = least_upper_bound(b,multiply(X1,sFlat1)),
inference(cp,[status(thm)],[t4589,t38]) ).
cnf(t10185,plain,
multiply(least_upper_bound(identity,multiply(X1,a)),b) = least_upper_bound(b,multiply(X1,sFlat1)),
inference(orient,[status(thm)],[t4724]) ).
cnf(t268,plain,
multiply(sFlat1,inverse(b)) = multiply(a,identity),
inference(cp,[status(thm)],[t100,t263]) ).
cnf(t174603,plain,
multiply(sFlat1,inverse(b)) = a,
inference(step,[status(thm)],[t268,t251]) ).
cnf(t291,plain,
multiply(sFlat1,inverse(b)) = a,
inference(orient,[status(thm)],[t174603]) ).
cnf(t294,plain,
inverse(b) = multiply(inverse(sFlat1),a),
inference(cp,[status(thm)],[t150,t291]) ).
cnf(t316,plain,
multiply(inverse(sFlat1),a) = inverse(b),
inference(orient,[status(thm)],[t294]) ).
cnf(t317,plain,
multiply(greatest_lower_bound(identity,inverse(sFlat1)),a) = greatest_lower_bound(a,inverse(b)),
inference(cp,[status(thm)],[t225,t316]) ).
cnf(t8908,plain,
multiply(greatest_lower_bound(identity,inverse(sFlat1)),a) = greatest_lower_bound(a,inverse(b)),
inference(orient,[status(thm)],[t317]) ).
cnf(t10199,plain,
least_upper_bound(b,multiply(greatest_lower_bound(identity,inverse(sFlat1)),sFlat1)) = multiply(least_upper_bound(identity,greatest_lower_bound(a,inverse(b))),b),
inference(cp,[status(thm)],[t10185,t8908]) ).
cnf(t60,plain,
multiply(greatest_lower_bound(X1,inverse(X2)),X2) = greatest_lower_bound(multiply(X1,X2),identity),
inference(cp,[status(thm)],[t33,t58]) ).
cnf(t174620,plain,
multiply(greatest_lower_bound(X1,inverse(X2)),X2) = greatest_lower_bound(identity,multiply(X1,X2)),
inference(step,[status(thm)],[t60,t79]) ).
cnf(t624,plain,
multiply(greatest_lower_bound(X1,inverse(X2)),X2) = greatest_lower_bound(identity,multiply(X1,X2)),
inference(orient,[status(thm)],[t174620]) ).
cnf(t174811,plain,
least_upper_bound(b,greatest_lower_bound(identity,multiply(identity,sFlat1))) = multiply(least_upper_bound(identity,greatest_lower_bound(a,inverse(b))),b),
inference(step,[status(thm)],[t10199,t624]) ).
cnf(t255,plain,
multiply(X1,greatest_lower_bound(identity,X2)) = greatest_lower_bound(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t26,t251]) ).
cnf(t693,plain,
greatest_lower_bound(X1,multiply(X1,X2)) = multiply(X1,greatest_lower_bound(identity,X2)),
inference(orient,[status(thm)],[t255]) ).
cnf(t174812,plain,
least_upper_bound(b,multiply(identity,greatest_lower_bound(identity,sFlat1))) = multiply(least_upper_bound(identity,greatest_lower_bound(a,inverse(b))),b),
inference(step,[status(thm)],[t174811,t693]) ).
cnf(t174813,plain,
least_upper_bound(b,greatest_lower_bound(identity,sFlat1)) = multiply(least_upper_bound(identity,greatest_lower_bound(a,inverse(b))),b),
inference(step,[status(thm)],[t174812,t18]) ).
cnf(t174814,plain,
least_upper_bound(b,greatest_lower_bound(sFlat1,identity)) = multiply(least_upper_bound(identity,greatest_lower_bound(a,inverse(b))),b),
inference(step,[status(thm)],[t174813,t79]) ).
cnf(t7,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)],[t7]) ).
cnf(t1029,plain,
greatest_lower_bound(X1,X2) = greatest_lower_bound(greatest_lower_bound(X1,X2),least_upper_bound(X3,X1)),
inference(cp,[status(thm)],[t1018,t20]) ).
cnf(t174709,plain,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X1,greatest_lower_bound(X2,least_upper_bound(X3,X1))),
inference(step,[status(thm)],[t1029,t80]) ).
cnf(t2935,plain,
greatest_lower_bound(X1,greatest_lower_bound(X2,least_upper_bound(X3,X1))) = greatest_lower_bound(X1,X2),
inference(orient,[status(thm)],[t174709]) ).
cnf(t85,plain,
greatest_lower_bound(X1,greatest_lower_bound(least_upper_bound(X1,X2),X3)) = greatest_lower_bound(X1,X3),
inference(cp,[status(thm)],[t80,t22]) ).
cnf(t1002,plain,
greatest_lower_bound(X1,greatest_lower_bound(least_upper_bound(X1,X2),X3)) = greatest_lower_bound(X1,X3),
inference(orient,[status(thm)],[t85]) ).
cnf(t1007,plain,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X1,greatest_lower_bound(X2,least_upper_bound(X1,X3))),
inference(cp,[status(thm)],[t1002,t79]) ).
cnf(t1665,plain,
greatest_lower_bound(X1,greatest_lower_bound(X2,least_upper_bound(X1,X3))) = greatest_lower_bound(X1,X2),
inference(orient,[status(thm)],[t1007]) ).
cnf(t9,axiom,
greatest_lower_bound(least_upper_bound(a,inverse(a)),least_upper_bound(b,inverse(b))) = identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t174596,plain,
greatest_lower_bound(least_upper_bound(b,inverse(b)),least_upper_bound(a,inverse(a))) = identity,
inference(step,[status(thm)],[t9,t79]) ).
cnf(t90,plain,
greatest_lower_bound(least_upper_bound(b,inverse(b)),least_upper_bound(a,inverse(a))) = identity,
inference(orient,[status(thm)],[t174596]) ).
cnf(t1668,plain,
greatest_lower_bound(a,least_upper_bound(b,inverse(b))) = greatest_lower_bound(a,identity),
inference(cp,[status(thm)],[t1665,t90]) ).
cnf(t174691,plain,
greatest_lower_bound(a,least_upper_bound(b,inverse(b))) = greatest_lower_bound(identity,a),
inference(step,[status(thm)],[t1668,t79]) ).
cnf(t2418,plain,
greatest_lower_bound(a,least_upper_bound(b,inverse(b))) = greatest_lower_bound(identity,a),
inference(orient,[status(thm)],[t174691]) ).
cnf(t2937,plain,
greatest_lower_bound(inverse(b),a) = greatest_lower_bound(inverse(b),greatest_lower_bound(identity,a)),
inference(cp,[status(thm)],[t2935,t2418]) ).
cnf(t174793,plain,
greatest_lower_bound(a,inverse(b)) = greatest_lower_bound(inverse(b),greatest_lower_bound(identity,a)),
inference(step,[status(thm)],[t2937,t79]) ).
cnf(t88,plain,
greatest_lower_bound(X1,greatest_lower_bound(X2,X3)) = greatest_lower_bound(greatest_lower_bound(X2,X1),X3),
inference(cp,[status(thm)],[t80,t79]) ).
cnf(t174598,plain,
greatest_lower_bound(X1,greatest_lower_bound(X2,X3)) = greatest_lower_bound(X2,greatest_lower_bound(X1,X3)),
inference(step,[status(thm)],[t88,t80]) ).
cnf(t149,plain,
greatest_lower_bound(X1,greatest_lower_bound(X2,X3)) = greatest_lower_bound(X2,greatest_lower_bound(X1,X3)),
inference(orient,[status(thm)],[t174598]) ).
cnf(t174794,plain,
greatest_lower_bound(a,inverse(b)) = greatest_lower_bound(identity,greatest_lower_bound(inverse(b),a)),
inference(step,[status(thm)],[t174793,t149]) ).
cnf(t174795,plain,
greatest_lower_bound(a,inverse(b)) = greatest_lower_bound(identity,greatest_lower_bound(a,inverse(b))),
inference(step,[status(thm)],[t174794,t79]) ).
cnf(t9252,plain,
greatest_lower_bound(identity,greatest_lower_bound(a,inverse(b))) = greatest_lower_bound(a,inverse(b)),
inference(orient,[status(thm)],[t174795]) ).
cnf(t9253,plain,
identity = least_upper_bound(identity,greatest_lower_bound(a,inverse(b))),
inference(cp,[status(thm)],[t20,t9252]) ).
cnf(t9268,plain,
least_upper_bound(identity,greatest_lower_bound(a,inverse(b))) = identity,
inference(orient,[status(thm)],[t9253]) ).
cnf(t174815,plain,
least_upper_bound(b,greatest_lower_bound(sFlat1,identity)) = multiply(identity,b),
inference(step,[status(thm)],[t174814,t9268]) ).
cnf(t174816,plain,
least_upper_bound(b,greatest_lower_bound(sFlat1,identity)) = b,
inference(step,[status(thm)],[t174815,t18]) ).
cnf(t10247,plain,
least_upper_bound(b,greatest_lower_bound(sFlat1,identity)) = b,
inference(orient,[status(thm)],[t174816]) ).
cnf(t175008,plain,
multiply(b,inverse(sFlat1)) = least_upper_bound(inverse(a),greatest_lower_bound(identity,inverse(sFlat1))),
inference(step,[status(thm)],[t31648,t10247]) ).
cnf(t175009,plain,
inverse(a) = least_upper_bound(inverse(a),greatest_lower_bound(identity,inverse(sFlat1))),
inference(step,[status(thm)],[t175008,t835]) ).
cnf(t31689,plain,
least_upper_bound(inverse(a),greatest_lower_bound(identity,inverse(sFlat1))) = inverse(a),
inference(orient,[status(thm)],[t175009]) ).
cnf(t31690,plain,
greatest_lower_bound(identity,inverse(sFlat1)) = greatest_lower_bound(greatest_lower_bound(identity,inverse(sFlat1)),inverse(a)),
inference(cp,[status(thm)],[t1048,t31689]) ).
cnf(t175475,plain,
greatest_lower_bound(identity,inverse(sFlat1)) = greatest_lower_bound(identity,greatest_lower_bound(inverse(sFlat1),inverse(a))),
inference(step,[status(thm)],[t31690,t80]) ).
cnf(t87667,plain,
greatest_lower_bound(identity,greatest_lower_bound(inverse(sFlat1),inverse(a))) = greatest_lower_bound(identity,inverse(sFlat1)),
inference(orient,[status(thm)],[t175475]) ).
cnf(t168787,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(a,multiply(greatest_lower_bound(inverse(sFlat1),inverse(a)),sFlat1))) = greatest_lower_bound(a,multiply(greatest_lower_bound(identity,inverse(sFlat1)),sFlat1)),
inference(cp,[status(thm)],[t168746,t87667]) ).
cnf(t59,plain,
multiply(greatest_lower_bound(inverse(X1),X2),X1) = greatest_lower_bound(identity,multiply(X2,X1)),
inference(cp,[status(thm)],[t33,t58]) ).
cnf(t599,plain,
multiply(greatest_lower_bound(inverse(X1),X2),X1) = greatest_lower_bound(identity,multiply(X2,X1)),
inference(orient,[status(thm)],[t59]) ).
cnf(t176101,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(a,greatest_lower_bound(identity,multiply(inverse(a),sFlat1)))) = greatest_lower_bound(a,multiply(greatest_lower_bound(identity,inverse(sFlat1)),sFlat1)),
inference(step,[status(thm)],[t168787,t599]) ).
cnf(t64,plain,
multiply(inverse(X1),greatest_lower_bound(X2,X1)) = greatest_lower_bound(multiply(inverse(X1),X2),identity),
inference(cp,[status(thm)],[t26,t58]) ).
cnf(t174636,plain,
multiply(inverse(X1),greatest_lower_bound(X2,X1)) = greatest_lower_bound(identity,multiply(inverse(X1),X2)),
inference(step,[status(thm)],[t64,t79]) ).
cnf(t892,plain,
multiply(inverse(X1),greatest_lower_bound(X2,X1)) = greatest_lower_bound(identity,multiply(inverse(X1),X2)),
inference(orient,[status(thm)],[t174636]) ).
cnf(t176102,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(a,multiply(inverse(a),greatest_lower_bound(sFlat1,a)))) = greatest_lower_bound(a,multiply(greatest_lower_bound(identity,inverse(sFlat1)),sFlat1)),
inference(step,[status(thm)],[t176101,t892]) ).
cnf(t474,plain,
greatest_lower_bound(identity,b) = multiply(inverse(a),greatest_lower_bound(sFlat1,a)),
inference(cp,[status(thm)],[t150,t470]) ).
cnf(t2008,plain,
multiply(inverse(a),greatest_lower_bound(sFlat1,a)) = greatest_lower_bound(identity,b),
inference(orient,[status(thm)],[t474]) ).
cnf(t176103,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(a,greatest_lower_bound(identity,b))) = greatest_lower_bound(a,multiply(greatest_lower_bound(identity,inverse(sFlat1)),sFlat1)),
inference(step,[status(thm)],[t176102,t2008]) ).
cnf(t176104,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(identity,greatest_lower_bound(a,b))) = greatest_lower_bound(a,multiply(greatest_lower_bound(identity,inverse(sFlat1)),sFlat1)),
inference(step,[status(thm)],[t176103,t149]) ).
cnf(t176105,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(identity,greatest_lower_bound(b,a))) = greatest_lower_bound(a,multiply(greatest_lower_bound(identity,inverse(sFlat1)),sFlat1)),
inference(step,[status(thm)],[t176104,t79]) ).
cnf(t1004,plain,
greatest_lower_bound(b,least_upper_bound(a,inverse(a))) = greatest_lower_bound(b,identity),
inference(cp,[status(thm)],[t1002,t90]) ).
cnf(t174660,plain,
greatest_lower_bound(b,least_upper_bound(a,inverse(a))) = greatest_lower_bound(identity,b),
inference(step,[status(thm)],[t1004,t79]) ).
cnf(t1492,plain,
greatest_lower_bound(b,least_upper_bound(a,inverse(a))) = greatest_lower_bound(identity,b),
inference(orient,[status(thm)],[t174660]) ).
cnf(t1667,plain,
greatest_lower_bound(a,b) = greatest_lower_bound(a,greatest_lower_bound(identity,b)),
inference(cp,[status(thm)],[t1665,t1492]) ).
cnf(t174665,plain,
greatest_lower_bound(b,a) = greatest_lower_bound(a,greatest_lower_bound(identity,b)),
inference(step,[status(thm)],[t1667,t79]) ).
cnf(t174666,plain,
greatest_lower_bound(b,a) = greatest_lower_bound(identity,greatest_lower_bound(a,b)),
inference(step,[status(thm)],[t174665,t149]) ).
cnf(t174667,plain,
greatest_lower_bound(b,a) = greatest_lower_bound(identity,greatest_lower_bound(b,a)),
inference(step,[status(thm)],[t174666,t79]) ).
cnf(t1678,plain,
greatest_lower_bound(identity,greatest_lower_bound(b,a)) = greatest_lower_bound(b,a),
inference(orient,[status(thm)],[t174667]) ).
cnf(t176106,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(b,a)) = greatest_lower_bound(a,multiply(greatest_lower_bound(identity,inverse(sFlat1)),sFlat1)),
inference(step,[status(thm)],[t176105,t1678]) ).
cnf(t14,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(t24,plain,
least_upper_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,least_upper_bound(X2,X3)),
inference(orient,[status(thm)],[t14]) ).
cnf(t257,plain,
multiply(X1,least_upper_bound(identity,X2)) = least_upper_bound(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t24,t251]) ).
cnf(t729,plain,
least_upper_bound(X1,multiply(X1,X2)) = multiply(X1,least_upper_bound(identity,X2)),
inference(orient,[status(thm)],[t257]) ).
cnf(t274,plain,
multiply(X1,greatest_lower_bound(X2,inverse(X1))) = greatest_lower_bound(multiply(X1,X2),identity),
inference(cp,[status(thm)],[t26,t263]) ).
cnf(t174670,plain,
multiply(X1,greatest_lower_bound(X2,inverse(X1))) = greatest_lower_bound(identity,multiply(X1,X2)),
inference(step,[status(thm)],[t274,t79]) ).
cnf(t1908,plain,
multiply(X1,greatest_lower_bound(X2,inverse(X1))) = greatest_lower_bound(identity,multiply(X1,X2)),
inference(orient,[status(thm)],[t174670]) ).
cnf(t1913,plain,
multiply(X1,least_upper_bound(identity,greatest_lower_bound(X2,inverse(X1)))) = least_upper_bound(X1,greatest_lower_bound(identity,multiply(X1,X2))),
inference(cp,[status(thm)],[t729,t1908]) ).
cnf(t112746,plain,
multiply(X1,least_upper_bound(identity,greatest_lower_bound(X2,inverse(X1)))) = least_upper_bound(X1,greatest_lower_bound(identity,multiply(X1,X2))),
inference(orient,[status(thm)],[t1913]) ).
cnf(t2939,plain,
greatest_lower_bound(inverse(a),least_upper_bound(b,inverse(b))) = greatest_lower_bound(inverse(a),identity),
inference(cp,[status(thm)],[t2935,t90]) ).
cnf(t174875,plain,
greatest_lower_bound(inverse(a),least_upper_bound(b,inverse(b))) = greatest_lower_bound(identity,inverse(a)),
inference(step,[status(thm)],[t2939,t79]) ).
cnf(t17208,plain,
greatest_lower_bound(inverse(a),least_upper_bound(b,inverse(b))) = greatest_lower_bound(identity,inverse(a)),
inference(orient,[status(thm)],[t174875]) ).
cnf(t17216,plain,
greatest_lower_bound(inverse(b),inverse(a)) = greatest_lower_bound(inverse(b),greatest_lower_bound(identity,inverse(a))),
inference(cp,[status(thm)],[t2935,t17208]) ).
cnf(t175235,plain,
greatest_lower_bound(inverse(b),inverse(a)) = greatest_lower_bound(identity,greatest_lower_bound(inverse(b),inverse(a))),
inference(step,[status(thm)],[t17216,t149]) ).
cnf(t58755,plain,
greatest_lower_bound(identity,greatest_lower_bound(inverse(b),inverse(a))) = greatest_lower_bound(inverse(b),inverse(a)),
inference(orient,[status(thm)],[t175235]) ).
cnf(t58756,plain,
identity = least_upper_bound(identity,greatest_lower_bound(inverse(b),inverse(a))),
inference(cp,[status(thm)],[t20,t58755]) ).
cnf(t58801,plain,
least_upper_bound(identity,greatest_lower_bound(inverse(b),inverse(a))) = identity,
inference(orient,[status(thm)],[t58756]) ).
cnf(t112750,plain,
least_upper_bound(a,greatest_lower_bound(identity,multiply(a,inverse(b)))) = multiply(a,identity),
inference(cp,[status(thm)],[t112746,t58801]) ).
cnf(t270,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X2)) = greatest_lower_bound(multiply(X1,inverse(X2)),identity),
inference(cp,[status(thm)],[t33,t263]) ).
cnf(t174707,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X2)) = greatest_lower_bound(identity,multiply(X1,inverse(X2))),
inference(step,[status(thm)],[t270,t79]) ).
cnf(t2797,plain,
multiply(greatest_lower_bound(X1,X2),inverse(X2)) = greatest_lower_bound(identity,multiply(X1,inverse(X2))),
inference(orient,[status(thm)],[t174707]) ).
cnf(t175889,plain,
least_upper_bound(a,multiply(greatest_lower_bound(a,b),inverse(b))) = multiply(a,identity),
inference(step,[status(thm)],[t112750,t2797]) ).
cnf(t297,plain,
multiply(least_upper_bound(sFlat1,X1),inverse(b)) = least_upper_bound(a,multiply(X1,inverse(b))),
inference(cp,[status(thm)],[t27,t291]) ).
cnf(t6468,plain,
least_upper_bound(a,multiply(X1,inverse(b))) = multiply(least_upper_bound(sFlat1,X1),inverse(b)),
inference(orient,[status(thm)],[t297]) ).
cnf(t175890,plain,
multiply(least_upper_bound(sFlat1,greatest_lower_bound(a,b)),inverse(b)) = multiply(a,identity),
inference(step,[status(thm)],[t175889,t6468]) ).
cnf(t175891,plain,
multiply(least_upper_bound(sFlat1,greatest_lower_bound(b,a)),inverse(b)) = multiply(a,identity),
inference(step,[status(thm)],[t175890,t79]) ).
cnf(t175892,plain,
multiply(least_upper_bound(sFlat1,greatest_lower_bound(b,a)),inverse(b)) = a,
inference(step,[status(thm)],[t175891,t251]) ).
cnf(t132950,plain,
multiply(least_upper_bound(sFlat1,greatest_lower_bound(b,a)),inverse(b)) = a,
inference(orient,[status(thm)],[t175892]) ).
cnf(t133008,plain,
inverse(least_upper_bound(sFlat1,greatest_lower_bound(b,a))) = multiply(inverse(b),inverse(a)),
inference(cp,[status(thm)],[t5039,t132950]) ).
cnf(t842,plain,
inverse(sFlat1) = multiply(inverse(b),inverse(a)),
inference(cp,[status(thm)],[t150,t835]) ).
cnf(t854,plain,
multiply(inverse(b),inverse(a)) = inverse(sFlat1),
inference(orient,[status(thm)],[t842]) ).
cnf(t175893,plain,
inverse(least_upper_bound(sFlat1,greatest_lower_bound(b,a))) = inverse(sFlat1),
inference(step,[status(thm)],[t133008,t854]) ).
cnf(t133066,plain,
inverse(least_upper_bound(sFlat1,greatest_lower_bound(b,a))) = inverse(sFlat1),
inference(orient,[status(thm)],[t175893]) ).
cnf(t133074,plain,
least_upper_bound(sFlat1,greatest_lower_bound(b,a)) = inverse(inverse(sFlat1)),
inference(cp,[status(thm)],[t260,t133066]) ).
cnf(t175894,plain,
least_upper_bound(sFlat1,greatest_lower_bound(b,a)) = sFlat1,
inference(step,[status(thm)],[t133074,t260]) ).
cnf(t133261,plain,
least_upper_bound(sFlat1,greatest_lower_bound(b,a)) = sFlat1,
inference(orient,[status(thm)],[t175894]) ).
cnf(t133262,plain,
greatest_lower_bound(b,a) = greatest_lower_bound(greatest_lower_bound(b,a),sFlat1),
inference(cp,[status(thm)],[t1048,t133261]) ).
cnf(t175895,plain,
greatest_lower_bound(b,a) = greatest_lower_bound(b,greatest_lower_bound(a,sFlat1)),
inference(step,[status(thm)],[t133262,t80]) ).
cnf(t83,plain,
greatest_lower_bound(X1,greatest_lower_bound(X2,X3)) = greatest_lower_bound(X3,greatest_lower_bound(X1,X2)),
inference(cp,[status(thm)],[t80,t79]) ).
cnf(t147,plain,
greatest_lower_bound(X1,greatest_lower_bound(X2,X3)) = greatest_lower_bound(X3,greatest_lower_bound(X1,X2)),
inference(orient,[status(thm)],[t83]) ).
cnf(t175896,plain,
greatest_lower_bound(b,a) = greatest_lower_bound(sFlat1,greatest_lower_bound(b,a)),
inference(step,[status(thm)],[t175895,t147]) ).
cnf(t133286,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(b,a)) = greatest_lower_bound(b,a),
inference(orient,[status(thm)],[t175896]) ).
cnf(t176107,plain,
greatest_lower_bound(b,a) = greatest_lower_bound(a,multiply(greatest_lower_bound(identity,inverse(sFlat1)),sFlat1)),
inference(step,[status(thm)],[t176106,t133286]) ).
cnf(t176108,plain,
greatest_lower_bound(b,a) = greatest_lower_bound(sFlat1,greatest_lower_bound(a,multiply(inverse(sFlat1),sFlat1))),
inference(step,[status(thm)],[t176107,t168746]) ).
cnf(t176109,plain,
greatest_lower_bound(b,a) = greatest_lower_bound(sFlat1,greatest_lower_bound(a,identity)),
inference(step,[status(thm)],[t176108,t58]) ).
cnf(t176110,plain,
greatest_lower_bound(b,a) = greatest_lower_bound(sFlat1,greatest_lower_bound(identity,a)),
inference(step,[status(thm)],[t176109,t79]) ).
cnf(t106,plain,
multiply(a,greatest_lower_bound(multiply(b,X1),X2)) = greatest_lower_bound(multiply(sFlat1,X1),multiply(a,X2)),
inference(cp,[status(thm)],[t26,t100]) ).
cnf(t6672,plain,
greatest_lower_bound(multiply(sFlat1,X1),multiply(a,X2)) = multiply(a,greatest_lower_bound(multiply(b,X1),X2)),
inference(orient,[status(thm)],[t106]) ).
cnf(t6703,plain,
multiply(a,greatest_lower_bound(multiply(b,X1),identity)) = greatest_lower_bound(multiply(sFlat1,X1),a),
inference(cp,[status(thm)],[t6672,t251]) ).
cnf(t174823,plain,
multiply(a,greatest_lower_bound(identity,multiply(b,X1))) = greatest_lower_bound(multiply(sFlat1,X1),a),
inference(step,[status(thm)],[t6703,t79]) ).
cnf(t174824,plain,
multiply(a,greatest_lower_bound(identity,multiply(b,X1))) = greatest_lower_bound(a,multiply(sFlat1,X1)),
inference(step,[status(thm)],[t174823,t79]) ).
cnf(t11092,plain,
multiply(a,greatest_lower_bound(identity,multiply(b,X1))) = greatest_lower_bound(a,multiply(sFlat1,X1)),
inference(orient,[status(thm)],[t174824]) ).
cnf(t837,plain,
multiply(b,greatest_lower_bound(identity,inverse(sFlat1))) = greatest_lower_bound(b,inverse(a)),
inference(cp,[status(thm)],[t693,t835]) ).
cnf(t3997,plain,
multiply(b,greatest_lower_bound(identity,inverse(sFlat1))) = greatest_lower_bound(b,inverse(a)),
inference(orient,[status(thm)],[t837]) ).
cnf(t11106,plain,
greatest_lower_bound(a,multiply(sFlat1,greatest_lower_bound(identity,inverse(sFlat1)))) = multiply(a,greatest_lower_bound(identity,greatest_lower_bound(b,inverse(a)))),
inference(cp,[status(thm)],[t11092,t3997]) ).
cnf(t1087,plain,
greatest_lower_bound(identity,inverse(inverse(X1))) = multiply(X1,greatest_lower_bound(inverse(X1),identity)),
inference(cp,[status(thm)],[t1086,t260]) ).
cnf(t174661,plain,
greatest_lower_bound(identity,X1) = multiply(X1,greatest_lower_bound(inverse(X1),identity)),
inference(step,[status(thm)],[t1087,t260]) ).
cnf(t174662,plain,
greatest_lower_bound(identity,X1) = multiply(X1,greatest_lower_bound(identity,inverse(X1))),
inference(step,[status(thm)],[t174661,t79]) ).
cnf(t1556,plain,
multiply(X1,greatest_lower_bound(identity,inverse(X1))) = greatest_lower_bound(identity,X1),
inference(orient,[status(thm)],[t174662]) ).
cnf(t174825,plain,
greatest_lower_bound(a,greatest_lower_bound(identity,sFlat1)) = multiply(a,greatest_lower_bound(identity,greatest_lower_bound(b,inverse(a)))),
inference(step,[status(thm)],[t11106,t1556]) ).
cnf(t174826,plain,
greatest_lower_bound(a,greatest_lower_bound(sFlat1,identity)) = multiply(a,greatest_lower_bound(identity,greatest_lower_bound(b,inverse(a)))),
inference(step,[status(thm)],[t174825,t79]) ).
cnf(t174827,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(a,identity)) = multiply(a,greatest_lower_bound(identity,greatest_lower_bound(b,inverse(a)))),
inference(step,[status(thm)],[t174826,t149]) ).
cnf(t174828,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(identity,a)) = multiply(a,greatest_lower_bound(identity,greatest_lower_bound(b,inverse(a)))),
inference(step,[status(thm)],[t174827,t79]) ).
cnf(t2938,plain,
greatest_lower_bound(inverse(a),b) = greatest_lower_bound(inverse(a),greatest_lower_bound(identity,b)),
inference(cp,[status(thm)],[t2935,t1492]) ).
cnf(t174740,plain,
greatest_lower_bound(b,inverse(a)) = greatest_lower_bound(inverse(a),greatest_lower_bound(identity,b)),
inference(step,[status(thm)],[t2938,t79]) ).
cnf(t174741,plain,
greatest_lower_bound(b,inverse(a)) = greatest_lower_bound(identity,greatest_lower_bound(inverse(a),b)),
inference(step,[status(thm)],[t174740,t149]) ).
cnf(t174742,plain,
greatest_lower_bound(b,inverse(a)) = greatest_lower_bound(identity,greatest_lower_bound(b,inverse(a))),
inference(step,[status(thm)],[t174741,t79]) ).
cnf(t4175,plain,
greatest_lower_bound(identity,greatest_lower_bound(b,inverse(a))) = greatest_lower_bound(b,inverse(a)),
inference(orient,[status(thm)],[t174742]) ).
cnf(t174829,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(identity,a)) = multiply(a,greatest_lower_bound(b,inverse(a))),
inference(step,[status(thm)],[t174828,t4175]) ).
cnf(t174830,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(identity,a)) = greatest_lower_bound(identity,multiply(a,b)),
inference(step,[status(thm)],[t174829,t1908]) ).
cnf(t174831,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(identity,a)) = greatest_lower_bound(identity,sFlat1),
inference(step,[status(thm)],[t174830,t38]) ).
cnf(t174832,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(identity,a)) = greatest_lower_bound(sFlat1,identity),
inference(step,[status(thm)],[t174831,t79]) ).
cnf(t11155,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(identity,a)) = greatest_lower_bound(sFlat1,identity),
inference(orient,[status(thm)],[t174832]) ).
cnf(t176111,plain,
greatest_lower_bound(b,a) = greatest_lower_bound(sFlat1,identity),
inference(step,[status(thm)],[t176110,t11155]) ).
cnf(t171779,plain,
greatest_lower_bound(b,a) = greatest_lower_bound(sFlat1,identity),
inference(orient,[status(thm)],[t176111]) ).
cnf(t171825,plain,
greatest_lower_bound(b,multiply(sFlat0,inverse(b))) = multiply(b,multiply(greatest_lower_bound(sFlat1,identity),inverse(b))),
inference(cp,[status(thm)],[t109311,t171779]) ).
cnf(t292,plain,
multiply(greatest_lower_bound(identity,sFlat1),inverse(b)) = greatest_lower_bound(inverse(b),a),
inference(cp,[status(thm)],[t225,t291]) ).
cnf(t174725,plain,
multiply(greatest_lower_bound(sFlat1,identity),inverse(b)) = greatest_lower_bound(inverse(b),a),
inference(step,[status(thm)],[t292,t79]) ).
cnf(t174726,plain,
multiply(greatest_lower_bound(sFlat1,identity),inverse(b)) = greatest_lower_bound(a,inverse(b)),
inference(step,[status(thm)],[t174725,t79]) ).
cnf(t3509,plain,
multiply(greatest_lower_bound(sFlat1,identity),inverse(b)) = greatest_lower_bound(a,inverse(b)),
inference(orient,[status(thm)],[t174726]) ).
cnf(t176169,plain,
greatest_lower_bound(b,multiply(sFlat0,inverse(b))) = multiply(b,greatest_lower_bound(a,inverse(b))),
inference(step,[status(thm)],[t171825,t3509]) ).
cnf(t176170,plain,
greatest_lower_bound(b,multiply(sFlat0,inverse(b))) = greatest_lower_bound(identity,multiply(b,a)),
inference(step,[status(thm)],[t176169,t1908]) ).
cnf(t176171,plain,
greatest_lower_bound(b,multiply(sFlat0,inverse(b))) = greatest_lower_bound(identity,sFlat0),
inference(step,[status(thm)],[t176170,t48]) ).
cnf(t176172,plain,
greatest_lower_bound(b,multiply(sFlat0,inverse(b))) = greatest_lower_bound(sFlat0,identity),
inference(step,[status(thm)],[t176171,t79]) ).
cnf(t171947,plain,
greatest_lower_bound(b,multiply(sFlat0,inverse(b))) = greatest_lower_bound(sFlat0,identity),
inference(orient,[status(thm)],[t176172]) ).
cnf(t171964,plain,
greatest_lower_bound(multiply(inverse(sFlat0),b),inverse(b)) = multiply(inverse(sFlat0),greatest_lower_bound(sFlat0,identity)),
inference(cp,[status(thm)],[t13692,t171947]) ).
cnf(t176173,plain,
greatest_lower_bound(inverse(b),multiply(inverse(sFlat0),b)) = multiply(inverse(sFlat0),greatest_lower_bound(sFlat0,identity)),
inference(step,[status(thm)],[t171964,t79]) ).
cnf(t267,plain,
multiply(sFlat0,inverse(a)) = multiply(b,identity),
inference(cp,[status(thm)],[t120,t263]) ).
cnf(t174602,plain,
multiply(sFlat0,inverse(a)) = b,
inference(step,[status(thm)],[t267,t251]) ).
cnf(t278,plain,
multiply(sFlat0,inverse(a)) = b,
inference(orient,[status(thm)],[t174602]) ).
cnf(t281,plain,
inverse(a) = multiply(inverse(sFlat0),b),
inference(cp,[status(thm)],[t150,t278]) ).
cnf(t304,plain,
multiply(inverse(sFlat0),b) = inverse(a),
inference(orient,[status(thm)],[t281]) ).
cnf(t176174,plain,
greatest_lower_bound(inverse(b),inverse(a)) = multiply(inverse(sFlat0),greatest_lower_bound(sFlat0,identity)),
inference(step,[status(thm)],[t176173,t304]) ).
cnf(t176175,plain,
greatest_lower_bound(inverse(b),inverse(a)) = greatest_lower_bound(identity,inverse(sFlat0)),
inference(step,[status(thm)],[t176174,t1086]) ).
cnf(t171993,plain,
greatest_lower_bound(inverse(b),inverse(a)) = greatest_lower_bound(identity,inverse(sFlat0)),
inference(orient,[status(thm)],[t176175]) ).
cnf(t172002,plain,
greatest_lower_bound(identity,inverse(multiply(a,inverse(b)))) = multiply(inverse(inverse(b)),greatest_lower_bound(identity,inverse(sFlat0))),
inference(cp,[status(thm)],[t38249,t171993]) ).
cnf(t243,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(cp,[status(thm)],[t241,t150]) ).
cnf(t542,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t243]) ).
cnf(t5191,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(cp,[status(thm)],[t542,t5039]) ).
cnf(t5241,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t5191]) ).
cnf(t176190,plain,
greatest_lower_bound(identity,multiply(b,inverse(a))) = multiply(inverse(inverse(b)),greatest_lower_bound(identity,inverse(sFlat0))),
inference(step,[status(thm)],[t172002,t5241]) ).
cnf(t176191,plain,
multiply(greatest_lower_bound(b,a),inverse(a)) = multiply(inverse(inverse(b)),greatest_lower_bound(identity,inverse(sFlat0))),
inference(step,[status(thm)],[t176190,t2797]) ).
cnf(t176192,plain,
multiply(greatest_lower_bound(sFlat1,identity),inverse(a)) = multiply(inverse(inverse(b)),greatest_lower_bound(identity,inverse(sFlat0))),
inference(step,[status(thm)],[t176191,t171779]) ).
cnf(t176193,plain,
multiply(greatest_lower_bound(sFlat1,identity),inverse(a)) = multiply(b,greatest_lower_bound(identity,inverse(sFlat0))),
inference(step,[status(thm)],[t176192,t241]) ).
cnf(t172451,plain,
multiply(greatest_lower_bound(sFlat1,identity),inverse(a)) = multiply(b,greatest_lower_bound(identity,inverse(sFlat0))),
inference(orient,[status(thm)],[t176193]) ).
cnf(t78,plain,
least_upper_bound(X1,X2) = greatest_lower_bound(least_upper_bound(X1,X2),least_upper_bound(X1,least_upper_bound(X2,X3))),
inference(cp,[status(thm)],[t22,t69]) ).
cnf(t8662,plain,
greatest_lower_bound(least_upper_bound(X1,X2),least_upper_bound(X1,least_upper_bound(X2,X3))) = least_upper_bound(X1,X2),
inference(orient,[status(thm)],[t78]) ).
cnf(t8666,plain,
least_upper_bound(X1,X2) = greatest_lower_bound(least_upper_bound(X1,X2),least_upper_bound(X2,least_upper_bound(X3,X1))),
inference(cp,[status(thm)],[t8662,t144]) ).
cnf(t16716,plain,
greatest_lower_bound(least_upper_bound(X1,X2),least_upper_bound(X2,least_upper_bound(X3,X1))) = least_upper_bound(X1,X2),
inference(orient,[status(thm)],[t8666]) ).
cnf(t16743,plain,
least_upper_bound(greatest_lower_bound(X1,X2),X3) = greatest_lower_bound(least_upper_bound(greatest_lower_bound(X1,X2),X3),least_upper_bound(X3,X1)),
inference(cp,[status(thm)],[t16716,t20]) ).
cnf(t175389,plain,
least_upper_bound(greatest_lower_bound(X1,X2),X3) = greatest_lower_bound(least_upper_bound(X3,X1),least_upper_bound(greatest_lower_bound(X1,X2),X3)),
inference(step,[status(thm)],[t16743,t79]) ).
cnf(t79148,plain,
greatest_lower_bound(least_upper_bound(X1,X2),least_upper_bound(greatest_lower_bound(X2,X3),X1)) = least_upper_bound(greatest_lower_bound(X2,X3),X1),
inference(orient,[status(thm)],[t175389]) ).
cnf(t133266,plain,
least_upper_bound(greatest_lower_bound(greatest_lower_bound(b,a),X1),sFlat1) = greatest_lower_bound(sFlat1,least_upper_bound(greatest_lower_bound(greatest_lower_bound(b,a),X1),sFlat1)),
inference(cp,[status(thm)],[t79148,t133261]) ).
cnf(t175911,plain,
least_upper_bound(sFlat1,greatest_lower_bound(greatest_lower_bound(b,a),X1)) = greatest_lower_bound(sFlat1,least_upper_bound(greatest_lower_bound(greatest_lower_bound(b,a),X1),sFlat1)),
inference(step,[status(thm)],[t133266,t68]) ).
cnf(t175912,plain,
least_upper_bound(sFlat1,greatest_lower_bound(b,greatest_lower_bound(a,X1))) = greatest_lower_bound(sFlat1,least_upper_bound(greatest_lower_bound(greatest_lower_bound(b,a),X1),sFlat1)),
inference(step,[status(thm)],[t175911,t80]) ).
cnf(t175913,plain,
least_upper_bound(sFlat1,greatest_lower_bound(b,greatest_lower_bound(a,X1))) = sFlat1,
inference(step,[status(thm)],[t175912,t1048]) ).
cnf(t133327,plain,
least_upper_bound(sFlat1,greatest_lower_bound(b,greatest_lower_bound(a,X1))) = sFlat1,
inference(orient,[status(thm)],[t175913]) ).
cnf(t49,plain,
multiply(greatest_lower_bound(b,X1),a) = greatest_lower_bound(sFlat0,multiply(X1,a)),
inference(cp,[status(thm)],[t33,t48]) ).
cnf(t352,plain,
greatest_lower_bound(sFlat0,multiply(X1,a)) = multiply(greatest_lower_bound(b,X1),a),
inference(orient,[status(thm)],[t49]) ).
cnf(t13705,plain,
greatest_lower_bound(multiply(inverse(X1),sFlat0),a) = multiply(inverse(X1),multiply(greatest_lower_bound(b,X1),a)),
inference(cp,[status(thm)],[t13692,t352]) ).
cnf(t175141,plain,
greatest_lower_bound(a,multiply(inverse(X1),sFlat0)) = multiply(inverse(X1),multiply(greatest_lower_bound(b,X1),a)),
inference(step,[status(thm)],[t13705,t79]) ).
cnf(t48338,plain,
multiply(inverse(X1),multiply(greatest_lower_bound(b,X1),a)) = greatest_lower_bound(a,multiply(inverse(X1),sFlat0)),
inference(orient,[status(thm)],[t175141]) ).
cnf(t171833,plain,
greatest_lower_bound(a,multiply(inverse(a),sFlat0)) = multiply(inverse(a),multiply(greatest_lower_bound(sFlat1,identity),a)),
inference(cp,[status(thm)],[t48338,t171779]) ).
cnf(t829,plain,
multiply(inverse(a),greatest_lower_bound(multiply(sFlat1,X1),X2)) = greatest_lower_bound(multiply(b,X1),multiply(inverse(a),X2)),
inference(cp,[status(thm)],[t26,t818]) ).
cnf(t101181,plain,
greatest_lower_bound(multiply(b,X1),multiply(inverse(a),X2)) = multiply(inverse(a),greatest_lower_bound(multiply(sFlat1,X1),X2)),
inference(orient,[status(thm)],[t829]) ).
cnf(t101182,plain,
multiply(inverse(a),greatest_lower_bound(multiply(sFlat1,X1),X1)) = multiply(greatest_lower_bound(b,inverse(a)),X1),
inference(cp,[status(thm)],[t101181,t33]) ).
cnf(t175626,plain,
multiply(inverse(a),greatest_lower_bound(X1,multiply(sFlat1,X1))) = multiply(greatest_lower_bound(b,inverse(a)),X1),
inference(step,[status(thm)],[t101182,t79]) ).
cnf(t175627,plain,
multiply(inverse(a),multiply(greatest_lower_bound(identity,sFlat1),X1)) = multiply(greatest_lower_bound(b,inverse(a)),X1),
inference(step,[status(thm)],[t175626,t225]) ).
cnf(t175628,plain,
multiply(inverse(a),multiply(greatest_lower_bound(sFlat1,identity),X1)) = multiply(greatest_lower_bound(b,inverse(a)),X1),
inference(step,[status(thm)],[t175627,t79]) ).
cnf(t111437,plain,
multiply(inverse(a),multiply(greatest_lower_bound(sFlat1,identity),X1)) = multiply(greatest_lower_bound(b,inverse(a)),X1),
inference(orient,[status(thm)],[t175628]) ).
cnf(t176176,plain,
greatest_lower_bound(a,multiply(inverse(a),sFlat0)) = multiply(greatest_lower_bound(b,inverse(a)),a),
inference(step,[status(thm)],[t171833,t111437]) ).
cnf(t176177,plain,
greatest_lower_bound(a,multiply(inverse(a),sFlat0)) = greatest_lower_bound(identity,multiply(b,a)),
inference(step,[status(thm)],[t176176,t624]) ).
cnf(t176178,plain,
greatest_lower_bound(a,multiply(inverse(a),sFlat0)) = greatest_lower_bound(identity,sFlat0),
inference(step,[status(thm)],[t176177,t48]) ).
cnf(t176179,plain,
greatest_lower_bound(a,multiply(inverse(a),sFlat0)) = greatest_lower_bound(sFlat0,identity),
inference(step,[status(thm)],[t176178,t79]) ).
cnf(t172053,plain,
greatest_lower_bound(a,multiply(inverse(a),sFlat0)) = greatest_lower_bound(sFlat0,identity),
inference(orient,[status(thm)],[t176179]) ).
cnf(t172056,plain,
sFlat1 = least_upper_bound(sFlat1,greatest_lower_bound(b,greatest_lower_bound(sFlat0,identity))),
inference(cp,[status(thm)],[t133327,t172053]) ).
cnf(t176199,plain,
sFlat1 = least_upper_bound(sFlat1,greatest_lower_bound(sFlat0,greatest_lower_bound(b,identity))),
inference(step,[status(thm)],[t172056,t149]) ).
cnf(t176200,plain,
sFlat1 = least_upper_bound(sFlat1,greatest_lower_bound(sFlat0,greatest_lower_bound(identity,b))),
inference(step,[status(thm)],[t176199,t79]) ).
cnf(t154,plain,
multiply(a,X1) = multiply(inverse(b),multiply(sFlat0,X1)),
inference(cp,[status(thm)],[t150,t120]) ).
cnf(t766,plain,
multiply(inverse(b),multiply(sFlat0,X1)) = multiply(a,X1),
inference(orient,[status(thm)],[t154]) ).
cnf(t768,plain,
multiply(a,inverse(sFlat0)) = multiply(inverse(b),identity),
inference(cp,[status(thm)],[t766,t263]) ).
cnf(t174634,plain,
multiply(a,inverse(sFlat0)) = inverse(b),
inference(step,[status(thm)],[t768,t251]) ).
cnf(t783,plain,
multiply(a,inverse(sFlat0)) = inverse(b),
inference(orient,[status(thm)],[t174634]) ).
cnf(t785,plain,
multiply(a,greatest_lower_bound(identity,inverse(sFlat0))) = greatest_lower_bound(a,inverse(b)),
inference(cp,[status(thm)],[t693,t783]) ).
cnf(t3901,plain,
multiply(a,greatest_lower_bound(identity,inverse(sFlat0))) = greatest_lower_bound(a,inverse(b)),
inference(orient,[status(thm)],[t785]) ).
cnf(t11244,plain,
greatest_lower_bound(b,multiply(sFlat0,greatest_lower_bound(identity,inverse(sFlat0)))) = multiply(b,greatest_lower_bound(identity,greatest_lower_bound(a,inverse(b)))),
inference(cp,[status(thm)],[t11228,t3901]) ).
cnf(t174837,plain,
greatest_lower_bound(b,greatest_lower_bound(identity,sFlat0)) = multiply(b,greatest_lower_bound(identity,greatest_lower_bound(a,inverse(b)))),
inference(step,[status(thm)],[t11244,t1556]) ).
cnf(t174838,plain,
greatest_lower_bound(b,greatest_lower_bound(sFlat0,identity)) = multiply(b,greatest_lower_bound(identity,greatest_lower_bound(a,inverse(b)))),
inference(step,[status(thm)],[t174837,t79]) ).
cnf(t174839,plain,
greatest_lower_bound(sFlat0,greatest_lower_bound(b,identity)) = multiply(b,greatest_lower_bound(identity,greatest_lower_bound(a,inverse(b)))),
inference(step,[status(thm)],[t174838,t149]) ).
cnf(t174840,plain,
greatest_lower_bound(sFlat0,greatest_lower_bound(identity,b)) = multiply(b,greatest_lower_bound(identity,greatest_lower_bound(a,inverse(b)))),
inference(step,[status(thm)],[t174839,t79]) ).
cnf(t174841,plain,
greatest_lower_bound(sFlat0,greatest_lower_bound(identity,b)) = multiply(b,greatest_lower_bound(a,inverse(b))),
inference(step,[status(thm)],[t174840,t9252]) ).
cnf(t174842,plain,
greatest_lower_bound(sFlat0,greatest_lower_bound(identity,b)) = greatest_lower_bound(identity,multiply(b,a)),
inference(step,[status(thm)],[t174841,t1908]) ).
cnf(t174843,plain,
greatest_lower_bound(sFlat0,greatest_lower_bound(identity,b)) = greatest_lower_bound(identity,sFlat0),
inference(step,[status(thm)],[t174842,t48]) ).
cnf(t174844,plain,
greatest_lower_bound(sFlat0,greatest_lower_bound(identity,b)) = greatest_lower_bound(sFlat0,identity),
inference(step,[status(thm)],[t174843,t79]) ).
cnf(t11295,plain,
greatest_lower_bound(sFlat0,greatest_lower_bound(identity,b)) = greatest_lower_bound(sFlat0,identity),
inference(orient,[status(thm)],[t174844]) ).
cnf(t176201,plain,
sFlat1 = least_upper_bound(sFlat1,greatest_lower_bound(sFlat0,identity)),
inference(step,[status(thm)],[t176200,t11295]) ).
cnf(t172796,plain,
least_upper_bound(sFlat1,greatest_lower_bound(sFlat0,identity)) = sFlat1,
inference(orient,[status(thm)],[t176201]) ).
cnf(t172797,plain,
greatest_lower_bound(sFlat0,identity) = greatest_lower_bound(greatest_lower_bound(sFlat0,identity),sFlat1),
inference(cp,[status(thm)],[t1048,t172796]) ).
cnf(t176202,plain,
greatest_lower_bound(sFlat0,identity) = greatest_lower_bound(sFlat0,greatest_lower_bound(identity,sFlat1)),
inference(step,[status(thm)],[t172797,t80]) ).
cnf(t176203,plain,
greatest_lower_bound(sFlat0,identity) = greatest_lower_bound(sFlat0,greatest_lower_bound(sFlat1,identity)),
inference(step,[status(thm)],[t176202,t79]) ).
cnf(t273,plain,
multiply(X1,greatest_lower_bound(inverse(X1),X2)) = greatest_lower_bound(identity,multiply(X1,X2)),
inference(cp,[status(thm)],[t26,t263]) ).
cnf(t1868,plain,
multiply(X1,greatest_lower_bound(inverse(X1),X2)) = greatest_lower_bound(identity,multiply(X1,X2)),
inference(orient,[status(thm)],[t273]) ).
cnf(t1883,plain,
multiply(X1,least_upper_bound(identity,greatest_lower_bound(inverse(X1),X2))) = least_upper_bound(X1,greatest_lower_bound(identity,multiply(X1,X2))),
inference(cp,[status(thm)],[t729,t1868]) ).
cnf(t111740,plain,
multiply(X1,least_upper_bound(identity,greatest_lower_bound(inverse(X1),X2))) = least_upper_bound(X1,greatest_lower_bound(identity,multiply(X1,X2))),
inference(orient,[status(thm)],[t1883]) ).
cnf(t111744,plain,
least_upper_bound(b,greatest_lower_bound(identity,multiply(b,inverse(a)))) = multiply(b,identity),
inference(cp,[status(thm)],[t111740,t58801]) ).
cnf(t175864,plain,
least_upper_bound(b,multiply(greatest_lower_bound(b,a),inverse(a))) = multiply(b,identity),
inference(step,[status(thm)],[t111744,t2797]) ).
cnf(t284,plain,
multiply(least_upper_bound(sFlat0,X1),inverse(a)) = least_upper_bound(b,multiply(X1,inverse(a))),
inference(cp,[status(thm)],[t27,t278]) ).
cnf(t6428,plain,
least_upper_bound(b,multiply(X1,inverse(a))) = multiply(least_upper_bound(sFlat0,X1),inverse(a)),
inference(orient,[status(thm)],[t284]) ).
cnf(t175865,plain,
multiply(least_upper_bound(sFlat0,greatest_lower_bound(b,a)),inverse(a)) = multiply(b,identity),
inference(step,[status(thm)],[t175864,t6428]) ).
cnf(t175866,plain,
multiply(least_upper_bound(sFlat0,greatest_lower_bound(b,a)),inverse(a)) = b,
inference(step,[status(thm)],[t175865,t251]) ).
cnf(t132451,plain,
multiply(least_upper_bound(sFlat0,greatest_lower_bound(b,a)),inverse(a)) = b,
inference(orient,[status(thm)],[t175866]) ).
cnf(t132509,plain,
inverse(least_upper_bound(sFlat0,greatest_lower_bound(b,a))) = multiply(inverse(a),inverse(b)),
inference(cp,[status(thm)],[t5039,t132451]) ).
cnf(t790,plain,
inverse(sFlat0) = multiply(inverse(a),inverse(b)),
inference(cp,[status(thm)],[t150,t783]) ).
cnf(t802,plain,
multiply(inverse(a),inverse(b)) = inverse(sFlat0),
inference(orient,[status(thm)],[t790]) ).
cnf(t175867,plain,
inverse(least_upper_bound(sFlat0,greatest_lower_bound(b,a))) = inverse(sFlat0),
inference(step,[status(thm)],[t132509,t802]) ).
cnf(t132567,plain,
inverse(least_upper_bound(sFlat0,greatest_lower_bound(b,a))) = inverse(sFlat0),
inference(orient,[status(thm)],[t175867]) ).
cnf(t132575,plain,
least_upper_bound(sFlat0,greatest_lower_bound(b,a)) = inverse(inverse(sFlat0)),
inference(cp,[status(thm)],[t260,t132567]) ).
cnf(t175868,plain,
least_upper_bound(sFlat0,greatest_lower_bound(b,a)) = sFlat0,
inference(step,[status(thm)],[t132575,t260]) ).
cnf(t132762,plain,
least_upper_bound(sFlat0,greatest_lower_bound(b,a)) = sFlat0,
inference(orient,[status(thm)],[t175868]) ).
cnf(t132763,plain,
greatest_lower_bound(b,a) = greatest_lower_bound(greatest_lower_bound(b,a),sFlat0),
inference(cp,[status(thm)],[t1048,t132762]) ).
cnf(t175869,plain,
greatest_lower_bound(b,a) = greatest_lower_bound(b,greatest_lower_bound(a,sFlat0)),
inference(step,[status(thm)],[t132763,t80]) ).
cnf(t175870,plain,
greatest_lower_bound(b,a) = greatest_lower_bound(sFlat0,greatest_lower_bound(b,a)),
inference(step,[status(thm)],[t175869,t147]) ).
cnf(t132787,plain,
greatest_lower_bound(sFlat0,greatest_lower_bound(b,a)) = greatest_lower_bound(b,a),
inference(orient,[status(thm)],[t175870]) ).
cnf(t176158,plain,
greatest_lower_bound(sFlat0,greatest_lower_bound(sFlat1,identity)) = greatest_lower_bound(b,a),
inference(step,[status(thm)],[t132787,t171779]) ).
cnf(t176159,plain,
greatest_lower_bound(sFlat0,greatest_lower_bound(sFlat1,identity)) = greatest_lower_bound(sFlat1,identity),
inference(step,[status(thm)],[t176158,t171779]) ).
cnf(t171859,plain,
greatest_lower_bound(sFlat0,greatest_lower_bound(sFlat1,identity)) = greatest_lower_bound(sFlat1,identity),
inference(rw,[status(thm)],[t176159]) ).
cnf(t171895,plain,
greatest_lower_bound(sFlat0,greatest_lower_bound(sFlat1,identity)) = greatest_lower_bound(sFlat1,identity),
inference(orient,[status(thm)],[t171859]) ).
cnf(t176204,plain,
greatest_lower_bound(sFlat0,identity) = greatest_lower_bound(sFlat1,identity),
inference(step,[status(thm)],[t176203,t171895]) ).
cnf(t172823,plain,
greatest_lower_bound(sFlat1,identity) = greatest_lower_bound(sFlat0,identity),
inference(orient,[status(thm)],[t176204]) ).
cnf(t176286,plain,
multiply(greatest_lower_bound(sFlat0,identity),inverse(a)) = multiply(b,greatest_lower_bound(identity,inverse(sFlat0))),
inference(step,[status(thm)],[t172451,t172823]) ).
cnf(t279,plain,
multiply(greatest_lower_bound(identity,sFlat0),inverse(a)) = greatest_lower_bound(inverse(a),b),
inference(cp,[status(thm)],[t225,t278]) ).
cnf(t174721,plain,
multiply(greatest_lower_bound(sFlat0,identity),inverse(a)) = greatest_lower_bound(inverse(a),b),
inference(step,[status(thm)],[t279,t79]) ).
cnf(t174722,plain,
multiply(greatest_lower_bound(sFlat0,identity),inverse(a)) = greatest_lower_bound(b,inverse(a)),
inference(step,[status(thm)],[t174721,t79]) ).
cnf(t3463,plain,
multiply(greatest_lower_bound(sFlat0,identity),inverse(a)) = greatest_lower_bound(b,inverse(a)),
inference(orient,[status(thm)],[t174722]) ).
cnf(t176287,plain,
greatest_lower_bound(b,inverse(a)) = multiply(b,greatest_lower_bound(identity,inverse(sFlat0))),
inference(step,[status(thm)],[t176286,t3463]) ).
cnf(t172941,plain,
greatest_lower_bound(b,inverse(a)) = multiply(b,greatest_lower_bound(identity,inverse(sFlat0))),
inference(rw,[status(thm)],[t176287]) ).
cnf(t173713,plain,
multiply(b,greatest_lower_bound(identity,inverse(sFlat0))) = greatest_lower_bound(b,inverse(a)),
inference(orient,[status(thm)],[t172941]) ).
cnf(t173739,plain,
greatest_lower_bound(identity,inverse(sFlat0)) = multiply(inverse(b),greatest_lower_bound(b,inverse(a))),
inference(cp,[status(thm)],[t150,t173713]) ).
cnf(t165,plain,
multiply(inverse(X1),greatest_lower_bound(multiply(X1,X2),X3)) = greatest_lower_bound(X2,multiply(inverse(X1),X3)),
inference(cp,[status(thm)],[t26,t150]) ).
cnf(t13405,plain,
multiply(inverse(X1),greatest_lower_bound(multiply(X1,X2),X3)) = greatest_lower_bound(X2,multiply(inverse(X1),X3)),
inference(orient,[status(thm)],[t165]) ).
cnf(t13599,plain,
greatest_lower_bound(inverse(sFlat1),multiply(inverse(b),X1)) = multiply(inverse(b),greatest_lower_bound(inverse(a),X1)),
inference(cp,[status(thm)],[t13405,t835]) ).
cnf(t24422,plain,
greatest_lower_bound(inverse(sFlat1),multiply(inverse(b),X1)) = multiply(inverse(b),greatest_lower_bound(inverse(a),X1)),
inference(orient,[status(thm)],[t13599]) ).
cnf(t24431,plain,
multiply(inverse(b),greatest_lower_bound(inverse(a),b)) = greatest_lower_bound(inverse(sFlat1),identity),
inference(cp,[status(thm)],[t24422,t58]) ).
cnf(t174943,plain,
multiply(inverse(b),greatest_lower_bound(b,inverse(a))) = greatest_lower_bound(inverse(sFlat1),identity),
inference(step,[status(thm)],[t24431,t79]) ).
cnf(t174944,plain,
multiply(inverse(b),greatest_lower_bound(b,inverse(a))) = greatest_lower_bound(identity,inverse(sFlat1)),
inference(step,[status(thm)],[t174943,t79]) ).
cnf(t24510,plain,
multiply(inverse(b),greatest_lower_bound(b,inverse(a))) = greatest_lower_bound(identity,inverse(sFlat1)),
inference(orient,[status(thm)],[t174944]) ).
cnf(t176310,plain,
greatest_lower_bound(identity,inverse(sFlat0)) = greatest_lower_bound(identity,inverse(sFlat1)),
inference(step,[status(thm)],[t173739,t24510]) ).
cnf(t173850,plain,
greatest_lower_bound(identity,inverse(sFlat1)) = greatest_lower_bound(identity,inverse(sFlat0)),
inference(orient,[status(thm)],[t176310]) ).
cnf(t173925,plain,
sFlat1 = multiply(greatest_lower_bound(sFlat1,identity),inverse(greatest_lower_bound(identity,inverse(sFlat0)))),
inference(cp,[status(thm)],[t78908,t173850]) ).
cnf(t176339,plain,
sFlat1 = multiply(greatest_lower_bound(sFlat0,identity),inverse(greatest_lower_bound(identity,inverse(sFlat0)))),
inference(step,[status(thm)],[t173925,t172823]) ).
cnf(t176340,plain,
sFlat1 = sFlat0,
inference(step,[status(thm)],[t176339,t78908]) ).
cnf(t173958,plain,
sFlat1 = sFlat0,
inference(orient,[status(thm)],[t176340]) ).
cnf(t176341,plain,
multiply(a,b) = sFlat0,
inference(step,[status(thm)],[t38,t173958]) ).
cnf(t173959,plain,
multiply(a,b) = sFlat0,
inference(orient,[status(thm)],[t176341]) ).
cnf(goal_0,negated_conjecture,
multiply(b,a) != multiply(a,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
sFlat0 != multiply(a,b),
inference(rw,[status(thm)],[goal_0,t48]) ).
cnf(g0_1,plain,
sFlat0 != sFlat0,
inference(rw,[status(thm)],[g0_0,t173959]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP187-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.13/0.41 % Computer : n014.cluster.edu
% 0.13/0.41 % Model : x86_64 x86_64
% 0.13/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.41 % Memory : 8046.5625MB
% 0.13/0.41 % OS : Linux 6.8.0-71-generic
% 0.13/0.41 % CPULimit : 300
% 0.13/0.41 % WCLimit : 300
% 0.13/0.41 % DateTime : Wed Sep 23 14:04:19 UTC 2026
% 0.13/0.41 % CPUTime :
% 0.13/0.41 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 91.82/13.82 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 91.82/13.82 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------