%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP404-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 : n009.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:05 PM UTC 2026
% Result : Unsatisfiable 15.81s 2.56s
% Output : CNFRefutation 15.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 61
% Number of leaves : 2
% Syntax : Number of clauses : 90 ( 90 unt; 0 nHn; 3 RR)
% Number of literals : 90 ( 89 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 321 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),inverse(multiply(X2,multiply(inverse(X2),X2)))))) = X3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t1,plain,
multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),inverse(multiply(X2,multiply(inverse(X2),X2)))))) = X3,
inference(orient,[status(thm)],[t0]) ).
cnf(t2,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),Y3)),inverse(multiply(X3,multiply(inverse(X3),X3))))) = multiply(X1,inverse(multiply(inverse(Y3),inverse(multiply(X2,multiply(inverse(X2),X2)))))),
inference(cp,[status(thm)],[t1,t1]) ).
cnf(t4,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),Y3)),inverse(multiply(X3,multiply(inverse(X3),X3))))) = multiply(X1,inverse(multiply(inverse(Y3),inverse(multiply(X2,multiply(inverse(X2),X2)))))),
inference(orient,[status(thm)],[t2]) ).
cnf(t8,plain,
X1 = multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(inverse(X1),inverse(multiply(X3,multiply(inverse(X3),X3))))))),
inference(cp,[status(thm)],[t1,t4]) ).
cnf(t29,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(inverse(X3),inverse(multiply(X2,multiply(inverse(X2),X2))))))) = X3,
inference(orient,[status(thm)],[t8]) ).
cnf(t33,plain,
multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),Y3) = multiply(inverse(multiply(Y4,X3)),multiply(Y4,multiply(X1,inverse(multiply(inverse(Y3),inverse(multiply(X2,multiply(inverse(X2),X2)))))))),
inference(cp,[status(thm)],[t29,t4]) ).
cnf(t41,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,multiply(X3,inverse(multiply(inverse(Y3),inverse(multiply(Y4,multiply(inverse(Y4),Y4)))))))) = multiply(inverse(multiply(inverse(multiply(X3,Y4)),X2)),Y3),
inference(orient,[status(thm)],[t33]) ).
cnf(t46,plain,
multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),multiply(inverse(multiply(X1,X2)),Y3)) = multiply(inverse(multiply(Y4,X3)),multiply(Y4,Y3)),
inference(cp,[status(thm)],[t41,t1]) ).
cnf(t64,plain,
multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),multiply(inverse(multiply(X1,X2)),Y3)) = multiply(inverse(multiply(Y4,X3)),multiply(Y4,Y3)),
inference(orient,[status(thm)],[t46]) ).
cnf(t102,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(multiply(Y3,X2)),multiply(Y3,X3)),
inference(cp,[status(thm)],[t64,t64]) ).
cnf(t132,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(multiply(Y3,X2)),multiply(Y3,X3)),
inference(orient,[status(thm)],[t102]) ).
cnf(t152,plain,
multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),inverse(multiply(X2,multiply(inverse(X2),X2)))))) = inverse(multiply(inverse(multiply(inverse(multiply(Y3,Y4)),multiply(Y3,X3))),inverse(multiply(Y4,multiply(inverse(Y4),Y4))))),
inference(cp,[status(thm)],[t4,t132]) ).
cnf(t6521,plain,
X3 = inverse(multiply(inverse(multiply(inverse(multiply(Y3,Y4)),multiply(Y3,X3))),inverse(multiply(Y4,multiply(inverse(Y4),Y4))))),
inference(step,[status(thm)],[t152,t1]) ).
cnf(t157,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X3))),inverse(multiply(X2,multiply(inverse(X2),X2))))) = X3,
inference(orient,[status(thm)],[t6521]) ).
cnf(t176,plain,
inverse(multiply(X1,multiply(inverse(X1),X1))) = multiply(inverse(multiply(X2,X1)),inverse(multiply(X3,inverse(multiply(multiply(X2,X3),multiply(inverse(multiply(X2,X3)),multiply(X2,X3))))))),
inference(cp,[status(thm)],[t1,t157]) ).
cnf(t2127,plain,
inverse(multiply(X1,multiply(inverse(X1),X1))) = multiply(inverse(multiply(X2,X1)),inverse(multiply(X3,inverse(multiply(multiply(X2,X3),multiply(inverse(multiply(X2,X3)),multiply(X2,X3))))))),
inference(orient,[status(thm)],[t176]) ).
cnf(t2360,plain,
X1 = multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(X1)))),inverse(multiply(X3,multiply(inverse(X3),X3)))),
inference(cp,[status(thm)],[t29,t2127]) ).
cnf(t2383,plain,
multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(X3)))),inverse(multiply(X2,multiply(inverse(X2),X2)))) = X3,
inference(orient,[status(thm)],[t2360]) ).
cnf(t187,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,multiply(inverse(X2),X2))))),multiply(X1,X3)) = multiply(Y3,multiply(inverse(multiply(inverse(multiply(Y4,X2)),multiply(Y4,Y3))),X3)),
inference(cp,[status(thm)],[t132,t157]) ).
cnf(t1239,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,multiply(inverse(X2),X2))))),multiply(X1,X3)) = multiply(Y3,multiply(inverse(multiply(inverse(multiply(Y4,X2)),multiply(Y4,Y3))),X3)),
inference(orient,[status(thm)],[t187]) ).
cnf(t1246,plain,
multiply(X1,multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,X1))),Y3)) = multiply(Y4,multiply(inverse(multiply(inverse(multiply(Y5,X3)),multiply(Y5,Y4))),Y3)),
inference(cp,[status(thm)],[t1239,t157]) ).
cnf(t1470,plain,
multiply(X1,multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,X1))),Y3)) = multiply(Y4,multiply(inverse(multiply(inverse(multiply(Y5,X3)),multiply(Y5,Y4))),Y3)),
inference(orient,[status(thm)],[t1246]) ).
cnf(t134,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),Y3)),inverse(multiply(X3,multiply(inverse(X3),X3))))))),multiply(X1,Y4)) = multiply(inverse(Y3),multiply(X2,Y4)),
inference(cp,[status(thm)],[t132,t1]) ).
cnf(t277,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),Y3)),inverse(multiply(X3,multiply(inverse(X3),X3))))))),multiply(X1,Y4)) = multiply(inverse(Y3),multiply(X2,Y4)),
inference(orient,[status(thm)],[t134]) ).
cnf(t1490,plain,
multiply(X1,multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(multiply(X3,Y3)),Y4)),inverse(multiply(Y3,multiply(inverse(Y3),Y3))))))),multiply(X2,X1))),Y5)) = multiply(Y6,multiply(inverse(multiply(inverse(Y4),multiply(X3,Y6))),Y5)),
inference(cp,[status(thm)],[t1470,t277]) ).
cnf(t6523,plain,
multiply(X1,multiply(inverse(multiply(inverse(Y4),multiply(X3,X1))),Y5)) = multiply(Y6,multiply(inverse(multiply(inverse(Y4),multiply(X3,Y6))),Y5)),
inference(step,[status(thm)],[t1490,t277]) ).
cnf(t1600,plain,
multiply(X1,multiply(inverse(multiply(inverse(X2),multiply(X3,X1))),Y3)) = multiply(Y4,multiply(inverse(multiply(inverse(X2),multiply(X3,Y4))),Y3)),
inference(orient,[status(thm)],[t6523]) ).
cnf(t138,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X3,Y3)),Y4)),inverse(multiply(Y3,multiply(inverse(Y3),Y3))))))) = multiply(inverse(multiply(X3,X2)),Y4),
inference(cp,[status(thm)],[t132,t1]) ).
cnf(t335,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X3,Y3)),Y4)),inverse(multiply(Y3,multiply(inverse(Y3),Y3))))))) = multiply(inverse(multiply(X3,X2)),Y4),
inference(orient,[status(thm)],[t138]) ).
cnf(t1606,plain,
multiply(X1,multiply(inverse(multiply(inverse(X2),multiply(X3,X1))),multiply(inverse(X2),inverse(multiply(inverse(multiply(inverse(multiply(Y3,Y4)),Y5)),inverse(multiply(Y4,multiply(inverse(Y4),Y4)))))))) = multiply(Y6,multiply(inverse(multiply(Y3,multiply(X3,Y6))),Y5)),
inference(cp,[status(thm)],[t1600,t335]) ).
cnf(t6524,plain,
multiply(X1,multiply(inverse(multiply(Y3,multiply(X3,X1))),Y5)) = multiply(Y6,multiply(inverse(multiply(Y3,multiply(X3,Y6))),Y5)),
inference(step,[status(thm)],[t1606,t335]) ).
cnf(t1721,plain,
multiply(X1,multiply(inverse(multiply(X2,multiply(X3,X1))),Y3)) = multiply(Y4,multiply(inverse(multiply(X2,multiply(X3,Y4))),Y3)),
inference(orient,[status(thm)],[t6524]) ).
cnf(t1775,plain,
multiply(inverse(multiply(X1,multiply(X2,inverse(multiply(X3,Y3))))),Y4) = multiply(X3,inverse(multiply(inverse(multiply(Y5,multiply(inverse(multiply(X1,multiply(X2,Y5))),Y4))),inverse(multiply(Y3,multiply(inverse(Y3),Y3)))))),
inference(cp,[status(thm)],[t1,t1721]) ).
cnf(t1975,plain,
multiply(X1,inverse(multiply(inverse(multiply(X2,multiply(inverse(multiply(X3,multiply(Y3,X2))),Y4))),inverse(multiply(Y5,multiply(inverse(Y5),Y5)))))) = multiply(inverse(multiply(X3,multiply(Y3,inverse(multiply(X1,Y5))))),Y4),
inference(orient,[status(thm)],[t1775]) ).
cnf(t2467,plain,
multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(X3,Y3))))),inverse(multiply(X2,multiply(inverse(X2),X2)))) = multiply(X3,inverse(multiply(inverse(multiply(inverse(Y4),Y4)),inverse(multiply(Y3,multiply(inverse(Y3),Y3)))))),
inference(cp,[status(thm)],[t1975,t2383]) ).
cnf(t6525,plain,
multiply(X3,Y3) = multiply(X3,inverse(multiply(inverse(multiply(inverse(Y4),Y4)),inverse(multiply(Y3,multiply(inverse(Y3),Y3)))))),
inference(step,[status(thm)],[t2467,t2383]) ).
cnf(t2516,plain,
multiply(X1,inverse(multiply(inverse(multiply(inverse(X2),X2)),inverse(multiply(X3,multiply(inverse(X3),X3)))))) = multiply(X1,X3),
inference(orient,[status(thm)],[t6525]) ).
cnf(t2562,plain,
multiply(inverse(X1),X1) = multiply(inverse(multiply(X2,X3)),multiply(X2,X3)),
inference(cp,[status(thm)],[t29,t2516]) ).
cnf(t2625,plain,
multiply(inverse(X1),X1) = multiply(inverse(multiply(X2,X3)),multiply(X2,X3)),
inference(orient,[status(thm)],[t2562]) ).
cnf(t2738,plain,
multiply(inverse(X1),X1) = multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),Y3)),inverse(multiply(X3,multiply(inverse(X3),X3))))))),Y3),
inference(cp,[status(thm)],[t2625,t335]) ).
cnf(t6526,plain,
multiply(inverse(X1),X1) = multiply(inverse(Y3),Y3),
inference(step,[status(thm)],[t2738,t1]) ).
cnf(t2867,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),X2),
inference(orient,[status(thm)],[t6526]) ).
cnf(t2884,plain,
X1 = multiply(inverse(multiply(inverse(X2),X2)),inverse(multiply(inverse(X1),multiply(inverse(inverse(X1)),inverse(X1))))),
inference(cp,[status(thm)],[t2383,t2867]) ).
cnf(t6528,plain,
X1 = multiply(inverse(multiply(inverse(X2),X2)),inverse(multiply(inverse(X1),multiply(inverse(b2),b2)))),
inference(step,[status(thm)],[t2884,t2867]) ).
cnf(t3127,plain,
multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(X2),multiply(inverse(b2),b2)))) = X2,
inference(orient,[status(thm)],[t6528]) ).
cnf(t3445,plain,
multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(X2),multiply(inverse(b2),b2)))) = X2,
inference(rw,[status(thm)],[t3127]) ).
cnf(t3139,plain,
multiply(inverse(b2),b2) = multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(X2),X2))),
inference(cp,[status(thm)],[t3127,t2867]) ).
cnf(t3193,plain,
multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(X2),X2))) = multiply(inverse(b2),b2),
inference(orient,[status(thm)],[t3139]) ).
cnf(t3218,plain,
inverse(multiply(inverse(X1),X1)) = multiply(inverse(X2),inverse(multiply(inverse(multiply(inverse(b2),b2)),inverse(multiply(X2,multiply(inverse(X2),X2)))))),
inference(cp,[status(thm)],[t1,t3193]) ).
cnf(t6529,plain,
inverse(multiply(inverse(X1),X1)) = multiply(inverse(X2),X2),
inference(step,[status(thm)],[t3218,t2516]) ).
cnf(t3264,plain,
inverse(multiply(inverse(X1),X1)) = multiply(inverse(X2),X2),
inference(orient,[status(thm)],[t6529]) ).
cnf(t6532,plain,
multiply(multiply(inverse(b2),b2),inverse(multiply(inverse(X2),multiply(inverse(b2),b2)))) = X2,
inference(step,[status(thm)],[t3445,t3264]) ).
cnf(t3776,plain,
multiply(multiply(inverse(b2),b2),inverse(multiply(inverse(X1),multiply(inverse(b2),b2)))) = X1,
inference(orient,[status(thm)],[t6532]) ).
cnf(t3777,plain,
X1 = multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(X1),multiply(inverse(b2),b2)))),
inference(cp,[status(thm)],[t3776,t2867]) ).
cnf(t3824,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X2),multiply(inverse(b2),b2)))) = X2,
inference(orient,[status(thm)],[t3777]) ).
cnf(t3845,plain,
X1 = multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(X1),multiply(inverse(X3),X3)))),
inference(cp,[status(thm)],[t3824,t2867]) ).
cnf(t3882,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X2),multiply(inverse(X3),X3)))) = X2,
inference(orient,[status(thm)],[t3845]) ).
cnf(t3904,plain,
multiply(inverse(X1),X2) = multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(multiply(Y3,X2)),multiply(Y3,X1)))),
inference(cp,[status(thm)],[t3882,t132]) ).
cnf(t3964,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,Y3)))) = multiply(inverse(Y3),X3),
inference(orient,[status(thm)],[t3904]) ).
cnf(t3285,plain,
X1 = inverse(multiply(multiply(inverse(X2),X2),inverse(multiply(X1,multiply(inverse(X1),X1))))),
inference(cp,[status(thm)],[t157,t3264]) ).
cnf(t3624,plain,
inverse(multiply(multiply(inverse(X1),X1),inverse(multiply(X2,multiply(inverse(X2),X2))))) = X2,
inference(orient,[status(thm)],[t3285]) ).
cnf(t3641,plain,
X1 = inverse(multiply(multiply(inverse(X2),X2),inverse(multiply(X1,multiply(inverse(X3),X3))))),
inference(cp,[status(thm)],[t3624,t2867]) ).
cnf(t3695,plain,
inverse(multiply(multiply(inverse(X1),X1),inverse(multiply(X2,multiply(inverse(X3),X3))))) = X2,
inference(orient,[status(thm)],[t3641]) ).
cnf(t3292,plain,
inverse(multiply(X1,multiply(inverse(X1),X1))) = multiply(inverse(multiply(X2,X1)),multiply(X2,multiply(inverse(X3),X3))),
inference(cp,[status(thm)],[t29,t3264]) ).
cnf(t4762,plain,
inverse(multiply(X1,multiply(inverse(X1),X1))) = multiply(inverse(multiply(X2,X1)),multiply(X2,multiply(inverse(X3),X3))),
inference(orient,[status(thm)],[t3292]) ).
cnf(t4801,plain,
X1 = inverse(multiply(multiply(inverse(X2),X2),multiply(inverse(multiply(X3,X1)),multiply(X3,multiply(inverse(Y3),Y3))))),
inference(cp,[status(thm)],[t3695,t4762]) ).
cnf(t3314,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(multiply(inverse(Y3),Y3),multiply(inverse(X2),X3)),
inference(cp,[status(thm)],[t132,t3264]) ).
cnf(t4166,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(multiply(inverse(Y3),Y3),multiply(inverse(X2),X3)),
inference(orient,[status(thm)],[t3314]) ).
cnf(t6534,plain,
X1 = inverse(multiply(inverse(multiply(b2,multiply(X3,X1))),multiply(b2,multiply(X3,multiply(inverse(Y3),Y3))))),
inference(step,[status(thm)],[t4801,t4166]) ).
cnf(t5345,plain,
inverse(multiply(inverse(multiply(b2,multiply(X1,X2))),multiply(b2,multiply(X1,multiply(inverse(X3),X3))))) = X2,
inference(orient,[status(thm)],[t6534]) ).
cnf(t150,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,multiply(X3,Y3))) = multiply(inverse(multiply(inverse(multiply(X3,Y4)),X2)),multiply(inverse(multiply(Y5,Y4)),multiply(Y5,Y3))),
inference(cp,[status(thm)],[t132,t132]) ).
cnf(t549,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,multiply(X3,Y3))) = multiply(inverse(multiply(inverse(multiply(X3,Y4)),X2)),multiply(inverse(multiply(Y5,Y4)),multiply(Y5,Y3))),
inference(orient,[status(thm)],[t150]) ).
cnf(t149,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)],[t132,t132]) ).
cnf(t401,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)],[t149]) ).
cnf(t632,plain,
multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,multiply(X2,Y3))) = multiply(inverse(multiply(Y4,multiply(Y5,X3))),multiply(Y4,multiply(Y5,Y3))),
inference(cp,[status(thm)],[t549,t401]) ).
cnf(t731,plain,
multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,multiply(X2,Y3))) = multiply(inverse(multiply(Y4,multiply(Y5,X3))),multiply(Y4,multiply(Y5,Y3))),
inference(orient,[status(thm)],[t632]) ).
cnf(t5348,plain,
X1 = inverse(multiply(inverse(multiply(X2,multiply(X3,X1))),multiply(X2,multiply(X3,multiply(inverse(Y3),Y3))))),
inference(cp,[status(thm)],[t5345,t731]) ).
cnf(t5499,plain,
inverse(multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,multiply(X2,multiply(inverse(Y3),Y3))))) = X3,
inference(orient,[status(thm)],[t5348]) ).
cnf(t5626,plain,
multiply(inverse(multiply(X1,multiply(inverse(X2),X2))),multiply(X1,X3)) = multiply(multiply(inverse(Y3),Y3),X3),
inference(cp,[status(thm)],[t3964,t5499]) ).
cnf(t5695,plain,
multiply(inverse(multiply(X1,multiply(inverse(X2),X2))),multiply(X1,X3)) = multiply(multiply(inverse(Y3),Y3),X3),
inference(orient,[status(thm)],[t5626]) ).
cnf(t5767,plain,
multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X2),multiply(inverse(X3),X3)))) = multiply(inverse(multiply(multiply(inverse(Y3),Y3),multiply(inverse(Y4),Y4))),X2),
inference(cp,[status(thm)],[t5695,t3882]) ).
cnf(t6535,plain,
X2 = multiply(inverse(multiply(multiply(inverse(Y3),Y3),multiply(inverse(Y4),Y4))),X2),
inference(step,[status(thm)],[t5767,t3882]) ).
cnf(t6536,plain,
X2 = multiply(inverse(multiply(inverse(multiply(b2,Y4)),multiply(b2,Y4))),X2),
inference(step,[status(thm)],[t6535,t4166]) ).
cnf(t6537,plain,
X2 = multiply(inverse(multiply(inverse(b2),b2)),X2),
inference(step,[status(thm)],[t6536,t2625]) ).
cnf(t6538,plain,
X2 = multiply(multiply(inverse(b2),b2),X2),
inference(step,[status(thm)],[t6537,t3264]) ).
cnf(t6422,plain,
multiply(multiply(inverse(b2),b2),X1) = X1,
inference(orient,[status(thm)],[t6538]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
a2 != a2,
inference(rw,[status(thm)],[goal_0,t6422]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP404-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 : n009.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:40:43 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.44 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 15.81/2.56 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.81/2.56 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------