%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP287-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 : n007.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:33 AM UTC 2026
% Result : Unsatisfiable 245.24s 32.54s
% Output : CNFRefutation 245.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 19
% Syntax : Number of formulae : 147 ( 27 unt; 0 def)
% Number of atoms : 391 ( 390 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 392 ( 148 ~; 244 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 3 avg)
% Maximal term depth : 4 ( 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 : 52 ( 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_c7,sk_c6) = sk_c5 ),
file('theBenchmark.p',prove_this_1) ).
cnf(c_4,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c7,sk_c6) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_1]) ).
fof(prove_this_6,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_6) ).
cnf(c_9,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_6]) ).
fof(prove_this_7,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_7) ).
cnf(c_10,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_7]) ).
fof(prove_this_8,axiom,
( inverse(sk_c3) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_11,plain,
( inverse(sk_c3) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_8]) ).
fof(prove_this_9,axiom,
( inverse(sk_c4) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_9) ).
cnf(c_12,plain,
( inverse(sk_c4) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_9]) ).
fof(prove_this_10,axiom,
( multiply(sk_c4,sk_c5) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_10) ).
cnf(c_13,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_10]) ).
fof(prove_this_11,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_11) ).
cnf(c_14,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_11]) ).
fof(prove_this_12,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_12) ).
cnf(c_15,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_12]) ).
fof(prove_this_13,axiom,
( inverse(sk_c3) = sk_c6
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_13) ).
cnf(c_16,plain,
( inverse(sk_c3) = sk_c6
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_13]) ).
fof(prove_this_14,axiom,
( inverse(sk_c4) = sk_c6
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_14) ).
cnf(c_17,plain,
( inverse(sk_c4) = sk_c6
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_14]) ).
fof(prove_this_15,axiom,
( multiply(sk_c4,sk_c5) = sk_c6
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_15) ).
cnf(c_18,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_15]) ).
fof(prove_this_17,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c2,sk_c6) = sk_c5 ),
file('theBenchmark.p',prove_this_17) ).
cnf(c_20,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_17]) ).
fof(prove_this_18,axiom,
( inverse(sk_c3) = sk_c6
| multiply(sk_c2,sk_c6) = sk_c5 ),
file('theBenchmark.p',prove_this_18) ).
cnf(c_21,plain,
( inverse(sk_c3) = sk_c6
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_18]) ).
fof(prove_this_22,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_22) ).
cnf(c_25,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_22]) ).
fof(prove_this_23,axiom,
( inverse(sk_c3) = sk_c6
| inverse(sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_23) ).
cnf(c_26,plain,
( inverse(sk_c3) = sk_c6
| inverse(sk_c2) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_23]) ).
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
| inverse(VAR_2) != sk_c6
| multiply(VAR_2,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(VAR_1) != sk_c6
| multiply(VAR_1,sk_c6) != sk_c5
| inverse(VAR_0) != sk_c7
| multiply(VAR_0,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
file('theBenchmark.p',prove_this_26) ).
cnf(c_29,plain,
( multiply(D,sk_c5) != sk_c6
| inverse(D) != sk_c6
| inverse(C) != sk_c6
| multiply(C,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(B) != sk_c6
| multiply(B,sk_c6) != sk_c5
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(clausify,[status(thm)],[prove_this_26]) ).
cnf(c_32,plain,
( multiply(B,sk_c5) != sk_c6
| inverse(C) != sk_c6
| multiply(C,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(B) != sk_c6
| multiply(B,sk_c6) != sk_c5
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(factor,[status(thm)],[c_29]) ).
cnf(c_29145,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_29146,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_29145]) ).
cnf(c_39,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_29146]) ).
cnf(c_40,plain,
( multiply(sk_c5,A) = multiply(sk_c7,multiply(sk_c6,A))
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_4,c_3]) ).
cnf(c_53,plain,
( multiply(sk_c6,sk_c4) = identity
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_12,c_2]) ).
cnf(c_57,plain,
( multiply(sk_c7,sk_c1) = identity
| multiply(sk_c3,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_15,c_2]) ).
cnf(c_59,plain,
( multiply(sk_c6,sk_c4) = identity
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_17,c_2]) ).
cnf(c_375,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_39]) ).
cnf(c_402,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_39,c_39]) ).
cnf(c_403,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_402,c_375]) ).
cnf(c_404,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_403,c_2]) ).
cnf(c_29147,plain,
( multiply(identity,sk_c5) != sk_c6
| inverse(B) != sk_c6
| multiply(B,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c6
| multiply(identity,sk_c6) != sk_c5
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(paramod,[status(thm)],[c_404,c_32]) ).
cnf(c_29148,plain,
( multiply(identity,sk_c5) != sk_c6
| inverse(B) != sk_c6
| multiply(B,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c6
| sk_c6 != sk_c5
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(paramod,[status(thm)],[c_1,c_29147]) ).
cnf(c_29149,plain,
( sk_c5 != sk_c6
| inverse(B) != sk_c6
| multiply(B,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c6
| sk_c6 != sk_c5
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(paramod,[status(thm)],[c_1,c_29148]) ).
cnf(c_29150,plain,
( sk_c5 != sk_c6
| inverse(B) != sk_c6
| multiply(B,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c6
| sk_c5 != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(copy,[status(thm)],[c_29149]) ).
cnf(c_416,plain,
( inverse(B) != sk_c6
| multiply(B,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c6
| sk_c5 != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(copy,[status(thm)],[c_29150]) ).
cnf(c_571,plain,
multiply(A,inverse(A)) = identity,
inference(paramod,[status(thm)],[c_402,c_2]) ).
cnf(c_29151,plain,
multiply(A,identity) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_402,c_403]) ).
cnf(c_29152,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_403,c_29151]) ).
cnf(c_589,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_29152]) ).
cnf(c_29153,plain,
( inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c6
| sk_c5 != sk_c6
| multiply(inverse(sk_c7),sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(resolve,[status(thm)],[c_589,c_416]) ).
cnf(c_29154,plain,
( inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c6
| sk_c5 != sk_c6
| identity != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(paramod,[status(thm)],[c_2,c_29153]) ).
cnf(c_596,plain,
( inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c5 != sk_c6
| identity != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(copy,[status(thm)],[c_29154]) ).
cnf(c_29155,plain,
( multiply(inverse(sk_c6),sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c5 != sk_c6
| identity != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(resolve,[status(thm)],[c_596,c_589]) ).
cnf(c_673,plain,
( identity != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c5 != sk_c6
| identity != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(paramod,[status(thm)],[c_2,c_29155]) ).
cnf(c_706,plain,
( multiply(sk_c3,sk_c6) = identity
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_11,c_571]) ).
cnf(c_708,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_14,c_571]) ).
cnf(c_710,plain,
( multiply(sk_c3,sk_c6) = identity
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_16,c_571]) ).
cnf(c_712,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c4,sk_c5) = sk_c6 ),
inference(paramod,[status(thm)],[c_18,c_571]) ).
cnf(c_713,plain,
( multiply(sk_c3,sk_c6) = identity
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_21,c_571]) ).
cnf(c_717,plain,
( multiply(sk_c3,sk_c6) = identity
| inverse(sk_c2) = sk_c6 ),
inference(paramod,[status(thm)],[c_26,c_571]) ).
cnf(c_721,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c6,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_59,c_571]) ).
cnf(c_29156,plain,
( multiply(sk_c5,inverse(sk_c6)) = multiply(sk_c7,identity)
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_571,c_40]) ).
cnf(c_723,plain,
( multiply(sk_c5,inverse(sk_c6)) = sk_c7
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_403,c_29156]) ).
cnf(c_2470,plain,
( multiply(sk_c7,sk_c1) = identity
| multiply(sk_c3,sk_c6) = identity ),
inference(paramod,[status(thm)],[c_710,c_2]) ).
cnf(c_29157,plain,
( identity = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_706,c_10]) ).
cnf(c_16058,plain,
( identity = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(copy,[status(thm)],[c_29157]) ).
cnf(c_29158,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| identity = sk_c6
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_708,c_9]) ).
cnf(c_16201,plain,
( identity = sk_c6
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_29158]) ).
cnf(c_16213,plain,
( multiply(inverse(sk_c6),sk_c5) = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_16201,c_39]) ).
cnf(c_29159,plain,
( identity = sk_c7
| multiply(sk_c2,sk_c6) = sk_c5
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_713,c_20]) ).
cnf(c_16314,plain,
( identity = sk_c7
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(copy,[status(thm)],[c_29159]) ).
cnf(c_16319,plain,
( multiply(inverse(sk_c2),sk_c5) = sk_c6
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_16314,c_39]) ).
cnf(c_16378,plain,
( multiply(sk_c6,sk_c5) = sk_c6
| identity = sk_c7
| multiply(sk_c3,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_25,c_16319]) ).
cnf(c_16385,plain,
( multiply(sk_c6,sk_c5) = sk_c6
| identity = sk_c7
| multiply(sk_c3,sk_c6) = identity ),
inference(paramod,[status(thm)],[c_717,c_16319]) ).
cnf(c_29160,plain,
( multiply(sk_c6,sk_c4) = identity
| identity = sk_c6
| multiply(sk_c6,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_721,c_53]) ).
cnf(c_16872,plain,
( identity = sk_c6
| multiply(sk_c6,sk_c4) = identity ),
inference(copy,[status(thm)],[c_29160]) ).
cnf(c_29161,plain,
( multiply(inverse(sk_c6),identity) = sk_c4
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_16872,c_39]) ).
cnf(c_16875,plain,
( inverse(sk_c6) = sk_c4
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_403,c_29161]) ).
cnf(c_29162,plain,
( multiply(sk_c4,sk_c5) = sk_c7
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_16875,c_16213]) ).
cnf(c_17069,plain,
( multiply(sk_c4,sk_c5) = sk_c7
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_29162]) ).
cnf(c_17139,plain,
( multiply(inverse(sk_c4),sk_c7) = sk_c5
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_17069,c_39]) ).
cnf(c_29163,plain,
( multiply(sk_c7,sk_c1) = identity
| identity = sk_c7
| multiply(sk_c7,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_2470,c_57]) ).
cnf(c_19078,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c1) = identity ),
inference(copy,[status(thm)],[c_29163]) ).
cnf(c_29164,plain,
( multiply(inverse(sk_c7),identity) = sk_c1
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_19078,c_39]) ).
cnf(c_19081,plain,
( inverse(sk_c7) = sk_c1
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_403,c_29164]) ).
cnf(c_19083,plain,
( multiply(sk_c1,sk_c7) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_19081,c_2]) ).
cnf(c_29165,plain,
( identity = sk_c7
| identity = sk_c6
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_19083,c_16058]) ).
cnf(c_19224,plain,
( identity = sk_c6
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_29165]) ).
cnf(c_19226,plain,
( multiply(A,sk_c7) = A
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_19224,c_403]) ).
cnf(c_29166,plain,
( inverse(sk_c4) = sk_c5
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_19226,c_17139]) ).
cnf(c_19849,plain,
( inverse(sk_c4) = sk_c5
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_29166]) ).
cnf(c_19950,plain,
( multiply(sk_c4,sk_c5) = identity
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_19849,c_571]) ).
cnf(c_29167,plain,
( identity = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_19950,c_13]) ).
cnf(c_20509,plain,
( multiply(sk_c1,sk_c7) = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_29167]) ).
cnf(c_29168,plain,
( multiply(sk_c1,sk_c7) = identity
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_19950,c_712]) ).
cnf(c_20513,plain,
( multiply(sk_c1,sk_c7) = identity
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_29168]) ).
cnf(c_29169,plain,
( identity = sk_c6
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_20513,c_20509]) ).
cnf(c_29170,plain,
( identity = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_29169]) ).
cnf(c_21885,plain,
identity = sk_c6,
inference(copy,[status(thm)],[c_29170]) ).
cnf(c_29171,plain,
( multiply(sk_c6,sk_c5) = sk_c6
| identity = sk_c7
| multiply(sk_c3,sk_c6) = sk_c6 ),
inference(paramod,[status(thm)],[c_21885,c_16385]) ).
cnf(c_29172,plain,
( multiply(sk_c6,sk_c5) = sk_c6
| sk_c6 = sk_c7
| multiply(sk_c3,sk_c6) = sk_c6 ),
inference(paramod,[status(thm)],[c_21885,c_29171]) ).
cnf(c_23334,plain,
( multiply(sk_c6,sk_c5) = sk_c6
| sk_c7 = sk_c6
| multiply(sk_c3,sk_c6) = sk_c6 ),
inference(copy,[status(thm)],[c_29172]) ).
cnf(c_29173,plain,
( multiply(sk_c6,sk_c5) = sk_c6
| sk_c6 = sk_c7
| multiply(sk_c3,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_21885,c_16378]) ).
cnf(c_23341,plain,
( multiply(sk_c6,sk_c5) = sk_c6
| sk_c7 = sk_c6
| multiply(sk_c3,sk_c6) = sk_c7 ),
inference(copy,[status(thm)],[c_29173]) ).
cnf(c_29174,plain,
( identity != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c5 != sk_c6
| sk_c6 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(paramod,[status(thm)],[c_21885,c_673]) ).
cnf(c_29175,plain,
( sk_c6 != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c5 != sk_c6
| sk_c6 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(paramod,[status(thm)],[c_21885,c_29174]) ).
cnf(c_29176,plain,
( sk_c7 != sk_c6
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c5 != sk_c6
| sk_c6 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(copy,[status(thm)],[c_29175]) ).
cnf(c_27998,plain,
( sk_c7 != sk_c6
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c5 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(copy,[status(thm)],[c_29176]) ).
cnf(c_29177,plain,
inverse(sk_c6) = identity,
inference(paramod,[status(thm)],[c_21885,c_404]) ).
cnf(c_28034,plain,
inverse(sk_c6) = sk_c6,
inference(paramod,[status(thm)],[c_21885,c_29177]) ).
cnf(c_28035,plain,
multiply(A,sk_c6) = A,
inference(paramod,[status(thm)],[c_21885,c_403]) ).
cnf(c_28051,plain,
multiply(sk_c6,A) = A,
inference(paramod,[status(thm)],[c_21885,c_1]) ).
cnf(c_29178,plain,
( multiply(sk_c5,inverse(sk_c6)) = sk_c7
| sk_c7 = sk_c5 ),
inference(paramod,[status(thm)],[c_28051,c_723]) ).
cnf(c_29179,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| sk_c7 = sk_c5 ),
inference(paramod,[status(thm)],[c_28034,c_29178]) ).
cnf(c_29180,plain,
( sk_c5 = sk_c7
| sk_c7 = sk_c5 ),
inference(paramod,[status(thm)],[c_28035,c_29179]) ).
cnf(c_29181,plain,
( sk_c5 = sk_c7
| sk_c5 = sk_c7 ),
inference(copy,[status(thm)],[c_29180]) ).
cnf(c_28951,plain,
sk_c5 = sk_c7,
inference(copy,[status(thm)],[c_29181]) ).
cnf(c_29182,plain,
( sk_c7 != sk_c6
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c5 != sk_c6
| sk_c7 != sk_c5 ),
inference(paramod,[status(thm)],[c_28035,c_27998]) ).
cnf(c_29183,plain,
( sk_c7 != sk_c6
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c5 != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_28951,c_29182]) ).
cnf(c_29184,plain,
( sk_c7 != sk_c6
| multiply(sk_c6,sk_c7) != sk_c5
| sk_c7 != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_28951,c_29183]) ).
cnf(c_29185,plain,
( sk_c7 != sk_c6
| sk_c7 != sk_c5
| sk_c7 != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_28051,c_29184]) ).
cnf(c_29186,plain,
( sk_c7 != sk_c6
| sk_c7 != sk_c7
| sk_c7 != sk_c6
| sk_c7 != sk_c7 ),
inference(paramod,[status(thm)],[c_28951,c_29185]) ).
cnf(c_29187,plain,
( sk_c7 != sk_c6
| sk_c7 != sk_c7
| sk_c7 != sk_c6 ),
inference(copy,[status(thm)],[c_29186]) ).
cnf(c_29188,plain,
( sk_c7 != sk_c6
| sk_c7 != sk_c6 ),
inference(copy,[status(thm)],[c_29187]) ).
cnf(c_28977,plain,
sk_c7 != sk_c6,
inference(copy,[status(thm)],[c_29188]) ).
cnf(c_29189,plain,
( multiply(sk_c6,sk_c5) = sk_c6
| sk_c7 = sk_c6
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_28035,c_23341]) ).
cnf(c_29190,plain,
( multiply(sk_c6,sk_c7) = sk_c6
| sk_c7 = sk_c6
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_28951,c_29189]) ).
cnf(c_29191,plain,
( sk_c7 = sk_c6
| sk_c7 = sk_c6
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_28051,c_29190]) ).
cnf(c_29192,plain,
( sk_c7 = sk_c6
| sk_c3 = sk_c7 ),
inference(copy,[status(thm)],[c_29191]) ).
cnf(c_29143,plain,
sk_c3 = sk_c7,
inference(resolve,[status(thm)],[c_28977,c_29192]) ).
cnf(c_29193,plain,
( multiply(sk_c6,sk_c5) = sk_c6
| sk_c7 = sk_c6
| multiply(sk_c7,sk_c6) = sk_c6 ),
inference(paramod,[status(thm)],[c_29143,c_23334]) ).
cnf(c_29194,plain,
( multiply(sk_c6,sk_c5) = sk_c6
| sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_28035,c_29193]) ).
cnf(c_29195,plain,
( multiply(sk_c6,sk_c7) = sk_c6
| sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_28951,c_29194]) ).
cnf(c_29196,plain,
( sk_c7 = sk_c6
| sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_28051,c_29195]) ).
cnf(c_29197,plain,
( sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_29196]) ).
cnf(c_29198,plain,
sk_c7 = sk_c6,
inference(copy,[status(thm)],[c_29197]) ).
cnf(c_29144,plain,
$false,
inference(resolve,[status(thm)],[c_28977,c_29198]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP287-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.18/0.43 % Computer : n007.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Fri Sep 25 14:41:08 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.43 % Process 1246823 was started by sandbox2 on n007,
% 0.18/0.43 % Fri Sep 25 14:41:08 2026
% 0.18/0.43 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.18/0.44
% 0.18/0.44 % From the command line: assign(max_seconds, 300).
% 245.24/32.54
% 245.24/32.54 % given #500 (T,wt=8): 10375 sk_c4 = sk_c3 | multiply(sk_c2,sk_c1) = sk_c6. [para(3466(b,1),8585(b,2)),merge(b)].
% 245.24/32.54
% 245.24/32.54 % SZS status Unsatisfiable for theBenchmark
% 245.24/32.54
% 245.24/32.54 % Proof 1 at 27.26 (+ 4.59) seconds.
% 245.24/32.54 % Length of proof is 74.
% 245.24/32.54 % Level of proof is 19.
% 245.24/32.54 % Maximum clause weight is 46.000.
% 245.24/32.54 % Given clauses 992.
% 245.24/32.54
% 245.24/32.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------