%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP078-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 : n004.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 7.63s 1.57s
% Output : Proof 7.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 59
% Number of leaves : 20
% Syntax : Number of formulae : 222 ( 218 unt; 0 def)
% Number of atoms : 230 ( 229 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 : 26 ( 26 usr; 22 con; 0-4 aty)
% Number of variables : 76 ( 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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',multiply) ).
fof(f1_nnf,plain,
! [X,Y] : multiply(X,Y) = double_divide(double_divide(Y,X),identity),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y] : multiply(X,Y) = double_divide(double_divide(Y,X),identity),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
multiply(X0,X1) = double_divide(double_divide(X1,X0),identity),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(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/sandbox2/benchmark/theBenchmark.p',inverse) ).
fof(f2_nnf,plain,
! [X] : inverse(X) = double_divide(X,identity),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X] : inverse(X) = double_divide(X,identity),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
inverse(X0) = double_divide(X0,identity),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(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/sandbox2/benchmark/theBenchmark.p',identity) ).
fof(f3_nnf,plain,
! [X] : identity = double_divide(X,inverse(X)),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X] : identity = double_divide(X,inverse(X)),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
identity = double_divide(X0,inverse(X0)),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(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(t1905,plain,
sF1 = identity,
inference(step,[status(thm)],[t5,t24]) ).
cnf(t30,plain,
identity = sF1,
inference(orient,[status(thm)],[t1905]) ).
cnf(t1926,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(t1922,plain,
double_divide(X1,double_divide(X1,sF1)) = sF1,
inference(step,[status(thm)],[t33,t30]) ).
cnf(t64,plain,
double_divide(X1,double_divide(X1,sF1)) = sF1,
inference(orient,[status(thm)],[t1922]) ).
cnf(t1927,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)],[t1926,t64]) ).
cnf(t1928,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)],[t1927,t30]) ).
cnf(t6,axiom,
sF2 = double_divide(double_divide(a1,double_divide(a1,identity)),identity),
introduced(definition) ).
cnf(t1923,plain,
sF2 = double_divide(double_divide(a1,double_divide(a1,sF1)),identity),
inference(step,[status(thm)],[t6,t30]) ).
cnf(t1924,plain,
sF2 = double_divide(sF1,identity),
inference(step,[status(thm)],[t1923,t64]) ).
cnf(t1925,plain,
sF2 = double_divide(sF1,sF1),
inference(step,[status(thm)],[t1924,t30]) ).
cnf(t81,plain,
double_divide(sF1,sF1) = sF2,
inference(orient,[status(thm)],[t1925]) ).
cnf(t1929,plain,
ifeq(sF2,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)],[t1928,t81]) ).
cnf(t1930,plain,
ifeq(sF2,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)],[t1929,t30]) ).
cnf(t1931,plain,
ifeq(sF2,sF1,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) = true,
inference(step,[status(thm)],[t1930,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(t1907,plain,
double_divide(a2,sF1) = sF3,
inference(step,[status(thm)],[t21,t30]) ).
cnf(t32,plain,
double_divide(a2,sF1) = sF3,
inference(rw,[status(thm)],[t1907]) ).
cnf(t52,plain,
double_divide(a2,sF1) = sF3,
inference(orient,[status(thm)],[t32]) ).
cnf(t1932,plain,
ifeq(sF2,sF1,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) = true,
inference(step,[status(thm)],[t1931,t52]) ).
cnf(t1933,plain,
ifeq(sF2,sF1,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) = true,
inference(step,[status(thm)],[t1932,t30]) ).
cnf(t8,axiom,
sF4 = double_divide(double_divide(a2,identity),identity),
introduced(definition) ).
cnf(t1915,plain,
sF4 = double_divide(double_divide(a2,sF1),identity),
inference(step,[status(thm)],[t8,t30]) ).
cnf(t1916,plain,
sF4 = double_divide(sF3,identity),
inference(step,[status(thm)],[t1915,t52]) ).
cnf(t1917,plain,
sF4 = double_divide(sF3,sF1),
inference(step,[status(thm)],[t1916,t30]) ).
cnf(t55,plain,
double_divide(sF3,sF1) = sF4,
inference(orient,[status(thm)],[t1917]) ).
cnf(t1934,plain,
ifeq(sF2,sF1,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) = true,
inference(step,[status(thm)],[t1933,t55]) ).
cnf(t9,axiom,
sF5 = double_divide(b3,a3),
introduced(definition) ).
cnf(t22,plain,
double_divide(b3,a3) = sF5,
inference(orient,[status(thm)],[t9]) ).
cnf(t1935,plain,
ifeq(sF2,sF1,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) = true,
inference(step,[status(thm)],[t1934,t22]) ).
cnf(t1936,plain,
ifeq(sF2,sF1,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) = true,
inference(step,[status(thm)],[t1935,t30]) ).
cnf(t10,axiom,
sF6 = double_divide(double_divide(b3,a3),identity),
introduced(definition) ).
cnf(t1918,plain,
sF6 = double_divide(sF5,identity),
inference(step,[status(thm)],[t10,t22]) ).
cnf(t1919,plain,
sF6 = double_divide(sF5,sF1),
inference(step,[status(thm)],[t1918,t30]) ).
cnf(t58,plain,
double_divide(sF5,sF1) = sF6,
inference(orient,[status(thm)],[t1919]) ).
cnf(t1937,plain,
ifeq(sF2,sF1,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) = true,
inference(step,[status(thm)],[t1936,t58]) ).
cnf(t1938,plain,
ifeq(sF2,sF1,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) = true,
inference(step,[status(thm)],[t1937,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(t1939,plain,
ifeq(sF2,sF1,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) = true,
inference(step,[status(thm)],[t1938,t23]) ).
cnf(t1940,plain,
ifeq(sF2,sF1,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) = true,
inference(step,[status(thm)],[t1939,t30]) ).
cnf(t14,axiom,
sF10 = double_divide(double_divide(c3,b3),identity),
introduced(definition) ).
cnf(t1920,plain,
sF10 = double_divide(sF9,identity),
inference(step,[status(thm)],[t14,t23]) ).
cnf(t1921,plain,
sF10 = double_divide(sF9,sF1),
inference(step,[status(thm)],[t1920,t30]) ).
cnf(t61,plain,
double_divide(sF9,sF1) = sF10,
inference(orient,[status(thm)],[t1921]) ).
cnf(t1941,plain,
ifeq(sF2,sF1,ifeq(sF4,a2,ifeq(double_divide(double_divide(c3,sF6),sF1),double_divide(double_divide(sF10,a3),identity),false,true),true),true) = true,
inference(step,[status(thm)],[t1940,t61]) ).
cnf(t1942,plain,
ifeq(sF2,sF1,ifeq(sF4,a2,ifeq(double_divide(double_divide(c3,sF6),sF1),double_divide(double_divide(sF10,a3),sF1),false,true),true),true) = true,
inference(step,[status(thm)],[t1941,t30]) ).
cnf(t90,plain,
ifeq(sF2,sF1,ifeq(sF4,a2,ifeq(double_divide(double_divide(c3,sF6),sF1),double_divide(double_divide(sF10,a3),sF1),false,true),true),true) = true,
inference(orient,[status(thm)],[t1942]) ).
cnf(t11,axiom,
sF7 = double_divide(c3,double_divide(double_divide(b3,a3),identity)),
introduced(definition) ).
cnf(t1943,plain,
sF7 = double_divide(c3,double_divide(sF5,identity)),
inference(step,[status(thm)],[t11,t22]) ).
cnf(t1944,plain,
sF7 = double_divide(c3,double_divide(sF5,sF1)),
inference(step,[status(thm)],[t1943,t30]) ).
cnf(t1945,plain,
sF7 = double_divide(c3,sF6),
inference(step,[status(thm)],[t1944,t58]) ).
cnf(t91,plain,
double_divide(c3,sF6) = sF7,
inference(orient,[status(thm)],[t1945]) ).
cnf(t1946,plain,
ifeq(sF2,sF1,ifeq(sF4,a2,ifeq(double_divide(sF7,sF1),double_divide(double_divide(sF10,a3),sF1),false,true),true),true) = true,
inference(step,[status(thm)],[t90,t91]) ).
cnf(t92,plain,
ifeq(sF2,sF1,ifeq(sF4,a2,ifeq(double_divide(sF7,sF1),double_divide(double_divide(sF10,a3),sF1),false,true),true),true) = true,
inference(rw,[status(thm)],[t1946]) ).
cnf(f0,axiom,
double_divide(double_divide(identity,X),double_divide(identity,double_divide(double_divide(double_divide(X,Y),identity),double_divide(Z,Y)))) = Z,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f0_nnf,plain,
! [X,Y,Z] : double_divide(double_divide(identity,X),double_divide(identity,double_divide(double_divide(double_divide(X,Y),identity),double_divide(Z,Y)))) = Z,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y,Z] : double_divide(double_divide(identity,X),double_divide(identity,double_divide(double_divide(double_divide(X,Y),identity),double_divide(Z,Y)))) = Z,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
double_divide(double_divide(identity,X0),double_divide(identity,double_divide(double_divide(double_divide(X0,X1),identity),double_divide(X2,X1)))) = X2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t2,plain,
double_divide(double_divide(identity,X1),double_divide(identity,double_divide(double_divide(double_divide(X1,X2),identity),double_divide(X3,X2)))) = X3,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t1912,plain,
double_divide(double_divide(sF1,X1),double_divide(identity,double_divide(double_divide(double_divide(X1,X2),identity),double_divide(X3,X2)))) = X3,
inference(step,[status(thm)],[t2,t30]) ).
cnf(t1913,plain,
double_divide(double_divide(sF1,X1),double_divide(sF1,double_divide(double_divide(double_divide(X1,X2),identity),double_divide(X3,X2)))) = X3,
inference(step,[status(thm)],[t1912,t30]) ).
cnf(t1914,plain,
double_divide(double_divide(sF1,X1),double_divide(sF1,double_divide(double_divide(double_divide(X1,X2),sF1),double_divide(X3,X2)))) = X3,
inference(step,[status(thm)],[t1913,t30]) ).
cnf(t39,plain,
double_divide(double_divide(sF1,X1),double_divide(sF1,double_divide(double_divide(double_divide(X1,X2),sF1),double_divide(X3,X2)))) = X3,
inference(orient,[status(thm)],[t1914]) ).
cnf(t85,plain,
sF1 = double_divide(sF1,sF2),
inference(cp,[status(thm)],[t64,t81]) ).
cnf(t86,plain,
double_divide(sF1,sF2) = sF1,
inference(orient,[status(thm)],[t85]) ).
cnf(t88,plain,
X1 = double_divide(double_divide(sF1,sF1),double_divide(sF1,double_divide(double_divide(sF1,sF1),double_divide(X1,sF2)))),
inference(cp,[status(thm)],[t39,t86]) ).
cnf(t1978,plain,
X1 = double_divide(sF2,double_divide(sF1,double_divide(double_divide(sF1,sF1),double_divide(X1,sF2)))),
inference(step,[status(thm)],[t88,t81]) ).
cnf(t1979,plain,
X1 = double_divide(sF2,double_divide(sF1,double_divide(sF2,double_divide(X1,sF2)))),
inference(step,[status(thm)],[t1978,t81]) ).
cnf(t169,plain,
double_divide(sF2,double_divide(sF1,double_divide(sF2,double_divide(X1,sF2)))) = X1,
inference(orient,[status(thm)],[t1979]) ).
cnf(t69,plain,
double_divide(double_divide(X1,sF1),sF1) = double_divide(double_divide(sF1,X1),double_divide(sF1,sF1)),
inference(cp,[status(thm)],[t39,t64]) ).
cnf(t1950,plain,
double_divide(double_divide(X1,sF1),sF1) = double_divide(double_divide(sF1,X1),sF2),
inference(step,[status(thm)],[t69,t81]) ).
cnf(t98,plain,
double_divide(double_divide(X1,sF1),sF1) = double_divide(double_divide(sF1,X1),sF2),
inference(orient,[status(thm)],[t1950]) ).
cnf(t104,plain,
double_divide(double_divide(sF1,sF1),sF2) = double_divide(sF2,sF1),
inference(cp,[status(thm)],[t98,t81]) ).
cnf(t1951,plain,
double_divide(sF2,sF2) = double_divide(sF2,sF1),
inference(step,[status(thm)],[t104,t81]) ).
cnf(t110,plain,
double_divide(sF2,sF2) = double_divide(sF2,sF1),
inference(orient,[status(thm)],[t1951]) ).
cnf(t171,plain,
sF2 = double_divide(sF2,double_divide(sF1,double_divide(sF2,double_divide(sF2,sF1)))),
inference(cp,[status(thm)],[t169,t110]) ).
cnf(t1980,plain,
sF2 = double_divide(sF2,double_divide(sF1,sF1)),
inference(step,[status(thm)],[t171,t64]) ).
cnf(t1981,plain,
sF2 = double_divide(sF2,sF2),
inference(step,[status(thm)],[t1980,t81]) ).
cnf(t1982,plain,
sF2 = double_divide(sF2,sF1),
inference(step,[status(thm)],[t1981,t110]) ).
cnf(t182,plain,
double_divide(sF2,sF1) = sF2,
inference(orient,[status(thm)],[t1982]) ).
cnf(t188,plain,
sF1 = double_divide(sF2,sF2),
inference(cp,[status(thm)],[t64,t182]) ).
cnf(t1983,plain,
double_divide(sF2,sF2) = sF2,
inference(step,[status(thm)],[t110,t182]) ).
cnf(t183,plain,
double_divide(sF2,sF2) = sF2,
inference(orient,[status(thm)],[t1983]) ).
cnf(t1985,plain,
sF1 = sF2,
inference(step,[status(thm)],[t188,t183]) ).
cnf(t189,plain,
sF2 = sF1,
inference(orient,[status(thm)],[t1985]) ).
cnf(t2087,plain,
ifeq(sF1,sF1,ifeq(sF4,a2,ifeq(double_divide(sF7,sF1),double_divide(double_divide(sF10,a3),sF1),false,true),true),true) = true,
inference(step,[status(thm)],[t92,t189]) ).
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(t2088,plain,
ifeq(sF4,a2,ifeq(double_divide(sF7,sF1),double_divide(double_divide(sF10,a3),sF1),false,true),true) = true,
inference(step,[status(thm)],[t2087,t29]) ).
cnf(t1995,plain,
double_divide(sF1,double_divide(sF1,double_divide(sF2,double_divide(X1,sF2)))) = X1,
inference(step,[status(thm)],[t169,t189]) ).
cnf(t1996,plain,
double_divide(sF1,double_divide(sF1,double_divide(sF1,double_divide(X1,sF2)))) = X1,
inference(step,[status(thm)],[t1995,t189]) ).
cnf(t1997,plain,
double_divide(sF1,double_divide(sF1,double_divide(sF1,double_divide(X1,sF1)))) = X1,
inference(step,[status(thm)],[t1996,t189]) ).
cnf(t202,plain,
double_divide(sF1,double_divide(sF1,double_divide(sF1,double_divide(X1,sF1)))) = X1,
inference(rw,[status(thm)],[t1997]) ).
cnf(t390,plain,
double_divide(sF1,double_divide(sF1,double_divide(sF1,double_divide(X1,sF1)))) = X1,
inference(orient,[status(thm)],[t202]) ).
cnf(t396,plain,
double_divide(X1,sF1) = double_divide(sF1,double_divide(sF1,double_divide(sF1,double_divide(double_divide(sF1,X1),sF2)))),
inference(cp,[status(thm)],[t390,t98]) ).
cnf(t2074,plain,
double_divide(X1,sF1) = double_divide(sF1,double_divide(sF1,double_divide(sF1,double_divide(double_divide(sF1,X1),sF1)))),
inference(step,[status(thm)],[t396,t189]) ).
cnf(t2075,plain,
double_divide(X1,sF1) = double_divide(sF1,X1),
inference(step,[status(thm)],[t2074,t390]) ).
cnf(t421,plain,
double_divide(X1,sF1) = double_divide(sF1,X1),
inference(orient,[status(thm)],[t2075]) ).
cnf(t2089,plain,
ifeq(sF4,a2,ifeq(double_divide(sF1,sF7),double_divide(double_divide(sF10,a3),sF1),false,true),true) = true,
inference(step,[status(thm)],[t2088,t421]) ).
cnf(t12,axiom,
sF8 = double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity),
introduced(definition) ).
cnf(t1953,plain,
sF8 = double_divide(double_divide(c3,double_divide(sF5,identity)),identity),
inference(step,[status(thm)],[t12,t22]) ).
cnf(t1954,plain,
sF8 = double_divide(double_divide(c3,double_divide(sF5,sF1)),identity),
inference(step,[status(thm)],[t1953,t30]) ).
cnf(t1955,plain,
sF8 = double_divide(double_divide(c3,sF6),identity),
inference(step,[status(thm)],[t1954,t58]) ).
cnf(t1956,plain,
sF8 = double_divide(sF7,identity),
inference(step,[status(thm)],[t1955,t91]) ).
cnf(t1957,plain,
sF8 = double_divide(sF7,sF1),
inference(step,[status(thm)],[t1956,t30]) ).
cnf(t140,plain,
double_divide(sF7,sF1) = sF8,
inference(orient,[status(thm)],[t1957]) ).
cnf(t144,plain,
double_divide(double_divide(sF1,sF7),sF2) = double_divide(sF8,sF1),
inference(cp,[status(thm)],[t98,t140]) ).
cnf(t148,plain,
double_divide(double_divide(sF1,sF7),sF2) = double_divide(sF8,sF1),
inference(orient,[status(thm)],[t144]) ).
cnf(t1993,plain,
double_divide(double_divide(sF1,sF7),sF1) = double_divide(sF8,sF1),
inference(step,[status(thm)],[t148,t189]) ).
cnf(t200,plain,
double_divide(double_divide(sF1,sF7),sF1) = double_divide(sF8,sF1),
inference(rw,[status(thm)],[t1993]) ).
cnf(t255,plain,
double_divide(double_divide(sF1,sF7),sF1) = double_divide(sF8,sF1),
inference(orient,[status(thm)],[t200]) ).
cnf(t258,plain,
double_divide(sF1,sF7) = double_divide(double_divide(sF1,X1),double_divide(sF1,double_divide(double_divide(double_divide(X1,sF1),sF1),double_divide(sF8,sF1)))),
inference(cp,[status(thm)],[t39,t255]) ).
cnf(t2047,plain,
double_divide(sF1,sF7) = sF8,
inference(step,[status(thm)],[t258,t39]) ).
cnf(t262,plain,
double_divide(sF1,sF7) = sF8,
inference(orient,[status(thm)],[t2047]) ).
cnf(t2090,plain,
ifeq(sF4,a2,ifeq(sF8,double_divide(double_divide(sF10,a3),sF1),false,true),true) = true,
inference(step,[status(thm)],[t2089,t262]) ).
cnf(t2091,plain,
ifeq(sF4,a2,ifeq(sF8,double_divide(sF1,double_divide(sF10,a3)),false,true),true) = true,
inference(step,[status(thm)],[t2090,t421]) ).
cnf(t15,axiom,
sF11 = double_divide(double_divide(double_divide(c3,b3),identity),a3),
introduced(definition) ).
cnf(t1947,plain,
sF11 = double_divide(double_divide(sF9,identity),a3),
inference(step,[status(thm)],[t15,t23]) ).
cnf(t1948,plain,
sF11 = double_divide(double_divide(sF9,sF1),a3),
inference(step,[status(thm)],[t1947,t30]) ).
cnf(t1949,plain,
sF11 = double_divide(sF10,a3),
inference(step,[status(thm)],[t1948,t61]) ).
cnf(t95,plain,
double_divide(sF10,a3) = sF11,
inference(orient,[status(thm)],[t1949]) ).
cnf(t2092,plain,
ifeq(sF4,a2,ifeq(sF8,double_divide(sF1,sF11),false,true),true) = true,
inference(step,[status(thm)],[t2091,t95]) ).
cnf(t16,axiom,
sF12 = double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),
introduced(definition) ).
cnf(t1961,plain,
sF12 = double_divide(double_divide(double_divide(sF9,identity),a3),identity),
inference(step,[status(thm)],[t16,t23]) ).
cnf(t1962,plain,
sF12 = double_divide(double_divide(double_divide(sF9,sF1),a3),identity),
inference(step,[status(thm)],[t1961,t30]) ).
cnf(t1963,plain,
sF12 = double_divide(double_divide(sF10,a3),identity),
inference(step,[status(thm)],[t1962,t61]) ).
cnf(t1964,plain,
sF12 = double_divide(sF11,identity),
inference(step,[status(thm)],[t1963,t95]) ).
cnf(t1965,plain,
sF12 = double_divide(sF11,sF1),
inference(step,[status(thm)],[t1964,t30]) ).
cnf(t156,plain,
double_divide(sF11,sF1) = sF12,
inference(orient,[status(thm)],[t1965]) ).
cnf(t160,plain,
double_divide(double_divide(sF1,sF11),sF2) = double_divide(sF12,sF1),
inference(cp,[status(thm)],[t98,t156]) ).
cnf(t165,plain,
double_divide(double_divide(sF1,sF11),sF2) = double_divide(sF12,sF1),
inference(orient,[status(thm)],[t160]) ).
cnf(t1994,plain,
double_divide(double_divide(sF1,sF11),sF1) = double_divide(sF12,sF1),
inference(step,[status(thm)],[t165,t189]) ).
cnf(t201,plain,
double_divide(double_divide(sF1,sF11),sF1) = double_divide(sF12,sF1),
inference(rw,[status(thm)],[t1994]) ).
cnf(t267,plain,
double_divide(double_divide(sF1,sF11),sF1) = double_divide(sF12,sF1),
inference(orient,[status(thm)],[t201]) ).
cnf(t270,plain,
double_divide(sF1,sF11) = double_divide(double_divide(sF1,X1),double_divide(sF1,double_divide(double_divide(double_divide(X1,sF1),sF1),double_divide(sF12,sF1)))),
inference(cp,[status(thm)],[t39,t267]) ).
cnf(t2049,plain,
double_divide(sF1,sF11) = sF12,
inference(step,[status(thm)],[t270,t39]) ).
cnf(t273,plain,
double_divide(sF1,sF11) = sF12,
inference(orient,[status(thm)],[t2049]) ).
cnf(t2093,plain,
ifeq(sF4,a2,ifeq(sF8,sF12,false,true),true) = true,
inference(step,[status(thm)],[t2092,t273]) ).
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(t1966,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(t1967,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)],[t1966,t30]) ).
cnf(t1968,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)],[t1967,t58]) ).
cnf(t1969,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)],[t1968,t91]) ).
cnf(t1970,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)],[t1969,t30]) ).
cnf(t1971,plain,
sF13 = ifeq(sF8,double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),false,true),
inference(step,[status(thm)],[t1970,t140]) ).
cnf(t1972,plain,
sF13 = ifeq(sF8,double_divide(double_divide(double_divide(sF9,identity),a3),identity),false,true),
inference(step,[status(thm)],[t1971,t23]) ).
cnf(t1973,plain,
sF13 = ifeq(sF8,double_divide(double_divide(double_divide(sF9,sF1),a3),identity),false,true),
inference(step,[status(thm)],[t1972,t30]) ).
cnf(t1974,plain,
sF13 = ifeq(sF8,double_divide(double_divide(sF10,a3),identity),false,true),
inference(step,[status(thm)],[t1973,t61]) ).
cnf(t1975,plain,
sF13 = ifeq(sF8,double_divide(sF11,identity),false,true),
inference(step,[status(thm)],[t1974,t95]) ).
cnf(t1976,plain,
sF13 = ifeq(sF8,double_divide(sF11,sF1),false,true),
inference(step,[status(thm)],[t1975,t30]) ).
cnf(t1977,plain,
sF13 = ifeq(sF8,sF12,false,true),
inference(step,[status(thm)],[t1976,t156]) ).
cnf(t161,plain,
ifeq(sF8,sF12,false,true) = sF13,
inference(orient,[status(thm)],[t1977]) ).
cnf(t2094,plain,
ifeq(sF4,a2,sF13,true) = true,
inference(step,[status(thm)],[t2093,t161]) ).
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(t1998,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(t1999,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)],[t1998,t52]) ).
cnf(t2000,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)],[t1999,t30]) ).
cnf(t2001,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)],[t2000,t55]) ).
cnf(t2002,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)],[t2001,t22]) ).
cnf(t2003,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)],[t2002,t30]) ).
cnf(t2004,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)],[t2003,t58]) ).
cnf(t2005,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)],[t2004,t91]) ).
cnf(t2006,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)],[t2005,t30]) ).
cnf(t2007,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)],[t2006,t140]) ).
cnf(t2008,plain,
sF14 = ifeq(sF4,a2,ifeq(sF8,double_divide(double_divide(double_divide(sF9,identity),a3),identity),false,true),true),
inference(step,[status(thm)],[t2007,t23]) ).
cnf(t2009,plain,
sF14 = ifeq(sF4,a2,ifeq(sF8,double_divide(double_divide(double_divide(sF9,sF1),a3),identity),false,true),true),
inference(step,[status(thm)],[t2008,t30]) ).
cnf(t2010,plain,
sF14 = ifeq(sF4,a2,ifeq(sF8,double_divide(double_divide(sF10,a3),identity),false,true),true),
inference(step,[status(thm)],[t2009,t61]) ).
cnf(t2011,plain,
sF14 = ifeq(sF4,a2,ifeq(sF8,double_divide(sF11,identity),false,true),true),
inference(step,[status(thm)],[t2010,t95]) ).
cnf(t2012,plain,
sF14 = ifeq(sF4,a2,ifeq(sF8,double_divide(sF11,sF1),false,true),true),
inference(step,[status(thm)],[t2011,t30]) ).
cnf(t2013,plain,
sF14 = ifeq(sF4,a2,ifeq(sF8,sF12,false,true),true),
inference(step,[status(thm)],[t2012,t156]) ).
cnf(t2014,plain,
sF14 = ifeq(sF4,a2,sF13,true),
inference(step,[status(thm)],[t2013,t161]) ).
cnf(t204,plain,
ifeq(sF4,a2,sF13,true) = sF14,
inference(orient,[status(thm)],[t2014]) ).
cnf(t2095,plain,
sF14 = true,
inference(step,[status(thm)],[t2094,t204]) ).
cnf(t443,plain,
true = sF14,
inference(orient,[status(thm)],[t2095]) ).
cnf(t2097,plain,
ifeq(sF4,a2,sF13,sF14) = sF14,
inference(step,[status(thm)],[t204,t443]) ).
cnf(t445,plain,
ifeq(sF4,a2,sF13,sF14) = sF14,
inference(rw,[status(thm)],[t2097]) ).
cnf(t458,plain,
ifeq(sF4,a2,sF13,sF14) = sF14,
inference(orient,[status(thm)],[t445]) ).
cnf(t851,plain,
ifeq(sF4,sF4,sF13,sF14) = sF14,
inference(rw,[status(thm)],[t458]) ).
cnf(t2131,plain,
sF13 = sF14,
inference(step,[status(thm)],[t851,t29]) ).
cnf(t935,plain,
sF14 = sF13,
inference(orient,[status(thm)],[t2131]) ).
cnf(t2134,plain,
true = sF13,
inference(step,[status(thm)],[t443,t935]) ).
cnf(t938,plain,
true = sF13,
inference(orient,[status(thm)],[t2134]) ).
cnf(t2096,plain,
ifeq(sF8,sF12,false,sF14) = sF13,
inference(step,[status(thm)],[t161,t443]) ).
cnf(t444,plain,
ifeq(sF8,sF12,false,sF14) = sF13,
inference(rw,[status(thm)],[t2096]) ).
cnf(t457,plain,
ifeq(sF8,sF12,false,sF14) = sF13,
inference(orient,[status(thm)],[t444]) ).
cnf(t2136,plain,
ifeq(sF8,sF12,false,sF13) = sF13,
inference(step,[status(thm)],[t457,t935]) ).
cnf(t940,plain,
ifeq(sF8,sF12,false,sF13) = sF13,
inference(rw,[status(thm)],[t2136]) ).
cnf(t969,plain,
ifeq(sF8,sF12,false,sF13) = sF13,
inference(orient,[status(thm)],[t940]) ).
cnf(t1330,plain,
ifeq(sF8,sF8,false,sF13) = sF13,
inference(rw,[status(thm)],[t969]) ).
cnf(t2205,plain,
false = sF13,
inference(step,[status(thm)],[t1330,t29]) ).
cnf(t1904,plain,
false = sF13,
inference(orient,[status(thm)],[t2205]) ).
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,t938]) ).
cnf(g0_1,plain,
sF13 != sF13,
inference(rw,[status(thm)],[g0_0,t1904]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP078-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n004.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Wed Sep 23 13:28:21 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.63/1.57 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.63/1.57 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------