%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP362-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 : n016.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:42 AM UTC 2026
% Result : Unsatisfiable 9.21s 21.87s
% Output : CNFRefutation 9.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 59
% Number of leaves : 23
% Syntax : Number of formulae : 239 ( 42 unt; 0 def)
% Number of atoms : 591 ( 590 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 531 ( 179 ~; 352 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 80 ( 0 sgn 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(left_identity,axiom,
! [VAR_0] : multiply(identity,VAR_0) = VAR_0,
file('theBenchmark.p',left_identity) ).
cnf(c_1,plain,
multiply(identity,A) = A,
inference(clausify,[status(thm)],[left_identity]) ).
fof(left_inverse,axiom,
! [VAR_0] : multiply(inverse(VAR_0),VAR_0) = identity,
file('theBenchmark.p',left_inverse) ).
cnf(c_2,plain,
multiply(inverse(A),A) = identity,
inference(clausify,[status(thm)],[left_inverse]) ).
fof(associativity,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(multiply(VAR_0,VAR_1),VAR_2) = multiply(VAR_0,multiply(VAR_1,VAR_2)),
file('theBenchmark.p',associativity) ).
cnf(c_3,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(clausify,[status(thm)],[associativity]) ).
fof(prove_this_8,axiom,
( inverse(sk_c7) = sk_c10
| multiply(sk_c9,sk_c8) = sk_c10 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_11,plain,
( inverse(sk_c7) = sk_c10
| multiply(sk_c9,sk_c8) = sk_c10 ),
inference(clausify,[status(thm)],[prove_this_8]) ).
fof(prove_this_9,axiom,
( multiply(sk_c7,sk_c8) = sk_c10
| multiply(sk_c9,sk_c8) = sk_c10 ),
file('theBenchmark.p',prove_this_9) ).
cnf(c_12,plain,
( multiply(sk_c7,sk_c8) = sk_c10
| multiply(sk_c9,sk_c8) = sk_c10 ),
inference(clausify,[status(thm)],[prove_this_9]) ).
fof(prove_this_10,axiom,
( inverse(sk_c10) = sk_c9
| inverse(sk_c9) = sk_c10 ),
file('theBenchmark.p',prove_this_10) ).
cnf(c_13,plain,
( inverse(sk_c10) = sk_c9
| inverse(sk_c9) = sk_c10 ),
inference(clausify,[status(thm)],[prove_this_10]) ).
fof(prove_this_20,axiom,
( multiply(sk_c10,sk_c4) = sk_c9
| multiply(sk_c10,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_20) ).
cnf(c_23,plain,
( multiply(sk_c10,sk_c4) = sk_c9
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_20]) ).
fof(prove_this_21,axiom,
( multiply(sk_c3,sk_c10) = sk_c4
| multiply(sk_c10,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_21) ).
cnf(c_24,plain,
( multiply(sk_c3,sk_c10) = sk_c4
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_21]) ).
fof(prove_this_22,axiom,
( inverse(sk_c3) = sk_c10
| multiply(sk_c10,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_22) ).
cnf(c_25,plain,
( inverse(sk_c3) = sk_c10
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_22]) ).
fof(prove_this_23,axiom,
( multiply(sk_c5,sk_c6) = sk_c8
| multiply(sk_c10,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_23) ).
cnf(c_26,plain,
( multiply(sk_c5,sk_c6) = sk_c8
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_23]) ).
fof(prove_this_24,axiom,
( inverse(sk_c5) = sk_c6
| multiply(sk_c10,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_24) ).
cnf(c_27,plain,
( inverse(sk_c5) = sk_c6
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_24]) ).
fof(prove_this_30,axiom,
( multiply(sk_c3,sk_c10) = sk_c4
| multiply(sk_c10,sk_c2) = sk_c9 ),
file('theBenchmark.p',prove_this_30) ).
cnf(c_33,plain,
( multiply(sk_c3,sk_c10) = sk_c4
| multiply(sk_c10,sk_c2) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_30]) ).
fof(prove_this_32,axiom,
( multiply(sk_c5,sk_c6) = sk_c8
| multiply(sk_c10,sk_c2) = sk_c9 ),
file('theBenchmark.p',prove_this_32) ).
cnf(c_35,plain,
( multiply(sk_c5,sk_c6) = sk_c8
| multiply(sk_c10,sk_c2) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_32]) ).
fof(prove_this_33,axiom,
( inverse(sk_c5) = sk_c6
| multiply(sk_c10,sk_c2) = sk_c9 ),
file('theBenchmark.p',prove_this_33) ).
cnf(c_36,plain,
( inverse(sk_c5) = sk_c6
| multiply(sk_c10,sk_c2) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_33]) ).
fof(prove_this_38,axiom,
( multiply(sk_c10,sk_c4) = sk_c9
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('theBenchmark.p',prove_this_38) ).
cnf(c_41,plain,
( multiply(sk_c10,sk_c4) = sk_c9
| multiply(sk_c1,sk_c10) = sk_c2 ),
inference(clausify,[status(thm)],[prove_this_38]) ).
fof(prove_this_40,axiom,
( inverse(sk_c3) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('theBenchmark.p',prove_this_40) ).
cnf(c_43,plain,
( inverse(sk_c3) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c2 ),
inference(clausify,[status(thm)],[prove_this_40]) ).
fof(prove_this_41,axiom,
( multiply(sk_c5,sk_c6) = sk_c8
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('theBenchmark.p',prove_this_41) ).
cnf(c_44,plain,
( multiply(sk_c5,sk_c6) = sk_c8
| multiply(sk_c1,sk_c10) = sk_c2 ),
inference(clausify,[status(thm)],[prove_this_41]) ).
fof(prove_this_42,axiom,
( inverse(sk_c5) = sk_c6
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('theBenchmark.p',prove_this_42) ).
cnf(c_45,plain,
( inverse(sk_c5) = sk_c6
| multiply(sk_c1,sk_c10) = sk_c2 ),
inference(clausify,[status(thm)],[prove_this_42]) ).
fof(prove_this_48,axiom,
( multiply(sk_c3,sk_c10) = sk_c4
| inverse(sk_c1) = sk_c10 ),
file('theBenchmark.p',prove_this_48) ).
cnf(c_51,plain,
( multiply(sk_c3,sk_c10) = sk_c4
| inverse(sk_c1) = sk_c10 ),
inference(clausify,[status(thm)],[prove_this_48]) ).
fof(prove_this_49,axiom,
( inverse(sk_c3) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('theBenchmark.p',prove_this_49) ).
cnf(c_52,plain,
( inverse(sk_c3) = sk_c10
| inverse(sk_c1) = sk_c10 ),
inference(clausify,[status(thm)],[prove_this_49]) ).
fof(prove_this_50,axiom,
( multiply(sk_c5,sk_c6) = sk_c8
| inverse(sk_c1) = sk_c10 ),
file('theBenchmark.p',prove_this_50) ).
cnf(c_53,plain,
( multiply(sk_c5,sk_c6) = sk_c8
| inverse(sk_c1) = sk_c10 ),
inference(clausify,[status(thm)],[prove_this_50]) ).
fof(prove_this_51,axiom,
( inverse(sk_c5) = sk_c6
| inverse(sk_c1) = sk_c10 ),
file('theBenchmark.p',prove_this_51) ).
cnf(c_54,plain,
( inverse(sk_c5) = sk_c6
| inverse(sk_c1) = sk_c10 ),
inference(clausify,[status(thm)],[prove_this_51]) ).
fof(prove_this_55,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( multiply(VAR_6,sk_c8) != sk_c10
| inverse(VAR_6) != sk_c10
| multiply(VAR_5,sk_c9) != sk_c8
| inverse(VAR_4) != VAR_5
| multiply(VAR_4,VAR_5) != sk_c8
| inverse(VAR_3) != sk_c10
| multiply(VAR_3,sk_c10) != VAR_2
| multiply(sk_c10,VAR_2) != sk_c9
| inverse(sk_c10) != sk_c9
| inverse(VAR_1) != sk_c10
| multiply(VAR_1,sk_c10) != VAR_0
| multiply(sk_c10,VAR_0) != sk_c9
| multiply(sk_c10,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c10
| multiply(sk_c9,sk_c8) != sk_c10 ),
file('theBenchmark.p',prove_this_55) ).
cnf(c_58,plain,
( multiply(V6,sk_c8) != sk_c10
| inverse(V6) != sk_c10
| multiply(F,sk_c9) != sk_c8
| inverse(E) != F
| multiply(E,F) != sk_c8
| inverse(D) != sk_c10
| multiply(D,sk_c10) != C
| multiply(sk_c10,C) != sk_c9
| inverse(sk_c10) != sk_c9
| inverse(B) != sk_c10
| multiply(B,sk_c10) != A
| multiply(sk_c10,A) != sk_c9
| multiply(sk_c10,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c10
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(clausify,[status(thm)],[prove_this_55]) ).
cnf(c_2312,plain,
( inverse(sk_c9) != sk_c10
| multiply(F,sk_c9) != sk_c8
| inverse(E) != F
| multiply(E,F) != sk_c8
| inverse(D) != sk_c10
| multiply(D,sk_c10) != C
| multiply(sk_c10,C) != sk_c9
| inverse(sk_c10) != sk_c9
| inverse(B) != sk_c10
| multiply(B,sk_c10) != A
| multiply(sk_c10,A) != sk_c9
| multiply(sk_c10,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c10
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(factor,[status(thm)],[c_58]) ).
cnf(c_59,plain,
( multiply(F,sk_c9) != sk_c8
| inverse(E) != F
| multiply(E,F) != sk_c8
| inverse(D) != sk_c10
| multiply(D,sk_c10) != C
| multiply(sk_c10,C) != sk_c9
| inverse(sk_c10) != sk_c9
| inverse(B) != sk_c10
| multiply(B,sk_c10) != A
| multiply(sk_c10,A) != sk_c9
| multiply(sk_c10,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c10
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(copy,[status(thm)],[c_2312]) ).
cnf(c_63,plain,
( multiply(E,sk_c9) != sk_c8
| inverse(D) != E
| multiply(D,E) != sk_c8
| inverse(C) != sk_c10
| multiply(C,sk_c10) != B
| multiply(sk_c10,B) != sk_c9
| inverse(sk_c10) != sk_c9
| multiply(sk_c9,sk_c10) != A
| multiply(sk_c10,A) != sk_c9
| multiply(sk_c10,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c10
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(factor,[status(thm)],[c_59]) ).
cnf(c_2313,plain,
( multiply(C,sk_c9) != sk_c8
| inverse(B) != C
| multiply(B,C) != sk_c8
| inverse(sk_c9) != sk_c10
| multiply(sk_c10,A) != sk_c9
| inverse(sk_c10) != sk_c9
| multiply(sk_c9,sk_c10) != A
| multiply(sk_c10,A) != sk_c9
| multiply(sk_c10,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c10
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(factor,[status(thm)],[c_63]) ).
cnf(c_2314,plain,
( multiply(C,sk_c9) != sk_c8
| inverse(B) != C
| multiply(B,C) != sk_c8
| inverse(sk_c9) != sk_c10
| inverse(sk_c10) != sk_c9
| multiply(sk_c9,sk_c10) != A
| multiply(sk_c10,A) != sk_c9
| multiply(sk_c10,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c10
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(copy,[status(thm)],[c_2313]) ).
cnf(c_71,plain,
( multiply(C,sk_c9) != sk_c8
| inverse(B) != C
| multiply(B,C) != sk_c8
| inverse(sk_c10) != sk_c9
| multiply(sk_c9,sk_c10) != A
| multiply(sk_c10,A) != sk_c9
| multiply(sk_c10,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c10
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(copy,[status(thm)],[c_2314]) ).
cnf(c_2315,plain,
( multiply(sk_c10,sk_c9) != sk_c8
| inverse(sk_c9) != sk_c10
| inverse(sk_c10) != sk_c9
| multiply(sk_c9,sk_c10) != sk_c8
| multiply(sk_c10,sk_c8) != sk_c9
| multiply(sk_c10,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c10
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(factor,[status(thm)],[c_71]) ).
cnf(c_2316,plain,
( multiply(sk_c10,sk_c9) != sk_c8
| inverse(sk_c9) != sk_c10
| inverse(sk_c10) != sk_c9
| multiply(sk_c9,sk_c10) != sk_c8
| multiply(sk_c10,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c10
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(copy,[status(thm)],[c_2315]) ).
cnf(c_83,plain,
( multiply(sk_c10,sk_c9) != sk_c8
| inverse(sk_c10) != sk_c9
| multiply(sk_c9,sk_c10) != sk_c8
| multiply(sk_c10,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c10
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(copy,[status(thm)],[c_2316]) ).
cnf(c_2317,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_2318,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_2317]) ).
cnf(c_88,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_2318]) ).
cnf(c_114,plain,
( multiply(sk_c10,sk_c7) = identity
| multiply(sk_c9,sk_c8) = sk_c10 ),
inference(paramod,[status(thm)],[c_11,c_2]) ).
cnf(c_121,plain,
( multiply(sk_c10,sk_c9) = identity
| inverse(sk_c10) = sk_c9 ),
inference(paramod,[status(thm)],[c_13,c_2]) ).
cnf(c_2319,plain,
( multiply(sk_c9,A) = multiply(sk_c10,multiply(sk_c4,A))
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_23,c_3]) ).
cnf(c_149,plain,
( multiply(sk_c10,multiply(sk_c4,A)) = multiply(sk_c9,A)
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(copy,[status(thm)],[c_2319]) ).
cnf(c_155,plain,
( multiply(sk_c10,sk_c3) = identity
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_25,c_2]) ).
cnf(c_2320,plain,
( multiply(sk_c9,A) = multiply(sk_c10,multiply(sk_c8,A))
| multiply(sk_c5,sk_c6) = sk_c8 ),
inference(paramod,[status(thm)],[c_26,c_3]) ).
cnf(c_158,plain,
( multiply(sk_c10,multiply(sk_c8,A)) = multiply(sk_c9,A)
| multiply(sk_c5,sk_c6) = sk_c8 ),
inference(copy,[status(thm)],[c_2320]) ).
cnf(c_2321,plain,
( multiply(multiply(A,sk_c5),sk_c6) = multiply(A,sk_c8)
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_26,c_3]) ).
cnf(c_161,plain,
( multiply(A,multiply(sk_c5,sk_c6)) = multiply(A,sk_c8)
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_3,c_2321]) ).
cnf(c_2322,plain,
( multiply(multiply(A,sk_c10),sk_c8) = multiply(A,sk_c9)
| inverse(sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_27,c_3]) ).
cnf(c_164,plain,
( multiply(A,multiply(sk_c10,sk_c8)) = multiply(A,sk_c9)
| inverse(sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_3,c_2322]) ).
cnf(c_2323,plain,
( multiply(multiply(A,sk_c10),sk_c2) = multiply(A,sk_c9)
| multiply(sk_c3,sk_c10) = sk_c4 ),
inference(paramod,[status(thm)],[c_33,c_3]) ).
cnf(c_184,plain,
( multiply(A,multiply(sk_c10,sk_c2)) = multiply(A,sk_c9)
| multiply(sk_c3,sk_c10) = sk_c4 ),
inference(paramod,[status(thm)],[c_3,c_2323]) ).
cnf(c_248,plain,
( multiply(sk_c10,sk_c1) = identity
| inverse(sk_c3) = sk_c10 ),
inference(paramod,[status(thm)],[c_52,c_2]) ).
cnf(c_249,plain,
( multiply(sk_c10,sk_c3) = identity
| inverse(sk_c1) = sk_c10 ),
inference(paramod,[status(thm)],[c_52,c_2]) ).
cnf(c_253,plain,
( multiply(sk_c10,sk_c1) = identity
| inverse(sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_54,c_2]) ).
cnf(c_264,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_88]) ).
cnf(c_328,plain,
( multiply(inverse(sk_c10),sk_c9) = sk_c2
| multiply(sk_c5,sk_c6) = sk_c8 ),
inference(paramod,[status(thm)],[c_35,c_88]) ).
cnf(c_330,plain,
( multiply(inverse(sk_c10),sk_c9) = sk_c2
| inverse(sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_36,c_88]) ).
cnf(c_340,plain,
( multiply(inverse(sk_c1),sk_c2) = sk_c10
| multiply(sk_c10,sk_c4) = sk_c9 ),
inference(paramod,[status(thm)],[c_41,c_88]) ).
cnf(c_374,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_88,c_88]) ).
cnf(c_375,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_374,c_264]) ).
cnf(c_2324,plain,
( multiply(inverse(sk_c10),identity) = sk_c9
| inverse(sk_c10) = sk_c9 ),
inference(paramod,[status(thm)],[c_121,c_88]) ).
cnf(c_2325,plain,
( inverse(sk_c10) = sk_c9
| inverse(sk_c10) = sk_c9 ),
inference(paramod,[status(thm)],[c_375,c_2324]) ).
cnf(c_385,plain,
inverse(sk_c10) = sk_c9,
inference(copy,[status(thm)],[c_2325]) ).
cnf(c_391,plain,
( multiply(sk_c9,sk_c9) = sk_c2
| inverse(sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_385,c_330]) ).
cnf(c_392,plain,
( multiply(sk_c9,sk_c9) = sk_c2
| multiply(sk_c5,sk_c6) = sk_c8 ),
inference(paramod,[status(thm)],[c_385,c_328]) ).
cnf(c_2326,plain,
( multiply(sk_c10,sk_c9) != sk_c8
| sk_c9 != sk_c9
| multiply(sk_c9,sk_c10) != sk_c8
| multiply(sk_c10,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c10
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(paramod,[status(thm)],[c_385,c_83]) ).
cnf(c_408,plain,
( multiply(sk_c10,sk_c9) != sk_c8
| multiply(sk_c9,sk_c10) != sk_c8
| multiply(sk_c10,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c10
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(copy,[status(thm)],[c_2326]) ).
cnf(c_409,plain,
multiply(sk_c9,sk_c10) = identity,
inference(paramod,[status(thm)],[c_385,c_2]) ).
cnf(c_410,plain,
multiply(sk_c9,multiply(sk_c10,A)) = A,
inference(paramod,[status(thm)],[c_385,c_88]) ).
cnf(c_411,plain,
( multiply(sk_c10,sk_c9) != sk_c8
| identity != sk_c8
| multiply(sk_c10,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c10
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(paramod,[status(thm)],[c_409,c_408]) ).
cnf(c_2327,plain,
multiply(inverse(sk_c9),identity) = sk_c10,
inference(paramod,[status(thm)],[c_409,c_88]) ).
cnf(c_412,plain,
inverse(sk_c9) = sk_c10,
inference(paramod,[status(thm)],[c_375,c_2327]) ).
cnf(c_2328,plain,
( multiply(sk_c10,sk_c9) != sk_c8
| identity != sk_c8
| multiply(sk_c10,sk_c8) != sk_c9
| sk_c10 != sk_c10
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(paramod,[status(thm)],[c_412,c_411]) ).
cnf(c_413,plain,
( multiply(sk_c10,sk_c9) != sk_c8
| identity != sk_c8
| multiply(sk_c10,sk_c8) != sk_c9
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(copy,[status(thm)],[c_2328]) ).
cnf(c_447,plain,
( inverse(sk_c5) = sk_c6
| multiply(sk_c10,sk_c9) != sk_c8
| identity != sk_c8
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(resolve,[status(thm)],[c_413,c_27]) ).
cnf(c_452,plain,
multiply(sk_c10,sk_c9) = identity,
inference(paramod,[status(thm)],[c_412,c_2]) ).
cnf(c_2329,plain,
( inverse(sk_c5) = sk_c6
| identity != sk_c8
| identity != sk_c8
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(paramod,[status(thm)],[c_452,c_447]) ).
cnf(c_458,plain,
( inverse(sk_c5) = sk_c6
| identity != sk_c8
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(copy,[status(thm)],[c_2329]) ).
cnf(c_2330,plain,
( identity != sk_c8
| identity != sk_c8
| multiply(sk_c10,sk_c8) != sk_c9
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(paramod,[status(thm)],[c_452,c_413]) ).
cnf(c_470,plain,
( identity != sk_c8
| multiply(sk_c10,sk_c8) != sk_c9
| multiply(sk_c9,sk_c8) != sk_c10 ),
inference(copy,[status(thm)],[c_2330]) ).
cnf(c_2331,plain,
( multiply(inverse(sk_c10),identity) = sk_c1
| inverse(sk_c3) = sk_c10 ),
inference(paramod,[status(thm)],[c_248,c_88]) ).
cnf(c_2332,plain,
( multiply(sk_c9,identity) = sk_c1
| inverse(sk_c3) = sk_c10 ),
inference(paramod,[status(thm)],[c_385,c_2331]) ).
cnf(c_2333,plain,
( sk_c9 = sk_c1
| inverse(sk_c3) = sk_c10 ),
inference(paramod,[status(thm)],[c_375,c_2332]) ).
cnf(c_476,plain,
( sk_c1 = sk_c9
| inverse(sk_c3) = sk_c10 ),
inference(copy,[status(thm)],[c_2333]) ).
cnf(c_2334,plain,
( inverse(sk_c3) = sk_c10
| multiply(sk_c9,sk_c10) = sk_c2
| inverse(sk_c3) = sk_c10 ),
inference(paramod,[status(thm)],[c_476,c_43]) ).
cnf(c_2335,plain,
( inverse(sk_c3) = sk_c10
| identity = sk_c2
| inverse(sk_c3) = sk_c10 ),
inference(paramod,[status(thm)],[c_409,c_2334]) ).
cnf(c_481,plain,
( identity = sk_c2
| inverse(sk_c3) = sk_c10 ),
inference(copy,[status(thm)],[c_2335]) ).
cnf(c_484,plain,
( multiply(sk_c10,sk_c3) = identity
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_481,c_2]) ).
cnf(c_2336,plain,
( multiply(inverse(sk_c10),identity) = sk_c3
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_484,c_88]) ).
cnf(c_2337,plain,
( multiply(sk_c9,identity) = sk_c3
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_385,c_2336]) ).
cnf(c_2338,plain,
( sk_c9 = sk_c3
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_375,c_2337]) ).
cnf(c_518,plain,
( sk_c3 = sk_c9
| identity = sk_c2 ),
inference(copy,[status(thm)],[c_2338]) ).
cnf(c_529,plain,
( multiply(A,sk_c2) = A
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_518,c_375]) ).
cnf(c_2339,plain,
( multiply(sk_c5,sk_c6) = sk_c8
| sk_c10 = sk_c9
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_529,c_35]) ).
cnf(c_597,plain,
( multiply(sk_c5,sk_c6) = sk_c8
| sk_c9 = sk_c10
| sk_c3 = sk_c9 ),
inference(copy,[status(thm)],[c_2339]) ).
cnf(c_2340,plain,
( multiply(inverse(sk_c10),identity) = sk_c3
| inverse(sk_c1) = sk_c10 ),
inference(paramod,[status(thm)],[c_249,c_88]) ).
cnf(c_2341,plain,
( multiply(sk_c9,identity) = sk_c3
| inverse(sk_c1) = sk_c10 ),
inference(paramod,[status(thm)],[c_385,c_2340]) ).
cnf(c_2342,plain,
( sk_c9 = sk_c3
| inverse(sk_c1) = sk_c10 ),
inference(paramod,[status(thm)],[c_375,c_2341]) ).
cnf(c_664,plain,
( sk_c3 = sk_c9
| inverse(sk_c1) = sk_c10 ),
inference(copy,[status(thm)],[c_2342]) ).
cnf(c_2343,plain,
( multiply(sk_c9,sk_c10) = sk_c4
| inverse(sk_c1) = sk_c10
| inverse(sk_c1) = sk_c10 ),
inference(paramod,[status(thm)],[c_664,c_51]) ).
cnf(c_2344,plain,
( identity = sk_c4
| inverse(sk_c1) = sk_c10
| inverse(sk_c1) = sk_c10 ),
inference(paramod,[status(thm)],[c_409,c_2343]) ).
cnf(c_671,plain,
( identity = sk_c4
| inverse(sk_c1) = sk_c10 ),
inference(copy,[status(thm)],[c_2344]) ).
cnf(c_676,plain,
( multiply(sk_c10,sk_c1) = identity
| identity = sk_c4 ),
inference(paramod,[status(thm)],[c_671,c_2]) ).
cnf(c_2345,plain,
( multiply(inverse(sk_c10),identity) = sk_c1
| identity = sk_c4 ),
inference(paramod,[status(thm)],[c_676,c_88]) ).
cnf(c_2346,plain,
( multiply(sk_c9,identity) = sk_c1
| identity = sk_c4 ),
inference(paramod,[status(thm)],[c_385,c_2345]) ).
cnf(c_2347,plain,
( sk_c9 = sk_c1
| identity = sk_c4 ),
inference(paramod,[status(thm)],[c_375,c_2346]) ).
cnf(c_709,plain,
( sk_c1 = sk_c9
| identity = sk_c4 ),
inference(copy,[status(thm)],[c_2347]) ).
cnf(c_2348,plain,
( multiply(inverse(sk_c10),identity) = sk_c1
| inverse(sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_253,c_88]) ).
cnf(c_2349,plain,
( multiply(sk_c9,identity) = sk_c1
| inverse(sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_385,c_2348]) ).
cnf(c_2350,plain,
( sk_c9 = sk_c1
| inverse(sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_375,c_2349]) ).
cnf(c_951,plain,
( sk_c1 = sk_c9
| inverse(sk_c5) = sk_c6 ),
inference(copy,[status(thm)],[c_2350]) ).
cnf(c_956,plain,
( multiply(sk_c6,sk_c5) = identity
| sk_c1 = sk_c9 ),
inference(paramod,[status(thm)],[c_951,c_2]) ).
cnf(c_2351,plain,
( inverse(sk_c5) = sk_c6
| multiply(sk_c9,sk_c10) = sk_c2
| inverse(sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_951,c_45]) ).
cnf(c_2352,plain,
( inverse(sk_c5) = sk_c6
| identity = sk_c2
| inverse(sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_409,c_2351]) ).
cnf(c_960,plain,
( identity = sk_c2
| inverse(sk_c5) = sk_c6 ),
inference(copy,[status(thm)],[c_2352]) ).
cnf(c_2353,plain,
( multiply(inverse(sk_c6),identity) = sk_c5
| sk_c1 = sk_c9 ),
inference(paramod,[status(thm)],[c_956,c_88]) ).
cnf(c_992,plain,
( inverse(sk_c6) = sk_c5
| sk_c1 = sk_c9 ),
inference(paramod,[status(thm)],[c_375,c_2353]) ).
cnf(c_996,plain,
( multiply(sk_c5,sk_c6) = identity
| sk_c1 = sk_c9 ),
inference(paramod,[status(thm)],[c_992,c_2]) ).
cnf(c_2354,plain,
( multiply(sk_c5,sk_c6) = sk_c4
| sk_c1 = sk_c9
| sk_c1 = sk_c9 ),
inference(paramod,[status(thm)],[c_709,c_996]) ).
cnf(c_1077,plain,
( multiply(sk_c5,sk_c6) = sk_c4
| sk_c1 = sk_c9 ),
inference(copy,[status(thm)],[c_2354]) ).
cnf(c_2355,plain,
( multiply(sk_c5,sk_c6) = sk_c8
| multiply(sk_c9,sk_c10) = sk_c2
| multiply(sk_c5,sk_c6) = sk_c4 ),
inference(paramod,[status(thm)],[c_1077,c_44]) ).
cnf(c_1153,plain,
( multiply(sk_c5,sk_c6) = sk_c8
| identity = sk_c2
| multiply(sk_c5,sk_c6) = sk_c4 ),
inference(paramod,[status(thm)],[c_409,c_2355]) ).
cnf(c_2356,plain,
( multiply(inverse(sk_c10),identity) = sk_c7
| multiply(sk_c9,sk_c8) = sk_c10 ),
inference(paramod,[status(thm)],[c_114,c_88]) ).
cnf(c_2357,plain,
( multiply(sk_c9,identity) = sk_c7
| multiply(sk_c9,sk_c8) = sk_c10 ),
inference(paramod,[status(thm)],[c_385,c_2356]) ).
cnf(c_2358,plain,
( sk_c9 = sk_c7
| multiply(sk_c9,sk_c8) = sk_c10 ),
inference(paramod,[status(thm)],[c_375,c_2357]) ).
cnf(c_1193,plain,
( sk_c7 = sk_c9
| multiply(sk_c9,sk_c8) = sk_c10 ),
inference(copy,[status(thm)],[c_2358]) ).
cnf(c_2359,plain,
( multiply(sk_c9,sk_c8) = sk_c10
| multiply(sk_c9,sk_c8) = sk_c10
| multiply(sk_c9,sk_c8) = sk_c10 ),
inference(paramod,[status(thm)],[c_1193,c_12]) ).
cnf(c_2360,plain,
( multiply(sk_c9,sk_c8) = sk_c10
| multiply(sk_c9,sk_c8) = sk_c10 ),
inference(copy,[status(thm)],[c_2359]) ).
cnf(c_1232,plain,
multiply(sk_c9,sk_c8) = sk_c10,
inference(copy,[status(thm)],[c_2360]) ).
cnf(c_2361,plain,
( identity != sk_c8
| multiply(sk_c10,sk_c8) != sk_c9
| sk_c10 != sk_c10 ),
inference(paramod,[status(thm)],[c_1232,c_470]) ).
cnf(c_1246,plain,
( identity != sk_c8
| multiply(sk_c10,sk_c8) != sk_c9 ),
inference(copy,[status(thm)],[c_2361]) ).
cnf(c_2362,plain,
( inverse(sk_c5) = sk_c6
| identity != sk_c8
| sk_c10 != sk_c10 ),
inference(paramod,[status(thm)],[c_1232,c_458]) ).
cnf(c_1250,plain,
( inverse(sk_c5) = sk_c6
| identity != sk_c8 ),
inference(copy,[status(thm)],[c_2362]) ).
cnf(c_2363,plain,
multiply(inverse(sk_c9),sk_c10) = sk_c8,
inference(paramod,[status(thm)],[c_1232,c_88]) ).
cnf(c_1256,plain,
multiply(sk_c10,sk_c10) = sk_c8,
inference(paramod,[status(thm)],[c_412,c_2363]) ).
cnf(c_1257,plain,
multiply(sk_c8,A) = multiply(sk_c10,multiply(sk_c10,A)),
inference(paramod,[status(thm)],[c_1256,c_3]) ).
cnf(c_2364,plain,
( multiply(sk_c10,multiply(sk_c10,multiply(sk_c10,A))) = multiply(sk_c9,A)
| multiply(sk_c5,sk_c6) = sk_c8 ),
inference(paramod,[status(thm)],[c_1257,c_158]) ).
cnf(c_1274,plain,
( multiply(sk_c9,A) = multiply(sk_c10,multiply(sk_c10,multiply(sk_c10,A)))
| multiply(sk_c5,sk_c6) = sk_c8 ),
inference(copy,[status(thm)],[c_2364]) ).
cnf(c_2365,plain,
( inverse(sk_c5) = sk_c6
| sk_c2 != sk_c8
| inverse(sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_960,c_1250]) ).
cnf(c_1311,plain,
( sk_c2 != sk_c8
| inverse(sk_c5) = sk_c6 ),
inference(copy,[status(thm)],[c_2365]) ).
cnf(c_2366,plain,
( multiply(inverse(sk_c10),identity) = sk_c3
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_155,c_88]) ).
cnf(c_2367,plain,
( multiply(sk_c9,identity) = sk_c3
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_385,c_2366]) ).
cnf(c_2368,plain,
( sk_c9 = sk_c3
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_375,c_2367]) ).
cnf(c_1454,plain,
( sk_c3 = sk_c9
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(copy,[status(thm)],[c_2368]) ).
cnf(c_2369,plain,
( multiply(sk_c10,multiply(sk_c4,sk_c8)) = multiply(sk_c9,multiply(sk_c5,sk_c6))
| multiply(sk_c10,sk_c8) = sk_c9
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_161,c_149]) ).
cnf(c_2370,plain,
( multiply(sk_c9,multiply(sk_c5,sk_c6)) = multiply(sk_c10,multiply(sk_c4,sk_c8))
| multiply(sk_c10,sk_c8) = sk_c9
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(copy,[status(thm)],[c_2369]) ).
cnf(c_1534,plain,
( multiply(sk_c9,multiply(sk_c5,sk_c6)) = multiply(sk_c10,multiply(sk_c4,sk_c8))
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(copy,[status(thm)],[c_2370]) ).
cnf(c_1561,plain,
( identity != sk_c8
| sk_c3 = sk_c9 ),
inference(resolve,[status(thm)],[c_1454,c_1246]) ).
cnf(c_2371,plain,
( multiply(sk_c9,sk_c10) = sk_c4
| multiply(sk_c10,sk_c8) = sk_c9
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_1454,c_24]) ).
cnf(c_2372,plain,
( identity = sk_c4
| multiply(sk_c10,sk_c8) = sk_c9
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_409,c_2371]) ).
cnf(c_1564,plain,
( identity = sk_c4
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(copy,[status(thm)],[c_2372]) ).
cnf(c_1628,plain,
( identity != sk_c8
| identity = sk_c4 ),
inference(resolve,[status(thm)],[c_1564,c_1246]) ).
cnf(c_2373,plain,
( multiply(inverse(sk_c10),sk_c9) = sk_c8
| identity = sk_c4 ),
inference(paramod,[status(thm)],[c_1564,c_88]) ).
cnf(c_1631,plain,
( multiply(sk_c9,sk_c9) = sk_c8
| identity = sk_c4 ),
inference(paramod,[status(thm)],[c_385,c_2373]) ).
cnf(c_2374,plain,
( multiply(sk_c9,multiply(sk_c10,sk_c8)) = sk_c2
| inverse(sk_c5) = sk_c6
| inverse(sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_391,c_164]) ).
cnf(c_2375,plain,
( sk_c8 = sk_c2
| inverse(sk_c5) = sk_c6
| inverse(sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_410,c_2374]) ).
cnf(c_2376,plain,
( sk_c2 = sk_c8
| inverse(sk_c5) = sk_c6
| inverse(sk_c5) = sk_c6 ),
inference(copy,[status(thm)],[c_2375]) ).
cnf(c_1857,plain,
( sk_c2 = sk_c8
| inverse(sk_c5) = sk_c6 ),
inference(copy,[status(thm)],[c_2376]) ).
cnf(c_2377,plain,
( multiply(sk_c9,multiply(sk_c10,sk_c2)) = sk_c8
| multiply(sk_c3,sk_c10) = sk_c4
| identity = sk_c4 ),
inference(paramod,[status(thm)],[c_1631,c_184]) ).
cnf(c_1901,plain,
( sk_c2 = sk_c8
| multiply(sk_c3,sk_c10) = sk_c4
| identity = sk_c4 ),
inference(paramod,[status(thm)],[c_410,c_2377]) ).
cnf(c_2378,plain,
( inverse(sk_c5) = sk_c6
| inverse(sk_c5) = sk_c6 ),
inference(resolve,[status(thm)],[c_1857,c_1311]) ).
cnf(c_1908,plain,
inverse(sk_c5) = sk_c6,
inference(copy,[status(thm)],[c_2378]) ).
cnf(c_1916,plain,
multiply(sk_c6,sk_c5) = identity,
inference(paramod,[status(thm)],[c_1908,c_2]) ).
cnf(c_2379,plain,
multiply(inverse(sk_c6),identity) = sk_c5,
inference(paramod,[status(thm)],[c_1916,c_88]) ).
cnf(c_1918,plain,
inverse(sk_c6) = sk_c5,
inference(paramod,[status(thm)],[c_375,c_2379]) ).
cnf(c_1924,plain,
multiply(sk_c5,sk_c6) = identity,
inference(paramod,[status(thm)],[c_1918,c_2]) ).
cnf(c_2380,plain,
( multiply(sk_c9,identity) = multiply(sk_c10,multiply(sk_c4,sk_c8))
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_1924,c_1534]) ).
cnf(c_2381,plain,
( sk_c9 = multiply(sk_c10,multiply(sk_c4,sk_c8))
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_375,c_2380]) ).
cnf(c_1928,plain,
( multiply(sk_c10,multiply(sk_c4,sk_c8)) = sk_c9
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(copy,[status(thm)],[c_2381]) ).
cnf(c_1943,plain,
( multiply(sk_c9,A) = multiply(sk_c10,multiply(sk_c10,multiply(sk_c10,A)))
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_1924,c_1274]) ).
cnf(c_2382,plain,
( multiply(sk_c5,sk_c6) = sk_c8
| identity = sk_c2
| identity = sk_c4 ),
inference(paramod,[status(thm)],[c_1924,c_1153]) ).
cnf(c_1944,plain,
( identity = sk_c8
| identity = sk_c2
| identity = sk_c4 ),
inference(paramod,[status(thm)],[c_1924,c_2382]) ).
cnf(c_1952,plain,
( identity = sk_c8
| sk_c9 = sk_c10
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_1924,c_597]) ).
cnf(c_1954,plain,
( multiply(sk_c9,sk_c9) = sk_c2
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_1924,c_392]) ).
cnf(c_1967,plain,
( identity = sk_c8
| inverse(sk_c1) = sk_c10 ),
inference(paramod,[status(thm)],[c_1924,c_53]) ).
cnf(c_2383,plain,
( identity = sk_c4
| identity = sk_c2
| identity = sk_c4 ),
inference(resolve,[status(thm)],[c_1944,c_1628]) ).
cnf(c_2027,plain,
( identity = sk_c2
| identity = sk_c4 ),
inference(copy,[status(thm)],[c_2383]) ).
cnf(c_2384,plain,
( sk_c2 != sk_c8
| identity = sk_c4
| identity = sk_c4 ),
inference(paramod,[status(thm)],[c_2027,c_1628]) ).
cnf(c_2057,plain,
( sk_c2 != sk_c8
| identity = sk_c4 ),
inference(copy,[status(thm)],[c_2384]) ).
cnf(c_2385,plain,
( multiply(sk_c10,sk_c10) = identity
| identity = sk_c8
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_1952,c_409]) ).
cnf(c_2386,plain,
( sk_c8 = identity
| identity = sk_c8
| sk_c3 = sk_c9 ),
inference(paramod,[status(thm)],[c_1256,c_2385]) ).
cnf(c_2387,plain,
( identity = sk_c8
| identity = sk_c8
| sk_c3 = sk_c9 ),
inference(copy,[status(thm)],[c_2386]) ).
cnf(c_2064,plain,
( identity = sk_c8
| sk_c3 = sk_c9 ),
inference(copy,[status(thm)],[c_2387]) ).
cnf(c_2388,plain,
( sk_c3 = sk_c9
| sk_c3 = sk_c9 ),
inference(resolve,[status(thm)],[c_2064,c_1561]) ).
cnf(c_2108,plain,
sk_c3 = sk_c9,
inference(copy,[status(thm)],[c_2388]) ).
cnf(c_2389,plain,
( sk_c2 = sk_c8
| multiply(sk_c9,sk_c10) = sk_c4
| identity = sk_c4 ),
inference(paramod,[status(thm)],[c_2108,c_1901]) ).
cnf(c_2390,plain,
( sk_c2 = sk_c8
| identity = sk_c4
| identity = sk_c4 ),
inference(paramod,[status(thm)],[c_409,c_2389]) ).
cnf(c_2130,plain,
( sk_c2 = sk_c8
| identity = sk_c4 ),
inference(copy,[status(thm)],[c_2390]) ).
cnf(c_2391,plain,
( identity = sk_c4
| identity = sk_c4 ),
inference(resolve,[status(thm)],[c_2130,c_2057]) ).
cnf(c_2176,plain,
identity = sk_c4,
inference(copy,[status(thm)],[c_2391]) ).
cnf(c_2194,plain,
( sk_c4 = sk_c8
| inverse(sk_c1) = sk_c10 ),
inference(paramod,[status(thm)],[c_2176,c_1967]) ).
cnf(c_2203,plain,
( multiply(sk_c9,sk_c9) = sk_c2
| sk_c4 = sk_c8 ),
inference(paramod,[status(thm)],[c_2176,c_1954]) ).
cnf(c_2205,plain,
( multiply(sk_c9,A) = multiply(sk_c10,multiply(sk_c10,multiply(sk_c10,A)))
| sk_c4 = sk_c8 ),
inference(paramod,[status(thm)],[c_2176,c_1943]) ).
cnf(c_2235,plain,
( sk_c4 != sk_c8
| multiply(sk_c10,sk_c8) != sk_c9 ),
inference(paramod,[status(thm)],[c_2176,c_1246]) ).
cnf(c_2239,plain,
multiply(sk_c10,sk_c9) = sk_c4,
inference(paramod,[status(thm)],[c_2176,c_452]) ).
cnf(c_2242,plain,
multiply(A,sk_c4) = A,
inference(paramod,[status(thm)],[c_2176,c_375]) ).
cnf(c_2246,plain,
multiply(sk_c4,A) = A,
inference(paramod,[status(thm)],[c_2176,c_1]) ).
cnf(c_2392,plain,
( multiply(inverse(sk_c1),sk_c2) = sk_c10
| sk_c10 = sk_c9 ),
inference(paramod,[status(thm)],[c_2242,c_340]) ).
cnf(c_2274,plain,
( multiply(inverse(sk_c1),sk_c2) = sk_c10
| sk_c9 = sk_c10 ),
inference(copy,[status(thm)],[c_2392]) ).
cnf(c_2393,plain,
( multiply(sk_c10,sk_c8) = sk_c9
| multiply(sk_c10,sk_c8) = sk_c9 ),
inference(paramod,[status(thm)],[c_2246,c_1928]) ).
cnf(c_2289,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(copy,[status(thm)],[c_2393]) ).
cnf(c_2394,plain,
( sk_c4 != sk_c8
| sk_c9 != sk_c9 ),
inference(paramod,[status(thm)],[c_2289,c_2235]) ).
cnf(c_2297,plain,
sk_c4 != sk_c8,
inference(copy,[status(thm)],[c_2394]) ).
cnf(c_2298,plain,
multiply(sk_c9,A) = multiply(sk_c10,multiply(sk_c10,multiply(sk_c10,A))),
inference(resolve,[status(thm)],[c_2297,c_2205]) ).
cnf(c_2395,plain,
( multiply(sk_c10,multiply(sk_c10,multiply(sk_c10,sk_c9))) = sk_c2
| sk_c4 = sk_c8 ),
inference(paramod,[status(thm)],[c_2298,c_2203]) ).
cnf(c_2396,plain,
( multiply(sk_c10,multiply(sk_c10,sk_c4)) = sk_c2
| sk_c4 = sk_c8 ),
inference(paramod,[status(thm)],[c_2239,c_2395]) ).
cnf(c_2397,plain,
( multiply(sk_c10,sk_c10) = sk_c2
| sk_c4 = sk_c8 ),
inference(paramod,[status(thm)],[c_2242,c_2396]) ).
cnf(c_2398,plain,
( sk_c8 = sk_c2
| sk_c4 = sk_c8 ),
inference(paramod,[status(thm)],[c_1256,c_2397]) ).
cnf(c_2399,plain,
( sk_c2 = sk_c8
| sk_c4 = sk_c8 ),
inference(copy,[status(thm)],[c_2398]) ).
cnf(c_2299,plain,
sk_c2 = sk_c8,
inference(resolve,[status(thm)],[c_2297,c_2399]) ).
cnf(c_2305,plain,
inverse(sk_c1) = sk_c10,
inference(resolve,[status(thm)],[c_2297,c_2194]) ).
cnf(c_2400,plain,
( multiply(sk_c10,sk_c2) = sk_c10
| sk_c9 = sk_c10 ),
inference(paramod,[status(thm)],[c_2305,c_2274]) ).
cnf(c_2401,plain,
( multiply(sk_c10,sk_c8) = sk_c10
| sk_c9 = sk_c10 ),
inference(paramod,[status(thm)],[c_2299,c_2400]) ).
cnf(c_2402,plain,
( sk_c9 = sk_c10
| sk_c9 = sk_c10 ),
inference(paramod,[status(thm)],[c_2289,c_2401]) ).
cnf(c_2308,plain,
sk_c9 = sk_c10,
inference(copy,[status(thm)],[c_2402]) ).
cnf(c_2403,plain,
multiply(sk_c10,sk_c10) = sk_c4,
inference(paramod,[status(thm)],[c_2308,c_2239]) ).
cnf(c_2404,plain,
sk_c8 = sk_c4,
inference(paramod,[status(thm)],[c_1256,c_2403]) ).
cnf(c_2405,plain,
sk_c4 = sk_c8,
inference(copy,[status(thm)],[c_2404]) ).
cnf(c_2311,plain,
$false,
inference(resolve,[status(thm)],[c_2297,c_2405]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP362-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n016.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.15/20.68 % CPULimit : 300
% 0.15/20.68 % WCLimit : 300
% 0.15/20.68 % DateTime : Fri Sep 25 14:48:13 UTC 2026
% 0.15/20.69 % CPUTime :
% 0.15/20.69 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/20.69 % Process 668203 was started by sandbox on n013,
% 0.15/20.69 % Fri Sep 25 14:48:13 2026
% 0.15/20.69 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.56/20.70
% 0.56/20.70 % From the command line: assign(max_seconds, 300).
% 9.21/21.87
% 9.21/21.87 % SZS status Unsatisfiable for theBenchmark
% 9.21/21.87
% 9.21/21.87 % Proof 1 at 0.86 (+ 0.27) seconds.
% 9.21/21.87 % Length of proof is 122.
% 9.21/21.87 % Level of proof is 27.
% 9.21/21.87 % Maximum clause weight is 73.000.
% 9.21/21.87 % Given clauses 260.
% 9.21/21.87
% 9.21/21.87 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------