%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP128-3.005 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n015.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 : Fri Sep 25 01:31:25 PM UTC 2026
% Result : Unsatisfiable 3.82s 1.14s
% Output : CNFRefutation 3.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 46
% Syntax : Number of formulae : 775 ( 73 unt; 0 def)
% Number of atoms : 2396 ( 0 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 3138 (1517 ~;1621 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 425 ( 0 sgn 425 !; 0 ?; 390 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
next(e_0,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_0_then_e_1) ).
fof(f3,axiom,
next(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_then_e_3) ).
fof(f4,axiom,
next(e_3,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_then_e_4) ).
fof(f5,axiom,
next(e_4,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_then_e_5) ).
fof(f6,axiom,
greater(e_1,e_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_greater_e_0) ).
fof(f7,axiom,
greater(e_2,e_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_greater_e_0) ).
fof(f8,axiom,
greater(e_3,e_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_greater_e_0) ).
fof(f9,axiom,
greater(e_4,e_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_greater_e_0) ).
fof(f16,axiom,
greater(e_4,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_greater_e_2) ).
fof(f18,axiom,
greater(e_4,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_greater_e_3) ).
fof(f22,axiom,
! [X0] :
( cycle(X0,e_4)
| cycle(X0,e_3)
| cycle(X0,e_2)
| cycle(X0,e_1)
| cycle(X0,e_0)
| ~ group_element(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle2) ).
fof(f23,axiom,
cycle(e_5,e_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle3) ).
fof(f24,axiom,
! [X2,X3,X0,X1,X4] :
( equalish(X1,X4)
| ~ next(X3,X4)
| ~ greater(X1,e_0)
| ~ next(X0,X2)
| ~ cycle(X2,X3)
| ~ cycle(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle4) ).
fof(f25,axiom,
! [X2,X3,X0,X1,X4] :
( ~ greater(X1,X4)
| ~ greater(X2,X0)
| ~ next(X2,X3)
| ~ cycle(X3,X4)
| ~ cycle(X2,e_0)
| ~ cycle(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle5) ).
fof(f26,axiom,
! [X0,X1] :
( ~ greater(X1,X0)
| ~ product(X0,e_1,X1)
| ~ cycle(X0,e_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle6) ).
fof(f27,axiom,
! [X2,X3,X0,X1] :
( equalish(X2,X3)
| ~ next(X0,X3)
| ~ greater(X1,e_0)
| ~ product(X0,e_1,X2)
| ~ cycle(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle7) ).
fof(f28,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
fof(f29,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
fof(f30,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
fof(f31,axiom,
group_element(e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_4) ).
fof(f32,axiom,
group_element(e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_5) ).
fof(f33,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f34,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f35,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
fof(f36,axiom,
~ equalish(e_1,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_5) ).
fof(f37,axiom,
~ equalish(e_2,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_1) ).
fof(f38,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f39,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
fof(f40,axiom,
~ equalish(e_2,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_5) ).
fof(f41,axiom,
~ equalish(e_3,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_1) ).
fof(f42,axiom,
~ equalish(e_3,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_2) ).
fof(f43,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
fof(f44,axiom,
~ equalish(e_3,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_5) ).
fof(f45,axiom,
~ equalish(e_4,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_1) ).
fof(f46,axiom,
~ equalish(e_4,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_2) ).
fof(f47,axiom,
~ equalish(e_4,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_3) ).
fof(f48,axiom,
~ equalish(e_4,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_5) ).
fof(f49,axiom,
~ equalish(e_5,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_is_not_e_1) ).
fof(f50,axiom,
~ equalish(e_5,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_is_not_e_2) ).
fof(f51,axiom,
~ equalish(e_5,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_is_not_e_3) ).
fof(f52,axiom,
~ equalish(e_5,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_is_not_e_4) ).
fof(f53,axiom,
! [X0,X1] :
( product(X0,X1,e_5)
| product(X0,X1,e_4)
| product(X0,X1,e_3)
| product(X0,X1,e_2)
| product(X0,X1,e_1)
| ~ group_element(X1)
| ~ group_element(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function1) ).
fof(f54,axiom,
! [X2,X3,X0,X1] :
( equalish(X2,X3)
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function2) ).
fof(f55,axiom,
! [X2,X3,X0,X1] :
( equalish(X1,X3)
| ~ product(X0,X3,X2)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_right_cancellation) ).
fof(f56,axiom,
! [X2,X3,X0,X1] :
( equalish(X0,X3)
| ~ product(X3,X1,X2)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_left_cancellation) ).
fof(f57,negated_conjecture,
! [X2,X3,X0,X1] :
( product(X0,X2,X3)
| ~ product(X2,X1,X3)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg3) ).
tcf(c_106,plain,
next(e_0,e_1),
inference(cnf_transformation,[],[f1]) ).
tcf(c_108,plain,
next(e_2,e_3),
inference(cnf_transformation,[],[f3]) ).
tcf(c_109,plain,
next(e_3,e_4),
inference(cnf_transformation,[],[f4]) ).
tcf(c_110,plain,
next(e_4,e_5),
inference(cnf_transformation,[],[f5]) ).
tcf(c_111,plain,
greater(e_1,e_0),
inference(cnf_transformation,[],[f6]) ).
tcf(c_112,plain,
greater(e_2,e_0),
inference(cnf_transformation,[],[f7]) ).
tcf(c_113,plain,
greater(e_3,e_0),
inference(cnf_transformation,[],[f8]) ).
tcf(c_114,plain,
greater(e_4,e_0),
inference(cnf_transformation,[],[f9]) ).
tcf(c_121,plain,
greater(e_4,e_2),
inference(cnf_transformation,[],[f16]) ).
tcf(c_123,plain,
greater(e_4,e_3),
inference(cnf_transformation,[],[f18]) ).
tcf(c_127,plain,
! [X0: $i] :
( cycle(X0,e_4)
| cycle(X0,e_3)
| cycle(X0,e_2)
| cycle(X0,e_1)
| cycle(X0,e_0)
| ~ group_element(X0) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_128,plain,
cycle(e_5,e_0),
inference(cnf_transformation,[],[f23]) ).
tcf(c_129,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( equalish(X4,X3)
| ~ greater(X4,e_0)
| ~ cycle(X1,X2)
| ~ cycle(X0,X4)
| ~ next(X2,X3)
| ~ next(X0,X1) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ~ cycle(X0,e_0)
| ~ cycle(X4,X2)
| ~ cycle(X1,X3)
| ~ greater(X2,X3)
| ~ greater(X0,X4)
| ~ next(X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i] :
( ~ cycle(X0,e_0)
| ~ greater(X1,X0)
| ~ product(X0,e_1,X1) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equalish(X1,X2)
| ~ greater(X3,e_0)
| ~ cycle(X0,X3)
| ~ next(X0,X2)
| ~ product(X0,e_1,X1) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_133,plain,
group_element(e_1),
inference(cnf_transformation,[],[f28]) ).
tcf(c_134,plain,
group_element(e_2),
inference(cnf_transformation,[],[f29]) ).
tcf(c_135,plain,
group_element(e_3),
inference(cnf_transformation,[],[f30]) ).
tcf(c_136,plain,
group_element(e_4),
inference(cnf_transformation,[],[f31]) ).
tcf(c_137,plain,
group_element(e_5),
inference(cnf_transformation,[],[f32]) ).
tcf(c_138,plain,
~ equalish(e_1,e_2),
inference(cnf_transformation,[],[f33]) ).
tcf(c_139,plain,
~ equalish(e_1,e_3),
inference(cnf_transformation,[],[f34]) ).
tcf(c_140,plain,
~ equalish(e_1,e_4),
inference(cnf_transformation,[],[f35]) ).
tcf(c_141,plain,
~ equalish(e_1,e_5),
inference(cnf_transformation,[],[f36]) ).
tcf(c_142,plain,
~ equalish(e_2,e_1),
inference(cnf_transformation,[],[f37]) ).
tcf(c_143,plain,
~ equalish(e_2,e_3),
inference(cnf_transformation,[],[f38]) ).
tcf(c_144,plain,
~ equalish(e_2,e_4),
inference(cnf_transformation,[],[f39]) ).
tcf(c_145,plain,
~ equalish(e_2,e_5),
inference(cnf_transformation,[],[f40]) ).
tcf(c_146,plain,
~ equalish(e_3,e_1),
inference(cnf_transformation,[],[f41]) ).
tcf(c_147,plain,
~ equalish(e_3,e_2),
inference(cnf_transformation,[],[f42]) ).
tcf(c_148,plain,
~ equalish(e_3,e_4),
inference(cnf_transformation,[],[f43]) ).
tcf(c_149,plain,
~ equalish(e_3,e_5),
inference(cnf_transformation,[],[f44]) ).
tcf(c_150,plain,
~ equalish(e_4,e_1),
inference(cnf_transformation,[],[f45]) ).
tcf(c_151,plain,
~ equalish(e_4,e_2),
inference(cnf_transformation,[],[f46]) ).
tcf(c_152,plain,
~ equalish(e_4,e_3),
inference(cnf_transformation,[],[f47]) ).
tcf(c_153,plain,
~ equalish(e_4,e_5),
inference(cnf_transformation,[],[f48]) ).
tcf(c_154,plain,
~ equalish(e_5,e_1),
inference(cnf_transformation,[],[f49]) ).
tcf(c_155,plain,
~ equalish(e_5,e_2),
inference(cnf_transformation,[],[f50]) ).
tcf(c_156,plain,
~ equalish(e_5,e_3),
inference(cnf_transformation,[],[f51]) ).
tcf(c_157,plain,
~ equalish(e_5,e_4),
inference(cnf_transformation,[],[f52]) ).
tcf(c_158,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,e_5)
| product(X1,X0,e_4)
| product(X1,X0,e_3)
| product(X1,X0,e_2)
| product(X1,X0,e_1)
| ~ group_element(X1)
| ~ group_element(X0) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_159,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equalish(X2,X3)
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_160,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equalish(X1,X3)
| ~ product(X0,X3,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_161,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equalish(X0,X3)
| ~ product(X3,X1,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_162,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( product(X0,X2,X3)
| ~ product(X2,X1,X3)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_168,plain,
( product(e_1,e_1,e_5)
| 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)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_158]) ).
tcf(c_173,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_2)
| ~ product(X0,X1,e_2)
| ~ product(X0,X1,e_1) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_175,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_2)
| ~ product(X0,e_2,X1)
| ~ product(X0,e_1,X1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_177,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_2)
| ~ product(e_2,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_185,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_3)
| ~ product(e_3,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_193,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_4)
| ~ product(e_4,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_194,plain,
( equalish(e_1,e_4)
| ~ product(e_4,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_193]) ).
tcf(c_195,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_5)
| ~ greater(X1,e_0)
| ~ next(X0,e_5)
| ~ cycle(X0,X1)
| ~ product(X0,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_132]) ).
tcf(c_197,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_5)
| ~ product(X0,X1,e_5)
| ~ product(X0,X1,e_1) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_199,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_5)
| ~ product(X0,e_5,X1)
| ~ product(X0,e_1,X1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_201,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_5)
| ~ product(e_5,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_205,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_1)
| ~ product(X0,X1,e_2)
| ~ product(X0,X1,e_1) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_207,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_1)
| ~ product(X0,e_2,X1)
| ~ product(X0,e_1,X1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_208,plain,
( equalish(e_2,e_1)
| ~ product(e_1,e_2,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_209,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_1)
| ~ product(e_2,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_213,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_3)
| ~ product(X0,X1,e_3)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_215,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_3)
| ~ product(X0,e_3,X1)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_217,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_3)
| ~ product(e_3,X0,X1)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_223,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_4)
| ~ product(X0,e_4,X1)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_225,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_4)
| ~ product(e_4,X0,X1)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_227,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_5)
| ~ greater(X1,e_0)
| ~ next(X0,e_5)
| ~ cycle(X0,X1)
| ~ product(X0,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_132]) ).
tcf(c_229,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_5)
| ~ product(X0,X1,e_5)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_231,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_5)
| ~ product(X0,e_5,X1)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_233,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_5)
| ~ product(e_5,X0,X1)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_237,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_1)
| ~ product(X0,X1,e_3)
| ~ product(X0,X1,e_1) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_239,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_1)
| ~ product(X0,e_3,X1)
| ~ product(X0,e_1,X1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_240,plain,
( equalish(e_3,e_1)
| ~ product(e_1,e_3,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_239]) ).
tcf(c_241,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_1)
| ~ product(e_3,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_247,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_2)
| ~ product(X0,e_3,X1)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_249,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_2)
| ~ product(e_3,X0,X1)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_253,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_4)
| ~ product(X0,X1,e_4)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_255,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_4)
| ~ product(X0,e_4,X1)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_257,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_4)
| ~ product(e_4,X0,X1)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_259,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_5)
| ~ greater(X1,e_0)
| ~ next(X0,e_5)
| ~ cycle(X0,X1)
| ~ product(X0,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_132]) ).
tcf(c_265,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_5)
| ~ product(e_5,X0,X1)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_269,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_1)
| ~ product(X0,X1,e_4)
| ~ product(X0,X1,e_1) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_271,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_1)
| ~ product(X0,e_4,X1)
| ~ product(X0,e_1,X1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_272,plain,
( equalish(e_4,e_1)
| ~ product(e_1,e_4,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_271]) ).
tcf(c_273,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_1)
| ~ product(e_4,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_277,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_2)
| ~ product(X0,X1,e_4)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_279,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_2)
| ~ product(X0,e_4,X1)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_281,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_2)
| ~ product(e_4,X0,X1)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_283,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_3)
| ~ greater(X1,e_0)
| ~ next(X0,e_3)
| ~ cycle(X0,X1)
| ~ product(X0,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_132]) ).
tcf(c_285,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_3)
| ~ product(X0,X1,e_4)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_287,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_3)
| ~ product(X0,e_4,X1)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_288,plain,
( equalish(e_4,e_3)
| ~ product(e_1,e_4,e_1)
| ~ product(e_1,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_287]) ).
tcf(c_289,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_3)
| ~ product(e_4,X0,X1)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_293,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_5)
| ~ product(X0,X1,e_5)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_295,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_5)
| ~ product(X0,e_5,X1)
| ~ product(X0,e_4,X1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_297,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_5)
| ~ product(e_5,X0,X1)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_303,plain,
! [X0: $i,X1: $i] :
( equalish(e_5,e_1)
| ~ product(X0,e_5,X1)
| ~ product(X0,e_1,X1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_304,plain,
( equalish(e_5,e_1)
| ~ product(e_1,e_5,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_303]) ).
tcf(c_305,plain,
! [X0: $i,X1: $i] :
( equalish(e_5,e_1)
| ~ product(e_5,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_311,plain,
! [X0: $i,X1: $i] :
( equalish(e_5,e_2)
| ~ product(X0,e_5,X1)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_313,plain,
! [X0: $i,X1: $i] :
( equalish(e_5,e_2)
| ~ product(e_5,X0,X1)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_319,plain,
! [X0: $i,X1: $i] :
( equalish(e_5,e_3)
| ~ product(X0,e_5,X1)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_321,plain,
! [X0: $i,X1: $i] :
( equalish(e_5,e_3)
| ~ product(e_5,X0,X1)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_325,plain,
! [X0: $i,X1: $i] :
( equalish(e_5,e_4)
| ~ product(X0,X1,e_5)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_327,plain,
! [X0: $i,X1: $i] :
( equalish(e_5,e_4)
| ~ product(X0,e_5,X1)
| ~ product(X0,e_4,X1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_329,plain,
! [X0: $i,X1: $i] :
( equalish(e_5,e_4)
| ~ product(e_5,X0,X1)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_345,plain,
( ~ cycle(e_2,e_0)
| ~ greater(e_4,e_2)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_347,plain,
( ~ cycle(e_3,e_0)
| ~ greater(e_4,e_3)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_350,plain,
! [X0: $i,X1: $i,X2: $i] :
( equalish(X2,e_1)
| ~ next(e_0,e_1)
| ~ cycle(X1,e_0)
| ~ greater(X2,e_0)
| ~ cycle(X0,X2)
| ~ next(X0,X1) ),
inference(instantiation,[status(thm)],[c_129]) ).
tcf(c_367,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ cycle(e_4,e_0)
| ~ next(e_4,e_5)
| ~ cycle(e_5,X1)
| ~ greater(e_4,X2)
| ~ cycle(X2,X0)
| ~ greater(X0,X1) ),
inference(instantiation,[status(thm)],[c_130]) ).
tcf(c_382,plain,
! [X0: $i] :
( product(e_2,e_1,e_3)
| ~ product(e_2,X0,e_1)
| ~ product(e_1,X0,e_3) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_384,plain,
! [X0: $i] :
( product(e_2,e_1,e_4)
| ~ product(e_2,X0,e_1)
| ~ product(e_1,X0,e_4) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_386,plain,
! [X0: $i] :
( product(e_2,e_1,e_5)
| ~ product(e_2,X0,e_1)
| ~ product(e_1,X0,e_5) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_388,plain,
! [X0: $i] :
( product(e_3,e_1,e_4)
| ~ product(e_3,X0,e_1)
| ~ product(e_1,X0,e_4) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_390,plain,
! [X0: $i] :
( product(e_3,e_1,e_5)
| ~ product(e_3,X0,e_1)
| ~ product(e_1,X0,e_5) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_392,plain,
! [X0: $i] :
( product(e_4,e_1,e_5)
| ~ product(e_4,X0,e_1)
| ~ product(e_1,X0,e_5) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_394,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X0,e_2,X2)
| ~ product(e_2,X1,X2)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_397,plain,
! [X0: $i] :
( product(X0,e_2,e_5)
| product(X0,e_2,e_4)
| product(X0,e_2,e_3)
| product(X0,e_2,e_2)
| product(X0,e_2,e_1)
| ~ group_element(e_2)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_158]) ).
tcf(c_398,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)
| ~ group_element(e_2)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_397]) ).
tcf(c_399,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_2,X0,X2)
| ~ product(e_2,X1,X0)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_401,plain,
! [X0: $i] :
( product(e_2,X0,e_5)
| product(e_2,X0,e_4)
| product(e_2,X0,e_3)
| product(e_2,X0,e_2)
| product(e_2,X0,e_1)
| ~ group_element(e_2)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_158]) ).
tcf(c_402,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)
| ~ group_element(e_2)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_401]) ).
tcf(c_403,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X0,e_3,X2)
| ~ product(e_3,X1,X2)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_406,plain,
! [X0: $i] :
( product(X0,e_3,e_5)
| product(X0,e_3,e_4)
| product(X0,e_3,e_3)
| product(X0,e_3,e_2)
| product(X0,e_3,e_1)
| ~ group_element(e_3)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_158]) ).
tcf(c_407,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)
| ~ group_element(e_3)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_406]) ).
tcf(c_408,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_3,X0,X2)
| ~ product(e_3,X1,X0)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_410,plain,
! [X0: $i] :
( product(e_3,X0,e_5)
| product(e_3,X0,e_4)
| product(e_3,X0,e_3)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1)
| ~ group_element(e_3)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_158]) ).
tcf(c_412,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X0,e_4,X2)
| ~ product(e_4,X1,X2)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_415,plain,
! [X0: $i] :
( product(X0,e_4,e_5)
| product(X0,e_4,e_4)
| product(X0,e_4,e_3)
| product(X0,e_4,e_2)
| product(X0,e_4,e_1)
| ~ group_element(e_4)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_158]) ).
tcf(c_416,plain,
( product(e_1,e_4,e_5)
| 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)
| ~ group_element(e_4)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_415]) ).
tcf(c_425,plain,
! [X0: $i] :
( product(e_4,X0,e_5)
| product(e_4,X0,e_4)
| product(e_4,X0,e_3)
| product(e_4,X0,e_2)
| product(e_4,X0,e_1)
| ~ group_element(e_4)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_158]) ).
tcf(c_426,plain,
( 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)
| ~ group_element(e_4)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_425]) ).
tcf(c_427,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X0,e_5,X2)
| ~ product(e_5,X1,X2)
| ~ product(X0,X1,e_5) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_430,plain,
! [X0: $i] :
( product(X0,e_5,e_5)
| product(X0,e_5,e_4)
| product(X0,e_5,e_3)
| product(X0,e_5,e_2)
| product(X0,e_5,e_1)
| ~ group_element(e_5)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_158]) ).
tcf(c_431,plain,
( 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)
| ~ group_element(e_5)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_430]) ).
tcf(c_432,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_5,X0,X2)
| ~ product(e_5,X1,X0)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_434,plain,
! [X0: $i] :
( product(e_5,X0,e_5)
| product(e_5,X0,e_4)
| product(e_5,X0,e_3)
| product(e_5,X0,e_2)
| product(e_5,X0,e_1)
| ~ group_element(e_5)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_158]) ).
tcf(c_435,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)
| ~ group_element(e_5)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_434]) ).
tcf(c_502,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X0,X2,e_2)
| ~ product(X2,X1,e_2)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_503,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X0,X2,e_3)
| ~ product(X2,X1,e_3)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_541,plain,
! [X0: $i] :
( equalish(e_1,e_5)
| ~ next(e_4,e_5)
| ~ cycle(e_4,X0)
| ~ greater(X0,e_0)
| ~ product(e_4,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_195]) ).
tcf(c_542,plain,
( equalish(e_1,e_5)
| ~ cycle(e_4,e_1)
| ~ greater(e_1,e_0)
| ~ next(e_4,e_5)
| ~ product(e_4,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_541]) ).
tcf(c_549,plain,
! [X0: $i] :
( equalish(e_2,e_5)
| ~ next(e_4,e_5)
| ~ cycle(e_4,X0)
| ~ greater(X0,e_0)
| ~ product(e_4,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_227]) ).
tcf(c_550,plain,
( equalish(e_2,e_5)
| ~ cycle(e_4,e_1)
| ~ greater(e_1,e_0)
| ~ next(e_4,e_5)
| ~ product(e_4,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_549]) ).
tcf(c_556,plain,
! [X0: $i] :
( equalish(e_3,e_5)
| ~ next(e_4,e_5)
| ~ cycle(e_4,X0)
| ~ greater(X0,e_0)
| ~ product(e_4,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_259]) ).
tcf(c_557,plain,
( equalish(e_3,e_5)
| ~ cycle(e_4,e_1)
| ~ greater(e_1,e_0)
| ~ next(e_4,e_5)
| ~ product(e_4,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_556]) ).
tcf(c_560,plain,
! [X0: $i,X1: $i] :
( product(X0,e_1,e_4)
| ~ product(e_1,X1,e_4)
| ~ product(X0,X1,e_1) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_561,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ next(e_2,e_3)
| ~ cycle(e_2,X0)
| ~ greater(X0,e_0)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_283]) ).
tcf(c_562,plain,
( equalish(e_4,e_3)
| ~ cycle(e_2,e_1)
| ~ greater(e_1,e_0)
| ~ next(e_2,e_3)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_561]) ).
tcf(c_563,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X0,X2,e_4)
| ~ product(X2,X1,e_4)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_564,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X0,X2,e_5)
| ~ product(X2,X1,e_5)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_592,plain,
( cycle(e_2,e_4)
| cycle(e_2,e_3)
| cycle(e_2,e_2)
| cycle(e_2,e_1)
| cycle(e_2,e_0)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_127]) ).
tcf(c_593,plain,
( cycle(e_3,e_4)
| cycle(e_3,e_3)
| cycle(e_3,e_2)
| cycle(e_3,e_1)
| cycle(e_3,e_0)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_127]) ).
tcf(c_599,plain,
! [X0: $i] :
( equalish(X0,e_1)
| ~ cycle(e_4,e_0)
| ~ next(e_3,e_4)
| ~ next(e_0,e_1)
| ~ cycle(e_3,X0)
| ~ greater(X0,e_0) ),
inference(instantiation,[status(thm)],[c_350]) ).
tcf(c_601,plain,
! [X0: $i] :
( equalish(X0,e_1)
| ~ cycle(e_5,e_0)
| ~ next(e_4,e_5)
| ~ next(e_0,e_1)
| ~ cycle(e_4,X0)
| ~ greater(X0,e_0) ),
inference(instantiation,[status(thm)],[c_350]) ).
tcf(c_603,plain,
( cycle(e_4,e_4)
| cycle(e_4,e_3)
| cycle(e_4,e_2)
| cycle(e_4,e_1)
| cycle(e_4,e_0)
| ~ group_element(e_4) ),
inference(instantiation,[status(thm)],[c_127]) ).
tcf(c_681,plain,
! [X0: $i] :
( equalish(e_2,e_1)
| ~ product(X0,e_2,e_2)
| ~ product(X0,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_685,plain,
( product(e_2,e_2,e_5)
| 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)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_397]) ).
tcf(c_686,plain,
( equalish(e_2,e_1)
| ~ product(e_2,e_2,e_2)
| ~ product(e_1,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_209]) ).
tcf(c_687,plain,
( equalish(e_1,e_2)
| ~ product(e_2,e_2,e_2)
| ~ product(e_1,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_177]) ).
tcf(c_688,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)
| ~ group_element(e_3)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_397]) ).
tcf(c_693,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)
| ~ group_element(e_4)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_397]) ).
tcf(c_704,plain,
! [X0: $i] :
( product(e_5,X0,e_2)
| ~ product(e_5,e_2,X0)
| ~ product(X0,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_432]) ).
tcf(c_705,plain,
( product(e_5,e_1,e_2)
| ~ product(e_5,e_2,e_1)
| ~ product(e_1,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_704]) ).
tcf(c_723,plain,
! [X0: $i] :
( product(e_2,e_3,e_2)
| ~ product(e_3,X0,e_2)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_729,plain,
! [X0: $i] :
( equalish(e_5,e_2)
| ~ product(e_5,X0,e_3)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_313]) ).
tcf(c_731,plain,
! [X0: $i] :
( equalish(e_2,e_1)
| ~ product(e_2,X0,e_3)
| ~ product(e_1,X0,e_3) ),
inference(instantiation,[status(thm)],[c_209]) ).
tcf(c_737,plain,
! [X0: $i,X1: $i] :
( product(e_2,e_3,X1)
| ~ product(e_2,X0,e_3)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_403]) ).
tcf(c_739,plain,
! [X0: $i] :
( equalish(e_3,e_1)
| ~ product(e_2,X0,e_3)
| ~ product(e_2,X0,e_1) ),
inference(instantiation,[status(thm)],[c_237]) ).
tcf(c_747,plain,
( product(e_2,e_3,e_5)
| product(e_2,e_3,e_4)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| ~ group_element(e_3)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_401]) ).
tcf(c_752,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)
| ~ group_element(e_4)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_401]) ).
tcf(c_754,plain,
( equalish(e_4,e_2)
| ~ product(e_2,e_4,e_3)
| ~ product(e_2,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_279]) ).
tcf(c_755,plain,
( equalish(e_4,e_1)
| ~ product(e_2,e_4,e_3)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_271]) ).
tcf(c_762,plain,
! [X0: $i,X1: $i] :
( product(X0,e_2,e_3)
| ~ product(e_2,X1,e_3)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_394]) ).
tcf(c_763,plain,
( product(e_1,e_2,e_3)
| ~ product(e_2,e_1,e_3)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_762]) ).
tcf(c_806,plain,
! [X0: $i,X1: $i] :
( product(X0,e_2,e_2)
| ~ product(e_2,X1,e_2)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_807,plain,
! [X0: $i,X1: $i] :
( product(e_5,X0,e_2)
| ~ product(e_5,X1,X0)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_432]) ).
tcf(c_813,plain,
! [X0: $i] :
( equalish(e_5,e_1)
| ~ product(e_5,X0,e_2)
| ~ product(e_1,X0,e_2) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_853,plain,
! [X0: $i] :
( equalish(e_5,e_2)
| ~ product(X0,e_5,e_2)
| ~ product(X0,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_311]) ).
tcf(c_854,plain,
( equalish(e_5,e_2)
| ~ product(e_1,e_5,e_2)
| ~ product(e_1,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_853]) ).
tcf(c_872,plain,
! [X0: $i] :
( equalish(e_5,e_3)
| ~ product(X0,e_5,e_2)
| ~ product(X0,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_319]) ).
tcf(c_874,plain,
! [X0: $i] :
( equalish(e_3,e_2)
| ~ product(X0,e_3,e_2)
| ~ product(X0,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_875,plain,
! [X0: $i] :
( equalish(e_3,e_1)
| ~ product(X0,e_3,e_2)
| ~ product(X0,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_239]) ).
tcf(c_883,plain,
( equalish(e_5,e_3)
| ~ product(e_1,e_5,e_2)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_872]) ).
tcf(c_884,plain,
( product(e_3,e_3,e_5)
| product(e_3,e_3,e_4)
| product(e_3,e_3,e_3)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_1)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_406]) ).
tcf(c_891,plain,
( product(e_4,e_3,e_5)
| product(e_4,e_3,e_4)
| product(e_4,e_3,e_3)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_1)
| ~ group_element(e_4)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_406]) ).
tcf(c_893,plain,
( equalish(e_4,e_5)
| ~ product(e_5,e_3,e_2)
| ~ product(e_4,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_907,plain,
! [X0: $i] :
( product(e_3,e_4,e_2)
| ~ product(e_4,X0,e_2)
| ~ product(e_3,X0,e_4) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_908,plain,
! [X0: $i] :
( product(e_5,e_3,e_4)
| ~ product(e_5,X0,e_3)
| ~ product(e_3,X0,e_4) ),
inference(instantiation,[status(thm)],[c_432]) ).
tcf(c_910,plain,
( product(e_3,e_4,e_2)
| ~ product(e_4,e_1,e_2)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_907]) ).
tcf(c_914,plain,
! [X0: $i] :
( equalish(e_5,e_3)
| ~ product(e_5,X0,e_4)
| ~ product(e_3,X0,e_4) ),
inference(instantiation,[status(thm)],[c_321]) ).
tcf(c_915,plain,
! [X0: $i] :
( equalish(e_3,e_5)
| ~ product(e_5,X0,e_4)
| ~ product(e_3,X0,e_4) ),
inference(instantiation,[status(thm)],[c_265]) ).
tcf(c_916,plain,
! [X0: $i] :
( equalish(e_3,e_2)
| ~ product(e_3,X0,e_4)
| ~ product(e_2,X0,e_4) ),
inference(instantiation,[status(thm)],[c_249]) ).
tcf(c_917,plain,
! [X0: $i] :
( equalish(e_3,e_1)
| ~ product(e_3,X0,e_4)
| ~ product(e_1,X0,e_4) ),
inference(instantiation,[status(thm)],[c_241]) ).
tcf(c_923,plain,
( equalish(e_3,e_2)
| ~ product(e_3,e_1,e_4)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_916]) ).
tcf(c_924,plain,
( equalish(e_3,e_5)
| ~ product(e_5,e_1,e_4)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_915]) ).
tcf(c_926,plain,
! [X0: $i,X1: $i] :
( product(e_3,e_4,X1)
| ~ product(e_3,X0,e_4)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_929,plain,
! [X0: $i] :
( equalish(e_4,e_1)
| ~ product(e_3,X0,e_4)
| ~ product(e_3,X0,e_1) ),
inference(instantiation,[status(thm)],[c_269]) ).
tcf(c_939,plain,
( product(e_3,e_4,e_1)
| ~ product(e_4,e_1,e_1)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_926]) ).
tcf(c_940,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)
| ~ group_element(e_4)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_410]) ).
tcf(c_951,plain,
! [X0: $i,X1: $i] :
( product(X0,e_3,e_4)
| ~ product(e_3,X1,e_4)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_563]) ).
tcf(c_961,plain,
! [X0: $i] :
( equalish(e_5,e_4)
| ~ product(X0,e_5,e_2)
| ~ product(X0,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_963,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ product(X0,e_4,e_2)
| ~ product(X0,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_287]) ).
tcf(c_964,plain,
! [X0: $i] :
( equalish(e_4,e_2)
| ~ product(X0,e_4,e_2)
| ~ product(X0,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_279]) ).
tcf(c_966,plain,
! [X0: $i] :
( equalish(e_3,e_4)
| ~ product(X0,e_4,e_2)
| ~ product(X0,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_255]) ).
tcf(c_971,plain,
( equalish(e_3,e_4)
| ~ product(e_1,e_4,e_2)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_966]) ).
tcf(c_974,plain,
( equalish(e_4,e_3)
| ~ product(e_1,e_4,e_2)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_963]) ).
tcf(c_976,plain,
( equalish(e_5,e_4)
| ~ product(e_1,e_5,e_2)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_961]) ).
tcf(c_977,plain,
( product(e_4,e_4,e_5)
| 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)
| ~ group_element(e_4) ),
inference(instantiation,[status(thm)],[c_415]) ).
tcf(c_978,plain,
( equalish(e_5,e_4)
| ~ product(e_5,e_4,e_2)
| ~ product(e_4,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_983,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_4,e_2)
| ~ product(e_3,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_257]) ).
tcf(c_985,plain,
( equalish(e_1,e_4)
| ~ product(e_4,e_4,e_2)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_193]) ).
tcf(c_992,plain,
( equalish(e_1,e_5)
| ~ product(e_4,e_5,e_5)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_199]) ).
tcf(c_993,plain,
! [X0: $i] :
( product(e_4,e_5,e_2)
| ~ product(e_5,X0,e_2)
| ~ product(e_4,X0,e_5) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_994,plain,
! [X0: $i] :
( product(e_5,e_4,e_5)
| ~ product(e_5,X0,e_4)
| ~ product(e_4,X0,e_5) ),
inference(instantiation,[status(thm)],[c_432]) ).
tcf(c_995,plain,
( product(e_5,e_4,e_5)
| ~ product(e_5,e_1,e_4)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_994]) ).
tcf(c_1001,plain,
! [X0: $i] :
( equalish(e_5,e_4)
| ~ product(e_5,X0,e_5)
| ~ product(e_4,X0,e_5) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_1002,plain,
! [X0: $i] :
( equalish(e_4,e_5)
| ~ product(e_5,X0,e_5)
| ~ product(e_4,X0,e_5) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_1003,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ product(e_4,X0,e_5)
| ~ product(e_3,X0,e_5) ),
inference(instantiation,[status(thm)],[c_289]) ).
tcf(c_1004,plain,
! [X0: $i] :
( equalish(e_4,e_2)
| ~ product(e_4,X0,e_5)
| ~ product(e_2,X0,e_5) ),
inference(instantiation,[status(thm)],[c_281]) ).
tcf(c_1005,plain,
! [X0: $i] :
( equalish(e_4,e_1)
| ~ product(e_4,X0,e_5)
| ~ product(e_1,X0,e_5) ),
inference(instantiation,[status(thm)],[c_273]) ).
tcf(c_1013,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_1,e_5)
| ~ product(e_2,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_1004]) ).
tcf(c_1015,plain,
( equalish(e_4,e_5)
| ~ product(e_5,e_1,e_5)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_1002]) ).
tcf(c_1017,plain,
! [X0: $i,X1: $i] :
( product(e_4,e_5,X1)
| ~ product(e_4,X0,e_5)
| ~ product(e_5,X0,X1) ),
inference(instantiation,[status(thm)],[c_427]) ).
tcf(c_1034,plain,
( product(e_4,e_5,e_1)
| ~ product(e_5,e_1,e_1)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_1017]) ).
tcf(c_1037,plain,
! [X0: $i,X1: $i] :
( product(X0,e_4,e_5)
| ~ product(e_4,X1,e_5)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_564]) ).
tcf(c_1043,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,e_1)
| ~ product(X1,e_5,e_1)
| ~ product(X0,e_5,X1) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_1044,plain,
( product(e_1,e_1,e_1)
| ~ product(e_1,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_1043]) ).
tcf(c_1048,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)
| ~ group_element(e_5)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_430]) ).
tcf(c_1049,plain,
( equalish(e_5,e_2)
| ~ product(e_5,e_5,e_1)
| ~ product(e_2,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_313]) ).
tcf(c_1051,plain,
( equalish(e_2,e_1)
| ~ product(e_2,e_5,e_1)
| ~ product(e_1,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_209]) ).
tcf(c_1053,plain,
( product(e_3,e_5,e_5)
| product(e_3,e_5,e_4)
| product(e_3,e_5,e_3)
| product(e_3,e_5,e_2)
| product(e_3,e_5,e_1)
| ~ group_element(e_5)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_430]) ).
tcf(c_1054,plain,
( equalish(e_5,e_3)
| ~ product(e_5,e_5,e_1)
| ~ product(e_3,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_321]) ).
tcf(c_1056,plain,
( equalish(e_3,e_2)
| ~ product(e_3,e_5,e_1)
| ~ product(e_2,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_249]) ).
tcf(c_1057,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_5,e_1)
| ~ product(e_1,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_241]) ).
tcf(c_1060,plain,
( product(e_4,e_5,e_5)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_2)
| product(e_4,e_5,e_1)
| ~ group_element(e_5)
| ~ group_element(e_4) ),
inference(instantiation,[status(thm)],[c_430]) ).
tcf(c_1063,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_5,e_1)
| ~ product(e_3,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_289]) ).
tcf(c_1067,plain,
( equalish(e_2,e_4)
| ~ product(e_4,e_5,e_1)
| ~ product(e_2,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_1089,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)
| ~ group_element(e_5)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_434]) ).
tcf(c_1092,plain,
( equalish(e_2,e_1)
| ~ product(e_5,e_2,e_1)
| ~ product(e_5,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_1094,plain,
( product(e_5,e_3,e_5)
| product(e_5,e_3,e_4)
| product(e_5,e_3,e_3)
| product(e_5,e_3,e_2)
| product(e_5,e_3,e_1)
| ~ group_element(e_5)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_434]) ).
tcf(c_1097,plain,
( equalish(e_3,e_2)
| ~ product(e_5,e_3,e_1)
| ~ product(e_5,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_1101,plain,
( product(e_5,e_4,e_5)
| product(e_5,e_4,e_4)
| product(e_5,e_4,e_3)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_1)
| ~ group_element(e_5)
| ~ group_element(e_4) ),
inference(instantiation,[status(thm)],[c_434]) ).
tcf(c_1104,plain,
( equalish(e_4,e_3)
| ~ product(e_5,e_4,e_1)
| ~ product(e_5,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_287]) ).
tcf(c_1105,plain,
( equalish(e_4,e_2)
| ~ product(e_5,e_4,e_1)
| ~ product(e_5,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_279]) ).
tcf(c_1117,plain,
( equalish(e_2,e_1)
| ~ cycle(e_5,e_0)
| ~ cycle(e_4,e_2)
| ~ greater(e_2,e_0)
| ~ next(e_4,e_5)
| ~ next(e_0,e_1) ),
inference(instantiation,[status(thm)],[c_601]) ).
tcf(c_1118,plain,
( equalish(e_3,e_1)
| ~ cycle(e_5,e_0)
| ~ cycle(e_4,e_3)
| ~ greater(e_3,e_0)
| ~ next(e_4,e_5)
| ~ next(e_0,e_1) ),
inference(instantiation,[status(thm)],[c_601]) ).
tcf(c_1119,plain,
( equalish(e_4,e_1)
| ~ cycle(e_5,e_0)
| ~ cycle(e_4,e_4)
| ~ greater(e_4,e_0)
| ~ next(e_4,e_5)
| ~ next(e_0,e_1) ),
inference(instantiation,[status(thm)],[c_601]) ).
tcf(c_1121,plain,
! [X0: $i] :
( equalish(e_1,e_2)
| ~ product(X0,e_5,e_2)
| ~ product(X0,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_173]) ).
tcf(c_1139,plain,
( equalish(e_5,e_3)
| ~ product(e_5,e_4,e_2)
| ~ product(e_3,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_321]) ).
tcf(c_1140,plain,
( equalish(e_3,e_5)
| ~ product(e_5,e_4,e_2)
| ~ product(e_3,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_265]) ).
tcf(c_1142,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_4,e_2)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_241]) ).
tcf(c_1144,plain,
( equalish(e_1,e_3)
| ~ product(e_3,e_4,e_2)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_185]) ).
tcf(c_1153,plain,
! [X0: $i] :
( product(e_3,e_2,X0)
| ~ product(e_3,e_4,e_2)
| ~ product(e_2,e_4,X0) ),
inference(instantiation,[status(thm)],[c_408]) ).
tcf(c_1154,plain,
( product(e_3,e_2,e_1)
| ~ product(e_3,e_4,e_2)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_1153]) ).
tcf(c_1155,plain,
( product(e_2,e_3,e_2)
| ~ product(e_3,e_4,e_2)
| ~ product(e_2,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_723]) ).
tcf(c_1211,plain,
! [X0: $i] :
( product(X0,e_3,e_2)
| ~ product(e_3,e_4,e_2)
| ~ product(X0,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_1212,plain,
( product(e_1,e_3,e_2)
| ~ product(e_3,e_4,e_2)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_1211]) ).
tcf(c_1251,plain,
! [X0: $i] :
( product(e_2,e_3,e_4)
| ~ product(e_3,X0,e_4)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_737]) ).
tcf(c_1265,plain,
( product(e_5,e_3,e_2)
| ~ product(e_5,e_4,e_3)
| ~ product(e_3,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_1266,plain,
( equalish(e_5,e_2)
| ~ product(e_2,e_5,e_1)
| ~ product(e_2,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_311]) ).
tcf(c_1275,plain,
! [X0: $i] :
( product(X0,e_2,e_1)
| ~ product(e_2,e_2,e_1)
| ~ product(X0,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_394]) ).
tcf(c_1276,plain,
( product(e_1,e_2,e_1)
| ~ product(e_2,e_2,e_1)
| ~ product(e_1,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_1275]) ).
tcf(c_1287,plain,
( equalish(e_5,e_3)
| ~ product(e_5,e_2,e_1)
| ~ product(e_3,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_321]) ).
tcf(c_1295,plain,
! [X0: $i] :
( product(e_3,e_1,X0)
| ~ product(e_3,e_2,e_1)
| ~ product(e_1,e_2,X0) ),
inference(instantiation,[status(thm)],[c_408]) ).
tcf(c_1301,plain,
( equalish(e_5,e_2)
| ~ product(e_4,e_5,e_1)
| ~ product(e_4,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_311]) ).
tcf(c_1305,plain,
( product(e_3,e_4,e_1)
| ~ product(e_4,e_2,e_1)
| ~ product(e_3,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_926]) ).
tcf(c_1307,plain,
( equalish(e_4,e_5)
| ~ product(e_5,e_2,e_1)
| ~ product(e_4,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_1326,plain,
( equalish(e_5,e_2)
| ~ product(e_1,e_5,e_3)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_311]) ).
tcf(c_1327,plain,
( equalish(e_2,e_5)
| ~ product(e_1,e_5,e_3)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_231]) ).
tcf(c_1328,plain,
( equalish(e_2,e_1)
| ~ product(e_1,e_2,e_3)
| ~ product(e_1,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_1330,plain,
( product(e_1,e_3,e_4)
| ~ product(e_3,e_2,e_4)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_951]) ).
tcf(c_1331,plain,
! [X0: $i] :
( product(e_1,e_3,X0)
| ~ product(e_1,e_2,e_3)
| ~ product(e_3,e_2,X0) ),
inference(instantiation,[status(thm)],[c_403]) ).
tcf(c_1336,plain,
( product(e_1,e_3,e_1)
| ~ product(e_3,e_2,e_1)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_1331]) ).
tcf(c_1353,plain,
! [X0: $i] :
( product(X0,e_2,e_2)
| ~ product(e_2,e_3,e_2)
| ~ product(X0,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_394]) ).
tcf(c_1367,plain,
( equalish(e_5,e_2)
| ~ product(e_5,e_4,e_1)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_313]) ).
tcf(c_1368,plain,
( equalish(e_2,e_5)
| ~ product(e_5,e_4,e_1)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_233]) ).
tcf(c_1369,plain,
( equalish(e_2,e_1)
| ~ product(e_2,e_4,e_1)
| ~ product(e_1,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_209]) ).
tcf(c_1371,plain,
( equalish(e_5,e_4)
| ~ product(e_2,e_5,e_1)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_1372,plain,
( equalish(e_4,e_5)
| ~ product(e_2,e_5,e_1)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_295]) ).
tcf(c_1380,plain,
! [X0: $i] :
( product(X0,e_2,e_1)
| ~ product(e_2,e_4,e_1)
| ~ product(X0,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_394]) ).
tcf(c_1381,plain,
( product(e_1,e_2,e_1)
| ~ product(e_2,e_4,e_1)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_1380]) ).
tcf(c_1411,plain,
( equalish(e_5,e_3)
| ~ product(e_3,e_5,e_1)
| ~ product(e_3,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_319]) ).
tcf(c_1417,plain,
( product(e_2,e_3,e_1)
| ~ product(e_3,e_3,e_1)
| ~ product(e_2,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_737]) ).
tcf(c_1435,plain,
( equalish(e_5,e_3)
| ~ product(e_4,e_5,e_1)
| ~ product(e_4,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_319]) ).
tcf(c_1438,plain,
( equalish(e_3,e_1)
| ~ product(e_4,e_3,e_1)
| ~ product(e_4,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_239]) ).
tcf(c_1520,plain,
( equalish(e_5,e_4)
| ~ product(e_4,e_5,e_1)
| ~ product(e_4,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_1521,plain,
( equalish(e_4,e_5)
| ~ product(e_4,e_5,e_1)
| ~ product(e_4,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_295]) ).
tcf(c_1523,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_4,e_1)
| ~ product(e_4,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_279]) ).
tcf(c_1528,plain,
( product(e_3,e_4,e_1)
| ~ product(e_4,e_4,e_1)
| ~ product(e_3,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_926]) ).
tcf(c_1529,plain,
( equalish(e_5,e_4)
| ~ product(e_5,e_4,e_1)
| ~ product(e_4,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_1530,plain,
( equalish(e_4,e_5)
| ~ product(e_5,e_4,e_1)
| ~ product(e_4,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_1531,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_4,e_1)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_289]) ).
tcf(c_1532,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_4,e_1)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_281]) ).
tcf(c_1533,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_4,e_1)
| ~ product(e_1,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_273]) ).
tcf(c_1534,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_4,e_1)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_257]) ).
tcf(c_1535,plain,
( equalish(e_2,e_4)
| ~ product(e_4,e_4,e_1)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_1549,plain,
( product(e_5,e_4,e_2)
| ~ product(e_5,e_1,e_4)
| ~ product(e_4,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_1567,plain,
( product(e_1,e_2,e_3)
| ~ product(e_2,e_5,e_3)
| ~ product(e_1,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_762]) ).
tcf(c_1579,plain,
! [X0: $i] :
( product(X0,e_2,e_2)
| ~ product(e_2,e_5,e_2)
| ~ product(X0,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_394]) ).
tcf(c_1591,plain,
( product(e_2,e_3,e_1)
| ~ product(e_3,e_5,e_1)
| ~ product(e_2,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_737]) ).
tcf(c_1602,plain,
! [X0: $i] :
( product(X0,e_3,e_1)
| ~ product(e_3,e_5,e_1)
| ~ product(X0,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_1043]) ).
tcf(c_1603,plain,
( product(e_1,e_3,e_1)
| ~ product(e_3,e_5,e_1)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_1602]) ).
tcf(c_1633,plain,
! [X0: $i] :
( product(e_4,e_5,X0)
| ~ product(e_4,e_5,e_5)
| ~ product(e_5,e_5,X0) ),
inference(instantiation,[status(thm)],[c_1017]) ).
tcf(c_1634,plain,
( product(e_4,e_5,e_1)
| ~ product(e_5,e_5,e_1)
| ~ product(e_4,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_1633]) ).
tcf(c_1636,plain,
! [X0: $i] :
( product(X0,e_4,e_5)
| ~ product(e_4,e_5,e_5)
| ~ product(X0,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_1037]) ).
tcf(c_1637,plain,
( product(e_1,e_4,e_5)
| ~ product(e_4,e_5,e_5)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_1636]) ).
tcf(c_1664,plain,
! [X0: $i] :
( product(X0,e_5,e_5)
| ~ product(e_5,e_1,e_5)
| ~ product(X0,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_564]) ).
tcf(c_1665,plain,
( product(e_1,e_5,e_5)
| ~ product(e_5,e_1,e_5)
| ~ product(e_1,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_1664]) ).
tcf(c_1669,plain,
( product(e_5,e_2,e_3)
| ~ product(e_5,e_2,e_2)
| ~ product(e_2,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_762]) ).
tcf(c_1675,plain,
! [X0: $i] :
( product(e_5,e_2,X0)
| ~ product(e_5,e_2,e_2)
| ~ product(e_2,e_2,X0) ),
inference(instantiation,[status(thm)],[c_432]) ).
tcf(c_1676,plain,
( product(e_5,e_2,e_1)
| ~ product(e_5,e_2,e_2)
| ~ product(e_2,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_1675]) ).
tcf(c_1679,plain,
! [X0: $i] :
( product(X0,e_5,e_2)
| ~ product(e_5,e_2,e_2)
| ~ product(X0,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_1680,plain,
( product(e_1,e_5,e_2)
| ~ product(e_5,e_2,e_2)
| ~ product(e_1,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_1679]) ).
tcf(c_1707,plain,
! [X0: $i] :
( product(e_5,e_4,X0)
| ~ product(e_5,e_4,e_4)
| ~ product(e_4,e_4,X0) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_1711,plain,
( equalish(e_3,e_4)
| ~ product(e_5,e_4,e_4)
| ~ product(e_5,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_253]) ).
tcf(c_1714,plain,
( product(e_5,e_4,e_1)
| ~ product(e_5,e_4,e_4)
| ~ product(e_4,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_1707]) ).
tcf(c_1715,plain,
( equalish(e_5,e_4)
| ~ product(e_5,e_5,e_4)
| ~ product(e_5,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_1717,plain,
( equalish(e_4,e_3)
| ~ product(e_5,e_4,e_4)
| ~ product(e_5,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_287]) ).
tcf(c_1724,plain,
( product(e_5,e_4,e_5)
| ~ product(e_5,e_4,e_4)
| ~ product(e_4,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_994]) ).
tcf(c_1725,plain,
! [X0: $i] :
( product(X0,e_5,e_4)
| ~ product(e_5,e_4,e_4)
| ~ product(X0,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_563]) ).
tcf(c_1726,plain,
( product(e_1,e_5,e_4)
| ~ product(e_5,e_4,e_4)
| ~ product(e_1,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_1725]) ).
tcf(c_1750,plain,
( equalish(e_2,e_1)
| ~ product(e_5,e_2,e_2)
| ~ product(e_5,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_681]) ).
tcf(c_1765,plain,
( equalish(e_3,e_1)
| ~ product(e_2,e_4,e_3)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_739]) ).
tcf(c_1788,plain,
( equalish(e_3,e_2)
| ~ product(e_2,e_3,e_2)
| ~ product(e_2,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_874]) ).
tcf(c_1796,plain,
( equalish(e_5,e_3)
| ~ product(e_5,e_4,e_4)
| ~ product(e_3,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_914]) ).
tcf(c_1808,plain,
( equalish(e_4,e_1)
| ~ product(e_3,e_2,e_4)
| ~ product(e_3,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_1820,plain,
( equalish(e_5,e_4)
| ~ product(e_3,e_5,e_2)
| ~ product(e_3,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_961]) ).
tcf(c_1826,plain,
( equalish(e_4,e_2)
| ~ product(e_5,e_4,e_2)
| ~ product(e_5,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_964]) ).
tcf(c_1836,plain,
( equalish(e_5,e_4)
| ~ product(e_5,e_5,e_5)
| ~ product(e_4,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_1001]) ).
tcf(c_1860,plain,
( equalish(e_1,e_2)
| ~ product(e_3,e_5,e_2)
| ~ product(e_3,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_1121]) ).
tcf(c_1882,plain,
( equalish(e_1,e_5)
| ~ product(e_5,e_4,e_4)
| ~ product(e_1,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_201]) ).
tcf(c_1889,plain,
( equalish(e_5,e_1)
| ~ product(e_1,e_5,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_303]) ).
tcf(c_1910,plain,
! [X0: $i,X1: $i] :
( product(X0,e_3,X1)
| ~ product(e_3,e_2,X1)
| ~ product(X0,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_403]) ).
tcf(c_1927,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,e_3)
| ~ product(X1,e_2,e_3)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_503]) ).
tcf(c_1941,plain,
! [X0: $i] :
( equalish(e_5,e_3)
| ~ product(X0,e_5,e_3)
| ~ product(X0,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_319]) ).
tcf(c_1943,plain,
! [X0: $i] :
( equalish(e_3,e_2)
| ~ product(X0,e_3,e_3)
| ~ product(X0,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_1945,plain,
! [X0: $i] :
( equalish(e_2,e_3)
| ~ product(X0,e_3,e_3)
| ~ product(X0,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_215]) ).
tcf(c_1948,plain,
( equalish(e_2,e_3)
| ~ product(e_1,e_3,e_3)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_1945]) ).
tcf(c_1950,plain,
( equalish(e_3,e_2)
| ~ product(e_1,e_3,e_3)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_1943]) ).
tcf(c_1952,plain,
( equalish(e_5,e_3)
| ~ product(e_1,e_5,e_3)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_1941]) ).
tcf(c_1958,plain,
( equalish(e_2,e_1)
| ~ product(e_2,e_3,e_3)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_1959,plain,
( product(e_2,e_1,e_3)
| ~ product(e_2,e_3,e_1)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_382]) ).
tcf(c_1970,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,e_3)
| ~ product(X1,e_3,e_3)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_503]) ).
tcf(c_1974,plain,
! [X0: $i,X1: $i] :
( product(X0,e_4,X1)
| ~ product(e_4,e_4,X1)
| ~ product(X0,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_1976,plain,
! [X0: $i] :
( equalish(e_4,e_2)
| ~ product(X0,e_4,e_4)
| ~ product(X0,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_277]) ).
tcf(c_1977,plain,
! [X0: $i] :
( equalish(e_4,e_1)
| ~ product(X0,e_4,e_4)
| ~ product(X0,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_269]) ).
tcf(c_1984,plain,
( equalish(e_4,e_1)
| ~ product(e_1,e_4,e_4)
| ~ product(e_1,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_1977]) ).
tcf(c_1985,plain,
( equalish(e_4,e_2)
| ~ product(e_1,e_4,e_4)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_1976]) ).
tcf(c_1987,plain,
( product(e_1,e_4,e_1)
| ~ product(e_4,e_4,e_1)
| ~ product(e_1,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_1974]) ).
tcf(c_1988,plain,
! [X0: $i] :
( equalish(e_5,e_4)
| ~ product(X0,e_5,e_4)
| ~ product(X0,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_1990,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ product(X0,e_4,e_4)
| ~ product(X0,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_287]) ).
tcf(c_1991,plain,
! [X0: $i] :
( equalish(e_4,e_2)
| ~ product(X0,e_4,e_4)
| ~ product(X0,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_279]) ).
tcf(c_1992,plain,
! [X0: $i] :
( equalish(e_4,e_1)
| ~ product(X0,e_4,e_4)
| ~ product(X0,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_271]) ).
tcf(c_1999,plain,
( equalish(e_4,e_1)
| ~ product(e_1,e_4,e_4)
| ~ product(e_1,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_1992]) ).
tcf(c_2000,plain,
( equalish(e_4,e_2)
| ~ product(e_1,e_4,e_4)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_1991]) ).
tcf(c_2001,plain,
( equalish(e_4,e_3)
| ~ product(e_1,e_4,e_4)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_1990]) ).
tcf(c_2003,plain,
( equalish(e_5,e_4)
| ~ product(e_1,e_5,e_4)
| ~ product(e_1,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_1988]) ).
tcf(c_2008,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_4,e_4)
| ~ product(e_1,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_917]) ).
tcf(c_2009,plain,
( product(e_3,e_1,e_4)
| ~ product(e_3,e_4,e_1)
| ~ product(e_1,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_388]) ).
tcf(c_2010,plain,
( product(e_2,e_1,e_4)
| ~ product(e_2,e_4,e_1)
| ~ product(e_1,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_384]) ).
tcf(c_2024,plain,
! [X0: $i] :
( product(e_5,e_4,e_2)
| ~ product(e_5,X0,e_4)
| ~ product(e_4,X0,e_2) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_2025,plain,
! [X0: $i] :
( product(e_4,e_2,e_3)
| ~ product(e_4,X0,e_2)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_762]) ).
tcf(c_2032,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ product(e_4,X0,e_2)
| ~ product(e_3,X0,e_2) ),
inference(instantiation,[status(thm)],[c_289]) ).
tcf(c_2033,plain,
! [X0: $i] :
( equalish(e_4,e_2)
| ~ product(e_4,X0,e_2)
| ~ product(e_2,X0,e_2) ),
inference(instantiation,[status(thm)],[c_281]) ).
tcf(c_2044,plain,
! [X0: $i,X1: $i] :
( product(X0,e_4,e_2)
| ~ product(e_4,X1,e_2)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_2065,plain,
( product(e_5,e_5,e_5)
| product(e_5,e_5,e_4)
| product(e_5,e_5,e_3)
| product(e_5,e_5,e_2)
| product(e_5,e_5,e_1)
| ~ group_element(e_5) ),
inference(instantiation,[status(thm)],[c_430]) ).
tcf(c_2066,plain,
! [X0: $i] :
( product(e_5,e_2,X0)
| ~ product(e_5,e_5,e_2)
| ~ product(e_2,e_5,X0) ),
inference(instantiation,[status(thm)],[c_432]) ).
tcf(c_2069,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,e_2)
| ~ product(X1,e_5,e_2)
| ~ product(X0,e_5,X1) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_2075,plain,
! [X0: $i,X1: $i] :
( product(e_5,e_5,X1)
| ~ product(e_5,X0,e_5)
| ~ product(e_5,X0,X1) ),
inference(instantiation,[status(thm)],[c_427]) ).
tcf(c_2085,plain,
! [X0: $i] :
( equalish(e_5,e_1)
| ~ product(e_5,X0,e_5)
| ~ product(e_1,X0,e_5) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_2089,plain,
! [X0: $i,X1: $i] :
( product(X0,e_5,e_5)
| ~ product(e_5,X1,e_5)
| ~ product(X0,X1,e_5) ),
inference(instantiation,[status(thm)],[c_564]) ).
tcf(c_2134,plain,
( equalish(e_3,e_1)
| ~ cycle(e_4,e_0)
| ~ cycle(e_3,e_3)
| ~ greater(e_3,e_0)
| ~ next(e_3,e_4)
| ~ next(e_0,e_1) ),
inference(instantiation,[status(thm)],[c_599]) ).
tcf(c_2148,plain,
( equalish(e_1,e_2)
| ~ product(e_3,e_4,e_2)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_173]) ).
tcf(c_2172,plain,
! [X0: $i,X1: $i] :
( ~ cycle(e_5,e_0)
| ~ cycle(e_4,e_0)
| ~ next(e_4,e_5)
| ~ greater(e_4,X0)
| ~ greater(X1,e_0)
| ~ cycle(X0,X1) ),
inference(instantiation,[status(thm)],[c_367]) ).
tcf(c_2208,plain,
( product(e_5,e_1,e_2)
| ~ product(e_5,e_3,e_1)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_2209,plain,
( product(e_1,e_2,e_3)
| ~ product(e_2,e_3,e_3)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_762]) ).
tcf(c_2224,plain,
! [X0: $i] :
( product(e_1,e_3,X0)
| ~ product(e_1,e_4,e_3)
| ~ product(e_3,e_4,X0) ),
inference(instantiation,[status(thm)],[c_403]) ).
tcf(c_2229,plain,
( product(e_1,e_3,e_1)
| ~ product(e_3,e_4,e_1)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_2224]) ).
tcf(c_2230,plain,
( equalish(e_5,e_4)
| ~ product(e_1,e_5,e_3)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_2233,plain,
( equalish(e_4,e_2)
| ~ product(e_1,e_4,e_3)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_279]) ).
tcf(c_2239,plain,
( equalish(e_2,e_1)
| ~ product(e_2,e_4,e_3)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_2259,plain,
! [X0: $i] :
( product(X0,e_5,e_1)
| ~ product(e_5,e_5,e_1)
| ~ product(X0,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_1043]) ).
tcf(c_2260,plain,
( product(e_1,e_5,e_1)
| ~ product(e_5,e_5,e_1)
| ~ product(e_1,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_2259]) ).
tcf(c_2307,plain,
( product(e_2,e_2,e_2)
| ~ product(e_2,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_1579]) ).
tcf(c_2367,plain,
! [X0: $i] :
( product(e_5,e_5,e_5)
| ~ product(e_5,X0,e_5) ),
inference(instantiation,[status(thm)],[c_2075]) ).
tcf(c_2440,plain,
( equalish(e_2,e_5)
| ~ product(e_5,e_3,e_4)
| ~ product(e_2,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_233]) ).
tcf(c_2443,plain,
( equalish(e_5,e_3)
| ~ product(e_2,e_5,e_4)
| ~ product(e_2,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_319]) ).
tcf(c_2457,plain,
! [X0: $i] :
( product(X0,e_2,e_4)
| ~ product(e_2,e_3,e_4)
| ~ product(X0,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_394]) ).
tcf(c_2458,plain,
( product(e_1,e_2,e_4)
| ~ product(e_2,e_3,e_4)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_2457]) ).
tcf(c_2475,plain,
( equalish(e_5,e_2)
| ~ product(e_2,e_5,e_4)
| ~ product(e_2,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_311]) ).
tcf(c_2478,plain,
( equalish(e_1,e_2)
| ~ product(e_2,e_2,e_4)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_175]) ).
tcf(c_2491,plain,
! [X0: $i] :
( product(X0,e_2,e_4)
| ~ product(e_2,e_2,e_4)
| ~ product(X0,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_394]) ).
tcf(c_2492,plain,
( product(e_1,e_2,e_4)
| ~ product(e_2,e_2,e_4)
| ~ product(e_1,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_2491]) ).
tcf(c_2497,plain,
( product(e_5,e_2,e_4)
| ~ product(e_5,e_2,e_2)
| ~ product(e_2,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_1675]) ).
tcf(c_2522,plain,
( product(e_5,e_4,e_2)
| ~ product(e_5,e_2,e_4)
| ~ product(e_4,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_704]) ).
tcf(c_2527,plain,
( product(e_3,e_4,e_2)
| ~ product(e_4,e_2,e_2)
| ~ product(e_3,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_907]) ).
tcf(c_2529,plain,
! [X0: $i] :
( product(X0,e_4,e_2)
| ~ product(e_4,e_2,e_2)
| ~ product(X0,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_2044]) ).
tcf(c_2530,plain,
( product(e_1,e_4,e_2)
| ~ product(e_4,e_2,e_2)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_2529]) ).
tcf(c_2537,plain,
( equalish(e_5,e_2)
| ~ product(e_1,e_5,e_4)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_311]) ).
tcf(c_2545,plain,
( equalish(e_3,e_4)
| ~ product(e_1,e_2,e_4)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_253]) ).
tcf(c_2550,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_2,e_4)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_917]) ).
tcf(c_2597,plain,
( equalish(e_2,e_3)
| ~ product(e_3,e_3,e_3)
| ~ product(e_2,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_217]) ).
tcf(c_2605,plain,
( product(e_2,e_3,e_1)
| ~ product(e_3,e_4,e_1)
| ~ product(e_2,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_737]) ).
tcf(c_2606,plain,
( equalish(e_5,e_3)
| ~ product(e_5,e_4,e_1)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_321]) ).
tcf(c_2607,plain,
( equalish(e_3,e_5)
| ~ product(e_5,e_4,e_1)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_265]) ).
tcf(c_2608,plain,
( equalish(e_3,e_2)
| ~ product(e_3,e_4,e_1)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_249]) ).
tcf(c_2609,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_4,e_1)
| ~ product(e_1,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_241]) ).
tcf(c_2610,plain,
( equalish(e_2,e_3)
| ~ product(e_3,e_4,e_1)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_217]) ).
tcf(c_2612,plain,
( equalish(e_5,e_4)
| ~ product(e_3,e_5,e_1)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_2615,plain,
( equalish(e_4,e_2)
| ~ product(e_3,e_4,e_1)
| ~ product(e_3,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_279]) ).
tcf(c_2649,plain,
( equalish(e_5,e_4)
| ~ product(e_4,e_5,e_2)
| ~ product(e_4,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_961]) ).
tcf(c_2651,plain,
( product(e_4,e_2,e_3)
| ~ product(e_4,e_4,e_2)
| ~ product(e_2,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_2025]) ).
tcf(c_2652,plain,
( product(e_5,e_4,e_2)
| ~ product(e_5,e_4,e_4)
| ~ product(e_4,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_2024]) ).
tcf(c_2654,plain,
( product(e_3,e_4,e_2)
| ~ product(e_4,e_4,e_2)
| ~ product(e_3,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_907]) ).
tcf(c_2657,plain,
! [X0: $i] :
( product(X0,e_4,e_2)
| ~ product(e_4,e_4,e_2)
| ~ product(X0,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_2044]) ).
tcf(c_2658,plain,
( product(e_1,e_4,e_2)
| ~ product(e_4,e_4,e_2)
| ~ product(e_1,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_2657]) ).
tcf(c_2673,plain,
( product(e_3,e_4,e_3)
| ~ product(e_4,e_1,e_3)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_926]) ).
tcf(c_2680,plain,
( equalish(e_2,e_4)
| ~ product(e_4,e_1,e_3)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_2687,plain,
! [X0: $i] :
( product(e_1,e_4,X0)
| ~ product(e_1,e_5,e_4)
| ~ product(e_4,e_5,X0) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_2688,plain,
( equalish(e_4,e_3)
| ~ product(e_1,e_5,e_4)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_285]) ).
tcf(c_2689,plain,
( equalish(e_4,e_2)
| ~ product(e_1,e_5,e_4)
| ~ product(e_1,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_277]) ).
tcf(c_2690,plain,
( equalish(e_4,e_1)
| ~ product(e_1,e_5,e_4)
| ~ product(e_1,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_269]) ).
tcf(c_2694,plain,
( product(e_1,e_4,e_1)
| ~ product(e_4,e_5,e_1)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_2687]) ).
tcf(c_2698,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_5,e_4)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_917]) ).
tcf(c_2699,plain,
( product(e_3,e_1,e_4)
| ~ product(e_3,e_5,e_1)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_388]) ).
tcf(c_2700,plain,
( product(e_2,e_1,e_4)
| ~ product(e_2,e_5,e_1)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_384]) ).
tcf(c_2716,plain,
( product(e_2,e_3,e_2)
| ~ product(e_3,e_5,e_2)
| ~ product(e_2,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_737]) ).
tcf(c_2718,plain,
( equalish(e_3,e_5)
| ~ product(e_5,e_5,e_2)
| ~ product(e_3,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_265]) ).
tcf(c_2719,plain,
( equalish(e_3,e_2)
| ~ product(e_3,e_5,e_2)
| ~ product(e_2,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_249]) ).
tcf(c_2720,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_5,e_2)
| ~ product(e_1,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_241]) ).
tcf(c_2722,plain,
( equalish(e_1,e_3)
| ~ product(e_3,e_5,e_2)
| ~ product(e_1,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_185]) ).
tcf(c_2725,plain,
! [X0: $i] :
( product(e_3,e_2,X0)
| ~ product(e_3,e_5,e_2)
| ~ product(e_2,e_5,X0) ),
inference(instantiation,[status(thm)],[c_408]) ).
tcf(c_2726,plain,
( product(e_3,e_2,e_1)
| ~ product(e_3,e_5,e_2)
| ~ product(e_2,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_2725]) ).
tcf(c_2733,plain,
! [X0: $i] :
( product(X0,e_3,e_2)
| ~ product(e_3,e_5,e_2)
| ~ product(X0,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_2069]) ).
tcf(c_2734,plain,
( product(e_1,e_3,e_2)
| ~ product(e_3,e_5,e_2)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_2733]) ).
tcf(c_2755,plain,
( product(e_4,e_2,e_3)
| ~ product(e_4,e_5,e_2)
| ~ product(e_2,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_2025]) ).
tcf(c_2763,plain,
! [X0: $i] :
( product(X0,e_4,e_2)
| ~ product(e_4,e_5,e_2)
| ~ product(X0,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_2044]) ).
tcf(c_2764,plain,
( product(e_1,e_4,e_2)
| ~ product(e_4,e_5,e_2)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_2763]) ).
tcf(c_2790,plain,
! [X0: $i] :
( product(e_5,e_2,X0)
| ~ product(e_5,e_3,e_2)
| ~ product(e_2,e_3,X0) ),
inference(instantiation,[status(thm)],[c_432]) ).
tcf(c_2791,plain,
( product(e_5,e_2,e_1)
| ~ product(e_5,e_3,e_2)
| ~ product(e_2,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_2790]) ).
tcf(c_2795,plain,
( equalish(e_5,e_1)
| ~ product(e_5,e_3,e_2)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_813]) ).
tcf(c_2796,plain,
( product(e_4,e_5,e_2)
| ~ product(e_5,e_3,e_2)
| ~ product(e_4,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_993]) ).
tcf(c_2798,plain,
! [X0: $i] :
( product(X0,e_5,e_2)
| ~ product(e_5,e_3,e_2)
| ~ product(X0,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_2799,plain,
( product(e_1,e_5,e_2)
| ~ product(e_5,e_3,e_2)
| ~ product(e_1,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_2798]) ).
tcf(c_2879,plain,
( ~ cycle(e_5,e_0)
| ~ cycle(e_4,e_0)
| ~ cycle(e_3,e_1)
| ~ greater(e_4,e_3)
| ~ greater(e_1,e_0)
| ~ next(e_4,e_5) ),
inference(instantiation,[status(thm)],[c_2172]) ).
tcf(c_2880,plain,
( ~ cycle(e_5,e_0)
| ~ cycle(e_4,e_0)
| ~ cycle(e_2,e_2)
| ~ greater(e_4,e_2)
| ~ greater(e_2,e_0)
| ~ next(e_4,e_5) ),
inference(instantiation,[status(thm)],[c_2172]) ).
tcf(c_2881,plain,
! [X0: $i] :
( equalish(e_5,e_2)
| ~ product(X0,e_5,e_5)
| ~ product(X0,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_311]) ).
tcf(c_2883,plain,
! [X0: $i] :
( equalish(e_2,e_1)
| ~ product(X0,e_2,e_5)
| ~ product(X0,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_2893,plain,
! [X0: $i,X1: $i] :
( product(X0,e_5,X1)
| ~ product(e_5,e_2,X1)
| ~ product(X0,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_427]) ).
tcf(c_2894,plain,
! [X0: $i] :
( equalish(e_5,e_4)
| ~ product(X0,e_2,e_5)
| ~ product(X0,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_325]) ).
tcf(c_2909,plain,
( equalish(e_5,e_4)
| ~ product(e_1,e_2,e_5)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_2894]) ).
tcf(c_2910,plain,
( product(e_1,e_5,e_1)
| ~ product(e_5,e_2,e_1)
| ~ product(e_1,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_2893]) ).
tcf(c_2922,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,e_5)
| ~ product(X1,e_2,e_5)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_564]) ).
tcf(c_2942,plain,
( equalish(e_5,e_1)
| ~ product(e_5,e_2,e_3)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_2943,plain,
( equalish(e_1,e_5)
| ~ product(e_5,e_2,e_3)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_201]) ).
tcf(c_2944,plain,
! [X0: $i] :
( product(e_5,e_3,X0)
| ~ product(e_5,e_2,e_3)
| ~ product(e_3,e_2,X0) ),
inference(instantiation,[status(thm)],[c_1910]) ).
tcf(c_2949,plain,
( product(e_5,e_3,e_4)
| ~ product(e_5,e_2,e_3)
| ~ product(e_3,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_908]) ).
tcf(c_2951,plain,
! [X0: $i] :
( product(X0,e_5,e_3)
| ~ product(e_5,e_2,e_3)
| ~ product(X0,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_1927]) ).
tcf(c_2952,plain,
( product(e_1,e_5,e_3)
| ~ product(e_5,e_2,e_3)
| ~ product(e_1,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_2951]) ).
tcf(c_2990,plain,
! [X0: $i] :
( equalish(e_5,e_3)
| ~ product(X0,e_5,e_5)
| ~ product(X0,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_319]) ).
tcf(c_2992,plain,
! [X0: $i] :
( equalish(e_3,e_2)
| ~ product(X0,e_3,e_5)
| ~ product(X0,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_2994,plain,
! [X0: $i] :
( equalish(e_2,e_3)
| ~ product(X0,e_3,e_5)
| ~ product(X0,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_215]) ).
tcf(c_2997,plain,
( equalish(e_2,e_3)
| ~ product(e_1,e_3,e_5)
| ~ product(e_1,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_2994]) ).
tcf(c_2999,plain,
( equalish(e_3,e_2)
| ~ product(e_1,e_3,e_5)
| ~ product(e_1,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_2992]) ).
tcf(c_3004,plain,
! [X0: $i] :
( product(X0,e_5,e_5)
| ~ product(e_5,e_3,e_5)
| ~ product(X0,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_2089]) ).
tcf(c_3005,plain,
! [X0: $i,X1: $i] :
( product(X0,e_5,X1)
| ~ product(e_5,e_3,X1)
| ~ product(X0,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_427]) ).
tcf(c_3022,plain,
( product(e_1,e_5,e_1)
| ~ product(e_5,e_3,e_1)
| ~ product(e_1,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_3005]) ).
tcf(c_3023,plain,
( product(e_1,e_5,e_5)
| ~ product(e_5,e_3,e_5)
| ~ product(e_1,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_3004]) ).
tcf(c_3048,plain,
! [X0: $i] :
( equalish(e_5,e_4)
| ~ product(X0,e_5,e_3)
| ~ product(X0,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_3050,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ product(X0,e_4,e_3)
| ~ product(X0,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_287]) ).
tcf(c_3051,plain,
! [X0: $i] :
( equalish(e_4,e_2)
| ~ product(X0,e_4,e_3)
| ~ product(X0,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_279]) ).
tcf(c_3052,plain,
! [X0: $i] :
( equalish(e_4,e_1)
| ~ product(X0,e_4,e_3)
| ~ product(X0,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_271]) ).
tcf(c_3066,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,e_3)
| ~ product(X1,e_4,e_3)
| ~ product(X0,e_4,X1) ),
inference(instantiation,[status(thm)],[c_503]) ).
tcf(c_3128,plain,
! [X0: $i,X1: $i] :
( product(e_4,e_3,X1)
| ~ product(e_4,X0,e_3)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_403]) ).
tcf(c_3138,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ product(e_4,X0,e_3)
| ~ product(e_3,X0,e_3) ),
inference(instantiation,[status(thm)],[c_289]) ).
tcf(c_3139,plain,
! [X0: $i] :
( equalish(e_4,e_2)
| ~ product(e_4,X0,e_3)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_281]) ).
tcf(c_3140,plain,
! [X0: $i] :
( equalish(e_4,e_1)
| ~ product(e_4,X0,e_3)
| ~ product(e_1,X0,e_3) ),
inference(instantiation,[status(thm)],[c_273]) ).
tcf(c_3156,plain,
! [X0: $i,X1: $i] :
( product(X0,e_4,X1)
| ~ product(e_4,e_5,X1)
| ~ product(X0,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_3164,plain,
! [X0: $i] :
( equalish(e_5,e_1)
| ~ product(X0,e_5,e_4)
| ~ product(X0,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_303]) ).
tcf(c_3177,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,e_4)
| ~ product(X1,e_5,e_4)
| ~ product(X0,e_5,X1) ),
inference(instantiation,[status(thm)],[c_563]) ).
tcf(c_3360,plain,
( product(e_2,e_1,e_5)
| ~ product(e_2,e_3,e_1)
| ~ product(e_1,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_386]) ).
tcf(c_3391,plain,
( equalish(e_3,e_2)
| ~ product(e_5,e_3,e_2)
| ~ product(e_5,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_874]) ).
tcf(c_3458,plain,
! [X0: $i] :
( product(X0,e_4,e_3)
| ~ product(e_4,e_2,e_3)
| ~ product(X0,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_1927]) ).
tcf(c_3562,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_5,e_2)
| ~ product(e_3,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_2032]) ).
tcf(c_3564,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_5,e_2)
| ~ product(e_2,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_2033]) ).
tcf(c_3675,plain,
( product(e_3,e_4,e_5)
| ~ product(e_4,e_1,e_5)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_926]) ).
tcf(c_3834,plain,
! [X0: $i] :
( product(X0,e_4,e_4)
| ~ product(e_4,e_5,e_4)
| ~ product(X0,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_3177]) ).
tcf(c_3837,plain,
( product(e_3,e_2,e_4)
| ~ product(e_3,e_5,e_2)
| ~ product(e_2,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_3177]) ).
tcf(c_3885,plain,
( ~ cycle(e_5,e_0)
| ~ cycle(e_4,e_0)
| ~ cycle(e_3,e_4)
| ~ greater(e_4,e_3)
| ~ greater(e_4,e_0)
| ~ next(e_4,e_5) ),
inference(instantiation,[status(thm)],[c_2172]) ).
tcf(c_3986,plain,
! [X0: $i] :
( product(X0,e_2,e_3)
| ~ product(e_2,e_2,e_3)
| ~ product(X0,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_762]) ).
tcf(c_3987,plain,
( product(e_1,e_2,e_3)
| ~ product(e_2,e_2,e_3)
| ~ product(e_1,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_3986]) ).
tcf(c_4008,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,e_2)
| ~ product(X1,e_2,e_2)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_4092,plain,
( equalish(e_1,e_2)
| ~ product(e_2,e_2,e_5)
| ~ product(e_1,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_177]) ).
tcf(c_4103,plain,
! [X0: $i] :
( product(X0,e_2,e_5)
| ~ product(e_2,e_2,e_5)
| ~ product(X0,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_394]) ).
tcf(c_4104,plain,
( product(e_1,e_2,e_5)
| ~ product(e_2,e_2,e_5)
| ~ product(e_1,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_4103]) ).
tcf(c_4110,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_2,e_5)
| ~ product(e_2,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_1004]) ).
tcf(c_4138,plain,
( product(e_5,e_3,e_3)
| ~ product(e_5,e_2,e_3)
| ~ product(e_3,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_2944]) ).
tcf(c_4139,plain,
! [X0: $i] :
( product(X0,e_3,e_3)
| ~ product(e_3,e_2,e_3)
| ~ product(X0,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_1927]) ).
tcf(c_4140,plain,
( product(e_1,e_3,e_3)
| ~ product(e_3,e_2,e_3)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_4139]) ).
tcf(c_4160,plain,
( product(e_3,e_1,e_2)
| ~ product(e_3,e_2,e_1)
| ~ product(e_1,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_1295]) ).
tcf(c_4191,plain,
( product(e_2,e_2,e_2)
| ~ product(e_2,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_1353]) ).
tcf(c_4244,plain,
( equalish(e_1,e_2)
| ~ product(e_2,e_4,e_4)
| ~ product(e_1,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_177]) ).
tcf(c_4245,plain,
( product(e_2,e_4,e_5)
| ~ product(e_4,e_4,e_5)
| ~ product(e_2,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_1037]) ).
tcf(c_4253,plain,
( product(e_2,e_4,e_3)
| ~ product(e_4,e_4,e_3)
| ~ product(e_2,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_3066]) ).
tcf(c_4262,plain,
! [X0: $i] :
( product(X0,e_2,e_4)
| ~ product(e_2,e_4,e_4)
| ~ product(X0,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_394]) ).
tcf(c_4263,plain,
( product(e_1,e_2,e_4)
| ~ product(e_2,e_4,e_4)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_4262]) ).
tcf(c_4264,plain,
! [X0: $i] :
( product(e_2,e_4,X0)
| ~ product(e_2,e_4,e_4)
| ~ product(e_4,e_4,X0) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_4265,plain,
( product(e_2,e_4,e_1)
| ~ product(e_4,e_4,e_1)
| ~ product(e_2,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_4264]) ).
tcf(c_4268,plain,
( product(e_2,e_4,e_2)
| ~ product(e_4,e_4,e_2)
| ~ product(e_2,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_2657]) ).
tcf(c_4272,plain,
( equalish(e_4,e_1)
| ~ product(e_2,e_4,e_4)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_1992]) ).
tcf(c_4291,plain,
( product(e_2,e_3,e_5)
| ~ product(e_3,e_3,e_5)
| ~ product(e_2,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_737]) ).
tcf(c_4297,plain,
( equalish(e_1,e_3)
| ~ product(e_3,e_3,e_5)
| ~ product(e_1,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_185]) ).
tcf(c_4386,plain,
( equalish(e_1,e_2)
| ~ product(e_2,e_5,e_4)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_177]) ).
tcf(c_4398,plain,
! [X0: $i] :
( product(X0,e_2,e_4)
| ~ product(e_2,e_5,e_4)
| ~ product(X0,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_394]) ).
tcf(c_4399,plain,
( product(e_1,e_2,e_4)
| ~ product(e_2,e_5,e_4)
| ~ product(e_1,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_4398]) ).
tcf(c_4400,plain,
! [X0: $i] :
( product(e_2,e_4,X0)
| ~ product(e_2,e_5,e_4)
| ~ product(e_4,e_5,X0) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_4401,plain,
( product(e_2,e_4,e_1)
| ~ product(e_4,e_5,e_1)
| ~ product(e_2,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_4400]) ).
tcf(c_4426,plain,
! [X0: $i] :
( product(e_4,e_3,X0)
| ~ product(e_4,e_5,e_3)
| ~ product(e_3,e_5,X0) ),
inference(instantiation,[status(thm)],[c_3128]) ).
tcf(c_4434,plain,
! [X0: $i] :
( product(X0,e_4,e_3)
| ~ product(e_4,e_5,e_3)
| ~ product(X0,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_3156]) ).
tcf(c_4435,plain,
( product(e_1,e_4,e_3)
| ~ product(e_4,e_5,e_3)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_4434]) ).
tcf(c_4455,plain,
! [X0: $i] :
( product(X0,e_5,e_4)
| ~ product(e_5,e_1,e_4)
| ~ product(X0,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_563]) ).
tcf(c_4456,plain,
( product(e_1,e_5,e_4)
| ~ product(e_5,e_1,e_4)
| ~ product(e_1,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_4455]) ).
tcf(c_4459,plain,
( equalish(e_4,e_5)
| ~ product(e_5,e_5,e_5)
| ~ product(e_5,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_295]) ).
tcf(c_4482,plain,
( product(e_5,e_5,e_5)
| ~ product(e_5,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_2367]) ).
tcf(c_4501,plain,
( equalish(e_1,e_5)
| ~ product(e_5,e_3,e_3)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_201]) ).
tcf(c_4505,plain,
( equalish(e_3,e_2)
| ~ product(e_5,e_3,e_3)
| ~ product(e_5,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_1943]) ).
tcf(c_4514,plain,
( equalish(e_5,e_2)
| ~ product(e_5,e_3,e_3)
| ~ product(e_2,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_729]) ).
tcf(c_4517,plain,
! [X0: $i] :
( product(X0,e_5,e_3)
| ~ product(e_5,e_3,e_3)
| ~ product(X0,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_1970]) ).
tcf(c_4518,plain,
( product(e_1,e_5,e_3)
| ~ product(e_5,e_3,e_3)
| ~ product(e_1,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_4517]) ).
tcf(c_4563,plain,
! [X0: $i,X1: $i] :
( product(e_5,e_4,X1)
| ~ product(e_5,X0,e_4)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_4574,plain,
! [X0: $i] :
( equalish(e_5,e_1)
| ~ product(e_5,X0,e_4)
| ~ product(e_1,X0,e_4) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_4802,plain,
( equalish(e_5,e_4)
| ~ product(e_5,e_4,e_5)
| ~ product(e_4,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_1001]) ).
tcf(c_4866,plain,
( equalish(e_5,e_2)
| ~ product(e_5,e_5,e_5)
| ~ product(e_5,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_2881]) ).
tcf(c_4910,plain,
( equalish(e_5,e_3)
| ~ product(e_5,e_5,e_5)
| ~ product(e_5,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_2990]) ).
tcf(c_4976,plain,
( equalish(e_5,e_4)
| ~ product(e_4,e_5,e_3)
| ~ product(e_4,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_3048]) ).
tcf(c_4987,plain,
( equalish(e_4,e_3)
| ~ product(e_5,e_4,e_3)
| ~ product(e_5,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_3050]) ).
tcf(c_4993,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_4,e_3)
| ~ product(e_4,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_3051]) ).
tcf(c_4994,plain,
( equalish(e_4,e_2)
| ~ product(e_5,e_4,e_3)
| ~ product(e_5,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_3051]) ).
tcf(c_5048,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_2,e_3)
| ~ product(e_3,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_3138]) ).
tcf(c_5049,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_5,e_3)
| ~ product(e_3,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_3138]) ).
tcf(c_5054,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_5,e_3)
| ~ product(e_2,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_3139]) ).
tcf(c_5058,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_4,e_3)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_3140]) ).
tcf(c_5176,plain,
! [X0: $i,X1: $i] :
( product(e_3,X0,e_2)
| ~ product(e_3,X1,X0)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_408]) ).
tcf(c_5181,plain,
! [X0: $i] :
( product(e_3,X0,e_3)
| ~ product(e_3,e_4,X0)
| ~ product(X0,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_408]) ).
tcf(c_5227,plain,
( product(e_4,e_5,e_2)
| ~ product(e_5,e_5,e_2)
| ~ product(e_4,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_993]) ).
tcf(c_5229,plain,
! [X0: $i] :
( product(X0,e_5,e_2)
| ~ product(e_5,e_5,e_2)
| ~ product(X0,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_2069]) ).
tcf(c_5230,plain,
( product(e_1,e_5,e_2)
| ~ product(e_5,e_5,e_2)
| ~ product(e_1,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_5229]) ).
tcf(c_5370,plain,
( product(e_5,e_4,e_3)
| ~ product(e_5,e_5,e_4)
| ~ product(e_4,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_4434]) ).
tcf(c_5371,plain,
( product(e_4,e_5,e_3)
| ~ product(e_5,e_4,e_3)
| ~ product(e_4,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_1017]) ).
tcf(c_5373,plain,
( equalish(e_5,e_1)
| ~ product(e_5,e_4,e_3)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_5374,plain,
( equalish(e_1,e_5)
| ~ product(e_5,e_4,e_3)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_201]) ).
tcf(c_5391,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_4,e_3)
| ~ product(e_2,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_3139]) ).
tcf(c_5397,plain,
! [X0: $i] :
( product(e_4,e_3,X0)
| ~ product(e_4,e_4,e_3)
| ~ product(e_3,e_4,X0) ),
inference(instantiation,[status(thm)],[c_3128]) ).
tcf(c_5398,plain,
( product(e_4,e_3,e_1)
| ~ product(e_4,e_4,e_3)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_5397]) ).
tcf(c_5470,plain,
( product(e_3,e_4,e_5)
| ~ product(e_4,e_2,e_5)
| ~ product(e_3,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_1037]) ).
tcf(c_5480,plain,
( product(e_3,e_4,e_3)
| ~ product(e_4,e_2,e_3)
| ~ product(e_3,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_3458]) ).
tcf(c_5487,plain,
( equalish(e_5,e_3)
| ~ product(e_5,e_2,e_4)
| ~ product(e_3,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_914]) ).
tcf(c_5508,plain,
( equalish(e_5,e_4)
| ~ product(e_5,e_2,e_4)
| ~ product(e_4,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_5513,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_2,e_4)
| ~ product(e_3,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_257]) ).
tcf(c_5515,plain,
( equalish(e_1,e_4)
| ~ product(e_4,e_2,e_4)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_193]) ).
tcf(c_5526,plain,
! [X0: $i] :
( product(X0,e_1,e_1)
| ~ product(e_1,e_2,e_1)
| ~ product(X0,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_5527,plain,
( product(e_1,e_1,e_1)
| ~ product(e_1,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_5526]) ).
tcf(c_5560,plain,
! [X0: $i] :
( product(X0,e_2,e_5)
| ~ product(e_2,e_3,e_5)
| ~ product(X0,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_394]) ).
tcf(c_5561,plain,
( product(e_1,e_2,e_5)
| ~ product(e_2,e_3,e_5)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_5560]) ).
tcf(c_5568,plain,
( product(e_2,e_5,e_2)
| ~ product(e_5,e_4,e_2)
| ~ product(e_2,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_5571,plain,
( equalish(e_3,e_2)
| ~ product(e_3,e_4,e_5)
| ~ product(e_2,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_249]) ).
tcf(c_5572,plain,
( equalish(e_2,e_3)
| ~ product(e_3,e_4,e_5)
| ~ product(e_2,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_217]) ).
tcf(c_5575,plain,
( equalish(e_2,e_1)
| ~ product(e_2,e_4,e_5)
| ~ product(e_1,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_209]) ).
tcf(c_5576,plain,
( equalish(e_1,e_2)
| ~ product(e_2,e_4,e_5)
| ~ product(e_1,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_177]) ).
tcf(c_5577,plain,
( product(e_2,e_5,e_3)
| ~ product(e_5,e_4,e_3)
| ~ product(e_2,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_3066]) ).
tcf(c_5578,plain,
( equalish(e_5,e_4)
| ~ product(e_2,e_5,e_5)
| ~ product(e_2,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_5580,plain,
( equalish(e_4,e_3)
| ~ product(e_2,e_4,e_5)
| ~ product(e_2,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_287]) ).
tcf(c_5581,plain,
( equalish(e_4,e_2)
| ~ product(e_2,e_4,e_5)
| ~ product(e_2,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_279]) ).
tcf(c_5582,plain,
( equalish(e_4,e_1)
| ~ product(e_2,e_4,e_5)
| ~ product(e_2,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_271]) ).
tcf(c_5587,plain,
! [X0: $i] :
( product(e_2,e_5,X0)
| ~ product(e_2,e_4,e_5)
| ~ product(e_5,e_4,X0) ),
inference(instantiation,[status(thm)],[c_427]) ).
tcf(c_5588,plain,
( equalish(e_5,e_4)
| ~ product(e_2,e_4,e_5)
| ~ product(e_2,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_325]) ).
tcf(c_5596,plain,
( product(e_2,e_5,e_1)
| ~ product(e_5,e_4,e_1)
| ~ product(e_2,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_5587]) ).
tcf(c_5597,plain,
! [X0: $i] :
( product(X0,e_2,e_5)
| ~ product(e_2,e_4,e_5)
| ~ product(X0,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_394]) ).
tcf(c_5598,plain,
( product(e_1,e_2,e_5)
| ~ product(e_2,e_4,e_5)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_5597]) ).
tcf(c_5601,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_4,e_5)
| ~ product(e_2,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_1004]) ).
tcf(c_5602,plain,
( product(e_2,e_5,e_4)
| ~ product(e_5,e_4,e_4)
| ~ product(e_2,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_1725]) ).
tcf(c_5608,plain,
( product(e_3,e_2,e_4)
| ~ product(e_3,e_1,e_2)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_408]) ).
tcf(c_5616,plain,
( product(e_2,e_4,e_5)
| ~ product(e_4,e_1,e_5)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_1037]) ).
tcf(c_5626,plain,
( equalish(e_5,e_1)
| ~ product(e_2,e_5,e_4)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_3164]) ).
tcf(c_5656,plain,
( product(e_2,e_3,e_2)
| ~ product(e_3,e_3,e_2)
| ~ product(e_2,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_723]) ).
tcf(c_5692,plain,
( product(e_3,e_5,e_2)
| ~ product(e_5,e_4,e_2)
| ~ product(e_3,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_5695,plain,
( product(e_3,e_5,e_3)
| ~ product(e_5,e_4,e_3)
| ~ product(e_3,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_3066]) ).
tcf(c_5699,plain,
( equalish(e_4,e_2)
| ~ product(e_3,e_4,e_5)
| ~ product(e_3,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_279]) ).
tcf(c_5700,plain,
( equalish(e_4,e_1)
| ~ product(e_3,e_4,e_5)
| ~ product(e_3,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_271]) ).
tcf(c_5704,plain,
( product(e_3,e_5,e_5)
| ~ product(e_5,e_4,e_5)
| ~ product(e_3,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_2089]) ).
tcf(c_5705,plain,
! [X0: $i] :
( product(e_3,e_5,X0)
| ~ product(e_3,e_4,e_5)
| ~ product(e_5,e_4,X0) ),
inference(instantiation,[status(thm)],[c_427]) ).
tcf(c_5712,plain,
( equalish(e_2,e_5)
| ~ product(e_3,e_4,e_5)
| ~ product(e_3,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_229]) ).
tcf(c_5713,plain,
( equalish(e_1,e_5)
| ~ product(e_3,e_4,e_5)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_197]) ).
tcf(c_5714,plain,
( product(e_3,e_5,e_1)
| ~ product(e_5,e_4,e_1)
| ~ product(e_3,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_5705]) ).
tcf(c_5716,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_4,e_5)
| ~ product(e_3,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_1003]) ).
tcf(c_5717,plain,
( product(e_3,e_5,e_4)
| ~ product(e_5,e_4,e_4)
| ~ product(e_3,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_1725]) ).
tcf(c_5718,plain,
! [X0: $i] :
( product(X0,e_3,e_5)
| ~ product(e_3,e_4,e_5)
| ~ product(X0,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_564]) ).
tcf(c_5719,plain,
( product(e_1,e_3,e_5)
| ~ product(e_3,e_4,e_5)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_5718]) ).
tcf(c_5726,plain,
( equalish(e_2,e_3)
| ~ product(e_3,e_5,e_5)
| ~ product(e_2,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_217]) ).
tcf(c_5728,plain,
( equalish(e_2,e_5)
| ~ product(e_5,e_5,e_5)
| ~ product(e_2,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_233]) ).
tcf(c_5744,plain,
( equalish(e_5,e_1)
| ~ product(e_2,e_5,e_5)
| ~ product(e_2,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_303]) ).
tcf(c_5750,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_5,e_5)
| ~ product(e_2,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_1004]) ).
tcf(c_5756,plain,
( product(e_5,e_2,e_5)
| ~ product(e_5,e_5,e_2)
| ~ product(e_2,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_2066]) ).
tcf(c_5757,plain,
( product(e_3,e_2,e_5)
| ~ product(e_3,e_5,e_2)
| ~ product(e_2,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_2725]) ).
tcf(c_5771,plain,
( equalish(e_1,e_5)
| ~ product(e_3,e_5,e_5)
| ~ product(e_3,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_197]) ).
tcf(c_5778,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_5,e_5)
| ~ product(e_3,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_1003]) ).
tcf(c_5785,plain,
( product(e_4,e_3,e_5)
| ~ product(e_4,e_5,e_3)
| ~ product(e_3,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_4426]) ).
tcf(c_5788,plain,
( product(e_5,e_3,e_2)
| ~ product(e_5,e_1,e_3)
| ~ product(e_3,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_5800,plain,
( product(e_4,e_5,e_3)
| ~ product(e_5,e_1,e_3)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_1017]) ).
tcf(c_5805,plain,
( equalish(e_4,e_1)
| ~ product(e_5,e_4,e_3)
| ~ product(e_5,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_3052]) ).
tcf(c_5851,plain,
( product(e_5,e_5,e_5)
| ~ product(e_5,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_2367]) ).
tcf(c_5865,plain,
( equalish(e_3,e_1)
| ~ product(e_5,e_3,e_4)
| ~ product(e_5,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_239]) ).
tcf(c_5967,plain,
( ~ cycle(e_5,e_0)
| ~ cycle(e_4,e_0)
| ~ cycle(e_3,e_2)
| ~ greater(e_4,e_3)
| ~ greater(e_2,e_0)
| ~ next(e_4,e_5) ),
inference(instantiation,[status(thm)],[c_2172]) ).
tcf(c_5981,plain,
( equalish(e_4,e_3)
| ~ cycle(e_2,e_3)
| ~ greater(e_3,e_0)
| ~ next(e_2,e_3)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_561]) ).
tcf(c_6071,plain,
! [X0: $i] :
( product(e_3,e_1,e_2)
| ~ product(e_3,X0,e_1)
| ~ product(e_1,X0,e_2) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_6108,plain,
! [X0: $i] :
( product(e_4,e_5,e_3)
| ~ product(e_5,X0,e_3)
| ~ product(e_4,X0,e_5) ),
inference(instantiation,[status(thm)],[c_1017]) ).
tcf(c_6118,plain,
! [X0: $i,X1: $i] :
( product(X0,e_5,e_3)
| ~ product(e_5,X1,e_3)
| ~ product(X0,X1,e_5) ),
inference(instantiation,[status(thm)],[c_503]) ).
tcf(c_6280,plain,
( equalish(e_5,e_1)
| ~ product(e_5,e_3,e_4)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_4574]) ).
tcf(c_6310,plain,
( equalish(e_3,e_1)
| ~ product(e_5,e_3,e_2)
| ~ product(e_5,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_875]) ).
tcf(c_6632,plain,
( equalish(e_5,e_3)
| ~ product(e_1,e_5,e_4)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_319]) ).
tcf(c_6634,plain,
( equalish(e_3,e_2)
| ~ product(e_1,e_3,e_4)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_6635,plain,
( equalish(e_3,e_1)
| ~ product(e_1,e_3,e_4)
| ~ product(e_1,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_239]) ).
tcf(c_6636,plain,
( equalish(e_2,e_3)
| ~ product(e_1,e_3,e_4)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_215]) ).
tcf(c_6639,plain,
! [X0: $i] :
( product(e_1,e_4,X0)
| ~ product(e_1,e_3,e_4)
| ~ product(e_4,e_3,X0) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_6646,plain,
( product(e_1,e_4,e_1)
| ~ product(e_4,e_3,e_1)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_6639]) ).
tcf(c_6648,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_3,e_4)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_917]) ).
tcf(c_6650,plain,
( product(e_2,e_1,e_4)
| ~ product(e_2,e_3,e_1)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_384]) ).
tcf(c_6782,plain,
( equalish(e_2,e_1)
| ~ product(e_1,e_4,e_2)
| ~ product(e_1,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_205]) ).
tcf(c_6785,plain,
( product(e_1,e_2,e_3)
| ~ product(e_2,e_4,e_3)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_3066]) ).
tcf(c_6794,plain,
( product(e_3,e_1,e_2)
| ~ product(e_3,e_4,e_1)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_6071]) ).
tcf(c_6869,plain,
( equalish(e_5,e_2)
| ~ product(e_5,e_4,e_3)
| ~ product(e_2,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_729]) ).
tcf(c_7008,plain,
( equalish(e_3,e_2)
| ~ product(e_4,e_3,e_3)
| ~ product(e_4,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_1943]) ).
tcf(c_7123,plain,
( equalish(e_5,e_2)
| ~ product(e_5,e_2,e_2)
| ~ product(e_2,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_313]) ).
tcf(c_7143,plain,
( equalish(e_1,e_3)
| ~ product(e_3,e_2,e_5)
| ~ product(e_1,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_185]) ).
tcf(c_7168,plain,
! [X0: $i] :
( product(e_3,e_5,X0)
| ~ product(e_3,e_2,e_5)
| ~ product(e_5,e_2,X0) ),
inference(instantiation,[status(thm)],[c_2893]) ).
tcf(c_7169,plain,
( product(e_3,e_5,e_1)
| ~ product(e_5,e_2,e_1)
| ~ product(e_3,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_7168]) ).
tcf(c_7170,plain,
( product(e_3,e_5,e_2)
| ~ product(e_5,e_2,e_2)
| ~ product(e_3,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_5176]) ).
tcf(c_7177,plain,
( product(e_1,e_3,e_5)
| ~ product(e_3,e_2,e_5)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_1331]) ).
tcf(c_7215,plain,
( equalish(e_2,e_1)
| ~ product(e_4,e_2,e_5)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_2883]) ).
tcf(c_7217,plain,
! [X0: $i] :
( product(e_4,e_5,X0)
| ~ product(e_4,e_2,e_5)
| ~ product(e_5,e_2,X0) ),
inference(instantiation,[status(thm)],[c_2893]) ).
tcf(c_7218,plain,
( product(e_4,e_5,e_1)
| ~ product(e_5,e_2,e_1)
| ~ product(e_4,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_7217]) ).
tcf(c_7221,plain,
! [X0: $i] :
( product(X0,e_4,e_5)
| ~ product(e_4,e_2,e_5)
| ~ product(X0,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_2922]) ).
tcf(c_7222,plain,
( product(e_1,e_4,e_5)
| ~ product(e_4,e_2,e_5)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_7221]) ).
tcf(c_7235,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_2,e_3)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_3140]) ).
tcf(c_7312,plain,
( equalish(e_4,e_3)
| ~ product(e_3,e_4,e_3)
| ~ product(e_3,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_3050]) ).
tcf(c_7357,plain,
( product(e_3,e_4,e_5)
| ~ product(e_4,e_4,e_5)
| ~ product(e_3,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_1037]) ).
tcf(c_7365,plain,
( product(e_3,e_4,e_3)
| ~ product(e_4,e_4,e_3)
| ~ product(e_3,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_3066]) ).
tcf(c_7434,plain,
( equalish(e_5,e_4)
| ~ product(e_5,e_4,e_4)
| ~ product(e_4,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_7435,plain,
( equalish(e_4,e_5)
| ~ product(e_5,e_4,e_4)
| ~ product(e_4,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_7436,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_4,e_4)
| ~ product(e_3,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_289]) ).
tcf(c_7437,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_4,e_4)
| ~ product(e_2,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_281]) ).
tcf(c_7439,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_4,e_4)
| ~ product(e_3,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_257]) ).
tcf(c_7440,plain,
( equalish(e_2,e_4)
| ~ product(e_4,e_4,e_4)
| ~ product(e_2,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_7441,plain,
( equalish(e_1,e_4)
| ~ product(e_4,e_4,e_4)
| ~ product(e_1,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_193]) ).
tcf(c_7447,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_4,e_4)
| ~ product(e_4,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_1991]) ).
tcf(c_7448,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_4,e_4)
| ~ product(e_4,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_1990]) ).
tcf(c_7450,plain,
( equalish(e_5,e_4)
| ~ product(e_4,e_5,e_4)
| ~ product(e_4,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_1988]) ).
tcf(c_7464,plain,
( product(e_1,e_5,e_3)
| ~ product(e_5,e_5,e_3)
| ~ product(e_1,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_6118]) ).
tcf(c_7471,plain,
( equalish(e_4,e_5)
| ~ product(e_1,e_5,e_5)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_293]) ).
tcf(c_7473,plain,
( equalish(e_2,e_5)
| ~ product(e_1,e_5,e_5)
| ~ product(e_1,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_229]) ).
tcf(c_7477,plain,
( product(e_1,e_5,e_4)
| ~ product(e_5,e_5,e_4)
| ~ product(e_1,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_3177]) ).
tcf(c_7481,plain,
( equalish(e_5,e_1)
| ~ product(e_5,e_5,e_5)
| ~ product(e_1,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_2085]) ).
tcf(c_7485,plain,
( product(e_3,e_1,e_5)
| ~ product(e_3,e_5,e_1)
| ~ product(e_1,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_390]) ).
tcf(c_7521,plain,
! [X0: $i] :
( product(X0,e_1,e_1)
| ~ product(e_1,e_3,e_1)
| ~ product(X0,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_7522,plain,
( product(e_1,e_1,e_1)
| ~ product(e_1,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_7521]) ).
tcf(c_7525,plain,
( product(e_1,e_5,e_3)
| ~ product(e_5,e_4,e_3)
| ~ product(e_1,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_3066]) ).
tcf(c_7526,plain,
( equalish(e_5,e_4)
| ~ product(e_1,e_5,e_5)
| ~ product(e_1,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_7528,plain,
( equalish(e_4,e_3)
| ~ product(e_1,e_4,e_5)
| ~ product(e_1,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_287]) ).
tcf(c_7529,plain,
( equalish(e_4,e_2)
| ~ product(e_1,e_4,e_5)
| ~ product(e_1,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_279]) ).
tcf(c_7531,plain,
( equalish(e_3,e_4)
| ~ product(e_1,e_4,e_5)
| ~ product(e_1,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_255]) ).
tcf(c_7532,plain,
( equalish(e_2,e_4)
| ~ product(e_1,e_4,e_5)
| ~ product(e_1,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_223]) ).
tcf(c_7536,plain,
! [X0: $i] :
( product(e_1,e_5,X0)
| ~ product(e_1,e_4,e_5)
| ~ product(e_5,e_4,X0) ),
inference(instantiation,[status(thm)],[c_427]) ).
tcf(c_7541,plain,
( equalish(e_4,e_5)
| ~ product(e_1,e_4,e_5)
| ~ product(e_1,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_293]) ).
tcf(c_7545,plain,
( product(e_1,e_5,e_1)
| ~ product(e_5,e_4,e_1)
| ~ product(e_1,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_7536]) ).
tcf(c_7549,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_4,e_5)
| ~ product(e_1,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_1005]) ).
tcf(c_7550,plain,
( product(e_4,e_1,e_5)
| ~ product(e_4,e_4,e_1)
| ~ product(e_1,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_392]) ).
tcf(c_7650,plain,
( product(e_3,e_3,e_1)
| ~ product(e_3,e_5,e_3)
| ~ product(e_3,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_1602]) ).
tcf(c_7655,plain,
( product(e_5,e_3,e_1)
| ~ product(e_5,e_5,e_3)
| ~ product(e_3,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_1602]) ).
tcf(c_7696,plain,
( product(e_4,e_5,e_3)
| ~ product(e_5,e_5,e_3)
| ~ product(e_4,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_6108]) ).
tcf(c_7739,plain,
( equalish(e_2,e_1)
| ~ product(e_3,e_2,e_2)
| ~ product(e_3,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_681]) ).
tcf(c_7744,plain,
! [X0: $i] :
( product(X0,e_3,e_2)
| ~ product(e_3,e_2,e_2)
| ~ product(X0,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_4008]) ).
tcf(c_7745,plain,
( product(e_1,e_3,e_2)
| ~ product(e_3,e_2,e_2)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_7744]) ).
tcf(c_7771,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_2,e_5)
| ~ product(e_1,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_1005]) ).
tcf(c_7773,plain,
( product(e_3,e_1,e_5)
| ~ product(e_3,e_2,e_1)
| ~ product(e_1,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_390]) ).
tcf(c_7793,plain,
( equalish(e_2,e_5)
| ~ product(e_5,e_3,e_1)
| ~ product(e_2,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_233]) ).
tcf(c_7794,plain,
( equalish(e_2,e_1)
| ~ product(e_2,e_3,e_1)
| ~ product(e_1,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_209]) ).
tcf(c_7800,plain,
! [X0: $i] :
( product(X0,e_2,e_1)
| ~ product(e_2,e_3,e_1)
| ~ product(X0,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_394]) ).
tcf(c_7801,plain,
( product(e_1,e_2,e_1)
| ~ product(e_2,e_3,e_1)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_7800]) ).
tcf(c_7807,plain,
( product(e_2,e_2,e_2)
| ~ product(e_2,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_806]) ).
tcf(c_7814,plain,
( equalish(e_1,e_2)
| ~ product(e_2,e_4,e_2)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_177]) ).
tcf(c_7835,plain,
( equalish(e_2,e_5)
| ~ product(e_5,e_1,e_5)
| ~ product(e_2,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_233]) ).
tcf(c_7840,plain,
! [X0: $i] :
( product(e_2,e_5,X0)
| ~ product(e_2,e_1,e_5)
| ~ product(e_5,e_1,X0) ),
inference(instantiation,[status(thm)],[c_427]) ).
tcf(c_7841,plain,
( equalish(e_5,e_4)
| ~ product(e_2,e_1,e_5)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_325]) ).
tcf(c_7849,plain,
( product(e_2,e_5,e_1)
| ~ product(e_5,e_1,e_1)
| ~ product(e_2,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_7840]) ).
tcf(c_7898,plain,
( product(e_2,e_3,e_4)
| ~ product(e_3,e_3,e_4)
| ~ product(e_2,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_1251]) ).
tcf(c_7952,plain,
( product(e_3,e_3,e_3)
| ~ product(e_3,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_5181]) ).
tcf(c_7966,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_4,e_5)
| ~ product(e_4,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_287]) ).
tcf(c_7995,plain,
! [X0: $i] :
( product(X0,e_4,e_5)
| ~ product(e_4,e_4,e_5)
| ~ product(X0,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_1037]) ).
tcf(c_7996,plain,
( product(e_1,e_4,e_5)
| ~ product(e_4,e_4,e_5)
| ~ product(e_1,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_7995]) ).
tcf(c_8004,plain,
( equalish(e_5,e_4)
| ~ product(e_5,e_1,e_4)
| ~ product(e_4,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_8009,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_1,e_4)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_257]) ).
tcf(c_8010,plain,
( equalish(e_2,e_4)
| ~ product(e_4,e_1,e_4)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_8017,plain,
( product(e_1,e_3,e_4)
| ~ product(e_3,e_5,e_4)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_951]) ).
tcf(c_8021,plain,
( equalish(e_2,e_3)
| ~ product(e_1,e_5,e_3)
| ~ product(e_1,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_213]) ).
tcf(c_8026,plain,
( equalish(e_5,e_1)
| ~ product(e_1,e_5,e_3)
| ~ product(e_1,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_303]) ).
tcf(c_8031,plain,
( equalish(e_2,e_1)
| ~ product(e_2,e_5,e_3)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_8032,plain,
( product(e_2,e_1,e_3)
| ~ product(e_2,e_5,e_1)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_382]) ).
tcf(c_8081,plain,
( product(e_4,e_4,e_4)
| ~ product(e_4,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_3834]) ).
tcf(c_8092,plain,
( product(e_5,e_2,e_2)
| ~ product(e_5,e_1,e_2)
| ~ product(e_2,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_806]) ).
tcf(c_8095,plain,
( equalish(e_3,e_5)
| ~ product(e_5,e_1,e_2)
| ~ product(e_3,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_265]) ).
tcf(c_8101,plain,
! [X0: $i] :
( product(e_5,e_2,X0)
| ~ product(e_5,e_1,e_2)
| ~ product(e_2,e_1,X0) ),
inference(instantiation,[status(thm)],[c_432]) ).
tcf(c_8102,plain,
( product(e_5,e_2,e_1)
| ~ product(e_5,e_1,e_2)
| ~ product(e_2,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_8101]) ).
tcf(c_8106,plain,
( product(e_4,e_5,e_2)
| ~ product(e_5,e_4,e_2)
| ~ product(e_4,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_993]) ).
tcf(c_8113,plain,
( equalish(e_1,e_2)
| ~ product(e_5,e_2,e_4)
| ~ product(e_5,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_175]) ).
tcf(c_8126,plain,
( equalish(e_5,e_1)
| ~ product(e_5,e_2,e_4)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_4574]) ).
tcf(c_8132,plain,
! [X0: $i] :
( product(e_5,e_4,X0)
| ~ product(e_5,e_2,e_4)
| ~ product(e_4,e_2,X0) ),
inference(instantiation,[status(thm)],[c_4563]) ).
tcf(c_8133,plain,
( product(e_5,e_4,e_5)
| ~ product(e_5,e_2,e_4)
| ~ product(e_4,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_994]) ).
tcf(c_8134,plain,
( product(e_5,e_4,e_1)
| ~ product(e_5,e_2,e_4)
| ~ product(e_4,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_8132]) ).
tcf(c_8136,plain,
! [X0: $i] :
( product(X0,e_5,e_4)
| ~ product(e_5,e_2,e_4)
| ~ product(X0,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_2893]) ).
tcf(c_8137,plain,
( product(e_1,e_5,e_4)
| ~ product(e_5,e_2,e_4)
| ~ product(e_1,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_8136]) ).
tcf(c_8170,plain,
( product(e_5,e_5,e_5)
| ~ product(e_5,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_2367]) ).
tcf(c_8180,plain,
( product(e_5,e_1,e_4)
| ~ product(e_5,e_4,e_1)
| ~ product(e_1,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_560]) ).
tcf(c_8194,plain,
( equalish(e_5,e_1)
| ~ product(e_5,e_4,e_1)
| ~ product(e_1,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_8231,plain,
( equalish(e_3,e_2)
| ~ product(e_2,e_3,e_1)
| ~ product(e_2,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_8323,plain,
( equalish(e_4,e_3)
| ~ cycle(e_2,e_4)
| ~ greater(e_4,e_0)
| ~ next(e_2,e_3)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_561]) ).
tcf(c_8377,plain,
( equalish(e_4,e_2)
| ~ product(e_2,e_4,e_2)
| ~ product(e_2,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_964]) ).
tcf(c_8575,plain,
( equalish(e_5,e_4)
| ~ product(e_3,e_5,e_3)
| ~ product(e_3,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_3048]) ).
tcf(c_8847,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_8575,c_8377,c_8323,c_8231,c_8194,c_8180,c_8170,c_8137,c_8126,c_8134,c_8133,c_8113,c_8106,c_8102,c_8095,c_8092,c_8081,c_8031,c_8032,c_8026,c_8017,c_8021,c_8004,c_8009,c_8010,c_7996,c_7966,c_7952,c_7898,c_7849,c_7841,c_7835,c_7814,c_7807,c_7801,c_7793,c_7794,c_7771,c_7773,c_7745,c_7739,c_7696,c_7655,c_7650,c_7549,c_7550,c_7545,c_7541,c_7525,c_7526,c_7528,c_7529,c_7531,c_7532,c_7522,c_7481,c_7485,c_7477,c_7464,c_7471,c_7473,c_7447,c_7448,c_7450,c_7434,c_7435,c_7436,c_7437,c_7439,c_7440,c_7441,c_7365,c_7357,c_7312,c_7235,c_7222,c_7215,c_7218,c_7177,c_7170,c_7169,c_7143,c_7123,c_7008,c_6869,c_6794,c_6785,c_6782,c_6648,c_6650,c_6646,c_6632,c_6634,c_6635,c_6636,c_6310,c_6280,c_5981,c_5967,c_5865,c_5851,c_5805,c_5800,c_5788,c_5785,c_5778,c_5771,c_5756,c_5757,c_5750,c_5744,c_5726,c_5728,c_5719,c_5717,c_5716,c_5704,c_5714,c_5712,c_5713,c_5695,c_5699,c_5700,c_5692,c_5656,c_5626,c_5616,c_5608,c_5602,c_5601,c_5598,c_5596,c_5588,c_5577,c_5578,c_5580,c_5581,c_5582,c_5571,c_5572,c_5575,c_5576,c_5568,c_5561,c_5527,c_5508,c_5513,c_5515,c_5487,c_5480,c_5470,c_5391,c_5398,c_5371,c_5373,c_5374,c_5370,c_5230,c_5227,c_5058,c_5054,c_5049,c_5048,c_4994,c_4993,c_4987,c_4976,c_4910,c_4866,c_4802,c_4518,c_4514,c_4505,c_4501,c_4482,c_4459,c_4456,c_4435,c_4401,c_4399,c_4386,c_4291,c_4297,c_4268,c_4272,c_4265,c_4263,c_4253,c_4245,c_4244,c_4191,c_4160,c_4140,c_4138,c_4110,c_4104,c_4092,c_3987,c_3885,c_3837,c_3675,c_3564,c_3562,c_3391,c_3360,c_3023,c_3022,c_2999,c_2997,c_2952,c_2949,c_2942,c_2943,c_2910,c_2909,c_2880,c_2879,c_2799,c_2795,c_2796,c_2791,c_2764,c_2755,c_2734,c_2726,c_2716,c_2718,c_2719,c_2720,c_2722,c_2698,c_2699,c_2700,c_2694,c_2688,c_2689,c_2690,c_2673,c_2680,c_2658,c_2651,c_2652,c_2654,c_2649,c_2612,c_2615,c_2605,c_2606,c_2607,c_2608,c_2609,c_2610,c_2597,c_2550,c_2545,c_2537,c_2530,c_2527,c_2522,c_2497,c_2492,c_2475,c_2478,c_2458,c_2443,c_2440,c_2307,c_2260,c_2239,c_2230,c_2233,c_2229,c_2208,c_2209,c_2148,c_2134,c_2065,c_2008,c_2009,c_2010,c_2003,c_2001,c_2000,c_1999,c_1987,c_1985,c_1984,c_1958,c_1959,c_1952,c_1950,c_1948,c_1889,c_1882,c_1860,c_1836,c_1826,c_1820,c_1808,c_1796,c_1788,c_1765,c_1750,c_1726,c_1724,c_1715,c_1717,c_1714,c_1711,c_1680,c_1676,c_1669,c_1665,c_1637,c_1634,c_1603,c_1591,c_1567,c_1549,c_1528,c_1529,c_1530,c_1531,c_1532,c_1533,c_1534,c_1535,c_1520,c_1521,c_1523,c_1435,c_1438,c_1417,c_1411,c_1381,c_1371,c_1372,c_1367,c_1368,c_1369,c_1330,c_1336,c_1326,c_1327,c_1328,c_1305,c_1307,c_1301,c_1287,c_1276,c_1266,c_1265,c_1212,c_1155,c_1154,c_1139,c_1140,c_1142,c_1144,c_1119,c_1118,c_1117,c_1104,c_1105,c_1101,c_1097,c_1094,c_1092,c_1089,c_1063,c_1067,c_1060,c_1054,c_1056,c_1057,c_1053,c_1049,c_1051,c_1048,c_1044,c_1034,c_1015,c_1013,c_995,c_992,c_978,c_983,c_985,c_977,c_976,c_974,c_971,c_940,c_939,c_924,c_923,c_910,c_893,c_891,c_884,c_883,c_854,c_763,c_754,c_755,c_752,c_747,c_705,c_693,c_688,c_686,c_687,c_685,c_603,c_593,c_592,c_562,c_557,c_550,c_542,c_435,c_431,c_426,c_416,c_407,c_402,c_398,c_347,c_345,c_304,c_288,c_272,c_240,c_208,c_194,c_168,c_138,c_139,c_140,c_141,c_142,c_143,c_144,c_145,c_146,c_147,c_148,c_149,c_150,c_151,c_152,c_153,c_154,c_155,c_156,c_157,c_106,c_108,c_109,c_110,c_111,c_112,c_113,c_114,c_121,c_123,c_128,c_133,c_134,c_135,c_136,c_137]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP128-3.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n015.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Wed Sep 23 13:47:25 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.41 Running EPR theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s epr_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 3.82/1.14 % SZS status Started for theBenchmark.p
% 3.82/1.14 % SZS status Unsatisfiable for theBenchmark.p
% 3.82/1.14
% 3.82/1.14 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.82/1.14
% 3.82/1.14 % ------ iProver source info
% 3.82/1.14
% 3.82/1.14 % git: date: 2026-07-19 20:42:38 +0200
% 3.82/1.14 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.82/1.14 % git: non_committed_changes: false
% 3.82/1.14
% 3.82/1.14 % ------ Parsing...% successful
% 3.82/1.14
% 3.82/1.14
% 3.82/1.14 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 3.82/1.14 % ------ Proving...
% 3.82/1.14 % ------ Problem Properties
% 3.82/1.14
% 3.82/1.14 %
% 3.82/1.14 % clauses 57
% 3.82/1.14 % conjectures 1
% 3.82/1.14 % EPR 57
% 3.82/1.14 % Horn 55
% 3.82/1.14 % unary 46
% 3.82/1.14 % binary 0
% 3.82/1.14 % lits 94
% 3.82/1.14 % lits eq 0
% 3.82/1.14 % fd_pure 0
% 3.82/1.14 % fd_pseudo 0
% 3.82/1.14 % fd_cond 0
% 3.82/1.14 % fd_pseudo_cond 0
% 3.82/1.14 % AC symbols 0
% 3.82/1.14
% 3.82/1.14 % ------ Input Options Time Limit: Unbounded
% 3.82/1.14
% 3.82/1.14
% 3.82/1.14 % ------
% 3.82/1.14 % Current options:
% 3.82/1.14 % ------
% 3.82/1.14
% 3.82/1.14
% 3.82/1.14 %
% 3.82/1.14
% 3.82/1.14 % ------ Proving...
% 3.82/1.14 %
% 3.82/1.14
% 3.82/1.14 % SZS status Unsatisfiable for theBenchmark.p
% 3.82/1.14
% 3.82/1.14 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.82/1.16
% 3.82/1.16
%------------------------------------------------------------------------------