%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP002-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/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:26:07 AM UTC 2026
% Result : Unsatisfiable 7.51s 2.07s
% Output : CNFRefutation 7.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 16
% Syntax : Number of formulae : 164 ( 97 unt; 0 def)
% Number of atoms : 263 ( 40 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 208 ( 109 ~; 99 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 2 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 271 ( 0 sgn 26 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(left_identity,axiom,
! [VAR_0] : product(identity,VAR_0,VAR_0),
file('theBenchmark.p',left_identity) ).
cnf(c_1,plain,
product(identity,A,A),
inference(clausify,[status(thm)],[left_identity]) ).
fof(right_identity,axiom,
! [VAR_0] : product(VAR_0,identity,VAR_0),
file('theBenchmark.p',right_identity) ).
cnf(c_2,plain,
product(A,identity,A),
inference(clausify,[status(thm)],[right_identity]) ).
fof(left_inverse,axiom,
! [VAR_0] : product(inverse(VAR_0),VAR_0,identity),
file('theBenchmark.p',left_inverse) ).
cnf(c_3,plain,
product(inverse(A),A,identity),
inference(clausify,[status(thm)],[left_inverse]) ).
fof(right_inverse,axiom,
! [VAR_0] : product(VAR_0,inverse(VAR_0),identity),
file('theBenchmark.p',right_inverse) ).
cnf(c_4,plain,
product(A,inverse(A),identity),
inference(clausify,[status(thm)],[right_inverse]) ).
fof(total_function1,axiom,
! [VAR_0,VAR_1] : product(VAR_0,VAR_1,multiply(VAR_0,VAR_1)),
file('theBenchmark.p',total_function1) ).
cnf(c_5,plain,
product(A,B,multiply(A,B)),
inference(clausify,[status(thm)],[total_function1]) ).
fof(total_function2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( VAR_2 = VAR_3
| ~ product(VAR_0,VAR_1,VAR_3)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',total_function2) ).
cnf(c_6,plain,
( C = D
| ~ product(A,B,D)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[total_function2]) ).
fof(associativity1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( product(VAR_0,VAR_4,VAR_5)
| ~ product(VAR_2,VAR_3,VAR_5)
| ~ product(VAR_1,VAR_3,VAR_4)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',associativity1) ).
cnf(c_7,plain,
( product(A,E,F)
| ~ product(C,D,F)
| ~ product(B,D,E)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[associativity1]) ).
fof(associativity2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( product(VAR_2,VAR_3,VAR_5)
| ~ product(VAR_0,VAR_4,VAR_5)
| ~ product(VAR_1,VAR_3,VAR_4)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',associativity2) ).
cnf(c_8,plain,
( product(C,D,F)
| ~ product(A,E,F)
| ~ product(B,D,E)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[associativity2]) ).
fof(x_cubed_is_identity_1,axiom,
! [VAR_0,VAR_1] :
( product(VAR_0,VAR_1,identity)
| ~ product(VAR_0,VAR_0,VAR_1) ),
file('theBenchmark.p',x_cubed_is_identity_1) ).
cnf(c_9,plain,
( product(A,B,identity)
| ~ product(A,A,B) ),
inference(clausify,[status(thm)],[x_cubed_is_identity_1]) ).
fof(x_cubed_is_identity_2,axiom,
! [VAR_0,VAR_1] :
( product(VAR_1,VAR_0,identity)
| ~ product(VAR_0,VAR_0,VAR_1) ),
file('theBenchmark.p',x_cubed_is_identity_2) ).
cnf(c_10,plain,
( product(B,A,identity)
| ~ product(A,A,B) ),
inference(clausify,[status(thm)],[x_cubed_is_identity_2]) ).
fof(a_times_b_is_c,axiom,
product(a,b,c),
file('theBenchmark.p',a_times_b_is_c) ).
cnf(c_11,plain,
product(a,b,c),
inference(clausify,[status(thm)],[a_times_b_is_c]) ).
fof(c_times_inverse_a_is_d,axiom,
product(c,inverse(a),d),
file('theBenchmark.p',c_times_inverse_a_is_d) ).
cnf(c_12,plain,
product(c,inverse(a),d),
inference(clausify,[status(thm)],[c_times_inverse_a_is_d]) ).
fof(d_times_inverse_b_is_h,axiom,
product(d,inverse(b),h),
file('theBenchmark.p',d_times_inverse_b_is_h) ).
cnf(c_13,plain,
product(d,inverse(b),h),
inference(clausify,[status(thm)],[d_times_inverse_b_is_h]) ).
fof(h_times_b_is_j,axiom,
product(h,b,j),
file('theBenchmark.p',h_times_b_is_j) ).
cnf(c_14,plain,
product(h,b,j),
inference(clausify,[status(thm)],[h_times_b_is_j]) ).
fof(j_times_inverse_h_is_k,axiom,
product(j,inverse(h),k),
file('theBenchmark.p',j_times_inverse_h_is_k) ).
cnf(c_15,plain,
product(j,inverse(h),k),
inference(clausify,[status(thm)],[j_times_inverse_h_is_k]) ).
fof(prove_k_times_inverse_b_is_e,axiom,
~ product(k,inverse(b),identity),
file('theBenchmark.p',prove_k_times_inverse_b_is_e) ).
cnf(c_16,plain,
~ product(k,inverse(b),identity),
inference(clausify,[status(thm)],[prove_k_times_inverse_b_is_e]) ).
cnf(c_3903,plain,
( multiply(A,B) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_19,plain,
multiply(A,identity) = A,
inference(resolve,[status(thm)],[c_3903,c_2]) ).
cnf(c_3904,plain,
( multiply(A,B) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_20,plain,
multiply(identity,A) = A,
inference(resolve,[status(thm)],[c_3904,c_1]) ).
cnf(c_3905,plain,
( identity = B
| ~ product(A,inverse(A),B) ),
inference(resolve,[status(thm)],[c_6,c_4]) ).
cnf(c_3906,plain,
identity = inverse(identity),
inference(resolve,[status(thm)],[c_3905,c_1]) ).
cnf(c_21,plain,
inverse(identity) = identity,
inference(copy,[status(thm)],[c_3906]) ).
cnf(c_3907,plain,
( product(D,C,E)
| ~ product(multiply(D,A),B,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_7,c_5]) ).
cnf(c_3908,plain,
( product(A,multiply(B,C),D)
| ~ product(multiply(A,B),C,D) ),
inference(resolve,[status(thm)],[c_3907,c_5]) ).
cnf(c_22,plain,
product(A,multiply(B,C),multiply(multiply(A,B),C)),
inference(resolve,[status(thm)],[c_3908,c_5]) ).
cnf(c_3909,plain,
( product(A,C,D)
| ~ product(identity,B,D)
| ~ product(inverse(A),B,C) ),
inference(resolve,[status(thm)],[c_7,c_4]) ).
cnf(c_3910,plain,
( product(C,multiply(inverse(C),A),B)
| ~ product(identity,A,B) ),
inference(resolve,[status(thm)],[c_3909,c_5]) ).
cnf(c_3911,plain,
product(A,multiply(inverse(A),B),multiply(identity,B)),
inference(resolve,[status(thm)],[c_3910,c_5]) ).
cnf(c_26,plain,
product(A,multiply(inverse(A),B),B),
inference(paramod,[status(thm)],[c_20,c_3911]) ).
cnf(c_3912,plain,
( product(A,C,D)
| ~ product(identity,B,D)
| ~ product(inverse(A),B,C) ),
inference(resolve,[status(thm)],[c_7,c_4]) ).
cnf(c_3913,plain,
( product(A,identity,B)
| ~ product(identity,inverse(inverse(A)),B) ),
inference(resolve,[status(thm)],[c_3912,c_4]) ).
cnf(c_3914,plain,
product(A,identity,multiply(identity,inverse(inverse(A)))),
inference(resolve,[status(thm)],[c_3913,c_5]) ).
cnf(c_27,plain,
product(A,identity,inverse(inverse(A))),
inference(paramod,[status(thm)],[c_20,c_3914]) ).
cnf(c_3915,plain,
( product(inverse(A),C,D)
| ~ product(identity,B,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_7,c_3]) ).
cnf(c_3916,plain,
( product(inverse(C),multiply(C,A),B)
| ~ product(identity,A,B) ),
inference(resolve,[status(thm)],[c_3915,c_5]) ).
cnf(c_3917,plain,
product(inverse(A),multiply(A,B),multiply(identity,B)),
inference(resolve,[status(thm)],[c_3916,c_5]) ).
cnf(c_28,plain,
product(inverse(A),multiply(A,B),B),
inference(paramod,[status(thm)],[c_20,c_3917]) ).
cnf(c_38,plain,
product(A,multiply(A,A),identity),
inference(resolve,[status(thm)],[c_9,c_5]) ).
cnf(c_39,plain,
product(multiply(A,A),A,identity),
inference(resolve,[status(thm)],[c_10,c_5]) ).
cnf(c_3918,plain,
( product(c,A,C)
| ~ product(a,B,C)
| ~ product(b,A,B) ),
inference(resolve,[status(thm)],[c_8,c_11]) ).
cnf(c_3919,plain,
( product(c,A,B)
| ~ product(a,multiply(b,A),B) ),
inference(resolve,[status(thm)],[c_3918,c_5]) ).
cnf(c_44,plain,
product(c,A,multiply(a,multiply(b,A))),
inference(resolve,[status(thm)],[c_3919,c_5]) ).
cnf(c_3920,plain,
( product(inverse(A),C,D)
| ~ product(identity,B,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_7,c_3]) ).
cnf(c_3921,plain,
( product(inverse(a),c,A)
| ~ product(identity,b,A) ),
inference(resolve,[status(thm)],[c_3920,c_11]) ).
cnf(c_3922,plain,
product(inverse(a),c,multiply(identity,b)),
inference(resolve,[status(thm)],[c_3921,c_5]) ).
cnf(c_49,plain,
product(inverse(a),c,b),
inference(paramod,[status(thm)],[c_20,c_3922]) ).
cnf(c_3923,plain,
( multiply(A,B) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_54,plain,
multiply(a,b) = c,
inference(resolve,[status(thm)],[c_3923,c_11]) ).
cnf(c_3924,plain,
( product(d,A,C)
| ~ product(c,B,C)
| ~ product(inverse(a),A,B) ),
inference(resolve,[status(thm)],[c_8,c_12]) ).
cnf(c_3925,plain,
( product(d,a,A)
| ~ product(c,identity,A) ),
inference(resolve,[status(thm)],[c_3924,c_3]) ).
cnf(c_3926,plain,
product(d,a,multiply(c,identity)),
inference(resolve,[status(thm)],[c_3925,c_5]) ).
cnf(c_61,plain,
product(d,a,c),
inference(paramod,[status(thm)],[c_19,c_3926]) ).
cnf(c_3927,plain,
( product(h,A,C)
| ~ product(d,B,C)
| ~ product(inverse(b),A,B) ),
inference(resolve,[status(thm)],[c_8,c_13]) ).
cnf(c_3928,plain,
( product(h,b,A)
| ~ product(d,identity,A) ),
inference(resolve,[status(thm)],[c_3927,c_3]) ).
cnf(c_3929,plain,
product(h,b,multiply(d,identity)),
inference(resolve,[status(thm)],[c_3928,c_5]) ).
cnf(c_79,plain,
product(h,b,d),
inference(paramod,[status(thm)],[c_19,c_3929]) ).
cnf(c_3930,plain,
( product(k,A,C)
| ~ product(j,B,C)
| ~ product(inverse(h),A,B) ),
inference(resolve,[status(thm)],[c_8,c_15]) ).
cnf(c_3931,plain,
( product(k,h,A)
| ~ product(j,identity,A) ),
inference(resolve,[status(thm)],[c_3930,c_3]) ).
cnf(c_3932,plain,
product(k,h,multiply(j,identity)),
inference(resolve,[status(thm)],[c_3931,c_5]) ).
cnf(c_113,plain,
product(k,h,j),
inference(paramod,[status(thm)],[c_19,c_3932]) ).
cnf(c_3933,plain,
( product(C,inverse(B),D)
| ~ product(A,identity,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_8,c_4]) ).
cnf(c_3934,plain,
( product(B,inverse(A),identity)
| ~ product(inverse(identity),A,B) ),
inference(resolve,[status(thm)],[c_3933,c_3]) ).
cnf(c_3935,plain,
~ product(inverse(identity),b,k),
inference(resolve,[status(thm)],[c_3934,c_16]) ).
cnf(c_129,plain,
~ product(identity,b,k),
inference(paramod,[status(thm)],[c_21,c_3935]) ).
cnf(c_3936,plain,
( product(identity,B,D)
| ~ product(inverse(A),C,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_8,c_3]) ).
cnf(c_3937,plain,
( product(identity,b,A)
| ~ product(inverse(a),c,A) ),
inference(resolve,[status(thm)],[c_3936,c_11]) ).
cnf(c_147,plain,
~ product(inverse(a),c,k),
inference(resolve,[status(thm)],[c_3937,c_129]) ).
cnf(c_3938,plain,
( product(c,A,C)
| ~ product(d,B,C)
| ~ product(a,A,B) ),
inference(resolve,[status(thm)],[c_8,c_61]) ).
cnf(c_3939,plain,
( product(c,A,B)
| ~ product(d,multiply(a,A),B) ),
inference(resolve,[status(thm)],[c_3938,c_5]) ).
cnf(c_168,plain,
product(c,A,multiply(d,multiply(a,A))),
inference(resolve,[status(thm)],[c_3939,c_5]) ).
cnf(c_3940,plain,
( product(d,A,C)
| ~ product(h,B,C)
| ~ product(b,A,B) ),
inference(resolve,[status(thm)],[c_8,c_79]) ).
cnf(c_3941,plain,
( product(d,A,B)
| ~ product(h,multiply(b,A),B) ),
inference(resolve,[status(thm)],[c_3940,c_5]) ).
cnf(c_181,plain,
product(d,A,multiply(h,multiply(b,A))),
inference(resolve,[status(thm)],[c_3941,c_5]) ).
cnf(c_3942,plain,
( product(h,B,C)
| ~ product(d,A,C)
| ~ product(b,A,B) ),
inference(resolve,[status(thm)],[c_7,c_79]) ).
cnf(c_3943,plain,
( product(h,multiply(b,A),B)
| ~ product(d,A,B) ),
inference(resolve,[status(thm)],[c_3942,c_5]) ).
cnf(c_186,plain,
product(h,multiply(b,a),c),
inference(resolve,[status(thm)],[c_3943,c_61]) ).
cnf(c_3944,plain,
( j = A
| ~ product(h,b,A) ),
inference(resolve,[status(thm)],[c_6,c_14]) ).
cnf(c_189,plain,
j = d,
inference(resolve,[status(thm)],[c_3944,c_79]) ).
cnf(c_203,plain,
product(k,h,d),
inference(paramod,[status(thm)],[c_189,c_113]) ).
cnf(c_3945,plain,
( multiply(A,B) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_290,plain,
multiply(inverse(a),c) = b,
inference(resolve,[status(thm)],[c_3945,c_49]) ).
cnf(c_301,plain,
product(multiply(multiply(multiply(A,B),A),B),multiply(A,B),identity),
inference(resolve,[status(thm)],[c_10,c_22]) ).
cnf(c_3946,plain,
( multiply(A,B) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3947,plain,
multiply(A,multiply(B,C)) = multiply(multiply(A,B),C),
inference(resolve,[status(thm)],[c_3946,c_22]) ).
cnf(c_369,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(copy,[status(thm)],[c_3947]) ).
cnf(c_3948,plain,
product(multiply(multiply(A,multiply(B,A)),B),multiply(A,B),identity),
inference(paramod,[status(thm)],[c_369,c_301]) ).
cnf(c_3949,plain,
product(multiply(A,multiply(multiply(B,A),B)),multiply(A,B),identity),
inference(paramod,[status(thm)],[c_369,c_3948]) ).
cnf(c_374,plain,
product(multiply(A,multiply(B,multiply(A,B))),multiply(A,B),identity),
inference(paramod,[status(thm)],[c_369,c_3949]) ).
cnf(c_3950,plain,
( product(C,A,D)
| ~ product(C,B,D)
| ~ product(identity,A,B) ),
inference(resolve,[status(thm)],[c_8,c_2]) ).
cnf(c_3951,plain,
( product(B,A,C)
| ~ product(identity,A,multiply(inverse(B),C)) ),
inference(resolve,[status(thm)],[c_3950,c_26]) ).
cnf(c_711,plain,
~ product(identity,c,multiply(inverse(inverse(a)),k)),
inference(resolve,[status(thm)],[c_3951,c_147]) ).
cnf(c_3952,plain,
( multiply(A,B) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3953,plain,
multiply(A,identity) = inverse(inverse(A)),
inference(resolve,[status(thm)],[c_3952,c_27]) ).
cnf(c_3954,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_19,c_3953]) ).
cnf(c_920,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_3954]) ).
cnf(c_927,plain,
~ product(identity,c,multiply(a,k)),
inference(paramod,[status(thm)],[c_920,c_711]) ).
cnf(c_3955,plain,
( product(multiply(D,A),B,E)
| ~ product(D,C,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_8,c_5]) ).
cnf(c_3956,plain,
( product(multiply(A,C),multiply(C,C),B)
| ~ product(A,identity,B) ),
inference(resolve,[status(thm)],[c_3955,c_38]) ).
cnf(c_3957,plain,
product(multiply(A,B),multiply(B,B),multiply(A,identity)),
inference(resolve,[status(thm)],[c_3956,c_5]) ).
cnf(c_1080,plain,
product(multiply(A,B),multiply(B,B),A),
inference(paramod,[status(thm)],[c_19,c_3957]) ).
cnf(c_3958,plain,
( product(B,C,E)
| ~ product(inverse(A),D,E)
| ~ product(multiply(A,B),C,D) ),
inference(resolve,[status(thm)],[c_8,c_28]) ).
cnf(c_3959,plain,
( product(A,A,B)
| ~ product(inverse(A),identity,B) ),
inference(resolve,[status(thm)],[c_3958,c_39]) ).
cnf(c_3960,plain,
product(A,A,multiply(inverse(A),identity)),
inference(resolve,[status(thm)],[c_3959,c_5]) ).
cnf(c_1340,plain,
product(A,A,inverse(A)),
inference(paramod,[status(thm)],[c_19,c_3960]) ).
cnf(c_3961,plain,
( product(inverse(A),B,D)
| ~ product(A,C,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_8,c_1340]) ).
cnf(c_3962,plain,
( product(inverse(inverse(A)),multiply(A,B),C)
| ~ product(inverse(A),B,C) ),
inference(resolve,[status(thm)],[c_3961,c_28]) ).
cnf(c_3963,plain,
product(inverse(inverse(a)),multiply(a,c),b),
inference(resolve,[status(thm)],[c_3962,c_49]) ).
cnf(c_1625,plain,
product(a,multiply(a,c),b),
inference(paramod,[status(thm)],[c_920,c_3963]) ).
cnf(c_3964,plain,
( multiply(A,B) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3965,plain,
multiply(A,A) = inverse(A),
inference(resolve,[status(thm)],[c_3964,c_1340]) ).
cnf(c_1678,plain,
inverse(A) = multiply(A,A),
inference(copy,[status(thm)],[c_3965]) ).
cnf(c_3966,plain,
multiply(multiply(a,a),c) = b,
inference(paramod,[status(thm)],[c_1678,c_290]) ).
cnf(c_2225,plain,
multiply(a,multiply(a,c)) = b,
inference(paramod,[status(thm)],[c_369,c_3966]) ).
cnf(c_3967,plain,
( product(d,A,C)
| ~ product(k,B,C)
| ~ product(h,A,B) ),
inference(resolve,[status(thm)],[c_8,c_203]) ).
cnf(c_3968,plain,
( product(d,multiply(b,a),A)
| ~ product(k,c,A) ),
inference(resolve,[status(thm)],[c_3967,c_186]) ).
cnf(c_2301,plain,
product(d,multiply(b,a),multiply(k,c)),
inference(resolve,[status(thm)],[c_3968,c_5]) ).
cnf(c_3969,plain,
( multiply(A,B) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2391,plain,
multiply(c,A) = multiply(a,multiply(b,A)),
inference(resolve,[status(thm)],[c_3969,c_44]) ).
cnf(c_3970,plain,
( multiply(a,multiply(b,A)) = B
| ~ product(c,A,B) ),
inference(resolve,[status(thm)],[c_6,c_44]) ).
cnf(c_3971,plain,
multiply(a,multiply(b,A)) = multiply(d,multiply(a,A)),
inference(resolve,[status(thm)],[c_3970,c_168]) ).
cnf(c_2550,plain,
multiply(d,multiply(a,A)) = multiply(a,multiply(b,A)),
inference(copy,[status(thm)],[c_3971]) ).
cnf(c_3972,plain,
( multiply(A,B) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2718,plain,
multiply(d,A) = multiply(h,multiply(b,A)),
inference(resolve,[status(thm)],[c_3972,c_181]) ).
cnf(c_3973,plain,
multiply(h,multiply(b,multiply(a,A))) = multiply(a,multiply(b,A)),
inference(paramod,[status(thm)],[c_2718,c_2550]) ).
cnf(c_2743,plain,
multiply(a,multiply(b,A)) = multiply(h,multiply(b,multiply(a,A))),
inference(copy,[status(thm)],[c_3973]) ).
cnf(c_2847,plain,
multiply(c,A) = multiply(h,multiply(b,multiply(a,A))),
inference(paramod,[status(thm)],[c_2743,c_2391]) ).
cnf(c_3974,plain,
( product(multiply(D,A),B,E)
| ~ product(D,C,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_8,c_5]) ).
cnf(c_3975,plain,
( product(multiply(A,a),multiply(a,c),B)
| ~ product(A,b,B) ),
inference(resolve,[status(thm)],[c_3974,c_1625]) ).
cnf(c_2927,plain,
product(multiply(A,a),multiply(a,c),multiply(A,b)),
inference(resolve,[status(thm)],[c_3975,c_5]) ).
cnf(c_3976,plain,
( product(C,D,E)
| ~ product(A,multiply(B,D),E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_8,c_5]) ).
cnf(c_3977,plain,
( product(C,B,A)
| ~ product(multiply(A,B),B,C) ),
inference(resolve,[status(thm)],[c_3976,c_1080]) ).
cnf(c_3978,plain,
~ product(multiply(multiply(a,k),c),c,identity),
inference(resolve,[status(thm)],[c_3977,c_927]) ).
cnf(c_3087,plain,
~ product(multiply(a,multiply(k,c)),c,identity),
inference(paramod,[status(thm)],[c_369,c_3978]) ).
cnf(c_3979,plain,
( multiply(h,multiply(b,A)) = B
| ~ product(d,A,B) ),
inference(resolve,[status(thm)],[c_6,c_181]) ).
cnf(c_3980,plain,
multiply(h,multiply(b,multiply(b,a))) = multiply(k,c),
inference(resolve,[status(thm)],[c_3979,c_2301]) ).
cnf(c_3313,plain,
multiply(k,c) = multiply(h,multiply(b,multiply(b,a))),
inference(copy,[status(thm)],[c_3980]) ).
cnf(c_3318,plain,
~ product(multiply(a,multiply(h,multiply(b,multiply(b,a)))),c,identity),
inference(paramod,[status(thm)],[c_3313,c_3087]) ).
cnf(c_3981,plain,
( product(multiply(D,A),C,E)
| ~ product(D,B,E)
| ~ product(multiply(A,A),B,C) ),
inference(resolve,[status(thm)],[c_7,c_1080]) ).
cnf(c_3982,plain,
( product(multiply(A,a),multiply(a,b),B)
| ~ product(A,multiply(a,c),B) ),
inference(resolve,[status(thm)],[c_3981,c_2927]) ).
cnf(c_3983,plain,
product(multiply(multiply(a,multiply(c,multiply(a,c))),a),multiply(a,b),identity),
inference(resolve,[status(thm)],[c_3982,c_374]) ).
cnf(c_3984,plain,
product(multiply(multiply(a,multiply(h,multiply(b,multiply(a,multiply(a,c))))),a),multiply(a,b),identity),
inference(paramod,[status(thm)],[c_2847,c_3983]) ).
cnf(c_3985,plain,
product(multiply(multiply(a,multiply(h,multiply(b,b))),a),multiply(a,b),identity),
inference(paramod,[status(thm)],[c_2225,c_3984]) ).
cnf(c_3986,plain,
product(multiply(a,multiply(multiply(h,multiply(b,b)),a)),multiply(a,b),identity),
inference(paramod,[status(thm)],[c_369,c_3985]) ).
cnf(c_3987,plain,
product(multiply(a,multiply(h,multiply(multiply(b,b),a))),multiply(a,b),identity),
inference(paramod,[status(thm)],[c_369,c_3986]) ).
cnf(c_3988,plain,
product(multiply(a,multiply(h,multiply(b,multiply(b,a)))),multiply(a,b),identity),
inference(paramod,[status(thm)],[c_369,c_3987]) ).
cnf(c_3901,plain,
product(multiply(a,multiply(h,multiply(b,multiply(b,a)))),c,identity),
inference(paramod,[status(thm)],[c_54,c_3988]) ).
cnf(c_3902,plain,
$false,
inference(resolve,[status(thm)],[c_3901,c_3318]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP002-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n016.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 14:20:16 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 2568803 was started by sandbox on n016,
% 0.10/0.36 % Fri Sep 25 14:20:16 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 7.51/2.07
% 7.51/2.07 % SZS status Unsatisfiable for theBenchmark
% 7.51/2.07
% 7.51/2.07 % Proof 1 at 0.69 (+ 0.28) seconds.
% 7.51/2.07 % Length of proof is 62.
% 7.51/2.07 % Level of proof is 8.
% 7.51/2.07 % Maximum clause weight is 28.000.
% 7.51/2.07 % Given clauses 155.
% 7.51/2.07
% 7.51/2.07 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------