%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP002-3 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n007.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 4.11s 0.92s
% Output : CNFRefutation 4.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 68
% Number of leaves : 15
% Syntax : Number of clauses : 373 ( 373 unt; 0 nHn; 259 RR)
% Number of literals : 373 ( 372 equ; 19 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 12 con; 0-2 aty)
% Number of variables : 131 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t3,axiom,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t3]) ).
cnf(t4,axiom,
sF0 = inverse(a),
introduced(definition) ).
cnf(t13,plain,
inverse(a) = sF0,
inference(orient,[status(thm)],[t4]) ).
cnf(t7,axiom,
sF3 = multiply(b,multiply(inverse(a),inverse(b))),
introduced(definition) ).
cnf(t2283,plain,
sF3 = multiply(b,multiply(sF0,inverse(b))),
inference(step,[status(thm)],[t7,t13]) ).
cnf(t5,axiom,
sF1 = inverse(b),
introduced(definition) ).
cnf(t14,plain,
inverse(b) = sF1,
inference(orient,[status(thm)],[t5]) ).
cnf(t2284,plain,
sF3 = multiply(b,multiply(sF0,sF1)),
inference(step,[status(thm)],[t2283,t14]) ).
cnf(t6,axiom,
sF2 = multiply(inverse(a),inverse(b)),
introduced(definition) ).
cnf(t2280,plain,
sF2 = multiply(sF0,inverse(b)),
inference(step,[status(thm)],[t6,t13]) ).
cnf(t2281,plain,
sF2 = multiply(sF0,sF1),
inference(step,[status(thm)],[t2280,t14]) ).
cnf(t28,plain,
multiply(sF0,sF1) = sF2,
inference(orient,[status(thm)],[t2281]) ).
cnf(t2285,plain,
sF3 = multiply(b,sF2),
inference(step,[status(thm)],[t2284,t28]) ).
cnf(t32,plain,
multiply(b,sF2) = sF3,
inference(orient,[status(thm)],[t2285]) ).
cnf(t33,plain,
multiply(b,multiply(sF2,X1)) = multiply(sF3,X1),
inference(cp,[status(thm)],[t22,t32]) ).
cnf(t55,plain,
multiply(b,multiply(sF2,X1)) = multiply(sF3,X1),
inference(orient,[status(thm)],[t33]) ).
cnf(t29,plain,
multiply(sF0,multiply(sF1,X1)) = multiply(sF2,X1),
inference(cp,[status(thm)],[t22,t28]) ).
cnf(t47,plain,
multiply(sF0,multiply(sF1,X1)) = multiply(sF2,X1),
inference(orient,[status(thm)],[t29]) ).
cnf(t1,axiom,
multiply(inverse(X1),X1) = identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t16,plain,
multiply(inverse(X1),X1) = identity,
inference(orient,[status(thm)],[t1]) ).
cnf(t18,plain,
identity = multiply(sF1,b),
inference(cp,[status(thm)],[t16,t14]) ).
cnf(t20,plain,
multiply(sF1,b) = identity,
inference(orient,[status(thm)],[t18]) ).
cnf(t25,plain,
multiply(sF1,multiply(b,X1)) = multiply(identity,X1),
inference(cp,[status(thm)],[t22,t20]) ).
cnf(t0,axiom,
multiply(identity,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t15,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t2286,plain,
multiply(sF1,multiply(b,X1)) = X1,
inference(step,[status(thm)],[t25,t15]) ).
cnf(t38,plain,
multiply(sF1,multiply(b,X1)) = X1,
inference(orient,[status(thm)],[t2286]) ).
cnf(t50,plain,
multiply(sF2,multiply(b,X1)) = multiply(sF0,X1),
inference(cp,[status(thm)],[t47,t38]) ).
cnf(t98,plain,
multiply(sF2,multiply(b,X1)) = multiply(sF0,X1),
inference(orient,[status(thm)],[t50]) ).
cnf(t101,plain,
multiply(sF3,multiply(b,X1)) = multiply(b,multiply(sF0,X1)),
inference(cp,[status(thm)],[t55,t98]) ).
cnf(t492,plain,
multiply(b,multiply(sF0,X1)) = multiply(sF3,multiply(b,X1)),
inference(orient,[status(thm)],[t101]) ).
cnf(t8,axiom,
sF4 = multiply(a,multiply(b,multiply(inverse(a),inverse(b)))),
introduced(definition) ).
cnf(t2289,plain,
sF4 = multiply(a,multiply(b,multiply(sF0,inverse(b)))),
inference(step,[status(thm)],[t8,t13]) ).
cnf(t2290,plain,
sF4 = multiply(a,multiply(b,multiply(sF0,sF1))),
inference(step,[status(thm)],[t2289,t14]) ).
cnf(t2291,plain,
sF4 = multiply(a,multiply(b,sF2)),
inference(step,[status(thm)],[t2290,t28]) ).
cnf(t2292,plain,
sF4 = multiply(a,sF3),
inference(step,[status(thm)],[t2291,t32]) ).
cnf(t65,plain,
multiply(a,sF3) = sF4,
inference(orient,[status(thm)],[t2292]) ).
cnf(t66,plain,
multiply(a,multiply(sF3,X1)) = multiply(sF4,X1),
inference(cp,[status(thm)],[t22,t65]) ).
cnf(t139,plain,
multiply(a,multiply(sF3,X1)) = multiply(sF4,X1),
inference(orient,[status(thm)],[t66]) ).
cnf(t23,plain,
multiply(inverse(X1),multiply(X1,X2)) = multiply(identity,X2),
inference(cp,[status(thm)],[t22,t16]) ).
cnf(t2361,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(step,[status(thm)],[t23,t15]) ).
cnf(t194,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(orient,[status(thm)],[t2361]) ).
cnf(t2,axiom,
multiply(X1,multiply(X1,X1)) = identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t21,plain,
multiply(X1,multiply(X1,X1)) = identity,
inference(orient,[status(thm)],[t2]) ).
cnf(t26,plain,
multiply(X1,multiply(X2,multiply(multiply(X1,X2),multiply(X1,X2)))) = identity,
inference(cp,[status(thm)],[t22,t21]) ).
cnf(t2364,plain,
multiply(X1,multiply(X2,multiply(X1,multiply(X2,multiply(X1,X2))))) = identity,
inference(step,[status(thm)],[t26,t22]) ).
cnf(t245,plain,
multiply(X1,multiply(X2,multiply(X1,multiply(X2,multiply(X1,X2))))) = identity,
inference(orient,[status(thm)],[t2364]) ).
cnf(t269,plain,
identity = multiply(X1,multiply(inverse(X1),multiply(X1,inverse(X1)))),
inference(cp,[status(thm)],[t245,t194]) ).
cnf(t2385,plain,
identity = multiply(X1,inverse(X1)),
inference(step,[status(thm)],[t269,t194]) ).
cnf(t409,plain,
multiply(X1,inverse(X1)) = identity,
inference(orient,[status(thm)],[t2385]) ).
cnf(t415,plain,
multiply(sF4,inverse(sF3)) = multiply(a,identity),
inference(cp,[status(thm)],[t139,t409]) ).
cnf(t27,plain,
multiply(X1,multiply(multiply(X1,X1),X2)) = multiply(identity,X2),
inference(cp,[status(thm)],[t22,t21]) ).
cnf(t2365,plain,
multiply(X1,multiply(X1,multiply(X1,X2))) = multiply(identity,X2),
inference(step,[status(thm)],[t27,t22]) ).
cnf(t2366,plain,
multiply(X1,multiply(X1,multiply(X1,X2))) = X2,
inference(step,[status(thm)],[t2365,t15]) ).
cnf(t311,plain,
multiply(X1,multiply(X1,multiply(X1,X2))) = X2,
inference(orient,[status(thm)],[t2366]) ).
cnf(t313,plain,
X1 = multiply(X1,identity),
inference(cp,[status(thm)],[t311,t21]) ).
cnf(t337,plain,
multiply(X1,identity) = X1,
inference(orient,[status(thm)],[t313]) ).
cnf(t2395,plain,
multiply(sF4,inverse(sF3)) = a,
inference(step,[status(thm)],[t415,t337]) ).
cnf(t456,plain,
multiply(sF4,inverse(sF3)) = a,
inference(orient,[status(thm)],[t2395]) ).
cnf(t458,plain,
inverse(sF3) = multiply(inverse(sF4),a),
inference(cp,[status(thm)],[t194,t456]) ).
cnf(t9,axiom,
sF5 = inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),
introduced(definition) ).
cnf(t2297,plain,
sF5 = inverse(multiply(a,multiply(b,multiply(sF0,inverse(b))))),
inference(step,[status(thm)],[t9,t13]) ).
cnf(t2298,plain,
sF5 = inverse(multiply(a,multiply(b,multiply(sF0,sF1)))),
inference(step,[status(thm)],[t2297,t14]) ).
cnf(t2299,plain,
sF5 = inverse(multiply(a,multiply(b,sF2))),
inference(step,[status(thm)],[t2298,t28]) ).
cnf(t2300,plain,
sF5 = inverse(multiply(a,sF3)),
inference(step,[status(thm)],[t2299,t32]) ).
cnf(t2301,plain,
sF5 = inverse(sF4),
inference(step,[status(thm)],[t2300,t65]) ).
cnf(t91,plain,
inverse(sF4) = sF5,
inference(orient,[status(thm)],[t2301]) ).
cnf(t2396,plain,
inverse(sF3) = multiply(sF5,a),
inference(step,[status(thm)],[t458,t91]) ).
cnf(t461,plain,
multiply(sF5,a) = inverse(sF3),
inference(orient,[status(thm)],[t2396]) ).
cnf(t462,plain,
multiply(sF5,multiply(a,X1)) = multiply(inverse(sF3),X1),
inference(cp,[status(thm)],[t22,t461]) ).
cnf(t1159,plain,
multiply(sF5,multiply(a,X1)) = multiply(inverse(sF3),X1),
inference(orient,[status(thm)],[t462]) ).
cnf(t40,plain,
sF2 = multiply(sF1,sF3),
inference(cp,[status(thm)],[t38,t32]) ).
cnf(t45,plain,
multiply(sF1,sF3) = sF2,
inference(orient,[status(thm)],[t40]) ).
cnf(t51,plain,
multiply(sF2,sF3) = multiply(sF0,sF2),
inference(cp,[status(thm)],[t47,t45]) ).
cnf(t53,plain,
multiply(sF2,sF3) = multiply(sF0,sF2),
inference(orient,[status(thm)],[t51]) ).
cnf(t54,plain,
multiply(sF2,multiply(sF3,X1)) = multiply(multiply(sF0,sF2),X1),
inference(cp,[status(thm)],[t22,t53]) ).
cnf(t2302,plain,
multiply(sF2,multiply(sF3,X1)) = multiply(sF0,multiply(sF2,X1)),
inference(step,[status(thm)],[t54,t22]) ).
cnf(t102,plain,
multiply(sF2,multiply(sF3,X1)) = multiply(sF0,multiply(sF2,X1)),
inference(orient,[status(thm)],[t2302]) ).
cnf(t251,plain,
identity = multiply(sF3,multiply(sF0,multiply(sF2,multiply(sF2,multiply(sF3,sF2))))),
inference(cp,[status(thm)],[t245,t102]) ).
cnf(t2546,plain,
identity = multiply(sF3,multiply(sF0,multiply(sF2,multiply(sF0,multiply(sF2,sF2))))),
inference(step,[status(thm)],[t251,t102]) ).
cnf(t417,plain,
inverse(X1) = multiply(X1,multiply(X1,identity)),
inference(cp,[status(thm)],[t311,t409]) ).
cnf(t2386,plain,
inverse(X1) = multiply(X1,X1),
inference(step,[status(thm)],[t417,t337]) ).
cnf(t418,plain,
multiply(X1,X1) = inverse(X1),
inference(orient,[status(thm)],[t2386]) ).
cnf(t2547,plain,
identity = multiply(sF3,multiply(sF0,multiply(sF2,multiply(sF0,inverse(sF2))))),
inference(step,[status(thm)],[t2546,t418]) ).
cnf(t17,plain,
identity = multiply(sF0,a),
inference(cp,[status(thm)],[t16,t13]) ).
cnf(t19,plain,
multiply(sF0,a) = identity,
inference(orient,[status(thm)],[t17]) ).
cnf(t24,plain,
multiply(sF0,multiply(a,X1)) = multiply(identity,X1),
inference(cp,[status(thm)],[t22,t19]) ).
cnf(t2282,plain,
multiply(sF0,multiply(a,X1)) = X1,
inference(step,[status(thm)],[t24,t15]) ).
cnf(t30,plain,
multiply(sF0,multiply(a,X1)) = X1,
inference(orient,[status(thm)],[t2282]) ).
cnf(t67,plain,
sF3 = multiply(sF0,sF4),
inference(cp,[status(thm)],[t30,t65]) ).
cnf(t70,plain,
multiply(sF0,sF4) = sF3,
inference(orient,[status(thm)],[t67]) ).
cnf(t71,plain,
multiply(sF0,multiply(sF4,X1)) = multiply(sF3,X1),
inference(cp,[status(thm)],[t22,t70]) ).
cnf(t142,plain,
multiply(sF0,multiply(sF4,X1)) = multiply(sF3,X1),
inference(orient,[status(thm)],[t71]) ).
cnf(t10,axiom,
sF6 = multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b)),
introduced(definition) ).
cnf(t2309,plain,
sF6 = multiply(inverse(multiply(a,multiply(b,multiply(sF0,inverse(b))))),inverse(b)),
inference(step,[status(thm)],[t10,t13]) ).
cnf(t2310,plain,
sF6 = multiply(inverse(multiply(a,multiply(b,multiply(sF0,sF1)))),inverse(b)),
inference(step,[status(thm)],[t2309,t14]) ).
cnf(t2311,plain,
sF6 = multiply(inverse(multiply(a,multiply(b,sF2))),inverse(b)),
inference(step,[status(thm)],[t2310,t28]) ).
cnf(t2312,plain,
sF6 = multiply(inverse(multiply(a,sF3)),inverse(b)),
inference(step,[status(thm)],[t2311,t32]) ).
cnf(t2313,plain,
sF6 = multiply(inverse(sF4),inverse(b)),
inference(step,[status(thm)],[t2312,t65]) ).
cnf(t2314,plain,
sF6 = multiply(sF5,inverse(b)),
inference(step,[status(thm)],[t2313,t91]) ).
cnf(t2315,plain,
sF6 = multiply(sF5,sF1),
inference(step,[status(thm)],[t2314,t14]) ).
cnf(t118,plain,
multiply(sF5,sF1) = sF6,
inference(orient,[status(thm)],[t2315]) ).
cnf(t215,plain,
sF1 = multiply(inverse(sF5),sF6),
inference(cp,[status(thm)],[t194,t118]) ).
cnf(t307,plain,
multiply(inverse(sF5),sF6) = sF1,
inference(orient,[status(thm)],[t215]) ).
cnf(t92,plain,
identity = multiply(sF5,sF4),
inference(cp,[status(thm)],[t16,t91]) ).
cnf(t93,plain,
multiply(sF5,sF4) = identity,
inference(orient,[status(thm)],[t92]) ).
cnf(t210,plain,
sF4 = multiply(inverse(sF5),identity),
inference(cp,[status(thm)],[t194,t93]) ).
cnf(t300,plain,
multiply(inverse(sF5),identity) = sF4,
inference(orient,[status(thm)],[t210]) ).
cnf(t2374,plain,
inverse(sF5) = sF4,
inference(step,[status(thm)],[t300,t337]) ).
cnf(t345,plain,
inverse(sF5) = sF4,
inference(rw,[status(thm)],[t2374]) ).
cnf(t348,plain,
inverse(sF5) = sF4,
inference(orient,[status(thm)],[t345]) ).
cnf(t2375,plain,
multiply(sF4,sF6) = sF1,
inference(step,[status(thm)],[t307,t348]) ).
cnf(t349,plain,
multiply(sF4,sF6) = sF1,
inference(rw,[status(thm)],[t2375]) ).
cnf(t361,plain,
multiply(sF4,sF6) = sF1,
inference(orient,[status(thm)],[t349]) ).
cnf(t362,plain,
multiply(sF4,multiply(sF6,X1)) = multiply(sF1,X1),
inference(cp,[status(thm)],[t22,t361]) ).
cnf(t993,plain,
multiply(sF4,multiply(sF6,X1)) = multiply(sF1,X1),
inference(orient,[status(thm)],[t362]) ).
cnf(t996,plain,
multiply(sF1,sF6) = multiply(sF4,inverse(sF6)),
inference(cp,[status(thm)],[t993,t418]) ).
cnf(t1027,plain,
multiply(sF4,inverse(sF6)) = multiply(sF1,sF6),
inference(orient,[status(thm)],[t996]) ).
cnf(t1028,plain,
multiply(sF3,inverse(sF6)) = multiply(sF0,multiply(sF1,sF6)),
inference(cp,[status(thm)],[t142,t1027]) ).
cnf(t2435,plain,
multiply(sF3,inverse(sF6)) = multiply(sF2,sF6),
inference(step,[status(thm)],[t1028,t47]) ).
cnf(t46,plain,
multiply(sF1,multiply(sF3,X1)) = multiply(sF2,X1),
inference(cp,[status(thm)],[t22,t45]) ).
cnf(t89,plain,
multiply(sF1,multiply(sF3,X1)) = multiply(sF2,X1),
inference(orient,[status(thm)],[t46]) ).
cnf(t363,plain,
multiply(sF3,sF6) = multiply(sF0,sF1),
inference(cp,[status(thm)],[t142,t361]) ).
cnf(t2382,plain,
multiply(sF3,sF6) = sF2,
inference(step,[status(thm)],[t363,t28]) ).
cnf(t374,plain,
multiply(sF3,sF6) = sF2,
inference(orient,[status(thm)],[t2382]) ).
cnf(t376,plain,
multiply(sF2,sF6) = multiply(sF1,sF2),
inference(cp,[status(thm)],[t89,t374]) ).
cnf(t399,plain,
multiply(sF2,sF6) = multiply(sF1,sF2),
inference(orient,[status(thm)],[t376]) ).
cnf(t2436,plain,
multiply(sF3,inverse(sF6)) = multiply(sF1,sF2),
inference(step,[status(thm)],[t2435,t399]) ).
cnf(t1041,plain,
multiply(sF3,inverse(sF6)) = multiply(sF1,sF2),
inference(orient,[status(thm)],[t2436]) ).
cnf(t1043,plain,
multiply(sF4,inverse(sF6)) = multiply(a,multiply(sF1,sF2)),
inference(cp,[status(thm)],[t139,t1041]) ).
cnf(t2437,plain,
multiply(sF1,sF6) = multiply(a,multiply(sF1,sF2)),
inference(step,[status(thm)],[t1043,t1027]) ).
cnf(t31,plain,
multiply(a,a) = multiply(sF0,identity),
inference(cp,[status(thm)],[t30,t21]) ).
cnf(t34,plain,
multiply(a,a) = multiply(sF0,identity),
inference(orient,[status(thm)],[t31]) ).
cnf(t36,plain,
multiply(a,multiply(a,X1)) = multiply(multiply(sF0,identity),X1),
inference(cp,[status(thm)],[t22,t34]) ).
cnf(t2287,plain,
multiply(a,multiply(a,X1)) = multiply(sF0,multiply(identity,X1)),
inference(step,[status(thm)],[t36,t22]) ).
cnf(t2288,plain,
multiply(a,multiply(a,X1)) = multiply(sF0,X1),
inference(step,[status(thm)],[t2287,t15]) ).
cnf(t61,plain,
multiply(a,multiply(a,X1)) = multiply(sF0,X1),
inference(orient,[status(thm)],[t2288]) ).
cnf(t35,plain,
identity = multiply(a,multiply(sF0,identity)),
inference(cp,[status(thm)],[t21,t34]) ).
cnf(t59,plain,
multiply(a,multiply(sF0,identity)) = identity,
inference(orient,[status(thm)],[t35]) ).
cnf(t60,plain,
multiply(a,multiply(multiply(sF0,identity),X1)) = multiply(identity,X1),
inference(cp,[status(thm)],[t22,t59]) ).
cnf(t2304,plain,
multiply(a,multiply(sF0,multiply(identity,X1))) = multiply(identity,X1),
inference(step,[status(thm)],[t60,t22]) ).
cnf(t2305,plain,
multiply(a,multiply(sF0,X1)) = multiply(identity,X1),
inference(step,[status(thm)],[t2304,t15]) ).
cnf(t2306,plain,
multiply(a,multiply(sF0,X1)) = X1,
inference(step,[status(thm)],[t2305,t15]) ).
cnf(t111,plain,
multiply(a,multiply(sF0,X1)) = X1,
inference(orient,[status(thm)],[t2306]) ).
cnf(t114,plain,
sF1 = multiply(a,sF2),
inference(cp,[status(thm)],[t111,t28]) ).
cnf(t120,plain,
multiply(a,sF2) = sF1,
inference(orient,[status(thm)],[t114]) ).
cnf(t121,plain,
multiply(sF0,sF2) = multiply(a,sF1),
inference(cp,[status(thm)],[t61,t120]) ).
cnf(t132,plain,
multiply(a,sF1) = multiply(sF0,sF2),
inference(orient,[status(thm)],[t121]) ).
cnf(t133,plain,
multiply(a,multiply(sF1,X1)) = multiply(multiply(sF0,sF2),X1),
inference(cp,[status(thm)],[t22,t132]) ).
cnf(t2405,plain,
multiply(a,multiply(sF1,X1)) = multiply(sF0,multiply(sF2,X1)),
inference(step,[status(thm)],[t133,t22]) ).
cnf(t568,plain,
multiply(a,multiply(sF1,X1)) = multiply(sF0,multiply(sF2,X1)),
inference(orient,[status(thm)],[t2405]) ).
cnf(t2438,plain,
multiply(sF1,sF6) = multiply(sF0,multiply(sF2,sF2)),
inference(step,[status(thm)],[t2437,t568]) ).
cnf(t2439,plain,
multiply(sF1,sF6) = multiply(sF0,inverse(sF2)),
inference(step,[status(thm)],[t2438,t418]) ).
cnf(t1054,plain,
multiply(sF0,inverse(sF2)) = multiply(sF1,sF6),
inference(orient,[status(thm)],[t2439]) ).
cnf(t2548,plain,
identity = multiply(sF3,multiply(sF0,multiply(sF2,multiply(sF1,sF6)))),
inference(step,[status(thm)],[t2547,t1054]) ).
cnf(t39,plain,
multiply(b,b) = multiply(sF1,identity),
inference(cp,[status(thm)],[t38,t21]) ).
cnf(t41,plain,
multiply(b,b) = multiply(sF1,identity),
inference(orient,[status(thm)],[t39]) ).
cnf(t43,plain,
multiply(b,multiply(b,X1)) = multiply(multiply(sF1,identity),X1),
inference(cp,[status(thm)],[t22,t41]) ).
cnf(t2294,plain,
multiply(b,multiply(b,X1)) = multiply(sF1,multiply(identity,X1)),
inference(step,[status(thm)],[t43,t22]) ).
cnf(t2295,plain,
multiply(b,multiply(b,X1)) = multiply(sF1,X1),
inference(step,[status(thm)],[t2294,t15]) ).
cnf(t78,plain,
multiply(b,multiply(b,X1)) = multiply(sF1,X1),
inference(orient,[status(thm)],[t2295]) ).
cnf(t99,plain,
multiply(sF0,multiply(b,X1)) = multiply(sF2,multiply(sF1,X1)),
inference(cp,[status(thm)],[t98,t78]) ).
cnf(t468,plain,
multiply(sF2,multiply(sF1,X1)) = multiply(sF0,multiply(b,X1)),
inference(orient,[status(thm)],[t99]) ).
cnf(t2549,plain,
identity = multiply(sF3,multiply(sF0,multiply(sF0,multiply(b,sF6)))),
inference(step,[status(thm)],[t2548,t468]) ).
cnf(t336,plain,
multiply(X1,multiply(X1,X2)) = multiply(inverse(X1),X2),
inference(cp,[status(thm)],[t194,t311]) ).
cnf(t749,plain,
multiply(X1,multiply(X1,X2)) = multiply(inverse(X1),X2),
inference(orient,[status(thm)],[t336]) ).
cnf(t2550,plain,
identity = multiply(sF3,multiply(inverse(sF0),multiply(b,sF6))),
inference(step,[status(thm)],[t2549,t749]) ).
cnf(t202,plain,
multiply(a,X1) = multiply(inverse(sF0),X1),
inference(cp,[status(thm)],[t194,t30]) ).
cnf(t240,plain,
multiply(inverse(sF0),X1) = multiply(a,X1),
inference(orient,[status(thm)],[t202]) ).
cnf(t346,plain,
inverse(sF0) = multiply(a,identity),
inference(cp,[status(thm)],[t337,t240]) ).
cnf(t2376,plain,
inverse(sF0) = a,
inference(step,[status(thm)],[t346,t337]) ).
cnf(t352,plain,
inverse(sF0) = a,
inference(orient,[status(thm)],[t2376]) ).
cnf(t2551,plain,
identity = multiply(sF3,multiply(a,multiply(b,sF6))),
inference(step,[status(thm)],[t2550,t352]) ).
cnf(t11,axiom,
sF7 = multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b))),
introduced(definition) ).
cnf(t2325,plain,
sF7 = multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(sF0,inverse(b))))),inverse(b))),
inference(step,[status(thm)],[t11,t13]) ).
cnf(t2326,plain,
sF7 = multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(sF0,sF1)))),inverse(b))),
inference(step,[status(thm)],[t2325,t14]) ).
cnf(t2327,plain,
sF7 = multiply(b,multiply(inverse(multiply(a,multiply(b,sF2))),inverse(b))),
inference(step,[status(thm)],[t2326,t28]) ).
cnf(t2328,plain,
sF7 = multiply(b,multiply(inverse(multiply(a,sF3)),inverse(b))),
inference(step,[status(thm)],[t2327,t32]) ).
cnf(t2329,plain,
sF7 = multiply(b,multiply(inverse(sF4),inverse(b))),
inference(step,[status(thm)],[t2328,t65]) ).
cnf(t2330,plain,
sF7 = multiply(b,multiply(sF5,inverse(b))),
inference(step,[status(thm)],[t2329,t91]) ).
cnf(t2331,plain,
sF7 = multiply(b,multiply(sF5,sF1)),
inference(step,[status(thm)],[t2330,t14]) ).
cnf(t2332,plain,
sF7 = multiply(b,sF6),
inference(step,[status(thm)],[t2331,t118]) ).
cnf(t146,plain,
multiply(b,sF6) = sF7,
inference(orient,[status(thm)],[t2332]) ).
cnf(t2552,plain,
identity = multiply(sF3,multiply(a,sF7)),
inference(step,[status(thm)],[t2551,t146]) ).
cnf(t2104,plain,
multiply(sF3,multiply(a,sF7)) = identity,
inference(orient,[status(thm)],[t2552]) ).
cnf(t2110,plain,
multiply(a,sF7) = multiply(inverse(sF3),identity),
inference(cp,[status(thm)],[t194,t2104]) ).
cnf(t2553,plain,
multiply(a,sF7) = inverse(sF3),
inference(step,[status(thm)],[t2110,t337]) ).
cnf(t2116,plain,
multiply(a,sF7) = inverse(sF3),
inference(orient,[status(thm)],[t2553]) ).
cnf(t2126,plain,
multiply(inverse(sF3),sF7) = multiply(sF5,inverse(sF3)),
inference(cp,[status(thm)],[t1159,t2116]) ).
cnf(t12,axiom,
sF8 = multiply(multiply(a,multiply(b,multiply(inverse(a),inverse(b)))),multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b)))),
introduced(definition) ).
cnf(t2341,plain,
sF8 = multiply(a,multiply(multiply(b,multiply(inverse(a),inverse(b))),multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b))))),
inference(step,[status(thm)],[t12,t22]) ).
cnf(t2342,plain,
sF8 = multiply(a,multiply(b,multiply(multiply(inverse(a),inverse(b)),multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b)))))),
inference(step,[status(thm)],[t2341,t22]) ).
cnf(t2343,plain,
sF8 = multiply(a,multiply(b,multiply(inverse(a),multiply(inverse(b),multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b))))))),
inference(step,[status(thm)],[t2342,t22]) ).
cnf(t2344,plain,
sF8 = multiply(a,multiply(b,multiply(sF0,multiply(inverse(b),multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b))))))),
inference(step,[status(thm)],[t2343,t13]) ).
cnf(t2345,plain,
sF8 = multiply(a,multiply(b,multiply(sF0,multiply(sF1,multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b))))))),
inference(step,[status(thm)],[t2344,t14]) ).
cnf(t2346,plain,
sF8 = multiply(a,multiply(b,multiply(sF2,multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b)))))),
inference(step,[status(thm)],[t2345,t47]) ).
cnf(t2347,plain,
sF8 = multiply(a,multiply(sF3,multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b))))),
inference(step,[status(thm)],[t2346,t55]) ).
cnf(t2348,plain,
sF8 = multiply(sF4,multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b)))),
inference(step,[status(thm)],[t2347,t139]) ).
cnf(t2349,plain,
sF8 = multiply(sF4,multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(sF0,inverse(b))))),inverse(b)))),
inference(step,[status(thm)],[t2348,t13]) ).
cnf(t2350,plain,
sF8 = multiply(sF4,multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(sF0,sF1)))),inverse(b)))),
inference(step,[status(thm)],[t2349,t14]) ).
cnf(t2351,plain,
sF8 = multiply(sF4,multiply(b,multiply(inverse(multiply(a,multiply(b,sF2))),inverse(b)))),
inference(step,[status(thm)],[t2350,t28]) ).
cnf(t2352,plain,
sF8 = multiply(sF4,multiply(b,multiply(inverse(multiply(a,sF3)),inverse(b)))),
inference(step,[status(thm)],[t2351,t32]) ).
cnf(t2353,plain,
sF8 = multiply(sF4,multiply(b,multiply(inverse(sF4),inverse(b)))),
inference(step,[status(thm)],[t2352,t65]) ).
cnf(t2354,plain,
sF8 = multiply(sF4,multiply(b,multiply(sF5,inverse(b)))),
inference(step,[status(thm)],[t2353,t91]) ).
cnf(t2355,plain,
sF8 = multiply(sF4,multiply(b,multiply(sF5,sF1))),
inference(step,[status(thm)],[t2354,t14]) ).
cnf(t2356,plain,
sF8 = multiply(sF4,multiply(b,sF6)),
inference(step,[status(thm)],[t2355,t118]) ).
cnf(t2357,plain,
sF8 = multiply(sF4,sF7),
inference(step,[status(thm)],[t2356,t146]) ).
cnf(t175,plain,
multiply(sF4,sF7) = sF8,
inference(orient,[status(thm)],[t2357]) ).
cnf(t177,plain,
multiply(sF3,sF7) = multiply(sF0,sF8),
inference(cp,[status(thm)],[t142,t175]) ).
cnf(t182,plain,
multiply(sF3,sF7) = multiply(sF0,sF8),
inference(orient,[status(thm)],[t177]) ).
cnf(t762,plain,
multiply(inverse(sF3),sF7) = multiply(sF3,multiply(sF0,sF8)),
inference(cp,[status(thm)],[t749,t182]) ).
cnf(t185,plain,
multiply(sF0,multiply(sF2,sF7)) = multiply(sF2,multiply(sF0,sF8)),
inference(cp,[status(thm)],[t102,t182]) ).
cnf(t150,plain,
multiply(sF0,sF6) = multiply(sF2,sF7),
inference(cp,[status(thm)],[t98,t146]) ).
cnf(t157,plain,
multiply(sF2,sF7) = multiply(sF0,sF6),
inference(orient,[status(thm)],[t150]) ).
cnf(t2414,plain,
multiply(sF0,multiply(sF0,sF6)) = multiply(sF2,multiply(sF0,sF8)),
inference(step,[status(thm)],[t185,t157]) ).
cnf(t64,plain,
multiply(a,X1) = multiply(sF0,multiply(sF0,X1)),
inference(cp,[status(thm)],[t30,t61]) ).
cnf(t138,plain,
multiply(sF0,multiply(sF0,X1)) = multiply(a,X1),
inference(orient,[status(thm)],[t64]) ).
cnf(t2415,plain,
multiply(a,sF6) = multiply(sF2,multiply(sF0,sF8)),
inference(step,[status(thm)],[t2414,t138]) ).
cnf(t686,plain,
multiply(sF2,multiply(sF0,sF8)) = multiply(a,sF6),
inference(orient,[status(thm)],[t2415]) ).
cnf(t687,plain,
multiply(sF3,multiply(sF0,sF8)) = multiply(b,multiply(a,sF6)),
inference(cp,[status(thm)],[t55,t686]) ).
cnf(t42,plain,
identity = multiply(b,multiply(sF1,identity)),
inference(cp,[status(thm)],[t21,t41]) ).
cnf(t76,plain,
multiply(b,multiply(sF1,identity)) = identity,
inference(orient,[status(thm)],[t42]) ).
cnf(t77,plain,
multiply(b,multiply(multiply(sF1,identity),X1)) = multiply(identity,X1),
inference(cp,[status(thm)],[t22,t76]) ).
cnf(t2333,plain,
multiply(b,multiply(sF1,multiply(identity,X1))) = multiply(identity,X1),
inference(step,[status(thm)],[t77,t22]) ).
cnf(t2334,plain,
multiply(b,multiply(sF1,X1)) = multiply(identity,X1),
inference(step,[status(thm)],[t2333,t15]) ).
cnf(t2335,plain,
multiply(b,multiply(sF1,X1)) = X1,
inference(step,[status(thm)],[t2334,t15]) ).
cnf(t160,plain,
multiply(b,multiply(sF1,X1)) = X1,
inference(orient,[status(thm)],[t2335]) ).
cnf(t115,plain,
multiply(sF1,X1) = multiply(a,multiply(sF2,X1)),
inference(cp,[status(thm)],[t111,t47]) ).
cnf(t501,plain,
multiply(a,multiply(sF2,X1)) = multiply(sF1,X1),
inference(orient,[status(thm)],[t115]) ).
cnf(t506,plain,
multiply(sF1,inverse(sF2)) = multiply(a,identity),
inference(cp,[status(thm)],[t501,t409]) ).
cnf(t2398,plain,
multiply(sF1,inverse(sF2)) = a,
inference(step,[status(thm)],[t506,t337]) ).
cnf(t508,plain,
multiply(sF1,inverse(sF2)) = a,
inference(orient,[status(thm)],[t2398]) ).
cnf(t510,plain,
inverse(sF2) = multiply(b,a),
inference(cp,[status(thm)],[t160,t508]) ).
cnf(t514,plain,
multiply(b,a) = inverse(sF2),
inference(orient,[status(thm)],[t510]) ).
cnf(t515,plain,
multiply(b,multiply(a,X1)) = multiply(inverse(sF2),X1),
inference(cp,[status(thm)],[t22,t514]) ).
cnf(t1179,plain,
multiply(b,multiply(a,X1)) = multiply(inverse(sF2),X1),
inference(orient,[status(thm)],[t515]) ).
cnf(t2458,plain,
multiply(sF3,multiply(sF0,sF8)) = multiply(inverse(sF2),sF6),
inference(step,[status(thm)],[t687,t1179]) ).
cnf(t768,plain,
multiply(inverse(sF2),sF6) = multiply(sF2,multiply(sF1,sF2)),
inference(cp,[status(thm)],[t749,t399]) ).
cnf(t2426,plain,
multiply(inverse(sF2),sF6) = multiply(sF0,multiply(b,sF2)),
inference(step,[status(thm)],[t768,t468]) ).
cnf(t2427,plain,
multiply(inverse(sF2),sF6) = multiply(sF0,sF3),
inference(step,[status(thm)],[t2426,t32]) ).
cnf(t972,plain,
multiply(inverse(sF2),sF6) = multiply(sF0,sF3),
inference(orient,[status(thm)],[t2427]) ).
cnf(t2459,plain,
multiply(sF3,multiply(sF0,sF8)) = multiply(sF0,sF3),
inference(step,[status(thm)],[t2458,t972]) ).
cnf(t1320,plain,
multiply(sF3,multiply(sF0,sF8)) = multiply(sF0,sF3),
inference(orient,[status(thm)],[t2459]) ).
cnf(t2467,plain,
multiply(inverse(sF3),sF7) = multiply(sF0,sF3),
inference(step,[status(thm)],[t762,t1320]) ).
cnf(t1377,plain,
multiply(inverse(sF3),sF7) = multiply(sF0,sF3),
inference(orient,[status(thm)],[t2467]) ).
cnf(t2569,plain,
multiply(sF0,sF3) = multiply(sF5,inverse(sF3)),
inference(step,[status(thm)],[t2126,t1377]) ).
cnf(t771,plain,
multiply(inverse(sF4),inverse(sF3)) = multiply(sF4,a),
inference(cp,[status(thm)],[t749,t456]) ).
cnf(t2428,plain,
multiply(sF5,inverse(sF3)) = multiply(sF4,a),
inference(step,[status(thm)],[t771,t91]) ).
cnf(t979,plain,
multiply(sF5,inverse(sF3)) = multiply(sF4,a),
inference(orient,[status(thm)],[t2428]) ).
cnf(t2570,plain,
multiply(sF0,sF3) = multiply(sF4,a),
inference(step,[status(thm)],[t2569,t979]) ).
cnf(t2160,plain,
multiply(sF4,a) = multiply(sF0,sF3),
inference(orient,[status(thm)],[t2570]) ).
cnf(t2167,plain,
identity = multiply(sF4,multiply(a,multiply(sF4,multiply(a,multiply(sF0,sF3))))),
inference(cp,[status(thm)],[t245,t2160]) ).
cnf(t68,plain,
multiply(sF0,sF3) = multiply(a,sF4),
inference(cp,[status(thm)],[t61,t65]) ).
cnf(t72,plain,
multiply(a,sF4) = multiply(sF0,sF3),
inference(orient,[status(thm)],[t68]) ).
cnf(t73,plain,
multiply(a,multiply(sF4,X1)) = multiply(multiply(sF0,sF3),X1),
inference(cp,[status(thm)],[t22,t72]) ).
cnf(t2324,plain,
multiply(a,multiply(sF4,X1)) = multiply(sF0,multiply(sF3,X1)),
inference(step,[status(thm)],[t73,t22]) ).
cnf(t144,plain,
multiply(a,multiply(sF4,X1)) = multiply(sF0,multiply(sF3,X1)),
inference(orient,[status(thm)],[t2324]) ).
cnf(t2573,plain,
identity = multiply(sF4,multiply(sF0,multiply(sF3,multiply(a,multiply(sF0,sF3))))),
inference(step,[status(thm)],[t2167,t144]) ).
cnf(t2574,plain,
identity = multiply(sF4,multiply(sF0,multiply(sF3,sF3))),
inference(step,[status(thm)],[t2573,t111]) ).
cnf(t2575,plain,
identity = multiply(sF4,multiply(sF0,inverse(sF3))),
inference(step,[status(thm)],[t2574,t418]) ).
cnf(t375,plain,
multiply(sF3,multiply(sF6,X1)) = multiply(sF2,X1),
inference(cp,[status(thm)],[t22,t374]) ).
cnf(t1059,plain,
multiply(sF3,multiply(sF6,X1)) = multiply(sF2,X1),
inference(orient,[status(thm)],[t375]) ).
cnf(t148,plain,
sF6 = multiply(sF1,sF7),
inference(cp,[status(thm)],[t38,t146]) ).
cnf(t151,plain,
multiply(sF1,sF7) = sF6,
inference(orient,[status(thm)],[t148]) ).
cnf(t152,plain,
multiply(sF1,multiply(sF7,X1)) = multiply(sF6,X1),
inference(cp,[status(thm)],[t22,t151]) ).
cnf(t608,plain,
multiply(sF1,multiply(sF7,X1)) = multiply(sF6,X1),
inference(orient,[status(thm)],[t152]) ).
cnf(t611,plain,
multiply(sF6,inverse(sF7)) = multiply(sF1,identity),
inference(cp,[status(thm)],[t608,t409]) ).
cnf(t2407,plain,
multiply(sF6,inverse(sF7)) = sF1,
inference(step,[status(thm)],[t611,t337]) ).
cnf(t616,plain,
multiply(sF6,inverse(sF7)) = sF1,
inference(orient,[status(thm)],[t2407]) ).
cnf(t1063,plain,
multiply(sF2,inverse(sF7)) = multiply(sF3,sF1),
inference(cp,[status(thm)],[t1059,t616]) ).
cnf(t1071,plain,
multiply(sF2,inverse(sF7)) = multiply(sF3,sF1),
inference(orient,[status(thm)],[t1063]) ).
cnf(t1073,plain,
multiply(sF3,inverse(sF7)) = multiply(b,multiply(sF3,sF1)),
inference(cp,[status(thm)],[t55,t1071]) ).
cnf(t81,plain,
multiply(sF1,multiply(sF2,X1)) = multiply(b,multiply(sF3,X1)),
inference(cp,[status(thm)],[t78,t55]) ).
cnf(t189,plain,
multiply(b,multiply(sF3,X1)) = multiply(sF1,multiply(sF2,X1)),
inference(orient,[status(thm)],[t81]) ).
cnf(t2497,plain,
multiply(sF3,inverse(sF7)) = multiply(sF1,multiply(sF2,sF1)),
inference(step,[status(thm)],[t1073,t189]) ).
cnf(t162,plain,
multiply(sF1,sF1) = multiply(b,identity),
inference(cp,[status(thm)],[t160,t21]) ).
cnf(t79,plain,
multiply(sF1,multiply(b,b)) = multiply(b,identity),
inference(cp,[status(thm)],[t78,t21]) ).
cnf(t2296,plain,
b = multiply(b,identity),
inference(step,[status(thm)],[t79,t38]) ).
cnf(t84,plain,
multiply(b,identity) = b,
inference(orient,[status(thm)],[t2296]) ).
cnf(t2337,plain,
multiply(sF1,sF1) = b,
inference(step,[status(thm)],[t162,t84]) ).
cnf(t163,plain,
multiply(sF1,sF1) = b,
inference(orient,[status(thm)],[t2337]) ).
cnf(t165,plain,
multiply(sF2,sF1) = multiply(sF0,b),
inference(cp,[status(thm)],[t47,t163]) ).
cnf(t167,plain,
multiply(sF2,sF1) = multiply(sF0,b),
inference(orient,[status(thm)],[t165]) ).
cnf(t2498,plain,
multiply(sF3,inverse(sF7)) = multiply(sF1,multiply(sF0,b)),
inference(step,[status(thm)],[t2497,t167]) ).
cnf(t1861,plain,
multiply(sF1,multiply(sF0,b)) = multiply(sF3,inverse(sF7)),
inference(orient,[status(thm)],[t2498]) ).
cnf(t1866,plain,
multiply(sF0,multiply(sF2,multiply(sF0,b))) = multiply(a,multiply(sF3,inverse(sF7))),
inference(cp,[status(thm)],[t568,t1861]) ).
cnf(t761,plain,
multiply(inverse(sF2),sF1) = multiply(sF2,multiply(sF0,b)),
inference(cp,[status(thm)],[t749,t167]) ).
cnf(t413,plain,
multiply(sF2,inverse(sF3)) = multiply(sF1,identity),
inference(cp,[status(thm)],[t89,t409]) ).
cnf(t2394,plain,
multiply(sF2,inverse(sF3)) = sF1,
inference(step,[status(thm)],[t413,t337]) ).
cnf(t451,plain,
multiply(sF2,inverse(sF3)) = sF1,
inference(orient,[status(thm)],[t2394]) ).
cnf(t453,plain,
inverse(sF3) = multiply(inverse(sF2),sF1),
inference(cp,[status(thm)],[t194,t451]) ).
cnf(t488,plain,
multiply(inverse(sF2),sF1) = inverse(sF3),
inference(orient,[status(thm)],[t453]) ).
cnf(t2466,plain,
inverse(sF3) = multiply(sF2,multiply(sF0,b)),
inference(step,[status(thm)],[t761,t488]) ).
cnf(t1371,plain,
multiply(sF2,multiply(sF0,b)) = inverse(sF3),
inference(orient,[status(thm)],[t2466]) ).
cnf(t2499,plain,
multiply(sF0,inverse(sF3)) = multiply(a,multiply(sF3,inverse(sF7))),
inference(step,[status(thm)],[t1866,t1371]) ).
cnf(t2500,plain,
multiply(sF0,inverse(sF3)) = multiply(sF4,inverse(sF7)),
inference(step,[status(thm)],[t2499,t139]) ).
cnf(t176,plain,
multiply(sF4,multiply(sF7,X1)) = multiply(sF8,X1),
inference(cp,[status(thm)],[t22,t175]) ).
cnf(t642,plain,
multiply(sF4,multiply(sF7,X1)) = multiply(sF8,X1),
inference(orient,[status(thm)],[t176]) ).
cnf(t646,plain,
multiply(sF8,sF7) = multiply(sF4,inverse(sF7)),
inference(cp,[status(thm)],[t642,t418]) ).
cnf(t656,plain,
multiply(sF4,inverse(sF7)) = multiply(sF8,sF7),
inference(orient,[status(thm)],[t646]) ).
cnf(t2501,plain,
multiply(sF0,inverse(sF3)) = multiply(sF8,sF7),
inference(step,[status(thm)],[t2500,t656]) ).
cnf(t1871,plain,
multiply(sF0,inverse(sF3)) = multiply(sF8,sF7),
inference(orient,[status(thm)],[t2501]) ).
cnf(t2121,plain,
sF7 = multiply(sF0,inverse(sF3)),
inference(cp,[status(thm)],[t30,t2116]) ).
cnf(t2554,plain,
sF7 = multiply(sF8,sF7),
inference(step,[status(thm)],[t2121,t1871]) ).
cnf(t2129,plain,
multiply(sF8,sF7) = sF7,
inference(orient,[status(thm)],[t2554]) ).
cnf(t2558,plain,
multiply(sF0,inverse(sF3)) = sF7,
inference(step,[status(thm)],[t1871,t2129]) ).
cnf(t2134,plain,
multiply(sF0,inverse(sF3)) = sF7,
inference(orient,[status(thm)],[t2558]) ).
cnf(t2576,plain,
identity = multiply(sF4,sF7),
inference(step,[status(thm)],[t2575,t2134]) ).
cnf(t2577,plain,
identity = sF8,
inference(step,[status(thm)],[t2576,t175]) ).
cnf(t2173,plain,
identity = sF8,
inference(orient,[status(thm)],[t2577]) ).
cnf(t2596,plain,
multiply(X1,inverse(X1)) = sF8,
inference(step,[status(thm)],[t409,t2173]) ).
cnf(t2193,plain,
multiply(X1,inverse(X1)) = sF8,
inference(orient,[status(thm)],[t2596]) ).
cnf(t222,plain,
sF7 = multiply(inverse(sF4),sF8),
inference(cp,[status(thm)],[t194,t175]) ).
cnf(t2362,plain,
sF7 = multiply(sF5,sF8),
inference(step,[status(thm)],[t222,t91]) ).
cnf(t226,plain,
multiply(sF5,sF8) = sF7,
inference(orient,[status(thm)],[t2362]) ).
cnf(t227,plain,
multiply(sF5,multiply(sF8,X1)) = multiply(sF7,X1),
inference(cp,[status(thm)],[t22,t226]) ).
cnf(t696,plain,
multiply(sF5,multiply(sF8,X1)) = multiply(sF7,X1),
inference(orient,[status(thm)],[t227]) ).
cnf(t2139,plain,
multiply(sF7,sF7) = multiply(sF5,sF7),
inference(cp,[status(thm)],[t696,t2129]) ).
cnf(t2611,plain,
inverse(sF7) = multiply(sF5,sF7),
inference(step,[status(thm)],[t2139,t418]) ).
cnf(t324,plain,
sF7 = multiply(sF4,multiply(sF4,sF8)),
inference(cp,[status(thm)],[t311,t175]) ).
cnf(t741,plain,
multiply(sF4,multiply(sF4,sF8)) = sF7,
inference(orient,[status(thm)],[t324]) ).
cnf(t744,plain,
multiply(sF4,sF8) = multiply(inverse(sF4),sF7),
inference(cp,[status(thm)],[t194,t741]) ).
cnf(t2424,plain,
multiply(sF4,sF8) = multiply(sF5,sF7),
inference(step,[status(thm)],[t744,t91]) ).
cnf(t746,plain,
multiply(sF5,sF7) = multiply(sF4,sF8),
inference(orient,[status(thm)],[t2424]) ).
cnf(t2612,plain,
inverse(sF7) = multiply(sF4,sF8),
inference(step,[status(thm)],[t2611,t746]) ).
cnf(t2212,plain,
multiply(sF4,sF8) = inverse(sF7),
inference(orient,[status(thm)],[t2612]) ).
cnf(t645,plain,
multiply(sF8,inverse(sF7)) = multiply(sF4,identity),
inference(cp,[status(thm)],[t642,t409]) ).
cnf(t2411,plain,
multiply(sF8,inverse(sF7)) = sF4,
inference(step,[status(thm)],[t645,t337]) ).
cnf(t651,plain,
multiply(sF8,inverse(sF7)) = sF4,
inference(orient,[status(thm)],[t2411]) ).
cnf(t2578,plain,
multiply(sF8,X1) = X1,
inference(step,[status(thm)],[t15,t2173]) ).
cnf(t2174,plain,
multiply(sF8,X1) = X1,
inference(rw,[status(thm)],[t2578]) ).
cnf(t2236,plain,
multiply(sF8,X1) = X1,
inference(orient,[status(thm)],[t2174]) ).
cnf(t2620,plain,
inverse(sF7) = sF4,
inference(step,[status(thm)],[t651,t2236]) ).
cnf(t2239,plain,
inverse(sF7) = sF4,
inference(rw,[status(thm)],[t2620]) ).
cnf(t2255,plain,
inverse(sF7) = sF4,
inference(orient,[status(thm)],[t2239]) ).
cnf(t2646,plain,
multiply(sF4,sF8) = sF4,
inference(step,[status(thm)],[t2212,t2255]) ).
cnf(t2276,plain,
multiply(sF4,sF8) = sF4,
inference(orient,[status(thm)],[t2646]) ).
cnf(t147,plain,
multiply(b,multiply(sF6,X1)) = multiply(sF7,X1),
inference(cp,[status(thm)],[t22,t146]) ).
cnf(t571,plain,
multiply(b,multiply(sF6,X1)) = multiply(sF7,X1),
inference(orient,[status(thm)],[t147]) ).
cnf(t119,plain,
multiply(sF5,multiply(sF1,X1)) = multiply(sF6,X1),
inference(cp,[status(thm)],[t22,t118]) ).
cnf(t529,plain,
multiply(sF5,multiply(sF1,X1)) = multiply(sF6,X1),
inference(orient,[status(thm)],[t119]) ).
cnf(t530,plain,
multiply(sF6,b) = multiply(sF5,identity),
inference(cp,[status(thm)],[t529,t20]) ).
cnf(t2402,plain,
multiply(sF6,b) = sF5,
inference(step,[status(thm)],[t530,t337]) ).
cnf(t542,plain,
multiply(sF6,b) = sF5,
inference(orient,[status(thm)],[t2402]) ).
cnf(t576,plain,
multiply(sF7,b) = multiply(b,sF5),
inference(cp,[status(thm)],[t571,t542]) ).
cnf(t582,plain,
multiply(b,sF5) = multiply(sF7,b),
inference(orient,[status(thm)],[t576]) ).
cnf(t583,plain,
multiply(b,multiply(sF5,X1)) = multiply(multiply(sF7,b),X1),
inference(cp,[status(thm)],[t22,t582]) ).
cnf(t2457,plain,
multiply(b,multiply(sF5,X1)) = multiply(sF7,multiply(b,X1)),
inference(step,[status(thm)],[t583,t22]) ).
cnf(t1292,plain,
multiply(b,multiply(sF5,X1)) = multiply(sF7,multiply(b,X1)),
inference(orient,[status(thm)],[t2457]) ).
cnf(t2618,plain,
multiply(sF4,multiply(sF7,X1)) = X1,
inference(step,[status(thm)],[t642,t2236]) ).
cnf(t2237,plain,
multiply(sF4,multiply(sF7,X1)) = X1,
inference(orient,[status(thm)],[t2618]) ).
cnf(u0,negated_conjecture,
commutator(commutator(a,b),b) != identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
commutator(X,Y) = multiply(X,multiply(Y,multiply(inverse(X),inverse(Y)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
multiply(multiply(a,multiply(b,multiply(inverse(a),inverse(b)))),multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b)))) != identity,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(g0_0,plain,
multiply(a,multiply(multiply(b,multiply(inverse(a),inverse(b))),multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b))))) != identity,
inference(rw,[status(thm)],[goal_0,t22]) ).
cnf(g0_1,plain,
multiply(a,multiply(b,multiply(multiply(inverse(a),inverse(b)),multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b)))))) != identity,
inference(rw,[status(thm)],[g0_0,t22]) ).
cnf(g0_2,plain,
multiply(a,multiply(b,multiply(inverse(a),multiply(inverse(b),multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b))))))) != identity,
inference(rw,[status(thm)],[g0_1,t22]) ).
cnf(g0_3,plain,
multiply(a,multiply(b,multiply(sF0,multiply(inverse(b),multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b))))))) != identity,
inference(rw,[status(thm)],[g0_2,t13]) ).
cnf(g0_4,plain,
multiply(a,multiply(sF3,multiply(b,multiply(inverse(b),multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b))))))) != identity,
inference(rw,[status(thm)],[g0_3,t492]) ).
cnf(g0_5,plain,
multiply(sF4,multiply(b,multiply(inverse(b),multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b)))))) != identity,
inference(rw,[status(thm)],[g0_4,t139]) ).
cnf(g0_6,plain,
multiply(sF4,multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(inverse(a),inverse(b))))),inverse(b)))) != identity,
inference(rw,[status(thm)],[g0_5,t194]) ).
cnf(g0_7,plain,
multiply(sF4,multiply(b,multiply(inverse(multiply(a,multiply(b,multiply(sF0,inverse(b))))),inverse(b)))) != identity,
inference(rw,[status(thm)],[g0_6,t13]) ).
cnf(g0_8,plain,
multiply(sF4,multiply(b,multiply(inverse(multiply(a,multiply(sF3,multiply(b,inverse(b))))),inverse(b)))) != identity,
inference(rw,[status(thm)],[g0_7,t492]) ).
cnf(g0_9,plain,
multiply(sF4,multiply(b,multiply(inverse(multiply(sF4,multiply(b,inverse(b)))),inverse(b)))) != identity,
inference(rw,[status(thm)],[g0_8,t139]) ).
cnf(g0_10,plain,
multiply(sF4,multiply(b,multiply(inverse(multiply(sF4,sF8)),inverse(b)))) != identity,
inference(rw,[status(thm)],[g0_9,t2193]) ).
cnf(g0_11,plain,
multiply(sF4,multiply(b,multiply(inverse(sF4),inverse(b)))) != identity,
inference(rw,[status(thm)],[g0_10,t2276]) ).
cnf(g0_12,plain,
multiply(sF4,multiply(b,multiply(sF5,inverse(b)))) != identity,
inference(rw,[status(thm)],[g0_11,t91]) ).
cnf(g0_13,plain,
multiply(sF4,multiply(sF7,multiply(b,inverse(b)))) != identity,
inference(rw,[status(thm)],[g0_12,t1292]) ).
cnf(g0_14,plain,
multiply(b,inverse(b)) != identity,
inference(rw,[status(thm)],[g0_13,t2237]) ).
cnf(g0_15,plain,
sF8 != identity,
inference(rw,[status(thm)],[g0_14,t2193]) ).
cnf(g0_16,plain,
sF8 != sF8,
inference(rw,[status(thm)],[g0_15,t2173]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_16]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP002-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 13:09:06 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 4.11/0.92 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.11/0.92 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------