%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP471-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : 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 15.46s 3.12s
% Output : CNFRefutation 15.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 126
% Number of leaves : 3
% Syntax : Number of clauses : 232 ( 232 unt; 0 nHn; 3 RR)
% Number of literals : 232 ( 231 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 11 ( 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 : 840 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t1,axiom,
divide(inverse(divide(X1,divide(X2,divide(X3,X4)))),divide(divide(X4,X3),X1)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t2,plain,
divide(inverse(divide(X1,divide(X2,divide(X3,X4)))),divide(divide(X4,X3),X1)) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(t0,axiom,
divide(X1,inverse(X2)) = multiply(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t7,plain,
divide(X1,inverse(X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t0]) ).
cnf(t9,plain,
X1 = divide(inverse(divide(inverse(X2),divide(X1,divide(X3,X4)))),multiply(divide(X4,X3),X2)),
inference(cp,[status(thm)],[t2,t7]) ).
cnf(t22,plain,
divide(inverse(divide(inverse(X1),divide(X2,divide(X3,X4)))),multiply(divide(X4,X3),X1)) = X2,
inference(orient,[status(thm)],[t9]) ).
cnf(t23,plain,
divide(X1,X2) = divide(inverse(X3),multiply(divide(X4,Y4),divide(divide(Y4,X4),divide(X3,divide(X2,X1))))),
inference(cp,[status(thm)],[t22,t2]) ).
cnf(t849,plain,
divide(inverse(X1),multiply(divide(X2,X3),divide(divide(X3,X2),divide(X1,divide(X4,Y4))))) = divide(Y4,X4),
inference(orient,[status(thm)],[t23]) ).
cnf(t930,plain,
divide(multiply(divide(X1,X2),divide(divide(X2,X1),divide(X3,divide(X4,Y4)))),inverse(X3)) = divide(inverse(Y5),multiply(divide(Y6,Y7),divide(divide(Y7,Y6),divide(Y5,divide(Y4,X4))))),
inference(cp,[status(thm)],[t849,t849]) ).
cnf(t25815,plain,
multiply(multiply(divide(X1,X2),divide(divide(X2,X1),divide(X3,divide(X4,Y4)))),X3) = divide(inverse(Y5),multiply(divide(Y6,Y7),divide(divide(Y7,Y6),divide(Y5,divide(Y4,X4))))),
inference(step,[status(thm)],[t930,t7]) ).
cnf(t25816,plain,
multiply(multiply(divide(X1,X2),divide(divide(X2,X1),divide(X3,divide(X4,Y4)))),X3) = divide(X4,Y4),
inference(step,[status(thm)],[t25815,t849]) ).
cnf(t949,plain,
multiply(multiply(divide(X1,X2),divide(divide(X2,X1),divide(X3,divide(X4,Y4)))),X3) = divide(X4,Y4),
inference(orient,[status(thm)],[t25816]) ).
cnf(t1001,plain,
divide(inverse(divide(inverse(X1),divide(X2,divide(X3,X4)))),multiply(divide(X4,X3),X1)) = multiply(multiply(divide(Y4,Y5),divide(divide(Y5,Y4),divide(Y6,X2))),Y6),
inference(cp,[status(thm)],[t949,t22]) ).
cnf(t25817,plain,
X2 = multiply(multiply(divide(Y4,Y5),divide(divide(Y5,Y4),divide(Y6,X2))),Y6),
inference(step,[status(thm)],[t1001,t22]) ).
cnf(t1014,plain,
multiply(multiply(divide(X1,X2),divide(divide(X2,X1),divide(X3,X4))),X3) = X4,
inference(orient,[status(thm)],[t25817]) ).
cnf(t1049,plain,
inverse(X1) = multiply(multiply(divide(X2,X3),divide(divide(X3,X2),multiply(X4,X1))),X4),
inference(cp,[status(thm)],[t1014,t7]) ).
cnf(t1082,plain,
multiply(multiply(divide(X1,X2),divide(divide(X2,X1),multiply(X3,X4))),X3) = inverse(X4),
inference(orient,[status(thm)],[t1049]) ).
cnf(t1084,plain,
inverse(X1) = multiply(multiply(multiply(X2,X3),divide(divide(inverse(X3),X2),multiply(X4,X1))),X4),
inference(cp,[status(thm)],[t1082,t7]) ).
cnf(t1262,plain,
multiply(multiply(multiply(X1,X2),divide(divide(inverse(X2),X1),multiply(X3,X4))),X3) = inverse(X4),
inference(orient,[status(thm)],[t1084]) ).
cnf(t4,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)],[t2,t2]) ).
cnf(t59,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)],[t4]) ).
cnf(t60,plain,
inverse(divide(X1,divide(divide(X2,divide(divide(X3,X4),X1)),divide(X4,X3)))) = X2,
inference(cp,[status(thm)],[t59,t2]) ).
cnf(t90,plain,
inverse(divide(X1,divide(divide(X2,divide(divide(X3,X4),X1)),divide(X4,X3)))) = X2,
inference(orient,[status(thm)],[t60]) ).
cnf(t91,plain,
X1 = inverse(inverse(divide(X1,divide(X2,divide(inverse(divide(divide(X3,X4),X2)),divide(X4,X3)))))),
inference(cp,[status(thm)],[t90,t59]) ).
cnf(t433,plain,
inverse(inverse(divide(X1,divide(X2,divide(inverse(divide(divide(X3,X4),X2)),divide(X4,X3)))))) = X1,
inference(orient,[status(thm)],[t91]) ).
cnf(t438,plain,
inverse(divide(divide(inverse(divide(divide(X1,X2),divide(X3,X4))),divide(X2,X1)),divide(Y4,divide(X4,X3)))) = inverse(inverse(Y4)),
inference(cp,[status(thm)],[t433,t2]) ).
cnf(t4744,plain,
inverse(divide(divide(inverse(divide(divide(X1,X2),divide(X3,X4))),divide(X2,X1)),divide(Y4,divide(X4,X3)))) = inverse(inverse(Y4)),
inference(orient,[status(thm)],[t438]) ).
cnf(t4942,plain,
divide(inverse(divide(divide(X1,X2),divide(divide(X3,X4),inverse(divide(divide(X4,X3),Y4))))),divide(X2,X1)) = inverse(inverse(inverse(Y4))),
inference(cp,[status(thm)],[t433,t4744]) ).
cnf(t25828,plain,
divide(inverse(divide(divide(X1,X2),multiply(divide(X3,X4),divide(divide(X4,X3),Y4)))),divide(X2,X1)) = inverse(inverse(inverse(Y4))),
inference(step,[status(thm)],[t4942,t7]) ).
cnf(t4973,plain,
divide(inverse(divide(divide(X1,X2),multiply(divide(X3,X4),divide(divide(X4,X3),Y4)))),divide(X2,X1)) = inverse(inverse(inverse(Y4))),
inference(orient,[status(thm)],[t25828]) ).
cnf(t5212,plain,
X1 = inverse(inverse(divide(X1,divide(multiply(divide(X2,X3),divide(divide(X3,X2),X4)),inverse(inverse(inverse(X4))))))),
inference(cp,[status(thm)],[t433,t4973]) ).
cnf(t25829,plain,
X1 = inverse(inverse(divide(X1,multiply(multiply(divide(X2,X3),divide(divide(X3,X2),X4)),inverse(inverse(X4)))))),
inference(step,[status(thm)],[t5212,t7]) ).
cnf(t5239,plain,
inverse(inverse(divide(X1,multiply(multiply(divide(X2,X3),divide(divide(X3,X2),X4)),inverse(inverse(X4)))))) = X1,
inference(orient,[status(thm)],[t25829]) ).
cnf(t30,plain,
X1 = divide(inverse(divide(inverse(X2),divide(X1,divide(inverse(X3),X4)))),multiply(multiply(X4,X3),X2)),
inference(cp,[status(thm)],[t22,t7]) ).
cnf(t384,plain,
divide(inverse(divide(inverse(X1),divide(X2,divide(inverse(X3),X4)))),multiply(multiply(X4,X3),X1)) = X2,
inference(orient,[status(thm)],[t30]) ).
cnf(t5240,plain,
inverse(divide(inverse(inverse(inverse(X1))),divide(X2,divide(inverse(divide(divide(X3,X4),X1)),divide(X4,X3))))) = inverse(inverse(X2)),
inference(cp,[status(thm)],[t5239,t384]) ).
cnf(t6033,plain,
inverse(divide(inverse(inverse(inverse(X1))),divide(X2,divide(inverse(divide(divide(X3,X4),X1)),divide(X4,X3))))) = inverse(inverse(X2)),
inference(orient,[status(thm)],[t5240]) ).
cnf(t6140,plain,
X1 = divide(inverse(inverse(X1)),divide(divide(divide(X2,X3),inverse(divide(divide(X3,X2),X4))),inverse(inverse(inverse(X4))))),
inference(cp,[status(thm)],[t2,t6033]) ).
cnf(t25833,plain,
X1 = divide(inverse(inverse(X1)),multiply(divide(divide(X2,X3),inverse(divide(divide(X3,X2),X4))),inverse(inverse(X4)))),
inference(step,[status(thm)],[t6140,t7]) ).
cnf(t25834,plain,
X1 = divide(inverse(inverse(X1)),multiply(multiply(divide(X2,X3),divide(divide(X3,X2),X4)),inverse(inverse(X4)))),
inference(step,[status(thm)],[t25833,t7]) ).
cnf(t6243,plain,
divide(inverse(inverse(X1)),multiply(multiply(divide(X2,X3),divide(divide(X3,X2),X4)),inverse(inverse(X4)))) = X1,
inference(orient,[status(thm)],[t25834]) ).
cnf(t6338,plain,
X1 = divide(inverse(inverse(X1)),multiply(multiply(divide(X2,X3),divide(divide(X3,X2),divide(X4,divide(Y4,divide(inverse(divide(divide(Y5,Y6),Y4)),divide(Y6,Y5)))))),X4)),
inference(cp,[status(thm)],[t6243,t433]) ).
cnf(t25835,plain,
X1 = divide(inverse(inverse(X1)),divide(Y4,divide(inverse(divide(divide(Y5,Y6),Y4)),divide(Y6,Y5)))),
inference(step,[status(thm)],[t6338,t949]) ).
cnf(t6490,plain,
divide(inverse(inverse(X1)),divide(X2,divide(inverse(divide(divide(X3,X4),X2)),divide(X4,X3)))) = X1,
inference(orient,[status(thm)],[t25835]) ).
cnf(t6619,plain,
X1 = divide(inverse(X2),divide(divide(divide(X3,X4),inverse(divide(divide(X4,X3),X1))),inverse(inverse(X2)))),
inference(cp,[status(thm)],[t2,t6490]) ).
cnf(t25836,plain,
X1 = divide(inverse(X2),multiply(divide(divide(X3,X4),inverse(divide(divide(X4,X3),X1))),inverse(X2))),
inference(step,[status(thm)],[t6619,t7]) ).
cnf(t25837,plain,
X1 = divide(inverse(X2),multiply(multiply(divide(X3,X4),divide(divide(X4,X3),X1)),inverse(X2))),
inference(step,[status(thm)],[t25836,t7]) ).
cnf(t6738,plain,
divide(inverse(X1),multiply(multiply(divide(X2,X3),divide(divide(X3,X2),X4)),inverse(X1))) = X4,
inference(orient,[status(thm)],[t25837]) ).
cnf(t6739,plain,
X1 = divide(X2,multiply(multiply(divide(X3,X4),divide(divide(X4,X3),X1)),inverse(inverse(divide(X2,multiply(multiply(divide(Y4,Y5),divide(divide(Y5,Y4),Y6)),inverse(inverse(Y6)))))))),
inference(cp,[status(thm)],[t6738,t5239]) ).
cnf(t25838,plain,
X1 = divide(X2,multiply(multiply(divide(X3,X4),divide(divide(X4,X3),X1)),X2)),
inference(step,[status(thm)],[t6739,t5239]) ).
cnf(t6970,plain,
divide(X1,multiply(multiply(divide(X2,X3),divide(divide(X3,X2),X4)),X1)) = X4,
inference(orient,[status(thm)],[t25838]) ).
cnf(t7017,plain,
inverse(X1) = divide(X2,multiply(multiply(divide(X3,X4),multiply(divide(X4,X3),X1)),X2)),
inference(cp,[status(thm)],[t6970,t7]) ).
cnf(t7230,plain,
divide(X1,multiply(multiply(divide(X2,X3),multiply(divide(X3,X2),X4)),X1)) = inverse(X4),
inference(orient,[status(thm)],[t7017]) ).
cnf(t7248,plain,
inverse(X1) = divide(X2,multiply(multiply(multiply(X3,X4),multiply(divide(inverse(X4),X3),X1)),X2)),
inference(cp,[status(thm)],[t7230,t7]) ).
cnf(t8023,plain,
divide(X1,multiply(multiply(multiply(X2,X3),multiply(divide(inverse(X3),X2),X4)),X1)) = inverse(X4),
inference(orient,[status(thm)],[t7248]) ).
cnf(t7075,plain,
inverse(divide(X1,X2)) = multiply(multiply(divide(X2,X1),X3),multiply(divide(X4,Y4),divide(divide(Y4,X4),X3))),
inference(cp,[status(thm)],[t1082,t6970]) ).
cnf(t9273,plain,
multiply(multiply(divide(X1,X2),X3),multiply(divide(X4,Y4),divide(divide(Y4,X4),X3))) = inverse(divide(X2,X1)),
inference(orient,[status(thm)],[t7075]) ).
cnf(t9449,plain,
inverse(divide(divide(divide(X1,X2),inverse(X3)),X3)) = divide(X4,multiply(inverse(divide(X2,X1)),X4)),
inference(cp,[status(thm)],[t8023,t9273]) ).
cnf(t25844,plain,
inverse(divide(multiply(divide(X1,X2),X3),X3)) = divide(X4,multiply(inverse(divide(X2,X1)),X4)),
inference(step,[status(thm)],[t9449,t7]) ).
cnf(t9473,plain,
inverse(divide(multiply(divide(X1,X2),X3),X3)) = divide(X4,multiply(inverse(divide(X2,X1)),X4)),
inference(orient,[status(thm)],[t25844]) ).
cnf(t8,plain,
X1 = divide(inverse(divide(X2,divide(X1,multiply(X3,X4)))),divide(divide(inverse(X4),X3),X2)),
inference(cp,[status(thm)],[t2,t7]) ).
cnf(t11,plain,
divide(inverse(divide(X1,divide(X2,multiply(X3,X4)))),divide(divide(inverse(X4),X3),X1)) = X2,
inference(orient,[status(thm)],[t8]) ).
cnf(t15,plain,
X1 = divide(inverse(divide(X2,divide(X1,multiply(inverse(X3),X4)))),divide(multiply(inverse(X4),X3),X2)),
inference(cp,[status(thm)],[t11,t7]) ).
cnf(t341,plain,
divide(inverse(divide(X1,divide(X2,multiply(inverse(X3),X4)))),divide(multiply(inverse(X4),X3),X1)) = X2,
inference(orient,[status(thm)],[t15]) ).
cnf(t346,plain,
divide(X1,X2) = divide(inverse(X3),divide(multiply(inverse(X4),Y4),inverse(divide(multiply(inverse(Y4),X4),divide(X3,divide(X2,X1)))))),
inference(cp,[status(thm)],[t341,t2]) ).
cnf(t25826,plain,
divide(X1,X2) = divide(inverse(X3),multiply(multiply(inverse(X4),Y4),divide(multiply(inverse(Y4),X4),divide(X3,divide(X2,X1))))),
inference(step,[status(thm)],[t346,t7]) ).
cnf(t4131,plain,
divide(inverse(X1),multiply(multiply(inverse(X2),X3),divide(multiply(inverse(X3),X2),divide(X1,divide(X4,Y4))))) = divide(Y4,X4),
inference(orient,[status(thm)],[t25826]) ).
cnf(t9509,plain,
divide(X1,multiply(inverse(divide(multiply(multiply(inverse(X2),X3),divide(multiply(inverse(X3),X2),divide(X4,divide(Y4,Y5)))),inverse(X4))),X1)) = inverse(divide(multiply(divide(Y5,Y4),Y6),Y6)),
inference(cp,[status(thm)],[t9473,t4131]) ).
cnf(t25846,plain,
divide(X1,multiply(inverse(multiply(multiply(multiply(inverse(X2),X3),divide(multiply(inverse(X3),X2),divide(X4,divide(Y4,Y5)))),X4)),X1)) = inverse(divide(multiply(divide(Y5,Y4),Y6),Y6)),
inference(step,[status(thm)],[t9509,t7]) ).
cnf(t1017,plain,
X1 = multiply(multiply(multiply(X2,X3),divide(divide(inverse(X3),X2),divide(X4,X1))),X4),
inference(cp,[status(thm)],[t1014,t7]) ).
cnf(t1134,plain,
multiply(multiply(multiply(X1,X2),divide(divide(inverse(X2),X1),divide(X3,X4))),X3) = X4,
inference(orient,[status(thm)],[t1017]) ).
cnf(t1154,plain,
X1 = multiply(multiply(multiply(inverse(X2),X3),divide(multiply(inverse(X3),X2),divide(X4,X1))),X4),
inference(cp,[status(thm)],[t1134,t7]) ).
cnf(t1374,plain,
multiply(multiply(multiply(inverse(X1),X2),divide(multiply(inverse(X2),X1),divide(X3,X4))),X3) = X4,
inference(orient,[status(thm)],[t1154]) ).
cnf(t25847,plain,
divide(X1,multiply(inverse(divide(Y4,Y5)),X1)) = inverse(divide(multiply(divide(Y5,Y4),Y6),Y6)),
inference(step,[status(thm)],[t25846,t1374]) ).
cnf(t25848,plain,
divide(X1,multiply(inverse(divide(Y4,Y5)),X1)) = divide(c3,multiply(inverse(divide(Y4,Y5)),c3)),
inference(step,[status(thm)],[t25847,t9473]) ).
cnf(t10278,plain,
divide(X1,multiply(inverse(divide(X2,X3)),X1)) = divide(c3,multiply(inverse(divide(X2,X3)),c3)),
inference(orient,[status(thm)],[t25848]) ).
cnf(t10293,plain,
divide(c3,multiply(inverse(divide(X1,divide(divide(X2,divide(divide(X3,X4),X1)),divide(X4,X3)))),c3)) = divide(Y4,multiply(X2,Y4)),
inference(cp,[status(thm)],[t10278,t90]) ).
cnf(t25849,plain,
divide(c3,multiply(X2,c3)) = divide(Y4,multiply(X2,Y4)),
inference(step,[status(thm)],[t10293,t90]) ).
cnf(t10724,plain,
divide(c3,multiply(X1,c3)) = divide(X2,multiply(X1,X2)),
inference(orient,[status(thm)],[t25849]) ).
cnf(t10843,plain,
divide(X1,multiply(X2,X1)) = divide(X3,multiply(X2,X3)),
inference(cp,[status(thm)],[t10724,t10724]) ).
cnf(t11610,plain,
divide(X1,multiply(X2,X1)) = divide(X3,multiply(X2,X3)),
inference(orient,[status(thm)],[t10843]) ).
cnf(t11746,plain,
inverse(divide(inverse(X1),X2)) = multiply(multiply(multiply(X2,X1),divide(X3,multiply(X4,X3))),X4),
inference(cp,[status(thm)],[t1262,t11610]) ).
cnf(t12738,plain,
multiply(multiply(multiply(X1,X2),divide(X3,multiply(X4,X3))),X4) = inverse(divide(inverse(X2),X1)),
inference(orient,[status(thm)],[t11746]) ).
cnf(t1033,plain,
X1 = multiply(multiply(divide(inverse(X2),X3),divide(multiply(X3,X2),divide(X4,X1))),X4),
inference(cp,[status(thm)],[t1014,t7]) ).
cnf(t1197,plain,
multiply(multiply(divide(inverse(X1),X2),divide(multiply(X2,X1),divide(X3,X4))),X3) = X4,
inference(orient,[status(thm)],[t1033]) ).
cnf(t105,plain,
multiply(X1,divide(X2,divide(divide(X3,divide(divide(X4,Y4),X2)),divide(Y4,X4)))) = divide(X1,X3),
inference(cp,[status(thm)],[t7,t90]) ).
cnf(t273,plain,
multiply(X1,divide(X2,divide(divide(X3,divide(divide(X4,Y4),X2)),divide(Y4,X4)))) = divide(X1,X3),
inference(orient,[status(thm)],[t105]) ).
cnf(t1199,plain,
divide(X1,X2) = multiply(divide(divide(inverse(X3),X4),Y4),divide(Y4,divide(divide(X2,X1),multiply(X4,X3)))),
inference(cp,[status(thm)],[t1197,t273]) ).
cnf(t1807,plain,
multiply(divide(divide(inverse(X1),X2),X3),divide(X3,divide(divide(X4,Y4),multiply(X2,X1)))) = divide(Y4,X4),
inference(orient,[status(thm)],[t1199]) ).
cnf(t1808,plain,
divide(X1,X2) = multiply(multiply(divide(inverse(X3),X4),Y4),divide(inverse(Y4),divide(divide(X2,X1),multiply(X4,X3)))),
inference(cp,[status(thm)],[t1807,t7]) ).
cnf(t3298,plain,
multiply(multiply(divide(inverse(X1),X2),X3),divide(inverse(X3),divide(divide(X4,Y4),multiply(X2,X1)))) = divide(Y4,X4),
inference(orient,[status(thm)],[t1808]) ).
cnf(t10730,plain,
divide(multiply(X1,c3),c3) = multiply(multiply(divide(inverse(X2),X3),X4),divide(inverse(X4),divide(divide(Y4,multiply(X1,Y4)),multiply(X3,X2)))),
inference(cp,[status(thm)],[t3298,t10724]) ).
cnf(t25850,plain,
divide(multiply(X1,c3),c3) = divide(multiply(X1,Y4),Y4),
inference(step,[status(thm)],[t10730,t3298]) ).
cnf(t11099,plain,
divide(multiply(X1,c3),c3) = divide(multiply(X1,X2),X2),
inference(orient,[status(thm)],[t25850]) ).
cnf(t11225,plain,
divide(multiply(X1,c3),c3) = multiply(multiply(X1,inverse(X2)),X2),
inference(cp,[status(thm)],[t11099,t7]) ).
cnf(t11477,plain,
multiply(multiply(X1,inverse(X2)),X2) = divide(multiply(X1,c3),c3),
inference(orient,[status(thm)],[t11225]) ).
cnf(t12752,plain,
inverse(divide(inverse(inverse(divide(X1,multiply(X2,X1)))),X3)) = multiply(divide(multiply(X3,c3),c3),X2),
inference(cp,[status(thm)],[t12738,t11477]) ).
cnf(t12904,plain,
inverse(divide(inverse(inverse(divide(X1,multiply(X2,X1)))),X3)) = multiply(divide(multiply(X3,c3),c3),X2),
inference(orient,[status(thm)],[t12752]) ).
cnf(t5268,plain,
X1 = inverse(inverse(divide(X1,multiply(multiply(divide(X2,X3),multiply(divide(X3,X2),X4)),inverse(inverse(inverse(X4))))))),
inference(cp,[status(thm)],[t5239,t7]) ).
cnf(t5758,plain,
inverse(inverse(divide(X1,multiply(multiply(divide(X2,X3),multiply(divide(X3,X2),X4)),inverse(inverse(inverse(X4))))))) = X1,
inference(orient,[status(thm)],[t5268]) ).
cnf(t348,plain,
divide(inverse(X1),X2) = divide(inverse(X3),divide(multiply(inverse(X4),Y4),inverse(divide(multiply(inverse(Y4),X4),divide(X3,multiply(X2,X1)))))),
inference(cp,[status(thm)],[t341,t11]) ).
cnf(t25827,plain,
divide(inverse(X1),X2) = divide(inverse(X3),multiply(multiply(inverse(X4),Y4),divide(multiply(inverse(Y4),X4),divide(X3,multiply(X2,X1))))),
inference(step,[status(thm)],[t348,t7]) ).
cnf(t4489,plain,
divide(inverse(X1),multiply(multiply(inverse(X2),X3),divide(multiply(inverse(X3),X2),divide(X1,multiply(X4,Y4))))) = divide(inverse(Y4),X4),
inference(orient,[status(thm)],[t25827]) ).
cnf(t6997,plain,
X1 = divide(X2,multiply(multiply(divide(inverse(X3),X4),divide(divide(multiply(multiply(inverse(Y4),Y5),divide(multiply(inverse(Y5),Y4),divide(Y6,multiply(X4,X3)))),inverse(Y6)),X1)),X2)),
inference(cp,[status(thm)],[t6970,t4489]) ).
cnf(t25839,plain,
X1 = divide(X2,multiply(multiply(divide(inverse(X3),X4),divide(multiply(multiply(multiply(inverse(Y4),Y5),divide(multiply(inverse(Y5),Y4),divide(Y6,multiply(X4,X3)))),Y6),X1)),X2)),
inference(step,[status(thm)],[t6997,t7]) ).
cnf(t25840,plain,
X1 = divide(X2,multiply(multiply(divide(inverse(X3),X4),divide(multiply(X4,X3),X1)),X2)),
inference(step,[status(thm)],[t25839,t1374]) ).
cnf(t7762,plain,
divide(X1,multiply(multiply(divide(inverse(X2),X3),divide(multiply(X3,X2),X4)),X1)) = X4,
inference(orient,[status(thm)],[t25840]) ).
cnf(t11223,plain,
divide(multiply(X1,X2),X2) = divide(multiply(X1,X3),X3),
inference(cp,[status(thm)],[t11099,t11099]) ).
cnf(t11867,plain,
divide(multiply(X1,X2),X2) = divide(multiply(X1,X3),X3),
inference(orient,[status(thm)],[t11223]) ).
cnf(t11958,plain,
X1 = divide(X2,multiply(multiply(divide(inverse(X1),X3),divide(multiply(X3,X4),X4)),X2)),
inference(cp,[status(thm)],[t7762,t11867]) ).
cnf(t13562,plain,
divide(X1,multiply(multiply(divide(inverse(X2),X3),divide(multiply(X3,X4),X4)),X1)) = X2,
inference(orient,[status(thm)],[t11958]) ).
cnf(t11936,plain,
X1 = multiply(multiply(divide(inverse(divide(X2,X1)),X3),divide(multiply(X3,X4),X4)),X2),
inference(cp,[status(thm)],[t1197,t11867]) ).
cnf(t13333,plain,
multiply(multiply(divide(inverse(divide(X1,X2)),X3),divide(multiply(X3,X4),X4)),X1) = X2,
inference(orient,[status(thm)],[t11936]) ).
cnf(t13352,plain,
divide(X1,divide(X2,X3)) = multiply(multiply(X1,divide(multiply(divide(divide(X3,X2),X4),Y4),Y4)),X4),
inference(cp,[status(thm)],[t13333,t2]) ).
cnf(t14933,plain,
multiply(multiply(X1,divide(multiply(divide(divide(X2,X3),X4),Y4),Y4)),X4) = divide(X1,divide(X3,X2)),
inference(orient,[status(thm)],[t13352]) ).
cnf(t15071,plain,
X1 = divide(X2,divide(divide(inverse(X1),divide(divide(X3,X4),X2)),divide(X4,X3))),
inference(cp,[status(thm)],[t13562,t14933]) ).
cnf(t16302,plain,
divide(X1,divide(divide(inverse(X2),divide(divide(X3,X4),X1)),divide(X4,X3))) = X2,
inference(orient,[status(thm)],[t15071]) ).
cnf(t16491,plain,
X1 = divide(divide(X2,X3),divide(X4,divide(divide(divide(X3,X2),inverse(X1)),inverse(X4)))),
inference(cp,[status(thm)],[t16302,t16302]) ).
cnf(t25853,plain,
X1 = divide(divide(X2,X3),divide(X4,multiply(divide(divide(X3,X2),inverse(X1)),X4))),
inference(step,[status(thm)],[t16491,t7]) ).
cnf(t25854,plain,
X1 = divide(divide(X2,X3),divide(X4,multiply(multiply(divide(X3,X2),X1),X4))),
inference(step,[status(thm)],[t25853,t7]) ).
cnf(t16667,plain,
divide(divide(X1,X2),divide(X3,multiply(multiply(divide(X2,X1),X4),X3))) = X4,
inference(orient,[status(thm)],[t25854]) ).
cnf(t11625,plain,
divide(X1,multiply(multiply(X2,inverse(X3)),X1)) = divide(X3,divide(multiply(X2,c3),c3)),
inference(cp,[status(thm)],[t11610,t11477]) ).
cnf(t12122,plain,
divide(X1,multiply(multiply(X2,inverse(X3)),X1)) = divide(X3,divide(multiply(X2,c3),c3)),
inference(orient,[status(thm)],[t11625]) ).
cnf(t16712,plain,
inverse(X1) = divide(divide(X2,X3),divide(X1,divide(multiply(divide(X3,X2),c3),c3))),
inference(cp,[status(thm)],[t16667,t12122]) ).
cnf(t16983,plain,
divide(divide(X1,X2),divide(X3,divide(multiply(divide(X2,X1),c3),c3))) = inverse(X3),
inference(orient,[status(thm)],[t16712]) ).
cnf(t17035,plain,
inverse(X1) = divide(divide(X2,X3),divide(X1,divide(multiply(divide(X3,X2),X4),X4))),
inference(cp,[status(thm)],[t16983,t11867]) ).
cnf(t17276,plain,
divide(divide(X1,X2),divide(X3,divide(multiply(divide(X2,X1),X4),X4))) = inverse(X3),
inference(orient,[status(thm)],[t17035]) ).
cnf(t14935,plain,
divide(divide(inverse(divide(X1,X2)),divide(divide(X3,X4),X1)),divide(X4,X3)) = X2,
inference(cp,[status(thm)],[t14933,t13333]) ).
cnf(t15141,plain,
divide(divide(inverse(divide(X1,X2)),divide(divide(X3,X4),X1)),divide(X4,X3)) = X2,
inference(orient,[status(thm)],[t14935]) ).
cnf(t17321,plain,
inverse(divide(inverse(divide(X1,X2)),divide(divide(X3,multiply(divide(X4,Y4),X3)),X1))) = divide(divide(Y4,X4),X2),
inference(cp,[status(thm)],[t17276,t15141]) ).
cnf(t10,plain,
X1 = divide(inverse(divide(X2,divide(X1,divide(inverse(X3),X4)))),divide(multiply(X4,X3),X2)),
inference(cp,[status(thm)],[t2,t7]) ).
cnf(t39,plain,
divide(inverse(divide(X1,divide(X2,divide(inverse(X3),X4)))),divide(multiply(X4,X3),X1)) = X2,
inference(orient,[status(thm)],[t10]) ).
cnf(t48,plain,
inverse(divide(X1,divide(X2,divide(inverse(X3),X4)))) = divide(inverse(divide(Y4,X2)),divide(divide(X1,multiply(X4,X3)),Y4)),
inference(cp,[status(thm)],[t2,t39]) ).
cnf(t168,plain,
divide(inverse(divide(X1,X2)),divide(divide(X3,multiply(X4,Y4)),X1)) = inverse(divide(X3,divide(X2,divide(inverse(Y4),X4)))),
inference(orient,[status(thm)],[t48]) ).
cnf(t25855,plain,
inverse(inverse(divide(X3,divide(X2,divide(inverse(X3),divide(X4,Y4)))))) = divide(divide(Y4,X4),X2),
inference(step,[status(thm)],[t17321,t168]) ).
cnf(t17597,plain,
inverse(inverse(divide(X1,divide(X2,divide(inverse(X1),divide(X3,X4)))))) = divide(divide(X4,X3),X2),
inference(orient,[status(thm)],[t25855]) ).
cnf(t17605,plain,
divide(divide(divide(X1,X2),inverse(divide(divide(X2,X1),inverse(X3)))),inverse(inverse(X4))) = inverse(inverse(divide(X3,X4))),
inference(cp,[status(thm)],[t17597,t6490]) ).
cnf(t25856,plain,
multiply(divide(divide(X1,X2),inverse(divide(divide(X2,X1),inverse(X3)))),inverse(X4)) = inverse(inverse(divide(X3,X4))),
inference(step,[status(thm)],[t17605,t7]) ).
cnf(t25857,plain,
multiply(multiply(divide(X1,X2),divide(divide(X2,X1),inverse(X3))),inverse(X4)) = inverse(inverse(divide(X3,X4))),
inference(step,[status(thm)],[t25856,t7]) ).
cnf(t25858,plain,
multiply(multiply(divide(X1,X2),multiply(divide(X2,X1),X3)),inverse(X4)) = inverse(inverse(divide(X3,X4))),
inference(step,[status(thm)],[t25857,t7]) ).
cnf(t17827,plain,
multiply(multiply(divide(X1,X2),multiply(divide(X2,X1),X3)),inverse(X4)) = inverse(inverse(divide(X3,X4))),
inference(orient,[status(thm)],[t25858]) ).
cnf(t25859,plain,
inverse(inverse(divide(X1,inverse(inverse(divide(X4,inverse(inverse(X4)))))))) = X1,
inference(step,[status(thm)],[t5758,t17827]) ).
cnf(t25860,plain,
inverse(inverse(multiply(X1,inverse(divide(X4,inverse(inverse(X4))))))) = X1,
inference(step,[status(thm)],[t25859,t7]) ).
cnf(t25861,plain,
inverse(inverse(multiply(X1,inverse(multiply(X4,inverse(X4)))))) = X1,
inference(step,[status(thm)],[t25860,t7]) ).
cnf(t18061,plain,
inverse(inverse(multiply(X1,inverse(multiply(X4,inverse(X4)))))) = X1,
inference(rw,[status(thm)],[t25861]) ).
cnf(t18462,plain,
inverse(inverse(multiply(X1,inverse(multiply(X2,inverse(X2)))))) = X1,
inference(orient,[status(thm)],[t18061]) ).
cnf(t18470,plain,
multiply(X1,inverse(inverse(multiply(X2,inverse(X2))))) = inverse(inverse(divide(multiply(X1,c3),c3))),
inference(cp,[status(thm)],[t18462,t11477]) ).
cnf(t19325,plain,
multiply(X1,inverse(inverse(multiply(X2,inverse(X2))))) = inverse(inverse(divide(multiply(X1,c3),c3))),
inference(orient,[status(thm)],[t18470]) ).
cnf(t19485,plain,
multiply(divide(multiply(X1,c3),c3),X2) = inverse(divide(inverse(inverse(divide(inverse(inverse(multiply(X3,inverse(X3)))),inverse(inverse(divide(multiply(X2,c3),c3)))))),X1)),
inference(cp,[status(thm)],[t12904,t19325]) ).
cnf(t25866,plain,
multiply(divide(multiply(X1,c3),c3),X2) = inverse(divide(inverse(inverse(multiply(inverse(inverse(multiply(X3,inverse(X3)))),inverse(divide(multiply(X2,c3),c3))))),X1)),
inference(step,[status(thm)],[t19485,t7]) ).
cnf(t18006,plain,
inverse(X1) = divide(inverse(X2),inverse(inverse(divide(X1,X2)))),
inference(cp,[status(thm)],[t7230,t17827]) ).
cnf(t25862,plain,
inverse(X1) = multiply(inverse(X2),inverse(divide(X1,X2))),
inference(step,[status(thm)],[t18006,t7]) ).
cnf(t18062,plain,
multiply(inverse(X1),inverse(divide(X2,X1))) = inverse(X2),
inference(orient,[status(thm)],[t25862]) ).
cnf(t18158,plain,
inverse(multiply(X1,X2)) = multiply(inverse(X2),inverse(divide(multiply(X1,X3),X3))),
inference(cp,[status(thm)],[t18062,t11867]) ).
cnf(t18852,plain,
multiply(inverse(X1),inverse(divide(multiply(X2,X3),X3))) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t18158]) ).
cnf(t25867,plain,
multiply(divide(multiply(X1,c3),c3),X2) = inverse(divide(inverse(inverse(inverse(multiply(X2,inverse(multiply(X3,inverse(X3))))))),X1)),
inference(step,[status(thm)],[t25866,t18852]) ).
cnf(t25868,plain,
multiply(divide(multiply(X1,c3),c3),X2) = inverse(divide(inverse(X2),X1)),
inference(step,[status(thm)],[t25867,t18462]) ).
cnf(t19554,plain,
multiply(divide(multiply(X1,c3),c3),X2) = inverse(divide(inverse(X2),X1)),
inference(orient,[status(thm)],[t25868]) ).
cnf(t275,plain,
divide(X1,X2) = multiply(X1,inverse(divide(X2,divide(X3,divide(inverse(divide(divide(X4,Y4),X3)),divide(Y4,X4)))))),
inference(cp,[status(thm)],[t273,t59]) ).
cnf(t2973,plain,
multiply(X1,inverse(divide(X2,divide(X3,divide(inverse(divide(divide(X4,Y4),X3)),divide(Y4,X4)))))) = divide(X1,X2),
inference(orient,[status(thm)],[t275]) ).
cnf(t5223,plain,
divide(X1,X2) = multiply(X1,inverse(divide(X2,divide(multiply(divide(X3,X4),divide(divide(X4,X3),Y4)),inverse(inverse(inverse(Y4))))))),
inference(cp,[status(thm)],[t2973,t4973]) ).
cnf(t25832,plain,
divide(X1,X2) = multiply(X1,inverse(divide(X2,multiply(multiply(divide(X3,X4),divide(divide(X4,X3),Y4)),inverse(inverse(Y4)))))),
inference(step,[status(thm)],[t5223,t7]) ).
cnf(t5944,plain,
multiply(X1,inverse(divide(X2,multiply(multiply(divide(X3,X4),divide(divide(X4,X3),Y4)),inverse(inverse(Y4)))))) = divide(X1,X2),
inference(orient,[status(thm)],[t25832]) ).
cnf(t19569,plain,
inverse(divide(inverse(inverse(divide(X1,multiply(multiply(divide(X2,X3),divide(divide(X3,X2),X4)),inverse(inverse(X4)))))),Y4)) = divide(divide(multiply(Y4,c3),c3),X1),
inference(cp,[status(thm)],[t19554,t5944]) ).
cnf(t25885,plain,
inverse(divide(X1,Y4)) = divide(divide(multiply(Y4,c3),c3),X1),
inference(step,[status(thm)],[t19569,t5239]) ).
cnf(t19717,plain,
divide(divide(multiply(X1,c3),c3),X2) = inverse(divide(X2,X1)),
inference(orient,[status(thm)],[t25885]) ).
cnf(t19738,plain,
inverse(divide(X1,X2)) = divide(divide(multiply(X2,X3),X3),X1),
inference(cp,[status(thm)],[t19717,t11867]) ).
cnf(t20019,plain,
divide(divide(multiply(X1,X2),X2),X3) = inverse(divide(X3,X1)),
inference(orient,[status(thm)],[t19738]) ).
cnf(t15329,plain,
X1 = multiply(multiply(divide(divide(divide(X1,X2),X3),inverse(divide(X3,X4))),X4),X2),
inference(cp,[status(thm)],[t1014,t15141]) ).
cnf(t25851,plain,
X1 = multiply(multiply(multiply(divide(divide(X1,X2),X3),divide(X3,X4)),X4),X2),
inference(step,[status(thm)],[t15329,t7]) ).
cnf(t15482,plain,
multiply(multiply(multiply(divide(divide(X1,X2),X3),divide(X3,X4)),X4),X2) = X1,
inference(orient,[status(thm)],[t25851]) ).
cnf(t15484,plain,
X1 = divide(multiply(multiply(divide(divide(X1,X2),X3),divide(X3,inverse(X2))),c3),c3),
inference(cp,[status(thm)],[t15482,t11477]) ).
cnf(t25852,plain,
X1 = divide(multiply(multiply(divide(divide(X1,X2),X3),multiply(X3,X2)),c3),c3),
inference(step,[status(thm)],[t15484,t7]) ).
cnf(t15724,plain,
divide(multiply(multiply(divide(divide(X1,X2),X3),multiply(X3,X2)),c3),c3) = X1,
inference(orient,[status(thm)],[t25852]) ).
cnf(t15725,plain,
X1 = divide(multiply(multiply(divide(divide(X1,X2),X3),multiply(X3,X2)),X4),X4),
inference(cp,[status(thm)],[t15724,t11867]) ).
cnf(t15958,plain,
divide(multiply(multiply(divide(divide(X1,X2),X3),multiply(X3,X2)),X4),X4) = X1,
inference(orient,[status(thm)],[t15725]) ).
cnf(t18542,plain,
X1 = divide(inverse(inverse(X1)),multiply(multiply(divide(X2,X3),divide(divide(X3,X2),multiply(X4,inverse(multiply(Y4,inverse(Y4)))))),X4)),
inference(cp,[status(thm)],[t6243,t18462]) ).
cnf(t25863,plain,
X1 = divide(inverse(inverse(X1)),inverse(inverse(multiply(Y4,inverse(Y4))))),
inference(step,[status(thm)],[t18542,t1082]) ).
cnf(t25864,plain,
X1 = multiply(inverse(inverse(X1)),inverse(multiply(Y4,inverse(Y4)))),
inference(step,[status(thm)],[t25863,t7]) ).
cnf(t18653,plain,
multiply(inverse(inverse(X1)),inverse(multiply(X2,inverse(X2)))) = X1,
inference(orient,[status(thm)],[t25864]) ).
cnf(t19430,plain,
inverse(X1) = divide(inverse(inverse(multiply(X2,inverse(X2)))),inverse(inverse(divide(multiply(multiply(divide(X3,X4),multiply(divide(X4,X3),X1)),c3),c3)))),
inference(cp,[status(thm)],[t7230,t19325]) ).
cnf(t25902,plain,
inverse(X1) = multiply(inverse(inverse(multiply(X2,inverse(X2)))),inverse(divide(multiply(multiply(divide(X3,X4),multiply(divide(X4,X3),X1)),c3),c3))),
inference(step,[status(thm)],[t19430,t7]) ).
cnf(t25903,plain,
inverse(X1) = inverse(multiply(multiply(divide(X3,X4),multiply(divide(X4,X3),X1)),inverse(multiply(X2,inverse(X2))))),
inference(step,[status(thm)],[t25902,t18852]) ).
cnf(t25904,plain,
inverse(X1) = inverse(inverse(inverse(divide(X1,multiply(X2,inverse(X2)))))),
inference(step,[status(thm)],[t25903,t17827]) ).
cnf(t11882,plain,
divide(multiply(multiply(X1,inverse(X2)),X3),X3) = divide(divide(multiply(X1,c3),c3),X2),
inference(cp,[status(thm)],[t11867,t11477]) ).
cnf(t12395,plain,
divide(multiply(multiply(X1,inverse(X2)),X3),X3) = divide(divide(multiply(X1,c3),c3),X2),
inference(orient,[status(thm)],[t11882]) ).
cnf(t25886,plain,
divide(multiply(multiply(X1,inverse(X2)),X3),X3) = inverse(divide(X2,X1)),
inference(step,[status(thm)],[t12395,t19717]) ).
cnf(t19718,plain,
divide(multiply(multiply(X1,inverse(X2)),X3),X3) = inverse(divide(X2,X1)),
inference(orient,[status(thm)],[t25886]) ).
cnf(t20037,plain,
inverse(divide(X1,multiply(X2,inverse(X3)))) = divide(inverse(divide(X3,X2)),X1),
inference(cp,[status(thm)],[t20019,t19718]) ).
cnf(t20558,plain,
inverse(divide(X1,multiply(X2,inverse(X3)))) = divide(inverse(divide(X3,X2)),X1),
inference(orient,[status(thm)],[t20037]) ).
cnf(t25905,plain,
inverse(X1) = inverse(inverse(divide(inverse(divide(X2,X2)),X1))),
inference(step,[status(thm)],[t25904,t20558]) ).
cnf(t21909,plain,
inverse(inverse(divide(inverse(divide(X1,X1)),X2))) = inverse(X2),
inference(orient,[status(thm)],[t25905]) ).
cnf(t21978,plain,
inverse(divide(inverse(divide(X1,X1)),X2)) = multiply(inverse(inverse(X2)),inverse(multiply(X3,inverse(X3)))),
inference(cp,[status(thm)],[t18653,t21909]) ).
cnf(t25906,plain,
inverse(divide(inverse(divide(X1,X1)),X2)) = X2,
inference(step,[status(thm)],[t21978,t18653]) ).
cnf(t22110,plain,
inverse(divide(inverse(divide(X1,X1)),X2)) = X2,
inference(orient,[status(thm)],[t25906]) ).
cnf(t22148,plain,
inverse(X1) = inverse(multiply(inverse(divide(X2,X2)),X1)),
inference(cp,[status(thm)],[t22110,t7]) ).
cnf(t22328,plain,
inverse(multiply(inverse(divide(X1,X1)),X2)) = inverse(X2),
inference(orient,[status(thm)],[t22148]) ).
cnf(t22346,plain,
multiply(inverse(divide(X1,X1)),X2) = multiply(inverse(inverse(X2)),inverse(multiply(X3,inverse(X3)))),
inference(cp,[status(thm)],[t18653,t22328]) ).
cnf(t25907,plain,
multiply(inverse(divide(X1,X1)),X2) = X2,
inference(step,[status(thm)],[t22346,t18653]) ).
cnf(t22481,plain,
multiply(inverse(divide(X1,X1)),X2) = X2,
inference(orient,[status(thm)],[t25907]) ).
cnf(t22505,plain,
divide(multiply(inverse(divide(X1,X1)),c3),c3) = multiply(inverse(X2),X2),
inference(cp,[status(thm)],[t11477,t22481]) ).
cnf(t25908,plain,
divide(c3,c3) = multiply(inverse(X2),X2),
inference(step,[status(thm)],[t22505,t22481]) ).
cnf(t22631,plain,
multiply(inverse(X1),X1) = divide(c3,c3),
inference(orient,[status(thm)],[t25908]) ).
cnf(t22633,plain,
divide(c3,c3) = multiply(X1,inverse(X1)),
inference(cp,[status(thm)],[t22631,t18653]) ).
cnf(t23122,plain,
multiply(X1,inverse(X1)) = divide(c3,c3),
inference(orient,[status(thm)],[t22633]) ).
cnf(t23202,plain,
X1 = divide(multiply(multiply(divide(divide(X1,inverse(X2)),X2),divide(c3,c3)),X3),X3),
inference(cp,[status(thm)],[t15958,t23122]) ).
cnf(t25913,plain,
X1 = divide(multiply(multiply(divide(multiply(X1,X2),X2),divide(c3,c3)),X3),X3),
inference(step,[status(thm)],[t23202,t7]) ).
cnf(t19584,plain,
inverse(divide(inverse(X1),X2)) = multiply(divide(multiply(X2,X3),X3),X1),
inference(cp,[status(thm)],[t19554,t11867]) ).
cnf(t20375,plain,
multiply(divide(multiply(X1,X2),X2),X3) = inverse(divide(inverse(X3),X1)),
inference(orient,[status(thm)],[t19584]) ).
cnf(t25914,plain,
X1 = divide(multiply(inverse(divide(inverse(divide(c3,c3)),X1)),X3),X3),
inference(step,[status(thm)],[t25913,t20375]) ).
cnf(t25915,plain,
X1 = divide(multiply(X1,X3),X3),
inference(step,[status(thm)],[t25914,t22110]) ).
cnf(t23334,plain,
divide(multiply(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t25915]) ).
cnf(t25922,plain,
divide(X1,X3) = inverse(divide(X3,X1)),
inference(step,[status(thm)],[t20019,t23334]) ).
cnf(t23613,plain,
divide(X1,X3) = inverse(divide(X3,X1)),
inference(rw,[status(thm)],[t25922]) ).
cnf(t23866,plain,
inverse(divide(X1,X2)) = divide(X2,X1),
inference(orient,[status(thm)],[t23613]) ).
cnf(t23894,plain,
divide(X1,multiply(X2,X1)) = inverse(X2),
inference(cp,[status(thm)],[t23866,t23334]) ).
cnf(t24704,plain,
divide(X1,multiply(X2,X1)) = inverse(X2),
inference(orient,[status(thm)],[t23894]) ).
cnf(t25926,plain,
multiply(divide(divide(X1,X2),X3),multiply(X3,X2)) = X1,
inference(step,[status(thm)],[t15958,t23334]) ).
cnf(t23617,plain,
multiply(divide(divide(X1,X2),X3),multiply(X3,X2)) = X1,
inference(rw,[status(thm)],[t25926]) ).
cnf(t25728,plain,
multiply(divide(divide(X1,X2),X3),multiply(X3,X2)) = X1,
inference(orient,[status(thm)],[t23617]) ).
cnf(t25752,plain,
inverse(divide(divide(X1,X2),X3)) = divide(multiply(X3,X2),X1),
inference(cp,[status(thm)],[t24704,t25728]) ).
cnf(t26127,plain,
divide(X3,divide(X1,X2)) = divide(multiply(X3,X2),X1),
inference(step,[status(thm)],[t25752,t23866]) ).
cnf(t23900,plain,
multiply(X1,divide(X2,X3)) = divide(X1,divide(X3,X2)),
inference(cp,[status(thm)],[t7,t23866]) ).
cnf(t25591,plain,
divide(X1,divide(X2,X3)) = multiply(X1,divide(X3,X2)),
inference(orient,[status(thm)],[t23900]) ).
cnf(t26128,plain,
multiply(X3,divide(X2,X1)) = divide(multiply(X3,X2),X1),
inference(step,[status(thm)],[t26127,t25591]) ).
cnf(t25764,plain,
divide(multiply(X1,X2),X3) = multiply(X1,divide(X2,X3)),
inference(orient,[status(thm)],[t26128]) ).
cnf(t25768,plain,
multiply(X1,divide(X2,inverse(X3))) = multiply(multiply(X1,X2),X3),
inference(cp,[status(thm)],[t25764,t7]) ).
cnf(t26131,plain,
multiply(X1,multiply(X2,X3)) = multiply(multiply(X1,X2),X3),
inference(step,[status(thm)],[t25768,t7]) ).
cnf(t25797,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t26131]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)),
inference(rw,[status(thm)],[goal_0,t25797]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP471-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/1.11 % Computer : n008.cluster.edu
% 0.09/1.11 % Model : x86_64 x86_64
% 0.09/1.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/1.11 % Memory : 8046.5625MB
% 0.09/1.11 % OS : Linux 6.8.0-71-generic
% 0.09/1.12 % CPULimit : 300
% 0.09/1.12 % WCLimit : 300
% 0.09/1.12 % DateTime : Wed Sep 23 14:51:40 UTC 2026
% 0.09/1.12 % CPUTime :
% 0.09/1.12 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 15.46/3.12 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.46/3.12 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------