%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP237-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 : n012.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:26 AM UTC 2026
% Result : Unsatisfiable 38.13s 5.17s
% Output : CNFRefutation 38.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 92
% Number of leaves : 27
% Syntax : Number of formulae : 431 ( 45 unt; 0 def)
% Number of atoms : 1112 (1111 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 1041 ( 360 ~; 681 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 132 ( 0 sgn 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(left_identity,axiom,
! [VAR_0] : multiply(identity,VAR_0) = VAR_0,
file('theBenchmark.p',left_identity) ).
cnf(c_1,plain,
multiply(identity,A) = A,
inference(clausify,[status(thm)],[left_identity]) ).
fof(left_inverse,axiom,
! [VAR_0] : multiply(inverse(VAR_0),VAR_0) = identity,
file('theBenchmark.p',left_inverse) ).
cnf(c_2,plain,
multiply(inverse(A),A) = identity,
inference(clausify,[status(thm)],[left_inverse]) ).
fof(associativity,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(multiply(VAR_0,VAR_1),VAR_2) = multiply(VAR_0,multiply(VAR_1,VAR_2)),
file('theBenchmark.p',associativity) ).
cnf(c_3,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(clausify,[status(thm)],[associativity]) ).
fof(prove_this_1,axiom,
( multiply(sk_c4,sk_c5) = sk_c9
| inverse(sk_c9) = sk_c8 ),
file('theBenchmark.p',prove_this_1) ).
cnf(c_4,plain,
( multiply(sk_c4,sk_c5) = sk_c9
| inverse(sk_c9) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_1]) ).
fof(prove_this_2,axiom,
( inverse(sk_c4) = sk_c5
| inverse(sk_c9) = sk_c8 ),
file('theBenchmark.p',prove_this_2) ).
cnf(c_5,plain,
( inverse(sk_c4) = sk_c5
| inverse(sk_c9) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_2]) ).
fof(prove_this_4,axiom,
( multiply(sk_c9,sk_c7) = sk_c8
| inverse(sk_c9) = sk_c8 ),
file('theBenchmark.p',prove_this_4) ).
cnf(c_7,plain,
( multiply(sk_c9,sk_c7) = sk_c8
| inverse(sk_c9) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_4]) ).
fof(prove_this_5,axiom,
( multiply(sk_c6,sk_c9) = sk_c7
| inverse(sk_c9) = sk_c8 ),
file('theBenchmark.p',prove_this_5) ).
cnf(c_8,plain,
( multiply(sk_c6,sk_c9) = sk_c7
| inverse(sk_c9) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_5]) ).
fof(prove_this_6,axiom,
( inverse(sk_c6) = sk_c9
| inverse(sk_c9) = sk_c8 ),
file('theBenchmark.p',prove_this_6) ).
cnf(c_9,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c9) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_6]) ).
fof(prove_this_7,axiom,
( multiply(sk_c4,sk_c5) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('theBenchmark.p',prove_this_7) ).
cnf(c_10,plain,
( multiply(sk_c4,sk_c5) = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_7]) ).
fof(prove_this_8,axiom,
( inverse(sk_c4) = sk_c5
| inverse(sk_c1) = sk_c9 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_11,plain,
( inverse(sk_c4) = sk_c5
| inverse(sk_c1) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_8]) ).
fof(prove_this_12,axiom,
( inverse(sk_c6) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('theBenchmark.p',prove_this_12) ).
cnf(c_15,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_12]) ).
fof(prove_this_13,axiom,
( multiply(sk_c4,sk_c5) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_13) ).
cnf(c_16,plain,
( multiply(sk_c4,sk_c5) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_13]) ).
fof(prove_this_14,axiom,
( inverse(sk_c4) = sk_c5
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_14) ).
cnf(c_17,plain,
( inverse(sk_c4) = sk_c5
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_14]) ).
fof(prove_this_15,axiom,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_15) ).
cnf(c_18,plain,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_15]) ).
fof(prove_this_16,axiom,
( multiply(sk_c9,sk_c7) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_16) ).
cnf(c_19,plain,
( multiply(sk_c9,sk_c7) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_16]) ).
fof(prove_this_17,axiom,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_17) ).
cnf(c_20,plain,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_17]) ).
fof(prove_this_18,axiom,
( inverse(sk_c6) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_18) ).
cnf(c_21,plain,
( inverse(sk_c6) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_18]) ).
fof(prove_this_20,axiom,
( inverse(sk_c4) = sk_c5
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('theBenchmark.p',prove_this_20) ).
cnf(c_23,plain,
( inverse(sk_c4) = sk_c5
| multiply(sk_c9,sk_c3) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_20]) ).
fof(prove_this_22,axiom,
( multiply(sk_c9,sk_c7) = sk_c8
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('theBenchmark.p',prove_this_22) ).
cnf(c_25,plain,
( multiply(sk_c9,sk_c7) = sk_c8
| multiply(sk_c9,sk_c3) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_22]) ).
fof(prove_this_23,axiom,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('theBenchmark.p',prove_this_23) ).
cnf(c_26,plain,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c9,sk_c3) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_23]) ).
fof(prove_this_24,axiom,
( inverse(sk_c6) = sk_c9
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('theBenchmark.p',prove_this_24) ).
cnf(c_27,plain,
( inverse(sk_c6) = sk_c9
| multiply(sk_c9,sk_c3) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_24]) ).
fof(prove_this_25,axiom,
( multiply(sk_c4,sk_c5) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c3 ),
file('theBenchmark.p',prove_this_25) ).
cnf(c_28,plain,
( multiply(sk_c4,sk_c5) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_25]) ).
fof(prove_this_26,axiom,
( inverse(sk_c4) = sk_c5
| multiply(sk_c2,sk_c9) = sk_c3 ),
file('theBenchmark.p',prove_this_26) ).
cnf(c_29,plain,
( inverse(sk_c4) = sk_c5
| multiply(sk_c2,sk_c9) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_26]) ).
fof(prove_this_30,axiom,
( inverse(sk_c6) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c3 ),
file('theBenchmark.p',prove_this_30) ).
cnf(c_33,plain,
( inverse(sk_c6) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_30]) ).
fof(prove_this_31,axiom,
( multiply(sk_c4,sk_c5) = sk_c9
| inverse(sk_c2) = sk_c9 ),
file('theBenchmark.p',prove_this_31) ).
cnf(c_34,plain,
( multiply(sk_c4,sk_c5) = sk_c9
| inverse(sk_c2) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_31]) ).
fof(prove_this_32,axiom,
( inverse(sk_c4) = sk_c5
| inverse(sk_c2) = sk_c9 ),
file('theBenchmark.p',prove_this_32) ).
cnf(c_35,plain,
( inverse(sk_c4) = sk_c5
| inverse(sk_c2) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_32]) ).
fof(prove_this_37,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( inverse(VAR_6) != sk_c9
| multiply(VAR_6,sk_c9) != VAR_5
| multiply(sk_c9,VAR_5) != sk_c8
| multiply(VAR_4,sk_c8) != sk_c9
| inverse(VAR_3) != VAR_4
| multiply(VAR_3,VAR_4) != sk_c9
| inverse(VAR_2) != sk_c9
| multiply(VAR_2,sk_c9) != VAR_1
| multiply(sk_c9,VAR_1) != sk_c8
| multiply(VAR_0,sk_c8) != sk_c9
| inverse(VAR_0) != sk_c9
| inverse(sk_c9) != sk_c8 ),
file('theBenchmark.p',prove_this_37) ).
cnf(c_40,plain,
( inverse(V6) != sk_c9
| multiply(V6,sk_c9) != F
| multiply(sk_c9,F) != sk_c8
| multiply(E,sk_c8) != sk_c9
| inverse(D) != E
| multiply(D,E) != sk_c9
| inverse(C) != sk_c9
| multiply(C,sk_c9) != B
| multiply(sk_c9,B) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(clausify,[status(thm)],[prove_this_37]) ).
cnf(c_42,plain,
( inverse(F) != sk_c9
| multiply(F,sk_c9) != E
| multiply(sk_c9,E) != sk_c8
| multiply(D,sk_c8) != sk_c9
| inverse(C) != D
| multiply(C,D) != sk_c9
| multiply(A,sk_c9) != B
| multiply(sk_c9,B) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(factor,[status(thm)],[c_40]) ).
cnf(c_16336,plain,
( inverse(C) != sk_c9
| multiply(C,sk_c9) != B
| multiply(sk_c9,B) != sk_c8
| multiply(sk_c9,sk_c8) != sk_c9
| inverse(A) != sk_c9
| multiply(A,sk_c9) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(factor,[status(thm)],[c_42]) ).
cnf(c_53,plain,
( inverse(C) != sk_c9
| multiply(C,sk_c9) != B
| multiply(sk_c9,B) != sk_c8
| multiply(sk_c9,sk_c8) != sk_c9
| multiply(A,sk_c9) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(copy,[status(thm)],[c_16336]) ).
cnf(c_16337,plain,
( inverse(A) != sk_c9
| multiply(sk_c9,B) != sk_c8
| multiply(D,sk_c8) != sk_c9
| inverse(C) != D
| multiply(C,D) != sk_c9
| multiply(A,sk_c9) != B
| multiply(sk_c9,B) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(factor,[status(thm)],[c_42]) ).
cnf(c_16338,plain,
( inverse(A) != sk_c9
| multiply(D,sk_c8) != sk_c9
| inverse(C) != D
| multiply(C,D) != sk_c9
| multiply(A,sk_c9) != B
| multiply(sk_c9,B) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(copy,[status(thm)],[c_16337]) ).
cnf(c_54,plain,
( multiply(D,sk_c8) != sk_c9
| inverse(C) != D
| multiply(C,D) != sk_c9
| multiply(A,sk_c9) != B
| multiply(sk_c9,B) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(copy,[status(thm)],[c_16338]) ).
cnf(c_16339,plain,
( inverse(A) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c8
| multiply(sk_c9,sk_c8) != sk_c9
| multiply(A,sk_c9) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(factor,[status(thm)],[c_53]) ).
cnf(c_16340,plain,
( inverse(A) != sk_c9
| multiply(sk_c9,sk_c8) != sk_c9
| multiply(A,sk_c9) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(copy,[status(thm)],[c_16339]) ).
cnf(c_68,plain,
( multiply(sk_c9,sk_c8) != sk_c9
| multiply(A,sk_c9) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(copy,[status(thm)],[c_16340]) ).
cnf(c_69,plain,
( multiply(sk_c8,sk_c8) != sk_c9
| inverse(A) != sk_c8
| multiply(A,sk_c9) != B
| multiply(sk_c9,B) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(factor,[status(thm)],[c_54]) ).
cnf(c_70,plain,
( inverse(C) != A
| multiply(C,A) != sk_c9
| multiply(A,sk_c9) != B
| multiply(sk_c9,B) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(factor,[status(thm)],[c_54]) ).
cnf(c_79,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c8
| multiply(sk_c9,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(factor,[status(thm)],[c_68]) ).
cnf(c_80,plain,
( inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c9) != A
| multiply(sk_c9,A) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c9
| inverse(sk_c8) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(factor,[status(thm)],[c_69]) ).
cnf(c_16341,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_16342,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_16341]) ).
cnf(c_81,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_16342]) ).
cnf(c_86,plain,
( multiply(sk_c5,sk_c4) = identity
| inverse(sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_5,c_2]) ).
cnf(c_97,plain,
( multiply(sk_c9,sk_c6) = identity
| inverse(sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_9,c_2]) ).
cnf(c_101,plain,
( multiply(sk_c9,sk_c1) = identity
| inverse(sk_c4) = sk_c5 ),
inference(paramod,[status(thm)],[c_11,c_2]) ).
cnf(c_102,plain,
( multiply(sk_c5,sk_c4) = identity
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_11,c_2]) ).
cnf(c_112,plain,
( multiply(sk_c9,sk_c1) = identity
| inverse(sk_c6) = sk_c9 ),
inference(paramod,[status(thm)],[c_15,c_2]) ).
cnf(c_113,plain,
( multiply(sk_c9,sk_c6) = identity
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_15,c_2]) ).
cnf(c_16343,plain,
( multiply(sk_c9,A) = multiply(sk_c4,multiply(sk_c5,A))
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_16,c_3]) ).
cnf(c_116,plain,
( multiply(sk_c4,multiply(sk_c5,A)) = multiply(sk_c9,A)
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(copy,[status(thm)],[c_16343]) ).
cnf(c_16344,plain,
( multiply(sk_c9,A) = multiply(sk_c5,multiply(sk_c8,A))
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_18,c_3]) ).
cnf(c_123,plain,
( multiply(sk_c5,multiply(sk_c8,A)) = multiply(sk_c9,A)
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(copy,[status(thm)],[c_16344]) ).
cnf(c_16345,plain,
( multiply(multiply(A,sk_c9),sk_c7) = multiply(A,sk_c8)
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_19,c_3]) ).
cnf(c_128,plain,
( multiply(A,multiply(sk_c9,sk_c7)) = multiply(A,sk_c8)
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_3,c_16345]) ).
cnf(c_131,plain,
( multiply(sk_c7,A) = multiply(sk_c6,multiply(sk_c9,A))
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_20,c_3]) ).
cnf(c_16346,plain,
( multiply(multiply(A,sk_c6),sk_c9) = multiply(A,sk_c7)
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_20,c_3]) ).
cnf(c_132,plain,
( multiply(A,multiply(sk_c6,sk_c9)) = multiply(A,sk_c7)
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_3,c_16346]) ).
cnf(c_16347,plain,
( multiply(multiply(A,sk_c9),sk_c3) = multiply(A,sk_c8)
| inverse(sk_c4) = sk_c5 ),
inference(paramod,[status(thm)],[c_23,c_3]) ).
cnf(c_142,plain,
( multiply(A,multiply(sk_c9,sk_c3)) = multiply(A,sk_c8)
| inverse(sk_c4) = sk_c5 ),
inference(paramod,[status(thm)],[c_3,c_16347]) ).
cnf(c_16348,plain,
( multiply(multiply(A,sk_c9),sk_c3) = multiply(A,sk_c8)
| multiply(sk_c6,sk_c9) = sk_c7 ),
inference(paramod,[status(thm)],[c_26,c_3]) ).
cnf(c_152,plain,
( multiply(A,multiply(sk_c9,sk_c3)) = multiply(A,sk_c8)
| multiply(sk_c6,sk_c9) = sk_c7 ),
inference(paramod,[status(thm)],[c_3,c_16348]) ).
cnf(c_16349,plain,
( multiply(multiply(A,sk_c6),sk_c9) = multiply(A,sk_c7)
| multiply(sk_c9,sk_c3) = sk_c8 ),
inference(paramod,[status(thm)],[c_26,c_3]) ).
cnf(c_154,plain,
( multiply(A,multiply(sk_c6,sk_c9)) = multiply(A,sk_c7)
| multiply(sk_c9,sk_c3) = sk_c8 ),
inference(paramod,[status(thm)],[c_3,c_16349]) ).
cnf(c_16350,plain,
( multiply(multiply(A,sk_c2),sk_c9) = multiply(A,sk_c3)
| inverse(sk_c6) = sk_c9 ),
inference(paramod,[status(thm)],[c_33,c_3]) ).
cnf(c_179,plain,
( multiply(A,multiply(sk_c2,sk_c9)) = multiply(A,sk_c3)
| inverse(sk_c6) = sk_c9 ),
inference(paramod,[status(thm)],[c_3,c_16350]) ).
cnf(c_183,plain,
( multiply(sk_c9,sk_c2) = identity
| inverse(sk_c4) = sk_c5 ),
inference(paramod,[status(thm)],[c_35,c_2]) ).
cnf(c_184,plain,
( multiply(sk_c5,sk_c4) = identity
| inverse(sk_c2) = sk_c9 ),
inference(paramod,[status(thm)],[c_35,c_2]) ).
cnf(c_214,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c9) != sk_c3
| multiply(sk_c8,sk_c8) != sk_c9
| inverse(sk_c8) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(resolve,[status(thm)],[c_80,c_27]) ).
cnf(c_218,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_81]) ).
cnf(c_219,plain,
multiply(inverse(multiply(A,B)),multiply(A,multiply(B,C))) = C,
inference(paramod,[status(thm)],[c_3,c_81]) ).
cnf(c_227,plain,
( multiply(inverse(sk_c9),sk_c8) = sk_c7
| inverse(sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_7,c_81]) ).
cnf(c_292,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_81,c_81]) ).
cnf(c_293,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_292,c_218]) ).
cnf(c_342,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_293,c_2]) ).
cnf(c_16351,plain,
( inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c9) != identity
| sk_c9 != sk_c8
| multiply(sk_c8,sk_c8) != sk_c9
| inverse(sk_c8) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(paramod,[status(thm)],[c_293,c_80]) ).
cnf(c_347,plain,
( inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c9) != identity
| sk_c8 != sk_c9
| multiply(sk_c8,sk_c8) != sk_c9
| inverse(sk_c8) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(copy,[status(thm)],[c_16351]) ).
cnf(c_16352,plain,
( multiply(identity,identity) != sk_c9
| multiply(identity,sk_c9) != A
| multiply(sk_c9,A) != sk_c8
| multiply(identity,sk_c8) != sk_c9
| inverse(identity) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(resolve,[status(thm)],[c_342,c_70]) ).
cnf(c_16353,plain,
( multiply(identity,identity) != sk_c9
| multiply(identity,sk_c9) != A
| multiply(sk_c9,A) != sk_c8
| multiply(identity,sk_c8) != sk_c9
| identity != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(paramod,[status(thm)],[c_342,c_16352]) ).
cnf(c_16354,plain,
( multiply(identity,identity) != sk_c9
| multiply(identity,sk_c9) != A
| multiply(sk_c9,A) != sk_c8
| sk_c8 != sk_c9
| identity != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(paramod,[status(thm)],[c_1,c_16353]) ).
cnf(c_16355,plain,
( multiply(identity,identity) != sk_c9
| sk_c9 != A
| multiply(sk_c9,A) != sk_c8
| sk_c8 != sk_c9
| identity != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(paramod,[status(thm)],[c_1,c_16354]) ).
cnf(c_16356,plain,
( identity != sk_c9
| sk_c9 != A
| multiply(sk_c9,A) != sk_c8
| sk_c8 != sk_c9
| identity != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(paramod,[status(thm)],[c_293,c_16355]) ).
cnf(c_397,plain,
( sk_c9 != A
| multiply(sk_c9,A) != sk_c8
| sk_c8 != sk_c9
| identity != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(copy,[status(thm)],[c_16356]) ).
cnf(c_16357,plain,
( multiply(inverse(sk_c5),identity) = sk_c4
| inverse(sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_86,c_81]) ).
cnf(c_413,plain,
( inverse(sk_c5) = sk_c4
| inverse(sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_293,c_16357]) ).
cnf(c_16358,plain,
( sk_c9 != identity
| sk_c9 != sk_c8
| sk_c8 != sk_c9
| identity != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(paramod,[status(thm)],[c_293,c_397]) ).
cnf(c_16359,plain,
( sk_c9 != identity
| sk_c8 != sk_c9
| sk_c8 != sk_c9
| identity != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(copy,[status(thm)],[c_16358]) ).
cnf(c_16360,plain,
( identity != sk_c9
| sk_c8 != sk_c9
| sk_c8 != sk_c9
| identity != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(copy,[status(thm)],[c_16359]) ).
cnf(c_16361,plain,
( identity != sk_c9
| sk_c8 != sk_c9
| identity != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(copy,[status(thm)],[c_16360]) ).
cnf(c_479,plain,
( sk_c8 != sk_c9
| identity != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(copy,[status(thm)],[c_16361]) ).
cnf(c_513,plain,
( multiply(sk_c4,sk_c5) = identity
| inverse(sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_413,c_2]) ).
cnf(c_16362,plain,
( multiply(inverse(sk_c9),identity) = sk_c6
| inverse(sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_97,c_81]) ).
cnf(c_533,plain,
( inverse(sk_c9) = sk_c6
| inverse(sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_293,c_16362]) ).
cnf(c_540,plain,
( multiply(sk_c6,sk_c9) = identity
| inverse(sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_533,c_2]) ).
cnf(c_16363,plain,
( multiply(inverse(sk_c9),identity) = sk_c1
| inverse(sk_c4) = sk_c5 ),
inference(paramod,[status(thm)],[c_101,c_81]) ).
cnf(c_605,plain,
( inverse(sk_c9) = sk_c1
| inverse(sk_c4) = sk_c5 ),
inference(paramod,[status(thm)],[c_293,c_16363]) ).
cnf(c_16364,plain,
( inverse(sk_c4) = sk_c5
| sk_c1 = sk_c8
| inverse(sk_c4) = sk_c5 ),
inference(paramod,[status(thm)],[c_605,c_5]) ).
cnf(c_610,plain,
( sk_c1 = sk_c8
| inverse(sk_c4) = sk_c5 ),
inference(copy,[status(thm)],[c_16364]) ).
cnf(c_16365,plain,
( inverse(sk_c4) = sk_c5
| multiply(sk_c8,sk_c8) = sk_c9
| inverse(sk_c4) = sk_c5 ),
inference(paramod,[status(thm)],[c_610,c_17]) ).
cnf(c_617,plain,
( multiply(sk_c8,sk_c8) = sk_c9
| inverse(sk_c4) = sk_c5 ),
inference(copy,[status(thm)],[c_16365]) ).
cnf(c_16366,plain,
( multiply(inverse(sk_c5),identity) = sk_c4
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_102,c_81]) ).
cnf(c_707,plain,
( inverse(sk_c5) = sk_c4
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_293,c_16366]) ).
cnf(c_710,plain,
( multiply(sk_c4,sk_c5) = identity
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_707,c_2]) ).
cnf(c_16367,plain,
( multiply(inverse(sk_c9),identity) = sk_c1
| inverse(sk_c6) = sk_c9 ),
inference(paramod,[status(thm)],[c_112,c_81]) ).
cnf(c_726,plain,
( inverse(sk_c9) = sk_c1
| inverse(sk_c6) = sk_c9 ),
inference(paramod,[status(thm)],[c_293,c_16367]) ).
cnf(c_16368,plain,
( inverse(sk_c6) = sk_c9
| sk_c1 = sk_c8
| inverse(sk_c6) = sk_c9 ),
inference(paramod,[status(thm)],[c_726,c_9]) ).
cnf(c_755,plain,
( sk_c1 = sk_c8
| inverse(sk_c6) = sk_c9 ),
inference(copy,[status(thm)],[c_16368]) ).
cnf(c_762,plain,
( multiply(sk_c9,sk_c6) = identity
| sk_c1 = sk_c8 ),
inference(paramod,[status(thm)],[c_755,c_2]) ).
cnf(c_16369,plain,
( inverse(sk_c6) = sk_c9
| multiply(sk_c8,sk_c8) = sk_c9
| inverse(sk_c6) = sk_c9 ),
inference(paramod,[status(thm)],[c_755,c_21]) ).
cnf(c_767,plain,
( multiply(sk_c8,sk_c8) = sk_c9
| inverse(sk_c6) = sk_c9 ),
inference(copy,[status(thm)],[c_16369]) ).
cnf(c_16370,plain,
( multiply(inverse(sk_c9),identity) = sk_c6
| sk_c1 = sk_c8 ),
inference(paramod,[status(thm)],[c_762,c_81]) ).
cnf(c_774,plain,
( inverse(sk_c9) = sk_c6
| sk_c1 = sk_c8 ),
inference(paramod,[status(thm)],[c_293,c_16370]) ).
cnf(c_776,plain,
( multiply(sk_c6,sk_c9) = identity
| sk_c1 = sk_c8 ),
inference(paramod,[status(thm)],[c_774,c_2]) ).
cnf(c_16371,plain,
( multiply(inverse(sk_c9),identity) = sk_c6
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_113,c_81]) ).
cnf(c_838,plain,
( inverse(sk_c9) = sk_c6
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_293,c_16371]) ).
cnf(c_16372,plain,
( inverse(sk_c9) = sk_c6
| inverse(sk_c8) = sk_c9
| inverse(sk_c9) = sk_c6 ),
inference(paramod,[status(thm)],[c_774,c_838]) ).
cnf(c_850,plain,
( inverse(sk_c8) = sk_c9
| inverse(sk_c9) = sk_c6 ),
inference(copy,[status(thm)],[c_16372]) ).
cnf(c_16373,plain,
( multiply(inverse(sk_c9),identity) = sk_c2
| inverse(sk_c4) = sk_c5 ),
inference(paramod,[status(thm)],[c_183,c_81]) ).
cnf(c_875,plain,
( inverse(sk_c9) = sk_c2
| inverse(sk_c4) = sk_c5 ),
inference(paramod,[status(thm)],[c_293,c_16373]) ).
cnf(c_878,plain,
( multiply(sk_c2,sk_c9) = identity
| inverse(sk_c4) = sk_c5 ),
inference(paramod,[status(thm)],[c_875,c_2]) ).
cnf(c_16374,plain,
( multiply(inverse(sk_c5),identity) = sk_c4
| inverse(sk_c2) = sk_c9 ),
inference(paramod,[status(thm)],[c_184,c_81]) ).
cnf(c_998,plain,
( inverse(sk_c5) = sk_c4
| inverse(sk_c2) = sk_c9 ),
inference(paramod,[status(thm)],[c_293,c_16374]) ).
cnf(c_1001,plain,
( multiply(sk_c4,sk_c5) = identity
| inverse(sk_c2) = sk_c9 ),
inference(paramod,[status(thm)],[c_998,c_2]) ).
cnf(c_16375,plain,
( identity = sk_c9
| inverse(sk_c9) = sk_c8
| inverse(sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_513,c_4]) ).
cnf(c_1285,plain,
( identity = sk_c9
| inverse(sk_c9) = sk_c8 ),
inference(copy,[status(thm)],[c_16375]) ).
cnf(c_1296,plain,
( multiply(sk_c8,sk_c9) = identity
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_1285,c_2]) ).
cnf(c_1299,plain,
( inverse(sk_c9) = identity
| inverse(sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_1285,c_342]) ).
cnf(c_16376,plain,
( multiply(inverse(sk_c8),identity) = sk_c9
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_1296,c_81]) ).
cnf(c_1408,plain,
( inverse(sk_c8) = sk_c9
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_293,c_16376]) ).
cnf(c_1440,plain,
( inverse(sk_c9) = identity
| inverse(sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_1408,c_342]) ).
cnf(c_16377,plain,
( inverse(sk_c8) = sk_c9
| identity = sk_c6
| inverse(sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_1440,c_850]) ).
cnf(c_1898,plain,
( identity = sk_c6
| inverse(sk_c8) = sk_c9 ),
inference(copy,[status(thm)],[c_16377]) ).
cnf(c_2128,plain,
( multiply(inverse(sk_c1),sk_c9) = sk_c8
| multiply(sk_c5,multiply(sk_c8,A)) = multiply(sk_c9,A) ),
inference(paramod,[status(thm)],[c_123,c_81]) ).
cnf(c_16378,plain,
( identity = sk_c7
| inverse(sk_c9) = sk_c8
| inverse(sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_540,c_8]) ).
cnf(c_2328,plain,
( identity = sk_c7
| inverse(sk_c9) = sk_c8 ),
inference(copy,[status(thm)],[c_16378]) ).
cnf(c_2334,plain,
( sk_c8 != sk_c9
| identity != sk_c9
| identity = sk_c7 ),
inference(resolve,[status(thm)],[c_2328,c_479]) ).
cnf(c_2347,plain,
( multiply(sk_c8,sk_c9) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2328,c_2]) ).
cnf(c_16379,plain,
( sk_c8 = sk_c6
| sk_c1 = sk_c8
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2328,c_774]) ).
cnf(c_2356,plain,
( sk_c6 = sk_c8
| sk_c1 = sk_c8
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_16379]) ).
cnf(c_16380,plain,
( inverse(sk_c9) = sk_c7
| inverse(sk_c9) = sk_c8
| inverse(sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_2328,c_1299]) ).
cnf(c_2366,plain,
( inverse(sk_c9) = sk_c7
| inverse(sk_c9) = sk_c8 ),
inference(copy,[status(thm)],[c_16380]) ).
cnf(c_2394,plain,
( multiply(inverse(sk_c8),multiply(sk_c9,sk_c7)) = identity
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_2,c_128]) ).
cnf(c_2396,plain,
( multiply(inverse(sk_c1),sk_c9) = sk_c8
| multiply(A,multiply(sk_c9,sk_c7)) = multiply(A,sk_c8) ),
inference(paramod,[status(thm)],[c_128,c_81]) ).
cnf(c_16381,plain,
( multiply(sk_c4,multiply(sk_c5,sk_c7)) = multiply(sk_c9,multiply(sk_c6,sk_c9))
| multiply(sk_c1,sk_c8) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_132,c_116]) ).
cnf(c_16382,plain,
( multiply(sk_c9,multiply(sk_c6,sk_c9)) = multiply(sk_c4,multiply(sk_c5,sk_c7))
| multiply(sk_c1,sk_c8) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(copy,[status(thm)],[c_16381]) ).
cnf(c_2892,plain,
( multiply(sk_c9,multiply(sk_c6,sk_c9)) = multiply(sk_c4,multiply(sk_c5,sk_c7))
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(copy,[status(thm)],[c_16382]) ).
cnf(c_16383,plain,
( multiply(inverse(sk_c8),identity) = sk_c9
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2347,c_81]) ).
cnf(c_2976,plain,
( inverse(sk_c8) = sk_c9
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_293,c_16383]) ).
cnf(c_16384,plain,
( sk_c7 = sk_c6
| inverse(sk_c8) = sk_c9
| inverse(sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_2976,c_1898]) ).
cnf(c_3035,plain,
( sk_c7 = sk_c6
| inverse(sk_c8) = sk_c9 ),
inference(copy,[status(thm)],[c_16384]) ).
cnf(c_3098,plain,
( multiply(sk_c9,sk_c8) = identity
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_3035,c_2]) ).
cnf(c_16385,plain,
( multiply(multiply(A,sk_c9),sk_c8) = multiply(A,identity)
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_3098,c_3]) ).
cnf(c_16386,plain,
( multiply(A,multiply(sk_c9,sk_c8)) = multiply(A,identity)
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_3,c_16385]) ).
cnf(c_3419,plain,
( multiply(A,multiply(sk_c9,sk_c8)) = A
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_293,c_16386]) ).
cnf(c_16387,plain,
( multiply(sk_c8,multiply(sk_c9,sk_c3)) = sk_c9
| inverse(sk_c4) = sk_c5
| inverse(sk_c4) = sk_c5 ),
inference(paramod,[status(thm)],[c_617,c_142]) ).
cnf(c_3641,plain,
( multiply(sk_c8,multiply(sk_c9,sk_c3)) = sk_c9
| inverse(sk_c4) = sk_c5 ),
inference(copy,[status(thm)],[c_16387]) ).
cnf(c_16388,plain,
( identity = sk_c9
| inverse(sk_c1) = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_710,c_10]) ).
cnf(c_3690,plain,
( identity = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(copy,[status(thm)],[c_16388]) ).
cnf(c_3710,plain,
( multiply(sk_c9,sk_c1) = identity
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_3690,c_2]) ).
cnf(c_16389,plain,
( multiply(inverse(sk_c9),identity) = sk_c1
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_3710,c_81]) ).
cnf(c_3740,plain,
( inverse(sk_c9) = sk_c1
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_293,c_16389]) ).
cnf(c_16390,plain,
( identity = sk_c9
| sk_c1 = sk_c8
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_3740,c_1285]) ).
cnf(c_3814,plain,
( sk_c1 = sk_c8
| identity = sk_c9 ),
inference(copy,[status(thm)],[c_16390]) ).
cnf(c_3875,plain,
( sk_c8 != sk_c9
| identity = sk_c7
| sk_c1 = sk_c8 ),
inference(resolve,[status(thm)],[c_3814,c_2334]) ).
cnf(c_3891,plain,
( inverse(sk_c9) = identity
| sk_c1 = sk_c8 ),
inference(paramod,[status(thm)],[c_3814,c_342]) ).
cnf(c_16391,plain,
( identity = sk_c6
| sk_c1 = sk_c8
| sk_c1 = sk_c8 ),
inference(paramod,[status(thm)],[c_3891,c_774]) ).
cnf(c_4062,plain,
( identity = sk_c6
| sk_c1 = sk_c8 ),
inference(copy,[status(thm)],[c_16391]) ).
cnf(c_16392,plain,
( inverse(sk_c9) = sk_c9
| sk_c1 = sk_c8
| sk_c1 = sk_c8 ),
inference(paramod,[status(thm)],[c_3814,c_3891]) ).
cnf(c_4097,plain,
( inverse(sk_c9) = sk_c9
| sk_c1 = sk_c8 ),
inference(copy,[status(thm)],[c_16392]) ).
cnf(c_16393,plain,
( sk_c1 = sk_c8
| sk_c6 = sk_c9
| sk_c1 = sk_c8 ),
inference(paramod,[status(thm)],[c_4062,c_3814]) ).
cnf(c_4140,plain,
( sk_c6 = sk_c9
| sk_c1 = sk_c8 ),
inference(copy,[status(thm)],[c_16393]) ).
cnf(c_16394,plain,
( sk_c9 = sk_c8
| sk_c1 = sk_c8
| identity = sk_c7
| sk_c1 = sk_c8 ),
inference(paramod,[status(thm)],[c_4140,c_2356]) ).
cnf(c_16395,plain,
( sk_c8 = sk_c9
| sk_c1 = sk_c8
| identity = sk_c7
| sk_c1 = sk_c8 ),
inference(copy,[status(thm)],[c_16394]) ).
cnf(c_4222,plain,
( sk_c8 = sk_c9
| identity = sk_c7
| sk_c1 = sk_c8 ),
inference(copy,[status(thm)],[c_16395]) ).
cnf(c_16396,plain,
( sk_c8 != sk_c9
| identity != sk_c9
| sk_c9 != sk_c8
| sk_c1 = sk_c8 ),
inference(paramod,[status(thm)],[c_4097,c_479]) ).
cnf(c_16397,plain,
( sk_c8 != sk_c9
| identity != sk_c9
| sk_c8 != sk_c9
| sk_c1 = sk_c8 ),
inference(copy,[status(thm)],[c_16396]) ).
cnf(c_4379,plain,
( identity != sk_c9
| sk_c8 != sk_c9
| sk_c1 = sk_c8 ),
inference(copy,[status(thm)],[c_16397]) ).
cnf(c_16398,plain,
( multiply(sk_c1,multiply(sk_c9,sk_c3)) = sk_c9
| multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c6,sk_c9) = sk_c7 ),
inference(paramod,[status(thm)],[c_20,c_152]) ).
cnf(c_4444,plain,
( multiply(sk_c1,multiply(sk_c9,sk_c3)) = sk_c9
| multiply(sk_c6,sk_c9) = sk_c7 ),
inference(copy,[status(thm)],[c_16398]) ).
cnf(c_16399,plain,
( identity = sk_c7
| sk_c1 = sk_c8
| identity = sk_c7
| sk_c1 = sk_c8 ),
inference(resolve,[status(thm)],[c_4222,c_3875]) ).
cnf(c_16400,plain,
( identity = sk_c7
| identity = sk_c7
| sk_c1 = sk_c8 ),
inference(copy,[status(thm)],[c_16399]) ).
cnf(c_4499,plain,
( identity = sk_c7
| sk_c1 = sk_c8 ),
inference(copy,[status(thm)],[c_16400]) ).
cnf(c_16401,plain,
( multiply(sk_c6,sk_c9) = sk_c7
| sk_c1 = sk_c8
| sk_c1 = sk_c8 ),
inference(paramod,[status(thm)],[c_4499,c_776]) ).
cnf(c_4537,plain,
( multiply(sk_c6,sk_c9) = sk_c7
| sk_c1 = sk_c8 ),
inference(copy,[status(thm)],[c_16401]) ).
cnf(c_16402,plain,
( multiply(sk_c9,multiply(sk_c6,sk_c9)) = sk_c8
| multiply(sk_c9,sk_c3) = sk_c8
| multiply(sk_c9,sk_c3) = sk_c8 ),
inference(paramod,[status(thm)],[c_25,c_154]) ).
cnf(c_4689,plain,
( multiply(sk_c9,multiply(sk_c6,sk_c9)) = sk_c8
| multiply(sk_c9,sk_c3) = sk_c8 ),
inference(copy,[status(thm)],[c_16402]) ).
cnf(c_16403,plain,
( sk_c1 = sk_c8
| sk_c8 != sk_c9
| sk_c1 = sk_c8 ),
inference(resolve,[status(thm)],[c_4379,c_3814]) ).
cnf(c_4727,plain,
( sk_c8 != sk_c9
| sk_c1 = sk_c8 ),
inference(copy,[status(thm)],[c_16403]) ).
cnf(c_16404,plain,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c8,sk_c8) = sk_c9
| multiply(sk_c6,sk_c9) = sk_c7 ),
inference(paramod,[status(thm)],[c_4537,c_20]) ).
cnf(c_5964,plain,
( multiply(sk_c8,sk_c8) = sk_c9
| multiply(sk_c6,sk_c9) = sk_c7 ),
inference(copy,[status(thm)],[c_16404]) ).
cnf(c_16405,plain,
( multiply(sk_c9,multiply(sk_c2,sk_c9)) = sk_c8
| inverse(sk_c6) = sk_c9
| inverse(sk_c6) = sk_c9 ),
inference(paramod,[status(thm)],[c_27,c_179]) ).
cnf(c_7974,plain,
( multiply(sk_c9,multiply(sk_c2,sk_c9)) = sk_c8
| inverse(sk_c6) = sk_c9 ),
inference(copy,[status(thm)],[c_16405]) ).
cnf(c_16406,plain,
( inverse(sk_c4) = sk_c5
| identity = sk_c3
| inverse(sk_c4) = sk_c5 ),
inference(paramod,[status(thm)],[c_878,c_29]) ).
cnf(c_9391,plain,
( identity = sk_c3
| inverse(sk_c4) = sk_c5 ),
inference(copy,[status(thm)],[c_16406]) ).
cnf(c_9437,plain,
( multiply(sk_c5,sk_c4) = identity
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_9391,c_2]) ).
cnf(c_16407,plain,
( multiply(inverse(sk_c5),identity) = sk_c4
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_9437,c_81]) ).
cnf(c_9452,plain,
( inverse(sk_c5) = sk_c4
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_293,c_16407]) ).
cnf(c_9502,plain,
( multiply(sk_c4,sk_c5) = identity
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_9452,c_2]) ).
cnf(c_9546,plain,
( identity = sk_c9
| multiply(sk_c2,sk_c9) = sk_c3
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_9502,c_28]) ).
cnf(c_16408,plain,
( identity = sk_c9
| inverse(sk_c2) = sk_c9
| inverse(sk_c2) = sk_c9 ),
inference(paramod,[status(thm)],[c_1001,c_34]) ).
cnf(c_9742,plain,
( identity = sk_c9
| inverse(sk_c2) = sk_c9 ),
inference(copy,[status(thm)],[c_16408]) ).
cnf(c_9769,plain,
( multiply(sk_c9,sk_c2) = identity
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_9742,c_2]) ).
cnf(c_16409,plain,
( multiply(inverse(sk_c9),identity) = sk_c2
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_9769,c_81]) ).
cnf(c_9810,plain,
( inverse(sk_c9) = sk_c2
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_293,c_16409]) ).
cnf(c_9824,plain,
( multiply(sk_c5,multiply(sk_c8,sk_c2)) = identity
| multiply(sk_c1,sk_c8) = sk_c9
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_9769,c_123]) ).
cnf(c_16410,plain,
( multiply(sk_c7,sk_c2) = multiply(sk_c6,identity)
| multiply(sk_c1,sk_c8) = sk_c9
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_9769,c_131]) ).
cnf(c_9826,plain,
( multiply(sk_c7,sk_c2) = sk_c6
| multiply(sk_c1,sk_c8) = sk_c9
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_293,c_16410]) ).
cnf(c_16411,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c6) = sk_c9
| inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c9) != sk_c3
| inverse(sk_c8) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(resolve,[status(thm)],[c_214,c_767]) ).
cnf(c_9896,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c9) != sk_c3
| inverse(sk_c8) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(copy,[status(thm)],[c_16411]) ).
cnf(c_16412,plain,
( identity = sk_c9
| sk_c2 = sk_c8
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_9810,c_1285]) ).
cnf(c_9976,plain,
( sk_c2 = sk_c8
| identity = sk_c9 ),
inference(copy,[status(thm)],[c_16412]) ).
cnf(c_16413,plain,
( sk_c2 = sk_c1
| identity = sk_c9
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_9810,c_3740]) ).
cnf(c_9991,plain,
( sk_c2 = sk_c1
| identity = sk_c9 ),
inference(copy,[status(thm)],[c_16413]) ).
cnf(c_10030,plain,
( inverse(sk_c9) = identity
| sk_c2 = sk_c8 ),
inference(paramod,[status(thm)],[c_9976,c_342]) ).
cnf(c_10087,plain,
( sk_c8 != sk_c9
| inverse(sk_c9) != sk_c8
| sk_c2 = sk_c1 ),
inference(resolve,[status(thm)],[c_9991,c_479]) ).
cnf(c_10099,plain,
( inverse(sk_c9) = identity
| sk_c2 = sk_c1 ),
inference(paramod,[status(thm)],[c_9991,c_342]) ).
cnf(c_10184,plain,
( multiply(inverse(sk_c8),multiply(sk_c9,multiply(sk_c7,A))) = A
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_19,c_219]) ).
cnf(c_16414,plain,
( inverse(sk_c9) = sk_c9
| sk_c2 = sk_c8
| sk_c2 = sk_c8 ),
inference(paramod,[status(thm)],[c_9976,c_10030]) ).
cnf(c_10544,plain,
( inverse(sk_c9) = sk_c9
| sk_c2 = sk_c8 ),
inference(copy,[status(thm)],[c_16414]) ).
cnf(c_16415,plain,
( inverse(sk_c9) = sk_c9
| sk_c2 = sk_c1
| sk_c2 = sk_c1 ),
inference(paramod,[status(thm)],[c_9991,c_10099]) ).
cnf(c_10761,plain,
( inverse(sk_c9) = sk_c9
| sk_c2 = sk_c1 ),
inference(copy,[status(thm)],[c_16415]) ).
cnf(c_16416,plain,
( multiply(identity,sk_c8) = sk_c7
| inverse(sk_c9) = sk_c8
| inverse(sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_1299,c_227]) ).
cnf(c_16417,plain,
( sk_c8 = sk_c7
| inverse(sk_c9) = sk_c8
| inverse(sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_1,c_16416]) ).
cnf(c_16418,plain,
( sk_c7 = sk_c8
| inverse(sk_c9) = sk_c8
| inverse(sk_c9) = sk_c8 ),
inference(copy,[status(thm)],[c_16417]) ).
cnf(c_11260,plain,
( sk_c7 = sk_c8
| inverse(sk_c9) = sk_c8 ),
inference(copy,[status(thm)],[c_16418]) ).
cnf(c_16419,plain,
( inverse(sk_c9) = sk_c8
| inverse(sk_c9) = sk_c8
| inverse(sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_11260,c_2366]) ).
cnf(c_16420,plain,
( inverse(sk_c9) = sk_c8
| inverse(sk_c9) = sk_c8 ),
inference(copy,[status(thm)],[c_16419]) ).
cnf(c_12224,plain,
inverse(sk_c9) = sk_c8,
inference(copy,[status(thm)],[c_16420]) ).
cnf(c_12307,plain,
( sk_c8 = sk_c9
| sk_c2 = sk_c1 ),
inference(paramod,[status(thm)],[c_12224,c_10761]) ).
cnf(c_12330,plain,
( sk_c8 = sk_c9
| sk_c2 = sk_c8 ),
inference(paramod,[status(thm)],[c_12224,c_10544]) ).
cnf(c_16421,plain,
( sk_c8 != sk_c9
| sk_c8 != sk_c8
| sk_c2 = sk_c1 ),
inference(paramod,[status(thm)],[c_12224,c_10087]) ).
cnf(c_12397,plain,
( sk_c8 != sk_c9
| sk_c2 = sk_c1 ),
inference(copy,[status(thm)],[c_16421]) ).
cnf(c_16422,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c9) != sk_c3
| inverse(sk_c8) != sk_c9
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_12224,c_9896]) ).
cnf(c_12416,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c9) != sk_c3
| inverse(sk_c8) != sk_c9 ),
inference(copy,[status(thm)],[c_16422]) ).
cnf(c_16423,plain,
( sk_c8 != sk_c9
| identity != sk_c9
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_12224,c_479]) ).
cnf(c_13071,plain,
( sk_c8 != sk_c9
| identity != sk_c9 ),
inference(copy,[status(thm)],[c_16423]) ).
cnf(c_16424,plain,
( inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c9) != identity
| sk_c8 != sk_c9
| multiply(sk_c8,sk_c8) != sk_c9
| inverse(sk_c8) != sk_c9
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_12224,c_347]) ).
cnf(c_13076,plain,
( inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c9) != identity
| sk_c8 != sk_c9
| multiply(sk_c8,sk_c8) != sk_c9
| inverse(sk_c8) != sk_c9 ),
inference(copy,[status(thm)],[c_16424]) ).
cnf(c_16425,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c8
| multiply(sk_c9,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c9
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_12224,c_79]) ).
cnf(c_16426,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c8
| multiply(sk_c9,sk_c8) != sk_c9
| sk_c8 != sk_c9
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_12224,c_16425]) ).
cnf(c_13090,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c8
| multiply(sk_c9,sk_c8) != sk_c9
| sk_c8 != sk_c9 ),
inference(copy,[status(thm)],[c_16426]) ).
cnf(c_13096,plain,
multiply(sk_c8,sk_c9) = identity,
inference(paramod,[status(thm)],[c_12224,c_2]) ).
cnf(c_13097,plain,
multiply(sk_c8,multiply(sk_c9,A)) = A,
inference(paramod,[status(thm)],[c_12224,c_81]) ).
cnf(c_16427,plain,
( inverse(sk_c8) != sk_c8
| identity != identity
| sk_c8 != sk_c9
| multiply(sk_c8,sk_c8) != sk_c9
| inverse(sk_c8) != sk_c9 ),
inference(paramod,[status(thm)],[c_13096,c_13076]) ).
cnf(c_13103,plain,
( inverse(sk_c8) != sk_c8
| sk_c8 != sk_c9
| multiply(sk_c8,sk_c8) != sk_c9
| inverse(sk_c8) != sk_c9 ),
inference(copy,[status(thm)],[c_16427]) ).
cnf(c_13221,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c8) != sk_c8
| identity != sk_c3
| inverse(sk_c8) != sk_c9 ),
inference(paramod,[status(thm)],[c_13096,c_12416]) ).
cnf(c_13505,plain,
( sk_c3 = sk_c9
| inverse(sk_c4) = sk_c5 ),
inference(paramod,[status(thm)],[c_13097,c_3641]) ).
cnf(c_13789,plain,
( sk_c1 = sk_c8
| sk_c2 = sk_c8 ),
inference(resolve,[status(thm)],[c_12330,c_4727]) ).
cnf(c_16428,plain,
( sk_c2 = sk_c1
| sk_c2 = sk_c1 ),
inference(resolve,[status(thm)],[c_12397,c_12307]) ).
cnf(c_14017,plain,
sk_c2 = sk_c1,
inference(copy,[status(thm)],[c_16428]) ).
cnf(c_16429,plain,
( sk_c1 = sk_c8
| sk_c1 = sk_c8 ),
inference(paramod,[status(thm)],[c_14017,c_13789]) ).
cnf(c_14054,plain,
sk_c1 = sk_c8,
inference(copy,[status(thm)],[c_16429]) ).
cnf(c_16430,plain,
( multiply(sk_c7,sk_c2) = sk_c6
| multiply(sk_c8,sk_c8) = sk_c9
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_14054,c_9826]) ).
cnf(c_16431,plain,
( multiply(sk_c7,sk_c1) = sk_c6
| multiply(sk_c8,sk_c8) = sk_c9
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_14017,c_16430]) ).
cnf(c_14124,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c8,sk_c8) = sk_c9
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_14054,c_16431]) ).
cnf(c_16432,plain,
( multiply(sk_c5,multiply(sk_c8,sk_c2)) = identity
| multiply(sk_c8,sk_c8) = sk_c9
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_14054,c_9824]) ).
cnf(c_16433,plain,
( multiply(sk_c5,multiply(sk_c8,sk_c1)) = identity
| multiply(sk_c8,sk_c8) = sk_c9
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_14017,c_16432]) ).
cnf(c_14125,plain,
( multiply(sk_c5,multiply(sk_c8,sk_c8)) = identity
| multiply(sk_c8,sk_c8) = sk_c9
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_14054,c_16433]) ).
cnf(c_16434,plain,
( identity = sk_c9
| multiply(sk_c1,sk_c9) = sk_c3
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_14017,c_9546]) ).
cnf(c_16435,plain,
( identity = sk_c9
| multiply(sk_c8,sk_c9) = sk_c3
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_14054,c_16434]) ).
cnf(c_16436,plain,
( identity = sk_c9
| identity = sk_c3
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_13096,c_16435]) ).
cnf(c_14135,plain,
( identity = sk_c9
| identity = sk_c3 ),
inference(copy,[status(thm)],[c_16436]) ).
cnf(c_16437,plain,
( multiply(sk_c9,multiply(sk_c1,sk_c9)) = sk_c8
| inverse(sk_c6) = sk_c9 ),
inference(paramod,[status(thm)],[c_14017,c_7974]) ).
cnf(c_16438,plain,
( multiply(sk_c9,multiply(sk_c8,sk_c9)) = sk_c8
| inverse(sk_c6) = sk_c9 ),
inference(paramod,[status(thm)],[c_14054,c_16437]) ).
cnf(c_16439,plain,
( multiply(sk_c9,identity) = sk_c8
| inverse(sk_c6) = sk_c9 ),
inference(paramod,[status(thm)],[c_13096,c_16438]) ).
cnf(c_16440,plain,
( sk_c9 = sk_c8
| inverse(sk_c6) = sk_c9 ),
inference(paramod,[status(thm)],[c_293,c_16439]) ).
cnf(c_14267,plain,
( sk_c8 = sk_c9
| inverse(sk_c6) = sk_c9 ),
inference(copy,[status(thm)],[c_16440]) ).
cnf(c_14608,plain,
( multiply(inverse(sk_c8),multiply(sk_c9,multiply(sk_c7,A))) = A
| multiply(sk_c8,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_14054,c_10184]) ).
cnf(c_16441,plain,
( multiply(sk_c8,multiply(sk_c9,sk_c3)) = sk_c9
| multiply(sk_c6,sk_c9) = sk_c7 ),
inference(paramod,[status(thm)],[c_14054,c_4444]) ).
cnf(c_14649,plain,
( sk_c3 = sk_c9
| multiply(sk_c6,sk_c9) = sk_c7 ),
inference(paramod,[status(thm)],[c_13097,c_16441]) ).
cnf(c_14697,plain,
( multiply(sk_c9,multiply(sk_c6,sk_c9)) = multiply(sk_c4,multiply(sk_c5,sk_c7))
| multiply(sk_c8,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_14054,c_2892]) ).
cnf(c_14731,plain,
( multiply(inverse(sk_c8),sk_c9) = sk_c8
| multiply(A,multiply(sk_c9,sk_c7)) = multiply(A,sk_c8) ),
inference(paramod,[status(thm)],[c_14054,c_2396]) ).
cnf(c_14733,plain,
( multiply(inverse(sk_c8),multiply(sk_c9,sk_c7)) = identity
| multiply(sk_c8,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_14054,c_2394]) ).
cnf(c_14764,plain,
( multiply(inverse(sk_c8),sk_c9) = sk_c8
| multiply(sk_c5,multiply(sk_c8,A)) = multiply(sk_c9,A) ),
inference(paramod,[status(thm)],[c_14054,c_2128]) ).
cnf(c_14989,plain,
( sk_c8 != sk_c9
| identity = sk_c3 ),
inference(resolve,[status(thm)],[c_14135,c_13071]) ).
cnf(c_16442,plain,
( inverse(sk_c9) = identity
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_14135,c_342]) ).
cnf(c_16443,plain,
( sk_c8 = identity
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_12224,c_16442]) ).
cnf(c_14995,plain,
( identity = sk_c8
| identity = sk_c3 ),
inference(copy,[status(thm)],[c_16443]) ).
cnf(c_16444,plain,
( sk_c8 = sk_c9
| identity = sk_c3
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_14995,c_14135]) ).
cnf(c_15045,plain,
( sk_c8 = sk_c9
| identity = sk_c3 ),
inference(copy,[status(thm)],[c_16444]) ).
cnf(c_16445,plain,
( identity = sk_c3
| identity = sk_c3 ),
inference(resolve,[status(thm)],[c_15045,c_14989]) ).
cnf(c_15048,plain,
identity = sk_c3,
inference(copy,[status(thm)],[c_16445]) ).
cnf(c_15183,plain,
( multiply(inverse(sk_c8),multiply(sk_c9,sk_c7)) = sk_c3
| multiply(sk_c8,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_15048,c_14733]) ).
cnf(c_16446,plain,
( multiply(sk_c5,multiply(sk_c8,sk_c8)) = identity
| multiply(sk_c8,sk_c8) = sk_c9
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_15048,c_14125]) ).
cnf(c_15303,plain,
( multiply(sk_c5,multiply(sk_c8,sk_c8)) = sk_c3
| multiply(sk_c8,sk_c8) = sk_c9
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_15048,c_16446]) ).
cnf(c_15304,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c8,sk_c8) = sk_c9
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_15048,c_14124]) ).
cnf(c_16447,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c8) != sk_c8
| sk_c3 != sk_c3
| inverse(sk_c8) != sk_c9 ),
inference(paramod,[status(thm)],[c_15048,c_13221]) ).
cnf(c_15378,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c8) != sk_c8
| inverse(sk_c8) != sk_c9 ),
inference(copy,[status(thm)],[c_16447]) ).
cnf(c_15414,plain,
multiply(sk_c8,sk_c9) = sk_c3,
inference(paramod,[status(thm)],[c_15048,c_13096]) ).
cnf(c_15418,plain,
( sk_c8 != sk_c9
| sk_c3 != sk_c9 ),
inference(paramod,[status(thm)],[c_15048,c_13071]) ).
cnf(c_15660,plain,
multiply(A,sk_c3) = A,
inference(paramod,[status(thm)],[c_15048,c_293]) ).
cnf(c_16448,plain,
( multiply(sk_c9,multiply(sk_c6,sk_c9)) = sk_c8
| sk_c9 = sk_c8 ),
inference(paramod,[status(thm)],[c_15660,c_4689]) ).
cnf(c_15827,plain,
( multiply(sk_c9,multiply(sk_c6,sk_c9)) = sk_c8
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_16448]) ).
cnf(c_15968,plain,
multiply(inverse(sk_c8),A) = multiply(sk_c9,A),
inference(paramod,[status(thm)],[c_12224,c_292]) ).
cnf(c_15977,plain,
( multiply(sk_c9,multiply(sk_c9,sk_c7)) = sk_c3
| multiply(sk_c8,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_15968,c_15183]) ).
cnf(c_15981,plain,
( multiply(sk_c9,sk_c9) = sk_c8
| multiply(sk_c5,multiply(sk_c8,A)) = multiply(sk_c9,A) ),
inference(paramod,[status(thm)],[c_15968,c_14764]) ).
cnf(c_15984,plain,
( multiply(sk_c9,sk_c9) = sk_c8
| multiply(A,multiply(sk_c9,sk_c7)) = multiply(A,sk_c8) ),
inference(paramod,[status(thm)],[c_15968,c_14731]) ).
cnf(c_15987,plain,
( multiply(sk_c9,multiply(sk_c9,multiply(sk_c7,A))) = A
| multiply(sk_c8,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_15968,c_14608]) ).
cnf(c_16449,plain,
multiply(inverse(sk_c8),sk_c3) = sk_c9,
inference(paramod,[status(thm)],[c_15414,c_81]) ).
cnf(c_16011,plain,
inverse(sk_c8) = sk_c9,
inference(paramod,[status(thm)],[c_15660,c_16449]) ).
cnf(c_16450,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c8) != sk_c8
| sk_c9 != sk_c9 ),
inference(paramod,[status(thm)],[c_16011,c_15378]) ).
cnf(c_16451,plain,
( inverse(sk_c6) = sk_c9
| sk_c9 != sk_c8
| sk_c9 != sk_c9 ),
inference(paramod,[status(thm)],[c_16011,c_16450]) ).
cnf(c_16452,plain,
( inverse(sk_c6) = sk_c9
| sk_c8 != sk_c9
| sk_c9 != sk_c9 ),
inference(copy,[status(thm)],[c_16451]) ).
cnf(c_16035,plain,
( inverse(sk_c6) = sk_c9
| sk_c8 != sk_c9 ),
inference(copy,[status(thm)],[c_16452]) ).
cnf(c_16453,plain,
( inverse(sk_c8) != sk_c8
| sk_c8 != sk_c9
| multiply(sk_c8,sk_c8) != sk_c9
| sk_c9 != sk_c9 ),
inference(paramod,[status(thm)],[c_16011,c_13103]) ).
cnf(c_16454,plain,
( sk_c9 != sk_c8
| sk_c8 != sk_c9
| multiply(sk_c8,sk_c8) != sk_c9
| sk_c9 != sk_c9 ),
inference(paramod,[status(thm)],[c_16011,c_16453]) ).
cnf(c_16455,plain,
( sk_c8 != sk_c9
| sk_c8 != sk_c9
| multiply(sk_c8,sk_c8) != sk_c9
| sk_c9 != sk_c9 ),
inference(copy,[status(thm)],[c_16454]) ).
cnf(c_16456,plain,
( sk_c8 != sk_c9
| sk_c8 != sk_c9
| multiply(sk_c8,sk_c8) != sk_c9 ),
inference(copy,[status(thm)],[c_16455]) ).
cnf(c_16091,plain,
( sk_c8 != sk_c9
| multiply(sk_c8,sk_c8) != sk_c9 ),
inference(copy,[status(thm)],[c_16456]) ).
cnf(c_16100,plain,
multiply(sk_c9,multiply(sk_c8,A)) = A,
inference(paramod,[status(thm)],[c_16011,c_81]) ).
cnf(c_16129,plain,
( multiply(sk_c5,multiply(sk_c4,A)) = A
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_13505,c_81]) ).
cnf(c_16457,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c6) = sk_c9 ),
inference(resolve,[status(thm)],[c_16035,c_14267]) ).
cnf(c_16184,plain,
inverse(sk_c6) = sk_c9,
inference(copy,[status(thm)],[c_16457]) ).
cnf(c_16194,plain,
multiply(sk_c9,multiply(sk_c6,A)) = A,
inference(paramod,[status(thm)],[c_16184,c_81]) ).
cnf(c_16458,plain,
( sk_c9 = sk_c8
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_16194,c_15827]) ).
cnf(c_16459,plain,
( sk_c8 = sk_c9
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_16458]) ).
cnf(c_16196,plain,
sk_c8 = sk_c9,
inference(copy,[status(thm)],[c_16459]) ).
cnf(c_16460,plain,
( multiply(sk_c9,multiply(sk_c6,sk_c9)) = multiply(sk_c4,multiply(sk_c5,sk_c7))
| multiply(sk_c9,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_14697]) ).
cnf(c_16461,plain,
( multiply(sk_c9,multiply(sk_c6,sk_c9)) = multiply(sk_c4,multiply(sk_c5,sk_c7))
| multiply(sk_c9,sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_16460]) ).
cnf(c_16462,plain,
( sk_c9 = multiply(sk_c4,multiply(sk_c5,sk_c7))
| multiply(sk_c9,sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_16194,c_16461]) ).
cnf(c_16198,plain,
( multiply(sk_c4,multiply(sk_c5,sk_c7)) = sk_c9
| multiply(sk_c9,sk_c9) = sk_c9 ),
inference(copy,[status(thm)],[c_16462]) ).
cnf(c_16223,plain,
multiply(sk_c9,multiply(sk_c9,A)) = A,
inference(paramod,[status(thm)],[c_16196,c_16100]) ).
cnf(c_16463,plain,
( sk_c8 != sk_c9
| multiply(sk_c9,sk_c8) != sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_16091]) ).
cnf(c_16464,plain,
( sk_c8 != sk_c9
| multiply(sk_c9,sk_c9) != sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_16463]) ).
cnf(c_16465,plain,
( sk_c9 != sk_c9
| multiply(sk_c9,sk_c9) != sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_16464]) ).
cnf(c_16228,plain,
multiply(sk_c9,sk_c9) != sk_c9,
inference(copy,[status(thm)],[c_16465]) ).
cnf(c_16466,plain,
( multiply(sk_c9,multiply(sk_c9,multiply(sk_c7,A))) = A
| multiply(sk_c9,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_15987]) ).
cnf(c_16467,plain,
( multiply(sk_c9,multiply(sk_c9,multiply(sk_c7,A))) = A
| multiply(sk_c9,sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_16466]) ).
cnf(c_16468,plain,
( multiply(sk_c7,A) = A
| multiply(sk_c9,sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_16223,c_16467]) ).
cnf(c_16233,plain,
multiply(sk_c7,A) = A,
inference(resolve,[status(thm)],[c_16228,c_16468]) ).
cnf(c_16469,plain,
( multiply(sk_c9,sk_c9) = sk_c8
| multiply(A,multiply(sk_c9,sk_c7)) = multiply(A,sk_c9) ),
inference(paramod,[status(thm)],[c_16196,c_15984]) ).
cnf(c_16470,plain,
( multiply(sk_c9,sk_c9) = sk_c9
| multiply(A,multiply(sk_c9,sk_c7)) = multiply(A,sk_c9) ),
inference(paramod,[status(thm)],[c_16196,c_16469]) ).
cnf(c_16236,plain,
multiply(A,multiply(sk_c9,sk_c7)) = multiply(A,sk_c9),
inference(resolve,[status(thm)],[c_16228,c_16470]) ).
cnf(c_16471,plain,
( multiply(sk_c9,sk_c9) = sk_c8
| multiply(sk_c5,multiply(sk_c9,A)) = multiply(sk_c9,A) ),
inference(paramod,[status(thm)],[c_16196,c_15981]) ).
cnf(c_16472,plain,
( multiply(sk_c9,sk_c9) = sk_c9
| multiply(sk_c5,multiply(sk_c9,A)) = multiply(sk_c9,A) ),
inference(paramod,[status(thm)],[c_16196,c_16471]) ).
cnf(c_16238,plain,
multiply(sk_c5,multiply(sk_c9,A)) = multiply(sk_c9,A),
inference(resolve,[status(thm)],[c_16228,c_16472]) ).
cnf(c_16473,plain,
( multiply(sk_c9,multiply(sk_c9,sk_c7)) = sk_c3
| multiply(sk_c9,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_15977]) ).
cnf(c_16474,plain,
( multiply(sk_c9,multiply(sk_c9,sk_c7)) = sk_c3
| multiply(sk_c9,sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_16473]) ).
cnf(c_16475,plain,
( multiply(sk_c9,sk_c9) = sk_c3
| multiply(sk_c9,sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_16236,c_16474]) ).
cnf(c_16242,plain,
multiply(sk_c9,sk_c9) = sk_c3,
inference(resolve,[status(thm)],[c_16228,c_16475]) ).
cnf(c_16476,plain,
( sk_c9 != sk_c9
| sk_c3 != sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_15418]) ).
cnf(c_16254,plain,
sk_c3 != sk_c9,
inference(copy,[status(thm)],[c_16476]) ).
cnf(c_16477,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c9,sk_c8) = sk_c9
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_15304]) ).
cnf(c_16478,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c9,sk_c9) = sk_c9
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_16477]) ).
cnf(c_16479,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| sk_c3 = sk_c9
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_16242,c_16478]) ).
cnf(c_16480,plain,
( multiply(sk_c7,sk_c9) = sk_c6
| sk_c3 = sk_c9
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_16479]) ).
cnf(c_16481,plain,
( sk_c9 = sk_c6
| sk_c3 = sk_c9
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_16233,c_16480]) ).
cnf(c_16482,plain,
( sk_c6 = sk_c9
| sk_c3 = sk_c9
| sk_c3 = sk_c9 ),
inference(copy,[status(thm)],[c_16481]) ).
cnf(c_16483,plain,
( sk_c6 = sk_c9
| sk_c3 = sk_c9 ),
inference(copy,[status(thm)],[c_16482]) ).
cnf(c_16255,plain,
sk_c6 = sk_c9,
inference(resolve,[status(thm)],[c_16254,c_16483]) ).
cnf(c_16484,plain,
( multiply(sk_c5,multiply(sk_c8,sk_c8)) = sk_c3
| multiply(sk_c9,sk_c8) = sk_c9
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_15303]) ).
cnf(c_16485,plain,
( multiply(sk_c5,multiply(sk_c8,sk_c8)) = sk_c3
| multiply(sk_c9,sk_c9) = sk_c9
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_16484]) ).
cnf(c_16486,plain,
( multiply(sk_c5,multiply(sk_c8,sk_c8)) = sk_c3
| sk_c3 = sk_c9
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_16242,c_16485]) ).
cnf(c_16487,plain,
( multiply(sk_c5,multiply(sk_c9,sk_c8)) = sk_c3
| sk_c3 = sk_c9
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_16486]) ).
cnf(c_16488,plain,
( multiply(sk_c5,multiply(sk_c9,sk_c9)) = sk_c3
| sk_c3 = sk_c9
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_16487]) ).
cnf(c_16489,plain,
( multiply(sk_c5,sk_c3) = sk_c3
| sk_c3 = sk_c9
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_16242,c_16488]) ).
cnf(c_16490,plain,
( sk_c5 = sk_c3
| sk_c3 = sk_c9
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_15660,c_16489]) ).
cnf(c_16491,plain,
( sk_c3 = sk_c5
| sk_c3 = sk_c9
| sk_c3 = sk_c9 ),
inference(copy,[status(thm)],[c_16490]) ).
cnf(c_16492,plain,
( sk_c3 = sk_c5
| sk_c3 = sk_c9 ),
inference(copy,[status(thm)],[c_16491]) ).
cnf(c_16256,plain,
sk_c3 = sk_c5,
inference(resolve,[status(thm)],[c_16254,c_16492]) ).
cnf(c_16493,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c8
| multiply(sk_c9,sk_c8) != sk_c9
| sk_c9 != sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_13090]) ).
cnf(c_16494,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c8
| multiply(sk_c9,sk_c9) != sk_c9
| sk_c9 != sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_16493]) ).
cnf(c_16495,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c8
| sk_c3 != sk_c9
| sk_c9 != sk_c9 ),
inference(paramod,[status(thm)],[c_16242,c_16494]) ).
cnf(c_16496,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c8
| sk_c5 != sk_c9
| sk_c9 != sk_c9 ),
inference(paramod,[status(thm)],[c_16256,c_16495]) ).
cnf(c_16497,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| sk_c3 != sk_c8
| sk_c5 != sk_c9
| sk_c9 != sk_c9 ),
inference(paramod,[status(thm)],[c_16242,c_16496]) ).
cnf(c_16498,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| sk_c5 != sk_c8
| sk_c5 != sk_c9
| sk_c9 != sk_c9 ),
inference(paramod,[status(thm)],[c_16256,c_16497]) ).
cnf(c_16499,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| sk_c5 != sk_c9
| sk_c5 != sk_c9
| sk_c9 != sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_16498]) ).
cnf(c_16500,plain,
( sk_c3 != sk_c9
| sk_c5 != sk_c9
| sk_c5 != sk_c9
| sk_c9 != sk_c9 ),
inference(paramod,[status(thm)],[c_16242,c_16499]) ).
cnf(c_16501,plain,
( sk_c5 != sk_c9
| sk_c5 != sk_c9
| sk_c5 != sk_c9
| sk_c9 != sk_c9 ),
inference(paramod,[status(thm)],[c_16256,c_16500]) ).
cnf(c_16502,plain,
( sk_c5 != sk_c9
| sk_c5 != sk_c9
| sk_c5 != sk_c9 ),
inference(copy,[status(thm)],[c_16501]) ).
cnf(c_16503,plain,
( sk_c5 != sk_c9
| sk_c5 != sk_c9 ),
inference(copy,[status(thm)],[c_16502]) ).
cnf(c_16320,plain,
sk_c5 != sk_c9,
inference(copy,[status(thm)],[c_16503]) ).
cnf(c_16504,plain,
( multiply(sk_c8,sk_c8) = sk_c9
| multiply(sk_c9,sk_c9) = sk_c7 ),
inference(paramod,[status(thm)],[c_16255,c_5964]) ).
cnf(c_16505,plain,
( multiply(sk_c8,sk_c8) = sk_c9
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_16242,c_16504]) ).
cnf(c_16506,plain,
( multiply(sk_c8,sk_c8) = sk_c9
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_16256,c_16505]) ).
cnf(c_16507,plain,
( multiply(sk_c9,sk_c8) = sk_c9
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_16196,c_16506]) ).
cnf(c_16508,plain,
( multiply(sk_c9,sk_c9) = sk_c9
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_16196,c_16507]) ).
cnf(c_16509,plain,
( sk_c3 = sk_c9
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_16242,c_16508]) ).
cnf(c_16510,plain,
( sk_c5 = sk_c9
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_16256,c_16509]) ).
cnf(c_16511,plain,
( sk_c5 = sk_c9
| sk_c7 = sk_c5 ),
inference(copy,[status(thm)],[c_16510]) ).
cnf(c_16326,plain,
sk_c7 = sk_c5,
inference(resolve,[status(thm)],[c_16320,c_16511]) ).
cnf(c_16512,plain,
( multiply(A,multiply(sk_c9,sk_c8)) = A
| sk_c5 = sk_c6 ),
inference(paramod,[status(thm)],[c_16326,c_3419]) ).
cnf(c_16513,plain,
( multiply(A,multiply(sk_c9,sk_c8)) = A
| sk_c5 = sk_c9 ),
inference(paramod,[status(thm)],[c_16255,c_16512]) ).
cnf(c_16514,plain,
( multiply(A,multiply(sk_c9,sk_c9)) = A
| sk_c5 = sk_c9 ),
inference(paramod,[status(thm)],[c_16196,c_16513]) ).
cnf(c_16515,plain,
( multiply(A,sk_c3) = A
| sk_c5 = sk_c9 ),
inference(paramod,[status(thm)],[c_16242,c_16514]) ).
cnf(c_16516,plain,
( multiply(A,sk_c5) = A
| sk_c5 = sk_c9 ),
inference(paramod,[status(thm)],[c_16256,c_16515]) ).
cnf(c_16328,plain,
multiply(A,sk_c5) = A,
inference(resolve,[status(thm)],[c_16320,c_16516]) ).
cnf(c_16517,plain,
( multiply(sk_c4,multiply(sk_c5,sk_c7)) = sk_c9
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_16242,c_16198]) ).
cnf(c_16518,plain,
( multiply(sk_c4,multiply(sk_c5,sk_c7)) = sk_c9
| sk_c5 = sk_c9 ),
inference(paramod,[status(thm)],[c_16256,c_16517]) ).
cnf(c_16519,plain,
( multiply(sk_c4,multiply(sk_c5,sk_c5)) = sk_c9
| sk_c5 = sk_c9 ),
inference(paramod,[status(thm)],[c_16326,c_16518]) ).
cnf(c_16520,plain,
( multiply(sk_c4,sk_c5) = sk_c9
| sk_c5 = sk_c9 ),
inference(paramod,[status(thm)],[c_16328,c_16519]) ).
cnf(c_16521,plain,
( sk_c4 = sk_c9
| sk_c5 = sk_c9 ),
inference(paramod,[status(thm)],[c_16328,c_16520]) ).
cnf(c_16332,plain,
sk_c4 = sk_c9,
inference(resolve,[status(thm)],[c_16320,c_16521]) ).
cnf(c_16522,plain,
( multiply(sk_c5,multiply(sk_c4,A)) = A
| sk_c5 = sk_c9 ),
inference(paramod,[status(thm)],[c_16256,c_16129]) ).
cnf(c_16523,plain,
( multiply(sk_c5,multiply(sk_c9,A)) = A
| sk_c5 = sk_c9 ),
inference(paramod,[status(thm)],[c_16332,c_16522]) ).
cnf(c_16524,plain,
( multiply(sk_c9,A) = A
| sk_c5 = sk_c9 ),
inference(paramod,[status(thm)],[c_16238,c_16523]) ).
cnf(c_16334,plain,
multiply(sk_c9,A) = A,
inference(resolve,[status(thm)],[c_16320,c_16524]) ).
cnf(c_16525,plain,
( sk_c3 = sk_c9
| multiply(sk_c9,sk_c9) = sk_c7 ),
inference(paramod,[status(thm)],[c_16255,c_14649]) ).
cnf(c_16526,plain,
( sk_c3 = sk_c9
| sk_c9 = sk_c7 ),
inference(paramod,[status(thm)],[c_16334,c_16525]) ).
cnf(c_16527,plain,
( sk_c3 = sk_c9
| sk_c9 = sk_c5 ),
inference(paramod,[status(thm)],[c_16326,c_16526]) ).
cnf(c_16528,plain,
( sk_c5 = sk_c9
| sk_c9 = sk_c5 ),
inference(paramod,[status(thm)],[c_16256,c_16527]) ).
cnf(c_16529,plain,
( sk_c5 = sk_c9
| sk_c5 = sk_c9 ),
inference(copy,[status(thm)],[c_16528]) ).
cnf(c_16530,plain,
sk_c5 = sk_c9,
inference(copy,[status(thm)],[c_16529]) ).
cnf(c_16335,plain,
$false,
inference(resolve,[status(thm)],[c_16320,c_16530]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP237-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Fri Sep 25 14:39:50 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.03/0.30 % Process 2327874 was started by sandbox2 on n012,
% 0.03/0.30 % Fri Sep 25 14:39:50 2026
% 0.03/0.30 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.03/0.30
% 0.03/0.30 % From the command line: assign(max_seconds, 300).
% 38.13/5.17
% 38.13/5.17 % given #500 (W,wt=11): 10500 sk_c2 = sk_c8 | identity = sk_c8 | identity = sk_c7. [para(10030(b,1),2328(a,1))].
% 38.13/5.17
% 38.13/5.17 % SZS status Unsatisfiable for theBenchmark
% 38.13/5.17
% 38.13/5.17 % Proof 1 at 3.86 (+ 0.91) seconds.
% 38.13/5.17 % Length of proof is 209.
% 38.13/5.17 % Level of proof is 35.
% 38.13/5.17 % Maximum clause weight is 59.000.
% 38.13/5.17 % Given clauses 597.
% 38.13/5.17
% 38.13/5.17 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------