%------------------------------------------------------------------------------
% File : Toma---0.7
% Problem : GRP048-10 : TPTP v9.0.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_Leo-III %s %d THM
% Computer : n007.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:43:21 AM UTC 2025
% Result : Unsatisfiable 75.94s 76.14s
% Output : CNFRefutation 75.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 9
% Syntax : Number of clauses : 39 ( 39 unt; 0 nHn; 13 RR)
% Number of literals : 39 ( 38 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 : 9 ( 9 usr; 4 con; 0-4 aty)
% Number of variables : 58 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,negated_conjecture,
equalish(inverse(a),inverse(b)) != true,
file('theBenchmark.p',prove_inverse_substitution) ).
cnf(c1,axiom,
equalish(a,b) = true,
file('theBenchmark.p',a_equals_b) ).
cnf(c2,axiom,
product(identity,X,X) = true,
file('theBenchmark.p',left_identity) ).
cnf(c3,axiom,
ifeq(X,X,Y,Z) = Y,
file('theBenchmark.p',ifeq_axiom) ).
cnf(c4,axiom,
product(inverse(X),X,identity) = true,
file('theBenchmark.p',left_inverse) ).
cnf(c5,axiom,
product(X,Y,multiply(X,Y)) = true,
file('theBenchmark.p',total_function1) ).
cnf(c6,axiom,
ifeq(product(X,Y,Z),true,ifeq(product(X,Y,W),true,equalish(W,Z),true),true) = true,
file('theBenchmark.p',total_function2) ).
cnf(c7,plain,
ifeq(product(identity,X,Y),true,equalish(Y,X),true) = true,
inference(equational,[status(thm)],[c2,c3,c6]) ).
cnf(c16,plain,
ifeq(product(inverse(X),X,Y),true,equalish(Y,identity),true) = true,
inference(equational,[status(thm)],[c3,c4,c6]) ).
cnf(c28,axiom,
ifeq(equalish(X,Y),true,ifeq(product(Z,W,X),true,product(Z,W,Y),true),true) = true,
file('theBenchmark.p',product_substitution3) ).
cnf(c29,plain,
ifeq(equalish(X,Y),true,product(identity,X,Y),true) = true,
inference(equational,[status(thm)],[c2,c3,c28]) ).
cnf(c56,plain,
ifeq(product(X,Y,a),true,product(X,Y,b),true) = true,
inference(equational,[status(thm)],[c1,c3,c28]) ).
cnf(c76,plain,
ifeq(equalish(multiply(X,Y),Z),true,product(X,Y,Z),true) = true,
inference(equational,[status(thm)],[c3,c5,c28]) ).
cnf(c694,axiom,
ifeq(product(X,Y,Z),true,ifeq(product(W,Y,V),true,ifeq(product(U,W,X),true,product(U,V,Z),true),true),true) = true,
file('theBenchmark.p',associativity1) ).
cnf(c1122,plain,
ifeq(product(X,Y,Z),true,ifeq(product(W,X,identity),true,product(W,Z,Y),true),true) = true,
inference(equational,[status(thm)],[c2,c3,c694]) ).
cnf(c1187,plain,
ifeq(product(X,Y,Z),true,product(inverse(X),Z,Y),true) = true,
inference(equational,[status(thm)],[c3,c4,c1122]) ).
cnf(c1188,plain,
product(inverse(inverse(X)),identity,X) = true,
inference(equational,[status(thm)],[c3,c4,c1187]) ).
cnf(c1194,plain,
product(inverse(X),multiply(X,Y),Y) = true,
inference(equational,[status(thm)],[c3,c5,c1187]) ).
cnf(c1195,plain,
product(inverse(inverse(a)),identity,b) = true,
inference(equational,[status(thm)],[c3,c56,c1188]) ).
cnf(c1221,plain,
product(inverse(inverse(X)),Y,multiply(X,Y)) = true,
inference(equational,[status(thm)],[c3,c1187,c1194]) ).
cnf(c1222,plain,
equalish(multiply(X,inverse(X)),identity) = true,
inference(equational,[status(thm)],[c3,c16,c1221]) ).
cnf(c1223,plain,
product(X,inverse(X),identity) = true,
inference(equational,[status(thm)],[c3,c76,c1222]) ).
cnf(c1230,plain,
product(inverse(inverse(inverse(a))),b,identity) = true,
inference(equational,[status(thm)],[c3,c1187,c1195]) ).
cnf(c1549,plain,
ifeq(product(X,inverse(Y),identity),true,product(X,identity,Y),true) = true,
inference(equational,[status(thm)],[c3,c4,c1122]) ).
cnf(c1550,plain,
product(X,identity,X) = true,
inference(equational,[status(thm)],[c3,c1223,c1549]) ).
cnf(c1962,plain,
ifeq(product(X,Y,identity),true,product(X,multiply(Y,Z),Z),true) = true,
inference(equational,[status(thm)],[c3,c5,c1122]) ).
cnf(c1996,plain,
product(inverse(inverse(inverse(a))),multiply(b,X),X) = true,
inference(equational,[status(thm)],[c3,c1230,c1962]) ).
cnf(c2452,plain,
ifeq(product(inverse(inverse(X)),identity,Y),true,equalish(Y,X),true) = true,
inference(equational,[status(thm)],[c3,c6,c1188]) ).
cnf(c2790,plain,
product(inverse(inverse(inverse(inverse(a)))),X,multiply(b,X)) = true,
inference(equational,[status(thm)],[c3,c1187,c1996]) ).
cnf(c2792,plain,
equalish(multiply(b,identity),inverse(inverse(a))) = true,
inference(equational,[status(thm)],[c3,c2452,c2790]) ).
cnf(c2793,plain,
product(b,identity,inverse(inverse(a))) = true,
inference(equational,[status(thm)],[c3,c76,c2792]) ).
cnf(c2797,plain,
product(inverse(b),inverse(inverse(a)),identity) = true,
inference(equational,[status(thm)],[c3,c1187,c2793]) ).
cnf(c2798,plain,
product(inverse(b),identity,inverse(a)) = true,
inference(equational,[status(thm)],[c3,c1549,c2797]) ).
cnf(c3086,plain,
ifeq(product(X,identity,Y),true,equalish(X,Y),true) = true,
inference(equational,[status(thm)],[c3,c6,c1550]) ).
cnf(c3088,plain,
equalish(inverse(b),inverse(a)) = true,
inference(equational,[status(thm)],[c3,c2798,c3086]) ).
cnf(c3115,plain,
product(identity,inverse(b),inverse(a)) = true,
inference(equational,[status(thm)],[c3,c29,c3088]) ).
cnf(c3116,plain,
equalish(inverse(a),inverse(b)) = true,
inference(equational,[status(thm)],[c3,c7,c3115]) ).
cnf(g1,plain,
equalish(inverse(a),inverse(b)) = true,
inference(equational,[status(thm)],[c3116]) ).
cnf(g2,plain,
$false,
inference(resolution,[status(thm)],[g0,g1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP048-10 : TPTP v9.0.0. Released v7.5.0.
% 0.07/0.12 % Command : run_Leo-III %s %d THM
% 0.12/0.33 % Computer : n007.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Jul 14 08:06:49 EDT 2025
% 0.12/0.34 % CPUTime :
% 75.94/76.14 % SZS status Unsatisfiable
% 75.94/76.14 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------