%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP101-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n011.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 7.03s 1.32s
% Output : Proof 7.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 82
% Number of leaves : 6
% Syntax : Number of formulae : 192 ( 188 unt; 0 def)
% Number of atoms : 204 ( 203 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 42 ( 30 ~; 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 : 298 ( 2 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f0,axiom,
double_divide(double_divide(X,double_divide(double_divide(Y,double_divide(Z,X)),double_divide(Z,identity))),double_divide(identity,identity)) = Y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
fof(f0_nnf,plain,
! [X,Y,Z] : double_divide(double_divide(X,double_divide(double_divide(Y,double_divide(Z,X)),double_divide(Z,identity))),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(Z,X)),double_divide(Z,identity))),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(X2,X0)),double_divide(X2,identity))),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(X3,X1)),double_divide(X3,identity))),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(X3,X1)),double_divide(X3,identity))),double_divide(identity,identity)) = X2,
inference(orient,[status(thm)],[t4]) ).
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(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(t7110,plain,
double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X3,X1)),inverse(X3))),double_divide(identity,identity)) = X2,
inference(step,[status(thm)],[t6,t10]) ).
cnf(t7111,plain,
double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X3,X1)),inverse(X3))),inverse(identity)) = X2,
inference(step,[status(thm)],[t7110,t10]) ).
cnf(t11,plain,
double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X3,X1)),inverse(X3))),inverse(identity)) = X2,
inference(rw,[status(thm)],[t7111]) ).
cnf(t74,plain,
double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X3,X1)),inverse(X3))),inverse(identity)) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(t75,plain,
X1 = double_divide(double_divide(identity,double_divide(double_divide(X1,inverse(X2)),inverse(X2))),inverse(identity)),
inference(cp,[status(thm)],[t74,t10]) ).
cnf(t142,plain,
double_divide(double_divide(identity,double_divide(double_divide(X1,inverse(X2)),inverse(X2))),inverse(identity)) = X1,
inference(orient,[status(thm)],[t75]) ).
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(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(t143,plain,
X1 = double_divide(double_divide(identity,double_divide(identity,inverse(X1))),inverse(identity)),
inference(cp,[status(thm)],[t142,t12]) ).
cnf(t160,plain,
double_divide(double_divide(identity,double_divide(identity,inverse(X1))),inverse(identity)) = X1,
inference(orient,[status(thm)],[t143]) ).
cnf(t161,plain,
identity = double_divide(double_divide(identity,identity),inverse(identity)),
inference(cp,[status(thm)],[t160,t12]) ).
cnf(t7118,plain,
identity = double_divide(inverse(identity),inverse(identity)),
inference(step,[status(thm)],[t161,t10]) ).
cnf(t172,plain,
double_divide(inverse(identity),inverse(identity)) = identity,
inference(orient,[status(thm)],[t7118]) ).
cnf(t180,plain,
inverse(identity) = double_divide(double_divide(identity,double_divide(identity,inverse(identity))),inverse(identity)),
inference(cp,[status(thm)],[t142,t172]) ).
cnf(t7119,plain,
inverse(identity) = identity,
inference(step,[status(thm)],[t180,t160]) ).
cnf(t181,plain,
inverse(identity) = identity,
inference(orient,[status(thm)],[t7119]) ).
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(t7149,plain,
double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X3,X1)),inverse(X3))),identity) = X2,
inference(step,[status(thm)],[t74,t181]) ).
cnf(t7150,plain,
inverse(double_divide(X1,double_divide(double_divide(X2,double_divide(X3,X1)),inverse(X3)))) = X2,
inference(step,[status(thm)],[t7149,t10]) ).
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(t3,plain,
double_divide(double_divide(X1,X2),identity) = multiply(X2,X1),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t7112,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)],[t7112]) ).
cnf(t7151,plain,
multiply(double_divide(double_divide(X2,double_divide(X3,X1)),inverse(X3)),X1) = X2,
inference(step,[status(thm)],[t7150,t13]) ).
cnf(t211,plain,
multiply(double_divide(double_divide(X2,double_divide(X3,X1)),inverse(X3)),X1) = X2,
inference(rw,[status(thm)],[t7151]) ).
cnf(t339,plain,
multiply(double_divide(double_divide(X1,double_divide(X2,X3)),inverse(X2)),X3) = X1,
inference(orient,[status(thm)],[t211]) ).
cnf(t76,plain,
X1 = double_divide(double_divide(inverse(X2),double_divide(double_divide(X1,identity),inverse(X2))),inverse(identity)),
inference(cp,[status(thm)],[t74,t12]) ).
cnf(t7114,plain,
X1 = double_divide(double_divide(inverse(X2),double_divide(inverse(X1),inverse(X2))),inverse(identity)),
inference(step,[status(thm)],[t76,t10]) ).
cnf(t90,plain,
double_divide(double_divide(inverse(X1),double_divide(inverse(X2),inverse(X1))),inverse(identity)) = X2,
inference(orient,[status(thm)],[t7114]) ).
cnf(t7146,plain,
double_divide(double_divide(inverse(X1),double_divide(inverse(X2),inverse(X1))),identity) = X2,
inference(step,[status(thm)],[t90,t181]) ).
cnf(t7147,plain,
inverse(double_divide(inverse(X1),double_divide(inverse(X2),inverse(X1)))) = X2,
inference(step,[status(thm)],[t7146,t10]) ).
cnf(t7148,plain,
multiply(double_divide(inverse(X2),inverse(X1)),inverse(X1)) = X2,
inference(step,[status(thm)],[t7147,t13]) ).
cnf(t210,plain,
multiply(double_divide(inverse(X2),inverse(X1)),inverse(X1)) = X2,
inference(rw,[status(thm)],[t7148]) ).
cnf(t292,plain,
multiply(double_divide(inverse(X1),inverse(X2)),inverse(X2)) = X1,
inference(orient,[status(thm)],[t210]) ).
cnf(t297,plain,
X1 = multiply(double_divide(inverse(X1),identity),inverse(identity)),
inference(cp,[status(thm)],[t292,t181]) ).
cnf(t7168,plain,
X1 = multiply(inverse(inverse(X1)),inverse(identity)),
inference(step,[status(thm)],[t297,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(t7169,plain,
X1 = multiply(multiply(identity,X1),inverse(identity)),
inference(step,[status(thm)],[t7168,t18]) ).
cnf(t7170,plain,
X1 = multiply(multiply(identity,X1),identity),
inference(step,[status(thm)],[t7169,t181]) ).
cnf(t94,plain,
X1 = double_divide(double_divide(inverse(inverse(X1)),identity),inverse(identity)),
inference(cp,[status(thm)],[t90,t12]) ).
cnf(t7115,plain,
X1 = double_divide(inverse(inverse(inverse(X1))),inverse(identity)),
inference(step,[status(thm)],[t94,t10]) ).
cnf(t7116,plain,
X1 = double_divide(multiply(identity,inverse(X1)),inverse(identity)),
inference(step,[status(thm)],[t7115,t18]) ).
cnf(t106,plain,
double_divide(multiply(identity,inverse(X1)),inverse(identity)) = X1,
inference(orient,[status(thm)],[t7116]) ).
cnf(t108,plain,
double_divide(X1,X2) = double_divide(multiply(identity,multiply(X2,X1)),inverse(identity)),
inference(cp,[status(thm)],[t106,t13]) ).
cnf(t125,plain,
double_divide(multiply(identity,multiply(X1,X2)),inverse(identity)) = double_divide(X2,X1),
inference(orient,[status(thm)],[t108]) ).
cnf(t7133,plain,
double_divide(multiply(identity,multiply(X1,X2)),identity) = double_divide(X2,X1),
inference(step,[status(thm)],[t125,t181]) ).
cnf(t7134,plain,
inverse(multiply(identity,multiply(X1,X2))) = double_divide(X2,X1),
inference(step,[status(thm)],[t7133,t10]) ).
cnf(t21,plain,
multiply(identity,inverse(X1)) = inverse(multiply(identity,X1)),
inference(cp,[status(thm)],[t18,t18]) ).
cnf(t26,plain,
inverse(multiply(identity,X1)) = multiply(identity,inverse(X1)),
inference(orient,[status(thm)],[t21]) ).
cnf(t7135,plain,
multiply(identity,inverse(multiply(X1,X2))) = double_divide(X2,X1),
inference(step,[status(thm)],[t7134,t26]) ).
cnf(t205,plain,
multiply(identity,inverse(multiply(X1,X2))) = double_divide(X2,X1),
inference(rw,[status(thm)],[t7135]) ).
cnf(t232,plain,
multiply(identity,inverse(multiply(X1,X2))) = double_divide(X2,X1),
inference(orient,[status(thm)],[t205]) ).
cnf(t7141,plain,
double_divide(double_divide(identity,double_divide(identity,inverse(X1))),identity) = X1,
inference(step,[status(thm)],[t160,t181]) ).
cnf(t7142,plain,
inverse(double_divide(identity,double_divide(identity,inverse(X1)))) = X1,
inference(step,[status(thm)],[t7141,t10]) ).
cnf(t7143,plain,
multiply(double_divide(identity,inverse(X1)),identity) = X1,
inference(step,[status(thm)],[t7142,t13]) ).
cnf(t208,plain,
multiply(double_divide(identity,inverse(X1)),identity) = X1,
inference(rw,[status(thm)],[t7143]) ).
cnf(t222,plain,
multiply(double_divide(identity,inverse(X1)),identity) = X1,
inference(orient,[status(thm)],[t208]) ).
cnf(t233,plain,
double_divide(identity,double_divide(identity,inverse(X1))) = multiply(identity,inverse(X1)),
inference(cp,[status(thm)],[t232,t222]) ).
cnf(t240,plain,
double_divide(identity,double_divide(identity,inverse(X1))) = multiply(identity,inverse(X1)),
inference(orient,[status(thm)],[t233]) ).
cnf(t243,plain,
multiply(identity,inverse(inverse(X1))) = double_divide(identity,double_divide(identity,multiply(identity,X1))),
inference(cp,[status(thm)],[t240,t18]) ).
cnf(t7161,plain,
multiply(identity,multiply(identity,X1)) = double_divide(identity,double_divide(identity,multiply(identity,X1))),
inference(step,[status(thm)],[t243,t18]) ).
cnf(t7137,plain,
double_divide(multiply(identity,inverse(X1)),identity) = X1,
inference(step,[status(thm)],[t106,t181]) ).
cnf(t7138,plain,
inverse(multiply(identity,inverse(X1))) = X1,
inference(step,[status(thm)],[t7137,t10]) ).
cnf(t7139,plain,
multiply(identity,inverse(inverse(X1))) = X1,
inference(step,[status(thm)],[t7138,t26]) ).
cnf(t7140,plain,
multiply(identity,multiply(identity,X1)) = X1,
inference(step,[status(thm)],[t7139,t18]) ).
cnf(t207,plain,
multiply(identity,multiply(identity,X1)) = X1,
inference(rw,[status(thm)],[t7140]) ).
cnf(t214,plain,
multiply(identity,multiply(identity,X1)) = X1,
inference(orient,[status(thm)],[t207]) ).
cnf(t7162,plain,
X1 = double_divide(identity,double_divide(identity,multiply(identity,X1))),
inference(step,[status(thm)],[t7161,t214]) ).
cnf(t244,plain,
double_divide(identity,double_divide(identity,multiply(identity,X1))) = X1,
inference(orient,[status(thm)],[t7162]) ).
cnf(t246,plain,
multiply(identity,X1) = double_divide(identity,double_divide(identity,X1)),
inference(cp,[status(thm)],[t244,t214]) ).
cnf(t251,plain,
double_divide(identity,double_divide(identity,X1)) = multiply(identity,X1),
inference(orient,[status(thm)],[t246]) ).
cnf(t252,plain,
multiply(identity,double_divide(identity,X1)) = double_divide(identity,multiply(identity,X1)),
inference(cp,[status(thm)],[t251,t251]) ).
cnf(t19,plain,
multiply(identity,double_divide(X1,X2)) = inverse(multiply(X2,X1)),
inference(cp,[status(thm)],[t18,t13]) ).
cnf(t34,plain,
multiply(identity,double_divide(X1,X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t19]) ).
cnf(t7164,plain,
inverse(multiply(X1,identity)) = double_divide(identity,multiply(identity,X1)),
inference(step,[status(thm)],[t252,t34]) ).
cnf(t268,plain,
double_divide(identity,multiply(identity,X1)) = inverse(multiply(X1,identity)),
inference(orient,[status(thm)],[t7164]) ).
cnf(t276,plain,
multiply(multiply(identity,X1),identity) = inverse(inverse(multiply(X1,identity))),
inference(cp,[status(thm)],[t13,t268]) ).
cnf(t7167,plain,
multiply(multiply(identity,X1),identity) = multiply(identity,multiply(X1,identity)),
inference(step,[status(thm)],[t276,t18]) ).
cnf(t289,plain,
multiply(multiply(identity,X1),identity) = multiply(identity,multiply(X1,identity)),
inference(orient,[status(thm)],[t7167]) ).
cnf(t7171,plain,
X1 = multiply(identity,multiply(X1,identity)),
inference(step,[status(thm)],[t7170,t289]) ).
cnf(t308,plain,
multiply(identity,multiply(X1,identity)) = X1,
inference(orient,[status(thm)],[t7171]) ).
cnf(t256,plain,
multiply(double_divide(identity,X1),identity) = inverse(multiply(identity,X1)),
inference(cp,[status(thm)],[t13,t251]) ).
cnf(t7166,plain,
multiply(double_divide(identity,X1),identity) = multiply(identity,inverse(X1)),
inference(step,[status(thm)],[t256,t26]) ).
cnf(t283,plain,
multiply(double_divide(identity,X1),identity) = multiply(identity,inverse(X1)),
inference(orient,[status(thm)],[t7166]) ).
cnf(t311,plain,
double_divide(identity,X1) = multiply(identity,multiply(identity,inverse(X1))),
inference(cp,[status(thm)],[t308,t283]) ).
cnf(t7174,plain,
double_divide(identity,X1) = inverse(X1),
inference(step,[status(thm)],[t311,t214]) ).
cnf(t323,plain,
double_divide(identity,X1) = inverse(X1),
inference(orient,[status(thm)],[t7174]) ).
cnf(t343,plain,
X1 = multiply(double_divide(double_divide(X1,inverse(X2)),inverse(identity)),X2),
inference(cp,[status(thm)],[t339,t323]) ).
cnf(t7180,plain,
X1 = multiply(double_divide(double_divide(X1,inverse(X2)),identity),X2),
inference(step,[status(thm)],[t343,t181]) ).
cnf(t7181,plain,
X1 = multiply(inverse(double_divide(X1,inverse(X2))),X2),
inference(step,[status(thm)],[t7180,t10]) ).
cnf(t7182,plain,
X1 = multiply(multiply(inverse(X2),X1),X2),
inference(step,[status(thm)],[t7181,t13]) ).
cnf(t383,plain,
multiply(multiply(inverse(X1),X2),X1) = X2,
inference(orient,[status(thm)],[t7182]) ).
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(t7120,plain,
multiply(inverse(X1),X1) = identity,
inference(step,[status(thm)],[t22,t181]) ).
cnf(t182,plain,
multiply(inverse(X1),X1) = identity,
inference(orient,[status(thm)],[t7120]) ).
cnf(t384,plain,
X1 = multiply(identity,X1),
inference(cp,[status(thm)],[t383,t182]) ).
cnf(t395,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t384]) ).
cnf(t16,plain,
identity = double_divide(double_divide(X1,X2),multiply(X2,X1)),
inference(cp,[status(thm)],[t12,t13]) ).
cnf(t39,plain,
double_divide(double_divide(X1,X2),multiply(X2,X1)) = identity,
inference(orient,[status(thm)],[t16]) ).
cnf(t401,plain,
identity = double_divide(double_divide(X1,identity),X1),
inference(cp,[status(thm)],[t39,t395]) ).
cnf(t7198,plain,
identity = double_divide(inverse(X1),X1),
inference(step,[status(thm)],[t401,t10]) ).
cnf(t419,plain,
double_divide(inverse(X1),X1) = identity,
inference(orient,[status(thm)],[t7198]) ).
cnf(t421,plain,
inverse(double_divide(X1,X2)) = multiply(double_divide(identity,inverse(X1)),X2),
inference(cp,[status(thm)],[t339,t419]) ).
cnf(t7199,plain,
multiply(X2,X1) = multiply(double_divide(identity,inverse(X1)),X2),
inference(step,[status(thm)],[t421,t13]) ).
cnf(t7200,plain,
multiply(X2,X1) = multiply(inverse(inverse(X1)),X2),
inference(step,[status(thm)],[t7199,t323]) ).
cnf(t7183,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t18,t395]) ).
cnf(t396,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t7183]) ).
cnf(t7201,plain,
multiply(X2,X1) = multiply(X1,X2),
inference(step,[status(thm)],[t7200,t396]) ).
cnf(t434,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(orient,[status(thm)],[t7201]) ).
cnf(t7190,plain,
double_divide(X1,X2) = inverse(multiply(X2,X1)),
inference(step,[status(thm)],[t34,t395]) ).
cnf(t405,plain,
double_divide(X1,X2) = inverse(multiply(X2,X1)),
inference(rw,[status(thm)],[t7190]) ).
cnf(t423,plain,
inverse(multiply(X1,X2)) = double_divide(X2,X1),
inference(orient,[status(thm)],[t405]) ).
cnf(t439,plain,
multiply(multiply(inverse(X1),X2),X1) = X2,
inference(rw,[status(thm)],[t383]) ).
cnf(t7203,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(step,[status(thm)],[t439,t434]) ).
cnf(t447,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t7203]) ).
cnf(t451,plain,
X1 = multiply(inverse(X2),multiply(X2,X1)),
inference(cp,[status(thm)],[t447,t396]) ).
cnf(t461,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(orient,[status(thm)],[t451]) ).
cnf(t448,plain,
X1 = multiply(X2,multiply(X1,inverse(X2))),
inference(cp,[status(thm)],[t447,t434]) ).
cnf(t454,plain,
multiply(X1,multiply(X2,inverse(X1))) = X2,
inference(orient,[status(thm)],[t448]) ).
cnf(t457,plain,
X1 = multiply(inverse(X2),multiply(X1,X2)),
inference(cp,[status(thm)],[t454,t396]) ).
cnf(t469,plain,
multiply(inverse(X1),multiply(X2,X1)) = X2,
inference(orient,[status(thm)],[t457]) ).
cnf(t474,plain,
inverse(X1) = multiply(inverse(multiply(X1,X2)),X2),
inference(cp,[status(thm)],[t469,t461]) ).
cnf(t7204,plain,
inverse(X1) = multiply(X2,inverse(multiply(X1,X2))),
inference(step,[status(thm)],[t474,t434]) ).
cnf(t7205,plain,
inverse(X1) = multiply(X2,double_divide(X2,X1)),
inference(step,[status(thm)],[t7204,t423]) ).
cnf(t481,plain,
multiply(X1,double_divide(X1,X2)) = inverse(X2),
inference(orient,[status(thm)],[t7205]) ).
cnf(t484,plain,
double_divide(X1,X2) = multiply(inverse(X1),inverse(X2)),
inference(cp,[status(thm)],[t461,t481]) ).
cnf(t521,plain,
multiply(inverse(X1),inverse(X2)) = double_divide(X1,X2),
inference(orient,[status(thm)],[t484]) ).
cnf(t525,plain,
double_divide(X1,multiply(X2,X3)) = multiply(inverse(X1),double_divide(X3,X2)),
inference(cp,[status(thm)],[t521,t423]) ).
cnf(t626,plain,
multiply(inverse(X1),double_divide(X2,X3)) = double_divide(X1,multiply(X3,X2)),
inference(orient,[status(thm)],[t525]) ).
cnf(t644,plain,
double_divide(double_divide(X1,X2),inverse(X3)) = inverse(double_divide(X3,multiply(X2,X1))),
inference(cp,[status(thm)],[t423,t626]) ).
cnf(t487,plain,
double_divide(inverse(X1),X2) = multiply(X1,inverse(X2)),
inference(cp,[status(thm)],[t447,t481]) ).
cnf(t499,plain,
double_divide(inverse(X1),X2) = multiply(X1,inverse(X2)),
inference(orient,[status(thm)],[t487]) ).
cnf(t435,plain,
double_divide(X1,X2) = inverse(multiply(X1,X2)),
inference(cp,[status(thm)],[t423,t434]) ).
cnf(t7202,plain,
double_divide(X1,X2) = double_divide(X2,X1),
inference(step,[status(thm)],[t435,t423]) ).
cnf(t442,plain,
double_divide(X1,X2) = double_divide(X2,X1),
inference(orient,[status(thm)],[t7202]) ).
cnf(t500,plain,
multiply(X1,inverse(X2)) = double_divide(X2,inverse(X1)),
inference(cp,[status(thm)],[t499,t442]) ).
cnf(t506,plain,
double_divide(X1,inverse(X2)) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t500]) ).
cnf(t7347,plain,
multiply(X3,inverse(double_divide(X1,X2))) = inverse(double_divide(X3,multiply(X2,X1))),
inference(step,[status(thm)],[t644,t506]) ).
cnf(t7348,plain,
multiply(X3,multiply(X2,X1)) = inverse(double_divide(X3,multiply(X2,X1))),
inference(step,[status(thm)],[t7347,t13]) ).
cnf(t7349,plain,
multiply(X3,multiply(X2,X1)) = multiply(multiply(X2,X1),X3),
inference(step,[status(thm)],[t7348,t13]) ).
cnf(t441,plain,
multiply(double_divide(double_divide(X1,double_divide(X2,X3)),inverse(X2)),X3) = X1,
inference(rw,[status(thm)],[t339]) ).
cnf(t7216,plain,
multiply(X3,double_divide(double_divide(X1,double_divide(X2,X3)),inverse(X2))) = X1,
inference(step,[status(thm)],[t441,t434]) ).
cnf(t7217,plain,
multiply(X3,multiply(X2,inverse(double_divide(X1,double_divide(X2,X3))))) = X1,
inference(step,[status(thm)],[t7216,t506]) ).
cnf(t7218,plain,
multiply(X3,multiply(X2,multiply(double_divide(X2,X3),X1))) = X1,
inference(step,[status(thm)],[t7217,t13]) ).
cnf(t1337,plain,
multiply(X1,multiply(X2,multiply(double_divide(X2,X1),X3))) = X3,
inference(orient,[status(thm)],[t7218]) ).
cnf(t450,plain,
X1 = multiply(double_divide(X2,X3),multiply(multiply(X3,X2),X1)),
inference(cp,[status(thm)],[t447,t13]) ).
cnf(t700,plain,
multiply(double_divide(X1,X2),multiply(multiply(X2,X1),X3)) = X3,
inference(orient,[status(thm)],[t450]) ).
cnf(t1343,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(cp,[status(thm)],[t1337,t700]) ).
cnf(t1396,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t1343]) ).
cnf(t7350,plain,
multiply(X3,multiply(X2,X1)) = multiply(X2,multiply(X1,X3)),
inference(step,[status(thm)],[t7349,t1396]) ).
cnf(t6892,plain,
multiply(X1,multiply(X2,X3)) = multiply(X2,multiply(X3,X1)),
inference(orient,[status(thm)],[t7350]) ).
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/sandbox/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(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(g0_0,plain,
true != 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),
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
true != 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),
inference(rw,[status(thm)],[g0_0]) ).
cnf(g0_2,plain,
true != ifeq(inverse(identity),inverse(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),
inference(rw,[status(thm)],[g0_1,t181]) ).
cnf(g0_3,plain,
true != 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),
inference(rw,[status(thm)],[g0_2,t9]) ).
cnf(g0_4,plain,
true != 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),
inference(rw,[status(thm)],[g0_3,t395]) ).
cnf(g0_5,plain,
true != ifeq(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3)),ifeq(multiply(a4,b4),multiply(b4,a4),false,true),true),
inference(rw,[status(thm)],[g0_4,t9]) ).
cnf(g0_6,plain,
true != ifeq(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3)),ifeq(multiply(a4,b4),multiply(a4,b4),false,true),true),
inference(rw,[status(thm)],[g0_5,t434]) ).
cnf(g0_7,plain,
true != ifeq(multiply(multiply(a3,b3),c3),multiply(a3,multiply(c3,b3)),ifeq(multiply(a4,b4),multiply(a4,b4),false,true),true),
inference(rw,[status(thm)],[g0_6,t434]) ).
cnf(g0_8,plain,
true != ifeq(multiply(multiply(b3,a3),c3),multiply(a3,multiply(c3,b3)),ifeq(multiply(a4,b4),multiply(a4,b4),false,true),true),
inference(rw,[status(thm)],[g0_7,t434]) ).
cnf(g0_9,plain,
true != ifeq(multiply(c3,multiply(b3,a3)),multiply(a3,multiply(c3,b3)),ifeq(multiply(a4,b4),multiply(a4,b4),false,true),true),
inference(rw,[status(thm)],[g0_8,t434]) ).
cnf(g0_10,plain,
true != ifeq(multiply(c3,multiply(b3,a3)),multiply(a3,multiply(c3,b3)),false,true),
inference(rw,[status(thm)],[g0_9,t9]) ).
cnf(g0_11,plain,
true != ifeq(multiply(c3,multiply(b3,a3)),multiply(c3,multiply(b3,a3)),false,true),
inference(rw,[status(thm)],[g0_10,t6892]) ).
cnf(g0_12,plain,
true != false,
inference(rw,[status(thm)],[g0_11,t9]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP101-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.33 % Computer : n011.cluster.edu
% 0.08/0.33 % Model : x86_64 x86_64
% 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.33 % Memory : 8046.5625MB
% 0.08/0.33 % OS : Linux 6.8.0-71-generic
% 0.08/0.33 % CPULimit : 300
% 0.08/0.33 % WCLimit : 300
% 0.08/0.33 % DateTime : Wed Sep 23 13:31:27 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.34 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 7.03/1.32 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.03/1.32 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------