FindProof---0.1.UNS-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : FindProof---0.1
% Problem  : GRP506-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300

% Computer : n008.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:12 PM UTC 2026

% Result   : Unsatisfiable 51.15s 6.99s
% Output   : CNFRefutation 51.15s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :  136
%            Number of leaves      :    5
% Syntax   : Number of clauses     :  350 ( 350 unt;   0 nHn; 117 RR)
%            Number of literals    :  350 ( 349 equ;   3 neg)
%            Maximal clause size   :    1 (   1 avg)
%            Maximal term depth    :   14 (   3 avg)
%            Number of predicates  :    2 (   0 usr;   1 prp; 0-2 aty)
%            Number of functors    :    7 (   7 usr;   5 con; 0-2 aty)
%            Number of variables   :  487 (   0 sgn)

% Comments : 
%------------------------------------------------------------------------------
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(t4,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(t9,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(X5,inverse(inverse(X6))),inverse(X4))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(Y6,Y7)),multiply(Y7,Y6))),multiply(inverse(multiply(Y8,Y9)),multiply(Y8,inverse(multiply(X5,inverse(Y9))))))),X6),
    inference(cp,[status(thm)],[t4,t4]) ).

cnf(t33438,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(X5,inverse(inverse(X6))),inverse(X4))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(Y6,Y7)),multiply(Y7,Y6))),multiply(inverse(multiply(Y8,Y9)),multiply(Y8,inverse(multiply(X5,inverse(Y9))))))),X6),
    inference(orient,[status(thm)],[t9]) ).

cnf(t33970,plain,
    X1 = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,X5)),multiply(X4,inverse(multiply(X1,inverse(X5))))))),X6),inverse(X6)),
    inference(cp,[status(thm)],[t4,t33438]) ).

cnf(t60120,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X5,inverse(X4))))))),X6),inverse(X6)) = X5,
    inference(orient,[status(thm)],[t33970]) ).

cnf(t1,axiom,
    sFlat0 = inverse(b2),
    introduced(definition) ).

cnf(t19,plain,
    inverse(b2) = sFlat0,
    inference(orient,[status(thm)],[t1]) ).

cnf(t20,plain,
    X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,X5)),multiply(X4,inverse(multiply(multiply(X1,sFlat0),inverse(X5))))))),b2),
    inference(cp,[status(thm)],[t4,t19]) ).

cnf(t2117,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(X5,sFlat0),inverse(X4))))))),b2) = X5,
    inference(orient,[status(thm)],[t20]) ).

cnf(t34039,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(multiply(X5,sFlat0),inverse(inverse(b2))),inverse(X4))))))) = X5,
    inference(cp,[status(thm)],[t33438,t2117]) ).

cnf(t67595,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(multiply(X5,sFlat0),inverse(sFlat0)),inverse(X4))))))) = X5,
    inference(step,[status(thm)],[t34039,t19]) ).

cnf(t2,axiom,
    sFlat1 = multiply(inverse(b2),b2),
    introduced(definition) ).

cnf(t14,plain,
    multiply(inverse(b2),b2) = sFlat1,
    inference(orient,[status(thm)],[t2]) ).

cnf(t67532,plain,
    multiply(sFlat0,b2) = sFlat1,
    inference(step,[status(thm)],[t14,t19]) ).

cnf(t22,plain,
    multiply(sFlat0,b2) = sFlat1,
    inference(rw,[status(thm)],[t67532]) ).

cnf(t27,plain,
    multiply(sFlat0,b2) = sFlat1,
    inference(orient,[status(thm)],[t22]) ).

cnf(t30,plain,
    X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(X1,inverse(X4)),inverse(b2))))))),X4),
    inference(cp,[status(thm)],[t4,t27]) ).

cnf(t67533,plain,
    X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(X1,inverse(X4)),sFlat0)))))),X4),
    inference(step,[status(thm)],[t30,t19]) ).

cnf(t31,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(X3,inverse(X4)),sFlat0)))))),X4) = X3,
    inference(orient,[status(thm)],[t67533]) ).

cnf(t32,plain,
    X1 = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(X1,inverse(X2)),sFlat0)))))),X2),
    inference(cp,[status(thm)],[t31,t27]) ).

cnf(t48,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(X1,inverse(X2)),sFlat0)))))),X2) = X1,
    inference(orient,[status(thm)],[t32]) ).

cnf(t51,plain,
    X1 = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(X1,sFlat0),sFlat0)))))),b2),
    inference(cp,[status(thm)],[t48,t19]) ).

cnf(t61,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(X1,sFlat0),sFlat0)))))),b2) = X1,
    inference(orient,[status(thm)],[t51]) ).

cnf(t62,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(X1,inverse(sFlat0)),sFlat0)))))) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X1,sFlat0)))))),b2),
    inference(cp,[status(thm)],[t61,t48]) ).

cnf(t2736,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(X1,inverse(sFlat0)),sFlat0)))))) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X1,sFlat0)))))),b2),
    inference(orient,[status(thm)],[t62]) ).

cnf(t2802,plain,
    X1 = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X1,sFlat0)))))),b2),sFlat0),
    inference(cp,[status(thm)],[t48,t2736]) ).

cnf(t2806,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X1,sFlat0)))))),b2),sFlat0) = X1,
    inference(orient,[status(thm)],[t2802]) ).

cnf(t2807,plain,
    multiply(X1,inverse(sFlat0)) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X1,sFlat0)))))),b2),b2),sFlat0),
    inference(cp,[status(thm)],[t2806,t2736]) ).

cnf(t2874,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X1,sFlat0)))))),b2),b2),sFlat0) = multiply(X1,inverse(sFlat0)),
    inference(orient,[status(thm)],[t2807]) ).

cnf(t2875,plain,
    multiply(multiply(X1,inverse(b2)),inverse(sFlat0)) = multiply(multiply(X1,b2),sFlat0),
    inference(cp,[status(thm)],[t2874,t48]) ).

cnf(t67534,plain,
    multiply(multiply(X1,sFlat0),inverse(sFlat0)) = multiply(multiply(X1,b2),sFlat0),
    inference(step,[status(thm)],[t2875,t19]) ).

cnf(t2946,plain,
    multiply(multiply(X1,sFlat0),inverse(sFlat0)) = multiply(multiply(X1,b2),sFlat0),
    inference(orient,[status(thm)],[t67534]) ).

cnf(t67596,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(multiply(X5,b2),sFlat0),inverse(X4))))))) = X5,
    inference(step,[status(thm)],[t67595,t2946]) ).

cnf(t35236,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(multiply(X5,b2),sFlat0),inverse(X4))))))) = X5,
    inference(orient,[status(thm)],[t67596]) ).

cnf(t60123,plain,
    multiply(multiply(X1,b2),sFlat0) = multiply(multiply(X1,X2),inverse(X2)),
    inference(cp,[status(thm)],[t60120,t35236]) ).

cnf(t61283,plain,
    multiply(multiply(X1,X2),inverse(X2)) = multiply(multiply(X1,b2),sFlat0),
    inference(orient,[status(thm)],[t60123]) ).

cnf(t2825,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(X1,inverse(sFlat0)),sFlat0)))))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(X1))))),b2),sFlat0),
    inference(cp,[status(thm)],[t2806,t48]) ).

cnf(t67548,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X1,sFlat0)))))),b2) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(X1))))),b2),sFlat0),
    inference(step,[status(thm)],[t2825,t2736]) ).

cnf(t11864,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X1,sFlat0)))))),b2) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(X1))))),b2),sFlat0),
    inference(orient,[status(thm)],[t67548]) ).

cnf(t11867,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X1,inverse(b2))))))),b2),sFlat0) = X1,
    inference(cp,[status(thm)],[t11864,t48]) ).

cnf(t67553,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X1,sFlat0)))))),b2),sFlat0) = X1,
    inference(step,[status(thm)],[t11867,t19]) ).

cnf(t67554,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(X1))))),b2),sFlat0),sFlat0) = X1,
    inference(step,[status(thm)],[t67553,t11864]) ).

cnf(t11930,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(X1))))),b2),sFlat0),sFlat0) = X1,
    inference(orient,[status(thm)],[t67554]) ).

