%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP295-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 : n017.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:35 AM UTC 2026
% Result : Unsatisfiable 67.70s 9.08s
% Output : CNFRefutation 67.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 68
% Number of leaves : 22
% Syntax : Number of formulae : 211 ( 28 unt; 0 def)
% Number of atoms : 713 ( 712 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 887 ( 385 ~; 502 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 103 ( 0 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(left_identity,axiom,
! [VAR_0] : multiply(identity,VAR_0) = VAR_0,
file('theBenchmark.p',left_identity) ).
cnf(c_1,plain,
multiply(identity,A) = A,
inference(clausify,[status(thm)],[left_identity]) ).
fof(left_inverse,axiom,
! [VAR_0] : multiply(inverse(VAR_0),VAR_0) = identity,
file('theBenchmark.p',left_inverse) ).
cnf(c_2,plain,
multiply(inverse(A),A) = identity,
inference(clausify,[status(thm)],[left_inverse]) ).
fof(associativity,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(multiply(VAR_0,VAR_1),VAR_2) = multiply(VAR_0,multiply(VAR_1,VAR_2)),
file('theBenchmark.p',associativity) ).
cnf(c_3,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(clausify,[status(thm)],[associativity]) ).
fof(prove_this_1,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c7,sk_c6) = sk_c5 ),
file('theBenchmark.p',prove_this_1) ).
cnf(c_4,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c7,sk_c6) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_1]) ).
fof(prove_this_6,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_6) ).
cnf(c_9,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_6]) ).
fof(prove_this_7,axiom,
( inverse(sk_c3) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_7) ).
cnf(c_10,plain,
( inverse(sk_c3) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_7]) ).
fof(prove_this_8,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_11,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_8]) ).
fof(prove_this_9,axiom,
( inverse(sk_c4) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_9) ).
cnf(c_12,plain,
( inverse(sk_c4) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_9]) ).
fof(prove_this_10,axiom,
( multiply(sk_c4,sk_c5) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_10) ).
cnf(c_13,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_10]) ).
fof(prove_this_11,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_11) ).
cnf(c_14,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_11]) ).
fof(prove_this_12,axiom,
( inverse(sk_c3) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_12) ).
cnf(c_15,plain,
( inverse(sk_c3) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_12]) ).
fof(prove_this_13,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_13) ).
cnf(c_16,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_13]) ).
fof(prove_this_14,axiom,
( inverse(sk_c4) = sk_c6
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_14) ).
cnf(c_17,plain,
( inverse(sk_c4) = sk_c6
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_14]) ).
fof(prove_this_15,axiom,
( multiply(sk_c4,sk_c5) = sk_c6
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_15) ).
cnf(c_18,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_15]) ).
fof(prove_this_16,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c7,sk_c5) = sk_c6 ),
file('theBenchmark.p',prove_this_16) ).
cnf(c_19,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_16]) ).
fof(prove_this_21,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c2,sk_c7) = sk_c5 ),
file('theBenchmark.p',prove_this_21) ).
cnf(c_24,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c2,sk_c7) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_21]) ).
fof(prove_this_24,axiom,
( inverse(sk_c4) = sk_c6
| multiply(sk_c2,sk_c7) = sk_c5 ),
file('theBenchmark.p',prove_this_24) ).
cnf(c_27,plain,
( inverse(sk_c4) = sk_c6
| multiply(sk_c2,sk_c7) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_24]) ).
fof(prove_this_25,axiom,
( multiply(sk_c4,sk_c5) = sk_c6
| multiply(sk_c2,sk_c7) = sk_c5 ),
file('theBenchmark.p',prove_this_25) ).
cnf(c_28,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| multiply(sk_c2,sk_c7) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_25]) ).
fof(prove_this_26,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c2) = sk_c7 ),
file('theBenchmark.p',prove_this_26) ).
cnf(c_29,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c2) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_26]) ).
fof(prove_this_29,axiom,
( inverse(sk_c4) = sk_c6
| inverse(sk_c2) = sk_c7 ),
file('theBenchmark.p',prove_this_29) ).
cnf(c_32,plain,
( inverse(sk_c4) = sk_c6
| inverse(sk_c2) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_29]) ).
fof(prove_this_30,axiom,
( multiply(sk_c4,sk_c5) = sk_c6
| inverse(sk_c2) = sk_c7 ),
file('theBenchmark.p',prove_this_30) ).
cnf(c_33,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| inverse(sk_c2) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_30]) ).
fof(prove_this_31,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( multiply(VAR_3,sk_c5) != sk_c6
| inverse(VAR_3) != sk_c6
| multiply(VAR_2,sk_c6) != sk_c7
| inverse(VAR_2) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(VAR_1) != sk_c7
| multiply(VAR_1,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(VAR_0) != sk_c7
| multiply(VAR_0,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
file('theBenchmark.p',prove_this_31) ).
cnf(c_34,plain,
( multiply(D,sk_c5) != sk_c6
| inverse(D) != sk_c6
| multiply(C,sk_c6) != sk_c7
| inverse(C) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(B) != sk_c7
| multiply(B,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(clausify,[status(thm)],[prove_this_31]) ).
cnf(c_38,plain,
( multiply(C,sk_c5) != sk_c6
| inverse(C) != sk_c6
| multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(factor,[status(thm)],[c_34]) ).
cnf(c_39,plain,
( multiply(C,sk_c5) != sk_c6
| inverse(C) != sk_c6
| multiply(B,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(B) != sk_c7
| multiply(B,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(factor,[status(thm)],[c_34]) ).
cnf(c_14349,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_14350,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_14349]) ).
cnf(c_54,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_14350]) ).
cnf(c_14351,plain,
( multiply(multiply(A,sk_c6),sk_c7) = multiply(A,sk_c5)
| multiply(sk_c7,sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_4,c_3]) ).
cnf(c_56,plain,
( multiply(A,multiply(sk_c6,sk_c7)) = multiply(A,sk_c5)
| multiply(sk_c7,sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_3,c_14351]) ).
cnf(c_65,plain,
( multiply(sk_c7,sk_c3) = identity
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_10,c_2]) ).
cnf(c_68,plain,
( multiply(sk_c6,sk_c4) = identity
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_12,c_2]) ).
cnf(c_14352,plain,
( multiply(multiply(A,sk_c6),sk_c7) = multiply(A,sk_c5)
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_19,c_3]) ).
cnf(c_77,plain,
( multiply(A,multiply(sk_c6,sk_c7)) = multiply(A,sk_c5)
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_3,c_14352]) ).
cnf(c_89,plain,
( multiply(sk_c6,sk_c4) = identity
| multiply(sk_c2,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_27,c_2]) ).
cnf(c_578,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_54]) ).
cnf(c_610,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_54,c_54]) ).
cnf(c_611,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_610,c_578]) ).
cnf(c_612,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_611,c_2]) ).
cnf(c_836,plain,
multiply(A,inverse(A)) = identity,
inference(paramod,[status(thm)],[c_610,c_2]) ).
cnf(c_14353,plain,
multiply(A,identity) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_610,c_611]) ).
cnf(c_14354,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_611,c_14353]) ).
cnf(c_856,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_14354]) ).
cnf(c_14355,plain,
( multiply(B,sk_c5) != sk_c6
| inverse(B) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| multiply(inverse(sk_c7),sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(resolve,[status(thm)],[c_856,c_39]) ).
cnf(c_885,plain,
( multiply(B,sk_c5) != sk_c6
| inverse(B) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| identity != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(paramod,[status(thm)],[c_2,c_14355]) ).
cnf(c_886,plain,
( multiply(inverse(sk_c6),sk_c5) != sk_c6
| multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(resolve,[status(thm)],[c_856,c_38]) ).
cnf(c_977,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_14,c_836]) ).
cnf(c_978,plain,
( multiply(sk_c1,sk_c7) = identity
| inverse(sk_c3) = sk_c7 ),
inference(paramod,[status(thm)],[c_15,c_836]) ).
cnf(c_979,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c3,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_16,c_836]) ).
cnf(c_980,plain,
( multiply(sk_c1,sk_c7) = identity
| inverse(sk_c4) = sk_c6 ),
inference(paramod,[status(thm)],[c_17,c_836]) ).
cnf(c_981,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c4,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_18,c_836]) ).
cnf(c_986,plain,
( multiply(sk_c2,sk_c7) = identity
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_29,c_836]) ).
cnf(c_989,plain,
( multiply(sk_c2,sk_c7) = identity
| inverse(sk_c4) = sk_c6 ),
inference(paramod,[status(thm)],[c_32,c_836]) ).
cnf(c_990,plain,
( multiply(sk_c2,sk_c7) = identity
| multiply(sk_c4,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_33,c_836]) ).
cnf(c_2848,plain,
( multiply(sk_c7,sk_c3) = identity
| multiply(sk_c1,sk_c7) = identity ),
inference(paramod,[status(thm)],[c_978,c_2]) ).
cnf(c_2892,plain,
( multiply(sk_c6,sk_c4) = identity
| multiply(sk_c1,sk_c7) = identity ),
inference(paramod,[status(thm)],[c_980,c_2]) ).
cnf(c_3106,plain,
( multiply(sk_c6,sk_c4) = identity
| multiply(sk_c2,sk_c7) = identity ),
inference(paramod,[status(thm)],[c_989,c_2]) ).
cnf(c_14356,plain,
( multiply(B,sk_c5) != sk_c6
| inverse(B) != sk_c6
| multiply(inverse(A),sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| A != sk_c7
| multiply(inverse(A),sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| identity != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(paramod,[status(thm)],[c_856,c_885]) ).
cnf(c_8147,plain,
( multiply(B,sk_c5) != sk_c6
| inverse(B) != sk_c6
| multiply(inverse(A),sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c7 != A
| multiply(inverse(A),sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| identity != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(copy,[status(thm)],[c_14356]) ).
cnf(c_14357,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| identity = sk_c6
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_977,c_9]) ).
cnf(c_8266,plain,
( identity = sk_c6
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_14357]) ).
cnf(c_8438,plain,
( multiply(inverse(sk_c6),sk_c5) = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_8266,c_54]) ).
cnf(c_14358,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| identity = sk_c6
| multiply(sk_c3,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_979,c_11]) ).
cnf(c_8469,plain,
( identity = sk_c6
| multiply(sk_c3,sk_c6) = sk_c7 ),
inference(copy,[status(thm)],[c_14358]) ).
cnf(c_8473,plain,
( multiply(inverse(sk_c3),sk_c7) = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_8469,c_54]) ).
cnf(c_14359,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| identity = sk_c6
| multiply(sk_c4,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_981,c_13]) ).
cnf(c_8694,plain,
( identity = sk_c6
| multiply(sk_c4,sk_c5) = sk_c6 ),
inference(copy,[status(thm)],[c_14359]) ).
cnf(c_14360,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| identity = sk_c5
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_986,c_24]) ).
cnf(c_9034,plain,
( identity = sk_c5
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_14360]) ).
cnf(c_9039,plain,
( multiply(inverse(sk_c6),sk_c5) = sk_c7
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_9034,c_54]) ).
cnf(c_14361,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| identity = sk_c5
| multiply(sk_c4,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_990,c_28]) ).
cnf(c_9305,plain,
( identity = sk_c5
| multiply(sk_c4,sk_c5) = sk_c6 ),
inference(copy,[status(thm)],[c_14361]) ).
cnf(c_9309,plain,
( multiply(inverse(sk_c4),sk_c6) = sk_c5
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_9305,c_54]) ).
cnf(c_14362,plain,
( multiply(A,sk_c5) != sk_c6
| inverse(A) != sk_c6
| identity != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c7 != sk_c6
| multiply(inverse(sk_c6),sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| identity != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(paramod,[status(thm)],[c_2,c_8147]) ).
cnf(c_9755,plain,
( multiply(A,sk_c5) != sk_c6
| inverse(A) != sk_c6
| identity != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c6 != sk_c7
| multiply(inverse(sk_c6),sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| identity != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(copy,[status(thm)],[c_14362]) ).
cnf(c_14363,plain,
( multiply(sk_c7,sk_c3) = identity
| identity = sk_c6
| multiply(sk_c7,sk_c3) = identity ),
inference(paramod,[status(thm)],[c_2848,c_65]) ).
cnf(c_9765,plain,
( identity = sk_c6
| multiply(sk_c7,sk_c3) = identity ),
inference(copy,[status(thm)],[c_14363]) ).
cnf(c_14364,plain,
( multiply(inverse(sk_c7),identity) = sk_c3
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9765,c_54]) ).
cnf(c_9768,plain,
( inverse(sk_c7) = sk_c3
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_611,c_14364]) ).
cnf(c_9779,plain,
( inverse(sk_c3) = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9768,c_856]) ).
cnf(c_14365,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9779,c_8473]) ).
cnf(c_9926,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_14365]) ).
cnf(c_9930,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9926,c_54]) ).
cnf(c_14366,plain,
( multiply(sk_c6,sk_c4) = identity
| identity = sk_c6
| multiply(sk_c6,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_2892,c_68]) ).
cnf(c_10021,plain,
( identity = sk_c6
| multiply(sk_c6,sk_c4) = identity ),
inference(copy,[status(thm)],[c_14366]) ).
cnf(c_14367,plain,
( multiply(inverse(sk_c6),identity) = sk_c4
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_10021,c_54]) ).
cnf(c_10024,plain,
( inverse(sk_c6) = sk_c4
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_611,c_14367]) ).
cnf(c_14368,plain,
( multiply(sk_c4,sk_c5) = sk_c7
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_10024,c_8438]) ).
cnf(c_10075,plain,
( multiply(sk_c4,sk_c5) = sk_c7
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_14368]) ).
cnf(c_14369,plain,
( identity = sk_c6
| sk_c7 = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_10075,c_8694]) ).
cnf(c_14370,plain,
( identity = sk_c6
| sk_c6 = sk_c7
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_14369]) ).
cnf(c_10167,plain,
( sk_c6 = sk_c7
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_14370]) ).
cnf(c_10169,plain,
( multiply(A,sk_c6) = A
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_10167,c_611]) ).
cnf(c_10170,plain,
( inverse(sk_c6) = identity
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_10167,c_612]) ).
cnf(c_14371,plain,
( inverse(sk_c6) = sk_c6
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_10167,c_10170]) ).
cnf(c_10325,plain,
( inverse(sk_c6) = sk_c6
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_14371]) ).
cnf(c_10338,plain,
( multiply(sk_c6,sk_c6) = identity
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_10325,c_2]) ).
cnf(c_14372,plain,
( multiply(sk_c6,sk_c4) = identity
| identity = sk_c5
| multiply(sk_c6,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_3106,c_89]) ).
cnf(c_10909,plain,
( identity = sk_c5
| multiply(sk_c6,sk_c4) = identity ),
inference(copy,[status(thm)],[c_14372]) ).
cnf(c_14373,plain,
( multiply(inverse(sk_c6),identity) = sk_c4
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_10909,c_54]) ).
cnf(c_10913,plain,
( inverse(sk_c6) = sk_c4
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_611,c_14373]) ).
cnf(c_10950,plain,
( inverse(sk_c4) = sk_c6
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_10913,c_856]) ).
cnf(c_14374,plain,
( multiply(sk_c4,sk_c5) = sk_c7
| identity = sk_c5
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_10913,c_9039]) ).
cnf(c_11009,plain,
( multiply(sk_c4,sk_c5) = sk_c7
| identity = sk_c5 ),
inference(copy,[status(thm)],[c_14374]) ).
cnf(c_14375,plain,
( multiply(sk_c6,sk_c6) = sk_c5
| identity = sk_c5
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_10950,c_9309]) ).
cnf(c_11028,plain,
( multiply(sk_c6,sk_c6) = sk_c5
| identity = sk_c5 ),
inference(copy,[status(thm)],[c_14375]) ).
cnf(c_14376,plain,
( identity = sk_c5
| sk_c7 = sk_c6
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_11009,c_9305]) ).
cnf(c_14377,plain,
( identity = sk_c5
| sk_c6 = sk_c7
| identity = sk_c5 ),
inference(copy,[status(thm)],[c_14376]) ).
cnf(c_11041,plain,
( sk_c6 = sk_c7
| identity = sk_c5 ),
inference(copy,[status(thm)],[c_14377]) ).
cnf(c_14378,plain,
( sk_c6 = sk_c7
| sk_c5 = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_11041,c_10167]) ).
cnf(c_11084,plain,
( sk_c5 = sk_c6
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_14378]) ).
cnf(c_14379,plain,
( multiply(sk_c6,sk_c6) = sk_c5
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_11041,c_10338]) ).
cnf(c_11086,plain,
( multiply(sk_c6,sk_c6) = sk_c5
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_14379]) ).
cnf(c_11282,plain,
( multiply(inverse(sk_c6),sk_c5) = sk_c6
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_11028,c_54]) ).
cnf(c_11393,plain,
( multiply(inverse(sk_c6),sk_c5) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_11086,c_54]) ).
cnf(c_11553,plain,
( multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5
| identity = sk_c5 ),
inference(resolve,[status(thm)],[c_11282,c_886]) ).
cnf(c_14380,plain,
( multiply(inverse(sk_c6),multiply(sk_c6,sk_c7)) = sk_c6
| multiply(sk_c7,sk_c6) = sk_c5
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_11393,c_56]) ).
cnf(c_14381,plain,
( sk_c7 = sk_c6
| multiply(sk_c7,sk_c6) = sk_c5
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_54,c_14380]) ).
cnf(c_14382,plain,
( sk_c6 = sk_c7
| multiply(sk_c7,sk_c6) = sk_c5
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_14381]) ).
cnf(c_11624,plain,
( multiply(sk_c7,sk_c6) = sk_c5
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_14382]) ).
cnf(c_14383,plain,
( sk_c5 = sk_c7
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_11624,c_10169]) ).
cnf(c_11641,plain,
( sk_c5 = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_14383]) ).
cnf(c_14384,plain,
( sk_c7 = sk_c6
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_11641,c_11084]) ).
cnf(c_14385,plain,
( sk_c6 = sk_c7
| sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_14384]) ).
cnf(c_14386,plain,
( sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_14385]) ).
cnf(c_11661,plain,
sk_c6 = sk_c7,
inference(copy,[status(thm)],[c_14386]) ).
cnf(c_14387,plain,
( multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6
| multiply(sk_c7,sk_c7) != sk_c5
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_11661,c_11553]) ).
cnf(c_14388,plain,
( multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_11661,c_14387]) ).
cnf(c_14389,plain,
( multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_11661,c_14388]) ).
cnf(c_14390,plain,
( multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| inverse(sk_c6) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_11661,c_14389]) ).
cnf(c_14391,plain,
( multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| inverse(sk_c7) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_11661,c_14390]) ).
cnf(c_14392,plain,
( multiply(B,sk_c7) != sk_c7
| inverse(B) != sk_c7
| inverse(sk_c7) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_11661,c_14391]) ).
cnf(c_11680,plain,
( multiply(B,sk_c7) != sk_c7
| inverse(B) != sk_c7
| inverse(sk_c7) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| identity = sk_c5 ),
inference(copy,[status(thm)],[c_14392]) ).
cnf(c_14393,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_11661,c_9930]) ).
cnf(c_14394,plain,
( multiply(inverse(sk_c7),sk_c7) = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_11661,c_14393]) ).
cnf(c_14395,plain,
( identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_14394]) ).
cnf(c_12090,plain,
identity = sk_c7,
inference(copy,[status(thm)],[c_14395]) ).
cnf(c_14396,plain,
( multiply(A,sk_c5) != sk_c6
| inverse(A) != sk_c6
| identity != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c6 != sk_c7
| multiply(inverse(sk_c6),sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| identity != sk_c6
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(paramod,[status(thm)],[c_11661,c_9755]) ).
cnf(c_14397,plain,
( multiply(A,sk_c5) != sk_c6
| inverse(A) != sk_c6
| identity != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c6 != sk_c7
| multiply(inverse(sk_c6),sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| sk_c7 != sk_c6
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(paramod,[status(thm)],[c_12090,c_14396]) ).
cnf(c_14398,plain,
( multiply(A,sk_c5) != sk_c6
| inverse(A) != sk_c6
| identity != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c6 != sk_c7
| multiply(inverse(sk_c6),sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(paramod,[status(thm)],[c_11661,c_14397]) ).
cnf(c_14399,plain,
( multiply(A,sk_c5) != sk_c6
| inverse(A) != sk_c6
| identity != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c6 != sk_c7
| multiply(inverse(sk_c6),sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(paramod,[status(thm)],[c_11661,c_14398]) ).
cnf(c_14400,plain,
( multiply(A,sk_c5) != sk_c6
| inverse(A) != sk_c6
| identity != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c6 != sk_c7
| multiply(inverse(sk_c7),sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(paramod,[status(thm)],[c_11661,c_14399]) ).
cnf(c_14401,plain,
( multiply(A,sk_c5) != sk_c6
| inverse(A) != sk_c6
| identity != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c6 != sk_c7
| identity != sk_c5
| multiply(sk_c7,sk_c5) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(paramod,[status(thm)],[c_2,c_14400]) ).
cnf(c_14402,plain,
( multiply(A,sk_c5) != sk_c6
| inverse(A) != sk_c6
| identity != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c6 != sk_c7
| sk_c7 != sk_c5
| multiply(sk_c7,sk_c5) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(paramod,[status(thm)],[c_12090,c_14401]) ).
cnf(c_14403,plain,
( multiply(A,sk_c5) != sk_c6
| inverse(A) != sk_c6
| identity != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c7 != sk_c7
| sk_c7 != sk_c5
| multiply(sk_c7,sk_c5) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(paramod,[status(thm)],[c_11661,c_14402]) ).
cnf(c_14404,plain,
( multiply(A,sk_c5) != sk_c6
| inverse(A) != sk_c6
| identity != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| sk_c7 != sk_c7
| sk_c7 != sk_c5
| multiply(sk_c7,sk_c5) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(paramod,[status(thm)],[c_11661,c_14403]) ).
cnf(c_14405,plain,
( multiply(A,sk_c5) != sk_c6
| inverse(A) != sk_c6
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| sk_c7 != sk_c7
| sk_c7 != sk_c5
| multiply(sk_c7,sk_c5) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(paramod,[status(thm)],[c_12090,c_14404]) ).
cnf(c_14406,plain,
( multiply(A,sk_c5) != sk_c6
| inverse(A) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| sk_c7 != sk_c7
| sk_c7 != sk_c5
| multiply(sk_c7,sk_c5) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(paramod,[status(thm)],[c_11661,c_14405]) ).
cnf(c_14407,plain,
( multiply(A,sk_c5) != sk_c7
| inverse(A) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| sk_c7 != sk_c7
| sk_c7 != sk_c5
| multiply(sk_c7,sk_c5) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(paramod,[status(thm)],[c_11661,c_14406]) ).
cnf(c_14408,plain,
( multiply(A,sk_c5) != sk_c7
| inverse(A) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| sk_c7 != sk_c7
| sk_c5 != sk_c7
| multiply(sk_c7,sk_c5) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(copy,[status(thm)],[c_14407]) ).
cnf(c_14409,plain,
( multiply(A,sk_c5) != sk_c7
| inverse(A) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| sk_c7 != sk_c7
| sk_c5 != sk_c7
| multiply(sk_c7,sk_c5) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(copy,[status(thm)],[c_14408]) ).
cnf(c_14410,plain,
( multiply(A,sk_c5) != sk_c7
| inverse(A) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| sk_c5 != sk_c7
| multiply(sk_c7,sk_c5) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(copy,[status(thm)],[c_14409]) ).
cnf(c_14411,plain,
( multiply(A,sk_c5) != sk_c7
| inverse(A) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| sk_c5 != sk_c7
| multiply(sk_c7,sk_c5) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(copy,[status(thm)],[c_14410]) ).
cnf(c_12151,plain,
( multiply(A,sk_c5) != sk_c7
| inverse(A) != sk_c7
| sk_c5 != sk_c7
| multiply(sk_c7,sk_c5) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(copy,[status(thm)],[c_14411]) ).
cnf(c_14412,plain,
( multiply(A,multiply(sk_c6,sk_c7)) = multiply(A,sk_c5)
| multiply(sk_c7,sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_11661,c_77]) ).
cnf(c_13988,plain,
( multiply(A,multiply(sk_c7,sk_c7)) = multiply(A,sk_c5)
| multiply(sk_c7,sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_11661,c_14412]) ).
cnf(c_14413,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c7,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_11661,c_4]) ).
cnf(c_14414,plain,
( multiply(sk_c7,sk_c7) = sk_c5
| multiply(sk_c7,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_11661,c_14413]) ).
cnf(c_14015,plain,
multiply(sk_c7,sk_c7) = sk_c5,
inference(copy,[status(thm)],[c_14414]) ).
cnf(c_14415,plain,
( inverse(A) != sk_c7
| inverse(sk_c7) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| identity = sk_c5 ),
inference(factor,[status(thm)],[c_11680]) ).
cnf(c_14416,plain,
( inverse(A) != sk_c7
| inverse(sk_c7) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5
| sk_c7 = sk_c5 ),
inference(paramod,[status(thm)],[c_12090,c_14415]) ).
cnf(c_14417,plain,
( inverse(A) != sk_c7
| inverse(sk_c7) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c7
| sk_c5 != sk_c5
| sk_c7 = sk_c5 ),
inference(paramod,[status(thm)],[c_14015,c_14416]) ).
cnf(c_14418,plain,
( inverse(A) != sk_c7
| inverse(sk_c7) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c7
| sk_c5 != sk_c5
| sk_c5 = sk_c7 ),
inference(copy,[status(thm)],[c_14417]) ).
cnf(c_14419,plain,
( inverse(A) != sk_c7
| inverse(sk_c7) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c7
| sk_c5 = sk_c7 ),
inference(copy,[status(thm)],[c_14418]) ).
cnf(c_14020,plain,
( inverse(sk_c7) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c7
| sk_c5 = sk_c7 ),
inference(copy,[status(thm)],[c_14419]) ).
cnf(c_14420,plain,
inverse(sk_c7) = identity,
inference(paramod,[status(thm)],[c_12090,c_612]) ).
cnf(c_14331,plain,
inverse(sk_c7) = sk_c7,
inference(paramod,[status(thm)],[c_12090,c_14420]) ).
cnf(c_14332,plain,
multiply(A,sk_c7) = A,
inference(paramod,[status(thm)],[c_12090,c_611]) ).
cnf(c_14335,plain,
multiply(sk_c7,A) = A,
inference(paramod,[status(thm)],[c_12090,c_1]) ).
cnf(c_14421,plain,
( inverse(sk_c7) != sk_c7
| sk_c5 != sk_c7
| multiply(sk_c7,sk_c5) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c5 ),
inference(factor,[status(thm)],[c_12151]) ).
cnf(c_14422,plain,
( inverse(sk_c7) != sk_c7
| sk_c5 != sk_c7
| multiply(sk_c7,sk_c5) != sk_c7
| sk_c7 != sk_c5 ),
inference(paramod,[status(thm)],[c_14332,c_14421]) ).
cnf(c_14423,plain,
( inverse(sk_c7) != sk_c7
| sk_c5 != sk_c7
| sk_c5 != sk_c7
| sk_c7 != sk_c5 ),
inference(paramod,[status(thm)],[c_14335,c_14422]) ).
cnf(c_14424,plain,
( sk_c7 != sk_c7
| sk_c5 != sk_c7
| sk_c5 != sk_c7
| sk_c7 != sk_c5 ),
inference(paramod,[status(thm)],[c_14331,c_14423]) ).
cnf(c_14425,plain,
( sk_c7 != sk_c7
| sk_c5 != sk_c7
| sk_c5 != sk_c7
| sk_c5 != sk_c7 ),
inference(copy,[status(thm)],[c_14424]) ).
cnf(c_14426,plain,
( sk_c5 != sk_c7
| sk_c5 != sk_c7
| sk_c5 != sk_c7 ),
inference(copy,[status(thm)],[c_14425]) ).
cnf(c_14427,plain,
( sk_c5 != sk_c7
| sk_c5 != sk_c7 ),
inference(copy,[status(thm)],[c_14426]) ).
cnf(c_14342,plain,
sk_c5 != sk_c7,
inference(copy,[status(thm)],[c_14427]) ).
cnf(c_14428,plain,
( multiply(A,multiply(sk_c7,sk_c7)) = multiply(A,sk_c5)
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_14335,c_13988]) ).
cnf(c_14429,plain,
( multiply(A,sk_c7) = multiply(A,sk_c5)
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_14332,c_14428]) ).
cnf(c_14430,plain,
( A = multiply(A,sk_c5)
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_14332,c_14429]) ).
cnf(c_14431,plain,
( multiply(A,sk_c5) = A
| sk_c5 = sk_c7 ),
inference(copy,[status(thm)],[c_14430]) ).
cnf(c_14343,plain,
multiply(A,sk_c5) = A,
inference(resolve,[status(thm)],[c_14342,c_14431]) ).
cnf(c_14432,plain,
( multiply(sk_c7,sk_c5) != sk_c7
| inverse(sk_c7) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c7
| sk_c5 = sk_c7 ),
inference(factor,[status(thm)],[c_14020]) ).
cnf(c_14433,plain,
( multiply(sk_c7,sk_c5) != sk_c7
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c7
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_14332,c_14432]) ).
cnf(c_14434,plain,
( multiply(sk_c7,sk_c5) != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_14331,c_14433]) ).
cnf(c_14435,plain,
( sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_14343,c_14434]) ).
cnf(c_14436,plain,
( sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c5 = sk_c7 ),
inference(copy,[status(thm)],[c_14435]) ).
cnf(c_14437,plain,
( sk_c7 != sk_c7
| sk_c5 = sk_c7 ),
inference(copy,[status(thm)],[c_14436]) ).
cnf(c_14438,plain,
sk_c5 = sk_c7,
inference(copy,[status(thm)],[c_14437]) ).
cnf(c_14348,plain,
$false,
inference(resolve,[status(thm)],[c_14342,c_14438]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP295-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.45 % Computer : n017.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Fri Sep 25 14:38:47 UTC 2026
% 0.20/0.45 % CPUTime :
% 0.20/0.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.20/0.46 % Process 2513912 was started by sandbox2 on n017,
% 0.20/0.46 % Fri Sep 25 14:38:47 2026
% 0.20/0.46 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.20/0.46
% 0.20/0.46 % From the command line: assign(max_seconds, 300).
% 67.70/9.08
% 67.70/9.08 % given #500 (A,wt=51): 115 multiply(sk_c7,sk_c6) != sk_c5 | multiply(A,sk_c7) != sk_c6 | inverse(A) != sk_c7 | multiply(sk_c7,sk_c5) != sk_c6 | multiply(sk_c1,sk_c7) != sk_c5 | multiply(sk_c6,sk_c7) != sk_c5 | inverse(B) != sk_c7 | multiply(B,sk_c6) != sk_c7 | inverse(C) != sk_c6 | multiply(C,sk_c5) != sk_c6 | inverse(sk_c3) = sk_c7. [resolve(34,f,15,a)].
% 67.70/9.08
% 67.70/9.08 % SZS status Unsatisfiable for theBenchmark
% 67.70/9.08
% 67.70/9.08 % Proof 1 at 7.54 (+ 1.02) seconds.
% 67.70/9.08 % Length of proof is 99.
% 67.70/9.08 % Level of proof is 22.
% 67.70/9.08 % Maximum clause weight is 51.000.
% 67.70/9.08 % Given clauses 535.
% 67.70/9.08
% 67.70/9.08 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------