%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP319-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 : n020.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:37 AM UTC 2026
% Result : Unsatisfiable 282.86s 69.24s
% Output : CNFRefutation 282.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 68
% Number of leaves : 26
% Syntax : Number of formulae : 238 ( 35 unt; 0 def)
% Number of atoms : 606 ( 605 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 564 ( 196 ~; 368 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 3 avg)
% Maximal term depth : 5 ( 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 : 93 ( 0 sgn 11 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(left_identity,axiom,
! [VAR_0] : multiply(identity,VAR_0) = VAR_0,
file('theBenchmark.p',left_identity) ).
cnf(c_1,plain,
multiply(identity,A) = A,
inference(clausify,[status(thm)],[left_identity]) ).
fof(left_inverse,axiom,
! [VAR_0] : multiply(inverse(VAR_0),VAR_0) = identity,
file('theBenchmark.p',left_inverse) ).
cnf(c_2,plain,
multiply(inverse(A),A) = identity,
inference(clausify,[status(thm)],[left_inverse]) ).
fof(associativity,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(multiply(VAR_0,VAR_1),VAR_2) = multiply(VAR_0,multiply(VAR_1,VAR_2)),
file('theBenchmark.p',associativity) ).
cnf(c_3,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(clausify,[status(thm)],[associativity]) ).
fof(prove_this_1,axiom,
( multiply(sk_c4,sk_c9) = sk_c8
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('theBenchmark.p',prove_this_1) ).
cnf(c_4,plain,
( multiply(sk_c4,sk_c9) = sk_c8
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_1]) ).
fof(prove_this_2,axiom,
( inverse(sk_c4) = sk_c9
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('theBenchmark.p',prove_this_2) ).
cnf(c_5,plain,
( inverse(sk_c4) = sk_c9
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_2]) ).
fof(prove_this_3,axiom,
( multiply(sk_c5,sk_c8) = sk_c7
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('theBenchmark.p',prove_this_3) ).
cnf(c_6,plain,
( multiply(sk_c5,sk_c8) = sk_c7
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_3]) ).
fof(prove_this_4,axiom,
( inverse(sk_c5) = sk_c8
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('theBenchmark.p',prove_this_4) ).
cnf(c_7,plain,
( inverse(sk_c5) = sk_c8
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_4]) ).
fof(prove_this_7,axiom,
( multiply(sk_c4,sk_c9) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_7) ).
cnf(c_10,plain,
( multiply(sk_c4,sk_c9) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_7]) ).
fof(prove_this_8,axiom,
( inverse(sk_c4) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_11,plain,
( inverse(sk_c4) = sk_c9
| 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_c7
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_9) ).
cnf(c_12,plain,
( multiply(sk_c5,sk_c8) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_9]) ).
fof(prove_this_10,axiom,
( inverse(sk_c5) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_10) ).
cnf(c_13,plain,
( inverse(sk_c5) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_10]) ).
fof(prove_this_11,axiom,
( inverse(sk_c6) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_11) ).
cnf(c_14,plain,
( inverse(sk_c6) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_11]) ).
fof(prove_this_12,axiom,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_12) ).
cnf(c_15,plain,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_12]) ).
fof(prove_this_13,axiom,
( multiply(sk_c4,sk_c9) = sk_c8
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_13) ).
cnf(c_16,plain,
( multiply(sk_c4,sk_c9) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_13]) ).
fof(prove_this_14,axiom,
( inverse(sk_c4) = sk_c9
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_14) ).
cnf(c_17,plain,
( inverse(sk_c4) = sk_c9
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_14]) ).
fof(prove_this_15,axiom,
( multiply(sk_c5,sk_c8) = sk_c7
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_15) ).
cnf(c_18,plain,
( multiply(sk_c5,sk_c8) = sk_c7
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_15]) ).
fof(prove_this_16,axiom,
( inverse(sk_c5) = sk_c8
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_16) ).
cnf(c_19,plain,
( inverse(sk_c5) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_16]) ).
fof(prove_this_17,axiom,
( inverse(sk_c6) = sk_c7
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_17) ).
cnf(c_20,plain,
( inverse(sk_c6) = sk_c7
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_17]) ).
fof(prove_this_18,axiom,
( multiply(sk_c6,sk_c9) = sk_c7
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_18) ).
cnf(c_21,plain,
( multiply(sk_c6,sk_c9) = sk_c7
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_18]) ).
fof(prove_this_19,axiom,
( multiply(sk_c4,sk_c9) = sk_c8
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('theBenchmark.p',prove_this_19) ).
cnf(c_22,plain,
( multiply(sk_c4,sk_c9) = sk_c8
| multiply(sk_c9,sk_c3) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_19]) ).
fof(prove_this_20,axiom,
( inverse(sk_c4) = sk_c9
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('theBenchmark.p',prove_this_20) ).
cnf(c_23,plain,
( inverse(sk_c4) = sk_c9
| multiply(sk_c9,sk_c3) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_20]) ).
fof(prove_this_27,axiom,
( multiply(sk_c5,sk_c8) = sk_c7
| multiply(sk_c2,sk_c9) = sk_c3 ),
file('theBenchmark.p',prove_this_27) ).
cnf(c_30,plain,
( multiply(sk_c5,sk_c8) = sk_c7
| multiply(sk_c2,sk_c9) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_27]) ).
fof(prove_this_28,axiom,
( inverse(sk_c5) = sk_c8
| multiply(sk_c2,sk_c9) = sk_c3 ),
file('theBenchmark.p',prove_this_28) ).
cnf(c_31,plain,
( inverse(sk_c5) = sk_c8
| multiply(sk_c2,sk_c9) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_28]) ).
fof(prove_this_33,axiom,
( multiply(sk_c5,sk_c8) = sk_c7
| inverse(sk_c2) = sk_c9 ),
file('theBenchmark.p',prove_this_33) ).
cnf(c_36,plain,
( multiply(sk_c5,sk_c8) = sk_c7
| inverse(sk_c2) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_33]) ).
fof(prove_this_34,axiom,
( inverse(sk_c5) = sk_c8
| inverse(sk_c2) = sk_c9 ),
file('theBenchmark.p',prove_this_34) ).
cnf(c_37,plain,
( inverse(sk_c5) = sk_c8
| inverse(sk_c2) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_34]) ).
fof(prove_this_37,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( multiply(VAR_5,sk_c9) != sk_c7
| inverse(VAR_5) != sk_c7
| inverse(VAR_4) != sk_c8
| multiply(VAR_4,sk_c8) != sk_c7
| inverse(VAR_3) != sk_c9
| multiply(VAR_3,sk_c9) != sk_c8
| inverse(VAR_2) != sk_c9
| multiply(VAR_2,sk_c9) != VAR_1
| multiply(sk_c9,VAR_1) != sk_c8
| inverse(VAR_0) != sk_c8
| multiply(VAR_0,sk_c8) != sk_c9
| multiply(sk_c8,sk_c9) != sk_c7 ),
file('theBenchmark.p',prove_this_37) ).
cnf(c_40,plain,
( multiply(F,sk_c9) != sk_c7
| inverse(F) != sk_c7
| inverse(E) != sk_c8
| multiply(E,sk_c8) != sk_c7
| inverse(D) != sk_c9
| multiply(D,sk_c9) != sk_c8
| inverse(C) != sk_c9
| multiply(C,sk_c9) != B
| multiply(sk_c9,B) != sk_c8
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c9
| multiply(sk_c8,sk_c9) != sk_c7 ),
inference(clausify,[status(thm)],[prove_this_37]) ).
cnf(c_42,plain,
( inverse(sk_c8) != sk_c7
| inverse(E) != sk_c8
| multiply(E,sk_c8) != sk_c7
| inverse(D) != sk_c9
| multiply(D,sk_c9) != sk_c8
| inverse(C) != sk_c9
| multiply(C,sk_c9) != B
| multiply(sk_c9,B) != sk_c8
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c9
| multiply(sk_c8,sk_c9) != sk_c7 ),
inference(factor,[status(thm)],[c_40]) ).
cnf(c_54,plain,
( inverse(sk_c8) != sk_c7
| inverse(D) != sk_c8
| multiply(D,sk_c8) != sk_c7
| multiply(C,sk_c9) != sk_c8
| inverse(C) != sk_c9
| multiply(C,sk_c9) != B
| multiply(sk_c9,B) != sk_c8
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c9
| multiply(sk_c8,sk_c9) != sk_c7 ),
inference(factor,[status(thm)],[c_42]) ).
cnf(c_54325,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_54326,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_54325]) ).
cnf(c_72,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_54326]) ).
cnf(c_88,plain,
( multiply(sk_c7,sk_c6) = identity
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_14,c_2]) ).
cnf(c_54327,plain,
( multiply(multiply(A,sk_c6),sk_c9) = multiply(A,sk_c7)
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_15,c_3]) ).
cnf(c_90,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_54327]) ).
cnf(c_91,plain,
( multiply(sk_c8,sk_c1) = identity
| multiply(sk_c4,sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_16,c_2]) ).
cnf(c_93,plain,
( multiply(sk_c8,sk_c1) = identity
| multiply(sk_c5,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_95,plain,
( multiply(sk_c7,sk_c6) = identity
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_20,c_2]) ).
cnf(c_96,plain,
( multiply(sk_c8,sk_c1) = identity
| multiply(sk_c6,sk_c9) = sk_c7 ),
inference(paramod,[status(thm)],[c_21,c_2]) ).
cnf(c_54328,plain,
( multiply(sk_c7,A) = multiply(sk_c5,multiply(sk_c8,A))
| multiply(sk_c2,sk_c9) = sk_c3 ),
inference(paramod,[status(thm)],[c_30,c_3]) ).
cnf(c_109,plain,
( multiply(sk_c5,multiply(sk_c8,A)) = multiply(sk_c7,A)
| multiply(sk_c2,sk_c9) = sk_c3 ),
inference(copy,[status(thm)],[c_54328]) ).
cnf(c_111,plain,
( multiply(sk_c8,sk_c5) = identity
| multiply(sk_c2,sk_c9) = sk_c3 ),
inference(paramod,[status(thm)],[c_31,c_2]) ).
cnf(c_117,plain,
( multiply(sk_c9,sk_c2) = identity
| multiply(sk_c5,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_36,c_2]) ).
cnf(c_118,plain,
( multiply(sk_c8,sk_c5) = identity
| inverse(sk_c2) = sk_c9 ),
inference(paramod,[status(thm)],[c_37,c_2]) ).
cnf(c_2314,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_72]) ).
cnf(c_2352,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_72,c_72]) ).
cnf(c_2353,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_2352,c_2314]) ).
cnf(c_2430,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_2353,c_2]) ).
cnf(c_3249,plain,
multiply(A,inverse(A)) = identity,
inference(paramod,[status(thm)],[c_2352,c_2]) ).
cnf(c_3282,plain,
multiply(A,multiply(inverse(A),B)) = B,
inference(paramod,[status(thm)],[c_2352,c_72]) ).
cnf(c_54329,plain,
multiply(A,identity) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_2352,c_2353]) ).
cnf(c_54330,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_2353,c_54329]) ).
cnf(c_3283,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_54330]) ).
cnf(c_54331,plain,
( inverse(sk_c8) != sk_c7
| inverse(C) != sk_c8
| multiply(C,sk_c8) != sk_c7
| multiply(B,sk_c9) != sk_c8
| inverse(B) != sk_c9
| multiply(B,sk_c9) != A
| multiply(sk_c9,A) != sk_c8
| multiply(inverse(sk_c8),sk_c8) != sk_c9
| multiply(sk_c8,sk_c9) != sk_c7 ),
inference(resolve,[status(thm)],[c_3283,c_54]) ).
cnf(c_3384,plain,
( inverse(sk_c8) != sk_c7
| inverse(C) != sk_c8
| multiply(C,sk_c8) != sk_c7
| multiply(B,sk_c9) != sk_c8
| inverse(B) != sk_c9
| multiply(B,sk_c9) != A
| multiply(sk_c9,A) != sk_c8
| identity != sk_c9
| multiply(sk_c8,sk_c9) != sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_54331]) ).
cnf(c_54332,plain,
identity = multiply(A,multiply(B,inverse(multiply(A,B)))),
inference(paramod,[status(thm)],[c_3249,c_3]) ).
cnf(c_3553,plain,
multiply(A,multiply(B,inverse(multiply(A,B)))) = identity,
inference(copy,[status(thm)],[c_54332]) ).
cnf(c_3554,plain,
( multiply(sk_c4,sk_c9) = identity
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(paramod,[status(thm)],[c_5,c_3249]) ).
cnf(c_3555,plain,
( multiply(sk_c5,sk_c8) = identity
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(paramod,[status(thm)],[c_7,c_3249]) ).
cnf(c_3557,plain,
( multiply(sk_c4,sk_c9) = identity
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_11,c_3249]) ).
cnf(c_3558,plain,
( multiply(sk_c5,sk_c8) = identity
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_13,c_3249]) ).
cnf(c_3561,plain,
( multiply(sk_c4,sk_c9) = identity
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_17,c_3249]) ).
cnf(c_3563,plain,
( multiply(sk_c5,sk_c8) = identity
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_19,c_3249]) ).
cnf(c_3566,plain,
( multiply(sk_c4,sk_c9) = identity
| multiply(sk_c9,sk_c3) = sk_c8 ),
inference(paramod,[status(thm)],[c_23,c_3249]) ).
cnf(c_3590,plain,
( multiply(sk_c1,sk_c8) = identity
| multiply(sk_c7,sk_c6) = identity ),
inference(paramod,[status(thm)],[c_95,c_3249]) ).
cnf(c_3592,plain,
( multiply(sk_c2,sk_c9) = identity
| multiply(sk_c8,sk_c5) = identity ),
inference(paramod,[status(thm)],[c_118,c_3249]) ).
cnf(c_8461,plain,
( multiply(sk_c8,sk_c1) = identity
| multiply(sk_c4,sk_c9) = identity ),
inference(paramod,[status(thm)],[c_3561,c_2]) ).
cnf(c_8539,plain,
( multiply(sk_c8,sk_c1) = identity
| multiply(sk_c5,sk_c8) = identity ),
inference(paramod,[status(thm)],[c_3563,c_2]) ).
cnf(c_10405,plain,
( multiply(inverse(sk_c7),multiply(sk_c6,sk_c9)) = identity
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_2,c_90]) ).
cnf(c_54333,plain,
multiply(inverse(A),identity) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_3553,c_72]) ).
cnf(c_54334,plain,
inverse(A) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_2353,c_54333]) ).
cnf(c_13138,plain,
multiply(A,inverse(multiply(B,A))) = inverse(B),
inference(copy,[status(thm)],[c_54334]) ).
cnf(c_13165,plain,
( multiply(sk_c5,multiply(sk_c8,inverse(sk_c7))) = identity
| multiply(sk_c9,sk_c2) = identity ),
inference(paramod,[status(thm)],[c_117,c_3553]) ).
cnf(c_54335,plain,
( multiply(sk_c9,inverse(sk_c7)) = inverse(sk_c6)
| multiply(sk_c8,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_96,c_13138]) ).
cnf(c_13203,plain,
( inverse(sk_c6) = multiply(sk_c9,inverse(sk_c7))
| multiply(sk_c8,sk_c1) = identity ),
inference(copy,[status(thm)],[c_54335]) ).
cnf(c_54336,plain,
( identity = sk_c8
| multiply(sk_c8,sk_c9) = sk_c7
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(paramod,[status(thm)],[c_3554,c_4]) ).
cnf(c_13303,plain,
( identity = sk_c8
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(copy,[status(thm)],[c_54336]) ).
cnf(c_54337,plain,
( identity = sk_c7
| multiply(sk_c8,sk_c9) = sk_c7
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(paramod,[status(thm)],[c_3555,c_6]) ).
cnf(c_13734,plain,
( identity = sk_c7
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(copy,[status(thm)],[c_54337]) ).
cnf(c_13739,plain,
( multiply(inverse(sk_c8),sk_c7) = sk_c9
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_13734,c_72]) ).
cnf(c_54338,plain,
( multiply(multiply(A,inverse(sk_c8)),sk_c7) = multiply(A,sk_c9)
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_13739,c_3]) ).
cnf(c_13745,plain,
( multiply(A,multiply(inverse(sk_c8),sk_c7)) = multiply(A,sk_c9)
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_3,c_54338]) ).
cnf(c_54339,plain,
( identity = sk_c8
| multiply(sk_c1,sk_c8) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_3557,c_10]) ).
cnf(c_14165,plain,
( identity = sk_c8
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(copy,[status(thm)],[c_54339]) ).
cnf(c_14174,plain,
( multiply(inverse(sk_c1),sk_c9) = sk_c8
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_14165,c_72]) ).
cnf(c_54340,plain,
( identity = sk_c7
| multiply(sk_c1,sk_c8) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_3558,c_12]) ).
cnf(c_14570,plain,
( identity = sk_c7
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(copy,[status(thm)],[c_54340]) ).
cnf(c_14576,plain,
( multiply(inverse(sk_c1),sk_c9) = sk_c8
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_14570,c_72]) ).
cnf(c_54341,plain,
( multiply(sk_c5,identity) = multiply(sk_c7,inverse(sk_c8))
| multiply(sk_c2,sk_c9) = sk_c3 ),
inference(paramod,[status(thm)],[c_3249,c_109]) ).
cnf(c_54342,plain,
( sk_c5 = multiply(sk_c7,inverse(sk_c8))
| multiply(sk_c2,sk_c9) = sk_c3 ),
inference(paramod,[status(thm)],[c_2353,c_54341]) ).
cnf(c_14600,plain,
( multiply(sk_c7,inverse(sk_c8)) = sk_c5
| multiply(sk_c2,sk_c9) = sk_c3 ),
inference(copy,[status(thm)],[c_54342]) ).
cnf(c_54343,plain,
( identity = sk_c8
| multiply(sk_c9,sk_c3) = sk_c8
| multiply(sk_c9,sk_c3) = sk_c8 ),
inference(paramod,[status(thm)],[c_3566,c_22]) ).
cnf(c_14991,plain,
( identity = sk_c8
| multiply(sk_c9,sk_c3) = sk_c8 ),
inference(copy,[status(thm)],[c_54343]) ).
cnf(c_54344,plain,
( multiply(sk_c7,sk_c6) = identity
| identity = sk_c9
| multiply(sk_c7,sk_c6) = identity ),
inference(paramod,[status(thm)],[c_3590,c_88]) ).
cnf(c_16532,plain,
( identity = sk_c9
| multiply(sk_c7,sk_c6) = identity ),
inference(copy,[status(thm)],[c_54344]) ).
cnf(c_54345,plain,
( multiply(inverse(sk_c7),identity) = sk_c6
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_16532,c_72]) ).
cnf(c_16535,plain,
( inverse(sk_c7) = sk_c6
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_2353,c_54345]) ).
cnf(c_54346,plain,
( multiply(sk_c8,sk_c5) = identity
| identity = sk_c3
| multiply(sk_c8,sk_c5) = identity ),
inference(paramod,[status(thm)],[c_3592,c_111]) ).
cnf(c_16939,plain,
( identity = sk_c3
| multiply(sk_c8,sk_c5) = identity ),
inference(copy,[status(thm)],[c_54346]) ).
cnf(c_54347,plain,
( multiply(inverse(sk_c8),identity) = sk_c5
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_16939,c_72]) ).
cnf(c_16946,plain,
( inverse(sk_c8) = sk_c5
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_2353,c_54347]) ).
cnf(c_16954,plain,
( inverse(sk_c5) = sk_c8
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_16946,c_3283]) ).
cnf(c_54348,plain,
( multiply(sk_c8,sk_c1) = identity
| identity = sk_c8
| multiply(sk_c8,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_8461,c_91]) ).
cnf(c_17292,plain,
( identity = sk_c8
| multiply(sk_c8,sk_c1) = identity ),
inference(copy,[status(thm)],[c_54348]) ).
cnf(c_54349,plain,
( multiply(inverse(sk_c8),identity) = sk_c1
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_17292,c_72]) ).
cnf(c_17374,plain,
( inverse(sk_c8) = sk_c1
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_2353,c_54349]) ).
cnf(c_17376,plain,
( multiply(sk_c1,sk_c8) = identity
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_17374,c_2]) ).
cnf(c_17378,plain,
( inverse(sk_c1) = sk_c8
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_17374,c_3283]) ).
cnf(c_54350,plain,
( multiply(sk_c8,sk_c9) = sk_c8
| identity = sk_c8
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_17378,c_14174]) ).
cnf(c_17431,plain,
( multiply(sk_c8,sk_c9) = sk_c8
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_54350]) ).
cnf(c_54351,plain,
( identity = sk_c8
| identity = sk_c9
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_17376,c_14165]) ).
cnf(c_17434,plain,
( identity = sk_c9
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_54351]) ).
cnf(c_17504,plain,
( inverse(sk_c8) = identity
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_17434,c_2430]) ).
cnf(c_54352,plain,
( identity = sk_c8
| sk_c8 = sk_c7
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_17431,c_13303]) ).
cnf(c_54353,plain,
( identity = sk_c8
| sk_c7 = sk_c8
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_54352]) ).
cnf(c_18091,plain,
( sk_c7 = sk_c8
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_54353]) ).
cnf(c_54354,plain,
( multiply(sk_c8,sk_c1) = identity
| identity = sk_c7
| multiply(sk_c8,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_8539,c_93]) ).
cnf(c_22447,plain,
( identity = sk_c7
| multiply(sk_c8,sk_c1) = identity ),
inference(copy,[status(thm)],[c_54354]) ).
cnf(c_54355,plain,
( multiply(inverse(sk_c8),identity) = sk_c1
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_22447,c_72]) ).
cnf(c_22460,plain,
( inverse(sk_c8) = sk_c1
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2353,c_54355]) ).
cnf(c_22486,plain,
( multiply(sk_c1,sk_c8) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_22460,c_2]) ).
cnf(c_22488,plain,
( inverse(sk_c1) = sk_c8
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_22460,c_3283]) ).
cnf(c_54356,plain,
( multiply(sk_c8,sk_c9) = sk_c8
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_22488,c_14576]) ).
cnf(c_22563,plain,
( multiply(sk_c8,sk_c9) = sk_c8
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_54356]) ).
cnf(c_54357,plain,
( identity = sk_c7
| identity = sk_c9
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_22486,c_14570]) ).
cnf(c_22566,plain,
( identity = sk_c9
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_54357]) ).
cnf(c_22573,plain,
( inverse(sk_c7) = identity
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_22566,c_2430]) ).
cnf(c_54358,plain,
( identity = sk_c6
| identity = sk_c9
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_22573,c_16535]) ).
cnf(c_22831,plain,
( identity = sk_c6
| identity = sk_c9 ),
inference(copy,[status(thm)],[c_54358]) ).
cnf(c_54359,plain,
( inverse(sk_c8) = sk_c6
| identity = sk_c9
| identity = sk_c9 ),
inference(paramod,[status(thm)],[c_22831,c_17504]) ).
cnf(c_22881,plain,
( inverse(sk_c8) = sk_c6
| identity = sk_c9 ),
inference(copy,[status(thm)],[c_54359]) ).
cnf(c_54360,plain,
( identity = sk_c7
| sk_c8 = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_22563,c_13734]) ).
cnf(c_54361,plain,
( identity = sk_c7
| sk_c7 = sk_c8
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_54360]) ).
cnf(c_24162,plain,
( sk_c7 = sk_c8
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_54361]) ).
cnf(c_54362,plain,
( sk_c7 = sk_c8
| sk_c7 = sk_c8
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_24162,c_18091]) ).
cnf(c_54363,plain,
( sk_c7 = sk_c8
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_54362]) ).
cnf(c_24198,plain,
sk_c7 = sk_c8,
inference(copy,[status(thm)],[c_54363]) ).
cnf(c_54364,plain,
( multiply(sk_c8,inverse(sk_c8)) = sk_c5
| multiply(sk_c2,sk_c9) = sk_c3 ),
inference(paramod,[status(thm)],[c_24198,c_14600]) ).
cnf(c_27992,plain,
( identity = sk_c5
| multiply(sk_c2,sk_c9) = sk_c3 ),
inference(paramod,[status(thm)],[c_3249,c_54364]) ).
cnf(c_54365,plain,
( multiply(A,multiply(inverse(sk_c8),sk_c7)) = multiply(A,sk_c9)
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_24198,c_13745]) ).
cnf(c_54366,plain,
( multiply(A,multiply(inverse(sk_c8),sk_c8)) = multiply(A,sk_c9)
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_24198,c_54365]) ).
cnf(c_54367,plain,
( multiply(A,identity) = multiply(A,sk_c9)
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_2,c_54366]) ).
cnf(c_54368,plain,
( A = multiply(A,sk_c9)
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_2353,c_54367]) ).
cnf(c_28007,plain,
( multiply(A,sk_c9) = A
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_54368]) ).
cnf(c_28400,plain,
( inverse(sk_c6) = multiply(sk_c9,inverse(sk_c8))
| multiply(sk_c8,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_24198,c_13203]) ).
cnf(c_54369,plain,
( multiply(sk_c5,multiply(sk_c8,inverse(sk_c8))) = identity
| multiply(sk_c9,sk_c2) = identity ),
inference(paramod,[status(thm)],[c_24198,c_13165]) ).
cnf(c_54370,plain,
( multiply(sk_c5,identity) = identity
| multiply(sk_c9,sk_c2) = identity ),
inference(paramod,[status(thm)],[c_3249,c_54369]) ).
cnf(c_54371,plain,
( sk_c5 = identity
| multiply(sk_c9,sk_c2) = identity ),
inference(paramod,[status(thm)],[c_2353,c_54370]) ).
cnf(c_28415,plain,
( identity = sk_c5
| multiply(sk_c9,sk_c2) = identity ),
inference(copy,[status(thm)],[c_54371]) ).
cnf(c_29696,plain,
( multiply(inverse(sk_c8),multiply(sk_c6,sk_c9)) = identity
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_24198,c_10405]) ).
cnf(c_54372,plain,
( inverse(sk_c8) != sk_c7
| inverse(C) != sk_c8
| multiply(C,sk_c8) != sk_c7
| multiply(B,sk_c9) != sk_c8
| inverse(B) != sk_c9
| multiply(B,sk_c9) != A
| multiply(sk_c9,A) != sk_c8
| identity != sk_c9
| multiply(sk_c8,sk_c9) != sk_c8 ),
inference(paramod,[status(thm)],[c_24198,c_3384]) ).
cnf(c_54373,plain,
( inverse(sk_c8) != sk_c7
| inverse(C) != sk_c8
| multiply(C,sk_c8) != sk_c8
| multiply(B,sk_c9) != sk_c8
| inverse(B) != sk_c9
| multiply(B,sk_c9) != A
| multiply(sk_c9,A) != sk_c8
| identity != sk_c9
| multiply(sk_c8,sk_c9) != sk_c8 ),
inference(paramod,[status(thm)],[c_24198,c_54372]) ).
cnf(c_33250,plain,
( inverse(sk_c8) != sk_c8
| inverse(C) != sk_c8
| multiply(C,sk_c8) != sk_c8
| multiply(B,sk_c9) != sk_c8
| inverse(B) != sk_c9
| multiply(B,sk_c9) != A
| multiply(sk_c9,A) != sk_c8
| identity != sk_c9
| multiply(sk_c8,sk_c9) != sk_c8 ),
inference(paramod,[status(thm)],[c_24198,c_54373]) ).
cnf(c_39825,plain,
( inverse(sk_c8) != sk_c8
| inverse(B) != sk_c8
| multiply(B,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c9
| multiply(sk_c8,sk_c9) != A
| multiply(sk_c9,A) != sk_c8
| identity != sk_c9
| multiply(sk_c8,sk_c9) != sk_c8 ),
inference(factor,[status(thm)],[c_33250]) ).
cnf(c_41855,plain,
( inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c9
| multiply(sk_c8,sk_c9) != A
| multiply(sk_c9,A) != sk_c8
| identity != sk_c9
| multiply(sk_c8,sk_c9) != sk_c8 ),
inference(factor,[status(thm)],[c_39825]) ).
cnf(c_42769,plain,
( inverse(sk_c9) = identity
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_28007,c_2]) ).
cnf(c_54374,plain,
( multiply(inverse(sk_c9),identity) = sk_c2
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_28415,c_72]) ).
cnf(c_43099,plain,
( inverse(sk_c9) = sk_c2
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_2353,c_54374]) ).
cnf(c_43116,plain,
( multiply(sk_c2,sk_c9) = identity
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_43099,c_2]) ).
cnf(c_54375,plain,
( identity = sk_c5
| identity = sk_c3
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_43116,c_27992]) ).
cnf(c_46080,plain,
( identity = sk_c3
| identity = sk_c5 ),
inference(copy,[status(thm)],[c_54375]) ).
cnf(c_46089,plain,
( inverse(sk_c5) = identity
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_46080,c_2430]) ).
cnf(c_54376,plain,
( identity = sk_c8
| identity = sk_c3
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_46089,c_16954]) ).
cnf(c_46124,plain,
( identity = sk_c8
| identity = sk_c3 ),
inference(copy,[status(thm)],[c_54376]) ).
cnf(c_54377,plain,
( inverse(sk_c9) = sk_c3
| identity = sk_c8
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_46124,c_42769]) ).
cnf(c_46272,plain,
( inverse(sk_c9) = sk_c3
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_54377]) ).
cnf(c_46656,plain,
( multiply(sk_c9,sk_c3) = identity
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_46272,c_3249]) ).
cnf(c_54378,plain,
( inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c9
| multiply(sk_c8,sk_c9) != multiply(inverse(sk_c9),A)
| A != sk_c8
| identity != sk_c9
| multiply(sk_c8,sk_c9) != sk_c8 ),
inference(paramod,[status(thm)],[c_3282,c_41855]) ).
cnf(c_54379,plain,
( inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c9
| multiply(sk_c8,sk_c9) != multiply(inverse(sk_c9),A)
| sk_c8 != A
| identity != sk_c9
| multiply(sk_c8,sk_c9) != sk_c8 ),
inference(copy,[status(thm)],[c_54378]) ).
cnf(c_47109,plain,
( inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c9
| multiply(inverse(sk_c9),A) != multiply(sk_c8,sk_c9)
| sk_c8 != A
| identity != sk_c9
| multiply(sk_c8,sk_c9) != sk_c8 ),
inference(copy,[status(thm)],[c_54379]) ).
cnf(c_54380,plain,
( identity = sk_c8
| identity = sk_c8
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_46656,c_14991]) ).
cnf(c_54381,plain,
( identity = sk_c8
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_54380]) ).
cnf(c_48381,plain,
identity = sk_c8,
inference(copy,[status(thm)],[c_54381]) ).
cnf(c_48935,plain,
( inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c9
| multiply(inverse(sk_c9),A) != multiply(sk_c8,sk_c9)
| sk_c8 != A
| sk_c8 != sk_c9
| multiply(sk_c8,sk_c9) != sk_c8 ),
inference(paramod,[status(thm)],[c_48381,c_47109]) ).
cnf(c_52408,plain,
( multiply(inverse(sk_c8),multiply(sk_c6,sk_c9)) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_48381,c_29696]) ).
cnf(c_52760,plain,
( inverse(sk_c6) = multiply(sk_c9,inverse(sk_c8))
| multiply(sk_c8,sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_48381,c_28400]) ).
cnf(c_54002,plain,
( inverse(sk_c8) = sk_c6
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_48381,c_22881]) ).
cnf(c_54382,plain,
inverse(sk_c8) = identity,
inference(paramod,[status(thm)],[c_48381,c_2430]) ).
cnf(c_54285,plain,
inverse(sk_c8) = sk_c8,
inference(paramod,[status(thm)],[c_48381,c_54382]) ).
cnf(c_54286,plain,
multiply(A,sk_c8) = A,
inference(paramod,[status(thm)],[c_48381,c_2353]) ).
cnf(c_54297,plain,
multiply(inverse(A),A) = sk_c8,
inference(paramod,[status(thm)],[c_48381,c_2]) ).
cnf(c_54298,plain,
multiply(sk_c8,A) = A,
inference(paramod,[status(thm)],[c_48381,c_1]) ).
cnf(c_54383,plain,
( inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c9
| multiply(inverse(sk_c9),sk_c9) != multiply(sk_c8,sk_c9)
| sk_c8 != sk_c9
| multiply(sk_c8,sk_c9) != sk_c8 ),
inference(factor,[status(thm)],[c_48935]) ).
cnf(c_54384,plain,
( inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c9
| multiply(inverse(sk_c9),sk_c9) != multiply(sk_c8,sk_c9)
| sk_c8 != sk_c9
| sk_c9 != sk_c8 ),
inference(paramod,[status(thm)],[c_54298,c_54383]) ).
cnf(c_54385,plain,
( inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c9
| sk_c8 != multiply(sk_c8,sk_c9)
| sk_c8 != sk_c9
| sk_c9 != sk_c8 ),
inference(paramod,[status(thm)],[c_54297,c_54384]) ).
cnf(c_54386,plain,
( inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| inverse(sk_c8) != sk_c9
| sk_c8 != sk_c9
| sk_c8 != sk_c9
| sk_c9 != sk_c8 ),
inference(paramod,[status(thm)],[c_54298,c_54385]) ).
cnf(c_54387,plain,
( inverse(sk_c8) != sk_c8
| multiply(sk_c8,sk_c8) != sk_c8
| sk_c8 != sk_c9
| sk_c8 != sk_c9
| sk_c8 != sk_c9
| sk_c9 != sk_c8 ),
inference(paramod,[status(thm)],[c_54285,c_54386]) ).
cnf(c_54388,plain,
( inverse(sk_c8) != sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c9
| sk_c8 != sk_c9
| sk_c8 != sk_c9
| sk_c9 != sk_c8 ),
inference(paramod,[status(thm)],[c_54286,c_54387]) ).
cnf(c_54389,plain,
( sk_c8 != sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c9
| sk_c8 != sk_c9
| sk_c8 != sk_c9
| sk_c9 != sk_c8 ),
inference(paramod,[status(thm)],[c_54285,c_54388]) ).
cnf(c_54390,plain,
( sk_c8 != sk_c8
| sk_c8 != sk_c8
| sk_c8 != sk_c9
| sk_c8 != sk_c9
| sk_c8 != sk_c9
| sk_c8 != sk_c9 ),
inference(copy,[status(thm)],[c_54389]) ).
cnf(c_54391,plain,
( sk_c8 != sk_c8
| sk_c8 != sk_c9
| sk_c8 != sk_c9
| sk_c8 != sk_c9
| sk_c8 != sk_c9 ),
inference(copy,[status(thm)],[c_54390]) ).
cnf(c_54392,plain,
( sk_c8 != sk_c9
| sk_c8 != sk_c9
| sk_c8 != sk_c9
| sk_c8 != sk_c9 ),
inference(copy,[status(thm)],[c_54391]) ).
cnf(c_54393,plain,
( sk_c8 != sk_c9
| sk_c8 != sk_c9
| sk_c8 != sk_c9 ),
inference(copy,[status(thm)],[c_54392]) ).
cnf(c_54394,plain,
( sk_c8 != sk_c9
| sk_c8 != sk_c9 ),
inference(copy,[status(thm)],[c_54393]) ).
cnf(c_54304,plain,
sk_c8 != sk_c9,
inference(copy,[status(thm)],[c_54394]) ).
cnf(c_54395,plain,
( sk_c8 = sk_c6
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_54285,c_54002]) ).
cnf(c_54396,plain,
( sk_c6 = sk_c8
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_54395]) ).
cnf(c_54315,plain,
sk_c6 = sk_c8,
inference(resolve,[status(thm)],[c_54304,c_54396]) ).
cnf(c_54397,plain,
( inverse(sk_c6) = multiply(sk_c9,inverse(sk_c8))
| sk_c1 = sk_c8 ),
inference(paramod,[status(thm)],[c_54298,c_52760]) ).
cnf(c_54398,plain,
( inverse(sk_c8) = multiply(sk_c9,inverse(sk_c8))
| sk_c1 = sk_c8 ),
inference(paramod,[status(thm)],[c_54315,c_54397]) ).
cnf(c_54399,plain,
( sk_c8 = multiply(sk_c9,inverse(sk_c8))
| sk_c1 = sk_c8 ),
inference(paramod,[status(thm)],[c_54285,c_54398]) ).
cnf(c_54400,plain,
( sk_c8 = multiply(sk_c9,sk_c8)
| sk_c1 = sk_c8 ),
inference(paramod,[status(thm)],[c_54285,c_54399]) ).
cnf(c_54401,plain,
( sk_c8 = sk_c9
| sk_c1 = sk_c8 ),
inference(paramod,[status(thm)],[c_54286,c_54400]) ).
cnf(c_54322,plain,
sk_c1 = sk_c8,
inference(resolve,[status(thm)],[c_54304,c_54401]) ).
cnf(c_54402,plain,
( multiply(inverse(sk_c8),multiply(sk_c6,sk_c9)) = sk_c8
| multiply(sk_c8,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_54322,c_52408]) ).
cnf(c_54403,plain,
( multiply(inverse(sk_c8),multiply(sk_c6,sk_c9)) = sk_c8
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_54286,c_54402]) ).
cnf(c_54404,plain,
( multiply(sk_c8,multiply(sk_c6,sk_c9)) = sk_c8
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_54285,c_54403]) ).
cnf(c_54405,plain,
( multiply(sk_c8,multiply(sk_c8,sk_c9)) = sk_c8
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_54315,c_54404]) ).
cnf(c_54406,plain,
( multiply(sk_c8,sk_c9) = sk_c8
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_54298,c_54405]) ).
cnf(c_54407,plain,
( sk_c9 = sk_c8
| sk_c8 = sk_c9 ),
inference(paramod,[status(thm)],[c_54298,c_54406]) ).
cnf(c_54408,plain,
( sk_c8 = sk_c9
| sk_c8 = sk_c9 ),
inference(copy,[status(thm)],[c_54407]) ).
cnf(c_54409,plain,
sk_c8 = sk_c9,
inference(copy,[status(thm)],[c_54408]) ).
cnf(c_54324,plain,
$false,
inference(resolve,[status(thm)],[c_54304,c_54409]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP319-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/10.44 % Computer : n020.cluster.edu
% 0.16/10.44 % Model : x86_64 x86_64
% 0.16/10.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/10.44 % Memory : 8046.5625MB
% 0.16/10.44 % OS : Linux 6.8.0-71-generic
% 0.16/10.44 % CPULimit : 300
% 0.16/10.44 % WCLimit : 300
% 0.16/10.44 % DateTime : Fri Sep 25 14:46:29 UTC 2026
% 0.16/10.44 % CPUTime :
% 0.16/10.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/10.44 % Process 3168848 was started by sandbox on n020,
% 0.16/10.44 % Fri Sep 25 14:46:29 2026
% 0.16/10.44 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.16/10.45
% 0.16/10.45 % From the command line: assign(max_seconds, 300).
% 282.86/69.24
% 282.86/69.24 % given #500 (T,wt=7): 18098 sk_c7 = sk_c8 | inverse(sk_c8) = identity. [para(18091(a,1),2430(a,1,1))].
% 282.86/69.24
% 282.86/69.24 % given #1000 (F,wt=30): 41982 multiply(sk_c8,sk_c9) != sk_c8 | multiply(sk_c8,sk_c8) != sk_c9 | inverse(sk_c8) != sk_c8 | multiply(sk_c9,multiply(sk_c8,sk_c9)) != sk_c8 | inverse(sk_c8) != sk_c9 | multiply(sk_c8,sk_c8) != sk_c8. [factor(40795,c,g)].
% 282.86/69.24
% 282.86/69.24 % SZS status Unsatisfiable for theBenchmark
% 282.86/69.24
% 282.86/69.24 % Proof 1 at 32.25 (+ 3.49) seconds.
% 282.86/69.24 % Length of proof is 127.
% 282.86/69.24 % Level of proof is 25.
% 282.86/69.24 % Maximum clause weight is 55.000.
% 282.86/69.24 % Given clauses 1214.
% 282.86/69.24
% 282.86/69.24 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------