%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP094-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 : n019.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:09 PM UTC 2026
% Result : Unsatisfiable 4.65s 6.14s
% Output : Proof 4.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 22
% Syntax : Number of formulae : 185 ( 181 unt; 0 def)
% Number of atoms : 197 ( 196 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 31 ( 19 ~; 12 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 28 con; 0-4 aty)
% Number of variables : 64 ( 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(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
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(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
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(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
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(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(u0,axiom,
ifeq(multiply(inverse(a1),a1),multiply(inverse(b1),b1),ifeq(multiply(multiply(inverse(b2),b2),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(f1,axiom,
multiply(X,Y) = divide(X,divide(identity,Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiply) ).
fof(f1_nnf,plain,
! [X,Y] : multiply(X,Y) = divide(X,divide(identity,Y)),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y] : multiply(X,Y) = divide(X,divide(identity,Y)),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
multiply(X0,X1) = divide(X0,divide(identity,X1)),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(d0,axiom,
multiply(X0,X1) = divide(X0,divide(identity,X1)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(f2,axiom,
inverse(X) = divide(identity,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inverse) ).
fof(f2_nnf,plain,
! [X] : inverse(X) = divide(identity,X),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X] : inverse(X) = divide(identity,X),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
inverse(X0) = divide(identity,X0),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(d1,axiom,
inverse(X0) = divide(identity,X0),
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t3,plain,
ifeq(divide(divide(identity,a1),divide(identity,a1)),divide(divide(identity,b1),divide(identity,b1)),ifeq(divide(divide(divide(identity,b2),divide(identity,b2)),divide(identity,a2)),a2,ifeq(divide(divide(a3,divide(identity,b3)),divide(identity,c3)),divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),true),true) = true,
inference(definition_unfolding,[status(thm)],[u0,d0,d1]) ).
cnf(f3,axiom,
identity = divide(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity) ).
fof(f3_nnf,plain,
! [X] : identity = divide(X,X),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X] : identity = divide(X,X),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
identity = divide(X0,X0),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t0,plain,
divide(X1,X1) = identity,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t27,plain,
divide(X1,X1) = identity,
inference(orient,[status(thm)],[t0]) ).
cnf(t5,axiom,
sF1 = divide(divide(identity,a1),divide(identity,a1)),
introduced(definition) ).
cnf(t791,plain,
sF1 = identity,
inference(step,[status(thm)],[t5,t27]) ).
cnf(t72,plain,
identity = sF1,
inference(orient,[status(thm)],[t791]) ).
cnf(t792,plain,
divide(X1,X1) = sF1,
inference(step,[status(thm)],[t27,t72]) ).
cnf(t73,plain,
divide(X1,X1) = sF1,
inference(orient,[status(thm)],[t792]) ).
cnf(t803,plain,
ifeq(sF1,divide(divide(identity,b1),divide(identity,b1)),ifeq(divide(divide(divide(identity,b2),divide(identity,b2)),divide(identity,a2)),a2,ifeq(divide(divide(a3,divide(identity,b3)),divide(identity,c3)),divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),true),true) = true,
inference(step,[status(thm)],[t3,t73]) ).
cnf(t804,plain,
ifeq(sF1,sF1,ifeq(divide(divide(divide(identity,b2),divide(identity,b2)),divide(identity,a2)),a2,ifeq(divide(divide(a3,divide(identity,b3)),divide(identity,c3)),divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),true),true) = true,
inference(step,[status(thm)],[t803,t73]) ).
cnf(t1,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t36,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(t805,plain,
ifeq(divide(divide(divide(identity,b2),divide(identity,b2)),divide(identity,a2)),a2,ifeq(divide(divide(a3,divide(identity,b3)),divide(identity,c3)),divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),true) = true,
inference(step,[status(thm)],[t804,t36]) ).
cnf(t806,plain,
ifeq(divide(sF1,divide(identity,a2)),a2,ifeq(divide(divide(a3,divide(identity,b3)),divide(identity,c3)),divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),true) = true,
inference(step,[status(thm)],[t805,t73]) ).
cnf(t807,plain,
ifeq(divide(sF1,divide(sF1,a2)),a2,ifeq(divide(divide(a3,divide(identity,b3)),divide(identity,c3)),divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),true) = true,
inference(step,[status(thm)],[t806,t72]) ).
cnf(t10,axiom,
sF6 = divide(identity,a2),
introduced(definition) ).
cnf(t31,plain,
divide(identity,a2) = sF6,
inference(orient,[status(thm)],[t10]) ).
cnf(t797,plain,
divide(sF1,a2) = sF6,
inference(step,[status(thm)],[t31,t72]) ).
cnf(t78,plain,
divide(sF1,a2) = sF6,
inference(rw,[status(thm)],[t797]) ).
cnf(t87,plain,
divide(sF1,a2) = sF6,
inference(orient,[status(thm)],[t78]) ).
cnf(t808,plain,
ifeq(divide(sF1,sF6),a2,ifeq(divide(divide(a3,divide(identity,b3)),divide(identity,c3)),divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),true) = true,
inference(step,[status(thm)],[t807,t87]) ).
cnf(t809,plain,
ifeq(divide(sF1,sF6),a2,ifeq(divide(divide(a3,divide(sF1,b3)),divide(identity,c3)),divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),true) = true,
inference(step,[status(thm)],[t808,t72]) ).
cnf(t12,axiom,
sF8 = divide(identity,b3),
introduced(definition) ).
cnf(t32,plain,
divide(identity,b3) = sF8,
inference(orient,[status(thm)],[t12]) ).
cnf(t798,plain,
divide(sF1,b3) = sF8,
inference(step,[status(thm)],[t32,t72]) ).
cnf(t79,plain,
divide(sF1,b3) = sF8,
inference(rw,[status(thm)],[t798]) ).
cnf(t88,plain,
divide(sF1,b3) = sF8,
inference(orient,[status(thm)],[t79]) ).
cnf(t810,plain,
ifeq(divide(sF1,sF6),a2,ifeq(divide(divide(a3,sF8),divide(identity,c3)),divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),true) = true,
inference(step,[status(thm)],[t809,t88]) ).
cnf(t13,axiom,
sF9 = divide(a3,divide(identity,b3)),
introduced(definition) ).
cnf(t787,plain,
sF9 = divide(a3,sF8),
inference(step,[status(thm)],[t13,t32]) ).
cnf(t60,plain,
divide(a3,sF8) = sF9,
inference(orient,[status(thm)],[t787]) ).
cnf(t811,plain,
ifeq(divide(sF1,sF6),a2,ifeq(divide(sF9,divide(identity,c3)),divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),true) = true,
inference(step,[status(thm)],[t810,t60]) ).
cnf(t812,plain,
ifeq(divide(sF1,sF6),a2,ifeq(divide(sF9,divide(sF1,c3)),divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),true) = true,
inference(step,[status(thm)],[t811,t72]) ).
cnf(t813,plain,
ifeq(divide(sF1,sF6),a2,ifeq(divide(sF9,divide(sF1,c3)),divide(a3,divide(sF1,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),true) = true,
inference(step,[status(thm)],[t812,t72]) ).
cnf(t814,plain,
ifeq(divide(sF1,sF6),a2,ifeq(divide(sF9,divide(sF1,c3)),divide(a3,divide(sF1,divide(b3,divide(sF1,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),true) = true,
inference(step,[status(thm)],[t813,t72]) ).
cnf(t815,plain,
ifeq(divide(sF1,sF6),a2,ifeq(divide(sF9,divide(sF1,c3)),divide(a3,divide(sF1,divide(b3,divide(sF1,c3)))),ifeq(divide(a4,divide(sF1,b4)),divide(b4,divide(identity,a4)),false,true),true),true) = true,
inference(step,[status(thm)],[t814,t72]) ).
cnf(t816,plain,
ifeq(divide(sF1,sF6),a2,ifeq(divide(sF9,divide(sF1,c3)),divide(a3,divide(sF1,divide(b3,divide(sF1,c3)))),ifeq(divide(a4,divide(sF1,b4)),divide(b4,divide(sF1,a4)),false,true),true),true) = true,
inference(step,[status(thm)],[t815,t72]) ).
cnf(t89,plain,
ifeq(divide(sF1,sF6),a2,ifeq(divide(sF9,divide(sF1,c3)),divide(a3,divide(sF1,divide(b3,divide(sF1,c3)))),ifeq(divide(a4,divide(sF1,b4)),divide(b4,divide(sF1,a4)),false,true),true),true) = true,
inference(orient,[status(thm)],[t816]) ).
cnf(t91,plain,
ifeq(divide(sF1,sF6),a2,ifeq(divide(sF9,sF10),divide(a3,divide(sF1,divide(b3,sF10))),ifeq(divide(a4,divide(sF1,b4)),divide(b4,divide(sF1,a4)),false,true),true),true) = true,
inference(rw,[status(thm)],[t89]) ).
cnf(t11,axiom,
sF7 = divide(divide(divide(identity,b2),divide(identity,b2)),divide(identity,a2)),
introduced(definition) ).
cnf(t833,plain,
sF7 = divide(sF1,divide(identity,a2)),
inference(step,[status(thm)],[t11,t73]) ).
cnf(t834,plain,
sF7 = divide(sF1,divide(sF1,a2)),
inference(step,[status(thm)],[t833,t72]) ).
cnf(t835,plain,
sF7 = divide(sF1,sF6),
inference(step,[status(thm)],[t834,t87]) ).
cnf(t99,plain,
divide(sF1,sF6) = sF7,
inference(orient,[status(thm)],[t835]) ).
cnf(t924,plain,
ifeq(sF7,a2,ifeq(divide(sF9,sF10),divide(a3,divide(sF1,divide(b3,sF10))),ifeq(divide(a4,divide(sF1,b4)),divide(b4,divide(sF1,a4)),false,true),true),true) = true,
inference(step,[status(thm)],[t91,t99]) ).
cnf(f0,axiom,
divide(divide(identity,divide(X,Y)),divide(divide(Y,Z),X)) = Z,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
fof(f0_nnf,plain,
! [X,Y,Z] : divide(divide(identity,divide(X,Y)),divide(divide(Y,Z),X)) = Z,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y,Z] : divide(divide(identity,divide(X,Y)),divide(divide(Y,Z),X)) = Z,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
divide(divide(identity,divide(X0,X1)),divide(divide(X1,X2),X0)) = X2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t2,plain,
divide(divide(identity,divide(X1,X2)),divide(divide(X2,X3),X1)) = X3,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t37,plain,
divide(divide(identity,divide(X1,X2)),divide(divide(X2,X3),X1)) = X3,
inference(orient,[status(thm)],[t2]) ).
cnf(t802,plain,
divide(divide(sF1,divide(X1,X2)),divide(divide(X2,X3),X1)) = X3,
inference(step,[status(thm)],[t37,t72]) ).
cnf(t83,plain,
divide(divide(sF1,divide(X1,X2)),divide(divide(X2,X3),X1)) = X3,
inference(rw,[status(thm)],[t802]) ).
cnf(t100,plain,
divide(divide(sF1,divide(X1,X2)),divide(divide(X2,X3),X1)) = X3,
inference(orient,[status(thm)],[t83]) ).
cnf(t101,plain,
X1 = divide(divide(sF1,sF1),divide(divide(X2,X1),X2)),
inference(cp,[status(thm)],[t100,t73]) ).
cnf(t842,plain,
X1 = divide(sF1,divide(divide(X2,X1),X2)),
inference(step,[status(thm)],[t101,t73]) ).
cnf(t140,plain,
divide(sF1,divide(divide(X1,X2),X1)) = X2,
inference(orient,[status(thm)],[t842]) ).
cnf(t141,plain,
X1 = divide(sF1,divide(sF1,X1)),
inference(cp,[status(thm)],[t140,t73]) ).
cnf(t163,plain,
divide(sF1,divide(sF1,X1)) = X1,
inference(orient,[status(thm)],[t141]) ).
cnf(t167,plain,
a2 = divide(sF1,sF6),
inference(cp,[status(thm)],[t163,t87]) ).
cnf(t843,plain,
a2 = sF7,
inference(step,[status(thm)],[t167,t99]) ).
cnf(t178,plain,
a2 = sF7,
inference(orient,[status(thm)],[t843]) ).
cnf(t925,plain,
ifeq(sF7,sF7,ifeq(divide(sF9,sF10),divide(a3,divide(sF1,divide(b3,sF10))),ifeq(divide(a4,divide(sF1,b4)),divide(b4,divide(sF1,a4)),false,true),true),true) = true,
inference(step,[status(thm)],[t924,t178]) ).
cnf(t926,plain,
ifeq(divide(sF9,sF10),divide(a3,divide(sF1,divide(b3,sF10))),ifeq(divide(a4,divide(sF1,b4)),divide(b4,divide(sF1,a4)),false,true),true) = true,
inference(step,[status(thm)],[t925,t36]) ).
cnf(t15,axiom,
sF11 = divide(divide(a3,divide(identity,b3)),divide(identity,c3)),
introduced(definition) ).
cnf(t823,plain,
sF11 = divide(divide(a3,divide(sF1,b3)),divide(identity,c3)),
inference(step,[status(thm)],[t15,t72]) ).
cnf(t824,plain,
sF11 = divide(divide(a3,sF8),divide(identity,c3)),
inference(step,[status(thm)],[t823,t88]) ).
cnf(t825,plain,
sF11 = divide(sF9,divide(identity,c3)),
inference(step,[status(thm)],[t824,t60]) ).
cnf(t826,plain,
sF11 = divide(sF9,divide(sF1,c3)),
inference(step,[status(thm)],[t825,t72]) ).
cnf(t14,axiom,
sF10 = divide(identity,c3),
introduced(definition) ).
cnf(t33,plain,
divide(identity,c3) = sF10,
inference(orient,[status(thm)],[t14]) ).
cnf(t799,plain,
divide(sF1,c3) = sF10,
inference(step,[status(thm)],[t33,t72]) ).
cnf(t80,plain,
divide(sF1,c3) = sF10,
inference(rw,[status(thm)],[t799]) ).
cnf(t90,plain,
divide(sF1,c3) = sF10,
inference(orient,[status(thm)],[t80]) ).
cnf(t827,plain,
sF11 = divide(sF9,sF10),
inference(step,[status(thm)],[t826,t90]) ).
cnf(t97,plain,
divide(sF9,sF10) = sF11,
inference(orient,[status(thm)],[t827]) ).
cnf(t927,plain,
ifeq(sF11,divide(a3,divide(sF1,divide(b3,sF10))),ifeq(divide(a4,divide(sF1,b4)),divide(b4,divide(sF1,a4)),false,true),true) = true,
inference(step,[status(thm)],[t926,t97]) ).
cnf(t16,axiom,
sF12 = divide(b3,divide(identity,c3)),
introduced(definition) ).
cnf(t788,plain,
sF12 = divide(b3,sF10),
inference(step,[status(thm)],[t16,t33]) ).
cnf(t63,plain,
divide(b3,sF10) = sF12,
inference(orient,[status(thm)],[t788]) ).
cnf(t928,plain,
ifeq(sF11,divide(a3,divide(sF1,sF12)),ifeq(divide(a4,divide(sF1,b4)),divide(b4,divide(sF1,a4)),false,true),true) = true,
inference(step,[status(thm)],[t927,t63]) ).
cnf(t17,axiom,
sF13 = divide(identity,divide(b3,divide(identity,c3))),
introduced(definition) ).
cnf(t819,plain,
sF13 = divide(sF1,divide(b3,divide(identity,c3))),
inference(step,[status(thm)],[t17,t72]) ).
cnf(t820,plain,
sF13 = divide(sF1,divide(b3,divide(sF1,c3))),
inference(step,[status(thm)],[t819,t72]) ).
cnf(t821,plain,
sF13 = divide(sF1,divide(b3,sF10)),
inference(step,[status(thm)],[t820,t90]) ).
cnf(t822,plain,
sF13 = divide(sF1,sF12),
inference(step,[status(thm)],[t821,t63]) ).
cnf(t96,plain,
divide(sF1,sF12) = sF13,
inference(orient,[status(thm)],[t822]) ).
cnf(t929,plain,
ifeq(sF11,divide(a3,sF13),ifeq(divide(a4,divide(sF1,b4)),divide(b4,divide(sF1,a4)),false,true),true) = true,
inference(step,[status(thm)],[t928,t96]) ).
cnf(t18,axiom,
sF14 = divide(a3,divide(identity,divide(b3,divide(identity,c3)))),
introduced(definition) ).
cnf(t828,plain,
sF14 = divide(a3,divide(sF1,divide(b3,divide(identity,c3)))),
inference(step,[status(thm)],[t18,t72]) ).
cnf(t829,plain,
sF14 = divide(a3,divide(sF1,divide(b3,divide(sF1,c3)))),
inference(step,[status(thm)],[t828,t72]) ).
cnf(t830,plain,
sF14 = divide(a3,divide(sF1,divide(b3,sF10))),
inference(step,[status(thm)],[t829,t90]) ).
cnf(t831,plain,
sF14 = divide(a3,divide(sF1,sF12)),
inference(step,[status(thm)],[t830,t63]) ).
cnf(t832,plain,
sF14 = divide(a3,sF13),
inference(step,[status(thm)],[t831,t96]) ).
cnf(t98,plain,
divide(a3,sF13) = sF14,
inference(orient,[status(thm)],[t832]) ).
cnf(t930,plain,
ifeq(sF11,sF14,ifeq(divide(a4,divide(sF1,b4)),divide(b4,divide(sF1,a4)),false,true),true) = true,
inference(step,[status(thm)],[t929,t98]) ).
cnf(t19,axiom,
sF15 = divide(identity,b4),
introduced(definition) ).
cnf(t34,plain,
divide(identity,b4) = sF15,
inference(orient,[status(thm)],[t19]) ).
cnf(t800,plain,
divide(sF1,b4) = sF15,
inference(step,[status(thm)],[t34,t72]) ).
cnf(t81,plain,
divide(sF1,b4) = sF15,
inference(rw,[status(thm)],[t800]) ).
cnf(t92,plain,
divide(sF1,b4) = sF15,
inference(orient,[status(thm)],[t81]) ).
cnf(t931,plain,
ifeq(sF11,sF14,ifeq(divide(a4,sF15),divide(b4,divide(sF1,a4)),false,true),true) = true,
inference(step,[status(thm)],[t930,t92]) ).
cnf(t20,axiom,
sF16 = divide(a4,divide(identity,b4)),
introduced(definition) ).
cnf(t789,plain,
sF16 = divide(a4,sF15),
inference(step,[status(thm)],[t20,t34]) ).
cnf(t66,plain,
divide(a4,sF15) = sF16,
inference(orient,[status(thm)],[t789]) ).
cnf(t932,plain,
ifeq(sF11,sF14,ifeq(sF16,divide(b4,divide(sF1,a4)),false,true),true) = true,
inference(step,[status(thm)],[t931,t66]) ).
cnf(t21,axiom,
sF17 = divide(identity,a4),
introduced(definition) ).
cnf(t35,plain,
divide(identity,a4) = sF17,
inference(orient,[status(thm)],[t21]) ).
cnf(t801,plain,
divide(sF1,a4) = sF17,
inference(step,[status(thm)],[t35,t72]) ).
cnf(t82,plain,
divide(sF1,a4) = sF17,
inference(rw,[status(thm)],[t801]) ).
cnf(t93,plain,
divide(sF1,a4) = sF17,
inference(orient,[status(thm)],[t82]) ).
cnf(t933,plain,
ifeq(sF11,sF14,ifeq(sF16,divide(b4,sF17),false,true),true) = true,
inference(step,[status(thm)],[t932,t93]) ).
cnf(t22,axiom,
sF18 = divide(b4,divide(identity,a4)),
introduced(definition) ).
cnf(t790,plain,
sF18 = divide(b4,sF17),
inference(step,[status(thm)],[t22,t35]) ).
cnf(t69,plain,
divide(b4,sF17) = sF18,
inference(orient,[status(thm)],[t790]) ).
cnf(t934,plain,
ifeq(sF11,sF14,ifeq(sF16,sF18,false,true),true) = true,
inference(step,[status(thm)],[t933,t69]) ).
cnf(t23,axiom,
sF19 = ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),
introduced(definition) ).
cnf(t836,plain,
sF19 = ifeq(divide(a4,divide(sF1,b4)),divide(b4,divide(identity,a4)),false,true),
inference(step,[status(thm)],[t23,t72]) ).
cnf(t837,plain,
sF19 = ifeq(divide(a4,sF15),divide(b4,divide(identity,a4)),false,true),
inference(step,[status(thm)],[t836,t92]) ).
cnf(t838,plain,
sF19 = ifeq(sF16,divide(b4,divide(identity,a4)),false,true),
inference(step,[status(thm)],[t837,t66]) ).
cnf(t839,plain,
sF19 = ifeq(sF16,divide(b4,divide(sF1,a4)),false,true),
inference(step,[status(thm)],[t838,t72]) ).
cnf(t840,plain,
sF19 = ifeq(sF16,divide(b4,sF17),false,true),
inference(step,[status(thm)],[t839,t93]) ).
cnf(t841,plain,
sF19 = ifeq(sF16,sF18,false,true),
inference(step,[status(thm)],[t840,t69]) ).
cnf(t139,plain,
ifeq(sF16,sF18,false,true) = sF19,
inference(orient,[status(thm)],[t841]) ).
cnf(t935,plain,
ifeq(sF11,sF14,sF19,true) = true,
inference(step,[status(thm)],[t934,t139]) ).
cnf(t24,axiom,
sF20 = ifeq(divide(divide(a3,divide(identity,b3)),divide(identity,c3)),divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),
introduced(definition) ).
cnf(t845,plain,
sF20 = ifeq(divide(divide(a3,divide(sF1,b3)),divide(identity,c3)),divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),
inference(step,[status(thm)],[t24,t72]) ).
cnf(t846,plain,
sF20 = ifeq(divide(divide(a3,sF8),divide(identity,c3)),divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),
inference(step,[status(thm)],[t845,t88]) ).
cnf(t847,plain,
sF20 = ifeq(divide(sF9,divide(identity,c3)),divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),
inference(step,[status(thm)],[t846,t60]) ).
cnf(t848,plain,
sF20 = ifeq(divide(sF9,divide(sF1,c3)),divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),
inference(step,[status(thm)],[t847,t72]) ).
cnf(t849,plain,
sF20 = ifeq(divide(sF9,sF10),divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),
inference(step,[status(thm)],[t848,t90]) ).
cnf(t850,plain,
sF20 = ifeq(sF11,divide(a3,divide(identity,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),
inference(step,[status(thm)],[t849,t97]) ).
cnf(t851,plain,
sF20 = ifeq(sF11,divide(a3,divide(sF1,divide(b3,divide(identity,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),
inference(step,[status(thm)],[t850,t72]) ).
cnf(t852,plain,
sF20 = ifeq(sF11,divide(a3,divide(sF1,divide(b3,divide(sF1,c3)))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),
inference(step,[status(thm)],[t851,t72]) ).
cnf(t853,plain,
sF20 = ifeq(sF11,divide(a3,divide(sF1,divide(b3,sF10))),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),
inference(step,[status(thm)],[t852,t90]) ).
cnf(t854,plain,
sF20 = ifeq(sF11,divide(a3,divide(sF1,sF12)),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),
inference(step,[status(thm)],[t853,t63]) ).
cnf(t855,plain,
sF20 = ifeq(sF11,divide(a3,sF13),ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),
inference(step,[status(thm)],[t854,t96]) ).
cnf(t856,plain,
sF20 = ifeq(sF11,sF14,ifeq(divide(a4,divide(identity,b4)),divide(b4,divide(identity,a4)),false,true),true),
inference(step,[status(thm)],[t855,t98]) ).
cnf(t857,plain,
sF20 = ifeq(sF11,sF14,ifeq(divide(a4,divide(sF1,b4)),divide(b4,divide(identity,a4)),false,true),true),
inference(step,[status(thm)],[t856,t72]) ).
cnf(t858,plain,
sF20 = ifeq(sF11,sF14,ifeq(divide(a4,sF15),divide(b4,divide(identity,a4)),false,true),true),
inference(step,[status(thm)],[t857,t92]) ).
cnf(t859,plain,
sF20 = ifeq(sF11,sF14,ifeq(sF16,divide(b4,divide(identity,a4)),false,true),true),
inference(step,[status(thm)],[t858,t66]) ).
cnf(t860,plain,
sF20 = ifeq(sF11,sF14,ifeq(sF16,divide(b4,divide(sF1,a4)),false,true),true),
inference(step,[status(thm)],[t859,t72]) ).
cnf(t861,plain,
sF20 = ifeq(sF11,sF14,ifeq(sF16,divide(b4,sF17),false,true),true),
inference(step,[status(thm)],[t860,t93]) ).
cnf(t862,plain,
sF20 = ifeq(sF11,sF14,ifeq(sF16,sF18,false,true),true),
inference(step,[status(thm)],[t861,t69]) ).
cnf(t863,plain,
sF20 = ifeq(sF11,sF14,sF19,true),
inference(step,[status(thm)],[t862,t139]) ).
cnf(t201,plain,
ifeq(sF11,sF14,sF19,true) = sF20,
inference(orient,[status(thm)],[t863]) ).
cnf(t936,plain,
sF20 = true,
inference(step,[status(thm)],[t935,t201]) ).
cnf(t304,plain,
true = sF20,
inference(orient,[status(thm)],[t936]) ).
cnf(t938,plain,
ifeq(sF11,sF14,sF19,sF20) = sF20,
inference(step,[status(thm)],[t201,t304]) ).
cnf(t306,plain,
ifeq(sF11,sF14,sF19,sF20) = sF20,
inference(rw,[status(thm)],[t938]) ).
cnf(t472,plain,
ifeq(sF11,sF14,sF19,sF20) = sF20,
inference(orient,[status(thm)],[t306]) ).
cnf(t640,plain,
ifeq(sF11,sF11,sF19,sF20) = sF20,
inference(rw,[status(thm)],[t472]) ).
cnf(t1006,plain,
sF19 = sF20,
inference(step,[status(thm)],[t640,t36]) ).
cnf(t780,plain,
sF20 = sF19,
inference(orient,[status(thm)],[t1006]) ).
cnf(t1011,plain,
true = sF19,
inference(step,[status(thm)],[t304,t780]) ).
cnf(t785,plain,
true = sF19,
inference(orient,[status(thm)],[t1011]) ).
cnf(t937,plain,
ifeq(sF16,sF18,false,sF20) = sF19,
inference(step,[status(thm)],[t139,t304]) ).
cnf(t305,plain,
ifeq(sF16,sF18,false,sF20) = sF19,
inference(rw,[status(thm)],[t937]) ).
cnf(t471,plain,
ifeq(sF16,sF18,false,sF20) = sF19,
inference(orient,[status(thm)],[t305]) ).
cnf(t515,plain,
ifeq(sF16,sF16,false,sF20) = sF19,
inference(rw,[status(thm)],[t471]) ).
cnf(t1003,plain,
false = sF19,
inference(step,[status(thm)],[t515,t36]) ).
cnf(t726,plain,
false = sF19,
inference(orient,[status(thm)],[t1003]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(g0_0,plain,
sF19 != false,
inference(rw,[status(thm)],[goal_0,t785]) ).
cnf(g0_1,plain,
sF19 != sF19,
inference(rw,[status(thm)],[g0_0,t726]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP094-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/5.38 % Computer : n019.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Wed Sep 23 13:30:41 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.10/5.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 4.65/6.14 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.65/6.14 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------