cnf(t2967,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(X1,sFlat0),sFlat0)))))),b2) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(X1,b2),sFlat0),sFlat0)))))),
    inference(cp,[status(thm)],[t2736,t2946]) ).

cnf(t67535,plain,
    X1 = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(X1,b2),sFlat0),sFlat0)))))),
    inference(step,[status(thm)],[t2967,t61]) ).

cnf(t3019,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(X1,b2),sFlat0),sFlat0)))))) = X1,
    inference(orient,[status(thm)],[t67535]) ).

cnf(t11951,plain,
    multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(X1,b2),sFlat0),sFlat0))))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,X1)))),b2),sFlat0),sFlat0),
    inference(cp,[status(thm)],[t11930,t3019]) ).

cnf(t32488,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,X1)))),b2),sFlat0),sFlat0) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(X1,b2),sFlat0),sFlat0))))),
    inference(orient,[status(thm)],[t11951]) ).

cnf(t67582,plain,
    multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(X1),b2),sFlat0),sFlat0))))) = X1,
    inference(step,[status(thm)],[t11930,t32488]) ).

cnf(t32636,plain,
    multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(X1),b2),sFlat0),sFlat0))))) = X1,
    inference(rw,[status(thm)],[t67582]) ).

cnf(t32637,plain,
    multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(X1),b2),sFlat0),sFlat0))))) = X1,
    inference(orient,[status(thm)],[t32636]) ).

cnf(t35671,plain,
    X1 = inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,sFlat0)),multiply(X4,inverse(multiply(multiply(multiply(X1,b2),b2),sFlat0)))))),
    inference(cp,[status(thm)],[t35236,t2946]) ).

cnf(t39693,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,sFlat0)),multiply(X3,inverse(multiply(multiply(multiply(X4,b2),b2),sFlat0)))))) = X4,
    inference(orient,[status(thm)],[t35671]) ).

cnf(t3,axiom,
    sFlat2 = multiply(multiply(inverse(b2),b2),a2),
    introduced(definition) ).

cnf(t10,plain,
    multiply(multiply(inverse(b2),b2),a2) = sFlat2,
    inference(orient,[status(thm)],[t3]) ).

cnf(t67531,plain,
    multiply(sFlat1,a2) = sFlat2,
    inference(step,[status(thm)],[t10,t14]) ).

cnf(t18,plain,
    multiply(sFlat1,a2) = sFlat2,
    inference(rw,[status(thm)],[t67531]) ).

cnf(t23,plain,
    multiply(sFlat1,a2) = sFlat2,
    inference(orient,[status(thm)],[t18]) ).

cnf(t25,plain,
    X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(X1,inverse(X4)),inverse(X3))))))),X4),
    inference(cp,[status(thm)],[t4,t23]) ).

cnf(t441,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(multiply(X3,inverse(X4)),inverse(X2))))))),X4) = X3,
    inference(orient,[status(thm)],[t25]) ).

cnf(t478,plain,
    X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(X1,sFlat0),inverse(X3))))))),b2),
    inference(cp,[status(thm)],[t441,t19]) ).

cnf(t589,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(multiply(X3,sFlat0),inverse(X2))))))),b2) = X3,
    inference(orient,[status(thm)],[t478]) ).

cnf(t2981,plain,
    X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(multiply(multiply(X1,b2),sFlat0)))))),b2),
    inference(cp,[status(thm)],[t589,t2946]) ).

cnf(t3997,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(multiply(multiply(X2,b2),sFlat0)))))),b2) = X2,
    inference(orient,[status(thm)],[t2981]) ).

cnf(t4042,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X1,sFlat0)))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(X1))))),b2),
    inference(cp,[status(thm)],[t3997,t2806]) ).

cnf(t10759,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(X2))))),b2) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X2,sFlat0)))))),
    inference(orient,[status(thm)],[t4042]) ).

cnf(t10815,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(b2,sFlat0)))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)))),b2),
    inference(cp,[status(thm)],[t10759,t19]) ).

cnf(t10888,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)))),b2) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(b2,sFlat0)))))),
    inference(orient,[status(thm)],[t10815]) ).

cnf(t479,plain,
    X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X2,b2)),multiply(X2,inverse(multiply(multiply(X1,inverse(X3)),sFlat0)))))),X3),
    inference(cp,[status(thm)],[t441,t19]) ).

cnf(t704,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X1,b2)),multiply(X1,inverse(multiply(multiply(X2,inverse(X3)),sFlat0)))))),X3) = X2,
    inference(orient,[status(thm)],[t479]) ).

cnf(t3004,plain,
    multiply(X1,sFlat0) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X2,b2)),multiply(X2,inverse(multiply(multiply(multiply(X1,b2),sFlat0),sFlat0)))))),sFlat0),
    inference(cp,[status(thm)],[t704,t2946]) ).

cnf(t8045,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X1,b2)),multiply(X1,inverse(multiply(multiply(multiply(X2,b2),sFlat0),sFlat0)))))),sFlat0) = multiply(X2,sFlat0),
    inference(orient,[status(thm)],[t3004]) ).

cnf(t8146,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X1,b2)),multiply(X1,inverse(multiply(multiply(multiply(X2,b2),sFlat0),sFlat0)))))) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(X2,sFlat0),sFlat0)))))),b2),
    inference(cp,[status(thm)],[t61,t8045]) ).

cnf(t67545,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X1,b2)),multiply(X1,inverse(multiply(multiply(multiply(X2,b2),sFlat0),sFlat0)))))) = X2,
    inference(step,[status(thm)],[t8146,t61]) ).

cnf(t8198,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X1,b2)),multiply(X1,inverse(multiply(multiply(multiply(X2,b2),sFlat0),sFlat0)))))) = X2,
    inference(orient,[status(thm)],[t67545]) ).

cnf(t8250,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X1,sFlat0)))))) = inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X2,b2)),multiply(X2,inverse(multiply(X1,sFlat0)))))),
    inference(cp,[status(thm)],[t8198,t2806]) ).

cnf(t11480,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X1,b2)),multiply(X1,inverse(multiply(X2,sFlat0)))))) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X2,sFlat0)))))),
    inference(orient,[status(thm)],[t8250]) ).

cnf(t32494,plain,
    multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(b2,b2),sFlat0),sFlat0))))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),sFlat1))),b2),sFlat0),sFlat0),
    inference(cp,[status(thm)],[t32488,t27]) ).

cnf(t33012,plain,
    multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(b2,b2),sFlat0),sFlat0))))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),sFlat1))),b2),sFlat0),sFlat0),
    inference(orient,[status(thm)],[t32494]) ).

cnf(t33047,plain,
    b2 = inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),sFlat1))),b2),sFlat0),sFlat0)),
    inference(cp,[status(thm)],[t3019,t33012]) ).

cnf(t33094,plain,
    inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),sFlat1))),b2),sFlat0),sFlat0)) = b2,
    inference(orient,[status(thm)],[t33047]) ).

cnf(t35742,plain,
    X1 = inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,b2)),multiply(X4,inverse(multiply(multiply(multiply(X1,b2),sFlat0),sFlat0)))))),
    inference(cp,[status(thm)],[t35236,t19]) ).

cnf(t40187,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,b2)),multiply(X3,inverse(multiply(multiply(multiply(X4,b2),sFlat0),sFlat0)))))) = X4,
    inference(orient,[status(thm)],[t35742]) ).

cnf(t40520,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),sFlat1))) = inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,b2)),multiply(X3,b2)))),
    inference(cp,[status(thm)],[t40187,t33094]) ).

cnf(t40702,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,b2)),multiply(X3,b2)))) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),sFlat1))),
    inference(orient,[status(thm)],[t40520]) ).

cnf(t40851,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),sFlat1))) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,b2)),multiply(X1,b2)))),
    inference(cp,[status(thm)],[t40702,t27]) ).

cnf(t41980,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,b2)),multiply(X1,b2)))) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),sFlat1))),
    inference(orient,[status(thm)],[t40851]) ).

cnf(t2973,plain,
    X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,sFlat0)),multiply(X4,inverse(multiply(multiply(X1,b2),sFlat0)))))),b2),
    inference(cp,[status(thm)],[t2117,t2946]) ).

cnf(t6527,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,sFlat0)),multiply(X3,inverse(multiply(multiply(X4,b2),sFlat0)))))),b2) = X4,
    inference(orient,[status(thm)],[t2973]) ).

