%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP414-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:17 PM UTC 2026
% Result : Unsatisfiable 9.25s 1.97s
% Output : CNFRefutation 9.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 88
% Number of leaves : 2
% Syntax : Number of clauses : 140 ( 140 unt; 0 nHn; 3 RR)
% Number of literals : 140 ( 139 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 14 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 421 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X1,inverse(X2))),X3))),X2))) = X3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t1,plain,
multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X1,inverse(X2))),X3))),X2))) = X3,
inference(orient,[status(thm)],[t0]) ).
cnf(t2,plain,
inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),inverse(X1))),Y3))),X1)) = multiply(X2,inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(Y3)),X3))),
inference(cp,[status(thm)],[t1,t1]) ).
cnf(t4,plain,
inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),inverse(X1))),Y3))),X1)) = multiply(X2,inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(Y3)),X3))),
inference(orient,[status(thm)],[t2]) ).
cnf(t8,plain,
X1 = multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X1)),X3)))),
inference(cp,[status(thm)],[t1,t4]) ).
cnf(t34,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2)))) = X3,
inference(orient,[status(thm)],[t8]) ).
cnf(t39,plain,
multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),inverse(X3))),Y3) = multiply(inverse(multiply(Y4,inverse(X3))),multiply(Y4,multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(Y3)),X2))))),
inference(cp,[status(thm)],[t34,t4]) ).
cnf(t46,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,multiply(X3,inverse(multiply(multiply(multiply(inverse(Y3),Y3),inverse(Y4)),Y3))))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(Y3))),inverse(X2))),Y4),
inference(orient,[status(thm)],[t39]) ).
cnf(t51,plain,
multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),inverse(X3))),multiply(inverse(multiply(X1,inverse(X2))),Y3)) = multiply(inverse(multiply(Y4,inverse(X3))),multiply(Y4,Y3)),
inference(cp,[status(thm)],[t46,t1]) ).
cnf(t62,plain,
multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),inverse(X3))),multiply(inverse(multiply(X1,inverse(X2))),Y3)) = multiply(inverse(multiply(Y4,inverse(X3))),multiply(Y4,Y3)),
inference(orient,[status(thm)],[t51]) ).
cnf(t87,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X3)) = multiply(inverse(multiply(Y3,inverse(X2))),multiply(Y3,X3)),
inference(cp,[status(thm)],[t62,t62]) ).
cnf(t107,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X3)) = multiply(inverse(multiply(Y3,inverse(X2))),multiply(Y3,X3)),
inference(orient,[status(thm)],[t87]) ).
cnf(t123,plain,
multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X1,inverse(X2))),X3))),X2))) = inverse(multiply(multiply(multiply(inverse(Y3),Y3),inverse(multiply(inverse(multiply(Y4,inverse(Y3))),multiply(Y4,X3)))),Y3)),
inference(cp,[status(thm)],[t4,t107]) ).
cnf(t6213,plain,
X3 = inverse(multiply(multiply(multiply(inverse(Y3),Y3),inverse(multiply(inverse(multiply(Y4,inverse(Y3))),multiply(Y4,X3)))),Y3)),
inference(step,[status(thm)],[t123,t1]) ).
cnf(t125,plain,
inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,X3)))),X1)) = X3,
inference(orient,[status(thm)],[t6213]) ).
cnf(t157,plain,
multiply(inverse(multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,Y3)))),X2)))),multiply(X1,Y4)) = multiply(inverse(multiply(Y5,Y3)),multiply(Y5,Y4)),
inference(cp,[status(thm)],[t107,t125]) ).
cnf(t6214,plain,
multiply(inverse(multiply(X1,Y3)),multiply(X1,Y4)) = multiply(inverse(multiply(Y5,Y3)),multiply(Y5,Y4)),
inference(step,[status(thm)],[t157,t125]) ).
cnf(t165,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(multiply(Y3,X2)),multiply(Y3,X3)),
inference(orient,[status(thm)],[t6214]) ).
cnf(t41,plain,
multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(multiply(inverse(X2),X2),inverse(X1))),X3))),X1) = multiply(inverse(multiply(Y3,inverse(X2))),multiply(Y3,inverse(multiply(X3,X2)))),
inference(cp,[status(thm)],[t34,t1]) ).
cnf(t1697,plain,
multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(multiply(inverse(X2),X2),inverse(X1))),X3))),X1) = multiply(inverse(multiply(Y3,inverse(X2))),multiply(Y3,inverse(multiply(X3,X2)))),
inference(orient,[status(thm)],[t41]) ).
cnf(t166,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(Y3,multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(Y4,inverse(X2))),multiply(Y4,Y3)))),X3)),
inference(cp,[status(thm)],[t165,t125]) ).
cnf(t1165,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(Y3,multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(Y4,inverse(X2))),multiply(Y4,Y3)))),X3)),
inference(orient,[status(thm)],[t166]) ).
cnf(t1827,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X2)) = multiply(X3,multiply(inverse(multiply(Y3,inverse(Y4))),multiply(Y3,inverse(multiply(multiply(multiply(inverse(Y4),Y4),X3),Y4))))),
inference(cp,[status(thm)],[t1165,t1697]) ).
cnf(t2953,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X2)) = multiply(X3,multiply(inverse(multiply(Y3,inverse(Y4))),multiply(Y3,inverse(multiply(multiply(multiply(inverse(Y4),Y4),X3),Y4))))),
inference(orient,[status(thm)],[t1827]) ).
cnf(t168,plain,
multiply(inverse(multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X3,inverse(X2))),Y3))),X2)))),multiply(X1,Y4)) = multiply(inverse(Y3),multiply(X3,Y4)),
inference(cp,[status(thm)],[t165,t1]) ).
cnf(t295,plain,
multiply(inverse(multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X3,inverse(X2))),Y3))),X2)))),multiply(X1,Y4)) = multiply(inverse(Y3),multiply(X3,Y4)),
inference(orient,[status(thm)],[t168]) ).
cnf(t1798,plain,
multiply(inverse(X1),multiply(multiply(inverse(X2),X2),X3)) = multiply(inverse(multiply(Y3,inverse(multiply(inverse(multiply(Y4,inverse(X2))),multiply(Y4,inverse(multiply(X1,X2))))))),multiply(Y3,X3)),
inference(cp,[status(thm)],[t295,t1697]) ).
cnf(t2314,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(multiply(Y3,X3))))))),multiply(X1,Y4)) = multiply(inverse(Y3),multiply(multiply(inverse(X3),X3),Y4)),
inference(orient,[status(thm)],[t1798]) ).
cnf(t3133,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X2)) = multiply(inverse(X3),multiply(multiply(inverse(Y3),Y3),multiply(Y4,inverse(multiply(multiply(multiply(inverse(Y5),Y5),inverse(multiply(inverse(multiply(Y4,inverse(Y5))),inverse(multiply(inverse(multiply(Y6,inverse(Y3))),multiply(Y6,inverse(multiply(X3,Y3)))))))),Y5))))),
inference(cp,[status(thm)],[t2953,t2314]) ).
cnf(t6218,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X2)) = multiply(inverse(X3),multiply(multiply(inverse(Y3),Y3),inverse(multiply(inverse(multiply(Y6,inverse(Y3))),multiply(Y6,inverse(multiply(X3,Y3))))))),
inference(step,[status(thm)],[t3133,t1]) ).
cnf(t1767,plain,
X1 = multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(multiply(X1,X2)))))),
inference(cp,[status(thm)],[t1,t1697]) ).
cnf(t2023,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(multiply(X3,X1)))))) = X3,
inference(orient,[status(thm)],[t1767]) ).
cnf(t6219,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X2)) = multiply(inverse(X3),X3),
inference(step,[status(thm)],[t6218,t2023]) ).
cnf(t3279,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X2)) = multiply(inverse(X3),X3),
inference(orient,[status(thm)],[t6219]) ).
cnf(t146,plain,
multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(multiply(Y3,inverse(X3))),multiply(Y3,Y4)))),X3)))),Y5) = multiply(inverse(multiply(Y6,Y4)),multiply(Y6,multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(Y5)),X2))))),
inference(cp,[status(thm)],[t46,t125]) ).
cnf(t6215,plain,
multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),Y4)),Y5) = multiply(inverse(multiply(Y6,Y4)),multiply(Y6,multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(Y5)),X2))))),
inference(step,[status(thm)],[t146,t125]) ).
cnf(t187,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,multiply(X3,inverse(multiply(multiply(multiply(inverse(Y3),Y3),inverse(Y4)),Y3))))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(Y3))),X2)),Y4),
inference(orient,[status(thm)],[t6215]) ).
cnf(t3280,plain,
multiply(inverse(X1),X1) = multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(Y3)),X3))))),Y3),
inference(cp,[status(thm)],[t3279,t187]) ).
cnf(t1753,plain,
X1 = inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(multiply(multiply(multiply(inverse(X3),X3),X1),X3))))),
inference(cp,[status(thm)],[t125,t1697]) ).
cnf(t1931,plain,
inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),X3),X2))))) = X3,
inference(orient,[status(thm)],[t1753]) ).
cnf(t6220,plain,
multiply(inverse(X1),X1) = multiply(inverse(Y3),Y3),
inference(step,[status(thm)],[t3280,t1931]) ).
cnf(t3519,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),X2),
inference(orient,[status(thm)],[t6220]) ).
cnf(t3619,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2)))) = multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(Y3),Y3))),X3),
inference(cp,[status(thm)],[t1697,t3519]) ).
cnf(t6221,plain,
X3 = multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(Y3),Y3))),X3),
inference(step,[status(thm)],[t3619,t34]) ).
cnf(t3625,plain,
multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X2),X2))),X1) = X1,
inference(orient,[status(thm)],[t6221]) ).
cnf(t3633,plain,
X1 = multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(X3),X3))),X1),
inference(cp,[status(thm)],[t3625,t3519]) ).
cnf(t3722,plain,
multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X2),X2))),X3) = X3,
inference(orient,[status(thm)],[t3633]) ).
cnf(t3782,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(X2),multiply(multiply(multiply(inverse(Y3),Y3),inverse(multiply(inverse(Y4),Y4))),X3)),
inference(cp,[status(thm)],[t165,t3722]) ).
cnf(t6222,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(X2),X3),
inference(step,[status(thm)],[t3782,t3722]) ).
cnf(t3810,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(X2),X3),
inference(orient,[status(thm)],[t6222]) ).
cnf(t3819,plain,
multiply(inverse(X1),X2) = multiply(inverse(multiply(inverse(X2),X1)),multiply(inverse(X3),X3)),
inference(cp,[status(thm)],[t3810,t3519]) ).
cnf(t3884,plain,
multiply(inverse(multiply(inverse(X1),X2)),multiply(inverse(X3),X3)) = multiply(inverse(X2),X1),
inference(orient,[status(thm)],[t3819]) ).
cnf(t3896,plain,
multiply(inverse(multiply(inverse(X1),X1)),X2) = multiply(inverse(multiply(inverse(X3),Y3)),multiply(inverse(multiply(inverse(Y3),X3)),X2)),
inference(cp,[status(thm)],[t3810,t3884]) ).
cnf(t3815,plain,
multiply(inverse(X1),X2) = multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X1),X2)),
inference(cp,[status(thm)],[t3810,t3519]) ).
cnf(t3846,plain,
multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X2),X3)) = multiply(inverse(X2),X3),
inference(orient,[status(thm)],[t3815]) ).
cnf(t3851,plain,
multiply(inverse(X1),inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(inverse(X1),inverse(X2))),X3))),X2))) = multiply(inverse(multiply(inverse(Y3),Y3)),X3),
inference(cp,[status(thm)],[t3846,t1]) ).
cnf(t6242,plain,
X3 = multiply(inverse(multiply(inverse(Y3),Y3)),X3),
inference(step,[status(thm)],[t3851,t1]) ).
cnf(t3866,plain,
multiply(inverse(multiply(inverse(X1),X1)),X2) = X2,
inference(orient,[status(thm)],[t6242]) ).
cnf(t6243,plain,
X2 = multiply(inverse(multiply(inverse(X3),Y3)),multiply(inverse(multiply(inverse(Y3),X3)),X2)),
inference(step,[status(thm)],[t3896,t3866]) ).
cnf(t3907,plain,
multiply(inverse(multiply(inverse(X1),X2)),multiply(inverse(multiply(inverse(X2),X1)),X3)) = X3,
inference(orient,[status(thm)],[t6243]) ).
cnf(t3908,plain,
X1 = multiply(inverse(X2),multiply(inverse(multiply(inverse(X2),multiply(inverse(X3),X3))),X1)),
inference(cp,[status(thm)],[t3907,t3866]) ).
cnf(t3932,plain,
multiply(inverse(X1),multiply(inverse(multiply(inverse(X1),multiply(inverse(X2),X2))),X3)) = X3,
inference(orient,[status(thm)],[t3908]) ).
cnf(t3723,plain,
inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(X3),X3))),inverse(X1))),Y3))),X1)) = Y3,
inference(cp,[status(thm)],[t3722,t1]) ).
cnf(t6244,plain,
inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X1)),Y3))),X1)) = Y3,
inference(step,[status(thm)],[t3723,t3722]) ).
cnf(t3990,plain,
inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X1)),X2))),X1)) = X2,
inference(orient,[status(thm)],[t6244]) ).
cnf(t4012,plain,
X1 = multiply(X2,multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(inverse(X3)),X2))),X3)),multiply(inverse(Y3),Y3))),X1)),
inference(cp,[status(thm)],[t3932,t3990]) ).
cnf(t6245,plain,
X1 = multiply(X2,multiply(inverse(multiply(X2,multiply(inverse(Y3),Y3))),X1)),
inference(step,[status(thm)],[t4012,t3990]) ).
cnf(t4031,plain,
multiply(X1,multiply(inverse(multiply(X1,multiply(inverse(X2),X2))),X3)) = X3,
inference(orient,[status(thm)],[t6245]) ).
cnf(t6230,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X1)),inverse(multiply(X3,X1))))) = X3,
inference(step,[status(thm)],[t2023,t3810]) ).
cnf(t3836,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X1)),inverse(multiply(X3,X1))))) = X3,
inference(rw,[status(thm)],[t6230]) ).
cnf(t4059,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1))))) = X2,
inference(orient,[status(thm)],[t3836]) ).
cnf(t4064,plain,
X1 = multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(inverse(X3)),inverse(multiply(X1,X3))))),
inference(cp,[status(thm)],[t4059,t3519]) ).
cnf(t4220,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X2)),inverse(multiply(X3,X2))))) = X3,
inference(orient,[status(thm)],[t4064]) ).
cnf(t4244,plain,
inverse(X1) = multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X3),X3))))),
inference(cp,[status(thm)],[t4220,t3519]) ).
cnf(t4921,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X2)),inverse(multiply(inverse(X3),X3))))) = inverse(X2),
inference(orient,[status(thm)],[t4244]) ).
cnf(t3996,plain,
X1 = inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(inverse(X3)),X1))),X3)),
inference(cp,[status(thm)],[t3990,t3519]) ).
cnf(t4175,plain,
inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X2)),X3))),X2)) = X3,
inference(orient,[status(thm)],[t3996]) ).
cnf(t4930,plain,
inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X2)),X3))),X2)) = multiply(multiply(inverse(Y3),Y3),inverse(multiply(inverse(X3),inverse(multiply(inverse(Y4),Y4))))),
inference(cp,[status(thm)],[t4921,t4175]) ).
cnf(t6248,plain,
X3 = multiply(multiply(inverse(Y3),Y3),inverse(multiply(inverse(X3),inverse(multiply(inverse(Y4),Y4))))),
inference(step,[status(thm)],[t4930,t4175]) ).
cnf(t4959,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X2),inverse(multiply(inverse(X3),X3))))) = X2,
inference(orient,[status(thm)],[t6248]) ).
cnf(t6231,plain,
multiply(inverse(inverse(X2)),inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))) = X3,
inference(step,[status(thm)],[t34,t3810]) ).
cnf(t3837,plain,
multiply(inverse(inverse(X2)),inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))) = X3,
inference(rw,[status(thm)],[t6231]) ).
cnf(t4091,plain,
multiply(inverse(inverse(X1)),inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X1))) = X2,
inference(orient,[status(thm)],[t3837]) ).
cnf(t4103,plain,
X1 = multiply(inverse(inverse(X2)),inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X1)),X2))),
inference(cp,[status(thm)],[t4091,t3519]) ).
cnf(t4256,plain,
multiply(inverse(inverse(X1)),inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X1))) = X3,
inference(orient,[status(thm)],[t4103]) ).
cnf(t4994,plain,
inverse(multiply(inverse(X1),X1)) = multiply(X2,inverse(multiply(multiply(X2,inverse(X3)),X3))),
inference(cp,[status(thm)],[t1,t4959]) ).
cnf(t5004,plain,
inverse(multiply(inverse(X1),X1)) = multiply(X2,inverse(multiply(multiply(X2,inverse(X3)),X3))),
inference(orient,[status(thm)],[t4994]) ).
cnf(t5164,plain,
multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X2) = multiply(inverse(inverse(X3)),inverse(multiply(inverse(multiply(inverse(Y3),Y3)),X3))),
inference(cp,[status(thm)],[t4256,t5004]) ).
cnf(t6250,plain,
multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X2) = multiply(inverse(inverse(X3)),inverse(X3)),
inference(step,[status(thm)],[t5164,t3866]) ).
cnf(t6251,plain,
multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X2) = multiply(inverse(c3),c3),
inference(step,[status(thm)],[t6250,t3519]) ).
cnf(t5653,plain,
multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X2) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t6251]) ).
cnf(t5684,plain,
multiply(multiply(inverse(X1),X1),inverse(X2)) = multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(inverse(X2)),inverse(multiply(inverse(c3),c3))))),
inference(cp,[status(thm)],[t4220,t5653]) ).
cnf(t6252,plain,
multiply(multiply(inverse(X1),X1),inverse(X2)) = inverse(X2),
inference(step,[status(thm)],[t5684,t4921]) ).
cnf(t5701,plain,
multiply(multiply(inverse(X1),X1),inverse(X2)) = inverse(X2),
inference(orient,[status(thm)],[t6252]) ).
cnf(t6263,plain,
inverse(multiply(inverse(X2),inverse(multiply(inverse(X3),X3)))) = X2,
inference(step,[status(thm)],[t4959,t5701]) ).
cnf(t5733,plain,
inverse(multiply(inverse(X2),inverse(multiply(inverse(X3),X3)))) = X2,
inference(rw,[status(thm)],[t6263]) ).
cnf(t6237,plain,
inverse(multiply(inverse(inverse(X2)),inverse(multiply(multiply(multiply(inverse(X2),X2),X3),X2)))) = X3,
inference(step,[status(thm)],[t1931,t3810]) ).
cnf(t3841,plain,
inverse(multiply(inverse(inverse(X2)),inverse(multiply(multiply(multiply(inverse(X2),X2),X3),X2)))) = X3,
inference(rw,[status(thm)],[t6237]) ).
cnf(t4121,plain,
inverse(multiply(inverse(inverse(X1)),inverse(multiply(multiply(multiply(inverse(X1),X1),X2),X1)))) = X2,
inference(orient,[status(thm)],[t3841]) ).
cnf(t4134,plain,
X1 = inverse(multiply(inverse(inverse(X2)),inverse(multiply(multiply(multiply(inverse(X3),X3),X1),X2)))),
inference(cp,[status(thm)],[t4121,t3519]) ).
cnf(t4287,plain,
inverse(multiply(inverse(inverse(X1)),inverse(multiply(multiply(multiply(inverse(X2),X2),X3),X1)))) = X3,
inference(orient,[status(thm)],[t4134]) ).
cnf(t5710,plain,
inverse(multiply(inverse(inverse(X1)),inverse(multiply(multiply(multiply(inverse(X2),X2),X3),X1)))) = multiply(multiply(inverse(Y3),Y3),X3),
inference(cp,[status(thm)],[t5701,t4287]) ).
cnf(t6267,plain,
X3 = multiply(multiply(inverse(Y3),Y3),X3),
inference(step,[status(thm)],[t5710,t4287]) ).
cnf(t5737,plain,
multiply(multiply(inverse(X1),X1),X2) = X2,
inference(orient,[status(thm)],[t6267]) ).
cnf(t4970,plain,
multiply(inverse(X1),X1) = multiply(multiply(inverse(X2),X2),inverse(inverse(multiply(inverse(X3),X3)))),
inference(cp,[status(thm)],[t4959,t3866]) ).
cnf(t5175,plain,
multiply(inverse(X1),X1) = multiply(multiply(inverse(X2),X2),inverse(inverse(multiply(inverse(X3),X3)))),
inference(orient,[status(thm)],[t4970]) ).
cnf(t5309,plain,
multiply(inverse(X1),X1) = multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(inverse(inverse(inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(Y3),Y3))))),
inference(cp,[status(thm)],[t4220,t5175]) ).
cnf(t6249,plain,
multiply(inverse(X1),X1) = inverse(inverse(inverse(multiply(inverse(X3),X3)))),
inference(step,[status(thm)],[t5309,t4921]) ).
cnf(t5316,plain,
multiply(inverse(X1),X1) = inverse(inverse(inverse(multiply(inverse(X2),X2)))),
inference(orient,[status(thm)],[t6249]) ).
cnf(t5744,plain,
X1 = multiply(multiply(multiply(inverse(X2),X2),inverse(inverse(multiply(inverse(X3),X3)))),X1),
inference(cp,[status(thm)],[t5737,t5316]) ).
cnf(t6276,plain,
X1 = multiply(inverse(inverse(multiply(inverse(X3),X3))),X1),
inference(step,[status(thm)],[t5744,t5701]) ).
cnf(t5753,plain,
multiply(inverse(inverse(multiply(inverse(X1),X1))),X2) = X2,
inference(orient,[status(thm)],[t6276]) ).
cnf(t5757,plain,
inverse(multiply(inverse(X1),X1)) = multiply(inverse(X2),X2),
inference(cp,[status(thm)],[t5753,t3519]) ).
cnf(t5780,plain,
inverse(multiply(inverse(X1),X1)) = multiply(inverse(X2),X2),
inference(orient,[status(thm)],[t5757]) ).
cnf(t6277,plain,
inverse(multiply(inverse(X2),multiply(inverse(c3),c3))) = X2,
inference(step,[status(thm)],[t5733,t5780]) ).
cnf(t5890,plain,
inverse(multiply(inverse(X1),multiply(inverse(c3),c3))) = X1,
inference(orient,[status(thm)],[t6277]) ).
cnf(t5922,plain,
X1 = multiply(inverse(X2),multiply(X2,X1)),
inference(cp,[status(thm)],[t4031,t5890]) ).
cnf(t5933,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(orient,[status(thm)],[t5922]) ).
cnf(t5951,plain,
multiply(X1,X2) = multiply(inverse(inverse(X1)),X2),
inference(cp,[status(thm)],[t5933,t5933]) ).
cnf(t5973,plain,
multiply(inverse(inverse(X1)),X2) = multiply(X1,X2),
inference(orient,[status(thm)],[t5951]) ).
cnf(t5975,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(cp,[status(thm)],[t5973,t5933]) ).
cnf(t5994,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t5975]) ).
cnf(t6008,plain,
X1 = multiply(X1,multiply(inverse(X2),X2)),
inference(cp,[status(thm)],[t5994,t3519]) ).
cnf(t6044,plain,
multiply(X1,multiply(inverse(X2),X2)) = X1,
inference(orient,[status(thm)],[t6008]) ).
cnf(t6045,plain,
inverse(inverse(X1)) = multiply(X1,multiply(inverse(X2),X2)),
inference(cp,[status(thm)],[t6044,t5973]) ).
cnf(t6283,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t6045,t6044]) ).
cnf(t6082,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t6283]) ).
cnf(t6084,plain,
X1 = multiply(X1,multiply(X2,inverse(X2))),
inference(cp,[status(thm)],[t6044,t6082]) ).
cnf(t6091,plain,
multiply(X1,multiply(X2,inverse(X2))) = X1,
inference(orient,[status(thm)],[t6084]) ).
cnf(t6096,plain,
inverse(multiply(X1,X2)) = multiply(inverse(X2),inverse(X1)),
inference(cp,[status(thm)],[t6091,t3810]) ).
cnf(t6143,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t6096]) ).
cnf(t6152,plain,
inverse(X1) = multiply(X2,inverse(multiply(X1,X2))),
inference(cp,[status(thm)],[t5994,t6143]) ).
cnf(t6200,plain,
multiply(X1,inverse(multiply(X2,X1))) = inverse(X2),
inference(orient,[status(thm)],[t6152]) ).
cnf(t6204,plain,
multiply(inverse(inverse(multiply(X1,X2))),X3) = multiply(inverse(inverse(X1)),multiply(X2,X3)),
inference(cp,[status(thm)],[t3810,t6200]) ).
cnf(t6295,plain,
multiply(multiply(X1,X2),X3) = multiply(inverse(inverse(X1)),multiply(X2,X3)),
inference(step,[status(thm)],[t6204,t5973]) ).
cnf(t6296,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(step,[status(thm)],[t6295,t5973]) ).
cnf(t6206,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t6296]) ).
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,t6206]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP414-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.16/0.44 % Computer : n013.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Wed Sep 23 14:41:21 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.44 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 9.25/1.97 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.25/1.97 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------