%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP129-2.004 : 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 : n020.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:52 AM UTC 2026
% Result : Unsatisfiable 2.06s 0.70s
% Output : CNFRefutation 2.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 99
% Number of leaves : 21
% Syntax : Number of formulae : 235 ( 53 unt; 0 def)
% Number of atoms : 862 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 752 ( 125 ~; 627 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 89 ( 0 sgn 21 !; 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_2_then_e_3,axiom,
next(e_2,e_3),
file('theBenchmark.p',e_2_then_e_3) ).
cnf(c_3,plain,
next(e_2,e_3),
inference(clausify,[status(thm)],[e_2_then_e_3]) ).
fof(e_1_then_e_2,axiom,
next(e_1,e_2),
file('theBenchmark.p',e_1_then_e_2) ).
cnf(c_4,plain,
next(e_1,e_2),
inference(clausify,[status(thm)],[e_1_then_e_2]) ).
fof(e_4_greater_e_3,axiom,
greater(e_4,e_3),
file('theBenchmark.p',e_4_greater_e_3) ).
cnf(c_5,plain,
greater(e_4,e_3),
inference(clausify,[status(thm)],[e_4_greater_e_3]) ).
cnf(c_7,plain,
( ~ greater(A,e_3)
| ~ product(e_2,e_1,A) ),
inference(resolve,[status(thm)],[c_1,c_3]) ).
cnf(c_8,plain,
( ~ greater(A,e_2)
| ~ product(e_1,e_1,A) ),
inference(resolve,[status(thm)],[c_1,c_4]) ).
fof(e_4_greater_e_2,axiom,
greater(e_4,e_2),
file('theBenchmark.p',e_4_greater_e_2) ).
cnf(c_9,plain,
greater(e_4,e_2),
inference(clausify,[status(thm)],[e_4_greater_e_2]) ).
fof(e_3_greater_e_2,axiom,
greater(e_3,e_2),
file('theBenchmark.p',e_3_greater_e_2) ).
cnf(c_10,plain,
greater(e_3,e_2),
inference(clausify,[status(thm)],[e_3_greater_e_2]) ).
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_14,plain,
( equalish(C,D)
| ~ product(A,B,D)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[product_total_function2]) ).
fof(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3),
file('theBenchmark.p',e_4_is_not_e_3) ).
cnf(c_15,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_16,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_17,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_19,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_20,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_23,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_27,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_28,plain,
( equalish(A,D)
| ~ product(D,B,C)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[product_left_cancellation]) ).
cnf(c_29,plain,
( ~ product(e_1,A,B)
| ~ product(e_2,A,B) ),
inference(resolve,[status(thm)],[c_28,c_23]) ).
cnf(c_30,plain,
( ~ product(e_1,A,B)
| ~ product(e_3,A,B) ),
inference(resolve,[status(thm)],[c_28,c_20]) ).
cnf(c_31,plain,
( ~ product(e_2,A,B)
| ~ product(e_3,A,B) ),
inference(resolve,[status(thm)],[c_28,c_19]) ).
cnf(c_32,plain,
( ~ product(e_1,A,B)
| ~ product(e_4,A,B) ),
inference(resolve,[status(thm)],[c_28,c_17]) ).
cnf(c_33,plain,
( ~ product(e_2,A,B)
| ~ product(e_4,A,B) ),
inference(resolve,[status(thm)],[c_28,c_16]) ).
cnf(c_34,plain,
( ~ product(e_3,A,B)
| ~ product(e_4,A,B) ),
inference(resolve,[status(thm)],[c_28,c_15]) ).
cnf(c_35,plain,
( ~ product(A,e_1,B)
| ~ product(A,e_2,B) ),
inference(resolve,[status(thm)],[c_27,c_23]) ).
cnf(c_36,plain,
( ~ product(A,e_1,B)
| ~ product(A,e_3,B) ),
inference(resolve,[status(thm)],[c_27,c_20]) ).
cnf(c_38,plain,
( ~ product(A,e_1,B)
| ~ product(A,e_4,B) ),
inference(resolve,[status(thm)],[c_27,c_17]) ).
cnf(c_39,plain,
( ~ product(A,e_2,B)
| ~ product(A,e_4,B) ),
inference(resolve,[status(thm)],[c_27,c_16]) ).
cnf(c_45,plain,
( ~ product(A,B,e_2)
| ~ product(A,B,e_4) ),
inference(resolve,[status(thm)],[c_14,c_16]) ).
fof(qg3,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( product(VAR_2,VAR_0,VAR_3)
| ~ product(VAR_1,VAR_2,VAR_3)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',qg3) ).
cnf(c_47,plain,
( product(C,A,D)
| ~ product(B,C,D)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[qg3]) ).
fof(product_total_function1,axiom,
! [VAR_0,VAR_1] :
( 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_48,plain,
( 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_4,axiom,
group_element(e_4),
file('theBenchmark.p',element_4) ).
cnf(c_49,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_50,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_51,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_52,plain,
group_element(e_1),
inference(clausify,[status(thm)],[element_1]) ).
cnf(c_53,plain,
~ product(e_2,e_1,e_4),
inference(resolve,[status(thm)],[c_5,c_7]) ).
cnf(c_54,plain,
~ product(e_1,e_1,e_4),
inference(resolve,[status(thm)],[c_9,c_8]) ).
cnf(c_55,plain,
~ product(e_1,e_1,e_3),
inference(resolve,[status(thm)],[c_10,c_8]) ).
cnf(c_56,plain,
( product(A,A,e_4)
| product(A,A,e_3)
| product(A,A,e_2)
| product(A,A,e_1)
| ~ group_element(A) ),
inference(factor,[status(thm)],[c_48]) ).
cnf(c_57,plain,
( product(A,e_4,e_4)
| product(A,e_4,e_3)
| product(A,e_4,e_2)
| product(A,e_4,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_49,c_48]) ).
cnf(c_58,plain,
( 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_49,c_48]) ).
cnf(c_60,plain,
( 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_50,c_48]) ).
cnf(c_61,plain,
( 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_51,c_48]) ).
cnf(c_62,plain,
( 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_51,c_48]) ).
cnf(c_1647,plain,
( product(e_1,e_1,e_4)
| product(e_1,e_1,e_3)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_1) ),
inference(resolve,[status(thm)],[c_56,c_52]) ).
cnf(c_1648,plain,
( product(e_1,e_1,e_4)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_1) ),
inference(resolve,[status(thm)],[c_55,c_1647]) ).
cnf(c_65,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_1,e_1) ),
inference(resolve,[status(thm)],[c_54,c_1648]) ).
cnf(c_66,plain,
( product(e_2,e_2,e_4)
| product(e_2,e_2,e_3)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_1) ),
inference(resolve,[status(thm)],[c_56,c_51]) ).
cnf(c_68,plain,
( product(e_4,e_4,e_4)
| product(e_4,e_4,e_3)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_1) ),
inference(resolve,[status(thm)],[c_56,c_49]) ).
cnf(c_69,plain,
( product(e_1,e_4,e_4)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_57,c_52]) ).
cnf(c_72,plain,
( 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_58,c_52]) ).
cnf(c_75,plain,
( product(e_1,A,e_2)
| ~ product(A,e_1,e_1)
| product(e_1,e_1,e_1) ),
inference(resolve,[status(thm)],[c_65,c_47]) ).
cnf(c_77,plain,
( product(e_2,A,e_4)
| ~ product(A,e_2,e_2)
| product(e_2,e_2,e_3)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_1) ),
inference(resolve,[status(thm)],[c_66,c_47]) ).
cnf(c_92,plain,
( ~ product(e_1,e_4,e_4)
| product(e_4,e_4,e_3)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_1) ),
inference(resolve,[status(thm)],[c_68,c_32]) ).
cnf(c_95,plain,
( 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_60,c_52]) ).
cnf(c_97,plain,
( product(e_4,A,e_4)
| ~ product(A,e_1,e_4)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_69,c_47]) ).
cnf(c_98,plain,
( product(e_4,e_1,A)
| ~ product(e_4,e_4,A)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_69,c_47]) ).
cnf(c_113,plain,
( product(e_1,A,e_4)
| ~ product(A,e_4,e_1)
| 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_72,c_47]) ).
cnf(c_114,plain,
( product(e_4,e_4,A)
| ~ product(e_1,e_4,A)
| 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_72,c_47]) ).
cnf(c_129,plain,
( 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_61,c_52]) ).
cnf(c_1649,plain,
( 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_62,c_52]) ).
cnf(c_130,plain,
( 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_53,c_1649]) ).
cnf(c_138,plain,
( product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1)
| product(e_4,e_4,e_3)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_1) ),
inference(resolve,[status(thm)],[c_92,c_69]) ).
cnf(c_151,plain,
( product(e_4,e_3,A)
| ~ product(e_1,e_4,A)
| 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_95,c_47]) ).
cnf(c_167,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_4,e_4,e_4)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_97,c_72]) ).
cnf(c_189,plain,
( product(e_2,A,e_4)
| ~ product(A,e_1,e_2)
| 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_129,c_47]) ).
cnf(c_190,plain,
( product(e_4,e_1,A)
| ~ product(e_2,e_4,A)
| 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_129,c_47]) ).
cnf(c_254,plain,
( ~ product(e_4,e_1,e_3)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_1) ),
inference(resolve,[status(thm)],[c_138,c_38]) ).
cnf(c_343,plain,
( ~ 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)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_167,c_38]) ).
cnf(c_1650,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_343,c_72]) ).
cnf(c_1651,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1650]) ).
cnf(c_1652,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1651]) ).
cnf(c_569,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1652]) ).
cnf(c_1653,plain,
( product(e_4,e_4,e_3)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_569,c_114]) ).
cnf(c_1654,plain,
( product(e_4,e_4,e_3)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1653]) ).
cnf(c_1655,plain,
( product(e_4,e_4,e_3)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1654]) ).
cnf(c_610,plain,
( product(e_4,e_4,e_3)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1655]) ).
cnf(c_1656,plain,
( product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_569,c_254]) ).
cnf(c_1657,plain,
( product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1656]) ).
cnf(c_1658,plain,
( product(e_1,e_4,e_3)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1657]) ).
cnf(c_615,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1658]) ).
cnf(c_663,plain,
( ~ product(e_1,e_4,e_3)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_610,c_32]) ).
cnf(c_1659,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_663,c_569]) ).
cnf(c_1660,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1659]) ).
cnf(c_1661,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1660]) ).
cnf(c_1662,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1661]) ).
cnf(c_1663,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1662]) ).
cnf(c_706,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1663]) ).
cnf(c_709,plain,
( ~ product(e_3,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_706,c_34]) ).
cnf(c_710,plain,
( ~ product(e_2,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_706,c_33]) ).
cnf(c_712,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_710,c_130]) ).
cnf(c_1664,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_712,c_114]) ).
cnf(c_1665,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1664]) ).
cnf(c_722,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1665]) ).
cnf(c_727,plain,
( ~ product(e_1,e_1,e_2)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_712,c_38]) ).
cnf(c_735,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_727,c_65]) ).
cnf(c_740,plain,
( ~ product(e_1,e_1,e_2)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_735,c_32]) ).
cnf(c_1666,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_740,c_65]) ).
cnf(c_746,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1666]) ).
cnf(c_1667,plain,
( product(e_1,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)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_1) ),
inference(resolve,[status(thm)],[c_746,c_113]) ).
cnf(c_1668,plain,
( product(e_1,e_1,e_4)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_1) ),
inference(copy,[status(thm)],[c_1667]) ).
cnf(c_748,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_1) ),
inference(resolve,[status(thm)],[c_54,c_1668]) ).
cnf(c_1669,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_746,c_75]) ).
cnf(c_752,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1669]) ).
cnf(c_761,plain,
( ~ product(e_1,e_1,e_2)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_752,c_38]) ).
cnf(c_1670,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_1,e_4,e_1) ),
inference(resolve,[status(thm)],[c_761,c_65]) ).
cnf(c_764,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_1,e_4,e_1) ),
inference(copy,[status(thm)],[c_1670]) ).
cnf(c_767,plain,
( product(e_1,e_1,A)
| ~ product(e_4,e_1,A)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_764,c_47]) ).
cnf(c_769,plain,
( ~ product(e_4,e_1,e_1)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(factor,[status(thm)],[c_767]) ).
cnf(c_1671,plain,
( product(e_1,e_1,e_3)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_1) ),
inference(resolve,[status(thm)],[c_748,c_767]) ).
cnf(c_1672,plain,
( product(e_1,e_1,e_3)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_4,e_1,e_2)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_1) ),
inference(copy,[status(thm)],[c_1671]) ).
cnf(c_1673,plain,
( product(e_1,e_1,e_3)
| product(e_1,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_1) ),
inference(copy,[status(thm)],[c_1672]) ).
cnf(c_1674,plain,
( product(e_1,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_1) ),
inference(copy,[status(thm)],[c_1673]) ).
cnf(c_770,plain,
( product(e_4,e_1,e_2)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_1) ),
inference(resolve,[status(thm)],[c_55,c_1674]) ).
cnf(c_775,plain,
( ~ product(e_1,e_1,e_2)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_1) ),
inference(resolve,[status(thm)],[c_770,c_32]) ).
cnf(c_1675,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_1) ),
inference(resolve,[status(thm)],[c_775,c_65]) ).
cnf(c_776,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_1) ),
inference(copy,[status(thm)],[c_1675]) ).
cnf(c_1676,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_776,c_769]) ).
cnf(c_1677,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(copy,[status(thm)],[c_1676]) ).
cnf(c_1678,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(copy,[status(thm)],[c_1677]) ).
cnf(c_777,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(copy,[status(thm)],[c_1678]) ).
cnf(c_781,plain,
( ~ product(e_1,e_1,e_2)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_777,c_29]) ).
cnf(c_1679,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_781,c_65]) ).
cnf(c_782,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_1) ),
inference(copy,[status(thm)],[c_1679]) ).
cnf(c_1680,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_1) ),
inference(resolve,[status(thm)],[c_782,c_75]) ).
cnf(c_783,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_1,e_1) ),
inference(copy,[status(thm)],[c_1680]) ).
cnf(c_791,plain,
( ~ product(e_1,e_1,e_2)
| product(e_1,e_1,e_1) ),
inference(resolve,[status(thm)],[c_783,c_35]) ).
cnf(c_1681,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_1) ),
inference(resolve,[status(thm)],[c_791,c_65]) ).
cnf(c_795,plain,
product(e_1,e_1,e_1),
inference(copy,[status(thm)],[c_1681]) ).
cnf(c_798,plain,
~ product(e_1,e_4,e_1),
inference(resolve,[status(thm)],[c_38,c_795]) ).
cnf(c_800,plain,
~ product(e_1,e_2,e_1),
inference(resolve,[status(thm)],[c_35,c_795]) ).
cnf(c_801,plain,
~ product(e_4,e_1,e_1),
inference(resolve,[status(thm)],[c_32,c_795]) ).
cnf(c_802,plain,
~ product(e_3,e_1,e_1),
inference(resolve,[status(thm)],[c_30,c_795]) ).
cnf(c_803,plain,
~ product(e_2,e_1,e_1),
inference(resolve,[status(thm)],[c_29,c_795]) ).
cnf(c_1682,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1) ),
inference(resolve,[status(thm)],[c_798,c_722]) ).
cnf(c_1683,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_801,c_1682]) ).
cnf(c_814,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_803,c_1683]) ).
cnf(c_1684,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2) ),
inference(resolve,[status(thm)],[c_798,c_712]) ).
cnf(c_1685,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_1,e_4,e_2) ),
inference(resolve,[status(thm)],[c_801,c_1684]) ).
cnf(c_815,plain,
( product(e_2,e_1,e_2)
| product(e_4,e_1,e_2)
| product(e_1,e_4,e_2) ),
inference(resolve,[status(thm)],[c_803,c_1685]) ).
cnf(c_1686,plain,
( ~ product(e_3,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2) ),
inference(resolve,[status(thm)],[c_798,c_709]) ).
cnf(c_817,plain,
( ~ product(e_3,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_1,e_4,e_2) ),
inference(resolve,[status(thm)],[c_801,c_1686]) ).
cnf(c_1687,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_2) ),
inference(resolve,[status(thm)],[c_798,c_706]) ).
cnf(c_820,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_1,e_4,e_2) ),
inference(resolve,[status(thm)],[c_801,c_1687]) ).
cnf(c_1688,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2) ),
inference(resolve,[status(thm)],[c_798,c_615]) ).
cnf(c_821,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_1)
| product(e_4,e_1,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2) ),
inference(resolve,[status(thm)],[c_801,c_1688]) ).
cnf(c_874,plain,
( product(e_4,e_1,A)
| ~ product(e_4,e_4,A)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2) ),
inference(resolve,[status(thm)],[c_798,c_98]) ).
cnf(c_935,plain,
( product(e_4,e_1,A)
| ~ product(e_2,e_4,A)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2) ),
inference(resolve,[status(thm)],[c_800,c_190]) ).
cnf(c_936,plain,
( product(e_2,A,e_4)
| ~ product(A,e_1,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2) ),
inference(resolve,[status(thm)],[c_800,c_189]) ).
cnf(c_940,plain,
( 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_800,c_129]) ).
cnf(c_994,plain,
( product(e_4,e_3,A)
| ~ product(e_1,e_4,A)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_2) ),
inference(resolve,[status(thm)],[c_802,c_151]) ).
cnf(c_1003,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_2) ),
inference(resolve,[status(thm)],[c_803,c_130]) ).
cnf(c_1052,plain,
( ~ product(e_1,e_4,e_2)
| product(e_4,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_814,c_32]) ).
cnf(c_1689,plain,
( product(e_4,e_1,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_4,e_4,e_1)
| product(e_4,e_1,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2) ),
inference(resolve,[status(thm)],[c_821,c_874]) ).
cnf(c_1690,plain,
( product(e_4,e_1,e_2)
| product(e_1,e_4,e_3)
| product(e_4,e_4,e_1)
| product(e_4,e_1,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2) ),
inference(copy,[status(thm)],[c_1689]) ).
cnf(c_1691,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_4,e_1)
| product(e_4,e_1,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2) ),
inference(copy,[status(thm)],[c_1690]) ).
cnf(c_1091,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_1,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2) ),
inference(copy,[status(thm)],[c_1691]) ).
cnf(c_1692,plain,
( product(e_2,e_1,e_2)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_1052,c_815]) ).
cnf(c_1693,plain,
( product(e_2,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_4,e_1,e_2) ),
inference(copy,[status(thm)],[c_1692]) ).
cnf(c_1093,plain,
( product(e_4,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_4,e_1,e_2) ),
inference(copy,[status(thm)],[c_1693]) ).
cnf(c_1105,plain,
( ~ product(e_2,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_1093,c_33]) ).
cnf(c_1694,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_2)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_1105,c_1003]) ).
cnf(c_1106,plain,
( product(e_2,e_1,e_2)
| product(e_4,e_1,e_2) ),
inference(copy,[status(thm)],[c_1694]) ).
cnf(c_1119,plain,
( product(e_2,e_4,e_4)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_2,e_1,e_2) ),
inference(resolve,[status(thm)],[c_1106,c_936]) ).
cnf(c_1126,plain,
( product(e_2,e_4,A)
| ~ product(e_1,e_2,A)
| product(e_2,e_1,e_2) ),
inference(resolve,[status(thm)],[c_1106,c_47]) ).
cnf(c_1695,plain,
( product(e_4,e_1,e_1)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_4,e_1,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2) ),
inference(resolve,[status(thm)],[c_1091,c_874]) ).
cnf(c_1696,plain,
( product(e_4,e_1,e_1)
| product(e_1,e_4,e_3)
| product(e_4,e_1,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2) ),
inference(copy,[status(thm)],[c_1695]) ).
cnf(c_1697,plain,
( product(e_4,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2) ),
inference(copy,[status(thm)],[c_1696]) ).
cnf(c_1128,plain,
( product(e_4,e_1,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2) ),
inference(resolve,[status(thm)],[c_801,c_1697]) ).
cnf(c_1129,plain,
( product(e_4,e_3,e_3)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_2)
| product(e_4,e_1,e_2)
| product(e_1,e_4,e_2) ),
inference(resolve,[status(thm)],[c_1128,c_994]) ).
cnf(c_1698,plain,
( product(e_4,e_1,e_4)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_2,e_1,e_2) ),
inference(resolve,[status(thm)],[c_1119,c_935]) ).
cnf(c_1699,plain,
( product(e_4,e_1,e_4)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_2,e_1,e_2) ),
inference(copy,[status(thm)],[c_1698]) ).
cnf(c_1153,plain,
( product(e_4,e_1,e_4)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_2,e_1,e_2) ),
inference(copy,[status(thm)],[c_1699]) ).
cnf(c_1167,plain,
( ~ product(e_4,e_1,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_2,e_1,e_2) ),
inference(resolve,[status(thm)],[c_1153,c_45]) ).
cnf(c_1700,plain,
( product(e_2,e_1,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_2,e_1,e_2) ),
inference(resolve,[status(thm)],[c_1167,c_1106]) ).
cnf(c_1172,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_2,e_1,e_2) ),
inference(copy,[status(thm)],[c_1700]) ).
cnf(c_1701,plain,
( product(e_2,e_4,e_3)
| product(e_2,e_1,e_2)
| product(e_1,e_2,e_2)
| product(e_2,e_1,e_2) ),
inference(resolve,[status(thm)],[c_1172,c_1126]) ).
cnf(c_1173,plain,
( product(e_2,e_4,e_3)
| product(e_1,e_2,e_2)
| product(e_2,e_1,e_2) ),
inference(copy,[status(thm)],[c_1701]) ).
cnf(c_1195,plain,
( ~ product(e_2,e_1,e_3)
| product(e_1,e_2,e_2)
| product(e_2,e_1,e_2) ),
inference(resolve,[status(thm)],[c_1173,c_38]) ).
cnf(c_1702,plain,
( product(e_2,e_1,e_2)
| product(e_1,e_2,e_2)
| product(e_2,e_1,e_2) ),
inference(resolve,[status(thm)],[c_1195,c_1003]) ).
cnf(c_1197,plain,
( product(e_1,e_2,e_2)
| product(e_2,e_1,e_2) ),
inference(copy,[status(thm)],[c_1702]) ).
cnf(c_1703,plain,
( product(e_2,e_2,e_4)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_2) ),
inference(resolve,[status(thm)],[c_1197,c_936]) ).
cnf(c_1198,plain,
( product(e_2,e_2,e_4)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2) ),
inference(copy,[status(thm)],[c_1703]) ).
cnf(c_1200,plain,
( product(e_2,e_2,A)
| ~ product(e_1,e_2,A)
| product(e_1,e_2,e_2) ),
inference(resolve,[status(thm)],[c_1197,c_47]) ).
cnf(c_1222,plain,
( ~ 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_1198,c_29]) ).
cnf(c_1704,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2) ),
inference(resolve,[status(thm)],[c_1222,c_940]) ).
cnf(c_1705,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2) ),
inference(copy,[status(thm)],[c_1704]) ).
cnf(c_1225,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_2) ),
inference(copy,[status(thm)],[c_1705]) ).
cnf(c_1706,plain,
( product(e_2,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_2) ),
inference(resolve,[status(thm)],[c_1225,c_1200]) ).
cnf(c_1226,plain,
( product(e_2,e_2,e_3)
| product(e_1,e_2,e_2) ),
inference(copy,[status(thm)],[c_1706]) ).
cnf(c_1240,plain,
( ~ product(e_1,e_2,e_3)
| product(e_1,e_2,e_2) ),
inference(resolve,[status(thm)],[c_1226,c_29]) ).
cnf(c_1707,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_2) ),
inference(resolve,[status(thm)],[c_1240,c_1225]) ).
cnf(c_1241,plain,
product(e_1,e_2,e_2),
inference(copy,[status(thm)],[c_1707]) ).
cnf(c_1708,plain,
( product(e_2,e_1,e_4)
| product(e_2,e_2,e_3)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_1) ),
inference(resolve,[status(thm)],[c_1241,c_77]) ).
cnf(c_1243,plain,
( product(e_2,e_2,e_3)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_1) ),
inference(resolve,[status(thm)],[c_53,c_1708]) ).
cnf(c_1709,plain,
( product(e_2,e_1,A)
| ~ product(e_2,e_2,A) ),
inference(resolve,[status(thm)],[c_47,c_1241]) ).
cnf(c_1246,plain,
~ product(e_2,e_2,e_1),
inference(resolve,[status(thm)],[c_1709,c_803]) ).
cnf(c_1250,plain,
~ product(e_1,e_4,e_2),
inference(resolve,[status(thm)],[c_39,c_1241]) ).
cnf(c_1254,plain,
~ product(e_2,e_2,e_2),
inference(resolve,[status(thm)],[c_29,c_1241]) ).
cnf(c_1710,plain,
( product(e_2,e_2,e_3)
| product(e_2,e_2,e_2) ),
inference(resolve,[status(thm)],[c_1246,c_1243]) ).
cnf(c_1255,plain,
product(e_2,e_2,e_3),
inference(resolve,[status(thm)],[c_1254,c_1710]) ).
cnf(c_1279,plain,
( product(e_4,e_3,e_3)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_2)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_1250,c_1129]) ).
cnf(c_1339,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_1250,c_820]) ).
cnf(c_1342,plain,
( ~ product(e_3,e_1,e_3)
| product(e_4,e_1,e_2) ),
inference(resolve,[status(thm)],[c_1250,c_817]) ).
cnf(c_1450,plain,
~ product(e_2,e_1,e_3),
inference(resolve,[status(thm)],[c_1255,c_35]) ).
cnf(c_1455,plain,
product(e_2,e_1,e_2),
inference(resolve,[status(thm)],[c_1450,c_1003]) ).
cnf(c_1554,plain,
~ product(e_4,e_1,e_2),
inference(resolve,[status(thm)],[c_33,c_1455]) ).
cnf(c_1555,plain,
~ product(e_3,e_1,e_2),
inference(resolve,[status(thm)],[c_31,c_1455]) ).
cnf(c_1609,plain,
~ product(e_3,e_1,e_3),
inference(resolve,[status(thm)],[c_1554,c_1342]) ).
cnf(c_1612,plain,
product(e_4,e_1,e_3),
inference(resolve,[status(thm)],[c_1554,c_1339]) ).
cnf(c_1711,plain,
( product(e_4,e_3,e_3)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_2) ),
inference(resolve,[status(thm)],[c_1554,c_1279]) ).
cnf(c_1712,plain,
( product(e_4,e_3,e_3)
| product(e_3,e_1,e_3) ),
inference(resolve,[status(thm)],[c_1555,c_1711]) ).
cnf(c_1617,plain,
product(e_4,e_3,e_3),
inference(resolve,[status(thm)],[c_1609,c_1712]) ).
cnf(c_1713,plain,
~ product(e_4,e_3,e_3),
inference(resolve,[status(thm)],[c_36,c_1612]) ).
cnf(c_1646,plain,
$false,
inference(resolve,[status(thm)],[c_1617,c_1713]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP129-2.004 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n020.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 14:29:33 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.36 % Process 3122761 was started by sandbox on n020,
% 0.13/0.36 % Fri Sep 25 14:29:33 2026
% 0.13/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/0.36
% 0.13/0.36 % From the command line: assign(max_seconds, 300).
% 2.06/0.70
% 2.06/0.70 % given #500 (W,wt=22): 710 product(e_1,e_4,e_1) | product(e_1,e_4,e_2) | product(e_4,e_1,e_1) | product(e_4,e_1,e_2) | -product(e_2,e_1,e_3). [resolve(706,e,33,a)].
% 2.06/0.70
% 2.06/0.70 % SZS status Unsatisfiable for theBenchmark
% 2.06/0.70
% 2.06/0.70 % Proof 1 at 0.27 (+ 0.05) seconds.
% 2.06/0.70 % Length of proof is 147.
% 2.06/0.70 % Level of proof is 55.
% 2.06/0.70 % Maximum clause weight is 30.000.
% 2.06/0.70 % Given clauses 737.
% 2.06/0.70
% 2.06/0.70 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------