%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP383-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 : n007.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:45 AM UTC 2026
% Result : Unsatisfiable 66.43s 20.57s
% Output : CNFRefutation 66.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 20
% Syntax : Number of formulae : 205 ( 34 unt; 0 def)
% Number of atoms : 659 ( 658 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 808 ( 354 ~; 454 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 4 avg)
% Maximal term depth : 5 ( 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 : 125 ( 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
| inverse(sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_1) ).
cnf(c_4,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_1]) ).
fof(prove_this_2,axiom,
( inverse(sk_c4) = sk_c8
| inverse(sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_2) ).
cnf(c_5,plain,
( inverse(sk_c4) = sk_c8
| inverse(sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_2]) ).
fof(prove_this_3,axiom,
( multiply(sk_c4,sk_c7) = sk_c8
| inverse(sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_3) ).
cnf(c_6,plain,
( multiply(sk_c4,sk_c7) = sk_c8
| inverse(sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_3]) ).
fof(prove_this_4,axiom,
( inverse(sk_c5) = sk_c7
| inverse(sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_4) ).
cnf(c_7,plain,
( inverse(sk_c5) = sk_c7
| inverse(sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_4]) ).
fof(prove_this_5,axiom,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_5) ).
cnf(c_8,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_5]) ).
fof(prove_this_6,axiom,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c7,sk_c6) = sk_c8 ),
file('theBenchmark.p',prove_this_6) ).
cnf(c_9,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c7,sk_c6) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_6]) ).
fof(prove_this_21,axiom,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c2,sk_c3) = sk_c7 ),
file('theBenchmark.p',prove_this_21) ).
cnf(c_24,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c2,sk_c3) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_21]) ).
fof(prove_this_22,axiom,
( inverse(sk_c4) = sk_c8
| multiply(sk_c2,sk_c3) = sk_c7 ),
file('theBenchmark.p',prove_this_22) ).
cnf(c_25,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c2,sk_c3) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_22]) ).
fof(prove_this_23,axiom,
( multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c2,sk_c3) = sk_c7 ),
file('theBenchmark.p',prove_this_23) ).
cnf(c_26,plain,
( multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c2,sk_c3) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_23]) ).
fof(prove_this_24,axiom,
( inverse(sk_c5) = sk_c7
| multiply(sk_c2,sk_c3) = sk_c7 ),
file('theBenchmark.p',prove_this_24) ).
cnf(c_27,plain,
( inverse(sk_c5) = sk_c7
| multiply(sk_c2,sk_c3) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_24]) ).
fof(prove_this_25,axiom,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c2,sk_c3) = sk_c7 ),
file('theBenchmark.p',prove_this_25) ).
cnf(c_28,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c2,sk_c3) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_25]) ).
fof(prove_this_26,axiom,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c2) = sk_c3 ),
file('theBenchmark.p',prove_this_26) ).
cnf(c_29,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c2) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_26]) ).
fof(prove_this_27,axiom,
( inverse(sk_c4) = sk_c8
| inverse(sk_c2) = sk_c3 ),
file('theBenchmark.p',prove_this_27) ).
cnf(c_30,plain,
( inverse(sk_c4) = sk_c8
| inverse(sk_c2) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_27]) ).
fof(prove_this_28,axiom,
( multiply(sk_c4,sk_c7) = sk_c8
| inverse(sk_c2) = sk_c3 ),
file('theBenchmark.p',prove_this_28) ).
cnf(c_31,plain,
( multiply(sk_c4,sk_c7) = sk_c8
| inverse(sk_c2) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_28]) ).
fof(prove_this_29,axiom,
( inverse(sk_c5) = sk_c7
| inverse(sk_c2) = sk_c3 ),
file('theBenchmark.p',prove_this_29) ).
cnf(c_32,plain,
( inverse(sk_c5) = sk_c7
| inverse(sk_c2) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_29]) ).
fof(prove_this_30,axiom,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c3 ),
file('theBenchmark.p',prove_this_30) ).
cnf(c_33,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_30]) ).
fof(prove_this_36,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( multiply(VAR_4,sk_c6) != sk_c7
| inverse(VAR_4) != sk_c7
| multiply(VAR_3,sk_c7) != sk_c8
| inverse(VAR_3) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(VAR_2,sk_c8) != sk_c7
| inverse(VAR_1) != VAR_2
| multiply(VAR_1,VAR_2) != sk_c7
| multiply(VAR_0,sk_c7) != sk_c8
| inverse(VAR_0) != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
file('theBenchmark.p',prove_this_36) ).
cnf(c_39,plain,
( multiply(E,sk_c6) != sk_c7
| inverse(E) != sk_c7
| multiply(D,sk_c7) != sk_c8
| inverse(D) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(C,sk_c8) != sk_c7
| inverse(B) != C
| multiply(B,C) != sk_c7
| multiply(A,sk_c7) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(clausify,[status(thm)],[prove_this_36]) ).
cnf(c_16295,plain,
( multiply(D,sk_c6) != sk_c7
| inverse(D) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(C,sk_c8) != sk_c7
| inverse(B) != C
| multiply(B,C) != sk_c7
| multiply(A,sk_c7) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_39]) ).
cnf(c_43,plain,
( multiply(D,sk_c6) != sk_c7
| inverse(D) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(C,sk_c8) != sk_c7
| inverse(B) != C
| multiply(B,C) != sk_c7
| multiply(A,sk_c7) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16295]) ).
cnf(c_16296,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_16297,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_16296]) ).
cnf(c_58,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_16297]) ).
cnf(c_59,plain,
( multiply(sk_c7,sk_c8) = identity
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_4,c_2]) ).
cnf(c_60,plain,
( multiply(sk_c8,sk_c4) = identity
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_5,c_2]) ).
cnf(c_16298,plain,
( multiply(sk_c8,A) = multiply(sk_c7,multiply(sk_c6,A))
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_9,c_3]) ).
cnf(c_64,plain,
( multiply(sk_c7,multiply(sk_c6,A)) = multiply(sk_c8,A)
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_16298]) ).
cnf(c_87,plain,
( multiply(sk_c8,sk_c4) = identity
| multiply(sk_c2,sk_c3) = sk_c7 ),
inference(paramod,[status(thm)],[c_25,c_2]) ).
cnf(c_90,plain,
( multiply(sk_c7,sk_c5) = identity
| multiply(sk_c2,sk_c3) = sk_c7 ),
inference(paramod,[status(thm)],[c_27,c_2]) ).
cnf(c_527,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_58]) ).
cnf(c_566,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_58,c_58]) ).
cnf(c_567,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_566,c_527]) ).
cnf(c_618,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_567,c_2]) ).
cnf(c_16299,plain,
( multiply(inverse(sk_c7),identity) = sk_c8
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_59,c_58]) ).
cnf(c_745,plain,
( inverse(sk_c7) = sk_c8
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_567,c_16299]) ).
cnf(c_919,plain,
multiply(A,inverse(A)) = identity,
inference(paramod,[status(thm)],[c_566,c_2]) ).
cnf(c_16300,plain,
multiply(A,identity) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_566,c_567]) ).
cnf(c_16301,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_567,c_16300]) ).
cnf(c_948,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_16301]) ).
cnf(c_988,plain,
( inverse(sk_c7) = sk_c8
| multiply(sk_c4,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_6,c_948]) ).
cnf(c_989,plain,
( inverse(sk_c7) = sk_c5
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_7,c_948]) ).
cnf(c_990,plain,
( inverse(sk_c7) = sk_c8
| multiply(sk_c5,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_8,c_948]) ).
cnf(c_1029,plain,
( inverse(sk_c7) = sk_c8
| multiply(sk_c8,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_60,c_948]) ).
cnf(c_16302,plain,
identity = multiply(A,multiply(B,inverse(multiply(A,B)))),
inference(paramod,[status(thm)],[c_919,c_3]) ).
cnf(c_1050,plain,
multiply(A,multiply(B,inverse(multiply(A,B)))) = identity,
inference(copy,[status(thm)],[c_16302]) ).
cnf(c_1067,plain,
( multiply(sk_c2,sk_c3) = identity
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_29,c_919]) ).
cnf(c_1068,plain,
( multiply(sk_c2,sk_c3) = identity
| inverse(sk_c4) = sk_c8 ),
inference(paramod,[status(thm)],[c_30,c_919]) ).
cnf(c_1069,plain,
( multiply(sk_c2,sk_c3) = identity
| multiply(sk_c4,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_31,c_919]) ).
cnf(c_1070,plain,
( multiply(sk_c2,sk_c3) = identity
| inverse(sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_32,c_919]) ).
cnf(c_1071,plain,
( multiply(sk_c2,sk_c3) = identity
| multiply(sk_c5,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_33,c_919]) ).
cnf(c_1263,plain,
( multiply(sk_c7,multiply(sk_c6,inverse(sk_c8))) = identity
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_919,c_64]) ).
cnf(c_3872,plain,
( multiply(sk_c8,sk_c4) = identity
| multiply(sk_c2,sk_c3) = identity ),
inference(paramod,[status(thm)],[c_1068,c_2]) ).
cnf(c_3911,plain,
( multiply(sk_c7,sk_c5) = identity
| multiply(sk_c2,sk_c3) = identity ),
inference(paramod,[status(thm)],[c_1070,c_2]) ).
cnf(c_16303,plain,
multiply(inverse(A),identity) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_1050,c_58]) ).
cnf(c_16304,plain,
inverse(A) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_567,c_16303]) ).
cnf(c_8479,plain,
multiply(A,inverse(multiply(B,A))) = inverse(B),
inference(copy,[status(thm)],[c_16304]) ).
cnf(c_16305,plain,
( multiply(D,sk_c6) != sk_c7
| inverse(D) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(inverse(multiply(B,C)),sk_c8) != sk_c7
| inverse(C) != inverse(multiply(B,C))
| inverse(B) != sk_c7
| multiply(A,sk_c7) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_8479,c_43]) ).
cnf(c_8538,plain,
( multiply(D,sk_c6) != sk_c7
| inverse(D) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(inverse(multiply(B,C)),sk_c8) != sk_c7
| inverse(multiply(B,C)) != inverse(C)
| inverse(B) != sk_c7
| multiply(A,sk_c7) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16305]) ).
cnf(c_16306,plain,
multiply(inverse(A),inverse(B)) = inverse(multiply(B,A)),
inference(paramod,[status(thm)],[c_8479,c_58]) ).
cnf(c_8540,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_16306]) ).
cnf(c_16307,plain,
( multiply(C,sk_c6) != sk_c7
| inverse(C) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(inverse(multiply(sk_c8,B)),sk_c8) != sk_c7
| inverse(multiply(sk_c8,B)) != inverse(B)
| multiply(A,sk_c7) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_8538]) ).
cnf(c_16308,plain,
( multiply(C,sk_c6) != sk_c7
| inverse(C) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(inverse(multiply(sk_c8,B)),sk_c8) != sk_c7
| multiply(inverse(B),inverse(sk_c8)) != inverse(B)
| multiply(A,sk_c7) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_8540,c_16307]) ).
cnf(c_16309,plain,
( multiply(C,sk_c6) != sk_c7
| inverse(C) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(multiply(inverse(B),inverse(sk_c8)),sk_c8) != sk_c7
| multiply(inverse(B),inverse(sk_c8)) != inverse(B)
| multiply(A,sk_c7) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_8540,c_16308]) ).
cnf(c_16310,plain,
( multiply(C,sk_c6) != sk_c7
| inverse(C) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(inverse(B),multiply(inverse(sk_c8),sk_c8)) != sk_c7
| multiply(inverse(B),inverse(sk_c8)) != inverse(B)
| multiply(A,sk_c7) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_3,c_16309]) ).
cnf(c_16311,plain,
( multiply(C,sk_c6) != sk_c7
| inverse(C) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(inverse(B),identity) != sk_c7
| multiply(inverse(B),inverse(sk_c8)) != inverse(B)
| multiply(A,sk_c7) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_16310]) ).
cnf(c_8566,plain,
( multiply(C,sk_c6) != sk_c7
| inverse(C) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(B) != sk_c7
| multiply(inverse(B),inverse(sk_c8)) != inverse(B)
| multiply(A,sk_c7) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_567,c_16311]) ).
cnf(c_8622,plain,
( multiply(B,sk_c6) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(B) != sk_c7
| multiply(inverse(B),inverse(sk_c8)) != inverse(B)
| multiply(A,sk_c7) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_8566]) ).
cnf(c_16312,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| identity = sk_c7
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_1067,c_24]) ).
cnf(c_10525,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_16312]) ).
cnf(c_10742,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c8
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_10525,c_58]) ).
cnf(c_16313,plain,
( multiply(sk_c4,sk_c7) = sk_c8
| identity = sk_c7
| multiply(sk_c4,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_1069,c_26]) ).
cnf(c_10798,plain,
( identity = sk_c7
| multiply(sk_c4,sk_c7) = sk_c8 ),
inference(copy,[status(thm)],[c_16313]) ).
cnf(c_10802,plain,
( multiply(inverse(sk_c4),sk_c8) = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_10798,c_58]) ).
cnf(c_16314,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| identity = sk_c7
| multiply(sk_c5,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_1071,c_28]) ).
cnf(c_11062,plain,
( identity = sk_c7
| multiply(sk_c5,sk_c6) = sk_c7 ),
inference(copy,[status(thm)],[c_16314]) ).
cnf(c_16315,plain,
( multiply(A,sk_c6) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(A) != sk_c7
| multiply(inverse(A),inverse(sk_c8)) != inverse(A)
| multiply(identity,sk_c7) != sk_c8
| identity != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_618,c_8622]) ).
cnf(c_16316,plain,
( multiply(A,sk_c6) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(A) != sk_c7
| multiply(inverse(A),inverse(sk_c8)) != inverse(A)
| sk_c7 != sk_c8
| identity != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_1,c_16315]) ).
cnf(c_12176,plain,
( multiply(A,sk_c6) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(A) != sk_c7
| multiply(inverse(A),inverse(sk_c8)) != inverse(A)
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16316]) ).
cnf(c_16317,plain,
( multiply(sk_c8,sk_c4) = identity
| identity = sk_c7
| multiply(sk_c8,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_3872,c_87]) ).
cnf(c_12344,plain,
( identity = sk_c7
| multiply(sk_c8,sk_c4) = identity ),
inference(copy,[status(thm)],[c_16317]) ).
cnf(c_16318,plain,
( multiply(inverse(sk_c8),identity) = sk_c4
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_12344,c_58]) ).
cnf(c_12347,plain,
( inverse(sk_c8) = sk_c4
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_567,c_16318]) ).
cnf(c_16319,plain,
( multiply(inverse(A),sk_c6) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(inverse(A)) != sk_c7
| multiply(A,inverse(sk_c8)) != inverse(inverse(A))
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_948,c_12176]) ).
cnf(c_16320,plain,
( multiply(inverse(A),sk_c6) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(inverse(A)) != sk_c7
| multiply(A,inverse(sk_c8)) != A
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_948,c_16319]) ).
cnf(c_16321,plain,
( multiply(inverse(A),sk_c6) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| A != sk_c7
| multiply(A,inverse(sk_c8)) != A
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_948,c_16320]) ).
cnf(c_12482,plain,
( multiply(inverse(A),sk_c6) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| sk_c7 != A
| multiply(A,inverse(sk_c8)) != A
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16321]) ).
cnf(c_16322,plain,
( multiply(inverse(multiply(A,B)),sk_c6) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| sk_c7 != multiply(A,B)
| multiply(A,multiply(B,inverse(sk_c8))) != multiply(A,B)
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_3,c_12482]) ).
cnf(c_16323,plain,
( multiply(multiply(inverse(B),inverse(A)),sk_c6) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| sk_c7 != multiply(A,B)
| multiply(A,multiply(B,inverse(sk_c8))) != multiply(A,B)
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_8540,c_16322]) ).
cnf(c_16324,plain,
( multiply(inverse(B),multiply(inverse(A),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| sk_c7 != multiply(A,B)
| multiply(A,multiply(B,inverse(sk_c8))) != multiply(A,B)
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_3,c_16323]) ).
cnf(c_12512,plain,
( multiply(inverse(B),multiply(inverse(A),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(A,B) != sk_c7
| multiply(A,multiply(B,inverse(sk_c8))) != multiply(A,B)
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_16324]) ).
cnf(c_12621,plain,
( inverse(sk_c4) = sk_c8
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_12347,c_948]) ).
cnf(c_16325,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_12621,c_10802]) ).
cnf(c_12767,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_16325]) ).
cnf(c_12777,plain,
( multiply(inverse(sk_c8),sk_c7) = sk_c8
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_12767,c_58]) ).
cnf(c_16326,plain,
( multiply(sk_c7,sk_c5) = identity
| identity = sk_c7
| multiply(sk_c7,sk_c5) = identity ),
inference(paramod,[status(thm)],[c_3911,c_90]) ).
cnf(c_12908,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c5) = identity ),
inference(copy,[status(thm)],[c_16326]) ).
cnf(c_16327,plain,
( multiply(inverse(sk_c7),identity) = sk_c5
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_12908,c_58]) ).
cnf(c_12911,plain,
( inverse(sk_c7) = sk_c5
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_567,c_16327]) ).
cnf(c_16328,plain,
( multiply(sk_c5,sk_c6) = sk_c8
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_12911,c_10742]) ).
cnf(c_12937,plain,
( multiply(sk_c5,sk_c6) = sk_c8
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_16328]) ).
cnf(c_16329,plain,
( identity = sk_c7
| sk_c8 = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_12937,c_11062]) ).
cnf(c_12972,plain,
( sk_c8 = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_16329]) ).
cnf(c_12987,plain,
( multiply(sk_c7,A) = A
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_12972,c_1]) ).
cnf(c_12988,plain,
( multiply(A,sk_c7) = A
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_12972,c_567]) ).
cnf(c_12989,plain,
( inverse(sk_c7) = identity
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_12972,c_618]) ).
cnf(c_16330,plain,
( inverse(sk_c7) = sk_c7
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_12972,c_12989]) ).
cnf(c_13084,plain,
( inverse(sk_c7) = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16330]) ).
cnf(c_16331,plain,
( sk_c7 = sk_c8
| multiply(sk_c7,sk_c8) = sk_c6
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_13084,c_745]) ).
cnf(c_16332,plain,
( sk_c8 = sk_c7
| multiply(sk_c7,sk_c8) = sk_c6
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16331]) ).
cnf(c_13097,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16332]) ).
cnf(c_16333,plain,
( sk_c7 = sk_c8
| multiply(sk_c4,sk_c7) = sk_c8
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_13084,c_988]) ).
cnf(c_16334,plain,
( sk_c8 = sk_c7
| multiply(sk_c4,sk_c7) = sk_c8
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16333]) ).
cnf(c_13098,plain,
( multiply(sk_c4,sk_c7) = sk_c8
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16334]) ).
cnf(c_16335,plain,
( sk_c7 = sk_c8
| multiply(sk_c5,sk_c6) = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_13084,c_990]) ).
cnf(c_16336,plain,
( sk_c8 = sk_c7
| multiply(sk_c5,sk_c6) = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16335]) ).
cnf(c_13099,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16336]) ).
cnf(c_16337,plain,
( sk_c7 = sk_c8
| multiply(sk_c8,sk_c4) = identity
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_13084,c_1029]) ).
cnf(c_16338,plain,
( sk_c8 = sk_c7
| multiply(sk_c8,sk_c4) = identity
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16337]) ).
cnf(c_13104,plain,
( multiply(sk_c8,sk_c4) = identity
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16338]) ).
cnf(c_16339,plain,
( sk_c6 = sk_c8
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_13097,c_12987]) ).
cnf(c_13234,plain,
( sk_c6 = sk_c8
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16339]) ).
cnf(c_16340,plain,
( sk_c8 = sk_c4
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_13098,c_12988]) ).
cnf(c_16341,plain,
( sk_c4 = sk_c8
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16340]) ).
cnf(c_13285,plain,
( sk_c4 = sk_c8
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16341]) ).
cnf(c_16342,plain,
( multiply(sk_c5,sk_c8) = sk_c7
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_13234,c_13099]) ).
cnf(c_13309,plain,
( multiply(sk_c5,sk_c8) = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16342]) ).
cnf(c_16343,plain,
( multiply(inverse(sk_c8),identity) = sk_c4
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_13104,c_58]) ).
cnf(c_13428,plain,
( inverse(sk_c8) = sk_c4
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_567,c_16343]) ).
cnf(c_16344,plain,
( inverse(sk_c8) = sk_c8
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_13285,c_13428]) ).
cnf(c_13509,plain,
( inverse(sk_c8) = sk_c8
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16344]) ).
cnf(c_16345,plain,
( inverse(sk_c7) = sk_c5
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_13509,c_989]) ).
cnf(c_13551,plain,
( inverse(sk_c7) = sk_c5
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16345]) ).
cnf(c_16346,plain,
( sk_c5 = identity
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_13551,c_12989]) ).
cnf(c_16347,plain,
( identity = sk_c5
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16346]) ).
cnf(c_13822,plain,
( identity = sk_c5
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16347]) ).
cnf(c_13827,plain,
( multiply(sk_c5,A) = A
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_13822,c_1]) ).
cnf(c_16348,plain,
( sk_c8 = sk_c7
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_13827,c_13309]) ).
cnf(c_16349,plain,
( sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_16348]) ).
cnf(c_14314,plain,
sk_c8 = sk_c7,
inference(copy,[status(thm)],[c_16349]) ).
cnf(c_16350,plain,
( multiply(inverse(sk_c7),sk_c7) = sk_c8
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_14314,c_12777]) ).
cnf(c_16351,plain,
( identity = sk_c8
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_16350]) ).
cnf(c_16352,plain,
( identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_14314,c_16351]) ).
cnf(c_14965,plain,
identity = sk_c7,
inference(copy,[status(thm)],[c_16352]) ).
cnf(c_16353,plain,
( multiply(inverse(B),multiply(inverse(A),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(A,B) != sk_c7
| multiply(A,multiply(B,inverse(sk_c8))) != multiply(A,B)
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8
| inverse(sk_c7) != sk_c7 ),
inference(paramod,[status(thm)],[c_14314,c_12512]) ).
cnf(c_16354,plain,
( multiply(inverse(B),multiply(inverse(A),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(A,B) != sk_c7
| multiply(A,multiply(B,inverse(sk_c8))) != multiply(A,B)
| sk_c8 != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c6) != sk_c7
| inverse(sk_c7) != sk_c7 ),
inference(paramod,[status(thm)],[c_14314,c_16353]) ).
cnf(c_16355,plain,
( multiply(inverse(B),multiply(inverse(A),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(A,B) != sk_c7
| multiply(A,multiply(B,inverse(sk_c8))) != multiply(A,B)
| sk_c8 != sk_c7
| sk_c7 != sk_c8
| multiply(sk_c7,sk_c6) != sk_c7
| inverse(sk_c7) != sk_c7 ),
inference(paramod,[status(thm)],[c_14965,c_16354]) ).
cnf(c_16356,plain,
( multiply(inverse(B),multiply(inverse(A),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(A,B) != sk_c7
| multiply(A,multiply(B,inverse(sk_c8))) != multiply(A,B)
| sk_c8 != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c6) != sk_c7
| inverse(sk_c7) != sk_c7 ),
inference(paramod,[status(thm)],[c_14314,c_16355]) ).
cnf(c_16357,plain,
( multiply(inverse(B),multiply(inverse(A),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(A,B) != sk_c7
| multiply(A,multiply(B,inverse(sk_c8))) != multiply(A,B)
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c6) != sk_c7
| inverse(sk_c7) != sk_c7 ),
inference(paramod,[status(thm)],[c_14314,c_16356]) ).
cnf(c_16358,plain,
( multiply(inverse(B),multiply(inverse(A),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(A,B) != sk_c7
| multiply(A,multiply(B,inverse(sk_c7))) != multiply(A,B)
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c6) != sk_c7
| inverse(sk_c7) != sk_c7 ),
inference(paramod,[status(thm)],[c_14314,c_16357]) ).
cnf(c_16359,plain,
( multiply(inverse(B),multiply(inverse(A),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(A,B) != sk_c7
| multiply(A,multiply(B,inverse(sk_c7))) != multiply(A,B)
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c6) != sk_c7
| inverse(sk_c7) != sk_c7 ),
inference(paramod,[status(thm)],[c_14314,c_16358]) ).
cnf(c_16360,plain,
( multiply(inverse(B),multiply(inverse(A),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(A,B) != sk_c7
| multiply(A,multiply(B,inverse(sk_c7))) != multiply(A,B)
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c6) != sk_c7
| inverse(sk_c7) != sk_c7 ),
inference(copy,[status(thm)],[c_16359]) ).
cnf(c_14988,plain,
( multiply(inverse(B),multiply(inverse(A),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(A,B) != sk_c7
| multiply(A,multiply(B,inverse(sk_c7))) != multiply(A,B)
| multiply(sk_c7,sk_c6) != sk_c7
| inverse(sk_c7) != sk_c7 ),
inference(copy,[status(thm)],[c_16360]) ).
cnf(c_16361,plain,
( multiply(sk_c7,multiply(sk_c6,inverse(sk_c8))) = identity
| multiply(sk_c7,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_14314,c_1263]) ).
cnf(c_16362,plain,
( multiply(sk_c7,multiply(sk_c6,inverse(sk_c7))) = identity
| multiply(sk_c7,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_14314,c_16361]) ).
cnf(c_16077,plain,
( multiply(sk_c7,multiply(sk_c6,inverse(sk_c7))) = sk_c7
| multiply(sk_c7,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_14965,c_16362]) ).
cnf(c_16363,plain,
inverse(sk_c7) = identity,
inference(paramod,[status(thm)],[c_14965,c_618]) ).
cnf(c_16265,plain,
inverse(sk_c7) = sk_c7,
inference(paramod,[status(thm)],[c_14965,c_16363]) ).
cnf(c_16266,plain,
multiply(A,sk_c7) = A,
inference(paramod,[status(thm)],[c_14965,c_567]) ).
cnf(c_16269,plain,
multiply(inverse(A),A) = sk_c7,
inference(paramod,[status(thm)],[c_14965,c_2]) ).
cnf(c_16270,plain,
multiply(sk_c7,A) = A,
inference(paramod,[status(thm)],[c_14965,c_1]) ).
cnf(c_16364,plain,
( multiply(inverse(sk_c6),multiply(inverse(sk_c7),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(sk_c7,multiply(sk_c6,inverse(sk_c7))) != multiply(sk_c7,sk_c6)
| multiply(sk_c7,sk_c6) != sk_c7
| inverse(sk_c7) != sk_c7 ),
inference(factor,[status(thm)],[c_14988]) ).
cnf(c_16365,plain,
( multiply(inverse(sk_c6),multiply(inverse(sk_c7),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(sk_c7,multiply(sk_c6,inverse(sk_c7))) != multiply(sk_c7,sk_c6)
| multiply(sk_c7,sk_c6) != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_16265,c_16364]) ).
cnf(c_16366,plain,
( multiply(inverse(sk_c6),multiply(inverse(sk_c7),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(sk_c7,multiply(sk_c6,inverse(sk_c7))) != multiply(sk_c7,sk_c6)
| sk_c6 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_16270,c_16365]) ).
cnf(c_16367,plain,
( multiply(inverse(sk_c6),multiply(inverse(sk_c7),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(sk_c7,multiply(sk_c6,sk_c7)) != multiply(sk_c7,sk_c6)
| sk_c6 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_16265,c_16366]) ).
cnf(c_16368,plain,
( multiply(inverse(sk_c6),multiply(inverse(sk_c7),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != multiply(sk_c7,sk_c6)
| sk_c6 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_16266,c_16367]) ).
cnf(c_16369,plain,
( multiply(inverse(sk_c6),multiply(inverse(sk_c7),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| sk_c6 != multiply(sk_c7,sk_c6)
| sk_c6 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_16270,c_16368]) ).
cnf(c_16370,plain,
( multiply(inverse(sk_c6),multiply(inverse(sk_c7),sk_c6)) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| sk_c6 != sk_c6
| sk_c6 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_16270,c_16369]) ).
cnf(c_16371,plain,
( multiply(inverse(sk_c6),multiply(inverse(sk_c7),sk_c6)) != sk_c7
| sk_c7 != sk_c6
| sk_c6 != sk_c6
| sk_c6 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_16266,c_16370]) ).
cnf(c_16372,plain,
( multiply(inverse(sk_c6),multiply(sk_c7,sk_c6)) != sk_c7
| sk_c7 != sk_c6
| sk_c6 != sk_c6
| sk_c6 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_16265,c_16371]) ).
cnf(c_16373,plain,
( multiply(inverse(sk_c6),sk_c6) != sk_c7
| sk_c7 != sk_c6
| sk_c6 != sk_c6
| sk_c6 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_16270,c_16372]) ).
cnf(c_16374,plain,
( sk_c7 != sk_c7
| sk_c7 != sk_c6
| sk_c6 != sk_c6
| sk_c6 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_16269,c_16373]) ).
cnf(c_16375,plain,
( sk_c7 != sk_c7
| sk_c6 != sk_c7
| sk_c6 != sk_c6
| sk_c6 != sk_c7
| sk_c7 != sk_c7 ),
inference(copy,[status(thm)],[c_16374]) ).
cnf(c_16376,plain,
( sk_c7 != sk_c7
| sk_c6 != sk_c7
| sk_c6 != sk_c6
| sk_c6 != sk_c7 ),
inference(copy,[status(thm)],[c_16375]) ).
cnf(c_16377,plain,
( sk_c7 != sk_c7
| sk_c6 != sk_c7
| sk_c6 != sk_c7 ),
inference(copy,[status(thm)],[c_16376]) ).
cnf(c_16378,plain,
( sk_c6 != sk_c7
| sk_c6 != sk_c7 ),
inference(copy,[status(thm)],[c_16377]) ).
cnf(c_16281,plain,
sk_c6 != sk_c7,
inference(copy,[status(thm)],[c_16378]) ).
cnf(c_16379,plain,
( multiply(sk_c7,multiply(sk_c6,inverse(sk_c7))) = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_16266,c_16077]) ).
cnf(c_16380,plain,
( multiply(sk_c7,multiply(sk_c6,sk_c7)) = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_16265,c_16379]) ).
cnf(c_16381,plain,
( multiply(sk_c7,sk_c6) = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_16266,c_16380]) ).
cnf(c_16382,plain,
( sk_c6 = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_16270,c_16381]) ).
cnf(c_16383,plain,
( sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_16382]) ).
cnf(c_16384,plain,
sk_c6 = sk_c7,
inference(copy,[status(thm)],[c_16383]) ).
cnf(c_16294,plain,
$false,
inference(resolve,[status(thm)],[c_16281,c_16384]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP383-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n007.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Fri Sep 25 14:47:38 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 1261622 was started by sandbox on n007,
% 0.08/0.36 % Fri Sep 25 14:47:38 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.37
% 0.08/0.37 % From the command line: assign(max_seconds, 300).
% 66.43/20.57
% 66.43/20.57 % given #500 (T,wt=8): 12918 identity = sk_c7 | multiply(sk_c5,sk_c7) = identity. [para(12911(b,1),2(a,1,1))].
% 66.43/20.57
% 66.43/20.57 % SZS status Unsatisfiable for theBenchmark
% 66.43/20.57
% 66.43/20.57 % Proof 1 at 8.34 (+ 1.10) seconds.
% 66.43/20.57 % Length of proof is 95.
% 66.43/20.57 % Level of proof is 22.
% 66.43/20.57 % Maximum clause weight is 55.000.
% 66.43/20.57 % Given clauses 570.
% 66.43/20.57
% 66.43/20.57 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------