%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP422-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n015.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:48 PM UTC 2026
% Result : Unsatisfiable 42.29s 6.06s
% Output : CNFRefutation 42.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 136
% Number of leaves : 2
% Syntax : Number of clauses : 235 ( 235 unt; 0 nHn; 6 RR)
% Number of literals : 235 ( 234 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 19 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 691 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),multiply(inverse(X3),inverse(multiply(inverse(X3),X3))))))),multiply(X1,X3))) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t1,plain,
inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),multiply(inverse(X3),inverse(multiply(inverse(X3),X3))))))),multiply(X1,X3))) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t3,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),multiply(inverse(X3),inverse(multiply(inverse(X3),X3))))))),multiply(X1,X3)) = inverse(multiply(inverse(multiply(Y3,inverse(multiply(X2,multiply(inverse(Y4),inverse(multiply(inverse(Y4),Y4))))))),multiply(Y3,Y4))),
inference(cp,[status(thm)],[t1,t1]) ).
cnf(t153,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),multiply(inverse(X3),inverse(multiply(inverse(X3),X3))))))),multiply(X1,X3)) = inverse(multiply(inverse(multiply(Y3,inverse(multiply(X2,multiply(inverse(Y4),inverse(multiply(inverse(Y4),Y4))))))),multiply(Y3,Y4))),
inference(orient,[status(thm)],[t3]) ).
cnf(t9486,plain,
multiply(inverse(multiply(f1,inverse(multiply(inverse(inverse(X2)),multiply(inverse(f1),inverse(multiply(inverse(f1),f1))))))),multiply(f1,f1)) = X2,
inference(step,[status(thm)],[t1,t153]) ).
cnf(t154,plain,
multiply(inverse(multiply(f1,inverse(multiply(inverse(inverse(X1)),multiply(inverse(f1),inverse(multiply(inverse(f1),f1))))))),multiply(f1,f1)) = X1,
inference(rw,[status(thm)],[t9486]) ).
cnf(t204,plain,
multiply(inverse(multiply(f1,inverse(multiply(inverse(inverse(X1)),multiply(inverse(f1),inverse(multiply(inverse(f1),f1))))))),multiply(f1,f1)) = X1,
inference(orient,[status(thm)],[t154]) ).
cnf(t2,plain,
multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))))))) = inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,X1))),
inference(cp,[status(thm)],[t1,t1]) ).
cnf(t5,plain,
multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))))))) = inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,X1))),
inference(orient,[status(thm)],[t2]) ).
cnf(t9,plain,
X1 = inverse(multiply(inverse(inverse(multiply(inverse(multiply(X2,X1)),multiply(X2,X3)))),multiply(inverse(X3),inverse(multiply(inverse(X3),X3))))),
inference(cp,[status(thm)],[t1,t5]) ).
cnf(t11,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X3)))),multiply(inverse(X3),inverse(multiply(inverse(X3),X3))))) = X2,
inference(orient,[status(thm)],[t9]) ).
cnf(t18,plain,
inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X3))) = inverse(multiply(inverse(multiply(Y3,X2)),multiply(Y3,X3))),
inference(cp,[status(thm)],[t1,t11]) ).
cnf(t24,plain,
inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X3))) = inverse(multiply(inverse(multiply(Y3,X2)),multiply(Y3,X3))),
inference(orient,[status(thm)],[t18]) ).
cnf(t30,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = inverse(multiply(inverse(multiply(Y3,inverse(multiply(inverse(multiply(inverse(multiply(Y4,X2)),multiply(Y4,X3))),multiply(inverse(Y5),inverse(multiply(inverse(Y5),Y5))))))),multiply(Y3,Y5))),
inference(cp,[status(thm)],[t1,t24]) ).
cnf(t9484,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(multiply(Y4,X2)),multiply(Y4,X3)),
inference(step,[status(thm)],[t30,t1]) ).
cnf(t47,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(multiply(Y3,X2)),multiply(Y3,X3)),
inference(orient,[status(thm)],[t9484]) ).
cnf(t208,plain,
X1 = multiply(inverse(multiply(X2,inverse(multiply(inverse(inverse(X1)),multiply(inverse(f1),inverse(multiply(inverse(f1),f1))))))),multiply(X2,f1)),
inference(cp,[status(thm)],[t204,t47]) ).
cnf(t298,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X2)),multiply(inverse(f1),inverse(multiply(inverse(f1),f1))))))),multiply(X1,f1)) = X2,
inference(orient,[status(thm)],[t208]) ).
cnf(t45,plain,
X1 = inverse(multiply(inverse(inverse(multiply(inverse(multiply(X2,X1)),multiply(X2,multiply(X3,Y3))))),multiply(inverse(multiply(X3,Y3)),inverse(multiply(inverse(multiply(Y4,Y3)),multiply(Y4,Y3)))))),
inference(cp,[status(thm)],[t11,t24]) ).
cnf(t1762,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,multiply(X3,Y3))))),multiply(inverse(multiply(X3,Y3)),inverse(multiply(inverse(multiply(Y4,Y3)),multiply(Y4,Y3)))))) = X2,
inference(orient,[status(thm)],[t45]) ).
cnf(t22,plain,
inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(inverse(Y3),Y3))))))),multiply(X1,Y3))) = multiply(inverse(Y3),X3),
inference(cp,[status(thm)],[t5,t11]) ).
cnf(t58,plain,
inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(inverse(Y3),Y3))))))),multiply(X1,Y3))) = multiply(inverse(Y3),X3),
inference(orient,[status(thm)],[t22]) ).
cnf(t68,plain,
multiply(inverse(multiply(X1,X2)),X3) = inverse(multiply(inverse(multiply(Y3,inverse(multiply(inverse(multiply(Y4,X3)),multiply(Y4,inverse(multiply(inverse(multiply(Y5,X2)),multiply(Y5,X2)))))))),multiply(Y3,multiply(X1,X2)))),
inference(cp,[status(thm)],[t58,t24]) ).
cnf(t1029,plain,
inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(inverse(multiply(Y3,Y4)),multiply(Y3,Y4)))))))),multiply(X1,multiply(Y5,Y4)))) = multiply(inverse(multiply(Y5,Y4)),X3),
inference(orient,[status(thm)],[t68]) ).
cnf(t1063,plain,
multiply(inverse(multiply(X1,multiply(X2,f1))),X3) = inverse(multiply(inverse(multiply(Y3,inverse(multiply(inverse(multiply(Y4,X3)),multiply(Y4,inverse(multiply(inverse(Y5),multiply(inverse(multiply(X2,inverse(multiply(inverse(inverse(Y5)),multiply(inverse(f1),inverse(multiply(inverse(f1),f1))))))),multiply(X2,f1))))))))),multiply(Y3,multiply(X1,multiply(X2,f1))))),
inference(cp,[status(thm)],[t1029,t298]) ).
cnf(t9501,plain,
multiply(inverse(multiply(X1,multiply(X2,f1))),X3) = inverse(multiply(inverse(multiply(Y3,inverse(multiply(inverse(multiply(Y4,X3)),multiply(Y4,inverse(multiply(inverse(Y5),Y5))))))),multiply(Y3,multiply(X1,multiply(X2,f1))))),
inference(step,[status(thm)],[t1063,t298]) ).
cnf(t1116,plain,
inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(inverse(Y3),Y3))))))),multiply(X1,multiply(Y4,multiply(Y5,f1))))) = multiply(inverse(multiply(Y4,multiply(Y5,f1))),X3),
inference(orient,[status(thm)],[t9501]) ).
cnf(t1144,plain,
multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X2)),multiply(inverse(f1),inverse(multiply(inverse(f1),f1))))))),multiply(X1,f1))),X3) = inverse(multiply(inverse(multiply(Y3,inverse(multiply(inverse(multiply(Y4,X3)),multiply(Y4,inverse(multiply(inverse(Y5),Y5))))))),multiply(Y3,X2))),
inference(cp,[status(thm)],[t1116,t298]) ).
cnf(t9502,plain,
multiply(multiply(inverse(multiply(f1,inverse(multiply(inverse(inverse(inverse(X2))),multiply(inverse(f1),inverse(multiply(inverse(f1),f1))))))),multiply(f1,f1)),X3) = inverse(multiply(inverse(multiply(Y3,inverse(multiply(inverse(multiply(Y4,X3)),multiply(Y4,inverse(multiply(inverse(Y5),Y5))))))),multiply(Y3,X2))),
inference(step,[status(thm)],[t1144,t153]) ).
cnf(t9503,plain,
multiply(inverse(X2),X3) = inverse(multiply(inverse(multiply(Y3,inverse(multiply(inverse(multiply(Y4,X3)),multiply(Y4,inverse(multiply(inverse(Y5),Y5))))))),multiply(Y3,X2))),
inference(step,[status(thm)],[t9502,t298]) ).
cnf(t1351,plain,
inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(inverse(Y3),Y3))))))),multiply(X1,Y4))) = multiply(inverse(Y4),X3),
inference(orient,[status(thm)],[t9503]) ).
cnf(t1355,plain,
multiply(inverse(X1),X2) = inverse(multiply(inverse(inverse(multiply(inverse(multiply(X3,multiply(inverse(inverse(multiply(inverse(Y3),Y3))),X2))),multiply(X3,Y3)))),multiply(inverse(Y3),X1))),
inference(cp,[status(thm)],[t1351,t5]) ).
cnf(t1450,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,multiply(inverse(inverse(multiply(inverse(X2),X2))),X3))),multiply(X1,X2)))),multiply(inverse(X2),Y3))) = multiply(inverse(Y3),X3),
inference(orient,[status(thm)],[t1355]) ).
cnf(t1825,plain,
multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2)))),X3) = multiply(inverse(inverse(multiply(inverse(multiply(Y3,X2)),multiply(Y3,X2)))),X3),
inference(cp,[status(thm)],[t1762,t1450]) ).
cnf(t1868,plain,
multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2)))),X3) = multiply(inverse(inverse(multiply(inverse(multiply(Y3,X2)),multiply(Y3,X2)))),X3),
inference(orient,[status(thm)],[t1825]) ).
cnf(t1925,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X2)) = multiply(inverse(multiply(X3,inverse(multiply(inverse(inverse(multiply(inverse(multiply(Y3,X2)),multiply(Y3,X2)))),multiply(inverse(f1),inverse(multiply(inverse(f1),f1))))))),multiply(X3,f1)),
inference(cp,[status(thm)],[t298,t1868]) ).
cnf(t9507,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X2)) = multiply(inverse(multiply(Y3,X2)),multiply(Y3,X2)),
inference(step,[status(thm)],[t1925,t298]) ).
cnf(t1977,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X2)) = multiply(inverse(multiply(X3,X2)),multiply(X3,X2)),
inference(orient,[status(thm)],[t9507]) ).
cnf(t1981,plain,
multiply(inverse(multiply(X1,multiply(X2,f1))),multiply(X1,multiply(X2,f1))) = multiply(inverse(X3),multiply(inverse(multiply(X2,inverse(multiply(inverse(inverse(X3)),multiply(inverse(f1),inverse(multiply(inverse(f1),f1))))))),multiply(X2,f1))),
inference(cp,[status(thm)],[t1977,t298]) ).
cnf(t9508,plain,
multiply(inverse(multiply(X1,multiply(X2,f1))),multiply(X1,multiply(X2,f1))) = multiply(inverse(X3),X3),
inference(step,[status(thm)],[t1981,t298]) ).
cnf(t1992,plain,
multiply(inverse(multiply(X1,multiply(X2,f1))),multiply(X1,multiply(X2,f1))) = multiply(inverse(X3),X3),
inference(orient,[status(thm)],[t9508]) ).
cnf(t2005,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),multiply(inverse(multiply(X3,inverse(multiply(inverse(inverse(X2)),multiply(inverse(f1),inverse(multiply(inverse(f1),f1))))))),multiply(X3,f1))),
inference(cp,[status(thm)],[t1992,t298]) ).
cnf(t9521,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),X2),
inference(step,[status(thm)],[t2005,t298]) ).
cnf(t2075,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),X2),
inference(orient,[status(thm)],[t9521]) ).
cnf(t9525,plain,
multiply(inverse(f1),f1) = multiply(inverse(X3),X3),
inference(step,[status(thm)],[t1992,t2075]) ).
cnf(t2079,plain,
multiply(inverse(f1),f1) = multiply(inverse(X1),X1),
inference(rw,[status(thm)],[t9525]) ).
cnf(t2164,plain,
multiply(inverse(f1),f1) = multiply(inverse(X1),X1),
inference(orient,[status(thm)],[t2079]) ).
cnf(t2090,plain,
X1 = inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),multiply(inverse(X1),inverse(multiply(inverse(X1),X1))))),
inference(cp,[status(thm)],[t11,t2075]) ).
cnf(t2536,plain,
inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))) = X2,
inference(orient,[status(thm)],[t2090]) ).
cnf(t2569,plain,
X1 = inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),multiply(inverse(X1),inverse(multiply(inverse(X3),X3))))),
inference(cp,[status(thm)],[t2536,t2075]) ).
cnf(t2615,plain,
inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),multiply(inverse(X2),inverse(multiply(inverse(X3),X3))))) = X2,
inference(orient,[status(thm)],[t2569]) ).
cnf(t52,plain,
multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,Y3)) = multiply(inverse(multiply(inverse(multiply(Y4,Y5)),multiply(Y4,X3))),multiply(inverse(multiply(X2,Y5)),Y3)),
inference(cp,[status(thm)],[t47,t24]) ).
cnf(t83,plain,
multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,Y3)) = multiply(inverse(multiply(inverse(multiply(Y4,Y5)),multiply(Y4,X3))),multiply(inverse(multiply(X2,Y5)),Y3)),
inference(orient,[status(thm)],[t52]) ).
cnf(t94,plain,
multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,multiply(X3,Y3)))),multiply(inverse(multiply(inverse(multiply(X3,multiply(Y4,Y5))),X2)),Y6)) = multiply(inverse(multiply(Y7,multiply(inverse(multiply(inverse(multiply(Y8,Y9)),multiply(Y8,Y5))),multiply(inverse(multiply(Y4,Y9)),Y3)))),multiply(Y7,Y6)),
inference(cp,[status(thm)],[t83,t83]) ).
cnf(t9593,plain,
multiply(inverse(multiply(f1,multiply(inverse(multiply(X3,multiply(Y4,Y5))),multiply(X3,Y3)))),multiply(f1,Y6)) = multiply(inverse(multiply(Y7,multiply(inverse(multiply(inverse(multiply(Y8,Y9)),multiply(Y8,Y5))),multiply(inverse(multiply(Y4,Y9)),Y3)))),multiply(Y7,Y6)),
inference(step,[status(thm)],[t94,t83]) ).
cnf(t9594,plain,
multiply(inverse(multiply(f1,multiply(inverse(multiply(X3,multiply(Y4,Y5))),multiply(X3,Y3)))),multiply(f1,Y6)) = multiply(inverse(multiply(Y7,multiply(inverse(multiply(f1,multiply(Y4,Y5))),multiply(f1,Y3)))),multiply(Y7,Y6)),
inference(step,[status(thm)],[t9593,t83]) ).
cnf(t6230,plain,
multiply(inverse(multiply(f1,multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,Y3)))),multiply(f1,Y4)) = multiply(inverse(multiply(Y5,multiply(inverse(multiply(f1,multiply(X2,X3))),multiply(f1,Y3)))),multiply(Y5,Y4)),
inference(orient,[status(thm)],[t9594]) ).
cnf(t6246,plain,
inverse(multiply(inverse(multiply(X1,multiply(inverse(multiply(X2,multiply(X3,Y3))),multiply(X2,Y4)))),multiply(X1,Y5))) = inverse(multiply(inverse(multiply(Y6,multiply(inverse(multiply(f1,multiply(X3,Y3))),multiply(f1,Y4)))),multiply(Y6,Y5))),
inference(cp,[status(thm)],[t24,t6230]) ).
cnf(t23,plain,
inverse(multiply(inverse(multiply(X1,multiply(inverse(inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,Y3)))),multiply(inverse(Y3),inverse(multiply(inverse(Y3),Y3)))))),multiply(X1,Y4))) = multiply(inverse(Y4),inverse(multiply(X3,multiply(inverse(inverse(multiply(inverse(Y4),Y4))),inverse(multiply(inverse(inverse(multiply(inverse(Y4),Y4))),inverse(multiply(inverse(Y4),Y4)))))))),
inference(cp,[status(thm)],[t5,t11]) ).
cnf(t768,plain,
inverse(multiply(inverse(multiply(X1,multiply(inverse(inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,Y3)))),multiply(inverse(Y3),inverse(multiply(inverse(Y3),Y3)))))),multiply(X1,Y4))) = multiply(inverse(Y4),inverse(multiply(X3,multiply(inverse(inverse(multiply(inverse(Y4),Y4))),inverse(multiply(inverse(inverse(multiply(inverse(Y4),Y4))),inverse(multiply(inverse(Y4),Y4)))))))),
inference(orient,[status(thm)],[t23]) ).
cnf(t2151,plain,
multiply(inverse(X1),inverse(multiply(inverse(X2),X2))) = inverse(multiply(inverse(inverse(multiply(inverse(multiply(X3,multiply(inverse(Y3),Y3))),multiply(X3,X2)))),multiply(inverse(X2),X1))),
inference(cp,[status(thm)],[t1450,t2075]) ).
cnf(t3136,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,multiply(inverse(X2),X2))),multiply(X1,X3)))),multiply(inverse(X3),Y3))) = multiply(inverse(Y3),inverse(multiply(inverse(X3),X3))),
inference(orient,[status(thm)],[t2151]) ).
cnf(t3194,plain,
multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))) = multiply(inverse(X2),X2),
inference(cp,[status(thm)],[t3136,t2615]) ).
cnf(t9534,plain,
multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(multiply(f1,X2)),multiply(f1,X2)))) = multiply(inverse(X2),X2),
inference(step,[status(thm)],[t3194,t24]) ).
cnf(t2094,plain,
inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2))) = inverse(multiply(inverse(X3),X3)),
inference(cp,[status(thm)],[t24,t2075]) ).
cnf(t9529,plain,
inverse(multiply(inverse(f1),f1)) = inverse(multiply(inverse(X3),X3)),
inference(step,[status(thm)],[t2094,t2075]) ).
cnf(t2275,plain,
inverse(multiply(inverse(f1),f1)) = inverse(multiply(inverse(X1),X1)),
inference(orient,[status(thm)],[t9529]) ).
cnf(t9535,plain,
multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(f1),f1))) = multiply(inverse(X2),X2),
inference(step,[status(thm)],[t9534,t2275]) ).
cnf(t3257,plain,
multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(f1),f1))) = multiply(inverse(X2),X2),
inference(orient,[status(thm)],[t9535]) ).
cnf(t3272,plain,
multiply(inverse(X1),X1) = multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X3),X3))),
inference(cp,[status(thm)],[t3257,t2075]) ).
cnf(t3337,plain,
multiply(inverse(X1),X1) = multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X3),X3))),
inference(orient,[status(thm)],[t3272]) ).
cnf(t9536,plain,
inverse(multiply(inverse(multiply(X1,multiply(inverse(inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,Y3)))),multiply(inverse(Y3),inverse(multiply(inverse(Y3),Y3)))))),multiply(X1,Y4))) = multiply(inverse(Y4),inverse(multiply(X3,multiply(inverse(f1),f1)))),
inference(step,[status(thm)],[t768,t3337]) ).
cnf(t3338,plain,
inverse(multiply(inverse(multiply(X1,multiply(inverse(inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,Y3)))),multiply(inverse(Y3),inverse(multiply(inverse(Y3),Y3)))))),multiply(X1,Y4))) = multiply(inverse(Y4),inverse(multiply(X3,multiply(inverse(f1),f1)))),
inference(orient,[status(thm)],[t9536]) ).
cnf(t3406,plain,
multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(f1),f1)))) = inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(Y3),Y3)))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(Y4,X2)),multiply(Y4,Y5)))),multiply(inverse(Y5),inverse(multiply(inverse(Y5),Y5))))),X1))),
inference(cp,[status(thm)],[t3338,t3337]) ).
cnf(t9541,plain,
multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(f1),f1)))) = inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(Y3),Y3)))),multiply(X2,X1))),
inference(step,[status(thm)],[t3406,t11]) ).
cnf(t9542,plain,
multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(f1),f1)))) = inverse(multiply(inverse(multiply(inverse(f1),f1)),multiply(X2,X1))),
inference(step,[status(thm)],[t9541,t3337]) ).
cnf(t3522,plain,
inverse(multiply(inverse(multiply(inverse(f1),f1)),multiply(X1,X2))) = multiply(inverse(X2),inverse(multiply(X1,multiply(inverse(f1),f1)))),
inference(orient,[status(thm)],[t9542]) ).
cnf(t3533,plain,
multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(f1),f1)))) = inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(X2,X1))),
inference(cp,[status(thm)],[t3522,t2075]) ).
cnf(t3619,plain,
inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(X2,X3))) = multiply(inverse(X3),inverse(multiply(X2,multiply(inverse(f1),f1)))),
inference(orient,[status(thm)],[t3533]) ).
cnf(t3638,plain,
multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(f1),f1)))) = inverse(multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(X3,Y3)),multiply(X3,Y4)))),multiply(inverse(Y4),inverse(multiply(inverse(Y4),Y4))))),inverse(multiply(Y3,multiply(inverse(f1),f1)))),multiply(X2,X1))),
inference(cp,[status(thm)],[t3619,t3338]) ).
cnf(t9546,plain,
multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(f1),f1)))) = inverse(multiply(multiply(Y3,inverse(multiply(Y3,multiply(inverse(f1),f1)))),multiply(X2,X1))),
inference(step,[status(thm)],[t3638,t11]) ).
cnf(t3990,plain,
inverse(multiply(multiply(X1,inverse(multiply(X1,multiply(inverse(f1),f1)))),multiply(X2,X3))) = multiply(inverse(X3),inverse(multiply(X2,multiply(inverse(f1),f1)))),
inference(orient,[status(thm)],[t9546]) ).
cnf(t4007,plain,
multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(f1),f1)))) = inverse(multiply(multiply(X3,inverse(multiply(X3,multiply(inverse(Y3),Y3)))),multiply(X2,X1))),
inference(cp,[status(thm)],[t3990,t2075]) ).
cnf(t4078,plain,
inverse(multiply(multiply(X1,inverse(multiply(X1,multiply(inverse(X2),X2)))),multiply(X3,Y3))) = multiply(inverse(Y3),inverse(multiply(X3,multiply(inverse(f1),f1)))),
inference(orient,[status(thm)],[t4007]) ).
cnf(t4113,plain,
multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(f1),f1)))) = inverse(multiply(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(Y3),Y3))),multiply(X2,X1))),
inference(cp,[status(thm)],[t4078,t2615]) ).
cnf(t9548,plain,
multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(f1),f1)))) = inverse(multiply(multiply(inverse(f1),f1),multiply(X2,X1))),
inference(step,[status(thm)],[t4113,t3337]) ).
cnf(t4281,plain,
multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(f1),f1)))) = inverse(multiply(multiply(inverse(f1),f1),multiply(X2,X1))),
inference(orient,[status(thm)],[t9548]) ).
cnf(t4309,plain,
inverse(multiply(multiply(inverse(f1),f1),multiply(X1,X2))) = multiply(inverse(X2),inverse(multiply(X1,multiply(inverse(X3),X3)))),
inference(cp,[status(thm)],[t4281,t2075]) ).
cnf(t4419,plain,
multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(X3),X3)))) = inverse(multiply(multiply(inverse(f1),f1),multiply(X2,X1))),
inference(orient,[status(thm)],[t4309]) ).
cnf(t2097,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(multiply(inverse(Y3),Y3)),multiply(inverse(X2),X3)),
inference(cp,[status(thm)],[t47,t2075]) ).
cnf(t2961,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(multiply(inverse(Y3),Y3)),multiply(inverse(X2),X3)),
inference(orient,[status(thm)],[t2097]) ).
cnf(t4469,plain,
inverse(multiply(multiply(inverse(f1),f1),multiply(inverse(multiply(inverse(X1),X2)),X3))) = multiply(inverse(X3),inverse(multiply(inverse(multiply(inverse(Y3),Y3)),multiply(inverse(X2),X1)))),
inference(cp,[status(thm)],[t4419,t2961]) ).
cnf(t2098,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(multiply(inverse(X3),X2)),multiply(inverse(Y3),Y3)),
inference(cp,[status(thm)],[t47,t2075]) ).
cnf(t3047,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(multiply(inverse(X3),X2)),multiply(inverse(Y3),Y3)),
inference(orient,[status(thm)],[t2098]) ).
cnf(t3658,plain,
multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(f1),f1)))) = inverse(multiply(inverse(multiply(inverse(X1),X2)),multiply(inverse(X3),X3))),
inference(cp,[status(thm)],[t3619,t3047]) ).
cnf(t9544,plain,
multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(f1),f1)))) = inverse(multiply(inverse(multiply(f1,X2)),multiply(f1,X1))),
inference(step,[status(thm)],[t3658,t3047]) ).
cnf(t3735,plain,
multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(f1),f1)))) = inverse(multiply(inverse(multiply(f1,X2)),multiply(f1,X1))),
inference(orient,[status(thm)],[t9544]) ).
cnf(t3761,plain,
inverse(multiply(inverse(multiply(f1,X1)),multiply(f1,X2))) = multiply(inverse(X2),inverse(multiply(inverse(X1),multiply(inverse(X3),X3)))),
inference(cp,[status(thm)],[t3735,t2075]) ).
cnf(t3855,plain,
multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(X3),X3)))) = inverse(multiply(inverse(multiply(f1,X2)),multiply(f1,X1))),
inference(orient,[status(thm)],[t3761]) ).
cnf(t9557,plain,
inverse(multiply(multiply(inverse(f1),f1),multiply(inverse(X2),X1))) = inverse(multiply(inverse(multiply(f1,X2)),multiply(f1,X1))),
inference(step,[status(thm)],[t3855,t4419]) ).
cnf(t4420,plain,
inverse(multiply(multiply(inverse(f1),f1),multiply(inverse(X1),X2))) = inverse(multiply(inverse(multiply(f1,X1)),multiply(f1,X2))),
inference(rw,[status(thm)],[t9557]) ).
cnf(t4567,plain,
inverse(multiply(multiply(inverse(f1),f1),multiply(inverse(X1),X2))) = inverse(multiply(inverse(multiply(f1,X1)),multiply(f1,X2))),
inference(orient,[status(thm)],[t4420]) ).
cnf(t4600,plain,
multiply(multiply(inverse(f1),f1),multiply(inverse(X1),X2)) = multiply(inverse(multiply(X3,inverse(multiply(inverse(inverse(multiply(inverse(multiply(f1,X1)),multiply(f1,X2)))),multiply(inverse(f1),inverse(multiply(inverse(f1),f1))))))),multiply(X3,f1)),
inference(cp,[status(thm)],[t298,t4567]) ).
cnf(t9559,plain,
multiply(multiply(inverse(f1),f1),multiply(inverse(X1),X2)) = multiply(inverse(multiply(f1,X1)),multiply(f1,X2)),
inference(step,[status(thm)],[t4600,t298]) ).
cnf(t4646,plain,
multiply(multiply(inverse(f1),f1),multiply(inverse(X1),X2)) = multiply(inverse(multiply(f1,X1)),multiply(f1,X2)),
inference(orient,[status(thm)],[t9559]) ).
cnf(t4661,plain,
multiply(inverse(multiply(f1,X1)),multiply(f1,X2)) = multiply(multiply(inverse(X3),X3),multiply(inverse(X1),X2)),
inference(cp,[status(thm)],[t4646,t2075]) ).
cnf(t4729,plain,
multiply(multiply(inverse(X1),X1),multiply(inverse(X2),X3)) = multiply(inverse(multiply(f1,X2)),multiply(f1,X3)),
inference(orient,[status(thm)],[t4661]) ).
cnf(t9563,plain,
inverse(multiply(inverse(multiply(f1,multiply(inverse(X1),X2))),multiply(f1,X3))) = multiply(inverse(X3),inverse(multiply(inverse(multiply(inverse(Y3),Y3)),multiply(inverse(X2),X1)))),
inference(step,[status(thm)],[t4469,t4729]) ).
cnf(t9551,plain,
inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(X2,X3))) = inverse(multiply(multiply(inverse(f1),f1),multiply(X2,X3))),
inference(step,[status(thm)],[t3619,t4281]) ).
cnf(t4284,plain,
inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(X2,X3))) = inverse(multiply(multiply(inverse(f1),f1),multiply(X2,X3))),
inference(orient,[status(thm)],[t9551]) ).
cnf(t9564,plain,
inverse(multiply(inverse(multiply(f1,multiply(inverse(X1),X2))),multiply(f1,X3))) = multiply(inverse(X3),inverse(multiply(multiply(inverse(f1),f1),multiply(inverse(X2),X1)))),
inference(step,[status(thm)],[t9563,t4284]) ).
cnf(t9565,plain,
inverse(multiply(inverse(multiply(f1,multiply(inverse(X1),X2))),multiply(f1,X3))) = multiply(inverse(X3),inverse(multiply(inverse(multiply(f1,X2)),multiply(f1,X1)))),
inference(step,[status(thm)],[t9564,t4729]) ).
cnf(t4961,plain,
inverse(multiply(inverse(multiply(f1,multiply(inverse(X1),X2))),multiply(f1,X3))) = multiply(inverse(X3),inverse(multiply(inverse(multiply(f1,X2)),multiply(f1,X1)))),
inference(orient,[status(thm)],[t9565]) ).
cnf(t4963,plain,
multiply(inverse(X1),inverse(multiply(inverse(multiply(f1,X2)),multiply(f1,X3)))) = inverse(multiply(inverse(multiply(Y3,multiply(inverse(X3),X2))),multiply(Y3,X1))),
inference(cp,[status(thm)],[t4961,t24]) ).
cnf(t5083,plain,
inverse(multiply(inverse(multiply(X1,multiply(inverse(X2),X3))),multiply(X1,Y3))) = multiply(inverse(Y3),inverse(multiply(inverse(multiply(f1,X3)),multiply(f1,X2)))),
inference(orient,[status(thm)],[t4963]) ).
cnf(t9609,plain,
multiply(inverse(Y5),inverse(multiply(inverse(multiply(f1,multiply(X2,Y4))),multiply(f1,multiply(X2,multiply(X3,Y3)))))) = inverse(multiply(inverse(multiply(Y6,multiply(inverse(multiply(f1,multiply(X3,Y3))),multiply(f1,Y4)))),multiply(Y6,Y5))),
inference(step,[status(thm)],[t6246,t5083]) ).
cnf(t9610,plain,
multiply(inverse(Y5),inverse(multiply(inverse(multiply(f1,multiply(X2,Y4))),multiply(f1,multiply(X2,multiply(X3,Y3)))))) = multiply(inverse(Y5),inverse(multiply(inverse(multiply(f1,multiply(f1,Y4))),multiply(f1,multiply(f1,multiply(X3,Y3)))))),
inference(step,[status(thm)],[t9609,t5083]) ).
cnf(t4478,plain,
inverse(multiply(multiply(inverse(f1),f1),multiply(inverse(multiply(inverse(X1),X1)),X2))) = multiply(inverse(X2),inverse(multiply(multiply(inverse(f1),f1),multiply(inverse(X3),X3)))),
inference(cp,[status(thm)],[t4419,t4284]) ).
cnf(t9570,plain,
inverse(multiply(inverse(multiply(f1,multiply(inverse(X1),X1))),multiply(f1,X2))) = multiply(inverse(X2),inverse(multiply(multiply(inverse(f1),f1),multiply(inverse(X3),X3)))),
inference(step,[status(thm)],[t4478,t4729]) ).
cnf(t9571,plain,
multiply(inverse(X2),inverse(multiply(inverse(multiply(f1,X1)),multiply(f1,X1)))) = multiply(inverse(X2),inverse(multiply(multiply(inverse(f1),f1),multiply(inverse(X3),X3)))),
inference(step,[status(thm)],[t9570,t5083]) ).
cnf(t9572,plain,
multiply(inverse(X2),inverse(multiply(inverse(f1),f1))) = multiply(inverse(X2),inverse(multiply(multiply(inverse(f1),f1),multiply(inverse(X3),X3)))),
inference(step,[status(thm)],[t9571,t2275]) ).
cnf(t9573,plain,
multiply(inverse(X2),inverse(multiply(inverse(f1),f1))) = inverse(multiply(multiply(inverse(f1),f1),multiply(multiply(inverse(f1),f1),X2))),
inference(step,[status(thm)],[t9572,t4419]) ).
cnf(t5232,plain,
inverse(multiply(multiply(inverse(f1),f1),multiply(multiply(inverse(f1),f1),X1))) = multiply(inverse(X1),inverse(multiply(inverse(f1),f1))),
inference(orient,[status(thm)],[t9573]) ).
cnf(t5233,plain,
multiply(inverse(X1),inverse(multiply(inverse(f1),f1))) = inverse(multiply(multiply(inverse(X2),X2),multiply(multiply(inverse(f1),f1),X1))),
inference(cp,[status(thm)],[t5232,t2075]) ).
cnf(t5290,plain,
inverse(multiply(multiply(inverse(X1),X1),multiply(multiply(inverse(f1),f1),X2))) = multiply(inverse(X2),inverse(multiply(inverse(f1),f1))),
inference(orient,[status(thm)],[t5233]) ).
cnf(t5298,plain,
multiply(inverse(X1),inverse(multiply(inverse(f1),f1))) = inverse(multiply(multiply(inverse(X2),X2),multiply(multiply(inverse(X3),X3),X1))),
inference(cp,[status(thm)],[t5290,t2075]) ).
cnf(t5364,plain,
inverse(multiply(multiply(inverse(X1),X1),multiply(multiply(inverse(X2),X2),X3))) = multiply(inverse(X3),inverse(multiply(inverse(f1),f1))),
inference(orient,[status(thm)],[t5298]) ).
cnf(t5400,plain,
multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(inverse(f1),f1))) = inverse(multiply(multiply(inverse(X3),X3),multiply(inverse(multiply(f1,X1)),multiply(f1,X2)))),
inference(cp,[status(thm)],[t5364,t4729]) ).
cnf(t9576,plain,
multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(inverse(f1),f1))) = inverse(multiply(inverse(multiply(f1,multiply(f1,X1))),multiply(f1,multiply(f1,X2)))),
inference(step,[status(thm)],[t5400,t4729]) ).
cnf(t5453,plain,
inverse(multiply(inverse(multiply(f1,multiply(f1,X1))),multiply(f1,multiply(f1,X2)))) = multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(inverse(f1),f1))),
inference(orient,[status(thm)],[t9576]) ).
cnf(t5454,plain,
multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(inverse(f1),f1))) = inverse(multiply(inverse(multiply(X3,multiply(f1,X1))),multiply(X3,multiply(f1,X2)))),
inference(cp,[status(thm)],[t5453,t24]) ).
cnf(t5527,plain,
inverse(multiply(inverse(multiply(X1,multiply(f1,X2))),multiply(X1,multiply(f1,X3)))) = multiply(inverse(multiply(inverse(X2),X3)),inverse(multiply(inverse(f1),f1))),
inference(orient,[status(thm)],[t5454]) ).
cnf(t9611,plain,
multiply(inverse(Y5),inverse(multiply(inverse(multiply(f1,multiply(X2,Y4))),multiply(f1,multiply(X2,multiply(X3,Y3)))))) = multiply(inverse(Y5),multiply(inverse(multiply(inverse(Y4),multiply(X3,Y3))),inverse(multiply(inverse(f1),f1)))),
inference(step,[status(thm)],[t9610,t5527]) ).
cnf(t7552,plain,
multiply(inverse(X1),inverse(multiply(inverse(multiply(f1,multiply(X2,X3))),multiply(f1,multiply(X2,multiply(Y3,Y4)))))) = multiply(inverse(X1),multiply(inverse(multiply(inverse(X3),multiply(Y3,Y4))),inverse(multiply(inverse(f1),f1)))),
inference(orient,[status(thm)],[t9611]) ).
cnf(t2650,plain,
inverse(multiply(inverse(X1),X1)) = inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),multiply(inverse(X3),X3))),
inference(cp,[status(thm)],[t2615,t2075]) ).
cnf(t2813,plain,
inverse(multiply(inverse(X1),X1)) = inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),multiply(inverse(X3),X3))),
inference(orient,[status(thm)],[t2650]) ).
cnf(t7592,plain,
multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,X3))),inverse(multiply(inverse(f1),f1)))) = multiply(inverse(X1),inverse(multiply(inverse(inverse(multiply(inverse(Y3),Y3))),multiply(inverse(Y4),Y4)))),
inference(cp,[status(thm)],[t7552,t2813]) ).
cnf(t4559,plain,
inverse(multiply(multiply(inverse(f1),f1),multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(X3),X3)))))) = inverse(multiply(inverse(multiply(inverse(Y3),Y3)),inverse(multiply(multiply(inverse(f1),f1),multiply(X2,X1))))),
inference(cp,[status(thm)],[t4284,t4419]) ).
cnf(t9578,plain,
inverse(multiply(multiply(inverse(f1),f1),inverse(multiply(multiply(inverse(f1),f1),multiply(X2,X1))))) = inverse(multiply(inverse(multiply(inverse(Y3),Y3)),inverse(multiply(multiply(inverse(f1),f1),multiply(X2,X1))))),
inference(step,[status(thm)],[t4559,t4419]) ).
cnf(t5632,plain,
inverse(multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(multiply(inverse(f1),f1),multiply(X2,X3))))) = inverse(multiply(multiply(inverse(f1),f1),inverse(multiply(multiply(inverse(f1),f1),multiply(X2,X3))))),
inference(orient,[status(thm)],[t9578]) ).
cnf(t5691,plain,
multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(multiply(inverse(f1),f1),multiply(X2,X3)))) = multiply(inverse(multiply(Y3,inverse(multiply(inverse(inverse(multiply(multiply(inverse(f1),f1),inverse(multiply(multiply(inverse(f1),f1),multiply(X2,X3)))))),multiply(inverse(f1),inverse(multiply(inverse(f1),f1))))))),multiply(Y3,f1)),
inference(cp,[status(thm)],[t298,t5632]) ).
cnf(t9579,plain,
multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(multiply(inverse(f1),f1),multiply(X2,X3)))) = multiply(multiply(inverse(f1),f1),inverse(multiply(multiply(inverse(f1),f1),multiply(X2,X3)))),
inference(step,[status(thm)],[t5691,t298]) ).
cnf(t5730,plain,
multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(multiply(inverse(f1),f1),multiply(X2,X3)))) = multiply(multiply(inverse(f1),f1),inverse(multiply(multiply(inverse(f1),f1),multiply(X2,X3)))),
inference(orient,[status(thm)],[t9579]) ).
cnf(t5750,plain,
multiply(multiply(inverse(f1),f1),inverse(multiply(multiply(inverse(f1),f1),multiply(X1,X2)))) = multiply(inverse(multiply(inverse(X3),X3)),inverse(multiply(multiply(inverse(Y3),Y3),multiply(X1,X2)))),
inference(cp,[status(thm)],[t5730,t2075]) ).
cnf(t5820,plain,
multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(multiply(inverse(X2),X2),multiply(X3,Y3)))) = multiply(multiply(inverse(f1),f1),inverse(multiply(multiply(inverse(f1),f1),multiply(X3,Y3)))),
inference(orient,[status(thm)],[t5750]) ).
cnf(t5876,plain,
multiply(multiply(inverse(f1),f1),inverse(multiply(multiply(inverse(f1),f1),multiply(inverse(X1),X2)))) = multiply(inverse(multiply(inverse(X3),X3)),inverse(multiply(inverse(multiply(f1,X1)),multiply(f1,X2)))),
inference(cp,[status(thm)],[t5820,t4729]) ).
cnf(t9582,plain,
multiply(multiply(inverse(f1),f1),inverse(multiply(inverse(multiply(f1,X1)),multiply(f1,X2)))) = multiply(inverse(multiply(inverse(X3),X3)),inverse(multiply(inverse(multiply(f1,X1)),multiply(f1,X2)))),
inference(step,[status(thm)],[t5876,t4729]) ).
cnf(t5930,plain,
multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(multiply(f1,X2)),multiply(f1,X3)))) = multiply(multiply(inverse(f1),f1),inverse(multiply(inverse(multiply(f1,X2)),multiply(f1,X3)))),
inference(orient,[status(thm)],[t9582]) ).
cnf(t5937,plain,
multiply(multiply(inverse(f1),f1),inverse(multiply(inverse(multiply(f1,inverse(multiply(inverse(inverse(X1)),multiply(inverse(f1),inverse(multiply(inverse(f1),f1))))))),multiply(f1,f1)))) = multiply(inverse(multiply(inverse(X2),X2)),inverse(X1)),
inference(cp,[status(thm)],[t5930,t298]) ).
cnf(t9583,plain,
multiply(multiply(inverse(f1),f1),inverse(X1)) = multiply(inverse(multiply(inverse(X2),X2)),inverse(X1)),
inference(step,[status(thm)],[t5937,t298]) ).
cnf(t6011,plain,
multiply(inverse(multiply(inverse(X1),X1)),inverse(X2)) = multiply(multiply(inverse(f1),f1),inverse(X2)),
inference(orient,[status(thm)],[t9583]) ).
cnf(t6016,plain,
multiply(multiply(inverse(f1),f1),inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X3)))),multiply(inverse(X3),inverse(multiply(inverse(X3),X3)))))) = multiply(inverse(multiply(inverse(Y3),Y3)),X2),
inference(cp,[status(thm)],[t6011,t11]) ).
cnf(t9587,plain,
multiply(multiply(inverse(f1),f1),X2) = multiply(inverse(multiply(inverse(Y3),Y3)),X2),
inference(step,[status(thm)],[t6016,t11]) ).
cnf(t6093,plain,
multiply(inverse(multiply(inverse(X1),X1)),X2) = multiply(multiply(inverse(f1),f1),X2),
inference(orient,[status(thm)],[t9587]) ).
cnf(t9612,plain,
multiply(inverse(X1),multiply(multiply(inverse(f1),f1),inverse(multiply(inverse(f1),f1)))) = multiply(inverse(X1),inverse(multiply(inverse(inverse(multiply(inverse(Y3),Y3))),multiply(inverse(Y4),Y4)))),
inference(step,[status(thm)],[t7592,t6093]) ).
cnf(t5542,plain,
multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(f1),f1))) = inverse(multiply(inverse(X2),X2)),
inference(cp,[status(thm)],[t5527,t2075]) ).
cnf(t9595,plain,
multiply(multiply(inverse(f1),f1),inverse(multiply(inverse(f1),f1))) = inverse(multiply(inverse(X2),X2)),
inference(step,[status(thm)],[t5542,t6093]) ).
cnf(t6290,plain,
multiply(multiply(inverse(f1),f1),inverse(multiply(inverse(f1),f1))) = inverse(multiply(inverse(X1),X1)),
inference(orient,[status(thm)],[t9595]) ).
cnf(t6291,plain,
inverse(multiply(inverse(X1),X1)) = multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(f1),f1))),
inference(cp,[status(thm)],[t6290,t2075]) ).
cnf(t6341,plain,
inverse(multiply(inverse(X1),X1)) = multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(f1),f1))),
inference(orient,[status(thm)],[t6291]) ).
cnf(t9613,plain,
multiply(inverse(X1),inverse(multiply(inverse(f1),f1))) = multiply(inverse(X1),inverse(multiply(inverse(inverse(multiply(inverse(Y3),Y3))),multiply(inverse(Y4),Y4)))),
inference(step,[status(thm)],[t9612,t6341]) ).
cnf(t9614,plain,
multiply(inverse(X1),inverse(multiply(inverse(f1),f1))) = inverse(multiply(multiply(inverse(f1),f1),multiply(inverse(inverse(multiply(inverse(Y3),Y3))),X1))),
inference(step,[status(thm)],[t9613,t4419]) ).
cnf(t9615,plain,
multiply(inverse(X1),inverse(multiply(inverse(f1),f1))) = inverse(multiply(inverse(multiply(f1,inverse(multiply(inverse(Y3),Y3)))),multiply(f1,X1))),
inference(step,[status(thm)],[t9614,t4729]) ).
cnf(t7694,plain,
inverse(multiply(inverse(multiply(f1,inverse(multiply(inverse(X1),X1)))),multiply(f1,X2))) = multiply(inverse(X2),inverse(multiply(inverse(f1),f1))),
inference(orient,[status(thm)],[t9615]) ).
cnf(t7727,plain,
multiply(inverse(X1),inverse(multiply(inverse(f1),f1))) = inverse(multiply(inverse(multiply(f1,multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(f1),f1))))),multiply(f1,X1))),
inference(cp,[status(thm)],[t7694,t7694]) ).
cnf(t9626,plain,
multiply(inverse(X1),inverse(multiply(inverse(f1),f1))) = multiply(inverse(X1),inverse(multiply(inverse(multiply(f1,inverse(multiply(inverse(f1),f1)))),multiply(f1,inverse(multiply(inverse(X2),X2)))))),
inference(step,[status(thm)],[t7727,t5083]) ).
cnf(t9627,plain,
multiply(inverse(X1),inverse(multiply(inverse(f1),f1))) = multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(f1),f1)))),
inference(step,[status(thm)],[t9626,t7694]) ).
cnf(t9628,plain,
multiply(inverse(X1),inverse(multiply(inverse(f1),f1))) = multiply(inverse(X1),multiply(inverse(f1),f1)),
inference(step,[status(thm)],[t9627,t3337]) ).
cnf(t8565,plain,
multiply(inverse(X1),inverse(multiply(inverse(f1),f1))) = multiply(inverse(X1),multiply(inverse(f1),f1)),
inference(orient,[status(thm)],[t9628]) ).
cnf(t8591,plain,
inverse(multiply(inverse(f1),f1)) = inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(X1),multiply(inverse(f1),f1))),multiply(inverse(X1),X2)))),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))),
inference(cp,[status(thm)],[t11,t8565]) ).
cnf(t9644,plain,
inverse(multiply(inverse(f1),f1)) = multiply(inverse(f1),f1),
inference(step,[status(thm)],[t8591,t11]) ).
cnf(t8655,plain,
inverse(multiply(inverse(f1),f1)) = multiply(inverse(f1),f1),
inference(orient,[status(thm)],[t9644]) ).
cnf(t8684,plain,
X1 = inverse(multiply(inverse(multiply(inverse(f1),f1)),multiply(inverse(X1),inverse(multiply(inverse(X2),X2))))),
inference(cp,[status(thm)],[t2615,t8655]) ).
cnf(t9651,plain,
X1 = inverse(multiply(multiply(inverse(f1),f1),multiply(inverse(X1),inverse(multiply(inverse(X2),X2))))),
inference(step,[status(thm)],[t8684,t6093]) ).
cnf(t9652,plain,
X1 = inverse(multiply(inverse(multiply(f1,X1)),multiply(f1,inverse(multiply(inverse(X2),X2))))),
inference(step,[status(thm)],[t9651,t4729]) ).
cnf(t2276,plain,
inverse(multiply(inverse(X1),X1)) = inverse(multiply(inverse(X2),X2)),
inference(cp,[status(thm)],[t2275,t2075]) ).
cnf(t2301,plain,
inverse(multiply(inverse(X1),X1)) = inverse(multiply(inverse(X2),X2)),
inference(orient,[status(thm)],[t2276]) ).
cnf(t2302,plain,
inverse(multiply(inverse(X1),X1)) = inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,X3))),
inference(cp,[status(thm)],[t2301,t24]) ).
cnf(t9530,plain,
inverse(multiply(inverse(X1),X1)) = inverse(multiply(inverse(f1),f1)),
inference(step,[status(thm)],[t2302,t2275]) ).
cnf(t2435,plain,
inverse(multiply(inverse(X1),X1)) = inverse(multiply(inverse(f1),f1)),
inference(orient,[status(thm)],[t9530]) ).
cnf(t9646,plain,
inverse(multiply(inverse(X1),X1)) = multiply(inverse(f1),f1),
inference(step,[status(thm)],[t2435,t8655]) ).
cnf(t8657,plain,
inverse(multiply(inverse(X1),X1)) = multiply(inverse(f1),f1),
inference(orient,[status(thm)],[t9646]) ).
cnf(t9653,plain,
X1 = inverse(multiply(inverse(multiply(f1,X1)),multiply(f1,multiply(inverse(f1),f1)))),
inference(step,[status(thm)],[t9652,t8657]) ).
cnf(t8729,plain,
inverse(multiply(inverse(multiply(f1,X1)),multiply(f1,multiply(inverse(f1),f1)))) = X1,
inference(orient,[status(thm)],[t9653]) ).
cnf(t8748,plain,
X1 = inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(f1),f1)),inverse(multiply(inverse(multiply(inverse(f1),f1)),multiply(inverse(f1),f1)))))),
inference(cp,[status(thm)],[t11,t8729]) ).
cnf(t9654,plain,
X1 = inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(f1),f1),multiply(inverse(multiply(inverse(f1),f1)),multiply(inverse(f1),f1)))))),
inference(step,[status(thm)],[t8748,t4419]) ).
cnf(t9655,plain,
X1 = inverse(inverse(multiply(multiply(inverse(f1),f1),multiply(multiply(inverse(f1),f1),X1)))),
inference(step,[status(thm)],[t9654,t4419]) ).
cnf(t9633,plain,
inverse(multiply(multiply(inverse(X1),X1),multiply(multiply(inverse(X2),X2),X3))) = multiply(inverse(X3),multiply(inverse(f1),f1)),
inference(step,[status(thm)],[t5364,t8565]) ).
cnf(t8570,plain,
inverse(multiply(multiply(inverse(X1),X1),multiply(multiply(inverse(X2),X2),X3))) = multiply(inverse(X3),multiply(inverse(f1),f1)),
inference(orient,[status(thm)],[t9633]) ).
cnf(t9656,plain,
X1 = inverse(multiply(inverse(X1),multiply(inverse(f1),f1))),
inference(step,[status(thm)],[t9655,t8570]) ).
cnf(t8835,plain,
inverse(multiply(inverse(X1),multiply(inverse(f1),f1))) = X1,
inference(orient,[status(thm)],[t9656]) ).
cnf(t8866,plain,
multiply(inverse(X1),multiply(inverse(f1),f1)) = inverse(multiply(X1,multiply(inverse(f1),f1))),
inference(cp,[status(thm)],[t8835,t8835]) ).
cnf(t8947,plain,
inverse(multiply(X1,multiply(inverse(f1),f1))) = multiply(inverse(X1),multiply(inverse(f1),f1)),
inference(orient,[status(thm)],[t8866]) ).
cnf(t9657,plain,
multiply(inverse(inverse(X1)),multiply(inverse(f1),f1)) = X1,
inference(step,[status(thm)],[t8835,t8947]) ).
cnf(t8948,plain,
multiply(inverse(inverse(X1)),multiply(inverse(f1),f1)) = X1,
inference(rw,[status(thm)],[t9657]) ).
cnf(t9201,plain,
multiply(inverse(inverse(X1)),multiply(inverse(f1),f1)) = X1,
inference(orient,[status(thm)],[t8948]) ).
cnf(t9208,plain,
X1 = multiply(inverse(inverse(X1)),multiply(inverse(X2),X2)),
inference(cp,[status(thm)],[t9201,t2075]) ).
cnf(t9268,plain,
multiply(inverse(inverse(X1)),multiply(inverse(X2),X2)) = X1,
inference(orient,[status(thm)],[t9208]) ).
cnf(t9302,plain,
X1 = inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X2)),X1)),X2))),multiply(inverse(multiply(inverse(X3),X3)),inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3)))))),
inference(cp,[status(thm)],[t11,t9268]) ).
cnf(t9664,plain,
X1 = inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X2)),X1)),X2))),multiply(multiply(inverse(f1),f1),inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3)))))),
inference(step,[status(thm)],[t9302,t6093]) ).
cnf(t7623,plain,
inverse(multiply(inverse(multiply(f1,multiply(X1,X2))),multiply(f1,multiply(X1,multiply(X3,Y3))))) = inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(Y4),multiply(inverse(multiply(inverse(X2),multiply(X3,Y3))),inverse(multiply(inverse(f1),f1))))),multiply(inverse(Y4),Y5)))),multiply(inverse(Y5),inverse(multiply(inverse(Y5),Y5))))),
inference(cp,[status(thm)],[t11,t7552]) ).
cnf(t9616,plain,
inverse(multiply(inverse(multiply(f1,multiply(X1,X2))),multiply(f1,multiply(X1,multiply(X3,Y3))))) = multiply(inverse(multiply(inverse(X2),multiply(X3,Y3))),inverse(multiply(inverse(f1),f1))),
inference(step,[status(thm)],[t7623,t11]) ).
cnf(t7825,plain,
inverse(multiply(inverse(multiply(f1,multiply(X1,X2))),multiply(f1,multiply(X1,multiply(X3,Y3))))) = multiply(inverse(multiply(inverse(X2),multiply(X3,Y3))),inverse(multiply(inverse(f1),f1))),
inference(orient,[status(thm)],[t9616]) ).
cnf(t7846,plain,
multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(X2,inverse(multiply(inverse(inverse(X3)),multiply(inverse(f1),inverse(multiply(inverse(f1),f1))))))),multiply(X2,f1)))),inverse(multiply(inverse(f1),f1))) = inverse(multiply(inverse(multiply(f1,multiply(Y3,X1))),multiply(f1,multiply(Y3,X3)))),
inference(cp,[status(thm)],[t7825,t298]) ).
cnf(t9618,plain,
multiply(inverse(multiply(inverse(X1),X3)),inverse(multiply(inverse(f1),f1))) = inverse(multiply(inverse(multiply(f1,multiply(Y3,X1))),multiply(f1,multiply(Y3,X3)))),
inference(step,[status(thm)],[t7846,t298]) ).
cnf(t7966,plain,
inverse(multiply(inverse(multiply(f1,multiply(X1,X2))),multiply(f1,multiply(X1,X3)))) = multiply(inverse(multiply(inverse(X2),X3)),inverse(multiply(inverse(f1),f1))),
inference(orient,[status(thm)],[t9618]) ).
cnf(t7968,plain,
multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(inverse(f1),f1))) = inverse(multiply(inverse(multiply(X3,multiply(Y3,X1))),multiply(X3,multiply(Y3,X2)))),
inference(cp,[status(thm)],[t7966,t24]) ).
cnf(t8090,plain,
inverse(multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,multiply(X2,Y3)))) = multiply(inverse(multiply(inverse(X3),Y3)),inverse(multiply(inverse(f1),f1))),
inference(orient,[status(thm)],[t7968]) ).
cnf(t8122,plain,
multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(inverse(f1),f1))) = inverse(multiply(inverse(multiply(X3,multiply(inverse(X2),X1))),multiply(X3,multiply(inverse(Y3),Y3)))),
inference(cp,[status(thm)],[t8090,t2075]) ).
cnf(t9622,plain,
multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(inverse(f1),f1))) = multiply(inverse(multiply(inverse(Y3),Y3)),inverse(multiply(inverse(multiply(f1,X1)),multiply(f1,X2)))),
inference(step,[status(thm)],[t8122,t5083]) ).
cnf(t9623,plain,
multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(inverse(f1),f1))) = multiply(multiply(inverse(f1),f1),inverse(multiply(inverse(multiply(f1,X1)),multiply(f1,X2)))),
inference(step,[status(thm)],[t9622,t6093]) ).
cnf(t8253,plain,
multiply(multiply(inverse(f1),f1),inverse(multiply(inverse(multiply(f1,X1)),multiply(f1,X2)))) = multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(inverse(f1),f1))),
inference(orient,[status(thm)],[t9623]) ).
cnf(t8254,plain,
multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(inverse(f1),f1))) = multiply(multiply(inverse(f1),f1),inverse(multiply(inverse(multiply(X3,X1)),multiply(X3,X2)))),
inference(cp,[status(thm)],[t8253,t24]) ).
cnf(t8323,plain,
multiply(multiply(inverse(f1),f1),inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X3)))) = multiply(inverse(multiply(inverse(X2),X3)),inverse(multiply(inverse(f1),f1))),
inference(orient,[status(thm)],[t8254]) ).
cnf(t8346,plain,
multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(inverse(f1),f1))) = multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(multiply(Y3,X1)),multiply(Y3,X2)))),
inference(cp,[status(thm)],[t8323,t2075]) ).
cnf(t8433,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,Y3)))) = multiply(inverse(multiply(inverse(X3),Y3)),inverse(multiply(inverse(f1),f1))),
inference(orient,[status(thm)],[t8346]) ).
cnf(t9642,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,Y3)))) = multiply(inverse(multiply(inverse(X3),Y3)),multiply(inverse(f1),f1)),
inference(step,[status(thm)],[t8433,t8565]) ).
cnf(t8579,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,Y3)))) = multiply(inverse(multiply(inverse(X3),Y3)),multiply(inverse(f1),f1)),
inference(orient,[status(thm)],[t9642]) ).
cnf(t9665,plain,
X1 = inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X2)),X1)),X2))),multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(f1),f1)))),
inference(step,[status(thm)],[t9664,t8579]) ).
cnf(t9666,plain,
X1 = inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X2)),X1)),X2))),multiply(multiply(inverse(f1),f1),multiply(inverse(f1),f1)))),
inference(step,[status(thm)],[t9665,t6093]) ).
cnf(t9667,plain,
X1 = inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X2)),X1)),X2))),multiply(inverse(multiply(f1,f1)),multiply(f1,f1)))),
inference(step,[status(thm)],[t9666,t4729]) ).
cnf(t8954,plain,
multiply(inverse(X1),multiply(inverse(f1),f1)) = inverse(multiply(X1,multiply(inverse(X2),X2))),
inference(cp,[status(thm)],[t8947,t2075]) ).
cnf(t9066,plain,
inverse(multiply(X1,multiply(inverse(X2),X2))) = multiply(inverse(X1),multiply(inverse(f1),f1)),
inference(orient,[status(thm)],[t8954]) ).
cnf(t9668,plain,
X1 = multiply(inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X2)),X1)),X2)))),multiply(inverse(f1),f1)),
inference(step,[status(thm)],[t9667,t9066]) ).
cnf(t9669,plain,
X1 = inverse(multiply(inverse(multiply(inverse(inverse(X2)),X1)),X2)),
inference(step,[status(thm)],[t9668,t9268]) ).
cnf(t9349,plain,
inverse(multiply(inverse(multiply(inverse(inverse(X1)),X2)),X1)) = X2,
inference(orient,[status(thm)],[t9669]) ).
cnf(t9363,plain,
X1 = inverse(multiply(inverse(multiply(inverse(multiply(inverse(f1),f1)),X1)),multiply(inverse(X2),X2))),
inference(cp,[status(thm)],[t9349,t8657]) ).
cnf(t9670,plain,
X1 = multiply(inverse(inverse(multiply(inverse(multiply(inverse(f1),f1)),X1))),multiply(inverse(f1),f1)),
inference(step,[status(thm)],[t9363,t9066]) ).
cnf(t9671,plain,
X1 = multiply(inverse(multiply(inverse(f1),f1)),X1),
inference(step,[status(thm)],[t9670,t9268]) ).
cnf(t9672,plain,
X1 = multiply(multiply(inverse(f1),f1),X1),
inference(step,[status(thm)],[t9671,t6093]) ).
cnf(t9436,plain,
multiply(multiply(inverse(f1),f1),X1) = X1,
inference(orient,[status(thm)],[t9672]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(multiply(inverse(f1),f1),a2) != a2,
inference(rw,[status(thm)],[goal_0,t2164]) ).
cnf(g0_1,plain,
a2 != a2,
inference(rw,[status(thm)],[g0_0,t9436]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP422-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n015.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.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 14:46:25 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 42.29/6.06 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 42.29/6.06 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------