%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP129-2.004 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n012.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:26 PM UTC 2026
% Result : Unsatisfiable 0.79s 1.02s
% Output : CNFRefutation 0.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 68
% Number of leaves : 27
% Syntax : Number of formulae : 318 ( 52 unt; 0 def)
% Number of atoms : 1025 ( 0 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 1087 ( 380 ~; 707 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 193 ( 0 sgn 193 !; 0 ?; 172 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
next(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_then_e_2) ).
fof(f2,axiom,
next(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_then_e_3) ).
fof(f7,axiom,
greater(e_3,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_greater_e_2) ).
fof(f8,axiom,
greater(e_4,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_greater_e_2) ).
fof(f9,axiom,
greater(e_4,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_greater_e_3) ).
fof(f10,axiom,
! [X2,X0,X1] :
( ~ greater(X1,X2)
| ~ next(X0,X2)
| ~ product(X0,e_1,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',no_redundancy) ).
fof(f11,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
fof(f12,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
fof(f13,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
fof(f14,axiom,
group_element(e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_4) ).
fof(f15,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f16,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f17,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
fof(f18,axiom,
~ equalish(e_2,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_1) ).
fof(f19,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f20,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
fof(f21,axiom,
~ equalish(e_3,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_1) ).
fof(f22,axiom,
~ equalish(e_3,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_2) ).
fof(f23,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
fof(f24,axiom,
~ equalish(e_4,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_1) ).
fof(f25,axiom,
~ equalish(e_4,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_2) ).
fof(f26,axiom,
~ equalish(e_4,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_3) ).
fof(f27,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(f28,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(f29,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(f30,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(f31,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_80,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( product(X1,X3,X2)
| ~ product(X3,X0,X1)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equalish(X0,X3)
| ~ product(X3,X1,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equalish(X1,X3)
| ~ product(X0,X3,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( equalish(X2,X3)
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_84,plain,
! [X0: $i,X1: $i] :
( 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,[],[f27]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ greater(X1,X2)
| ~ next(X0,X2)
| ~ product(X0,e_1,X1) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_86,plain,
~ equalish(e_4,e_3),
inference(cnf_transformation,[],[f26]) ).
tcf(c_87,plain,
~ equalish(e_4,e_2),
inference(cnf_transformation,[],[f25]) ).
tcf(c_88,plain,
~ equalish(e_4,e_1),
inference(cnf_transformation,[],[f24]) ).
tcf(c_89,plain,
~ equalish(e_3,e_4),
inference(cnf_transformation,[],[f23]) ).
tcf(c_90,plain,
~ equalish(e_3,e_2),
inference(cnf_transformation,[],[f22]) ).
tcf(c_91,plain,
~ equalish(e_3,e_1),
inference(cnf_transformation,[],[f21]) ).
tcf(c_92,plain,
~ equalish(e_2,e_4),
inference(cnf_transformation,[],[f20]) ).
tcf(c_93,plain,
~ equalish(e_2,e_3),
inference(cnf_transformation,[],[f19]) ).
tcf(c_94,plain,
~ equalish(e_2,e_1),
inference(cnf_transformation,[],[f18]) ).
tcf(c_95,plain,
~ equalish(e_1,e_4),
inference(cnf_transformation,[],[f17]) ).
tcf(c_96,plain,
~ equalish(e_1,e_3),
inference(cnf_transformation,[],[f16]) ).
tcf(c_97,plain,
~ equalish(e_1,e_2),
inference(cnf_transformation,[],[f15]) ).
tcf(c_98,plain,
group_element(e_4),
inference(cnf_transformation,[],[f14]) ).
tcf(c_99,plain,
group_element(e_3),
inference(cnf_transformation,[],[f13]) ).
tcf(c_100,plain,
group_element(e_2),
inference(cnf_transformation,[],[f12]) ).
tcf(c_101,plain,
group_element(e_1),
inference(cnf_transformation,[],[f11]) ).
tcf(c_103,plain,
next(e_2,e_3),
inference(cnf_transformation,[],[f2]) ).
tcf(c_104,plain,
next(e_1,e_2),
inference(cnf_transformation,[],[f1]) ).
tcf(c_105,plain,
greater(e_4,e_3),
inference(cnf_transformation,[],[f9]) ).
tcf(c_106,plain,
greater(e_4,e_2),
inference(cnf_transformation,[],[f8]) ).
tcf(c_107,plain,
greater(e_3,e_2),
inference(cnf_transformation,[],[f7]) ).
tcf(c_113,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_84]) ).
tcf(c_206,plain,
! [X0: $i] :
( ~ greater(X0,e_2)
| ~ product(e_1,e_1,X0) ),
inference(resolution,[status(thm)],[c_104,c_85]) ).
tcf(c_214,plain,
! [X0: $i] :
( ~ greater(X0,e_3)
| ~ product(e_2,e_1,X0) ),
inference(resolution,[status(thm)],[c_103,c_85]) ).
tcf(c_236,plain,
~ product(e_1,e_1,e_3),
inference(resolution,[status(thm)],[c_107,c_206]) ).
tcf(c_240,plain,
~ product(e_1,e_1,e_4),
inference(resolution,[status(thm)],[c_106,c_206]) ).
tcf(c_244,plain,
~ product(e_2,e_1,e_4),
inference(resolution,[status(thm)],[c_105,c_214]) ).
tcf(c_259,plain,
! [X0: $i,X1: $i] :
( ~ product(X0,e_2,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[status(thm)],[c_97,c_82]) ).
tcf(c_260,plain,
( ~ product(e_1,e_2,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_259]) ).
tcf(c_267,plain,
! [X0: $i,X1: $i] :
( ~ product(e_2,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[status(thm)],[c_97,c_81]) ).
tcf(c_268,plain,
( ~ product(e_2,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_267]) ).
tcf(c_282,plain,
! [X0: $i,X1: $i] :
( ~ product(X0,e_3,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[status(thm)],[c_96,c_82]) ).
tcf(c_283,plain,
( ~ product(e_1,e_3,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_282]) ).
tcf(c_290,plain,
! [X0: $i,X1: $i] :
( ~ product(e_3,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[status(thm)],[c_96,c_81]) ).
tcf(c_291,plain,
( ~ product(e_3,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_290]) ).
tcf(c_305,plain,
! [X0: $i,X1: $i] :
( ~ product(X0,e_4,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[status(thm)],[c_95,c_82]) ).
tcf(c_306,plain,
( ~ product(e_1,e_4,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_313,plain,
! [X0: $i,X1: $i] :
( ~ product(e_4,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[status(thm)],[c_95,c_81]) ).
tcf(c_314,plain,
( ~ product(e_4,e_1,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_313]) ).
tcf(c_700,plain,
! [X0: $i] :
( product(e_2,e_1,e_4)
| ~ product(e_1,X0,e_2)
| ~ product(X0,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_704,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_81]) ).
tcf(c_706,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_82]) ).
tcf(c_707,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_81]) ).
tcf(c_710,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_81]) ).
tcf(c_712,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_82]) ).
tcf(c_713,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_81]) ).
tcf(c_714,plain,
! [X0: $i,X1: $i] :
( equalish(e_3,e_2)
| ~ product(X0,X1,e_3)
| ~ product(X0,X1,e_2) ),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_715,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_82]) ).
tcf(c_716,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_81]) ).
tcf(c_718,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_82]) ).
tcf(c_719,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_81]) ).
tcf(c_720,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_83]) ).
tcf(c_721,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_82]) ).
tcf(c_722,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_81]) ).
tcf(c_723,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_83]) ).
tcf(c_724,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_82]) ).
tcf(c_725,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_81]) ).
tcf(c_727,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_82]) ).
tcf(c_728,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_81]) ).
tcf(c_730,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_82]) ).
tcf(c_736,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_82]) ).
tcf(c_738,plain,
! [X0: $i,X1: $i] :
( product(X1,e_1,e_3)
| ~ product(e_1,X0,X1)
| ~ product(X0,X1,e_3) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_743,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_84]) ).
tcf(c_744,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_743]) ).
tcf(c_746,plain,
! [X0: $i,X1: $i] :
( product(e_1,X0,e_2)
| ~ product(X1,e_1,e_2)
| ~ product(X0,X1,e_1) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_749,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_84]) ).
tcf(c_750,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_749]) ).
tcf(c_769,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_80]) ).
tcf(c_771,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_84]) ).
tcf(c_772,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_771]) ).
tcf(c_773,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_3,X2,X1)
| ~ product(X2,X0,e_3)
| ~ product(X0,e_3,X1) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_775,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_84]) ).
tcf(c_776,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_775]) ).
tcf(c_795,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_80]) ).
tcf(c_797,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_84]) ).
tcf(c_798,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_797]) ).
tcf(c_799,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(e_2,X2,X1)
| ~ product(X2,X0,e_2)
| ~ product(X0,e_2,X1) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_829,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_80]) ).
tcf(c_895,plain,
( equalish(e_4,e_1)
| ~ product(e_4,e_4,e_2)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_710]) ).
tcf(c_900,plain,
( product(e_2,e_1,e_4)
| ~ product(e_4,e_2,e_4)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_700]) ).
tcf(c_901,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_799]) ).
tcf(c_902,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_901]) ).
tcf(c_903,plain,
! [X0: $i,X1: $i] :
( product(e_4,X0,e_2)
| ~ product(X1,e_4,e_2)
| ~ product(X0,X1,e_4) ),
inference(instantiation,[status(thm)],[c_829]) ).
tcf(c_906,plain,
( equalish(e_2,e_3)
| ~ product(e_4,e_3,e_2)
| ~ product(e_4,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_724]) ).
tcf(c_912,plain,
! [X0: $i] :
( equalish(e_2,e_4)
| ~ product(e_4,X0,e_2)
| ~ product(e_2,X0,e_2) ),
inference(instantiation,[status(thm)],[c_722]) ).
tcf(c_913,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_713]) ).
tcf(c_920,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_913]) ).
tcf(c_921,plain,
( equalish(e_2,e_4)
| ~ product(e_4,e_1,e_2)
| ~ product(e_2,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_912]) ).
tcf(c_981,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X0,e_4)
| product(X1,X2,e_3)
| product(X1,X2,e_2)
| product(X1,X2,e_1)
| ~ group_element(X2)
| ~ group_element(X1)
| ~ product(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_84,c_80]) ).
tcf(c_982,plain,
( 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(superposition,[status(thm)],[c_84,c_240]) ).
tcf(c_983,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| ~ group_element(e_2)
| ~ group_element(e_1) ),
inference(superposition,[status(thm)],[c_84,c_244]) ).
tcf(c_984,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_1,e_1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_982,c_236,c_101]) ).
tcf(c_987,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_983,c_100,c_101]) ).
tcf(c_1034,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X2,X0,e_4)
| product(X1,X2,e_3)
| product(X1,X2,e_2)
| product(X1,X2,e_1)
| ~ group_element(X2)
| ~ group_element(X1)
| ~ product(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_84,c_80]) ).
tcf(c_1035,plain,
( 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(superposition,[status(thm)],[c_84,c_240]) ).
tcf(c_1036,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| ~ group_element(e_2)
| ~ group_element(e_1) ),
inference(superposition,[status(thm)],[c_84,c_244]) ).
tcf(c_1037,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_1,e_1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1035,c_236,c_101]) ).
tcf(c_1040,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1036,c_100,c_101]) ).
tcf(c_1076,plain,
! [X0: $i] :
( product(e_1,e_2,e_2)
| ~ product(e_2,X0,e_1)
| ~ product(X0,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_746]) ).
tcf(c_1077,plain,
( product(e_1,e_2,e_2)
| ~ product(e_2,e_1,e_1)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1076]) ).
tcf(c_1081,plain,
! [X0: $i] :
( equalish(e_2,e_3)
| ~ product(e_2,X0,e_3)
| ~ product(e_2,X0,e_2) ),
inference(instantiation,[status(thm)],[c_723]) ).
tcf(c_1083,plain,
! [X0: $i] :
( equalish(e_3,e_2)
| ~ product(e_2,X0,e_3)
| ~ product(e_2,X0,e_2) ),
inference(instantiation,[status(thm)],[c_714]) ).
tcf(c_1085,plain,
( equalish(e_3,e_2)
| ~ product(e_2,e_1,e_3)
| ~ product(e_2,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1083]) ).
tcf(c_1102,plain,
! [X0: $i] :
( equalish(e_2,e_4)
| ~ product(e_2,X0,e_4)
| ~ product(e_2,X0,e_2) ),
inference(instantiation,[status(thm)],[c_720]) ).
tcf(c_1172,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_829]) ).
tcf(c_1185,plain,
( product(e_2,e_1,e_4)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_1)
| product(e_1,e_1,e_1)
| ~ group_element(e_2)
| ~ group_element(e_1) ),
inference(superposition,[status(thm)],[c_984,c_981]) ).
tcf(c_1201,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_1)
| product(e_1,e_1,e_1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1185,c_244,c_100,c_101]) ).
tcf(c_1212,plain,
( product(e_2,e_1,e_4)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_1)
| product(e_1,e_1,e_1)
| ~ group_element(e_2)
| ~ group_element(e_1) ),
inference(superposition,[status(thm)],[c_1037,c_1034]) ).
tcf(c_1228,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_1)
| product(e_1,e_1,e_1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1212,c_244,c_100,c_101]) ).
tcf(c_1252,plain,
! [X0: $i] :
( equalish(e_1,e_4)
| ~ product(X0,e_4,e_3)
| ~ product(X0,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_730]) ).
tcf(c_1253,plain,
! [X0: $i] :
( equalish(e_2,e_4)
| ~ product(X0,e_4,e_3)
| ~ product(X0,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_721]) ).
tcf(c_1254,plain,
! [X0: $i] :
( equalish(e_3,e_4)
| ~ product(X0,e_4,e_3)
| ~ product(X0,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_712]) ).
tcf(c_1260,plain,
( equalish(e_3,e_4)
| ~ product(e_1,e_4,e_3)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_1254]) ).
tcf(c_1261,plain,
( equalish(e_2,e_4)
| ~ product(e_1,e_4,e_3)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_1253]) ).
tcf(c_1263,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_773]) ).
tcf(c_1264,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_1263]) ).
tcf(c_1266,plain,
! [X0: $i] :
( product(e_2,X0,e_2)
| ~ product(e_3,e_2,e_2)
| ~ product(X0,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_829]) ).
tcf(c_1267,plain,
! [X0: $i] :
( product(e_3,e_2,e_2)
| ~ product(e_2,X0,e_3)
| ~ product(X0,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_795]) ).
tcf(c_1268,plain,
( product(e_3,e_2,e_2)
| ~ product(e_2,e_1,e_3)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_1267]) ).
tcf(c_1269,plain,
( product(e_2,e_1,e_2)
| ~ product(e_3,e_2,e_2)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_1266]) ).
tcf(c_1276,plain,
! [X0: $i] :
( equalish(e_3,e_1)
| ~ product(X0,e_3,e_2)
| ~ product(X0,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_718]) ).
tcf(c_1279,plain,
( equalish(e_3,e_1)
| ~ product(e_1,e_3,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1276]) ).
tcf(c_1282,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_771]) ).
tcf(c_1297,plain,
( product(e_3,e_2,e_4)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| 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(superposition,[status(thm)],[c_987,c_981]) ).
tcf(c_1300,plain,
! [X0: $i] :
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_1,X0,e_3)
| ~ product(X0,e_2,e_1) ),
inference(superposition,[status(thm)],[c_987,c_80]) ).
tcf(c_1317,plain,
( product(e_3,e_2,e_4)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1297,c_99,c_101]) ).
tcf(c_1333,plain,
( product(e_3,e_2,e_4)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| 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(superposition,[status(thm)],[c_1040,c_1034]) ).
tcf(c_1353,plain,
( product(e_3,e_2,e_4)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1333,c_99,c_101]) ).
tcf(c_1373,plain,
! [X0: $i] :
( equalish(e_2,e_3)
| ~ product(e_3,X0,e_2)
| ~ product(e_2,X0,e_2) ),
inference(instantiation,[status(thm)],[c_725]) ).
tcf(c_1374,plain,
! [X0: $i] :
( equalish(e_3,e_1)
| ~ product(e_3,X0,e_2)
| ~ product(e_1,X0,e_2) ),
inference(instantiation,[status(thm)],[c_719]) ).
tcf(c_1377,plain,
( equalish(e_3,e_1)
| ~ product(e_3,e_1,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1374]) ).
tcf(c_1378,plain,
( equalish(e_2,e_3)
| ~ product(e_3,e_1,e_2)
| ~ product(e_2,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1373]) ).
tcf(c_1398,plain,
( 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_797]) ).
tcf(c_1526,plain,
! [X0: $i] :
( equalish(e_1,e_2)
| ~ product(X0,e_2,e_2)
| ~ product(X0,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_736]) ).
tcf(c_1527,plain,
! [X0: $i] :
( equalish(e_2,e_1)
| ~ product(X0,e_2,e_2)
| ~ product(X0,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1528,plain,
( equalish(e_2,e_1)
| ~ product(e_1,e_2,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1527]) ).
tcf(c_1536,plain,
! [X0: $i] :
( equalish(e_2,e_1)
| ~ product(e_2,X0,e_2)
| ~ product(e_1,X0,e_2) ),
inference(instantiation,[status(thm)],[c_728]) ).
tcf(c_1537,plain,
( equalish(e_2,e_1)
| ~ product(e_2,e_1,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1536]) ).
tcf(c_1679,plain,
! [X0: $i] :
( product(e_2,e_1,e_2)
| ~ product(X0,e_2,e_1)
| product(e_1,X0,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_1300,c_101,c_94,c_113,c_236,c_240,c_268,c_1077,c_1300,c_1528]) ).
tcf(c_1680,plain,
! [X0: $i] :
( product(e_2,e_1,e_2)
| product(e_1,X0,e_3)
| ~ product(X0,e_2,e_1) ),
inference(renaming,[status(thm)],[c_1679]) ).
tcf(c_1681,plain,
( product(e_2,e_1,e_2)
| product(e_1,e_1,e_3)
| ~ product(e_1,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_1680]) ).
tcf(c_1696,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_1,e_1) ),
inference(global_subsumption_just,[status(thm)],[c_1201,c_101,c_94,c_113,c_236,c_240,c_1201,c_1528,c_1537,c_1681]) ).
tcf(c_1702,plain,
! [X0: $i] :
( equalish(X0,e_3)
| product(e_1,e_1,e_1)
| ~ product(e_1,e_2,X0) ),
inference(superposition,[status(thm)],[c_1696,c_83]) ).
tcf(c_1703,plain,
( product(e_3,e_1,e_4)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| product(e_1,e_1,e_1)
| ~ group_element(e_3)
| ~ group_element(e_2) ),
inference(superposition,[status(thm)],[c_1696,c_981]) ).
tcf(c_1706,plain,
! [X0: $i] :
( product(e_1,e_1,e_1)
| product(e_2,X0,e_3)
| ~ product(X0,e_1,e_2) ),
inference(superposition,[status(thm)],[c_1696,c_80]) ).
tcf(c_1719,plain,
( product(e_3,e_1,e_4)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| product(e_1,e_1,e_1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1703,c_99,c_100]) ).
tcf(c_1725,plain,
( equalish(e_1,e_3)
| product(e_1,e_1,e_1)
| ~ product(e_1,e_2,e_1) ),
inference(instantiation,[status(thm)],[c_1702]) ).
tcf(c_1726,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_1)
| ~ product(e_1,e_1,e_2) ),
inference(instantiation,[status(thm)],[c_1706]) ).
tcf(c_1727,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_1,e_1) ),
inference(global_subsumption_just,[status(thm)],[c_1228,c_1696]) ).
tcf(c_1734,plain,
( product(e_3,e_1,e_4)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| product(e_1,e_1,e_1)
| ~ group_element(e_3)
| ~ group_element(e_2) ),
inference(superposition,[status(thm)],[c_1727,c_1034]) ).
tcf(c_1737,plain,
! [X0: $i] :
( product(e_1,e_1,e_1)
| product(e_2,X0,e_3)
| ~ product(X0,e_1,e_2) ),
inference(superposition,[status(thm)],[c_1727,c_80]) ).
tcf(c_1750,plain,
( product(e_3,e_1,e_4)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| product(e_1,e_1,e_1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1734,c_99,c_100]) ).
tcf(c_1780,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_712]) ).
tcf(c_1782,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_706]) ).
tcf(c_1806,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_1) ),
inference(superposition,[status(thm)],[c_984,c_1706]) ).
tcf(c_1815,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_1) ),
inference(superposition,[status(thm)],[c_1037,c_1737]) ).
tcf(c_1838,plain,
! [X0: $i] :
( equalish(X0,e_3)
| product(e_1,e_1,e_1)
| ~ product(e_2,e_1,X0) ),
inference(superposition,[status(thm)],[c_1806,c_83]) ).
tcf(c_1839,plain,
( product(e_3,e_2,e_4)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| product(e_1,e_1,e_1)
| ~ group_element(e_3)
| ~ group_element(e_1) ),
inference(superposition,[status(thm)],[c_1806,c_981]) ).
tcf(c_1855,plain,
( product(e_3,e_2,e_4)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| product(e_1,e_1,e_1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1839,c_99,c_101]) ).
tcf(c_1861,plain,
( equalish(e_1,e_3)
| product(e_1,e_1,e_1)
| ~ product(e_2,e_1,e_1) ),
inference(instantiation,[status(thm)],[c_1838]) ).
tcf(c_1868,plain,
( product(e_3,e_2,e_4)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| product(e_1,e_1,e_1)
| ~ group_element(e_3)
| ~ group_element(e_1) ),
inference(superposition,[status(thm)],[c_1815,c_1034]) ).
tcf(c_1869,plain,
! [X0: $i] :
( equalish(e_1,X0)
| product(e_1,e_1,e_1)
| ~ product(e_2,X0,e_3) ),
inference(superposition,[status(thm)],[c_1815,c_82]) ).
tcf(c_1884,plain,
( product(e_3,e_2,e_4)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| product(e_1,e_1,e_1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1868,c_99,c_101]) ).
tcf(c_2087,plain,
( equalish(e_3,e_4)
| ~ product(e_4,e_1,e_3)
| ~ product(e_3,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_713]) ).
tcf(c_2089,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_707]) ).
tcf(c_2090,plain,
( equalish(e_4,e_3)
| ~ product(e_4,e_1,e_3)
| ~ product(e_3,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_704]) ).
tcf(c_2095,plain,
( product(e_3,e_2,e_4)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_1) ),
inference(global_subsumption_just,[status(thm)],[c_1317,c_96,c_268,c_987,c_1268,c_1269,c_1317,c_1861]) ).
tcf(c_2097,plain,
( product(e_3,e_2,e_4)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_2095,c_96,c_268,c_1861,c_2095]) ).
tcf(c_2098,plain,
( product(e_3,e_2,e_4)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_1) ),
inference(renaming,[status(thm)],[c_2097]) ).
tcf(c_2108,plain,
( product(e_4,e_3,e_4)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_1)
| ~ group_element(e_4)
| ~ group_element(e_2) ),
inference(superposition,[status(thm)],[c_2098,c_981]) ).
tcf(c_2109,plain,
! [X0: $i] :
( equalish(e_2,X0)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_1)
| ~ product(e_3,X0,e_4) ),
inference(superposition,[status(thm)],[c_2098,c_82]) ).
tcf(c_2111,plain,
! [X0: $i] :
( product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_1)
| product(e_2,X0,e_4)
| ~ product(X0,e_3,e_2) ),
inference(superposition,[status(thm)],[c_2098,c_80]) ).
tcf(c_2132,plain,
( product(e_4,e_3,e_4)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2108,c_98,c_100]) ).
tcf(c_2141,plain,
( equalish(e_2,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_1)
| ~ product(e_3,e_1,e_4) ),
inference(instantiation,[status(thm)],[c_2109]) ).
tcf(c_2143,plain,
( product(e_2,e_1,e_4)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_1)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_2111]) ).
tcf(c_2144,plain,
( product(e_3,e_2,e_4)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_1353,c_101,c_94,c_113,c_236,c_240,c_268,c_1077,c_1528,c_2095]) ).
tcf(c_2145,plain,
( product(e_3,e_2,e_4)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_1) ),
inference(renaming,[status(thm)],[c_2144]) ).
tcf(c_2155,plain,
( product(e_4,e_3,e_4)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_1)
| ~ group_element(e_4)
| ~ group_element(e_2) ),
inference(superposition,[status(thm)],[c_2145,c_1034]) ).
tcf(c_2179,plain,
( product(e_4,e_3,e_4)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2155,c_98,c_100]) ).
tcf(c_2189,plain,
( equalish(e_2,e_3)
| ~ product(e_1,e_3,e_3)
| ~ product(e_1,e_3,e_2) ),
inference(instantiation,[status(thm)],[c_723]) ).
tcf(c_2195,plain,
( equalish(e_3,e_2)
| ~ product(e_1,e_3,e_3)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_715]) ).
tcf(c_2196,plain,
! [X0: $i] :
( product(e_3,e_1,X0)
| ~ product(e_1,e_3,e_3)
| ~ product(e_3,e_3,X0) ),
inference(instantiation,[status(thm)],[c_773]) ).
tcf(c_2197,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_2196]) ).
tcf(c_2214,plain,
( equalish(e_3,e_2)
| ~ product(e_3,e_1,e_3)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_716]) ).
tcf(c_2221,plain,
( product(e_2,e_2,e_2)
| ~ product(e_2,e_1,e_2)
| ~ product(e_1,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_1172]) ).
tcf(c_2384,plain,
! [X0: $i] :
( product(e_1,e_2,X0)
| ~ product(e_2,e_3,e_1)
| ~ product(e_3,e_1,X0) ),
inference(instantiation,[status(thm)],[c_795]) ).
tcf(c_2385,plain,
( product(e_1,e_2,e_1)
| ~ product(e_3,e_1,e_1)
| ~ product(e_2,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_2384]) ).
tcf(c_2395,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_1526]) ).
tcf(c_2419,plain,
( equalish(e_1,e_4)
| ~ product(e_2,e_4,e_3)
| ~ product(e_2,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_1252]) ).
tcf(c_2608,plain,
( product(e_3,e_1,e_4)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_1,e_1,e_1) ),
inference(global_subsumption_just,[status(thm)],[c_1719,c_101,c_99,c_96,c_91,c_90,c_113,c_236,c_240,c_776,c_1377,c_1725,c_1726,c_1719,c_2214,c_2385]) ).
tcf(c_2622,plain,
! [X0: $i] :
( product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_1,e_1,e_1)
| product(e_1,X0,e_4)
| ~ product(X0,e_3,e_1) ),
inference(superposition,[status(thm)],[c_2608,c_80]) ).
tcf(c_2652,plain,
( product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_1,e_1,e_4)
| product(e_1,e_1,e_1)
| ~ product(e_1,e_3,e_1) ),
inference(instantiation,[status(thm)],[c_2622]) ).
tcf(c_2653,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_1750,c_101,c_94,c_90,c_113,c_236,c_240,c_1537,c_1696,c_2141,c_2195,c_2608,c_2652]) ).
tcf(c_2654,plain,
( product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_1,e_1,e_1) ),
inference(renaming,[status(thm)],[c_2653]) ).
tcf(c_2666,plain,
( equalish(e_1,e_3)
| product(e_2,e_3,e_2)
| product(e_1,e_1,e_1) ),
inference(superposition,[status(thm)],[c_2654,c_1869]) ).
tcf(c_2667,plain,
( product(e_2,e_3,e_2)
| product(e_1,e_1,e_1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2666,c_96]) ).
tcf(c_2671,plain,
! [X0: $i] :
( product(X0,e_1,e_3)
| ~ product(e_4,X0,e_3)
| ~ product(e_1,e_4,X0) ),
inference(instantiation,[status(thm)],[c_738]) ).
tcf(c_2691,plain,
( product(e_3,e_2,e_4)
| product(e_1,e_3,e_1)
| product(e_1,e_1,e_1) ),
inference(global_subsumption_just,[status(thm)],[c_1884,c_101,c_91,c_90,c_113,c_236,c_240,c_1279,c_1696,c_1855,c_2195]) ).
tcf(c_2703,plain,
! [X0: $i] :
( product(e_1,e_3,e_1)
| product(e_1,e_1,e_1)
| product(e_2,X0,e_4)
| ~ product(X0,e_3,e_2) ),
inference(superposition,[status(thm)],[c_2691,c_80]) ).
tcf(c_2746,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_3,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_2622,c_2667]) ).
tcf(c_2747,plain,
( product(e_2,e_3,e_2)
| product(e_1,e_1,e_1) ),
inference(renaming,[status(thm)],[c_2746]) ).
tcf(c_2756,plain,
! [X0: $i] :
( product(e_1,e_1,e_1)
| product(e_3,X0,e_2)
| ~ product(X0,e_2,e_3) ),
inference(superposition,[status(thm)],[c_2747,c_80]) ).
tcf(c_2784,plain,
( product(e_3,e_1,e_2)
| product(e_1,e_1,e_1)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_2756]) ).
tcf(c_2804,plain,
product(e_1,e_1,e_1),
inference(global_subsumption_just,[status(thm)],[c_2703,c_101,c_91,c_113,c_236,c_240,c_1377,c_1696,c_2784]) ).
tcf(c_2832,plain,
( product(e_4,e_3,e_4)
| product(e_1,e_3,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_4,e_1)
| product(e_2,e_4,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_2179,c_101,c_95,c_94,c_113,c_236,c_240,c_268,c_283,c_987,c_1077,c_1528,c_2132,c_2419,c_2804]) ).
tcf(c_2833,plain,
( product(e_4,e_3,e_4)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3) ),
inference(renaming,[status(thm)],[c_2832]) ).
tcf(c_2847,plain,
! [X0: $i] :
( equalish(e_4,X0)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| ~ product(X0,e_3,e_4) ),
inference(superposition,[status(thm)],[c_2833,c_81]) ).
tcf(c_2848,plain,
! [X0: $i] :
( product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_3,X0,e_4)
| ~ product(X0,e_4,e_3) ),
inference(superposition,[status(thm)],[c_2833,c_80]) ).
tcf(c_2882,plain,
( equalish(e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| ~ product(e_1,e_3,e_4) ),
inference(instantiation,[status(thm)],[c_2847]) ).
tcf(c_2972,plain,
( product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_2848,c_101,c_99,c_88,c_244,c_283,c_772,c_2143,c_2804,c_2882]) ).
tcf(c_2984,plain,
! [X0: $i] :
( equalish(e_4,X0)
| product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| ~ product(e_2,X0,e_2) ),
inference(superposition,[status(thm)],[c_2972,c_82]) ).
tcf(c_2986,plain,
! [X0: $i] :
( product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_4,X0,e_2)
| ~ product(X0,e_2,e_4) ),
inference(superposition,[status(thm)],[c_2972,c_80]) ).
tcf(c_3028,plain,
( product(e_4,e_3,e_2)
| product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_1) ),
inference(superposition,[status(thm)],[c_2145,c_2986]) ).
tcf(c_3389,plain,
( product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_2132,c_2972]) ).
tcf(c_3403,plain,
! [X0: $i] :
( product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_4,X0,e_2)
| ~ product(X0,e_2,e_4) ),
inference(superposition,[status(thm)],[c_3389,c_80]) ).
tcf(c_3443,plain,
( product(e_4,e_3,e_2)
| product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_1) ),
inference(superposition,[status(thm)],[c_2098,c_3403]) ).
tcf(c_3458,plain,
( product(e_4,e_3,e_2)
| product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_3443,c_283,c_2804,c_3028]) ).
tcf(c_3473,plain,
( product(e_2,e_4,e_4)
| product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_1) ),
inference(superposition,[status(thm)],[c_3458,c_2111]) ).
tcf(c_3521,plain,
( product(e_2,e_4,e_4)
| product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_3473,c_283,c_2804,c_3473]) ).
tcf(c_3535,plain,
! [X0: $i] :
( product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_4,X0,e_4)
| ~ product(X0,e_2,e_4) ),
inference(superposition,[status(thm)],[c_3521,c_80]) ).
tcf(c_3577,plain,
( product(e_4,e_3,e_4)
| product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_1) ),
inference(superposition,[status(thm)],[c_2098,c_3535]) ).
tcf(c_3723,plain,
( equalish(e_2,e_4)
| ~ product(e_2,e_4,e_4)
| ~ product(e_2,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_1102]) ).
tcf(c_3737,plain,
( product(e_3,e_1,e_3)
| ~ product(e_3,e_3,e_3)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_2196]) ).
tcf(c_3885,plain,
! [X0: $i] :
( product(e_4,e_4,e_2)
| ~ product(e_4,X0,e_4)
| ~ product(X0,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_903]) ).
tcf(c_3900,plain,
( product(e_4,e_4,e_2)
| ~ product(e_4,e_1,e_4)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_3885]) ).
tcf(c_3959,plain,
! [X0: $i] :
( product(e_4,e_3,X0)
| ~ product(e_3,e_2,e_4)
| ~ product(e_2,e_4,X0) ),
inference(instantiation,[status(thm)],[c_769]) ).
tcf(c_3964,plain,
( product(e_4,e_3,e_1)
| ~ product(e_3,e_2,e_4)
| ~ product(e_2,e_4,e_1) ),
inference(instantiation,[status(thm)],[c_3959]) ).
tcf(c_3983,plain,
( product(e_1,e_3,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_4,e_1) ),
inference(global_subsumption_just,[status(thm)],[c_2984,c_101,c_92,c_91,c_113,c_236,c_240,c_283,c_1377,c_1696,c_2784,c_2972,c_3473,c_3723]) ).
tcf(c_3984,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_1,e_2)
| product(e_1,e_3,e_3) ),
inference(renaming,[status(thm)],[c_3983]) ).
tcf(c_3985,plain,
( product(e_1,e_3,e_3)
| product(e_2,e_1,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_3984,c_101,c_99,c_98,c_94,c_91,c_90,c_89,c_88,c_87,c_113,c_236,c_240,c_268,c_283,c_291,c_306,c_314,c_744,c_750,c_772,c_776,c_895,c_920,c_987,c_1077,c_1264,c_1268,c_1269,c_1317,c_1377,c_1528,c_1696,c_1780,c_2089,c_2141,c_2214,c_2784,c_3900,c_3964,c_3984]) ).
tcf(c_3986,plain,
( product(e_2,e_1,e_2)
| product(e_1,e_3,e_3) ),
inference(renaming,[status(thm)],[c_3985]) ).
tcf(c_3992,plain,
( product(e_2,e_2,e_4)
| product(e_1,e_3,e_3)
| 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(superposition,[status(thm)],[c_3986,c_1034]) ).
tcf(c_4012,plain,
( product(e_2,e_2,e_4)
| product(e_1,e_3,e_3)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3992,c_100,c_101]) ).
tcf(c_4211,plain,
( product(e_2,e_1,e_3)
| ~ product(e_4,e_2,e_3)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_2671]) ).
tcf(c_4226,plain,
( product(e_2,e_1,e_2)
| product(e_1,e_3,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_3577,c_3986]) ).
tcf(c_4233,plain,
( product(e_2,e_2,e_4)
| product(e_1,e_3,e_3)
| 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(superposition,[status(thm)],[c_4226,c_981]) ).
tcf(c_4250,plain,
( product(e_2,e_2,e_4)
| product(e_1,e_3,e_3)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4233,c_100,c_101]) ).
tcf(c_4319,plain,
( product(e_2,e_2,e_4)
| product(e_1,e_3,e_3)
| product(e_1,e_2,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_4250,c_97,c_260,c_2221,c_2395,c_2804,c_3986,c_4012]) ).
tcf(c_4330,plain,
! [X0: $i] :
( equalish(e_2,X0)
| product(e_1,e_3,e_3)
| product(e_1,e_2,e_3)
| ~ product(X0,e_2,e_4) ),
inference(superposition,[status(thm)],[c_4319,c_81]) ).
tcf(c_4331,plain,
! [X0: $i] :
( product(e_1,e_3,e_3)
| product(e_1,e_2,e_3)
| product(e_2,X0,e_4)
| ~ product(X0,e_2,e_2) ),
inference(superposition,[status(thm)],[c_4319,c_80]) ).
tcf(c_4355,plain,
( equalish(e_2,e_1)
| product(e_1,e_3,e_3)
| product(e_1,e_2,e_3)
| ~ product(e_1,e_2,e_4) ),
inference(instantiation,[status(thm)],[c_4330]) ).
tcf(c_4357,plain,
( product(e_2,e_1,e_4)
| product(e_1,e_3,e_3)
| product(e_1,e_2,e_3)
| ~ product(e_1,e_2,e_2) ),
inference(instantiation,[status(thm)],[c_4331]) ).
tcf(c_4358,plain,
( product(e_1,e_3,e_3)
| product(e_1,e_2,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_4331,c_101,c_100,c_94,c_244,c_260,c_798,c_2804,c_4355,c_4357]) ).
tcf(c_4364,plain,
! [X0: $i] :
( equalish(X0,e_3)
| product(e_1,e_2,e_3)
| ~ product(e_1,e_3,X0) ),
inference(superposition,[status(thm)],[c_4358,c_83]) ).
tcf(c_4368,plain,
! [X0: $i] :
( product(e_1,e_2,e_3)
| product(e_3,X0,e_3)
| ~ product(X0,e_1,e_3) ),
inference(superposition,[status(thm)],[c_4358,c_80]) ).
tcf(c_4400,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_718]) ).
tcf(c_4456,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_3,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_4012,c_4358]) ).
tcf(c_4457,plain,
( product(e_1,e_3,e_3)
| product(e_1,e_2,e_3) ),
inference(renaming,[status(thm)],[c_4456]) ).
tcf(c_4463,plain,
( product(e_3,e_3,e_3)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_1)
| product(e_3,e_1,e_4)
| product(e_1,e_2,e_3)
| ~ group_element(e_3) ),
inference(superposition,[status(thm)],[c_4457,c_1034]) ).
tcf(c_4466,plain,
! [X0: $i] :
( product(e_1,e_2,e_3)
| product(e_3,X0,e_3)
| ~ product(X0,e_1,e_3) ),
inference(superposition,[status(thm)],[c_4457,c_80]) ).
tcf(c_4479,plain,
( product(e_3,e_3,e_3)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_1)
| product(e_3,e_1,e_4)
| product(e_1,e_2,e_3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4463,c_99]) ).
tcf(c_4491,plain,
( product(e_3,e_2,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_1,e_2,e_3) ),
inference(superposition,[status(thm)],[c_1040,c_4466]) ).
tcf(c_4538,plain,
( equalish(e_4,e_3)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| product(e_1,e_2,e_3)
| ~ group_element(e_3)
| ~ group_element(e_1) ),
inference(superposition,[status(thm)],[c_84,c_4364]) ).
tcf(c_4540,plain,
( product(e_1,e_3,e_3)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| product(e_1,e_2,e_3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4538,c_86,c_99,c_101]) ).
tcf(c_4571,plain,
( product(e_3,e_2,e_3)
| product(e_2,e_1,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_4491,c_101,c_94,c_90,c_113,c_236,c_240,c_268,c_1077,c_1528,c_2195,c_3986,c_4491]) ).
tcf(c_4579,plain,
! [X0: $i] :
( equalish(e_2,X0)
| product(e_2,e_1,e_2)
| ~ product(e_3,X0,e_3) ),
inference(superposition,[status(thm)],[c_4571,c_82]) ).
tcf(c_4580,plain,
! [X0: $i] :
( equalish(e_3,X0)
| product(e_2,e_1,e_2)
| ~ product(X0,e_2,e_3) ),
inference(superposition,[status(thm)],[c_4571,c_81]) ).
tcf(c_4581,plain,
! [X0: $i] :
( product(e_2,e_1,e_2)
| product(e_2,X0,e_3)
| ~ product(X0,e_3,e_2) ),
inference(superposition,[status(thm)],[c_4571,c_80]) ).
tcf(c_4600,plain,
( equalish(e_3,e_1)
| product(e_2,e_1,e_2)
| ~ product(e_1,e_2,e_3) ),
inference(instantiation,[status(thm)],[c_4580]) ).
tcf(c_4601,plain,
( equalish(e_2,e_1)
| product(e_2,e_1,e_2)
| ~ product(e_3,e_1,e_3) ),
inference(instantiation,[status(thm)],[c_4579]) ).
tcf(c_4645,plain,
! [X0: $i] :
( product(e_4,e_3,e_2)
| ~ product(e_3,X0,e_4)
| ~ product(X0,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_903]) ).
tcf(c_4660,plain,
( product(e_4,e_3,e_2)
| ~ product(e_3,e_1,e_4)
| ~ product(e_1,e_4,e_2) ),
inference(instantiation,[status(thm)],[c_4645]) ).
tcf(c_4683,plain,
( product(e_3,e_2,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_1,e_2,e_3) ),
inference(superposition,[status(thm)],[c_987,c_4368]) ).
tcf(c_4694,plain,
( product(e_1,e_3,e_3)
| product(e_1,e_3,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_4540,c_101,c_100,c_99,c_98,c_94,c_93,c_92,c_91,c_90,c_89,c_88,c_86,c_113,c_236,c_240,c_244,c_268,c_283,c_291,c_306,c_314,c_744,c_750,c_772,c_776,c_895,c_900,c_902,c_906,c_921,c_1077,c_1085,c_1261,c_1377,c_1378,c_1398,c_1528,c_1696,c_1780,c_2090,c_2784,c_3900,c_3986,c_4211,c_4358,c_4660]) ).
tcf(c_4700,plain,
! [X0: $i] :
( equalish(X0,e_3)
| product(e_1,e_3,e_2)
| ~ product(e_1,e_3,X0) ),
inference(superposition,[status(thm)],[c_4694,c_83]) ).
tcf(c_4701,plain,
( product(e_3,e_3,e_3)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_1)
| product(e_3,e_1,e_4)
| product(e_1,e_3,e_2)
| ~ group_element(e_3) ),
inference(superposition,[status(thm)],[c_4694,c_981]) ).
tcf(c_4720,plain,
( product(e_3,e_3,e_3)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_1)
| product(e_3,e_1,e_4)
| product(e_1,e_3,e_2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4701,c_99]) ).
tcf(c_4834,plain,
! [X0: $i] :
( product(e_2,e_1,e_2)
| ~ product(X0,e_3,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_4581,c_93,c_1081,c_1267,c_1266,c_4581]) ).
tcf(c_4913,plain,
( product(e_3,e_2,e_3)
| product(e_2,e_1,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_4683,c_4571]) ).
tcf(c_4923,plain,
! [X0: $i] :
( product(e_2,e_1,e_2)
| product(e_2,X0,e_3)
| ~ product(X0,e_3,e_2) ),
inference(superposition,[status(thm)],[c_4913,c_80]) ).
tcf(c_5076,plain,
( product(e_3,e_3,e_3)
| product(e_3,e_3,e_2)
| product(e_1,e_2,e_3) ),
inference(global_subsumption_just,[status(thm)],[c_4479,c_101,c_100,c_99,c_98,c_97,c_94,c_93,c_92,c_91,c_89,c_88,c_87,c_113,c_236,c_240,c_244,c_260,c_291,c_306,c_314,c_744,c_750,c_798,c_895,c_921,c_1260,c_1282,c_1377,c_1696,c_1782,c_2087,c_2189,c_2197,c_2221,c_2395,c_2784,c_3737,c_3900,c_4355,c_4357,c_4400,c_4601,c_4720]) ).
tcf(c_5078,plain,
( product(e_1,e_2,e_3)
| product(e_3,e_3,e_2) ),
inference(global_subsumption_just,[status(thm)],[c_5076,c_101,c_100,c_98,c_97,c_94,c_92,c_91,c_89,c_88,c_87,c_113,c_236,c_240,c_244,c_260,c_306,c_314,c_744,c_750,c_798,c_895,c_921,c_1260,c_1377,c_1696,c_1782,c_2087,c_2221,c_2395,c_2784,c_3737,c_3900,c_4355,c_4357,c_4601,c_5076]) ).
tcf(c_5079,plain,
( product(e_3,e_3,e_2)
| product(e_1,e_2,e_3) ),
inference(renaming,[status(thm)],[c_5078]) ).
tcf(c_5088,plain,
! [X0: $i] :
( product(e_1,e_2,e_3)
| product(e_3,X0,e_2)
| ~ product(X0,e_3,e_3) ),
inference(superposition,[status(thm)],[c_5079,c_80]) ).
tcf(c_5089,plain,
( product(e_2,e_1,e_2)
| product(e_1,e_2,e_3) ),
inference(superposition,[status(thm)],[c_5079,c_4834]) ).
tcf(c_5113,plain,
( product(e_3,e_1,e_2)
| product(e_1,e_2,e_3)
| ~ product(e_1,e_3,e_3) ),
inference(instantiation,[status(thm)],[c_5088]) ).
tcf(c_5235,plain,
product(e_2,e_1,e_2),
inference(global_subsumption_just,[status(thm)],[c_4923,c_91,c_4600,c_5089]) ).
tcf(c_5287,plain,
product(e_1,e_3,e_2),
inference(global_subsumption_just,[status(thm)],[c_4700,c_93,c_91,c_90,c_1378,c_2195,c_4600,c_4694,c_5089,c_5113]) ).
tcf(c_5294,plain,
( equalish(e_2,e_3)
| product(e_1,e_2,e_3) ),
inference(superposition,[status(thm)],[c_5287,c_4364]) ).
tcf(c_5295,plain,
product(e_1,e_2,e_3),
inference(forward_subsumption_resolution,[status(thm)],[c_5294,c_93]) ).
tcf(c_5329,plain,
! [X0: $i] :
( equalish(e_1,X0)
| ~ product(X0,e_2,e_3) ),
inference(superposition,[status(thm)],[c_5295,c_81]) ).
tcf(c_5330,plain,
! [X0: $i] :
( product(e_2,X0,e_3)
| ~ product(X0,e_1,e_2) ),
inference(superposition,[status(thm)],[c_5295,c_80]) ).
tcf(c_5370,plain,
product(e_2,e_2,e_3),
inference(superposition,[status(thm)],[c_5235,c_5330]) ).
tcf(c_5376,plain,
equalish(e_1,e_2),
inference(superposition,[status(thm)],[c_5370,c_5329]) ).
tcf(c_5377,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_5376,c_97]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP129-2.004 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Wed Sep 23 13:44:51 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.04/0.30 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.04/0.32 Running EPR theorem proving
% 0.04/0.32 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.06/0.32
% 0.06/0.32 % ======== iProver multi-core TPTP/SMT =========
% 0.06/0.32
% 0.06/0.33 % Detected problem language: tptp
% 0.06/0.33 % Proving...
% 0.79/1.02 % SZS status Started for theBenchmark.p
% 0.79/1.02 % SZS status Unsatisfiable for theBenchmark.p
% 0.79/1.02
% 0.79/1.02 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 0.79/1.02
% 0.79/1.02 % ------ iProver source info
% 0.79/1.02
% 0.79/1.02 % git: date: 2026-07-19 20:42:38 +0200
% 0.79/1.02 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 0.79/1.02 % git: non_committed_changes: false
% 0.79/1.02
% 0.79/1.02 % ------ Parsing...% successful
% 0.79/1.02
% 0.79/1.02
% 0.79/1.02 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_non_eq
% 0.79/1.02 %
% 0.79/1.02
% 0.79/1.02 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 0.79/1.02
% 0.79/1.02 % ------ Preprocessing...% ------ preprocesses with Option_epr_non_horn_non_eq
% 0.79/1.02 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 0.79/1.02 % ------ Proving...
% 0.79/1.02 % ------ Problem Properties
% 0.79/1.02
% 0.79/1.02 %
% 0.79/1.02 % clauses 24
% 0.79/1.02 % conjectures 1
% 0.79/1.02 % EPR 24
% 0.79/1.02 % Horn 23
% 0.79/1.02 % unary 19
% 0.79/1.02 % binary 0
% 0.79/1.02 % lits 37
% 0.79/1.02 % lits eq 0
% 0.79/1.02 % fd_pure 0
% 0.79/1.02 % fd_pseudo 0
% 0.79/1.02 % fd_cond 0
% 0.79/1.02 % fd_pseudo_cond 0
% 0.79/1.02 % AC symbols 0
% 0.79/1.02
% 0.79/1.02 % ------ Schedule EPR non Horn non eq is on
% 0.79/1.02
% 0.79/1.02 % ------ no equalities: superposition off
% 0.79/1.02
% 0.79/1.02 % ------ Input Options "--resolution_flag false" Time Limit: 70.
% 0.79/1.02
% 0.79/1.02
% 0.79/1.02 % ------
% 0.79/1.02 % Current options:
% 0.79/1.02 % ------
% 0.79/1.02
% 0.79/1.02
% 0.79/1.02 %
% 0.79/1.02
% 0.79/1.02 % ------ Proving...
% 0.79/1.02 %
% 0.79/1.02
% 0.79/1.02 % SZS status Unsatisfiable for theBenchmark.p
% 0.79/1.02
% 0.79/1.02 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 0.79/1.03
% 0.79/1.03
%------------------------------------------------------------------------------