%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP272-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 : n015.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:31 AM UTC 2026
% Result : Unsatisfiable 154.87s 25.46s
% Output : CNFRefutation 154.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 67
% Number of leaves : 21
% Syntax : Number of formulae : 215 ( 34 unt; 0 def)
% Number of atoms : 525 ( 524 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 467 ( 157 ~; 310 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 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 : 67 ( 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
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_1) ).
cnf(c_4,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_1]) ).
fof(prove_this_2,axiom,
( inverse(sk_c3) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_2) ).
cnf(c_5,plain,
( inverse(sk_c3) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_2]) ).
fof(prove_this_3,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_3) ).
cnf(c_6,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_3]) ).
fof(prove_this_4,axiom,
( inverse(sk_c4) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_4) ).
cnf(c_7,plain,
( inverse(sk_c4) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_4]) ).
fof(prove_this_5,axiom,
( multiply(sk_c4,sk_c5) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_5) ).
cnf(c_8,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_5]) ).
fof(prove_this_6,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_6) ).
cnf(c_9,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_6]) ).
fof(prove_this_7,axiom,
( inverse(sk_c3) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_7) ).
cnf(c_10,plain,
( inverse(sk_c3) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_7]) ).
fof(prove_this_8,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_11,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_8]) ).
fof(prove_this_9,axiom,
( inverse(sk_c4) = sk_c6
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_9) ).
cnf(c_12,plain,
( inverse(sk_c4) = sk_c6
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_9]) ).
fof(prove_this_10,axiom,
( multiply(sk_c4,sk_c5) = sk_c6
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_10) ).
cnf(c_13,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_10]) ).
fof(prove_this_11,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c7,sk_c5) = sk_c6 ),
file('theBenchmark.p',prove_this_11) ).
cnf(c_14,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_11]) ).
fof(prove_this_16,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c2,sk_c6) = sk_c5 ),
file('theBenchmark.p',prove_this_16) ).
cnf(c_19,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_16]) ).
fof(prove_this_19,axiom,
( inverse(sk_c4) = sk_c6
| multiply(sk_c2,sk_c6) = sk_c5 ),
file('theBenchmark.p',prove_this_19) ).
cnf(c_22,plain,
( inverse(sk_c4) = sk_c6
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_19]) ).
fof(prove_this_20,axiom,
( multiply(sk_c4,sk_c5) = sk_c6
| multiply(sk_c2,sk_c6) = sk_c5 ),
file('theBenchmark.p',prove_this_20) ).
cnf(c_23,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_20]) ).
fof(prove_this_21,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_21) ).
cnf(c_24,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c2) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_21]) ).
fof(prove_this_24,axiom,
( inverse(sk_c4) = sk_c6
| inverse(sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_24) ).
cnf(c_27,plain,
( inverse(sk_c4) = sk_c6
| inverse(sk_c2) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_24]) ).
fof(prove_this_25,axiom,
( multiply(sk_c4,sk_c5) = sk_c6
| inverse(sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_25) ).
cnf(c_28,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| inverse(sk_c2) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_25]) ).
fof(prove_this_26,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( multiply(VAR_3,sk_c5) != sk_c6
| inverse(VAR_3) != sk_c6
| multiply(VAR_2,sk_c6) != sk_c7
| inverse(VAR_2) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(VAR_1) != sk_c6
| multiply(VAR_1,sk_c6) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(VAR_0) != sk_c7
| multiply(VAR_0,sk_c7) != sk_c6 ),
file('theBenchmark.p',prove_this_26) ).
cnf(c_29,plain,
( multiply(D,sk_c5) != sk_c6
| inverse(D) != sk_c6
| multiply(C,sk_c6) != sk_c7
| inverse(C) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(B) != sk_c6
| multiply(B,sk_c6) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6 ),
inference(clausify,[status(thm)],[prove_this_26]) ).
cnf(c_30,plain,
( multiply(C,sk_c5) != sk_c6
| inverse(C) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(B) != sk_c6
| multiply(B,sk_c6) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6 ),
inference(factor,[status(thm)],[c_29]) ).
cnf(c_34,plain,
( multiply(B,sk_c5) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(B) != sk_c6
| multiply(B,sk_c6) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6 ),
inference(factor,[status(thm)],[c_30]) ).
cnf(c_31580,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_31581,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_31580]) ).
cnf(c_37,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_31581]) ).
cnf(c_40,plain,
( multiply(sk_c7,sk_c3) = identity
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_5,c_2]) ).
cnf(c_43,plain,
( multiply(sk_c6,sk_c4) = identity
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_7,c_2]) ).
cnf(c_47,plain,
( multiply(sk_c7,sk_c3) = identity
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_10,c_2]) ).
cnf(c_48,plain,
( multiply(sk_c7,sk_c1) = identity
| multiply(sk_c3,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_11,c_2]) ).
cnf(c_49,plain,
( multiply(sk_c6,sk_c4) = identity
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_12,c_2]) ).
cnf(c_50,plain,
( multiply(sk_c7,sk_c1) = identity
| multiply(sk_c4,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_13,c_2]) ).
cnf(c_31582,plain,
( multiply(sk_c6,A) = multiply(sk_c7,multiply(sk_c5,A))
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_14,c_3]) ).
cnf(c_51,plain,
( multiply(sk_c7,multiply(sk_c5,A)) = multiply(sk_c6,A)
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_31582]) ).
cnf(c_31583,plain,
( multiply(multiply(A,sk_c2),sk_c6) = multiply(A,sk_c5)
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_19,c_3]) ).
cnf(c_60,plain,
( multiply(A,multiply(sk_c2,sk_c6)) = multiply(A,sk_c5)
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_3,c_31583]) ).
cnf(c_71,plain,
( multiply(sk_c6,sk_c2) = identity
| multiply(sk_c4,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_28,c_2]) ).
cnf(c_313,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_37]) ).
cnf(c_317,plain,
( multiply(inverse(sk_c3),sk_c7) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_6,c_37]) ).
cnf(c_319,plain,
( multiply(inverse(sk_c4),sk_c6) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_8,c_37]) ).
cnf(c_334,plain,
( multiply(inverse(sk_c4),sk_c6) = sk_c5
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_23,c_37]) ).
cnf(c_340,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_37,c_37]) ).
cnf(c_341,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_340,c_313]) ).
cnf(c_342,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_341,c_2]) ).
cnf(c_483,plain,
multiply(A,inverse(A)) = identity,
inference(paramod,[status(thm)],[c_340,c_2]) ).
cnf(c_500,plain,
multiply(A,multiply(inverse(A),B)) = B,
inference(paramod,[status(thm)],[c_340,c_37]) ).
cnf(c_31584,plain,
multiply(A,identity) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_340,c_341]) ).
cnf(c_31585,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_341,c_31584]) ).
cnf(c_501,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_31585]) ).
cnf(c_31586,plain,
( multiply(inverse(sk_c6),sk_c5) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(inverse(sk_c6),sk_c6) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6 ),
inference(resolve,[status(thm)],[c_501,c_34]) ).
cnf(c_511,plain,
( multiply(inverse(sk_c6),sk_c5) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_2,c_31586]) ).
cnf(c_531,plain,
( inverse(sk_c7) = sk_c3
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_10,c_501]) ).
cnf(c_533,plain,
( inverse(sk_c6) = sk_c4
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_12,c_501]) ).
cnf(c_542,plain,
( inverse(sk_c6) = sk_c4
| inverse(sk_c2) = sk_c6 ),
inference(paramod,[status(thm)],[c_27,c_501]) ).
cnf(c_31587,plain,
identity = multiply(A,multiply(B,inverse(multiply(A,B)))),
inference(paramod,[status(thm)],[c_483,c_3]) ).
cnf(c_576,plain,
multiply(A,multiply(B,inverse(multiply(A,B)))) = identity,
inference(copy,[status(thm)],[c_31587]) ).
cnf(c_579,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_9,c_483]) ).
cnf(c_588,plain,
( multiply(sk_c2,sk_c6) = identity
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_24,c_483]) ).
cnf(c_593,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c7,sk_c3) = identity ),
inference(paramod,[status(thm)],[c_47,c_483]) ).
cnf(c_594,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c6,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_49,c_483]) ).
cnf(c_634,plain,
( multiply(sk_c7,sk_c1) = identity
| inverse(sk_c7) = sk_c3 ),
inference(paramod,[status(thm)],[c_531,c_2]) ).
cnf(c_661,plain,
( multiply(sk_c7,sk_c1) = identity
| inverse(sk_c6) = sk_c4 ),
inference(paramod,[status(thm)],[c_533,c_2]) ).
cnf(c_780,plain,
( inverse(sk_c6) = sk_c2
| inverse(sk_c6) = sk_c4 ),
inference(paramod,[status(thm)],[c_542,c_501]) ).
cnf(c_982,plain,
( multiply(sk_c6,multiply(sk_c4,A)) = A
| inverse(sk_c6) = sk_c2 ),
inference(paramod,[status(thm)],[c_780,c_500]) ).
cnf(c_31588,plain,
( multiply(inverse(sk_c6),sk_c5) != sk_c6
| multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| multiply(inverse(sk_c7),sk_c7) != sk_c6 ),
inference(resolve,[status(thm)],[c_511,c_501]) ).
cnf(c_1223,plain,
( multiply(inverse(sk_c6),sk_c5) != sk_c6
| multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| identity != sk_c6 ),
inference(paramod,[status(thm)],[c_2,c_31588]) ).
cnf(c_2181,plain,
( multiply(inverse(sk_c3),sk_c7) = sk_c6
| multiply(sk_c7,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_48,c_37]) ).
cnf(c_2439,plain,
( inverse(sk_c3) = sk_c7
| multiply(sk_c7,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_634,c_501]) ).
cnf(c_2565,plain,
( inverse(sk_c4) = sk_c6
| multiply(sk_c7,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_661,c_501]) ).
cnf(c_2598,plain,
( multiply(inverse(sk_c4),sk_c6) = sk_c5
| multiply(sk_c7,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_50,c_37]) ).
cnf(c_31589,plain,
multiply(inverse(A),identity) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_576,c_37]) ).
cnf(c_31590,plain,
inverse(A) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_341,c_31589]) ).
cnf(c_5158,plain,
multiply(A,inverse(multiply(B,A))) = inverse(B),
inference(copy,[status(thm)],[c_31590]) ).
cnf(c_31591,plain,
multiply(inverse(A),inverse(B)) = inverse(multiply(B,A)),
inference(paramod,[status(thm)],[c_5158,c_37]) ).
cnf(c_5496,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_31591]) ).
cnf(c_31592,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| identity = sk_c6
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_579,c_4]) ).
cnf(c_5528,plain,
( identity = sk_c6
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_31592]) ).
cnf(c_5867,plain,
( multiply(inverse(sk_c6),sk_c5) = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_5528,c_37]) ).
cnf(c_31593,plain,
( multiply(A,identity) = multiply(A,sk_c5)
| multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_588,c_60]) ).
cnf(c_31594,plain,
( A = multiply(A,sk_c5)
| multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_341,c_31593]) ).
cnf(c_31595,plain,
( multiply(A,sk_c5) = A
| multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_31594]) ).
cnf(c_6457,plain,
( multiply(A,sk_c5) = A
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_31595]) ).
cnf(c_31596,plain,
( multiply(sk_c7,sk_c3) = identity
| identity = sk_c6
| multiply(sk_c7,sk_c3) = identity ),
inference(paramod,[status(thm)],[c_593,c_40]) ).
cnf(c_6856,plain,
( identity = sk_c6
| multiply(sk_c7,sk_c3) = identity ),
inference(copy,[status(thm)],[c_31596]) ).
cnf(c_31597,plain,
( multiply(inverse(sk_c7),identity) = sk_c3
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_6856,c_37]) ).
cnf(c_6859,plain,
( inverse(sk_c7) = sk_c3
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_341,c_31597]) ).
cnf(c_31598,plain,
( multiply(sk_c6,sk_c4) = identity
| identity = sk_c6
| multiply(sk_c6,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_594,c_43]) ).
cnf(c_7264,plain,
( identity = sk_c6
| multiply(sk_c6,sk_c4) = identity ),
inference(copy,[status(thm)],[c_31598]) ).
cnf(c_31599,plain,
( multiply(inverse(sk_c6),identity) = sk_c4
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_7264,c_37]) ).
cnf(c_7267,plain,
( inverse(sk_c6) = sk_c4
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_341,c_31599]) ).
cnf(c_7488,plain,
( multiply(sk_c4,multiply(sk_c6,A)) = A
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_7267,c_37]) ).
cnf(c_31600,plain,
( inverse(sk_c7) = multiply(inverse(sk_c5),inverse(inverse(sk_c6)))
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_5867,c_5496]) ).
cnf(c_31601,plain,
( inverse(sk_c7) = multiply(inverse(sk_c5),sk_c6)
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_501,c_31600]) ).
cnf(c_8800,plain,
( multiply(inverse(sk_c5),sk_c6) = inverse(sk_c7)
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_31601]) ).
cnf(c_31602,plain,
( multiply(sk_c7,multiply(sk_c5,sk_c5)) = sk_c6
| multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_6457,c_51]) ).
cnf(c_9649,plain,
( multiply(sk_c7,multiply(sk_c5,sk_c5)) = sk_c6
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_31602]) ).
cnf(c_31603,plain,
( multiply(inverse(sk_c5),sk_c6) = sk_c3
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_6859,c_8800]) ).
cnf(c_11018,plain,
( multiply(inverse(sk_c5),sk_c6) = sk_c3
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_31603]) ).
cnf(c_31604,plain,
( inverse(sk_c3) = multiply(inverse(sk_c6),inverse(inverse(sk_c5)))
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_11018,c_5496]) ).
cnf(c_11433,plain,
( inverse(sk_c3) = multiply(inverse(sk_c6),sk_c5)
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_501,c_31604]) ).
cnf(c_31605,plain,
( inverse(sk_c3) = multiply(sk_c4,sk_c5)
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_7267,c_11433]) ).
cnf(c_13212,plain,
( inverse(sk_c3) = multiply(sk_c4,sk_c5)
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_31605]) ).
cnf(c_31606,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_5,c_317]) ).
cnf(c_14394,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(copy,[status(thm)],[c_31606]) ).
cnf(c_31607,plain,
( multiply(sk_c6,sk_c6) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_7,c_319]) ).
cnf(c_14485,plain,
( multiply(sk_c6,sk_c6) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(copy,[status(thm)],[c_31607]) ).
cnf(c_31608,plain,
( multiply(sk_c6,sk_c6) = sk_c5
| multiply(sk_c2,sk_c6) = sk_c5
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_22,c_334]) ).
cnf(c_15494,plain,
( multiply(sk_c6,sk_c6) = sk_c5
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(copy,[status(thm)],[c_31608]) ).
cnf(c_16647,plain,
( multiply(sk_c6,sk_c6) = sk_c5
| inverse(sk_c6) = sk_c2
| multiply(sk_c6,sk_c2) = identity ),
inference(paramod,[status(thm)],[c_71,c_982]) ).
cnf(c_31609,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| multiply(sk_c7,sk_c1) = identity
| multiply(sk_c7,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_2439,c_2181]) ).
cnf(c_16748,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| multiply(sk_c7,sk_c1) = identity ),
inference(copy,[status(thm)],[c_31609]) ).
cnf(c_31610,plain,
( multiply(inverse(sk_c7),identity) = sk_c1
| multiply(sk_c7,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_16748,c_37]) ).
cnf(c_16763,plain,
( inverse(sk_c7) = sk_c1
| multiply(sk_c7,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_341,c_31610]) ).
cnf(c_16774,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c7,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_16763,c_2]) ).
cnf(c_31611,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| identity = sk_c6
| multiply(sk_c7,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_16774,c_14394]) ).
cnf(c_16863,plain,
( identity = sk_c6
| multiply(sk_c7,sk_c7) = sk_c6 ),
inference(copy,[status(thm)],[c_31611]) ).
cnf(c_16890,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_16863,c_37]) ).
cnf(c_31612,plain,
( inverse(sk_c7) = multiply(inverse(sk_c6),inverse(inverse(sk_c7)))
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_16890,c_5496]) ).
cnf(c_16929,plain,
( inverse(sk_c7) = multiply(inverse(sk_c6),sk_c7)
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_501,c_31612]) ).
cnf(c_31613,plain,
( multiply(inverse(sk_c6),sk_c7) = sk_c3
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_16929,c_6859]) ).
cnf(c_16984,plain,
( multiply(inverse(sk_c6),sk_c7) = sk_c3
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_31613]) ).
cnf(c_31614,plain,
( inverse(sk_c3) = multiply(inverse(sk_c7),inverse(inverse(sk_c6)))
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_16984,c_5496]) ).
cnf(c_17014,plain,
( inverse(sk_c3) = multiply(inverse(sk_c7),sk_c6)
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_501,c_31614]) ).
cnf(c_31615,plain,
( inverse(sk_c3) = multiply(sk_c3,sk_c6)
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_6859,c_17014]) ).
cnf(c_17200,plain,
( inverse(sk_c3) = multiply(sk_c3,sk_c6)
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_31615]) ).
cnf(c_31616,plain,
( inverse(multiply(sk_c3,sk_c6)) = sk_c3
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_17200,c_501]) ).
cnf(c_17219,plain,
( multiply(inverse(sk_c6),inverse(sk_c3)) = sk_c3
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_5496,c_31616]) ).
cnf(c_31617,plain,
( multiply(sk_c6,sk_c6) = sk_c5
| multiply(sk_c7,sk_c1) = identity
| multiply(sk_c7,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_2565,c_2598]) ).
cnf(c_18739,plain,
( multiply(sk_c6,sk_c6) = sk_c5
| multiply(sk_c7,sk_c1) = identity ),
inference(copy,[status(thm)],[c_31617]) ).
cnf(c_31618,plain,
( multiply(inverse(sk_c7),identity) = sk_c1
| multiply(sk_c6,sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_18739,c_37]) ).
cnf(c_18752,plain,
( inverse(sk_c7) = sk_c1
| multiply(sk_c6,sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_341,c_31618]) ).
cnf(c_18760,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c6,sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_18752,c_2]) ).
cnf(c_31619,plain,
( multiply(sk_c6,sk_c6) = sk_c5
| identity = sk_c6
| multiply(sk_c6,sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_18760,c_14485]) ).
cnf(c_18845,plain,
( identity = sk_c6
| multiply(sk_c6,sk_c6) = sk_c5 ),
inference(copy,[status(thm)],[c_31619]) ).
cnf(c_31620,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_18845,c_7488]) ).
cnf(c_18855,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_31620]) ).
cnf(c_31621,plain,
( inverse(sk_c3) = sk_c6
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_18855,c_13212]) ).
cnf(c_18864,plain,
( inverse(sk_c3) = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_31621]) ).
cnf(c_31622,plain,
( multiply(inverse(sk_c6),sk_c6) = sk_c3
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_18864,c_17219]) ).
cnf(c_31623,plain,
( identity = sk_c3
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_2,c_31622]) ).
cnf(c_18938,plain,
( identity = sk_c3
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_31623]) ).
cnf(c_18947,plain,
( inverse(sk_c3) = identity
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_18938,c_342]) ).
cnf(c_31624,plain,
( identity = sk_c6
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_18947,c_18864]) ).
cnf(c_31625,plain,
( identity = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_31624]) ).
cnf(c_19181,plain,
identity = sk_c6,
inference(copy,[status(thm)],[c_31625]) ).
cnf(c_19973,plain,
( multiply(sk_c6,sk_c6) = sk_c5
| inverse(sk_c6) = sk_c2
| multiply(sk_c6,sk_c2) = sk_c6 ),
inference(paramod,[status(thm)],[c_19181,c_16647]) ).
cnf(c_31626,plain,
( multiply(inverse(sk_c6),sk_c5) != sk_c6
| multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| sk_c6 != sk_c6 ),
inference(paramod,[status(thm)],[c_19181,c_1223]) ).
cnf(c_31627,plain,
( multiply(inverse(sk_c6),sk_c5) != sk_c6
| multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c6 != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| sk_c6 != sk_c6 ),
inference(paramod,[status(thm)],[c_19181,c_31626]) ).
cnf(c_31628,plain,
( multiply(inverse(sk_c6),sk_c5) != sk_c6
| multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c5 != sk_c6
| multiply(sk_c7,sk_c5) != sk_c6
| sk_c6 != sk_c6 ),
inference(copy,[status(thm)],[c_31627]) ).
cnf(c_28759,plain,
( multiply(inverse(sk_c6),sk_c5) != sk_c6
| multiply(inverse(sk_c7),sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c5 != sk_c6
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(copy,[status(thm)],[c_31628]) ).
cnf(c_31629,plain,
inverse(sk_c6) = identity,
inference(paramod,[status(thm)],[c_19181,c_342]) ).
cnf(c_29060,plain,
inverse(sk_c6) = sk_c6,
inference(paramod,[status(thm)],[c_19181,c_31629]) ).
cnf(c_29061,plain,
multiply(A,sk_c6) = A,
inference(paramod,[status(thm)],[c_19181,c_341]) ).
cnf(c_29077,plain,
multiply(sk_c6,A) = A,
inference(paramod,[status(thm)],[c_19181,c_1]) ).
cnf(c_31630,plain,
( multiply(inverse(sk_c6),sk_c5) != sk_c6
| multiply(inverse(sk_c7),sk_c6) != sk_c7
| sk_c7 != sk_c5
| sk_c5 != sk_c6
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(paramod,[status(thm)],[c_29077,c_28759]) ).
cnf(c_31631,plain,
( multiply(inverse(sk_c6),sk_c5) != sk_c6
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c5
| sk_c5 != sk_c6
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(paramod,[status(thm)],[c_29061,c_31630]) ).
cnf(c_31632,plain,
( multiply(sk_c6,sk_c5) != sk_c6
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c5
| sk_c5 != sk_c6
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(paramod,[status(thm)],[c_29060,c_31631]) ).
cnf(c_31633,plain,
( sk_c5 != sk_c6
| inverse(sk_c7) != sk_c7
| sk_c7 != sk_c5
| sk_c5 != sk_c6
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(paramod,[status(thm)],[c_29077,c_31632]) ).
cnf(c_31634,plain,
( sk_c5 != sk_c6
| inverse(sk_c7) != sk_c7
| sk_c5 != sk_c7
| sk_c5 != sk_c6
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(copy,[status(thm)],[c_31633]) ).
cnf(c_29369,plain,
( inverse(sk_c7) != sk_c7
| sk_c5 != sk_c7
| sk_c5 != sk_c6
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(copy,[status(thm)],[c_31634]) ).
cnf(c_31635,plain,
( multiply(sk_c6,sk_c6) = sk_c5
| inverse(sk_c6) = sk_c2
| sk_c2 = sk_c6 ),
inference(paramod,[status(thm)],[c_29077,c_19973]) ).
cnf(c_31636,plain,
( multiply(sk_c6,sk_c6) = sk_c5
| sk_c6 = sk_c2
| sk_c2 = sk_c6 ),
inference(paramod,[status(thm)],[c_29060,c_31635]) ).
cnf(c_31637,plain,
( sk_c6 = sk_c5
| sk_c6 = sk_c2
| sk_c2 = sk_c6 ),
inference(paramod,[status(thm)],[c_29061,c_31636]) ).
cnf(c_31638,plain,
( sk_c6 = sk_c5
| sk_c2 = sk_c6
| sk_c2 = sk_c6 ),
inference(copy,[status(thm)],[c_31637]) ).
cnf(c_31639,plain,
( sk_c5 = sk_c6
| sk_c2 = sk_c6
| sk_c2 = sk_c6 ),
inference(copy,[status(thm)],[c_31638]) ).
cnf(c_29590,plain,
( sk_c5 = sk_c6
| sk_c2 = sk_c6 ),
inference(copy,[status(thm)],[c_31639]) ).
cnf(c_31640,plain,
( multiply(sk_c6,sk_c6) = sk_c5
| sk_c2 = sk_c5 ),
inference(paramod,[status(thm)],[c_29061,c_15494]) ).
cnf(c_31641,plain,
( sk_c6 = sk_c5
| sk_c2 = sk_c5 ),
inference(paramod,[status(thm)],[c_29061,c_31640]) ).
cnf(c_30900,plain,
( sk_c5 = sk_c6
| sk_c2 = sk_c5 ),
inference(copy,[status(thm)],[c_31641]) ).
cnf(c_31642,plain,
( multiply(sk_c7,multiply(sk_c5,sk_c5)) = sk_c6
| sk_c7 = sk_c5 ),
inference(paramod,[status(thm)],[c_29077,c_9649]) ).
cnf(c_31403,plain,
( multiply(sk_c7,multiply(sk_c5,sk_c5)) = sk_c6
| sk_c5 = sk_c7 ),
inference(copy,[status(thm)],[c_31642]) ).
cnf(c_31643,plain,
( sk_c5 = sk_c6
| sk_c5 = sk_c6
| sk_c5 = sk_c6 ),
inference(paramod,[status(thm)],[c_30900,c_29590]) ).
cnf(c_31644,plain,
( sk_c5 = sk_c6
| sk_c5 = sk_c6 ),
inference(copy,[status(thm)],[c_31643]) ).
cnf(c_31504,plain,
sk_c5 = sk_c6,
inference(copy,[status(thm)],[c_31644]) ).
cnf(c_31645,plain,
( multiply(sk_c7,multiply(sk_c5,sk_c5)) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_31504,c_31403]) ).
cnf(c_31646,plain,
( multiply(sk_c7,multiply(sk_c6,sk_c5)) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_31504,c_31645]) ).
cnf(c_31647,plain,
( multiply(sk_c7,multiply(sk_c6,sk_c6)) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_31504,c_31646]) ).
cnf(c_31648,plain,
( multiply(sk_c7,sk_c6) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_29061,c_31647]) ).
cnf(c_31649,plain,
( sk_c7 = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_29061,c_31648]) ).
cnf(c_31650,plain,
( sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_31649]) ).
cnf(c_31543,plain,
sk_c7 = sk_c6,
inference(copy,[status(thm)],[c_31650]) ).
cnf(c_31651,plain,
( inverse(sk_c7) != sk_c7
| sk_c5 != sk_c7
| sk_c5 != sk_c6
| multiply(sk_c6,sk_c5) != sk_c6 ),
inference(paramod,[status(thm)],[c_31543,c_29369]) ).
cnf(c_31652,plain,
( inverse(sk_c7) != sk_c7
| sk_c5 != sk_c7
| sk_c5 != sk_c6
| multiply(sk_c6,sk_c6) != sk_c6 ),
inference(paramod,[status(thm)],[c_31504,c_31651]) ).
cnf(c_31653,plain,
( inverse(sk_c7) != sk_c7
| sk_c5 != sk_c7
| sk_c5 != sk_c6
| sk_c6 != sk_c6 ),
inference(paramod,[status(thm)],[c_29061,c_31652]) ).
cnf(c_31654,plain,
( inverse(sk_c7) != sk_c7
| sk_c5 != sk_c7
| sk_c6 != sk_c6
| sk_c6 != sk_c6 ),
inference(paramod,[status(thm)],[c_31504,c_31653]) ).
cnf(c_31655,plain,
( inverse(sk_c7) != sk_c7
| sk_c6 != sk_c7
| sk_c6 != sk_c6
| sk_c6 != sk_c6 ),
inference(paramod,[status(thm)],[c_31504,c_31654]) ).
cnf(c_31656,plain,
( inverse(sk_c7) != sk_c7
| sk_c6 != sk_c6
| sk_c6 != sk_c6
| sk_c6 != sk_c6 ),
inference(paramod,[status(thm)],[c_31543,c_31655]) ).
cnf(c_31657,plain,
( inverse(sk_c6) != sk_c7
| sk_c6 != sk_c6
| sk_c6 != sk_c6
| sk_c6 != sk_c6 ),
inference(paramod,[status(thm)],[c_31543,c_31656]) ).
cnf(c_31658,plain,
( sk_c6 != sk_c7
| sk_c6 != sk_c6
| sk_c6 != sk_c6
| sk_c6 != sk_c6 ),
inference(paramod,[status(thm)],[c_29060,c_31657]) ).
cnf(c_31659,plain,
( sk_c6 != sk_c6
| sk_c6 != sk_c6
| sk_c6 != sk_c6
| sk_c6 != sk_c6 ),
inference(paramod,[status(thm)],[c_31543,c_31658]) ).
cnf(c_31660,plain,
( sk_c6 != sk_c6
| sk_c6 != sk_c6
| sk_c6 != sk_c6 ),
inference(copy,[status(thm)],[c_31659]) ).
cnf(c_31661,plain,
( sk_c6 != sk_c6
| sk_c6 != sk_c6 ),
inference(copy,[status(thm)],[c_31660]) ).
cnf(c_31662,plain,
sk_c6 != sk_c6,
inference(copy,[status(thm)],[c_31661]) ).
cnf(c_31579,plain,
$false,
inference(copy,[status(thm)],[c_31662]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP272-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.37 % Computer : n015.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Fri Sep 25 14:45:33 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/5.37 % Process 1628881 was started by sandbox2 on n015,
% 0.10/5.37 % Fri Sep 25 14:45:33 2026
% 0.10/5.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/5.37
% 0.10/5.37 % From the command line: assign(max_seconds, 300).
% 154.87/25.46
% 154.87/25.46 % given #500 (T,wt=10): 12305 identity = sk_c5 | multiply(sk_c5,multiply(sk_c3,sk_c4)) = identity. [para(12274(b,1),483(a,1,2))].
% 154.87/25.46
% 154.87/25.46 % given #1000 (F,wt=39): 8758 multiply(A,multiply(B,sk_c7)) != sk_c6 | multiply(inverse(B),inverse(A)) != sk_c7 | multiply(sk_c7,sk_c5) != sk_c6 | identity != sk_c5 | multiply(sk_c6,sk_c7) != sk_c5 | multiply(inverse(sk_c7),sk_c6) != sk_c7 | multiply(inverse(sk_c6),sk_c5) != sk_c6. [para(5496(a,1),4423(b,1)),rewrite([3(3)])].
% 154.87/25.46
% 154.87/25.46 % SZS status Unsatisfiable for theBenchmark
% 154.87/25.46
% 154.87/25.46 % Proof 1 at 16.43 (+ 3.20) seconds.
% 154.87/25.46 % Length of proof is 111.
% 154.87/25.46 % Level of proof is 25.
% 154.87/25.46 % Maximum clause weight is 46.000.
% 154.87/25.46 % Given clauses 1049.
% 154.87/25.46
% 154.87/25.46 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------