%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP024-5 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n019.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:24:57 PM UTC 2026
% Result : Unsatisfiable 39.04s 5.87s
% Output : CNFRefutation 39.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 151
% Number of leaves : 6
% Syntax : Number of clauses : 539 ( 539 unt; 0 nHn; 5 RR)
% Number of literals : 539 ( 538 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 1421 ( 66 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t3,axiom,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t6,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t3]) ).
cnf(t1,axiom,
multiply(inverse(X1),X1) = identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t7,plain,
multiply(inverse(X1),X1) = identity,
inference(orient,[status(thm)],[t1]) ).
cnf(t8,plain,
multiply(inverse(X1),multiply(X1,X2)) = multiply(identity,X2),
inference(cp,[status(thm)],[t6,t7]) ).
cnf(t0,axiom,
multiply(identity,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t5,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t110650,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(step,[status(thm)],[t8,t5]) ).
cnf(t17,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(orient,[status(thm)],[t110650]) ).
cnf(t4,axiom,
multiply(inverse(X1),multiply(inverse(X2),multiply(X1,X2))) = commutator(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t9,plain,
multiply(inverse(X1),multiply(inverse(X2),multiply(X1,X2))) = commutator(X1,X2),
inference(orient,[status(thm)],[t4]) ).
cnf(t19,plain,
X1 = multiply(inverse(inverse(X1)),identity),
inference(cp,[status(thm)],[t17,t7]) ).
cnf(t36,plain,
multiply(inverse(inverse(X1)),identity) = X1,
inference(orient,[status(thm)],[t19]) ).
cnf(t23,plain,
multiply(X1,X2) = multiply(inverse(inverse(X1)),X2),
inference(cp,[status(thm)],[t17,t17]) ).
cnf(t50,plain,
multiply(inverse(inverse(X1)),X2) = multiply(X1,X2),
inference(orient,[status(thm)],[t23]) ).
cnf(t110655,plain,
multiply(X1,identity) = X1,
inference(step,[status(thm)],[t36,t50]) ).
cnf(t56,plain,
multiply(X1,identity) = X1,
inference(rw,[status(thm)],[t110655]) ).
cnf(t57,plain,
multiply(X1,identity) = X1,
inference(orient,[status(thm)],[t56]) ).
cnf(t58,plain,
inverse(inverse(X1)) = multiply(X1,identity),
inference(cp,[status(thm)],[t57,t50]) ).
cnf(t110656,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t58,t57]) ).
cnf(t59,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t110656]) ).
cnf(t62,plain,
identity = multiply(X1,inverse(X1)),
inference(cp,[status(thm)],[t7,t59]) ).
cnf(t68,plain,
multiply(X1,inverse(X1)) = identity,
inference(orient,[status(thm)],[t62]) ).
cnf(t69,plain,
identity = multiply(X1,multiply(X2,inverse(multiply(X1,X2)))),
inference(cp,[status(thm)],[t68,t6]) ).
cnf(t90,plain,
multiply(X1,multiply(X2,inverse(multiply(X1,X2)))) = identity,
inference(orient,[status(thm)],[t69]) ).
cnf(t96,plain,
multiply(X1,inverse(multiply(X2,X1))) = multiply(inverse(X2),identity),
inference(cp,[status(thm)],[t17,t90]) ).
cnf(t110659,plain,
multiply(X1,inverse(multiply(X2,X1))) = inverse(X2),
inference(step,[status(thm)],[t96,t57]) ).
cnf(t99,plain,
multiply(X1,inverse(multiply(X2,X1))) = inverse(X2),
inference(orient,[status(thm)],[t110659]) ).
cnf(t104,plain,
inverse(multiply(X1,X2)) = multiply(inverse(X2),inverse(X1)),
inference(cp,[status(thm)],[t17,t99]) ).
cnf(t108,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t104]) ).
cnf(t111,plain,
multiply(inverse(X1),multiply(inverse(X2),X3)) = multiply(inverse(multiply(X2,X1)),X3),
inference(cp,[status(thm)],[t6,t108]) ).
cnf(t166,plain,
multiply(inverse(X1),multiply(inverse(X2),X3)) = multiply(inverse(multiply(X2,X1)),X3),
inference(orient,[status(thm)],[t111]) ).
cnf(t110663,plain,
multiply(inverse(multiply(X2,X1)),multiply(X1,X2)) = commutator(X1,X2),
inference(step,[status(thm)],[t9,t166]) ).
cnf(t173,plain,
multiply(inverse(multiply(X2,X1)),multiply(X1,X2)) = commutator(X1,X2),
inference(rw,[status(thm)],[t110663]) ).
cnf(t174,plain,
multiply(inverse(multiply(X1,X2)),multiply(X2,X1)) = commutator(X2,X1),
inference(orient,[status(thm)],[t173]) ).
cnf(t193,plain,
multiply(X1,X2) = multiply(inverse(inverse(multiply(X2,X1))),commutator(X1,X2)),
inference(cp,[status(thm)],[t17,t174]) ).
cnf(t110691,plain,
multiply(X1,X2) = multiply(multiply(X2,X1),commutator(X1,X2)),
inference(step,[status(thm)],[t193,t50]) ).
cnf(t110692,plain,
multiply(X1,X2) = multiply(X2,multiply(X1,commutator(X1,X2))),
inference(step,[status(thm)],[t110691,t6]) ).
cnf(t556,plain,
multiply(X1,multiply(X2,commutator(X2,X1))) = multiply(X2,X1),
inference(orient,[status(thm)],[t110692]) ).
cnf(t2,axiom,
commutator(commutator(X1,X2),X3) = commutator(X1,commutator(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t15,plain,
commutator(commutator(X1,X2),X3) = commutator(X1,commutator(X2,X3)),
inference(orient,[status(thm)],[t2]) ).
cnf(t24,plain,
commutator(X1,X1) = multiply(inverse(X1),X1),
inference(cp,[status(thm)],[t9,t17]) ).
cnf(t110651,plain,
commutator(X1,X1) = identity,
inference(step,[status(thm)],[t24,t7]) ).
cnf(t26,plain,
commutator(X1,X1) = identity,
inference(orient,[status(thm)],[t110651]) ).
cnf(t28,plain,
commutator(X1,commutator(X1,X2)) = commutator(identity,X2),
inference(cp,[status(thm)],[t15,t26]) ).
cnf(t11,plain,
commutator(identity,X1) = multiply(inverse(identity),multiply(inverse(X1),X1)),
inference(cp,[status(thm)],[t9,t5]) ).
cnf(t110648,plain,
commutator(identity,X1) = multiply(inverse(identity),identity),
inference(step,[status(thm)],[t11,t7]) ).
cnf(t110649,plain,
commutator(identity,X1) = identity,
inference(step,[status(thm)],[t110648,t7]) ).
cnf(t16,plain,
commutator(identity,X1) = identity,
inference(orient,[status(thm)],[t110649]) ).
cnf(t110654,plain,
commutator(X1,commutator(X1,X2)) = identity,
inference(step,[status(thm)],[t28,t16]) ).
cnf(t40,plain,
commutator(X1,commutator(X1,X2)) = identity,
inference(orient,[status(thm)],[t110654]) ).
cnf(t61,plain,
X1 = multiply(X2,multiply(inverse(X2),X1)),
inference(cp,[status(thm)],[t17,t59]) ).
cnf(t74,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t61]) ).
cnf(t178,plain,
commutator(multiply(inverse(X1),X2),X1) = multiply(inverse(X2),multiply(multiply(inverse(X1),X2),X1)),
inference(cp,[status(thm)],[t174,t74]) ).
cnf(t110671,plain,
commutator(multiply(inverse(X1),X2),X1) = multiply(inverse(X2),multiply(inverse(X1),multiply(X2,X1))),
inference(step,[status(thm)],[t178,t6]) ).
cnf(t110672,plain,
commutator(multiply(inverse(X1),X2),X1) = multiply(inverse(multiply(X1,X2)),multiply(X2,X1)),
inference(step,[status(thm)],[t110671,t166]) ).
cnf(t110673,plain,
commutator(multiply(inverse(X1),X2),X1) = commutator(X2,X1),
inference(step,[status(thm)],[t110672,t174]) ).
cnf(t239,plain,
commutator(multiply(inverse(X1),X2),X1) = commutator(X2,X1),
inference(orient,[status(thm)],[t110673]) ).
cnf(t241,plain,
commutator(multiply(X1,X2),X1) = commutator(X2,X1),
inference(cp,[status(thm)],[t239,t17]) ).
cnf(t257,plain,
commutator(multiply(X1,X2),X1) = commutator(X2,X1),
inference(orient,[status(thm)],[t241]) ).
cnf(t267,plain,
identity = commutator(multiply(X1,X2),commutator(X2,X1)),
inference(cp,[status(thm)],[t40,t257]) ).
cnf(t351,plain,
commutator(multiply(X1,X2),commutator(X2,X1)) = identity,
inference(orient,[status(thm)],[t267]) ).
cnf(t573,plain,
multiply(multiply(X1,X2),commutator(X2,X1)) = multiply(commutator(X2,X1),multiply(multiply(X1,X2),identity)),
inference(cp,[status(thm)],[t556,t351]) ).
cnf(t110695,plain,
multiply(X1,multiply(X2,commutator(X2,X1))) = multiply(commutator(X2,X1),multiply(multiply(X1,X2),identity)),
inference(step,[status(thm)],[t573,t6]) ).
cnf(t110696,plain,
multiply(X2,X1) = multiply(commutator(X2,X1),multiply(multiply(X1,X2),identity)),
inference(step,[status(thm)],[t110695,t556]) ).
cnf(t110697,plain,
multiply(X2,X1) = multiply(commutator(X2,X1),multiply(X1,multiply(X2,identity))),
inference(step,[status(thm)],[t110696,t6]) ).
cnf(t110698,plain,
multiply(X2,X1) = multiply(commutator(X2,X1),multiply(X1,X2)),
inference(step,[status(thm)],[t110697,t57]) ).
cnf(t659,plain,
multiply(commutator(X1,X2),multiply(X2,X1)) = multiply(X1,X2),
inference(orient,[status(thm)],[t110698]) ).
cnf(t705,plain,
inverse(commutator(X1,X2)) = multiply(multiply(X2,X1),inverse(multiply(X1,X2))),
inference(cp,[status(thm)],[t99,t659]) ).
cnf(t110,plain,
inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(cp,[status(thm)],[t108,t59]) ).
cnf(t125,plain,
inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(orient,[status(thm)],[t110]) ).
cnf(t198,plain,
multiply(inverse(multiply(X1,X2)),multiply(X2,X1)) = inverse(commutator(X1,X2)),
inference(cp,[status(thm)],[t125,t174]) ).
cnf(t110664,plain,
commutator(X2,X1) = inverse(commutator(X1,X2)),
inference(step,[status(thm)],[t198,t174]) ).
cnf(t201,plain,
inverse(commutator(X1,X2)) = commutator(X2,X1),
inference(orient,[status(thm)],[t110664]) ).
cnf(t110740,plain,
commutator(X2,X1) = multiply(multiply(X2,X1),inverse(multiply(X1,X2))),
inference(step,[status(thm)],[t705,t201]) ).
cnf(t110741,plain,
commutator(X2,X1) = multiply(X2,multiply(X1,inverse(multiply(X1,X2)))),
inference(step,[status(thm)],[t110740,t6]) ).
cnf(t2037,plain,
multiply(X1,multiply(X2,inverse(multiply(X2,X1)))) = commutator(X1,X2),
inference(orient,[status(thm)],[t110741]) ).
cnf(t2049,plain,
commutator(inverse(multiply(X1,X2)),X2) = multiply(inverse(multiply(X1,X2)),multiply(X2,inverse(inverse(X1)))),
inference(cp,[status(thm)],[t2037,t99]) ).
cnf(t240,plain,
commutator(inverse(X1),X2) = commutator(inverse(multiply(X1,X2)),X2),
inference(cp,[status(thm)],[t239,t108]) ).
cnf(t421,plain,
commutator(inverse(multiply(X1,X2)),X2) = commutator(inverse(X1),X2),
inference(orient,[status(thm)],[t240]) ).
cnf(t110742,plain,
commutator(inverse(X1),X2) = multiply(inverse(multiply(X1,X2)),multiply(X2,inverse(inverse(X1)))),
inference(step,[status(thm)],[t2049,t421]) ).
cnf(t110743,plain,
commutator(inverse(X1),X2) = multiply(inverse(multiply(X1,X2)),multiply(X2,X1)),
inference(step,[status(thm)],[t110742,t59]) ).
cnf(t110744,plain,
commutator(inverse(X1),X2) = commutator(X2,X1),
inference(step,[status(thm)],[t110743,t174]) ).
cnf(t2100,plain,
commutator(inverse(X1),X2) = commutator(X2,X1),
inference(orient,[status(thm)],[t110744]) ).
cnf(t2127,plain,
multiply(inverse(X1),X2) = multiply(X2,multiply(inverse(X1),commutator(X2,X1))),
inference(cp,[status(thm)],[t556,t2100]) ).
cnf(t3404,plain,
multiply(X1,multiply(inverse(X2),commutator(X1,X2))) = multiply(inverse(X2),X1),
inference(orient,[status(thm)],[t2127]) ).
cnf(t203,plain,
commutator(commutator(X1,X2),X1) = inverse(identity),
inference(cp,[status(thm)],[t201,t40]) ).
cnf(t110665,plain,
commutator(X1,commutator(X2,X1)) = inverse(identity),
inference(step,[status(thm)],[t203,t15]) ).
cnf(t21,plain,
X1 = multiply(inverse(identity),X1),
inference(cp,[status(thm)],[t17,t5]) ).
cnf(t31,plain,
multiply(inverse(identity),X1) = X1,
inference(orient,[status(thm)],[t21]) ).
cnf(t32,plain,
X1 = multiply(inverse(inverse(identity)),X1),
inference(cp,[status(thm)],[t17,t31]) ).
cnf(t43,plain,
multiply(inverse(inverse(identity)),X1) = X1,
inference(orient,[status(thm)],[t32]) ).
cnf(t44,plain,
inverse(identity) = identity,
inference(cp,[status(thm)],[t43,t7]) ).
cnf(t49,plain,
inverse(identity) = identity,
inference(orient,[status(thm)],[t44]) ).
cnf(t110666,plain,
commutator(X1,commutator(X2,X1)) = identity,
inference(step,[status(thm)],[t110665,t49]) ).
cnf(t221,plain,
commutator(X1,commutator(X2,X1)) = identity,
inference(orient,[status(thm)],[t110666]) ).
cnf(t565,plain,
multiply(X1,commutator(X2,X1)) = multiply(commutator(X2,X1),multiply(X1,identity)),
inference(cp,[status(thm)],[t556,t221]) ).
cnf(t110693,plain,
multiply(X1,commutator(X2,X1)) = multiply(commutator(X2,X1),X1),
inference(step,[status(thm)],[t565,t57]) ).
cnf(t611,plain,
multiply(commutator(X1,X2),X2) = multiply(X2,commutator(X1,X2)),
inference(orient,[status(thm)],[t110693]) ).
cnf(t265,plain,
commutator(X1,multiply(X1,X2)) = inverse(commutator(X2,X1)),
inference(cp,[status(thm)],[t201,t257]) ).
cnf(t110674,plain,
commutator(X1,multiply(X1,X2)) = commutator(X1,X2),
inference(step,[status(thm)],[t265,t201]) ).
cnf(t271,plain,
commutator(X1,multiply(X1,X2)) = commutator(X1,X2),
inference(orient,[status(thm)],[t110674]) ).
cnf(t280,plain,
commutator(multiply(X1,X2),X3) = commutator(multiply(X1,X2),multiply(X1,multiply(X2,X3))),
inference(cp,[status(thm)],[t271,t6]) ).
cnf(t8270,plain,
commutator(multiply(X1,X2),multiply(X1,multiply(X2,X3))) = commutator(multiply(X1,X2),X3),
inference(orient,[status(thm)],[t280]) ).
cnf(t576,plain,
multiply(multiply(inverse(X1),X2),X1) = multiply(X1,multiply(multiply(inverse(X1),X2),commutator(X2,X1))),
inference(cp,[status(thm)],[t556,t239]) ).
cnf(t110928,plain,
multiply(inverse(X1),multiply(X2,X1)) = multiply(X1,multiply(multiply(inverse(X1),X2),commutator(X2,X1))),
inference(step,[status(thm)],[t576,t6]) ).
cnf(t110929,plain,
multiply(inverse(X1),multiply(X2,X1)) = multiply(X1,multiply(inverse(X1),multiply(X2,commutator(X2,X1)))),
inference(step,[status(thm)],[t110928,t6]) ).
cnf(t110930,plain,
multiply(inverse(X1),multiply(X2,X1)) = multiply(X2,commutator(X2,X1)),
inference(step,[status(thm)],[t110929,t74]) ).
cnf(t7057,plain,
multiply(inverse(X1),multiply(X2,X1)) = multiply(X2,commutator(X2,X1)),
inference(orient,[status(thm)],[t110930]) ).
cnf(t8309,plain,
commutator(multiply(inverse(X1),X2),X1) = commutator(multiply(inverse(X1),X2),multiply(X2,commutator(X2,X1))),
inference(cp,[status(thm)],[t8270,t7057]) ).
cnf(t111072,plain,
commutator(X2,X1) = commutator(multiply(inverse(X1),X2),multiply(X2,commutator(X2,X1))),
inference(step,[status(thm)],[t8309,t239]) ).
cnf(t17302,plain,
commutator(multiply(inverse(X1),X2),multiply(X2,commutator(X2,X1))) = commutator(X2,X1),
inference(orient,[status(thm)],[t111072]) ).
cnf(t2047,plain,
commutator(multiply(X1,commutator(X1,X2)),X2) = multiply(multiply(X1,commutator(X1,X2)),multiply(X2,inverse(multiply(X1,X2)))),
inference(cp,[status(thm)],[t2037,t556]) ).
cnf(t591,plain,
commutator(multiply(X1,commutator(X1,X2)),X2) = commutator(multiply(X1,X2),X2),
inference(cp,[status(thm)],[t257,t556]) ).
cnf(t1775,plain,
commutator(multiply(X1,commutator(X1,X2)),X2) = commutator(multiply(X1,X2),X2),
inference(orient,[status(thm)],[t591]) ).
cnf(t110771,plain,
commutator(multiply(X1,X2),X2) = multiply(multiply(X1,commutator(X1,X2)),multiply(X2,inverse(multiply(X1,X2)))),
inference(step,[status(thm)],[t2047,t1775]) ).
cnf(t110772,plain,
commutator(multiply(X1,X2),X2) = multiply(X1,multiply(commutator(X1,X2),multiply(X2,inverse(multiply(X1,X2))))),
inference(step,[status(thm)],[t110771,t6]) ).
cnf(t110773,plain,
commutator(multiply(X1,X2),X2) = multiply(X1,multiply(commutator(X1,X2),inverse(X1))),
inference(step,[status(thm)],[t110772,t99]) ).
cnf(t18,plain,
multiply(inverse(X1),X1) = commutator(inverse(X1),X1),
inference(cp,[status(thm)],[t17,t9]) ).
cnf(t110652,plain,
identity = commutator(inverse(X1),X1),
inference(step,[status(thm)],[t18,t7]) ).
cnf(t29,plain,
commutator(inverse(X1),X1) = identity,
inference(orient,[status(thm)],[t110652]) ).
cnf(t30,plain,
commutator(inverse(X1),commutator(X1,X2)) = commutator(identity,X2),
inference(cp,[status(thm)],[t15,t29]) ).
cnf(t110657,plain,
commutator(inverse(X1),commutator(X1,X2)) = identity,
inference(step,[status(thm)],[t30,t16]) ).
cnf(t71,plain,
commutator(inverse(X1),commutator(X1,X2)) = identity,
inference(orient,[status(thm)],[t110657]) ).
cnf(t578,plain,
multiply(inverse(X1),commutator(X1,X2)) = multiply(commutator(X1,X2),multiply(inverse(X1),identity)),
inference(cp,[status(thm)],[t556,t71]) ).
cnf(t110728,plain,
multiply(inverse(X1),commutator(X1,X2)) = multiply(commutator(X1,X2),inverse(X1)),
inference(step,[status(thm)],[t578,t57]) ).
cnf(t1421,plain,
multiply(commutator(X1,X2),inverse(X1)) = multiply(inverse(X1),commutator(X1,X2)),
inference(orient,[status(thm)],[t110728]) ).
cnf(t110774,plain,
commutator(multiply(X1,X2),X2) = multiply(X1,multiply(inverse(X1),commutator(X1,X2))),
inference(step,[status(thm)],[t110773,t1421]) ).
cnf(t110775,plain,
commutator(multiply(X1,X2),X2) = commutator(X1,X2),
inference(step,[status(thm)],[t110774,t74]) ).
cnf(t2153,plain,
commutator(multiply(X1,X2),X2) = commutator(X1,X2),
inference(orient,[status(thm)],[t110775]) ).
cnf(t2055,plain,
commutator(multiply(X1,X2),inverse(X1)) = multiply(multiply(X1,X2),multiply(inverse(X1),inverse(X2))),
inference(cp,[status(thm)],[t2037,t17]) ).
cnf(t250,plain,
commutator(X1,inverse(X2)) = commutator(multiply(X2,X1),inverse(X2)),
inference(cp,[status(thm)],[t239,t59]) ).
cnf(t458,plain,
commutator(multiply(X1,X2),inverse(X1)) = commutator(X2,inverse(X1)),
inference(orient,[status(thm)],[t250]) ).
cnf(t110760,plain,
commutator(X2,inverse(X1)) = multiply(multiply(X1,X2),multiply(inverse(X1),inverse(X2))),
inference(step,[status(thm)],[t2055,t458]) ).
cnf(t110761,plain,
commutator(X2,inverse(X1)) = multiply(X1,multiply(X2,multiply(inverse(X1),inverse(X2)))),
inference(step,[status(thm)],[t110760,t6]) ).
cnf(t110762,plain,
commutator(X2,inverse(X1)) = multiply(X1,multiply(X2,inverse(multiply(X2,X1)))),
inference(step,[status(thm)],[t110761,t108]) ).
cnf(t110763,plain,
commutator(X2,inverse(X1)) = commutator(X1,X2),
inference(step,[status(thm)],[t110762,t2037]) ).
cnf(t2133,plain,
commutator(X1,inverse(X2)) = commutator(X2,X1),
inference(orient,[status(thm)],[t110763]) ).
cnf(t2149,plain,
multiply(X1,inverse(X2)) = multiply(inverse(X2),multiply(X1,commutator(X2,X1))),
inference(cp,[status(thm)],[t556,t2133]) ).
cnf(t3541,plain,
multiply(inverse(X1),multiply(X2,commutator(X1,X2))) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t2149]) ).
cnf(t3578,plain,
commutator(inverse(X1),multiply(X2,commutator(X1,X2))) = commutator(multiply(X2,inverse(X1)),multiply(X2,commutator(X1,X2))),
inference(cp,[status(thm)],[t2153,t3541]) ).
cnf(t111043,plain,
commutator(multiply(X2,commutator(X1,X2)),X1) = commutator(multiply(X2,inverse(X1)),multiply(X2,commutator(X1,X2))),
inference(step,[status(thm)],[t3578,t2100]) ).
cnf(t208,plain,
inverse(multiply(commutator(X1,X2),X3)) = multiply(inverse(X3),commutator(X2,X1)),
inference(cp,[status(thm)],[t108,t201]) ).
cnf(t1321,plain,
inverse(multiply(commutator(X1,X2),X3)) = multiply(inverse(X3),commutator(X2,X1)),
inference(orient,[status(thm)],[t208]) ).
cnf(t623,plain,
multiply(commutator(X1,X2),multiply(X2,X3)) = multiply(multiply(X2,commutator(X1,X2)),X3),
inference(cp,[status(thm)],[t6,t611]) ).
cnf(t110821,plain,
multiply(commutator(X1,X2),multiply(X2,X3)) = multiply(X2,multiply(commutator(X1,X2),X3)),
inference(step,[status(thm)],[t623,t6]) ).
cnf(t3769,plain,
multiply(commutator(X1,X2),multiply(X2,X3)) = multiply(X2,multiply(commutator(X1,X2),X3)),
inference(orient,[status(thm)],[t110821]) ).
cnf(t3833,plain,
multiply(inverse(multiply(X1,X2)),commutator(X1,X3)) = inverse(multiply(X1,multiply(commutator(X3,X1),X2))),
inference(cp,[status(thm)],[t1321,t3769]) ).
cnf(t10071,plain,
inverse(multiply(X1,multiply(commutator(X2,X1),X3))) = multiply(inverse(multiply(X1,X3)),commutator(X1,X2)),
inference(orient,[status(thm)],[t3833]) ).
cnf(t10159,plain,
commutator(multiply(commutator(X1,X2),X3),X2) = multiply(multiply(inverse(multiply(X2,X3)),commutator(X2,X1)),multiply(multiply(commutator(X1,X2),X3),X2)),
inference(cp,[status(thm)],[t174,t10071]) ).
cnf(t110961,plain,
commutator(multiply(commutator(X1,X2),X3),X2) = multiply(inverse(multiply(X2,X3)),multiply(commutator(X2,X1),multiply(multiply(commutator(X1,X2),X3),X2))),
inference(step,[status(thm)],[t10159,t6]) ).
cnf(t110962,plain,
commutator(multiply(commutator(X1,X2),X3),X2) = multiply(inverse(multiply(X2,X3)),multiply(commutator(X2,X1),multiply(commutator(X1,X2),multiply(X3,X2)))),
inference(step,[status(thm)],[t110961,t6]) ).
cnf(t210,plain,
X1 = multiply(commutator(X2,X3),multiply(commutator(X3,X2),X1)),
inference(cp,[status(thm)],[t17,t201]) ).
cnf(t2881,plain,
multiply(commutator(X1,X2),multiply(commutator(X2,X1),X3)) = X3,
inference(orient,[status(thm)],[t210]) ).
cnf(t110963,plain,
commutator(multiply(commutator(X1,X2),X3),X2) = multiply(inverse(multiply(X2,X3)),multiply(X3,X2)),
inference(step,[status(thm)],[t110962,t2881]) ).
cnf(t110964,plain,
commutator(multiply(commutator(X1,X2),X3),X2) = commutator(X3,X2),
inference(step,[status(thm)],[t110963,t174]) ).
cnf(t10189,plain,
commutator(multiply(commutator(X1,X2),X3),X2) = commutator(X3,X2),
inference(orient,[status(thm)],[t110964]) ).
cnf(t207,plain,
inverse(multiply(X1,commutator(X2,X3))) = multiply(commutator(X3,X2),inverse(X1)),
inference(cp,[status(thm)],[t108,t201]) ).
cnf(t1255,plain,
inverse(multiply(X1,commutator(X2,X3))) = multiply(commutator(X3,X2),inverse(X1)),
inference(orient,[status(thm)],[t207]) ).
cnf(t2113,plain,
commutator(X1,multiply(X2,commutator(X3,Y3))) = commutator(multiply(commutator(Y3,X3),inverse(X2)),X1),
inference(cp,[status(thm)],[t2100,t1255]) ).
cnf(t7528,plain,
commutator(multiply(commutator(X1,X2),inverse(X3)),Y3) = commutator(Y3,multiply(X3,commutator(X2,X1))),
inference(orient,[status(thm)],[t2113]) ).
cnf(t10190,plain,
commutator(inverse(X1),X2) = commutator(X2,multiply(X1,commutator(X2,X3))),
inference(cp,[status(thm)],[t10189,t7528]) ).
cnf(t110965,plain,
commutator(X2,X1) = commutator(X2,multiply(X1,commutator(X2,X3))),
inference(step,[status(thm)],[t10190,t2100]) ).
cnf(t10318,plain,
commutator(X1,multiply(X2,commutator(X1,X3))) = commutator(X1,X2),
inference(orient,[status(thm)],[t110965]) ).
cnf(t10370,plain,
commutator(multiply(X1,commutator(X2,X3)),X2) = inverse(commutator(X2,X1)),
inference(cp,[status(thm)],[t201,t10318]) ).
cnf(t110974,plain,
commutator(multiply(X1,commutator(X2,X3)),X2) = commutator(X1,X2),
inference(step,[status(thm)],[t10370,t201]) ).
cnf(t10907,plain,
commutator(multiply(X1,commutator(X2,X3)),X2) = commutator(X1,X2),
inference(orient,[status(thm)],[t110974]) ).
cnf(t111044,plain,
commutator(X2,X1) = commutator(multiply(X2,inverse(X1)),multiply(X2,commutator(X1,X2))),
inference(step,[status(thm)],[t111043,t10907]) ).
cnf(t16270,plain,
commutator(multiply(X1,inverse(X2)),multiply(X1,commutator(X2,X1))) = commutator(X1,X2),
inference(orient,[status(thm)],[t111044]) ).
cnf(t17397,plain,
commutator(multiply(X1,inverse(X2)),multiply(X1,commutator(X2,X1))) = commutator(multiply(inverse(multiply(X1,commutator(X2,X1))),multiply(X1,inverse(X2))),multiply(multiply(X1,inverse(X2)),commutator(X1,X2))),
inference(cp,[status(thm)],[t17302,t16270]) ).
cnf(t111140,plain,
commutator(X1,X2) = commutator(multiply(inverse(multiply(X1,commutator(X2,X1))),multiply(X1,inverse(X2))),multiply(multiply(X1,inverse(X2)),commutator(X1,X2))),
inference(step,[status(thm)],[t17397,t16270]) ).
cnf(t106,plain,
inverse(X1) = multiply(inverse(multiply(X2,X1)),inverse(inverse(X2))),
inference(cp,[status(thm)],[t99,t99]) ).
cnf(t110660,plain,
inverse(X1) = inverse(multiply(inverse(X2),multiply(X2,X1))),
inference(step,[status(thm)],[t106,t108]) ).
cnf(t110661,plain,
inverse(X1) = multiply(inverse(multiply(X2,X1)),X2),
inference(step,[status(thm)],[t110660,t125]) ).
cnf(t140,plain,
multiply(inverse(multiply(X1,X2)),X1) = inverse(X2),
inference(orient,[status(thm)],[t110661]) ).
cnf(t143,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(X2),X3),
inference(cp,[status(thm)],[t6,t140]) ).
cnf(t3226,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(X2),X3),
inference(orient,[status(thm)],[t143]) ).
cnf(t111141,plain,
commutator(X1,X2) = commutator(multiply(inverse(commutator(X2,X1)),inverse(X2)),multiply(multiply(X1,inverse(X2)),commutator(X1,X2))),
inference(step,[status(thm)],[t111140,t3226]) ).
cnf(t111142,plain,
commutator(X1,X2) = commutator(inverse(multiply(X2,commutator(X2,X1))),multiply(multiply(X1,inverse(X2)),commutator(X1,X2))),
inference(step,[status(thm)],[t111141,t108]) ).
cnf(t111143,plain,
commutator(X1,X2) = commutator(multiply(commutator(X1,X2),inverse(X2)),multiply(multiply(X1,inverse(X2)),commutator(X1,X2))),
inference(step,[status(thm)],[t111142,t1255]) ).
cnf(t60,plain,
identity = commutator(X1,inverse(X1)),
inference(cp,[status(thm)],[t29,t59]) ).
cnf(t65,plain,
commutator(X1,inverse(X1)) = identity,
inference(orient,[status(thm)],[t60]) ).
cnf(t67,plain,
commutator(X1,commutator(inverse(X1),X2)) = commutator(identity,X2),
inference(cp,[status(thm)],[t15,t65]) ).
cnf(t110658,plain,
commutator(X1,commutator(inverse(X1),X2)) = identity,
inference(step,[status(thm)],[t67,t16]) ).
cnf(t78,plain,
commutator(X1,commutator(inverse(X1),X2)) = identity,
inference(orient,[status(thm)],[t110658]) ).
cnf(t204,plain,
commutator(commutator(inverse(X1),X2),X1) = inverse(identity),
inference(cp,[status(thm)],[t201,t78]) ).
cnf(t110667,plain,
commutator(inverse(X1),commutator(X2,X1)) = inverse(identity),
inference(step,[status(thm)],[t204,t15]) ).
cnf(t110668,plain,
commutator(inverse(X1),commutator(X2,X1)) = identity,
inference(step,[status(thm)],[t110667,t49]) ).
cnf(t225,plain,
commutator(inverse(X1),commutator(X2,X1)) = identity,
inference(orient,[status(thm)],[t110668]) ).
cnf(t579,plain,
multiply(inverse(X1),commutator(X2,X1)) = multiply(commutator(X2,X1),multiply(inverse(X1),identity)),
inference(cp,[status(thm)],[t556,t225]) ).
cnf(t110729,plain,
multiply(inverse(X1),commutator(X2,X1)) = multiply(commutator(X2,X1),inverse(X1)),
inference(step,[status(thm)],[t579,t57]) ).
cnf(t1445,plain,
multiply(commutator(X1,X2),inverse(X2)) = multiply(inverse(X2),commutator(X1,X2)),
inference(orient,[status(thm)],[t110729]) ).
cnf(t111144,plain,
commutator(X1,X2) = commutator(multiply(inverse(X2),commutator(X1,X2)),multiply(multiply(X1,inverse(X2)),commutator(X1,X2))),
inference(step,[status(thm)],[t111143,t1445]) ).
cnf(t2110,plain,
commutator(X1,multiply(commutator(X2,X3),Y3)) = commutator(multiply(inverse(Y3),commutator(X3,X2)),X1),
inference(cp,[status(thm)],[t2100,t1321]) ).
cnf(t7419,plain,
commutator(multiply(inverse(X1),commutator(X2,X3)),Y3) = commutator(Y3,multiply(commutator(X3,X2),X1)),
inference(orient,[status(thm)],[t2110]) ).
cnf(t111145,plain,
commutator(X1,X2) = commutator(multiply(multiply(X1,inverse(X2)),commutator(X1,X2)),multiply(commutator(X2,X1),X2)),
inference(step,[status(thm)],[t111144,t7419]) ).
cnf(t111146,plain,
commutator(X1,X2) = commutator(multiply(X1,multiply(inverse(X2),commutator(X1,X2))),multiply(commutator(X2,X1),X2)),
inference(step,[status(thm)],[t111145,t6]) ).
cnf(t111147,plain,
commutator(X1,X2) = commutator(multiply(inverse(X2),X1),multiply(commutator(X2,X1),X2)),
inference(step,[status(thm)],[t111146,t3404]) ).
cnf(t568,plain,
multiply(X1,commutator(X1,X2)) = multiply(commutator(X1,X2),multiply(X1,identity)),
inference(cp,[status(thm)],[t556,t40]) ).
cnf(t110694,plain,
multiply(X1,commutator(X1,X2)) = multiply(commutator(X1,X2),X1),
inference(step,[status(thm)],[t568,t57]) ).
cnf(t634,plain,
multiply(commutator(X1,X2),X1) = multiply(X1,commutator(X1,X2)),
inference(orient,[status(thm)],[t110694]) ).
cnf(t111148,plain,
commutator(X1,X2) = commutator(multiply(inverse(X2),X1),multiply(X2,commutator(X2,X1))),
inference(step,[status(thm)],[t111147,t634]) ).
cnf(t19869,plain,
commutator(multiply(inverse(X1),X2),multiply(X1,commutator(X1,X2))) = commutator(X2,X1),
inference(orient,[status(thm)],[t111148]) ).
cnf(t2058,plain,
multiply(X1,multiply(multiply(X2,inverse(multiply(X2,X1))),X3)) = multiply(commutator(X1,X2),X3),
inference(cp,[status(thm)],[t6,t2037]) ).
cnf(t111464,plain,
multiply(X1,multiply(X2,multiply(inverse(multiply(X2,X1)),X3))) = multiply(commutator(X1,X2),X3),
inference(step,[status(thm)],[t2058,t6]) ).
cnf(t39460,plain,
multiply(X1,multiply(X2,multiply(inverse(multiply(X2,X1)),X3))) = multiply(commutator(X1,X2),X3),
inference(orient,[status(thm)],[t111464]) ).
cnf(t39576,plain,
commutator(multiply(X1,multiply(inverse(multiply(X1,inverse(X2))),X3)),X2) = commutator(multiply(commutator(inverse(X2),X1),X3),multiply(X2,commutator(X2,multiply(X1,multiply(inverse(multiply(X1,inverse(X2))),X3))))),
inference(cp,[status(thm)],[t19869,t39460]) ).
cnf(t107,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(cp,[status(thm)],[t74,t99]) ).
cnf(t114,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t107]) ).
cnf(t111857,plain,
commutator(multiply(X1,multiply(multiply(X2,inverse(X1)),X3)),X2) = commutator(multiply(commutator(inverse(X2),X1),X3),multiply(X2,commutator(X2,multiply(X1,multiply(inverse(multiply(X1,inverse(X2))),X3))))),
inference(step,[status(thm)],[t39576,t114]) ).
cnf(t111858,plain,
commutator(multiply(X1,multiply(X2,multiply(inverse(X1),X3))),X2) = commutator(multiply(commutator(inverse(X2),X1),X3),multiply(X2,commutator(X2,multiply(X1,multiply(inverse(multiply(X1,inverse(X2))),X3))))),
inference(step,[status(thm)],[t111857,t6]) ).
cnf(t646,plain,
multiply(commutator(X1,X2),multiply(X1,X3)) = multiply(multiply(X1,commutator(X1,X2)),X3),
inference(cp,[status(thm)],[t6,t634]) ).
cnf(t110822,plain,
multiply(commutator(X1,X2),multiply(X1,X3)) = multiply(X1,multiply(commutator(X1,X2),X3)),
inference(step,[status(thm)],[t646,t6]) ).
cnf(t3845,plain,
multiply(commutator(X1,X2),multiply(X1,X3)) = multiply(X1,multiply(commutator(X1,X2),X3)),
inference(orient,[status(thm)],[t110822]) ).
cnf(t10200,plain,
commutator(multiply(X1,X2),X3) = commutator(multiply(X1,multiply(commutator(X1,X3),X2)),X3),
inference(cp,[status(thm)],[t10189,t3845]) ).
cnf(t11943,plain,
commutator(multiply(X1,multiply(commutator(X1,X2),X3)),X2) = commutator(multiply(X1,X3),X2),
inference(orient,[status(thm)],[t10200]) ).
cnf(t12016,plain,
commutator(multiply(multiply(X1,X2),X3),X1) = commutator(multiply(multiply(X1,X2),multiply(commutator(X2,X1),X3)),X1),
inference(cp,[status(thm)],[t11943,t257]) ).
cnf(t111009,plain,
commutator(multiply(X1,multiply(X2,X3)),X1) = commutator(multiply(multiply(X1,X2),multiply(commutator(X2,X1),X3)),X1),
inference(step,[status(thm)],[t12016,t6]) ).
cnf(t111010,plain,
commutator(multiply(X2,X3),X1) = commutator(multiply(multiply(X1,X2),multiply(commutator(X2,X1),X3)),X1),
inference(step,[status(thm)],[t111009,t257]) ).
cnf(t111011,plain,
commutator(multiply(X2,X3),X1) = commutator(multiply(X1,multiply(X2,multiply(commutator(X2,X1),X3))),X1),
inference(step,[status(thm)],[t111010,t6]) ).
cnf(t581,plain,
multiply(X1,multiply(multiply(X2,commutator(X2,X1)),X3)) = multiply(multiply(X2,X1),X3),
inference(cp,[status(thm)],[t6,t556]) ).
cnf(t110939,plain,
multiply(X1,multiply(X2,multiply(commutator(X2,X1),X3))) = multiply(multiply(X2,X1),X3),
inference(step,[status(thm)],[t581,t6]) ).
cnf(t110940,plain,
multiply(X1,multiply(X2,multiply(commutator(X2,X1),X3))) = multiply(X2,multiply(X1,X3)),
inference(step,[status(thm)],[t110939,t6]) ).
cnf(t8494,plain,
multiply(X1,multiply(X2,multiply(commutator(X2,X1),X3))) = multiply(X2,multiply(X1,X3)),
inference(orient,[status(thm)],[t110940]) ).
cnf(t111012,plain,
commutator(multiply(X2,X3),X1) = commutator(multiply(X2,multiply(X1,X3)),X1),
inference(step,[status(thm)],[t111011,t8494]) ).
cnf(t12090,plain,
commutator(multiply(X1,multiply(X2,X3)),X2) = commutator(multiply(X1,X3),X2),
inference(orient,[status(thm)],[t111012]) ).
cnf(t111859,plain,
commutator(multiply(X1,multiply(inverse(X1),X3)),X2) = commutator(multiply(commutator(inverse(X2),X1),X3),multiply(X2,commutator(X2,multiply(X1,multiply(inverse(multiply(X1,inverse(X2))),X3))))),
inference(step,[status(thm)],[t111858,t12090]) ).
cnf(t111860,plain,
commutator(X3,X2) = commutator(multiply(commutator(inverse(X2),X1),X3),multiply(X2,commutator(X2,multiply(X1,multiply(inverse(multiply(X1,inverse(X2))),X3))))),
inference(step,[status(thm)],[t111859,t74]) ).
cnf(t111861,plain,
commutator(X3,X2) = commutator(multiply(commutator(X1,X2),X3),multiply(X2,commutator(X2,multiply(X1,multiply(inverse(multiply(X1,inverse(X2))),X3))))),
inference(step,[status(thm)],[t111860,t2100]) ).
cnf(t111862,plain,
commutator(X3,X2) = commutator(multiply(commutator(X1,X2),X3),multiply(X2,commutator(X2,multiply(X1,multiply(multiply(X2,inverse(X1)),X3))))),
inference(step,[status(thm)],[t111861,t114]) ).
cnf(t111863,plain,
commutator(X3,X2) = commutator(multiply(commutator(X1,X2),X3),multiply(X2,commutator(X2,multiply(X1,multiply(X2,multiply(inverse(X1),X3)))))),
inference(step,[status(thm)],[t111862,t6]) ).
cnf(t12135,plain,
commutator(multiply(X1,multiply(X2,X3)),inverse(X2)) = commutator(multiply(X1,X3),inverse(X2)),
inference(cp,[status(thm)],[t12090,t17]) ).
cnf(t111013,plain,
commutator(X2,multiply(X1,multiply(X2,X3))) = commutator(multiply(X1,X3),inverse(X2)),
inference(step,[status(thm)],[t12135,t2133]) ).
cnf(t111014,plain,
commutator(X2,multiply(X1,multiply(X2,X3))) = commutator(X2,multiply(X1,X3)),
inference(step,[status(thm)],[t111013,t2133]) ).
cnf(t12205,plain,
commutator(X1,multiply(X2,multiply(X1,X3))) = commutator(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t111014]) ).
cnf(t111864,plain,
commutator(X3,X2) = commutator(multiply(commutator(X1,X2),X3),multiply(X2,commutator(X2,multiply(X1,multiply(inverse(X1),X3))))),
inference(step,[status(thm)],[t111863,t12205]) ).
cnf(t111865,plain,
commutator(X3,X2) = commutator(multiply(commutator(X1,X2),X3),multiply(X2,commutator(X2,X3))),
inference(step,[status(thm)],[t111864,t74]) ).
cnf(t89074,plain,
commutator(multiply(commutator(X1,X2),X3),multiply(X2,commutator(X2,X3))) = commutator(X3,X2),
inference(orient,[status(thm)],[t111865]) ).
cnf(t2112,plain,
commutator(X1,multiply(X2,inverse(X3))) = commutator(multiply(X3,inverse(X2)),X1),
inference(cp,[status(thm)],[t2100,t114]) ).
cnf(t23137,plain,
commutator(X1,multiply(X2,inverse(X3))) = commutator(multiply(X3,inverse(X2)),X1),
inference(orient,[status(thm)],[t2112]) ).
cnf(t89076,plain,
commutator(inverse(X1),X2) = commutator(multiply(X2,commutator(X2,inverse(X1))),multiply(X1,inverse(commutator(X3,X2)))),
inference(cp,[status(thm)],[t89074,t23137]) ).
cnf(t111940,plain,
commutator(X2,X1) = commutator(multiply(X2,commutator(X2,inverse(X1))),multiply(X1,inverse(commutator(X3,X2)))),
inference(step,[status(thm)],[t89076,t2100]) ).
cnf(t111941,plain,
commutator(X2,X1) = commutator(multiply(X2,commutator(X1,X2)),multiply(X1,inverse(commutator(X3,X2)))),
inference(step,[status(thm)],[t111940,t2133]) ).
cnf(t111942,plain,
commutator(X2,X1) = commutator(multiply(X2,commutator(X1,X2)),multiply(X1,commutator(X2,X3))),
inference(step,[status(thm)],[t111941,t201]) ).
cnf(t96668,plain,
commutator(multiply(X1,commutator(X2,X1)),multiply(X2,commutator(X1,X3))) = commutator(X1,X2),
inference(orient,[status(thm)],[t111942]) ).
cnf(t96986,plain,
multiply(multiply(X1,commutator(X2,X3)),commutator(multiply(X2,commutator(X1,X2)),multiply(X1,commutator(X2,X3)))) = multiply(commutator(X2,X1),multiply(X1,commutator(X2,X3))),
inference(cp,[status(thm)],[t611,t96668]) ).
cnf(t111943,plain,
multiply(X1,multiply(commutator(X2,X3),commutator(multiply(X2,commutator(X1,X2)),multiply(X1,commutator(X2,X3))))) = multiply(commutator(X2,X1),multiply(X1,commutator(X2,X3))),
inference(step,[status(thm)],[t96986,t6]) ).
cnf(t111944,plain,
multiply(X1,multiply(commutator(X2,X3),commutator(X2,X1))) = multiply(commutator(X2,X1),multiply(X1,commutator(X2,X3))),
inference(step,[status(thm)],[t111943,t96668]) ).
cnf(t192,plain,
multiply(inverse(multiply(X1,X2)),multiply(multiply(X2,X1),X3)) = multiply(commutator(X2,X1),X3),
inference(cp,[status(thm)],[t6,t174]) ).
cnf(t111316,plain,
multiply(inverse(multiply(X1,X2)),multiply(X2,multiply(X1,X3))) = multiply(commutator(X2,X1),X3),
inference(step,[status(thm)],[t192,t6]) ).
cnf(t28323,plain,
multiply(inverse(multiply(X1,X2)),multiply(X2,multiply(X1,X3))) = multiply(commutator(X2,X1),X3),
inference(orient,[status(thm)],[t111316]) ).
cnf(t196,plain,
multiply(inverse(multiply(multiply(X1,X2),X3)),multiply(X2,X1)) = multiply(inverse(X3),commutator(X2,X1)),
inference(cp,[status(thm)],[t166,t174]) ).
cnf(t111901,plain,
multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X2,X1)) = multiply(inverse(X3),commutator(X2,X1)),
inference(step,[status(thm)],[t196,t6]) ).
cnf(t93588,plain,
multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X2,X1)) = multiply(inverse(X3),commutator(X2,X1)),
inference(orient,[status(thm)],[t111901]) ).
cnf(t93797,plain,
multiply(commutator(inverse(multiply(X1,multiply(X2,X3))),X2),X1) = multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(X2,X3))))),multiply(inverse(X3),commutator(X2,X1))),
inference(cp,[status(thm)],[t28323,t93588]) ).
cnf(t111902,plain,
multiply(commutator(X2,multiply(X1,multiply(X2,X3))),X1) = multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(X2,X3))))),multiply(inverse(X3),commutator(X2,X1))),
inference(step,[status(thm)],[t93797,t2100]) ).
cnf(t111903,plain,
multiply(commutator(X2,multiply(X1,X3)),X1) = multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(X2,X3))))),multiply(inverse(X3),commutator(X2,X1))),
inference(step,[status(thm)],[t111902,t12205]) ).
cnf(t111904,plain,
multiply(commutator(X2,multiply(X1,X3)),X1) = multiply(inverse(multiply(X3,multiply(X2,inverse(multiply(X1,multiply(X2,X3)))))),commutator(X2,X1)),
inference(step,[status(thm)],[t111903,t166]) ).
cnf(t115,plain,
multiply(X1,inverse(multiply(X2,X3))) = inverse(multiply(X2,multiply(X3,inverse(X1)))),
inference(cp,[status(thm)],[t114,t6]) ).
cnf(t3076,plain,
inverse(multiply(X1,multiply(X2,inverse(X3)))) = multiply(X3,inverse(multiply(X1,X2))),
inference(orient,[status(thm)],[t115]) ).
cnf(t111905,plain,
multiply(commutator(X2,multiply(X1,X3)),X1) = multiply(multiply(multiply(X1,multiply(X2,X3)),inverse(multiply(X3,X2))),commutator(X2,X1)),
inference(step,[status(thm)],[t111904,t3076]) ).
cnf(t111906,plain,
multiply(commutator(X2,multiply(X1,X3)),X1) = multiply(multiply(X1,multiply(multiply(X2,X3),inverse(multiply(X3,X2)))),commutator(X2,X1)),
inference(step,[status(thm)],[t111905,t6]) ).
cnf(t111907,plain,
multiply(commutator(X2,multiply(X1,X3)),X1) = multiply(X1,multiply(multiply(multiply(X2,X3),inverse(multiply(X3,X2))),commutator(X2,X1))),
inference(step,[status(thm)],[t111906,t6]) ).
cnf(t111908,plain,
multiply(commutator(X2,multiply(X1,X3)),X1) = multiply(X1,multiply(multiply(X2,X3),multiply(inverse(multiply(X3,X2)),commutator(X2,X1)))),
inference(step,[status(thm)],[t111907,t6]) ).
cnf(t111909,plain,
multiply(commutator(X2,multiply(X1,X3)),X1) = multiply(X1,multiply(X2,multiply(X3,multiply(inverse(multiply(X3,X2)),commutator(X2,X1))))),
inference(step,[status(thm)],[t111908,t6]) ).
cnf(t111910,plain,
multiply(commutator(X2,multiply(X1,X3)),X1) = multiply(X1,multiply(commutator(X2,X3),commutator(X2,X1))),
inference(step,[status(thm)],[t111909,t39460]) ).
cnf(t93951,plain,
multiply(X1,multiply(commutator(X2,X3),commutator(X2,X1))) = multiply(commutator(X2,multiply(X1,X3)),X1),
inference(orient,[status(thm)],[t111910]) ).
cnf(t111945,plain,
multiply(commutator(X2,multiply(X1,X3)),X1) = multiply(commutator(X2,X1),multiply(X1,commutator(X2,X3))),
inference(step,[status(thm)],[t111944,t93951]) ).
cnf(t111946,plain,
multiply(commutator(X2,multiply(X1,X3)),X1) = multiply(X1,multiply(commutator(X2,X1),commutator(X2,X3))),
inference(step,[status(thm)],[t111945,t3769]) ).
cnf(t97182,plain,
multiply(X1,multiply(commutator(X2,X1),commutator(X2,X3))) = multiply(commutator(X2,multiply(X1,X3)),X1),
inference(orient,[status(thm)],[t111946]) ).
cnf(t97328,plain,
multiply(commutator(inverse(X1),multiply(X2,X3)),X2) = multiply(X2,multiply(commutator(X2,X1),commutator(inverse(X1),X3))),
inference(cp,[status(thm)],[t97182,t2100]) ).
cnf(t111953,plain,
multiply(commutator(multiply(X2,X3),X1),X2) = multiply(X2,multiply(commutator(X2,X1),commutator(inverse(X1),X3))),
inference(step,[status(thm)],[t97328,t2100]) ).
cnf(t111954,plain,
multiply(commutator(multiply(X2,X3),X1),X2) = multiply(X2,multiply(commutator(X2,X1),commutator(X3,X1))),
inference(step,[status(thm)],[t111953,t2100]) ).
cnf(t99051,plain,
multiply(X1,multiply(commutator(X1,X2),commutator(X3,X2))) = multiply(commutator(multiply(X1,X3),X2),X1),
inference(orient,[status(thm)],[t111954]) ).
cnf(t99207,plain,
multiply(commutator(multiply(multiply(X1,X2),X3),X1),multiply(X1,X2)) = multiply(multiply(X1,X2),multiply(commutator(X2,X1),commutator(X3,X1))),
inference(cp,[status(thm)],[t99051,t257]) ).
cnf(t111957,plain,
multiply(X1,multiply(commutator(multiply(multiply(X1,X2),X3),X1),X2)) = multiply(multiply(X1,X2),multiply(commutator(X2,X1),commutator(X3,X1))),
inference(step,[status(thm)],[t99207,t3769]) ).
cnf(t111958,plain,
multiply(X1,multiply(commutator(multiply(X1,multiply(X2,X3)),X1),X2)) = multiply(multiply(X1,X2),multiply(commutator(X2,X1),commutator(X3,X1))),
inference(step,[status(thm)],[t111957,t6]) ).
cnf(t111959,plain,
multiply(X1,multiply(commutator(multiply(X2,X3),X1),X2)) = multiply(multiply(X1,X2),multiply(commutator(X2,X1),commutator(X3,X1))),
inference(step,[status(thm)],[t111958,t257]) ).
cnf(t111960,plain,
multiply(X1,multiply(commutator(multiply(X2,X3),X1),X2)) = multiply(X1,multiply(X2,multiply(commutator(X2,X1),commutator(X3,X1)))),
inference(step,[status(thm)],[t111959,t6]) ).
cnf(t111961,plain,
multiply(X1,multiply(commutator(multiply(X2,X3),X1),X2)) = multiply(X2,multiply(X1,commutator(X3,X1))),
inference(step,[status(thm)],[t111960,t8494]) ).
cnf(t100334,plain,
multiply(X1,multiply(commutator(multiply(X2,X3),X1),X2)) = multiply(X2,multiply(X1,commutator(X3,X1))),
inference(orient,[status(thm)],[t111961]) ).
cnf(t100546,plain,
multiply(X1,multiply(X2,commutator(inverse(multiply(X3,X1)),X2))) = multiply(X2,multiply(commutator(inverse(X3),X2),X1)),
inference(cp,[status(thm)],[t100334,t99]) ).
cnf(t111962,plain,
multiply(X1,multiply(X2,commutator(X2,multiply(X3,X1)))) = multiply(X2,multiply(commutator(inverse(X3),X2),X1)),
inference(step,[status(thm)],[t100546,t2100]) ).
cnf(t111963,plain,
multiply(X1,multiply(X2,commutator(X2,multiply(X3,X1)))) = multiply(X2,multiply(commutator(X2,X3),X1)),
inference(step,[status(thm)],[t111962,t2100]) ).
cnf(t100902,plain,
multiply(X1,multiply(X2,commutator(X2,multiply(X3,X1)))) = multiply(X2,multiply(commutator(X2,X3),X1)),
inference(orient,[status(thm)],[t111963]) ).
cnf(t101314,plain,
commutator(multiply(X1,commutator(X1,multiply(X2,X3))),X3) = multiply(multiply(X1,commutator(X1,multiply(X2,X3))),multiply(X3,inverse(multiply(X1,multiply(commutator(X1,X2),X3))))),
inference(cp,[status(thm)],[t2037,t100902]) ).
cnf(t185,plain,
commutator(X1,multiply(inverse(X1),X2)) = multiply(inverse(multiply(multiply(inverse(X1),X2),X1)),X2),
inference(cp,[status(thm)],[t174,t74]) ).
cnf(t110675,plain,
commutator(X1,multiply(inverse(X1),X2)) = multiply(inverse(multiply(inverse(X1),multiply(X2,X1))),X2),
inference(step,[status(thm)],[t185,t6]) ).
cnf(t110676,plain,
commutator(X1,multiply(inverse(X1),X2)) = multiply(multiply(inverse(multiply(X2,X1)),X1),X2),
inference(step,[status(thm)],[t110675,t125]) ).
cnf(t110677,plain,
commutator(X1,multiply(inverse(X1),X2)) = multiply(inverse(multiply(X2,X1)),multiply(X1,X2)),
inference(step,[status(thm)],[t110676,t6]) ).
cnf(t110678,plain,
commutator(X1,multiply(inverse(X1),X2)) = commutator(X1,X2),
inference(step,[status(thm)],[t110677,t174]) ).
cnf(t284,plain,
commutator(X1,multiply(inverse(X1),X2)) = commutator(X1,X2),
inference(orient,[status(thm)],[t110678]) ).
cnf(t287,plain,
commutator(X1,multiply(inverse(X2),X3)) = commutator(X1,multiply(inverse(multiply(X2,X1)),X3)),
inference(cp,[status(thm)],[t284,t166]) ).
cnf(t6361,plain,
commutator(X1,multiply(inverse(multiply(X2,X1)),X3)) = commutator(X1,multiply(inverse(X2),X3)),
inference(orient,[status(thm)],[t287]) ).
cnf(t2088,plain,
inverse(multiply(X1,inverse(multiply(X1,X2)))) = multiply(inverse(commutator(X2,X1)),X2),
inference(cp,[status(thm)],[t140,t2037]) ).
cnf(t110931,plain,
multiply(multiply(X1,X2),inverse(X1)) = multiply(inverse(commutator(X2,X1)),X2),
inference(step,[status(thm)],[t2088,t114]) ).
cnf(t110932,plain,
multiply(X1,multiply(X2,inverse(X1))) = multiply(inverse(commutator(X2,X1)),X2),
inference(step,[status(thm)],[t110931,t6]) ).
cnf(t110933,plain,
multiply(X1,multiply(X2,inverse(X1))) = multiply(commutator(X1,X2),X2),
inference(step,[status(thm)],[t110932,t201]) ).
cnf(t110934,plain,
multiply(X1,multiply(X2,inverse(X1))) = multiply(X2,commutator(X1,X2)),
inference(step,[status(thm)],[t110933,t611]) ).
cnf(t7234,plain,
multiply(X1,multiply(X2,inverse(X1))) = multiply(X2,commutator(X1,X2)),
inference(orient,[status(thm)],[t110934]) ).
cnf(t7378,plain,
multiply(inverse(commutator(X1,X2)),X3) = multiply(inverse(multiply(X1,multiply(X2,inverse(X1)))),multiply(X2,X3)),
inference(cp,[status(thm)],[t3226,t7234]) ).
cnf(t111465,plain,
multiply(commutator(X2,X1),X3) = multiply(inverse(multiply(X1,multiply(X2,inverse(X1)))),multiply(X2,X3)),
inference(step,[status(thm)],[t7378,t201]) ).
cnf(t111466,plain,
multiply(commutator(X2,X1),X3) = multiply(multiply(X1,inverse(multiply(X1,X2))),multiply(X2,X3)),
inference(step,[status(thm)],[t111465,t3076]) ).
cnf(t111467,plain,
multiply(commutator(X2,X1),X3) = multiply(X1,multiply(inverse(multiply(X1,X2)),multiply(X2,X3))),
inference(step,[status(thm)],[t111466,t6]) ).
cnf(t39713,plain,
multiply(X1,multiply(inverse(multiply(X1,X2)),multiply(X2,X3))) = multiply(commutator(X2,X1),X3),
inference(orient,[status(thm)],[t111467]) ).
cnf(t39953,plain,
commutator(X1,multiply(inverse(X2),multiply(inverse(multiply(inverse(multiply(X2,X1)),X3)),multiply(X3,Y3)))) = commutator(X1,multiply(commutator(X3,inverse(multiply(X2,X1))),Y3)),
inference(cp,[status(thm)],[t6361,t39713]) ).
cnf(t111562,plain,
commutator(X1,multiply(inverse(multiply(multiply(inverse(multiply(X2,X1)),X3),X2)),multiply(X3,Y3))) = commutator(X1,multiply(commutator(X3,inverse(multiply(X2,X1))),Y3)),
inference(step,[status(thm)],[t39953,t166]) ).
cnf(t111563,plain,
commutator(X1,multiply(inverse(multiply(inverse(multiply(X2,X1)),multiply(X3,X2))),multiply(X3,Y3))) = commutator(X1,multiply(commutator(X3,inverse(multiply(X2,X1))),Y3)),
inference(step,[status(thm)],[t111562,t6]) ).
cnf(t111564,plain,
commutator(X1,multiply(multiply(inverse(multiply(X3,X2)),multiply(X2,X1)),multiply(X3,Y3))) = commutator(X1,multiply(commutator(X3,inverse(multiply(X2,X1))),Y3)),
inference(step,[status(thm)],[t111563,t125]) ).
cnf(t111565,plain,
commutator(X1,multiply(inverse(multiply(X3,X2)),multiply(multiply(X2,X1),multiply(X3,Y3)))) = commutator(X1,multiply(commutator(X3,inverse(multiply(X2,X1))),Y3)),
inference(step,[status(thm)],[t111564,t6]) ).
cnf(t111566,plain,
commutator(X1,multiply(inverse(multiply(X3,X2)),multiply(X2,multiply(X1,multiply(X3,Y3))))) = commutator(X1,multiply(commutator(X3,inverse(multiply(X2,X1))),Y3)),
inference(step,[status(thm)],[t111565,t6]) ).
cnf(t12221,plain,
commutator(X1,multiply(multiply(X2,X3),Y3)) = commutator(X1,multiply(X2,multiply(X3,multiply(X1,Y3)))),
inference(cp,[status(thm)],[t12205,t6]) ).
cnf(t111242,plain,
commutator(X1,multiply(X2,multiply(X3,Y3))) = commutator(X1,multiply(X2,multiply(X3,multiply(X1,Y3)))),
inference(step,[status(thm)],[t12221,t6]) ).
cnf(t25424,plain,
commutator(X1,multiply(X2,multiply(X3,multiply(X1,Y3)))) = commutator(X1,multiply(X2,multiply(X3,Y3))),
inference(orient,[status(thm)],[t111242]) ).
cnf(t111567,plain,
commutator(X1,multiply(inverse(multiply(X3,X2)),multiply(X2,multiply(X3,Y3)))) = commutator(X1,multiply(commutator(X3,inverse(multiply(X2,X1))),Y3)),
inference(step,[status(thm)],[t111566,t25424]) ).
cnf(t111568,plain,
commutator(X1,multiply(commutator(X2,X3),Y3)) = commutator(X1,multiply(commutator(X3,inverse(multiply(X2,X1))),Y3)),
inference(step,[status(thm)],[t111567,t28323]) ).
cnf(t111569,plain,
commutator(X1,multiply(commutator(X2,X3),Y3)) = commutator(X1,multiply(commutator(multiply(X2,X1),X3),Y3)),
inference(step,[status(thm)],[t111568,t2133]) ).
cnf(t61149,plain,
commutator(X1,multiply(commutator(multiply(X2,X1),X3),Y3)) = commutator(X1,multiply(commutator(X2,X3),Y3)),
inference(orient,[status(thm)],[t111569]) ).
cnf(t2142,plain,
commutator(multiply(X1,commutator(X2,X3)),Y3) = commutator(Y3,multiply(commutator(X3,X2),inverse(X1))),
inference(cp,[status(thm)],[t2133,t1255]) ).
cnf(t7716,plain,
commutator(X1,multiply(commutator(X2,X3),inverse(Y3))) = commutator(multiply(Y3,commutator(X3,X2)),X1),
inference(orient,[status(thm)],[t2142]) ).
cnf(t61154,plain,
commutator(X1,multiply(commutator(X2,X3),inverse(Y3))) = commutator(multiply(Y3,commutator(X3,multiply(X2,X1))),X1),
inference(cp,[status(thm)],[t61149,t7716]) ).
cnf(t111650,plain,
commutator(multiply(Y3,commutator(X3,X2)),X1) = commutator(multiply(Y3,commutator(X3,multiply(X2,X1))),X1),
inference(step,[status(thm)],[t61154,t7716]) ).
cnf(t67954,plain,
commutator(multiply(X1,commutator(X2,multiply(X3,Y3))),Y3) = commutator(multiply(X1,commutator(X2,X3)),Y3),
inference(orient,[status(thm)],[t111650]) ).
cnf(t111973,plain,
commutator(multiply(X1,commutator(X1,X2)),X3) = multiply(multiply(X1,commutator(X1,multiply(X2,X3))),multiply(X3,inverse(multiply(X1,multiply(commutator(X1,X2),X3))))),
inference(step,[status(thm)],[t101314,t67954]) ).
cnf(t12113,plain,
commutator(multiply(X1,multiply(X2,inverse(multiply(X2,X3)))),X3) = commutator(multiply(X1,commutator(X3,X2)),X3),
inference(cp,[status(thm)],[t12090,t2037]) ).
cnf(t111073,plain,
commutator(multiply(X1,multiply(X2,inverse(multiply(X2,X3)))),X3) = commutator(X1,X3),
inference(step,[status(thm)],[t12113,t10907]) ).
cnf(t17467,plain,
commutator(multiply(X1,multiply(X2,inverse(multiply(X2,X3)))),X3) = commutator(X1,X3),
inference(orient,[status(thm)],[t111073]) ).
cnf(t17506,plain,
commutator(X1,inverse(multiply(X2,X3))) = commutator(multiply(X1,multiply(X3,inverse(inverse(X2)))),inverse(multiply(X2,X3))),
inference(cp,[status(thm)],[t17467,t99]) ).
cnf(t111074,plain,
commutator(multiply(X2,X3),X1) = commutator(multiply(X1,multiply(X3,inverse(inverse(X2)))),inverse(multiply(X2,X3))),
inference(step,[status(thm)],[t17506,t2133]) ).
cnf(t111075,plain,
commutator(multiply(X2,X3),X1) = commutator(multiply(X2,X3),multiply(X1,multiply(X3,inverse(inverse(X2))))),
inference(step,[status(thm)],[t111074,t2133]) ).
cnf(t111076,plain,
commutator(multiply(X2,X3),X1) = commutator(multiply(X2,X3),multiply(X1,multiply(X3,X2))),
inference(step,[status(thm)],[t111075,t59]) ).
cnf(t17603,plain,
commutator(multiply(X1,X2),multiply(X3,multiply(X2,X1))) = commutator(multiply(X1,X2),X3),
inference(orient,[status(thm)],[t111076]) ).
cnf(t17692,plain,
commutator(multiply(X1,multiply(X2,X3)),multiply(X3,X2)) = inverse(commutator(multiply(X3,X2),X1)),
inference(cp,[status(thm)],[t201,t17603]) ).
cnf(t111080,plain,
commutator(multiply(X1,multiply(X2,X3)),multiply(X3,X2)) = commutator(X1,multiply(X3,X2)),
inference(step,[status(thm)],[t17692,t201]) ).
cnf(t17901,plain,
commutator(multiply(X1,multiply(X2,X3)),multiply(X3,X2)) = commutator(X1,multiply(X3,X2)),
inference(orient,[status(thm)],[t111080]) ).
cnf(t17937,plain,
commutator(X1,multiply(inverse(X2),inverse(X3))) = commutator(multiply(X1,inverse(multiply(X2,X3))),multiply(inverse(X2),inverse(X3))),
inference(cp,[status(thm)],[t17901,t108]) ).
cnf(t111720,plain,
commutator(X1,inverse(multiply(X3,X2))) = commutator(multiply(X1,inverse(multiply(X2,X3))),multiply(inverse(X2),inverse(X3))),
inference(step,[status(thm)],[t17937,t108]) ).
cnf(t111721,plain,
commutator(multiply(X3,X2),X1) = commutator(multiply(X1,inverse(multiply(X2,X3))),multiply(inverse(X2),inverse(X3))),
inference(step,[status(thm)],[t111720,t2133]) ).
cnf(t111722,plain,
commutator(multiply(X3,X2),X1) = commutator(multiply(inverse(X2),inverse(X3)),multiply(multiply(X2,X3),inverse(X1))),
inference(step,[status(thm)],[t111721,t23137]) ).
cnf(t111723,plain,
commutator(multiply(X3,X2),X1) = commutator(inverse(multiply(X3,X2)),multiply(multiply(X2,X3),inverse(X1))),
inference(step,[status(thm)],[t111722,t108]) ).
cnf(t111724,plain,
commutator(multiply(X3,X2),X1) = commutator(multiply(multiply(X2,X3),inverse(X1)),multiply(X3,X2)),
inference(step,[status(thm)],[t111723,t2100]) ).
cnf(t111725,plain,
commutator(multiply(X3,X2),X1) = commutator(multiply(X3,X2),multiply(X1,inverse(multiply(X2,X3)))),
inference(step,[status(thm)],[t111724,t23137]) ).
cnf(t76283,plain,
commutator(multiply(X1,X2),multiply(X3,inverse(multiply(X2,X1)))) = commutator(multiply(X1,X2),X3),
inference(orient,[status(thm)],[t111725]) ).
cnf(t102,plain,
inverse(multiply(X1,X2)) = multiply(X3,inverse(multiply(X1,multiply(X2,X3)))),
inference(cp,[status(thm)],[t99,t6]) ).
cnf(t3126,plain,
multiply(X1,inverse(multiply(X2,multiply(X3,X1)))) = inverse(multiply(X2,X3)),
inference(orient,[status(thm)],[t102]) ).
cnf(t76326,plain,
commutator(multiply(multiply(X1,X2),X3),X2) = commutator(multiply(multiply(X1,X2),X3),inverse(multiply(X3,X1))),
inference(cp,[status(thm)],[t76283,t3126]) ).
cnf(t111726,plain,
commutator(multiply(X1,multiply(X2,X3)),X2) = commutator(multiply(multiply(X1,X2),X3),inverse(multiply(X3,X1))),
inference(step,[status(thm)],[t76326,t6]) ).
cnf(t111727,plain,
commutator(multiply(X1,X3),X2) = commutator(multiply(multiply(X1,X2),X3),inverse(multiply(X3,X1))),
inference(step,[status(thm)],[t111726,t12090]) ).
cnf(t111728,plain,
commutator(multiply(X1,X3),X2) = commutator(multiply(X3,X1),multiply(multiply(X1,X2),X3)),
inference(step,[status(thm)],[t111727,t2133]) ).
cnf(t111729,plain,
commutator(multiply(X1,X3),X2) = commutator(multiply(X3,X1),multiply(X1,multiply(X2,X3))),
inference(step,[status(thm)],[t111728,t6]) ).
cnf(t76515,plain,
commutator(multiply(X1,X2),multiply(X2,multiply(X3,X1))) = commutator(multiply(X2,X1),X3),
inference(orient,[status(thm)],[t111729]) ).
cnf(t76527,plain,
commutator(multiply(multiply(inverse(X1),X2),X1),X3) = commutator(X2,multiply(multiply(inverse(X1),X2),multiply(X3,X1))),
inference(cp,[status(thm)],[t76515,t74]) ).
cnf(t111731,plain,
commutator(multiply(inverse(X1),multiply(X2,X1)),X3) = commutator(X2,multiply(multiply(inverse(X1),X2),multiply(X3,X1))),
inference(step,[status(thm)],[t76527,t6]) ).
cnf(t111732,plain,
commutator(multiply(X2,commutator(X2,X1)),X3) = commutator(X2,multiply(multiply(inverse(X1),X2),multiply(X3,X1))),
inference(step,[status(thm)],[t111731,t7057]) ).
cnf(t111733,plain,
commutator(multiply(X2,commutator(X2,X1)),X3) = commutator(X2,multiply(inverse(X1),multiply(X2,multiply(X3,X1)))),
inference(step,[status(thm)],[t111732,t6]) ).
cnf(t111734,plain,
commutator(multiply(X2,commutator(X2,X1)),X3) = commutator(X2,multiply(inverse(X1),multiply(X3,X1))),
inference(step,[status(thm)],[t111733,t12205]) ).
cnf(t111735,plain,
commutator(multiply(X2,commutator(X2,X1)),X3) = commutator(X2,multiply(X3,commutator(X3,X1))),
inference(step,[status(thm)],[t111734,t7057]) ).
cnf(t77096,plain,
commutator(multiply(X1,commutator(X1,X2)),X3) = commutator(X1,multiply(X3,commutator(X3,X2))),
inference(orient,[status(thm)],[t111735]) ).
cnf(t111974,plain,
commutator(X1,multiply(X3,commutator(X3,X2))) = multiply(multiply(X1,commutator(X1,multiply(X2,X3))),multiply(X3,inverse(multiply(X1,multiply(commutator(X1,X2),X3))))),
inference(step,[status(thm)],[t111973,t77096]) ).
cnf(t111975,plain,
commutator(X1,multiply(X3,commutator(X3,X2))) = multiply(X1,multiply(commutator(X1,multiply(X2,X3)),multiply(X3,inverse(multiply(X1,multiply(commutator(X1,X2),X3)))))),
inference(step,[status(thm)],[t111974,t6]) ).
cnf(t111976,plain,
commutator(X1,multiply(X3,commutator(X3,X2))) = multiply(X1,multiply(commutator(X1,multiply(X2,X3)),inverse(multiply(X1,commutator(X1,X2))))),
inference(step,[status(thm)],[t111975,t3126]) ).
cnf(t111977,plain,
commutator(X1,multiply(X3,commutator(X3,X2))) = multiply(X1,multiply(commutator(X1,multiply(X2,X3)),multiply(commutator(X2,X1),inverse(X1)))),
inference(step,[status(thm)],[t111976,t1255]) ).
cnf(t111978,plain,
commutator(X1,multiply(X3,commutator(X3,X2))) = multiply(X1,multiply(commutator(X1,multiply(X2,X3)),multiply(inverse(X1),commutator(X2,X1)))),
inference(step,[status(thm)],[t111977,t1445]) ).
cnf(t1435,plain,
multiply(commutator(X1,X2),multiply(inverse(X1),X3)) = multiply(multiply(inverse(X1),commutator(X1,X2)),X3),
inference(cp,[status(thm)],[t6,t1421]) ).
cnf(t110959,plain,
multiply(commutator(X1,X2),multiply(inverse(X1),X3)) = multiply(inverse(X1),multiply(commutator(X1,X2),X3)),
inference(step,[status(thm)],[t1435,t6]) ).
cnf(t9811,plain,
multiply(commutator(X1,X2),multiply(inverse(X1),X3)) = multiply(inverse(X1),multiply(commutator(X1,X2),X3)),
inference(orient,[status(thm)],[t110959]) ).
cnf(t111979,plain,
commutator(X1,multiply(X3,commutator(X3,X2))) = multiply(X1,multiply(inverse(X1),multiply(commutator(X1,multiply(X2,X3)),commutator(X2,X1)))),
inference(step,[status(thm)],[t111978,t9811]) ).
cnf(t111980,plain,
commutator(X1,multiply(X3,commutator(X3,X2))) = multiply(commutator(X1,multiply(X2,X3)),commutator(X2,X1)),
inference(step,[status(thm)],[t111979,t74]) ).
cnf(t103321,plain,
commutator(X1,multiply(X2,commutator(X2,X3))) = multiply(commutator(X1,multiply(X3,X2)),commutator(X3,X1)),
inference(orient,[status(thm)],[t111980]) ).
cnf(t607,plain,
inverse(multiply(X1,commutator(X1,X2))) = multiply(inverse(multiply(X1,X2)),X2),
inference(cp,[status(thm)],[t140,t556]) ).
cnf(t111201,plain,
multiply(commutator(X2,X1),inverse(X1)) = multiply(inverse(multiply(X1,X2)),X2),
inference(step,[status(thm)],[t607,t1255]) ).
cnf(t111202,plain,
multiply(inverse(X1),commutator(X2,X1)) = multiply(inverse(multiply(X1,X2)),X2),
inference(step,[status(thm)],[t111201,t1445]) ).
cnf(t22489,plain,
multiply(inverse(X1),commutator(X2,X1)) = multiply(inverse(multiply(X1,X2)),X2),
inference(orient,[status(thm)],[t111202]) ).
cnf(t209,plain,
identity = multiply(commutator(X1,X2),commutator(X2,X1)),
inference(cp,[status(thm)],[t68,t201]) ).
cnf(t330,plain,
multiply(commutator(X1,X2),commutator(X2,X1)) = identity,
inference(orient,[status(thm)],[t209]) ).
cnf(t331,plain,
identity = multiply(commutator(X1,commutator(X2,X3)),commutator(X3,commutator(X1,X2))),
inference(cp,[status(thm)],[t330,t15]) ).
cnf(t2169,plain,
commutator(multiply(X1,X2),commutator(X2,X3)) = commutator(commutator(X1,X2),X3),
inference(cp,[status(thm)],[t15,t2153]) ).
cnf(t110786,plain,
commutator(multiply(X1,X2),commutator(X2,X3)) = commutator(X1,commutator(X2,X3)),
inference(step,[status(thm)],[t2169,t15]) ).
cnf(t2299,plain,
commutator(multiply(X1,X2),commutator(X2,X3)) = commutator(X1,commutator(X2,X3)),
inference(orient,[status(thm)],[t110786]) ).
cnf(t2331,plain,
commutator(commutator(X1,X2),multiply(X3,X1)) = inverse(commutator(X3,commutator(X1,X2))),
inference(cp,[status(thm)],[t201,t2299]) ).
cnf(t110801,plain,
commutator(X1,commutator(X2,multiply(X3,X1))) = inverse(commutator(X3,commutator(X1,X2))),
inference(step,[status(thm)],[t2331,t15]) ).
cnf(t2306,plain,
commutator(X1,commutator(inverse(multiply(X2,X1)),X3)) = commutator(inverse(X2),commutator(inverse(multiply(X2,X1)),X3)),
inference(cp,[status(thm)],[t2299,t99]) ).
cnf(t110788,plain,
commutator(X1,commutator(X3,multiply(X2,X1))) = commutator(inverse(X2),commutator(inverse(multiply(X2,X1)),X3)),
inference(step,[status(thm)],[t2306,t2100]) ).
cnf(t110789,plain,
commutator(X1,commutator(X3,multiply(X2,X1))) = commutator(commutator(inverse(multiply(X2,X1)),X3),X2),
inference(step,[status(thm)],[t110788,t2100]) ).
cnf(t110790,plain,
commutator(X1,commutator(X3,multiply(X2,X1))) = commutator(inverse(multiply(X2,X1)),commutator(X3,X2)),
inference(step,[status(thm)],[t110789,t15]) ).
cnf(t110791,plain,
commutator(X1,commutator(X3,multiply(X2,X1))) = commutator(commutator(X3,X2),multiply(X2,X1)),
inference(step,[status(thm)],[t110790,t2100]) ).
cnf(t110792,plain,
commutator(X1,commutator(X3,multiply(X2,X1))) = commutator(X3,commutator(X2,multiply(X2,X1))),
inference(step,[status(thm)],[t110791,t15]) ).
cnf(t110793,plain,
commutator(X1,commutator(X3,multiply(X2,X1))) = commutator(X3,commutator(X2,X1)),
inference(step,[status(thm)],[t110792,t271]) ).
cnf(t2432,plain,
commutator(X1,commutator(X2,multiply(X3,X1))) = commutator(X2,commutator(X3,X1)),
inference(orient,[status(thm)],[t110793]) ).
cnf(t2310,plain,
commutator(inverse(X1),commutator(multiply(X1,X2),X3)) = commutator(X2,commutator(multiply(X1,X2),X3)),
inference(cp,[status(thm)],[t2299,t17]) ).
cnf(t110794,plain,
commutator(commutator(multiply(X1,X2),X3),X1) = commutator(X2,commutator(multiply(X1,X2),X3)),
inference(step,[status(thm)],[t2310,t2100]) ).
cnf(t110795,plain,
commutator(multiply(X1,X2),commutator(X3,X1)) = commutator(X2,commutator(multiply(X1,X2),X3)),
inference(step,[status(thm)],[t110794,t15]) ).
cnf(t283,plain,
commutator(X1,commutator(multiply(X1,X2),X3)) = commutator(commutator(X1,X2),X3),
inference(cp,[status(thm)],[t15,t271]) ).
cnf(t110731,plain,
commutator(X1,commutator(multiply(X1,X2),X3)) = commutator(X1,commutator(X2,X3)),
inference(step,[status(thm)],[t283,t15]) ).
cnf(t1649,plain,
commutator(X1,commutator(multiply(X1,X2),X3)) = commutator(X1,commutator(X2,X3)),
inference(orient,[status(thm)],[t110731]) ).
cnf(t1695,plain,
commutator(commutator(multiply(X1,X2),X3),X1) = inverse(commutator(X1,commutator(X2,X3))),
inference(cp,[status(thm)],[t201,t1649]) ).
cnf(t110735,plain,
commutator(multiply(X1,X2),commutator(X3,X1)) = inverse(commutator(X1,commutator(X2,X3))),
inference(step,[status(thm)],[t1695,t15]) ).
cnf(t110736,plain,
commutator(multiply(X1,X2),commutator(X3,X1)) = commutator(commutator(X2,X3),X1),
inference(step,[status(thm)],[t110735,t201]) ).
cnf(t110737,plain,
commutator(multiply(X1,X2),commutator(X3,X1)) = commutator(X2,commutator(X3,X1)),
inference(step,[status(thm)],[t110736,t15]) ).
cnf(t1891,plain,
commutator(multiply(X1,X2),commutator(X3,X1)) = commutator(X2,commutator(X3,X1)),
inference(orient,[status(thm)],[t110737]) ).
cnf(t110796,plain,
commutator(X2,commutator(X3,X1)) = commutator(X2,commutator(multiply(X1,X2),X3)),
inference(step,[status(thm)],[t110795,t1891]) ).
cnf(t277,plain,
commutator(inverse(X1),inverse(X2)) = commutator(inverse(X1),inverse(multiply(X2,X1))),
inference(cp,[status(thm)],[t271,t108]) ).
cnf(t1619,plain,
commutator(inverse(X1),inverse(multiply(X2,X1))) = commutator(inverse(X1),inverse(X2)),
inference(orient,[status(thm)],[t277]) ).
cnf(t2130,plain,
commutator(X1,multiply(X2,X1)) = commutator(X1,X2),
inference(rw,[status(thm)],[t1619]) ).
cnf(t2179,plain,
commutator(X1,multiply(X2,X1)) = commutator(X1,X2),
inference(orient,[status(thm)],[t2130]) ).
cnf(t2190,plain,
commutator(X1,commutator(multiply(X2,X1),X3)) = commutator(commutator(X1,X2),X3),
inference(cp,[status(thm)],[t15,t2179]) ).
cnf(t110787,plain,
commutator(X1,commutator(multiply(X2,X1),X3)) = commutator(X1,commutator(X2,X3)),
inference(step,[status(thm)],[t2190,t15]) ).
cnf(t2381,plain,
commutator(X1,commutator(multiply(X2,X1),X3)) = commutator(X1,commutator(X2,X3)),
inference(orient,[status(thm)],[t110787]) ).
cnf(t110797,plain,
commutator(X2,commutator(X3,X1)) = commutator(X2,commutator(X1,X3)),
inference(step,[status(thm)],[t110796,t2381]) ).
cnf(t2489,plain,
commutator(X1,commutator(X2,X3)) = commutator(X1,commutator(X3,X2)),
inference(orient,[status(thm)],[t110797]) ).
cnf(t110798,plain,
commutator(X1,commutator(X2,multiply(X3,X1))) = commutator(X2,commutator(X1,X3)),
inference(step,[status(thm)],[t2432,t2489]) ).
cnf(t2490,plain,
commutator(X1,commutator(X2,multiply(X3,X1))) = commutator(X2,commutator(X1,X3)),
inference(orient,[status(thm)],[t110798]) ).
cnf(t110802,plain,
commutator(X2,commutator(X1,X3)) = inverse(commutator(X3,commutator(X1,X2))),
inference(step,[status(thm)],[t110801,t2490]) ).
cnf(t110803,plain,
commutator(X2,commutator(X1,X3)) = commutator(commutator(X1,X2),X3),
inference(step,[status(thm)],[t110802,t201]) ).
cnf(t110804,plain,
commutator(X2,commutator(X1,X3)) = commutator(X1,commutator(X2,X3)),
inference(step,[status(thm)],[t110803,t15]) ).
cnf(t2594,plain,
commutator(X1,commutator(X2,X3)) = commutator(X2,commutator(X1,X3)),
inference(orient,[status(thm)],[t110804]) ).
cnf(t111185,plain,
identity = multiply(commutator(X1,commutator(X2,X3)),commutator(X1,commutator(X3,X2))),
inference(step,[status(thm)],[t331,t2594]) ).
cnf(t111186,plain,
identity = multiply(commutator(X1,commutator(X2,X3)),commutator(X1,commutator(X2,X3))),
inference(step,[status(thm)],[t111185,t2489]) ).
cnf(t21359,plain,
multiply(commutator(X1,commutator(X2,X3)),commutator(X1,commutator(X2,X3))) = identity,
inference(orient,[status(thm)],[t111186]) ).
cnf(t2196,plain,
multiply(X1,multiply(X2,X1)) = multiply(multiply(X2,X1),multiply(X1,commutator(X1,X2))),
inference(cp,[status(thm)],[t556,t2179]) ).
cnf(t110943,plain,
multiply(X1,multiply(X2,X1)) = multiply(X2,multiply(X1,multiply(X1,commutator(X1,X2)))),
inference(step,[status(thm)],[t2196,t6]) ).
cnf(t8809,plain,
multiply(X1,multiply(X2,multiply(X2,commutator(X2,X1)))) = multiply(X2,multiply(X1,X2)),
inference(orient,[status(thm)],[t110943]) ).
cnf(t28332,plain,
multiply(commutator(multiply(X1,multiply(X1,commutator(X1,X2))),X2),X3) = multiply(inverse(multiply(X1,multiply(X2,X1))),multiply(multiply(X1,multiply(X1,commutator(X1,X2))),multiply(X2,X3))),
inference(cp,[status(thm)],[t28323,t8809]) ).
cnf(t10267,plain,
commutator(X1,multiply(commutator(X2,X1),X3)) = inverse(commutator(X3,X1)),
inference(cp,[status(thm)],[t201,t10189]) ).
cnf(t110971,plain,
commutator(X1,multiply(commutator(X2,X1),X3)) = commutator(X1,X3),
inference(step,[status(thm)],[t10267,t201]) ).
cnf(t10727,plain,
commutator(X1,multiply(commutator(X2,X1),X3)) = commutator(X1,X3),
inference(orient,[status(thm)],[t110971]) ).
cnf(t10747,plain,
commutator(X1,inverse(multiply(X2,multiply(X3,commutator(Y3,X1))))) = commutator(X1,inverse(multiply(X2,X3))),
inference(cp,[status(thm)],[t10727,t3126]) ).
cnf(t111039,plain,
commutator(multiply(X2,multiply(X3,commutator(Y3,X1))),X1) = commutator(X1,inverse(multiply(X2,X3))),
inference(step,[status(thm)],[t10747,t2133]) ).
cnf(t111040,plain,
commutator(multiply(X2,multiply(X3,commutator(Y3,X1))),X1) = commutator(multiply(X2,X3),X1),
inference(step,[status(thm)],[t111039,t2133]) ).
cnf(t15605,plain,
commutator(multiply(X1,multiply(X2,commutator(X3,Y3))),Y3) = commutator(multiply(X1,X2),Y3),
inference(orient,[status(thm)],[t111040]) ).
cnf(t111344,plain,
multiply(commutator(multiply(X1,X1),X2),X3) = multiply(inverse(multiply(X1,multiply(X2,X1))),multiply(multiply(X1,multiply(X1,commutator(X1,X2))),multiply(X2,X3))),
inference(step,[status(thm)],[t28332,t15605]) ).
cnf(t111345,plain,
multiply(commutator(multiply(X1,X1),X2),X3) = multiply(inverse(multiply(X1,multiply(X2,X1))),multiply(X1,multiply(multiply(X1,commutator(X1,X2)),multiply(X2,X3)))),
inference(step,[status(thm)],[t111344,t6]) ).
cnf(t111346,plain,
multiply(commutator(multiply(X1,X1),X2),X3) = multiply(inverse(multiply(X2,X1)),multiply(multiply(X1,commutator(X1,X2)),multiply(X2,X3))),
inference(step,[status(thm)],[t111345,t3226]) ).
cnf(t111347,plain,
multiply(commutator(multiply(X1,X1),X2),X3) = multiply(inverse(multiply(X2,X1)),multiply(X1,multiply(commutator(X1,X2),multiply(X2,X3)))),
inference(step,[status(thm)],[t111346,t6]) ).
cnf(t111348,plain,
multiply(commutator(multiply(X1,X1),X2),X3) = multiply(inverse(multiply(X2,X1)),multiply(X1,multiply(X2,multiply(commutator(X1,X2),X3)))),
inference(step,[status(thm)],[t111347,t3769]) ).
cnf(t111349,plain,
multiply(commutator(multiply(X1,X1),X2),X3) = multiply(commutator(X1,X2),multiply(commutator(X1,X2),X3)),
inference(step,[status(thm)],[t111348,t28323]) ).
cnf(t29659,plain,
multiply(commutator(X1,X2),multiply(commutator(X1,X2),X3)) = multiply(commutator(multiply(X1,X1),X2),X3),
inference(orient,[status(thm)],[t111349]) ).
cnf(t29786,plain,
multiply(commutator(multiply(X1,X1),X2),identity) = multiply(commutator(X1,X2),commutator(X1,X2)),
inference(cp,[status(thm)],[t29659,t57]) ).
cnf(t111350,plain,
commutator(multiply(X1,X1),X2) = multiply(commutator(X1,X2),commutator(X1,X2)),
inference(step,[status(thm)],[t29786,t57]) ).
cnf(t30034,plain,
multiply(commutator(X1,X2),commutator(X1,X2)) = commutator(multiply(X1,X1),X2),
inference(orient,[status(thm)],[t111350]) ).
cnf(t111351,plain,
commutator(multiply(X1,X1),commutator(X2,X3)) = identity,
inference(step,[status(thm)],[t21359,t30034]) ).
cnf(t30352,plain,
commutator(multiply(X1,X1),commutator(X2,X3)) = identity,
inference(rw,[status(thm)],[t111351]) ).
cnf(t111352,plain,
commutator(X2,commutator(multiply(X1,X1),X3)) = identity,
inference(step,[status(thm)],[t30352,t2594]) ).
cnf(t111353,plain,
commutator(X2,commutator(X3,multiply(X1,X1))) = identity,
inference(step,[status(thm)],[t111352,t2489]) ).
cnf(t30353,plain,
commutator(X1,commutator(X2,multiply(X3,X3))) = identity,
inference(orient,[status(thm)],[t111353]) ).
cnf(t30415,plain,
multiply(inverse(multiply(commutator(X1,multiply(X2,X2)),X3)),X3) = multiply(inverse(commutator(X1,multiply(X2,X2))),identity),
inference(cp,[status(thm)],[t22489,t30353]) ).
cnf(t111763,plain,
multiply(multiply(inverse(X3),commutator(multiply(X2,X2),X1)),X3) = multiply(inverse(commutator(X1,multiply(X2,X2))),identity),
inference(step,[status(thm)],[t30415,t1321]) ).
cnf(t111764,plain,
multiply(inverse(X3),multiply(commutator(multiply(X2,X2),X1),X3)) = multiply(inverse(commutator(X1,multiply(X2,X2))),identity),
inference(step,[status(thm)],[t111763,t6]) ).
cnf(t30018,plain,
inverse(multiply(commutator(X1,X2),commutator(X1,X2))) = multiply(X3,inverse(multiply(commutator(multiply(X1,X1),X2),X3))),
inference(cp,[status(thm)],[t3126,t29659]) ).
cnf(t111354,plain,
multiply(inverse(commutator(X1,X2)),commutator(X2,X1)) = multiply(X3,inverse(multiply(commutator(multiply(X1,X1),X2),X3))),
inference(step,[status(thm)],[t30018,t1321]) ).
cnf(t111355,plain,
multiply(commutator(X2,X1),commutator(X2,X1)) = multiply(X3,inverse(multiply(commutator(multiply(X1,X1),X2),X3))),
inference(step,[status(thm)],[t111354,t201]) ).
cnf(t111356,plain,
commutator(multiply(X2,X2),X1) = multiply(X3,inverse(multiply(commutator(multiply(X1,X1),X2),X3))),
inference(step,[status(thm)],[t111355,t30034]) ).
cnf(t111357,plain,
commutator(multiply(X2,X2),X1) = inverse(commutator(multiply(X1,X1),X2)),
inference(step,[status(thm)],[t111356,t99]) ).
cnf(t111358,plain,
commutator(multiply(X2,X2),X1) = commutator(X2,multiply(X1,X1)),
inference(step,[status(thm)],[t111357,t201]) ).
cnf(t30418,plain,
commutator(multiply(X1,X1),X2) = commutator(X1,multiply(X2,X2)),
inference(orient,[status(thm)],[t111358]) ).
cnf(t111765,plain,
multiply(inverse(X3),multiply(commutator(X2,multiply(X1,X1)),X3)) = multiply(inverse(commutator(X1,multiply(X2,X2))),identity),
inference(step,[status(thm)],[t111764,t30418]) ).
cnf(t111766,plain,
multiply(inverse(X3),multiply(commutator(X2,multiply(X1,X1)),X3)) = inverse(commutator(X1,multiply(X2,X2))),
inference(step,[status(thm)],[t111765,t57]) ).
cnf(t111767,plain,
multiply(inverse(X3),multiply(commutator(X2,multiply(X1,X1)),X3)) = commutator(multiply(X2,X2),X1),
inference(step,[status(thm)],[t111766,t201]) ).
cnf(t111768,plain,
multiply(inverse(X3),multiply(commutator(X2,multiply(X1,X1)),X3)) = commutator(X2,multiply(X1,X1)),
inference(step,[status(thm)],[t111767,t30418]) ).
cnf(t80559,plain,
multiply(inverse(X1),multiply(commutator(X2,multiply(X3,X3)),X1)) = commutator(X2,multiply(X3,X3)),
inference(orient,[status(thm)],[t111768]) ).
cnf(t103943,plain,
commutator(X1,multiply(multiply(commutator(X2,multiply(X3,X3)),Y3),commutator(multiply(commutator(X2,multiply(X3,X3)),Y3),inverse(Y3)))) = multiply(commutator(X1,commutator(X2,multiply(X3,X3))),commutator(inverse(Y3),X1)),
inference(cp,[status(thm)],[t103321,t80559]) ).
cnf(t111981,plain,
commutator(X1,multiply(commutator(X2,multiply(X3,X3)),multiply(Y3,commutator(multiply(commutator(X2,multiply(X3,X3)),Y3),inverse(Y3))))) = multiply(commutator(X1,commutator(X2,multiply(X3,X3))),commutator(inverse(Y3),X1)),
inference(step,[status(thm)],[t103943,t6]) ).
cnf(t111982,plain,
commutator(X1,multiply(commutator(X2,multiply(X3,X3)),multiply(Y3,commutator(Y3,multiply(commutator(X2,multiply(X3,X3)),Y3))))) = multiply(commutator(X1,commutator(X2,multiply(X3,X3))),commutator(inverse(Y3),X1)),
inference(step,[status(thm)],[t111981,t2133]) ).
cnf(t111983,plain,
commutator(X1,multiply(commutator(X2,multiply(X3,X3)),multiply(Y3,commutator(Y3,commutator(X2,multiply(X3,X3)))))) = multiply(commutator(X1,commutator(X2,multiply(X3,X3))),commutator(inverse(Y3),X1)),
inference(step,[status(thm)],[t111982,t2179]) ).
cnf(t111984,plain,
commutator(X1,multiply(commutator(X2,multiply(X3,X3)),multiply(Y3,identity))) = multiply(commutator(X1,commutator(X2,multiply(X3,X3))),commutator(inverse(Y3),X1)),
inference(step,[status(thm)],[t111983,t30353]) ).
cnf(t111985,plain,
commutator(X1,multiply(commutator(X2,multiply(X3,X3)),Y3)) = multiply(commutator(X1,commutator(X2,multiply(X3,X3))),commutator(inverse(Y3),X1)),
inference(step,[status(thm)],[t111984,t57]) ).
cnf(t111986,plain,
commutator(X1,multiply(commutator(X2,multiply(X3,X3)),Y3)) = multiply(identity,commutator(inverse(Y3),X1)),
inference(step,[status(thm)],[t111985,t30353]) ).
cnf(t111987,plain,
commutator(X1,multiply(commutator(X2,multiply(X3,X3)),Y3)) = commutator(inverse(Y3),X1),
inference(step,[status(thm)],[t111986,t5]) ).
cnf(t111988,plain,
commutator(X1,multiply(commutator(X2,multiply(X3,X3)),Y3)) = commutator(X1,Y3),
inference(step,[status(thm)],[t111987,t2100]) ).
cnf(t104417,plain,
commutator(X1,multiply(commutator(X2,multiply(X3,X3)),Y3)) = commutator(X1,Y3),
inference(orient,[status(thm)],[t111988]) ).
cnf(t97233,plain,
multiply(commutator(X1,multiply(multiply(X2,X1),X3)),multiply(X2,X1)) = multiply(multiply(X2,X1),multiply(commutator(X1,X2),commutator(X1,X3))),
inference(cp,[status(thm)],[t97182,t2179]) ).
cnf(t111947,plain,
multiply(commutator(X1,multiply(X2,multiply(X1,X3))),multiply(X2,X1)) = multiply(multiply(X2,X1),multiply(commutator(X1,X2),commutator(X1,X3))),
inference(step,[status(thm)],[t97233,t6]) ).
cnf(t111948,plain,
multiply(commutator(X1,multiply(X2,X3)),multiply(X2,X1)) = multiply(multiply(X2,X1),multiply(commutator(X1,X2),commutator(X1,X3))),
inference(step,[status(thm)],[t111947,t12205]) ).
cnf(t111949,plain,
multiply(commutator(X1,multiply(X2,X3)),multiply(X2,X1)) = multiply(X2,multiply(X1,multiply(commutator(X1,X2),commutator(X1,X3)))),
inference(step,[status(thm)],[t111948,t6]) ).
cnf(t111950,plain,
multiply(commutator(X1,multiply(X2,X3)),multiply(X2,X1)) = multiply(X1,multiply(X2,commutator(X1,X3))),
inference(step,[status(thm)],[t111949,t8494]) ).
cnf(t97897,plain,
multiply(commutator(X1,multiply(X2,X3)),multiply(X2,X1)) = multiply(X1,multiply(X2,commutator(X1,X3))),
inference(orient,[status(thm)],[t111950]) ).
cnf(t104522,plain,
commutator(X1,multiply(X2,X3)) = commutator(X1,multiply(X3,multiply(X2,commutator(X3,X2)))),
inference(cp,[status(thm)],[t104417,t97897]) ).
cnf(t105952,plain,
commutator(X1,multiply(X2,multiply(X3,commutator(X2,X3)))) = commutator(X1,multiply(X3,X2)),
inference(orient,[status(thm)],[t104522]) ).
cnf(t106420,plain,
commutator(X1,multiply(multiply(X2,commutator(X3,X2)),commutator(multiply(X2,commutator(X3,X2)),X3))) = multiply(commutator(X1,multiply(X2,X3)),commutator(X3,X1)),
inference(cp,[status(thm)],[t103321,t105952]) ).
cnf(t111995,plain,
commutator(X1,multiply(X2,multiply(commutator(X3,X2),commutator(multiply(X2,commutator(X3,X2)),X3)))) = multiply(commutator(X1,multiply(X2,X3)),commutator(X3,X1)),
inference(step,[status(thm)],[t106420,t6]) ).
cnf(t111996,plain,
commutator(X1,multiply(X2,multiply(commutator(X3,X2),commutator(X2,X3)))) = multiply(commutator(X1,multiply(X2,X3)),commutator(X3,X1)),
inference(step,[status(thm)],[t111995,t10907]) ).
cnf(t111997,plain,
commutator(X1,multiply(X2,identity)) = multiply(commutator(X1,multiply(X2,X3)),commutator(X3,X1)),
inference(step,[status(thm)],[t111996,t330]) ).
cnf(t111998,plain,
commutator(X1,X2) = multiply(commutator(X1,multiply(X2,X3)),commutator(X3,X1)),
inference(step,[status(thm)],[t111997,t57]) ).
cnf(t191,plain,
commutator(multiply(X1,X2),X3) = multiply(inverse(multiply(X3,multiply(X1,X2))),multiply(X1,multiply(X2,X3))),
inference(cp,[status(thm)],[t174,t6]) ).
cnf(t73916,plain,
multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X2,multiply(X3,X1))) = commutator(multiply(X2,X3),X1),
inference(orient,[status(thm)],[t191]) ).
cnf(t100775,plain,
commutator(multiply(X1,commutator(multiply(X2,X3),X1)),X2) = multiply(inverse(multiply(X2,multiply(X1,commutator(multiply(X2,X3),X1)))),multiply(X2,multiply(X1,commutator(X3,X1)))),
inference(cp,[status(thm)],[t73916,t100334]) ).
cnf(t12107,plain,
commutator(multiply(inverse(X1),X2),inverse(X3)) = commutator(multiply(inverse(multiply(X3,X1)),X2),inverse(X3)),
inference(cp,[status(thm)],[t12090,t166]) ).
cnf(t111020,plain,
commutator(X3,multiply(inverse(X1),X2)) = commutator(multiply(inverse(multiply(X3,X1)),X2),inverse(X3)),
inference(step,[status(thm)],[t12107,t2133]) ).
cnf(t111021,plain,
commutator(X3,multiply(inverse(X1),X2)) = commutator(X3,multiply(inverse(multiply(X3,X1)),X2)),
inference(step,[status(thm)],[t111020,t2133]) ).
cnf(t12771,plain,
commutator(X1,multiply(inverse(multiply(X1,X2)),X3)) = commutator(X1,multiply(inverse(X2),X3)),
inference(orient,[status(thm)],[t111021]) ).
cnf(t39948,plain,
commutator(X1,multiply(inverse(X2),multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),multiply(X3,Y3)))) = commutator(X1,multiply(commutator(X3,inverse(multiply(X1,X2))),Y3)),
inference(cp,[status(thm)],[t12771,t39713]) ).
cnf(t111468,plain,
commutator(X1,multiply(inverse(multiply(multiply(inverse(multiply(X1,X2)),X3),X2)),multiply(X3,Y3))) = commutator(X1,multiply(commutator(X3,inverse(multiply(X1,X2))),Y3)),
inference(step,[status(thm)],[t39948,t166]) ).
cnf(t111469,plain,
commutator(X1,multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X3,X2))),multiply(X3,Y3))) = commutator(X1,multiply(commutator(X3,inverse(multiply(X1,X2))),Y3)),
inference(step,[status(thm)],[t111468,t6]) ).
cnf(t111470,plain,
commutator(X1,multiply(multiply(inverse(multiply(X3,X2)),multiply(X1,X2)),multiply(X3,Y3))) = commutator(X1,multiply(commutator(X3,inverse(multiply(X1,X2))),Y3)),
inference(step,[status(thm)],[t111469,t125]) ).
cnf(t111471,plain,
commutator(X1,multiply(inverse(multiply(X3,X2)),multiply(multiply(X1,X2),multiply(X3,Y3)))) = commutator(X1,multiply(commutator(X3,inverse(multiply(X1,X2))),Y3)),
inference(step,[status(thm)],[t111470,t6]) ).
cnf(t111472,plain,
commutator(X1,multiply(inverse(multiply(X3,X2)),multiply(X1,multiply(X2,multiply(X3,Y3))))) = commutator(X1,multiply(commutator(X3,inverse(multiply(X1,X2))),Y3)),
inference(step,[status(thm)],[t111471,t6]) ).
cnf(t111473,plain,
commutator(X1,multiply(inverse(multiply(X3,X2)),multiply(X2,multiply(X3,Y3)))) = commutator(X1,multiply(commutator(X3,inverse(multiply(X1,X2))),Y3)),
inference(step,[status(thm)],[t111472,t12205]) ).
cnf(t111474,plain,
commutator(X1,multiply(commutator(X2,X3),Y3)) = commutator(X1,multiply(commutator(X3,inverse(multiply(X1,X2))),Y3)),
inference(step,[status(thm)],[t111473,t28323]) ).
cnf(t111475,plain,
commutator(X1,multiply(commutator(X2,X3),Y3)) = commutator(X1,multiply(commutator(multiply(X1,X2),X3),Y3)),
inference(step,[status(thm)],[t111474,t2133]) ).
cnf(t39989,plain,
commutator(X1,multiply(commutator(multiply(X1,X2),X3),Y3)) = commutator(X1,multiply(commutator(X2,X3),Y3)),
inference(orient,[status(thm)],[t111475]) ).
cnf(t39990,plain,
commutator(X1,multiply(commutator(X2,X3),inverse(Y3))) = commutator(multiply(Y3,commutator(X3,multiply(X1,X2))),X1),
inference(cp,[status(thm)],[t39989,t7716]) ).
cnf(t111597,plain,
commutator(multiply(Y3,commutator(X3,X2)),X1) = commutator(multiply(Y3,commutator(X3,multiply(X1,X2))),X1),
inference(step,[status(thm)],[t39990,t7716]) ).
cnf(t63341,plain,
commutator(multiply(X1,commutator(X2,multiply(X3,Y3))),X3) = commutator(multiply(X1,commutator(X2,Y3)),X3),
inference(orient,[status(thm)],[t111597]) ).
cnf(t63445,plain,
commutator(multiply(X1,commutator(inverse(X2),X3)),Y3) = commutator(multiply(X1,commutator(multiply(Y3,X3),X2)),Y3),
inference(cp,[status(thm)],[t63341,t2100]) ).
cnf(t111677,plain,
commutator(multiply(X1,commutator(X3,X2)),Y3) = commutator(multiply(X1,commutator(multiply(Y3,X3),X2)),Y3),
inference(step,[status(thm)],[t63445,t2100]) ).
cnf(t70365,plain,
commutator(multiply(X1,commutator(multiply(X2,X3),Y3)),X2) = commutator(multiply(X1,commutator(X3,Y3)),X2),
inference(orient,[status(thm)],[t111677]) ).
cnf(t111964,plain,
commutator(multiply(X1,commutator(X3,X1)),X2) = multiply(inverse(multiply(X2,multiply(X1,commutator(multiply(X2,X3),X1)))),multiply(X2,multiply(X1,commutator(X3,X1)))),
inference(step,[status(thm)],[t100775,t70365]) ).
cnf(t76562,plain,
commutator(multiply(multiply(X1,X2),inverse(X1)),X3) = commutator(X2,multiply(multiply(X1,X2),multiply(X3,inverse(X1)))),
inference(cp,[status(thm)],[t76515,t17]) ).
cnf(t111754,plain,
commutator(multiply(X1,multiply(X2,inverse(X1))),X3) = commutator(X2,multiply(multiply(X1,X2),multiply(X3,inverse(X1)))),
inference(step,[status(thm)],[t76562,t6]) ).
cnf(t111755,plain,
commutator(multiply(X1,multiply(X2,inverse(X1))),X3) = commutator(X2,multiply(X1,multiply(X2,multiply(X3,inverse(X1))))),
inference(step,[status(thm)],[t111754,t6]) ).
cnf(t111756,plain,
commutator(multiply(X1,multiply(X2,inverse(X1))),X3) = commutator(X2,multiply(X1,multiply(X3,inverse(X1)))),
inference(step,[status(thm)],[t111755,t12205]) ).
cnf(t111757,plain,
commutator(multiply(X2,commutator(X1,X2)),X3) = commutator(X2,multiply(X1,multiply(X3,inverse(X1)))),
inference(step,[status(thm)],[t111756,t7234]) ).
cnf(t111758,plain,
commutator(multiply(X2,commutator(X1,X2)),X3) = commutator(X2,multiply(X3,commutator(X1,X3))),
inference(step,[status(thm)],[t111757,t7234]) ).
cnf(t79708,plain,
commutator(multiply(X1,commutator(X2,X1)),X3) = commutator(X1,multiply(X3,commutator(X2,X3))),
inference(orient,[status(thm)],[t111758]) ).
cnf(t111965,plain,
commutator(X1,multiply(X2,commutator(X3,X2))) = multiply(inverse(multiply(X2,multiply(X1,commutator(multiply(X2,X3),X1)))),multiply(X2,multiply(X1,commutator(X3,X1)))),
inference(step,[status(thm)],[t111964,t79708]) ).
cnf(t111966,plain,
commutator(X1,multiply(X2,commutator(X3,X2))) = multiply(inverse(multiply(X1,commutator(multiply(X2,X3),X1))),multiply(X1,commutator(X3,X1))),
inference(step,[status(thm)],[t111965,t3226]) ).
cnf(t111967,plain,
commutator(X1,multiply(X2,commutator(X3,X2))) = multiply(inverse(commutator(multiply(X2,X3),X1)),commutator(X3,X1)),
inference(step,[status(thm)],[t111966,t3226]) ).
cnf(t111968,plain,
commutator(X1,multiply(X2,commutator(X3,X2))) = multiply(commutator(X1,multiply(X2,X3)),commutator(X3,X1)),
inference(step,[status(thm)],[t111967,t201]) ).
cnf(t101451,plain,
commutator(X1,multiply(X2,commutator(X3,X2))) = multiply(commutator(X1,multiply(X2,X3)),commutator(X3,X1)),
inference(orient,[status(thm)],[t111968]) ).
cnf(t111999,plain,
commutator(X1,X2) = commutator(X1,multiply(X2,commutator(X3,X2))),
inference(step,[status(thm)],[t111998,t101451]) ).
cnf(t106435,plain,
commutator(X1,multiply(X2,commutator(X3,X2))) = commutator(X1,X2),
inference(orient,[status(thm)],[t111999]) ).
cnf(t106769,plain,
commutator(X1,multiply(commutator(X2,X3),commutator(commutator(X2,X3),X3))) = multiply(commutator(X1,X3),commutator(X3,X1)),
inference(cp,[status(thm)],[t103321,t106435]) ).
cnf(t112015,plain,
commutator(X1,multiply(commutator(X2,X3),commutator(X2,commutator(X3,X3)))) = multiply(commutator(X1,X3),commutator(X3,X1)),
inference(step,[status(thm)],[t106769,t15]) ).
cnf(t112016,plain,
commutator(X1,multiply(commutator(X2,X3),commutator(X2,identity))) = multiply(commutator(X1,X3),commutator(X3,X1)),
inference(step,[status(thm)],[t112015,t26]) ).
cnf(t33,plain,
commutator(X1,identity) = multiply(inverse(X1),multiply(X1,identity)),
inference(cp,[status(thm)],[t9,t31]) ).
cnf(t110653,plain,
commutator(X1,identity) = identity,
inference(step,[status(thm)],[t33,t17]) ).
cnf(t35,plain,
commutator(X1,identity) = identity,
inference(orient,[status(thm)],[t110653]) ).
cnf(t112017,plain,
commutator(X1,multiply(commutator(X2,X3),identity)) = multiply(commutator(X1,X3),commutator(X3,X1)),
inference(step,[status(thm)],[t112016,t35]) ).
cnf(t112018,plain,
commutator(X1,commutator(X2,X3)) = multiply(commutator(X1,X3),commutator(X3,X1)),
inference(step,[status(thm)],[t112017,t57]) ).
cnf(t112019,plain,
commutator(X1,commutator(X2,X3)) = identity,
inference(step,[status(thm)],[t112018,t330]) ).
cnf(t106784,plain,
commutator(X1,commutator(X2,X3)) = identity,
inference(orient,[status(thm)],[t112019]) ).
cnf(t106800,plain,
multiply(inverse(commutator(X1,X2)),X3) = multiply(X3,multiply(inverse(commutator(X1,X2)),identity)),
inference(cp,[status(thm)],[t3404,t106784]) ).
cnf(t112107,plain,
multiply(commutator(X2,X1),X3) = multiply(X3,multiply(inverse(commutator(X1,X2)),identity)),
inference(step,[status(thm)],[t106800,t201]) ).
cnf(t112108,plain,
multiply(commutator(X2,X1),X3) = multiply(X3,inverse(commutator(X1,X2))),
inference(step,[status(thm)],[t112107,t57]) ).
cnf(t112109,plain,
multiply(commutator(X2,X1),X3) = multiply(X3,commutator(X2,X1)),
inference(step,[status(thm)],[t112108,t201]) ).
cnf(t110307,plain,
multiply(commutator(X1,X2),X3) = multiply(X3,commutator(X1,X2)),
inference(orient,[status(thm)],[t112109]) ).
cnf(goal_0,negated_conjecture,
multiply(commutator(b,c),a) != multiply(a,commutator(b,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(a,commutator(b,c)) != multiply(a,commutator(b,c)),
inference(rw,[status(thm)],[goal_0,t110307]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP024-5 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n019.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Wed Sep 23 13:16:50 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 39.04/5.87 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 39.04/5.87 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------