%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP320-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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 : Sun Sep 27 07:28:38 AM UTC 2026
% Result : Unsatisfiable 100.45s 32.33s
% Output : CNFRefutation 100.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 27
% Syntax : Number of formulae : 208 ( 26 unt; 0 def)
% Number of atoms : 543 ( 542 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 493 ( 158 ~; 335 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 55 ( 0 sgn 10 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(left_identity,axiom,
! [VAR_0] : multiply(identity,VAR_0) = VAR_0,
file('theBenchmark.p',left_identity) ).
cnf(c_1,plain,
multiply(identity,A) = A,
inference(clausify,[status(thm)],[left_identity]) ).
fof(left_inverse,axiom,
! [VAR_0] : multiply(inverse(VAR_0),VAR_0) = identity,
file('theBenchmark.p',left_inverse) ).
cnf(c_2,plain,
multiply(inverse(A),A) = identity,
inference(clausify,[status(thm)],[left_inverse]) ).
fof(associativity,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(multiply(VAR_0,VAR_1),VAR_2) = multiply(VAR_0,multiply(VAR_1,VAR_2)),
file('theBenchmark.p',associativity) ).
cnf(c_3,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(clausify,[status(thm)],[associativity]) ).
fof(prove_this_1,axiom,
( multiply(sk_c4,sk_c8) = sk_c7
| multiply(sk_c7,sk_c8) = sk_c6 ),
file('theBenchmark.p',prove_this_1) ).
cnf(c_4,plain,
( multiply(sk_c4,sk_c8) = sk_c7
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_1]) ).
fof(prove_this_2,axiom,
( inverse(sk_c4) = sk_c8
| multiply(sk_c7,sk_c8) = sk_c6 ),
file('theBenchmark.p',prove_this_2) ).
cnf(c_5,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_2]) ).
fof(prove_this_3,axiom,
( multiply(sk_c5,sk_c7) = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
file('theBenchmark.p',prove_this_3) ).
cnf(c_6,plain,
( multiply(sk_c5,sk_c7) = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_3]) ).
fof(prove_this_4,axiom,
( inverse(sk_c5) = sk_c7
| multiply(sk_c7,sk_c8) = sk_c6 ),
file('theBenchmark.p',prove_this_4) ).
cnf(c_7,plain,
( inverse(sk_c5) = sk_c7
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_4]) ).
fof(prove_this_5,axiom,
( multiply(sk_c6,sk_c8) = sk_c7
| multiply(sk_c7,sk_c8) = sk_c6 ),
file('theBenchmark.p',prove_this_5) ).
cnf(c_8,plain,
( multiply(sk_c6,sk_c8) = sk_c7
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_5]) ).
fof(prove_this_6,axiom,
( multiply(sk_c4,sk_c8) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c8 ),
file('theBenchmark.p',prove_this_6) ).
cnf(c_9,plain,
( multiply(sk_c4,sk_c8) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_6]) ).
fof(prove_this_7,axiom,
( inverse(sk_c4) = sk_c8
| multiply(sk_c1,sk_c7) = sk_c8 ),
file('theBenchmark.p',prove_this_7) ).
cnf(c_10,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c1,sk_c7) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_7]) ).
fof(prove_this_8,axiom,
( multiply(sk_c5,sk_c7) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c8 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_11,plain,
( multiply(sk_c5,sk_c7) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_8]) ).
fof(prove_this_9,axiom,
( inverse(sk_c5) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c8 ),
file('theBenchmark.p',prove_this_9) ).
cnf(c_12,plain,
( inverse(sk_c5) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_9]) ).
fof(prove_this_10,axiom,
( multiply(sk_c6,sk_c8) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c8 ),
file('theBenchmark.p',prove_this_10) ).
cnf(c_13,plain,
( multiply(sk_c6,sk_c8) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_10]) ).
fof(prove_this_11,axiom,
( multiply(sk_c4,sk_c8) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_11) ).
cnf(c_14,plain,
( multiply(sk_c4,sk_c8) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_11]) ).
fof(prove_this_12,axiom,
( inverse(sk_c4) = sk_c8
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_12) ).
cnf(c_15,plain,
( inverse(sk_c4) = sk_c8
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_12]) ).
fof(prove_this_13,axiom,
( multiply(sk_c5,sk_c7) = sk_c6
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_13) ).
cnf(c_16,plain,
( multiply(sk_c5,sk_c7) = sk_c6
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_13]) ).
fof(prove_this_14,axiom,
( inverse(sk_c5) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_14) ).
cnf(c_17,plain,
( inverse(sk_c5) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_14]) ).
fof(prove_this_15,axiom,
( multiply(sk_c6,sk_c8) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_15) ).
cnf(c_18,plain,
( multiply(sk_c6,sk_c8) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_15]) ).
fof(prove_this_16,axiom,
( multiply(sk_c4,sk_c8) = sk_c7
| multiply(sk_c8,sk_c3) = sk_c7 ),
file('theBenchmark.p',prove_this_16) ).
cnf(c_19,plain,
( multiply(sk_c4,sk_c8) = sk_c7
| multiply(sk_c8,sk_c3) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_16]) ).
fof(prove_this_17,axiom,
( inverse(sk_c4) = sk_c8
| multiply(sk_c8,sk_c3) = sk_c7 ),
file('theBenchmark.p',prove_this_17) ).
cnf(c_20,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c8,sk_c3) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_17]) ).
fof(prove_this_18,axiom,
( multiply(sk_c5,sk_c7) = sk_c6
| multiply(sk_c8,sk_c3) = sk_c7 ),
file('theBenchmark.p',prove_this_18) ).
cnf(c_21,plain,
( multiply(sk_c5,sk_c7) = sk_c6
| multiply(sk_c8,sk_c3) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_18]) ).
fof(prove_this_19,axiom,
( inverse(sk_c5) = sk_c7
| multiply(sk_c8,sk_c3) = sk_c7 ),
file('theBenchmark.p',prove_this_19) ).
cnf(c_22,plain,
( inverse(sk_c5) = sk_c7
| multiply(sk_c8,sk_c3) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_19]) ).
fof(prove_this_23,axiom,
( multiply(sk_c5,sk_c7) = sk_c6
| multiply(sk_c2,sk_c8) = sk_c3 ),
file('theBenchmark.p',prove_this_23) ).
cnf(c_26,plain,
( multiply(sk_c5,sk_c7) = sk_c6
| multiply(sk_c2,sk_c8) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_23]) ).
fof(prove_this_24,axiom,
( inverse(sk_c5) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c3 ),
file('theBenchmark.p',prove_this_24) ).
cnf(c_27,plain,
( inverse(sk_c5) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_24]) ).
fof(prove_this_28,axiom,
( multiply(sk_c5,sk_c7) = sk_c6
| inverse(sk_c2) = sk_c8 ),
file('theBenchmark.p',prove_this_28) ).
cnf(c_31,plain,
( multiply(sk_c5,sk_c7) = sk_c6
| inverse(sk_c2) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_28]) ).
fof(prove_this_29,axiom,
( inverse(sk_c5) = sk_c7
| inverse(sk_c2) = sk_c8 ),
file('theBenchmark.p',prove_this_29) ).
cnf(c_32,plain,
( inverse(sk_c5) = sk_c7
| inverse(sk_c2) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_29]) ).
fof(prove_this_31,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( multiply(sk_c6,sk_c8) != sk_c7
| inverse(VAR_4) != sk_c7
| multiply(VAR_4,sk_c7) != sk_c6
| inverse(VAR_3) != sk_c8
| multiply(VAR_3,sk_c8) != sk_c7
| inverse(VAR_2) != sk_c8
| multiply(VAR_2,sk_c8) != VAR_1
| multiply(sk_c8,VAR_1) != sk_c7
| inverse(VAR_0) != sk_c7
| multiply(VAR_0,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6 ),
file('theBenchmark.p',prove_this_31) ).
cnf(c_34,plain,
( multiply(sk_c6,sk_c8) != sk_c7
| inverse(E) != sk_c7
| multiply(E,sk_c7) != sk_c6
| inverse(D) != sk_c8
| multiply(D,sk_c8) != sk_c7
| inverse(C) != sk_c8
| multiply(C,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6 ),
inference(clausify,[status(thm)],[prove_this_31]) ).
cnf(c_36,plain,
( multiply(sk_c6,sk_c8) != sk_c7
| multiply(A,sk_c7) != sk_c6
| inverse(D) != sk_c8
| multiply(D,sk_c8) != sk_c7
| inverse(C) != sk_c8
| multiply(C,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6 ),
inference(factor,[status(thm)],[c_34]) ).
cnf(c_46,plain,
( multiply(sk_c6,sk_c8) != sk_c7
| multiply(A,sk_c7) != sk_c6
| multiply(C,sk_c8) != sk_c7
| inverse(C) != sk_c8
| multiply(C,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6 ),
inference(factor,[status(thm)],[c_36]) ).
cnf(c_25072,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_25073,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_25072]) ).
cnf(c_56,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_25073]) ).
cnf(c_67,plain,
( multiply(sk_c8,sk_c4) = identity
| multiply(sk_c1,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_10,c_2]) ).
cnf(c_70,plain,
( multiply(sk_c7,sk_c5) = identity
| multiply(sk_c1,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_12,c_2]) ).
cnf(c_25074,plain,
( multiply(multiply(A,sk_c2),sk_c8) = multiply(A,sk_c3)
| multiply(sk_c5,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_26,c_3]) ).
cnf(c_90,plain,
( multiply(A,multiply(sk_c2,sk_c8)) = multiply(A,sk_c3)
| multiply(sk_c5,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_3,c_25074]) ).
cnf(c_96,plain,
( multiply(sk_c8,sk_c2) = identity
| multiply(sk_c5,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_31,c_2]) ).
cnf(c_97,plain,
( multiply(sk_c8,sk_c2) = identity
| inverse(sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_32,c_2]) ).
cnf(c_858,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_56]) ).
cnf(c_890,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_56,c_56]) ).
cnf(c_891,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_890,c_858]) ).
cnf(c_954,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_891,c_2]) ).
cnf(c_1258,plain,
multiply(A,inverse(A)) = identity,
inference(paramod,[status(thm)],[c_890,c_2]) ).
cnf(c_25075,plain,
multiply(A,identity) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_890,c_891]) ).
cnf(c_25076,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_891,c_25075]) ).
cnf(c_1284,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_25076]) ).
cnf(c_25077,plain,
( multiply(sk_c6,sk_c8) != sk_c7
| multiply(inverse(sk_c7),sk_c7) != sk_c6
| multiply(B,sk_c8) != sk_c7
| inverse(B) != sk_c8
| multiply(B,sk_c8) != A
| multiply(sk_c8,A) != sk_c7
| multiply(inverse(sk_c7),sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6 ),
inference(resolve,[status(thm)],[c_1284,c_46]) ).
cnf(c_25078,plain,
( multiply(sk_c6,sk_c8) != sk_c7
| multiply(inverse(sk_c7),sk_c7) != sk_c6
| multiply(B,sk_c8) != sk_c7
| inverse(B) != sk_c8
| multiply(B,sk_c8) != A
| multiply(sk_c8,A) != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6 ),
inference(paramod,[status(thm)],[c_2,c_25077]) ).
cnf(c_1335,plain,
( multiply(sk_c6,sk_c8) != sk_c7
| identity != sk_c6
| multiply(B,sk_c8) != sk_c7
| inverse(B) != sk_c8
| multiply(B,sk_c8) != A
| multiply(sk_c8,A) != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6 ),
inference(paramod,[status(thm)],[c_2,c_25078]) ).
cnf(c_1376,plain,
( inverse(sk_c8) = sk_c2
| inverse(sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_32,c_1284]) ).
cnf(c_1438,plain,
( multiply(sk_c4,sk_c8) = identity
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_5,c_1258]) ).
cnf(c_1439,plain,
( multiply(sk_c5,sk_c7) = identity
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_7,c_1258]) ).
cnf(c_1442,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c4,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_14,c_1258]) ).
cnf(c_1443,plain,
( multiply(sk_c1,sk_c7) = identity
| inverse(sk_c4) = sk_c8 ),
inference(paramod,[status(thm)],[c_15,c_1258]) ).
cnf(c_1444,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c5,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_16,c_1258]) ).
cnf(c_1445,plain,
( multiply(sk_c1,sk_c7) = identity
| inverse(sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_17,c_1258]) ).
cnf(c_1446,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c6,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_18,c_1258]) ).
cnf(c_1447,plain,
( multiply(sk_c4,sk_c8) = identity
| multiply(sk_c8,sk_c3) = sk_c7 ),
inference(paramod,[status(thm)],[c_20,c_1258]) ).
cnf(c_1448,plain,
( multiply(sk_c5,sk_c7) = identity
| multiply(sk_c8,sk_c3) = sk_c7 ),
inference(paramod,[status(thm)],[c_22,c_1258]) ).
cnf(c_1450,plain,
( multiply(sk_c5,sk_c7) = identity
| multiply(sk_c2,sk_c8) = sk_c3 ),
inference(paramod,[status(thm)],[c_27,c_1258]) ).
cnf(c_1469,plain,
( multiply(sk_c5,sk_c7) = identity
| multiply(sk_c8,sk_c2) = identity ),
inference(paramod,[status(thm)],[c_97,c_1258]) ).
cnf(c_1723,plain,
( multiply(sk_c5,sk_c7) = identity
| inverse(sk_c8) = sk_c2 ),
inference(paramod,[status(thm)],[c_1376,c_1258]) ).
cnf(c_3391,plain,
( multiply(sk_c8,sk_c4) = identity
| multiply(sk_c1,sk_c7) = identity ),
inference(paramod,[status(thm)],[c_1443,c_2]) ).
cnf(c_3613,plain,
( multiply(sk_c7,sk_c5) = identity
| multiply(sk_c1,sk_c7) = identity ),
inference(paramod,[status(thm)],[c_1445,c_2]) ).
cnf(c_25079,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_1438,c_4]) ).
cnf(c_6316,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_25079]) ).
cnf(c_25080,plain,
( identity = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_1439,c_6]) ).
cnf(c_6417,plain,
( identity = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_25080]) ).
cnf(c_25081,plain,
( multiply(sk_c4,sk_c8) = sk_c7
| identity = sk_c8
| multiply(sk_c4,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_1442,c_9]) ).
cnf(c_6626,plain,
( identity = sk_c8
| multiply(sk_c4,sk_c8) = sk_c7 ),
inference(copy,[status(thm)],[c_25081]) ).
cnf(c_25082,plain,
( multiply(sk_c5,sk_c7) = sk_c6
| identity = sk_c8
| multiply(sk_c5,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_1444,c_11]) ).
cnf(c_6879,plain,
( identity = sk_c8
| multiply(sk_c5,sk_c7) = sk_c6 ),
inference(copy,[status(thm)],[c_25082]) ).
cnf(c_25083,plain,
( multiply(sk_c6,sk_c8) = sk_c7
| identity = sk_c8
| multiply(sk_c6,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_1446,c_13]) ).
cnf(c_7106,plain,
( identity = sk_c8
| multiply(sk_c6,sk_c8) = sk_c7 ),
inference(copy,[status(thm)],[c_25083]) ).
cnf(c_7116,plain,
( multiply(inverse(sk_c6),sk_c7) = sk_c8
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_7106,c_56]) ).
cnf(c_25084,plain,
( multiply(sk_c6,sk_c8) != sk_c7
| identity != sk_c6
| multiply(identity,sk_c8) != sk_c7
| inverse(identity) != sk_c8
| sk_c8 != A
| multiply(sk_c8,A) != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6 ),
inference(paramod,[status(thm)],[c_1,c_1335]) ).
cnf(c_25085,plain,
( multiply(sk_c6,sk_c8) != sk_c7
| identity != sk_c6
| multiply(identity,sk_c8) != sk_c7
| identity != sk_c8
| sk_c8 != A
| multiply(sk_c8,A) != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6 ),
inference(paramod,[status(thm)],[c_954,c_25084]) ).
cnf(c_25086,plain,
( multiply(sk_c6,sk_c8) != sk_c7
| identity != sk_c6
| sk_c8 != sk_c7
| identity != sk_c8
| sk_c8 != A
| multiply(sk_c8,A) != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6 ),
inference(paramod,[status(thm)],[c_1,c_25085]) ).
cnf(c_7321,plain,
( multiply(sk_c6,sk_c8) != sk_c7
| identity != sk_c6
| sk_c8 != sk_c7
| sk_c8 != A
| multiply(sk_c8,A) != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6 ),
inference(copy,[status(thm)],[c_25086]) ).
cnf(c_25087,plain,
( multiply(sk_c6,sk_c8) != sk_c7
| identity != sk_c6
| sk_c8 != sk_c7
| sk_c8 != identity
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6 ),
inference(paramod,[status(thm)],[c_891,c_7321]) ).
cnf(c_25088,plain,
( multiply(sk_c6,sk_c8) != sk_c7
| identity != sk_c6
| sk_c8 != sk_c7
| identity != sk_c8
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6 ),
inference(copy,[status(thm)],[c_25087]) ).
cnf(c_25089,plain,
( multiply(sk_c6,sk_c8) != sk_c7
| identity != sk_c6
| sk_c8 != sk_c7
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6 ),
inference(copy,[status(thm)],[c_25088]) ).
cnf(c_7383,plain,
( multiply(sk_c6,sk_c8) != sk_c7
| identity != sk_c6
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6 ),
inference(copy,[status(thm)],[c_25089]) ).
cnf(c_25090,plain,
( identity = sk_c7
| multiply(sk_c8,sk_c3) = sk_c7
| multiply(sk_c8,sk_c3) = sk_c7 ),
inference(paramod,[status(thm)],[c_1447,c_19]) ).
cnf(c_7385,plain,
( identity = sk_c7
| multiply(sk_c8,sk_c3) = sk_c7 ),
inference(copy,[status(thm)],[c_25090]) ).
cnf(c_7406,plain,
( multiply(inverse(sk_c8),sk_c7) = sk_c3
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_7385,c_56]) ).
cnf(c_25091,plain,
( identity = sk_c6
| multiply(sk_c8,sk_c3) = sk_c7
| multiply(sk_c8,sk_c3) = sk_c7 ),
inference(paramod,[status(thm)],[c_1448,c_21]) ).
cnf(c_7436,plain,
( identity = sk_c6
| multiply(sk_c8,sk_c3) = sk_c7 ),
inference(copy,[status(thm)],[c_25091]) ).
cnf(c_7635,plain,
( multiply(inverse(sk_c8),sk_c7) = sk_c3
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_7436,c_56]) ).
cnf(c_25092,plain,
( multiply(sk_c8,sk_c2) = identity
| identity = sk_c6
| multiply(sk_c8,sk_c2) = identity ),
inference(paramod,[status(thm)],[c_1469,c_96]) ).
cnf(c_10224,plain,
( identity = sk_c6
| multiply(sk_c8,sk_c2) = identity ),
inference(copy,[status(thm)],[c_25092]) ).
cnf(c_25093,plain,
( multiply(inverse(sk_c8),identity) = sk_c2
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_10224,c_56]) ).
cnf(c_10229,plain,
( inverse(sk_c8) = sk_c2
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_891,c_25093]) ).
cnf(c_25094,plain,
( multiply(sk_c2,sk_c7) = sk_c3
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_10229,c_7635]) ).
cnf(c_10387,plain,
( multiply(sk_c2,sk_c7) = sk_c3
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_25094]) ).
cnf(c_10442,plain,
( multiply(inverse(sk_c2),sk_c3) = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_10387,c_56]) ).
cnf(c_25095,plain,
( multiply(inverse(sk_c2),multiply(sk_c2,sk_c8)) = sk_c7
| multiply(sk_c5,sk_c7) = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_10442,c_90]) ).
cnf(c_10583,plain,
( sk_c8 = sk_c7
| multiply(sk_c5,sk_c7) = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_56,c_25095]) ).
cnf(c_25096,plain,
( multiply(sk_c8,sk_c4) = identity
| identity = sk_c8
| multiply(sk_c8,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_3391,c_67]) ).
cnf(c_10833,plain,
( identity = sk_c8
| multiply(sk_c8,sk_c4) = identity ),
inference(copy,[status(thm)],[c_25096]) ).
cnf(c_25097,plain,
( multiply(inverse(sk_c8),identity) = sk_c4
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_10833,c_56]) ).
cnf(c_10837,plain,
( inverse(sk_c8) = sk_c4
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_891,c_25097]) ).
cnf(c_10965,plain,
( multiply(sk_c4,sk_c8) = identity
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_10837,c_2]) ).
cnf(c_25098,plain,
( identity = sk_c8
| identity = sk_c7
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_10965,c_6626]) ).
cnf(c_11037,plain,
( identity = sk_c7
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_25098]) ).
cnf(c_11039,plain,
( multiply(A,sk_c8) = A
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_11037,c_891]) ).
cnf(c_11040,plain,
( inverse(sk_c8) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_11037,c_954]) ).
cnf(c_25099,plain,
( multiply(identity,sk_c7) = sk_c3
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_11040,c_7406]) ).
cnf(c_25100,plain,
( sk_c7 = sk_c3
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_1,c_25099]) ).
cnf(c_25101,plain,
( sk_c3 = sk_c7
| identity = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_25100]) ).
cnf(c_11216,plain,
( sk_c3 = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_25101]) ).
cnf(c_25102,plain,
( identity = sk_c7
| sk_c7 = sk_c6
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_11039,c_6316]) ).
cnf(c_25103,plain,
( identity = sk_c7
| sk_c6 = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_25102]) ).
cnf(c_11970,plain,
( sk_c6 = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_25103]) ).
cnf(c_25104,plain,
( multiply(sk_c7,sk_c5) = identity
| identity = sk_c8
| multiply(sk_c7,sk_c5) = identity ),
inference(paramod,[status(thm)],[c_3613,c_70]) ).
cnf(c_15587,plain,
( identity = sk_c8
| multiply(sk_c7,sk_c5) = identity ),
inference(copy,[status(thm)],[c_25104]) ).
cnf(c_25105,plain,
( multiply(inverse(sk_c7),identity) = sk_c5
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_15587,c_56]) ).
cnf(c_15600,plain,
( inverse(sk_c7) = sk_c5
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_891,c_25105]) ).
cnf(c_15625,plain,
( multiply(sk_c5,sk_c7) = identity
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_15600,c_2]) ).
cnf(c_25106,plain,
( identity = sk_c8
| identity = sk_c6
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_15625,c_6879]) ).
cnf(c_15700,plain,
( identity = sk_c6
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_25106]) ).
cnf(c_25107,plain,
( sk_c6 = sk_c7
| sk_c6 = sk_c7
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_15700,c_11970]) ).
cnf(c_15723,plain,
( sk_c6 = sk_c7
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_25107]) ).
cnf(c_15728,plain,
( multiply(A,sk_c8) = A
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_15723,c_891]) ).
cnf(c_25108,plain,
( sk_c6 = sk_c7
| sk_c8 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_15723,c_11970]) ).
cnf(c_15755,plain,
( sk_c8 = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_25108]) ).
cnf(c_25109,plain,
( multiply(inverse(sk_c7),sk_c7) = sk_c8
| identity = sk_c8
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_15755,c_7116]) ).
cnf(c_25110,plain,
( identity = sk_c8
| identity = sk_c8
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_25109]) ).
cnf(c_15829,plain,
( identity = sk_c8
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_25110]) ).
cnf(c_15870,plain,
( inverse(sk_c8) = identity
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_15829,c_954]) ).
cnf(c_25111,plain,
( sk_c3 = sk_c7
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_15829,c_11216]) ).
cnf(c_15896,plain,
( sk_c3 = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_25111]) ).
cnf(c_15911,plain,
( multiply(sk_c5,sk_c7) = identity
| multiply(sk_c2,sk_c8) = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_15896,c_1450]) ).
cnf(c_16189,plain,
( multiply(sk_c5,sk_c7) = identity
| identity = sk_c2
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_15870,c_1723]) ).
cnf(c_25112,plain,
( inverse(sk_c8) = sk_c8
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_15829,c_15870]) ).
cnf(c_16223,plain,
( inverse(sk_c8) = sk_c8
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_25112]) ).
cnf(c_16380,plain,
( multiply(sk_c8,sk_c8) = identity
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_16223,c_2]) ).
cnf(c_25113,plain,
( identity = sk_c6
| sk_c7 = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_15728,c_6417]) ).
cnf(c_25114,plain,
( identity = sk_c6
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_25113]) ).
cnf(c_16573,plain,
( identity = sk_c6
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_25114]) ).
cnf(c_25115,plain,
( sk_c6 = sk_c7
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_16573,c_11970]) ).
cnf(c_25116,plain,
( sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_25115]) ).
cnf(c_16598,plain,
sk_c6 = sk_c7,
inference(copy,[status(thm)],[c_25116]) ).
cnf(c_25117,plain,
( sk_c8 = sk_c7
| multiply(sk_c5,sk_c7) = sk_c6
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_16598,c_10583]) ).
cnf(c_19361,plain,
( sk_c8 = sk_c7
| multiply(sk_c5,sk_c7) = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_16598,c_25117]) ).
cnf(c_25118,plain,
( multiply(sk_c6,sk_c8) != sk_c7
| identity != sk_c6
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_16598,c_7383]) ).
cnf(c_25119,plain,
( multiply(sk_c6,sk_c8) != sk_c7
| identity != sk_c7
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_16598,c_25118]) ).
cnf(c_25120,plain,
( multiply(sk_c7,sk_c8) != sk_c7
| identity != sk_c7
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_16598,c_25119]) ).
cnf(c_20834,plain,
( identity != sk_c7
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_25120]) ).
cnf(c_25121,plain,
( multiply(inverse(sk_c7),sk_c7) = sk_c8
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_16598,c_7116]) ).
cnf(c_25122,plain,
( identity = sk_c8
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_2,c_25121]) ).
cnf(c_21036,plain,
identity = sk_c8,
inference(copy,[status(thm)],[c_25122]) ).
cnf(c_25123,plain,
( multiply(sk_c6,sk_c8) = sk_c7
| multiply(sk_c7,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_16598,c_8]) ).
cnf(c_25124,plain,
( multiply(sk_c7,sk_c8) = sk_c7
| multiply(sk_c7,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_16598,c_25123]) ).
cnf(c_23910,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(copy,[status(thm)],[c_25124]) ).
cnf(c_25125,plain,
( identity != sk_c7
| sk_c8 != sk_c7
| identity != sk_c8
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_23910,c_20834]) ).
cnf(c_25126,plain,
( identity != sk_c7
| sk_c8 != sk_c7
| sk_c8 != sk_c8
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_21036,c_25125]) ).
cnf(c_25127,plain,
( sk_c8 != sk_c7
| sk_c8 != sk_c7
| sk_c8 != sk_c8
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_21036,c_25126]) ).
cnf(c_25128,plain,
( sk_c8 != sk_c7
| sk_c8 != sk_c7
| sk_c8 != sk_c8 ),
inference(copy,[status(thm)],[c_25127]) ).
cnf(c_25129,plain,
( sk_c8 != sk_c7
| sk_c8 != sk_c7 ),
inference(copy,[status(thm)],[c_25128]) ).
cnf(c_24551,plain,
sk_c8 != sk_c7,
inference(copy,[status(thm)],[c_25129]) ).
cnf(c_25130,plain,
( sk_c8 = sk_c7
| multiply(sk_c5,sk_c7) = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_21036,c_19361]) ).
cnf(c_25131,plain,
( multiply(sk_c5,sk_c7) = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_25130]) ).
cnf(c_24776,plain,
multiply(sk_c5,sk_c7) = sk_c7,
inference(resolve,[status(thm)],[c_24551,c_25131]) ).
cnf(c_25132,plain,
( multiply(sk_c8,sk_c8) = sk_c8
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_21036,c_16380]) ).
cnf(c_25064,plain,
multiply(sk_c8,sk_c8) = sk_c8,
inference(resolve,[status(thm)],[c_24551,c_25132]) ).
cnf(c_25133,plain,
( multiply(sk_c5,sk_c7) = identity
| sk_c8 = sk_c2
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_21036,c_16189]) ).
cnf(c_25134,plain,
( sk_c7 = identity
| sk_c8 = sk_c2
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_24776,c_25133]) ).
cnf(c_25135,plain,
( sk_c7 = sk_c8
| sk_c8 = sk_c2
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_21036,c_25134]) ).
cnf(c_25136,plain,
( sk_c7 = sk_c8
| sk_c2 = sk_c8
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_25135]) ).
cnf(c_25137,plain,
( sk_c8 = sk_c7
| sk_c2 = sk_c8
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_25136]) ).
cnf(c_25138,plain,
( sk_c2 = sk_c8
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_25137]) ).
cnf(c_25065,plain,
sk_c2 = sk_c8,
inference(resolve,[status(thm)],[c_24551,c_25138]) ).
cnf(c_25139,plain,
( multiply(sk_c5,sk_c7) = identity
| multiply(sk_c8,sk_c8) = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_25065,c_15911]) ).
cnf(c_25140,plain,
( multiply(sk_c5,sk_c7) = identity
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_25064,c_25139]) ).
cnf(c_25141,plain,
( sk_c7 = identity
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_24776,c_25140]) ).
cnf(c_25142,plain,
( sk_c7 = sk_c8
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_21036,c_25141]) ).
cnf(c_25143,plain,
( sk_c8 = sk_c7
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_25142]) ).
cnf(c_25144,plain,
( sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_25143]) ).
cnf(c_25145,plain,
sk_c8 = sk_c7,
inference(copy,[status(thm)],[c_25144]) ).
cnf(c_25071,plain,
$false,
inference(resolve,[status(thm)],[c_24551,c_25145]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP320-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.41 % Computer : n002.cluster.edu
% 0.09/5.41 % Model : x86_64 x86_64
% 0.09/5.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.41 % Memory : 8046.5625MB
% 0.09/5.41 % OS : Linux 6.8.0-71-generic
% 0.09/5.41 % CPULimit : 300
% 0.09/5.41 % WCLimit : 300
% 0.09/5.41 % DateTime : Fri Sep 25 14:48:10 UTC 2026
% 0.09/5.41 % CPUTime :
% 0.09/5.41 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/5.41 % Process 3545209 was started by sandbox on n002,
% 0.09/5.41 % Fri Sep 25 14:48:10 2026
% 0.09/5.41 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/5.42
% 0.09/5.42 % From the command line: assign(max_seconds, 300).
% 100.45/32.33
% 100.45/32.33 % given #500 (F,wt=34): 13516 multiply(sk_c7,sk_c8) != sk_c6 | identity != sk_c8 | sk_c7 != A | multiply(inverse(sk_c8),A) != multiply(sk_c6,sk_c8) | inverse(sk_c6) != sk_c8 | multiply(sk_c6,sk_c8) != sk_c7 | multiply(inverse(A),sk_c7) != sk_c6. [factor(13510,c,h)].
% 100.45/32.33
% 100.45/32.33 % SZS status Unsatisfiable for theBenchmark
% 100.45/32.33
% 100.45/32.33 % Proof 1 at 11.09 (+ 1.54) seconds.
% 100.45/32.33 % Length of proof is 107.
% 100.45/32.33 % Level of proof is 20.
% 100.45/32.33 % Maximum clause weight is 51.000.
% 100.45/32.33 % Given clauses 703.
% 100.45/32.33
% 100.45/32.33 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------