cnf(t6713,plain,
    sFlat0 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,sFlat0)),multiply(X3,inverse(multiply(sFlat1,sFlat0)))))),b2),
    inference(cp,[status(thm)],[t6527,t27]) ).

cnf(t6770,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,sFlat0)),multiply(X3,inverse(multiply(sFlat1,sFlat0)))))),b2) = sFlat0,
    inference(orient,[status(thm)],[t6713]) ).

cnf(t42011,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),sFlat1))) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,sFlat0)),multiply(X3,inverse(multiply(sFlat1,sFlat0)))))),b2)))),
    inference(cp,[status(thm)],[t41980,t6770]) ).

cnf(t67603,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),sFlat1))) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat0),sFlat0))),
    inference(step,[status(thm)],[t42011,t6770]) ).

cnf(t42207,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),sFlat1))) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat0),sFlat0))),
    inference(orient,[status(thm)],[t67603]) ).

cnf(t67610,plain,
    inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat0),sFlat0))),b2),sFlat0),sFlat0)) = b2,
    inference(step,[status(thm)],[t33094,t42207]) ).

cnf(t42344,plain,
    inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat0),sFlat0))),b2),sFlat0),sFlat0)) = b2,
    inference(rw,[status(thm)],[t67610]) ).

cnf(t42447,plain,
    inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat0),sFlat0))),b2),sFlat0),sFlat0)) = b2,
    inference(orient,[status(thm)],[t42344]) ).

cnf(t40854,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),sFlat1))) = inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),multiply(inverse(multiply(X1,b2)),multiply(X1,b2)))),
    inference(cp,[status(thm)],[t40702,t23]) ).

cnf(t67622,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat0),sFlat0))) = inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),multiply(inverse(multiply(X1,b2)),multiply(X1,b2)))),
    inference(step,[status(thm)],[t40854,t42207]) ).

cnf(t42794,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),multiply(inverse(multiply(X1,b2)),multiply(X1,b2)))) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat0),sFlat0))),
    inference(orient,[status(thm)],[t67622]) ).

cnf(t42838,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat0),sFlat0))) = inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(X1,inverse(b2)),sFlat0)))))),b2)))),
    inference(cp,[status(thm)],[t42794,t48]) ).

cnf(t67625,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat0),sFlat0))) = inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),multiply(inverse(X1),X1))),
    inference(step,[status(thm)],[t42838,t48]) ).

cnf(t43246,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),multiply(inverse(X1),X1))) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat0),sFlat0))),
    inference(orient,[status(thm)],[t67625]) ).

cnf(t43343,plain,
    multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),multiply(inverse(X1),X1)) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat0),sFlat0))),b2),sFlat0),sFlat0))))),
    inference(cp,[status(thm)],[t32637,t43246]) ).

cnf(t67627,plain,
    multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),multiply(inverse(X1),X1)) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat0),sFlat0)),
    inference(step,[status(thm)],[t43343,t32637]) ).

cnf(t43410,plain,
    multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),multiply(inverse(X1),X1)) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat0),sFlat0)),
    inference(orient,[status(thm)],[t67627]) ).

cnf(t43438,plain,
    multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat0),sFlat0)) = multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),multiply(sFlat0,b2)),
    inference(cp,[status(thm)],[t43410,t19]) ).

cnf(t67628,plain,
    multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat0),sFlat0)) = multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1),
    inference(step,[status(thm)],[t43438,t27]) ).

cnf(t43535,plain,
    multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat0),sFlat0)) = multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1),
    inference(orient,[status(thm)],[t67628]) ).

cnf(t67645,plain,
    inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),sFlat0),sFlat0)) = b2,
    inference(step,[status(thm)],[t42447,t43535]) ).

cnf(t43645,plain,
    inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),sFlat0),sFlat0)) = b2,
    inference(rw,[status(thm)],[t67645]) ).

cnf(t43646,plain,
    inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),sFlat0),sFlat0)) = b2,
    inference(orient,[status(thm)],[t43645]) ).

cnf(t43677,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),sFlat0),sFlat0)))))) = inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X1,b2)),multiply(X1,b2)))),
    inference(cp,[status(thm)],[t11480,t43646]) ).

cnf(t67646,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X1,b2)),multiply(X1,b2)))),
    inference(step,[status(thm)],[t43677,t3019]) ).

cnf(t43801,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(multiply(X1,b2)),multiply(X1,b2)))) = inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),
    inference(orient,[status(thm)],[t67646]) ).

cnf(t43830,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,sFlat0)),multiply(X4,inverse(multiply(multiply(X1,b2),sFlat0)))))),b2)))),
    inference(cp,[status(thm)],[t43801,t6527]) ).

cnf(t67649,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(X1),X1))),
    inference(step,[status(thm)],[t43830,t6527]) ).

cnf(t44253,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(inverse(X1),X1))) = inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),
    inference(orient,[status(thm)],[t67649]) ).

cnf(t67650,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(b2,sFlat0)))))),
    inference(step,[status(thm)],[t10888,t44253]) ).

cnf(t44417,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(b2,sFlat0)))))),
    inference(rw,[status(thm)],[t67650]) ).

cnf(t45739,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(b2,sFlat0)))))) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),
    inference(orient,[status(thm)],[t44417]) ).

cnf(t45811,plain,
    multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(multiply(b2,sFlat0)),b2),sFlat0),sFlat0))))) = multiply(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),b2),sFlat0),sFlat0),
    inference(cp,[status(thm)],[t32488,t45739]) ).

cnf(t67664,plain,
    multiply(b2,sFlat0) = multiply(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),b2),sFlat0),sFlat0),
    inference(step,[status(thm)],[t45811,t32637]) ).

cnf(t45879,plain,
    multiply(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),b2),sFlat0),sFlat0) = multiply(b2,sFlat0),
    inference(orient,[status(thm)],[t67664]) ).

cnf(t45990,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),b2),sFlat0) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(b2,sFlat0),inverse(X4))))))),b2),
    inference(cp,[status(thm)],[t2117,t45879]) ).

cnf(t67665,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),b2),sFlat0) = b2,
    inference(step,[status(thm)],[t45990,t2117]) ).

cnf(t46032,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),b2),sFlat0) = b2,
    inference(orient,[status(thm)],[t67665]) ).

cnf(t28,plain,
    X1 = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(X1,inverse(X4)),inverse(X3))))))),X4),
    inference(cp,[status(thm)],[t4,t27]) ).

cnf(t1199,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(multiply(X3,inverse(X4)),inverse(X2))))))),X4) = X3,
    inference(orient,[status(thm)],[t28]) ).

cnf(t1259,plain,
    X1 = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(X1,sFlat0),inverse(X3))))))),b2),
    inference(cp,[status(thm)],[t1199,t19]) ).

cnf(t1321,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(multiply(X3,sFlat0),inverse(X2))))))),b2) = X3,
    inference(orient,[status(thm)],[t1259]) ).

cnf(t2977,plain,
    X1 = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(multiply(multiply(X1,b2),sFlat0)))))),b2),
    inference(cp,[status(thm)],[t1321,t2946]) ).

cnf(t3775,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(multiply(multiply(X2,b2),sFlat0)))))),b2) = X2,
    inference(orient,[status(thm)],[t2977]) ).

cnf(t3820,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X1,sFlat0)))))) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(X1))))),b2),
    inference(cp,[status(thm)],[t3775,t2806]) ).

cnf(t10523,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(X2))))),b2) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X2,sFlat0)))))),
    inference(orient,[status(thm)],[t3820]) ).

cnf(t10579,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(b2,sFlat0)))))) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)))),b2),
    inference(cp,[status(thm)],[t10523,t19]) ).

cnf(t10653,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)))),b2) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(b2,sFlat0)))))),
    inference(orient,[status(thm)],[t10579]) ).

cnf(t67662,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)))),b2) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),
    inference(step,[status(thm)],[t10653,t45739]) ).

cnf(t45740,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)))),b2) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),
    inference(orient,[status(thm)],[t67662]) ).

cnf(t46082,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(b2),multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),b2),sFlat0)))),b2),
    inference(cp,[status(thm)],[t45740,t46032]) ).

