%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP477-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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:27:08 PM UTC 2026
% Result : Unsatisfiable 4.12s 1.03s
% Output : CNFRefutation 4.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 78
% Number of leaves : 3
% Syntax : Number of clauses : 147 ( 147 unt; 0 nHn; 3 RR)
% Number of literals : 147 ( 146 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 555 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t1,axiom,
divide(inverse(divide(divide(divide(X1,X2),X3),divide(X4,X3))),divide(X2,X1)) = X4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t2,plain,
divide(inverse(divide(divide(divide(X1,X2),X3),divide(X4,X3))),divide(X2,X1)) = X4,
inference(orient,[status(thm)],[t1]) ).
cnf(t0,axiom,
divide(X1,inverse(X2)) = multiply(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t6,plain,
divide(X1,inverse(X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t0]) ).
cnf(t7,plain,
X1 = divide(inverse(divide(multiply(divide(X2,X3),X4),divide(X1,inverse(X4)))),divide(X3,X2)),
inference(cp,[status(thm)],[t2,t6]) ).
cnf(t11064,plain,
X1 = divide(inverse(divide(multiply(divide(X2,X3),X4),multiply(X1,X4))),divide(X3,X2)),
inference(step,[status(thm)],[t7,t6]) ).
cnf(t11,plain,
divide(inverse(divide(multiply(divide(X1,X2),X3),multiply(X4,X3))),divide(X2,X1)) = X4,
inference(orient,[status(thm)],[t11064]) ).
cnf(t12,plain,
X1 = divide(inverse(divide(multiply(multiply(X2,X3),X4),multiply(X1,X4))),divide(inverse(X3),X2)),
inference(cp,[status(thm)],[t11,t6]) ).
cnf(t55,plain,
divide(inverse(divide(multiply(multiply(X1,X2),X3),multiply(X4,X3))),divide(inverse(X2),X1)) = X4,
inference(orient,[status(thm)],[t12]) ).
cnf(t64,plain,
X1 = divide(inverse(divide(multiply(multiply(divide(inverse(X2),X3),divide(multiply(multiply(X3,X2),X4),multiply(Y4,X4))),Y5),multiply(X1,Y5))),Y4),
inference(cp,[status(thm)],[t55,t55]) ).
cnf(t1806,plain,
divide(inverse(divide(multiply(multiply(divide(inverse(X1),X2),divide(multiply(multiply(X2,X1),X3),multiply(X4,X3))),Y4),multiply(Y5,Y4))),X4) = Y5,
inference(orient,[status(thm)],[t64]) ).
cnf(t67,plain,
X1 = divide(inverse(divide(multiply(X2,X3),multiply(X1,X3))),divide(divide(inverse(X4),Y4),inverse(divide(multiply(multiply(Y4,X4),Y5),multiply(X2,Y5))))),
inference(cp,[status(thm)],[t11,t55]) ).
cnf(t11081,plain,
X1 = divide(inverse(divide(multiply(X2,X3),multiply(X1,X3))),multiply(divide(inverse(X4),Y4),divide(multiply(multiply(Y4,X4),Y5),multiply(X2,Y5)))),
inference(step,[status(thm)],[t67,t6]) ).
cnf(t1901,plain,
divide(inverse(divide(multiply(X1,X2),multiply(X3,X2))),multiply(divide(inverse(X4),Y4),divide(multiply(multiply(Y4,X4),Y5),multiply(X1,Y5)))) = X3,
inference(orient,[status(thm)],[t11081]) ).
cnf(t19,plain,
X1 = divide(inverse(divide(multiply(X2,X3),multiply(X1,X3))),divide(divide(X4,Y4),inverse(divide(multiply(divide(Y4,X4),Y5),multiply(X2,Y5))))),
inference(cp,[status(thm)],[t11,t11]) ).
cnf(t11069,plain,
X1 = divide(inverse(divide(multiply(X2,X3),multiply(X1,X3))),multiply(divide(X4,Y4),divide(multiply(divide(Y4,X4),Y5),multiply(X2,Y5)))),
inference(step,[status(thm)],[t19,t6]) ).
cnf(t349,plain,
divide(inverse(divide(multiply(X1,X2),multiply(X3,X2))),multiply(divide(X4,Y4),divide(multiply(divide(Y4,X4),Y5),multiply(X1,Y5)))) = X3,
inference(orient,[status(thm)],[t11069]) ).
cnf(t4,plain,
inverse(divide(divide(divide(X1,X2),X3),divide(X4,X3))) = divide(inverse(divide(divide(divide(Y4,Y5),divide(X2,X1)),X4)),divide(Y5,Y4)),
inference(cp,[status(thm)],[t2,t2]) ).
cnf(t3151,plain,
inverse(divide(divide(divide(X1,X2),X3),divide(X4,X3))) = divide(inverse(divide(divide(divide(Y4,Y5),divide(X2,X1)),X4)),divide(Y5,Y4)),
inference(orient,[status(thm)],[t4]) ).
cnf(t3258,plain,
inverse(divide(divide(divide(X1,X2),X3),divide(divide(X4,divide(X2,X1)),X3))) = X4,
inference(cp,[status(thm)],[t3151,t2]) ).
cnf(t3451,plain,
inverse(divide(divide(divide(X1,X2),X3),divide(divide(X4,divide(X2,X1)),X3))) = X4,
inference(orient,[status(thm)],[t3258]) ).
cnf(t3452,plain,
X1 = inverse(divide(multiply(divide(X2,X3),X4),divide(divide(X1,divide(X3,X2)),inverse(X4)))),
inference(cp,[status(thm)],[t3451,t6]) ).
cnf(t11085,plain,
X1 = inverse(divide(multiply(divide(X2,X3),X4),multiply(divide(X1,divide(X3,X2)),X4))),
inference(step,[status(thm)],[t3452,t6]) ).
cnf(t3574,plain,
inverse(divide(multiply(divide(X1,X2),X3),multiply(divide(X4,divide(X2,X1)),X3))) = X4,
inference(orient,[status(thm)],[t11085]) ).
cnf(t3667,plain,
divide(X1,divide(X2,X3)) = divide(X1,multiply(divide(X4,Y4),divide(multiply(divide(Y4,X4),Y5),multiply(divide(X3,X2),Y5)))),
inference(cp,[status(thm)],[t349,t3574]) ).
cnf(t5694,plain,
divide(X1,multiply(divide(X2,X3),divide(multiply(divide(X3,X2),X4),multiply(divide(Y4,Y5),X4)))) = divide(X1,divide(Y5,Y4)),
inference(orient,[status(thm)],[t3667]) ).
cnf(t5755,plain,
divide(X1,divide(multiply(divide(X2,X3),divide(multiply(divide(X3,X2),X4),multiply(divide(Y4,Y5),X4))),Y6)) = divide(X1,multiply(divide(Y7,Y8),divide(multiply(divide(Y8,Y7),Y9),multiply(divide(Y6,divide(Y5,Y4)),Y9)))),
inference(cp,[status(thm)],[t5694,t5694]) ).
cnf(t11095,plain,
divide(X1,divide(multiply(divide(X2,X3),divide(multiply(divide(X3,X2),X4),multiply(divide(Y4,Y5),X4))),Y6)) = divide(X1,divide(divide(Y5,Y4),Y6)),
inference(step,[status(thm)],[t5755,t5694]) ).
cnf(t7175,plain,
divide(X1,divide(multiply(divide(X2,X3),divide(multiply(divide(X3,X2),X4),multiply(divide(Y4,Y5),X4))),Y6)) = divide(X1,divide(divide(Y5,Y4),Y6)),
inference(orient,[status(thm)],[t11095]) ).
cnf(t7180,plain,
divide(X1,divide(divide(X2,X3),inverse(X4))) = divide(X1,multiply(multiply(divide(Y4,Y5),divide(multiply(divide(Y5,Y4),Y6),multiply(divide(X3,X2),Y6))),X4)),
inference(cp,[status(thm)],[t7175,t6]) ).
cnf(t11096,plain,
divide(X1,multiply(divide(X2,X3),X4)) = divide(X1,multiply(multiply(divide(Y4,Y5),divide(multiply(divide(Y5,Y4),Y6),multiply(divide(X3,X2),Y6))),X4)),
inference(step,[status(thm)],[t7180,t6]) ).
cnf(t7307,plain,
divide(X1,multiply(multiply(divide(X2,X3),divide(multiply(divide(X3,X2),X4),multiply(divide(Y4,Y5),X4))),Y6)) = divide(X1,multiply(divide(Y5,Y4),Y6)),
inference(orient,[status(thm)],[t11096]) ).
cnf(t7411,plain,
multiply(divide(X1,X2),divide(multiply(divide(X2,X1),X3),multiply(divide(X4,Y4),X3))) = divide(inverse(divide(multiply(Y5,Y6),multiply(divide(Y4,X4),Y6))),multiply(divide(inverse(Y7),Y8),divide(multiply(multiply(Y8,Y7),Y9),multiply(Y5,Y9)))),
inference(cp,[status(thm)],[t1901,t7307]) ).
cnf(t11097,plain,
multiply(divide(X1,X2),divide(multiply(divide(X2,X1),X3),multiply(divide(X4,Y4),X3))) = divide(Y4,X4),
inference(step,[status(thm)],[t7411,t1901]) ).
cnf(t7464,plain,
multiply(divide(X1,X2),divide(multiply(divide(X2,X1),X3),multiply(divide(X4,Y4),X3))) = divide(Y4,X4),
inference(orient,[status(thm)],[t11097]) ).
cnf(t7472,plain,
divide(X1,X2) = multiply(multiply(X3,X4),divide(multiply(divide(inverse(X4),X3),Y4),multiply(divide(X2,X1),Y4))),
inference(cp,[status(thm)],[t7464,t6]) ).
cnf(t7747,plain,
multiply(multiply(X1,X2),divide(multiply(divide(inverse(X2),X1),X3),multiply(divide(X4,Y4),X3))) = divide(Y4,X4),
inference(orient,[status(thm)],[t7472]) ).
cnf(t7857,plain,
X1 = divide(inverse(divide(divide(X2,X3),multiply(X1,divide(multiply(divide(inverse(divide(multiply(multiply(X4,Y4),Y5),multiply(Y6,Y5))),divide(inverse(Y4),X4)),Y7),multiply(divide(X3,X2),Y7))))),Y6),
inference(cp,[status(thm)],[t1806,t7747]) ).
cnf(t11098,plain,
X1 = divide(inverse(divide(divide(X2,X3),multiply(X1,divide(multiply(Y6,Y7),multiply(divide(X3,X2),Y7))))),Y6),
inference(step,[status(thm)],[t7857,t55]) ).
cnf(t8367,plain,
divide(inverse(divide(divide(X1,X2),multiply(X3,divide(multiply(X4,Y4),multiply(divide(X2,X1),Y4))))),X4) = X3,
inference(orient,[status(thm)],[t11098]) ).
cnf(t8391,plain,
divide(X1,X2) = divide(inverse(divide(divide(X3,X4),divide(X3,X4))),divide(X2,X1)),
inference(cp,[status(thm)],[t8367,t7464]) ).
cnf(t3505,plain,
X1 = inverse(divide(divide(divide(inverse(X2),X3),X4),divide(divide(X1,multiply(X3,X2)),X4))),
inference(cp,[status(thm)],[t3451,t6]) ).
cnf(t3792,plain,
inverse(divide(divide(divide(inverse(X1),X2),X3),divide(divide(X4,multiply(X2,X1)),X3))) = X4,
inference(orient,[status(thm)],[t3505]) ).
cnf(t10,plain,
X1 = divide(inverse(divide(divide(divide(inverse(X2),X3),X4),divide(X1,X4))),multiply(X3,X2)),
inference(cp,[status(thm)],[t2,t6]) ).
cnf(t36,plain,
divide(inverse(divide(divide(divide(inverse(X1),X2),X3),divide(X4,X3))),multiply(X2,X1)) = X4,
inference(orient,[status(thm)],[t10]) ).
cnf(t51,plain,
X1 = divide(inverse(divide(multiply(X2,X3),multiply(X1,X3))),divide(multiply(X4,Y4),inverse(divide(divide(divide(inverse(Y4),X4),Y5),divide(X2,Y5))))),
inference(cp,[status(thm)],[t11,t36]) ).
cnf(t11077,plain,
X1 = divide(inverse(divide(multiply(X2,X3),multiply(X1,X3))),multiply(multiply(X4,Y4),divide(divide(divide(inverse(Y4),X4),Y5),divide(X2,Y5)))),
inference(step,[status(thm)],[t51,t6]) ).
cnf(t1330,plain,
divide(inverse(divide(multiply(X1,X2),multiply(X3,X2))),multiply(multiply(X4,Y4),divide(divide(divide(inverse(Y4),X4),Y5),divide(X1,Y5)))) = X3,
inference(orient,[status(thm)],[t11077]) ).
cnf(t3851,plain,
inverse(divide(multiply(X1,X2),multiply(X3,X2))) = inverse(divide(divide(divide(inverse(divide(divide(divide(inverse(X4),Y4),Y5),divide(X1,Y5))),multiply(Y4,X4)),Y6),divide(X3,Y6))),
inference(cp,[status(thm)],[t3792,t1330]) ).
cnf(t11087,plain,
inverse(divide(multiply(X1,X2),multiply(X3,X2))) = inverse(divide(divide(X1,Y6),divide(X3,Y6))),
inference(step,[status(thm)],[t3851,t36]) ).
cnf(t4217,plain,
inverse(divide(multiply(X1,X2),multiply(X3,X2))) = inverse(divide(divide(X1,X4),divide(X3,X4))),
inference(orient,[status(thm)],[t11087]) ).
cnf(t11099,plain,
divide(X1,X2) = divide(inverse(divide(multiply(X3,c3),multiply(X3,c3))),divide(X2,X1)),
inference(step,[status(thm)],[t8391,t4217]) ).
cnf(t8485,plain,
divide(inverse(divide(multiply(X1,c3),multiply(X1,c3))),divide(X2,X3)) = divide(X3,X2),
inference(orient,[status(thm)],[t11099]) ).
cnf(t4291,plain,
inverse(divide(multiply(X1,X2),multiply(inverse(divide(multiply(divide(X3,X4),Y4),multiply(Y5,Y4))),X2))) = inverse(divide(divide(X1,divide(X4,X3)),Y5)),
inference(cp,[status(thm)],[t4217,t11]) ).
cnf(t6250,plain,
inverse(divide(multiply(X1,X2),multiply(inverse(divide(multiply(divide(X3,X4),Y4),multiply(Y5,Y4))),X2))) = inverse(divide(divide(X1,divide(X4,X3)),Y5)),
inference(orient,[status(thm)],[t4291]) ).
cnf(t8486,plain,
divide(X1,X2) = divide(inverse(divide(divide(inverse(divide(multiply(divide(X3,X4),Y4),multiply(Y5,Y4))),divide(X4,X3)),Y5)),divide(X2,X1)),
inference(cp,[status(thm)],[t8485,t6250]) ).
cnf(t11100,plain,
divide(X1,X2) = divide(inverse(divide(Y5,Y5)),divide(X2,X1)),
inference(step,[status(thm)],[t8486,t11]) ).
cnf(t8556,plain,
divide(inverse(divide(X1,X1)),divide(X2,X3)) = divide(X3,X2),
inference(orient,[status(thm)],[t11100]) ).
cnf(t8573,plain,
divide(divide(X1,X2),inverse(divide(X3,X3))) = divide(inverse(divide(X4,X4)),divide(X2,X1)),
inference(cp,[status(thm)],[t8556,t8556]) ).
cnf(t11101,plain,
multiply(divide(X1,X2),divide(X3,X3)) = divide(inverse(divide(X4,X4)),divide(X2,X1)),
inference(step,[status(thm)],[t8573,t6]) ).
cnf(t11102,plain,
multiply(divide(X1,X2),divide(X3,X3)) = divide(X1,X2),
inference(step,[status(thm)],[t11101,t8556]) ).
cnf(t8622,plain,
multiply(divide(X1,X2),divide(X3,X3)) = divide(X1,X2),
inference(orient,[status(thm)],[t11102]) ).
cnf(t8624,plain,
divide(inverse(divide(divide(X1,X2),multiply(X3,divide(multiply(X4,Y4),multiply(divide(X2,X1),Y4))))),X4) = multiply(X3,divide(Y5,Y5)),
inference(cp,[status(thm)],[t8622,t8367]) ).
cnf(t11103,plain,
X3 = multiply(X3,divide(Y5,Y5)),
inference(step,[status(thm)],[t8624,t8367]) ).
cnf(t8714,plain,
multiply(X1,divide(X2,X2)) = X1,
inference(orient,[status(thm)],[t11103]) ).
cnf(t8800,plain,
X1 = divide(inverse(divide(divide(X2,X3),X1)),divide(X3,X2)),
inference(cp,[status(thm)],[t8367,t8714]) ).
cnf(t10209,plain,
divide(inverse(divide(divide(X1,X2),X3)),divide(X2,X1)) = X3,
inference(orient,[status(thm)],[t8800]) ).
cnf(t3626,plain,
X1 = inverse(divide(multiply(divide(inverse(X2),X3),X4),multiply(divide(X1,multiply(X3,X2)),X4))),
inference(cp,[status(thm)],[t3574,t6]) ).
cnf(t4001,plain,
inverse(divide(multiply(divide(inverse(X1),X2),X3),multiply(divide(X4,multiply(X2,X1)),X3))) = X4,
inference(orient,[status(thm)],[t3626]) ).
cnf(t4060,plain,
inverse(divide(multiply(X1,X2),multiply(X3,X2))) = inverse(divide(multiply(divide(inverse(divide(divide(divide(inverse(X4),Y4),Y5),divide(X1,Y5))),multiply(Y4,X4)),Y6),multiply(X3,Y6))),
inference(cp,[status(thm)],[t4001,t1330]) ).
cnf(t11088,plain,
inverse(divide(multiply(X1,X2),multiply(X3,X2))) = inverse(divide(multiply(divide(inverse(divide(multiply(divide(inverse(X4),Y4),c3),multiply(X1,c3))),multiply(Y4,X4)),Y6),multiply(X3,Y6))),
inference(step,[status(thm)],[t4060,t4217]) ).
cnf(t14,plain,
X1 = divide(inverse(divide(multiply(divide(inverse(X2),X3),X4),multiply(X1,X4))),multiply(X3,X2)),
inference(cp,[status(thm)],[t11,t6]) ).
cnf(t71,plain,
divide(inverse(divide(multiply(divide(inverse(X1),X2),X3),multiply(X4,X3))),multiply(X2,X1)) = X4,
inference(orient,[status(thm)],[t14]) ).
cnf(t11089,plain,
inverse(divide(multiply(X1,X2),multiply(X3,X2))) = inverse(divide(multiply(X1,Y6),multiply(X3,Y6))),
inference(step,[status(thm)],[t11088,t71]) ).
cnf(t4336,plain,
inverse(divide(multiply(X1,X2),multiply(X3,X2))) = inverse(divide(multiply(X1,X4),multiply(X3,X4))),
inference(orient,[status(thm)],[t11089]) ).
cnf(t8849,plain,
inverse(divide(multiply(X1,X2),multiply(X3,X2))) = inverse(divide(X1,multiply(X3,divide(X4,X4)))),
inference(cp,[status(thm)],[t4336,t8714]) ).
cnf(t11104,plain,
inverse(divide(multiply(X1,X2),multiply(X3,X2))) = inverse(divide(X1,X3)),
inference(step,[status(thm)],[t8849,t8714]) ).
cnf(t10079,plain,
inverse(divide(multiply(X1,X2),multiply(X3,X2))) = inverse(divide(X1,X3)),
inference(orient,[status(thm)],[t11104]) ).
cnf(t3660,plain,
multiply(X1,divide(multiply(divide(X2,X3),X4),multiply(divide(Y4,divide(X3,X2)),X4))) = divide(X1,Y4),
inference(cp,[status(thm)],[t6,t3574]) ).
cnf(t4360,plain,
multiply(X1,divide(multiply(divide(X2,X3),X4),multiply(divide(Y4,divide(X3,X2)),X4))) = divide(X1,Y4),
inference(orient,[status(thm)],[t3660]) ).
cnf(t10081,plain,
inverse(divide(X1,X2)) = inverse(divide(divide(X1,X3),multiply(X2,divide(multiply(divide(X4,Y4),Y5),multiply(divide(X3,divide(Y4,X4)),Y5))))),
inference(cp,[status(thm)],[t10079,t4360]) ).
cnf(t11132,plain,
inverse(divide(X1,X2)) = inverse(divide(divide(X1,X3),divide(X2,X3))),
inference(step,[status(thm)],[t10081,t4360]) ).
cnf(t10149,plain,
inverse(divide(divide(X1,X2),divide(X3,X2))) = inverse(divide(X1,X3)),
inference(orient,[status(thm)],[t11132]) ).
cnf(t10210,plain,
divide(X1,X2) = divide(inverse(divide(X3,X1)),divide(X2,X3)),
inference(cp,[status(thm)],[t10209,t10149]) ).
cnf(t10250,plain,
divide(inverse(divide(X1,X2)),divide(X3,X1)) = divide(X2,X3),
inference(orient,[status(thm)],[t10210]) ).
cnf(t8558,plain,
divide(X1,X2) = divide(inverse(multiply(inverse(X3),X3)),divide(X2,X1)),
inference(cp,[status(thm)],[t8556,t6]) ).
cnf(t10173,plain,
divide(inverse(multiply(inverse(X1),X1)),divide(X2,X3)) = divide(X3,X2),
inference(orient,[status(thm)],[t8558]) ).
cnf(t10182,plain,
divide(X1,X2) = divide(inverse(inverse(divide(X3,X3))),divide(X2,X1)),
inference(cp,[status(thm)],[t10173,t8714]) ).
cnf(t10199,plain,
divide(inverse(inverse(divide(X1,X1))),divide(X2,X3)) = divide(X3,X2),
inference(orient,[status(thm)],[t10182]) ).
cnf(t10256,plain,
divide(divide(X1,X2),X3) = divide(inverse(divide(X2,X1)),divide(X3,inverse(inverse(divide(X4,X4))))),
inference(cp,[status(thm)],[t10250,t10199]) ).
cnf(t11134,plain,
divide(divide(X1,X2),X3) = divide(inverse(divide(X2,X1)),multiply(X3,inverse(divide(X4,X4)))),
inference(step,[status(thm)],[t10256,t6]) ).
cnf(t8717,plain,
X1 = multiply(X1,multiply(inverse(X2),X2)),
inference(cp,[status(thm)],[t8714,t6]) ).
cnf(t8857,plain,
multiply(X1,multiply(inverse(X2),X2)) = X1,
inference(orient,[status(thm)],[t8717]) ).
cnf(t8859,plain,
X1 = multiply(X1,inverse(divide(X2,X2))),
inference(cp,[status(thm)],[t8857,t8714]) ).
cnf(t9007,plain,
multiply(X1,inverse(divide(X2,X2))) = X1,
inference(orient,[status(thm)],[t8859]) ).
cnf(t11135,plain,
divide(divide(X1,X2),X3) = divide(inverse(divide(X2,X1)),X3),
inference(step,[status(thm)],[t11134,t9007]) ).
cnf(t10354,plain,
divide(inverse(divide(X1,X2)),X3) = divide(divide(X2,X1),X3),
inference(orient,[status(thm)],[t11135]) ).
cnf(t11137,plain,
divide(divide(X2,X1),divide(X3,X1)) = divide(X2,X3),
inference(step,[status(thm)],[t10250,t10354]) ).
cnf(t10393,plain,
divide(divide(X2,X1),divide(X3,X1)) = divide(X2,X3),
inference(rw,[status(thm)],[t11137]) ).
cnf(t10366,plain,
divide(X1,inverse(divide(X2,X3))) = multiply(divide(X4,Y4),divide(multiply(divide(Y4,X4),Y5),multiply(divide(divide(X3,X2),X1),Y5))),
inference(cp,[status(thm)],[t7464,t10354]) ).
cnf(t11142,plain,
multiply(X1,divide(X2,X3)) = multiply(divide(X4,Y4),divide(multiply(divide(Y4,X4),Y5),multiply(divide(divide(X3,X2),X1),Y5))),
inference(step,[status(thm)],[t10366,t6]) ).
cnf(t11143,plain,
multiply(X1,divide(X2,X3)) = divide(X1,divide(X3,X2)),
inference(step,[status(thm)],[t11142,t7464]) ).
cnf(t10398,plain,
divide(X1,divide(X2,X3)) = multiply(X1,divide(X3,X2)),
inference(orient,[status(thm)],[t11143]) ).
cnf(t11166,plain,
multiply(divide(X2,X1),divide(X1,X3)) = divide(X2,X3),
inference(step,[status(thm)],[t10393,t10398]) ).
cnf(t10797,plain,
multiply(divide(X1,X2),divide(X2,X3)) = divide(X1,X3),
inference(orient,[status(thm)],[t11166]) ).
cnf(t10355,plain,
divide(divide(X1,X2),inverse(X3)) = multiply(inverse(divide(X2,X1)),X3),
inference(cp,[status(thm)],[t10354,t6]) ).
cnf(t11155,plain,
multiply(divide(X1,X2),X3) = multiply(inverse(divide(X2,X1)),X3),
inference(step,[status(thm)],[t10355,t6]) ).
cnf(t10427,plain,
multiply(inverse(divide(X1,X2)),X3) = multiply(divide(X2,X1),X3),
inference(orient,[status(thm)],[t11155]) ).
cnf(t8868,plain,
X1 = multiply(X1,inverse(multiply(inverse(X2),X2))),
inference(cp,[status(thm)],[t8857,t8857]) ).
cnf(t9150,plain,
multiply(X1,inverse(multiply(inverse(X2),X2))) = X1,
inference(orient,[status(thm)],[t8868]) ).
cnf(t9011,plain,
X1 = multiply(X1,inverse(inverse(divide(X2,X2)))),
inference(cp,[status(thm)],[t8857,t9007]) ).
cnf(t9303,plain,
multiply(X1,inverse(inverse(divide(X2,X2)))) = X1,
inference(orient,[status(thm)],[t9011]) ).
cnf(t9310,plain,
X1 = multiply(X1,inverse(inverse(inverse(inverse(divide(X2,X2)))))),
inference(cp,[status(thm)],[t9150,t9303]) ).
cnf(t9906,plain,
multiply(X1,inverse(inverse(inverse(inverse(divide(X2,X2)))))) = X1,
inference(orient,[status(thm)],[t9310]) ).
cnf(t10428,plain,
multiply(divide(X1,X2),inverse(inverse(inverse(inverse(divide(X3,X3)))))) = inverse(divide(X2,X1)),
inference(cp,[status(thm)],[t10427,t9906]) ).
cnf(t11156,plain,
divide(X1,X2) = inverse(divide(X2,X1)),
inference(step,[status(thm)],[t10428,t9906]) ).
cnf(t10459,plain,
inverse(divide(X1,X2)) = divide(X2,X1),
inference(orient,[status(thm)],[t11156]) ).
cnf(t10462,plain,
divide(inverse(X1),X2) = inverse(multiply(X2,X1)),
inference(cp,[status(thm)],[t10459,t6]) ).
cnf(t10479,plain,
inverse(multiply(X1,X2)) = divide(inverse(X2),X1),
inference(orient,[status(thm)],[t10462]) ).
cnf(t10481,plain,
divide(inverse(divide(X1,X1)),X2) = inverse(X2),
inference(cp,[status(thm)],[t10479,t8714]) ).
cnf(t11159,plain,
divide(divide(X1,X1),X2) = inverse(X2),
inference(step,[status(thm)],[t10481,t10354]) ).
cnf(t10504,plain,
divide(divide(X1,X1),X2) = inverse(X2),
inference(orient,[status(thm)],[t11159]) ).
cnf(t10805,plain,
divide(divide(X1,X1),X2) = multiply(inverse(X3),divide(X3,X2)),
inference(cp,[status(thm)],[t10797,t10504]) ).
cnf(t11167,plain,
inverse(X2) = multiply(inverse(X3),divide(X3,X2)),
inference(step,[status(thm)],[t10805,t10504]) ).
cnf(t10825,plain,
multiply(inverse(X1),divide(X1,X2)) = inverse(X2),
inference(orient,[status(thm)],[t11167]) ).
cnf(t10837,plain,
divide(inverse(divide(X1,X2)),inverse(X1)) = inverse(inverse(X2)),
inference(cp,[status(thm)],[t10479,t10825]) ).
cnf(t11168,plain,
divide(divide(X2,X1),inverse(X1)) = inverse(inverse(X2)),
inference(step,[status(thm)],[t10837,t10354]) ).
cnf(t11169,plain,
multiply(divide(X2,X1),X1) = inverse(inverse(X2)),
inference(step,[status(thm)],[t11168,t6]) ).
cnf(t10511,plain,
divide(X1,divide(X2,X2)) = inverse(inverse(X1)),
inference(cp,[status(thm)],[t10459,t10504]) ).
cnf(t11160,plain,
multiply(X1,divide(X2,X2)) = inverse(inverse(X1)),
inference(step,[status(thm)],[t10511,t10398]) ).
cnf(t11161,plain,
X1 = inverse(inverse(X1)),
inference(step,[status(thm)],[t11160,t8714]) ).
cnf(t10520,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t11161]) ).
cnf(t11170,plain,
multiply(divide(X2,X1),X1) = X2,
inference(step,[status(thm)],[t11169,t10520]) ).
cnf(t10855,plain,
multiply(divide(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t11170]) ).
cnf(t10521,plain,
multiply(X1,inverse(X2)) = divide(X1,X2),
inference(cp,[status(thm)],[t6,t10520]) ).
cnf(t10534,plain,
multiply(X1,inverse(X2)) = divide(X1,X2),
inference(orient,[status(thm)],[t10521]) ).
cnf(t10857,plain,
X1 = divide(divide(X1,inverse(X2)),X2),
inference(cp,[status(thm)],[t10855,t10534]) ).
cnf(t11171,plain,
X1 = divide(multiply(X1,X2),X2),
inference(step,[status(thm)],[t10857,t6]) ).
cnf(t10888,plain,
divide(multiply(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t11171]) ).
cnf(t10895,plain,
divide(multiply(X1,X2),X3) = multiply(X1,divide(X2,X3)),
inference(cp,[status(thm)],[t10797,t10888]) ).
cnf(t11017,plain,
divide(multiply(X1,X2),X3) = multiply(X1,divide(X2,X3)),
inference(orient,[status(thm)],[t10895]) ).
cnf(t11020,plain,
multiply(X1,divide(X2,inverse(X3))) = multiply(multiply(X1,X2),X3),
inference(cp,[status(thm)],[t11017,t6]) ).
cnf(t11213,plain,
multiply(X1,multiply(X2,X3)) = multiply(multiply(X1,X2),X3),
inference(step,[status(thm)],[t11020,t6]) ).
cnf(t11055,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t11213]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)),
inference(rw,[status(thm)],[goal_0,t11055]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP477-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n002.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 14:54:18 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 4.12/1.03 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.12/1.03 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------