%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP127-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:14 PM UTC 2026
% Result : Unsatisfiable 5.29s 11.75s
% Output : CNFRefutation 5.29s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
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(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,axiom,
! [X0] : product(X0,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_idempotence) ).
fof(f63,negated_conjecture,
! [X2,X3,X0,X1] :
( product(X3,X0,X1)
| ~ product(X2,X0,X3)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg3) ).
tcf(c_113,plain,
next(e_2,e_3),
inference(cnf_transformation,[],[f2]) ).
tcf(c_114,plain,
next(e_3,e_4),
inference(cnf_transformation,[],[f3]) ).
tcf(c_115,plain,
next(e_4,e_5),
inference(cnf_transformation,[],[f4]) ).
tcf(c_126,plain,
greater(e_4,e_3),
inference(cnf_transformation,[],[f15]) ).
tcf(c_127,plain,
greater(e_5,e_3),
inference(cnf_transformation,[],[f16]) ).
tcf(c_128,plain,
greater(e_6,e_3),
inference(cnf_transformation,[],[f17]) ).
tcf(c_129,plain,
greater(e_5,e_4),
inference(cnf_transformation,[],[f18]) ).
tcf(c_130,plain,
greater(e_6,e_4),
inference(cnf_transformation,[],[f19]) ).
tcf(c_131,plain,
greater(e_6,e_5),
inference(cnf_transformation,[],[f20]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ greater(X1,X2)
| ~ next(X0,X2)
| ~ product(X0,e_1,X1) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_133,plain,
group_element(e_1),
inference(cnf_transformation,[],[f22]) ).
tcf(c_134,plain,
group_element(e_2),
inference(cnf_transformation,[],[f23]) ).
tcf(c_135,plain,
group_element(e_3),
inference(cnf_transformation,[],[f24]) ).
tcf(c_136,plain,
group_element(e_4),
inference(cnf_transformation,[],[f25]) ).
tcf(c_137,plain,
group_element(e_5),
inference(cnf_transformation,[],[f26]) ).
tcf(c_138,plain,
group_element(e_6),
inference(cnf_transformation,[],[f27]) ).
tcf(c_139,plain,
~ equalish(e_1,e_2),
inference(cnf_transformation,[],[f28]) ).
tcf(c_140,plain,
~ equalish(e_1,e_3),
inference(cnf_transformation,[],[f29]) ).
tcf(c_141,plain,
~ equalish(e_1,e_4),
inference(cnf_transformation,[],[f30]) ).
tcf(c_142,plain,
~ equalish(e_1,e_5),
inference(cnf_transformation,[],[f31]) ).
tcf(c_143,plain,
~ equalish(e_1,e_6),
inference(cnf_transformation,[],[f32]) ).
tcf(c_144,plain,
~ equalish(e_2,e_1),
inference(cnf_transformation,[],[f33]) ).
tcf(c_145,plain,
~ equalish(e_2,e_3),
inference(cnf_transformation,[],[f34]) ).
tcf(c_146,plain,
~ equalish(e_2,e_4),
inference(cnf_transformation,[],[f35]) ).
tcf(c_147,plain,
~ equalish(e_2,e_5),
inference(cnf_transformation,[],[f36]) ).
tcf(c_148,plain,
~ equalish(e_2,e_6),
inference(cnf_transformation,[],[f37]) ).
tcf(c_149,plain,
~ equalish(e_3,e_1),
inference(cnf_transformation,[],[f38]) ).
tcf(c_150,plain,
~ equalish(e_3,e_2),
inference(cnf_transformation,[],[f39]) ).
tcf(c_151,plain,
~ equalish(e_3,e_4),
inference(cnf_transformation,[],[f40]) ).
tcf(c_152,plain,
~ equalish(e_3,e_5),
inference(cnf_transformation,[],[f41]) ).
tcf(c_153,plain,
~ equalish(e_3,e_6),
inference(cnf_transformation,[],[f42]) ).
tcf(c_154,plain,
~ equalish(e_4,e_1),
inference(cnf_transformation,[],[f43]) ).
tcf(c_155,plain,
~ equalish(e_4,e_2),
inference(cnf_transformation,[],[f44]) ).
tcf(c_156,plain,
~ equalish(e_4,e_3),
inference(cnf_transformation,[],[f45]) ).
tcf(c_157,plain,
~ equalish(e_4,e_5),
inference(cnf_transformation,[],[f46]) ).
tcf(c_158,plain,
~ equalish(e_4,e_6),
inference(cnf_transformation,[],[f47]) ).
tcf(c_159,plain,
~ equalish(e_5,e_1),
inference(cnf_transformation,[],[f48]) ).
tcf(c_160,plain,
~ equalish(e_5,e_2),
inference(cnf_transformation,[],[f49]) ).
tcf(c_161,plain,
~ equalish(e_5,e_3),
inference(cnf_transformation,[],[f50]) ).
tcf(c_162,plain,
~ equalish(e_5,e_4),
inference(cnf_transformation,[],[f51]) ).
tcf(c_163,plain,
~ equalish(e_5,e_6),
inference(cnf_transformation,[],[f52]) ).
tcf(c_164,plain,
~ equalish(e_6,e_1),
inference(cnf_transformation,[],[f53]) ).
tcf(c_165,plain,
~ equalish(e_6,e_2),
inference(cnf_transformation,[],[f54]) ).
tcf(c_166,plain,
~ equalish(e_6,e_3),
inference(cnf_transformation,[],[f55]) ).
tcf(c_167,plain,
~ equalish(e_6,e_4),
inference(cnf_transformation,[],[f56]) ).
tcf(c_168,plain,
~ equalish(e_6,e_5),
inference(cnf_transformation,[],[f57]) ).
tcf(c_169,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_170,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_171,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_172,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_173,plain,
! [X0: $i] : product(X0,X0,X0),
inference(cnf_transformation,[],[f62]) ).
tcf(c_174,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( product(X3,X0,X1)
| ~ product(X2,X0,X3)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_175,plain,
product(e_1,e_1,e_1),
inference(instantiation,[status(thm)],[c_173]) ).
tcf(c_346,plain,
! [X0: $i] :
( ~ greater(X0,e_3)
| ~ product(e_2,e_1,X0) ),
inference(resolution,[status(thm)],[c_113,c_132]) ).
tcf(c_354,plain,
! [X0: $i] :
( ~ greater(X0,e_4)
| ~ product(e_3,e_1,X0) ),
inference(resolution,[status(thm)],[c_114,c_132]) ).
tcf(c_362,plain,
! [X0: $i] :
( ~ greater(X0,e_5)
| ~ product(e_4,e_1,X0) ),
inference(resolution,[status(thm)],[c_115,c_132]) ).
tcf(c_404,plain,
~ product(e_2,e_1,e_4),
inference(resolution,[status(thm)],[c_126,c_346]) ).
tcf(c_408,plain,
~ product(e_2,e_1,e_5),
inference(resolution,[status(thm)],[c_127,c_346]) ).
tcf(c_412,plain,
~ product(e_2,e_1,e_6),
inference(resolution,[status(thm)],[c_128,c_346]) ).
tcf(c_416,plain,
~ product(e_3,e_1,e_5),
inference(resolution,[status(thm)],[c_129,c_354]) ).
tcf(c_420,plain,
~ product(e_3,e_1,e_6),
inference(resolution,[status(thm)],[c_130,c_354]) ).
tcf(c_424,plain,
~ product(e_4,e_1,e_6),
inference(resolution,[status(thm)],[c_131,c_362]) ).
tcf(c_446,plain,
! [X0: $i,X1: $i] :
( ~ product(X0,e_2,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[status(thm)],[c_139,c_171]) ).
tcf(c_447,plain,
( ~ product(e_1,e_2,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_446]) ).
tcf(c_454,plain,
! [X0: $i,X1: $i] :
( ~ product(e_2,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[status(thm)],[c_139,c_172]) ).
tcf(c_455,plain,
( ~ product(e_2,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_454]) ).
tcf(c_469,plain,
! [X0: $i,X1: $i] :
( ~ product(X0,e_3,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[status(thm)],[c_140,c_171]) ).
tcf(c_470,plain,
( ~ product(e_1,e_3,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_477,plain,
! [X0: $i,X1: $i] :
( ~ product(e_3,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[status(thm)],[c_140,c_172]) ).
tcf(c_478,plain,
( ~ product(e_3,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_477]) ).
tcf(c_492,plain,
! [X0: $i,X1: $i] :
( ~ product(X0,e_4,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[status(thm)],[c_141,c_171]) ).
tcf(c_493,plain,
( ~ product(e_1,e_4,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_492]) ).
tcf(c_500,plain,
! [X0: $i,X1: $i] :
( ~ product(e_4,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[status(thm)],[c_141,c_172]) ).
tcf(c_501,plain,
( ~ product(e_4,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_500]) ).
tcf(c_515,plain,
! [X0: $i,X1: $i] :
( ~ product(X0,e_5,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[status(thm)],[c_142,c_171]) ).
tcf(c_516,plain,
( ~ product(e_1,e_5,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_515]) ).
tcf(c_523,plain,
! [X0: $i,X1: $i] :
( ~ product(e_5,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[status(thm)],[c_142,c_172]) ).
tcf(c_524,plain,
( ~ product(e_5,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_523]) ).
tcf(c_538,plain,
! [X0: $i,X1: $i] :
( ~ product(X0,e_6,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[status(thm)],[c_143,c_171]) ).
tcf(c_539,plain,
( ~ product(e_1,e_6,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_538]) ).
tcf(c_546,plain,
! [X0: $i,X1: $i] :
( ~ product(e_6,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[status(thm)],[c_143,c_172]) ).
tcf(c_547,plain,
( ~ product(e_6,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_546]) ).
tcf(c_1511,plain,
! [X0: $i] :
( product(e_2,e_1,e_4)
| ~ product(e_1,e_4,X0)
| ~ product(X0,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1513,plain,
! [X0: $i] :
( product(e_2,e_1,e_5)
| ~ product(e_1,e_5,X0)
| ~ product(X0,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1515,plain,
! [X0: $i] :
( product(e_2,e_1,e_6)
| ~ product(e_1,e_6,X0)
| ~ product(X0,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1517,plain,
! [X0: $i] :
( product(e_3,e_1,e_5)
| ~ product(e_1,e_5,X0)
| ~ product(X0,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1518,plain,
! [X0: $i] :
( product(e_3,e_1,e_6)
| ~ product(e_1,e_6,X0)
| ~ product(X0,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1519,plain,
! [X0: $i] :
( product(e_4,e_1,e_6)
| ~ product(e_1,e_6,X0)
| ~ product(X0,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1520,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_2)
| ~ product(X0,X1,e_2)
| ~ product(X0,X1,e_1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_1521,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_171]) ).
tcf(c_1522,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_172]) ).
tcf(c_1523,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_3)
| ~ product(X0,X1,e_3)
| ~ product(X0,X1,e_1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_1524,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_171]) ).
tcf(c_1525,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_172]) ).
tcf(c_1527,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_171]) ).
tcf(c_1528,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_172]) ).
tcf(c_1530,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_171]) ).
tcf(c_1531,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_172]) ).
tcf(c_1533,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_171]) ).
tcf(c_1534,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_172]) ).
tcf(c_1536,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_171]) ).
tcf(c_1539,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_3)
| ~ product(X0,e_3,X1)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_1543,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_172]) ).
tcf(c_1545,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_5)
| ~ product(X0,e_5,X1)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_1546,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_172]) ).
tcf(c_1548,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_171]) ).
tcf(c_1549,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_172]) ).
tcf(c_1550,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_1)
| ~ product(X0,X1,e_3)
| ~ product(X0,X1,e_1) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_1551,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_171]) ).
tcf(c_1553,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_2)
| ~ product(X0,X1,e_3)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_1557,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_171]) ).
tcf(c_1558,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_172]) ).
tcf(c_1560,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_171]) ).
tcf(c_1561,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_172]) ).
tcf(c_1563,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_171]) ).
tcf(c_1564,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_172]) ).
tcf(c_1566,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_171]) ).
tcf(c_1568,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_170]) ).
tcf(c_1570,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_172]) ).
tcf(c_1573,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_172]) ).
tcf(c_1575,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_171]) ).
tcf(c_1576,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_172]) ).
tcf(c_1578,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_6)
| ~ product(X0,e_6,X1)
| ~ product(X0,e_4,X1) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_1579,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_172]) ).
tcf(c_1581,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_171]) ).
tcf(c_1582,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_172]) ).
tcf(c_1583,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,X0)
| ~ product(X0,X0,X1) ),
inference(superposition,[status(thm)],[c_173,c_174]) ).
tcf(c_1584,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_170]) ).
tcf(c_1585,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_171]) ).
tcf(c_1589,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_171]) ).
tcf(c_1590,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_172]) ).
tcf(c_1591,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_170]) ).
tcf(c_1592,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_171]) ).
tcf(c_1593,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_172]) ).
tcf(c_1595,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_171]) ).
tcf(c_1596,plain,
! [X0: $i,X1: $i] :
( equalish(e_5,e_6)
| ~ product(e_6,X0,X1)
| ~ product(e_5,X0,X1) ),
inference(instantiation,[status(thm)],[c_172]) ).
tcf(c_1598,plain,
! [X0: $i,X1: $i] :
( product(X0,X0,X1)
| ~ product(X0,X1,X0) ),
inference(resolution,[status(thm)],[c_174,c_173]) ).
tcf(c_1602,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_171]) ).
tcf(c_1604,plain,
! [X0: $i,X1: $i] :
( equalish(X0,X1)
| ~ product(X0,X1,X1) ),
inference(resolution,[status(thm)],[c_172,c_173]) ).
tcf(c_1605,plain,
! [X0: $i,X1: $i] :
( equalish(e_6,e_2)
| ~ product(X0,X1,e_6)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_1606,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_171]) ).
tcf(c_1607,plain,
! [X0: $i,X1: $i] :
( equalish(e_6,e_2)
| ~ product(e_6,X0,X1)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_172]) ).
tcf(c_1610,plain,
! [X0: $i,X1: $i] :
( equalish(e_6,e_3)
| ~ product(X0,X1,e_6)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_1611,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_171]) ).
tcf(c_1612,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_172]) ).
tcf(c_1613,plain,
! [X0: $i,X1: $i] :
( equalish(X1,X0)
| ~ product(X0,X1,X0) ),
inference(resolution,[status(thm)],[c_171,c_173]) ).
tcf(c_1614,plain,
! [X0: $i,X1: $i] :
( equalish(e_6,e_4)
| ~ product(X0,X1,e_6)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_1615,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_171]) ).
tcf(c_1616,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_172]) ).
tcf(c_1618,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_171]) ).
tcf(c_1619,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_172]) ).
tcf(c_1626,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X0,X2,e_5)
| product(X0,X2,e_4)
| product(X0,X2,e_3)
| product(X0,X2,e_2)
| product(X0,X2,e_1)
| product(X1,X0,X2)
| ~ group_element(X2)
| ~ group_element(X0)
| ~ product(e_6,X0,X1) ),
inference(superposition,[status(thm)],[c_169,c_174]) ).
tcf(c_1627,plain,
! [X0: $i] :
( product(e_6,X0,X0)
| product(X0,X0,e_5)
| product(X0,X0,e_4)
| product(X0,X0,e_3)
| product(X0,X0,e_2)
| product(X0,X0,e_1)
| ~ group_element(X0) ),
inference(superposition,[status(thm)],[c_169,c_1583]) ).
tcf(c_1629,plain,
( equalish(e_1,e_2)
| ~ product(e_2,e_2,e_2)
| ~ product(e_2,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_1520]) ).
tcf(c_1630,plain,
product(e_2,e_2,e_2),
inference(instantiation,[status(thm)],[c_173]) ).
tcf(c_1631,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X1,e_2)
| ~ product(X1,e_2,X0)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1635,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X1,e_2,X2)
| ~ product(e_2,X2,X0)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1637,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_169]) ).
tcf(c_1638,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_1637]) ).
tcf(c_1643,plain,
! [X0: $i,X1: $i] :
( product(e_1,e_4,X0)
| ~ product(X1,e_4,e_1)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1645,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_169]) ).
tcf(c_1646,plain,
! [X0: $i] :
( product(e_6,e_6,X0)
| 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(superposition,[status(thm)],[c_173,c_1626]) ).
tcf(c_1648,plain,
( product(e_6,e_6,e_1)
| 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_1646]) ).
tcf(c_1649,plain,
! [X0: $i,X1: $i] :
( product(e_1,e_5,X0)
| ~ product(X1,e_5,e_1)
| ~ product(e_5,X0,X1) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1651,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_169]) ).
tcf(c_1652,plain,
! [X0: $i,X1: $i] :
( product(e_1,e_6,X0)
| ~ product(X1,e_6,e_1)
| ~ product(e_6,X0,X1) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1654,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_169]) ).
tcf(c_1660,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(X0) ),
inference(resolution,[status(thm)],[c_169,c_138]) ).
tcf(c_1661,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_1) ),
inference(instantiation,[status(thm)],[c_1660]) ).
tcf(c_1662,plain,
! [X0: $i,X1: $i] :
( product(X1,e_1,e_4)
| ~ product(e_1,e_4,X0)
| ~ product(X0,e_1,X1) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1665,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_2,X0,X1)
| ~ product(X2,X0,e_2)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1667,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_169]) ).
tcf(c_1668,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_1667]) ).
tcf(c_1674,plain,
( product(e_6,e_6,e_6)
| product(e_6,e_6,e_5)
| product(e_6,e_6,e_4)
| product(e_6,e_6,e_3)
| product(e_6,e_6,e_2)
| product(e_6,e_6,e_1)
| ~ group_element(e_6) ),
inference(superposition,[status(thm)],[c_1627,c_1583]) ).
tcf(c_1682,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_1524]) ).
tcf(c_1683,plain,
product(e_3,e_3,e_3),
inference(instantiation,[status(thm)],[c_173]) ).
tcf(c_1684,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X1,e_3,X2)
| ~ product(e_3,X2,X0)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1686,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_169]) ).
tcf(c_1689,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_3,X0,X1)
| ~ product(X2,X0,e_3)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1693,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_1527]) ).
tcf(c_1694,plain,
product(e_4,e_4,e_4),
inference(instantiation,[status(thm)],[c_173]) ).
tcf(c_1700,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_4,X0,X1)
| ~ product(X2,X0,e_4)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1705,plain,
( equalish(e_1,e_5)
| ~ product(e_5,e_5,e_5)
| ~ product(e_5,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_1530]) ).
tcf(c_1706,plain,
product(e_5,e_5,e_5),
inference(instantiation,[status(thm)],[c_173]) ).
tcf(c_1707,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X1,e_5,X2)
| ~ product(e_5,X2,X0)
| ~ product(X0,e_5,X1) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1723,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_5,X0,X1)
| ~ product(X2,X0,e_5)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1725,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_169]) ).
tcf(c_1726,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_1725]) ).
tcf(c_1727,plain,
( equalish(e_1,e_6)
| ~ product(e_6,e_6,e_6)
| ~ product(e_6,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_1533]) ).
tcf(c_1728,plain,
product(e_6,e_6,e_6),
inference(instantiation,[status(thm)],[c_173]) ).
tcf(c_1729,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X1,e_6,X2)
| ~ product(e_6,X2,X0)
| ~ product(X0,e_6,X1) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1742,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_6,X0,X1)
| ~ product(X2,X0,e_6)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1782,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X1,e_3)
| ~ product(X1,e_3,X0)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1785,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X1,e_4)
| ~ product(X1,e_4,X0)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1911,plain,
product(e_6,e_6,e_6),
inference(global_subsumption_just,[status(thm)],[c_1674,c_1728]) ).
tcf(c_1913,plain,
! [X0: $i] :
( equalish(X0,e_6)
| ~ product(e_6,e_6,X0) ),
inference(superposition,[status(thm)],[c_1911,c_170]) ).
tcf(c_1914,plain,
! [X0: $i] :
( equalish(e_6,X0)
| ~ product(X0,e_6,e_6) ),
inference(superposition,[status(thm)],[c_1911,c_172]) ).
tcf(c_1921,plain,
( equalish(e_6,e_1)
| ~ product(e_1,e_6,e_6) ),
inference(instantiation,[status(thm)],[c_1914]) ).
tcf(c_1922,plain,
( equalish(e_1,e_6)
| ~ product(e_6,e_6,e_1) ),
inference(instantiation,[status(thm)],[c_1913]) ).
tcf(c_1943,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X1,e_5)
| ~ product(X1,e_5,X0)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_1955,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X1,e_6)
| ~ product(X1,e_6,X0)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_174]) ).
tcf(c_2210,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_1521]) ).
tcf(c_2212,plain,
( equalish(e_1,e_2)
| ~ product(e_2,e_2,e_2)
| ~ product(e_1,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_1522]) ).
tcf(c_2226,plain,
( equalish(e_1,e_3)
| ~ product(e_3,e_3,e_3)
| ~ product(e_3,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_1523]) ).
tcf(c_2229,plain,
( equalish(e_2,e_3)
| ~ product(e_3,e_3,e_3)
| ~ product(e_3,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_1539]) ).
tcf(c_2253,plain,
( product(e_3,e_1,e_5)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_1)
| ~ group_element(e_3)
| ~ group_element(e_1) ),
inference(superposition,[status(thm)],[c_169,c_420]) ).
tcf(c_2357,plain,
! [X0: $i] :
( product(X0,e_1,e_4)
| ~ product(e_1,e_4,e_2)
| ~ product(e_2,e_1,X0) ),
inference(instantiation,[status(thm)],[c_1662]) ).
tcf(c_2418,plain,
( product(e_6,e_5,e_6)
| product(e_6,e_5,e_5)
| product(e_6,e_5,e_4)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1) ),
inference(resolution,[status(thm)],[c_137,c_1660]) ).
tcf(c_2419,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(X0) ),
inference(resolution,[status(thm)],[c_137,c_169]) ).
tcf(c_2420,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_1) ),
inference(instantiation,[status(thm)],[c_2419]) ).
tcf(c_2422,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) ),
inference(resolution,[status(thm)],[c_2419,c_138]) ).
tcf(c_2436,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_4,e_4)
| ~ product(e_4,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_1557]) ).
tcf(c_2444,plain,
( equalish(e_1,e_4)
| ~ product(e_4,e_4,e_4)
| ~ product(e_1,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_1528]) ).
tcf(c_2457,plain,
( equalish(e_5,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) ),
inference(resolution,[status(thm)],[c_2422,c_1604]) ).
tcf(c_2475,plain,
( equalish(e_4,e_5)
| ~ product(e_5,e_5,e_5)
| ~ product(e_5,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_1575]) ).
tcf(c_2476,plain,
( equalish(e_3,e_5)
| ~ product(e_5,e_5,e_5)
| ~ product(e_5,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_1560]) ).
tcf(c_2477,plain,
( equalish(e_2,e_5)
| ~ product(e_5,e_5,e_5)
| ~ product(e_5,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_1545]) ).
tcf(c_2483,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_1576]) ).
tcf(c_2486,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_1531]) ).
tcf(c_2515,plain,
( equalish(e_5,e_6)
| ~ product(e_6,e_6,e_6)
| ~ product(e_6,e_5,e_6) ),
inference(instantiation,[status(thm)],[c_1595]) ).
tcf(c_2516,plain,
( equalish(e_4,e_6)
| ~ product(e_6,e_6,e_6)
| ~ product(e_6,e_4,e_6) ),
inference(instantiation,[status(thm)],[c_1578]) ).
tcf(c_2526,plain,
( equalish(e_4,e_6)
| ~ product(e_6,e_6,e_6)
| ~ product(e_4,e_6,e_6) ),
inference(instantiation,[status(thm)],[c_1579]) ).
tcf(c_2545,plain,
( product(e_5,e_6,e_1)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_4)
| product(e_5,e_6,e_5) ),
inference(global_subsumption_just,[status(thm)],[c_2457,c_163,c_2457]) ).
tcf(c_2546,plain,
( 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) ),
inference(renaming,[status(thm)],[c_2545]) ).
tcf(c_2554,plain,
( 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)
| product(e_5,e_5,e_6) ),
inference(resolution,[status(thm)],[c_2546,c_1598]) ).
tcf(c_2555,plain,
( equalish(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) ),
inference(resolution,[status(thm)],[c_2546,c_1613]) ).
tcf(c_2595,plain,
( 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) ),
inference(global_subsumption_just,[status(thm)],[c_2554,c_168,c_2555]) ).
tcf(c_2617,plain,
! [X0: $i] :
( equalish(X0,e_6)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| ~ product(e_5,X0,e_4) ),
inference(resolution,[status(thm)],[c_2595,c_171]) ).
tcf(c_2618,plain,
( equalish(e_1,e_6)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| ~ product(e_5,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_2617]) ).
tcf(c_2619,plain,
! [X0: $i] :
( equalish(X0,e_5)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| ~ product(X0,e_6,e_4) ),
inference(resolution,[status(thm)],[c_2595,c_172]) ).
tcf(c_2620,plain,
( equalish(e_1,e_5)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| ~ product(e_1,e_6,e_4) ),
inference(instantiation,[status(thm)],[c_2619]) ).
tcf(c_2621,plain,
! [X0: $i] :
( product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,X0)
| ~ product(e_6,X0,e_5) ),
inference(resolution,[status(thm)],[c_2595,c_174]) ).
tcf(c_2622,plain,
( product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_1)
| ~ product(e_6,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_2621]) ).
tcf(c_2756,plain,
( equalish(e_1,e_5)
| ~ product(e_2,e_5,e_3)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_1530]) ).
tcf(c_2769,plain,
( product(e_3,e_1,e_6)
| ~ product(e_2,e_1,e_3)
| ~ product(e_1,e_6,e_2) ),
inference(instantiation,[status(thm)],[c_1518]) ).
tcf(c_2770,plain,
( product(e_3,e_1,e_5)
| ~ product(e_2,e_1,e_3)
| ~ product(e_1,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_1517]) ).
tcf(c_2772,plain,
! [X0: $i,X1: $i] :
( product(X1,e_2,X0)
| ~ product(e_3,e_2,X1)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_1635]) ).
tcf(c_2773,plain,
( product(e_1,e_2,e_1)
| ~ product(e_3,e_2,e_1)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_2772]) ).
tcf(c_2888,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_1686]) ).
tcf(c_2916,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,e_3)
| ~ product(X0,e_3,e_4)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_1782]) ).
tcf(c_2951,plain,
( product(e_3,e_1,e_5)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_1)
| ~ group_element(e_3)
| ~ group_element(e_1) ),
inference(superposition,[status(thm)],[c_169,c_420]) ).
tcf(c_2954,plain,
( product(e_4,e_1,e_5)
| product(e_4,e_1,e_4)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| ~ group_element(e_4)
| ~ group_element(e_1) ),
inference(superposition,[status(thm)],[c_169,c_424]) ).
tcf(c_3065,plain,
( product(e_2,e_1,e_6)
| ~ product(e_3,e_1,e_2)
| ~ product(e_1,e_6,e_3) ),
inference(instantiation,[status(thm)],[c_1515]) ).
tcf(c_3066,plain,
( product(e_2,e_1,e_5)
| ~ product(e_3,e_1,e_2)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_1513]) ).
tcf(c_3067,plain,
( product(e_2,e_1,e_4)
| ~ product(e_3,e_1,e_2)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_1511]) ).
tcf(c_3069,plain,
! [X0: $i,X1: $i] :
( product(e_2,X0,X1)
| ~ product(e_3,X0,e_2)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_1665]) ).
tcf(c_3118,plain,
( product(e_6,e_5,e_1)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_4)
| product(e_6,e_5,e_5) ),
inference(global_subsumption_just,[status(thm)],[c_2418,c_163,c_1728,c_2418,c_2515]) ).
tcf(c_3119,plain,
( product(e_6,e_5,e_5)
| product(e_6,e_5,e_4)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1) ),
inference(renaming,[status(thm)],[c_3118]) ).
tcf(c_3127,plain,
( equalish(e_6,e_5)
| product(e_6,e_5,e_4)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1) ),
inference(resolution,[status(thm)],[c_3119,c_1604]) ).
tcf(c_3128,plain,
( product(e_6,e_5,e_4)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_5) ),
inference(resolution,[status(thm)],[c_3119,c_2621]) ).
tcf(c_3142,plain,
( product(e_6,e_5,e_4)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1) ),
inference(global_subsumption_just,[status(thm)],[c_3128,c_168,c_3127]) ).
tcf(c_3144,plain,
! [X0: $i] :
( equalish(X0,e_4)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| ~ product(e_6,e_5,X0) ),
inference(resolution,[status(thm)],[c_3142,c_170]) ).
tcf(c_3145,plain,
! [X0: $i] :
( equalish(X0,e_5)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| ~ product(e_6,X0,e_4) ),
inference(resolution,[status(thm)],[c_3142,c_171]) ).
tcf(c_3146,plain,
( equalish(e_1,e_5)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| ~ product(e_6,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_3145]) ).
tcf(c_3147,plain,
! [X0: $i] :
( equalish(X0,e_6)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| ~ product(X0,e_5,e_4) ),
inference(resolution,[status(thm)],[c_3142,c_172]) ).
tcf(c_3149,plain,
! [X0: $i] :
( product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_4,e_5,X0)
| ~ product(e_5,X0,e_6) ),
inference(resolution,[status(thm)],[c_3142,c_174]) ).
tcf(c_3150,plain,
( product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_4,e_5,e_1)
| ~ product(e_5,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_3149]) ).
tcf(c_3157,plain,
! [X0: $i] :
( equalish(e_4,e_1)
| ~ product(X0,e_4,e_2)
| ~ product(X0,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1566]) ).
tcf(c_3166,plain,
( equalish(e_5,e_1)
| ~ product(e_5,e_4,e_2)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_1582]) ).
tcf(c_3184,plain,
! [X0: $i,X1: $i] :
( product(e_2,e_4,X0)
| ~ product(X1,e_4,e_2)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_1665]) ).
tcf(c_3189,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,e_4)
| ~ product(X0,e_4,e_2)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_1785]) ).
tcf(c_3268,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_1573]) ).
tcf(c_3271,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_1558]) ).
tcf(c_3276,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_3271]) ).
tcf(c_3279,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_3268]) ).
tcf(c_3284,plain,
( equalish(e_5,e_1)
| ~ product(e_4,e_5,e_2)
| ~ product(e_4,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1581]) ).
tcf(c_3290,plain,
( equalish(e_6,e_5)
| ~ product(e_4,e_6,e_2)
| ~ product(e_4,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_1618]) ).
tcf(c_3292,plain,
( equalish(e_6,e_3)
| ~ product(e_4,e_6,e_2)
| ~ product(e_4,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_1611]) ).
tcf(c_3294,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_1602]) ).
tcf(c_3295,plain,
( equalish(e_5,e_6)
| ~ product(e_4,e_6,e_2)
| ~ product(e_4,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_1595]) ).
tcf(c_3297,plain,
( equalish(e_3,e_6)
| ~ product(e_4,e_6,e_2)
| ~ product(e_4,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_1563]) ).
tcf(c_3301,plain,
( product(e_2,e_1,e_6)
| ~ product(e_4,e_1,e_2)
| ~ product(e_1,e_6,e_4) ),
inference(instantiation,[status(thm)],[c_1515]) ).
tcf(c_3302,plain,
( product(e_2,e_1,e_5)
| ~ product(e_4,e_1,e_2)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_1513]) ).
tcf(c_3305,plain,
! [X0: $i,X1: $i] :
( product(e_2,X0,X1)
| ~ product(e_4,X0,e_2)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_1665]) ).
tcf(c_3321,plain,
( product(e_6,e_4,e_6)
| product(e_6,e_4,e_5)
| product(e_6,e_4,e_4)
| product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1) ),
inference(resolution,[status(thm)],[c_136,c_1660]) ).
tcf(c_3323,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(X0) ),
inference(resolution,[status(thm)],[c_136,c_169]) ).
tcf(c_3324,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_1) ),
inference(instantiation,[status(thm)],[c_3323]) ).
tcf(c_3339,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) ),
inference(resolution,[status(thm)],[c_3323,c_137]) ).
tcf(c_3340,plain,
( product(e_4,e_6,e_6)
| product(e_4,e_6,e_5)
| product(e_4,e_6,e_4)
| product(e_4,e_6,e_3)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1) ),
inference(resolution,[status(thm)],[c_3323,c_138]) ).
tcf(c_3350,plain,
! [X0: $i] :
( equalish(e_3,e_2)
| ~ product(X0,e_5,e_3)
| ~ product(X0,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_1553]) ).
tcf(c_3360,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_1592]) ).
tcf(c_3361,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_1589]) ).
tcf(c_3362,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_1585]) ).
tcf(c_3371,plain,
( equalish(e_5,e_2)
| ~ product(e_1,e_5,e_3)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_3362]) ).
tcf(c_3373,plain,
( equalish(e_5,e_4)
| ~ product(e_1,e_5,e_3)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_3360]) ).
tcf(c_3382,plain,
( equalish(e_4,e_6)
| ~ product(e_6,e_5,e_3)
| ~ product(e_4,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_1579]) ).
tcf(c_3385,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_1534]) ).
tcf(c_3389,plain,
! [X0: $i,X1: $i] :
( product(e_3,e_5,X0)
| ~ product(X1,e_5,e_3)
| ~ product(e_5,X0,X1) ),
inference(instantiation,[status(thm)],[c_1689]) ).
tcf(c_3433,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_1590]) ).
tcf(c_3437,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_1561]) ).
tcf(c_3442,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_3437]) ).
tcf(c_3446,plain,
( equalish(e_5,e_3)
| ~ product(e_5,e_1,e_2)
| ~ product(e_3,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_3433]) ).
tcf(c_3451,plain,
( equalish(e_6,e_3)
| ~ product(e_5,e_6,e_2)
| ~ product(e_5,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_1611]) ).
tcf(c_3453,plain,
( equalish(e_6,e_1)
| ~ product(e_5,e_6,e_2)
| ~ product(e_5,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1602]) ).
tcf(c_3455,plain,
( equalish(e_4,e_6)
| ~ product(e_5,e_6,e_2)
| ~ product(e_5,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_1578]) ).
tcf(c_3458,plain,
( equalish(e_1,e_6)
| ~ product(e_5,e_6,e_2)
| ~ product(e_5,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1533]) ).
tcf(c_3460,plain,
( product(e_2,e_1,e_6)
| ~ product(e_5,e_1,e_2)
| ~ product(e_1,e_6,e_5) ),
inference(instantiation,[status(thm)],[c_1515]) ).
tcf(c_3471,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_4) ),
inference(global_subsumption_just,[status(thm)],[c_2951,c_135,c_133,c_175,c_140,c_416,c_478,c_1682,c_1683,c_2253]) ).
tcf(c_3472,plain,
( product(e_3,e_1,e_4)
| product(e_3,e_1,e_2) ),
inference(renaming,[status(thm)],[c_3471]) ).
tcf(c_3476,plain,
! [X0: $i] :
( product(e_3,e_1,e_2)
| product(X0,e_3,e_1)
| ~ product(e_4,e_3,X0) ),
inference(superposition,[status(thm)],[c_3472,c_174]) ).
tcf(c_3479,plain,
( product(e_3,e_1,e_2)
| product(e_1,e_3,e_1)
| ~ product(e_4,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_3476]) ).
tcf(c_3480,plain,
( product(e_4,e_1,e_5)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_2954,c_133,c_175,c_141,c_424,c_501,c_1693,c_1694,c_3324]) ).
tcf(c_3481,plain,
( product(e_4,e_1,e_5)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2) ),
inference(renaming,[status(thm)],[c_3480]) ).
tcf(c_3485,plain,
! [X0: $i] :
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(X0,e_4,e_1)
| ~ product(e_5,e_4,X0) ),
inference(superposition,[status(thm)],[c_3481,c_174]) ).
tcf(c_3488,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_1,e_4,e_1)
| ~ product(e_5,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_3485]) ).
tcf(c_3491,plain,
! [X0: $i] :
( equalish(e_3,e_1)
| ~ product(X0,e_6,e_3)
| ~ product(X0,e_6,e_1) ),
inference(instantiation,[status(thm)],[c_1550]) ).
tcf(c_3502,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_1615]) ).
tcf(c_3522,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,e_6)
| ~ product(X0,e_6,e_3)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_1955]) ).
tcf(c_3525,plain,
! [X0: $i,X1: $i] :
( product(e_3,e_6,X0)
| ~ product(X1,e_6,e_3)
| ~ product(e_6,X0,X1) ),
inference(instantiation,[status(thm)],[c_1689]) ).
tcf(c_3559,plain,
( product(e_4,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_3)
| product(e_4,e_6,e_4)
| product(e_4,e_6,e_5) ),
inference(global_subsumption_just,[status(thm)],[c_3340,c_158,c_1728,c_2526,c_3340]) ).
tcf(c_3560,plain,
( product(e_4,e_6,e_5)
| product(e_4,e_6,e_4)
| product(e_4,e_6,e_3)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1) ),
inference(renaming,[status(thm)],[c_3559]) ).
tcf(c_3562,plain,
! [X0: $i] :
( equalish(X0,e_6)
| product(e_4,e_6,e_4)
| product(e_4,e_6,e_3)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| ~ product(e_4,X0,e_5) ),
inference(resolution,[status(thm)],[c_3560,c_171]) ).
tcf(c_3563,plain,
( equalish(e_1,e_6)
| product(e_4,e_6,e_4)
| product(e_4,e_6,e_3)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_3562]) ).
tcf(c_3564,plain,
! [X0: $i] :
( equalish(X0,e_4)
| product(e_4,e_6,e_4)
| product(e_4,e_6,e_3)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| ~ product(X0,e_6,e_5) ),
inference(resolution,[status(thm)],[c_3560,c_172]) ).
tcf(c_3565,plain,
( equalish(e_1,e_4)
| product(e_4,e_6,e_4)
| product(e_4,e_6,e_3)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| ~ product(e_1,e_6,e_5) ),
inference(instantiation,[status(thm)],[c_3564]) ).
tcf(c_3566,plain,
! [X0: $i] :
( product(e_4,e_6,e_4)
| product(e_4,e_6,e_3)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_5,e_6,X0)
| ~ product(e_6,X0,e_4) ),
inference(resolution,[status(thm)],[c_3560,c_174]) ).
tcf(c_3577,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_1619]) ).
tcf(c_3578,plain,
! [X0: $i] :
( equalish(e_6,e_4)
| ~ product(e_6,X0,e_2)
| ~ product(e_4,X0,e_2) ),
inference(instantiation,[status(thm)],[c_1616]) ).
tcf(c_3579,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_1612]) ).
tcf(c_3582,plain,
! [X0: $i] :
( equalish(e_5,e_6)
| ~ product(e_6,X0,e_2)
| ~ product(e_5,X0,e_2) ),
inference(instantiation,[status(thm)],[c_1596]) ).
tcf(c_3583,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_1579]) ).
tcf(c_3584,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_1564]) ).
tcf(c_3589,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_3584]) ).
tcf(c_3590,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_3583]) ).
tcf(c_3591,plain,
( equalish(e_5,e_6)
| ~ product(e_6,e_1,e_2)
| ~ product(e_5,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_3582]) ).
tcf(c_3594,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_3579]) ).
tcf(c_3595,plain,
( equalish(e_6,e_4)
| ~ product(e_6,e_1,e_2)
| ~ product(e_4,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_3578]) ).
tcf(c_3596,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_3577]) ).
tcf(c_3599,plain,
( product(e_2,e_1,e_5)
| ~ product(e_6,e_1,e_2)
| ~ product(e_1,e_5,e_6) ),
inference(instantiation,[status(thm)],[c_1513]) ).
tcf(c_3600,plain,
( product(e_2,e_1,e_4)
| ~ product(e_6,e_1,e_2)
| ~ product(e_1,e_4,e_6) ),
inference(instantiation,[status(thm)],[c_1511]) ).
tcf(c_3602,plain,
! [X0: $i,X1: $i] :
( product(e_2,X0,X1)
| ~ product(e_6,X0,e_2)
| ~ product(X0,X1,e_6) ),
inference(instantiation,[status(thm)],[c_1665]) ).
tcf(c_3610,plain,
( product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_5)
| product(e_4,e_6,e_4)
| product(e_4,e_6,e_3)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1) ),
inference(resolution,[status(thm)],[c_3566,c_3142]) ).
tcf(c_3611,plain,
! [X0: $i] :
( equalish(X0,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_5)
| product(e_4,e_6,e_4)
| product(e_4,e_6,e_3)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| ~ product(e_6,e_5,X0) ),
inference(resolution,[status(thm)],[c_3610,c_170]) ).
tcf(c_3692,plain,
( equalish(e_4,e_2)
| ~ product(e_3,e_1,e_4)
| ~ product(e_3,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1568]) ).
tcf(c_3697,plain,
( product(e_4,e_1,e_6)
| ~ product(e_3,e_1,e_4)
| ~ product(e_1,e_6,e_3) ),
inference(instantiation,[status(thm)],[c_1519]) ).
tcf(c_3698,plain,
! [X0: $i] :
( product(X0,e_3,e_1)
| ~ product(e_3,e_1,e_4)
| ~ product(e_4,e_3,X0) ),
inference(instantiation,[status(thm)],[c_1684]) ).
tcf(c_3700,plain,
! [X0: $i] :
( product(e_4,e_1,X0)
| ~ product(e_3,e_1,e_4)
| ~ product(e_1,X0,e_3) ),
inference(instantiation,[status(thm)],[c_1700]) ).
tcf(c_3713,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_1543]) ).
tcf(c_3720,plain,
( product(e_4,e_6,e_4)
| product(e_4,e_6,e_3)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1) ),
inference(global_subsumption_just,[status(thm)],[c_3611,c_138,c_134,c_133,c_175,c_164,c_146,c_143,c_141,c_139,c_404,c_408,c_412,c_420,c_424,c_455,c_539,c_1630,c_1654,c_1668,c_1921,c_2210,c_2769,c_3065,c_3301,c_3472,c_3481,c_3563,c_3565,c_3697,c_3713]) ).
tcf(c_3722,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,X0)
| ~ product(X0,X0,X1) ),
inference(superposition,[status(thm)],[c_173,c_174]) ).
tcf(c_3731,plain,
( equalish(e_6,e_4)
| product(e_4,e_6,e_3)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1) ),
inference(resolution,[status(thm)],[c_3720,c_1613]) ).
tcf(c_3732,plain,
( equalish(e_4,e_5)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_3)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1) ),
inference(resolution,[status(thm)],[c_3720,c_2619]) ).
tcf(c_3743,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X0,X2,e_5)
| product(X0,X2,e_4)
| product(X0,X2,e_3)
| product(X0,X2,e_2)
| product(X0,X2,e_1)
| product(X1,X0,X2)
| ~ group_element(X2)
| ~ group_element(X0)
| ~ product(e_6,X0,X1) ),
inference(superposition,[status(thm)],[c_169,c_174]) ).
tcf(c_3744,plain,
! [X0: $i] :
( product(e_6,X0,X0)
| product(X0,X0,e_5)
| product(X0,X0,e_4)
| product(X0,X0,e_3)
| product(X0,X0,e_2)
| product(X0,X0,e_1)
| ~ group_element(X0) ),
inference(superposition,[status(thm)],[c_169,c_3722]) ).
tcf(c_3755,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_1546]) ).
tcf(c_3779,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_1549]) ).
tcf(c_3786,plain,
( product(e_4,e_6,e_3)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1) ),
inference(global_subsumption_just,[status(thm)],[c_3732,c_167,c_3731]) ).
tcf(c_3791,plain,
! [X0: $i] :
( equalish(X0,e_4)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| ~ product(X0,e_6,e_3) ),
inference(resolution,[status(thm)],[c_3786,c_172]) ).
tcf(c_3792,plain,
( equalish(e_1,e_4)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| ~ product(e_1,e_6,e_3) ),
inference(instantiation,[status(thm)],[c_3791]) ).
tcf(c_3793,plain,
! [X0: $i] :
( product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_3,e_6,X0)
| ~ product(e_6,X0,e_4) ),
inference(resolution,[status(thm)],[c_3786,c_174]) ).
tcf(c_3794,plain,
( product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_3,e_6,e_1)
| ~ product(e_6,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_3793]) ).
tcf(c_3798,plain,
! [X0: $i] :
( product(e_6,e_6,X0)
| 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(superposition,[status(thm)],[c_173,c_3743]) ).
tcf(c_3821,plain,
( product(e_6,e_6,e_6)
| product(e_6,e_6,e_5)
| product(e_6,e_6,e_4)
| product(e_6,e_6,e_3)
| product(e_6,e_6,e_2)
| product(e_6,e_6,e_1)
| ~ group_element(e_6) ),
inference(superposition,[status(thm)],[c_3744,c_3722]) ).
tcf(c_3887,plain,
( product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_3,e_6,e_5) ),
inference(resolution,[status(thm)],[c_3793,c_3142]) ).
tcf(c_3888,plain,
! [X0: $i] :
( equalish(X0,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_3,e_6,e_5)
| ~ product(e_6,e_5,X0) ),
inference(resolution,[status(thm)],[c_3887,c_170]) ).
tcf(c_3889,plain,
! [X0: $i] :
( equalish(X0,e_5)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_3,e_6,e_5)
| ~ product(e_6,X0,e_3) ),
inference(resolution,[status(thm)],[c_3887,c_171]) ).
tcf(c_3932,plain,
( product(e_3,e_1,e_4)
| ~ product(e_2,e_1,e_3)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_2357]) ).
tcf(c_3949,plain,
product(e_6,e_6,e_6),
inference(global_subsumption_just,[status(thm)],[c_3821,c_1728]) ).
tcf(c_3955,plain,
! [X0: $i] :
( product(X0,e_6,e_6)
| ~ product(e_6,e_6,X0) ),
inference(superposition,[status(thm)],[c_3949,c_174]) ).
tcf(c_4076,plain,
! [X0: $i] :
( product(X0,e_1,e_5)
| ~ product(e_1,e_5,e_4)
| ~ product(e_4,e_1,X0) ),
inference(instantiation,[status(thm)],[c_1943]) ).
tcf(c_4098,plain,
! [X0: $i,X1: $i] :
( product(e_3,X0,X1)
| ~ product(e_4,X0,e_3)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_1689]) ).
tcf(c_4279,plain,
! [X0: $i] :
( product(e_3,X0,e_3)
| ~ product(e_4,X0,e_3)
| ~ product(X0,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_2916]) ).
tcf(c_4285,plain,
( product(e_4,e_5,e_6)
| product(e_4,e_5,e_1)
| product(e_4,e_5,e_2)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_4) ),
inference(global_subsumption_just,[status(thm)],[c_3339,c_157,c_1706,c_2483,c_3339]) ).
tcf(c_4286,plain,
( product(e_4,e_5,e_6)
| 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) ),
inference(renaming,[status(thm)],[c_4285]) ).
tcf(c_4289,plain,
! [X0: $i] :
( equalish(X0,e_4)
| 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)
| ~ product(X0,e_5,e_6) ),
inference(resolution,[status(thm)],[c_4286,c_172]) ).
tcf(c_4290,plain,
( equalish(e_1,e_4)
| 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)
| ~ product(e_1,e_5,e_6) ),
inference(instantiation,[status(thm)],[c_4289]) ).
tcf(c_4291,plain,
! [X0: $i] :
( 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)
| product(e_6,e_5,X0)
| ~ product(e_5,X0,e_4) ),
inference(resolution,[status(thm)],[c_4286,c_174]) ).
tcf(c_4292,plain,
( product(e_6,e_5,e_1)
| 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)
| ~ product(e_5,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_4291]) ).
tcf(c_4320,plain,
( product(e_6,e_5,e_6)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| 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) ),
inference(resolution,[status(thm)],[c_4291,c_2595]) ).
tcf(c_4354,plain,
( product(e_4,e_5,e_1)
| product(e_4,e_5,e_2)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_4)
| product(e_5,e_6,e_1)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_4320,c_163,c_1728,c_2515,c_4320]) ).
tcf(c_4355,plain,
( product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| 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) ),
inference(renaming,[status(thm)],[c_4354]) ).
tcf(c_4393,plain,
! [X0: $i] :
( equalish(e_5,e_3)
| ~ product(e_5,X0,e_3)
| ~ product(e_3,X0,e_3) ),
inference(instantiation,[status(thm)],[c_1590]) ).
tcf(c_4405,plain,
! [X0: $i,X1: $i] :
( product(e_3,X0,X1)
| ~ product(e_5,X0,e_3)
| ~ product(X0,X1,e_5) ),
inference(instantiation,[status(thm)],[c_1689]) ).
tcf(c_4425,plain,
! [X0: $i] :
( product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| 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)
| product(e_3,e_6,X0)
| ~ product(e_6,X0,e_5) ),
inference(resolution,[status(thm)],[c_4355,c_174]) ).
tcf(c_4426,plain,
( product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| 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)
| product(e_3,e_6,e_1)
| ~ product(e_6,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_4425]) ).
tcf(c_4429,plain,
( equalish(e_5,e_4)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| 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) ),
inference(resolution,[status(thm)],[c_4355,c_3791]) ).
tcf(c_4430,plain,
( product(e_2,e_1,e_5)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| ~ group_element(e_2)
| ~ group_element(e_1) ),
inference(superposition,[status(thm)],[c_169,c_412]) ).
tcf(c_4431,plain,
( product(e_3,e_1,e_5)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_1)
| ~ group_element(e_3)
| ~ group_element(e_1) ),
inference(superposition,[status(thm)],[c_169,c_420]) ).
tcf(c_4432,plain,
( product(e_4,e_1,e_5)
| product(e_4,e_1,e_4)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| ~ group_element(e_4)
| ~ group_element(e_1) ),
inference(superposition,[status(thm)],[c_169,c_424]) ).
tcf(c_4584,plain,
( product(e_4,e_5,e_1)
| product(e_4,e_5,e_2)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_4)
| product(e_4,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_5,e_6,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_4429,c_162,c_4429]) ).
tcf(c_4585,plain,
( product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| 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) ),
inference(renaming,[status(thm)],[c_4584]) ).
tcf(c_4610,plain,
! [X0: $i] :
( equalish(X0,e_6)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| 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)
| ~ product(e_5,X0,e_2) ),
inference(resolution,[status(thm)],[c_4585,c_171]) ).
tcf(c_4611,plain,
( equalish(e_1,e_6)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| 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)
| ~ product(e_5,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_4610]) ).
tcf(c_4614,plain,
! [X0: $i] :
( product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| 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)
| product(e_2,e_6,X0)
| ~ product(e_6,X0,e_5) ),
inference(resolution,[status(thm)],[c_4585,c_174]) ).
tcf(c_4615,plain,
( product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| 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)
| product(e_2,e_6,e_1)
| ~ product(e_6,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_4614]) ).
tcf(c_4750,plain,
! [X0: $i] :
( product(e_2,e_2,X0)
| ~ product(e_3,e_2,e_2)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_3069]) ).
tcf(c_4751,plain,
( product(e_2,e_2,e_1)
| ~ product(e_3,e_2,e_2)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_4750]) ).
tcf(c_4860,plain,
! [X0: $i] :
( product(X0,e_6,e_2)
| ~ product(e_6,e_2,e_1)
| ~ product(e_1,e_6,X0) ),
inference(instantiation,[status(thm)],[c_1631]) ).
tcf(c_4958,plain,
! [X0: $i] :
( product(e_3,e_6,X0)
| ~ product(e_4,e_6,e_3)
| ~ product(e_6,X0,e_4) ),
inference(instantiation,[status(thm)],[c_3525]) ).
tcf(c_4960,plain,
! [X0: $i] :
( equalish(e_6,e_4)
| ~ product(e_6,X0,e_4)
| ~ product(e_4,X0,e_4) ),
inference(instantiation,[status(thm)],[c_1616]) ).
tcf(c_4961,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_1612]) ).
tcf(c_4964,plain,
! [X0: $i] :
( equalish(e_5,e_6)
| ~ product(e_6,X0,e_4)
| ~ product(e_5,X0,e_4) ),
inference(instantiation,[status(thm)],[c_1596]) ).
tcf(c_4966,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_1564]) ).
tcf(c_4969,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_4966]) ).
tcf(c_4971,plain,
( equalish(e_5,e_6)
| ~ product(e_6,e_1,e_4)
| ~ product(e_5,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_4964]) ).
tcf(c_4972,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_4961]) ).
tcf(c_4975,plain,
( product(e_3,e_6,e_1)
| ~ product(e_6,e_1,e_4)
| ~ product(e_4,e_6,e_3) ),
inference(instantiation,[status(thm)],[c_4958]) ).
tcf(c_4982,plain,
! [X0: $i,X1: $i] :
( product(X0,e_6,X1)
| ~ product(e_6,X1,e_4)
| ~ product(e_4,e_6,X0) ),
inference(instantiation,[status(thm)],[c_1729]) ).
tcf(c_4983,plain,
( product(e_1,e_6,e_1)
| ~ product(e_6,e_1,e_4)
| ~ product(e_4,e_6,e_1) ),
inference(instantiation,[status(thm)],[c_4982]) ).
tcf(c_5092,plain,
! [X0: $i] :
( product(e_1,e_4,X0)
| ~ product(e_2,e_4,e_1)
| ~ product(e_4,X0,e_2) ),
inference(instantiation,[status(thm)],[c_1643]) ).
tcf(c_5123,plain,
( product(e_1,e_5,e_4)
| ~ product(e_5,e_4,e_2)
| ~ product(e_2,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_3189]) ).
tcf(c_5134,plain,
! [X0: $i] :
( product(X0,e_2,e_5)
| ~ product(e_2,e_5,e_1)
| ~ product(e_1,e_2,X0) ),
inference(instantiation,[status(thm)],[c_1635]) ).
tcf(c_5140,plain,
! [X0: $i] :
( product(e_6,e_6,X0)
| 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(X0) ),
inference(global_subsumption_just,[status(thm)],[c_3798,c_138,c_1646]) ).
tcf(c_5160,plain,
! [X0: $i] :
( 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)
| product(X0,e_6,e_6)
| ~ group_element(X0) ),
inference(superposition,[status(thm)],[c_5140,c_3955]) ).
tcf(c_5166,plain,
! [X0: $i,X1: $i] :
( product(e_6,e_6,X1)
| product(e_6,X1,e_4)
| product(e_6,X1,e_3)
| product(e_6,X1,e_2)
| product(e_6,X1,e_1)
| product(X0,e_6,X1)
| ~ group_element(X1)
| ~ product(e_5,e_6,X0) ),
inference(superposition,[status(thm)],[c_5140,c_174]) ).
tcf(c_5182,plain,
( product(e_6,e_6,e_1)
| 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)
| product(e_1,e_6,e_1)
| ~ group_element(e_1)
| ~ product(e_5,e_6,e_1) ),
inference(instantiation,[status(thm)],[c_5166]) ).
tcf(c_5201,plain,
! [X0: $i] :
( product(e_2,e_4,X0)
| ~ product(e_5,e_4,e_2)
| ~ product(e_4,X0,e_5) ),
inference(instantiation,[status(thm)],[c_3184]) ).
tcf(c_5208,plain,
( product(e_2,e_4,e_1)
| ~ product(e_5,e_4,e_2)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_5201]) ).
tcf(c_5210,plain,
! [X0: $i] :
( equalish(e_5,e_4)
| ~ product(e_4,X0,e_5)
| ~ product(e_4,X0,e_4) ),
inference(instantiation,[status(thm)],[c_1591]) ).
tcf(c_5212,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_1584]) ).
tcf(c_5223,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_5212]) ).
tcf(c_5232,plain,
! [X0: $i,X1: $i] :
( product(e_5,X0,X1)
| ~ product(e_4,X0,e_5)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_1723]) ).
tcf(c_5269,plain,
! [X0: $i] :
( equalish(e_5,e_4)
| ~ product(e_5,X0,e_4)
| ~ product(e_4,X0,e_4) ),
inference(instantiation,[status(thm)],[c_1593]) ).
tcf(c_5270,plain,
! [X0: $i] :
( equalish(e_5,e_3)
| ~ product(e_5,X0,e_4)
| ~ product(e_3,X0,e_4) ),
inference(instantiation,[status(thm)],[c_1590]) ).
tcf(c_5272,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_1582]) ).
tcf(c_5274,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_1561]) ).
tcf(c_5277,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_5274]) ).
tcf(c_5279,plain,
( equalish(e_5,e_3)
| ~ product(e_5,e_1,e_4)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_5270]) ).
tcf(c_5286,plain,
! [X0: $i,X1: $i] :
( product(X0,e_5,X1)
| ~ product(e_5,X1,e_4)
| ~ product(e_4,e_5,X0) ),
inference(instantiation,[status(thm)],[c_1707]) ).
tcf(c_5287,plain,
( product(e_1,e_5,e_1)
| ~ product(e_5,e_1,e_4)
| ~ product(e_4,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_5286]) ).
tcf(c_5301,plain,
( product(e_6,e_4,e_1)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_3)
| product(e_6,e_4,e_4)
| product(e_6,e_4,e_5) ),
inference(global_subsumption_just,[status(thm)],[c_3321,c_158,c_1728,c_2516,c_3321]) ).
tcf(c_5302,plain,
( product(e_6,e_4,e_5)
| product(e_6,e_4,e_4)
| product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1) ),
inference(renaming,[status(thm)],[c_5301]) ).
tcf(c_5304,plain,
! [X0: $i] :
( equalish(X0,e_4)
| 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)
| ~ product(e_6,X0,e_5) ),
inference(resolution,[status(thm)],[c_5302,c_171]) ).
tcf(c_5305,plain,
( equalish(e_1,e_4)
| 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)
| ~ product(e_6,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_5304]) ).
tcf(c_5306,plain,
! [X0: $i] :
( equalish(X0,e_6)
| 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)
| ~ product(X0,e_4,e_5) ),
inference(resolution,[status(thm)],[c_5302,c_172]) ).
tcf(c_5307,plain,
( equalish(e_1,e_6)
| 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)
| ~ product(e_1,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_5306]) ).
tcf(c_5309,plain,
( 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)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_4) ),
inference(resolution,[status(thm)],[c_5302,c_2621]) ).
tcf(c_5311,plain,
( 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)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| 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)
| product(e_2,e_6,e_4) ),
inference(resolution,[status(thm)],[c_5302,c_4614]) ).
tcf(c_5322,plain,
( equalish(e_6,e_5)
| ~ product(e_2,e_6,e_1)
| ~ product(e_2,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_1618]) ).
tcf(c_5360,plain,
( equalish(e_6,e_4)
| product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_4) ),
inference(resolution,[status(thm)],[c_5309,c_1604]) ).
tcf(c_5361,plain,
( equalish(e_4,e_5)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_4) ),
inference(resolution,[status(thm)],[c_5309,c_3145]) ).
tcf(c_5486,plain,
! [X0: $i] :
( equalish(e_3,e_1)
| ~ product(X0,e_3,e_5)
| ~ product(X0,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_1551]) ).
tcf(c_5524,plain,
( product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_4) ),
inference(global_subsumption_just,[status(thm)],[c_5361,c_167,c_5360]) ).
tcf(c_5542,plain,
! [X0: $i] :
( equalish(e_6,e_5)
| ~ product(X0,e_6,e_4)
| ~ product(X0,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_1618]) ).
tcf(c_5543,plain,
! [X0: $i] :
( equalish(e_6,e_4)
| ~ product(X0,e_6,e_4)
| ~ product(X0,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_1615]) ).
tcf(c_5545,plain,
! [X0: $i] :
( equalish(e_6,e_2)
| ~ product(X0,e_6,e_4)
| ~ product(X0,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_1606]) ).
tcf(c_5556,plain,
( equalish(e_6,e_2)
| ~ product(e_1,e_6,e_4)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_5545]) ).
tcf(c_5559,plain,
( equalish(e_6,e_5)
| ~ product(e_1,e_6,e_4)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_5542]) ).
tcf(c_5569,plain,
! [X0: $i,X1: $i] :
( product(e_4,e_6,X0)
| ~ product(X1,e_6,e_4)
| ~ product(e_6,X0,X1) ),
inference(instantiation,[status(thm)],[c_1700]) ).
tcf(c_5575,plain,
! [X0: $i] :
( equalish(X0,e_4)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_4)
| ~ product(e_6,X0,e_3) ),
inference(resolution,[status(thm)],[c_5524,c_171]) ).
tcf(c_5581,plain,
( equalish(e_4,e_5)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_4)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_3,e_6,e_5) ),
inference(resolution,[status(thm)],[c_5524,c_3889]) ).
tcf(c_5593,plain,
( product(e_3,e_6,e_5)
| product(e_4,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_4)
| product(e_5,e_6,e_1)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_3)
| product(e_6,e_4,e_1)
| product(e_6,e_4,e_2)
| product(e_6,e_5,e_1)
| product(e_6,e_5,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_5581,c_157,c_5581]) ).
tcf(c_5594,plain,
( product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_4)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_3,e_6,e_5) ),
inference(renaming,[status(thm)],[c_5593]) ).
tcf(c_5649,plain,
! [X0: $i] :
( equalish(X0,e_2)
| product(e_6,e_5,e_1)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_4)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_3,e_6,e_5)
| ~ product(e_6,e_5,X0) ),
inference(resolution,[status(thm)],[c_5594,c_170]) ).
tcf(c_5763,plain,
! [X0: $i] :
( product(e_1,e_5,X0)
| ~ product(e_3,e_5,e_1)
| ~ product(e_5,X0,e_3) ),
inference(instantiation,[status(thm)],[c_1649]) ).
tcf(c_5815,plain,
( equalish(e_6,e_5)
| ~ product(e_3,e_6,e_1)
| ~ product(e_3,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_1618]) ).
tcf(c_5816,plain,
( equalish(e_6,e_4)
| ~ product(e_3,e_6,e_1)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_1615]) ).
tcf(c_5820,plain,
( equalish(e_5,e_6)
| ~ product(e_3,e_6,e_1)
| ~ product(e_3,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_1595]) ).
tcf(c_5821,plain,
( equalish(e_4,e_6)
| ~ product(e_3,e_6,e_1)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_1578]) ).
tcf(c_6044,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_5,e_1)
| ~ product(e_3,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_1573]) ).
tcf(c_6045,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_5,e_1)
| ~ product(e_2,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_1570]) ).
tcf(c_6047,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_5,e_1)
| ~ product(e_3,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_1558]) ).
tcf(c_6052,plain,
( equalish(e_5,e_2)
| ~ product(e_4,e_5,e_1)
| ~ product(e_4,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_1585]) ).
tcf(c_6080,plain,
product(e_2,e_1,e_3),
inference(global_subsumption_just,[status(thm)],[c_4430,c_134,c_133,c_175,c_139,c_404,c_408,c_412,c_455,c_1630,c_1668,c_2210]) ).
tcf(c_6086,plain,
! [X0: $i] :
( product(X0,e_2,e_1)
| ~ product(e_3,e_2,X0) ),
inference(superposition,[status(thm)],[c_6080,c_174]) ).
tcf(c_6090,plain,
( product(e_6,e_2,e_1)
| 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(superposition,[status(thm)],[c_169,c_6086]) ).
tcf(c_6095,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_6,e_1)
| ~ product(e_3,e_6,e_1) ),
inference(instantiation,[status(thm)],[c_1573]) ).
tcf(c_6132,plain,
( product(e_6,e_2,e_1)
| product(e_3,e_2,e_5)
| product(e_3,e_2,e_4) ),
inference(global_subsumption_just,[status(thm)],[c_6090,c_135,c_134,c_133,c_175,c_145,c_139,c_404,c_408,c_412,c_447,c_455,c_1629,c_1630,c_1668,c_1683,c_2210,c_2229,c_2773,c_4751,c_6090]) ).
tcf(c_6137,plain,
! [X0: $i] :
( equalish(e_2,X0)
| product(e_3,e_2,e_5)
| product(e_3,e_2,e_4)
| ~ product(e_6,X0,e_1) ),
inference(superposition,[status(thm)],[c_6132,c_171]) ).
tcf(c_6138,plain,
! [X0: $i] :
( product(e_3,e_2,e_5)
| product(e_3,e_2,e_4)
| product(X0,e_6,e_2)
| ~ product(e_1,e_6,X0) ),
inference(superposition,[status(thm)],[c_6132,c_174]) ).
tcf(c_6153,plain,
( equalish(e_4,e_5)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| 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)
| product(e_2,e_6,e_4) ),
inference(resolution,[status(thm)],[c_5311,c_3145]) ).
tcf(c_6155,plain,
( product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| 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)
| product(e_3,e_6,e_4)
| product(e_2,e_6,e_4) ),
inference(resolution,[status(thm)],[c_5311,c_3793]) ).
tcf(c_6188,plain,
( product(e_6,e_6,e_2)
| 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)
| product(e_3,e_2,e_5)
| product(e_3,e_2,e_4)
| ~ group_element(e_1) ),
inference(superposition,[status(thm)],[c_5160,c_6138]) ).
tcf(c_6190,plain,
( equalish(e_5,e_3)
| ~ product(e_6,e_5,e_1)
| ~ product(e_6,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_1589]) ).
tcf(c_6194,plain,
( equalish(e_3,e_5)
| ~ product(e_6,e_5,e_1)
| ~ product(e_6,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_1560]) ).
tcf(c_6195,plain,
( equalish(e_2,e_5)
| ~ product(e_6,e_5,e_1)
| ~ product(e_6,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_1545]) ).
tcf(c_6199,plain,
( equalish(e_6,e_4)
| ~ product(e_6,e_5,e_1)
| ~ product(e_4,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_1616]) ).
tcf(c_6201,plain,
( equalish(e_6,e_2)
| ~ product(e_6,e_5,e_1)
| ~ product(e_2,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_1607]) ).
tcf(c_6204,plain,
( equalish(e_4,e_6)
| ~ product(e_6,e_5,e_1)
| ~ product(e_4,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_1579]) ).
tcf(c_6205,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_1564]) ).
tcf(c_6209,plain,
! [X0: $i] :
( product(e_1,e_5,X0)
| ~ product(e_6,e_5,e_1)
| ~ product(e_5,X0,e_6) ),
inference(instantiation,[status(thm)],[c_1649]) ).
tcf(c_6210,plain,
( product(e_1,e_5,e_1)
| ~ product(e_6,e_5,e_1)
| ~ product(e_5,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_6209]) ).
tcf(c_6221,plain,
( product(e_6,e_1,e_2)
| product(e_6,e_1,e_4)
| product(e_6,e_1,e_5) ),
inference(global_subsumption_just,[status(thm)],[c_6188,c_134,c_133,c_175,c_148,c_143,c_139,c_404,c_408,c_412,c_455,c_547,c_1630,c_1661,c_1668,c_1727,c_1728,c_2210,c_3779]) ).
tcf(c_6222,plain,
( product(e_6,e_1,e_5)
| product(e_6,e_1,e_4)
| product(e_6,e_1,e_2) ),
inference(renaming,[status(thm)],[c_6221]) ).
tcf(c_6225,plain,
! [X0: $i] :
( equalish(e_6,X0)
| product(e_6,e_1,e_4)
| product(e_6,e_1,e_2)
| ~ product(X0,e_1,e_5) ),
inference(superposition,[status(thm)],[c_6222,c_172]) ).
tcf(c_6227,plain,
! [X0: $i] :
( product(e_6,e_1,e_4)
| product(e_6,e_1,e_2)
| product(X0,e_6,e_1)
| ~ product(e_5,e_6,X0) ),
inference(superposition,[status(thm)],[c_6222,c_174]) ).
tcf(c_6231,plain,
( product(e_6,e_1,e_4)
| product(e_6,e_1,e_2)
| product(e_1,e_6,e_1)
| ~ product(e_5,e_6,e_1) ),
inference(instantiation,[status(thm)],[c_6227]) ).
tcf(c_6251,plain,
( equalish(e_5,e_4)
| ~ product(e_5,e_6,e_1)
| ~ product(e_4,e_6,e_1) ),
inference(instantiation,[status(thm)],[c_1593]) ).
tcf(c_6255,plain,
( equalish(e_4,e_5)
| ~ product(e_5,e_6,e_1)
| ~ product(e_4,e_6,e_1) ),
inference(instantiation,[status(thm)],[c_1576]) ).
tcf(c_6256,plain,
( equalish(e_3,e_5)
| ~ product(e_5,e_6,e_1)
| ~ product(e_3,e_6,e_1) ),
inference(instantiation,[status(thm)],[c_1561]) ).
tcf(c_6267,plain,
( equalish(e_2,e_6)
| ~ product(e_5,e_6,e_1)
| ~ product(e_5,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_1548]) ).
tcf(c_6269,plain,
! [X0: $i] :
( product(e_1,e_6,X0)
| ~ product(e_5,e_6,e_1)
| ~ product(e_6,X0,e_5) ),
inference(instantiation,[status(thm)],[c_1652]) ).
tcf(c_6270,plain,
( product(e_1,e_6,e_1)
| ~ product(e_6,e_1,e_5)
| ~ product(e_5,e_6,e_1) ),
inference(instantiation,[status(thm)],[c_6269]) ).
tcf(c_6276,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_4) ),
inference(global_subsumption_just,[status(thm)],[c_4431,c_135,c_133,c_175,c_140,c_416,c_478,c_1682,c_1683,c_2253]) ).
tcf(c_6277,plain,
( product(e_3,e_1,e_4)
| product(e_3,e_1,e_2) ),
inference(renaming,[status(thm)],[c_6276]) ).
tcf(c_6282,plain,
! [X0: $i] :
( product(e_3,e_1,e_2)
| product(X0,e_3,e_1)
| ~ product(e_4,e_3,X0) ),
inference(superposition,[status(thm)],[c_6277,c_174]) ).
tcf(c_6288,plain,
( 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)
| product(e_4,e_6,e_2)
| product(e_6,e_5,e_1)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_6153,c_138,c_134,c_133,c_175,c_168,c_156,c_148,c_147,c_143,c_142,c_139,c_404,c_408,c_412,c_455,c_524,c_539,c_547,c_1630,c_1648,c_1668,c_1705,c_1706,c_1922,c_2210,c_2420,c_3146,c_3150,c_3458,c_3596,c_3755,c_3779,c_4292,c_4426,c_4611,c_5182,c_6095]) ).
tcf(c_6289,plain,
( product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_4,e_6,e_2)
| 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) ),
inference(renaming,[status(thm)],[c_6288]) ).
tcf(c_6294,plain,
( product(e_6,e_3,e_1)
| 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)
| product(e_3,e_1,e_2)
| ~ group_element(e_4)
| ~ group_element(e_3) ),
inference(superposition,[status(thm)],[c_169,c_6282]) ).
tcf(c_6303,plain,
( product(e_6,e_6,e_1)
| 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)
| product(e_6,e_1,e_4)
| product(e_6,e_1,e_2)
| ~ group_element(e_5) ),
inference(superposition,[status(thm)],[c_5160,c_6227]) ).
tcf(c_6312,plain,
( product(e_6,e_3,e_1)
| product(e_4,e_3,e_5)
| product(e_3,e_1,e_2)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_6294,c_136,c_135,c_175,c_151,c_470,c_1694,c_2436,c_3479,c_6294]) ).
tcf(c_6313,plain,
( product(e_6,e_3,e_1)
| product(e_4,e_3,e_5)
| product(e_4,e_3,e_3)
| product(e_4,e_3,e_2)
| product(e_3,e_1,e_2) ),
inference(renaming,[status(thm)],[c_6312]) ).
tcf(c_6331,plain,
! [X0: $i] :
( product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_4,e_6,e_2)
| 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)
| product(e_3,e_5,X0)
| ~ product(e_5,X0,e_6) ),
inference(resolution,[status(thm)],[c_6289,c_174]) ).
tcf(c_6340,plain,
( equalish(e_3,e_2)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_4)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| 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)
| product(e_3,e_6,e_5) ),
inference(resolution,[status(thm)],[c_6289,c_5649]) ).
tcf(c_6390,plain,
( product(e_6,e_5,e_4)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1) ),
inference(global_subsumption_just,[status(thm)],[c_6303,c_168,c_3127]) ).
tcf(c_6398,plain,
! [X0: $i] :
( product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| 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)
| product(e_4,e_5,X0)
| ~ group_element(e_5)
| ~ group_element(X0) ),
inference(superposition,[status(thm)],[c_6390,c_3743]) ).
tcf(c_6402,plain,
( product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| 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)
| product(e_4,e_5,e_1)
| ~ group_element(e_5)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_6398]) ).
tcf(c_6444,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_1536]) ).
tcf(c_6463,plain,
! [X0: $i] :
( product(e_4,e_2,X0)
| ~ product(e_3,e_2,e_4)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_2772]) ).
tcf(c_6464,plain,
( product(e_4,e_2,e_1)
| ~ product(e_3,e_2,e_4)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_6463]) ).
tcf(c_6524,plain,
( product(e_4,e_5,e_4)
| product(e_4,e_5,e_1)
| product(e_4,e_5,e_2)
| product(e_5,e_6,e_1)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_3)
| product(e_6,e_5,e_1)
| product(e_6,e_5,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_6340,c_138,c_137,c_134,c_133,c_175,c_164,c_163,c_158,c_147,c_143,c_142,c_139,c_404,c_408,c_412,c_420,c_424,c_455,c_524,c_539,c_1630,c_1654,c_1668,c_1705,c_1706,c_1728,c_1921,c_2210,c_2515,c_2618,c_2620,c_2769,c_3065,c_3382,c_3460,c_3472,c_3697,c_3755,c_4320,c_6402]) ).
tcf(c_6525,plain,
( product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_2)
| product(e_4,e_5,e_1) ),
inference(renaming,[status(thm)],[c_6524]) ).
tcf(c_6526,plain,
( product(e_6,e_5,e_2)
| product(e_4,e_5,e_1)
| product(e_4,e_5,e_2)
| product(e_4,e_5,e_4)
| product(e_5,e_6,e_1)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_6525,c_138,c_134,c_133,c_175,c_164,c_147,c_143,c_142,c_139,c_404,c_408,c_412,c_420,c_424,c_455,c_516,c_524,c_539,c_1630,c_1654,c_1668,c_1705,c_1706,c_1921,c_2210,c_2420,c_2618,c_2620,c_2769,c_3065,c_3460,c_3472,c_3697,c_3755,c_6210,c_6525]) ).
tcf(c_6527,plain,
( product(e_6,e_5,e_2)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_2)
| product(e_4,e_5,e_1) ),
inference(renaming,[status(thm)],[c_6526]) ).
tcf(c_6571,plain,
( equalish(e_2,e_4)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_2)
| product(e_4,e_5,e_1) ),
inference(resolution,[status(thm)],[c_6527,c_3144]) ).
tcf(c_6644,plain,
( product(e_4,e_5,e_1)
| product(e_5,e_6,e_1)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_3)
| product(e_6,e_5,e_1)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_6571,c_138,c_137,c_134,c_133,c_175,c_164,c_147,c_143,c_142,c_139,c_404,c_408,c_412,c_420,c_424,c_455,c_524,c_539,c_1630,c_1654,c_1668,c_1705,c_1706,c_1921,c_2210,c_2618,c_2620,c_2769,c_3065,c_3460,c_3472,c_3697,c_3755,c_6402]) ).
tcf(c_6645,plain,
( product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_5,e_1) ),
inference(renaming,[status(thm)],[c_6644]) ).
tcf(c_6646,plain,
( product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_4,e_5,e_1) ),
inference(global_subsumption_just,[status(thm)],[c_6645,c_134,c_133,c_175,c_163,c_153,c_152,c_148,c_147,c_143,c_142,c_139,c_404,c_408,c_412,c_455,c_524,c_539,c_547,c_1630,c_1668,c_1705,c_1706,c_1922,c_2210,c_2420,c_3146,c_3150,c_3472,c_3589,c_3591,c_3755,c_3779,c_5182,c_5277,c_6645]) ).
tcf(c_6663,plain,
( equalish(e_2,e_3)
| product(e_4,e_3,e_5)
| product(e_4,e_3,e_3)
| product(e_4,e_3,e_2)
| product(e_3,e_2,e_5)
| product(e_3,e_2,e_4)
| product(e_3,e_1,e_2) ),
inference(superposition,[status(thm)],[c_6313,c_6137]) ).
tcf(c_6708,plain,
! [X0: $i] :
( equalish(X0,e_6)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_4,e_5,e_1)
| ~ product(X0,e_5,e_3) ),
inference(resolution,[status(thm)],[c_6646,c_172]) ).
tcf(c_6709,plain,
( equalish(e_1,e_6)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_4,e_5,e_1)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_6708]) ).
tcf(c_6714,plain,
( equalish(e_5,e_4)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_4)
| product(e_4,e_5,e_1) ),
inference(resolution,[status(thm)],[c_6646,c_5575]) ).
tcf(c_6719,plain,
( equalish(e_3,e_2)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_4)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_4,e_5,e_1)
| product(e_3,e_6,e_5) ),
inference(resolution,[status(thm)],[c_6646,c_5649]) ).
tcf(c_6720,plain,
( product(e_4,e_1,e_5)
| product(e_4,e_1,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_4432,c_134,c_133,c_175,c_146,c_141,c_139,c_404,c_408,c_412,c_424,c_455,c_501,c_1630,c_1668,c_1693,c_1694,c_2210,c_3324,c_3713]) ).
tcf(c_6724,plain,
! [X0: $i] :
( equalish(e_4,X0)
| product(e_4,e_1,e_2)
| ~ product(X0,e_1,e_5) ),
inference(superposition,[status(thm)],[c_6720,c_172]) ).
tcf(c_6726,plain,
! [X0: $i] :
( product(e_4,e_1,e_2)
| product(X0,e_4,e_1)
| ~ product(e_5,e_4,X0) ),
inference(superposition,[status(thm)],[c_6720,c_174]) ).
tcf(c_6841,plain,
( product(e_3,e_3,e_1)
| ~ product(e_4,e_3,e_3)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_3698]) ).
tcf(c_6868,plain,
( product(e_4,e_1,e_6)
| ~ product(e_5,e_1,e_4)
| ~ product(e_1,e_6,e_5) ),
inference(instantiation,[status(thm)],[c_1519]) ).
tcf(c_6902,plain,
( product(e_5,e_1,e_5)
| ~ product(e_4,e_1,e_5)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_4076]) ).
tcf(c_6911,plain,
( product(e_4,e_6,e_2)
| ~ product(e_6,e_2,e_1)
| ~ product(e_1,e_6,e_4) ),
inference(instantiation,[status(thm)],[c_4860]) ).
tcf(c_6913,plain,
( product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_4)
| product(e_4,e_5,e_1)
| product(e_6,e_5,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_6719,c_138,c_134,c_133,c_175,c_164,c_162,c_147,c_143,c_142,c_139,c_404,c_408,c_412,c_420,c_424,c_455,c_516,c_524,c_539,c_1630,c_1654,c_1668,c_1705,c_1706,c_1921,c_2210,c_2420,c_2618,c_2620,c_2769,c_3065,c_3460,c_3472,c_3697,c_3755,c_6210,c_6714]) ).
tcf(c_6914,plain,
( product(e_6,e_5,e_2)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_4)
| product(e_4,e_5,e_1) ),
inference(renaming,[status(thm)],[c_6913]) ).
tcf(c_6934,plain,
! [X0: $i] :
( equalish(X0,e_2)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_4)
| product(e_4,e_5,e_1)
| ~ product(e_6,e_5,X0) ),
inference(resolution,[status(thm)],[c_6914,c_170]) ).
tcf(c_6966,plain,
! [X0: $i] :
( product(e_2,X0,e_2)
| ~ product(e_6,X0,e_2)
| ~ product(X0,e_2,e_6) ),
inference(instantiation,[status(thm)],[c_3602]) ).
tcf(c_6987,plain,
( product(e_2,e_1,e_2)
| ~ product(e_6,e_1,e_2)
| ~ product(e_1,e_2,e_6) ),
inference(instantiation,[status(thm)],[c_6966]) ).
tcf(c_7142,plain,
( product(e_4,e_1,e_5)
| ~ product(e_3,e_1,e_4)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_3700]) ).
tcf(c_7258,plain,
( equalish(e_4,e_2)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_4)
| product(e_4,e_5,e_1) ),
inference(resolution,[status(thm)],[c_6934,c_3142]) ).
tcf(c_7357,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_1616]) ).
tcf(c_7362,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_1579]) ).
tcf(c_7366,plain,
! [X0: $i] :
( product(e_5,e_1,X0)
| ~ product(e_6,e_1,e_5)
| ~ product(e_1,X0,e_6) ),
inference(instantiation,[status(thm)],[c_1723]) ).
tcf(c_7417,plain,
( product(e_2,e_5,e_1)
| ~ product(e_6,e_5,e_2)
| ~ product(e_5,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_3602]) ).
tcf(c_7419,plain,
( equalish(e_6,e_4)
| ~ product(e_5,e_1,e_6)
| ~ product(e_5,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_1614]) ).
tcf(c_7421,plain,
( equalish(e_6,e_2)
| ~ product(e_5,e_1,e_6)
| ~ product(e_5,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1605]) ).
tcf(c_7430,plain,
( product(e_4,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_6,e_5,e_1)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_7258,c_138,c_137,c_134,c_133,c_175,c_164,c_158,c_153,c_152,c_151,c_148,c_147,c_146,c_143,c_142,c_141,c_139,c_404,c_408,c_412,c_424,c_455,c_501,c_524,c_547,c_1630,c_1648,c_1668,c_1693,c_1694,c_1705,c_1706,c_1922,c_2210,c_3146,c_3276,c_3324,c_3453,c_3472,c_3589,c_3713,c_3755,c_3779,c_5277,c_6402,c_6646,c_7362]) ).
tcf(c_7431,plain,
( product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_4,e_5,e_1) ),
inference(renaming,[status(thm)],[c_7430]) ).
tcf(c_7432,plain,
! [X0: $i] :
( equalish(X0,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_4,e_5,e_1)
| ~ product(e_6,e_5,X0) ),
inference(resolution,[status(thm)],[c_7431,c_170]) ).
tcf(c_7433,plain,
! [X0: $i] :
( equalish(X0,e_5)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_4,e_5,e_1)
| ~ product(e_6,X0,e_3) ),
inference(resolution,[status(thm)],[c_7431,c_171]) ).
tcf(c_7435,plain,
! [X0: $i] :
( equalish(X0,e_6)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_4,e_5,e_1)
| ~ product(X0,e_5,e_3) ),
inference(resolution,[status(thm)],[c_7431,c_172]) ).
tcf(c_7436,plain,
( equalish(e_1,e_6)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_4,e_5,e_1)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_7435]) ).
tcf(c_7437,plain,
! [X0: $i] :
( product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_4,e_5,e_1)
| product(e_3,e_5,X0)
| ~ product(e_5,X0,e_6) ),
inference(resolution,[status(thm)],[c_7431,c_174]) ).
tcf(c_7438,plain,
( product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_4,e_5,e_1)
| product(e_3,e_5,e_1)
| ~ product(e_5,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_7437]) ).
tcf(c_7480,plain,
( product(e_6,e_4,e_1)
| 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)
| product(e_4,e_1,e_2)
| ~ group_element(e_5)
| ~ group_element(e_4) ),
inference(superposition,[status(thm)],[c_169,c_6726]) ).
tcf(c_7512,plain,
! [X0: $i] :
( equalish(e_5,e_4)
| ~ product(X0,e_5,e_6)
| ~ product(X0,e_4,e_6) ),
inference(instantiation,[status(thm)],[c_1592]) ).
tcf(c_7514,plain,
! [X0: $i] :
( equalish(e_5,e_2)
| ~ product(X0,e_5,e_6)
| ~ product(X0,e_2,e_6) ),
inference(instantiation,[status(thm)],[c_1585]) ).
tcf(c_7516,plain,
! [X0: $i] :
( equalish(e_4,e_5)
| ~ product(X0,e_5,e_6)
| ~ product(X0,e_4,e_6) ),
inference(instantiation,[status(thm)],[c_1575]) ).
tcf(c_7522,plain,
( equalish(e_4,e_5)
| ~ product(e_1,e_5,e_6)
| ~ product(e_1,e_4,e_6) ),
inference(instantiation,[status(thm)],[c_7516]) ).
tcf(c_7523,plain,
( equalish(e_5,e_2)
| ~ product(e_1,e_5,e_6)
| ~ product(e_1,e_2,e_6) ),
inference(instantiation,[status(thm)],[c_7514]) ).
tcf(c_7525,plain,
( equalish(e_5,e_4)
| ~ product(e_1,e_5,e_6)
| ~ product(e_1,e_4,e_6) ),
inference(instantiation,[status(thm)],[c_7512]) ).
tcf(c_7550,plain,
! [X0: $i,X1: $i] :
( product(e_6,e_5,X0)
| ~ product(X1,e_5,e_6)
| ~ product(e_5,X0,X1) ),
inference(instantiation,[status(thm)],[c_1742]) ).
tcf(c_7609,plain,
( product(e_3,e_5,e_1)
| ~ product(e_6,e_5,e_3)
| ~ product(e_5,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_3389]) ).
tcf(c_7652,plain,
( equalish(e_2,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_2)
| product(e_4,e_5,e_1) ),
inference(resolution,[status(thm)],[c_7432,c_6527]) ).
tcf(c_7826,plain,
( product(e_4,e_5,e_1)
| product(e_4,e_5,e_4)
| product(e_5,e_6,e_1)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_3)
| product(e_6,e_5,e_1)
| product(e_6,e_5,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_7652,c_138,c_137,c_134,c_133,c_175,c_168,c_164,c_163,c_159,c_158,c_147,c_146,c_143,c_142,c_141,c_139,c_404,c_408,c_412,c_416,c_420,c_424,c_455,c_501,c_516,c_524,c_539,c_1630,c_1651,c_1654,c_1668,c_1693,c_1694,c_1705,c_1706,c_1921,c_2210,c_2420,c_2486,c_2618,c_2620,c_2770,c_2769,c_3065,c_3284,c_3295,c_3302,c_3324,c_3460,c_3472,c_3599,c_3697,c_3713,c_3755,c_3794,c_4983,c_5815,c_6222,c_6525,c_6709,c_6902,c_7362,c_7438]) ).
tcf(c_7827,plain,
( product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_1) ),
inference(renaming,[status(thm)],[c_7826]) ).
tcf(c_7828,plain,
( product(e_6,e_5,e_2)
| product(e_4,e_5,e_1)
| product(e_4,e_5,e_4)
| product(e_5,e_6,e_1)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_7827,c_138,c_134,c_133,c_175,c_164,c_147,c_143,c_142,c_139,c_404,c_408,c_412,c_420,c_424,c_455,c_516,c_524,c_539,c_1630,c_1654,c_1668,c_1705,c_1706,c_1921,c_2210,c_2420,c_2618,c_2620,c_2769,c_3065,c_3460,c_3472,c_3697,c_3755,c_6210,c_7827]) ).
tcf(c_7829,plain,
( product(e_6,e_5,e_2)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_1) ),
inference(renaming,[status(thm)],[c_7828]) ).
tcf(c_7857,plain,
( equalish(e_2,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_1)
| product(e_3,e_6,e_5) ),
inference(resolution,[status(thm)],[c_7829,c_3888]) ).
tcf(c_7860,plain,
( equalish(e_2,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_1) ),
inference(resolution,[status(thm)],[c_7829,c_7432]) ).
tcf(c_7869,plain,
( product(e_5,e_1,e_6)
| ~ product(e_4,e_1,e_5)
| ~ product(e_1,e_6,e_4) ),
inference(instantiation,[status(thm)],[c_5232]) ).
tcf(c_7909,plain,
! [X0: $i] :
( product(e_2,e_5,X0)
| ~ product(e_6,e_5,e_2)
| ~ product(e_5,X0,e_6) ),
inference(instantiation,[status(thm)],[c_3602]) ).
tcf(c_7912,plain,
! [X0: $i] :
( equalish(e_6,e_3)
| ~ product(e_5,X0,e_6)
| ~ product(e_5,X0,e_3) ),
inference(instantiation,[status(thm)],[c_1610]) ).
tcf(c_7921,plain,
! [X0: $i,X1: $i] :
( product(e_6,X0,X1)
| ~ product(e_5,X0,e_6)
| ~ product(X0,X1,e_5) ),
inference(instantiation,[status(thm)],[c_1742]) ).
tcf(c_7938,plain,
( equalish(e_4,e_6)
| product(e_6,e_1,e_4)
| product(e_6,e_1,e_2)
| product(e_4,e_1,e_2) ),
inference(superposition,[status(thm)],[c_6222,c_6724]) ).
tcf(c_7987,plain,
( equalish(e_6,e_4)
| product(e_6,e_1,e_4)
| product(e_6,e_1,e_2)
| product(e_4,e_1,e_2) ),
inference(superposition,[status(thm)],[c_6720,c_6225]) ).
tcf(c_8115,plain,
( product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_4,e_5,e_1)
| product(e_6,e_5,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_7857,c_138,c_137,c_134,c_133,c_175,c_168,c_164,c_147,c_146,c_143,c_142,c_141,c_139,c_404,c_408,c_412,c_416,c_420,c_424,c_455,c_501,c_516,c_524,c_539,c_1630,c_1651,c_1654,c_1668,c_1693,c_1694,c_1705,c_1706,c_1726,c_1921,c_2210,c_2486,c_2618,c_2620,c_2622,c_2770,c_2769,c_3065,c_3302,c_3324,c_3460,c_3472,c_3599,c_3697,c_3713,c_3755,c_3794,c_5815,c_6210,c_6222,c_6709,c_6902,c_7438]) ).
tcf(c_8116,plain,
( product(e_6,e_5,e_2)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_4,e_5,e_1) ),
inference(renaming,[status(thm)],[c_8115]) ).
tcf(c_8117,plain,
( product(e_6,e_5,e_2)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_4,e_5,e_1)
| product(e_4,e_6,e_1)
| product(e_4,e_6,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_8116,c_138,c_137,c_134,c_133,c_175,c_163,c_158,c_153,c_152,c_151,c_148,c_147,c_146,c_143,c_142,c_141,c_139,c_404,c_408,c_412,c_416,c_424,c_455,c_501,c_516,c_524,c_539,c_547,c_1630,c_1648,c_1651,c_1661,c_1668,c_1693,c_1694,c_1705,c_1706,c_1726,c_1727,c_1728,c_1922,c_2210,c_2486,c_2770,c_3276,c_3302,c_3324,c_3472,c_3589,c_3591,c_3599,c_3713,c_3755,c_3779,c_3794,c_5277,c_6210,c_6256,c_6270,c_6902,c_7362,c_7436,c_8116]) ).
tcf(c_8118,plain,
( product(e_6,e_5,e_2)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_4,e_5,e_1) ),
inference(renaming,[status(thm)],[c_8117]) ).
tcf(c_8140,plain,
! [X0: $i] :
( equalish(X0,e_2)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_4,e_5,e_1)
| ~ product(e_6,e_5,X0) ),
inference(resolution,[status(thm)],[c_8118,c_170]) ).
tcf(c_8141,plain,
( equalish(e_1,e_2)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_4,e_5,e_1)
| ~ product(e_6,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_8140]) ).
tcf(c_8142,plain,
! [X0: $i] :
( equalish(X0,e_5)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_4,e_5,e_1)
| ~ product(e_6,X0,e_2) ),
inference(resolution,[status(thm)],[c_8118,c_171]) ).
tcf(c_8143,plain,
( equalish(e_1,e_5)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_4,e_5,e_1)
| ~ product(e_6,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_8142]) ).
tcf(c_8199,plain,
( equalish(e_5,e_3)
| ~ product(e_3,e_5,e_3)
| ~ product(e_3,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_3361]) ).
tcf(c_8298,plain,
( equalish(e_1,e_3)
| ~ product(e_3,e_2,e_5)
| ~ product(e_1,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_1525]) ).
tcf(c_8313,plain,
! [X0: $i] :
( product(e_5,e_2,X0)
| ~ product(e_3,e_2,e_5)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_2772]) ).
tcf(c_8314,plain,
( product(e_5,e_2,e_1)
| ~ product(e_3,e_2,e_5)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_8313]) ).
tcf(c_8470,plain,
( product(e_4,e_5,e_4)
| product(e_4,e_5,e_1)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_3)
| product(e_6,e_5,e_1)
| product(e_6,e_5,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_7860,c_137,c_134,c_133,c_175,c_163,c_162,c_158,c_153,c_152,c_148,c_147,c_146,c_143,c_142,c_141,c_139,c_404,c_408,c_412,c_416,c_424,c_455,c_501,c_516,c_524,c_539,c_547,c_1630,c_1651,c_1668,c_1693,c_1694,c_1705,c_1706,c_1922,c_2210,c_2420,c_2486,c_2770,c_3146,c_3150,c_3295,c_3302,c_3324,c_3382,c_3472,c_3589,c_3591,c_3599,c_3713,c_3755,c_3779,c_3794,c_4290,c_5182,c_5277,c_6256,c_6251,c_6645,c_6902,c_7436,c_7829]) ).
tcf(c_8471,plain,
( product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_1) ),
inference(renaming,[status(thm)],[c_8470]) ).
tcf(c_8472,plain,
( product(e_6,e_5,e_2)
| product(e_4,e_5,e_1)
| product(e_4,e_5,e_4)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_8471,c_138,c_137,c_135,c_134,c_133,c_175,c_164,c_163,c_162,c_159,c_158,c_152,c_148,c_147,c_146,c_145,c_144,c_143,c_142,c_141,c_140,c_139,c_404,c_408,c_412,c_416,c_420,c_424,c_447,c_455,c_478,c_501,c_516,c_524,c_539,c_1629,c_1630,c_1651,c_1654,c_1668,c_1682,c_1683,c_1693,c_1694,c_1705,c_1706,c_1921,c_2210,c_2229,c_2253,c_2420,c_2486,c_2770,c_2769,c_2773,c_3065,c_3284,c_3295,c_3294,c_3302,c_3324,c_3382,c_3442,c_3453,c_3472,c_3599,c_3697,c_3713,c_3755,c_3794,c_4290,c_4751,c_4971,c_4983,c_5820,c_6090,c_6195,c_6210,c_6251,c_6267,c_6444,c_6868,c_6902,c_7431,c_7436,c_7438,c_7829,c_7869,c_7938,c_8141,c_8314,c_8471]) ).
tcf(c_8473,plain,
( product(e_6,e_5,e_2)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_1) ),
inference(renaming,[status(thm)],[c_8472]) ).
tcf(c_8626,plain,
( product(e_1,e_4,e_5)
| ~ product(e_4,e_5,e_2)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_5092]) ).
tcf(c_8635,plain,
! [X0: $i] :
( product(e_2,e_5,X0)
| ~ product(e_4,e_5,e_2)
| ~ product(e_5,X0,e_4) ),
inference(instantiation,[status(thm)],[c_3305]) ).
tcf(c_8636,plain,
( product(e_2,e_5,e_1)
| ~ product(e_5,e_1,e_4)
| ~ product(e_4,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_8635]) ).
tcf(c_8751,plain,
( equalish(e_6,e_4)
| ~ product(e_5,e_6,e_3)
| ~ product(e_5,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_3502]) ).
tcf(c_8754,plain,
( equalish(e_3,e_1)
| ~ product(e_5,e_6,e_3)
| ~ product(e_5,e_6,e_1) ),
inference(instantiation,[status(thm)],[c_3491]) ).
tcf(c_8756,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,X0)
| ~ product(X0,X0,X1) ),
inference(superposition,[status(thm)],[c_173,c_174]) ).
tcf(c_8760,plain,
! [X0: $i,X1: $i] :
( equalish(X1,X0)
| ~ product(X0,X1,X1) ),
inference(superposition,[status(thm)],[c_173,c_172]) ).
tcf(c_8764,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X0,X2,e_5)
| product(X0,X2,e_4)
| product(X0,X2,e_3)
| product(X0,X2,e_2)
| product(X0,X2,e_1)
| product(X1,X0,X2)
| ~ group_element(X2)
| ~ group_element(X0)
| ~ product(e_6,X0,X1) ),
inference(superposition,[status(thm)],[c_169,c_174]) ).
tcf(c_8844,plain,
! [X0: $i] :
( product(e_6,e_6,X0)
| 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(superposition,[status(thm)],[c_173,c_8764]) ).
tcf(c_9093,plain,
! [X0: $i] :
( product(e_6,e_6,X0)
| 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(X0) ),
inference(global_subsumption_just,[status(thm)],[c_8844,c_5140]) ).
tcf(c_9104,plain,
! [X0: $i] :
( 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)
| product(X0,e_6,e_6)
| ~ group_element(X0) ),
inference(superposition,[status(thm)],[c_9093,c_8756]) ).
tcf(c_9365,plain,
( product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_4,e_6,e_2)
| 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) ),
inference(global_subsumption_just,[status(thm)],[c_6331,c_137,c_134,c_133,c_175,c_166,c_163,c_160,c_158,c_152,c_151,c_147,c_146,c_143,c_142,c_141,c_139,c_404,c_408,c_412,c_416,c_424,c_455,c_501,c_516,c_524,c_1630,c_1651,c_1668,c_1693,c_1694,c_1705,c_1706,c_1726,c_2210,c_2486,c_2770,c_3066,c_3150,c_3276,c_3302,c_3324,c_3385,c_3472,c_3481,c_3591,c_3713,c_3755,c_4290,c_4972,c_5223,c_5277,c_6210,c_6902,c_7142,c_7938]) ).
tcf(c_9367,plain,
( product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_4,e_5,e_1)
| product(e_4,e_5,e_2)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_4) ),
inference(global_subsumption_just,[status(thm)],[c_9365,c_137,c_134,c_133,c_175,c_166,c_164,c_163,c_158,c_152,c_151,c_147,c_146,c_143,c_142,c_141,c_139,c_404,c_408,c_412,c_416,c_424,c_455,c_501,c_516,c_524,c_1630,c_1651,c_1668,c_1693,c_1694,c_1705,c_1706,c_2210,c_2486,c_2770,c_3066,c_3276,c_3294,c_3324,c_3385,c_3472,c_3481,c_3591,c_3713,c_3755,c_4290,c_4972,c_5277,c_6402,c_6902,c_7938,c_9365]) ).
tcf(c_9368,plain,
( product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| 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) ),
inference(renaming,[status(thm)],[c_9367]) ).
tcf(c_9394,plain,
! [X0: $i] :
( equalish(X0,e_5)
| product(e_6,e_5,e_1)
| 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)
| ~ product(e_6,X0,e_2) ),
inference(resolution,[status(thm)],[c_9368,c_171]) ).
tcf(c_9395,plain,
( equalish(e_1,e_5)
| product(e_6,e_5,e_1)
| 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)
| ~ product(e_6,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_9394]) ).
tcf(c_9398,plain,
! [X0: $i] :
( product(e_6,e_5,e_1)
| 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)
| product(e_2,e_5,X0)
| ~ product(e_5,X0,e_6) ),
inference(resolution,[status(thm)],[c_9368,c_174]) ).
tcf(c_9399,plain,
( product(e_6,e_5,e_1)
| 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)
| product(e_2,e_5,e_1)
| ~ product(e_5,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_9398]) ).
tcf(c_9412,plain,
( equalish(e_2,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| 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) ),
inference(resolution,[status(thm)],[c_9368,c_7432]) ).
tcf(c_9461,plain,
( product(e_2,e_1,e_5)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| ~ group_element(e_2)
| ~ group_element(e_1) ),
inference(superposition,[status(thm)],[c_169,c_412]) ).
tcf(c_9469,plain,
( product(e_4,e_1,e_5)
| product(e_4,e_1,e_4)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| ~ group_element(e_4)
| ~ group_element(e_1) ),
inference(superposition,[status(thm)],[c_169,c_424]) ).
tcf(c_9508,plain,
( product(e_4,e_1,e_5)
| product(e_4,e_1,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_9469,c_134,c_133,c_175,c_146,c_141,c_139,c_404,c_408,c_412,c_424,c_455,c_501,c_1630,c_1668,c_1693,c_1694,c_2210,c_3324,c_3713]) ).
tcf(c_9513,plain,
! [X0: $i] :
( product(e_4,e_1,e_2)
| product(X0,e_4,e_1)
| ~ product(e_5,e_4,X0) ),
inference(superposition,[status(thm)],[c_9508,c_174]) ).
tcf(c_9539,plain,
( product(e_6,e_4,e_1)
| 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)
| product(e_4,e_1,e_2)
| ~ group_element(e_5)
| ~ group_element(e_4) ),
inference(superposition,[status(thm)],[c_169,c_9513]) ).
tcf(c_9617,plain,
( product(e_4,e_5,e_1)
| product(e_4,e_5,e_4)
| product(e_5,e_6,e_3)
| product(e_6,e_5,e_1)
| product(e_6,e_5,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_9412,c_137,c_134,c_133,c_175,c_164,c_163,c_159,c_158,c_147,c_146,c_143,c_142,c_141,c_139,c_404,c_408,c_412,c_416,c_424,c_455,c_501,c_516,c_524,c_539,c_1630,c_1651,c_1668,c_1693,c_1694,c_1705,c_1706,c_2210,c_2420,c_2486,c_2770,c_3284,c_3295,c_3302,c_3324,c_3382,c_3453,c_3599,c_3713,c_3755,c_3794,c_4290,c_4971,c_4983,c_5820,c_6902,c_7431,c_7436,c_7438,c_7938,c_8471]) ).
tcf(c_9618,plain,
( product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_1) ),
inference(renaming,[status(thm)],[c_9617]) ).
tcf(c_9619,plain,
( product(e_6,e_5,e_2)
| product(e_4,e_5,e_1)
| product(e_4,e_5,e_4)
| product(e_5,e_6,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_9618,c_138,c_137,c_135,c_134,c_133,c_175,c_164,c_161,c_151,c_147,c_146,c_142,c_141,c_140,c_139,c_404,c_408,c_412,c_416,c_420,c_424,c_455,c_478,c_501,c_516,c_524,c_539,c_1630,c_1654,c_1668,c_1682,c_1683,c_1693,c_1694,c_1705,c_1706,c_1726,c_1921,c_2210,c_2253,c_2769,c_3065,c_3276,c_3324,c_3453,c_3472,c_3697,c_3713,c_3755,c_5279,c_6210,c_6868,c_7869,c_8473,c_9618]) ).
tcf(c_9620,plain,
( product(e_6,e_5,e_2)
| product(e_5,e_6,e_3)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_1) ),
inference(renaming,[status(thm)],[c_9619]) ).
tcf(c_9645,plain,
! [X0: $i] :
( equalish(X0,e_5)
| product(e_5,e_6,e_3)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_1)
| ~ product(e_6,X0,e_2) ),
inference(resolution,[status(thm)],[c_9620,c_171]) ).
tcf(c_9646,plain,
( equalish(e_1,e_5)
| product(e_5,e_6,e_3)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_1)
| ~ product(e_6,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_9645]) ).
tcf(c_9730,plain,
( equalish(e_5,e_3)
| ~ product(e_5,e_3,e_3)
| ~ product(e_3,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_4393]) ).
tcf(c_9913,plain,
( equalish(e_5,e_6)
| product(e_6,e_5,e_4)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_6)
| ~ group_element(e_5) ),
inference(superposition,[status(thm)],[c_9104,c_8760]) ).
tcf(c_9922,plain,
( equalish(e_6,e_4)
| ~ product(e_6,e_4,e_4)
| ~ product(e_4,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_4960]) ).
tcf(c_10106,plain,
( equalish(e_5,e_4)
| ~ product(e_4,e_4,e_5)
| ~ product(e_4,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_5210]) ).
tcf(c_10164,plain,
( equalish(e_5,e_4)
| ~ product(e_5,e_4,e_4)
| ~ product(e_4,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_5269]) ).
tcf(c_10240,plain,
( equalish(e_3,e_1)
| ~ product(e_4,e_3,e_5)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_5486]) ).
tcf(c_10366,plain,
( equalish(e_6,e_4)
| ~ product(e_4,e_6,e_4)
| ~ product(e_4,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_5543]) ).
tcf(c_10441,plain,
product(e_2,e_1,e_3),
inference(global_subsumption_just,[status(thm)],[c_9461,c_134,c_133,c_175,c_139,c_404,c_408,c_412,c_455,c_1630,c_1668,c_2210]) ).
tcf(c_10446,plain,
! [X0: $i] :
( product(X0,e_2,e_1)
| ~ product(e_3,e_2,X0) ),
inference(superposition,[status(thm)],[c_10441,c_174]) ).
tcf(c_10450,plain,
( product(e_6,e_2,e_1)
| 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(superposition,[status(thm)],[c_169,c_10446]) ).
tcf(c_10482,plain,
( product(e_5,e_1,e_5)
| ~ product(e_6,e_1,e_5)
| ~ product(e_1,e_5,e_6) ),
inference(instantiation,[status(thm)],[c_7366]) ).
tcf(c_10650,plain,
( product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| 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) ),
inference(global_subsumption_just,[status(thm)],[c_6155,c_138,c_137,c_134,c_133,c_175,c_168,c_167,c_166,c_164,c_152,c_151,c_149,c_148,c_147,c_146,c_143,c_142,c_141,c_140,c_139,c_404,c_408,c_412,c_416,c_455,c_516,c_524,c_539,c_547,c_1630,c_1648,c_1651,c_1668,c_1683,c_1705,c_1706,c_1726,c_1922,c_2210,c_2226,c_2486,c_2770,c_3066,c_3276,c_3294,c_3292,c_3472,c_3481,c_3713,c_3755,c_3779,c_4290,c_4611,c_4615,c_4972,c_5277,c_5322,c_6194,c_6210,c_6231,c_6313,c_6841,c_6902,c_7987,c_8754,c_9395,c_9399,c_9646,c_10240]) ).
tcf(c_10652,plain,
( product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_1) ),
inference(global_subsumption_just,[status(thm)],[c_10650,c_138,c_137,c_136,c_134,c_133,c_175,c_167,c_162,c_159,c_157,c_153,c_148,c_146,c_143,c_142,c_141,c_139,c_404,c_408,c_412,c_416,c_455,c_493,c_516,c_547,c_1630,c_1645,c_1648,c_1651,c_1668,c_1694,c_1705,c_1706,c_1922,c_2210,c_2444,c_2475,c_2486,c_2770,c_3067,c_3066,c_3284,c_3472,c_3481,c_3488,c_3713,c_3779,c_3932,c_4969,c_5208,c_5305,c_5307,c_6902,c_7480,c_7522,c_8626,c_8751,c_9646,c_9922,c_10164,c_10650]) ).
tcf(c_10654,plain,
( product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_5,e_1)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_4) ),
inference(global_subsumption_just,[status(thm)],[c_10652,c_137,c_136,c_134,c_133,c_175,c_167,c_162,c_159,c_158,c_157,c_146,c_143,c_142,c_141,c_139,c_404,c_408,c_412,c_416,c_455,c_493,c_516,c_539,c_1630,c_1645,c_1651,c_1668,c_1694,c_1705,c_1706,c_2210,c_2444,c_2475,c_2486,c_2770,c_3166,c_3373,c_3481,c_3488,c_3590,c_3600,c_3599,c_3713,c_4983,c_5305,c_5307,c_6222,c_6902,c_7480,c_8751,c_9646,c_9922,c_10164,c_10652]) ).
tcf(c_10655,plain,
( product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_1) ),
inference(renaming,[status(thm)],[c_10654]) ).
tcf(c_10656,plain,
( product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_1)
| product(e_4,e_5,e_1)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_4) ),
inference(global_subsumption_just,[status(thm)],[c_10655,c_137,c_134,c_133,c_175,c_168,c_167,c_166,c_164,c_161,c_149,c_146,c_142,c_141,c_140,c_139,c_404,c_408,c_412,c_416,c_455,c_516,c_1630,c_1651,c_1668,c_1683,c_1694,c_1705,c_1706,c_2210,c_2226,c_2486,c_2770,c_3066,c_3294,c_3292,c_3290,c_3472,c_3481,c_3713,c_4290,c_4972,c_5305,c_6190,c_6222,c_6313,c_6841,c_6902,c_9395,c_9922,c_10240,c_10655]) ).
tcf(c_10657,plain,
( product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_1)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_1) ),
inference(renaming,[status(thm)],[c_10656]) ).
tcf(c_10658,plain,
( product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_4,e_5,e_1)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_4) ),
inference(global_subsumption_just,[status(thm)],[c_10657,c_138,c_137,c_134,c_133,c_175,c_168,c_167,c_164,c_157,c_153,c_152,c_149,c_148,c_146,c_143,c_142,c_141,c_139,c_404,c_408,c_412,c_416,c_455,c_516,c_547,c_1630,c_1648,c_1651,c_1668,c_1694,c_1705,c_1706,c_1922,c_2210,c_2486,c_2770,c_3066,c_3294,c_3290,c_3472,c_3481,c_3713,c_3779,c_3794,c_4290,c_4969,c_5305,c_6256,c_6255,c_6902,c_8754,c_9646,c_9922,c_10657]) ).
tcf(c_10659,plain,
( product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_1) ),
inference(renaming,[status(thm)],[c_10658]) ).
tcf(c_10777,plain,
! [X0: $i] :
( product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_1)
| product(e_3,e_4,X0)
| ~ product(e_4,X0,e_6) ),
inference(resolution,[status(thm)],[c_10659,c_174]) ).
tcf(c_10915,plain,
( product(e_6,e_2,e_1)
| product(e_3,e_2,e_5)
| product(e_3,e_2,e_4) ),
inference(global_subsumption_just,[status(thm)],[c_10450,c_135,c_134,c_133,c_175,c_145,c_139,c_404,c_408,c_412,c_447,c_455,c_1629,c_1630,c_1668,c_1683,c_2210,c_2229,c_2773,c_4751,c_6090]) ).
tcf(c_10920,plain,
! [X0: $i] :
( product(e_3,e_2,e_5)
| product(e_3,e_2,e_4)
| product(X0,e_6,e_2)
| ~ product(e_1,e_6,X0) ),
inference(superposition,[status(thm)],[c_10915,c_174]) ).
tcf(c_10981,plain,
( product(e_6,e_6,e_2)
| 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)
| product(e_3,e_2,e_5)
| product(e_3,e_2,e_4)
| ~ group_element(e_1) ),
inference(superposition,[status(thm)],[c_9104,c_10920]) ).
tcf(c_11072,plain,
( equalish(e_4,e_1)
| ~ product(e_6,e_4,e_2)
| ~ product(e_6,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_3157]) ).
tcf(c_11091,plain,
( product(e_6,e_4,e_1)
| product(e_5,e_4,e_3)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_1) ),
inference(global_subsumption_just,[status(thm)],[c_9539,c_138,c_137,c_136,c_134,c_133,c_175,c_167,c_162,c_158,c_157,c_156,c_153,c_151,c_148,c_146,c_143,c_142,c_141,c_139,c_404,c_408,c_412,c_416,c_424,c_455,c_493,c_501,c_516,c_547,c_1630,c_1648,c_1651,c_1661,c_1668,c_1693,c_1694,c_1705,c_1706,c_1727,c_1728,c_1922,c_2210,c_2475,c_2486,c_2770,c_3276,c_3279,c_3302,c_3324,c_3472,c_3488,c_3589,c_3595,c_3713,c_3779,c_4969,c_6902,c_7142,c_7362,c_7480,c_10164,c_10482]) ).
tcf(c_11093,plain,
( product(e_6,e_4,e_1)
| product(e_5,e_4,e_3)
| product(e_5,e_4,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_11091,c_138,c_137,c_136,c_134,c_133,c_175,c_167,c_162,c_158,c_157,c_156,c_153,c_151,c_148,c_146,c_143,c_142,c_141,c_139,c_404,c_408,c_412,c_416,c_424,c_455,c_493,c_501,c_516,c_547,c_1630,c_1648,c_1651,c_1661,c_1668,c_1693,c_1694,c_1705,c_1706,c_1727,c_1728,c_1922,c_2210,c_2475,c_2486,c_2770,c_3276,c_3279,c_3302,c_3324,c_3472,c_3488,c_3589,c_3595,c_3713,c_3779,c_4969,c_6902,c_7142,c_7362,c_7480,c_10164,c_10482]) ).
tcf(c_11168,plain,
( product(e_6,e_1,e_4)
| product(e_6,e_1,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_10981,c_138,c_137,c_134,c_133,c_175,c_158,c_153,c_151,c_148,c_146,c_143,c_142,c_141,c_139,c_404,c_408,c_412,c_416,c_424,c_455,c_501,c_516,c_547,c_1630,c_1648,c_1651,c_1661,c_1668,c_1693,c_1694,c_1705,c_1706,c_1727,c_1728,c_1922,c_2210,c_2486,c_2770,c_3276,c_3302,c_3324,c_3472,c_3589,c_3713,c_3779,c_6902,c_7142,c_7362,c_10482]) ).
tcf(c_11173,plain,
! [X0: $i] :
( product(e_6,e_1,e_2)
| product(X0,e_6,e_1)
| ~ product(e_4,e_6,X0) ),
inference(superposition,[status(thm)],[c_11168,c_174]) ).
tcf(c_11327,plain,
( product(e_6,e_1,e_6)
| ~ product(e_5,e_1,e_6)
| ~ product(e_1,e_6,e_5) ),
inference(instantiation,[status(thm)],[c_7921]) ).
tcf(c_11427,plain,
( product(e_6,e_1,e_2)
| ~ product(e_5,e_1,e_6)
| ~ product(e_1,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_7921]) ).
tcf(c_11438,plain,
( product(e_5,e_2,e_5)
| ~ product(e_2,e_5,e_1)
| ~ product(e_1,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_5134]) ).
tcf(c_11899,plain,
! [X0: $i] :
( ~ product(e_4,e_6,X0)
| product(X0,e_6,e_1) ),
inference(global_subsumption_just,[status(thm)],[c_11173,c_138,c_137,c_134,c_133,c_175,c_167,c_165,c_164,c_160,c_158,c_156,c_155,c_153,c_149,c_147,c_146,c_145,c_143,c_142,c_141,c_140,c_139,c_404,c_408,c_412,c_416,c_420,c_424,c_447,c_455,c_501,c_516,c_524,c_539,c_1630,c_1638,c_1651,c_1654,c_1668,c_1683,c_1693,c_1694,c_1705,c_1706,c_1726,c_1727,c_1728,c_1921,c_2210,c_2212,c_2226,c_2477,c_2486,c_2770,c_2769,c_3065,c_3146,c_3297,c_3302,c_3301,c_3324,c_3371,c_3385,c_3460,c_3472,c_3589,c_3599,c_3697,c_3713,c_3755,c_5556,c_6045,c_6044,c_6052,c_6132,c_6210,c_6222,c_6402,c_6464,c_6663,c_6841,c_6868,c_6902,c_6911,c_6987,c_7362,c_7421,c_7419,c_7417,c_7609,c_7869,c_8298,c_10240,c_11173,c_11327,c_11438]) ).
tcf(c_11900,plain,
! [X0: $i] :
( product(X0,e_6,e_1)
| ~ product(e_4,e_6,X0) ),
inference(renaming,[status(thm)],[c_11899]) ).
tcf(c_11901,plain,
( product(e_1,e_6,e_1)
| ~ product(e_4,e_6,e_1) ),
inference(instantiation,[status(thm)],[c_11900]) ).
tcf(c_11979,plain,
( product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| 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)
| product(e_3,e_4,e_5) ),
inference(resolution,[status(thm)],[c_10777,c_4286]) ).
tcf(c_12038,plain,
( product(e_6,e_4,e_2)
| product(e_3,e_4,e_5)
| product(e_4,e_5,e_1)
| product(e_4,e_5,e_2)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_4) ),
inference(global_subsumption_just,[status(thm)],[c_11979,c_138,c_137,c_134,c_133,c_175,c_168,c_167,c_165,c_164,c_160,c_156,c_155,c_153,c_149,c_147,c_146,c_145,c_143,c_142,c_141,c_140,c_139,c_404,c_408,c_412,c_416,c_420,c_424,c_447,c_455,c_516,c_524,c_539,c_1630,c_1638,c_1651,c_1654,c_1668,c_1683,c_1705,c_1706,c_1726,c_1727,c_1728,c_1921,c_2210,c_2212,c_2226,c_2486,c_2770,c_2769,c_3066,c_3065,c_3146,c_3297,c_3301,c_3371,c_3460,c_3472,c_3481,c_3589,c_3599,c_3697,c_3713,c_3755,c_4290,c_4969,c_5556,c_5559,c_6045,c_6044,c_6052,c_6132,c_6210,c_6222,c_6402,c_6464,c_6663,c_6841,c_6868,c_6911,c_6987,c_7357,c_7421,c_7419,c_7417,c_7609,c_7869,c_8298,c_9395,c_10240,c_11168,c_11327]) ).
tcf(c_12039,plain,
( product(e_6,e_4,e_2)
| 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)
| product(e_3,e_4,e_5) ),
inference(renaming,[status(thm)],[c_12038]) ).
tcf(c_12040,plain,
( product(e_3,e_4,e_5)
| product(e_4,e_5,e_1)
| product(e_4,e_5,e_2)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_4) ),
inference(global_subsumption_just,[status(thm)],[c_12039,c_138,c_137,c_134,c_133,c_175,c_168,c_167,c_165,c_164,c_160,c_156,c_155,c_153,c_149,c_147,c_146,c_145,c_143,c_142,c_141,c_140,c_139,c_404,c_408,c_412,c_416,c_420,c_424,c_447,c_455,c_516,c_524,c_539,c_1630,c_1638,c_1651,c_1654,c_1668,c_1683,c_1705,c_1706,c_1726,c_1727,c_1728,c_1921,c_2210,c_2212,c_2226,c_2486,c_2770,c_2769,c_3066,c_3065,c_3146,c_3297,c_3301,c_3371,c_3460,c_3472,c_3481,c_3589,c_3599,c_3697,c_3713,c_3755,c_4290,c_4969,c_5556,c_5559,c_6045,c_6044,c_6052,c_6132,c_6210,c_6222,c_6402,c_6464,c_6663,c_6841,c_6868,c_6911,c_6987,c_7357,c_7421,c_7419,c_7417,c_7609,c_7869,c_8298,c_9395,c_10240,c_11168,c_11327]) ).
tcf(c_12041,plain,
( 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)
| product(e_3,e_4,e_5) ),
inference(renaming,[status(thm)],[c_12040]) ).
tcf(c_12057,plain,
( product(e_4,e_5,e_3)
| product(e_4,e_5,e_2)
| product(e_4,e_5,e_1)
| product(e_4,e_4,e_5)
| product(e_3,e_4,e_5) ),
inference(resolution,[status(thm)],[c_12041,c_1598]) ).
tcf(c_12058,plain,
( equalish(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)
| product(e_3,e_4,e_5) ),
inference(resolution,[status(thm)],[c_12041,c_1613]) ).
tcf(c_12061,plain,
( equalish(e_4,e_6)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_2)
| product(e_4,e_5,e_1)
| product(e_3,e_4,e_5) ),
inference(resolution,[status(thm)],[c_12041,c_3147]) ).
tcf(c_12152,plain,
( product(e_2,e_5,e_3)
| ~ product(e_6,e_5,e_2)
| ~ product(e_5,e_3,e_6) ),
inference(instantiation,[status(thm)],[c_7909]) ).
tcf(c_12244,plain,
( product(e_6,e_5,e_1)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_12061,c_138,c_137,c_134,c_133,c_175,c_168,c_167,c_165,c_164,c_160,c_153,c_149,c_147,c_146,c_145,c_143,c_142,c_140,c_139,c_404,c_408,c_412,c_416,c_420,c_424,c_447,c_455,c_516,c_524,c_539,c_1630,c_1638,c_1651,c_1654,c_1668,c_1683,c_1705,c_1706,c_1726,c_1727,c_1728,c_1921,c_2210,c_2212,c_2226,c_2486,c_2770,c_2769,c_3065,c_3146,c_3297,c_3301,c_3371,c_3460,c_3472,c_3481,c_3589,c_3599,c_3697,c_3713,c_3755,c_5556,c_5559,c_6052,c_6132,c_6210,c_6222,c_6402,c_6464,c_6663,c_6841,c_6868,c_6911,c_6987,c_7357,c_7421,c_7419,c_7869,c_8298,c_10240,c_11327]) ).
tcf(c_12245,plain,
( product(e_6,e_5,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1) ),
inference(renaming,[status(thm)],[c_12244]) ).
tcf(c_12259,plain,
! [X0: $i] :
( equalish(X0,e_6)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| ~ product(X0,e_5,e_3) ),
inference(resolution,[status(thm)],[c_12245,c_172]) ).
tcf(c_12260,plain,
( equalish(e_1,e_6)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| ~ product(e_1,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_12259]) ).
tcf(c_12261,plain,
! [X0: $i] :
( product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_3,e_5,X0)
| ~ product(e_5,X0,e_6) ),
inference(resolution,[status(thm)],[c_12245,c_174]) ).
tcf(c_12262,plain,
( product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_3,e_5,e_1)
| ~ product(e_5,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_12261]) ).
tcf(c_12265,plain,
( equalish(e_5,e_4)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_4) ),
inference(resolution,[status(thm)],[c_12245,c_5575]) ).
tcf(c_12387,plain,
( product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_6,e_5,e_1)
| product(e_6,e_5,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_12265,c_138,c_137,c_134,c_133,c_175,c_164,c_147,c_143,c_142,c_139,c_404,c_408,c_412,c_420,c_424,c_455,c_524,c_539,c_1630,c_1654,c_1668,c_1705,c_1706,c_1726,c_1727,c_1728,c_1921,c_2210,c_2620,c_2769,c_3065,c_3460,c_3472,c_3697,c_3755,c_6868,c_11327]) ).
tcf(c_12388,plain,
( product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1) ),
inference(renaming,[status(thm)],[c_12387]) ).
tcf(c_12389,plain,
( product(e_6,e_5,e_2)
| product(e_5,e_6,e_1)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_3)
| product(e_6,e_4,e_1) ),
inference(global_subsumption_just,[status(thm)],[c_12388,c_138,c_137,c_134,c_133,c_175,c_164,c_147,c_143,c_142,c_139,c_404,c_408,c_412,c_420,c_424,c_455,c_524,c_539,c_1630,c_1654,c_1668,c_1705,c_1706,c_1726,c_1727,c_1728,c_1921,c_2210,c_2620,c_2769,c_3065,c_3460,c_3472,c_3697,c_3755,c_6868,c_11327]) ).
tcf(c_12390,plain,
( product(e_6,e_5,e_2)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1) ),
inference(renaming,[status(thm)],[c_12389]) ).
tcf(c_12408,plain,
! [X0: $i] :
( product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_2,e_5,X0)
| ~ product(e_5,X0,e_6) ),
inference(resolution,[status(thm)],[c_12390,c_174]) ).
tcf(c_12425,plain,
( equalish(e_2,e_3)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_3,e_6,e_5) ),
inference(resolution,[status(thm)],[c_12390,c_3888]) ).
tcf(c_12998,plain,
( product(e_6,e_5,e_3)
| ~ product(e_5,e_3,e_1)
| ~ product(e_1,e_5,e_6) ),
inference(instantiation,[status(thm)],[c_7550]) ).
tcf(c_13135,plain,
( product(e_5,e_4,e_6)
| ~ product(e_4,e_6,e_3)
| ~ product(e_3,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_3522]) ).
tcf(c_13140,plain,
( equalish(e_1,e_3)
| ~ product(e_3,e_4,e_5)
| ~ product(e_1,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_1525]) ).
tcf(c_13191,plain,
! [X0: $i] :
( product(e_3,e_4,X0)
| ~ product(e_5,e_4,e_3)
| ~ product(e_4,X0,e_5) ),
inference(instantiation,[status(thm)],[c_4405]) ).
tcf(c_13192,plain,
( product(e_1,e_5,e_4)
| ~ product(e_5,e_4,e_3)
| ~ product(e_3,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_5763]) ).
tcf(c_13193,plain,
( product(e_3,e_4,e_1)
| ~ product(e_5,e_4,e_3)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_13191]) ).
tcf(c_13197,plain,
( product(e_5,e_6,e_1)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_3)
| product(e_6,e_4,e_1) ),
inference(global_subsumption_just,[status(thm)],[c_12425,c_138,c_137,c_134,c_133,c_175,c_164,c_147,c_143,c_142,c_139,c_404,c_408,c_412,c_420,c_424,c_455,c_524,c_539,c_1630,c_1654,c_1668,c_1705,c_1706,c_1726,c_1727,c_1728,c_1921,c_2210,c_2620,c_2769,c_3065,c_3460,c_3472,c_3697,c_3755,c_6868,c_11327]) ).
tcf(c_13198,plain,
( product(e_6,e_4,e_1)
| product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1) ),
inference(renaming,[status(thm)],[c_13197]) ).
tcf(c_13207,plain,
( product(e_4,e_6,e_4)
| ~ product(e_6,e_4,e_1)
| ~ product(e_1,e_6,e_4) ),
inference(instantiation,[status(thm)],[c_5569]) ).
tcf(c_13208,plain,
( product(e_3,e_6,e_4)
| ~ product(e_6,e_4,e_1)
| ~ product(e_1,e_6,e_3) ),
inference(instantiation,[status(thm)],[c_3525]) ).
tcf(c_13324,plain,
( product(e_3,e_5,e_3)
| ~ product(e_5,e_3,e_4)
| ~ product(e_4,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_4279]) ).
tcf(c_13325,plain,
! [X0: $i] :
( product(e_3,e_5,X0)
| ~ product(e_4,e_5,e_3)
| ~ product(e_5,X0,e_4) ),
inference(instantiation,[status(thm)],[c_4098]) ).
tcf(c_13327,plain,
( product(e_3,e_5,e_1)
| ~ product(e_5,e_1,e_4)
| ~ product(e_4,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_13325]) ).
tcf(c_13375,plain,
( equalish(e_5,e_4)
| ~ product(e_6,e_5,e_2)
| ~ product(e_6,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_1592]) ).
tcf(c_13378,plain,
( equalish(e_5,e_1)
| ~ product(e_6,e_5,e_2)
| ~ product(e_6,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1581]) ).
tcf(c_13382,plain,
( equalish(e_1,e_5)
| ~ product(e_6,e_5,e_2)
| ~ product(e_6,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1530]) ).
tcf(c_13399,plain,
( equalish(e_3,e_2)
| ~ product(e_6,e_5,e_3)
| ~ product(e_6,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_3350]) ).
tcf(c_13447,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_5272]) ).
tcf(c_13448,plain,
( equalish(e_5,e_3)
| ~ product(e_5,e_6,e_4)
| ~ product(e_3,e_6,e_4) ),
inference(instantiation,[status(thm)],[c_5270]) ).
tcf(c_13455,plain,
( product(e_5,e_6,e_1)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_12408,c_138,c_137,c_134,c_133,c_175,c_164,c_161,c_147,c_143,c_142,c_139,c_404,c_408,c_412,c_420,c_424,c_455,c_524,c_539,c_1630,c_1654,c_1668,c_1705,c_1706,c_1726,c_1727,c_1728,c_1921,c_2210,c_2595,c_2620,c_2769,c_3460,c_3755,c_6868,c_11327,c_13198,c_13208,c_13448]) ).
tcf(c_13456,plain,
( product(e_5,e_6,e_3)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1) ),
inference(renaming,[status(thm)],[c_13455]) ).
tcf(c_13469,plain,
( equalish(e_5,e_4)
| product(e_5,e_6,e_2)
| product(e_5,e_6,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1) ),
inference(resolution,[status(thm)],[c_13456,c_3791]) ).
tcf(c_13556,plain,
( product(e_4,e_6,e_2)
| product(e_5,e_6,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_13469,c_137,c_134,c_133,c_175,c_167,c_163,c_162,c_156,c_152,c_149,c_147,c_142,c_139,c_404,c_408,c_412,c_455,c_516,c_524,c_539,c_1630,c_1668,c_1694,c_1705,c_1706,c_1726,c_2210,c_3591,c_3720,c_3755,c_4975,c_5287,c_6044,c_6199,c_6222,c_6256,c_6270,c_8143,c_8754,c_10366,c_11901,c_12262,c_13382,c_13469]) ).
tcf(c_13557,plain,
( product(e_5,e_6,e_2)
| product(e_4,e_6,e_2) ),
inference(renaming,[status(thm)],[c_13556]) ).
tcf(c_13572,plain,
! [X0: $i] :
( equalish(X0,e_6)
| product(e_4,e_6,e_2)
| ~ product(e_5,X0,e_2) ),
inference(resolution,[status(thm)],[c_13557,c_171]) ).
tcf(c_13573,plain,
( equalish(e_1,e_6)
| product(e_4,e_6,e_2)
| ~ product(e_5,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_13572]) ).
tcf(c_13576,plain,
! [X0: $i] :
( product(e_4,e_6,e_2)
| product(e_2,e_6,X0)
| ~ product(e_6,X0,e_5) ),
inference(resolution,[status(thm)],[c_13557,c_174]) ).
tcf(c_13719,plain,
( 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)
| product(e_4,e_6,e_2)
| product(e_2,e_6,e_4) ),
inference(resolution,[status(thm)],[c_13576,c_5302]) ).
tcf(c_13731,plain,
( product(e_4,e_6,e_2)
| product(e_6,e_4,e_1)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_13719,c_138,c_137,c_136,c_134,c_133,c_175,c_168,c_167,c_164,c_162,c_159,c_158,c_157,c_147,c_146,c_143,c_142,c_141,c_139,c_404,c_408,c_412,c_420,c_424,c_455,c_493,c_516,c_524,c_539,c_1630,c_1654,c_1668,c_1694,c_1705,c_1706,c_1726,c_1727,c_1728,c_1921,c_2210,c_2475,c_2769,c_3301,c_3455,c_3481,c_3488,c_3713,c_3720,c_3755,c_3792,c_4975,c_5559,c_5816,c_6210,c_6868,c_7480,c_7869,c_10164,c_10366,c_11168,c_11327,c_11901,c_12262,c_13192,c_13193,c_13207,c_13378,c_13557,c_13573]) ).
tcf(c_13732,plain,
( product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_6,e_4,e_1)
| product(e_4,e_6,e_2) ),
inference(renaming,[status(thm)],[c_13731]) ).
tcf(c_13733,plain,
( product(e_6,e_4,e_3)
| product(e_6,e_4,e_2)
| product(e_4,e_6,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_13732,c_138,c_137,c_136,c_134,c_133,c_175,c_168,c_167,c_164,c_162,c_159,c_158,c_157,c_147,c_146,c_143,c_142,c_141,c_139,c_404,c_408,c_412,c_420,c_424,c_455,c_493,c_516,c_524,c_539,c_1630,c_1654,c_1668,c_1694,c_1705,c_1706,c_1726,c_1727,c_1728,c_1921,c_2210,c_2475,c_2769,c_3301,c_3455,c_3481,c_3488,c_3713,c_3720,c_3755,c_3792,c_4975,c_5559,c_5816,c_6210,c_6868,c_7480,c_7869,c_10164,c_10366,c_11168,c_11327,c_11901,c_12262,c_13192,c_13193,c_13207,c_13378,c_13557,c_13573]) ).
tcf(c_13735,plain,
( product(e_6,e_4,e_3)
| product(e_4,e_6,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_13733,c_137,c_134,c_133,c_175,c_163,c_162,c_154,c_147,c_143,c_142,c_139,c_404,c_408,c_412,c_455,c_516,c_524,c_539,c_1630,c_1668,c_1705,c_1706,c_1726,c_2210,c_3755,c_3794,c_4971,c_5820,c_6210,c_11072,c_11168,c_11901,c_12262,c_13375,c_13573,c_13733]) ).
tcf(c_13753,plain,
! [X0: $i] :
( equalish(X0,e_3)
| product(e_4,e_6,e_2)
| ~ product(e_6,e_4,X0) ),
inference(resolution,[status(thm)],[c_13735,c_170]) ).
tcf(c_13754,plain,
( equalish(e_1,e_3)
| product(e_4,e_6,e_2)
| ~ product(e_6,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_13753]) ).
tcf(c_13761,plain,
( equalish(e_4,e_5)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_4,e_6,e_2)
| product(e_4,e_6,e_1)
| product(e_3,e_6,e_5) ),
inference(resolution,[status(thm)],[c_13735,c_3889]) ).
tcf(c_13763,plain,
( equalish(e_4,e_5)
| product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_5,e_6,e_3)
| product(e_4,e_6,e_2)
| product(e_4,e_5,e_1) ),
inference(resolution,[status(thm)],[c_13735,c_7433]) ).
tcf(c_13863,plain,
( product(e_4,e_6,e_2)
| product(e_6,e_5,e_1)
| product(e_6,e_5,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_13761,c_137,c_136,c_134,c_133,c_175,c_168,c_167,c_164,c_163,c_162,c_158,c_157,c_156,c_153,c_152,c_151,c_147,c_146,c_143,c_142,c_141,c_140,c_139,c_404,c_408,c_412,c_416,c_455,c_493,c_516,c_524,c_1630,c_1645,c_1651,c_1668,c_1694,c_1705,c_1706,c_2210,c_2420,c_2444,c_2486,c_2770,c_3067,c_3294,c_3290,c_3382,c_3442,c_3455,c_3472,c_3481,c_3599,c_3713,c_3755,c_3932,c_4969,c_4971,c_5287,c_6047,c_6044,c_6902,c_7525,c_8751,c_10106,c_11093,c_11168,c_12057,c_12245,c_12260,c_12262,c_13140,c_13557,c_13573,c_13754,c_13763]) ).
tcf(c_13864,plain,
( product(e_6,e_5,e_2)
| product(e_6,e_5,e_1)
| product(e_4,e_6,e_2) ),
inference(renaming,[status(thm)],[c_13863]) ).
tcf(c_13865,plain,
( product(e_6,e_5,e_2)
| product(e_6,e_5,e_1) ),
inference(global_subsumption_just,[status(thm)],[c_13864,c_137,c_136,c_134,c_133,c_175,c_168,c_164,c_163,c_162,c_158,c_153,c_152,c_151,c_147,c_146,c_143,c_142,c_141,c_140,c_139,c_404,c_408,c_412,c_416,c_455,c_493,c_516,c_524,c_1630,c_1645,c_1651,c_1668,c_1694,c_1705,c_1706,c_2210,c_2420,c_2444,c_2486,c_2770,c_3067,c_3294,c_3290,c_3382,c_3442,c_3472,c_3481,c_3599,c_3713,c_3755,c_3932,c_4969,c_4971,c_6047,c_6902,c_7525,c_7609,c_11168,c_12058,c_12245,c_12260,c_13140,c_13864]) ).
tcf(c_13986,plain,
! [X0: $i] :
( equalish(X0,e_5)
| product(e_6,e_5,e_1)
| ~ product(e_6,X0,e_2) ),
inference(resolution,[status(thm)],[c_13865,c_171]) ).
tcf(c_13987,plain,
( equalish(e_1,e_5)
| product(e_6,e_5,e_1)
| ~ product(e_6,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_13986]) ).
tcf(c_13990,plain,
! [X0: $i] :
( product(e_6,e_5,e_1)
| product(e_2,e_5,X0)
| ~ product(e_5,X0,e_6) ),
inference(resolution,[status(thm)],[c_13865,c_174]) ).
tcf(c_13991,plain,
( product(e_6,e_5,e_1)
| product(e_2,e_5,e_1)
| ~ product(e_5,e_1,e_6) ),
inference(instantiation,[status(thm)],[c_13990]) ).
tcf(c_14700,plain,
( equalish(e_6,e_3)
| ~ product(e_5,e_4,e_6)
| ~ product(e_5,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_7912]) ).
tcf(c_14771,plain,
( product(e_6,e_5,e_1)
| product(e_6,e_5,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_9913,c_13865]) ).
tcf(c_14772,plain,
( product(e_6,e_5,e_2)
| product(e_6,e_5,e_1) ),
inference(renaming,[status(thm)],[c_14771]) ).
tcf(c_14775,plain,
! [X0: $i] :
( equalish(e_5,X0)
| product(e_6,e_5,e_1)
| ~ product(e_6,X0,e_2) ),
inference(superposition,[status(thm)],[c_14772,c_171]) ).
tcf(c_14783,plain,
( equalish(e_5,e_1)
| product(e_6,e_5,e_1)
| ~ product(e_6,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_14775]) ).
tcf(c_15003,plain,
( product(e_3,e_2,e_5)
| ~ product(e_2,e_5,e_1)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_5134]) ).
tcf(c_15006,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_15003,c_14783,c_14700,c_13991,c_13987,c_13865,c_13754,c_13573,c_13557,c_13447,c_13399,c_13324,c_13327,c_13207,c_13193,c_13135,c_13140,c_12998,c_12152,c_12058,c_11901,c_11427,c_11327,c_11168,c_11093,c_11091,c_10366,c_10240,c_9730,c_8751,c_8636,c_8314,c_8199,c_7525,c_7523,c_7417,c_7357,c_6902,c_6841,c_6313,c_6267,c_6222,c_6210,c_6199,c_6201,c_6204,c_6205,c_6190,c_6045,c_5821,c_5556,c_5287,c_5123,c_4972,c_4971,c_4969,c_3932,c_3794,c_3755,c_3720,c_3713,c_3692,c_3594,c_3488,c_3481,c_3472,c_3451,c_3455,c_3446,c_3442,c_3290,c_3292,c_3294,c_3276,c_3065,c_3066,c_3067,c_2888,c_2769,c_2770,c_2756,c_2595,c_2486,c_2476,c_2444,c_2420,c_2226,c_2212,c_2210,c_1921,c_1728,c_1727,c_1726,c_1706,c_1705,c_1694,c_1683,c_1668,c_1654,c_1651,c_1645,c_1638,c_1630,c_539,c_524,c_516,c_493,c_455,c_447,c_420,c_416,c_412,c_408,c_404,c_139,c_140,c_141,c_142,c_143,c_146,c_147,c_148,c_149,c_150,c_151,c_152,c_153,c_155,c_158,c_159,c_160,c_161,c_162,c_163,c_164,c_165,c_166,c_167,c_168,c_175,c_133,c_134,c_135,c_136,c_137,c_138]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP127-2.006 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.17/10.44 % Computer : n015.cluster.edu
% 0.17/10.44 % Model : x86_64 x86_64
% 0.17/10.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/10.44 % Memory : 8046.5625MB
% 0.17/10.44 % OS : Linux 6.8.0-71-generic
% 0.17/10.44 % CPULimit : 300
% 0.17/10.44 % WCLimit : 300
% 0.17/10.44 % DateTime : Wed Sep 23 13:46:36 UTC 2026
% 0.17/10.44 % CPUTime :
% 0.17/10.44 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.17/10.48 Running EPR theorem proving
% 0.17/10.48 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.17/10.49
% 0.17/10.49 % ======== iProver multi-core TPTP/SMT =========
% 0.17/10.49
% 0.17/10.49 % Detected problem language: tptp
% 0.21/10.50 % Proving...
% 5.29/11.75 % SZS status Started for theBenchmark.p
% 5.29/11.75 % SZS status Unsatisfiable for theBenchmark.p
% 5.29/11.75
% 5.29/11.75 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 5.29/11.75
% 5.29/11.75 % ------ iProver source info
% 5.29/11.75
% 5.29/11.75 % git: date: 2026-07-19 20:42:38 +0200
% 5.29/11.75 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 5.29/11.75 % git: non_committed_changes: false
% 5.29/11.75
% 5.29/11.75 % ------ Parsing...% successful
% 5.29/11.75
% 5.29/11.75
% 5.29/11.75 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 5.29/11.75
% 5.29/11.75 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 5.29/11.75
% 5.29/11.75 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 5.29/11.75 % ------ Proving...
% 5.29/11.75 % ------ Problem Properties
% 5.29/11.75
% 5.29/11.75 %
% 5.29/11.75 % clauses 52
% 5.29/11.75 % conjectures 1
% 5.29/11.75 % EPR 52
% 5.29/11.75 % Horn 51
% 5.29/11.75 % unary 47
% 5.29/11.75 % binary 0
% 5.29/11.75 % lits 67
% 5.29/11.75 % lits eq 0
% 5.29/11.75 % fd_pure 0
% 5.29/11.75 % fd_pseudo 0
% 5.29/11.75 % fd_cond 0
% 5.29/11.75 % fd_pseudo_cond 0
% 5.29/11.75 % AC symbols 0
% 5.29/11.75
% 5.29/11.75 % ------ Input Options Time Limit: Unbounded
% 5.29/11.75
% 5.29/11.75
% 5.29/11.75 % ------
% 5.29/11.75 % Current options:
% 5.29/11.75 % ------
% 5.29/11.75
% 5.29/11.75
% 5.29/11.75 %
% 5.29/11.75
% 5.29/11.75 % ------ Proving...
% 5.29/11.75 %
% 5.29/11.75
% 5.29/11.75 % SZS status Unsatisfiable for theBenchmark.p
% 5.29/11.75
% 5.29/11.75 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 5.29/11.77
% 5.29/11.77
%------------------------------------------------------------------------------