%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP070-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n017.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:06 PM UTC 2026
% Result : Unsatisfiable 7.30s 1.56s
% Output : Proof 7.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 52
% Number of leaves : 21
% Syntax : Number of formulae : 174 ( 170 unt; 0 def)
% Number of atoms : 182 ( 181 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 : 31 ( 31 usr; 27 con; 0-4 aty)
% Number of variables : 16 ( 2 sgn 4 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t20,axiom,
sF17 = ifeq(divide(inverse(a1),inverse(a1)),divide(inverse(b1),inverse(b1)),ifeq(divide(divide(inverse(b2),inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true),
introduced(definition) ).
cnf(t3,axiom,
sF0 = inverse(a1),
introduced(definition) ).
cnf(t21,plain,
inverse(a1) = sF0,
inference(orient,[status(thm)],[t3]) ).
cnf(t7183,plain,
sF17 = ifeq(divide(sF0,inverse(a1)),divide(inverse(b1),inverse(b1)),ifeq(divide(divide(inverse(b2),inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true),
inference(step,[status(thm)],[t20,t21]) ).
cnf(t7184,plain,
sF17 = ifeq(divide(sF0,sF0),divide(inverse(b1),inverse(b1)),ifeq(divide(divide(inverse(b2),inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true),
inference(step,[status(thm)],[t7183,t21]) ).
cnf(t4,axiom,
sF1 = divide(inverse(a1),inverse(a1)),
introduced(definition) ).
cnf(t7121,plain,
sF1 = divide(sF0,inverse(a1)),
inference(step,[status(thm)],[t4,t21]) ).
cnf(t7122,plain,
sF1 = divide(sF0,sF0),
inference(step,[status(thm)],[t7121,t21]) ).
cnf(t30,plain,
divide(sF0,sF0) = sF1,
inference(orient,[status(thm)],[t7122]) ).
cnf(t7185,plain,
sF17 = ifeq(sF1,divide(inverse(b1),inverse(b1)),ifeq(divide(divide(inverse(b2),inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true),
inference(step,[status(thm)],[t7184,t30]) ).
cnf(t5,axiom,
sF2 = inverse(b1),
introduced(definition) ).
cnf(t22,plain,
inverse(b1) = sF2,
inference(orient,[status(thm)],[t5]) ).
cnf(t7186,plain,
sF17 = ifeq(sF1,divide(sF2,inverse(b1)),ifeq(divide(divide(inverse(b2),inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true),
inference(step,[status(thm)],[t7185,t22]) ).
cnf(t7187,plain,
sF17 = ifeq(sF1,divide(sF2,sF2),ifeq(divide(divide(inverse(b2),inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true),
inference(step,[status(thm)],[t7186,t22]) ).
cnf(t6,axiom,
sF3 = divide(inverse(b1),inverse(b1)),
introduced(definition) ).
cnf(t7123,plain,
sF3 = divide(sF2,inverse(b1)),
inference(step,[status(thm)],[t6,t22]) ).
cnf(t7124,plain,
sF3 = divide(sF2,sF2),
inference(step,[status(thm)],[t7123,t22]) ).
cnf(t44,plain,
divide(sF2,sF2) = sF3,
inference(orient,[status(thm)],[t7124]) ).
cnf(t7188,plain,
sF17 = ifeq(sF1,sF3,ifeq(divide(divide(inverse(b2),inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true),
inference(step,[status(thm)],[t7187,t44]) ).
cnf(t7,axiom,
sF4 = inverse(b2),
introduced(definition) ).
cnf(t23,plain,
inverse(b2) = sF4,
inference(orient,[status(thm)],[t7]) ).
cnf(t7189,plain,
sF17 = ifeq(sF1,sF3,ifeq(divide(divide(sF4,inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true),
inference(step,[status(thm)],[t7188,t23]) ).
cnf(t7190,plain,
sF17 = ifeq(sF1,sF3,ifeq(divide(divide(sF4,sF4),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true),
inference(step,[status(thm)],[t7189,t23]) ).
cnf(t8,axiom,
sF5 = divide(inverse(b2),inverse(b2)),
introduced(definition) ).
cnf(t7125,plain,
sF5 = divide(sF4,inverse(b2)),
inference(step,[status(thm)],[t8,t23]) ).
cnf(t7126,plain,
sF5 = divide(sF4,sF4),
inference(step,[status(thm)],[t7125,t23]) ).
cnf(t47,plain,
divide(sF4,sF4) = sF5,
inference(orient,[status(thm)],[t7126]) ).
cnf(t7191,plain,
sF17 = ifeq(sF1,sF3,ifeq(divide(sF5,inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true),
inference(step,[status(thm)],[t7190,t47]) ).
cnf(t9,axiom,
sF6 = inverse(a2),
introduced(definition) ).
cnf(t24,plain,
inverse(a2) = sF6,
inference(orient,[status(thm)],[t9]) ).
cnf(t7192,plain,
sF17 = ifeq(sF1,sF3,ifeq(divide(sF5,sF6),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true),
inference(step,[status(thm)],[t7191,t24]) ).
cnf(t10,axiom,
sF7 = divide(divide(inverse(b2),inverse(b2)),inverse(a2)),
introduced(definition) ).
cnf(t7135,plain,
sF7 = divide(divide(sF4,inverse(b2)),inverse(a2)),
inference(step,[status(thm)],[t10,t23]) ).
cnf(t7136,plain,
sF7 = divide(divide(sF4,sF4),inverse(a2)),
inference(step,[status(thm)],[t7135,t23]) ).
cnf(t7137,plain,
sF7 = divide(sF5,inverse(a2)),
inference(step,[status(thm)],[t7136,t47]) ).
cnf(t7138,plain,
sF7 = divide(sF5,sF6),
inference(step,[status(thm)],[t7137,t24]) ).
cnf(t56,plain,
divide(sF5,sF6) = sF7,
inference(orient,[status(thm)],[t7138]) ).
cnf(t7193,plain,
sF17 = ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true),
inference(step,[status(thm)],[t7192,t56]) ).
cnf(t11,axiom,
sF8 = inverse(b3),
introduced(definition) ).
cnf(t25,plain,
inverse(b3) = sF8,
inference(orient,[status(thm)],[t11]) ).
cnf(t7194,plain,
sF17 = ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(divide(divide(a3,sF8),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true),
inference(step,[status(thm)],[t7193,t25]) ).
cnf(t12,axiom,
sF9 = divide(a3,inverse(b3)),
introduced(definition) ).
cnf(t7119,plain,
sF9 = divide(a3,sF8),
inference(step,[status(thm)],[t12,t25]) ).
cnf(t27,plain,
divide(a3,sF8) = sF9,
inference(orient,[status(thm)],[t7119]) ).
cnf(t7195,plain,
sF17 = ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(divide(sF9,inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true),
inference(step,[status(thm)],[t7194,t27]) ).
cnf(t13,axiom,
sF10 = inverse(c3),
introduced(definition) ).
cnf(t26,plain,
inverse(c3) = sF10,
inference(orient,[status(thm)],[t13]) ).
cnf(t7196,plain,
sF17 = ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(divide(sF9,sF10),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true),
inference(step,[status(thm)],[t7195,t26]) ).
cnf(t14,axiom,
sF11 = divide(divide(a3,inverse(b3)),inverse(c3)),
introduced(definition) ).
cnf(t7129,plain,
sF11 = divide(divide(a3,sF8),inverse(c3)),
inference(step,[status(thm)],[t14,t25]) ).
cnf(t7130,plain,
sF11 = divide(sF9,inverse(c3)),
inference(step,[status(thm)],[t7129,t27]) ).
cnf(t7131,plain,
sF11 = divide(sF9,sF10),
inference(step,[status(thm)],[t7130,t26]) ).
cnf(t52,plain,
divide(sF9,sF10) = sF11,
inference(orient,[status(thm)],[t7131]) ).
cnf(t7197,plain,
sF17 = ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(sF11,divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true),
inference(step,[status(thm)],[t7196,t52]) ).
cnf(t7198,plain,
sF17 = ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(sF11,divide(a3,inverse(divide(b3,sF10))),false,true),true),true),
inference(step,[status(thm)],[t7197,t26]) ).
cnf(t15,axiom,
sF12 = divide(b3,inverse(c3)),
introduced(definition) ).
cnf(t7120,plain,
sF12 = divide(b3,sF10),
inference(step,[status(thm)],[t15,t26]) ).
cnf(t28,plain,
divide(b3,sF10) = sF12,
inference(orient,[status(thm)],[t7120]) ).
cnf(t7199,plain,
sF17 = ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(sF11,divide(a3,inverse(sF12)),false,true),true),true),
inference(step,[status(thm)],[t7198,t28]) ).
cnf(t16,axiom,
sF13 = inverse(divide(b3,inverse(c3))),
introduced(definition) ).
cnf(t7127,plain,
sF13 = inverse(divide(b3,sF10)),
inference(step,[status(thm)],[t16,t26]) ).
cnf(t7128,plain,
sF13 = inverse(sF12),
inference(step,[status(thm)],[t7127,t28]) ).
cnf(t50,plain,
inverse(sF12) = sF13,
inference(orient,[status(thm)],[t7128]) ).
cnf(t7200,plain,
sF17 = ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(sF11,divide(a3,sF13),false,true),true),true),
inference(step,[status(thm)],[t7199,t50]) ).
cnf(t17,axiom,
sF14 = divide(a3,inverse(divide(b3,inverse(c3)))),
introduced(definition) ).
cnf(t7132,plain,
sF14 = divide(a3,inverse(divide(b3,sF10))),
inference(step,[status(thm)],[t17,t26]) ).
cnf(t7133,plain,
sF14 = divide(a3,inverse(sF12)),
inference(step,[status(thm)],[t7132,t28]) ).
cnf(t7134,plain,
sF14 = divide(a3,sF13),
inference(step,[status(thm)],[t7133,t50]) ).
cnf(t54,plain,
divide(a3,sF13) = sF14,
inference(orient,[status(thm)],[t7134]) ).
cnf(t7201,plain,
sF17 = ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(sF11,sF14,false,true),true),true),
inference(step,[status(thm)],[t7200,t54]) ).
cnf(t18,axiom,
sF15 = ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),
introduced(definition) ).
cnf(t7159,plain,
sF15 = ifeq(divide(divide(a3,sF8),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),
inference(step,[status(thm)],[t18,t25]) ).
cnf(t7160,plain,
sF15 = ifeq(divide(sF9,inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),
inference(step,[status(thm)],[t7159,t27]) ).
cnf(t7161,plain,
sF15 = ifeq(divide(sF9,sF10),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),
inference(step,[status(thm)],[t7160,t26]) ).
cnf(t7162,plain,
sF15 = ifeq(sF11,divide(a3,inverse(divide(b3,inverse(c3)))),false,true),
inference(step,[status(thm)],[t7161,t52]) ).
cnf(t7163,plain,
sF15 = ifeq(sF11,divide(a3,inverse(divide(b3,sF10))),false,true),
inference(step,[status(thm)],[t7162,t26]) ).
cnf(t7164,plain,
sF15 = ifeq(sF11,divide(a3,inverse(sF12)),false,true),
inference(step,[status(thm)],[t7163,t28]) ).
cnf(t7165,plain,
sF15 = ifeq(sF11,divide(a3,sF13),false,true),
inference(step,[status(thm)],[t7164,t50]) ).
cnf(t7166,plain,
sF15 = ifeq(sF11,sF14,false,true),
inference(step,[status(thm)],[t7165,t54]) ).
cnf(t150,plain,
ifeq(sF11,sF14,false,true) = sF15,
inference(orient,[status(thm)],[t7166]) ).
cnf(t7202,plain,
sF17 = ifeq(sF1,sF3,ifeq(sF7,a2,sF15,true),true),
inference(step,[status(thm)],[t7201,t150]) ).
cnf(t19,axiom,
sF16 = ifeq(divide(divide(inverse(b2),inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),
introduced(definition) ).
cnf(t7168,plain,
sF16 = ifeq(divide(divide(sF4,inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),
inference(step,[status(thm)],[t19,t23]) ).
cnf(t7169,plain,
sF16 = ifeq(divide(divide(sF4,sF4),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),
inference(step,[status(thm)],[t7168,t23]) ).
cnf(t7170,plain,
sF16 = ifeq(divide(sF5,inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),
inference(step,[status(thm)],[t7169,t47]) ).
cnf(t7171,plain,
sF16 = ifeq(divide(sF5,sF6),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),
inference(step,[status(thm)],[t7170,t24]) ).
cnf(t7172,plain,
sF16 = ifeq(sF7,a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),
inference(step,[status(thm)],[t7171,t56]) ).
cnf(t7173,plain,
sF16 = ifeq(sF7,a2,ifeq(divide(divide(a3,sF8),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),
inference(step,[status(thm)],[t7172,t25]) ).
cnf(t7174,plain,
sF16 = ifeq(sF7,a2,ifeq(divide(sF9,inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),
inference(step,[status(thm)],[t7173,t27]) ).
cnf(t7175,plain,
sF16 = ifeq(sF7,a2,ifeq(divide(sF9,sF10),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),
inference(step,[status(thm)],[t7174,t26]) ).
cnf(t7176,plain,
sF16 = ifeq(sF7,a2,ifeq(sF11,divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),
inference(step,[status(thm)],[t7175,t52]) ).
cnf(t7177,plain,
sF16 = ifeq(sF7,a2,ifeq(sF11,divide(a3,inverse(divide(b3,sF10))),false,true),true),
inference(step,[status(thm)],[t7176,t26]) ).
cnf(t7178,plain,
sF16 = ifeq(sF7,a2,ifeq(sF11,divide(a3,inverse(sF12)),false,true),true),
inference(step,[status(thm)],[t7177,t28]) ).
cnf(t7179,plain,
sF16 = ifeq(sF7,a2,ifeq(sF11,divide(a3,sF13),false,true),true),
inference(step,[status(thm)],[t7178,t50]) ).
cnf(t7180,plain,
sF16 = ifeq(sF7,a2,ifeq(sF11,sF14,false,true),true),
inference(step,[status(thm)],[t7179,t54]) ).
cnf(t7181,plain,
sF16 = ifeq(sF7,a2,sF15,true),
inference(step,[status(thm)],[t7180,t150]) ).
cnf(t263,plain,
ifeq(sF7,a2,sF15,true) = sF16,
inference(orient,[status(thm)],[t7181]) ).
cnf(t7203,plain,
sF17 = ifeq(sF1,sF3,sF16,true),
inference(step,[status(thm)],[t7202,t263]) ).
cnf(f2,negated_conjecture,
( 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/sandbox2/benchmark/theBenchmark.p',prove_these_axioms) ).
fof(f2_nnf,plain,
( 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)],[f2]) ).
fof(f2_sk,plain,
( 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)],[f2_nnf]) ).
cnf(c2,plain,
( 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)],[f2_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)),false,true),true),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(f1,axiom,
multiply(X,Y) = divide(X,inverse(Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiply) ).
fof(f1_nnf,plain,
! [X,Y] : multiply(X,Y) = divide(X,inverse(Y)),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y] : multiply(X,Y) = divide(X,inverse(Y)),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
multiply(X0,X1) = divide(X0,inverse(X1)),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(d0,axiom,
multiply(X0,X1) = divide(X0,inverse(X1)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t2,plain,
ifeq(divide(inverse(a1),inverse(a1)),divide(inverse(b1),inverse(b1)),ifeq(divide(divide(inverse(b2),inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true) = true,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t7140,plain,
ifeq(divide(sF0,inverse(a1)),divide(inverse(b1),inverse(b1)),ifeq(divide(divide(inverse(b2),inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true) = true,
inference(step,[status(thm)],[t2,t21]) ).
cnf(t7141,plain,
ifeq(divide(sF0,sF0),divide(inverse(b1),inverse(b1)),ifeq(divide(divide(inverse(b2),inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true) = true,
inference(step,[status(thm)],[t7140,t21]) ).
cnf(t7142,plain,
ifeq(sF1,divide(inverse(b1),inverse(b1)),ifeq(divide(divide(inverse(b2),inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true) = true,
inference(step,[status(thm)],[t7141,t30]) ).
cnf(t7143,plain,
ifeq(sF1,divide(sF2,inverse(b1)),ifeq(divide(divide(inverse(b2),inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true) = true,
inference(step,[status(thm)],[t7142,t22]) ).
cnf(t7144,plain,
ifeq(sF1,divide(sF2,sF2),ifeq(divide(divide(inverse(b2),inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true) = true,
inference(step,[status(thm)],[t7143,t22]) ).
cnf(t7145,plain,
ifeq(sF1,sF3,ifeq(divide(divide(inverse(b2),inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true) = true,
inference(step,[status(thm)],[t7144,t44]) ).
cnf(t7146,plain,
ifeq(sF1,sF3,ifeq(divide(divide(sF4,inverse(b2)),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true) = true,
inference(step,[status(thm)],[t7145,t23]) ).
cnf(t7147,plain,
ifeq(sF1,sF3,ifeq(divide(divide(sF4,sF4),inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true) = true,
inference(step,[status(thm)],[t7146,t23]) ).
cnf(t7148,plain,
ifeq(sF1,sF3,ifeq(divide(sF5,inverse(a2)),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true) = true,
inference(step,[status(thm)],[t7147,t47]) ).
cnf(t7149,plain,
ifeq(sF1,sF3,ifeq(divide(sF5,sF6),a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true) = true,
inference(step,[status(thm)],[t7148,t24]) ).
cnf(t7150,plain,
ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(divide(divide(a3,inverse(b3)),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true) = true,
inference(step,[status(thm)],[t7149,t56]) ).
cnf(t7151,plain,
ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(divide(divide(a3,sF8),inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true) = true,
inference(step,[status(thm)],[t7150,t25]) ).
cnf(t7152,plain,
ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(divide(sF9,inverse(c3)),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true) = true,
inference(step,[status(thm)],[t7151,t27]) ).
cnf(t7153,plain,
ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(divide(sF9,sF10),divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true) = true,
inference(step,[status(thm)],[t7152,t26]) ).
cnf(t7154,plain,
ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(sF11,divide(a3,inverse(divide(b3,inverse(c3)))),false,true),true),true) = true,
inference(step,[status(thm)],[t7153,t52]) ).
cnf(t7155,plain,
ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(sF11,divide(a3,inverse(divide(b3,sF10))),false,true),true),true) = true,
inference(step,[status(thm)],[t7154,t26]) ).
cnf(t7156,plain,
ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(sF11,divide(a3,inverse(sF12)),false,true),true),true) = true,
inference(step,[status(thm)],[t7155,t28]) ).
cnf(t7157,plain,
ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(sF11,divide(a3,sF13),false,true),true),true) = true,
inference(step,[status(thm)],[t7156,t50]) ).
cnf(t7158,plain,
ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(sF11,sF14,false,true),true),true) = true,
inference(step,[status(thm)],[t7157,t54]) ).
cnf(t73,plain,
ifeq(sF1,sF3,ifeq(sF7,a2,ifeq(sF11,sF14,false,true),true),true) = true,
inference(orient,[status(thm)],[t7158]) ).
cnf(t7167,plain,
ifeq(sF1,sF3,ifeq(sF7,a2,sF15,true),true) = true,
inference(step,[status(thm)],[t73,t150]) ).
cnf(t151,plain,
ifeq(sF1,sF3,ifeq(sF7,a2,sF15,true),true) = true,
inference(rw,[status(thm)],[t7167]) ).
cnf(t152,plain,
ifeq(sF1,sF3,ifeq(sF7,a2,sF15,true),true) = true,
inference(orient,[status(thm)],[t151]) ).
cnf(t7182,plain,
ifeq(sF1,sF3,sF16,true) = true,
inference(step,[status(thm)],[t152,t263]) ).
cnf(t264,plain,
ifeq(sF1,sF3,sF16,true) = true,
inference(rw,[status(thm)],[t7182]) ).
cnf(t265,plain,
ifeq(sF1,sF3,sF16,true) = true,
inference(orient,[status(thm)],[t264]) ).
cnf(t7204,plain,
sF17 = true,
inference(step,[status(thm)],[t7203,t265]) ).
cnf(t414,plain,
true = sF17,
inference(orient,[status(thm)],[t7204]) ).
cnf(t417,plain,
ifeq(sF1,sF3,sF16,sF17) = true,
inference(rw,[status(thm)],[t265]) ).
cnf(t7207,plain,
ifeq(sF1,sF3,sF16,sF17) = sF17,
inference(step,[status(thm)],[t417,t414]) ).
cnf(t420,plain,
ifeq(sF1,sF3,sF16,sF17) = sF17,
inference(orient,[status(thm)],[t7207]) ).
cnf(t1289,plain,
ifeq(sF1,sF1,sF16,sF17) = sF17,
inference(rw,[status(thm)],[t420]) ).
cnf(t0,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t29,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t7216,plain,
sF16 = sF17,
inference(step,[status(thm)],[t1289,t29]) ).
cnf(t1298,plain,
sF17 = sF16,
inference(orient,[status(thm)],[t7216]) ).
cnf(t7217,plain,
true = sF16,
inference(step,[status(thm)],[t414,t1298]) ).
cnf(t1299,plain,
true = sF16,
inference(orient,[status(thm)],[t7217]) ).
cnf(t7206,plain,
ifeq(sF7,a2,sF15,sF17) = sF16,
inference(step,[status(thm)],[t263,t414]) ).
cnf(t416,plain,
ifeq(sF7,a2,sF15,sF17) = sF16,
inference(rw,[status(thm)],[t7206]) ).
cnf(t419,plain,
ifeq(sF7,a2,sF15,sF17) = sF16,
inference(orient,[status(thm)],[t416]) ).
cnf(t7220,plain,
ifeq(sF7,a2,sF15,sF16) = sF16,
inference(step,[status(thm)],[t419,t1298]) ).
cnf(t1302,plain,
ifeq(sF7,a2,sF15,sF16) = sF16,
inference(rw,[status(thm)],[t7220]) ).
cnf(t1347,plain,
ifeq(sF7,a2,sF15,sF16) = sF16,
inference(orient,[status(thm)],[t1302]) ).
cnf(t6046,plain,
ifeq(sF7,sF7,sF15,sF16) = sF16,
inference(rw,[status(thm)],[t1347]) ).
cnf(t7328,plain,
sF15 = sF16,
inference(step,[status(thm)],[t6046,t29]) ).
cnf(t6321,plain,
sF16 = sF15,
inference(orient,[status(thm)],[t7328]) ).
cnf(t7329,plain,
true = sF15,
inference(step,[status(thm)],[t1299,t6321]) ).
cnf(t6322,plain,
true = sF15,
inference(orient,[status(thm)],[t7329]) ).
cnf(t7205,plain,
ifeq(sF11,sF14,false,sF17) = sF15,
inference(step,[status(thm)],[t150,t414]) ).
cnf(t415,plain,
ifeq(sF11,sF14,false,sF17) = sF15,
inference(rw,[status(thm)],[t7205]) ).
cnf(t418,plain,
ifeq(sF11,sF14,false,sF17) = sF15,
inference(orient,[status(thm)],[t415]) ).
cnf(t7219,plain,
ifeq(sF11,sF14,false,sF16) = sF15,
inference(step,[status(thm)],[t418,t1298]) ).
cnf(t1301,plain,
ifeq(sF11,sF14,false,sF16) = sF15,
inference(rw,[status(thm)],[t7219]) ).
cnf(t1346,plain,
ifeq(sF11,sF14,false,sF16) = sF15,
inference(orient,[status(thm)],[t1301]) ).
cnf(t7333,plain,
ifeq(sF11,sF14,false,sF15) = sF15,
inference(step,[status(thm)],[t1346,t6321]) ).
cnf(t6326,plain,
ifeq(sF11,sF14,false,sF15) = sF15,
inference(rw,[status(thm)],[t7333]) ).
cnf(t6546,plain,
ifeq(sF11,sF14,false,sF15) = sF15,
inference(orient,[status(thm)],[t6326]) ).
cnf(t6953,plain,
ifeq(sF11,sF11,false,sF15) = sF15,
inference(rw,[status(thm)],[t6546]) ).
cnf(t7564,plain,
false = sF15,
inference(step,[status(thm)],[t6953,t29]) ).
cnf(t7118,plain,
false = sF15,
inference(orient,[status(thm)],[t7564]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(g0_0,plain,
sF15 != false,
inference(rw,[status(thm)],[goal_0,t6322]) ).
cnf(g0_1,plain,
sF15 != sF15,
inference(rw,[status(thm)],[g0_0,t7118]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP070-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n017.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 13:22:16 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.30/1.56 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.30/1.56 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------