%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP598-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 : n009.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:37 PM UTC 2026
% Result : Unsatisfiable 5.46s 1.21s
% Output : CNFRefutation 5.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 8
% Syntax : Number of clauses : 113 ( 113 unt; 0 nHn; 58 RR)
% Number of literals : 113 ( 112 equ; 8 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 : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 78 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
double_divide(double_divide(X1,X2),inverse(double_divide(X1,inverse(double_divide(inverse(X3),X2))))) = X3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t11,plain,
double_divide(double_divide(X1,X2),inverse(double_divide(X1,inverse(double_divide(inverse(X3),X2))))) = X3,
inference(orient,[status(thm)],[t0]) ).
cnf(t2,axiom,
sF1 = double_divide(b2,inverse(b2)),
introduced(definition) ).
cnf(t1,axiom,
sF0 = inverse(b2),
introduced(definition) ).
cnf(t6,plain,
inverse(b2) = sF0,
inference(orient,[status(thm)],[t1]) ).
cnf(t1042,plain,
sF1 = double_divide(b2,sF0),
inference(step,[status(thm)],[t2,t6]) ).
cnf(t7,plain,
double_divide(b2,sF0) = sF1,
inference(orient,[status(thm)],[t1042]) ).
cnf(t13,plain,
X1 = double_divide(sF1,inverse(double_divide(b2,inverse(double_divide(inverse(X1),sF0))))),
inference(cp,[status(thm)],[t11,t7]) ).
cnf(t19,plain,
double_divide(sF1,inverse(double_divide(b2,inverse(double_divide(inverse(X1),sF0))))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t17,plain,
X1 = double_divide(X2,inverse(double_divide(double_divide(X3,Y3),inverse(double_divide(inverse(X1),inverse(double_divide(X3,inverse(double_divide(inverse(X2),Y3))))))))),
inference(cp,[status(thm)],[t11,t11]) ).
cnf(t118,plain,
double_divide(X1,inverse(double_divide(double_divide(X2,X3),inverse(double_divide(inverse(Y3),inverse(double_divide(X2,inverse(double_divide(inverse(X1),X3))))))))) = Y3,
inference(orient,[status(thm)],[t17]) ).
cnf(t140,plain,
X1 = double_divide(X2,inverse(double_divide(double_divide(double_divide(X3,Y3),inverse(double_divide(X3,inverse(double_divide(inverse(inverse(X1)),Y3))))),inverse(X2)))),
inference(cp,[status(thm)],[t118,t118]) ).
cnf(t1062,plain,
X1 = double_divide(X2,inverse(double_divide(inverse(X1),inverse(X2)))),
inference(step,[status(thm)],[t140,t11]) ).
cnf(t218,plain,
double_divide(X1,inverse(double_divide(inverse(X2),inverse(X1)))) = X2,
inference(orient,[status(thm)],[t1062]) ).
cnf(t220,plain,
X1 = double_divide(b2,inverse(double_divide(inverse(X1),sF0))),
inference(cp,[status(thm)],[t218,t6]) ).
cnf(t287,plain,
double_divide(b2,inverse(double_divide(inverse(X1),sF0))) = X1,
inference(orient,[status(thm)],[t220]) ).
cnf(t1063,plain,
double_divide(sF1,inverse(X1)) = X1,
inference(step,[status(thm)],[t19,t287]) ).
cnf(t288,plain,
double_divide(sF1,inverse(X1)) = X1,
inference(rw,[status(thm)],[t1063]) ).
cnf(t297,plain,
double_divide(sF1,inverse(X1)) = X1,
inference(orient,[status(thm)],[t288]) ).
cnf(t303,plain,
double_divide(inverse(X1),inverse(sF1)) = X1,
inference(cp,[status(thm)],[t297,t218]) ).
cnf(t3,axiom,
sF2 = inverse(double_divide(b2,inverse(b2))),
introduced(definition) ).
cnf(t1043,plain,
sF2 = inverse(double_divide(b2,sF0)),
inference(step,[status(thm)],[t3,t6]) ).
cnf(t1044,plain,
sF2 = inverse(sF1),
inference(step,[status(thm)],[t1043,t7]) ).
cnf(t8,plain,
inverse(sF1) = sF2,
inference(orient,[status(thm)],[t1044]) ).
cnf(t1067,plain,
double_divide(inverse(X1),sF2) = X1,
inference(step,[status(thm)],[t303,t8]) ).
cnf(t375,plain,
double_divide(inverse(X1),sF2) = X1,
inference(orient,[status(thm)],[t1067]) ).
cnf(t14,plain,
sF1 = double_divide(double_divide(X1,X2),inverse(double_divide(X1,inverse(double_divide(sF2,X2))))),
inference(cp,[status(thm)],[t11,t8]) ).
cnf(t59,plain,
double_divide(double_divide(X1,X2),inverse(double_divide(X1,inverse(double_divide(sF2,X2))))) = sF1,
inference(orient,[status(thm)],[t14]) ).
cnf(t377,plain,
sF1 = double_divide(sF2,sF2),
inference(cp,[status(thm)],[t375,t8]) ).
cnf(t389,plain,
double_divide(sF2,sF2) = sF1,
inference(orient,[status(thm)],[t377]) ).
cnf(t391,plain,
X1 = double_divide(sF1,inverse(double_divide(sF2,inverse(double_divide(inverse(X1),sF2))))),
inference(cp,[status(thm)],[t11,t389]) ).
cnf(t1076,plain,
X1 = double_divide(sF2,inverse(double_divide(inverse(X1),sF2))),
inference(step,[status(thm)],[t391,t297]) ).
cnf(t1077,plain,
X1 = double_divide(sF2,inverse(X1)),
inference(step,[status(thm)],[t1076,t375]) ).
cnf(t419,plain,
double_divide(sF2,inverse(X1)) = X1,
inference(orient,[status(thm)],[t1077]) ).
cnf(t427,plain,
sF1 = double_divide(X1,inverse(double_divide(sF2,inverse(double_divide(sF2,inverse(X1)))))),
inference(cp,[status(thm)],[t59,t419]) ).
cnf(t1078,plain,
sF1 = double_divide(X1,inverse(double_divide(sF2,inverse(X1)))),
inference(step,[status(thm)],[t427,t419]) ).
cnf(t1079,plain,
sF1 = double_divide(X1,inverse(X1)),
inference(step,[status(thm)],[t1078,t419]) ).
cnf(t462,plain,
double_divide(X1,inverse(X1)) = sF1,
inference(orient,[status(thm)],[t1079]) ).
cnf(t465,plain,
sF1 = sF2,
inference(cp,[status(thm)],[t462,t419]) ).
cnf(t480,plain,
sF2 = sF1,
inference(orient,[status(thm)],[t465]) ).
cnf(t1089,plain,
double_divide(inverse(X1),sF1) = X1,
inference(step,[status(thm)],[t375,t480]) ).
cnf(t489,plain,
double_divide(inverse(X1),sF1) = X1,
inference(rw,[status(thm)],[t1089]) ).
cnf(t547,plain,
double_divide(inverse(X1),sF1) = X1,
inference(orient,[status(thm)],[t489]) ).
cnf(t5,axiom,
sF4 = inverse(double_divide(a2,inverse(double_divide(b2,inverse(b2))))),
introduced(definition) ).
cnf(t1048,plain,
sF4 = inverse(double_divide(a2,inverse(double_divide(b2,sF0)))),
inference(step,[status(thm)],[t5,t6]) ).
cnf(t1049,plain,
sF4 = inverse(double_divide(a2,inverse(sF1))),
inference(step,[status(thm)],[t1048,t7]) ).
cnf(t1050,plain,
sF4 = inverse(double_divide(a2,sF2)),
inference(step,[status(thm)],[t1049,t8]) ).
cnf(t4,axiom,
sF3 = double_divide(a2,inverse(double_divide(b2,inverse(b2)))),
introduced(definition) ).
cnf(t1045,plain,
sF3 = double_divide(a2,inverse(double_divide(b2,sF0))),
inference(step,[status(thm)],[t4,t6]) ).
cnf(t1046,plain,
sF3 = double_divide(a2,inverse(sF1)),
inference(step,[status(thm)],[t1045,t7]) ).
cnf(t1047,plain,
sF3 = double_divide(a2,sF2),
inference(step,[status(thm)],[t1046,t8]) ).
cnf(t9,plain,
double_divide(a2,sF2) = sF3,
inference(orient,[status(thm)],[t1047]) ).
cnf(t1051,plain,
sF4 = inverse(sF3),
inference(step,[status(thm)],[t1050,t9]) ).
cnf(t10,plain,
inverse(sF3) = sF4,
inference(orient,[status(thm)],[t1051]) ).
cnf(t223,plain,
sF3 = double_divide(X1,inverse(double_divide(sF4,inverse(X1)))),
inference(cp,[status(thm)],[t218,t10]) ).
cnf(t619,plain,
double_divide(X1,inverse(double_divide(sF4,inverse(X1)))) = sF3,
inference(orient,[status(thm)],[t223]) ).
cnf(t12,plain,
b2 = double_divide(double_divide(X1,X2),inverse(double_divide(X1,inverse(double_divide(sF0,X2))))),
inference(cp,[status(thm)],[t11,t6]) ).
cnf(t30,plain,
double_divide(double_divide(X1,X2),inverse(double_divide(X1,inverse(double_divide(sF0,X2))))) = b2,
inference(orient,[status(thm)],[t12]) ).
cnf(t550,plain,
b2 = double_divide(X1,inverse(double_divide(inverse(X1),inverse(double_divide(sF0,sF1))))),
inference(cp,[status(thm)],[t30,t547]) ).
cnf(t219,plain,
b2 = double_divide(X1,inverse(double_divide(sF0,inverse(X1)))),
inference(cp,[status(thm)],[t218,t6]) ).
cnf(t245,plain,
double_divide(X1,inverse(double_divide(sF0,inverse(X1)))) = b2,
inference(orient,[status(thm)],[t219]) ).
cnf(t247,plain,
b2 = double_divide(sF1,inverse(double_divide(sF0,sF2))),
inference(cp,[status(thm)],[t245,t8]) ).
cnf(t275,plain,
double_divide(sF1,inverse(double_divide(sF0,sF2))) = b2,
inference(orient,[status(thm)],[t247]) ).
cnf(t1066,plain,
double_divide(sF0,sF2) = b2,
inference(step,[status(thm)],[t275,t297]) ).
cnf(t300,plain,
double_divide(sF0,sF2) = b2,
inference(rw,[status(thm)],[t1066]) ).
cnf(t309,plain,
double_divide(sF0,sF2) = b2,
inference(orient,[status(thm)],[t300]) ).
cnf(t1088,plain,
double_divide(sF0,sF1) = b2,
inference(step,[status(thm)],[t309,t480]) ).
cnf(t488,plain,
double_divide(sF0,sF1) = b2,
inference(rw,[status(thm)],[t1088]) ).
cnf(t505,plain,
double_divide(sF0,sF1) = b2,
inference(orient,[status(thm)],[t488]) ).
cnf(t1119,plain,
b2 = double_divide(X1,inverse(double_divide(inverse(X1),inverse(b2)))),
inference(step,[status(thm)],[t550,t505]) ).
cnf(t1120,plain,
b2 = double_divide(X1,inverse(double_divide(inverse(X1),sF0))),
inference(step,[status(thm)],[t1119,t6]) ).
cnf(t956,plain,
double_divide(X1,inverse(double_divide(inverse(X1),sF0))) = b2,
inference(orient,[status(thm)],[t1120]) ).
cnf(t975,plain,
sF3 = double_divide(double_divide(inverse(sF4),sF0),inverse(b2)),
inference(cp,[status(thm)],[t619,t956]) ).
cnf(t1124,plain,
sF3 = double_divide(double_divide(inverse(sF4),sF0),sF0),
inference(step,[status(thm)],[t975,t6]) ).
cnf(t41,plain,
X1 = double_divide(double_divide(double_divide(inverse(X1),X2),inverse(double_divide(sF0,X2))),inverse(b2)),
inference(cp,[status(thm)],[t11,t30]) ).
cnf(t1101,plain,
X1 = double_divide(double_divide(double_divide(inverse(X1),X2),inverse(double_divide(sF0,X2))),sF0),
inference(step,[status(thm)],[t41,t6]) ).
cnf(t673,plain,
double_divide(double_divide(double_divide(inverse(X1),X2),inverse(double_divide(sF0,X2))),sF0) = X1,
inference(orient,[status(thm)],[t1101]) ).
cnf(t679,plain,
X1 = double_divide(double_divide(double_divide(inverse(X1),inverse(double_divide(sF0,inverse(sF0)))),inverse(b2)),sF0),
inference(cp,[status(thm)],[t673,t245]) ).
cnf(t1102,plain,
X1 = double_divide(double_divide(double_divide(inverse(X1),inverse(sF1)),inverse(b2)),sF0),
inference(step,[status(thm)],[t679,t462]) ).
cnf(t1080,plain,
inverse(sF1) = sF1,
inference(step,[status(thm)],[t8,t480]) ).
cnf(t481,plain,
inverse(sF1) = sF1,
inference(orient,[status(thm)],[t1080]) ).
cnf(t1103,plain,
X1 = double_divide(double_divide(double_divide(inverse(X1),sF1),inverse(b2)),sF0),
inference(step,[status(thm)],[t1102,t481]) ).
cnf(t1104,plain,
X1 = double_divide(double_divide(X1,inverse(b2)),sF0),
inference(step,[status(thm)],[t1103,t547]) ).
cnf(t1105,plain,
X1 = double_divide(double_divide(X1,sF0),sF0),
inference(step,[status(thm)],[t1104,t6]) ).
cnf(t690,plain,
double_divide(double_divide(X1,sF0),sF0) = X1,
inference(orient,[status(thm)],[t1105]) ).
cnf(t1125,plain,
sF3 = inverse(sF4),
inference(step,[status(thm)],[t1124,t690]) ).
cnf(t1006,plain,
inverse(sF4) = sF3,
inference(orient,[status(thm)],[t1125]) ).
cnf(t1021,plain,
sF4 = double_divide(sF3,sF1),
inference(cp,[status(thm)],[t547,t1006]) ).
cnf(t15,plain,
X1 = double_divide(sF3,inverse(double_divide(a2,inverse(double_divide(inverse(X1),sF2))))),
inference(cp,[status(thm)],[t11,t9]) ).
cnf(t45,plain,
double_divide(sF3,inverse(double_divide(a2,inverse(double_divide(inverse(X1),sF2))))) = X1,
inference(orient,[status(thm)],[t15]) ).
cnf(t1068,plain,
double_divide(sF3,inverse(double_divide(a2,inverse(X1)))) = X1,
inference(step,[status(thm)],[t45,t375]) ).
cnf(t376,plain,
double_divide(sF3,inverse(double_divide(a2,inverse(X1)))) = X1,
inference(rw,[status(thm)],[t1068]) ).
cnf(t739,plain,
double_divide(sF3,inverse(double_divide(a2,inverse(X1)))) = X1,
inference(orient,[status(thm)],[t376]) ).
cnf(t745,plain,
a2 = double_divide(sF3,inverse(sF1)),
inference(cp,[status(thm)],[t739,t462]) ).
cnf(t1108,plain,
a2 = double_divide(sF3,sF1),
inference(step,[status(thm)],[t745,t481]) ).
cnf(t754,plain,
double_divide(sF3,sF1) = a2,
inference(orient,[status(thm)],[t1108]) ).
cnf(t1127,plain,
sF4 = a2,
inference(step,[status(thm)],[t1021,t754]) ).
cnf(t1030,plain,
a2 = sF4,
inference(orient,[status(thm)],[t1127]) ).
cnf(t378,plain,
sF3 = double_divide(sF4,sF2),
inference(cp,[status(thm)],[t375,t10]) ).
cnf(t398,plain,
double_divide(sF4,sF2) = sF3,
inference(orient,[status(thm)],[t378]) ).
cnf(t1092,plain,
double_divide(sF4,sF1) = sF3,
inference(step,[status(thm)],[t398,t480]) ).
cnf(t491,plain,
double_divide(sF4,sF1) = sF3,
inference(rw,[status(thm)],[t1092]) ).
cnf(t512,plain,
double_divide(sF4,sF1) = sF3,
inference(orient,[status(thm)],[t491]) ).
cnf(u0,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
multiply(A,B) = inverse(double_divide(B,A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
inverse(double_divide(a2,inverse(double_divide(b2,inverse(b2))))) != a2,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(g0_0,plain,
inverse(double_divide(sF4,inverse(double_divide(b2,inverse(b2))))) != a2,
inference(rw,[status(thm)],[goal_0,t1030]) ).
cnf(g0_1,plain,
inverse(double_divide(sF4,inverse(sF1))) != a2,
inference(rw,[status(thm)],[g0_0,t462]) ).
cnf(g0_2,plain,
inverse(double_divide(sF4,sF1)) != a2,
inference(rw,[status(thm)],[g0_1,t481]) ).
cnf(g0_3,plain,
inverse(sF3) != a2,
inference(rw,[status(thm)],[g0_2,t512]) ).
cnf(g0_4,plain,
sF4 != a2,
inference(rw,[status(thm)],[g0_3,t10]) ).
cnf(g0_5,plain,
sF4 != sF4,
inference(rw,[status(thm)],[g0_4,t1030]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP598-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.37 % Computer : n009.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 15:10:43 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 5.46/1.21 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.46/1.21 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------