cnf(t67666,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(sFlat0,multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),b2),sFlat0)))),b2),
    inference(step,[status(thm)],[t46082,t19]) ).

cnf(t67667,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(sFlat0,b2))),b2),
    inference(step,[status(thm)],[t67666,t46032]) ).

cnf(t67668,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)),b2),
    inference(step,[status(thm)],[t67667,t27]) ).

cnf(t46205,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)),b2),
    inference(orient,[status(thm)],[t67668]) ).

cnf(t67675,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)),b2),b2),sFlat0) = b2,
    inference(step,[status(thm)],[t46032,t46205]) ).

cnf(t46367,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)),b2),b2),sFlat0) = b2,
    inference(rw,[status(thm)],[t67675]) ).

cnf(t46879,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)),b2),b2),sFlat0) = b2,
    inference(orient,[status(thm)],[t46367]) ).

cnf(t46977,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,sFlat0)),multiply(X3,inverse(b2))))),
    inference(cp,[status(thm)],[t39693,t46879]) ).

cnf(t67717,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,sFlat0)),multiply(X3,sFlat0)))),
    inference(step,[status(thm)],[t46977,t19]) ).

cnf(t49281,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,sFlat0)),multiply(X3,sFlat0)))) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)),
    inference(orient,[status(thm)],[t67717]) ).

cnf(t49558,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(b2),multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)),b2),b2),sFlat0)))),
    inference(cp,[status(thm)],[t49281,t46879]) ).

cnf(t67718,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(sFlat0,multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)),b2),b2),sFlat0)))),
    inference(step,[status(thm)],[t49558,t19]) ).

cnf(t67719,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(sFlat0,b2))),
    inference(step,[status(thm)],[t67718,t46879]) ).

cnf(t67720,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),sFlat1)),
    inference(step,[status(thm)],[t67719,t27]) ).

cnf(t49750,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)),
    inference(orient,[status(thm)],[t67720]) ).

cnf(t50092,plain,
    multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),sFlat1) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)),b2),sFlat0),sFlat0))))),
    inference(cp,[status(thm)],[t32637,t49750]) ).

cnf(t67721,plain,
    multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),sFlat1) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1),
    inference(step,[status(thm)],[t50092,t32637]) ).

cnf(t50158,plain,
    multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),sFlat1) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1),
    inference(orient,[status(thm)],[t67721]) ).

cnf(t61353,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),b2),sFlat0) = multiply(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1),inverse(sFlat1)),
    inference(cp,[status(thm)],[t61283,t50158]) ).

cnf(t67746,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),b2),sFlat0) = multiply(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),b2),sFlat0),
    inference(step,[status(thm)],[t61353,t61283]) ).

cnf(t64475,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),b2),sFlat0) = multiply(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),b2),sFlat0),
    inference(orient,[status(thm)],[t67746]) ).

cnf(t64806,plain,
    multiply(inverse(multiply(X1,X2)),multiply(X2,X1)) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),b2),sFlat0),sFlat0))))),
    inference(cp,[status(thm)],[t32637,t64475]) ).

cnf(t67747,plain,
    multiply(inverse(multiply(X1,X2)),multiply(X2,X1)) = multiply(inverse(sFlat1),multiply(b2,sFlat0)),
    inference(step,[status(thm)],[t64806,t32637]) ).

cnf(t64853,plain,
    multiply(inverse(multiply(X1,X2)),multiply(X2,X1)) = multiply(inverse(sFlat1),multiply(b2,sFlat0)),
    inference(orient,[status(thm)],[t67747]) ).

cnf(t65022,plain,
    multiply(multiply(inverse(multiply(X1,X2)),b2),sFlat0) = multiply(multiply(inverse(sFlat1),multiply(b2,sFlat0)),inverse(multiply(X2,X1))),
    inference(cp,[status(thm)],[t61283,t64853]) ).

cnf(t65063,plain,
    multiply(multiply(inverse(sFlat1),multiply(b2,sFlat0)),inverse(multiply(X1,X2))) = multiply(multiply(inverse(multiply(X2,X1)),b2),sFlat0),
    inference(orient,[status(thm)],[t65022]) ).

cnf(t65089,plain,
    multiply(multiply(inverse(multiply(inverse(X1),multiply(X2,X1))),b2),sFlat0) = multiply(multiply(inverse(sFlat1),multiply(b2,sFlat0)),inverse(multiply(multiply(X2,b2),sFlat0))),
    inference(cp,[status(thm)],[t65063,t61283]) ).

cnf(t67752,plain,
    multiply(multiply(inverse(multiply(inverse(X1),multiply(X2,X1))),b2),sFlat0) = multiply(multiply(inverse(multiply(sFlat0,multiply(X2,b2))),b2),sFlat0),
    inference(step,[status(thm)],[t65089,t65063]) ).

cnf(t65285,plain,
    multiply(multiply(inverse(multiply(inverse(X1),multiply(X2,X1))),b2),sFlat0) = multiply(multiply(inverse(multiply(sFlat0,multiply(X2,b2))),b2),sFlat0),
    inference(orient,[status(thm)],[t67752]) ).

cnf(t65422,plain,
    multiply(inverse(X1),multiply(X2,X1)) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(multiply(sFlat0,multiply(X2,b2))),b2),sFlat0),sFlat0))))),
    inference(cp,[status(thm)],[t32637,t65285]) ).

cnf(t67753,plain,
    multiply(inverse(X1),multiply(X2,X1)) = multiply(sFlat0,multiply(X2,b2)),
    inference(step,[status(thm)],[t65422,t32637]) ).

cnf(t65436,plain,
    multiply(inverse(X1),multiply(X2,X1)) = multiply(sFlat0,multiply(X2,b2)),
    inference(orient,[status(thm)],[t67753]) ).

cnf(t65498,plain,
    multiply(multiply(inverse(X1),b2),sFlat0) = multiply(multiply(sFlat0,multiply(X2,b2)),inverse(multiply(X2,X1))),
    inference(cp,[status(thm)],[t61283,t65436]) ).

cnf(t65709,plain,
    multiply(multiply(sFlat0,multiply(X1,b2)),inverse(multiply(X1,X2))) = multiply(multiply(inverse(X2),b2),sFlat0),
    inference(orient,[status(thm)],[t65498]) ).

cnf(t61392,plain,
    multiply(multiply(sFlat1,b2),sFlat0) = multiply(sFlat2,inverse(a2)),
    inference(cp,[status(thm)],[t61283,t23]) ).

cnf(t61649,plain,
    multiply(multiply(sFlat1,b2),sFlat0) = multiply(sFlat2,inverse(a2)),
    inference(orient,[status(thm)],[t61392]) ).

cnf(t65088,plain,
    multiply(multiply(inverse(multiply(sFlat0,multiply(sFlat1,b2))),b2),sFlat0) = multiply(multiply(inverse(sFlat1),multiply(b2,sFlat0)),inverse(multiply(sFlat2,inverse(a2)))),
    inference(cp,[status(thm)],[t65063,t61649]) ).

cnf(t67749,plain,
    multiply(multiply(inverse(multiply(sFlat0,multiply(sFlat1,b2))),b2),sFlat0) = multiply(multiply(inverse(multiply(inverse(a2),sFlat2)),b2),sFlat0),
    inference(step,[status(thm)],[t65088,t65063]) ).

cnf(t65187,plain,
    multiply(multiply(inverse(multiply(sFlat0,multiply(sFlat1,b2))),b2),sFlat0) = multiply(multiply(inverse(multiply(inverse(a2),sFlat2)),b2),sFlat0),
    inference(orient,[status(thm)],[t67749]) ).

cnf(t65228,plain,
    multiply(sFlat0,multiply(sFlat1,b2)) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(multiply(inverse(a2),sFlat2)),b2),sFlat0),sFlat0))))),
    inference(cp,[status(thm)],[t32637,t65187]) ).

cnf(t67750,plain,
    multiply(sFlat0,multiply(sFlat1,b2)) = multiply(inverse(a2),sFlat2),
    inference(step,[status(thm)],[t65228,t32637]) ).

cnf(t65242,plain,
    multiply(sFlat0,multiply(sFlat1,b2)) = multiply(inverse(a2),sFlat2),
    inference(orient,[status(thm)],[t67750]) ).

