%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP483-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 : n014.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:09 PM UTC 2026
% Result : Unsatisfiable 5.71s 6.15s
% Output : CNFRefutation 5.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 5
% Syntax : Number of clauses : 119 ( 119 unt; 0 nHn; 5 RR)
% Number of literals : 119 ( 118 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 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 : 217 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t2,axiom,
double_divide(double_divide(X1,X2),identity) = multiply(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t0,axiom,
double_divide(X1,identity) = inverse(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t11,plain,
double_divide(X1,identity) = inverse(X1),
inference(orient,[status(thm)],[t0]) ).
cnf(t733,plain,
inverse(double_divide(X1,X2)) = multiply(X2,X1),
inference(step,[status(thm)],[t2,t11]) ).
cnf(t14,plain,
inverse(double_divide(X1,X2)) = multiply(X2,X1),
inference(orient,[status(thm)],[t733]) ).
cnf(t3,axiom,
double_divide(double_divide(double_divide(X1,double_divide(X2,identity)),double_divide(double_divide(X3,double_divide(X4,double_divide(X4,identity))),double_divide(X1,identity))),X2) = X3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t4,plain,
double_divide(double_divide(double_divide(X1,double_divide(X2,identity)),double_divide(double_divide(X3,double_divide(X4,double_divide(X4,identity))),double_divide(X1,identity))),X2) = X3,
inference(orient,[status(thm)],[t3]) ).
cnf(t730,plain,
double_divide(double_divide(double_divide(X1,inverse(X2)),double_divide(double_divide(X3,double_divide(X4,double_divide(X4,identity))),double_divide(X1,identity))),X2) = X3,
inference(step,[status(thm)],[t4,t11]) ).
cnf(t731,plain,
double_divide(double_divide(double_divide(X1,inverse(X2)),double_divide(double_divide(X3,double_divide(X4,inverse(X4))),double_divide(X1,identity))),X2) = X3,
inference(step,[status(thm)],[t730,t11]) ).
cnf(t732,plain,
double_divide(double_divide(double_divide(X1,inverse(X2)),double_divide(double_divide(X3,double_divide(X4,inverse(X4))),inverse(X1))),X2) = X3,
inference(step,[status(thm)],[t731,t11]) ).
cnf(t12,plain,
double_divide(double_divide(double_divide(X1,inverse(X2)),double_divide(double_divide(X3,double_divide(X4,inverse(X4))),inverse(X1))),X2) = X3,
inference(rw,[status(thm)],[t732]) ).
cnf(t1,axiom,
double_divide(X1,inverse(X1)) = identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t13,plain,
double_divide(X1,inverse(X1)) = identity,
inference(orient,[status(thm)],[t1]) ).
cnf(t734,plain,
double_divide(double_divide(double_divide(X1,inverse(X2)),double_divide(double_divide(X3,identity),inverse(X1))),X2) = X3,
inference(step,[status(thm)],[t12,t13]) ).
cnf(t735,plain,
double_divide(double_divide(double_divide(X1,inverse(X2)),double_divide(inverse(X3),inverse(X1))),X2) = X3,
inference(step,[status(thm)],[t734,t11]) ).
cnf(t83,plain,
double_divide(double_divide(double_divide(X1,inverse(X2)),double_divide(inverse(X3),inverse(X1))),X2) = X3,
inference(orient,[status(thm)],[t735]) ).
cnf(t89,plain,
X1 = double_divide(double_divide(double_divide(inverse(X1),inverse(X2)),identity),X2),
inference(cp,[status(thm)],[t83,t13]) ).
cnf(t736,plain,
X1 = double_divide(inverse(double_divide(inverse(X1),inverse(X2))),X2),
inference(step,[status(thm)],[t89,t11]) ).
cnf(t737,plain,
X1 = double_divide(multiply(inverse(X2),inverse(X1)),X2),
inference(step,[status(thm)],[t736,t14]) ).
cnf(t101,plain,
double_divide(multiply(inverse(X1),inverse(X2)),X1) = X2,
inference(orient,[status(thm)],[t737]) ).
cnf(t16,plain,
multiply(inverse(X1),X1) = inverse(identity),
inference(cp,[status(thm)],[t14,t13]) ).
cnf(t22,plain,
multiply(inverse(X1),X1) = inverse(identity),
inference(orient,[status(thm)],[t16]) ).
cnf(t103,plain,
X1 = double_divide(inverse(identity),inverse(X1)),
inference(cp,[status(thm)],[t101,t22]) ).
cnf(t115,plain,
double_divide(inverse(identity),inverse(X1)) = X1,
inference(orient,[status(thm)],[t103]) ).
cnf(t116,plain,
inverse(identity) = identity,
inference(cp,[status(thm)],[t115,t13]) ).
cnf(t126,plain,
inverse(identity) = identity,
inference(orient,[status(thm)],[t116]) ).
cnf(t152,plain,
X1 = double_divide(double_divide(double_divide(X2,identity),double_divide(inverse(X1),inverse(X2))),identity),
inference(cp,[status(thm)],[t83,t126]) ).
cnf(t787,plain,
X1 = inverse(double_divide(double_divide(X2,identity),double_divide(inverse(X1),inverse(X2)))),
inference(step,[status(thm)],[t152,t11]) ).
cnf(t788,plain,
X1 = multiply(double_divide(inverse(X1),inverse(X2)),double_divide(X2,identity)),
inference(step,[status(thm)],[t787,t14]) ).
cnf(t789,plain,
X1 = multiply(double_divide(inverse(X1),inverse(X2)),inverse(X2)),
inference(step,[status(thm)],[t788,t11]) ).
cnf(t279,plain,
multiply(double_divide(inverse(X1),inverse(X2)),inverse(X2)) = X1,
inference(orient,[status(thm)],[t789]) ).
cnf(t15,plain,
multiply(identity,X1) = inverse(inverse(X1)),
inference(cp,[status(thm)],[t14,t11]) ).
cnf(t18,plain,
inverse(inverse(X1)) = multiply(identity,X1),
inference(orient,[status(thm)],[t15]) ).
cnf(t23,plain,
inverse(identity) = multiply(multiply(X1,X2),double_divide(X2,X1)),
inference(cp,[status(thm)],[t22,t14]) ).
cnf(t42,plain,
multiply(multiply(X1,X2),double_divide(X2,X1)) = inverse(identity),
inference(orient,[status(thm)],[t23]) ).
cnf(t742,plain,
multiply(multiply(X1,X2),double_divide(X2,X1)) = identity,
inference(step,[status(thm)],[t42,t126]) ).
cnf(t131,plain,
multiply(multiply(X1,X2),double_divide(X2,X1)) = identity,
inference(orient,[status(thm)],[t742]) ).
cnf(t147,plain,
identity = double_divide(multiply(inverse(X1),identity),X1),
inference(cp,[status(thm)],[t101,t126]) ).
cnf(t752,plain,
double_divide(identity,inverse(X1)) = X1,
inference(step,[status(thm)],[t115,t126]) ).
cnf(t158,plain,
double_divide(identity,inverse(X1)) = X1,
inference(rw,[status(thm)],[t752]) ).
cnf(t160,plain,
double_divide(identity,inverse(X1)) = X1,
inference(orient,[status(thm)],[t158]) ).
cnf(t167,plain,
multiply(inverse(X1),identity) = inverse(X1),
inference(cp,[status(thm)],[t14,t160]) ).
cnf(t169,plain,
multiply(inverse(X1),identity) = inverse(X1),
inference(orient,[status(thm)],[t167]) ).
cnf(t767,plain,
identity = double_divide(inverse(X1),X1),
inference(step,[status(thm)],[t147,t169]) ).
cnf(t215,plain,
double_divide(inverse(X1),X1) = identity,
inference(orient,[status(thm)],[t767]) ).
cnf(t219,plain,
identity = multiply(multiply(X1,inverse(X1)),identity),
inference(cp,[status(thm)],[t131,t215]) ).
cnf(t21,plain,
multiply(identity,inverse(X1)) = inverse(multiply(identity,X1)),
inference(cp,[status(thm)],[t18,t18]) ).
cnf(t25,plain,
inverse(multiply(identity,X1)) = multiply(identity,inverse(X1)),
inference(orient,[status(thm)],[t21]) ).
cnf(t163,plain,
inverse(X1) = double_divide(identity,multiply(identity,X1)),
inference(cp,[status(thm)],[t160,t18]) ).
cnf(t181,plain,
double_divide(identity,multiply(identity,X1)) = inverse(X1),
inference(orient,[status(thm)],[t163]) ).
cnf(t146,plain,
X1 = double_divide(multiply(identity,inverse(X1)),identity),
inference(cp,[status(thm)],[t101,t126]) ).
cnf(t753,plain,
X1 = inverse(multiply(identity,inverse(X1))),
inference(step,[status(thm)],[t146,t11]) ).
cnf(t754,plain,
X1 = multiply(identity,inverse(inverse(X1))),
inference(step,[status(thm)],[t753,t25]) ).
cnf(t755,plain,
X1 = multiply(identity,multiply(identity,X1)),
inference(step,[status(thm)],[t754,t18]) ).
cnf(t173,plain,
multiply(identity,multiply(identity,X1)) = X1,
inference(orient,[status(thm)],[t755]) ).
cnf(t182,plain,
inverse(multiply(identity,X1)) = double_divide(identity,X1),
inference(cp,[status(thm)],[t181,t173]) ).
cnf(t758,plain,
multiply(identity,inverse(X1)) = double_divide(identity,X1),
inference(step,[status(thm)],[t182,t25]) ).
cnf(t187,plain,
multiply(identity,inverse(X1)) = double_divide(identity,X1),
inference(orient,[status(thm)],[t758]) ).
cnf(t759,plain,
inverse(multiply(identity,X1)) = double_divide(identity,X1),
inference(step,[status(thm)],[t25,t187]) ).
cnf(t188,plain,
inverse(multiply(identity,X1)) = double_divide(identity,X1),
inference(orient,[status(thm)],[t759]) ).
cnf(t198,plain,
double_divide(identity,inverse(X1)) = inverse(double_divide(identity,X1)),
inference(cp,[status(thm)],[t188,t187]) ).
cnf(t763,plain,
X1 = inverse(double_divide(identity,X1)),
inference(step,[status(thm)],[t198,t160]) ).
cnf(t764,plain,
X1 = multiply(X1,identity),
inference(step,[status(thm)],[t763,t14]) ).
cnf(t201,plain,
multiply(X1,identity) = X1,
inference(orient,[status(thm)],[t764]) ).
cnf(t768,plain,
identity = multiply(X1,inverse(X1)),
inference(step,[status(thm)],[t219,t201]) ).
cnf(t224,plain,
multiply(X1,inverse(X1)) = identity,
inference(orient,[status(thm)],[t768]) ).
cnf(t228,plain,
inverse(X1) = double_divide(identity,X1),
inference(cp,[status(thm)],[t101,t224]) ).
cnf(t229,plain,
double_divide(identity,X1) = inverse(X1),
inference(orient,[status(thm)],[t228]) ).
cnf(t234,plain,
multiply(X1,identity) = inverse(inverse(X1)),
inference(cp,[status(thm)],[t14,t229]) ).
cnf(t779,plain,
X1 = inverse(inverse(X1)),
inference(step,[status(thm)],[t234,t201]) ).
cnf(t780,plain,
X1 = multiply(identity,X1),
inference(step,[status(thm)],[t779,t18]) ).
cnf(t239,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t780]) ).
cnf(t781,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t18,t239]) ).
cnf(t240,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t781]) ).
cnf(t285,plain,
X1 = multiply(double_divide(inverse(X1),X2),inverse(inverse(X2))),
inference(cp,[status(thm)],[t279,t240]) ).
cnf(t790,plain,
X1 = multiply(double_divide(inverse(X1),X2),X2),
inference(step,[status(thm)],[t285,t240]) ).
cnf(t296,plain,
multiply(double_divide(inverse(X1),X2),X2) = X1,
inference(orient,[status(thm)],[t790]) ).
cnf(t299,plain,
inverse(X1) = multiply(double_divide(X1,X2),X2),
inference(cp,[status(thm)],[t296,t240]) ).
cnf(t307,plain,
multiply(double_divide(X1,X2),X2) = inverse(X1),
inference(orient,[status(thm)],[t299]) ).
cnf(t223,plain,
inverse(X1) = double_divide(double_divide(double_divide(X1,inverse(X2)),identity),X2),
inference(cp,[status(thm)],[t83,t215]) ).
cnf(t784,plain,
inverse(X1) = double_divide(inverse(double_divide(X1,inverse(X2))),X2),
inference(step,[status(thm)],[t223,t11]) ).
cnf(t785,plain,
inverse(X1) = double_divide(multiply(inverse(X2),X1),X2),
inference(step,[status(thm)],[t784,t14]) ).
cnf(t251,plain,
double_divide(multiply(inverse(X1),X2),X1) = inverse(X2),
inference(orient,[status(thm)],[t785]) ).
cnf(t308,plain,
inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(cp,[status(thm)],[t307,t251]) ).
cnf(t162,plain,
double_divide(X1,X2) = double_divide(identity,multiply(X2,X1)),
inference(cp,[status(thm)],[t160,t14]) ).
cnf(t207,plain,
double_divide(identity,multiply(X1,X2)) = double_divide(X2,X1),
inference(orient,[status(thm)],[t162]) ).
cnf(t776,plain,
inverse(multiply(X1,X2)) = double_divide(X2,X1),
inference(step,[status(thm)],[t207,t229]) ).
cnf(t237,plain,
inverse(multiply(X1,X2)) = double_divide(X2,X1),
inference(rw,[status(thm)],[t776]) ).
cnf(t243,plain,
inverse(multiply(X1,X2)) = double_divide(X2,X1),
inference(orient,[status(thm)],[t237]) ).
cnf(t792,plain,
double_divide(X2,inverse(X1)) = multiply(inverse(X2),X1),
inference(step,[status(thm)],[t308,t243]) ).
cnf(t366,plain,
double_divide(X1,inverse(X2)) = multiply(inverse(X1),X2),
inference(orient,[status(thm)],[t792]) ).
cnf(t793,plain,
double_divide(double_divide(multiply(inverse(X1),X2),double_divide(inverse(X3),inverse(X1))),X2) = X3,
inference(step,[status(thm)],[t83,t366]) ).
cnf(t794,plain,
double_divide(double_divide(multiply(inverse(X1),X2),multiply(inverse(inverse(X3)),X1)),X2) = X3,
inference(step,[status(thm)],[t793,t366]) ).
cnf(t795,plain,
double_divide(double_divide(multiply(inverse(X1),X2),multiply(X3,X1)),X2) = X3,
inference(step,[status(thm)],[t794,t240]) ).
cnf(t378,plain,
double_divide(double_divide(multiply(inverse(X1),X2),multiply(X3,X1)),X2) = X3,
inference(rw,[status(thm)],[t795]) ).
cnf(t370,plain,
multiply(inverse(X1),double_divide(X2,X3)) = double_divide(X1,multiply(X3,X2)),
inference(cp,[status(thm)],[t366,t14]) ).
cnf(t421,plain,
multiply(inverse(X1),double_divide(X2,X3)) = double_divide(X1,multiply(X3,X2)),
inference(orient,[status(thm)],[t370]) ).
cnf(t422,plain,
double_divide(multiply(X1,X2),multiply(X3,X4)) = multiply(double_divide(X2,X1),double_divide(X4,X3)),
inference(cp,[status(thm)],[t421,t243]) ).
cnf(t585,plain,
double_divide(multiply(X1,X2),multiply(X3,X4)) = multiply(double_divide(X2,X1),double_divide(X4,X3)),
inference(orient,[status(thm)],[t422]) ).
cnf(t801,plain,
double_divide(multiply(double_divide(X2,inverse(X1)),double_divide(X1,X3)),X2) = X3,
inference(step,[status(thm)],[t378,t585]) ).
cnf(t802,plain,
double_divide(multiply(multiply(inverse(X2),X1),double_divide(X1,X3)),X2) = X3,
inference(step,[status(thm)],[t801,t366]) ).
cnf(t605,plain,
double_divide(multiply(multiply(inverse(X1),X2),double_divide(X2,X3)),X1) = X3,
inference(orient,[status(thm)],[t802]) ).
cnf(t315,plain,
double_divide(X1,double_divide(X2,X1)) = inverse(inverse(X2)),
inference(cp,[status(thm)],[t243,t307]) ).
cnf(t791,plain,
double_divide(X1,double_divide(X2,X1)) = X2,
inference(step,[status(thm)],[t315,t240]) ).
cnf(t318,plain,
double_divide(X1,double_divide(X2,X1)) = X2,
inference(orient,[status(thm)],[t791]) ).
cnf(t619,plain,
double_divide(X1,X2) = double_divide(multiply(multiply(inverse(X3),X2),X1),X3),
inference(cp,[status(thm)],[t605,t318]) ).
cnf(t645,plain,
double_divide(multiply(multiply(inverse(X1),X2),X3),X1) = double_divide(X3,X2),
inference(orient,[status(thm)],[t619]) ).
cnf(t257,plain,
multiply(X1,multiply(inverse(X1),X2)) = inverse(inverse(X2)),
inference(cp,[status(thm)],[t14,t251]) ).
cnf(t786,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(step,[status(thm)],[t257,t240]) ).
cnf(t259,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t786]) ).
cnf(t655,plain,
double_divide(X1,multiply(inverse(inverse(X2)),X3)) = double_divide(multiply(X3,X1),X2),
inference(cp,[status(thm)],[t645,t259]) ).
cnf(t803,plain,
double_divide(X1,multiply(X2,X3)) = double_divide(multiply(X3,X1),X2),
inference(step,[status(thm)],[t655,t240]) ).
cnf(t676,plain,
double_divide(multiply(X1,X2),X3) = double_divide(X2,multiply(X3,X1)),
inference(orient,[status(thm)],[t803]) ).
cnf(t705,plain,
multiply(X1,multiply(X2,X3)) = inverse(double_divide(X3,multiply(X1,X2))),
inference(cp,[status(thm)],[t14,t676]) ).
cnf(t808,plain,
multiply(X1,multiply(X2,X3)) = multiply(multiply(X1,X2),X3),
inference(step,[status(thm)],[t705,t14]) ).
cnf(t712,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t808]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)),
inference(rw,[status(thm)],[goal_0,t712]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP483-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/5.37 % Computer : n014.cluster.edu
% 0.08/5.37 % Model : x86_64 x86_64
% 0.08/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.37 % Memory : 8046.5625MB
% 0.08/5.37 % OS : Linux 6.8.0-71-generic
% 0.08/5.37 % CPULimit : 300
% 0.08/5.37 % WCLimit : 300
% 0.08/5.37 % DateTime : Wed Sep 23 14:52:24 UTC 2026
% 0.08/5.37 % CPUTime :
% 0.08/5.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.71/6.15 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.71/6.15 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------