%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP563-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:32 PM UTC 2026
% Result : Unsatisfiable 6.48s 1.30s
% Output : CNFRefutation 6.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 10
% Syntax : Number of clauses : 143 ( 143 unt; 0 nHn; 76 RR)
% Number of literals : 143 ( 142 equ; 10 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 10 con; 0-2 aty)
% Number of variables : 105 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t1,axiom,
sF0 = inverse(b3),
introduced(definition) ).
cnf(t8,plain,
inverse(b3) = sF0,
inference(orient,[status(thm)],[t1]) ).
cnf(t2,axiom,
sF1 = divide(a3,inverse(b3)),
introduced(definition) ).
cnf(t1893,plain,
sF1 = divide(a3,sF0),
inference(step,[status(thm)],[t2,t8]) ).
cnf(t10,plain,
divide(a3,sF0) = sF1,
inference(orient,[status(thm)],[t1893]) ).
cnf(t3,axiom,
sF2 = inverse(c3),
introduced(definition) ).
cnf(t9,plain,
inverse(c3) = sF2,
inference(orient,[status(thm)],[t3]) ).
cnf(t4,axiom,
sF3 = divide(divide(a3,inverse(b3)),inverse(c3)),
introduced(definition) ).
cnf(t1897,plain,
sF3 = divide(divide(a3,sF0),inverse(c3)),
inference(step,[status(thm)],[t4,t8]) ).
cnf(t1898,plain,
sF3 = divide(sF1,inverse(c3)),
inference(step,[status(thm)],[t1897,t10]) ).
cnf(t1899,plain,
sF3 = divide(sF1,sF2),
inference(step,[status(thm)],[t1898,t9]) ).
cnf(t13,plain,
divide(sF1,sF2) = sF3,
inference(orient,[status(thm)],[t1899]) ).
cnf(t0,axiom,
divide(divide(divide(X1,inverse(X2)),X3),divide(X1,X3)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t15,plain,
divide(divide(divide(X1,inverse(X2)),X3),divide(X1,X3)) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t24,plain,
X1 = divide(divide(divide(divide(divide(X2,inverse(X3)),Y3),inverse(X1)),divide(X2,Y3)),X3),
inference(cp,[status(thm)],[t15,t15]) ).
cnf(t430,plain,
divide(divide(divide(divide(divide(X1,inverse(X2)),X3),inverse(Y3)),divide(X1,X3)),X2) = Y3,
inference(orient,[status(thm)],[t24]) ).
cnf(t497,plain,
X1 = divide(divide(X2,divide(divide(divide(X3,inverse(inverse(X1))),Y3),divide(X3,Y3))),X2),
inference(cp,[status(thm)],[t430,t430]) ).
cnf(t1915,plain,
X1 = divide(divide(X2,inverse(X1)),X2),
inference(step,[status(thm)],[t497,t15]) ).
cnf(t532,plain,
divide(divide(X1,inverse(X2)),X1) = X2,
inference(orient,[status(thm)],[t1915]) ).
cnf(t23,plain,
X1 = divide(X2,divide(divide(X3,inverse(X2)),divide(X3,inverse(X1)))),
inference(cp,[status(thm)],[t15,t15]) ).
cnf(t322,plain,
divide(X1,divide(divide(X2,inverse(X1)),divide(X2,inverse(X3)))) = X3,
inference(orient,[status(thm)],[t23]) ).
cnf(t533,plain,
b3 = divide(divide(X1,sF0),X1),
inference(cp,[status(thm)],[t532,t8]) ).
cnf(t552,plain,
divide(divide(X1,sF0),X1) = b3,
inference(orient,[status(thm)],[t533]) ).
cnf(t556,plain,
b3 = divide(X1,divide(sF0,inverse(X1))),
inference(cp,[status(thm)],[t552,t532]) ).
cnf(t930,plain,
divide(X1,divide(sF0,inverse(X1))) = b3,
inference(orient,[status(thm)],[t556]) ).
cnf(t945,plain,
divide(sF0,inverse(X1)) = divide(X1,b3),
inference(cp,[status(thm)],[t322,t930]) ).
cnf(t950,plain,
divide(sF0,inverse(X1)) = divide(X1,b3),
inference(orient,[status(thm)],[t945]) ).
cnf(t963,plain,
X1 = divide(divide(X1,b3),sF0),
inference(cp,[status(thm)],[t532,t950]) ).
cnf(t1013,plain,
divide(divide(X1,b3),sF0) = X1,
inference(orient,[status(thm)],[t963]) ).
cnf(t1016,plain,
divide(b3,inverse(X1)) = divide(X1,sF0),
inference(cp,[status(thm)],[t1013,t532]) ).
cnf(t1145,plain,
divide(b3,inverse(X1)) = divide(X1,sF0),
inference(orient,[status(thm)],[t1016]) ).
cnf(t6,axiom,
sF5 = inverse(divide(b3,inverse(c3))),
introduced(definition) ).
cnf(t1895,plain,
sF5 = inverse(divide(b3,sF2)),
inference(step,[status(thm)],[t6,t9]) ).
cnf(t5,axiom,
sF4 = divide(b3,inverse(c3)),
introduced(definition) ).
cnf(t1894,plain,
sF4 = divide(b3,sF2),
inference(step,[status(thm)],[t5,t9]) ).
cnf(t11,plain,
divide(b3,sF2) = sF4,
inference(orient,[status(thm)],[t1894]) ).
cnf(t1896,plain,
sF5 = inverse(sF4),
inference(step,[status(thm)],[t1895,t11]) ).
cnf(t12,plain,
inverse(sF4) = sF5,
inference(orient,[status(thm)],[t1896]) ).
cnf(t535,plain,
sF4 = divide(divide(X1,sF5),X1),
inference(cp,[status(thm)],[t532,t12]) ).
cnf(t618,plain,
divide(divide(X1,sF5),X1) = sF4,
inference(orient,[status(thm)],[t535]) ).
cnf(t954,plain,
divide(sF4,b3) = divide(sF0,sF5),
inference(cp,[status(thm)],[t950,t12]) ).
cnf(t17,plain,
c3 = divide(divide(divide(X1,sF2),X2),divide(X1,X2)),
inference(cp,[status(thm)],[t15,t9]) ).
cnf(t81,plain,
divide(divide(divide(X1,sF2),X2),divide(X1,X2)) = c3,
inference(orient,[status(thm)],[t17]) ).
cnf(t82,plain,
c3 = divide(divide(sF4,X1),divide(b3,X1)),
inference(cp,[status(thm)],[t81,t11]) ).
cnf(t130,plain,
divide(divide(sF4,X1),divide(b3,X1)) = c3,
inference(orient,[status(thm)],[t82]) ).
cnf(t20,plain,
sF4 = divide(divide(divide(X1,sF5),X2),divide(X1,X2)),
inference(cp,[status(thm)],[t15,t12]) ).
cnf(t212,plain,
divide(divide(divide(X1,sF5),X2),divide(X1,X2)) = sF4,
inference(orient,[status(thm)],[t20]) ).
cnf(t7,axiom,
sF6 = divide(a3,inverse(divide(b3,inverse(c3)))),
introduced(definition) ).
cnf(t1900,plain,
sF6 = divide(a3,inverse(divide(b3,sF2))),
inference(step,[status(thm)],[t7,t9]) ).
cnf(t1901,plain,
sF6 = divide(a3,inverse(sF4)),
inference(step,[status(thm)],[t1900,t11]) ).
cnf(t1902,plain,
sF6 = divide(a3,sF5),
inference(step,[status(thm)],[t1901,t12]) ).
cnf(t14,plain,
divide(a3,sF5) = sF6,
inference(orient,[status(thm)],[t1902]) ).
cnf(t22,plain,
X1 = divide(divide(divide(a3,inverse(X1)),sF5),sF6),
inference(cp,[status(thm)],[t15,t14]) ).
cnf(t207,plain,
divide(divide(divide(a3,inverse(X1)),sF5),sF6) = X1,
inference(orient,[status(thm)],[t22]) ).
cnf(t208,plain,
sF4 = divide(divide(divide(a3,sF5),sF5),sF6),
inference(cp,[status(thm)],[t207,t12]) ).
cnf(t1909,plain,
sF4 = divide(divide(sF6,sF5),sF6),
inference(step,[status(thm)],[t208,t14]) ).
cnf(t266,plain,
divide(divide(sF6,sF5),sF6) = sF4,
inference(orient,[status(thm)],[t1909]) ).
cnf(t270,plain,
sF4 = divide(sF4,divide(sF6,sF6)),
inference(cp,[status(thm)],[t212,t266]) ).
cnf(t277,plain,
divide(sF4,divide(sF6,sF6)) = sF4,
inference(orient,[status(thm)],[t270]) ).
cnf(t281,plain,
c3 = divide(sF4,divide(b3,divide(sF6,sF6))),
inference(cp,[status(thm)],[t130,t277]) ).
cnf(t310,plain,
divide(sF4,divide(b3,divide(sF6,sF6))) = c3,
inference(orient,[status(thm)],[t281]) ).
cnf(t16,plain,
b3 = divide(divide(divide(X1,sF0),X2),divide(X1,X2)),
inference(cp,[status(thm)],[t15,t8]) ).
cnf(t32,plain,
divide(divide(divide(X1,sF0),X2),divide(X1,X2)) = b3,
inference(orient,[status(thm)],[t16]) ).
cnf(t43,plain,
b3 = divide(b3,divide(divide(X1,sF0),divide(X1,sF0))),
inference(cp,[status(thm)],[t32,t32]) ).
cnf(t425,plain,
divide(b3,divide(divide(X1,sF0),divide(X1,sF0))) = b3,
inference(orient,[status(thm)],[t43]) ).
cnf(t509,plain,
b3 = divide(b3,divide(X1,divide(divide(divide(divide(divide(X2,inverse(sF0)),X3),inverse(X1)),divide(X2,X3)),sF0))),
inference(cp,[status(thm)],[t425,t430]) ).
cnf(t1911,plain,
b3 = divide(b3,divide(X1,X1)),
inference(step,[status(thm)],[t509,t430]) ).
cnf(t510,plain,
divide(b3,divide(X1,X1)) = b3,
inference(orient,[status(thm)],[t1911]) ).
cnf(t1913,plain,
divide(sF4,b3) = c3,
inference(step,[status(thm)],[t310,t510]) ).
cnf(t512,plain,
divide(sF4,b3) = c3,
inference(rw,[status(thm)],[t1913]) ).
cnf(t519,plain,
divide(sF4,b3) = c3,
inference(orient,[status(thm)],[t512]) ).
cnf(t1931,plain,
c3 = divide(sF0,sF5),
inference(step,[status(thm)],[t954,t519]) ).
cnf(t974,plain,
divide(sF0,sF5) = c3,
inference(orient,[status(thm)],[t1931]) ).
cnf(t980,plain,
sF4 = divide(c3,sF0),
inference(cp,[status(thm)],[t618,t974]) ).
cnf(t982,plain,
divide(c3,sF0) = sF4,
inference(orient,[status(thm)],[t980]) ).
cnf(t538,plain,
X1 = divide(X1,divide(X2,X2)),
inference(cp,[status(thm)],[t15,t532]) ).
cnf(t647,plain,
divide(X1,divide(X2,X2)) = X1,
inference(orient,[status(thm)],[t538]) ).
cnf(t655,plain,
divide(divide(X1,X1),inverse(X2)) = X2,
inference(cp,[status(thm)],[t647,t532]) ).
cnf(t1701,plain,
divide(divide(X1,X1),inverse(X2)) = X2,
inference(orient,[status(thm)],[t655]) ).
cnf(t1704,plain,
X1 = divide(X2,divide(X2,divide(divide(X3,X3),inverse(X1)))),
inference(cp,[status(thm)],[t322,t1701]) ).
cnf(t1952,plain,
X1 = divide(X2,divide(X2,X1)),
inference(step,[status(thm)],[t1704,t1701]) ).
cnf(t1713,plain,
divide(X1,divide(X1,X2)) = X2,
inference(orient,[status(thm)],[t1952]) ).
cnf(t36,plain,
b3 = divide(divide(divide(a3,sF0),sF5),sF6),
inference(cp,[status(thm)],[t32,t14]) ).
cnf(t1905,plain,
b3 = divide(divide(sF1,sF5),sF6),
inference(step,[status(thm)],[t36,t10]) ).
cnf(t51,plain,
divide(divide(sF1,sF5),sF6) = b3,
inference(orient,[status(thm)],[t1905]) ).
cnf(t221,plain,
sF4 = divide(b3,divide(sF1,sF6)),
inference(cp,[status(thm)],[t212,t51]) ).
cnf(t272,plain,
divide(b3,divide(sF1,sF6)) = sF4,
inference(orient,[status(thm)],[t221]) ).
cnf(t1745,plain,
divide(sF1,sF6) = divide(b3,sF4),
inference(cp,[status(thm)],[t1713,t272]) ).
cnf(t45,plain,
X1 = divide(b3,divide(divide(X2,sF0),divide(X2,inverse(X1)))),
inference(cp,[status(thm)],[t15,t32]) ).
cnf(t1195,plain,
divide(b3,divide(divide(X1,sF0),divide(X1,inverse(X2)))) = X2,
inference(orient,[status(thm)],[t45]) ).
cnf(t622,plain,
sF4 = divide(X1,divide(sF5,inverse(X1))),
inference(cp,[status(thm)],[t618,t532]) ).
cnf(t1460,plain,
divide(X1,divide(sF5,inverse(X1))) = sF4,
inference(orient,[status(thm)],[t622]) ).
cnf(t1482,plain,
divide(sF5,sF0) = divide(b3,sF4),
inference(cp,[status(thm)],[t1195,t1460]) ).
cnf(t1485,plain,
divide(b3,sF4) = divide(sF5,sF0),
inference(orient,[status(thm)],[t1482]) ).
cnf(t1475,plain,
divide(sF5,inverse(X1)) = divide(X1,sF4),
inference(cp,[status(thm)],[t322,t1460]) ).
cnf(t1491,plain,
divide(sF5,inverse(X1)) = divide(X1,sF4),
inference(orient,[status(thm)],[t1475]) ).
cnf(t1503,plain,
X1 = divide(divide(X1,sF4),sF5),
inference(cp,[status(thm)],[t532,t1491]) ).
cnf(t1556,plain,
divide(divide(X1,sF4),sF5) = X1,
inference(orient,[status(thm)],[t1503]) ).
cnf(t1560,plain,
divide(sF4,inverse(X1)) = divide(X1,sF5),
inference(cp,[status(thm)],[t1556,t532]) ).
cnf(t1572,plain,
divide(sF4,inverse(X1)) = divide(X1,sF5),
inference(orient,[status(thm)],[t1560]) ).
cnf(t1581,plain,
X1 = divide(divide(X1,sF5),sF4),
inference(cp,[status(thm)],[t532,t1572]) ).
cnf(t1608,plain,
divide(divide(X1,sF5),sF4) = X1,
inference(orient,[status(thm)],[t1581]) ).
cnf(t534,plain,
c3 = divide(divide(X1,sF2),X1),
inference(cp,[status(thm)],[t532,t9]) ).
cnf(t576,plain,
divide(divide(X1,sF2),X1) = c3,
inference(orient,[status(thm)],[t534]) ).
cnf(t581,plain,
c3 = divide(X1,divide(sF2,inverse(X1))),
inference(cp,[status(thm)],[t576,t532]) ).
cnf(t1214,plain,
divide(X1,divide(sF2,inverse(X1))) = c3,
inference(orient,[status(thm)],[t581]) ).
cnf(t1229,plain,
divide(sF2,inverse(X1)) = divide(X1,c3),
inference(cp,[status(thm)],[t322,t1214]) ).
cnf(t1242,plain,
divide(sF2,inverse(X1)) = divide(X1,c3),
inference(orient,[status(thm)],[t1229]) ).
cnf(t1245,plain,
divide(sF4,c3) = divide(sF2,sF5),
inference(cp,[status(thm)],[t1242,t12]) ).
cnf(t657,plain,
divide(divide(X1,X1),sF2) = c3,
inference(cp,[status(thm)],[t647,t576]) ).
cnf(t845,plain,
divide(divide(X1,X1),sF2) = c3,
inference(orient,[status(thm)],[t657]) ).
cnf(t847,plain,
b3 = divide(divide(divide(divide(X1,X1),sF0),sF2),c3),
inference(cp,[status(thm)],[t32,t845]) ).
cnf(t656,plain,
divide(divide(X1,X1),sF0) = b3,
inference(cp,[status(thm)],[t647,t552]) ).
cnf(t834,plain,
divide(divide(X1,X1),sF0) = b3,
inference(orient,[status(thm)],[t656]) ).
cnf(t1926,plain,
b3 = divide(divide(b3,sF2),c3),
inference(step,[status(thm)],[t847,t834]) ).
cnf(t1927,plain,
b3 = divide(sF4,c3),
inference(step,[status(thm)],[t1926,t11]) ).
cnf(t854,plain,
divide(sF4,c3) = b3,
inference(orient,[status(thm)],[t1927]) ).
cnf(t1941,plain,
b3 = divide(sF2,sF5),
inference(step,[status(thm)],[t1245,t854]) ).
cnf(t1261,plain,
divide(sF2,sF5) = b3,
inference(orient,[status(thm)],[t1941]) ).
cnf(t1616,plain,
sF2 = divide(b3,sF4),
inference(cp,[status(thm)],[t1608,t1261]) ).
cnf(t1949,plain,
sF2 = divide(sF5,sF0),
inference(step,[status(thm)],[t1616,t1485]) ).
cnf(t1649,plain,
divide(sF5,sF0) = sF2,
inference(orient,[status(thm)],[t1949]) ).
cnf(t1950,plain,
divide(b3,sF4) = sF2,
inference(step,[status(thm)],[t1485,t1649]) ).
cnf(t1651,plain,
divide(b3,sF4) = sF2,
inference(orient,[status(thm)],[t1950]) ).
cnf(t1962,plain,
divide(sF1,sF6) = sF2,
inference(step,[status(thm)],[t1745,t1651]) ).
cnf(t1864,plain,
divide(sF1,sF6) = sF2,
inference(orient,[status(thm)],[t1962]) ).
cnf(t1874,plain,
sF6 = divide(sF1,sF2),
inference(cp,[status(thm)],[t1713,t1864]) ).
cnf(t1964,plain,
sF6 = sF3,
inference(step,[status(thm)],[t1874,t13]) ).
cnf(t1875,plain,
sF6 = sF3,
inference(orient,[status(thm)],[t1964]) ).
cnf(t1965,plain,
divide(a3,sF5) = sF3,
inference(step,[status(thm)],[t14,t1875]) ).
cnf(t1876,plain,
divide(a3,sF5) = sF3,
inference(orient,[status(thm)],[t1965]) ).
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) = divide(A,inverse(B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
divide(divide(a3,inverse(b3)),inverse(c3)) != divide(a3,inverse(divide(b3,inverse(c3)))),
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(g0_0,plain,
divide(divide(a3,sF0),inverse(c3)) != divide(a3,inverse(divide(b3,inverse(c3)))),
inference(rw,[status(thm)],[goal_0,t8]) ).
cnf(g0_1,plain,
divide(sF1,inverse(c3)) != divide(a3,inverse(divide(b3,inverse(c3)))),
inference(rw,[status(thm)],[g0_0,t10]) ).
cnf(g0_2,plain,
divide(sF1,sF2) != divide(a3,inverse(divide(b3,inverse(c3)))),
inference(rw,[status(thm)],[g0_1,t9]) ).
cnf(g0_3,plain,
sF3 != divide(a3,inverse(divide(b3,inverse(c3)))),
inference(rw,[status(thm)],[g0_2,t13]) ).
cnf(g0_4,plain,
sF3 != divide(a3,inverse(divide(c3,sF0))),
inference(rw,[status(thm)],[g0_3,t1145]) ).
cnf(g0_5,plain,
sF3 != divide(a3,inverse(sF4)),
inference(rw,[status(thm)],[g0_4,t982]) ).
cnf(g0_6,plain,
sF3 != divide(a3,sF5),
inference(rw,[status(thm)],[g0_5,t12]) ).
cnf(g0_7,plain,
sF3 != sF3,
inference(rw,[status(thm)],[g0_6,t1876]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP563-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n003.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 15:07:06 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 6.48/1.30 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.48/1.30 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------