%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP390-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:28:45 AM UTC 2026
% Result : Unsatisfiable 117.74s 15.39s
% Output : CNFRefutation 117.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 17
% Syntax : Number of formulae : 182 ( 25 unt; 0 def)
% Number of atoms : 558 ( 557 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 665 ( 289 ~; 376 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 77 ( 0 sgn 11 !; 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_c5,sk_c8) = sk_c7
| inverse(sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_3) ).
cnf(c_6,plain,
( multiply(sk_c5,sk_c8) = sk_c7
| inverse(sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_3]) ).
fof(prove_this_4,axiom,
( inverse(sk_c5) = sk_c8
| inverse(sk_c8) = sk_c7 ),
file('theBenchmark.p',prove_this_4) ).
cnf(c_7,plain,
( inverse(sk_c5) = sk_c8
| inverse(sk_c8) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_4]) ).
fof(prove_this_8,axiom,
( inverse(sk_c4) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_11,plain,
( inverse(sk_c4) = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_8]) ).
fof(prove_this_11,axiom,
( inverse(sk_c6) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('theBenchmark.p',prove_this_11) ).
cnf(c_14,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_11]) ).
fof(prove_this_12,axiom,
( multiply(sk_c6,sk_c8) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('theBenchmark.p',prove_this_12) ).
cnf(c_15,plain,
( multiply(sk_c6,sk_c8) = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_12]) ).
fof(prove_this_17,axiom,
( inverse(sk_c6) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_17) ).
cnf(c_20,plain,
( inverse(sk_c6) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_17]) ).
fof(prove_this_18,axiom,
( multiply(sk_c6,sk_c8) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('theBenchmark.p',prove_this_18) ).
cnf(c_21,plain,
( multiply(sk_c6,sk_c8) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
inference(clausify,[status(thm)],[prove_this_18]) ).
fof(prove_this_19,axiom,
( multiply(sk_c4,sk_c9) = sk_c8
| multiply(sk_c2,sk_c3) = sk_c8 ),
file('theBenchmark.p',prove_this_19) ).
cnf(c_22,plain,
( multiply(sk_c4,sk_c9) = sk_c8
| multiply(sk_c2,sk_c3) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_19]) ).
fof(prove_this_20,axiom,
( inverse(sk_c4) = sk_c9
| multiply(sk_c2,sk_c3) = sk_c8 ),
file('theBenchmark.p',prove_this_20) ).
cnf(c_23,plain,
( inverse(sk_c4) = sk_c9
| multiply(sk_c2,sk_c3) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_20]) ).
fof(prove_this_23,axiom,
( inverse(sk_c6) = sk_c9
| multiply(sk_c2,sk_c3) = sk_c8 ),
file('theBenchmark.p',prove_this_23) ).
cnf(c_26,plain,
( inverse(sk_c6) = sk_c9
| multiply(sk_c2,sk_c3) = sk_c8 ),
inference(clausify,[status(thm)],[prove_this_23]) ).
fof(prove_this_25,axiom,
( multiply(sk_c4,sk_c9) = sk_c8
| inverse(sk_c2) = sk_c3 ),
file('theBenchmark.p',prove_this_25) ).
cnf(c_28,plain,
( multiply(sk_c4,sk_c9) = sk_c8
| inverse(sk_c2) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_25]) ).
fof(prove_this_26,axiom,
( inverse(sk_c4) = sk_c9
| inverse(sk_c2) = sk_c3 ),
file('theBenchmark.p',prove_this_26) ).
cnf(c_29,plain,
( inverse(sk_c4) = sk_c9
| inverse(sk_c2) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_26]) ).
fof(prove_this_29,axiom,
( inverse(sk_c6) = sk_c9
| inverse(sk_c2) = sk_c3 ),
file('theBenchmark.p',prove_this_29) ).
cnf(c_32,plain,
( inverse(sk_c6) = sk_c9
| inverse(sk_c2) = sk_c3 ),
inference(clausify,[status(thm)],[prove_this_29]) ).
fof(prove_this_37,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( multiply(VAR_5,sk_c8) != sk_c9
| inverse(VAR_5) != sk_c9
| inverse(VAR_4) != sk_c8
| multiply(VAR_4,sk_c8) != sk_c7
| inverse(VAR_3) != sk_c9
| multiply(VAR_3,sk_c9) != sk_c8
| multiply(VAR_2,sk_c7) != sk_c8
| inverse(VAR_1) != VAR_2
| multiply(VAR_1,VAR_2) != sk_c8
| multiply(VAR_0,sk_c8) != sk_c9
| inverse(VAR_0) != sk_c9
| inverse(sk_c8) != sk_c7 ),
file('theBenchmark.p',prove_this_37) ).
cnf(c_40,plain,
( multiply(F,sk_c8) != sk_c9
| inverse(F) != sk_c9
| inverse(E) != sk_c8
| multiply(E,sk_c8) != sk_c7
| inverse(D) != sk_c9
| multiply(D,sk_c9) != sk_c8
| multiply(C,sk_c7) != sk_c8
| inverse(B) != C
| multiply(B,C) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(clausify,[status(thm)],[prove_this_37]) ).
cnf(c_43,plain,
( multiply(E,sk_c8) != sk_c9
| inverse(E) != sk_c9
| inverse(D) != sk_c8
| multiply(D,sk_c8) != sk_c7
| multiply(A,sk_c9) != sk_c8
| multiply(C,sk_c7) != sk_c8
| inverse(B) != C
| multiply(B,C) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_40]) ).
cnf(c_13861,plain,
( multiply(A,sk_c8) != sk_c9
| inverse(E) != sk_c8
| multiply(E,sk_c8) != sk_c7
| inverse(D) != sk_c9
| multiply(D,sk_c9) != sk_c8
| multiply(C,sk_c7) != sk_c8
| inverse(B) != C
| multiply(B,C) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_40]) ).
cnf(c_44,plain,
( inverse(E) != sk_c8
| multiply(E,sk_c8) != sk_c7
| inverse(D) != sk_c9
| multiply(D,sk_c9) != sk_c8
| multiply(C,sk_c7) != sk_c8
| inverse(B) != C
| multiply(B,C) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_13861]) ).
cnf(c_13862,plain,
( multiply(A,sk_c8) != sk_c9
| inverse(D) != sk_c8
| multiply(D,sk_c8) != sk_c7
| multiply(A,sk_c9) != sk_c8
| multiply(C,sk_c7) != sk_c8
| inverse(B) != C
| multiply(B,C) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_43]) ).
cnf(c_48,plain,
( inverse(D) != sk_c8
| multiply(D,sk_c8) != sk_c7
| multiply(A,sk_c9) != sk_c8
| multiply(C,sk_c7) != sk_c8
| inverse(B) != C
| multiply(B,C) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_13862]) ).
cnf(c_13863,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_13864,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_13863]) ).
cnf(c_56,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_13864]) ).
cnf(c_59,plain,
( multiply(sk_c7,sk_c8) = identity
| multiply(sk_c5,sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_6,c_2]) ).
cnf(c_60,plain,
( multiply(sk_c8,sk_c5) = identity
| inverse(sk_c8) = sk_c7 ),
inference(paramod,[status(thm)],[c_7,c_2]) ).
cnf(c_64,plain,
( multiply(sk_c9,sk_c4) = identity
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_11,c_2]) ).
cnf(c_67,plain,
( multiply(sk_c9,sk_c6) = identity
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_14,c_2]) ).
cnf(c_80,plain,
( multiply(sk_c9,sk_c4) = identity
| multiply(sk_c2,sk_c3) = sk_c8 ),
inference(paramod,[status(thm)],[c_23,c_2]) ).
cnf(c_84,plain,
( multiply(sk_c9,sk_c6) = identity
| multiply(sk_c2,sk_c3) = sk_c8 ),
inference(paramod,[status(thm)],[c_26,c_2]) ).
cnf(c_87,plain,
( multiply(sk_c3,sk_c2) = identity
| multiply(sk_c4,sk_c9) = sk_c8 ),
inference(paramod,[status(thm)],[c_28,c_2]) ).
cnf(c_88,plain,
( multiply(sk_c9,sk_c4) = identity
| inverse(sk_c2) = sk_c3 ),
inference(paramod,[status(thm)],[c_29,c_2]) ).
cnf(c_91,plain,
( multiply(sk_c9,sk_c6) = identity
| inverse(sk_c2) = sk_c3 ),
inference(paramod,[status(thm)],[c_32,c_2]) ).
cnf(c_121,plain,
( inverse(C) != sk_c8
| multiply(C,sk_c8) != sk_c7
| inverse(B) != sk_c9
| multiply(B,sk_c9) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c8
| inverse(identity) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(resolve,[status(thm)],[c_44,c_1]) ).
cnf(c_13865,plain,
( multiply(identity,sk_c8) != sk_c7
| inverse(B) != sk_c9
| multiply(B,sk_c9) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c8
| inverse(identity) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_121]) ).
cnf(c_13866,plain,
( sk_c8 != sk_c7
| inverse(B) != sk_c9
| multiply(B,sk_c9) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c8
| inverse(identity) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_1,c_13865]) ).
cnf(c_333,plain,
( sk_c7 != sk_c8
| inverse(B) != sk_c9
| multiply(B,sk_c9) != sk_c8
| multiply(sk_c8,sk_c7) != sk_c8
| inverse(identity) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_13866]) ).
cnf(c_1243,plain,
( multiply(sk_c7,sk_c8) = identity
| multiply(sk_c8,sk_c5) = identity ),
inference(paramod,[status(thm)],[c_60,c_2]) ).
cnf(c_1332,plain,
( multiply(sk_c9,sk_c1) = identity
| multiply(sk_c9,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_64,c_2]) ).
cnf(c_1392,plain,
( multiply(sk_c9,sk_c1) = identity
| multiply(sk_c9,sk_c6) = identity ),
inference(paramod,[status(thm)],[c_67,c_2]) ).
cnf(c_1558,plain,
( multiply(sk_c3,sk_c2) = identity
| multiply(sk_c9,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_88,c_2]) ).
cnf(c_1628,plain,
( multiply(sk_c3,sk_c2) = identity
| multiply(sk_c9,sk_c6) = identity ),
inference(paramod,[status(thm)],[c_91,c_2]) ).
cnf(c_1851,plain,
( sk_c7 != sk_c8
| inverse(inverse(sk_c9)) != sk_c9
| identity != sk_c8
| multiply(sk_c8,sk_c7) != sk_c8
| inverse(identity) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_333]) ).
cnf(c_3176,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_56]) ).
cnf(c_3241,plain,
( multiply(inverse(sk_c9),identity) = sk_c4
| multiply(sk_c9,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_1332,c_56]) ).
cnf(c_3243,plain,
( multiply(inverse(sk_c9),identity) = sk_c6
| multiply(sk_c9,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_1392,c_56]) ).
cnf(c_3244,plain,
( multiply(inverse(sk_c3),identity) = sk_c2
| multiply(sk_c9,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_1558,c_56]) ).
cnf(c_3246,plain,
( multiply(inverse(sk_c3),identity) = sk_c2
| multiply(sk_c9,sk_c6) = identity ),
inference(paramod,[status(thm)],[c_1628,c_56]) ).
cnf(c_3247,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_56,c_56]) ).
cnf(c_3255,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_3247,c_3176]) ).
cnf(c_3256,plain,
( inverse(sk_c3) = sk_c2
| multiply(sk_c9,sk_c6) = identity ),
inference(paramod,[status(thm)],[c_3255,c_3246]) ).
cnf(c_3258,plain,
( inverse(sk_c3) = sk_c2
| multiply(sk_c9,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_3255,c_3244]) ).
cnf(c_3259,plain,
( inverse(sk_c9) = sk_c6
| multiply(sk_c9,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_3255,c_3243]) ).
cnf(c_3261,plain,
( inverse(sk_c9) = sk_c4
| multiply(sk_c9,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_3255,c_3241]) ).
cnf(c_13867,plain,
( inverse(B) != sk_c8
| multiply(B,sk_c8) != sk_c7
| multiply(A,sk_c9) != sk_c8
| multiply(identity,sk_c7) != sk_c8
| inverse(sk_c8) != identity
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(resolve,[status(thm)],[c_3255,c_48]) ).
cnf(c_3371,plain,
( inverse(B) != sk_c8
| multiply(B,sk_c8) != sk_c7
| multiply(A,sk_c9) != sk_c8
| sk_c7 != sk_c8
| inverse(sk_c8) != identity
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_1,c_13867]) ).
cnf(c_3373,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_3255,c_2]) ).
cnf(c_13868,plain,
( sk_c7 != sk_c8
| inverse(inverse(sk_c9)) != sk_c9
| identity != sk_c8
| multiply(sk_c8,sk_c7) != sk_c8
| identity != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_3373,c_1851]) ).
cnf(c_4130,plain,
( sk_c7 != sk_c8
| inverse(inverse(sk_c9)) != sk_c9
| multiply(sk_c8,sk_c7) != sk_c8
| identity != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_13868]) ).
cnf(c_4526,plain,
( multiply(sk_c2,sk_c3) = identity
| multiply(sk_c9,sk_c6) = identity ),
inference(paramod,[status(thm)],[c_3256,c_2]) ).
cnf(c_4588,plain,
( multiply(sk_c2,sk_c3) = identity
| multiply(sk_c9,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_3258,c_2]) ).
cnf(c_13869,plain,
( sk_c4 = sk_c6
| multiply(sk_c9,sk_c1) = identity
| multiply(sk_c9,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_3261,c_3259]) ).
cnf(c_13870,plain,
( sk_c6 = sk_c4
| multiply(sk_c9,sk_c1) = identity
| multiply(sk_c9,sk_c1) = identity ),
inference(copy,[status(thm)],[c_13869]) ).
cnf(c_4781,plain,
( sk_c6 = sk_c4
| multiply(sk_c9,sk_c1) = identity ),
inference(copy,[status(thm)],[c_13870]) ).
cnf(c_13871,plain,
( multiply(inverse(sk_c9),identity) = sk_c1
| sk_c6 = sk_c4 ),
inference(paramod,[status(thm)],[c_4781,c_56]) ).
cnf(c_4786,plain,
( inverse(sk_c9) = sk_c1
| sk_c6 = sk_c4 ),
inference(paramod,[status(thm)],[c_3255,c_13871]) ).
cnf(c_4789,plain,
( multiply(sk_c1,sk_c9) = identity
| sk_c6 = sk_c4 ),
inference(paramod,[status(thm)],[c_4786,c_2]) ).
cnf(c_13872,plain,
( multiply(inverse(sk_c1),identity) = sk_c9
| sk_c6 = sk_c4 ),
inference(paramod,[status(thm)],[c_4789,c_56]) ).
cnf(c_4831,plain,
( inverse(sk_c1) = sk_c9
| sk_c6 = sk_c4 ),
inference(paramod,[status(thm)],[c_3255,c_13872]) ).
cnf(c_13873,plain,
( multiply(sk_c9,sk_c6) = identity
| identity = sk_c8
| multiply(sk_c9,sk_c6) = identity ),
inference(paramod,[status(thm)],[c_4526,c_84]) ).
cnf(c_5051,plain,
( identity = sk_c8
| multiply(sk_c9,sk_c6) = identity ),
inference(copy,[status(thm)],[c_13873]) ).
cnf(c_13874,plain,
( multiply(inverse(sk_c9),identity) = sk_c6
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_5051,c_56]) ).
cnf(c_5054,plain,
( inverse(sk_c9) = sk_c6
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_3255,c_13874]) ).
cnf(c_13875,plain,
( multiply(sk_c9,sk_c4) = identity
| identity = sk_c8
| multiply(sk_c9,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_4588,c_80]) ).
cnf(c_5405,plain,
( identity = sk_c8
| multiply(sk_c9,sk_c4) = identity ),
inference(copy,[status(thm)],[c_13875]) ).
cnf(c_13876,plain,
( multiply(inverse(sk_c9),identity) = sk_c4
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_5405,c_56]) ).
cnf(c_5409,plain,
( inverse(sk_c9) = sk_c4
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_3255,c_13876]) ).
cnf(c_5412,plain,
( multiply(sk_c4,sk_c9) = identity
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_5409,c_2]) ).
cnf(c_13877,plain,
( sk_c4 = sk_c6
| identity = sk_c8
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_5409,c_5054]) ).
cnf(c_13878,plain,
( sk_c6 = sk_c4
| identity = sk_c8
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_13877]) ).
cnf(c_5449,plain,
( sk_c6 = sk_c4
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_13878]) ).
cnf(c_13879,plain,
( multiply(sk_c1,sk_c9) = sk_c8
| sk_c6 = sk_c4
| sk_c6 = sk_c4 ),
inference(paramod,[status(thm)],[c_5449,c_4789]) ).
cnf(c_5544,plain,
( multiply(sk_c1,sk_c9) = sk_c8
| sk_c6 = sk_c4 ),
inference(copy,[status(thm)],[c_13879]) ).
cnf(c_13880,plain,
( identity = sk_c8
| multiply(sk_c2,sk_c3) = sk_c8
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_5412,c_22]) ).
cnf(c_5697,plain,
( multiply(sk_c2,sk_c3) = sk_c8
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_13880]) ).
cnf(c_13881,plain,
( multiply(sk_c3,sk_c2) = identity
| identity = sk_c8
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_5412,c_87]) ).
cnf(c_5701,plain,
( multiply(sk_c3,sk_c2) = identity
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_13881]) ).
cnf(c_6301,plain,
( sk_c6 = sk_c4
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| sk_c7 != sk_c8
| inverse(sk_c8) != identity
| multiply(sk_c1,sk_c8) != sk_c9
| inverse(sk_c1) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(resolve,[status(thm)],[c_3371,c_5544]) ).
cnf(c_13882,plain,
( multiply(inverse(sk_c3),identity) = sk_c2
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_5701,c_56]) ).
cnf(c_7127,plain,
( inverse(sk_c3) = sk_c2
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_3255,c_13882]) ).
cnf(c_7379,plain,
( multiply(sk_c2,sk_c3) = identity
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_7127,c_2]) ).
cnf(c_13883,plain,
( identity = sk_c8
| identity = sk_c8
| identity = sk_c8 ),
inference(paramod,[status(thm)],[c_7379,c_5697]) ).
cnf(c_13884,plain,
( identity = sk_c8
| identity = sk_c8 ),
inference(copy,[status(thm)],[c_13883]) ).
cnf(c_8920,plain,
identity = sk_c8,
inference(copy,[status(thm)],[c_13884]) ).
cnf(c_10265,plain,
( sk_c6 = sk_c4
| inverse(A) != sk_c8
| multiply(A,sk_c8) != sk_c7
| sk_c7 != sk_c8
| inverse(sk_c8) != sk_c8
| multiply(sk_c1,sk_c8) != sk_c9
| inverse(sk_c1) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_8920,c_6301]) ).
cnf(c_13885,plain,
( sk_c7 != sk_c8
| inverse(inverse(sk_c9)) != sk_c9
| multiply(sk_c8,sk_c7) != sk_c8
| sk_c8 != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(paramod,[status(thm)],[c_8920,c_4130]) ).
cnf(c_11286,plain,
( sk_c7 != sk_c8
| inverse(inverse(sk_c9)) != sk_c9
| multiply(sk_c8,sk_c7) != sk_c8
| multiply(A,sk_c8) != sk_c9
| inverse(A) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(copy,[status(thm)],[c_13885]) ).
cnf(c_13886,plain,
inverse(sk_c8) = identity,
inference(paramod,[status(thm)],[c_8920,c_3373]) ).
cnf(c_11783,plain,
inverse(sk_c8) = sk_c8,
inference(paramod,[status(thm)],[c_8920,c_13886]) ).
cnf(c_11804,plain,
multiply(A,sk_c8) = A,
inference(paramod,[status(thm)],[c_8920,c_3255]) ).
cnf(c_13887,plain,
( multiply(sk_c7,sk_c8) = identity
| multiply(sk_c8,sk_c5) = sk_c8 ),
inference(paramod,[status(thm)],[c_8920,c_1243]) ).
cnf(c_13888,plain,
( sk_c7 = identity
| multiply(sk_c8,sk_c5) = sk_c8 ),
inference(paramod,[status(thm)],[c_11804,c_13887]) ).
cnf(c_12282,plain,
( sk_c7 = sk_c8
| multiply(sk_c8,sk_c5) = sk_c8 ),
inference(paramod,[status(thm)],[c_8920,c_13888]) ).
cnf(c_13889,plain,
( multiply(sk_c7,sk_c8) = identity
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_11804,c_59]) ).
cnf(c_13890,plain,
( sk_c7 = identity
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_11804,c_13889]) ).
cnf(c_12366,plain,
( sk_c7 = sk_c8
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_8920,c_13890]) ).
cnf(c_12369,plain,
multiply(sk_c8,A) = A,
inference(paramod,[status(thm)],[c_8920,c_1]) ).
cnf(c_13891,plain,
( sk_c6 = sk_c4
| multiply(sk_c8,sk_c8) != sk_c7
| sk_c7 != sk_c8
| inverse(sk_c8) != sk_c8
| multiply(sk_c1,sk_c8) != sk_c9
| inverse(sk_c1) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_10265]) ).
cnf(c_13892,plain,
( sk_c6 = sk_c4
| multiply(sk_c8,sk_c8) != sk_c7
| sk_c7 != sk_c8
| inverse(sk_c8) != sk_c8
| multiply(sk_c1,sk_c8) != sk_c9
| inverse(sk_c1) != sk_c9
| sk_c8 != sk_c7 ),
inference(paramod,[status(thm)],[c_11783,c_13891]) ).
cnf(c_13893,plain,
( sk_c6 = sk_c4
| multiply(sk_c8,sk_c8) != sk_c7
| sk_c7 != sk_c8
| inverse(sk_c8) != sk_c8
| sk_c1 != sk_c9
| inverse(sk_c1) != sk_c9
| sk_c8 != sk_c7 ),
inference(paramod,[status(thm)],[c_11804,c_13892]) ).
cnf(c_13894,plain,
( sk_c6 = sk_c4
| multiply(sk_c8,sk_c8) != sk_c7
| sk_c7 != sk_c8
| sk_c8 != sk_c8
| sk_c1 != sk_c9
| inverse(sk_c1) != sk_c9
| sk_c8 != sk_c7 ),
inference(paramod,[status(thm)],[c_11783,c_13893]) ).
cnf(c_13895,plain,
( sk_c6 = sk_c4
| sk_c8 != sk_c7
| sk_c7 != sk_c8
| sk_c8 != sk_c8
| sk_c1 != sk_c9
| inverse(sk_c1) != sk_c9
| sk_c8 != sk_c7 ),
inference(paramod,[status(thm)],[c_11804,c_13894]) ).
cnf(c_13896,plain,
( sk_c6 = sk_c4
| sk_c8 != sk_c7
| sk_c7 != sk_c8
| sk_c8 != sk_c8
| sk_c1 != sk_c9
| inverse(sk_c1) != sk_c9
| sk_c7 != sk_c8 ),
inference(copy,[status(thm)],[c_13895]) ).
cnf(c_13897,plain,
( sk_c6 = sk_c4
| sk_c7 != sk_c8
| sk_c7 != sk_c8
| sk_c8 != sk_c8
| sk_c1 != sk_c9
| inverse(sk_c1) != sk_c9
| sk_c7 != sk_c8 ),
inference(copy,[status(thm)],[c_13896]) ).
cnf(c_13898,plain,
( sk_c6 = sk_c4
| sk_c7 != sk_c8
| sk_c7 != sk_c8
| sk_c1 != sk_c9
| inverse(sk_c1) != sk_c9
| sk_c7 != sk_c8 ),
inference(copy,[status(thm)],[c_13897]) ).
cnf(c_13899,plain,
( sk_c6 = sk_c4
| sk_c7 != sk_c8
| sk_c1 != sk_c9
| inverse(sk_c1) != sk_c9
| sk_c7 != sk_c8 ),
inference(copy,[status(thm)],[c_13898]) ).
cnf(c_12495,plain,
( sk_c6 = sk_c4
| sk_c1 != sk_c9
| inverse(sk_c1) != sk_c9
| sk_c7 != sk_c8 ),
inference(copy,[status(thm)],[c_13899]) ).
cnf(c_13900,plain,
( sk_c7 != sk_c8
| multiply(sk_c8,sk_c7) != sk_c8
| multiply(inverse(sk_c9),sk_c8) != sk_c9
| inverse(inverse(sk_c9)) != sk_c9
| inverse(sk_c8) != sk_c7 ),
inference(factor,[status(thm)],[c_11286]) ).
cnf(c_13901,plain,
( sk_c7 != sk_c8
| multiply(sk_c8,sk_c7) != sk_c8
| multiply(inverse(sk_c9),sk_c8) != sk_c9
| inverse(inverse(sk_c9)) != sk_c9
| sk_c8 != sk_c7 ),
inference(paramod,[status(thm)],[c_11783,c_13900]) ).
cnf(c_13902,plain,
( sk_c7 != sk_c8
| multiply(sk_c8,sk_c7) != sk_c8
| inverse(sk_c9) != sk_c9
| inverse(inverse(sk_c9)) != sk_c9
| sk_c8 != sk_c7 ),
inference(paramod,[status(thm)],[c_11804,c_13901]) ).
cnf(c_13903,plain,
( sk_c7 != sk_c8
| sk_c7 != sk_c8
| inverse(sk_c9) != sk_c9
| inverse(inverse(sk_c9)) != sk_c9
| sk_c8 != sk_c7 ),
inference(paramod,[status(thm)],[c_12369,c_13902]) ).
cnf(c_13904,plain,
( sk_c7 != sk_c8
| sk_c7 != sk_c8
| inverse(sk_c9) != sk_c9
| inverse(inverse(sk_c9)) != sk_c9
| sk_c7 != sk_c8 ),
inference(copy,[status(thm)],[c_13903]) ).
cnf(c_13905,plain,
( sk_c7 != sk_c8
| inverse(sk_c9) != sk_c9
| inverse(inverse(sk_c9)) != sk_c9
| sk_c7 != sk_c8 ),
inference(copy,[status(thm)],[c_13904]) ).
cnf(c_12553,plain,
( inverse(sk_c9) != sk_c9
| inverse(inverse(sk_c9)) != sk_c9
| sk_c7 != sk_c8 ),
inference(copy,[status(thm)],[c_13905]) ).
cnf(c_13906,plain,
( multiply(sk_c6,sk_c8) = sk_c9
| sk_c1 = sk_c9 ),
inference(paramod,[status(thm)],[c_11804,c_21]) ).
cnf(c_12907,plain,
( sk_c6 = sk_c9
| sk_c1 = sk_c9 ),
inference(paramod,[status(thm)],[c_11804,c_13906]) ).
cnf(c_12908,plain,
( inverse(sk_c6) = sk_c9
| sk_c1 = sk_c9 ),
inference(paramod,[status(thm)],[c_11804,c_20]) ).
cnf(c_12912,plain,
( sk_c6 = sk_c9
| inverse(sk_c1) = sk_c9 ),
inference(paramod,[status(thm)],[c_11804,c_15]) ).
cnf(c_12924,plain,
( sk_c7 = sk_c8
| sk_c5 = sk_c8 ),
inference(paramod,[status(thm)],[c_12369,c_12282]) ).
cnf(c_13907,plain,
( sk_c7 = sk_c8
| sk_c8 = sk_c7
| sk_c7 = sk_c8 ),
inference(paramod,[status(thm)],[c_12924,c_12366]) ).
cnf(c_13908,plain,
( sk_c7 = sk_c8
| sk_c7 = sk_c8
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_13907]) ).
cnf(c_13909,plain,
( sk_c7 = sk_c8
| sk_c7 = sk_c8 ),
inference(copy,[status(thm)],[c_13908]) ).
cnf(c_13000,plain,
sk_c7 = sk_c8,
inference(copy,[status(thm)],[c_13909]) ).
cnf(c_13910,plain,
( inverse(sk_c9) != sk_c9
| inverse(inverse(sk_c9)) != sk_c9
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_13000,c_12553]) ).
cnf(c_13175,plain,
( inverse(sk_c9) != sk_c9
| inverse(inverse(sk_c9)) != sk_c9 ),
inference(copy,[status(thm)],[c_13910]) ).
cnf(c_13911,plain,
( sk_c6 = sk_c4
| sk_c1 != sk_c9
| inverse(sk_c1) != sk_c9
| sk_c8 != sk_c8 ),
inference(paramod,[status(thm)],[c_13000,c_12495]) ).
cnf(c_13200,plain,
( sk_c6 = sk_c4
| sk_c1 != sk_c9
| inverse(sk_c1) != sk_c9 ),
inference(copy,[status(thm)],[c_13911]) ).
cnf(c_13912,plain,
( inverse(sk_c9) = sk_c9
| sk_c1 = sk_c9
| sk_c1 = sk_c9 ),
inference(paramod,[status(thm)],[c_12907,c_12908]) ).
cnf(c_13285,plain,
( inverse(sk_c9) = sk_c9
| sk_c1 = sk_c9 ),
inference(copy,[status(thm)],[c_13912]) ).
cnf(c_13913,plain,
( inverse(sk_c9) != sk_c9
| inverse(sk_c9) != sk_c9
| sk_c1 = sk_c9 ),
inference(paramod,[status(thm)],[c_13285,c_13175]) ).
cnf(c_13442,plain,
( inverse(sk_c9) != sk_c9
| sk_c1 = sk_c9 ),
inference(copy,[status(thm)],[c_13913]) ).
cnf(c_13914,plain,
( sk_c1 = sk_c9
| sk_c1 = sk_c9 ),
inference(resolve,[status(thm)],[c_13442,c_13285]) ).
cnf(c_13453,plain,
sk_c1 = sk_c9,
inference(copy,[status(thm)],[c_13914]) ).
cnf(c_13915,plain,
( sk_c6 = sk_c4
| sk_c1 != sk_c9
| inverse(sk_c9) != sk_c9 ),
inference(paramod,[status(thm)],[c_13453,c_13200]) ).
cnf(c_13916,plain,
( sk_c6 = sk_c4
| sk_c9 != sk_c9
| inverse(sk_c9) != sk_c9 ),
inference(paramod,[status(thm)],[c_13453,c_13915]) ).
cnf(c_13519,plain,
( sk_c6 = sk_c4
| inverse(sk_c9) != sk_c9 ),
inference(copy,[status(thm)],[c_13916]) ).
cnf(c_13560,plain,
( sk_c6 = sk_c9
| inverse(sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_13453,c_12912]) ).
cnf(c_13584,plain,
( inverse(sk_c9) = sk_c9
| sk_c6 = sk_c4 ),
inference(paramod,[status(thm)],[c_13453,c_4831]) ).
cnf(c_13592,plain,
( inverse(sk_c4) = sk_c9
| inverse(sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_13453,c_11]) ).
cnf(c_13917,plain,
( inverse(sk_c9) != sk_c9
| inverse(sk_c9) != sk_c9
| sk_c6 = sk_c9 ),
inference(paramod,[status(thm)],[c_13560,c_13175]) ).
cnf(c_13760,plain,
( inverse(sk_c9) != sk_c9
| sk_c6 = sk_c9 ),
inference(copy,[status(thm)],[c_13917]) ).
cnf(c_13918,plain,
( sk_c6 = sk_c4
| sk_c6 = sk_c4 ),
inference(resolve,[status(thm)],[c_13584,c_13519]) ).
cnf(c_13762,plain,
sk_c6 = sk_c4,
inference(copy,[status(thm)],[c_13918]) ).
cnf(c_13763,plain,
( inverse(sk_c9) != sk_c9
| sk_c4 = sk_c9 ),
inference(paramod,[status(thm)],[c_13762,c_13760]) ).
cnf(c_13783,plain,
( sk_c4 = sk_c9
| inverse(sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_13762,c_13560]) ).
cnf(c_13919,plain,
( sk_c4 = sk_c9
| sk_c4 = sk_c9 ),
inference(resolve,[status(thm)],[c_13783,c_13763]) ).
cnf(c_13801,plain,
sk_c4 = sk_c9,
inference(copy,[status(thm)],[c_13919]) ).
cnf(c_13920,plain,
( inverse(sk_c9) = sk_c9
| inverse(sk_c9) = sk_c9 ),
inference(paramod,[status(thm)],[c_13801,c_13592]) ).
cnf(c_13849,plain,
inverse(sk_c9) = sk_c9,
inference(copy,[status(thm)],[c_13920]) ).
cnf(c_13921,plain,
( inverse(sk_c9) != sk_c9
| inverse(sk_c9) != sk_c9 ),
inference(paramod,[status(thm)],[c_13849,c_13175]) ).
cnf(c_13922,plain,
( inverse(sk_c9) != sk_c9
| sk_c9 != sk_c9 ),
inference(paramod,[status(thm)],[c_13849,c_13921]) ).
cnf(c_13923,plain,
( sk_c9 != sk_c9
| sk_c9 != sk_c9 ),
inference(paramod,[status(thm)],[c_13849,c_13922]) ).
cnf(c_13924,plain,
sk_c9 != sk_c9,
inference(copy,[status(thm)],[c_13923]) ).
cnf(c_13860,plain,
$false,
inference(copy,[status(thm)],[c_13924]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP390-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 : n003.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.44 % DateTime : Fri Sep 25 14:52:08 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.44 % Process 449824 was started by sandbox2 on n003,
% 0.18/0.44 % Fri Sep 25 14:52:08 2026
% 0.18/0.44 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.18/0.45
% 0.18/0.45 % From the command line: assign(max_seconds, 300).
% 117.74/15.39
% 117.74/15.39 % SZS status Unsatisfiable for theBenchmark
% 117.74/15.39
% 117.74/15.39 % Proof 1 at 5.92 (+ 0.92) seconds.
% 117.74/15.39 % Length of proof is 101.
% 117.74/15.39 % Level of proof is 25.
% 117.74/15.39 % Maximum clause weight is 64.000.
% 117.74/15.39 % Given clauses 308.
% 117.74/15.39
% 117.74/15.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------