%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP099-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n001.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:25:10 PM UTC 2026
% Result : Unsatisfiable 9.88s 6.89s
% Output : Proof 9.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 6
% Syntax : Number of formulae : 154 ( 150 unt; 0 def)
% Number of atoms : 166 ( 165 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 30 ( 18 ~; 12 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-4 aty)
% Number of variables : 250 ( 2 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f4,negated_conjecture,
( multiply(a4,b4) != multiply(b4,a4)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(identity,a2) != a2
| multiply(inverse(a1),a1) != identity ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms) ).
fof(f4_nnf,plain,
( multiply(a4,b4) != multiply(b4,a4)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(identity,a2) != a2
| multiply(inverse(a1),a1) != identity ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
( multiply(a4,b4) != multiply(b4,a4)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(identity,a2) != a2
| multiply(inverse(a1),a1) != identity ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( multiply(a4,b4) != multiply(b4,a4)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(identity,a2) != a2
| multiply(inverse(a1),a1) != identity ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t5,plain,
ifeq(multiply(inverse(a1),a1),identity,ifeq(multiply(identity,a2),a2,ifeq(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3)),ifeq(multiply(a4,b4),multiply(b4,a4),false,true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t17,plain,
ifeq(multiply(inverse(a1),a1),identity,ifeq(multiply(identity,a2),a2,ifeq(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3)),ifeq(multiply(a4,b4),multiply(b4,a4),false,true),true),true),true) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(f1,axiom,
multiply(X,Y) = double_divide(double_divide(Y,X),identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiply) ).
fof(f1_nnf,plain,
! [X,Y] : multiply(X,Y) = double_divide(double_divide(Y,X),identity),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y] : multiply(X,Y) = double_divide(double_divide(Y,X),identity),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
multiply(X0,X1) = double_divide(double_divide(X1,X0),identity),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t3,plain,
double_divide(double_divide(X1,X2),identity) = multiply(X2,X1),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(f2,axiom,
inverse(X) = double_divide(X,identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inverse) ).
fof(f2_nnf,plain,
! [X] : inverse(X) = double_divide(X,identity),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X] : inverse(X) = double_divide(X,identity),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
inverse(X0) = double_divide(X0,identity),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t0,plain,
double_divide(X1,identity) = inverse(X1),
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t10,plain,
double_divide(X1,identity) = inverse(X1),
inference(orient,[status(thm)],[t0]) ).
cnf(t20276,plain,
inverse(double_divide(X1,X2)) = multiply(X2,X1),
inference(step,[status(thm)],[t3,t10]) ).
cnf(t13,plain,
inverse(double_divide(X1,X2)) = multiply(X2,X1),
inference(orient,[status(thm)],[t20276]) ).
cnf(f3,axiom,
identity = double_divide(X,inverse(X)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity) ).
fof(f3_nnf,plain,
! [X] : identity = double_divide(X,inverse(X)),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X] : identity = double_divide(X,inverse(X)),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
identity = double_divide(X0,inverse(X0)),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t1,plain,
double_divide(X1,inverse(X1)) = identity,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t12,plain,
double_divide(X1,inverse(X1)) = identity,
inference(orient,[status(thm)],[t1]) ).
cnf(t15,plain,
multiply(inverse(X1),X1) = inverse(identity),
inference(cp,[status(thm)],[t13,t12]) ).
cnf(t22,plain,
multiply(inverse(X1),X1) = inverse(identity),
inference(orient,[status(thm)],[t15]) ).
cnf(t20277,plain,
ifeq(inverse(identity),identity,ifeq(multiply(identity,a2),a2,ifeq(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3)),ifeq(multiply(a4,b4),multiply(b4,a4),false,true),true),true),true) = true,
inference(step,[status(thm)],[t17,t22]) ).
cnf(t25,plain,
ifeq(inverse(identity),identity,ifeq(multiply(identity,a2),a2,ifeq(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3)),ifeq(multiply(a4,b4),multiply(b4,a4),false,true),true),true),true) = true,
inference(rw,[status(thm)],[t20277]) ).
cnf(f0,axiom,
double_divide(double_divide(X,double_divide(double_divide(Y,double_divide(X,Z)),double_divide(identity,Z))),double_divide(identity,identity)) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f0_nnf,plain,
! [X,Y,Z] : double_divide(double_divide(X,double_divide(double_divide(Y,double_divide(X,Z)),double_divide(identity,Z))),double_divide(identity,identity)) = Y,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y,Z] : double_divide(double_divide(X,double_divide(double_divide(Y,double_divide(X,Z)),double_divide(identity,Z))),double_divide(identity,identity)) = Y,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2))),double_divide(identity,identity)) = X1,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t4,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(equality_encoding,[status(esa)],[c0]) ).
cnf(t6,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)],[t4]) ).
cnf(t20275,plain,
double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3))),inverse(identity)) = X2,
inference(step,[status(thm)],[t6,t10]) ).
cnf(t11,plain,
double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3))),inverse(identity)) = X2,
inference(rw,[status(thm)],[t20275]) ).
cnf(t74,plain,
double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3))),inverse(identity)) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(t75,plain,
X1 = double_divide(double_divide(X2,double_divide(double_divide(X1,inverse(X2)),double_divide(identity,identity))),inverse(identity)),
inference(cp,[status(thm)],[t74,t10]) ).
cnf(t20281,plain,
X1 = double_divide(double_divide(X2,double_divide(double_divide(X1,inverse(X2)),inverse(identity))),inverse(identity)),
inference(step,[status(thm)],[t75,t10]) ).
cnf(t121,plain,
double_divide(double_divide(X1,double_divide(double_divide(X2,inverse(X1)),inverse(identity))),inverse(identity)) = X2,
inference(orient,[status(thm)],[t20281]) ).
cnf(t123,plain,
X1 = double_divide(double_divide(X1,double_divide(identity,inverse(identity))),inverse(identity)),
inference(cp,[status(thm)],[t121,t12]) ).
cnf(t20282,plain,
X1 = double_divide(double_divide(X1,identity),inverse(identity)),
inference(step,[status(thm)],[t123,t12]) ).
cnf(t20283,plain,
X1 = double_divide(inverse(X1),inverse(identity)),
inference(step,[status(thm)],[t20282,t10]) ).
cnf(t139,plain,
double_divide(inverse(X1),inverse(identity)) = X1,
inference(orient,[status(thm)],[t20283]) ).
cnf(t148,plain,
inverse(X1) = double_divide(double_divide(identity,double_divide(X1,inverse(identity))),inverse(identity)),
inference(cp,[status(thm)],[t121,t139]) ).
cnf(t192,plain,
double_divide(double_divide(identity,double_divide(X1,inverse(identity))),inverse(identity)) = inverse(X1),
inference(orient,[status(thm)],[t148]) ).
cnf(t194,plain,
inverse(identity) = double_divide(double_divide(identity,identity),inverse(identity)),
inference(cp,[status(thm)],[t192,t12]) ).
cnf(t20288,plain,
inverse(identity) = double_divide(inverse(identity),inverse(identity)),
inference(step,[status(thm)],[t194,t10]) ).
cnf(t20289,plain,
inverse(identity) = identity,
inference(step,[status(thm)],[t20288,t139]) ).
cnf(t212,plain,
inverse(identity) = identity,
inference(orient,[status(thm)],[t20289]) ).
cnf(t20361,plain,
ifeq(identity,identity,ifeq(multiply(identity,a2),a2,ifeq(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3)),ifeq(multiply(a4,b4),multiply(b4,a4),false,true),true),true),true) = true,
inference(step,[status(thm)],[t25,t212]) ).
cnf(t2,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t9,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t2]) ).
cnf(t20362,plain,
ifeq(multiply(identity,a2),a2,ifeq(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3)),ifeq(multiply(a4,b4),multiply(b4,a4),false,true),true),true) = true,
inference(step,[status(thm)],[t20361,t9]) ).
cnf(t20306,plain,
double_divide(inverse(X1),identity) = X1,
inference(step,[status(thm)],[t139,t212]) ).
cnf(t20307,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t20306,t10]) ).
cnf(t14,plain,
multiply(identity,X1) = inverse(inverse(X1)),
inference(cp,[status(thm)],[t13,t10]) ).
cnf(t18,plain,
inverse(inverse(X1)) = multiply(identity,X1),
inference(orient,[status(thm)],[t14]) ).
cnf(t20308,plain,
multiply(identity,X1) = X1,
inference(step,[status(thm)],[t20307,t18]) ).
cnf(t238,plain,
multiply(identity,X1) = X1,
inference(rw,[status(thm)],[t20308]) ).
cnf(t250,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t238]) ).
cnf(t20363,plain,
ifeq(a2,a2,ifeq(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3)),ifeq(multiply(a4,b4),multiply(b4,a4),false,true),true),true) = true,
inference(step,[status(thm)],[t20362,t250]) ).
cnf(t20364,plain,
ifeq(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3)),ifeq(multiply(a4,b4),multiply(b4,a4),false,true),true) = true,
inference(step,[status(thm)],[t20363,t9]) ).
cnf(t320,plain,
ifeq(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3)),ifeq(multiply(a4,b4),multiply(b4,a4),false,true),true) = true,
inference(orient,[status(thm)],[t20364]) ).
cnf(t710,plain,
ifeq(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3)),ifeq(multiply(a4,b4),multiply(b4,a4),false,true),true) = true,
inference(rw,[status(thm)],[t320]) ).
cnf(t20327,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)],[t74,t212]) ).
cnf(t20328,plain,
inverse(double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3)))) = X2,
inference(step,[status(thm)],[t20327,t10]) ).
cnf(t20329,plain,
multiply(double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3)),X1) = X2,
inference(step,[status(thm)],[t20328,t13]) ).
cnf(t245,plain,
multiply(double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3)),X1) = X2,
inference(rw,[status(thm)],[t20329]) ).
cnf(t147,plain,
X1 = double_divide(double_divide(inverse(X2),double_divide(double_divide(X1,X2),double_divide(identity,inverse(identity)))),inverse(identity)),
inference(cp,[status(thm)],[t74,t139]) ).
cnf(t20285,plain,
X1 = double_divide(double_divide(inverse(X2),double_divide(double_divide(X1,X2),identity)),inverse(identity)),
inference(step,[status(thm)],[t147,t12]) ).
cnf(t20286,plain,
X1 = double_divide(double_divide(inverse(X2),inverse(double_divide(X1,X2))),inverse(identity)),
inference(step,[status(thm)],[t20285,t10]) ).
cnf(t20287,plain,
X1 = double_divide(double_divide(inverse(X2),multiply(X2,X1)),inverse(identity)),
inference(step,[status(thm)],[t20286,t13]) ).
cnf(t174,plain,
double_divide(double_divide(inverse(X1),multiply(X1,X2)),inverse(identity)) = X2,
inference(orient,[status(thm)],[t20287]) ).
cnf(t20309,plain,
double_divide(double_divide(inverse(X1),multiply(X1,X2)),identity) = X2,
inference(step,[status(thm)],[t174,t212]) ).
cnf(t20310,plain,
inverse(double_divide(inverse(X1),multiply(X1,X2))) = X2,
inference(step,[status(thm)],[t20309,t10]) ).
cnf(t20311,plain,
multiply(multiply(X1,X2),inverse(X1)) = X2,
inference(step,[status(thm)],[t20310,t13]) ).
cnf(t239,plain,
multiply(multiply(X1,X2),inverse(X1)) = X2,
inference(rw,[status(thm)],[t20311]) ).
cnf(t278,plain,
multiply(multiply(X1,X2),inverse(X1)) = X2,
inference(orient,[status(thm)],[t239]) ).
cnf(t282,plain,
inverse(X1) = multiply(X2,inverse(multiply(X1,X2))),
inference(cp,[status(thm)],[t278,t278]) ).
cnf(t141,plain,
double_divide(X1,X2) = double_divide(multiply(X2,X1),inverse(identity)),
inference(cp,[status(thm)],[t139,t13]) ).
cnf(t164,plain,
double_divide(multiply(X1,X2),inverse(identity)) = double_divide(X2,X1),
inference(orient,[status(thm)],[t141]) ).
cnf(t20303,plain,
double_divide(multiply(X1,X2),identity) = double_divide(X2,X1),
inference(step,[status(thm)],[t164,t212]) ).
cnf(t20304,plain,
inverse(multiply(X1,X2)) = double_divide(X2,X1),
inference(step,[status(thm)],[t20303,t10]) ).
cnf(t236,plain,
inverse(multiply(X1,X2)) = double_divide(X2,X1),
inference(rw,[status(thm)],[t20304]) ).
cnf(t273,plain,
inverse(multiply(X1,X2)) = double_divide(X2,X1),
inference(orient,[status(thm)],[t236]) ).
cnf(t20359,plain,
inverse(X1) = multiply(X2,double_divide(X2,X1)),
inference(step,[status(thm)],[t282,t273]) ).
cnf(t286,plain,
multiply(X1,double_divide(X1,X2)) = inverse(X2),
inference(orient,[status(thm)],[t20359]) ).
cnf(t287,plain,
double_divide(X1,X2) = multiply(inverse(X2),inverse(X1)),
inference(cp,[status(thm)],[t278,t286]) ).
cnf(t300,plain,
multiply(inverse(X1),inverse(X2)) = double_divide(X2,X1),
inference(orient,[status(thm)],[t287]) ).
cnf(t302,plain,
double_divide(X1,double_divide(X2,X3)) = multiply(multiply(X3,X2),inverse(X1)),
inference(cp,[status(thm)],[t300,t13]) ).
cnf(t369,plain,
multiply(multiply(X1,X2),inverse(X3)) = double_divide(X3,double_divide(X2,X1)),
inference(orient,[status(thm)],[t302]) ).
cnf(t371,plain,
double_divide(double_divide(X1,X2),double_divide(X3,Y3)) = multiply(multiply(Y3,X3),multiply(X2,X1)),
inference(cp,[status(thm)],[t369,t13]) ).
cnf(t542,plain,
double_divide(double_divide(X1,X2),double_divide(X3,Y3)) = multiply(multiply(Y3,X3),multiply(X2,X1)),
inference(orient,[status(thm)],[t371]) ).
cnf(t20368,plain,
multiply(multiply(multiply(X3,identity),multiply(double_divide(X1,X3),X2)),X1) = X2,
inference(step,[status(thm)],[t245,t542]) ).
cnf(t20317,plain,
double_divide(double_divide(identity,double_divide(X1,identity)),inverse(identity)) = inverse(X1),
inference(step,[status(thm)],[t192,t212]) ).
cnf(t20318,plain,
double_divide(double_divide(identity,inverse(X1)),inverse(identity)) = inverse(X1),
inference(step,[status(thm)],[t20317,t10]) ).
cnf(t20319,plain,
double_divide(double_divide(identity,inverse(X1)),identity) = inverse(X1),
inference(step,[status(thm)],[t20318,t212]) ).
cnf(t20320,plain,
inverse(double_divide(identity,inverse(X1))) = inverse(X1),
inference(step,[status(thm)],[t20319,t10]) ).
cnf(t20321,plain,
multiply(inverse(X1),identity) = inverse(X1),
inference(step,[status(thm)],[t20320,t13]) ).
cnf(t242,plain,
multiply(inverse(X1),identity) = inverse(X1),
inference(rw,[status(thm)],[t20321]) ).
cnf(t265,plain,
multiply(inverse(X1),identity) = inverse(X1),
inference(orient,[status(thm)],[t242]) ).
cnf(t20345,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t18,t250]) ).
cnf(t251,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t20345]) ).
cnf(t267,plain,
inverse(inverse(X1)) = multiply(X1,identity),
inference(cp,[status(thm)],[t265,t251]) ).
cnf(t20358,plain,
X1 = multiply(X1,identity),
inference(step,[status(thm)],[t267,t251]) ).
cnf(t270,plain,
multiply(X1,identity) = X1,
inference(orient,[status(thm)],[t20358]) ).
cnf(t20369,plain,
multiply(multiply(X3,multiply(double_divide(X1,X3),X2)),X1) = X2,
inference(step,[status(thm)],[t20368,t270]) ).
cnf(t549,plain,
multiply(multiply(X1,multiply(double_divide(X2,X1),X3)),X2) = X3,
inference(orient,[status(thm)],[t20369]) ).
cnf(t715,plain,
multiply(multiply(X1,multiply(double_divide(X2,X1),X3)),X2) = X3,
inference(rw,[status(thm)],[t549]) ).
cnf(t303,plain,
double_divide(X1,inverse(X2)) = multiply(X2,inverse(X1)),
inference(cp,[status(thm)],[t300,t251]) ).
cnf(t310,plain,
double_divide(X1,inverse(X2)) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t303]) ).
cnf(t288,plain,
double_divide(double_divide(X1,X2),X1) = inverse(inverse(X2)),
inference(cp,[status(thm)],[t273,t286]) ).
cnf(t20360,plain,
double_divide(double_divide(X1,X2),X1) = X2,
inference(step,[status(thm)],[t288,t251]) ).
cnf(t291,plain,
double_divide(double_divide(X1,X2),X1) = X2,
inference(orient,[status(thm)],[t20360]) ).
cnf(t311,plain,
multiply(X1,inverse(double_divide(inverse(X1),X2))) = X2,
inference(cp,[status(thm)],[t310,t291]) ).
cnf(t20366,plain,
multiply(X1,multiply(X2,inverse(X1))) = X2,
inference(step,[status(thm)],[t311,t13]) ).
cnf(t342,plain,
multiply(X1,multiply(X2,inverse(X1))) = X2,
inference(orient,[status(thm)],[t20366]) ).
cnf(t552,plain,
inverse(X1) = multiply(double_divide(X2,X1),X2),
inference(cp,[status(thm)],[t549,t342]) ).
cnf(t593,plain,
multiply(double_divide(X1,X2),X1) = inverse(X2),
inference(orient,[status(thm)],[t552]) ).
cnf(t292,plain,
X1 = double_divide(X2,double_divide(X1,X2)),
inference(cp,[status(thm)],[t291,t291]) ).
cnf(t294,plain,
double_divide(X1,double_divide(X2,X1)) = X2,
inference(orient,[status(thm)],[t292]) ).
cnf(t597,plain,
inverse(double_divide(X1,X2)) = multiply(X1,X2),
inference(cp,[status(thm)],[t593,t294]) ).
cnf(t20372,plain,
multiply(X2,X1) = multiply(X1,X2),
inference(step,[status(thm)],[t597,t13]) ).
cnf(t683,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(orient,[status(thm)],[t20372]) ).
cnf(t20374,plain,
multiply(X2,multiply(X1,multiply(double_divide(X2,X1),X3))) = X3,
inference(step,[status(thm)],[t715,t683]) ).
cnf(t995,plain,
multiply(X1,multiply(X2,multiply(double_divide(X1,X2),X3))) = X3,
inference(orient,[status(thm)],[t20374]) ).
cnf(t344,plain,
X1 = multiply(double_divide(X2,X3),multiply(X1,multiply(X3,X2))),
inference(cp,[status(thm)],[t342,t13]) ).
cnf(t444,plain,
multiply(double_divide(X1,X2),multiply(X3,multiply(X2,X1))) = X3,
inference(orient,[status(thm)],[t344]) ).
cnf(t697,plain,
X1 = multiply(double_divide(X2,X3),multiply(multiply(X3,X2),X1)),
inference(cp,[status(thm)],[t444,t683]) ).
cnf(t804,plain,
multiply(double_divide(X1,X2),multiply(multiply(X2,X1),X3)) = X3,
inference(orient,[status(thm)],[t697]) ).
cnf(t1004,plain,
multiply(multiply(X1,X2),X3) = multiply(X2,multiply(X1,X3)),
inference(cp,[status(thm)],[t995,t804]) ).
cnf(t1047,plain,
multiply(multiply(X1,X2),X3) = multiply(X2,multiply(X1,X3)),
inference(orient,[status(thm)],[t1004]) ).
cnf(t20708,plain,
ifeq(multiply(b3,multiply(a3,c3)),multiply(a3,multiply(b3,c3)),ifeq(multiply(a4,b4),multiply(b4,a4),false,true),true) = true,
inference(step,[status(thm)],[t710,t1047]) ).
cnf(t1007,plain,
double_divide(double_divide(X1,X2),X3) = multiply(X1,multiply(X2,inverse(X3))),
inference(cp,[status(thm)],[t995,t286]) ).
cnf(t1124,plain,
multiply(X1,multiply(X2,inverse(X3))) = double_divide(double_divide(X1,X2),X3),
inference(orient,[status(thm)],[t1007]) ).
cnf(t1133,plain,
double_divide(double_divide(X1,X2),X3) = multiply(X1,multiply(inverse(X3),X2)),
inference(cp,[status(thm)],[t1124,t683]) ).
cnf(t1171,plain,
multiply(X1,multiply(inverse(X2),X3)) = double_divide(double_divide(X1,X3),X2),
inference(orient,[status(thm)],[t1133]) ).
cnf(t1191,plain,
double_divide(double_divide(X1,X2),inverse(X3)) = multiply(X1,multiply(X3,X2)),
inference(cp,[status(thm)],[t1171,t251]) ).
cnf(t20548,plain,
multiply(X3,inverse(double_divide(X1,X2))) = multiply(X1,multiply(X3,X2)),
inference(step,[status(thm)],[t1191,t310]) ).
cnf(t20549,plain,
multiply(X3,multiply(X2,X1)) = multiply(X1,multiply(X3,X2)),
inference(step,[status(thm)],[t20548,t13]) ).
cnf(t7828,plain,
multiply(X1,multiply(X2,X3)) = multiply(X3,multiply(X1,X2)),
inference(orient,[status(thm)],[t20549]) ).
cnf(t20709,plain,
ifeq(multiply(c3,multiply(b3,a3)),multiply(a3,multiply(b3,c3)),ifeq(multiply(a4,b4),multiply(b4,a4),false,true),true) = true,
inference(step,[status(thm)],[t20708,t7828]) ).
cnf(t20710,plain,
ifeq(multiply(c3,multiply(b3,a3)),multiply(b3,multiply(c3,a3)),ifeq(multiply(a4,b4),multiply(b4,a4),false,true),true) = true,
inference(step,[status(thm)],[t20709,t7828]) ).
cnf(t20711,plain,
ifeq(multiply(c3,multiply(b3,a3)),multiply(c3,multiply(a3,b3)),ifeq(multiply(a4,b4),multiply(b4,a4),false,true),true) = true,
inference(step,[status(thm)],[t20710,t7828]) ).
cnf(t20712,plain,
ifeq(multiply(c3,multiply(b3,a3)),multiply(c3,multiply(b3,a3)),ifeq(multiply(a4,b4),multiply(b4,a4),false,true),true) = true,
inference(step,[status(thm)],[t20711,t683]) ).
cnf(t20713,plain,
ifeq(multiply(a4,b4),multiply(b4,a4),false,true) = true,
inference(step,[status(thm)],[t20712,t9]) ).
cnf(t20714,plain,
ifeq(multiply(b4,a4),multiply(b4,a4),false,true) = true,
inference(step,[status(thm)],[t20713,t683]) ).
cnf(t20715,plain,
false = true,
inference(step,[status(thm)],[t20714,t9]) ).
cnf(t20274,plain,
false = true,
inference(orient,[status(thm)],[t20715]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t20274]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP099-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/5.37 % Computer : n001.cluster.edu
% 0.12/5.37 % Model : x86_64 x86_64
% 0.12/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.37 % Memory : 8046.5625MB
% 0.12/5.37 % OS : Linux 6.8.0-71-generic
% 0.12/5.37 % CPULimit : 300
% 0.12/5.37 % WCLimit : 300
% 0.12/5.37 % DateTime : Wed Sep 23 13:36:55 UTC 2026
% 0.12/5.38 % CPUTime :
% 0.12/5.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 9.88/6.89 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.88/6.89 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------