%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP498-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 : n013.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:11 PM UTC 2026
% Result : Unsatisfiable 5.66s 11.19s
% Output : CNFRefutation 5.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 5
% Syntax : Number of clauses : 106 ( 106 unt; 0 nHn; 5 RR)
% Number of literals : 106 ( 105 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 178 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t2,axiom,
double_divide(double_divide(X1,X2),identity) = multiply(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t0,axiom,
double_divide(X1,identity) = inverse(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t8,plain,
double_divide(X1,identity) = inverse(X1),
inference(orient,[status(thm)],[t0]) ).
cnf(t658,plain,
inverse(double_divide(X1,X2)) = multiply(X2,X1),
inference(step,[status(thm)],[t2,t8]) ).
cnf(t11,plain,
inverse(double_divide(X1,X2)) = multiply(X2,X1),
inference(orient,[status(thm)],[t658]) ).
cnf(t3,axiom,
double_divide(double_divide(identity,double_divide(X1,double_divide(X2,identity))),double_divide(double_divide(X2,double_divide(X3,X1)),identity)) = X3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t4,plain,
double_divide(double_divide(identity,double_divide(X1,double_divide(X2,identity))),double_divide(double_divide(X2,double_divide(X3,X1)),identity)) = X3,
inference(orient,[status(thm)],[t3]) ).
cnf(t656,plain,
double_divide(double_divide(identity,double_divide(X1,inverse(X2))),double_divide(double_divide(X2,double_divide(X3,X1)),identity)) = X3,
inference(step,[status(thm)],[t4,t8]) ).
cnf(t657,plain,
double_divide(double_divide(identity,double_divide(X1,inverse(X2))),inverse(double_divide(X2,double_divide(X3,X1)))) = X3,
inference(step,[status(thm)],[t656,t8]) ).
cnf(t9,plain,
double_divide(double_divide(identity,double_divide(X1,inverse(X2))),inverse(double_divide(X2,double_divide(X3,X1)))) = X3,
inference(rw,[status(thm)],[t657]) ).
cnf(t659,plain,
double_divide(double_divide(identity,double_divide(X1,inverse(X2))),multiply(double_divide(X3,X1),X2)) = X3,
inference(step,[status(thm)],[t9,t11]) ).
cnf(t70,plain,
double_divide(double_divide(identity,double_divide(X1,inverse(X2))),multiply(double_divide(X3,X1),X2)) = X3,
inference(orient,[status(thm)],[t659]) ).
cnf(t1,axiom,
double_divide(X1,inverse(X1)) = identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t10,plain,
double_divide(X1,inverse(X1)) = identity,
inference(orient,[status(thm)],[t1]) ).
cnf(t72,plain,
X1 = double_divide(double_divide(identity,identity),multiply(double_divide(X1,X2),X2)),
inference(cp,[status(thm)],[t70,t10]) ).
cnf(t672,plain,
X1 = double_divide(inverse(identity),multiply(double_divide(X1,X2),X2)),
inference(step,[status(thm)],[t72,t8]) ).
cnf(t14,plain,
identity = double_divide(double_divide(X1,X2),multiply(X2,X1)),
inference(cp,[status(thm)],[t10,t11]) ).
cnf(t35,plain,
double_divide(double_divide(X1,X2),multiply(X2,X1)) = identity,
inference(orient,[status(thm)],[t14]) ).
cnf(t71,plain,
inverse(identity) = identity,
inference(cp,[status(thm)],[t70,t35]) ).
cnf(t88,plain,
inverse(identity) = identity,
inference(orient,[status(thm)],[t71]) ).
cnf(t673,plain,
X1 = double_divide(identity,multiply(double_divide(X1,X2),X2)),
inference(step,[status(thm)],[t672,t88]) ).
cnf(t113,plain,
double_divide(identity,multiply(double_divide(X1,X2),X2)) = X1,
inference(orient,[status(thm)],[t673]) ).
cnf(t114,plain,
X1 = double_divide(identity,multiply(inverse(X1),identity)),
inference(cp,[status(thm)],[t113,t8]) ).
cnf(t128,plain,
double_divide(identity,multiply(inverse(X1),identity)) = X1,
inference(orient,[status(thm)],[t114]) ).
cnf(t12,plain,
multiply(identity,X1) = inverse(inverse(X1)),
inference(cp,[status(thm)],[t11,t8]) ).
cnf(t15,plain,
inverse(inverse(X1)) = multiply(identity,X1),
inference(orient,[status(thm)],[t12]) ).
cnf(t131,plain,
inverse(X1) = double_divide(identity,multiply(multiply(identity,X1),identity)),
inference(cp,[status(thm)],[t128,t15]) ).
cnf(t174,plain,
double_divide(identity,multiply(multiply(identity,X1),identity)) = inverse(X1),
inference(orient,[status(thm)],[t131]) ).
cnf(t115,plain,
X1 = double_divide(identity,multiply(identity,inverse(X1))),
inference(cp,[status(thm)],[t113,t10]) ).
cnf(t138,plain,
double_divide(identity,multiply(identity,inverse(X1))) = X1,
inference(orient,[status(thm)],[t115]) ).
cnf(t145,plain,
multiply(multiply(identity,inverse(X1)),identity) = inverse(X1),
inference(cp,[status(thm)],[t11,t138]) ).
cnf(t152,plain,
multiply(multiply(identity,inverse(X1)),identity) = inverse(X1),
inference(orient,[status(thm)],[t145]) ).
cnf(t175,plain,
inverse(inverse(X1)) = double_divide(identity,inverse(X1)),
inference(cp,[status(thm)],[t174,t152]) ).
cnf(t674,plain,
multiply(identity,X1) = double_divide(identity,inverse(X1)),
inference(step,[status(thm)],[t175,t15]) ).
cnf(t183,plain,
double_divide(identity,inverse(X1)) = multiply(identity,X1),
inference(orient,[status(thm)],[t674]) ).
cnf(t18,plain,
multiply(identity,inverse(X1)) = inverse(multiply(identity,X1)),
inference(cp,[status(thm)],[t15,t15]) ).
cnf(t22,plain,
inverse(multiply(identity,X1)) = multiply(identity,inverse(X1)),
inference(orient,[status(thm)],[t18]) ).
cnf(t184,plain,
multiply(identity,multiply(identity,X1)) = double_divide(identity,multiply(identity,inverse(X1))),
inference(cp,[status(thm)],[t183,t22]) ).
cnf(t675,plain,
multiply(identity,multiply(identity,X1)) = X1,
inference(step,[status(thm)],[t184,t138]) ).
cnf(t193,plain,
multiply(identity,multiply(identity,X1)) = X1,
inference(orient,[status(thm)],[t675]) ).
cnf(t16,plain,
multiply(identity,double_divide(X1,X2)) = inverse(multiply(X2,X1)),
inference(cp,[status(thm)],[t15,t11]) ).
cnf(t30,plain,
multiply(identity,double_divide(X1,X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t16]) ).
cnf(t194,plain,
double_divide(X1,X2) = multiply(identity,inverse(multiply(X2,X1))),
inference(cp,[status(thm)],[t193,t30]) ).
cnf(t291,plain,
multiply(identity,inverse(multiply(X1,X2))) = double_divide(X2,X1),
inference(orient,[status(thm)],[t194]) ).
cnf(t17,plain,
identity = double_divide(inverse(X1),multiply(identity,X1)),
inference(cp,[status(thm)],[t10,t15]) ).
cnf(t25,plain,
double_divide(inverse(X1),multiply(identity,X1)) = identity,
inference(orient,[status(thm)],[t17]) ).
cnf(t121,plain,
inverse(X1) = double_divide(identity,multiply(identity,multiply(identity,X1))),
inference(cp,[status(thm)],[t113,t25]) ).
cnf(t156,plain,
double_divide(identity,multiply(identity,multiply(identity,X1))) = inverse(X1),
inference(orient,[status(thm)],[t121]) ).
cnf(t676,plain,
double_divide(identity,X1) = inverse(X1),
inference(step,[status(thm)],[t156,t193]) ).
cnf(t200,plain,
double_divide(identity,X1) = inverse(X1),
inference(rw,[status(thm)],[t676]) ).
cnf(t203,plain,
double_divide(identity,X1) = inverse(X1),
inference(orient,[status(thm)],[t200]) ).
cnf(t681,plain,
inverse(multiply(double_divide(X1,X2),X2)) = X1,
inference(step,[status(thm)],[t113,t203]) ).
cnf(t210,plain,
inverse(multiply(double_divide(X1,X2),X2)) = X1,
inference(rw,[status(thm)],[t681]) ).
cnf(t278,plain,
inverse(multiply(double_divide(X1,X2),X2)) = X1,
inference(orient,[status(thm)],[t210]) ).
cnf(t292,plain,
double_divide(X1,double_divide(X2,X1)) = multiply(identity,X2),
inference(cp,[status(thm)],[t291,t278]) ).
cnf(t299,plain,
double_divide(X1,double_divide(X2,X1)) = multiply(identity,X2),
inference(orient,[status(thm)],[t292]) ).
cnf(t300,plain,
multiply(identity,X1) = double_divide(double_divide(X2,X1),multiply(identity,X2)),
inference(cp,[status(thm)],[t299,t299]) ).
cnf(t308,plain,
double_divide(double_divide(X1,X2),multiply(identity,X1)) = multiply(identity,X2),
inference(orient,[status(thm)],[t300]) ).
cnf(t206,plain,
inverse(multiply(X1,identity)) = multiply(identity,inverse(X1)),
inference(cp,[status(thm)],[t30,t203]) ).
cnf(t235,plain,
inverse(multiply(X1,identity)) = multiply(identity,inverse(X1)),
inference(orient,[status(thm)],[t206]) ).
cnf(t241,plain,
multiply(identity,multiply(X1,identity)) = inverse(multiply(identity,inverse(X1))),
inference(cp,[status(thm)],[t15,t235]) ).
cnf(t686,plain,
multiply(identity,multiply(X1,identity)) = multiply(identity,inverse(inverse(X1))),
inference(step,[status(thm)],[t241,t22]) ).
cnf(t687,plain,
multiply(identity,multiply(X1,identity)) = multiply(identity,multiply(identity,X1)),
inference(step,[status(thm)],[t686,t15]) ).
cnf(t688,plain,
multiply(identity,multiply(X1,identity)) = X1,
inference(step,[status(thm)],[t687,t193]) ).
cnf(t244,plain,
multiply(identity,multiply(X1,identity)) = X1,
inference(orient,[status(thm)],[t688]) ).
cnf(t312,plain,
multiply(identity,X1) = double_divide(double_divide(multiply(X2,identity),X1),X2),
inference(cp,[status(thm)],[t308,t244]) ).
cnf(t430,plain,
double_divide(double_divide(multiply(X1,identity),X2),X1) = multiply(identity,X2),
inference(orient,[status(thm)],[t312]) ).
cnf(t682,plain,
double_divide(inverse(double_divide(X1,inverse(X2))),multiply(double_divide(X3,X1),X2)) = X3,
inference(step,[status(thm)],[t70,t203]) ).
cnf(t683,plain,
double_divide(multiply(inverse(X2),X1),multiply(double_divide(X3,X1),X2)) = X3,
inference(step,[status(thm)],[t682,t11]) ).
cnf(t211,plain,
double_divide(multiply(inverse(X2),X1),multiply(double_divide(X3,X1),X2)) = X3,
inference(rw,[status(thm)],[t683]) ).
cnf(t385,plain,
double_divide(multiply(inverse(X1),X2),multiply(double_divide(X3,X2),X1)) = X3,
inference(orient,[status(thm)],[t211]) ).
cnf(t432,plain,
multiply(identity,multiply(double_divide(X1,identity),X2)) = double_divide(X1,inverse(X2)),
inference(cp,[status(thm)],[t430,t385]) ).
cnf(t697,plain,
multiply(identity,multiply(inverse(X1),X2)) = double_divide(X1,inverse(X2)),
inference(step,[status(thm)],[t432,t8]) ).
cnf(t440,plain,
multiply(identity,multiply(inverse(X1),X2)) = double_divide(X1,inverse(X2)),
inference(orient,[status(thm)],[t697]) ).
cnf(t443,plain,
double_divide(identity,inverse(X1)) = multiply(identity,multiply(identity,X1)),
inference(cp,[status(thm)],[t440,t88]) ).
cnf(t698,plain,
multiply(identity,X1) = multiply(identity,multiply(identity,X1)),
inference(step,[status(thm)],[t443,t183]) ).
cnf(t699,plain,
multiply(identity,X1) = X1,
inference(step,[status(thm)],[t698,t193]) ).
cnf(t463,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t699]) ).
cnf(t715,plain,
double_divide(double_divide(X1,X2),X1) = multiply(identity,X2),
inference(step,[status(thm)],[t308,t463]) ).
cnf(t716,plain,
double_divide(double_divide(X1,X2),X1) = X2,
inference(step,[status(thm)],[t715,t463]) ).
cnf(t482,plain,
double_divide(double_divide(X1,X2),X1) = X2,
inference(rw,[status(thm)],[t716]) ).
cnf(t513,plain,
double_divide(double_divide(X1,X2),X1) = X2,
inference(orient,[status(thm)],[t482]) ).
cnf(t517,plain,
multiply(X1,double_divide(X1,X2)) = inverse(X2),
inference(cp,[status(thm)],[t11,t513]) ).
cnf(t530,plain,
multiply(X1,double_divide(X1,X2)) = inverse(X2),
inference(orient,[status(thm)],[t517]) ).
cnf(t532,plain,
inverse(multiply(double_divide(X1,X2),X3)) = multiply(multiply(inverse(X3),X2),X1),
inference(cp,[status(thm)],[t530,t385]) ).
cnf(t719,plain,
double_divide(X1,X2) = inverse(multiply(X2,X1)),
inference(step,[status(thm)],[t30,t463]) ).
cnf(t485,plain,
double_divide(X1,X2) = inverse(multiply(X2,X1)),
inference(rw,[status(thm)],[t719]) ).
cnf(t509,plain,
inverse(multiply(X1,X2)) = double_divide(X2,X1),
inference(orient,[status(thm)],[t485]) ).
cnf(t744,plain,
double_divide(X3,double_divide(X1,X2)) = multiply(multiply(inverse(X3),X2),X1),
inference(step,[status(thm)],[t532,t509]) ).
cnf(t631,plain,
multiply(multiply(inverse(X1),X2),X3) = double_divide(X1,double_divide(X3,X2)),
inference(orient,[status(thm)],[t744]) ).
cnf(t700,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t15,t463]) ).
cnf(t464,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t700]) ).
cnf(t638,plain,
double_divide(inverse(X1),double_divide(X2,X3)) = multiply(multiply(X1,X3),X2),
inference(cp,[status(thm)],[t631,t464]) ).
cnf(t721,plain,
multiply(inverse(X1),X2) = double_divide(X1,inverse(X2)),
inference(step,[status(thm)],[t440,t463]) ).
cnf(t487,plain,
multiply(inverse(X1),X2) = double_divide(X1,inverse(X2)),
inference(rw,[status(thm)],[t721]) ).
cnf(t519,plain,
double_divide(X1,inverse(X2)) = multiply(inverse(X1),X2),
inference(orient,[status(thm)],[t487]) ).
cnf(t523,plain,
multiply(inverse(X1),inverse(X2)) = double_divide(X1,X2),
inference(cp,[status(thm)],[t519,t464]) ).
cnf(t535,plain,
multiply(inverse(X1),inverse(X2)) = double_divide(X1,X2),
inference(orient,[status(thm)],[t523]) ).
cnf(t538,plain,
double_divide(inverse(X1),X2) = multiply(X1,inverse(X2)),
inference(cp,[status(thm)],[t535,t464]) ).
cnf(t544,plain,
double_divide(inverse(X1),X2) = multiply(X1,inverse(X2)),
inference(orient,[status(thm)],[t538]) ).
cnf(t745,plain,
multiply(X1,inverse(double_divide(X2,X3))) = multiply(multiply(X1,X3),X2),
inference(step,[status(thm)],[t638,t544]) ).
cnf(t746,plain,
multiply(X1,multiply(X3,X2)) = multiply(multiply(X1,X3),X2),
inference(step,[status(thm)],[t745,t11]) ).
cnf(t642,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t746]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)),
inference(rw,[status(thm)],[goal_0,t642]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP498-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.12/10.38 % Computer : n013.cluster.edu
% 0.12/10.38 % Model : x86_64 x86_64
% 0.12/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.38 % Memory : 8046.5625MB
% 0.12/10.38 % OS : Linux 6.8.0-71-generic
% 0.12/10.38 % CPULimit : 300
% 0.12/10.38 % WCLimit : 300
% 0.12/10.38 % DateTime : Wed Sep 23 14:54:48 UTC 2026
% 0.12/10.38 % CPUTime :
% 0.12/10.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 5.66/11.19 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.66/11.19 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------