%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP276-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 : n016.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 12.36s 7.06s
% Output : CNFRefutation 12.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 55
% Number of leaves : 14
% Syntax : Number of formulae : 154 ( 29 unt; 0 def)
% Number of atoms : 444 ( 443 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 522 ( 232 ~; 290 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 77 ( 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_4,axiom,
( inverse(sk_c7) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_4) ).
cnf(c_7,plain,
( inverse(sk_c7) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_4]) ).
fof(prove_this_9,axiom,
( inverse(sk_c3) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_9) ).
cnf(c_12,plain,
( inverse(sk_c3) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_9]) ).
fof(prove_this_10,axiom,
( inverse(sk_c7) = sk_c5
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_10) ).
cnf(c_13,plain,
( inverse(sk_c7) = sk_c5
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_10]) ).
fof(prove_this_14,axiom,
( multiply(sk_c3,sk_c7) = sk_c6
| multiply(sk_c7,sk_c5) = sk_c6 ),
file('theBenchmark.p',prove_this_14) ).
cnf(c_17,plain,
( multiply(sk_c3,sk_c7) = sk_c6
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_14]) ).
fof(prove_this_15,axiom,
( inverse(sk_c3) = sk_c7
| multiply(sk_c7,sk_c5) = sk_c6 ),
file('theBenchmark.p',prove_this_15) ).
cnf(c_18,plain,
( inverse(sk_c3) = sk_c7
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_15]) ).
fof(prove_this_16,axiom,
( inverse(sk_c7) = sk_c5
| multiply(sk_c7,sk_c5) = sk_c6 ),
file('theBenchmark.p',prove_this_16) ).
cnf(c_19,plain,
( inverse(sk_c7) = sk_c5
| multiply(sk_c7,sk_c5) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_16]) ).
fof(prove_this_19,axiom,
( multiply(sk_c6,sk_c5) = sk_c7
| inverse(sk_c2) = sk_c7 ),
file('theBenchmark.p',prove_this_19) ).
cnf(c_22,plain,
( multiply(sk_c6,sk_c5) = sk_c7
| inverse(sk_c2) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_19]) ).
fof(prove_this_21,axiom,
( inverse(sk_c3) = sk_c7
| inverse(sk_c2) = sk_c7 ),
file('theBenchmark.p',prove_this_21) ).
cnf(c_24,plain,
( inverse(sk_c3) = sk_c7
| inverse(sk_c2) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_21]) ).
fof(prove_this_22,axiom,
( inverse(sk_c7) = sk_c5
| inverse(sk_c2) = sk_c7 ),
file('theBenchmark.p',prove_this_22) ).
cnf(c_25,plain,
( inverse(sk_c7) = sk_c5
| inverse(sk_c2) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_22]) ).
fof(prove_this_25,axiom,
( multiply(sk_c6,sk_c5) = sk_c7
| multiply(sk_c2,sk_c6) = sk_c7 ),
file('theBenchmark.p',prove_this_25) ).
cnf(c_28,plain,
( multiply(sk_c6,sk_c5) = sk_c7
| multiply(sk_c2,sk_c6) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_25]) ).
fof(prove_this_31,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( inverse(VAR_3) != sk_c5
| multiply(VAR_3,sk_c5) != sk_c6
| inverse(sk_c7) != sk_c5
| inverse(VAR_2) != sk_c7
| multiply(VAR_2,sk_c7) != sk_c6
| multiply(sk_c6,sk_c5) != sk_c7
| multiply(VAR_1,sk_c6) != sk_c7
| inverse(VAR_1) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(VAR_0) != sk_c7
| multiply(VAR_0,sk_c7) != sk_c6 ),
file('theBenchmark.p',prove_this_31) ).
cnf(c_34,plain,
( inverse(D) != sk_c5
| multiply(D,sk_c5) != sk_c6
| inverse(sk_c7) != sk_c5
| inverse(C) != sk_c7
| multiply(C,sk_c7) != sk_c6
| multiply(sk_c6,sk_c5) != sk_c7
| multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6 ),
inference(clausify,[status(thm)],[prove_this_31]) ).
cnf(c_1731,plain,
( inverse(C) != sk_c5
| multiply(C,sk_c5) != sk_c6
| inverse(sk_c7) != sk_c5
| inverse(A) != sk_c7
| multiply(sk_c6,sk_c5) != sk_c7
| multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6 ),
inference(factor,[status(thm)],[c_34]) ).
cnf(c_35,plain,
( inverse(C) != sk_c5
| multiply(C,sk_c5) != sk_c6
| inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6 ),
inference(copy,[status(thm)],[c_1731]) ).
cnf(c_1732,plain,
( inverse(sk_c7) != sk_c5
| inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6 ),
inference(factor,[status(thm)],[c_35]) ).
cnf(c_38,plain,
( inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6 ),
inference(copy,[status(thm)],[c_1732]) ).
cnf(c_1733,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_1734,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_1733]) ).
cnf(c_40,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_1734]) ).
cnf(c_57,plain,
( multiply(sk_c7,sk_c3) = identity
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_12,c_2]) ).
cnf(c_58,plain,
( multiply(sk_c7,sk_c1) = identity
| inverse(sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_13,c_2]) ).
cnf(c_78,plain,
( multiply(sk_c7,sk_c3) = identity
| inverse(sk_c2) = sk_c7 ),
inference(paramod,[status(thm)],[c_24,c_2]) ).
cnf(c_79,plain,
( multiply(sk_c7,sk_c2) = identity
| inverse(sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_25,c_2]) ).
cnf(c_109,plain,
( inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| multiply(C,sk_c6) != sk_c7
| inverse(C) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(multiply(A,B)) != sk_c7
| multiply(A,multiply(B,sk_c7)) != sk_c6 ),
inference(paramod,[status(thm)],[c_3,c_38]) ).
cnf(c_126,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_40]) ).
cnf(c_143,plain,
( multiply(inverse(sk_c7),sk_c6) = sk_c5
| inverse(sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_19,c_40]) ).
cnf(c_146,plain,
( multiply(inverse(sk_c6),sk_c7) = sk_c5
| inverse(sk_c2) = sk_c7 ),
inference(paramod,[status(thm)],[c_22,c_40]) ).
cnf(c_158,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_40,c_40]) ).
cnf(c_159,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_158,c_126]) ).
cnf(c_170,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_159,c_2]) ).
cnf(c_1735,plain,
( multiply(inverse(sk_c7),identity) = sk_c3
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_57,c_40]) ).
cnf(c_175,plain,
( inverse(sk_c7) = sk_c3
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_159,c_1735]) ).
cnf(c_176,plain,
( multiply(sk_c7,sk_c1) = identity
| inverse(sk_c7) = sk_c3 ),
inference(paramod,[status(thm)],[c_175,c_2]) ).
cnf(c_1736,plain,
( multiply(inverse(sk_c7),identity) = sk_c1
| inverse(sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_58,c_40]) ).
cnf(c_179,plain,
( inverse(sk_c7) = sk_c1
| inverse(sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_159,c_1736]) ).
cnf(c_180,plain,
( multiply(sk_c1,sk_c7) = identity
| inverse(sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_179,c_2]) ).
cnf(c_1737,plain,
( inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(multiply(A,inverse(sk_c7))) != sk_c7
| multiply(A,identity) != sk_c6 ),
inference(paramod,[status(thm)],[c_2,c_109]) ).
cnf(c_1738,plain,
( inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(multiply(A,inverse(sk_c7))) != sk_c7
| A != sk_c6 ),
inference(paramod,[status(thm)],[c_159,c_1737]) ).
cnf(c_203,plain,
( inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| multiply(B,sk_c6) != sk_c7
| inverse(B) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(multiply(A,inverse(sk_c7))) != sk_c7
| sk_c6 != A ),
inference(copy,[status(thm)],[c_1738]) ).
cnf(c_1739,plain,
( multiply(inverse(sk_c7),identity) = sk_c3
| inverse(sk_c2) = sk_c7 ),
inference(paramod,[status(thm)],[c_78,c_40]) ).
cnf(c_227,plain,
( inverse(sk_c7) = sk_c3
| inverse(sk_c2) = sk_c7 ),
inference(paramod,[status(thm)],[c_159,c_1739]) ).
cnf(c_228,plain,
( multiply(sk_c7,sk_c2) = identity
| inverse(sk_c7) = sk_c3 ),
inference(paramod,[status(thm)],[c_227,c_2]) ).
cnf(c_1740,plain,
( multiply(inverse(sk_c7),identity) = sk_c2
| inverse(sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_79,c_40]) ).
cnf(c_231,plain,
( inverse(sk_c7) = sk_c2
| inverse(sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_159,c_1740]) ).
cnf(c_1741,plain,
( sk_c2 = sk_c1
| inverse(sk_c7) = sk_c5
| inverse(sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_231,c_179]) ).
cnf(c_235,plain,
( sk_c2 = sk_c1
| inverse(sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_1741]) ).
cnf(c_249,plain,
( inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| multiply(B,multiply(C,sk_c6)) != sk_c7
| inverse(multiply(B,C)) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(multiply(A,inverse(sk_c7))) != sk_c7
| sk_c6 != A ),
inference(paramod,[status(thm)],[c_3,c_203]) ).
cnf(c_278,plain,
( multiply(sk_c5,sk_c7) = identity
| sk_c2 = sk_c1 ),
inference(paramod,[status(thm)],[c_235,c_2]) ).
cnf(c_1742,plain,
( multiply(inverse(sk_c7),identity) = sk_c1
| inverse(sk_c7) = sk_c3 ),
inference(paramod,[status(thm)],[c_176,c_40]) ).
cnf(c_337,plain,
( inverse(sk_c7) = sk_c1
| inverse(sk_c7) = sk_c3 ),
inference(paramod,[status(thm)],[c_159,c_1742]) ).
cnf(c_1743,plain,
( inverse(sk_c7) = sk_c5
| identity = sk_c6
| inverse(sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_180,c_7]) ).
cnf(c_351,plain,
( identity = sk_c6
| inverse(sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_1743]) ).
cnf(c_353,plain,
( multiply(sk_c5,sk_c7) = identity
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_351,c_2]) ).
cnf(c_1744,plain,
( multiply(inverse(sk_c5),identity) = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_353,c_40]) ).
cnf(c_361,plain,
( inverse(sk_c5) = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_159,c_1744]) ).
cnf(c_362,plain,
( multiply(sk_c7,sk_c5) = identity
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_361,c_2]) ).
cnf(c_1745,plain,
( inverse(sk_c3) = sk_c7
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_362,c_18]) ).
cnf(c_388,plain,
( inverse(sk_c3) = sk_c7
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_1745]) ).
cnf(c_392,plain,
( multiply(sk_c7,sk_c3) = identity
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_388,c_2]) ).
cnf(c_1746,plain,
( multiply(inverse(sk_c7),identity) = sk_c3
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_392,c_40]) ).
cnf(c_397,plain,
( inverse(sk_c7) = sk_c3
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_159,c_1746]) ).
cnf(c_400,plain,
( multiply(sk_c3,sk_c7) = identity
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_397,c_2]) ).
cnf(c_1747,plain,
( inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| multiply(B,identity) != sk_c7
| inverse(multiply(B,inverse(sk_c6))) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(multiply(A,inverse(sk_c7))) != sk_c7
| sk_c6 != A ),
inference(paramod,[status(thm)],[c_2,c_249]) ).
cnf(c_1748,plain,
( inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| B != sk_c7
| inverse(multiply(B,inverse(sk_c6))) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(multiply(A,inverse(sk_c7))) != sk_c7
| sk_c6 != A ),
inference(paramod,[status(thm)],[c_159,c_1747]) ).
cnf(c_535,plain,
( inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| sk_c7 != B
| inverse(multiply(B,inverse(sk_c6))) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(multiply(A,inverse(sk_c7))) != sk_c7
| sk_c6 != A ),
inference(copy,[status(thm)],[c_1748]) ).
cnf(c_1749,plain,
( inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| sk_c7 != C
| inverse(multiply(C,inverse(sk_c6))) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(multiply(A,multiply(B,inverse(sk_c7)))) != sk_c7
| sk_c6 != multiply(A,B) ),
inference(paramod,[status(thm)],[c_3,c_535]) ).
cnf(c_550,plain,
( inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| sk_c7 != C
| inverse(multiply(C,inverse(sk_c6))) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(multiply(A,multiply(B,inverse(sk_c7)))) != sk_c7
| multiply(A,B) != sk_c6 ),
inference(copy,[status(thm)],[c_1749]) ).
cnf(c_559,plain,
( inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| sk_c7 != A
| inverse(multiply(A,inverse(sk_c6))) != sk_c7
| inverse(multiply(sk_c7,multiply(sk_c5,inverse(sk_c7)))) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(factor,[status(thm)],[c_550]) ).
cnf(c_1750,plain,
( identity = sk_c6
| multiply(sk_c7,sk_c5) = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_400,c_17]) ).
cnf(c_591,plain,
( multiply(sk_c7,sk_c5) = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_1750]) ).
cnf(c_1751,plain,
( inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| sk_c7 != multiply(A,B)
| inverse(multiply(A,multiply(B,inverse(sk_c6)))) != sk_c7
| inverse(multiply(sk_c7,multiply(sk_c5,inverse(sk_c7)))) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(paramod,[status(thm)],[c_3,c_559]) ).
cnf(c_935,plain,
( inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| multiply(A,B) != sk_c7
| inverse(multiply(A,multiply(B,inverse(sk_c6)))) != sk_c7
| inverse(multiply(sk_c7,multiply(sk_c5,inverse(sk_c7)))) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(copy,[status(thm)],[c_1751]) ).
cnf(c_1752,plain,
( sk_c6 = identity
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_591,c_362]) ).
cnf(c_1753,plain,
( identity = sk_c6
| identity = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_1752]) ).
cnf(c_1754,plain,
( identity = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_1753]) ).
cnf(c_981,plain,
identity = sk_c6,
inference(copy,[status(thm)],[c_1754]) ).
cnf(c_1201,plain,
( multiply(sk_c5,sk_c7) = sk_c6
| sk_c2 = sk_c1 ),
inference(paramod,[status(thm)],[c_981,c_278]) ).
cnf(c_1217,plain,
( multiply(sk_c7,sk_c2) = sk_c6
| inverse(sk_c7) = sk_c3 ),
inference(paramod,[status(thm)],[c_981,c_228]) ).
cnf(c_1755,plain,
inverse(sk_c6) = identity,
inference(paramod,[status(thm)],[c_981,c_170]) ).
cnf(c_1238,plain,
inverse(sk_c6) = sk_c6,
inference(paramod,[status(thm)],[c_981,c_1755]) ).
cnf(c_1246,plain,
multiply(A,sk_c6) = A,
inference(paramod,[status(thm)],[c_981,c_159]) ).
cnf(c_1256,plain,
multiply(sk_c6,A) = A,
inference(paramod,[status(thm)],[c_981,c_1]) ).
cnf(c_1756,plain,
( inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| multiply(A,B) != sk_c7
| inverse(multiply(A,multiply(B,sk_c6))) != sk_c7
| inverse(multiply(sk_c7,multiply(sk_c5,inverse(sk_c7)))) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(paramod,[status(thm)],[c_1238,c_935]) ).
cnf(c_1757,plain,
( inverse(sk_c7) != sk_c5
| multiply(sk_c6,sk_c5) != sk_c7
| multiply(A,B) != sk_c7
| inverse(multiply(A,B)) != sk_c7
| inverse(multiply(sk_c7,multiply(sk_c5,inverse(sk_c7)))) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(paramod,[status(thm)],[c_1246,c_1756]) ).
cnf(c_1316,plain,
( inverse(sk_c7) != sk_c5
| sk_c5 != sk_c7
| multiply(A,B) != sk_c7
| inverse(multiply(A,B)) != sk_c7
| inverse(multiply(sk_c7,multiply(sk_c5,inverse(sk_c7)))) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(paramod,[status(thm)],[c_1256,c_1757]) ).
cnf(c_1758,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c2) = sk_c7 ),
inference(paramod,[status(thm)],[c_1238,c_146]) ).
cnf(c_1759,plain,
( sk_c7 = sk_c5
| inverse(sk_c2) = sk_c7 ),
inference(paramod,[status(thm)],[c_1256,c_1758]) ).
cnf(c_1362,plain,
( sk_c5 = sk_c7
| inverse(sk_c2) = sk_c7 ),
inference(copy,[status(thm)],[c_1759]) ).
cnf(c_1760,plain,
( inverse(sk_c7) = sk_c5
| inverse(sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_1246,c_143]) ).
cnf(c_1416,plain,
inverse(sk_c7) = sk_c5,
inference(copy,[status(thm)],[c_1760]) ).
cnf(c_1761,plain,
( multiply(sk_c6,sk_c5) = sk_c7
| sk_c2 = sk_c7 ),
inference(paramod,[status(thm)],[c_1246,c_28]) ).
cnf(c_1460,plain,
( sk_c5 = sk_c7
| sk_c2 = sk_c7 ),
inference(paramod,[status(thm)],[c_1256,c_1761]) ).
cnf(c_1762,plain,
( inverse(sk_c7) != sk_c5
| sk_c5 != sk_c7
| multiply(sk_c7,multiply(sk_c5,inverse(sk_c7))) != sk_c7
| inverse(multiply(sk_c7,multiply(sk_c5,inverse(sk_c7)))) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(factor,[status(thm)],[c_1316]) ).
cnf(c_1763,plain,
( inverse(sk_c7) != sk_c5
| sk_c5 != sk_c7
| multiply(sk_c7,multiply(sk_c5,inverse(sk_c7))) != sk_c7
| inverse(multiply(sk_c7,multiply(sk_c5,sk_c5))) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(paramod,[status(thm)],[c_1416,c_1762]) ).
cnf(c_1764,plain,
( inverse(sk_c7) != sk_c5
| sk_c5 != sk_c7
| multiply(sk_c7,multiply(sk_c5,sk_c5)) != sk_c7
| inverse(multiply(sk_c7,multiply(sk_c5,sk_c5))) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(paramod,[status(thm)],[c_1416,c_1763]) ).
cnf(c_1765,plain,
( sk_c5 != sk_c5
| sk_c5 != sk_c7
| multiply(sk_c7,multiply(sk_c5,sk_c5)) != sk_c7
| inverse(multiply(sk_c7,multiply(sk_c5,sk_c5))) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(paramod,[status(thm)],[c_1416,c_1764]) ).
cnf(c_1542,plain,
( sk_c5 != sk_c7
| multiply(sk_c7,multiply(sk_c5,sk_c5)) != sk_c7
| inverse(multiply(sk_c7,multiply(sk_c5,sk_c5))) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6 ),
inference(copy,[status(thm)],[c_1765]) ).
cnf(c_1766,plain,
( multiply(sk_c7,sk_c2) = sk_c6
| sk_c5 = sk_c3 ),
inference(paramod,[status(thm)],[c_1416,c_1217]) ).
cnf(c_1593,plain,
( multiply(sk_c7,sk_c2) = sk_c6
| sk_c3 = sk_c5 ),
inference(copy,[status(thm)],[c_1766]) ).
cnf(c_1767,plain,
( inverse(sk_c7) = sk_c1
| sk_c5 = sk_c3 ),
inference(paramod,[status(thm)],[c_1416,c_337]) ).
cnf(c_1768,plain,
( sk_c5 = sk_c1
| sk_c5 = sk_c3 ),
inference(paramod,[status(thm)],[c_1416,c_1767]) ).
cnf(c_1769,plain,
( sk_c5 = sk_c1
| sk_c3 = sk_c5 ),
inference(copy,[status(thm)],[c_1768]) ).
cnf(c_1597,plain,
( sk_c1 = sk_c5
| sk_c3 = sk_c5 ),
inference(copy,[status(thm)],[c_1769]) ).
cnf(c_1607,plain,
( multiply(sk_c5,sk_c7) = sk_c6
| multiply(sk_c7,sk_c5) = sk_c6
| sk_c1 = sk_c5 ),
inference(paramod,[status(thm)],[c_1597,c_17]) ).
cnf(c_1610,plain,
multiply(sk_c5,multiply(sk_c7,A)) = A,
inference(paramod,[status(thm)],[c_1416,c_40]) ).
cnf(c_1770,plain,
( sk_c5 = sk_c7
| inverse(sk_c7) = sk_c7
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_1460,c_1362]) ).
cnf(c_1771,plain,
( sk_c5 = sk_c7
| sk_c5 = sk_c7
| sk_c5 = sk_c7 ),
inference(paramod,[status(thm)],[c_1416,c_1770]) ).
cnf(c_1772,plain,
( sk_c5 = sk_c7
| sk_c5 = sk_c7 ),
inference(copy,[status(thm)],[c_1771]) ).
cnf(c_1646,plain,
sk_c5 = sk_c7,
inference(copy,[status(thm)],[c_1772]) ).
cnf(c_1659,plain,
multiply(sk_c7,multiply(sk_c7,A)) = A,
inference(paramod,[status(thm)],[c_1646,c_1610]) ).
cnf(c_1773,plain,
( multiply(sk_c5,sk_c7) = sk_c6
| multiply(sk_c7,sk_c5) = sk_c6
| sk_c1 = sk_c7 ),
inference(paramod,[status(thm)],[c_1646,c_1607]) ).
cnf(c_1774,plain,
( multiply(sk_c5,sk_c7) = sk_c6
| multiply(sk_c7,sk_c7) = sk_c6
| sk_c1 = sk_c7 ),
inference(paramod,[status(thm)],[c_1646,c_1773]) ).
cnf(c_1775,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| multiply(sk_c7,sk_c7) = sk_c6
| sk_c1 = sk_c7 ),
inference(paramod,[status(thm)],[c_1646,c_1774]) ).
cnf(c_1661,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| sk_c1 = sk_c7 ),
inference(copy,[status(thm)],[c_1775]) ).
cnf(c_1670,plain,
( multiply(sk_c7,sk_c2) = sk_c6
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_1646,c_1593]) ).
cnf(c_1776,plain,
( sk_c5 != sk_c7
| multiply(sk_c7,multiply(sk_c5,sk_c5)) != sk_c7
| inverse(multiply(sk_c7,multiply(sk_c5,sk_c5))) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_1646,c_1542]) ).
cnf(c_1777,plain,
( sk_c5 != sk_c7
| multiply(sk_c7,multiply(sk_c5,sk_c5)) != sk_c7
| inverse(multiply(sk_c7,multiply(sk_c7,sk_c5))) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_1646,c_1776]) ).
cnf(c_1778,plain,
( sk_c5 != sk_c7
| multiply(sk_c7,multiply(sk_c5,sk_c5)) != sk_c7
| inverse(multiply(sk_c7,multiply(sk_c7,sk_c7))) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_1646,c_1777]) ).
cnf(c_1779,plain,
( sk_c5 != sk_c7
| multiply(sk_c7,multiply(sk_c5,sk_c5)) != sk_c7
| inverse(sk_c7) != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_1659,c_1778]) ).
cnf(c_1780,plain,
( sk_c5 != sk_c7
| multiply(sk_c7,multiply(sk_c5,sk_c5)) != sk_c7
| sk_c5 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_1416,c_1779]) ).
cnf(c_1781,plain,
( sk_c5 != sk_c7
| multiply(sk_c7,multiply(sk_c5,sk_c5)) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_1646,c_1780]) ).
cnf(c_1782,plain,
( sk_c5 != sk_c7
| multiply(sk_c7,multiply(sk_c7,sk_c5)) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_1646,c_1781]) ).
cnf(c_1783,plain,
( sk_c5 != sk_c7
| multiply(sk_c7,multiply(sk_c7,sk_c7)) != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_1646,c_1782]) ).
cnf(c_1784,plain,
( sk_c5 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_1659,c_1783]) ).
cnf(c_1785,plain,
( sk_c7 != sk_c7
| sk_c7 != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6 ),
inference(paramod,[status(thm)],[c_1646,c_1784]) ).
cnf(c_1786,plain,
( sk_c7 != sk_c7
| sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6 ),
inference(copy,[status(thm)],[c_1785]) ).
cnf(c_1787,plain,
( sk_c7 != sk_c7
| multiply(sk_c7,sk_c7) != sk_c6 ),
inference(copy,[status(thm)],[c_1786]) ).
cnf(c_1697,plain,
multiply(sk_c7,sk_c7) != sk_c6,
inference(copy,[status(thm)],[c_1787]) ).
cnf(c_1788,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| sk_c2 = sk_c1 ),
inference(paramod,[status(thm)],[c_1646,c_1201]) ).
cnf(c_1713,plain,
sk_c2 = sk_c1,
inference(resolve,[status(thm)],[c_1697,c_1788]) ).
cnf(c_1789,plain,
( multiply(sk_c3,sk_c7) = sk_c6
| multiply(sk_c7,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_1646,c_17]) ).
cnf(c_1720,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(resolve,[status(thm)],[c_1697,c_1789]) ).
cnf(c_1721,plain,
sk_c1 = sk_c7,
inference(resolve,[status(thm)],[c_1697,c_1661]) ).
cnf(c_1790,plain,
( multiply(sk_c7,sk_c1) = sk_c6
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_1713,c_1670]) ).
cnf(c_1791,plain,
( multiply(sk_c7,sk_c7) = sk_c6
| sk_c3 = sk_c7 ),
inference(paramod,[status(thm)],[c_1721,c_1790]) ).
cnf(c_1724,plain,
sk_c3 = sk_c7,
inference(resolve,[status(thm)],[c_1697,c_1791]) ).
cnf(c_1792,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(paramod,[status(thm)],[c_1724,c_1720]) ).
cnf(c_1730,plain,
$false,
inference(resolve,[status(thm)],[c_1697,c_1792]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP276-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/5.45 % Computer : n016.cluster.edu
% 0.18/5.45 % Model : x86_64 x86_64
% 0.18/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.45 % Memory : 8046.5625MB
% 0.18/5.45 % OS : Linux 6.8.0-71-generic
% 0.18/5.45 % CPULimit : 300
% 0.18/5.45 % WCLimit : 300
% 0.18/5.45 % DateTime : Fri Sep 25 14:47:20 UTC 2026
% 0.18/5.45 % CPUTime :
% 0.18/5.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/5.45 % Process 2644601 was started by sandbox2 on n016,
% 0.18/5.45 % Fri Sep 25 14:47:20 2026
% 0.18/5.45 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.18/5.46
% 0.18/5.46 % From the command line: assign(max_seconds, 300).
% 12.36/7.06
% 12.36/7.06 % Assigning unary symbol inverse kb_weight 0 and highest precedence (11).
% 12.36/7.06
% 12.36/7.06 % SZS status Unsatisfiable for theBenchmark
% 12.36/7.06
% 12.36/7.06 % Proof 1 at 1.23 (+ 0.34) seconds.
% 12.36/7.06 % Length of proof is 78.
% 12.36/7.06 % Level of proof is 23.
% 12.36/7.06 % Maximum clause weight is 72.000.
% 12.36/7.06 % Given clauses 144.
% 12.36/7.06
% 12.36/7.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------