%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP344-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:40 AM UTC 2026
% Result : Unsatisfiable 156.93s 26.31s
% Output : CNFRefutation 156.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 72
% Number of leaves : 17
% Syntax : Number of formulae : 247 ( 42 unt; 0 def)
% Number of atoms : 660 ( 659 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 628 ( 215 ~; 413 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 3 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 : 124 ( 0 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(left_identity,axiom,
! [VAR_0] : multiply(identity,VAR_0) = VAR_0,
file('theBenchmark.p',left_identity) ).
cnf(c_1,plain,
multiply(identity,A) = A,
inference(clausify,[status(thm)],[left_identity]) ).
fof(left_inverse,axiom,
! [VAR_0] : multiply(inverse(VAR_0),VAR_0) = identity,
file('theBenchmark.p',left_inverse) ).
cnf(c_2,plain,
multiply(inverse(A),A) = identity,
inference(clausify,[status(thm)],[left_inverse]) ).
fof(associativity,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(multiply(VAR_0,VAR_1),VAR_2) = multiply(VAR_0,multiply(VAR_1,VAR_2)),
file('theBenchmark.p',associativity) ).
cnf(c_3,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(clausify,[status(thm)],[associativity]) ).
fof(prove_this_1,axiom,
multiply(sk_c6,sk_c7) = sk_c5,
file('theBenchmark.p',prove_this_1) ).
cnf(c_4,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(clausify,[status(thm)],[prove_this_1]) ).
cnf(c_5,plain,
sk_c5 = multiply(sk_c6,sk_c7),
inference(copy,[status(thm)],[c_4]) ).
fof(prove_this_2,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_2) ).
cnf(c_6,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_2]) ).
fof(prove_this_3,axiom,
( inverse(sk_c3) = sk_c6
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_3) ).
cnf(c_7,plain,
( inverse(sk_c3) = sk_c6
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_3]) ).
fof(prove_this_4,axiom,
( inverse(sk_c4) = sk_c5
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_4) ).
cnf(c_8,plain,
( inverse(sk_c4) = sk_c5
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_4]) ).
cnf(c_9,plain,
( inverse(sk_c4) = multiply(sk_c6,sk_c7)
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_5,c_8]) ).
fof(prove_this_5,axiom,
( multiply(sk_c4,sk_c6) = sk_c5
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_5) ).
cnf(c_10,plain,
( multiply(sk_c4,sk_c6) = sk_c5
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_5]) ).
cnf(c_11,plain,
( multiply(sk_c4,sk_c6) = multiply(sk_c6,sk_c7)
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_5,c_10]) ).
fof(prove_this_6,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('theBenchmark.p',prove_this_6) ).
cnf(c_12,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_6]) ).
fof(prove_this_7,axiom,
( inverse(sk_c3) = sk_c6
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('theBenchmark.p',prove_this_7) ).
cnf(c_13,plain,
( inverse(sk_c3) = sk_c6
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_7]) ).
fof(prove_this_8,axiom,
( inverse(sk_c4) = sk_c5
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_14,plain,
( inverse(sk_c4) = sk_c5
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_8]) ).
cnf(c_15,plain,
( inverse(sk_c4) = multiply(sk_c6,sk_c7)
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_5,c_14]) ).
fof(prove_this_9,axiom,
( multiply(sk_c4,sk_c6) = sk_c5
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('theBenchmark.p',prove_this_9) ).
cnf(c_16,plain,
( multiply(sk_c4,sk_c6) = sk_c5
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_9]) ).
cnf(c_17,plain,
( multiply(sk_c4,sk_c6) = multiply(sk_c6,sk_c7)
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_5,c_16]) ).
fof(prove_this_10,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_10) ).
cnf(c_18,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_10]) ).
fof(prove_this_11,axiom,
( inverse(sk_c3) = sk_c6
| inverse(sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_11) ).
cnf(c_19,plain,
( inverse(sk_c3) = sk_c6
| inverse(sk_c2) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_11]) ).
fof(prove_this_14,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c2,sk_c5) = sk_c6 ),
file('theBenchmark.p',prove_this_14) ).
cnf(c_24,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c2,sk_c5) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_14]) ).
cnf(c_25,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c2,multiply(sk_c6,sk_c7)) = sk_c6 ),
inference(paramod,[status(thm)],[c_5,c_24]) ).
fof(prove_this_15,axiom,
( inverse(sk_c3) = sk_c6
| multiply(sk_c2,sk_c5) = sk_c6 ),
file('theBenchmark.p',prove_this_15) ).
cnf(c_26,plain,
( inverse(sk_c3) = sk_c6
| multiply(sk_c2,sk_c5) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_15]) ).
cnf(c_27,plain,
( inverse(sk_c3) = sk_c6
| multiply(sk_c2,multiply(sk_c6,sk_c7)) = sk_c6 ),
inference(paramod,[status(thm)],[c_5,c_26]) ).
fof(prove_this_18,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( multiply(VAR_3,sk_c6) != sk_c5
| inverse(VAR_3) != sk_c5
| inverse(VAR_2) != sk_c6
| multiply(VAR_2,sk_c6) != sk_c7
| multiply(VAR_1,sk_c5) != sk_c6
| inverse(VAR_1) != sk_c6
| multiply(VAR_0,sk_c6) != sk_c7
| inverse(VAR_0) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5 ),
file('theBenchmark.p',prove_this_18) ).
cnf(c_32,plain,
( multiply(D,sk_c6) != sk_c5
| inverse(D) != sk_c5
| inverse(C) != sk_c6
| multiply(C,sk_c6) != sk_c7
| multiply(B,sk_c5) != sk_c6
| inverse(B) != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5 ),
inference(clausify,[status(thm)],[prove_this_18]) ).
cnf(c_26239,plain,
( multiply(D,sk_c6) != sk_c5
| inverse(D) != sk_c5
| inverse(C) != sk_c6
| multiply(C,sk_c6) != sk_c7
| multiply(B,sk_c5) != sk_c6
| inverse(B) != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7
| multiply(sk_c6,sk_c7) != multiply(sk_c6,sk_c7) ),
inference(paramod,[status(thm)],[c_5,c_32]) ).
cnf(c_26240,plain,
( multiply(D,sk_c6) != sk_c5
| inverse(D) != sk_c5
| inverse(C) != sk_c6
| multiply(C,sk_c6) != sk_c7
| multiply(B,multiply(sk_c6,sk_c7)) != sk_c6
| inverse(B) != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7
| multiply(sk_c6,sk_c7) != multiply(sk_c6,sk_c7) ),
inference(paramod,[status(thm)],[c_5,c_26239]) ).
cnf(c_26241,plain,
( multiply(D,sk_c6) != sk_c5
| inverse(D) != multiply(sk_c6,sk_c7)
| inverse(C) != sk_c6
| multiply(C,sk_c6) != sk_c7
| multiply(B,multiply(sk_c6,sk_c7)) != sk_c6
| inverse(B) != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7
| multiply(sk_c6,sk_c7) != multiply(sk_c6,sk_c7) ),
inference(paramod,[status(thm)],[c_5,c_26240]) ).
cnf(c_26242,plain,
( multiply(D,sk_c6) != multiply(sk_c6,sk_c7)
| inverse(D) != multiply(sk_c6,sk_c7)
| inverse(C) != sk_c6
| multiply(C,sk_c6) != sk_c7
| multiply(B,multiply(sk_c6,sk_c7)) != sk_c6
| inverse(B) != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7
| multiply(sk_c6,sk_c7) != multiply(sk_c6,sk_c7) ),
inference(paramod,[status(thm)],[c_5,c_26241]) ).
cnf(c_26243,plain,
( multiply(sk_c6,sk_c7) != multiply(D,sk_c6)
| inverse(D) != multiply(sk_c6,sk_c7)
| inverse(C) != sk_c6
| multiply(C,sk_c6) != sk_c7
| multiply(B,multiply(sk_c6,sk_c7)) != sk_c6
| inverse(B) != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7
| multiply(sk_c6,sk_c7) != multiply(sk_c6,sk_c7) ),
inference(copy,[status(thm)],[c_26242]) ).
cnf(c_33,plain,
( multiply(sk_c6,sk_c7) != multiply(D,sk_c6)
| inverse(D) != multiply(sk_c6,sk_c7)
| inverse(C) != sk_c6
| multiply(C,sk_c6) != sk_c7
| multiply(B,multiply(sk_c6,sk_c7)) != sk_c6
| inverse(B) != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(copy,[status(thm)],[c_26243]) ).
cnf(c_26244,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_26245,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_26244]) ).
cnf(c_37,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_26245]) ).
cnf(c_38,plain,
( multiply(sk_c7,sk_c1) = identity
| multiply(sk_c3,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_6,c_2]) ).
cnf(c_26246,plain,
( multiply(multiply(A,sk_c3),sk_c6) = multiply(A,sk_c7)
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_12,c_3]) ).
cnf(c_43,plain,
( multiply(A,multiply(sk_c3,sk_c6)) = multiply(A,sk_c7)
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_3,c_26246]) ).
cnf(c_48,plain,
( multiply(sk_c6,sk_c2) = identity
| multiply(sk_c3,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_227,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_37]) ).
cnf(c_245,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_37,c_37]) ).
cnf(c_246,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_245,c_227]) ).
cnf(c_247,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_246,c_2]) ).
cnf(c_341,plain,
multiply(A,inverse(A)) = identity,
inference(paramod,[status(thm)],[c_245,c_2]) ).
cnf(c_26247,plain,
multiply(A,identity) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_245,c_246]) ).
cnf(c_26248,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_246,c_26247]) ).
cnf(c_355,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_26248]) ).
cnf(c_26249,plain,
( multiply(sk_c6,sk_c7) != multiply(C,sk_c6)
| inverse(C) != multiply(sk_c6,sk_c7)
| inverse(B) != sk_c6
| multiply(B,sk_c6) != sk_c7
| multiply(inverse(sk_c6),multiply(sk_c6,sk_c7)) != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(resolve,[status(thm)],[c_355,c_33]) ).
cnf(c_372,plain,
( multiply(sk_c6,sk_c7) != multiply(C,sk_c6)
| inverse(C) != multiply(sk_c6,sk_c7)
| inverse(B) != sk_c6
| multiply(B,sk_c6) != sk_c7
| sk_c7 != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(paramod,[status(thm)],[c_37,c_26249]) ).
cnf(c_375,plain,
( inverse(sk_c6) = sk_c3
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_7,c_355]) ).
cnf(c_376,plain,
( inverse(multiply(sk_c6,sk_c7)) = sk_c4
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_9,c_355]) ).
cnf(c_26250,plain,
identity = multiply(A,multiply(B,inverse(multiply(A,B)))),
inference(paramod,[status(thm)],[c_341,c_3]) ).
cnf(c_403,plain,
multiply(A,multiply(B,inverse(multiply(A,B)))) = identity,
inference(copy,[status(thm)],[c_26250]) ).
cnf(c_405,plain,
( multiply(sk_c3,sk_c6) = identity
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_7,c_341]) ).
cnf(c_408,plain,
( multiply(sk_c3,sk_c6) = identity
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_13,c_341]) ).
cnf(c_411,plain,
( multiply(sk_c3,sk_c6) = identity
| inverse(sk_c2) = sk_c6 ),
inference(paramod,[status(thm)],[c_19,c_341]) ).
cnf(c_414,plain,
( multiply(sk_c3,sk_c6) = identity
| multiply(sk_c2,multiply(sk_c6,sk_c7)) = sk_c6 ),
inference(paramod,[status(thm)],[c_27,c_341]) ).
cnf(c_488,plain,
( multiply(sk_c7,multiply(sk_c1,A)) = A
| inverse(sk_c6) = sk_c3 ),
inference(paramod,[status(thm)],[c_375,c_37]) ).
cnf(c_825,plain,
( multiply(sk_c7,sk_c1) = identity
| multiply(sk_c3,sk_c6) = identity ),
inference(paramod,[status(thm)],[c_405,c_2]) ).
cnf(c_846,plain,
( multiply(sk_c6,sk_c2) = identity
| multiply(sk_c3,sk_c6) = identity ),
inference(paramod,[status(thm)],[c_411,c_2]) ).
cnf(c_26251,plain,
multiply(inverse(A),identity) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_403,c_37]) ).
cnf(c_26252,plain,
inverse(A) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_246,c_26251]) ).
cnf(c_1607,plain,
multiply(A,inverse(multiply(B,A))) = inverse(B),
inference(copy,[status(thm)],[c_26252]) ).
cnf(c_26253,plain,
multiply(inverse(A),inverse(B)) = inverse(multiply(B,A)),
inference(paramod,[status(thm)],[c_1607,c_37]) ).
cnf(c_1744,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_26253]) ).
cnf(c_26254,plain,
( multiply(sk_c7,sk_c4) = inverse(sk_c6)
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_376,c_1607]) ).
cnf(c_1751,plain,
( inverse(sk_c6) = multiply(sk_c7,sk_c4)
| inverse(sk_c1) = sk_c7 ),
inference(copy,[status(thm)],[c_26254]) ).
cnf(c_26255,plain,
( identity = sk_c7
| multiply(sk_c1,sk_c6) = sk_c7
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_408,c_12]) ).
cnf(c_1957,plain,
( identity = sk_c7
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(copy,[status(thm)],[c_26255]) ).
cnf(c_26256,plain,
( multiply(A,identity) = multiply(A,sk_c7)
| multiply(sk_c1,sk_c6) = sk_c7
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_408,c_43]) ).
cnf(c_26257,plain,
( A = multiply(A,sk_c7)
| multiply(sk_c1,sk_c6) = sk_c7
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_246,c_26256]) ).
cnf(c_26258,plain,
( multiply(A,sk_c7) = A
| multiply(sk_c1,sk_c6) = sk_c7
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(copy,[status(thm)],[c_26257]) ).
cnf(c_1958,plain,
( multiply(A,sk_c7) = A
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(copy,[status(thm)],[c_26258]) ).
cnf(c_1961,plain,
( multiply(inverse(sk_c1),sk_c7) = sk_c6
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_1957,c_37]) ).
cnf(c_26259,plain,
( multiply(sk_c7,sk_c1) = identity
| identity = sk_c7
| multiply(sk_c7,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_825,c_38]) ).
cnf(c_2053,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c1) = identity ),
inference(copy,[status(thm)],[c_26259]) ).
cnf(c_26260,plain,
( multiply(inverse(sk_c7),identity) = sk_c1
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2053,c_37]) ).
cnf(c_2056,plain,
( inverse(sk_c7) = sk_c1
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_246,c_26260]) ).
cnf(c_2072,plain,
( inverse(sk_c1) = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2056,c_355]) ).
cnf(c_26261,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2072,c_1961]) ).
cnf(c_2117,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_26261]) ).
cnf(c_2182,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2117,c_37]) ).
cnf(c_26262,plain,
( multiply(sk_c6,sk_c2) = identity
| identity = sk_c7
| multiply(sk_c6,sk_c2) = identity ),
inference(paramod,[status(thm)],[c_846,c_48]) ).
cnf(c_2401,plain,
( identity = sk_c7
| multiply(sk_c6,sk_c2) = identity ),
inference(copy,[status(thm)],[c_26262]) ).
cnf(c_26263,plain,
( multiply(identity,A) = multiply(sk_c6,multiply(sk_c2,A))
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2401,c_3]) ).
cnf(c_26264,plain,
( A = multiply(sk_c6,multiply(sk_c2,A))
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_1,c_26263]) ).
cnf(c_2403,plain,
( multiply(sk_c6,multiply(sk_c2,A)) = A
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_26264]) ).
cnf(c_26265,plain,
( multiply(inverse(sk_c6),identity) = sk_c2
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2401,c_37]) ).
cnf(c_2405,plain,
( inverse(sk_c6) = sk_c2
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_246,c_26265]) ).
cnf(c_26266,plain,
( inverse(sk_c7) = multiply(inverse(sk_c6),inverse(sk_c1))
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_1957,c_1744]) ).
cnf(c_2806,plain,
( multiply(inverse(sk_c6),inverse(sk_c1)) = inverse(sk_c7)
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_26266]) ).
cnf(c_26267,plain,
( inverse(sk_c7) = multiply(inverse(sk_c6),inverse(inverse(sk_c7)))
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2182,c_1744]) ).
cnf(c_2830,plain,
( inverse(sk_c7) = multiply(inverse(sk_c6),sk_c7)
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_355,c_26267]) ).
cnf(c_26268,plain,
( inverse(sk_c4) = sk_c6
| multiply(sk_c1,sk_c6) = sk_c7
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_1958,c_15]) ).
cnf(c_3138,plain,
( inverse(sk_c4) = sk_c6
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(copy,[status(thm)],[c_26268]) ).
cnf(c_26269,plain,
( multiply(sk_c4,sk_c6) = sk_c6
| multiply(sk_c1,sk_c6) = sk_c7
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_1958,c_17]) ).
cnf(c_3139,plain,
( multiply(sk_c4,sk_c6) = sk_c6
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(copy,[status(thm)],[c_26269]) ).
cnf(c_3273,plain,
( multiply(sk_c4,sk_c6) = identity
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_3138,c_341]) ).
cnf(c_26270,plain,
( multiply(inverse(sk_c6),sk_c7) = sk_c1
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2830,c_2056]) ).
cnf(c_5627,plain,
( multiply(inverse(sk_c6),sk_c7) = sk_c1
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_26270]) ).
cnf(c_26271,plain,
( inverse(sk_c7) = multiply(sk_c2,sk_c7)
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2405,c_2830]) ).
cnf(c_5640,plain,
( inverse(sk_c7) = multiply(sk_c2,sk_c7)
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_26271]) ).
cnf(c_26272,plain,
( inverse(sk_c1) = multiply(inverse(sk_c7),inverse(inverse(sk_c6)))
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_5627,c_1744]) ).
cnf(c_5710,plain,
( inverse(sk_c1) = multiply(inverse(sk_c7),sk_c6)
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_355,c_26272]) ).
cnf(c_26273,plain,
( multiply(multiply(sk_c2,sk_c7),sk_c6) = sk_c7
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_5640,c_2182]) ).
cnf(c_26274,plain,
( multiply(sk_c2,multiply(sk_c7,sk_c6)) = sk_c7
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_3,c_26273]) ).
cnf(c_6320,plain,
( multiply(sk_c2,multiply(sk_c7,sk_c6)) = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_26274]) ).
cnf(c_26275,plain,
( identity = sk_c6
| multiply(sk_c1,sk_c6) = sk_c7
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_3273,c_3139]) ).
cnf(c_8079,plain,
( identity = sk_c6
| multiply(sk_c1,sk_c6) = sk_c7 ),
inference(copy,[status(thm)],[c_26275]) ).
cnf(c_8347,plain,
( multiply(inverse(sk_c1),sk_c7) = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_8079,c_37]) ).
cnf(c_26276,plain,
( inverse(sk_c7) = multiply(inverse(sk_c6),inverse(sk_c1))
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_8079,c_1744]) ).
cnf(c_8348,plain,
( multiply(inverse(sk_c6),inverse(sk_c1)) = inverse(sk_c7)
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_26276]) ).
cnf(c_26277,plain,
( inverse(sk_c6) = multiply(inverse(sk_c7),inverse(inverse(sk_c1)))
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_8347,c_1744]) ).
cnf(c_26278,plain,
( inverse(sk_c6) = multiply(inverse(sk_c7),sk_c1)
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_355,c_26277]) ).
cnf(c_8375,plain,
( multiply(inverse(sk_c7),sk_c1) = inverse(sk_c6)
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_26278]) ).
cnf(c_26279,plain,
( inverse(sk_c1) = multiply(multiply(sk_c2,sk_c7),sk_c6)
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_5640,c_5710]) ).
cnf(c_26280,plain,
( inverse(sk_c1) = multiply(sk_c2,multiply(sk_c7,sk_c6))
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_3,c_26279]) ).
cnf(c_9538,plain,
( inverse(sk_c1) = multiply(sk_c2,multiply(sk_c7,sk_c6))
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_26280]) ).
cnf(c_26281,plain,
( multiply(sk_c6,sk_c7) = multiply(sk_c7,sk_c6)
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_6320,c_2403]) ).
cnf(c_26282,plain,
( multiply(sk_c7,sk_c6) = multiply(sk_c6,sk_c7)
| identity = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_26281]) ).
cnf(c_9629,plain,
( multiply(sk_c7,sk_c6) = multiply(sk_c6,sk_c7)
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_26282]) ).
cnf(c_26283,plain,
( multiply(inverse(inverse(sk_c7)),inverse(sk_c6)) = sk_c1
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_8375,c_37]) ).
cnf(c_9886,plain,
( multiply(sk_c7,inverse(sk_c6)) = sk_c1
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_355,c_26283]) ).
cnf(c_26284,plain,
( inverse(sk_c1) = multiply(inverse(inverse(sk_c6)),inverse(sk_c7))
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9886,c_1744]) ).
cnf(c_9927,plain,
( inverse(sk_c1) = multiply(sk_c6,inverse(sk_c7))
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_355,c_26284]) ).
cnf(c_10564,plain,
( multiply(sk_c1,multiply(sk_c6,inverse(sk_c7))) = identity
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9927,c_341]) ).
cnf(c_10567,plain,
( inverse(sk_c6) = sk_c3
| multiply(sk_c6,inverse(sk_c7)) = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9927,c_375]) ).
cnf(c_10573,plain,
( multiply(sk_c3,sk_c6) = identity
| multiply(sk_c6,inverse(sk_c7)) = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9927,c_405]) ).
cnf(c_10583,plain,
( inverse(sk_c6) = multiply(sk_c7,sk_c4)
| multiply(sk_c6,inverse(sk_c7)) = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9927,c_1751]) ).
cnf(c_11521,plain,
( inverse(sk_c3) = sk_c6
| multiply(sk_c7,multiply(sk_c1,A)) = A ),
inference(paramod,[status(thm)],[c_488,c_355]) ).
cnf(c_26285,plain,
( multiply(sk_c6,sk_c7) != multiply(B,sk_c6)
| inverse(B) != multiply(sk_c6,sk_c7)
| identity != sk_c6
| multiply(identity,sk_c6) != sk_c7
| sk_c7 != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(paramod,[status(thm)],[c_247,c_372]) ).
cnf(c_26286,plain,
( multiply(sk_c6,sk_c7) != multiply(B,sk_c6)
| inverse(B) != multiply(sk_c6,sk_c7)
| identity != sk_c6
| sk_c6 != sk_c7
| sk_c7 != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(paramod,[status(thm)],[c_1,c_26285]) ).
cnf(c_26287,plain,
( multiply(sk_c6,sk_c7) != multiply(B,sk_c6)
| inverse(B) != multiply(sk_c6,sk_c7)
| identity != sk_c6
| sk_c7 != sk_c6
| sk_c7 != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(copy,[status(thm)],[c_26286]) ).
cnf(c_13597,plain,
( multiply(sk_c6,sk_c7) != multiply(B,sk_c6)
| inverse(B) != multiply(sk_c6,sk_c7)
| identity != sk_c6
| sk_c7 != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(copy,[status(thm)],[c_26287]) ).
cnf(c_26288,plain,
( multiply(sk_c6,sk_c7) != multiply(multiply(C,B),sk_c6)
| multiply(inverse(B),inverse(C)) != multiply(sk_c6,sk_c7)
| identity != sk_c6
| sk_c7 != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(paramod,[status(thm)],[c_1744,c_13597]) ).
cnf(c_14586,plain,
( multiply(sk_c6,sk_c7) != multiply(C,multiply(B,sk_c6))
| multiply(inverse(B),inverse(C)) != multiply(sk_c6,sk_c7)
| identity != sk_c6
| sk_c7 != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(paramod,[status(thm)],[c_3,c_26288]) ).
cnf(c_26289,plain,
( multiply(inverse(sk_c6),sk_c7) = inverse(sk_c7)
| identity = sk_c6
| multiply(sk_c4,sk_c6) = multiply(sk_c6,sk_c7) ),
inference(paramod,[status(thm)],[c_11,c_8348]) ).
cnf(c_14773,plain,
( inverse(sk_c7) = multiply(inverse(sk_c6),sk_c7)
| identity = sk_c6
| multiply(sk_c4,sk_c6) = multiply(sk_c6,sk_c7) ),
inference(copy,[status(thm)],[c_26289]) ).
cnf(c_26290,plain,
( inverse(sk_c1) = multiply(sk_c2,multiply(sk_c6,sk_c7))
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_9629,c_9538]) ).
cnf(c_15248,plain,
( inverse(sk_c1) = multiply(sk_c2,multiply(sk_c6,sk_c7))
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_26290]) ).
cnf(c_26291,plain,
( inverse(sk_c3) = sk_c6
| multiply(sk_c7,identity) = multiply(sk_c6,inverse(sk_c7))
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_10564,c_11521]) ).
cnf(c_26292,plain,
( inverse(sk_c3) = sk_c6
| sk_c7 = multiply(sk_c6,inverse(sk_c7))
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_246,c_26291]) ).
cnf(c_16985,plain,
( inverse(sk_c3) = sk_c6
| multiply(sk_c6,inverse(sk_c7)) = sk_c7
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_26292]) ).
cnf(c_26293,plain,
( identity = sk_c7
| multiply(sk_c2,multiply(sk_c6,sk_c7)) = sk_c6
| multiply(sk_c2,multiply(sk_c6,sk_c7)) = sk_c6 ),
inference(paramod,[status(thm)],[c_414,c_25]) ).
cnf(c_18955,plain,
( identity = sk_c7
| multiply(sk_c2,multiply(sk_c6,sk_c7)) = sk_c6 ),
inference(copy,[status(thm)],[c_26293]) ).
cnf(c_26294,plain,
( inverse(sk_c1) = sk_c6
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_18955,c_15248]) ).
cnf(c_18966,plain,
( inverse(sk_c1) = sk_c6
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_26294]) ).
cnf(c_26295,plain,
( multiply(sk_c6,sk_c7) != multiply(B,identity)
| multiply(inverse(inverse(sk_c6)),inverse(B)) != multiply(sk_c6,sk_c7)
| identity != sk_c6
| sk_c7 != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_14586]) ).
cnf(c_26296,plain,
( multiply(sk_c6,sk_c7) != multiply(B,identity)
| multiply(sk_c6,inverse(B)) != multiply(sk_c6,sk_c7)
| identity != sk_c6
| sk_c7 != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(paramod,[status(thm)],[c_355,c_26295]) ).
cnf(c_18969,plain,
( multiply(sk_c6,sk_c7) != B
| multiply(sk_c6,inverse(B)) != multiply(sk_c6,sk_c7)
| identity != sk_c6
| sk_c7 != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(paramod,[status(thm)],[c_246,c_26296]) ).
cnf(c_26297,plain,
( multiply(sk_c6,sk_c7) != inverse(B)
| multiply(sk_c6,B) != multiply(sk_c6,sk_c7)
| identity != sk_c6
| sk_c7 != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(paramod,[status(thm)],[c_355,c_18969]) ).
cnf(c_26298,plain,
( multiply(sk_c6,sk_c7) != inverse(B)
| multiply(sk_c6,sk_c7) != multiply(sk_c6,B)
| identity != sk_c6
| sk_c7 != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(copy,[status(thm)],[c_26297]) ).
cnf(c_18974,plain,
( inverse(B) != multiply(sk_c6,sk_c7)
| multiply(sk_c6,sk_c7) != multiply(sk_c6,B)
| identity != sk_c6
| sk_c7 != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(copy,[status(thm)],[c_26298]) ).
cnf(c_26299,plain,
( multiply(inverse(sk_c6),sk_c6) = inverse(sk_c7)
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_18966,c_2806]) ).
cnf(c_26300,plain,
( identity = inverse(sk_c7)
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_26299]) ).
cnf(c_26301,plain,
( inverse(sk_c7) = identity
| identity = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_26300]) ).
cnf(c_19024,plain,
( inverse(sk_c7) = identity
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_26301]) ).
cnf(c_26302,plain,
( multiply(sk_c6,sk_c7) != multiply(sk_c6,inverse(multiply(sk_c6,sk_c7)))
| identity != sk_c6
| sk_c7 != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(resolve,[status(thm)],[c_18974,c_355]) ).
cnf(c_26303,plain,
( multiply(sk_c6,sk_c7) != multiply(sk_c6,multiply(inverse(sk_c7),inverse(sk_c6)))
| identity != sk_c6
| sk_c7 != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(paramod,[status(thm)],[c_1744,c_26302]) ).
cnf(c_19127,plain,
( multiply(sk_c6,multiply(inverse(sk_c7),inverse(sk_c6))) != multiply(sk_c6,sk_c7)
| identity != sk_c6
| sk_c7 != sk_c6
| multiply(A,sk_c6) != sk_c7
| inverse(A) != sk_c7 ),
inference(copy,[status(thm)],[c_26303]) ).
cnf(c_26304,plain,
( multiply(sk_c6,multiply(inverse(sk_c7),inverse(sk_c6))) != multiply(sk_c6,sk_c7)
| identity != sk_c6
| sk_c7 != sk_c6
| multiply(inverse(A),sk_c6) != sk_c7
| A != sk_c7 ),
inference(paramod,[status(thm)],[c_355,c_19127]) ).
cnf(c_19133,plain,
( multiply(sk_c6,multiply(inverse(sk_c7),inverse(sk_c6))) != multiply(sk_c6,sk_c7)
| identity != sk_c6
| sk_c7 != sk_c6
| multiply(inverse(A),sk_c6) != sk_c7
| sk_c7 != A ),
inference(copy,[status(thm)],[c_26304]) ).
cnf(c_26305,plain,
( multiply(identity,sk_c7) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_19024,c_2]) ).
cnf(c_26306,plain,
( sk_c7 = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_1,c_26305]) ).
cnf(c_26307,plain,
( identity = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_26306]) ).
cnf(c_19193,plain,
identity = sk_c7,
inference(copy,[status(thm)],[c_26307]) ).
cnf(c_26308,plain,
( multiply(sk_c6,multiply(inverse(sk_c7),inverse(sk_c6))) != multiply(sk_c6,sk_c7)
| sk_c7 != sk_c6
| sk_c7 != sk_c6
| multiply(inverse(A),sk_c6) != sk_c7
| sk_c7 != A ),
inference(paramod,[status(thm)],[c_19193,c_19133]) ).
cnf(c_19208,plain,
( multiply(sk_c6,multiply(inverse(sk_c7),inverse(sk_c6))) != multiply(sk_c6,sk_c7)
| sk_c7 != sk_c6
| multiply(inverse(A),sk_c6) != sk_c7
| sk_c7 != A ),
inference(copy,[status(thm)],[c_26308]) ).
cnf(c_19819,plain,
( inverse(sk_c3) = sk_c6
| multiply(sk_c6,inverse(sk_c7)) = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_19193,c_16985]) ).
cnf(c_20308,plain,
( inverse(sk_c7) = multiply(inverse(sk_c6),sk_c7)
| sk_c7 = sk_c6
| multiply(sk_c4,sk_c6) = multiply(sk_c6,sk_c7) ),
inference(paramod,[status(thm)],[c_19193,c_14773]) ).
cnf(c_22192,plain,
( inverse(sk_c6) = multiply(sk_c7,sk_c4)
| multiply(sk_c6,inverse(sk_c7)) = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_19193,c_10583]) ).
cnf(c_26309,plain,
( multiply(sk_c3,sk_c6) = identity
| multiply(sk_c6,inverse(sk_c7)) = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_19193,c_10573]) ).
cnf(c_22198,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c6,inverse(sk_c7)) = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_19193,c_26309]) ).
cnf(c_22200,plain,
( inverse(sk_c6) = sk_c3
| multiply(sk_c6,inverse(sk_c7)) = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_19193,c_10567]) ).
cnf(c_22838,plain,
( multiply(inverse(sk_c7),sk_c1) = inverse(sk_c6)
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_19193,c_8375]) ).
cnf(c_26086,plain,
multiply(A,inverse(A)) = sk_c7,
inference(paramod,[status(thm)],[c_19193,c_341]) ).
cnf(c_26310,plain,
inverse(sk_c7) = identity,
inference(paramod,[status(thm)],[c_19193,c_247]) ).
cnf(c_26120,plain,
inverse(sk_c7) = sk_c7,
inference(paramod,[status(thm)],[c_19193,c_26310]) ).
cnf(c_26121,plain,
multiply(A,sk_c7) = A,
inference(paramod,[status(thm)],[c_19193,c_246]) ).
cnf(c_26131,plain,
multiply(inverse(A),A) = sk_c7,
inference(paramod,[status(thm)],[c_19193,c_2]) ).
cnf(c_26132,plain,
multiply(sk_c7,A) = A,
inference(paramod,[status(thm)],[c_19193,c_1]) ).
cnf(c_26311,plain,
( multiply(sk_c6,multiply(inverse(sk_c7),inverse(sk_c6))) != multiply(sk_c6,sk_c7)
| multiply(inverse(sk_c6),sk_c6) != sk_c7
| sk_c7 != sk_c6 ),
inference(factor,[status(thm)],[c_19208]) ).
cnf(c_26312,plain,
( multiply(sk_c6,multiply(inverse(sk_c7),inverse(sk_c6))) != multiply(sk_c6,sk_c7)
| sk_c7 != sk_c7
| sk_c7 != sk_c6 ),
inference(paramod,[status(thm)],[c_26131,c_26311]) ).
cnf(c_26313,plain,
( multiply(sk_c6,multiply(sk_c7,inverse(sk_c6))) != multiply(sk_c6,sk_c7)
| sk_c7 != sk_c7
| sk_c7 != sk_c6 ),
inference(paramod,[status(thm)],[c_26120,c_26312]) ).
cnf(c_26314,plain,
( multiply(sk_c6,inverse(sk_c6)) != multiply(sk_c6,sk_c7)
| sk_c7 != sk_c7
| sk_c7 != sk_c6 ),
inference(paramod,[status(thm)],[c_26132,c_26313]) ).
cnf(c_26315,plain,
( sk_c7 != multiply(sk_c6,sk_c7)
| sk_c7 != sk_c7
| sk_c7 != sk_c6 ),
inference(paramod,[status(thm)],[c_26086,c_26314]) ).
cnf(c_26316,plain,
( sk_c7 != sk_c6
| sk_c7 != sk_c7
| sk_c7 != sk_c6 ),
inference(paramod,[status(thm)],[c_26121,c_26315]) ).
cnf(c_26317,plain,
( sk_c7 != sk_c6
| sk_c7 != sk_c6 ),
inference(copy,[status(thm)],[c_26316]) ).
cnf(c_26135,plain,
sk_c7 != sk_c6,
inference(copy,[status(thm)],[c_26317]) ).
cnf(c_26318,plain,
( multiply(sk_c7,sk_c1) = inverse(sk_c6)
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26120,c_22838]) ).
cnf(c_26319,plain,
( sk_c1 = inverse(sk_c6)
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26132,c_26318]) ).
cnf(c_26320,plain,
( inverse(sk_c6) = sk_c1
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_26319]) ).
cnf(c_26207,plain,
inverse(sk_c6) = sk_c1,
inference(resolve,[status(thm)],[c_26135,c_26320]) ).
cnf(c_26321,plain,
( inverse(sk_c6) = sk_c3
| multiply(sk_c6,sk_c7) = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26120,c_22200]) ).
cnf(c_26322,plain,
( inverse(sk_c6) = sk_c3
| sk_c6 = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26121,c_26321]) ).
cnf(c_26323,plain,
( sk_c1 = sk_c3
| sk_c6 = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26207,c_26322]) ).
cnf(c_26324,plain,
( sk_c1 = sk_c3
| sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_26323]) ).
cnf(c_26325,plain,
( sk_c3 = sk_c1
| sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_26324]) ).
cnf(c_26326,plain,
( sk_c3 = sk_c1
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_26325]) ).
cnf(c_26229,plain,
sk_c3 = sk_c1,
inference(resolve,[status(thm)],[c_26135,c_26326]) ).
cnf(c_26327,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c6,sk_c7) = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26120,c_22198]) ).
cnf(c_26328,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| sk_c6 = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26121,c_26327]) ).
cnf(c_26329,plain,
( multiply(sk_c1,sk_c6) = sk_c7
| sk_c6 = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26229,c_26328]) ).
cnf(c_26330,plain,
( multiply(sk_c1,sk_c6) = sk_c7
| sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_26329]) ).
cnf(c_26331,plain,
( multiply(sk_c1,sk_c6) = sk_c7
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_26330]) ).
cnf(c_26230,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(resolve,[status(thm)],[c_26135,c_26331]) ).
cnf(c_26332,plain,
( inverse(sk_c6) = multiply(sk_c7,sk_c4)
| multiply(sk_c6,sk_c7) = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26120,c_22192]) ).
cnf(c_26333,plain,
( inverse(sk_c6) = multiply(sk_c7,sk_c4)
| sk_c6 = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26121,c_26332]) ).
cnf(c_26334,plain,
( sk_c1 = multiply(sk_c7,sk_c4)
| sk_c6 = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26207,c_26333]) ).
cnf(c_26335,plain,
( sk_c1 = sk_c4
| sk_c6 = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26132,c_26334]) ).
cnf(c_26336,plain,
( sk_c1 = sk_c4
| sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_26335]) ).
cnf(c_26337,plain,
( sk_c4 = sk_c1
| sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_26336]) ).
cnf(c_26338,plain,
( sk_c4 = sk_c1
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_26337]) ).
cnf(c_26231,plain,
sk_c4 = sk_c1,
inference(resolve,[status(thm)],[c_26135,c_26338]) ).
cnf(c_26339,plain,
( inverse(sk_c7) = multiply(inverse(sk_c6),sk_c7)
| sk_c7 = sk_c6
| multiply(sk_c1,sk_c6) = multiply(sk_c6,sk_c7) ),
inference(paramod,[status(thm)],[c_26231,c_20308]) ).
cnf(c_26340,plain,
( inverse(sk_c7) = multiply(inverse(sk_c6),sk_c7)
| sk_c7 = sk_c6
| sk_c7 = multiply(sk_c6,sk_c7) ),
inference(paramod,[status(thm)],[c_26230,c_26339]) ).
cnf(c_26341,plain,
( inverse(sk_c7) = multiply(inverse(sk_c6),sk_c7)
| sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26121,c_26340]) ).
cnf(c_26342,plain,
( sk_c7 = multiply(inverse(sk_c6),sk_c7)
| sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26120,c_26341]) ).
cnf(c_26343,plain,
( sk_c7 = multiply(sk_c1,sk_c7)
| sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26207,c_26342]) ).
cnf(c_26344,plain,
( sk_c7 = sk_c1
| sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26121,c_26343]) ).
cnf(c_26345,plain,
( sk_c1 = sk_c7
| sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_26344]) ).
cnf(c_26346,plain,
( sk_c1 = sk_c7
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_26345]) ).
cnf(c_26236,plain,
sk_c1 = sk_c7,
inference(resolve,[status(thm)],[c_26135,c_26346]) ).
cnf(c_26347,plain,
( inverse(sk_c3) = sk_c6
| multiply(sk_c6,sk_c7) = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26120,c_19819]) ).
cnf(c_26348,plain,
( inverse(sk_c3) = sk_c6
| sk_c6 = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26121,c_26347]) ).
cnf(c_26349,plain,
( inverse(sk_c1) = sk_c6
| sk_c6 = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26229,c_26348]) ).
cnf(c_26350,plain,
( inverse(sk_c7) = sk_c6
| sk_c6 = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26236,c_26349]) ).
cnf(c_26351,plain,
( sk_c7 = sk_c6
| sk_c6 = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26120,c_26350]) ).
cnf(c_26352,plain,
( sk_c7 = sk_c6
| sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_26351]) ).
cnf(c_26353,plain,
( sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_26352]) ).
cnf(c_26354,plain,
sk_c7 = sk_c6,
inference(copy,[status(thm)],[c_26353]) ).
cnf(c_26238,plain,
$false,
inference(resolve,[status(thm)],[c_26135,c_26354]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP344-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.38 % Computer : n019.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Fri Sep 25 14:47:10 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/5.38 % Process 3015945 was started by sandbox2 on n019,
% 0.10/5.38 % Fri Sep 25 14:47:10 2026
% 0.10/5.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/5.39
% 0.10/5.39 % From the command line: assign(max_seconds, 300).
% 156.93/26.31
% 156.93/26.31 % given #500 (F,wt=33): 13333 multiply(A,inverse(B)) != sk_c7 | multiply(B,multiply(inverse(A),sk_c6)) != sk_c7 | identity != sk_c6 | multiply(sk_c6,sk_c7) != sk_c6 | multiply(A,inverse(B)) != sk_c6 | multiply(sk_c6,sk_c7) != identity. [para(355(a,1),13047(b,1,1))].
% 156.93/26.31
% 156.93/26.31 % SZS status Unsatisfiable for theBenchmark
% 156.93/26.31
% 156.93/26.31 % Proof 1 at 16.63 (+ 3.99) seconds.
% 156.93/26.31 % Length of proof is 114.
% 156.93/26.31 % Level of proof is 25.
% 156.93/26.31 % Maximum clause weight is 42.000.
% 156.93/26.31 % Given clauses 964.
% 156.93/26.31
% 156.93/26.31 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------