%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP223-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:24 AM UTC 2026
% Result : Unsatisfiable 75.52s 18.09s
% Output : CNFRefutation 75.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 91
% Number of leaves : 22
% Syntax : Number of formulae : 243 ( 25 unt; 0 def)
% Number of atoms : 674 ( 673 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 636 ( 205 ~; 431 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 3 avg)
% Maximal term depth : 3 ( 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 : 88 ( 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_c1) = sk_c9 ),
file('theBenchmark.p',prove_this_1) ).
cnf(c_4,plain,
( multiply(sk_c4,sk_c5) = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_1]) ).
fof(prove_this_2,axiom,
( inverse(sk_c4) = sk_c5
| inverse(sk_c1) = sk_c9 ),
file('theBenchmark.p',prove_this_2) ).
cnf(c_5,plain,
( inverse(sk_c4) = sk_c5
| inverse(sk_c1) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_2]) ).
fof(prove_this_4,axiom,
( multiply(sk_c9,sk_c7) = sk_c8
| inverse(sk_c1) = sk_c9 ),
file('theBenchmark.p',prove_this_4) ).
cnf(c_7,plain,
( multiply(sk_c9,sk_c7) = sk_c8
| inverse(sk_c1) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_4]) ).
fof(prove_this_5,axiom,
( multiply(sk_c6,sk_c9) = sk_c7
| inverse(sk_c1) = sk_c9 ),
file('theBenchmark.p',prove_this_5) ).
cnf(c_8,plain,
( multiply(sk_c6,sk_c9) = sk_c7
| inverse(sk_c1) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_5]) ).
fof(prove_this_6,axiom,
( inverse(sk_c6) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('theBenchmark.p',prove_this_6) ).
cnf(c_9,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_6]) ).
fof(prove_this_7,axiom,
( multiply(sk_c4,sk_c5) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_7) ).
cnf(c_10,plain,
( multiply(sk_c4,sk_c5) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_7]) ).
fof(prove_this_8,axiom,
( inverse(sk_c4) = sk_c5
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_11,plain,
( inverse(sk_c4) = sk_c5
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_8]) ).
fof(prove_this_9,axiom,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_9) ).
cnf(c_12,plain,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_9]) ).
fof(prove_this_12,axiom,
( inverse(sk_c6) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_12) ).
cnf(c_15,plain,
( inverse(sk_c6) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_12]) ).
fof(prove_this_16,axiom,
( multiply(sk_c9,sk_c7) = sk_c8
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('theBenchmark.p',prove_this_16) ).
cnf(c_19,plain,
( multiply(sk_c9,sk_c7) = sk_c8
| multiply(sk_c9,sk_c3) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_16]) ).
fof(prove_this_17,axiom,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('theBenchmark.p',prove_this_17) ).
cnf(c_20,plain,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c9,sk_c3) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_17]) ).
fof(prove_this_18,axiom,
( inverse(sk_c6) = sk_c9
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('theBenchmark.p',prove_this_18) ).
cnf(c_21,plain,
( inverse(sk_c6) = sk_c9
| multiply(sk_c9,sk_c3) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_18]) ).
fof(prove_this_22,axiom,
( multiply(sk_c9,sk_c7) = sk_c8
| multiply(sk_c2,sk_c9) = sk_c3 ),
file('theBenchmark.p',prove_this_22) ).
cnf(c_25,plain,
( multiply(sk_c9,sk_c7) = sk_c8
| multiply(sk_c2,sk_c9) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_22]) ).
fof(prove_this_23,axiom,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c2,sk_c9) = sk_c3 ),
file('theBenchmark.p',prove_this_23) ).
cnf(c_26,plain,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c2,sk_c9) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_23]) ).
fof(prove_this_24,axiom,
( inverse(sk_c6) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c3 ),
file('theBenchmark.p',prove_this_24) ).
cnf(c_27,plain,
( inverse(sk_c6) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_24]) ).
fof(prove_this_28,axiom,
( multiply(sk_c9,sk_c7) = sk_c8
| inverse(sk_c2) = sk_c9 ),
file('theBenchmark.p',prove_this_28) ).
cnf(c_31,plain,
( multiply(sk_c9,sk_c7) = sk_c8
| inverse(sk_c2) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_28]) ).
fof(prove_this_29,axiom,
( multiply(sk_c6,sk_c9) = sk_c7
| inverse(sk_c2) = sk_c9 ),
file('theBenchmark.p',prove_this_29) ).
cnf(c_32,plain,
( multiply(sk_c6,sk_c9) = sk_c7
| inverse(sk_c2) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_29]) ).
fof(prove_this_30,axiom,
( inverse(sk_c6) = sk_c9
| inverse(sk_c2) = sk_c9 ),
file('theBenchmark.p',prove_this_30) ).
cnf(c_33,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c2) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_30]) ).
fof(prove_this_31,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 ),
file('theBenchmark.p',prove_this_31) ).
cnf(c_34,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 ),
inference(clausify,[status(thm)],[prove_this_31]) ).
cnf(c_35,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 ),
inference(factor,[status(thm)],[c_34]) ).
cnf(c_12211,plain,
( inverse(C) != sk_c9
| multiply(sk_c9,B) != 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 ),
inference(factor,[status(thm)],[c_34]) ).
cnf(c_12212,plain,
( inverse(C) != sk_c9
| 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 ),
inference(copy,[status(thm)],[c_12211]) ).
cnf(c_41,plain,
( 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 ),
inference(copy,[status(thm)],[c_12212]) ).
cnf(c_12213,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 ),
inference(factor,[status(thm)],[c_35]) ).
cnf(c_44,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 ),
inference(copy,[status(thm)],[c_12213]) ).
cnf(c_12214,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 ),
inference(factor,[status(thm)],[c_44]) ).
cnf(c_12215,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 ),
inference(copy,[status(thm)],[c_12214]) ).
cnf(c_55,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 ),
inference(copy,[status(thm)],[c_12215]) ).
cnf(c_66,plain,
multiply(multiply(A,identity),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_1,c_3]) ).
cnf(c_12216,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_68,plain,
multiply(inverse(A),multiply(A,B)) = multiply(identity,B),
inference(copy,[status(thm)],[c_12216]) ).
cnf(c_83,plain,
( multiply(sk_c9,sk_c6) = identity
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_9,c_2]) ).
cnf(c_177,plain,
( multiply(D,sk_c8) != sk_c9
| inverse(C) != D
| multiply(C,D) != sk_c9
| inverse(identity) != sk_c9
| sk_c9 != B
| multiply(sk_c9,B) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9 ),
inference(paramod,[status(thm)],[c_1,c_41]) ).
cnf(c_397,plain,
( multiply(C,sk_c8) != sk_c9
| inverse(B) != C
| multiply(B,C) != sk_c9
| sk_c9 != A
| multiply(sk_c9,A) != sk_c8
| multiply(identity,sk_c8) != sk_c9
| inverse(identity) != sk_c9 ),
inference(factor,[status(thm)],[c_177]) ).
cnf(c_12217,plain,
( multiply(sk_c9,sk_c8) != sk_c9
| multiply(identity,sk_c9) != sk_c9
| sk_c9 != A
| multiply(sk_c9,A) != sk_c8
| multiply(identity,sk_c8) != sk_c9
| inverse(identity) != sk_c9 ),
inference(factor,[status(thm)],[c_397]) ).
cnf(c_712,plain,
( multiply(sk_c9,sk_c8) != sk_c9
| sk_c9 != A
| multiply(sk_c9,A) != sk_c8
| multiply(identity,sk_c8) != sk_c9
| inverse(identity) != sk_c9 ),
inference(resolve,[status(thm)],[c_1,c_12217]) ).
cnf(c_12218,plain,
multiply(A,B) = multiply(A,multiply(identity,B)),
inference(paramod,[status(thm)],[c_66,c_3]) ).
cnf(c_1032,plain,
multiply(A,multiply(identity,B)) = multiply(A,B),
inference(copy,[status(thm)],[c_12218]) ).
cnf(c_12219,plain,
( multiply(sk_c9,sk_c8) != sk_c9
| sk_c9 != multiply(identity,A)
| multiply(sk_c9,A) != sk_c8
| multiply(identity,sk_c8) != sk_c9
| inverse(identity) != sk_c9 ),
inference(paramod,[status(thm)],[c_1032,c_712]) ).
cnf(c_1642,plain,
( multiply(sk_c9,sk_c8) != sk_c9
| multiply(identity,A) != sk_c9
| multiply(sk_c9,A) != sk_c8
| multiply(identity,sk_c8) != sk_c9
| inverse(identity) != sk_c9 ),
inference(copy,[status(thm)],[c_12219]) ).
cnf(c_1659,plain,
( multiply(sk_c9,sk_c8) != sk_c9
| multiply(sk_c9,sk_c8) != sk_c8
| multiply(identity,sk_c8) != sk_c9
| inverse(identity) != sk_c9 ),
inference(factor,[status(thm)],[c_1642]) ).
cnf(c_1660,plain,
( multiply(sk_c9,sk_c8) != sk_c9
| multiply(sk_c9,sk_c8) != sk_c8
| sk_c8 != sk_c9
| inverse(identity) != sk_c9 ),
inference(paramod,[status(thm)],[c_1,c_1659]) ).
cnf(c_1731,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(paramod,[status(thm)],[c_1,c_68]) ).
cnf(c_1819,plain,
( multiply(inverse(sk_c4),sk_c9) = sk_c5
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_4,c_1731]) ).
cnf(c_1823,plain,
( multiply(inverse(sk_c6),sk_c7) = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_8,c_1731]) ).
cnf(c_1826,plain,
( multiply(inverse(sk_c1),sk_c9) = sk_c8
| inverse(sk_c4) = sk_c5 ),
inference(paramod,[status(thm)],[c_11,c_1731]) ).
cnf(c_1830,plain,
( multiply(inverse(sk_c1),sk_c9) = sk_c8
| inverse(sk_c6) = sk_c9 ),
inference(paramod,[status(thm)],[c_15,c_1731]) ).
cnf(c_1842,plain,
( multiply(inverse(sk_c2),sk_c3) = sk_c9
| inverse(sk_c6) = sk_c9 ),
inference(paramod,[status(thm)],[c_27,c_1731]) ).
cnf(c_1847,plain,
( multiply(inverse(sk_c6),sk_c7) = sk_c9
| inverse(sk_c2) = sk_c9 ),
inference(paramod,[status(thm)],[c_32,c_1731]) ).
cnf(c_12220,plain,
( multiply(sk_c5,sk_c9) = sk_c5
| inverse(sk_c1) = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_5,c_1819]) ).
cnf(c_2008,plain,
( multiply(sk_c5,sk_c9) = sk_c5
| inverse(sk_c1) = sk_c9 ),
inference(copy,[status(thm)],[c_12220]) ).
cnf(c_2081,plain,
( multiply(inverse(sk_c5),sk_c5) = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_2008,c_1731]) ).
cnf(c_12221,plain,
( multiply(sk_c9,sk_c7) = sk_c9
| inverse(sk_c1) = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_9,c_1823]) ).
cnf(c_2164,plain,
( multiply(sk_c9,sk_c7) = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(copy,[status(thm)],[c_12221]) ).
cnf(c_12222,plain,
( sk_c9 = sk_c8
| inverse(sk_c1) = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_2164,c_7]) ).
cnf(c_12223,plain,
( sk_c8 = sk_c9
| inverse(sk_c1) = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(copy,[status(thm)],[c_12222]) ).
cnf(c_2176,plain,
( sk_c8 = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(copy,[status(thm)],[c_12223]) ).
cnf(c_2181,plain,
( multiply(inverse(sk_c9),sk_c9) = sk_c7
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_2164,c_1731]) ).
cnf(c_2183,plain,
( multiply(sk_c9,sk_c1) = identity
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_2176,c_2]) ).
cnf(c_2186,plain,
( multiply(sk_c9,multiply(sk_c1,A)) = A
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_2176,c_1731]) ).
cnf(c_2213,plain,
( multiply(inverse(sk_c9),identity) = sk_c1
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_2183,c_1731]) ).
cnf(c_12224,plain,
( multiply(sk_c9,sk_c7) = sk_c9
| inverse(sk_c2) = sk_c9
| inverse(sk_c2) = sk_c9 ),
inference(paramod,[status(thm)],[c_33,c_1847]) ).
cnf(c_2703,plain,
( multiply(sk_c9,sk_c7) = sk_c9
| inverse(sk_c2) = sk_c9 ),
inference(copy,[status(thm)],[c_12224]) ).
cnf(c_12225,plain,
( sk_c9 = sk_c8
| inverse(sk_c2) = sk_c9
| inverse(sk_c2) = sk_c9 ),
inference(paramod,[status(thm)],[c_2703,c_31]) ).
cnf(c_12226,plain,
( sk_c8 = sk_c9
| inverse(sk_c2) = sk_c9
| inverse(sk_c2) = sk_c9 ),
inference(copy,[status(thm)],[c_12225]) ).
cnf(c_2716,plain,
( sk_c8 = sk_c9
| inverse(sk_c2) = sk_c9 ),
inference(copy,[status(thm)],[c_12226]) ).
cnf(c_2722,plain,
( multiply(sk_c9,sk_c2) = identity
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_2716,c_2]) ).
cnf(c_2727,plain,
( multiply(sk_c9,sk_c3) = sk_c9
| inverse(sk_c6) = sk_c9
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_2716,c_1842]) ).
cnf(c_2771,plain,
( multiply(inverse(sk_c9),identity) = sk_c2
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_2722,c_1731]) ).
cnf(c_12227,plain,
( inverse(sk_c6) = sk_c9
| sk_c9 = sk_c8
| inverse(sk_c6) = sk_c9
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_2727,c_21]) ).
cnf(c_12228,plain,
( inverse(sk_c6) = sk_c9
| sk_c8 = sk_c9
| inverse(sk_c6) = sk_c9
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12227]) ).
cnf(c_12229,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c6) = sk_c9
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12228]) ).
cnf(c_2802,plain,
( inverse(sk_c6) = sk_c9
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12229]) ).
cnf(c_2803,plain,
( multiply(sk_c9,sk_c6) = identity
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_2802,c_2]) ).
cnf(c_2835,plain,
( multiply(inverse(sk_c9),identity) = sk_c6
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_2803,c_1731]) ).
cnf(c_12230,plain,
( sk_c2 = sk_c1
| sk_c8 = sk_c9
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_2771,c_2213]) ).
cnf(c_2853,plain,
( sk_c2 = sk_c1
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12230]) ).
cnf(c_2855,plain,
( multiply(sk_c9,sk_c7) = sk_c8
| multiply(sk_c1,sk_c9) = sk_c3
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_2853,c_25]) ).
cnf(c_12231,plain,
( sk_c6 = sk_c1
| sk_c8 = sk_c9
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_2835,c_2213]) ).
cnf(c_2976,plain,
( sk_c6 = sk_c1
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12231]) ).
cnf(c_2979,plain,
( multiply(sk_c1,sk_c9) = sk_c7
| multiply(sk_c9,sk_c3) = sk_c8
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_2976,c_20]) ).
cnf(c_2980,plain,
( multiply(sk_c1,sk_c9) = sk_c7
| multiply(sk_c2,sk_c9) = sk_c3
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_2976,c_26]) ).
cnf(c_12232,plain,
( multiply(sk_c1,sk_c9) = sk_c7
| multiply(sk_c1,sk_c9) = sk_c3
| sk_c8 = sk_c9
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_2853,c_2980]) ).
cnf(c_3100,plain,
( multiply(sk_c1,sk_c9) = sk_c7
| multiply(sk_c1,sk_c9) = sk_c3
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12232]) ).
cnf(c_12233,plain,
( sk_c9 = identity
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_2081,c_2]) ).
cnf(c_3478,plain,
( identity = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(copy,[status(thm)],[c_12233]) ).
cnf(c_3486,plain,
( multiply(sk_c9,sk_c1) = identity
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_3478,c_2]) ).
cnf(c_3491,plain,
( multiply(sk_c9,sk_c9) = sk_c8
| inverse(sk_c6) = sk_c9
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_3478,c_1830]) ).
cnf(c_3516,plain,
( multiply(inverse(sk_c9),identity) = sk_c1
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_3486,c_1731]) ).
cnf(c_12234,plain,
( sk_c7 = identity
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_2181,c_2]) ).
cnf(c_3765,plain,
( identity = sk_c7
| inverse(sk_c1) = sk_c9 ),
inference(copy,[status(thm)],[c_12234]) ).
cnf(c_3799,plain,
( multiply(sk_c9,sk_c1) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_3765,c_2]) ).
cnf(c_3804,plain,
( multiply(sk_c9,sk_c9) = sk_c8
| inverse(sk_c6) = sk_c9
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_3765,c_1830]) ).
cnf(c_3847,plain,
( multiply(inverse(sk_c9),identity) = sk_c1
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_3799,c_1731]) ).
cnf(c_12235,plain,
( multiply(sk_c9,sk_c3) = sk_c9
| sk_c8 = sk_c9
| multiply(sk_c9,sk_c7) = sk_c8
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_2855,c_2186]) ).
cnf(c_4182,plain,
( multiply(sk_c9,sk_c3) = sk_c9
| multiply(sk_c9,sk_c7) = sk_c8
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12235]) ).
cnf(c_12236,plain,
( multiply(sk_c9,sk_c7) = sk_c9
| sk_c8 = sk_c9
| multiply(sk_c9,sk_c3) = sk_c8
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_2979,c_2186]) ).
cnf(c_4184,plain,
( multiply(sk_c9,sk_c7) = sk_c9
| multiply(sk_c9,sk_c3) = sk_c8
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12236]) ).
cnf(c_12237,plain,
( multiply(sk_c9,sk_c7) = sk_c9
| sk_c8 = sk_c9
| multiply(sk_c1,sk_c9) = sk_c3
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_3100,c_2186]) ).
cnf(c_4186,plain,
( multiply(sk_c9,sk_c7) = sk_c9
| multiply(sk_c1,sk_c9) = sk_c3
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12237]) ).
cnf(c_12238,plain,
( sk_c9 = sk_c8
| multiply(sk_c9,sk_c3) = sk_c8
| multiply(sk_c9,sk_c3) = sk_c8
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_4184,c_19]) ).
cnf(c_12239,plain,
( sk_c8 = sk_c9
| multiply(sk_c9,sk_c3) = sk_c8
| multiply(sk_c9,sk_c3) = sk_c8
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12238]) ).
cnf(c_12240,plain,
( sk_c8 = sk_c9
| multiply(sk_c9,sk_c3) = sk_c8
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12239]) ).
cnf(c_4395,plain,
( multiply(sk_c9,sk_c3) = sk_c8
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12240]) ).
cnf(c_12241,plain,
( multiply(sk_c9,sk_c3) = sk_c9
| sk_c8 = sk_c9
| multiply(sk_c9,sk_c7) = sk_c9
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_4186,c_2186]) ).
cnf(c_4472,plain,
( multiply(sk_c9,sk_c3) = sk_c9
| multiply(sk_c9,sk_c7) = sk_c9
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12241]) ).
cnf(c_12242,plain,
( multiply(sk_c9,sk_c3) = sk_c9
| sk_c9 = sk_c8
| sk_c8 = sk_c9
| multiply(sk_c9,sk_c3) = sk_c9
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_4472,c_4182]) ).
cnf(c_12243,plain,
( multiply(sk_c9,sk_c3) = sk_c9
| sk_c8 = sk_c9
| sk_c8 = sk_c9
| multiply(sk_c9,sk_c3) = sk_c9
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12242]) ).
cnf(c_12244,plain,
( multiply(sk_c9,sk_c3) = sk_c9
| sk_c8 = sk_c9
| multiply(sk_c9,sk_c3) = sk_c9
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12243]) ).
cnf(c_12245,plain,
( multiply(sk_c9,sk_c3) = sk_c9
| multiply(sk_c9,sk_c3) = sk_c9
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12244]) ).
cnf(c_4693,plain,
( multiply(sk_c9,sk_c3) = sk_c9
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12245]) ).
cnf(c_12246,plain,
( sk_c9 = sk_c8
| sk_c8 = sk_c9
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_4693,c_4395]) ).
cnf(c_12247,plain,
( sk_c8 = sk_c9
| sk_c8 = sk_c9
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12246]) ).
cnf(c_12248,plain,
( sk_c8 = sk_c9
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_12247]) ).
cnf(c_4705,plain,
sk_c8 = sk_c9,
inference(copy,[status(thm)],[c_12248]) ).
cnf(c_4988,plain,
( multiply(sk_c9,sk_c8) != sk_c9
| multiply(sk_c9,sk_c8) != sk_c8
| inverse(identity) != sk_c9 ),
inference(resolve,[status(thm)],[c_4705,c_1660]) ).
cnf(c_5064,plain,
( inverse(sk_c4) = sk_c5
| multiply(sk_c1,sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_4705,c_11]) ).
cnf(c_5065,plain,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c1,sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_4705,c_12]) ).
cnf(c_5067,plain,
( inverse(sk_c6) = sk_c9
| multiply(sk_c1,sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_4705,c_15]) ).
cnf(c_12249,plain,
( multiply(sk_c9,sk_c8) != sk_c9
| multiply(A,sk_c9) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c8
| multiply(A,sk_c9) != sk_c9
| inverse(A) != sk_c9 ),
inference(paramod,[status(thm)],[c_4705,c_55]) ).
cnf(c_5098,plain,
( multiply(sk_c9,sk_c8) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c8
| multiply(A,sk_c9) != sk_c9
| inverse(A) != sk_c9 ),
inference(copy,[status(thm)],[c_12249]) ).
cnf(c_5135,plain,
( multiply(sk_c9,sk_c9) = sk_c9
| inverse(sk_c6) = sk_c9
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_4705,c_3491]) ).
cnf(c_5137,plain,
( multiply(sk_c9,sk_c9) = sk_c9
| inverse(sk_c6) = sk_c9
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_4705,c_3804]) ).
cnf(c_12250,plain,
( multiply(sk_c9,sk_c8) != sk_c9
| multiply(sk_c9,sk_c8) != sk_c9
| inverse(identity) != sk_c9 ),
inference(paramod,[status(thm)],[c_4705,c_4988]) ).
cnf(c_5247,plain,
( multiply(sk_c9,sk_c8) != sk_c9
| inverse(identity) != sk_c9 ),
inference(copy,[status(thm)],[c_12250]) ).
cnf(c_5248,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| inverse(identity) != sk_c9 ),
inference(paramod,[status(thm)],[c_4705,c_5247]) ).
cnf(c_5791,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c8
| multiply(A,sk_c9) != sk_c9
| inverse(A) != sk_c9 ),
inference(paramod,[status(thm)],[c_4705,c_5098]) ).
cnf(c_12251,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| multiply(sk_c9,sk_c9) != sk_c9
| multiply(A,sk_c9) != sk_c9
| inverse(A) != sk_c9 ),
inference(paramod,[status(thm)],[c_4705,c_5791]) ).
cnf(c_5834,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| multiply(A,sk_c9) != sk_c9
| inverse(A) != sk_c9 ),
inference(copy,[status(thm)],[c_12251]) ).
cnf(c_5839,plain,
( inverse(sk_c6) = sk_c9
| multiply(sk_c9,sk_c9) != sk_c9
| inverse(sk_c1) != sk_c9 ),
inference(resolve,[status(thm)],[c_5834,c_5067]) ).
cnf(c_5841,plain,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c9,sk_c9) != sk_c9
| inverse(sk_c1) != sk_c9 ),
inference(resolve,[status(thm)],[c_5834,c_5065]) ).
cnf(c_5842,plain,
( inverse(sk_c4) = sk_c5
| multiply(sk_c9,sk_c9) != sk_c9
| inverse(sk_c1) != sk_c9 ),
inference(resolve,[status(thm)],[c_5834,c_5064]) ).
cnf(c_5863,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| multiply(A,sk_c9) != sk_c9
| inverse(multiply(A,identity)) != sk_c9 ),
inference(paramod,[status(thm)],[c_66,c_5834]) ).
cnf(c_12252,plain,
( inverse(sk_c6) = sk_c9
| identity = sk_c7
| inverse(sk_c6) = sk_c9
| inverse(sk_c1) != sk_c9 ),
inference(resolve,[status(thm)],[c_5839,c_5137]) ).
cnf(c_6113,plain,
( identity = sk_c7
| inverse(sk_c6) = sk_c9
| inverse(sk_c1) != sk_c9 ),
inference(copy,[status(thm)],[c_12252]) ).
cnf(c_12253,plain,
( inverse(sk_c6) = sk_c9
| identity = sk_c9
| inverse(sk_c6) = sk_c9
| inverse(sk_c1) != sk_c9 ),
inference(resolve,[status(thm)],[c_5839,c_5135]) ).
cnf(c_6114,plain,
( identity = sk_c9
| inverse(sk_c6) = sk_c9
| inverse(sk_c1) != sk_c9 ),
inference(copy,[status(thm)],[c_12253]) ).
cnf(c_12254,plain,
( identity = sk_c7
| identity = sk_c7
| inverse(sk_c6) = sk_c9 ),
inference(resolve,[status(thm)],[c_6113,c_3765]) ).
cnf(c_6175,plain,
( identity = sk_c7
| inverse(sk_c6) = sk_c9 ),
inference(copy,[status(thm)],[c_12254]) ).
cnf(c_6176,plain,
( multiply(sk_c9,sk_c6) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_6175,c_2]) ).
cnf(c_6198,plain,
( multiply(inverse(sk_c9),identity) = sk_c6
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_6176,c_1731]) ).
cnf(c_12255,plain,
( identity = sk_c9
| identity = sk_c9
| inverse(sk_c6) = sk_c9 ),
inference(resolve,[status(thm)],[c_6114,c_3478]) ).
cnf(c_6230,plain,
( identity = sk_c9
| inverse(sk_c6) = sk_c9 ),
inference(copy,[status(thm)],[c_12255]) ).
cnf(c_6231,plain,
( multiply(sk_c9,sk_c6) = identity
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_6230,c_2]) ).
cnf(c_6249,plain,
( multiply(inverse(sk_c9),identity) = sk_c6
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_6231,c_1731]) ).
cnf(c_12256,plain,
( sk_c6 = sk_c1
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_6198,c_3847]) ).
cnf(c_6839,plain,
( sk_c6 = sk_c1
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_12256]) ).
cnf(c_6845,plain,
( multiply(sk_c7,A) = A
| sk_c6 = sk_c1 ),
inference(paramod,[status(thm)],[c_6839,c_1]) ).
cnf(c_6848,plain,
( multiply(sk_c9,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c9
| sk_c6 = sk_c1 ),
inference(paramod,[status(thm)],[c_6839,c_83]) ).
cnf(c_6943,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| inverse(sk_c7) != sk_c9
| sk_c6 = sk_c1 ),
inference(resolve,[status(thm)],[c_6845,c_5834]) ).
cnf(c_12257,plain,
( sk_c6 = sk_c1
| identity = sk_c9
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_6249,c_3516]) ).
cnf(c_7309,plain,
( sk_c6 = sk_c1
| identity = sk_c9 ),
inference(copy,[status(thm)],[c_12257]) ).
cnf(c_7331,plain,
( multiply(sk_c9,A) = A
| sk_c6 = sk_c1 ),
inference(paramod,[status(thm)],[c_7309,c_1]) ).
cnf(c_12258,plain,
( inverse(sk_c7) != sk_c9
| sk_c6 = sk_c1
| sk_c6 = sk_c1 ),
inference(resolve,[status(thm)],[c_7331,c_6943]) ).
cnf(c_7413,plain,
( inverse(sk_c7) != sk_c9
| sk_c6 = sk_c1 ),
inference(copy,[status(thm)],[c_12258]) ).
cnf(c_7428,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c1) != sk_c9
| sk_c6 = sk_c1 ),
inference(resolve,[status(thm)],[c_7331,c_5839]) ).
cnf(c_7434,plain,
( inverse(identity) != sk_c9
| sk_c6 = sk_c1 ),
inference(resolve,[status(thm)],[c_7331,c_5248]) ).
cnf(c_12259,plain,
( sk_c6 = identity
| inverse(sk_c1) = sk_c9
| sk_c6 = sk_c1 ),
inference(paramod,[status(thm)],[c_7331,c_83]) ).
cnf(c_7470,plain,
( identity = sk_c6
| inverse(sk_c1) = sk_c9
| sk_c6 = sk_c1 ),
inference(copy,[status(thm)],[c_12259]) ).
cnf(c_12260,plain,
( sk_c6 = sk_c7
| inverse(sk_c1) = sk_c9
| sk_c6 = sk_c1
| sk_c6 = sk_c1 ),
inference(paramod,[status(thm)],[c_7331,c_6848]) ).
cnf(c_12261,plain,
( sk_c7 = sk_c6
| inverse(sk_c1) = sk_c9
| sk_c6 = sk_c1
| sk_c6 = sk_c1 ),
inference(copy,[status(thm)],[c_12260]) ).
cnf(c_7475,plain,
( sk_c7 = sk_c6
| inverse(sk_c1) = sk_c9
| sk_c6 = sk_c1 ),
inference(copy,[status(thm)],[c_12261]) ).
cnf(c_7656,plain,
( multiply(sk_c9,sk_c1) = identity
| identity = sk_c6
| sk_c6 = sk_c1 ),
inference(paramod,[status(thm)],[c_7470,c_2]) ).
cnf(c_12262,plain,
( identity = sk_c1
| sk_c6 = sk_c1
| identity = sk_c6
| sk_c6 = sk_c1 ),
inference(paramod,[status(thm)],[c_7656,c_7331]) ).
cnf(c_8808,plain,
( identity = sk_c1
| identity = sk_c6
| sk_c6 = sk_c1 ),
inference(copy,[status(thm)],[c_12262]) ).
cnf(c_12263,plain,
( sk_c6 = sk_c1
| sk_c6 = sk_c7
| identity = sk_c1
| sk_c6 = sk_c1 ),
inference(paramod,[status(thm)],[c_8808,c_6839]) ).
cnf(c_12264,plain,
( sk_c6 = sk_c1
| sk_c7 = sk_c6
| identity = sk_c1
| sk_c6 = sk_c1 ),
inference(copy,[status(thm)],[c_12263]) ).
cnf(c_8851,plain,
( sk_c7 = sk_c6
| identity = sk_c1
| sk_c6 = sk_c1 ),
inference(copy,[status(thm)],[c_12264]) ).
cnf(c_12265,plain,
( inverse(sk_c1) != sk_c9
| sk_c6 = sk_c1
| sk_c7 = sk_c6
| sk_c6 = sk_c1 ),
inference(paramod,[status(thm)],[c_8851,c_7434]) ).
cnf(c_8898,plain,
( inverse(sk_c1) != sk_c9
| sk_c7 = sk_c6
| sk_c6 = sk_c1 ),
inference(copy,[status(thm)],[c_12265]) ).
cnf(c_12266,plain,
( sk_c7 = sk_c6
| sk_c6 = sk_c1
| sk_c7 = sk_c6
| sk_c6 = sk_c1 ),
inference(resolve,[status(thm)],[c_8898,c_7475]) ).
cnf(c_12267,plain,
( sk_c7 = sk_c6
| sk_c7 = sk_c6
| sk_c6 = sk_c1 ),
inference(copy,[status(thm)],[c_12266]) ).
cnf(c_9458,plain,
( sk_c7 = sk_c6
| sk_c6 = sk_c1 ),
inference(copy,[status(thm)],[c_12267]) ).
cnf(c_12268,plain,
( inverse(sk_c6) != sk_c9
| sk_c6 = sk_c1
| sk_c6 = sk_c1 ),
inference(paramod,[status(thm)],[c_9458,c_7413]) ).
cnf(c_9514,plain,
( inverse(sk_c6) != sk_c9
| sk_c6 = sk_c1 ),
inference(copy,[status(thm)],[c_12268]) ).
cnf(c_9587,plain,
( inverse(sk_c1) = sk_c9
| sk_c6 = sk_c1 ),
inference(resolve,[status(thm)],[c_9514,c_9]) ).
cnf(c_12269,plain,
( inverse(sk_c6) = sk_c9
| sk_c6 = sk_c1
| sk_c6 = sk_c1 ),
inference(resolve,[status(thm)],[c_9587,c_7428]) ).
cnf(c_9661,plain,
( inverse(sk_c6) = sk_c9
| sk_c6 = sk_c1 ),
inference(copy,[status(thm)],[c_12269]) ).
cnf(c_12270,plain,
( sk_c6 = sk_c1
| sk_c6 = sk_c1 ),
inference(resolve,[status(thm)],[c_9661,c_9514]) ).
cnf(c_9668,plain,
sk_c6 = sk_c1,
inference(copy,[status(thm)],[c_12270]) ).
cnf(c_12271,plain,
( inverse(sk_c1) = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_9668,c_9]) ).
cnf(c_9794,plain,
inverse(sk_c1) = sk_c9,
inference(copy,[status(thm)],[c_12271]) ).
cnf(c_10028,plain,
( inverse(sk_c4) = sk_c5
| multiply(sk_c9,sk_c9) != sk_c9 ),
inference(resolve,[status(thm)],[c_9794,c_5842]) ).
cnf(c_10029,plain,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c9,sk_c9) != sk_c9 ),
inference(resolve,[status(thm)],[c_9794,c_5841]) ).
cnf(c_10173,plain,
multiply(sk_c9,sk_c1) = identity,
inference(paramod,[status(thm)],[c_9794,c_2]) ).
cnf(c_10176,plain,
multiply(sk_c9,multiply(sk_c1,A)) = A,
inference(paramod,[status(thm)],[c_9794,c_1731]) ).
cnf(c_10177,plain,
( multiply(sk_c9,sk_c9) = sk_c8
| inverse(sk_c4) = sk_c5 ),
inference(paramod,[status(thm)],[c_9794,c_1826]) ).
cnf(c_10198,plain,
multiply(inverse(sk_c9),identity) = sk_c1,
inference(paramod,[status(thm)],[c_10173,c_1731]) ).
cnf(c_12272,plain,
( inverse(sk_c4) = sk_c5
| sk_c8 != sk_c9
| inverse(sk_c4) = sk_c5 ),
inference(paramod,[status(thm)],[c_10177,c_10028]) ).
cnf(c_12273,plain,
( sk_c8 != sk_c9
| inverse(sk_c4) = sk_c5 ),
inference(copy,[status(thm)],[c_12272]) ).
cnf(c_10335,plain,
inverse(sk_c4) = sk_c5,
inference(resolve,[status(thm)],[c_4705,c_12273]) ).
cnf(c_10359,plain,
multiply(sk_c5,multiply(sk_c4,A)) = A,
inference(paramod,[status(thm)],[c_10335,c_1731]) ).
cnf(c_12274,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| multiply(inverse(sk_c9),sk_c9) != sk_c9
| inverse(sk_c1) != sk_c9 ),
inference(paramod,[status(thm)],[c_10198,c_5863]) ).
cnf(c_10807,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| multiply(inverse(sk_c9),sk_c9) != sk_c9 ),
inference(resolve,[status(thm)],[c_9794,c_12274]) ).
cnf(c_10992,plain,
( multiply(sk_c9,sk_c9) = sk_c8
| multiply(sk_c5,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_12,c_10176]) ).
cnf(c_11013,plain,
( multiply(sk_c9,sk_c9) = sk_c9
| multiply(sk_c5,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_5065,c_10176]) ).
cnf(c_11090,plain,
( multiply(sk_c9,sk_c9) = sk_c8
| multiply(sk_c5,sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_4705,c_10992]) ).
cnf(c_11164,plain,
( multiply(sk_c9,sk_c9) = sk_c9
| multiply(sk_c5,sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_4705,c_11013]) ).
cnf(c_11469,plain,
( multiply(sk_c5,sk_c9) = sk_c5
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_10,c_10359]) ).
cnf(c_11509,plain,
( multiply(sk_c5,sk_c9) = sk_c5
| multiply(sk_c1,sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_4705,c_11469]) ).
cnf(c_11510,plain,
( multiply(sk_c9,sk_c9) = sk_c8
| multiply(sk_c5,sk_c9) = sk_c5 ),
inference(paramod,[status(thm)],[c_11469,c_10176]) ).
cnf(c_12275,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| inverse(sk_c1) != sk_c9
| multiply(sk_c5,sk_c9) = sk_c5 ),
inference(resolve,[status(thm)],[c_11509,c_5834]) ).
cnf(c_11682,plain,
( multiply(sk_c9,sk_c9) != sk_c9
| multiply(sk_c5,sk_c9) = sk_c5 ),
inference(resolve,[status(thm)],[c_9794,c_12275]) ).
cnf(c_12276,plain,
( multiply(sk_c9,sk_c9) = sk_c8
| sk_c5 = sk_c9
| multiply(sk_c9,sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_11510,c_11090]) ).
cnf(c_11744,plain,
( sk_c5 = sk_c9
| multiply(sk_c9,sk_c9) = sk_c8 ),
inference(copy,[status(thm)],[c_12276]) ).
cnf(c_11800,plain,
( sk_c5 = sk_c9
| multiply(sk_c9,sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_4705,c_11744]) ).
cnf(c_12277,plain,
( multiply(sk_c5,sk_c8) = sk_c9
| sk_c8 != sk_c9
| sk_c5 = sk_c9 ),
inference(paramod,[status(thm)],[c_11744,c_10029]) ).
cnf(c_11810,plain,
( multiply(sk_c5,sk_c8) = sk_c9
| sk_c5 = sk_c9 ),
inference(resolve,[status(thm)],[c_4705,c_12277]) ).
cnf(c_11861,plain,
( multiply(sk_c5,sk_c9) = sk_c9
| sk_c5 = sk_c9 ),
inference(paramod,[status(thm)],[c_4705,c_11810]) ).
cnf(c_11936,plain,
( sk_c5 = sk_c9
| multiply(sk_c5,sk_c9) = sk_c5 ),
inference(resolve,[status(thm)],[c_11682,c_11800]) ).
cnf(c_12278,plain,
( sk_c5 = sk_c9
| sk_c5 = sk_c9
| sk_c5 = sk_c9 ),
inference(paramod,[status(thm)],[c_11936,c_11861]) ).
cnf(c_12279,plain,
( sk_c5 = sk_c9
| sk_c5 = sk_c9 ),
inference(copy,[status(thm)],[c_12278]) ).
cnf(c_11961,plain,
sk_c5 = sk_c9,
inference(copy,[status(thm)],[c_12279]) ).
cnf(c_12280,plain,
( multiply(sk_c9,sk_c9) = sk_c9
| multiply(sk_c9,sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_11961,c_11164]) ).
cnf(c_12011,plain,
multiply(sk_c9,sk_c9) = sk_c9,
inference(copy,[status(thm)],[c_12280]) ).
cnf(c_12040,plain,
multiply(inverse(sk_c9),sk_c9) != sk_c9,
inference(resolve,[status(thm)],[c_12011,c_10807]) ).
cnf(c_12281,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c9,
inference(paramod,[status(thm)],[c_12011,c_1731]) ).
cnf(c_12210,plain,
$false,
inference(resolve,[status(thm)],[c_12040,c_12281]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP223-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n010.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 25 14:39:29 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.35 % Process 982053 was started by sandbox on n010,
% 0.08/0.35 % Fri Sep 25 14:39:29 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.35
% 0.08/0.35 % From the command line: assign(max_seconds, 300).
% 75.52/18.09
% 75.52/18.09 % Assigning unary symbol inverse kb_weight 0 and highest precedence (13).
% 75.52/18.09
% 75.52/18.09 % given #500 (T,wt=14): 9004 sk_c6 = sk_c1 | sk_c6 = sk_c8 | sk_c1 = sk_c8. [para(8857(b,1),8310(b,1)),merge(c)].
% 75.52/18.09
% 75.52/18.09 % SZS status Unsatisfiable for theBenchmark
% 75.52/18.09
% 75.52/18.09 % Proof 1 at 1.41 (+ 0.24) seconds.
% 75.52/18.09 % Length of proof is 150.
% 75.52/18.09 % Level of proof is 49.
% 75.52/18.09 % Maximum clause weight is 61.000.
% 75.52/18.09 % Given clauses 640.
% 75.52/18.09
% 75.52/18.09 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------