%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP288-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 : n010.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 143.60s 19.40s
% Output : CNFRefutation 143.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 25
% Syntax : Number of formulae : 206 ( 26 unt; 0 def)
% Number of atoms : 512 ( 511 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 446 ( 140 ~; 306 |; 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 : 50 ( 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_3,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c7,sk_c6) = sk_c5 ),
file('theBenchmark.p',prove_this_3) ).
cnf(c_6,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c7,sk_c6) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_3]) ).
fof(prove_this_4,axiom,
( multiply(sk_c4,sk_c6) = sk_c7
| multiply(sk_c7,sk_c6) = sk_c5 ),
file('theBenchmark.p',prove_this_4) ).
cnf(c_7,plain,
( multiply(sk_c4,sk_c6) = sk_c7
| multiply(sk_c7,sk_c6) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_4]) ).
fof(prove_this_5,axiom,
( inverse(sk_c4) = sk_c6
| multiply(sk_c7,sk_c6) = sk_c5 ),
file('theBenchmark.p',prove_this_5) ).
cnf(c_8,plain,
( inverse(sk_c4) = sk_c6
| multiply(sk_c7,sk_c6) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_5]) ).
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,
( inverse(sk_c3) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_7) ).
cnf(c_10,plain,
( inverse(sk_c3) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_7]) ).
fof(prove_this_8,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_11,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_8]) ).
fof(prove_this_9,axiom,
( multiply(sk_c4,sk_c6) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_9) ).
cnf(c_12,plain,
( multiply(sk_c4,sk_c6) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_9]) ).
fof(prove_this_10,axiom,
( inverse(sk_c4) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_10) ).
cnf(c_13,plain,
( inverse(sk_c4) = 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,
( inverse(sk_c3) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_12) ).
cnf(c_15,plain,
( inverse(sk_c3) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_12]) ).
fof(prove_this_13,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_13) ).
cnf(c_16,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_13]) ).
fof(prove_this_14,axiom,
( multiply(sk_c4,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_14) ).
cnf(c_17,plain,
( multiply(sk_c4,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_14]) ).
fof(prove_this_15,axiom,
( inverse(sk_c4) = sk_c6
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_15) ).
cnf(c_18,plain,
( inverse(sk_c4) = sk_c6
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_15]) ).
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_18,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c2,sk_c6) = sk_c5 ),
file('theBenchmark.p',prove_this_18) ).
cnf(c_21,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_18]) ).
fof(prove_this_19,axiom,
( multiply(sk_c4,sk_c6) = sk_c7
| multiply(sk_c2,sk_c6) = sk_c5 ),
file('theBenchmark.p',prove_this_19) ).
cnf(c_22,plain,
( multiply(sk_c4,sk_c6) = sk_c7
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_19]) ).
fof(prove_this_20,axiom,
( inverse(sk_c4) = sk_c6
| multiply(sk_c2,sk_c6) = sk_c5 ),
file('theBenchmark.p',prove_this_20) ).
cnf(c_23,plain,
( inverse(sk_c4) = 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_23,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_23) ).
cnf(c_26,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_23]) ).
fof(prove_this_24,axiom,
( multiply(sk_c4,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_24) ).
cnf(c_27,plain,
( multiply(sk_c4,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_24]) ).
fof(prove_this_25,axiom,
( inverse(sk_c4) = sk_c6
| inverse(sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_25) ).
cnf(c_28,plain,
( inverse(sk_c4) = 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] :
( inverse(VAR_3) != sk_c6
| multiply(VAR_3,sk_c6) != sk_c7
| 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
| 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,
( inverse(D) != sk_c6
| multiply(D,sk_c6) != sk_c7
| 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
| 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_31,plain,
( inverse(C) != sk_c6
| multiply(C,sk_c6) != sk_c7
| multiply(A,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_37,plain,
( multiply(B,sk_c6) != sk_c7
| multiply(A,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_31]) ).
cnf(c_32353,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_32354,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_32353]) ).
cnf(c_45,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_32354]) ).
cnf(c_56,plain,
( multiply(sk_c7,sk_c3) = identity
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_10,c_2]) ).
cnf(c_63,plain,
( multiply(sk_c7,sk_c3) = identity
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_15,c_2]) ).
cnf(c_64,plain,
( multiply(sk_c7,sk_c1) = identity
| multiply(sk_c3,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_16,c_2]) ).
cnf(c_65,plain,
( multiply(sk_c7,sk_c1) = identity
| multiply(sk_c4,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_17,c_2]) ).
cnf(c_78,plain,
( multiply(sk_c6,sk_c2) = identity
| multiply(sk_c4,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_27,c_2]) ).
cnf(c_537,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_45]) ).
cnf(c_545,plain,
( multiply(sk_c7,multiply(sk_c3,A)) = A
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_10,c_45]) ).
cnf(c_564,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_45,c_45]) ).
cnf(c_565,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_564,c_537]) ).
cnf(c_566,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_565,c_2]) ).
cnf(c_32355,plain,
( multiply(A,sk_c6) != sk_c7
| multiply(identity,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c5
| identity != sk_c7
| multiply(identity,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(paramod,[status(thm)],[c_566,c_37]) ).
cnf(c_32356,plain,
( multiply(A,sk_c6) != sk_c7
| multiply(identity,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c5
| identity != sk_c7
| sk_c7 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(paramod,[status(thm)],[c_1,c_32355]) ).
cnf(c_32357,plain,
( multiply(A,sk_c6) != sk_c7
| sk_c6 != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c5
| identity != sk_c7
| sk_c7 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(paramod,[status(thm)],[c_1,c_32356]) ).
cnf(c_32358,plain,
( multiply(A,sk_c6) != sk_c7
| sk_c7 != sk_c6
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c5
| identity != sk_c7
| sk_c7 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(copy,[status(thm)],[c_32357]) ).
cnf(c_583,plain,
( multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c5
| identity != sk_c7
| sk_c7 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(copy,[status(thm)],[c_32358]) ).
cnf(c_769,plain,
multiply(A,inverse(A)) = identity,
inference(paramod,[status(thm)],[c_564,c_2]) ).
cnf(c_32359,plain,
multiply(A,identity) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_564,c_565]) ).
cnf(c_32360,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_565,c_32359]) ).
cnf(c_787,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_32360]) ).
cnf(c_885,plain,
( multiply(sk_c4,sk_c6) = identity
| multiply(sk_c7,sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_8,c_769]) ).
cnf(c_887,plain,
( multiply(sk_c4,sk_c6) = identity
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_13,c_769]) ).
cnf(c_888,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_14,c_769]) ).
cnf(c_892,plain,
( multiply(sk_c4,sk_c6) = identity
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_18,c_769]) ).
cnf(c_894,plain,
( multiply(sk_c4,sk_c6) = identity
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_23,c_769]) ).
cnf(c_895,plain,
( multiply(sk_c2,sk_c6) = identity
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_24,c_769]) ).
cnf(c_897,plain,
( multiply(sk_c2,sk_c6) = identity
| multiply(sk_c3,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_26,c_769]) ).
cnf(c_899,plain,
( multiply(sk_c4,sk_c6) = identity
| inverse(sk_c2) = sk_c6 ),
inference(paramod,[status(thm)],[c_28,c_769]) ).
cnf(c_900,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c7,sk_c3) = identity ),
inference(paramod,[status(thm)],[c_63,c_769]) ).
cnf(c_32361,plain,
( multiply(inverse(sk_c6),sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(inverse(sk_c6),sk_c6) != sk_c5
| identity != sk_c7
| sk_c7 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(resolve,[status(thm)],[c_583,c_787]) ).
cnf(c_32362,plain,
( multiply(inverse(sk_c6),sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c5
| identity != sk_c7
| sk_c7 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(paramod,[status(thm)],[c_2,c_32361]) ).
cnf(c_32363,plain,
( identity != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c5
| identity != sk_c7
| sk_c7 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(paramod,[status(thm)],[c_2,c_32362]) ).
cnf(c_1206,plain,
( multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c5
| identity != sk_c7
| sk_c7 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(copy,[status(thm)],[c_32363]) ).
cnf(c_2562,plain,
( multiply(sk_c7,sk_c1) = identity
| multiply(sk_c4,sk_c6) = identity ),
inference(paramod,[status(thm)],[c_892,c_2]) ).
cnf(c_2769,plain,
( multiply(sk_c6,sk_c2) = identity
| multiply(sk_c4,sk_c6) = identity ),
inference(paramod,[status(thm)],[c_899,c_2]) ).
cnf(c_32364,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c6) = sk_c5
| multiply(sk_c7,sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_885,c_7]) ).
cnf(c_5581,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c6) = sk_c5 ),
inference(copy,[status(thm)],[c_32364]) ).
cnf(c_5585,plain,
( multiply(inverse(sk_c7),sk_c5) = sk_c6
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_5581,c_45]) ).
cnf(c_32365,plain,
( identity = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_887,c_12]) ).
cnf(c_5913,plain,
( identity = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(copy,[status(thm)],[c_32365]) ).
cnf(c_32366,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| identity = sk_c6
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_888,c_9]) ).
cnf(c_5944,plain,
( identity = sk_c6
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_32366]) ).
cnf(c_32367,plain,
( identity = sk_c7
| multiply(sk_c2,sk_c6) = sk_c5
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_894,c_22]) ).
cnf(c_6380,plain,
( identity = sk_c7
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(copy,[status(thm)],[c_32367]) ).
cnf(c_32368,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| identity = sk_c5
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_895,c_19]) ).
cnf(c_6855,plain,
( identity = sk_c5
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_32368]) ).
cnf(c_32369,plain,
( multiply(sk_c7,sk_c3) = identity
| identity = sk_c6
| multiply(sk_c7,sk_c3) = identity ),
inference(paramod,[status(thm)],[c_900,c_56]) ).
cnf(c_7251,plain,
( identity = sk_c6
| multiply(sk_c7,sk_c3) = identity ),
inference(copy,[status(thm)],[c_32369]) ).
cnf(c_32370,plain,
( multiply(inverse(sk_c7),identity) = sk_c3
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_7251,c_45]) ).
cnf(c_7254,plain,
( inverse(sk_c7) = sk_c3
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_565,c_32370]) ).
cnf(c_32371,plain,
( multiply(sk_c7,sk_c1) = identity
| identity = sk_c7
| multiply(sk_c7,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_2562,c_65]) ).
cnf(c_9356,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c1) = identity ),
inference(copy,[status(thm)],[c_32371]) ).
cnf(c_32372,plain,
( multiply(inverse(sk_c7),identity) = sk_c1
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_9356,c_45]) ).
cnf(c_9431,plain,
( inverse(sk_c7) = sk_c1
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_565,c_32372]) ).
cnf(c_9432,plain,
( multiply(sk_c1,sk_c7) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_9431,c_2]) ).
cnf(c_32373,plain,
( identity = sk_c7
| identity = sk_c6
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_9432,c_5913]) ).
cnf(c_9553,plain,
( identity = sk_c6
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_32373]) ).
cnf(c_9664,plain,
( multiply(A,sk_c7) = A
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9553,c_565]) ).
cnf(c_9665,plain,
( inverse(sk_c7) = identity
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9553,c_566]) ).
cnf(c_32374,plain,
( identity = sk_c3
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9665,c_7254]) ).
cnf(c_9718,plain,
( identity = sk_c3
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_32374]) ).
cnf(c_32375,plain,
( identity = sk_c6
| sk_c3 = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9718,c_9553]) ).
cnf(c_9739,plain,
( sk_c3 = sk_c7
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_32375]) ).
cnf(c_9741,plain,
( multiply(A,sk_c6) = A
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_9739,c_565]) ).
cnf(c_9742,plain,
( inverse(sk_c6) = identity
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_9739,c_566]) ).
cnf(c_32376,plain,
( identity = sk_c6
| sk_c6 = sk_c5
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9664,c_5944]) ).
cnf(c_32377,plain,
( identity = sk_c6
| sk_c5 = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_32376]) ).
cnf(c_10466,plain,
( sk_c5 = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_32377]) ).
cnf(c_32378,plain,
( sk_c3 = sk_c7
| multiply(sk_c7,sk_c6) = sk_c5
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_9741,c_6]) ).
cnf(c_10894,plain,
( multiply(sk_c7,sk_c6) = sk_c5
| sk_c3 = sk_c7 ),
inference(copy,[status(thm)],[c_32378]) ).
cnf(c_32379,plain,
( sk_c3 = sk_c7
| multiply(sk_c2,sk_c6) = sk_c5
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_9741,c_21]) ).
cnf(c_10897,plain,
( multiply(sk_c2,sk_c6) = sk_c5
| sk_c3 = sk_c7 ),
inference(copy,[status(thm)],[c_32379]) ).
cnf(c_32380,plain,
( multiply(sk_c7,sk_c1) = identity
| sk_c3 = sk_c7
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_9741,c_64]) ).
cnf(c_10923,plain,
( multiply(sk_c7,sk_c1) = identity
| sk_c3 = sk_c7 ),
inference(copy,[status(thm)],[c_32380]) ).
cnf(c_32381,plain,
( multiply(sk_c2,sk_c6) = identity
| sk_c3 = sk_c7
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_9741,c_897]) ).
cnf(c_10947,plain,
( multiply(sk_c2,sk_c6) = identity
| sk_c3 = sk_c7 ),
inference(copy,[status(thm)],[c_32381]) ).
cnf(c_11417,plain,
( multiply(inverse(sk_c7),sk_c5) = sk_c6
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_10894,c_45]) ).
cnf(c_32382,plain,
( multiply(inverse(sk_c7),identity) = sk_c1
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_10923,c_45]) ).
cnf(c_11569,plain,
( inverse(sk_c7) = sk_c1
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_565,c_32382]) ).
cnf(c_32383,plain,
( identity = sk_c5
| sk_c3 = sk_c7
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_10947,c_10897]) ).
cnf(c_12120,plain,
( identity = sk_c5
| sk_c3 = sk_c7 ),
inference(copy,[status(thm)],[c_32383]) ).
cnf(c_12122,plain,
( multiply(A,sk_c5) = A
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_12120,c_565]) ).
cnf(c_32384,plain,
( sk_c6 = inverse(sk_c7)
| sk_c3 = sk_c7
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_11417,c_12122]) ).
cnf(c_32385,plain,
( inverse(sk_c7) = sk_c6
| sk_c3 = sk_c7
| sk_c3 = sk_c7 ),
inference(copy,[status(thm)],[c_32384]) ).
cnf(c_12918,plain,
( inverse(sk_c7) = sk_c6
| sk_c3 = sk_c7 ),
inference(copy,[status(thm)],[c_32385]) ).
cnf(c_12968,plain,
( inverse(sk_c6) = sk_c7
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_12918,c_787]) ).
cnf(c_32386,plain,
( sk_c7 = identity
| sk_c3 = sk_c7
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_12968,c_9742]) ).
cnf(c_32387,plain,
( identity = sk_c7
| sk_c3 = sk_c7
| sk_c3 = sk_c7 ),
inference(copy,[status(thm)],[c_32386]) ).
cnf(c_13055,plain,
( identity = sk_c7
| sk_c3 = sk_c7 ),
inference(copy,[status(thm)],[c_32387]) ).
cnf(c_13060,plain,
( inverse(sk_c7) = identity
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_13055,c_566]) ).
cnf(c_32388,plain,
( identity = sk_c1
| sk_c3 = sk_c7
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_13060,c_11569]) ).
cnf(c_13180,plain,
( identity = sk_c1
| sk_c3 = sk_c7 ),
inference(copy,[status(thm)],[c_32388]) ).
cnf(c_32389,plain,
( inverse(sk_c7) = sk_c7
| sk_c3 = sk_c7
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_13055,c_13060]) ).
cnf(c_13183,plain,
( inverse(sk_c7) = sk_c7
| sk_c3 = sk_c7 ),
inference(copy,[status(thm)],[c_32389]) ).
cnf(c_13428,plain,
( multiply(sk_c7,sk_c7) = identity
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_13183,c_2]) ).
cnf(c_32390,plain,
( multiply(sk_c7,sk_c7) = sk_c1
| sk_c3 = sk_c7
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_13180,c_13428]) ).
cnf(c_15492,plain,
( multiply(sk_c7,sk_c7) = sk_c1
| sk_c3 = sk_c7 ),
inference(copy,[status(thm)],[c_32390]) ).
cnf(c_32391,plain,
( multiply(sk_c6,sk_c2) = identity
| identity = sk_c7
| multiply(sk_c6,sk_c2) = identity ),
inference(paramod,[status(thm)],[c_2769,c_78]) ).
cnf(c_17229,plain,
( identity = sk_c7
| multiply(sk_c6,sk_c2) = identity ),
inference(copy,[status(thm)],[c_32391]) ).
cnf(c_32392,plain,
( multiply(inverse(sk_c6),identity) = sk_c2
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_17229,c_45]) ).
cnf(c_17232,plain,
( inverse(sk_c6) = sk_c2
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_565,c_32392]) ).
cnf(c_17239,plain,
( multiply(sk_c2,sk_c6) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_17232,c_2]) ).
cnf(c_32393,plain,
( identity = sk_c7
| identity = sk_c5
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_17239,c_6380]) ).
cnf(c_17503,plain,
( identity = sk_c5
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_32393]) ).
cnf(c_17507,plain,
( multiply(A,sk_c5) = A
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_17503,c_565]) ).
cnf(c_17508,plain,
( inverse(sk_c5) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_17503,c_566]) ).
cnf(c_32394,plain,
( sk_c5 = sk_c6
| sk_c5 = sk_c6
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_17503,c_10466]) ).
cnf(c_17517,plain,
( sk_c5 = sk_c6
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_32394]) ).
cnf(c_17520,plain,
( multiply(A,sk_c7) = A
| sk_c5 = sk_c6 ),
inference(paramod,[status(thm)],[c_17517,c_565]) ).
cnf(c_32395,plain,
( inverse(sk_c7) = sk_c6
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_17507,c_5585]) ).
cnf(c_18216,plain,
( inverse(sk_c7) = sk_c6
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_32395]) ).
cnf(c_18321,plain,
( inverse(sk_c6) = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_18216,c_787]) ).
cnf(c_32396,plain,
( identity = sk_c5
| sk_c6 = sk_c5
| sk_c5 = sk_c6 ),
inference(paramod,[status(thm)],[c_17520,c_6855]) ).
cnf(c_32397,plain,
( identity = sk_c5
| sk_c5 = sk_c6
| sk_c5 = sk_c6 ),
inference(copy,[status(thm)],[c_32396]) ).
cnf(c_19049,plain,
( identity = sk_c5
| sk_c5 = sk_c6 ),
inference(copy,[status(thm)],[c_32397]) ).
cnf(c_32398,plain,
( sk_c5 = sk_c6
| sk_c5 = sk_c6
| sk_c5 = sk_c6 ),
inference(paramod,[status(thm)],[c_19049,c_10466]) ).
cnf(c_32399,plain,
( sk_c5 = sk_c6
| sk_c5 = sk_c6 ),
inference(copy,[status(thm)],[c_32398]) ).
cnf(c_19107,plain,
sk_c5 = sk_c6,
inference(copy,[status(thm)],[c_32399]) ).
cnf(c_19653,plain,
( inverse(sk_c6) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_19107,c_17508]) ).
cnf(c_32400,plain,
( multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c5
| identity != sk_c7
| sk_c7 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c6 ),
inference(paramod,[status(thm)],[c_19107,c_1206]) ).
cnf(c_32401,plain,
( multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c6
| identity != sk_c7
| sk_c7 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c6 ),
inference(paramod,[status(thm)],[c_19107,c_32400]) ).
cnf(c_26643,plain,
( multiply(sk_c6,sk_c7) != sk_c6
| identity != sk_c6
| identity != sk_c7
| sk_c7 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c6 ),
inference(paramod,[status(thm)],[c_19107,c_32401]) ).
cnf(c_32402,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_11,c_545]) ).
cnf(c_28798,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(copy,[status(thm)],[c_32402]) ).
cnf(c_32403,plain,
( identity = sk_c7
| identity = sk_c7
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_19653,c_18321]) ).
cnf(c_32404,plain,
( identity = sk_c7
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_32403]) ).
cnf(c_28845,plain,
identity = sk_c7,
inference(copy,[status(thm)],[c_32404]) ).
cnf(c_32405,plain,
( multiply(sk_c6,sk_c7) != sk_c6
| identity != sk_c6
| sk_c7 != sk_c7
| sk_c7 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c6 ),
inference(paramod,[status(thm)],[c_28845,c_26643]) ).
cnf(c_32406,plain,
( multiply(sk_c6,sk_c7) != sk_c6
| sk_c7 != sk_c6
| sk_c7 != sk_c7
| sk_c7 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c6 ),
inference(paramod,[status(thm)],[c_28845,c_32405]) ).
cnf(c_32407,plain,
( multiply(sk_c6,sk_c7) != sk_c6
| sk_c7 != sk_c6
| sk_c7 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c6 ),
inference(copy,[status(thm)],[c_32406]) ).
cnf(c_29322,plain,
( multiply(sk_c6,sk_c7) != sk_c6
| sk_c7 != sk_c6
| multiply(sk_c7,sk_c6) != sk_c6 ),
inference(copy,[status(thm)],[c_32407]) ).
cnf(c_31092,plain,
multiply(A,sk_c7) = A,
inference(paramod,[status(thm)],[c_28845,c_565]) ).
cnf(c_31097,plain,
( multiply(sk_c7,sk_c1) = sk_c7
| multiply(sk_c3,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_28845,c_64]) ).
cnf(c_31102,plain,
multiply(sk_c7,A) = A,
inference(paramod,[status(thm)],[c_28845,c_1]) ).
cnf(c_32408,plain,
( multiply(sk_c6,sk_c7) != sk_c6
| sk_c7 != sk_c6
| sk_c6 != sk_c6 ),
inference(paramod,[status(thm)],[c_31102,c_29322]) ).
cnf(c_32409,plain,
( sk_c6 != sk_c6
| sk_c7 != sk_c6
| sk_c6 != sk_c6 ),
inference(paramod,[status(thm)],[c_31092,c_32408]) ).
cnf(c_32410,plain,
( sk_c6 != sk_c6
| sk_c7 != sk_c6 ),
inference(copy,[status(thm)],[c_32409]) ).
cnf(c_31954,plain,
sk_c7 != sk_c6,
inference(copy,[status(thm)],[c_32410]) ).
cnf(c_32411,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| sk_c1 = sk_c6 ),
inference(paramod,[status(thm)],[c_31092,c_28798]) ).
cnf(c_32412,plain,
( sk_c7 = sk_c6
| sk_c1 = sk_c6 ),
inference(paramod,[status(thm)],[c_31092,c_32411]) ).
cnf(c_31988,plain,
sk_c1 = sk_c6,
inference(resolve,[status(thm)],[c_31954,c_32412]) ).
cnf(c_32413,plain,
( sk_c7 = sk_c1
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_31092,c_15492]) ).
cnf(c_32414,plain,
( sk_c7 = sk_c6
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_31988,c_32413]) ).
cnf(c_32351,plain,
sk_c3 = sk_c7,
inference(resolve,[status(thm)],[c_31954,c_32414]) ).
cnf(c_32415,plain,
( multiply(sk_c7,sk_c1) = sk_c7
| multiply(sk_c7,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_32351,c_31097]) ).
cnf(c_32416,plain,
( multiply(sk_c7,sk_c1) = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_31102,c_32415]) ).
cnf(c_32417,plain,
( multiply(sk_c7,sk_c6) = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_31988,c_32416]) ).
cnf(c_32418,plain,
( sk_c6 = sk_c7
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_31102,c_32417]) ).
cnf(c_32419,plain,
( sk_c6 = sk_c7
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_32418]) ).
cnf(c_32420,plain,
( sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_32419]) ).
cnf(c_32421,plain,
sk_c7 = sk_c6,
inference(copy,[status(thm)],[c_32420]) ).
cnf(c_32352,plain,
$false,
inference(resolve,[status(thm)],[c_31954,c_32421]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP288-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.19/0.46 % Computer : n010.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Fri Sep 25 14:43:30 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.47 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.19/0.47 % Process 997975 was started by sandbox2 on n010,
% 0.19/0.47 % Fri Sep 25 14:43:30 2026
% 0.19/0.47 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.19/0.47
% 0.19/0.47 % From the command line: assign(max_seconds, 300).
% 143.60/19.40
% 143.60/19.40 % given #500 (A,wt=49): 108 inverse(sk_c1) = sk_c7 | multiply(sk_c7,sk_c6) != sk_c5 | multiply(A,sk_c7) != sk_c6 | inverse(A) != sk_c7 | multiply(sk_c3,sk_c6) != sk_c5 | sk_c7 != sk_c6 | multiply(sk_c6,sk_c7) != sk_c5 | inverse(B) != sk_c7 | multiply(B,sk_c6) != sk_c7 | multiply(C,sk_c6) != sk_c7 | inverse(C) != sk_c6. [para(15(b,1),29(e,1))].
% 143.60/19.40
% 143.60/19.40 % SZS status Unsatisfiable for theBenchmark
% 143.60/19.40
% 143.60/19.40 % Proof 1 at 16.57 (+ 2.25) seconds.
% 143.60/19.40 % Length of proof is 112.
% 143.60/19.40 % Level of proof is 25.
% 143.60/19.40 % Maximum clause weight is 46.000.
% 143.60/19.40 % Given clauses 922.
% 143.60/19.40
% 143.60/19.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------