%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP002-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n026.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:24:53 PM UTC 2026
% Result : Unsatisfiable 260.15s 34.05s
% Output : CNFRefutation 260.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 21
% Syntax : Number of clauses : 224 ( 224 unt; 0 nHn; 95 RR)
% Number of literals : 224 ( 223 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 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 : 248 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t253,axiom,
ifeq2(product(X1,X2,X3),true,ifeq2(product(X1,X2,X4),true,X4,X3),X3) = X3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t315,plain,
ifeq2(product(X1,X2,X3),true,ifeq2(product(X1,X2,X4),true,X4,X3),X3) = X3,
inference(orient,[status(thm)],[t253]) ).
cnf(t167,axiom,
product(X1,X2,multiply(X1,X2)) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t383,plain,
product(X1,X2,multiply(X1,X2)) = true,
inference(orient,[status(thm)],[t167]) ).
cnf(t402,plain,
multiply(X1,X2) = ifeq2(true,true,ifeq2(product(X1,X2,X3),true,X3,multiply(X1,X2)),multiply(X1,X2)),
inference(cp,[status(thm)],[t315,t383]) ).
cnf(t43,axiom,
ifeq2(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t314,plain,
ifeq2(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t43]) ).
cnf(t91159,plain,
multiply(X1,X2) = ifeq2(product(X1,X2,X3),true,X3,multiply(X1,X2)),
inference(step,[status(thm)],[t402,t314]) ).
cnf(t1403,plain,
ifeq2(product(X1,X2,X3),true,X3,multiply(X1,X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t91159]) ).
cnf(t255,axiom,
ifeq(product(X1,X2,X3),true,ifeq(product(X4,X3,X5),true,ifeq(product(X4,X1,X6),true,product(X6,X2,X5),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t477,plain,
ifeq(product(X1,X2,X3),true,ifeq(product(X4,X3,X5),true,ifeq(product(X4,X1,X6),true,product(X6,X2,X5),true),true),true) = true,
inference(orient,[status(thm)],[t255]) ).
cnf(t478,plain,
true = ifeq(true,true,ifeq(product(X1,multiply(X2,X3),X4),true,ifeq(product(X1,X2,X5),true,product(X5,X3,X4),true),true),true),
inference(cp,[status(thm)],[t477,t383]) ).
cnf(t42,axiom,
ifeq(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t313,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t42]) ).
cnf(t91208,plain,
true = ifeq(product(X1,multiply(X2,X3),X4),true,ifeq(product(X1,X2,X5),true,product(X5,X3,X4),true),true),
inference(step,[status(thm)],[t478,t313]) ).
cnf(t2579,plain,
ifeq(product(X1,multiply(X2,X3),X4),true,ifeq(product(X1,X2,X5),true,product(X5,X3,X4),true),true) = true,
inference(orient,[status(thm)],[t91208]) ).
cnf(hi7,axiom,
ifeq(product(Y,Z,V),true,ifeq(product(X,V,W),true,ifeq(product(X,Y,U),true,product(U,Z,W),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(hi4,axiom,
product(X,Y,multiply(X,Y)) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(hi2,axiom,
product(inverse(X),X,identity) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(h41,plain,
product(identity,V0,multiply(inverse(V1),multiply(V1,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi4,hi4,hi2]) ).
cnf(hi5,axiom,
ifeq2(product(X,Y,W),true,ifeq2(product(X,Y,Z),true,Z,W),W) = W,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(hi0,axiom,
product(identity,X,X) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t141,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(hyper_resolution,[status(thm)],[hi5,hi0,h41]) ).
cnf(t298,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(orient,[status(thm)],[t141]) ).
cnf(hi8,axiom,
ifeq(product(X,X,Y),true,product(X,Y,identity),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(h19,plain,
product(V0,multiply(V0,V0),identity) = true,
inference(hyper_resolution,[status(thm)],[hi8,hi4]) ).
cnf(t57,plain,
multiply(X1,multiply(X1,X1)) = identity,
inference(hyper_resolution,[status(thm)],[hi5,hi4,h19]) ).
cnf(t316,plain,
multiply(X1,multiply(X1,X1)) = identity,
inference(orient,[status(thm)],[t57]) ).
cnf(t322,plain,
multiply(X1,X1) = multiply(inverse(X1),identity),
inference(cp,[status(thm)],[t298,t316]) ).
cnf(hi1,axiom,
product(X,identity,X) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t6,plain,
multiply(X1,identity) = X1,
inference(hyper_resolution,[status(thm)],[hi5,hi1,hi4]) ).
cnf(t268,plain,
multiply(X1,identity) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t91120,plain,
multiply(X1,X1) = inverse(X1),
inference(step,[status(thm)],[t322,t268]) ).
cnf(t691,plain,
multiply(X1,X1) = inverse(X1),
inference(orient,[status(thm)],[t91120]) ).
cnf(t692,plain,
true = product(X1,X1,inverse(X1)),
inference(cp,[status(thm)],[t383,t691]) ).
cnf(t736,plain,
product(X1,X1,inverse(X1)) = true,
inference(orient,[status(thm)],[t692]) ).
cnf(t2666,plain,
true = ifeq(product(X1,multiply(X1,X2),X3),true,ifeq(true,true,product(inverse(X1),X2,X3),true),true),
inference(cp,[status(thm)],[t2579,t736]) ).
cnf(t92856,plain,
true = ifeq(product(X1,multiply(X1,X2),X3),true,product(inverse(X1),X2,X3),true),
inference(step,[status(thm)],[t2666,t313]) ).
cnf(t87093,plain,
ifeq(product(X1,multiply(X1,X2),X3),true,product(inverse(X1),X2,X3),true) = true,
inference(orient,[status(thm)],[t92856]) ).
cnf(t87094,plain,
true = ifeq(true,true,product(inverse(X1),X2,multiply(X1,multiply(X1,X2))),true),
inference(cp,[status(thm)],[t87093,t383]) ).
cnf(t92857,plain,
true = product(inverse(X1),X2,multiply(X1,multiply(X1,X2))),
inference(step,[status(thm)],[t87094,t313]) ).
cnf(t87879,plain,
product(inverse(X1),X2,multiply(X1,multiply(X1,X2))) = true,
inference(orient,[status(thm)],[t92857]) ).
cnf(t88626,plain,
multiply(inverse(X1),X2) = ifeq2(true,true,multiply(X1,multiply(X1,X2)),multiply(inverse(X1),X2)),
inference(cp,[status(thm)],[t1403,t87879]) ).
cnf(t92858,plain,
multiply(inverse(X1),X2) = multiply(X1,multiply(X1,X2)),
inference(step,[status(thm)],[t88626,t314]) ).
cnf(t88737,plain,
multiply(X1,multiply(X1,X2)) = multiply(inverse(X1),X2),
inference(orient,[status(thm)],[t92858]) ).
cnf(hi3,axiom,
product(X,inverse(X),identity) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(h25,plain,
product(multiply(V0,V1),inverse(V1),V0) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi3,hi1,hi4]) ).
cnf(t151,plain,
multiply(multiply(X1,X2),inverse(X2)) = X1,
inference(hyper_resolution,[status(thm)],[hi5,hi4,h25]) ).
cnf(t277,plain,
multiply(multiply(X1,X2),inverse(X2)) = X1,
inference(orient,[status(thm)],[t151]) ).
cnf(t306,plain,
inverse(X1) = multiply(X2,inverse(multiply(X1,X2))),
inference(cp,[status(thm)],[t277,t298]) ).
cnf(t801,plain,
multiply(X1,inverse(multiply(X2,X1))) = inverse(X2),
inference(orient,[status(thm)],[t306]) ).
cnf(h29,plain,
product(multiply(V0,inverse(V1)),V1,V0) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi2,hi1,hi4]) ).
cnf(t154,plain,
multiply(multiply(X1,inverse(X2)),X2) = X1,
inference(hyper_resolution,[status(thm)],[hi5,hi4,h29]) ).
cnf(t283,plain,
multiply(multiply(X1,inverse(X2)),X2) = X1,
inference(orient,[status(thm)],[t154]) ).
cnf(t804,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(cp,[status(thm)],[t801,t283]) ).
cnf(t840,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t804]) ).
cnf(t851,plain,
X1 = multiply(multiply(X2,inverse(X3)),multiply(multiply(X3,inverse(X2)),X1)),
inference(cp,[status(thm)],[t298,t840]) ).
cnf(t2174,plain,
multiply(multiply(X1,inverse(X2)),multiply(multiply(X2,inverse(X1)),X3)) = X3,
inference(orient,[status(thm)],[t851]) ).
cnf(t304,plain,
inverse(X1) = multiply(inverse(multiply(X2,X1)),X2),
inference(cp,[status(thm)],[t298,t277]) ).
cnf(t792,plain,
multiply(inverse(multiply(X1,X2)),X1) = inverse(X2),
inference(orient,[status(thm)],[t304]) ).
cnf(t796,plain,
inverse(multiply(X1,X2)) = multiply(inverse(X2),inverse(X1)),
inference(cp,[status(thm)],[t792,t298]) ).
cnf(t835,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t796]) ).
cnf(t843,plain,
inverse(multiply(X1,multiply(X2,inverse(X3)))) = multiply(multiply(X3,inverse(X2)),inverse(X1)),
inference(cp,[status(thm)],[t835,t840]) ).
cnf(t1581,plain,
inverse(multiply(X1,multiply(X2,inverse(X3)))) = multiply(multiply(X3,inverse(X2)),inverse(X1)),
inference(orient,[status(thm)],[t843]) ).
cnf(hi14,negated_conjecture,
product(j,inverse(h),k) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t207,plain,
product(k,inverse(inverse(h)),j) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi3,hi1,hi14]) ).
cnf(h10,plain,
product(identity,inverse(inverse(V0)),V0) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi3,hi1,hi3]) ).
cnf(t68,plain,
multiply(identity,inverse(inverse(X1))) = X1,
inference(hyper_resolution,[status(thm)],[hi5,hi4,h10]) ).
cnf(h35,plain,
product(multiply(identity,V0),identity,V0) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi1,hi0,hi4]) ).
cnf(t99,plain,
multiply(multiply(identity,X1),identity) = X1,
inference(hyper_resolution,[status(thm)],[hi5,hi4,h35]) ).
cnf(t91089,plain,
multiply(identity,X1) = X1,
inference(step,[status(thm)],[t99,t268]) ).
cnf(t288,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t91089]) ).
cnf(t91090,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t68,t288]) ).
cnf(t296,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t91090]) ).
cnf(t91119,plain,
product(k,h,j) = true,
inference(step,[status(thm)],[t207,t296]) ).
cnf(t474,plain,
product(k,h,j) = true,
inference(orient,[status(thm)],[t91119]) ).
cnf(t2701,plain,
true = ifeq(product(k,multiply(h,X1),X2),true,ifeq(true,true,product(j,X1,X2),true),true),
inference(cp,[status(thm)],[t2579,t474]) ).
cnf(t91355,plain,
true = ifeq(product(k,multiply(h,X1),X2),true,product(j,X1,X2),true),
inference(step,[status(thm)],[t2701,t313]) ).
cnf(t7485,plain,
ifeq(product(k,multiply(h,X1),X2),true,product(j,X1,X2),true) = true,
inference(orient,[status(thm)],[t91355]) ).
cnf(t7486,plain,
true = ifeq(true,true,product(j,X1,multiply(k,multiply(h,X1))),true),
inference(cp,[status(thm)],[t7485,t383]) ).
cnf(t91356,plain,
true = product(j,X1,multiply(k,multiply(h,X1))),
inference(step,[status(thm)],[t7486,t313]) ).
cnf(t7495,plain,
product(j,X1,multiply(k,multiply(h,X1))) = true,
inference(orient,[status(thm)],[t91356]) ).
cnf(t7502,plain,
multiply(j,X1) = ifeq2(true,true,multiply(k,multiply(h,X1)),multiply(j,X1)),
inference(cp,[status(thm)],[t1403,t7495]) ).
cnf(t91358,plain,
multiply(j,X1) = multiply(k,multiply(h,X1)),
inference(step,[status(thm)],[t7502,t314]) ).
cnf(t7743,plain,
multiply(k,multiply(h,X1)) = multiply(j,X1),
inference(orient,[status(thm)],[t91358]) ).
cnf(t7746,plain,
multiply(j,inverse(multiply(X1,h))) = multiply(k,inverse(X1)),
inference(cp,[status(thm)],[t7743,t801]) ).
cnf(t8217,plain,
multiply(j,inverse(multiply(X1,h))) = multiply(k,inverse(X1)),
inference(orient,[status(thm)],[t7746]) ).
cnf(hi6,axiom,
ifeq(product(U,Z,W),true,ifeq(product(Y,Z,V),true,ifeq(product(X,Y,U),true,product(X,V,W),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(hi10,negated_conjecture,
product(a,b,c) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t110,plain,
product(inverse(a),c,b) = true,
inference(hyper_resolution,[status(thm)],[hi6,hi0,hi10,hi2]) ).
cnf(t438,plain,
product(inverse(a),c,b) = true,
inference(orient,[status(thm)],[t110]) ).
cnf(t491,plain,
true = ifeq(true,true,ifeq(product(X1,b,X2),true,ifeq(product(X1,inverse(a),X3),true,product(X3,c,X2),true),true),true),
inference(cp,[status(thm)],[t477,t438]) ).
cnf(t91449,plain,
true = ifeq(product(X1,b,X2),true,ifeq(product(X1,inverse(a),X3),true,product(X3,c,X2),true),true),
inference(step,[status(thm)],[t491,t313]) ).
cnf(t13691,plain,
ifeq(product(X1,b,X2),true,ifeq(product(X1,inverse(a),X3),true,product(X3,c,X2),true),true) = true,
inference(orient,[status(thm)],[t91449]) ).
cnf(hi13,negated_conjecture,
product(h,b,j) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t217,plain,
product(multiply(identity,h),b,j) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi13,hi0,hi4]) ).
cnf(t91108,plain,
product(h,b,j) = true,
inference(step,[status(thm)],[t217,t288]) ).
cnf(t411,plain,
product(h,b,j) = true,
inference(orient,[status(thm)],[t91108]) ).
cnf(t13702,plain,
true = ifeq(true,true,ifeq(product(h,inverse(a),X1),true,product(X1,c,j),true),true),
inference(cp,[status(thm)],[t13691,t411]) ).
cnf(t91499,plain,
true = ifeq(product(h,inverse(a),X1),true,product(X1,c,j),true),
inference(step,[status(thm)],[t13702,t313]) ).
cnf(t16539,plain,
ifeq(product(h,inverse(a),X1),true,product(X1,c,j),true) = true,
inference(orient,[status(thm)],[t91499]) ).
cnf(t16540,plain,
true = ifeq(true,true,product(multiply(h,inverse(a)),c,j),true),
inference(cp,[status(thm)],[t16539,t383]) ).
cnf(t91500,plain,
true = product(multiply(h,inverse(a)),c,j),
inference(step,[status(thm)],[t16540,t313]) ).
cnf(t16541,plain,
product(multiply(h,inverse(a)),c,j) = true,
inference(orient,[status(thm)],[t91500]) ).
cnf(t16542,plain,
multiply(multiply(h,inverse(a)),c) = ifeq2(true,true,j,multiply(multiply(h,inverse(a)),c)),
inference(cp,[status(thm)],[t1403,t16541]) ).
cnf(t91501,plain,
multiply(multiply(h,inverse(a)),c) = j,
inference(step,[status(thm)],[t16542,t314]) ).
cnf(t16562,plain,
multiply(multiply(h,inverse(a)),c) = j,
inference(orient,[status(thm)],[t91501]) ).
cnf(t16571,plain,
multiply(h,inverse(a)) = multiply(j,inverse(c)),
inference(cp,[status(thm)],[t277,t16562]) ).
cnf(t16598,plain,
multiply(h,inverse(a)) = multiply(j,inverse(c)),
inference(orient,[status(thm)],[t16571]) ).
cnf(t16641,plain,
inverse(inverse(a)) = multiply(inverse(multiply(j,inverse(c))),h),
inference(cp,[status(thm)],[t792,t16598]) ).
cnf(t91507,plain,
a = multiply(inverse(multiply(j,inverse(c))),h),
inference(step,[status(thm)],[t16641,t296]) ).
cnf(t91508,plain,
a = multiply(multiply(c,inverse(j)),h),
inference(step,[status(thm)],[t91507,t840]) ).
cnf(t16746,plain,
multiply(multiply(c,inverse(j)),h) = a,
inference(orient,[status(thm)],[t91508]) ).
cnf(t16759,plain,
multiply(k,inverse(multiply(c,inverse(j)))) = multiply(j,inverse(a)),
inference(cp,[status(thm)],[t8217,t16746]) ).
cnf(t91512,plain,
multiply(k,multiply(j,inverse(c))) = multiply(j,inverse(a)),
inference(step,[status(thm)],[t16759,t840]) ).
cnf(h62,plain,
product(V0,V1,multiply(multiply(V0,identity),V1)) = true,
inference(hyper_resolution,[status(thm)],[hi6,hi4,hi0,hi4]) ).
cnf(hi11,negated_conjecture,
product(c,inverse(a),d) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(h121,plain,
product(d,a,c) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi2,hi1,hi11]) ).
cnf(t93,plain,
multiply(multiply(d,identity),a) = c,
inference(hyper_resolution,[status(thm)],[hi5,h121,h62]) ).
cnf(t91102,plain,
multiply(d,a) = c,
inference(step,[status(thm)],[t93,t268]) ).
cnf(t98,plain,
multiply(multiply(h,identity),b) = j,
inference(hyper_resolution,[status(thm)],[hi5,hi13,h62]) ).
cnf(t91096,plain,
multiply(h,b) = j,
inference(step,[status(thm)],[t98,t268]) ).
cnf(hi12,negated_conjecture,
product(d,inverse(b),h) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(h150,plain,
product(h,b,d) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi2,hi1,hi12]) ).
cnf(t97,plain,
multiply(multiply(h,identity),b) = d,
inference(hyper_resolution,[status(thm)],[hi5,h62,h150]) ).
cnf(t91095,plain,
multiply(h,b) = d,
inference(step,[status(thm)],[t97,t268]) ).
cnf(t351,plain,
multiply(h,b) = d,
inference(orient,[status(thm)],[t91095]) ).
cnf(t91097,plain,
d = j,
inference(step,[status(thm)],[t91096,t351]) ).
cnf(t356,plain,
d = j,
inference(orient,[status(thm)],[t91097]) ).
cnf(t91103,plain,
multiply(j,a) = c,
inference(step,[status(thm)],[t91102,t356]) ).
cnf(t363,plain,
multiply(j,a) = c,
inference(orient,[status(thm)],[t91103]) ).
cnf(t393,plain,
true = product(j,a,c),
inference(cp,[status(thm)],[t383,t363]) ).
cnf(t711,plain,
product(j,a,c) = true,
inference(orient,[status(thm)],[t393]) ).
cnf(t2703,plain,
true = ifeq(product(j,multiply(a,X1),X2),true,ifeq(true,true,product(c,X1,X2),true),true),
inference(cp,[status(thm)],[t2579,t711]) ).
cnf(t91399,plain,
true = ifeq(product(j,multiply(a,X1),X2),true,product(c,X1,X2),true),
inference(step,[status(thm)],[t2703,t313]) ).
cnf(t10864,plain,
ifeq(product(j,multiply(a,X1),X2),true,product(c,X1,X2),true) = true,
inference(orient,[status(thm)],[t91399]) ).
cnf(t10865,plain,
true = ifeq(true,true,product(c,X1,multiply(j,multiply(a,X1))),true),
inference(cp,[status(thm)],[t10864,t383]) ).
cnf(t91400,plain,
true = product(c,X1,multiply(j,multiply(a,X1))),
inference(step,[status(thm)],[t10865,t313]) ).
cnf(t10873,plain,
product(c,X1,multiply(j,multiply(a,X1))) = true,
inference(orient,[status(thm)],[t91400]) ).
cnf(t10877,plain,
multiply(c,X1) = ifeq2(true,true,multiply(j,multiply(a,X1)),multiply(c,X1)),
inference(cp,[status(thm)],[t1403,t10873]) ).
cnf(t91404,plain,
multiply(c,X1) = multiply(j,multiply(a,X1)),
inference(step,[status(thm)],[t10877,t314]) ).
cnf(t11265,plain,
multiply(j,multiply(a,X1)) = multiply(c,X1),
inference(orient,[status(thm)],[t91404]) ).
cnf(t11266,plain,
multiply(c,a) = multiply(j,inverse(a)),
inference(cp,[status(thm)],[t11265,t691]) ).
cnf(t11309,plain,
multiply(j,inverse(a)) = multiply(c,a),
inference(orient,[status(thm)],[t11266]) ).
cnf(t91513,plain,
multiply(k,multiply(j,inverse(c))) = multiply(c,a),
inference(step,[status(thm)],[t91512,t11309]) ).
cnf(t16810,plain,
multiply(k,multiply(j,inverse(c))) = multiply(c,a),
inference(orient,[status(thm)],[t91513]) ).
cnf(t16840,plain,
multiply(multiply(c,inverse(j)),inverse(k)) = inverse(multiply(c,a)),
inference(cp,[status(thm)],[t1581,t16810]) ).
cnf(t11347,plain,
multiply(a,inverse(j)) = inverse(multiply(c,a)),
inference(cp,[status(thm)],[t840,t11309]) ).
cnf(t11442,plain,
inverse(multiply(c,a)) = multiply(a,inverse(j)),
inference(orient,[status(thm)],[t11347]) ).
cnf(t91519,plain,
multiply(multiply(c,inverse(j)),inverse(k)) = multiply(a,inverse(j)),
inference(step,[status(thm)],[t16840,t11442]) ).
cnf(t16961,plain,
multiply(multiply(c,inverse(j)),inverse(k)) = multiply(a,inverse(j)),
inference(orient,[status(thm)],[t91519]) ).
cnf(t16994,plain,
X1 = multiply(multiply(a,inverse(j)),multiply(multiply(k,inverse(multiply(c,inverse(j)))),X1)),
inference(cp,[status(thm)],[t2174,t16961]) ).
cnf(t91588,plain,
X1 = multiply(multiply(a,inverse(j)),multiply(multiply(k,multiply(j,inverse(c))),X1)),
inference(step,[status(thm)],[t16994,t840]) ).
cnf(t91589,plain,
X1 = multiply(multiply(a,inverse(j)),multiply(multiply(c,a),X1)),
inference(step,[status(thm)],[t91588,t16810]) ).
cnf(t18303,plain,
multiply(multiply(a,inverse(j)),multiply(multiply(c,a),X1)) = X1,
inference(orient,[status(thm)],[t91589]) ).
cnf(h40,plain,
product(identity,V0,multiply(V1,multiply(inverse(V1),V0))) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi4,hi4,hi3]) ).
cnf(t127,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(hyper_resolution,[status(thm)],[hi5,hi0,h40]) ).
cnf(t256,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t127]) ).
cnf(t11268,plain,
multiply(c,multiply(inverse(a),X1)) = multiply(j,X1),
inference(cp,[status(thm)],[t11265,t256]) ).
cnf(t11633,plain,
multiply(c,multiply(inverse(a),X1)) = multiply(j,X1),
inference(orient,[status(thm)],[t11268]) ).
cnf(t11676,plain,
multiply(multiply(X1,inverse(inverse(a))),inverse(c)) = inverse(multiply(j,inverse(X1))),
inference(cp,[status(thm)],[t1581,t11633]) ).
cnf(t91437,plain,
multiply(multiply(X1,a),inverse(c)) = inverse(multiply(j,inverse(X1))),
inference(step,[status(thm)],[t11676,t296]) ).
cnf(t91438,plain,
multiply(multiply(X1,a),inverse(c)) = multiply(X1,inverse(j)),
inference(step,[status(thm)],[t91437,t840]) ).
cnf(t13357,plain,
multiply(multiply(X1,a),inverse(c)) = multiply(X1,inverse(j)),
inference(orient,[status(thm)],[t91438]) ).
cnf(t18304,plain,
inverse(c) = multiply(multiply(a,inverse(j)),multiply(c,inverse(j))),
inference(cp,[status(thm)],[t18303,t13357]) ).
cnf(t18320,plain,
multiply(multiply(a,inverse(j)),multiply(c,inverse(j))) = inverse(c),
inference(orient,[status(thm)],[t18304]) ).
cnf(t400,plain,
true = product(multiply(X1,X2),inverse(X2),X1),
inference(cp,[status(thm)],[t383,t277]) ).
cnf(t897,plain,
product(multiply(X1,X2),inverse(X2),X1) = true,
inference(orient,[status(thm)],[t400]) ).
cnf(t908,plain,
true = product(X1,inverse(multiply(X2,X1)),inverse(X2)),
inference(cp,[status(thm)],[t897,t298]) ).
cnf(t1067,plain,
product(X1,inverse(multiply(X2,X1)),inverse(X2)) = true,
inference(orient,[status(thm)],[t908]) ).
cnf(t13705,plain,
true = ifeq(product(inverse(a),b,X1),true,ifeq(true,true,product(inverse(inverse(a)),c,X1),true),true),
inference(cp,[status(thm)],[t13691,t736]) ).
cnf(t91529,plain,
true = ifeq(product(inverse(a),b,X1),true,product(inverse(inverse(a)),c,X1),true),
inference(step,[status(thm)],[t13705,t313]) ).
cnf(t91530,plain,
true = ifeq(product(inverse(a),b,X1),true,product(a,c,X1),true),
inference(step,[status(thm)],[t91529,t296]) ).
cnf(t17239,plain,
ifeq(product(inverse(a),b,X1),true,product(a,c,X1),true) = true,
inference(orient,[status(thm)],[t91530]) ).
cnf(t17240,plain,
true = ifeq(true,true,product(a,c,multiply(inverse(a),b)),true),
inference(cp,[status(thm)],[t17239,t383]) ).
cnf(t91531,plain,
true = product(a,c,multiply(inverse(a),b)),
inference(step,[status(thm)],[t17240,t313]) ).
cnf(t17241,plain,
product(a,c,multiply(inverse(a),b)) = true,
inference(orient,[status(thm)],[t91531]) ).
cnf(t17242,plain,
multiply(a,c) = ifeq2(true,true,multiply(inverse(a),b),multiply(a,c)),
inference(cp,[status(thm)],[t1403,t17241]) ).
cnf(t91532,plain,
multiply(a,c) = multiply(inverse(a),b),
inference(step,[status(thm)],[t17242,t314]) ).
cnf(t17262,plain,
multiply(inverse(a),b) = multiply(a,c),
inference(orient,[status(thm)],[t91532]) ).
cnf(t17291,plain,
true = product(b,inverse(multiply(a,c)),inverse(inverse(a))),
inference(cp,[status(thm)],[t1067,t17262]) ).
cnf(t738,plain,
inverse(X1) = ifeq2(true,true,ifeq2(product(X1,X1,X2),true,X2,inverse(X1)),inverse(X1)),
inference(cp,[status(thm)],[t315,t736]) ).
cnf(t91152,plain,
inverse(X1) = ifeq2(product(X1,X1,X2),true,X2,inverse(X1)),
inference(step,[status(thm)],[t738,t314]) ).
cnf(t1207,plain,
ifeq2(product(X1,X1,X2),true,X2,inverse(X1)) = inverse(X1),
inference(orient,[status(thm)],[t91152]) ).
cnf(t10879,plain,
inverse(c) = ifeq2(true,true,multiply(j,multiply(a,c)),inverse(c)),
inference(cp,[status(thm)],[t1207,t10873]) ).
cnf(t91401,plain,
inverse(c) = multiply(j,multiply(a,c)),
inference(step,[status(thm)],[t10879,t314]) ).
cnf(t10920,plain,
multiply(j,multiply(a,c)) = inverse(c),
inference(orient,[status(thm)],[t91401]) ).
cnf(t10952,plain,
inverse(multiply(a,c)) = multiply(inverse(inverse(c)),j),
inference(cp,[status(thm)],[t792,t10920]) ).
cnf(t91403,plain,
inverse(multiply(a,c)) = multiply(c,j),
inference(step,[status(thm)],[t10952,t296]) ).
cnf(t11112,plain,
inverse(multiply(a,c)) = multiply(c,j),
inference(orient,[status(thm)],[t91403]) ).
cnf(t91543,plain,
true = product(b,multiply(c,j),inverse(inverse(a))),
inference(step,[status(thm)],[t17291,t11112]) ).
cnf(t91544,plain,
true = product(b,multiply(c,j),a),
inference(step,[status(thm)],[t91543,t296]) ).
cnf(t17444,plain,
product(b,multiply(c,j),a) = true,
inference(orient,[status(thm)],[t91544]) ).
cnf(t17447,plain,
true = ifeq(true,true,ifeq(product(b,c,X1),true,product(X1,j,a),true),true),
inference(cp,[status(thm)],[t2579,t17444]) ).
cnf(t91645,plain,
true = ifeq(product(b,c,X1),true,product(X1,j,a),true),
inference(step,[status(thm)],[t17447,t313]) ).
cnf(t19600,plain,
ifeq(product(b,c,X1),true,product(X1,j,a),true) = true,
inference(orient,[status(thm)],[t91645]) ).
cnf(t19601,plain,
true = ifeq(true,true,product(multiply(b,c),j,a),true),
inference(cp,[status(thm)],[t19600,t383]) ).
cnf(t91646,plain,
true = product(multiply(b,c),j,a),
inference(step,[status(thm)],[t19601,t313]) ).
cnf(t19602,plain,
product(multiply(b,c),j,a) = true,
inference(orient,[status(thm)],[t91646]) ).
cnf(t19603,plain,
multiply(multiply(b,c),j) = ifeq2(true,true,a,multiply(multiply(b,c),j)),
inference(cp,[status(thm)],[t1403,t19602]) ).
cnf(t91647,plain,
multiply(multiply(b,c),j) = a,
inference(step,[status(thm)],[t19603,t314]) ).
cnf(t19624,plain,
multiply(multiply(b,c),j) = a,
inference(orient,[status(thm)],[t91647]) ).
cnf(t19636,plain,
multiply(b,c) = multiply(a,inverse(j)),
inference(cp,[status(thm)],[t277,t19624]) ).
cnf(t19665,plain,
multiply(a,inverse(j)) = multiply(b,c),
inference(orient,[status(thm)],[t19636]) ).
cnf(t91653,plain,
multiply(multiply(b,c),multiply(c,inverse(j))) = inverse(c),
inference(step,[status(thm)],[t18320,t19665]) ).
cnf(t19733,plain,
multiply(multiply(b,c),multiply(c,inverse(j))) = inverse(c),
inference(rw,[status(thm)],[t91653]) ).
cnf(t21280,plain,
multiply(multiply(b,c),multiply(c,inverse(j))) = inverse(c),
inference(orient,[status(thm)],[t19733]) ).
cnf(t88938,plain,
multiply(inverse(multiply(b,c)),multiply(c,inverse(j))) = multiply(multiply(b,c),inverse(c)),
inference(cp,[status(thm)],[t88737,t21280]) ).
cnf(t19712,plain,
multiply(j,inverse(a)) = inverse(multiply(b,c)),
inference(cp,[status(thm)],[t840,t19665]) ).
cnf(t91670,plain,
multiply(c,a) = inverse(multiply(b,c)),
inference(step,[status(thm)],[t19712,t11309]) ).
cnf(t19750,plain,
inverse(multiply(b,c)) = multiply(c,a),
inference(orient,[status(thm)],[t91670]) ).
cnf(t92927,plain,
multiply(multiply(c,a),multiply(c,inverse(j))) = multiply(multiply(b,c),inverse(c)),
inference(step,[status(thm)],[t88938,t19750]) ).
cnf(t16817,plain,
k = multiply(multiply(c,a),inverse(multiply(j,inverse(c)))),
inference(cp,[status(thm)],[t277,t16810]) ).
cnf(t91521,plain,
k = multiply(multiply(c,a),multiply(c,inverse(j))),
inference(step,[status(thm)],[t16817,t840]) ).
cnf(t17028,plain,
multiply(multiply(c,a),multiply(c,inverse(j))) = k,
inference(orient,[status(thm)],[t91521]) ).
cnf(t92928,plain,
k = multiply(multiply(b,c),inverse(c)),
inference(step,[status(thm)],[t92927,t17028]) ).
cnf(t92929,plain,
k = b,
inference(step,[status(thm)],[t92928,t277]) ).
cnf(t89813,plain,
b = k,
inference(orient,[status(thm)],[t92929]) ).
cnf(t105,axiom,
product(X1,inverse(X1),identity) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t407,plain,
product(X1,inverse(X1),identity) = true,
inference(orient,[status(thm)],[t105]) ).
cnf(goal_0,negated_conjecture,
product(k,inverse(b),identity) != true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
product(k,inverse(k),identity) != true,
inference(rw,[status(thm)],[goal_0,t89813]) ).
cnf(g0_1,plain,
true != true,
inference(rw,[status(thm)],[g0_0,t407]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP002-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n026.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Wed Sep 23 13:13:38 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 260.15/34.05 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 260.15/34.05 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------