cnf(t65710,plain,
    multiply(multiply(inverse(X1),b2),sFlat0) = multiply(multiply(inverse(a2),sFlat2),inverse(multiply(sFlat1,X1))),
    inference(cp,[status(thm)],[t65709,t65242]) ).

cnf(t65830,plain,
    multiply(multiply(inverse(a2),sFlat2),inverse(multiply(sFlat1,X1))) = multiply(multiply(inverse(X1),b2),sFlat0),
    inference(orient,[status(thm)],[t65710]) ).

cnf(t29,plain,
    X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(X1,inverse(X4)),inverse(X3))))))),X4),
    inference(cp,[status(thm)],[t4,t27]) ).

cnf(t1626,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(multiply(X3,inverse(X4)),inverse(X2))))))),X4) = X3,
    inference(orient,[status(thm)],[t29]) ).

cnf(t1694,plain,
    X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(X1,sFlat0),inverse(X3))))))),b2),
    inference(cp,[status(thm)],[t1626,t19]) ).

cnf(t1768,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(multiply(X3,sFlat0),inverse(X2))))))),b2) = X3,
    inference(orient,[status(thm)],[t1694]) ).

cnf(t2998,plain,
    multiply(X1,sFlat0) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(multiply(X1,b2),sFlat0),inverse(X3))))))),sFlat0),
    inference(cp,[status(thm)],[t1199,t2946]) ).

cnf(t15363,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(multiply(multiply(X3,b2),sFlat0),inverse(X2))))))),sFlat0) = multiply(X3,sFlat0),
    inference(orient,[status(thm)],[t2998]) ).

cnf(t15447,plain,
    multiply(X1,sFlat0) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(multiply(multiply(multiply(X1,b2),b2),sFlat0)))))),sFlat0),
    inference(cp,[status(thm)],[t15363,t2946]) ).

cnf(t16460,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(multiply(multiply(multiply(X2,b2),b2),sFlat0)))))),sFlat0) = multiply(X2,sFlat0),
    inference(orient,[status(thm)],[t15447]) ).

cnf(t16582,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(multiply(multiply(multiply(X2,b2),b2),sFlat0)))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(X2,sFlat0),inverse(X4))))))),b2),
    inference(cp,[status(thm)],[t1768,t16460]) ).

cnf(t67566,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(multiply(multiply(multiply(X2,b2),b2),sFlat0)))))) = X2,
    inference(step,[status(thm)],[t16582,t1768]) ).

cnf(t16619,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(multiply(multiply(multiply(X2,b2),b2),sFlat0)))))) = X2,
    inference(orient,[status(thm)],[t67566]) ).

cnf(t47003,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(b2))))),
    inference(cp,[status(thm)],[t16619,t46879]) ).

cnf(t67699,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)))),
    inference(step,[status(thm)],[t47003,t19]) ).

cnf(t47371,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)))) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)),
    inference(orient,[status(thm)],[t67699]) ).

cnf(t21,plain,
    X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,b2)),multiply(X4,inverse(multiply(multiply(X1,inverse(X5)),sFlat0)))))),X5),
    inference(cp,[status(thm)],[t4,t19]) ).

cnf(t2484,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,b2)),multiply(X3,inverse(multiply(multiply(X4,inverse(X5)),sFlat0)))))),X5) = X4,
    inference(orient,[status(thm)],[t21]) ).

cnf(t47398,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,b2)),multiply(X4,inverse(multiply(multiply(X1,inverse(sFlat0)),sFlat0)))))),sFlat0)))),
    inference(cp,[status(thm)],[t47371,t2484]) ).

cnf(t67700,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(X1),X1))),
    inference(step,[status(thm)],[t47398,t2484]) ).

cnf(t47574,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(X1),X1))) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)),
    inference(orient,[status(thm)],[t67700]) ).

cnf(t47675,plain,
    multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(X1),X1)) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)),b2),sFlat0),sFlat0))))),
    inference(cp,[status(thm)],[t32637,t47574]) ).

cnf(t67701,plain,
    multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(X1),X1)) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1),
    inference(step,[status(thm)],[t47675,t32637]) ).

cnf(t47741,plain,
    multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(X1),X1)) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1),
    inference(orient,[status(thm)],[t67701]) ).

cnf(t65774,plain,
    multiply(multiply(inverse(multiply(inverse(X1),X1)),b2),sFlat0) = multiply(multiply(sFlat0,multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),b2)),inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1))),
    inference(cp,[status(thm)],[t65709,t47741]) ).

cnf(t67755,plain,
    multiply(multiply(inverse(multiply(inverse(X1),X1)),b2),sFlat0) = multiply(multiply(inverse(sFlat1),b2),sFlat0),
    inference(step,[status(thm)],[t65774,t65709]) ).

cnf(t65847,plain,
    multiply(multiply(inverse(multiply(inverse(X1),X1)),b2),sFlat0) = multiply(multiply(inverse(sFlat1),b2),sFlat0),
    inference(orient,[status(thm)],[t67755]) ).

cnf(t65877,plain,
    multiply(inverse(X1),X1) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(sFlat1),b2),sFlat0),sFlat0))))),
    inference(cp,[status(thm)],[t32637,t65847]) ).

cnf(t67756,plain,
    multiply(inverse(X1),X1) = sFlat1,
    inference(step,[status(thm)],[t65877,t32637]) ).

cnf(t65884,plain,
    multiply(inverse(X1),X1) = sFlat1,
    inference(orient,[status(thm)],[t67756]) ).

cnf(t65897,plain,
    multiply(multiply(inverse(X1),b2),sFlat0) = multiply(sFlat1,inverse(X1)),
    inference(cp,[status(thm)],[t61283,t65884]) ).

cnf(t66005,plain,
    multiply(multiply(inverse(X1),b2),sFlat0) = multiply(sFlat1,inverse(X1)),
    inference(orient,[status(thm)],[t65897]) ).

cnf(t67859,plain,
    multiply(multiply(inverse(a2),sFlat2),inverse(multiply(sFlat1,X1))) = multiply(sFlat1,inverse(X1)),
    inference(step,[status(thm)],[t65830,t66005]) ).

cnf(t66012,plain,
    multiply(multiply(inverse(a2),sFlat2),inverse(multiply(sFlat1,X1))) = multiply(sFlat1,inverse(X1)),
    inference(orient,[status(thm)],[t67859]) ).

cnf(t44281,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),multiply(sFlat0,b2))),
    inference(cp,[status(thm)],[t44253,t19]) ).

cnf(t67651,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),sFlat1)),
    inference(step,[status(thm)],[t44281,t27]) ).

cnf(t44418,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),sFlat1)) = inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),
    inference(orient,[status(thm)],[t67651]) ).

cnf(t44485,plain,
    multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),sFlat1) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),sFlat0),sFlat0))))),
    inference(cp,[status(thm)],[t32637,t44418]) ).

cnf(t67652,plain,
    multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),sFlat1) = multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1),
    inference(step,[status(thm)],[t44485,t32637]) ).

cnf(t44551,plain,
    multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),sFlat1) = multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1),
    inference(orient,[status(thm)],[t67652]) ).

cnf(t46319,plain,
    multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1)),b2),sFlat0),sFlat0))))),
    inference(cp,[status(thm)],[t32637,t46205]) ).

cnf(t67677,plain,
    multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1),
    inference(step,[status(thm)],[t46319,t32637]) ).

cnf(t46369,plain,
    multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1),
    inference(orient,[status(thm)],[t67677]) ).

cnf(t67690,plain,
    multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),sFlat1) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1),
    inference(step,[status(thm)],[t44551,t46369]) ).

cnf(t46382,plain,
    multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),sFlat1) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1),
    inference(orient,[status(thm)],[t67690]) ).

cnf(t61331,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),b2),sFlat0) = multiply(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1),inverse(sFlat1)),
    inference(cp,[status(thm)],[t61283,t46382]) ).

cnf(t67740,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),b2),sFlat0) = multiply(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),b2),sFlat0),
    inference(step,[status(thm)],[t61331,t61283]) ).

cnf(t63335,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(a2,sFlat1)),sFlat2)),b2),sFlat0) = multiply(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),b2),sFlat0),
    inference(orient,[status(thm)],[t67740]) ).

