%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP129-4.004 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n017.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:28 PM UTC 2026
% Result : Unsatisfiable 2.09s 6.16s
% Output : CNFRefutation 2.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 22
% Syntax : Number of formulae : 401 ( 27 unt; 0 def)
% Number of atoms : 1295 ( 0 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 1647 ( 753 ~; 894 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 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 : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 377 ( 0 sgn 377 !; 0 ?; 347 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( product(e_4,X0,X1)
| product(e_3,X0,X1)
| product(e_2,X0,X1)
| product(e_1,X0,X1)
| ~ group_element(X1)
| ~ group_element(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',row_surjectivity) ).
fof(f2,axiom,
! [X0,X1] :
( product(X0,e_4,X1)
| product(X0,e_3,X1)
| product(X0,e_2,X1)
| product(X0,e_1,X1)
| ~ group_element(X1)
| ~ group_element(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',column_surjectivity) ).
fof(f3,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ product(X1,X2,X3)
| ~ product(X2,X0,X3)
| product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg3_1) ).
fof(f4,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ product(X3,X0,X1)
| ~ product(X1,X3,X2)
| product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg3_2) ).
fof(f5,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
fof(f6,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
fof(f7,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
fof(f8,axiom,
group_element(e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_4) ).
fof(f9,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f10,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f11,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
fof(f15,axiom,
~ equalish(e_3,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_1) ).
fof(f16,axiom,
~ equalish(e_3,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_2) ).
fof(f17,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
fof(f18,axiom,
~ equalish(e_4,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_1) ).
fof(f19,axiom,
~ equalish(e_4,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_2) ).
fof(f20,axiom,
~ equalish(e_4,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_3) ).
fof(f21,axiom,
! [X0,X1] :
( 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(f22,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(f23,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(f24,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(f25,negated_conjecture,
! [X2,X3,X0,X1] :
( product(X2,X0,X3)
| ~ product(X1,X2,X3)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg3) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( product(e_4,X0,X1)
| product(e_3,X0,X1)
| product(e_2,X0,X1)
| product(e_1,X0,X1)
| ~ group_element(X1)
| ~ group_element(X0) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i] :
( product(X0,e_4,X1)
| product(X0,e_3,X1)
| product(X0,e_2,X1)
| product(X0,e_1,X1)
| ~ group_element(X1)
| ~ group_element(X0) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_76,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( product(X3,X0,X1)
| ~ product(X1,X3,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_77,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( product(X3,X0,X2)
| ~ product(X1,X3,X0)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f4]) ).
tcf(c_78,plain,
group_element(e_1),
inference(cnf_transformation,[],[f5]) ).
tcf(c_79,plain,
group_element(e_2),
inference(cnf_transformation,[],[f6]) ).
tcf(c_80,plain,
group_element(e_3),
inference(cnf_transformation,[],[f7]) ).
tcf(c_81,plain,
group_element(e_4),
inference(cnf_transformation,[],[f8]) ).
tcf(c_82,plain,
~ equalish(e_1,e_2),
inference(cnf_transformation,[],[f9]) ).
tcf(c_83,plain,
~ equalish(e_1,e_3),
inference(cnf_transformation,[],[f10]) ).
tcf(c_84,plain,
~ equalish(e_1,e_4),
inference(cnf_transformation,[],[f11]) ).
tcf(c_88,plain,
~ equalish(e_3,e_1),
inference(cnf_transformation,[],[f15]) ).
tcf(c_89,plain,
~ equalish(e_3,e_2),
inference(cnf_transformation,[],[f16]) ).
tcf(c_90,plain,
~ equalish(e_3,e_4),
inference(cnf_transformation,[],[f17]) ).
tcf(c_91,plain,
~ equalish(e_4,e_1),
inference(cnf_transformation,[],[f18]) ).
tcf(c_92,plain,
~ equalish(e_4,e_2),
inference(cnf_transformation,[],[f19]) ).
tcf(c_93,plain,
~ equalish(e_4,e_3),
inference(cnf_transformation,[],[f20]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i] :
( 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) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equalish(X2,X3)
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equalish(X1,X3)
| ~ product(X0,X3,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equalish(X0,X3)
| ~ product(X3,X1,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_98,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( product(X2,X0,X3)
| ~ product(X1,X2,X3)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_100,plain,
( product(e_1,e_1,e_4)
| product(e_1,e_1,e_3)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_1)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_101,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_3,e_1)
| product(e_1,e_2,e_1)
| product(e_1,e_1,e_1)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_103,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_95]) ).
tcf(c_104,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_103]) ).
tcf(c_107,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_97]) ).
tcf(c_111,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_96]) ).
tcf(c_115,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_95]) ).
tcf(c_117,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_96]) ).
tcf(c_119,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_97]) ).
tcf(c_139,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_95]) ).
tcf(c_140,plain,
( equalish(e_3,e_1)
| ~ product(e_1,e_1,e_3)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_139]) ).
tcf(c_141,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_96]) ).
tcf(c_143,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_97]) ).
tcf(c_144,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_147,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_96]) ).
tcf(c_149,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_97]) ).
tcf(c_151,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_95]) ).
tcf(c_153,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_96]) ).
tcf(c_155,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_97]) ).
tcf(c_157,plain,
! [X0: $i,X1: $i] :
( equalish(e_4,e_1)
| ~ product(X0,X1,e_4)
| ~ product(X0,X1,e_1) ),
inference(instantiation,[status(thm)],[c_95]) ).
tcf(c_158,plain,
( equalish(e_4,e_1)
| ~ product(e_1,e_1,e_4)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_157]) ).
tcf(c_159,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_96]) ).
tcf(c_161,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_97]) ).
tcf(c_165,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_96]) ).
tcf(c_167,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_97]) ).
tcf(c_169,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_95]) ).
tcf(c_171,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_96]) ).
tcf(c_173,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_97]) ).
tcf(c_176,plain,
! [X0: $i] :
( product(e_4,X0,e_2)
| product(e_3,X0,e_2)
| product(e_2,X0,e_2)
| product(e_1,X0,e_2)
| ~ group_element(e_2)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_177,plain,
( product(e_4,e_1,e_2)
| product(e_3,e_1,e_2)
| product(e_2,e_1,e_2)
| product(e_1,e_1,e_2)
| ~ group_element(e_2)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_176]) ).
tcf(c_181,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X0,e_2)
| ~ product(e_2,X2,X1)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_183,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X0,e_2)
| ~ product(X1,X2,e_2)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_184,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X1,X2,e_2)
| ~ product(X2,X0,e_2)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_186,plain,
! [X0: $i] :
( product(e_4,e_2,X0)
| product(e_3,e_2,X0)
| product(e_2,e_2,X0)
| product(e_1,e_2,X0)
| ~ group_element(e_2)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_187,plain,
( product(e_4,e_2,e_1)
| product(e_3,e_2,e_1)
| product(e_2,e_2,e_1)
| product(e_1,e_2,e_1)
| ~ group_element(e_2)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_186]) ).
tcf(c_190,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X1,e_2,X2)
| ~ product(e_2,X0,X1)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_192,plain,
! [X0: $i] :
( 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_94]) ).
tcf(c_193,plain,
( product(e_1,e_2,e_4)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_1)
| ~ group_element(e_2)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_192]) ).
tcf(c_194,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X1,e_2,X2)
| ~ product(e_2,X0,X2)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_197,plain,
! [X0: $i] :
( product(e_2,e_4,X0)
| product(e_2,e_3,X0)
| product(e_2,e_2,X0)
| product(e_2,e_1,X0)
| ~ group_element(e_2)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_199,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_2,X0,X1)
| ~ product(X1,e_2,X2)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_201,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_2,X0,X2)
| ~ product(X1,e_2,X2)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_204,plain,
! [X0: $i] :
( 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_94]) ).
tcf(c_206,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_2,X0,X2)
| ~ product(X1,e_2,X0)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_208,plain,
! [X0: $i] :
( product(e_4,X0,e_3)
| product(e_3,X0,e_3)
| product(e_2,X0,e_3)
| product(e_1,X0,e_3)
| ~ group_element(e_3)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_209,plain,
( product(e_4,e_1,e_3)
| product(e_3,e_1,e_3)
| product(e_2,e_1,e_3)
| product(e_1,e_1,e_3)
| ~ group_element(e_3)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_208]) ).
tcf(c_211,plain,
! [X0: $i] :
( product(X0,e_4,e_3)
| product(X0,e_3,e_3)
| product(X0,e_2,e_3)
| product(X0,e_1,e_3)
| ~ group_element(e_3)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_212,plain,
( product(e_1,e_4,e_3)
| product(e_1,e_3,e_3)
| product(e_1,e_2,e_3)
| product(e_1,e_1,e_3)
| ~ group_element(e_3)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_211]) ).
tcf(c_213,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X0,e_3)
| ~ product(e_3,X2,X1)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_215,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X0,e_3)
| ~ product(X1,X2,e_3)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_216,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X1,X2,e_3)
| ~ product(X2,X0,e_3)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_217,plain,
! [X0: $i] :
( equalish(e_1,e_3)
| ~ product(e_1,e_3,X0)
| ~ product(e_1,e_1,X0) ),
inference(instantiation,[status(thm)],[c_111]) ).
tcf(c_218,plain,
! [X0: $i] :
( product(e_4,e_3,X0)
| product(e_3,e_3,X0)
| product(e_2,e_3,X0)
| product(e_1,e_3,X0)
| ~ group_element(e_3)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_219,plain,
( product(e_4,e_3,e_1)
| product(e_3,e_3,e_1)
| product(e_2,e_3,e_1)
| product(e_1,e_3,e_1)
| ~ group_element(e_3)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_218]) ).
tcf(c_220,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X1,e_3,X0)
| ~ product(e_3,X0,X2)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_222,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X1,e_3,X2)
| ~ product(e_3,X0,X1)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_224,plain,
! [X0: $i] :
( 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_94]) ).
tcf(c_225,plain,
( 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_224]) ).
tcf(c_226,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X1,e_3,X2)
| ~ product(e_3,X0,X2)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_229,plain,
! [X0: $i] :
( product(e_3,e_4,X0)
| product(e_3,e_3,X0)
| product(e_3,e_2,X0)
| product(e_3,e_1,X0)
| ~ group_element(e_3)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_230,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_3,e_1)
| product(e_3,e_2,e_1)
| product(e_3,e_1,e_1)
| ~ group_element(e_3)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_229]) ).
tcf(c_231,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_3,X0,X1)
| ~ product(X1,e_3,X2)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_233,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_3,X0,X2)
| ~ product(X1,e_3,X2)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_236,plain,
! [X0: $i] :
( 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_94]) ).
tcf(c_237,plain,
( product(e_3,e_1,e_4)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_1)
| ~ group_element(e_3)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_236]) ).
tcf(c_238,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_3,X0,X2)
| ~ product(X1,e_3,X0)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_240,plain,
! [X0: $i] :
( product(e_4,X0,e_4)
| product(e_3,X0,e_4)
| product(e_2,X0,e_4)
| product(e_1,X0,e_4)
| ~ group_element(e_4)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_241,plain,
( product(e_4,e_1,e_4)
| product(e_3,e_1,e_4)
| product(e_2,e_1,e_4)
| product(e_1,e_1,e_4)
| ~ group_element(e_4)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_240]) ).
tcf(c_243,plain,
! [X0: $i] :
( product(X0,e_4,e_4)
| product(X0,e_3,e_4)
| product(X0,e_2,e_4)
| product(X0,e_1,e_4)
| ~ group_element(e_4)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_244,plain,
( product(e_1,e_4,e_4)
| product(e_1,e_3,e_4)
| product(e_1,e_2,e_4)
| product(e_1,e_1,e_4)
| ~ group_element(e_4)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_243]) ).
tcf(c_245,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X0,e_4)
| ~ product(e_4,X2,X1)
| ~ product(X0,e_4,X1) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_247,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X0,e_4)
| ~ product(X1,X2,e_4)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_248,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X1,X2,e_4)
| ~ product(X2,X0,e_4)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_259,plain,
! [X0: $i] :
( product(e_4,e_4,X0)
| product(e_3,e_4,X0)
| product(e_2,e_4,X0)
| product(e_1,e_4,X0)
| ~ group_element(e_4)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_262,plain,
( product(e_4,e_4,e_1)
| product(e_3,e_4,e_1)
| product(e_2,e_4,e_1)
| product(e_1,e_4,e_1)
| ~ group_element(e_4)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_259]) ).
tcf(c_274,plain,
! [X0: $i] :
( product(e_4,e_4,X0)
| product(e_4,e_3,X0)
| product(e_4,e_2,X0)
| product(e_4,e_1,X0)
| ~ group_element(e_4)
| ~ group_element(X0) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_276,plain,
! [X0: $i] :
( equalish(e_1,e_4)
| ~ product(e_4,e_3,X0)
| ~ product(e_1,e_3,X0) ),
inference(instantiation,[status(thm)],[c_119]) ).
tcf(c_277,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_3,e_1)
| product(e_4,e_2,e_1)
| product(e_4,e_1,e_1)
| ~ group_element(e_4)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_274]) ).
tcf(c_284,plain,
! [X0: $i] :
( equalish(e_1,e_4)
| ~ product(e_2,X0,e_4)
| ~ product(e_2,X0,e_1) ),
inference(instantiation,[status(thm)],[c_115]) ).
tcf(c_286,plain,
( equalish(e_1,e_4)
| ~ product(e_2,e_1,e_4)
| ~ product(e_2,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_284]) ).
tcf(c_287,plain,
! [X0: $i] :
( equalish(e_1,e_4)
| ~ product(X0,e_3,e_4)
| ~ product(X0,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_115]) ).
tcf(c_322,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X0,X1)
| ~ product(X1,X2,e_4)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_323,plain,
( product(e_1,e_1,e_1)
| ~ product(e_1,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_322]) ).
tcf(c_324,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X1,e_4,X2)
| ~ product(e_4,X0,X2)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_328,plain,
! [X0: $i] :
( equalish(e_1,e_3)
| ~ product(X0,e_3,e_4)
| ~ product(X0,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_111]) ).
tcf(c_329,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_141]) ).
tcf(c_333,plain,
! [X0: $i] :
( 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_94]) ).
tcf(c_334,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ product(X0,e_4,e_4)
| ~ product(X0,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_335,plain,
! [X0: $i] :
( equalish(e_4,e_2)
| ~ product(X0,e_4,e_4)
| ~ product(X0,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_165]) ).
tcf(c_336,plain,
! [X0: $i] :
( equalish(e_4,e_1)
| ~ product(X0,e_4,e_4)
| ~ product(X0,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_337,plain,
! [X0: $i] :
( equalish(e_3,e_4)
| ~ product(X0,e_4,e_4)
| ~ product(X0,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_153]) ).
tcf(c_340,plain,
( product(e_1,e_4,e_4)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_1)
| ~ group_element(e_4)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_333]) ).
tcf(c_343,plain,
( equalish(e_3,e_4)
| ~ product(e_1,e_4,e_4)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_337]) ).
tcf(c_344,plain,
( equalish(e_4,e_1)
| ~ product(e_1,e_4,e_4)
| ~ product(e_1,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_336]) ).
tcf(c_345,plain,
( equalish(e_4,e_2)
| ~ product(e_1,e_4,e_4)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_335]) ).
tcf(c_346,plain,
( equalish(e_4,e_3)
| ~ product(e_1,e_4,e_4)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_334]) ).
tcf(c_353,plain,
! [X0: $i] :
( 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_94]) ).
tcf(c_354,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ product(e_4,X0,e_4)
| ~ product(e_3,X0,e_4) ),
inference(instantiation,[status(thm)],[c_173]) ).
tcf(c_355,plain,
! [X0: $i] :
( equalish(e_4,e_2)
| ~ product(e_4,X0,e_4)
| ~ product(e_2,X0,e_4) ),
inference(instantiation,[status(thm)],[c_167]) ).
tcf(c_356,plain,
! [X0: $i] :
( equalish(e_4,e_1)
| ~ product(e_4,X0,e_4)
| ~ product(e_1,X0,e_4) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_357,plain,
! [X0: $i] :
( equalish(e_3,e_4)
| ~ product(e_4,X0,e_4)
| ~ product(e_3,X0,e_4) ),
inference(instantiation,[status(thm)],[c_155]) ).
tcf(c_360,plain,
( product(e_4,e_1,e_4)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_1)
| ~ group_element(e_4)
| ~ group_element(e_1) ),
inference(instantiation,[status(thm)],[c_353]) ).
tcf(c_363,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_1,e_4)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_357]) ).
tcf(c_423,plain,
! [X0: $i,X1: $i] :
( product(e_3,e_2,X1)
| ~ product(e_2,X0,e_3)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_190]) ).
tcf(c_452,plain,
! [X0: $i,X1: $i] :
( product(e_3,X0,e_3)
| ~ product(e_3,e_3,X1)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_231]) ).
tcf(c_454,plain,
! [X0: $i,X1: $i] :
( product(e_3,X0,X1)
| ~ product(X1,e_3,e_4)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_231]) ).
tcf(c_460,plain,
! [X0: $i,X1: $i] :
( product(e_3,X0,e_4)
| ~ product(X1,e_3,X0)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_238]) ).
tcf(c_463,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,e_4)
| ~ product(e_3,X1,e_4)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_464,plain,
( product(e_1,e_1,e_4)
| ~ product(e_3,e_1,e_4)
| ~ product(e_1,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_463]) ).
tcf(c_470,plain,
! [X0: $i,X1: $i] :
( product(X1,e_4,e_4)
| ~ product(e_4,X0,e_4)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_248]) ).
tcf(c_472,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,e_4)
| ~ product(X1,e_3,e_4)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_248]) ).
tcf(c_473,plain,
! [X0: $i,X1: $i] :
( product(X1,e_3,e_4)
| ~ product(e_3,X0,X1)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_474,plain,
! [X0: $i,X1: $i] :
( product(e_3,e_3,X1)
| ~ product(X0,e_3,e_3)
| ~ product(e_3,X0,X1) ),
inference(instantiation,[status(thm)],[c_238]) ).
tcf(c_481,plain,
( product(e_3,e_3,e_1)
| ~ product(e_3,e_1,e_1)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_482,plain,
( product(e_1,e_3,e_4)
| ~ product(e_3,e_1,e_1)
| ~ product(e_1,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_473]) ).
tcf(c_483,plain,
( product(e_1,e_1,e_4)
| ~ product(e_3,e_1,e_1)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_472]) ).
tcf(c_485,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X0,X1)
| ~ product(e_3,X2,X0)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_487,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X1,X0,X2)
| ~ product(e_3,X1,X2)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_501,plain,
! [X0: $i,X1: $i] :
( product(e_4,X1,e_4)
| ~ product(X1,X0,e_4)
| ~ product(X0,e_4,X1) ),
inference(instantiation,[status(thm)],[c_248]) ).
tcf(c_503,plain,
! [X0: $i,X1: $i] :
( product(e_3,X0,X1)
| ~ product(e_4,e_3,X0)
| ~ product(X0,e_4,X1) ),
inference(instantiation,[status(thm)],[c_238]) ).
tcf(c_504,plain,
! [X0: $i,X1: $i] :
( product(e_3,X0,e_4)
| ~ product(e_4,e_3,X1)
| ~ product(X0,e_4,X1) ),
inference(instantiation,[status(thm)],[c_231]) ).
tcf(c_510,plain,
( product(e_3,e_1,e_1)
| ~ product(e_4,e_3,e_1)
| ~ product(e_1,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_503]) ).
tcf(c_515,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_4,X0,X2)
| ~ product(X1,e_4,X0)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_516,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_4,X0,X2)
| ~ product(X1,e_4,X2)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_540,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,e_2)
| ~ product(e_4,X1,e_2)
| ~ product(X0,e_4,X1) ),
inference(instantiation,[status(thm)],[c_183]) ).
tcf(c_541,plain,
( product(e_1,e_1,e_2)
| ~ product(e_4,e_1,e_2)
| ~ product(e_1,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_540]) ).
tcf(c_552,plain,
! [X0: $i,X1: $i] :
( product(e_4,e_3,X1)
| ~ product(e_3,X0,e_4)
| ~ product(X0,e_4,X1) ),
inference(instantiation,[status(thm)],[c_222]) ).
tcf(c_553,plain,
( product(e_4,e_3,e_1)
| ~ product(e_3,e_1,e_4)
| ~ product(e_1,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_552]) ).
tcf(c_588,plain,
! [X0: $i,X1: $i] :
( product(X1,e_2,e_2)
| ~ product(e_2,X0,X1)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_190]) ).
tcf(c_599,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X0,X1)
| ~ product(X1,X2,e_2)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_600,plain,
( product(e_1,e_1,e_1)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_599]) ).
tcf(c_707,plain,
( equalish(e_4,e_1)
| ~ product(e_3,e_4,e_2)
| ~ product(e_3,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_708,plain,
( equalish(e_1,e_4)
| ~ product(e_3,e_4,e_2)
| ~ product(e_3,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_725,plain,
( equalish(e_4,e_3)
| ~ product(e_3,e_4,e_2)
| ~ product(e_3,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_727,plain,
! [X0: $i] :
( product(X0,e_3,e_3)
| ~ product(e_3,e_3,e_2)
| ~ product(e_3,X0,e_2) ),
inference(instantiation,[status(thm)],[c_213]) ).
tcf(c_746,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,e_3)
| ~ product(e_3,X1,e_2)
| ~ product(X0,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_213]) ).
tcf(c_747,plain,
( product(e_1,e_1,e_3)
| ~ product(e_3,e_1,e_2)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_746]) ).
tcf(c_753,plain,
( equalish(e_1,e_2)
| ~ product(e_2,e_3,e_2)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_107]) ).
tcf(c_787,plain,
( equalish(e_1,e_4)
| ~ product(e_3,e_2,e_4)
| ~ product(e_3,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_115]) ).
tcf(c_793,plain,
! [X0: $i,X1: $i] :
( product(X0,e_3,X1)
| ~ product(e_3,e_4,X0)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_222]) ).
tcf(c_794,plain,
! [X0: $i,X1: $i] :
( product(X0,e_3,e_4)
| ~ product(e_3,e_4,X1)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_220]) ).
tcf(c_797,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,e_4)
| ~ product(X1,e_4,e_4)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_248]) ).
tcf(c_798,plain,
! [X0: $i,X1: $i] :
( product(X1,e_4,e_4)
| ~ product(e_4,X0,X1)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_799,plain,
! [X0: $i,X1: $i] :
( product(e_3,e_4,X1)
| ~ product(X0,e_3,e_4)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_238]) ).
tcf(c_800,plain,
! [X0: $i,X1: $i] :
( product(e_3,e_4,X0)
| ~ product(e_4,X0,X1)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_231]) ).
tcf(c_808,plain,
( product(e_1,e_1,e_4)
| ~ product(e_4,e_1,e_1)
| ~ product(e_1,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_797]) ).
tcf(c_811,plain,
( product(e_1,e_3,e_4)
| ~ product(e_4,e_1,e_1)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_794]) ).
tcf(c_851,plain,
! [X0: $i] :
( product(X0,e_3,e_4)
| ~ product(e_3,e_4,e_2)
| ~ product(e_4,X0,e_2) ),
inference(instantiation,[status(thm)],[c_245]) ).
tcf(c_853,plain,
( product(e_1,e_3,e_4)
| ~ product(e_4,e_1,e_2)
| ~ product(e_3,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_851]) ).
tcf(c_866,plain,
! [X0: $i,X1: $i] :
( product(e_2,e_4,X1)
| ~ product(X0,e_2,e_4)
| ~ product(e_4,X0,X1) ),
inference(instantiation,[status(thm)],[c_206]) ).
tcf(c_874,plain,
! [X0: $i,X1: $i] :
( product(X1,e_4,e_3)
| ~ product(e_4,X0,X1)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_215]) ).
tcf(c_878,plain,
! [X0: $i] :
( product(e_2,X0,e_3)
| ~ product(e_3,e_2,e_3)
| ~ product(X0,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_215]) ).
tcf(c_879,plain,
( product(e_2,e_1,e_3)
| ~ product(e_3,e_2,e_3)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_878]) ).
tcf(c_936,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_147]) ).
tcf(c_937,plain,
( equalish(e_3,e_2)
| ~ product(e_1,e_3,e_2)
| ~ product(e_1,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_936]) ).
tcf(c_943,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,e_3)
| ~ product(e_2,X1,e_3)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_215]) ).
tcf(c_949,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,e_2)
| ~ product(e_2,X1,e_2)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_183]) ).
tcf(c_951,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,e_4)
| ~ product(e_2,X1,e_4)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_952,plain,
! [X0: $i,X1: $i] :
( product(e_3,X0,X1)
| ~ product(e_2,e_3,X0)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_238]) ).
tcf(c_959,plain,
( product(e_3,e_1,e_1)
| ~ product(e_2,e_3,e_1)
| ~ product(e_1,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_952]) ).
tcf(c_960,plain,
( product(e_1,e_1,e_4)
| ~ product(e_2,e_1,e_4)
| ~ product(e_1,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_951]) ).
tcf(c_962,plain,
( product(e_1,e_1,e_2)
| ~ product(e_2,e_1,e_2)
| ~ product(e_1,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_949]) ).
tcf(c_967,plain,
( product(e_1,e_1,e_3)
| ~ product(e_2,e_1,e_3)
| ~ product(e_1,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_943]) ).
tcf(c_988,plain,
! [X0: $i,X1: $i] :
( product(X1,e_3,e_3)
| ~ product(e_3,X0,e_3)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_216]) ).
tcf(c_991,plain,
! [X0: $i,X1: $i] :
( product(e_2,X0,X1)
| ~ product(X1,e_2,e_3)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_199]) ).
tcf(c_992,plain,
! [X0: $i,X1: $i] :
( product(X1,e_3,e_3)
| ~ product(e_3,X0,X1)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_222]) ).
tcf(c_996,plain,
! [X0: $i,X1: $i] :
( product(X1,e_3,e_4)
| ~ product(e_3,X0,e_4)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_248]) ).
tcf(c_997,plain,
! [X0: $i,X1: $i] :
( product(e_3,X0,e_4)
| ~ product(X1,e_3,e_4)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_1007,plain,
( product(e_1,e_3,e_4)
| ~ product(e_3,e_1,e_4)
| ~ product(e_1,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_996]) ).
tcf(c_1009,plain,
( product(e_1,e_3,e_3)
| ~ product(e_3,e_1,e_1)
| ~ product(e_1,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_992]) ).
tcf(c_1010,plain,
( product(e_2,e_1,e_1)
| ~ product(e_1,e_2,e_3)
| ~ product(e_1,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_991]) ).
tcf(c_1013,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X0,X1)
| ~ product(X1,X2,e_3)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_1014,plain,
( product(e_1,e_1,e_1)
| ~ product(e_1,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_1013]) ).
tcf(c_1041,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_155]) ).
tcf(c_1042,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_1041]) ).
tcf(c_1044,plain,
! [X0: $i] :
( equalish(e_3,e_4)
| ~ product(e_4,e_2,X0)
| ~ product(e_3,e_2,X0) ),
inference(instantiation,[status(thm)],[c_155]) ).
tcf(c_1045,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_2,e_1)
| ~ product(e_3,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_1044]) ).
tcf(c_1096,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_2,e_3)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_1115,plain,
! [X0: $i] :
( product(e_4,X0,e_3)
| ~ product(e_2,e_4,X0)
| ~ product(X0,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_216]) ).
tcf(c_1116,plain,
! [X0: $i] :
( product(X0,e_2,e_3)
| ~ product(e_4,X0,e_3)
| ~ product(e_2,e_4,X0) ),
inference(instantiation,[status(thm)],[c_215]) ).
tcf(c_1132,plain,
( product(e_4,e_1,e_3)
| ~ product(e_2,e_4,e_1)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_1115]) ).
tcf(c_1144,plain,
( product(e_2,e_4,e_4)
| product(e_2,e_3,e_4)
| product(e_2,e_2,e_4)
| product(e_2,e_1,e_4)
| ~ group_element(e_4)
| ~ group_element(e_2) ),
inference(instantiation,[status(thm)],[c_197]) ).
tcf(c_1155,plain,
! [X0: $i] :
( equalish(e_4,e_2)
| ~ product(e_4,e_4,X0)
| ~ product(e_2,e_4,X0) ),
inference(instantiation,[status(thm)],[c_167]) ).
tcf(c_1157,plain,
! [X0: $i] :
( equalish(e_3,e_2)
| ~ product(e_3,e_4,X0)
| ~ product(e_2,e_4,X0) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_1160,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_1157]) ).
tcf(c_1162,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_4,e_1)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_1155]) ).
tcf(c_1165,plain,
! [X0: $i,X1: $i] :
( product(X1,e_2,X0)
| ~ product(e_4,X1,e_2)
| ~ product(e_2,e_4,X0) ),
inference(instantiation,[status(thm)],[c_194]) ).
tcf(c_1198,plain,
( 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_204]) ).
tcf(c_1247,plain,
( equalish(e_1,e_4)
| ~ product(e_1,e_4,e_3)
| ~ product(e_1,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_1250,plain,
( product(e_4,e_3,e_3)
| product(e_3,e_3,e_3)
| product(e_2,e_3,e_3)
| product(e_1,e_3,e_3)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_208]) ).
tcf(c_1323,plain,
! [X0: $i] :
( product(e_3,e_3,e_2)
| ~ product(e_3,e_2,X0)
| ~ product(e_2,e_3,X0) ),
inference(instantiation,[status(thm)],[c_220]) ).
tcf(c_1324,plain,
! [X0: $i] :
( product(e_3,X0,e_2)
| ~ product(e_2,e_3,X0)
| ~ product(X0,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_184]) ).
tcf(c_1333,plain,
( product(e_3,e_1,e_2)
| ~ product(e_2,e_3,e_1)
| ~ product(e_1,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_1324]) ).
tcf(c_1334,plain,
( product(e_3,e_3,e_2)
| ~ product(e_3,e_2,e_1)
| ~ product(e_2,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_1323]) ).
tcf(c_1348,plain,
( equalish(e_4,e_1)
| ~ product(e_2,e_3,e_4)
| ~ product(e_2,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_157]) ).
tcf(c_1351,plain,
( product(e_4,e_3,e_4)
| product(e_3,e_3,e_4)
| product(e_2,e_3,e_4)
| product(e_1,e_3,e_4)
| ~ group_element(e_4)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_218]) ).
tcf(c_1354,plain,
! [X0: $i] :
( product(e_3,e_4,X0)
| ~ product(e_2,e_3,e_4)
| ~ product(e_4,e_2,X0) ),
inference(instantiation,[status(thm)],[c_324]) ).
tcf(c_1357,plain,
( product(e_3,e_4,e_1)
| ~ product(e_4,e_2,e_1)
| ~ product(e_2,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_1354]) ).
tcf(c_1369,plain,
! [X0: $i] :
( equalish(e_3,e_2)
| ~ product(e_3,e_3,X0)
| ~ product(e_2,e_3,X0) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_1372,plain,
( equalish(e_3,e_2)
| ~ product(e_3,e_3,e_1)
| ~ product(e_2,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_1369]) ).
tcf(c_1375,plain,
! [X0: $i,X1: $i] :
( product(X1,e_2,X0)
| ~ product(e_3,X1,e_2)
| ~ product(e_2,e_3,X0) ),
inference(instantiation,[status(thm)],[c_194]) ).
tcf(c_1376,plain,
( product(e_1,e_2,e_1)
| ~ product(e_3,e_1,e_2)
| ~ product(e_2,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_1375]) ).
tcf(c_1378,plain,
! [X0: $i,X1: $i] :
( product(e_3,X0,X1)
| ~ product(e_2,e_3,X1)
| ~ product(X0,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_233]) ).
tcf(c_1379,plain,
( product(e_3,e_1,e_1)
| ~ product(e_2,e_3,e_1)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_1378]) ).
tcf(c_1425,plain,
( equalish(e_1,e_3)
| ~ product(e_1,e_3,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_217]) ).
tcf(c_1426,plain,
( 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_224]) ).
tcf(c_1462,plain,
( product(e_3,e_4,e_4)
| product(e_3,e_3,e_4)
| product(e_3,e_2,e_4)
| product(e_3,e_1,e_4)
| ~ group_element(e_4)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_229]) ).
tcf(c_1465,plain,
! [X0: $i] :
( product(e_2,e_4,X0)
| ~ product(e_3,e_2,e_4)
| ~ product(e_4,e_3,X0) ),
inference(instantiation,[status(thm)],[c_324]) ).
tcf(c_1468,plain,
( product(e_2,e_4,e_1)
| ~ product(e_4,e_3,e_1)
| ~ product(e_3,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_1465]) ).
tcf(c_1517,plain,
! [X0: $i] :
( product(e_2,e_2,e_4)
| ~ product(e_2,X0,e_4)
| ~ product(X0,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_206]) ).
tcf(c_1519,plain,
! [X0: $i] :
( product(X0,e_3,e_4)
| ~ product(e_3,e_2,X0)
| ~ product(e_2,X0,e_4) ),
inference(instantiation,[status(thm)],[c_222]) ).
tcf(c_1532,plain,
( product(e_1,e_3,e_4)
| ~ product(e_3,e_2,e_1)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_1519]) ).
tcf(c_1534,plain,
( product(e_2,e_2,e_4)
| ~ product(e_2,e_1,e_4)
| ~ product(e_1,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_1517]) ).
tcf(c_1540,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ product(e_2,X0,e_4)
| ~ product(e_2,X0,e_3) ),
inference(instantiation,[status(thm)],[c_169]) ).
tcf(c_1542,plain,
! [X0: $i,X1: $i] :
( product(X0,e_4,X1)
| ~ product(e_4,e_2,X1)
| ~ product(e_2,X0,e_4) ),
inference(instantiation,[status(thm)],[c_324]) ).
tcf(c_1547,plain,
( product(e_1,e_4,e_1)
| ~ product(e_4,e_2,e_1)
| ~ product(e_2,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_1542]) ).
tcf(c_1549,plain,
( equalish(e_4,e_3)
| ~ product(e_2,e_1,e_4)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_1540]) ).
tcf(c_1568,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,e_2)
| ~ product(e_2,X1,e_4)
| ~ product(X0,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_181]) ).
tcf(c_1569,plain,
( product(e_1,e_1,e_2)
| ~ product(e_2,e_1,e_4)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_1568]) ).
tcf(c_1576,plain,
( product(e_4,e_4,e_4)
| product(e_3,e_4,e_4)
| product(e_2,e_4,e_4)
| product(e_1,e_4,e_4)
| ~ group_element(e_4) ),
inference(instantiation,[status(thm)],[c_240]) ).
tcf(c_1622,plain,
( product(e_4,e_4,e_4)
| product(e_4,e_3,e_4)
| product(e_4,e_2,e_4)
| product(e_4,e_1,e_4)
| ~ group_element(e_4) ),
inference(instantiation,[status(thm)],[c_243]) ).
tcf(c_1626,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_2,e_4)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_356]) ).
tcf(c_1627,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_2,e_4)
| ~ product(e_2,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_355]) ).
tcf(c_1628,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_2,e_4)
| ~ product(e_3,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_354]) ).
tcf(c_1686,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X1,e_4,X2)
| ~ product(e_4,X0,X1)
| ~ product(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_2056,plain,
! [X0: $i] :
( equalish(e_4,e_1)
| ~ product(X0,e_2,e_4)
| ~ product(X0,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_157]) ).
tcf(c_2057,plain,
( equalish(e_4,e_1)
| ~ product(e_1,e_2,e_4)
| ~ product(e_1,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_2056]) ).
tcf(c_2077,plain,
! [X0: $i,X1: $i] :
( product(e_2,e_4,X1)
| ~ product(e_4,X0,e_2)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_201]) ).
tcf(c_2086,plain,
! [X0: $i] :
( equalish(e_4,e_1)
| ~ product(e_4,X0,e_2)
| ~ product(e_1,X0,e_2) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_2089,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_1,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_2086]) ).
tcf(c_2091,plain,
! [X0: $i,X1: $i] :
( product(X1,e_4,e_2)
| ~ product(e_4,X0,e_2)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_184]) ).
tcf(c_2092,plain,
( product(e_1,e_4,e_2)
| ~ product(e_4,e_1,e_2)
| ~ product(e_1,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_2091]) ).
tcf(c_2103,plain,
! [X0: $i,X1: $i] :
( product(e_2,X0,X1)
| ~ product(e_4,e_2,X1)
| ~ product(X0,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_201]) ).
tcf(c_2104,plain,
( product(e_2,e_1,e_1)
| ~ product(e_4,e_2,e_1)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_2103]) ).
tcf(c_2121,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_143]) ).
tcf(c_2317,plain,
( product(e_3,e_4,e_3)
| product(e_3,e_3,e_3)
| product(e_3,e_2,e_3)
| product(e_3,e_1,e_3)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_211]) ).
tcf(c_2321,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_173]) ).
tcf(c_2334,plain,
( product(e_4,e_4,e_3)
| product(e_4,e_3,e_3)
| product(e_4,e_2,e_3)
| product(e_4,e_1,e_3)
| ~ group_element(e_4)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_211]) ).
tcf(c_2335,plain,
( equalish(e_1,e_4)
| ~ product(e_4,e_3,e_3)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_276]) ).
tcf(c_2346,plain,
! [X0: $i] :
( equalish(e_3,e_1)
| ~ product(e_3,e_3,X0)
| ~ product(e_3,e_1,X0) ),
inference(instantiation,[status(thm)],[c_141]) ).
tcf(c_2348,plain,
! [X0: $i] :
( equalish(e_3,e_2)
| ~ product(e_3,e_3,X0)
| ~ product(e_3,e_2,X0) ),
inference(instantiation,[status(thm)],[c_147]) ).
tcf(c_2350,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ product(e_3,e_4,X0)
| ~ product(e_3,e_3,X0) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_2351,plain,
! [X0: $i] :
( equalish(e_3,e_4)
| ~ product(e_3,e_4,X0)
| ~ product(e_3,e_3,X0) ),
inference(instantiation,[status(thm)],[c_153]) ).
tcf(c_2353,plain,
( equalish(e_3,e_4)
| ~ product(e_3,e_4,e_1)
| ~ product(e_3,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_2351]) ).
tcf(c_2354,plain,
( equalish(e_4,e_3)
| ~ product(e_3,e_4,e_1)
| ~ product(e_3,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_2350]) ).
tcf(c_2356,plain,
( equalish(e_3,e_2)
| ~ product(e_3,e_3,e_1)
| ~ product(e_3,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_2348]) ).
tcf(c_2358,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_3,e_1)
| ~ product(e_3,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_2346]) ).
tcf(c_2359,plain,
! [X0: $i] :
( equalish(e_3,e_1)
| ~ product(e_3,e_3,X0)
| ~ product(e_1,e_3,X0) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_2363,plain,
! [X0: $i] :
( equalish(e_3,e_4)
| ~ product(e_4,e_3,X0)
| ~ product(e_3,e_3,X0) ),
inference(instantiation,[status(thm)],[c_155]) ).
tcf(c_2364,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_3,e_1)
| ~ product(e_3,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_2363]) ).
tcf(c_2367,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_3,e_1)
| ~ product(e_1,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_2359]) ).
tcf(c_2373,plain,
! [X0: $i,X1: $i] :
( product(X0,e_3,X1)
| ~ product(e_3,e_3,X1)
| ~ product(e_3,X0,e_3) ),
inference(instantiation,[status(thm)],[c_226]) ).
tcf(c_2374,plain,
( product(e_1,e_3,e_1)
| ~ product(e_3,e_3,e_1)
| ~ product(e_3,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_2373]) ).
tcf(c_2377,plain,
! [X0: $i,X1: $i] :
( product(e_3,X0,X1)
| ~ product(e_3,e_3,X1)
| ~ product(X0,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_233]) ).
tcf(c_2378,plain,
( product(e_3,e_1,e_1)
| ~ product(e_3,e_3,e_1)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_2377]) ).
tcf(c_2427,plain,
! [X0: $i] :
( equalish(e_3,e_1)
| ~ product(e_3,e_4,X0)
| ~ product(e_1,e_4,X0) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_2430,plain,
! [X0: $i] :
( equalish(e_4,e_3)
| ~ product(e_4,e_4,X0)
| ~ product(e_3,e_4,X0) ),
inference(instantiation,[status(thm)],[c_173]) ).
tcf(c_2431,plain,
! [X0: $i] :
( equalish(e_3,e_4)
| ~ product(e_4,e_4,X0)
| ~ product(e_3,e_4,X0) ),
inference(instantiation,[status(thm)],[c_155]) ).
tcf(c_2432,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_4,e_1)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_2431]) ).
tcf(c_2433,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_4,e_1)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_2430]) ).
tcf(c_2435,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_4,e_1)
| ~ product(e_1,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_2427]) ).
tcf(c_2441,plain,
! [X0: $i,X1: $i] :
( product(X1,e_3,X0)
| ~ product(e_4,X1,e_3)
| ~ product(e_3,e_4,X0) ),
inference(instantiation,[status(thm)],[c_226]) ).
tcf(c_2442,plain,
( product(e_1,e_3,e_1)
| ~ product(e_4,e_1,e_3)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_2441]) ).
tcf(c_2451,plain,
! [X0: $i,X1: $i] :
( product(X0,e_4,X1)
| ~ product(e_4,e_3,X1)
| ~ product(e_3,X0,e_4) ),
inference(instantiation,[status(thm)],[c_324]) ).
tcf(c_2456,plain,
( product(e_1,e_4,e_1)
| ~ product(e_4,e_3,e_1)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_2451]) ).
tcf(c_2478,plain,
! [X0: $i] :
( equalish(e_3,e_1)
| ~ product(e_3,X0,e_4)
| ~ product(e_1,X0,e_4) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_2484,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_1,e_4)
| ~ product(e_1,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_2478]) ).
tcf(c_2500,plain,
( 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_236]) ).
tcf(c_2502,plain,
( equalish(e_4,e_3)
| ~ product(e_3,e_4,e_4)
| ~ product(e_3,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_334]) ).
tcf(c_2504,plain,
( equalish(e_4,e_2)
| ~ product(e_3,e_4,e_4)
| ~ product(e_3,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_335]) ).
tcf(c_2507,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,e_3)
| ~ product(e_3,X1,e_4)
| ~ product(X0,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_322]) ).
tcf(c_2508,plain,
( product(e_1,e_1,e_3)
| ~ product(e_3,e_1,e_4)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_2507]) ).
tcf(c_2672,plain,
( product(e_4,e_4,e_4)
| product(e_4,e_4,e_3)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_1)
| ~ group_element(e_4) ),
inference(instantiation,[status(thm)],[c_353]) ).
tcf(c_2673,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_4,e_3)
| ~ product(e_4,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_2675,plain,
( equalish(e_4,e_2)
| ~ product(e_4,e_4,e_3)
| ~ product(e_4,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_165]) ).
tcf(c_2709,plain,
! [X0: $i,X1: $i] :
( product(e_4,X0,X1)
| ~ product(e_3,e_4,X1)
| ~ product(X0,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_516]) ).
tcf(c_2710,plain,
( product(e_4,e_1,e_1)
| ~ product(e_3,e_4,e_1)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_2709]) ).
tcf(c_2793,plain,
! [X0: $i,X1: $i] :
( product(e_4,X0,X1)
| ~ product(e_3,e_4,X0)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_515]) ).
tcf(c_2794,plain,
( product(e_4,e_1,e_1)
| ~ product(e_3,e_4,e_1)
| ~ product(e_1,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_2793]) ).
tcf(c_2906,plain,
! [X0: $i,X1: $i] :
( product(X0,e_4,X1)
| ~ product(e_4,e_2,X0)
| ~ product(e_2,X0,X1) ),
inference(instantiation,[status(thm)],[c_1686]) ).
tcf(c_2907,plain,
( product(e_1,e_4,e_1)
| ~ product(e_4,e_2,e_1)
| ~ product(e_2,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_2906]) ).
tcf(c_2949,plain,
! [X0: $i] :
( product(e_2,e_4,X0)
| ~ product(e_4,e_3,e_2)
| ~ product(e_3,e_2,X0) ),
inference(instantiation,[status(thm)],[c_487]) ).
tcf(c_2950,plain,
! [X0: $i] :
( product(X0,e_4,e_2)
| ~ product(e_4,e_3,e_2)
| ~ product(e_3,X0,e_4) ),
inference(instantiation,[status(thm)],[c_485]) ).
tcf(c_2958,plain,
( product(e_1,e_4,e_2)
| ~ product(e_4,e_3,e_2)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_2950]) ).
tcf(c_2959,plain,
( product(e_2,e_4,e_1)
| ~ product(e_4,e_3,e_2)
| ~ product(e_3,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_2949]) ).
tcf(c_2998,plain,
! [X0: $i] :
( product(e_4,e_2,X0)
| ~ product(e_2,e_3,e_4)
| ~ product(e_3,e_4,X0) ),
inference(instantiation,[status(thm)],[c_487]) ).
tcf(c_3008,plain,
( product(e_4,e_2,e_1)
| ~ product(e_3,e_4,e_1)
| ~ product(e_2,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_2998]) ).
tcf(c_3114,plain,
( equalish(e_4,e_1)
| ~ product(e_1,e_3,e_4)
| ~ product(e_1,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_157]) ).
tcf(c_3116,plain,
( equalish(e_4,e_3)
| ~ product(e_1,e_3,e_4)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_169]) ).
tcf(c_3117,plain,
( equalish(e_3,e_4)
| ~ product(e_1,e_3,e_4)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_151]) ).
tcf(c_3125,plain,
( equalish(e_3,e_2)
| ~ product(e_1,e_3,e_4)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_147]) ).
tcf(c_3156,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_3,e_4)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_3157,plain,
( equalish(e_1,e_3)
| ~ product(e_3,e_3,e_4)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_328]) ).
tcf(c_3159,plain,
( equalish(e_4,e_1)
| ~ product(e_3,e_4,e_4)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_336]) ).
tcf(c_3247,plain,
( product(e_3,e_3,e_3)
| ~ product(e_3,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_3919,plain,
! [X0: $i] :
( product(e_3,e_2,X0)
| ~ product(e_2,e_3,e_3)
| ~ product(e_3,e_3,X0) ),
inference(instantiation,[status(thm)],[c_423]) ).
tcf(c_3920,plain,
( product(e_3,e_2,e_1)
| ~ product(e_3,e_3,e_1)
| ~ product(e_2,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_3919]) ).
tcf(c_3958,plain,
( product(e_3,e_4,e_4)
| ~ product(e_4,e_3,e_4)
| ~ product(e_3,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_470]) ).
tcf(c_3988,plain,
! [X0: $i] :
( product(e_3,X0,e_3)
| ~ product(e_3,e_3,e_4)
| ~ product(X0,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_452]) ).
tcf(c_3989,plain,
( product(e_3,e_1,e_3)
| ~ product(e_3,e_3,e_4)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_3988]) ).
tcf(c_4026,plain,
! [X0: $i] :
( product(e_3,e_2,e_4)
| ~ product(e_4,e_3,X0)
| ~ product(e_2,e_4,X0) ),
inference(instantiation,[status(thm)],[c_504]) ).
tcf(c_4027,plain,
( product(e_3,e_2,e_4)
| ~ product(e_4,e_3,e_1)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_4026]) ).
tcf(c_4033,plain,
( product(e_3,e_3,e_4)
| ~ product(e_4,e_3,e_3)
| ~ product(e_3,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_504]) ).
tcf(c_4146,plain,
( product(e_3,e_4,e_3)
| ~ product(e_4,e_2,e_3)
| ~ product(e_2,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_799]) ).
tcf(c_4147,plain,
( product(e_4,e_2,e_3)
| ~ product(e_4,e_4,e_3)
| ~ product(e_2,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_1116]) ).
tcf(c_4150,plain,
! [X0: $i] :
( product(e_3,e_4,e_3)
| ~ product(e_4,X0,e_3)
| ~ product(X0,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_799]) ).
tcf(c_4151,plain,
( product(e_3,e_4,e_3)
| ~ product(e_4,e_1,e_3)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_4150]) ).
tcf(c_4222,plain,
! [X0: $i] :
( product(e_2,e_4,X0)
| ~ product(e_2,e_2,e_4)
| ~ product(e_4,e_2,X0) ),
inference(instantiation,[status(thm)],[c_866]) ).
tcf(c_4223,plain,
( product(e_2,e_4,e_1)
| ~ product(e_4,e_2,e_1)
| ~ product(e_2,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_4222]) ).
tcf(c_4275,plain,
( product(e_1,e_3,e_3)
| ~ product(e_3,e_3,e_3)
| ~ product(e_3,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_988]) ).
tcf(c_4277,plain,
( product(e_4,e_3,e_3)
| ~ product(e_3,e_4,e_3)
| ~ product(e_3,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_988]) ).
tcf(c_4311,plain,
( product(e_3,e_3,e_4)
| ~ product(e_4,e_3,e_4)
| ~ product(e_3,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_997]) ).
tcf(c_4337,plain,
! [X0: $i] :
( product(e_4,e_2,X0)
| ~ product(e_4,e_4,e_2)
| ~ product(e_2,e_4,X0) ),
inference(instantiation,[status(thm)],[c_1165]) ).
tcf(c_4338,plain,
( product(e_4,e_2,e_1)
| ~ product(e_4,e_4,e_2)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_4337]) ).
tcf(c_4483,plain,
! [X0: $i] :
( product(e_2,e_4,X0)
| ~ product(e_4,e_4,e_2)
| ~ product(e_4,e_2,X0) ),
inference(instantiation,[status(thm)],[c_2077]) ).
tcf(c_4484,plain,
( product(e_2,e_4,e_1)
| ~ product(e_4,e_4,e_2)
| ~ product(e_4,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_4483]) ).
tcf(c_4616,plain,
! [X0: $i] :
( product(e_3,X0,e_4)
| ~ product(e_3,e_3,e_4)
| ~ product(X0,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_2377]) ).
tcf(c_4617,plain,
( product(e_3,e_1,e_4)
| ~ product(e_3,e_3,e_4)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_4616]) ).
tcf(c_4713,plain,
( product(e_3,e_3,e_3)
| ~ product(e_3,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_454]) ).
tcf(c_4728,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_141]) ).
tcf(c_4730,plain,
! [X0: $i] :
( equalish(e_3,e_2)
| ~ product(e_4,e_3,X0)
| ~ product(e_4,e_2,X0) ),
inference(instantiation,[status(thm)],[c_147]) ).
tcf(c_4733,plain,
! [X0: $i] :
( equalish(e_3,e_4)
| ~ product(e_4,e_4,X0)
| ~ product(e_4,e_3,X0) ),
inference(instantiation,[status(thm)],[c_153]) ).
tcf(c_4736,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_4,e_1)
| ~ product(e_4,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_4733]) ).
tcf(c_4739,plain,
( equalish(e_3,e_2)
| ~ product(e_4,e_3,e_1)
| ~ product(e_4,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_4730]) ).
tcf(c_4741,plain,
( equalish(e_3,e_1)
| ~ product(e_4,e_3,e_1)
| ~ product(e_4,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_4728]) ).
tcf(c_4746,plain,
! [X0: $i] :
( equalish(e_4,e_1)
| ~ product(e_4,e_3,X0)
| ~ product(e_1,e_3,X0) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_4748,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_3,e_1)
| ~ product(e_1,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_4746]) ).
tcf(c_4758,plain,
! [X0: $i,X1: $i] :
( product(e_3,X0,X1)
| ~ product(e_4,e_3,X1)
| ~ product(X0,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_233]) ).
tcf(c_4759,plain,
( product(e_3,e_1,e_1)
| ~ product(e_4,e_3,e_1)
| ~ product(e_1,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_4758]) ).
tcf(c_4789,plain,
( product(e_3,e_1,e_4)
| ~ product(e_3,e_3,e_1)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_4842,plain,
( product(e_4,e_3,e_4)
| ~ product(e_3,e_4,e_3)
| ~ product(e_3,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_472]) ).
tcf(c_5114,plain,
! [X0: $i] :
( product(X0,e_2,e_2)
| ~ product(e_2,e_2,X0)
| ~ product(e_2,X0,e_2) ),
inference(instantiation,[status(thm)],[c_588]) ).
tcf(c_5115,plain,
( product(e_1,e_2,e_2)
| ~ product(e_2,e_2,e_1)
| ~ product(e_2,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_5114]) ).
tcf(c_5158,plain,
! [X0: $i] :
( product(e_3,e_3,X0)
| ~ product(e_3,e_4,e_3)
| ~ product(e_4,e_3,X0) ),
inference(instantiation,[status(thm)],[c_793]) ).
tcf(c_5159,plain,
( product(e_3,e_3,e_1)
| ~ product(e_4,e_3,e_1)
| ~ product(e_3,e_4,e_3) ),
inference(instantiation,[status(thm)],[c_5158]) ).
tcf(c_5199,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_3,e_4)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_356]) ).
tcf(c_5247,plain,
( product(e_3,e_4,e_4)
| ~ product(e_4,e_3,e_3)
| ~ product(e_3,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_798]) ).
tcf(c_5271,plain,
( product(e_3,e_4,e_4)
| ~ product(e_4,e_4,e_2)
| ~ product(e_4,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_800]) ).
tcf(c_5330,plain,
! [X0: $i] :
( product(e_3,e_4,e_3)
| ~ product(e_4,X0,e_3)
| ~ product(X0,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_874]) ).
tcf(c_5331,plain,
( product(e_3,e_4,e_3)
| ~ product(e_4,e_1,e_3)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_5330]) ).
tcf(c_6366,plain,
( product(e_3,e_3,e_4)
| product(e_3,e_3,e_3)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_1)
| ~ group_element(e_3) ),
inference(instantiation,[status(thm)],[c_236]) ).
tcf(c_6574,plain,
! [X0: $i] :
( product(X0,e_4,e_4)
| ~ product(e_4,e_4,X0)
| ~ product(e_4,X0,e_4) ),
inference(instantiation,[status(thm)],[c_798]) ).
tcf(c_6575,plain,
! [X0: $i] :
( product(X0,e_3,e_4)
| ~ product(e_4,X0,e_4)
| ~ product(e_3,e_4,X0) ),
inference(instantiation,[status(thm)],[c_473]) ).
tcf(c_6582,plain,
! [X0: $i] :
( equalish(e_4,e_1)
| ~ product(e_4,X0,e_4)
| ~ product(e_4,X0,e_1) ),
inference(instantiation,[status(thm)],[c_157]) ).
tcf(c_6595,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_1,e_4)
| ~ product(e_4,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_6582]) ).
tcf(c_6599,plain,
( product(e_1,e_3,e_4)
| ~ product(e_4,e_1,e_4)
| ~ product(e_3,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_6575]) ).
tcf(c_6600,plain,
( product(e_1,e_4,e_4)
| ~ product(e_4,e_4,e_1)
| ~ product(e_4,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_6574]) ).
tcf(c_6629,plain,
! [X0: $i,X1: $i] :
( product(X1,X0,e_4)
| ~ product(e_4,X1,e_4)
| ~ product(X0,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_322]) ).
tcf(c_6630,plain,
( product(e_1,e_1,e_4)
| ~ product(e_4,e_1,e_4)
| ~ product(e_1,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_6629]) ).
tcf(c_6636,plain,
! [X0: $i] :
( product(e_4,e_4,e_4)
| ~ product(e_4,X0,e_4)
| ~ product(X0,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_501]) ).
tcf(c_6638,plain,
( product(e_4,e_4,e_4)
| ~ product(e_4,e_1,e_4)
| ~ product(e_1,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_6636]) ).
tcf(c_6812,plain,
( equalish(e_1,e_4)
| ~ product(e_4,e_3,e_4)
| ~ product(e_4,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_287]) ).
tcf(c_7125,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_4,e_4)
| ~ product(e_4,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_336]) ).
tcf(c_7183,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_4,e_4)
| ~ product(e_4,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_334]) ).
tcf(c_7191,plain,
! [X0: $i] :
( product(e_4,X0,e_4)
| ~ product(e_4,e_4,e_4)
| ~ product(X0,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_516]) ).
tcf(c_7192,plain,
( product(e_4,e_1,e_4)
| ~ product(e_4,e_4,e_4)
| ~ product(e_1,e_4,e_4) ),
inference(instantiation,[status(thm)],[c_7191]) ).
tcf(c_7790,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_7192,c_7183,c_7125,c_6812,c_6638,c_6630,c_6600,c_6599,c_6595,c_6366,c_5331,c_5271,c_5247,c_5199,c_5159,c_5115,c_4842,c_4789,c_4759,c_4748,c_4741,c_4739,c_4736,c_4713,c_4617,c_4484,c_4338,c_4311,c_4277,c_4275,c_4223,c_4151,c_4147,c_4146,c_4033,c_4027,c_3989,c_3958,c_3920,c_3247,c_3156,c_3157,c_3159,c_3125,c_3114,c_3116,c_3117,c_3008,c_2959,c_2958,c_2907,c_2794,c_2710,c_2673,c_2675,c_2672,c_2508,c_2502,c_2504,c_2500,c_2484,c_2456,c_2442,c_2435,c_2433,c_2432,c_2378,c_2374,c_2367,c_2364,c_2358,c_2356,c_2354,c_2353,c_2335,c_2334,c_2321,c_2317,c_2121,c_2104,c_2092,c_2089,c_2057,c_1626,c_1627,c_1628,c_1622,c_1576,c_1569,c_1549,c_1547,c_1534,c_1532,c_1468,c_1462,c_1426,c_1425,c_1379,c_1376,c_1372,c_1357,c_1351,c_1348,c_1334,c_1333,c_1250,c_1247,c_1198,c_1162,c_1160,c_1144,c_1132,c_1096,c_1045,c_1042,c_1014,c_1010,c_1009,c_1007,c_967,c_962,c_960,c_959,c_937,c_879,c_853,c_811,c_808,c_787,c_753,c_747,c_725,c_707,c_708,c_600,c_553,c_541,c_510,c_483,c_482,c_481,c_464,c_363,c_360,c_346,c_345,c_344,c_343,c_340,c_323,c_286,c_277,c_262,c_244,c_241,c_237,c_230,c_225,c_219,c_212,c_209,c_193,c_187,c_177,c_158,c_144,c_140,c_104,c_101,c_100,c_82,c_83,c_84,c_88,c_89,c_90,c_91,c_92,c_93,c_78,c_79,c_80,c_81]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP129-4.004 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/5.39 % Computer : n017.cluster.edu
% 0.10/5.39 % Model : x86_64 x86_64
% 0.10/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.39 % Memory : 8046.5625MB
% 0.10/5.39 % OS : Linux 6.8.0-71-generic
% 0.10/5.39 % CPULimit : 300
% 0.10/5.39 % WCLimit : 300
% 0.10/5.39 % DateTime : Wed Sep 23 13:41:26 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.10/5.39 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.15/5.43 Running EPR theorem proving
% 0.15/5.43 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.15/5.44
% 0.15/5.44 % ======== iProver multi-core TPTP/SMT =========
% 0.15/5.44
% 0.15/5.44 % Detected problem language: tptp
% 0.15/5.46 % Proving...
% 2.09/6.16 % SZS status Started for theBenchmark.p
% 2.09/6.16 % SZS status Unsatisfiable for theBenchmark.p
% 2.09/6.16
% 2.09/6.16 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.09/6.16
% 2.09/6.16 % ------ iProver source info
% 2.09/6.16
% 2.09/6.16 % git: date: 2026-07-19 20:42:38 +0200
% 2.09/6.16 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.09/6.16 % git: non_committed_changes: false
% 2.09/6.16
% 2.09/6.16 % ------ Parsing...% successful
% 2.09/6.16
% 2.09/6.16
% 2.09/6.16 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 2.09/6.16 % ------ Proving...
% 2.09/6.16 % ------ Problem Properties
% 2.09/6.16
% 2.09/6.16 %
% 2.09/6.16 % clauses 25
% 2.09/6.16 % conjectures 3
% 2.09/6.16 % EPR 25
% 2.09/6.16 % Horn 22
% 2.09/6.16 % unary 16
% 2.09/6.16 % binary 0
% 2.09/6.16 % lits 52
% 2.09/6.16 % lits eq 0
% 2.09/6.16 % fd_pure 0
% 2.09/6.16 % fd_pseudo 0
% 2.09/6.16 % fd_cond 0
% 2.09/6.16 % fd_pseudo_cond 0
% 2.09/6.16 % AC symbols 0
% 2.09/6.16
% 2.09/6.16 % ------ Input Options Time Limit: Unbounded
% 2.09/6.16
% 2.09/6.16
% 2.09/6.16 % ------
% 2.09/6.16 % Current options:
% 2.09/6.16 % ------
% 2.09/6.16
% 2.09/6.16
% 2.09/6.16 %
% 2.09/6.16
% 2.09/6.16 % ------ Proving...
% 2.09/6.16 %
% 2.09/6.16
% 2.09/6.16 % SZS status Unsatisfiable for theBenchmark.p
% 2.09/6.16
% 2.09/6.16 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.09/6.17
% 2.09/6.17
%------------------------------------------------------------------------------