%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP327-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 : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:28:38 AM UTC 2026
% Result : Unsatisfiable 225.31s 30.07s
% Output : CNFRefutation 225.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 19
% Syntax : Number of formulae : 184 ( 34 unt; 0 def)
% Number of atoms : 564 ( 563 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 673 ( 293 ~; 380 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 113 ( 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,
file('theBenchmark.p',prove_this_1) ).
cnf(c_4,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(clausify,[status(thm)],[prove_this_1]) ).
cnf(c_5,plain,
sk_c6 = multiply(sk_c7,sk_c8),
inference(copy,[status(thm)],[c_4]) ).
fof(prove_this_4,axiom,
( inverse(sk_c4) = sk_c8
| multiply(sk_c1,sk_c7) = sk_c8 ),
file('theBenchmark.p',prove_this_4) ).
cnf(c_10,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c1,sk_c7) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_4]) ).
fof(prove_this_5,axiom,
( multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c1,sk_c7) = sk_c8 ),
file('theBenchmark.p',prove_this_5) ).
cnf(c_11,plain,
( multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c1,sk_c7) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_5]) ).
fof(prove_this_7,axiom,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c8 ),
file('theBenchmark.p',prove_this_7) ).
cnf(c_13,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_7]) ).
cnf(c_14,plain,
( multiply(sk_c5,multiply(sk_c7,sk_c8)) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_5,c_13]) ).
fof(prove_this_9,axiom,
( multiply(sk_c6,sk_c8) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_9) ).
cnf(c_17,plain,
( multiply(sk_c6,sk_c8) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_9]) ).
cnf(c_35669,plain,
( multiply(multiply(sk_c7,sk_c8),sk_c8) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_5,c_17]) ).
cnf(c_18,plain,
( multiply(sk_c7,multiply(sk_c8,sk_c8)) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_3,c_35669]) ).
fof(prove_this_10,axiom,
( inverse(sk_c4) = sk_c8
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_10) ).
cnf(c_19,plain,
( inverse(sk_c4) = sk_c8
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_10]) ).
fof(prove_this_11,axiom,
( multiply(sk_c4,sk_c7) = sk_c8
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_11) ).
cnf(c_20,plain,
( multiply(sk_c4,sk_c7) = sk_c8
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_11]) ).
fof(prove_this_12,axiom,
( inverse(sk_c5) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_12) ).
cnf(c_21,plain,
( inverse(sk_c5) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_12]) ).
fof(prove_this_13,axiom,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_13) ).
cnf(c_22,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_13]) ).
cnf(c_23,plain,
( multiply(sk_c5,multiply(sk_c7,sk_c8)) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_5,c_22]) ).
fof(prove_this_18,axiom,
( inverse(sk_c5) = sk_c7
| multiply(sk_c8,sk_c3) = sk_c7 ),
file('theBenchmark.p',prove_this_18) ).
cnf(c_30,plain,
( inverse(sk_c5) = sk_c7
| multiply(sk_c8,sk_c3) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_18]) ).
fof(prove_this_19,axiom,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c8,sk_c3) = sk_c7 ),
file('theBenchmark.p',prove_this_19) ).
cnf(c_31,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c8,sk_c3) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_19]) ).
cnf(c_32,plain,
( multiply(sk_c5,multiply(sk_c7,sk_c8)) = sk_c7
| multiply(sk_c8,sk_c3) = sk_c7 ),
inference(paramod,[status(thm)],[c_5,c_31]) ).
fof(prove_this_24,axiom,
( inverse(sk_c5) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c3 ),
file('theBenchmark.p',prove_this_24) ).
cnf(c_39,plain,
( inverse(sk_c5) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_24]) ).
fof(prove_this_25,axiom,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c3 ),
file('theBenchmark.p',prove_this_25) ).
cnf(c_40,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_25]) ).
cnf(c_41,plain,
( multiply(sk_c5,multiply(sk_c7,sk_c8)) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c3 ),
inference(paramod,[status(thm)],[c_5,c_40]) ).
fof(prove_this_30,axiom,
( inverse(sk_c5) = sk_c7
| inverse(sk_c2) = sk_c8 ),
file('theBenchmark.p',prove_this_30) ).
cnf(c_48,plain,
( inverse(sk_c5) = sk_c7
| inverse(sk_c2) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_30]) ).
fof(prove_this_31,axiom,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c8 ),
file('theBenchmark.p',prove_this_31) ).
cnf(c_49,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_31]) ).
cnf(c_50,plain,
( multiply(sk_c5,multiply(sk_c7,sk_c8)) = sk_c7
| inverse(sk_c2) = sk_c8 ),
inference(paramod,[status(thm)],[c_5,c_49]) ).
fof(prove_this_32,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_c6,sk_c8) != sk_c7
| inverse(sk_c7) != sk_c6
| inverse(VAR_2) != sk_c8
| multiply(VAR_2,sk_c8) != VAR_1
| multiply(sk_c8,VAR_1) != sk_c7
| inverse(VAR_0) != sk_c7
| multiply(VAR_0,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6 ),
file('theBenchmark.p',prove_this_32) ).
cnf(c_51,plain,
( multiply(E,sk_c6) != sk_c7
| inverse(E) != sk_c7
| multiply(D,sk_c7) != sk_c8
| inverse(D) != sk_c8
| multiply(sk_c6,sk_c8) != sk_c7
| inverse(sk_c7) != sk_c6
| inverse(C) != sk_c8
| multiply(C,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6 ),
inference(clausify,[status(thm)],[prove_this_32]) ).
cnf(c_35670,plain,
( multiply(E,sk_c6) != sk_c7
| inverse(E) != sk_c7
| multiply(D,sk_c7) != sk_c8
| inverse(D) != sk_c8
| multiply(sk_c6,sk_c8) != sk_c7
| inverse(sk_c7) != sk_c6
| inverse(C) != sk_c8
| multiply(C,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != multiply(sk_c7,sk_c8) ),
inference(paramod,[status(thm)],[c_5,c_51]) ).
cnf(c_35671,plain,
( multiply(E,sk_c6) != sk_c7
| inverse(E) != sk_c7
| multiply(D,sk_c7) != sk_c8
| inverse(D) != sk_c8
| multiply(sk_c6,sk_c8) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| inverse(C) != sk_c8
| multiply(C,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != multiply(sk_c7,sk_c8) ),
inference(paramod,[status(thm)],[c_5,c_35670]) ).
cnf(c_35672,plain,
( multiply(E,sk_c6) != sk_c7
| inverse(E) != sk_c7
| multiply(D,sk_c7) != sk_c8
| inverse(D) != sk_c8
| multiply(multiply(sk_c7,sk_c8),sk_c8) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| inverse(C) != sk_c8
| multiply(C,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != multiply(sk_c7,sk_c8) ),
inference(paramod,[status(thm)],[c_5,c_35671]) ).
cnf(c_35673,plain,
( multiply(E,sk_c6) != sk_c7
| inverse(E) != sk_c7
| multiply(D,sk_c7) != sk_c8
| inverse(D) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| inverse(C) != sk_c8
| multiply(C,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != multiply(sk_c7,sk_c8) ),
inference(paramod,[status(thm)],[c_3,c_35672]) ).
cnf(c_35674,plain,
( multiply(E,multiply(sk_c7,sk_c8)) != sk_c7
| inverse(E) != sk_c7
| multiply(D,sk_c7) != sk_c8
| inverse(D) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| inverse(C) != sk_c8
| multiply(C,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != multiply(sk_c7,sk_c8) ),
inference(paramod,[status(thm)],[c_5,c_35673]) ).
cnf(c_52,plain,
( multiply(E,multiply(sk_c7,sk_c8)) != sk_c7
| inverse(E) != sk_c7
| multiply(D,sk_c7) != sk_c8
| inverse(D) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| inverse(C) != sk_c8
| multiply(C,sk_c8) != B
| multiply(sk_c8,B) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8 ),
inference(copy,[status(thm)],[c_35674]) ).
cnf(c_35675,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_35676,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_35675]) ).
cnf(c_68,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_35676]) ).
cnf(c_79,plain,
( multiply(sk_c7,sk_c1) = identity
| multiply(sk_c7,multiply(sk_c8,sk_c8)) = sk_c7 ),
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_81,plain,
( multiply(sk_c7,sk_c1) = identity
| multiply(sk_c4,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_20,c_2]) ).
cnf(c_83,plain,
( multiply(sk_c7,sk_c1) = identity
| multiply(sk_c5,multiply(sk_c7,sk_c8)) = sk_c7 ),
inference(paramod,[status(thm)],[c_23,c_2]) ).
cnf(c_90,plain,
( multiply(sk_c7,sk_c5) = identity
| multiply(sk_c8,sk_c3) = sk_c7 ),
inference(paramod,[status(thm)],[c_30,c_2]) ).
cnf(c_99,plain,
( multiply(sk_c7,sk_c5) = identity
| multiply(sk_c2,sk_c8) = sk_c3 ),
inference(paramod,[status(thm)],[c_39,c_2]) ).
cnf(c_106,plain,
( multiply(sk_c7,sk_c5) = identity
| inverse(sk_c2) = sk_c8 ),
inference(paramod,[status(thm)],[c_48,c_2]) ).
cnf(c_107,plain,
( multiply(sk_c8,sk_c2) = identity
| multiply(sk_c5,multiply(sk_c7,sk_c8)) = sk_c7 ),
inference(paramod,[status(thm)],[c_50,c_2]) ).
cnf(c_116,plain,
( multiply(C,multiply(sk_c7,sk_c8)) != sk_c7
| inverse(C) != sk_c7
| multiply(B,sk_c7) != sk_c8
| inverse(B) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| inverse(inverse(sk_c8)) != sk_c8
| multiply(sk_c8,identity) != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8 ),
inference(resolve,[status(thm)],[c_52,c_2]) ).
cnf(c_978,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_68]) ).
cnf(c_983,plain,
( multiply(inverse(sk_c4),sk_c8) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_11,c_68]) ).
cnf(c_1010,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_68,c_68]) ).
cnf(c_1011,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_1010,c_978]) ).
cnf(c_1019,plain,
( multiply(C,multiply(sk_c7,sk_c8)) != sk_c7
| inverse(C) != sk_c7
| multiply(B,sk_c7) != sk_c8
| inverse(B) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| inverse(inverse(sk_c8)) != sk_c8
| sk_c8 != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8 ),
inference(paramod,[status(thm)],[c_1011,c_116]) ).
cnf(c_1020,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_1011,c_2]) ).
cnf(c_1263,plain,
multiply(A,inverse(A)) = identity,
inference(paramod,[status(thm)],[c_1010,c_2]) ).
cnf(c_35677,plain,
multiply(A,identity) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_1010,c_1011]) ).
cnf(c_35678,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_1011,c_35677]) ).
cnf(c_1294,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_35678]) ).
cnf(c_35679,plain,
( multiply(C,multiply(sk_c7,sk_c8)) != sk_c7
| inverse(C) != sk_c7
| multiply(B,sk_c7) != sk_c8
| inverse(B) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| sk_c8 != sk_c8
| sk_c8 != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8 ),
inference(paramod,[status(thm)],[c_1294,c_1019]) ).
cnf(c_1299,plain,
( multiply(C,multiply(sk_c7,sk_c8)) != sk_c7
| inverse(C) != sk_c7
| multiply(B,sk_c7) != sk_c8
| inverse(B) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| sk_c8 != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8 ),
inference(copy,[status(thm)],[c_35679]) ).
cnf(c_1337,plain,
( inverse(sk_c8) = sk_c4
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_19,c_1294]) ).
cnf(c_35680,plain,
identity = multiply(A,multiply(B,inverse(multiply(A,B)))),
inference(paramod,[status(thm)],[c_1263,c_3]) ).
cnf(c_1419,plain,
multiply(A,multiply(B,inverse(multiply(A,B)))) = identity,
inference(copy,[status(thm)],[c_35680]) ).
cnf(c_1427,plain,
( multiply(sk_c5,sk_c7) = identity
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_21,c_1263]) ).
cnf(c_1509,plain,
( multiply(sk_c7,sk_c1) = identity
| inverse(sk_c8) = sk_c4 ),
inference(paramod,[status(thm)],[c_1337,c_2]) ).
cnf(c_3357,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c5,sk_c7) = identity ),
inference(paramod,[status(thm)],[c_1427,c_1263]) ).
cnf(c_3557,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c7,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_1509,c_1294]) ).
cnf(c_35681,plain,
( multiply(inverse(sk_c7),sk_c7) = multiply(sk_c8,sk_c8)
| multiply(sk_c7,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_79,c_68]) ).
cnf(c_35682,plain,
( identity = multiply(sk_c8,sk_c8)
| multiply(sk_c7,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_2,c_35681]) ).
cnf(c_4315,plain,
( multiply(sk_c8,sk_c8) = identity
| multiply(sk_c7,sk_c1) = identity ),
inference(copy,[status(thm)],[c_35682]) ).
cnf(c_4780,plain,
( multiply(inverse(sk_c4),sk_c8) = sk_c7
| multiply(sk_c7,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_81,c_68]) ).
cnf(c_5750,plain,
( multiply(inverse(sk_c2),sk_c3) = sk_c8
| multiply(sk_c7,sk_c5) = identity ),
inference(paramod,[status(thm)],[c_99,c_68]) ).
cnf(c_35683,plain,
multiply(inverse(A),identity) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_1419,c_68]) ).
cnf(c_35684,plain,
inverse(A) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_1011,c_35683]) ).
cnf(c_6527,plain,
multiply(A,inverse(multiply(B,A))) = inverse(B),
inference(copy,[status(thm)],[c_35684]) ).
cnf(c_35685,plain,
multiply(inverse(A),inverse(B)) = inverse(multiply(B,A)),
inference(paramod,[status(thm)],[c_6527,c_68]) ).
cnf(c_6568,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_35685]) ).
cnf(c_35686,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c8
| multiply(sk_c1,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_10,c_983]) ).
cnf(c_20390,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c8 ),
inference(copy,[status(thm)],[c_35686]) ).
cnf(c_35687,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| multiply(sk_c7,sk_c1) = identity
| multiply(sk_c7,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_3557,c_4780]) ).
cnf(c_21777,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| multiply(sk_c7,sk_c1) = identity ),
inference(copy,[status(thm)],[c_35687]) ).
cnf(c_35688,plain,
( sk_c7 = identity
| multiply(sk_c7,sk_c1) = identity
| multiply(sk_c7,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_21777,c_4315]) ).
cnf(c_35689,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c1) = identity
| multiply(sk_c7,sk_c1) = identity ),
inference(copy,[status(thm)],[c_35688]) ).
cnf(c_21807,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c1) = identity ),
inference(copy,[status(thm)],[c_35689]) ).
cnf(c_35690,plain,
( multiply(inverse(sk_c7),identity) = sk_c1
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_21807,c_68]) ).
cnf(c_21814,plain,
( inverse(sk_c7) = sk_c1
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_1011,c_35690]) ).
cnf(c_21830,plain,
( multiply(sk_c1,sk_c7) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_21814,c_2]) ).
cnf(c_21930,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| identity = sk_c8
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_21830,c_20390]) ).
cnf(c_35691,plain,
( multiply(sk_c8,sk_c3) = sk_c8
| multiply(sk_c7,sk_c5) = identity
| multiply(sk_c7,sk_c5) = identity ),
inference(paramod,[status(thm)],[c_106,c_5750]) ).
cnf(c_24747,plain,
( multiply(sk_c8,sk_c3) = sk_c8
| multiply(sk_c7,sk_c5) = identity ),
inference(copy,[status(thm)],[c_35691]) ).
cnf(c_35692,plain,
( multiply(sk_c7,sk_c5) = identity
| sk_c8 = sk_c7
| multiply(sk_c7,sk_c5) = identity ),
inference(paramod,[status(thm)],[c_24747,c_90]) ).
cnf(c_24758,plain,
( sk_c8 = sk_c7
| multiply(sk_c7,sk_c5) = identity ),
inference(copy,[status(thm)],[c_35692]) ).
cnf(c_35693,plain,
( multiply(inverse(sk_c7),identity) = sk_c5
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_24758,c_68]) ).
cnf(c_24764,plain,
( inverse(sk_c7) = sk_c5
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_1011,c_35693]) ).
cnf(c_24781,plain,
( multiply(sk_c5,multiply(sk_c7,A)) = A
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_24764,c_68]) ).
cnf(c_35694,plain,
( multiply(inverse(sk_c7),multiply(sk_c7,sk_c8)) != sk_c7
| multiply(B,sk_c7) != sk_c8
| inverse(B) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| sk_c8 != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8 ),
inference(resolve,[status(thm)],[c_1299,c_1294]) ).
cnf(c_35695,plain,
( sk_c8 != sk_c7
| multiply(B,sk_c7) != sk_c8
| inverse(B) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| sk_c8 != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8 ),
inference(paramod,[status(thm)],[c_68,c_35694]) ).
cnf(c_24961,plain,
( multiply(B,sk_c7) != sk_c8
| inverse(B) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| sk_c8 != sk_c7
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c8 ),
inference(copy,[status(thm)],[c_35695]) ).
cnf(c_35696,plain,
( multiply(A,sk_c7) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| sk_c8 != sk_c7
| identity != sk_c7
| multiply(identity,sk_c7) != sk_c8 ),
inference(paramod,[status(thm)],[c_1020,c_24961]) ).
cnf(c_35697,plain,
( multiply(A,sk_c7) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| sk_c8 != sk_c7
| identity != sk_c7
| sk_c7 != sk_c8 ),
inference(paramod,[status(thm)],[c_1,c_35696]) ).
cnf(c_35698,plain,
( multiply(A,sk_c7) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| sk_c8 != sk_c7
| identity != sk_c7
| sk_c8 != sk_c7 ),
inference(copy,[status(thm)],[c_35697]) ).
cnf(c_24969,plain,
( multiply(A,sk_c7) != sk_c8
| inverse(A) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| identity != sk_c7
| sk_c8 != sk_c7 ),
inference(copy,[status(thm)],[c_35698]) ).
cnf(c_35699,plain,
( multiply(multiply(B,A),sk_c7) != sk_c8
| multiply(inverse(A),inverse(B)) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| identity != sk_c7
| sk_c8 != sk_c7 ),
inference(paramod,[status(thm)],[c_6568,c_24969]) ).
cnf(c_25103,plain,
( multiply(B,multiply(A,sk_c7)) != sk_c8
| multiply(inverse(A),inverse(B)) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| identity != sk_c7
| sk_c8 != sk_c7 ),
inference(paramod,[status(thm)],[c_3,c_35699]) ).
cnf(c_35700,plain,
( multiply(A,identity) != sk_c8
| multiply(inverse(inverse(sk_c7)),inverse(A)) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| identity != sk_c7
| sk_c8 != sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_25103]) ).
cnf(c_35701,plain,
( multiply(A,identity) != sk_c8
| multiply(sk_c7,inverse(A)) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| identity != sk_c7
| sk_c8 != sk_c7 ),
inference(paramod,[status(thm)],[c_1294,c_35700]) ).
cnf(c_35702,plain,
( A != sk_c8
| multiply(sk_c7,inverse(A)) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| identity != sk_c7
| sk_c8 != sk_c7 ),
inference(paramod,[status(thm)],[c_1011,c_35701]) ).
cnf(c_25129,plain,
( sk_c8 != A
| multiply(sk_c7,inverse(A)) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| identity != sk_c7
| sk_c8 != sk_c7 ),
inference(copy,[status(thm)],[c_35702]) ).
cnf(c_35703,plain,
( sk_c8 != inverse(A)
| multiply(sk_c7,A) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| identity != sk_c7
| sk_c8 != sk_c7 ),
inference(paramod,[status(thm)],[c_1294,c_25129]) ).
cnf(c_25175,plain,
( inverse(A) != sk_c8
| multiply(sk_c7,A) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| identity != sk_c7
| sk_c8 != sk_c7 ),
inference(copy,[status(thm)],[c_35703]) ).
cnf(c_35704,plain,
( sk_c8 = sk_c7
| multiply(sk_c1,sk_c7) = sk_c8
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_24781,c_14]) ).
cnf(c_25199,plain,
( multiply(sk_c1,sk_c7) = sk_c8
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_35704]) ).
cnf(c_35705,plain,
( sk_c8 = sk_c7
| multiply(sk_c8,sk_c3) = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_24781,c_32]) ).
cnf(c_25200,plain,
( multiply(sk_c8,sk_c3) = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_35705]) ).
cnf(c_35706,plain,
( sk_c8 = sk_c7
| multiply(sk_c2,sk_c8) = sk_c3
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_24781,c_41]) ).
cnf(c_25201,plain,
( multiply(sk_c2,sk_c8) = sk_c3
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_35706]) ).
cnf(c_35707,plain,
( multiply(sk_c7,sk_c1) = identity
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_24781,c_83]) ).
cnf(c_25203,plain,
( multiply(sk_c7,sk_c1) = identity
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_35707]) ).
cnf(c_35708,plain,
( multiply(sk_c8,sk_c2) = identity
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_24781,c_107]) ).
cnf(c_25206,plain,
( multiply(sk_c8,sk_c2) = identity
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_35708]) ).
cnf(c_25251,plain,
( multiply(sk_c7,inverse(sk_c8)) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| identity != sk_c7
| sk_c8 != sk_c7 ),
inference(resolve,[status(thm)],[c_25175,c_1294]) ).
cnf(c_35709,plain,
( multiply(sk_c5,identity) = sk_c1
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_25203,c_24781]) ).
cnf(c_35710,plain,
( sk_c5 = sk_c1
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_1011,c_35709]) ).
cnf(c_25305,plain,
( sk_c5 = sk_c1
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_35710]) ).
cnf(c_35711,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c1,sk_c7) = identity
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_25305,c_3357]) ).
cnf(c_25309,plain,
( multiply(sk_c1,sk_c7) = identity
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_35711]) ).
cnf(c_35712,plain,
( multiply(inverse(sk_c8),identity) = sk_c2
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_25206,c_68]) ).
cnf(c_25644,plain,
( inverse(sk_c8) = sk_c2
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_1011,c_35712]) ).
cnf(c_25649,plain,
( multiply(sk_c2,sk_c8) = identity
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_25644,c_2]) ).
cnf(c_35713,plain,
( identity = sk_c8
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_25309,c_25199]) ).
cnf(c_25687,plain,
( identity = sk_c8
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_35713]) ).
cnf(c_25722,plain,
( multiply(sk_c8,A) = A
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_25687,c_1]) ).
cnf(c_35714,plain,
( identity = sk_c3
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_25649,c_25201]) ).
cnf(c_25890,plain,
( identity = sk_c3
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_35714]) ).
cnf(c_35715,plain,
( sk_c3 = sk_c8
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_25890,c_25687]) ).
cnf(c_25940,plain,
( sk_c3 = sk_c8
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_35715]) ).
cnf(c_35716,plain,
( sk_c3 = sk_c7
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_25722,c_25200]) ).
cnf(c_26036,plain,
( sk_c3 = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_35716]) ).
cnf(c_35717,plain,
( sk_c7 = sk_c8
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_26036,c_25940]) ).
cnf(c_35718,plain,
( sk_c8 = sk_c7
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_35717]) ).
cnf(c_35719,plain,
( sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_35718]) ).
cnf(c_26046,plain,
sk_c8 = sk_c7,
inference(copy,[status(thm)],[c_35719]) ).
cnf(c_35720,plain,
( multiply(sk_c7,inverse(sk_c8)) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c8)
| identity != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_26046,c_25251]) ).
cnf(c_35721,plain,
( multiply(sk_c7,inverse(sk_c8)) != sk_c8
| multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c7)
| identity != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_26046,c_35720]) ).
cnf(c_35722,plain,
( multiply(sk_c7,inverse(sk_c8)) != sk_c8
| multiply(sk_c7,multiply(sk_c7,sk_c8)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c7)
| identity != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_26046,c_35721]) ).
cnf(c_35723,plain,
( multiply(sk_c7,inverse(sk_c8)) != sk_c8
| multiply(sk_c7,multiply(sk_c7,sk_c7)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c7)
| identity != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_26046,c_35722]) ).
cnf(c_35724,plain,
( multiply(sk_c7,inverse(sk_c7)) != sk_c8
| multiply(sk_c7,multiply(sk_c7,sk_c7)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c7)
| identity != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_26046,c_35723]) ).
cnf(c_35725,plain,
( identity != sk_c8
| multiply(sk_c7,multiply(sk_c7,sk_c7)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c7)
| identity != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_1263,c_35724]) ).
cnf(c_35726,plain,
( identity != sk_c7
| multiply(sk_c7,multiply(sk_c7,sk_c7)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c7)
| identity != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_26046,c_35725]) ).
cnf(c_35727,plain,
( identity != sk_c7
| multiply(sk_c7,multiply(sk_c7,sk_c7)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c7)
| identity != sk_c7 ),
inference(copy,[status(thm)],[c_35726]) ).
cnf(c_26308,plain,
( multiply(sk_c7,multiply(sk_c7,sk_c7)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c7)
| identity != sk_c7 ),
inference(copy,[status(thm)],[c_35727]) ).
cnf(c_35728,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_26046,c_21930]) ).
cnf(c_35729,plain,
( multiply(sk_c7,sk_c8) = sk_c7
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_26046,c_35728]) ).
cnf(c_35730,plain,
( multiply(sk_c7,sk_c7) = sk_c7
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_26046,c_35729]) ).
cnf(c_27209,plain,
( multiply(sk_c7,sk_c7) = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_35730]) ).
cnf(c_35731,plain,
( multiply(inverse(sk_c7),sk_c7) = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_27209,c_68]) ).
cnf(c_35732,plain,
( identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_35731]) ).
cnf(c_34007,plain,
identity = sk_c7,
inference(copy,[status(thm)],[c_35732]) ).
cnf(c_35733,plain,
( multiply(sk_c7,multiply(sk_c7,sk_c7)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c7)
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_34007,c_26308]) ).
cnf(c_35451,plain,
( multiply(sk_c7,multiply(sk_c7,sk_c7)) != sk_c7
| inverse(sk_c7) != multiply(sk_c7,sk_c7) ),
inference(copy,[status(thm)],[c_35733]) ).
cnf(c_35734,plain,
inverse(sk_c7) = identity,
inference(paramod,[status(thm)],[c_34007,c_1020]) ).
cnf(c_35648,plain,
inverse(sk_c7) = sk_c7,
inference(paramod,[status(thm)],[c_34007,c_35734]) ).
cnf(c_35649,plain,
multiply(A,sk_c7) = A,
inference(paramod,[status(thm)],[c_34007,c_1011]) ).
cnf(c_35735,plain,
( multiply(sk_c7,multiply(sk_c7,sk_c7)) != sk_c7
| sk_c7 != multiply(sk_c7,sk_c7) ),
inference(paramod,[status(thm)],[c_35648,c_35451]) ).
cnf(c_35736,plain,
( multiply(sk_c7,multiply(sk_c7,sk_c7)) != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_35649,c_35735]) ).
cnf(c_35737,plain,
( multiply(sk_c7,sk_c7) != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_35649,c_35736]) ).
cnf(c_35738,plain,
( sk_c7 != sk_c7
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_35649,c_35737]) ).
cnf(c_35739,plain,
sk_c7 != sk_c7,
inference(copy,[status(thm)],[c_35738]) ).
cnf(c_35668,plain,
$false,
inference(copy,[status(thm)],[c_35739]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP327-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n003.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Fri Sep 25 14:47:38 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/0.44 % Process 437740 was started by sandbox2 on n003,
% 0.16/0.44 % Fri Sep 25 14:47:38 2026
% 0.16/0.44 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.16/0.44
% 0.16/0.44 % From the command line: assign(max_seconds, 300).
% 225.31/30.07
% 225.31/30.07 % given #500 (T,wt=9): 16850 identity = sk_c8 | inverse(sk_c7) = multiply(sk_c8,sk_c7). [para(7561(b,1),15469(b,1,2)),flip(c),merge(b)].
% 225.31/30.07
% 225.31/30.07 % given #1000 (F,wt=44): 22510 multiply(A,B) != sk_c8 | multiply(sk_c7,multiply(inverse(B),inverse(A))) != sk_c7 | sk_c8 != sk_c7 | multiply(C,sk_c8) != identity | inverse(C) != sk_c8 | inverse(sk_c7) != multiply(sk_c7,sk_c8) | multiply(sk_c7,multiply(sk_c8,sk_c8)) != sk_c7 | multiply(C,sk_c7) != sk_c8. [para(6568(a,1),22501(b,1,2)),flip(a)].
% 225.31/30.07
% 225.31/30.07 % SZS status Unsatisfiable for theBenchmark
% 225.31/30.07
% 225.31/30.07 % Proof 1 at 25.95 (+ 3.45) seconds.
% 225.31/30.07 % Length of proof is 94.
% 225.31/30.07 % Level of proof is 17.
% 225.31/30.07 % Maximum clause weight is 56.000.
% 225.31/30.07 % Given clauses 1182.
% 225.31/30.07
% 225.31/30.07 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------