%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP293-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 : n009.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:34 AM UTC 2026
% Result : Unsatisfiable 142.71s 19.46s
% Output : CNFRefutation 142.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 89
% Number of leaves : 32
% Syntax : Number of formulae : 274 ( 32 unt; 0 def)
% Number of atoms : 785 ( 784 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 758 ( 247 ~; 511 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 3 avg)
% Maximal term depth : 3 ( 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 : 74 ( 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_c7,sk_c8) = sk_c6
| multiply(sk_c8,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_1) ).
cnf(c_4,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c8,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_1]) ).
fof(prove_this_4,axiom,
( multiply(sk_c8,sk_c5) = sk_c7
| multiply(sk_c8,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_4) ).
cnf(c_7,plain,
( multiply(sk_c8,sk_c5) = sk_c7
| multiply(sk_c8,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_4]) ).
fof(prove_this_5,axiom,
( multiply(sk_c4,sk_c8) = sk_c5
| multiply(sk_c8,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_5) ).
cnf(c_8,plain,
( multiply(sk_c4,sk_c8) = sk_c5
| multiply(sk_c8,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_5]) ).
fof(prove_this_7,axiom,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_7) ).
cnf(c_10,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_7]) ).
fof(prove_this_8,axiom,
( multiply(sk_c3,sk_c7) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_11,plain,
( multiply(sk_c3,sk_c7) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_8]) ).
fof(prove_this_9,axiom,
( inverse(sk_c3) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_9) ).
cnf(c_12,plain,
( inverse(sk_c3) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_9]) ).
fof(prove_this_10,axiom,
( multiply(sk_c8,sk_c5) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_10) ).
cnf(c_13,plain,
( multiply(sk_c8,sk_c5) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_10]) ).
fof(prove_this_11,axiom,
( multiply(sk_c4,sk_c8) = sk_c5
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_11) ).
cnf(c_14,plain,
( multiply(sk_c4,sk_c8) = sk_c5
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_11]) ).
fof(prove_this_12,axiom,
( inverse(sk_c4) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_12) ).
cnf(c_15,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_12]) ).
fof(prove_this_13,axiom,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_13) ).
cnf(c_16,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_13]) ).
fof(prove_this_14,axiom,
( multiply(sk_c3,sk_c7) = sk_c8
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_14) ).
cnf(c_17,plain,
( multiply(sk_c3,sk_c7) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_14]) ).
fof(prove_this_15,axiom,
( inverse(sk_c3) = sk_c7
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_15) ).
cnf(c_18,plain,
( inverse(sk_c3) = sk_c7
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_15]) ).
fof(prove_this_16,axiom,
( multiply(sk_c8,sk_c5) = sk_c7
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_16) ).
cnf(c_19,plain,
( multiply(sk_c8,sk_c5) = sk_c7
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_16]) ).
fof(prove_this_17,axiom,
( multiply(sk_c4,sk_c8) = sk_c5
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_17) ).
cnf(c_20,plain,
( multiply(sk_c4,sk_c8) = sk_c5
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_17]) ).
fof(prove_this_18,axiom,
( inverse(sk_c4) = sk_c8
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_18) ).
cnf(c_21,plain,
( inverse(sk_c4) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_18]) ).
fof(prove_this_24,axiom,
( inverse(sk_c4) = sk_c8
| multiply(sk_c8,sk_c6) = sk_c7 ),
file('theBenchmark.p',prove_this_24) ).
cnf(c_27,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c8,sk_c6) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_24]) ).
fof(prove_this_25,axiom,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c2,sk_c8) = sk_c6 ),
file('theBenchmark.p',prove_this_25) ).
cnf(c_28,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c2,sk_c8) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_25]) ).
fof(prove_this_26,axiom,
( multiply(sk_c3,sk_c7) = sk_c8
| multiply(sk_c2,sk_c8) = sk_c6 ),
file('theBenchmark.p',prove_this_26) ).
cnf(c_29,plain,
( multiply(sk_c3,sk_c7) = sk_c8
| multiply(sk_c2,sk_c8) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_26]) ).
fof(prove_this_27,axiom,
( inverse(sk_c3) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c6 ),
file('theBenchmark.p',prove_this_27) ).
cnf(c_30,plain,
( inverse(sk_c3) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_27]) ).
fof(prove_this_28,axiom,
( multiply(sk_c8,sk_c5) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c6 ),
file('theBenchmark.p',prove_this_28) ).
cnf(c_31,plain,
( multiply(sk_c8,sk_c5) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_28]) ).
fof(prove_this_29,axiom,
( multiply(sk_c4,sk_c8) = sk_c5
| multiply(sk_c2,sk_c8) = sk_c6 ),
file('theBenchmark.p',prove_this_29) ).
cnf(c_32,plain,
( multiply(sk_c4,sk_c8) = sk_c5
| multiply(sk_c2,sk_c8) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_29]) ).
fof(prove_this_30,axiom,
( inverse(sk_c4) = sk_c8
| multiply(sk_c2,sk_c8) = sk_c6 ),
file('theBenchmark.p',prove_this_30) ).
cnf(c_33,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c2,sk_c8) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_30]) ).
fof(prove_this_31,axiom,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c2) = sk_c8 ),
file('theBenchmark.p',prove_this_31) ).
cnf(c_34,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c2) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_31]) ).
fof(prove_this_32,axiom,
( multiply(sk_c3,sk_c7) = sk_c8
| inverse(sk_c2) = sk_c8 ),
file('theBenchmark.p',prove_this_32) ).
cnf(c_35,plain,
( multiply(sk_c3,sk_c7) = sk_c8
| inverse(sk_c2) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_32]) ).
fof(prove_this_33,axiom,
( inverse(sk_c3) = sk_c7
| inverse(sk_c2) = sk_c8 ),
file('theBenchmark.p',prove_this_33) ).
cnf(c_36,plain,
( inverse(sk_c3) = sk_c7
| inverse(sk_c2) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_33]) ).
fof(prove_this_34,axiom,
( multiply(sk_c8,sk_c5) = sk_c7
| inverse(sk_c2) = sk_c8 ),
file('theBenchmark.p',prove_this_34) ).
cnf(c_37,plain,
( multiply(sk_c8,sk_c5) = sk_c7
| inverse(sk_c2) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_34]) ).
fof(prove_this_35,axiom,
( multiply(sk_c4,sk_c8) = sk_c5
| inverse(sk_c2) = sk_c8 ),
file('theBenchmark.p',prove_this_35) ).
cnf(c_38,plain,
( multiply(sk_c4,sk_c8) = sk_c5
| inverse(sk_c2) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_35]) ).
fof(prove_this_36,axiom,
( inverse(sk_c4) = sk_c8
| inverse(sk_c2) = sk_c8 ),
file('theBenchmark.p',prove_this_36) ).
cnf(c_39,plain,
( inverse(sk_c4) = sk_c8
| inverse(sk_c2) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_36]) ).
fof(prove_this_37,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( inverse(VAR_4) != sk_c8
| multiply(VAR_4,sk_c8) != VAR_3
| multiply(sk_c8,VAR_3) != sk_c7
| inverse(VAR_2) != sk_c7
| multiply(VAR_2,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(VAR_1) != sk_c8
| multiply(VAR_1,sk_c8) != sk_c6
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(VAR_0) != sk_c8
| multiply(VAR_0,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
file('theBenchmark.p',prove_this_37) ).
cnf(c_40,plain,
( inverse(E) != sk_c8
| multiply(E,sk_c8) != D
| multiply(sk_c8,D) != sk_c7
| inverse(C) != sk_c7
| multiply(C,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(B) != sk_c8
| multiply(B,sk_c8) != sk_c6
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(clausify,[status(thm)],[prove_this_37]) ).
cnf(c_43,plain,
( inverse(D) != sk_c8
| multiply(D,sk_c8) != C
| multiply(sk_c8,C) != sk_c7
| inverse(B) != sk_c7
| multiply(B,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(A,sk_c8) != sk_c6
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(factor,[status(thm)],[c_40]) ).
cnf(c_8898,plain,
( inverse(B) != sk_c8
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(C) != sk_c7
| multiply(C,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(B) != sk_c8
| multiply(B,sk_c8) != sk_c6
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(factor,[status(thm)],[c_40]) ).
cnf(c_8899,plain,
( inverse(B) != sk_c8
| inverse(C) != sk_c7
| multiply(C,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(B) != sk_c8
| multiply(B,sk_c8) != sk_c6
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(copy,[status(thm)],[c_8898]) ).
cnf(c_47,plain,
( inverse(C) != sk_c7
| multiply(C,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(B) != sk_c8
| multiply(B,sk_c8) != sk_c6
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(copy,[status(thm)],[c_8899]) ).
cnf(c_51,plain,
( multiply(A,sk_c8) != C
| multiply(sk_c8,C) != sk_c7
| inverse(B) != sk_c7
| multiply(B,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(A,sk_c8) != sk_c6
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(factor,[status(thm)],[c_43]) ).
cnf(c_8900,plain,
( multiply(sk_c8,sk_c6) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(factor,[status(thm)],[c_51]) ).
cnf(c_8901,plain,
( multiply(sk_c8,sk_c6) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(copy,[status(thm)],[c_8900]) ).
cnf(c_58,plain,
( inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(copy,[status(thm)],[c_8901]) ).
cnf(c_59,plain,
multiply(multiply(A,identity),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_1,c_3]) ).
cnf(c_8902,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_61,plain,
multiply(inverse(A),multiply(A,B)) = multiply(identity,B),
inference(copy,[status(thm)],[c_8902]) ).
cnf(c_100,plain,
( multiply(sk_c8,sk_c4) = identity
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_21,c_2]) ).
cnf(c_149,plain,
( inverse(identity) != sk_c7
| sk_c7 != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(B) != sk_c8
| multiply(B,sk_c8) != sk_c6
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_1,c_47]) ).
cnf(c_196,plain,
( inverse(identity) != sk_c7
| sk_c7 != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(A,sk_c8) != sk_c6
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(factor,[status(thm)],[c_149]) ).
cnf(c_8903,plain,
multiply(identity,A) = multiply(inverse(identity),A),
inference(paramod,[status(thm)],[c_2,c_59]) ).
cnf(c_288,plain,
multiply(inverse(identity),A) = multiply(identity,A),
inference(copy,[status(thm)],[c_8903]) ).
cnf(c_8904,plain,
multiply(A,B) = multiply(A,multiply(identity,B)),
inference(paramod,[status(thm)],[c_59,c_3]) ).
cnf(c_291,plain,
multiply(A,multiply(identity,B)) = multiply(A,B),
inference(copy,[status(thm)],[c_8904]) ).
cnf(c_584,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(paramod,[status(thm)],[c_1,c_61]) ).
cnf(c_658,plain,
( multiply(inverse(sk_c3),sk_c8) = sk_c7
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_17,c_584]) ).
cnf(c_661,plain,
( multiply(inverse(sk_c4),sk_c5) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_20,c_584]) ).
cnf(c_674,plain,
( multiply(inverse(sk_c2),sk_c6) = sk_c8
| inverse(sk_c4) = sk_c8 ),
inference(paramod,[status(thm)],[c_33,c_584]) ).
cnf(c_676,plain,
( multiply(inverse(sk_c3),sk_c8) = sk_c7
| inverse(sk_c2) = sk_c8 ),
inference(paramod,[status(thm)],[c_35,c_584]) ).
cnf(c_679,plain,
( multiply(inverse(sk_c4),sk_c5) = sk_c8
| inverse(sk_c2) = sk_c8 ),
inference(paramod,[status(thm)],[c_38,c_584]) ).
cnf(c_8905,plain,
( multiply(sk_c7,sk_c8) = sk_c7
| inverse(sk_c1) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_18,c_658]) ).
cnf(c_790,plain,
( multiply(sk_c7,sk_c8) = sk_c7
| inverse(sk_c1) = sk_c8 ),
inference(copy,[status(thm)],[c_8905]) ).
cnf(c_8906,plain,
( sk_c7 = sk_c6
| inverse(sk_c1) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_790,c_16]) ).
cnf(c_8907,plain,
( sk_c6 = sk_c7
| inverse(sk_c1) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(copy,[status(thm)],[c_8906]) ).
cnf(c_807,plain,
( sk_c6 = sk_c7
| inverse(sk_c1) = sk_c8 ),
inference(copy,[status(thm)],[c_8907]) ).
cnf(c_813,plain,
( multiply(sk_c8,sk_c1) = identity
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_807,c_2]) ).
cnf(c_816,plain,
( multiply(sk_c8,multiply(sk_c1,A)) = A
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_807,c_584]) ).
cnf(c_823,plain,
( multiply(inverse(sk_c8),identity) = sk_c1
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_813,c_584]) ).
cnf(c_8908,plain,
( multiply(sk_c8,sk_c5) = sk_c8
| inverse(sk_c1) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_21,c_661]) ).
cnf(c_901,plain,
( multiply(sk_c8,sk_c5) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(copy,[status(thm)],[c_8908]) ).
cnf(c_8909,plain,
( sk_c8 = sk_c7
| inverse(sk_c1) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_901,c_19]) ).
cnf(c_8910,plain,
( sk_c7 = sk_c8
| inverse(sk_c1) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(copy,[status(thm)],[c_8909]) ).
cnf(c_971,plain,
( sk_c7 = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(copy,[status(thm)],[c_8910]) ).
cnf(c_977,plain,
( multiply(sk_c8,sk_c1) = identity
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_971,c_2]) ).
cnf(c_980,plain,
( multiply(sk_c8,multiply(sk_c1,A)) = A
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_971,c_584]) ).
cnf(c_987,plain,
( multiply(inverse(sk_c8),identity) = sk_c1
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_977,c_584]) ).
cnf(c_8911,plain,
( multiply(sk_c7,sk_c8) = sk_c7
| inverse(sk_c2) = sk_c8
| inverse(sk_c2) = sk_c8 ),
inference(paramod,[status(thm)],[c_36,c_676]) ).
cnf(c_1209,plain,
( multiply(sk_c7,sk_c8) = sk_c7
| inverse(sk_c2) = sk_c8 ),
inference(copy,[status(thm)],[c_8911]) ).
cnf(c_8912,plain,
( sk_c7 = sk_c6
| inverse(sk_c2) = sk_c8
| inverse(sk_c2) = sk_c8 ),
inference(paramod,[status(thm)],[c_1209,c_34]) ).
cnf(c_8913,plain,
( sk_c6 = sk_c7
| inverse(sk_c2) = sk_c8
| inverse(sk_c2) = sk_c8 ),
inference(copy,[status(thm)],[c_8912]) ).
cnf(c_1230,plain,
( sk_c6 = sk_c7
| inverse(sk_c2) = sk_c8 ),
inference(copy,[status(thm)],[c_8913]) ).
cnf(c_1236,plain,
( multiply(sk_c8,sk_c2) = identity
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1230,c_2]) ).
cnf(c_1250,plain,
( multiply(inverse(sk_c8),identity) = sk_c2
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1236,c_584]) ).
cnf(c_8914,plain,
( sk_c2 = sk_c1
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1250,c_823]) ).
cnf(c_1297,plain,
( sk_c2 = sk_c1
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8914]) ).
cnf(c_1299,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c1,sk_c8) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1297,c_28]) ).
cnf(c_1300,plain,
( inverse(sk_c3) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1297,c_30]) ).
cnf(c_1301,plain,
( multiply(sk_c8,sk_c5) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1297,c_31]) ).
cnf(c_1302,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1297,c_33]) ).
cnf(c_8915,plain,
( inverse(sk_c3) = sk_c7
| sk_c6 = sk_c7
| inverse(sk_c3) = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1300,c_12]) ).
cnf(c_8916,plain,
( inverse(sk_c3) = sk_c7
| inverse(sk_c3) = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8915]) ).
cnf(c_1314,plain,
( inverse(sk_c3) = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8916]) ).
cnf(c_1315,plain,
( multiply(sk_c7,sk_c3) = identity
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1314,c_2]) ).
cnf(c_1323,plain,
( multiply(inverse(sk_c7),identity) = sk_c3
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1315,c_584]) ).
cnf(c_8917,plain,
( inverse(sk_c4) = sk_c8
| sk_c6 = sk_c7
| inverse(sk_c4) = sk_c8
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1302,c_15]) ).
cnf(c_8918,plain,
( inverse(sk_c4) = sk_c8
| inverse(sk_c4) = sk_c8
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8917]) ).
cnf(c_1339,plain,
( inverse(sk_c4) = sk_c8
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8918]) ).
cnf(c_1340,plain,
( multiply(sk_c8,sk_c4) = identity
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1339,c_2]) ).
cnf(c_1348,plain,
( multiply(inverse(sk_c8),identity) = sk_c4
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1340,c_584]) ).
cnf(c_8919,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| sk_c6 = sk_c7
| multiply(sk_c7,sk_c8) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1299,c_10]) ).
cnf(c_8920,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8919]) ).
cnf(c_1351,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8920]) ).
cnf(c_8921,plain,
( multiply(sk_c8,sk_c5) = sk_c7
| sk_c6 = sk_c7
| multiply(sk_c8,sk_c5) = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1301,c_13]) ).
cnf(c_8922,plain,
( multiply(sk_c8,sk_c5) = sk_c7
| multiply(sk_c8,sk_c5) = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8921]) ).
cnf(c_1397,plain,
( multiply(sk_c8,sk_c5) = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8922]) ).
cnf(c_8923,plain,
( sk_c4 = sk_c1
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1348,c_823]) ).
cnf(c_1429,plain,
( sk_c4 = sk_c1
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8923]) ).
cnf(c_1433,plain,
( multiply(sk_c1,sk_c8) = sk_c5
| multiply(sk_c1,sk_c8) = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1429,c_14]) ).
cnf(c_1435,plain,
( multiply(sk_c1,sk_c8) = sk_c5
| multiply(sk_c2,sk_c8) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1429,c_32]) ).
cnf(c_8924,plain,
( multiply(sk_c1,sk_c8) = sk_c5
| multiply(sk_c1,sk_c8) = sk_c6
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1297,c_1435]) ).
cnf(c_1519,plain,
( multiply(sk_c1,sk_c8) = sk_c5
| multiply(sk_c1,sk_c8) = sk_c6
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8924]) ).
cnf(c_8925,plain,
( multiply(sk_c8,sk_c5) = sk_c8
| inverse(sk_c2) = sk_c8
| inverse(sk_c2) = sk_c8 ),
inference(paramod,[status(thm)],[c_39,c_679]) ).
cnf(c_1670,plain,
( multiply(sk_c8,sk_c5) = sk_c8
| inverse(sk_c2) = sk_c8 ),
inference(copy,[status(thm)],[c_8925]) ).
cnf(c_8926,plain,
( sk_c8 = sk_c7
| inverse(sk_c2) = sk_c8
| inverse(sk_c2) = sk_c8 ),
inference(paramod,[status(thm)],[c_1670,c_37]) ).
cnf(c_8927,plain,
( sk_c7 = sk_c8
| inverse(sk_c2) = sk_c8
| inverse(sk_c2) = sk_c8 ),
inference(copy,[status(thm)],[c_8926]) ).
cnf(c_1715,plain,
( sk_c7 = sk_c8
| inverse(sk_c2) = sk_c8 ),
inference(copy,[status(thm)],[c_8927]) ).
cnf(c_1726,plain,
( multiply(sk_c8,sk_c6) = sk_c8
| inverse(sk_c4) = sk_c8
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_1715,c_674]) ).
cnf(c_8928,plain,
( inverse(sk_c4) = sk_c8
| sk_c8 = sk_c7
| inverse(sk_c4) = sk_c8
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_1726,c_27]) ).
cnf(c_8929,plain,
( inverse(sk_c4) = sk_c8
| sk_c7 = sk_c8
| inverse(sk_c4) = sk_c8
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_8928]) ).
cnf(c_8930,plain,
( inverse(sk_c4) = sk_c8
| inverse(sk_c4) = sk_c8
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_8929]) ).
cnf(c_1773,plain,
( inverse(sk_c4) = sk_c8
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_8930]) ).
cnf(c_1774,plain,
( multiply(sk_c8,sk_c4) = identity
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_1773,c_2]) ).
cnf(c_1782,plain,
( multiply(inverse(sk_c8),identity) = sk_c4
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_1774,c_584]) ).
cnf(c_8931,plain,
( sk_c4 = sk_c1
| sk_c7 = sk_c8
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_1782,c_987]) ).
cnf(c_1861,plain,
( sk_c4 = sk_c1
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_8931]) ).
cnf(c_1864,plain,
( multiply(sk_c1,sk_c8) = sk_c5
| multiply(sk_c8,sk_c7) = sk_c6
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_1861,c_8]) ).
cnf(c_1865,plain,
( multiply(sk_c1,sk_c8) = sk_c5
| multiply(sk_c1,sk_c8) = sk_c7
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_1861,c_14]) ).
cnf(c_8932,plain,
( multiply(sk_c8,sk_c5) = sk_c8
| sk_c6 = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1433,c_816]) ).
cnf(c_2209,plain,
( multiply(sk_c8,sk_c5) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8932]) ).
cnf(c_8933,plain,
( multiply(sk_c8,sk_c5) = sk_c8
| sk_c6 = sk_c7
| multiply(sk_c1,sk_c8) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1519,c_816]) ).
cnf(c_2211,plain,
( multiply(sk_c8,sk_c5) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c6
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8933]) ).
cnf(c_8934,plain,
( multiply(sk_c8,sk_c5) = sk_c8
| sk_c6 = sk_c7
| sk_c6 = sk_c7
| multiply(sk_c8,sk_c5) = sk_c8
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_2211,c_2209]) ).
cnf(c_8935,plain,
( multiply(sk_c8,sk_c5) = sk_c8
| sk_c6 = sk_c7
| multiply(sk_c8,sk_c5) = sk_c8
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8934]) ).
cnf(c_8936,plain,
( multiply(sk_c8,sk_c5) = sk_c8
| multiply(sk_c8,sk_c5) = sk_c8
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8935]) ).
cnf(c_2372,plain,
( multiply(sk_c8,sk_c5) = sk_c8
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8936]) ).
cnf(c_2379,plain,
( multiply(inverse(sk_c8),sk_c8) = sk_c5
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_2372,c_584]) ).
cnf(c_8937,plain,
( sk_c5 = identity
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_2379,c_2]) ).
cnf(c_2468,plain,
( identity = sk_c5
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8937]) ).
cnf(c_2497,plain,
( multiply(inverse(A),A) = sk_c5
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_2468,c_2]) ).
cnf(c_8938,plain,
( sk_c5 = multiply(identity,identity)
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_2497,c_288]) ).
cnf(c_2724,plain,
( multiply(identity,identity) = sk_c5
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8938]) ).
cnf(c_8939,plain,
( multiply(A,sk_c5) = multiply(A,identity)
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_2724,c_291]) ).
cnf(c_2799,plain,
( multiply(A,identity) = multiply(A,sk_c5)
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8939]) ).
cnf(c_8940,plain,
( multiply(sk_c8,identity) = sk_c7
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1397,c_2799]) ).
cnf(c_2843,plain,
( multiply(sk_c8,identity) = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8940]) ).
cnf(c_2850,plain,
( multiply(sk_c7,A) = multiply(sk_c8,A)
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_2843,c_59]) ).
cnf(c_8941,plain,
( multiply(sk_c7,sk_c1) = identity
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_813,c_2850]) ).
cnf(c_2957,plain,
( multiply(sk_c7,sk_c1) = identity
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8941]) ).
cnf(c_8942,plain,
( multiply(sk_c8,sk_c8) = sk_c6
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_2850,c_1351]) ).
cnf(c_2967,plain,
( multiply(sk_c8,sk_c8) = sk_c6
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8942]) ).
cnf(c_3014,plain,
( multiply(inverse(sk_c7),identity) = sk_c1
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_2957,c_584]) ).
cnf(c_8943,plain,
( sk_c1 = sk_c3
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_3014,c_1323]) ).
cnf(c_8944,plain,
( sk_c3 = sk_c1
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8943]) ).
cnf(c_3439,plain,
( sk_c3 = sk_c1
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8944]) ).
cnf(c_3445,plain,
( multiply(sk_c1,sk_c7) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_3439,c_11]) ).
cnf(c_3447,plain,
( multiply(sk_c1,sk_c7) = sk_c8
| multiply(sk_c2,sk_c8) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_3439,c_29]) ).
cnf(c_8945,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| sk_c6 = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_3445,c_816]) ).
cnf(c_3526,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8945]) ).
cnf(c_8946,plain,
( multiply(sk_c1,sk_c7) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c6
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1297,c_3447]) ).
cnf(c_3555,plain,
( multiply(sk_c1,sk_c7) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c6
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8946]) ).
cnf(c_8947,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| sk_c6 = sk_c7
| multiply(sk_c1,sk_c8) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_3555,c_816]) ).
cnf(c_3676,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c6
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8947]) ).
cnf(c_8948,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| sk_c6 = sk_c7
| sk_c6 = sk_c7
| multiply(sk_c8,sk_c8) = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_3676,c_3526]) ).
cnf(c_8949,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| sk_c6 = sk_c7
| multiply(sk_c8,sk_c8) = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8948]) ).
cnf(c_8950,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| multiply(sk_c8,sk_c8) = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8949]) ).
cnf(c_3971,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8950]) ).
cnf(c_8951,plain,
( sk_c7 = sk_c6
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_3971,c_2967]) ).
cnf(c_8952,plain,
( sk_c6 = sk_c7
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8951]) ).
cnf(c_8953,plain,
( sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_8952]) ).
cnf(c_3999,plain,
sk_c6 = sk_c7,
inference(copy,[status(thm)],[c_8953]) ).
cnf(c_8954,plain,
( inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c7
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_3999,c_58]) ).
cnf(c_4109,plain,
( inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(copy,[status(thm)],[c_8954]) ).
cnf(c_8955,plain,
( inverse(identity) != sk_c7
| sk_c7 != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(A,sk_c8) != sk_c7
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_3999,c_196]) ).
cnf(c_4115,plain,
( inverse(identity) != sk_c7
| sk_c7 != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(copy,[status(thm)],[c_8955]) ).
cnf(c_8956,plain,
( inverse(identity) != sk_c7
| sk_c7 != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(identity) != sk_c8
| sk_c8 != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_1,c_4115]) ).
cnf(c_8957,plain,
( inverse(identity) != sk_c7
| sk_c7 != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(identity) != sk_c8
| sk_c7 != sk_c8
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(copy,[status(thm)],[c_8956]) ).
cnf(c_4246,plain,
( inverse(identity) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(identity) != sk_c8
| sk_c7 != sk_c8
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(copy,[status(thm)],[c_8957]) ).
cnf(c_4307,plain,
( inverse(identity) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c7
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(identity) != sk_c8
| sk_c7 != sk_c8
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_3999,c_4246]) ).
cnf(c_4474,plain,
( multiply(sk_c8,sk_c7) = sk_c8
| sk_c7 = sk_c8
| multiply(sk_c8,sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_13,c_980]) ).
cnf(c_8958,plain,
( multiply(sk_c8,sk_c5) = sk_c8
| sk_c7 = sk_c8
| multiply(sk_c8,sk_c7) = sk_c6
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_1864,c_980]) ).
cnf(c_4481,plain,
( multiply(sk_c8,sk_c5) = sk_c8
| multiply(sk_c8,sk_c7) = sk_c6
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_8958]) ).
cnf(c_8959,plain,
( multiply(sk_c8,sk_c5) = sk_c8
| sk_c7 = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_1865,c_980]) ).
cnf(c_4482,plain,
( multiply(sk_c8,sk_c5) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_8959]) ).
cnf(c_8960,plain,
( sk_c8 = sk_c7
| multiply(sk_c8,sk_c7) = sk_c6
| multiply(sk_c8,sk_c7) = sk_c6
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_4481,c_7]) ).
cnf(c_8961,plain,
( sk_c7 = sk_c8
| multiply(sk_c8,sk_c7) = sk_c6
| multiply(sk_c8,sk_c7) = sk_c6
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_8960]) ).
cnf(c_8962,plain,
( sk_c7 = sk_c8
| multiply(sk_c8,sk_c7) = sk_c6
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_8961]) ).
cnf(c_4582,plain,
( multiply(sk_c8,sk_c7) = sk_c6
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_8962]) ).
cnf(c_4592,plain,
( multiply(sk_c8,sk_c7) = sk_c7
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_3999,c_4582]) ).
cnf(c_8963,plain,
( multiply(sk_c8,sk_c7) = sk_c8
| sk_c7 = sk_c8
| multiply(sk_c8,sk_c5) = sk_c8
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_4482,c_980]) ).
cnf(c_4612,plain,
( multiply(sk_c8,sk_c7) = sk_c8
| multiply(sk_c8,sk_c5) = sk_c8
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_8963]) ).
cnf(c_8964,plain,
( multiply(sk_c8,sk_c7) = sk_c8
| sk_c7 = sk_c8
| sk_c8 = sk_c7
| multiply(sk_c8,sk_c7) = sk_c8
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_4612,c_4474]) ).
cnf(c_8965,plain,
( multiply(sk_c8,sk_c7) = sk_c8
| sk_c7 = sk_c8
| sk_c7 = sk_c8
| multiply(sk_c8,sk_c7) = sk_c8
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_8964]) ).
cnf(c_8966,plain,
( multiply(sk_c8,sk_c7) = sk_c8
| sk_c7 = sk_c8
| multiply(sk_c8,sk_c7) = sk_c8
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_8965]) ).
cnf(c_8967,plain,
( multiply(sk_c8,sk_c7) = sk_c8
| multiply(sk_c8,sk_c7) = sk_c8
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_8966]) ).
cnf(c_4713,plain,
( multiply(sk_c8,sk_c7) = sk_c8
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_8967]) ).
cnf(c_8968,plain,
( sk_c8 = sk_c7
| sk_c7 = sk_c8
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_4713,c_4592]) ).
cnf(c_8969,plain,
( sk_c7 = sk_c8
| sk_c7 = sk_c8
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_8968]) ).
cnf(c_8970,plain,
( sk_c7 = sk_c8
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_8969]) ).
cnf(c_4726,plain,
sk_c7 = sk_c8,
inference(copy,[status(thm)],[c_8970]) ).
cnf(c_4809,plain,
( inverse(identity) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c7
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(identity) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(resolve,[status(thm)],[c_4726,c_4307]) ).
cnf(c_4970,plain,
( multiply(sk_c8,sk_c8) = sk_c6
| multiply(sk_c8,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_4726,c_4]) ).
cnf(c_5028,plain,
sk_c6 = sk_c8,
inference(paramod,[status(thm)],[c_4726,c_3999]) ).
cnf(c_5035,plain,
( inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(sk_c7) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_4726,c_4109]) ).
cnf(c_5108,plain,
( inverse(identity) != sk_c7
| multiply(sk_c8,sk_c8) != sk_c7
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(identity) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_4726,c_4809]) ).
cnf(c_8971,plain,
( inverse(identity) != sk_c7
| multiply(sk_c8,sk_c8) != sk_c7
| multiply(sk_c8,sk_c8) != sk_c7
| inverse(identity) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_5028,c_5108]) ).
cnf(c_5117,plain,
( inverse(identity) != sk_c7
| multiply(sk_c8,sk_c8) != sk_c7
| inverse(identity) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(copy,[status(thm)],[c_8971]) ).
cnf(c_5162,plain,
( inverse(identity) != sk_c7
| multiply(sk_c8,sk_c8) != sk_c7
| inverse(identity) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7 ),
inference(paramod,[status(thm)],[c_3999,c_5117]) ).
cnf(c_8972,plain,
( inverse(identity) != sk_c7
| multiply(sk_c8,sk_c8) != sk_c7
| inverse(identity) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_4726,c_5162]) ).
cnf(c_5165,plain,
( inverse(identity) != sk_c7
| inverse(identity) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_8972]) ).
cnf(c_8973,plain,
( multiply(sk_c8,sk_c8) = sk_c6
| multiply(sk_c8,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_4726,c_4970]) ).
cnf(c_5340,plain,
multiply(sk_c8,sk_c8) = sk_c6,
inference(copy,[status(thm)],[c_8973]) ).
cnf(c_5355,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(paramod,[status(thm)],[c_3999,c_5340]) ).
cnf(c_5356,plain,
multiply(sk_c8,sk_c8) = sk_c8,
inference(paramod,[status(thm)],[c_5028,c_5340]) ).
cnf(c_8974,plain,
( inverse(identity) != sk_c7
| inverse(identity) != sk_c8
| sk_c6 != sk_c7 ),
inference(paramod,[status(thm)],[c_5340,c_5165]) ).
cnf(c_5357,plain,
( inverse(identity) != sk_c7
| inverse(identity) != sk_c8 ),
inference(resolve,[status(thm)],[c_3999,c_8974]) ).
cnf(c_5360,plain,
( inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c8,sk_c6) != sk_c7
| inverse(sk_c7) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(resolve,[status(thm)],[c_5355,c_5035]) ).
cnf(c_8975,plain,
( inverse(identity) != sk_c8
| inverse(identity) != sk_c8 ),
inference(paramod,[status(thm)],[c_4726,c_5357]) ).
cnf(c_5376,plain,
inverse(identity) != sk_c8,
inference(copy,[status(thm)],[c_8975]) ).
cnf(c_8976,plain,
( inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7
| inverse(sk_c7) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_5028,c_5360]) ).
cnf(c_5401,plain,
( inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| inverse(sk_c7) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(resolve,[status(thm)],[c_5355,c_8976]) ).
cnf(c_5408,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c8,
inference(paramod,[status(thm)],[c_5356,c_584]) ).
cnf(c_8977,plain,
( inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| inverse(sk_c7) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c6 ),
inference(paramod,[status(thm)],[c_4726,c_5401]) ).
cnf(c_5468,plain,
( inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| inverse(sk_c7) != sk_c8 ),
inference(resolve,[status(thm)],[c_5340,c_8977]) ).
cnf(c_5492,plain,
( inverse(A) != sk_c7
| multiply(A,sk_c8) != sk_c8
| inverse(sk_c7) != sk_c8 ),
inference(paramod,[status(thm)],[c_4726,c_5468]) ).
cnf(c_5493,plain,
( inverse(sk_c8) != sk_c7
| inverse(sk_c7) != sk_c8 ),
inference(resolve,[status(thm)],[c_5492,c_5356]) ).
cnf(c_5518,plain,
( inverse(sk_c8) != sk_c7
| inverse(sk_c8) != sk_c8 ),
inference(paramod,[status(thm)],[c_4726,c_5493]) ).
cnf(c_8978,plain,
( inverse(sk_c8) != sk_c8
| inverse(sk_c8) != sk_c8 ),
inference(paramod,[status(thm)],[c_4726,c_5518]) ).
cnf(c_5547,plain,
inverse(sk_c8) != sk_c8,
inference(copy,[status(thm)],[c_8978]) ).
cnf(c_8979,plain,
sk_c8 = identity,
inference(paramod,[status(thm)],[c_5408,c_2]) ).
cnf(c_5609,plain,
identity = sk_c8,
inference(copy,[status(thm)],[c_8979]) ).
cnf(c_5635,plain,
multiply(sk_c8,A) = A,
inference(paramod,[status(thm)],[c_5609,c_1]) ).
cnf(c_8980,plain,
( sk_c4 = identity
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_5635,c_100]) ).
cnf(c_5686,plain,
( identity = sk_c4
| inverse(sk_c1) = sk_c8 ),
inference(copy,[status(thm)],[c_8980]) ).
cnf(c_5922,plain,
( multiply(sk_c8,sk_c1) = identity
| identity = sk_c4 ),
inference(paramod,[status(thm)],[c_5686,c_2]) ).
cnf(c_8135,plain,
( identity = sk_c1
| identity = sk_c4 ),
inference(paramod,[status(thm)],[c_5922,c_5635]) ).
cnf(c_8173,plain,
( sk_c4 = sk_c8
| identity = sk_c1 ),
inference(paramod,[status(thm)],[c_8135,c_5609]) ).
cnf(c_8263,plain,
( inverse(sk_c1) != sk_c8
| sk_c4 = sk_c8 ),
inference(paramod,[status(thm)],[c_8173,c_5376]) ).
cnf(c_8648,plain,
( identity = sk_c4
| sk_c4 = sk_c8 ),
inference(resolve,[status(thm)],[c_8263,c_5686]) ).
cnf(c_8981,plain,
( sk_c4 = sk_c8
| sk_c4 = sk_c8 ),
inference(paramod,[status(thm)],[c_8648,c_5609]) ).
cnf(c_8759,plain,
sk_c4 = sk_c8,
inference(copy,[status(thm)],[c_8981]) ).
cnf(c_8982,plain,
( inverse(sk_c8) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_8759,c_21]) ).
cnf(c_8762,plain,
inverse(sk_c1) = sk_c8,
inference(resolve,[status(thm)],[c_5547,c_8982]) ).
cnf(c_8780,plain,
multiply(sk_c8,sk_c1) = identity,
inference(paramod,[status(thm)],[c_8762,c_2]) ).
cnf(c_8864,plain,
identity = sk_c1,
inference(paramod,[status(thm)],[c_8780,c_5635]) ).
cnf(c_8983,plain,
inverse(sk_c1) != sk_c8,
inference(paramod,[status(thm)],[c_8864,c_5376]) ).
cnf(c_8897,plain,
$false,
inference(resolve,[status(thm)],[c_8762,c_8983]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP293-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n009.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Fri Sep 25 14:43:44 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 1852035 was started by sandbox on n009,
% 0.08/0.36 % Fri Sep 25 14:43:44 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.37
% 0.08/0.37 % From the command line: assign(max_seconds, 300).
% 142.71/19.46
% 142.71/19.46 % Assigning unary symbol inverse kb_weight 0 and highest precedence (12).
% 142.71/19.46
% 142.71/19.46 % given #500 (T,wt=19): 5032 multiply(sk_c8,sk_c7) = sk_c8 | inverse(sk_c4) = sk_c8. [para(4726(a,1),4098(a,2))].
% 142.71/19.46
% 142.71/19.46 % SZS status Unsatisfiable for theBenchmark
% 142.71/19.46
% 142.71/19.46 % Proof 1 at 2.45 (+ 0.50) seconds.
% 142.71/19.46 % Length of proof is 156.
% 142.71/19.46 % Level of proof is 51.
% 142.71/19.46 % Maximum clause weight is 66.000.
% 142.71/19.46 % Given clauses 769.
% 142.71/19.46
% 142.71/19.46 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------