%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP286-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 : n003.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:33 AM UTC 2026
% Result : Unsatisfiable 150.77s 20.64s
% Output : CNFRefutation 150.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 25
% Syntax : Number of formulae : 235 ( 37 unt; 0 def)
% Number of atoms : 593 ( 592 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 546 ( 188 ~; 358 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 103 ( 0 sgn 10 !; 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_c7,sk_c8) = sk_c6
| multiply(sk_c8,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_1) ).
cnf(c_4,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c8,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_1]) ).
fof(prove_this_2,axiom,
( multiply(sk_c3,sk_c7) = sk_c8
| multiply(sk_c8,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_2) ).
cnf(c_5,plain,
( multiply(sk_c3,sk_c7) = sk_c8
| multiply(sk_c8,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_2]) ).
fof(prove_this_3,axiom,
( inverse(sk_c3) = sk_c7
| multiply(sk_c8,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_3) ).
cnf(c_6,plain,
( inverse(sk_c3) = sk_c7
| multiply(sk_c8,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_3]) ).
fof(prove_this_7,axiom,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_7) ).
cnf(c_10,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_7]) ).
fof(prove_this_8,axiom,
( multiply(sk_c3,sk_c7) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_11,plain,
( multiply(sk_c3,sk_c7) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_8]) ).
fof(prove_this_9,axiom,
( inverse(sk_c3) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_9) ).
cnf(c_12,plain,
( inverse(sk_c3) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_9]) ).
fof(prove_this_10,axiom,
( multiply(sk_c8,sk_c5) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_10) ).
cnf(c_13,plain,
( multiply(sk_c8,sk_c5) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_10]) ).
fof(prove_this_11,axiom,
( multiply(sk_c4,sk_c8) = sk_c5
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_11) ).
cnf(c_14,plain,
( multiply(sk_c4,sk_c8) = sk_c5
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_11]) ).
fof(prove_this_12,axiom,
( inverse(sk_c4) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_12) ).
cnf(c_15,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_12]) ).
fof(prove_this_13,axiom,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_13) ).
cnf(c_16,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_13]) ).
fof(prove_this_14,axiom,
( multiply(sk_c3,sk_c7) = sk_c8
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_14) ).
cnf(c_17,plain,
( multiply(sk_c3,sk_c7) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_14]) ).
fof(prove_this_15,axiom,
( inverse(sk_c3) = sk_c7
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_15) ).
cnf(c_18,plain,
( inverse(sk_c3) = sk_c7
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_15]) ).
fof(prove_this_16,axiom,
( multiply(sk_c8,sk_c5) = sk_c7
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_16) ).
cnf(c_19,plain,
( multiply(sk_c8,sk_c5) = sk_c7
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_16]) ).
fof(prove_this_17,axiom,
( multiply(sk_c4,sk_c8) = sk_c5
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_17) ).
cnf(c_20,plain,
( multiply(sk_c4,sk_c8) = sk_c5
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_17]) ).
fof(prove_this_18,axiom,
( inverse(sk_c4) = sk_c8
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_18) ).
cnf(c_21,plain,
( inverse(sk_c4) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_18]) ).
fof(prove_this_19,axiom,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c2,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_19) ).
cnf(c_22,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c2,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_19]) ).
fof(prove_this_20,axiom,
( multiply(sk_c3,sk_c7) = sk_c8
| multiply(sk_c2,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_20) ).
cnf(c_23,plain,
( multiply(sk_c3,sk_c7) = sk_c8
| multiply(sk_c2,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_20]) ).
fof(prove_this_21,axiom,
( inverse(sk_c3) = sk_c7
| multiply(sk_c2,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_21) ).
cnf(c_24,plain,
( inverse(sk_c3) = sk_c7
| multiply(sk_c2,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_21]) ).
fof(prove_this_25,axiom,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c2) = sk_c7 ),
file('theBenchmark.p',prove_this_25) ).
cnf(c_28,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c2) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_25]) ).
fof(prove_this_26,axiom,
( multiply(sk_c3,sk_c7) = sk_c8
| inverse(sk_c2) = sk_c7 ),
file('theBenchmark.p',prove_this_26) ).
cnf(c_29,plain,
( multiply(sk_c3,sk_c7) = sk_c8
| inverse(sk_c2) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_26]) ).
fof(prove_this_27,axiom,
( inverse(sk_c3) = sk_c7
| inverse(sk_c2) = sk_c7 ),
file('theBenchmark.p',prove_this_27) ).
cnf(c_30,plain,
( inverse(sk_c3) = sk_c7
| inverse(sk_c2) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_27]) ).
fof(prove_this_31,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( inverse(VAR_4) != sk_c8
| multiply(VAR_4,sk_c8) != VAR_3
| multiply(sk_c8,VAR_3) != sk_c7
| inverse(VAR_2) != sk_c7
| multiply(VAR_2,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(VAR_1) != sk_c7
| multiply(VAR_1,sk_c7) != sk_c6
| inverse(VAR_0) != sk_c8
| multiply(VAR_0,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
file('theBenchmark.p',prove_this_31) ).
cnf(c_34,plain,
( inverse(E) != sk_c8
| multiply(E,sk_c8) != D
| multiply(sk_c8,D) != sk_c7
| inverse(C) != sk_c7
| multiply(C,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(B) != sk_c7
| multiply(B,sk_c7) != sk_c6
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(clausify,[status(thm)],[prove_this_31]) ).
cnf(c_38,plain,
( multiply(A,sk_c8) != D
| multiply(sk_c8,D) != sk_c7
| inverse(C) != sk_c7
| multiply(C,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(B) != sk_c7
| multiply(B,sk_c7) != sk_c6
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(factor,[status(thm)],[c_34]) ).
cnf(c_49,plain,
( multiply(A,sk_c8) != C
| multiply(sk_c8,C) != sk_c7
| multiply(B,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(B) != sk_c7
| multiply(B,sk_c7) != sk_c6
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(factor,[status(thm)],[c_38]) ).
cnf(c_35084,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_35085,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_35084]) ).
cnf(c_62,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_35085]) ).
cnf(c_63,plain,
( multiply(sk_c6,A) = multiply(sk_c8,multiply(sk_c7,A))
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_4,c_3]) ).
cnf(c_77,plain,
( multiply(sk_c7,sk_c3) = identity
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_12,c_2]) ).
cnf(c_84,plain,
( multiply(sk_c8,sk_c1) = identity
| multiply(sk_c3,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_17,c_2]) ).
cnf(c_85,plain,
( multiply(sk_c7,sk_c3) = identity
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_87,plain,
( multiply(sk_c8,sk_c1) = identity
| multiply(sk_c4,sk_c8) = sk_c5 ),
inference(paramod,[status(thm)],[c_20,c_2]) ).
cnf(c_35086,plain,
( multiply(multiply(A,sk_c3),sk_c7) = multiply(A,sk_c8)
| multiply(sk_c2,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_23,c_3]) ).
cnf(c_92,plain,
( multiply(A,multiply(sk_c3,sk_c7)) = multiply(A,sk_c8)
| multiply(sk_c2,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_3,c_35086]) ).
cnf(c_93,plain,
( multiply(sk_c7,sk_c3) = identity
| multiply(sk_c2,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_24,c_2]) ).
cnf(c_101,plain,
( multiply(sk_c7,sk_c3) = identity
| inverse(sk_c2) = sk_c7 ),
inference(paramod,[status(thm)],[c_30,c_2]) ).
cnf(c_970,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_62]) ).
cnf(c_1002,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_62,c_62]) ).
cnf(c_1003,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_1002,c_970]) ).
cnf(c_1012,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_1003,c_2]) ).
cnf(c_1190,plain,
( multiply(inverse(sk_c6),multiply(sk_c8,multiply(sk_c7,A))) = A
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_63,c_62]) ).
cnf(c_1307,plain,
multiply(A,inverse(A)) = identity,
inference(paramod,[status(thm)],[c_1002,c_2]) ).
cnf(c_35087,plain,
multiply(A,identity) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_1002,c_1003]) ).
cnf(c_35088,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_1003,c_35087]) ).
cnf(c_1335,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_35088]) ).
cnf(c_35089,plain,
( multiply(A,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| multiply(inverse(sk_c7),sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(inverse(sk_c7),sk_c7) != sk_c6
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(resolve,[status(thm)],[c_1335,c_49]) ).
cnf(c_35090,plain,
( multiply(A,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| multiply(inverse(sk_c7),sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| identity != sk_c6
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_2,c_35089]) ).
cnf(c_1369,plain,
( multiply(A,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| identity != sk_c6
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_2,c_35090]) ).
cnf(c_1409,plain,
( inverse(sk_c7) = sk_c2
| multiply(sk_c3,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_29,c_1335]) ).
cnf(c_35091,plain,
identity = multiply(A,multiply(B,inverse(multiply(A,B)))),
inference(paramod,[status(thm)],[c_1307,c_3]) ).
cnf(c_1493,plain,
multiply(A,multiply(B,inverse(multiply(A,B)))) = identity,
inference(copy,[status(thm)],[c_35091]) ).
cnf(c_1494,plain,
( multiply(sk_c3,sk_c7) = identity
| multiply(sk_c8,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_6,c_1307]) ).
cnf(c_1496,plain,
( multiply(sk_c3,sk_c7) = identity
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_12,c_1307]) ).
cnf(c_1497,plain,
( multiply(sk_c4,sk_c8) = identity
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_15,c_1307]) ).
cnf(c_1498,plain,
( multiply(sk_c1,sk_c8) = identity
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_16,c_1307]) ).
cnf(c_1500,plain,
( multiply(sk_c3,sk_c7) = identity
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_18,c_1307]) ).
cnf(c_1501,plain,
( multiply(sk_c1,sk_c8) = identity
| multiply(sk_c8,sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_19,c_1307]) ).
cnf(c_1503,plain,
( multiply(sk_c4,sk_c8) = identity
| inverse(sk_c1) = sk_c8 ),
inference(paramod,[status(thm)],[c_21,c_1307]) ).
cnf(c_1506,plain,
( multiply(sk_c2,sk_c7) = identity
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_28,c_1307]) ).
cnf(c_1520,plain,
( multiply(sk_c1,sk_c8) = identity
| multiply(sk_c7,sk_c3) = identity ),
inference(paramod,[status(thm)],[c_85,c_1307]) ).
cnf(c_1524,plain,
( multiply(sk_c2,sk_c7) = identity
| multiply(sk_c7,sk_c3) = identity ),
inference(paramod,[status(thm)],[c_101,c_1307]) ).
cnf(c_3454,plain,
( multiply(sk_c8,sk_c1) = identity
| multiply(sk_c3,sk_c7) = identity ),
inference(paramod,[status(thm)],[c_1500,c_2]) ).
cnf(c_3598,plain,
( multiply(sk_c8,sk_c1) = identity
| multiply(sk_c4,sk_c8) = identity ),
inference(paramod,[status(thm)],[c_1503,c_2]) ).
cnf(c_35092,plain,
multiply(inverse(A),identity) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_1493,c_62]) ).
cnf(c_35093,plain,
inverse(A) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_1003,c_35092]) ).
cnf(c_6493,plain,
multiply(A,inverse(multiply(B,A))) = inverse(B),
inference(copy,[status(thm)],[c_35093]) ).
cnf(c_35094,plain,
multiply(inverse(A),inverse(B)) = inverse(multiply(B,A)),
inference(paramod,[status(thm)],[c_6493,c_62]) ).
cnf(c_6547,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_35094]) ).
cnf(c_35095,plain,
( identity = sk_c8
| multiply(sk_c8,sk_c7) = sk_c6
| multiply(sk_c8,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_1494,c_5]) ).
cnf(c_6805,plain,
( identity = sk_c8
| multiply(sk_c8,sk_c7) = sk_c6 ),
inference(copy,[status(thm)],[c_35095]) ).
cnf(c_35096,plain,
( identity = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_1496,c_11]) ).
cnf(c_7085,plain,
( identity = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(copy,[status(thm)],[c_35096]) ).
cnf(c_7097,plain,
( multiply(inverse(sk_c1),sk_c7) = sk_c8
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_7085,c_62]) ).
cnf(c_35097,plain,
( identity = sk_c5
| multiply(sk_c1,sk_c8) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_1497,c_14]) ).
cnf(c_7259,plain,
( identity = sk_c5
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(copy,[status(thm)],[c_35097]) ).
cnf(c_35098,plain,
( multiply(inverse(multiply(sk_c3,sk_c7)),sk_c8) = identity
| multiply(sk_c2,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_92,c_2]) ).
cnf(c_35099,plain,
( multiply(multiply(inverse(sk_c7),inverse(sk_c3)),sk_c8) = identity
| multiply(sk_c2,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_6547,c_35098]) ).
cnf(c_7302,plain,
( multiply(inverse(sk_c7),multiply(inverse(sk_c3),sk_c8)) = identity
| multiply(sk_c2,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_3,c_35099]) ).
cnf(c_35100,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| identity = sk_c7
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_1498,c_10]) ).
cnf(c_7380,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_35100]) ).
cnf(c_7392,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c8
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_7380,c_62]) ).
cnf(c_35101,plain,
( multiply(sk_c8,sk_c5) = sk_c7
| identity = sk_c7
| multiply(sk_c8,sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_1501,c_13]) ).
cnf(c_7657,plain,
( identity = sk_c7
| multiply(sk_c8,sk_c5) = sk_c7 ),
inference(copy,[status(thm)],[c_35101]) ).
cnf(c_7669,plain,
( multiply(inverse(sk_c8),sk_c7) = sk_c5
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_7657,c_62]) ).
cnf(c_35102,plain,
( multiply(A,multiply(B,sk_c8)) != C
| multiply(sk_c8,C) != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| identity != sk_c6
| inverse(multiply(A,B)) != sk_c8
| multiply(multiply(A,B),sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_3,c_1369]) ).
cnf(c_35103,plain,
( multiply(A,multiply(B,sk_c8)) != C
| multiply(sk_c8,C) != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| identity != sk_c6
| inverse(multiply(A,B)) != sk_c8
| multiply(A,multiply(B,sk_c8)) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_3,c_35102]) ).
cnf(c_7849,plain,
( multiply(A,multiply(B,sk_c8)) != C
| multiply(sk_c8,C) != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| identity != sk_c6
| multiply(inverse(B),inverse(A)) != sk_c8
| multiply(A,multiply(B,sk_c8)) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_6547,c_35103]) ).
cnf(c_7909,plain,
( multiply(sk_c8,sk_c7) != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| identity != sk_c6
| multiply(inverse(B),inverse(A)) != sk_c8
| multiply(A,multiply(B,sk_c8)) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(factor,[status(thm)],[c_7849]) ).
cnf(c_35104,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| identity = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_1506,c_22]) ).
cnf(c_8211,plain,
( identity = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_35104]) ).
cnf(c_8223,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c8
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_8211,c_62]) ).
cnf(c_35105,plain,
( multiply(sk_c7,sk_c3) = identity
| identity = sk_c7
| multiply(sk_c7,sk_c3) = identity ),
inference(paramod,[status(thm)],[c_1520,c_77]) ).
cnf(c_8798,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c3) = identity ),
inference(copy,[status(thm)],[c_35105]) ).
cnf(c_35106,plain,
( multiply(inverse(sk_c7),identity) = sk_c3
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_8798,c_62]) ).
cnf(c_8805,plain,
( inverse(sk_c7) = sk_c3
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_1003,c_35106]) ).
cnf(c_8925,plain,
( multiply(sk_c8,sk_c7) != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| identity != sk_c6
| multiply(B,inverse(A)) != sk_c8
| multiply(A,multiply(inverse(B),sk_c8)) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_1335,c_7909]) ).
cnf(c_9141,plain,
( inverse(sk_c3) = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_8805,c_1335]) ).
cnf(c_35107,plain,
( multiply(sk_c3,sk_c6) = sk_c8
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_8805,c_7392]) ).
cnf(c_9160,plain,
( multiply(sk_c3,sk_c6) = sk_c8
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_35107]) ).
cnf(c_9217,plain,
( multiply(inverse(sk_c3),sk_c8) = sk_c6
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_9160,c_62]) ).
cnf(c_9527,plain,
( multiply(sk_c8,sk_c7) != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| identity != sk_c6
| multiply(B,A) != sk_c8
| multiply(inverse(A),multiply(inverse(B),sk_c8)) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_1335,c_8925]) ).
cnf(c_35108,plain,
( multiply(sk_c7,sk_c3) = identity
| identity = sk_c6
| multiply(sk_c7,sk_c3) = identity ),
inference(paramod,[status(thm)],[c_1524,c_93]) ).
cnf(c_10120,plain,
( identity = sk_c6
| multiply(sk_c7,sk_c3) = identity ),
inference(copy,[status(thm)],[c_35108]) ).
cnf(c_35109,plain,
( multiply(inverse(sk_c7),identity) = sk_c3
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_10120,c_62]) ).
cnf(c_10124,plain,
( inverse(sk_c7) = sk_c3
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_1003,c_35109]) ).
cnf(c_35110,plain,
( multiply(sk_c8,sk_c1) = identity
| identity = sk_c8
| multiply(sk_c8,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_3454,c_84]) ).
cnf(c_10902,plain,
( identity = sk_c8
| multiply(sk_c8,sk_c1) = identity ),
inference(copy,[status(thm)],[c_35110]) ).
cnf(c_35111,plain,
( multiply(inverse(sk_c8),identity) = sk_c1
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_10902,c_62]) ).
cnf(c_10906,plain,
( inverse(sk_c8) = sk_c1
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_1003,c_35111]) ).
cnf(c_11112,plain,
( multiply(sk_c1,sk_c8) = identity
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_10906,c_2]) ).
cnf(c_11128,plain,
( inverse(sk_c1) = sk_c8
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_10906,c_1335]) ).
cnf(c_35112,plain,
( multiply(sk_c8,sk_c7) = sk_c8
| identity = sk_c8
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_11128,c_7097]) ).
cnf(c_11215,plain,
( multiply(sk_c8,sk_c7) = sk_c8
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_35112]) ).
cnf(c_35113,plain,
( identity = sk_c8
| identity = sk_c7
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_11112,c_7085]) ).
cnf(c_11223,plain,
( identity = sk_c7
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_35113]) ).
cnf(c_11225,plain,
( multiply(A,sk_c8) = A
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_11223,c_1003]) ).
cnf(c_11226,plain,
( inverse(sk_c8) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_11223,c_1012]) ).
cnf(c_35114,plain,
( multiply(identity,sk_c7) = sk_c5
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_11226,c_7669]) ).
cnf(c_35115,plain,
( sk_c7 = sk_c5
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_1,c_35114]) ).
cnf(c_35116,plain,
( sk_c5 = sk_c7
| identity = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_35115]) ).
cnf(c_11405,plain,
( sk_c5 = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_35116]) ).
cnf(c_11428,plain,
( inverse(sk_c7) = identity
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_11405,c_1012]) ).
cnf(c_35117,plain,
( multiply(identity,sk_c6) = sk_c8
| identity = sk_c6
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_11428,c_8223]) ).
cnf(c_11772,plain,
( sk_c6 = sk_c8
| identity = sk_c6
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_1,c_35117]) ).
cnf(c_35118,plain,
( identity = sk_c8
| sk_c8 = sk_c6
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_11215,c_6805]) ).
cnf(c_35119,plain,
( identity = sk_c8
| sk_c6 = sk_c8
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_35118]) ).
cnf(c_12311,plain,
( sk_c6 = sk_c8
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_35119]) ).
cnf(c_35120,plain,
( inverse(sk_c3) = sk_c6
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_11225,c_9217]) ).
cnf(c_12762,plain,
( inverse(sk_c3) = sk_c6
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_35120]) ).
cnf(c_12815,plain,
( multiply(sk_c6,sk_c3) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_12762,c_2]) ).
cnf(c_35121,plain,
( multiply(sk_c6,sk_c3) = sk_c8
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_11223,c_12815]) ).
cnf(c_14256,plain,
( multiply(sk_c6,sk_c3) = sk_c8
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_35121]) ).
cnf(c_14364,plain,
( multiply(inverse(sk_c6),sk_c8) = sk_c3
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_14256,c_62]) ).
cnf(c_35122,plain,
( sk_c6 = sk_c8
| sk_c6 = sk_c8
| sk_c6 = sk_c8
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_11772,c_12311]) ).
cnf(c_35123,plain,
( sk_c6 = sk_c8
| sk_c6 = sk_c8
| sk_c5 = sk_c7 ),
inference(copy,[status(thm)],[c_35122]) ).
cnf(c_14445,plain,
( sk_c6 = sk_c8
| sk_c5 = sk_c7 ),
inference(copy,[status(thm)],[c_35123]) ).
cnf(c_35124,plain,
( multiply(sk_c8,sk_c1) = identity
| identity = sk_c5
| multiply(sk_c8,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_3598,c_87]) ).
cnf(c_16864,plain,
( identity = sk_c5
| multiply(sk_c8,sk_c1) = identity ),
inference(copy,[status(thm)],[c_35124]) ).
cnf(c_35125,plain,
( multiply(inverse(sk_c8),identity) = sk_c1
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_16864,c_62]) ).
cnf(c_16886,plain,
( inverse(sk_c8) = sk_c1
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_1003,c_35125]) ).
cnf(c_16927,plain,
( multiply(sk_c1,sk_c8) = identity
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_16886,c_2]) ).
cnf(c_35126,plain,
( identity = sk_c5
| identity = sk_c7
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_16927,c_7259]) ).
cnf(c_17082,plain,
( identity = sk_c7
| identity = sk_c5 ),
inference(copy,[status(thm)],[c_35126]) ).
cnf(c_35127,plain,
( identity = sk_c7
| identity = sk_c7
| sk_c6 = sk_c8 ),
inference(paramod,[status(thm)],[c_14445,c_17082]) ).
cnf(c_17123,plain,
( identity = sk_c7
| sk_c6 = sk_c8 ),
inference(copy,[status(thm)],[c_35127]) ).
cnf(c_17205,plain,
( inverse(sk_c7) = identity
| sk_c6 = sk_c8 ),
inference(paramod,[status(thm)],[c_17123,c_1012]) ).
cnf(c_35128,plain,
( multiply(identity,sk_c6) = sk_c8
| identity = sk_c6
| sk_c6 = sk_c8 ),
inference(paramod,[status(thm)],[c_17205,c_8223]) ).
cnf(c_35129,plain,
( sk_c6 = sk_c8
| identity = sk_c6
| sk_c6 = sk_c8 ),
inference(paramod,[status(thm)],[c_1,c_35128]) ).
cnf(c_17584,plain,
( identity = sk_c6
| sk_c6 = sk_c8 ),
inference(copy,[status(thm)],[c_35129]) ).
cnf(c_35130,plain,
( sk_c6 = sk_c8
| sk_c6 = sk_c8
| sk_c6 = sk_c8 ),
inference(paramod,[status(thm)],[c_17584,c_12311]) ).
cnf(c_35131,plain,
( sk_c6 = sk_c8
| sk_c6 = sk_c8 ),
inference(copy,[status(thm)],[c_35130]) ).
cnf(c_17625,plain,
sk_c6 = sk_c8,
inference(copy,[status(thm)],[c_35131]) ).
cnf(c_35132,plain,
( multiply(inverse(sk_c8),sk_c8) = sk_c3
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_17625,c_14364]) ).
cnf(c_19270,plain,
( identity = sk_c3
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_35132]) ).
cnf(c_21698,plain,
( inverse(sk_c7) = sk_c3
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_17625,c_10124]) ).
cnf(c_35133,plain,
( multiply(sk_c8,sk_c7) != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| identity != sk_c6
| multiply(B,A) != sk_c8
| multiply(inverse(A),multiply(inverse(B),sk_c8)) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c8 ),
inference(paramod,[status(thm)],[c_17625,c_9527]) ).
cnf(c_35134,plain,
( multiply(sk_c8,sk_c7) != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| identity != sk_c8
| multiply(B,A) != sk_c8
| multiply(inverse(A),multiply(inverse(B),sk_c8)) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c8 ),
inference(paramod,[status(thm)],[c_17625,c_35133]) ).
cnf(c_35135,plain,
( multiply(sk_c8,sk_c7) != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c8) != sk_c8
| identity != sk_c8
| multiply(B,A) != sk_c8
| multiply(inverse(A),multiply(inverse(B),sk_c8)) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c8 ),
inference(paramod,[status(thm)],[c_17625,c_35134]) ).
cnf(c_22199,plain,
( multiply(sk_c8,sk_c7) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c8
| identity != sk_c8
| multiply(B,A) != sk_c8
| multiply(inverse(A),multiply(inverse(B),sk_c8)) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c8 ),
inference(copy,[status(thm)],[c_35135]) ).
cnf(c_23637,plain,
( multiply(inverse(sk_c7),multiply(inverse(sk_c3),sk_c8)) = identity
| multiply(sk_c2,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_17625,c_7302]) ).
cnf(c_35136,plain,
( multiply(inverse(sk_c6),multiply(sk_c8,multiply(sk_c7,A))) = A
| multiply(sk_c7,sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_17625,c_1190]) ).
cnf(c_35137,plain,
( multiply(inverse(sk_c8),multiply(sk_c8,multiply(sk_c7,A))) = A
| multiply(sk_c7,sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_17625,c_35136]) ).
cnf(c_26147,plain,
( multiply(sk_c7,A) = A
| multiply(sk_c7,sk_c8) = sk_c8 ),
inference(paramod,[status(thm)],[c_62,c_35137]) ).
cnf(c_26547,plain,
multiply(sk_c7,sk_c8) = sk_c8,
inference(factor,[status(thm)],[c_26147]) ).
cnf(c_35138,plain,
( multiply(sk_c8,sk_c7) != sk_c7
| sk_c8 != sk_c8
| identity != sk_c8
| multiply(B,A) != sk_c8
| multiply(inverse(A),multiply(inverse(B),sk_c8)) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c8 ),
inference(paramod,[status(thm)],[c_26547,c_22199]) ).
cnf(c_29496,plain,
( multiply(sk_c8,sk_c7) != sk_c7
| identity != sk_c8
| multiply(B,A) != sk_c8
| multiply(inverse(A),multiply(inverse(B),sk_c8)) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c8 ),
inference(copy,[status(thm)],[c_35138]) ).
cnf(c_31743,plain,
( inverse(sk_c3) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_19270,c_1012]) ).
cnf(c_35139,plain,
( identity = sk_c7
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_31743,c_9141]) ).
cnf(c_35140,plain,
( identity = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_35139]) ).
cnf(c_32020,plain,
identity = sk_c7,
inference(copy,[status(thm)],[c_35140]) ).
cnf(c_35141,plain,
( multiply(sk_c8,sk_c7) != sk_c7
| sk_c7 != sk_c8
| multiply(B,A) != sk_c8
| multiply(inverse(A),multiply(inverse(B),sk_c8)) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c8 ),
inference(paramod,[status(thm)],[c_32020,c_29496]) ).
cnf(c_33370,plain,
( multiply(sk_c8,sk_c7) != sk_c7
| sk_c8 != sk_c7
| multiply(B,A) != sk_c8
| multiply(inverse(A),multiply(inverse(B),sk_c8)) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c8 ),
inference(copy,[status(thm)],[c_35141]) ).
cnf(c_34529,plain,
( multiply(inverse(sk_c7),multiply(inverse(sk_c3),sk_c8)) = sk_c7
| multiply(sk_c2,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_32020,c_23637]) ).
cnf(c_35142,plain,
( inverse(sk_c7) = sk_c3
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_32020,c_21698]) ).
cnf(c_34563,plain,
( inverse(sk_c7) = sk_c3
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_35142]) ).
cnf(c_35143,plain,
inverse(sk_c7) = identity,
inference(paramod,[status(thm)],[c_32020,c_1012]) ).
cnf(c_34920,plain,
inverse(sk_c7) = sk_c7,
inference(paramod,[status(thm)],[c_32020,c_35143]) ).
cnf(c_34921,plain,
multiply(A,sk_c7) = A,
inference(paramod,[status(thm)],[c_32020,c_1003]) ).
cnf(c_34932,plain,
multiply(inverse(A),A) = sk_c7,
inference(paramod,[status(thm)],[c_32020,c_2]) ).
cnf(c_34933,plain,
multiply(sk_c7,A) = A,
inference(paramod,[status(thm)],[c_32020,c_1]) ).
cnf(c_35144,plain,
( multiply(sk_c8,sk_c7) != sk_c7
| sk_c8 != sk_c7
| multiply(inverse(sk_c7),multiply(inverse(sk_c8),sk_c8)) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c8 ),
inference(factor,[status(thm)],[c_33370]) ).
cnf(c_35145,plain,
( multiply(sk_c8,sk_c7) != sk_c7
| sk_c8 != sk_c7
| multiply(inverse(sk_c7),multiply(inverse(sk_c8),sk_c8)) != sk_c7
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_34921,c_35144]) ).
cnf(c_35146,plain,
( multiply(sk_c8,sk_c7) != sk_c7
| sk_c8 != sk_c7
| multiply(sk_c7,multiply(inverse(sk_c8),sk_c8)) != sk_c7
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_34920,c_35145]) ).
cnf(c_35147,plain,
( multiply(sk_c8,sk_c7) != sk_c7
| sk_c8 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c7
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_34932,c_35146]) ).
cnf(c_35148,plain,
( multiply(sk_c8,sk_c7) != sk_c7
| sk_c8 != sk_c7
| sk_c7 != sk_c7
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_34921,c_35147]) ).
cnf(c_35149,plain,
( sk_c8 != sk_c7
| sk_c8 != sk_c7
| sk_c7 != sk_c7
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_34921,c_35148]) ).
cnf(c_35150,plain,
( sk_c8 != sk_c7
| sk_c8 != sk_c7
| sk_c7 != sk_c7 ),
inference(copy,[status(thm)],[c_35149]) ).
cnf(c_35151,plain,
( sk_c8 != sk_c7
| sk_c8 != sk_c7 ),
inference(copy,[status(thm)],[c_35150]) ).
cnf(c_34970,plain,
sk_c8 != sk_c7,
inference(copy,[status(thm)],[c_35151]) ).
cnf(c_35152,plain,
( sk_c7 = sk_c3
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_34920,c_34563]) ).
cnf(c_35153,plain,
( sk_c3 = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_35152]) ).
cnf(c_35049,plain,
sk_c3 = sk_c7,
inference(resolve,[status(thm)],[c_34970,c_35153]) ).
cnf(c_35154,plain,
( multiply(inverse(sk_c7),multiply(inverse(sk_c3),sk_c8)) = sk_c7
| sk_c2 = sk_c8 ),
inference(paramod,[status(thm)],[c_34921,c_34529]) ).
cnf(c_35155,plain,
( multiply(sk_c7,multiply(inverse(sk_c3),sk_c8)) = sk_c7
| sk_c2 = sk_c8 ),
inference(paramod,[status(thm)],[c_34920,c_35154]) ).
cnf(c_35156,plain,
( multiply(sk_c7,multiply(inverse(sk_c7),sk_c8)) = sk_c7
| sk_c2 = sk_c8 ),
inference(paramod,[status(thm)],[c_35049,c_35155]) ).
cnf(c_35157,plain,
( multiply(sk_c7,multiply(sk_c7,sk_c8)) = sk_c7
| sk_c2 = sk_c8 ),
inference(paramod,[status(thm)],[c_34920,c_35156]) ).
cnf(c_35158,plain,
( multiply(sk_c7,sk_c8) = sk_c7
| sk_c2 = sk_c8 ),
inference(paramod,[status(thm)],[c_34933,c_35157]) ).
cnf(c_35159,plain,
( sk_c8 = sk_c7
| sk_c2 = sk_c8 ),
inference(paramod,[status(thm)],[c_34933,c_35158]) ).
cnf(c_35050,plain,
sk_c2 = sk_c8,
inference(resolve,[status(thm)],[c_34970,c_35159]) ).
cnf(c_35160,plain,
( inverse(sk_c7) = sk_c2
| multiply(sk_c7,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_35049,c_1409]) ).
cnf(c_35161,plain,
( inverse(sk_c7) = sk_c2
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_34921,c_35160]) ).
cnf(c_35162,plain,
( sk_c7 = sk_c2
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_34920,c_35161]) ).
cnf(c_35163,plain,
( sk_c7 = sk_c8
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_35050,c_35162]) ).
cnf(c_35164,plain,
( sk_c7 = sk_c8
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_35163]) ).
cnf(c_35165,plain,
( sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_35164]) ).
cnf(c_35166,plain,
sk_c8 = sk_c7,
inference(copy,[status(thm)],[c_35165]) ).
cnf(c_35083,plain,
$false,
inference(resolve,[status(thm)],[c_34970,c_35166]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP286-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.43 % Computer : n003.cluster.edu
% 0.15/0.43 % Model : x86_64 x86_64
% 0.15/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.43 % Memory : 8046.5625MB
% 0.15/0.43 % OS : Linux 6.8.0-71-generic
% 0.15/0.43 % CPULimit : 300
% 0.15/0.43 % WCLimit : 300
% 0.15/0.43 % DateTime : Fri Sep 25 14:44:22 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/0.43 % Process 426071 was started by sandbox on n003,
% 0.15/0.43 % Fri Sep 25 14:44:22 2026
% 0.15/0.43 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.15/0.44
% 0.15/0.44 % From the command line: assign(max_seconds, 300).
% 150.77/20.64
% 150.77/20.64 % given #500 (T,wt=8): 12818 identity = sk_c7 | multiply(sk_c3,sk_c6) = identity. [para(12762(b,1),1307(a,1,2))].
% 150.77/20.64
% 150.77/20.64 % SZS status Unsatisfiable for theBenchmark
% 150.77/20.64
% 150.77/20.64 % Proof 1 at 17.38 (+ 2.72) seconds.
% 150.77/20.64 % Length of proof is 127.
% 150.77/20.64 % Level of proof is 26.
% 150.77/20.64 % Maximum clause weight is 51.000.
% 150.77/20.64 % Given clauses 806.
% 150.77/20.64
% 150.77/20.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------