%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP243-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 : n005.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:27 AM UTC 2026
% Result : Unsatisfiable 51.82s 7.02s
% Output : CNFRefutation 51.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 20
% Syntax : Number of formulae : 205 ( 27 unt; 0 def)
% Number of atoms : 696 ( 695 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 886 ( 395 ~; 491 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 157 ( 0 sgn 14 !; 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_2,axiom,
( multiply(sk_c6,sk_c11) = sk_c12
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('theBenchmark.p',prove_this_2) ).
cnf(c_5,plain,
( multiply(sk_c6,sk_c11) = sk_c12
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(clausify,[status(thm)],[prove_this_2]) ).
fof(prove_this_3,axiom,
( inverse(sk_c7) = sk_c11
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('theBenchmark.p',prove_this_3) ).
cnf(c_6,plain,
( inverse(sk_c7) = sk_c11
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(clausify,[status(thm)],[prove_this_3]) ).
fof(prove_this_5,axiom,
( multiply(sk_c8,sk_c9) = sk_c11
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('theBenchmark.p',prove_this_5) ).
cnf(c_8,plain,
( multiply(sk_c8,sk_c9) = sk_c11
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(clausify,[status(thm)],[prove_this_5]) ).
fof(prove_this_6,axiom,
( inverse(sk_c8) = sk_c9
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('theBenchmark.p',prove_this_6) ).
cnf(c_9,plain,
( inverse(sk_c8) = sk_c9
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(clausify,[status(thm)],[prove_this_6]) ).
fof(prove_this_8,axiom,
( inverse(sk_c6) = sk_c12
| inverse(sk_c1) = sk_c12 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_11,plain,
( inverse(sk_c6) = sk_c12
| inverse(sk_c1) = sk_c12 ),
inference(clausify,[status(thm)],[prove_this_8]) ).
fof(prove_this_10,axiom,
( inverse(sk_c7) = sk_c11
| inverse(sk_c1) = sk_c12 ),
file('theBenchmark.p',prove_this_10) ).
cnf(c_13,plain,
( inverse(sk_c7) = sk_c11
| inverse(sk_c1) = sk_c12 ),
inference(clausify,[status(thm)],[prove_this_10]) ).
fof(prove_this_12,axiom,
( multiply(sk_c8,sk_c9) = sk_c11
| inverse(sk_c1) = sk_c12 ),
file('theBenchmark.p',prove_this_12) ).
cnf(c_15,plain,
( multiply(sk_c8,sk_c9) = sk_c11
| inverse(sk_c1) = sk_c12 ),
inference(clausify,[status(thm)],[prove_this_12]) ).
fof(prove_this_13,axiom,
( inverse(sk_c8) = sk_c9
| inverse(sk_c1) = sk_c12 ),
file('theBenchmark.p',prove_this_13) ).
cnf(c_16,plain,
( inverse(sk_c8) = sk_c9
| inverse(sk_c1) = sk_c12 ),
inference(clausify,[status(thm)],[prove_this_13]) ).
fof(prove_this_17,axiom,
( inverse(sk_c7) = sk_c11
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('theBenchmark.p',prove_this_17) ).
cnf(c_20,plain,
( inverse(sk_c7) = sk_c11
| multiply(sk_c2,sk_c11) = sk_c10 ),
inference(clausify,[status(thm)],[prove_this_17]) ).
fof(prove_this_18,axiom,
( multiply(sk_c7,sk_c10) = sk_c11
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('theBenchmark.p',prove_this_18) ).
cnf(c_21,plain,
( multiply(sk_c7,sk_c10) = sk_c11
| multiply(sk_c2,sk_c11) = sk_c10 ),
inference(clausify,[status(thm)],[prove_this_18]) ).
fof(prove_this_24,axiom,
( inverse(sk_c7) = sk_c11
| inverse(sk_c2) = sk_c11 ),
file('theBenchmark.p',prove_this_24) ).
cnf(c_27,plain,
( inverse(sk_c7) = sk_c11
| inverse(sk_c2) = sk_c11 ),
inference(clausify,[status(thm)],[prove_this_24]) ).
fof(prove_this_25,axiom,
( multiply(sk_c7,sk_c10) = sk_c11
| inverse(sk_c2) = sk_c11 ),
file('theBenchmark.p',prove_this_25) ).
cnf(c_28,plain,
( multiply(sk_c7,sk_c10) = sk_c11
| inverse(sk_c2) = sk_c11 ),
inference(clausify,[status(thm)],[prove_this_25]) ).
fof(prove_this_29,axiom,
( inverse(sk_c6) = sk_c12
| inverse(sk_c3) = sk_c12 ),
file('theBenchmark.p',prove_this_29) ).
cnf(c_32,plain,
( inverse(sk_c6) = sk_c12
| inverse(sk_c3) = sk_c12 ),
inference(clausify,[status(thm)],[prove_this_29]) ).
fof(prove_this_30,axiom,
( multiply(sk_c6,sk_c11) = sk_c12
| inverse(sk_c3) = sk_c12 ),
file('theBenchmark.p',prove_this_30) ).
cnf(c_33,plain,
( multiply(sk_c6,sk_c11) = sk_c12
| inverse(sk_c3) = sk_c12 ),
inference(clausify,[status(thm)],[prove_this_30]) ).
fof(prove_this_36,axiom,
( inverse(sk_c6) = sk_c12
| multiply(sk_c3,sk_c11) = sk_c12 ),
file('theBenchmark.p',prove_this_36) ).
cnf(c_39,plain,
( inverse(sk_c6) = sk_c12
| multiply(sk_c3,sk_c11) = sk_c12 ),
inference(clausify,[status(thm)],[prove_this_36]) ).
fof(prove_this_37,axiom,
( multiply(sk_c6,sk_c11) = sk_c12
| multiply(sk_c3,sk_c11) = sk_c12 ),
file('theBenchmark.p',prove_this_37) ).
cnf(c_40,plain,
( multiply(sk_c6,sk_c11) = sk_c12
| multiply(sk_c3,sk_c11) = sk_c12 ),
inference(clausify,[status(thm)],[prove_this_37]) ).
fof(prove_this_64,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_8] :
( multiply(VAR_8,sk_c10) != sk_c11
| inverse(VAR_7) != VAR_8
| multiply(VAR_7,VAR_8) != sk_c11
| multiply(VAR_6,sk_c10) != sk_c11
| inverse(VAR_6) != sk_c11
| multiply(VAR_5,sk_c11) != sk_c12
| inverse(VAR_5) != sk_c12
| multiply(VAR_4,sk_c10) != sk_c11
| inverse(VAR_3) != VAR_4
| multiply(VAR_3,VAR_4) != sk_c11
| multiply(VAR_2,sk_c11) != sk_c12
| inverse(VAR_2) != sk_c12
| inverse(VAR_1) != sk_c11
| multiply(VAR_1,sk_c11) != sk_c10
| inverse(VAR_0) != sk_c12
| multiply(VAR_0,sk_c12) != sk_c11 ),
file('theBenchmark.p',prove_this_64) ).
cnf(c_67,plain,
( multiply(V8,sk_c10) != sk_c11
| inverse(V7) != V8
| multiply(V7,V8) != sk_c11
| multiply(V6,sk_c10) != sk_c11
| inverse(V6) != sk_c11
| multiply(F,sk_c11) != sk_c12
| inverse(F) != sk_c12
| multiply(E,sk_c10) != sk_c11
| inverse(D) != E
| multiply(D,E) != sk_c11
| multiply(C,sk_c11) != sk_c12
| inverse(C) != sk_c12
| inverse(B) != sk_c11
| multiply(B,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(clausify,[status(thm)],[prove_this_64]) ).
cnf(c_69,plain,
( multiply(V7,sk_c10) != sk_c11
| inverse(V6) != V7
| multiply(V6,V7) != sk_c11
| multiply(F,sk_c10) != sk_c11
| inverse(F) != sk_c11
| multiply(E,sk_c11) != sk_c12
| inverse(E) != sk_c12
| multiply(D,sk_c10) != sk_c11
| inverse(C) != D
| multiply(C,D) != sk_c11
| multiply(A,sk_c11) != sk_c12
| inverse(B) != sk_c11
| multiply(B,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(factor,[status(thm)],[c_67]) ).
cnf(c_71,plain,
( multiply(V7,sk_c10) != sk_c11
| inverse(V6) != V7
| multiply(V6,V7) != sk_c11
| multiply(B,sk_c10) != sk_c11
| multiply(F,sk_c11) != sk_c12
| inverse(F) != sk_c12
| multiply(E,sk_c10) != sk_c11
| inverse(D) != E
| multiply(D,E) != sk_c11
| multiply(C,sk_c11) != sk_c12
| inverse(C) != sk_c12
| inverse(B) != sk_c11
| multiply(B,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(factor,[status(thm)],[c_67]) ).
cnf(c_12703,plain,
( multiply(V6,sk_c10) != sk_c11
| inverse(F) != V6
| multiply(F,V6) != sk_c11
| multiply(E,sk_c10) != sk_c11
| inverse(E) != sk_c11
| multiply(A,sk_c11) != sk_c12
| multiply(D,sk_c10) != sk_c11
| inverse(C) != D
| multiply(C,D) != sk_c11
| multiply(A,sk_c11) != sk_c12
| inverse(B) != sk_c11
| multiply(B,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(factor,[status(thm)],[c_69]) ).
cnf(c_77,plain,
( multiply(V6,sk_c10) != sk_c11
| inverse(F) != V6
| multiply(F,V6) != sk_c11
| multiply(E,sk_c10) != sk_c11
| inverse(E) != sk_c11
| multiply(D,sk_c10) != sk_c11
| inverse(C) != D
| multiply(C,D) != sk_c11
| multiply(A,sk_c11) != sk_c12
| inverse(B) != sk_c11
| multiply(B,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(copy,[status(thm)],[c_12703]) ).
cnf(c_12704,plain,
( multiply(V6,sk_c10) != sk_c11
| inverse(F) != V6
| multiply(F,V6) != sk_c11
| multiply(B,sk_c10) != sk_c11
| multiply(C,sk_c11) != sk_c12
| multiply(E,sk_c10) != sk_c11
| inverse(D) != E
| multiply(D,E) != sk_c11
| multiply(C,sk_c11) != sk_c12
| inverse(C) != sk_c12
| inverse(B) != sk_c11
| multiply(B,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(factor,[status(thm)],[c_71]) ).
cnf(c_82,plain,
( multiply(V6,sk_c10) != sk_c11
| inverse(F) != V6
| multiply(F,V6) != sk_c11
| multiply(B,sk_c10) != sk_c11
| multiply(E,sk_c10) != sk_c11
| inverse(D) != E
| multiply(D,E) != sk_c11
| multiply(C,sk_c11) != sk_c12
| inverse(C) != sk_c12
| inverse(B) != sk_c11
| multiply(B,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(copy,[status(thm)],[c_12704]) ).
cnf(c_94,plain,
( multiply(F,sk_c10) != sk_c11
| inverse(E) != F
| multiply(E,F) != sk_c11
| multiply(B,sk_c10) != sk_c11
| multiply(D,sk_c10) != sk_c11
| inverse(C) != D
| multiply(C,D) != sk_c11
| multiply(A,sk_c11) != sk_c12
| inverse(B) != sk_c11
| multiply(B,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(factor,[status(thm)],[c_77]) ).
cnf(c_12705,plain,
( multiply(E,sk_c10) != sk_c11
| inverse(D) != E
| multiply(B,sk_c10) != sk_c11
| multiply(E,sk_c10) != sk_c11
| inverse(D) != E
| multiply(D,E) != sk_c11
| multiply(C,sk_c11) != sk_c12
| inverse(C) != sk_c12
| inverse(B) != sk_c11
| multiply(B,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(factor,[status(thm)],[c_82]) ).
cnf(c_12706,plain,
( multiply(E,sk_c10) != sk_c11
| multiply(B,sk_c10) != sk_c11
| multiply(E,sk_c10) != sk_c11
| inverse(D) != E
| multiply(D,E) != sk_c11
| multiply(C,sk_c11) != sk_c12
| inverse(C) != sk_c12
| inverse(B) != sk_c11
| multiply(B,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(copy,[status(thm)],[c_12705]) ).
cnf(c_103,plain,
( multiply(B,sk_c10) != sk_c11
| multiply(E,sk_c10) != sk_c11
| inverse(D) != E
| multiply(D,E) != sk_c11
| multiply(C,sk_c11) != sk_c12
| inverse(C) != sk_c12
| inverse(B) != sk_c11
| multiply(B,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(copy,[status(thm)],[c_12706]) ).
cnf(c_12707,plain,
( multiply(D,sk_c10) != sk_c11
| inverse(C) != D
| multiply(B,sk_c10) != sk_c11
| multiply(D,sk_c10) != sk_c11
| inverse(C) != D
| multiply(C,D) != sk_c11
| multiply(A,sk_c11) != sk_c12
| inverse(B) != sk_c11
| multiply(B,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(factor,[status(thm)],[c_94]) ).
cnf(c_12708,plain,
( multiply(D,sk_c10) != sk_c11
| multiply(B,sk_c10) != sk_c11
| multiply(D,sk_c10) != sk_c11
| inverse(C) != D
| multiply(C,D) != sk_c11
| multiply(A,sk_c11) != sk_c12
| inverse(B) != sk_c11
| multiply(B,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(copy,[status(thm)],[c_12707]) ).
cnf(c_116,plain,
( multiply(B,sk_c10) != sk_c11
| multiply(D,sk_c10) != sk_c11
| inverse(C) != D
| multiply(C,D) != sk_c11
| multiply(A,sk_c11) != sk_c12
| inverse(B) != sk_c11
| multiply(B,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(copy,[status(thm)],[c_12708]) ).
cnf(c_126,plain,
( multiply(B,sk_c10) != sk_c11
| inverse(D) != B
| multiply(D,B) != sk_c11
| multiply(C,sk_c11) != sk_c12
| inverse(C) != sk_c12
| inverse(B) != sk_c11
| multiply(B,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(factor,[status(thm)],[c_103]) ).
cnf(c_136,plain,
( multiply(B,sk_c10) != sk_c11
| inverse(C) != B
| multiply(C,B) != sk_c11
| multiply(A,sk_c11) != sk_c12
| inverse(B) != sk_c11
| multiply(B,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(factor,[status(thm)],[c_116]) ).
cnf(c_12709,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_12710,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_12709]) ).
cnf(c_144,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_12710]) ).
cnf(c_12711,plain,
( multiply(sk_c11,A) = multiply(sk_c1,multiply(sk_c12,A))
| multiply(sk_c6,sk_c11) = sk_c12 ),
inference(paramod,[status(thm)],[c_5,c_3]) ).
cnf(c_148,plain,
( multiply(sk_c1,multiply(sk_c12,A)) = multiply(sk_c11,A)
| multiply(sk_c6,sk_c11) = sk_c12 ),
inference(copy,[status(thm)],[c_12711]) ).
cnf(c_170,plain,
( multiply(sk_c12,sk_c1) = identity
| inverse(sk_c6) = sk_c12 ),
inference(paramod,[status(thm)],[c_11,c_2]) ).
cnf(c_175,plain,
( multiply(sk_c12,sk_c1) = identity
| inverse(sk_c7) = sk_c11 ),
inference(paramod,[status(thm)],[c_13,c_2]) ).
cnf(c_180,plain,
( multiply(sk_c12,sk_c1) = identity
| multiply(sk_c8,sk_c9) = sk_c11 ),
inference(paramod,[status(thm)],[c_15,c_2]) ).
cnf(c_183,plain,
( multiply(sk_c12,sk_c1) = identity
| inverse(sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_16,c_2]) ).
cnf(c_195,plain,
( multiply(sk_c11,sk_c7) = identity
| multiply(sk_c2,sk_c11) = sk_c10 ),
inference(paramod,[status(thm)],[c_20,c_2]) ).
cnf(c_218,plain,
( multiply(sk_c11,sk_c2) = identity
| inverse(sk_c7) = sk_c11 ),
inference(paramod,[status(thm)],[c_27,c_2]) ).
cnf(c_220,plain,
( multiply(sk_c11,sk_c2) = identity
| multiply(sk_c7,sk_c10) = sk_c11 ),
inference(paramod,[status(thm)],[c_28,c_2]) ).
cnf(c_231,plain,
( multiply(sk_c12,sk_c3) = identity
| inverse(sk_c6) = sk_c12 ),
inference(paramod,[status(thm)],[c_32,c_2]) ).
cnf(c_233,plain,
( multiply(sk_c12,sk_c3) = identity
| multiply(sk_c6,sk_c11) = sk_c12 ),
inference(paramod,[status(thm)],[c_33,c_2]) ).
cnf(c_350,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_144]) ).
cnf(c_387,plain,
( multiply(inverse(sk_c7),sk_c11) = sk_c10
| multiply(sk_c2,sk_c11) = sk_c10 ),
inference(paramod,[status(thm)],[c_21,c_144]) ).
cnf(c_478,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_144,c_144]) ).
cnf(c_479,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_478,c_350]) ).
cnf(c_533,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_479,c_2]) ).
cnf(c_12712,plain,
( multiply(identity,sk_c10) != sk_c11
| multiply(identity,identity) != sk_c11
| multiply(A,sk_c11) != sk_c12
| inverse(identity) != sk_c11
| multiply(identity,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(resolve,[status(thm)],[c_533,c_136]) ).
cnf(c_12713,plain,
( multiply(identity,sk_c10) != sk_c11
| multiply(identity,identity) != sk_c11
| multiply(A,sk_c11) != sk_c12
| inverse(identity) != sk_c11
| sk_c11 != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(paramod,[status(thm)],[c_1,c_12712]) ).
cnf(c_12714,plain,
( multiply(identity,sk_c10) != sk_c11
| multiply(identity,identity) != sk_c11
| multiply(A,sk_c11) != sk_c12
| identity != sk_c11
| sk_c11 != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(paramod,[status(thm)],[c_533,c_12713]) ).
cnf(c_12715,plain,
( multiply(identity,sk_c10) != sk_c11
| identity != sk_c11
| multiply(A,sk_c11) != sk_c12
| identity != sk_c11
| sk_c11 != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(paramod,[status(thm)],[c_479,c_12714]) ).
cnf(c_12716,plain,
( sk_c10 != sk_c11
| identity != sk_c11
| multiply(A,sk_c11) != sk_c12
| identity != sk_c11
| sk_c11 != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(paramod,[status(thm)],[c_1,c_12715]) ).
cnf(c_12717,plain,
( sk_c10 != sk_c11
| identity != sk_c11
| multiply(A,sk_c11) != sk_c12
| identity != sk_c11
| sk_c10 != sk_c11
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(copy,[status(thm)],[c_12716]) ).
cnf(c_12718,plain,
( sk_c10 != sk_c11
| multiply(A,sk_c11) != sk_c12
| identity != sk_c11
| sk_c10 != sk_c11
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(copy,[status(thm)],[c_12717]) ).
cnf(c_589,plain,
( multiply(A,sk_c11) != sk_c12
| identity != sk_c11
| sk_c10 != sk_c11
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(copy,[status(thm)],[c_12718]) ).
cnf(c_12719,plain,
( multiply(identity,sk_c10) != sk_c11
| multiply(identity,identity) != sk_c11
| multiply(B,sk_c11) != sk_c12
| inverse(B) != sk_c12
| inverse(identity) != sk_c11
| multiply(identity,sk_c11) != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(resolve,[status(thm)],[c_533,c_126]) ).
cnf(c_12720,plain,
( multiply(identity,sk_c10) != sk_c11
| multiply(identity,identity) != sk_c11
| multiply(B,sk_c11) != sk_c12
| inverse(B) != sk_c12
| inverse(identity) != sk_c11
| sk_c11 != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(paramod,[status(thm)],[c_1,c_12719]) ).
cnf(c_12721,plain,
( multiply(identity,sk_c10) != sk_c11
| multiply(identity,identity) != sk_c11
| multiply(B,sk_c11) != sk_c12
| inverse(B) != sk_c12
| identity != sk_c11
| sk_c11 != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(paramod,[status(thm)],[c_533,c_12720]) ).
cnf(c_12722,plain,
( multiply(identity,sk_c10) != sk_c11
| identity != sk_c11
| multiply(B,sk_c11) != sk_c12
| inverse(B) != sk_c12
| identity != sk_c11
| sk_c11 != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(paramod,[status(thm)],[c_479,c_12721]) ).
cnf(c_12723,plain,
( sk_c10 != sk_c11
| identity != sk_c11
| multiply(B,sk_c11) != sk_c12
| inverse(B) != sk_c12
| identity != sk_c11
| sk_c11 != sk_c10
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(paramod,[status(thm)],[c_1,c_12722]) ).
cnf(c_12724,plain,
( sk_c10 != sk_c11
| identity != sk_c11
| multiply(B,sk_c11) != sk_c12
| inverse(B) != sk_c12
| identity != sk_c11
| sk_c10 != sk_c11
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(copy,[status(thm)],[c_12723]) ).
cnf(c_12725,plain,
( sk_c10 != sk_c11
| multiply(B,sk_c11) != sk_c12
| inverse(B) != sk_c12
| identity != sk_c11
| sk_c10 != sk_c11
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(copy,[status(thm)],[c_12724]) ).
cnf(c_590,plain,
( multiply(B,sk_c11) != sk_c12
| inverse(B) != sk_c12
| identity != sk_c11
| sk_c10 != sk_c11
| inverse(A) != sk_c12
| multiply(A,sk_c12) != sk_c11 ),
inference(copy,[status(thm)],[c_12725]) ).
cnf(c_12726,plain,
( multiply(inverse(sk_c12),identity) = sk_c1
| inverse(sk_c6) = sk_c12 ),
inference(paramod,[status(thm)],[c_170,c_144]) ).
cnf(c_594,plain,
( inverse(sk_c12) = sk_c1
| inverse(sk_c6) = sk_c12 ),
inference(paramod,[status(thm)],[c_479,c_12726]) ).
cnf(c_12727,plain,
( multiply(inverse(sk_c12),sk_c11) != sk_c12
| identity != sk_c11
| sk_c10 != sk_c11
| inverse(inverse(sk_c12)) != sk_c12
| identity != sk_c11 ),
inference(paramod,[status(thm)],[c_2,c_589]) ).
cnf(c_664,plain,
( multiply(inverse(sk_c12),sk_c11) != sk_c12
| sk_c10 != sk_c11
| inverse(inverse(sk_c12)) != sk_c12
| identity != sk_c11 ),
inference(copy,[status(thm)],[c_12727]) ).
cnf(c_707,plain,
( multiply(sk_c1,sk_c11) != sk_c12
| sk_c10 != sk_c11
| inverse(inverse(sk_c12)) != sk_c12
| identity != sk_c11
| inverse(sk_c6) = sk_c12 ),
inference(paramod,[status(thm)],[c_594,c_664]) ).
cnf(c_12728,plain,
( multiply(inverse(sk_c12),identity) = sk_c1
| inverse(sk_c7) = sk_c11 ),
inference(paramod,[status(thm)],[c_175,c_144]) ).
cnf(c_720,plain,
( inverse(sk_c12) = sk_c1
| inverse(sk_c7) = sk_c11 ),
inference(paramod,[status(thm)],[c_479,c_12728]) ).
cnf(c_723,plain,
( multiply(sk_c1,sk_c12) = identity
| inverse(sk_c7) = sk_c11 ),
inference(paramod,[status(thm)],[c_720,c_2]) ).
cnf(c_12729,plain,
( multiply(A,sk_c11) != sk_c12
| inverse(A) != sk_c12
| identity != sk_c11
| sk_c10 != sk_c11
| inverse(inverse(sk_c12)) != sk_c12
| identity != sk_c11 ),
inference(paramod,[status(thm)],[c_2,c_590]) ).
cnf(c_852,plain,
( multiply(A,sk_c11) != sk_c12
| inverse(A) != sk_c12
| sk_c10 != sk_c11
| inverse(inverse(sk_c12)) != sk_c12
| identity != sk_c11 ),
inference(copy,[status(thm)],[c_12729]) ).
cnf(c_12730,plain,
( multiply(inverse(sk_c12),identity) = sk_c1
| inverse(sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_183,c_144]) ).
cnf(c_860,plain,
( inverse(sk_c12) = sk_c1
| inverse(sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_479,c_12730]) ).
cnf(c_864,plain,
( multiply(sk_c1,sk_c12) = identity
| inverse(sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_860,c_2]) ).
cnf(c_12731,plain,
( multiply(inverse(sk_c11),identity) = sk_c2
| inverse(sk_c7) = sk_c11 ),
inference(paramod,[status(thm)],[c_218,c_144]) ).
cnf(c_1080,plain,
( inverse(sk_c11) = sk_c2
| inverse(sk_c7) = sk_c11 ),
inference(paramod,[status(thm)],[c_479,c_12731]) ).
cnf(c_12732,plain,
( multiply(inverse(sk_c12),identity) = sk_c3
| inverse(sk_c6) = sk_c12 ),
inference(paramod,[status(thm)],[c_231,c_144]) ).
cnf(c_1169,plain,
( inverse(sk_c12) = sk_c3
| inverse(sk_c6) = sk_c12 ),
inference(paramod,[status(thm)],[c_479,c_12732]) ).
cnf(c_12733,plain,
( sk_c3 = sk_c1
| inverse(sk_c6) = sk_c12
| inverse(sk_c6) = sk_c12 ),
inference(paramod,[status(thm)],[c_1169,c_594]) ).
cnf(c_1181,plain,
( sk_c3 = sk_c1
| inverse(sk_c6) = sk_c12 ),
inference(copy,[status(thm)],[c_12733]) ).
cnf(c_12734,plain,
( inverse(sk_c6) = sk_c12
| multiply(sk_c1,sk_c11) = sk_c12
| inverse(sk_c6) = sk_c12 ),
inference(paramod,[status(thm)],[c_1181,c_39]) ).
cnf(c_1195,plain,
( multiply(sk_c1,sk_c11) = sk_c12
| inverse(sk_c6) = sk_c12 ),
inference(copy,[status(thm)],[c_12734]) ).
cnf(c_12735,plain,
( inverse(sk_c7) = sk_c11
| identity = sk_c11
| inverse(sk_c7) = sk_c11 ),
inference(paramod,[status(thm)],[c_723,c_6]) ).
cnf(c_2238,plain,
( identity = sk_c11
| inverse(sk_c7) = sk_c11 ),
inference(copy,[status(thm)],[c_12735]) ).
cnf(c_2258,plain,
( inverse(sk_c11) = identity
| inverse(sk_c7) = sk_c11 ),
inference(paramod,[status(thm)],[c_2238,c_533]) ).
cnf(c_12736,plain,
( identity = sk_c2
| inverse(sk_c7) = sk_c11
| inverse(sk_c7) = sk_c11 ),
inference(paramod,[status(thm)],[c_2258,c_1080]) ).
cnf(c_2363,plain,
( identity = sk_c2
| inverse(sk_c7) = sk_c11 ),
inference(copy,[status(thm)],[c_12736]) ).
cnf(c_12737,plain,
( sk_c2 = sk_c11
| inverse(sk_c7) = sk_c11
| inverse(sk_c7) = sk_c11 ),
inference(paramod,[status(thm)],[c_2363,c_2238]) ).
cnf(c_2382,plain,
( sk_c2 = sk_c11
| inverse(sk_c7) = sk_c11 ),
inference(copy,[status(thm)],[c_12737]) ).
cnf(c_12738,plain,
( multiply(inverse(sk_c11),identity) = sk_c7
| multiply(sk_c2,sk_c11) = sk_c10 ),
inference(paramod,[status(thm)],[c_195,c_144]) ).
cnf(c_2678,plain,
( inverse(sk_c11) = sk_c7
| multiply(sk_c2,sk_c11) = sk_c10 ),
inference(paramod,[status(thm)],[c_479,c_12738]) ).
cnf(c_12739,plain,
( inverse(sk_c8) = sk_c9
| identity = sk_c11
| inverse(sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_864,c_9]) ).
cnf(c_2820,plain,
( identity = sk_c11
| inverse(sk_c8) = sk_c9 ),
inference(copy,[status(thm)],[c_12739]) ).
cnf(c_2841,plain,
( multiply(sk_c9,sk_c8) = identity
| identity = sk_c11 ),
inference(paramod,[status(thm)],[c_2820,c_2]) ).
cnf(c_12740,plain,
( multiply(inverse(sk_c9),identity) = sk_c8
| identity = sk_c11 ),
inference(paramod,[status(thm)],[c_2841,c_144]) ).
cnf(c_2871,plain,
( inverse(sk_c9) = sk_c8
| identity = sk_c11 ),
inference(paramod,[status(thm)],[c_479,c_12740]) ).
cnf(c_2931,plain,
( multiply(sk_c8,sk_c9) = identity
| identity = sk_c11 ),
inference(paramod,[status(thm)],[c_2871,c_2]) ).
cnf(c_12741,plain,
( identity = sk_c11
| multiply(sk_c1,sk_c12) = sk_c11
| identity = sk_c11 ),
inference(paramod,[status(thm)],[c_2931,c_8]) ).
cnf(c_3010,plain,
( multiply(sk_c1,sk_c12) = sk_c11
| identity = sk_c11 ),
inference(copy,[status(thm)],[c_12741]) ).
cnf(c_12742,plain,
( multiply(sk_c12,sk_c1) = identity
| identity = sk_c11
| identity = sk_c11 ),
inference(paramod,[status(thm)],[c_2931,c_180]) ).
cnf(c_3035,plain,
( multiply(sk_c12,sk_c1) = identity
| identity = sk_c11 ),
inference(copy,[status(thm)],[c_12742]) ).
cnf(c_12743,plain,
( multiply(inverse(sk_c12),identity) = sk_c1
| identity = sk_c11 ),
inference(paramod,[status(thm)],[c_3035,c_144]) ).
cnf(c_3590,plain,
( inverse(sk_c12) = sk_c1
| identity = sk_c11 ),
inference(paramod,[status(thm)],[c_479,c_12743]) ).
cnf(c_3623,plain,
( multiply(sk_c1,sk_c12) = identity
| identity = sk_c11 ),
inference(paramod,[status(thm)],[c_3590,c_2]) ).
cnf(c_4817,plain,
( multiply(inverse(sk_c7),sk_c11) = sk_c10
| multiply(sk_c11,sk_c2) = identity ),
inference(paramod,[status(thm)],[c_220,c_144]) ).
cnf(c_12744,plain,
( multiply(inverse(sk_c12),identity) = sk_c3
| multiply(sk_c6,sk_c11) = sk_c12 ),
inference(paramod,[status(thm)],[c_233,c_144]) ).
cnf(c_5530,plain,
( inverse(sk_c12) = sk_c3
| multiply(sk_c6,sk_c11) = sk_c12 ),
inference(paramod,[status(thm)],[c_479,c_12744]) ).
cnf(c_12745,plain,
( multiply(sk_c1,identity) = multiply(sk_c11,sk_c3)
| multiply(sk_c6,sk_c11) = sk_c12
| multiply(sk_c6,sk_c11) = sk_c12 ),
inference(paramod,[status(thm)],[c_233,c_148]) ).
cnf(c_12746,plain,
( sk_c1 = multiply(sk_c11,sk_c3)
| multiply(sk_c6,sk_c11) = sk_c12
| multiply(sk_c6,sk_c11) = sk_c12 ),
inference(paramod,[status(thm)],[c_479,c_12745]) ).
cnf(c_12747,plain,
( multiply(sk_c11,sk_c3) = sk_c1
| multiply(sk_c6,sk_c11) = sk_c12
| multiply(sk_c6,sk_c11) = sk_c12 ),
inference(copy,[status(thm)],[c_12746]) ).
cnf(c_5531,plain,
( multiply(sk_c11,sk_c3) = sk_c1
| multiply(sk_c6,sk_c11) = sk_c12 ),
inference(copy,[status(thm)],[c_12747]) ).
cnf(c_12748,plain,
( identity = sk_c11
| identity = sk_c11
| identity = sk_c11 ),
inference(paramod,[status(thm)],[c_3623,c_3010]) ).
cnf(c_12749,plain,
( identity = sk_c11
| identity = sk_c11 ),
inference(copy,[status(thm)],[c_12748]) ).
cnf(c_5928,plain,
identity = sk_c11,
inference(copy,[status(thm)],[c_12749]) ).
cnf(c_6156,plain,
( multiply(inverse(sk_c7),sk_c11) = sk_c10
| multiply(sk_c11,sk_c2) = sk_c11 ),
inference(paramod,[status(thm)],[c_5928,c_4817]) ).
cnf(c_12750,plain,
( multiply(A,sk_c11) != sk_c12
| inverse(A) != sk_c12
| sk_c10 != sk_c11
| inverse(inverse(sk_c12)) != sk_c12
| sk_c11 != sk_c11 ),
inference(paramod,[status(thm)],[c_5928,c_852]) ).
cnf(c_7193,plain,
( multiply(A,sk_c11) != sk_c12
| inverse(A) != sk_c12
| sk_c10 != sk_c11
| inverse(inverse(sk_c12)) != sk_c12 ),
inference(copy,[status(thm)],[c_12750]) ).
cnf(c_12751,plain,
( multiply(sk_c1,sk_c11) != sk_c12
| sk_c10 != sk_c11
| inverse(inverse(sk_c12)) != sk_c12
| sk_c11 != sk_c11
| inverse(sk_c6) = sk_c12 ),
inference(paramod,[status(thm)],[c_5928,c_707]) ).
cnf(c_7304,plain,
( multiply(sk_c1,sk_c11) != sk_c12
| sk_c10 != sk_c11
| inverse(inverse(sk_c12)) != sk_c12
| inverse(sk_c6) = sk_c12 ),
inference(copy,[status(thm)],[c_12751]) ).
cnf(c_12752,plain,
inverse(sk_c11) = identity,
inference(paramod,[status(thm)],[c_5928,c_533]) ).
cnf(c_7437,plain,
inverse(sk_c11) = sk_c11,
inference(paramod,[status(thm)],[c_5928,c_12752]) ).
cnf(c_7441,plain,
multiply(A,sk_c11) = A,
inference(paramod,[status(thm)],[c_5928,c_479]) ).
cnf(c_7469,plain,
multiply(sk_c11,A) = A,
inference(paramod,[status(thm)],[c_5928,c_1]) ).
cnf(c_12753,plain,
( multiply(inverse(sk_c12),sk_c11) != sk_c12
| sk_c10 != sk_c11
| inverse(inverse(sk_c12)) != sk_c12 ),
inference(factor,[status(thm)],[c_7193]) ).
cnf(c_7515,plain,
( inverse(sk_c12) != sk_c12
| sk_c10 != sk_c11
| inverse(inverse(sk_c12)) != sk_c12 ),
inference(paramod,[status(thm)],[c_7441,c_12753]) ).
cnf(c_12754,plain,
( inverse(sk_c11) = sk_c7
| sk_c2 = sk_c10 ),
inference(paramod,[status(thm)],[c_7441,c_2678]) ).
cnf(c_12755,plain,
( sk_c11 = sk_c7
| sk_c2 = sk_c10 ),
inference(paramod,[status(thm)],[c_7437,c_12754]) ).
cnf(c_7587,plain,
( sk_c7 = sk_c11
| sk_c2 = sk_c10 ),
inference(copy,[status(thm)],[c_12755]) ).
cnf(c_7689,plain,
( sk_c1 != sk_c12
| sk_c10 != sk_c11
| inverse(inverse(sk_c12)) != sk_c12
| inverse(sk_c6) = sk_c12 ),
inference(paramod,[status(thm)],[c_7441,c_7304]) ).
cnf(c_12756,plain,
( multiply(inverse(sk_c7),sk_c11) = sk_c10
| sk_c2 = sk_c11 ),
inference(paramod,[status(thm)],[c_7469,c_6156]) ).
cnf(c_8178,plain,
( inverse(sk_c7) = sk_c10
| sk_c2 = sk_c11 ),
inference(paramod,[status(thm)],[c_7441,c_12756]) ).
cnf(c_12757,plain,
( multiply(sk_c11,sk_c3) = sk_c1
| sk_c6 = sk_c12 ),
inference(paramod,[status(thm)],[c_7441,c_5531]) ).
cnf(c_8221,plain,
( sk_c3 = sk_c1
| sk_c6 = sk_c12 ),
inference(paramod,[status(thm)],[c_7469,c_12757]) ).
cnf(c_8222,plain,
( inverse(sk_c12) = sk_c3
| sk_c6 = sk_c12 ),
inference(paramod,[status(thm)],[c_7441,c_5530]) ).
cnf(c_8515,plain,
( sk_c1 = sk_c12
| inverse(sk_c6) = sk_c12 ),
inference(paramod,[status(thm)],[c_7441,c_1195]) ).
cnf(c_12758,plain,
( multiply(inverse(sk_c7),sk_c11) = sk_c10
| sk_c2 = sk_c10 ),
inference(paramod,[status(thm)],[c_7441,c_387]) ).
cnf(c_8565,plain,
( inverse(sk_c7) = sk_c10
| sk_c2 = sk_c10 ),
inference(paramod,[status(thm)],[c_7441,c_12758]) ).
cnf(c_12759,plain,
( multiply(sk_c6,sk_c11) = sk_c12
| sk_c3 = sk_c12 ),
inference(paramod,[status(thm)],[c_7441,c_40]) ).
cnf(c_8658,plain,
( sk_c6 = sk_c12
| sk_c3 = sk_c12 ),
inference(paramod,[status(thm)],[c_7441,c_12759]) ).
cnf(c_12760,plain,
( sk_c12 = sk_c1
| sk_c6 = sk_c12
| sk_c6 = sk_c12 ),
inference(paramod,[status(thm)],[c_8658,c_8221]) ).
cnf(c_12761,plain,
( sk_c1 = sk_c12
| sk_c6 = sk_c12
| sk_c6 = sk_c12 ),
inference(copy,[status(thm)],[c_12760]) ).
cnf(c_9229,plain,
( sk_c1 = sk_c12
| sk_c6 = sk_c12 ),
inference(copy,[status(thm)],[c_12761]) ).
cnf(c_12762,plain,
( sk_c2 = sk_c11
| sk_c10 = sk_c11
| sk_c2 = sk_c11 ),
inference(paramod,[status(thm)],[c_8178,c_2382]) ).
cnf(c_9770,plain,
( sk_c10 = sk_c11
| sk_c2 = sk_c11 ),
inference(copy,[status(thm)],[c_12762]) ).
cnf(c_12763,plain,
( inverse(sk_c12) = sk_c12
| sk_c6 = sk_c12
| sk_c6 = sk_c12 ),
inference(paramod,[status(thm)],[c_8658,c_8222]) ).
cnf(c_9924,plain,
( inverse(sk_c12) = sk_c12
| sk_c6 = sk_c12 ),
inference(copy,[status(thm)],[c_12763]) ).
cnf(c_12764,plain,
( sk_c1 = sk_c12
| inverse(sk_c12) = sk_c12
| sk_c1 = sk_c12 ),
inference(paramod,[status(thm)],[c_9229,c_8515]) ).
cnf(c_10291,plain,
( inverse(sk_c12) = sk_c12
| sk_c1 = sk_c12 ),
inference(copy,[status(thm)],[c_12764]) ).
cnf(c_12765,plain,
( inverse(sk_c11) = sk_c10
| sk_c2 = sk_c10
| sk_c2 = sk_c10 ),
inference(paramod,[status(thm)],[c_7587,c_8565]) ).
cnf(c_12766,plain,
( sk_c11 = sk_c10
| sk_c2 = sk_c10
| sk_c2 = sk_c10 ),
inference(paramod,[status(thm)],[c_7437,c_12765]) ).
cnf(c_12767,plain,
( sk_c10 = sk_c11
| sk_c2 = sk_c10
| sk_c2 = sk_c10 ),
inference(copy,[status(thm)],[c_12766]) ).
cnf(c_10610,plain,
( sk_c10 = sk_c11
| sk_c2 = sk_c10 ),
inference(copy,[status(thm)],[c_12767]) ).
cnf(c_12768,plain,
( sk_c10 = sk_c11
| sk_c10 = sk_c11
| sk_c10 = sk_c11 ),
inference(paramod,[status(thm)],[c_10610,c_9770]) ).
cnf(c_12769,plain,
( sk_c10 = sk_c11
| sk_c10 = sk_c11 ),
inference(copy,[status(thm)],[c_12768]) ).
cnf(c_10640,plain,
sk_c10 = sk_c11,
inference(copy,[status(thm)],[c_12769]) ).
cnf(c_12770,plain,
( sk_c1 != sk_c12
| sk_c11 != sk_c11
| inverse(inverse(sk_c12)) != sk_c12
| inverse(sk_c6) = sk_c12 ),
inference(paramod,[status(thm)],[c_10640,c_7689]) ).
cnf(c_11684,plain,
( sk_c1 != sk_c12
| inverse(inverse(sk_c12)) != sk_c12
| inverse(sk_c6) = sk_c12 ),
inference(copy,[status(thm)],[c_12770]) ).
cnf(c_12771,plain,
( inverse(sk_c12) != sk_c12
| sk_c11 != sk_c11
| inverse(inverse(sk_c12)) != sk_c12 ),
inference(paramod,[status(thm)],[c_10640,c_7515]) ).
cnf(c_11709,plain,
( inverse(sk_c12) != sk_c12
| inverse(inverse(sk_c12)) != sk_c12 ),
inference(copy,[status(thm)],[c_12771]) ).
cnf(c_12172,plain,
( inverse(inverse(sk_c12)) != sk_c12
| sk_c6 = sk_c12 ),
inference(resolve,[status(thm)],[c_9924,c_11709]) ).
cnf(c_12243,plain,
( inverse(inverse(sk_c12)) != sk_c12
| sk_c1 = sk_c12 ),
inference(resolve,[status(thm)],[c_10291,c_11709]) ).
cnf(c_12772,plain,
multiply(A,sk_c11) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_478,c_7441]) ).
cnf(c_12773,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_7441,c_12772]) ).
cnf(c_12616,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_12773]) ).
cnf(c_12774,plain,
( sk_c12 != sk_c12
| sk_c1 = sk_c12 ),
inference(paramod,[status(thm)],[c_12616,c_12243]) ).
cnf(c_12676,plain,
sk_c1 = sk_c12,
inference(copy,[status(thm)],[c_12774]) ).
cnf(c_12775,plain,
( sk_c12 != sk_c12
| sk_c6 = sk_c12 ),
inference(paramod,[status(thm)],[c_12616,c_12172]) ).
cnf(c_12681,plain,
sk_c6 = sk_c12,
inference(copy,[status(thm)],[c_12775]) ).
cnf(c_12776,plain,
( inverse(sk_c12) != sk_c12
| sk_c12 != sk_c12 ),
inference(paramod,[status(thm)],[c_12616,c_11709]) ).
cnf(c_12701,plain,
inverse(sk_c12) != sk_c12,
inference(copy,[status(thm)],[c_12776]) ).
cnf(c_12777,plain,
( sk_c1 != sk_c12
| inverse(inverse(sk_c12)) != sk_c12
| inverse(sk_c12) = sk_c12 ),
inference(paramod,[status(thm)],[c_12681,c_11684]) ).
cnf(c_12778,plain,
( sk_c1 != sk_c12
| sk_c12 != sk_c12
| inverse(sk_c12) = sk_c12 ),
inference(paramod,[status(thm)],[c_12616,c_12777]) ).
cnf(c_12779,plain,
( sk_c12 != sk_c12
| sk_c12 != sk_c12
| inverse(sk_c12) = sk_c12 ),
inference(paramod,[status(thm)],[c_12676,c_12778]) ).
cnf(c_12780,plain,
( sk_c12 != sk_c12
| inverse(sk_c12) = sk_c12 ),
inference(copy,[status(thm)],[c_12779]) ).
cnf(c_12781,plain,
inverse(sk_c12) = sk_c12,
inference(copy,[status(thm)],[c_12780]) ).
cnf(c_12702,plain,
$false,
inference(resolve,[status(thm)],[c_12701,c_12781]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP243-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.10/0.35 % Computer : n005.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Fri Sep 25 14:40:32 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 3715823 was started by sandbox2 on n005,
% 0.10/0.36 % Fri Sep 25 14:40:32 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.14/0.36
% 0.14/0.36 % From the command line: assign(max_seconds, 300).
% 51.82/7.02
% 51.82/7.02 % given #500 (A,wt=19): 409 inverse(sk_c3) = sk_c12 | multiply(sk_c12,multiply(sk_c6,A)) = A. [para(32(b,1),144(a,1,1))].
% 51.82/7.02
% 51.82/7.02 % SZS status Unsatisfiable for theBenchmark
% 51.82/7.02
% 51.82/7.02 % Proof 1 at 5.12 (+ 1.48) seconds.
% 51.82/7.02 % Length of proof is 106.
% 51.82/7.02 % Level of proof is 21.
% 51.82/7.02 % Maximum clause weight is 77.000.
% 51.82/7.02 % Given clauses 579.
% 51.82/7.02
% 51.82/7.02 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------