%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP183-2 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:25:35 PM UTC 2026
% Result : Unsatisfiable 19.44s 8.08s
% Output : CNFRefutation 19.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 89
% Number of leaves : 23
% Syntax : Number of clauses : 420 ( 420 unt; 0 nHn; 239 RR)
% Number of literals : 420 ( 419 equ; 10 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 : 10 ( 10 usr; 6 con; 0-2 aty)
% Number of variables : 263 ( 23 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t8,axiom,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t88,plain,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t14,axiom,
greatest_lower_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,greatest_lower_bound(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t29,plain,
greatest_lower_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,greatest_lower_bound(X2,X3)),
inference(orient,[status(thm)],[t14]) ).
cnf(t2,axiom,
inverse(inverse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t27,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t10,axiom,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t54,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t10]) ).
cnf(t0,axiom,
inverse(identity) = identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t105,plain,
inverse(identity) = identity,
inference(orient,[status(thm)],[t0]) ).
cnf(t106,plain,
inverse(multiply(X1,identity)) = multiply(identity,inverse(X1)),
inference(cp,[status(thm)],[t54,t105]) ).
cnf(t4,axiom,
multiply(identity,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t23966,plain,
inverse(multiply(X1,identity)) = inverse(X1),
inference(step,[status(thm)],[t106,t22]) ).
cnf(t158,plain,
inverse(multiply(X1,identity)) = inverse(X1),
inference(orient,[status(thm)],[t23966]) ).
cnf(t162,plain,
multiply(X1,identity) = inverse(inverse(X1)),
inference(cp,[status(thm)],[t27,t158]) ).
cnf(t23967,plain,
multiply(X1,identity) = X1,
inference(step,[status(thm)],[t162,t27]) ).
cnf(t163,plain,
multiply(X1,identity) = X1,
inference(orient,[status(thm)],[t23967]) ).
cnf(t166,plain,
multiply(X1,greatest_lower_bound(identity,X2)) = greatest_lower_bound(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t29,t163]) ).
cnf(t1879,plain,
greatest_lower_bound(X1,multiply(X1,X2)) = multiply(X1,greatest_lower_bound(identity,X2)),
inference(orient,[status(thm)],[t166]) ).
cnf(t57,plain,
inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(cp,[status(thm)],[t54,t27]) ).
cnf(t1690,plain,
inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(orient,[status(thm)],[t57]) ).
cnf(t13,axiom,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t28,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/sandbox/benchmark/theBenchmark.p') ).
cnf(t43,plain,
multiply(inverse(X1),X1) = identity,
inference(orient,[status(thm)],[t5]) ).
cnf(t53,plain,
multiply(inverse(X1),multiply(X1,X2)) = multiply(identity,X2),
inference(cp,[status(thm)],[t28,t43]) ).
cnf(t24018,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(step,[status(thm)],[t53,t22]) ).
cnf(t1013,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(orient,[status(thm)],[t24018]) ).
cnf(t1691,plain,
multiply(inverse(multiply(X1,X2)),X1) = inverse(X2),
inference(cp,[status(thm)],[t1690,t1013]) ).
cnf(t1717,plain,
multiply(inverse(multiply(X1,X2)),X1) = inverse(X2),
inference(orient,[status(thm)],[t1691]) ).
cnf(t52,plain,
multiply(inverse(X1),greatest_lower_bound(X2,X1)) = greatest_lower_bound(multiply(inverse(X1),X2),identity),
inference(cp,[status(thm)],[t29,t43]) ).
cnf(t6,axiom,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t67,plain,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t24364,plain,
multiply(inverse(X1),greatest_lower_bound(X2,X1)) = greatest_lower_bound(identity,multiply(inverse(X1),X2)),
inference(step,[status(thm)],[t52,t67]) ).
cnf(t10059,plain,
multiply(inverse(X1),greatest_lower_bound(X2,X1)) = greatest_lower_bound(identity,multiply(inverse(X1),X2)),
inference(orient,[status(thm)],[t24364]) ).
cnf(t7,axiom,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t24,plain,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t91,plain,
X1 = greatest_lower_bound(X1,least_upper_bound(X2,X1)),
inference(cp,[status(thm)],[t24,t88]) ).
cnf(t181,plain,
greatest_lower_bound(X1,least_upper_bound(X2,X1)) = X1,
inference(orient,[status(thm)],[t91]) ).
cnf(t9,axiom,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t26,plain,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t183,plain,
greatest_lower_bound(X1,X2) = greatest_lower_bound(greatest_lower_bound(X1,X2),X1),
inference(cp,[status(thm)],[t181,t26]) ).
cnf(t11,axiom,
greatest_lower_bound(greatest_lower_bound(X1,X2),X3) = greatest_lower_bound(X1,greatest_lower_bound(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t71,plain,
greatest_lower_bound(greatest_lower_bound(X1,X2),X3) = greatest_lower_bound(X1,greatest_lower_bound(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t23980,plain,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X1,greatest_lower_bound(X2,X1)),
inference(step,[status(thm)],[t183,t71]) ).
cnf(t438,plain,
greatest_lower_bound(X1,greatest_lower_bound(X2,X1)) = greatest_lower_bound(X1,X2),
inference(orient,[status(thm)],[t23980]) ).
cnf(t15,axiom,
greatest_lower_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(greatest_lower_bound(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t32,plain,
greatest_lower_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(greatest_lower_bound(X1,X3),X2),
inference(orient,[status(thm)],[t15]) ).
cnf(t33,plain,
multiply(greatest_lower_bound(identity,X1),X2) = greatest_lower_bound(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t32,t22]) ).
cnf(t273,plain,
greatest_lower_bound(X1,multiply(X2,X1)) = multiply(greatest_lower_bound(identity,X2),X1),
inference(orient,[status(thm)],[t33]) ).
cnf(t1880,plain,
multiply(X1,greatest_lower_bound(identity,X1)) = multiply(greatest_lower_bound(identity,X1),X1),
inference(cp,[status(thm)],[t1879,t273]) ).
cnf(t2399,plain,
multiply(greatest_lower_bound(identity,X1),X1) = multiply(X1,greatest_lower_bound(identity,X1)),
inference(orient,[status(thm)],[t1880]) ).
cnf(t19,axiom,
sFlat1 = greatest_lower_bound(a,identity),
introduced(definition) ).
cnf(t23959,plain,
sFlat1 = greatest_lower_bound(identity,a),
inference(step,[status(thm)],[t19,t67]) ).
cnf(t84,plain,
greatest_lower_bound(identity,a) = sFlat1,
inference(orient,[status(thm)],[t23959]) ).
cnf(t2410,plain,
multiply(a,greatest_lower_bound(identity,a)) = multiply(sFlat1,a),
inference(cp,[status(thm)],[t2399,t84]) ).
cnf(t24097,plain,
multiply(a,sFlat1) = multiply(sFlat1,a),
inference(step,[status(thm)],[t2410,t84]) ).
cnf(t2440,plain,
multiply(a,sFlat1) = multiply(sFlat1,a),
inference(orient,[status(thm)],[t24097]) ).
cnf(t2455,plain,
multiply(a,multiply(sFlat1,X1)) = multiply(multiply(sFlat1,a),X1),
inference(cp,[status(thm)],[t28,t2440]) ).
cnf(t24165,plain,
multiply(a,multiply(sFlat1,X1)) = multiply(sFlat1,multiply(a,X1)),
inference(step,[status(thm)],[t2455,t28]) ).
cnf(t3269,plain,
multiply(a,multiply(sFlat1,X1)) = multiply(sFlat1,multiply(a,X1)),
inference(orient,[status(thm)],[t24165]) ).
cnf(t86,plain,
identity = least_upper_bound(identity,sFlat1),
inference(cp,[status(thm)],[t26,t84]) ).
cnf(t23964,plain,
identity = least_upper_bound(sFlat1,identity),
inference(step,[status(thm)],[t86,t88]) ).
cnf(t117,plain,
least_upper_bound(sFlat1,identity) = identity,
inference(orient,[status(thm)],[t23964]) ).
cnf(t118,plain,
sFlat1 = greatest_lower_bound(sFlat1,identity),
inference(cp,[status(thm)],[t24,t117]) ).
cnf(t143,plain,
greatest_lower_bound(sFlat1,identity) = sFlat1,
inference(orient,[status(thm)],[t118]) ).
cnf(t144,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(identity,X1)) = greatest_lower_bound(sFlat1,X1),
inference(cp,[status(thm)],[t71,t143]) ).
cnf(t409,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(identity,X1)) = greatest_lower_bound(sFlat1,X1),
inference(orient,[status(thm)],[t144]) ).
cnf(t20,axiom,
sFlat2 = inverse(greatest_lower_bound(a,identity)),
introduced(definition) ).
cnf(t23962,plain,
sFlat2 = inverse(greatest_lower_bound(identity,a)),
inference(step,[status(thm)],[t20,t67]) ).
cnf(t23963,plain,
sFlat2 = inverse(sFlat1),
inference(step,[status(thm)],[t23962,t84]) ).
cnf(t108,plain,
inverse(sFlat1) = sFlat2,
inference(orient,[status(thm)],[t23963]) ).
cnf(t109,plain,
inverse(multiply(X1,sFlat1)) = multiply(sFlat2,inverse(X1)),
inference(cp,[status(thm)],[t54,t108]) ).
cnf(t212,plain,
inverse(multiply(X1,sFlat1)) = multiply(sFlat2,inverse(X1)),
inference(orient,[status(thm)],[t109]) ).
cnf(t2446,plain,
multiply(sFlat2,inverse(a)) = inverse(multiply(sFlat1,a)),
inference(cp,[status(thm)],[t212,t2440]) ).
cnf(t110,plain,
inverse(multiply(sFlat1,X1)) = multiply(inverse(X1),sFlat2),
inference(cp,[status(thm)],[t54,t108]) ).
cnf(t218,plain,
inverse(multiply(sFlat1,X1)) = multiply(inverse(X1),sFlat2),
inference(orient,[status(thm)],[t110]) ).
cnf(t24098,plain,
multiply(sFlat2,inverse(a)) = multiply(inverse(a),sFlat2),
inference(step,[status(thm)],[t2446,t218]) ).
cnf(t2462,plain,
multiply(inverse(a),sFlat2) = multiply(sFlat2,inverse(a)),
inference(orient,[status(thm)],[t24098]) ).
cnf(t2468,plain,
sFlat2 = multiply(inverse(inverse(a)),multiply(sFlat2,inverse(a))),
inference(cp,[status(thm)],[t1013,t2462]) ).
cnf(t24116,plain,
sFlat2 = multiply(a,multiply(sFlat2,inverse(a))),
inference(step,[status(thm)],[t2468,t27]) ).
cnf(t2696,plain,
multiply(a,multiply(sFlat2,inverse(a))) = sFlat2,
inference(orient,[status(thm)],[t24116]) ).
cnf(t2700,plain,
multiply(greatest_lower_bound(identity,a),multiply(sFlat2,inverse(a))) = greatest_lower_bound(multiply(sFlat2,inverse(a)),sFlat2),
inference(cp,[status(thm)],[t273,t2696]) ).
cnf(t24118,plain,
multiply(sFlat1,multiply(sFlat2,inverse(a))) = greatest_lower_bound(multiply(sFlat2,inverse(a)),sFlat2),
inference(step,[status(thm)],[t2700,t84]) ).
cnf(t112,plain,
sFlat1 = inverse(sFlat2),
inference(cp,[status(thm)],[t27,t108]) ).
cnf(t113,plain,
inverse(sFlat2) = sFlat1,
inference(orient,[status(thm)],[t112]) ).
cnf(t116,plain,
identity = multiply(sFlat1,sFlat2),
inference(cp,[status(thm)],[t43,t113]) ).
cnf(t133,plain,
multiply(sFlat1,sFlat2) = identity,
inference(orient,[status(thm)],[t116]) ).
cnf(t142,plain,
multiply(sFlat1,multiply(sFlat2,X1)) = multiply(identity,X1),
inference(cp,[status(thm)],[t28,t133]) ).
cnf(t23971,plain,
multiply(sFlat1,multiply(sFlat2,X1)) = X1,
inference(step,[status(thm)],[t142,t22]) ).
cnf(t203,plain,
multiply(sFlat1,multiply(sFlat2,X1)) = X1,
inference(orient,[status(thm)],[t23971]) ).
cnf(t24119,plain,
inverse(a) = greatest_lower_bound(multiply(sFlat2,inverse(a)),sFlat2),
inference(step,[status(thm)],[t24118,t203]) ).
cnf(t24120,plain,
inverse(a) = greatest_lower_bound(sFlat2,multiply(sFlat2,inverse(a))),
inference(step,[status(thm)],[t24119,t67]) ).
cnf(t24121,plain,
inverse(a) = multiply(sFlat2,greatest_lower_bound(identity,inverse(a))),
inference(step,[status(thm)],[t24120,t1879]) ).
cnf(t2749,plain,
multiply(sFlat2,greatest_lower_bound(identity,inverse(a))) = inverse(a),
inference(orient,[status(thm)],[t24121]) ).
cnf(t2753,plain,
greatest_lower_bound(identity,inverse(a)) = multiply(inverse(sFlat2),inverse(a)),
inference(cp,[status(thm)],[t1013,t2749]) ).
cnf(t24122,plain,
greatest_lower_bound(identity,inverse(a)) = inverse(multiply(a,sFlat2)),
inference(step,[status(thm)],[t2753,t54]) ).
cnf(t114,plain,
inverse(multiply(X1,sFlat2)) = multiply(sFlat1,inverse(X1)),
inference(cp,[status(thm)],[t54,t113]) ).
cnf(t224,plain,
inverse(multiply(X1,sFlat2)) = multiply(sFlat1,inverse(X1)),
inference(orient,[status(thm)],[t114]) ).
cnf(t24123,plain,
greatest_lower_bound(identity,inverse(a)) = multiply(sFlat1,inverse(a)),
inference(step,[status(thm)],[t24122,t224]) ).
cnf(t2774,plain,
greatest_lower_bound(identity,inverse(a)) = multiply(sFlat1,inverse(a)),
inference(orient,[status(thm)],[t24123]) ).
cnf(t2781,plain,
greatest_lower_bound(sFlat1,inverse(a)) = greatest_lower_bound(sFlat1,multiply(sFlat1,inverse(a))),
inference(cp,[status(thm)],[t409,t2774]) ).
cnf(t24510,plain,
greatest_lower_bound(sFlat1,inverse(a)) = multiply(sFlat1,greatest_lower_bound(identity,inverse(a))),
inference(step,[status(thm)],[t2781,t1879]) ).
cnf(t24511,plain,
greatest_lower_bound(sFlat1,inverse(a)) = multiply(sFlat1,multiply(sFlat1,inverse(a))),
inference(step,[status(thm)],[t24510,t2774]) ).
cnf(t15157,plain,
multiply(sFlat1,multiply(sFlat1,inverse(a))) = greatest_lower_bound(sFlat1,inverse(a)),
inference(orient,[status(thm)],[t24511]) ).
cnf(t15159,plain,
multiply(sFlat1,multiply(a,multiply(sFlat1,inverse(a)))) = multiply(a,greatest_lower_bound(sFlat1,inverse(a))),
inference(cp,[status(thm)],[t3269,t15157]) ).
cnf(t44,plain,
identity = multiply(X1,inverse(X1)),
inference(cp,[status(thm)],[t43,t27]) ).
cnf(t147,plain,
multiply(X1,inverse(X1)) = identity,
inference(orient,[status(thm)],[t44]) ).
cnf(t157,plain,
multiply(X1,multiply(inverse(X1),X2)) = multiply(identity,X2),
inference(cp,[status(thm)],[t28,t147]) ).
cnf(t24063,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(step,[status(thm)],[t157,t22]) ).
cnf(t1663,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t24063]) ).
cnf(t1665,plain,
inverse(X1) = multiply(X2,inverse(multiply(X1,X2))),
inference(cp,[status(thm)],[t1663,t54]) ).
cnf(t1698,plain,
multiply(X1,inverse(multiply(X2,X1))) = inverse(X2),
inference(orient,[status(thm)],[t1665]) ).
cnf(t2445,plain,
sFlat1 = multiply(inverse(a),multiply(sFlat1,a)),
inference(cp,[status(thm)],[t1013,t2440]) ).
cnf(t2485,plain,
multiply(inverse(a),multiply(sFlat1,a)) = sFlat1,
inference(orient,[status(thm)],[t2445]) ).
cnf(t2502,plain,
inverse(inverse(a)) = multiply(multiply(sFlat1,a),inverse(sFlat1)),
inference(cp,[status(thm)],[t1698,t2485]) ).
cnf(t24099,plain,
a = multiply(multiply(sFlat1,a),inverse(sFlat1)),
inference(step,[status(thm)],[t2502,t27]) ).
cnf(t24100,plain,
a = multiply(sFlat1,multiply(a,inverse(sFlat1))),
inference(step,[status(thm)],[t24099,t28]) ).
cnf(t24101,plain,
a = multiply(sFlat1,multiply(a,sFlat2)),
inference(step,[status(thm)],[t24100,t108]) ).
cnf(t2506,plain,
multiply(sFlat1,multiply(a,sFlat2)) = a,
inference(orient,[status(thm)],[t24101]) ).
cnf(t2508,plain,
multiply(a,sFlat2) = multiply(inverse(sFlat1),a),
inference(cp,[status(thm)],[t1013,t2506]) ).
cnf(t24102,plain,
multiply(a,sFlat2) = multiply(sFlat2,a),
inference(step,[status(thm)],[t2508,t108]) ).
cnf(t2528,plain,
multiply(a,sFlat2) = multiply(sFlat2,a),
inference(orient,[status(thm)],[t24102]) ).
cnf(t2532,plain,
multiply(sFlat1,inverse(a)) = inverse(multiply(sFlat2,a)),
inference(cp,[status(thm)],[t224,t2528]) ).
cnf(t115,plain,
inverse(multiply(sFlat2,X1)) = multiply(inverse(X1),sFlat1),
inference(cp,[status(thm)],[t54,t113]) ).
cnf(t229,plain,
inverse(multiply(sFlat2,X1)) = multiply(inverse(X1),sFlat1),
inference(orient,[status(thm)],[t115]) ).
cnf(t24103,plain,
multiply(sFlat1,inverse(a)) = multiply(inverse(a),sFlat1),
inference(step,[status(thm)],[t2532,t229]) ).
cnf(t2547,plain,
multiply(inverse(a),sFlat1) = multiply(sFlat1,inverse(a)),
inference(orient,[status(thm)],[t24103]) ).
cnf(t2553,plain,
sFlat1 = multiply(inverse(inverse(a)),multiply(sFlat1,inverse(a))),
inference(cp,[status(thm)],[t1013,t2547]) ).
cnf(t24117,plain,
sFlat1 = multiply(a,multiply(sFlat1,inverse(a))),
inference(step,[status(thm)],[t2553,t27]) ).
cnf(t2719,plain,
multiply(a,multiply(sFlat1,inverse(a))) = sFlat1,
inference(orient,[status(thm)],[t24117]) ).
cnf(t24517,plain,
multiply(sFlat1,sFlat1) = multiply(a,greatest_lower_bound(sFlat1,inverse(a))),
inference(step,[status(thm)],[t15159,t2719]) ).
cnf(t15218,plain,
multiply(a,greatest_lower_bound(sFlat1,inverse(a))) = multiply(sFlat1,sFlat1),
inference(orient,[status(thm)],[t24517]) ).
cnf(t156,plain,
multiply(X1,greatest_lower_bound(X2,inverse(X1))) = greatest_lower_bound(multiply(X1,X2),identity),
inference(cp,[status(thm)],[t29,t147]) ).
cnf(t24714,plain,
multiply(X1,greatest_lower_bound(X2,inverse(X1))) = greatest_lower_bound(identity,multiply(X1,X2)),
inference(step,[status(thm)],[t156,t67]) ).
cnf(t22495,plain,
multiply(X1,greatest_lower_bound(X2,inverse(X1))) = greatest_lower_bound(identity,multiply(X1,X2)),
inference(orient,[status(thm)],[t24714]) ).
cnf(t24715,plain,
greatest_lower_bound(identity,multiply(a,sFlat1)) = multiply(sFlat1,sFlat1),
inference(step,[status(thm)],[t15218,t22495]) ).
cnf(t111,plain,
identity = multiply(sFlat2,sFlat1),
inference(cp,[status(thm)],[t43,t108]) ).
cnf(t123,plain,
multiply(sFlat2,sFlat1) = identity,
inference(orient,[status(thm)],[t111]) ).
cnf(t126,plain,
multiply(greatest_lower_bound(sFlat2,X1),sFlat1) = greatest_lower_bound(identity,multiply(X1,sFlat1)),
inference(cp,[status(thm)],[t32,t123]) ).
cnf(t1746,plain,
greatest_lower_bound(identity,multiply(X1,sFlat1)) = multiply(greatest_lower_bound(sFlat2,X1),sFlat1),
inference(orient,[status(thm)],[t126]) ).
cnf(t24716,plain,
multiply(greatest_lower_bound(sFlat2,a),sFlat1) = multiply(sFlat1,sFlat1),
inference(step,[status(thm)],[t24715,t1746]) ).
cnf(t2443,plain,
multiply(greatest_lower_bound(sFlat2,a),sFlat1) = greatest_lower_bound(identity,multiply(sFlat1,a)),
inference(cp,[status(thm)],[t1746,t2440]) ).
cnf(t140,plain,
multiply(sFlat1,greatest_lower_bound(sFlat2,X1)) = greatest_lower_bound(identity,multiply(sFlat1,X1)),
inference(cp,[status(thm)],[t29,t133]) ).
cnf(t1821,plain,
greatest_lower_bound(identity,multiply(sFlat1,X1)) = multiply(sFlat1,greatest_lower_bound(sFlat2,X1)),
inference(orient,[status(thm)],[t140]) ).
cnf(t24164,plain,
multiply(greatest_lower_bound(sFlat2,a),sFlat1) = multiply(sFlat1,greatest_lower_bound(sFlat2,a)),
inference(step,[status(thm)],[t2443,t1821]) ).
cnf(t3246,plain,
multiply(greatest_lower_bound(sFlat2,a),sFlat1) = multiply(sFlat1,greatest_lower_bound(sFlat2,a)),
inference(orient,[status(thm)],[t24164]) ).
cnf(t24717,plain,
multiply(sFlat1,greatest_lower_bound(sFlat2,a)) = multiply(sFlat1,sFlat1),
inference(step,[status(thm)],[t24716,t3246]) ).
cnf(t22586,plain,
multiply(sFlat1,greatest_lower_bound(sFlat2,a)) = multiply(sFlat1,sFlat1),
inference(rw,[status(thm)],[t24717]) ).
cnf(t22588,plain,
multiply(sFlat1,greatest_lower_bound(sFlat2,a)) = multiply(sFlat1,sFlat1),
inference(orient,[status(thm)],[t22586]) ).
cnf(t22598,plain,
greatest_lower_bound(sFlat2,a) = multiply(inverse(sFlat1),multiply(sFlat1,sFlat1)),
inference(cp,[status(thm)],[t1013,t22588]) ).
cnf(t24723,plain,
greatest_lower_bound(sFlat2,a) = sFlat1,
inference(step,[status(thm)],[t22598,t1013]) ).
cnf(t22629,plain,
greatest_lower_bound(sFlat2,a) = sFlat1,
inference(orient,[status(thm)],[t24723]) ).
cnf(t22643,plain,
greatest_lower_bound(sFlat2,greatest_lower_bound(a,X1)) = greatest_lower_bound(sFlat1,X1),
inference(cp,[status(thm)],[t71,t22629]) ).
cnf(t23213,plain,
greatest_lower_bound(sFlat2,greatest_lower_bound(a,X1)) = greatest_lower_bound(sFlat1,X1),
inference(orient,[status(thm)],[t22643]) ).
cnf(t23231,plain,
greatest_lower_bound(greatest_lower_bound(a,X1),sFlat2) = greatest_lower_bound(greatest_lower_bound(a,X1),greatest_lower_bound(sFlat1,X1)),
inference(cp,[status(thm)],[t438,t23213]) ).
cnf(t24736,plain,
greatest_lower_bound(a,greatest_lower_bound(X1,sFlat2)) = greatest_lower_bound(greatest_lower_bound(a,X1),greatest_lower_bound(sFlat1,X1)),
inference(step,[status(thm)],[t23231,t71]) ).
cnf(t24737,plain,
greatest_lower_bound(a,greatest_lower_bound(X1,sFlat2)) = greatest_lower_bound(a,greatest_lower_bound(X1,greatest_lower_bound(sFlat1,X1))),
inference(step,[status(thm)],[t24736,t71]) ).
cnf(t24738,plain,
greatest_lower_bound(a,greatest_lower_bound(X1,sFlat2)) = greatest_lower_bound(a,greatest_lower_bound(X1,sFlat1)),
inference(step,[status(thm)],[t24737,t438]) ).
cnf(t1,axiom,
greatest_lower_bound(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t23,plain,
greatest_lower_bound(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t75,plain,
greatest_lower_bound(X1,greatest_lower_bound(X1,X2)) = greatest_lower_bound(X1,X2),
inference(cp,[status(thm)],[t71,t23]) ).
cnf(t233,plain,
greatest_lower_bound(X1,greatest_lower_bound(X1,X2)) = greatest_lower_bound(X1,X2),
inference(orient,[status(thm)],[t75]) ).
cnf(t17,axiom,
least_upper_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(least_upper_bound(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t38,plain,
least_upper_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(least_upper_bound(X1,X3),X2),
inference(orient,[status(thm)],[t17]) ).
cnf(t39,plain,
multiply(least_upper_bound(identity,X1),X2) = least_upper_bound(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t38,t22]) ).
cnf(t1594,plain,
least_upper_bound(X1,multiply(X2,X1)) = multiply(least_upper_bound(identity,X2),X1),
inference(orient,[status(thm)],[t39]) ).
cnf(t1597,plain,
multiply(least_upper_bound(identity,X1),inverse(X1)) = least_upper_bound(inverse(X1),identity),
inference(cp,[status(thm)],[t1594,t147]) ).
cnf(t24492,plain,
multiply(least_upper_bound(identity,X1),inverse(X1)) = least_upper_bound(identity,inverse(X1)),
inference(step,[status(thm)],[t1597,t88]) ).
cnf(t14290,plain,
multiply(least_upper_bound(identity,X1),inverse(X1)) = least_upper_bound(identity,inverse(X1)),
inference(orient,[status(thm)],[t24492]) ).
cnf(t12,axiom,
least_upper_bound(least_upper_bound(X1,X2),X3) = least_upper_bound(X1,least_upper_bound(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t92,plain,
least_upper_bound(least_upper_bound(X1,X2),X3) = least_upper_bound(X1,least_upper_bound(X2,X3)),
inference(orient,[status(thm)],[t12]) ).
cnf(t3,axiom,
least_upper_bound(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t25,plain,
least_upper_bound(X1,X1) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t96,plain,
least_upper_bound(X1,least_upper_bound(X1,X2)) = least_upper_bound(X1,X2),
inference(cp,[status(thm)],[t92,t25]) ).
cnf(t305,plain,
least_upper_bound(X1,least_upper_bound(X1,X2)) = least_upper_bound(X1,X2),
inference(orient,[status(thm)],[t96]) ).
cnf(t14316,plain,
least_upper_bound(identity,inverse(least_upper_bound(identity,X1))) = multiply(least_upper_bound(identity,X1),inverse(least_upper_bound(identity,X1))),
inference(cp,[status(thm)],[t14290,t305]) ).
cnf(t24493,plain,
least_upper_bound(identity,inverse(least_upper_bound(identity,X1))) = identity,
inference(step,[status(thm)],[t14316,t147]) ).
cnf(t14398,plain,
least_upper_bound(identity,inverse(least_upper_bound(identity,X1))) = identity,
inference(orient,[status(thm)],[t24493]) ).
cnf(t14405,plain,
identity = least_upper_bound(identity,inverse(least_upper_bound(X1,identity))),
inference(cp,[status(thm)],[t14398,t88]) ).
cnf(t14437,plain,
least_upper_bound(identity,inverse(least_upper_bound(X1,identity))) = identity,
inference(orient,[status(thm)],[t14405]) ).
cnf(t277,plain,
multiply(greatest_lower_bound(identity,sFlat1),sFlat2) = greatest_lower_bound(sFlat2,identity),
inference(cp,[status(thm)],[t273,t133]) ).
cnf(t23984,plain,
multiply(greatest_lower_bound(sFlat1,identity),sFlat2) = greatest_lower_bound(sFlat2,identity),
inference(step,[status(thm)],[t277,t67]) ).
cnf(t23985,plain,
multiply(sFlat1,sFlat2) = greatest_lower_bound(sFlat2,identity),
inference(step,[status(thm)],[t23984,t143]) ).
cnf(t23986,plain,
identity = greatest_lower_bound(sFlat2,identity),
inference(step,[status(thm)],[t23985,t133]) ).
cnf(t514,plain,
greatest_lower_bound(sFlat2,identity) = identity,
inference(orient,[status(thm)],[t23986]) ).
cnf(t517,plain,
greatest_lower_bound(sFlat2,greatest_lower_bound(identity,X1)) = greatest_lower_bound(identity,X1),
inference(cp,[status(thm)],[t71,t514]) ).
cnf(t718,plain,
greatest_lower_bound(sFlat2,greatest_lower_bound(identity,X1)) = greatest_lower_bound(identity,X1),
inference(orient,[status(thm)],[t517]) ).
cnf(t726,plain,
greatest_lower_bound(greatest_lower_bound(identity,X1),sFlat2) = greatest_lower_bound(greatest_lower_bound(identity,X1),greatest_lower_bound(identity,X1)),
inference(cp,[status(thm)],[t438,t718]) ).
cnf(t24004,plain,
greatest_lower_bound(identity,greatest_lower_bound(X1,sFlat2)) = greatest_lower_bound(greatest_lower_bound(identity,X1),greatest_lower_bound(identity,X1)),
inference(step,[status(thm)],[t726,t71]) ).
cnf(t24005,plain,
greatest_lower_bound(identity,greatest_lower_bound(X1,sFlat2)) = greatest_lower_bound(identity,greatest_lower_bound(X1,greatest_lower_bound(identity,X1))),
inference(step,[status(thm)],[t24004,t71]) ).
cnf(t24006,plain,
greatest_lower_bound(identity,greatest_lower_bound(X1,sFlat2)) = greatest_lower_bound(identity,greatest_lower_bound(X1,identity)),
inference(step,[status(thm)],[t24005,t438]) ).
cnf(t24007,plain,
greatest_lower_bound(identity,greatest_lower_bound(X1,sFlat2)) = greatest_lower_bound(identity,X1),
inference(step,[status(thm)],[t24006,t438]) ).
cnf(t911,plain,
greatest_lower_bound(identity,greatest_lower_bound(X1,sFlat2)) = greatest_lower_bound(identity,X1),
inference(orient,[status(thm)],[t24007]) ).
cnf(t21,axiom,
sFlat3 = greatest_lower_bound(least_upper_bound(a,identity),inverse(greatest_lower_bound(a,identity))),
introduced(definition) ).
cnf(t23958,plain,
sFlat3 = greatest_lower_bound(least_upper_bound(a,identity),inverse(greatest_lower_bound(identity,a))),
inference(step,[status(thm)],[t21,t67]) ).
cnf(t81,plain,
greatest_lower_bound(least_upper_bound(a,identity),inverse(greatest_lower_bound(identity,a))) = sFlat3,
inference(orient,[status(thm)],[t23958]) ).
cnf(t23960,plain,
greatest_lower_bound(least_upper_bound(a,identity),inverse(sFlat1)) = sFlat3,
inference(step,[status(thm)],[t81,t84]) ).
cnf(t87,plain,
greatest_lower_bound(least_upper_bound(a,identity),inverse(sFlat1)) = sFlat3,
inference(rw,[status(thm)],[t23960]) ).
cnf(t24019,plain,
greatest_lower_bound(inverse(sFlat1),least_upper_bound(a,identity)) = sFlat3,
inference(step,[status(thm)],[t87,t67]) ).
cnf(t24020,plain,
greatest_lower_bound(sFlat2,least_upper_bound(a,identity)) = sFlat3,
inference(step,[status(thm)],[t24019,t108]) ).
cnf(t24021,plain,
greatest_lower_bound(sFlat2,least_upper_bound(identity,a)) = sFlat3,
inference(step,[status(thm)],[t24020,t88]) ).
cnf(t18,axiom,
sFlat0 = least_upper_bound(a,identity),
introduced(definition) ).
cnf(t23961,plain,
sFlat0 = least_upper_bound(identity,a),
inference(step,[status(thm)],[t18,t88]) ).
cnf(t102,plain,
least_upper_bound(identity,a) = sFlat0,
inference(orient,[status(thm)],[t23961]) ).
cnf(t24022,plain,
greatest_lower_bound(sFlat2,sFlat0) = sFlat3,
inference(step,[status(thm)],[t24021,t102]) ).
cnf(t24023,plain,
greatest_lower_bound(sFlat0,sFlat2) = sFlat3,
inference(step,[status(thm)],[t24022,t67]) ).
cnf(t1027,plain,
greatest_lower_bound(sFlat0,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t24023]) ).
cnf(t1029,plain,
greatest_lower_bound(identity,sFlat0) = greatest_lower_bound(identity,sFlat3),
inference(cp,[status(thm)],[t911,t1027]) ).
cnf(t24028,plain,
greatest_lower_bound(sFlat0,identity) = greatest_lower_bound(identity,sFlat3),
inference(step,[status(thm)],[t1029,t67]) ).
cnf(t103,plain,
identity = greatest_lower_bound(identity,sFlat0),
inference(cp,[status(thm)],[t24,t102]) ).
cnf(t23965,plain,
identity = greatest_lower_bound(sFlat0,identity),
inference(step,[status(thm)],[t103,t67]) ).
cnf(t120,plain,
greatest_lower_bound(sFlat0,identity) = identity,
inference(orient,[status(thm)],[t23965]) ).
cnf(t24029,plain,
identity = greatest_lower_bound(identity,sFlat3),
inference(step,[status(thm)],[t24028,t120]) ).
cnf(t24030,plain,
identity = greatest_lower_bound(sFlat3,identity),
inference(step,[status(thm)],[t24029,t67]) ).
cnf(t1068,plain,
greatest_lower_bound(sFlat3,identity) = identity,
inference(orient,[status(thm)],[t24030]) ).
cnf(t1073,plain,
sFlat3 = least_upper_bound(sFlat3,identity),
inference(cp,[status(thm)],[t26,t1068]) ).
cnf(t1074,plain,
least_upper_bound(sFlat3,identity) = sFlat3,
inference(orient,[status(thm)],[t1073]) ).
cnf(t14438,plain,
identity = least_upper_bound(identity,inverse(sFlat3)),
inference(cp,[status(thm)],[t14437,t1074]) ).
cnf(t14463,plain,
least_upper_bound(identity,inverse(sFlat3)) = identity,
inference(orient,[status(thm)],[t14438]) ).
cnf(t14466,plain,
inverse(sFlat3) = greatest_lower_bound(inverse(sFlat3),identity),
inference(cp,[status(thm)],[t181,t14463]) ).
cnf(t24495,plain,
inverse(sFlat3) = greatest_lower_bound(identity,inverse(sFlat3)),
inference(step,[status(thm)],[t14466,t67]) ).
cnf(t14483,plain,
greatest_lower_bound(identity,inverse(sFlat3)) = inverse(sFlat3),
inference(orient,[status(thm)],[t24495]) ).
cnf(t14486,plain,
greatest_lower_bound(identity,greatest_lower_bound(inverse(sFlat3),X1)) = greatest_lower_bound(inverse(sFlat3),X1),
inference(cp,[status(thm)],[t71,t14483]) ).
cnf(t19369,plain,
greatest_lower_bound(identity,greatest_lower_bound(inverse(sFlat3),X1)) = greatest_lower_bound(inverse(sFlat3),X1),
inference(orient,[status(thm)],[t14486]) ).
cnf(t85,plain,
greatest_lower_bound(identity,greatest_lower_bound(a,X1)) = greatest_lower_bound(sFlat1,X1),
inference(cp,[status(thm)],[t71,t84]) ).
cnf(t238,plain,
greatest_lower_bound(identity,greatest_lower_bound(a,X1)) = greatest_lower_bound(sFlat1,X1),
inference(orient,[status(thm)],[t85]) ).
cnf(t242,plain,
greatest_lower_bound(sFlat1,X1) = greatest_lower_bound(identity,greatest_lower_bound(X1,a)),
inference(cp,[status(thm)],[t238,t67]) ).
cnf(t463,plain,
greatest_lower_bound(identity,greatest_lower_bound(X1,a)) = greatest_lower_bound(sFlat1,X1),
inference(orient,[status(thm)],[t242]) ).
cnf(t19373,plain,
greatest_lower_bound(inverse(sFlat3),a) = greatest_lower_bound(sFlat1,inverse(sFlat3)),
inference(cp,[status(thm)],[t19369,t463]) ).
cnf(t24649,plain,
greatest_lower_bound(a,inverse(sFlat3)) = greatest_lower_bound(sFlat1,inverse(sFlat3)),
inference(step,[status(thm)],[t19373,t67]) ).
cnf(t16,axiom,
least_upper_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,least_upper_bound(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t31,plain,
least_upper_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,least_upper_bound(X2,X3)),
inference(orient,[status(thm)],[t16]) ).
cnf(t164,plain,
multiply(X1,least_upper_bound(identity,X2)) = least_upper_bound(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t31,t163]) ).
cnf(t1837,plain,
least_upper_bound(X1,multiply(X1,X2)) = multiply(X1,least_upper_bound(identity,X2)),
inference(orient,[status(thm)],[t164]) ).
cnf(t1838,plain,
multiply(X1,least_upper_bound(identity,X1)) = multiply(least_upper_bound(identity,X1),X1),
inference(cp,[status(thm)],[t1837,t1594]) ).
cnf(t2018,plain,
multiply(least_upper_bound(identity,X1),X1) = multiply(X1,least_upper_bound(identity,X1)),
inference(orient,[status(thm)],[t1838]) ).
cnf(t2028,plain,
multiply(a,least_upper_bound(identity,a)) = multiply(sFlat0,a),
inference(cp,[status(thm)],[t2018,t102]) ).
cnf(t24078,plain,
multiply(a,sFlat0) = multiply(sFlat0,a),
inference(step,[status(thm)],[t2028,t102]) ).
cnf(t2056,plain,
multiply(a,sFlat0) = multiply(sFlat0,a),
inference(orient,[status(thm)],[t24078]) ).
cnf(t2060,plain,
multiply(greatest_lower_bound(identity,a),sFlat0) = greatest_lower_bound(sFlat0,multiply(sFlat0,a)),
inference(cp,[status(thm)],[t273,t2056]) ).
cnf(t24079,plain,
multiply(sFlat1,sFlat0) = greatest_lower_bound(sFlat0,multiply(sFlat0,a)),
inference(step,[status(thm)],[t2060,t84]) ).
cnf(t24080,plain,
multiply(sFlat1,sFlat0) = multiply(sFlat0,greatest_lower_bound(identity,a)),
inference(step,[status(thm)],[t24079,t1879]) ).
cnf(t24081,plain,
multiply(sFlat1,sFlat0) = multiply(sFlat0,sFlat1),
inference(step,[status(thm)],[t24080,t84]) ).
cnf(t2076,plain,
multiply(sFlat1,sFlat0) = multiply(sFlat0,sFlat1),
inference(orient,[status(thm)],[t24081]) ).
cnf(t2079,plain,
multiply(sFlat1,greatest_lower_bound(sFlat2,sFlat0)) = greatest_lower_bound(identity,multiply(sFlat0,sFlat1)),
inference(cp,[status(thm)],[t1821,t2076]) ).
cnf(t24125,plain,
multiply(sFlat1,greatest_lower_bound(sFlat0,sFlat2)) = greatest_lower_bound(identity,multiply(sFlat0,sFlat1)),
inference(step,[status(thm)],[t2079,t67]) ).
cnf(t24126,plain,
multiply(sFlat1,sFlat3) = greatest_lower_bound(identity,multiply(sFlat0,sFlat1)),
inference(step,[status(thm)],[t24125,t1027]) ).
cnf(t24127,plain,
multiply(sFlat1,sFlat3) = multiply(greatest_lower_bound(sFlat2,sFlat0),sFlat1),
inference(step,[status(thm)],[t24126,t1746]) ).
cnf(t24128,plain,
multiply(sFlat1,sFlat3) = multiply(greatest_lower_bound(sFlat0,sFlat2),sFlat1),
inference(step,[status(thm)],[t24127,t67]) ).
cnf(t24129,plain,
multiply(sFlat1,sFlat3) = multiply(sFlat3,sFlat1),
inference(step,[status(thm)],[t24128,t1027]) ).
cnf(t2878,plain,
multiply(sFlat3,sFlat1) = multiply(sFlat1,sFlat3),
inference(orient,[status(thm)],[t24129]) ).
cnf(t2882,plain,
sFlat1 = multiply(inverse(sFlat3),multiply(sFlat1,sFlat3)),
inference(cp,[status(thm)],[t1013,t2878]) ).
cnf(t2927,plain,
multiply(inverse(sFlat3),multiply(sFlat1,sFlat3)) = sFlat1,
inference(orient,[status(thm)],[t2882]) ).
cnf(t2928,plain,
multiply(inverse(sFlat3),greatest_lower_bound(identity,multiply(sFlat1,sFlat3))) = greatest_lower_bound(inverse(sFlat3),sFlat1),
inference(cp,[status(thm)],[t1879,t2927]) ).
cnf(t24131,plain,
multiply(inverse(sFlat3),multiply(sFlat1,greatest_lower_bound(sFlat2,sFlat3))) = greatest_lower_bound(inverse(sFlat3),sFlat1),
inference(step,[status(thm)],[t2928,t1821]) ).
cnf(t70,plain,
X1 = least_upper_bound(X1,greatest_lower_bound(X2,X1)),
inference(cp,[status(thm)],[t26,t67]) ).
cnf(t168,plain,
least_upper_bound(X1,greatest_lower_bound(X2,X1)) = X1,
inference(orient,[status(thm)],[t70]) ).
cnf(t1035,plain,
sFlat2 = least_upper_bound(sFlat2,sFlat3),
inference(cp,[status(thm)],[t168,t1027]) ).
cnf(t1050,plain,
least_upper_bound(sFlat2,sFlat3) = sFlat2,
inference(orient,[status(thm)],[t1035]) ).
cnf(t1052,plain,
sFlat3 = greatest_lower_bound(sFlat3,sFlat2),
inference(cp,[status(thm)],[t181,t1050]) ).
cnf(t24027,plain,
sFlat3 = greatest_lower_bound(sFlat2,sFlat3),
inference(step,[status(thm)],[t1052,t67]) ).
cnf(t1065,plain,
greatest_lower_bound(sFlat2,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t24027]) ).
cnf(t24132,plain,
multiply(inverse(sFlat3),multiply(sFlat1,sFlat3)) = greatest_lower_bound(inverse(sFlat3),sFlat1),
inference(step,[status(thm)],[t24131,t1065]) ).
cnf(t24133,plain,
sFlat1 = greatest_lower_bound(inverse(sFlat3),sFlat1),
inference(step,[status(thm)],[t24132,t2927]) ).
cnf(t24134,plain,
sFlat1 = greatest_lower_bound(sFlat1,inverse(sFlat3)),
inference(step,[status(thm)],[t24133,t67]) ).
cnf(t2951,plain,
greatest_lower_bound(sFlat1,inverse(sFlat3)) = sFlat1,
inference(orient,[status(thm)],[t24134]) ).
cnf(t24650,plain,
greatest_lower_bound(a,inverse(sFlat3)) = sFlat1,
inference(step,[status(thm)],[t24649,t2951]) ).
cnf(t19404,plain,
greatest_lower_bound(a,inverse(sFlat3)) = sFlat1,
inference(orient,[status(thm)],[t24650]) ).
cnf(t19410,plain,
greatest_lower_bound(a,greatest_lower_bound(inverse(sFlat3),X1)) = greatest_lower_bound(sFlat1,X1),
inference(cp,[status(thm)],[t71,t19404]) ).
cnf(t19428,plain,
greatest_lower_bound(a,greatest_lower_bound(inverse(sFlat3),X1)) = greatest_lower_bound(sFlat1,X1),
inference(orient,[status(thm)],[t19410]) ).
cnf(t19436,plain,
greatest_lower_bound(a,greatest_lower_bound(inverse(sFlat3),X1)) = greatest_lower_bound(a,greatest_lower_bound(sFlat1,X1)),
inference(cp,[status(thm)],[t233,t19428]) ).
cnf(t24651,plain,
greatest_lower_bound(sFlat1,X1) = greatest_lower_bound(a,greatest_lower_bound(sFlat1,X1)),
inference(step,[status(thm)],[t19436,t19428]) ).
cnf(t19440,plain,
greatest_lower_bound(a,greatest_lower_bound(sFlat1,X1)) = greatest_lower_bound(sFlat1,X1),
inference(orient,[status(thm)],[t24651]) ).
cnf(t19622,plain,
greatest_lower_bound(sFlat1,X1) = greatest_lower_bound(a,greatest_lower_bound(X1,sFlat1)),
inference(cp,[status(thm)],[t19440,t67]) ).
cnf(t19624,plain,
greatest_lower_bound(a,greatest_lower_bound(X1,sFlat1)) = greatest_lower_bound(sFlat1,X1),
inference(orient,[status(thm)],[t19622]) ).
cnf(t24739,plain,
greatest_lower_bound(a,greatest_lower_bound(X1,sFlat2)) = greatest_lower_bound(sFlat1,X1),
inference(step,[status(thm)],[t24738,t19624]) ).
cnf(t23274,plain,
greatest_lower_bound(a,greatest_lower_bound(X1,sFlat2)) = greatest_lower_bound(sFlat1,X1),
inference(orient,[status(thm)],[t24739]) ).
cnf(t23283,plain,
greatest_lower_bound(sFlat1,X1) = greatest_lower_bound(a,greatest_lower_bound(sFlat2,X1)),
inference(cp,[status(thm)],[t23274,t67]) ).
cnf(t23289,plain,
greatest_lower_bound(a,greatest_lower_bound(sFlat2,X1)) = greatest_lower_bound(sFlat1,X1),
inference(orient,[status(thm)],[t23283]) ).
cnf(t518,plain,
sFlat2 = least_upper_bound(sFlat2,identity),
inference(cp,[status(thm)],[t26,t514]) ).
cnf(t524,plain,
least_upper_bound(sFlat2,identity) = sFlat2,
inference(orient,[status(thm)],[t518]) ).
cnf(t526,plain,
least_upper_bound(sFlat2,least_upper_bound(identity,X1)) = least_upper_bound(sFlat2,X1),
inference(cp,[status(thm)],[t92,t524]) ).
cnf(t786,plain,
least_upper_bound(sFlat2,least_upper_bound(identity,X1)) = least_upper_bound(sFlat2,X1),
inference(orient,[status(thm)],[t526]) ).
cnf(t49,plain,
multiply(inverse(X1),least_upper_bound(X1,X2)) = least_upper_bound(identity,multiply(inverse(X1),X2)),
inference(cp,[status(thm)],[t31,t43]) ).
cnf(t7541,plain,
multiply(inverse(X1),least_upper_bound(X1,X2)) = least_upper_bound(identity,multiply(inverse(X1),X2)),
inference(orient,[status(thm)],[t49]) ).
cnf(t2059,plain,
sFlat0 = multiply(inverse(a),multiply(sFlat0,a)),
inference(cp,[status(thm)],[t1013,t2056]) ).
cnf(t2149,plain,
multiply(inverse(a),multiply(sFlat0,a)) = sFlat0,
inference(orient,[status(thm)],[t2059]) ).
cnf(t2166,plain,
inverse(inverse(a)) = multiply(multiply(sFlat0,a),inverse(sFlat0)),
inference(cp,[status(thm)],[t1698,t2149]) ).
cnf(t24092,plain,
a = multiply(multiply(sFlat0,a),inverse(sFlat0)),
inference(step,[status(thm)],[t2166,t27]) ).
cnf(t24093,plain,
a = multiply(sFlat0,multiply(a,inverse(sFlat0))),
inference(step,[status(thm)],[t24092,t28]) ).
cnf(t2280,plain,
multiply(sFlat0,multiply(a,inverse(sFlat0))) = a,
inference(orient,[status(thm)],[t24093]) ).
cnf(t2284,plain,
multiply(a,inverse(sFlat0)) = multiply(inverse(sFlat0),a),
inference(cp,[status(thm)],[t1013,t2280]) ).
cnf(t2302,plain,
multiply(inverse(sFlat0),a) = multiply(a,inverse(sFlat0)),
inference(orient,[status(thm)],[t2284]) ).
cnf(t7605,plain,
multiply(inverse(sFlat0),least_upper_bound(sFlat0,a)) = least_upper_bound(identity,multiply(a,inverse(sFlat0))),
inference(cp,[status(thm)],[t7541,t2302]) ).
cnf(t185,plain,
a = greatest_lower_bound(a,sFlat0),
inference(cp,[status(thm)],[t181,t102]) ).
cnf(t23969,plain,
a = greatest_lower_bound(sFlat0,a),
inference(step,[status(thm)],[t185,t67]) ).
cnf(t188,plain,
greatest_lower_bound(sFlat0,a) = a,
inference(orient,[status(thm)],[t23969]) ).
cnf(t190,plain,
sFlat0 = least_upper_bound(sFlat0,a),
inference(cp,[status(thm)],[t26,t188]) ).
cnf(t191,plain,
least_upper_bound(sFlat0,a) = sFlat0,
inference(orient,[status(thm)],[t190]) ).
cnf(t24291,plain,
multiply(inverse(sFlat0),sFlat0) = least_upper_bound(identity,multiply(a,inverse(sFlat0))),
inference(step,[status(thm)],[t7605,t191]) ).
cnf(t24292,plain,
identity = least_upper_bound(identity,multiply(a,inverse(sFlat0))),
inference(step,[status(thm)],[t24291,t43]) ).
cnf(t7641,plain,
least_upper_bound(identity,multiply(a,inverse(sFlat0))) = identity,
inference(orient,[status(thm)],[t24292]) ).
cnf(t7643,plain,
least_upper_bound(sFlat2,multiply(a,inverse(sFlat0))) = least_upper_bound(sFlat2,identity),
inference(cp,[status(thm)],[t786,t7641]) ).
cnf(t24300,plain,
least_upper_bound(sFlat2,multiply(a,inverse(sFlat0))) = sFlat2,
inference(step,[status(thm)],[t7643,t524]) ).
cnf(t7726,plain,
least_upper_bound(sFlat2,multiply(a,inverse(sFlat0))) = sFlat2,
inference(orient,[status(thm)],[t24300]) ).
cnf(t7731,plain,
multiply(a,inverse(sFlat0)) = greatest_lower_bound(multiply(a,inverse(sFlat0)),sFlat2),
inference(cp,[status(thm)],[t181,t7726]) ).
cnf(t24528,plain,
multiply(a,inverse(sFlat0)) = greatest_lower_bound(sFlat2,multiply(a,inverse(sFlat0))),
inference(step,[status(thm)],[t7731,t67]) ).
cnf(t15499,plain,
greatest_lower_bound(sFlat2,multiply(a,inverse(sFlat0))) = multiply(a,inverse(sFlat0)),
inference(orient,[status(thm)],[t24528]) ).
cnf(t23314,plain,
greatest_lower_bound(sFlat1,multiply(a,inverse(sFlat0))) = greatest_lower_bound(a,multiply(a,inverse(sFlat0))),
inference(cp,[status(thm)],[t23289,t15499]) ).
cnf(t24751,plain,
greatest_lower_bound(sFlat1,multiply(a,inverse(sFlat0))) = multiply(a,greatest_lower_bound(identity,inverse(sFlat0))),
inference(step,[status(thm)],[t23314,t1879]) ).
cnf(t50,plain,
multiply(inverse(X1),least_upper_bound(X2,X1)) = least_upper_bound(multiply(inverse(X1),X2),identity),
inference(cp,[status(thm)],[t31,t43]) ).
cnf(t24311,plain,
multiply(inverse(X1),least_upper_bound(X2,X1)) = least_upper_bound(identity,multiply(inverse(X1),X2)),
inference(step,[status(thm)],[t50,t88]) ).
cnf(t8289,plain,
multiply(inverse(X1),least_upper_bound(X2,X1)) = least_upper_bound(identity,multiply(inverse(X1),X2)),
inference(orient,[status(thm)],[t24311]) ).
cnf(t104,plain,
least_upper_bound(identity,least_upper_bound(a,X1)) = least_upper_bound(sFlat0,X1),
inference(cp,[status(thm)],[t92,t102]) ).
cnf(t310,plain,
least_upper_bound(identity,least_upper_bound(a,X1)) = least_upper_bound(sFlat0,X1),
inference(orient,[status(thm)],[t104]) ).
cnf(t316,plain,
least_upper_bound(identity,least_upper_bound(a,X1)) = least_upper_bound(identity,least_upper_bound(sFlat0,X1)),
inference(cp,[status(thm)],[t305,t310]) ).
cnf(t23989,plain,
least_upper_bound(sFlat0,X1) = least_upper_bound(identity,least_upper_bound(sFlat0,X1)),
inference(step,[status(thm)],[t316,t310]) ).
cnf(t540,plain,
least_upper_bound(identity,least_upper_bound(sFlat0,X1)) = least_upper_bound(sFlat0,X1),
inference(orient,[status(thm)],[t23989]) ).
cnf(t8500,plain,
least_upper_bound(identity,multiply(inverse(least_upper_bound(sFlat0,X1)),identity)) = multiply(inverse(least_upper_bound(sFlat0,X1)),least_upper_bound(sFlat0,X1)),
inference(cp,[status(thm)],[t8289,t540]) ).
cnf(t24324,plain,
multiply(least_upper_bound(identity,inverse(least_upper_bound(sFlat0,X1))),identity) = multiply(inverse(least_upper_bound(sFlat0,X1)),least_upper_bound(sFlat0,X1)),
inference(step,[status(thm)],[t8500,t1594]) ).
cnf(t24325,plain,
least_upper_bound(identity,inverse(least_upper_bound(sFlat0,X1))) = multiply(inverse(least_upper_bound(sFlat0,X1)),least_upper_bound(sFlat0,X1)),
inference(step,[status(thm)],[t24324,t163]) ).
cnf(t24326,plain,
least_upper_bound(identity,inverse(least_upper_bound(sFlat0,X1))) = identity,
inference(step,[status(thm)],[t24325,t43]) ).
cnf(t8679,plain,
least_upper_bound(identity,inverse(least_upper_bound(sFlat0,X1))) = identity,
inference(orient,[status(thm)],[t24326]) ).
cnf(t121,plain,
greatest_lower_bound(sFlat0,greatest_lower_bound(identity,X1)) = greatest_lower_bound(identity,X1),
inference(cp,[status(thm)],[t71,t120]) ).
cnf(t379,plain,
greatest_lower_bound(sFlat0,greatest_lower_bound(identity,X1)) = greatest_lower_bound(identity,X1),
inference(orient,[status(thm)],[t121]) ).
cnf(t382,plain,
sFlat0 = least_upper_bound(sFlat0,greatest_lower_bound(identity,X1)),
inference(cp,[status(thm)],[t26,t379]) ).
cnf(t383,plain,
least_upper_bound(sFlat0,greatest_lower_bound(identity,X1)) = sFlat0,
inference(orient,[status(thm)],[t382]) ).
cnf(t1834,plain,
sFlat0 = least_upper_bound(sFlat0,multiply(sFlat1,greatest_lower_bound(sFlat2,X1))),
inference(cp,[status(thm)],[t383,t1821]) ).
cnf(t5385,plain,
least_upper_bound(sFlat0,multiply(sFlat1,greatest_lower_bound(sFlat2,X1))) = sFlat0,
inference(orient,[status(thm)],[t1834]) ).
cnf(t5397,plain,
sFlat0 = least_upper_bound(sFlat0,multiply(sFlat1,greatest_lower_bound(X1,sFlat2))),
inference(cp,[status(thm)],[t5385,t67]) ).
cnf(t8059,plain,
least_upper_bound(sFlat0,multiply(sFlat1,greatest_lower_bound(X1,sFlat2))) = sFlat0,
inference(orient,[status(thm)],[t5397]) ).
cnf(t8680,plain,
identity = least_upper_bound(identity,inverse(sFlat0)),
inference(cp,[status(thm)],[t8679,t8059]) ).
cnf(t8759,plain,
least_upper_bound(identity,inverse(sFlat0)) = identity,
inference(orient,[status(thm)],[t8680]) ).
cnf(t8762,plain,
inverse(sFlat0) = greatest_lower_bound(inverse(sFlat0),identity),
inference(cp,[status(thm)],[t181,t8759]) ).
cnf(t24329,plain,
inverse(sFlat0) = greatest_lower_bound(identity,inverse(sFlat0)),
inference(step,[status(thm)],[t8762,t67]) ).
cnf(t8796,plain,
greatest_lower_bound(identity,inverse(sFlat0)) = inverse(sFlat0),
inference(orient,[status(thm)],[t24329]) ).
cnf(t24752,plain,
greatest_lower_bound(sFlat1,multiply(a,inverse(sFlat0))) = multiply(a,inverse(sFlat0)),
inference(step,[status(thm)],[t24751,t8796]) ).
cnf(t23638,plain,
greatest_lower_bound(sFlat1,multiply(a,inverse(sFlat0))) = multiply(a,inverse(sFlat0)),
inference(orient,[status(thm)],[t24752]) ).
cnf(t23668,plain,
greatest_lower_bound(identity,multiply(inverse(multiply(a,inverse(sFlat0))),sFlat1)) = multiply(inverse(multiply(a,inverse(sFlat0))),multiply(a,inverse(sFlat0))),
inference(cp,[status(thm)],[t10059,t23638]) ).
cnf(t24753,plain,
multiply(greatest_lower_bound(sFlat2,inverse(multiply(a,inverse(sFlat0)))),sFlat1) = multiply(inverse(multiply(a,inverse(sFlat0))),multiply(a,inverse(sFlat0))),
inference(step,[status(thm)],[t23668,t1746]) ).
cnf(t56,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(cp,[status(thm)],[t54,t27]) ).
cnf(t1681,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t56]) ).
cnf(t24754,plain,
multiply(greatest_lower_bound(sFlat2,multiply(sFlat0,inverse(a))),sFlat1) = multiply(inverse(multiply(a,inverse(sFlat0))),multiply(a,inverse(sFlat0))),
inference(step,[status(thm)],[t24753,t1681]) ).
cnf(t14311,plain,
least_upper_bound(identity,inverse(a)) = multiply(sFlat0,inverse(a)),
inference(cp,[status(thm)],[t14290,t102]) ).
cnf(t14364,plain,
least_upper_bound(identity,inverse(a)) = multiply(sFlat0,inverse(a)),
inference(orient,[status(thm)],[t14311]) ).
cnf(t14368,plain,
least_upper_bound(sFlat2,inverse(a)) = least_upper_bound(sFlat2,multiply(sFlat0,inverse(a))),
inference(cp,[status(thm)],[t786,t14364]) ).
cnf(t2458,plain,
inverse(sFlat1) = multiply(inverse(multiply(sFlat1,a)),a),
inference(cp,[status(thm)],[t1717,t2440]) ).
cnf(t24104,plain,
sFlat2 = multiply(inverse(multiply(sFlat1,a)),a),
inference(step,[status(thm)],[t2458,t108]) ).
cnf(t24105,plain,
sFlat2 = multiply(multiply(inverse(a),sFlat2),a),
inference(step,[status(thm)],[t24104,t218]) ).
cnf(t24106,plain,
sFlat2 = multiply(inverse(a),multiply(sFlat2,a)),
inference(step,[status(thm)],[t24105,t28]) ).
cnf(t2570,plain,
multiply(inverse(a),multiply(sFlat2,a)) = sFlat2,
inference(orient,[status(thm)],[t24106]) ).
cnf(t2572,plain,
multiply(inverse(a),least_upper_bound(identity,multiply(sFlat2,a))) = least_upper_bound(inverse(a),sFlat2),
inference(cp,[status(thm)],[t1837,t2570]) ).
cnf(t128,plain,
multiply(sFlat2,least_upper_bound(sFlat1,X1)) = least_upper_bound(identity,multiply(sFlat2,X1)),
inference(cp,[status(thm)],[t31,t123]) ).
cnf(t1757,plain,
least_upper_bound(identity,multiply(sFlat2,X1)) = multiply(sFlat2,least_upper_bound(sFlat1,X1)),
inference(orient,[status(thm)],[t128]) ).
cnf(t24107,plain,
multiply(inverse(a),multiply(sFlat2,least_upper_bound(sFlat1,a))) = least_upper_bound(inverse(a),sFlat2),
inference(step,[status(thm)],[t2572,t1757]) ).
cnf(t172,plain,
a = least_upper_bound(a,sFlat1),
inference(cp,[status(thm)],[t168,t84]) ).
cnf(t23968,plain,
a = least_upper_bound(sFlat1,a),
inference(step,[status(thm)],[t172,t88]) ).
cnf(t175,plain,
least_upper_bound(sFlat1,a) = a,
inference(orient,[status(thm)],[t23968]) ).
cnf(t24108,plain,
multiply(inverse(a),multiply(sFlat2,a)) = least_upper_bound(inverse(a),sFlat2),
inference(step,[status(thm)],[t24107,t175]) ).
cnf(t24109,plain,
sFlat2 = least_upper_bound(inverse(a),sFlat2),
inference(step,[status(thm)],[t24108,t2570]) ).
cnf(t24110,plain,
sFlat2 = least_upper_bound(sFlat2,inverse(a)),
inference(step,[status(thm)],[t24109,t88]) ).
cnf(t2682,plain,
least_upper_bound(sFlat2,inverse(a)) = sFlat2,
inference(orient,[status(thm)],[t24110]) ).
cnf(t24494,plain,
sFlat2 = least_upper_bound(sFlat2,multiply(sFlat0,inverse(a))),
inference(step,[status(thm)],[t14368,t2682]) ).
cnf(t14425,plain,
least_upper_bound(sFlat2,multiply(sFlat0,inverse(a))) = sFlat2,
inference(orient,[status(thm)],[t24494]) ).
cnf(t14431,plain,
multiply(sFlat0,inverse(a)) = greatest_lower_bound(multiply(sFlat0,inverse(a)),sFlat2),
inference(cp,[status(thm)],[t181,t14425]) ).
cnf(t24648,plain,
multiply(sFlat0,inverse(a)) = greatest_lower_bound(sFlat2,multiply(sFlat0,inverse(a))),
inference(step,[status(thm)],[t14431,t67]) ).
cnf(t19358,plain,
greatest_lower_bound(sFlat2,multiply(sFlat0,inverse(a))) = multiply(sFlat0,inverse(a)),
inference(orient,[status(thm)],[t24648]) ).
cnf(t24755,plain,
multiply(multiply(sFlat0,inverse(a)),sFlat1) = multiply(inverse(multiply(a,inverse(sFlat0))),multiply(a,inverse(sFlat0))),
inference(step,[status(thm)],[t24754,t19358]) ).
cnf(t24756,plain,
multiply(sFlat0,multiply(inverse(a),sFlat1)) = multiply(inverse(multiply(a,inverse(sFlat0))),multiply(a,inverse(sFlat0))),
inference(step,[status(thm)],[t24755,t28]) ).
cnf(t24757,plain,
multiply(sFlat0,multiply(sFlat1,inverse(a))) = multiply(inverse(multiply(a,inverse(sFlat0))),multiply(a,inverse(sFlat0))),
inference(step,[status(thm)],[t24756,t2547]) ).
cnf(t24758,plain,
multiply(sFlat0,multiply(sFlat1,inverse(a))) = identity,
inference(step,[status(thm)],[t24757,t43]) ).
cnf(t23681,plain,
multiply(sFlat0,multiply(sFlat1,inverse(a))) = identity,
inference(orient,[status(thm)],[t24758]) ).
cnf(t23714,plain,
inverse(multiply(sFlat1,inverse(a))) = multiply(inverse(identity),sFlat0),
inference(cp,[status(thm)],[t1717,t23681]) ).
cnf(t24764,plain,
multiply(inverse(inverse(a)),sFlat2) = multiply(inverse(identity),sFlat0),
inference(step,[status(thm)],[t23714,t218]) ).
cnf(t24765,plain,
multiply(a,sFlat2) = multiply(inverse(identity),sFlat0),
inference(step,[status(thm)],[t24764,t27]) ).
cnf(t24766,plain,
multiply(sFlat2,a) = multiply(inverse(identity),sFlat0),
inference(step,[status(thm)],[t24765,t2528]) ).
cnf(t24767,plain,
multiply(sFlat2,a) = multiply(identity,sFlat0),
inference(step,[status(thm)],[t24766,t105]) ).
cnf(t24768,plain,
multiply(sFlat2,a) = sFlat0,
inference(step,[status(thm)],[t24767,t22]) ).
cnf(t23761,plain,
multiply(sFlat2,a) = sFlat0,
inference(orient,[status(thm)],[t24768]) ).
cnf(t23768,plain,
multiply(sFlat2,greatest_lower_bound(identity,a)) = greatest_lower_bound(sFlat2,sFlat0),
inference(cp,[status(thm)],[t1879,t23761]) ).
cnf(t24786,plain,
multiply(sFlat2,sFlat1) = greatest_lower_bound(sFlat2,sFlat0),
inference(step,[status(thm)],[t23768,t84]) ).
cnf(t24787,plain,
identity = greatest_lower_bound(sFlat2,sFlat0),
inference(step,[status(thm)],[t24786,t123]) ).
cnf(t24788,plain,
identity = greatest_lower_bound(sFlat0,sFlat2),
inference(step,[status(thm)],[t24787,t67]) ).
cnf(t24789,plain,
identity = sFlat3,
inference(step,[status(thm)],[t24788,t1027]) ).
cnf(t23809,plain,
identity = sFlat3,
inference(orient,[status(thm)],[t24789]) ).
cnf(t1077,plain,
least_upper_bound(sFlat3,least_upper_bound(identity,X1)) = least_upper_bound(sFlat3,X1),
inference(cp,[status(thm)],[t92,t1074]) ).
cnf(t1303,plain,
least_upper_bound(sFlat3,least_upper_bound(identity,X1)) = least_upper_bound(sFlat3,X1),
inference(orient,[status(thm)],[t1077]) ).
cnf(t1309,plain,
least_upper_bound(sFlat3,a) = least_upper_bound(sFlat3,sFlat0),
inference(cp,[status(thm)],[t1303,t102]) ).
cnf(t24039,plain,
least_upper_bound(sFlat3,a) = least_upper_bound(sFlat0,sFlat3),
inference(step,[status(thm)],[t1309,t88]) ).
cnf(t1037,plain,
sFlat0 = least_upper_bound(sFlat0,sFlat3),
inference(cp,[status(thm)],[t26,t1027]) ).
cnf(t1054,plain,
least_upper_bound(sFlat0,sFlat3) = sFlat0,
inference(orient,[status(thm)],[t1037]) ).
cnf(t24040,plain,
least_upper_bound(sFlat3,a) = sFlat0,
inference(step,[status(thm)],[t24039,t1054]) ).
cnf(t1313,plain,
least_upper_bound(sFlat3,a) = sFlat0,
inference(orient,[status(thm)],[t24040]) ).
cnf(t312,plain,
least_upper_bound(sFlat0,greatest_lower_bound(a,X1)) = least_upper_bound(identity,a),
inference(cp,[status(thm)],[t310,t26]) ).
cnf(t23977,plain,
least_upper_bound(sFlat0,greatest_lower_bound(a,X1)) = sFlat0,
inference(step,[status(thm)],[t312,t102]) ).
cnf(t318,plain,
least_upper_bound(sFlat0,greatest_lower_bound(a,X1)) = sFlat0,
inference(orient,[status(thm)],[t23977]) ).
cnf(t321,plain,
greatest_lower_bound(a,X1) = greatest_lower_bound(greatest_lower_bound(a,X1),sFlat0),
inference(cp,[status(thm)],[t181,t318]) ).
cnf(t23990,plain,
greatest_lower_bound(a,X1) = greatest_lower_bound(a,greatest_lower_bound(X1,sFlat0)),
inference(step,[status(thm)],[t321,t71]) ).
cnf(t557,plain,
greatest_lower_bound(a,greatest_lower_bound(X1,sFlat0)) = greatest_lower_bound(a,X1),
inference(orient,[status(thm)],[t23990]) ).
cnf(t560,plain,
greatest_lower_bound(a,X1) = greatest_lower_bound(a,greatest_lower_bound(sFlat0,X1)),
inference(cp,[status(thm)],[t557,t67]) ).
cnf(t815,plain,
greatest_lower_bound(a,greatest_lower_bound(sFlat0,X1)) = greatest_lower_bound(a,X1),
inference(orient,[status(thm)],[t560]) ).
cnf(t1032,plain,
greatest_lower_bound(a,sFlat2) = greatest_lower_bound(a,sFlat3),
inference(cp,[status(thm)],[t815,t1027]) ).
cnf(t24031,plain,
greatest_lower_bound(sFlat2,a) = greatest_lower_bound(a,sFlat3),
inference(step,[status(thm)],[t1032,t67]) ).
cnf(t24032,plain,
greatest_lower_bound(sFlat2,a) = greatest_lower_bound(sFlat3,a),
inference(step,[status(thm)],[t24031,t67]) ).
cnf(t1078,plain,
greatest_lower_bound(sFlat3,a) = greatest_lower_bound(sFlat2,a),
inference(orient,[status(thm)],[t24032]) ).
cnf(t24724,plain,
greatest_lower_bound(sFlat3,a) = sFlat1,
inference(step,[status(thm)],[t1078,t22629]) ).
cnf(t22630,plain,
greatest_lower_bound(sFlat3,a) = sFlat1,
inference(orient,[status(thm)],[t24724]) ).
cnf(goal_0,negated_conjecture,
greatest_lower_bound(least_upper_bound(a,identity),inverse(greatest_lower_bound(a,identity))) != identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
greatest_lower_bound(least_upper_bound(identity,a),inverse(greatest_lower_bound(a,identity))) != identity,
inference(rw,[status(thm)],[goal_0,t88]) ).
cnf(g0_1,plain,
greatest_lower_bound(least_upper_bound(sFlat3,a),inverse(greatest_lower_bound(a,identity))) != identity,
inference(rw,[status(thm)],[g0_0,t23809]) ).
cnf(g0_2,plain,
greatest_lower_bound(sFlat0,inverse(greatest_lower_bound(a,identity))) != identity,
inference(rw,[status(thm)],[g0_1,t1313]) ).
cnf(g0_3,plain,
greatest_lower_bound(sFlat0,inverse(greatest_lower_bound(identity,a))) != identity,
inference(rw,[status(thm)],[g0_2,t67]) ).
cnf(g0_4,plain,
greatest_lower_bound(sFlat0,inverse(greatest_lower_bound(sFlat3,a))) != identity,
inference(rw,[status(thm)],[g0_3,t23809]) ).
cnf(g0_5,plain,
greatest_lower_bound(sFlat0,inverse(sFlat1)) != identity,
inference(rw,[status(thm)],[g0_4,t22630]) ).
cnf(g0_6,plain,
greatest_lower_bound(sFlat0,sFlat2) != identity,
inference(rw,[status(thm)],[g0_5,t108]) ).
cnf(g0_7,plain,
sFlat3 != identity,
inference(rw,[status(thm)],[g0_6,t1027]) ).
cnf(g0_8,plain,
sFlat3 != sFlat3,
inference(rw,[status(thm)],[g0_7,t23809]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP183-2 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/5.37 % Computer : n018.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Wed Sep 23 14:04:38 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 19.44/8.08 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.44/8.08 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------