cnf(t63464,plain,
    multiply(inverse(multiply(a2,sFlat1)),sFlat2) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),b2),sFlat0),sFlat0))))),
    inference(cp,[status(thm)],[t32637,t63335]) ).

cnf(t67741,plain,
    multiply(inverse(multiply(a2,sFlat1)),sFlat2) = multiply(inverse(sFlat1),multiply(b2,sFlat0)),
    inference(step,[status(thm)],[t63464,t32637]) ).

cnf(t63523,plain,
    multiply(inverse(multiply(a2,sFlat1)),sFlat2) = multiply(inverse(sFlat1),multiply(b2,sFlat0)),
    inference(orient,[status(thm)],[t67741]) ).

cnf(t65454,plain,
    multiply(sFlat0,multiply(inverse(multiply(a2,sFlat1)),b2)) = multiply(inverse(sFlat2),multiply(inverse(sFlat1),multiply(b2,sFlat0))),
    inference(cp,[status(thm)],[t65436,t63523]) ).

cnf(t65614,plain,
    multiply(inverse(sFlat2),multiply(inverse(sFlat1),multiply(b2,sFlat0))) = multiply(sFlat0,multiply(inverse(multiply(a2,sFlat1)),b2)),
    inference(orient,[status(thm)],[t65454]) ).

cnf(t65885,plain,
    sFlat1 = multiply(inverse(sFlat1),multiply(b2,sFlat0)),
    inference(cp,[status(thm)],[t65884,t64853]) ).

cnf(t65936,plain,
    multiply(inverse(sFlat1),multiply(b2,sFlat0)) = sFlat1,
    inference(orient,[status(thm)],[t65885]) ).

cnf(t67765,plain,
    multiply(inverse(sFlat2),sFlat1) = multiply(sFlat0,multiply(inverse(multiply(a2,sFlat1)),b2)),
    inference(step,[status(thm)],[t65614,t65936]) ).

cnf(t65950,plain,
    multiply(inverse(sFlat2),sFlat1) = multiply(sFlat0,multiply(inverse(multiply(a2,sFlat1)),b2)),
    inference(rw,[status(thm)],[t67765]) ).

cnf(t65898,plain,
    multiply(sFlat0,multiply(inverse(X1),b2)) = multiply(inverse(X1),sFlat1),
    inference(cp,[status(thm)],[t65436,t65884]) ).

cnf(t66021,plain,
    multiply(sFlat0,multiply(inverse(X1),b2)) = multiply(inverse(X1),sFlat1),
    inference(orient,[status(thm)],[t65898]) ).

cnf(t67876,plain,
    multiply(inverse(sFlat2),sFlat1) = multiply(inverse(multiply(a2,sFlat1)),sFlat1),
    inference(step,[status(thm)],[t65950,t66021]) ).

cnf(t66159,plain,
    multiply(inverse(multiply(a2,sFlat1)),sFlat1) = multiply(inverse(sFlat2),sFlat1),
    inference(orient,[status(thm)],[t67876]) ).

cnf(t66160,plain,
    multiply(multiply(inverse(multiply(a2,sFlat1)),b2),sFlat0) = multiply(multiply(inverse(sFlat2),sFlat1),inverse(sFlat1)),
    inference(cp,[status(thm)],[t61283,t66159]) ).

cnf(t67877,plain,
    multiply(sFlat1,inverse(multiply(a2,sFlat1))) = multiply(multiply(inverse(sFlat2),sFlat1),inverse(sFlat1)),
    inference(step,[status(thm)],[t66160,t66005]) ).

cnf(t67878,plain,
    multiply(sFlat1,inverse(multiply(a2,sFlat1))) = multiply(multiply(inverse(sFlat2),b2),sFlat0),
    inference(step,[status(thm)],[t67877,t61283]) ).

cnf(t67879,plain,
    multiply(sFlat1,inverse(multiply(a2,sFlat1))) = multiply(sFlat1,inverse(sFlat2)),
    inference(step,[status(thm)],[t67878,t66005]) ).

cnf(t66164,plain,
    multiply(sFlat1,inverse(multiply(a2,sFlat1))) = multiply(sFlat1,inverse(sFlat2)),
    inference(orient,[status(thm)],[t67879]) ).

cnf(t66167,plain,
    multiply(sFlat1,inverse(inverse(multiply(a2,sFlat1)))) = multiply(multiply(inverse(a2),sFlat2),inverse(multiply(sFlat1,inverse(sFlat2)))),
    inference(cp,[status(thm)],[t66012,t66164]) ).

cnf(t67880,plain,
    multiply(sFlat1,inverse(inverse(multiply(a2,sFlat1)))) = multiply(sFlat1,inverse(inverse(sFlat2))),
    inference(step,[status(thm)],[t66167,t66012]) ).

cnf(t66169,plain,
    multiply(sFlat1,inverse(inverse(multiply(a2,sFlat1)))) = multiply(sFlat1,inverse(inverse(sFlat2))),
    inference(orient,[status(thm)],[t67880]) ).

cnf(t67734,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X5,inverse(X4))))))),b2),sFlat0) = X5,
    inference(step,[status(thm)],[t60120,t61283]) ).

cnf(t61648,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X5,inverse(X4))))))),b2),sFlat0) = X5,
    inference(rw,[status(thm)],[t67734]) ).

cnf(t67930,plain,
    multiply(sFlat1,inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X5,inverse(X4)))))))) = X5,
    inference(step,[status(thm)],[t61648,t66005]) ).

cnf(t67763,plain,
    multiply(inverse(multiply(X1,X2)),multiply(X2,X1)) = sFlat1,
    inference(step,[status(thm)],[t64853,t65936]) ).

cnf(t65943,plain,
    multiply(inverse(multiply(X1,X2)),multiply(X2,X1)) = sFlat1,
    inference(orient,[status(thm)],[t67763]) ).

cnf(t67931,plain,
    multiply(sFlat1,inverse(multiply(inverse(sFlat1),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X5,inverse(X4)))))))) = X5,
    inference(step,[status(thm)],[t67930,t65943]) ).

cnf(t67855,plain,
    multiply(multiply(sFlat0,multiply(X1,b2)),inverse(multiply(X1,X2))) = multiply(sFlat1,inverse(X2)),
    inference(step,[status(thm)],[t65709,t66005]) ).

cnf(t66008,plain,
    multiply(multiply(sFlat0,multiply(X1,b2)),inverse(multiply(X1,X2))) = multiply(sFlat1,inverse(X2)),
    inference(orient,[status(thm)],[t67855]) ).

cnf(t66027,plain,
    multiply(sFlat1,inverse(X1)) = multiply(multiply(inverse(X2),sFlat1),inverse(multiply(inverse(X2),X1))),
    inference(cp,[status(thm)],[t66008,t66021]) ).

cnf(t66751,plain,
    multiply(multiply(inverse(X1),sFlat1),inverse(multiply(inverse(X1),X2))) = multiply(sFlat1,inverse(X2)),
    inference(orient,[status(thm)],[t66027]) ).

cnf(t66752,plain,
    multiply(sFlat1,inverse(X1)) = multiply(sFlat1,inverse(multiply(inverse(sFlat1),X1))),
    inference(cp,[status(thm)],[t66751,t65884]) ).

cnf(t66798,plain,
    multiply(sFlat1,inverse(multiply(inverse(sFlat1),X1))) = multiply(sFlat1,inverse(X1)),
    inference(orient,[status(thm)],[t66752]) ).

cnf(t67932,plain,
    multiply(sFlat1,inverse(multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X5,inverse(X4))))))) = X5,
    inference(step,[status(thm)],[t67931,t66798]) ).

cnf(t67069,plain,
    multiply(sFlat1,inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(X3,inverse(X2))))))) = X3,
    inference(orient,[status(thm)],[t67932]) ).

cnf(t1695,plain,
    X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(multiply(X2,b2)),multiply(X2,inverse(multiply(multiply(X1,inverse(X3)),sFlat0)))))),X3),
    inference(cp,[status(thm)],[t1626,t19]) ).

cnf(t1963,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(multiply(X1,b2)),multiply(X1,inverse(multiply(multiply(X2,inverse(X3)),sFlat0)))))),X3) = X2,
    inference(orient,[status(thm)],[t1695]) ).

