%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP125-3.005 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n019.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:12 PM UTC 2026
% Result : Unsatisfiable 2.49s 1.13s
% Output : CNFRefutation 4.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 48
% Syntax : Number of formulae : 473 ( 82 unt; 0 def)
% Number of atoms : 1480 ( 0 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 1930 ( 923 ~;1007 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 348 ( 0 sgn 348 !; 0 ?; 312 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
next(e_0,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_0_then_e_1) ).
fof(f3,axiom,
next(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_then_e_3) ).
fof(f4,axiom,
next(e_3,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_then_e_4) ).
fof(f5,axiom,
next(e_4,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_then_e_5) ).
fof(f6,axiom,
greater(e_1,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_greater_e_0) ).
fof(f7,axiom,
greater(e_2,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_greater_e_0) ).
fof(f8,axiom,
greater(e_3,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_greater_e_0) ).
fof(f9,axiom,
greater(e_4,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_greater_e_0) ).
fof(f16,axiom,
greater(e_4,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_greater_e_2) ).
fof(f17,axiom,
greater(e_5,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_greater_e_2) ).
fof(f18,axiom,
greater(e_4,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_greater_e_3) ).
fof(f22,axiom,
! [X0] :
( cycle(X0,e_4)
| cycle(X0,e_3)
| cycle(X0,e_2)
| cycle(X0,e_1)
| cycle(X0,e_0)
| ~ group_element(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle2) ).
fof(f23,axiom,
cycle(e_5,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle3) ).
fof(f24,axiom,
! [X2,X3,X0,X1,X4] :
( equalish(X1,X4)
| ~ next(X3,X4)
| ~ greater(X1,e_0)
| ~ next(X0,X2)
| ~ cycle(X2,X3)
| ~ cycle(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle4) ).
fof(f25,axiom,
! [X2,X3,X0,X1,X4] :
( ~ greater(X1,X4)
| ~ greater(X2,X0)
| ~ next(X2,X3)
| ~ cycle(X3,X4)
| ~ cycle(X2,e_0)
| ~ cycle(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle5) ).
fof(f26,axiom,
! [X0,X1] :
( ~ greater(X1,X0)
| ~ product(X0,e_1,X1)
| ~ cycle(X0,e_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle6) ).
fof(f27,axiom,
! [X2,X3,X0,X1] :
( equalish(X2,X3)
| ~ next(X0,X3)
| ~ greater(X1,e_0)
| ~ product(X0,e_1,X2)
| ~ cycle(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle7) ).
fof(f28,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
fof(f29,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
fof(f30,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
fof(f31,axiom,
group_element(e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_4) ).
fof(f32,axiom,
group_element(e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_5) ).
fof(f33,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f34,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f35,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
fof(f36,axiom,
~ equalish(e_1,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_5) ).
fof(f37,axiom,
~ equalish(e_2,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_1) ).
fof(f38,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f39,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
fof(f40,axiom,
~ equalish(e_2,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_5) ).
fof(f41,axiom,
~ equalish(e_3,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_1) ).
fof(f42,axiom,
~ equalish(e_3,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_2) ).
fof(f43,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
fof(f44,axiom,
~ equalish(e_3,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_5) ).
fof(f45,axiom,
~ equalish(e_4,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_1) ).
fof(f46,axiom,
~ equalish(e_4,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_2) ).
fof(f47,axiom,
~ equalish(e_4,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_3) ).
fof(f48,axiom,
~ equalish(e_4,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_5) ).
fof(f49,axiom,
~ equalish(e_5,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_is_not_e_1) ).
fof(f50,axiom,
~ equalish(e_5,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_is_not_e_2) ).
fof(f51,axiom,
~ equalish(e_5,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_is_not_e_3) ).
fof(f52,axiom,
~ equalish(e_5,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_is_not_e_4) ).
fof(f53,axiom,
! [X0,X1] :
( product(X0,X1,e_5)
| product(X0,X1,e_4)
| product(X0,X1,e_3)
| product(X0,X1,e_2)
| product(X0,X1,e_1)
| ~ group_element(X1)
| ~ group_element(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function1) ).
fof(f54,axiom,
! [X2,X3,X0,X1] :
( equalish(X2,X3)
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function2) ).
fof(f55,axiom,
! [X2,X3,X0,X1] :
( equalish(X1,X3)
| ~ product(X0,X3,X2)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_cancellation) ).
fof(f56,axiom,
! [X2,X3,X0,X1] :
( equalish(X0,X3)
| ~ product(X3,X1,X2)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
fof(f57,axiom,
! [X0] : product(X0,X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_idempotence) ).
fof(f58,negated_conjecture,
! [X2,X3,X0,X1] :
( product(X2,X3,X0)
| ~ product(X1,X0,X3)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3) ).
tcf(c_107,plain,
next(e_0,e_1),
inference(cnf_transformation,[],[f1]) ).
tcf(c_109,plain,
next(e_2,e_3),
inference(cnf_transformation,[],[f3]) ).
tcf(c_110,plain,
next(e_3,e_4),
inference(cnf_transformation,[],[f4]) ).
tcf(c_111,plain,
next(e_4,e_5),
inference(cnf_transformation,[],[f5]) ).
tcf(c_112,plain,
greater(e_1,e_0),
inference(cnf_transformation,[],[f6]) ).
tcf(c_113,plain,
greater(e_2,e_0),
inference(cnf_transformation,[],[f7]) ).
tcf(c_114,plain,
greater(e_3,e_0),
inference(cnf_transformation,[],[f8]) ).
tcf(c_115,plain,
greater(e_4,e_0),
inference(cnf_transformation,[],[f9]) ).
tcf(c_122,plain,
greater(e_4,e_2),
inference(cnf_transformation,[],[f16]) ).
tcf(c_123,plain,
greater(e_5,e_2),
inference(cnf_transformation,[],[f17]) ).
tcf(c_124,plain,
greater(e_4,e_3),
inference(cnf_transformation,[],[f18]) ).
tcf(c_128,plain,
! [X0: $i] :
( cycle(X0,e_4)
| cycle(X0,e_3)
| cycle(X0,e_2)
| cycle(X0,e_1)
| cycle(X0,e_0)
| ~ group_element(X0) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_129,plain,
cycle(e_5,e_0),
inference(cnf_transformation,[],[f23]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( equalish(X4,X3)
| ~ greater(X4,e_0)
| ~ cycle(X1,X2)
| ~ cycle(X0,X4)
| ~ next(X2,X3)
| ~ next(X0,X1) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ~ cycle(X0,e_0)
| ~ cycle(X4,X2)
| ~ cycle(X1,X3)
| ~ greater(X2,X3)
| ~ greater(X0,X4)
| ~ next(X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i] :
( ~ cycle(X0,e_0)
| ~ greater(X1,X0)
| ~ product(X0,e_1,X1) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_133,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equalish(X1,X2)
| ~ greater(X3,e_0)
| ~ cycle(X0,X3)
| ~ next(X0,X2)
| ~ product(X0,e_1,X1) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_134,plain,
group_element(e_1),
inference(cnf_transformation,[],[f28]) ).
tcf(c_135,plain,
group_element(e_2),
inference(cnf_transformation,[],[f29]) ).
tcf(c_136,plain,
group_element(e_3),
inference(cnf_transformation,[],[f30]) ).
tcf(c_137,plain,
group_element(e_4),
inference(cnf_transformation,[],[f31]) ).
tcf(c_138,plain,
group_element(e_5),
inference(cnf_transformation,[],[f32]) ).
tcf(c_139,plain,
~ equalish(e_1,e_2),
inference(cnf_transformation,[],[f33]) ).
tcf(c_140,plain,
~ equalish(e_1,e_3),
inference(cnf_transformation,[],[f34]) ).
tcf(c_141,plain,
~ equalish(e_1,e_4),
inference(cnf_transformation,[],[f35]) ).
tcf(c_142,plain,
~ equalish(e_1,e_5),
inference(cnf_transformation,[],[f36]) ).
tcf(c_143,plain,
~ equalish(e_2,e_1),
inference(cnf_transformation,[],[f37]) ).
tcf(c_144,plain,
~ equalish(e_2,e_3),
inference(cnf_transformation,[],[f38]) ).
tcf(c_145,plain,
~ equalish(e_2,e_4),
inference(cnf_transformation,[],[f39]) ).
tcf(c_146,plain,
~ equalish(e_2,e_5),
inference(cnf_transformation,[],[f40]) ).
tcf(c_147,plain,
~ equalish(e_3,e_1),
inference(cnf_transformation,[],[f41]) ).
tcf(c_148,plain,
~ equalish(e_3,e_2),
inference(cnf_transformation,[],[f42]) ).
tcf(c_149,plain,
~ equalish(e_3,e_4),
inference(cnf_transformation,[],[f43]) ).
tcf(c_150,plain,
~ equalish(e_3,e_5),
inference(cnf_transformation,[],[f44]) ).
tcf(c_151,plain,
~ equalish(e_4,e_1),
inference(cnf_transformation,[],[f45]) ).
tcf(c_152,plain,
~ equalish(e_4,e_2),
inference(cnf_transformation,[],[f46]) ).
tcf(c_153,plain,
~ equalish(e_4,e_3),
inference(cnf_transformation,[],[f47]) ).
tcf(c_154,plain,
~ equalish(e_4,e_5),
inference(cnf_transformation,[],[f48]) ).
tcf(c_155,plain,
~ equalish(e_5,e_1),
inference(cnf_transformation,[],[f49]) ).
tcf(c_156,plain,
~ equalish(e_5,e_2),
inference(cnf_transformation,[],[f50]) ).
tcf(c_157,plain,
~ equalish(e_5,e_3),
inference(cnf_transformation,[],[f51]) ).
tcf(c_158,plain,
~ equalish(e_5,e_4),
inference(cnf_transformation,[],[f52]) ).
tcf(c_159,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,e_5)
| product(X1,X0,e_4)
| product(X1,X0,e_3)
| product(X1,X0,e_2)
| product(X1,X0,e_1)
| ~ group_element(X1)
| ~ group_element(X0) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_160,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equalish(X2,X3)
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_161,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equalish(X1,X3)
| ~ product(X0,X3,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_162,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equalish(X0,X3)
| ~ product(X3,X1,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_163,plain,
! [X0: $i] : product(X0,X0,X0),
inference(cnf_transformation,[],[f57]) ).
tcf(c_164,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( product(X3,X2,X1)
| ~ product(X1,X0,X3)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_165,plain,
product(e_1,e_1,e_1),
inference(instantiation,[status(thm)],[c_163]) ).
tcf(c_175,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_160]) ).
tcf(c_176,plain,
( equalish(e_1,e_2)
| ~ product(e_1,e_1,e_2)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_175]) ).
tcf(c_177,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_161]) ).
tcf(c_178,plain,
( equalish(e_1,e_2)
| ~ product(e_1,e_2,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_177]) ).
tcf(c_179,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_162]) ).
tcf(c_180,plain,
( equalish(e_1,e_2)
| ~ product(e_2,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_179]) ).
tcf(c_183,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_160]) ).
tcf(c_184,plain,
( equalish(e_1,e_3)
| ~ product(e_1,e_1,e_3)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_183]) ).
tcf(c_185,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_161]) ).
tcf(c_186,plain,
( equalish(e_1,e_3)
| ~ product(e_1,e_3,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_185]) ).
tcf(c_187,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_162]) ).
tcf(c_191,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_4)
| ~ product(X0,X1,e_4)
| ~ product(X0,X1,e_1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_192,plain,
( equalish(e_1,e_4)
| ~ product(e_1,e_1,e_4)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_191]) ).
tcf(c_193,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_161]) ).
tcf(c_194,plain,
( equalish(e_1,e_4)
| ~ product(e_1,e_4,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_193]) ).
tcf(c_195,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_162]) ).
tcf(c_196,plain,
( equalish(e_1,e_4)
| ~ product(e_4,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_195]) ).
tcf(c_199,plain,
! [X0: $i,X1: $i] :
( equalish(e_1,e_5)
| ~ product(X0,X1,e_5)
| ~ product(X0,X1,e_1) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_200,plain,
( equalish(e_1,e_5)
| ~ product(e_1,e_1,e_5)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_199]) ).
tcf(c_201,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_161]) ).
tcf(c_202,plain,
( equalish(e_1,e_5)
| ~ product(e_1,e_5,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_201]) ).
tcf(c_203,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_162]) ).
tcf(c_204,plain,
( equalish(e_1,e_5)
| ~ product(e_5,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_203]) ).
tcf(c_209,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_161]) ).
tcf(c_211,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_1)
| ~ product(e_2,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_215,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_3)
| ~ product(X0,X1,e_3)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_217,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_161]) ).
tcf(c_219,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_3)
| ~ product(e_3,X0,X1)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_223,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_4)
| ~ product(X0,X1,e_4)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_225,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_4)
| ~ product(X0,e_4,X1)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_227,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_162]) ).
tcf(c_229,plain,
! [X0: $i,X1: $i] :
( equalish(e_2,e_5)
| ~ greater(X1,e_0)
| ~ next(X0,e_5)
| ~ cycle(X0,X1)
| ~ product(X0,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_133]) ).
tcf(c_233,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_161]) ).
tcf(c_235,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_162]) ).
tcf(c_241,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_161]) ).
tcf(c_243,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_1)
| ~ product(e_3,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_249,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_2)
| ~ product(X0,e_3,X1)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_251,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_2)
| ~ product(e_3,X0,X1)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_255,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_4)
| ~ product(X0,X1,e_4)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_257,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_161]) ).
tcf(c_259,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_162]) ).
tcf(c_261,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_5)
| ~ greater(X1,e_0)
| ~ next(X0,e_5)
| ~ cycle(X0,X1)
| ~ product(X0,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_133]) ).
tcf(c_263,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_5)
| ~ product(X0,X1,e_5)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_265,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_161]) ).
tcf(c_267,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_162]) ).
tcf(c_273,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_161]) ).
tcf(c_275,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_1)
| ~ product(e_4,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_281,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_2)
| ~ product(X0,e_4,X1)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_283,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_162]) ).
tcf(c_285,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_3)
| ~ greater(X1,e_0)
| ~ next(X0,e_3)
| ~ cycle(X0,X1)
| ~ product(X0,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_133]) ).
tcf(c_287,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_3)
| ~ product(X0,X1,e_4)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_289,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_3)
| ~ product(X0,e_4,X1)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_291,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_162]) ).
tcf(c_295,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_5)
| ~ product(X0,X1,e_5)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_297,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_161]) ).
tcf(c_299,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_162]) ).
tcf(c_305,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_161]) ).
tcf(c_307,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_162]) ).
tcf(c_311,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_160]) ).
tcf(c_313,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_161]) ).
tcf(c_315,plain,
! [X0: $i,X1: $i] :
( equalish(e_5,e_2)
| ~ product(e_5,X0,X1)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_162]) ).
tcf(c_317,plain,
! [X0: $i,X1: $i] :
( equalish(e_5,e_3)
| ~ greater(X1,e_0)
| ~ next(X0,e_3)
| ~ cycle(X0,X1)
| ~ product(X0,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_133]) ).
tcf(c_321,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_161]) ).
tcf(c_323,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_162]) ).
tcf(c_329,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_161]) ).
tcf(c_331,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_162]) ).
tcf(c_347,plain,
( ~ cycle(e_2,e_0)
| ~ greater(e_4,e_2)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_132]) ).
tcf(c_348,plain,
( ~ cycle(e_2,e_0)
| ~ greater(e_5,e_2)
| ~ product(e_2,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_132]) ).
tcf(c_352,plain,
! [X0: $i,X1: $i,X2: $i] :
( equalish(X2,e_1)
| ~ next(e_0,e_1)
| ~ cycle(X1,e_0)
| ~ greater(X2,e_0)
| ~ cycle(X0,X2)
| ~ next(X0,X1) ),
inference(instantiation,[status(thm)],[c_130]) ).
tcf(c_369,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ cycle(e_4,e_0)
| ~ next(e_4,e_5)
| ~ cycle(e_5,X1)
| ~ greater(e_4,X2)
| ~ cycle(X2,X0)
| ~ greater(X0,X1) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_376,plain,
! [X0: $i] :
( product(e_1,e_1,e_2)
| ~ product(e_2,X0,e_1)
| ~ product(X0,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_164]) ).
tcf(c_378,plain,
! [X0: $i] :
( product(e_1,e_1,e_3)
| ~ product(e_3,X0,e_1)
| ~ product(X0,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_164]) ).
tcf(c_380,plain,
! [X0: $i] :
( product(e_1,e_1,e_4)
| ~ product(e_4,X0,e_1)
| ~ product(X0,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_164]) ).
tcf(c_382,plain,
! [X0: $i] :
( product(e_1,e_1,e_5)
| ~ product(e_5,X0,e_1)
| ~ product(X0,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_164]) ).
tcf(c_384,plain,
( cycle(e_2,e_4)
| cycle(e_2,e_3)
| cycle(e_2,e_2)
| cycle(e_2,e_1)
| cycle(e_2,e_0)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_128]) ).
tcf(c_387,plain,
( cycle(e_3,e_4)
| cycle(e_3,e_3)
| cycle(e_3,e_2)
| cycle(e_3,e_1)
| cycle(e_3,e_0)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_128]) ).
tcf(c_389,plain,
( cycle(e_4,e_4)
| cycle(e_4,e_3)
| cycle(e_4,e_2)
| cycle(e_4,e_1)
| cycle(e_4,e_0)
| ~ group_element(e_4) ),
inference(instantiation,[status(thm)],[c_128]) ).
tcf(c_390,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_177]) ).
tcf(c_391,plain,
product(e_2,e_2,e_2),
inference(instantiation,[status(thm)],[c_163]) ).
tcf(c_393,plain,
! [X0: $i] :
( product(X0,e_2,e_5)
| product(X0,e_2,e_4)
| product(X0,e_2,e_3)
| product(X0,e_2,e_2)
| product(X0,e_2,e_1)
| ~ group_element(e_2)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_394,plain,
( product(e_1,e_2,e_5)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_1)
| ~ group_element(e_2)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_393]) ).
tcf(c_395,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,e_2,X0)
| ~ product(X1,X0,e_2)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_164]) ).
tcf(c_400,plain,
! [X0: $i] :
( product(e_2,X0,e_5)
| product(e_2,X0,e_4)
| product(e_2,X0,e_3)
| product(e_2,X0,e_2)
| product(e_2,X0,e_1)
| ~ group_element(e_2)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_401,plain,
( product(e_2,e_1,e_5)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| ~ group_element(e_2)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_400]) ).
tcf(c_402,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_2,X2,X1)
| ~ product(X1,X0,e_2)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_164]) ).
tcf(c_405,plain,
product(e_3,e_3,e_3),
inference(instantiation,[status(thm)],[c_163]) ).
tcf(c_407,plain,
! [X0: $i] :
( product(X0,e_3,e_5)
| product(X0,e_3,e_4)
| product(X0,e_3,e_3)
| product(X0,e_3,e_2)
| product(X0,e_3,e_1)
| ~ group_element(e_3)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_408,plain,
( product(e_1,e_3,e_5)
| product(e_1,e_3,e_4)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| ~ group_element(e_3)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_407]) ).
tcf(c_409,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,e_3,X0)
| ~ product(X1,X0,e_3)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_164]) ).
tcf(c_414,plain,
! [X0: $i] :
( product(e_3,X0,e_5)
| product(e_3,X0,e_4)
| product(e_3,X0,e_3)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1)
| ~ group_element(e_3)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_416,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_3,X2,X1)
| ~ product(X1,X0,e_3)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_164]) ).
tcf(c_424,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_193]) ).
tcf(c_425,plain,
product(e_4,e_4,e_4),
inference(instantiation,[status(thm)],[c_163]) ).
tcf(c_427,plain,
! [X0: $i] :
( product(X0,e_4,e_5)
| product(X0,e_4,e_4)
| product(X0,e_4,e_3)
| product(X0,e_4,e_2)
| product(X0,e_4,e_1)
| ~ group_element(e_4)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_428,plain,
( product(e_1,e_4,e_5)
| product(e_1,e_4,e_4)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1)
| ~ group_element(e_4)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_427]) ).
tcf(c_429,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,e_4,X0)
| ~ product(X1,X0,e_4)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_164]) ).
tcf(c_434,plain,
! [X0: $i] :
( product(e_4,X0,e_5)
| product(e_4,X0,e_4)
| product(e_4,X0,e_3)
| product(e_4,X0,e_2)
| product(e_4,X0,e_1)
| ~ group_element(e_4)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_435,plain,
( product(e_4,e_1,e_5)
| product(e_4,e_1,e_4)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| ~ group_element(e_4)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_434]) ).
tcf(c_436,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_4,X2,X1)
| ~ product(X1,X0,e_4)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_164]) ).
tcf(c_438,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_201]) ).
tcf(c_439,plain,
product(e_5,e_5,e_5),
inference(instantiation,[status(thm)],[c_163]) ).
tcf(c_441,plain,
! [X0: $i] :
( product(X0,e_5,e_5)
| product(X0,e_5,e_4)
| product(X0,e_5,e_3)
| product(X0,e_5,e_2)
| product(X0,e_5,e_1)
| ~ group_element(e_5)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_442,plain,
( product(e_1,e_5,e_5)
| product(e_1,e_5,e_4)
| product(e_1,e_5,e_3)
| product(e_1,e_5,e_2)
| product(e_1,e_5,e_1)
| ~ group_element(e_5)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_441]) ).
tcf(c_443,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,e_5,X0)
| ~ product(X1,X0,e_5)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_164]) ).
tcf(c_448,plain,
! [X0: $i] :
( product(e_5,X0,e_5)
| product(e_5,X0,e_4)
| product(e_5,X0,e_3)
| product(e_5,X0,e_2)
| product(e_5,X0,e_1)
| ~ group_element(e_5)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_449,plain,
( product(e_5,e_1,e_5)
| product(e_5,e_1,e_4)
| product(e_5,e_1,e_3)
| product(e_5,e_1,e_2)
| product(e_5,e_1,e_1)
| ~ group_element(e_5)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_448]) ).
tcf(c_450,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_5,X2,X1)
| ~ product(X1,X0,e_5)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_164]) ).
tcf(c_562,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X1,e_3)
| ~ product(e_3,X0,X2)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_164]) ).
tcf(c_633,plain,
! [X0: $i] :
( equalish(e_2,e_5)
| ~ next(e_4,e_5)
| ~ cycle(e_4,X0)
| ~ greater(X0,e_0)
| ~ product(e_4,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_229]) ).
tcf(c_634,plain,
( equalish(e_2,e_5)
| ~ cycle(e_4,e_1)
| ~ greater(e_1,e_0)
| ~ next(e_4,e_5)
| ~ product(e_4,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_633]) ).
tcf(c_640,plain,
! [X0: $i] :
( equalish(e_3,e_5)
| ~ next(e_4,e_5)
| ~ cycle(e_4,X0)
| ~ greater(X0,e_0)
| ~ product(e_4,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_261]) ).
tcf(c_641,plain,
( equalish(e_3,e_5)
| ~ cycle(e_4,e_1)
| ~ greater(e_1,e_0)
| ~ next(e_4,e_5)
| ~ product(e_4,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_640]) ).
tcf(c_644,plain,
! [X0: $i,X1: $i] :
( product(X1,e_1,e_4)
| ~ product(X0,e_4,e_1)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_164]) ).
tcf(c_650,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X1,e_5)
| ~ product(e_5,X0,X2)
| ~ product(X0,e_5,X1) ),
inference(instantiation,[status(thm)],[c_164]) ).
tcf(c_651,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ next(e_2,e_3)
| ~ cycle(e_2,X0)
| ~ greater(X0,e_0)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_285]) ).
tcf(c_652,plain,
( equalish(e_4,e_3)
| ~ cycle(e_2,e_1)
| ~ greater(e_1,e_0)
| ~ next(e_2,e_3)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_651]) ).
tcf(c_658,plain,
! [X0: $i] :
( equalish(e_5,e_3)
| ~ next(e_2,e_3)
| ~ cycle(e_2,X0)
| ~ greater(X0,e_0)
| ~ product(e_2,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_317]) ).
tcf(c_659,plain,
( equalish(e_5,e_3)
| ~ cycle(e_2,e_1)
| ~ greater(e_1,e_0)
| ~ next(e_2,e_3)
| ~ product(e_2,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_658]) ).
tcf(c_716,plain,
! [X0: $i] :
( equalish(X0,e_1)
| ~ cycle(e_3,e_0)
| ~ next(e_2,e_3)
| ~ next(e_0,e_1)
| ~ cycle(e_2,X0)
| ~ greater(X0,e_0) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_718,plain,
! [X0: $i] :
( equalish(X0,e_1)
| ~ cycle(e_4,e_0)
| ~ next(e_3,e_4)
| ~ next(e_0,e_1)
| ~ cycle(e_3,X0)
| ~ greater(X0,e_0) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_720,plain,
! [X0: $i] :
( equalish(X0,e_1)
| ~ cycle(e_5,e_0)
| ~ next(e_4,e_5)
| ~ next(e_0,e_1)
| ~ cycle(e_4,X0)
| ~ greater(X0,e_0) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_788,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_179]) ).
tcf(c_797,plain,
( equalish(e_2,e_3)
| ~ product(e_3,e_3,e_3)
| ~ product(e_3,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_215]) ).
tcf(c_801,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_217]) ).
tcf(c_805,plain,
( equalish(e_2,e_3)
| ~ product(e_3,e_3,e_3)
| ~ product(e_2,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_219]) ).
tcf(c_806,plain,
( equalish(e_1,e_3)
| ~ product(e_3,e_3,e_3)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_187]) ).
tcf(c_815,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_4,e_4)
| ~ product(e_4,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_255]) ).
tcf(c_816,plain,
( equalish(e_2,e_4)
| ~ product(e_4,e_4,e_4)
| ~ product(e_4,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_223]) ).
tcf(c_821,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_257]) ).
tcf(c_822,plain,
( equalish(e_2,e_4)
| ~ product(e_4,e_4,e_4)
| ~ product(e_4,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_827,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_4,e_4)
| ~ product(e_3,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_259]) ).
tcf(c_828,plain,
( equalish(e_2,e_4)
| ~ product(e_4,e_4,e_4)
| ~ product(e_2,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_227]) ).
tcf(c_829,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_195]) ).
tcf(c_841,plain,
( equalish(e_4,e_5)
| ~ product(e_5,e_5,e_5)
| ~ product(e_5,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_295]) ).
tcf(c_842,plain,
( equalish(e_3,e_5)
| ~ product(e_5,e_5,e_5)
| ~ product(e_5,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_263]) ).
tcf(c_849,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_297]) ).
tcf(c_850,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_265]) ).
tcf(c_851,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_233]) ).
tcf(c_857,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_299]) ).
tcf(c_858,plain,
( equalish(e_3,e_5)
| ~ product(e_5,e_5,e_5)
| ~ product(e_3,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_267]) ).
tcf(c_859,plain,
( equalish(e_2,e_5)
| ~ product(e_5,e_5,e_5)
| ~ product(e_2,e_5,e_5) ),
inference(instantiation,[status(thm)],[c_235]) ).
tcf(c_860,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_203]) ).
tcf(c_898,plain,
! [X0: $i,X1: $i] :
( product(e_3,X1,X0)
| ~ product(X0,e_2,e_3)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_416]) ).
tcf(c_899,plain,
! [X0: $i,X1: $i] :
( product(X1,e_3,e_2)
| ~ product(X0,e_2,e_3)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_409]) ).
tcf(c_915,plain,
( product(e_3,e_2,e_5)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_1)
| ~ group_element(e_3)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_393]) ).
tcf(c_920,plain,
( product(e_4,e_2,e_5)
| product(e_4,e_2,e_4)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_1)
| ~ group_element(e_4)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_393]) ).
tcf(c_927,plain,
( product(e_5,e_2,e_5)
| product(e_5,e_2,e_4)
| product(e_5,e_2,e_3)
| product(e_5,e_2,e_2)
| product(e_5,e_2,e_1)
| ~ group_element(e_5)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_393]) ).
tcf(c_940,plain,
! [X0: $i,X1: $i] :
( product(e_5,X1,e_2)
| ~ product(e_2,X0,e_5)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_450]) ).
tcf(c_941,plain,
! [X0: $i,X1: $i] :
( product(X1,e_5,X0)
| ~ product(e_2,X0,e_5)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_443]) ).
tcf(c_945,plain,
! [X0: $i] :
( equalish(e_2,e_1)
| ~ product(e_2,X0,e_5)
| ~ product(e_1,X0,e_5) ),
inference(instantiation,[status(thm)],[c_211]) ).
tcf(c_949,plain,
( product(e_2,e_3,e_5)
| product(e_2,e_3,e_4)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| ~ group_element(e_3)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_400]) ).
tcf(c_954,plain,
( product(e_2,e_4,e_5)
| product(e_2,e_4,e_4)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| ~ group_element(e_4)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_400]) ).
tcf(c_977,plain,
( product(e_2,e_5,e_5)
| product(e_2,e_5,e_4)
| product(e_2,e_5,e_3)
| product(e_2,e_5,e_2)
| product(e_2,e_5,e_1)
| ~ group_element(e_5)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_400]) ).
tcf(c_990,plain,
! [X0: $i,X1: $i] :
( product(e_2,X1,X0)
| ~ product(X0,e_3,e_2)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_402]) ).
tcf(c_991,plain,
! [X0: $i,X1: $i] :
( product(X1,e_2,e_3)
| ~ product(X0,e_3,e_2)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_395]) ).
tcf(c_999,plain,
! [X0: $i] :
( equalish(e_3,e_2)
| ~ product(X0,e_3,e_2)
| ~ product(X0,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_249]) ).
tcf(c_1008,plain,
( product(e_4,e_3,e_5)
| product(e_4,e_3,e_4)
| product(e_4,e_3,e_3)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_1)
| ~ group_element(e_4)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_407]) ).
tcf(c_1015,plain,
( product(e_5,e_3,e_5)
| product(e_5,e_3,e_4)
| product(e_5,e_3,e_3)
| product(e_5,e_3,e_2)
| product(e_5,e_3,e_1)
| ~ group_element(e_5)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_407]) ).
tcf(c_1028,plain,
! [X0: $i,X1: $i] :
( product(e_4,X1,e_3)
| ~ product(e_3,X0,e_4)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_436]) ).
tcf(c_1029,plain,
! [X0: $i,X1: $i] :
( product(X1,e_4,X0)
| ~ product(e_3,X0,e_4)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_429]) ).
tcf(c_1036,plain,
! [X0: $i] :
( equalish(e_2,e_3)
| ~ product(e_3,X0,e_4)
| ~ product(e_2,X0,e_4) ),
inference(instantiation,[status(thm)],[c_219]) ).
tcf(c_1039,plain,
( equalish(e_2,e_3)
| ~ product(e_3,e_1,e_4)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_1036]) ).
tcf(c_1042,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ product(e_3,X0,e_4)
| ~ product(e_3,X0,e_3) ),
inference(instantiation,[status(thm)],[c_287]) ).
tcf(c_1054,plain,
( product(e_3,e_4,e_5)
| product(e_3,e_4,e_4)
| product(e_3,e_4,e_3)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_1)
| ~ group_element(e_4)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_414]) ).
tcf(c_1061,plain,
( product(e_3,e_5,e_5)
| product(e_3,e_5,e_4)
| product(e_3,e_5,e_3)
| product(e_3,e_5,e_2)
| product(e_3,e_5,e_1)
| ~ group_element(e_5)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_414]) ).
tcf(c_1065,plain,
( equalish(e_5,e_1)
| ~ product(e_3,e_5,e_4)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_1068,plain,
( equalish(e_2,e_5)
| ~ product(e_3,e_5,e_4)
| ~ product(e_3,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_233]) ).
tcf(c_1074,plain,
! [X0: $i,X1: $i] :
( product(e_2,X1,X0)
| ~ product(X0,e_4,e_2)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_402]) ).
tcf(c_1075,plain,
! [X0: $i,X1: $i] :
( product(X1,e_2,e_4)
| ~ product(X0,e_4,e_2)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_395]) ).
tcf(c_1084,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ product(X0,e_4,e_2)
| ~ product(X0,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_289]) ).
tcf(c_1085,plain,
! [X0: $i] :
( equalish(e_4,e_2)
| ~ product(X0,e_4,e_2)
| ~ product(X0,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_281]) ).
tcf(c_1086,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_273]) ).
tcf(c_1095,plain,
( equalish(e_4,e_3)
| ~ product(e_1,e_4,e_2)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_1084]) ).
tcf(c_1097,plain,
( product(e_5,e_4,e_5)
| product(e_5,e_4,e_4)
| product(e_5,e_4,e_3)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_1)
| ~ group_element(e_5)
| ~ group_element(e_4) ),
inference(instantiation,[status(thm)],[c_427]) ).
tcf(c_1099,plain,
( equalish(e_5,e_3)
| ~ product(e_5,e_4,e_2)
| ~ product(e_3,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_323]) ).
tcf(c_1101,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_307]) ).
tcf(c_1103,plain,
( equalish(e_3,e_5)
| ~ product(e_5,e_4,e_2)
| ~ product(e_3,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_267]) ).
tcf(c_1105,plain,
( equalish(e_1,e_5)
| ~ product(e_5,e_4,e_2)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_203]) ).
tcf(c_1110,plain,
! [X0: $i,X1: $i] :
( product(e_5,X1,e_4)
| ~ product(e_4,X0,e_5)
| ~ product(X0,e_4,X1) ),
inference(instantiation,[status(thm)],[c_450]) ).
tcf(c_1117,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ product(e_4,X0,e_5)
| ~ product(e_3,X0,e_5) ),
inference(instantiation,[status(thm)],[c_291]) ).
tcf(c_1118,plain,
! [X0: $i] :
( equalish(e_4,e_2)
| ~ product(e_4,X0,e_5)
| ~ product(e_2,X0,e_5) ),
inference(instantiation,[status(thm)],[c_283]) ).
tcf(c_1119,plain,
! [X0: $i] :
( equalish(e_4,e_1)
| ~ product(e_4,X0,e_5)
| ~ product(e_1,X0,e_5) ),
inference(instantiation,[status(thm)],[c_275]) ).
tcf(c_1128,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_1,e_5)
| ~ product(e_3,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_1117]) ).
tcf(c_1145,plain,
( product(e_4,e_5,e_5)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_2)
| product(e_4,e_5,e_1)
| ~ group_element(e_5)
| ~ group_element(e_4) ),
inference(instantiation,[status(thm)],[c_434]) ).
tcf(c_1158,plain,
! [X0: $i,X1: $i] :
( product(e_2,X1,X0)
| ~ product(X0,e_5,e_2)
| ~ product(e_5,X0,X1) ),
inference(instantiation,[status(thm)],[c_402]) ).
tcf(c_1159,plain,
! [X0: $i,X1: $i] :
( product(X1,e_2,e_5)
| ~ product(X0,e_5,e_2)
| ~ product(e_5,X0,X1) ),
inference(instantiation,[status(thm)],[c_395]) ).
tcf(c_1169,plain,
! [X0: $i] :
( equalish(e_5,e_4)
| ~ product(X0,e_5,e_2)
| ~ product(X0,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_1170,plain,
! [X0: $i] :
( equalish(e_5,e_3)
| ~ product(X0,e_5,e_2)
| ~ product(X0,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_321]) ).
tcf(c_1171,plain,
! [X0: $i] :
( equalish(e_5,e_2)
| ~ product(X0,e_5,e_2)
| ~ product(X0,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_313]) ).
tcf(c_1190,plain,
! [X0: $i,X1: $i] :
( product(e_2,X1,e_5)
| ~ product(e_5,X0,e_2)
| ~ product(X0,e_5,X1) ),
inference(instantiation,[status(thm)],[c_402]) ).
tcf(c_1204,plain,
! [X0: $i] :
( equalish(e_5,e_2)
| ~ product(e_5,X0,e_2)
| ~ product(e_2,X0,e_2) ),
inference(instantiation,[status(thm)],[c_315]) ).
tcf(c_1225,plain,
( equalish(e_5,e_3)
| ~ cycle(e_2,e_2)
| ~ greater(e_2,e_0)
| ~ next(e_2,e_3)
| ~ product(e_2,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_658]) ).
tcf(c_1247,plain,
( equalish(e_2,e_1)
| ~ cycle(e_3,e_0)
| ~ cycle(e_2,e_2)
| ~ greater(e_2,e_0)
| ~ next(e_2,e_3)
| ~ next(e_0,e_1) ),
inference(instantiation,[status(thm)],[c_716]) ).
tcf(c_1251,plain,
( equalish(e_2,e_1)
| ~ cycle(e_4,e_0)
| ~ cycle(e_3,e_2)
| ~ greater(e_2,e_0)
| ~ next(e_3,e_4)
| ~ next(e_0,e_1) ),
inference(instantiation,[status(thm)],[c_718]) ).
tcf(c_1253,plain,
( equalish(e_4,e_1)
| ~ cycle(e_4,e_0)
| ~ cycle(e_3,e_4)
| ~ greater(e_4,e_0)
| ~ next(e_3,e_4)
| ~ next(e_0,e_1) ),
inference(instantiation,[status(thm)],[c_718]) ).
tcf(c_1255,plain,
( equalish(e_2,e_1)
| ~ cycle(e_5,e_0)
| ~ cycle(e_4,e_2)
| ~ greater(e_2,e_0)
| ~ next(e_4,e_5)
| ~ next(e_0,e_1) ),
inference(instantiation,[status(thm)],[c_720]) ).
tcf(c_1256,plain,
( equalish(e_3,e_1)
| ~ cycle(e_5,e_0)
| ~ cycle(e_4,e_3)
| ~ greater(e_3,e_0)
| ~ next(e_4,e_5)
| ~ next(e_0,e_1) ),
inference(instantiation,[status(thm)],[c_720]) ).
tcf(c_1257,plain,
( equalish(e_4,e_1)
| ~ cycle(e_5,e_0)
| ~ cycle(e_4,e_4)
| ~ greater(e_4,e_0)
| ~ next(e_4,e_5)
| ~ next(e_0,e_1) ),
inference(instantiation,[status(thm)],[c_720]) ).
tcf(c_1293,plain,
! [X0: $i,X1: $i] :
( product(e_4,X1,X0)
| ~ product(X0,e_3,e_4)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_436]) ).
tcf(c_1294,plain,
! [X0: $i,X1: $i] :
( product(X1,e_4,e_3)
| ~ product(X0,e_3,e_4)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_429]) ).
tcf(c_1298,plain,
! [X0: $i] :
( equalish(e_3,e_2)
| ~ product(X0,e_3,e_4)
| ~ product(X0,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_249]) ).
tcf(c_1299,plain,
! [X0: $i] :
( equalish(e_3,e_1)
| ~ product(X0,e_3,e_4)
| ~ product(X0,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_241]) ).
tcf(c_1362,plain,
! [X0: $i] :
( product(e_5,e_3,e_2)
| ~ product(e_2,X0,e_5)
| ~ product(X0,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_899]) ).
tcf(c_1391,plain,
! [X0: $i] :
( product(e_4,e_4,e_3)
| ~ product(e_3,X0,e_4)
| ~ product(X0,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_1028]) ).
tcf(c_1433,plain,
! [X0: $i] :
( product(e_3,e_5,X0)
| ~ product(e_2,X0,e_5)
| ~ product(X0,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_898]) ).
tcf(c_1501,plain,
! [X0: $i,X1: $i] :
( product(e_3,X1,X0)
| ~ product(X0,e_4,e_3)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_416]) ).
tcf(c_1502,plain,
! [X0: $i,X1: $i] :
( product(X1,e_3,e_4)
| ~ product(X0,e_4,e_3)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_409]) ).
tcf(c_1515,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ product(X0,e_4,e_3)
| ~ product(X0,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_289]) ).
tcf(c_1516,plain,
! [X0: $i] :
( equalish(e_4,e_2)
| ~ product(X0,e_4,e_3)
| ~ product(X0,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_281]) ).
tcf(c_1517,plain,
! [X0: $i] :
( equalish(e_4,e_1)
| ~ product(X0,e_4,e_3)
| ~ product(X0,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_273]) ).
tcf(c_1534,plain,
! [X0: $i,X1: $i] :
( product(e_3,X1,e_4)
| ~ product(e_4,X0,e_3)
| ~ product(X0,e_4,X1) ),
inference(instantiation,[status(thm)],[c_416]) ).
tcf(c_1535,plain,
! [X0: $i,X1: $i] :
( product(X1,e_3,X0)
| ~ product(e_4,X0,e_3)
| ~ product(X0,e_4,X1) ),
inference(instantiation,[status(thm)],[c_409]) ).
tcf(c_1549,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ product(e_4,X0,e_3)
| ~ product(e_3,X0,e_3) ),
inference(instantiation,[status(thm)],[c_291]) ).
tcf(c_1550,plain,
! [X0: $i] :
( equalish(e_4,e_2)
| ~ product(e_4,X0,e_3)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_283]) ).
tcf(c_1559,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_1,e_3)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_1550]) ).
tcf(c_1659,plain,
( product(e_1,e_1,e_3)
| ~ product(e_3,e_2,e_1)
| ~ product(e_2,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_378]) ).
tcf(c_1669,plain,
( product(e_1,e_5,e_4)
| ~ product(e_4,e_2,e_1)
| ~ product(e_2,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_941]) ).
tcf(c_1670,plain,
( product(e_5,e_1,e_2)
| ~ product(e_4,e_2,e_1)
| ~ product(e_2,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_940]) ).
tcf(c_1713,plain,
( product(e_1,e_1,e_5)
| ~ product(e_5,e_2,e_1)
| ~ product(e_2,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_382]) ).
tcf(c_1756,plain,
( product(e_3,e_1,e_4)
| ~ product(e_4,e_2,e_3)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_898]) ).
tcf(c_1767,plain,
( product(e_1,e_1,e_2)
| ~ product(e_4,e_2,e_1)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_376]) ).
tcf(c_1784,plain,
( product(e_1,e_3,e_2)
| ~ product(e_5,e_2,e_3)
| ~ product(e_2,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_899]) ).
tcf(c_1837,plain,
( equalish(e_2,e_3)
| ~ product(e_4,e_3,e_1)
| ~ product(e_4,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_217]) ).
tcf(c_1847,plain,
( product(e_1,e_1,e_4)
| ~ product(e_4,e_3,e_1)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_380]) ).
tcf(c_1861,plain,
( product(e_1,e_4,e_5)
| ~ product(e_5,e_3,e_1)
| ~ product(e_3,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_1029]) ).
tcf(c_1869,plain,
( equalish(e_5,e_4)
| ~ product(e_5,e_3,e_1)
| ~ product(e_4,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_331]) ).
tcf(c_1889,plain,
( equalish(e_3,e_2)
| ~ product(e_3,e_4,e_1)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_251]) ).
tcf(c_1894,plain,
( equalish(e_4,e_2)
| ~ product(e_3,e_4,e_1)
| ~ product(e_3,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_281]) ).
tcf(c_1916,plain,
( equalish(e_3,e_2)
| ~ product(e_3,e_5,e_1)
| ~ product(e_2,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_251]) ).
tcf(c_1921,plain,
( product(e_2,e_1,e_5)
| ~ product(e_5,e_3,e_2)
| ~ product(e_3,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_1190]) ).
tcf(c_1922,plain,
( equalish(e_5,e_4)
| ~ product(e_3,e_5,e_1)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_1931,plain,
( product(e_1,e_1,e_3)
| ~ product(e_5,e_3,e_1)
| ~ product(e_3,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_378]) ).
tcf(c_1975,plain,
( equalish(e_4,e_3)
| ~ product(e_5,e_4,e_1)
| ~ product(e_5,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_289]) ).
tcf(c_1976,plain,
( equalish(e_4,e_2)
| ~ product(e_5,e_4,e_1)
| ~ product(e_5,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_281]) ).
tcf(c_1981,plain,
( product(e_2,e_1,e_4)
| ~ product(e_5,e_4,e_1)
| ~ product(e_4,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_1158]) ).
tcf(c_1982,plain,
( product(e_1,e_2,e_5)
| ~ product(e_5,e_4,e_1)
| ~ product(e_4,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_1159]) ).
tcf(c_1984,plain,
( equalish(e_5,e_3)
| ~ product(e_5,e_4,e_1)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_323]) ).
tcf(c_1985,plain,
( equalish(e_5,e_2)
| ~ product(e_5,e_4,e_1)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_315]) ).
tcf(c_1992,plain,
! [X0: $i] :
( product(X0,e_1,e_4)
| ~ product(e_5,e_4,e_1)
| ~ product(e_4,e_5,X0) ),
inference(instantiation,[status(thm)],[c_644]) ).
tcf(c_1993,plain,
( product(e_1,e_1,e_4)
| ~ product(e_5,e_4,e_1)
| ~ product(e_4,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_1992]) ).
tcf(c_2012,plain,
( product(e_2,e_1,e_5)
| ~ product(e_5,e_4,e_2)
| ~ product(e_4,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_1190]) ).
tcf(c_2014,plain,
( equalish(e_5,e_3)
| ~ product(e_4,e_5,e_1)
| ~ product(e_4,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_321]) ).
tcf(c_2018,plain,
( equalish(e_3,e_5)
| ~ product(e_4,e_5,e_1)
| ~ product(e_4,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_265]) ).
tcf(c_2057,plain,
( equalish(e_5,e_3)
| ~ cycle(e_2,e_3)
| ~ greater(e_3,e_0)
| ~ next(e_2,e_3)
| ~ product(e_2,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_658]) ).
tcf(c_2083,plain,
( product(e_3,e_3,e_4)
| ~ product(e_4,e_2,e_3)
| ~ product(e_2,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_898]) ).
tcf(c_2085,plain,
( equalish(e_2,e_1)
| ~ product(e_2,e_4,e_3)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_211]) ).
tcf(c_2086,plain,
( equalish(e_1,e_2)
| ~ product(e_2,e_4,e_3)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_179]) ).
tcf(c_2155,plain,
! [X0: $i,X1: $i] :
( product(e_4,X1,X0)
| ~ product(X0,e_2,e_4)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_436]) ).
tcf(c_2156,plain,
! [X0: $i,X1: $i] :
( product(X1,e_4,e_2)
| ~ product(X0,e_2,e_4)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_429]) ).
tcf(c_2193,plain,
! [X0: $i,X1: $i] :
( product(e_5,X1,X0)
| ~ product(X0,e_3,e_5)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_450]) ).
tcf(c_2194,plain,
! [X0: $i,X1: $i] :
( product(X1,e_5,e_3)
| ~ product(X0,e_3,e_5)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_443]) ).
tcf(c_2200,plain,
! [X0: $i] :
( equalish(e_3,e_2)
| ~ product(X0,e_3,e_5)
| ~ product(X0,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_249]) ).
tcf(c_2201,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_241]) ).
tcf(c_2214,plain,
! [X0: $i] :
( equalish(e_5,e_2)
| ~ product(X0,e_3,e_5)
| ~ product(X0,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_311]) ).
tcf(c_2243,plain,
( equalish(e_4,e_3)
| ~ product(e_3,e_3,e_4)
| ~ product(e_3,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_1042]) ).
tcf(c_2262,plain,
( equalish(e_2,e_3)
| ~ product(e_3,e_2,e_2)
| ~ product(e_2,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_219]) ).
tcf(c_2273,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_5,e_2)
| ~ product(e_1,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_243]) ).
tcf(c_2287,plain,
! [X0: $i] :
( product(e_2,X0,e_3)
| ~ product(e_3,e_5,e_2)
| ~ product(e_5,e_3,X0) ),
inference(instantiation,[status(thm)],[c_562]) ).
tcf(c_2365,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_329]) ).
tcf(c_2368,plain,
! [X0: $i] :
( equalish(e_5,e_1)
| ~ product(X0,e_5,e_3)
| ~ product(X0,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_2369,plain,
! [X0: $i] :
( equalish(e_4,e_5)
| ~ product(X0,e_5,e_3)
| ~ product(X0,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_2376,plain,
( equalish(e_4,e_5)
| ~ product(e_1,e_5,e_3)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_2369]) ).
tcf(c_2421,plain,
( equalish(e_5,e_2)
| ~ product(e_2,e_5,e_2)
| ~ product(e_2,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_1171]) ).
tcf(c_2525,plain,
( equalish(e_4,e_1)
| ~ product(e_5,e_4,e_2)
| ~ product(e_5,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1086]) ).
tcf(c_2527,plain,
( equalish(e_4,e_3)
| ~ product(e_5,e_4,e_2)
| ~ product(e_5,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_1084]) ).
tcf(c_2542,plain,
( equalish(e_5,e_2)
| ~ product(e_5,e_2,e_2)
| ~ product(e_2,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_1204]) ).
tcf(c_2564,plain,
! [X0: $i,X1: $i] :
( ~ cycle(e_5,e_0)
| ~ cycle(e_4,e_0)
| ~ next(e_4,e_5)
| ~ greater(e_4,X0)
| ~ greater(X1,e_0)
| ~ cycle(X0,X1) ),
inference(instantiation,[status(thm)],[c_369]) ).
tcf(c_2631,plain,
( ~ cycle(e_5,e_0)
| ~ cycle(e_4,e_0)
| ~ cycle(e_3,e_1)
| ~ greater(e_4,e_3)
| ~ greater(e_1,e_0)
| ~ next(e_4,e_5) ),
inference(instantiation,[status(thm)],[c_2564]) ).
tcf(c_2632,plain,
( ~ cycle(e_5,e_0)
| ~ cycle(e_4,e_0)
| ~ cycle(e_2,e_3)
| ~ greater(e_4,e_2)
| ~ greater(e_3,e_0)
| ~ next(e_4,e_5) ),
inference(instantiation,[status(thm)],[c_2564]) ).
tcf(c_2701,plain,
( product(e_3,e_1,e_5)
| ~ product(e_5,e_4,e_3)
| ~ product(e_4,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_1501]) ).
tcf(c_2710,plain,
( product(e_4,e_2,e_2)
| ~ product(e_2,e_2,e_4)
| ~ product(e_2,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_2155]) ).
tcf(c_2723,plain,
! [X0: $i,X1: $i] :
( product(e_3,X1,e_2)
| ~ product(e_2,X0,e_3)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_416]) ).
tcf(c_2854,plain,
! [X0: $i] :
( product(e_3,e_5,X0)
| ~ product(e_4,X0,e_5)
| ~ product(X0,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_1501]) ).
tcf(c_2855,plain,
! [X0: $i] :
( product(e_5,e_3,e_4)
| ~ product(e_4,X0,e_5)
| ~ product(X0,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_1502]) ).
tcf(c_2862,plain,
( product(e_5,e_3,e_4)
| ~ product(e_4,e_1,e_5)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_2855]) ).
tcf(c_2863,plain,
( product(e_3,e_5,e_1)
| ~ product(e_4,e_1,e_5)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_2854]) ).
tcf(c_2975,plain,
! [X0: $i] :
( product(e_5,X0,e_3)
| ~ product(e_3,e_2,e_5)
| ~ product(e_2,e_3,X0) ),
inference(instantiation,[status(thm)],[c_450]) ).
tcf(c_2978,plain,
( product(e_5,e_1,e_3)
| ~ product(e_3,e_2,e_5)
| ~ product(e_2,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_2975]) ).
tcf(c_2988,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_187]) ).
tcf(c_3015,plain,
( equalish(e_2,e_4)
| ~ product(e_4,e_2,e_2)
| ~ product(e_2,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_227]) ).
tcf(c_3042,plain,
( equalish(e_5,e_3)
| ~ product(e_5,e_2,e_4)
| ~ product(e_3,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_323]) ).
tcf(c_3044,plain,
( equalish(e_5,e_1)
| ~ product(e_5,e_2,e_4)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_307]) ).
tcf(c_3048,plain,
( equalish(e_1,e_5)
| ~ product(e_5,e_2,e_4)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_203]) ).
tcf(c_3049,plain,
! [X0: $i] :
( product(e_4,X0,e_5)
| ~ product(e_5,e_2,e_4)
| ~ product(e_2,e_5,X0) ),
inference(instantiation,[status(thm)],[c_650]) ).
tcf(c_3050,plain,
( product(e_4,e_1,e_5)
| ~ product(e_5,e_2,e_4)
| ~ product(e_2,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_3049]) ).
tcf(c_3059,plain,
( equalish(e_1,e_2)
| ~ product(e_2,e_3,e_4)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_179]) ).
tcf(c_3179,plain,
! [X0: $i] :
( equalish(e_2,e_1)
| ~ product(X0,e_2,e_5)
| ~ product(X0,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_209]) ).
tcf(c_3238,plain,
! [X0: $i] :
( equalish(e_5,e_4)
| ~ product(X0,e_5,e_4)
| ~ product(X0,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_3239,plain,
! [X0: $i] :
( equalish(e_5,e_3)
| ~ product(X0,e_5,e_4)
| ~ product(X0,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_321]) ).
tcf(c_3241,plain,
! [X0: $i] :
( equalish(e_5,e_1)
| ~ product(X0,e_5,e_4)
| ~ product(X0,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_3243,plain,
! [X0: $i] :
( equalish(e_3,e_5)
| ~ product(X0,e_5,e_4)
| ~ product(X0,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_265]) ).
tcf(c_3248,plain,
( equalish(e_3,e_5)
| ~ product(e_1,e_5,e_4)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_3243]) ).
tcf(c_3362,plain,
( equalish(e_3,e_5)
| ~ product(e_5,e_3,e_3)
| ~ product(e_3,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_267]) ).
tcf(c_3409,plain,
( product(e_2,e_3,e_4)
| ~ product(e_5,e_4,e_3)
| ~ product(e_4,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_1158]) ).
tcf(c_3414,plain,
( equalish(e_5,e_1)
| ~ product(e_5,e_4,e_3)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_307]) ).
tcf(c_3417,plain,
( equalish(e_2,e_5)
| ~ product(e_5,e_4,e_3)
| ~ product(e_2,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_235]) ).
tcf(c_3418,plain,
( equalish(e_1,e_5)
| ~ product(e_5,e_4,e_3)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_203]) ).
tcf(c_3487,plain,
! [X0: $i] :
( equalish(e_5,e_2)
| ~ product(e_5,X0,e_3)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_315]) ).
tcf(c_3498,plain,
( equalish(e_5,e_2)
| ~ product(e_5,e_1,e_3)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_3487]) ).
tcf(c_3563,plain,
( ~ cycle(e_5,e_0)
| ~ cycle(e_4,e_0)
| ~ cycle(e_2,e_4)
| ~ greater(e_4,e_2)
| ~ greater(e_4,e_0)
| ~ next(e_4,e_5) ),
inference(instantiation,[status(thm)],[c_2564]) ).
tcf(c_3571,plain,
( equalish(e_5,e_3)
| ~ cycle(e_2,e_4)
| ~ greater(e_4,e_0)
| ~ next(e_2,e_3)
| ~ product(e_2,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_658]) ).
tcf(c_3760,plain,
( equalish(e_3,e_2)
| ~ product(e_2,e_3,e_2)
| ~ product(e_2,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_999]) ).
tcf(c_4011,plain,
( equalish(e_5,e_3)
| ~ product(e_4,e_5,e_2)
| ~ product(e_4,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_1170]) ).
tcf(c_4022,plain,
( equalish(e_3,e_1)
| ~ product(e_2,e_3,e_4)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_1299]) ).
tcf(c_4062,plain,
( equalish(e_4,e_3)
| ~ product(e_3,e_4,e_3)
| ~ product(e_3,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_1515]) ).
tcf(c_4074,plain,
( equalish(e_4,e_1)
| ~ product(e_2,e_4,e_3)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_1517]) ).
tcf(c_4078,plain,
( equalish(e_4,e_1)
| ~ product(e_5,e_4,e_3)
| ~ product(e_5,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_1517]) ).
tcf(c_4116,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_3,e_3)
| ~ product(e_3,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_1549]) ).
tcf(c_4220,plain,
( equalish(e_5,e_4)
| ~ product(e_2,e_5,e_3)
| ~ product(e_2,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_2365]) ).
tcf(c_4238,plain,
( equalish(e_5,e_1)
| ~ product(e_2,e_5,e_3)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_2368]) ).
tcf(c_4264,plain,
( ~ cycle(e_5,e_0)
| ~ cycle(e_4,e_0)
| ~ cycle(e_3,e_3)
| ~ greater(e_4,e_3)
| ~ greater(e_3,e_0)
| ~ next(e_4,e_5) ),
inference(instantiation,[status(thm)],[c_2564]) ).
tcf(c_4584,plain,
( product(e_3,e_3,e_4)
| ~ product(e_5,e_4,e_3)
| ~ product(e_4,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_1502]) ).
tcf(c_4605,plain,
! [X0: $i] :
( product(X0,e_3,e_5)
| ~ product(e_4,e_5,e_3)
| ~ product(e_5,e_4,X0) ),
inference(instantiation,[status(thm)],[c_1535]) ).
tcf(c_4606,plain,
! [X0: $i] :
( product(e_3,X0,e_4)
| ~ product(e_4,e_5,e_3)
| ~ product(e_5,e_4,X0) ),
inference(instantiation,[status(thm)],[c_1534]) ).
tcf(c_4607,plain,
( product(e_3,e_1,e_4)
| ~ product(e_5,e_4,e_1)
| ~ product(e_4,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_4606]) ).
tcf(c_4608,plain,
( product(e_1,e_3,e_5)
| ~ product(e_5,e_4,e_1)
| ~ product(e_4,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_4605]) ).
tcf(c_4624,plain,
( product(e_5,e_2,e_4)
| ~ product(e_4,e_3,e_5)
| ~ product(e_3,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_2193]) ).
tcf(c_4625,plain,
( product(e_2,e_5,e_3)
| ~ product(e_4,e_3,e_5)
| ~ product(e_3,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_2194]) ).
tcf(c_4626,plain,
( product(e_2,e_2,e_4)
| ~ product(e_4,e_3,e_2)
| ~ product(e_3,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_990]) ).
tcf(c_4629,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_4,e_2)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_243]) ).
tcf(c_4631,plain,
( equalish(e_1,e_3)
| ~ product(e_3,e_4,e_2)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_187]) ).
tcf(c_4647,plain,
( equalish(e_5,e_4)
| ~ product(e_3,e_5,e_2)
| ~ product(e_3,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_1169]) ).
tcf(c_4656,plain,
! [X0: $i] :
( product(e_2,X0,e_3)
| ~ product(e_3,e_4,e_2)
| ~ product(e_4,e_3,X0) ),
inference(instantiation,[status(thm)],[c_1074]) ).
tcf(c_4657,plain,
! [X0: $i] :
( product(X0,e_2,e_4)
| ~ product(e_3,e_4,e_2)
| ~ product(e_4,e_3,X0) ),
inference(instantiation,[status(thm)],[c_1075]) ).
tcf(c_4658,plain,
( product(e_1,e_2,e_4)
| ~ product(e_4,e_3,e_1)
| ~ product(e_3,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_4657]) ).
tcf(c_4659,plain,
( product(e_2,e_1,e_3)
| ~ product(e_4,e_3,e_1)
| ~ product(e_3,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_4656]) ).
tcf(c_4700,plain,
( equalish(e_3,e_1)
| ~ product(e_5,e_3,e_4)
| ~ product(e_5,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_1299]) ).
tcf(c_4701,plain,
( equalish(e_3,e_2)
| ~ product(e_5,e_3,e_4)
| ~ product(e_5,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_1298]) ).
tcf(c_4703,plain,
( product(e_4,e_4,e_3)
| ~ product(e_5,e_3,e_4)
| ~ product(e_3,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_1391]) ).
tcf(c_4704,plain,
! [X0: $i] :
( product(e_4,X0,e_5)
| ~ product(e_5,e_3,e_4)
| ~ product(e_3,e_5,X0) ),
inference(instantiation,[status(thm)],[c_1293]) ).
tcf(c_4705,plain,
! [X0: $i] :
( product(X0,e_4,e_3)
| ~ product(e_5,e_3,e_4)
| ~ product(e_3,e_5,X0) ),
inference(instantiation,[status(thm)],[c_1294]) ).
tcf(c_4706,plain,
( product(e_1,e_4,e_3)
| ~ product(e_5,e_3,e_4)
| ~ product(e_3,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_4705]) ).
tcf(c_4707,plain,
( product(e_4,e_1,e_5)
| ~ product(e_5,e_3,e_4)
| ~ product(e_3,e_5,e_1) ),
inference(instantiation,[status(thm)],[c_4704]) ).
tcf(c_4709,plain,
( product(e_2,e_4,e_3)
| ~ product(e_5,e_3,e_4)
| ~ product(e_3,e_5,e_2) ),
inference(instantiation,[status(thm)],[c_2287]) ).
tcf(c_4777,plain,
! [X0: $i] :
( equalish(e_5,e_4)
| ~ product(e_5,e_4,X0)
| ~ product(e_4,e_4,X0) ),
inference(instantiation,[status(thm)],[c_331]) ).
tcf(c_4852,plain,
! [X0: $i] :
( equalish(e_3,e_1)
| ~ product(e_4,e_3,X0)
| ~ product(e_4,e_1,X0) ),
inference(instantiation,[status(thm)],[c_241]) ).
tcf(c_4979,plain,
! [X0: $i] :
( equalish(e_5,e_3)
| ~ product(e_3,e_5,X0)
| ~ product(e_3,e_3,X0) ),
inference(instantiation,[status(thm)],[c_321]) ).
tcf(c_5109,plain,
( product(e_3,e_3,e_2)
| ~ product(e_5,e_2,e_3)
| ~ product(e_2,e_5,e_3) ),
inference(instantiation,[status(thm)],[c_2723]) ).
tcf(c_5131,plain,
( equalish(e_4,e_2)
| ~ product(e_5,e_4,e_3)
| ~ product(e_5,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_1516]) ).
tcf(c_5179,plain,
( equalish(e_4,e_2)
| ~ product(e_2,e_4,e_2)
| ~ product(e_2,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_1085]) ).
tcf(c_5192,plain,
( product(e_3,e_4,e_5)
| ~ product(e_5,e_2,e_3)
| ~ product(e_2,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_898]) ).
tcf(c_5194,plain,
( equalish(e_2,e_1)
| ~ product(e_2,e_5,e_4)
| ~ product(e_1,e_5,e_4) ),
inference(instantiation,[status(thm)],[c_211]) ).
tcf(c_5530,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_3,e_5)
| ~ product(e_1,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_1119]) ).
tcf(c_5612,plain,
( equalish(e_3,e_2)
| ~ product(e_4,e_3,e_5)
| ~ product(e_4,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_2200]) ).
tcf(c_5614,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_2201]) ).
tcf(c_5959,plain,
( equalish(e_2,e_1)
| ~ product(e_4,e_2,e_5)
| ~ product(e_4,e_1,e_5) ),
inference(instantiation,[status(thm)],[c_3179]) ).
tcf(c_6026,plain,
( equalish(e_5,e_4)
| ~ product(e_4,e_5,e_4)
| ~ product(e_4,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_3238]) ).
tcf(c_6035,plain,
( equalish(e_5,e_3)
| ~ product(e_2,e_5,e_4)
| ~ product(e_2,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_3239]) ).
tcf(c_6047,plain,
( equalish(e_5,e_1)
| ~ product(e_2,e_5,e_4)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_3241]) ).
tcf(c_6333,plain,
! [X0: $i] :
( product(e_4,e_4,e_2)
| ~ product(e_2,X0,e_4)
| ~ product(X0,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_2156]) ).
tcf(c_6335,plain,
! [X0: $i] :
( product(e_4,e_3,e_2)
| ~ product(e_2,X0,e_4)
| ~ product(X0,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_899]) ).
tcf(c_6340,plain,
( product(e_4,e_3,e_2)
| ~ product(e_2,e_1,e_4)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_6335]) ).
tcf(c_6342,plain,
( product(e_4,e_4,e_2)
| ~ product(e_2,e_1,e_4)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_6333]) ).
tcf(c_6348,plain,
! [X0: $i] :
( equalish(e_3,e_4)
| ~ product(e_2,X0,e_4)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_255]) ).
tcf(c_6353,plain,
( equalish(e_3,e_4)
| ~ product(e_2,e_1,e_4)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_6348]) ).
tcf(c_6631,plain,
! [X0: $i] :
( product(e_5,e_5,e_4)
| ~ product(e_4,X0,e_5)
| ~ product(X0,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_1110]) ).
tcf(c_6633,plain,
! [X0: $i] :
( equalish(e_4,e_2)
| ~ product(X0,e_4,e_5)
| ~ product(X0,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_281]) ).
tcf(c_6642,plain,
( equalish(e_4,e_2)
| ~ product(e_1,e_4,e_5)
| ~ product(e_1,e_2,e_5) ),
inference(instantiation,[status(thm)],[c_6633]) ).
tcf(c_6644,plain,
( product(e_5,e_5,e_4)
| ~ product(e_4,e_1,e_5)
| ~ product(e_1,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_6631]) ).
tcf(c_6764,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_3,e_5)
| ~ product(e_2,e_3,e_5) ),
inference(instantiation,[status(thm)],[c_1118]) ).
tcf(c_6944,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_4777]) ).
tcf(c_7067,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_4979]) ).
tcf(c_7254,plain,
( product(e_3,e_5,e_4)
| ~ product(e_4,e_2,e_3)
| ~ product(e_2,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_1433]) ).
tcf(c_7256,plain,
( product(e_5,e_3,e_2)
| ~ product(e_4,e_2,e_3)
| ~ product(e_2,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_1362]) ).
tcf(c_7470,plain,
( equalish(e_5,e_2)
| ~ product(e_4,e_3,e_5)
| ~ product(e_4,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_2214]) ).
tcf(c_7490,plain,
( equalish(e_3,e_1)
| ~ product(e_4,e_3,e_2)
| ~ product(e_4,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_4852]) ).
tcf(c_7511,plain,
( product(e_5,e_5,e_3)
| ~ product(e_4,e_3,e_5)
| ~ product(e_3,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_2194]) ).
tcf(c_7512,plain,
( product(e_2,e_5,e_4)
| ~ product(e_4,e_3,e_2)
| ~ product(e_3,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_990]) ).
tcf(c_7513,plain,
( product(e_5,e_2,e_3)
| ~ product(e_4,e_3,e_2)
| ~ product(e_3,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_991]) ).
tcf(c_7514,plain,
( equalish(e_3,e_2)
| ~ product(e_3,e_4,e_5)
| ~ product(e_2,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_251]) ).
tcf(c_7515,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_4,e_5)
| ~ product(e_1,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_243]) ).
tcf(c_7516,plain,
( equalish(e_2,e_3)
| ~ product(e_3,e_4,e_5)
| ~ product(e_2,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_219]) ).
tcf(c_7536,plain,
! [X0: $i] :
( product(e_5,X0,e_3)
| ~ product(e_3,e_4,e_5)
| ~ product(e_4,e_3,X0) ),
inference(instantiation,[status(thm)],[c_562]) ).
tcf(c_7537,plain,
( product(e_5,e_1,e_3)
| ~ product(e_4,e_3,e_1)
| ~ product(e_3,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_7536]) ).
tcf(c_7887,plain,
( equalish(e_2,e_1)
| ~ product(e_2,e_4,e_5)
| ~ product(e_1,e_4,e_5) ),
inference(instantiation,[status(thm)],[c_945]) ).
tcf(c_8322,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_7887,c_7537,c_7511,c_7512,c_7513,c_7514,c_7515,c_7516,c_7490,c_7470,c_7254,c_7256,c_7067,c_6944,c_6764,c_6644,c_6642,c_6353,c_6342,c_6340,c_6047,c_6035,c_6026,c_5959,c_5614,c_5612,c_5530,c_5192,c_5194,c_5179,c_5131,c_5109,c_4709,c_4700,c_4701,c_4703,c_4707,c_4706,c_4647,c_4659,c_4658,c_4624,c_4625,c_4626,c_4629,c_4631,c_4608,c_4607,c_4584,c_4264,c_4238,c_4220,c_4116,c_4078,c_4074,c_4062,c_4022,c_4011,c_3760,c_3571,c_3563,c_3498,c_3409,c_3414,c_3417,c_3418,c_3362,c_3248,c_3059,c_3050,c_3042,c_3044,c_3048,c_3015,c_2988,c_2978,c_2863,c_2862,c_2710,c_2701,c_2632,c_2631,c_2542,c_2525,c_2527,c_2421,c_2376,c_2273,c_2262,c_2243,c_2083,c_2085,c_2086,c_2057,c_2012,c_2014,c_2018,c_1993,c_1981,c_1982,c_1984,c_1985,c_1975,c_1976,c_1931,c_1921,c_1922,c_1916,c_1894,c_1889,c_1869,c_1861,c_1847,c_1837,c_1784,c_1767,c_1756,c_1713,c_1669,c_1670,c_1659,c_1559,c_1257,c_1256,c_1255,c_1253,c_1251,c_1247,c_1225,c_1145,c_1128,c_1099,c_1101,c_1103,c_1105,c_1097,c_1095,c_1065,c_1068,c_1061,c_1054,c_1039,c_1015,c_1008,c_977,c_954,c_949,c_927,c_920,c_915,c_857,c_858,c_859,c_860,c_849,c_850,c_851,c_841,c_842,c_827,c_828,c_829,c_821,c_822,c_815,c_816,c_805,c_806,c_801,c_797,c_788,c_659,c_652,c_641,c_634,c_449,c_442,c_439,c_438,c_435,c_428,c_425,c_424,c_408,c_405,c_401,c_394,c_391,c_390,c_389,c_387,c_384,c_348,c_347,c_204,c_202,c_200,c_196,c_194,c_192,c_186,c_184,c_180,c_178,c_176,c_139,c_140,c_141,c_142,c_143,c_144,c_145,c_146,c_147,c_148,c_149,c_150,c_151,c_152,c_153,c_154,c_155,c_156,c_157,c_158,c_165,c_107,c_109,c_110,c_111,c_112,c_113,c_114,c_115,c_122,c_123,c_124,c_129,c_134,c_135,c_136,c_137,c_138]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP125-3.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.37 % Computer : n019.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 13:41:22 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.41 Running EPR theorem proving
% 0.09/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s epr_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.42
% 0.09/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.42
% 0.09/0.42 % Detected problem language: tptp
% 0.09/0.43 % Proving...
% 2.49/1.13 % SZS status Started for theBenchmark.p
% 2.49/1.13 % SZS status Unsatisfiable for theBenchmark.p
% 2.49/1.13
% 2.49/1.13 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.49/1.13
% 2.49/1.13 % ------ iProver source info
% 2.49/1.13
% 2.49/1.13 % git: date: 2026-07-19 20:42:38 +0200
% 2.49/1.13 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.49/1.13 % git: non_committed_changes: false
% 2.49/1.13
% 2.49/1.13 % ------ Parsing...% successful
% 2.49/1.13
% 2.49/1.13
% 2.49/1.13 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 2.49/1.13 % ------ Proving...
% 2.49/1.13 % ------ Problem Properties
% 2.49/1.13
% 2.49/1.13 %
% 2.49/1.13 % clauses 58
% 2.49/1.13 % conjectures 1
% 2.49/1.13 % EPR 58
% 2.49/1.13 % Horn 56
% 2.49/1.13 % unary 47
% 2.49/1.13 % binary 0
% 2.49/1.13 % lits 95
% 2.49/1.13 % lits eq 0
% 2.49/1.13 % fd_pure 0
% 2.49/1.13 % fd_pseudo 0
% 2.49/1.13 % fd_cond 0
% 2.49/1.13 % fd_pseudo_cond 0
% 2.49/1.13 % AC symbols 0
% 2.49/1.13
% 2.49/1.13 % ------ Input Options Time Limit: Unbounded
% 2.49/1.13
% 2.49/1.13
% 2.49/1.13 % ------
% 2.49/1.13 % Current options:
% 2.49/1.13 % ------
% 2.49/1.13
% 2.49/1.13
% 2.49/1.13 %
% 2.49/1.13
% 2.49/1.13 % ------ Proving...
% 2.49/1.13 %
% 2.49/1.13
% 2.49/1.13 % SZS status Unsatisfiable for theBenchmark.p
% 2.49/1.13
% 2.49/1.13 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.15/1.14
% 4.15/1.14
%------------------------------------------------------------------------------