%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP507-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 : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:27:13 PM UTC 2026
% Result : Unsatisfiable 44.42s 6.97s
% Output : CNFRefutation 44.42s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% 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(t1,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(t6,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)],[t1,t1]) ).
cnf(t191,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)],[t6]) ).
cnf(t212,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)],[t1,t191]) ).
cnf(t334,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)],[t212]) ).
cnf(t335,plain,
multiply(X1,inverse(inverse(X2))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(multiply(X5,X6)),multiply(X5,inverse(multiply(X1,inverse(X6))))))),X2),Y6),inverse(Y6)),
inference(cp,[status(thm)],[t334,t191]) ).
cnf(t419,plain,
multiply(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),Y6),inverse(Y6)) = multiply(X5,inverse(inverse(X6))),
inference(orient,[status(thm)],[t335]) ).
cnf(t420,plain,
multiply(multiply(X1,inverse(X2)),inverse(inverse(X2))) = multiply(multiply(X1,X3),inverse(X3)),
inference(cp,[status(thm)],[t419,t1]) ).
cnf(t515,plain,
multiply(multiply(X1,inverse(X2)),inverse(inverse(X2))) = multiply(multiply(X1,X3),inverse(X3)),
inference(orient,[status(thm)],[t420]) ).
cnf(t572,plain,
multiply(multiply(X1,X2),inverse(X2)) = multiply(multiply(X1,X3),inverse(X3)),
inference(cp,[status(thm)],[t515,t515]) ).
cnf(t640,plain,
multiply(multiply(X1,X2),inverse(X2)) = multiply(multiply(X1,X3),inverse(X3)),
inference(orient,[status(thm)],[t572]) ).
cnf(t657,plain,
multiply(X1,X2) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(multiply(X5,X2)),multiply(X5,inverse(multiply(multiply(X1,X6),inverse(X6))))))),Y6),inverse(Y6)),
inference(cp,[status(thm)],[t334,t640]) ).
cnf(t1687,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(X5,X6),inverse(X6))))))),Y6),inverse(Y6)) = multiply(X5,X4),
inference(orient,[status(thm)],[t657]) ).
cnf(t651,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,inverse(X5))),multiply(X4,inverse(multiply(multiply(X1,X6),inverse(X6))))))),X5),
inference(cp,[status(thm)],[t1,t640]) ).
cnf(t1383,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(multiply(multiply(X5,X6),inverse(X6))))))),X4) = X5,
inference(orient,[status(thm)],[t651]) ).
cnf(t1420,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(multiply(X4,X5),inverse(X5))),multiply(multiply(X4,X6),inverse(multiply(multiply(X1,Y6),inverse(Y6))))))),X6),
inference(cp,[status(thm)],[t1383,t640]) ).
cnf(t3052,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(multiply(X3,X4),inverse(X4))),multiply(multiply(X3,X5),inverse(multiply(multiply(X6,Y6),inverse(Y6))))))),X5) = X6,
inference(orient,[status(thm)],[t1420]) ).
cnf(t3132,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(multiply(X4,X5),inverse(X5))),multiply(multiply(X4,X6),inverse(X6))))),multiply(multiply(X1,Y6),inverse(Y6))),
inference(cp,[status(thm)],[t3052,t640]) ).
cnf(t3510,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(multiply(X3,X4),inverse(X4))),multiply(multiply(X3,X5),inverse(X5))))),multiply(multiply(X6,Y6),inverse(Y6))) = X6,
inference(orient,[status(thm)],[t3132]) ).
cnf(t3679,plain,
multiply(X1,inverse(multiply(multiply(X1,X2),inverse(X2)))) = multiply(X3,inverse(multiply(multiply(X3,X4),inverse(X4)))),
inference(cp,[status(thm)],[t1687,t3510]) ).
cnf(t3728,plain,
multiply(X1,inverse(multiply(multiply(X1,X2),inverse(X2)))) = multiply(X3,inverse(multiply(multiply(X3,X4),inverse(X4)))),
inference(orient,[status(thm)],[t3679]) ).
cnf(t3812,plain,
X1 = multiply(multiply(X2,inverse(multiply(multiply(X2,X3),inverse(X3)))),inverse(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,X5)),multiply(X5,X4))),multiply(inverse(multiply(X6,Y6)),multiply(X6,inverse(multiply(X1,inverse(Y6))))))),Y7),inverse(Y7))))),
inference(cp,[status(thm)],[t334,t3728]) ).
cnf(t330438,plain,
X1 = multiply(multiply(X2,inverse(multiply(multiply(X2,X3),inverse(X3)))),inverse(inverse(X1))),
inference(step,[status(thm)],[t3812,t334]) ).
cnf(t3894,plain,
multiply(multiply(X1,inverse(multiply(multiply(X1,X2),inverse(X2)))),inverse(inverse(X3))) = X3,
inference(orient,[status(thm)],[t330438]) ).
cnf(t693,plain,
multiply(multiply(multiply(X1,X2),X3),inverse(X3)) = multiply(multiply(multiply(X1,X4),inverse(X4)),inverse(inverse(X2))),
inference(cp,[status(thm)],[t640,t640]) ).
cnf(t706,plain,
multiply(multiply(multiply(X1,X2),X3),inverse(X3)) = multiply(multiply(multiply(X1,X4),inverse(X4)),inverse(inverse(X2))),
inference(orient,[status(thm)],[t693]) ).
cnf(t3952,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,inverse(X5))),multiply(X4,inverse(X5))))),multiply(multiply(X1,X6),inverse(X6))),
inference(cp,[status(thm)],[t1,t3894]) ).
cnf(t13008,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(X4))))),multiply(multiply(X5,X6),inverse(X6))) = X5,
inference(orient,[status(thm)],[t3952]) ).
cnf(t716,plain,
multiply(multiply(multiply(multiply(X1,X2),X3),inverse(X3)),inverse(inverse(inverse(X2)))) = multiply(multiply(multiply(multiply(X1,X4),inverse(X4)),X5),inverse(X5)),
inference(cp,[status(thm)],[t706,t640]) ).
cnf(t330435,plain,
multiply(multiply(multiply(multiply(X1,X2),inverse(X2)),c3),inverse(c3)) = multiply(multiply(multiply(multiply(X1,X4),inverse(X4)),X5),inverse(X5)),
inference(step,[status(thm)],[t716,t706]) ).
cnf(t847,plain,
multiply(multiply(multiply(multiply(X1,X2),inverse(X2)),c3),inverse(c3)) = multiply(multiply(multiply(multiply(X1,X3),inverse(X3)),X4),inverse(X4)),
inference(orient,[status(thm)],[t330435]) ).
cnf(t848,plain,
multiply(multiply(multiply(multiply(X1,X2),inverse(X2)),X3),inverse(X3)) = multiply(multiply(multiply(multiply(X1,X4),inverse(X4)),X5),inverse(X5)),
inference(cp,[status(thm)],[t847,t640]) ).
cnf(t1006,plain,
multiply(multiply(multiply(multiply(X1,X2),inverse(X2)),X3),inverse(X3)) = multiply(multiply(multiply(multiply(X1,X4),inverse(X4)),X5),inverse(X5)),
inference(orient,[status(thm)],[t848]) ).
cnf(t1077,plain,
multiply(multiply(multiply(multiply(multiply(X1,X2),inverse(X2)),X3),X4),inverse(X4)) = multiply(multiply(multiply(multiply(multiply(X1,X5),inverse(X5)),X6),inverse(X6)),inverse(inverse(X3))),
inference(cp,[status(thm)],[t640,t1006]) ).
cnf(t330436,plain,
multiply(multiply(multiply(multiply(multiply(X1,X2),inverse(X2)),X3),X4),inverse(X4)) = multiply(multiply(multiply(multiply(multiply(X1,X5),inverse(X5)),X3),c3),inverse(c3)),
inference(step,[status(thm)],[t1077,t706]) ).
cnf(t1097,plain,
multiply(multiply(multiply(multiply(multiply(X1,X2),inverse(X2)),X3),X4),inverse(X4)) = multiply(multiply(multiply(multiply(multiply(X1,X5),inverse(X5)),X3),c3),inverse(c3)),
inference(orient,[status(thm)],[t330436]) ).
cnf(t1205,plain,
multiply(multiply(multiply(multiply(multiply(X1,X2),inverse(X2)),X3),X4),inverse(X4)) = multiply(multiply(multiply(multiply(multiply(X1,X5),inverse(X5)),X3),X6),inverse(X6)),
inference(cp,[status(thm)],[t1097,t640]) ).
cnf(t1280,plain,
multiply(multiply(multiply(multiply(multiply(X1,X2),inverse(X2)),X3),X4),inverse(X4)) = multiply(multiply(multiply(multiply(multiply(X1,X5),inverse(X5)),X3),X6),inverse(X6)),
inference(orient,[status(thm)],[t1205]) ).
cnf(t3907,plain,
X1 = multiply(multiply(multiply(multiply(multiply(X2,X3),inverse(X3)),X4),inverse(multiply(multiply(multiply(multiply(multiply(X2,X5),inverse(X5)),X4),X6),inverse(X6)))),inverse(inverse(X1))),
inference(cp,[status(thm)],[t3894,t1280]) ).
cnf(t9041,plain,
multiply(multiply(multiply(multiply(multiply(X1,X2),inverse(X2)),X3),inverse(multiply(multiply(multiply(multiply(multiply(X1,X4),inverse(X4)),X3),X5),inverse(X5)))),inverse(inverse(X6))) = X6,
inference(orient,[status(thm)],[t3907]) ).
cnf(t13116,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(X4),multiply(multiply(multiply(multiply(multiply(X5,X6),inverse(X6)),Y6),inverse(multiply(multiply(multiply(multiply(multiply(X5,Y7),inverse(Y7)),Y6),Y8),inverse(Y8)))),inverse(inverse(X4)))))),multiply(multiply(X1,Y9),inverse(Y9))),
inference(cp,[status(thm)],[t13008,t9041]) ).
cnf(t330443,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(X4),X4))),multiply(multiply(X1,Y9),inverse(Y9))),
inference(step,[status(thm)],[t13116,t9041]) ).
cnf(t13383,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(X3),X3))),multiply(multiply(X4,X5),inverse(X5))) = X4,
inference(orient,[status(thm)],[t330443]) ).
cnf(t13661,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(X3),X3))),X4),X5),inverse(X5)) = multiply(multiply(X6,inverse(multiply(multiply(X6,Y6),inverse(Y6)))),inverse(inverse(X4))),
inference(cp,[status(thm)],[t706,t13383]) ).
cnf(t330444,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(X3),X3))),X4),X5),inverse(X5)) = X4,
inference(step,[status(thm)],[t13661,t3894]) ).
cnf(t13685,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(X3),X3))),X4),X5),inverse(X5)) = X4,
inference(orient,[status(thm)],[t330444]) ).
cnf(t13979,plain,
multiply(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(X3),X3))),X4),X5),X6),inverse(X6)) = multiply(X4,inverse(inverse(X5))),
inference(cp,[status(thm)],[t640,t13685]) ).
cnf(t16137,plain,
multiply(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(X3),X3))),X4),X5),X6),inverse(X6)) = multiply(X4,inverse(inverse(X5))),
inference(orient,[status(thm)],[t13979]) ).
cnf(t13982,plain,
multiply(multiply(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(X3),X3))),X4),X5),X6),Y6),inverse(Y6)) = multiply(multiply(X4,inverse(inverse(X5))),inverse(inverse(X6))),
inference(cp,[status(thm)],[t706,t13685]) ).
cnf(t51579,plain,
multiply(multiply(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(X3),X3))),X4),X5),X6),Y6),inverse(Y6)) = multiply(multiply(X4,inverse(inverse(X5))),inverse(inverse(X6))),
inference(orient,[status(thm)],[t13982]) ).
cnf(t3975,plain,
multiply(X1,inverse(inverse(inverse(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)))))) = multiply(Y6,inverse(inverse(inverse(Y6)))),
inference(cp,[status(thm)],[t419,t3894]) ).
cnf(t330439,plain,
multiply(X1,inverse(inverse(inverse(X1)))) = multiply(Y6,inverse(inverse(inverse(Y6)))),
inference(step,[status(thm)],[t3975,t334]) ).
cnf(t4040,plain,
multiply(X1,inverse(inverse(inverse(X1)))) = multiply(X2,inverse(inverse(inverse(X2)))),
inference(orient,[status(thm)],[t330439]) ).
cnf(t4041,plain,
multiply(X1,inverse(inverse(inverse(X1)))) = inverse(multiply(X2,inverse(multiply(multiply(X2,X3),inverse(X3))))),
inference(cp,[status(thm)],[t4040,t3894]) ).
cnf(t4160,plain,
multiply(X1,inverse(inverse(inverse(X1)))) = inverse(multiply(X2,inverse(multiply(multiply(X2,X3),inverse(X3))))),
inference(orient,[status(thm)],[t4041]) ).
cnf(t4328,plain,
multiply(multiply(multiply(X1,multiply(X2,inverse(multiply(multiply(X2,X3),inverse(X3))))),X4),inverse(X4)) = multiply(multiply(multiply(X1,X5),inverse(X5)),inverse(multiply(X6,inverse(inverse(inverse(X6)))))),
inference(cp,[status(thm)],[t706,t4160]) ).
cnf(t42625,plain,
multiply(multiply(multiply(X1,multiply(X2,inverse(multiply(multiply(X2,X3),inverse(X3))))),X4),inverse(X4)) = multiply(multiply(multiply(X1,X5),inverse(X5)),inverse(multiply(X6,inverse(inverse(inverse(X6)))))),
inference(orient,[status(thm)],[t4328]) ).
cnf(t4325,plain,
multiply(multiply(X1,X2),inverse(X2)) = multiply(multiply(X1,multiply(X3,inverse(multiply(multiply(X3,X4),inverse(X4))))),multiply(X5,inverse(inverse(inverse(X5))))),
inference(cp,[status(thm)],[t640,t4160]) ).
cnf(t6585,plain,
multiply(multiply(X1,X2),inverse(X2)) = multiply(multiply(X1,multiply(X3,inverse(multiply(multiply(X3,X4),inverse(X4))))),multiply(X5,inverse(inverse(inverse(X5))))),
inference(orient,[status(thm)],[t4325]) ).
cnf(t42689,plain,
multiply(multiply(multiply(X1,X2),inverse(X2)),inverse(multiply(X3,inverse(inverse(inverse(X3)))))) = multiply(multiply(multiply(X1,X4),inverse(X4)),inverse(multiply(X5,inverse(inverse(inverse(X5)))))),
inference(cp,[status(thm)],[t42625,t6585]) ).
cnf(t43779,plain,
multiply(multiply(multiply(X1,X2),inverse(X2)),inverse(multiply(X3,inverse(inverse(inverse(X3)))))) = multiply(multiply(multiply(X1,X4),inverse(X4)),inverse(multiply(X5,inverse(inverse(inverse(X5)))))),
inference(orient,[status(thm)],[t42689]) ).
cnf(t51602,plain,
multiply(multiply(X1,inverse(inverse(X2))),inverse(inverse(inverse(X2)))) = multiply(multiply(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(X5),X5))),X1),X6),inverse(X6)),inverse(multiply(Y6,inverse(inverse(inverse(Y6)))))),inverse(inverse(multiply(Y7,inverse(inverse(inverse(Y7))))))),
inference(cp,[status(thm)],[t51579,t43779]) ).
cnf(t330447,plain,
multiply(multiply(X1,c3),inverse(c3)) = multiply(multiply(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(X5),X5))),X1),X6),inverse(X6)),inverse(multiply(Y6,inverse(inverse(inverse(Y6)))))),inverse(inverse(multiply(Y7,inverse(inverse(inverse(Y7))))))),
inference(step,[status(thm)],[t51602,t515]) ).
cnf(t330448,plain,
multiply(multiply(X1,c3),inverse(c3)) = multiply(multiply(X1,inverse(multiply(Y6,inverse(inverse(inverse(Y6)))))),inverse(inverse(multiply(Y7,inverse(inverse(inverse(Y7))))))),
inference(step,[status(thm)],[t330447,t13685]) ).
cnf(t52419,plain,
multiply(multiply(X1,inverse(multiply(X2,inverse(inverse(inverse(X2)))))),inverse(inverse(multiply(X3,inverse(inverse(inverse(X3))))))) = multiply(multiply(X1,c3),inverse(c3)),
inference(orient,[status(thm)],[t330448]) ).
cnf(t52692,plain,
multiply(inverse(multiply(X1,inverse(inverse(inverse(X1))))),inverse(inverse(inverse(inverse(multiply(X2,inverse(inverse(inverse(X2))))))))) = multiply(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(X5),X5))),c3),inverse(c3)),X6),inverse(X6)),
inference(cp,[status(thm)],[t16137,t52419]) ).
cnf(t330449,plain,
multiply(inverse(multiply(X1,inverse(inverse(inverse(X1))))),inverse(inverse(inverse(inverse(multiply(X2,inverse(inverse(inverse(X2))))))))) = multiply(c3,inverse(inverse(inverse(c3)))),
inference(step,[status(thm)],[t52692,t16137]) ).
cnf(t52918,plain,
multiply(inverse(multiply(X1,inverse(inverse(inverse(X1))))),inverse(inverse(inverse(inverse(multiply(X2,inverse(inverse(inverse(X2))))))))) = multiply(c3,inverse(inverse(inverse(c3)))),
inference(orient,[status(thm)],[t330449]) ).
cnf(t4021,plain,
multiply(X1,inverse(multiply(multiply(X1,X2),inverse(X2)))) = multiply(multiply(X3,inverse(multiply(multiply(X3,X4),inverse(X4)))),inverse(multiply(X5,inverse(inverse(inverse(X5)))))),
inference(cp,[status(thm)],[t3728,t3894]) ).
cnf(t7764,plain,
multiply(X1,inverse(multiply(multiply(X1,X2),inverse(X2)))) = multiply(multiply(X3,inverse(multiply(multiply(X3,X4),inverse(X4)))),inverse(multiply(X5,inverse(inverse(inverse(X5)))))),
inference(orient,[status(thm)],[t4021]) ).
cnf(t8142,plain,
X1 = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(multiply(X4,inverse(multiply(multiply(X4,X5),inverse(X5)))),inverse(inverse(X1)))),multiply(X6,inverse(multiply(multiply(X6,Y6),inverse(Y6))))))),Y7),inverse(Y7)),
inference(cp,[status(thm)],[t334,t7764]) ).
cnf(t330445,plain,
X1 = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(X1),multiply(X6,inverse(multiply(multiply(X6,Y6),inverse(Y6))))))),Y7),inverse(Y7)),
inference(step,[status(thm)],[t8142,t3894]) ).
cnf(t21038,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(X3),multiply(X4,inverse(multiply(multiply(X4,X5),inverse(X5))))))),X6),inverse(X6)) = X3,
inference(orient,[status(thm)],[t330445]) ).
cnf(t21059,plain,
X1 = multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2)))),multiply(inverse(X1),multiply(X4,inverse(multiply(multiply(X4,X5),inverse(X5))))))),X6),inverse(X6)),
inference(cp,[status(thm)],[t21038,t13383]) ).
cnf(t40592,plain,
multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)))),multiply(inverse(X3),multiply(X4,inverse(multiply(multiply(X4,X5),inverse(X5))))))),X6),inverse(X6)) = X3,
inference(orient,[status(thm)],[t21059]) ).
cnf(t3819,plain,
multiply(X1,inverse(inverse(inverse(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)))))) = multiply(multiply(multiply(Y6,inverse(multiply(multiply(Y6,Y7),inverse(Y7)))),Y8),inverse(Y8)),
inference(cp,[status(thm)],[t419,t3728]) ).
cnf(t330440,plain,
multiply(X1,inverse(inverse(inverse(X1)))) = multiply(multiply(multiply(Y6,inverse(multiply(multiply(Y6,Y7),inverse(Y7)))),Y8),inverse(Y8)),
inference(step,[status(thm)],[t3819,t334]) ).
cnf(t4755,plain,
multiply(X1,inverse(inverse(inverse(X1)))) = multiply(multiply(multiply(X2,inverse(multiply(multiply(X2,X3),inverse(X3)))),X4),inverse(X4)),
inference(orient,[status(thm)],[t330440]) ).
cnf(t13687,plain,
inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(X3),X3))),X4),inverse(X4))) = multiply(X5,inverse(inverse(inverse(X5)))),
inference(cp,[status(thm)],[t13685,t4755]) ).
cnf(t17324,plain,
inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(X3),X3))),X4),inverse(X4))) = multiply(X5,inverse(inverse(inverse(X5)))),
inference(orient,[status(thm)],[t13687]) ).
cnf(t17485,plain,
X1 = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(X4),X4))),multiply(X5,inverse(inverse(inverse(X5))))),inverse(inverse(X1))),
inference(cp,[status(thm)],[t3894,t17324]) ).
cnf(t17942,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(X3),X3))),multiply(X4,inverse(inverse(inverse(X4))))),inverse(inverse(X5))) = X5,
inference(orient,[status(thm)],[t17485]) ).
cnf(t13570,plain,
X1 = multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2)))),multiply(inverse(X4),X4))),multiply(multiply(X1,X5),inverse(X5))),
inference(cp,[status(thm)],[t13383,t13383]) ).
cnf(t14037,plain,
multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)))),multiply(inverse(X3),X3))),multiply(multiply(X4,X5),inverse(X5))) = X4,
inference(orient,[status(thm)],[t13570]) ).
cnf(t17948,plain,
X1 = multiply(multiply(inverse(multiply(inverse(inverse(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))))),multiply(inverse(X4),X4))),multiply(X5,inverse(inverse(inverse(X5))))),inverse(inverse(X1))),
inference(cp,[status(thm)],[t17942,t14037]) ).
cnf(t25921,plain,
multiply(multiply(inverse(multiply(inverse(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))))),multiply(inverse(X3),X3))),multiply(X4,inverse(inverse(inverse(X4))))),inverse(inverse(X5))) = X5,
inference(orient,[status(thm)],[t17948]) ).
cnf(t25927,plain,
inverse(multiply(inverse(multiply(inverse(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))))),multiply(inverse(X3),X3))),multiply(X4,inverse(inverse(inverse(X4)))))) = multiply(X5,inverse(inverse(inverse(X5)))),
inference(cp,[status(thm)],[t25921,t4040]) ).
cnf(t118773,plain,
inverse(multiply(inverse(multiply(inverse(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))))),multiply(inverse(X3),X3))),multiply(X4,inverse(inverse(inverse(X4)))))) = multiply(X5,inverse(inverse(inverse(X5)))),
inference(orient,[status(thm)],[t25927]) ).
cnf(t119343,plain,
X1 = multiply(multiply(inverse(multiply(inverse(multiply(X2,inverse(inverse(inverse(X2))))),multiply(inverse(X1),multiply(X3,inverse(multiply(multiply(X3,X4),inverse(X4))))))),X5),inverse(X5)),
inference(cp,[status(thm)],[t40592,t118773]) ).
cnf(t170832,plain,
multiply(multiply(inverse(multiply(inverse(multiply(X1,inverse(inverse(inverse(X1))))),multiply(inverse(X2),multiply(X3,inverse(multiply(multiply(X3,X4),inverse(X4))))))),X5),inverse(X5)) = X2,
inference(orient,[status(thm)],[t119343]) ).
cnf(t119273,plain,
X1 = multiply(inverse(multiply(inverse(multiply(X2,inverse(inverse(inverse(X2))))),multiply(inverse(X3),X3))),multiply(multiply(X1,X4),inverse(X4))),
inference(cp,[status(thm)],[t14037,t118773]) ).
cnf(t122482,plain,
multiply(inverse(multiply(inverse(multiply(X1,inverse(inverse(inverse(X1))))),multiply(inverse(X2),X2))),multiply(multiply(X3,X4),inverse(X4))) = X3,
inference(orient,[status(thm)],[t119273]) ).
cnf(t119380,plain,
X1 = multiply(multiply(multiply(inverse(multiply(multiply(X2,inverse(inverse(inverse(X2)))),multiply(inverse(X3),X3))),X1),X4),inverse(X4)),
inference(cp,[status(thm)],[t13685,t118773]) ).
cnf(t121210,plain,
multiply(multiply(multiply(inverse(multiply(multiply(X1,inverse(inverse(inverse(X1)))),multiply(inverse(X2),X2))),X3),X4),inverse(X4)) = X3,
inference(orient,[status(thm)],[t119380]) ).
cnf(t122539,plain,
multiply(inverse(multiply(multiply(X1,inverse(inverse(inverse(X1)))),multiply(inverse(X2),X2))),X3) = multiply(inverse(multiply(inverse(multiply(X4,inverse(inverse(inverse(X4))))),multiply(inverse(X5),X5))),X3),
inference(cp,[status(thm)],[t122482,t121210]) ).
cnf(t287021,plain,
multiply(inverse(multiply(multiply(X1,inverse(inverse(inverse(X1)))),multiply(inverse(X2),X2))),X3) = multiply(inverse(multiply(inverse(multiply(X4,inverse(inverse(inverse(X4))))),multiply(inverse(X5),X5))),X3),
inference(orient,[status(thm)],[t122539]) ).
cnf(t287416,plain,
multiply(multiply(X1,inverse(inverse(inverse(X1)))),multiply(inverse(X2),X2)) = multiply(multiply(inverse(multiply(inverse(multiply(X3,inverse(inverse(inverse(X3))))),multiply(inverse(multiply(inverse(multiply(X4,inverse(inverse(inverse(X4))))),multiply(inverse(X5),X5))),multiply(X6,inverse(multiply(multiply(X6,Y6),inverse(Y6))))))),Y7),inverse(Y7)),
inference(cp,[status(thm)],[t170832,t287021]) ).
cnf(t330483,plain,
multiply(multiply(X1,inverse(inverse(inverse(X1)))),multiply(inverse(X2),X2)) = multiply(inverse(multiply(X4,inverse(inverse(inverse(X4))))),multiply(inverse(X5),X5)),
inference(step,[status(thm)],[t287416,t170832]) ).
cnf(t289606,plain,
multiply(multiply(X1,inverse(inverse(inverse(X1)))),multiply(inverse(X2),X2)) = multiply(inverse(multiply(X3,inverse(inverse(inverse(X3))))),multiply(inverse(X4),X4)),
inference(orient,[status(thm)],[t330483]) ).
cnf(t290374,plain,
multiply(multiply(inverse(multiply(X1,inverse(inverse(inverse(X1))))),X2),inverse(X2)) = multiply(multiply(multiply(X3,inverse(inverse(inverse(X3)))),multiply(inverse(X4),X4)),inverse(multiply(inverse(X5),X5))),
inference(cp,[status(thm)],[t640,t289606]) ).
cnf(t119247,plain,
X1 = multiply(inverse(multiply(multiply(X2,inverse(inverse(inverse(X2)))),multiply(inverse(X3),X3))),multiply(multiply(X1,X4),inverse(X4))),
inference(cp,[status(thm)],[t13383,t118773]) ).
cnf(t120585,plain,
multiply(inverse(multiply(multiply(X1,inverse(inverse(inverse(X1)))),multiply(inverse(X2),X2))),multiply(multiply(X3,X4),inverse(X4))) = X3,
inference(orient,[status(thm)],[t119247]) ).
cnf(t121361,plain,
multiply(inverse(multiply(multiply(X1,inverse(inverse(inverse(X1)))),multiply(inverse(X2),X2))),X3) = multiply(inverse(multiply(multiply(X4,inverse(inverse(inverse(X4)))),multiply(inverse(X5),X5))),X3),
inference(cp,[status(thm)],[t120585,t121210]) ).
cnf(t219555,plain,
multiply(inverse(multiply(multiply(X1,inverse(inverse(inverse(X1)))),multiply(inverse(X2),X2))),X3) = multiply(inverse(multiply(multiply(X4,inverse(inverse(inverse(X4)))),multiply(inverse(X5),X5))),X3),
inference(orient,[status(thm)],[t121361]) ).
cnf(t219844,plain,
multiply(multiply(X1,inverse(inverse(inverse(X1)))),multiply(inverse(X2),X2)) = multiply(multiply(inverse(multiply(inverse(multiply(X3,inverse(inverse(inverse(X3))))),multiply(inverse(multiply(multiply(X4,inverse(inverse(inverse(X4)))),multiply(inverse(X5),X5))),multiply(X6,inverse(multiply(multiply(X6,Y6),inverse(Y6))))))),Y7),inverse(Y7)),
inference(cp,[status(thm)],[t170832,t219555]) ).
cnf(t330475,plain,
multiply(multiply(X1,inverse(inverse(inverse(X1)))),multiply(inverse(X2),X2)) = multiply(multiply(X4,inverse(inverse(inverse(X4)))),multiply(inverse(X5),X5)),
inference(step,[status(thm)],[t219844,t170832]) ).
cnf(t220684,plain,
multiply(multiply(X1,inverse(inverse(inverse(X1)))),multiply(inverse(X2),X2)) = multiply(multiply(X3,inverse(inverse(inverse(X3)))),multiply(inverse(X4),X4)),
inference(orient,[status(thm)],[t330475]) ).
cnf(t221167,plain,
multiply(multiply(multiply(X1,inverse(inverse(inverse(X1)))),X2),inverse(X2)) = multiply(multiply(multiply(X3,inverse(inverse(inverse(X3)))),multiply(inverse(X4),X4)),inverse(multiply(inverse(X5),X5))),
inference(cp,[status(thm)],[t640,t220684]) ).
cnf(t221254,plain,
multiply(multiply(multiply(X1,inverse(inverse(inverse(X1)))),X2),inverse(X2)) = multiply(multiply(multiply(X3,inverse(inverse(inverse(X3)))),multiply(inverse(X4),X4)),inverse(multiply(inverse(X5),X5))),
inference(orient,[status(thm)],[t221167]) ).
cnf(t330485,plain,
multiply(multiply(inverse(multiply(X1,inverse(inverse(inverse(X1))))),X2),inverse(X2)) = multiply(multiply(multiply(c3,inverse(inverse(inverse(c3)))),c3),inverse(c3)),
inference(step,[status(thm)],[t290374,t221254]) ).
cnf(t309825,plain,
multiply(multiply(inverse(multiply(X1,inverse(inverse(inverse(X1))))),X2),inverse(X2)) = multiply(multiply(multiply(c3,inverse(inverse(inverse(c3)))),c3),inverse(c3)),
inference(orient,[status(thm)],[t330485]) ).
cnf(t309978,plain,
inverse(multiply(X1,inverse(inverse(inverse(X1))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(multiply(X4,X5),inverse(X5))),multiply(multiply(X4,X6),inverse(X6))))),multiply(multiply(multiply(c3,inverse(inverse(inverse(c3)))),c3),inverse(c3))),
inference(cp,[status(thm)],[t3510,t309825]) ).
cnf(t330497,plain,
inverse(multiply(X1,inverse(inverse(inverse(X1))))) = multiply(c3,inverse(inverse(inverse(c3)))),
inference(step,[status(thm)],[t309978,t3510]) ).
cnf(t310739,plain,
inverse(multiply(X1,inverse(inverse(inverse(X1))))) = multiply(c3,inverse(inverse(inverse(c3)))),
inference(orient,[status(thm)],[t330497]) ).
cnf(t330561,plain,
multiply(multiply(c3,inverse(inverse(inverse(c3)))),inverse(inverse(inverse(inverse(multiply(X2,inverse(inverse(inverse(X2))))))))) = multiply(c3,inverse(inverse(inverse(c3)))),
inference(step,[status(thm)],[t52918,t310739]) ).
cnf(t330562,plain,
multiply(multiply(c3,inverse(inverse(inverse(c3)))),inverse(inverse(inverse(multiply(c3,inverse(inverse(inverse(c3)))))))) = multiply(c3,inverse(inverse(inverse(c3)))),
inference(step,[status(thm)],[t330561,t310739]) ).
cnf(t330563,plain,
multiply(multiply(c3,inverse(inverse(inverse(c3)))),inverse(inverse(multiply(c3,inverse(inverse(inverse(c3))))))) = multiply(c3,inverse(inverse(inverse(c3)))),
inference(step,[status(thm)],[t330562,t310739]) ).
cnf(t330564,plain,
multiply(multiply(c3,inverse(inverse(inverse(c3)))),inverse(multiply(c3,inverse(inverse(inverse(c3)))))) = multiply(c3,inverse(inverse(inverse(c3)))),
inference(step,[status(thm)],[t330563,t310739]) ).
cnf(t330565,plain,
multiply(multiply(c3,inverse(inverse(inverse(c3)))),multiply(c3,inverse(inverse(inverse(c3))))) = multiply(c3,inverse(inverse(inverse(c3)))),
inference(step,[status(thm)],[t330564,t310739]) ).
cnf(t311534,plain,
multiply(multiply(c3,inverse(inverse(inverse(c3)))),multiply(c3,inverse(inverse(inverse(c3))))) = multiply(c3,inverse(inverse(inverse(c3)))),
inference(rw,[status(thm)],[t330565]) ).
cnf(t311550,plain,
multiply(multiply(c3,inverse(inverse(inverse(c3)))),multiply(c3,inverse(inverse(inverse(c3))))) = multiply(c3,inverse(inverse(inverse(c3)))),
inference(orient,[status(thm)],[t311534]) ).
cnf(t311553,plain,
X1 = multiply(multiply(multiply(c3,inverse(inverse(inverse(c3)))),inverse(multiply(multiply(c3,inverse(inverse(inverse(c3)))),inverse(multiply(c3,inverse(inverse(inverse(c3)))))))),inverse(inverse(X1))),
inference(cp,[status(thm)],[t3894,t311550]) ).
cnf(t330623,plain,
X1 = multiply(multiply(multiply(c3,inverse(inverse(inverse(c3)))),inverse(multiply(multiply(c3,inverse(inverse(inverse(c3)))),multiply(c3,inverse(inverse(inverse(c3))))))),inverse(inverse(X1))),
inference(step,[status(thm)],[t311553,t310739]) ).
cnf(t330624,plain,
X1 = multiply(multiply(multiply(c3,inverse(inverse(inverse(c3)))),inverse(multiply(c3,inverse(inverse(inverse(c3)))))),inverse(inverse(X1))),
inference(step,[status(thm)],[t330623,t311550]) ).
cnf(t330625,plain,
X1 = multiply(multiply(multiply(c3,inverse(inverse(inverse(c3)))),multiply(c3,inverse(inverse(inverse(c3))))),inverse(inverse(X1))),
inference(step,[status(thm)],[t330624,t310739]) ).
cnf(t330626,plain,
X1 = multiply(multiply(c3,inverse(inverse(inverse(c3)))),inverse(inverse(X1))),
inference(step,[status(thm)],[t330625,t311550]) ).
cnf(t311813,plain,
multiply(multiply(c3,inverse(inverse(inverse(c3)))),inverse(inverse(X1))) = X1,
inference(orient,[status(thm)],[t330626]) ).
cnf(t4133,plain,
multiply(multiply(X1,X2),inverse(X2)) = multiply(multiply(X3,inverse(inverse(inverse(X3)))),inverse(inverse(inverse(inverse(X1))))),
inference(cp,[status(thm)],[t640,t4040]) ).
cnf(t4435,plain,
multiply(multiply(X1,X2),inverse(X2)) = multiply(multiply(X3,inverse(inverse(inverse(X3)))),inverse(inverse(inverse(inverse(X1))))),
inference(orient,[status(thm)],[t4133]) ).
cnf(t311814,plain,
inverse(inverse(X1)) = multiply(multiply(X1,X2),inverse(X2)),
inference(cp,[status(thm)],[t311813,t4435]) ).
cnf(t312430,plain,
multiply(multiply(X1,X2),inverse(X2)) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t311814]) ).
cnf(t656,plain,
X1 = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(multiply(X4,multiply(X1,inverse(X5))),X5)),multiply(multiply(X4,X6),inverse(X6))))),Y6),inverse(Y6)),
inference(cp,[status(thm)],[t334,t640]) ).
cnf(t2845,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(multiply(X3,multiply(X4,inverse(X5))),X5)),multiply(multiply(X3,X6),inverse(X6))))),Y6),inverse(Y6)) = X4,
inference(orient,[status(thm)],[t656]) ).
cnf(t121053,plain,
X1 = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(multiply(inverse(multiply(multiply(X4,inverse(inverse(inverse(X4)))),multiply(inverse(X5),X5))),multiply(X1,inverse(X6))),X6)),multiply(Y6,inverse(multiply(multiply(Y6,Y7),inverse(Y7))))))),Y8),inverse(Y8)),
inference(cp,[status(thm)],[t2845,t120585]) ).
cnf(t330465,plain,
X1 = multiply(multiply(inverse(multiply(multiply(X4,inverse(inverse(inverse(X4)))),multiply(inverse(X5),X5))),multiply(X1,inverse(X6))),X6),
inference(step,[status(thm)],[t121053,t21038]) ).
cnf(t121896,plain,
multiply(multiply(inverse(multiply(multiply(X1,inverse(inverse(inverse(X1)))),multiply(inverse(X2),X2))),multiply(X3,inverse(X4))),X4) = X3,
inference(orient,[status(thm)],[t330465]) ).
cnf(t312477,plain,
inverse(inverse(multiply(X1,X2))) = multiply(inverse(inverse(X1)),inverse(inverse(X2))),
inference(cp,[status(thm)],[t312430,t312430]) ).
cnf(t312796,plain,
multiply(inverse(inverse(X1)),inverse(inverse(X2))) = inverse(inverse(multiply(X1,X2))),
inference(orient,[status(thm)],[t312477]) ).
cnf(t312800,plain,
inverse(inverse(multiply(multiply(X1,inverse(inverse(inverse(X1)))),X2))) = multiply(inverse(multiply(c3,inverse(inverse(inverse(c3))))),inverse(inverse(X2))),
inference(cp,[status(thm)],[t312796,t310739]) ).
cnf(t330831,plain,
inverse(inverse(multiply(multiply(X1,inverse(inverse(inverse(X1)))),X2))) = multiply(multiply(c3,inverse(inverse(inverse(c3)))),inverse(inverse(X2))),
inference(step,[status(thm)],[t312800,t310739]) ).
cnf(t330832,plain,
inverse(inverse(multiply(multiply(X1,inverse(inverse(inverse(X1)))),X2))) = X2,
inference(step,[status(thm)],[t330831,t311813]) ).
cnf(t313136,plain,
inverse(inverse(multiply(multiply(X1,inverse(inverse(inverse(X1)))),X2))) = X2,
inference(orient,[status(thm)],[t330832]) ).
cnf(t313137,plain,
multiply(inverse(X1),X1) = inverse(inverse(multiply(multiply(X2,inverse(inverse(inverse(X2)))),multiply(inverse(X3),X3)))),
inference(cp,[status(thm)],[t313136,t220684]) ).
cnf(t330833,plain,
multiply(inverse(X1),X1) = multiply(inverse(X3),X3),
inference(step,[status(thm)],[t313137,t313136]) ).
cnf(t313305,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),X2),
inference(orient,[status(thm)],[t330833]) ).
cnf(t313314,plain,
inverse(inverse(inverse(X1))) = multiply(multiply(inverse(X2),X2),inverse(X1)),
inference(cp,[status(thm)],[t312430,t313305]) ).
cnf(t313499,plain,
multiply(multiply(inverse(X1),X1),inverse(X2)) = inverse(inverse(inverse(X2))),
inference(orient,[status(thm)],[t313314]) ).
cnf(t313512,plain,
inverse(inverse(inverse(inverse(multiply(multiply(X1,inverse(inverse(inverse(X1)))),X2))))) = multiply(multiply(inverse(X3),X3),X2),
inference(cp,[status(thm)],[t313499,t313136]) ).
cnf(t330834,plain,
inverse(inverse(X2)) = multiply(multiply(inverse(X3),X3),X2),
inference(step,[status(thm)],[t313512,t313136]) ).
cnf(t313709,plain,
multiply(multiply(inverse(X1),X1),X2) = inverse(inverse(X2)),
inference(orient,[status(thm)],[t330834]) ).
cnf(t313713,plain,
inverse(inverse(X1)) = multiply(inverse(inverse(multiply(inverse(X2),X2))),X1),
inference(cp,[status(thm)],[t313709,t312796]) ).
cnf(t313914,plain,
multiply(inverse(inverse(multiply(inverse(X1),X1))),X2) = inverse(inverse(X2)),
inference(orient,[status(thm)],[t313713]) ).
cnf(t313938,plain,
X1 = multiply(multiply(inverse(multiply(multiply(X2,inverse(inverse(inverse(X2)))),inverse(inverse(inverse(multiply(inverse(X3),X3)))))),multiply(X1,inverse(X4))),X4),
inference(cp,[status(thm)],[t121896,t313914]) ).
cnf(t311820,plain,
X1 = multiply(multiply(X2,inverse(inverse(inverse(X2)))),inverse(inverse(X1))),
inference(cp,[status(thm)],[t311813,t4040]) ).
cnf(t312949,plain,
multiply(multiply(X1,inverse(inverse(inverse(X1)))),inverse(inverse(X2))) = X2,
inference(orient,[status(thm)],[t311820]) ).
cnf(t330835,plain,
X1 = multiply(multiply(inverse(inverse(multiply(inverse(X3),X3))),multiply(X1,inverse(X4))),X4),
inference(step,[status(thm)],[t313938,t312949]) ).
cnf(t330836,plain,
X1 = multiply(inverse(inverse(multiply(X1,inverse(X4)))),X4),
inference(step,[status(thm)],[t330835,t313914]) ).
cnf(t314129,plain,
multiply(inverse(inverse(multiply(X1,inverse(X2)))),X2) = X1,
inference(orient,[status(thm)],[t330836]) ).
cnf(t314135,plain,
multiply(X1,X2) = multiply(inverse(inverse(inverse(inverse(X1)))),X2),
inference(cp,[status(thm)],[t314129,t312430]) ).
cnf(t314319,plain,
multiply(inverse(inverse(inverse(inverse(X1)))),X2) = multiply(X1,X2),
inference(orient,[status(thm)],[t314135]) ).
cnf(t314333,plain,
inverse(inverse(inverse(inverse(X1)))) = multiply(inverse(inverse(multiply(X1,inverse(X2)))),X2),
inference(cp,[status(thm)],[t314129,t314319]) ).
cnf(t330840,plain,
inverse(inverse(inverse(inverse(X1)))) = X1,
inference(step,[status(thm)],[t314333,t314129]) ).
cnf(t314498,plain,
inverse(inverse(inverse(inverse(X1)))) = X1,
inference(orient,[status(thm)],[t330840]) ).
cnf(t314505,plain,
inverse(inverse(X1)) = multiply(multiply(X1,inverse(inverse(inverse(X2)))),X2),
inference(cp,[status(thm)],[t312430,t314498]) ).
cnf(t315518,plain,
multiply(multiply(X1,inverse(inverse(inverse(X2)))),X2) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t314505]) ).
cnf(t314175,plain,
inverse(inverse(multiply(X1,inverse(inverse(X2))))) = multiply(inverse(inverse(X1)),X2),
inference(cp,[status(thm)],[t314129,t314129]) ).
cnf(t314658,plain,
inverse(inverse(multiply(X1,inverse(inverse(X2))))) = multiply(inverse(inverse(X1)),X2),
inference(orient,[status(thm)],[t314175]) ).
cnf(t314659,plain,
multiply(inverse(inverse(X1)),inverse(X1)) = inverse(multiply(c3,inverse(inverse(inverse(c3))))),
inference(cp,[status(thm)],[t314658,t310739]) ).
cnf(t330841,plain,
multiply(inverse(c3),c3) = inverse(multiply(c3,inverse(inverse(inverse(c3))))),
inference(step,[status(thm)],[t314659,t313305]) ).
cnf(t330842,plain,
multiply(inverse(c3),c3) = multiply(c3,inverse(inverse(inverse(c3)))),
inference(step,[status(thm)],[t330841,t310739]) ).
cnf(t314841,plain,
multiply(c3,inverse(inverse(inverse(c3)))) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t330842]) ).
cnf(t330843,plain,
inverse(multiply(X1,inverse(inverse(inverse(X1))))) = multiply(inverse(c3),c3),
inference(step,[status(thm)],[t310739,t314841]) ).
cnf(t314842,plain,
inverse(multiply(X1,inverse(inverse(inverse(X1))))) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t330843]) ).
cnf(t314846,plain,
multiply(inverse(c3),c3) = inverse(multiply(inverse(c3),c3)),
inference(cp,[status(thm)],[t314842,t314841]) ).
cnf(t314963,plain,
inverse(multiply(inverse(c3),c3)) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t314846]) ).
cnf(t314964,plain,
multiply(inverse(c3),c3) = inverse(multiply(inverse(X1),X1)),
inference(cp,[status(thm)],[t314963,t313305]) ).
cnf(t315113,plain,
inverse(multiply(inverse(X1),X1)) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t314964]) ).
cnf(t315121,plain,
inverse(inverse(X1)) = multiply(multiply(X1,multiply(inverse(X2),X2)),multiply(inverse(c3),c3)),
inference(cp,[status(thm)],[t312430,t315113]) ).
cnf(t315791,plain,
multiply(multiply(X1,multiply(inverse(X2),X2)),multiply(inverse(c3),c3)) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t315121]) ).
cnf(t315814,plain,
inverse(inverse(X1)) = multiply(multiply(X1,multiply(inverse(X2),X2)),multiply(inverse(X3),X3)),
inference(cp,[status(thm)],[t315791,t313305]) ).
cnf(t316303,plain,
multiply(multiply(X1,multiply(inverse(X2),X2)),multiply(inverse(X3),X3)) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t315814]) ).
cnf(t119403,plain,
X1 = multiply(multiply(inverse(multiply(multiply(X2,inverse(inverse(inverse(X2)))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X1,inverse(X4))))))),X5),inverse(X5)),
inference(cp,[status(thm)],[t334,t118773]) ).
cnf(t145605,plain,
multiply(multiply(inverse(multiply(multiply(X1,inverse(inverse(inverse(X1)))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(X4,inverse(X3))))))),X5),inverse(X5)) = X4,
inference(orient,[status(thm)],[t119403]) ).
cnf(t14327,plain,
multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)))),multiply(inverse(X3),X3))),X4),inverse(X4)) = multiply(X5,inverse(multiply(multiply(X5,X6),inverse(X6)))),
inference(cp,[status(thm)],[t640,t14037]) ).
cnf(t46875,plain,
multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)))),multiply(inverse(X3),X3))),X4),inverse(X4)) = multiply(X5,inverse(multiply(multiply(X5,X6),inverse(X6)))),
inference(orient,[status(thm)],[t14327]) ).
cnf(t146003,plain,
X1 = multiply(multiply(inverse(multiply(multiply(X2,inverse(inverse(inverse(X2)))),multiply(inverse(multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3)))),multiply(inverse(X5),X5))),multiply(X1,inverse(X6))),X6)),multiply(Y6,inverse(multiply(multiply(Y6,Y7),inverse(Y7))))))),Y8),inverse(Y8)),
inference(cp,[status(thm)],[t145605,t46875]) ).
cnf(t119366,plain,
X1 = multiply(multiply(inverse(multiply(multiply(X2,inverse(inverse(inverse(X2)))),multiply(inverse(X1),multiply(X3,inverse(multiply(multiply(X3,X4),inverse(X4))))))),X5),inverse(X5)),
inference(cp,[status(thm)],[t21038,t118773]) ).
cnf(t144585,plain,
multiply(multiply(inverse(multiply(multiply(X1,inverse(inverse(inverse(X1)))),multiply(inverse(X2),multiply(X3,inverse(multiply(multiply(X3,X4),inverse(X4))))))),X5),inverse(X5)) = X2,
inference(orient,[status(thm)],[t119366]) ).
cnf(t330470,plain,
X1 = multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3)))),multiply(inverse(X5),X5))),multiply(X1,inverse(X6))),X6),
inference(step,[status(thm)],[t146003,t144585]) ).
cnf(t148531,plain,
multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)))),multiply(inverse(X3),X3))),multiply(X4,inverse(X5))),X5) = X4,
inference(orient,[status(thm)],[t330470]) ).
cnf(t316305,plain,
inverse(inverse(inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)))),multiply(inverse(X3),X3))))) = inverse(inverse(multiply(inverse(X4),X4))),
inference(cp,[status(thm)],[t316303,t148531]) ).
cnf(t314506,plain,
inverse(inverse(multiply(inverse(inverse(X1)),X2))) = multiply(X1,inverse(inverse(X2))),
inference(cp,[status(thm)],[t312796,t314498]) ).
cnf(t315428,plain,
inverse(inverse(multiply(inverse(inverse(X1)),X2))) = multiply(X1,inverse(inverse(X2))),
inference(orient,[status(thm)],[t314506]) ).
cnf(t330875,plain,
inverse(multiply(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)),inverse(inverse(multiply(inverse(X3),X3))))) = inverse(inverse(multiply(inverse(X4),X4))),
inference(step,[status(thm)],[t316305,t315428]) ).
cnf(t330876,plain,
inverse(multiply(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)),inverse(multiply(inverse(c3),c3)))) = inverse(inverse(multiply(inverse(X4),X4))),
inference(step,[status(thm)],[t330875,t315113]) ).
cnf(t330877,plain,
inverse(multiply(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)),multiply(inverse(c3),c3))) = inverse(inverse(multiply(inverse(X4),X4))),
inference(step,[status(thm)],[t330876,t314963]) ).
cnf(t330878,plain,
inverse(multiply(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)),multiply(inverse(c3),c3))) = inverse(multiply(inverse(c3),c3)),
inference(step,[status(thm)],[t330877,t315113]) ).
cnf(t330879,plain,
inverse(multiply(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)),multiply(inverse(c3),c3))) = multiply(inverse(c3),c3),
inference(step,[status(thm)],[t330878,t314963]) ).
cnf(t318297,plain,
inverse(multiply(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)),multiply(inverse(c3),c3))) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t330879]) ).
cnf(t314844,plain,
multiply(inverse(c3),c3) = multiply(X1,inverse(inverse(inverse(X1)))),
inference(cp,[status(thm)],[t314841,t4040]) ).
cnf(t315296,plain,
multiply(X1,inverse(inverse(inverse(X1)))) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t314844]) ).
cnf(t318332,plain,
multiply(inverse(c3),c3) = inverse(multiply(multiply(inverse(multiply(inverse(inverse(inverse(X1))),X1)),multiply(inverse(c3),c3)),multiply(inverse(c3),c3))),
inference(cp,[status(thm)],[t318297,t315296]) ).
cnf(t315539,plain,
inverse(inverse(X1)) = multiply(multiply(X1,inverse(inverse(multiply(inverse(c3),c3)))),multiply(inverse(X2),X2)),
inference(cp,[status(thm)],[t315518,t315113]) ).
cnf(t330867,plain,
inverse(inverse(X1)) = multiply(multiply(X1,inverse(multiply(inverse(c3),c3))),multiply(inverse(X2),X2)),
inference(step,[status(thm)],[t315539,t314963]) ).
cnf(t330868,plain,
inverse(inverse(X1)) = multiply(multiply(X1,multiply(inverse(c3),c3)),multiply(inverse(X2),X2)),
inference(step,[status(thm)],[t330867,t314963]) ).
cnf(t315877,plain,
multiply(multiply(X1,multiply(inverse(c3),c3)),multiply(inverse(X2),X2)) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t330868]) ).
cnf(t330880,plain,
multiply(inverse(c3),c3) = inverse(inverse(inverse(inverse(multiply(inverse(inverse(inverse(X1))),X1))))),
inference(step,[status(thm)],[t318332,t315877]) ).
cnf(t330881,plain,
multiply(inverse(c3),c3) = multiply(inverse(inverse(inverse(X1))),X1),
inference(step,[status(thm)],[t330880,t314498]) ).
cnf(t318503,plain,
multiply(inverse(inverse(inverse(X1))),X1) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t330881]) ).
cnf(t318534,plain,
inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(X1)))))))) = multiply(multiply(inverse(c3),c3),X1),
inference(cp,[status(thm)],[t315518,t318503]) ).
cnf(t330882,plain,
inverse(inverse(inverse(inverse(X1)))) = multiply(multiply(inverse(c3),c3),X1),
inference(step,[status(thm)],[t318534,t314498]) ).
cnf(t330883,plain,
X1 = multiply(multiply(inverse(c3),c3),X1),
inference(step,[status(thm)],[t330882,t314498]) ).
cnf(t330884,plain,
X1 = inverse(inverse(X1)),
inference(step,[status(thm)],[t330883,t313709]) ).
cnf(t318658,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t330884]) ).
cnf(t330885,plain,
multiply(multiply(X1,X2),inverse(X2)) = X1,
inference(step,[status(thm)],[t312430,t318658]) ).
cnf(t318659,plain,
multiply(multiply(X1,X2),inverse(X2)) = X1,
inference(orient,[status(thm)],[t330885]) ).
cnf(t318667,plain,
X1 = multiply(multiply(X1,inverse(X2)),X2),
inference(cp,[status(thm)],[t318659,t318658]) ).
cnf(t318738,plain,
multiply(multiply(X1,inverse(X2)),X2) = X1,
inference(orient,[status(thm)],[t318667]) ).
cnf(t319965,plain,
multiply(multiply(X1,inverse(X2)),X2) = X1,
inference(rw,[status(thm)],[t318738]) ).
cnf(t330887,plain,
multiply(multiply(inverse(X1),X1),X2) = X2,
inference(step,[status(thm)],[t313709,t318658]) ).
cnf(t318661,plain,
multiply(multiply(inverse(X1),X1),X2) = X2,
inference(orient,[status(thm)],[t330887]) ).
cnf(t318669,plain,
X1 = multiply(multiply(X2,inverse(X2)),X1),
inference(cp,[status(thm)],[t318661,t318658]) ).
cnf(t318850,plain,
multiply(multiply(X1,inverse(X1)),X2) = X2,
inference(orient,[status(thm)],[t318669]) ).
cnf(t319213,plain,
inverse(multiply(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)),multiply(inverse(c3),c3))) = multiply(inverse(c3),c3),
inference(rw,[status(thm)],[t318297]) ).
cnf(t318665,plain,
multiply(inverse(X1),X1) = inverse(multiply(inverse(c3),c3)),
inference(cp,[status(thm)],[t318658,t315113]) ).
cnf(t330918,plain,
multiply(inverse(X1),X1) = multiply(inverse(c3),c3),
inference(step,[status(thm)],[t318665,t314963]) ).
cnf(t318298,plain,
multiply(inverse(c3),c3) = inverse(inverse(inverse(inverse(multiply(X1,inverse(X1)))))),
inference(cp,[status(thm)],[t318297,t316303]) ).
cnf(t330913,plain,
multiply(inverse(c3),c3) = multiply(X1,inverse(X1)),
inference(step,[status(thm)],[t318298,t314498]) ).
cnf(t319067,plain,
multiply(inverse(c3),c3) = multiply(X1,inverse(X1)),
inference(orient,[status(thm)],[t330913]) ).
cnf(t330919,plain,
multiply(inverse(X1),X1) = multiply(c3,inverse(c3)),
inference(step,[status(thm)],[t330918,t319067]) ).
cnf(t319215,plain,
multiply(inverse(X1),X1) = multiply(c3,inverse(c3)),
inference(orient,[status(thm)],[t330919]) ).
cnf(t330927,plain,
inverse(multiply(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)),multiply(c3,inverse(c3)))) = multiply(inverse(c3),c3),
inference(step,[status(thm)],[t319213,t319215]) ).
cnf(t330928,plain,
inverse(multiply(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)),multiply(c3,inverse(c3)))) = multiply(c3,inverse(c3)),
inference(step,[status(thm)],[t330927,t319215]) ).
cnf(t319710,plain,
inverse(multiply(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)),multiply(c3,inverse(c3)))) = multiply(c3,inverse(c3)),
inference(orient,[status(thm)],[t330928]) ).
cnf(t319740,plain,
X1 = multiply(multiply(multiply(multiply(inverse(multiply(X2,X3)),multiply(X3,X2)),multiply(c3,inverse(c3))),multiply(c3,inverse(c3))),X1),
inference(cp,[status(thm)],[t318850,t319710]) ).
cnf(t318668,plain,
multiply(inverse(c3),c3) = inverse(multiply(X1,inverse(X1))),
inference(cp,[status(thm)],[t315113,t318658]) ).
cnf(t318961,plain,
inverse(multiply(X1,inverse(X1))) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t318668]) ).
cnf(t318967,plain,
X1 = multiply(multiply(X1,multiply(inverse(c3),c3)),multiply(X2,inverse(X2))),
inference(cp,[status(thm)],[t318738,t318961]) ).
cnf(t330926,plain,
X1 = multiply(multiply(X1,multiply(c3,inverse(c3))),multiply(X2,inverse(X2))),
inference(step,[status(thm)],[t318967,t319215]) ).
cnf(t319605,plain,
multiply(multiply(X1,multiply(c3,inverse(c3))),multiply(X2,inverse(X2))) = X1,
inference(orient,[status(thm)],[t330926]) ).
cnf(t330929,plain,
X1 = multiply(multiply(inverse(multiply(X2,X3)),multiply(X3,X2)),X1),
inference(step,[status(thm)],[t319740,t319605]) ).
cnf(t319818,plain,
multiply(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)),X3) = X3,
inference(orient,[status(thm)],[t330929]) ).
cnf(t319820,plain,
inverse(multiply(X1,X2)) = inverse(multiply(X2,X1)),
inference(cp,[status(thm)],[t319818,t318659]) ).
cnf(t319936,plain,
inverse(multiply(X1,X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t319820]) ).
cnf(t319944,plain,
multiply(X1,X2) = inverse(inverse(multiply(X2,X1))),
inference(cp,[status(thm)],[t318658,t319936]) ).
cnf(t330930,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(step,[status(thm)],[t319944,t318658]) ).
cnf(t319959,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(orient,[status(thm)],[t330930]) ).
cnf(t330933,plain,
multiply(X2,multiply(X1,inverse(X2))) = X1,
inference(step,[status(thm)],[t319965,t319959]) ).
cnf(t319977,plain,
multiply(X1,multiply(X2,inverse(X1))) = X2,
inference(orient,[status(thm)],[t330933]) ).
cnf(t319979,plain,
X1 = multiply(X2,multiply(inverse(X2),X1)),
inference(cp,[status(thm)],[t319977,t319959]) ).
cnf(t319989,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t319979]) ).
cnf(t330704,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(inverse(inverse(X5))))))),X4) = X5,
inference(step,[status(thm)],[t1383,t312430]) ).
cnf(t312705,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(inverse(inverse(X5))))))),X4) = X5,
inference(rw,[status(thm)],[t330704]) ).
cnf(t319963,plain,
multiply(multiply(X1,X2),inverse(X2)) = X1,
inference(rw,[status(thm)],[t318659]) ).
cnf(t330932,plain,
multiply(inverse(X2),multiply(X1,X2)) = X1,
inference(step,[status(thm)],[t319963,t319959]) ).
cnf(t319971,plain,
multiply(inverse(X1),multiply(X2,X1)) = X2,
inference(orient,[status(thm)],[t330932]) ).
cnf(t319976,plain,
inverse(X1) = multiply(inverse(multiply(X2,X1)),X2),
inference(cp,[status(thm)],[t319971,t319971]) ).
cnf(t330934,plain,
inverse(X1) = multiply(X2,inverse(multiply(X2,X1))),
inference(step,[status(thm)],[t319976,t319959]) ).
cnf(t319995,plain,
multiply(X1,inverse(multiply(X1,X2))) = inverse(X2),
inference(orient,[status(thm)],[t330934]) ).
cnf(t319997,plain,
inverse(multiply(inverse(X1),X2)) = multiply(X1,inverse(X2)),
inference(cp,[status(thm)],[t319995,t319989]) ).
cnf(t320007,plain,
inverse(multiply(inverse(X1),X2)) = multiply(X1,inverse(X2)),
inference(orient,[status(thm)],[t319997]) ).
cnf(t320020,plain,
multiply(multiply(inverse(X1),X2),inverse(X3)) = inverse(multiply(multiply(X1,inverse(X2)),X3)),
inference(cp,[status(thm)],[t320007,t320007]) ).
cnf(t320070,plain,
inverse(multiply(multiply(X1,inverse(X2)),X3)) = multiply(multiply(inverse(X1),X2),inverse(X3)),
inference(orient,[status(thm)],[t320020]) ).
cnf(t320000,plain,
inverse(multiply(X1,X2)) = multiply(inverse(X2),inverse(X1)),
inference(cp,[status(thm)],[t319995,t319971]) ).
cnf(t320043,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t320000]) ).
cnf(t319999,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(cp,[status(thm)],[t319995,t319977]) ).
cnf(t320026,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t319999]) ).
cnf(t320051,plain,
inverse(multiply(multiply(X1,inverse(X2)),X3)) = multiply(inverse(X3),multiply(X2,inverse(X1))),
inference(cp,[status(thm)],[t320043,t320026]) ).
cnf(t330937,plain,
multiply(multiply(inverse(X1),X2),inverse(X3)) = multiply(inverse(X3),multiply(X2,inverse(X1))),
inference(step,[status(thm)],[t320051,t320070]) ).
cnf(t320208,plain,
multiply(multiply(inverse(X1),X2),inverse(X3)) = multiply(inverse(X3),multiply(X2,inverse(X1))),
inference(orient,[status(thm)],[t330937]) ).
cnf(t320239,plain,
multiply(multiply(inverse(inverse(X1)),X2),inverse(inverse(X3))) = inverse(multiply(inverse(X3),multiply(inverse(X2),inverse(X1)))),
inference(cp,[status(thm)],[t320070,t320208]) ).
cnf(t330938,plain,
multiply(multiply(X1,X2),inverse(inverse(X3))) = inverse(multiply(inverse(X3),multiply(inverse(X2),inverse(X1)))),
inference(step,[status(thm)],[t320239,t318658]) ).
cnf(t330939,plain,
multiply(multiply(X1,X2),X3) = inverse(multiply(inverse(X3),multiply(inverse(X2),inverse(X1)))),
inference(step,[status(thm)],[t330938,t318658]) ).
cnf(t330940,plain,
multiply(multiply(X1,X2),X3) = multiply(X3,inverse(multiply(inverse(X2),inverse(X1)))),
inference(step,[status(thm)],[t330939,t320007]) ).
cnf(t330941,plain,
multiply(multiply(X1,X2),X3) = multiply(X3,multiply(X2,inverse(inverse(X1)))),
inference(step,[status(thm)],[t330940,t320007]) ).
cnf(t330942,plain,
multiply(multiply(X1,X2),X3) = multiply(X3,multiply(X2,X1)),
inference(step,[status(thm)],[t330941,t318658]) ).
cnf(t320278,plain,
multiply(multiply(X1,X2),X3) = multiply(X3,multiply(X2,X1)),
inference(orient,[status(thm)],[t330942]) ).
cnf(t320287,plain,
multiply(X1,multiply(inverse(X2),inverse(X3))) = multiply(inverse(multiply(X2,X3)),X1),
inference(cp,[status(thm)],[t320278,t320043]) ).
cnf(t330963,plain,
multiply(X1,inverse(multiply(X3,X2))) = multiply(inverse(multiply(X2,X3)),X1),
inference(step,[status(thm)],[t320287,t320043]) ).
cnf(t321988,plain,
multiply(X1,inverse(multiply(X2,X3))) = multiply(inverse(multiply(X3,X2)),X1),
inference(orient,[status(thm)],[t330963]) ).
cnf(t330982,plain,
multiply(X4,inverse(multiply(multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(inverse(inverse(X5))))),inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)))))) = X5,
inference(step,[status(thm)],[t312705,t321988]) ).
cnf(t320050,plain,
inverse(multiply(multiply(inverse(X1),X2),X3)) = multiply(inverse(X3),multiply(X1,inverse(X2))),
inference(cp,[status(thm)],[t320043,t320007]) ).
cnf(t320168,plain,
inverse(multiply(multiply(inverse(X1),X2),X3)) = multiply(inverse(X3),multiply(X1,inverse(X2))),
inference(orient,[status(thm)],[t320050]) ).
cnf(t330983,plain,
multiply(X4,multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)))),multiply(multiply(X3,inverse(X4)),inverse(multiply(X3,inverse(inverse(inverse(X5)))))))) = X5,
inference(step,[status(thm)],[t330982,t320168]) ).
cnf(t320047,plain,
inverse(multiply(X1,multiply(inverse(X2),X3))) = multiply(multiply(X2,inverse(X3)),inverse(X1)),
inference(cp,[status(thm)],[t320043,t320007]) ).
cnf(t320134,plain,
inverse(multiply(X1,multiply(inverse(X2),X3))) = multiply(multiply(X2,inverse(X3)),inverse(X1)),
inference(orient,[status(thm)],[t320047]) ).
cnf(t320154,plain,
inverse(multiply(multiply(X1,multiply(inverse(X2),X3)),X4)) = multiply(inverse(X4),multiply(multiply(X2,inverse(X3)),inverse(X1))),
inference(cp,[status(thm)],[t320043,t320134]) ).
cnf(t323007,plain,
multiply(inverse(X1),multiply(multiply(X2,inverse(X3)),inverse(X4))) = inverse(multiply(multiply(X4,multiply(inverse(X2),X3)),X1)),
inference(orient,[status(thm)],[t320154]) ).
cnf(t330984,plain,
multiply(X4,inverse(multiply(multiply(multiply(X3,inverse(inverse(inverse(X5)))),multiply(inverse(X3),X4)),inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)))))) = X5,
inference(step,[status(thm)],[t330983,t323007]) ).
cnf(t330985,plain,
multiply(X4,multiply(multiply(inverse(multiply(X1,X2)),multiply(X2,X1)),inverse(multiply(multiply(X3,inverse(inverse(inverse(X5)))),multiply(inverse(X3),X4))))) = X5,
inference(step,[status(thm)],[t330984,t320026]) ).
cnf(t330986,plain,
multiply(X4,multiply(multiply(multiply(X2,X1),inverse(multiply(X2,X1))),inverse(multiply(multiply(X3,inverse(inverse(inverse(X5)))),multiply(inverse(X3),X4))))) = X5,
inference(step,[status(thm)],[t330985,t321988]) ).
cnf(t318852,plain,
multiply(X1,inverse(X1)) = multiply(X2,inverse(X2)),
inference(cp,[status(thm)],[t318659,t318850]) ).
cnf(t319457,plain,
multiply(X1,inverse(X1)) = multiply(X2,inverse(X2)),
inference(orient,[status(thm)],[t318852]) ).
cnf(t330987,plain,
multiply(X4,multiply(multiply(c3,inverse(c3)),inverse(multiply(multiply(X3,inverse(inverse(inverse(X5)))),multiply(inverse(X3),X4))))) = X5,
inference(step,[status(thm)],[t330986,t319457]) ).
cnf(t330988,plain,
multiply(X4,inverse(multiply(multiply(X3,inverse(inverse(inverse(X5)))),multiply(inverse(X3),X4)))) = X5,
inference(step,[status(thm)],[t330987,t318850]) ).
cnf(t330989,plain,
multiply(X4,multiply(multiply(inverse(X3),inverse(inverse(X5))),inverse(multiply(inverse(X3),X4)))) = X5,
inference(step,[status(thm)],[t330988,t320070]) ).
cnf(t330990,plain,
multiply(X4,multiply(inverse(multiply(inverse(X5),X3)),inverse(multiply(inverse(X3),X4)))) = X5,
inference(step,[status(thm)],[t330989,t320043]) ).
cnf(t330991,plain,
multiply(X4,multiply(multiply(X5,inverse(X3)),inverse(multiply(inverse(X3),X4)))) = X5,
inference(step,[status(thm)],[t330990,t320007]) ).
cnf(t330992,plain,
multiply(X4,multiply(multiply(X5,inverse(X3)),multiply(X3,inverse(X4)))) = X5,
inference(step,[status(thm)],[t330991,t320007]) ).
cnf(t329633,plain,
multiply(X1,multiply(multiply(X2,inverse(X3)),multiply(X3,inverse(X1)))) = X2,
inference(orient,[status(thm)],[t330992]) ).
cnf(t329732,plain,
multiply(multiply(X1,inverse(X2)),multiply(X2,inverse(inverse(X3)))) = multiply(X3,X1),
inference(cp,[status(thm)],[t319989,t329633]) ).
cnf(t330993,plain,
multiply(multiply(X1,inverse(X2)),multiply(X2,X3)) = multiply(X3,X1),
inference(step,[status(thm)],[t329732,t318658]) ).
cnf(t329855,plain,
multiply(multiply(X1,inverse(X2)),multiply(X2,X3)) = multiply(X3,X1),
inference(orient,[status(thm)],[t330993]) ).
cnf(t320308,plain,
multiply(multiply(X1,X2),multiply(X3,X4)) = multiply(multiply(X2,X1),multiply(X4,X3)),
inference(cp,[status(thm)],[t320278,t320278]) ).
cnf(t324533,plain,
multiply(multiply(X1,X2),multiply(X3,X4)) = multiply(multiply(X2,X1),multiply(X4,X3)),
inference(orient,[status(thm)],[t320308]) ).
cnf(t324542,plain,
multiply(multiply(X1,X2),multiply(X3,X4)) = multiply(multiply(X4,X3),multiply(X2,X1)),
inference(cp,[status(thm)],[t324533,t319959]) ).
cnf(t325793,plain,
multiply(multiply(X1,X2),multiply(X3,X4)) = multiply(multiply(X4,X3),multiply(X2,X1)),
inference(orient,[status(thm)],[t324542]) ).
cnf(t329868,plain,
multiply(X1,X2) = multiply(multiply(X1,X3),multiply(inverse(X3),X2)),
inference(cp,[status(thm)],[t329855,t325793]) ).
cnf(t330104,plain,
multiply(multiply(X1,X2),multiply(inverse(X2),X3)) = multiply(X1,X3),
inference(orient,[status(thm)],[t329868]) ).
cnf(t330184,plain,
multiply(X1,multiply(X2,X3)) = multiply(multiply(X1,X3),X2),
inference(cp,[status(thm)],[t330104,t319971]) ).
cnf(t330346,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X3,X2)),
inference(orient,[status(thm)],[t330184]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(a3,multiply(c3,b3)) != multiply(a3,multiply(b3,c3)),
inference(rw,[status(thm)],[goal_0,t330346]) ).
cnf(g0_1,plain,
multiply(a3,multiply(c3,b3)) != multiply(a3,multiply(c3,b3)),
inference(rw,[status(thm)],[g0_0,t319959]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP507-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n004.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 14:56:35 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 44.42/6.97 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 44.42/6.97 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------