cnf(t2993,plain,
    multiply(X1,sFlat0) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(multiply(X2,b2)),multiply(X2,inverse(multiply(multiply(multiply(X1,b2),sFlat0),sFlat0)))))),sFlat0),
    inference(cp,[status(thm)],[t1963,t2946]) ).

cnf(t7247,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(multiply(X1,b2)),multiply(X1,inverse(multiply(multiply(multiply(X2,b2),sFlat0),sFlat0)))))),sFlat0) = multiply(X2,sFlat0),
    inference(orient,[status(thm)],[t2993]) ).

cnf(t7348,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(multiply(X1,b2)),multiply(X1,inverse(multiply(multiply(multiply(X2,b2),sFlat0),sFlat0)))))) = multiply(inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(X2,sFlat0),sFlat0)))))),b2),
    inference(cp,[status(thm)],[t61,t7247]) ).

cnf(t67543,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(multiply(X1,b2)),multiply(X1,inverse(multiply(multiply(multiply(X2,b2),sFlat0),sFlat0)))))) = X2,
    inference(step,[status(thm)],[t7348,t61]) ).

cnf(t7400,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(multiply(X1,b2)),multiply(X1,inverse(multiply(multiply(multiply(X2,b2),sFlat0),sFlat0)))))) = X2,
    inference(orient,[status(thm)],[t67543]) ).

cnf(t7452,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X1,sFlat0)))))) = inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(multiply(X2,b2)),multiply(X2,inverse(multiply(X1,sFlat0)))))),
    inference(cp,[status(thm)],[t7400,t2806]) ).

cnf(t11225,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(multiply(X1,b2)),multiply(X1,inverse(multiply(X2,sFlat0)))))) = inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(X2,sFlat0)))))),
    inference(orient,[status(thm)],[t7452]) ).

cnf(t43678,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),sFlat0),sFlat0)))))) = inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(multiply(X1,b2)),multiply(X1,b2)))),
    inference(cp,[status(thm)],[t11225,t43646]) ).

cnf(t67654,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(multiply(X1,b2)),multiply(X1,b2)))),
    inference(step,[status(thm)],[t43678,t3019]) ).

cnf(t44769,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(multiply(X1,b2)),multiply(X1,b2)))) = inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),
    inference(orient,[status(thm)],[t67654]) ).

cnf(t44797,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,sFlat0)),multiply(X4,inverse(multiply(multiply(X1,b2),sFlat0)))))),b2)))),
    inference(cp,[status(thm)],[t44769,t6527]) ).

cnf(t67657,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(X1),X1))),
    inference(step,[status(thm)],[t44797,t6527]) ).

cnf(t45221,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(inverse(X1),X1))) = inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),
    inference(orient,[status(thm)],[t67657]) ).

cnf(t45249,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),multiply(sFlat0,b2))),
    inference(cp,[status(thm)],[t45221,t19]) ).

cnf(t67659,plain,
    inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)) = inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),sFlat1)),
    inference(step,[status(thm)],[t45249,t27]) ).

cnf(t45387,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),sFlat1)) = inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),
    inference(orient,[status(thm)],[t67659]) ).

cnf(t45455,plain,
    multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),sFlat1) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1)),b2),sFlat0),sFlat0))))),
    inference(cp,[status(thm)],[t32637,t45387]) ).

cnf(t67660,plain,
    multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),sFlat1) = multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1),
    inference(step,[status(thm)],[t45455,t32637]) ).

cnf(t45521,plain,
    multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),sFlat1) = multiply(inverse(multiply(inverse(sFlat2),multiply(a2,sFlat1))),sFlat1),
    inference(orient,[status(thm)],[t67660]) ).

cnf(t67694,plain,
    multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),sFlat1) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1),
    inference(step,[status(thm)],[t45521,t46369]) ).

cnf(t46386,plain,
    multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),sFlat1) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1),
    inference(orient,[status(thm)],[t67694]) ).

cnf(t61362,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),b2),sFlat0) = multiply(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),sFlat1),inverse(sFlat1)),
    inference(cp,[status(thm)],[t61283,t46386]) ).

cnf(t67744,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),b2),sFlat0) = multiply(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),b2),sFlat0),
    inference(step,[status(thm)],[t61362,t61283]) ).

cnf(t64122,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(b2,sFlat0)),sFlat1)),b2),sFlat0) = multiply(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),b2),sFlat0),
    inference(orient,[status(thm)],[t67744]) ).

cnf(t64231,plain,
    multiply(inverse(multiply(b2,sFlat0)),sFlat1) = multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),multiply(inverse(sFlat1),multiply(sFlat0,inverse(multiply(multiply(multiply(inverse(multiply(inverse(sFlat1),multiply(b2,sFlat0))),b2),sFlat0),sFlat0))))),
    inference(cp,[status(thm)],[t32637,t64122]) ).

cnf(t67745,plain,
    multiply(inverse(multiply(b2,sFlat0)),sFlat1) = multiply(inverse(sFlat1),multiply(b2,sFlat0)),
    inference(step,[status(thm)],[t64231,t32637]) ).

cnf(t64282,plain,
    multiply(inverse(multiply(b2,sFlat0)),sFlat1) = multiply(inverse(sFlat1),multiply(b2,sFlat0)),
    inference(orient,[status(thm)],[t67745]) ).

cnf(t67761,plain,
    multiply(inverse(multiply(b2,sFlat0)),sFlat1) = sFlat1,
    inference(step,[status(thm)],[t64282,t65936]) ).

cnf(t65941,plain,
    multiply(inverse(multiply(b2,sFlat0)),sFlat1) = sFlat1,
    inference(orient,[status(thm)],[t67761]) ).

cnf(t67122,plain,
    X1 = multiply(sFlat1,inverse(multiply(inverse(sFlat1),multiply(inverse(multiply(b2,sFlat0)),inverse(multiply(X1,inverse(sFlat1))))))),
    inference(cp,[status(thm)],[t67069,t65941]) ).

cnf(t67933,plain,
    X1 = multiply(sFlat1,inverse(multiply(inverse(multiply(b2,sFlat0)),inverse(multiply(X1,inverse(sFlat1)))))),
    inference(step,[status(thm)],[t67122,t66798]) ).

cnf(t66764,plain,
    multiply(sFlat1,inverse(X1)) = multiply(sFlat1,inverse(multiply(inverse(multiply(b2,sFlat0)),X1))),
    inference(cp,[status(thm)],[t66751,t65941]) ).

cnf(t66915,plain,
    multiply(sFlat1,inverse(multiply(inverse(multiply(b2,sFlat0)),X1))) = multiply(sFlat1,inverse(X1)),
    inference(orient,[status(thm)],[t66764]) ).

cnf(t67934,plain,
    X1 = multiply(sFlat1,inverse(inverse(multiply(X1,inverse(sFlat1))))),
    inference(step,[status(thm)],[t67933,t66915]) ).

cnf(t67768,plain,
    multiply(sFlat1,inverse(multiply(X1,X2))) = multiply(multiply(inverse(multiply(X2,X1)),b2),sFlat0),
    inference(step,[status(thm)],[t65063,t65936]) ).

cnf(t65952,plain,
    multiply(sFlat1,inverse(multiply(X1,X2))) = multiply(multiply(inverse(multiply(X2,X1)),b2),sFlat0),
    inference(rw,[status(thm)],[t67768]) ).

cnf(t67885,plain,
    multiply(sFlat1,inverse(multiply(X1,X2))) = multiply(sFlat1,inverse(multiply(X2,X1))),
    inference(step,[status(thm)],[t65952,t66005]) ).

cnf(t66233,plain,
    multiply(sFlat1,inverse(multiply(X1,X2))) = multiply(sFlat1,inverse(multiply(X2,X1))),
    inference(orient,[status(thm)],[t67885]) ).

cnf(t66800,plain,
    multiply(sFlat1,inverse(X1)) = multiply(sFlat1,inverse(multiply(X1,inverse(sFlat1)))),
    inference(cp,[status(thm)],[t66798,t66233]) ).

cnf(t66829,plain,
    multiply(sFlat1,inverse(multiply(X1,inverse(sFlat1)))) = multiply(sFlat1,inverse(X1)),
    inference(orient,[status(thm)],[t66800]) ).

