%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP469-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 : n012.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:56 PM UTC 2026
% Result : Unsatisfiable 7.72s 6.37s
% Output : CNFRefutation 7.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 108
% Number of leaves : 3
% Syntax : Number of clauses : 199 ( 199 unt; 0 nHn; 4 RR)
% Number of literals : 199 ( 198 equ; 3 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 : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 745 ( 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(t22705,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(t22706,plain,
multiply(multiply(divide(X1,X2),divide(divide(X2,X1),divide(X3,divide(X4,Y4)))),X3) = divide(X4,Y4),
inference(step,[status(thm)],[t22705,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)],[t22706]) ).
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(t22707,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)],[t22707]) ).
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(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(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(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(t22718,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)],[t22718]) ).
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(t22719,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)],[t22719]) ).
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(t22723,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(t22724,plain,
X1 = divide(inverse(inverse(X1)),multiply(multiply(divide(X2,X3),divide(divide(X3,X2),X4)),inverse(inverse(X4)))),
inference(step,[status(thm)],[t22723,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)],[t22724]) ).
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(t22725,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)],[t22725]) ).
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(t22726,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(t22727,plain,
X1 = divide(inverse(X2),multiply(multiply(divide(X3,X4),divide(divide(X4,X3),X1)),inverse(X2))),
inference(step,[status(thm)],[t22726,t7]) ).
cnf(t6738,plain,
divide(inverse(X1),multiply(multiply(divide(X2,X3),divide(divide(X3,X2),X4)),inverse(X1))) = X4,
inference(orient,[status(thm)],[t22727]) ).
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(t22728,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)],[t22728]) ).
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(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(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(t22734,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)],[t22734]) ).
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(t22716,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)],[t22716]) ).
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(t22736,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(t22737,plain,
divide(X1,multiply(inverse(divide(Y4,Y5)),X1)) = inverse(divide(multiply(divide(Y5,Y4),Y6),Y6)),
inference(step,[status(thm)],[t22736,t1374]) ).
cnf(t22738,plain,
divide(X1,multiply(inverse(divide(Y4,Y5)),X1)) = divide(b1,multiply(inverse(divide(Y4,Y5)),b1)),
inference(step,[status(thm)],[t22737,t9473]) ).
cnf(t10278,plain,
divide(X1,multiply(inverse(divide(X2,X3)),X1)) = divide(b1,multiply(inverse(divide(X2,X3)),b1)),
inference(orient,[status(thm)],[t22738]) ).
cnf(t10293,plain,
divide(b1,multiply(inverse(divide(X1,divide(divide(X2,divide(divide(X3,X4),X1)),divide(X4,X3)))),b1)) = divide(Y4,multiply(X2,Y4)),
inference(cp,[status(thm)],[t10278,t90]) ).
cnf(t22739,plain,
divide(b1,multiply(X2,b1)) = divide(Y4,multiply(X2,Y4)),
inference(step,[status(thm)],[t10293,t90]) ).
cnf(t10724,plain,
divide(b1,multiply(X1,b1)) = divide(X2,multiply(X1,X2)),
inference(orient,[status(thm)],[t22739]) ).
cnf(t10730,plain,
divide(multiply(X1,b1),b1) = 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(t22740,plain,
divide(multiply(X1,b1),b1) = divide(multiply(X1,Y4),Y4),
inference(step,[status(thm)],[t10730,t3298]) ).
cnf(t11099,plain,
divide(multiply(X1,b1),b1) = divide(multiply(X1,X2),X2),
inference(orient,[status(thm)],[t22740]) ).
cnf(t11225,plain,
divide(multiply(X1,b1),b1) = multiply(multiply(X1,inverse(X2)),X2),
inference(cp,[status(thm)],[t11099,t7]) ).
cnf(t11477,plain,
multiply(multiply(X1,inverse(X2)),X2) = divide(multiply(X1,b1),b1),
inference(orient,[status(thm)],[t11225]) ).
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(t22717,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)],[t22717]) ).
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(t22729,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(t22730,plain,
X1 = divide(X2,multiply(multiply(divide(inverse(X3),X4),divide(multiply(X4,X3),X1)),X2)),
inference(step,[status(thm)],[t22729,t1374]) ).
cnf(t7762,plain,
divide(X1,multiply(multiply(divide(inverse(X2),X3),divide(multiply(X3,X2),X4)),X1)) = X4,
inference(orient,[status(thm)],[t22730]) ).
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(t22743,plain,
X1 = divide(divide(X2,X3),divide(X4,multiply(divide(divide(X3,X2),inverse(X1)),X4))),
inference(step,[status(thm)],[t16491,t7]) ).
cnf(t22744,plain,
X1 = divide(divide(X2,X3),divide(X4,multiply(multiply(divide(X3,X2),X1),X4))),
inference(step,[status(thm)],[t22743,t7]) ).
cnf(t16667,plain,
divide(divide(X1,X2),divide(X3,multiply(multiply(divide(X2,X1),X4),X3))) = X4,
inference(orient,[status(thm)],[t22744]) ).
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(t11625,plain,
divide(X1,multiply(multiply(X2,inverse(X3)),X1)) = divide(X3,divide(multiply(X2,b1),b1)),
inference(cp,[status(thm)],[t11610,t11477]) ).
cnf(t12122,plain,
divide(X1,multiply(multiply(X2,inverse(X3)),X1)) = divide(X3,divide(multiply(X2,b1),b1)),
inference(orient,[status(thm)],[t11625]) ).
cnf(t16712,plain,
inverse(X1) = divide(divide(X2,X3),divide(X1,divide(multiply(divide(X3,X2),b1),b1))),
inference(cp,[status(thm)],[t16667,t12122]) ).
cnf(t16983,plain,
divide(divide(X1,X2),divide(X3,divide(multiply(divide(X2,X1),b1),b1))) = 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(t22745,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)],[t22745]) ).
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(t22746,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(t22747,plain,
multiply(multiply(divide(X1,X2),divide(divide(X2,X1),inverse(X3))),inverse(X4)) = inverse(inverse(divide(X3,X4))),
inference(step,[status(thm)],[t22746,t7]) ).
cnf(t22748,plain,
multiply(multiply(divide(X1,X2),multiply(divide(X2,X1),X3)),inverse(X4)) = inverse(inverse(divide(X3,X4))),
inference(step,[status(thm)],[t22747,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)],[t22748]) ).
cnf(t22749,plain,
inverse(inverse(divide(X1,inverse(inverse(divide(X4,inverse(inverse(X4)))))))) = X1,
inference(step,[status(thm)],[t5758,t17827]) ).
cnf(t22750,plain,
inverse(inverse(multiply(X1,inverse(divide(X4,inverse(inverse(X4))))))) = X1,
inference(step,[status(thm)],[t22749,t7]) ).
cnf(t22751,plain,
inverse(inverse(multiply(X1,inverse(multiply(X4,inverse(X4)))))) = X1,
inference(step,[status(thm)],[t22750,t7]) ).
cnf(t18061,plain,
inverse(inverse(multiply(X1,inverse(multiply(X4,inverse(X4)))))) = X1,
inference(rw,[status(thm)],[t22751]) ).
cnf(t18462,plain,
inverse(inverse(multiply(X1,inverse(multiply(X2,inverse(X2)))))) = X1,
inference(orient,[status(thm)],[t18061]) ).
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(t22753,plain,
X1 = divide(inverse(inverse(X1)),inverse(inverse(multiply(Y4,inverse(Y4))))),
inference(step,[status(thm)],[t18542,t1082]) ).
cnf(t22754,plain,
X1 = multiply(inverse(inverse(X1)),inverse(multiply(Y4,inverse(Y4)))),
inference(step,[status(thm)],[t22753,t7]) ).
cnf(t18653,plain,
multiply(inverse(inverse(X1)),inverse(multiply(X2,inverse(X2)))) = X1,
inference(orient,[status(thm)],[t22754]) ).
cnf(t18470,plain,
multiply(X1,inverse(inverse(multiply(X2,inverse(X2))))) = inverse(inverse(divide(multiply(X1,b1),b1))),
inference(cp,[status(thm)],[t18462,t11477]) ).
cnf(t19325,plain,
multiply(X1,inverse(inverse(multiply(X2,inverse(X2))))) = inverse(inverse(divide(multiply(X1,b1),b1))),
inference(orient,[status(thm)],[t18470]) ).
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)),b1),b1)))),
inference(cp,[status(thm)],[t7230,t19325]) ).
cnf(t22792,plain,
inverse(X1) = multiply(inverse(inverse(multiply(X2,inverse(X2)))),inverse(divide(multiply(multiply(divide(X3,X4),multiply(divide(X4,X3),X1)),b1),b1))),
inference(step,[status(thm)],[t19430,t7]) ).
cnf(t18006,plain,
inverse(X1) = divide(inverse(X2),inverse(inverse(divide(X1,X2)))),
inference(cp,[status(thm)],[t7230,t17827]) ).
cnf(t22752,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)],[t22752]) ).
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(t22793,plain,
inverse(X1) = inverse(multiply(multiply(divide(X3,X4),multiply(divide(X4,X3),X1)),inverse(multiply(X2,inverse(X2))))),
inference(step,[status(thm)],[t22792,t18852]) ).
cnf(t22794,plain,
inverse(X1) = inverse(inverse(inverse(divide(X1,multiply(X2,inverse(X2)))))),
inference(step,[status(thm)],[t22793,t17827]) ).
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(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(t12752,plain,
inverse(divide(inverse(inverse(divide(X1,multiply(X2,X1)))),X3)) = multiply(divide(multiply(X3,b1),b1),X2),
inference(cp,[status(thm)],[t12738,t11477]) ).
cnf(t12904,plain,
inverse(divide(inverse(inverse(divide(X1,multiply(X2,X1)))),X3)) = multiply(divide(multiply(X3,b1),b1),X2),
inference(orient,[status(thm)],[t12752]) ).
cnf(t19485,plain,
multiply(divide(multiply(X1,b1),b1),X2) = inverse(divide(inverse(inverse(divide(inverse(inverse(multiply(X3,inverse(X3)))),inverse(inverse(divide(multiply(X2,b1),b1)))))),X1)),
inference(cp,[status(thm)],[t12904,t19325]) ).
cnf(t22756,plain,
multiply(divide(multiply(X1,b1),b1),X2) = inverse(divide(inverse(inverse(multiply(inverse(inverse(multiply(X3,inverse(X3)))),inverse(divide(multiply(X2,b1),b1))))),X1)),
inference(step,[status(thm)],[t19485,t7]) ).
cnf(t22757,plain,
multiply(divide(multiply(X1,b1),b1),X2) = inverse(divide(inverse(inverse(inverse(multiply(X2,inverse(multiply(X3,inverse(X3))))))),X1)),
inference(step,[status(thm)],[t22756,t18852]) ).
cnf(t22758,plain,
multiply(divide(multiply(X1,b1),b1),X2) = inverse(divide(inverse(X2),X1)),
inference(step,[status(thm)],[t22757,t18462]) ).
cnf(t19554,plain,
multiply(divide(multiply(X1,b1),b1),X2) = inverse(divide(inverse(X2),X1)),
inference(orient,[status(thm)],[t22758]) ).
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(t22722,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)],[t22722]) ).
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,b1),b1),X1),
inference(cp,[status(thm)],[t19554,t5944]) ).
cnf(t22775,plain,
inverse(divide(X1,Y4)) = divide(divide(multiply(Y4,b1),b1),X1),
inference(step,[status(thm)],[t19569,t5239]) ).
cnf(t19717,plain,
divide(divide(multiply(X1,b1),b1),X2) = inverse(divide(X2,X1)),
inference(orient,[status(thm)],[t22775]) ).
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(t11882,plain,
divide(multiply(multiply(X1,inverse(X2)),X3),X3) = divide(divide(multiply(X1,b1),b1),X2),
inference(cp,[status(thm)],[t11867,t11477]) ).
cnf(t12395,plain,
divide(multiply(multiply(X1,inverse(X2)),X3),X3) = divide(divide(multiply(X1,b1),b1),X2),
inference(orient,[status(thm)],[t11882]) ).
cnf(t22776,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)],[t22776]) ).
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(t22795,plain,
inverse(X1) = inverse(inverse(divide(inverse(divide(X2,X2)),X1))),
inference(step,[status(thm)],[t22794,t20558]) ).
cnf(t21909,plain,
inverse(inverse(divide(inverse(divide(X1,X1)),X2))) = inverse(X2),
inference(orient,[status(thm)],[t22795]) ).
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(t22796,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)],[t22796]) ).
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(t22797,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)],[t22797]) ).
cnf(t22505,plain,
divide(multiply(inverse(divide(X1,X1)),b1),b1) = multiply(inverse(X2),X2),
inference(cp,[status(thm)],[t11477,t22481]) ).
cnf(t22798,plain,
divide(b1,b1) = multiply(inverse(X2),X2),
inference(step,[status(thm)],[t22505,t22481]) ).
cnf(t22631,plain,
multiply(inverse(X1),X1) = divide(b1,b1),
inference(orient,[status(thm)],[t22798]) ).
cnf(goal_0,negated_conjecture,
multiply(inverse(b1),b1) != multiply(inverse(a1),a1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
divide(b1,b1) != multiply(inverse(a1),a1),
inference(rw,[status(thm)],[goal_0,t22631]) ).
cnf(g0_1,plain,
divide(b1,b1) != divide(b1,b1),
inference(rw,[status(thm)],[g0_0,t22631]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP469-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.03/5.32 % Computer : n012.cluster.edu
% 0.03/5.32 % Model : x86_64 x86_64
% 0.03/5.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/5.32 % Memory : 8046.5625MB
% 0.03/5.32 % OS : Linux 6.8.0-71-generic
% 0.03/5.32 % CPULimit : 300
% 0.03/5.32 % WCLimit : 300
% 0.03/5.32 % DateTime : Wed Sep 23 14:50:00 UTC 2026
% 0.03/5.32 % CPUTime :
% 0.03/5.32 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.72/6.37 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.72/6.37 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------