%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP233-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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:25 AM UTC 2026
% Result : Unsatisfiable 46.39s 6.39s
% Output : CNFRefutation 46.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 92
% Number of leaves : 19
% Syntax : Number of formulae : 341 ( 28 unt; 0 def)
% Number of atoms : 1008 (1007 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 1105 ( 438 ~; 667 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 121 ( 0 sgn 11 !; 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,
( inverse(sk_c4) = sk_c8
| inverse(sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_1) ).
cnf(c_4,plain,
( inverse(sk_c4) = sk_c8
| inverse(sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_1]) ).
fof(prove_this_2,axiom,
( multiply(sk_c4,sk_c7) = sk_c8
| inverse(sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_2) ).
cnf(c_5,plain,
( multiply(sk_c4,sk_c7) = sk_c8
| inverse(sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_2]) ).
fof(prove_this_3,axiom,
( multiply(sk_c8,sk_c6) = sk_c7
| inverse(sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_3) ).
cnf(c_6,plain,
( multiply(sk_c8,sk_c6) = sk_c7
| inverse(sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_3]) ).
fof(prove_this_4,axiom,
( multiply(sk_c5,sk_c8) = sk_c6
| inverse(sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_4) ).
cnf(c_7,plain,
( multiply(sk_c5,sk_c8) = sk_c6
| inverse(sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_4]) ).
fof(prove_this_5,axiom,
( inverse(sk_c5) = sk_c8
| inverse(sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_5) ).
cnf(c_8,plain,
( inverse(sk_c5) = sk_c8
| inverse(sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_5]) ).
fof(prove_this_6,axiom,
( inverse(sk_c4) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_6) ).
cnf(c_9,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_6]) ).
fof(prove_this_7,axiom,
( multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_7) ).
cnf(c_10,plain,
( multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_7]) ).
fof(prove_this_8,axiom,
( multiply(sk_c8,sk_c6) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_11,plain,
( multiply(sk_c8,sk_c6) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_8]) ).
fof(prove_this_9,axiom,
( multiply(sk_c5,sk_c8) = sk_c6
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_9) ).
cnf(c_12,plain,
( multiply(sk_c5,sk_c8) = sk_c6
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_9]) ).
fof(prove_this_10,axiom,
( inverse(sk_c5) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_10) ).
cnf(c_13,plain,
( inverse(sk_c5) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_10]) ).
fof(prove_this_11,axiom,
( inverse(sk_c4) = sk_c8
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_11) ).
cnf(c_14,plain,
( inverse(sk_c4) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_11]) ).
fof(prove_this_12,axiom,
( multiply(sk_c4,sk_c7) = sk_c8
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_12) ).
cnf(c_15,plain,
( multiply(sk_c4,sk_c7) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_12]) ).
fof(prove_this_13,axiom,
( multiply(sk_c8,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_13) ).
cnf(c_16,plain,
( multiply(sk_c8,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_13]) ).
fof(prove_this_14,axiom,
( multiply(sk_c5,sk_c8) = sk_c6
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_14) ).
cnf(c_17,plain,
( multiply(sk_c5,sk_c8) = sk_c6
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_14]) ).
fof(prove_this_15,axiom,
( inverse(sk_c5) = sk_c8
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_15) ).
cnf(c_18,plain,
( inverse(sk_c5) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_15]) ).
fof(prove_this_31,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( inverse(VAR_5) != sk_c8
| multiply(VAR_5,sk_c8) != VAR_4
| multiply(sk_c8,VAR_4) != sk_c7
| multiply(VAR_3,sk_c7) != sk_c8
| inverse(VAR_3) != sk_c8
| inverse(VAR_2) != sk_c8
| multiply(VAR_2,sk_c8) != VAR_1
| multiply(sk_c8,VAR_1) != sk_c7
| inverse(VAR_0) != sk_c8
| multiply(VAR_0,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
file('theBenchmark.p',prove_this_31) ).
cnf(c_34,plain,
( inverse(F) != sk_c8
| multiply(F,sk_c8) != E
| multiply(sk_c8,E) != sk_c7
| multiply(D,sk_c7) != sk_c8
| inverse(D) != sk_c8
| inverse(C) != sk_c8
| multiply(C,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(clausify,[status(thm)],[prove_this_31]) ).
cnf(c_35,plain,
( inverse(D) != sk_c8
| multiply(D,sk_c8) != C
| multiply(sk_c8,C) != sk_c7
| multiply(B,sk_c7) != sk_c8
| inverse(B) != sk_c8
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_34]) ).
cnf(c_16058,plain,
( inverse(D) != sk_c8
| multiply(D,sk_c8) != C
| multiply(sk_c8,C) != sk_c7
| multiply(B,sk_c7) != sk_c8
| inverse(B) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_34]) ).
cnf(c_36,plain,
( inverse(D) != sk_c8
| multiply(D,sk_c8) != C
| multiply(sk_c8,C) != sk_c7
| multiply(B,sk_c7) != sk_c8
| inverse(B) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16058]) ).
cnf(c_38,plain,
( inverse(E) != sk_c8
| multiply(E,sk_c8) != D
| multiply(sk_c8,D) != sk_c7
| multiply(A,sk_c7) != sk_c8
| inverse(C) != sk_c8
| multiply(C,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_34]) ).
cnf(c_16059,plain,
( inverse(A) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7
| multiply(B,sk_c7) != sk_c8
| inverse(B) != sk_c8
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_35]) ).
cnf(c_16060,plain,
( inverse(A) != sk_c8
| multiply(B,sk_c7) != sk_c8
| inverse(B) != sk_c8
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16059]) ).
cnf(c_42,plain,
( multiply(B,sk_c7) != sk_c8
| inverse(B) != sk_c8
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16060]) ).
cnf(c_16061,plain,
( inverse(A) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| multiply(B,sk_c7) != sk_c8
| inverse(B) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_36]) ).
cnf(c_16062,plain,
( inverse(A) != sk_c8
| multiply(B,sk_c7) != sk_c8
| inverse(B) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16061]) ).
cnf(c_43,plain,
( multiply(B,sk_c7) != sk_c8
| inverse(B) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16062]) ).
cnf(c_16063,plain,
( inverse(C) != sk_c8
| multiply(sk_c8,B) != sk_c7
| multiply(A,sk_c7) != sk_c8
| inverse(C) != sk_c8
| multiply(C,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_38]) ).
cnf(c_16064,plain,
( inverse(C) != sk_c8
| multiply(A,sk_c7) != sk_c8
| inverse(C) != sk_c8
| multiply(C,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16063]) ).
cnf(c_47,plain,
( multiply(A,sk_c7) != sk_c8
| inverse(C) != sk_c8
| multiply(C,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16064]) ).
cnf(c_49,plain,
( multiply(A,sk_c7) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_42]) ).
cnf(c_52,plain,
( multiply(A,sk_c7) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_43]) ).
cnf(c_55,plain,
( multiply(sk_c8,sk_c7) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_49]) ).
cnf(c_16065,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_16066,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_16065]) ).
cnf(c_56,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_16066]) ).
cnf(c_57,plain,
( multiply(sk_c7,sk_c8) = identity
| inverse(sk_c4) = sk_c8 ),
inference(paramod,[status(thm)],[c_4,c_2]) ).
cnf(c_58,plain,
( multiply(sk_c8,sk_c4) = identity
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_4,c_2]) ).
cnf(c_65,plain,
( multiply(sk_c7,sk_c8) = identity
| multiply(sk_c5,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_7,c_2]) ).
cnf(c_66,plain,
( multiply(sk_c6,A) = multiply(sk_c5,multiply(sk_c8,A))
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_7,c_3]) ).
cnf(c_16067,plain,
( multiply(multiply(A,sk_c5),sk_c8) = multiply(A,sk_c6)
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_7,c_3]) ).
cnf(c_67,plain,
( multiply(A,multiply(sk_c5,sk_c8)) = multiply(A,sk_c6)
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_3,c_16067]) ).
cnf(c_69,plain,
( multiply(sk_c8,sk_c5) = identity
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_8,c_2]) ).
cnf(c_16068,plain,
( multiply(sk_c7,A) = multiply(sk_c1,multiply(sk_c8,A))
| multiply(sk_c5,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_12,c_3]) ).
cnf(c_81,plain,
( multiply(sk_c1,multiply(sk_c8,A)) = multiply(sk_c7,A)
| multiply(sk_c5,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_16068]) ).
cnf(c_88,plain,
( multiply(sk_c8,sk_c1) = identity
| inverse(sk_c4) = sk_c8 ),
inference(paramod,[status(thm)],[c_14,c_2]) ).
cnf(c_89,plain,
( multiply(sk_c8,sk_c4) = identity
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_14,c_2]) ).
cnf(c_90,plain,
( multiply(sk_c8,sk_c1) = identity
| multiply(sk_c4,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_15,c_2]) ).
cnf(c_93,plain,
( multiply(sk_c8,sk_c1) = identity
| multiply(sk_c8,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_16,c_2]) ).
cnf(c_99,plain,
( multiply(sk_c8,sk_c1) = identity
| inverse(sk_c5) = sk_c8 ),
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_100,plain,
( multiply(sk_c8,sk_c5) = identity
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_156,plain,
( inverse(sk_c1) = sk_c8
| inverse(sk_c4) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(resolve,[status(thm)],[c_43,c_15]) ).
cnf(c_16069,plain,
( multiply(identity,sk_c7) != sk_c8
| inverse(B) != sk_c8
| multiply(B,sk_c8) != A
| multiply(sk_c8,A) != sk_c7
| inverse(identity) != sk_c8
| sk_c8 != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_1,c_47]) ).
cnf(c_16070,plain,
( sk_c7 != sk_c8
| inverse(B) != sk_c8
| multiply(B,sk_c8) != A
| multiply(sk_c8,A) != sk_c7
| inverse(identity) != sk_c8
| sk_c8 != sk_c7
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_1,c_16069]) ).
cnf(c_16071,plain,
( sk_c7 != sk_c8
| inverse(B) != sk_c8
| multiply(B,sk_c8) != A
| multiply(sk_c8,A) != sk_c7
| inverse(identity) != sk_c8
| sk_c7 != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16070]) ).
cnf(c_166,plain,
( inverse(B) != sk_c8
| multiply(B,sk_c8) != A
| multiply(sk_c8,A) != sk_c7
| inverse(identity) != sk_c8
| sk_c7 != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16071]) ).
cnf(c_16072,plain,
( multiply(identity,sk_c8) != A
| multiply(sk_c8,A) != sk_c7
| inverse(identity) != sk_c8
| sk_c7 != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_166]) ).
cnf(c_167,plain,
( sk_c8 != A
| multiply(sk_c8,A) != sk_c7
| inverse(identity) != sk_c8
| sk_c7 != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_1,c_16072]) ).
cnf(c_176,plain,
( inverse(sk_c4) = sk_c8
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7 ),
inference(resolve,[status(thm)],[c_52,c_4]) ).
cnf(c_218,plain,
( multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c8,sk_c7) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7 ),
inference(resolve,[status(thm)],[c_55,c_5]) ).
cnf(c_223,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_56]) ).
cnf(c_227,plain,
( multiply(sk_c7,multiply(sk_c8,A)) = A
| multiply(sk_c4,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_5,c_56]) ).
cnf(c_229,plain,
( multiply(sk_c7,multiply(sk_c8,A)) = A
| multiply(sk_c8,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_6,c_56]) ).
cnf(c_236,plain,
( multiply(sk_c8,multiply(sk_c4,A)) = A
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_9,c_56]) ).
cnf(c_239,plain,
( multiply(inverse(sk_c1),sk_c7) = sk_c8
| multiply(sk_c8,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_11,c_56]) ).
cnf(c_241,plain,
( multiply(inverse(sk_c1),sk_c7) = sk_c8
| multiply(sk_c5,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_12,c_56]) ).
cnf(c_285,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_56,c_56]) ).
cnf(c_286,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_285,c_223]) ).
cnf(c_16073,plain,
( multiply(inverse(sk_c7),identity) = sk_c8
| inverse(sk_c4) = sk_c8 ),
inference(paramod,[status(thm)],[c_57,c_56]) ).
cnf(c_293,plain,
( inverse(sk_c7) = sk_c8
| inverse(sk_c4) = sk_c8 ),
inference(paramod,[status(thm)],[c_286,c_16073]) ).
cnf(c_347,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_286,c_2]) ).
cnf(c_16074,plain,
( sk_c8 != identity
| sk_c8 != sk_c7
| inverse(identity) != sk_c8
| sk_c7 != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_286,c_167]) ).
cnf(c_16075,plain,
( sk_c8 != identity
| sk_c8 != sk_c7
| identity != sk_c8
| sk_c7 != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_347,c_16074]) ).
cnf(c_16076,plain,
( sk_c8 != identity
| sk_c7 != sk_c8
| identity != sk_c8
| sk_c7 != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16075]) ).
cnf(c_16077,plain,
( identity != sk_c8
| sk_c7 != sk_c8
| identity != sk_c8
| sk_c7 != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16076]) ).
cnf(c_16078,plain,
( identity != sk_c8
| identity != sk_c8
| sk_c7 != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16077]) ).
cnf(c_349,plain,
( identity != sk_c8
| sk_c7 != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16078]) ).
cnf(c_16079,plain,
( multiply(inverse(sk_c8),identity) = sk_c4
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_58,c_56]) ).
cnf(c_382,plain,
( inverse(sk_c8) = sk_c4
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_286,c_16079]) ).
cnf(c_16080,plain,
( multiply(inverse(sk_c8),identity) = sk_c5
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_69,c_56]) ).
cnf(c_487,plain,
( inverse(sk_c8) = sk_c5
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_286,c_16080]) ).
cnf(c_496,plain,
( multiply(sk_c5,sk_c8) = identity
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_487,c_2]) ).
cnf(c_16081,plain,
( sk_c5 = sk_c4
| inverse(sk_c8) = sk_c7
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_487,c_382]) ).
cnf(c_503,plain,
( sk_c5 = sk_c4
| inverse(sk_c8) = sk_c7 ),
inference(copy,[status(thm)],[c_16081]) ).
cnf(c_509,plain,
( identity != sk_c8
| sk_c7 != sk_c8
| sk_c5 = sk_c4 ),
inference(resolve,[status(thm)],[c_503,c_349]) ).
cnf(c_516,plain,
( multiply(sk_c7,sk_c8) = identity
| sk_c5 = sk_c4 ),
inference(paramod,[status(thm)],[c_503,c_2]) ).
cnf(c_16082,plain,
( multiply(inverse(sk_c7),identity) = sk_c8
| sk_c5 = sk_c4 ),
inference(paramod,[status(thm)],[c_516,c_56]) ).
cnf(c_592,plain,
( inverse(sk_c7) = sk_c8
| sk_c5 = sk_c4 ),
inference(paramod,[status(thm)],[c_286,c_16082]) ).
cnf(c_16083,plain,
( multiply(inverse(sk_c8),identity) = sk_c1
| inverse(sk_c4) = sk_c8 ),
inference(paramod,[status(thm)],[c_88,c_56]) ).
cnf(c_621,plain,
( inverse(sk_c8) = sk_c1
| inverse(sk_c4) = sk_c8 ),
inference(paramod,[status(thm)],[c_286,c_16083]) ).
cnf(c_641,plain,
( multiply(sk_c1,sk_c8) = identity
| inverse(sk_c4) = sk_c8 ),
inference(paramod,[status(thm)],[c_621,c_2]) ).
cnf(c_16084,plain,
( inverse(sk_c4) = sk_c8
| sk_c1 = sk_c7
| inverse(sk_c4) = sk_c8 ),
inference(paramod,[status(thm)],[c_621,c_4]) ).
cnf(c_642,plain,
( sk_c1 = sk_c7
| inverse(sk_c4) = sk_c8 ),
inference(copy,[status(thm)],[c_16084]) ).
cnf(c_657,plain,
( multiply(sk_c8,sk_c4) = identity
| sk_c1 = sk_c7 ),
inference(paramod,[status(thm)],[c_642,c_2]) ).
cnf(c_16085,plain,
( multiply(inverse(sk_c8),identity) = sk_c4
| sk_c1 = sk_c7 ),
inference(paramod,[status(thm)],[c_657,c_56]) ).
cnf(c_665,plain,
( inverse(sk_c8) = sk_c4
| sk_c1 = sk_c7 ),
inference(paramod,[status(thm)],[c_286,c_16085]) ).
cnf(c_666,plain,
( multiply(sk_c4,sk_c8) = identity
| sk_c1 = sk_c7 ),
inference(paramod,[status(thm)],[c_665,c_2]) ).
cnf(c_16086,plain,
( multiply(inverse(sk_c8),identity) = sk_c4
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_89,c_56]) ).
cnf(c_741,plain,
( inverse(sk_c8) = sk_c4
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_286,c_16086]) ).
cnf(c_746,plain,
( multiply(sk_c4,sk_c8) = identity
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_741,c_2]) ).
cnf(c_16087,plain,
( inverse(sk_c8) = sk_c4
| inverse(sk_c7) = sk_c8
| inverse(sk_c8) = sk_c4 ),
inference(paramod,[status(thm)],[c_665,c_741]) ).
cnf(c_759,plain,
( inverse(sk_c7) = sk_c8
| inverse(sk_c8) = sk_c4 ),
inference(copy,[status(thm)],[c_16087]) ).
cnf(c_16088,plain,
( multiply(inverse(sk_c8),identity) = sk_c1
| inverse(sk_c5) = sk_c8 ),
inference(paramod,[status(thm)],[c_99,c_56]) ).
cnf(c_787,plain,
( inverse(sk_c8) = sk_c1
| inverse(sk_c5) = sk_c8 ),
inference(paramod,[status(thm)],[c_286,c_16088]) ).
cnf(c_788,plain,
( identity != sk_c8
| sk_c7 != sk_c8
| multiply(A,multiply(sk_c5,sk_c8)) = multiply(A,sk_c6) ),
inference(resolve,[status(thm)],[c_67,c_349]) ).
cnf(c_16089,plain,
( multiply(sk_c6,sk_c6) = multiply(sk_c5,multiply(sk_c8,multiply(sk_c5,sk_c8)))
| inverse(sk_c8) = sk_c7
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_67,c_66]) ).
cnf(c_799,plain,
( multiply(sk_c6,sk_c6) = multiply(sk_c5,multiply(sk_c8,multiply(sk_c5,sk_c8)))
| inverse(sk_c8) = sk_c7 ),
inference(copy,[status(thm)],[c_16089]) ).
cnf(c_814,plain,
( multiply(sk_c1,sk_c8) = identity
| inverse(sk_c5) = sk_c8 ),
inference(paramod,[status(thm)],[c_787,c_2]) ).
cnf(c_16090,plain,
( multiply(inverse(sk_c8),identity) = sk_c5
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_100,c_56]) ).
cnf(c_909,plain,
( inverse(sk_c8) = sk_c5
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_286,c_16090]) ).
cnf(c_16091,plain,
( sk_c5 = sk_c4
| inverse(sk_c1) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_909,c_741]) ).
cnf(c_926,plain,
( sk_c5 = sk_c4
| inverse(sk_c1) = sk_c8 ),
inference(copy,[status(thm)],[c_16091]) ).
cnf(c_16092,plain,
( multiply(sk_c4,sk_c8) = sk_c6
| inverse(sk_c1) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_926,c_17]) ).
cnf(c_937,plain,
( multiply(sk_c4,sk_c8) = sk_c6
| inverse(sk_c1) = sk_c8 ),
inference(copy,[status(thm)],[c_16092]) ).
cnf(c_16093,plain,
( multiply(sk_c1,multiply(sk_c8,sk_c8)) = identity
| multiply(sk_c5,sk_c8) = sk_c6
| multiply(sk_c5,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_65,c_81]) ).
cnf(c_1377,plain,
( multiply(sk_c1,multiply(sk_c8,sk_c8)) = identity
| multiply(sk_c5,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_16093]) ).
cnf(c_16094,plain,
( identity = sk_c6
| inverse(sk_c8) = sk_c7
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_496,c_7]) ).
cnf(c_1908,plain,
( identity = sk_c6
| inverse(sk_c8) = sk_c7 ),
inference(copy,[status(thm)],[c_16094]) ).
cnf(c_1916,plain,
( identity != sk_c8
| sk_c7 != sk_c8
| identity = sk_c6 ),
inference(resolve,[status(thm)],[c_1908,c_349]) ).
cnf(c_16095,plain,
( inverse(sk_c4) = sk_c8
| identity = sk_c7
| inverse(sk_c4) = sk_c8 ),
inference(paramod,[status(thm)],[c_641,c_9]) ).
cnf(c_2376,plain,
( identity = sk_c7
| inverse(sk_c4) = sk_c8 ),
inference(copy,[status(thm)],[c_16095]) ).
cnf(c_2389,plain,
( multiply(sk_c8,sk_c4) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2376,c_2]) ).
cnf(c_16096,plain,
( multiply(inverse(sk_c8),identity) = sk_c4
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2389,c_56]) ).
cnf(c_2402,plain,
( inverse(sk_c8) = sk_c4
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_286,c_16096]) ).
cnf(c_2438,plain,
( inverse(sk_c7) = identity
| inverse(sk_c8) = sk_c4 ),
inference(paramod,[status(thm)],[c_2402,c_347]) ).
cnf(c_16097,plain,
( identity = sk_c8
| inverse(sk_c8) = sk_c4
| inverse(sk_c8) = sk_c4 ),
inference(paramod,[status(thm)],[c_2438,c_759]) ).
cnf(c_2818,plain,
( identity = sk_c8
| inverse(sk_c8) = sk_c4 ),
inference(copy,[status(thm)],[c_16097]) ).
cnf(c_2819,plain,
( multiply(A,multiply(sk_c5,sk_c8)) = multiply(A,sk_c6)
| sk_c4 = sk_c7
| inverse(sk_c7) = identity ),
inference(paramod,[status(thm)],[c_2438,c_67]) ).
cnf(c_2832,plain,
( multiply(sk_c4,sk_c8) = identity
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_2818,c_2]) ).
cnf(c_16098,plain,
( inverse(sk_c8) = sk_c4
| sk_c8 = sk_c7
| inverse(sk_c8) = sk_c4 ),
inference(paramod,[status(thm)],[c_2818,c_2402]) ).
cnf(c_16099,plain,
( inverse(sk_c8) = sk_c4
| sk_c7 = sk_c8
| inverse(sk_c8) = sk_c4 ),
inference(copy,[status(thm)],[c_16098]) ).
cnf(c_2872,plain,
( sk_c7 = sk_c8
| inverse(sk_c8) = sk_c4 ),
inference(copy,[status(thm)],[c_16099]) ).
cnf(c_3055,plain,
( multiply(sk_c8,sk_c6) = sk_c7
| sk_c4 = sk_c7
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_2872,c_6]) ).
cnf(c_16100,plain,
( inverse(sk_c5) = sk_c8
| identity = sk_c7
| inverse(sk_c5) = sk_c8 ),
inference(paramod,[status(thm)],[c_814,c_13]) ).
cnf(c_6263,plain,
( identity = sk_c7
| inverse(sk_c5) = sk_c8 ),
inference(copy,[status(thm)],[c_16100]) ).
cnf(c_6285,plain,
( multiply(sk_c8,sk_c5) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_6263,c_2]) ).
cnf(c_16101,plain,
( multiply(inverse(sk_c8),identity) = sk_c5
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_6285,c_56]) ).
cnf(c_6316,plain,
( inverse(sk_c8) = sk_c5
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_286,c_16101]) ).
cnf(c_16102,plain,
( sk_c5 = sk_c4
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_6316,c_2402]) ).
cnf(c_6465,plain,
( sk_c5 = sk_c4
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_16102]) ).
cnf(c_6495,plain,
( inverse(sk_c7) = identity
| sk_c5 = sk_c4 ),
inference(paramod,[status(thm)],[c_6465,c_347]) ).
cnf(c_16103,plain,
( sk_c7 != sk_c8
| sk_c7 != sk_c8
| sk_c5 = sk_c4
| sk_c5 = sk_c4 ),
inference(paramod,[status(thm)],[c_6465,c_509]) ).
cnf(c_16104,plain,
( sk_c7 != sk_c8
| sk_c7 != sk_c8
| sk_c5 = sk_c4 ),
inference(copy,[status(thm)],[c_16103]) ).
cnf(c_6497,plain,
( sk_c7 != sk_c8
| sk_c5 = sk_c4 ),
inference(copy,[status(thm)],[c_16104]) ).
cnf(c_16105,plain,
( identity = sk_c8
| sk_c5 = sk_c4
| sk_c5 = sk_c4 ),
inference(paramod,[status(thm)],[c_6495,c_592]) ).
cnf(c_6603,plain,
( identity = sk_c8
| sk_c5 = sk_c4 ),
inference(copy,[status(thm)],[c_16105]) ).
cnf(c_16106,plain,
( sk_c5 = sk_c4
| sk_c8 = sk_c7
| sk_c5 = sk_c4 ),
inference(paramod,[status(thm)],[c_6603,c_6465]) ).
cnf(c_16107,plain,
( sk_c5 = sk_c4
| sk_c7 = sk_c8
| sk_c5 = sk_c4 ),
inference(copy,[status(thm)],[c_16106]) ).
cnf(c_6756,plain,
( sk_c7 = sk_c8
| sk_c5 = sk_c4 ),
inference(copy,[status(thm)],[c_16107]) ).
cnf(c_16108,plain,
( sk_c5 = sk_c4
| sk_c5 = sk_c4 ),
inference(resolve,[status(thm)],[c_6756,c_6497]) ).
cnf(c_6757,plain,
sk_c5 = sk_c4,
inference(copy,[status(thm)],[c_16108]) ).
cnf(c_7101,plain,
( multiply(A,multiply(sk_c4,sk_c8)) = multiply(A,sk_c6)
| sk_c4 = sk_c7
| inverse(sk_c7) = identity ),
inference(paramod,[status(thm)],[c_6757,c_2819]) ).
cnf(c_7181,plain,
( multiply(sk_c1,multiply(sk_c8,sk_c8)) = identity
| multiply(sk_c4,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_6757,c_1377]) ).
cnf(c_16109,plain,
( multiply(sk_c6,sk_c6) = multiply(sk_c4,multiply(sk_c8,multiply(sk_c5,sk_c8)))
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_6757,c_799]) ).
cnf(c_7191,plain,
( multiply(sk_c6,sk_c6) = multiply(sk_c4,multiply(sk_c8,multiply(sk_c4,sk_c8)))
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_6757,c_16109]) ).
cnf(c_7200,plain,
( identity != sk_c8
| sk_c7 != sk_c8
| multiply(A,multiply(sk_c4,sk_c8)) = multiply(A,sk_c6) ),
inference(paramod,[status(thm)],[c_6757,c_788]) ).
cnf(c_7228,plain,
( multiply(inverse(sk_c1),sk_c7) = sk_c8
| multiply(sk_c4,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_6757,c_241]) ).
cnf(c_16110,plain,
( sk_c6 = identity
| inverse(sk_c1) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_937,c_746]) ).
cnf(c_16111,plain,
( identity = sk_c6
| inverse(sk_c1) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(copy,[status(thm)],[c_16110]) ).
cnf(c_7266,plain,
( identity = sk_c6
| inverse(sk_c1) = sk_c8 ),
inference(copy,[status(thm)],[c_16111]) ).
cnf(c_7275,plain,
( multiply(sk_c8,sk_c1) = identity
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_7266,c_2]) ).
cnf(c_16112,plain,
( inverse(sk_c1) = sk_c8
| inverse(sk_c4) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| sk_c4 != sk_c7
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_741,c_156]) ).
cnf(c_7367,plain,
( inverse(sk_c4) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| sk_c4 != sk_c7
| inverse(sk_c1) = sk_c8 ),
inference(copy,[status(thm)],[c_16112]) ).
cnf(c_16113,plain,
( multiply(inverse(sk_c8),identity) = sk_c1
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_7275,c_56]) ).
cnf(c_7383,plain,
( inverse(sk_c8) = sk_c1
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_286,c_16113]) ).
cnf(c_16114,plain,
( identity = sk_c6
| sk_c1 = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_7383,c_1908]) ).
cnf(c_7437,plain,
( sk_c1 = sk_c7
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_16114]) ).
cnf(c_7466,plain,
( multiply(A,sk_c6) = A
| sk_c1 = sk_c7 ),
inference(paramod,[status(thm)],[c_7437,c_286]) ).
cnf(c_16115,plain,
( inverse(sk_c4) = sk_c8
| inverse(sk_c4) = sk_c8
| multiply(sk_c7,sk_c7) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c7 ),
inference(resolve,[status(thm)],[c_176,c_293]) ).
cnf(c_8325,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c7,sk_c7) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16115]) ).
cnf(c_16116,plain,
( multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c8,sk_c7) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| sk_c7 != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7
| multiply(sk_c4,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_5,c_218]) ).
cnf(c_8937,plain,
( multiply(sk_c8,sk_c7) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| sk_c7 != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7
| multiply(sk_c4,sk_c7) = sk_c8 ),
inference(copy,[status(thm)],[c_16116]) ).
cnf(c_16117,plain,
( multiply(sk_c7,identity) = sk_c1
| multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c4,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_90,c_227]) ).
cnf(c_16118,plain,
( sk_c7 = sk_c1
| multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c4,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_286,c_16117]) ).
cnf(c_16119,plain,
( sk_c1 = sk_c7
| multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c4,sk_c7) = sk_c8 ),
inference(copy,[status(thm)],[c_16118]) ).
cnf(c_9380,plain,
( sk_c1 = sk_c7
| multiply(sk_c4,sk_c7) = sk_c8 ),
inference(copy,[status(thm)],[c_16119]) ).
cnf(c_16120,plain,
( multiply(sk_c7,identity) = sk_c1
| multiply(sk_c8,sk_c6) = sk_c7
| multiply(sk_c8,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_93,c_229]) ).
cnf(c_16121,plain,
( sk_c7 = sk_c1
| multiply(sk_c8,sk_c6) = sk_c7
| multiply(sk_c8,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_286,c_16120]) ).
cnf(c_16122,plain,
( sk_c1 = sk_c7
| multiply(sk_c8,sk_c6) = sk_c7
| multiply(sk_c8,sk_c6) = sk_c7 ),
inference(copy,[status(thm)],[c_16121]) ).
cnf(c_9534,plain,
( sk_c1 = sk_c7
| multiply(sk_c8,sk_c6) = sk_c7 ),
inference(copy,[status(thm)],[c_16122]) ).
cnf(c_16123,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_10,c_236]) ).
cnf(c_9766,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(copy,[status(thm)],[c_16123]) ).
cnf(c_16124,plain,
( sk_c7 = sk_c8
| sk_c1 = sk_c7
| sk_c1 = sk_c7 ),
inference(paramod,[status(thm)],[c_9534,c_7466]) ).
cnf(c_10225,plain,
( sk_c7 = sk_c8
| sk_c1 = sk_c7 ),
inference(copy,[status(thm)],[c_16124]) ).
cnf(c_16125,plain,
( multiply(inverse(sk_c7),sk_c7) = sk_c8
| multiply(sk_c8,sk_c6) = sk_c7
| multiply(sk_c8,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_9534,c_239]) ).
cnf(c_16126,plain,
( identity = sk_c8
| multiply(sk_c8,sk_c6) = sk_c7
| multiply(sk_c8,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_16125]) ).
cnf(c_10228,plain,
( identity = sk_c8
| multiply(sk_c8,sk_c6) = sk_c7 ),
inference(copy,[status(thm)],[c_16126]) ).
cnf(c_16127,plain,
( sk_c1 = sk_c7
| multiply(sk_c4,sk_c8) = sk_c8
| sk_c1 = sk_c7 ),
inference(paramod,[status(thm)],[c_10225,c_9380]) ).
cnf(c_10287,plain,
( multiply(sk_c4,sk_c8) = sk_c8
| sk_c1 = sk_c7 ),
inference(copy,[status(thm)],[c_16127]) ).
cnf(c_10524,plain,
( inverse(sk_c8) = identity
| multiply(sk_c8,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_10228,c_347]) ).
cnf(c_16128,plain,
( sk_c8 = identity
| sk_c1 = sk_c7
| sk_c1 = sk_c7 ),
inference(paramod,[status(thm)],[c_10287,c_666]) ).
cnf(c_16129,plain,
( identity = sk_c8
| sk_c1 = sk_c7
| sk_c1 = sk_c7 ),
inference(copy,[status(thm)],[c_16128]) ).
cnf(c_10929,plain,
( identity = sk_c8
| sk_c1 = sk_c7 ),
inference(copy,[status(thm)],[c_16129]) ).
cnf(c_10972,plain,
( inverse(sk_c8) = identity
| sk_c1 = sk_c7 ),
inference(paramod,[status(thm)],[c_10929,c_347]) ).
cnf(c_16130,plain,
( inverse(sk_c8) = sk_c8
| sk_c1 = sk_c7
| sk_c1 = sk_c7 ),
inference(paramod,[status(thm)],[c_10929,c_10972]) ).
cnf(c_11094,plain,
( inverse(sk_c8) = sk_c8
| sk_c1 = sk_c7 ),
inference(copy,[status(thm)],[c_16130]) ).
cnf(c_16131,plain,
( identity != sk_c8
| sk_c7 != sk_c8
| sk_c8 != sk_c7
| sk_c1 = sk_c7 ),
inference(paramod,[status(thm)],[c_11094,c_349]) ).
cnf(c_16132,plain,
( identity != sk_c8
| sk_c7 != sk_c8
| sk_c7 != sk_c8
| sk_c1 = sk_c7 ),
inference(copy,[status(thm)],[c_16131]) ).
cnf(c_11832,plain,
( identity != sk_c8
| sk_c7 != sk_c8
| sk_c1 = sk_c7 ),
inference(copy,[status(thm)],[c_16132]) ).
cnf(c_16133,plain,
( sk_c1 = sk_c7
| identity != sk_c8
| sk_c1 = sk_c7 ),
inference(resolve,[status(thm)],[c_11832,c_10225]) ).
cnf(c_11946,plain,
( identity != sk_c8
| sk_c1 = sk_c7 ),
inference(copy,[status(thm)],[c_16133]) ).
cnf(c_16134,plain,
( sk_c1 = sk_c7
| sk_c1 = sk_c7 ),
inference(resolve,[status(thm)],[c_11946,c_10929]) ).
cnf(c_11952,plain,
sk_c1 = sk_c7,
inference(copy,[status(thm)],[c_16134]) ).
cnf(c_12093,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| multiply(sk_c7,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_11952,c_9766]) ).
cnf(c_12210,plain,
( inverse(sk_c4) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| sk_c4 != sk_c7
| inverse(sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_11952,c_7367]) ).
cnf(c_16135,plain,
( multiply(inverse(sk_c7),sk_c7) = sk_c8
| multiply(sk_c4,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_11952,c_7228]) ).
cnf(c_12219,plain,
( identity = sk_c8
| multiply(sk_c4,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_2,c_16135]) ).
cnf(c_12228,plain,
( multiply(sk_c7,multiply(sk_c8,sk_c8)) = identity
| multiply(sk_c4,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_11952,c_7181]) ).
cnf(c_16136,plain,
( sk_c6 = identity
| identity = sk_c8
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_12219,c_2832]) ).
cnf(c_16137,plain,
( identity = sk_c6
| identity = sk_c8
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_16136]) ).
cnf(c_13079,plain,
( identity = sk_c6
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_16137]) ).
cnf(c_16138,plain,
( sk_c7 != sk_c8
| identity = sk_c6
| identity = sk_c6 ),
inference(resolve,[status(thm)],[c_13079,c_1916]) ).
cnf(c_13108,plain,
( sk_c7 != sk_c8
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_16138]) ).
cnf(c_13116,plain,
( inverse(sk_c8) = identity
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_13079,c_347]) ).
cnf(c_16139,plain,
( identity = sk_c6
| identity = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_13116,c_1908]) ).
cnf(c_13157,plain,
( identity = sk_c7
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_16139]) ).
cnf(c_16140,plain,
( identity = sk_c6
| sk_c7 = sk_c8
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_13157,c_13079]) ).
cnf(c_13234,plain,
( sk_c7 = sk_c8
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_16140]) ).
cnf(c_16141,plain,
( identity = sk_c6
| identity = sk_c6 ),
inference(resolve,[status(thm)],[c_13234,c_13108]) ).
cnf(c_13556,plain,
identity = sk_c6,
inference(copy,[status(thm)],[c_16141]) ).
cnf(c_13893,plain,
( multiply(sk_c7,multiply(sk_c8,sk_c8)) = sk_c6
| multiply(sk_c4,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_13556,c_12228]) ).
cnf(c_13947,plain,
( inverse(sk_c8) = sk_c6
| multiply(sk_c8,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_13556,c_10524]) ).
cnf(c_13971,plain,
( sk_c6 = sk_c8
| multiply(sk_c8,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_13556,c_10228]) ).
cnf(c_14159,plain,
( sk_c6 != sk_c8
| sk_c7 != sk_c8
| multiply(A,multiply(sk_c4,sk_c8)) = multiply(A,sk_c6) ),
inference(paramod,[status(thm)],[c_13556,c_7200]) ).
cnf(c_14164,plain,
( multiply(A,multiply(sk_c4,sk_c8)) = multiply(A,sk_c6)
| sk_c4 = sk_c7
| inverse(sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_13556,c_7101]) ).
cnf(c_14515,plain,
multiply(A,sk_c6) = A,
inference(paramod,[status(thm)],[c_13556,c_286]) ).
cnf(c_14570,plain,
( multiply(A,multiply(sk_c4,sk_c8)) = A
| sk_c4 = sk_c7
| inverse(sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_14515,c_14164]) ).
cnf(c_14572,plain,
( sk_c6 != sk_c8
| sk_c7 != sk_c8
| multiply(A,multiply(sk_c4,sk_c8)) = A ),
inference(paramod,[status(thm)],[c_14515,c_14159]) ).
cnf(c_16142,plain,
( sk_c6 = sk_c8
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_14515,c_13971]) ).
cnf(c_14575,plain,
( sk_c6 = sk_c8
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_16142]) ).
cnf(c_16143,plain,
( inverse(sk_c8) = sk_c6
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_14515,c_13947]) ).
cnf(c_14577,plain,
( inverse(sk_c8) = sk_c6
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_16143]) ).
cnf(c_16144,plain,
( sk_c6 = multiply(sk_c4,multiply(sk_c8,multiply(sk_c4,sk_c8)))
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_14515,c_7191]) ).
cnf(c_14796,plain,
( multiply(sk_c4,multiply(sk_c8,multiply(sk_c4,sk_c8))) = sk_c6
| inverse(sk_c8) = sk_c7 ),
inference(copy,[status(thm)],[c_16144]) ).
cnf(c_16145,plain,
( sk_c8 = sk_c7
| sk_c4 = sk_c7
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_14515,c_3055]) ).
cnf(c_16146,plain,
( sk_c7 = sk_c8
| sk_c4 = sk_c7
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_16145]) ).
cnf(c_14873,plain,
( sk_c4 = sk_c7
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_16146]) ).
cnf(c_16147,plain,
( sk_c7 = sk_c8
| sk_c6 = sk_c4
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_14577,c_2872]) ).
cnf(c_15208,plain,
( sk_c6 = sk_c4
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_16147]) ).
cnf(c_16148,plain,
( sk_c4 = sk_c8
| sk_c7 = sk_c8
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_15208,c_14575]) ).
cnf(c_15343,plain,
( sk_c4 = sk_c8
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_16148]) ).
cnf(c_16149,plain,
( sk_c8 = sk_c7
| sk_c7 = sk_c8
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_15343,c_14873]) ).
cnf(c_16150,plain,
( sk_c7 = sk_c8
| sk_c7 = sk_c8
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_16149]) ).
cnf(c_16151,plain,
( sk_c7 = sk_c8
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_16150]) ).
cnf(c_15411,plain,
sk_c7 = sk_c8,
inference(copy,[status(thm)],[c_16151]) ).
cnf(c_15562,plain,
( multiply(sk_c4,multiply(sk_c8,multiply(sk_c4,sk_c8))) = sk_c6
| inverse(sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_14796]) ).
cnf(c_16152,plain,
( sk_c6 != sk_c8
| sk_c8 != sk_c8
| multiply(A,multiply(sk_c4,sk_c8)) = A ),
inference(paramod,[status(thm)],[c_15411,c_14572]) ).
cnf(c_15576,plain,
( sk_c6 != sk_c8
| multiply(A,multiply(sk_c4,sk_c8)) = A ),
inference(copy,[status(thm)],[c_16152]) ).
cnf(c_16153,plain,
( multiply(A,multiply(sk_c4,sk_c8)) = A
| sk_c4 = sk_c7
| inverse(sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_15411,c_14570]) ).
cnf(c_15577,plain,
( multiply(A,multiply(sk_c4,sk_c8)) = A
| sk_c4 = sk_c8
| inverse(sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_15411,c_16153]) ).
cnf(c_15678,plain,
( multiply(sk_c8,multiply(sk_c8,sk_c8)) = sk_c6
| multiply(sk_c4,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_15411,c_13893]) ).
cnf(c_16154,plain,
( inverse(sk_c4) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| sk_c4 != sk_c7
| inverse(sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_12210]) ).
cnf(c_16155,plain,
( inverse(sk_c4) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| sk_c4 != sk_c8
| inverse(sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_16154]) ).
cnf(c_16156,plain,
( inverse(sk_c4) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c8
| sk_c4 != sk_c8
| inverse(sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_16155]) ).
cnf(c_16157,plain,
( inverse(sk_c4) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c8
| sk_c4 != sk_c8
| inverse(sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_16156]) ).
cnf(c_15834,plain,
( inverse(sk_c4) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c8
| sk_c4 != sk_c8
| inverse(sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_16157]) ).
cnf(c_16158,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| multiply(sk_c8,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_15411,c_12093]) ).
cnf(c_16159,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| multiply(sk_c8,sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_16158]) ).
cnf(c_16160,plain,
( multiply(sk_c8,sk_c8) = sk_c8
| multiply(sk_c8,sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_16159]) ).
cnf(c_15852,plain,
multiply(sk_c8,sk_c8) = sk_c8,
inference(copy,[status(thm)],[c_16160]) ).
cnf(c_16161,plain,
( multiply(sk_c8,sk_c7) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| sk_c7 != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7
| multiply(sk_c4,sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_8937]) ).
cnf(c_16162,plain,
( multiply(sk_c8,sk_c7) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| sk_c7 != sk_c8
| sk_c8 != sk_c7
| multiply(sk_c4,sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15852,c_16161]) ).
cnf(c_16163,plain,
( multiply(sk_c8,sk_c7) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| sk_c7 != sk_c8
| sk_c8 != sk_c8
| multiply(sk_c4,sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_16162]) ).
cnf(c_16164,plain,
( multiply(sk_c8,sk_c7) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c8
| multiply(sk_c4,sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_16163]) ).
cnf(c_16165,plain,
( multiply(sk_c8,sk_c7) != sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c8
| multiply(sk_c4,sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15852,c_16164]) ).
cnf(c_16166,plain,
( multiply(sk_c8,sk_c8) != sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c8
| multiply(sk_c4,sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_16165]) ).
cnf(c_16167,plain,
( sk_c8 != sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c8
| multiply(sk_c4,sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15852,c_16166]) ).
cnf(c_16168,plain,
( sk_c8 != sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c8
| multiply(sk_c4,sk_c8) = sk_c8 ),
inference(copy,[status(thm)],[c_16167]) ).
cnf(c_16169,plain,
( sk_c8 != sk_c8
| sk_c8 != sk_c8
| multiply(sk_c4,sk_c8) = sk_c8 ),
inference(copy,[status(thm)],[c_16168]) ).
cnf(c_16170,plain,
( sk_c8 != sk_c8
| multiply(sk_c4,sk_c8) = sk_c8 ),
inference(copy,[status(thm)],[c_16169]) ).
cnf(c_15972,plain,
multiply(sk_c4,sk_c8) = sk_c8,
inference(copy,[status(thm)],[c_16170]) ).
cnf(c_16171,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c7,sk_c7) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| multiply(sk_c8,sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_15411,c_8325]) ).
cnf(c_16172,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c7,sk_c7) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| sk_c8 != sk_c7 ),
inference(paramod,[status(thm)],[c_15852,c_16171]) ).
cnf(c_16173,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c7,sk_c7) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c7
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_16172]) ).
cnf(c_16174,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c7,sk_c7) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_16173]) ).
cnf(c_16175,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c7,sk_c7) != sk_c8
| sk_c8 != sk_c7
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_15852,c_16174]) ).
cnf(c_16176,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c7,sk_c7) != sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_16175]) ).
cnf(c_16177,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c8,sk_c7) != sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_16176]) ).
cnf(c_16178,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_16177]) ).
cnf(c_16179,plain,
( inverse(sk_c4) = sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_15852,c_16178]) ).
cnf(c_16180,plain,
( inverse(sk_c4) = sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c8 ),
inference(copy,[status(thm)],[c_16179]) ).
cnf(c_16181,plain,
( inverse(sk_c4) = sk_c8
| sk_c8 != sk_c8 ),
inference(copy,[status(thm)],[c_16180]) ).
cnf(c_15993,plain,
inverse(sk_c4) = sk_c8,
inference(copy,[status(thm)],[c_16181]) ).
cnf(c_16182,plain,
( multiply(sk_c8,sk_c7) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c7
| inverse(sk_c8) != sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_55]) ).
cnf(c_16183,plain,
( multiply(sk_c8,sk_c7) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c8
| sk_c8 != sk_c7
| inverse(sk_c8) != sk_c8 ),
inference(paramod,[status(thm)],[c_15852,c_16182]) ).
cnf(c_16184,plain,
( multiply(sk_c8,sk_c7) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c8
| sk_c8 != sk_c8
| inverse(sk_c8) != sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_16183]) ).
cnf(c_16185,plain,
( multiply(sk_c8,sk_c7) != sk_c8
| sk_c8 != sk_c8
| inverse(sk_c8) != sk_c8
| sk_c8 != sk_c8
| inverse(sk_c8) != sk_c8 ),
inference(paramod,[status(thm)],[c_15852,c_16184]) ).
cnf(c_16186,plain,
( multiply(sk_c8,sk_c8) != sk_c8
| sk_c8 != sk_c8
| inverse(sk_c8) != sk_c8
| sk_c8 != sk_c8
| inverse(sk_c8) != sk_c8 ),
inference(paramod,[status(thm)],[c_15411,c_16185]) ).
cnf(c_16187,plain,
( sk_c8 != sk_c8
| sk_c8 != sk_c8
| inverse(sk_c8) != sk_c8
| sk_c8 != sk_c8
| inverse(sk_c8) != sk_c8 ),
inference(paramod,[status(thm)],[c_15852,c_16186]) ).
cnf(c_16188,plain,
( sk_c8 != sk_c8
| sk_c8 != sk_c8
| inverse(sk_c8) != sk_c8
| inverse(sk_c8) != sk_c8 ),
inference(copy,[status(thm)],[c_16187]) ).
cnf(c_16189,plain,
( sk_c8 != sk_c8
| inverse(sk_c8) != sk_c8
| inverse(sk_c8) != sk_c8 ),
inference(copy,[status(thm)],[c_16188]) ).
cnf(c_16190,plain,
( inverse(sk_c8) != sk_c8
| inverse(sk_c8) != sk_c8 ),
inference(copy,[status(thm)],[c_16189]) ).
cnf(c_16043,plain,
inverse(sk_c8) != sk_c8,
inference(copy,[status(thm)],[c_16190]) ).
cnf(c_16191,plain,
( multiply(sk_c8,sk_c8) != sk_c8
| inverse(sk_c4) != sk_c8
| multiply(sk_c4,sk_c8) != sk_c8
| sk_c4 != sk_c8
| inverse(sk_c8) = sk_c8 ),
inference(factor,[status(thm)],[c_15834]) ).
cnf(c_16192,plain,
( multiply(sk_c8,sk_c8) != sk_c8
| inverse(sk_c4) != sk_c8
| sk_c8 != sk_c8
| sk_c4 != sk_c8
| inverse(sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15972,c_16191]) ).
cnf(c_16193,plain,
( multiply(sk_c8,sk_c8) != sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c8
| sk_c4 != sk_c8
| inverse(sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15993,c_16192]) ).
cnf(c_16194,plain,
( sk_c8 != sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c8
| sk_c4 != sk_c8
| inverse(sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15852,c_16193]) ).
cnf(c_16195,plain,
( sk_c8 != sk_c8
| sk_c8 != sk_c8
| sk_c4 != sk_c8
| inverse(sk_c8) = sk_c8 ),
inference(copy,[status(thm)],[c_16194]) ).
cnf(c_16196,plain,
( sk_c8 != sk_c8
| sk_c4 != sk_c8
| inverse(sk_c8) = sk_c8 ),
inference(copy,[status(thm)],[c_16195]) ).
cnf(c_16197,plain,
( sk_c4 != sk_c8
| inverse(sk_c8) = sk_c8 ),
inference(copy,[status(thm)],[c_16196]) ).
cnf(c_16044,plain,
sk_c4 != sk_c8,
inference(resolve,[status(thm)],[c_16043,c_16197]) ).
cnf(c_16198,plain,
( multiply(sk_c8,multiply(sk_c8,sk_c8)) = sk_c6
| sk_c8 = sk_c6 ),
inference(paramod,[status(thm)],[c_15972,c_15678]) ).
cnf(c_16199,plain,
( multiply(sk_c8,sk_c8) = sk_c6
| sk_c8 = sk_c6 ),
inference(paramod,[status(thm)],[c_15852,c_16198]) ).
cnf(c_16200,plain,
( sk_c8 = sk_c6
| sk_c8 = sk_c6 ),
inference(paramod,[status(thm)],[c_15852,c_16199]) ).
cnf(c_16201,plain,
( sk_c8 = sk_c6
| sk_c6 = sk_c8 ),
inference(copy,[status(thm)],[c_16200]) ).
cnf(c_16202,plain,
( sk_c6 = sk_c8
| sk_c6 = sk_c8 ),
inference(copy,[status(thm)],[c_16201]) ).
cnf(c_16049,plain,
sk_c6 = sk_c8,
inference(copy,[status(thm)],[c_16202]) ).
cnf(c_16203,plain,
( multiply(A,multiply(sk_c4,sk_c8)) = A
| sk_c4 = sk_c8
| inverse(sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_16049,c_15577]) ).
cnf(c_16204,plain,
( multiply(A,sk_c8) = A
| sk_c4 = sk_c8
| inverse(sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_15972,c_16203]) ).
cnf(c_16205,plain,
( multiply(A,sk_c8) = A
| sk_c4 = sk_c8 ),
inference(resolve,[status(thm)],[c_16043,c_16204]) ).
cnf(c_16055,plain,
multiply(A,sk_c8) = A,
inference(resolve,[status(thm)],[c_16044,c_16205]) ).
cnf(c_16206,plain,
( sk_c6 != sk_c8
| multiply(A,sk_c4) = A ),
inference(paramod,[status(thm)],[c_16055,c_15576]) ).
cnf(c_16207,plain,
( sk_c8 != sk_c8
| multiply(A,sk_c4) = A ),
inference(paramod,[status(thm)],[c_16049,c_16206]) ).
cnf(c_16056,plain,
multiply(A,sk_c4) = A,
inference(copy,[status(thm)],[c_16207]) ).
cnf(c_16208,plain,
( multiply(sk_c4,multiply(sk_c8,sk_c4)) = sk_c6
| inverse(sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_16055,c_15562]) ).
cnf(c_16209,plain,
( multiply(sk_c4,sk_c8) = sk_c6
| inverse(sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_16056,c_16208]) ).
cnf(c_16210,plain,
( sk_c4 = sk_c6
| inverse(sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_16055,c_16209]) ).
cnf(c_16211,plain,
( sk_c4 = sk_c8
| inverse(sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_16049,c_16210]) ).
cnf(c_16212,plain,
sk_c4 = sk_c8,
inference(resolve,[status(thm)],[c_16043,c_16211]) ).
cnf(c_16057,plain,
$false,
inference(resolve,[status(thm)],[c_16044,c_16212]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP233-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n016.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Fri Sep 25 14:44:44 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.43 % Process 2637090 was started by sandbox2 on n016,
% 0.17/0.43 % Fri Sep 25 14:44:44 2026
% 0.17/0.43 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/0.44
% 0.17/0.44 % From the command line: assign(max_seconds, 300).
% 46.39/6.39
% 46.39/6.39 % given #500 (T,wt=11): 11243 sk_c1 = sk_c7 | inverse(sk_c4) = sk_c6. [para(11197(b,1),7989(b,1,1)),merge(b)].
% 46.39/6.39
% 46.39/6.39 % SZS status Unsatisfiable for theBenchmark
% 46.39/6.39
% 46.39/6.39 % Proof 1 at 4.65 (+ 1.22) seconds.
% 46.39/6.39 % Length of proof is 167.
% 46.39/6.39 % Level of proof is 36.
% 46.39/6.39 % Maximum clause weight is 54.000.
% 46.39/6.39 % Given clauses 556.
% 46.39/6.39
% 46.39/6.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------