%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP473-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 : n008.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:57 PM UTC 2026
% Result : Unsatisfiable 16.36s 2.82s
% Output : CNFRefutation 16.36s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% 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(t50121,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(t50122,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)],[t50121,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)],[t50122]) ).
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(t50102,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(t50103,plain,
X1 = divide(multiply(inverse(divide(divide(X2,X3),X1)),X4),multiply(divide(divide(X3,X2),Y4),multiply(Y4,X4))),
inference(step,[status(thm)],[t50102,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)],[t50103]) ).
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(t50143,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)],[t50143]) ).
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(t50145,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)],[t50145]) ).
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(t50132,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(t50133,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)],[t50132,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)],[t50133]) ).
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(t50146,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)],[t50146]) ).
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(t50148,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)],[t50148]) ).
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(t50149,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)],[t50149]) ).
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(t50114,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(t50115,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)],[t50114,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)],[t50115]) ).
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(t50144,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)],[t50144]) ).
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(t50150,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)],[t50150]) ).
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(t50151,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)],[t50151]) ).
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(t50147,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)],[t50147]) ).
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(t50152,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)],[t50152]) ).
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(t50153,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(t50154,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)],[t50153,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)],[t50154]) ).
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(t50160,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(t50161,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)],[t50160,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)],[t50161]) ).
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(t50183,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)],[t50183]) ).
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(t50184,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)],[t50184]) ).
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(t50112,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(t50113,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)],[t50112,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)],[t50113]) ).
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(t50155,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(t50156,plain,
multiply(inverse(divide(divide(inverse(divide(X1,X2)),divide(multiply(inverse(Y5),X2),X1)),Y6)),Y5) = Y6,
inference(step,[status(thm)],[t50155,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)],[t50156]) ).
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(t50157,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)],[t50157]) ).
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(t50197,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)],[t50197]) ).
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(t50198,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)],[t50198]) ).
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(t50221,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)],[t50221]) ).
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(t50222,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)],[t50222]) ).
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(t50226,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)],[t50226]) ).
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(t50207,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)],[t50207]) ).
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(t50208,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)],[t50208]) ).
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(t50216,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)],[t50216]) ).
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(t50229,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)],[t50229]) ).
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(t50230,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)],[t50230]) ).
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(t50246,plain,
multiply(inverse(divide(divide(X1,divide(X2,X3)),divide(X3,X2))),divide(X1,X4)) = inverse(X4),
inference(step,[status(thm)],[t30235,t7]) ).
cnf(t50247,plain,
multiply(divide(inverse(divide(divide(X3,X2),divide(X3,X2))),X1),divide(X1,X4)) = inverse(X4),
inference(step,[status(thm)],[t50246,t30217]) ).
cnf(t35939,plain,
multiply(divide(inverse(divide(divide(X1,X2),divide(X1,X2))),X3),divide(X3,X4)) = inverse(X4),
inference(orient,[status(thm)],[t50247]) ).
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(t50248,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)],[t50248]) ).
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(t50250,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)],[t50250]) ).
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(t50251,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)],[t50251]) ).
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(t50264,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)],[t50264]) ).
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(t50265,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(t50266,plain,
divide(inverse(inverse(divide(X1,divide(X2,X3)))),divide(X4,X4)) = multiply(X1,divide(X3,X2)),
inference(step,[status(thm)],[t50265,t7]) ).
cnf(t44516,plain,
divide(inverse(inverse(divide(X1,divide(X2,X3)))),divide(X4,X4)) = multiply(X1,divide(X3,X2)),
inference(orient,[status(thm)],[t50266]) ).
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(t50272,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(t50273,plain,
multiply(X4,multiply(multiply(X2,X3),X1)) = multiply(inverse(divide(divide(inverse(X3),X2),X4)),X1),
inference(step,[status(thm)],[t50272,t7]) ).
cnf(t50274,plain,
multiply(X4,multiply(multiply(X2,X3),X1)) = multiply(multiply(X4,divide(X2,inverse(X3))),X1),
inference(step,[status(thm)],[t50273,t44799]) ).
cnf(t50275,plain,
multiply(X4,multiply(multiply(X2,X3),X1)) = multiply(multiply(X4,multiply(X2,X3)),X1),
inference(step,[status(thm)],[t50274,t7]) ).
cnf(t45026,plain,
multiply(X4,multiply(multiply(X2,X3),X1)) = multiply(multiply(X4,multiply(X2,X3)),X1),
inference(rw,[status(thm)],[t50275]) ).
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(t50348,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)],[t50348]) ).
cnf(t37858,plain,
inverse(divide(inverse(X1),X2)) = divide(inverse(X3),divide(inverse(multiply(X2,X1)),X3)),
inference(cp,[status(thm)],[t37801,t7]) ).
cnf(t38112,plain,
divide(inverse(X1),divide(inverse(multiply(X2,X3)),X1)) = inverse(divide(inverse(X3),X2)),
inference(orient,[status(thm)],[t37858]) ).
cnf(t46666,plain,
multiply(X1,multiply(X2,divide(X3,divide(divide(X4,divide(divide(Y4,Y5),X3)),divide(Y5,Y4))))) = divide(multiply(X1,X2),X4),
inference(cp,[status(thm)],[t46656,t29537]) ).
cnf(t50395,plain,
multiply(X1,divide(X2,X4)) = divide(multiply(X1,X2),X4),
inference(step,[status(thm)],[t46666,t29537]) ).
cnf(t46805,plain,
divide(multiply(X1,X2),X3) = multiply(X1,divide(X2,X3)),
inference(orient,[status(thm)],[t50395]) ).
cnf(t37199,plain,
inverse(inverse(X1)) = multiply(divide(inverse(multiply(inverse(X2),X2)),X3),multiply(X3,X1)),
inference(cp,[status(thm)],[t37166,t7]) ).
cnf(t39858,plain,
multiply(divide(inverse(multiply(inverse(X1),X1)),X2),multiply(X2,X3)) = inverse(inverse(X3)),
inference(orient,[status(thm)],[t37199]) ).
cnf(t46814,plain,
multiply(divide(inverse(multiply(inverse(X1),X1)),X2),divide(multiply(X2,X3),X4)) = divide(inverse(inverse(X3)),X4),
inference(cp,[status(thm)],[t46805,t39858]) ).
cnf(t50496,plain,
multiply(divide(inverse(multiply(inverse(X1),X1)),X2),multiply(X2,divide(X3,X4))) = divide(inverse(inverse(X3)),X4),
inference(step,[status(thm)],[t46814,t46805]) ).
cnf(t50497,plain,
inverse(inverse(divide(X3,X4))) = divide(inverse(inverse(X3)),X4),
inference(step,[status(thm)],[t50496,t39858]) ).
cnf(t47008,plain,
inverse(inverse(divide(X1,X2))) = divide(inverse(inverse(X1)),X2),
inference(orient,[status(thm)],[t50497]) ).
cnf(t47041,plain,
multiply(X1,inverse(divide(X2,X3))) = divide(X1,divide(inverse(inverse(X2)),X3)),
inference(cp,[status(thm)],[t7,t47008]) ).
cnf(t47837,plain,
divide(X1,divide(inverse(inverse(X2)),X3)) = multiply(X1,inverse(divide(X2,X3))),
inference(orient,[status(thm)],[t47041]) ).
cnf(t18,plain,
inverse(X1) = divide(divide(inverse(multiply(X2,X1)),divide(divide(divide(X3,X4),divide(inverse(divide(Y4,Y5)),divide(divide(X4,X3),Y4))),X2)),Y5),
inference(cp,[status(thm)],[t12,t2]) ).
cnf(t22152,plain,
inverse(divide(X1,divide(inverse(X2),divide(X3,X4)))) = divide(inverse(multiply(Y4,X2)),divide(divide(X1,divide(X4,X3)),Y4)),
inference(cp,[status(thm)],[t22145,t7]) ).
cnf(t24519,plain,
divide(inverse(multiply(X1,X2)),divide(divide(X3,divide(X4,Y4)),X1)) = inverse(divide(X3,divide(inverse(X2),divide(Y4,X4)))),
inference(orient,[status(thm)],[t22152]) ).
cnf(t50533,plain,
inverse(X1) = divide(inverse(divide(divide(X3,X4),divide(inverse(X1),divide(divide(divide(X4,X3),Y4),inverse(divide(Y4,Y5)))))),Y5),
inference(step,[status(thm)],[t18,t24519]) ).
cnf(t50534,plain,
inverse(X1) = divide(multiply(divide(inverse(X1),divide(divide(divide(X4,X3),Y4),inverse(divide(Y4,Y5)))),divide(X4,X3)),Y5),
inference(step,[status(thm)],[t50533,t44799]) ).
cnf(t50535,plain,
inverse(X1) = multiply(divide(inverse(X1),divide(divide(divide(X4,X3),Y4),inverse(divide(Y4,Y5)))),divide(divide(X4,X3),Y5)),
inference(step,[status(thm)],[t50534,t46805]) ).
cnf(t50536,plain,
inverse(X1) = multiply(divide(inverse(X1),multiply(divide(divide(X4,X3),Y4),divide(Y4,Y5))),divide(divide(X4,X3),Y5)),
inference(step,[status(thm)],[t50535,t7]) ).
cnf(t44898,plain,
multiply(X1,divide(divide(X2,X3),X4)) = divide(X1,multiply(X4,divide(X3,X2))),
inference(cp,[status(thm)],[t7,t44799]) ).
cnf(t46151,plain,
divide(X1,multiply(X2,divide(X3,X4))) = multiply(X1,divide(divide(X4,X3),X2)),
inference(orient,[status(thm)],[t44898]) ).
cnf(t50537,plain,
inverse(X1) = multiply(multiply(inverse(X1),divide(divide(Y5,Y4),divide(divide(X4,X3),Y4))),divide(divide(X4,X3),Y5)),
inference(step,[status(thm)],[t50536,t46151]) ).
cnf(t50538,plain,
inverse(X1) = multiply(inverse(X1),multiply(divide(divide(Y5,Y4),divide(divide(X4,X3),Y4)),divide(divide(X4,X3),Y5))),
inference(step,[status(thm)],[t50537,t46656]) ).
cnf(t48595,plain,
multiply(inverse(X1),multiply(divide(divide(X2,X3),divide(divide(X4,Y4),X3)),divide(divide(X4,Y4),X2))) = inverse(X1),
inference(orient,[status(thm)],[t50538]) ).
cnf(t48600,plain,
inverse(inverse(divide(X1,X2))) = multiply(divide(inverse(inverse(X1)),X2),multiply(divide(divide(X3,X4),divide(divide(Y4,Y5),X4)),divide(divide(Y4,Y5),X3))),
inference(cp,[status(thm)],[t48595,t47008]) ).
cnf(t50539,plain,
divide(inverse(inverse(X1)),X2) = multiply(divide(inverse(inverse(X1)),X2),multiply(divide(divide(X3,X4),divide(divide(Y4,Y5),X4)),divide(divide(Y4,Y5),X3))),
inference(step,[status(thm)],[t48600,t47008]) ).
cnf(t47011,plain,
divide(inverse(inverse(divide(X1,X2))),X3) = inverse(multiply(X3,divide(X2,X1))),
inference(cp,[status(thm)],[t47008,t44799]) ).
cnf(t50512,plain,
divide(divide(inverse(inverse(X1)),X2),X3) = inverse(multiply(X3,divide(X2,X1))),
inference(step,[status(thm)],[t47011,t47008]) ).
cnf(t44843,plain,
multiply(X1,divide(inverse(X2),X3)) = inverse(divide(multiply(X3,X2),X1)),
inference(cp,[status(thm)],[t44799,t7]) ).
cnf(t45239,plain,
inverse(divide(multiply(X1,X2),X3)) = multiply(X3,divide(inverse(X2),X1)),
inference(orient,[status(thm)],[t44843]) ).
cnf(t50396,plain,
inverse(multiply(X1,divide(X2,X3))) = multiply(X3,divide(inverse(X2),X1)),
inference(step,[status(thm)],[t45239,t46805]) ).
cnf(t46925,plain,
inverse(multiply(X1,divide(X2,X3))) = multiply(X3,divide(inverse(X2),X1)),
inference(rw,[status(thm)],[t50396]) ).
cnf(t47074,plain,
inverse(multiply(X1,divide(X2,X3))) = multiply(X3,divide(inverse(X2),X1)),
inference(orient,[status(thm)],[t46925]) ).
cnf(t50513,plain,
divide(divide(inverse(inverse(X1)),X2),X3) = multiply(X1,divide(inverse(X2),X3)),
inference(step,[status(thm)],[t50512,t47074]) ).
cnf(t47682,plain,
divide(divide(inverse(inverse(X1)),X2),X3) = multiply(X1,divide(inverse(X2),X3)),
inference(orient,[status(thm)],[t50513]) ).
cnf(t47687,plain,
multiply(X1,divide(inverse(X2),inverse(X3))) = multiply(divide(inverse(inverse(X1)),X2),X3),
inference(cp,[status(thm)],[t47682,t7]) ).
cnf(t50522,plain,
multiply(X1,multiply(inverse(X2),X3)) = multiply(divide(inverse(inverse(X1)),X2),X3),
inference(step,[status(thm)],[t47687,t7]) ).
cnf(t48162,plain,
multiply(divide(inverse(inverse(X1)),X2),X3) = multiply(X1,multiply(inverse(X2),X3)),
inference(orient,[status(thm)],[t50522]) ).
cnf(t50540,plain,
divide(inverse(inverse(X1)),X2) = multiply(X1,multiply(inverse(X2),multiply(divide(divide(X3,X4),divide(divide(Y4,Y5),X4)),divide(divide(Y4,Y5),X3)))),
inference(step,[status(thm)],[t50539,t48162]) ).
cnf(t50541,plain,
divide(inverse(inverse(X1)),X2) = multiply(X1,inverse(X2)),
inference(step,[status(thm)],[t50540,t48595]) ).
cnf(t48789,plain,
divide(inverse(inverse(X1)),X2) = multiply(X1,inverse(X2)),
inference(orient,[status(thm)],[t50541]) ).
cnf(t50546,plain,
divide(X1,multiply(X2,inverse(X3))) = multiply(X1,inverse(divide(X2,X3))),
inference(step,[status(thm)],[t47837,t48789]) ).
cnf(t48902,plain,
divide(X1,multiply(X2,inverse(X3))) = multiply(X1,inverse(divide(X2,X3))),
inference(rw,[status(thm)],[t50546]) ).
cnf(t48905,plain,
divide(X1,multiply(X2,inverse(X3))) = multiply(X1,inverse(divide(X2,X3))),
inference(orient,[status(thm)],[t48902]) ).
cnf(t47083,plain,
multiply(X1,divide(inverse(X2),divide(inverse(divide(X3,X3)),X2))) = inverse(inverse(X1)),
inference(cp,[status(thm)],[t47074,t36274]) ).
cnf(t50500,plain,
multiply(X1,inverse(divide(X3,X3))) = inverse(inverse(X1)),
inference(step,[status(thm)],[t47083,t37801]) ).
cnf(t47168,plain,
multiply(X1,inverse(divide(X2,X2))) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t50500]) ).
cnf(t48913,plain,
multiply(X1,inverse(divide(X2,divide(X3,X3)))) = divide(X1,inverse(inverse(X2))),
inference(cp,[status(thm)],[t48905,t47168]) ).
cnf(t50549,plain,
multiply(X1,inverse(divide(X2,divide(X3,X3)))) = multiply(X1,inverse(X2)),
inference(step,[status(thm)],[t48913,t7]) ).
cnf(t49035,plain,
multiply(X1,inverse(divide(X2,divide(X3,X3)))) = multiply(X1,inverse(X2)),
inference(orient,[status(thm)],[t50549]) ).
cnf(t49042,plain,
multiply(X1,inverse(inverse(inverse(divide(X2,X3))))) = multiply(X1,inverse(inverse(divide(X3,X2)))),
inference(cp,[status(thm)],[t49035,t37801]) ).
cnf(t50544,plain,
inverse(inverse(divide(X1,X2))) = multiply(X1,inverse(X2)),
inference(step,[status(thm)],[t47008,t48789]) ).
cnf(t48792,plain,
inverse(inverse(divide(X1,X2))) = multiply(X1,inverse(X2)),
inference(orient,[status(thm)],[t50544]) ).
cnf(t50550,plain,
multiply(X1,inverse(multiply(X2,inverse(X3)))) = multiply(X1,inverse(inverse(divide(X3,X2)))),
inference(step,[status(thm)],[t49042,t48792]) ).
cnf(t50551,plain,
multiply(X1,inverse(multiply(X2,inverse(X3)))) = multiply(X1,multiply(X3,inverse(X2))),
inference(step,[status(thm)],[t50550,t48792]) ).
cnf(t49103,plain,
multiply(X1,inverse(multiply(X2,inverse(X3)))) = multiply(X1,multiply(X3,inverse(X2))),
inference(orient,[status(thm)],[t50551]) ).
cnf(t36307,plain,
inverse(X1) = multiply(divide(inverse(multiply(inverse(X2),X2)),X3),divide(X3,X1)),
inference(cp,[status(thm)],[t36274,t7]) ).
cnf(t38401,plain,
multiply(divide(inverse(multiply(inverse(X1),X1)),X2),divide(X2,X3)) = inverse(X3),
inference(orient,[status(thm)],[t36307]) ).
cnf(t47082,plain,
multiply(X1,divide(inverse(X2),divide(inverse(multiply(inverse(X3),X3)),X2))) = inverse(inverse(X1)),
inference(cp,[status(thm)],[t47074,t38401]) ).
cnf(t50506,plain,
multiply(X1,inverse(divide(inverse(X3),inverse(X3)))) = inverse(inverse(X1)),
inference(step,[status(thm)],[t47082,t38112]) ).
cnf(t50507,plain,
multiply(X1,inverse(multiply(inverse(X3),X3))) = inverse(inverse(X1)),
inference(step,[status(thm)],[t50506,t7]) ).
cnf(t47300,plain,
multiply(X1,inverse(multiply(inverse(X2),X2))) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t50507]) ).
cnf(t49104,plain,
multiply(X1,multiply(X2,inverse(inverse(inverse(X2))))) = inverse(inverse(X1)),
inference(cp,[status(thm)],[t49103,t47300]) ).
cnf(t49143,plain,
inverse(inverse(multiply(X1,inverse(X2)))) = divide(divide(inverse(multiply(X3,multiply(X2,inverse(X1)))),divide(divide(X4,Y4),X3)),divide(Y4,X4)),
inference(cp,[status(thm)],[t12,t49103]) ).
cnf(t46679,plain,
multiply(divide(inverse(multiply(inverse(X1),X1)),X2),multiply(multiply(X2,X3),X4)) = multiply(inverse(inverse(X3)),X4),
inference(cp,[status(thm)],[t46656,t39858]) ).
cnf(t50492,plain,
multiply(divide(inverse(multiply(inverse(X1),X1)),X2),multiply(X2,multiply(X3,X4))) = multiply(inverse(inverse(X3)),X4),
inference(step,[status(thm)],[t46679,t46656]) ).
cnf(t50493,plain,
inverse(inverse(multiply(X3,X4))) = multiply(inverse(inverse(X3)),X4),
inference(step,[status(thm)],[t50492,t39858]) ).
cnf(t46952,plain,
inverse(inverse(multiply(X1,X2))) = multiply(inverse(inverse(X1)),X2),
inference(orient,[status(thm)],[t50493]) ).
cnf(t47169,plain,
inverse(inverse(multiply(X1,X2))) = multiply(X1,multiply(X2,inverse(divide(X3,X3)))),
inference(cp,[status(thm)],[t47168,t46656]) ).
cnf(t50501,plain,
multiply(inverse(inverse(X1)),X2) = multiply(X1,multiply(X2,inverse(divide(X3,X3)))),
inference(step,[status(thm)],[t47169,t46952]) ).
cnf(t50502,plain,
multiply(inverse(inverse(X1)),X2) = multiply(X1,inverse(inverse(X2))),
inference(step,[status(thm)],[t50501,t47168]) ).
cnf(t47234,plain,
multiply(inverse(inverse(X1)),X2) = multiply(X1,inverse(inverse(X2))),
inference(orient,[status(thm)],[t50502]) ).
cnf(t50503,plain,
inverse(inverse(multiply(X1,X2))) = multiply(X1,inverse(inverse(X2))),
inference(step,[status(thm)],[t46952,t47234]) ).
cnf(t47235,plain,
inverse(inverse(multiply(X1,X2))) = multiply(X1,inverse(inverse(X2))),
inference(orient,[status(thm)],[t50503]) ).
cnf(t50552,plain,
multiply(X1,inverse(inverse(inverse(X2)))) = divide(divide(inverse(multiply(X3,multiply(X2,inverse(X1)))),divide(divide(X4,Y4),X3)),divide(Y4,X4)),
inference(step,[status(thm)],[t49143,t47235]) ).
cnf(t50553,plain,
multiply(X1,inverse(inverse(inverse(X2)))) = inverse(multiply(X2,inverse(X1))),
inference(step,[status(thm)],[t50552,t12]) ).
cnf(t49167,plain,
multiply(X1,inverse(inverse(inverse(X2)))) = inverse(multiply(X2,inverse(X1))),
inference(orient,[status(thm)],[t50553]) ).
cnf(t50554,plain,
multiply(X1,inverse(multiply(X2,inverse(X2)))) = inverse(inverse(X1)),
inference(step,[status(thm)],[t49104,t49167]) ).
cnf(t50555,plain,
multiply(X1,multiply(X2,inverse(X2))) = inverse(inverse(X1)),
inference(step,[status(thm)],[t50554,t49103]) ).
cnf(t49225,plain,
multiply(X1,multiply(X2,inverse(X2))) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t50555]) ).
cnf(t49226,plain,
inverse(inverse(inverse(inverse(X1)))) = multiply(X1,inverse(inverse(multiply(X2,inverse(X2))))),
inference(cp,[status(thm)],[t49225,t47234]) ).
cnf(t50556,plain,
inverse(inverse(inverse(inverse(X1)))) = multiply(X1,multiply(X2,inverse(inverse(inverse(X2))))),
inference(step,[status(thm)],[t49226,t47235]) ).
cnf(t50557,plain,
inverse(inverse(inverse(inverse(X1)))) = multiply(X1,inverse(multiply(X2,inverse(X2)))),
inference(step,[status(thm)],[t50556,t49167]) ).
cnf(t50558,plain,
inverse(inverse(inverse(inverse(X1)))) = multiply(X1,multiply(X2,inverse(X2))),
inference(step,[status(thm)],[t50557,t49103]) ).
cnf(t50559,plain,
inverse(inverse(inverse(inverse(X1)))) = inverse(inverse(X1)),
inference(step,[status(thm)],[t50558,t49225]) ).
cnf(t49300,plain,
inverse(inverse(inverse(inverse(X1)))) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t50559]) ).
cnf(t49302,plain,
inverse(inverse(divide(X1,X2))) = inverse(inverse(multiply(X1,inverse(X2)))),
inference(cp,[status(thm)],[t49300,t48792]) ).
cnf(t50560,plain,
multiply(X1,inverse(X2)) = inverse(inverse(multiply(X1,inverse(X2)))),
inference(step,[status(thm)],[t49302,t48792]) ).
cnf(t50561,plain,
multiply(X1,inverse(X2)) = multiply(X1,inverse(inverse(inverse(X2)))),
inference(step,[status(thm)],[t50560,t47235]) ).
cnf(t50562,plain,
multiply(X1,inverse(X2)) = inverse(multiply(X2,inverse(X1))),
inference(step,[status(thm)],[t50561,t49167]) ).
cnf(t49339,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t50562]) ).
cnf(t49343,plain,
multiply(divide(X1,X1),inverse(X2)) = inverse(inverse(inverse(X2))),
inference(cp,[status(thm)],[t49339,t47168]) ).
cnf(t44837,plain,
multiply(inverse(X1),divide(X2,X3)) = inverse(multiply(divide(X3,X2),X1)),
inference(cp,[status(thm)],[t44799,t7]) ).
cnf(t45036,plain,
inverse(multiply(divide(X1,X2),X3)) = multiply(inverse(X3),divide(X2,X1)),
inference(orient,[status(thm)],[t44837]) ).
cnf(t46953,plain,
multiply(inverse(inverse(divide(X1,X2))),X3) = inverse(multiply(inverse(X3),divide(X2,X1))),
inference(cp,[status(thm)],[t46952,t45036]) ).
cnf(t50527,plain,
multiply(divide(X1,X2),inverse(inverse(X3))) = inverse(multiply(inverse(X3),divide(X2,X1))),
inference(step,[status(thm)],[t46953,t47234]) ).
cnf(t50528,plain,
multiply(divide(X1,X2),inverse(inverse(X3))) = multiply(X1,divide(inverse(X2),inverse(X3))),
inference(step,[status(thm)],[t50527,t47074]) ).
cnf(t50529,plain,
multiply(divide(X1,X2),inverse(inverse(X3))) = multiply(X1,multiply(inverse(X2),X3)),
inference(step,[status(thm)],[t50528,t7]) ).
cnf(t48420,plain,
multiply(divide(X1,X2),inverse(inverse(X3))) = multiply(X1,multiply(inverse(X2),X3)),
inference(orient,[status(thm)],[t50529]) ).
cnf(t48462,plain,
multiply(X1,multiply(inverse(X2),divide(X3,divide(divide(X4,divide(divide(Y4,Y5),X3)),divide(Y5,Y4))))) = multiply(divide(X1,X2),inverse(X4)),
inference(cp,[status(thm)],[t48420,t22482]) ).
cnf(t50530,plain,
multiply(X1,divide(inverse(X2),X4)) = multiply(divide(X1,X2),inverse(X4)),
inference(step,[status(thm)],[t48462,t29537]) ).
cnf(t48507,plain,
multiply(divide(X1,X2),inverse(X3)) = multiply(X1,divide(inverse(X2),X3)),
inference(orient,[status(thm)],[t50530]) ).
cnf(t50565,plain,
multiply(X1,divide(inverse(X1),X2)) = inverse(inverse(inverse(X2))),
inference(step,[status(thm)],[t49343,t48507]) ).
cnf(t49405,plain,
multiply(X1,divide(inverse(X1),X2)) = inverse(inverse(inverse(X2))),
inference(orient,[status(thm)],[t50565]) ).
cnf(t49469,plain,
inverse(divide(inverse(X1),X2)) = divide(divide(inverse(inverse(inverse(inverse(X2)))),divide(divide(inverse(X3),X4),X1)),multiply(X4,X3)),
inference(cp,[status(thm)],[t128,t49405]) ).
cnf(t49487,plain,
inverse(divide(inverse(X1),X2)) = multiply(X2,inverse(inverse(X1))),
inference(orient,[status(thm)],[t49469]) ).
cnf(t50566,plain,
divide(inverse(X1),divide(inverse(multiply(X2,X3)),X1)) = multiply(X2,inverse(inverse(X3))),
inference(step,[status(thm)],[t38112,t49487]) ).
cnf(t49488,plain,
divide(inverse(X1),divide(inverse(multiply(X2,X3)),X1)) = multiply(X2,inverse(inverse(X3))),
inference(orient,[status(thm)],[t50566]) ).
cnf(t49555,plain,
X1 = divide(divide(multiply(X1,inverse(inverse(X2))),divide(divide(inverse(X3),X4),inverse(X2))),multiply(X4,X3)),
inference(cp,[status(thm)],[t60,t49487]) ).
cnf(t50583,plain,
X1 = divide(multiply(X1,divide(inverse(inverse(X2)),divide(divide(inverse(X3),X4),inverse(X2)))),multiply(X4,X3)),
inference(step,[status(thm)],[t49555,t46805]) ).
cnf(t46845,plain,
inverse(divide(X1,multiply(X2,X3))) = divide(inverse(X4),divide(inverse(multiply(X2,divide(X3,X1))),X4)),
inference(cp,[status(thm)],[t37801,t46805]) ).
cnf(t50508,plain,
inverse(divide(X1,multiply(X2,X3))) = inverse(divide(inverse(divide(X3,X1)),X2)),
inference(step,[status(thm)],[t46845,t38112]) ).
cnf(t47371,plain,
inverse(divide(inverse(divide(X1,X2)),X3)) = inverse(divide(X2,multiply(X3,X1))),
inference(orient,[status(thm)],[t50508]) ).
cnf(t36462,plain,
inverse(divide(divide(multiply(inverse(X1),X2),X2),X3)) = multiply(inverse(inverse(X3)),X1),
inference(cp,[status(thm)],[t16759,t36274]) ).
cnf(t36492,plain,
inverse(divide(divide(multiply(inverse(X1),X2),X2),X3)) = multiply(inverse(inverse(X3)),X1),
inference(orient,[status(thm)],[t36462]) ).
cnf(t36527,plain,
multiply(inverse(inverse(X1)),divide(X2,divide(divide(X3,divide(divide(X4,Y4),X2)),divide(Y4,X4)))) = inverse(divide(divide(multiply(X3,Y5),Y5),X1)),
inference(cp,[status(thm)],[t36492,t22482]) ).
cnf(t50249,plain,
divide(inverse(inverse(X1)),X3) = inverse(divide(divide(multiply(X3,Y5),Y5),X1)),
inference(step,[status(thm)],[t36527,t29537]) ).
cnf(t36651,plain,
inverse(divide(divide(multiply(X1,X2),X2),X3)) = divide(inverse(inverse(X3)),X1),
inference(orient,[status(thm)],[t50249]) ).
cnf(t50271,plain,
multiply(X3,divide(X2,multiply(X1,X2))) = divide(inverse(inverse(X3)),X1),
inference(step,[status(thm)],[t36651,t44799]) ).
cnf(t45025,plain,
multiply(X3,divide(X2,multiply(X1,X2))) = divide(inverse(inverse(X3)),X1),
inference(rw,[status(thm)],[t50271]) ).
cnf(t45429,plain,
multiply(X1,divide(X2,multiply(X3,X2))) = divide(inverse(inverse(X1)),X3),
inference(orient,[status(thm)],[t45025]) ).
cnf(t45574,plain,
divide(inverse(divide(X1,multiply(X2,X1))),X3) = multiply(divide(divide(X4,Y4),Y5),divide(Y5,divide(divide(inverse(inverse(X3)),X2),divide(Y4,X4)))),
inference(cp,[status(thm)],[t15873,t45429]) ).
cnf(t50334,plain,
divide(inverse(divide(X1,multiply(X2,X1))),X3) = divide(X2,inverse(inverse(X3))),
inference(step,[status(thm)],[t45574,t15516]) ).
cnf(t50335,plain,
divide(inverse(divide(X1,multiply(X2,X1))),X3) = multiply(X2,inverse(X3)),
inference(step,[status(thm)],[t50334,t7]) ).
cnf(t45891,plain,
divide(inverse(divide(X1,multiply(X2,X1))),X3) = multiply(X2,inverse(X3)),
inference(orient,[status(thm)],[t50335]) ).
cnf(t47377,plain,
inverse(divide(multiply(X1,X2),multiply(X3,X2))) = inverse(multiply(X1,inverse(X3))),
inference(cp,[status(thm)],[t47371,t45891]) ).
cnf(t50509,plain,
inverse(multiply(X1,divide(X2,multiply(X3,X2)))) = inverse(multiply(X1,inverse(X3))),
inference(step,[status(thm)],[t47377,t46805]) ).
cnf(t50510,plain,
inverse(divide(inverse(inverse(X1)),X3)) = inverse(multiply(X1,inverse(X3))),
inference(step,[status(thm)],[t50509,t45429]) ).
cnf(t47473,plain,
inverse(divide(inverse(inverse(X1)),X2)) = inverse(multiply(X1,inverse(X2))),
inference(orient,[status(thm)],[t50510]) ).
cnf(t47483,plain,
inverse(multiply(divide(X1,X2),inverse(X3))) = inverse(divide(divide(inverse(inverse(X1)),X2),X3)),
inference(cp,[status(thm)],[t47473,t47008]) ).
cnf(t50516,plain,
multiply(inverse(inverse(X3)),divide(X2,X1)) = inverse(divide(divide(inverse(inverse(X1)),X2),X3)),
inference(step,[status(thm)],[t47483,t45036]) ).
cnf(t50517,plain,
multiply(X3,inverse(inverse(divide(X2,X1)))) = inverse(divide(divide(inverse(inverse(X1)),X2),X3)),
inference(step,[status(thm)],[t50516,t47234]) ).
cnf(t50518,plain,
multiply(X3,divide(inverse(inverse(X2)),X1)) = inverse(divide(divide(inverse(inverse(X1)),X2),X3)),
inference(step,[status(thm)],[t50517,t47008]) ).
cnf(t50519,plain,
multiply(X3,divide(inverse(inverse(X2)),X1)) = multiply(X3,divide(X2,inverse(inverse(X1)))),
inference(step,[status(thm)],[t50518,t44799]) ).
cnf(t50520,plain,
multiply(X3,divide(inverse(inverse(X2)),X1)) = multiply(X3,multiply(X2,inverse(X1))),
inference(step,[status(thm)],[t50519,t7]) ).
cnf(t47990,plain,
multiply(X1,divide(inverse(inverse(X2)),X3)) = multiply(X1,multiply(X2,inverse(X3))),
inference(orient,[status(thm)],[t50520]) ).
cnf(t50584,plain,
X1 = divide(multiply(X1,multiply(X2,inverse(divide(divide(inverse(X3),X4),inverse(X2))))),multiply(X4,X3)),
inference(step,[status(thm)],[t50583,t47990]) ).
cnf(t50585,plain,
X1 = multiply(X1,divide(multiply(X2,inverse(divide(divide(inverse(X3),X4),inverse(X2)))),multiply(X4,X3))),
inference(step,[status(thm)],[t50584,t46805]) ).
cnf(t50586,plain,
X1 = multiply(X1,multiply(X2,divide(inverse(divide(divide(inverse(X3),X4),inverse(X2))),multiply(X4,X3)))),
inference(step,[status(thm)],[t50585,t46805]) ).
cnf(t50587,plain,
X1 = multiply(X1,multiply(X2,divide(multiply(inverse(X2),divide(X4,inverse(X3))),multiply(X4,X3)))),
inference(step,[status(thm)],[t50586,t44799]) ).
cnf(t50588,plain,
X1 = multiply(X1,multiply(X2,multiply(inverse(X2),divide(divide(X4,inverse(X3)),multiply(X4,X3))))),
inference(step,[status(thm)],[t50587,t46805]) ).
cnf(t50589,plain,
X1 = multiply(X1,multiply(X2,multiply(inverse(X2),divide(multiply(X4,X3),multiply(X4,X3))))),
inference(step,[status(thm)],[t50588,t7]) ).
cnf(t50590,plain,
X1 = multiply(X1,multiply(X2,multiply(inverse(X2),multiply(X4,divide(X3,multiply(X4,X3)))))),
inference(step,[status(thm)],[t50589,t46805]) ).
cnf(t50542,plain,
multiply(X1,divide(X2,multiply(X3,X2))) = multiply(X1,inverse(X3)),
inference(step,[status(thm)],[t45429,t48789]) ).
cnf(t48790,plain,
multiply(X1,divide(X2,multiply(X3,X2))) = multiply(X1,inverse(X3)),
inference(orient,[status(thm)],[t50542]) ).
cnf(t50591,plain,
X1 = multiply(X1,multiply(X2,multiply(inverse(X2),multiply(X4,inverse(X4))))),
inference(step,[status(thm)],[t50590,t48790]) ).
cnf(t50592,plain,
X1 = multiply(X1,multiply(X2,inverse(inverse(inverse(X2))))),
inference(step,[status(thm)],[t50591,t49225]) ).
cnf(t50563,plain,
multiply(X1,inverse(inverse(inverse(X2)))) = multiply(X1,inverse(X2)),
inference(step,[status(thm)],[t49167,t49339]) ).
cnf(t49340,plain,
multiply(X1,inverse(inverse(inverse(X2)))) = multiply(X1,inverse(X2)),
inference(orient,[status(thm)],[t50563]) ).
cnf(t50593,plain,
X1 = multiply(X1,multiply(X2,inverse(X2))),
inference(step,[status(thm)],[t50592,t49340]) ).
cnf(t50594,plain,
X1 = inverse(inverse(X1)),
inference(step,[status(thm)],[t50593,t49225]) ).
cnf(t49566,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t50594]) ).
cnf(t50597,plain,
divide(inverse(X1),divide(inverse(multiply(X2,X3)),X1)) = multiply(X2,X3),
inference(step,[status(thm)],[t49488,t49566]) ).
cnf(t49569,plain,
divide(inverse(X1),divide(inverse(multiply(X2,X3)),X1)) = multiply(X2,X3),
inference(orient,[status(thm)],[t50597]) ).
cnf(t49588,plain,
multiply(X1,inverse(X2)) = divide(X1,X2),
inference(cp,[status(thm)],[t7,t49566]) ).
cnf(t49618,plain,
multiply(X1,inverse(X2)) = divide(X1,X2),
inference(orient,[status(thm)],[t49588]) ).
cnf(t49638,plain,
multiply(X1,inverse(X2)) = divide(inverse(X3),divide(inverse(divide(X1,X2)),X3)),
inference(cp,[status(thm)],[t49569,t49618]) ).
cnf(t50627,plain,
divide(X1,X2) = divide(inverse(X3),divide(inverse(divide(X1,X2)),X3)),
inference(step,[status(thm)],[t49638,t49618]) ).
cnf(t50628,plain,
divide(X1,X2) = inverse(divide(X2,X1)),
inference(step,[status(thm)],[t50627,t37801]) ).
cnf(t49658,plain,
inverse(divide(X1,X2)) = divide(X2,X1),
inference(orient,[status(thm)],[t50628]) ).
cnf(t50601,plain,
multiply(X1,inverse(divide(X2,X2))) = X1,
inference(step,[status(thm)],[t47168,t49566]) ).
cnf(t49573,plain,
multiply(X1,inverse(divide(X2,X2))) = X1,
inference(orient,[status(thm)],[t50601]) ).
cnf(t50623,plain,
divide(X1,divide(X2,X2)) = X1,
inference(step,[status(thm)],[t49573,t49618]) ).
cnf(t49655,plain,
divide(X1,divide(X2,X2)) = X1,
inference(rw,[status(thm)],[t50623]) ).
cnf(t49766,plain,
divide(X1,divide(X2,X2)) = X1,
inference(orient,[status(thm)],[t49655]) ).
cnf(t49777,plain,
divide(divide(X1,X1),X2) = inverse(X2),
inference(cp,[status(thm)],[t49658,t49766]) ).
cnf(t49884,plain,
divide(divide(X1,X1),X2) = inverse(X2),
inference(orient,[status(thm)],[t49777]) ).
cnf(t49888,plain,
inverse(inverse(X1)) = multiply(divide(X2,X2),X1),
inference(cp,[status(thm)],[t49884,t7]) ).
cnf(t50710,plain,
X1 = multiply(divide(X2,X2),X1),
inference(step,[status(thm)],[t49888,t49566]) ).
cnf(t49922,plain,
multiply(divide(X1,X1),X2) = X2,
inference(orient,[status(thm)],[t50710]) ).
cnf(t49931,plain,
X1 = multiply(multiply(inverse(X2),X2),X1),
inference(cp,[status(thm)],[t49922,t7]) ).
cnf(t50714,plain,
X1 = multiply(inverse(X2),multiply(X2,X1)),
inference(step,[status(thm)],[t49931,t46656]) ).
cnf(t50077,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(orient,[status(thm)],[t50714]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(inverse(b2),multiply(b2,a2)) != a2,
inference(rw,[status(thm)],[goal_0,t46656]) ).
cnf(g0_1,plain,
a2 != a2,
inference(rw,[status(thm)],[g0_0,t50077]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP473-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/0.38 % Computer : n008.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 14:51:55 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 16.36/2.82 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.36/2.82 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------