%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP508-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n004.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:27:23 PM UTC 2026
% Result : Unsatisfiable 22.89s 3.46s
% Output : CNFRefutation 22.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 117
% Number of leaves : 4
% Syntax : Number of clauses : 262 ( 262 unt; 0 nHn; 104 RR)
% Number of literals : 262 ( 261 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 16 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 320 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t1,axiom,
sFlat0 = multiply(b,a),
introduced(definition) ).
cnf(t13,plain,
multiply(b,a) = sFlat0,
inference(orient,[status(thm)],[t1]) ).
cnf(t2,axiom,
sFlat1 = multiply(a,b),
introduced(definition) ).
cnf(t9,plain,
multiply(a,b) = sFlat1,
inference(orient,[status(thm)],[t2]) ).
cnf(t0,axiom,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(X5,inverse(X6)),inverse(X4))))))),X6) = X5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t3,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(X5,inverse(X6)),inverse(X4))))))),X6) = X5,
inference(orient,[status(thm)],[t0]) ).
cnf(t14,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),multiply(a,b))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(X1,inverse(X4)),inverse(X3))))))),X4),
inference(cp,[status(thm)],[t3,t13]) ).
cnf(t27427,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(X1,inverse(X4)),inverse(X3))))))),X4),
inference(step,[status(thm)],[t14,t9]) ).
cnf(t17,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(multiply(X3,inverse(X4)),inverse(X2))))))),X4) = X3,
inference(orient,[status(thm)],[t27427]) ).
cnf(t18,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(X1,inverse(X2)),inverse(a))))))),X2),
inference(cp,[status(thm)],[t17,t13]) ).
cnf(t31,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(X1,inverse(X2)),inverse(a))))))),X2) = X1,
inference(orient,[status(thm)],[t18]) ).
cnf(t39,plain,
inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(X1,inverse(inverse(X2))),inverse(a))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(X1,inverse(a))))))),X2),
inference(cp,[status(thm)],[t31,t31]) ).
cnf(t301,plain,
inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(X1,inverse(inverse(X2))),inverse(a))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(X1,inverse(a))))))),X2),
inference(orient,[status(thm)],[t39]) ).
cnf(t327,plain,
X1 = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(X1,inverse(a))))))),X2),inverse(X2)),
inference(cp,[status(thm)],[t31,t301]) ).
cnf(t338,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(X1,inverse(a))))))),X2),inverse(X2)) = X1,
inference(orient,[status(thm)],[t327]) ).
cnf(t339,plain,
multiply(X1,inverse(inverse(X2))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(X1,inverse(a))))))),X2),X3),inverse(X3)),
inference(cp,[status(thm)],[t338,t301]) ).
cnf(t499,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(X1,inverse(a))))))),X2),X3),inverse(X3)) = multiply(X1,inverse(inverse(X2))),
inference(orient,[status(thm)],[t339]) ).
cnf(t500,plain,
multiply(multiply(X1,inverse(X2)),inverse(inverse(X2))) = multiply(multiply(X1,X3),inverse(X3)),
inference(cp,[status(thm)],[t499,t31]) ).
cnf(t551,plain,
multiply(multiply(X1,inverse(X2)),inverse(inverse(X2))) = multiply(multiply(X1,X3),inverse(X3)),
inference(orient,[status(thm)],[t500]) ).
cnf(t600,plain,
multiply(multiply(X1,X2),inverse(X2)) = multiply(multiply(X1,X3),inverse(X3)),
inference(cp,[status(thm)],[t551,t551]) ).
cnf(t650,plain,
multiply(multiply(X1,X2),inverse(X2)) = multiply(multiply(X1,X3),inverse(X3)),
inference(orient,[status(thm)],[t600]) ).
cnf(t704,plain,
multiply(multiply(multiply(X1,X2),X3),inverse(X3)) = multiply(multiply(multiply(X1,X4),inverse(X4)),inverse(inverse(X2))),
inference(cp,[status(thm)],[t650,t650]) ).
cnf(t870,plain,
multiply(multiply(multiply(X1,X2),X3),inverse(X3)) = multiply(multiply(multiply(X1,X4),inverse(X4)),inverse(inverse(X2))),
inference(orient,[status(thm)],[t704]) ).
cnf(t15,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(a,b)),sFlat0)),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(X1,inverse(X4)),inverse(X3))))))),X4),
inference(cp,[status(thm)],[t3,t13]) ).
cnf(t27428,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(X1,inverse(X4)),inverse(X3))))))),X4),
inference(step,[status(thm)],[t15,t9]) ).
cnf(t57,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(multiply(X3,inverse(X4)),inverse(X2))))))),X4) = X3,
inference(orient,[status(thm)],[t27428]) ).
cnf(t659,plain,
multiply(multiply(b,X1),inverse(X1)) = multiply(sFlat0,inverse(a)),
inference(cp,[status(thm)],[t650,t13]) ).
cnf(t706,plain,
multiply(multiply(b,X1),inverse(X1)) = multiply(sFlat0,inverse(a)),
inference(orient,[status(thm)],[t659]) ).
cnf(t728,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(multiply(b,multiply(multiply(X1,inverse(X2)),inverse(X3))),X3)),multiply(sFlat0,inverse(a))))),X2),
inference(cp,[status(thm)],[t57,t706]) ).
cnf(t9625,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(multiply(b,multiply(multiply(X1,inverse(X2)),inverse(X3))),X3)),multiply(sFlat0,inverse(a))))),X2) = X1,
inference(orient,[status(thm)],[t728]) ).
cnf(t664,plain,
multiply(multiply(a,X1),inverse(X1)) = multiply(sFlat1,inverse(b)),
inference(cp,[status(thm)],[t650,t9]) ).
cnf(t745,plain,
multiply(multiply(a,X1),inverse(X1)) = multiply(sFlat1,inverse(b)),
inference(orient,[status(thm)],[t664]) ).
cnf(t9629,plain,
a = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(multiply(b,multiply(sFlat1,inverse(b))),inverse(X1))),multiply(sFlat0,inverse(a))))),X1),
inference(cp,[status(thm)],[t9625,t745]) ).
cnf(t9822,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(multiply(b,multiply(sFlat1,inverse(b))),inverse(X1))),multiply(sFlat0,inverse(a))))),X1) = a,
inference(orient,[status(thm)],[t9629]) ).
cnf(t9823,plain,
a = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(sFlat0,inverse(a))),multiply(sFlat0,inverse(a))))),multiply(sFlat1,inverse(b))),
inference(cp,[status(thm)],[t9822,t706]) ).
cnf(t9939,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(sFlat0,inverse(a))),multiply(sFlat0,inverse(a))))),multiply(sFlat1,inverse(b))) = a,
inference(orient,[status(thm)],[t9823]) ).
cnf(t9968,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(sFlat0,inverse(a))),multiply(sFlat0,inverse(a))))),X1),inverse(X1)) = multiply(a,inverse(multiply(sFlat1,inverse(b)))),
inference(cp,[status(thm)],[t650,t9939]) ).
cnf(t10122,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(sFlat0,inverse(a))),multiply(sFlat0,inverse(a))))),X1),inverse(X1)) = multiply(a,inverse(multiply(sFlat1,inverse(b)))),
inference(orient,[status(thm)],[t9968]) ).
cnf(t369,plain,
inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(X1,inverse(a))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(X1))))),X3),
inference(cp,[status(thm)],[t57,t338]) ).
cnf(t383,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3))))),X2) = inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(X3,inverse(a))))))),
inference(orient,[status(thm)],[t369]) ).
cnf(t10124,plain,
multiply(a,inverse(multiply(sFlat1,inverse(b)))) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(a,inverse(a))))))),inverse(a)),
inference(cp,[status(thm)],[t10122,t383]) ).
cnf(t9630,plain,
b = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(multiply(b,multiply(sFlat0,inverse(a))),inverse(X1))),multiply(sFlat0,inverse(a))))),X1),
inference(cp,[status(thm)],[t9625,t706]) ).
cnf(t9972,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(multiply(b,multiply(sFlat0,inverse(a))),inverse(X1))),multiply(sFlat0,inverse(a))))),X1) = b,
inference(orient,[status(thm)],[t9630]) ).
cnf(t9973,plain,
b = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(sFlat0,inverse(a))),multiply(sFlat0,inverse(a))))),multiply(sFlat0,inverse(a))),
inference(cp,[status(thm)],[t9972,t706]) ).
cnf(t10089,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(sFlat0,inverse(a))),multiply(sFlat0,inverse(a))))),multiply(sFlat0,inverse(a))) = b,
inference(orient,[status(thm)],[t9973]) ).
cnf(t10123,plain,
multiply(a,inverse(multiply(sFlat1,inverse(b)))) = multiply(b,inverse(multiply(sFlat0,inverse(a)))),
inference(cp,[status(thm)],[t10122,t10089]) ).
cnf(t10251,plain,
multiply(a,inverse(multiply(sFlat1,inverse(b)))) = multiply(b,inverse(multiply(sFlat0,inverse(a)))),
inference(orient,[status(thm)],[t10123]) ).
cnf(t27465,plain,
multiply(b,inverse(multiply(sFlat0,inverse(a)))) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(a,inverse(a))))))),inverse(a)),
inference(step,[status(thm)],[t10124,t10251]) ).
cnf(t10666,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(a,inverse(a))))))),inverse(a)) = multiply(b,inverse(multiply(sFlat0,inverse(a)))),
inference(orient,[status(thm)],[t27465]) ).
cnf(t10686,plain,
a = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(inverse(a))),
inference(cp,[status(thm)],[t338,t10666]) ).
cnf(t10723,plain,
multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(inverse(a))) = a,
inference(orient,[status(thm)],[t10686]) ).
cnf(t10750,plain,
b = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(X1,inverse(a))),multiply(X1,inverse(a))))),multiply(sFlat0,inverse(a))),
inference(cp,[status(thm)],[t57,t10723]) ).
cnf(t11109,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(X1,inverse(a))),multiply(X1,inverse(a))))),multiply(sFlat0,inverse(a))) = b,
inference(orient,[status(thm)],[t10750]) ).
cnf(t11115,plain,
b = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(multiply(b,multiply(multiply(X1,inverse(inverse(a))),inverse(X2))),X2)),multiply(sFlat0,inverse(a))))),inverse(a))))),multiply(sFlat0,inverse(a))),
inference(cp,[status(thm)],[t11109,t9625]) ).
cnf(t27471,plain,
b = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(X1),X1))),multiply(sFlat0,inverse(a))),
inference(step,[status(thm)],[t11115,t9625]) ).
cnf(t11266,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(X1),X1))),multiply(sFlat0,inverse(a))) = b,
inference(orient,[status(thm)],[t27471]) ).
cnf(t11336,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(X1),X1))),X2),X3),inverse(X3)) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(inverse(X2))),
inference(cp,[status(thm)],[t870,t11266]) ).
cnf(t12814,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(X1),X1))),X2),X3),inverse(X3)) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(inverse(X2))),
inference(orient,[status(thm)],[t11336]) ).
cnf(t12815,plain,
multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(inverse(X1))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(X1,inverse(a))))))),X2),inverse(X2)),
inference(cp,[status(thm)],[t12814,t383]) ).
cnf(t27475,plain,
multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(inverse(X1))) = X1,
inference(step,[status(thm)],[t12815,t338]) ).
cnf(t12981,plain,
multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(inverse(X1))) = X1,
inference(orient,[status(thm)],[t27475]) ).
cnf(t744,plain,
multiply(multiply(multiply(b,X1),X2),inverse(X2)) = multiply(multiply(sFlat0,inverse(a)),inverse(inverse(X1))),
inference(cp,[status(thm)],[t650,t706]) ).
cnf(t786,plain,
multiply(multiply(multiply(b,X1),X2),inverse(X2)) = multiply(multiply(sFlat0,inverse(a)),inverse(inverse(X1))),
inference(orient,[status(thm)],[t744]) ).
cnf(t13022,plain,
multiply(multiply(sFlat0,inverse(a)),inverse(inverse(inverse(multiply(sFlat0,inverse(a)))))) = multiply(X1,inverse(inverse(inverse(X1)))),
inference(cp,[status(thm)],[t786,t12981]) ).
cnf(t10699,plain,
multiply(a,inverse(inverse(inverse(a)))) = multiply(multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),X1),inverse(X1)),
inference(cp,[status(thm)],[t499,t10666]) ).
cnf(t27466,plain,
multiply(a,inverse(inverse(inverse(a)))) = multiply(multiply(sFlat0,inverse(a)),inverse(inverse(inverse(multiply(sFlat0,inverse(a)))))),
inference(step,[status(thm)],[t10699,t786]) ).
cnf(t10784,plain,
multiply(multiply(sFlat0,inverse(a)),inverse(inverse(inverse(multiply(sFlat0,inverse(a)))))) = multiply(a,inverse(inverse(inverse(a)))),
inference(orient,[status(thm)],[t27466]) ).
cnf(t27478,plain,
multiply(a,inverse(inverse(inverse(a)))) = multiply(X1,inverse(inverse(inverse(X1)))),
inference(step,[status(thm)],[t13022,t10784]) ).
cnf(t13983,plain,
multiply(a,inverse(inverse(inverse(a)))) = multiply(X1,inverse(inverse(inverse(X1)))),
inference(orient,[status(thm)],[t27478]) ).
cnf(t14056,plain,
multiply(a,inverse(inverse(inverse(a)))) = inverse(multiply(b,inverse(multiply(sFlat0,inverse(a))))),
inference(cp,[status(thm)],[t13983,t12981]) ).
cnf(t27483,plain,
multiply(sFlat0,inverse(inverse(inverse(sFlat0)))) = inverse(multiply(b,inverse(multiply(sFlat0,inverse(a))))),
inference(step,[status(thm)],[t14056,t13983]) ).
cnf(t14204,plain,
inverse(multiply(b,inverse(multiply(sFlat0,inverse(a))))) = multiply(sFlat0,inverse(inverse(inverse(sFlat0)))),
inference(orient,[status(thm)],[t27483]) ).
cnf(t14209,plain,
multiply(b,inverse(multiply(sFlat0,inverse(a)))) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(multiply(sFlat0,inverse(inverse(inverse(sFlat0)))))),
inference(cp,[status(thm)],[t12981,t14204]) ).
cnf(t16780,plain,
multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(multiply(sFlat0,inverse(inverse(inverse(sFlat0)))))) = multiply(b,inverse(multiply(sFlat0,inverse(a)))),
inference(orient,[status(thm)],[t14209]) ).
cnf(t13078,plain,
multiply(multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),X1),inverse(X1)) = multiply(X2,inverse(inverse(inverse(X2)))),
inference(cp,[status(thm)],[t650,t12981]) ).
cnf(t27484,plain,
multiply(multiply(sFlat0,inverse(a)),inverse(inverse(inverse(multiply(sFlat0,inverse(a)))))) = multiply(X2,inverse(inverse(inverse(X2)))),
inference(step,[status(thm)],[t13078,t786]) ).
cnf(t27485,plain,
multiply(a,inverse(inverse(inverse(a)))) = multiply(X2,inverse(inverse(inverse(X2)))),
inference(step,[status(thm)],[t27484,t13983]) ).
cnf(t27486,plain,
multiply(sFlat0,inverse(inverse(inverse(sFlat0)))) = multiply(X2,inverse(inverse(inverse(X2)))),
inference(step,[status(thm)],[t27485,t13983]) ).
cnf(t14332,plain,
multiply(sFlat0,inverse(inverse(inverse(sFlat0)))) = multiply(X1,inverse(inverse(inverse(X1)))),
inference(orient,[status(thm)],[t27486]) ).
cnf(t14399,plain,
multiply(X1,inverse(inverse(inverse(X1)))) = multiply(X2,inverse(inverse(inverse(X2)))),
inference(cp,[status(thm)],[t14332,t14332]) ).
cnf(t14566,plain,
multiply(X1,inverse(inverse(inverse(X1)))) = multiply(X2,inverse(inverse(inverse(X2)))),
inference(orient,[status(thm)],[t14399]) ).
cnf(t16781,plain,
multiply(b,inverse(multiply(sFlat0,inverse(a)))) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(multiply(X1,inverse(inverse(inverse(X1)))))),
inference(cp,[status(thm)],[t16780,t14566]) ).
cnf(t16845,plain,
multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(multiply(X1,inverse(inverse(inverse(X1)))))) = multiply(b,inverse(multiply(sFlat0,inverse(a)))),
inference(orient,[status(thm)],[t16781]) ).
cnf(t575,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(X1,inverse(X2)),inverse(a))))))),X2) = inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(multiply(X1,X3),inverse(X3)),inverse(a))))))),
inference(cp,[status(thm)],[t301,t551]) ).
cnf(t27431,plain,
X1 = inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(multiply(X1,X3),inverse(X3)),inverse(a))))))),
inference(step,[status(thm)],[t575,t31]) ).
cnf(t1273,plain,
inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(multiply(X1,X2),inverse(X2)),inverse(a))))))) = X1,
inference(orient,[status(thm)],[t27431]) ).
cnf(t14570,plain,
multiply(X1,inverse(inverse(inverse(X1)))) = multiply(multiply(multiply(X2,inverse(multiply(multiply(X2,X3),inverse(X3)))),X4),inverse(X4)),
inference(cp,[status(thm)],[t14566,t870]) ).
cnf(t17600,plain,
multiply(X1,inverse(inverse(inverse(X1)))) = multiply(multiply(multiply(X2,inverse(multiply(multiply(X2,X3),inverse(X3)))),X4),inverse(X4)),
inference(orient,[status(thm)],[t14570]) ).
cnf(t17656,plain,
X1 = inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(multiply(multiply(multiply(X2,inverse(multiply(multiply(X2,X3),inverse(X3)))),X4),inverse(X4)),inverse(inverse(inverse(inverse(X1))))),inverse(a))))))),
inference(cp,[status(thm)],[t1273,t17600]) ).
cnf(t27509,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(multiply(multiply(X2,inverse(multiply(multiply(X2,X3),inverse(X3)))),X4),inverse(X4)),inverse(a))))))),inverse(inverse(X1))),
inference(step,[status(thm)],[t17656,t301]) ).
cnf(t27510,plain,
X1 = multiply(multiply(X2,inverse(multiply(multiply(X2,X3),inverse(X3)))),inverse(inverse(X1))),
inference(step,[status(thm)],[t27509,t1273]) ).
cnf(t17984,plain,
multiply(multiply(X1,inverse(multiply(multiply(X1,X2),inverse(X2)))),inverse(inverse(X3))) = X3,
inference(orient,[status(thm)],[t27510]) ).
cnf(t18113,plain,
multiply(b,inverse(multiply(sFlat0,inverse(a)))) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(inverse(multiply(X1,inverse(multiply(multiply(X1,X2),inverse(X2))))))),
inference(cp,[status(thm)],[t16845,t17984]) ).
cnf(t27511,plain,
multiply(b,inverse(multiply(sFlat0,inverse(a)))) = multiply(X1,inverse(multiply(multiply(X1,X2),inverse(X2)))),
inference(step,[status(thm)],[t18113,t12981]) ).
cnf(t18196,plain,
multiply(X1,inverse(multiply(multiply(X1,X2),inverse(X2)))) = multiply(b,inverse(multiply(sFlat0,inverse(a)))),
inference(orient,[status(thm)],[t27511]) ).
cnf(t893,plain,
multiply(multiply(multiply(multiply(X1,X2),X3),inverse(X3)),inverse(inverse(inverse(X2)))) = multiply(multiply(multiply(multiply(X1,X4),inverse(X4)),X5),inverse(X5)),
inference(cp,[status(thm)],[t870,t650]) ).
cnf(t27438,plain,
multiply(multiply(multiply(multiply(X1,X2),inverse(X2)),sFlat0),inverse(sFlat0)) = multiply(multiply(multiply(multiply(X1,X4),inverse(X4)),X5),inverse(X5)),
inference(step,[status(thm)],[t893,t870]) ).
cnf(t1903,plain,
multiply(multiply(multiply(multiply(X1,X2),inverse(X2)),sFlat0),inverse(sFlat0)) = multiply(multiply(multiply(multiply(X1,X3),inverse(X3)),X4),inverse(X4)),
inference(orient,[status(thm)],[t27438]) ).
cnf(t1904,plain,
multiply(multiply(multiply(multiply(X1,X2),inverse(X2)),X3),inverse(X3)) = multiply(multiply(multiply(multiply(X1,X4),inverse(X4)),X5),inverse(X5)),
inference(cp,[status(thm)],[t1903,t650]) ).
cnf(t2123,plain,
multiply(multiply(multiply(multiply(X1,X2),inverse(X2)),X3),inverse(X3)) = multiply(multiply(multiply(multiply(X1,X4),inverse(X4)),X5),inverse(X5)),
inference(orient,[status(thm)],[t1904]) ).
cnf(t18210,plain,
multiply(b,inverse(multiply(sFlat0,inverse(a)))) = multiply(multiply(multiply(X1,X2),inverse(X2)),inverse(multiply(multiply(multiply(multiply(X1,X3),inverse(X3)),X4),inverse(X4)))),
inference(cp,[status(thm)],[t18196,t2123]) ).
cnf(t21426,plain,
multiply(multiply(multiply(X1,X2),inverse(X2)),inverse(multiply(multiply(multiply(multiply(X1,X3),inverse(X3)),X4),inverse(X4)))) = multiply(b,inverse(multiply(sFlat0,inverse(a)))),
inference(orient,[status(thm)],[t18210]) ).
cnf(t10753,plain,
b = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(multiply(X1,inverse(a))),multiply(X1,inverse(a))))),multiply(sFlat0,inverse(a))),
inference(cp,[status(thm)],[t17,t10723]) ).
cnf(t11915,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(multiply(X1,inverse(a))),multiply(X1,inverse(a))))),multiply(sFlat0,inverse(a))) = b,
inference(orient,[status(thm)],[t10753]) ).
cnf(t11921,plain,
b = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(multiply(multiply(b,multiply(multiply(X1,inverse(inverse(a))),inverse(X2))),X2)),multiply(sFlat0,inverse(a))))),inverse(a))))),multiply(sFlat0,inverse(a))),
inference(cp,[status(thm)],[t11915,t9625]) ).
cnf(t27474,plain,
b = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(X1),X1))),multiply(sFlat0,inverse(a))),
inference(step,[status(thm)],[t11921,t9625]) ).
cnf(t12072,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(X1),X1))),multiply(sFlat0,inverse(a))) = b,
inference(orient,[status(thm)],[t27474]) ).
cnf(t16,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(X1,inverse(X4)),inverse(a))))))),X4),
inference(cp,[status(thm)],[t3,t13]) ).
cnf(t167,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(X3,inverse(X4)),inverse(a))))))),X4) = X3,
inference(orient,[status(thm)],[t16]) ).
cnf(t758,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(a,inverse(X1)),inverse(a))))))),X1) = inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(sFlat1,inverse(b)),inverse(a))))))),
inference(cp,[status(thm)],[t301,t745]) ).
cnf(t27430,plain,
a = inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(sFlat1,inverse(b)),inverse(a))))))),
inference(step,[status(thm)],[t758,t31]) ).
cnf(t1041,plain,
inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(sFlat1,inverse(b)),inverse(a))))))) = a,
inference(orient,[status(thm)],[t27430]) ).
cnf(t13019,plain,
multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(sFlat1,inverse(b)),inverse(a)))))) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(a)),
inference(cp,[status(thm)],[t12981,t1041]) ).
cnf(t23386,plain,
multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(sFlat1,inverse(b)),inverse(a)))))) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(a)),
inference(orient,[status(thm)],[t13019]) ).
cnf(t27526,plain,
inverse(multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(a))) = a,
inference(step,[status(thm)],[t1041,t23386]) ).
cnf(t23435,plain,
inverse(multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(a))) = a,
inference(rw,[status(thm)],[t27526]) ).
cnf(t23438,plain,
inverse(multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(a))) = a,
inference(orient,[status(thm)],[t23435]) ).
cnf(t23509,plain,
b = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sFlat0),multiply(b,a)))),multiply(sFlat0,inverse(a))),
inference(cp,[status(thm)],[t167,t23438]) ).
cnf(t27531,plain,
b = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sFlat0),sFlat0))),multiply(sFlat0,inverse(a))),
inference(step,[status(thm)],[t23509,t13]) ).
cnf(t24195,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sFlat0),sFlat0))),multiply(sFlat0,inverse(a))) = b,
inference(orient,[status(thm)],[t27531]) ).
cnf(t24377,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sFlat0),sFlat0))) = inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(a))))))),
inference(cp,[status(thm)],[t1273,t24195]) ).
cnf(t27532,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sFlat0),sFlat0))) = inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,a)))),
inference(step,[status(thm)],[t24377,t23438]) ).
cnf(t27533,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sFlat0),sFlat0))) = inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),sFlat0))),
inference(step,[status(thm)],[t27532,t13]) ).
cnf(t24413,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sFlat0),sFlat0))) = inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),sFlat0))),
inference(orient,[status(thm)],[t27533]) ).
cnf(t24595,plain,
multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sFlat0),sFlat0)) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),sFlat0))))),
inference(cp,[status(thm)],[t12981,t24413]) ).
cnf(t27534,plain,
multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sFlat0),sFlat0)) = multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),sFlat0)),
inference(step,[status(thm)],[t24595,t12981]) ).
cnf(t24723,plain,
multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sFlat0),sFlat0)) = multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),sFlat0)),
inference(orient,[status(thm)],[t27534]) ).
cnf(t24905,plain,
inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))) = inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),sFlat0)),inverse(multiply(inverse(sFlat0),sFlat0))),inverse(a))))))),
inference(cp,[status(thm)],[t1273,t24723]) ).
cnf(t27535,plain,
inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))) = inverse(multiply(inverse(sFlat0),sFlat1)),
inference(step,[status(thm)],[t24905,t1273]) ).
cnf(t24941,plain,
inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))) = inverse(multiply(inverse(sFlat0),sFlat1)),
inference(orient,[status(thm)],[t27535]) ).
cnf(t25106,plain,
multiply(inverse(multiply(X1,X2)),multiply(X2,X1)) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(inverse(multiply(inverse(sFlat0),sFlat1)))),
inference(cp,[status(thm)],[t12981,t24941]) ).
cnf(t27536,plain,
multiply(inverse(multiply(X1,X2)),multiply(X2,X1)) = multiply(inverse(sFlat0),sFlat1),
inference(step,[status(thm)],[t25106,t12981]) ).
cnf(t25193,plain,
multiply(inverse(multiply(X1,X2)),multiply(X2,X1)) = multiply(inverse(sFlat0),sFlat1),
inference(orient,[status(thm)],[t27536]) ).
cnf(t25379,plain,
multiply(multiply(inverse(multiply(X1,X2)),X3),inverse(X3)) = multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(X2,X1))),
inference(cp,[status(thm)],[t650,t25193]) ).
cnf(t25417,plain,
multiply(multiply(inverse(multiply(X1,X2)),X3),inverse(X3)) = multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(X2,X1))),
inference(orient,[status(thm)],[t25379]) ).
cnf(t16897,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(inverse(multiply(X1,inverse(X2)))))),multiply(b,inverse(multiply(sFlat0,inverse(a))))))),X2),
inference(cp,[status(thm)],[t17,t16845]) ).
cnf(t27520,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(multiply(X1,inverse(X2))),multiply(b,inverse(multiply(sFlat0,inverse(a))))))),X2),
inference(step,[status(thm)],[t16897,t12981]) ).
cnf(t21910,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(multiply(X1,inverse(X2))),multiply(b,inverse(multiply(sFlat0,inverse(a))))))),X2) = X1,
inference(orient,[status(thm)],[t27520]) ).
cnf(t21927,plain,
multiply(b,inverse(multiply(sFlat0,inverse(a)))) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(X1),multiply(b,inverse(multiply(sFlat0,inverse(a))))))),inverse(X1)),
inference(cp,[status(thm)],[t21910,t12981]) ).
cnf(t22899,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(X1),multiply(b,inverse(multiply(sFlat0,inverse(a))))))),inverse(X1)) = multiply(b,inverse(multiply(sFlat0,inverse(a)))),
inference(orient,[status(thm)],[t21927]) ).
cnf(t22932,plain,
multiply(b,inverse(multiply(sFlat0,inverse(a)))) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(X1,multiply(b,inverse(multiply(sFlat0,inverse(a))))))),inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(multiply(X1,X2),inverse(X2)),inverse(a)))))))),
inference(cp,[status(thm)],[t22899,t1273]) ).
cnf(t27524,plain,
multiply(b,inverse(multiply(sFlat0,inverse(a)))) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(X1,multiply(b,inverse(multiply(sFlat0,inverse(a))))))),X1),
inference(step,[status(thm)],[t22932,t1273]) ).
cnf(t23124,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(X1,multiply(b,inverse(multiply(sFlat0,inverse(a))))))),X1) = multiply(b,inverse(multiply(sFlat0,inverse(a)))),
inference(orient,[status(thm)],[t27524]) ).
cnf(t25238,plain,
multiply(inverse(sFlat0),sFlat1) = multiply(inverse(X1),multiply(inverse(inverse(X1)),multiply(b,inverse(multiply(sFlat0,inverse(a)))))),
inference(cp,[status(thm)],[t25193,t12981]) ).
cnf(t25823,plain,
multiply(inverse(X1),multiply(inverse(inverse(X1)),multiply(b,inverse(multiply(sFlat0,inverse(a)))))) = multiply(inverse(sFlat0),sFlat1),
inference(orient,[status(thm)],[t25238]) ).
cnf(t25861,plain,
multiply(b,inverse(multiply(sFlat0,inverse(a)))) = multiply(inverse(multiply(inverse(sFlat0),sFlat1)),inverse(inverse(multiply(inverse(sFlat0),sFlat1)))),
inference(cp,[status(thm)],[t23124,t25823]) ).
cnf(t26501,plain,
multiply(inverse(multiply(inverse(sFlat0),sFlat1)),inverse(inverse(multiply(inverse(sFlat0),sFlat1)))) = multiply(b,inverse(multiply(sFlat0,inverse(a)))),
inference(orient,[status(thm)],[t25861]) ).
cnf(t26504,plain,
multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(sFlat1,inverse(sFlat0)))) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(inverse(inverse(multiply(inverse(sFlat0),sFlat1))))),
inference(cp,[status(thm)],[t25417,t26501]) ).
cnf(t59,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(X1,inverse(X2)),inverse(a))))))),X2),
inference(cp,[status(thm)],[t57,t13]) ).
cnf(t85,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(X1,inverse(X2)),inverse(a))))))),X2) = X1,
inference(orient,[status(thm)],[t59]) ).
cnf(t685,plain,
multiply(X1,X2) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(multiply(X1,X3),inverse(X3)),inverse(a))))))),X2),
inference(cp,[status(thm)],[t85,t650]) ).
cnf(t3429,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(multiply(X1,X2),inverse(X2)),inverse(a))))))),X3) = multiply(X1,X3),
inference(orient,[status(thm)],[t685]) ).
cnf(t3497,plain,
inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(multiply(X1,X2),inverse(X2)),inverse(a))))))) = inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(multiply(X1,X3),inverse(X3)),inverse(a))))))),
inference(cp,[status(thm)],[t1273,t3429]) ).
cnf(t27440,plain,
inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(multiply(X1,X2),inverse(X2)),inverse(a))))))) = X1,
inference(step,[status(thm)],[t3497,t1273]) ).
cnf(t3550,plain,
inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(multiply(X1,X2),inverse(X2)),inverse(a))))))) = X1,
inference(orient,[status(thm)],[t27440]) ).
cnf(t3553,plain,
inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(X1,inverse(a))))))) = inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(X1,inverse(a))))))),
inference(cp,[status(thm)],[t3550,t338]) ).
cnf(t3672,plain,
inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(X1,inverse(a))))))) = inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(X1,inverse(a))))))),
inference(orient,[status(thm)],[t3553]) ).
cnf(t3676,plain,
inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(X1,inverse(a))))))),a),inverse(a))))))) = inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),multiply(b,inverse(X1))))),
inference(cp,[status(thm)],[t3672,t338]) ).
cnf(t27441,plain,
inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(X1))))) = inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),multiply(b,inverse(X1))))),
inference(step,[status(thm)],[t3676,t338]) ).
cnf(t3750,plain,
inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),multiply(b,inverse(X1))))) = inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(X1))))),
inference(orient,[status(thm)],[t27441]) ).
cnf(t20,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat1),multiply(a,inverse(multiply(multiply(X1,inverse(X2)),inverse(b))))))),X2),
inference(cp,[status(thm)],[t17,t9]) ).
cnf(t43,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat1),multiply(a,inverse(multiply(multiply(X1,inverse(X2)),inverse(b))))))),X2) = X1,
inference(orient,[status(thm)],[t20]) ).
cnf(t771,plain,
multiply(a,X1) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat1),multiply(a,inverse(multiply(multiply(sFlat1,inverse(b)),inverse(b))))))),X1),
inference(cp,[status(thm)],[t43,t745]) ).
cnf(t1816,plain,
multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat1),multiply(a,inverse(multiply(multiply(sFlat1,inverse(b)),inverse(b))))))),X1) = multiply(a,X1),
inference(orient,[status(thm)],[t771]) ).
cnf(t1821,plain,
inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat1),multiply(a,inverse(multiply(multiply(sFlat1,inverse(b)),inverse(b))))))) = inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(multiply(a,X1),inverse(X1)),inverse(a))))))),
inference(cp,[status(thm)],[t1273,t1816]) ).
cnf(t27437,plain,
inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat1),multiply(a,inverse(multiply(multiply(sFlat1,inverse(b)),inverse(b))))))) = a,
inference(step,[status(thm)],[t1821,t1273]) ).
cnf(t1855,plain,
inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat1),multiply(a,inverse(multiply(multiply(sFlat1,inverse(b)),inverse(b))))))) = a,
inference(orient,[status(thm)],[t27437]) ).
cnf(t3753,plain,
inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat1),multiply(a,inverse(multiply(multiply(sFlat1,inverse(b)),inverse(b))))))))))) = inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),multiply(b,a)))),
inference(cp,[status(thm)],[t3750,t1855]) ).
cnf(t27442,plain,
inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,a)))) = inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),multiply(b,a)))),
inference(step,[status(thm)],[t3753,t1855]) ).
cnf(t27443,plain,
inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),sFlat0))) = inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),multiply(b,a)))),
inference(step,[status(thm)],[t27442,t13]) ).
cnf(t27444,plain,
inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),sFlat0))) = inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),sFlat0))),
inference(step,[status(thm)],[t27443,t13]) ).
cnf(t3816,plain,
inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),sFlat0))) = inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),sFlat0))),
inference(orient,[status(thm)],[t27444]) ).
cnf(t13016,plain,
multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),sFlat0)) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),sFlat0))))),
inference(cp,[status(thm)],[t12981,t3816]) ).
cnf(t27487,plain,
multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),sFlat0)) = multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),sFlat0)),
inference(step,[status(thm)],[t13016,t12981]) ).
cnf(t14990,plain,
multiply(inverse(multiply(inverse(sFlat1),sFlat0)),multiply(inverse(sFlat0),sFlat0)) = multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),sFlat0)),
inference(orient,[status(thm)],[t27487]) ).
cnf(t14998,plain,
inverse(multiply(inverse(sFlat1),sFlat0)) = inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),multiply(b,inverse(multiply(multiply(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),sFlat0)),inverse(multiply(inverse(sFlat0),sFlat0))),inverse(a))))))),
inference(cp,[status(thm)],[t1273,t14990]) ).
cnf(t27488,plain,
inverse(multiply(inverse(sFlat1),sFlat0)) = inverse(multiply(inverse(sFlat0),sFlat1)),
inference(step,[status(thm)],[t14998,t1273]) ).
cnf(t15029,plain,
inverse(multiply(inverse(sFlat1),sFlat0)) = inverse(multiply(inverse(sFlat0),sFlat1)),
inference(orient,[status(thm)],[t27488]) ).
cnf(t15036,plain,
multiply(inverse(sFlat1),sFlat0) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(inverse(multiply(inverse(sFlat0),sFlat1)))),
inference(cp,[status(thm)],[t12981,t15029]) ).
cnf(t27494,plain,
multiply(inverse(sFlat1),sFlat0) = multiply(inverse(sFlat0),sFlat1),
inference(step,[status(thm)],[t15036,t12981]) ).
cnf(t15130,plain,
multiply(inverse(sFlat1),sFlat0) = multiply(inverse(sFlat0),sFlat1),
inference(orient,[status(thm)],[t27494]) ).
cnf(t25236,plain,
multiply(inverse(sFlat0),sFlat1) = multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(sFlat0,inverse(sFlat1))),
inference(cp,[status(thm)],[t25193,t15130]) ).
cnf(t25385,plain,
multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(sFlat0,inverse(sFlat1))) = multiply(inverse(sFlat0),sFlat1),
inference(orient,[status(thm)],[t25236]) ).
cnf(t25397,plain,
multiply(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),X1),inverse(X1)) = multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(sFlat0,inverse(sFlat1)))),
inference(cp,[status(thm)],[t650,t25385]) ).
cnf(t27543,plain,
multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(sFlat1,inverse(sFlat0)))) = multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(sFlat0,inverse(sFlat1)))),
inference(step,[status(thm)],[t25397,t25417]) ).
cnf(t25781,plain,
multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(sFlat1,inverse(sFlat0)))) = multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(sFlat0,inverse(sFlat1)))),
inference(orient,[status(thm)],[t27543]) ).
cnf(t27546,plain,
multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(sFlat0,inverse(sFlat1)))) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(inverse(inverse(multiply(inverse(sFlat0),sFlat1))))),
inference(step,[status(thm)],[t26504,t25781]) ).
cnf(t27547,plain,
multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(sFlat0,inverse(sFlat1)))) = inverse(multiply(inverse(sFlat0),sFlat1)),
inference(step,[status(thm)],[t27546,t12981]) ).
cnf(t26527,plain,
multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(sFlat0,inverse(sFlat1)))) = inverse(multiply(inverse(sFlat0),sFlat1)),
inference(orient,[status(thm)],[t27547]) ).
cnf(t26531,plain,
multiply(inverse(sFlat0),sFlat1) = multiply(inverse(multiply(inverse(multiply(sFlat0,inverse(sFlat1))),multiply(inverse(sFlat0),sFlat1))),inverse(multiply(inverse(sFlat0),sFlat1))),
inference(cp,[status(thm)],[t25193,t26527]) ).
cnf(t25302,plain,
multiply(inverse(sFlat0),sFlat1) = multiply(inverse(multiply(sFlat0,inverse(sFlat1))),multiply(inverse(sFlat0),sFlat1)),
inference(cp,[status(thm)],[t25193,t15130]) ).
cnf(t25401,plain,
multiply(inverse(multiply(sFlat0,inverse(sFlat1))),multiply(inverse(sFlat0),sFlat1)) = multiply(inverse(sFlat0),sFlat1),
inference(orient,[status(thm)],[t25302]) ).
cnf(t27551,plain,
multiply(inverse(sFlat0),sFlat1) = multiply(inverse(multiply(inverse(sFlat0),sFlat1)),inverse(multiply(inverse(sFlat0),sFlat1))),
inference(step,[status(thm)],[t26531,t25401]) ).
cnf(t26570,plain,
multiply(inverse(multiply(inverse(sFlat0),sFlat1)),inverse(multiply(inverse(sFlat0),sFlat1))) = multiply(inverse(sFlat0),sFlat1),
inference(orient,[status(thm)],[t27551]) ).
cnf(t26571,plain,
multiply(inverse(sFlat0),sFlat1) = multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(multiply(inverse(sFlat0),sFlat1)),inverse(multiply(inverse(sFlat0),sFlat1)))),
inference(cp,[status(thm)],[t25193,t26570]) ).
cnf(t27552,plain,
multiply(inverse(sFlat0),sFlat1) = multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),sFlat1)),
inference(step,[status(thm)],[t26571,t26570]) ).
cnf(t26595,plain,
multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),sFlat1)) = multiply(inverse(sFlat0),sFlat1),
inference(orient,[status(thm)],[t27552]) ).
cnf(t26601,plain,
b = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(inverse(sFlat0),sFlat1))),multiply(sFlat0,inverse(a))),
inference(cp,[status(thm)],[t12072,t26595]) ).
cnf(t27553,plain,
b = multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(sFlat0,inverse(a))),
inference(step,[status(thm)],[t26601,t26595]) ).
cnf(t26618,plain,
multiply(inverse(multiply(inverse(sFlat0),sFlat1)),multiply(sFlat0,inverse(a))) = b,
inference(orient,[status(thm)],[t27553]) ).
cnf(t26624,plain,
multiply(b,inverse(multiply(sFlat0,inverse(a)))) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(multiply(multiply(multiply(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),X1),inverse(X1)),X2),inverse(X2)))),
inference(cp,[status(thm)],[t21426,t26618]) ).
cnf(t27554,plain,
multiply(b,inverse(multiply(sFlat0,inverse(a)))) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(multiply(multiply(multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(sFlat1,inverse(sFlat0)))),X2),inverse(X2)))),
inference(step,[status(thm)],[t26624,t25417]) ).
cnf(t27548,plain,
multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(sFlat1,inverse(sFlat0)))) = inverse(multiply(inverse(sFlat0),sFlat1)),
inference(step,[status(thm)],[t25781,t26527]) ).
cnf(t26528,plain,
multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(sFlat1,inverse(sFlat0)))) = inverse(multiply(inverse(sFlat0),sFlat1)),
inference(orient,[status(thm)],[t27548]) ).
cnf(t27555,plain,
multiply(b,inverse(multiply(sFlat0,inverse(a)))) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(multiply(multiply(inverse(multiply(inverse(sFlat0),sFlat1)),X2),inverse(X2)))),
inference(step,[status(thm)],[t27554,t26528]) ).
cnf(t27556,plain,
multiply(b,inverse(multiply(sFlat0,inverse(a)))) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(sFlat1,inverse(sFlat0)))))),
inference(step,[status(thm)],[t27555,t25417]) ).
cnf(t27557,plain,
multiply(b,inverse(multiply(sFlat0,inverse(a)))) = multiply(multiply(b,inverse(multiply(sFlat0,inverse(a)))),inverse(inverse(multiply(inverse(sFlat0),sFlat1)))),
inference(step,[status(thm)],[t27556,t26528]) ).
cnf(t27558,plain,
multiply(b,inverse(multiply(sFlat0,inverse(a)))) = multiply(inverse(sFlat0),sFlat1),
inference(step,[status(thm)],[t27557,t12981]) ).
cnf(t26636,plain,
multiply(b,inverse(multiply(sFlat0,inverse(a)))) = multiply(inverse(sFlat0),sFlat1),
inference(orient,[status(thm)],[t27558]) ).
cnf(t27584,plain,
multiply(multiply(inverse(sFlat0),sFlat1),inverse(inverse(X1))) = X1,
inference(step,[status(thm)],[t12981,t26636]) ).
cnf(t26692,plain,
multiply(multiply(inverse(sFlat0),sFlat1),inverse(inverse(X1))) = X1,
inference(rw,[status(thm)],[t27584]) ).
cnf(t26851,plain,
multiply(multiply(inverse(sFlat0),sFlat1),inverse(inverse(X1))) = X1,
inference(orient,[status(thm)],[t26692]) ).
cnf(t26621,plain,
multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(sFlat1,inverse(sFlat0)))) = multiply(b,inverse(multiply(sFlat0,inverse(a)))),
inference(cp,[status(thm)],[t25417,t26618]) ).
cnf(t27613,plain,
inverse(multiply(inverse(sFlat0),sFlat1)) = multiply(b,inverse(multiply(sFlat0,inverse(a)))),
inference(step,[status(thm)],[t26621,t26528]) ).
cnf(t27614,plain,
inverse(multiply(inverse(sFlat0),sFlat1)) = multiply(inverse(sFlat0),sFlat1),
inference(step,[status(thm)],[t27613,t26636]) ).
cnf(t26965,plain,
inverse(multiply(inverse(sFlat0),sFlat1)) = multiply(inverse(sFlat0),sFlat1),
inference(orient,[status(thm)],[t27614]) ).
cnf(t26983,plain,
multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(sFlat1,inverse(sFlat0)))) = multiply(multiply(multiply(inverse(sFlat0),sFlat1),X1),inverse(X1)),
inference(cp,[status(thm)],[t25417,t26965]) ).
cnf(t27615,plain,
multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(sFlat1,inverse(sFlat0)))) = multiply(inverse(sFlat0),sFlat1),
inference(step,[status(thm)],[t26528,t26965]) ).
cnf(t26966,plain,
multiply(multiply(inverse(sFlat0),sFlat1),inverse(multiply(sFlat1,inverse(sFlat0)))) = multiply(inverse(sFlat0),sFlat1),
inference(orient,[status(thm)],[t27615]) ).
cnf(t27667,plain,
multiply(inverse(sFlat0),sFlat1) = multiply(multiply(multiply(inverse(sFlat0),sFlat1),X1),inverse(X1)),
inference(step,[status(thm)],[t26983,t26966]) ).
cnf(t27111,plain,
multiply(multiply(multiply(inverse(sFlat0),sFlat1),X1),inverse(X1)) = multiply(inverse(sFlat0),sFlat1),
inference(orient,[status(thm)],[t27667]) ).
cnf(t27113,plain,
multiply(inverse(sFlat0),sFlat1) = multiply(multiply(inverse(sFlat0),sFlat1),inverse(inverse(multiply(sFlat1,inverse(sFlat0))))),
inference(cp,[status(thm)],[t27111,t26966]) ).
cnf(t27668,plain,
multiply(inverse(sFlat0),sFlat1) = multiply(sFlat1,inverse(sFlat0)),
inference(step,[status(thm)],[t27113,t26851]) ).
cnf(t27129,plain,
multiply(inverse(sFlat0),sFlat1) = multiply(sFlat1,inverse(sFlat0)),
inference(orient,[status(thm)],[t27668]) ).
cnf(t27707,plain,
multiply(multiply(sFlat1,inverse(sFlat0)),inverse(inverse(X1))) = X1,
inference(step,[status(thm)],[t26851,t27129]) ).
cnf(t27173,plain,
multiply(multiply(sFlat1,inverse(sFlat0)),inverse(inverse(X1))) = X1,
inference(rw,[status(thm)],[t27707]) ).
cnf(t27215,plain,
multiply(multiply(sFlat1,inverse(sFlat0)),inverse(inverse(X1))) = X1,
inference(orient,[status(thm)],[t27173]) ).
cnf(t15161,plain,
multiply(multiply(inverse(sFlat1),X1),inverse(X1)) = multiply(multiply(inverse(sFlat0),sFlat1),inverse(sFlat0)),
inference(cp,[status(thm)],[t650,t15130]) ).
cnf(t15165,plain,
multiply(multiply(inverse(sFlat1),X1),inverse(X1)) = multiply(multiply(inverse(sFlat0),sFlat1),inverse(sFlat0)),
inference(orient,[status(thm)],[t15161]) ).
cnf(t27673,plain,
multiply(multiply(inverse(sFlat1),X1),inverse(X1)) = multiply(multiply(sFlat1,inverse(sFlat0)),inverse(sFlat0)),
inference(step,[status(thm)],[t15165,t27129]) ).
cnf(t27134,plain,
multiply(multiply(inverse(sFlat1),X1),inverse(X1)) = multiply(multiply(sFlat1,inverse(sFlat0)),inverse(sFlat0)),
inference(orient,[status(thm)],[t27673]) ).
cnf(t27583,plain,
inverse(multiply(inverse(sFlat0),sFlat1)) = multiply(sFlat0,inverse(inverse(inverse(sFlat0)))),
inference(step,[status(thm)],[t14204,t26636]) ).
cnf(t26691,plain,
inverse(multiply(inverse(sFlat0),sFlat1)) = multiply(sFlat0,inverse(inverse(inverse(sFlat0)))),
inference(rw,[status(thm)],[t27583]) ).
cnf(t26710,plain,
multiply(sFlat0,inverse(inverse(inverse(sFlat0)))) = inverse(multiply(inverse(sFlat0),sFlat1)),
inference(orient,[status(thm)],[t26691]) ).
cnf(t26713,plain,
inverse(multiply(inverse(sFlat0),sFlat1)) = multiply(X1,inverse(inverse(inverse(X1)))),
inference(cp,[status(thm)],[t26710,t14566]) ).
cnf(t26748,plain,
multiply(X1,inverse(inverse(inverse(X1)))) = inverse(multiply(inverse(sFlat0),sFlat1)),
inference(orient,[status(thm)],[t26713]) ).
cnf(t27619,plain,
multiply(X1,inverse(inverse(inverse(X1)))) = multiply(inverse(sFlat0),sFlat1),
inference(step,[status(thm)],[t26748,t26965]) ).
cnf(t26970,plain,
multiply(X1,inverse(inverse(inverse(X1)))) = multiply(inverse(sFlat0),sFlat1),
inference(orient,[status(thm)],[t27619]) ).
cnf(t27697,plain,
multiply(X1,inverse(inverse(inverse(X1)))) = multiply(sFlat1,inverse(sFlat0)),
inference(step,[status(thm)],[t26970,t27129]) ).
cnf(t27158,plain,
multiply(X1,inverse(inverse(inverse(X1)))) = multiply(sFlat1,inverse(sFlat0)),
inference(orient,[status(thm)],[t27697]) ).
cnf(t27216,plain,
sFlat0 = multiply(multiply(sFlat1,X1),inverse(X1)),
inference(cp,[status(thm)],[t27215,t650]) ).
cnf(t27233,plain,
multiply(multiply(sFlat1,X1),inverse(X1)) = sFlat0,
inference(orient,[status(thm)],[t27216]) ).
cnf(t27234,plain,
sFlat0 = multiply(multiply(sFlat1,inverse(sFlat0)),inverse(inverse(inverse(inverse(sFlat1))))),
inference(cp,[status(thm)],[t27233,t27158]) ).
cnf(t27724,plain,
sFlat0 = inverse(inverse(sFlat1)),
inference(step,[status(thm)],[t27234,t27215]) ).
cnf(t27249,plain,
inverse(inverse(sFlat1)) = sFlat0,
inference(orient,[status(thm)],[t27724]) ).
cnf(t27258,plain,
multiply(sFlat1,inverse(sFlat0)) = multiply(inverse(sFlat1),inverse(inverse(sFlat0))),
inference(cp,[status(thm)],[t27158,t27249]) ).
cnf(t27329,plain,
multiply(inverse(sFlat1),inverse(inverse(sFlat0))) = multiply(sFlat1,inverse(sFlat0)),
inference(orient,[status(thm)],[t27258]) ).
cnf(t27332,plain,
multiply(multiply(sFlat1,inverse(sFlat0)),inverse(sFlat0)) = multiply(multiply(sFlat1,inverse(sFlat0)),inverse(inverse(inverse(sFlat0)))),
inference(cp,[status(thm)],[t27134,t27329]) ).
cnf(t27255,plain,
inverse(sFlat1) = multiply(multiply(sFlat1,inverse(sFlat0)),inverse(sFlat0)),
inference(cp,[status(thm)],[t27215,t27249]) ).
cnf(t27340,plain,
multiply(multiply(sFlat1,inverse(sFlat0)),inverse(sFlat0)) = inverse(sFlat1),
inference(orient,[status(thm)],[t27255]) ).
cnf(t27727,plain,
inverse(sFlat1) = multiply(multiply(sFlat1,inverse(sFlat0)),inverse(inverse(inverse(sFlat0)))),
inference(step,[status(thm)],[t27332,t27340]) ).
cnf(t27728,plain,
inverse(sFlat1) = inverse(sFlat0),
inference(step,[status(thm)],[t27727,t27215]) ).
cnf(t27353,plain,
inverse(sFlat1) = inverse(sFlat0),
inference(orient,[status(thm)],[t27728]) ).
cnf(t27360,plain,
sFlat1 = multiply(multiply(sFlat1,inverse(sFlat0)),inverse(inverse(sFlat0))),
inference(cp,[status(thm)],[t27215,t27353]) ).
cnf(t27740,plain,
sFlat1 = sFlat0,
inference(step,[status(thm)],[t27360,t27215]) ).
cnf(t27390,plain,
sFlat1 = sFlat0,
inference(orient,[status(thm)],[t27740]) ).
cnf(t27741,plain,
multiply(a,b) = sFlat0,
inference(step,[status(thm)],[t9,t27390]) ).
cnf(t27391,plain,
multiply(a,b) = sFlat0,
inference(orient,[status(thm)],[t27741]) ).
cnf(goal_0,negated_conjecture,
multiply(b,a) != multiply(a,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
sFlat0 != multiply(a,b),
inference(rw,[status(thm)],[goal_0,t13]) ).
cnf(g0_1,plain,
sFlat0 != sFlat0,
inference(rw,[status(thm)],[g0_0,t27391]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP508-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n004.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 14:56:52 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 22.89/3.46 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.89/3.46 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------