%------------------------------------------------------------------------------
% File : Toma---0.7
% Problem : GRP767-1 : TPTP v9.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_Leo-III %s %d THM
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Jul 15 06:44:52 AM UTC 2025
% Result : Unsatisfiable 62.06s 62.11s
% Output : CNFRefutation 62.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 18
% Syntax : Number of clauses : 125 ( 125 unt; 0 nHn; 3 RR)
% Number of literals : 125 ( 124 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-3 aty)
% Number of variables : 242 ( 13 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,negated_conjecture,
product(j(j(x0)),j(product(x1,x0))) != j(x1),
file('theBenchmark.p',goals) ).
cnf(c1,axiom,
product(X,one) = X,
file('theBenchmark.p',sos01) ).
cnf(c2,axiom,
product(one,X) = X,
file('theBenchmark.p',sos02) ).
cnf(c3,axiom,
i(X) = difference(X,one),
file('theBenchmark.p',sos09) ).
cnf(c4,plain,
difference(X,one) = i(X),
inference(equational,[status(thm)],[c3]) ).
cnf(c5,axiom,
j(X) = quotient(one,X),
file('theBenchmark.p',sos10) ).
cnf(c6,plain,
quotient(one,X) = j(X),
inference(equational,[status(thm)],[c5]) ).
cnf(c7,axiom,
eta(X) = product(i(X),X),
file('theBenchmark.p',sos12) ).
cnf(c8,plain,
product(i(X),X) = eta(X),
inference(equational,[status(thm)],[c7]) ).
cnf(c10,axiom,
product(i(X),X) = product(X,j(X)),
file('theBenchmark.p',sos11) ).
cnf(c11,plain,
product(X,j(X)) = eta(X),
inference(equational,[status(thm)],[c8,c10]) ).
cnf(c13,axiom,
quotient(product(X,Y),Y) = X,
file('theBenchmark.p',sos05) ).
cnf(c14,plain,
quotient(X,X) = one,
inference(equational,[status(thm)],[c2,c13]) ).
cnf(c18,axiom,
difference(X,product(X,Y)) = Y,
file('theBenchmark.p',sos04) ).
cnf(c20,plain,
difference(one,X) = X,
inference(equational,[status(thm)],[c2,c18]) ).
cnf(c21,plain,
difference(X,eta(X)) = j(X),
inference(equational,[status(thm)],[c11,c18]) ).
cnf(c22,axiom,
product(quotient(X,Y),Y) = X,
file('theBenchmark.p',sos06) ).
cnf(c23,plain,
product(j(X),X) = one,
inference(equational,[status(thm)],[c6,c22]) ).
cnf(c24,plain,
i(j(X)) = X,
inference(equational,[status(thm)],[c4,c18,c23]) ).
cnf(c25,axiom,
product(X,difference(X,Y)) = Y,
file('theBenchmark.p',sos03) ).
cnf(c26,plain,
product(X,i(X)) = one,
inference(equational,[status(thm)],[c4,c25]) ).
cnf(c27,plain,
j(i(X)) = X,
inference(equational,[status(thm)],[c6,c13,c26]) ).
cnf(c28,plain,
eta(i(X)) = eta(X),
inference(equational,[status(thm)],[c8,c11,c27]) ).
cnf(c29,plain,
eta(j(X)) = eta(X),
inference(equational,[status(thm)],[c8,c11,c24]) ).
cnf(c30,axiom,
t(X,Y) = quotient(product(X,Y),X),
file('theBenchmark.p',sos19) ).
cnf(c31,plain,
quotient(product(X,Y),X) = t(X,Y),
inference(equational,[status(thm)],[c30]) ).
cnf(c37,plain,
quotient(X,difference(Y,X)) = Y,
inference(equational,[status(thm)],[c13,c25]) ).
cnf(c38,plain,
difference(quotient(X,Y),X) = Y,
inference(equational,[status(thm)],[c18,c22]) ).
cnf(c39,plain,
difference(i(X),eta(X)) = X,
inference(equational,[status(thm)],[c8,c18]) ).
cnf(c47,axiom,
product(X,product(eta(X),Y)) = product(j(j(X)),Y),
file('theBenchmark.p',sos14) ).
cnf(c48,plain,
product(X,eta(X)) = j(j(X)),
inference(equational,[status(thm)],[c1,c47]) ).
cnf(c49,plain,
difference(X,j(j(X))) = eta(X),
inference(equational,[status(thm)],[c18,c48]) ).
cnf(c50,axiom,
product(i(i(X)),Y) = product(eta(X),product(X,Y)),
file('theBenchmark.p',sos13) ).
cnf(c51,plain,
product(eta(X),product(X,Y)) = product(i(i(X)),Y),
inference(equational,[status(thm)],[c50]) ).
cnf(c52,plain,
product(eta(X),X) = i(i(X)),
inference(equational,[status(thm)],[c1,c51]) ).
cnf(c53,plain,
quotient(i(i(X)),X) = eta(X),
inference(equational,[status(thm)],[c13,c52]) ).
cnf(c57,axiom,
product(X,product(Y,eta(X))) = product(product(X,Y),eta(X)),
file('theBenchmark.p',sos15) ).
cnf(c58,plain,
product(product(X,Y),eta(X)) = product(X,product(Y,eta(X))),
inference(equational,[status(thm)],[c57]) ).
cnf(c59,axiom,
product(eta(X),product(Y,Z)) = product(product(eta(X),Y),Z),
file('theBenchmark.p',sos16) ).
cnf(c60,plain,
product(product(eta(X),Y),Z) = product(eta(X),product(Y,Z)),
inference(equational,[status(thm)],[c59]) ).
cnf(c86,axiom,
difference(X,product(product(X,Y),Z)) = quotient(product(Y,product(Z,X)),X),
file('theBenchmark.p',sos07) ).
cnf(c87,plain,
quotient(product(X,product(Y,Z)),Z) = difference(Z,product(product(Z,X),Y)),
inference(equational,[status(thm)],[c86]) ).
cnf(c108,plain,
product(j(j(X)),j(eta(X))) = product(X,eta(eta(X))),
inference(equational,[status(thm)],[c11,c47]) ).
cnf(c109,plain,
product(X,i(i(eta(X)))) = j(j(X)),
inference(equational,[status(thm)],[c1,c23,c29,c52,c58,c108]) ).
cnf(c110,plain,
i(i(eta(X))) = eta(X),
inference(equational,[status(thm)],[c18,c49,c109]) ).
cnf(c111,plain,
eta(eta(X)) = one,
inference(equational,[status(thm)],[c14,c53,c110]) ).
cnf(c112,plain,
j(eta(X)) = i(eta(X)),
inference(equational,[status(thm)],[c21,c28,c39,c110]) ).
cnf(c121,plain,
quotient(product(X,i(i(Y))),Y) = product(X,eta(Y)),
inference(equational,[status(thm)],[c18,c52,c58,c87]) ).
cnf(c122,plain,
product(product(X,eta(Y)),Y) = product(X,i(i(Y))),
inference(equational,[status(thm)],[c22,c121]) ).
cnf(c126,plain,
difference(X,product(product(X,Y),eta(Y))) = j(j(Y)),
inference(equational,[status(thm)],[c13,c47,c87]) ).
cnf(c143,plain,
product(j(j(X)),difference(eta(X),Y)) = product(X,Y),
inference(equational,[status(thm)],[c25,c47]) ).
cnf(c144,plain,
product(X,difference(eta(X),Y)) = product(i(i(X)),Y),
inference(equational,[status(thm)],[c24,c29,c51,c143]) ).
cnf(c149,plain,
difference(eta(X),product(i(i(X)),Y)) = product(X,Y),
inference(equational,[status(thm)],[c18,c51]) ).
cnf(c152,plain,
difference(eta(X),product(X,Y)) = product(j(j(X)),Y),
inference(equational,[status(thm)],[c27,c28,c47,c149]) ).
cnf(c168,plain,
difference(X,product(product(X,eta(Y)),Z)) = product(eta(Y),Z),
inference(equational,[status(thm)],[c13,c60,c87]) ).
cnf(c169,plain,
difference(i(eta(X)),Y) = product(eta(X),Y),
inference(equational,[status(thm)],[c2,c8,c111,c168]) ).
cnf(c170,plain,
quotient(X,product(eta(Y),X)) = i(eta(Y)),
inference(equational,[status(thm)],[c37,c169]) ).
cnf(c174,plain,
product(product(X,eta(Y)),Z) = product(X,product(eta(Y),Z)),
inference(equational,[status(thm)],[c25,c168]) ).
cnf(c177,plain,
quotient(difference(eta(X),Y),Y) = i(eta(X)),
inference(equational,[status(thm)],[c25,c170]) ).
cnf(c178,plain,
product(i(eta(X)),Y) = difference(eta(X),Y),
inference(equational,[status(thm)],[c22,c177]) ).
cnf(c193,axiom,
l(X,Y,Z) = difference(product(X,Y),product(X,product(Y,Z))),
file('theBenchmark.p',sos17) ).
cnf(c194,plain,
difference(product(X,Y),product(X,product(Y,Z))) = l(X,Y,Z),
inference(equational,[status(thm)],[c193]) ).
cnf(c200,plain,
difference(product(X,Y),X) = l(X,Y,i(Y)),
inference(equational,[status(thm)],[c1,c26,c194]) ).
cnf(c204,plain,
product(j(X),product(X,Y)) = l(j(X),X,Y),
inference(equational,[status(thm)],[c20,c23,c194]) ).
cnf(c207,plain,
product(X,product(i(X),Y)) = l(X,i(X),Y),
inference(equational,[status(thm)],[c20,c26,c194]) ).
cnf(c209,plain,
difference(product(X,j(Y)),X) = l(X,j(Y),Y),
inference(equational,[status(thm)],[c1,c23,c194]) ).
cnf(c224,plain,
difference(product(X,Y),product(X,Z)) = l(X,Y,difference(Y,Z)),
inference(equational,[status(thm)],[c25,c194]) ).
cnf(c238,plain,
product(product(X,Y),l(X,Y,Z)) = product(X,product(Y,Z)),
inference(equational,[status(thm)],[c25,c194]) ).
cnf(c239,plain,
l(i(eta(X)),eta(X),Y) = Y,
inference(equational,[status(thm)],[c18,c110,c178,c207]) ).
cnf(c252,plain,
product(eta(X),i(product(Y,eta(X)))) = i(Y),
inference(equational,[status(thm)],[c4,c26,c168]) ).
cnf(c253,plain,
difference(eta(X),i(Y)) = i(product(Y,eta(X))),
inference(equational,[status(thm)],[c112,c178,c204,c239,c252]) ).
cnf(c254,plain,
product(eta(X),i(Y)) = i(quotient(Y,eta(X))),
inference(equational,[status(thm)],[c22,c252]) ).
cnf(c285,plain,
difference(X,product(product(X,Y),j(X))) = quotient(Y,X),
inference(equational,[status(thm)],[c1,c23,c87]) ).
cnf(c289,plain,
product(eta(X),j(Y)) = quotient(eta(X),Y),
inference(equational,[status(thm)],[c18,c174,c285]) ).
cnf(c290,plain,
product(X,i(eta(Y))) = quotient(X,eta(Y)),
inference(equational,[status(thm)],[c18,c60,c112,c285]) ).
cnf(c292,plain,
l(eta(X),j(Y),Y) = Y,
inference(equational,[status(thm)],[c38,c209,c289]) ).
cnf(c308,plain,
l(eta(X),Y,i(Y)) = i(Y),
inference(equational,[status(thm)],[c27,c292]) ).
cnf(c328,plain,
l(j(j(X)),j(X),Y) = l(X,j(X),Y),
inference(equational,[status(thm)],[c11,c152,c194,c204]) ).
cnf(c329,plain,
l(j(X),X,Y) = l(i(X),X,Y),
inference(equational,[status(thm)],[c27,c328]) ).
cnf(c330,plain,
difference(X,quotient(X,Y)) = l(quotient(X,Y),Y,i(Y)),
inference(equational,[status(thm)],[c22,c200]) ).
cnf(c334,plain,
quotient(product(X,Y),difference(eta(X),Y)) = j(j(X)),
inference(equational,[status(thm)],[c13,c143]) ).
cnf(c348,plain,
difference(eta(X),quotient(eta(X),Y)) = j(Y),
inference(equational,[status(thm)],[c18,c289]) ).
cnf(c349,plain,
j(difference(X,eta(Y))) = difference(eta(Y),X),
inference(equational,[status(thm)],[c37,c348]) ).
cnf(c368,plain,
product(X,quotient(eta(X),Y)) = product(j(j(X)),j(Y)),
inference(equational,[status(thm)],[c47,c289]) ).
cnf(c369,plain,
difference(X,product(product(X,Y),i(X))) = quotient(product(Y,eta(X)),X),
inference(equational,[status(thm)],[c8,c87]) ).
cnf(c373,plain,
quotient(product(eta(X),eta(Y)),Y) = i(quotient(Y,eta(X))),
inference(equational,[status(thm)],[c168,c254,c369]) ).
cnf(c374,plain,
quotient(product(X,j(j(Y))),eta(Y)) = product(X,Y),
inference(equational,[status(thm)],[c18,c48,c60,c87]) ).
cnf(c375,plain,
quotient(product(X,Y),eta(Y)) = product(X,i(i(Y))),
inference(equational,[status(thm)],[c24,c29,c52,c122,c174,c374]) ).
cnf(c387,plain,
product(i(quotient(X,eta(Y))),X) = product(eta(Y),eta(X)),
inference(equational,[status(thm)],[c22,c373]) ).
cnf(c388,plain,
difference(quotient(X,eta(Y)),product(X,Z)) = product(eta(Y),Z),
inference(equational,[status(thm)],[c22,c168]) ).
cnf(c389,plain,
product(eta(X),difference(Y,Z)) = difference(quotient(Y,eta(X)),Z),
inference(equational,[status(thm)],[c25,c388]) ).
cnf(c392,plain,
product(eta(X),l(Y,eta(X),Z)) = product(eta(X),Z),
inference(equational,[status(thm)],[c18,c168,c238]) ).
cnf(c393,plain,
l(X,eta(Y),Z) = Z,
inference(equational,[status(thm)],[c18,c112,c178,c204,c239,c392]) ).
cnf(c410,plain,
l(X,Y,difference(Y,difference(X,Z))) = difference(product(X,Y),Z),
inference(equational,[status(thm)],[c25,c224]) ).
cnf(c411,plain,
difference(product(X,eta(Y)),Z) = difference(eta(Y),difference(X,Z)),
inference(equational,[status(thm)],[c393,c410]) ).
cnf(c440,plain,
product(eta(X),product(product(X,Y),Z)) = product(product(i(i(X)),Y),Z),
inference(equational,[status(thm)],[c51,c60]) ).
cnf(c441,plain,
l(eta(X),product(X,Y),Z) = Z,
inference(equational,[status(thm)],[c18,c51,c194,c440]) ).
cnf(c442,plain,
l(eta(X),Y,Z) = Z,
inference(equational,[status(thm)],[c25,c441]) ).
cnf(c444,plain,
difference(product(eta(X),Y),Z) = difference(Y,difference(eta(X),Z)),
inference(equational,[status(thm)],[c410,c442]) ).
cnf(c458,plain,
product(eta(X),product(difference(eta(X),Y),Z)) = product(Y,Z),
inference(equational,[status(thm)],[c25,c60]) ).
cnf(c459,plain,
product(difference(eta(X),Y),Z) = difference(eta(X),product(Y,Z)),
inference(equational,[status(thm)],[c18,c194,c393,c411,c458]) ).
cnf(c465,plain,
quotient(i(X),i(product(X,eta(Y)))) = eta(Y),
inference(equational,[status(thm)],[c20,c27,c111,c112,c252,c334]) ).
cnf(c466,plain,
i(i(product(X,eta(Y)))) = difference(i(X),eta(Y)),
inference(equational,[status(thm)],[c308,c330,c465]) ).
cnf(c497,plain,
difference(j(X),l(i(X),X,Y)) = product(X,Y),
inference(equational,[status(thm)],[c18,c204,c329]) ).
cnf(c526,plain,
product(i(i(X)),product(eta(X),Y)) = product(X,Y),
inference(equational,[status(thm)],[c18,c144]) ).
cnf(c537,plain,
product(difference(X,product(product(X,Y),Z)),X) = product(Y,product(Z,X)),
inference(equational,[status(thm)],[c22,c87]) ).
cnf(c539,plain,
product(product(X,Y),eta(Z)) = product(X,product(Y,eta(Z))),
inference(equational,[status(thm)],[c18,c60,c537]) ).
cnf(c540,plain,
l(X,Y,eta(Z)) = eta(Z),
inference(equational,[status(thm)],[c1,c27,c111,c112,c126,c194,c539]) ).
cnf(c542,plain,
difference(j(X),eta(Y)) = product(X,eta(Y)),
inference(equational,[status(thm)],[c497,c540]) ).
cnf(c545,plain,
product(X,quotient(Y,eta(Z))) = quotient(product(X,Y),eta(Z)),
inference(equational,[status(thm)],[c14,c20,c169,c178,c290,c389,c459,c537]) ).
cnf(c546,plain,
eta(quotient(X,eta(Y))) = t(eta(Y),eta(X)),
inference(equational,[status(thm)],[c8,c31,c387,c545]) ).
cnf(c550,plain,
product(X,product(i(product(Y,X)),Y)) = eta(Y),
inference(equational,[status(thm)],[c4,c8,c26,c537]) ).
cnf(c551,plain,
product(i(product(X,Y)),X) = difference(Y,eta(X)),
inference(equational,[status(thm)],[c18,c550]) ).
cnf(c554,plain,
quotient(difference(X,eta(Y)),Y) = i(product(Y,X)),
inference(equational,[status(thm)],[c13,c551]) ).
cnf(c555,plain,
eta(product(eta(X),Y)) = t(eta(X),eta(Y)),
inference(equational,[status(thm)],[c4,c28,c111,c546,c554]) ).
cnf(c565,plain,
product(difference(X,product(Y,Z)),X) = product(difference(X,Y),product(Z,X)),
inference(equational,[status(thm)],[c25,c537]) ).
cnf(c567,plain,
j(product(X,eta(Y))) = difference(eta(Y),j(X)),
inference(equational,[status(thm)],[c349,c542]) ).
cnf(c568,plain,
eta(product(X,eta(Y))) = eta(X),
inference(equational,[status(thm)],[c11,c14,c20,c174,c389,c567]) ).
cnf(c578,plain,
product(i(X),product(X,eta(Y))) = product(eta(X),eta(Y)),
inference(equational,[status(thm)],[c8,c539]) ).
cnf(c579,plain,
t(eta(X),eta(Y)) = eta(Y),
inference(equational,[status(thm)],[c25,c31,c375,c466,c568,c578]) ).
cnf(c612,plain,
product(difference(X,Y),product(i(Y),X)) = eta(X),
inference(equational,[status(thm)],[c4,c8,c26,c565]) ).
cnf(c615,plain,
quotient(eta(X),product(i(Y),X)) = difference(X,Y),
inference(equational,[status(thm)],[c13,c612]) ).
cnf(c616,plain,
quotient(eta(X),product(Y,X)) = difference(X,j(Y)),
inference(equational,[status(thm)],[c24,c48,c253,c444,c526,c555,c579,c615]) ).
cnf(g1,plain,
product(j(j(x0)),j(product(x1,x0))) = j(x1),
inference(equational,[status(thm)],[c25,c368,c616]) ).
cnf(g2,plain,
$false,
inference(resolution,[status(thm)],[g0,g1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP767-1 : TPTP v9.0.0. Released v4.1.0.
% 0.07/0.12 % Command : run_Leo-III %s %d THM
% 0.12/0.32 % Computer : n013.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Mon Jul 14 09:04:04 EDT 2025
% 0.12/0.32 % CPUTime :
% 62.06/62.11 % SZS status Unsatisfiable
% 62.06/62.11 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------