%------------------------------------------------------------------------------
% File : Toma---0.7
% Problem : GRP002-10 : TPTP v9.0.0. Released v7.3.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:43:15 AM UTC 2025
% Result : Unsatisfiable 105.63s 105.71s
% Output : CNFRefutation 105.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 16
% Syntax : Number of clauses : 88 ( 88 unt; 0 nHn; 26 RR)
% Number of literals : 88 ( 87 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 : 14 ( 14 usr; 9 con; 0-4 aty)
% Number of variables : 130 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,negated_conjecture,
product(k,inverse(b),identity) != true,
file('theBenchmark.p',prove_k_times_inverse_b_is_e) ).
cnf(c1,axiom,
product(identity,X,X) = true,
file('theBenchmark.p',left_identity) ).
cnf(c2,axiom,
product(X,identity,X) = true,
file('theBenchmark.p',right_identity) ).
cnf(c3,axiom,
product(a,b,c) = true,
file('theBenchmark.p',a_times_b_is_c) ).
cnf(c4,axiom,
product(h,b,j) = true,
file('theBenchmark.p',h_times_b_is_j) ).
cnf(c5,axiom,
ifeq(X,X,Y,Z) = Y,
file('theBenchmark.p',ifeq_axiom_001) ).
cnf(c6,axiom,
ifeq2(X,X,Y,Z) = Y,
file('theBenchmark.p',ifeq_axiom) ).
cnf(c7,axiom,
product(inverse(X),X,identity) = true,
file('theBenchmark.p',left_inverse) ).
cnf(c8,axiom,
product(X,inverse(X),identity) = true,
file('theBenchmark.p',right_inverse) ).
cnf(c9,axiom,
product(d,inverse(b),h) = true,
file('theBenchmark.p',d_times_inverse_b_is_h) ).
cnf(c10,axiom,
product(c,inverse(a),d) = true,
file('theBenchmark.p',c_times_inverse_a_is_d) ).
cnf(c11,axiom,
product(j,inverse(h),k) = true,
file('theBenchmark.p',j_times_inverse_h_is_k) ).
cnf(c12,axiom,
product(X,Y,multiply(X,Y)) = true,
file('theBenchmark.p',total_function1) ).
cnf(c13,axiom,
ifeq(product(X,X,Y),true,product(X,Y,identity),true) = true,
file('theBenchmark.p',x_cubed_is_identity_1) ).
cnf(c14,plain,
product(X,multiply(X,X),identity) = true,
inference(equational,[status(thm)],[c5,c12,c13]) ).
cnf(c20,axiom,
ifeq2(product(X,Y,Z),true,ifeq2(product(X,Y,W),true,W,Z),Z) = Z,
file('theBenchmark.p',total_function2) ).
cnf(c21,plain,
ifeq2(product(X,identity,Y),true,Y,X) = X,
inference(equational,[status(thm)],[c2,c6,c20]) ).
cnf(c23,plain,
multiply(X,identity) = X,
inference(equational,[status(thm)],[c6,c12,c21]) ).
cnf(c26,plain,
ifeq2(product(X,identity,Y),true,X,Y) = Y,
inference(equational,[status(thm)],[c2,c6,c20]) ).
cnf(c49,plain,
ifeq2(product(X,Y,Z),true,multiply(X,Y),Z) = Z,
inference(equational,[status(thm)],[c6,c12,c20]) ).
cnf(c50,plain,
multiply(X,multiply(X,X)) = identity,
inference(equational,[status(thm)],[c6,c14,c49]) ).
cnf(c52,plain,
ifeq2(product(X,Y,Z),true,Z,multiply(X,Y)) = multiply(X,Y),
inference(equational,[status(thm)],[c6,c12,c20]) ).
cnf(c57,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(c322,plain,
ifeq(product(X,Y,Z),true,ifeq(product(W,X,identity),true,product(W,Z,Y),true),true) = true,
inference(equational,[status(thm)],[c1,c5,c57]) ).
cnf(c357,plain,
ifeq(product(X,Y,Z),true,product(inverse(X),Z,Y),true) = true,
inference(equational,[status(thm)],[c5,c7,c322]) ).
cnf(c358,plain,
product(inverse(inverse(X)),identity,X) = true,
inference(equational,[status(thm)],[c5,c7,c357]) ).
cnf(c359,plain,
inverse(inverse(X)) = X,
inference(equational,[status(thm)],[c6,c26,c358]) ).
cnf(c366,plain,
product(inverse(X),multiply(X,Y),Y) = true,
inference(equational,[status(thm)],[c5,c12,c357]) ).
cnf(c367,plain,
multiply(inverse(X),multiply(X,Y)) = Y,
inference(equational,[status(thm)],[c6,c52,c366]) ).
cnf(c368,plain,
multiply(X,X) = inverse(X),
inference(equational,[status(thm)],[c23,c50,c367]) ).
cnf(c383,plain,
ifeq(product(inverse(X),Y,Z),true,product(X,Z,Y),true) = true,
inference(equational,[status(thm)],[c5,c8,c322]) ).
cnf(c459,plain,
ifeq(product(X,b,Y),true,ifeq(product(Z,X,h),true,product(Z,Y,j),true),true) = true,
inference(equational,[status(thm)],[c4,c5,c57]) ).
cnf(c462,plain,
ifeq(product(X,inverse(b),h),true,product(X,identity,j),true) = true,
inference(equational,[status(thm)],[c5,c7,c459]) ).
cnf(c463,plain,
product(d,identity,j) = true,
inference(equational,[status(thm)],[c5,c9,c462]) ).
cnf(c464,plain,
j = d,
inference(equational,[status(thm)],[c6,c26,c463]) ).
cnf(c556,plain,
ifeq(product(X,b,Y),true,ifeq(product(Z,X,a),true,product(Z,Y,c),true),true) = true,
inference(equational,[status(thm)],[c3,c5,c57]) ).
cnf(c560,plain,
ifeq(product(X,Y,a),true,product(X,multiply(Y,b),c),true) = true,
inference(equational,[status(thm)],[c5,c12,c556]) ).
cnf(c561,plain,
product(inverse(X),multiply(multiply(X,a),b),c) = true,
inference(equational,[status(thm)],[c5,c366,c560]) ).
cnf(c562,plain,
product(X,c,multiply(multiply(X,a),b)) = true,
inference(equational,[status(thm)],[c5,c383,c561]) ).
cnf(c563,plain,
multiply(multiply(X,a),b) = multiply(X,c),
inference(equational,[status(thm)],[c6,c52,c562]) ).
cnf(c571,plain,
multiply(inverse(multiply(X,a)),multiply(X,c)) = b,
inference(equational,[status(thm)],[c367,c563]) ).
cnf(c576,plain,
multiply(inverse(multiply(c,a)),inverse(c)) = b,
inference(equational,[status(thm)],[c368,c571]) ).
cnf(c622,plain,
ifeq(product(c,X,Y),true,ifeq(product(b,X,Z),true,product(a,Z,Y),true),true) = true,
inference(equational,[status(thm)],[c3,c5,c57]) ).
cnf(c640,plain,
ifeq(product(b,X,Y),true,product(a,Y,multiply(c,X)),true) = true,
inference(equational,[status(thm)],[c5,c12,c622]) ).
cnf(c641,plain,
product(a,multiply(b,X),multiply(c,X)) = true,
inference(equational,[status(thm)],[c5,c12,c640]) ).
cnf(c642,plain,
multiply(a,multiply(b,X)) = multiply(c,X),
inference(equational,[status(thm)],[c6,c52,c641]) ).
cnf(c644,plain,
multiply(inverse(a),multiply(c,X)) = multiply(b,X),
inference(equational,[status(thm)],[c367,c642]) ).
cnf(c645,plain,
multiply(inverse(a),inverse(c)) = multiply(b,c),
inference(equational,[status(thm)],[c368,c644]) ).
cnf(c748,plain,
ifeq(product(d,X,Y),true,ifeq(product(b,X,Z),true,product(h,Z,Y),true),true) = true,
inference(equational,[status(thm)],[c4,c5,c57,c464]) ).
cnf(c750,plain,
ifeq(product(b,inverse(d),X),true,product(h,X,identity),true) = true,
inference(equational,[status(thm)],[c5,c8,c748]) ).
cnf(c751,plain,
product(h,multiply(b,inverse(d)),identity) = true,
inference(equational,[status(thm)],[c5,c12,c750]) ).
cnf(c752,plain,
multiply(h,multiply(b,inverse(d))) = identity,
inference(equational,[status(thm)],[c6,c52,c751]) ).
cnf(c753,plain,
multiply(b,inverse(d)) = inverse(h),
inference(equational,[status(thm)],[c23,c367,c752]) ).
cnf(c754,plain,
multiply(c,inverse(d)) = multiply(a,inverse(h)),
inference(equational,[status(thm)],[c642,c753]) ).
cnf(c1065,plain,
ifeq(product(X,Y,Z),true,ifeq(product(W,X,inverse(Y)),true,product(W,Z,identity),true),true) = true,
inference(equational,[status(thm)],[c5,c7,c57]) ).
cnf(c1123,plain,
ifeq(product(X,Y,inverse(Z)),true,product(X,multiply(Y,Z),identity),true) = true,
inference(equational,[status(thm)],[c5,c12,c1065]) ).
cnf(c1124,plain,
product(inverse(X),multiply(multiply(X,inverse(Y)),Y),identity) = true,
inference(equational,[status(thm)],[c5,c366,c1123]) ).
cnf(c1125,plain,
product(X,identity,multiply(multiply(X,inverse(Y)),Y)) = true,
inference(equational,[status(thm)],[c5,c383,c1124]) ).
cnf(c1126,plain,
multiply(multiply(X,inverse(Y)),Y) = X,
inference(equational,[status(thm)],[c6,c26,c1125]) ).
cnf(c1129,plain,
multiply(multiply(b,c),c) = inverse(a),
inference(equational,[status(thm)],[c645,c1126]) ).
cnf(c1131,plain,
multiply(multiply(X,Y),inverse(Y)) = X,
inference(equational,[status(thm)],[c359,c1126]) ).
cnf(c1134,plain,
inverse(multiply(c,a)) = multiply(b,c),
inference(equational,[status(thm)],[c359,c576,c1131]) ).
cnf(c1139,plain,
multiply(multiply(a,inverse(h)),d) = c,
inference(equational,[status(thm)],[c754,c1126]) ).
cnf(c1141,plain,
inverse(multiply(b,c)) = multiply(c,a),
inference(equational,[status(thm)],[c359,c1134]) ).
cnf(c1149,plain,
multiply(inverse(multiply(X,Y)),X) = inverse(Y),
inference(equational,[status(thm)],[c367,c1131]) ).
cnf(c1153,plain,
multiply(inverse(X),inverse(Y)) = inverse(multiply(Y,X)),
inference(equational,[status(thm)],[c367,c1149]) ).
cnf(c2453,plain,
ifeq(product(X,inverse(h),Y),true,ifeq(product(Z,d,X),true,product(Z,k,Y),true),true) = true,
inference(equational,[status(thm)],[c5,c11,c57,c464]) ).
cnf(c2455,plain,
ifeq(product(X,d,Y),true,product(X,k,multiply(Y,inverse(h))),true) = true,
inference(equational,[status(thm)],[c5,c12,c2453]) ).
cnf(c2461,plain,
product(X,k,multiply(multiply(X,d),inverse(h))) = true,
inference(equational,[status(thm)],[c5,c12,c2455]) ).
cnf(c2462,plain,
multiply(multiply(X,d),inverse(h)) = multiply(X,k),
inference(equational,[status(thm)],[c6,c52,c2461]) ).
cnf(c3334,plain,
ifeq(product(X,inverse(a),Y),true,ifeq(product(Z,c,X),true,product(Z,d,Y),true),true) = true,
inference(equational,[status(thm)],[c5,c10,c57]) ).
cnf(c3336,plain,
ifeq(product(X,c,Y),true,product(X,d,multiply(Y,inverse(a))),true) = true,
inference(equational,[status(thm)],[c5,c12,c3334]) ).
cnf(c3337,plain,
product(X,d,multiply(multiply(X,c),inverse(a))) = true,
inference(equational,[status(thm)],[c5,c12,c3336]) ).
cnf(c3338,plain,
multiply(multiply(X,c),inverse(a)) = multiply(X,d),
inference(equational,[status(thm)],[c6,c52,c3337]) ).
cnf(c3342,plain,
multiply(multiply(X,d),a) = multiply(X,c),
inference(equational,[status(thm)],[c1126,c3338]) ).
cnf(c3344,plain,
multiply(multiply(b,c),d) = a,
inference(equational,[status(thm)],[c359,c368,c1129,c1153,c3338]) ).
cnf(c3360,plain,
multiply(multiply(b,c),k) = multiply(a,inverse(h)),
inference(equational,[status(thm)],[c2462,c3344]) ).
cnf(c3365,plain,
multiply(multiply(a,inverse(h)),c) = multiply(c,a),
inference(equational,[status(thm)],[c1139,c3342]) ).
cnf(c3492,plain,
multiply(multiply(b,c),multiply(a,inverse(h))) = inverse(c),
inference(equational,[status(thm)],[c1134,c1149,c3365]) ).
cnf(c3520,plain,
multiply(multiply(c,a),multiply(a,inverse(h))) = k,
inference(equational,[status(thm)],[c367,c1141,c3360]) ).
cnf(c5319,plain,
ifeq(product(multiply(X,Y),Z,W),true,ifeq(product(Y,Z,V),true,product(X,V,W),true),true) = true,
inference(equational,[status(thm)],[c5,c12,c57]) ).
cnf(c5322,plain,
ifeq(product(X,Y,Z),true,product(W,Z,multiply(multiply(W,X),Y)),true) = true,
inference(equational,[status(thm)],[c5,c12,c5319]) ).
cnf(c5323,plain,
product(X,multiply(Y,Z),multiply(multiply(X,Y),Z)) = true,
inference(equational,[status(thm)],[c5,c12,c5322]) ).
cnf(c5324,plain,
multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)),
inference(equational,[status(thm)],[c6,c52,c5323]) ).
cnf(c5325,plain,
multiply(X,multiply(X,Y)) = multiply(inverse(X),Y),
inference(equational,[status(thm)],[c368,c5324]) ).
cnf(c5326,plain,
b = k,
inference(equational,[status(thm)],[c1131,c1141,c3492,c3520,c5325]) ).
cnf(g1,plain,
product(k,inverse(b),identity) = true,
inference(equational,[status(thm)],[c8,c5326]) ).
cnf(g2,plain,
$false,
inference(resolution,[status(thm)],[g0,g1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : GRP002-10 : TPTP v9.0.0. Released v7.3.0.
% 0.11/0.11 % Command : run_Leo-III %s %d THM
% 0.11/0.31 % Computer : n003.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Mon Jul 14 08:05:04 EDT 2025
% 0.11/0.31 % CPUTime :
% 105.63/105.71 % SZS status Unsatisfiable
% 105.63/105.71 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------