%------------------------------------------------------------------------------
% File : Toma---0.7
% Problem : GRP772-1 : TPTP v9.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_Leo-III %s %d THM
% Computer : n003.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 114.74s 114.57s
% Output : CNFRefutation 114.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 30
% Syntax : Number of clauses : 302 ( 302 unt; 0 nHn; 6 RR)
% Number of literals : 302 ( 301 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 3 con; 0-3 aty)
% Number of variables : 623 ( 20 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,negated_conjecture,
a(x0,x1,x1) != a(x1,x1,x0),
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(c9,plain,
i(one) = eta(one),
inference(equational,[status(thm)],[c1,c8]) ).
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(c12,plain,
j(one) = eta(one),
inference(equational,[status(thm)],[c2,c11]) ).
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(c15,plain,
eta(one) = one,
inference(equational,[status(thm)],[c6,c12,c14]) ).
cnf(c16,plain,
quotient(X,one) = X,
inference(equational,[status(thm)],[c1,c13]) ).
cnf(c17,plain,
quotient(eta(X),X) = i(X),
inference(equational,[status(thm)],[c8,c13]) ).
cnf(c18,axiom,
difference(X,product(X,Y)) = Y,
file('theBenchmark.p',sos04) ).
cnf(c19,plain,
difference(X,X) = one,
inference(equational,[status(thm)],[c1,c18]) ).
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(c35,plain,
t(X,j(X)) = i(X),
inference(equational,[status(thm)],[c11,c17,c31]) ).
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,axiom,
a(j(X),Y,Z) = a(Y,Z,X),
file('theBenchmark.p',sos32) ).
cnf(c40,plain,
difference(i(X),eta(X)) = X,
inference(equational,[status(thm)],[c8,c18]) ).
cnf(c43,axiom,
quotient(j(X),X) = product(j(X),i(X)),
file('theBenchmark.p',sos17) ).
cnf(c44,plain,
product(j(X),i(X)) = quotient(j(X),X),
inference(equational,[status(thm)],[c43]) ).
cnf(c45,axiom,
a(X,i(Y),Z) = a(X,j(Y),Z),
file('theBenchmark.p',sos30) ).
cnf(c46,plain,
a(X,j(Y),Z) = a(X,i(Y),Z),
inference(equational,[status(thm)],[c45]) ).
cnf(c47,axiom,
a(i(X),Y,Z) = a(j(X),Y,Z),
file('theBenchmark.p',sos31) ).
cnf(c48,plain,
a(i(X),Y,Z) = a(Y,Z,X),
inference(equational,[status(thm)],[c39,c47]) ).
cnf(c51,plain,
product(t(X,Y),X) = product(X,Y),
inference(equational,[status(thm)],[c22,c31]) ).
cnf(c52,plain,
t(i(X),X) = i(i(X)),
inference(equational,[status(thm)],[c27,c35]) ).
cnf(c53,plain,
quotient(eta(X),i(X)) = i(i(X)),
inference(equational,[status(thm)],[c8,c31,c52]) ).
cnf(c56,axiom,
product(i(i(X)),Y) = product(eta(X),product(X,Y)),
file('theBenchmark.p',sos13) ).
cnf(c57,plain,
product(eta(X),product(X,Y)) = product(i(i(X)),Y),
inference(equational,[status(thm)],[c56]) ).
cnf(c58,plain,
product(eta(X),X) = i(i(X)),
inference(equational,[status(thm)],[c1,c57]) ).
cnf(c59,plain,
quotient(i(i(X)),X) = eta(X),
inference(equational,[status(thm)],[c13,c58]) ).
cnf(c60,axiom,
product(X,product(eta(X),Y)) = product(j(j(X)),Y),
file('theBenchmark.p',sos14) ).
cnf(c61,plain,
product(X,eta(X)) = j(j(X)),
inference(equational,[status(thm)],[c1,c60]) ).
cnf(c62,plain,
difference(X,j(j(X))) = eta(X),
inference(equational,[status(thm)],[c18,c61]) ).
cnf(c63,plain,
quotient(j(j(X)),X) = t(X,eta(X)),
inference(equational,[status(thm)],[c31,c61]) ).
cnf(c65,plain,
quotient(i(X),j(X)) = eta(X),
inference(equational,[status(thm)],[c24,c29,c59]) ).
cnf(c66,axiom,
product(X,product(Y,eta(X))) = product(product(X,Y),eta(X)),
file('theBenchmark.p',sos15) ).
cnf(c67,plain,
product(product(X,Y),eta(X)) = product(X,product(Y,eta(X))),
inference(equational,[status(thm)],[c66]) ).
cnf(c68,axiom,
product(eta(X),product(Y,Z)) = product(product(eta(X),Y),Z),
file('theBenchmark.p',sos16) ).
cnf(c69,plain,
product(product(eta(X),Y),Z) = product(eta(X),product(Y,Z)),
inference(equational,[status(thm)],[c68]) ).
cnf(c71,plain,
quotient(j(j(X)),eta(X)) = X,
inference(equational,[status(thm)],[c13,c61]) ).
cnf(c72,plain,
quotient(j(X),eta(X)) = i(X),
inference(equational,[status(thm)],[c27,c28,c71]) ).
cnf(c73,plain,
quotient(X,eta(X)) = i(i(X)),
inference(equational,[status(thm)],[c27,c28,c72]) ).
cnf(c77,axiom,
product(product(X,Y),c(Y,X)) = product(Y,X),
file('theBenchmark.p',sos24) ).
cnf(c80,plain,
c(X,j(X)) = eta(X),
inference(equational,[status(thm)],[c2,c11,c23,c77]) ).
cnf(c86,plain,
a(X,Y,j(Z)) = a(Z,X,Y),
inference(equational,[status(thm)],[c24,c48]) ).
cnf(c87,plain,
a(X,Y,i(Z)) = a(Z,X,Y),
inference(equational,[status(thm)],[c27,c39]) ).
cnf(c88,plain,
difference(i(i(X)),eta(X)) = i(X),
inference(equational,[status(thm)],[c38,c53]) ).
cnf(c91,plain,
product(eta(X),c(j(X),X)) = one,
inference(equational,[status(thm)],[c11,c23,c77]) ).
cnf(c92,plain,
c(j(X),X) = i(eta(X)),
inference(equational,[status(thm)],[c4,c18,c91]) ).
cnf(c95,plain,
product(i(X),eta(X)) = j(X),
inference(equational,[status(thm)],[c27,c28,c61]) ).
cnf(c99,plain,
quotient(X,j(j(X))) = eta(X),
inference(equational,[status(thm)],[c24,c29,c65]) ).
cnf(c102,plain,
quotient(j(X),i(X)) = t(i(X),eta(X)),
inference(equational,[status(thm)],[c27,c28,c63]) ).
cnf(c105,plain,
difference(product(X,Y),product(Y,X)) = c(Y,X),
inference(equational,[status(thm)],[c18,c77]) ).
cnf(c107,plain,
quotient(product(X,Y),c(X,Y)) = product(Y,X),
inference(equational,[status(thm)],[c13,c77]) ).
cnf(c118,axiom,
product(i(product(X,Y)),i(i(X))) = i(Y),
file('theBenchmark.p',sos21) ).
cnf(c119,plain,
quotient(i(X),i(i(Y))) = i(product(Y,X)),
inference(equational,[status(thm)],[c13,c118]) ).
cnf(c120,plain,
product(i(X),i(i(Y))) = i(difference(Y,X)),
inference(equational,[status(thm)],[c25,c118]) ).
cnf(c121,plain,
i(difference(X,i(i(X)))) = eta(X),
inference(equational,[status(thm)],[c8,c28,c120]) ).
cnf(c122,plain,
difference(X,i(i(X))) = j(eta(X)),
inference(equational,[status(thm)],[c27,c121]) ).
cnf(c124,plain,
product(j(X),i(i(X))) = i(eta(X)),
inference(equational,[status(thm)],[c24,c61,c118]) ).
cnf(c125,plain,
product(i(X),i(Y)) = i(difference(j(Y),X)),
inference(equational,[status(thm)],[c24,c120]) ).
cnf(c126,plain,
product(X,i(i(Y))) = i(difference(Y,j(X))),
inference(equational,[status(thm)],[c24,c120]) ).
cnf(c127,plain,
i(product(X,j(Y))) = quotient(Y,i(i(X))),
inference(equational,[status(thm)],[c24,c119]) ).
cnf(c128,plain,
i(product(j(X),Y)) = quotient(i(Y),i(X)),
inference(equational,[status(thm)],[c24,c119]) ).
cnf(c129,plain,
i(i(eta(X))) = eta(X),
inference(equational,[status(thm)],[c28,c59,c124,c128]) ).
cnf(c130,plain,
eta(eta(X)) = one,
inference(equational,[status(thm)],[c9,c15,c19,c121,c129]) ).
cnf(c131,plain,
j(eta(X)) = i(eta(X)),
inference(equational,[status(thm)],[c21,c28,c40,c129]) ).
cnf(c132,plain,
t(i(X),eta(X)) = i(eta(X)),
inference(equational,[status(thm)],[c11,c24,c29,c102,c128]) ).
cnf(c133,plain,
t(X,eta(X)) = i(eta(X)),
inference(equational,[status(thm)],[c24,c29,c132]) ).
cnf(c135,plain,
product(X,i(eta(X))) = i(i(X)),
inference(equational,[status(thm)],[c25,c122,c131]) ).
cnf(c137,plain,
difference(i(product(X,Y)),i(Y)) = i(i(X)),
inference(equational,[status(thm)],[c18,c118]) ).
cnf(c139,plain,
i(i(quotient(X,Y))) = difference(i(X),i(Y)),
inference(equational,[status(thm)],[c22,c137]) ).
cnf(c147,axiom,
product(c(X,Y),product(Z,W)) = product(product(c(X,Y),Z),W),
file('theBenchmark.p',sos25) ).
cnf(c148,plain,
product(product(c(X,Y),Z),W) = product(c(X,Y),product(Z,W)),
inference(equational,[status(thm)],[c147]) ).
cnf(c150,axiom,
difference(X,product(product(X,Y),Z)) = quotient(product(Y,product(Z,X)),X),
file('theBenchmark.p',sos07) ).
cnf(c151,plain,
quotient(product(X,product(Y,Z)),Z) = difference(Z,product(product(Z,X),Y)),
inference(equational,[status(thm)],[c150]) ).
cnf(c152,axiom,
product(j(j(X)),j(product(Y,X))) = j(Y),
file('theBenchmark.p',sos22) ).
cnf(c153,plain,
difference(j(j(X)),j(Y)) = j(product(Y,X)),
inference(equational,[status(thm)],[c18,c152]) ).
cnf(c154,plain,
product(j(j(X)),j(Y)) = j(quotient(Y,X)),
inference(equational,[status(thm)],[c22,c152]) ).
cnf(c155,plain,
product(X,j(product(Y,X))) = product(eta(X),j(Y)),
inference(equational,[status(thm)],[c24,c29,c57,c152]) ).
cnf(c156,plain,
product(eta(X),j(j(X))) = X,
inference(equational,[status(thm)],[c1,c12,c15,c23,c155]) ).
cnf(c157,plain,
j(quotient(j(X),X)) = product(X,X),
inference(equational,[status(thm)],[c60,c154,c156]) ).
cnf(c162,plain,
product(j(j(X)),i(eta(X))) = X,
inference(equational,[status(thm)],[c8,c27,c131,c152]) ).
cnf(c164,plain,
quotient(X,i(eta(X))) = j(j(X)),
inference(equational,[status(thm)],[c13,c162]) ).
cnf(c166,plain,
product(j(j(X)),Y) = j(quotient(i(Y),X)),
inference(equational,[status(thm)],[c27,c154]) ).
cnf(c168,plain,
j(product(i(X),Y)) = difference(j(j(Y)),X),
inference(equational,[status(thm)],[c27,c153]) ).
cnf(c169,plain,
j(product(X,i(Y))) = difference(j(Y),j(X)),
inference(equational,[status(thm)],[c27,c153]) ).
cnf(c172,plain,
quotient(j(X),j(product(X,Y))) = j(j(Y)),
inference(equational,[status(thm)],[c13,c152]) ).
cnf(c173,plain,
j(j(difference(X,Y))) = quotient(j(X),j(Y)),
inference(equational,[status(thm)],[c25,c172]) ).
cnf(c182,axiom,
product(product(X,Y),c(Z,W)) = product(X,product(Y,c(Z,W))),
file('theBenchmark.p',sos26) ).
cnf(c186,plain,
product(i(i(X)),difference(X,Y)) = product(eta(X),Y),
inference(equational,[status(thm)],[c25,c57]) ).
cnf(c187,plain,
product(i(i(X)),eta(X)) = X,
inference(equational,[status(thm)],[c62,c156,c186]) ).
cnf(c188,plain,
difference(X,j(quotient(i(Y),X))) = product(eta(X),Y),
inference(equational,[status(thm)],[c18,c60,c166]) ).
cnf(c190,plain,
difference(X,product(product(X,X),Y)) = t(X,product(Y,X)),
inference(equational,[status(thm)],[c31,c151]) ).
cnf(c192,plain,
product(X,c(Y,quotient(X,Y))) = product(Y,quotient(X,Y)),
inference(equational,[status(thm)],[c22,c77]) ).
cnf(c197,plain,
j(product(X,eta(Y))) = difference(eta(Y),j(X)),
inference(equational,[status(thm)],[c27,c121,c122,c131,c169]) ).
cnf(c198,plain,
quotient(j(j(X)),product(X,X)) = j(X),
inference(equational,[status(thm)],[c27,c44,c157,c172]) ).
cnf(c199,plain,
product(j(X),product(X,X)) = j(j(X)),
inference(equational,[status(thm)],[c22,c198]) ).
cnf(c200,plain,
product(i(X),product(X,X)) = X,
inference(equational,[status(thm)],[c24,c29,c57,c156,c199]) ).
cnf(c201,plain,
quotient(X,product(X,X)) = i(X),
inference(equational,[status(thm)],[c13,c200]) ).
cnf(c203,plain,
a(X,i(i(Y)),Z) = a(X,Y,Z),
inference(equational,[status(thm)],[c27,c46]) ).
cnf(c219,plain,
j(difference(i(X),i(Y))) = i(quotient(X,Y)),
inference(equational,[status(thm)],[c27,c139]) ).
cnf(c220,plain,
j(difference(X,i(Y))) = i(quotient(j(X),Y)),
inference(equational,[status(thm)],[c24,c219]) ).
cnf(c221,plain,
j(difference(i(X),Y)) = i(quotient(X,j(Y))),
inference(equational,[status(thm)],[c24,c219]) ).
cnf(c223,plain,
quotient(j(quotient(X,Y)),j(X)) = j(j(Y)),
inference(equational,[status(thm)],[c22,c172]) ).
cnf(c225,plain,
difference(i(X),i(difference(Y,X))) = i(i(Y)),
inference(equational,[status(thm)],[c18,c120]) ).
cnf(c236,plain,
quotient(j(quotient(i(X),Y)),Y) = t(Y,product(eta(Y),X)),
inference(equational,[status(thm)],[c31,c60,c166]) ).
cnf(c238,plain,
product(eta(quotient(X,Y)),X) = product(difference(i(X),i(Y)),Y),
inference(equational,[status(thm)],[c22,c57,c139]) ).
cnf(c245,plain,
difference(i(eta(X)),j(j(X))) = X,
inference(equational,[status(thm)],[c2,c27,c28,c130,c164,c188]) ).
cnf(c246,plain,
difference(i(i(X)),product(X,Y)) = product(eta(X),Y),
inference(equational,[status(thm)],[c27,c28,c119,c188]) ).
cnf(c249,plain,
product(eta(X),j(quotient(Y,X))) = product(X,j(Y)),
inference(equational,[status(thm)],[c22,c155]) ).
cnf(c255,plain,
difference(X,product(eta(X),j(Y))) = j(product(Y,X)),
inference(equational,[status(thm)],[c18,c155]) ).
cnf(c256,plain,
difference(X,product(eta(X),Y)) = difference(j(j(X)),Y),
inference(equational,[status(thm)],[c27,c168,c255]) ).
cnf(c257,plain,
j(quotient(product(X,eta(Y)),Y)) = product(Y,j(X)),
inference(equational,[status(thm)],[c2,c60,c130,c154,c155]) ).
cnf(c258,plain,
quotient(product(X,eta(Y)),Y) = quotient(X,i(i(Y))),
inference(equational,[status(thm)],[c24,c127,c257]) ).
cnf(c263,plain,
quotient(i(difference(X,j(Y))),X) = product(Y,eta(X)),
inference(equational,[status(thm)],[c18,c58,c67,c126,c151]) ).
cnf(c264,plain,
product(product(X,eta(Y)),Y) = i(difference(Y,j(X))),
inference(equational,[status(thm)],[c22,c263]) ).
cnf(c265,plain,
quotient(i(difference(X,Y)),X) = product(i(Y),eta(X)),
inference(equational,[status(thm)],[c27,c263]) ).
cnf(c277,plain,
difference(X,product(Y,quotient(X,Y))) = c(Y,quotient(X,Y)),
inference(equational,[status(thm)],[c18,c192]) ).
cnf(c281,plain,
c(product(X,X),i(X)) = i(eta(X)),
inference(equational,[status(thm)],[c8,c133,c190,c201,c277]) ).
cnf(c283,plain,
product(product(X,X),i(X)) = i(i(X)),
inference(equational,[status(thm)],[c77,c135,c200,c281]) ).
cnf(c284,plain,
i(i(c(X,Y))) = c(X,Y),
inference(equational,[status(thm)],[c1,c26,c148,c283]) ).
cnf(c285,plain,
eta(c(X,Y)) = one,
inference(equational,[status(thm)],[c9,c15,c19,c121,c284]) ).
cnf(c286,plain,
j(c(X,Y)) = i(c(X,Y)),
inference(equational,[status(thm)],[c21,c28,c40,c284]) ).
cnf(c291,plain,
difference(X,i(difference(Y,j(X)))) = i(i(Y)),
inference(equational,[status(thm)],[c13,c57,c151,c264]) ).
cnf(c299,plain,
eta(quotient(X,j(Y))) = eta(difference(i(X),Y)),
inference(equational,[status(thm)],[c28,c29,c221]) ).
cnf(c301,plain,
i(product(eta(X),Y)) = quotient(i(Y),eta(X)),
inference(equational,[status(thm)],[c119,c129]) ).
cnf(c302,plain,
product(i(X),eta(Y)) = i(difference(eta(Y),X)),
inference(equational,[status(thm)],[c120,c129]) ).
cnf(c303,plain,
eta(quotient(j(X),Y)) = eta(difference(X,i(Y))),
inference(equational,[status(thm)],[c28,c29,c220]) ).
cnf(c307,plain,
product(X,product(i(i(X)),Y)) = j(quotient(i(product(X,Y)),X)),
inference(equational,[status(thm)],[c57,c60,c166]) ).
cnf(c321,plain,
j(quotient(i(difference(eta(X),Y)),X)) = product(X,Y),
inference(equational,[status(thm)],[c25,c60,c166]) ).
cnf(c322,plain,
product(X,difference(eta(X),Y)) = product(i(i(X)),Y),
inference(equational,[status(thm)],[c27,c28,c119,c321]) ).
cnf(c323,plain,
difference(eta(X),product(i(i(X)),Y)) = product(X,Y),
inference(equational,[status(thm)],[c18,c57]) ).
cnf(c324,plain,
difference(eta(X),product(X,Y)) = j(quotient(i(Y),X)),
inference(equational,[status(thm)],[c27,c28,c60,c166,c323]) ).
cnf(c326,plain,
product(X,difference(i(i(X)),Y)) = difference(eta(X),Y),
inference(equational,[status(thm)],[c25,c323]) ).
cnf(c331,plain,
j(quotient(quotient(i(X),Y),Y)) = product(Y,product(Y,X)),
inference(equational,[status(thm)],[c24,c27,c28,c60,c166,c307]) ).
cnf(c332,plain,
j(quotient(X,i(i(Y)))) = product(Y,j(X)),
inference(equational,[status(thm)],[c25,c258,c263,c331]) ).
cnf(c334,plain,
product(eta(X),j(Y)) = j(quotient(Y,eta(X))),
inference(equational,[status(thm)],[c129,c332]) ).
cnf(c344,plain,
eta(difference(i(X),i(Y))) = eta(quotient(X,Y)),
inference(equational,[status(thm)],[c28,c139]) ).
cnf(c354,plain,
product(eta(X),product(i(eta(X)),Y)) = Y,
inference(equational,[status(thm)],[c2,c26,c69]) ).
cnf(c355,plain,
product(i(eta(X)),Y) = difference(eta(X),Y),
inference(equational,[status(thm)],[c2,c129,c130,c246,c354]) ).
cnf(c356,plain,
difference(i(eta(X)),Y) = product(eta(X),Y),
inference(equational,[status(thm)],[c20,c28,c129,c130,c326,c354]) ).
cnf(c358,plain,
difference(X,quotient(X,eta(Y))) = i(eta(Y)),
inference(equational,[status(thm)],[c24,c129,c291,c334,c356]) ).
cnf(c359,plain,
product(X,i(eta(Y))) = quotient(X,eta(Y)),
inference(equational,[status(thm)],[c25,c358]) ).
cnf(c367,plain,
difference(X,product(product(X,eta(Y)),Z)) = product(eta(Y),Z),
inference(equational,[status(thm)],[c13,c69,c151]) ).
cnf(c368,plain,
product(product(X,eta(Y)),Z) = product(X,product(eta(Y),Z)),
inference(equational,[status(thm)],[c25,c367]) ).
cnf(c369,plain,
eta(product(X,eta(Y))) = eta(X),
inference(equational,[status(thm)],[c11,c25,c197,c368]) ).
cnf(c370,plain,
eta(quotient(X,eta(Y))) = eta(X),
inference(equational,[status(thm)],[c22,c369]) ).
cnf(c372,plain,
eta(t(eta(X),Y)) = eta(Y),
inference(equational,[status(thm)],[c2,c28,c29,c130,c236,c370]) ).
cnf(c373,plain,
eta(product(eta(X),Y)) = eta(Y),
inference(equational,[status(thm)],[c51,c369,c372]) ).
cnf(c375,plain,
eta(product(X,j(Y))) = eta(quotient(Y,X)),
inference(equational,[status(thm)],[c29,c249,c373]) ).
cnf(c376,plain,
eta(quotient(eta(X),Y)) = eta(Y),
inference(equational,[status(thm)],[c131,c359,c370,c375]) ).
cnf(c377,plain,
quotient(i(eta(X)),Y) = difference(eta(X),j(Y)),
inference(equational,[status(thm)],[c24,c95,c197,c302,c324,c369]) ).
cnf(c384,plain,
quotient(j(quotient(i(X),Y)),X) = j(j(Y)),
inference(equational,[status(thm)],[c27,c223]) ).
cnf(c388,plain,
quotient(product(X,Y),eta(Y)) = i(difference(Y,j(X))),
inference(equational,[status(thm)],[c18,c69,c126,c151,c187]) ).
cnf(c389,plain,
eta(difference(X,j(Y))) = eta(product(Y,X)),
inference(equational,[status(thm)],[c28,c370,c388]) ).
cnf(c395,plain,
eta(quotient(i(X),Y)) = eta(product(Y,X)),
inference(equational,[status(thm)],[c27,c375]) ).
cnf(c396,plain,
eta(difference(X,i(Y))) = eta(product(Y,X)),
inference(equational,[status(thm)],[c29,c153,c303,c375,c389]) ).
cnf(c397,plain,
eta(product(i(X),Y)) = eta(difference(Y,X)),
inference(equational,[status(thm)],[c27,c389]) ).
cnf(c402,axiom,
product(a(X,Y,Z),product(W,V)) = product(product(a(X,Y,Z),W),V),
file('theBenchmark.p',sos27) ).
cnf(c403,plain,
product(product(a(X,Y,Z),W),V) = product(a(X,Y,Z),product(W,V)),
inference(equational,[status(thm)],[c402]) ).
cnf(c404,axiom,
product(product(X,Y),a(Z,W,V)) = product(X,product(Y,a(Z,W,V))),
file('theBenchmark.p',sos28) ).
cnf(c412,plain,
product(difference(X,Y),j(Y)) = j(quotient(X,eta(difference(X,Y)))),
inference(equational,[status(thm)],[c25,c155,c334]) ).
cnf(c413,plain,
j(quotient(i(X),eta(Y))) = product(eta(Y),X),
inference(equational,[status(thm)],[c27,c28,c186,c225,c412]) ).
cnf(c414,plain,
quotient(i(X),eta(Y)) = difference(X,i(eta(Y))),
inference(equational,[status(thm)],[c27,c131,c245,c334,c356,c373,c388,c395,c413]) ).
cnf(c415,plain,
difference(product(X,eta(Y)),X) = i(eta(Y)),
inference(equational,[status(thm)],[c13,c358]) ).
cnf(c416,plain,
quotient(X,i(eta(Y))) = product(X,eta(Y)),
inference(equational,[status(thm)],[c37,c415]) ).
cnf(c417,plain,
i(difference(eta(X),Y)) = difference(Y,eta(X)),
inference(equational,[status(thm)],[c27,c128,c129,c291,c377,c415]) ).
cnf(c426,plain,
eta(quotient(X,i(i(Y)))) = eta(quotient(X,Y)),
inference(equational,[status(thm)],[c28,c127,c375]) ).
cnf(c429,plain,
eta(quotient(X,i(Y))) = eta(difference(i(X),Y)),
inference(equational,[status(thm)],[c24,c299,c426]) ).
cnf(c430,plain,
eta(product(X,i(Y))) = eta(quotient(Y,X)),
inference(equational,[status(thm)],[c24,c389,c429]) ).
cnf(c436,plain,
eta(difference(j(j(X)),Y)) = eta(difference(X,Y)),
inference(equational,[status(thm)],[c29,c168,c397]) ).
cnf(c437,plain,
eta(difference(j(X),Y)) = eta(difference(i(X),Y)),
inference(equational,[status(thm)],[c27,c436]) ).
cnf(c439,plain,
product(eta(X),i(product(Y,eta(X)))) = i(Y),
inference(equational,[status(thm)],[c4,c26,c367]) ).
cnf(c440,plain,
i(product(X,eta(Y))) = difference(eta(Y),i(X)),
inference(equational,[status(thm)],[c2,c129,c130,c246,c439]) ).
cnf(c441,plain,
product(eta(X),i(Y)) = i(quotient(Y,eta(X))),
inference(equational,[status(thm)],[c22,c439]) ).
cnf(c442,plain,
i(quotient(j(X),eta(Y))) = product(eta(Y),X),
inference(equational,[status(thm)],[c24,c441]) ).
cnf(c443,plain,
j(product(eta(X),Y)) = quotient(j(Y),eta(X)),
inference(equational,[status(thm)],[c27,c442]) ).
cnf(c444,plain,
difference(j(X),i(eta(Y))) = quotient(X,eta(Y)),
inference(equational,[status(thm)],[c27,c131,c169,c441]) ).
cnf(c448,plain,
i(quotient(eta(X),Y)) = quotient(Y,eta(X)),
inference(equational,[status(thm)],[c131,c169,c219,c356,c444]) ).
cnf(c449,plain,
j(quotient(X,eta(Y))) = quotient(eta(Y),X),
inference(equational,[status(thm)],[c27,c448]) ).
cnf(c457,plain,
product(X,quotient(eta(X),Y)) = j(quotient(Y,X)),
inference(equational,[status(thm)],[c22,c257,c449]) ).
cnf(c459,plain,
quotient(product(X,Y),j(j(Y))) = product(X,eta(Y)),
inference(equational,[status(thm)],[c24,c29,c153,c263]) ).
cnf(c460,plain,
product(quotient(X,Y),eta(Y)) = quotient(X,j(j(Y))),
inference(equational,[status(thm)],[c22,c459]) ).
cnf(c466,plain,
difference(X,product(i(i(X)),Y)) = difference(eta(X),Y),
inference(equational,[status(thm)],[c18,c322]) ).
cnf(c467,plain,
quotient(difference(X,eta(Y)),Y) = i(product(Y,X)),
inference(equational,[status(thm)],[c265,c302,c323,c417,c466]) ).
cnf(c478,plain,
product(j(X),product(X,c(Y,Z))) = c(Y,Z),
inference(equational,[status(thm)],[c2,c23,c182]) ).
cnf(c484,plain,
difference(X,product(product(X,Y),j(X))) = quotient(Y,X),
inference(equational,[status(thm)],[c1,c23,c151]) ).
cnf(c486,plain,
product(X,i(c(Y,Z))) = quotient(X,c(Y,Z)),
inference(equational,[status(thm)],[c18,c148,c286,c484]) ).
cnf(c487,plain,
difference(X,product(Y,j(X))) = quotient(difference(X,Y),X),
inference(equational,[status(thm)],[c25,c484]) ).
cnf(c497,plain,
difference(quotient(X,eta(Y)),product(X,Y)) = i(i(Y)),
inference(equational,[status(thm)],[c24,c127,c129,c137,c155]) ).
cnf(c508,plain,
difference(eta(X),quotient(eta(X),Y)) = j(Y),
inference(equational,[status(thm)],[c18,c28,c332,c457,c466]) ).
cnf(c512,plain,
i(i(a(X,Y,Z))) = a(X,Y,Z),
inference(equational,[status(thm)],[c1,c26,c283,c403]) ).
cnf(c513,plain,
eta(a(X,Y,Z)) = one,
inference(equational,[status(thm)],[c9,c15,c19,c121,c512]) ).
cnf(c514,plain,
j(a(X,Y,Z)) = i(a(X,Y,Z)),
inference(equational,[status(thm)],[c21,c88,c512]) ).
cnf(c521,plain,
difference(difference(X,i(Y)),j(X)) = product(eta(product(Y,X)),Y),
inference(equational,[status(thm)],[c37,c188,c396]) ).
cnf(c537,plain,
difference(i(i(X)),product(eta(X),Y)) = difference(X,Y),
inference(equational,[status(thm)],[c18,c186]) ).
cnf(c541,plain,
difference(X,product(product(X,Y),i(X))) = quotient(Y,i(i(X))),
inference(equational,[status(thm)],[c8,c151,c258]) ).
cnf(c550,plain,
quotient(product(X,j(j(Y))),eta(Y)) = product(X,Y),
inference(equational,[status(thm)],[c18,c61,c69,c151]) ).
cnf(c553,plain,
quotient(product(X,j(Y)),eta(Y)) = product(X,i(Y)),
inference(equational,[status(thm)],[c27,c28,c550]) ).
cnf(c562,plain,
difference(eta(X),i(eta(Y))) = difference(eta(Y),i(eta(X))),
inference(equational,[status(thm)],[c8,c69,c238,c301,c356,c376,c414,c440]) ).
cnf(c565,plain,
product(eta(X),eta(Y)) = product(eta(Y),eta(X)),
inference(equational,[status(thm)],[c131,c220,c356,c414,c417,c562]) ).
cnf(c566,plain,
quotient(eta(X),eta(Y)) = difference(eta(Y),eta(X)),
inference(equational,[status(thm)],[c1,c9,c14,c15,c69,c129,c441,c541,c565]) ).
cnf(c570,plain,
quotient(product(i(i(X)),Y),product(X,Y)) = eta(X),
inference(equational,[status(thm)],[c13,c57]) ).
cnf(c586,plain,
difference(quotient(X,eta(Y)),product(X,Z)) = product(eta(Y),Z),
inference(equational,[status(thm)],[c22,c367]) ).
cnf(c587,plain,
product(eta(X),difference(Y,Z)) = difference(quotient(Y,eta(X)),Z),
inference(equational,[status(thm)],[c25,c586]) ).
cnf(c650,plain,
difference(X,quotient(X,c(Y,Z))) = i(c(Y,Z)),
inference(equational,[status(thm)],[c16,c28,c284,c285,c486,c497]) ).
cnf(c651,plain,
i(c(X,Y)) = c(Y,X),
inference(equational,[status(thm)],[c105,c107,c650]) ).
cnf(c653,plain,
product(X,c(Y,Z)) = quotient(X,c(Z,Y)),
inference(equational,[status(thm)],[c486,c651]) ).
cnf(c699,plain,
difference(eta(quotient(X,Y)),X) = j(quotient(i(Y),quotient(X,Y))),
inference(equational,[status(thm)],[c22,c324]) ).
cnf(c791,plain,
product(j(quotient(X,c(Y,Z))),X) = c(Y,Z),
inference(equational,[status(thm)],[c22,c478]) ).
cnf(c792,plain,
j(quotient(X,c(Y,Z))) = quotient(c(Y,Z),X),
inference(equational,[status(thm)],[c13,c791]) ).
cnf(c794,plain,
difference(c(X,Y),j(Z)) = quotient(c(Y,X),Z),
inference(equational,[status(thm)],[c2,c24,c285,c521,c650,c651,c791,c792]) ).
cnf(c796,plain,
quotient(c(X,Y),i(Z)) = difference(c(Y,X),Z),
inference(equational,[status(thm)],[c27,c794]) ).
cnf(c798,plain,
product(c(X,Y),Z) = difference(c(Y,X),Z),
inference(equational,[status(thm)],[c4,c27,c285,c467,c792,c796]) ).
cnf(c801,plain,
product(j(product(X,Y)),product(Y,X)) = c(Y,X),
inference(equational,[status(thm)],[c77,c478]) ).
cnf(c802,plain,
quotient(c(X,Y),product(X,Y)) = j(product(Y,X)),
inference(equational,[status(thm)],[c13,c801]) ).
cnf(c844,plain,
quotient(i(X),quotient(j(Y),eta(X))) = quotient(j(X),j(Y)),
inference(equational,[status(thm)],[c27,c172,c173,c186,c443]) ).
cnf(c845,plain,
quotient(i(X),quotient(Y,eta(X))) = quotient(j(X),Y),
inference(equational,[status(thm)],[c27,c844]) ).
cnf(c904,plain,
product(quotient(X,Y),quotient(Y,c(Z,W))) = quotient(X,c(Z,W)),
inference(equational,[status(thm)],[c22,c182,c653]) ).
cnf(c906,plain,
product(X,quotient(Y,c(Z,W))) = quotient(product(X,Y),c(Z,W)),
inference(equational,[status(thm)],[c13,c904]) ).
cnf(c913,plain,
product(difference(X,product(product(X,Y),Z)),X) = product(Y,product(Z,X)),
inference(equational,[status(thm)],[c22,c151]) ).
cnf(c914,plain,
product(i(X),product(Y,X)) = product(difference(X,Y),X),
inference(equational,[status(thm)],[c2,c26,c913]) ).
cnf(c915,plain,
product(difference(X,quotient(Y,X)),X) = product(i(X),Y),
inference(equational,[status(thm)],[c22,c914]) ).
cnf(c920,plain,
product(difference(X,product(Y,Z)),X) = product(difference(X,Y),product(Z,X)),
inference(equational,[status(thm)],[c25,c913]) ).
cnf(c928,plain,
difference(i(X),product(difference(X,Y),X)) = product(Y,X),
inference(equational,[status(thm)],[c18,c914]) ).
cnf(c930,plain,
product(product(X,Y),i(Y)) = difference(i(Y),difference(Y,X)),
inference(equational,[status(thm)],[c1,c26,c920,c928]) ).
cnf(c931,plain,
product(product(X,j(Y)),Y) = difference(i(Y),difference(Y,X)),
inference(equational,[status(thm)],[c22,c487,c928]) ).
cnf(c935,plain,
difference(i(X),difference(X,Y)) = difference(X,difference(j(X),Y)),
inference(equational,[status(thm)],[c24,c930,c931]) ).
cnf(c963,plain,
quotient(difference(c(X,Y),product(Z,W)),W) = difference(c(X,Y),Z),
inference(equational,[status(thm)],[c13,c148,c798]) ).
cnf(c965,plain,
quotient(difference(c(X,Y),Z),W) = difference(c(X,Y),quotient(Z,W)),
inference(equational,[status(thm)],[c22,c963]) ).
cnf(c966,plain,
quotient(difference(eta(X),Y),Z) = difference(eta(X),quotient(Y,Z)),
inference(equational,[status(thm)],[c80,c965]) ).
cnf(c971,plain,
quotient(product(X,j(Y)),j(quotient(Y,X))) = eta(X),
inference(equational,[status(thm)],[c24,c29,c154,c570]) ).
cnf(c972,plain,
eta(product(X,Y)) = eta(product(Y,X)),
inference(equational,[status(thm)],[c99,c107,c182,c286,c651,c653,c802,c906,c971]) ).
cnf(c974,plain,
eta(quotient(X,Y)) = eta(difference(Y,X)),
inference(equational,[status(thm)],[c28,c120,c125,c344,c437,c972]) ).
cnf(c975,plain,
eta(difference(X,Y)) = eta(difference(Y,X)),
inference(equational,[status(thm)],[c25,c397,c915,c972,c974]) ).
cnf(c982,plain,
eta(difference(X,quotient(X,Y))) = eta(Y),
inference(equational,[status(thm)],[c38,c975]) ).
cnf(c1005,plain,
difference(eta(difference(X,Y)),Y) = j(quotient(i(X),quotient(Y,X))),
inference(equational,[status(thm)],[c699,c974]) ).
cnf(c1056,plain,
product(quotient(X,Y),product(Y,eta(Z))) = product(X,eta(Z)),
inference(equational,[status(thm)],[c92,c416,c904]) ).
cnf(c1057,plain,
product(quotient(X,Y),j(j(Y))) = product(X,eta(Y)),
inference(equational,[status(thm)],[c61,c1056]) ).
cnf(c1224,plain,
product(product(X,a(Y,Z,W)),V) = product(X,product(a(Y,Z,W),V)),
inference(equational,[status(thm)],[c18,c404,c913]) ).
cnf(c1225,plain,
eta(product(X,a(Y,Z,W))) = eta(X),
inference(equational,[status(thm)],[c2,c11,c155,c513,c1224]) ).
cnf(c1227,plain,
eta(difference(a(X,Y,Z),W)) = eta(W),
inference(equational,[status(thm)],[c22,c974,c1225]) ).
cnf(c1228,plain,
product(a(X,Y,Z),j(W)) = quotient(a(X,Y,Z),W),
inference(equational,[status(thm)],[c18,c484,c1224]) ).
cnf(c1232,plain,
quotient(a(X,Y,Z),i(W)) = product(a(X,Y,Z),W),
inference(equational,[status(thm)],[c27,c1228]) ).
cnf(c1233,plain,
eta(difference(X,a(Y,Z,W))) = eta(X),
inference(equational,[status(thm)],[c426,c430,c974,c1227,c1232]) ).
cnf(c1290,axiom,
product(product(X,product(Y,Z)),a(X,Y,Z)) = product(product(X,Y),Z),
file('theBenchmark.p',sos23) ).
cnf(c1291,plain,
product(X,product(Y,product(Z,a(X,Y,Z)))) = product(product(X,Y),Z),
inference(equational,[status(thm)],[c404,c1290]) ).
cnf(c1304,plain,
difference(X,product(product(X,Y),Z)) = product(Y,product(Z,a(X,Y,Z))),
inference(equational,[status(thm)],[c18,c1291]) ).
cnf(c1352,plain,
product(X,product(i(X),a(Y,Z,W))) = a(Y,Z,W),
inference(equational,[status(thm)],[c2,c26,c404]) ).
cnf(c1355,plain,
product(i(X),a(Y,Z,W)) = difference(X,a(Y,Z,W)),
inference(equational,[status(thm)],[c18,c1352]) ).
cnf(c1371,plain,
difference(j(X),a(Y,Z,W)) = product(X,a(Y,Z,W)),
inference(equational,[status(thm)],[c24,c1355]) ).
cnf(c1373,plain,
j(difference(X,a(Y,Z,W))) = difference(a(Y,Z,W),X),
inference(equational,[status(thm)],[c27,c168,c514,c1355]) ).
cnf(c1410,axiom,
difference(product(X,Y),product(X,product(Y,Z))) = quotient(quotient(product(Z,product(X,Y)),Y),X),
file('theBenchmark.p',sos08) ).
cnf(c1411,plain,
quotient(difference(X,product(product(X,Y),Z)),Z) = difference(product(Z,X),product(Z,product(X,Y))),
inference(equational,[status(thm)],[c151,c1410]) ).
cnf(c1412,plain,
quotient(difference(X,Y),Y) = difference(product(Y,X),Y),
inference(equational,[status(thm)],[c1,c2,c26,c1411]) ).
cnf(c1415,plain,
product(difference(product(X,Y),X),X) = difference(Y,X),
inference(equational,[status(thm)],[c22,c1412]) ).
cnf(c1416,plain,
product(difference(X,Y),Y) = difference(difference(Y,X),Y),
inference(equational,[status(thm)],[c25,c1415]) ).
cnf(c1425,plain,
difference(product(X,Y),product(X,eta(Y))) = difference(product(X,j(j(Y))),X),
inference(equational,[status(thm)],[c11,c256,c1411,c1412]) ).
cnf(c1430,plain,
difference(product(X,eta(Y)),product(X,Y)) = j(j(Y)),
inference(equational,[status(thm)],[c27,c72,c156,c324,c334,c384,c1411]) ).
cnf(c1437,plain,
difference(difference(X,quotient(X,Y)),X) = product(Y,X),
inference(equational,[status(thm)],[c38,c1416]) ).
cnf(c1438,plain,
quotient(X,product(Y,X)) = difference(X,quotient(X,Y)),
inference(equational,[status(thm)],[c37,c1437]) ).
cnf(c1449,plain,
difference(product(X,eta(Y)),product(X,Z)) = difference(eta(Y),Z),
inference(equational,[status(thm)],[c13,c19,c20,c354,c355,c566,c587,c966,c1411]) ).
cnf(c1450,plain,
difference(product(X,eta(Y)),Z) = difference(eta(Y),difference(X,Z)),
inference(equational,[status(thm)],[c25,c1449]) ).
cnf(c1458,plain,
difference(eta(X),difference(Y,quotient(Y,X))) = difference(Y,quotient(Y,j(j(X)))),
inference(equational,[status(thm)],[c22,c460,c1057,c1425,c1450]) ).
cnf(c1477,plain,
product(j(X),a(Y,Z,W)) = j(difference(a(Y,Z,W),X)),
inference(equational,[status(thm)],[c61,c1233,c1352,c1355,c1371,c1373,c1430]) ).
cnf(c1661,plain,
product(X,j(difference(a(Y,Z,W),X))) = product(eta(X),a(Y,Z,W)),
inference(equational,[status(thm)],[c11,c404,c1477]) ).
cnf(c1667,plain,
i(difference(a(X,Y,Z),W)) = difference(W,a(X,Y,Z)),
inference(equational,[status(thm)],[c24,c29,c73,c497,c537,c1227,c1661]) ).
cnf(c1676,plain,
product(i(X),product(X,a(Y,Z,W))) = product(eta(X),a(Y,Z,W)),
inference(equational,[status(thm)],[c8,c404]) ).
cnf(c1690,plain,
j(quotient(i(a(X,Y,Z)),W)) = j(difference(a(X,Y,Z),j(W))),
inference(equational,[status(thm)],[c25,c28,c60,c307,c1355,c1477,c1676]) ).
cnf(c1691,plain,
quotient(i(a(X,Y,Z)),W) = difference(a(X,Y,Z),j(W)),
inference(equational,[status(thm)],[c24,c1690]) ).
cnf(c1758,plain,
quotient(j(X),j(quotient(X,Y))) = difference(X,quotient(X,j(j(Y)))),
inference(equational,[status(thm)],[c29,c173,c377,c449,c508,c982,c1005,c1458]) ).
cnf(c1856,plain,
difference(j(X),quotient(j(X),Y)) = difference(i(X),quotient(i(X),Y)),
inference(equational,[status(thm)],[c553,c845,c1438]) ).
cnf(c1924,plain,
difference(i(X),quotient(i(X),Y)) = difference(X,quotient(X,Y)),
inference(equational,[status(thm)],[c27,c119,c1438,c1758]) ).
cnf(c2530,plain,
difference(X,difference(Y,product(product(Y,X),Z))) = product(Z,a(Y,X,Z)),
inference(equational,[status(thm)],[c18,c1304]) ).
cnf(c2535,plain,
difference(X,quotient(X,Y)) = j(difference(a(Y,Y,X),Y)),
inference(equational,[status(thm)],[c86,c484,c1477,c2530]) ).
cnf(c2539,plain,
difference(X,quotient(X,i(i(Y)))) = difference(Y,a(Y,Y,X)),
inference(equational,[status(thm)],[c87,c541,c1355,c2530]) ).
cnf(c2542,plain,
j(difference(a(X,Y,Y),Y)) = difference(X,quotient(X,Y)),
inference(equational,[status(thm)],[c86,c1856,c1924,c2535]) ).
cnf(c2543,plain,
difference(X,a(Y,X,X)) = difference(X,a(X,X,Y)),
inference(equational,[status(thm)],[c27,c48,c87,c203,c220,c514,c1667,c1691,c2539,c2542]) ).
cnf(c2544,plain,
a(X,Y,Y) = a(Y,Y,X),
inference(equational,[status(thm)],[c18,c935,c1371,c2543]) ).
cnf(g1,plain,
a(x0,x1,x1) = a(x1,x1,x0),
inference(equational,[status(thm)],[c2544]) ).
cnf(g2,plain,
$false,
inference(resolution,[status(thm)],[g0,g1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GRP772-1 : TPTP v9.0.0. Released v4.1.0.
% 0.06/0.12 % Command : run_Leo-III %s %d THM
% 0.11/0.32 % Computer : n003.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Mon Jul 14 09:04:34 EDT 2025
% 0.11/0.32 % CPUTime :
% 114.74/114.57 % SZS status Unsatisfiable
% 114.74/114.57 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------