%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP128-2.006 : 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 7.42s 6.73s
% Output : CNFRefutation 7.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 56
% Syntax : Number of formulae : 806 ( 101 unt; 0 def)
% Number of atoms : 2401 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 3072 (1477 ~;1595 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 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 : 6 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 561 ( 0 sgn 561 !; 0 ?; 540 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
next(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_then_e_2) ).
fof(f2,axiom,
next(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_then_e_3) ).
fof(f3,axiom,
next(e_3,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_then_e_4) ).
fof(f4,axiom,
next(e_4,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_then_e_5) ).
fof(f11,axiom,
greater(e_3,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_greater_e_2) ).
fof(f12,axiom,
greater(e_4,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_greater_e_2) ).
fof(f13,axiom,
greater(e_5,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_greater_e_2) ).
fof(f14,axiom,
greater(e_6,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_6_greater_e_2) ).
fof(f15,axiom,
greater(e_4,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_greater_e_3) ).
fof(f16,axiom,
greater(e_5,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_greater_e_3) ).
fof(f17,axiom,
greater(e_6,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_6_greater_e_3) ).
fof(f18,axiom,
greater(e_5,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_greater_e_4) ).
fof(f19,axiom,
greater(e_6,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_6_greater_e_4) ).
fof(f20,axiom,
greater(e_6,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_6_greater_e_5) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ greater(X1,X2)
| ~ next(X0,X2)
| ~ product(X0,e_1,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',no_redundancy) ).
fof(f22,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
fof(f23,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
fof(f24,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
fof(f25,axiom,
group_element(e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_4) ).
fof(f26,axiom,
group_element(e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_5) ).
fof(f27,axiom,
group_element(e_6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_6) ).
fof(f28,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f29,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f30,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
fof(f31,axiom,
~ equalish(e_1,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_5) ).
fof(f32,axiom,
~ equalish(e_1,e_6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_6) ).
fof(f33,axiom,
~ equalish(e_2,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_1) ).
fof(f34,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f35,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
fof(f36,axiom,
~ equalish(e_2,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_5) ).
fof(f37,axiom,
~ equalish(e_2,e_6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_6) ).
fof(f38,axiom,
~ equalish(e_3,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_1) ).
fof(f39,axiom,
~ equalish(e_3,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_2) ).
fof(f40,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
fof(f41,axiom,
~ equalish(e_3,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_5) ).
fof(f42,axiom,
~ equalish(e_3,e_6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_6) ).
fof(f43,axiom,
~ equalish(e_4,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_1) ).
fof(f44,axiom,
~ equalish(e_4,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_2) ).
fof(f45,axiom,
~ equalish(e_4,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_3) ).
fof(f46,axiom,
~ equalish(e_4,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_5) ).
fof(f47,axiom,
~ equalish(e_4,e_6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_6) ).
fof(f48,axiom,
~ equalish(e_5,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_is_not_e_1) ).
fof(f49,axiom,
~ equalish(e_5,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_is_not_e_2) ).
fof(f50,axiom,
~ equalish(e_5,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_is_not_e_3) ).
fof(f51,axiom,
~ equalish(e_5,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_is_not_e_4) ).
fof(f52,axiom,
~ equalish(e_5,e_6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_is_not_e_6) ).
fof(f53,axiom,
~ equalish(e_6,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_6_is_not_e_1) ).
fof(f54,axiom,
~ equalish(e_6,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_6_is_not_e_2) ).
fof(f55,axiom,
~ equalish(e_6,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_6_is_not_e_3) ).
fof(f56,axiom,
~ equalish(e_6,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_6_is_not_e_4) ).
fof(f57,axiom,
~ equalish(e_6,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_6_is_not_e_5) ).
fof(f58,axiom,
! [X0,X1] :
( product(X0,X1,e_6)
| 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(f59,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(f60,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(f61,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(f62,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_111,plain,
next(e_1,e_2),
inference(cnf_transformation,[],[f1]) ).
tcf(c_112,plain,
next(e_2,e_3),
inference(cnf_transformation,[],[f2]) ).
tcf(c_113,plain,
next(e_3,e_4),
inference(cnf_transformation,[],[f3]) ).
tcf(c_114,plain,
next(e_4,e_5),
inference(cnf_transformation,[],[f4]) ).
tcf(c_121,plain,
greater(e_3,e_2),
inference(cnf_transformation,[],[f11]) ).
tcf(c_122,plain,
greater(e_4,e_2),
inference(cnf_transformation,[],[f12]) ).
tcf(c_123,plain,
greater(e_5,e_2),
inference(cnf_transformation,[],[f13]) ).
tcf(c_124,plain,
greater(e_6,e_2),
inference(cnf_transformation,[],[f14]) ).
tcf(c_125,plain,
greater(e_4,e_3),
inference(cnf_transformation,[],[f15]) ).
tcf(c_126,plain,
greater(e_5,e_3),
inference(cnf_transformation,[],[f16]) ).
tcf(c_127,plain,
greater(e_6,e_3),
inference(cnf_transformation,[],[f17]) ).
tcf(c_128,plain,
greater(e_5,e_4),
inference(cnf_transformation,[],[f18]) ).
tcf(c_129,plain,
greater(e_6,e_4),
inference(cnf_transformation,[],[f19]) ).
tcf(c_130,plain,
greater(e_6,e_5),
inference(cnf_transformation,[],[f20]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ greater(X1,X2)
| ~ next(X0,X2)
| ~ product(X0,e_1,X1) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_132,plain,
group_element(e_1),
inference(cnf_transformation,[],[f22]) ).
tcf(c_133,plain,
group_element(e_2),
inference(cnf_transformation,[],[f23]) ).
tcf(c_134,plain,
group_element(e_3),
inference(cnf_transformation,[],[f24]) ).
tcf(c_135,plain,
group_element(e_4),
inference(cnf_transformation,[],[f25]) ).
tcf(c_136,plain,
group_element(e_5),
inference(cnf_transformation,[],[f26]) ).
tcf(c_137,plain,
group_element(e_6),
inference(cnf_transformation,[],[f27]) ).
tcf(c_138,plain,
~ equalish(e_1,e_2),
inference(cnf_transformation,[],[f28]) ).
tcf(c_139,plain,
~ equalish(e_1,e_3),
inference(cnf_transformation,[],[f29]) ).
tcf(c_140,plain,
~ equalish(e_1,e_4),
inference(cnf_transformation,[],[f30]) ).
tcf(c_141,plain,
~ equalish(e_1,e_5),
inference(cnf_transformation,[],[f31]) ).
tcf(c_142,plain,
~ equalish(e_1,e_6),
inference(cnf_transformation,[],[f32]) ).
tcf(c_143,plain,
~ equalish(e_2,e_1),
inference(cnf_transformation,[],[f33]) ).
tcf(c_144,plain,
~ equalish(e_2,e_3),
inference(cnf_transformation,[],[f34]) ).
tcf(c_145,plain,
~ equalish(e_2,e_4),
inference(cnf_transformation,[],[f35]) ).
tcf(c_146,plain,
~ equalish(e_2,e_5),
inference(cnf_transformation,[],[f36]) ).
tcf(c_147,plain,
~ equalish(e_2,e_6),
inference(cnf_transformation,[],[f37]) ).
tcf(c_148,plain,
~ equalish(e_3,e_1),
inference(cnf_transformation,[],[f38]) ).
tcf(c_149,plain,
~ equalish(e_3,e_2),
inference(cnf_transformation,[],[f39]) ).
tcf(c_150,plain,
~ equalish(e_3,e_4),
inference(cnf_transformation,[],[f40]) ).
tcf(c_151,plain,
~ equalish(e_3,e_5),
inference(cnf_transformation,[],[f41]) ).
tcf(c_152,plain,
~ equalish(e_3,e_6),
inference(cnf_transformation,[],[f42]) ).
tcf(c_153,plain,
~ equalish(e_4,e_1),
inference(cnf_transformation,[],[f43]) ).
tcf(c_154,plain,
~ equalish(e_4,e_2),
inference(cnf_transformation,[],[f44]) ).
tcf(c_155,plain,
~ equalish(e_4,e_3),
inference(cnf_transformation,[],[f45]) ).
tcf(c_156,plain,
~ equalish(e_4,e_5),
inference(cnf_transformation,[],[f46]) ).
tcf(c_157,plain,
~ equalish(e_4,e_6),
inference(cnf_transformation,[],[f47]) ).
tcf(c_158,plain,
~ equalish(e_5,e_1),
inference(cnf_transformation,[],[f48]) ).
tcf(c_159,plain,
~ equalish(e_5,e_2),
inference(cnf_transformation,[],[f49]) ).
tcf(c_160,plain,
~ equalish(e_5,e_3),
inference(cnf_transformation,[],[f50]) ).
tcf(c_161,plain,
~ equalish(e_5,e_4),
inference(cnf_transformation,[],[f51]) ).
tcf(c_162,plain,
~ equalish(e_5,e_6),
inference(cnf_transformation,[],[f52]) ).
tcf(c_163,plain,
~ equalish(e_6,e_1),
inference(cnf_transformation,[],[f53]) ).
tcf(c_164,plain,
~ equalish(e_6,e_2),
inference(cnf_transformation,[],[f54]) ).
tcf(c_165,plain,
~ equalish(e_6,e_3),
inference(cnf_transformation,[],[f55]) ).
tcf(c_166,plain,
~ equalish(e_6,e_4),
inference(cnf_transformation,[],[f56]) ).
tcf(c_167,plain,
~ equalish(e_6,e_5),
inference(cnf_transformation,[],[f57]) ).
tcf(c_168,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,e_6)
| 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,[],[f58]) ).
tcf(c_169,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equalish(X2,X3)
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_170,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equalish(X1,X3)
| ~ product(X0,X3,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_171,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equalish(X0,X3)
| ~ product(X3,X1,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_172,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,[],[f62]) ).
tcf(c_175,plain,
( product(e_1,e_1,e_6)
| 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_168]) ).
tcf(c_186,plain,
! [X0: $i] :
( ~ greater(e_3,e_2)
| ~ next(X0,e_2)
| ~ product(X0,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_187,plain,
( ~ greater(e_3,e_2)
| ~ next(e_1,e_2)
| ~ product(e_1,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_186]) ).
tcf(c_188,plain,
! [X0: $i] :
( ~ greater(e_4,e_2)
| ~ next(X0,e_2)
| ~ product(X0,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_189,plain,
( ~ greater(e_4,e_2)
| ~ next(e_1,e_2)
| ~ product(e_1,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_188]) ).
tcf(c_190,plain,
! [X0: $i] :
( ~ greater(e_5,e_2)
| ~ next(X0,e_2)
| ~ product(X0,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_191,plain,
( ~ greater(e_5,e_2)
| ~ next(e_1,e_2)
| ~ product(e_1,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_190]) ).
tcf(c_192,plain,
! [X0: $i] :
( ~ greater(e_6,e_2)
| ~ next(X0,e_2)
| ~ product(X0,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_193,plain,
( ~ greater(e_6,e_2)
| ~ next(e_1,e_2)
| ~ product(e_1,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_192]) ).
tcf(c_194,plain,
! [X0: $i] :
( ~ greater(e_4,e_3)
| ~ next(X0,e_3)
| ~ product(X0,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_196,plain,
! [X0: $i] :
( ~ greater(e_5,e_3)
| ~ next(X0,e_3)
| ~ product(X0,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_198,plain,
! [X0: $i] :
( ~ greater(e_6,e_3)
| ~ next(X0,e_3)
| ~ product(X0,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_200,plain,
! [X0: $i] :
( ~ greater(e_5,e_4)
| ~ next(X0,e_4)
| ~ product(X0,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_202,plain,
! [X0: $i] :
( ~ greater(e_6,e_4)
| ~ next(X0,e_4)
| ~ product(X0,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_204,plain,
! [X0: $i] :
( ~ greater(e_6,e_5)
| ~ next(X0,e_5)
| ~ product(X0,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_208,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_170]) ).
tcf(c_209,plain,
( equalish(e_1,e_2)
| ~ product(e_1,e_2,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_208]) ).
tcf(c_210,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_171]) ).
tcf(c_211,plain,
( equalish(e_1,e_2)
| ~ product(e_2,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_210]) ).
tcf(c_214,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_3)
| ~ product(X0,e_3,X1)
| ~ product(X0,e_1,X1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_215,plain,
( equalish(e_1,e_3)
| ~ product(e_1,e_3,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_214]) ).
tcf(c_216,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_171]) ).
tcf(c_220,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_4)
| ~ product(X0,e_4,X1)
| ~ product(X0,e_1,X1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_221,plain,
( equalish(e_1,e_4)
| ~ product(e_1,e_4,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_220]) ).
tcf(c_222,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_171]) ).
tcf(c_223,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_222]) ).
tcf(c_226,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_170]) ).
tcf(c_227,plain,
( equalish(e_1,e_5)
| ~ product(e_1,e_5,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_226]) ).
tcf(c_228,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_171]) ).
tcf(c_229,plain,
( equalish(e_1,e_5)
| ~ product(e_5,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_228]) ).
tcf(c_232,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_6)
| ~ product(X0,e_6,X1)
| ~ product(X0,e_1,X1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_233,plain,
( equalish(e_1,e_6)
| ~ product(e_1,e_6,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_234,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_6)
| ~ product(e_6,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_235,plain,
( equalish(e_1,e_6)
| ~ product(e_6,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_234]) ).
tcf(c_238,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_170]) ).
tcf(c_240,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_171]) ).
tcf(c_241,plain,
( equalish(e_2,e_1)
| ~ product(e_2,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_240]) ).
tcf(c_242,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_169]) ).
tcf(c_250,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_170]) ).
tcf(c_251,plain,
( equalish(e_2,e_4)
| ~ product(e_1,e_4,e_1)
| ~ product(e_1,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_250]) ).
tcf(c_252,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_171]) ).
tcf(c_253,plain,
( equalish(e_2,e_4)
| ~ product(e_4,e_1,e_1)
| ~ product(e_2,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_252]) ).
tcf(c_254,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_169]) ).
tcf(c_258,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_171]) ).
tcf(c_259,plain,
( equalish(e_2,e_5)
| ~ product(e_5,e_1,e_1)
| ~ product(e_2,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_258]) ).
tcf(c_262,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_6)
| ~ product(X0,e_6,X1)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_263,plain,
( equalish(e_2,e_6)
| ~ product(e_1,e_6,e_1)
| ~ product(e_1,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_262]) ).
tcf(c_264,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_6)
| ~ product(e_6,X0,X1)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_265,plain,
( equalish(e_2,e_6)
| ~ product(e_6,e_1,e_1)
| ~ product(e_2,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_264]) ).
tcf(c_268,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_170]) ).
tcf(c_270,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_171]) ).
tcf(c_271,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_270]) ).
tcf(c_274,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_170]) ).
tcf(c_276,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_171]) ).
tcf(c_278,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_169]) ).
tcf(c_280,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_170]) ).
tcf(c_282,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_171]) ).
tcf(c_286,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_5)
| ~ product(X0,e_5,X1)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_288,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_171]) ).
tcf(c_292,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_6)
| ~ product(X0,e_6,X1)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_294,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_6)
| ~ product(e_6,X0,X1)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_296,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_169]) ).
tcf(c_298,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_170]) ).
tcf(c_300,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_171]) ).
tcf(c_302,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_169]) ).
tcf(c_304,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_170]) ).
tcf(c_306,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_171]) ).
tcf(c_308,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_169]) ).
tcf(c_312,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_171]) ).
tcf(c_316,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_170]) ).
tcf(c_318,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_171]) ).
tcf(c_319,plain,
( equalish(e_4,e_5)
| ~ product(e_5,e_1,e_1)
| ~ product(e_4,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_318]) ).
tcf(c_324,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_6)
| ~ product(e_6,X0,X1)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_328,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_170]) ).
tcf(c_329,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_328]) ).
tcf(c_330,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_171]) ).
tcf(c_332,plain,
! [X0: $i,X1: $i] :
( equalish(e_5,e_2)
| ~ product(X0,X1,e_5)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_169]) ).
tcf(c_334,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_170]) ).
tcf(c_335,plain,
( equalish(e_5,e_2)
| ~ product(e_1,e_5,e_1)
| ~ product(e_1,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_334]) ).
tcf(c_336,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_171]) ).
tcf(c_338,plain,
! [X0: $i,X1: $i] :
( equalish(e_5,e_3)
| ~ product(X0,X1,e_5)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_169]) ).
tcf(c_340,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_170]) ).
tcf(c_342,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_171]) ).
tcf(c_344,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_169]) ).
tcf(c_346,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_170]) ).
tcf(c_348,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_171]) ).
tcf(c_350,plain,
! [X0: $i,X1: $i] :
( equalish(e_5,e_6)
| ~ product(X0,X1,e_6)
| ~ product(X0,X1,e_5) ),
inference(instantiation,[status(thm)],[c_169]) ).
tcf(c_352,plain,
! [X0: $i,X1: $i] :
( equalish(e_5,e_6)
| ~ product(X0,e_6,X1)
| ~ product(X0,e_5,X1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_358,plain,
! [X0: $i,X1: $i] :
( equalish(e_6,e_1)
| ~ product(X0,e_6,X1)
| ~ product(X0,e_1,X1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_360,plain,
! [X0: $i,X1: $i] :
( equalish(e_6,e_1)
| ~ product(e_6,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_364,plain,
! [X0: $i,X1: $i] :
( equalish(e_6,e_2)
| ~ product(X0,e_6,X1)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_370,plain,
! [X0: $i,X1: $i] :
( equalish(e_6,e_3)
| ~ product(X0,e_6,X1)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_372,plain,
! [X0: $i,X1: $i] :
( equalish(e_6,e_3)
| ~ product(e_6,X0,X1)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_376,plain,
! [X0: $i,X1: $i] :
( equalish(e_6,e_4)
| ~ product(X0,e_6,X1)
| ~ product(X0,e_4,X1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_378,plain,
! [X0: $i,X1: $i] :
( equalish(e_6,e_4)
| ~ product(e_6,X0,X1)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_380,plain,
! [X0: $i,X1: $i] :
( equalish(e_6,e_5)
| ~ product(X0,X1,e_6)
| ~ product(X0,X1,e_5) ),
inference(instantiation,[status(thm)],[c_169]) ).
tcf(c_382,plain,
! [X0: $i,X1: $i] :
( equalish(e_6,e_5)
| ~ product(X0,e_6,X1)
| ~ product(X0,e_5,X1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_384,plain,
! [X0: $i,X1: $i] :
( equalish(e_6,e_5)
| ~ product(e_6,X0,X1)
| ~ product(e_5,X0,X1) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_386,plain,
! [X0: $i,X1: $i] :
( product(X0,e_1,e_3)
| ~ product(e_1,X1,e_3)
| ~ product(X0,X1,e_1) ),
inference(instantiation,[status(thm)],[c_172]) ).
tcf(c_390,plain,
( ~ greater(e_4,e_3)
| ~ next(e_2,e_3)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_194]) ).
tcf(c_391,plain,
( ~ greater(e_5,e_3)
| ~ next(e_2,e_3)
| ~ product(e_2,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_196]) ).
tcf(c_392,plain,
( ~ greater(e_6,e_3)
| ~ next(e_2,e_3)
| ~ product(e_2,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_198]) ).
tcf(c_393,plain,
( ~ greater(e_5,e_4)
| ~ next(e_3,e_4)
| ~ product(e_3,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_200]) ).
tcf(c_394,plain,
( ~ greater(e_6,e_4)
| ~ next(e_3,e_4)
| ~ product(e_3,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_202]) ).
tcf(c_395,plain,
( ~ greater(e_6,e_5)
| ~ next(e_4,e_5)
| ~ product(e_4,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_204]) ).
tcf(c_396,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_172]) ).
tcf(c_397,plain,
( product(e_1,e_2,e_1)
| ~ product(e_2,e_1,e_1)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_396]) ).
tcf(c_399,plain,
! [X0: $i] :
( product(X0,e_2,e_6)
| 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_168]) ).
tcf(c_400,plain,
( product(e_1,e_2,e_6)
| product(e_1,e_2,e_5)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_1)
| ~ group_element(e_2)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_401,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_172]) ).
tcf(c_403,plain,
! [X0: $i] :
( product(e_2,X0,e_6)
| 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_168]) ).
tcf(c_404,plain,
( product(e_2,e_1,e_6)
| product(e_2,e_1,e_5)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| ~ group_element(e_2)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_403]) ).
tcf(c_405,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_172]) ).
tcf(c_406,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_172]) ).
tcf(c_407,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_172]) ).
tcf(c_410,plain,
! [X0: $i] :
( product(X0,e_3,e_6)
| 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_168]) ).
tcf(c_411,plain,
( product(e_1,e_3,e_6)
| product(e_1,e_3,e_5)
| product(e_1,e_3,e_4)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| ~ group_element(e_3)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_410]) ).
tcf(c_412,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_172]) ).
tcf(c_414,plain,
! [X0: $i] :
( product(e_3,X0,e_6)
| 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_168]) ).
tcf(c_415,plain,
( product(e_3,e_1,e_6)
| product(e_3,e_1,e_5)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_1)
| ~ group_element(e_3)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_414]) ).
tcf(c_416,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_172]) ).
tcf(c_419,plain,
! [X0: $i] :
( product(X0,e_4,e_6)
| 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_168]) ).
tcf(c_420,plain,
( product(e_1,e_4,e_6)
| 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_419]) ).
tcf(c_421,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_4,X0,X2)
| ~ product(e_4,X1,X0)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_172]) ).
tcf(c_423,plain,
! [X0: $i] :
( product(e_4,X0,e_6)
| 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_168]) ).
tcf(c_424,plain,
( product(e_4,e_1,e_6)
| product(e_4,e_1,e_5)
| product(e_4,e_1,e_4)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| ~ group_element(e_4)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_423]) ).
tcf(c_425,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_172]) ).
tcf(c_428,plain,
! [X0: $i] :
( product(X0,e_5,e_6)
| 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_168]) ).
tcf(c_429,plain,
( product(e_1,e_5,e_6)
| product(e_1,e_5,e_5)
| product(e_1,e_5,e_4)
| product(e_1,e_5,e_3)
| product(e_1,e_5,e_2)
| product(e_1,e_5,e_1)
| ~ group_element(e_5)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_428]) ).
tcf(c_430,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_172]) ).
tcf(c_432,plain,
! [X0: $i] :
( product(e_5,X0,e_6)
| 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_168]) ).
tcf(c_433,plain,
( product(e_5,e_1,e_6)
| product(e_5,e_1,e_5)
| product(e_5,e_1,e_4)
| product(e_5,e_1,e_3)
| product(e_5,e_1,e_2)
| product(e_5,e_1,e_1)
| ~ group_element(e_5)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_432]) ).
tcf(c_434,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X0,e_6,X2)
| ~ product(e_6,X1,X2)
| ~ product(X0,X1,e_6) ),
inference(instantiation,[status(thm)],[c_172]) ).
tcf(c_437,plain,
! [X0: $i] :
( product(X0,e_6,e_6)
| product(X0,e_6,e_5)
| product(X0,e_6,e_4)
| product(X0,e_6,e_3)
| product(X0,e_6,e_2)
| product(X0,e_6,e_1)
| ~ group_element(e_6)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_168]) ).
tcf(c_438,plain,
( product(e_1,e_6,e_6)
| product(e_1,e_6,e_5)
| product(e_1,e_6,e_4)
| product(e_1,e_6,e_3)
| product(e_1,e_6,e_2)
| product(e_1,e_6,e_1)
| ~ group_element(e_6)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_437]) ).
tcf(c_439,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_6,X0,X2)
| ~ product(e_6,X1,X0)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_172]) ).
tcf(c_441,plain,
! [X0: $i] :
( product(e_6,X0,e_6)
| product(e_6,X0,e_5)
| product(e_6,X0,e_4)
| product(e_6,X0,e_3)
| product(e_6,X0,e_2)
| product(e_6,X0,e_1)
| ~ group_element(e_6)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_168]) ).
tcf(c_442,plain,
( product(e_6,e_1,e_6)
| product(e_6,e_1,e_5)
| product(e_6,e_1,e_4)
| product(e_6,e_1,e_3)
| product(e_6,e_1,e_2)
| product(e_6,e_1,e_1)
| ~ group_element(e_6)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_441]) ).
tcf(c_494,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_172]) ).
tcf(c_495,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_172]) ).
tcf(c_571,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X0,X2,e_6)
| ~ product(X2,X1,e_6)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_172]) ).
tcf(c_667,plain,
! [X0: $i,X1: $i] :
( product(e_6,X0,e_2)
| ~ product(e_6,X1,X0)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_439]) ).
tcf(c_668,plain,
( product(e_6,e_1,e_2)
| ~ product(e_6,e_1,e_1)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_667]) ).
tcf(c_669,plain,
! [X0: $i] :
( equalish(e_1,e_6)
| ~ product(X0,e_6,e_2)
| ~ product(X0,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_671,plain,
( equalish(e_1,e_6)
| ~ product(e_1,e_6,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_669]) ).
tcf(c_672,plain,
! [X0: $i] :
( equalish(e_1,e_6)
| ~ product(e_6,X0,e_2)
| ~ product(e_1,X0,e_2) ),
inference(instantiation,[status(thm)],[c_234]) ).
tcf(c_674,plain,
( equalish(e_1,e_6)
| ~ product(e_6,e_1,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_672]) ).
tcf(c_725,plain,
( product(e_2,e_2,e_6)
| 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_399]) ).
tcf(c_730,plain,
( product(e_3,e_2,e_6)
| product(e_3,e_2,e_5)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_1)
| ~ group_element(e_3)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_771,plain,
! [X0: $i] :
( equalish(e_2,e_1)
| ~ product(e_2,X0,e_2)
| ~ product(e_1,X0,e_2) ),
inference(instantiation,[status(thm)],[c_240]) ).
tcf(c_772,plain,
! [X0: $i] :
( equalish(e_1,e_2)
| ~ product(e_2,X0,e_2)
| ~ product(e_1,X0,e_2) ),
inference(instantiation,[status(thm)],[c_210]) ).
tcf(c_773,plain,
( equalish(e_1,e_2)
| ~ product(e_2,e_1,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_772]) ).
tcf(c_780,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_274]) ).
tcf(c_793,plain,
( product(e_2,e_5,e_6)
| 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_403]) ).
tcf(c_796,plain,
( equalish(e_5,e_4)
| ~ product(e_2,e_5,e_2)
| ~ product(e_2,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_346]) ).
tcf(c_801,plain,
( equalish(e_3,e_5)
| ~ product(e_2,e_5,e_2)
| ~ product(e_2,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_286]) ).
tcf(c_811,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_268]) ).
tcf(c_813,plain,
! [X0: $i] :
( equalish(e_1,e_3)
| ~ product(X0,e_3,e_2)
| ~ product(X0,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_214]) ).
tcf(c_814,plain,
( equalish(e_1,e_3)
| ~ product(e_1,e_3,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_813]) ).
tcf(c_816,plain,
( equalish(e_3,e_1)
| ~ product(e_1,e_3,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_820,plain,
( product(e_3,e_3,e_6)
| 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_410]) ).
tcf(c_827,plain,
( product(e_4,e_3,e_6)
| 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_410]) ).
tcf(c_834,plain,
( equalish(e_2,e_4)
| ~ product(e_4,e_3,e_2)
| ~ product(e_2,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_252]) ).
tcf(c_836,plain,
( product(e_5,e_3,e_6)
| 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_410]) ).
tcf(c_845,plain,
( equalish(e_2,e_5)
| ~ product(e_5,e_3,e_2)
| ~ product(e_2,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_258]) ).
tcf(c_896,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,e_2)
| ~ product(X1,e_3,e_2)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_405]) ).
tcf(c_900,plain,
( product(e_6,e_3,e_6)
| product(e_6,e_3,e_5)
| product(e_6,e_3,e_4)
| product(e_6,e_3,e_3)
| product(e_6,e_3,e_2)
| product(e_6,e_3,e_1)
| ~ group_element(e_6)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_410]) ).
tcf(c_940,plain,
! [X0: $i] :
( equalish(e_6,e_2)
| ~ product(X0,e_6,e_3)
| ~ product(X0,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_364]) ).
tcf(c_942,plain,
! [X0: $i] :
( equalish(e_2,e_1)
| ~ product(X0,e_2,e_3)
| ~ product(X0,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_238]) ).
tcf(c_947,plain,
( equalish(e_6,e_2)
| ~ product(e_1,e_6,e_3)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_940]) ).
tcf(c_949,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_407]) ).
tcf(c_977,plain,
! [X0: $i] :
( equalish(e_2,e_6)
| ~ product(e_6,X0,e_3)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_264]) ).
tcf(c_982,plain,
( equalish(e_2,e_6)
| ~ product(e_6,e_1,e_3)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_977]) ).
tcf(c_984,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_407]) ).
tcf(c_997,plain,
( product(e_2,e_6,e_6)
| product(e_2,e_6,e_5)
| product(e_2,e_6,e_4)
| product(e_2,e_6,e_3)
| product(e_2,e_6,e_2)
| product(e_2,e_6,e_1)
| ~ group_element(e_6)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_403]) ).
tcf(c_999,plain,
( equalish(e_1,e_6)
| ~ product(e_2,e_6,e_3)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_1000,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_396]) ).
tcf(c_1001,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_1000]) ).
tcf(c_1008,plain,
! [X0: $i] :
( equalish(e_6,e_3)
| ~ product(e_6,X0,e_2)
| ~ product(e_3,X0,e_2) ),
inference(instantiation,[status(thm)],[c_372]) ).
tcf(c_1009,plain,
! [X0: $i] :
( equalish(e_3,e_6)
| ~ product(e_6,X0,e_2)
| ~ product(e_3,X0,e_2) ),
inference(instantiation,[status(thm)],[c_294]) ).
tcf(c_1010,plain,
! [X0: $i] :
( equalish(e_3,e_2)
| ~ product(e_3,X0,e_2)
| ~ product(e_2,X0,e_2) ),
inference(instantiation,[status(thm)],[c_276]) ).
tcf(c_1011,plain,
! [X0: $i] :
( equalish(e_3,e_1)
| ~ product(e_3,X0,e_2)
| ~ product(e_1,X0,e_2) ),
inference(instantiation,[status(thm)],[c_270]) ).
tcf(c_1013,plain,
! [X0: $i] :
( equalish(e_1,e_3)
| ~ product(e_3,X0,e_2)
| ~ product(e_1,X0,e_2) ),
inference(instantiation,[status(thm)],[c_216]) ).
tcf(c_1014,plain,
( equalish(e_1,e_3)
| ~ product(e_3,e_1,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1013]) ).
tcf(c_1016,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_1,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1011]) ).
tcf(c_1018,plain,
( equalish(e_3,e_6)
| ~ product(e_6,e_1,e_2)
| ~ product(e_3,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1009]) ).
tcf(c_1019,plain,
( equalish(e_6,e_3)
| ~ product(e_6,e_1,e_2)
| ~ product(e_3,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1008]) ).
tcf(c_1020,plain,
( product(e_3,e_4,e_6)
| 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_414]) ).
tcf(c_1028,plain,
( equalish(e_1,e_4)
| ~ product(e_3,e_4,e_2)
| ~ product(e_3,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_220]) ).
tcf(c_1029,plain,
( product(e_3,e_5,e_6)
| 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_414]) ).
tcf(c_1039,plain,
( equalish(e_1,e_5)
| ~ product(e_3,e_5,e_2)
| ~ product(e_3,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_226]) ).
tcf(c_1040,plain,
( product(e_3,e_6,e_6)
| product(e_3,e_6,e_5)
| product(e_3,e_6,e_4)
| product(e_3,e_6,e_3)
| product(e_3,e_6,e_2)
| product(e_3,e_6,e_1)
| ~ group_element(e_6)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_414]) ).
tcf(c_1041,plain,
( equalish(e_6,e_1)
| ~ product(e_3,e_6,e_2)
| ~ product(e_3,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_358]) ).
tcf(c_1043,plain,
! [X0: $i,X1: $i] :
( product(X0,e_3,e_2)
| ~ product(e_3,X1,e_2)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_405]) ).
tcf(c_1058,plain,
! [X0: $i] :
( equalish(e_1,e_4)
| ~ product(X0,e_4,e_2)
| ~ product(X0,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_220]) ).
tcf(c_1059,plain,
( equalish(e_1,e_4)
| ~ product(e_1,e_4,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1058]) ).
tcf(c_1076,plain,
( product(e_5,e_4,e_6)
| 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_419]) ).
tcf(c_1087,plain,
( product(e_6,e_4,e_6)
| product(e_6,e_4,e_5)
| product(e_6,e_4,e_4)
| product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| ~ group_element(e_6)
| ~ group_element(e_4) ),
inference(instantiation,[status(thm)],[c_419]) ).
tcf(c_1092,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,e_2)
| ~ product(X1,e_4,e_2)
| ~ product(X0,e_4,X1) ),
inference(instantiation,[status(thm)],[c_405]) ).
tcf(c_1104,plain,
! [X0: $i] :
( equalish(e_4,e_6)
| ~ product(e_6,X0,e_2)
| ~ product(e_4,X0,e_2) ),
inference(instantiation,[status(thm)],[c_324]) ).
tcf(c_1105,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_312]) ).
tcf(c_1107,plain,
! [X0: $i] :
( equalish(e_4,e_1)
| ~ product(e_4,X0,e_2)
| ~ product(e_1,X0,e_2) ),
inference(instantiation,[status(thm)],[c_300]) ).
tcf(c_1108,plain,
! [X0: $i] :
( equalish(e_3,e_4)
| ~ product(e_4,X0,e_2)
| ~ product(e_3,X0,e_2) ),
inference(instantiation,[status(thm)],[c_282]) ).
tcf(c_1110,plain,
! [X0: $i] :
( equalish(e_1,e_4)
| ~ product(e_4,X0,e_2)
| ~ product(e_1,X0,e_2) ),
inference(instantiation,[status(thm)],[c_222]) ).
tcf(c_1111,plain,
( equalish(e_1,e_4)
| ~ product(e_4,e_1,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1110]) ).
tcf(c_1113,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_1,e_2)
| ~ product(e_3,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1108]) ).
tcf(c_1114,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_1,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1107]) ).
tcf(c_1116,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_1,e_2)
| ~ product(e_3,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1105]) ).
tcf(c_1117,plain,
( equalish(e_4,e_6)
| ~ product(e_6,e_1,e_2)
| ~ product(e_4,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1104]) ).
tcf(c_1119,plain,
( product(e_4,e_5,e_6)
| 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_423]) ).
tcf(c_1129,plain,
( equalish(e_1,e_5)
| ~ product(e_4,e_5,e_2)
| ~ product(e_4,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_226]) ).
tcf(c_1131,plain,
( equalish(e_6,e_1)
| ~ product(e_4,e_6,e_2)
| ~ product(e_4,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_358]) ).
tcf(c_1133,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_405]) ).
tcf(c_1142,plain,
! [X0: $i] :
( equalish(e_6,e_5)
| ~ product(X0,e_6,e_2)
| ~ product(X0,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_382]) ).
tcf(c_1145,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_340]) ).
tcf(c_1151,plain,
! [X0: $i] :
( equalish(e_1,e_5)
| ~ product(X0,e_5,e_2)
| ~ product(X0,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_226]) ).
tcf(c_1152,plain,
( equalish(e_1,e_5)
| ~ product(e_1,e_5,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1151]) ).
tcf(c_1161,plain,
( equalish(e_6,e_5)
| ~ product(e_1,e_6,e_2)
| ~ product(e_1,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_1142]) ).
tcf(c_1162,plain,
( product(e_5,e_5,e_6)
| 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_428]) ).
tcf(c_1163,plain,
( equalish(e_6,e_5)
| ~ product(e_6,e_5,e_2)
| ~ product(e_5,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_384]) ).
tcf(c_1169,plain,
( equalish(e_4,e_5)
| ~ product(e_5,e_5,e_2)
| ~ product(e_4,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_318]) ).
tcf(c_1173,plain,
( product(e_6,e_5,e_6)
| product(e_6,e_5,e_5)
| product(e_6,e_5,e_4)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| ~ group_element(e_6)
| ~ group_element(e_5) ),
inference(instantiation,[status(thm)],[c_428]) ).
tcf(c_1174,plain,
( equalish(e_6,e_1)
| ~ product(e_6,e_5,e_2)
| ~ product(e_1,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_360]) ).
tcf(c_1190,plain,
! [X0: $i] :
( equalish(e_6,e_5)
| ~ product(e_6,X0,e_2)
| ~ product(e_5,X0,e_2) ),
inference(instantiation,[status(thm)],[c_384]) ).
tcf(c_1193,plain,
! [X0: $i] :
( equalish(e_5,e_3)
| ~ product(e_5,X0,e_2)
| ~ product(e_3,X0,e_2) ),
inference(instantiation,[status(thm)],[c_342]) ).
tcf(c_1194,plain,
! [X0: $i] :
( equalish(e_5,e_2)
| ~ product(e_5,X0,e_2)
| ~ product(e_2,X0,e_2) ),
inference(instantiation,[status(thm)],[c_336]) ).
tcf(c_1195,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_330]) ).
tcf(c_1196,plain,
! [X0: $i] :
( equalish(e_4,e_5)
| ~ product(e_5,X0,e_2)
| ~ product(e_4,X0,e_2) ),
inference(instantiation,[status(thm)],[c_318]) ).
tcf(c_1197,plain,
! [X0: $i] :
( equalish(e_3,e_5)
| ~ product(e_5,X0,e_2)
| ~ product(e_3,X0,e_2) ),
inference(instantiation,[status(thm)],[c_288]) ).
tcf(c_1199,plain,
! [X0: $i] :
( equalish(e_1,e_5)
| ~ product(e_5,X0,e_2)
| ~ product(e_1,X0,e_2) ),
inference(instantiation,[status(thm)],[c_228]) ).
tcf(c_1200,plain,
( equalish(e_1,e_5)
| ~ product(e_5,e_1,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1199]) ).
tcf(c_1202,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_1197]) ).
tcf(c_1203,plain,
( equalish(e_4,e_5)
| ~ product(e_5,e_1,e_2)
| ~ product(e_4,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1196]) ).
tcf(c_1209,plain,
( equalish(e_6,e_5)
| ~ product(e_6,e_1,e_2)
| ~ product(e_5,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1190]) ).
tcf(c_1210,plain,
( product(e_5,e_6,e_6)
| product(e_5,e_6,e_5)
| product(e_5,e_6,e_4)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| ~ group_element(e_6)
| ~ group_element(e_5) ),
inference(instantiation,[status(thm)],[c_432]) ).
tcf(c_1213,plain,
! [X0: $i,X1: $i] :
( product(X0,e_5,e_2)
| ~ product(e_5,X1,e_2)
| ~ product(X0,X1,e_5) ),
inference(instantiation,[status(thm)],[c_405]) ).
tcf(c_1215,plain,
! [X0: $i,X1: $i] :
( product(e_5,e_2,X1)
| ~ product(e_5,X0,e_2)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_430]) ).
tcf(c_1231,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,e_2)
| ~ product(X1,e_6,e_2)
| ~ product(X0,e_6,X1) ),
inference(instantiation,[status(thm)],[c_405]) ).
tcf(c_1247,plain,
! [X0: $i,X1: $i] :
( product(X0,e_6,e_2)
| ~ product(e_6,X1,e_2)
| ~ product(X0,X1,e_6) ),
inference(instantiation,[status(thm)],[c_405]) ).
tcf(c_1379,plain,
! [X0: $i] :
( product(e_6,e_2,e_3)
| ~ product(e_6,X0,e_2)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_1000]) ).
tcf(c_1380,plain,
( product(e_6,e_2,e_3)
| ~ product(e_6,e_1,e_2)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_1379]) ).
tcf(c_1459,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_396]) ).
tcf(c_1460,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_1459]) ).
tcf(c_1552,plain,
! [X0: $i,X1: $i] :
( product(X0,e_3,X1)
| ~ product(e_3,e_3,X1)
| ~ product(X0,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_407]) ).
tcf(c_1561,plain,
( product(e_1,e_3,e_1)
| ~ product(e_3,e_3,e_1)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_1552]) ).
tcf(c_1562,plain,
! [X0: $i] :
( equalish(e_6,e_3)
| ~ product(X0,e_6,e_3)
| ~ product(X0,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_370]) ).
tcf(c_1573,plain,
( equalish(e_6,e_3)
| ~ product(e_1,e_6,e_3)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_1562]) ).
tcf(c_1583,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_406]) ).
tcf(c_1605,plain,
( equalish(e_3,e_5)
| ~ product(e_5,e_2,e_1)
| ~ product(e_3,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_288]) ).
tcf(c_1678,plain,
! [X0: $i] :
( equalish(e_6,e_3)
| ~ product(e_6,X0,e_3)
| ~ product(e_3,X0,e_3) ),
inference(instantiation,[status(thm)],[c_372]) ).
tcf(c_1681,plain,
! [X0: $i] :
( equalish(e_3,e_1)
| ~ product(e_3,X0,e_3)
| ~ product(e_1,X0,e_3) ),
inference(instantiation,[status(thm)],[c_270]) ).
tcf(c_1711,plain,
! [X0: $i] :
( equalish(e_6,e_4)
| ~ product(X0,e_6,e_3)
| ~ product(X0,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_376]) ).
tcf(c_1714,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_304]) ).
tcf(c_1715,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_298]) ).
tcf(c_1723,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_1714]) ).
tcf(c_1726,plain,
( equalish(e_6,e_4)
| ~ product(e_1,e_6,e_3)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_1711]) ).
tcf(c_1731,plain,
! [X0: $i] :
( product(X0,e_1,e_3)
| ~ product(e_1,e_4,e_3)
| ~ product(X0,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_386]) ).
tcf(c_1784,plain,
! [X0: $i] :
( product(e_2,e_1,X0)
| ~ product(e_2,e_5,e_1)
| ~ product(e_1,e_5,X0) ),
inference(instantiation,[status(thm)],[c_401]) ).
tcf(c_1812,plain,
! [X0: $i] :
( product(e_3,e_1,X0)
| ~ product(e_3,e_3,e_1)
| ~ product(e_1,e_3,X0) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_1835,plain,
! [X0: $i] :
( equalish(e_4,e_6)
| ~ product(e_6,X0,e_3)
| ~ product(e_4,X0,e_3) ),
inference(instantiation,[status(thm)],[c_324]) ).
tcf(c_1840,plain,
! [X0: $i] :
( equalish(e_2,e_4)
| ~ product(e_4,X0,e_3)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_252]) ).
tcf(c_1843,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_1840]) ).
tcf(c_1848,plain,
( equalish(e_4,e_6)
| ~ product(e_6,e_1,e_3)
| ~ product(e_4,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_1835]) ).
tcf(c_1853,plain,
! [X0: $i,X1: $i] :
( product(X0,e_4,e_3)
| ~ product(e_4,X1,e_3)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_406]) ).
tcf(c_1870,plain,
! [X0: $i] :
( equalish(e_6,e_5)
| ~ product(X0,e_6,e_3)
| ~ product(X0,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_382]) ).
tcf(c_1872,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_346]) ).
tcf(c_1873,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_340]) ).
tcf(c_1874,plain,
! [X0: $i] :
( equalish(e_5,e_2)
| ~ product(X0,e_5,e_3)
| ~ product(X0,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_334]) ).
tcf(c_1875,plain,
! [X0: $i] :
( equalish(e_5,e_1)
| ~ product(X0,e_5,e_3)
| ~ product(X0,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_328]) ).
tcf(c_1876,plain,
! [X0: $i] :
( equalish(e_4,e_5)
| ~ product(X0,e_5,e_3)
| ~ product(X0,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_316]) ).
tcf(c_1883,plain,
( equalish(e_4,e_5)
| ~ product(e_1,e_5,e_3)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_1876]) ).
tcf(c_1889,plain,
( equalish(e_6,e_5)
| ~ product(e_1,e_6,e_3)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_1870]) ).
tcf(c_1893,plain,
! [X0: $i] :
( product(X0,e_1,e_3)
| ~ product(e_1,e_5,e_3)
| ~ product(X0,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_386]) ).
tcf(c_1897,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,e_3)
| ~ product(X1,e_5,e_3)
| ~ product(X0,e_5,X1) ),
inference(instantiation,[status(thm)],[c_406]) ).
tcf(c_1904,plain,
( equalish(e_6,e_3)
| ~ product(e_4,e_6,e_1)
| ~ product(e_4,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_370]) ).
tcf(c_1910,plain,
( equalish(e_6,e_4)
| ~ product(e_6,e_3,e_1)
| ~ product(e_4,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_378]) ).
tcf(c_1919,plain,
! [X0: $i] :
( product(e_4,e_1,X0)
| ~ product(e_4,e_3,e_1)
| ~ product(e_1,e_3,X0) ),
inference(instantiation,[status(thm)],[c_421]) ).
tcf(c_1947,plain,
! [X0: $i] :
( product(e_5,e_1,X0)
| ~ product(e_5,e_3,e_1)
| ~ product(e_1,e_3,X0) ),
inference(instantiation,[status(thm)],[c_430]) ).
tcf(c_1990,plain,
! [X0: $i] :
( equalish(e_6,e_5)
| ~ product(e_6,X0,e_3)
| ~ product(e_5,X0,e_3) ),
inference(instantiation,[status(thm)],[c_384]) ).
tcf(c_1992,plain,
! [X0: $i] :
( equalish(e_5,e_4)
| ~ product(e_5,X0,e_3)
| ~ product(e_4,X0,e_3) ),
inference(instantiation,[status(thm)],[c_348]) ).
tcf(c_1994,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_336]) ).
tcf(c_1996,plain,
! [X0: $i] :
( equalish(e_4,e_5)
| ~ product(e_5,X0,e_3)
| ~ product(e_4,X0,e_3) ),
inference(instantiation,[status(thm)],[c_318]) ).
tcf(c_1998,plain,
! [X0: $i] :
( equalish(e_2,e_5)
| ~ product(e_5,X0,e_3)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_258]) ).
tcf(c_2001,plain,
( equalish(e_2,e_5)
| ~ product(e_5,e_1,e_3)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_1998]) ).
tcf(c_2003,plain,
( equalish(e_4,e_5)
| ~ product(e_5,e_1,e_3)
| ~ product(e_4,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_1996]) ).
tcf(c_2009,plain,
( equalish(e_6,e_5)
| ~ product(e_6,e_1,e_3)
| ~ product(e_5,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_1990]) ).
tcf(c_2069,plain,
! [X0: $i] :
( product(e_3,e_1,X0)
| ~ product(e_3,e_4,e_1)
| ~ product(e_1,e_4,X0) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_2083,plain,
( equalish(e_3,e_6)
| ~ product(e_6,e_5,e_1)
| ~ product(e_3,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_294]) ).
tcf(c_2098,plain,
! [X0: $i] :
( product(e_3,e_1,X0)
| ~ product(e_3,e_5,e_1)
| ~ product(e_1,e_5,X0) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_2130,plain,
! [X0: $i] :
( product(X0,e_3,e_2)
| ~ product(e_3,e_6,e_2)
| ~ product(X0,e_6,e_3) ),
inference(instantiation,[status(thm)],[c_1043]) ).
tcf(c_2131,plain,
( product(e_1,e_3,e_2)
| ~ product(e_3,e_6,e_2)
| ~ product(e_1,e_6,e_3) ),
inference(instantiation,[status(thm)],[c_2130]) ).
tcf(c_2223,plain,
! [X0: $i] :
( product(X0,e_6,e_2)
| ~ product(e_6,e_4,e_2)
| ~ product(X0,e_4,e_6) ),
inference(instantiation,[status(thm)],[c_1092]) ).
tcf(c_2224,plain,
( product(e_1,e_6,e_2)
| ~ product(e_6,e_4,e_2)
| ~ product(e_1,e_4,e_6) ),
inference(instantiation,[status(thm)],[c_2223]) ).
tcf(c_2244,plain,
! [X0: $i] :
( product(e_4,e_1,X0)
| ~ product(e_4,e_5,e_1)
| ~ product(e_1,e_5,X0) ),
inference(instantiation,[status(thm)],[c_421]) ).
tcf(c_2491,plain,
! [X0: $i,X1: $i] :
( product(X0,e_3,X1)
| ~ product(e_3,e_6,X1)
| ~ product(X0,e_6,e_3) ),
inference(instantiation,[status(thm)],[c_407]) ).
tcf(c_2494,plain,
! [X0: $i] :
( equalish(e_2,e_3)
| ~ product(X0,e_6,e_3)
| ~ product(X0,e_6,e_2) ),
inference(instantiation,[status(thm)],[c_242]) ).
tcf(c_2497,plain,
( equalish(e_2,e_3)
| ~ product(e_1,e_6,e_3)
| ~ product(e_1,e_6,e_2) ),
inference(instantiation,[status(thm)],[c_2494]) ).
tcf(c_2500,plain,
( product(e_1,e_3,e_1)
| ~ product(e_3,e_6,e_1)
| ~ product(e_1,e_6,e_3) ),
inference(instantiation,[status(thm)],[c_2491]) ).
tcf(c_2546,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_396]) ).
tcf(c_2547,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_2546]) ).
tcf(c_2565,plain,
( equalish(e_3,e_2)
| ~ product(e_3,e_6,e_2)
| ~ product(e_2,e_6,e_2) ),
inference(instantiation,[status(thm)],[c_1010]) ).
tcf(c_2698,plain,
( equalish(e_5,e_3)
| ~ product(e_6,e_5,e_2)
| ~ product(e_6,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_1145]) ).
tcf(c_2704,plain,
( equalish(e_3,e_1)
| ~ product(e_6,e_3,e_2)
| ~ product(e_6,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_2709,plain,
! [X0: $i] :
( product(X0,e_6,e_2)
| ~ product(e_6,e_3,e_2)
| ~ product(X0,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_896]) ).
tcf(c_2710,plain,
( product(e_1,e_6,e_2)
| ~ product(e_6,e_3,e_2)
| ~ product(e_1,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_2709]) ).
tcf(c_2841,plain,
( product(e_3,e_1,e_3)
| ~ product(e_3,e_4,e_1)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_1731]) ).
tcf(c_2843,plain,
( product(e_5,e_1,e_3)
| ~ product(e_5,e_4,e_1)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_1731]) ).
tcf(c_2877,plain,
( product(e_3,e_1,e_3)
| ~ product(e_3,e_5,e_1)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_1893]) ).
tcf(c_2879,plain,
( product(e_5,e_1,e_3)
| ~ product(e_5,e_5,e_1)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_1893]) ).
tcf(c_3080,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_984]) ).
tcf(c_3081,plain,
! [X0: $i] :
( equalish(e_6,e_3)
| ~ product(e_6,X0,e_4)
| ~ product(e_3,X0,e_4) ),
inference(instantiation,[status(thm)],[c_372]) ).
tcf(c_3082,plain,
! [X0: $i] :
( equalish(e_3,e_6)
| ~ product(e_6,X0,e_4)
| ~ product(e_3,X0,e_4) ),
inference(instantiation,[status(thm)],[c_294]) ).
tcf(c_3084,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_270]) ).
tcf(c_3091,plain,
( equalish(e_3,e_6)
| ~ product(e_6,e_1,e_4)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_3082]) ).
tcf(c_3092,plain,
( equalish(e_6,e_3)
| ~ product(e_6,e_1,e_4)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_3081]) ).
tcf(c_3093,plain,
( product(e_2,e_3,e_4)
| ~ product(e_3,e_1,e_4)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_3080]) ).
tcf(c_3094,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_1133]) ).
tcf(c_3095,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_416]) ).
tcf(c_3108,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_3095]) ).
tcf(c_3109,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_3094]) ).
tcf(c_3114,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_494]) ).
tcf(c_3127,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_1133]) ).
tcf(c_3128,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_416]) ).
tcf(c_3129,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_308]) ).
tcf(c_3130,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_302]) ).
tcf(c_3131,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_296]) ).
tcf(c_3135,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_3128]) ).
tcf(c_3137,plain,
( equalish(e_5,e_6)
| ~ product(e_1,e_6,e_4)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_3138,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_346]) ).
tcf(c_3139,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_340]) ).
tcf(c_3140,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_334]) ).
tcf(c_3150,plain,
( product(e_4,e_1,e_4)
| ~ product(e_4,e_5,e_1)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_2244]) ).
tcf(c_3151,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_2098]) ).
tcf(c_3152,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_1784]) ).
tcf(c_3176,plain,
( product(e_6,e_3,e_2)
| ~ product(e_6,e_3,e_3)
| ~ product(e_3,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_896]) ).
tcf(c_3208,plain,
( equalish(e_2,e_1)
| ~ product(e_2,e_3,e_2)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_771]) ).
tcf(c_3236,plain,
! [X0: $i] :
( product(X0,e_6,e_3)
| ~ product(e_6,e_3,e_3)
| ~ product(X0,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_1583]) ).
tcf(c_3237,plain,
( product(e_1,e_6,e_3)
| ~ product(e_6,e_3,e_3)
| ~ product(e_1,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_3236]) ).
tcf(c_3297,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_298]) ).
tcf(c_3311,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,e_4)
| ~ product(X1,e_4,e_4)
| ~ product(X0,e_4,X1) ),
inference(instantiation,[status(thm)],[c_494]) ).
tcf(c_3337,plain,
! [X0: $i] :
( equalish(e_4,e_2)
| ~ product(e_4,X0,e_4)
| ~ product(e_2,X0,e_4) ),
inference(instantiation,[status(thm)],[c_306]) ).
tcf(c_3338,plain,
! [X0: $i] :
( equalish(e_4,e_1)
| ~ product(e_4,X0,e_4)
| ~ product(e_1,X0,e_4) ),
inference(instantiation,[status(thm)],[c_300]) ).
tcf(c_3339,plain,
! [X0: $i] :
( equalish(e_3,e_4)
| ~ product(e_4,X0,e_4)
| ~ product(e_3,X0,e_4) ),
inference(instantiation,[status(thm)],[c_282]) ).
tcf(c_3344,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_3339]) ).
tcf(c_3383,plain,
! [X0: $i] :
( equalish(e_6,e_2)
| ~ product(X0,e_6,e_6)
| ~ product(X0,e_2,e_6) ),
inference(instantiation,[status(thm)],[c_364]) ).
tcf(c_3390,plain,
( equalish(e_6,e_2)
| ~ product(e_1,e_6,e_6)
| ~ product(e_1,e_2,e_6) ),
inference(instantiation,[status(thm)],[c_3383]) ).
tcf(c_3437,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_1213]) ).
tcf(c_3438,plain,
! [X0: $i,X1: $i] :
( product(X0,e_5,X1)
| ~ product(e_5,e_5,X1)
| ~ product(X0,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_425]) ).
tcf(c_3439,plain,
! [X0: $i] :
( equalish(e_5,e_4)
| ~ product(X0,e_5,e_5)
| ~ product(X0,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_344]) ).
tcf(c_3440,plain,
! [X0: $i] :
( equalish(e_5,e_3)
| ~ product(X0,e_5,e_5)
| ~ product(X0,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_338]) ).
tcf(c_3441,plain,
! [X0: $i] :
( equalish(e_5,e_2)
| ~ product(X0,e_5,e_5)
| ~ product(X0,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_332]) ).
tcf(c_3452,plain,
( equalish(e_5,e_2)
| ~ product(e_1,e_5,e_5)
| ~ product(e_1,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_3441]) ).
tcf(c_3453,plain,
( equalish(e_5,e_3)
| ~ product(e_1,e_5,e_5)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_3440]) ).
tcf(c_3454,plain,
( equalish(e_5,e_4)
| ~ product(e_1,e_5,e_5)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_3439]) ).
tcf(c_3455,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_3438]) ).
tcf(c_3456,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_3437]) ).
tcf(c_3457,plain,
! [X0: $i] :
( equalish(e_6,e_5)
| ~ product(X0,e_6,e_5)
| ~ product(X0,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_382]) ).
tcf(c_3459,plain,
! [X0: $i] :
( equalish(e_5,e_4)
| ~ product(X0,e_5,e_5)
| ~ product(X0,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_346]) ).
tcf(c_3460,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_340]) ).
tcf(c_3462,plain,
! [X0: $i] :
( equalish(e_5,e_1)
| ~ product(X0,e_5,e_5)
| ~ product(X0,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_328]) ).
tcf(c_3486,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,e_5)
| ~ product(X1,e_5,e_5)
| ~ product(X0,e_5,X1) ),
inference(instantiation,[status(thm)],[c_495]) ).
tcf(c_3558,plain,
! [X0: $i] :
( equalish(e_6,e_5)
| ~ product(e_6,X0,e_4)
| ~ product(e_5,X0,e_4) ),
inference(instantiation,[status(thm)],[c_384]) ).
tcf(c_3562,plain,
! [X0: $i] :
( equalish(e_5,e_2)
| ~ product(e_5,X0,e_4)
| ~ product(e_2,X0,e_4) ),
inference(instantiation,[status(thm)],[c_336]) ).
tcf(c_3563,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_330]) ).
tcf(c_3565,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_288]) ).
tcf(c_3570,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_3565]) ).
tcf(c_3577,plain,
( equalish(e_6,e_5)
| ~ product(e_6,e_1,e_4)
| ~ product(e_5,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_3558]) ).
tcf(c_3580,plain,
! [X0: $i,X1: $i] :
( product(X0,e_5,e_4)
| ~ product(e_5,X1,e_4)
| ~ product(X0,X1,e_5) ),
inference(instantiation,[status(thm)],[c_494]) ).
tcf(c_3586,plain,
! [X0: $i] :
( product(X0,e_5,e_2)
| ~ product(e_5,e_6,e_2)
| ~ product(X0,e_6,e_5) ),
inference(instantiation,[status(thm)],[c_1213]) ).
tcf(c_3587,plain,
! [X0: $i,X1: $i] :
( product(X0,e_5,X1)
| ~ product(e_5,e_6,X1)
| ~ product(X0,e_6,e_5) ),
inference(instantiation,[status(thm)],[c_425]) ).
tcf(c_3608,plain,
! [X0: $i] :
( equalish(e_6,e_1)
| ~ product(X0,e_6,e_5)
| ~ product(X0,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_358]) ).
tcf(c_3692,plain,
! [X0: $i] :
( product(e_6,e_3,X0)
| ~ product(e_6,e_2,e_3)
| ~ product(e_3,e_2,X0) ),
inference(instantiation,[status(thm)],[c_949]) ).
tcf(c_3693,plain,
( product(e_6,e_3,e_1)
| ~ product(e_6,e_2,e_3)
| ~ product(e_3,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_3692]) ).
tcf(c_3854,plain,
( equalish(e_2,e_1)
| ~ product(e_2,e_2,e_3)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_942]) ).
tcf(c_3886,plain,
! [X0: $i] :
( product(e_3,e_6,X0)
| ~ product(e_3,e_2,e_6)
| ~ product(e_6,e_2,X0) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_4000,plain,
! [X0: $i] :
( product(X0,e_4,e_3)
| ~ product(e_4,e_3,e_3)
| ~ product(X0,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_1583]) ).
tcf(c_4001,plain,
( product(e_1,e_4,e_3)
| ~ product(e_4,e_3,e_3)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_4000]) ).
tcf(c_4029,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_1583]) ).
tcf(c_4030,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_4029]) ).
tcf(c_4073,plain,
! [X0: $i] :
( product(e_2,e_1,X0)
| ~ product(e_2,e_6,e_1)
| ~ product(e_1,e_6,X0) ),
inference(instantiation,[status(thm)],[c_401]) ).
tcf(c_4151,plain,
! [X0: $i] :
( product(e_3,e_1,X0)
| ~ product(e_3,e_6,e_1)
| ~ product(e_1,e_6,X0) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_4714,plain,
( equalish(e_5,e_1)
| ~ product(e_5,e_6,e_2)
| ~ product(e_1,e_6,e_2) ),
inference(instantiation,[status(thm)],[c_1195]) ).
tcf(c_4715,plain,
( equalish(e_5,e_2)
| ~ product(e_5,e_6,e_2)
| ~ product(e_2,e_6,e_2) ),
inference(instantiation,[status(thm)],[c_1194]) ).
tcf(c_4716,plain,
( equalish(e_5,e_3)
| ~ product(e_5,e_6,e_2)
| ~ product(e_3,e_6,e_2) ),
inference(instantiation,[status(thm)],[c_1193]) ).
tcf(c_4721,plain,
! [X0: $i] :
( product(e_5,e_2,X0)
| ~ product(e_5,e_6,e_2)
| ~ product(e_2,e_6,X0) ),
inference(instantiation,[status(thm)],[c_1215]) ).
tcf(c_4722,plain,
( product(e_5,e_2,e_1)
| ~ product(e_5,e_6,e_2)
| ~ product(e_2,e_6,e_1) ),
inference(instantiation,[status(thm)],[c_4721]) ).
tcf(c_4834,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_1853]) ).
tcf(c_4835,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_4834]) ).
tcf(c_5016,plain,
( product(e_2,e_4,e_2)
| ~ product(e_4,e_3,e_2)
| ~ product(e_2,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_896]) ).
tcf(c_5018,plain,
( equalish(e_3,e_6)
| ~ product(e_2,e_6,e_4)
| ~ product(e_2,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_292]) ).
tcf(c_5024,plain,
! [X0: $i] :
( product(e_2,e_4,X0)
| ~ product(e_2,e_3,e_4)
| ~ product(e_4,e_3,X0) ),
inference(instantiation,[status(thm)],[c_416]) ).
tcf(c_5032,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_396]) ).
tcf(c_5033,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_5032]) ).
tcf(c_5141,plain,
( equalish(e_6,e_3)
| ~ product(e_6,e_3,e_3)
| ~ product(e_3,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_1678]) ).
tcf(c_5142,plain,
( equalish(e_6,e_3)
| ~ product(e_6,e_2,e_3)
| ~ product(e_3,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_1678]) ).
tcf(c_5196,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_1715]) ).
tcf(c_5304,plain,
( equalish(e_5,e_2)
| ~ product(e_3,e_5,e_3)
| ~ product(e_3,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_1874]) ).
tcf(c_5309,plain,
( equalish(e_5,e_1)
| ~ product(e_2,e_5,e_3)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_1875]) ).
tcf(c_5349,plain,
( equalish(e_6,e_5)
| ~ product(e_6,e_3,e_3)
| ~ product(e_5,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_1990]) ).
tcf(c_5356,plain,
( equalish(e_5,e_4)
| ~ product(e_5,e_3,e_3)
| ~ product(e_4,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_1992]) ).
tcf(c_5464,plain,
( product(e_3,e_6,e_3)
| ~ product(e_6,e_2,e_3)
| ~ product(e_3,e_2,e_6) ),
inference(instantiation,[status(thm)],[c_3886]) ).
tcf(c_5505,plain,
( product(e_2,e_4,e_3)
| ~ product(e_4,e_3,e_3)
| ~ product(e_2,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_5024]) ).
tcf(c_5508,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_896]) ).
tcf(c_5510,plain,
( equalish(e_3,e_6)
| ~ product(e_1,e_6,e_5)
| ~ product(e_1,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_292]) ).
tcf(c_5511,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_274]) ).
tcf(c_5516,plain,
! [X0: $i] :
( product(e_1,e_5,X0)
| ~ product(e_1,e_3,e_5)
| ~ product(e_5,e_3,X0) ),
inference(instantiation,[status(thm)],[c_425]) ).
tcf(c_5525,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_5516]) ).
tcf(c_5530,plain,
( product(e_4,e_1,e_5)
| ~ product(e_4,e_3,e_1)
| ~ product(e_1,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_1919]) ).
tcf(c_5546,plain,
( product(e_5,e_3,e_4)
| ~ product(e_5,e_4,e_3)
| ~ product(e_3,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_3114]) ).
tcf(c_5569,plain,
! [X0: $i] :
( product(X0,e_6,e_5)
| ~ product(e_6,e_3,e_5)
| ~ product(X0,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_495]) ).
tcf(c_5570,plain,
( product(e_1,e_6,e_5)
| ~ product(e_6,e_3,e_5)
| ~ product(e_1,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_5569]) ).
tcf(c_5609,plain,
! [X0: $i] :
( equalish(e_6,e_3)
| ~ product(X0,e_6,e_5)
| ~ product(X0,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_370]) ).
tcf(c_5657,plain,
( equalish(e_3,e_5)
| ~ product(e_1,e_5,e_6)
| ~ product(e_1,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_286]) ).
tcf(c_5667,plain,
( equalish(e_5,e_6)
| ~ product(e_1,e_5,e_6)
| ~ product(e_1,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_350]) ).
tcf(c_5727,plain,
! [X0: $i] :
( product(e_3,e_4,e_5)
| ~ product(e_4,X0,e_5)
| ~ product(e_3,X0,e_4) ),
inference(instantiation,[status(thm)],[c_3095]) ).
tcf(c_5728,plain,
! [X0: $i] :
( equalish(e_6,e_4)
| ~ product(e_6,X0,e_5)
| ~ product(e_4,X0,e_5) ),
inference(instantiation,[status(thm)],[c_378]) ).
tcf(c_5729,plain,
! [X0: $i] :
( equalish(e_4,e_6)
| ~ product(e_6,X0,e_5)
| ~ product(e_4,X0,e_5) ),
inference(instantiation,[status(thm)],[c_324]) ).
tcf(c_5742,plain,
( equalish(e_4,e_6)
| ~ product(e_6,e_1,e_5)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_5729]) ).
tcf(c_5743,plain,
( equalish(e_6,e_4)
| ~ product(e_6,e_1,e_5)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_5728]) ).
tcf(c_5744,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_5727]) ).
tcf(c_5746,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_425]) ).
tcf(c_5749,plain,
! [X0: $i] :
( equalish(e_5,e_2)
| ~ product(e_4,X0,e_5)
| ~ product(e_4,X0,e_2) ),
inference(instantiation,[status(thm)],[c_332]) ).
tcf(c_5753,plain,
! [X0: $i] :
( equalish(e_2,e_5)
| ~ product(e_4,X0,e_5)
| ~ product(e_4,X0,e_2) ),
inference(instantiation,[status(thm)],[c_254]) ).
tcf(c_5756,plain,
( equalish(e_2,e_5)
| ~ product(e_4,e_1,e_5)
| ~ product(e_4,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_5753]) ).
tcf(c_5760,plain,
( equalish(e_5,e_2)
| ~ product(e_4,e_1,e_5)
| ~ product(e_4,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_5749]) ).
tcf(c_5770,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_495]) ).
tcf(c_5781,plain,
! [X0: $i] :
( equalish(e_6,e_5)
| ~ product(X0,e_6,e_6)
| ~ product(X0,e_5,e_6) ),
inference(instantiation,[status(thm)],[c_382]) ).
tcf(c_5784,plain,
! [X0: $i] :
( equalish(e_5,e_3)
| ~ product(X0,e_5,e_6)
| ~ product(X0,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_340]) ).
tcf(c_5871,plain,
! [X0: $i] :
( equalish(e_6,e_5)
| ~ product(e_6,X0,e_5)
| ~ product(e_5,X0,e_5) ),
inference(instantiation,[status(thm)],[c_384]) ).
tcf(c_5874,plain,
! [X0: $i] :
( equalish(e_5,e_3)
| ~ product(e_5,X0,e_5)
| ~ product(e_3,X0,e_5) ),
inference(instantiation,[status(thm)],[c_342]) ).
tcf(c_5876,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_330]) ).
tcf(c_5877,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_318]) ).
tcf(c_5884,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_5877]) ).
tcf(c_5890,plain,
( equalish(e_6,e_5)
| ~ product(e_6,e_1,e_5)
| ~ product(e_5,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_5871]) ).
tcf(c_5929,plain,
! [X0: $i] :
( equalish(e_6,e_1)
| ~ product(X0,e_6,e_6)
| ~ product(X0,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_358]) ).
tcf(c_6573,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_210]) ).
tcf(c_6632,plain,
( equalish(e_6,e_3)
| ~ product(e_5,e_6,e_4)
| ~ product(e_5,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_370]) ).
tcf(c_6660,plain,
! [X0: $i] :
( product(X0,e_5,e_4)
| ~ product(e_5,e_3,e_4)
| ~ product(X0,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_3580]) ).
tcf(c_6661,plain,
( product(e_1,e_5,e_4)
| ~ product(e_5,e_3,e_4)
| ~ product(e_1,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_6660]) ).
tcf(c_6684,plain,
( product(e_2,e_5,e_2)
| ~ product(e_5,e_6,e_2)
| ~ product(e_2,e_6,e_5) ),
inference(instantiation,[status(thm)],[c_3586]) ).
tcf(c_6744,plain,
( equalish(e_1,e_5)
| ~ product(e_3,e_5,e_4)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_226]) ).
tcf(c_6816,plain,
( product(e_4,e_1,e_2)
| ~ product(e_4,e_6,e_1)
| ~ product(e_1,e_6,e_2) ),
inference(instantiation,[status(thm)],[c_1231]) ).
tcf(c_6840,plain,
( product(e_6,e_1,e_3)
| ~ product(e_6,e_5,e_1)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_1893]) ).
tcf(c_6864,plain,
( product(e_3,e_1,e_6)
| ~ product(e_3,e_6,e_1)
| ~ product(e_1,e_6,e_6) ),
inference(instantiation,[status(thm)],[c_4151]) ).
tcf(c_6865,plain,
( product(e_2,e_1,e_6)
| ~ product(e_2,e_6,e_1)
| ~ product(e_1,e_6,e_6) ),
inference(instantiation,[status(thm)],[c_4073]) ).
tcf(c_7001,plain,
( equalish(e_5,e_3)
| ~ product(e_5,e_5,e_3)
| ~ product(e_5,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_1873]) ).
tcf(c_7011,plain,
! [X0: $i] :
( product(X0,e_5,e_3)
| ~ product(e_5,e_5,e_3)
| ~ product(X0,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_1897]) ).
tcf(c_7012,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_7011]) ).
tcf(c_7082,plain,
( equalish(e_6,e_3)
| ~ product(e_3,e_6,e_3)
| ~ product(e_3,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_1562]) ).
tcf(c_7372,plain,
( equalish(e_4,e_1)
| ~ product(e_3,e_4,e_4)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_3297]) ).
tcf(c_7431,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_3,e_4)
| ~ product(e_2,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_3337]) ).
tcf(c_7604,plain,
( equalish(e_5,e_2)
| ~ product(e_5,e_3,e_4)
| ~ product(e_2,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_3562]) ).
tcf(c_7718,plain,
( equalish(e_5,e_1)
| ~ product(e_5,e_5,e_4)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_3563]) ).
tcf(c_7720,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_5,e_4)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_3338]) ).
tcf(c_7722,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_3084]) ).
tcf(c_7776,plain,
( equalish(e_1,e_6)
| ~ product(e_6,e_3,e_6)
| ~ product(e_1,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_234]) ).
tcf(c_7782,plain,
( equalish(e_6,e_3)
| ~ product(e_1,e_6,e_6)
| ~ product(e_1,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_370]) ).
tcf(c_7783,plain,
( equalish(e_3,e_6)
| ~ product(e_1,e_6,e_6)
| ~ product(e_1,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_292]) ).
tcf(c_7789,plain,
! [X0: $i] :
( product(e_1,e_6,X0)
| ~ product(e_1,e_3,e_6)
| ~ product(e_6,e_3,X0) ),
inference(instantiation,[status(thm)],[c_434]) ).
tcf(c_7790,plain,
( equalish(e_6,e_5)
| ~ product(e_1,e_3,e_6)
| ~ product(e_1,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_380]) ).
tcf(c_7800,plain,
( product(e_1,e_6,e_1)
| ~ product(e_6,e_3,e_1)
| ~ product(e_1,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_7789]) ).
tcf(c_7805,plain,
( product(e_4,e_1,e_6)
| ~ product(e_4,e_3,e_1)
| ~ product(e_1,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_1919]) ).
tcf(c_7806,plain,
( product(e_3,e_1,e_6)
| ~ product(e_3,e_3,e_1)
| ~ product(e_1,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_1812]) ).
tcf(c_7909,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_5770]) ).
tcf(c_7913,plain,
( product(e_1,e_6,e_4)
| ~ product(e_6,e_4,e_4)
| ~ product(e_1,e_4,e_6) ),
inference(instantiation,[status(thm)],[c_3311]) ).
tcf(c_7914,plain,
( equalish(e_6,e_4)
| ~ product(e_1,e_6,e_6)
| ~ product(e_1,e_4,e_6) ),
inference(instantiation,[status(thm)],[c_376]) ).
tcf(c_7919,plain,
( equalish(e_3,e_4)
| ~ product(e_1,e_4,e_6)
| ~ product(e_1,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_280]) ).
tcf(c_7923,plain,
! [X0: $i] :
( product(e_1,e_6,X0)
| ~ product(e_1,e_4,e_6)
| ~ product(e_6,e_4,X0) ),
inference(instantiation,[status(thm)],[c_434]) ).
tcf(c_7934,plain,
( product(e_1,e_6,e_1)
| ~ product(e_6,e_4,e_1)
| ~ product(e_1,e_4,e_6) ),
inference(instantiation,[status(thm)],[c_7923]) ).
tcf(c_7941,plain,
( product(e_3,e_1,e_6)
| ~ product(e_3,e_4,e_1)
| ~ product(e_1,e_4,e_6) ),
inference(instantiation,[status(thm)],[c_2069]) ).
tcf(c_8106,plain,
! [X0: $i] :
( product(e_4,e_5,e_6)
| ~ product(e_5,X0,e_6)
| ~ product(e_4,X0,e_5) ),
inference(instantiation,[status(thm)],[c_5746]) ).
tcf(c_8127,plain,
( product(e_4,e_5,e_6)
| ~ product(e_5,e_1,e_6)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_8106]) ).
tcf(c_8128,plain,
! [X0: $i] :
( product(e_5,e_6,e_2)
| ~ product(e_6,X0,e_2)
| ~ product(e_5,X0,e_6) ),
inference(instantiation,[status(thm)],[c_1247]) ).
tcf(c_8129,plain,
! [X0: $i,X1: $i] :
( product(e_5,e_6,X1)
| ~ product(e_5,X0,e_6)
| ~ product(e_6,X0,X1) ),
inference(instantiation,[status(thm)],[c_434]) ).
tcf(c_8151,plain,
( product(e_5,e_6,e_2)
| ~ product(e_6,e_1,e_2)
| ~ product(e_5,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_8128]) ).
tcf(c_8156,plain,
! [X0: $i,X1: $i] :
( product(X0,e_5,e_6)
| ~ product(e_5,X1,e_6)
| ~ product(X0,X1,e_5) ),
inference(instantiation,[status(thm)],[c_571]) ).
tcf(c_8162,plain,
! [X0: $i] :
( product(X0,e_3,e_4)
| ~ product(e_3,e_6,e_4)
| ~ product(X0,e_6,e_3) ),
inference(instantiation,[status(thm)],[c_3114]) ).
tcf(c_8168,plain,
( product(e_1,e_3,e_4)
| ~ product(e_3,e_6,e_4)
| ~ product(e_1,e_6,e_3) ),
inference(instantiation,[status(thm)],[c_8162]) ).
tcf(c_8431,plain,
( equalish(e_6,e_3)
| ~ product(e_6,e_4,e_5)
| ~ product(e_3,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_372]) ).
tcf(c_8438,plain,
( equalish(e_6,e_4)
| ~ product(e_3,e_6,e_5)
| ~ product(e_3,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_376]) ).
tcf(c_8441,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_304]) ).
tcf(c_8443,plain,
( equalish(e_3,e_4)
| ~ product(e_3,e_4,e_5)
| ~ product(e_3,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_280]) ).
tcf(c_8459,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_495]) ).
tcf(c_8460,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_8459]) ).
tcf(c_8600,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_396]) ).
tcf(c_8601,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_8600]) ).
tcf(c_8606,plain,
( product(e_6,e_3,e_2)
| ~ product(e_6,e_2,e_3)
| ~ product(e_3,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_667]) ).
tcf(c_8729,plain,
! [X0: $i] :
( product(e_2,e_5,X0)
| ~ product(e_2,e_5,e_5)
| ~ product(e_5,e_5,X0) ),
inference(instantiation,[status(thm)],[c_401]) ).
tcf(c_8730,plain,
( product(e_2,e_5,e_1)
| ~ product(e_5,e_5,e_1)
| ~ product(e_2,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_8729]) ).
tcf(c_8731,plain,
( product(e_2,e_5,e_3)
| ~ product(e_5,e_5,e_3)
| ~ product(e_2,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_7011]) ).
tcf(c_8819,plain,
( equalish(e_1,e_2)
| ~ product(e_2,e_6,e_6)
| ~ product(e_1,e_6,e_6) ),
inference(instantiation,[status(thm)],[c_210]) ).
tcf(c_8842,plain,
( product(e_5,e_2,e_6)
| ~ product(e_5,e_6,e_2)
| ~ product(e_2,e_6,e_6) ),
inference(instantiation,[status(thm)],[c_4721]) ).
tcf(c_8911,plain,
( equalish(e_5,e_3)
| ~ product(e_3,e_5,e_5)
| ~ product(e_3,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_3460]) ).
tcf(c_8912,plain,
( equalish(e_5,e_4)
| ~ product(e_3,e_5,e_5)
| ~ product(e_3,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_3459]) ).
tcf(c_8914,plain,
( equalish(e_6,e_5)
| ~ product(e_3,e_6,e_5)
| ~ product(e_3,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_3457]) ).
tcf(c_8946,plain,
( equalish(e_1,e_6)
| ~ product(e_3,e_6,e_4)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_8994,plain,
( equalish(e_3,e_4)
| ~ product(e_5,e_4,e_5)
| ~ product(e_5,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_280]) ).
tcf(c_9110,plain,
( equalish(e_1,e_6)
| ~ product(e_6,e_5,e_3)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_234]) ).
tcf(c_9118,plain,
( equalish(e_5,e_3)
| ~ product(e_6,e_5,e_3)
| ~ product(e_6,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_1873]) ).
tcf(c_9119,plain,
( equalish(e_5,e_4)
| ~ product(e_6,e_5,e_3)
| ~ product(e_6,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_1872]) ).
tcf(c_9151,plain,
( equalish(e_5,e_1)
| ~ product(e_5,e_6,e_4)
| ~ product(e_1,e_6,e_4) ),
inference(instantiation,[status(thm)],[c_3563]) ).
tcf(c_9505,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_1011]) ).
tcf(c_9619,plain,
! [X0: $i] :
( product(X0,e_2,e_6)
| ~ product(e_2,e_2,e_6)
| ~ product(X0,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_396]) ).
tcf(c_9620,plain,
( product(e_1,e_2,e_6)
| ~ product(e_2,e_2,e_6)
| ~ product(e_1,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_9619]) ).
tcf(c_9631,plain,
! [X0: $i] :
( product(X0,e_3,e_4)
| ~ product(e_3,e_3,e_4)
| ~ product(X0,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_3114]) ).
tcf(c_9637,plain,
( product(e_1,e_3,e_4)
| ~ product(e_3,e_3,e_4)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_9631]) ).
tcf(c_9638,plain,
! [X0: $i] :
( product(X0,e_3,e_2)
| ~ product(e_3,e_3,e_2)
| ~ product(X0,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_896]) ).
tcf(c_9645,plain,
( product(e_1,e_3,e_2)
| ~ product(e_3,e_3,e_2)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_9638]) ).
tcf(c_9766,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_3,e_3)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_1681]) ).
tcf(c_9817,plain,
! [X0: $i,X1: $i] :
( product(e_6,e_6,X1)
| ~ product(e_6,X0,e_6)
| ~ product(e_6,X0,X1) ),
inference(instantiation,[status(thm)],[c_434]) ).
tcf(c_9887,plain,
( equalish(e_1,e_3)
| ~ product(e_3,e_3,e_6)
| ~ product(e_1,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_216]) ).
tcf(c_9904,plain,
! [X0: $i] :
( product(X0,e_3,e_6)
| ~ product(e_3,e_3,e_6)
| ~ product(X0,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_1552]) ).
tcf(c_9905,plain,
( product(e_1,e_3,e_6)
| ~ product(e_3,e_3,e_6)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_9904]) ).
tcf(c_9924,plain,
( equalish(e_1,e_4)
| ~ product(e_4,e_3,e_6)
| ~ product(e_1,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_222]) ).
tcf(c_10141,plain,
( equalish(e_4,e_2)
| ~ product(e_3,e_4,e_3)
| ~ product(e_3,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_1714]) ).
tcf(c_10176,plain,
( equalish(e_3,e_2)
| ~ product(e_3,e_5,e_6)
| ~ product(e_2,e_5,e_6) ),
inference(instantiation,[status(thm)],[c_276]) ).
tcf(c_10327,plain,
! [X0: $i] :
( product(X0,e_5,e_4)
| ~ product(e_5,e_5,e_4)
| ~ product(X0,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_3438]) ).
tcf(c_10328,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_10327]) ).
tcf(c_10357,plain,
( equalish(e_5,e_2)
| ~ product(e_5,e_6,e_3)
| ~ product(e_2,e_6,e_3) ),
inference(instantiation,[status(thm)],[c_1994]) ).
tcf(c_10940,plain,
( equalish(e_5,e_1)
| ~ product(e_4,e_5,e_5)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_3462]) ).
tcf(c_11094,plain,
( equalish(e_6,e_5)
| ~ product(e_3,e_6,e_6)
| ~ product(e_3,e_5,e_6) ),
inference(instantiation,[status(thm)],[c_5781]) ).
tcf(c_11304,plain,
( equalish(e_6,e_1)
| ~ product(e_6,e_6,e_6)
| ~ product(e_6,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_5929]) ).
tcf(c_11419,plain,
( product(e_4,e_5,e_4)
| ~ product(e_5,e_6,e_4)
| ~ product(e_4,e_6,e_5) ),
inference(instantiation,[status(thm)],[c_5746]) ).
tcf(c_11544,plain,
! [X0: $i] :
( product(e_6,e_6,e_6)
| ~ product(e_6,X0,e_6) ),
inference(instantiation,[status(thm)],[c_9817]) ).
tcf(c_11545,plain,
( product(e_6,e_6,e_6)
| ~ product(e_6,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_11544]) ).
tcf(c_11822,plain,
! [X0: $i] :
( product(e_3,e_2,e_3)
| ~ product(e_3,X0,e_2)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_1000]) ).
tcf(c_11825,plain,
( product(e_3,e_2,e_3)
| ~ product(e_3,e_1,e_2)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_11822]) ).
tcf(c_11829,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_984]) ).
tcf(c_11836,plain,
( product(e_2,e_3,e_2)
| ~ product(e_3,e_1,e_2)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_11829]) ).
tcf(c_11928,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_3563]) ).
tcf(c_11930,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_3,e_4)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_3338]) ).
tcf(c_11933,plain,
( product(e_5,e_1,e_4)
| ~ product(e_5,e_3,e_1)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_1947]) ).
tcf(c_11934,plain,
( product(e_4,e_1,e_4)
| ~ product(e_4,e_3,e_1)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_1919]) ).
tcf(c_11992,plain,
! [X0: $i] :
( product(X0,e_5,e_6)
| ~ product(e_5,e_5,e_6)
| ~ product(X0,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_8156]) ).
tcf(c_11993,plain,
( product(e_1,e_5,e_6)
| ~ product(e_5,e_5,e_6)
| ~ product(e_1,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_11992]) ).
tcf(c_12189,plain,
! [X0: $i] :
( product(e_6,e_4,e_5)
| ~ product(e_6,X0,e_4)
| ~ product(e_4,X0,e_5) ),
inference(instantiation,[status(thm)],[c_5770]) ).
tcf(c_12195,plain,
! [X0: $i] :
( equalish(e_3,e_4)
| ~ product(e_6,X0,e_4)
| ~ product(e_6,X0,e_3) ),
inference(instantiation,[status(thm)],[c_278]) ).
tcf(c_12200,plain,
( equalish(e_3,e_4)
| ~ product(e_6,e_1,e_4)
| ~ product(e_6,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_12195]) ).
tcf(c_12206,plain,
( product(e_6,e_4,e_5)
| ~ product(e_6,e_1,e_4)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_12189]) ).
tcf(c_12210,plain,
! [X0: $i] :
( product(e_5,e_6,e_4)
| ~ product(e_6,X0,e_4)
| ~ product(e_5,X0,e_6) ),
inference(instantiation,[status(thm)],[c_8129]) ).
tcf(c_12217,plain,
( product(e_5,e_6,e_4)
| ~ product(e_6,e_1,e_4)
| ~ product(e_5,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_12210]) ).
tcf(c_12295,plain,
( product(e_3,e_4,e_6)
| ~ product(e_4,e_5,e_6)
| ~ product(e_3,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_3095]) ).
tcf(c_12297,plain,
( equalish(e_4,e_6)
| ~ product(e_6,e_5,e_6)
| ~ product(e_4,e_5,e_6) ),
inference(instantiation,[status(thm)],[c_324]) ).
tcf(c_12298,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_5,e_6)
| ~ product(e_3,e_5,e_6) ),
inference(instantiation,[status(thm)],[c_312]) ).
tcf(c_12300,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_5,e_6)
| ~ product(e_1,e_5,e_6) ),
inference(instantiation,[status(thm)],[c_300]) ).
tcf(c_12301,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_5,e_6)
| ~ product(e_3,e_5,e_6) ),
inference(instantiation,[status(thm)],[c_282]) ).
tcf(c_12304,plain,
( product(e_4,e_6,e_5)
| ~ product(e_6,e_5,e_5)
| ~ product(e_4,e_5,e_6) ),
inference(instantiation,[status(thm)],[c_3486]) ).
tcf(c_12328,plain,
! [X0: $i] :
( product(e_4,e_6,X0)
| ~ product(e_4,e_5,e_6)
| ~ product(e_6,e_5,X0) ),
inference(instantiation,[status(thm)],[c_421]) ).
tcf(c_12329,plain,
( product(e_4,e_6,e_1)
| ~ product(e_6,e_5,e_1)
| ~ product(e_4,e_5,e_6) ),
inference(instantiation,[status(thm)],[c_12328]) ).
tcf(c_12346,plain,
( equalish(e_5,e_3)
| ~ product(e_4,e_5,e_6)
| ~ product(e_4,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_5784]) ).
tcf(c_12352,plain,
( product(e_1,e_4,e_6)
| ~ product(e_4,e_5,e_6)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_3128]) ).
tcf(c_12518,plain,
( product(e_6,e_3,e_4)
| ~ product(e_6,e_3,e_3)
| ~ product(e_3,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_9631]) ).
tcf(c_12707,plain,
( equalish(e_5,e_1)
| ~ product(e_5,e_3,e_5)
| ~ product(e_1,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_5876]) ).
tcf(c_12708,plain,
( equalish(e_5,e_3)
| ~ product(e_5,e_3,e_5)
| ~ product(e_3,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_5874]) ).
tcf(c_12757,plain,
( equalish(e_6,e_3)
| ~ product(e_4,e_6,e_5)
| ~ product(e_4,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_5609]) ).
tcf(c_12763,plain,
( equalish(e_6,e_5)
| ~ product(e_4,e_6,e_5)
| ~ product(e_4,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_3457]) ).
tcf(c_12765,plain,
( equalish(e_6,e_1)
| ~ product(e_4,e_6,e_5)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_3608]) ).
tcf(c_12771,plain,
! [X0: $i] :
( product(e_4,e_5,X0)
| ~ product(e_4,e_6,e_5)
| ~ product(e_5,e_6,X0) ),
inference(instantiation,[status(thm)],[c_3587]) ).
tcf(c_12772,plain,
( product(e_4,e_5,e_1)
| ~ product(e_5,e_6,e_1)
| ~ product(e_4,e_6,e_5) ),
inference(instantiation,[status(thm)],[c_12771]) ).
tcf(c_12897,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_170]) ).
tcf(c_12900,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_3)
| ~ product(X0,e_3,X1)
| ~ product(X0,e_1,X1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_12901,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_171]) ).
tcf(c_12903,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_4)
| ~ product(X0,e_4,X1)
| ~ product(X0,e_1,X1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_12904,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_171]) ).
tcf(c_12906,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_170]) ).
tcf(c_12907,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_171]) ).
tcf(c_12910,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_6)
| ~ product(e_6,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_12912,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_170]) ).
tcf(c_12922,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_171]) ).
tcf(c_12927,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_170]) ).
tcf(c_12928,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_171]) ).
tcf(c_12933,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_170]) ).
tcf(c_12934,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_171]) ).
tcf(c_12937,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_171]) ).
tcf(c_12942,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_170]) ).
tcf(c_12946,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_171]) ).
tcf(c_12948,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_170]) ).
tcf(c_12949,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_171]) ).
tcf(c_12952,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_171]) ).
tcf(c_12957,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_170]) ).
tcf(c_12958,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_171]) ).
tcf(c_12967,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_171]) ).
tcf(c_12978,plain,
! [X0: $i,X1: $i] :
( equalish(e_6,e_3)
| ~ product(X0,e_6,X1)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_12979,plain,
! [X0: $i,X1: $i] :
( equalish(e_6,e_3)
| ~ product(e_6,X0,X1)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_12984,plain,
! [X0: $i,X1: $i] :
( equalish(e_6,e_5)
| ~ product(X0,e_6,X1)
| ~ product(X0,e_5,X1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_12996,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_172]) ).
tcf(c_13002,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_172]) ).
tcf(c_13004,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_172]) ).
tcf(c_13007,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_172]) ).
tcf(c_13010,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_172]) ).
tcf(c_13016,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_172]) ).
tcf(c_13019,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_172]) ).
tcf(c_13022,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X0,e_6,X2)
| ~ product(e_6,X1,X2)
| ~ product(X0,X1,e_6) ),
inference(instantiation,[status(thm)],[c_172]) ).
tcf(c_13079,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_172]) ).
tcf(c_13080,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_172]) ).
tcf(c_13156,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X0,X2,e_6)
| ~ product(X2,X1,e_6)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_172]) ).
tcf(c_13261,plain,
! [X0: $i] :
( equalish(e_2,e_1)
| ~ product(X0,e_2,e_4)
| ~ product(X0,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_12912]) ).
tcf(c_13313,plain,
! [X0: $i,X1: $i] :
( product(e_2,e_2,X1)
| ~ product(e_2,X0,e_2)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_12996]) ).
tcf(c_13357,plain,
! [X0: $i] :
( equalish(e_3,e_1)
| ~ product(X0,e_3,e_6)
| ~ product(X0,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_12927]) ).
tcf(c_13373,plain,
( equalish(e_5,e_4)
| ~ product(e_5,e_3,e_6)
| ~ product(e_4,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_12967]) ).
tcf(c_13377,plain,
( equalish(e_4,e_5)
| ~ product(e_5,e_3,e_6)
| ~ product(e_4,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_12952]) ).
tcf(c_13380,plain,
( equalish(e_1,e_5)
| ~ product(e_5,e_3,e_6)
| ~ product(e_1,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_12907]) ).
tcf(c_13414,plain,
! [X0: $i,X1: $i] :
( product(e_3,e_3,X1)
| ~ product(e_3,X0,e_3)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_13004]) ).
tcf(c_13421,plain,
! [X0: $i] :
( equalish(e_3,e_1)
| ~ product(e_3,X0,e_3)
| ~ product(e_1,X0,e_3) ),
inference(instantiation,[status(thm)],[c_12928]) ).
tcf(c_13492,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,e_2)
| ~ product(X1,e_4,e_2)
| ~ product(X0,e_4,X1) ),
inference(instantiation,[status(thm)],[c_13002]) ).
tcf(c_13501,plain,
! [X0: $i,X1: $i] :
( product(e_4,e_4,X1)
| ~ product(e_4,X0,e_4)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_13010]) ).
tcf(c_13562,plain,
( equalish(e_4,e_5)
| ~ product(e_5,e_5,e_5)
| ~ product(e_4,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_12952]) ).
tcf(c_13563,plain,
( equalish(e_3,e_5)
| ~ product(e_5,e_5,e_5)
| ~ product(e_3,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_12937]) ).
tcf(c_13564,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_12922]) ).
tcf(c_13565,plain,
( equalish(e_1,e_5)
| ~ product(e_5,e_5,e_5)
| ~ product(e_1,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_12907]) ).
tcf(c_13594,plain,
! [X0: $i] :
( equalish(e_5,e_1)
| ~ product(e_5,X0,e_6)
| ~ product(e_1,X0,e_6) ),
inference(instantiation,[status(thm)],[c_12958]) ).
tcf(c_13599,plain,
! [X0: $i,X1: $i] :
( product(e_5,e_6,X1)
| ~ product(e_5,X0,e_6)
| ~ product(e_6,X0,X1) ),
inference(instantiation,[status(thm)],[c_13022]) ).
tcf(c_13622,plain,
! [X0: $i,X1: $i] :
( product(X0,e_5,e_6)
| ~ product(e_5,X1,e_6)
| ~ product(X0,X1,e_5) ),
inference(instantiation,[status(thm)],[c_13156]) ).
tcf(c_13636,plain,
! [X0: $i] :
( equalish(e_6,e_5)
| ~ product(X0,e_6,e_5)
| ~ product(X0,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_12984]) ).
tcf(c_13638,plain,
! [X0: $i] :
( equalish(e_6,e_3)
| ~ product(X0,e_6,e_5)
| ~ product(X0,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_12978]) ).
tcf(c_13672,plain,
! [X0: $i,X1: $i] :
( product(e_6,e_5,X1)
| ~ product(e_6,X0,e_5)
| ~ product(e_5,X0,X1) ),
inference(instantiation,[status(thm)],[c_13016]) ).
tcf(c_13709,plain,
! [X0: $i,X1: $i] :
( product(X0,e_6,e_5)
| ~ product(e_6,X1,e_5)
| ~ product(X0,X1,e_6) ),
inference(instantiation,[status(thm)],[c_13080]) ).
tcf(c_13799,plain,
! [X0: $i] :
( product(e_2,e_2,e_2)
| ~ product(e_2,X0,e_2) ),
inference(instantiation,[status(thm)],[c_13313]) ).
tcf(c_13800,plain,
( product(e_2,e_2,e_2)
| ~ product(e_2,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_13799]) ).
tcf(c_13822,plain,
! [X0: $i] :
( product(e_3,e_3,e_3)
| ~ product(e_3,X0,e_3) ),
inference(instantiation,[status(thm)],[c_13414]) ).
tcf(c_13823,plain,
( product(e_3,e_3,e_3)
| ~ product(e_3,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_13822]) ).
tcf(c_13844,plain,
! [X0: $i] :
( product(e_4,e_4,e_4)
| ~ product(e_4,X0,e_4) ),
inference(instantiation,[status(thm)],[c_13501]) ).
tcf(c_13845,plain,
( product(e_4,e_4,e_4)
| ~ product(e_4,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_13844]) ).
tcf(c_13866,plain,
! [X0: $i] :
( product(e_5,e_6,e_5)
| ~ product(e_6,X0,e_5)
| ~ product(e_5,X0,e_6) ),
inference(instantiation,[status(thm)],[c_13599]) ).
tcf(c_13867,plain,
( product(e_5,e_6,e_5)
| ~ product(e_6,e_1,e_5)
| ~ product(e_5,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_13866]) ).
tcf(c_13948,plain,
! [X0: $i] :
( equalish(e_5,e_1)
| ~ product(X0,e_5,e_3)
| ~ product(X0,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_12957]) ).
tcf(c_14215,plain,
( product(e_2,e_5,e_6)
| ~ product(e_5,e_5,e_6)
| ~ product(e_2,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_13622]) ).
tcf(c_14311,plain,
( equalish(e_1,e_3)
| ~ product(e_3,e_3,e_3)
| ~ product(e_3,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_12900]) ).
tcf(c_14336,plain,
( equalish(e_1,e_3)
| ~ product(e_4,e_3,e_2)
| ~ product(e_4,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_12900]) ).
tcf(c_14407,plain,
( equalish(e_1,e_3)
| ~ product(e_6,e_3,e_4)
| ~ product(e_6,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_12900]) ).
tcf(c_14429,plain,
! [X0: $i] :
( product(X0,e_6,e_4)
| ~ product(e_6,e_3,e_4)
| ~ product(X0,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_13079]) ).
tcf(c_14430,plain,
( product(e_1,e_6,e_4)
| ~ product(e_6,e_3,e_4)
| ~ product(e_1,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_14429]) ).
tcf(c_14529,plain,
! [X0: $i] :
( product(X0,e_3,e_4)
| ~ product(e_3,e_5,e_4)
| ~ product(X0,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_13079]) ).
tcf(c_14530,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_14529]) ).
tcf(c_14555,plain,
( equalish(e_1,e_3)
| ~ product(e_3,e_6,e_6)
| ~ product(e_1,e_6,e_6) ),
inference(instantiation,[status(thm)],[c_12901]) ).
tcf(c_14581,plain,
! [X0: $i] :
( product(X0,e_3,e_6)
| ~ product(e_3,e_6,e_6)
| ~ product(X0,e_6,e_3) ),
inference(instantiation,[status(thm)],[c_13156]) ).
tcf(c_14582,plain,
( product(e_1,e_3,e_6)
| ~ product(e_3,e_6,e_6)
| ~ product(e_1,e_6,e_3) ),
inference(instantiation,[status(thm)],[c_14581]) ).
tcf(c_14623,plain,
( equalish(e_1,e_4)
| ~ product(e_4,e_4,e_4)
| ~ product(e_4,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_12903]) ).
tcf(c_14661,plain,
( product(e_6,e_5,e_4)
| ~ product(e_6,e_4,e_5)
| ~ product(e_5,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_13672]) ).
tcf(c_14696,plain,
( product(e_6,e_3,e_2)
| ~ product(e_6,e_4,e_3)
| ~ product(e_3,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_13492]) ).
tcf(c_14699,plain,
( equalish(e_4,e_1)
| ~ product(e_6,e_4,e_3)
| ~ product(e_6,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_12942]) ).
tcf(c_14706,plain,
( equalish(e_6,e_3)
| ~ product(e_6,e_4,e_3)
| ~ product(e_3,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_12979]) ).
tcf(c_14810,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_6,e_5)
| ~ product(e_3,e_6,e_5) ),
inference(instantiation,[status(thm)],[c_12949]) ).
tcf(c_14811,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_6,e_5)
| ~ product(e_2,e_6,e_5) ),
inference(instantiation,[status(thm)],[c_12946]) ).
tcf(c_14873,plain,
( equalish(e_1,e_5)
| ~ product(e_5,e_5,e_6)
| ~ product(e_5,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_12906]) ).
tcf(c_14921,plain,
( equalish(e_1,e_5)
| ~ product(e_6,e_5,e_4)
| ~ product(e_6,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_12906]) ).
tcf(c_14932,plain,
( equalish(e_1,e_6)
| ~ product(e_6,e_5,e_4)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_12910]) ).
tcf(c_14949,plain,
( equalish(e_3,e_1)
| ~ product(e_5,e_3,e_6)
| ~ product(e_5,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_13357]) ).
tcf(c_14989,plain,
( equalish(e_4,e_5)
| ~ product(e_5,e_6,e_5)
| ~ product(e_4,e_6,e_5) ),
inference(instantiation,[status(thm)],[c_12952]) ).
tcf(c_14990,plain,
( equalish(e_3,e_5)
| ~ product(e_5,e_6,e_5)
| ~ product(e_3,e_6,e_5) ),
inference(instantiation,[status(thm)],[c_12937]) ).
tcf(c_15004,plain,
! [X0: $i] :
( product(e_5,e_5,X0)
| ~ product(e_5,e_6,e_5)
| ~ product(e_5,e_6,X0) ),
inference(instantiation,[status(thm)],[c_13019]) ).
tcf(c_15161,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_5,e_3)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_13421]) ).
tcf(c_15183,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_2,e_3)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_13421]) ).
tcf(c_15184,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_172]) ).
tcf(c_15185,plain,
( product(e_1,e_1,e_1)
| ~ product(e_1,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_15184]) ).
tcf(c_15254,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_13007]) ).
tcf(c_15255,plain,
( product(e_3,e_1,e_2)
| ~ product(e_3,e_1,e_1)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_15254]) ).
tcf(c_15299,plain,
( product(e_4,e_6,e_2)
| ~ product(e_6,e_5,e_2)
| ~ product(e_4,e_5,e_6) ),
inference(instantiation,[status(thm)],[c_13002]) ).
tcf(c_15417,plain,
( product(e_3,e_2,e_4)
| ~ product(e_3,e_6,e_2)
| ~ product(e_2,e_6,e_4) ),
inference(instantiation,[status(thm)],[c_13007]) ).
tcf(c_15453,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_3,e_5)
| ~ product(e_3,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_12934]) ).
tcf(c_15455,plain,
( equalish(e_1,e_4)
| ~ product(e_4,e_3,e_5)
| ~ product(e_1,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_12904]) ).
tcf(c_15545,plain,
( product(e_3,e_6,e_5)
| ~ product(e_6,e_4,e_5)
| ~ product(e_3,e_4,e_6) ),
inference(instantiation,[status(thm)],[c_13709]) ).
tcf(c_15558,plain,
! [X0: $i] :
( product(X0,e_3,e_6)
| ~ product(e_3,e_4,e_6)
| ~ product(X0,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_13156]) ).
tcf(c_15559,plain,
( product(e_1,e_3,e_6)
| ~ product(e_3,e_4,e_6)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_15558]) ).
tcf(c_15632,plain,
( equalish(e_1,e_4)
| ~ product(e_5,e_4,e_6)
| ~ product(e_5,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_12903]) ).
tcf(c_15659,plain,
( product(e_6,e_5,e_2)
| ~ product(e_6,e_4,e_5)
| ~ product(e_5,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_13492]) ).
tcf(c_15660,plain,
( equalish(e_4,e_3)
| ~ product(e_6,e_4,e_5)
| ~ product(e_6,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_12948]) ).
tcf(c_15689,plain,
( equalish(e_1,e_3)
| ~ product(e_4,e_3,e_5)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_12900]) ).
tcf(c_15822,plain,
( product(e_3,e_5,e_4)
| ~ product(e_5,e_6,e_4)
| ~ product(e_3,e_6,e_5) ),
inference(instantiation,[status(thm)],[c_13007]) ).
tcf(c_15843,plain,
( equalish(e_6,e_5)
| ~ product(e_5,e_6,e_4)
| ~ product(e_5,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_12984]) ).
tcf(c_15854,plain,
! [X0: $i] :
( product(X0,e_5,e_4)
| ~ product(e_5,e_6,e_4)
| ~ product(X0,e_6,e_5) ),
inference(instantiation,[status(thm)],[c_13079]) ).
tcf(c_15855,plain,
( product(e_1,e_5,e_4)
| ~ product(e_5,e_6,e_4)
| ~ product(e_1,e_6,e_5) ),
inference(instantiation,[status(thm)],[c_15854]) ).
tcf(c_16045,plain,
( equalish(e_6,e_5)
| ~ product(e_5,e_6,e_5)
| ~ product(e_5,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_13636]) ).
tcf(c_16178,plain,
! [X0: $i] :
( product(X0,e_6,e_5)
| ~ product(e_6,e_4,e_5)
| ~ product(X0,e_4,e_6) ),
inference(instantiation,[status(thm)],[c_13709]) ).
tcf(c_16190,plain,
( product(e_1,e_6,e_5)
| ~ product(e_6,e_4,e_5)
| ~ product(e_1,e_4,e_6) ),
inference(instantiation,[status(thm)],[c_16178]) ).
tcf(c_16345,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_13002]) ).
tcf(c_16346,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_16345]) ).
tcf(c_16441,plain,
( equalish(e_1,e_3)
| ~ product(e_3,e_4,e_6)
| ~ product(e_1,e_4,e_6) ),
inference(instantiation,[status(thm)],[c_12901]) ).
tcf(c_16795,plain,
( equalish(e_1,e_6)
| ~ product(e_6,e_4,e_6)
| ~ product(e_1,e_4,e_6) ),
inference(instantiation,[status(thm)],[c_12910]) ).
tcf(c_16921,plain,
! [X0: $i] :
( equalish(e_3,e_4)
| ~ product(X0,e_4,e_5)
| ~ product(X0,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_12933]) ).
tcf(c_16926,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_16921]) ).
tcf(c_17209,plain,
( equalish(e_1,e_2)
| ~ product(e_2,e_2,e_2)
| ~ product(e_2,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_12897]) ).
tcf(c_17265,plain,
( product(e_5,e_5,e_5)
| ~ product(e_5,e_6,e_5) ),
inference(instantiation,[status(thm)],[c_15004]) ).
tcf(c_17339,plain,
( equalish(e_5,e_1)
| ~ product(e_5,e_6,e_6)
| ~ product(e_1,e_6,e_6) ),
inference(instantiation,[status(thm)],[c_13594]) ).
tcf(c_17447,plain,
( equalish(e_1,e_2)
| ~ product(e_5,e_2,e_6)
| ~ product(e_5,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_12897]) ).
tcf(c_17603,plain,
! [X0: $i] :
( product(e_3,e_5,X0)
| ~ product(e_3,e_3,e_5)
| ~ product(e_5,e_3,X0) ),
inference(instantiation,[status(thm)],[c_13016]) ).
tcf(c_17612,plain,
( product(e_3,e_5,e_1)
| ~ product(e_5,e_3,e_1)
| ~ product(e_3,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_17603]) ).
tcf(c_17614,plain,
( equalish(e_6,e_3)
| ~ product(e_3,e_6,e_5)
| ~ product(e_3,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_13638]) ).
tcf(c_17619,plain,
! [X0: $i] :
( product(X0,e_3,e_5)
| ~ product(e_3,e_3,e_5)
| ~ product(X0,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_13080]) ).
tcf(c_17620,plain,
( product(e_1,e_3,e_5)
| ~ product(e_3,e_3,e_5)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_17619]) ).
tcf(c_17722,plain,
( equalish(e_2,e_1)
| ~ product(e_3,e_2,e_4)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_13261]) ).
tcf(c_17758,plain,
( product(e_3,e_3,e_3)
| ~ product(e_3,e_6,e_3) ),
inference(instantiation,[status(thm)],[c_13822]) ).
tcf(c_18695,plain,
( equalish(e_5,e_1)
| ~ product(e_4,e_5,e_3)
| ~ product(e_4,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_13948]) ).
tcf(c_19710,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_18695,c_17758,c_17722,c_17620,c_17614,c_17612,c_17447,c_17339,c_17265,c_17209,c_16926,c_16795,c_16441,c_16346,c_16190,c_16045,c_15855,c_15843,c_15822,c_15689,c_15659,c_15660,c_15632,c_15559,c_15545,c_15453,c_15455,c_15417,c_15299,c_15255,c_15185,c_15183,c_15161,c_14989,c_14990,c_14949,c_14932,c_14921,c_14873,c_14810,c_14811,c_14706,c_14696,c_14699,c_14661,c_14623,c_14582,c_14555,c_14530,c_14430,c_14407,c_14336,c_14311,c_14215,c_13867,c_13845,c_13823,c_13800,c_13562,c_13563,c_13564,c_13565,c_13373,c_13377,c_13380,c_12757,c_12763,c_12765,c_12772,c_12707,c_12708,c_12518,c_12352,c_12346,c_12329,c_12304,c_12295,c_12297,c_12298,c_12300,c_12301,c_12217,c_12206,c_12200,c_11993,c_11933,c_11934,c_11928,c_11930,c_11836,c_11825,c_11545,c_11419,c_11304,c_11094,c_10940,c_10357,c_10328,c_10176,c_10141,c_9924,c_9905,c_9887,c_9766,c_9645,c_9637,c_9620,c_9505,c_9151,c_9118,c_9119,c_9110,c_8994,c_8946,c_8911,c_8912,c_8914,c_8842,c_8819,c_8731,c_8730,c_8606,c_8601,c_8460,c_8438,c_8441,c_8443,c_8431,c_8168,c_8151,c_8127,c_7941,c_7934,c_7913,c_7914,c_7919,c_7909,c_7805,c_7806,c_7800,c_7790,c_7782,c_7783,c_7776,c_7718,c_7720,c_7722,c_7604,c_7431,c_7372,c_7082,c_7012,c_7001,c_6864,c_6865,c_6840,c_6816,c_6744,c_6684,c_6661,c_6632,c_6573,c_5890,c_5884,c_5760,c_5756,c_5744,c_5743,c_5742,c_5667,c_5657,c_5570,c_5546,c_5530,c_5525,c_5508,c_5510,c_5511,c_5505,c_5464,c_5356,c_5349,c_5309,c_5304,c_5196,c_5142,c_5141,c_5033,c_5016,c_5018,c_4835,c_4714,c_4715,c_4716,c_4722,c_4030,c_4001,c_3854,c_3693,c_3577,c_3570,c_3456,c_3455,c_3454,c_3453,c_3452,c_3390,c_3344,c_3237,c_3208,c_3176,c_3150,c_3151,c_3152,c_3137,c_3138,c_3139,c_3140,c_3127,c_3135,c_3129,c_3130,c_3131,c_3109,c_3108,c_3093,c_3092,c_3091,c_2879,c_2877,c_2843,c_2841,c_2710,c_2698,c_2704,c_2565,c_2547,c_2500,c_2497,c_2224,c_2131,c_2083,c_2009,c_2003,c_2001,c_1910,c_1904,c_1889,c_1883,c_1848,c_1843,c_1726,c_1723,c_1605,c_1573,c_1561,c_1460,c_1380,c_1210,c_1209,c_1203,c_1202,c_1200,c_1174,c_1173,c_1163,c_1169,c_1162,c_1161,c_1152,c_1131,c_1129,c_1119,c_1117,c_1116,c_1114,c_1113,c_1111,c_1087,c_1076,c_1059,c_1041,c_1040,c_1039,c_1029,c_1028,c_1020,c_1019,c_1018,c_1016,c_1014,c_1001,c_999,c_997,c_982,c_947,c_900,c_845,c_836,c_834,c_827,c_820,c_816,c_814,c_796,c_801,c_793,c_780,c_773,c_730,c_725,c_674,c_671,c_668,c_442,c_438,c_433,c_429,c_424,c_420,c_415,c_411,c_404,c_400,c_397,c_395,c_394,c_393,c_392,c_391,c_390,c_335,c_329,c_319,c_271,c_265,c_263,c_259,c_253,c_251,c_241,c_235,c_233,c_229,c_227,c_223,c_221,c_215,c_211,c_209,c_193,c_191,c_189,c_187,c_175,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_158,c_159,c_160,c_161,c_162,c_163,c_164,c_165,c_166,c_167,c_111,c_112,c_113,c_114,c_121,c_122,c_123,c_124,c_125,c_126,c_127,c_128,c_129,c_130,c_132,c_133,c_134,c_135,c_136,c_137]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP128-2.006 : 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/5.38 % Computer : n015.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Wed Sep 23 13:47:14 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/5.42 Running EPR theorem proving
% 0.14/5.42 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.14/5.43
% 0.14/5.43 % ======== iProver multi-core TPTP/SMT =========
% 0.14/5.43
% 0.14/5.43 % Detected problem language: tptp
% 0.14/5.44 % Proving...
% 7.42/6.73 % SZS status Started for theBenchmark.p
% 7.42/6.73 % SZS status Unsatisfiable for theBenchmark.p
% 7.42/6.73
% 7.42/6.73 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 7.42/6.73
% 7.42/6.73 % ------ iProver source info
% 7.42/6.73
% 7.42/6.73 % git: date: 2026-07-19 20:42:38 +0200
% 7.42/6.73 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 7.42/6.73 % git: non_committed_changes: false
% 7.42/6.73
% 7.42/6.73 % ------ Parsing...% successful
% 7.42/6.73
% 7.42/6.73
% 7.42/6.73 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 7.42/6.73 % ------ Proving...
% 7.42/6.73 % ------ Problem Properties
% 7.42/6.73
% 7.42/6.73 %
% 7.42/6.73 % clauses 62
% 7.42/6.73 % conjectures 1
% 7.42/6.73 % EPR 62
% 7.42/6.73 % Horn 61
% 7.42/6.73 % unary 56
% 7.42/6.73 % binary 0
% 7.42/6.73 % lits 79
% 7.42/6.73 % lits eq 0
% 7.42/6.73 % fd_pure 0
% 7.42/6.73 % fd_pseudo 0
% 7.42/6.73 % fd_cond 0
% 7.42/6.73 % fd_pseudo_cond 0
% 7.42/6.73 % AC symbols 0
% 7.42/6.73
% 7.42/6.73 % ------ Input Options Time Limit: Unbounded
% 7.42/6.73
% 7.42/6.73
% 7.42/6.73 % ------
% 7.42/6.73 % Current options:
% 7.42/6.73 % ------
% 7.42/6.73
% 7.42/6.73
% 7.42/6.73 %
% 7.42/6.73
% 7.42/6.73 % ------ Proving...
% 7.42/6.73 %
% 7.42/6.73
% 7.42/6.73 % SZS status Unsatisfiable for theBenchmark.p
% 7.42/6.73
% 7.42/6.73 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 7.42/6.75
% 7.42/6.75
%------------------------------------------------------------------------------