cnf(t66835,plain,
    multiply(sFlat1,inverse(inverse(multiply(X1,inverse(sFlat1))))) = multiply(multiply(inverse(a2),sFlat2),inverse(multiply(sFlat1,inverse(X1)))),
    inference(cp,[status(thm)],[t66012,t66829]) ).

cnf(t67914,plain,
    multiply(sFlat1,inverse(inverse(multiply(X1,inverse(sFlat1))))) = multiply(sFlat1,inverse(inverse(X1))),
    inference(step,[status(thm)],[t66835,t66012]) ).

cnf(t66877,plain,
    multiply(sFlat1,inverse(inverse(multiply(X1,inverse(sFlat1))))) = multiply(sFlat1,inverse(inverse(X1))),
    inference(orient,[status(thm)],[t67914]) ).

cnf(t67935,plain,
    X1 = multiply(sFlat1,inverse(inverse(X1))),
    inference(step,[status(thm)],[t67934,t66877]) ).

cnf(t67261,plain,
    multiply(sFlat1,inverse(inverse(X1))) = X1,
    inference(orient,[status(thm)],[t67935]) ).

cnf(t67940,plain,
    multiply(a2,sFlat1) = multiply(sFlat1,inverse(inverse(sFlat2))),
    inference(step,[status(thm)],[t66169,t67261]) ).

cnf(t67941,plain,
    multiply(a2,sFlat1) = sFlat2,
    inference(step,[status(thm)],[t67940,t67261]) ).

cnf(t67279,plain,
    multiply(a2,sFlat1) = sFlat2,
    inference(rw,[status(thm)],[t67941]) ).

cnf(t67295,plain,
    multiply(a2,sFlat1) = sFlat2,
    inference(orient,[status(thm)],[t67279]) ).

cnf(t67950,plain,
    multiply(X1,inverse(sFlat1)) = multiply(sFlat1,inverse(inverse(X1))),
    inference(step,[status(thm)],[t66877,t67261]) ).

cnf(t67951,plain,
    multiply(X1,inverse(sFlat1)) = X1,
    inference(step,[status(thm)],[t67950,t67261]) ).

cnf(t67284,plain,
    multiply(X1,inverse(sFlat1)) = X1,
    inference(rw,[status(thm)],[t67951]) ).

cnf(t65901,plain,
    multiply(inverse(sFlat1),multiply(b2,sFlat0)) = multiply(inverse(sFlat1),multiply(X1,inverse(X1))),
    inference(cp,[status(thm)],[t64853,t65884]) ).

cnf(t67873,plain,
    sFlat1 = multiply(inverse(sFlat1),multiply(X1,inverse(X1))),
    inference(step,[status(thm)],[t65901,t65936]) ).

cnf(t66126,plain,
    multiply(inverse(sFlat1),multiply(X1,inverse(X1))) = sFlat1,
    inference(orient,[status(thm)],[t67873]) ).

cnf(t66128,plain,
    multiply(multiply(inverse(sFlat1),b2),sFlat0) = multiply(sFlat1,inverse(multiply(X1,inverse(X1)))),
    inference(cp,[status(thm)],[t61283,t66126]) ).

cnf(t67875,plain,
    multiply(sFlat1,inverse(sFlat1)) = multiply(sFlat1,inverse(multiply(X1,inverse(X1)))),
    inference(step,[status(thm)],[t66128,t66005]) ).

cnf(t66138,plain,
    multiply(sFlat1,inverse(multiply(X1,inverse(X1)))) = multiply(sFlat1,inverse(sFlat1)),
    inference(orient,[status(thm)],[t67875]) ).

cnf(t66142,plain,
    multiply(sFlat1,inverse(inverse(multiply(X1,inverse(X1))))) = multiply(multiply(inverse(a2),sFlat2),inverse(multiply(sFlat1,inverse(sFlat1)))),
    inference(cp,[status(thm)],[t66012,t66138]) ).

cnf(t67881,plain,
    multiply(sFlat1,inverse(inverse(multiply(X1,inverse(X1))))) = multiply(sFlat1,inverse(inverse(sFlat1))),
    inference(step,[status(thm)],[t66142,t66012]) ).

cnf(t66198,plain,
    multiply(sFlat1,inverse(inverse(multiply(X1,inverse(X1))))) = multiply(sFlat1,inverse(inverse(sFlat1))),
    inference(orient,[status(thm)],[t67881]) ).

cnf(t67944,plain,
    multiply(X1,inverse(X1)) = multiply(sFlat1,inverse(inverse(sFlat1))),
    inference(step,[status(thm)],[t66198,t67261]) ).

cnf(t67945,plain,
    multiply(X1,inverse(X1)) = sFlat1,
    inference(step,[status(thm)],[t67944,t67261]) ).

cnf(t67281,plain,
    multiply(X1,inverse(X1)) = sFlat1,
    inference(rw,[status(thm)],[t67945]) ).

cnf(t67405,plain,
    multiply(X1,inverse(X1)) = sFlat1,
    inference(orient,[status(thm)],[t67281]) ).

cnf(t67415,plain,
    multiply(sFlat1,inverse(inverse(inverse(sFlat1)))) = multiply(sFlat1,inverse(sFlat1)),
    inference(cp,[status(thm)],[t66798,t67405]) ).

cnf(t67998,plain,
    inverse(sFlat1) = multiply(sFlat1,inverse(sFlat1)),
    inference(step,[status(thm)],[t67415,t67261]) ).

cnf(t67272,plain,
    sFlat1 = multiply(sFlat1,inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X2))))),
    inference(cp,[status(thm)],[t67069,t67261]) ).

cnf(t67975,plain,
    sFlat1 = multiply(sFlat1,inverse(multiply(multiply(X1,inverse(X2)),inverse(multiply(X1,inverse(X2)))))),
    inference(step,[status(thm)],[t67272,t66233]) ).

cnf(t67976,plain,
    sFlat1 = multiply(sFlat1,inverse(sFlat1)),
    inference(step,[status(thm)],[t67975,t66138]) ).

cnf(t67376,plain,
    multiply(sFlat1,inverse(sFlat1)) = sFlat1,
    inference(orient,[status(thm)],[t67976]) ).

cnf(t67999,plain,
    inverse(sFlat1) = sFlat1,
    inference(step,[status(thm)],[t67998,t67376]) ).

cnf(t67427,plain,
    inverse(sFlat1) = sFlat1,
    inference(orient,[status(thm)],[t67999]) ).

cnf(t68062,plain,
    multiply(X1,sFlat1) = X1,
    inference(step,[status(thm)],[t67284,t67427]) ).

cnf(t67499,plain,
    multiply(X1,sFlat1) = X1,
    inference(orient,[status(thm)],[t68062]) ).

cnf(t68071,plain,
    a2 = sFlat2,
    inference(step,[status(thm)],[t67295,t67499]) ).

cnf(t67515,plain,
    a2 = sFlat2,
    inference(rw,[status(thm)],[t68071]) ).

cnf(t67525,plain,
    a2 = sFlat2,
    inference(orient,[status(thm)],[t67515]) ).

cnf(goal_0,negated_conjecture,
    multiply(multiply(inverse(b2),b2),a2) != a2,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(g0_0,plain,
    multiply(multiply(inverse(b2),b2),a2) != sFlat2,
    inference(rw,[status(thm)],[goal_0]) ).

cnf(g0_1,plain,
    sFlat2 != sFlat2,
    inference(rw,[status(thm)],[g0_0,t67525]) ).

cnf(contradiction_0,plain,
    $false,
    inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP506-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04  % Command  : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.12/0.38  % Computer : n008.cluster.edu
% 0.12/0.38  % Model    : x86_64 x86_64
% 0.12/0.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38  % Memory   : 8046.5625MB
% 0.12/0.38  % OS       : Linux 6.8.0-71-generic
% 0.12/0.38  % CPULimit : 300
% 0.12/0.38  % WCLimit  : 300
% 0.12/0.38  % DateTime : Wed Sep 23 14:57:10 UTC 2026
% 0.12/0.38  % CPUTime  : 
% 0.12/0.38  Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 51.15/6.99  % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 51.15/6.99  % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------