%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP368-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 : n018.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:43 AM UTC 2026
% Result : Unsatisfiable 244.05s 38.33s
% Output : CNFRefutation 244.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 130
% Number of leaves : 30
% Syntax : Number of formulae : 346 ( 36 unt; 0 def)
% Number of atoms : 1018 (1017 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 1100 ( 428 ~; 672 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 89 ( 0 sgn 9 !; 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_c6,sk_c7) = sk_c5
| multiply(sk_c5,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_1) ).
cnf(c_4,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c5,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_1]) ).
fof(prove_this_3,axiom,
( multiply(sk_c7,sk_c5) = sk_c6
| multiply(sk_c5,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_3) ).
cnf(c_6,plain,
( multiply(sk_c7,sk_c5) = sk_c6
| multiply(sk_c5,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_3]) ).
fof(prove_this_7,axiom,
( inverse(sk_c6) = sk_c5
| multiply(sk_c7,sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_7) ).
cnf(c_10,plain,
( inverse(sk_c6) = sk_c5
| multiply(sk_c7,sk_c2) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_7]) ).
fof(prove_this_8,axiom,
( multiply(sk_c7,sk_c5) = sk_c6
| multiply(sk_c7,sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_11,plain,
( multiply(sk_c7,sk_c5) = sk_c6
| multiply(sk_c7,sk_c2) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_8]) ).
fof(prove_this_9,axiom,
( inverse(sk_c4) = sk_c7
| multiply(sk_c7,sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_9) ).
cnf(c_12,plain,
( inverse(sk_c4) = sk_c7
| multiply(sk_c7,sk_c2) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_9]) ).
fof(prove_this_10,axiom,
( multiply(sk_c4,sk_c6) = sk_c7
| multiply(sk_c7,sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_10) ).
cnf(c_13,plain,
( multiply(sk_c4,sk_c6) = sk_c7
| multiply(sk_c7,sk_c2) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_10]) ).
fof(prove_this_11,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c2 ),
file('theBenchmark.p',prove_this_11) ).
cnf(c_14,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c2 ),
inference(clausify,[status(thm)],[prove_this_11]) ).
fof(prove_this_12,axiom,
( inverse(sk_c6) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c2 ),
file('theBenchmark.p',prove_this_12) ).
cnf(c_15,plain,
( inverse(sk_c6) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c2 ),
inference(clausify,[status(thm)],[prove_this_12]) ).
fof(prove_this_13,axiom,
( multiply(sk_c7,sk_c5) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c2 ),
file('theBenchmark.p',prove_this_13) ).
cnf(c_16,plain,
( multiply(sk_c7,sk_c5) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c2 ),
inference(clausify,[status(thm)],[prove_this_13]) ).
fof(prove_this_14,axiom,
( inverse(sk_c4) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c2 ),
file('theBenchmark.p',prove_this_14) ).
cnf(c_17,plain,
( inverse(sk_c4) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c2 ),
inference(clausify,[status(thm)],[prove_this_14]) ).
fof(prove_this_15,axiom,
( multiply(sk_c4,sk_c6) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c2 ),
file('theBenchmark.p',prove_this_15) ).
cnf(c_18,plain,
( multiply(sk_c4,sk_c6) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c2 ),
inference(clausify,[status(thm)],[prove_this_15]) ).
fof(prove_this_16,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_16) ).
cnf(c_19,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_16]) ).
fof(prove_this_17,axiom,
( inverse(sk_c6) = sk_c5
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_17) ).
cnf(c_20,plain,
( inverse(sk_c6) = sk_c5
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_17]) ).
fof(prove_this_18,axiom,
( multiply(sk_c7,sk_c5) = sk_c6
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_18) ).
cnf(c_21,plain,
( multiply(sk_c7,sk_c5) = sk_c6
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_18]) ).
fof(prove_this_19,axiom,
( inverse(sk_c4) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_19) ).
cnf(c_22,plain,
( inverse(sk_c4) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_19]) ).
fof(prove_this_20,axiom,
( multiply(sk_c4,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_20) ).
cnf(c_23,plain,
( multiply(sk_c4,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_20]) ).
fof(prove_this_21,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c3,sk_c5) = sk_c7 ),
file('theBenchmark.p',prove_this_21) ).
cnf(c_24,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c3,sk_c5) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_21]) ).
fof(prove_this_22,axiom,
( inverse(sk_c6) = sk_c5
| multiply(sk_c3,sk_c5) = sk_c7 ),
file('theBenchmark.p',prove_this_22) ).
cnf(c_25,plain,
( inverse(sk_c6) = sk_c5
| multiply(sk_c3,sk_c5) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_22]) ).
fof(prove_this_23,axiom,
( multiply(sk_c7,sk_c5) = sk_c6
| multiply(sk_c3,sk_c5) = sk_c7 ),
file('theBenchmark.p',prove_this_23) ).
cnf(c_26,plain,
( multiply(sk_c7,sk_c5) = sk_c6
| multiply(sk_c3,sk_c5) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_23]) ).
fof(prove_this_24,axiom,
( inverse(sk_c4) = sk_c7
| multiply(sk_c3,sk_c5) = sk_c7 ),
file('theBenchmark.p',prove_this_24) ).
cnf(c_27,plain,
( inverse(sk_c4) = sk_c7
| multiply(sk_c3,sk_c5) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_24]) ).
fof(prove_this_25,axiom,
( multiply(sk_c4,sk_c6) = sk_c7
| multiply(sk_c3,sk_c5) = sk_c7 ),
file('theBenchmark.p',prove_this_25) ).
cnf(c_28,plain,
( multiply(sk_c4,sk_c6) = sk_c7
| multiply(sk_c3,sk_c5) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_25]) ).
fof(prove_this_26,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c3) = sk_c5 ),
file('theBenchmark.p',prove_this_26) ).
cnf(c_29,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c3) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_26]) ).
fof(prove_this_27,axiom,
( inverse(sk_c6) = sk_c5
| inverse(sk_c3) = sk_c5 ),
file('theBenchmark.p',prove_this_27) ).
cnf(c_30,plain,
( inverse(sk_c6) = sk_c5
| inverse(sk_c3) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_27]) ).
fof(prove_this_28,axiom,
( multiply(sk_c7,sk_c5) = sk_c6
| inverse(sk_c3) = sk_c5 ),
file('theBenchmark.p',prove_this_28) ).
cnf(c_31,plain,
( multiply(sk_c7,sk_c5) = sk_c6
| inverse(sk_c3) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_28]) ).
fof(prove_this_29,axiom,
( inverse(sk_c4) = sk_c7
| inverse(sk_c3) = sk_c5 ),
file('theBenchmark.p',prove_this_29) ).
cnf(c_32,plain,
( inverse(sk_c4) = sk_c7
| inverse(sk_c3) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_29]) ).
fof(prove_this_30,axiom,
( multiply(sk_c4,sk_c6) = sk_c7
| inverse(sk_c3) = sk_c5 ),
file('theBenchmark.p',prove_this_30) ).
cnf(c_33,plain,
( multiply(sk_c4,sk_c6) = sk_c7
| inverse(sk_c3) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_30]) ).
fof(prove_this_31,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( multiply(VAR_3,sk_c6) != sk_c7
| inverse(VAR_3) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(VAR_2) != sk_c5
| multiply(VAR_2,sk_c5) != sk_c7
| inverse(VAR_1) != sk_c7
| multiply(VAR_1,sk_c7) != VAR_0
| multiply(sk_c7,VAR_0) != sk_c6
| multiply(sk_c5,sk_c7) != sk_c6 ),
file('theBenchmark.p',prove_this_31) ).
cnf(c_34,plain,
( multiply(D,sk_c6) != sk_c7
| inverse(D) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(C) != sk_c5
| multiply(C,sk_c5) != sk_c7
| inverse(B) != sk_c7
| multiply(B,sk_c7) != A
| multiply(sk_c7,A) != sk_c6
| multiply(sk_c5,sk_c7) != sk_c6 ),
inference(clausify,[status(thm)],[prove_this_31]) ).
cnf(c_35,plain,
( multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(A) != sk_c5
| multiply(A,sk_c5) != sk_c7
| inverse(sk_c5) != sk_c7
| multiply(sk_c7,sk_c6) != sk_c6
| multiply(sk_c5,sk_c7) != sk_c6 ),
inference(factor,[status(thm)],[c_34]) ).
cnf(c_21308,plain,
( multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| inverse(A) != sk_c5
| multiply(A,sk_c5) != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| multiply(sk_c5,sk_c7) != sk_c6 ),
inference(factor,[status(thm)],[c_34]) ).
cnf(c_37,plain,
( multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| inverse(sk_c6) != sk_c5
| inverse(A) != sk_c5
| multiply(A,sk_c5) != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| multiply(sk_c5,sk_c7) != sk_c6 ),
inference(copy,[status(thm)],[c_21308]) ).
cnf(c_40,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(A) != sk_c5
| multiply(A,sk_c5) != sk_c7
| inverse(sk_c5) != sk_c7
| multiply(sk_c7,sk_c6) != sk_c6
| multiply(sk_c5,sk_c7) != sk_c6 ),
inference(factor,[status(thm)],[c_35]) ).
cnf(c_21309,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_21310,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_21309]) ).
cnf(c_50,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_21310]) ).
cnf(c_21311,plain,
( multiply(sk_c6,A) = multiply(sk_c5,multiply(sk_c7,A))
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_4,c_3]) ).
cnf(c_51,plain,
( multiply(sk_c5,multiply(sk_c7,A)) = multiply(sk_c6,A)
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_21311]) ).
cnf(c_21312,plain,
( multiply(sk_c6,A) = multiply(sk_c5,multiply(sk_c7,A))
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_6,c_3]) ).
cnf(c_54,plain,
( multiply(sk_c5,multiply(sk_c7,A)) = multiply(sk_c6,A)
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(copy,[status(thm)],[c_21312]) ).
cnf(c_64,plain,
( multiply(sk_c7,sk_c4) = identity
| multiply(sk_c7,sk_c2) = sk_c6 ),
inference(paramod,[status(thm)],[c_12,c_2]) ).
cnf(c_21313,plain,
( multiply(sk_c7,A) = multiply(sk_c4,multiply(sk_c6,A))
| multiply(sk_c7,sk_c2) = sk_c6 ),
inference(paramod,[status(thm)],[c_13,c_3]) ).
cnf(c_65,plain,
( multiply(sk_c4,multiply(sk_c6,A)) = multiply(sk_c7,A)
| multiply(sk_c7,sk_c2) = sk_c6 ),
inference(copy,[status(thm)],[c_21313]) ).
cnf(c_69,plain,
( multiply(sk_c5,sk_c6) = identity
| multiply(sk_c1,sk_c7) = sk_c2 ),
inference(paramod,[status(thm)],[c_15,c_2]) ).
cnf(c_21314,plain,
( multiply(multiply(A,sk_c1),sk_c7) = multiply(A,sk_c2)
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_16,c_3]) ).
cnf(c_71,plain,
( multiply(A,multiply(sk_c1,sk_c7)) = multiply(A,sk_c2)
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_3,c_21314]) ).
cnf(c_72,plain,
( multiply(sk_c7,sk_c4) = identity
| multiply(sk_c1,sk_c7) = sk_c2 ),
inference(paramod,[status(thm)],[c_17,c_2]) ).
cnf(c_21315,plain,
( multiply(multiply(A,sk_c3),sk_c5) = multiply(A,sk_c7)
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_24,c_3]) ).
cnf(c_81,plain,
( multiply(A,multiply(sk_c3,sk_c5)) = multiply(A,sk_c7)
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_3,c_21315]) ).
cnf(c_85,plain,
( multiply(sk_c7,sk_c4) = identity
| multiply(sk_c3,sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_27,c_2]) ).
cnf(c_404,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_50]) ).
cnf(c_436,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_50,c_50]) ).
cnf(c_437,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_436,c_404]) ).
cnf(c_449,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_437,c_2]) ).
cnf(c_630,plain,
multiply(A,inverse(A)) = identity,
inference(paramod,[status(thm)],[c_436,c_2]) ).
cnf(c_645,plain,
( multiply(inverse(sk_c5),A) = multiply(sk_c3,A)
| inverse(sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_30,c_436]) ).
cnf(c_21316,plain,
multiply(A,identity) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_436,c_437]) ).
cnf(c_21317,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_437,c_21316]) ).
cnf(c_654,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_21317]) ).
cnf(c_21318,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(inverse(sk_c5),sk_c5) != sk_c7
| inverse(sk_c5) != sk_c7
| multiply(sk_c7,sk_c6) != sk_c6
| multiply(sk_c5,sk_c7) != sk_c6 ),
inference(resolve,[status(thm)],[c_654,c_40]) ).
cnf(c_676,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c7
| inverse(sk_c5) != sk_c7
| multiply(sk_c7,sk_c6) != sk_c6
| multiply(sk_c5,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_2,c_21318]) ).
cnf(c_21319,plain,
( multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7
| inverse(sk_c6) != sk_c5
| multiply(inverse(sk_c5),sk_c5) != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| multiply(sk_c5,sk_c7) != sk_c6 ),
inference(resolve,[status(thm)],[c_654,c_37]) ).
cnf(c_680,plain,
( multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7
| inverse(sk_c6) != sk_c5
| identity != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| multiply(sk_c5,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_2,c_21319]) ).
cnf(c_694,plain,
( inverse(sk_c7) = sk_c1
| inverse(sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_20,c_654]) ).
cnf(c_21320,plain,
identity = multiply(A,multiply(B,inverse(multiply(A,B)))),
inference(paramod,[status(thm)],[c_630,c_3]) ).
cnf(c_758,plain,
multiply(A,multiply(B,inverse(multiply(A,B)))) = identity,
inference(copy,[status(thm)],[c_21320]) ).
cnf(c_761,plain,
( multiply(sk_c6,sk_c5) = identity
| multiply(sk_c7,sk_c2) = sk_c6 ),
inference(paramod,[status(thm)],[c_10,c_630]) ).
cnf(c_765,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_19,c_630]) ).
cnf(c_766,plain,
( multiply(sk_c1,sk_c7) = identity
| inverse(sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_20,c_630]) ).
cnf(c_767,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_21,c_630]) ).
cnf(c_768,plain,
( multiply(sk_c1,sk_c7) = identity
| inverse(sk_c4) = sk_c7 ),
inference(paramod,[status(thm)],[c_22,c_630]) ).
cnf(c_769,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c4,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_23,c_630]) ).
cnf(c_772,plain,
( multiply(sk_c3,sk_c5) = identity
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_29,c_630]) ).
cnf(c_774,plain,
( multiply(sk_c3,sk_c5) = identity
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_31,c_630]) ).
cnf(c_775,plain,
( multiply(sk_c3,sk_c5) = identity
| inverse(sk_c4) = sk_c7 ),
inference(paramod,[status(thm)],[c_32,c_630]) ).
cnf(c_776,plain,
( multiply(sk_c3,sk_c5) = identity
| multiply(sk_c4,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_33,c_630]) ).
cnf(c_855,plain,
( inverse(sk_c5) = sk_c6
| inverse(sk_c7) = sk_c1 ),
inference(paramod,[status(thm)],[c_694,c_654]) ).
cnf(c_899,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| inverse(sk_c6) != sk_c5
| identity != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| multiply(sk_c5,sk_c7) != sk_c6 ),
inference(resolve,[status(thm)],[c_680,c_654]) ).
cnf(c_1024,plain,
( multiply(sk_c5,multiply(sk_c7,inverse(sk_c6))) = identity
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_630,c_54]) ).
cnf(c_1808,plain,
( multiply(sk_c5,sk_c6) = identity
| multiply(sk_c1,sk_c7) = identity ),
inference(paramod,[status(thm)],[c_766,c_2]) ).
cnf(c_1857,plain,
( multiply(sk_c7,sk_c4) = identity
| multiply(sk_c1,sk_c7) = identity ),
inference(paramod,[status(thm)],[c_768,c_2]) ).
cnf(c_2083,plain,
( multiply(sk_c7,sk_c4) = identity
| multiply(sk_c3,sk_c5) = identity ),
inference(paramod,[status(thm)],[c_775,c_2]) ).
cnf(c_21321,plain,
multiply(inverse(A),identity) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_758,c_50]) ).
cnf(c_21322,plain,
inverse(A) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_437,c_21321]) ).
cnf(c_3944,plain,
multiply(A,inverse(multiply(B,A))) = inverse(B),
inference(copy,[status(thm)],[c_21322]) ).
cnf(c_21323,plain,
multiply(inverse(A),inverse(B)) = inverse(multiply(B,A)),
inference(paramod,[status(thm)],[c_3944,c_50]) ).
cnf(c_3989,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_21323]) ).
cnf(c_21324,plain,
( multiply(sk_c4,identity) = multiply(sk_c7,sk_c5)
| multiply(sk_c7,sk_c2) = sk_c6
| multiply(sk_c7,sk_c2) = sk_c6 ),
inference(paramod,[status(thm)],[c_761,c_65]) ).
cnf(c_21325,plain,
( sk_c4 = multiply(sk_c7,sk_c5)
| multiply(sk_c7,sk_c2) = sk_c6
| multiply(sk_c7,sk_c2) = sk_c6 ),
inference(paramod,[status(thm)],[c_437,c_21324]) ).
cnf(c_21326,plain,
( multiply(sk_c7,sk_c5) = sk_c4
| multiply(sk_c7,sk_c2) = sk_c6
| multiply(sk_c7,sk_c2) = sk_c6 ),
inference(copy,[status(thm)],[c_21325]) ).
cnf(c_4253,plain,
( multiply(sk_c7,sk_c5) = sk_c4
| multiply(sk_c7,sk_c2) = sk_c6 ),
inference(copy,[status(thm)],[c_21326]) ).
cnf(c_21327,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| identity = sk_c2
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_765,c_14]) ).
cnf(c_4401,plain,
( identity = sk_c2
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_21327]) ).
cnf(c_4405,plain,
( multiply(inverse(sk_c6),sk_c5) = sk_c7
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_4401,c_50]) ).
cnf(c_21328,plain,
( multiply(sk_c7,sk_c5) = sk_c6
| identity = sk_c2
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_767,c_16]) ).
cnf(c_4582,plain,
( identity = sk_c2
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(copy,[status(thm)],[c_21328]) ).
cnf(c_21329,plain,
( multiply(A,identity) = multiply(A,sk_c2)
| multiply(sk_c7,sk_c5) = sk_c6
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_767,c_71]) ).
cnf(c_21330,plain,
( A = multiply(A,sk_c2)
| multiply(sk_c7,sk_c5) = sk_c6
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_437,c_21329]) ).
cnf(c_21331,plain,
( multiply(A,sk_c2) = A
| multiply(sk_c7,sk_c5) = sk_c6
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(copy,[status(thm)],[c_21330]) ).
cnf(c_4583,plain,
( multiply(A,sk_c2) = A
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(copy,[status(thm)],[c_21331]) ).
cnf(c_4586,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c5
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_4582,c_50]) ).
cnf(c_21332,plain,
( multiply(sk_c4,sk_c6) = sk_c7
| identity = sk_c2
| multiply(sk_c4,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_769,c_18]) ).
cnf(c_4620,plain,
( identity = sk_c2
| multiply(sk_c4,sk_c6) = sk_c7 ),
inference(copy,[status(thm)],[c_21332]) ).
cnf(c_4803,plain,
( multiply(inverse(sk_c4),sk_c7) = sk_c6
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_4620,c_50]) ).
cnf(c_21333,plain,
( multiply(sk_c7,sk_c5) = sk_c6
| identity = sk_c7
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_774,c_26]) ).
cnf(c_4944,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(copy,[status(thm)],[c_21333]) ).
cnf(c_21334,plain,
( multiply(A,identity) = multiply(A,sk_c7)
| multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_772,c_81]) ).
cnf(c_21335,plain,
( A = multiply(A,sk_c7)
| multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_437,c_21334]) ).
cnf(c_21336,plain,
( multiply(A,sk_c7) = A
| multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_21335]) ).
cnf(c_4959,plain,
( multiply(A,sk_c7) = A
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_21336]) ).
cnf(c_5172,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c5
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_4944,c_50]) ).
cnf(c_21337,plain,
( multiply(sk_c4,sk_c6) = sk_c7
| identity = sk_c7
| multiply(sk_c4,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_776,c_28]) ).
cnf(c_5204,plain,
( identity = sk_c7
| multiply(sk_c4,sk_c6) = sk_c7 ),
inference(copy,[status(thm)],[c_21337]) ).
cnf(c_5207,plain,
( multiply(inverse(sk_c4),sk_c7) = sk_c6
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_5204,c_50]) ).
cnf(c_21338,plain,
( multiply(sk_c5,sk_c6) = identity
| identity = sk_c2
| multiply(sk_c5,sk_c6) = identity ),
inference(paramod,[status(thm)],[c_1808,c_69]) ).
cnf(c_5941,plain,
( identity = sk_c2
| multiply(sk_c5,sk_c6) = identity ),
inference(copy,[status(thm)],[c_21338]) ).
cnf(c_21339,plain,
( multiply(inverse(sk_c5),identity) = sk_c6
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_5941,c_50]) ).
cnf(c_6127,plain,
( inverse(sk_c5) = sk_c6
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_437,c_21339]) ).
cnf(c_21340,plain,
( multiply(sk_c7,sk_c4) = identity
| identity = sk_c2
| multiply(sk_c7,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_1857,c_72]) ).
cnf(c_6420,plain,
( identity = sk_c2
| multiply(sk_c7,sk_c4) = identity ),
inference(copy,[status(thm)],[c_21340]) ).
cnf(c_21341,plain,
( multiply(inverse(sk_c7),identity) = sk_c4
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_6420,c_50]) ).
cnf(c_6765,plain,
( inverse(sk_c7) = sk_c4
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_437,c_21341]) ).
cnf(c_6775,plain,
( multiply(sk_c4,sk_c7) = identity
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_6765,c_2]) ).
cnf(c_6800,plain,
( multiply(sk_c4,multiply(sk_c7,A)) = A
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_6765,c_50]) ).
cnf(c_6801,plain,
( inverse(sk_c4) = sk_c7
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_6765,c_654]) ).
cnf(c_21342,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| identity = sk_c2
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_6801,c_4803]) ).
cnf(c_6921,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| identity = sk_c2 ),
inference(copy,[status(thm)],[c_21342]) ).
cnf(c_21343,plain,
( multiply(multiply(A,sk_c4),sk_c7) = multiply(A,identity)
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_6775,c_3]) ).
cnf(c_21344,plain,
( multiply(A,multiply(sk_c4,sk_c7)) = multiply(A,identity)
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_3,c_21343]) ).
cnf(c_6930,plain,
( multiply(A,multiply(sk_c4,sk_c7)) = A
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_437,c_21344]) ).
cnf(c_8017,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c7
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_6921,c_50]) ).
cnf(c_21345,plain,
( multiply(sk_c7,sk_c4) = identity
| identity = sk_c7
| multiply(sk_c7,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_2083,c_85]) ).
cnf(c_8898,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c4) = identity ),
inference(copy,[status(thm)],[c_21345]) ).
cnf(c_21346,plain,
( multiply(inverse(sk_c7),identity) = sk_c4
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_8898,c_50]) ).
cnf(c_8903,plain,
( inverse(sk_c7) = sk_c4
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_437,c_21346]) ).
cnf(c_8927,plain,
( inverse(sk_c4) = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_8903,c_654]) ).
cnf(c_21347,plain,
( multiply(sk_c4,sk_c6) = sk_c5
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_8903,c_5172]) ).
cnf(c_8963,plain,
( multiply(sk_c4,sk_c6) = sk_c5
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_21347]) ).
cnf(c_21348,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_8927,c_5207]) ).
cnf(c_9017,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_21348]) ).
cnf(c_21349,plain,
( identity = sk_c7
| sk_c5 = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_8963,c_5204]) ).
cnf(c_9191,plain,
( sk_c5 = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_21349]) ).
cnf(c_9193,plain,
( multiply(A,sk_c7) = A
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_9191,c_437]) ).
cnf(c_9194,plain,
( inverse(sk_c7) = identity
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_9191,c_449]) ).
cnf(c_21350,plain,
( inverse(sk_c7) = sk_c7
| sk_c5 = sk_c7
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_9191,c_9194]) ).
cnf(c_9406,plain,
( inverse(sk_c7) = sk_c7
| sk_c5 = sk_c7 ),
inference(copy,[status(thm)],[c_21350]) ).
cnf(c_9544,plain,
( multiply(sk_c7,sk_c7) = identity
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_9406,c_2]) ).
cnf(c_9677,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_9017,c_50]) ).
cnf(c_21351,plain,
( multiply(sk_c5,identity) = multiply(sk_c6,sk_c7)
| multiply(sk_c6,sk_c7) = sk_c5
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_9544,c_51]) ).
cnf(c_21352,plain,
( sk_c5 = multiply(sk_c6,sk_c7)
| multiply(sk_c6,sk_c7) = sk_c5
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_437,c_21351]) ).
cnf(c_21353,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c6,sk_c7) = sk_c5
| sk_c5 = sk_c7 ),
inference(copy,[status(thm)],[c_21352]) ).
cnf(c_9886,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| sk_c5 = sk_c7 ),
inference(copy,[status(thm)],[c_21353]) ).
cnf(c_21354,plain,
( sk_c5 = sk_c6
| sk_c5 = sk_c7
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_9886,c_9193]) ).
cnf(c_9907,plain,
( sk_c5 = sk_c6
| sk_c5 = sk_c7 ),
inference(copy,[status(thm)],[c_21354]) ).
cnf(c_21355,plain,
( inverse(sk_c7) = multiply(inverse(sk_c5),inverse(inverse(sk_c6)))
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_4405,c_3989]) ).
cnf(c_21356,plain,
( inverse(sk_c7) = multiply(inverse(sk_c5),sk_c6)
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_654,c_21355]) ).
cnf(c_10624,plain,
( multiply(inverse(sk_c5),sk_c6) = inverse(sk_c7)
| identity = sk_c2 ),
inference(copy,[status(thm)],[c_21356]) ).
cnf(c_21357,plain,
( inverse(sk_c5) = multiply(inverse(sk_c6),inverse(inverse(sk_c7)))
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_4586,c_3989]) ).
cnf(c_10633,plain,
( inverse(sk_c5) = multiply(inverse(sk_c6),sk_c7)
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_654,c_21357]) ).
cnf(c_21358,plain,
( multiply(sk_c7,sk_c5) = sk_c6
| sk_c7 = sk_c6
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_4583,c_11]) ).
cnf(c_21359,plain,
( multiply(sk_c7,sk_c5) = sk_c6
| sk_c6 = sk_c7
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(copy,[status(thm)],[c_21358]) ).
cnf(c_10971,plain,
( sk_c6 = sk_c7
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(copy,[status(thm)],[c_21359]) ).
cnf(c_11015,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c5
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_10971,c_50]) ).
cnf(c_21360,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| sk_c1 = sk_c2
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_4959,c_14]) ).
cnf(c_21361,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| sk_c2 = sk_c1
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_21360]) ).
cnf(c_11254,plain,
( sk_c2 = sk_c1
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_21361]) ).
cnf(c_11387,plain,
( multiply(inverse(sk_c6),sk_c5) = sk_c7
| sk_c2 = sk_c1 ),
inference(paramod,[status(thm)],[c_11254,c_50]) ).
cnf(c_21362,plain,
( inverse(sk_c7) = multiply(inverse(sk_c5),inverse(inverse(sk_c6)))
| sk_c2 = sk_c1 ),
inference(paramod,[status(thm)],[c_11387,c_3989]) ).
cnf(c_21363,plain,
( inverse(sk_c7) = multiply(inverse(sk_c5),sk_c6)
| sk_c2 = sk_c1 ),
inference(paramod,[status(thm)],[c_654,c_21362]) ).
cnf(c_11513,plain,
( multiply(inverse(sk_c5),sk_c6) = inverse(sk_c7)
| sk_c2 = sk_c1 ),
inference(copy,[status(thm)],[c_21363]) ).
cnf(c_21364,plain,
( multiply(sk_c6,sk_c6) = inverse(sk_c7)
| identity = sk_c2
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_6127,c_10624]) ).
cnf(c_21365,plain,
( inverse(sk_c7) = multiply(sk_c6,sk_c6)
| identity = sk_c2
| identity = sk_c2 ),
inference(copy,[status(thm)],[c_21364]) ).
cnf(c_14269,plain,
( inverse(sk_c7) = multiply(sk_c6,sk_c6)
| identity = sk_c2 ),
inference(copy,[status(thm)],[c_21365]) ).
cnf(c_21366,plain,
( multiply(inverse(sk_c6),sk_c7) = sk_c6
| identity = sk_c2
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_10633,c_6127]) ).
cnf(c_14487,plain,
( multiply(inverse(sk_c6),sk_c7) = sk_c6
| identity = sk_c2 ),
inference(copy,[status(thm)],[c_21366]) ).
cnf(c_21367,plain,
( multiply(inverse(inverse(sk_c6)),sk_c6) = sk_c7
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_14487,c_50]) ).
cnf(c_14500,plain,
( multiply(sk_c6,sk_c6) = sk_c7
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_654,c_21367]) ).
cnf(c_21368,plain,
( inverse(sk_c7) = sk_c7
| identity = sk_c2
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_14500,c_14269]) ).
cnf(c_14603,plain,
( inverse(sk_c7) = sk_c7
| identity = sk_c2 ),
inference(copy,[status(thm)],[c_21368]) ).
cnf(c_21369,plain,
( multiply(sk_c7,sk_c6) = sk_c7
| identity = sk_c2
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_14603,c_8017]) ).
cnf(c_14662,plain,
( multiply(sk_c7,sk_c6) = sk_c7
| identity = sk_c2 ),
inference(copy,[status(thm)],[c_21369]) ).
cnf(c_21370,plain,
( multiply(sk_c4,sk_c7) = sk_c6
| identity = sk_c2
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_14662,c_6800]) ).
cnf(c_15247,plain,
( multiply(sk_c4,sk_c7) = sk_c6
| identity = sk_c2 ),
inference(copy,[status(thm)],[c_21370]) ).
cnf(c_21371,plain,
( multiply(A,sk_c6) = A
| identity = sk_c2
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_15247,c_6930]) ).
cnf(c_15380,plain,
( multiply(A,sk_c6) = A
| identity = sk_c2 ),
inference(copy,[status(thm)],[c_21371]) ).
cnf(c_21372,plain,
( sk_c6 = sk_c7
| identity = sk_c2
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_15380,c_14500]) ).
cnf(c_15418,plain,
( sk_c6 = sk_c7
| identity = sk_c2 ),
inference(copy,[status(thm)],[c_21372]) ).
cnf(c_15532,plain,
( multiply(A,sk_c2) = A
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_15418,c_437]) ).
cnf(c_21373,plain,
( multiply(sk_c7,sk_c4) = identity
| sk_c7 = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_15532,c_64]) ).
cnf(c_21374,plain,
( multiply(sk_c7,sk_c4) = identity
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_21373]) ).
cnf(c_16950,plain,
( multiply(sk_c7,sk_c4) = identity
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_21374]) ).
cnf(c_21375,plain,
( multiply(sk_c7,sk_c5) = sk_c4
| sk_c7 = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_15532,c_4253]) ).
cnf(c_21376,plain,
( multiply(sk_c7,sk_c5) = sk_c4
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_21375]) ).
cnf(c_16954,plain,
( multiply(sk_c7,sk_c5) = sk_c4
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_21376]) ).
cnf(c_21377,plain,
( multiply(inverse(sk_c7),identity) = sk_c4
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_16950,c_50]) ).
cnf(c_17544,plain,
( inverse(sk_c7) = sk_c4
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_437,c_21377]) ).
cnf(c_21378,plain,
( sk_c6 = sk_c7
| sk_c4 = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_16954,c_10971]) ).
cnf(c_17676,plain,
( sk_c4 = sk_c6
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_21378]) ).
cnf(c_21379,plain,
( inverse(sk_c7) = sk_c6
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_17676,c_17544]) ).
cnf(c_17741,plain,
( inverse(sk_c7) = sk_c6
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_21379]) ).
cnf(c_17763,plain,
( multiply(sk_c6,sk_c7) = identity
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_17741,c_2]) ).
cnf(c_21380,plain,
( sk_c6 = sk_c7
| sk_c5 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_17741,c_9406]) ).
cnf(c_17786,plain,
( sk_c5 = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_21380]) ).
cnf(c_21381,plain,
( sk_c6 = sk_c7
| multiply(sk_c7,sk_c7) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_17786,c_10971]) ).
cnf(c_17865,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_21381]) ).
cnf(c_21382,plain,
( sk_c6 = sk_c7
| multiply(sk_c6,sk_c7) = sk_c5
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_17865,c_4959]) ).
cnf(c_18092,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_21382]) ).
cnf(c_21383,plain,
( sk_c5 = identity
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_18092,c_17763]) ).
cnf(c_21384,plain,
( identity = sk_c5
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_21383]) ).
cnf(c_18193,plain,
( identity = sk_c5
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_21384]) ).
cnf(c_21385,plain,
( identity = sk_c7
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_17786,c_18193]) ).
cnf(c_18262,plain,
( identity = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_21385]) ).
cnf(c_18280,plain,
( inverse(sk_c7) = identity
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_18262,c_449]) ).
cnf(c_21386,plain,
( multiply(identity,sk_c6) = sk_c5
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_18280,c_11015]) ).
cnf(c_21387,plain,
( sk_c6 = sk_c5
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_1,c_21386]) ).
cnf(c_21388,plain,
( sk_c5 = sk_c6
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_21387]) ).
cnf(c_18417,plain,
( sk_c5 = sk_c6
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_21388]) ).
cnf(c_21389,plain,
( sk_c6 = sk_c7
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_18417,c_17786]) ).
cnf(c_21390,plain,
( sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_21389]) ).
cnf(c_18484,plain,
sk_c6 = sk_c7,
inference(copy,[status(thm)],[c_21390]) ).
cnf(c_20385,plain,
( multiply(inverse(sk_c5),sk_c7) = inverse(sk_c7)
| sk_c2 = sk_c1 ),
inference(paramod,[status(thm)],[c_18484,c_11513]) ).
cnf(c_21391,plain,
( sk_c5 = sk_c7
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_9907]) ).
cnf(c_20828,plain,
sk_c5 = sk_c7,
inference(copy,[status(thm)],[c_21391]) ).
cnf(c_21392,plain,
( multiply(inverse(sk_c7),sk_c7) = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_9677]) ).
cnf(c_21393,plain,
( identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_21392]) ).
cnf(c_20852,plain,
identity = sk_c7,
inference(copy,[status(thm)],[c_21393]) ).
cnf(c_21394,plain,
( multiply(sk_c5,multiply(sk_c7,inverse(sk_c6))) = identity
| multiply(sk_c7,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_20828,c_1024]) ).
cnf(c_21395,plain,
( multiply(sk_c5,multiply(sk_c7,inverse(sk_c6))) = identity
| multiply(sk_c7,sk_c7) = sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_21394]) ).
cnf(c_21396,plain,
( multiply(sk_c7,multiply(sk_c7,inverse(sk_c6))) = identity
| multiply(sk_c7,sk_c7) = sk_c7 ),
inference(paramod,[status(thm)],[c_20828,c_21395]) ).
cnf(c_21397,plain,
( multiply(sk_c7,multiply(sk_c7,inverse(sk_c7))) = identity
| multiply(sk_c7,sk_c7) = sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_21396]) ).
cnf(c_21398,plain,
( multiply(sk_c7,identity) = identity
| multiply(sk_c7,sk_c7) = sk_c7 ),
inference(paramod,[status(thm)],[c_630,c_21397]) ).
cnf(c_21399,plain,
( multiply(sk_c7,sk_c7) = identity
| multiply(sk_c7,sk_c7) = sk_c7 ),
inference(paramod,[status(thm)],[c_20852,c_21398]) ).
cnf(c_21400,plain,
( multiply(sk_c7,sk_c7) = sk_c7
| multiply(sk_c7,sk_c7) = sk_c7 ),
inference(paramod,[status(thm)],[c_20852,c_21399]) ).
cnf(c_21172,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(copy,[status(thm)],[c_21400]) ).
cnf(c_21401,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| inverse(sk_c6) != sk_c5
| identity != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| multiply(sk_c7,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_20828,c_899]) ).
cnf(c_21402,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| inverse(sk_c6) != sk_c5
| identity != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| sk_c7 != sk_c6 ),
inference(paramod,[status(thm)],[c_21172,c_21401]) ).
cnf(c_21403,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| inverse(sk_c6) != sk_c5
| identity != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_21402]) ).
cnf(c_21404,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| inverse(sk_c6) != sk_c5
| identity != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(sk_c7,sk_c7) != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_20828,c_21403]) ).
cnf(c_21405,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| inverse(sk_c6) != sk_c5
| identity != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c7 != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_21172,c_21404]) ).
cnf(c_21406,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| inverse(sk_c6) != sk_c5
| identity != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_21405]) ).
cnf(c_21407,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| inverse(sk_c6) != sk_c5
| identity != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_21406]) ).
cnf(c_21408,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| inverse(sk_c6) != sk_c5
| identity != sk_c7
| inverse(sk_c6) != sk_c7
| sk_c7 != sk_c5
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_21172,c_21407]) ).
cnf(c_21409,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| inverse(sk_c6) != sk_c5
| identity != sk_c7
| inverse(sk_c6) != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_20828,c_21408]) ).
cnf(c_21410,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| inverse(sk_c6) != sk_c5
| identity != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_21409]) ).
cnf(c_21411,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| inverse(sk_c6) != sk_c5
| sk_c7 != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_20852,c_21410]) ).
cnf(c_21412,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| inverse(sk_c7) != sk_c5
| sk_c7 != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_21411]) ).
cnf(c_21413,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_20828,c_21412]) ).
cnf(c_21414,plain,
( multiply(inverse(sk_c7),sk_c7) != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_21413]) ).
cnf(c_21415,plain,
( identity != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_21414]) ).
cnf(c_21416,plain,
( sk_c7 != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_20852,c_21415]) ).
cnf(c_21417,plain,
( sk_c7 != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(copy,[status(thm)],[c_21416]) ).
cnf(c_21418,plain,
( sk_c7 != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7 ),
inference(copy,[status(thm)],[c_21417]) ).
cnf(c_21419,plain,
( sk_c7 != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7
| inverse(sk_c7) != sk_c7 ),
inference(copy,[status(thm)],[c_21418]) ).
cnf(c_21420,plain,
( sk_c7 != sk_c7
| inverse(sk_c7) != sk_c7
| inverse(sk_c7) != sk_c7 ),
inference(copy,[status(thm)],[c_21419]) ).
cnf(c_21421,plain,
( inverse(sk_c7) != sk_c7
| inverse(sk_c7) != sk_c7 ),
inference(copy,[status(thm)],[c_21420]) ).
cnf(c_21201,plain,
inverse(sk_c7) != sk_c7,
inference(copy,[status(thm)],[c_21421]) ).
cnf(c_21422,plain,
( inverse(sk_c7) = sk_c6
| inverse(sk_c7) = sk_c1 ),
inference(paramod,[status(thm)],[c_20828,c_855]) ).
cnf(c_21423,plain,
( inverse(sk_c7) = sk_c7
| inverse(sk_c7) = sk_c1 ),
inference(paramod,[status(thm)],[c_18484,c_21422]) ).
cnf(c_21203,plain,
inverse(sk_c7) = sk_c1,
inference(resolve,[status(thm)],[c_21201,c_21423]) ).
cnf(c_21424,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c7
| inverse(sk_c5) != sk_c7
| multiply(sk_c7,sk_c6) != sk_c6
| multiply(sk_c7,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_20828,c_676]) ).
cnf(c_21425,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c7
| inverse(sk_c5) != sk_c7
| multiply(sk_c7,sk_c6) != sk_c6
| sk_c7 != sk_c6 ),
inference(paramod,[status(thm)],[c_21172,c_21424]) ).
cnf(c_21426,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c7
| inverse(sk_c5) != sk_c7
| multiply(sk_c7,sk_c6) != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_21425]) ).
cnf(c_21427,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c7
| inverse(sk_c5) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_21426]) ).
cnf(c_21428,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c7
| inverse(sk_c5) != sk_c7
| sk_c7 != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_21172,c_21427]) ).
cnf(c_21429,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c7
| inverse(sk_c5) != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_21428]) ).
cnf(c_21430,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_20828,c_21429]) ).
cnf(c_21431,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_21203,c_21430]) ).
cnf(c_21432,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_20852,c_21431]) ).
cnf(c_21433,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| multiply(sk_c7,sk_c7) != sk_c5
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_21432]) ).
cnf(c_21434,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| sk_c7 != sk_c5
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_21172,c_21433]) ).
cnf(c_21435,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_20828,c_21434]) ).
cnf(c_21436,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c7) != sk_c5
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_21435]) ).
cnf(c_21437,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| sk_c1 != sk_c5
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_21203,c_21436]) ).
cnf(c_21438,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_20828,c_21437]) ).
cnf(c_21439,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_20828,c_21438]) ).
cnf(c_21440,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| sk_c7 != sk_c6
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_21172,c_21439]) ).
cnf(c_21441,plain,
( multiply(sk_c5,sk_c6) != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_21440]) ).
cnf(c_21442,plain,
( multiply(sk_c7,sk_c6) != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_20828,c_21441]) ).
cnf(c_21443,plain,
( multiply(sk_c7,sk_c7) != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_21442]) ).
cnf(c_21444,plain,
( sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_21172,c_21443]) ).
cnf(c_21445,plain,
( sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7 ),
inference(copy,[status(thm)],[c_21444]) ).
cnf(c_21446,plain,
( sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7 ),
inference(copy,[status(thm)],[c_21445]) ).
cnf(c_21447,plain,
( sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7 ),
inference(copy,[status(thm)],[c_21446]) ).
cnf(c_21448,plain,
( sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c1 != sk_c7 ),
inference(copy,[status(thm)],[c_21447]) ).
cnf(c_21449,plain,
( sk_c7 != sk_c7
| sk_c1 != sk_c7
| sk_c1 != sk_c7 ),
inference(copy,[status(thm)],[c_21448]) ).
cnf(c_21450,plain,
( sk_c1 != sk_c7
| sk_c1 != sk_c7 ),
inference(copy,[status(thm)],[c_21449]) ).
cnf(c_21251,plain,
sk_c1 != sk_c7,
inference(copy,[status(thm)],[c_21450]) ).
cnf(c_21451,plain,
( multiply(inverse(sk_c5),A) = multiply(sk_c3,A)
| inverse(sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_18484,c_645]) ).
cnf(c_21452,plain,
( multiply(inverse(sk_c5),A) = multiply(sk_c3,A)
| sk_c1 = sk_c5 ),
inference(paramod,[status(thm)],[c_21203,c_21451]) ).
cnf(c_21453,plain,
( multiply(inverse(sk_c5),A) = multiply(sk_c3,A)
| sk_c1 = sk_c7 ),
inference(paramod,[status(thm)],[c_20828,c_21452]) ).
cnf(c_21454,plain,
( multiply(inverse(sk_c7),A) = multiply(sk_c3,A)
| sk_c1 = sk_c7 ),
inference(paramod,[status(thm)],[c_20828,c_21453]) ).
cnf(c_21455,plain,
( multiply(sk_c1,A) = multiply(sk_c3,A)
| sk_c1 = sk_c7 ),
inference(paramod,[status(thm)],[c_21203,c_21454]) ).
cnf(c_21456,plain,
( multiply(sk_c3,A) = multiply(sk_c1,A)
| sk_c1 = sk_c7 ),
inference(copy,[status(thm)],[c_21455]) ).
cnf(c_21255,plain,
multiply(sk_c3,A) = multiply(sk_c1,A),
inference(resolve,[status(thm)],[c_21251,c_21456]) ).
cnf(c_21457,plain,
( inverse(sk_c6) = sk_c5
| multiply(sk_c3,sk_c7) = sk_c7 ),
inference(paramod,[status(thm)],[c_20828,c_25]) ).
cnf(c_21458,plain,
( inverse(sk_c6) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c7 ),
inference(paramod,[status(thm)],[c_21255,c_21457]) ).
cnf(c_21459,plain,
( inverse(sk_c7) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c7 ),
inference(paramod,[status(thm)],[c_18484,c_21458]) ).
cnf(c_21460,plain,
( sk_c1 = sk_c5
| multiply(sk_c1,sk_c7) = sk_c7 ),
inference(paramod,[status(thm)],[c_21203,c_21459]) ).
cnf(c_21461,plain,
( sk_c1 = sk_c7
| multiply(sk_c1,sk_c7) = sk_c7 ),
inference(paramod,[status(thm)],[c_20828,c_21460]) ).
cnf(c_21291,plain,
multiply(sk_c1,sk_c7) = sk_c7,
inference(resolve,[status(thm)],[c_21251,c_21461]) ).
cnf(c_21462,plain,
( inverse(sk_c6) = sk_c5
| sk_c7 = sk_c2 ),
inference(paramod,[status(thm)],[c_21291,c_15]) ).
cnf(c_21463,plain,
( inverse(sk_c7) = sk_c5
| sk_c7 = sk_c2 ),
inference(paramod,[status(thm)],[c_18484,c_21462]) ).
cnf(c_21464,plain,
( sk_c1 = sk_c5
| sk_c7 = sk_c2 ),
inference(paramod,[status(thm)],[c_21203,c_21463]) ).
cnf(c_21465,plain,
( sk_c1 = sk_c7
| sk_c7 = sk_c2 ),
inference(paramod,[status(thm)],[c_20828,c_21464]) ).
cnf(c_21466,plain,
( sk_c1 = sk_c7
| sk_c2 = sk_c7 ),
inference(copy,[status(thm)],[c_21465]) ).
cnf(c_21294,plain,
sk_c2 = sk_c7,
inference(resolve,[status(thm)],[c_21251,c_21466]) ).
cnf(c_21467,plain,
( multiply(inverse(sk_c5),sk_c7) = inverse(sk_c7)
| sk_c7 = sk_c1 ),
inference(paramod,[status(thm)],[c_21294,c_20385]) ).
cnf(c_21468,plain,
( multiply(inverse(sk_c7),sk_c7) = inverse(sk_c7)
| sk_c7 = sk_c1 ),
inference(paramod,[status(thm)],[c_20828,c_21467]) ).
cnf(c_21469,plain,
( multiply(sk_c1,sk_c7) = inverse(sk_c7)
| sk_c7 = sk_c1 ),
inference(paramod,[status(thm)],[c_21203,c_21468]) ).
cnf(c_21470,plain,
( sk_c7 = inverse(sk_c7)
| sk_c7 = sk_c1 ),
inference(paramod,[status(thm)],[c_21291,c_21469]) ).
cnf(c_21471,plain,
( sk_c7 = sk_c1
| sk_c7 = sk_c1 ),
inference(paramod,[status(thm)],[c_21203,c_21470]) ).
cnf(c_21472,plain,
( sk_c7 = sk_c1
| sk_c1 = sk_c7 ),
inference(copy,[status(thm)],[c_21471]) ).
cnf(c_21473,plain,
( sk_c1 = sk_c7
| sk_c1 = sk_c7 ),
inference(copy,[status(thm)],[c_21472]) ).
cnf(c_21474,plain,
sk_c1 = sk_c7,
inference(copy,[status(thm)],[c_21473]) ).
cnf(c_21307,plain,
$false,
inference(resolve,[status(thm)],[c_21251,c_21474]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP368-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/5.38 % Computer : n018.cluster.edu
% 0.12/5.38 % Model : x86_64 x86_64
% 0.12/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.38 % Memory : 8046.5625MB
% 0.12/5.38 % OS : Linux 6.8.0-71-generic
% 0.12/5.38 % CPULimit : 300
% 0.12/5.38 % WCLimit : 300
% 0.12/5.38 % DateTime : Fri Sep 25 14:50:42 UTC 2026
% 0.12/5.38 % CPUTime :
% 0.12/5.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/5.39 % Process 2226688 was started by sandbox2 on n018,
% 0.12/5.39 % Fri Sep 25 14:50:42 2026
% 0.12/5.39 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/5.39
% 0.12/5.39 % From the command line: assign(max_seconds, 300).
% 244.05/38.33
% 244.05/38.33 % given #500 (A,wt=55): 124 multiply(sk_c4,sk_c6) = sk_c7 | multiply(sk_c5,sk_c7) != sk_c6 | multiply(sk_c7,A) != sk_c6 | multiply(B,sk_c7) != A | inverse(B) != sk_c7 | multiply(sk_c1,sk_c5) != sk_c7 | sk_c5 != sk_c7 | multiply(sk_c6,sk_c7) != sk_c5 | inverse(sk_c6) != sk_c5 | multiply(sk_c7,sk_c5) != sk_c6 | inverse(C) != sk_c7 | multiply(C,sk_c6) != sk_c7. [para(23(a,1),34(f,1)),flip(g)].
% 244.05/38.33
% 244.05/38.33 % SZS status Unsatisfiable for theBenchmark
% 244.05/38.33
% 244.05/38.33 % Proof 1 at 26.83 (+ 4.29) seconds.
% 244.05/38.33 % Length of proof is 149.
% 244.05/38.33 % Level of proof is 35.
% 244.05/38.33 % Maximum clause weight is 51.000.
% 244.05/38.33 % Given clauses 964.
% 244.05/38.33
% 244.05/38.33 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------