%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP255-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 : n008.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:29 AM UTC 2026
% Result : Unsatisfiable 198.16s 25.81s
% Output : CNFRefutation 198.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 22
% Syntax : Number of formulae : 205 ( 27 unt; 0 def)
% Number of atoms : 548 ( 547 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 540 ( 197 ~; 343 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 3 avg)
% Maximal term depth : 4 ( 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 : 77 ( 0 sgn 10 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(left_identity,axiom,
! [VAR_0] : multiply(identity,VAR_0) = VAR_0,
file('theBenchmark.p',left_identity) ).
cnf(c_1,plain,
multiply(identity,A) = A,
inference(clausify,[status(thm)],[left_identity]) ).
fof(left_inverse,axiom,
! [VAR_0] : multiply(inverse(VAR_0),VAR_0) = identity,
file('theBenchmark.p',left_inverse) ).
cnf(c_2,plain,
multiply(inverse(A),A) = identity,
inference(clausify,[status(thm)],[left_inverse]) ).
fof(associativity,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(multiply(VAR_0,VAR_1),VAR_2) = multiply(VAR_0,multiply(VAR_1,VAR_2)),
file('theBenchmark.p',associativity) ).
cnf(c_3,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(clausify,[status(thm)],[associativity]) ).
fof(prove_this_1,axiom,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_1) ).
cnf(c_4,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_1]) ).
fof(prove_this_2,axiom,
( inverse(sk_c4) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_2) ).
cnf(c_5,plain,
( inverse(sk_c4) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_2]) ).
fof(prove_this_3,axiom,
( multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_3) ).
cnf(c_6,plain,
( multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_3]) ).
fof(prove_this_4,axiom,
( inverse(sk_c5) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_4) ).
cnf(c_7,plain,
( inverse(sk_c5) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_4]) ).
fof(prove_this_5,axiom,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_5) ).
cnf(c_8,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_5]) ).
fof(prove_this_6,axiom,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_6) ).
cnf(c_9,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_6]) ).
fof(prove_this_7,axiom,
( inverse(sk_c4) = sk_c8
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_7) ).
cnf(c_10,plain,
( inverse(sk_c4) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_7]) ).
fof(prove_this_8,axiom,
( multiply(sk_c4,sk_c7) = sk_c8
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_11,plain,
( multiply(sk_c4,sk_c7) = sk_c8
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_8]) ).
fof(prove_this_9,axiom,
( inverse(sk_c5) = sk_c7
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_9) ).
cnf(c_12,plain,
( inverse(sk_c5) = sk_c7
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_9]) ).
fof(prove_this_10,axiom,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c8 ),
file('theBenchmark.p',prove_this_10) ).
cnf(c_13,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_10]) ).
fof(prove_this_11,axiom,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c2,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_11) ).
cnf(c_14,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c2,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_11]) ).
fof(prove_this_14,axiom,
( inverse(sk_c5) = sk_c7
| multiply(sk_c2,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_14) ).
cnf(c_17,plain,
( inverse(sk_c5) = sk_c7
| multiply(sk_c2,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_14]) ).
fof(prove_this_15,axiom,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c2,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_15) ).
cnf(c_18,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c2,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_15]) ).
fof(prove_this_16,axiom,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c2) = sk_c7 ),
file('theBenchmark.p',prove_this_16) ).
cnf(c_19,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c2) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_16]) ).
fof(prove_this_19,axiom,
( inverse(sk_c5) = sk_c7
| inverse(sk_c2) = sk_c7 ),
file('theBenchmark.p',prove_this_19) ).
cnf(c_22,plain,
( inverse(sk_c5) = sk_c7
| inverse(sk_c2) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_19]) ).
fof(prove_this_20,axiom,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c7 ),
file('theBenchmark.p',prove_this_20) ).
cnf(c_23,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_20]) ).
fof(prove_this_21,axiom,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c3) = sk_c6 ),
file('theBenchmark.p',prove_this_21) ).
cnf(c_24,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c3) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_21]) ).
fof(prove_this_26,axiom,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c3,sk_c8) = sk_c6 ),
file('theBenchmark.p',prove_this_26) ).
cnf(c_29,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c3,sk_c8) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_26]) ).
fof(prove_this_31,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( multiply(VAR_4,sk_c6) != sk_c7
| inverse(VAR_4) != sk_c7
| multiply(VAR_3,sk_c7) != sk_c8
| inverse(VAR_3) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(VAR_2,sk_c8) != sk_c6
| inverse(VAR_2) != sk_c6
| inverse(VAR_1) != sk_c7
| multiply(VAR_1,sk_c7) != sk_c6
| inverse(VAR_0) != sk_c8
| multiply(VAR_0,sk_c8) != sk_c7 ),
file('theBenchmark.p',prove_this_31) ).
cnf(c_34,plain,
( multiply(E,sk_c6) != sk_c7
| inverse(E) != sk_c7
| multiply(D,sk_c7) != sk_c8
| inverse(D) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(C,sk_c8) != sk_c6
| inverse(C) != sk_c6
| inverse(B) != sk_c7
| multiply(B,sk_c7) != sk_c6
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7 ),
inference(clausify,[status(thm)],[prove_this_31]) ).
cnf(c_35,plain,
( multiply(D,sk_c6) != sk_c7
| inverse(D) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(C,sk_c8) != sk_c6
| inverse(C) != sk_c6
| inverse(B) != sk_c7
| multiply(B,sk_c7) != sk_c6
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_34]) ).
cnf(c_38,plain,
( multiply(B,sk_c6) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(C,sk_c8) != sk_c6
| inverse(C) != sk_c6
| inverse(B) != sk_c7
| multiply(B,sk_c7) != sk_c6
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_35]) ).
cnf(c_26364,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_26365,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_26364]) ).
cnf(c_42,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_26365]) ).
cnf(c_26366,plain,
( multiply(multiply(A,sk_c1),sk_c8) = multiply(A,sk_c7)
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_4,c_3]) ).
cnf(c_44,plain,
( multiply(A,multiply(sk_c1,sk_c8)) = multiply(A,sk_c7)
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_3,c_26366]) ).
cnf(c_45,plain,
( multiply(sk_c8,sk_c4) = identity
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_5,c_2]) ).
cnf(c_48,plain,
( multiply(sk_c7,sk_c5) = identity
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_7,c_2]) ).
cnf(c_26367,plain,
( multiply(sk_c6,A) = multiply(sk_c2,multiply(sk_c7,A))
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_14,c_3]) ).
cnf(c_56,plain,
( multiply(sk_c2,multiply(sk_c7,A)) = multiply(sk_c6,A)
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_26367]) ).
cnf(c_26368,plain,
( multiply(multiply(A,sk_c2),sk_c7) = multiply(A,sk_c6)
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_14,c_3]) ).
cnf(c_57,plain,
( multiply(A,multiply(sk_c2,sk_c7)) = multiply(A,sk_c6)
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_3,c_26368]) ).
cnf(c_61,plain,
( multiply(sk_c7,sk_c5) = identity
| multiply(sk_c2,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_17,c_2]) ).
cnf(c_587,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_42]) ).
cnf(c_619,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_42,c_42]) ).
cnf(c_620,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_619,c_587]) ).
cnf(c_621,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_620,c_2]) ).
cnf(c_1054,plain,
multiply(A,inverse(A)) = identity,
inference(paramod,[status(thm)],[c_619,c_2]) ).
cnf(c_26369,plain,
multiply(A,identity) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_619,c_620]) ).
cnf(c_26370,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_620,c_26369]) ).
cnf(c_1077,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_26370]) ).
cnf(c_26371,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(B,sk_c8) != sk_c6
| inverse(B) != sk_c6
| multiply(inverse(sk_c7),sk_c7) != sk_c6
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7 ),
inference(resolve,[status(thm)],[c_1077,c_38]) ).
cnf(c_1101,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(A,sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(B,sk_c8) != sk_c6
| inverse(B) != sk_c6
| identity != sk_c6
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_26371]) ).
cnf(c_1187,plain,
( multiply(sk_c1,sk_c8) = identity
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_9,c_1054]) ).
cnf(c_1188,plain,
( multiply(sk_c1,sk_c8) = identity
| inverse(sk_c4) = sk_c8 ),
inference(paramod,[status(thm)],[c_10,c_1054]) ).
cnf(c_1189,plain,
( multiply(sk_c1,sk_c8) = identity
| multiply(sk_c4,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_11,c_1054]) ).
cnf(c_1190,plain,
( multiply(sk_c1,sk_c8) = identity
| inverse(sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_12,c_1054]) ).
cnf(c_1191,plain,
( multiply(sk_c1,sk_c8) = identity
| multiply(sk_c5,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_13,c_1054]) ).
cnf(c_1194,plain,
( multiply(sk_c2,sk_c7) = identity
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_19,c_1054]) ).
cnf(c_1197,plain,
( multiply(sk_c2,sk_c7) = identity
| inverse(sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_22,c_1054]) ).
cnf(c_1198,plain,
( multiply(sk_c2,sk_c7) = identity
| multiply(sk_c5,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_23,c_1054]) ).
cnf(c_1199,plain,
( multiply(sk_c3,sk_c6) = identity
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_24,c_1054]) ).
cnf(c_26372,plain,
( multiply(sk_c2,identity) = multiply(sk_c6,inverse(sk_c7))
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_1054,c_56]) ).
cnf(c_26373,plain,
( sk_c2 = multiply(sk_c6,inverse(sk_c7))
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_620,c_26372]) ).
cnf(c_3879,plain,
( multiply(sk_c6,inverse(sk_c7)) = sk_c2
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_26373]) ).
cnf(c_4186,plain,
( multiply(sk_c8,sk_c4) = identity
| multiply(sk_c1,sk_c8) = identity ),
inference(paramod,[status(thm)],[c_1188,c_2]) ).
cnf(c_4262,plain,
( multiply(sk_c7,sk_c5) = identity
| multiply(sk_c1,sk_c8) = identity ),
inference(paramod,[status(thm)],[c_1190,c_2]) ).
cnf(c_4744,plain,
( multiply(sk_c7,sk_c5) = identity
| multiply(sk_c2,sk_c7) = identity ),
inference(paramod,[status(thm)],[c_1197,c_2]) ).
cnf(c_26374,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(inverse(sk_c8),sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(A,sk_c8) != sk_c6
| inverse(A) != sk_c6
| identity != sk_c6
| multiply(inverse(sk_c8),sk_c8) != sk_c7 ),
inference(resolve,[status(thm)],[c_1101,c_1077]) ).
cnf(c_8783,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(inverse(sk_c8),sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(A,sk_c8) != sk_c6
| inverse(A) != sk_c6
| identity != sk_c6
| identity != sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_26374]) ).
cnf(c_26375,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(inverse(sk_c8),sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(inverse(A),sk_c8) != sk_c6
| A != sk_c6
| identity != sk_c6
| identity != sk_c7 ),
inference(paramod,[status(thm)],[c_1077,c_8783]) ).
cnf(c_9075,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(inverse(sk_c8),sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(inverse(A),sk_c8) != sk_c6
| sk_c6 != A
| identity != sk_c6
| identity != sk_c7 ),
inference(copy,[status(thm)],[c_26375]) ).
cnf(c_26376,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| identity = sk_c7
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_1187,c_4]) ).
cnf(c_10328,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_26376]) ).
cnf(c_26377,plain,
( multiply(A,identity) = multiply(A,sk_c7)
| multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_1187,c_44]) ).
cnf(c_26378,plain,
( A = multiply(A,sk_c7)
| multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_620,c_26377]) ).
cnf(c_26379,plain,
( multiply(A,sk_c7) = A
| multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_26378]) ).
cnf(c_10329,plain,
( multiply(A,sk_c7) = A
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_26379]) ).
cnf(c_10332,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c8
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_10328,c_42]) ).
cnf(c_26380,plain,
( multiply(sk_c4,sk_c7) = sk_c8
| identity = sk_c7
| multiply(sk_c4,sk_c7) = sk_c8 ),
inference(paramod,[status(thm)],[c_1189,c_6]) ).
cnf(c_10659,plain,
( identity = sk_c7
| multiply(sk_c4,sk_c7) = sk_c8 ),
inference(copy,[status(thm)],[c_26380]) ).
cnf(c_10663,plain,
( multiply(inverse(sk_c4),sk_c8) = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_10659,c_42]) ).
cnf(c_26381,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| identity = sk_c7
| multiply(sk_c5,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_1191,c_8]) ).
cnf(c_10694,plain,
( identity = sk_c7
| multiply(sk_c5,sk_c6) = sk_c7 ),
inference(copy,[status(thm)],[c_26381]) ).
cnf(c_26382,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| identity = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_1194,c_14]) ).
cnf(c_11097,plain,
( identity = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_26382]) ).
cnf(c_26383,plain,
( multiply(A,identity) = multiply(A,sk_c6)
| multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_1194,c_57]) ).
cnf(c_26384,plain,
( A = multiply(A,sk_c6)
| multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_620,c_26383]) ).
cnf(c_26385,plain,
( multiply(A,sk_c6) = A
| multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_26384]) ).
cnf(c_11099,plain,
( multiply(A,sk_c6) = A
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_26385]) ).
cnf(c_11102,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c8
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_11097,c_42]) ).
cnf(c_26386,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| identity = sk_c6
| multiply(sk_c5,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_1198,c_18]) ).
cnf(c_11442,plain,
( identity = sk_c6
| multiply(sk_c5,sk_c6) = sk_c7 ),
inference(copy,[status(thm)],[c_26386]) ).
cnf(c_26387,plain,
( multiply(sk_c8,sk_c4) = identity
| identity = sk_c7
| multiply(sk_c8,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_4186,c_45]) ).
cnf(c_11951,plain,
( identity = sk_c7
| multiply(sk_c8,sk_c4) = identity ),
inference(copy,[status(thm)],[c_26387]) ).
cnf(c_26388,plain,
( multiply(inverse(sk_c8),identity) = sk_c4
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_11951,c_42]) ).
cnf(c_11954,plain,
( inverse(sk_c8) = sk_c4
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_620,c_26388]) ).
cnf(c_11961,plain,
( inverse(sk_c4) = sk_c8
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_11954,c_1077]) ).
cnf(c_26389,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_11961,c_10663]) ).
cnf(c_12025,plain,
( multiply(sk_c8,sk_c8) = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_26389]) ).
cnf(c_12029,plain,
( multiply(inverse(sk_c8),sk_c7) = sk_c8
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_12025,c_42]) ).
cnf(c_26390,plain,
( multiply(sk_c7,sk_c5) = identity
| identity = sk_c7
| multiply(sk_c7,sk_c5) = identity ),
inference(paramod,[status(thm)],[c_4262,c_48]) ).
cnf(c_12070,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c5) = identity ),
inference(copy,[status(thm)],[c_26390]) ).
cnf(c_26391,plain,
( multiply(inverse(sk_c7),identity) = sk_c5
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_12070,c_42]) ).
cnf(c_12073,plain,
( inverse(sk_c7) = sk_c5
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_620,c_26391]) ).
cnf(c_26392,plain,
( multiply(sk_c5,sk_c6) = sk_c8
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_12073,c_10332]) ).
cnf(c_12105,plain,
( multiply(sk_c5,sk_c6) = sk_c8
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_26392]) ).
cnf(c_26393,plain,
( identity = sk_c7
| sk_c8 = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_12105,c_10694]) ).
cnf(c_12153,plain,
( sk_c8 = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_26393]) ).
cnf(c_12154,plain,
( multiply(sk_c7,A) = A
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_12153,c_1]) ).
cnf(c_12156,plain,
( inverse(sk_c7) = identity
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_12153,c_621]) ).
cnf(c_26394,plain,
( inverse(sk_c7) = sk_c7
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_12153,c_12156]) ).
cnf(c_12371,plain,
( inverse(sk_c7) = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_26394]) ).
cnf(c_12383,plain,
( multiply(sk_c7,sk_c7) = identity
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_12371,c_2]) ).
cnf(c_26395,plain,
( multiply(sk_c7,sk_c5) = identity
| identity = sk_c6
| multiply(sk_c7,sk_c5) = identity ),
inference(paramod,[status(thm)],[c_4744,c_61]) ).
cnf(c_12872,plain,
( identity = sk_c6
| multiply(sk_c7,sk_c5) = identity ),
inference(copy,[status(thm)],[c_26395]) ).
cnf(c_26396,plain,
( multiply(inverse(sk_c7),identity) = sk_c5
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_12872,c_42]) ).
cnf(c_12875,plain,
( inverse(sk_c7) = sk_c5
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_620,c_26396]) ).
cnf(c_26397,plain,
( multiply(sk_c5,sk_c6) = sk_c8
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_12875,c_11102]) ).
cnf(c_12913,plain,
( multiply(sk_c5,sk_c6) = sk_c8
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_26397]) ).
cnf(c_26398,plain,
( identity = sk_c6
| sk_c8 = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_12913,c_11442]) ).
cnf(c_12941,plain,
( sk_c8 = sk_c7
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_26398]) ).
cnf(c_26399,plain,
( sk_c8 = sk_c7
| sk_c6 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_12941,c_12153]) ).
cnf(c_12969,plain,
( sk_c6 = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_26399]) ).
cnf(c_26400,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_12941,c_12383]) ).
cnf(c_12971,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_26400]) ).
cnf(c_13433,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_12971,c_42]) ).
cnf(c_26401,plain,
( sk_c2 = identity
| multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_10329,c_1194]) ).
cnf(c_26402,plain,
( identity = sk_c2
| multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_26401]) ).
cnf(c_14664,plain,
( identity = sk_c2
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_26402]) ).
cnf(c_15108,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c8
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_14664,c_42]) ).
cnf(c_26403,plain,
( sk_c3 = identity
| multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(paramod,[status(thm)],[c_11099,c_1199]) ).
cnf(c_26404,plain,
( identity = sk_c3
| multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_26403]) ).
cnf(c_18711,plain,
( identity = sk_c3
| multiply(sk_c7,sk_c8) = sk_c6 ),
inference(copy,[status(thm)],[c_26404]) ).
cnf(c_18721,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c8
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_18711,c_42]) ).
cnf(c_26405,plain,
( sk_c8 = sk_c7
| sk_c8 = sk_c7
| identity = sk_c3 ),
inference(paramod,[status(thm)],[c_18721,c_13433]) ).
cnf(c_18846,plain,
( sk_c8 = sk_c7
| identity = sk_c3 ),
inference(copy,[status(thm)],[c_26405]) ).
cnf(c_26406,plain,
( sk_c8 = sk_c7
| sk_c3 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_18846,c_12153]) ).
cnf(c_18879,plain,
( sk_c3 = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_26406]) ).
cnf(c_26407,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c7,sk_c8) = sk_c6
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_18879,c_29]) ).
cnf(c_18899,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_26407]) ).
cnf(c_26408,plain,
( sk_c6 = sk_c8
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_18899,c_12154]) ).
cnf(c_19555,plain,
( sk_c6 = sk_c8
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_26408]) ).
cnf(c_26409,plain,
( sk_c8 = sk_c7
| sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(paramod,[status(thm)],[c_19555,c_12969]) ).
cnf(c_26410,plain,
( sk_c8 = sk_c7
| sk_c8 = sk_c7 ),
inference(copy,[status(thm)],[c_26409]) ).
cnf(c_19591,plain,
sk_c8 = sk_c7,
inference(copy,[status(thm)],[c_26410]) ).
cnf(c_21216,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c7
| identity = sk_c2 ),
inference(paramod,[status(thm)],[c_19591,c_15108]) ).
cnf(c_26411,plain,
( multiply(inverse(sk_c7),sk_c7) = sk_c8
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_19591,c_12029]) ).
cnf(c_26412,plain,
( identity = sk_c8
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_26411]) ).
cnf(c_26413,plain,
( identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_19591,c_26412]) ).
cnf(c_22219,plain,
identity = sk_c7,
inference(copy,[status(thm)],[c_26413]) ).
cnf(c_26414,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(inverse(sk_c8),sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(inverse(A),sk_c8) != sk_c6
| sk_c6 != A
| identity != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_22219,c_9075]) ).
cnf(c_26415,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(inverse(sk_c8),sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(inverse(A),sk_c8) != sk_c6
| sk_c6 != A
| sk_c7 != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_22219,c_26414]) ).
cnf(c_26416,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(inverse(sk_c8),sk_c7) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| multiply(inverse(A),sk_c7) != sk_c6
| sk_c6 != A
| sk_c7 != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_19591,c_26415]) ).
cnf(c_26417,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(inverse(sk_c8),sk_c7) != sk_c8
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(inverse(A),sk_c7) != sk_c6
| sk_c6 != A
| sk_c7 != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_19591,c_26416]) ).
cnf(c_26418,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(inverse(sk_c7),sk_c7) != sk_c8
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(inverse(A),sk_c7) != sk_c6
| sk_c6 != A
| sk_c7 != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_19591,c_26417]) ).
cnf(c_26419,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| identity != sk_c8
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(inverse(A),sk_c7) != sk_c6
| sk_c6 != A
| sk_c7 != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_26418]) ).
cnf(c_26420,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| sk_c7 != sk_c8
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(inverse(A),sk_c7) != sk_c6
| sk_c6 != A
| sk_c7 != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_22219,c_26419]) ).
cnf(c_26421,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(inverse(A),sk_c7) != sk_c6
| sk_c6 != A
| sk_c7 != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_19591,c_26420]) ).
cnf(c_26422,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(inverse(A),sk_c7) != sk_c6
| sk_c6 != A
| sk_c6 != sk_c7
| sk_c7 != sk_c7 ),
inference(copy,[status(thm)],[c_26421]) ).
cnf(c_26423,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(inverse(A),sk_c7) != sk_c6
| sk_c6 != A
| sk_c6 != sk_c7 ),
inference(copy,[status(thm)],[c_26422]) ).
cnf(c_23790,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(inverse(A),sk_c7) != sk_c6
| sk_c6 != A
| sk_c6 != sk_c7 ),
inference(copy,[status(thm)],[c_26423]) ).
cnf(c_25056,plain,
( multiply(sk_c6,inverse(sk_c7)) = sk_c2
| multiply(sk_c7,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_19591,c_3879]) ).
cnf(c_26424,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c7
| sk_c7 = sk_c2 ),
inference(paramod,[status(thm)],[c_22219,c_21216]) ).
cnf(c_25955,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c7
| sk_c2 = sk_c7 ),
inference(copy,[status(thm)],[c_26424]) ).
cnf(c_26425,plain,
inverse(sk_c7) = identity,
inference(paramod,[status(thm)],[c_22219,c_621]) ).
cnf(c_26211,plain,
inverse(sk_c7) = sk_c7,
inference(paramod,[status(thm)],[c_22219,c_26425]) ).
cnf(c_26212,plain,
multiply(A,sk_c7) = A,
inference(paramod,[status(thm)],[c_22219,c_620]) ).
cnf(c_26219,plain,
multiply(sk_c7,A) = A,
inference(paramod,[status(thm)],[c_22219,c_1]) ).
cnf(c_26426,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(inverse(sk_c7),sk_c7) != sk_c6
| sk_c6 != sk_c7 ),
inference(factor,[status(thm)],[c_23790]) ).
cnf(c_26427,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| multiply(sk_c7,sk_c7) != sk_c6
| sk_c6 != sk_c7 ),
inference(paramod,[status(thm)],[c_26211,c_26426]) ).
cnf(c_26428,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6
| sk_c7 != sk_c6
| sk_c6 != sk_c7 ),
inference(paramod,[status(thm)],[c_26212,c_26427]) ).
cnf(c_26429,plain,
( multiply(inverse(sk_c7),sk_c6) != sk_c7
| sk_c7 != sk_c6
| sk_c7 != sk_c6
| sk_c6 != sk_c7 ),
inference(paramod,[status(thm)],[c_26212,c_26428]) ).
cnf(c_26430,plain,
( multiply(sk_c7,sk_c6) != sk_c7
| sk_c7 != sk_c6
| sk_c7 != sk_c6
| sk_c6 != sk_c7 ),
inference(paramod,[status(thm)],[c_26211,c_26429]) ).
cnf(c_26431,plain,
( sk_c6 != sk_c7
| sk_c7 != sk_c6
| sk_c7 != sk_c6
| sk_c6 != sk_c7 ),
inference(paramod,[status(thm)],[c_26219,c_26430]) ).
cnf(c_26432,plain,
( sk_c6 != sk_c7
| sk_c7 != sk_c6
| sk_c6 != sk_c7
| sk_c6 != sk_c7 ),
inference(copy,[status(thm)],[c_26431]) ).
cnf(c_26433,plain,
( sk_c6 != sk_c7
| sk_c6 != sk_c7
| sk_c6 != sk_c7
| sk_c6 != sk_c7 ),
inference(copy,[status(thm)],[c_26432]) ).
cnf(c_26434,plain,
( sk_c6 != sk_c7
| sk_c6 != sk_c7
| sk_c6 != sk_c7 ),
inference(copy,[status(thm)],[c_26433]) ).
cnf(c_26435,plain,
( sk_c6 != sk_c7
| sk_c6 != sk_c7 ),
inference(copy,[status(thm)],[c_26434]) ).
cnf(c_26336,plain,
sk_c6 != sk_c7,
inference(copy,[status(thm)],[c_26435]) ).
cnf(c_26436,plain,
( multiply(sk_c7,sk_c6) = sk_c7
| sk_c2 = sk_c7 ),
inference(paramod,[status(thm)],[c_26211,c_25955]) ).
cnf(c_26437,plain,
( sk_c6 = sk_c7
| sk_c2 = sk_c7 ),
inference(paramod,[status(thm)],[c_26219,c_26436]) ).
cnf(c_26355,plain,
sk_c2 = sk_c7,
inference(resolve,[status(thm)],[c_26336,c_26437]) ).
cnf(c_26438,plain,
( multiply(sk_c6,inverse(sk_c7)) = sk_c2
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26212,c_25056]) ).
cnf(c_26439,plain,
( multiply(sk_c6,sk_c7) = sk_c2
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26211,c_26438]) ).
cnf(c_26440,plain,
( sk_c6 = sk_c2
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26212,c_26439]) ).
cnf(c_26441,plain,
( sk_c6 = sk_c7
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_26355,c_26440]) ).
cnf(c_26442,plain,
( sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(copy,[status(thm)],[c_26441]) ).
cnf(c_26443,plain,
sk_c6 = sk_c7,
inference(copy,[status(thm)],[c_26442]) ).
cnf(c_26363,plain,
$false,
inference(resolve,[status(thm)],[c_26336,c_26443]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP255-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n008.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.43 % DateTime : Fri Sep 25 14:41:39 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.43 % Process 1292961 was started by sandbox2 on n008,
% 0.17/0.43 % Fri Sep 25 14:41:39 2026
% 0.17/0.43 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/0.44
% 0.17/0.44 % From the command line: assign(max_seconds, 300).
% 198.16/25.81
% 198.16/25.81 % given #500 (F,wt=29): 14012 identity != sk_c7 | sk_c6 != sk_c7 | inverse(sk_c7) != sk_c6 | multiply(sk_c7,sk_c8) != sk_c6 | multiply(inverse(A),inverse(B)) != sk_c8 | multiply(B,multiply(A,sk_c7)) != sk_c8. [para(10084(a,1),1087(e,1)),rewrite([3(23)])].
% 198.16/25.81
% 198.16/25.81 % SZS status Unsatisfiable for theBenchmark
% 198.16/25.81
% 198.16/25.81 % Proof 1 at 22.01 (+ 3.18) seconds.
% 198.16/25.81 % Length of proof is 103.
% 198.16/25.81 % Level of proof is 24.
% 198.16/25.81 % Maximum clause weight is 50.000.
% 198.16/25.81 % Given clauses 684.
% 198.16/25.81
% 198.16/25.81 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------