%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP125-2.005 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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:27:39 AM UTC 2026
% Result : Unsatisfiable 0.17s 0.54s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 27
% Syntax : Number of formulae : 232 ( 87 unt; 0 def)
% Number of atoms : 554 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 491 ( 169 ~; 322 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 113 ( 0 sgn 22 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(no_redundancy,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ greater(VAR_1,VAR_2)
| ~ next(VAR_0,VAR_2)
| ~ product(VAR_0,e_1,VAR_1) ),
file('theBenchmark.p',no_redundancy) ).
cnf(c_1,plain,
( ~ greater(B,C)
| ~ next(A,C)
| ~ product(A,e_1,B) ),
inference(clausify,[status(thm)],[no_redundancy]) ).
fof(e_3_then_e_4,axiom,
next(e_3,e_4),
file('theBenchmark.p',e_3_then_e_4) ).
cnf(c_3,plain,
next(e_3,e_4),
inference(clausify,[status(thm)],[e_3_then_e_4]) ).
fof(e_2_then_e_3,axiom,
next(e_2,e_3),
file('theBenchmark.p',e_2_then_e_3) ).
cnf(c_4,plain,
next(e_2,e_3),
inference(clausify,[status(thm)],[e_2_then_e_3]) ).
fof(e_5_greater_e_4,axiom,
greater(e_5,e_4),
file('theBenchmark.p',e_5_greater_e_4) ).
cnf(c_6,plain,
greater(e_5,e_4),
inference(clausify,[status(thm)],[e_5_greater_e_4]) ).
cnf(c_8,plain,
( ~ greater(A,e_4)
| ~ product(e_3,e_1,A) ),
inference(resolve,[status(thm)],[c_1,c_3]) ).
cnf(c_9,plain,
( ~ greater(A,e_3)
| ~ product(e_2,e_1,A) ),
inference(resolve,[status(thm)],[c_1,c_4]) ).
fof(e_5_greater_e_3,axiom,
greater(e_5,e_3),
file('theBenchmark.p',e_5_greater_e_3) ).
cnf(c_11,plain,
greater(e_5,e_3),
inference(clausify,[status(thm)],[e_5_greater_e_3]) ).
fof(e_4_greater_e_3,axiom,
greater(e_4,e_3),
file('theBenchmark.p',e_4_greater_e_3) ).
cnf(c_12,plain,
greater(e_4,e_3),
inference(clausify,[status(thm)],[e_4_greater_e_3]) ).
fof(product_total_function2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( equalish(VAR_2,VAR_3)
| ~ product(VAR_0,VAR_1,VAR_3)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',product_total_function2) ).
cnf(c_20,plain,
( equalish(C,D)
| ~ product(A,B,D)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[product_total_function2]) ).
fof(e_5_is_not_e_4,axiom,
~ equalish(e_5,e_4),
file('theBenchmark.p',e_5_is_not_e_4) ).
cnf(c_21,plain,
~ equalish(e_5,e_4),
inference(clausify,[status(thm)],[e_5_is_not_e_4]) ).
fof(e_5_is_not_e_3,axiom,
~ equalish(e_5,e_3),
file('theBenchmark.p',e_5_is_not_e_3) ).
cnf(c_22,plain,
~ equalish(e_5,e_3),
inference(clausify,[status(thm)],[e_5_is_not_e_3]) ).
fof(e_5_is_not_e_2,axiom,
~ equalish(e_5,e_2),
file('theBenchmark.p',e_5_is_not_e_2) ).
cnf(c_23,plain,
~ equalish(e_5,e_2),
inference(clausify,[status(thm)],[e_5_is_not_e_2]) ).
fof(e_5_is_not_e_1,axiom,
~ equalish(e_5,e_1),
file('theBenchmark.p',e_5_is_not_e_1) ).
cnf(c_24,plain,
~ equalish(e_5,e_1),
inference(clausify,[status(thm)],[e_5_is_not_e_1]) ).
fof(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3),
file('theBenchmark.p',e_4_is_not_e_3) ).
cnf(c_26,plain,
~ equalish(e_4,e_3),
inference(clausify,[status(thm)],[e_4_is_not_e_3]) ).
fof(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2),
file('theBenchmark.p',e_4_is_not_e_2) ).
cnf(c_27,plain,
~ equalish(e_4,e_2),
inference(clausify,[status(thm)],[e_4_is_not_e_2]) ).
fof(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1),
file('theBenchmark.p',e_4_is_not_e_1) ).
cnf(c_28,plain,
~ equalish(e_4,e_1),
inference(clausify,[status(thm)],[e_4_is_not_e_1]) ).
fof(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2),
file('theBenchmark.p',e_3_is_not_e_2) ).
cnf(c_31,plain,
~ equalish(e_3,e_2),
inference(clausify,[status(thm)],[e_3_is_not_e_2]) ).
fof(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1),
file('theBenchmark.p',e_3_is_not_e_1) ).
cnf(c_32,plain,
~ equalish(e_3,e_1),
inference(clausify,[status(thm)],[e_3_is_not_e_1]) ).
fof(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1),
file('theBenchmark.p',e_2_is_not_e_1) ).
cnf(c_36,plain,
~ equalish(e_2,e_1),
inference(clausify,[status(thm)],[e_2_is_not_e_1]) ).
fof(product_right_cancellation,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( equalish(VAR_1,VAR_3)
| ~ product(VAR_0,VAR_3,VAR_2)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',product_right_cancellation) ).
cnf(c_41,plain,
( equalish(B,D)
| ~ product(A,D,C)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[product_right_cancellation]) ).
fof(product_left_cancellation,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( equalish(VAR_0,VAR_3)
| ~ product(VAR_3,VAR_1,VAR_2)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',product_left_cancellation) ).
cnf(c_42,plain,
( equalish(A,D)
| ~ product(D,B,C)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[product_left_cancellation]) ).
cnf(c_43,plain,
( ~ product(e_1,A,B)
| ~ product(e_2,A,B) ),
inference(resolve,[status(thm)],[c_42,c_36]) ).
cnf(c_44,plain,
( ~ product(e_1,A,B)
| ~ product(e_3,A,B) ),
inference(resolve,[status(thm)],[c_42,c_32]) ).
cnf(c_45,plain,
( ~ product(e_2,A,B)
| ~ product(e_3,A,B) ),
inference(resolve,[status(thm)],[c_42,c_31]) ).
cnf(c_46,plain,
( ~ product(e_1,A,B)
| ~ product(e_4,A,B) ),
inference(resolve,[status(thm)],[c_42,c_28]) ).
cnf(c_47,plain,
( ~ product(e_2,A,B)
| ~ product(e_4,A,B) ),
inference(resolve,[status(thm)],[c_42,c_27]) ).
cnf(c_48,plain,
( ~ product(e_3,A,B)
| ~ product(e_4,A,B) ),
inference(resolve,[status(thm)],[c_42,c_26]) ).
cnf(c_49,plain,
( ~ product(e_1,A,B)
| ~ product(e_5,A,B) ),
inference(resolve,[status(thm)],[c_42,c_24]) ).
cnf(c_50,plain,
( ~ product(e_2,A,B)
| ~ product(e_5,A,B) ),
inference(resolve,[status(thm)],[c_42,c_23]) ).
cnf(c_51,plain,
( ~ product(e_3,A,B)
| ~ product(e_5,A,B) ),
inference(resolve,[status(thm)],[c_42,c_22]) ).
cnf(c_52,plain,
( ~ product(e_4,A,B)
| ~ product(e_5,A,B) ),
inference(resolve,[status(thm)],[c_42,c_21]) ).
cnf(c_53,plain,
( ~ product(A,e_1,B)
| ~ product(A,e_2,B) ),
inference(resolve,[status(thm)],[c_41,c_36]) ).
cnf(c_54,plain,
( ~ product(A,e_1,B)
| ~ product(A,e_3,B) ),
inference(resolve,[status(thm)],[c_41,c_32]) ).
cnf(c_55,plain,
( ~ product(A,e_2,B)
| ~ product(A,e_3,B) ),
inference(resolve,[status(thm)],[c_41,c_31]) ).
cnf(c_56,plain,
( ~ product(A,e_1,B)
| ~ product(A,e_4,B) ),
inference(resolve,[status(thm)],[c_41,c_28]) ).
cnf(c_57,plain,
( ~ product(A,e_2,B)
| ~ product(A,e_4,B) ),
inference(resolve,[status(thm)],[c_41,c_27]) ).
cnf(c_58,plain,
( ~ product(A,e_3,B)
| ~ product(A,e_4,B) ),
inference(resolve,[status(thm)],[c_41,c_26]) ).
cnf(c_59,plain,
( ~ product(A,e_1,B)
| ~ product(A,e_5,B) ),
inference(resolve,[status(thm)],[c_41,c_24]) ).
cnf(c_60,plain,
( ~ product(A,e_2,B)
| ~ product(A,e_5,B) ),
inference(resolve,[status(thm)],[c_41,c_23]) ).
cnf(c_62,plain,
( ~ product(A,e_4,B)
| ~ product(A,e_5,B) ),
inference(resolve,[status(thm)],[c_41,c_21]) ).
cnf(c_65,plain,
( ~ product(A,B,e_2)
| ~ product(A,B,e_3) ),
inference(resolve,[status(thm)],[c_20,c_31]) ).
cnf(c_67,plain,
( ~ product(A,B,e_2)
| ~ product(A,B,e_4) ),
inference(resolve,[status(thm)],[c_20,c_27]) ).
cnf(c_68,plain,
( ~ product(A,B,e_3)
| ~ product(A,B,e_4) ),
inference(resolve,[status(thm)],[c_20,c_26]) ).
cnf(c_70,plain,
( ~ product(A,B,e_2)
| ~ product(A,B,e_5) ),
inference(resolve,[status(thm)],[c_20,c_23]) ).
fof(qg3,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( product(VAR_2,VAR_3,VAR_0)
| ~ product(VAR_1,VAR_0,VAR_3)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',qg3) ).
cnf(c_73,plain,
( product(C,D,A)
| ~ product(B,A,D)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[qg3]) ).
fof(product_idempotence,axiom,
! [VAR_0] : product(VAR_0,VAR_0,VAR_0),
file('theBenchmark.p',product_idempotence) ).
cnf(c_74,plain,
product(A,A,A),
inference(clausify,[status(thm)],[product_idempotence]) ).
fof(product_total_function1,axiom,
! [VAR_0,VAR_1] :
( product(VAR_0,VAR_1,e_5)
| product(VAR_0,VAR_1,e_4)
| product(VAR_0,VAR_1,e_3)
| product(VAR_0,VAR_1,e_2)
| product(VAR_0,VAR_1,e_1)
| ~ group_element(VAR_1)
| ~ group_element(VAR_0) ),
file('theBenchmark.p',product_total_function1) ).
cnf(c_75,plain,
( product(A,B,e_5)
| product(A,B,e_4)
| product(A,B,e_3)
| product(A,B,e_2)
| product(A,B,e_1)
| ~ group_element(B)
| ~ group_element(A) ),
inference(clausify,[status(thm)],[product_total_function1]) ).
fof(element_5,axiom,
group_element(e_5),
file('theBenchmark.p',element_5) ).
cnf(c_76,plain,
group_element(e_5),
inference(clausify,[status(thm)],[element_5]) ).
fof(element_4,axiom,
group_element(e_4),
file('theBenchmark.p',element_4) ).
cnf(c_77,plain,
group_element(e_4),
inference(clausify,[status(thm)],[element_4]) ).
fof(element_3,axiom,
group_element(e_3),
file('theBenchmark.p',element_3) ).
cnf(c_78,plain,
group_element(e_3),
inference(clausify,[status(thm)],[element_3]) ).
fof(element_2,axiom,
group_element(e_2),
file('theBenchmark.p',element_2) ).
cnf(c_79,plain,
group_element(e_2),
inference(clausify,[status(thm)],[element_2]) ).
fof(element_1,axiom,
group_element(e_1),
file('theBenchmark.p',element_1) ).
cnf(c_80,plain,
group_element(e_1),
inference(clausify,[status(thm)],[element_1]) ).
cnf(c_81,plain,
~ product(e_3,e_1,e_5),
inference(resolve,[status(thm)],[c_6,c_8]) ).
cnf(c_82,plain,
~ product(e_2,e_1,e_5),
inference(resolve,[status(thm)],[c_11,c_9]) ).
cnf(c_83,plain,
~ product(e_2,e_1,e_4),
inference(resolve,[status(thm)],[c_12,c_9]) ).
cnf(c_93,plain,
~ product(e_5,e_5,e_2),
inference(resolve,[status(thm)],[c_74,c_70]) ).
cnf(c_95,plain,
~ product(e_4,e_4,e_3),
inference(resolve,[status(thm)],[c_74,c_68]) ).
cnf(c_96,plain,
~ product(e_4,e_4,e_2),
inference(resolve,[status(thm)],[c_74,c_67]) ).
cnf(c_98,plain,
~ product(e_3,e_3,e_2),
inference(resolve,[status(thm)],[c_74,c_65]) ).
cnf(c_103,plain,
~ product(e_5,e_2,e_5),
inference(resolve,[status(thm)],[c_74,c_60]) ).
cnf(c_104,plain,
~ product(e_5,e_1,e_5),
inference(resolve,[status(thm)],[c_74,c_59]) ).
cnf(c_106,plain,
~ product(e_4,e_2,e_4),
inference(resolve,[status(thm)],[c_74,c_57]) ).
cnf(c_108,plain,
~ product(e_3,e_2,e_3),
inference(resolve,[status(thm)],[c_74,c_55]) ).
cnf(c_109,plain,
~ product(e_3,e_1,e_3),
inference(resolve,[status(thm)],[c_74,c_54]) ).
cnf(c_110,plain,
~ product(e_2,e_1,e_2),
inference(resolve,[status(thm)],[c_74,c_53]) ).
cnf(c_113,plain,
~ product(e_2,e_5,e_5),
inference(resolve,[status(thm)],[c_74,c_50]) ).
cnf(c_115,plain,
~ product(e_3,e_4,e_4),
inference(resolve,[status(thm)],[c_74,c_48]) ).
cnf(c_116,plain,
~ product(e_2,e_4,e_4),
inference(resolve,[status(thm)],[c_74,c_47]) ).
cnf(c_119,plain,
~ product(e_1,e_3,e_3),
inference(resolve,[status(thm)],[c_74,c_44]) ).
cnf(c_120,plain,
~ product(e_1,e_2,e_2),
inference(resolve,[status(thm)],[c_74,c_43]) ).
cnf(c_125,plain,
~ product(e_2,e_2,e_4),
inference(resolve,[status(thm)],[c_67,c_74]) ).
cnf(c_130,plain,
~ product(e_2,e_5,e_2),
inference(resolve,[status(thm)],[c_60,c_74]) ).
cnf(c_132,plain,
~ product(e_3,e_4,e_3),
inference(resolve,[status(thm)],[c_58,c_74]) ).
cnf(c_133,plain,
~ product(e_2,e_4,e_2),
inference(resolve,[status(thm)],[c_57,c_74]) ).
cnf(c_136,plain,
~ product(e_1,e_3,e_1),
inference(resolve,[status(thm)],[c_54,c_74]) ).
cnf(c_137,plain,
~ product(e_1,e_2,e_1),
inference(resolve,[status(thm)],[c_53,c_74]) ).
cnf(c_140,plain,
~ product(e_5,e_2,e_2),
inference(resolve,[status(thm)],[c_50,c_74]) ).
cnf(c_141,plain,
~ product(e_5,e_1,e_1),
inference(resolve,[status(thm)],[c_49,c_74]) ).
cnf(c_143,plain,
~ product(e_4,e_2,e_2),
inference(resolve,[status(thm)],[c_47,c_74]) ).
cnf(c_145,plain,
~ product(e_3,e_2,e_2),
inference(resolve,[status(thm)],[c_45,c_74]) ).
cnf(c_146,plain,
~ product(e_3,e_1,e_1),
inference(resolve,[status(thm)],[c_44,c_74]) ).
cnf(c_147,plain,
~ product(e_2,e_1,e_1),
inference(resolve,[status(thm)],[c_43,c_74]) ).
cnf(c_651,plain,
( product(e_3,A,e_5)
| product(e_3,A,e_4)
| product(e_3,A,e_3)
| product(e_3,A,e_2)
| product(e_3,A,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_75,c_78]) ).
cnf(c_652,plain,
( product(e_3,e_4,e_5)
| product(e_3,e_4,e_4)
| product(e_3,e_4,e_3)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_1) ),
inference(resolve,[status(thm)],[c_651,c_77]) ).
cnf(c_653,plain,
( product(e_3,e_4,e_5)
| product(e_3,e_4,e_4)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_1) ),
inference(resolve,[status(thm)],[c_132,c_652]) ).
cnf(c_158,plain,
( product(e_3,e_4,e_5)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_1) ),
inference(resolve,[status(thm)],[c_115,c_653]) ).
cnf(c_654,plain,
( product(e_3,A,e_5)
| product(e_3,A,e_4)
| product(e_3,A,e_3)
| product(e_3,A,e_2)
| product(e_3,A,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_75,c_78]) ).
cnf(c_655,plain,
( product(e_3,e_2,e_5)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_1) ),
inference(resolve,[status(thm)],[c_654,c_79]) ).
cnf(c_656,plain,
( product(e_3,e_2,e_5)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_1) ),
inference(resolve,[status(thm)],[c_145,c_655]) ).
cnf(c_162,plain,
( product(e_3,e_2,e_5)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_1) ),
inference(resolve,[status(thm)],[c_108,c_656]) ).
cnf(c_657,plain,
( product(e_4,A,e_5)
| product(e_4,A,e_4)
| product(e_4,A,e_3)
| product(e_4,A,e_2)
| product(e_4,A,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_75,c_77]) ).
cnf(c_658,plain,
( product(e_4,e_2,e_5)
| product(e_4,e_2,e_4)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_1) ),
inference(resolve,[status(thm)],[c_657,c_79]) ).
cnf(c_659,plain,
( product(e_4,e_2,e_5)
| product(e_4,e_2,e_4)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_1) ),
inference(resolve,[status(thm)],[c_143,c_658]) ).
cnf(c_163,plain,
( product(e_4,e_2,e_5)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_1) ),
inference(resolve,[status(thm)],[c_106,c_659]) ).
cnf(c_660,plain,
( product(e_5,A,e_5)
| product(e_5,A,e_4)
| product(e_5,A,e_3)
| product(e_5,A,e_2)
| product(e_5,A,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_75,c_76]) ).
cnf(c_661,plain,
( product(e_5,e_2,e_5)
| product(e_5,e_2,e_4)
| product(e_5,e_2,e_3)
| product(e_5,e_2,e_2)
| product(e_5,e_2,e_1) ),
inference(resolve,[status(thm)],[c_660,c_79]) ).
cnf(c_662,plain,
( product(e_5,e_2,e_5)
| product(e_5,e_2,e_4)
| product(e_5,e_2,e_3)
| product(e_5,e_2,e_1) ),
inference(resolve,[status(thm)],[c_140,c_661]) ).
cnf(c_164,plain,
( product(e_5,e_2,e_4)
| product(e_5,e_2,e_3)
| product(e_5,e_2,e_1) ),
inference(resolve,[status(thm)],[c_103,c_662]) ).
cnf(c_663,plain,
( product(e_2,A,e_5)
| product(e_2,A,e_4)
| product(e_2,A,e_3)
| product(e_2,A,e_2)
| product(e_2,A,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_75,c_79]) ).
cnf(c_664,plain,
( product(e_2,e_4,e_5)
| product(e_2,e_4,e_4)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(resolve,[status(thm)],[c_663,c_77]) ).
cnf(c_665,plain,
( product(e_2,e_4,e_5)
| product(e_2,e_4,e_4)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_1) ),
inference(resolve,[status(thm)],[c_133,c_664]) ).
cnf(c_166,plain,
( product(e_2,e_4,e_5)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_1) ),
inference(resolve,[status(thm)],[c_116,c_665]) ).
cnf(c_666,plain,
( product(e_2,A,e_5)
| product(e_2,A,e_4)
| product(e_2,A,e_3)
| product(e_2,A,e_2)
| product(e_2,A,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_75,c_79]) ).
cnf(c_667,plain,
( product(e_2,e_5,e_5)
| product(e_2,e_5,e_4)
| product(e_2,e_5,e_3)
| product(e_2,e_5,e_2)
| product(e_2,e_5,e_1) ),
inference(resolve,[status(thm)],[c_666,c_76]) ).
cnf(c_668,plain,
( product(e_2,e_5,e_5)
| product(e_2,e_5,e_4)
| product(e_2,e_5,e_3)
| product(e_2,e_5,e_1) ),
inference(resolve,[status(thm)],[c_130,c_667]) ).
cnf(c_167,plain,
( product(e_2,e_5,e_4)
| product(e_2,e_5,e_3)
| product(e_2,e_5,e_1) ),
inference(resolve,[status(thm)],[c_113,c_668]) ).
cnf(c_669,plain,
( product(e_2,A,e_5)
| product(e_2,A,e_4)
| product(e_2,A,e_3)
| product(e_2,A,e_2)
| product(e_2,A,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_75,c_79]) ).
cnf(c_670,plain,
( product(e_2,e_1,e_5)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_669,c_80]) ).
cnf(c_671,plain,
( product(e_2,e_1,e_5)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_2) ),
inference(resolve,[status(thm)],[c_147,c_670]) ).
cnf(c_672,plain,
( product(e_2,e_1,e_5)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_3) ),
inference(resolve,[status(thm)],[c_110,c_671]) ).
cnf(c_673,plain,
( product(e_2,e_1,e_5)
| product(e_2,e_1,e_3) ),
inference(resolve,[status(thm)],[c_83,c_672]) ).
cnf(c_170,plain,
product(e_2,e_1,e_3),
inference(resolve,[status(thm)],[c_82,c_673]) ).
cnf(c_674,plain,
( product(e_3,A,e_5)
| product(e_3,A,e_4)
| product(e_3,A,e_3)
| product(e_3,A,e_2)
| product(e_3,A,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_75,c_78]) ).
cnf(c_675,plain,
( product(e_3,e_1,e_5)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_1) ),
inference(resolve,[status(thm)],[c_674,c_80]) ).
cnf(c_676,plain,
( product(e_3,e_1,e_5)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_2) ),
inference(resolve,[status(thm)],[c_146,c_675]) ).
cnf(c_677,plain,
( product(e_3,e_1,e_5)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_2) ),
inference(resolve,[status(thm)],[c_109,c_676]) ).
cnf(c_171,plain,
( product(e_3,e_1,e_4)
| product(e_3,e_1,e_2) ),
inference(resolve,[status(thm)],[c_81,c_677]) ).
cnf(c_678,plain,
( product(e_5,A,e_5)
| product(e_5,A,e_4)
| product(e_5,A,e_3)
| product(e_5,A,e_2)
| product(e_5,A,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_75,c_76]) ).
cnf(c_679,plain,
( product(e_5,e_1,e_5)
| product(e_5,e_1,e_4)
| product(e_5,e_1,e_3)
| product(e_5,e_1,e_2)
| product(e_5,e_1,e_1) ),
inference(resolve,[status(thm)],[c_678,c_80]) ).
cnf(c_680,plain,
( product(e_5,e_1,e_5)
| product(e_5,e_1,e_4)
| product(e_5,e_1,e_3)
| product(e_5,e_1,e_2) ),
inference(resolve,[status(thm)],[c_141,c_679]) ).
cnf(c_173,plain,
( product(e_5,e_1,e_4)
| product(e_5,e_1,e_3)
| product(e_5,e_1,e_2) ),
inference(resolve,[status(thm)],[c_104,c_680]) ).
cnf(c_681,plain,
( product(e_1,A,e_5)
| product(e_1,A,e_4)
| product(e_1,A,e_3)
| product(e_1,A,e_2)
| product(e_1,A,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_75,c_80]) ).
cnf(c_682,plain,
( product(e_1,e_2,e_5)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_1) ),
inference(resolve,[status(thm)],[c_681,c_79]) ).
cnf(c_683,plain,
( product(e_1,e_2,e_5)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2) ),
inference(resolve,[status(thm)],[c_137,c_682]) ).
cnf(c_174,plain,
( product(e_1,e_2,e_5)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_3) ),
inference(resolve,[status(thm)],[c_120,c_683]) ).
cnf(c_684,plain,
( product(e_1,A,e_5)
| product(e_1,A,e_4)
| product(e_1,A,e_3)
| product(e_1,A,e_2)
| product(e_1,A,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_75,c_80]) ).
cnf(c_685,plain,
( product(e_1,e_3,e_5)
| product(e_1,e_3,e_4)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1) ),
inference(resolve,[status(thm)],[c_684,c_78]) ).
cnf(c_686,plain,
( product(e_1,e_3,e_5)
| product(e_1,e_3,e_4)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_2) ),
inference(resolve,[status(thm)],[c_136,c_685]) ).
cnf(c_175,plain,
( product(e_1,e_3,e_5)
| product(e_1,e_3,e_4)
| product(e_1,e_3,e_2) ),
inference(resolve,[status(thm)],[c_119,c_686]) ).
cnf(c_178,plain,
( product(A,e_3,e_1)
| ~ product(e_1,e_2,A) ),
inference(resolve,[status(thm)],[c_170,c_73]) ).
cnf(c_179,plain,
( product(e_3,A,e_2)
| ~ product(e_1,e_2,A) ),
inference(resolve,[status(thm)],[c_170,c_73]) ).
cnf(c_180,plain,
~ product(e_2,e_5,e_3),
inference(resolve,[status(thm)],[c_59,c_170]) ).
cnf(c_181,plain,
~ product(e_2,e_4,e_3),
inference(resolve,[status(thm)],[c_56,c_170]) ).
cnf(c_182,plain,
~ product(e_5,e_1,e_3),
inference(resolve,[status(thm)],[c_50,c_170]) ).
cnf(c_184,plain,
( product(e_2,e_5,e_4)
| product(e_2,e_5,e_1) ),
inference(resolve,[status(thm)],[c_180,c_167]) ).
cnf(c_185,plain,
( product(e_2,e_4,e_5)
| product(e_2,e_4,e_1) ),
inference(resolve,[status(thm)],[c_181,c_166]) ).
cnf(c_186,plain,
( product(e_5,e_1,e_4)
| product(e_5,e_1,e_2) ),
inference(resolve,[status(thm)],[c_182,c_173]) ).
cnf(c_189,plain,
( product(e_4,A,e_3)
| ~ product(e_1,e_3,A)
| product(e_3,e_1,e_2) ),
inference(resolve,[status(thm)],[c_171,c_73]) ).
cnf(c_687,plain,
( product(e_3,A,e_2)
| ~ product(e_1,e_2,A) ),
inference(resolve,[status(thm)],[c_73,c_170]) ).
cnf(c_190,plain,
~ product(e_1,e_2,e_3),
inference(resolve,[status(thm)],[c_687,c_98]) ).
cnf(c_191,plain,
( product(e_1,e_2,e_5)
| product(e_1,e_2,e_4) ),
inference(resolve,[status(thm)],[c_190,c_174]) ).
cnf(c_193,plain,
( product(e_4,A,e_2)
| ~ product(e_5,e_2,A)
| product(e_2,e_5,e_1) ),
inference(resolve,[status(thm)],[c_184,c_73]) ).
cnf(c_196,plain,
( product(A,e_5,e_4)
| ~ product(e_4,e_2,A)
| product(e_2,e_4,e_1) ),
inference(resolve,[status(thm)],[c_185,c_73]) ).
cnf(c_197,plain,
( product(e_5,A,e_2)
| ~ product(e_4,e_2,A)
| product(e_2,e_4,e_1) ),
inference(resolve,[status(thm)],[c_185,c_73]) ).
cnf(c_688,plain,
( product(e_5,e_1,e_2)
| ~ product(e_3,e_1,e_4) ),
inference(resolve,[status(thm)],[c_51,c_186]) ).
cnf(c_203,plain,
( product(e_3,e_1,e_2)
| product(e_5,e_1,e_2) ),
inference(resolve,[status(thm)],[c_688,c_171]) ).
cnf(c_206,plain,
( product(e_3,e_5,e_2)
| product(e_1,e_2,e_4) ),
inference(resolve,[status(thm)],[c_191,c_179]) ).
cnf(c_207,plain,
( product(e_5,e_3,e_1)
| product(e_1,e_2,e_4) ),
inference(resolve,[status(thm)],[c_191,c_178]) ).
cnf(c_212,plain,
( ~ product(e_4,e_1,e_2)
| product(e_3,e_1,e_2) ),
inference(resolve,[status(thm)],[c_203,c_52]) ).
cnf(c_216,plain,
( ~ product(e_3,e_4,e_2)
| product(e_1,e_2,e_4) ),
inference(resolve,[status(thm)],[c_206,c_62]) ).
cnf(c_217,plain,
( ~ product(e_3,e_1,e_2)
| product(e_1,e_2,e_4) ),
inference(resolve,[status(thm)],[c_206,c_59]) ).
cnf(c_221,plain,
( ~ product(e_5,e_2,e_1)
| product(e_1,e_2,e_4) ),
inference(resolve,[status(thm)],[c_207,c_55]) ).
cnf(c_689,plain,
( product(e_3,e_4,e_2)
| product(e_3,e_4,e_1)
| ~ product(e_2,e_4,e_5) ),
inference(resolve,[status(thm)],[c_45,c_158]) ).
cnf(c_253,plain,
( product(e_2,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_1) ),
inference(resolve,[status(thm)],[c_689,c_185]) ).
cnf(c_690,plain,
( product(e_3,e_2,e_4)
| product(e_3,e_2,e_1)
| ~ product(e_1,e_2,e_5) ),
inference(resolve,[status(thm)],[c_44,c_162]) ).
cnf(c_267,plain,
( product(e_1,e_2,e_4)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_1) ),
inference(resolve,[status(thm)],[c_690,c_191]) ).
cnf(c_691,plain,
( product(e_2,e_4,e_1)
| product(e_5,A,e_2)
| ~ product(e_4,e_2,A) ),
inference(resolve,[status(thm)],[c_73,c_185]) ).
cnf(c_692,plain,
( product(e_4,e_2,e_3)
| product(e_4,e_2,e_1)
| product(e_2,e_4,e_1)
| product(e_5,e_5,e_2) ),
inference(resolve,[status(thm)],[c_691,c_163]) ).
cnf(c_273,plain,
( product(e_4,e_2,e_3)
| product(e_4,e_2,e_1)
| product(e_2,e_4,e_1) ),
inference(resolve,[status(thm)],[c_93,c_692]) ).
cnf(c_693,plain,
( product(e_2,e_5,e_1)
| product(e_4,A,e_2)
| ~ product(e_5,e_2,A) ),
inference(resolve,[status(thm)],[c_73,c_184]) ).
cnf(c_694,plain,
( product(e_5,e_2,e_3)
| product(e_5,e_2,e_1)
| product(e_2,e_5,e_1)
| product(e_4,e_4,e_2) ),
inference(resolve,[status(thm)],[c_693,c_164]) ).
cnf(c_283,plain,
( product(e_5,e_2,e_3)
| product(e_5,e_2,e_1)
| product(e_2,e_5,e_1) ),
inference(resolve,[status(thm)],[c_96,c_694]) ).
cnf(c_695,plain,
( product(e_1,e_3,e_4)
| product(e_1,e_3,e_2)
| ~ product(e_1,e_2,e_5) ),
inference(resolve,[status(thm)],[c_55,c_175]) ).
cnf(c_297,plain,
( product(e_1,e_2,e_4)
| product(e_1,e_3,e_4)
| product(e_1,e_3,e_2) ),
inference(resolve,[status(thm)],[c_695,c_191]) ).
cnf(c_330,plain,
( product(e_1,e_2,e_4)
| product(e_2,e_4,e_1)
| product(e_3,e_4,e_1) ),
inference(resolve,[status(thm)],[c_253,c_216]) ).
cnf(c_696,plain,
( product(e_1,e_2,e_4)
| product(e_3,e_2,e_1)
| ~ product(e_3,e_1,e_4) ),
inference(resolve,[status(thm)],[c_53,c_267]) ).
cnf(c_359,plain,
( product(e_3,e_1,e_2)
| product(e_1,e_2,e_4)
| product(e_3,e_2,e_1) ),
inference(resolve,[status(thm)],[c_696,c_171]) ).
cnf(c_697,plain,
( product(e_5,e_3,e_2)
| product(e_2,e_4,e_1)
| product(e_4,e_2,e_1)
| product(e_2,e_4,e_1) ),
inference(resolve,[status(thm)],[c_273,c_197]) ).
cnf(c_362,plain,
( product(e_5,e_3,e_2)
| product(e_4,e_2,e_1)
| product(e_2,e_4,e_1) ),
inference(copy,[status(thm)],[c_697]) ).
cnf(c_698,plain,
( product(e_4,e_3,e_2)
| product(e_2,e_5,e_1)
| product(e_5,e_2,e_1)
| product(e_2,e_5,e_1) ),
inference(resolve,[status(thm)],[c_283,c_193]) ).
cnf(c_373,plain,
( product(e_4,e_3,e_2)
| product(e_5,e_2,e_1)
| product(e_2,e_5,e_1) ),
inference(copy,[status(thm)],[c_698]) ).
cnf(c_699,plain,
( product(e_4,e_4,e_3)
| product(e_3,e_1,e_2)
| product(e_1,e_2,e_4)
| product(e_1,e_3,e_2) ),
inference(resolve,[status(thm)],[c_297,c_189]) ).
cnf(c_396,plain,
( product(e_3,e_1,e_2)
| product(e_1,e_2,e_4)
| product(e_1,e_3,e_2) ),
inference(resolve,[status(thm)],[c_95,c_699]) ).
cnf(c_700,plain,
( product(e_1,e_2,e_4)
| product(e_2,e_4,e_1)
| ~ product(e_3,e_2,e_1) ),
inference(resolve,[status(thm)],[c_57,c_330]) ).
cnf(c_701,plain,
( product(e_3,e_1,e_2)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_4)
| product(e_2,e_4,e_1) ),
inference(resolve,[status(thm)],[c_700,c_359]) ).
cnf(c_439,plain,
( product(e_3,e_1,e_2)
| product(e_1,e_2,e_4)
| product(e_2,e_4,e_1) ),
inference(copy,[status(thm)],[c_701]) ).
cnf(c_702,plain,
( product(e_4,e_2,e_1)
| product(e_2,e_4,e_1)
| ~ product(e_5,e_1,e_2) ),
inference(resolve,[status(thm)],[c_54,c_362]) ).
cnf(c_461,plain,
( product(e_3,e_1,e_2)
| product(e_4,e_2,e_1)
| product(e_2,e_4,e_1) ),
inference(resolve,[status(thm)],[c_702,c_203]) ).
cnf(c_468,plain,
( product(e_1,e_2,e_4)
| product(e_4,e_3,e_2)
| product(e_2,e_5,e_1) ),
inference(resolve,[status(thm)],[c_373,c_221]) ).
cnf(c_703,plain,
( product(e_4,e_1,e_2)
| product(e_2,e_5,e_1)
| product(e_4,e_3,e_2)
| product(e_2,e_5,e_1) ),
inference(resolve,[status(thm)],[c_373,c_193]) ).
cnf(c_469,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_3,e_2)
| product(e_2,e_5,e_1) ),
inference(copy,[status(thm)],[c_703]) ).
cnf(c_704,plain,
( product(e_1,e_2,e_4)
| product(e_1,e_2,e_4)
| product(e_1,e_3,e_2) ),
inference(resolve,[status(thm)],[c_396,c_217]) ).
cnf(c_485,plain,
( product(e_1,e_2,e_4)
| product(e_1,e_3,e_2) ),
inference(copy,[status(thm)],[c_704]) ).
cnf(c_705,plain,
( product(e_1,e_2,e_4)
| product(e_1,e_2,e_4)
| product(e_2,e_4,e_1) ),
inference(resolve,[status(thm)],[c_439,c_217]) ).
cnf(c_510,plain,
( product(e_1,e_2,e_4)
| product(e_2,e_4,e_1) ),
inference(copy,[status(thm)],[c_705]) ).
cnf(c_706,plain,
( product(e_1,e_5,e_4)
| product(e_2,e_4,e_1)
| product(e_3,e_1,e_2)
| product(e_2,e_4,e_1) ),
inference(resolve,[status(thm)],[c_461,c_196]) ).
cnf(c_515,plain,
( product(e_1,e_5,e_4)
| product(e_3,e_1,e_2)
| product(e_2,e_4,e_1) ),
inference(copy,[status(thm)],[c_706]) ).
cnf(c_707,plain,
( product(e_1,e_2,e_4)
| product(e_2,e_5,e_1)
| ~ product(e_1,e_3,e_2) ),
inference(resolve,[status(thm)],[c_46,c_468]) ).
cnf(c_708,plain,
( product(e_1,e_2,e_4)
| product(e_1,e_2,e_4)
| product(e_2,e_5,e_1) ),
inference(resolve,[status(thm)],[c_707,c_485]) ).
cnf(c_542,plain,
( product(e_1,e_2,e_4)
| product(e_2,e_5,e_1) ),
inference(copy,[status(thm)],[c_708]) ).
cnf(c_709,plain,
( product(e_1,e_2,e_4)
| ~ product(e_2,e_4,e_1) ),
inference(resolve,[status(thm)],[c_62,c_542]) ).
cnf(c_710,plain,
( product(e_1,e_2,e_4)
| product(e_1,e_2,e_4) ),
inference(resolve,[status(thm)],[c_709,c_510]) ).
cnf(c_549,plain,
product(e_1,e_2,e_4),
inference(copy,[status(thm)],[c_710]) ).
cnf(c_552,plain,
product(e_3,e_4,e_2),
inference(resolve,[status(thm)],[c_549,c_179]) ).
cnf(c_557,plain,
~ product(e_1,e_5,e_4),
inference(resolve,[status(thm)],[c_60,c_549]) ).
cnf(c_573,plain,
( product(e_3,e_1,e_2)
| product(e_2,e_4,e_1) ),
inference(resolve,[status(thm)],[c_557,c_515]) ).
cnf(c_589,plain,
~ product(e_3,e_1,e_2),
inference(resolve,[status(thm)],[c_552,c_56]) ).
cnf(c_711,plain,
( product(A,e_2,e_4)
| ~ product(e_4,e_3,A) ),
inference(resolve,[status(thm)],[c_73,c_552]) ).
cnf(c_591,plain,
~ product(e_4,e_3,e_2),
inference(resolve,[status(thm)],[c_711,c_125]) ).
cnf(c_598,plain,
product(e_2,e_4,e_1),
inference(resolve,[status(thm)],[c_589,c_573]) ).
cnf(c_600,plain,
~ product(e_4,e_1,e_2),
inference(resolve,[status(thm)],[c_589,c_212]) ).
cnf(c_712,plain,
( product(e_4,e_1,e_2)
| product(e_2,e_5,e_1) ),
inference(resolve,[status(thm)],[c_591,c_469]) ).
cnf(c_617,plain,
product(e_2,e_5,e_1),
inference(resolve,[status(thm)],[c_600,c_712]) ).
cnf(c_713,plain,
~ product(e_2,e_5,e_1),
inference(resolve,[status(thm)],[c_62,c_598]) ).
cnf(c_650,plain,
$false,
inference(resolve,[status(thm)],[c_617,c_713]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP125-2.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n009.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Fri Sep 25 14:25:59 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.17/0.42 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.42 % Process 1805574 was started by sandbox2 on n009,
% 0.17/0.42 % Fri Sep 25 14:25:59 2026
% 0.17/0.42 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/0.43
% 0.17/0.43 % From the command line: assign(max_seconds, 300).
% 0.17/0.54
% 0.17/0.54 % SZS status Unsatisfiable for theBenchmark
% 0.17/0.54
% 0.17/0.54 % Proof 1 at 0.07 (+ 0.02) seconds.
% 0.17/0.54 % Length of proof is 142.
% 0.17/0.54 % Level of proof is 16.
% 0.17/0.54 % Maximum clause weight is 29.000.
% 0.17/0.54 % Given clauses 283.
% 0.17/0.54
% 0.17/0.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------