%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP567-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 : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:27:33 PM UTC 2026
% Result : Unsatisfiable 6.10s 1.19s
% Output : CNFRefutation 6.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 59
% Number of leaves : 13
% Syntax : Number of clauses : 161 ( 161 unt; 0 nHn; 79 RR)
% Number of literals : 161 ( 160 equ; 12 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 12 con; 0-2 aty)
% Number of variables : 122 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t2,axiom,
sF0 = double_divide(c3,b3),
introduced(definition) ).
cnf(t10,plain,
double_divide(c3,b3) = sF0,
inference(orient,[status(thm)],[t2]) ).
cnf(t3,axiom,
sF1 = double_divide(double_divide(c3,b3),identity),
introduced(definition) ).
cnf(t1732,plain,
sF1 = double_divide(sF0,identity),
inference(step,[status(thm)],[t3,t10]) ).
cnf(t13,plain,
double_divide(sF0,identity) = sF1,
inference(orient,[status(thm)],[t1732]) ).
cnf(t4,axiom,
sF2 = double_divide(double_divide(double_divide(c3,b3),identity),a3),
introduced(definition) ).
cnf(t1734,plain,
sF2 = double_divide(double_divide(sF0,identity),a3),
inference(step,[status(thm)],[t4,t10]) ).
cnf(t1735,plain,
sF2 = double_divide(sF1,a3),
inference(step,[status(thm)],[t1734,t13]) ).
cnf(t19,plain,
double_divide(sF1,a3) = sF2,
inference(orient,[status(thm)],[t1735]) ).
cnf(t5,axiom,
sF3 = double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),
introduced(definition) ).
cnf(t1738,plain,
sF3 = double_divide(double_divide(double_divide(sF0,identity),a3),identity),
inference(step,[status(thm)],[t5,t10]) ).
cnf(t1739,plain,
sF3 = double_divide(double_divide(sF1,a3),identity),
inference(step,[status(thm)],[t1738,t13]) ).
cnf(t1740,plain,
sF3 = double_divide(sF2,identity),
inference(step,[status(thm)],[t1739,t19]) ).
cnf(t21,plain,
double_divide(sF2,identity) = sF3,
inference(orient,[status(thm)],[t1740]) ).
cnf(t6,axiom,
sF4 = double_divide(b3,a3),
introduced(definition) ).
cnf(t11,plain,
double_divide(b3,a3) = sF4,
inference(orient,[status(thm)],[t6]) ).
cnf(t7,axiom,
sF5 = double_divide(double_divide(b3,a3),identity),
introduced(definition) ).
cnf(t1733,plain,
sF5 = double_divide(sF4,identity),
inference(step,[status(thm)],[t7,t11]) ).
cnf(t16,plain,
double_divide(sF4,identity) = sF5,
inference(orient,[status(thm)],[t1733]) ).
cnf(t1,axiom,
double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3))),double_divide(identity,identity)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t23,plain,
double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3))),double_divide(identity,identity)) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(u1,axiom,
identity = double_divide(A,inverse(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(d1,axiom,
inverse(A) = double_divide(A,identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t0,plain,
double_divide(X1,double_divide(X1,identity)) = identity,
inference(definition_unfolding,[status(thm)],[u1,d1]) ).
cnf(t12,plain,
double_divide(X1,double_divide(X1,identity)) = identity,
inference(orient,[status(thm)],[t0]) ).
cnf(t26,plain,
X1 = double_divide(double_divide(X1,double_divide(identity,double_divide(identity,identity))),double_divide(identity,identity)),
inference(cp,[status(thm)],[t23,t12]) ).
cnf(t1741,plain,
X1 = double_divide(double_divide(X1,identity),double_divide(identity,identity)),
inference(step,[status(thm)],[t26,t12]) ).
cnf(t40,plain,
double_divide(double_divide(X1,identity),double_divide(identity,identity)) = X1,
inference(orient,[status(thm)],[t1741]) ).
cnf(t44,plain,
double_divide(X1,identity) = double_divide(double_divide(identity,double_divide(X1,double_divide(identity,identity))),double_divide(identity,identity)),
inference(cp,[status(thm)],[t23,t40]) ).
cnf(t64,plain,
double_divide(double_divide(identity,double_divide(X1,double_divide(identity,identity))),double_divide(identity,identity)) = double_divide(X1,identity),
inference(orient,[status(thm)],[t44]) ).
cnf(t65,plain,
double_divide(identity,identity) = double_divide(double_divide(identity,identity),double_divide(identity,identity)),
inference(cp,[status(thm)],[t64,t12]) ).
cnf(t1745,plain,
double_divide(identity,identity) = identity,
inference(step,[status(thm)],[t65,t40]) ).
cnf(t76,plain,
double_divide(identity,identity) = identity,
inference(orient,[status(thm)],[t1745]) ).
cnf(t1746,plain,
double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3))),identity) = X2,
inference(step,[status(thm)],[t23,t76]) ).
cnf(t77,plain,
double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3))),identity) = X2,
inference(rw,[status(thm)],[t1746]) ).
cnf(t84,plain,
double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3))),identity) = X2,
inference(orient,[status(thm)],[t77]) ).
cnf(t1747,plain,
double_divide(double_divide(X1,identity),identity) = X1,
inference(step,[status(thm)],[t40,t76]) ).
cnf(t78,plain,
double_divide(double_divide(X1,identity),identity) = X1,
inference(rw,[status(thm)],[t1747]) ).
cnf(t122,plain,
double_divide(double_divide(X1,identity),identity) = X1,
inference(orient,[status(thm)],[t78]) ).
cnf(t124,plain,
identity = double_divide(double_divide(X1,identity),X1),
inference(cp,[status(thm)],[t12,t122]) ).
cnf(t126,plain,
double_divide(double_divide(X1,identity),X1) = identity,
inference(orient,[status(thm)],[t124]) ).
cnf(t1752,plain,
double_divide(double_divide(identity,double_divide(X1,identity)),double_divide(identity,identity)) = double_divide(X1,identity),
inference(step,[status(thm)],[t64,t76]) ).
cnf(t1753,plain,
double_divide(double_divide(identity,double_divide(X1,identity)),identity) = double_divide(X1,identity),
inference(step,[status(thm)],[t1752,t76]) ).
cnf(t83,plain,
double_divide(double_divide(identity,double_divide(X1,identity)),identity) = double_divide(X1,identity),
inference(rw,[status(thm)],[t1753]) ).
cnf(t130,plain,
double_divide(double_divide(identity,double_divide(X1,identity)),identity) = double_divide(X1,identity),
inference(orient,[status(thm)],[t83]) ).
cnf(t135,plain,
double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3))),identity) = double_divide(double_divide(identity,X2),identity),
inference(cp,[status(thm)],[t130,t84]) ).
cnf(t1762,plain,
X2 = double_divide(double_divide(identity,X2),identity),
inference(step,[status(thm)],[t135,t84]) ).
cnf(t182,plain,
double_divide(double_divide(identity,X1),identity) = X1,
inference(orient,[status(thm)],[t1762]) ).
cnf(t188,plain,
identity = double_divide(X1,double_divide(identity,X1)),
inference(cp,[status(thm)],[t126,t182]) ).
cnf(t193,plain,
double_divide(X1,double_divide(identity,X1)) = identity,
inference(orient,[status(thm)],[t188]) ).
cnf(t194,plain,
X1 = double_divide(double_divide(identity,double_divide(identity,double_divide(identity,X1))),identity),
inference(cp,[status(thm)],[t84,t193]) ).
cnf(t1764,plain,
X1 = double_divide(identity,double_divide(identity,X1)),
inference(step,[status(thm)],[t194,t182]) ).
cnf(t196,plain,
double_divide(identity,double_divide(identity,X1)) = X1,
inference(orient,[status(thm)],[t1764]) ).
cnf(t201,plain,
X1 = double_divide(double_divide(identity,double_divide(double_divide(X1,X2),double_divide(identity,double_divide(identity,X2)))),identity),
inference(cp,[status(thm)],[t84,t196]) ).
cnf(t1765,plain,
X1 = double_divide(double_divide(X1,X2),double_divide(identity,double_divide(identity,X2))),
inference(step,[status(thm)],[t201,t182]) ).
cnf(t1766,plain,
X1 = double_divide(double_divide(X1,X2),X2),
inference(step,[status(thm)],[t1765,t196]) ).
cnf(t218,plain,
double_divide(double_divide(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t1766]) ).
cnf(t227,plain,
double_divide(X1,identity) = double_divide(identity,X1),
inference(cp,[status(thm)],[t218,t126]) ).
cnf(t247,plain,
double_divide(X1,identity) = double_divide(identity,X1),
inference(orient,[status(thm)],[t227]) ).
cnf(t1769,plain,
double_divide(identity,double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3)))) = X2,
inference(step,[status(thm)],[t84,t247]) ).
cnf(t248,plain,
double_divide(identity,double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3)))) = X2,
inference(rw,[status(thm)],[t1769]) ).
cnf(t269,plain,
double_divide(identity,double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3)))) = X2,
inference(orient,[status(thm)],[t248]) ).
cnf(t270,plain,
X1 = double_divide(identity,double_divide(X2,double_divide(double_divide(X1,identity),double_divide(identity,double_divide(X2,identity))))),
inference(cp,[status(thm)],[t269,t12]) ).
cnf(t223,plain,
X1 = double_divide(identity,double_divide(X1,identity)),
inference(cp,[status(thm)],[t218,t12]) ).
cnf(t242,plain,
double_divide(identity,double_divide(X1,identity)) = X1,
inference(orient,[status(thm)],[t223]) ).
cnf(t1772,plain,
X1 = double_divide(identity,double_divide(X2,double_divide(double_divide(X1,identity),X2))),
inference(step,[status(thm)],[t270,t242]) ).
cnf(t322,plain,
double_divide(identity,double_divide(X1,double_divide(double_divide(X2,identity),X1))) = X2,
inference(orient,[status(thm)],[t1772]) ).
cnf(t331,plain,
double_divide(X1,identity) = double_divide(identity,double_divide(X2,double_divide(X1,X2))),
inference(cp,[status(thm)],[t322,t218]) ).
cnf(t912,plain,
double_divide(identity,double_divide(X1,double_divide(X2,X1))) = double_divide(X2,identity),
inference(orient,[status(thm)],[t331]) ).
cnf(t953,plain,
double_divide(X1,double_divide(X2,X1)) = double_divide(identity,double_divide(X2,identity)),
inference(cp,[status(thm)],[t196,t912]) ).
cnf(t1839,plain,
double_divide(X1,double_divide(X2,X1)) = X2,
inference(step,[status(thm)],[t953,t242]) ).
cnf(t1038,plain,
double_divide(X1,double_divide(X2,X1)) = X2,
inference(orient,[status(thm)],[t1839]) ).
cnf(t1074,plain,
X1 = double_divide(X2,double_divide(X2,X1)),
inference(cp,[status(thm)],[t218,t1038]) ).
cnf(t1247,plain,
double_divide(X1,double_divide(X1,X2)) = X2,
inference(orient,[status(thm)],[t1074]) ).
cnf(t274,plain,
X1 = double_divide(identity,double_divide(sF4,double_divide(double_divide(X1,sF5),double_divide(identity,identity)))),
inference(cp,[status(thm)],[t269,t16]) ).
cnf(t1789,plain,
X1 = double_divide(identity,double_divide(sF4,double_divide(double_divide(X1,sF5),identity))),
inference(step,[status(thm)],[t274,t76]) ).
cnf(t1790,plain,
X1 = double_divide(identity,double_divide(sF4,double_divide(identity,double_divide(X1,sF5)))),
inference(step,[status(thm)],[t1789,t247]) ).
cnf(t460,plain,
double_divide(identity,double_divide(sF4,double_divide(identity,double_divide(X1,sF5)))) = X1,
inference(orient,[status(thm)],[t1790]) ).
cnf(t1260,plain,
double_divide(sF4,double_divide(identity,double_divide(X1,sF5))) = double_divide(identity,X1),
inference(cp,[status(thm)],[t1247,t460]) ).
cnf(t1545,plain,
double_divide(sF4,double_divide(identity,double_divide(X1,sF5))) = double_divide(identity,X1),
inference(orient,[status(thm)],[t1260]) ).
cnf(t1556,plain,
double_divide(identity,double_divide(X1,sF5)) = double_divide(sF4,double_divide(identity,X1)),
inference(cp,[status(thm)],[t1247,t1545]) ).
cnf(t1558,plain,
double_divide(identity,double_divide(X1,sF5)) = double_divide(sF4,double_divide(identity,X1)),
inference(orient,[status(thm)],[t1556]) ).
cnf(t919,plain,
double_divide(double_divide(X1,X2),identity) = double_divide(identity,double_divide(X2,X1)),
inference(cp,[status(thm)],[t912,t218]) ).
cnf(t1838,plain,
double_divide(identity,double_divide(X1,X2)) = double_divide(identity,double_divide(X2,X1)),
inference(step,[status(thm)],[t919,t247]) ).
cnf(t991,plain,
double_divide(identity,double_divide(X1,X2)) = double_divide(identity,double_divide(X2,X1)),
inference(orient,[status(thm)],[t1838]) ).
cnf(t9,axiom,
sF7 = double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),
introduced(definition) ).
cnf(t1742,plain,
sF7 = double_divide(double_divide(c3,double_divide(sF4,identity)),identity),
inference(step,[status(thm)],[t9,t11]) ).
cnf(t1743,plain,
sF7 = double_divide(double_divide(c3,sF5),identity),
inference(step,[status(thm)],[t1742,t16]) ).
cnf(t8,axiom,
sF6 = double_divide(c3,double_divide(double_divide(b3,a3),identity)),
introduced(definition) ).
cnf(t1736,plain,
sF6 = double_divide(c3,double_divide(sF4,identity)),
inference(step,[status(thm)],[t8,t11]) ).
cnf(t1737,plain,
sF6 = double_divide(c3,sF5),
inference(step,[status(thm)],[t1736,t16]) ).
cnf(t20,plain,
double_divide(c3,sF5) = sF6,
inference(orient,[status(thm)],[t1737]) ).
cnf(t1744,plain,
sF7 = double_divide(sF6,identity),
inference(step,[status(thm)],[t1743,t20]) ).
cnf(t55,plain,
double_divide(sF6,identity) = sF7,
inference(orient,[status(thm)],[t1744]) ).
cnf(t58,plain,
sF6 = double_divide(sF7,double_divide(identity,identity)),
inference(cp,[status(thm)],[t40,t55]) ).
cnf(t61,plain,
double_divide(sF7,double_divide(identity,identity)) = sF6,
inference(orient,[status(thm)],[t58]) ).
cnf(t1751,plain,
double_divide(sF7,identity) = sF6,
inference(step,[status(thm)],[t61,t76]) ).
cnf(t82,plain,
double_divide(sF7,identity) = sF6,
inference(rw,[status(thm)],[t1751]) ).
cnf(t111,plain,
double_divide(sF7,identity) = sF6,
inference(orient,[status(thm)],[t82]) ).
cnf(t285,plain,
X1 = double_divide(identity,double_divide(sF7,double_divide(double_divide(X1,sF6),double_divide(identity,identity)))),
inference(cp,[status(thm)],[t269,t111]) ).
cnf(t1830,plain,
X1 = double_divide(identity,double_divide(sF7,double_divide(double_divide(X1,sF6),identity))),
inference(step,[status(thm)],[t285,t76]) ).
cnf(t1831,plain,
X1 = double_divide(identity,double_divide(sF7,double_divide(identity,double_divide(X1,sF6)))),
inference(step,[status(thm)],[t1830,t247]) ).
cnf(t884,plain,
double_divide(identity,double_divide(sF7,double_divide(identity,double_divide(X1,sF6)))) = X1,
inference(orient,[status(thm)],[t1831]) ).
cnf(t324,plain,
sF4 = double_divide(identity,double_divide(X1,double_divide(sF5,X1))),
inference(cp,[status(thm)],[t322,t16]) ).
cnf(t389,plain,
double_divide(identity,double_divide(X1,double_divide(sF5,X1))) = sF4,
inference(orient,[status(thm)],[t324]) ).
cnf(t393,plain,
double_divide(X1,double_divide(sF5,X1)) = double_divide(identity,sF4),
inference(cp,[status(thm)],[t196,t389]) ).
cnf(t1781,plain,
double_divide(X1,double_divide(sF5,X1)) = double_divide(sF4,identity),
inference(step,[status(thm)],[t393,t247]) ).
cnf(t1782,plain,
double_divide(X1,double_divide(sF5,X1)) = sF5,
inference(step,[status(thm)],[t1781,t16]) ).
cnf(t397,plain,
double_divide(X1,double_divide(sF5,X1)) = sF5,
inference(orient,[status(thm)],[t1782]) ).
cnf(t402,plain,
X1 = double_divide(sF5,double_divide(sF5,X1)),
inference(cp,[status(thm)],[t218,t397]) ).
cnf(t422,plain,
double_divide(sF5,double_divide(sF5,X1)) = X1,
inference(orient,[status(thm)],[t402]) ).
cnf(t330,plain,
sF7 = double_divide(identity,double_divide(X1,double_divide(sF6,X1))),
inference(cp,[status(thm)],[t322,t111]) ).
cnf(t790,plain,
double_divide(identity,double_divide(X1,double_divide(sF6,X1))) = sF7,
inference(orient,[status(thm)],[t330]) ).
cnf(t225,plain,
c3 = double_divide(sF6,sF5),
inference(cp,[status(thm)],[t218,t20]) ).
cnf(t240,plain,
double_divide(sF6,sF5) = c3,
inference(orient,[status(thm)],[t225]) ).
cnf(t792,plain,
sF7 = double_divide(identity,double_divide(sF5,c3)),
inference(cp,[status(thm)],[t790,t240]) ).
cnf(t804,plain,
double_divide(identity,double_divide(sF5,c3)) = sF7,
inference(orient,[status(thm)],[t792]) ).
cnf(t806,plain,
double_divide(sF5,c3) = double_divide(identity,sF7),
inference(cp,[status(thm)],[t196,t804]) ).
cnf(t1822,plain,
double_divide(sF5,c3) = double_divide(sF7,identity),
inference(step,[status(thm)],[t806,t247]) ).
cnf(t1823,plain,
double_divide(sF5,c3) = sF6,
inference(step,[status(thm)],[t1822,t111]) ).
cnf(t810,plain,
double_divide(sF5,c3) = sF6,
inference(orient,[status(thm)],[t1823]) ).
cnf(t815,plain,
c3 = double_divide(sF5,sF6),
inference(cp,[status(thm)],[t422,t810]) ).
cnf(t821,plain,
double_divide(sF5,sF6) = c3,
inference(orient,[status(thm)],[t815]) ).
cnf(t887,plain,
sF5 = double_divide(identity,double_divide(sF7,double_divide(identity,c3))),
inference(cp,[status(thm)],[t884,t821]) ).
cnf(t1437,plain,
double_divide(identity,double_divide(sF7,double_divide(identity,c3))) = sF5,
inference(orient,[status(thm)],[t887]) ).
cnf(t1441,plain,
double_divide(identity,double_divide(double_divide(sF7,double_divide(identity,c3)),identity)) = double_divide(identity,sF5),
inference(cp,[status(thm)],[t991,t1437]) ).
cnf(t1916,plain,
double_divide(sF7,double_divide(identity,c3)) = double_divide(identity,sF5),
inference(step,[status(thm)],[t1441,t1038]) ).
cnf(t1917,plain,
double_divide(sF7,double_divide(identity,c3)) = double_divide(sF5,identity),
inference(step,[status(thm)],[t1916,t247]) ).
cnf(t42,plain,
sF4 = double_divide(sF5,double_divide(identity,identity)),
inference(cp,[status(thm)],[t40,t16]) ).
cnf(t49,plain,
double_divide(sF5,double_divide(identity,identity)) = sF4,
inference(orient,[status(thm)],[t42]) ).
cnf(t1749,plain,
double_divide(sF5,identity) = sF4,
inference(step,[status(thm)],[t49,t76]) ).
cnf(t80,plain,
double_divide(sF5,identity) = sF4,
inference(rw,[status(thm)],[t1749]) ).
cnf(t105,plain,
double_divide(sF5,identity) = sF4,
inference(orient,[status(thm)],[t80]) ).
cnf(t1918,plain,
double_divide(sF7,double_divide(identity,c3)) = sF4,
inference(step,[status(thm)],[t1917,t105]) ).
cnf(t1446,plain,
double_divide(sF7,double_divide(identity,c3)) = sF4,
inference(orient,[status(thm)],[t1918]) ).
cnf(t1453,plain,
double_divide(identity,c3) = double_divide(sF7,sF4),
inference(cp,[status(thm)],[t1247,t1446]) ).
cnf(t1022,plain,
double_divide(identity,double_divide(double_divide(X1,X2),identity)) = double_divide(identity,double_divide(identity,double_divide(X2,X1))),
inference(cp,[status(thm)],[t991,t991]) ).
cnf(t1884,plain,
double_divide(X1,X2) = double_divide(identity,double_divide(identity,double_divide(X2,X1))),
inference(step,[status(thm)],[t1022,t1038]) ).
cnf(t1885,plain,
double_divide(X1,X2) = double_divide(X2,X1),
inference(step,[status(thm)],[t1884,t1247]) ).
cnf(t1269,plain,
double_divide(X1,X2) = double_divide(X2,X1),
inference(orient,[status(thm)],[t1885]) ).
cnf(t1920,plain,
double_divide(identity,c3) = double_divide(sF4,sF7),
inference(step,[status(thm)],[t1453,t1269]) ).
cnf(t1455,plain,
double_divide(identity,c3) = double_divide(sF4,sF7),
inference(orient,[status(thm)],[t1920]) ).
cnf(t1688,plain,
double_divide(sF2,identity) = sF7,
inference(rw,[status(thm)],[t55]) ).
cnf(t1949,plain,
sF3 = sF7,
inference(step,[status(thm)],[t1688,t21]) ).
cnf(t1724,plain,
sF7 = sF3,
inference(orient,[status(thm)],[t1949]) ).
cnf(t1950,plain,
double_divide(identity,c3) = double_divide(sF4,sF3),
inference(step,[status(thm)],[t1455,t1724]) ).
cnf(t1726,plain,
double_divide(identity,c3) = double_divide(sF4,sF3),
inference(orient,[status(thm)],[t1950]) ).
cnf(u0,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
multiply(A,B) = double_divide(double_divide(B,A),identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity) != double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(g0_0,plain,
double_divide(double_divide(double_divide(sF0,identity),a3),identity) != double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),
inference(rw,[status(thm)],[goal_0,t10]) ).
cnf(g0_1,plain,
double_divide(double_divide(sF1,a3),identity) != double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),
inference(rw,[status(thm)],[g0_0,t13]) ).
cnf(g0_2,plain,
double_divide(sF2,identity) != double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),
inference(rw,[status(thm)],[g0_1,t19]) ).
cnf(g0_3,plain,
sF3 != double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),
inference(rw,[status(thm)],[g0_2,t21]) ).
cnf(g0_4,plain,
sF3 != double_divide(double_divide(c3,double_divide(sF4,identity)),identity),
inference(rw,[status(thm)],[g0_3,t11]) ).
cnf(g0_5,plain,
sF3 != double_divide(double_divide(c3,sF5),identity),
inference(rw,[status(thm)],[g0_4,t16]) ).
cnf(g0_6,plain,
sF3 != double_divide(identity,double_divide(c3,sF5)),
inference(rw,[status(thm)],[g0_5,t247]) ).
cnf(g0_7,plain,
sF3 != double_divide(sF4,double_divide(identity,c3)),
inference(rw,[status(thm)],[g0_6,t1558]) ).
cnf(g0_8,plain,
sF3 != double_divide(sF4,double_divide(sF4,sF3)),
inference(rw,[status(thm)],[g0_7,t1726]) ).
cnf(g0_9,plain,
sF3 != sF3,
inference(rw,[status(thm)],[g0_8,t1247]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP567-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 15:07:19 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 6.10/1.19 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.10/1.19 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------