%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP420-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 : n013.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:26:38 PM UTC 2026
% Result : Unsatisfiable 42.49s 5.88s
% Output : CNFRefutation 42.49s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3))) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t1,plain,
inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3))) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t2,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)) = inverse(multiply(inverse(multiply(Y3,inverse(multiply(X2,inverse(multiply(Y4,inverse(multiply(inverse(Y4),Y4)))))))),multiply(Y3,Y4))),
inference(cp,[status(thm)],[t1,t1]) ).
cnf(t4,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)) = inverse(multiply(inverse(multiply(Y3,inverse(multiply(X2,inverse(multiply(Y4,inverse(multiply(inverse(Y4),Y4)))))))),multiply(Y3,Y4))),
inference(orient,[status(thm)],[t2]) ).
cnf(t12,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)) = multiply(inverse(multiply(Y3,inverse(multiply(inverse(X2),inverse(multiply(Y4,inverse(multiply(inverse(Y4),Y4)))))))),multiply(Y3,Y4)),
inference(cp,[status(thm)],[t4,t4]) ).
cnf(t28,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)) = multiply(inverse(multiply(Y3,inverse(multiply(inverse(X2),inverse(multiply(Y4,inverse(multiply(inverse(Y4),Y4)))))))),multiply(Y3,Y4)),
inference(orient,[status(thm)],[t12]) ).
cnf(t13,plain,
inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3))) = X2,
inference(rw,[status(thm)],[t1]) ).
cnf(t90469,plain,
multiply(inverse(multiply(c3,inverse(multiply(inverse(inverse(X2)),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),multiply(c3,c3)) = X2,
inference(step,[status(thm)],[t13,t4]) ).
cnf(t14,plain,
multiply(inverse(multiply(c3,inverse(multiply(inverse(inverse(X1)),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),multiply(c3,c3)) = X1,
inference(orient,[status(thm)],[t90469]) ).
cnf(t29,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X2)),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)) = X2,
inference(cp,[status(thm)],[t28,t14]) ).
cnf(t42,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X2)),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)) = X2,
inference(orient,[status(thm)],[t29]) ).
cnf(t48,plain,
X1 = multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(inverse(X3)),inverse(multiply(Y3,inverse(multiply(inverse(Y3),Y3)))))))),inverse(multiply(inverse(inverse(X1)),inverse(multiply(multiply(X2,Y3),inverse(multiply(inverse(multiply(X2,Y3)),multiply(X2,Y3))))))))),X3),
inference(cp,[status(thm)],[t42,t42]) ).
cnf(t52,plain,
multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X2)),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),inverse(multiply(inverse(inverse(Y3)),inverse(multiply(multiply(X1,X3),inverse(multiply(inverse(multiply(X1,X3)),multiply(X1,X3))))))))),X2) = Y3,
inference(orient,[status(thm)],[t48]) ).
cnf(t67,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(inverse(X3)),inverse(multiply(Y3,inverse(multiply(inverse(Y3),Y3)))))))),inverse(multiply(inverse(inverse(Y4)),inverse(multiply(multiply(X2,Y3),inverse(multiply(inverse(multiply(X2,Y3)),multiply(X2,Y3))))))))),inverse(multiply(inverse(inverse(X1)),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),Y4),
inference(cp,[status(thm)],[t42,t52]) ).
cnf(t111,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X2)),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),inverse(multiply(inverse(inverse(Y3)),inverse(multiply(multiply(X1,X3),inverse(multiply(inverse(multiply(X1,X3)),multiply(X1,X3))))))))),inverse(multiply(inverse(inverse(Y4)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),Y3) = Y4,
inference(orient,[status(thm)],[t67]) ).
cnf(t152,plain,
inverse(multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(inverse(X3)),inverse(multiply(Y3,inverse(multiply(inverse(Y3),Y3)))))))),inverse(multiply(inverse(inverse(inverse(multiply(Y4,inverse(multiply(inverse(Y4),Y4)))))),inverse(multiply(multiply(X2,Y3),inverse(multiply(inverse(multiply(X2,Y3)),multiply(X2,Y3))))))))),inverse(multiply(inverse(inverse(Y5)),inverse(multiply(X3,inverse(multiply(inverse(X3),X3))))))),inverse(multiply(Y6,inverse(multiply(inverse(Y6),Y6)))))))),multiply(X1,Y6))) = multiply(inverse(multiply(Y7,inverse(Y5))),multiply(Y7,Y4)),
inference(cp,[status(thm)],[t4,t111]) ).
cnf(t90475,plain,
multiply(inverse(multiply(c3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(inverse(X3)),inverse(multiply(Y3,inverse(multiply(inverse(Y3),Y3)))))))),inverse(multiply(inverse(inverse(inverse(multiply(Y4,inverse(multiply(inverse(Y4),Y4)))))),inverse(multiply(multiply(X2,Y3),inverse(multiply(inverse(multiply(X2,Y3)),multiply(X2,Y3))))))))),inverse(multiply(inverse(inverse(Y5)),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),multiply(c3,c3)) = multiply(inverse(multiply(Y7,inverse(Y5))),multiply(Y7,Y4)),
inference(step,[status(thm)],[t152,t4]) ).
cnf(t1597,plain,
multiply(inverse(multiply(c3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X2)),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),inverse(multiply(inverse(inverse(inverse(multiply(Y3,inverse(multiply(inverse(Y3),Y3)))))),inverse(multiply(multiply(X1,X3),inverse(multiply(inverse(multiply(X1,X3)),multiply(X1,X3))))))))),inverse(multiply(inverse(inverse(Y4)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),multiply(c3,c3)) = multiply(inverse(multiply(Y5,inverse(Y4))),multiply(Y5,Y3)),
inference(orient,[status(thm)],[t90475]) ).
cnf(t1708,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X3)) = multiply(inverse(multiply(Y3,inverse(X2))),multiply(Y3,X3)),
inference(cp,[status(thm)],[t1597,t1597]) ).
cnf(t1958,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X3)) = multiply(inverse(multiply(Y3,inverse(X2))),multiply(Y3,X3)),
inference(orient,[status(thm)],[t1708]) ).
cnf(t1976,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,multiply(X3,Y3))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(inverse(Y4)),inverse(multiply(Y3,inverse(multiply(inverse(Y3),Y3)))))))),inverse(X2))),Y4),
inference(cp,[status(thm)],[t1958,t42]) ).
cnf(t2413,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,multiply(X3,Y3))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(inverse(Y4)),inverse(multiply(Y3,inverse(multiply(inverse(Y3),Y3)))))))),inverse(X2))),Y4),
inference(orient,[status(thm)],[t1976]) ).
cnf(t2511,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X3)) = multiply(inverse(multiply(inverse(multiply(Y3,inverse(Y4))),multiply(Y3,multiply(Y5,Y6)))),multiply(inverse(multiply(inverse(multiply(Y5,inverse(multiply(inverse(inverse(inverse(X2))),inverse(multiply(Y6,inverse(multiply(inverse(Y6),Y6)))))))),inverse(Y4))),X3)),
inference(cp,[status(thm)],[t1958,t2413]) ).
cnf(t3123,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X3)) = multiply(inverse(multiply(inverse(multiply(Y3,inverse(Y4))),multiply(Y3,multiply(Y5,Y6)))),multiply(inverse(multiply(inverse(multiply(Y5,inverse(multiply(inverse(inverse(inverse(X2))),inverse(multiply(Y6,inverse(multiply(inverse(Y6),Y6)))))))),inverse(Y4))),X3)),
inference(orient,[status(thm)],[t2511]) ).
cnf(t3321,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X2))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(Y3))),multiply(X3,multiply(Y4,Y5)))),multiply(inverse(multiply(Y6,inverse(Y3))),multiply(Y6,multiply(Y4,Y5)))),
inference(cp,[status(thm)],[t3123,t2413]) ).
cnf(t3433,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X2))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(Y3))),multiply(X3,multiply(Y4,Y5)))),multiply(inverse(multiply(Y6,inverse(Y3))),multiply(Y6,multiply(Y4,Y5)))),
inference(orient,[status(thm)],[t3321]) ).
cnf(t3547,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X2))) = multiply(inverse(X3),multiply(inverse(multiply(Y3,inverse(multiply(inverse(inverse(X3)),inverse(multiply(multiply(Y4,Y5),inverse(multiply(inverse(multiply(Y4,Y5)),multiply(Y4,Y5))))))))),multiply(Y3,multiply(Y4,Y5)))),
inference(cp,[status(thm)],[t3433,t42]) ).
cnf(t90477,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X2))) = multiply(inverse(X3),X3),
inference(step,[status(thm)],[t3547,t42]) ).
cnf(t3752,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X2))) = multiply(inverse(X3),X3),
inference(orient,[status(thm)],[t90477]) ).
cnf(t3840,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),X2),
inference(cp,[status(thm)],[t3752,t3752]) ).
cnf(t3991,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),X2),
inference(orient,[status(thm)],[t3840]) ).
cnf(t3998,plain,
X1 = multiply(inverse(multiply(X2,inverse(multiply(inverse(inverse(X1)),inverse(multiply(X3,inverse(multiply(inverse(Y3),Y3)))))))),multiply(X2,X3)),
inference(cp,[status(thm)],[t42,t3991]) ).
cnf(t4548,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X2)),inverse(multiply(X3,inverse(multiply(inverse(Y3),Y3)))))))),multiply(X1,X3)) = X2,
inference(orient,[status(thm)],[t3998]) ).
cnf(t4002,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X3)) = multiply(inverse(multiply(inverse(Y3),Y3)),multiply(inverse(inverse(X2)),X3)),
inference(cp,[status(thm)],[t1958,t3991]) ).
cnf(t4165,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X3)) = multiply(inverse(multiply(inverse(Y3),Y3)),multiply(inverse(inverse(X2)),X3)),
inference(orient,[status(thm)],[t4002]) ).
cnf(t4251,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X2))) = multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(Y3),Y3)),
inference(cp,[status(thm)],[t4165,t3991]) ).
cnf(t90478,plain,
multiply(inverse(c3),c3) = multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(Y3),Y3)),
inference(step,[status(thm)],[t4251,t3752]) ).
cnf(t4431,plain,
multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X2),X2)) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t90478]) ).
cnf(t3997,plain,
multiply(X1,inverse(multiply(inverse(X1),X1))) = multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),X3)))),multiply(X2,X1)),
inference(cp,[status(thm)],[t42,t3991]) ).
cnf(t4055,plain,
multiply(X1,inverse(multiply(inverse(X1),X1))) = multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),X3)))),multiply(X2,X1)),
inference(orient,[status(thm)],[t3997]) ).
cnf(t4436,plain,
multiply(inverse(c3),c3) = multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))),
inference(cp,[status(thm)],[t4431,t4055]) ).
cnf(t90479,plain,
multiply(inverse(c3),c3) = multiply(inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))),multiply(c3,inverse(multiply(inverse(X1),X1)))),
inference(step,[status(thm)],[t4436,t4055]) ).
cnf(t4615,plain,
multiply(inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))),multiply(c3,inverse(multiply(inverse(X1),X1)))) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t90479]) ).
cnf(t4616,plain,
multiply(inverse(c3),c3) = multiply(inverse(multiply(X1,inverse(multiply(inverse(c3),c3)))),multiply(X1,inverse(multiply(inverse(X2),X2)))),
inference(cp,[status(thm)],[t4615,t1958]) ).
cnf(t4652,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(c3),c3)))),multiply(X1,inverse(multiply(inverse(X2),X2)))) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t4616]) ).
cnf(t4660,plain,
multiply(inverse(c3),c3) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),multiply(X1,inverse(multiply(inverse(X3),X3)))),
inference(cp,[status(thm)],[t4652,t3991]) ).
cnf(t4701,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),multiply(X1,inverse(multiply(inverse(X3),X3)))) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t4660]) ).
cnf(t4702,plain,
multiply(inverse(c3),c3) = multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(X2),X2))),
inference(cp,[status(thm)],[t4701,t4548]) ).
cnf(t4758,plain,
multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(X2),X2))) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t4702]) ).
cnf(t4764,plain,
multiply(X1,inverse(multiply(inverse(X2),X2))) = multiply(inverse(multiply(inverse(c3),c3)),multiply(inverse(multiply(inverse(X3),X3)),X1)),
inference(cp,[status(thm)],[t4548,t4758]) ).
cnf(t5574,plain,
multiply(X1,inverse(multiply(inverse(X2),X2))) = multiply(inverse(multiply(inverse(c3),c3)),multiply(inverse(multiply(inverse(X3),X3)),X1)),
inference(orient,[status(thm)],[t4764]) ).
cnf(t5689,plain,
multiply(X1,inverse(multiply(inverse(X2),X2))) = multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(multiply(inverse(Y3),Y3)),X1)),
inference(cp,[status(thm)],[t5574,t3991]) ).
cnf(t5889,plain,
multiply(X1,inverse(multiply(inverse(X2),X2))) = multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(multiply(inverse(Y3),Y3)),X1)),
inference(orient,[status(thm)],[t5689]) ).
cnf(t6029,plain,
multiply(multiply(inverse(inverse(X1)),X2),inverse(multiply(inverse(X3),X3))) = multiply(inverse(multiply(inverse(Y3),Y3)),multiply(inverse(multiply(Y4,inverse(X1))),multiply(Y4,X2))),
inference(cp,[status(thm)],[t5889,t4165]) ).
cnf(t14351,plain,
multiply(multiply(inverse(inverse(X1)),X2),inverse(multiply(inverse(X3),X3))) = multiply(inverse(multiply(inverse(Y3),Y3)),multiply(inverse(multiply(Y4,inverse(X1))),multiply(Y4,X2))),
inference(orient,[status(thm)],[t6029]) ).
cnf(t44,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)) = multiply(inverse(multiply(Y3,inverse(multiply(inverse(multiply(inverse(multiply(Y4,inverse(multiply(inverse(X2),inverse(multiply(Y5,inverse(multiply(inverse(Y5),Y5)))))))),multiply(Y4,Y5))),inverse(multiply(Y6,inverse(multiply(inverse(Y6),Y6)))))))),multiply(Y3,Y6)),
inference(cp,[status(thm)],[t42,t4]) ).
cnf(t90470,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)) = multiply(inverse(multiply(Y3,inverse(multiply(multiply(inverse(multiply(c3,inverse(multiply(inverse(inverse(X2)),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),multiply(c3,c3)),inverse(multiply(Y6,inverse(multiply(inverse(Y6),Y6)))))))),multiply(Y3,Y6)),
inference(step,[status(thm)],[t44,t4]) ).
cnf(t90471,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)) = multiply(inverse(multiply(Y3,inverse(multiply(X2,inverse(multiply(Y6,inverse(multiply(inverse(Y6),Y6)))))))),multiply(Y3,Y6)),
inference(step,[status(thm)],[t90470,t14]) ).
cnf(t157,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)) = multiply(inverse(multiply(Y3,inverse(multiply(X2,inverse(multiply(Y4,inverse(multiply(inverse(Y4),Y4)))))))),multiply(Y3,Y4)),
inference(orient,[status(thm)],[t90471]) ).
cnf(t4032,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,multiply(X3,Y3))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(Y4),Y4)))),inverse(X2))),multiply(Y3,inverse(multiply(inverse(Y3),Y3)))),
inference(cp,[status(thm)],[t2413,t3991]) ).
cnf(t78673,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,multiply(X3,Y3))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(Y4),Y4)))),inverse(X2))),multiply(Y3,inverse(multiply(inverse(Y3),Y3)))),
inference(orient,[status(thm)],[t4032]) ).
cnf(t79277,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,multiply(X3,inverse(multiply(X3,inverse(multiply(inverse(Y3),Y3))))))) = multiply(inverse(multiply(Y4,inverse(X2))),multiply(Y4,inverse(multiply(inverse(inverse(multiply(X3,inverse(multiply(inverse(Y3),Y3))))),inverse(multiply(X3,inverse(multiply(inverse(Y3),Y3)))))))),
inference(cp,[status(thm)],[t78673,t1958]) ).
cnf(t4452,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),multiply(X1,multiply(inverse(X3),X3))) = multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(c3),c3))),
inference(cp,[status(thm)],[t4055,t4431]) ).
cnf(t4478,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),multiply(X1,multiply(inverse(X3),X3))) = multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(c3),c3))),
inference(orient,[status(thm)],[t4452]) ).
cnf(t4763,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(c3),c3))) = multiply(inverse(multiply(inverse(c3),c3)),multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X1),X1))),
inference(cp,[status(thm)],[t4478,t4758]) ).
cnf(t90480,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(c3),c3))) = multiply(inverse(multiply(inverse(c3),c3)),multiply(inverse(c3),c3)),
inference(step,[status(thm)],[t4763,t4431]) ).
cnf(t90481,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(c3),c3))) = multiply(inverse(c3),c3),
inference(step,[status(thm)],[t90480,t4431]) ).
cnf(t4809,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(c3),c3))) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t90481]) ).
cnf(t4814,plain,
multiply(inverse(c3),c3) = multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X2),X2))),
inference(cp,[status(thm)],[t4809,t3991]) ).
cnf(t4847,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X2),X2))) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t4814]) ).
cnf(t4863,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(inverse(X3),X3)))) = multiply(inverse(multiply(multiply(inverse(Y3),Y3),inverse(X2))),multiply(inverse(c3),c3)),
inference(cp,[status(thm)],[t1958,t4847]) ).
cnf(t13692,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(inverse(X3),X3)))) = multiply(inverse(multiply(multiply(inverse(Y3),Y3),inverse(X2))),multiply(inverse(c3),c3)),
inference(orient,[status(thm)],[t4863]) ).
cnf(t13696,plain,
multiply(inverse(multiply(multiply(inverse(X1),X1),inverse(X2))),multiply(inverse(c3),c3)) = multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(multiply(inverse(Y3),Y3)))),
inference(cp,[status(thm)],[t13692,t1958]) ).
cnf(t90512,plain,
multiply(inverse(multiply(c3,inverse(X2))),multiply(c3,inverse(multiply(inverse(c3),c3)))) = multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(multiply(inverse(Y3),Y3)))),
inference(step,[status(thm)],[t13696,t13692]) ).
cnf(t15768,plain,
multiply(inverse(multiply(c3,inverse(X1))),multiply(c3,inverse(multiply(inverse(c3),c3)))) = multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(multiply(inverse(X3),X3)))),
inference(orient,[status(thm)],[t90512]) ).
cnf(t4853,plain,
multiply(X1,inverse(multiply(inverse(X2),X2))) = multiply(inverse(multiply(inverse(c3),c3)),multiply(multiply(inverse(X3),X3),X1)),
inference(cp,[status(thm)],[t4548,t4847]) ).
cnf(t5265,plain,
multiply(X1,inverse(multiply(inverse(X2),X2))) = multiply(inverse(multiply(inverse(c3),c3)),multiply(multiply(inverse(X3),X3),X1)),
inference(orient,[status(thm)],[t4853]) ).
cnf(t5378,plain,
multiply(X1,inverse(multiply(inverse(X2),X2))) = multiply(inverse(multiply(inverse(X3),X3)),multiply(multiply(inverse(Y3),Y3),X1)),
inference(cp,[status(thm)],[t5265,t3991]) ).
cnf(t5412,plain,
multiply(X1,inverse(multiply(inverse(X2),X2))) = multiply(inverse(multiply(inverse(X3),X3)),multiply(multiply(inverse(Y3),Y3),X1)),
inference(orient,[status(thm)],[t5378]) ).
cnf(t6030,plain,
multiply(multiply(multiply(inverse(X1),X1),X2),inverse(multiply(inverse(X3),X3))) = multiply(inverse(multiply(inverse(Y3),Y3)),multiply(X2,inverse(multiply(inverse(Y4),Y4)))),
inference(cp,[status(thm)],[t5889,t5412]) ).
cnf(t9348,plain,
multiply(multiply(multiply(inverse(X1),X1),X2),inverse(multiply(inverse(X3),X3))) = multiply(inverse(multiply(inverse(Y3),Y3)),multiply(X2,inverse(multiply(inverse(Y4),Y4)))),
inference(orient,[status(thm)],[t6030]) ).
cnf(t15892,plain,
multiply(inverse(multiply(c3,inverse(X1))),multiply(c3,inverse(multiply(inverse(c3),c3)))) = multiply(multiply(multiply(inverse(X2),X2),inverse(inverse(X1))),inverse(multiply(inverse(X3),X3))),
inference(cp,[status(thm)],[t15768,t9348]) ).
cnf(t16084,plain,
multiply(multiply(multiply(inverse(X1),X1),inverse(inverse(X2))),inverse(multiply(inverse(X3),X3))) = multiply(inverse(multiply(c3,inverse(X2))),multiply(c3,inverse(multiply(inverse(c3),c3)))),
inference(orient,[status(thm)],[t15892]) ).
cnf(t16085,plain,
multiply(inverse(multiply(c3,inverse(X1))),multiply(c3,inverse(multiply(inverse(c3),c3)))) = multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(inverse(X1)),inverse(multiply(inverse(X3),X3)))),
inference(cp,[status(thm)],[t16084,t9348]) ).
cnf(t15952,plain,
multiply(inverse(multiply(c3,inverse(X1))),multiply(c3,inverse(multiply(inverse(c3),c3)))) = multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),inverse(X1))),multiply(inverse(c3),c3)),
inference(cp,[status(thm)],[t15768,t4758]) ).
cnf(t4003,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X3)) = multiply(inverse(multiply(inverse(X3),inverse(X2))),multiply(inverse(Y3),Y3)),
inference(cp,[status(thm)],[t1958,t3991]) ).
cnf(t4289,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X3)) = multiply(inverse(multiply(inverse(X3),inverse(X2))),multiply(inverse(Y3),Y3)),
inference(orient,[status(thm)],[t4003]) ).
cnf(t90513,plain,
multiply(inverse(multiply(c3,inverse(X1))),multiply(c3,inverse(multiply(inverse(c3),c3)))) = multiply(inverse(multiply(c3,inverse(X1))),multiply(c3,multiply(inverse(X2),X2))),
inference(step,[status(thm)],[t15952,t4289]) ).
cnf(t16211,plain,
multiply(inverse(multiply(c3,inverse(X1))),multiply(c3,inverse(multiply(inverse(c3),c3)))) = multiply(inverse(multiply(c3,inverse(X1))),multiply(c3,multiply(inverse(X2),X2))),
inference(orient,[status(thm)],[t90513]) ).
cnf(t90516,plain,
multiply(inverse(multiply(c3,inverse(X1))),multiply(c3,multiply(inverse(c3),c3))) = multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(inverse(X1)),inverse(multiply(inverse(X3),X3)))),
inference(step,[status(thm)],[t16085,t16211]) ).
cnf(t90517,plain,
multiply(inverse(multiply(c3,inverse(X1))),multiply(c3,multiply(inverse(c3),c3))) = multiply(inverse(multiply(c3,inverse(X1))),multiply(c3,inverse(multiply(inverse(X3),X3)))),
inference(step,[status(thm)],[t90516,t4165]) ).
cnf(t16411,plain,
multiply(inverse(multiply(c3,inverse(X1))),multiply(c3,inverse(multiply(inverse(X2),X2)))) = multiply(inverse(multiply(c3,inverse(X1))),multiply(c3,multiply(inverse(c3),c3))),
inference(orient,[status(thm)],[t90517]) ).
cnf(t16413,plain,
multiply(inverse(multiply(c3,inverse(X1))),multiply(c3,multiply(inverse(c3),c3))) = multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(multiply(inverse(X3),X3)))),
inference(cp,[status(thm)],[t16411,t1958]) ).
cnf(t16541,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(inverse(X3),X3)))) = multiply(inverse(multiply(c3,inverse(X2))),multiply(c3,multiply(inverse(c3),c3))),
inference(orient,[status(thm)],[t16413]) ).
cnf(t90607,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,multiply(X3,inverse(multiply(X3,inverse(multiply(inverse(Y3),Y3))))))) = multiply(inverse(multiply(c3,inverse(X2))),multiply(c3,multiply(inverse(c3),c3))),
inference(step,[status(thm)],[t79277,t16541]) ).
cnf(t80287,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,multiply(X3,inverse(multiply(X3,inverse(multiply(inverse(Y3),Y3))))))) = multiply(inverse(multiply(c3,inverse(X2))),multiply(c3,multiply(inverse(c3),c3))),
inference(orient,[status(thm)],[t90607]) ).
cnf(t9604,plain,
multiply(multiply(multiply(inverse(X1),X1),X2),inverse(multiply(inverse(X3),X3))) = multiply(multiply(multiply(inverse(Y3),Y3),X2),inverse(multiply(inverse(Y4),Y4))),
inference(cp,[status(thm)],[t9348,t9348]) ).
cnf(t10106,plain,
multiply(multiply(multiply(inverse(X1),X1),X2),inverse(multiply(inverse(X3),X3))) = multiply(multiply(multiply(inverse(Y3),Y3),X2),inverse(multiply(inverse(Y4),Y4))),
inference(orient,[status(thm)],[t9604]) ).
cnf(t10168,plain,
multiply(X1,inverse(multiply(inverse(X2),X2))) = multiply(inverse(multiply(multiply(multiply(inverse(X3),X3),Y3),inverse(multiply(inverse(Y4),Y4)))),multiply(multiply(multiply(inverse(Y5),Y5),Y3),X1)),
inference(cp,[status(thm)],[t4548,t10106]) ).
cnf(t38443,plain,
multiply(X1,inverse(multiply(inverse(X2),X2))) = multiply(inverse(multiply(multiply(multiply(inverse(X3),X3),Y3),inverse(multiply(inverse(Y4),Y4)))),multiply(multiply(multiply(inverse(Y5),Y5),Y3),X1)),
inference(orient,[status(thm)],[t10168]) ).
cnf(t80306,plain,
multiply(inverse(multiply(c3,inverse(multiply(inverse(X1),X1)))),multiply(c3,multiply(inverse(c3),c3))) = multiply(multiply(X2,inverse(multiply(X2,inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(Y3),Y3))),
inference(cp,[status(thm)],[t80287,t38443]) ).
cnf(t90482,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),multiply(X1,multiply(inverse(X3),X3))) = multiply(inverse(c3),c3),
inference(step,[status(thm)],[t4478,t4809]) ).
cnf(t4810,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),multiply(X1,multiply(inverse(X3),X3))) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t90482]) ).
cnf(t90608,plain,
multiply(inverse(c3),c3) = multiply(multiply(X2,inverse(multiply(X2,inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(Y3),Y3))),
inference(step,[status(thm)],[t80306,t4810]) ).
cnf(t80689,plain,
multiply(multiply(X1,inverse(multiply(X1,inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X3),X3))) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t90608]) ).
cnf(t80894,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)) = multiply(inverse(multiply(Y3,inverse(multiply(X2,inverse(multiply(inverse(c3),c3)))))),multiply(Y3,multiply(Y4,inverse(multiply(Y4,inverse(multiply(inverse(Y5),Y5))))))),
inference(cp,[status(thm)],[t157,t80689]) ).
cnf(t90611,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)) = multiply(inverse(multiply(c3,inverse(multiply(X2,inverse(multiply(inverse(c3),c3)))))),multiply(c3,multiply(inverse(c3),c3))),
inference(step,[status(thm)],[t80894,t80287]) ).
cnf(t85029,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)) = multiply(inverse(multiply(c3,inverse(multiply(X2,inverse(multiply(inverse(c3),c3)))))),multiply(c3,multiply(inverse(c3),c3))),
inference(orient,[status(thm)],[t90611]) ).
cnf(t90612,plain,
multiply(inverse(multiply(c3,inverse(multiply(inverse(X2),inverse(multiply(inverse(c3),c3)))))),multiply(c3,multiply(inverse(c3),c3))) = inverse(multiply(inverse(multiply(Y3,inverse(multiply(X2,inverse(multiply(Y4,inverse(multiply(inverse(Y4),Y4)))))))),multiply(Y3,Y4))),
inference(step,[status(thm)],[t4,t85029]) ).
cnf(t90613,plain,
multiply(inverse(multiply(c3,inverse(multiply(inverse(X2),inverse(multiply(inverse(c3),c3)))))),multiply(c3,multiply(inverse(c3),c3))) = inverse(multiply(inverse(multiply(c3,inverse(multiply(X2,inverse(multiply(inverse(c3),c3)))))),multiply(c3,multiply(inverse(c3),c3)))),
inference(step,[status(thm)],[t90612,t85029]) ).
cnf(t85602,plain,
multiply(inverse(multiply(c3,inverse(multiply(inverse(X2),inverse(multiply(inverse(c3),c3)))))),multiply(c3,multiply(inverse(c3),c3))) = inverse(multiply(inverse(multiply(c3,inverse(multiply(X2,inverse(multiply(inverse(c3),c3)))))),multiply(c3,multiply(inverse(c3),c3)))),
inference(rw,[status(thm)],[t90613]) ).
cnf(t86736,plain,
inverse(multiply(inverse(multiply(c3,inverse(multiply(X1,inverse(multiply(inverse(c3),c3)))))),multiply(c3,multiply(inverse(c3),c3)))) = multiply(inverse(multiply(c3,inverse(multiply(inverse(X1),inverse(multiply(inverse(c3),c3)))))),multiply(c3,multiply(inverse(c3),c3))),
inference(orient,[status(thm)],[t85602]) ).
cnf(t86809,plain,
multiply(inverse(multiply(c3,inverse(multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(c3),c3)))))),multiply(c3,multiply(inverse(c3),c3))) = inverse(multiply(inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))),multiply(c3,multiply(inverse(c3),c3)))),
inference(cp,[status(thm)],[t86736,t4847]) ).
cnf(t90614,plain,
multiply(inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))),multiply(c3,multiply(inverse(c3),c3))) = inverse(multiply(inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))),multiply(c3,multiply(inverse(c3),c3)))),
inference(step,[status(thm)],[t86809,t4758]) ).
cnf(t90615,plain,
multiply(inverse(c3),c3) = inverse(multiply(inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))),multiply(c3,multiply(inverse(c3),c3)))),
inference(step,[status(thm)],[t90614,t4810]) ).
cnf(t90616,plain,
multiply(inverse(c3),c3) = inverse(multiply(inverse(c3),c3)),
inference(step,[status(thm)],[t90615,t4810]) ).
cnf(t87565,plain,
inverse(multiply(inverse(c3),c3)) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t90616]) ).
cnf(t87594,plain,
multiply(inverse(c3),c3) = inverse(multiply(inverse(X1),X1)),
inference(cp,[status(thm)],[t87565,t3991]) ).
cnf(t88542,plain,
inverse(multiply(inverse(X1),X1)) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t87594]) ).
cnf(t90659,plain,
multiply(multiply(inverse(inverse(X1)),X2),multiply(inverse(c3),c3)) = multiply(inverse(multiply(inverse(Y3),Y3)),multiply(inverse(multiply(Y4,inverse(X1))),multiply(Y4,X2))),
inference(step,[status(thm)],[t14351,t88542]) ).
cnf(t90660,plain,
multiply(multiply(inverse(inverse(X1)),X2),multiply(inverse(c3),c3)) = multiply(multiply(inverse(c3),c3),multiply(inverse(multiply(Y4,inverse(X1))),multiply(Y4,X2))),
inference(step,[status(thm)],[t90659,t88542]) ).
cnf(t88601,plain,
multiply(multiply(inverse(inverse(X1)),X2),multiply(inverse(c3),c3)) = multiply(multiply(inverse(c3),c3),multiply(inverse(multiply(Y4,inverse(X1))),multiply(Y4,X2))),
inference(rw,[status(thm)],[t90660]) ).
cnf(t89027,plain,
multiply(multiply(inverse(c3),c3),multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X3))) = multiply(multiply(inverse(inverse(X2)),X3),multiply(inverse(c3),c3)),
inference(orient,[status(thm)],[t88601]) ).
cnf(t89028,plain,
multiply(multiply(inverse(inverse(X1)),X2),multiply(inverse(c3),c3)) = multiply(multiply(inverse(X3),X3),multiply(inverse(multiply(Y3,inverse(X1))),multiply(Y3,X2))),
inference(cp,[status(thm)],[t89027,t3991]) ).
cnf(t89264,plain,
multiply(multiply(inverse(X1),X1),multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,Y3))) = multiply(multiply(inverse(inverse(X3)),Y3),multiply(inverse(c3),c3)),
inference(orient,[status(thm)],[t89028]) ).
cnf(t4854,plain,
X1 = multiply(inverse(multiply(X2,inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(c3),c3)))))),multiply(X2,multiply(inverse(X3),X3))),
inference(cp,[status(thm)],[t4548,t4847]) ).
cnf(t6104,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X2)),inverse(multiply(inverse(c3),c3)))))),multiply(X1,multiply(inverse(X3),X3))) = X2,
inference(orient,[status(thm)],[t4854]) ).
cnf(t6118,plain,
X1 = multiply(inverse(multiply(X2,inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X3),X3)))))),multiply(X2,multiply(inverse(Y3),Y3))),
inference(cp,[status(thm)],[t6104,t3991]) ).
cnf(t6177,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X2)),inverse(multiply(inverse(X3),X3)))))),multiply(X1,multiply(inverse(Y3),Y3))) = X2,
inference(orient,[status(thm)],[t6118]) ).
cnf(t90813,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X2)),multiply(inverse(c3),c3))))),multiply(X1,multiply(inverse(Y3),Y3))) = X2,
inference(step,[status(thm)],[t6177,t88542]) ).
cnf(t88673,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X2)),multiply(inverse(c3),c3))))),multiply(X1,multiply(inverse(Y3),Y3))) = X2,
inference(rw,[status(thm)],[t90813]) ).
cnf(t89567,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X2)),multiply(inverse(c3),c3))))),multiply(X1,multiply(inverse(X3),X3))) = X2,
inference(orient,[status(thm)],[t88673]) ).
cnf(t89588,plain,
multiply(multiply(inverse(inverse(multiply(inverse(inverse(X1)),multiply(inverse(c3),c3)))),multiply(inverse(X2),X2)),multiply(inverse(c3),c3)) = multiply(multiply(inverse(X3),X3),X1),
inference(cp,[status(thm)],[t89264,t89567]) ).
cnf(t90701,plain,
multiply(X1,multiply(inverse(c3),c3)) = multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),X3)))),multiply(X2,X1)),
inference(step,[status(thm)],[t4055,t88542]) ).
cnf(t90702,plain,
multiply(X1,multiply(inverse(c3),c3)) = multiply(inverse(multiply(X2,multiply(inverse(c3),c3))),multiply(X2,X1)),
inference(step,[status(thm)],[t90701,t88542]) ).
cnf(t88618,plain,
multiply(X1,multiply(inverse(c3),c3)) = multiply(inverse(multiply(X2,multiply(inverse(c3),c3))),multiply(X2,X1)),
inference(rw,[status(thm)],[t90702]) ).
cnf(t88796,plain,
multiply(inverse(multiply(X1,multiply(inverse(c3),c3))),multiply(X1,X2)) = multiply(X2,multiply(inverse(c3),c3)),
inference(orient,[status(thm)],[t88618]) ).
cnf(t88802,plain,
multiply(X1,multiply(inverse(c3),c3)) = multiply(inverse(multiply(X2,multiply(inverse(X3),X3))),multiply(X2,X1)),
inference(cp,[status(thm)],[t88796,t3991]) ).
cnf(t88840,plain,
multiply(inverse(multiply(X1,multiply(inverse(X2),X2))),multiply(X1,X3)) = multiply(X3,multiply(inverse(c3),c3)),
inference(orient,[status(thm)],[t88802]) ).
cnf(t88854,plain,
multiply(X1,multiply(inverse(c3),c3)) = multiply(inverse(multiply(inverse(X1),multiply(inverse(X2),X2))),multiply(inverse(X3),X3)),
inference(cp,[status(thm)],[t88840,t3991]) ).
cnf(t88933,plain,
multiply(inverse(multiply(inverse(X1),multiply(inverse(X2),X2))),multiply(inverse(X3),X3)) = multiply(X1,multiply(inverse(c3),c3)),
inference(orient,[status(thm)],[t88854]) ).
cnf(t88937,plain,
multiply(multiply(inverse(X1),inverse(X2)),multiply(inverse(c3),c3)) = multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,X1))),multiply(inverse(Y3),Y3)),
inference(cp,[status(thm)],[t88933,t4289]) ).
cnf(t89381,plain,
multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X3))),multiply(inverse(Y3),Y3)) = multiply(multiply(inverse(X3),inverse(X2)),multiply(inverse(c3),c3)),
inference(orient,[status(thm)],[t88937]) ).
cnf(t89387,plain,
multiply(multiply(inverse(X1),inverse(multiply(inverse(X2),X2))),multiply(inverse(c3),c3)) = multiply(inverse(multiply(inverse(multiply(X3,multiply(inverse(c3),c3))),multiply(X3,X1))),multiply(inverse(Y3),Y3)),
inference(cp,[status(thm)],[t89381,t88542]) ).
cnf(t91051,plain,
multiply(multiply(inverse(X1),multiply(inverse(c3),c3)),multiply(inverse(c3),c3)) = multiply(inverse(multiply(inverse(multiply(X3,multiply(inverse(c3),c3))),multiply(X3,X1))),multiply(inverse(Y3),Y3)),
inference(step,[status(thm)],[t89387,t88542]) ).
cnf(t91052,plain,
multiply(multiply(inverse(X1),multiply(inverse(c3),c3)),multiply(inverse(c3),c3)) = multiply(inverse(multiply(X1,multiply(inverse(c3),c3))),multiply(inverse(Y3),Y3)),
inference(step,[status(thm)],[t91051,t88796]) ).
cnf(t89432,plain,
multiply(inverse(multiply(X1,multiply(inverse(c3),c3))),multiply(inverse(X2),X2)) = multiply(multiply(inverse(X1),multiply(inverse(c3),c3)),multiply(inverse(c3),c3)),
inference(orient,[status(thm)],[t91052]) ).
cnf(t89433,plain,
multiply(multiply(inverse(inverse(X1)),multiply(inverse(c3),c3)),multiply(inverse(c3),c3)) = multiply(X1,multiply(inverse(c3),c3)),
inference(cp,[status(thm)],[t89432,t88840]) ).
cnf(t89471,plain,
multiply(multiply(inverse(inverse(X1)),multiply(inverse(c3),c3)),multiply(inverse(c3),c3)) = multiply(X1,multiply(inverse(c3),c3)),
inference(orient,[status(thm)],[t89433]) ).
cnf(t89472,plain,
multiply(X1,multiply(inverse(c3),c3)) = multiply(multiply(inverse(inverse(X1)),multiply(inverse(X2),X2)),multiply(inverse(c3),c3)),
inference(cp,[status(thm)],[t89471,t3991]) ).
cnf(t89492,plain,
multiply(multiply(inverse(inverse(X1)),multiply(inverse(X2),X2)),multiply(inverse(c3),c3)) = multiply(X1,multiply(inverse(c3),c3)),
inference(orient,[status(thm)],[t89472]) ).
cnf(t91053,plain,
multiply(multiply(inverse(inverse(X1)),multiply(inverse(c3),c3)),multiply(inverse(c3),c3)) = multiply(multiply(inverse(X3),X3),X1),
inference(step,[status(thm)],[t89588,t89492]) ).
cnf(t91054,plain,
multiply(X1,multiply(inverse(c3),c3)) = multiply(multiply(inverse(X3),X3),X1),
inference(step,[status(thm)],[t91053,t89471]) ).
cnf(t89620,plain,
multiply(X1,multiply(inverse(c3),c3)) = multiply(multiply(inverse(X2),X2),X1),
inference(orient,[status(thm)],[t91054]) ).
cnf(t91055,plain,
multiply(multiply(inverse(X1),X1),multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,Y3))) = multiply(multiply(inverse(c3),c3),multiply(inverse(inverse(X3)),Y3)),
inference(step,[status(thm)],[t89264,t89620]) ).
cnf(t88578,plain,
multiply(inverse(multiply(inverse(X1),inverse(X2))),multiply(inverse(X3),X3)) = multiply(multiply(inverse(c3),c3),multiply(inverse(inverse(X2)),X1)),
inference(cp,[status(thm)],[t4289,t88542]) ).
cnf(t91047,plain,
multiply(inverse(multiply(c3,inverse(X2))),multiply(c3,X1)) = multiply(multiply(inverse(c3),c3),multiply(inverse(inverse(X2)),X1)),
inference(step,[status(thm)],[t88578,t4289]) ).
cnf(t88877,plain,
multiply(multiply(inverse(c3),c3),multiply(inverse(inverse(X1)),X2)) = multiply(inverse(multiply(c3,inverse(X1))),multiply(c3,X2)),
inference(orient,[status(thm)],[t91047]) ).
cnf(t91056,plain,
multiply(multiply(inverse(X1),X1),multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,Y3))) = multiply(inverse(multiply(c3,inverse(X3))),multiply(c3,Y3)),
inference(step,[status(thm)],[t91055,t88877]) ).
cnf(t89621,plain,
multiply(multiply(inverse(X1),X1),multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,Y3))) = multiply(inverse(multiply(c3,inverse(X3))),multiply(c3,Y3)),
inference(orient,[status(thm)],[t91056]) ).
cnf(t89716,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(inverse(X1)),multiply(inverse(c3),c3))),multiply(inverse(c3),c3))),multiply(multiply(inverse(X2),X2),multiply(inverse(X3),X3))),
inference(cp,[status(thm)],[t89567,t89620]) ).
cnf(t89722,plain,
multiply(inverse(multiply(c3,inverse(X1))),multiply(c3,multiply(inverse(c3),c3))) = X1,
inference(orient,[status(thm)],[t89716]) ).
cnf(t89728,plain,
multiply(inverse(multiply(c3,inverse(X1))),multiply(c3,multiply(inverse(c3),c3))) = multiply(multiply(inverse(X2),X2),X1),
inference(cp,[status(thm)],[t89621,t89722]) ).
cnf(t91063,plain,
X1 = multiply(multiply(inverse(X2),X2),X1),
inference(step,[status(thm)],[t89728,t89722]) ).
cnf(t91064,plain,
X1 = multiply(X1,multiply(inverse(c3),c3)),
inference(step,[status(thm)],[t91063,t89620]) ).
cnf(t89747,plain,
multiply(X1,multiply(inverse(c3),c3)) = X1,
inference(orient,[status(thm)],[t91064]) ).
cnf(t91077,plain,
X1 = multiply(multiply(inverse(X2),X2),X1),
inference(step,[status(thm)],[t89620,t89747]) ).
cnf(t89803,plain,
X1 = multiply(multiply(inverse(X2),X2),X1),
inference(rw,[status(thm)],[t91077]) ).
cnf(t89862,plain,
multiply(multiply(inverse(X1),X1),X2) = X2,
inference(orient,[status(thm)],[t89803]) ).
cnf(t89493,plain,
multiply(X1,multiply(inverse(c3),c3)) = multiply(multiply(inverse(inverse(X1)),multiply(inverse(X2),X2)),multiply(inverse(X3),X3)),
inference(cp,[status(thm)],[t89492,t3991]) ).
cnf(t89512,plain,
multiply(multiply(inverse(inverse(X1)),multiply(inverse(X2),X2)),multiply(inverse(X3),X3)) = multiply(X1,multiply(inverse(c3),c3)),
inference(orient,[status(thm)],[t89493]) ).
cnf(t91069,plain,
multiply(multiply(inverse(inverse(X1)),multiply(inverse(X2),X2)),multiply(inverse(X3),X3)) = X1,
inference(step,[status(thm)],[t89512,t89747]) ).
cnf(t89752,plain,
multiply(multiply(inverse(inverse(X1)),multiply(inverse(X2),X2)),multiply(inverse(X3),X3)) = X1,
inference(orient,[status(thm)],[t91069]) ).
cnf(t89766,plain,
X1 = multiply(X1,multiply(inverse(X2),X2)),
inference(cp,[status(thm)],[t89747,t3991]) ).
cnf(t89806,plain,
multiply(X1,multiply(inverse(X2),X2)) = X1,
inference(orient,[status(thm)],[t89766]) ).
cnf(t91084,plain,
multiply(inverse(inverse(X1)),multiply(inverse(X2),X2)) = X1,
inference(step,[status(thm)],[t89752,t89806]) ).
cnf(t91085,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t91084,t89806]) ).
cnf(t89837,plain,
inverse(inverse(X1)) = X1,
inference(rw,[status(thm)],[t91085]) ).
cnf(t89843,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t89837]) ).
cnf(t89864,plain,
X1 = multiply(multiply(X2,inverse(X2)),X1),
inference(cp,[status(thm)],[t89862,t89843]) ).
cnf(t89925,plain,
multiply(multiply(X1,inverse(X1)),X2) = X2,
inference(orient,[status(thm)],[t89864]) ).
cnf(t89931,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X3)) = multiply(inverse(inverse(X2)),multiply(multiply(Y3,inverse(Y3)),X3)),
inference(cp,[status(thm)],[t1958,t89925]) ).
cnf(t91103,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X3)) = multiply(X2,multiply(multiply(Y3,inverse(Y3)),X3)),
inference(step,[status(thm)],[t89931,t89843]) ).
cnf(t91104,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X3)) = multiply(X2,X3),
inference(step,[status(thm)],[t91103,t89925]) ).
cnf(t90305,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X3)) = multiply(X2,X3),
inference(orient,[status(thm)],[t91104]) ).
cnf(t89846,plain,
X1 = multiply(X1,multiply(X2,inverse(X2))),
inference(cp,[status(thm)],[t89806,t89843]) ).
cnf(t89906,plain,
multiply(X1,multiply(X2,inverse(X2))) = X1,
inference(orient,[status(thm)],[t89846]) ).
cnf(t90307,plain,
multiply(X1,inverse(X2)) = inverse(multiply(X2,inverse(X1))),
inference(cp,[status(thm)],[t90305,t89906]) ).
cnf(t90332,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t90307]) ).
cnf(t91108,plain,
multiply(multiply(X2,inverse(X1)),multiply(X1,X3)) = multiply(X2,X3),
inference(step,[status(thm)],[t90305,t90332]) ).
cnf(t90356,plain,
multiply(multiply(X2,inverse(X1)),multiply(X1,X3)) = multiply(X2,X3),
inference(rw,[status(thm)],[t91108]) ).
cnf(t90434,plain,
multiply(multiply(X1,inverse(X2)),multiply(X2,X3)) = multiply(X1,X3),
inference(orient,[status(thm)],[t90356]) ).
cnf(t91065,plain,
multiply(inverse(multiply(X1,multiply(inverse(X2),X2))),multiply(X1,X3)) = X3,
inference(step,[status(thm)],[t88840,t89747]) ).
cnf(t89748,plain,
multiply(inverse(multiply(X1,multiply(inverse(X2),X2))),multiply(X1,X3)) = X3,
inference(orient,[status(thm)],[t91065]) ).
cnf(t91086,plain,
multiply(inverse(X1),multiply(X1,X3)) = X3,
inference(step,[status(thm)],[t89748,t89806]) ).
cnf(t89838,plain,
multiply(inverse(X1),multiply(X1,X3)) = X3,
inference(rw,[status(thm)],[t91086]) ).
cnf(t89886,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(orient,[status(thm)],[t89838]) ).
cnf(t90341,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(cp,[status(thm)],[t90332,t89843]) ).
cnf(t90363,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t90341]) ).
cnf(t90377,plain,
inverse(X1) = multiply(inverse(inverse(X2)),inverse(multiply(X1,X2))),
inference(cp,[status(thm)],[t89886,t90363]) ).
cnf(t91111,plain,
inverse(X1) = inverse(multiply(multiply(X1,X2),inverse(X2))),
inference(step,[status(thm)],[t90377,t90363]) ).
cnf(t91112,plain,
inverse(X1) = multiply(X2,inverse(multiply(X1,X2))),
inference(step,[status(thm)],[t91111,t90332]) ).
cnf(t90406,plain,
multiply(X1,inverse(multiply(X2,X1))) = inverse(X2),
inference(orient,[status(thm)],[t91112]) ).
cnf(t90409,plain,
inverse(inverse(X1)) = multiply(multiply(X1,X2),inverse(X2)),
inference(cp,[status(thm)],[t90406,t89886]) ).
cnf(t91113,plain,
X1 = multiply(multiply(X1,X2),inverse(X2)),
inference(step,[status(thm)],[t90409,t89843]) ).
cnf(t90414,plain,
multiply(multiply(X1,X2),inverse(X2)) = X1,
inference(orient,[status(thm)],[t91113]) ).
cnf(t90437,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(cp,[status(thm)],[t90434,t90414]) ).
cnf(t90456,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t90437]) ).
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(b3,c3)) != multiply(a3,multiply(b3,c3)),
inference(rw,[status(thm)],[goal_0,t90456]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP420-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n013.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 14:42:05 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 42.49/5.88 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 42.49/5.88 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------