%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP080-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n020.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:07 PM UTC 2026
% Result : Unsatisfiable 6.85s 1.32s
% Output : Proof 6.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 19
% Syntax : Number of formulae : 194 ( 190 unt; 0 def)
% Number of atoms : 202 ( 201 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 23 ( 15 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 21 con; 0-4 aty)
% Number of variables : 77 ( 2 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f4,negated_conjecture,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(identity,a2) != a2
| multiply(inverse(a1),a1) != identity ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms) ).
fof(f4_nnf,plain,
( 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(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(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(u0,axiom,
ifeq(multiply(inverse(a1),a1),identity,ifeq(multiply(identity,a2),a2,ifeq(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3)),false,true),true),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(f1,axiom,
multiply(X,Y) = double_divide(double_divide(Y,X),identity),
file('/export/starexec/sandbox/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(d0,axiom,
multiply(X0,X1) = double_divide(double_divide(X1,X0),identity),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(f2,axiom,
inverse(X) = double_divide(X,identity),
file('/export/starexec/sandbox/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(d1,axiom,
inverse(X0) = double_divide(X0,identity),
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t3,plain,
ifeq(double_divide(double_divide(a1,double_divide(a1,identity)),identity),identity,ifeq(double_divide(double_divide(a2,identity),identity),a2,ifeq(double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true),true) = true,
inference(definition_unfolding,[status(thm)],[u0,d0,d1]) ).
cnf(t5,axiom,
sF1 = double_divide(a1,double_divide(a1,identity)),
introduced(definition) ).
cnf(f3,axiom,
identity = double_divide(X,inverse(X)),
file('/export/starexec/sandbox/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(u1,axiom,
identity = double_divide(X0,inverse(X0)),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t0,plain,
double_divide(X1,double_divide(X1,identity)) = identity,
inference(definition_unfolding,[status(thm)],[u1,d1]) ).
cnf(t24,plain,
double_divide(X1,double_divide(X1,identity)) = identity,
inference(orient,[status(thm)],[t0]) ).
cnf(t3418,plain,
sF1 = identity,
inference(step,[status(thm)],[t5,t24]) ).
cnf(t30,plain,
identity = sF1,
inference(orient,[status(thm)],[t3418]) ).
cnf(t3440,plain,
ifeq(double_divide(double_divide(a1,double_divide(a1,sF1)),identity),identity,ifeq(double_divide(double_divide(a2,identity),identity),a2,ifeq(double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true),true) = true,
inference(step,[status(thm)],[t3,t30]) ).
cnf(t33,plain,
double_divide(X1,double_divide(X1,sF1)) = identity,
inference(rw,[status(thm)],[t24]) ).
cnf(t3435,plain,
double_divide(X1,double_divide(X1,sF1)) = sF1,
inference(step,[status(thm)],[t33,t30]) ).
cnf(t61,plain,
double_divide(X1,double_divide(X1,sF1)) = sF1,
inference(orient,[status(thm)],[t3435]) ).
cnf(t3441,plain,
ifeq(double_divide(sF1,identity),identity,ifeq(double_divide(double_divide(a2,identity),identity),a2,ifeq(double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true),true) = true,
inference(step,[status(thm)],[t3440,t61]) ).
cnf(t3442,plain,
ifeq(double_divide(sF1,sF1),identity,ifeq(double_divide(double_divide(a2,identity),identity),a2,ifeq(double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true),true) = true,
inference(step,[status(thm)],[t3441,t30]) ).
cnf(f0,axiom,
double_divide(double_divide(identity,double_divide(X,double_divide(Y,identity))),double_divide(double_divide(Y,double_divide(Z,X)),identity)) = Z,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
fof(f0_nnf,plain,
! [X,Y,Z] : double_divide(double_divide(identity,double_divide(X,double_divide(Y,identity))),double_divide(double_divide(Y,double_divide(Z,X)),identity)) = Z,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y,Z] : double_divide(double_divide(identity,double_divide(X,double_divide(Y,identity))),double_divide(double_divide(Y,double_divide(Z,X)),identity)) = Z,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
double_divide(double_divide(identity,double_divide(X0,double_divide(X1,identity))),double_divide(double_divide(X1,double_divide(X2,X0)),identity)) = X2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t2,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(equality_encoding,[status(esa)],[c0]) ).
cnf(t3425,plain,
double_divide(double_divide(sF1,double_divide(X1,double_divide(X2,identity))),double_divide(double_divide(X2,double_divide(X3,X1)),identity)) = X3,
inference(step,[status(thm)],[t2,t30]) ).
cnf(t3426,plain,
double_divide(double_divide(sF1,double_divide(X1,double_divide(X2,sF1))),double_divide(double_divide(X2,double_divide(X3,X1)),identity)) = X3,
inference(step,[status(thm)],[t3425,t30]) ).
cnf(t3427,plain,
double_divide(double_divide(sF1,double_divide(X1,double_divide(X2,sF1))),double_divide(double_divide(X2,double_divide(X3,X1)),sF1)) = X3,
inference(step,[status(thm)],[t3426,t30]) ).
cnf(t39,plain,
double_divide(double_divide(sF1,double_divide(X1,double_divide(X2,sF1))),double_divide(double_divide(X2,double_divide(X3,X1)),sF1)) = X3,
inference(orient,[status(thm)],[t3427]) ).
cnf(t62,plain,
sF1 = double_divide(sF1,sF1),
inference(cp,[status(thm)],[t61,t39]) ).
cnf(t69,plain,
double_divide(sF1,sF1) = sF1,
inference(orient,[status(thm)],[t62]) ).
cnf(t3443,plain,
ifeq(sF1,identity,ifeq(double_divide(double_divide(a2,identity),identity),a2,ifeq(double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true),true) = true,
inference(step,[status(thm)],[t3442,t69]) ).
cnf(t3444,plain,
ifeq(sF1,sF1,ifeq(double_divide(double_divide(a2,identity),identity),a2,ifeq(double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true),true) = true,
inference(step,[status(thm)],[t3443,t30]) ).
cnf(t1,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t29,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(t3445,plain,
ifeq(double_divide(double_divide(a2,identity),identity),a2,ifeq(double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true) = true,
inference(step,[status(thm)],[t3444,t29]) ).
cnf(t3446,plain,
ifeq(double_divide(double_divide(a2,sF1),identity),a2,ifeq(double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true) = true,
inference(step,[status(thm)],[t3445,t30]) ).
cnf(t7,axiom,
sF3 = double_divide(a2,identity),
introduced(definition) ).
cnf(t21,plain,
double_divide(a2,identity) = sF3,
inference(orient,[status(thm)],[t7]) ).
cnf(t3420,plain,
double_divide(a2,sF1) = sF3,
inference(step,[status(thm)],[t21,t30]) ).
cnf(t32,plain,
double_divide(a2,sF1) = sF3,
inference(rw,[status(thm)],[t3420]) ).
cnf(t49,plain,
double_divide(a2,sF1) = sF3,
inference(orient,[status(thm)],[t32]) ).
cnf(t3447,plain,
ifeq(double_divide(sF3,identity),a2,ifeq(double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true) = true,
inference(step,[status(thm)],[t3446,t49]) ).
cnf(t3448,plain,
ifeq(double_divide(sF3,sF1),a2,ifeq(double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true) = true,
inference(step,[status(thm)],[t3447,t30]) ).
cnf(t8,axiom,
sF4 = double_divide(double_divide(a2,identity),identity),
introduced(definition) ).
cnf(t3428,plain,
sF4 = double_divide(double_divide(a2,sF1),identity),
inference(step,[status(thm)],[t8,t30]) ).
cnf(t3429,plain,
sF4 = double_divide(sF3,identity),
inference(step,[status(thm)],[t3428,t49]) ).
cnf(t3430,plain,
sF4 = double_divide(sF3,sF1),
inference(step,[status(thm)],[t3429,t30]) ).
cnf(t52,plain,
double_divide(sF3,sF1) = sF4,
inference(orient,[status(thm)],[t3430]) ).
cnf(t3449,plain,
ifeq(sF4,a2,ifeq(double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true) = true,
inference(step,[status(thm)],[t3448,t52]) ).
cnf(t9,axiom,
sF5 = double_divide(b3,a3),
introduced(definition) ).
cnf(t22,plain,
double_divide(b3,a3) = sF5,
inference(orient,[status(thm)],[t9]) ).
cnf(t3450,plain,
ifeq(sF4,a2,ifeq(double_divide(double_divide(c3,double_divide(sF5,identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true) = true,
inference(step,[status(thm)],[t3449,t22]) ).
cnf(t3451,plain,
ifeq(sF4,a2,ifeq(double_divide(double_divide(c3,double_divide(sF5,sF1)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true) = true,
inference(step,[status(thm)],[t3450,t30]) ).
cnf(t10,axiom,
sF6 = double_divide(double_divide(b3,a3),identity),
introduced(definition) ).
cnf(t3431,plain,
sF6 = double_divide(sF5,identity),
inference(step,[status(thm)],[t10,t22]) ).
cnf(t3432,plain,
sF6 = double_divide(sF5,sF1),
inference(step,[status(thm)],[t3431,t30]) ).
cnf(t55,plain,
double_divide(sF5,sF1) = sF6,
inference(orient,[status(thm)],[t3432]) ).
cnf(t3452,plain,
ifeq(sF4,a2,ifeq(double_divide(double_divide(c3,sF6),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true) = true,
inference(step,[status(thm)],[t3451,t55]) ).
cnf(t3453,plain,
ifeq(sF4,a2,ifeq(double_divide(double_divide(c3,sF6),sF1),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true) = true,
inference(step,[status(thm)],[t3452,t30]) ).
cnf(t13,axiom,
sF9 = double_divide(c3,b3),
introduced(definition) ).
cnf(t23,plain,
double_divide(c3,b3) = sF9,
inference(orient,[status(thm)],[t13]) ).
cnf(t3454,plain,
ifeq(sF4,a2,ifeq(double_divide(double_divide(c3,sF6),sF1),double_divide(double_divide(double_divide(sF9,identity),a3),identity),false,true),true) = true,
inference(step,[status(thm)],[t3453,t23]) ).
cnf(t3455,plain,
ifeq(sF4,a2,ifeq(double_divide(double_divide(c3,sF6),sF1),double_divide(double_divide(double_divide(sF9,sF1),a3),identity),false,true),true) = true,
inference(step,[status(thm)],[t3454,t30]) ).
cnf(t14,axiom,
sF10 = double_divide(double_divide(c3,b3),identity),
introduced(definition) ).
cnf(t3433,plain,
sF10 = double_divide(sF9,identity),
inference(step,[status(thm)],[t14,t23]) ).
cnf(t3434,plain,
sF10 = double_divide(sF9,sF1),
inference(step,[status(thm)],[t3433,t30]) ).
cnf(t58,plain,
double_divide(sF9,sF1) = sF10,
inference(orient,[status(thm)],[t3434]) ).
cnf(t3456,plain,
ifeq(sF4,a2,ifeq(double_divide(double_divide(c3,sF6),sF1),double_divide(double_divide(sF10,a3),identity),false,true),true) = true,
inference(step,[status(thm)],[t3455,t58]) ).
cnf(t3457,plain,
ifeq(sF4,a2,ifeq(double_divide(double_divide(c3,sF6),sF1),double_divide(double_divide(sF10,a3),sF1),false,true),true) = true,
inference(step,[status(thm)],[t3456,t30]) ).
cnf(t79,plain,
ifeq(sF4,a2,ifeq(double_divide(double_divide(c3,sF6),sF1),double_divide(double_divide(sF10,a3),sF1),false,true),true) = true,
inference(orient,[status(thm)],[t3457]) ).
cnf(t11,axiom,
sF7 = double_divide(c3,double_divide(double_divide(b3,a3),identity)),
introduced(definition) ).
cnf(t3458,plain,
sF7 = double_divide(c3,double_divide(sF5,identity)),
inference(step,[status(thm)],[t11,t22]) ).
cnf(t3459,plain,
sF7 = double_divide(c3,double_divide(sF5,sF1)),
inference(step,[status(thm)],[t3458,t30]) ).
cnf(t3460,plain,
sF7 = double_divide(c3,sF6),
inference(step,[status(thm)],[t3459,t55]) ).
cnf(t80,plain,
double_divide(c3,sF6) = sF7,
inference(orient,[status(thm)],[t3460]) ).
cnf(t3461,plain,
ifeq(sF4,a2,ifeq(double_divide(sF7,sF1),double_divide(double_divide(sF10,a3),sF1),false,true),true) = true,
inference(step,[status(thm)],[t79,t80]) ).
cnf(t81,plain,
ifeq(sF4,a2,ifeq(double_divide(sF7,sF1),double_divide(double_divide(sF10,a3),sF1),false,true),true) = true,
inference(rw,[status(thm)],[t3461]) ).
cnf(t66,plain,
X1 = double_divide(double_divide(sF1,sF1),double_divide(double_divide(X2,double_divide(X1,X2)),sF1)),
inference(cp,[status(thm)],[t39,t61]) ).
cnf(t3475,plain,
X1 = double_divide(sF1,double_divide(double_divide(X2,double_divide(X1,X2)),sF1)),
inference(step,[status(thm)],[t66,t69]) ).
cnf(t97,plain,
double_divide(sF1,double_divide(double_divide(X1,double_divide(X2,X1)),sF1)) = X2,
inference(orient,[status(thm)],[t3475]) ).
cnf(t108,plain,
X1 = double_divide(sF1,double_divide(double_divide(double_divide(X1,sF1),sF1),sF1)),
inference(cp,[status(thm)],[t97,t61]) ).
cnf(t288,plain,
double_divide(sF1,double_divide(double_divide(double_divide(X1,sF1),sF1),sF1)) = X1,
inference(orient,[status(thm)],[t108]) ).
cnf(t290,plain,
double_divide(double_divide(X1,sF1),sF1) = double_divide(double_divide(sF1,double_divide(sF1,double_divide(sF1,sF1))),double_divide(X1,sF1)),
inference(cp,[status(thm)],[t39,t288]) ).
cnf(t3564,plain,
double_divide(double_divide(X1,sF1),sF1) = double_divide(double_divide(sF1,sF1),double_divide(X1,sF1)),
inference(step,[status(thm)],[t290,t61]) ).
cnf(t3565,plain,
double_divide(double_divide(X1,sF1),sF1) = double_divide(sF1,double_divide(X1,sF1)),
inference(step,[status(thm)],[t3564,t69]) ).
cnf(t293,plain,
double_divide(double_divide(X1,sF1),sF1) = double_divide(sF1,double_divide(X1,sF1)),
inference(orient,[status(thm)],[t3565]) ).
cnf(t301,plain,
double_divide(sF1,double_divide(double_divide(X1,sF1),sF1)) = double_divide(double_divide(sF1,double_divide(X1,sF1)),sF1),
inference(cp,[status(thm)],[t293,t293]) ).
cnf(t3588,plain,
double_divide(sF1,double_divide(sF1,double_divide(X1,sF1))) = double_divide(double_divide(sF1,double_divide(X1,sF1)),sF1),
inference(step,[status(thm)],[t301,t293]) ).
cnf(t427,plain,
double_divide(double_divide(sF1,double_divide(X1,sF1)),sF1) = double_divide(sF1,double_divide(sF1,double_divide(X1,sF1))),
inference(orient,[status(thm)],[t3588]) ).
cnf(t428,plain,
double_divide(sF1,double_divide(sF1,double_divide(double_divide(X1,double_divide(X2,X1)),sF1))) = double_divide(X2,sF1),
inference(cp,[status(thm)],[t427,t97]) ).
cnf(t3589,plain,
double_divide(sF1,X2) = double_divide(X2,sF1),
inference(step,[status(thm)],[t428,t97]) ).
cnf(t439,plain,
double_divide(sF1,X1) = double_divide(X1,sF1),
inference(orient,[status(thm)],[t3589]) ).
cnf(t3613,plain,
ifeq(sF4,a2,ifeq(double_divide(sF1,sF7),double_divide(double_divide(sF10,a3),sF1),false,true),true) = true,
inference(step,[status(thm)],[t81,t439]) ).
cnf(t3614,plain,
ifeq(sF4,a2,ifeq(double_divide(sF1,sF7),double_divide(sF1,double_divide(sF10,a3)),false,true),true) = true,
inference(step,[status(thm)],[t3613,t439]) ).
cnf(t15,axiom,
sF11 = double_divide(double_divide(double_divide(c3,b3),identity),a3),
introduced(definition) ).
cnf(t3462,plain,
sF11 = double_divide(double_divide(sF9,identity),a3),
inference(step,[status(thm)],[t15,t23]) ).
cnf(t3463,plain,
sF11 = double_divide(double_divide(sF9,sF1),a3),
inference(step,[status(thm)],[t3462,t30]) ).
cnf(t3464,plain,
sF11 = double_divide(sF10,a3),
inference(step,[status(thm)],[t3463,t58]) ).
cnf(t83,plain,
double_divide(sF10,a3) = sF11,
inference(orient,[status(thm)],[t3464]) ).
cnf(t3615,plain,
ifeq(sF4,a2,ifeq(double_divide(sF1,sF7),double_divide(sF1,sF11),false,true),true) = true,
inference(step,[status(thm)],[t3614,t83]) ).
cnf(t486,plain,
ifeq(sF4,a2,ifeq(double_divide(sF1,sF7),double_divide(sF1,sF11),false,true),true) = true,
inference(orient,[status(thm)],[t3615]) ).
cnf(t12,axiom,
sF8 = double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),
introduced(definition) ).
cnf(t3465,plain,
sF8 = double_divide(double_divide(c3,double_divide(sF5,identity)),identity),
inference(step,[status(thm)],[t12,t22]) ).
cnf(t3466,plain,
sF8 = double_divide(double_divide(c3,double_divide(sF5,sF1)),identity),
inference(step,[status(thm)],[t3465,t30]) ).
cnf(t3467,plain,
sF8 = double_divide(double_divide(c3,sF6),identity),
inference(step,[status(thm)],[t3466,t55]) ).
cnf(t3468,plain,
sF8 = double_divide(sF7,identity),
inference(step,[status(thm)],[t3467,t80]) ).
cnf(t3469,plain,
sF8 = double_divide(sF7,sF1),
inference(step,[status(thm)],[t3468,t30]) ).
cnf(t85,plain,
double_divide(sF7,sF1) = sF8,
inference(orient,[status(thm)],[t3469]) ).
cnf(t3593,plain,
double_divide(sF1,sF7) = sF8,
inference(step,[status(thm)],[t85,t439]) ).
cnf(t446,plain,
double_divide(sF1,sF7) = sF8,
inference(rw,[status(thm)],[t3593]) ).
cnf(t489,plain,
double_divide(sF1,sF7) = sF8,
inference(orient,[status(thm)],[t446]) ).
cnf(t3616,plain,
ifeq(sF4,a2,ifeq(sF8,double_divide(sF1,sF11),false,true),true) = true,
inference(step,[status(thm)],[t486,t489]) ).
cnf(t490,plain,
ifeq(sF4,a2,ifeq(sF8,double_divide(sF1,sF11),false,true),true) = true,
inference(rw,[status(thm)],[t3616]) ).
cnf(t16,axiom,
sF12 = double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),
introduced(definition) ).
cnf(t3470,plain,
sF12 = double_divide(double_divide(double_divide(sF9,identity),a3),identity),
inference(step,[status(thm)],[t16,t23]) ).
cnf(t3471,plain,
sF12 = double_divide(double_divide(double_divide(sF9,sF1),a3),identity),
inference(step,[status(thm)],[t3470,t30]) ).
cnf(t3472,plain,
sF12 = double_divide(double_divide(sF10,a3),identity),
inference(step,[status(thm)],[t3471,t58]) ).
cnf(t3473,plain,
sF12 = double_divide(sF11,identity),
inference(step,[status(thm)],[t3472,t83]) ).
cnf(t3474,plain,
sF12 = double_divide(sF11,sF1),
inference(step,[status(thm)],[t3473,t30]) ).
cnf(t91,plain,
double_divide(sF11,sF1) = sF12,
inference(orient,[status(thm)],[t3474]) ).
cnf(t3594,plain,
double_divide(sF1,sF11) = sF12,
inference(step,[status(thm)],[t91,t439]) ).
cnf(t447,plain,
double_divide(sF1,sF11) = sF12,
inference(rw,[status(thm)],[t3594]) ).
cnf(t492,plain,
double_divide(sF1,sF11) = sF12,
inference(orient,[status(thm)],[t447]) ).
cnf(t3653,plain,
ifeq(sF4,a2,ifeq(sF8,sF12,false,true),true) = true,
inference(step,[status(thm)],[t490,t492]) ).
cnf(t17,axiom,
sF13 = ifeq(double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),
introduced(definition) ).
cnf(t3480,plain,
sF13 = ifeq(double_divide(double_divide(c3,double_divide(sF5,identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),
inference(step,[status(thm)],[t17,t22]) ).
cnf(t3481,plain,
sF13 = ifeq(double_divide(double_divide(c3,double_divide(sF5,sF1)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),
inference(step,[status(thm)],[t3480,t30]) ).
cnf(t3482,plain,
sF13 = ifeq(double_divide(double_divide(c3,sF6),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),
inference(step,[status(thm)],[t3481,t55]) ).
cnf(t3483,plain,
sF13 = ifeq(double_divide(sF7,identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),
inference(step,[status(thm)],[t3482,t80]) ).
cnf(t3484,plain,
sF13 = ifeq(double_divide(sF7,sF1),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),
inference(step,[status(thm)],[t3483,t30]) ).
cnf(t3485,plain,
sF13 = ifeq(sF8,double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),
inference(step,[status(thm)],[t3484,t85]) ).
cnf(t3486,plain,
sF13 = ifeq(sF8,double_divide(double_divide(double_divide(sF9,identity),a3),identity),false,true),
inference(step,[status(thm)],[t3485,t23]) ).
cnf(t3487,plain,
sF13 = ifeq(sF8,double_divide(double_divide(double_divide(sF9,sF1),a3),identity),false,true),
inference(step,[status(thm)],[t3486,t30]) ).
cnf(t3488,plain,
sF13 = ifeq(sF8,double_divide(double_divide(sF10,a3),identity),false,true),
inference(step,[status(thm)],[t3487,t58]) ).
cnf(t3489,plain,
sF13 = ifeq(sF8,double_divide(sF11,identity),false,true),
inference(step,[status(thm)],[t3488,t83]) ).
cnf(t3490,plain,
sF13 = ifeq(sF8,double_divide(sF11,sF1),false,true),
inference(step,[status(thm)],[t3489,t30]) ).
cnf(t3491,plain,
sF13 = ifeq(sF8,sF12,false,true),
inference(step,[status(thm)],[t3490,t91]) ).
cnf(t134,plain,
ifeq(sF8,sF12,false,true) = sF13,
inference(orient,[status(thm)],[t3491]) ).
cnf(t3654,plain,
ifeq(sF4,a2,sF13,true) = true,
inference(step,[status(thm)],[t3653,t134]) ).
cnf(t18,axiom,
sF14 = ifeq(double_divide(double_divide(a2,identity),identity),a2,ifeq(double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true),
introduced(definition) ).
cnf(t3499,plain,
sF14 = ifeq(double_divide(double_divide(a2,sF1),identity),a2,ifeq(double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true),
inference(step,[status(thm)],[t18,t30]) ).
cnf(t3500,plain,
sF14 = ifeq(double_divide(sF3,identity),a2,ifeq(double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true),
inference(step,[status(thm)],[t3499,t49]) ).
cnf(t3501,plain,
sF14 = ifeq(double_divide(sF3,sF1),a2,ifeq(double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true),
inference(step,[status(thm)],[t3500,t30]) ).
cnf(t3502,plain,
sF14 = ifeq(sF4,a2,ifeq(double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true),
inference(step,[status(thm)],[t3501,t52]) ).
cnf(t3503,plain,
sF14 = ifeq(sF4,a2,ifeq(double_divide(double_divide(c3,double_divide(sF5,identity)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true),
inference(step,[status(thm)],[t3502,t22]) ).
cnf(t3504,plain,
sF14 = ifeq(sF4,a2,ifeq(double_divide(double_divide(c3,double_divide(sF5,sF1)),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true),
inference(step,[status(thm)],[t3503,t30]) ).
cnf(t3505,plain,
sF14 = ifeq(sF4,a2,ifeq(double_divide(double_divide(c3,sF6),identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true),
inference(step,[status(thm)],[t3504,t55]) ).
cnf(t3506,plain,
sF14 = ifeq(sF4,a2,ifeq(double_divide(sF7,identity),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true),
inference(step,[status(thm)],[t3505,t80]) ).
cnf(t3507,plain,
sF14 = ifeq(sF4,a2,ifeq(double_divide(sF7,sF1),double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true),
inference(step,[status(thm)],[t3506,t30]) ).
cnf(t3508,plain,
sF14 = ifeq(sF4,a2,ifeq(sF8,double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),true),
inference(step,[status(thm)],[t3507,t85]) ).
cnf(t3509,plain,
sF14 = ifeq(sF4,a2,ifeq(sF8,double_divide(double_divide(double_divide(sF9,identity),a3),identity),false,true),true),
inference(step,[status(thm)],[t3508,t23]) ).
cnf(t3510,plain,
sF14 = ifeq(sF4,a2,ifeq(sF8,double_divide(double_divide(double_divide(sF9,sF1),a3),identity),false,true),true),
inference(step,[status(thm)],[t3509,t30]) ).
cnf(t3511,plain,
sF14 = ifeq(sF4,a2,ifeq(sF8,double_divide(double_divide(sF10,a3),identity),false,true),true),
inference(step,[status(thm)],[t3510,t58]) ).
cnf(t3512,plain,
sF14 = ifeq(sF4,a2,ifeq(sF8,double_divide(sF11,identity),false,true),true),
inference(step,[status(thm)],[t3511,t83]) ).
cnf(t3513,plain,
sF14 = ifeq(sF4,a2,ifeq(sF8,double_divide(sF11,sF1),false,true),true),
inference(step,[status(thm)],[t3512,t30]) ).
cnf(t3514,plain,
sF14 = ifeq(sF4,a2,ifeq(sF8,sF12,false,true),true),
inference(step,[status(thm)],[t3513,t91]) ).
cnf(t3515,plain,
sF14 = ifeq(sF4,a2,sF13,true),
inference(step,[status(thm)],[t3514,t134]) ).
cnf(t167,plain,
ifeq(sF4,a2,sF13,true) = sF14,
inference(orient,[status(thm)],[t3515]) ).
cnf(t3655,plain,
sF14 = true,
inference(step,[status(thm)],[t3654,t167]) ).
cnf(t893,plain,
true = sF14,
inference(orient,[status(thm)],[t3655]) ).
cnf(t3657,plain,
ifeq(sF4,a2,sF13,sF14) = sF14,
inference(step,[status(thm)],[t167,t893]) ).
cnf(t895,plain,
ifeq(sF4,a2,sF13,sF14) = sF14,
inference(rw,[status(thm)],[t3657]) ).
cnf(t897,plain,
ifeq(sF4,a2,sF13,sF14) = sF14,
inference(orient,[status(thm)],[t895]) ).
cnf(t1220,plain,
ifeq(sF4,sF4,sF13,sF14) = sF14,
inference(rw,[status(thm)],[t897]) ).
cnf(t3732,plain,
sF13 = sF14,
inference(step,[status(thm)],[t1220,t29]) ).
cnf(t1434,plain,
sF14 = sF13,
inference(orient,[status(thm)],[t3732]) ).
cnf(t3735,plain,
true = sF13,
inference(step,[status(thm)],[t893,t1434]) ).
cnf(t1437,plain,
true = sF13,
inference(orient,[status(thm)],[t3735]) ).
cnf(t3656,plain,
ifeq(sF8,sF12,false,sF14) = sF13,
inference(step,[status(thm)],[t134,t893]) ).
cnf(t894,plain,
ifeq(sF8,sF12,false,sF14) = sF13,
inference(rw,[status(thm)],[t3656]) ).
cnf(t896,plain,
ifeq(sF8,sF12,false,sF14) = sF13,
inference(orient,[status(thm)],[t894]) ).
cnf(t3737,plain,
ifeq(sF8,sF12,false,sF13) = sF13,
inference(step,[status(thm)],[t896,t1434]) ).
cnf(t1439,plain,
ifeq(sF8,sF12,false,sF13) = sF13,
inference(rw,[status(thm)],[t3737]) ).
cnf(t1716,plain,
ifeq(sF8,sF12,false,sF13) = sF13,
inference(orient,[status(thm)],[t1439]) ).
cnf(t2806,plain,
ifeq(sF8,sF8,false,sF13) = sF13,
inference(rw,[status(thm)],[t1716]) ).
cnf(t3823,plain,
false = sF13,
inference(step,[status(thm)],[t2806,t29]) ).
cnf(t3417,plain,
false = sF13,
inference(orient,[status(thm)],[t3823]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(g0_0,plain,
sF13 != false,
inference(rw,[status(thm)],[goal_0,t1437]) ).
cnf(g0_1,plain,
sF13 != sF13,
inference(rw,[status(thm)],[g0_0,t3417]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP080-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n020.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 13:29:47 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 6.85/1.32 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.85/1.32 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------