%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP474-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 : n017.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:07 PM UTC 2026
% Result : Unsatisfiable 19.14s 2.83s
% Output : CNFRefutation 19.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 100
% Number of leaves : 3
% Syntax : Number of clauses : 201 ( 201 unt; 0 nHn; 3 RR)
% Number of literals : 201 ( 200 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 : 971 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t1,axiom,
divide(divide(inverse(divide(X1,X2)),divide(divide(X3,X4),X1)),divide(X4,X3)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t2,plain,
divide(divide(inverse(divide(X1,X2)),divide(divide(X3,X4),X1)),divide(X4,X3)) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(t0,axiom,
divide(X1,inverse(X2)) = multiply(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t7,plain,
divide(X1,inverse(X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t0]) ).
cnf(t8,plain,
inverse(X1) = divide(divide(inverse(multiply(X2,X1)),divide(divide(X3,X4),X2)),divide(X4,X3)),
inference(cp,[status(thm)],[t2,t7]) ).
cnf(t12,plain,
divide(divide(inverse(multiply(X1,X2)),divide(divide(X3,X4),X1)),divide(X4,X3)) = inverse(X2),
inference(orient,[status(thm)],[t8]) ).
cnf(t15,plain,
inverse(X1) = divide(divide(inverse(multiply(X2,X1)),divide(multiply(X3,X4),X2)),divide(inverse(X4),X3)),
inference(cp,[status(thm)],[t12,t7]) ).
cnf(t111,plain,
divide(divide(inverse(multiply(X1,X2)),divide(multiply(X3,X4),X1)),divide(inverse(X4),X3)) = inverse(X2),
inference(orient,[status(thm)],[t15]) ).
cnf(t119,plain,
inverse(X1) = divide(divide(inverse(multiply(divide(inverse(X2),X3),X1)),inverse(X4)),divide(divide(multiply(X3,X2),Y4),inverse(multiply(Y4,X4)))),
inference(cp,[status(thm)],[t12,t111]) ).
cnf(t46824,plain,
inverse(X1) = divide(multiply(inverse(multiply(divide(inverse(X2),X3),X1)),X4),divide(divide(multiply(X3,X2),Y4),inverse(multiply(Y4,X4)))),
inference(step,[status(thm)],[t119,t7]) ).
cnf(t46825,plain,
inverse(X1) = divide(multiply(inverse(multiply(divide(inverse(X2),X3),X1)),X4),multiply(divide(multiply(X3,X2),Y4),multiply(Y4,X4))),
inference(step,[status(thm)],[t46824,t7]) ).
cnf(t1601,plain,
divide(multiply(inverse(multiply(divide(inverse(X1),X2),X3)),X4),multiply(divide(multiply(X2,X1),Y4),multiply(Y4,X4))) = inverse(X3),
inference(orient,[status(thm)],[t46825]) ).
cnf(t20,plain,
X1 = divide(divide(inverse(divide(divide(X2,X3),X1)),inverse(X4)),divide(divide(divide(X3,X2),Y4),inverse(multiply(Y4,X4)))),
inference(cp,[status(thm)],[t2,t12]) ).
cnf(t46805,plain,
X1 = divide(multiply(inverse(divide(divide(X2,X3),X1)),X4),divide(divide(divide(X3,X2),Y4),inverse(multiply(Y4,X4)))),
inference(step,[status(thm)],[t20,t7]) ).
cnf(t46806,plain,
X1 = divide(multiply(inverse(divide(divide(X2,X3),X1)),X4),multiply(divide(divide(X3,X2),Y4),multiply(Y4,X4))),
inference(step,[status(thm)],[t46805,t7]) ).
cnf(t307,plain,
divide(multiply(inverse(divide(divide(X1,X2),X3)),X4),multiply(divide(divide(X2,X1),Y4),multiply(Y4,X4))) = X3,
inference(orient,[status(thm)],[t46806]) ).
cnf(t308,plain,
divide(X1,X2) = divide(multiply(inverse(X3),X4),multiply(divide(divide(divide(divide(X2,X1),Y4),inverse(divide(Y4,X3))),Y5),multiply(Y5,X4))),
inference(cp,[status(thm)],[t307,t2]) ).
cnf(t46846,plain,
divide(X1,X2) = divide(multiply(inverse(X3),X4),multiply(divide(multiply(divide(divide(X2,X1),Y4),divide(Y4,X3)),Y5),multiply(Y5,X4))),
inference(step,[status(thm)],[t308,t7]) ).
cnf(t2603,plain,
divide(multiply(inverse(X1),X2),multiply(divide(multiply(divide(divide(X3,X4),Y4),divide(Y4,X1)),Y5),multiply(Y5,X2))) = divide(X4,X3),
inference(orient,[status(thm)],[t46846]) ).
cnf(t2768,plain,
divide(multiply(divide(multiply(divide(divide(X1,X2),X3),divide(X3,X4)),Y4),multiply(Y4,Y5)),multiply(inverse(X4),Y5)) = divide(multiply(inverse(Y6),Y7),multiply(divide(multiply(divide(divide(X2,X1),Y8),divide(Y8,Y6)),Y9),multiply(Y9,Y7))),
inference(cp,[status(thm)],[t2603,t2603]) ).
cnf(t46848,plain,
divide(multiply(divide(multiply(divide(divide(X1,X2),X3),divide(X3,X4)),Y4),multiply(Y4,Y5)),multiply(inverse(X4),Y5)) = divide(X1,X2),
inference(step,[status(thm)],[t2768,t2603]) ).
cnf(t3015,plain,
divide(multiply(divide(multiply(divide(divide(X1,X2),X3),divide(X3,X4)),Y4),multiply(Y4,Y5)),multiply(inverse(X4),Y5)) = divide(X1,X2),
inference(orient,[status(thm)],[t46848]) ).
cnf(t113,plain,
inverse(X1) = divide(divide(inverse(multiply(X2,X1)),divide(multiply(inverse(X3),X4),X2)),multiply(inverse(X4),X3)),
inference(cp,[status(thm)],[t111,t7]) ).
cnf(t254,plain,
divide(divide(inverse(multiply(X1,X2)),divide(multiply(inverse(X3),X4),X1)),multiply(inverse(X4),X3)) = inverse(X2),
inference(orient,[status(thm)],[t113]) ).
cnf(t257,plain,
X1 = divide(divide(inverse(divide(multiply(inverse(X2),X3),X1)),inverse(X4)),divide(divide(multiply(inverse(X3),X2),Y4),inverse(multiply(Y4,X4)))),
inference(cp,[status(thm)],[t2,t254]) ).
cnf(t46835,plain,
X1 = divide(multiply(inverse(divide(multiply(inverse(X2),X3),X1)),X4),divide(divide(multiply(inverse(X3),X2),Y4),inverse(multiply(Y4,X4)))),
inference(step,[status(thm)],[t257,t7]) ).
cnf(t46836,plain,
X1 = divide(multiply(inverse(divide(multiply(inverse(X2),X3),X1)),X4),multiply(divide(multiply(inverse(X3),X2),Y4),multiply(Y4,X4))),
inference(step,[status(thm)],[t46835,t7]) ).
cnf(t2121,plain,
divide(multiply(inverse(divide(multiply(inverse(X1),X2),X3)),X4),multiply(divide(multiply(inverse(X2),X1),Y4),multiply(Y4,X4))) = X3,
inference(orient,[status(thm)],[t46836]) ).
cnf(t3052,plain,
divide(multiply(inverse(divide(multiply(inverse(X1),X2),X3)),X4),multiply(divide(multiply(inverse(X2),X1),Y4),multiply(Y4,X4))) = divide(multiply(divide(multiply(divide(X3,Y5),divide(Y5,Y6)),Y7),multiply(Y7,Y8)),multiply(inverse(Y6),Y8)),
inference(cp,[status(thm)],[t3015,t2121]) ).
cnf(t46849,plain,
X3 = divide(multiply(divide(multiply(divide(X3,Y5),divide(Y5,Y6)),Y7),multiply(Y7,Y8)),multiply(inverse(Y6),Y8)),
inference(step,[status(thm)],[t3052,t2121]) ).
cnf(t3167,plain,
divide(multiply(divide(multiply(divide(X1,X2),divide(X2,X3)),X4),multiply(X4,Y4)),multiply(inverse(X3),Y4)) = X1,
inference(orient,[status(thm)],[t46849]) ).
cnf(t3216,plain,
X1 = divide(multiply(divide(multiply(divide(X1,X2),multiply(X2,X3)),X4),multiply(X4,Y4)),multiply(inverse(inverse(X3)),Y4)),
inference(cp,[status(thm)],[t3167,t7]) ).
cnf(t3833,plain,
divide(multiply(divide(multiply(divide(X1,X2),multiply(X2,X3)),X4),multiply(X4,Y4)),multiply(inverse(inverse(X3)),Y4)) = X1,
inference(orient,[status(thm)],[t3216]) ).
cnf(t3834,plain,
multiply(divide(X1,X2),divide(X2,X3)) = divide(multiply(X1,multiply(multiply(inverse(X3),X4),Y4)),multiply(inverse(inverse(X4)),Y4)),
inference(cp,[status(thm)],[t3833,t3167]) ).
cnf(t4193,plain,
multiply(divide(X1,X2),divide(X2,X3)) = divide(multiply(X1,multiply(multiply(inverse(X3),X4),Y4)),multiply(inverse(inverse(X4)),Y4)),
inference(orient,[status(thm)],[t3834]) ).
cnf(t4384,plain,
multiply(divide(divide(multiply(divide(X1,X2),divide(X2,inverse(X3))),multiply(inverse(X4),X3)),Y4),divide(Y4,X4)) = X1,
inference(cp,[status(thm)],[t4193,t3167]) ).
cnf(t46851,plain,
multiply(divide(divide(multiply(divide(X1,X2),multiply(X2,X3)),multiply(inverse(X4),X3)),Y4),divide(Y4,X4)) = X1,
inference(step,[status(thm)],[t4384,t7]) ).
cnf(t5170,plain,
multiply(divide(divide(multiply(divide(X1,X2),multiply(X2,X3)),multiply(inverse(X4),X3)),Y4),divide(Y4,X4)) = X1,
inference(orient,[status(thm)],[t46851]) ).
cnf(t5176,plain,
X1 = multiply(divide(multiply(divide(divide(X1,multiply(inverse(X2),X3)),X4),divide(X4,X2)),Y4),divide(Y4,inverse(X3))),
inference(cp,[status(thm)],[t5170,t4193]) ).
cnf(t46852,plain,
X1 = multiply(divide(multiply(divide(divide(X1,multiply(inverse(X2),X3)),X4),divide(X4,X2)),Y4),multiply(Y4,X3)),
inference(step,[status(thm)],[t5176,t7]) ).
cnf(t5309,plain,
multiply(divide(multiply(divide(divide(X1,multiply(inverse(X2),X3)),X4),divide(X4,X2)),Y4),multiply(Y4,X3)) = X1,
inference(orient,[status(thm)],[t46852]) ).
cnf(t5417,plain,
inverse(X1) = divide(multiply(inverse(multiply(divide(inverse(divide(X2,X3)),divide(divide(X4,multiply(inverse(X3),Y4)),X2)),X1)),Y4),X4),
inference(cp,[status(thm)],[t1601,t5309]) ).
cnf(t11009,plain,
divide(multiply(inverse(multiply(divide(inverse(divide(X1,X2)),divide(divide(X3,multiply(inverse(X2),X4)),X1)),Y4)),X4),X3) = inverse(Y4),
inference(orient,[status(thm)],[t5417]) ).
cnf(t3,plain,
divide(X1,X2) = divide(divide(inverse(X3),divide(divide(X4,Y4),divide(inverse(divide(Y5,X3)),divide(divide(X2,X1),Y5)))),divide(Y4,X4)),
inference(cp,[status(thm)],[t2,t2]) ).
cnf(t3526,plain,
divide(divide(inverse(X1),divide(divide(X2,X3),divide(inverse(divide(X4,X1)),divide(divide(Y4,Y5),X4)))),divide(X3,X2)) = divide(Y5,Y4),
inference(orient,[status(thm)],[t3]) ).
cnf(t17,plain,
inverse(X1) = divide(divide(inverse(multiply(X2,X1)),divide(divide(inverse(X3),X4),X2)),multiply(X4,X3)),
inference(cp,[status(thm)],[t12,t7]) ).
cnf(t128,plain,
divide(divide(inverse(multiply(X1,X2)),divide(divide(inverse(X3),X4),X1)),multiply(X4,X3)) = inverse(X2),
inference(orient,[status(thm)],[t17]) ).
cnf(t139,plain,
X1 = divide(divide(inverse(divide(multiply(X2,X3),X1)),inverse(X4)),divide(divide(divide(inverse(X3),X2),Y4),inverse(multiply(Y4,X4)))),
inference(cp,[status(thm)],[t2,t128]) ).
cnf(t46817,plain,
X1 = divide(multiply(inverse(divide(multiply(X2,X3),X1)),X4),divide(divide(divide(inverse(X3),X2),Y4),inverse(multiply(Y4,X4)))),
inference(step,[status(thm)],[t139,t7]) ).
cnf(t46818,plain,
X1 = divide(multiply(inverse(divide(multiply(X2,X3),X1)),X4),multiply(divide(divide(inverse(X3),X2),Y4),multiply(Y4,X4))),
inference(step,[status(thm)],[t46817,t7]) ).
cnf(t1140,plain,
divide(multiply(inverse(divide(multiply(X1,X2),X3)),X4),multiply(divide(divide(inverse(X2),X1),Y4),multiply(Y4,X4))) = X3,
inference(orient,[status(thm)],[t46818]) ).
cnf(t11,plain,
X1 = divide(divide(inverse(divide(X2,X1)),divide(divide(inverse(X3),X4),X2)),multiply(X4,X3)),
inference(cp,[status(thm)],[t2,t7]) ).
cnf(t60,plain,
divide(divide(inverse(divide(X1,X2)),divide(divide(inverse(X3),X4),X1)),multiply(X4,X3)) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(t66,plain,
X1 = divide(divide(inverse(divide(divide(X2,X3),X1)),X4),multiply(divide(divide(X3,X2),Y4),divide(Y4,X4))),
inference(cp,[status(thm)],[t60,t2]) ).
cnf(t394,plain,
divide(divide(inverse(divide(divide(X1,X2),X3)),X4),multiply(divide(divide(X2,X1),Y4),divide(Y4,X4))) = X3,
inference(orient,[status(thm)],[t66]) ).
cnf(t395,plain,
divide(X1,X2) = divide(divide(inverse(X3),X4),multiply(divide(divide(divide(divide(X2,X1),Y4),inverse(divide(Y4,X3))),Y5),divide(Y5,X4))),
inference(cp,[status(thm)],[t394,t2]) ).
cnf(t46847,plain,
divide(X1,X2) = divide(divide(inverse(X3),X4),multiply(divide(multiply(divide(divide(X2,X1),Y4),divide(Y4,X3)),Y5),divide(Y5,X4))),
inference(step,[status(thm)],[t395,t7]) ).
cnf(t2782,plain,
divide(divide(inverse(X1),X2),multiply(divide(multiply(divide(divide(X3,X4),Y4),divide(Y4,X1)),Y5),divide(Y5,X2))) = divide(X4,X3),
inference(orient,[status(thm)],[t46847]) ).
cnf(t3003,plain,
divide(multiply(divide(multiply(divide(divide(X1,X2),X3),divide(X3,X4)),Y4),divide(Y4,Y5)),divide(inverse(X4),Y5)) = divide(divide(inverse(Y6),Y7),multiply(divide(multiply(divide(divide(X2,X1),Y8),divide(Y8,Y6)),Y9),divide(Y9,Y7))),
inference(cp,[status(thm)],[t2782,t2782]) ).
cnf(t46853,plain,
divide(multiply(divide(multiply(divide(divide(X1,X2),X3),divide(X3,X4)),Y4),divide(Y4,Y5)),divide(inverse(X4),Y5)) = divide(X1,X2),
inference(step,[status(thm)],[t3003,t2782]) ).
cnf(t14082,plain,
divide(multiply(divide(multiply(divide(divide(X1,X2),X3),divide(X3,X4)),Y4),divide(Y4,Y5)),divide(inverse(X4),Y5)) = divide(X1,X2),
inference(orient,[status(thm)],[t46853]) ).
cnf(t5,plain,
X1 = divide(divide(inverse(divide(X2,X1)),divide(X3,X2)),divide(divide(X4,Y4),divide(inverse(divide(Y5,X3)),divide(divide(Y4,X4),Y5)))),
inference(cp,[status(thm)],[t2,t2]) ).
cnf(t12818,plain,
divide(divide(inverse(divide(X1,X2)),divide(X3,X1)),divide(divide(X4,Y4),divide(inverse(divide(Y5,X3)),divide(divide(Y4,X4),Y5)))) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t14138,plain,
divide(divide(inverse(divide(X1,X2)),divide(X3,X1)),divide(divide(X4,Y4),divide(inverse(divide(Y5,X3)),divide(divide(Y4,X4),Y5)))) = divide(multiply(divide(multiply(divide(X2,Y6),divide(Y6,Y7)),Y8),divide(Y8,Y9)),divide(inverse(Y7),Y9)),
inference(cp,[status(thm)],[t14082,t12818]) ).
cnf(t46854,plain,
X2 = divide(multiply(divide(multiply(divide(X2,Y6),divide(Y6,Y7)),Y8),divide(Y8,Y9)),divide(inverse(Y7),Y9)),
inference(step,[status(thm)],[t14138,t12818]) ).
cnf(t14397,plain,
divide(multiply(divide(multiply(divide(X1,X2),divide(X2,X3)),X4),divide(X4,Y4)),divide(inverse(X3),Y4)) = X1,
inference(orient,[status(thm)],[t46854]) ).
cnf(t14630,plain,
divide(inverse(X1),X2) = divide(multiply(inverse(X3),X4),multiply(divide(divide(inverse(divide(Y4,X2)),divide(multiply(divide(X3,Y5),divide(Y5,X1)),Y4)),Y6),multiply(Y6,X4))),
inference(cp,[status(thm)],[t1140,t14397]) ).
cnf(t4460,plain,
multiply(divide(X1,X2),divide(X2,X3)) = multiply(divide(X1,X4),divide(X4,X3)),
inference(cp,[status(thm)],[t4193,t4193]) ).
cnf(t4461,plain,
multiply(divide(X1,X2),divide(X2,X3)) = multiply(divide(X1,X4),divide(X4,X3)),
inference(orient,[status(thm)],[t4460]) ).
cnf(t4519,plain,
multiply(divide(X1,X2),divide(X2,inverse(X3))) = multiply(divide(X1,X4),multiply(X4,X3)),
inference(cp,[status(thm)],[t4461,t7]) ).
cnf(t46850,plain,
multiply(divide(X1,X2),multiply(X2,X3)) = multiply(divide(X1,X4),multiply(X4,X3)),
inference(step,[status(thm)],[t4519,t7]) ).
cnf(t4642,plain,
multiply(divide(X1,X2),multiply(X2,X3)) = multiply(divide(X1,X4),multiply(X4,X3)),
inference(orient,[status(thm)],[t46850]) ).
cnf(t10,plain,
X1 = divide(divide(inverse(divide(X2,X1)),divide(multiply(X3,X4),X2)),divide(inverse(X4),X3)),
inference(cp,[status(thm)],[t2,t7]) ).
cnf(t43,plain,
divide(divide(inverse(divide(X1,X2)),divide(multiply(X3,X4),X1)),divide(inverse(X4),X3)) = X2,
inference(orient,[status(thm)],[t10]) ).
cnf(t4684,plain,
multiply(divide(divide(inverse(divide(X1,X2)),divide(multiply(X3,X4),X1)),Y4),multiply(Y4,Y5)) = multiply(X2,multiply(divide(inverse(X4),X3),Y5)),
inference(cp,[status(thm)],[t4642,t43]) ).
cnf(t6997,plain,
multiply(divide(divide(inverse(divide(X1,X2)),divide(multiply(X3,X4),X1)),Y4),multiply(Y4,Y5)) = multiply(X2,multiply(divide(inverse(X4),X3),Y5)),
inference(orient,[status(thm)],[t4684]) ).
cnf(t46855,plain,
divide(inverse(X1),X2) = divide(multiply(inverse(X3),X4),multiply(X2,multiply(divide(inverse(divide(Y5,X1)),divide(X3,Y5)),X4))),
inference(step,[status(thm)],[t14630,t6997]) ).
cnf(t14714,plain,
divide(multiply(inverse(X1),X2),multiply(X3,multiply(divide(inverse(divide(X4,Y4)),divide(X1,X4)),X2))) = divide(inverse(Y4),X3),
inference(orient,[status(thm)],[t46855]) ).
cnf(t14963,plain,
divide(multiply(X1,multiply(divide(inverse(divide(X2,X3)),divide(X4,X2)),Y4)),multiply(inverse(X4),Y4)) = divide(divide(inverse(Y5),divide(divide(Y6,Y7),divide(inverse(divide(Y8,Y5)),divide(divide(inverse(X3),X1),Y8)))),divide(Y7,Y6)),
inference(cp,[status(thm)],[t3526,t14714]) ).
cnf(t46856,plain,
divide(multiply(X1,multiply(divide(inverse(divide(X2,X3)),divide(X4,X2)),Y4)),multiply(inverse(X4),Y4)) = divide(X1,inverse(X3)),
inference(step,[status(thm)],[t14963,t3526]) ).
cnf(t46857,plain,
divide(multiply(X1,multiply(divide(inverse(divide(X2,X3)),divide(X4,X2)),Y4)),multiply(inverse(X4),Y4)) = multiply(X1,X3),
inference(step,[status(thm)],[t46856,t7]) ).
cnf(t15015,plain,
divide(multiply(X1,multiply(divide(inverse(divide(X2,X3)),divide(X4,X2)),Y4)),multiply(inverse(X4),Y4)) = multiply(X1,X3),
inference(orient,[status(thm)],[t46857]) ).
cnf(t11013,plain,
inverse(divide(divide(divide(X1,multiply(inverse(X2),X3)),X4),Y4)) = divide(multiply(inverse(multiply(divide(inverse(divide(X4,X2)),Y5),divide(Y5,Y4))),X3),X1),
inference(cp,[status(thm)],[t11009,t4461]) ).
cnf(t11222,plain,
divide(multiply(inverse(multiply(divide(inverse(divide(X1,X2)),X3),divide(X3,X4))),Y4),Y5) = inverse(divide(divide(divide(Y5,multiply(inverse(X2),Y4)),X1),X4)),
inference(orient,[status(thm)],[t11013]) ).
cnf(t15023,plain,
multiply(inverse(multiply(divide(inverse(divide(X1,X2)),X3),divide(X3,X4))),Y4) = inverse(divide(divide(divide(multiply(inverse(Y5),Y6),multiply(inverse(X2),multiply(divide(inverse(divide(Y7,Y4)),divide(Y5,Y7)),Y6))),X1),X4)),
inference(cp,[status(thm)],[t15015,t11222]) ).
cnf(t46863,plain,
multiply(inverse(multiply(divide(inverse(divide(X1,X2)),X3),divide(X3,X4))),Y4) = inverse(divide(divide(divide(inverse(Y4),inverse(X2)),X1),X4)),
inference(step,[status(thm)],[t15023,t14714]) ).
cnf(t46864,plain,
multiply(inverse(multiply(divide(inverse(divide(X1,X2)),X3),divide(X3,X4))),Y4) = inverse(divide(divide(multiply(inverse(Y4),X2),X1),X4)),
inference(step,[status(thm)],[t46863,t7]) ).
cnf(t16759,plain,
multiply(inverse(multiply(divide(inverse(divide(X1,X2)),X3),divide(X3,X4))),Y4) = inverse(divide(divide(multiply(inverse(Y4),X2),X1),X4)),
inference(orient,[status(thm)],[t46864]) ).
cnf(t17016,plain,
inverse(divide(divide(divide(X1,multiply(inverse(X2),X3)),X4),Y4)) = divide(inverse(divide(divide(multiply(inverse(X3),X2),X4),Y4)),X1),
inference(cp,[status(thm)],[t11009,t16759]) ).
cnf(t17028,plain,
inverse(divide(divide(divide(X1,multiply(inverse(X2),X3)),X4),Y4)) = divide(inverse(divide(divide(multiply(inverse(X3),X2),X4),Y4)),X1),
inference(orient,[status(thm)],[t17016]) ).
cnf(t17045,plain,
divide(inverse(divide(divide(multiply(inverse(X1),X2),inverse(X3)),X4)),Y4) = inverse(divide(multiply(divide(Y4,multiply(inverse(X2),X1)),X3),X4)),
inference(cp,[status(thm)],[t17028,t7]) ).
cnf(t46886,plain,
divide(inverse(divide(multiply(multiply(inverse(X1),X2),X3),X4)),Y4) = inverse(divide(multiply(divide(Y4,multiply(inverse(X2),X1)),X3),X4)),
inference(step,[status(thm)],[t17045,t7]) ).
cnf(t17341,plain,
inverse(divide(multiply(divide(X1,multiply(inverse(X2),X3)),X4),Y4)) = divide(inverse(divide(multiply(multiply(inverse(X3),X2),X4),Y4)),X1),
inference(orient,[status(thm)],[t46886]) ).
cnf(t17345,plain,
divide(inverse(divide(multiply(multiply(inverse(X1),X2),multiply(divide(inverse(divide(X3,X4)),divide(Y4,X3)),Y5)),multiply(inverse(Y4),Y5))),Y6) = inverse(multiply(divide(Y6,multiply(inverse(X2),X1)),X4)),
inference(cp,[status(thm)],[t17341,t15015]) ).
cnf(t46887,plain,
divide(inverse(multiply(multiply(inverse(X1),X2),X4)),Y6) = inverse(multiply(divide(Y6,multiply(inverse(X2),X1)),X4)),
inference(step,[status(thm)],[t17345,t15015]) ).
cnf(t17516,plain,
inverse(multiply(divide(X1,multiply(inverse(X2),X3)),X4)) = divide(inverse(multiply(multiply(inverse(X3),X2),X4)),X1),
inference(orient,[status(thm)],[t46887]) ).
cnf(t115,plain,
X1 = divide(divide(inverse(divide(divide(inverse(X2),X3),X1)),inverse(X4)),divide(divide(multiply(X3,X2),Y4),inverse(multiply(Y4,X4)))),
inference(cp,[status(thm)],[t2,t111]) ).
cnf(t46815,plain,
X1 = divide(multiply(inverse(divide(divide(inverse(X2),X3),X1)),X4),divide(divide(multiply(X3,X2),Y4),inverse(multiply(Y4,X4)))),
inference(step,[status(thm)],[t115,t7]) ).
cnf(t46816,plain,
X1 = divide(multiply(inverse(divide(divide(inverse(X2),X3),X1)),X4),multiply(divide(multiply(X3,X2),Y4),multiply(Y4,X4))),
inference(step,[status(thm)],[t46815,t7]) ).
cnf(t1077,plain,
divide(multiply(inverse(divide(divide(inverse(X1),X2),X3)),X4),multiply(divide(multiply(X2,X1),Y4),multiply(Y4,X4))) = X3,
inference(orient,[status(thm)],[t46816]) ).
cnf(t5421,plain,
X1 = divide(multiply(inverse(divide(divide(inverse(divide(X2,X3)),divide(divide(X4,multiply(inverse(X3),Y4)),X2)),X1)),Y4),X4),
inference(cp,[status(thm)],[t1077,t5309]) ).
cnf(t9086,plain,
divide(multiply(inverse(divide(divide(inverse(divide(X1,X2)),divide(divide(X3,multiply(inverse(X2),X4)),X1)),Y4)),X4),X3) = Y4,
inference(orient,[status(thm)],[t5421]) ).
cnf(t9092,plain,
multiply(divide(divide(X1,X2),X3),divide(X3,divide(divide(X4,multiply(inverse(Y4),Y5)),divide(X2,X1)))) = divide(multiply(inverse(Y4),Y5),X4),
inference(cp,[status(thm)],[t9086,t394]) ).
cnf(t10301,plain,
multiply(divide(divide(X1,X2),X3),divide(X3,divide(divide(X4,multiply(inverse(Y4),Y5)),divide(X2,X1)))) = divide(multiply(inverse(Y4),Y5),X4),
inference(orient,[status(thm)],[t9092]) ).
cnf(t15025,plain,
multiply(inverse(divide(divide(inverse(divide(X1,X2)),divide(divide(multiply(inverse(X3),X4),multiply(inverse(X2),multiply(divide(inverse(divide(Y4,Y5)),divide(X3,Y4)),X4))),X1)),Y6)),Y5) = Y6,
inference(cp,[status(thm)],[t15015,t9086]) ).
cnf(t46858,plain,
multiply(inverse(divide(divide(inverse(divide(X1,X2)),divide(divide(inverse(Y5),inverse(X2)),X1)),Y6)),Y5) = Y6,
inference(step,[status(thm)],[t15025,t14714]) ).
cnf(t46859,plain,
multiply(inverse(divide(divide(inverse(divide(X1,X2)),divide(multiply(inverse(Y5),X2),X1)),Y6)),Y5) = Y6,
inference(step,[status(thm)],[t46858,t7]) ).
cnf(t15291,plain,
multiply(inverse(divide(divide(inverse(divide(X1,X2)),divide(multiply(inverse(X3),X2),X1)),X4)),X3) = X4,
inference(orient,[status(thm)],[t46859]) ).
cnf(t15447,plain,
divide(multiply(inverse(divide(divide(inverse(divide(X1,X2)),divide(multiply(inverse(X3),X2),X1)),X4)),X3),Y4) = multiply(divide(divide(Y5,Y6),Y7),divide(Y7,divide(divide(Y4,X4),divide(Y6,Y5)))),
inference(cp,[status(thm)],[t10301,t15291]) ).
cnf(t46860,plain,
divide(X4,Y4) = multiply(divide(divide(Y5,Y6),Y7),divide(Y7,divide(divide(Y4,X4),divide(Y6,Y5)))),
inference(step,[status(thm)],[t15447,t15291]) ).
cnf(t15516,plain,
multiply(divide(divide(X1,X2),X3),divide(X3,divide(divide(X4,Y4),divide(X2,X1)))) = divide(Y4,X4),
inference(orient,[status(thm)],[t46860]) ).
cnf(t15660,plain,
divide(inverse(X1),X2) = multiply(divide(divide(X3,X4),Y4),divide(Y4,divide(multiply(X2,X1),divide(X4,X3)))),
inference(cp,[status(thm)],[t15516,t7]) ).
cnf(t15873,plain,
multiply(divide(divide(X1,X2),X3),divide(X3,divide(multiply(X4,Y4),divide(X2,X1)))) = divide(inverse(Y4),X4),
inference(orient,[status(thm)],[t15660]) ).
cnf(t16009,plain,
divide(inverse(divide(X1,divide(divide(X2,X3),divide(X4,Y4)))),divide(divide(Y4,X4),X1)) = multiply(divide(divide(Y5,Y6),Y7),divide(Y7,divide(divide(X3,X2),divide(Y6,Y5)))),
inference(cp,[status(thm)],[t15873,t15516]) ).
cnf(t46900,plain,
divide(inverse(divide(X1,divide(divide(X2,X3),divide(X4,Y4)))),divide(divide(Y4,X4),X1)) = divide(X2,X3),
inference(step,[status(thm)],[t16009,t15516]) ).
cnf(t20632,plain,
divide(inverse(divide(X1,divide(divide(X2,X3),divide(X4,Y4)))),divide(divide(Y4,X4),X1)) = divide(X2,X3),
inference(orient,[status(thm)],[t46900]) ).
cnf(t20672,plain,
divide(divide(inverse(divide(X1,X2)),divide(X3,X1)),divide(divide(X4,Y4),divide(inverse(divide(Y5,X3)),divide(divide(Y4,X4),Y5)))) = divide(inverse(divide(Y6,divide(X2,divide(Y7,Y8)))),divide(divide(Y8,Y7),Y6)),
inference(cp,[status(thm)],[t20632,t12818]) ).
cnf(t46901,plain,
X2 = divide(inverse(divide(Y6,divide(X2,divide(Y7,Y8)))),divide(divide(Y8,Y7),Y6)),
inference(step,[status(thm)],[t20672,t12818]) ).
cnf(t20969,plain,
divide(inverse(divide(X1,divide(X2,divide(X3,X4)))),divide(divide(X4,X3),X1)) = X2,
inference(orient,[status(thm)],[t46901]) ).
cnf(t21177,plain,
inverse(divide(X1,divide(X2,divide(X3,X4)))) = divide(inverse(divide(Y4,X2)),divide(divide(X1,divide(X4,X3)),Y4)),
inference(cp,[status(thm)],[t20969,t20969]) ).
cnf(t22145,plain,
divide(inverse(divide(X1,X2)),divide(divide(X3,divide(X4,Y4)),X1)) = inverse(divide(X3,divide(X2,divide(Y4,X4)))),
inference(orient,[status(thm)],[t21177]) ).
cnf(t22146,plain,
inverse(divide(X1,divide(divide(X2,divide(divide(X3,X4),X1)),divide(X4,X3)))) = X2,
inference(cp,[status(thm)],[t22145,t20969]) ).
cnf(t22482,plain,
inverse(divide(X1,divide(divide(X2,divide(divide(X3,X4),X1)),divide(X4,X3)))) = X2,
inference(orient,[status(thm)],[t22146]) ).
cnf(t22658,plain,
multiply(X1,divide(X2,divide(divide(X3,divide(divide(X4,Y4),X2)),divide(Y4,X4)))) = divide(X1,X3),
inference(cp,[status(thm)],[t7,t22482]) ).
cnf(t29537,plain,
multiply(X1,divide(X2,divide(divide(X3,divide(divide(X4,Y4),X2)),divide(Y4,X4)))) = divide(X1,X3),
inference(orient,[status(thm)],[t22658]) ).
cnf(t29745,plain,
divide(inverse(multiply(multiply(inverse(divide(X1,divide(divide(X2,divide(divide(X3,X4),X1)),divide(X4,X3)))),Y4),Y5)),Y6) = inverse(multiply(divide(Y6,divide(inverse(Y4),X2)),Y5)),
inference(cp,[status(thm)],[t17516,t29537]) ).
cnf(t46924,plain,
divide(inverse(multiply(multiply(X2,Y4),Y5)),Y6) = inverse(multiply(divide(Y6,divide(inverse(Y4),X2)),Y5)),
inference(step,[status(thm)],[t29745,t22482]) ).
cnf(t29820,plain,
inverse(multiply(divide(X1,divide(inverse(X2),X3)),X4)) = divide(inverse(multiply(multiply(X3,X2),X4)),X1),
inference(orient,[status(thm)],[t46924]) ).
cnf(t29882,plain,
divide(inverse(multiply(multiply(X1,divide(X2,divide(divide(X3,divide(divide(X4,Y4),X2)),divide(Y4,X4)))),Y5)),Y6) = inverse(multiply(divide(Y6,divide(X3,X1)),Y5)),
inference(cp,[status(thm)],[t29820,t22482]) ).
cnf(t46925,plain,
divide(inverse(multiply(divide(X1,X3),Y5)),Y6) = inverse(multiply(divide(Y6,divide(X3,X1)),Y5)),
inference(step,[status(thm)],[t29882,t29537]) ).
cnf(t29997,plain,
inverse(multiply(divide(X1,divide(X2,X3)),X4)) = divide(inverse(multiply(divide(X3,X2),X4)),X1),
inference(orient,[status(thm)],[t46925]) ).
cnf(t30015,plain,
divide(inverse(multiply(divide(X1,X2),divide(X3,divide(divide(X4,divide(divide(Y4,Y5),X3)),divide(Y5,Y4))))),Y6) = inverse(divide(divide(Y6,divide(X2,X1)),X4)),
inference(cp,[status(thm)],[t29997,t29537]) ).
cnf(t46929,plain,
divide(inverse(divide(divide(X1,X2),X4)),Y6) = inverse(divide(divide(Y6,divide(X2,X1)),X4)),
inference(step,[status(thm)],[t30015,t29537]) ).
cnf(t30217,plain,
inverse(divide(divide(X1,divide(X2,X3)),X4)) = divide(inverse(divide(divide(X3,X2),X4)),X1),
inference(orient,[status(thm)],[t46929]) ).
cnf(t30273,plain,
divide(inverse(divide(divide(inverse(X1),X2),X3)),X4) = inverse(divide(divide(X4,multiply(X2,X1)),X3)),
inference(cp,[status(thm)],[t30217,t7]) ).
cnf(t31243,plain,
divide(inverse(divide(divide(inverse(X1),X2),X3)),X4) = inverse(divide(divide(X4,multiply(X2,X1)),X3)),
inference(orient,[status(thm)],[t30273]) ).
cnf(t31251,plain,
inverse(divide(divide(inverse(X1),multiply(X2,X3)),X4)) = multiply(inverse(divide(divide(inverse(X3),X2),X4)),X1),
inference(cp,[status(thm)],[t31243,t7]) ).
cnf(t32588,plain,
inverse(divide(divide(inverse(X1),multiply(X2,X3)),X4)) = multiply(inverse(divide(divide(inverse(X3),X2),X4)),X1),
inference(orient,[status(thm)],[t31251]) ).
cnf(t21168,plain,
divide(X1,X2) = multiply(divide(divide(X3,X4),inverse(divide(divide(X4,X3),divide(Y4,divide(X1,X2))))),Y4),
inference(cp,[status(thm)],[t15516,t20969]) ).
cnf(t46910,plain,
divide(X1,X2) = multiply(multiply(divide(X3,X4),divide(divide(X4,X3),divide(Y4,divide(X1,X2)))),Y4),
inference(step,[status(thm)],[t21168,t7]) ).
cnf(t25100,plain,
multiply(multiply(divide(X1,X2),divide(divide(X2,X1),divide(X3,divide(X4,Y4)))),X3) = divide(X4,Y4),
inference(orient,[status(thm)],[t46910]) ).
cnf(t25260,plain,
divide(inverse(divide(X1,divide(X2,divide(X3,X4)))),divide(divide(X4,X3),X1)) = multiply(multiply(divide(Y4,Y5),divide(divide(Y5,Y4),divide(Y6,X2))),Y6),
inference(cp,[status(thm)],[t25100,t20969]) ).
cnf(t46911,plain,
X2 = multiply(multiply(divide(Y4,Y5),divide(divide(Y5,Y4),divide(Y6,X2))),Y6),
inference(step,[status(thm)],[t25260,t20969]) ).
cnf(t25395,plain,
multiply(multiply(divide(X1,X2),divide(divide(X2,X1),divide(X3,X4))),X3) = X4,
inference(orient,[status(thm)],[t46911]) ).
cnf(t25463,plain,
X1 = multiply(multiply(divide(divide(multiply(X1,X2),X3),inverse(multiply(X3,X4))),inverse(X4)),inverse(X2)),
inference(cp,[status(thm)],[t25395,t111]) ).
cnf(t46919,plain,
X1 = multiply(multiply(multiply(divide(multiply(X1,X2),X3),multiply(X3,X4)),inverse(X4)),inverse(X2)),
inference(step,[status(thm)],[t25463,t7]) ).
cnf(t27902,plain,
multiply(multiply(multiply(divide(multiply(X1,X2),X3),multiply(X3,X4)),inverse(X4)),inverse(X2)) = X1,
inference(orient,[status(thm)],[t46919]) ).
cnf(t5336,plain,
X1 = multiply(divide(multiply(divide(divide(X1,multiply(inverse(inverse(X2)),X3)),X4),multiply(X4,X2)),Y4),multiply(Y4,X3)),
inference(cp,[status(thm)],[t5309,t7]) ).
cnf(t6512,plain,
multiply(divide(multiply(divide(divide(X1,multiply(inverse(inverse(X2)),X3)),X4),multiply(X4,X2)),Y4),multiply(Y4,X3)) = X1,
inference(orient,[status(thm)],[t5336]) ).
cnf(t27904,plain,
divide(divide(X1,multiply(inverse(inverse(X2)),X3)),X4) = multiply(multiply(X1,inverse(X3)),inverse(multiply(X4,X2))),
inference(cp,[status(thm)],[t27902,t6512]) ).
cnf(t28308,plain,
divide(divide(X1,multiply(inverse(inverse(X2)),X3)),X4) = multiply(multiply(X1,inverse(X3)),inverse(multiply(X4,X2))),
inference(orient,[status(thm)],[t27904]) ).
cnf(t29747,plain,
multiply(multiply(X1,inverse(divide(X2,divide(divide(X3,divide(divide(X4,Y4),X2)),divide(Y4,X4))))),inverse(multiply(Y5,Y6))) = divide(divide(X1,divide(inverse(inverse(Y6)),X3)),Y5),
inference(cp,[status(thm)],[t28308,t29537]) ).
cnf(t46932,plain,
multiply(multiply(X1,X3),inverse(multiply(Y5,Y6))) = divide(divide(X1,divide(inverse(inverse(Y6)),X3)),Y5),
inference(step,[status(thm)],[t29747,t22482]) ).
cnf(t30440,plain,
divide(divide(X1,divide(inverse(inverse(X2)),X3)),X4) = multiply(multiply(X1,X3),inverse(multiply(X4,X2))),
inference(orient,[status(thm)],[t46932]) ).
cnf(t30479,plain,
multiply(multiply(X1,X2),inverse(multiply(X3,divide(X4,divide(divide(Y4,divide(divide(Y5,Y6),X4)),divide(Y6,Y5)))))) = divide(divide(X1,divide(inverse(Y4),X2)),X3),
inference(cp,[status(thm)],[t30440,t22482]) ).
cnf(t46933,plain,
multiply(multiply(X1,X2),inverse(divide(X3,Y4))) = divide(divide(X1,divide(inverse(Y4),X2)),X3),
inference(step,[status(thm)],[t30479,t29537]) ).
cnf(t30703,plain,
divide(divide(X1,divide(inverse(X2),X3)),X4) = multiply(multiply(X1,X3),inverse(divide(X4,X2))),
inference(orient,[status(thm)],[t46933]) ).
cnf(t21240,plain,
multiply(X1,divide(X2,divide(X3,X4))) = divide(multiply(X1,multiply(X2,Y4)),multiply(inverse(divide(X4,X3)),Y4)),
inference(cp,[status(thm)],[t15015,t20969]) ).
cnf(t21313,plain,
divide(multiply(X1,multiply(X2,X3)),multiply(inverse(divide(X4,Y4)),X3)) = multiply(X1,divide(X2,divide(Y4,X4))),
inference(orient,[status(thm)],[t21240]) ).
cnf(t30235,plain,
divide(inverse(divide(divide(X1,divide(X2,X3)),divide(X3,X2))),inverse(divide(X1,X4))) = inverse(X4),
inference(cp,[status(thm)],[t30217,t2]) ).
cnf(t46949,plain,
multiply(inverse(divide(divide(X1,divide(X2,X3)),divide(X3,X2))),divide(X1,X4)) = inverse(X4),
inference(step,[status(thm)],[t30235,t7]) ).
cnf(t46950,plain,
multiply(divide(inverse(divide(divide(X3,X2),divide(X3,X2))),X1),divide(X1,X4)) = inverse(X4),
inference(step,[status(thm)],[t46949,t30217]) ).
cnf(t35939,plain,
multiply(divide(inverse(divide(divide(X1,X2),divide(X1,X2))),X3),divide(X3,X4)) = inverse(X4),
inference(orient,[status(thm)],[t46950]) ).
cnf(t35991,plain,
inverse(X1) = multiply(divide(inverse(divide(X2,divide(inverse(divide(X3,divide(X2,divide(X4,Y4)))),divide(divide(Y4,X4),X3)))),Y5),divide(Y5,X1)),
inference(cp,[status(thm)],[t35939,t20969]) ).
cnf(t46951,plain,
inverse(X1) = multiply(divide(inverse(divide(X2,X2)),Y5),divide(Y5,X1)),
inference(step,[status(thm)],[t35991,t20969]) ).
cnf(t36274,plain,
multiply(divide(inverse(divide(X1,X1)),X2),divide(X2,X3)) = inverse(X3),
inference(orient,[status(thm)],[t46951]) ).
cnf(t36319,plain,
inverse(inverse(X1)) = multiply(divide(inverse(divide(X2,X2)),X3),multiply(X3,X1)),
inference(cp,[status(thm)],[t36274,t7]) ).
cnf(t37166,plain,
multiply(divide(inverse(divide(X1,X1)),X2),multiply(X2,X3)) = inverse(inverse(X3)),
inference(orient,[status(thm)],[t36319]) ).
cnf(t37278,plain,
multiply(divide(inverse(divide(X1,X1)),X2),divide(X2,divide(X3,X4))) = divide(inverse(inverse(Y4)),multiply(inverse(divide(X4,X3)),Y4)),
inference(cp,[status(thm)],[t21313,t37166]) ).
cnf(t46953,plain,
inverse(divide(X3,X4)) = divide(inverse(inverse(Y4)),multiply(inverse(divide(X4,X3)),Y4)),
inference(step,[status(thm)],[t37278,t36274]) ).
cnf(t37524,plain,
divide(inverse(inverse(X1)),multiply(inverse(divide(X2,X3)),X1)) = inverse(divide(X3,X2)),
inference(orient,[status(thm)],[t46953]) ).
cnf(t37534,plain,
inverse(divide(X1,X2)) = divide(inverse(X3),multiply(inverse(divide(X2,X1)),divide(X4,divide(divide(X3,divide(divide(Y4,Y5),X4)),divide(Y5,Y4))))),
inference(cp,[status(thm)],[t37524,t22482]) ).
cnf(t46954,plain,
inverse(divide(X1,X2)) = divide(inverse(X3),divide(inverse(divide(X2,X1)),X3)),
inference(step,[status(thm)],[t37534,t29537]) ).
cnf(t37801,plain,
divide(inverse(X1),divide(inverse(divide(X2,X3)),X1)) = inverse(divide(X3,X2)),
inference(orient,[status(thm)],[t46954]) ).
cnf(t37924,plain,
multiply(multiply(inverse(X1),X1),inverse(divide(X2,divide(X3,X4)))) = divide(inverse(divide(X4,X3)),X2),
inference(cp,[status(thm)],[t30703,t37801]) ).
cnf(t43781,plain,
multiply(multiply(inverse(X1),X1),inverse(divide(X2,divide(X3,X4)))) = divide(inverse(divide(X4,X3)),X2),
inference(orient,[status(thm)],[t37924]) ).
cnf(t43789,plain,
divide(inverse(divide(X1,X2)),X3) = multiply(divide(inverse(divide(X4,divide(divide(Y4,divide(divide(Y5,Y6),X4)),divide(Y6,Y5)))),Y4),inverse(divide(X3,divide(X2,X1)))),
inference(cp,[status(thm)],[t43781,t29537]) ).
cnf(t46967,plain,
divide(inverse(divide(X1,X2)),X3) = multiply(divide(Y4,Y4),inverse(divide(X3,divide(X2,X1)))),
inference(step,[status(thm)],[t43789,t22482]) ).
cnf(t44029,plain,
multiply(divide(X1,X1),inverse(divide(X2,divide(X3,X4)))) = divide(inverse(divide(X4,X3)),X2),
inference(orient,[status(thm)],[t46967]) ).
cnf(t44190,plain,
divide(inverse(inverse(divide(X1,divide(X2,X3)))),divide(X4,X4)) = multiply(divide(divide(Y4,Y5),Y6),divide(Y6,divide(divide(inverse(divide(X3,X2)),X1),divide(Y5,Y4)))),
inference(cp,[status(thm)],[t15873,t44029]) ).
cnf(t46968,plain,
divide(inverse(inverse(divide(X1,divide(X2,X3)))),divide(X4,X4)) = divide(X1,inverse(divide(X3,X2))),
inference(step,[status(thm)],[t44190,t15516]) ).
cnf(t46969,plain,
divide(inverse(inverse(divide(X1,divide(X2,X3)))),divide(X4,X4)) = multiply(X1,divide(X3,X2)),
inference(step,[status(thm)],[t46968,t7]) ).
cnf(t44516,plain,
divide(inverse(inverse(divide(X1,divide(X2,X3)))),divide(X4,X4)) = multiply(X1,divide(X3,X2)),
inference(orient,[status(thm)],[t46969]) ).
cnf(t44517,plain,
multiply(X1,divide(X2,X3)) = inverse(divide(divide(X3,X2),X1)),
inference(cp,[status(thm)],[t44516,t37801]) ).
cnf(t44799,plain,
inverse(divide(divide(X1,X2),X3)) = multiply(X3,divide(X2,X1)),
inference(orient,[status(thm)],[t44517]) ).
cnf(t46975,plain,
multiply(X4,divide(multiply(X2,X3),inverse(X1))) = multiply(inverse(divide(divide(inverse(X3),X2),X4)),X1),
inference(step,[status(thm)],[t32588,t44799]) ).
cnf(t46976,plain,
multiply(X4,multiply(multiply(X2,X3),X1)) = multiply(inverse(divide(divide(inverse(X3),X2),X4)),X1),
inference(step,[status(thm)],[t46975,t7]) ).
cnf(t46977,plain,
multiply(X4,multiply(multiply(X2,X3),X1)) = multiply(multiply(X4,divide(X2,inverse(X3))),X1),
inference(step,[status(thm)],[t46976,t44799]) ).
cnf(t46978,plain,
multiply(X4,multiply(multiply(X2,X3),X1)) = multiply(multiply(X4,multiply(X2,X3)),X1),
inference(step,[status(thm)],[t46977,t7]) ).
cnf(t45026,plain,
multiply(X4,multiply(multiply(X2,X3),X1)) = multiply(multiply(X4,multiply(X2,X3)),X1),
inference(rw,[status(thm)],[t46978]) ).
cnf(t46447,plain,
multiply(multiply(X1,multiply(X2,X3)),X4) = multiply(X1,multiply(multiply(X2,X3),X4)),
inference(orient,[status(thm)],[t45026]) ).
cnf(t25397,plain,
X1 = multiply(multiply(multiply(X2,X3),divide(divide(inverse(X3),X2),divide(X4,X1))),X4),
inference(cp,[status(thm)],[t25395,t7]) ).
cnf(t26173,plain,
multiply(multiply(multiply(X1,X2),divide(divide(inverse(X2),X1),divide(X3,X4))),X3) = X4,
inference(orient,[status(thm)],[t25397]) ).
cnf(t26225,plain,
X1 = multiply(multiply(multiply(inverse(X2),X3),divide(multiply(inverse(X3),X2),divide(X4,X1))),X4),
inference(cp,[status(thm)],[t26173,t7]) ).
cnf(t29154,plain,
multiply(multiply(multiply(inverse(X1),X2),divide(multiply(inverse(X2),X1),divide(X3,X4))),X3) = X4,
inference(orient,[status(thm)],[t26225]) ).
cnf(t46506,plain,
multiply(X1,multiply(multiply(multiply(multiply(inverse(X2),X3),divide(multiply(inverse(X3),X2),divide(X4,Y4))),X4),Y5)) = multiply(multiply(X1,Y4),Y5),
inference(cp,[status(thm)],[t46447,t29154]) ).
cnf(t47051,plain,
multiply(X1,multiply(Y4,Y5)) = multiply(multiply(X1,Y4),Y5),
inference(step,[status(thm)],[t46506,t29154]) ).
cnf(t46656,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t47051]) ).
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,t46656]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP474-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.07/0.35 % Computer : n017.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Wed Sep 23 14:46:29 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 19.14/2.83 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.14/2.83 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------