%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP127-2.006 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:41 AM UTC 2026
% Result : Unsatisfiable 2.37s 0.68s
% Output : CNFRefutation 2.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 37
% Syntax : Number of formulae : 359 ( 140 unt; 0 def)
% Number of atoms : 889 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 785 ( 255 ~; 530 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 140 ( 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_4_then_e_5,axiom,
next(e_4,e_5),
file('theBenchmark.p',e_4_then_e_5) ).
cnf(c_3,plain,
next(e_4,e_5),
inference(clausify,[status(thm)],[e_4_then_e_5]) ).
fof(e_3_then_e_4,axiom,
next(e_3,e_4),
file('theBenchmark.p',e_3_then_e_4) ).
cnf(c_4,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_5,plain,
next(e_2,e_3),
inference(clausify,[status(thm)],[e_2_then_e_3]) ).
fof(e_6_greater_e_5,axiom,
greater(e_6,e_5),
file('theBenchmark.p',e_6_greater_e_5) ).
cnf(c_7,plain,
greater(e_6,e_5),
inference(clausify,[status(thm)],[e_6_greater_e_5]) ).
cnf(c_9,plain,
( ~ greater(A,e_5)
| ~ product(e_4,e_1,A) ),
inference(resolve,[status(thm)],[c_1,c_3]) ).
cnf(c_10,plain,
( ~ greater(A,e_4)
| ~ product(e_3,e_1,A) ),
inference(resolve,[status(thm)],[c_1,c_4]) ).
cnf(c_11,plain,
( ~ greater(A,e_3)
| ~ product(e_2,e_1,A) ),
inference(resolve,[status(thm)],[c_1,c_5]) ).
fof(e_6_greater_e_4,axiom,
greater(e_6,e_4),
file('theBenchmark.p',e_6_greater_e_4) ).
cnf(c_13,plain,
greater(e_6,e_4),
inference(clausify,[status(thm)],[e_6_greater_e_4]) ).
fof(e_5_greater_e_4,axiom,
greater(e_5,e_4),
file('theBenchmark.p',e_5_greater_e_4) ).
cnf(c_14,plain,
greater(e_5,e_4),
inference(clausify,[status(thm)],[e_5_greater_e_4]) ).
fof(e_6_greater_e_3,axiom,
greater(e_6,e_3),
file('theBenchmark.p',e_6_greater_e_3) ).
cnf(c_15,plain,
greater(e_6,e_3),
inference(clausify,[status(thm)],[e_6_greater_e_3]) ).
fof(e_5_greater_e_3,axiom,
greater(e_5,e_3),
file('theBenchmark.p',e_5_greater_e_3) ).
cnf(c_16,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_17,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_27,plain,
( equalish(C,D)
| ~ product(A,B,D)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[product_total_function2]) ).
fof(e_6_is_not_e_5,axiom,
~ equalish(e_6,e_5),
file('theBenchmark.p',e_6_is_not_e_5) ).
cnf(c_28,plain,
~ equalish(e_6,e_5),
inference(clausify,[status(thm)],[e_6_is_not_e_5]) ).
fof(e_6_is_not_e_4,axiom,
~ equalish(e_6,e_4),
file('theBenchmark.p',e_6_is_not_e_4) ).
cnf(c_29,plain,
~ equalish(e_6,e_4),
inference(clausify,[status(thm)],[e_6_is_not_e_4]) ).
fof(e_6_is_not_e_3,axiom,
~ equalish(e_6,e_3),
file('theBenchmark.p',e_6_is_not_e_3) ).
cnf(c_30,plain,
~ equalish(e_6,e_3),
inference(clausify,[status(thm)],[e_6_is_not_e_3]) ).
fof(e_6_is_not_e_2,axiom,
~ equalish(e_6,e_2),
file('theBenchmark.p',e_6_is_not_e_2) ).
cnf(c_31,plain,
~ equalish(e_6,e_2),
inference(clausify,[status(thm)],[e_6_is_not_e_2]) ).
fof(e_6_is_not_e_1,axiom,
~ equalish(e_6,e_1),
file('theBenchmark.p',e_6_is_not_e_1) ).
cnf(c_32,plain,
~ equalish(e_6,e_1),
inference(clausify,[status(thm)],[e_6_is_not_e_1]) ).
fof(e_5_is_not_e_4,axiom,
~ equalish(e_5,e_4),
file('theBenchmark.p',e_5_is_not_e_4) ).
cnf(c_34,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_35,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_36,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_37,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_40,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_41,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_42,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_46,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_47,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_52,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_58,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_59,plain,
( equalish(A,D)
| ~ product(D,B,C)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[product_left_cancellation]) ).
cnf(c_60,plain,
( ~ product(e_1,A,B)
| ~ product(e_2,A,B) ),
inference(resolve,[status(thm)],[c_59,c_52]) ).
cnf(c_61,plain,
( ~ product(e_1,A,B)
| ~ product(e_3,A,B) ),
inference(resolve,[status(thm)],[c_59,c_47]) ).
cnf(c_62,plain,
( ~ product(e_2,A,B)
| ~ product(e_3,A,B) ),
inference(resolve,[status(thm)],[c_59,c_46]) ).
cnf(c_63,plain,
( ~ product(e_1,A,B)
| ~ product(e_4,A,B) ),
inference(resolve,[status(thm)],[c_59,c_42]) ).
cnf(c_64,plain,
( ~ product(e_2,A,B)
| ~ product(e_4,A,B) ),
inference(resolve,[status(thm)],[c_59,c_41]) ).
cnf(c_65,plain,
( ~ product(e_3,A,B)
| ~ product(e_4,A,B) ),
inference(resolve,[status(thm)],[c_59,c_40]) ).
cnf(c_66,plain,
( ~ product(e_1,A,B)
| ~ product(e_5,A,B) ),
inference(resolve,[status(thm)],[c_59,c_37]) ).
cnf(c_67,plain,
( ~ product(e_2,A,B)
| ~ product(e_5,A,B) ),
inference(resolve,[status(thm)],[c_59,c_36]) ).
cnf(c_68,plain,
( ~ product(e_3,A,B)
| ~ product(e_5,A,B) ),
inference(resolve,[status(thm)],[c_59,c_35]) ).
cnf(c_70,plain,
( ~ product(e_1,A,B)
| ~ product(e_6,A,B) ),
inference(resolve,[status(thm)],[c_59,c_32]) ).
cnf(c_71,plain,
( ~ product(e_2,A,B)
| ~ product(e_6,A,B) ),
inference(resolve,[status(thm)],[c_59,c_31]) ).
cnf(c_72,plain,
( ~ product(e_3,A,B)
| ~ product(e_6,A,B) ),
inference(resolve,[status(thm)],[c_59,c_30]) ).
cnf(c_73,plain,
( ~ product(e_4,A,B)
| ~ product(e_6,A,B) ),
inference(resolve,[status(thm)],[c_59,c_29]) ).
cnf(c_74,plain,
( ~ product(e_5,A,B)
| ~ product(e_6,A,B) ),
inference(resolve,[status(thm)],[c_59,c_28]) ).
cnf(c_75,plain,
( ~ product(A,e_1,B)
| ~ product(A,e_2,B) ),
inference(resolve,[status(thm)],[c_58,c_52]) ).
cnf(c_76,plain,
( ~ product(A,e_1,B)
| ~ product(A,e_3,B) ),
inference(resolve,[status(thm)],[c_58,c_47]) ).
cnf(c_77,plain,
( ~ product(A,e_2,B)
| ~ product(A,e_3,B) ),
inference(resolve,[status(thm)],[c_58,c_46]) ).
cnf(c_78,plain,
( ~ product(A,e_1,B)
| ~ product(A,e_4,B) ),
inference(resolve,[status(thm)],[c_58,c_42]) ).
cnf(c_80,plain,
( ~ product(A,e_3,B)
| ~ product(A,e_4,B) ),
inference(resolve,[status(thm)],[c_58,c_40]) ).
cnf(c_81,plain,
( ~ product(A,e_1,B)
| ~ product(A,e_5,B) ),
inference(resolve,[status(thm)],[c_58,c_37]) ).
cnf(c_82,plain,
( ~ product(A,e_2,B)
| ~ product(A,e_5,B) ),
inference(resolve,[status(thm)],[c_58,c_36]) ).
cnf(c_83,plain,
( ~ product(A,e_3,B)
| ~ product(A,e_5,B) ),
inference(resolve,[status(thm)],[c_58,c_35]) ).
cnf(c_85,plain,
( ~ product(A,e_1,B)
| ~ product(A,e_6,B) ),
inference(resolve,[status(thm)],[c_58,c_32]) ).
cnf(c_86,plain,
( ~ product(A,e_2,B)
| ~ product(A,e_6,B) ),
inference(resolve,[status(thm)],[c_58,c_31]) ).
cnf(c_87,plain,
( ~ product(A,e_3,B)
| ~ product(A,e_6,B) ),
inference(resolve,[status(thm)],[c_58,c_30]) ).
cnf(c_88,plain,
( ~ product(A,e_4,B)
| ~ product(A,e_6,B) ),
inference(resolve,[status(thm)],[c_58,c_29]) ).
cnf(c_89,plain,
( ~ product(A,e_5,B)
| ~ product(A,e_6,B) ),
inference(resolve,[status(thm)],[c_58,c_28]) ).
cnf(c_95,plain,
( ~ product(A,B,e_3)
| ~ product(A,B,e_4) ),
inference(resolve,[status(thm)],[c_27,c_40]) ).
cnf(c_97,plain,
( ~ product(A,B,e_2)
| ~ product(A,B,e_5) ),
inference(resolve,[status(thm)],[c_27,c_36]) ).
cnf(c_99,plain,
( ~ product(A,B,e_4)
| ~ product(A,B,e_5) ),
inference(resolve,[status(thm)],[c_27,c_34]) ).
fof(qg3,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( product(VAR_3,VAR_0,VAR_1)
| ~ product(VAR_2,VAR_0,VAR_3)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',qg3) ).
cnf(c_105,plain,
( product(D,A,B)
| ~ product(C,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_106,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_6)
| 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_107,plain,
( product(A,B,e_6)
| 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_6,axiom,
group_element(e_6),
file('theBenchmark.p',element_6) ).
cnf(c_108,plain,
group_element(e_6),
inference(clausify,[status(thm)],[element_6]) ).
fof(element_5,axiom,
group_element(e_5),
file('theBenchmark.p',element_5) ).
cnf(c_109,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_110,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_111,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_112,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_113,plain,
group_element(e_1),
inference(clausify,[status(thm)],[element_1]) ).
cnf(c_114,plain,
~ product(e_4,e_1,e_6),
inference(resolve,[status(thm)],[c_7,c_9]) ).
cnf(c_115,plain,
~ product(e_3,e_1,e_6),
inference(resolve,[status(thm)],[c_13,c_10]) ).
cnf(c_116,plain,
~ product(e_3,e_1,e_5),
inference(resolve,[status(thm)],[c_14,c_10]) ).
cnf(c_117,plain,
~ product(e_2,e_1,e_6),
inference(resolve,[status(thm)],[c_15,c_11]) ).
cnf(c_118,plain,
~ product(e_2,e_1,e_5),
inference(resolve,[status(thm)],[c_16,c_11]) ).
cnf(c_119,plain,
~ product(e_2,e_1,e_4),
inference(resolve,[status(thm)],[c_17,c_11]) ).
cnf(c_142,plain,
~ product(e_6,e_5,e_6),
inference(resolve,[status(thm)],[c_106,c_89]) ).
cnf(c_143,plain,
~ product(e_6,e_4,e_6),
inference(resolve,[status(thm)],[c_106,c_88]) ).
cnf(c_144,plain,
~ product(e_6,e_3,e_6),
inference(resolve,[status(thm)],[c_106,c_87]) ).
cnf(c_146,plain,
~ product(e_6,e_1,e_6),
inference(resolve,[status(thm)],[c_106,c_85]) ).
cnf(c_150,plain,
~ product(e_5,e_1,e_5),
inference(resolve,[status(thm)],[c_106,c_81]) ).
cnf(c_153,plain,
~ product(e_4,e_1,e_4),
inference(resolve,[status(thm)],[c_106,c_78]) ).
cnf(c_154,plain,
~ product(e_3,e_2,e_3),
inference(resolve,[status(thm)],[c_106,c_77]) ).
cnf(c_155,plain,
~ product(e_3,e_1,e_3),
inference(resolve,[status(thm)],[c_106,c_76]) ).
cnf(c_156,plain,
~ product(e_2,e_1,e_2),
inference(resolve,[status(thm)],[c_106,c_75]) ).
cnf(c_159,plain,
~ product(e_3,e_6,e_6),
inference(resolve,[status(thm)],[c_106,c_72]) ).
cnf(c_160,plain,
~ product(e_2,e_6,e_6),
inference(resolve,[status(thm)],[c_106,c_71]) ).
cnf(c_161,plain,
~ product(e_1,e_6,e_6),
inference(resolve,[status(thm)],[c_106,c_70]) ).
cnf(c_165,plain,
~ product(e_1,e_5,e_5),
inference(resolve,[status(thm)],[c_106,c_66]) ).
cnf(c_170,plain,
~ product(e_1,e_3,e_3),
inference(resolve,[status(thm)],[c_106,c_61]) ).
cnf(c_171,plain,
~ product(e_1,e_2,e_2),
inference(resolve,[status(thm)],[c_106,c_60]) ).
cnf(c_184,plain,
~ product(e_4,e_6,e_4),
inference(resolve,[status(thm)],[c_88,c_106]) ).
cnf(c_185,plain,
~ product(e_3,e_6,e_3),
inference(resolve,[status(thm)],[c_87,c_106]) ).
cnf(c_186,plain,
~ product(e_2,e_6,e_2),
inference(resolve,[status(thm)],[c_86,c_106]) ).
cnf(c_187,plain,
~ product(e_1,e_6,e_1),
inference(resolve,[status(thm)],[c_85,c_106]) ).
cnf(c_191,plain,
~ product(e_1,e_5,e_1),
inference(resolve,[status(thm)],[c_81,c_106]) ).
cnf(c_196,plain,
~ product(e_1,e_3,e_1),
inference(resolve,[status(thm)],[c_76,c_106]) ).
cnf(c_197,plain,
~ product(e_1,e_2,e_1),
inference(resolve,[status(thm)],[c_75,c_106]) ).
cnf(c_198,plain,
~ product(e_6,e_5,e_5),
inference(resolve,[status(thm)],[c_74,c_106]) ).
cnf(c_199,plain,
~ product(e_6,e_4,e_4),
inference(resolve,[status(thm)],[c_73,c_106]) ).
cnf(c_200,plain,
~ product(e_6,e_3,e_3),
inference(resolve,[status(thm)],[c_72,c_106]) ).
cnf(c_202,plain,
~ product(e_6,e_1,e_1),
inference(resolve,[status(thm)],[c_70,c_106]) ).
cnf(c_206,plain,
~ product(e_5,e_1,e_1),
inference(resolve,[status(thm)],[c_66,c_106]) ).
cnf(c_209,plain,
~ product(e_4,e_1,e_1),
inference(resolve,[status(thm)],[c_63,c_106]) ).
cnf(c_210,plain,
~ product(e_3,e_2,e_2),
inference(resolve,[status(thm)],[c_62,c_106]) ).
cnf(c_211,plain,
~ product(e_3,e_1,e_1),
inference(resolve,[status(thm)],[c_61,c_106]) ).
cnf(c_212,plain,
~ product(e_2,e_1,e_1),
inference(resolve,[status(thm)],[c_60,c_106]) ).
cnf(c_213,plain,
( product(A,e_6,e_6)
| product(A,e_6,e_5)
| product(A,e_6,e_4)
| product(A,e_6,e_3)
| product(A,e_6,e_2)
| product(A,e_6,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_108,c_107]) ).
cnf(c_214,plain,
( product(e_6,A,e_6)
| product(e_6,A,e_5)
| product(e_6,A,e_4)
| product(e_6,A,e_3)
| product(e_6,A,e_2)
| product(e_6,A,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_108,c_107]) ).
cnf(c_215,plain,
( product(A,e_5,e_6)
| product(A,e_5,e_5)
| product(A,e_5,e_4)
| product(A,e_5,e_3)
| product(A,e_5,e_2)
| product(A,e_5,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_109,c_107]) ).
cnf(c_216,plain,
( product(e_5,A,e_6)
| 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_109,c_107]) ).
cnf(c_218,plain,
( product(e_4,A,e_6)
| 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_110,c_107]) ).
cnf(c_219,plain,
( product(A,e_3,e_6)
| product(A,e_3,e_5)
| product(A,e_3,e_4)
| product(A,e_3,e_3)
| product(A,e_3,e_2)
| product(A,e_3,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_111,c_107]) ).
cnf(c_220,plain,
( product(e_3,A,e_6)
| 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_111,c_107]) ).
cnf(c_221,plain,
( product(A,e_2,e_6)
| product(A,e_2,e_5)
| product(A,e_2,e_4)
| product(A,e_2,e_3)
| product(A,e_2,e_2)
| product(A,e_2,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_112,c_107]) ).
cnf(c_222,plain,
( product(e_2,A,e_6)
| 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_112,c_107]) ).
cnf(c_2415,plain,
( product(e_1,e_6,e_6)
| product(e_1,e_6,e_5)
| product(e_1,e_6,e_4)
| product(e_1,e_6,e_3)
| product(e_1,e_6,e_2)
| product(e_1,e_6,e_1) ),
inference(resolve,[status(thm)],[c_213,c_113]) ).
cnf(c_2416,plain,
( product(e_1,e_6,e_6)
| product(e_1,e_6,e_5)
| product(e_1,e_6,e_4)
| product(e_1,e_6,e_3)
| product(e_1,e_6,e_2) ),
inference(resolve,[status(thm)],[c_187,c_2415]) ).
cnf(c_225,plain,
( product(e_1,e_6,e_5)
| product(e_1,e_6,e_4)
| product(e_1,e_6,e_3)
| product(e_1,e_6,e_2) ),
inference(resolve,[status(thm)],[c_161,c_2416]) ).
cnf(c_2417,plain,
( product(e_2,e_6,e_6)
| product(e_2,e_6,e_5)
| product(e_2,e_6,e_4)
| product(e_2,e_6,e_3)
| product(e_2,e_6,e_2)
| product(e_2,e_6,e_1) ),
inference(resolve,[status(thm)],[c_213,c_112]) ).
cnf(c_2418,plain,
( product(e_2,e_6,e_6)
| product(e_2,e_6,e_5)
| product(e_2,e_6,e_4)
| product(e_2,e_6,e_3)
| product(e_2,e_6,e_1) ),
inference(resolve,[status(thm)],[c_186,c_2417]) ).
cnf(c_226,plain,
( product(e_2,e_6,e_5)
| product(e_2,e_6,e_4)
| product(e_2,e_6,e_3)
| product(e_2,e_6,e_1) ),
inference(resolve,[status(thm)],[c_160,c_2418]) ).
cnf(c_2419,plain,
( product(e_3,e_6,e_6)
| product(e_3,e_6,e_5)
| product(e_3,e_6,e_4)
| product(e_3,e_6,e_3)
| product(e_3,e_6,e_2)
| product(e_3,e_6,e_1) ),
inference(resolve,[status(thm)],[c_213,c_111]) ).
cnf(c_2420,plain,
( product(e_3,e_6,e_6)
| product(e_3,e_6,e_5)
| product(e_3,e_6,e_4)
| product(e_3,e_6,e_2)
| product(e_3,e_6,e_1) ),
inference(resolve,[status(thm)],[c_185,c_2419]) ).
cnf(c_227,plain,
( product(e_3,e_6,e_5)
| product(e_3,e_6,e_4)
| product(e_3,e_6,e_2)
| product(e_3,e_6,e_1) ),
inference(resolve,[status(thm)],[c_159,c_2420]) ).
cnf(c_236,plain,
( product(A,e_1,e_6)
| ~ product(e_3,e_1,A)
| product(e_1,e_6,e_5)
| product(e_1,e_6,e_4)
| product(e_1,e_6,e_2) ),
inference(resolve,[status(thm)],[c_225,c_105]) ).
cnf(c_265,plain,
( ~ product(e_1,e_6,e_4)
| product(e_2,e_6,e_5)
| product(e_2,e_6,e_3)
| product(e_2,e_6,e_1) ),
inference(resolve,[status(thm)],[c_226,c_60]) ).
cnf(c_294,plain,
( ~ product(e_2,e_6,e_5)
| product(e_3,e_6,e_4)
| product(e_3,e_6,e_2)
| product(e_3,e_6,e_1) ),
inference(resolve,[status(thm)],[c_227,c_62]) ).
cnf(c_358,plain,
( product(e_1,e_6,e_5)
| product(e_1,e_6,e_3)
| product(e_1,e_6,e_2)
| product(e_2,e_6,e_5)
| product(e_2,e_6,e_3)
| product(e_2,e_6,e_1) ),
inference(resolve,[status(thm)],[c_265,c_225]) ).
cnf(c_2421,plain,
( product(e_6,e_1,e_6)
| product(e_6,e_1,e_5)
| product(e_6,e_1,e_4)
| product(e_6,e_1,e_3)
| product(e_6,e_1,e_2)
| product(e_6,e_1,e_1) ),
inference(resolve,[status(thm)],[c_214,c_113]) ).
cnf(c_2422,plain,
( product(e_6,e_1,e_6)
| product(e_6,e_1,e_5)
| product(e_6,e_1,e_4)
| product(e_6,e_1,e_3)
| product(e_6,e_1,e_2) ),
inference(resolve,[status(thm)],[c_202,c_2421]) ).
cnf(c_362,plain,
( product(e_6,e_1,e_5)
| product(e_6,e_1,e_4)
| product(e_6,e_1,e_3)
| product(e_6,e_1,e_2) ),
inference(resolve,[status(thm)],[c_146,c_2422]) ).
cnf(c_2423,plain,
( product(e_6,e_3,e_6)
| product(e_6,e_3,e_5)
| product(e_6,e_3,e_4)
| product(e_6,e_3,e_3)
| product(e_6,e_3,e_2)
| product(e_6,e_3,e_1) ),
inference(resolve,[status(thm)],[c_214,c_111]) ).
cnf(c_2424,plain,
( product(e_6,e_3,e_6)
| product(e_6,e_3,e_5)
| product(e_6,e_3,e_4)
| product(e_6,e_3,e_2)
| product(e_6,e_3,e_1) ),
inference(resolve,[status(thm)],[c_200,c_2423]) ).
cnf(c_364,plain,
( product(e_6,e_3,e_5)
| product(e_6,e_3,e_4)
| product(e_6,e_3,e_2)
| product(e_6,e_3,e_1) ),
inference(resolve,[status(thm)],[c_144,c_2424]) ).
cnf(c_2425,plain,
( product(e_6,e_4,e_6)
| product(e_6,e_4,e_5)
| product(e_6,e_4,e_4)
| product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1) ),
inference(resolve,[status(thm)],[c_214,c_110]) ).
cnf(c_2426,plain,
( product(e_6,e_4,e_6)
| product(e_6,e_4,e_5)
| product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1) ),
inference(resolve,[status(thm)],[c_199,c_2425]) ).
cnf(c_365,plain,
( product(e_6,e_4,e_5)
| product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1) ),
inference(resolve,[status(thm)],[c_143,c_2426]) ).
cnf(c_2427,plain,
( product(e_6,e_5,e_6)
| product(e_6,e_5,e_5)
| product(e_6,e_5,e_4)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1) ),
inference(resolve,[status(thm)],[c_214,c_109]) ).
cnf(c_2428,plain,
( product(e_6,e_5,e_6)
| product(e_6,e_5,e_4)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1) ),
inference(resolve,[status(thm)],[c_198,c_2427]) ).
cnf(c_366,plain,
( product(e_6,e_5,e_4)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1) ),
inference(resolve,[status(thm)],[c_142,c_2428]) ).
cnf(c_2429,plain,
( product(e_1,e_5,e_6)
| product(e_1,e_5,e_5)
| product(e_1,e_5,e_4)
| product(e_1,e_5,e_3)
| product(e_1,e_5,e_2)
| product(e_1,e_5,e_1) ),
inference(resolve,[status(thm)],[c_215,c_113]) ).
cnf(c_2430,plain,
( product(e_1,e_5,e_6)
| product(e_1,e_5,e_5)
| product(e_1,e_5,e_4)
| product(e_1,e_5,e_3)
| product(e_1,e_5,e_2) ),
inference(resolve,[status(thm)],[c_191,c_2429]) ).
cnf(c_367,plain,
( product(e_1,e_5,e_6)
| product(e_1,e_5,e_4)
| product(e_1,e_5,e_3)
| product(e_1,e_5,e_2) ),
inference(resolve,[status(thm)],[c_165,c_2430]) ).
cnf(c_2431,plain,
( product(e_5,e_1,e_6)
| 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_216,c_113]) ).
cnf(c_2432,plain,
( product(e_5,e_1,e_6)
| 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_206,c_2431]) ).
cnf(c_371,plain,
( product(e_5,e_1,e_6)
| 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_150,c_2432]) ).
cnf(c_377,plain,
( product(e_2,e_6,e_4)
| product(e_2,e_6,e_3)
| product(e_2,e_6,e_1)
| product(e_3,e_6,e_4)
| product(e_3,e_6,e_2)
| product(e_3,e_6,e_1) ),
inference(resolve,[status(thm)],[c_294,c_226]) ).
cnf(c_2433,plain,
( product(e_4,e_1,e_6)
| product(e_4,e_1,e_5)
| product(e_4,e_1,e_4)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1) ),
inference(resolve,[status(thm)],[c_218,c_113]) ).
cnf(c_2434,plain,
( product(e_4,e_1,e_6)
| product(e_4,e_1,e_5)
| product(e_4,e_1,e_4)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_209,c_2433]) ).
cnf(c_2435,plain,
( product(e_4,e_1,e_6)
| product(e_4,e_1,e_5)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_153,c_2434]) ).
cnf(c_382,plain,
( product(e_4,e_1,e_5)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_114,c_2435]) ).
cnf(c_2436,plain,
( product(e_1,e_3,e_6)
| 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_219,c_113]) ).
cnf(c_2437,plain,
( product(e_1,e_3,e_6)
| 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_196,c_2436]) ).
cnf(c_385,plain,
( product(e_1,e_3,e_6)
| 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_170,c_2437]) ).
cnf(c_387,plain,
( product(e_2,e_1,A)
| ~ product(e_1,A,e_4)
| product(e_4,e_1,e_5)
| product(e_4,e_1,e_3) ),
inference(resolve,[status(thm)],[c_382,c_105]) ).
cnf(c_389,plain,
( ~ product(e_3,e_1,e_2)
| product(e_4,e_1,e_5)
| product(e_4,e_1,e_3) ),
inference(resolve,[status(thm)],[c_382,c_65]) ).
cnf(c_393,plain,
( product(e_5,e_1,A)
| ~ product(e_1,A,e_4)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_382,c_105]) ).
cnf(c_2438,plain,
( product(e_3,e_1,e_6)
| 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_220,c_113]) ).
cnf(c_2439,plain,
( product(e_3,e_1,e_6)
| 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_211,c_2438]) ).
cnf(c_2440,plain,
( product(e_3,e_1,e_6)
| 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_155,c_2439]) ).
cnf(c_2441,plain,
( product(e_3,e_1,e_6)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_2) ),
inference(resolve,[status(thm)],[c_116,c_2440]) ).
cnf(c_395,plain,
( product(e_3,e_1,e_4)
| product(e_3,e_1,e_2) ),
inference(resolve,[status(thm)],[c_115,c_2441]) ).
cnf(c_2442,plain,
( product(e_3,e_2,e_6)
| 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_220,c_112]) ).
cnf(c_2443,plain,
( product(e_3,e_2,e_6)
| 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_210,c_2442]) ).
cnf(c_396,plain,
( product(e_3,e_2,e_6)
| 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_154,c_2443]) ).
cnf(c_2444,plain,
( product(e_1,e_2,e_6)
| 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_221,c_113]) ).
cnf(c_2445,plain,
( product(e_1,e_2,e_6)
| 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_197,c_2444]) ).
cnf(c_397,plain,
( product(e_1,e_2,e_6)
| 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_171,c_2445]) ).
cnf(c_2446,plain,
( product(e_2,e_1,e_6)
| 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_222,c_113]) ).
cnf(c_2447,plain,
( product(e_2,e_1,e_6)
| 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_212,c_2446]) ).
cnf(c_2448,plain,
( product(e_2,e_1,e_6)
| 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_156,c_2447]) ).
cnf(c_2449,plain,
( product(e_2,e_1,e_6)
| product(e_2,e_1,e_5)
| product(e_2,e_1,e_3) ),
inference(resolve,[status(thm)],[c_119,c_2448]) ).
cnf(c_2450,plain,
( product(e_2,e_1,e_6)
| product(e_2,e_1,e_3) ),
inference(resolve,[status(thm)],[c_118,c_2449]) ).
cnf(c_398,plain,
product(e_2,e_1,e_3),
inference(resolve,[status(thm)],[c_117,c_2450]) ).
cnf(c_402,plain,
( product(A,e_2,e_1)
| ~ product(e_3,e_2,A) ),
inference(resolve,[status(thm)],[c_398,c_105]) ).
cnf(c_2451,plain,
( product(e_3,e_1,A)
| ~ product(e_1,A,e_2) ),
inference(resolve,[status(thm)],[c_105,c_398]) ).
cnf(c_403,plain,
~ product(e_1,e_3,e_2),
inference(resolve,[status(thm)],[c_2451,c_155]) ).
cnf(c_2452,plain,
( product(e_3,e_1,A)
| ~ product(e_1,A,e_2) ),
inference(resolve,[status(thm)],[c_105,c_398]) ).
cnf(c_404,plain,
~ product(e_1,e_5,e_2),
inference(resolve,[status(thm)],[c_2452,c_116]) ).
cnf(c_2453,plain,
( product(e_3,e_1,A)
| ~ product(e_1,A,e_2) ),
inference(resolve,[status(thm)],[c_105,c_398]) ).
cnf(c_405,plain,
~ product(e_1,e_6,e_2),
inference(resolve,[status(thm)],[c_2453,c_115]) ).
cnf(c_2454,plain,
( product(A,e_2,e_1)
| ~ product(e_3,e_2,A) ),
inference(resolve,[status(thm)],[c_105,c_398]) ).
cnf(c_406,plain,
~ product(e_3,e_2,e_1),
inference(resolve,[status(thm)],[c_2454,c_197]) ).
cnf(c_407,plain,
~ product(e_2,e_6,e_3),
inference(resolve,[status(thm)],[c_85,c_398]) ).
cnf(c_410,plain,
~ product(e_6,e_1,e_3),
inference(resolve,[status(thm)],[c_71,c_398]) ).
cnf(c_411,plain,
~ product(e_5,e_1,e_3),
inference(resolve,[status(thm)],[c_67,c_398]) ).
cnf(c_412,plain,
~ product(e_4,e_1,e_3),
inference(resolve,[status(thm)],[c_64,c_398]) ).
cnf(c_413,plain,
( product(e_1,e_3,e_6)
| product(e_1,e_3,e_5)
| product(e_1,e_3,e_4) ),
inference(resolve,[status(thm)],[c_403,c_385]) ).
cnf(c_414,plain,
( product(e_1,e_5,e_6)
| product(e_1,e_5,e_4)
| product(e_1,e_5,e_3) ),
inference(resolve,[status(thm)],[c_404,c_367]) ).
cnf(c_2455,plain,
( product(e_1,e_6,e_5)
| product(e_1,e_6,e_3)
| product(e_1,e_6,e_2)
| product(e_2,e_6,e_5)
| product(e_2,e_6,e_1) ),
inference(resolve,[status(thm)],[c_407,c_358]) ).
cnf(c_418,plain,
( product(e_1,e_6,e_5)
| product(e_1,e_6,e_3)
| product(e_2,e_6,e_5)
| product(e_2,e_6,e_1) ),
inference(resolve,[status(thm)],[c_405,c_2455]) ).
cnf(c_432,plain,
( product(A,e_1,e_6)
| ~ product(e_3,e_1,A)
| product(e_1,e_6,e_5)
| product(e_1,e_6,e_4) ),
inference(resolve,[status(thm)],[c_405,c_236]) ).
cnf(c_434,plain,
( product(e_1,e_6,e_5)
| product(e_1,e_6,e_4)
| product(e_1,e_6,e_3) ),
inference(resolve,[status(thm)],[c_405,c_225]) ).
cnf(c_435,plain,
( product(e_3,e_2,e_6)
| product(e_3,e_2,e_5)
| product(e_3,e_2,e_4) ),
inference(resolve,[status(thm)],[c_406,c_396]) ).
cnf(c_436,plain,
( product(e_2,e_6,e_4)
| product(e_2,e_6,e_1)
| product(e_3,e_6,e_4)
| product(e_3,e_6,e_2)
| product(e_3,e_6,e_1) ),
inference(resolve,[status(thm)],[c_407,c_377]) ).
cnf(c_456,plain,
( product(e_6,e_1,e_5)
| product(e_6,e_1,e_4)
| product(e_6,e_1,e_2) ),
inference(resolve,[status(thm)],[c_410,c_362]) ).
cnf(c_457,plain,
( product(e_5,e_1,e_6)
| product(e_5,e_1,e_4)
| product(e_5,e_1,e_2) ),
inference(resolve,[status(thm)],[c_411,c_371]) ).
cnf(c_459,plain,
( product(e_5,e_1,A)
| ~ product(e_1,A,e_4)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_412,c_393]) ).
cnf(c_460,plain,
( ~ product(e_3,e_1,e_2)
| product(e_4,e_1,e_5) ),
inference(resolve,[status(thm)],[c_412,c_389]) ).
cnf(c_462,plain,
( product(e_2,e_1,A)
| ~ product(e_1,A,e_4)
| product(e_4,e_1,e_5) ),
inference(resolve,[status(thm)],[c_412,c_387]) ).
cnf(c_464,plain,
( product(e_2,e_1,A)
| ~ product(e_1,A,e_3)
| product(e_3,e_1,e_4) ),
inference(resolve,[status(thm)],[c_395,c_105]) ).
cnf(c_467,plain,
( product(e_4,e_1,A)
| ~ product(e_1,A,e_3)
| product(e_3,e_1,e_2) ),
inference(resolve,[status(thm)],[c_395,c_105]) ).
cnf(c_469,plain,
( product(e_3,e_1,e_4)
| product(e_4,e_1,e_5) ),
inference(resolve,[status(thm)],[c_460,c_395]) ).
cnf(c_470,plain,
( product(e_5,e_1,A)
| ~ product(e_1,A,e_4)
| product(e_3,e_1,e_4) ),
inference(resolve,[status(thm)],[c_469,c_105]) ).
cnf(c_474,plain,
( product(e_4,e_1,A)
| ~ product(e_1,A,e_3)
| product(e_4,e_1,e_5) ),
inference(resolve,[status(thm)],[c_469,c_105]) ).
cnf(c_476,plain,
( ~ product(e_1,e_5,e_3)
| product(e_4,e_1,e_5) ),
inference(factor,[status(thm)],[c_474]) ).
cnf(c_489,plain,
( product(e_4,e_1,e_5)
| product(e_1,e_5,e_6)
| product(e_1,e_5,e_4) ),
inference(resolve,[status(thm)],[c_414,c_476]) ).
cnf(c_518,plain,
( product(e_6,e_2,e_1)
| product(e_3,e_2,e_5)
| product(e_3,e_2,e_4) ),
inference(resolve,[status(thm)],[c_435,c_402]) ).
cnf(c_565,plain,
( ~ product(e_3,e_1,e_4)
| product(e_6,e_1,e_5)
| product(e_6,e_1,e_2) ),
inference(resolve,[status(thm)],[c_456,c_72]) ).
cnf(c_575,plain,
( ~ product(e_3,e_1,e_4)
| product(e_5,e_1,e_6)
| product(e_5,e_1,e_2) ),
inference(resolve,[status(thm)],[c_457,c_68]) ).
cnf(c_2456,plain,
( product(e_1,e_5,e_6)
| product(e_1,e_5,e_3)
| product(e_5,e_1,e_5)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_459,c_414]) ).
cnf(c_579,plain,
( product(e_1,e_5,e_6)
| product(e_1,e_5,e_3)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_150,c_2456]) ).
cnf(c_2457,plain,
( product(e_1,e_3,e_6)
| product(e_1,e_3,e_5)
| product(e_5,e_1,e_3)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_459,c_413]) ).
cnf(c_580,plain,
( product(e_1,e_3,e_6)
| product(e_1,e_3,e_5)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_411,c_2457]) ).
cnf(c_2458,plain,
( product(e_1,e_6,e_5)
| product(e_1,e_6,e_4)
| product(e_4,e_1,e_6)
| product(e_3,e_1,e_2) ),
inference(resolve,[status(thm)],[c_467,c_434]) ).
cnf(c_591,plain,
( product(e_1,e_6,e_5)
| product(e_1,e_6,e_4)
| product(e_3,e_1,e_2) ),
inference(resolve,[status(thm)],[c_114,c_2458]) ).
cnf(c_2459,plain,
( product(e_1,e_3,e_6)
| product(e_1,e_3,e_5)
| product(e_5,e_1,e_3)
| product(e_3,e_1,e_4) ),
inference(resolve,[status(thm)],[c_470,c_413]) ).
cnf(c_594,plain,
( product(e_1,e_3,e_6)
| product(e_1,e_3,e_5)
| product(e_3,e_1,e_4) ),
inference(resolve,[status(thm)],[c_411,c_2459]) ).
cnf(c_2460,plain,
( product(e_2,e_1,e_5)
| product(e_4,e_1,e_5)
| product(e_4,e_1,e_5)
| product(e_1,e_5,e_6) ),
inference(resolve,[status(thm)],[c_489,c_462]) ).
cnf(c_2461,plain,
( product(e_2,e_1,e_5)
| product(e_4,e_1,e_5)
| product(e_1,e_5,e_6) ),
inference(copy,[status(thm)],[c_2460]) ).
cnf(c_598,plain,
( product(e_4,e_1,e_5)
| product(e_1,e_5,e_6) ),
inference(resolve,[status(thm)],[c_118,c_2461]) ).
cnf(c_609,plain,
( product(A,e_1,e_5)
| ~ product(e_6,e_1,A)
| product(e_4,e_1,e_5) ),
inference(resolve,[status(thm)],[c_598,c_105]) ).
cnf(c_616,plain,
( ~ product(e_4,e_1,e_2)
| product(e_1,e_5,e_6) ),
inference(resolve,[status(thm)],[c_598,c_97]) ).
cnf(c_617,plain,
( ~ product(e_6,e_1,e_4)
| product(e_4,e_1,e_5) ),
inference(factor,[status(thm)],[c_609]) ).
cnf(c_622,plain,
( product(e_6,e_1,e_5)
| product(e_6,e_1,e_2)
| product(e_4,e_1,e_5) ),
inference(resolve,[status(thm)],[c_617,c_456]) ).
cnf(c_667,plain,
( ~ product(e_1,e_2,e_5)
| product(e_6,e_2,e_1)
| product(e_3,e_2,e_4) ),
inference(resolve,[status(thm)],[c_518,c_61]) ).
cnf(c_2462,plain,
( product(e_1,e_5,e_6)
| product(e_1,e_5,e_6)
| product(e_1,e_5,e_3) ),
inference(resolve,[status(thm)],[c_579,c_616]) ).
cnf(c_700,plain,
( product(e_1,e_5,e_6)
| product(e_1,e_5,e_3) ),
inference(copy,[status(thm)],[c_2462]) ).
cnf(c_2463,plain,
( product(e_2,e_1,e_5)
| product(e_3,e_1,e_4)
| product(e_1,e_5,e_6) ),
inference(resolve,[status(thm)],[c_700,c_464]) ).
cnf(c_716,plain,
( product(e_3,e_1,e_4)
| product(e_1,e_5,e_6) ),
inference(resolve,[status(thm)],[c_118,c_2463]) ).
cnf(c_729,plain,
( ~ product(e_1,e_3,e_6)
| product(e_1,e_5,e_3) ),
inference(resolve,[status(thm)],[c_700,c_83]) ).
cnf(c_738,plain,
( ~ product(e_1,e_3,e_6)
| product(e_3,e_1,e_4) ),
inference(resolve,[status(thm)],[c_716,c_83]) ).
cnf(c_766,plain,
( product(e_1,e_5,e_3)
| product(e_1,e_3,e_5)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_580,c_729]) ).
cnf(c_771,plain,
( ~ product(e_1,e_2,e_6)
| product(e_1,e_3,e_5)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_580,c_77]) ).
cnf(c_2464,plain,
( product(e_3,e_1,e_4)
| product(e_1,e_3,e_5)
| product(e_3,e_1,e_4) ),
inference(resolve,[status(thm)],[c_594,c_738]) ).
cnf(c_881,plain,
( product(e_1,e_3,e_5)
| product(e_3,e_1,e_4) ),
inference(copy,[status(thm)],[c_2464]) ).
cnf(c_920,plain,
( product(e_6,e_1,e_5)
| product(e_6,e_1,e_2)
| product(e_1,e_3,e_5) ),
inference(resolve,[status(thm)],[c_881,c_565]) ).
cnf(c_937,plain,
( ~ product(e_6,e_2,e_1)
| product(e_6,e_3,e_5)
| product(e_6,e_3,e_4)
| product(e_6,e_3,e_2) ),
inference(resolve,[status(thm)],[c_364,c_77]) ).
cnf(c_997,plain,
( ~ product(e_6,e_3,e_5)
| product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1) ),
inference(resolve,[status(thm)],[c_365,c_80]) ).
cnf(c_1034,plain,
( ~ product(e_6,e_3,e_4)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1) ),
inference(resolve,[status(thm)],[c_366,c_83]) ).
cnf(c_2465,plain,
( product(e_2,e_1,e_5)
| product(e_4,e_1,e_5)
| product(e_6,e_1,e_5)
| product(e_4,e_1,e_5) ),
inference(resolve,[status(thm)],[c_622,c_609]) ).
cnf(c_2466,plain,
( product(e_2,e_1,e_5)
| product(e_6,e_1,e_5)
| product(e_4,e_1,e_5) ),
inference(copy,[status(thm)],[c_2465]) ).
cnf(c_1143,plain,
( product(e_6,e_1,e_5)
| product(e_4,e_1,e_5) ),
inference(resolve,[status(thm)],[c_118,c_2466]) ).
cnf(c_2467,plain,
( product(e_5,e_1,e_5)
| product(e_4,e_1,e_5)
| product(e_4,e_1,e_5) ),
inference(resolve,[status(thm)],[c_1143,c_609]) ).
cnf(c_2468,plain,
( product(e_5,e_1,e_5)
| product(e_4,e_1,e_5) ),
inference(copy,[status(thm)],[c_2467]) ).
cnf(c_1149,plain,
product(e_4,e_1,e_5),
inference(resolve,[status(thm)],[c_150,c_2468]) ).
cnf(c_1152,plain,
( product(e_5,e_1,A)
| ~ product(e_1,A,e_4) ),
inference(resolve,[status(thm)],[c_1149,c_105]) ).
cnf(c_1154,plain,
~ product(e_4,e_1,e_2),
inference(resolve,[status(thm)],[c_1149,c_97]) ).
cnf(c_1161,plain,
~ product(e_6,e_1,e_5),
inference(resolve,[status(thm)],[c_73,c_1149]) ).
cnf(c_1163,plain,
( ~ product(e_1,e_2,e_6)
| product(e_1,e_3,e_5) ),
inference(resolve,[status(thm)],[c_1154,c_771]) ).
cnf(c_1167,plain,
( product(e_1,e_5,e_3)
| product(e_1,e_3,e_5) ),
inference(resolve,[status(thm)],[c_1154,c_766]) ).
cnf(c_1173,plain,
( product(e_1,e_3,e_6)
| product(e_1,e_3,e_5) ),
inference(resolve,[status(thm)],[c_1154,c_580]) ).
cnf(c_1222,plain,
( product(e_6,e_1,e_2)
| product(e_1,e_3,e_5) ),
inference(resolve,[status(thm)],[c_1161,c_920]) ).
cnf(c_1318,plain,
( ~ product(e_1,e_2,e_3)
| product(e_1,e_3,e_5) ),
inference(resolve,[status(thm)],[c_1167,c_82]) ).
cnf(c_1507,plain,
( ~ product(e_2,e_6,e_4)
| product(e_1,e_6,e_5)
| product(e_1,e_6,e_3)
| product(e_2,e_6,e_1) ),
inference(resolve,[status(thm)],[c_418,c_99]) ).
cnf(c_2469,plain,
( product(e_1,e_6,e_5)
| product(e_1,e_6,e_4)
| product(e_2,e_1,e_6)
| product(e_1,e_6,e_5)
| product(e_1,e_6,e_4) ),
inference(resolve,[status(thm)],[c_432,c_591]) ).
cnf(c_2470,plain,
( product(e_1,e_6,e_5)
| product(e_2,e_1,e_6)
| product(e_1,e_6,e_5)
| product(e_1,e_6,e_4) ),
inference(copy,[status(thm)],[c_2469]) ).
cnf(c_2471,plain,
( product(e_2,e_1,e_6)
| product(e_1,e_6,e_5)
| product(e_1,e_6,e_4) ),
inference(copy,[status(thm)],[c_2470]) ).
cnf(c_1542,plain,
( product(e_1,e_6,e_5)
| product(e_1,e_6,e_4) ),
inference(resolve,[status(thm)],[c_117,c_2471]) ).
cnf(c_1549,plain,
( product(e_2,e_6,A)
| ~ product(e_6,A,e_3)
| product(e_2,e_6,e_4)
| product(e_2,e_6,e_1)
| product(e_3,e_6,e_4)
| product(e_3,e_6,e_1) ),
inference(resolve,[status(thm)],[c_436,c_105]) ).
cnf(c_1573,plain,
( ~ product(e_6,e_4,e_3)
| product(e_2,e_6,e_4)
| product(e_2,e_6,e_1)
| product(e_3,e_6,e_4)
| product(e_3,e_6,e_1) ),
inference(factor,[status(thm)],[c_1549]) ).
cnf(c_1578,plain,
( product(e_5,e_1,e_6)
| product(e_1,e_6,e_5) ),
inference(resolve,[status(thm)],[c_1542,c_1152]) ).
cnf(c_1584,plain,
( ~ product(e_1,e_6,e_3)
| product(e_1,e_6,e_5) ),
inference(resolve,[status(thm)],[c_1542,c_95]) ).
cnf(c_1585,plain,
( ~ product(e_1,e_2,e_4)
| product(e_1,e_6,e_5) ),
inference(resolve,[status(thm)],[c_1542,c_86]) ).
cnf(c_1668,plain,
( ~ product(e_1,e_3,e_5)
| product(e_5,e_1,e_6) ),
inference(resolve,[status(thm)],[c_1578,c_87]) ).
cnf(c_1674,plain,
( product(e_1,e_2,e_6)
| product(e_1,e_2,e_5)
| product(e_1,e_2,e_3)
| product(e_1,e_6,e_5) ),
inference(resolve,[status(thm)],[c_1585,c_397]) ).
cnf(c_1697,plain,
( product(e_6,e_1,e_2)
| product(e_5,e_1,e_6) ),
inference(resolve,[status(thm)],[c_1668,c_1222]) ).
cnf(c_1700,plain,
( product(e_3,e_1,e_4)
| product(e_5,e_1,e_6) ),
inference(resolve,[status(thm)],[c_1668,c_881]) ).
cnf(c_1792,plain,
( ~ product(e_5,e_1,e_2)
| product(e_5,e_1,e_6) ),
inference(resolve,[status(thm)],[c_1697,c_74]) ).
cnf(c_2472,plain,
( product(e_5,e_1,e_6)
| product(e_5,e_1,e_2)
| product(e_5,e_1,e_6) ),
inference(resolve,[status(thm)],[c_1700,c_575]) ).
cnf(c_1858,plain,
( product(e_5,e_1,e_2)
| product(e_5,e_1,e_6) ),
inference(copy,[status(thm)],[c_2472]) ).
cnf(c_2473,plain,
( product(e_5,e_1,e_6)
| product(e_5,e_1,e_6) ),
inference(resolve,[status(thm)],[c_1858,c_1792]) ).
cnf(c_1964,plain,
product(e_5,e_1,e_6),
inference(copy,[status(thm)],[c_2473]) ).
cnf(c_2474,plain,
( product(e_6,e_1,A)
| ~ product(e_1,A,e_5) ),
inference(resolve,[status(thm)],[c_105,c_1964]) ).
cnf(c_1971,plain,
~ product(e_1,e_3,e_5),
inference(resolve,[status(thm)],[c_2474,c_410]) ).
cnf(c_2475,plain,
( product(e_6,e_1,A)
| ~ product(e_1,A,e_5) ),
inference(resolve,[status(thm)],[c_105,c_1964]) ).
cnf(c_1972,plain,
~ product(e_1,e_6,e_5),
inference(resolve,[status(thm)],[c_2475,c_146]) ).
cnf(c_2476,plain,
( product(A,e_5,e_1)
| ~ product(e_6,e_5,A) ),
inference(resolve,[status(thm)],[c_105,c_1964]) ).
cnf(c_1973,plain,
~ product(e_6,e_5,e_1),
inference(resolve,[status(thm)],[c_2476,c_191]) ).
cnf(c_1987,plain,
~ product(e_1,e_2,e_3),
inference(resolve,[status(thm)],[c_1971,c_1318]) ).
cnf(c_1992,plain,
product(e_6,e_1,e_2),
inference(resolve,[status(thm)],[c_1971,c_1222]) ).
cnf(c_1993,plain,
product(e_1,e_3,e_6),
inference(resolve,[status(thm)],[c_1971,c_1173]) ).
cnf(c_1994,plain,
product(e_1,e_5,e_3),
inference(resolve,[status(thm)],[c_1971,c_1167]) ).
cnf(c_1998,plain,
~ product(e_1,e_2,e_6),
inference(resolve,[status(thm)],[c_1971,c_1163]) ).
cnf(c_2004,plain,
product(e_3,e_1,e_4),
inference(resolve,[status(thm)],[c_1971,c_881]) ).
cnf(c_2477,plain,
( product(e_1,e_2,e_6)
| product(e_1,e_2,e_5)
| product(e_1,e_2,e_3) ),
inference(resolve,[status(thm)],[c_1972,c_1674]) ).
cnf(c_2478,plain,
( product(e_1,e_2,e_6)
| product(e_1,e_2,e_5) ),
inference(resolve,[status(thm)],[c_1987,c_2477]) ).
cnf(c_2005,plain,
product(e_1,e_2,e_5),
inference(resolve,[status(thm)],[c_1998,c_2478]) ).
cnf(c_2007,plain,
~ product(e_1,e_6,e_3),
inference(resolve,[status(thm)],[c_1972,c_1584]) ).
cnf(c_2012,plain,
product(e_1,e_6,e_4),
inference(resolve,[status(thm)],[c_1972,c_1542]) ).
cnf(c_2479,plain,
( ~ product(e_2,e_6,e_4)
| product(e_1,e_6,e_5)
| product(e_2,e_6,e_1) ),
inference(resolve,[status(thm)],[c_2007,c_1507]) ).
cnf(c_2022,plain,
( ~ product(e_2,e_6,e_4)
| product(e_2,e_6,e_1) ),
inference(resolve,[status(thm)],[c_1972,c_2479]) ).
cnf(c_2058,plain,
( ~ product(e_6,e_3,e_4)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2) ),
inference(resolve,[status(thm)],[c_1973,c_1034]) ).
cnf(c_2120,plain,
( product(e_6,e_2,e_1)
| product(e_3,e_2,e_4) ),
inference(resolve,[status(thm)],[c_2005,c_667]) ).
cnf(c_2480,plain,
( product(A,e_6,e_1)
| ~ product(e_2,e_6,A) ),
inference(resolve,[status(thm)],[c_105,c_1992]) ).
cnf(c_2126,plain,
~ product(e_2,e_6,e_1),
inference(resolve,[status(thm)],[c_2480,c_187]) ).
cnf(c_2128,plain,
~ product(e_6,e_5,e_2),
inference(resolve,[status(thm)],[c_81,c_1992]) ).
cnf(c_2129,plain,
~ product(e_6,e_4,e_2),
inference(resolve,[status(thm)],[c_78,c_1992]) ).
cnf(c_2130,plain,
~ product(e_6,e_3,e_2),
inference(resolve,[status(thm)],[c_76,c_1992]) ).
cnf(c_2142,plain,
~ product(e_2,e_6,e_4),
inference(resolve,[status(thm)],[c_2126,c_2022]) ).
cnf(c_2481,plain,
( ~ product(e_6,e_4,e_3)
| product(e_2,e_6,e_4)
| product(e_3,e_6,e_4)
| product(e_3,e_6,e_1) ),
inference(resolve,[status(thm)],[c_2126,c_1573]) ).
cnf(c_2147,plain,
( ~ product(e_6,e_4,e_3)
| product(e_3,e_6,e_4)
| product(e_3,e_6,e_1) ),
inference(resolve,[status(thm)],[c_2142,c_2481]) ).
cnf(c_2162,plain,
( ~ product(e_6,e_3,e_4)
| product(e_6,e_5,e_3) ),
inference(resolve,[status(thm)],[c_2128,c_2058]) ).
cnf(c_2172,plain,
( ~ product(e_6,e_3,e_5)
| product(e_6,e_4,e_3)
| product(e_6,e_4,e_1) ),
inference(resolve,[status(thm)],[c_2129,c_997]) ).
cnf(c_2199,plain,
( ~ product(e_6,e_2,e_1)
| product(e_6,e_3,e_5)
| product(e_6,e_3,e_4) ),
inference(resolve,[status(thm)],[c_2130,c_937]) ).
cnf(c_2482,plain,
( product(e_6,e_3,A)
| ~ product(e_3,A,e_1) ),
inference(resolve,[status(thm)],[c_105,c_1993]) ).
cnf(c_2223,plain,
~ product(e_3,e_6,e_1),
inference(resolve,[status(thm)],[c_2482,c_144]) ).
cnf(c_2233,plain,
( ~ product(e_6,e_4,e_3)
| product(e_3,e_6,e_4) ),
inference(resolve,[status(thm)],[c_2223,c_2147]) ).
cnf(c_2250,plain,
~ product(e_6,e_5,e_3),
inference(resolve,[status(thm)],[c_70,c_1994]) ).
cnf(c_2266,plain,
~ product(e_6,e_3,e_4),
inference(resolve,[status(thm)],[c_2250,c_2162]) ).
cnf(c_2311,plain,
( ~ product(e_6,e_2,e_1)
| product(e_6,e_3,e_5) ),
inference(resolve,[status(thm)],[c_2266,c_2199]) ).
cnf(c_2324,plain,
~ product(e_3,e_6,e_4),
inference(resolve,[status(thm)],[c_85,c_2004]) ).
cnf(c_2325,plain,
~ product(e_3,e_2,e_4),
inference(resolve,[status(thm)],[c_75,c_2004]) ).
cnf(c_2329,plain,
~ product(e_6,e_4,e_3),
inference(resolve,[status(thm)],[c_2324,c_2233]) ).
cnf(c_2338,plain,
product(e_6,e_2,e_1),
inference(resolve,[status(thm)],[c_2325,c_2120]) ).
cnf(c_2353,plain,
( ~ product(e_6,e_3,e_5)
| product(e_6,e_4,e_1) ),
inference(resolve,[status(thm)],[c_2329,c_2172]) ).
cnf(c_2372,plain,
product(e_6,e_3,e_5),
inference(resolve,[status(thm)],[c_2338,c_2311]) ).
cnf(c_2374,plain,
product(e_6,e_4,e_1),
inference(resolve,[status(thm)],[c_2372,c_2353]) ).
cnf(c_2483,plain,
( product(e_4,e_6,A)
| ~ product(e_6,A,e_1) ),
inference(resolve,[status(thm)],[c_105,c_2012]) ).
cnf(c_2484,plain,
~ product(e_6,e_4,e_1),
inference(resolve,[status(thm)],[c_2483,c_184]) ).
cnf(c_2414,plain,
$false,
inference(resolve,[status(thm)],[c_2374,c_2484]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP127-2.006 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n018.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 25 14:29:35 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.35 % Process 2161003 was started by sandbox on n018,
% 0.08/0.35 % Fri Sep 25 14:29:35 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.36
% 0.08/0.36 % From the command line: assign(max_seconds, 300).
% 2.37/0.68
% 2.37/0.68 % given #500 (T,wt=13): 1668 product(e_5,e_1,e_6) | -product(e_1,e_3,e_5). [resolve(1578,a,87,a)].
% 2.37/0.68
% 2.37/0.68 % SZS status Unsatisfiable for theBenchmark
% 2.37/0.68
% 2.37/0.68 % Proof 1 at 0.22 (+ 0.08) seconds.
% 2.37/0.68 % Length of proof is 252.
% 2.37/0.68 % Level of proof is 31.
% 2.37/0.68 % Maximum clause weight is 33.000.
% 2.37/0.68 % Given clauses 578.
% 2.37/0.68
% 2.37/0.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------