%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP476-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 : n007.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 7.08s 6.53s
% Output : CNFRefutation 7.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 3
% Syntax : Number of clauses : 130 ( 130 unt; 0 nHn; 3 RR)
% Number of literals : 130 ( 129 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 : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 511 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t1,axiom,
divide(inverse(divide(divide(divide(X1,X2),X3),divide(X4,X3))),divide(X2,X1)) = X4,
file('/export/starexec/sandbox/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/sandbox/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(t10655,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)],[t10655]) ).
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(t10672,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)],[t10672]) ).
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(t10660,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)],[t10660]) ).
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(t10676,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)],[t10676]) ).
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(t10686,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)],[t10686]) ).
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(t10687,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)],[t10687]) ).
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(t10688,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)],[t10688]) ).
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(t10689,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)],[t10689]) ).
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(t10668,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)],[t10668]) ).
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(t10678,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)],[t10678]) ).
cnf(t10690,plain,
divide(X1,X2) = divide(inverse(divide(multiply(X3,b2),multiply(X3,b2))),divide(X2,X1)),
inference(step,[status(thm)],[t8391,t4217]) ).
cnf(t8485,plain,
divide(inverse(divide(multiply(X1,b2),multiply(X1,b2))),divide(X2,X3)) = divide(X3,X2),
inference(orient,[status(thm)],[t10690]) ).
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(t10691,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)],[t10691]) ).
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(t10692,plain,
multiply(divide(X1,X2),divide(X3,X3)) = divide(inverse(divide(X4,X4)),divide(X2,X1)),
inference(step,[status(thm)],[t8573,t6]) ).
cnf(t10693,plain,
multiply(divide(X1,X2),divide(X3,X3)) = divide(X1,X2),
inference(step,[status(thm)],[t10692,t8556]) ).
cnf(t8622,plain,
multiply(divide(X1,X2),divide(X3,X3)) = divide(X1,X2),
inference(orient,[status(thm)],[t10693]) ).
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(t10694,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)],[t10694]) ).
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(t10679,plain,
inverse(divide(multiply(X1,X2),multiply(X3,X2))) = inverse(divide(multiply(divide(inverse(divide(multiply(divide(inverse(X4),Y4),b2),multiply(X1,b2))),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(t10680,plain,
inverse(divide(multiply(X1,X2),multiply(X3,X2))) = inverse(divide(multiply(X1,Y6),multiply(X3,Y6))),
inference(step,[status(thm)],[t10679,t71]) ).
cnf(t4336,plain,
inverse(divide(multiply(X1,X2),multiply(X3,X2))) = inverse(divide(multiply(X1,X4),multiply(X3,X4))),
inference(orient,[status(thm)],[t10680]) ).
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(t10695,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)],[t10695]) ).
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(t10723,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)],[t10723]) ).
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(t10725,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(t10726,plain,
divide(divide(X1,X2),X3) = divide(inverse(divide(X2,X1)),X3),
inference(step,[status(thm)],[t10725,t9007]) ).
cnf(t10354,plain,
divide(inverse(divide(X1,X2)),X3) = divide(divide(X2,X1),X3),
inference(orient,[status(thm)],[t10726]) ).
cnf(t10355,plain,
divide(divide(X1,X2),inverse(X3)) = multiply(inverse(divide(X2,X1)),X3),
inference(cp,[status(thm)],[t10354,t6]) ).
cnf(t10746,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)],[t10746]) ).
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(t10747,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)],[t10747]) ).
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(t10750,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)],[t10750]) ).
cnf(t10507,plain,
inverse(inverse(X1)) = multiply(divide(X2,X2),X1),
inference(cp,[status(thm)],[t10504,t6]) ).
cnf(t10511,plain,
divide(X1,divide(X2,X2)) = inverse(inverse(X1)),
inference(cp,[status(thm)],[t10459,t10504]) ).
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(t10733,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(t10734,plain,
multiply(X1,divide(X2,X3)) = divide(X1,divide(X3,X2)),
inference(step,[status(thm)],[t10733,t7464]) ).
cnf(t10398,plain,
divide(X1,divide(X2,X3)) = multiply(X1,divide(X3,X2)),
inference(orient,[status(thm)],[t10734]) ).
cnf(t10751,plain,
multiply(X1,divide(X2,X2)) = inverse(inverse(X1)),
inference(step,[status(thm)],[t10511,t10398]) ).
cnf(t10752,plain,
X1 = inverse(inverse(X1)),
inference(step,[status(thm)],[t10751,t8714]) ).
cnf(t10520,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t10752]) ).
cnf(t10753,plain,
X1 = multiply(divide(X2,X2),X1),
inference(step,[status(thm)],[t10507,t10520]) ).
cnf(t10560,plain,
multiply(divide(X1,X1),X2) = X2,
inference(orient,[status(thm)],[t10753]) ).
cnf(t10572,plain,
X1 = multiply(multiply(inverse(X2),X2),X1),
inference(cp,[status(thm)],[t10560,t6]) ).
cnf(t10618,plain,
multiply(multiply(inverse(X1),X1),X2) = X2,
inference(orient,[status(thm)],[t10572]) ).
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,t10618]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP476-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/5.38 % Computer : n007.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Wed Sep 23 14:49:41 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 7.08/6.53 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.08/6.53 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------